From b3e2078df318a2d5e54de0b09963f37d63327f0a Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Thu, 12 May 2022 20:47:14 +0100
Subject: Famous proven but not tested has been fixed

---
 src/hls/RTLPargenproof.v | 22 +++++++++++-----------
 1 file changed, 11 insertions(+), 11 deletions(-)

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

diff --git a/src/hls/RTLPargenproof.v b/src/hls/RTLPargenproof.v
index 689c11a..f975601 100644
--- a/src/hls/RTLPargenproof.v
+++ b/src/hls/RTLPargenproof.v
@@ -590,7 +590,7 @@ Proof.
     econstructor; auto.
     match goal with H: eval_pred _ _ _ _ |- _ => inv H end.
     repeat econstructor; try erewrite match_states_list; eauto.
-  - destruct p. match goal with H: eval_pred _ _ _ _ |- _ => inv H end.
+  (*- destruct p. match goal with H: eval_pred _ _ _ _ |- _ => inv H end.
     repeat econstructor; try erewrite match_states_list; eauto.
     erewrite <- eval_predf_pr_equiv; eassumption.
     apply PTree_matches; assumption.
@@ -615,7 +615,7 @@ Proof.
     match goal with
     H: forall _, _ |- context[Mem.storev] => erewrite <- H; eauto
     end.
-  - admit. Admitted.
+  - admit.*) Admitted.
 
 Lemma step_instr_list_matches :
   forall a ge sp st st',
@@ -799,22 +799,22 @@ Definition match_prog (prog : RTLBlock.program) (tprog : RTLPar.program) :=
 (* 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' bb bb',
+    forall f tf res sp pc rs rs' ps ps',
       transl_function f = OK tf ->
       (forall x, rs !! x = rs' !! x) ->
       (forall x, ps !! x = ps' !! x) ->
-      match_stackframes (Stackframe res f sp pc bb rs ps)
-                        (Stackframe res tf sp pc bb' rs' ps').
+      match_stackframes (Stackframe res f sp pc rs ps)
+                        (Stackframe res tf sp pc rs' ps').
 
 Inductive match_states: RTLBlock.state -> RTLPar.state -> Prop :=
 | match_state:
-    forall sf f sp pc rs rs' m sf' tf ps ps' bb bb'
+    forall sf f sp pc rs rs' m sf' tf ps ps'
       (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 bb rs ps m)
-                   (State sf' tf sp pc bb' rs' ps' m)
+      match_states (State sf f sp pc rs ps m)
+                   (State sf' tf sp pc rs' ps' m)
 | match_returnstate:
     forall stack stack' v m
       (STACKS: list_forall2 match_stackframes stack stack'),
@@ -1044,11 +1044,11 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed.
 
   (* TODO: Fix these proofs, now the cf_instr is in the State. *)
   Lemma step_cf_instr_correct:
-    forall t s s',
-      step_cf_instr ge s t s' ->
+    forall t s s' cf,
+      step_cf_instr ge s cf t s' ->
       forall r,
         match_states s r ->
-        exists r', step_cf_instr tge r t r' /\ match_states s' r'.
+        exists r', step_cf_instr tge r cf t r' /\ match_states s' r'.
   Proof using TRANSL.
 
     (*induction 1; repeat semantics_simpl;
-- 
cgit