No addmitted in Veriloggenproof

However, there may have been breaking changes to HTLgenproof.

4 files changed, 245 insertions, 100 deletions

diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v
index 1977f65..e02d759 100644
--- a/src/translation/HTLgen.v
+++ b/src/translation/HTLgen.v
@@ -402,7 +402,7 @@ Definition translate_arr_access (mem : AST.memory_chunk) (addr : Op.addressing)
     then ret (Vvari stack
                     (Vbinop Vdivu
                             (Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale))
-                            (ZToValue 4)))
+                            (Vlit (ZToValue 4))))
     else error (Errors.msg "HTLgen: translate_arr_access address misaligned")
   | Mint32, Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *)
     let a := Integers.Ptrofs.unsigned a in
@@ -510,32 +510,67 @@ Definition create_arr (i : option io) (sz : nat) (ln : nat) : mon (reg * nat) :=
 Definition stack_correct (sz : Z) : bool :=
   (0 <=? sz) && (sz <? Integers.Ptrofs.modulus) && (Z.modulo sz 4 =? 0).
 
+Definition max_pc_map (m : Maps.PTree.t stmnt) :=
+  PTree.fold (fun m pc i => Pos.max m pc) m 1%positive.
+
+Lemma max_pc_map_sound:
+  forall m pc i, m!pc = Some i -> Ple pc (max_pc_map m).
+Proof.
+  intros until i. unfold max_pc_function.
+  apply PTree_Properties.fold_rec with (P := fun c m => c!pc = Some i -> Ple pc m).
+  (* extensionality *)
+  intros. apply H0. rewrite H; auto.
+  (* base case *)
+  rewrite PTree.gempty. congruence.
+  (* inductive case *)
+  intros. rewrite PTree.gsspec in H2. destruct (peq pc k).
+  inv H2. xomega.
+  apply Ple_trans with a. auto. xomega.
+Qed.
+
+Lemma max_pc_wf :
+  forall m, Z.pos (max_pc_map m) <= Integers.Int.max_unsigned ->
+            map_well_formed m.
+Proof.
+  unfold map_well_formed. intros.
+  exploit list_in_map_inv. eassumption. intros [x [A B]]. destruct x.
+  apply Maps.PTree.elements_complete in B. apply max_pc_map_sound in B.
+  unfold Ple in B. apply Pos2Z.pos_le_pos in B. subst.
+  simplify. transitivity (Z.pos (max_pc_map m)); eauto.
+Qed.
+
 Definition transf_module (f: function) : mon module :=
   if stack_correct f.(fn_stacksize) then
-  do fin <- create_reg (Some Voutput) 1;
-  do rtrn <- create_reg (Some Voutput) 32;
-  do (stack, stack_len) <- create_arr None 32 (Z.to_nat (f.(fn_stacksize) / 4));
-  do _ <- collectlist (transf_instr fin rtrn stack) (Maps.PTree.elements f.(RTL.fn_code));
-  do _ <- collectlist (fun r => declare_reg (Some Vinput) r 32) f.(RTL.fn_params);
-  do start <- create_reg (Some Vinput) 1;
-  do rst <- create_reg (Some Vinput) 1;
-  do clk <- create_reg (Some Vinput) 1;
-  do current_state <- get;
-  ret (mkmodule
-         f.(RTL.fn_params)
-         current_state.(st_datapath)
-         current_state.(st_controllogic)
-         f.(fn_entrypoint)
-         current_state.(st_st)
-         stack
-         stack_len
-         fin
-         rtrn
-         start
-         rst
-         clk
-         current_state.(st_scldecls)
-         current_state.(st_arrdecls))
+    do fin <- create_reg (Some Voutput) 1;
+    do rtrn <- create_reg (Some Voutput) 32;
+    do (stack, stack_len) <- create_arr None 32 (Z.to_nat (f.(fn_stacksize) / 4));
+    do _ <- collectlist (transf_instr fin rtrn stack) (Maps.PTree.elements f.(RTL.fn_code));
+    do _ <- collectlist (fun r => declare_reg (Some Vinput) r 32) f.(RTL.fn_params);
+    do start <- create_reg (Some Vinput) 1;
+    do rst <- create_reg (Some Vinput) 1;
+    do clk <- create_reg (Some Vinput) 1;
+    do current_state <- get;
+    match zle (Z.pos (max_pc_map current_state.(st_datapath))) Integers.Int.max_unsigned,
+          zle (Z.pos (max_pc_map current_state.(st_controllogic))) Integers.Int.max_unsigned with
+    | left LEDATA, left LECTRL =>
+        ret (mkmodule
+           f.(RTL.fn_params)
+           current_state.(st_datapath)
+           current_state.(st_controllogic)
+           f.(fn_entrypoint)
+           current_state.(st_st)
+           stack
+           stack_len
+           fin
+           rtrn
+           start
+           rst
+           clk
+           current_state.(st_scldecls)
+           current_state.(st_arrdecls)
+           (conj (max_pc_wf _ LECTRL) (max_pc_wf _ LEDATA)))
+    | _, _ => error (Errors.msg "More than 2^32 states.")
+    end
   else error (Errors.msg "Stack size misalignment.").
 
 Definition max_state (f: function) : state :=
diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v
index 82d4cfc..305c14f 100644
--- a/src/translation/HTLgenproof.v
+++ b/src/translation/HTLgenproof.v
@@ -342,7 +342,6 @@ Section CORRECTNESS.
     intros (cu & tf & P & Q & R); exists tf; auto.
   Qed.
 
-
   Lemma functions_translated:
     forall (v: Values.val) (f: RTL.fundef),
       Genv.find_funct ge v = Some f ->
diff --git a/src/translation/Veriloggenproof.v b/src/translation/Veriloggenproof.v
index ee0aa64..5b467a7 100644
--- a/src/translation/Veriloggenproof.v
+++ b/src/translation/Veriloggenproof.v
@@ -16,7 +16,7 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-From compcert Require Import Smallstep Linking Integers.
+From compcert Require Import Smallstep Linking Integers Globalenvs.
 From coqup Require HTL.
 From coqup Require Import Coquplib Veriloggen Verilog ValueInt AssocMap.
 Require Import Lia.
@@ -89,6 +89,14 @@ Proof.
   rewrite H1. auto.
 Qed.
 
+Lemma unsigned_posToValue_le :
+  forall p,
+    Z.pos p <= Int.max_unsigned ->
+    0 < Int.unsigned (posToValue p).
+Proof.
+  intros. unfold posToValue. rewrite Int.unsigned_repr; lia.
+Qed.
+
 Lemma transl_list_fun_fst :
   forall p1 p2 a b,
     0 <= Z.pos p1 <= Int.max_unsigned ->
@@ -102,10 +110,17 @@ Proof.
   rewrite H1; auto.
 Qed.
 
+Lemma Zle_relax :
+  forall p q r,
+  p < q <= r ->
+  p <= q <= r.
+Proof. lia. Qed.
+Hint Resolve Zle_relax : verilogproof.
+
 Lemma transl_in :
   forall l p,
   0 <= Z.pos p <= Int.max_unsigned ->
-  (forall p0, In p0 (List.map fst l) -> 0 <= Z.pos p0 <= Int.max_unsigned) ->
+  (forall p0, In p0 (List.map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) ->
   In (Vlit (posToValue p)) (map fst (map transl_list_fun l)) ->
   In p (map fst l).
 Proof.
@@ -113,13 +128,14 @@ Proof.
   - simplify. auto.
   - intros. destruct a. simplify. destruct (peq p0 p); auto.
     right. inv H1. apply Vlit_inj in H. apply posToValue_inj in H; auto. contradiction.
+    auto with verilogproof.
     apply IHl; auto.
 Qed.
 
 Lemma transl_notin :
   forall l p,
     0 <= Z.pos p <= Int.max_unsigned ->
-    (forall p0, In p0 (List.map fst l) -> 0 <= Z.pos p0 <= Int.max_unsigned) ->
+    (forall p0, In p0 (List.map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) ->
     ~ In p (List.map fst l) -> ~ In (Vlit (posToValue p)) (List.map fst (transl_list l)).
 Proof.
   induction l; auto. intros. destruct a. unfold not in *. intros.
@@ -127,24 +143,88 @@ Proof.
   destruct (peq p0 p). apply H1. auto. apply H1.
   unfold transl_list in *. inv H2. apply Vlit_inj in H. apply posToValue_inj in H.
   contradiction.
-  apply H0; auto. auto.
+  auto with verilogproof. auto.
   right. apply transl_in; auto.
 Qed.
 
 Lemma transl_norepet :
   forall l,
-    (forall p0, In p0 (List.map fst l) -> 0 <= Z.pos p0 <= Int.max_unsigned) ->
+    (forall p0, In p0 (List.map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) ->
     list_norepet (List.map fst l) -> list_norepet (List.map fst (transl_list l)).
 Proof.
   induction l.
   - intros. simpl. apply list_norepet_nil.
   - destruct a. intros. simpl. apply list_norepet_cons.
-    inv H0. apply transl_notin. apply H. simplify; auto.
+    inv H0. apply transl_notin. apply Zle_relax. apply H. simplify; auto.
     intros. apply H. destruct (peq p0 p); subst; simplify; auto.
     assumption. apply IHl. intros. apply H. destruct (peq p0 p); subst; simplify; auto.
     simplify. inv H0. assumption.
 Qed.
 
+Lemma transl_list_correct :
+  forall l v ev f asr asa asrn asan asr' asa' asrn' asan',
+    (forall p0, In p0 (List.map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) ->
+    list_norepet (List.map fst l) ->
+    asr!ev = Some v ->
+    (forall p s,
+        In (p, s) l ->
+        v = posToValue p ->
+        stmnt_runp f
+                   {| assoc_blocking := asr; assoc_nonblocking := asrn |}
+                   {| assoc_blocking := asa; assoc_nonblocking := asan |}
+                   s
+                   {| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
+                   {| assoc_blocking := asa'; assoc_nonblocking := asan' |} ->
+        stmnt_runp f
+                   {| assoc_blocking := asr; assoc_nonblocking := asrn |}
+                   {| assoc_blocking := asa; assoc_nonblocking := asan |}
+                   (Vcase (Vvar ev) (transl_list l) (Some Vskip))
+                   {| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
+                   {| assoc_blocking := asa'; assoc_nonblocking := asan' |}).
+Proof.
+  induction l as [| a l IHl].
+  - contradiction.
+  - intros v ev f asr asa asrn asan asr' asa' asrn' asan' BOUND NOREP ASSOC p s IN EQ SRUN.
+    destruct a as [p' s']. simplify.
+    destruct (peq p p'); subst. eapply stmnt_runp_Vcase_match.
+    constructor. simplify. unfold AssocMap.find_assocmap, AssocMapExt.get_default.
+    rewrite ASSOC. trivial. constructor. auto.
+    inversion IN as [INV | INV]. inversion INV as [INV2]; subst. assumption.
+    inv NOREP. eapply in_map with (f := fst) in INV. contradiction.
+
+    eapply stmnt_runp_Vcase_nomatch. constructor. simplify.
+    unfold AssocMap.find_assocmap, AssocMapExt.get_default. rewrite ASSOC.
+    trivial. constructor. unfold not. intros. apply n. apply posToValue_inj.
+    apply Zle_relax. apply BOUND. right. inv IN. inv H0; contradiction.
+    eapply in_map with (f := fst) in H0. auto.
+    apply Zle_relax. apply BOUND; auto. auto.
+
+    eapply IHl. auto. inv NOREP. auto. eassumption. inv IN. inv H. contradiction. apply H.
+    trivial. assumption.
+Qed.
+Hint Resolve transl_list_correct : verilogproof.
+
+Lemma pc_wf :
+  forall A m p v,
+  (forall p0, In p0 (List.map fst (@AssocMap.elements A m)) -> 0 < Z.pos p0 <= Int.max_unsigned) ->
+  m!p = Some v ->
+  0 <= Z.pos p <= Int.max_unsigned.
+Proof.
+  intros A m p v LT S. apply Zle_relax. apply LT.
+  apply AssocMap.elements_correct in S. remember (p, v) as x.
+  exploit in_map. apply S. instantiate (1 := fst). subst. simplify. auto.
+Qed.
+
+Lemma mis_stepp_decl :
+  forall l asr asa f,
+    mis_stepp f asr asa (map Vdeclaration l) asr asa.
+Proof.
+  induction l.
+  - intros. constructor.
+  - intros. simplify. econstructor. constructor. auto.
+Qed.
+Hint Resolve mis_stepp_decl : verilogproof.
+
 Section CORRECTNESS.
 
   Variable prog: HTL.program.
@@ -152,58 +232,42 @@ Section CORRECTNESS.
 
   Hypothesis TRANSL : match_prog prog tprog.
 
-  Lemma transl_list_correct :
-  forall l v ev f asr asa asrn asan asr' asa' asrn' asan',
-    (forall p0, In p0 (List.map fst l) -> 0 <= Z.pos p0 <= Int.max_unsigned) ->
-    list_norepet (List.map fst l) ->
-    asr!ev = Some v ->
-    (forall p s,
-      In (p, s) l ->
-      v = posToValue p ->
-      stmnt_runp f
-                 {| assoc_blocking := asr; assoc_nonblocking := asrn |}
-                 {| assoc_blocking := asa; assoc_nonblocking := asan |}
-                 s
-                 {| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
-                 {| assoc_blocking := asa'; assoc_nonblocking := asan' |} ->
-      stmnt_runp f
-                 {| assoc_blocking := asr; assoc_nonblocking := asrn |}
-                 {| assoc_blocking := asa; assoc_nonblocking := asan |}
-                 (Vcase (Vvar ev) (transl_list l) (Some Vskip))
-                 {| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
-                 {| assoc_blocking := asa'; assoc_nonblocking := asan' |}).
+  Let ge : HTL.genv := Globalenvs.Genv.globalenv prog.
+  Let tge : genv := Globalenvs.Genv.globalenv tprog.
+
+  Lemma symbols_preserved:
+    forall (s: AST.ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
+  Proof. intros. eapply (Genv.find_symbol_match TRANSL). Qed.
+  Hint Resolve symbols_preserved : verilogproof.
+
+  Lemma function_ptr_translated:
+    forall (b: Values.block) (f: HTL.fundef),
+      Genv.find_funct_ptr ge b = Some f ->
+      exists tf,
+        Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = tf.
   Proof.
-    induction l as [| a l IHl].
-    - contradiction.
-    - intros v ev f asr asa asrn asan asr' asa' asrn' asan' BOUND NOREP ASSOC p s IN EQ SRUN.
-      destruct a as [p' s']. simplify.
-      destruct (peq p p'); subst. eapply stmnt_runp_Vcase_match.
-      constructor. simplify. unfold AssocMap.find_assocmap, AssocMapExt.get_default.
-      rewrite ASSOC. trivial. constructor. auto.
-      inversion IN as [INV | INV]. inversion INV as [INV2]; subst. assumption.
-      inv NOREP. eapply in_map with (f := fst) in INV. contradiction.
-
-      eapply stmnt_runp_Vcase_nomatch. constructor. simplify.
-      unfold AssocMap.find_assocmap, AssocMapExt.get_default. rewrite ASSOC.
-      trivial. constructor. unfold not. intros. apply n. apply posToValue_inj.
-      apply BOUND. right. inv IN. inv H0; contradiction. eapply in_map with (f := fst) in H0. auto.
-      apply BOUND; auto. auto.
-
-      eapply IHl. auto. inv NOREP. auto. eassumption. inv IN. inv H. contradiction. apply H.
-      trivial. assumption.
+    intros. exploit (Genv.find_funct_ptr_match TRANSL); eauto.
+    intros (cu & tf & P & Q & R); exists tf; auto.
   Qed.
+  Hint Resolve function_ptr_translated : verilogproof.
 
-  Lemma mis_stepp_decl :
-    forall l asr asa f,
-      mis_stepp f asr asa (map Vdeclaration l) asr asa.
+  Lemma functions_translated:
+    forall (v: Values.val) (f: HTL.fundef),
+      Genv.find_funct ge v = Some f ->
+      exists tf,
+        Genv.find_funct tge v = Some tf /\ transl_fundef f = tf.
   Proof.
-    induction l.
-    - intros. constructor.
-    - intros. simplify. econstructor. constructor. auto.
+    intros. exploit (Genv.find_funct_match TRANSL); eauto.
+    intros (cu & tf & P & Q & R); exists tf; auto.
   Qed.
+  Hint Resolve functions_translated : verilogproof.
 
-  Let ge : HTL.genv := Globalenvs.Genv.globalenv prog.
-  Let tge : genv := Globalenvs.Genv.globalenv tprog.
+  Lemma senv_preserved:
+    Senv.equiv (Genv.to_senv ge) (Genv.to_senv tge).
+  Proof.
+    intros. eapply (Genv.senv_match TRANSL).
+  Qed.
+  Hint Resolve senv_preserved : verilogproof.
 
   Theorem transl_step_correct :
     forall (S1 : HTL.state) t S2,
@@ -214,7 +278,10 @@ Section CORRECTNESS.
   Proof.
     induction 1; intros R1 MSTATE; inv MSTATE.
     - econstructor; split. apply Smallstep.plus_one. econstructor.
-      assumption. assumption. eassumption. trivial.
+      assumption. assumption. eassumption. apply valueToPos_posToValue.
+      split. lia.
+      eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _].
+      split. lia. apply HP. eassumption. eassumption.
       econstructor. econstructor. eapply stmnt_runp_Vcond_false. econstructor. econstructor.
       simpl. unfold find_assocmap. unfold AssocMapExt.get_default.
       rewrite H. trivial.
@@ -222,25 +289,33 @@ Section CORRECTNESS.
       econstructor. simpl. auto. auto.
 
       eapply transl_list_correct.
-      assert (forall p0 : positive, In p0 (map fst (Maps.PTree.elements (HTL.mod_controllogic m)))
-                                    -> 0 <= Z.pos p0 <= Int.max_unsigned) by admit; auto.
+      intros. split. lia. pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _]. auto.
       apply Maps.PTree.elements_keys_norepet. eassumption.
-      2: { apply valueToPos_inj. assert (0 < Int.unsigned ist) by admit; auto.
-      admit. rewrite valueToPos_posToValue.  trivial. admit. }
+      2: { apply valueToPos_inj. apply unsigned_posToValue_le.
+           eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _].
+           split. lia. apply HP. eassumption. eassumption.
+           apply unsigned_posToValue_le. eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP.
+           destruct HP as [HP _].
+           split. lia. apply HP. eassumption. eassumption. trivial.
+      }
       apply Maps.PTree.elements_correct. eassumption. eassumption.
 
       econstructor. econstructor.
 
       eapply transl_list_correct.
-      assert (forall p0 : positive, In p0 (map fst (Maps.PTree.elements (HTL.mod_datapath m)))
-                                    -> 0 <= Z.pos p0 <= Int.max_unsigned) by admit; auto.
+      intros. split. lia. pose proof (HTL.mod_wf m) as HP. destruct HP as [_ HP]. auto.
       apply Maps.PTree.elements_keys_norepet. eassumption.
-      2: { apply valueToPos_inj. assert (0 < Int.unsigned ist) by admit; auto.
-      admit. rewrite valueToPos_posToValue.  trivial. admit. }
+      2: { apply valueToPos_inj. apply unsigned_posToValue_le.
+           eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _].
+           split. lia. apply HP. eassumption. eassumption.
+           apply unsigned_posToValue_le. eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP.
+           destruct HP as [HP _].
+           split. lia. apply HP. eassumption. eassumption. trivial.
+      }
       apply Maps.PTree.elements_correct. eassumption. eassumption.
 
       apply mis_stepp_decl. trivial. trivial. simpl. eassumption. auto.
-      constructor; assumption.
+      rewrite valueToPos_posToValue. constructor; assumption. lia.
 
     - econstructor; split. apply Smallstep.plus_one. apply step_finish. assumption. eassumption.
       constructor; assumption.
@@ -250,12 +325,44 @@ Section CORRECTNESS.
     - inv H3. econstructor; split. apply Smallstep.plus_one. constructor. trivial.
 
       apply match_state. assumption.
-  Admitted.
+  Qed.
+  Hint Resolve transl_step_correct : verilogproof.
+
+  Lemma transl_initial_states :
+    forall s1 : Smallstep.state (HTL.semantics prog),
+      Smallstep.initial_state (HTL.semantics prog) s1 ->
+      exists s2 : Smallstep.state (Verilog.semantics tprog),
+        Smallstep.initial_state (Verilog.semantics tprog) s2 /\ match_states s1 s2.
+  Proof.
+    induction 1.
+    econstructor; split. econstructor.
+    apply (Genv.init_mem_transf TRANSL); eauto.
+    rewrite symbols_preserved.
+    replace (AST.prog_main tprog) with (AST.prog_main prog); eauto.
+    symmetry; eapply Linking.match_program_main; eauto.
+    exploit function_ptr_translated; eauto. intros [tf [A B]].
+    inv B. eauto.
+    constructor.
+  Qed.
+  Hint Resolve transl_initial_states : verilogproof.
+
+  Lemma transl_final_states :
+    forall (s1 : Smallstep.state (HTL.semantics prog))
+           (s2 : Smallstep.state (Verilog.semantics tprog))
+           (r : Integers.Int.int),
+      match_states s1 s2 ->
+      Smallstep.final_state (HTL.semantics prog) s1 r ->
+      Smallstep.final_state (Verilog.semantics tprog) s2 r.
+  Proof.
+    intros. inv H0. inv H. inv H3. constructor. reflexivity.
+  Qed.
+  Hint Resolve transl_final_states : verilogproof.
 
   Theorem transf_program_correct:
     forward_simulation (HTL.semantics prog) (Verilog.semantics tprog).
-    Admitted.
-
+  Proof.
+    eapply Smallstep.forward_simulation_plus; eauto with verilogproof.
+    apply senv_preserved.
+  Qed.
 
 End CORRECTNESS.
-
diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v
index a7a6ecc..3ba5b59 100644
--- a/src/verilog/HTL.v
+++ b/src/verilog/HTL.v
@@ -36,6 +36,11 @@ Definition node := positive.
 Definition datapath := PTree.t Verilog.stmnt.
 Definition controllogic := PTree.t Verilog.stmnt.
 
+Definition map_well_formed {A : Type} (m : PTree.t A) : Prop :=
+  forall p0 : positive,
+    In p0 (map fst (Maps.PTree.elements m)) ->
+    Z.pos p0 <= Integers.Int.max_unsigned.
+
 Record module: Type :=
   mkmodule {
     mod_params : list reg;
@@ -52,6 +57,7 @@ Record module: Type :=
     mod_clk : reg;
     mod_scldecls : AssocMap.t (option Verilog.io * Verilog.scl_decl);
     mod_arrdecls : AssocMap.t (option Verilog.io * Verilog.arr_decl);
+    mod_wf : (map_well_formed mod_controllogic /\ map_well_formed mod_datapath);
   }.
 
 Definition fundef := AST.fundef module.
@@ -97,16 +103,15 @@ Inductive state : Type :=
 
 Inductive step : genv -> state -> Events.trace -> state -> Prop :=
 | step_module :
-    forall g m st sf ctrl data ist
+    forall g m st sf ctrl data
       asr asa
       basr1 basa1 nasr1 nasa1
       basr2 basa2 nasr2 nasa2
       asr' asa'
-      f stval pstval,
+      f pstval,
       asr!(mod_reset m) = Some (ZToValue 0) ->
       asr!(mod_finish m) = Some (ZToValue 0) ->
-      asr!(m.(mod_st)) = Some ist ->
-      valueToPos ist = st ->
+      asr!(m.(mod_st)) = Some (posToValue st) ->
       m.(mod_controllogic)!st = Some ctrl ->
       m.(mod_datapath)!st = Some data ->
       Verilog.stmnt_runp f
@@ -115,8 +120,7 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop :=
         ctrl
         (Verilog.mkassociations basr1 nasr1)
         (Verilog.mkassociations basa1 nasa1) ->
-      basr1!(m.(mod_st)) = Some ist ->
-      valueToPos ist = st ->
+      basr1!(m.(mod_st)) = Some (posToValue st) ->
       Verilog.stmnt_runp f
         (Verilog.mkassociations basr1 nasr1)
         (Verilog.mkassociations basa1 nasa1)
@@ -125,8 +129,8 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop :=
         (Verilog.mkassociations basa2 nasa2) ->
       asr' = Verilog.merge_regs nasr2 basr2 ->
       asa' = Verilog.merge_arrs nasa2 basa2 ->
-      asr'!(m.(mod_st)) = Some stval ->
-      valueToPos stval = pstval ->
+      asr'!(m.(mod_st)) = Some (posToValue pstval) ->
+      Z.pos pstval <= Integers.Int.max_unsigned ->
       step g (State sf m st asr asa) Events.E0 (State sf m pstval asr' asa')
 | step_finish :
     forall g m st asr asa retval sf,