From cf9949a5151aa9ed86554fb31c2a56fad0614a10 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Thu, 25 Jun 2020 18:04:49 +0100
Subject: Progress on proof of Veriloggen

---
 src/translation/Veriloggenproof.v | 33 +++++++++++++++++++--------------
 src/verilog/HTL.v                 |  4 +++-
 src/verilog/Verilog.v             |  2 ++
 3 files changed, 24 insertions(+), 15 deletions(-)

diff --git a/src/translation/Veriloggenproof.v b/src/translation/Veriloggenproof.v
index 825cb7e..e556c69 100644
--- a/src/translation/Veriloggenproof.v
+++ b/src/translation/Veriloggenproof.v
@@ -17,8 +17,8 @@
  *)
 
 From compcert Require Import Smallstep Linking.
-From coqup Require Import Veriloggen.
-From coqup Require HTL Verilog.
+From coqup Require HTL.
+From coqup Require Import Coquplib Veriloggen Verilog.
 
 Definition match_prog (prog : HTL.program) (tprog : Verilog.program) :=
   match_program (fun cu f tf => tf = transl_fundef f) eq prog tprog.
@@ -29,47 +29,52 @@ Proof.
   intros. eapply match_transform_program_contextual. auto.
 Qed.
 
-Inductive match_stacks : list HTL.stackframe -> list Verilog.stackframe -> Prop :=
+Inductive match_stacks : list HTL.stackframe -> list stackframe -> Prop :=
 | match_stack :
     forall res m pc reg_assoc arr_assoc hstk vstk,
       match_stacks hstk vstk ->
       match_stacks (HTL.Stackframe res m pc reg_assoc arr_assoc :: hstk)
-                   (Verilog.Stackframe res (transl_module m) pc
+                   (Stackframe res (transl_module m) pc
                                        reg_assoc arr_assoc :: vstk)
 | match_stack_nil : match_stacks nil nil.
 
-Inductive match_states : HTL.state -> Verilog.state -> Prop :=
+Inductive match_states : HTL.state -> state -> Prop :=
 | match_state :
     forall m st reg_assoc arr_assoc hstk vstk,
       match_stacks hstk vstk ->
       match_states (HTL.State hstk m st reg_assoc arr_assoc)
-                   (Verilog.State vstk (transl_module m) st reg_assoc arr_assoc)
+                   (State vstk (transl_module m) st reg_assoc arr_assoc)
 | match_returnstate :
     forall v hstk vstk,
       match_stacks hstk vstk ->
-      match_states (HTL.Returnstate hstk v) (Verilog.Returnstate vstk v)
+      match_states (HTL.Returnstate hstk v) (Returnstate vstk v)
 | match_initial_call :
     forall m,
-      match_states (HTL.Callstate nil m nil) (Verilog.Callstate nil (transl_module m) nil).
+      match_states (HTL.Callstate nil m nil) (Callstate nil (transl_module m) nil).
 
 Section CORRECTNESS.
 
   Variable prog: HTL.program.
-  Variable tprog: Verilog.program.
+  Variable tprog: program.
 
   Hypothesis TRANSL : match_prog prog tprog.
 
   Let ge : HTL.genv := Globalenvs.Genv.globalenv prog.
-  Let tge : Verilog.genv := Globalenvs.Genv.globalenv tprog.
+  Let tge : genv := Globalenvs.Genv.globalenv tprog.
 
-  Theorem transl_step_correct:
+  Lemma stmnt_in_case :
+    exists e st,
+
+  Theorem transl_step_correct :
     forall (S1 : HTL.state) t S2,
       HTL.step ge S1 t S2 ->
-      forall (R1 : Verilog.state),
+      forall (R1 : state),
         match_states S1 R1 ->
-        exists R2, Smallstep.plus Verilog.step tge R1 t R2 /\ match_states S2 R2.
+        exists R2, Smallstep.plus step tge R1 t R2 /\ match_states S2 R2.
   Proof.
-    induction 1; intros R1 MSTATE.
+    induction 1; intros R1 MSTATE; inv MSTATE; econstructor; split.
+    - apply Smallstep.plus_one. econstructor. econstructor.
+      * econstructor.
 
   Theorem transf_program_correct:
     forward_simulation (HTL.semantics prog) (Verilog.semantics tprog).
diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v
index 0bf5072..a3623f0 100644
--- a/src/verilog/HTL.v
+++ b/src/verilog/HTL.v
@@ -99,12 +99,14 @@ Inductive state : Type :=
 
 Inductive step : genv -> state -> Events.trace -> state -> Prop :=
 | step_module :
-    forall g m st sf ctrl data
+    forall g m st sf ctrl data ist
       asr asa
       basr1 basa1 nasr1 nasa1
       basr2 basa2 nasr2 nasa2
       asr' asa'
       f stval pstval,
+      asr!(m.(mod_st)) = Some ist ->
+      valueToPos ist = st ->
       m.(mod_controllogic)!st = Some ctrl ->
       m.(mod_datapath)!st = Some data ->
       Verilog.stmnt_runp f
diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v
index 9c05fc9..d476710 100644
--- a/src/verilog/Verilog.v
+++ b/src/verilog/Verilog.v
@@ -713,6 +713,8 @@ Definition empty_stack (m : module) : assocmap_arr :=
 Inductive step : genv -> state -> Events.trace -> state -> Prop :=
   | step_module :
       forall asr asa asr' asa' basr1 nasr1 basa1 nasa1 f stval pstval m sf st g,
+      asr!(m.(mod_st)) = Some ist ->
+      valueToPos ist = st ->
       mis_stepp f (mkassociations asr empty_assocmap)
                   (mkassociations asa (empty_stack m))
                   m.(mod_body)
-- 
cgit