From 594c2825012d94675317f51cf6a3e97c2f88cd02 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Fri, 3 Jul 2020 21:05:45 +0100
Subject: Fixing HTLgenproof

---
 src/verilog/ValueInt.v | 21 +++++++++++++++------
 1 file changed, 15 insertions(+), 6 deletions(-)

(limited to 'src/verilog/ValueInt.v')

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.
-- 
cgit