diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-07-03 12:58:21 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-07-03 12:58:21 +0100 |
| commit | 2fa04589bc1e2404235e95ca272fc403c7234fa4 (patch) | |
| tree | 7e35e11075001f86a9767bb2886770ea28b03301 /src | |
| parent | 0b480d489a91f0d418523933b5e35288fcec65b1 (diff) | |
| download | vericert-2fa04589bc1e2404235e95ca272fc403c7234fa4.tar.gz vericert-2fa04589bc1e2404235e95ca272fc403c7234fa4.zip | |
Addition to int_add_v2
Diffstat (limited to 'src')
| -rw-r--r-- | src/verilog/Value.v | 16 |
1 files changed, 13 insertions, 3 deletions
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, |