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') 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