Work on the match_states definition

3 files changed, 26 insertions, 17 deletions

diff --git a/src/hls/RTLBlockgenproof.v b/src/hls/RTLBlockgenproof.v
index f57af34..a0a1ee8 100644
--- a/src/hls/RTLBlockgenproof.v
+++ b/src/hls/RTLBlockgenproof.v
@@ -115,7 +115,12 @@ Variant match_states : RTL.state -> RTLBlock.state -> Prop :=
   forall stk stk' f tf sp pc rs m pc' ps bb
          (TF: transl_function f = OK tf)
          (PC: find_block_spec tf.(fn_code) pc pc')
-         (STK: Forall2 match_stackframe stk stk'),
+         (STK: Forall2 match_stackframe stk stk')
+         (BB: forall i bb',
+             f.(RTL.fn_code) ! pc = Some i ->
+             tf.(fn_code) ! pc' = Some bb' ->
+             list_drop (Pos.to_nat pc' - Pos.to_nat pc)%nat bb'.(bb_body) = i' :: bb
+         ),
     match_states (RTL.State stk f sp pc rs m)
                  (State stk' tf sp pc' bb rs ps m).
 
diff --git a/src/hls/RTLPar.v b/src/hls/RTLPar.v
index 61e968e..2c60116 100644
--- a/src/hls/RTLPar.v
+++ b/src/hls/RTLPar.v
@@ -46,8 +46,9 @@ Section RELSEM.
 
   Context (ge: genv).
 
-  Definition step_instr_block :=
-    step_list (step_list (step_list (step_instr ge))).
+  Definition step_instr_list := step_list (step_instr ge).
+  Definition step_instr_seq := step_list step_instr_list.
+  Definition step_instr_block := step_list step_instr_seq.
 
   Inductive step: state -> trace -> state -> Prop :=
   | exec_bblock:
diff --git a/src/hls/RTLPargenproof.v b/src/hls/RTLPargenproof.v
index fac6455..689c11a 100644
--- a/src/hls/RTLPargenproof.v
+++ b/src/hls/RTLPargenproof.v
@@ -796,24 +796,25 @@ Qed.*)Admitted.
 Definition match_prog (prog : RTLBlock.program) (tprog : RTLPar.program) :=
   match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq prog tprog.
 
+(* TODO: Fix the `bb` and add matches for them. *)
 Inductive match_stackframes: RTLBlock.stackframe -> RTLPar.stackframe -> Prop :=
 | match_stackframe:
-    forall f tf res sp pc rs rs' ps ps',
+    forall f tf res sp pc rs rs' ps ps' bb bb',
       transl_function f = OK tf ->
       (forall x, rs !! x = rs' !! x) ->
       (forall x, ps !! x = ps' !! x) ->
-      match_stackframes (Stackframe res f sp pc rs ps)
-                        (Stackframe res tf sp pc rs' ps').
+      match_stackframes (Stackframe res f sp pc bb rs ps)
+                        (Stackframe res tf sp pc bb' rs' ps').
 
 Inductive match_states: RTLBlock.state -> RTLPar.state -> Prop :=
 | match_state:
-    forall sf f sp pc rs rs' m sf' tf ps ps'
+    forall sf f sp pc rs rs' m sf' tf ps ps' bb bb'
       (TRANSL: transl_function f = OK tf)
       (STACKS: list_forall2 match_stackframes sf sf')
       (REG: forall x, rs !! x = rs' !! x)
       (REG: forall x, ps !! x = ps' !! x),
-      match_states (State sf f sp pc nil rs ps m)
-                   (State sf' tf sp pc nil rs' ps' m)
+      match_states (State sf f sp pc bb rs ps m)
+                   (State sf' tf sp pc bb' rs' ps' m)
 | match_returnstate:
     forall stack stack' v m
       (STACKS: list_forall2 match_stackframes stack stack'),
@@ -1041,14 +1042,16 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed.
       constructor; eauto.
   Qed.
 
+  (* TODO: Fix these proofs, now the cf_instr is in the State. *)
   Lemma step_cf_instr_correct:
-    forall cfi t s s',
-      step_cf_instr ge s cfi t s' ->
+    forall t s s',
+      step_cf_instr ge s t s' ->
       forall r,
         match_states s r ->
-        exists r', step_cf_instr tge r cfi t r' /\ match_states s' r'.
+        exists r', step_cf_instr tge r t r' /\ match_states s' r'.
   Proof using TRANSL.
-    induction 1; repeat semantics_simpl;
+
+    (*induction 1; repeat semantics_simpl;
     try solve [repeat (try erewrite match_states_list; eauto; econstructor; eauto with rtlgp)].
     { do 3 (try erewrite match_states_list by eauto; econstructor; eauto with rtlgp).
       eapply eval_builtin_args_eq. eapply REG.
@@ -1069,7 +1072,7 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed.
       repeat (try erewrite match_states_list; eauto; econstructor; eauto with rtlgp).
       erewrite eval_predf_pr_equiv; eauto.
     }
-  Qed.
+  Qed.*) Admitted.
 
   Theorem transl_step_correct :
     forall (S1 : RTLBlock.state) t S2,
@@ -1079,12 +1082,12 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed.
         exists R2, Smallstep.plus RTLPar.step tge R1 t R2 /\ match_states S2 R2.
   Proof.
 
-    induction 1; repeat semantics_simpl.
+    (*induction 1; repeat semantics_simpl.
 
     { destruct bb; destruct x.
       assert (bb_exit = bb_exit0).
       { unfold schedule_oracle in *. simplify.
-        unfold check_control_flow_instr in *.
+      n  unfold check_control_flow_instr in *.
         destruct_match; crush.
       }
       subst.
@@ -1106,7 +1109,7 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed.
     { inv TRANSL0. repeat econstructor; eauto using Events.external_call_symbols_preserved, symbols_preserved, senv_preserved, Events.E0_right. }
     { inv STACKS. inv H2. repeat econstructor; eauto.
       intros. apply PTree_matches; eauto. }
-  Qed.
+  Qed.*) Admitted.
 
   Lemma transl_initial_states:
     forall S,