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 ++++++++++++++++++
 1 file changed, 18 insertions(+)

(limited to 'src/hls/RTLPargen.v')

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
 ===================
-- 
cgit