WIP: ex3

theories/opt/ex3.v

-From stbor.sim Require Import local invariant refl_step.
+From stbor.sim Require Import local invariant refl.
+From stbor.sim Require Import tactics simple program.
+From stbor.sim Require Import refl_step right_step left_step derived_step.
 
 Set Default Proof Using "Type".
 
 (** Moving a write to a mutable reference up across unknown code. *)
 
-(* TODO: check if Free is in the right place *)
 (* Assuming x : &mut i32 *)
-Definition ex3 : function :=
+Definition ex3_unopt : function :=
   fun: ["i"],
     let: "x" := new_place (&mut int) "i" in
     retag_place "x" (RefPtr Mutable) int FnEntry ;;
@@ -39,6 +40,80 @@ Definition ex3_opt_2 : function :=
   .
 
 (* TODO: show refinement to be transitive *)
-Lemma ex3_sim_fun : ⊨ᶠ ex3 ≥ ex3_opt_1.
+Lemma ex3_sim_fun : ⊨ᶠ ex3_unopt ≥ ex3_opt_1.
 Proof.
+  (* We can't use sim_simple because we need to track our stack frame id *)
+  intros fs ft LOOK rarg es et vls vlt σs σt FREL SUBSTs SUBSTt.
+  (* Substitution *)
+  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 [|arg []]; [done| |done]. clear Hls Hlt.
+  inversion FREL as [|???? VREL _].
+  clear FREL. specialize (vrel_eq _ _ _ VREL)=>?.
+  simplify_eq. simpl in SUBSTs, SUBSTt. simplify_eq/=.
+  (* Init call *)
+  exists 10%nat. apply sim_body_init_call=>/= Eqcs.
+  (* Alloc local *)
+  sim_apply sim_body_alloc_local => /=.
+  sim_apply sim_body_let=>/=.
+  (* Write local *)
+  sim_apply sim_body_write_local_1; [solve_sim..|].
+  intros sarg ? σs1 σt1. subst arg.
+  sim_apply sim_body_let=>/=.
+  apply: sim_body_result => _.
+  (* Retag a local place *)
+  sim_apply sim_body_let=>/=.
+  apply Forall2_cons_inv in VREL as [AREL _].
+  sim_apply sim_body_let=>/=.
+    (* Copy local place *)
+    sim_apply sim_body_copy_local; [solve_sim..|].
+    sim_apply sim_body_result => /= VALID.
+    (* Retag *)
+    sim_apply sim_body_retag_ref_fn_entry; [simpl; lia|eauto| |done|..].
+    { rewrite -cmra_assoc (cmra_comm (res_cs _ _)) cmra_assoc. eauto. }
+    { eapply arel_mono; [done|..|exact AREL]. solve_res. } clear VALID.
+    move=> l' told tnew hplt α' nxtp' r0 ? _ IS_i InD σs2 σt2 s_new tk _ /=.
+    subst sarg.
+    have IS_O := (IS_i O ltac:(simpl; lia)). rewrite shift_loc_0_nat in IS_O.
+    destruct IS_O as [(ss & st & Eql' & Eqss & Eqst & ARELs) TOP].
+    rewrite insert_empty.
+    (* Write local *)
+    sim_apply sim_body_write_local_1; [solve_sim..|].
+    intros s ?. simplify_eq. simpl.
+  sim_apply sim_body_let=>/=.
+  (* Copy local place *)
+  sim_apply sim_body_copy_local; [solve_sim..|].
+  sim_apply sim_body_result => /= VALID.
+  sim_apply (sim_body_deref _ _ _ _ (ValR _)).
+  move => ?? Eq. symmetry in Eq. simplify_eq/=.
+  (* Write unique of 42 *)
+  sim_apply sim_body_write_unique_1;
+    [done|solve_sim|by eexists|..]; [solve_sim..|].
+  move => σs3 σt3 TOP3 /=.
+  sim_apply sim_body_let=>/=.
+  (* Copy local (right) *)
+  sim_apply_r sim_body_copy_local_r; [solve_sim..|].
+  apply: sim_body_result=>_/=.
+  (* Write protected right *)
+  sim_apply_r sim_body_deref_r =>/=.
+  sim_apply_r sim_body_write_protected_r;
+    [solve_sim..|by rewrite lookup_insert |by rewrite lookup_insert
+    |by eapply (elem_of_dom_2 _ _ _ Eql')|].
+  intros Eqss3 σt3' rt'. simpl.
+  apply: sim_body_result=>_/=.
+  sim_apply sim_body_let_r =>/=.
+  (* Call *)
+  rewrite -(right_id ε op (_ ⋅ rt')).
+  sim_bind (Call _ _) (Call _ _). (* TODO: sim_apply fails to instantiate evars *)
+  apply (sim_body_step_over_call _ _ _ ε _ (ValR _) [] []); [solve_sim..|].
+  move => rf' ? _ _ frs' frt' σs4 σt4 VREL' /= Eqs1 Eqs2 ? _ _. simplify_eq.
+  exists 5%nat.
+  apply: sim_body_result=>_ /=.
+  sim_apply sim_body_let=>/=.
+  (* Copy local (left) *)
+  sim_apply_l sim_body_copy_local_l; [solve_sim..|].
+  apply: sim_body_result=>_/=.
+  (* Write protected left *)
+  sim_apply_l sim_body_deref_l =>/=.
 Abort.

theories/opt/ex3_down.v

@@ -5,7 +5,7 @@ Set Default Proof Using "Type".
 (** Moving a write to a mutable reference down across unknown code. *)
 
 (* Assuming x : &mut i32 *)
-Definition ex3_down : function :=
+Definition ex3_down_unopt : function :=
   fun: ["i"],
     let: "x" := new_place (&mut int) "i" in
     retag_place "x" (RefPtr Mutable) int FnEntry ;;
@@ -37,6 +37,6 @@ Definition ex3_down_opt_2 : function :=
     "v"
     .
 
-Lemma ex3_down_sim_fun : ⊨ᶠ ex3_down ≥ ex3_down_opt_1.
+Lemma ex3_down_sim_fun : ⊨ᶠ ex3_down_unopt ≥ ex3_down_opt_1.
 Proof.
 Abort.

theories/sim/right_step.v

@@ -302,4 +302,184 @@ Proof.
   - left. by apply CONT.
 Qed.
 
+
+(* Protected write *)
+Lemma sim_body_write_protected_r
+  fs ft (r r' r'': resUR) (h: heaplet) n (l: loc) t T (ss st st': scalar)
+  c Ts L es σs σt Φ :
+  (if st' is ScPtr l' t' then False else True) →
+  let tk := tkUnique in
+  tsize T = 1%nat →
+  r ≡ r' ⋅ res_tag t tk h →
+  r' ≡ r'' ⋅ res_cs c Ts →
+  h !! l = Some (ss, st) →
+  Ts !! t = Some L →
+  l ∈ L →
+  (σs.(shp) !! l = Some ss →
+    let σt' := mkState (<[l := st']> σt.(shp)) σt.(sst) σt.(scs) σt.(snp) σt.(snc) in
+    let rt' := res_tag t tk (<[l := (ss, st')]> h) in
+    r' ⋅ rt' ⊨{n,fs,ft} (es, σs) ≥ (#[☠], σt') : Φ : Prop) →
+  r ⊨{S n,fs,ft} (es, σs) ≥ (Place l (Tagged t) T <- #[st'], σt) : Φ.
+Proof.
+  intros NL tk LenT Eqr Eqr' Eqs EqTs InL CONT. pfold.
+  intros NT r_f WSAT. have WSAT1 := WSAT.
+
+  destruct WSAT as (WFS & WFT & VALID & PINV & CINV & SREL).
+
+  have HLc: (r_f ⋅ r).(rcm) !! c ≡ Excl' Ts.
+  { rewrite Eqr Eqr' 2!cmra_assoc lookup_op right_id.
+    apply (cmap_lookup_op_unique_included (res_cs c Ts).(rcm)).
+    - move : (proj2 VALID). rewrite Eqr Eqr' 2!cmra_assoc => VALID2.
+      by apply (cmra_valid_included _ _ VALID2), cmra_included_l.
+    - by apply cmra_included_r.
+    - by rewrite res_cs_lookup. }
+  destruct (CINV _ _ HLc) as [INc CINVc].
+  specialize (CINVc _ _ EqTs) as [Ltc CINVc].
+  specialize (CINVc _ InL) as (stk & pm & Eqstk & Instk & NDIS).
+
+  have HLtrf : (r_f ⋅ r).(rtm) !! t ≡ Some (to_tgkR tk, to_agree <$> h).
+  { rewrite ->Eqr in VALID. move : VALID. rewrite cmra_assoc => VALID.
+    rewrite Eqr cmra_assoc.
+    apply tmap_lookup_op_r_uniq_equiv; [apply VALID|].
+    by rewrite res_tag_lookup. }
+  have HLl : (to_agree <$> h) !! l ≡ Some (to_agree (ss, st))
+    by rewrite lookup_fmap Eqs.
+
+  destruct (PINV _ _ _ HLtrf) as [Ltt Pt].
+  specialize (Pt l ss st HLl) as (Eqst & Eqss & TPO).
+  { by exists stk, pm, (Some c). }
+
+  have [ns Eqstk']: ∃ n, access1 stk AccessWrite (Tagged t) σt.(scs) = Some (n, stk).
+  { destruct TPO as (stk1 & Eqstk1 & pro & TPO).
+    rewrite Eqstk1 in Eqstk. simplify_eq.
+    by eapply tag_unique_head_access. }
+  have Eqα : memory_written σt.(sst) σt.(scs) l (Tagged t) (tsize T) = Some σt.(sst).
+  { rewrite LenT /memory_written /= shift_loc_0_nat Eqstk /= Eqstk' /= insert_id //. }
+
+  set σt' := mkState (<[l := st']> σt.(shp)) σt.(sst) σt.(scs) σt.(snp) σt.(snc).
+  have STEPT: ((Place l (Tagged t) T <- #[st'])%E, σt) ~{ft}~> (#[☠]%E, σt').
+  { eapply (head_step_fill_tstep _ []); eapply write_head_step'; eauto.
+    - move => ?? /elem_of_list_singleton ?. by subst st'.
+    - clear -Eqst LenT.
+      intros i. rewrite LenT=>?. destruct i; [|lia].
+      rewrite shift_loc_0_nat. by eapply elem_of_dom_2. }
+
+  split; [right; by do 2 eexists|done|].
+  constructor 1. intros et1 σt1 STEPT1.
+  destruct (tstep_write_inv _ (PlaceR _ _ _) (ValR _) _ _ _ STEPT1)
+      as (l1&t1&T1& vs1 & α1 & EqH & ? & Eqvs & Eqα' & _ & _ & _ & ?).
+  clear STEPT1. symmetry in EqH. move : HLtrf. simplify_eq => HLtrf /=.
+
+  set rt' := res_tag t tk (<[l := (ss, st')]> h).
+  exists es, σs, (r' ⋅ rt'), n.
+  split; last split;
+    [right; split; [lia|done]| |left; by apply CONT].
+
+  have EQrcm: (r_f ⋅ r).(rcm) ≡ (r_f ⋅ r' ⋅ rt').(rcm)
+    by rewrite Eqr cmra_assoc.
+  have HLNt: (r_f ⋅ r').(rtm) !! t = None.
+  { destruct ((r_f ⋅ r').(rtm) !! t) as [ls|] eqn:Eqls; [|done].
+    exfalso. move : HLtrf.
+    rewrite Eqr cmra_assoc lookup_op Eqls res_tag_lookup.
+    apply tagKindR_exclusive_heaplet. }
+  have HLtrf' :
+    (r_f ⋅ r' ⋅ rt').(rtm) !! t ≡ Some (to_tgkR tk, to_hplR (<[l:=(ss, st')]> h)).
+  { by rewrite lookup_op HLNt res_tag_lookup left_id. }
+
+  have VALIDr: ✓ (r_f ⋅ r' ⋅ rt').
+  { move : VALID. rewrite Eqr cmra_assoc => VALID.
+    apply (local_update_discrete_valid_frame _ _ _ VALID).
+    apply res_tag_uniq_local_update; [by right|done]. }
+
+  rewrite cmra_assoc.
+  split; last split; last split; last split; last split.
+  - done.
+  - by apply (tstep_wf _ _ _ STEPT WFT).
+  - done.
+  - intros t1 k1 h1 Eqh1.
+    case (decide (t1 = t)) => ?; [subst t1|].
+    + split; [done|].
+      specialize (PINV _ _ _ HLtrf) as [? PINV].
+      have [? Eqh]: k1 = tk ∧ h1 ≡ to_agree <$> (<[l:=(ss, st')]> h).
+      { move : Eqh1. rewrite HLtrf'.
+        by intros [?%leibniz_equiv_iff%to_tgkR_inj ?]%Some_equiv_inj. } subst k1.
+      intros l1 ss1 st1. rewrite Eqh lookup_fmap.
+      case (decide (l1 = l)) => ?; [subst l1|].
+      * rewrite lookup_insert. intros Eq%Some_equiv_inj%to_agree_inj.
+        symmetry in Eq. simplify_eq.
+        rewrite /= lookup_insert. intros PRE. do 2 (split; [done|]).
+        specialize (PINV l ss st). rewrite lookup_fmap Eqs in PINV.
+        by specialize (PINV ltac:(done) PRE) as (Eqst1 & Eqss1 & HD).
+      * rewrite lookup_insert_ne // -lookup_fmap.
+        intros Eq. specialize (PINV _ _ _ Eq).
+        by setoid_rewrite lookup_insert_ne.
+
+    + have Eqh : (r_f ⋅ r).(rtm) !! t1 ≡ Some (to_tgkR k1, h1).
+      { rewrite Eqr cmra_assoc lookup_op res_tag_lookup_ne; [|done].
+        move : Eqh1. by rewrite lookup_op res_tag_lookup_ne. }
+      specialize (PINV _ _ _ Eqh) as [Ltt1 PINV].
+      split; [done|]. intros l1 ss1 st1 Eql1 PRE.
+      specialize (PINV _ _ _ Eql1 PRE) as (Eqst1 & Eqss1 & HPO).
+      rewrite /= lookup_insert_ne; [done|].
+      intros ?. subst l1.
+      (* t1 ≠ t, t is top of stack(l), t1 is top or SRO in stack (l).
+            This cannot happen. *)
+      exfalso.
+      have ND := proj2 (state_wf_stack_item _ WFT _ _ Eqstk).
+      destruct k1; simpl in *.
+      { rewrite Eqstk in HPO. simplify_eq.
+        eapply (access1_write_remove_incompatible_head _ (Tagged t) t1 _ _ _ ND);
+          eauto.
+        - by exists None, [].
+        - by inversion 1.
+        - by left. }
+      { destruct HPO as (stk1 & Eqstk1 & opro & HD).
+        rewrite Eqstk1 in Eqstk. simplify_eq.
+        eapply (access1_write_remove_incompatible_head _ (Tagged t) t1 _ _ _ ND);
+          eauto.
+        - by inversion 1.
+        - destruct HD as [? HD]. rewrite HD. by left. }
+      { destruct HPO as (stk1 & Eqstk1 & HD).
+        rewrite Eqstk1 in Eqstk. simplify_eq.
+        destruct PRE as (stk1 & pm1 & opro & Eqstk & In1 & ?).
+        rewrite Eqstk in Eqstk1. simplify_eq.
+        eapply (access1_write_remove_incompatible_active_SRO _
+                  (Tagged t) t1 _ _ _ ND); eauto. }
+  - move => ??. rewrite -EQrcm. by apply CINV.
+  - destruct SREL as (?&?&?&?& PB). do 4 (split; [done|]).
+    move => l1 /= InD.
+    have InD' : l1 ∈ dom (gset loc) σt.(shp).
+    { move : InD. rewrite dom_map_insert_is_Some; [done|by eexists]. }
+    case (decide (l1 = l)) => ?; [subst l1|].
+    { right.
+      exists t, tk, (to_hplR (<[l := (ss, st')]> h)). split; last split.
+      - done.
+      - rewrite /to_hplR lookup_fmap lookup_insert. by eexists.
+      - right. split; [done|]. exists c, Ts, L.
+        rewrite -EQrcm. by rewrite HLc. }
+    specialize (PB _ InD') as [PB|[t1 PV]]; [left|right].
+    { intros st1. rewrite /= lookup_insert_ne; [|done].
+      move => /PB [ss1 [Eqss1 ARELs]].
+      exists ss1. split; [done|].
+      move : ARELs. rewrite Eqr cmra_assoc.
+      apply arel_res_tag_overwrite. by right. }
+    destruct PV as (k1 & h1 & Eqt1 & IS1 & CASE).
+    case (decide (t1 = t)) => ?; [subst t1|].
+    { have [? Eqh]: k1 = tk ∧ h1 ≡ to_agree <$> h.
+      { move : Eqt1. rewrite HLtrf.
+        by intros [?%leibniz_equiv_iff%to_tgkR_inj ?]%Some_equiv_inj. }
+      subst k1.
+      exists t, tk, (to_hplR (<[l := (ss, st')]> h)). split; last split.
+      - done.
+      - rewrite /to_hplR lookup_fmap lookup_insert_ne; [|done].
+        move : (Eqh l1). destruct IS1 as [? Eq1].
+        rewrite Eq1 lookup_fmap.
+        destruct (h !! l1) eqn:Eqhl1; rewrite Eqhl1;
+          [by eexists|by inversion 1].
+      - by setoid_rewrite <- EQrcm. }
+    exists t1, k1, h1. setoid_rewrite <- EQrcm. split; [|done].
+    rewrite lookup_op res_tag_lookup_ne; [|done].
+    move : Eqt1. by rewrite Eqr cmra_assoc lookup_op res_tag_lookup_ne.
+Qed.
+
 End right.