1 files changed, 680 insertions, 0 deletions

diff --git a/theories/nix/operational_props.v b/theories/nix/operational_props.v
new file mode 100644
index 0000000..4041bfe
--- /dev/null
+++ b/theories/nix/operational_props.v
@@ -0,0 +1,680 @@
+From mininix Require Export utils nix.operational.
+From stdpp Require Import options.
+
+(** Properties of operational semantics *)
+Lemma float_to_bounded_Z_ok f : int_ok (float_to_bounded_Z f).
+Proof.
+  rewrite /float_to_bounded_Z.
+  destruct (Float.to_Z f); simplify_option_eq; done.
+Qed.
+
+Lemma int_ok_alt i :
+  int_ok i ↔ ∀ n, (63 ≤ n)%Z → Z.testbit i n = bool_decide (i < 0)%Z.
+Proof.
+  rewrite -Z.bounded_iff_bits //.
+  rewrite /int_ok bool_decide_spec /int_min /int_max Z.shiftl_1_l. lia.
+Qed.
+
+Lemma int_ok_land i1 i2 : int_ok i1 → int_ok i2 → int_ok (Z.land i1 i2).
+Proof.
+  rewrite !int_ok_alt=> Hi1 Hi2 n ?. rewrite Z.land_spec Hi1 // Hi2 //.
+  apply eq_bool_prop_intro. rewrite andb_True !bool_decide_spec Z.land_neg //.
+Qed.
+
+Lemma int_ok_lor i1 i2 : int_ok i1 → int_ok i2 → int_ok (Z.lor i1 i2).
+Proof.
+  rewrite !int_ok_alt=> Hi1 Hi2 n ?. rewrite Z.lor_spec Hi1 // Hi2 //.
+  apply eq_bool_prop_intro. rewrite orb_True !bool_decide_spec Z.lor_neg //.
+Qed.
+
+Lemma int_ok_lxor i1 i2 : int_ok i1 → int_ok i2 → int_ok (Z.lxor i1 i2).
+Proof.
+  rewrite !int_ok_alt=> Hi1 Hi2 n ?. rewrite Z.lxor_spec Hi1 // Hi2 //.
+  apply eq_bool_prop_intro. rewrite xorb_True !bool_decide_spec.
+  rewrite !Z.lt_nge Z.lxor_nonneg. lia.
+Qed.
+
+Lemma sem_bin_op_num_ok {op f n1 n2 bl} :
+  num_ok n1 → num_ok n2 →
+  sem_bin_op_num op n1 = Some f → f n2 = Some bl → base_lit_ok bl.
+Proof.
+  intros; destruct op, n1, n2; simplify_option_eq;
+    try (by apply (bool_decide_pack _));
+    auto using int_ok_land, int_ok_lor, int_ok_lxor.
+Qed.
+
+Lemma sem_bin_op_string_ok {op f s1 s2} :
+  sem_bin_op_string op = Some f → base_lit_ok (f s1 s2).
+Proof. intros; destruct op; naive_solver. Qed.
+
+Global Hint Extern 0 (no_recs (_ <$> _)) => by apply map_Forall_fmap : core.
+
+Ltac inv_step := repeat
+  match goal with
+  | H : ¬no_recs (_ <$> _) |- _ => destruct H; by apply map_Forall_fmap
+  | H : ?e -{_}-> _ |- _ => assert_succeeds (is_app_constructor e); inv H
+  | H : ctx1 _ _ ?K |- _ => is_var K; inv H
+  end.
+
+Global Instance Attr_inj τ : Inj (=) (=) (Attr τ).
+Proof. by injection 1. Qed.
+
+Lemma fmap_attr_expr_Attr τ (es : gmap string expr) :
+  attr_expr <$> (Attr τ <$> es) = es.
+Proof. apply map_eq=> x. rewrite !lookup_fmap. by destruct (_ !! _). Qed.
+
+Lemma no_recs_insert αs x e : no_recs αs → no_recs (<[x:=AttrN e]> αs).
+Proof. by apply map_Forall_insert_2. Qed.
+Lemma no_recs_insert_inv αs x τ e :
+  αs !! x = None → no_recs (<[x:=Attr τ e]> αs) → no_recs αs.
+Proof. intros ??%map_Forall_insert; naive_solver. Qed.
+Lemma no_recs_lookup αs x τ e : no_recs αs → αs !! x = Some (Attr τ e) → τ = NONREC.
+Proof. intros Hall. apply Hall. Qed.
+
+Lemma no_recs_attr_subst αs ds : no_recs αs → no_recs (attr_subst ds <$> αs).
+Proof.
+  intros. eapply map_Forall_fmap, map_Forall_impl; [done|]. by intros ? [[]] [=].
+Qed.
+
+Lemma from_attr_no_recs {A} (f g : expr → A) (αs : gmap string attr) :
+  no_recs αs → from_attr f g <$> αs = g ∘ attr_expr <$> αs.
+Proof.
+  intros Hrecs. apply map_eq=> x. rewrite !lookup_fmap. specialize (Hrecs x).
+  destruct (αs !! x) as [[]|] eqn:?; naive_solver.
+Qed.
+
+Lemma sem_and_attr_empty : sem_and_attr ∅ = ELit (LitBool true).
+Proof. done. Qed.
+Lemma sem_and_attr_insert es x e :
+  es !! x = None → (∀ y, is_Some (es !! y) → attr_le x y) →
+  sem_and_attr (<[x:=e]> es) = EIf e (sem_and_attr es) (ELit (LitBool false)).
+Proof. intros. by rewrite /sem_and_attr map_fold_sorted_insert. Qed.
+
+Lemma matches_strict es ms ds x e :
+  es !! x = None →
+  ms !! x = None →
+  matches es ms false ds →
+  matches (<[x:=e]> es) ms false ds.
+Proof.
+  remember false as strict.
+  induction 3; simplify_eq/=;
+    repeat match goal with
+    | H : <[ _ := _ ]> _ !! _ = None |- _ => apply lookup_insert_None in H as [??]
+    | _ => rewrite (insert_commute _ x) //
+    | _ => constructor
+    | _ => apply lookup_insert_None
+    end; eauto.
+Qed.
+
+Lemma subst_empty e : subst ∅ e = e.
+Proof.
+  induction e; repeat destruct select (option _); do 2 f_equal/=; auto.
+  - apply map_eq=> x. rewrite lookup_fmap.
+    destruct (_ !! x) as [[e'|]|] eqn:Hx; do 2 f_equal/=. apply (H _ _ Hx).
+  - induction H; f_equal/=; auto.
+  - apply map_eq; intros i. rewrite lookup_fmap.
+    destruct (_ !! i) as [[τ e]|] eqn:?; do 2 f_equal/=.
+    by eapply (H _ (Attr _ _)).
+Qed.
+
+Lemma subst_union ds1 ds2 e :
+  subst (union_kinded ds1 ds2) e = subst ds1 (subst ds2 e).
+Proof.
+  revert ds1 ds2. induction e; intros ds1 ds2; f_equal/=; auto.
+  - rewrite lookup_union_with.
+    destruct mkd as [[[]]|],
+      (ds1 !! x) as [[[] t1]|], (ds2 !! x) as [[[] t2]|]; naive_solver.
+  - apply map_eq=> y. rewrite !lookup_fmap.
+    destruct (_ !! y) as [[e'|]|] eqn:Hy; do 2 f_equal/=.
+    rewrite -(H _ _ Hy) //.
+  - induction H; f_equal/=; auto.
+  - apply map_eq=> y. rewrite !lookup_fmap.
+    destruct (_ !! y) as [[τ e]|] eqn:Hy; do 2 f_equal/=.
+    rewrite -(H _ _ Hy) //.
+Qed.
+
+Lemma SAppL μ e1 e1' e2 :
+  e1 -{SHALLOW}-> e1' → EApp e1 e2 -{μ}-> EApp e1' e2.
+Proof. apply (SCtx (λ e, EApp e _)). constructor. Qed.
+Lemma SAppR μ ms strict e1 e2 e2' :
+  e2 -{SHALLOW}-> e2' →
+  EApp (EAbsMatch ms strict e1) e2 -{μ}-> EApp (EAbsMatch ms strict e1) e2'.
+Proof. apply SCtx. constructor. Qed.
+Lemma SSeq μ μ' e1 e1' e2 :
+  e1 -{μ'}-> e1' → ESeq μ' e1 e2 -{μ}-> ESeq μ' e1' e2.
+Proof. apply (SCtx (λ e, ESeq _ e _)). constructor. Qed.
+Lemma SList es1 e e' es2 :
+  Forall (final DEEP) es1 →
+  e -{DEEP}-> e' →
+  EList (es1 ++ e :: es2) -{DEEP}-> EList (es1 ++ e' :: es2).
+Proof. intros ?. apply (SCtx (λ e, EList (_ ++ e :: _))). by constructor. Qed.
+Lemma SAttr αs x e e' :
+  no_recs αs →
+  αs !! x = None →
+  (∀ y α, αs !! y = Some α → final DEEP (attr_expr α) ∨ attr_le x y) →
+  e -{DEEP}-> e' →
+  EAttr (<[x:=AttrN e]> αs) -{DEEP}-> EAttr (<[x:=AttrN e']> αs).
+Proof. intros ???. apply (SCtx (λ e, EAttr (<[x:=AttrN e]> _))). by constructor. Qed.
+Lemma SLetAttr μ k e1 e1' e2 :
+  e1 -{SHALLOW}-> e1' → ELetAttr k e1 e2 -{μ}-> ELetAttr k e1' e2.
+Proof. apply (SCtx (λ e, ELetAttr _ e _)). constructor. Qed.
+Lemma SBinOpL μ op e1 e1' e2 :
+  e1 -{SHALLOW}-> e1' → EBinOp op e1 e2 -{μ}-> EBinOp op e1' e2.
+Proof. apply (SCtx (λ e, EBinOp _ e _)). constructor. Qed.
+Lemma SBinOpR μ op e1 Φ e2 e2' :
+  final SHALLOW e1 → sem_bin_op op e1 Φ →
+  e2 -{SHALLOW}-> e2' → EBinOp op e1 e2 -{μ}-> EBinOp op e1 e2'.
+Proof. intros ??. apply SCtx. by econstructor. Qed.
+Lemma SIf μ e1 e1' e2 e3 :
+  e1 -{SHALLOW}-> e1' → EIf e1 e2 e3 -{μ}-> EIf e1' e2 e3.
+Proof. apply (SCtx (λ e, EIf e _ _)). constructor. Qed.
+
+Global Hint Constructors step : step.
+Global Hint Resolve SAppL SAppR SSeq SList SAttr SLetAttr SBinOpL SBinOpR SIf : step.
+
+Lemma step_not_final μ e1 e2 : e1 -{μ}-> e2 → ¬final μ e1.
+Proof.
+  assert (∀ (αs : gmap string attr) x μ e,
+    map_Forall (λ _, final DEEP ∘ attr_expr) (<[x:=Attr μ e]> αs) → final DEEP e).
+  { intros αs x μ' e Hall. eapply (Hall _ (Attr _ _)), lookup_insert. }
+  induction 1; inv 1; inv_step; decompose_Forall; naive_solver.
+Qed.
+Lemma final_nf μ e : final μ e → nf (step μ) e.
+Proof. by intros ? [??%step_not_final]. Qed.
+
+Lemma step_any_shallow μ e1 e2 :
+  e1 -{μ}-> e2 → e1 -{SHALLOW}-> e2 ∨ final SHALLOW e1.
+Proof.
+  induction 1; inv_step;
+    naive_solver eauto using final, no_recs_insert with step.
+Qed.
+
+Lemma step_shallow_any μ e1 e2 : e1 -{SHALLOW}-> e2 → e1 -{μ}-> e2.
+Proof.
+  remember SHALLOW as μ'. induction 1; inv_step; simplify_eq/=; eauto with step.
+Qed.
+Lemma steps_shallow_any μ e1 e2 : e1 -{SHALLOW}->* e2 → e1 -{μ}->* e2.
+Proof. induction 1; eauto using rtc, step_shallow_any. Qed.
+Lemma final_any_shallow μ e : final μ e → final SHALLOW e.
+Proof. destruct μ; [done|]. induction 1; simplify_eq/=; eauto using final. Qed.
+Lemma stuck_shallow_any μ e : stuck SHALLOW e → stuck μ e.
+Proof.
+  intros [Hnf Hfinal]. split; [|naive_solver eauto using final_any_shallow].
+  intros [e' Hstep%step_any_shallow]; naive_solver.
+Qed.
+
+Lemma step_final_shallow μ e1 e2 :
+  final SHALLOW e1 → e1 -{μ}-> e2 → final SHALLOW e2.
+Proof.
+  induction 1; intros; inv_step; decompose_Forall;
+    eauto using step, final, no_recs_insert; try done.
+  - by odestruct step_not_final.
+  - apply map_Forall_insert in H0 as [??]; simpl in *; last done.
+    by odestruct step_not_final.
+Qed.
+
+Lemma SAppL_rtc μ e1 e1' e2 :
+  e1 -{SHALLOW}->* e1' → EApp e1 e2 -{μ}->* EApp e1' e2.
+Proof. induction 1; econstructor; eauto with step. Qed.
+Lemma SAppR_rtc μ ms strict e1 e2 e2' :
+  e2 -{SHALLOW}->* e2' →
+  EApp (EAbsMatch ms strict e1) e2 -{μ}->* EApp (EAbsMatch ms strict e1) e2'.
+Proof. induction 1; econstructor; eauto with step. Qed.
+Lemma SSeq_rtc μ μ' e1 e1' e2 :
+  e1 -{μ'}->* e1' → ESeq μ' e1 e2 -{μ}->* ESeq μ' e1' e2.
+Proof. induction 1; econstructor; eauto with step. Qed.
+Lemma SList_rtc es1 e e' es2 :
+  Forall (final DEEP) es1 →
+  e -{DEEP}->* e' →
+  EList (es1 ++ e :: es2) -{DEEP}->* EList (es1 ++ e' :: es2).
+Proof. induction 2; econstructor; eauto with step. Qed.
+Lemma SLetAttr_rtc μ k e1 e1' e2 :
+  e1 -{SHALLOW}->* e1' → ELetAttr k e1 e2 -{μ}->* ELetAttr k e1' e2.
+Proof. induction 1; econstructor; eauto with step. Qed.
+Lemma SBinOpL_rtc μ op e1 e1' e2 :
+  e1 -{SHALLOW}->* e1' → EBinOp op e1 e2 -{μ}->* EBinOp op e1' e2.
+Proof. induction 1; econstructor; eauto with step. Qed.
+Lemma SBinOpR_rtc μ op e1 Φ e2 e2' :
+  final SHALLOW e1 → sem_bin_op op e1 Φ →
+  e2 -{SHALLOW}->* e2' → EBinOp op e1 e2 -{μ}->* EBinOp op e1 e2'.
+Proof. induction 3; econstructor; eauto with step. Qed.
+Lemma SIf_rtc μ e1 e1' e2 e3 :
+  e1 -{SHALLOW}->* e1' → EIf e1 e2 e3 -{μ}->* EIf e1' e2 e3.
+Proof. induction 1; econstructor; eauto with step. Qed.
+
+Lemma SApp_tc μ e1 e1' e2 :
+  e1 -{SHALLOW}->+ e1' → EApp e1 e2 -{μ}->+ EApp e1' e2.
+Proof. induction 1; by econstructor; eauto with step. Qed.
+Lemma SSeq_tc μ μ' e1 e1' e2 :
+  e1 -{μ'}->+ e1' → ESeq μ' e1 e2 -{μ}->+ ESeq μ' e1' e2.
+Proof. induction 1; by econstructor; eauto with step. Qed.
+Lemma SList_tc es1 e e' es2 :
+  Forall (final DEEP) es1 →
+  e -{DEEP}->+ e' →
+  EList (es1 ++ e :: es2) -{DEEP}->+ EList (es1 ++ e' :: es2).
+Proof. induction 2; by econstructor; eauto with step. Qed.
+Lemma SLetAttr_tc μ k e1 e1' e2 :
+  e1 -{SHALLOW}->+ e1' → ELetAttr k e1 e2 -{μ}->+ ELetAttr k e1' e2.
+Proof. induction 1; by econstructor; eauto with step. Qed.
+Lemma SBinOpL_tc μ op e1 e1' e2 :
+  e1 -{SHALLOW}->+ e1' → EBinOp op e1 e2 -{μ}->+ EBinOp op e1' e2.
+Proof. induction 1; by econstructor; eauto with step. Qed.
+Lemma SBinOpR_tc μ op e1 Φ e2 e2' :
+  final SHALLOW e1 → sem_bin_op op e1 Φ →
+  e2 -{SHALLOW}->+ e2' → EBinOp op e1 e2 -{μ}->+ EBinOp op e1 e2'.
+Proof. induction 3; by econstructor; eauto with step. Qed.
+Lemma SIf_tc μ e1 e1' e2 e3 :
+  e1 -{SHALLOW}->+ e1' → EIf e1 e2 e3 -{μ}->+ EIf e1' e2 e3.
+Proof. induction 1; by econstructor; eauto with step. Qed.
+
+Lemma SList_inv es1 e2 :
+  EList es1 -{DEEP}-> e2 ↔ ∃ ds1 ds2 e e',
+    es1 = ds1 ++ e :: ds2 ∧ e2 = EList (ds1 ++ e' :: ds2) ∧
+    Forall (final DEEP) ds1 ∧
+    e -{DEEP}-> e'.
+Proof. split; intros; inv_step; naive_solver eauto using SList. Qed.
+
+Lemma List_nf_cons_final es e :
+  final DEEP e →
+  nf (step DEEP) (EList es) →
+  nf (step DEEP) (EList (e :: es)).
+Proof.
+  intros Hfinal Hnf [e' (ds1 & ds2 & e1 & e2 & ? & -> & Hds1 & Hstep)%SList_inv].
+  destruct Hds1; simplify_eq/=.
+  - by apply step_not_final in Hstep.
+  - naive_solver eauto with step.
+Qed.
+Lemma List_nf_cons es e :
+  ¬final DEEP e →
+  nf (step DEEP) e →
+  nf (step DEEP) (EList (e :: es)).
+Proof.
+  intros Hfinal Hnf [e' (ds1 & ds2 & e1 & e2 & ? & -> & Hds1 & Hstep)%SList_inv].
+  destruct Hds1; naive_solver.
+Qed.
+
+Lemma List_steps_cons es1 es2 e :
+  final DEEP e →
+  EList es1 -{DEEP}->* EList es2 →
+  EList (e :: es1) -{DEEP}->* EList (e :: es2).
+Proof.
+  intros ? Hstep.
+  remember (EList es1) as e1 eqn:He1; remember (EList es2) as e2 eqn:He2.
+  revert es1 es2 He1 He2.
+  induction Hstep as [|e1 e2 e3 Hstep Hstep' IH];
+    intros es1 es3 ??; simplify_eq/=; [done|].
+  inv_step. eapply rtc_l; [apply (SList (_ :: _))|]; naive_solver.
+Qed.
+
+Lemma SAttr_rec_rtc μ αs :
+  EAttr αs -{μ}->*
+    EAttr (AttrN ∘ from_attr (subst (indirects αs)) id <$> αs).
+Proof.
+  destruct (decide (no_recs αs)) as [Hαs|]; [|by eauto using rtc_once, step].
+  eapply reflexive_eq. f_equal. apply map_eq=> x. rewrite lookup_fmap.
+  destruct (αs !! x) as [[τ e]|] eqn:?; [|done].
+  assert (τ = NONREC) as -> by eauto using no_recs_lookup. done.
+Qed.
+
+Lemma SAttr_lookup_rtc αs x e e' :
+  no_recs αs →
+  αs !! x = None →
+  (∀ y α, αs !! y = Some α → final DEEP (attr_expr α) ∨ attr_le x y) →
+  e -{DEEP}->* e' →
+  EAttr (<[x:=AttrN e]> αs) -{DEEP}->* EAttr (<[x:=AttrN e']> αs).
+Proof.
+  intros Hrecs Hx Hfirst He. revert αs Hrecs Hx Hfirst.
+  induction He as [e|e1 e2 e3 He12 He23 IH]; intros eτs Hrec Hx Hfirst; [done|].
+  eapply rtc_l; first by eapply SAttr. apply IH; [done..|].
+  apply step_not_final in He12. naive_solver.
+Qed.
+
+Lemma SAttr_inv αs1 e2 :
+  no_recs αs1 →
+  EAttr αs1 -{DEEP}-> e2 ↔ ∃ αs x e e',
+    αs1 = <[x:=AttrN e]> αs ∧ e2 = EAttr (<[x:=AttrN e']> αs) ∧
+    αs !! x = None ∧
+    (∀ y α, αs !! y = Some α → final DEEP (attr_expr α) ∨ attr_le x y) ∧
+    e -{DEEP}-> e'.
+Proof.
+  split; [intros; inv_step|];
+    naive_solver eauto using SAttr, no_recs_insert_inv.
+Qed.
+
+Lemma Attr_nf_insert_final αs x e :
+  no_recs αs →
+  αs !! x = None →
+  final DEEP e →
+  (∀ y, is_Some (αs !! y) → attr_le x y) →
+  nf (step DEEP) (EAttr αs) →
+  nf (step DEEP) (EAttr (<[x:=AttrN e]> αs)).
+Proof.
+  intros Hrecs Hx Hfinal Hleast Hnf
+    [? (αs'&x'&e'&e''&Hαs&->&Hx'&?&Hstep)%SAttr_inv];
+    last by eauto using no_recs_insert.
+  assert (x ≠ x').
+  { intros ->. apply (f_equal (.!! x')) in Hαs. rewrite !lookup_insert in Hαs.
+    apply step_not_final in Hstep. naive_solver. }
+  destruct Hnf. exists (EAttr (<[x':=AttrN e'']> (delete x αs'))).
+  rewrite -(delete_insert αs x (AttrN e)) // Hαs delete_insert_ne //.
+  refine (SCtx _ _ _ _ _ (CAttr _ _ _ _ _) _);
+    [|by rewrite lookup_delete_ne| |done].
+  - apply (no_recs_insert _ x e) in Hrecs. rewrite Hαs in Hrecs.
+    apply no_recs_insert_inv in Hrecs; last done. by apply map_Forall_delete.
+  - intros ?? ?%lookup_delete_Some; naive_solver.
+Qed.
+Lemma Attr_nf_insert αs x e :
+  no_recs αs →
+  αs !! x = None →
+  ¬final DEEP e →
+  (∀ y, is_Some (αs !! y) → attr_le x y) →
+  nf (step DEEP) e →
+  nf (step DEEP) (EAttr (<[x:=AttrN e]> αs)).
+Proof.
+  intros Hrecs Hx ?? Hnf [? (αs'&x'&e'&e''&Hαs&->&Hx'&Hleast'&Hstep)%SAttr_inv];
+    last eauto using no_recs_insert.
+  assert (x ≠ x') as Hxx'.
+  { intros ->. apply (f_equal (.!! x')) in Hαs. rewrite !lookup_insert in Hαs.
+    naive_solver. }
+  odestruct (Hleast' x (AttrN e)); [|done|].
+  - apply (f_equal (.!! x)) in Hαs.
+    by rewrite lookup_insert lookup_insert_ne in Hαs.
+  - apply (f_equal (.!! x')) in Hαs.
+    rewrite lookup_insert lookup_insert_ne // in Hαs.
+    destruct Hxx'. apply (anti_symm attr_le); naive_solver.
+Qed.
+
+Lemma Attr_step_dom μ αs1 e2 :
+  EAttr αs1 -{μ}-> e2 →
+  ∃ αs2, e2 = EAttr αs2 ∧ ∀ i, αs1 !! i = None ↔ αs2 !! i = None.
+Proof.
+  intros; inv_step; (eexists; split; [done|]).
+  - intros i. by rewrite lookup_fmap fmap_None.
+  - intros i. rewrite !lookup_insert_None; naive_solver.
+Qed.
+Lemma Attr_steps_dom μ αs1 αs2 :
+  EAttr αs1 -{μ}->* EAttr αs2 → ∀ i, αs1 !! i = None ↔ αs2 !! i = None.
+Proof.
+  intros Hstep.
+  remember (EAttr αs1) as e1 eqn:He1; remember (EAttr αs2) as e2 eqn:He2.
+  revert αs1 αs2 He1 He2. induction Hstep as [|e1 e2 e3 Hstep Hstep' IH];
+    intros αs1 αs3 ??; simplify_eq/=; [done|].
+  apply Attr_step_dom in Hstep; naive_solver.
+Qed.
+
+Lemma Attr_step_recs αs1 αs2 :
+  EAttr αs1 -{DEEP}-> EAttr αs2 → no_recs αs1 → no_recs αs2.
+Proof. intros. inv_step; by eauto using no_recs_insert. Qed.
+Lemma Attr_steps_recs αs1 αs2 :
+  EAttr αs1 -{DEEP}->* EAttr αs2 → no_recs αs1 → no_recs αs2.
+Proof.
+  intros Hstep.
+  remember (EAttr αs1) as e1 eqn:He1; remember (EAttr αs2) as e2 eqn:He2.
+  revert αs1 αs2 He1 He2. induction Hstep as [|e1 e2 e3 Hstep Hstep' IH];
+    intros αs1 αs3 ???; simplify_eq/=; [done|].
+  pose proof (Attr_step_dom _ _ _ Hstep) as (es2 & -> & ?).
+  apply Attr_step_recs in Hstep; naive_solver.
+Qed.
+
+Lemma Attr_step_insert αs1 αs2 x e :
+  no_recs αs1 →
+  αs1 !! x = None →
+  final DEEP e →
+  EAttr αs1 -{DEEP}-> EAttr αs2 →
+  EAttr (<[x:=AttrN e]> αs1) -{DEEP}-> EAttr (<[x:=AttrN e]> αs2).
+Proof.
+  intros Hrecs Hx ?
+    (αs' & x' & e1 & e1' & ? & ? & ? & ? & ?)%SAttr_inv; [|done]; simplify_eq.
+  apply lookup_insert_None in Hx as [??]. rewrite !(insert_commute _ x) //.
+  eapply SAttr; [|by rewrite lookup_insert_ne| |done].
+  - by eapply no_recs_insert, no_recs_insert_inv.
+  - intros y e' ?%lookup_insert_Some; naive_solver.
+Qed.
+Lemma Attr_steps_insert αs1 αs2 x e :
+  no_recs αs1 →
+  αs1 !! x = None →
+  final DEEP e →
+  EAttr αs1 -{DEEP}->* EAttr αs2 →
+  EAttr (<[x:=AttrN e]> αs1) -{DEEP}->* EAttr (<[x:=AttrN e]> αs2).
+Proof.
+  intros Hrecs Hx ? Hstep.
+  remember (EAttr αs1) as e1 eqn:He1; remember (EAttr αs2) as e2 eqn:He2.
+  revert αs1 αs2 Hx Hrecs He1 He2.
+  induction Hstep as [|e1 e2 e3 Hstep Hstep' IH];
+    intros αs1 αs3 ????; simplify_eq/=; [done|].
+  pose proof (Attr_step_dom _ _ _ Hstep) as (αs2 & -> & Hdom).
+  eapply rtc_l; first by eapply Attr_step_insert.
+  eapply IH; naive_solver eauto using Attr_step_recs.
+Qed.
+
+Reserved Infix "=D=>" (right associativity, at level 55).
+
+Inductive step_delayed : relation expr :=
+  | RDrefl e :
+      e =D=> e
+  | RDId x e1 e2 :
+      e1 =D=> e2 →
+      EId x (Some (ABS, e1)) =D=> e2
+  | RDBinOp op e1 e1' e2 e2' :
+      e1 =D=> e1' → e2 =D=> e2' → EBinOp op e1 e2 =D=> EBinOp op e1' e2'
+  | RDIf e1 e1' e2 e2' e3 e3' :
+      e1 =D=> e1' → e2 =D=> e2' → e3 =D=> e3' → EIf e1 e2 e3 =D=> EIf e1' e2' e3'
+where "e1 =D=> e2" := (step_delayed e1 e2).
+
+Global Instance step_delayed_po : PreOrder step_delayed.
+Proof.
+  split; [constructor|].
+  intros e1 e2 e3 Hstep. revert e3.
+  induction Hstep; inv 1; eauto using step_delayed.
+Qed.
+Hint Extern 0 (_ =D=> _) => reflexivity : core.
+
+Lemma delayed_final_l e1 e2 :
+  final SHALLOW e1 →
+  e1 =D=> e2 →
+  e1 = e2.
+Proof. intros Hfinal. induction 1; try by inv Hfinal. Qed.
+
+Lemma delayed_final_r μ e1 e2 :
+  final μ e2 →
+  e1 =D=> e2 →
+  e1 -{μ}->* e2.
+Proof.
+  intros Hfinal. induction 1; try by inv Hfinal.
+  eapply rtc_l; [constructor|]. eauto.
+Qed.
+
+Lemma delayed_step_l μ e1 e1' e2 :
+  e1 =D=> e1' →
+  e1 -{μ}-> e2 →
+  ∃ e2', e1' -{μ}->* e2' ∧ e2 =D=> e2'.
+Proof.
+  intros Hrem. revert μ e2.
+  induction Hrem; intros μ ? Hstep.
+  - eauto using rtc_once.
+  - inv_step. by exists e2.
+  - inv_step.
+    + eapply delayed_final_l in Hrem1 as ->, Hrem2 as ->; [|by eauto..].
+      eexists; split; [|done]. eapply rtc_once. by econstructor.
+    + apply IHHrem1 in H2 as (e1'' & ? & ?).
+      eexists; split; [by eapply SBinOpL_rtc|]. by constructor.
+    + eapply delayed_final_l in Hrem1 as ->; [|by eauto..].
+      apply IHHrem2 in H2 as (e2'' & ? & ?).
+      eexists (EBinOp _ e1' e2''); split; [|by constructor].
+      by eapply SBinOpR_rtc.
+  - inv_step.
+    + eapply delayed_final_l in Hrem1 as <-; [|by repeat constructor].
+      eexists; split; [eapply rtc_once; constructor|]. by destruct b.
+    + apply IHHrem1 in H2 as (e1'' & ? & ?).
+      eexists; split; [by eapply SIf_rtc|]. by constructor.
+Qed.
+
+Lemma delayed_steps_l μ e1 e1' e2 :
+  e1 =D=> e1' →
+  e1 -{μ}->* e2 →
+  ∃ e2', e1' -{μ}->* e2' ∧ e2 =D=> e2'.
+Proof.
+  intros Hdel Hsteps. revert e1' Hdel.
+  induction Hsteps as [e|e1 e2 e3 Hstep Hsteps IH]; intros e1' Hdel.
+  { eexists; by split. }
+  eapply delayed_step_l in Hstep as (e2' & Hstep2 & Hdel2); [|done].
+  apply IH in Hdel2 as (e3' & ? & ?). eexists; by split; [etrans|].
+Qed.
+
+Lemma delayed_step_r μ e1 e1' e2 :
+  e1' =D=> e1 →
+  e1 -{μ}-> e2 →
+  ∃ e2', e1' -{μ}->+ e2' ∧ e2' =D=> e2.
+Proof.
+  intros Hrem. revert μ e2.
+  induction Hrem; intros μ ? Hstep.
+  - eauto using tc_once.
+  - apply IHHrem in Hstep as (e1' & ? & ?).
+    eexists. split; [|done]. eapply tc_l; [econstructor|done].
+  - inv_step.
+    + exists e0; split; [|done].
+      eapply tc_rtc_l; [by eapply SBinOpL_rtc, delayed_final_r, Hrem1|].
+      eapply tc_rtc_l; [by eapply SBinOpR_rtc, delayed_final_r, Hrem2|].
+      eapply tc_once. by econstructor.
+    + apply IHHrem1 in H2 as (e1'' & ? & ?).
+      eexists; split; [by eapply SBinOpL_tc|]. by constructor.
+    + apply IHHrem2 in H2 as (e2'' & ? & ?).
+      eexists (EBinOp _ e1' e2''); split; [|by apply RDBinOp].
+      eapply tc_rtc_l; [by eapply SBinOpL_rtc, delayed_final_r, Hrem1|].
+      by eapply SBinOpR_tc.
+  - inv_step.
+    + exists (if b then e2 else e3). split; [|by destruct b].
+      eapply tc_rtc_l;
+        [eapply SIf_rtc, delayed_final_r, Hrem1; by repeat constructor|].
+      eapply tc_once; constructor.
+    + apply IHHrem1 in H2 as (e1'' & ? & ?).
+      eexists; split; [by eapply SIf_tc|]. by constructor.
+Qed.
+
+Lemma delayed_steps_r μ e1 e1' e2 :
+  e1' =D=> e1 →
+  e1 -{μ}->* e2 →
+  ∃ e2', e1' -{μ}->* e2' ∧ e2' =D=> e2.
+Proof.
+  intros Hdel Hsteps. revert e1' Hdel.
+  induction Hsteps as [e|e1 e2 e3 Hstep Hsteps IH]; intros e1' Hdel.
+  { eexists; by split. }
+  eapply delayed_step_r in Hstep as (e2' & Hstep2%tc_rtc & Hdel2); [|done].
+  apply IH in Hdel2 as (e3' & ? & ?). eexists; by split; [etrans|].
+Qed.
+
+(** Determinism *)
+
+Lemma bin_op_det op e Φ Ψ :
+  sem_bin_op op e Φ →
+  sem_bin_op op e Ψ →
+  Φ = Ψ.
+Proof. by destruct 1; inv 1. Qed.
+
+Lemma bin_op_rel_det op e1 Φ e2 d1 d2 :
+  sem_bin_op op e1 Φ →
+  Φ e2 d1 →
+  Φ e2 d2 →
+  d1 = d2.
+Proof.
+  assert (AntiSymm eq attr_le) by apply _.
+  unfold AntiSymm in *. inv 1; repeat case_match; naive_solver.
+Qed.
+
+Lemma matches_present x e md es ms strict βs :
+  es !! x = Some e → ms !! x = Some md →
+  matches es ms strict βs →
+  βs !! x = Some (AttrN e).
+Proof.
+  intros Hes Hms. induction 1; try done.
+  - by apply lookup_insert_Some in Hes as [[]|[]]; simplify_map_eq.
+  - by simplify_map_eq.
+Qed.
+
+Lemma matches_default x es ms d strict βs :
+  es !! x = None →
+  ms !! x = Some (Some d) →
+  matches es ms strict βs →
+  βs !! x = Some (AttrR d).
+Proof.
+  intros Hes Hms. induction 1; try done.
+  - by apply lookup_insert_None in Hes as []; simplify_map_eq.
+  - by apply lookup_insert_Some in Hms as [[]|[]]; simplify_map_eq.
+Qed.
+
+Lemma matches_weaken x es ms strict βs :
+  matches es ms strict βs →
+  matches (delete x es) (delete x ms) strict (delete x βs).
+Proof.
+  induction 1; [constructor|constructor|..]; rename x0 into y;
+    (destruct (decide (x = y)) as [->|Hxy];
+      [ rewrite !delete_insert_delete //
+      | rewrite !delete_insert_ne //; constructor;
+        by simplify_map_eq ]).
+Qed.
+
+Lemma matches_det es ms strict βs1 βs2 :
+  matches es ms strict βs1 →
+  matches es ms strict βs2 →
+  βs1 = βs2.
+Proof.
+  intros Hβs1. revert βs2. induction Hβs1; intros βs2 Hβs2;
+    try (inv Hβs2; done || (by exfalso; eapply (insert_non_empty (M:=stringmap)))).
+  - eapply (matches_weaken x) in Hβs2 as Hβs2'.
+    rewrite !delete_insert // in Hβs2'.
+    rewrite (IHHβs1 _ Hβs2') insert_delete //.
+    eapply matches_present; eauto; apply lookup_insert.
+  - eapply (matches_weaken x) in Hβs2 as Hβs2'.
+    rewrite delete_notin // delete_insert // in Hβs2'.
+    rewrite (IHHβs1 _ Hβs2') insert_delete //.
+    eapply matches_default; eauto. apply lookup_insert.
+Qed.
+
+Lemma ctx_det K1 K2 e1 e2 μ μ1' μ2' :
+  K1 e1 = K2 e2 →
+  ctx1 μ1' μ K1 →
+  ctx1 μ2' μ K2 →
+  red (step μ1') e1 →
+  red (step μ2') e2 →
+  K1 = K2 ∧ e1 = e2 ∧ μ1' = μ2'.
+Proof.
+  intros Hes HK1 HK2 Hred1 Hred2.
+  induction HK1; inv HK2; try done.
+  - apply not_elem_of_app_cons_inv_l in Hes as [<- [<- <-]]; first done.
+    + intros He1. apply (proj1 (Forall_forall _ _) H0) in He1.
+      inv Hred1. by apply step_not_final in H1.
+    + intros He2. apply (proj1 (Forall_forall _ _) H) in He2.
+      inv Hred2. by apply step_not_final in H1.
+  - destruct (decide (x = x0)) as [<-|].
+    { by apply map_insert_inv_eq in Hes as [[= ->] [= ->]]. }
+    apply map_insert_inv_ne in Hes as (Hx0 & Hx & Hαs); try done.
+    apply H1 in Hx0 as [contra | Hxlex0].
+    + inv Hred2. by apply step_not_final in H5.
+    + apply H4 in Hx as [contra | Hx0lex].
+      * inv Hred1. by apply step_not_final in H5.
+      * assert (Hasym : AntiSymm eq attr_le) by apply _.
+        by pose proof (Hasym _ _ Hxlex0 Hx0lex).
+  - inv Hred1. inv_step.
+  - inv Hred2. inv_step.
+  - inv Hred1. by apply step_not_final in H1.
+  - inv Hred2. by apply step_not_final in H1.
+Qed.
+
+Lemma step_det μ e d1 d2 :
+  e -{μ}-> d1 →
+  e -{μ}-> d2 →
+  d1 = d2.
+Proof.
+  intros Hred1. revert d2.
+  induction Hred1; intros d2 Hred2; inv Hred2; try by inv_step.
+  - by apply (matches_det _ _ _ _ _ H0) in H8 as <-.
+  - inv_step. by apply step_not_final in H3.
+  - inv_step. destruct H. by apply no_recs_insert.
+  - assert (Φ = Φ0) as <- by (by eapply bin_op_det).
+    by eapply bin_op_rel_det.
+  - inv_step; by apply step_not_final in H6.
+  - inv_step. by apply step_not_final in Hred1.
+  - inv_step. destruct H2. by apply no_recs_insert.
+  - inv_step; by apply step_not_final in Hred1.
+  - eapply ctx_det in H0 as (?&?&?); [|by eauto..]; naive_solver.
+Qed.