From becbab413e16e40069329d8e7f21dc92e2e4c4e4 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Sun, 16 May 2021 11:26:22 +0100
Subject: Finish up step_cf_instr_correct again

---
 src/hls/RTLPargen.v      | 18 ++++++++++++++++++
 src/hls/RTLPargenproof.v | 44 +++++++++++++++++++++++++-------------------
 2 files changed, 43 insertions(+), 19 deletions(-)

diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v
index d2a7174..a8da344 100644
--- a/src/hls/RTLPargen.v
+++ b/src/hls/RTLPargen.v
@@ -467,6 +467,13 @@ Inductive match_states : instr_state -> instr_state -> Prop :=
     m = m' ->
     match_states (InstrState rs m) (InstrState rs' m').
 
+Inductive match_states_ld : instr_state -> instr_state -> Prop :=
+| match_states_ld_intro:
+  forall rs rs' m m',
+    regs_lessdef rs rs' ->
+    Mem.extends m m' ->
+    match_states_ld (InstrState rs m) (InstrState rs' m').
+
 Lemma sems_det:
   forall A ge tge sp st f,
   ge_preserved ge tge ->
@@ -1318,6 +1325,17 @@ Proof.
   econstructor; congruence.
 Qed.
 
+(*Lemma abstract_execution_correct_ld:
+  forall bb bb' cfi ge tge sp st st' tst,
+    RTLBlock.step_instr_list ge sp st bb st' ->
+    ge_preserved ge tge ->
+    schedule_oracle (mk_bblock bb cfi) (mk_bblock bb' cfi) = true ->
+    match_states_ld st tst ->
+    exists tst', RTLPar.step_instr_block tge sp tst bb' tst'
+                 /\ match_states st' tst'.
+Proof.
+  intros.*)
+
 (*|
 Top-level functions
 ===================
diff --git a/src/hls/RTLPargenproof.v b/src/hls/RTLPargenproof.v
index e8167e9..8ecaba2 100644
--- a/src/hls/RTLPargenproof.v
+++ b/src/hls/RTLPargenproof.v
@@ -44,26 +44,23 @@ Inductive match_stackframes: RTLBlock.stackframe -> RTLPar.stackframe -> Prop :=
 
 Inductive match_states: RTLBlock.state -> RTLPar.state -> Prop :=
 | match_state:
-    forall sf f sp pc rs rs' m m' sf' tf
+    forall sf f sp pc rs rs' m sf' tf
       (TRANSL: transl_function f = OK tf)
       (STACKS: list_forall2 match_stackframes sf sf')
-      (REG: forall x, rs !! x = rs' !! x)
-      (MEM: Mem.extends m m'),
+      (REG: forall x, rs !! x = rs' !! x),
       match_states (State sf f sp pc rs m)
-                   (State sf' tf sp pc rs' m')
+                   (State sf' tf sp pc rs' m)
 | match_returnstate:
-    forall stack stack' v m m'
-      (STACKS: list_forall2 match_stackframes stack stack')
-      (MEM: Mem.extends m m'),
+    forall stack stack' v m
+      (STACKS: list_forall2 match_stackframes stack stack'),
       match_states (Returnstate stack v m)
-                   (Returnstate stack' v m')
+                   (Returnstate stack' v m)
 | match_callstate:
-    forall stack stack' f tf args m m'
+    forall stack stack' f tf args m
       (TRANSL: transl_fundef f = OK tf)
-      (STACKS: list_forall2 match_stackframes stack stack')
-      (MEM: Mem.extends m m'),
+      (STACKS: list_forall2 match_stackframes stack stack'),
       match_states (Callstate stack f args m)
-                   (Callstate stack' tf args m').
+                   (Callstate stack' tf args m).
 
 Section CORRECTNESS.
 
@@ -266,7 +263,7 @@ Section CORRECTNESS.
       Events.eval_builtin_arg ge e2 sp m1 a v1.
 Proof. induction 2; try rewrite H; eauto with barg. Qed.
 
-  Lemma eval_builtin_args_lessdef:
+  Lemma eval_builtin_args_eq:
     forall A ge e1 sp m1 e2 al vl1,
       (forall x, e1 x = e2 x) ->
       @Events.eval_builtin_args A ge e1 sp m1 al vl1 ->
@@ -293,14 +290,23 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed.
     { (try erewrite match_states_list by eauto; econstructor; eauto with rtlgp).
     (try erewrite match_states_list by eauto; econstructor; eauto with rtlgp).
     (try erewrite match_states_list by eauto; econstructor; eauto with rtlgp).
-    exploit Events.eval_builtin_args_lessdef.
+    eapply eval_builtin_args_eq. eapply REG.
+    eapply Events.eval_builtin_args_preserved. eapply symbols_preserved.
+    eauto.
+    (econstructor; eauto with rtlgp).
+    intros.
+    unfold regmap_setres. destruct res.
+    destruct (Pos.eq_dec x0 x); subst.
+    repeat rewrite Regmap.gss; auto.
+    repeat rewrite Regmap.gso; auto.
+    eapply REG. eapply REG.
     }
-    repeat (econstructor; eauto with rtlgp).
-    erewrite match_states_list; eauto.
-    repeat (econstructor; eauto with rtlgp).
+    { repeat (try erewrite match_states_list; eauto; econstructor; eauto with rtlgp). }
+    { repeat (try erewrite match_states_list; eauto; econstructor; eauto with rtlgp). }
+    { repeat (try erewrite match_states_list; eauto; econstructor; eauto with rtlgp).
+      unfold regmap_optget. destruct or. rewrite REG. constructor; eauto.
+      constructor; eauto.
     }
-    repeat (econstructor; eauto with rtlgp).
-    exploit find_function_translated. eauto.
   Qed.
 
   Theorem transl_step_correct :
-- 
cgit