From 0c360ec297c42d73c1090958d061447c2bfbe31b Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Sun, 28 Jun 2020 23:48:06 +0100
Subject: Fix proof again with Verilog semantics changes

---
 src/translation/HTLgenproof.v | 12 +++++++++++-
 src/verilog/Value.v           | 12 ++++++++++++
 2 files changed, 23 insertions(+), 1 deletion(-)

(limited to 'src')

diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v
index 753dccf..2f296f2 100644
--- a/src/translation/HTLgenproof.v
+++ b/src/translation/HTLgenproof.v
@@ -18,7 +18,7 @@
 
 From compcert Require RTL Registers AST Integers.
 From compcert Require Import Globalenvs Memory.
-From coqup Require Import Coquplib HTLgenspec HTLgen Value AssocMap Array IntegerExtra ZExtra.
+From coqup Require Import Coquplib HTLgenspec HTLgen Value AssocMap Array IntegerExtra.
 From coqup Require HTL Verilog.
 
 Require Import Lia.
@@ -427,6 +427,7 @@ Section CORRECTNESS.
       split.
       apply Smallstep.plus_one.
       eapply HTL.step_module; eauto.
+      apply assumption_32bit.
       (* processing of state *)
       econstructor.
       simplify.
@@ -646,6 +647,7 @@ Section CORRECTNESS.
         eexists. split.
         eapply Smallstep.plus_one.
         eapply HTL.step_module; eauto.
+        apply assumption_32bit.
         econstructor. econstructor. econstructor. simplify.
         econstructor. econstructor. econstructor. simplify.
         eapply Verilog.erun_Vbinop with (EQ := ?[EQ1]). (* FIXME: These will be shelved and cause sadness. *)
@@ -859,6 +861,7 @@ Section CORRECTNESS.
         eexists. split.
         eapply Smallstep.plus_one.
         eapply HTL.step_module; eauto.
+        apply assumption_32bit.
         econstructor. econstructor. econstructor. simplify.
         econstructor. econstructor. econstructor. simplify.
         eapply Verilog.erun_Vbinop with (EQ := ?[EQ3]). (* FIXME: These will be shelved and cause sadness. *)
@@ -1037,6 +1040,7 @@ Section CORRECTNESS.
         eexists. split.
         eapply Smallstep.plus_one.
         eapply HTL.step_module; eauto.
+        apply assumption_32bit.
         econstructor. econstructor. econstructor. simplify.
         econstructor. econstructor. econstructor. econstructor. simplify.
 
@@ -1201,6 +1205,7 @@ Section CORRECTNESS.
         eexists. split.
         eapply Smallstep.plus_one.
         eapply HTL.step_module; eauto.
+        apply assumption_32bit.
         econstructor. econstructor. econstructor.
         eapply Verilog.stmnt_runp_Vnonblock_arr. simplify.
         econstructor.
@@ -1454,6 +1459,7 @@ Section CORRECTNESS.
         eexists. split.
         eapply Smallstep.plus_one.
         eapply HTL.step_module; eauto.
+        apply assumption_32bit.
         econstructor. econstructor. econstructor.
         eapply Verilog.stmnt_runp_Vnonblock_arr. simplify.
         econstructor.
@@ -1672,6 +1678,7 @@ Section CORRECTNESS.
         eexists. split.
         eapply Smallstep.plus_one.
         eapply HTL.step_module; eauto.
+        apply assumption_32bit.
         econstructor. econstructor. econstructor.
         eapply Verilog.stmnt_runp_Vnonblock_arr. simplify.
         econstructor. econstructor. econstructor. econstructor.
@@ -1856,6 +1863,7 @@ Section CORRECTNESS.
 
     - eexists. split. apply Smallstep.plus_one.
       eapply HTL.step_module; eauto.
+      apply assumption_32bit.
       eapply Verilog.stmnt_runp_Vnonblock_reg with
           (rhsval := if b then posToValue 32 ifso else posToValue 32 ifnot).
 
@@ -1966,6 +1974,7 @@ Section CORRECTNESS.
       eapply Smallstep.plus_two.
       
       eapply HTL.step_module; eauto.
+      apply assumption_32bit.
       constructor.
       econstructor; simpl; trivial.
       econstructor; simpl; trivial.
@@ -1998,6 +2007,7 @@ Section CORRECTNESS.
     - econstructor. split.
       eapply Smallstep.plus_two.
       eapply HTL.step_module; eauto.
+      apply assumption_32bit.
       constructor.
       econstructor; simpl; trivial.
       econstructor; simpl; trivial.
diff --git a/src/verilog/Value.v b/src/verilog/Value.v
index 52a87e3..e7b2362 100644
--- a/src/verilog/Value.v
+++ b/src/verilog/Value.v
@@ -345,6 +345,18 @@ Proof.
   simpl. rewrite <- Pos2Z.inj_pow_pos. trivial.
 Qed.
 
+Lemma valueToPos_posToValue :
+  forall p, valueToPos (posToValueAuto p) = p.
+Proof.
+  intros. unfold valueToPos, posToValueAuto.
+  rewrite uvalueToZ_ZToValue. auto. rewrite positive_nat_Z.
+  split. apply Zle_0_pos.
+
+  assert (p < 2 ^ (Pos.size p))%positive by apply Pos.size_gt.
+  inversion H. rewrite <- Z.compare_lt_iff. rewrite <- H1.
+  simpl. rewrite <- Pos2Z.inj_pow_pos. trivial.
+Qed.
+
 Lemma valueToInt_intToValue :
   forall v,
   valueToInt (intToValue v) = v.
-- 
cgit