From e568448eeddb13f8da8583f18e8e8f35956e6896 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 2 Jul 2020 16:13:37 +0100 Subject: Push current state --- src/verilog/Value.v | 2 ++ 1 file changed, 2 insertions(+) (limited to 'src/verilog/Value.v') diff --git a/src/verilog/Value.v b/src/verilog/Value.v index 8ba5138..dc163de 100644 --- a/src/verilog/Value.v +++ b/src/verilog/Value.v @@ -39,6 +39,8 @@ Record value : Type := vword: word vsize }. +Search N.of_nat. + (** ** Value conversions Various conversions to different number types such as [N], [Z], [positive] and -- cgit From 74819dfa35ee60feb81811247d59775bd66630d0 Mon Sep 17 00:00:00 2001 From: James Pollard Date: Thu, 2 Jul 2020 17:00:14 +0100 Subject: Complete ZToValue_valueToNat. --- src/verilog/Value.v | 27 ++++++++++++++++++--------- 1 file changed, 18 insertions(+), 9 deletions(-) (limited to 'src/verilog/Value.v') diff --git a/src/verilog/Value.v b/src/verilog/Value.v index dc163de..116986b 100644 --- a/src/verilog/Value.v +++ b/src/verilog/Value.v @@ -21,6 +21,7 @@ From bbv Require Import Word. From bbv Require HexNotation WordScope. From Coq Require Import ZArith.ZArith FSets.FMapPositive Lia. From compcert Require Import lib.Integers common.Values. +From coqup Require Import Coquplib. (* end hide *) (** * Value @@ -454,17 +455,25 @@ Proof. unfold wordBin. repeat (rewrite wordToN_NToWord_2); auto. Qed. -(*Lemma ZToValue_valueToNat : +Lemma ZToValue_valueToNat : forall x sz, - sz > 0 -> - (x < 2^(Z.of_nat sz))%Z -> + (sz > 0)%nat -> + (0 <= x < 2^(Z.of_nat sz))%Z -> valueToNat (ZToValue sz x) = Z.to_nat x. Proof. - destruct x; intros; unfold ZToValue, valueToNat; simpl. + destruct x; intros; unfold ZToValue, valueToNat; crush. - rewrite wzero'_def. apply wordToNat_wzero. - rewrite posToWord_nat. rewrite wordToNat_natToWord_2. trivial. - unfold Z.of_nat in *. destruct sz eqn:?. omega. simpl in H0. - rewrite <- Pos2Z.inj_pow_pos in H0. Search (Z.pos _ < Z.pos _)%Z. - Search Pos.to_nat (_ < _). (* Pos2Nat.inj_lt *) - Search "inj" positive nat. -*) + clear H1. + lazymatch goal with + | [ H : context[(_ < ?x)%Z] |- _ ] => replace x with (Z.of_nat (Z.to_nat x)) in H + end. + 2: { apply Z2Nat.id; apply Z.pow_nonneg; lia. } + + rewrite Z2Nat.inj_pow in H2; crush. + replace (Pos.to_nat 2) with 2%nat in H2 by reflexivity. + rewrite Nat2Z.id in H2. + rewrite <- positive_nat_Z in H2. + apply Nat2Z.inj_lt in H2. + assumption. +Qed. -- cgit From 1d8afa5949cd192620e4649ae32df49bca4da3f8 Mon Sep 17 00:00:00 2001 From: James Pollard Date: Thu, 2 Jul 2020 21:57:03 +0100 Subject: Switch to uvalueToZ in lessdef. --- src/verilog/Value.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src/verilog/Value.v') diff --git a/src/verilog/Value.v b/src/verilog/Value.v index 116986b..acabcf2 100644 --- a/src/verilog/Value.v +++ b/src/verilog/Value.v @@ -304,8 +304,8 @@ Inductive val_value_lessdef: val -> value -> Prop := val_value_lessdef (Vint i) v' | val_value_lessdef_ptr: forall b off v', - off = Ptrofs.repr (valueToZ v') -> - (Z.modulo (valueToZ v') 4) = 0%Z -> + off = Ptrofs.repr (uvalueToZ v') -> + (Z.modulo (uvalueToZ v') 4) = 0%Z -> val_value_lessdef (Vptr b off) v' | lessdef_undef: forall v, val_value_lessdef Vundef v. -- cgit From 0b480d489a91f0d418523933b5e35288fcec65b1 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 3 Jul 2020 12:14:39 +0100 Subject: Updates to Iop proof --- src/verilog/Value.v | 79 ++++++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 78 insertions(+), 1 deletion(-) (limited to 'src/verilog/Value.v') diff --git a/src/verilog/Value.v b/src/verilog/Value.v index acabcf2..23ce0f7 100644 --- a/src/verilog/Value.v +++ b/src/verilog/Value.v @@ -88,9 +88,18 @@ Definition intToValue (i : Integers.int) : value := Definition valueToInt (i : value) : Integers.int := Int.repr (uvalueToZ i). +Definition ptrToValue (i : Integers.ptrofs) : value := + ZToValue Ptrofs.wordsize (Ptrofs.unsigned i). + +Definition valueToPtr (i : value) : Integers.ptrofs := + Ptrofs.repr (uvalueToZ i). + Definition valToValue (v : Values.val) : option value := match v with | Values.Vint i => Some (intToValue i) + | Values.Vptr b off => if Z.eqb (Z.modulo (uvalueToZ (ptrToValue off)) 4) 0%Z + then Some (ptrToValue off) + else None | Values.Vundef => Some (ZToValue 32 0%Z) | _ => None end. @@ -304,7 +313,7 @@ Inductive val_value_lessdef: val -> value -> Prop := val_value_lessdef (Vint i) v' | val_value_lessdef_ptr: forall b off v', - off = Ptrofs.repr (uvalueToZ v') -> + off = valueToPtr v' -> (Z.modulo (uvalueToZ v') 4) = 0%Z -> val_value_lessdef (Vptr b off) v' | lessdef_undef: forall v, val_value_lessdef Vundef v. @@ -382,6 +391,41 @@ Proof. apply Z.lt_le_pred in H. apply H. Qed. +Lemma valueToPtr_ptrToValue : + forall v, + valueToPtr (ptrToValue v) = v. +Proof. + intros. + unfold valueToPtr, ptrToValue. rewrite uvalueToZ_ZToValue. auto using Ptrofs.repr_unsigned. + split. apply Ptrofs.unsigned_range_2. + assert ((Ptrofs.unsigned v <= Ptrofs.max_unsigned)%Z) by apply Ptrofs.unsigned_range_2. + apply Z.lt_le_pred in H. apply H. +Qed. + +Lemma intToValue_valueToInt : + forall v, + vsize v = 32%nat -> + intToValue (valueToInt v) = v. +Proof. + intros. unfold valueToInt, intToValue. rewrite Int.unsigned_repr_eq. + unfold ZToValue, uvalueToZ. unfold Int.modulus. unfold Int.wordsize. unfold Wordsize_32.wordsize. + pose proof (uwordToZ_bound (vword v)). + rewrite Z.mod_small. rewrite <- H. rewrite ZToWord_uwordToZ. destruct v; auto. + rewrite <- H. rewrite two_power_nat_equiv. apply H0. +Qed. + +Lemma ptrToValue_valueToPtr : + forall v, + vsize v = 32%nat -> + ptrToValue (valueToPtr v) = v. +Proof. + intros. unfold valueToPtr, ptrToValue. rewrite Ptrofs.unsigned_repr_eq. + unfold ZToValue, uvalueToZ. unfold Ptrofs.modulus. unfold Ptrofs.wordsize. unfold Wordsize_Ptrofs.wordsize. + pose proof (uwordToZ_bound (vword v)). + rewrite Z.mod_small. rewrite <- H. rewrite ZToWord_uwordToZ. destruct v; auto. + rewrite <- H. rewrite two_power_nat_equiv. apply H0. +Qed. + Lemma valToValue_lessdef : forall v v', valToValue v = Some v' -> @@ -391,6 +435,10 @@ Proof. destruct v; try discriminate; constructor. unfold valToValue in H. inversion H. symmetry. apply valueToInt_intToValue. + inv H. destruct (uvalueToZ (ptrToValue i) mod 4 =? 0); try discriminate. + inv H1. symmetry. apply valueToPtr_ptrToValue. + inv H. destruct (uvalueToZ (ptrToValue i) mod 4 =? 0) eqn:?; try discriminate. + inv H1. apply Z.eqb_eq. apply Heqb0. Qed. Lemma boolToValue_ValueToBool : @@ -418,6 +466,17 @@ Proof. rewrite ZToWord_plus; auto. Qed. +Lemma zadd_vplus3 : + forall w1 w2, + (wordToN w1 + wordToN w2 < Npow2 32)%N -> + valueToN (vplus (mkvalue 32 w1) (mkvalue 32 w2) eq_refl) = + (valueToN (mkvalue 32 w1) + valueToN (mkvalue 32 w2))%N. +Proof. + intros. unfold vplus, map_word2. rewrite unify_word_unfold. unfold valueToN. + simplify. unfold wplus. unfold wordBin. Search wordToN NToWord. + rewrite wordToN_NToWord_2. trivial. assumption. +Qed. + Lemma wordsize_32 : Int.wordsize = 32%nat. Proof. auto. Qed. @@ -431,6 +490,24 @@ Proof. rewrite Int.repr_unsigned. auto. rewrite wordsize_32. omega. Qed. +Lemma intadd_vplus2 : + forall v1 v2 EQ, + Int.add (valueToInt v1) (valueToInt v2) = valueToInt (vplus v1 v2 EQ). +Proof. + intros. unfold Int.add, valueToInt, intToValue. repeat (rewrite Int.unsigned_repr). + rewrite zadd_vplus3. trivial. + +Lemma valadd_vplus : + forall v1 v2 v1' v2' v v' EQ, + val_value_lessdef v1 v1' -> + val_value_lessdef v2 v2' -> + Val.add v1 v2 = v -> + vplus v1' v2' EQ = v' -> + val_value_lessdef v v'. +Proof. + intros. inv H; inv H0; constructor; simplify. + - + Lemma zsub_vminus : forall sz z1 z2, (sz > 0)%nat -> -- cgit From 2fa04589bc1e2404235e95ca272fc403c7234fa4 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 3 Jul 2020 12:58:21 +0100 Subject: Addition to int_add_v2 --- src/verilog/Value.v | 16 +++++++++++++--- 1 file changed, 13 insertions(+), 3 deletions(-) (limited to 'src/verilog/Value.v') diff --git a/src/verilog/Value.v b/src/verilog/Value.v index 23ce0f7..b80b614 100644 --- a/src/verilog/Value.v +++ b/src/verilog/Value.v @@ -473,7 +473,7 @@ Lemma zadd_vplus3 : (valueToN (mkvalue 32 w1) + valueToN (mkvalue 32 w2))%N. Proof. intros. unfold vplus, map_word2. rewrite unify_word_unfold. unfold valueToN. - simplify. unfold wplus. unfold wordBin. Search wordToN NToWord. + simplify. unfold wplus. unfold wordBin. rewrite wordToN_NToWord_2. trivial. assumption. Qed. @@ -490,12 +490,22 @@ Proof. rewrite Int.repr_unsigned. auto. rewrite wordsize_32. omega. Qed. +Lemma vadd_vplus : + forall v1 v2 EQ, + uvalueToZ v1 + uvalueToZ v2 = uvalueToZ (vplus v1 v2 EQ). +Proof. + Admitted. + Lemma intadd_vplus2 : forall v1 v2 EQ, + vsize v1 = 32%nat -> Int.add (valueToInt v1) (valueToInt v2) = valueToInt (vplus v1 v2 EQ). Proof. intros. unfold Int.add, valueToInt, intToValue. repeat (rewrite Int.unsigned_repr). - rewrite zadd_vplus3. trivial. + rewrite (@vadd_vplus v1 v2 EQ). trivial. + unfold uvalueToZ. Search word "bound". pose proof (@uwordToZ_bound (vsize v2) (vword v2)). + rewrite H in EQ. rewrite <- EQ in H0. + (*rewrite zadd_vplus3. trivia*) Lemma valadd_vplus : forall v1 v2 v1' v2' v v' EQ, @@ -506,7 +516,7 @@ Lemma valadd_vplus : val_value_lessdef v v'. Proof. intros. inv H; inv H0; constructor; simplify. - - + Abort. Lemma zsub_vminus : forall sz z1 z2, -- cgit From b5144a6f513c5c6e3344dcc935117706637ddd3f Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 3 Jul 2020 18:47:56 +0100 Subject: Add new value type to fix Iop proof --- src/verilog/Value.v | 23 +++++------------------ 1 file changed, 5 insertions(+), 18 deletions(-) (limited to 'src/verilog/Value.v') diff --git a/src/verilog/Value.v b/src/verilog/Value.v index b80b614..2718a46 100644 --- a/src/verilog/Value.v +++ b/src/verilog/Value.v @@ -466,16 +466,9 @@ Proof. rewrite ZToWord_plus; auto. Qed. -Lemma zadd_vplus3 : - forall w1 w2, - (wordToN w1 + wordToN w2 < Npow2 32)%N -> - valueToN (vplus (mkvalue 32 w1) (mkvalue 32 w2) eq_refl) = - (valueToN (mkvalue 32 w1) + valueToN (mkvalue 32 w2))%N. -Proof. - intros. unfold vplus, map_word2. rewrite unify_word_unfold. unfold valueToN. - simplify. unfold wplus. unfold wordBin. - rewrite wordToN_NToWord_2. trivial. assumption. -Qed. +Lemma ZToValue_eq : + forall w1, + (mkvalue 32 w1) = (ZToValue 32 (wordToZ w1)). Admitted. Lemma wordsize_32 : Int.wordsize = 32%nat. @@ -490,13 +483,7 @@ Proof. rewrite Int.repr_unsigned. auto. rewrite wordsize_32. omega. Qed. -Lemma vadd_vplus : - forall v1 v2 EQ, - uvalueToZ v1 + uvalueToZ v2 = uvalueToZ (vplus v1 v2 EQ). -Proof. - Admitted. - -Lemma intadd_vplus2 : +(*Lemma intadd_vplus2 : forall v1 v2 EQ, vsize v1 = 32%nat -> Int.add (valueToInt v1) (valueToInt v2) = valueToInt (vplus v1 v2 EQ). @@ -504,7 +491,7 @@ Proof. intros. unfold Int.add, valueToInt, intToValue. repeat (rewrite Int.unsigned_repr). rewrite (@vadd_vplus v1 v2 EQ). trivial. unfold uvalueToZ. Search word "bound". pose proof (@uwordToZ_bound (vsize v2) (vword v2)). - rewrite H in EQ. rewrite <- EQ in H0. + rewrite H in EQ. rewrite <- EQ in H0 at 3.*) (*rewrite zadd_vplus3. trivia*) Lemma valadd_vplus : -- cgit From 855ca59a303efd32f1979f4e508edb4ddb43adac Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 7 Jul 2020 09:47:40 +0100 Subject: No admitted in Deterministic proof --- src/verilog/Value.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/verilog/Value.v') diff --git a/src/verilog/Value.v b/src/verilog/Value.v index 2718a46..af2b822 100644 --- a/src/verilog/Value.v +++ b/src/verilog/Value.v @@ -468,7 +468,7 @@ Qed. Lemma ZToValue_eq : forall w1, - (mkvalue 32 w1) = (ZToValue 32 (wordToZ w1)). Admitted. + (mkvalue 32 w1) = (ZToValue 32 (wordToZ w1)). Abort. Lemma wordsize_32 : Int.wordsize = 32%nat. -- cgit