From 8398615fea7ab754854cb10e16e86de6415f1f2d Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Mon, 29 Jun 2020 16:55:08 +0100
Subject: Work on addition proof

---
 src/verilog/Value.v | 22 +++++++++++++++++++++-
 1 file changed, 21 insertions(+), 1 deletion(-)

(limited to 'src')

diff --git a/src/verilog/Value.v b/src/verilog/Value.v
index e7b2362..c380ca7 100644
--- a/src/verilog/Value.v
+++ b/src/verilog/Value.v
@@ -108,6 +108,12 @@ Definition boolToValue (sz : nat) (b : bool) : value :=
 Definition unify_word (sz1 sz2 : nat) (w1 : word sz2): sz1 = sz2 -> word sz1.
 intros; subst; assumption. Defined.
 
+Lemma unify_word_unfold :
+  forall sz w,
+  unify_word sz sz w eq_refl = w.
+Proof.
+  intros. unfold unify_word. Admitted.
+
 Definition value_eq_size:
   forall v1 v2 : value, { vsize v1 = vsize v2 } + { True }.
 Proof.
@@ -382,7 +388,21 @@ Qed.
 Lemma boolToValue_ValueToBool :
   forall b,
   valueToBool (boolToValue 32 b) = b.
-Proof. destruct b; unfold valueToBool, boolToValue; simpl; trivial. Qed.
+Proof. destruct b; auto. Qed.
+
+Lemma intToValue_eq_size :
+  forall n1 n2,
+  vsize (intToValue n1) = vsize (intToValue n2).
+Proof. auto. Qed.
+
+Local Open Scope Z.
+
+Lemma zadd_vplus :
+  forall z1 z2,
+  valueToZ (vplus (ZToValue 32 z1) (ZToValue 32 z2) eq_refl) = z1 + z2.
+Proof.
+  intros. unfold valueToZ, ZToValue. simpl.
+  Admitted.
 
 (*Lemma ZToValue_valueToNat :
   forall x sz,
-- 
cgit 


From 7e59d2723fb9c5b4631f5eac1e99ae8956871a7f Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Mon, 29 Jun 2020 16:59:31 +0100
Subject: Develop compiles again

---
 src/translation/HTLgen.v          | 10 +++++-----
 src/translation/HTLgenproof.v     |  2 +-
 src/translation/Veriloggenproof.v |  6 ++++--
 3 files changed, 10 insertions(+), 8 deletions(-)

(limited to 'src')

diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v
index 59fb70a..b32ed9d 100644
--- a/src/translation/HTLgen.v
+++ b/src/translation/HTLgen.v
@@ -294,24 +294,24 @@ Definition translate_eff_addressing (a: Op.addressing) (args: list reg) : mon ex
   | Op.Aindexed off, r1::nil =>
     if (check_address_parameter_signed off)
     then ret (boplitz Vadd r1 off)
-    else error (Errors.msg "Veriloggen: translate_eff_addressing address misaligned")
+    else error (Errors.msg "Veriloggen: translate_eff_addressing (Aindexed): address misaligned")
   | Op.Ascaled scale offset, r1::nil =>
     if (check_address_parameter_signed scale) && (check_address_parameter_signed offset)
     then ret (Vbinop Vadd (boplitz Vmul r1 scale) (Vlit (ZToValue 32 offset)))
-    else error (Errors.msg "Veriloggen: translate_eff_addressing address misaligned")
+    else error (Errors.msg "Veriloggen: translate_eff_addressing (Ascaled): address misaligned")
   | Op.Aindexed2 offset, r1::r2::nil =>
     if (check_address_parameter_signed offset)
     then ret (Vbinop Vadd (Vvar r1) (boplitz Vadd r2 offset))
-    else error (Errors.msg "Veriloggen: translate_eff_addressing address misaligned")
+    else error (Errors.msg "Veriloggen: translate_eff_addressing (Aindexed2): address misaligned")
   | Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *)
     if (check_address_parameter_signed scale) && (check_address_parameter_signed offset)
     then ret (Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale))
-    else error (Errors.msg "Veriloggen: translate_eff_addressing address misaligned")
+    else error (Errors.msg "Veriloggen: translate_eff_addressing (Aindexed2scaled): address misaligned")
   | Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *)
     let a := Integers.Ptrofs.unsigned a in
     if (check_address_parameter_unsigned a)
     then ret (Vlit (ZToValue 32 a))
-    else error (Errors.msg "Veriloggen: translate_eff_addressing address misaligned")
+    else error (Errors.msg "Veriloggen: translate_eff_addressing (Ainstack): address misaligned")
   | _, _ => error (Errors.msg "Veriloggen: translate_eff_addressing unsuported addressing")
   end.
 
diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v
index 2f296f2..6dd0688 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.
+From coqup Require Import Coquplib HTLgenspec HTLgen Value AssocMap Array IntegerExtra ZExtra.
 From coqup Require HTL Verilog.
 
 Require Import Lia.
diff --git a/src/translation/Veriloggenproof.v b/src/translation/Veriloggenproof.v
index db96949..ca4ecab 100644
--- a/src/translation/Veriloggenproof.v
+++ b/src/translation/Veriloggenproof.v
@@ -69,12 +69,14 @@ Section CORRECTNESS.
         match_states S1 R1 ->
         exists R2, Smallstep.plus step tge R1 t R2 /\ match_states S2 R2.
   Proof.
-    induction 1; intros R1 MSTATE; inv MSTATE; econstructor; split.
+(*    induction 1; intros R1 MSTATE; inv MSTATE; econstructor; split.
     - apply Smallstep.plus_one. econstructor. eassumption. trivial.
-      * econstructor. econstructor.
+      * econstructor. econstructor.*)
+    Admitted.
 
   Theorem transf_program_correct:
     forward_simulation (HTL.semantics prog) (Verilog.semantics tprog).
+    Admitted.
 
 
 End CORRECTNESS.
-- 
cgit