Merge branch 'develop' into arrays-proof

2 files changed, 19 insertions, 13 deletions

diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v
index 713a373..7cc0861 100644
--- a/src/translation/HTLgenspec.v
+++ b/src/translation/HTLgenspec.v
@@ -350,10 +350,9 @@ Proof.
   econstructor; simpl; trivial.
   intros.
   inv_incr.
-  assert (st_controllogic s8 = st_controllogic s2) by congruence.
-  rewrite <- H10.
-  assert (st_datapath s8 = st_datapath s2) by congruence.
-  assert (st_st s5 = st_st s2) by congruence.
-  rewrite H80. rewrite H81. rewrite H82.
+  assert (STC: st_controllogic s8 = st_controllogic s2) by congruence.
+  assert (STD: st_datapath s8 = st_datapath s2) by congruence.
+  assert (STST: st_st s8 = st_st s2) by congruence.
+  rewrite STC. rewrite STD. rewrite STST.
   eauto with htlspec.
 Qed.
diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v
index a21064c..fffbb81 100644
--- a/src/verilog/HTL.v
+++ b/src/verilog/HTL.v
@@ -47,10 +47,13 @@ Record module: Type :=
     mod_return : reg
   }.
 
+Definition fundef := AST.fundef module.
+
+Definition program := AST.program fundef unit.
+
 (** * Operational Semantics *)
 
-Definition genv := Globalenvs.Genv.t unit unit.
-Definition genv_empty := Globalenvs.Genv.empty_genv unit unit nil.
+Definition genv := Globalenvs.Genv.t fundef unit.
 
 Inductive state : Type :=
 | State :
@@ -84,15 +87,19 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop :=
     step g (State m st assoc) t (Returnstate retval).
 Hint Constructors step : htl.
 
-Inductive initial_state (m : module) : state -> Prop :=
-| initial_state_intro : forall st,
-    st = m.(mod_entrypoint) ->
-    initial_state m (State m st empty_assocmap).
+Inductive initial_state (p: program): state -> Prop :=
+  | initial_state_intro: forall b m0 st m,
+      let ge := Globalenvs.Genv.globalenv p in
+      Globalenvs.Genv.init_mem p = Some m0 ->
+      Globalenvs.Genv.find_symbol ge p.(AST.prog_main) = Some b ->
+      Globalenvs.Genv.find_funct_ptr ge b = Some (AST.Internal m) ->
+      st = m.(mod_entrypoint) ->
+      initial_state p (State m st empty_assocmap).
 
 Inductive final_state : state -> Integers.int -> Prop :=
 | final_state_intro : forall retval retvali,
     value_int_eqb retval retvali = true ->
     final_state (Returnstate retval) retvali.
 
-Definition semantics (m : module) :=
-  Smallstep.Semantics step (initial_state m) final_state genv_empty.
+Definition semantics (m : program) :=
+  Smallstep.Semantics step (initial_state m) final_state (Globalenvs.Genv.globalenv m).