simple rule for writes, and some res automation

theories/lang/expr_semantics.v

@@ -306,7 +306,7 @@ Inductive pure_expr_step (FNs: fn_env) (h: mem) : expr → event → expr → Pr
                          SilentEvt (Place (l +ₗ off) lbor T') *)
 | LetBS x e1 e2 e' :
     is_Some (to_result e1) →
-    subst x e1 e2 = e' →
+    subst' x e1 e2 = e' →
     pure_expr_step FNs h (let: x := e1 in e2) SilentEvt e'
 | CaseBS i el e :
     0 ≤ i →

theories/lang/steps_inversion.v

@@ -314,10 +314,10 @@ Proof.
   - by exists (Ki :: K').
 Qed.
 
-Lemma tstep_let_inv (x: string) e1 e2 e' σ σ'
+Lemma tstep_let_inv (x: binder) e1 e2 e' σ σ'
   (TERM: terminal e1)
   (STEP: ((let: x := e1 in e2)%E, σ) ~{fns}~> (e', σ')) :
-  e' = subst x e1 e2  ∧ σ' = σ.
+  e' = subst' x e1 e2  ∧ σ' = σ.
 Proof.
   inv_tstep. symmetry in Eq.
   destruct (fill_let_decompose _ _ _ _ _ Eq)

theories/opt/ex1.v

@@ -33,6 +33,12 @@ Proof.
   apply sim_simple_init_call=> c /= {css}.
   (* Alloc *)
   sim_apply sim_simple_alloc_local=> l t /=.
-  (* Let *)
   sim_apply sim_simple_let_place=>/=.
+  (* Write *)
+  rewrite (vrel_eq _ _ _ FREL).
+  sim_apply sim_simple_write_local; first solve_res.
+  intros s ->. clear dependent vs. simpl.
+  sim_apply sim_simple_let_val=>/=.
+  apply sim_simple_place.
+
 Abort.

theories/sim/refl_step.v

@@ -1240,28 +1240,28 @@ Qed.
 (** Let *)
 Lemma sim_body_let fs ft r n x es1 es2 et1 et2 σs σt Φ :
   terminal es1 → terminal et1 →
-  r ⊨{n,fs,ft} (subst x es1 es2, σs) ≥ (subst x et1 et2, σt) : Φ →
-  r ⊨{n,fs,ft} (let: x := es1 in es2, σs) ≥ ((let: x := et1 in et2), σt) : Φ.
+  r ⊨{n,fs,ft} (subst' x es1 es2, σs) ≥ (subst' x et1 et2, σt) : Φ →
+  r ⊨{n,fs,ft} (let: x := es1 in es2, σs) ≥ (let: x := et1 in et2, σt) : Φ.
 Proof.
   intros TS TT SIM. pfold.
   intros NT r_f WSAT. split; [|done|].
   { right. do 2 eexists. eapply (head_step_fill_tstep _ []).
-    econstructor 1. econstructor; eauto. }
+    econstructor 1. eapply LetBS; eauto. }
   constructor 1. intros.
   destruct (tstep_let_inv _ _ _ _ _ _ _ TT STEPT). subst et' σt'.
-  exists (subst x es1 es2), σs, r, n. split.
+  exists (subst' x es1 es2), σs, r, n. split.
   { left. constructor 1. eapply (head_step_fill_tstep _ []).
     by econstructor; econstructor. }
   split; [done|]. by left.
 Qed.
 
-Lemma sim_body_let_val fs ft r n x (vs1 vt1: value) es2 et2 σs σt Φ :
-  r ⊨{n,fs,ft} (subst x vs1 es2, σs) ≥ (subst x vt1 et2, σt) : Φ →
-  r ⊨{n,fs,ft} (let: x := vs1 in es2, σs) ≥ ((let: x := vt1 in et2), σt) : Φ.
+Lemma sim_body_let_val fs ft r n b (vs1 vt1: value) es2 et2 σs σt Φ :
+  r ⊨{n,fs,ft} (subst' b vs1 es2, σs) ≥ (subst' b vt1 et2, σt) : Φ →
+  r ⊨{n,fs,ft} (let: b := vs1 in es2, σs) ≥ (let: b := vt1 in et2, σt) : Φ.
 Proof. apply sim_body_let; eauto. Qed.
 
 Lemma sim_body_let_place fs ft r n x ls lt ts tt tys tyt es2 et2 σs σt Φ :
-  r ⊨{n,fs,ft} (subst x (Place ls ts tys) es2, σs) ≥ (subst x (Place lt tt tyt) et2, σt) : Φ →
+  r ⊨{n,fs,ft} (subst' x (Place ls ts tys) es2, σs) ≥ (subst' x (Place lt tt tyt) et2, σt) : Φ →
   r ⊨{n,fs,ft} (let: x := Place ls ts tys in es2, σs) ≥ ((let: x := Place lt tt tyt in et2), σt) : Φ.
 Proof. apply sim_body_let; eauto. Qed.
 

theories/sim/simple.v

@@ -80,6 +80,20 @@ Proof.
   clear. simpl. intros r n vs σs vt σt HH. exact: HH.
 Qed.
 
+Lemma sim_simple_val fs ft r n (vs vt: value) css cst Φ :
+  Φ r n vs css vt cst →
+  r ⊨ˢ{S n,fs,ft} (vs, css) ≥ (vt, cst) : Φ.
+Proof.
+  intros HH σs σt <-<-. eapply (sim_body_result _ _ _ _ vs vt). done.
+Qed.
+
+Lemma sim_simple_place fs ft r n ls lt ts tt tys tyt css cst Φ :
+  Φ r n (PlaceR ls ts tys) css (PlaceR lt tt tyt) cst →
+  r ⊨ˢ{S n,fs,ft} (Place ls ts tys, css) ≥ (Place lt tt tyt, cst) : Φ.
+Proof.
+  intros HH σs σt <-<-. eapply (sim_body_result _ _ _ _ (PlaceR _ _ _) (PlaceR _ _ _)). done.
+Qed.
+
 (** * Administrative *)
 Lemma sim_simple_init_call fs ft r n es css et cst Φ :
   (∀ c: call_id,
@@ -93,22 +107,32 @@ Qed.
 
 (** * Memory *)
 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) →
+  (∀ (l: loc) (tg: nat),
+    let r' := res_mapsto l ☠ (init_stack (Tagged tg)) in
+    Φ (r ⋅ r') n (PlaceR l (Tagged tg) T) css (PlaceR l (Tagged tg) T) cst) →
   r ⊨ˢ{n,fs,ft} (Alloc T, css) ≥ (Alloc T, cst) : Φ.
 Proof.
   intros HH σs σt <-<-. apply sim_body_alloc_local=>/=. eauto.
 Qed.
 
+(* FIXME notation is so broken, can one write this down without the Val? *)
+Lemma sim_simple_write_local fs ft r r' n l tg Ts Tt v v' css cst Φ :
+  r ≡ r' ⋅ res_mapsto l v' (init_stack (Tagged tg)) →
+  (∀ s, v = [s] → Φ (r' ⋅ res_mapsto l s (init_stack (Tagged tg))) n (ValR [☠%S]) css (ValR [☠%S]) cst) →
+  r ⊨ˢ{n,fs,ft}
+    (Place l (Tagged tg) Ts <- #v, css) ≥ (Place l (Tagged tg) Tt <- #v, cst)
+  : Φ.
+Proof.
+Admitted.
+
 (** * Pure *)
 Lemma sim_simple_let_val fs ft r n x (vs1 vt1: value) es2 et2 css cst Φ :
-  r ⊨ˢ{n,fs,ft} (subst x vs1 es2, css) ≥ (subst x vt1 et2, cst) : Φ →
+  r ⊨ˢ{n,fs,ft} (subst' x vs1 es2, css) ≥ (subst' x vt1 et2, cst) : Φ →
   r ⊨ˢ{n,fs,ft} (let: x := vs1 in es2, css) ≥ ((let: x := vt1 in et2), cst) : Φ.
 Proof. intros HH σs σt <-<-. apply sim_body_let; eauto. Qed.
 
 Lemma sim_simple_let_place fs ft r n x ls lt ts tt tys tyt es2 et2 css cst Φ :
-  r ⊨ˢ{n,fs,ft} (subst x (Place ls ts tys) es2, css) ≥ (subst x (Place lt tt tyt) et2, cst) : Φ →
+  r ⊨ˢ{n,fs,ft} (subst' x (Place ls ts tys) es2, css) ≥ (subst' x (Place lt tt tyt) et2, cst) : Φ →
   r ⊨ˢ{n,fs,ft} (let: x := Place ls ts tys in es2, css) ≥ ((let: x := Place lt tt tyt in et2), cst) : Φ.
 Proof. intros HH σs σt <-<-. apply sim_body_let; eauto. Qed.
 

theories/sim/tactics.v

@@ -22,6 +22,28 @@ Ltac reshape_expr e tac :=
   end
   in go (@nil ectx_item) e.
 
+
+(** bind if K is not empty. Otherwise do nothing.
+Binds cost us steps, so don't waste them! *)
+Ltac sim_body_bind_core Ks Kt es et :=
+  (* Ltac is SUCH a bad language... *)
+  match Ks with
+  | [] => match Kt with
+          | [] => idtac
+          | _ => eapply (sim_body_bind _ _ _ _ Ks Kt es et)
+          end
+  | _ => eapply (sim_body_bind _ _ _ _ Ks Kt es et)
+  end.
+Ltac sim_simple_bind_core Ks Kt es et :=
+  (* Ltac is SUCH a bad language... *)
+  match Ks with
+  | [] => match Kt with
+          | [] => idtac
+          | _ => eapply (sim_simple_bind _ _ Ks Kt es et)
+          end
+  | _ => eapply (sim_simple_bind _ _ Ks Kt es et)
+  end.
+
 Tactic Notation "sim_bind" open_constr(efocs) open_constr(efoct) :=
   match goal with 
   | |- _ ⊨{_,_,_} (?es, _) ≥ (?et, _) : _ =>
@@ -29,7 +51,7 @@ Tactic Notation "sim_bind" open_constr(efocs) open_constr(efoct) :=
       unify es efocs;
       reshape_expr et ltac:(fun Kt et =>
         unify et efoct;
-        eapply (sim_body_bind _ _ _ _ Ks Kt es et)
+        sim_body_bind_core Ks Kt es et
       )
     )
   | |- _ ⊨ˢ{_,_,_} (?es, _) ≥ (?et, _) : _ =>
@@ -37,7 +59,7 @@ Tactic Notation "sim_bind" open_constr(efocs) open_constr(efoct) :=
       unify es efocs;
       reshape_expr et ltac:(fun Kt et =>
         unify et efoct;
-        eapply (sim_simple_bind _ _ Ks Kt es et)
+        sim_simple_bind_core Ks Kt es et
       )
     )
   end.
@@ -47,15 +69,45 @@ Tactic Notation "sim_apply" open_constr(lem) :=
   | |- _ ⊨{_,_,_} (?es, _) ≥ (?et, _) : _ =>
     reshape_expr es ltac:(fun Ks es =>
       reshape_expr et ltac:(fun Kt et =>
-        eapply (sim_body_bind _ _ _ _ Ks Kt es et);
+        sim_body_bind_core Ks Kt es et;
         eapply lem
       )
     )
   | |- _ ⊨ˢ{_,_,_} (?es, _) ≥ (?et, _) : _ =>
     reshape_expr es ltac:(fun Ks es =>
       reshape_expr et ltac:(fun Kt et =>
-        eapply (sim_simple_bind _ _ Ks Kt es et);
+        sim_simple_bind_core Ks Kt es et;
         eapply lem
       )
     )
   end.
+
+
+(** The expectation is that lemmas state their resource requirements as
+[r ≡ frame ⋅ what_lemma_needs].  Users eapply the lemma, and [frame]
+becomes an evar. [solve_res] solves such goals. *)
+Lemma res_search_descend (R W T F L : resUR) :
+  T ⋅ L ≡ F ⋅ W →
+  T ⋅ L ⋅ R ≡ F ⋅ R ⋅ W.
+Proof. intros ->. rewrite - !assoc. f_equiv. exact: comm. Qed.
+Lemma res_search_found_left (F W : resUR) :
+  W ⋅ F ≡ F ⋅ W.
+Proof. exact: comm. Qed.
+Lemma res_search_singleton (R W : resUR) :
+  W ≡ ε ⋅ W.
+Proof. rewrite left_id //. Qed.
+Ltac solve_res :=
+  match goal with
+  | |- _ ⋅ _ ≡ _ =>
+      reflexivity
+  | |- _ ⋅ _ ≡ _ =>
+      exact: res_search_found_left
+  | |- _ ≡ _ =>
+      exact: res_search_singleton
+  | |- _ ⋅ _ ≡ _ =>
+    (* The descent lemma makes sure we don't descend below
+       the *last* operator. We always want to preserve having
+       an operator on the LHS. *)
+    simple apply res_search_descend;
+    solve_res
+end.