simplified sim relation that does not track the entire physical state, just the call id stacks

_CoqProject

@@ -32,6 +32,7 @@ theories/sim/body.v
 theories/sim/refl_step.v
 theories/sim/left_step.v
 theories/sim/right_step.v
+theories/sim/simple.v
 
 theories/opt/ex1.v
 theories/opt/ex1_down.v

theories/opt/ex1.v

@@ -28,17 +28,15 @@ Definition ex1_opt : function :=
 
 Lemma ex1_sim_body fs ft : ⊨ᶠ{fs,ft} ex1 ≥ ex1_opt.
 Proof.
-  intros rf es et vls vlt σs σt FREL SUBSTs SUBSTt.
-  destruct vls as [|vs []]; [done| |done].  simpl in SUBSTs.
-  destruct vlt as [|vt []]; [done| |done].  simpl in SUBSTt. simplify_eq.
+  apply (sim_fun_simple1 10)=>// rf es css et cs vs vt FREL ??. simplify_eq/=.
 
   (* InitCall *)
-  exists 10%nat.
-  apply sim_body_init_call. simpl.
-
+  apply sim_simple_init_call=>c /= {css}.
+(*
   (* Alloc *)
   sim_apply sim_body_alloc_local. simpl.
 
   (* Let *)
   sim_apply sim_body_let_place. simpl.
+*)
 Abort.

theories/sim/local.v

@@ -115,6 +115,11 @@ Qed.
   - We start after the substitution.
   - We assume the arguments are values related by [r]
   - The returned result must also be values and related by [vrel]. *)
+Definition fun_post (esat: A → state → state → Prop) initial_call_id_stack
+  (r: A) (n: nat) rs σs rt σt :=
+  (∃ c, σt.(scs) = c :: initial_call_id_stack) ∧
+  esat r σs σt ∧
+  (∃ vs vt, rs = ValR vs ∧ rt = ValR vt ∧ vrel r vs vt).
 Definition sim_local_fun
   (esat: A → state → state → Prop) (fn_src fn_tgt : function) : Prop :=
   ∀ r es et (vl_src vl_tgt: list value) σs σt
@@ -123,16 +128,12 @@ Definition sim_local_fun
     (EQT: subst_l fn_tgt.(fun_b) (Val <$> vl_tgt) fn_tgt.(fun_e) = Some et),
     ∃ idx, sim_local_body r idx
                           (InitCall es) σs (InitCall et) σt
-                          (λ r' _ rs' σs' rt' σt',
-                            (∃ c, σt'.(scs) = c :: σt.(scs)) ∧
-                            esat r' σs' σt' ∧
-                            (∃ vs' vt', rs' = ValR vs' ∧ rt' = ValR vt' ∧
-                               vrel r' vs' vt')).
+                          (fun_post esat σt.(scs)).
 
 Definition sim_local_funs (esat: A → state → state → Prop) : Prop :=
   ∀ name fn_tgt, fnt !! name = Some fn_tgt → ∃ fn_src,
     fns !! name = Some fn_src ∧
-    length (fn_src.(fun_b)) = length (fn_tgt.(fun_b)) ∧
+    length fn_src.(fun_b) = length fn_tgt.(fun_b) ∧
     sim_local_fun esat fn_src fn_tgt.
 
 End local.

theories/sim/refl_step.v

@@ -906,7 +906,8 @@ Lemma sim_body_init_call fs ft r n es et σs σt Φ :
   let σs' := mkState σs.(shp) σs.(sst) (σs.(snc) :: σs.(scs)) σs.(snp) (S σs.(snc)) in
   let σt' := mkState σt.(shp) σt.(sst) (σt.(snc) :: σt.(scs)) σt.(snp) (S σt.(snc)) in
   let r'  : resUR := res_callState σt.(snc) (csOwned ∅) in
-  r ⋅ r' ⊨{n,fs,ft} (es, σs') ≥ (et, σt') : Φ →
+  (σs'.(scs) = σt'.(scs) →
+    r ⋅ r' ⊨{n,fs,ft} (es, σs') ≥ (et, σt') : Φ) →
   r ⊨{n,fs,ft} (InitCall es, σs) ≥ (InitCall et, σt) : Φ.
 Proof.
   intros σs' σt1 r' SIM. pfold.
@@ -925,8 +926,12 @@ Proof.
   { apply prod_local_update_1, prod_local_update_2.
     rewrite /= right_id (comm _ (_ ⋅ _)) -insert_singleton_op //.
     by apply alloc_singleton_local_update. }
+  have ANNOYING: scs σs' = scs σt1.
+  { simpl. destruct WSAT as (_ & _ & _ & _ & _ & SREL & _).
+    destruct SREL as (?&?&->&->&?). done. }
+  
   exists n. split; last split; cycle 2.
-  { (* sim cont *)  by punfold SIM. }
+  { (* sim cont *)  specialize (SIM ANNOYING). punfold SIM. }
   { (* STEP src *)  left. by apply tc_once. }
   (* WSAT new *)
   destruct WSAT as (WFS & WFT & VALID & PINV & CINV & SREL & LINV).

theories/sim/simple.v

-(** A simpler simulation relation that hides the physical state.
+(** A simpler simulation relation that hides most of the physical state,
+except for the call ID stack.
 Useful whenever the resources we own are strong enough to carry us from step to step.
 
 When your goal is simple, to make it stateful just do [intros σs σt].
-To go the other direction, [apply sim_simplify]. Then you will likely
+To go the other direction, [apply sim_simplify NEW_POST]. Then you will likely
 want to clean some stuff from your context.
 *)
 
-From stbor.sim Require Export instance.
+From stbor.sim Require Export instance refl_step.
 
-Definition sim_simple fs ft r n es et Φ : Prop :=
-  ∀ σs σt, r ⊨{ n , fs , ft } ( es , σs ) ≥ ( et , σt ) : Φ.
+Section simple.
+Implicit Types Φ: resUR → nat → result → call_id_stack → result → call_id_stack → Prop.
 
-Notation "r ⊨ˢ{ n , fs , ft } es '≥' et : Φ" :=
-  (sim_simple fs ft r n%nat es%E et%E Φ)
+Definition fun_post_simple initial_call_id_stack (r: resUR) (n: nat) vs css vt cst :=
+  (∃ c, cst = c::initial_call_id_stack) ∧
+  end_call_sat r (mkState ∅ ∅ css 0 0) (mkState ∅ ∅ cst 0 0) ∧
+  vrel_res r vs vt.
+
+Definition sim_simple fs ft r n es css et cst
+  (Φ : resUR → nat → result → call_id_stack → result → call_id_stack → Prop) : Prop :=
+  ∀ σs σt, σs.(scs) = css → σt.(scs) = cst →
+    r ⊨{ n , fs , ft } ( es , σs ) ≥ ( et , σt ) :
+    (λ r n vs' σs' vt' σt', Φ r n vs' σs'.(scs) vt' σt'.(scs)).
+
+Notation "r ⊨ˢ{ n , fs , ft } ( es , css ) '≥' ( et , cst ) : Φ" :=
+  (sim_simple fs ft r n%nat es%E css et%E cst Φ)
   (at level 70, es, et at next level,
-   format "'[hv' r  '/' ⊨ˢ{ n , fs , ft }  '/  ' '[ ' es ']'  '/' ≥  '/  ' '[ ' et ']'  '/' :  Φ ']'").
+   format "'[hv' r  '/' ⊨ˢ{ n , fs , ft }  '/  ' '[ ' ( es ,  css ) ']'  '/' ≥  '/  ' '[ ' ( et ,  cst ) ']'  '/' :  Φ ']'").
+
+(* FIXME: does this [apply]? *)
+Lemma sim_simplify
+  (Φnew: resUR → nat → result → call_id_stack → result → call_id_stack → Prop)
+  (Φ: resUR → nat → result → state → result → state → Prop)
+  r n fs ft es σs et σt :
+  (∀ r n vs σs vt σt, Φnew r n vs σs.(scs) vt σt.(scs) → Φ r n vs σs vt σt) →
+  r ⊨ˢ{ n , fs , ft } (es, σs.(scs)) ≥ (et, σt.(scs)) : Φnew →
+  r ⊨{ n , fs , ft } (es, σs) ≥ (et, σt) : Φ.
+Proof.
+  intros HΦ HH. eapply sim_local_body_post_mono; last by apply HH.
+  apply HΦ.
+Qed.
 
-Lemma sim_fun_simple1 n fs ft (esf etf: function) Φ :
+(** Simple proof for a function taking one argument. *)
+(* TODO: make the two call stacks the same. *)
+Lemma sim_fun_simple1 n fs ft (esf etf: function) :
   length (esf.(fun_b)) = 1%nat →
   length (etf.(fun_b)) = 1%nat →
-  (∀ es et vs vt r, vrel r vs vt →
-   subst_l (esf.(fun_b)) [Val vs] (esf.(fun_e)) = Some es →
-   subst_l (etf.(fun_b)) [Val vt] (etf.(fun_e)) = Some et →
-   r ⊨ˢ{n,fs,ft} es ≥ et : Φ) →
+  (∀ rf es css et cst vs vt,
+    vrel rf vs vt →
+    subst_l (esf.(fun_b)) [Val vs] (esf.(fun_e)) = Some es →
+    subst_l (etf.(fun_b)) [Val vt] (etf.(fun_e)) = Some et →
+    rf ⊨ˢ{n,fs,ft} (InitCall es, css) ≥ (InitCall et, cst) : fun_post_simple cst) →
   ⊨ᶠ{fs,ft} esf ≥ etf.
-Abort.
+Proof.
+  intros Hls Hlt HH rf es et vls vlt σs σt FREL SUBSTs SUBSTt. exists n.
+  move:(subst_l_is_Some_length _ _ _ _ SUBSTs) (subst_l_is_Some_length _ _ _ _ SUBSTt).
+  rewrite Hls Hlt.
+  destruct vls as [|vs []]; [done| |done].
+  destruct vlt as [|vt []]; [done| |done].
+  inversion FREL. intros _ _. simplify_eq.
+  eapply sim_simplify; last by eapply HH.
+  intros ?????? (Hhead & Hend & Hrel). split; first done.
+  split; last done.
+  (* Currently [end_call_sat] still looks at the state, but we should be able to fix that. *)
+  admit.
+Admitted.
+
+Lemma sim_simple_init_call fs ft r n es css et cst Φ :
+  (∀ c: call_id,
+    let r' := res_callState c (csOwned ∅) in
+    r ⋅ r' ⊨ˢ{n,fs,ft} (es, c::cst) ≥ (et, c::cst) : Φ) →
+  r ⊨ˢ{n,fs,ft} (InitCall es, css) ≥ (InitCall et, cst) : Φ.
+Proof.
+  intros HH σs σt <-<-. apply sim_body_init_call=>/= ?.
+  apply HH; done.
+Qed.
+
+Lemma sim_simple_alloc_local fs ft r n T css cst Φ :
+  (∀ (l: loc) (t: tag),
+    let r' := res_mapsto l ☠ (init_stack t) in
+    Φ (r ⋅ r') n (PlaceR l t T) css (PlaceR l t T) cst) →
+  r ⊨ˢ{n,fs,ft} (Alloc T, css) ≥ (Alloc T, cst) : Φ.
+Proof.
+  intros HH σs σt <-<-. apply sim_body_alloc_local=>/=. apply HH.
+Qed.
+
+End simple.