more bind, more core, more refl

theories/sim/body.v

@@ -109,7 +109,7 @@ Proof.
   { left. rewrite to_of_result. by eexists. }
 Qed.
 
-Lemma sim_body_res_proper fs ft n es σs et σt Φ r1 r2:
+Lemma sim_body_res_ext fs ft n es σs et σt Φ r1 r2:
   r1 ≡ r2 →
   r1 ⊨{n,fs,ft} (es, σs) ≥ (et, σt) : Φ →
   r2 ⊨{n,fs,ft} (es, σs) ≥ (et, σt) : Φ.
@@ -135,11 +135,21 @@ Proof.
     right. eapply CIH; eauto.
 Qed.
 
+(* TODO: also allow rewriting the postcondition. *)
+Global Instance sim_body_res_proper fs ft :
+  Proper ((≡) ==> (=) ==> (=) ==> (=) ==> (=) ==> (=) ==> (=) ==> (↔))
+    (sim_local_body wsat vrel fs ft).
+Proof.
+  intros r1 r2 EQr n ? <- es ? <- σs ? <- et ? <- σt ? <- Φ ? <-.
+  split; eapply sim_body_res_ext; done.
+Qed.
+Global Instance: Params (@sim_local_body) 5.
+
 Lemma sim_body_frame' fs ft n (rf r: resUR) es σs et σt Φ :
   r ⊨{n,fs,ft} (es, σs) ≥ (et, σt) : Φ : Prop →
   ∀ (r': resUR), r' ≡ rf ⋅ r →
     r' ⊨{n,fs,ft} (es, σs) ≥ (et, σt) :
-    (λ r' n' es' σs' et' σt', ∃ r0, r' ≡ rf ⋅ r0 ∧ Φ r0 n' es' σs' et' σt').
+    (λ r' n' es' σs' et' σt', ∃ r0, r' = rf ⋅ r0 ∧ Φ r0 n' es' σs' et' σt').
 Proof.
   revert n rf r es σs et σt Φ. pcofix CIH.
   intros n rf r0 es σs et σt Φ SIM r' EQ'.
@@ -167,9 +177,20 @@ Qed.
 Lemma sim_body_frame fs ft n (rf r: resUR) es σs et σt Φ :
   r ⊨{n,fs,ft} (es, σs) ≥ (et, σt) : Φ : Prop →
   rf ⋅ r ⊨{n,fs,ft} (es, σs) ≥ (et, σt) :
-    (λ r' n' es' σs' et' σt', ∃ r0, r' ≡ rf ⋅ r0 ∧ Φ r0 n' es' σs' et' σt').
+    (λ r' n' es' σs' et' σt', ∃ r0, r' = rf ⋅ r0 ∧ Φ r0 n' es' σs' et' σt').
 Proof. intros. eapply sim_body_frame'; eauto. Qed.
 
+Lemma sim_body_frame_core fs ft n (r: resUR) es σs et σt Φ :
+  r ⊨{n,fs,ft}
+    (es, σs) ≥ (et, σt)
+  : (λ r' n' es' σs' et' σt', Φ (core r ⋅ r') n' es' σs' et' σt') →
+  r ⊨{n,fs,ft} (es, σs) ≥ (et, σt) : Φ.
+Proof.
+  intros HH. rewrite -(cmra_core_l r).
+  eapply sim_local_body_post_mono, sim_body_frame, HH.
+  intros r' n' rs' σs' rt' σt' [r'' [-> HΦ]]. done.
+Qed.
+
 Lemma sim_body_val_elim fs ft r n vs σs vt σt Φ :
   r ⊨{n,fs,ft} ((Val vs), σs) ≥ ((Val vt), σt) : Φ →
   ∀ r_f (WSAT: wsat (r_f ⋅ r) σs σt),

theories/sim/refl.v

@@ -70,30 +70,26 @@ Proof.
 Qed.
 
 Lemma expr_wf_soundness r e :
-  expr_wf e → sem_wf r e e.
+  ✓ r → expr_wf e → sem_wf r e e.
 Proof.
-  revert r. induction e using expr_ind; simpl; intros r Hwf.
+  revert r. induction e using expr_ind; simpl; intros r Hvalid.
   - (* Value *)
-    move=>_ _ /=.
+    move=>Hwf _ _ /=.
     apply sim_simple_val.
-    split; first done.
-    split; first done. split; first done.
+    do 3 (split; first done).
     apply value_wf_soundness. done.
   - (* Variable *)
-    move=>{Hwf} xs Hxswf /=.
+    move=>_ xs Hxswf /=.
     rewrite !lookup_fmap. specialize (Hxswf x).
     destruct (xs !! x); simplify_eq/=.
     + destruct p as [rs rt].
       intros σs σt ??. eapply sim_body_result=>_.
-      split; first done.
-      split; first done. split; first done.
+      do 3 (split; first done).
       eapply (Hxswf (rs, rt)). done.
-    + simpl.
-      (* FIXME: need lemma for when both sides are stuck on an unbound var. *)
-      admit.
+    + simpl. apply sim_simple_var.
   - (* Call *)
-    move=>xs Hxswf /=. sim_bind (subst_map _ e) (subst_map _ e).
-    eapply sim_simple_post_mono, IHe; [|by apply Hwf|done].
+    move=>[Hwf1 Hwf2] xs Hxswf /=. sim_bind (subst_map _ e) (subst_map _ e).
+    eapply sim_simple_post_mono, IHe; [|by auto..].
     intros r' n' rs css' rt cst' (-> & -> & -> & Hrel). simpl.
     admit.
   - (* InitCall *) done.
@@ -101,25 +97,36 @@ Proof.
   - (* Proj *) admit.
   - (* Conc *) admit.
   - (* BinOp *) admit.
-  - (* Place *) admit.
-  - (* Deref *) admit.
-  - (* Ref *) admit.
+  - (* Place *) done.
+  - (* Deref *)
+    move=>Hwf xs Hxswf /=. sim_bind (subst_map _ e) (subst_map _ e).
+    eapply sim_simple_post_mono, IHe; [|by auto..].
+    intros r' n' rs css' rt cst' (-> & -> & -> & Hrel). simpl.
+    Fail eapply sim_simple_deref.
+    admit.
+  - (* Ref *)
+    move=>Hwf xs Hxswf /=. sim_bind (subst_map _ e) (subst_map _ e).
+    eapply sim_simple_post_mono, IHe; [|by auto..].
+    intros r' n' rs css' rt cst' (-> & -> & -> & Hrel). simpl.
+    Fail eapply sim_simple_ref.
+    admit.
   - (* Copy *) admit.
   - (* Write *) admit.
   - (* Alloc *) admit.
   - (* Free *) done.
   - (* Retag *) admit.
   - (* Let *)
-    move=>xs Hxs /=. sim_bind (subst_map _ e1) (subst_map _ e1).
-    eapply sim_simple_post_mono, IHe1; [|by apply Hwf|done].
+    move=>[Hwf1 Hwf2] xs Hxs /=. sim_bind (subst_map _ e1) (subst_map _ e1).
+    eapply sim_simple_frame_core.
+    eapply sim_simple_post_mono, IHe1; [|by auto..].
     intros r' n' rs css' rt cst' (-> & -> & -> & Hrel). simpl.
-    intros σs σt ??. eapply sim_body_let.
-    { destruct rs; eauto. } { destruct rt; eauto. }
+    eapply sim_simple_let; [destruct rs, rt; by eauto..|].
     rewrite !subst'_subst_map.
     change rs with (fst (rs, rt)). change rt with (snd (rs, rt)) at 2.
     rewrite !binder_insert_map.
-    eapply sim_simplify', IHe2; [done..|by apply Hwf|].
-    admit. (* resources dont match?? *)
+    (* FIXME: we need validity. *)
+    Fail eapply IHe2; [|by auto..].
+    admit.
   - (* Case *) admit.
 Admitted.
 
@@ -144,7 +151,7 @@ Proof.
   }
   destruct (subst_l_map _ _ _ _ _ _ _ (rrel vrel r) Hsubst1 Hsubst2) as (map & -> & -> & Hmap).
   { clear -Hrel. induction Hrel; eauto using Forall2. }
-  eapply sim_simplify, expr_wf_soundness; [done..|].
+  Fail eapply sim_simplify, expr_wf_soundness; [done..|].
   admit. (* resource stuff. *)
 Admitted.
 

theories/sim/simple.v

@@ -54,6 +54,15 @@ Proof.
   intros HΦ <-<-. eapply sim_simplify. done.
 Qed.
 
+Lemma sim_simple_frame_core Φ r n fs ft es css et cst :
+  r ⊨ˢ{ n , fs , ft }
+    (es, css) ≥ (et, cst)
+  : (λ r' n' es' css' et' cst', Φ (core r ⋅ r') n' es' css' et' cst') →
+  r ⊨ˢ{ n , fs , ft } (es, css) ≥ (et, cst) : Φ.
+Proof.
+  intros Hold σs σt <-<-. eapply sim_body_frame_core. auto.
+Qed.
+
 Lemma sim_simple_post_mono Φ1 Φ2 r n fs ft es css et cst :
   Φ1 <6= Φ2 →
   r ⊨ˢ{ n , fs , ft } (es, css) ≥ (et, cst) : Φ1 →
@@ -136,9 +145,8 @@ Lemma sim_simple_call n' vls vlt rv fs ft r r' n fid css cst Φ :
   r ⊨ˢ{n,fs,ft}
     (Call #[ScFnPtr fid] (Val <$> vls), css) ≥ (Call #[ScFnPtr fid] (Val <$> vlt), cst) : Φ.
 Proof.
-  intros Hfns Hrel Hres HH σs σt <-<-.
-  eapply sim_body_res_proper; last apply: sim_body_step_over_call.
-  - symmetry. exact: Hres.
+  intros Hfns Hrel Hres HH σs σt <-<-. rewrite Hres.
+  apply: sim_body_step_over_call.
   - done.
   - done.
   - intros. exists n'. eapply sim_body_res_proper; last apply: HH; try done.

theories/sim/tactics.v

@@ -4,21 +4,33 @@ From stbor.sim Require Import body.
 
 Ltac reshape_expr e tac :=
   (* [vs] is the accumulator *)
-  let rec go_fun K f vs es :=
+  let rec go_list K Ki v vs es :=
     match es with
-    | (Val ?v) :: ?es => go_fun K f (v :: vs) es
-    | ?e :: ?es => go (CallRCtx f (reverse vs) es :: K) e
+    | (Val ?v) :: ?es => go_list K v (v :: vs) es
+    | ?e :: ?es => go (Ki v (reverse vs) es :: K) e
     end
   (* [K] accumulates the context *)
   with go K e :=
   match e with
   | _ => tac K e
-  | Let ?x ?e1 ?e2 => go (LetCtx x e2 :: K) e1
-  | Call (Val ?v) ?el => go_fun K v (@nil val) el
+  | Call (Val ?v) ?el => go_list K CallRCtx v (@nil val) el
   | Call ?e ?el => go (CallLCtx el :: K) e
+  | EndCall ?e => go (EndCallCtx :: K) e
   | BinOp ?op (Val ?v1) ?e2 => go (BinOpRCtx op v1 :: K) e2
   | BinOp ?op ?e1 ?e2 => go (BinOpLCtx op e2 :: K) e1
-  (* FIXME: add remaining context items *)
+  | Proj (Val ?v1) ?e2 => go (ProjRCtx v1 :: K) e2
+  | Proj ?e1 ?e2 => go (ProjLCtx op e2 :: K) e1
+  | Conc (Val ?v1) ?e2 => go (ConcRCtx v1 :: K) e2
+  | Conc ?e1 ?e2 => go (ConcLCtx op e2 :: K) e1
+  | Copy ?e => go (CopyCtx :: K) e
+  | Write (Val ?v1) ?e2 => go (WriteRCtx v1 :: K) e2
+  | Write ?e1 ?e2 => go (WriteLCtx op e2 :: K) e1
+  | Free ?e => go (FreeCtx :: K) e
+  | Deref ?e ?T => go (DerefCtx T :: K) e
+  | Ref ?e => go (RefCtx :: K) e
+  | Retag ?e ?k => go (RetagCtx k :: K) e
+  | Let ?x ?e1 ?e2 => go (LetCtx x e2 :: K) e1
+  | CaseCtx (Val ?v) ?el => go_list K CaseCtx v (@nil val) el
   end
   in go (@nil ectx_item) e.