diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-06-30 00:29:41 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-06-30 00:29:41 +0100 |
| commit | 9a640d4f50b93a9d5f9b48e10b0c4cbfa7f0680f (patch) | |
| tree | d21cbc18dc3fda48ce4adff336d8f035583ee385 /src | |
| parent | 8a260a8b81617e192fc929e0189fd3df1327f80a (diff) | |
| download | vericert-kvx-9a640d4f50b93a9d5f9b48e10b0c4cbfa7f0680f.tar.gz vericert-kvx-9a640d4f50b93a9d5f9b48e10b0c4cbfa7f0680f.zip | |
Make the proofs more concise
Diffstat (limited to 'src')
| -rw-r--r-- | src/verilog/Value.v | 38 |
1 files changed, 21 insertions, 17 deletions
diff --git a/src/verilog/Value.v b/src/verilog/Value.v index 3c5ed04..8ba5138 100644 --- a/src/verilog/Value.v +++ b/src/verilog/Value.v @@ -397,15 +397,15 @@ Proof. destruct b; auto. Qed. Local Open Scope Z. -Ltac eq_op H := +Ltac word_op_value H := intros; unfold uvalueToZ, ZToValue; simpl; rewrite unify_word_unfold; - rewrite <- H; rewrite uwordToZ_ZToWord; auto. + rewrite <- H; rewrite uwordToZ_ZToWord_full; auto; omega. Lemma zadd_vplus : - forall z1 z2, - 0 <= z1 + z2 < 2 ^ 32 -> - uvalueToZ (vplus (ZToValue 32 z1) (ZToValue 32 z2) eq_refl) = z1 + z2. -Proof. eq_op ZToWord_plus. Qed. + forall sz z1 z2, + (sz > 0)%nat -> + uvalueToZ (vplus (ZToValue sz z1) (ZToValue sz z2) eq_refl) = (z1 + z2) mod 2 ^ Z.of_nat sz. +Proof. word_op_value ZToWord_plus. Qed. Lemma zadd_vplus2 : forall z1 z2, @@ -415,26 +415,30 @@ Proof. rewrite ZToWord_plus; auto. Qed. +Lemma wordsize_32 : + Int.wordsize = 32%nat. +Proof. auto. Qed. + Lemma intadd_vplus : forall i1 i2, valueToInt (vplus (intToValue i1) (intToValue i2) eq_refl) = Int.add i1 i2. Proof. - intros. unfold Int.add, valueToInt, intToValue. rewrite zadd_vplus2. - rewrite uvalueToZ_ZToValue_full. rewrite <- Int.unsigned_repr_eq. - rewrite Int.repr_unsigned. auto. omega. + intros. unfold Int.add, valueToInt, intToValue. rewrite zadd_vplus. + rewrite <- Int.unsigned_repr_eq. + rewrite Int.repr_unsigned. auto. rewrite wordsize_32. omega. Qed. Lemma zsub_vminus : - forall z1 z2, - 0 <= z1 - z2 < 2 ^ 32 -> - uvalueToZ (vminus (ZToValue 32 z1) (ZToValue 32 z2) eq_refl) = z1 - z2. -Proof. eq_op ZToWord_minus. Qed. + forall sz z1 z2, + (sz > 0)%nat -> + uvalueToZ (vminus (ZToValue sz z1) (ZToValue sz z2) eq_refl) = (z1 - z2) mod 2 ^ Z.of_nat sz. +Proof. word_op_value ZToWord_minus. Qed. Lemma zmul_vmul : - forall z1 z2, - 0 <= z1 * z2 < 2 ^ 32 -> - uvalueToZ (vmul (ZToValue 32 z1) (ZToValue 32 z2) eq_refl) = z1 * z2. -Proof. eq_op ZToWord_mult. Qed. + forall sz z1 z2, + (sz > 0)%nat -> + uvalueToZ (vmul (ZToValue sz z1) (ZToValue sz z2) eq_refl) = (z1 * z2) mod 2 ^ Z.of_nat sz. +Proof. word_op_value ZToWord_mult. Qed. Local Open Scope N. Lemma zdiv_vdiv : |