proving the remaining lemma for sexec_rec_okpreserv

1 files changed, 162 insertions, 123 deletions

diff --git a/scheduling/BTL_SEsimuref.v b/scheduling/BTL_SEsimuref.v
index 852bced0..da680e63 100644
--- a/scheduling/BTL_SEsimuref.v
+++ b/scheduling/BTL_SEsimuref.v
@@ -31,7 +31,9 @@ Record ristate :=
     ris_smem: smem;
     (** For the values in registers:
         1) we store a list of sval evaluations
-        2) we encode the symbolic regset by a PTree + a boolean indicating the default sval *)
+        2) we encode the symbolic regset by a PTree + a boolean indicating the default sval
+        See [ris_sreg_get] below.
+     *)
     ris_input_init: bool;
     ok_rsval: list sval;
     ris_sreg:> PTree.t sval
@@ -51,18 +53,32 @@ Record ris_ok ctx (ris: ristate) : Prop := {
 Local Hint Resolve OK_RMEM OK_RREG: core.
 Local Hint Constructors ris_ok: core.
 
-(* TODO: Is it useful ?
-Definition ris_abs (ris: ristate) : sistate := {|
-  si_pre := fun ctx => ris_ok ctx ris;
-  si_sreg := ris_sreg_get ris;
-  si_smem := ris.(ris_smem)
-|}.
-*)
+(**
+   NOTE that this refinement relation *cannot* be decomposed into a abstraction function of type 
+   ristate -> sistate & an equivalence relation on istate.
+
+   Indeed, any [sis] satisfies [forall ctx r, si_ok ctx sis -> eval_sval ctx (sis r) <> None].
+   whereas this is generally not true for [ris] that [forall ctx r, ris_ok ctx ris -> eval_sval ctx (ris r) <> None], 
+   except when, precisely, [ris_refines ris sis].
+
+   An alternative design enabling to define ris_refines as the composition of an equivalence on sistate 
+   and a abstraction function would consist in constraining sistate with an additional [wf] field:
 
+   Record sistate := 
+    { si_pre: iblock_exec_context -> Prop; 
+      si_sreg:> reg -> sval;
+      si_smem: smem;
+      si_wf: forall ctx, si_pre ctx -> si_smem <> None /\ forall r, si_sreg r <> None 
+   }.
+
+  Such a constraint should also appear in [ristate]. This is not clear whether this alternative design 
+  would be really simpler.
+
+*)
 Record ris_refines ctx (ris: ristate) (sis: sistate): Prop := {
   OK_EQUIV: si_ok ctx sis <-> ris_ok ctx ris;
   MEM_EQ: ris_ok ctx ris ->  eval_smem ctx ris.(ris_smem) = eval_smem ctx sis.(si_smem);
-  REG_EQ: ris_ok ctx ris -> forall r, eval_sval ctx (ris_sreg_get ris r) = eval_sval ctx (si_sreg sis r)
+  REG_EQ: ris_ok ctx ris -> forall r, eval_sval ctx (ris r) = eval_sval ctx (sis r)
 }.
 Local Hint Resolve OK_EQUIV MEM_EQ REG_EQ: core.
 Local Hint Constructors ris_refines: core.
@@ -70,7 +86,7 @@ Local Hint Constructors ris_refines: core.
 Record ris_simu ris1 ris2: Prop := {
   SIMU_FAILS: forall sv, List.In sv ris2.(ok_rsval) -> List.In sv ris1.(ok_rsval);
   SIMU_MEM: ris1.(ris_smem) = ris2.(ris_smem);
-  SIMU_REG: forall r, ris_sreg_get ris1 r = ris_sreg_get ris2 r
+  SIMU_REG: forall r, ris1 r = ris2 r
 }.
 Local Hint Resolve SIMU_FAILS SIMU_MEM SIMU_REG: core.
 Local Hint Constructors ris_simu: core.
@@ -186,7 +202,6 @@ Inductive rstate :=
   | Rabort
   .
 
-
 Record routcome := rout {
   _ris: ristate;
   _rfv: sfval;
@@ -257,7 +272,7 @@ Proof.
   destruct b; simpl; auto.
 Qed.
 
-Lemma rst_refines_outcome_down ctx rst st:
+Lemma rst_refines_outcome_okpreserv ctx rst st:
    rst_refines ctx rst st ->
    forall sis sfv,
    get_soutcome ctx st = Some (sout sis sfv) ->
@@ -280,7 +295,7 @@ Proof.
   intros sis1 sfv1 SOUT OK1.
   exploit REF1; eauto.
   clear REF1; intros REF1.
-  exploit rst_refines_outcome_down; eauto. clear REF1 SOUT.
+  exploit rst_refines_outcome_okpreserv; eauto. clear REF1 SOUT.
   intros (ris1 & rfv1 & ROUT1 & REFI1 & REFF1).
   rewrite OK_EQUIV in OK1; eauto. 
   exploit REFF1; eauto. clear REFF1; intros REFF1.
@@ -294,7 +309,114 @@ Proof.
   do 2 eexists; split; eauto.
 Qed.
 
-(** * Refinement of the symbolic execution *)
+
+(** * Properties of the (abstract) operators involved in symbolic execution *)
+
+Lemma ok_set_mem ctx sm sis:
+  si_ok ctx (set_smem sm sis)
+  <-> (si_ok ctx sis /\ eval_smem ctx sm <> None).
+Proof.
+  split; destruct 1; econstructor; simpl in *; eauto.
+  intuition eauto.
+Qed.
+
+Lemma ok_set_sreg ctx r sv sis:
+  si_ok ctx (set_sreg r sv sis)
+  <-> (si_ok ctx sis /\ eval_sval ctx sv <> None).
+Proof.
+  unfold set_sreg; split.
+  + intros [(SVAL & PRE) SMEM SREG]; simpl in *; split.
+    - econstructor; eauto.
+      intros r0; generalize (SREG r0); destruct (Pos.eq_dec r r0); try congruence.
+    - generalize (SREG r); destruct (Pos.eq_dec r r); try congruence.
+  + intros ([PRE SMEM SREG] & SVAL).
+    econstructor; simpl; eauto.
+    intros r0;  destruct (Pos.eq_dec r r0); try congruence.
+Qed.
+
+Lemma si_ok_op_okpreserv ctx op args dest sis: si_ok ctx (sexec_op op args dest sis) -> si_ok ctx sis.
+Proof.
+  unfold sexec_op. rewrite ok_set_sreg. intuition.
+Qed.
+
+Lemma si_ok_load_okpreserv ctx chunk addr args dest sis: si_ok ctx (sexec_load TRAP chunk addr args dest sis) -> si_ok ctx sis.
+Proof.
+  unfold sexec_load. rewrite ok_set_sreg. intuition.
+Qed.
+
+Lemma si_ok_store_okpreserv ctx chunk addr args src sis: si_ok ctx (sexec_store chunk addr args src sis) -> si_ok ctx sis.
+Proof.
+  unfold sexec_store. rewrite ok_set_mem. intuition.
+Qed.
+
+Lemma si_ok_tr_okpreserv ctx fi sis: si_ok ctx (tr_sis (cf ctx) fi sis) -> si_ok ctx sis.
+Proof.
+  unfold tr_sis. intros OK; inv OK. simpl in *. intuition.
+Qed.
+
+(* These lemmas are very bad for eauto: we put them into a dedicated basis. *)
+Local Hint Resolve si_ok_tr_okpreserv si_ok_op_okpreserv si_ok_load_okpreserv si_ok_store_okpreserv: sis_ok.
+
+Lemma sexec_rec_okpreserv ctx ib: 
+  forall k
+  (CONT: forall sis lsis sfv, get_soutcome ctx (k sis) = Some (sout lsis sfv) ->  si_ok ctx lsis -> si_ok ctx sis)
+  sis lsis sfv
+  (SOUT: get_soutcome ctx (sexec_rec (cf ctx) ib sis k) = Some (sout lsis sfv))
+  (OK: si_ok ctx lsis)
+  ,si_ok ctx sis.
+Proof.
+  induction ib; simpl; try (autodestruct; simpl).
+  1-6: try_simplify_someHyps; eauto with sis_ok.
+  - intros. eapply IHib1. 2-3: eauto.
+    eapply IHib2; eauto.
+  - intros k CONT sis lsis sfv.
+    do 2 autodestruct; eauto.
+Qed.
+
+(* an alternative tr_sis *)
+
+Definition transfer_sis (inputs: list reg) (sis:sistate): sistate :=
+   {| si_pre := fun ctx => (sis.(si_pre) ctx /\ forall r, eval_sval ctx (sis.(si_sreg) r) <> None);
+      si_sreg := transfer_sreg inputs sis;
+      si_smem := sis.(si_smem) |}.
+
+Lemma ok_transfer_sis ctx inputs sis:
+  si_ok ctx (transfer_sis inputs sis)
+  <-> (si_ok ctx sis).
+Proof.
+  unfold transfer_sis. induction inputs as [|r l]; simpl.
+  + split; destruct 1; econstructor; simpl in *; intuition eauto. congruence.
+  + split.
+    * destruct 1; econstructor; simpl in *; intuition eauto.
+    * intros X; generalize X. rewrite <- IHl in X; clear IHl.
+      intros [PRE SMEM SREG].
+      econstructor; simpl; eauto.
+      intros r0;  destruct (Pos.eq_dec r r0); try congruence.
+      intros H; eapply OK_SREG; eauto.
+Qed.
+
+Definition alt_tr_sis := poly_tr (fun f tbl or => transfer_sis (Regset.elements (pre_inputs f tbl or))).
+
+Lemma tr_sis_alt_def f fi sis:
+  alt_tr_sis f fi sis = tr_sis f fi sis.
+Proof.
+  unfold tr_sis, str_inputs. destruct fi; simpl; auto.
+Qed.
+
+
+(** * Refinement of the symbolic execution (e.g. refinement of [sexec] into [rexec]).
+
+TODO: Est-ce qu'on garde cette vision purement fonctionnelle de l'implementation ?
+=> ça pourrait être pratique quand on va compliquer encore le vérificateur !
+
+Du coup, on introduirait une version avec hash-consing qui serait en correspondance 
+pour une relation d'equivalence sur les ristate ?
+
+Attention toutefois, il est possible que certaines parties de l'execution soient pénibles à formuler 
+en programmation fonctionnelle pure (exemple: usage de l'égalité de pointeur comme test d'égalité rapide!)
+
+
+*)
 
 Local Hint Constructors rfv_refines optrsv_refines rsvident_refines rsvident_refines: core.
 
@@ -361,14 +483,6 @@ Definition rset_smem rm (ris:ristate): ristate :=
      ris_sreg:= ris.(ris_sreg)
   |}.
 
-Lemma ok_set_mem ctx sm sis:
-  si_ok ctx (set_smem sm sis)
-  <-> (si_ok ctx sis /\ eval_smem ctx sm <> None).
-Proof.
-  split; destruct 1; econstructor; simpl in *; eauto.
-  intuition eauto.
-Qed.
-
 Lemma ok_rset_mem ctx rm (ris: ristate):
   (eval_smem ctx ris.(ris_smem) = None -> eval_smem ctx rm = None) ->
   ris_ok ctx (rset_smem rm ris)
@@ -414,20 +528,6 @@ Definition rset_sreg r rsv (ris:ristate): ristate :=
      ris_sreg:= PTree.set r rsv ris.(ris_sreg) (* TODO: A CHANGER *)
   |}.
 
-Lemma ok_set_sreg ctx r sv sis:
-  si_ok ctx (set_sreg r sv sis)
-  <-> (si_ok ctx sis /\ eval_sval ctx sv <> None).
-Proof.
-  unfold set_sreg; split.
-  + intros [(SVAL & PRE) SMEM SREG]; simpl in *; split.
-    - econstructor; eauto.
-      intros r0; generalize (SREG r0); destruct (Pos.eq_dec r r0); try congruence.
-    - generalize (SREG r); destruct (Pos.eq_dec r r); try congruence.
-  + intros ([PRE SMEM SREG] & SVAL).
-    econstructor; simpl; eauto.
-    intros r0;  destruct (Pos.eq_dec r r0); try congruence.
-Qed.
-
 Lemma ok_rset_sreg ctx r rsv ris:
   ris_ok ctx (rset_sreg r rsv ris)
   <-> (ris_ok ctx ris /\ eval_sval ctx rsv <> None).
@@ -528,26 +628,6 @@ Fixpoint transfer_ris (inputs: list reg) (ris:ristate): ristate :=
   | r::l => rseto_sreg r (ris_sreg_get ris r) (transfer_ris l ris)
   end.
 
-Definition transfer_sis (inputs: list reg) (sis:sistate): sistate :=
-   {| si_pre := fun ctx => (sis.(si_pre) ctx /\ forall r, eval_sval ctx (sis.(si_sreg) r) <> None);
-      si_sreg := transfer_sreg inputs sis;
-      si_smem := sis.(si_smem) |}.
-
-Lemma ok_transfer_sis ctx inputs sis:
-  si_ok ctx (transfer_sis inputs sis)
-  <-> (si_ok ctx sis).
-Proof.
-  unfold transfer_sis. induction inputs as [|r l]; simpl.
-  + split; destruct 1; econstructor; simpl in *; intuition eauto. congruence.
-  + split.
-    * destruct 1; econstructor; simpl in *; intuition eauto.
-    * intros X; generalize X. rewrite <- IHl in X; clear IHl.
-      intros [PRE SMEM SREG].
-      econstructor; simpl; eauto.
-      intros r0;  destruct (Pos.eq_dec r r0); try congruence.
-      intros H; eapply OK_SREG; eauto.
-Qed.
-
 Lemma ok_transfer_ris ctx inputs ris:
   ris_ok ctx (transfer_ris inputs ris)
   <-> (ris_ok ctx ris).
@@ -583,14 +663,6 @@ Proof.
       - rewrite ok_rseto_sreg, ok_transfer_ris. auto.
 Qed.
 
-Definition alt_tr_sis := poly_tr (fun f tbl or => transfer_sis (Regset.elements (pre_inputs f tbl or))).
-
-Lemma tr_sis_alt_def f fi sis:
-  alt_tr_sis f fi sis = tr_sis f fi sis.
-Proof.
-  unfold tr_sis, str_inputs. destruct fi; simpl; auto.
-Qed.
-
 Definition tr_ris := poly_tr (fun f tbl or => transfer_ris (Regset.elements (pre_inputs f tbl or))).
 
 Local Hint Resolve transfer_ris_correct ok_transfer_ris: core.
@@ -603,14 +675,11 @@ Proof.
    destruct fi; simpl; eauto.
 Qed.
 
-Lemma ok_tr_ris_imp ctx fi ris:
-  ris_ok ctx (tr_ris (cf ctx) fi ris)
-  -> (ris_ok ctx ris).
+Lemma ris_ok_tr_okpreserv ctx fi ris: ris_ok ctx (tr_ris (cf ctx) fi ris) -> ris_ok ctx ris.
 Proof.
   rewrite ok_tr_ris; auto.
 Qed.
 
-
 Lemma tr_ris_correct ctx fi ris sis:
   ris_refines ctx ris sis ->
   ris_refines ctx (tr_ris (cf ctx) fi ris) (tr_sis (cf ctx) fi sis).
@@ -619,40 +688,6 @@ Proof.
   destruct fi; simpl; eauto.
 Qed.
 
-Lemma si_ok_tr_down ctx fi sis: si_ok ctx (tr_sis (cf ctx) fi sis) -> si_ok ctx sis.
-Admitted.
-
-Lemma si_ok_op_down ctx op args dest sis: si_ok ctx (sexec_op op args dest sis) -> si_ok ctx sis.
-Admitted.
-
-Lemma si_ok_trap_down ctx chunk addr args dest sis: si_ok ctx (sexec_load TRAP chunk addr args dest sis) -> si_ok ctx sis.
-Admitted.
-
-Lemma si_ok_store_down ctx chunk addr args src sis: si_ok ctx (sexec_store chunk addr args src sis) -> si_ok ctx sis.
-Admitted.
-
-(* TODO: a revoir: ce n'est pas une bonne idee de mettre ça dans core => ça fait ramer "eauto" !!! *)
-Local Hint Resolve si_ok_tr_down si_ok_op_down si_ok_trap_down si_ok_store_down: core.
-
-Lemma sexec_rec_down ctx ib: 
-  forall k
-  (CONT: forall sis lsis sfv, get_soutcome ctx (k sis) = Some (sout lsis sfv) ->  si_ok ctx lsis -> si_ok ctx sis)
-  sis lsis sfv
-  (SOUT: get_soutcome ctx (sexec_rec (cf ctx) ib sis k) = Some (sout lsis sfv))
-  (OK: si_ok ctx lsis)
-  ,si_ok ctx sis.
-Proof.
-  induction ib; simpl; try (autodestruct; simpl).
-  1-6: try_simplify_someHyps.
-  - intros. eapply IHib1. 2-3: eauto.
-    eapply IHib2; eauto.
-  - intros k CONT sis lsis sfv.
-    do 2 autodestruct.
-    + intros; eapply IHib1; eauto.
-    + intros; eapply IHib2; eauto.
-Qed.
-
-
 (** RAFFINEMENT EXEC SYMBOLIQUE **)
 
 Fixpoint rexec_rec f ib ris (k: ristate -> rstate): rstate := 
@@ -678,7 +713,7 @@ Fixpoint rexec_rec f ib ris (k: ristate -> rstate): rstate :=
 Definition rexec f ib := rexec_rec f ib ris_init (fun _ => Rabort).
 
 
-Local Hint Resolve ris_init_correct exec_final_refpreserv tr_ris_correct ok_tr_ris_imp 
+Local Hint Resolve ris_init_correct exec_final_refpreserv tr_ris_correct ris_ok_tr_okpreserv
   rexec_op_correct rexec_load_correct rexec_store_correct: core.
 
 Local Hint Constructors rst_refines: core.
@@ -699,13 +734,13 @@ Proof.
   - (* seq *)
     intros; subst.
     eapply IHib1. 3-6: eauto.
-    + simpl. eapply sexec_rec_down; eauto.
+    + simpl. eapply sexec_rec_okpreserv; eauto.
     + intros; subst. eapply IHib2; eauto.
   - (* cond *)
     intros rk k CONTh CONT ris sis lsis sfv st REF EXEC OUT OK. subst.
     assert (rOK: ris_ok ctx ris). {
       erewrite <- OK_EQUIV. 2: eauto.
-      eapply sexec_rec_down with (ib:=(Bcond cond args ib1 ib2 iinfo)); simpl; eauto.
+      eapply sexec_rec_okpreserv with (ib:=(Bcond cond args ib1 ib2 iinfo)); simpl; eauto.
     }
     generalize OUT; clear OUT; simpl.
     autodestruct.
@@ -725,22 +760,28 @@ Qed.
 
 (** COPIER-COLLER ... Y a-t-il moyen de l'eviter ? **)
 
-Lemma ris_ok_tr_down ctx fi ris: ris_ok ctx (tr_ris (cf ctx) fi ris) -> ris_ok ctx ris.
-Admitted.
-
-Lemma ris_ok_op_down ctx op args dest ris: ris_ok ctx (rexec_op op args dest ris) -> ris_ok ctx ris.
-Admitted.
+Lemma ris_ok_op_okpreserv ctx op args dest ris: ris_ok ctx (rexec_op op args dest ris) -> ris_ok ctx ris.
+Proof.
+  unfold rexec_op. rewrite ok_rset_sreg. intuition.
+Qed.
 
-Lemma ris_ok_trap_down ctx chunk addr args dest ris: ris_ok ctx (rexec_load TRAP chunk addr args dest ris) -> ris_ok ctx ris.
-Admitted.
+Lemma ris_ok_load_okpreserv ctx chunk addr args dest ris: ris_ok ctx (rexec_load TRAP chunk addr args dest ris) -> ris_ok ctx ris.
+Proof.
+  unfold rexec_load. rewrite ok_rset_sreg. intuition.
+Qed.
 
-Lemma ris_ok_store_down ctx chunk addr args src ris: ris_ok ctx (rexec_store chunk addr args src ris) -> ris_ok ctx ris.
-Admitted.
+Lemma ris_ok_store_okpreserv ctx chunk addr args src ris: ris_ok ctx (rexec_store chunk addr args src ris) -> ris_ok ctx ris.
+Proof.
+  unfold rexec_store. rewrite ok_rset_mem; simpl. 
+  + intuition.
+  + intros X; rewrite X; simpl.
+    repeat autodestruct.
+Qed.
 
-(* TODO: a revoir: ce n'est pas une bonne idee de mettre ça dans core => ça fait ramer "eauto" !!! *)
-Local Hint Resolve ris_ok_tr_down ris_ok_op_down ris_ok_trap_down ris_ok_store_down: core.
+(* These lemmas are very bad for eauto: we put them into a dedicated basis. *)
+Local Hint Resolve ris_ok_store_okpreserv ris_ok_op_okpreserv ris_ok_load_okpreserv: ris_ok.
 
-Lemma rexec_rec_down ctx ib: 
+Lemma rexec_rec_okpreserv ctx ib: 
   forall k
   (CONT: forall ris lris rfv, get_routcome ctx (k ris) = Some (rout lris rfv) ->  ris_ok ctx lris -> ris_ok ctx ris)
   ris lris rfv
@@ -749,13 +790,11 @@ Lemma rexec_rec_down ctx ib:
   ,ris_ok ctx ris.
 Proof.
   induction ib; simpl; try (autodestruct; simpl).
-  1-6: try_simplify_someHyps.
+  1-6: try_simplify_someHyps; eauto with ris_ok.
   - intros. eapply IHib1. 2-3: eauto.
     eapply IHib2; eauto.
   - intros k CONT sis lsis sfv.
-    do 2 autodestruct.
-    + intros; eapply IHib1; eauto.
-    + intros; eapply IHib2; eauto.
+    do 2 autodestruct; eauto.
 Qed.
 
 Lemma rexec_rec_correct2 ctx ib: 
@@ -774,12 +813,12 @@ Proof.
   - (* seq *)
     intros; subst.
     eapply IHib1. 3-6: eauto.
-    + simpl. eapply rexec_rec_down; eauto.
+    + simpl. eapply rexec_rec_okpreserv; eauto.
     + intros; subst. eapply IHib2; eauto.
   - (* cond *)
     intros rk k CONTh CONT ris sis lsis sfv st REF EXEC OUT OK. subst.
     assert (OK0: ris_ok ctx ris). {
-      eapply rexec_rec_down with (ib:=(Bcond cond args ib1 ib2 iinfo)); simpl; eauto.
+      eapply rexec_rec_okpreserv with (ib:=(Bcond cond args ib1 ib2 iinfo)); simpl; eauto.
     }
     generalize OUT; clear OUT; simpl.
     autodestruct.