diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-07-03 18:47:56 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-07-03 18:47:56 +0100 |
| commit | b5144a6f513c5c6e3344dcc935117706637ddd3f (patch) | |
| tree | 34bf07611d40da221c3023c0b24a82ec71e5cad3 /src/verilog/Value.v | |
| parent | 2fa04589bc1e2404235e95ca272fc403c7234fa4 (diff) | |
| download | vericert-b5144a6f513c5c6e3344dcc935117706637ddd3f.tar.gz vericert-b5144a6f513c5c6e3344dcc935117706637ddd3f.zip | |
Add new value type to fix Iop proof
Diffstat (limited to 'src/verilog/Value.v')
| -rw-r--r-- | src/verilog/Value.v | 23 |
1 files changed, 5 insertions, 18 deletions
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 : |