prove sexec_exact

1 files changed, 323 insertions, 11 deletions

diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v
index 0a2c0a04..5f7ecb1b 100644
--- a/scheduling/BTL_SEtheory.v
+++ b/scheduling/BTL_SEtheory.v
@@ -13,6 +13,22 @@ Require Import RTL BTL OptionMonad.
 Ltac inversion_SOME := fail.  (* deprecated tactic of OptionMonad: use autodestruct instead *)
 Ltac inversion_ASSERT := fail. (* deprecated tactic of OptionMonad: use autodestruct instead *)
 
+
+Ltac depmatch exp := 
+  match exp with
+  | context f [match ?expr with | _ => _ end] => ltac: (depmatch expr)
+  | _ => exp
+  end.
+
+Ltac autodestruct :=
+  let EQ := fresh "EQ" in 
+  match goal with
+  | |- context f [match ?expr with | _ => _ end] => 
+    let t := ltac: (depmatch expr) in
+    destruct t eqn:EQ; generalize EQ; clear EQ; congruence || trivial
+  end.
+
+
 Record iblock_exec_context := Bctx {
   cge: BTL.genv;
   cstk: list stackframe;
@@ -206,7 +222,7 @@ Proof.
     eapply seval_builtin_arg_correct; eauto.
 Qed.
 
-Lemma seval_builtin_arg_complete ctx rs m sreg: forall arg varg,
+Lemma seval_builtin_arg_exact ctx rs m sreg: forall arg varg,
   (forall r, eval_sval ctx (sreg r) = Some rs # r) ->
   seval_builtin_arg ctx m (builtin_arg_map sreg arg) varg ->
   eval_builtin_arg (cge ctx) (fun r => rs # r) (csp ctx) m arg varg.
@@ -220,7 +236,7 @@ Proof.
     eapply IHarg1; eauto. eapply IHarg2; eauto.
 Qed.
 
-Lemma seval_builtin_args_complete ctx rs m sreg: forall args vargs,
+Lemma seval_builtin_args_exact ctx rs m sreg: forall args vargs,
   (forall r, eval_sval ctx (sreg r) = Some rs # r) ->
   seval_builtin_args ctx m (map (builtin_arg_map sreg) args) vargs ->
   eval_builtin_args (cge ctx) (fun r => rs # r) (csp ctx) m args vargs.
@@ -229,7 +245,7 @@ Proof.
   - simpl. intros. inv H0. constructor.
   - intros vargs SEVAL BARG. simpl in BARG. inv BARG.
     constructor; [| eapply IHargs; eauto].
-    eapply seval_builtin_arg_complete; eauto.
+    eapply seval_builtin_arg_exact; eauto.
 Qed.
 
 Fixpoint seval_builtin_sval ctx bsv :=
@@ -539,10 +555,19 @@ Definition sem_sistate ctx (st: sistate) (rs: regset) (m: mem): Prop :=
   /\ eval_smem ctx st.(si_smem) = Some m
   /\ forall (r:reg), eval_sval ctx (st.(si_sreg) r) = Some (rs#r).
 
-Definition abort_sistate ctx (st: sistate): Prop :=
-  ~(st.(si_pre) ctx)
-  \/ eval_smem ctx st.(si_smem) = None
-  \/ exists (r: reg), eval_sval ctx (st.(si_sreg) r) = None.
+(* Remark that we need to reason modulo "extensionality" wrt Regmap.get about regsets.
+   And, nothing in their representation as (val * PTree.t val) enforces that
+     (forall r, rs1#r = rs2#r) -> rs1 = rs2
+*)
+Lemma sem_sistate_determ ctx st rs1 m1 rs2 m2:
+  sem_sistate ctx st rs1 m1 ->
+  sem_sistate ctx st rs2 m2 ->
+  (forall r, rs1#r = rs2#r) /\ m1 = m2.
+Proof.
+  intros (_&MEM1&REG1) (_&MEM2&REG2).
+  intuition try congruence.
+  generalize (REG1 r); rewrite REG2; congruence.
+Qed.
 
 (** * Symbolic execution of final step *)
 Definition sexec_final_sfv (i: final) (sis: sistate): sfval := 
@@ -590,9 +615,9 @@ Proof.
 Qed.
 
 Local Hint Constructors final_step: core.
-Local Hint Resolve seval_builtin_args_complete: core.
+Local Hint Resolve seval_builtin_args_exact: core.
 
-Lemma sexec_final_svf_complete ctx i sis t rs m s:
+Lemma sexec_final_svf_exact ctx i sis t rs m s:
   sem_sistate ctx sis rs m ->
   sem_sfval ctx (sexec_final_sfv i sis) rs m t s
   -> final_step (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs m i t s.
@@ -640,7 +665,7 @@ Lemma set_sreg_correct ctx dst sv sis (rs rs': regset) m:
   sem_sistate ctx (set_sreg dst sv sis) rs' m.
 Proof.
   intros (PRE&MEM&REG) NEW OLD.
-  unfold sem_sistate, set_sreg; simpl.
+  unfold sem_sistate; simpl.
   intuition.
   - rewrite REG in *; congruence.
   - destruct (Pos.eq_dec dst r); simpl; subst; eauto.
@@ -658,7 +683,7 @@ Lemma set_smem_correct ctx sm sis rs m m':
   sem_sistate ctx (set_smem sm sis) rs m'.
 Proof.
   intros (PRE&MEM&REG) NEW.
-  unfold sem_sistate, set_smem; simpl.
+  unfold sem_sistate; simpl.
   intuition.
   rewrite MEM in *; congruence.
 Qed.
@@ -813,3 +838,290 @@ Proof.
   destruct 1 as (rs' & m' & fin & ISTEP & FSTEP).
   eapply sexec_rec_correct; simpl; eauto.
 Qed.
+
+
+(* TODO: déplacer les trucs sur equiv_stackframe -> regmap_setres_eq dans BTL! *)
+Inductive equiv_stackframe: stackframe -> stackframe -> Prop :=
+  | equiv_stackframe_intro res f sp pc rs1 rs2
+      (EQUIV: forall r : positive, rs1 !! r = rs2 !! r):
+      equiv_stackframe (Stackframe res f sp pc rs1) (Stackframe res f sp pc rs2)
+  .
+
+Inductive equiv_state: state -> state -> Prop :=
+  | State_equiv stack f sp pc rs1 m rs2
+     (EQUIV: forall r, rs1#r = rs2#r): 
+     equiv_state (State stack f sp pc rs1 m) (State stack f sp pc rs2 m)
+  | Call_equiv stk stk' f args m
+      (STACKS: list_forall2 equiv_stackframe stk stk'):
+      equiv_state (Callstate stk f args m) (Callstate stk' f args m)
+  | Return_equiv stk stk' v m
+      (STACKS: list_forall2 equiv_stackframe stk stk'):
+      equiv_state (Returnstate stk v m) (Returnstate stk' v m)
+  .
+
+Local Hint Constructors equiv_stackframe equiv_state: core.
+
+Lemma equiv_stackframe_refl stf: equiv_stackframe stf stf.
+Proof.
+  destruct stf; eauto.
+Qed.
+
+Lemma equiv_stack_refl stk: list_forall2 equiv_stackframe stk stk.
+Proof.
+  Local Hint Resolve equiv_stackframe_refl: core.
+  induction stk; simpl; constructor; auto.
+Qed.
+
+Lemma equiv_state_refl s: equiv_state s s.
+Proof.
+  Local Hint Resolve equiv_stack_refl: core.
+  induction s; simpl; constructor; auto.
+Qed.
+
+Lemma equiv_stackframe_trans stf1 stf2 stf3:
+  equiv_stackframe stf1 stf2 -> equiv_stackframe stf2 stf3 -> equiv_stackframe stf1 stf3.
+Proof.
+  destruct 1; intros EQ; inv EQ; try econstructor; eauto.
+  intros; eapply eq_trans; eauto.
+Qed.
+
+Lemma equiv_stack_trans stk1 stk2:
+  list_forall2 equiv_stackframe stk1 stk2 -> 
+  forall stk3, list_forall2 equiv_stackframe stk2 stk3 -> 
+  list_forall2 equiv_stackframe stk1 stk3.
+Proof.
+  Local Hint Resolve equiv_stackframe_trans: core.
+  induction 1; intros stk3 EQ; inv EQ; econstructor; eauto.
+Qed.
+
+Lemma equiv_state_trans s1 s2 s3: equiv_state s1 s2 -> equiv_state s2 s3 -> equiv_state s1 s3.
+Proof.
+  Local Hint Resolve equiv_stack_trans: core.
+  destruct 1; intros EQ; inv EQ; econstructor; eauto.
+  intros; eapply eq_trans; eauto.
+Qed.
+
+Lemma regmap_setres_eq (rs rs': regset) res vres:
+  (forall r, rs # r = rs' # r) ->
+  forall r, (regmap_setres res vres rs) # r = (regmap_setres res vres rs') # r.
+Proof.
+  intros RSEQ r. destruct res; simpl; try congruence.
+  destruct (peq x r).
+  - subst. repeat (rewrite Regmap.gss). reflexivity.
+  - repeat (rewrite Regmap.gso); auto.
+Qed.
+
+Lemma sem_sfval_equiv rs1 rs2 ctx sfv m t s:
+  sem_sfval ctx sfv rs1 m t s ->
+  (forall r, rs1#r = rs2#r) -> 
+  exists s', equiv_state s s' /\  sem_sfval ctx sfv rs2 m t s'.
+Proof. 
+  Local Hint Resolve equiv_stack_refl equiv_state_refl regmap_setres_eq: core.
+  Local Hint Constructors sem_sfval: core.
+  destruct 1; eexists; split; econstructor; eauto.
+  econstructor; eauto.
+Qed.
+
+Local Hint Resolve sexec_final_svf_exact: core.
+
+Definition abort_sistate ctx (sis: sistate): Prop :=
+  ~(sis.(si_pre) ctx)
+  \/ eval_smem ctx sis.(si_smem) = None
+  \/ exists (r: reg), eval_sval ctx (sis.(si_sreg) r) = None.
+
+Lemma sem_sistate_exclude_abort ctx sis rs m:
+  sem_sistate ctx sis rs m ->
+  abort_sistate ctx sis ->
+  False.
+Proof.
+  intros SIS ABORT. inv SIS. destruct H0 as (H0 & H0').
+  inversion ABORT as [ABORT1 | [ABORT2 | ABORT3]]; [ | | inv ABORT3]; congruence.
+Qed.
+
+Local Hint Resolve sem_sistate_exclude_abort: core.
+
+Lemma set_sreg_preserves_abort ctx sv dst sis:
+  abort_sistate ctx sis ->
+  abort_sistate ctx (set_sreg dst sv sis).
+Proof.
+  unfold abort_sistate; simpl; intros [PRE|[MEM|REG]]; try tauto.
+  destruct REG as [r REG].
+  destruct (Pos.eq_dec dst r) as [TEST|TEST] eqn: HTEST.
+  - subst; rewrite REG; tauto.
+  - right. right. eexists; rewrite HTEST. auto.
+Qed.
+
+Lemma sexec_op_preserves_abort ctx op args dest sis:
+  abort_sistate ctx sis
+  -> abort_sistate ctx (sexec_op op args dest sis).
+Proof.
+  intros; eapply set_sreg_preserves_abort; eauto.
+Qed.
+
+Lemma sexec_load_preserves_abort ctx chunk addr args dest sis:
+  abort_sistate ctx sis
+  -> abort_sistate ctx (sexec_load TRAP chunk addr args dest sis).
+Proof.
+  intros; eapply set_sreg_preserves_abort; eauto.
+Qed.
+
+Lemma set_smem_preserves_abort ctx sm sis:
+  abort_sistate ctx sis ->
+  abort_sistate ctx (set_smem sm sis).
+Proof.
+  unfold abort_sistate; simpl; try tauto.
+Qed.
+
+Lemma sexec_store_preserves_abort ctx chunk addr args src sis:
+  abort_sistate ctx sis
+  -> abort_sistate ctx (sexec_store chunk addr args src sis).
+Proof.
+  intros; eapply set_smem_preserves_abort; eauto.
+Qed.
+
+Local Hint Resolve sexec_op_preserves_abort sexec_load_preserves_abort
+  sexec_store_preserves_abort: core.
+
+Lemma sexec_exclude_abort ctx ib t s1: forall sis k
+  (SEXEC: sem_sstate ctx t s1 (sexec_rec ib sis k))
+  (CONT: forall sis', sem_sstate ctx t s1 (k sis') -> (abort_sistate ctx sis') -> False)
+  (ABORT: abort_sistate ctx sis),
+  False.
+Proof.
+  induction ib; simpl; intros; eauto.
+  - (* final *) inversion SEXEC; subst; eauto.
+  - (* load *) destruct trap; eauto.
+    inversion SEXEC.
+  - (* seq *)
+    eapply IHib1; eauto.
+    simpl. eauto.
+  - (* cond *)
+    inversion SEXEC; subst; eauto. clear SEXEC.
+    destruct b; eauto.
+Qed.
+
+Lemma set_sreg_abort ctx dst sv sis rs m:
+  sem_sistate ctx sis rs m -> 
+  (eval_sval ctx sv = None) ->
+  abort_sistate ctx (set_sreg dst sv sis).
+Proof.
+  intros (PRE&MEM&REG) NEW.
+  unfold sem_sistate, abort_sistate; simpl.
+  right; right.
+  exists dst; destruct (Pos.eq_dec dst dst); simpl; try congruence.
+Qed.
+
+Lemma sexec_op_abort ctx sis op args dest rs m
+  (EVAL: eval_operation (cge ctx) (csp ctx) op rs ## args m = None)
+  (SIS: sem_sistate ctx sis rs m)
+  : abort_sistate ctx (sexec_op op args dest sis).
+Proof.
+  eapply set_sreg_abort; eauto.
+  simpl. destruct SIS as (PRE&MEM&REG).
+  erewrite eval_list_sval_inj; simpl; auto.
+  try_simplify_someHyps.
+Qed.
+
+Lemma sexec_load_TRAP_abort ctx chunk addr args dst sis rs m
+ (EVAL: forall a, eval_addressing (cge ctx) (csp ctx) addr rs ## args = Some a -> Mem.loadv chunk m a = None)
+ (SIS: sem_sistate ctx sis rs m)
+ : abort_sistate ctx (sexec_load TRAP chunk addr args dst sis).
+Proof.
+  eapply set_sreg_abort; eauto.
+  simpl. destruct SIS as (PRE&MEM&REG).
+  erewrite eval_list_sval_inj; simpl; auto.
+  intros; autodestruct; try_simplify_someHyps.
+Qed.
+
+Lemma set_smem_abort ctx sm sis rs m:
+  sem_sistate ctx sis rs m ->
+  eval_smem ctx sm = None ->
+  abort_sistate ctx (set_smem sm sis).
+Proof.
+  intros (PRE&MEM&REG) NEW.
+  unfold abort_sistate; simpl.
+  tauto.
+Qed.
+
+Lemma sexec_store_abort ctx chunk addr args src sis rs m
+ (EVAL: forall a, eval_addressing (cge ctx) (csp ctx) addr rs ## args = Some a -> Mem.storev chunk m a (rs # src) = None)
+ (SIS: sem_sistate ctx sis rs m)
+ :abort_sistate ctx (sexec_store chunk addr args src sis).
+Proof.
+  eapply set_smem_abort; eauto.
+  simpl. destruct SIS as (PRE&MEM&REG).
+  erewrite eval_list_sval_inj; simpl; auto.
+  try_simplify_someHyps.
+  intros; rewrite REG; autodestruct; try_simplify_someHyps.
+Qed.
+
+Local Hint Resolve sexec_op_abort sexec_load_TRAP_abort sexec_store_abort: core.
+
+Lemma sexec_rec_exact ctx ib t s1: forall sis k
+  (SEXEC: sem_sstate ctx t s1 (sexec_rec ib sis k))
+  rs m
+  (SIS: sem_sistate ctx sis rs m)
+  (CONT: forall sis', sem_sstate ctx t s1 (k sis') -> (abort_sistate ctx sis') -> False)
+  ,
+     match iblock_istep_run (cge ctx) (csp ctx) ib rs m with
+     | Some (out rs' m' (Some fin)) =>
+        exists s2, final_step (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs' m' fin t s2 /\ equiv_state s1 s2
+     | Some (out rs' m' None) => exists sis', (sem_sstate ctx t s1 (k sis')) /\ (sem_sistate ctx sis' rs' m')
+     | None => False
+     end.
+Proof.
+  induction ib; simpl; intros; eauto.
+  - (* final *)
+    inv SEXEC.
+    exploit (sem_sistate_determ ctx sis rs m rs0 m0); eauto.
+    intros (REG&MEM); subst.
+    exploit (sem_sfval_equiv rs0 rs); eauto.
+    intros (s2 & EQUIV & SFV').
+    eexists; split; eauto.
+  - (* Bop *) autodestruct; eauto.
+  - destruct trap; [| inv SEXEC ].
+    repeat autodestruct; eauto.
+    all: intros; eapply CONT; eauto;
+        eapply sexec_load_TRAP_abort; eauto;
+        intros; try_simplify_someHyps.
+  - repeat autodestruct; eauto.
+    all: intros; eapply CONT; eauto;
+        eapply sexec_store_abort; eauto;
+        intros; try_simplify_someHyps.
+  - (* Bseq *)
+    exploit IHib1; eauto. clear sis SEXEC SIS.
+    { simpl; intros; eapply sexec_exclude_abort; eauto. }
+    destruct (iblock_istep_run _ _ _ _ _) eqn: ISTEP; auto.
+    destruct o.
+    destruct _fin eqn: OFIN; simpl; eauto.
+    intros (sis1 & SEXEC1 & SIS1).
+    exploit IHib2; eauto.
+  - (* Bcond *)
+    inv SEXEC.
+    erewrite seval_condition_eq in SEVAL; eauto.
+    rewrite SEVAL.
+    destruct b.
+    + exploit IHib1; eauto.
+    + exploit IHib2; eauto.
+Qed.
+
+
+(* NB: each execution of a symbolic state (produced from [sexec]) represents a concrete execution
+  (sexec is exact).
+*)
+Theorem sexec_exact ctx ib t s1: 
+  sem_sstate ctx t s1 (sexec ib) ->
+  exists s2, iblock_step (cge ctx) (cstk ctx) (cf ctx) (csp ctx) (crs0 ctx) (cm0 ctx) ib t s2
+             /\ equiv_state s1 s2.
+Proof.
+  intros; exploit sexec_rec_exact; eauto.
+  { intros sis' SEXEC; inversion SEXEC. }
+  repeat autodestruct; simpl; try tauto.
+  - intros D1 D2 ISTEP (s2 & FSTEP & EQSTEP); subst.
+    eexists; split; eauto.
+    repeat eexists; eauto.
+    erewrite iblock_istep_run_equiv; eauto.
+  - intros D1 D2 ISTEP (sis & SEXEC & _); subst.
+    inversion SEXEC.
+Qed.
+