Remove admitted in mis_stepp_Vdecl

3 files changed, 12 insertions, 9 deletions

diff --git a/src/translation/Veriloggen.v b/src/translation/Veriloggen.v
index f0ec576..f5d5fa7 100644
--- a/src/translation/Veriloggen.v
+++ b/src/translation/Veriloggen.v
@@ -28,12 +28,12 @@ Definition transl_list_fun (a : node * Verilog.stmnt) :=
 Definition transl_list st := map transl_list_fun st.
 
 Definition scl_to_Vdecl_fun (a : reg * (option io * scl_decl)) :=
-  match a with (r, (io, VScalar sz)) => Vdeclaration (Vdecl io r sz) end.
+  match a with (r, (io, VScalar sz)) => (Vdecl io r sz) end.
 
 Definition scl_to_Vdecl scldecl := map scl_to_Vdecl_fun scldecl.
 
 Definition arr_to_Vdeclarr_fun (a : reg * (option io * arr_decl)) :=
-  match a with (r, (io, VArray sz l)) => Vdeclaration (Vdeclarr io r sz l) end.
+  match a with (r, (io, VArray sz l)) => (Vdeclarr io r sz l) end.
 
 Definition arr_to_Vdeclarr arrdecl := map arr_to_Vdeclarr_fun arrdecl.
 
@@ -45,7 +45,7 @@ Definition transl_module (m : HTL.module) : Verilog.module :=
                                                (Vnonblock (Vvar m.(mod_st)) (Vlit (posToValue m.(mod_entrypoint))))
                                                (Vcase (Vvar m.(mod_st)) case_el_ctrl (Some Vskip)))
       :: Valways (Vposedge m.(mod_clk)) (Vcase (Vvar m.(mod_st)) case_el_data (Some Vskip))
-      :: (arr_to_Vdeclarr (AssocMap.elements m.(mod_arrdecls))
+      :: List.map Vdeclaration (arr_to_Vdeclarr (AssocMap.elements m.(mod_arrdecls))
                           ++ scl_to_Vdecl (AssocMap.elements m.(mod_scldecls))) in
   Verilog.mkmodule m.(mod_start)
                    m.(mod_reset)
diff --git a/src/translation/Veriloggenproof.v b/src/translation/Veriloggenproof.v
index 3052d03..ee0aa64 100644
--- a/src/translation/Veriloggenproof.v
+++ b/src/translation/Veriloggenproof.v
@@ -195,8 +195,12 @@ Section CORRECTNESS.
 
   Lemma mis_stepp_decl :
     forall l asr asa f,
-      mis_stepp f asr asa l asr asa.
-  Admitted.
+      mis_stepp f asr asa (map Vdeclaration l) asr asa.
+  Proof.
+    induction l.
+    - intros. constructor.
+    - intros. simplify. econstructor. constructor. auto.
+  Qed.
 
   Let ge : HTL.genv := Globalenvs.Genv.globalenv prog.
   Let tge : genv := Globalenvs.Genv.globalenv tprog.
diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v
index 1513330..064474a 100644
--- a/src/verilog/Verilog.v
+++ b/src/verilog/Verilog.v
@@ -610,8 +610,8 @@ Inductive mi_stepp : fext -> reg_associations -> arr_associations ->
     stmnt_runp f sr0 sa0 st sr1 sa1 ->
     mi_stepp f sr0 sa0 (Valways_comb c st) sr1 sa1
 | mi_stepp_Vdecl :
-    forall f sr sa lhs rhs io,
-    mi_stepp f sr sa (Vdeclaration (Vdecl io lhs rhs)) sr sa.
+    forall f sr sa d,
+    mi_stepp f sr sa (Vdeclaration d) sr sa.
 Hint Constructors mi_stepp : verilog.
 
 Inductive mis_stepp : fext -> reg_associations -> arr_associations ->
@@ -743,8 +743,7 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop :=
     forall g m asr i r sf pc mst asa,
     mst = mod_st m ->
     step g (Returnstate (Stackframe r m pc asr asa :: sf) i) Events.E0
-         (State sf m pc ((asr # mst <- (posToValue pc)) # r <- i)
-                asa).
+         (State sf m pc ((asr # mst <- (posToValue pc)) # r <- i) asa).
 Hint Constructors step : verilog.
 
 Inductive initial_state (p: program): state -> Prop :=