diff options
author | Yann Herklotz <git@yannherklotz.com> | 2020-07-03 21:05:45 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2020-07-03 21:05:45 +0100 |
commit | 594c2825012d94675317f51cf6a3e97c2f88cd02 (patch) | |
tree | 19c6b85504a9040cb48161325cdda14208ae9155 /src/verilog/ValueInt.v | |
parent | b5144a6f513c5c6e3344dcc935117706637ddd3f (diff) | |
download | vericert-kvx-594c2825012d94675317f51cf6a3e97c2f88cd02.tar.gz vericert-kvx-594c2825012d94675317f51cf6a3e97c2f88cd02.zip |
Fixing HTLgenproof
Diffstat (limited to 'src/verilog/ValueInt.v')
-rw-r--r-- | src/verilog/ValueInt.v | 21 |
1 files changed, 15 insertions, 6 deletions
diff --git a/src/verilog/ValueInt.v b/src/verilog/ValueInt.v index cc1d404..dff7b5c 100644 --- a/src/verilog/ValueInt.v +++ b/src/verilog/ValueInt.v @@ -138,6 +138,21 @@ Lemma uvalueToZ_ZToValue : uvalueToZ (ZToValue z) = z. Proof. auto using Int.unsigned_repr. Qed. +Lemma valueToPos_posToValue : + forall v, + 0 <= Z.pos v <= Int.max_unsigned -> + valueToPos (posToValue v) = v. +Proof. + unfold valueToPos, posToValue. + intros. rewrite Int.unsigned_repr. + apply Pos2Z.id. assumption. +Qed. + +Lemma valueToInt_intToValue : + forall v, + valueToInt (intToValue v) = v. +Proof. auto. Qed. + Lemma valToValue_lessdef : forall v v', valToValue v = Some v' -> @@ -152,9 +167,3 @@ Proof. inv H. destruct (uvalueToZ (ptrToValue i) mod 4 =? 0) eqn:?; try discriminate. inv H1. apply Z.eqb_eq. apply Heqb0. Qed. - -Local Open Scope Z. - -Ltac word_op_value H := - intros; unfold uvalueToZ, ZToValue; simpl; rewrite unify_word_unfold; - rewrite <- H; rewrite uwordToZ_ZToWord_full; auto; omega. |