Rename backwards proof

3 files changed, 55 insertions, 30 deletions

diff --git a/src/hls/GiblePargenproof.v b/src/hls/GiblePargenproof.v
index 9e58e03..010bc0a 100644
--- a/src/hls/GiblePargenproof.v
+++ b/src/hls/GiblePargenproof.v
@@ -35,6 +35,7 @@ Require Import vericert.hls.Predicate.
 Require Import vericert.hls.Abstr.
 Require Import vericert.common.Monad.
 Require Import vericert.hls.GiblePargenproofForward.
+Require Import vericert.hls.GiblePargenproofBackward.
 
 Module Import OptionExtra := MonadExtra(Option).
 
@@ -169,9 +170,10 @@ Section CORRECTNESS.
   Lemma schedule_oracle_nil2:
       schedule_oracle nil nil = true.
   Proof using .
-    unfold schedule_oracle, check_control_flow_instr.
+    unfold schedule_oracle, check_control_flow_instr, check.
     simplify; repeat destruct_match; crush.
-  Admitted.
+    now rewrite ! check_mutexcl_singleton.
+  Qed.
 
   Lemma eval_op_eq:
     forall (sp0 : Values.val) (op : Op.operation) (vl : list Values.val) m,
@@ -206,35 +208,7 @@ RTLBlock to abstract translation
 
 Correctness of translation from RTLBlock to the abstract interpretation
 language.
-|*)
-
-  Lemma abstr_seq_reverse_correct :
-    forall sp x i i' ti cf x',
-      abstract_sequence x = Some x' ->
-      sem (mk_ctx i sp ge) x' (i', (Some cf)) ->
-      state_lessdef i ti ->
-     exists ti', SeqBB.step ge sp (Iexec ti) x (Iterm ti' cf)
-             /\ state_lessdef i' ti'.
-  Proof.
-
-(*|
-Proof Sketch:
-
-We do an induction over the list of instructions ``x``.  This is trivial for the
-empty case and then for the inductive case we know that there exists an
-execution that matches the abstract execution, so we need to know that adding
-another instructions to it will still mean that the execution will result in the
-same value.
-
-Arithmetic operations will be a problem because we will have to show that these
-can be executed.  However, this should mostly be a problem in the abstract state
-comparison, because there two abstract states can be equal without one being
-evaluable.
-|*)
 
-  Admitted.
-
-(*|
 This is the top-level lemma which uses the following proofs to complete the
 square:
 
diff --git a/src/hls/GiblePargenproofBackwards.v b/src/hls/GiblePargenproofBackward.v
index 50b733a..e2bb23c 100644
--- a/src/hls/GiblePargenproofBackwards.v
+++ b/src/hls/GiblePargenproofBackward.v
@@ -47,3 +47,50 @@ Module Import OptionExtra := MonadExtra(Option).
 #[local] Ltac destr := destruct_match; try discriminate; [].
 
 Definition state_lessdef := GiblePargenproofEquiv.match_states.
+
+(*|
+===================================
+GiblePar to Abstr Translation Proof
+===================================
+
+This proof is for the correctness of the translation from the parallel Gible
+program into the Abstr language, which is the symbolic execution language.  The
+main characteristic of this proof is that it has to be performed backwards, as
+the translation goes from GiblePar to Abstr, whereas the correctness proof is
+needed from Abstr to GiblePar to get the proper direction of the proof.
+|*)
+
+Section CORRECTNESS.
+
+Context (prog: GibleSeq.program) (tprog : GiblePar.program).
+
+Let ge : GibleSeq.genv := Globalenvs.Genv.globalenv prog.
+Let tge : GiblePar.genv := Globalenvs.Genv.globalenv tprog.
+
+Lemma abstr_seq_reverse_correct :
+  forall sp x i i' ti cf x',
+    abstract_sequence x = Some x' ->
+    sem (mk_ctx i sp ge) x' (i', (Some cf)) ->
+    state_lessdef i ti ->
+   exists ti', SeqBB.step ge sp (Iexec ti) x (Iterm ti' cf)
+           /\ state_lessdef i' ti'.
+Proof.
+
+(*|
+Proof Sketch:
+
+We do an induction over the list of instructions ``x``.  This is trivial for the
+empty case and then for the inductive case we know that there exists an
+execution that matches the abstract execution, so we need to know that adding
+another instructions to it will still mean that the execution will result in the
+same value.
+
+Arithmetic operations will be a problem because we will have to show that these
+can be executed.  However, this should mostly be a problem in the abstract state
+comparison, because there two abstract states can be equal without one being
+evaluable.
+|*)
+
+Admitted.
+
+End CORRECTNESS.
diff --git a/src/hls/GiblePargenproofEquiv.v b/src/hls/GiblePargenproofEquiv.v
index 5f28d53..da2b2c1 100644
--- a/src/hls/GiblePargenproofEquiv.v
+++ b/src/hls/GiblePargenproofEquiv.v
@@ -1396,6 +1396,10 @@ Lemma check_mutexcl_correct:
     predicated_mutexcl pe.
 Proof. Admitted.
 
+Lemma check_mutexcl_singleton :
+  check_mutexcl (NE.singleton (T, EEbase)) = true.
+Proof. Admitted.
+
 Definition check_mutexcl_tree {A} (f: PTree.t (predicated A)) :=
   forall_ptree (fun _ => check_mutexcl) f.