remove useless (and unprovable) lemmas on completeness of the refinement

2 files changed, 67 insertions, 48 deletions

diff --git a/configure b/configure
index 0db4b3a5..959d0590 100755
--- a/configure
+++ b/configure
@@ -845,7 +845,7 @@ EXECUTE=kvx-cluster --syscall=libstd_scalls.so --
 CFLAGS= -D __KVX_COS__
 SIMU=kvx-cluster -- 
 BACKENDLIB=Machblock.v Machblockgen.v Machblockgenproof.v\\
-    RTLpath.v RTLpathproof.v RTLpathLivegen.v RTLpathLivegenproof.v RTLpathSE_theory.v RTLpathScheduler.v RTLpathSchedulerproof.v\\
+    RTLpath.v RTLpathproof.v RTLpathLivegen.v RTLpathLivegenproof.v RTLpathSE_theory.v RTLpathSE_impl.v RTLpathScheduler.v RTLpathSchedulerproof.v\\
     Asmblock.v Asmblockgen.v Asmblockgenproof0.v Asmblockgenproof1.v Asmblockgenproof.v Asmvliw.v Asmblockprops.v\\
     ForwardSimulationBlock.v PostpassScheduling.v PostpassSchedulingproof.v\\
     Asmblockdeps.v DecBoolOps.v Chunks.v Peephole.v ExtValues.v ExtFloats.v\\
diff --git a/kvx/lib/RTLpathSE_impl.v b/kvx/lib/RTLpathSE_impl.v
index 1c62825a..e4ae1af8 100644
--- a/kvx/lib/RTLpathSE_impl.v
+++ b/kvx/lib/RTLpathSE_impl.v
@@ -78,32 +78,32 @@ Definition hsok_local ge sp (hst: hsistate_local) rs0 m0: Prop :=
   /\ forall sm, List.In sm (hsi_lsmem hst) -> seval_smem ge sp sm rs0 m0 <> None.
 
 (* refinement link between a (st: sistate_local) and (hst: hsistate_local) *)
-Definition hsistate_local_refines (hst: hsistate_local) (st: sistate_local)  := forall ge sp,
-     (forall rs0 m0, sok_local ge sp st rs0 m0 <-> hsok_local ge sp hst rs0 m0)
-  /\ (forall rs0 m0, hsok_local ge sp hst rs0 m0 -> hsi_smem_eval ge sp hst rs0 m0 = seval_smem ge sp st.(si_smem) rs0 m0)
-  /\ (forall rs0 m0 r, hsok_local ge sp hst rs0 m0 -> hsi_sreg_eval ge sp hst r rs0 m0 = seval_sval ge sp (si_sreg st r) rs0 m0).
+Definition hsistate_local_refines ge sp rs0 m0 (hst: hsistate_local) (st: sistate_local) :=
+     (sok_local ge sp st rs0 m0 <-> hsok_local ge sp hst rs0 m0)
+  /\ (hsok_local ge sp hst rs0 m0 -> hsi_smem_eval ge sp hst rs0 m0 = seval_smem ge sp st.(si_smem) rs0 m0)
+  /\ (hsok_local ge sp hst rs0 m0 -> forall r, hsi_sreg_eval ge sp hst r rs0 m0 = seval_sval ge sp (si_sreg st r) rs0 m0).
 
 (* Syntax and semantics of symbolic exit states *)
 (* TODO: add hash-consing *)
 Record hsistate_exit := mk_hsistate_exit
   { hsi_cond: condition; hsi_scondargs: list_sval; hsi_elocal: hsistate_local; hsi_ifso: node }.
 
-Definition hsistate_exit_refines (hext: hsistate_exit) (ext: sistate_exit): Prop :=
+Definition hsistate_exit_refines ge sp rs0 m0 (hext: hsistate_exit) (ext: sistate_exit): Prop :=
   hsi_cond hext = si_cond ext
   /\ hsi_scondargs hext = si_scondargs ext
-  /\ hsistate_local_refines (hsi_elocal hext) (si_elocal ext)
+  /\ hsistate_local_refines ge sp rs0 m0 (hsi_elocal hext) (si_elocal ext)
   /\ hsi_ifso hext = si_ifso ext.
 
 (** * Syntax and Semantics of symbolic internal state *)
 Record hsistate := { hsi_pc: node; hsi_exits: list hsistate_exit; hsi_local: hsistate_local }.
 
-Definition hsistate_refines (hst: hsistate) (st:sistate): Prop :=
+Definition hsistate_refines ge sp rs0 m0 (hst: hsistate) (st:sistate): Prop :=
   hsi_pc hst = si_pc st
-  /\ list_forall2 hsistate_exit_refines (hsi_exits hst) (si_exits st)
-  /\ hsistate_local_refines (hsi_local hst) (si_local st).
+  /\ list_forall2 (hsistate_exit_refines ge sp rs0 m0) (hsi_exits hst) (si_exits st)
+  /\ hsistate_local_refines ge sp rs0 m0 (hsi_local hst) (si_local st).
 
-Lemma hsistate_refines_pceq st hst:
-  hsistate_refines hst st ->
+Lemma hsistate_refines_pceq ge sp rs0 m0 st hst:
+  hsistate_refines ge sp rs0 m0 hst st ->
   (hsi_pc hst) = (si_pc st).
 Proof.
 Admitted.
@@ -175,13 +175,16 @@ Definition hsiexec_inst (i: instruction) (hst: hsistate): option hsistate :=
   | _ => None (* TODO jumptable ? *)
   end.
 
-Lemma hsiexec_inst_none i st hst:
+(* SB: est-ce utile ?
+Lemma hsiexec_inst_none ge sp rs0 m0 i st hst:
   siexec_inst i st = None ->
-  hsistate_refines hst st ->
+  hsistate_refines ge sp rs0 m0 hst st ->
   hsiexec_inst i hst = None.
 Proof.
 Admitted.
+*)
 
+(* SB: inutile en principe 
 Lemma hsiexec_inst_complete i st st' hst:
   siexec_inst i st = Some st' ->
   hsistate_refines hst st ->
@@ -190,13 +193,14 @@ Lemma hsiexec_inst_complete i st st' hst:
   /\ hsistate_refines hst' st'.
 Proof.
 Admitted.
+*)
 
-Lemma hsiexec_inst_correct i hst hst' st:
+Lemma hsiexec_inst_correct ge sp rs0 m0 i hst hst' st:
   hsiexec_inst i hst = Some hst' ->
-  hsistate_refines hst st ->
+  hsistate_refines ge sp rs0 m0 hst st ->
   exists st',
      siexec_inst i st = Some st'
-  /\ hsistate_refines hst' st'.
+  /\ hsistate_refines ge sp rs0 m0 hst' st'.
 Proof.
 Admitted.
 
@@ -209,6 +213,7 @@ Fixpoint hsiexec_path (path:nat) (f: function) (hst: hsistate): option hsistate
     hsiexec_path p f hst1
   end.
 
+(* On ne devrait pas avoir besoin de ça !
 Lemma hsiexec_path_complete ps f st st' hst:
   siexec_path ps f st = Some st' ->
   hsistate_refines hst st ->
@@ -217,20 +222,21 @@ Lemma hsiexec_path_complete ps f st st' hst:
   /\ hsistate_refines hst' st'.
 Proof.
 Admitted.
+*)
 
 Lemma hsiexec_path_correct ps f hst hst' st:
   hsiexec_path ps f hst = Some hst' ->
-  hsistate_refines hst st ->
+  forall ge sp rs0 m0, hsistate_refines ge sp rs0 m0 hst st ->
   exists st',
      siexec_path ps f st = Some st'
-  /\ hsistate_refines hst' st'.
+  /\ hsistate_refines ge sp rs0 m0 hst' st'.
 Proof.
 Admitted.
 
 Record hsstate := { hinternal:> hsistate; hfinal: sfval }.
 
-Definition hsstate_refines (hst: hsstate) (st:sstate): Prop :=
-  hsistate_refines (hinternal hst) (internal st)
+Definition hsstate_refines ge sp rs0 m0 (hst: hsstate) (st:sstate): Prop :=
+  hsistate_refines ge sp rs0 m0 (hinternal hst) (internal st)
   /\ hfinal hst = final st. (* TODO *)
 
 Definition hsexec_final (i: instruction) (prev: hsistate_local): sfval := 
@@ -255,8 +261,8 @@ Definition hsexec_final (i: instruction) (prev: hsistate_local): sfval :=
   | _ => Snone
   end.
 
-Lemma hsexec_final_correct hsl sl i:
-  hsistate_local_refines hsl sl ->
+Lemma hsexec_final_correct ge sp rs0 m0 hsl sl i:
+  hsistate_local_refines ge sp rs0 m0 hsl sl ->
   hsexec_final i hsl = sexec_final i sl.
 Proof.
 Admitted.
@@ -265,8 +271,8 @@ Definition init_hsistate_local := {| hsi_lsmem := Sinit::nil; hsi_ok_lsval := ni
 
 Definition init_hsistate pc := {| hsi_pc := pc; hsi_exits := nil; hsi_local := init_hsistate_local |}.
 
-Remark init_hsistate_correct pc:
-  hsistate_refines (init_hsistate pc) (init_sistate pc).
+Remark init_hsistate_correct ge sp rs0 m0 pc:
+  hsistate_refines ge sp rs0 m0 (init_hsistate pc) (init_sistate pc).
 Proof.
 Admitted.
 
@@ -279,18 +285,21 @@ Definition hsexec (f: function) (pc:node): option hsstate :=
        | None => {| hinternal := hst; hfinal := hsexec_final i hst.(hsi_local) |}
        end).
 
-(* FIXME - this lemma might be unprovable ? *)
+(* FIXME - this lemma might be unprovable ?  SB: inutile en principe
 Lemma hsistate_refines_determ hst st st':
   hsistate_refines hst st ->
   hsistate_refines hst st' ->
   st = st'.
 Proof.
 Admitted.
+*)
 
-Lemma hsexec_correct f pc st hst:
+Lemma hsexec_correct f pc hst:
   hsexec f pc = Some hst ->
-  hsstate_refines hst st ->
-  sexec f pc = Some st.
+  exists st, sexec f pc = Some st /\
+  forall ge sp rs0 m0, hsstate_refines ge sp rs0 m0 hst st.
+Admitted.
+(*
 Proof.
   unfold hsexec. intros H HREF. explore.
   unfold sexec. rewrite EQ.
@@ -304,7 +313,10 @@ Proof.
     eapply hsistate_refines_determ in HIREF; eauto. congruence.
   - admit.
 Admitted.
+*)
+
 
+(* NB: inutile en principe.
 Lemma hsexec_complete f pc st:
   sexec f pc = Some st ->
   exists hst, hsexec f pc = Some hst /\ hsstate_refines hst st.
@@ -322,13 +334,12 @@ Proof.
       constructor; auto. simpl.
       destruct HREF as (_ & _ & HLREF). apply hsexec_final_correct. assumption.
 Qed.
+*)
 
 Definition hsstate_simu dm f (hst1 hst2: hsstate): Prop :=
-  forall st1,
-  hsstate_refines hst1 st1 ->
-  exists st2,
-     hsstate_refines hst2 st2
-  /\ sstate_simu dm f st1 st2.
+  forall ge sp rs0 m0 st1 st2,
+  hsstate_refines ge sp rs0 m0 hst1 st1 ->
+  hsstate_refines ge sp rs0 m0 hst2 st2 -> sstate_simu dm f st1 st2.
 
 Definition hsstate_simub (dm: PTree.t node) (f: RTLpath.function) (hst1 hst2: hsstate) := OK tt. (* TODO *)
 
@@ -338,21 +349,23 @@ Lemma hsstate_simub_correct dm f hst1 hst2:
 Proof.
 Admitted.
 
+(* SB: Hum, le "exists st2" ne me plaît pas du tout ici...
 Definition hsexec_simu dm (f1 f2: RTLpath.function) pc1 pc2: Prop :=
     forall hst1, hsexec f1 pc1 = Some hst1 -> 
     exists hst2, hsexec f2 pc2 = Some hst2 /\ hsstate_simu dm f1 hst1 hst2.
 
-Lemma hsexec_sexec_simu dm f1 f2 pc1 pc2:
-  hsexec_simu dm f1 f2 pc1 pc2 -> sexec_simu dm f1 f2 pc1 pc2.
+
+Lemma hsexec_sexec_simu dm f1 f2 pc1 pc2 hst1 hst2:
+  hsexec f1 pc1 = Some hst1 ->
+  hsexec f2 pc2 = Some hst2 ->
+  hsstate_simu dm f1 hst1 hst2 -> sexec_simu dm f1 f2 pc1 pc2.
 Proof.
-  intro HESIMU.
-  intros st1 SEXEC.
-  eapply hsexec_complete in SEXEC.
-  destruct SEXEC as (hst & HSEXEC & HREF).
+  intros HSEXEC1 HSEXEC2 HESIMU.
   eapply HESIMU in HSEXEC. destruct HSEXEC as (hst' & HSEXEC' & HSSIMU).
   eapply HSSIMU in HREF. destruct HREF as (st' & HREF' & SSIMU).
   eapply hsexec_correct in HSEXEC'; eauto.
 Qed.
+*)
 
 Definition simu_check_single (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpath.function) (m: node * node) :=
   let (pc2, pc1) := m in
@@ -369,14 +382,20 @@ Lemma simu_check_single_correct dm tf f pc1 pc2:
   simu_check_single dm f tf (pc2, pc1) = OK tt ->
   sexec_simu dm f tf pc1 pc2.
 Proof.
-  unfold simu_check_single. intro. explore.
-  assert (hsexec_simu dm f tf pc1 pc2). {
-    unfold hsexec_simu. intros st1 STEQ. assert (h = st1) by congruence. subst.
-    exists h0. constructor; auto.
-    apply hsstate_simub_correct. assumption.
-  }
-  apply hsexec_sexec_simu. assumption.
-Qed.
+  unfold simu_check_single. intro.
+  unfold sexec_simu.
+  intros st1 SEXEC.
+  explore.
+  exploit hsexec_correct; eauto.
+  intros (st2 & SEXEC2 & REF2).
+  clear EQ0. (* now, useless in principle and harmful for the next [exploit] *)
+  exploit hsexec_correct; eauto.
+  intros (st0 & SEXEC1 & REF1).
+  rewrite SEXEC1 in SEXEC; inversion SEXEC; subst.
+  eexists; split; eauto.
+  eapply hsstate_simub_correct; eauto.
+  (* SB: issue: remaining goals are on the shelf... *)
+Admitted.
 
 Fixpoint simu_check_rec (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpath.function) lm :=
   match lm with