5 files changed, 703 insertions, 0 deletions

diff --git a/theories/dynlang/equiv.v b/theories/dynlang/equiv.v
new file mode 100644
index 0000000..aa0b7f3
--- /dev/null
+++ b/theories/dynlang/equiv.v
@@ -0,0 +1,154 @@
+From mininix Require Export lambda.interp_proofs dynlang.interp_proofs.
+From stdpp Require Import options.
+
+Class Lift A B := lift : A → B.
+Global Hint Mode Lift ! - : typeclass_instances.
+Arguments lift {_ _ _} !_ /.
+Notation "⌜ x ⌝" := (lift x) (at level 0).
+Notation "⌜* x ⌝" := (fmap lift x) (at level 0).
+
+Module lambda.
+  Global Instance lambda_expr_lift : Lift lambda.expr dynlang.expr :=
+    fix go e := let _ : Lift _ _ := go in
+    match e with
+    | lambda.EString s => dynlang.EString s
+    | lambda.EId x => dynlang.EId ∅ (dynlang.EString x)
+    | lambda.EAbs x e => dynlang.EAbs (dynlang.EString x) ⌜e⌝
+    | lambda.EApp e1 e2 => dynlang.EApp ⌜e1⌝ ⌜e2⌝
+    end.
+
+  Global Instance lambda_thunk_lift : Lift lambda.thunk dynlang.thunk :=
+    fix go t := let _ : Lift _ _ := go in
+    dynlang.Thunk ⌜*lambda.thunk_env t⌝ ⌜lambda.thunk_expr t⌝.
+
+  Global Instance lambda_val_lift : Lift lambda.val dynlang.val := λ v,
+    match v with
+    | lambda.VString s => dynlang.VString s
+    | lambda.VClo x E e => dynlang.VClo x ⌜*E⌝ ⌜e⌝
+    end.
+End lambda.
+
+Lemma interp_open_lambda_dynlang E e mv n :
+  lambda.closed_env E → lambda.closed (dom E) e →
+  lambda.interp n E e = Res mv →
+  ∃ m, dynlang.interp m ⌜*E⌝ ⌜e⌝ = Res ⌜*mv⌝.
+Proof.
+  revert E e mv. induction n as [|n IH]; [done|]; intros E e mv HE He Hinterp.
+  rewrite lambda.interp_S in Hinterp. destruct e as [s|z|ex e|e1 e2]; simplify_res.
+  - (* EString *) by exists 1.
+  - (* EId *)
+    apply elem_of_dom in He as [[Et et] Hz]. rewrite Hz /= in Hinterp.
+    apply lambda.closed_env_lookup in Hz as He; last done.
+    rewrite lambda.closed_thunk_eq/= in He. destruct He as [HEtclosed Hetclosed].
+    apply IH in Hinterp as [m Hinterp]; [|done..].
+    exists (S (S m)). rewrite !dynlang.interp_S /= -dynlang.interp_S.
+    rewrite lookup_empty /= right_id_L lookup_fmap Hz /=.
+    eauto using dynlang.interp_le with lia.
+  - (* EAbs *) by exists 2.
+  - (* EApp *)
+    destruct He as [He1 He2].
+    destruct (lambda.interp _ _ e1) as [mw|] eqn:Hinterp1; simplify_res.
+    pose proof Hinterp1 as Hinterp1'.
+    apply lambda.interp_closed in Hinterp1' as Hmw; [|done..].
+    eapply IH in Hinterp1 as [m1 Hinterp1]; [|done..].
+    destruct mw as [w|]; simplify_res; last first.
+    { exists (S m1). by rewrite dynlang.interp_S /= Hinterp1. }
+    destruct (maybe3 lambda.VClo w) eqn:?; simplify_res; last first.
+    { exists (S m1). rewrite dynlang.interp_S /= Hinterp1 /=. by destruct w. }
+    destruct w; simplify_res.
+    apply IH in Hinterp as [m2 Hinterp2].
+    + exists (S (m1 + m2)). rewrite dynlang.interp_S /=.
+      rewrite (dynlang.interp_le Hinterp1) /=; last lia.
+      rewrite fmap_insert /= in Hinterp2.
+      rewrite (dynlang.interp_le Hinterp2) /=; last lia. done.
+    + apply lambda.closed_env_insert; [by split|naive_solver].
+    + rewrite dom_insert_L. set_solver.
+Qed.
+Lemma interp_lambda_dynlang e mv n :
+  lambda.closed ∅ e →
+  lambda.interp n ∅ e = Res mv →
+  ∃ m, dynlang.interp m ∅ ⌜e⌝ = Res ⌜*mv⌝.
+Proof. intro. by apply interp_open_lambda_dynlang. Qed.
+
+Lemma interp_open_dynlang_lambda E e mv n :
+  lambda.closed_env E → lambda.closed (dom E) e →
+  dynlang.interp n ⌜*E⌝ ⌜e⌝ = Res mv →
+  ∃ mw, lambda.interp n E e = Res mw ∧ mv = ⌜*mw⌝.
+Proof.
+  revert E e mv. induction n as [|n IH]; [done|]; intros E e mv HE He Hinterp.
+  rewrite dynlang.interp_S in Hinterp. destruct e as [s|z|ex e|e1 e2]; simplify_res.
+  - (* EString *) rewrite lambda.interp_S /=. by eexists.
+  - (* EId *)
+    destruct n as [|n]; [done|].
+    rewrite dynlang.interp_S /= -dynlang.interp_S in Hinterp.
+    apply elem_of_dom in He as [[Et et] Hz].
+    pose proof (f_equal (fmap lift) Hz) as Hz'.
+    rewrite -lookup_fmap /= in Hz'. rewrite Hz' lookup_empty /= {Hz'} in Hinterp.
+    pose proof Hz as Hz'.
+    apply lambda.closed_env_lookup in Hz' as [HEt Het]; simpl in *; last done.
+    apply IH in Hinterp as (mw & Hinterp & ->); [|done..].
+    exists mw. rewrite lambda.interp_S /= Hz /=. done.
+  - (* EAbs *)
+    destruct n as [|n]; [done|].
+    rewrite dynlang.interp_S /= in Hinterp; simplify_res.
+    rewrite lambda.interp_S /=. by eexists.
+  - (* EApp *)
+    destruct He as [He1 He2].
+    destruct (dynlang.interp _ _ _) as [mw1|] eqn:Hinterp1; simplify_res.
+    eapply IH in Hinterp1 as (mv1 & Hinterp1 & ->); [|done..].
+    destruct mv1 as [v1|]; simplify_res; last first.
+    { exists None. by rewrite lambda.interp_S /= Hinterp1. }
+    destruct (maybe3 dynlang.VClo _) eqn:?; simplify_res; last first.
+    { exists None. rewrite lambda.interp_S /= Hinterp1 /=. by destruct v1. }
+    destruct v1; simplify_res.
+    change (dynlang.Thunk ⌜*E⌝ ⌜e2⌝) with ⌜lambda.Thunk E e2⌝ in Hinterp.
+    rewrite -fmap_insert in Hinterp.
+    apply lambda.interp_closed in Hinterp1 as Hmw; [|done..].
+    apply IH in Hinterp as (mv2 & Hinterp2 & ->).
+    + exists mv2. rewrite lambda.interp_S /= Hinterp1 /=. done.
+    + apply lambda.closed_env_insert; [by split|]. naive_solver.
+    + rewrite dom_insert_L. set_solver.
+Qed.
+Lemma interp_dynlang_lambda e mv n :
+  lambda.closed ∅ e →
+  dynlang.interp n ∅ ⌜e⌝ = Res mv →
+  ∃ mw, lambda.interp n ∅ e = Res mw ∧ mv = ⌜*mw⌝.
+Proof. intros. by apply interp_open_dynlang_lambda. Qed.
+
+(* The following equivalences about the semantics trivially follow: *)
+
+Theorem interp_equiv_ret_string e s :
+  lambda.closed ∅ e →
+  rtc lambda.step e (lambda.EString s)
+  ↔ rtc dynlang.step ⌜e⌝ (dynlang.EString s).
+Proof.
+  intros. rewrite -lambda.interp_sound_complete_ret_string //.
+  rewrite -dynlang.interp_sound_complete_ret_string. split; intros [n Hinterp].
+  + by apply interp_lambda_dynlang in Hinterp.
+  + apply interp_dynlang_lambda in Hinterp as ([[]|] & ?); naive_solver.
+Qed.
+
+Theorem interp_equiv_fail e :
+  lambda.closed ∅ e →
+  (∃ e', rtc lambda.step e e' ∧ lambda.stuck e')
+  ↔ (∃ e', rtc dynlang.step ⌜e⌝ e' ∧ dynlang.stuck e').
+Proof.
+  intros. rewrite -lambda.interp_sound_complete_fail //.
+  rewrite -dynlang.interp_sound_complete_fail. split; intros [n Hinterp].
+  + by apply interp_lambda_dynlang in Hinterp.
+  + apply interp_dynlang_lambda in Hinterp as ([] & ?); naive_solver.
+Qed.
+
+Theorem interp_equiv_no_fuel e :
+  lambda.closed ∅ e →
+  all_loop lambda.step e ↔ all_loop dynlang.step ⌜e⌝.
+Proof.
+  intros He. rewrite -lambda.interp_sound_complete_no_fuel; last done.
+  rewrite -dynlang.interp_sound_complete_no_fuel. split; intros Hnofuel n.
+  - destruct (dynlang.interp n ∅ _) as [mv|] eqn:Hinterp; [|done].
+    apply interp_dynlang_lambda in Hinterp as (? & Hinterp & _); [|done].
+    by rewrite Hnofuel in Hinterp.
+  - destruct (lambda.interp n ∅ _) as [mv|] eqn:Hinterp; [|done].
+    apply interp_lambda_dynlang in Hinterp as [m Hinterp]; [|done..].
+    by rewrite Hnofuel in Hinterp.
+Qed.
diff --git a/theories/dynlang/interp.v b/theories/dynlang/interp.v
new file mode 100644
index 0000000..dcf6b95
--- /dev/null
+++ b/theories/dynlang/interp.v
@@ -0,0 +1,49 @@
+From mininix Require Export res dynlang.operational_props.
+From stdpp Require Import options.
+
+Module Import dynlang.
+Export dynlang.
+
+Inductive thunk := Thunk { thunk_env : gmap string thunk; thunk_expr : expr }.
+Add Printing Constructor thunk.
+Notation env := (gmap string thunk).
+
+Inductive val :=
+  | VString (s : string)
+  | VClo (x : string) (E : env) (e : expr).
+
+Global Instance maybe_VString : Maybe VString := λ v,
+  if v is VString s then Some s else None.
+Global Instance maybe_VClo : Maybe3 VClo := λ v,
+  if v is VClo x E e then Some (x, E, e) else None.
+
+Definition interp1 (interp : env → expr → res val) (E : env) (e : expr) : res val :=
+  match e with
+  | EString s =>
+      mret (VString s)
+  | EId ds e =>
+      v ← interp E e;
+      x ← Res $ maybe VString v;
+      t ← Res $ (E !! x) ∪ (Thunk ∅ <$> ds !! x);
+      interp (thunk_env t) (thunk_expr t)
+  | EAbs ex e =>
+      v ← interp E ex;
+      x ← Res $ maybe VString v;
+      mret (VClo x E e)
+  | EApp e1 e2 =>
+      v1 ← interp E e1;
+      '(x, E', e') ← Res (maybe3 VClo v1);
+      interp (<[x:=Thunk E e2]> E') e'
+  end.
+
+Fixpoint interp (n : nat) (E : env) (e : expr) : res val :=
+  match n with
+  | O => NoFuel
+  | S n => interp1 (interp n) E e
+  end.
+
+Global Opaque interp.
+
+End dynlang.
+
+Add Printing Constructor dynlang.thunk.
diff --git a/theories/dynlang/interp_proofs.v b/theories/dynlang/interp_proofs.v
new file mode 100644
index 0000000..f18a91c
--- /dev/null
+++ b/theories/dynlang/interp_proofs.v
@@ -0,0 +1,426 @@
+From mininix Require Export dynlang.interp.
+From stdpp Require Import options.
+
+Module Import dynlang.
+Export dynlang.
+
+Lemma interp_S n : interp (S n) = interp1 (interp n).
+Proof. done. Qed.
+
+Fixpoint thunk_size (t : thunk) : nat :=
+  S (map_sum_with thunk_size (thunk_env t)).
+Definition env_size (E : env) : nat :=
+  map_sum_with thunk_size E.
+
+Lemma env_ind (P : env → Prop) :
+  (∀ E, map_Forall (λ i, P ∘ thunk_env) E → P E) →
+  ∀ E : env, P E.
+Proof.
+  intros Pbs E.
+  induction (Nat.lt_wf_0_projected env_size E) as [E _ IH].
+  apply Pbs, map_Forall_lookup=> y [E' e'] Hy.
+  apply (map_sum_with_lookup_le thunk_size) in Hy.
+  apply IH. by rewrite -Nat.le_succ_l.
+Qed.
+
+(** Correspondence to operational semantics *)
+Definition subst_env' (thunk_to_expr : thunk → expr) (E : env) : expr → expr :=
+  subst (thunk_to_expr <$> E).
+Fixpoint thunk_to_expr (t : thunk) : expr :=
+  subst_env' thunk_to_expr (thunk_env t) (thunk_expr t).
+Notation subst_env := (subst_env' thunk_to_expr).
+
+Lemma subst_env_eq e E :
+  subst_env E e =
+    match e with
+    | EString s => EString s
+    | EId ds e => EId ((thunk_to_expr <$> E) ∪ ds) (subst_env E e)
+    | EAbs ex e => EAbs (subst_env E ex) (subst_env E e)
+    | EApp e1 e2 => EApp (subst_env E e1) (subst_env E e2)
+    end.
+Proof. by destruct e. Qed.
+
+Lemma subst_env_alt E e : subst_env E e = subst (thunk_to_expr <$> E) e.
+Proof. done. Qed.
+
+(* Use the unfolding lemmas, don't rely on conversion *)
+Opaque subst_env'.
+
+Definition val_to_expr (v : val) : expr :=
+  match v with
+  | VString s => EString s
+  | VClo x E e => EAbs (EString x) (subst_env E e)
+  end.
+
+Lemma val_final v : final (val_to_expr v).
+Proof. by destruct v. Qed.
+
+Lemma subst_empty e : subst ∅ e = e.
+Proof. induction e; f_equal/=; auto. by rewrite left_id_L. Qed.
+
+Lemma subst_env_empty e : subst_env ∅ e = e.
+Proof. rewrite subst_env_alt. apply subst_empty. Qed.
+
+Lemma interp_le {n1 n2 E e mv} :
+  interp n1 E e = Res mv → n1 ≤ n2 → interp n2 E e = Res mv.
+Proof.
+  revert n2 E e mv.
+  induction n1 as [|n1 IH]; intros [|n2] E e mv He ?; [by (done || lia)..|].
+  rewrite interp_S in He; rewrite interp_S; destruct e;
+    repeat match goal with
+    | _ => case_match
+    | H : context [(_ <$> ?mx)] |- _ => destruct mx eqn:?; simplify_res
+    | H : ?r ≫= _ = _ |- _ => destruct r as [[]|] eqn:?; simplify_res
+    | H : _ <$> ?r = _ |- _ => destruct r as [[]|] eqn:?; simplify_res
+    | |- interp ?n ?E ?e ≫= _ = _ => erewrite (IH n E e) by (done || lia)
+    | _ => progress simplify_res
+    | _ => progress simplify_option_eq
+    end; eauto with lia.
+Qed.
+
+Lemma interp_agree {n1 n2 E e mv1 mv2} :
+  interp n1 E e = Res mv1 → interp n2 E e = Res mv2 → mv1 = mv2.
+Proof.
+  intros He1 He2. apply (inj Res). destruct (total (≤) n1 n2).
+  - rewrite -He2. symmetry. eauto using interp_le. 
+  - rewrite -He1. eauto using interp_le.
+Qed.
+
+Lemma subst_env_union E1 E2 e :
+  subst_env (E1 ∪ E2) e = subst_env E1 (subst_env E2 e).
+Proof.
+  revert E1 E2. induction e; intros E1 E2; rewrite subst_env_eq /=.
+  - done.
+  - rewrite !(subst_env_eq (EId _ _)) IHe. f_equal.
+    by rewrite assoc_L map_fmap_union.
+  - rewrite !(subst_env_eq (EAbs _ _)) /=. f_equal; auto.
+  - rewrite !(subst_env_eq (EApp _ _)) /=. f_equal; auto.
+Qed.
+
+Lemma subst_env_insert E x e t :
+  subst_env (<[x:=t]> E) e = subst {[x:=thunk_to_expr t]} (subst_env E e).
+Proof.
+  rewrite insert_union_singleton_l subst_env_union subst_env_alt.
+  by rewrite map_fmap_singleton.
+Qed.
+
+Lemma subst_env_insert_eq e1 e2 E1 E2 x E1' E2' e1' e2' :
+  subst_env E1 e1 = subst_env E2 e2 →
+  subst_env E1' e1' = subst_env E2' e2' →
+  subst_env (<[x:=Thunk E1' e1']> E1) e1 = subst_env (<[x:=Thunk E2' e2']> E2) e2.
+Proof. intros He He'. by rewrite !subst_env_insert //= He' He. Qed.
+
+Lemma interp_proper n E1 E2 e1 e2 mv :
+  subst_env E1 e1 = subst_env E2 e2 →
+  interp n E1 e1 = Res mv →
+  ∃ mw m, interp m E2 e2 = Res mw ∧
+          val_to_expr <$> mv = val_to_expr <$> mw.
+Proof.
+  revert n E1 E2 e1 e2 mv. induction n as [|n IHn]; [done|].
+  intros E1 E2 e1 e2 mv Hsubst Hinterp.
+  rewrite 2!subst_env_eq in Hsubst.
+  rewrite interp_S in Hinterp. destruct e1, e2; simplify_res; try done.
+  - eexists (Some (VString _)), 1. by rewrite interp_S.
+  - destruct (interp n _ e1) as [mv1|] eqn:Hinterp'; simplify_eq/=.
+    eapply IHn in Hinterp' as (mw1 & m1 & Hinterp1 & ?); last done.
+    destruct mv1 as [v1|], mw1 as [w1|]; simplify_res; last first.
+    { exists None, (S m1). by rewrite interp_S /= Hinterp1. }
+    destruct (maybe VString v1) as [x|] eqn:Hv1;
+      simplify_res; last first.
+    { exists None, (S m1). split; [|done]. rewrite interp_S /= Hinterp1 /=.
+      destruct v1, w1; repeat destruct select base_lit; by simplify_eq/=. }
+    destruct v1, w1; repeat destruct select base_lit; simplify_eq/=.
+    assert (∀ (ds : stringmap expr) (E : env) x,
+      thunk_to_expr <$> (E !! x) ∪ (Thunk ∅ <$> ds !! x)
+      = ((thunk_to_expr <$> E) ∪ ds) !! x) as HE.
+    { intros ds' E x. rewrite lookup_union lookup_fmap.
+      repeat destruct (_ !! _); f_equal/=; by rewrite subst_env_empty. }
+    pose proof (f_equal (.!! s0) Hsubst) as Hs. rewrite -!HE {HE} in Hs.
+    destruct (E1 !! s0 ∪ _) as [[E1' e1']|],
+      (E2 !! s0 ∪ _) as [[E2' e2']|] eqn:HE2; simplify_res; last first.
+    { exists None, (S m1). rewrite interp_S /= Hinterp1 /=. by rewrite HE2. }
+    eapply IHn in Hinterp as (mw & m2 & Hinterp2 & ?); [|by eauto..].
+    exists mw, (S (m1 `max` m2)). split; [|done]. rewrite interp_S /=.
+    rewrite (interp_le Hinterp1) /=; last lia. rewrite HE2 /=.
+    eauto using interp_le with lia.
+  - destruct (interp n _ _) as [mv1|] eqn:Hinterp'; simplify_eq/=.
+    eapply IHn in Hinterp' as (mw1 & m1 & Hinterp1 & ?); last done.
+    destruct mv1 as [v1|], mw1 as [w1|]; simplify_res; last first.
+    { exists None, (S m1). by rewrite interp_S /= Hinterp1. }
+    destruct (maybe VString _) eqn:Hstring; simplify_res; last first.
+    { exists None, (S m1). rewrite interp_S /= Hinterp1 /=.
+      by assert (maybe VString w1 = None) as -> by (by destruct v1, w1). }
+    destruct v1, w1; simplify_eq/=.
+    eexists (Some (VClo _ _ _)), (S m1).
+    rewrite interp_S /= Hinterp1 /=. split; [done|]. by do 2 f_equal/=.
+  - destruct (interp n _ _) as [mv'|] eqn:Hinterp'; simplify_res.
+    eapply IHn in Hinterp' as (mw' & m1 & Hinterp1 & ?); last done.
+    destruct mv' as [v'|], mw' as [w'|]; simplify_res; last first.
+    { exists None, (S m1). by rewrite interp_S /= Hinterp1. }
+    destruct (maybe3 VClo _) eqn:Hclo; simplify_res; last first.
+    { exists None, (S m1). rewrite interp_S /= Hinterp1 /=.
+      by assert (maybe3 VClo w' = None) as -> by (by destruct v', w'). }
+    destruct v', w'; simplify_eq/=.
+    eapply IHn with (E2 := <[x0:=Thunk E2 e2_2]> E0) in Hinterp
+      as (w & m2 & Hinterp2 & ?); last by apply subst_env_insert_eq.
+    exists w, (S (m1 `max` m2)). rewrite interp_S /=.
+    rewrite (interp_le Hinterp1) /=; last lia.
+    rewrite (interp_le Hinterp2) /=; last lia. done.
+Qed.
+
+Lemma subst_as_subst_env x e1 e2 :
+  subst {[x:=e2]} e1 = subst_env (<[x:=Thunk ∅ e2]> ∅) e1.
+Proof. rewrite subst_env_insert //= !subst_env_empty //. Qed.
+
+Lemma interp_subst n x e1 e2 mv :
+  interp n ∅ (subst {[x:=e2]} e1) = Res mv →
+  ∃ mw m, interp m (<[x:=Thunk ∅ e2]> ∅) e1 = Res mw ∧
+          val_to_expr <$> mv = val_to_expr <$> mw.
+Proof.
+  apply interp_proper.
+  by rewrite subst_env_empty subst_as_subst_env.
+Qed.
+
+Lemma interp_step e1 e2 n mv :
+  e1 --> e2 →
+  interp n ∅ e2 = Res mv →
+  ∃ mw m, interp m ∅ e1 = Res mw ∧ val_to_expr <$> mv = val_to_expr <$> mw.
+Proof.
+  intros Hstep. revert mv n.
+  induction Hstep; intros mv n Hinterp.
+  - apply interp_subst in Hinterp as (w & [|m] & Hinterp & Hv);
+      simplify_eq/=; [|done..].
+    exists w, (S (S (S m))). rewrite !interp_S /= -!interp_S.
+    eauto using interp_le with lia.
+  - exists mv, (S (S n)). rewrite !interp_S /= -interp_S.
+    rewrite lookup_empty left_id_L H /=. eauto using interp_le with lia.
+  - destruct n as [|n]; [done|rewrite interp_S /= in Hinterp].
+    destruct (interp n _ _) as [mv'|] eqn:Hinterp'; simplify_res.
+    apply IHHstep in Hinterp' as (mw' & m1 & Hinterp1 & ?); simplify_res.
+    destruct mv' as [v'|], mw' as [w'|]; simplify_res; last first.
+    { exists None, (S m1). by rewrite interp_S /= Hinterp1. }
+    destruct (maybe VString _) eqn:Hstring; simplify_res; last first.
+    { exists None, (S m1). rewrite interp_S /= Hinterp1 /=.
+      by assert (maybe VString w' = None) as -> by (by destruct v', w'). }
+    destruct v', w'; simplify_eq/=.
+    eexists (Some (VClo _ _ _)), (S m1). rewrite !interp_S /=.
+    rewrite (interp_le Hinterp1) /=; last lia. done.
+  - destruct n as [|n]; [done|rewrite interp_S /= in Hinterp].
+    destruct (interp n _ _) as [mv'|] eqn:Hinterp'; simplify_res.
+    apply IHHstep in Hinterp' as (mw' & m1 & Hinterp1 & ?); simplify_res.
+    destruct mv' as [v'|], mw' as [w'|]; simplify_res; last first.
+    { exists None, (S m1). by rewrite interp_S /= Hinterp1. }
+    destruct (maybe3 VClo _) eqn:Hclo; simplify_res; last first.
+    { exists None, (S m1). rewrite interp_S /= Hinterp1 /=.
+      by assert (maybe3 VClo w' = None) as -> by (by destruct v', w'). }
+    destruct v', w'; simplify_eq/=.
+    eapply interp_proper in Hinterp as (mw & m2 & Hinterp2 & Hv);
+      last apply subst_env_insert_eq; try done.
+    exists mw, (S (m1 `max` m2)). rewrite !interp_S /=.
+    rewrite (interp_le Hinterp1) /=; last lia.
+    by rewrite (interp_le Hinterp2) /=; last lia.
+  - destruct n as [|n]; [done|rewrite interp_S /= in Hinterp].
+    destruct (interp n _ e1') as [mv1|] eqn:Hinterp1; simplify_eq/=.
+    apply IHHstep in Hinterp1 as (mw1 & m & Hinterp1 & Hw1).
+    destruct mv1 as [v1|], mw1 as [w1|]; simplify_res; last first.
+    { exists None, (S m). by rewrite interp_S /= Hinterp1. }
+    exists mv, (S (n `max` m)). split; [|done].
+    rewrite interp_S /= (interp_le Hinterp1) /=; last lia.
+    assert (maybe VString w1 = maybe VString v1) as ->.
+    { destruct v1, w1; naive_solver. }
+    destruct (maybe VString v1); simplify_res; [|done].
+    destruct (_ ∪ _); simplify_res; eauto using interp_le with lia.
+Qed.
+
+Lemma final_interp e :
+  final e →
+  ∃ w m, interp m ∅ e = mret w ∧ e = val_to_expr w.
+Proof.
+  induction e as [| |[]|]; inv 1.
+  - eexists (VString _), 1. by rewrite interp_S /=.
+  - eexists (VClo _ _ _), 2. rewrite interp_S /=. split; [done|].
+    by rewrite subst_env_empty.
+Qed.
+
+Lemma red_final_interp e :
+  red step e ∨ final e ∨ ∃ m, interp m ∅ e = mfail.
+Proof.
+  induction e.
+  - (* ENat *) right; left. constructor.
+  - (* EId *) destruct IHe as [[??]|[Hfinal|[m Hinterp]]].
+    + left. by repeat econstructor.
+    + apply final_interp in Hfinal as (w & m & Hinterp & ->).
+      destruct (maybe VString w) as [x|] eqn:Hw; last first.
+      { do 2 right. eexists (S m). rewrite interp_S /= Hinterp /=.
+        by rewrite Hw. }
+      destruct w; simplify_eq/=.
+      destruct (ds !! x) as [e|] eqn:Hx; last first.
+      { do 2 right. eexists (S m). rewrite interp_S /= Hinterp /=.
+        by rewrite Hx. }
+      left. by repeat econstructor.
+    + do 2 right. exists (S m). rewrite interp_S /= Hinterp. done.
+  - (* EAbs *) destruct IHe1 as [[??]|[Hfinal|[m Hinterp]]].
+    + left. by repeat econstructor.
+    + apply final_interp in Hfinal as (w & m & Hinterp & ->).
+      destruct (maybe VString w) as [x|] eqn:Hw; last first.
+      { do 2 right. eexists (S m). rewrite interp_S /= Hinterp /=.
+        by rewrite Hw. }
+      destruct w; naive_solver.
+    + do 2 right. exists (S m). rewrite interp_S /= Hinterp. done.
+  - (* EApp *) destruct IHe1 as [[??]|[Hfinal|[m Hinterp]]].
+    + left. by repeat econstructor.
+    + apply final_interp in Hfinal as (w & m & Hinterp & ->).
+      destruct (maybe3 VClo w) eqn:Hw.
+      { destruct w; simplify_eq/=. left. by repeat econstructor. }
+      do 2 right. exists (S m). by rewrite interp_S /= Hinterp /= Hw.
+    + do 2 right. exists (S m). by rewrite interp_S /= Hinterp.
+Qed.
+
+Lemma interp_complete e1 e2 :
+  e1 -->* e2 →
+  nf step e2 →
+  ∃ mw m, interp m ∅ e1 = Res mw ∧
+    if mw is Some w then e2 = val_to_expr w else ¬final e2.
+Proof.
+  intros Hsteps Hnf. induction Hsteps as [e|e1 e2 e3 Hstep _ IH].
+  { destruct (red_final_interp e) as [?|[Hfinal|[m Hinterp]]]; [done|..].
+    - apply final_interp in Hfinal as (w & m & ? & ?).
+      by exists (Some w), m.
+    - exists None, m. split; [done|]. intros Hfinal.
+      apply final_interp in Hfinal as (w & m' & ? & _).
+      by assert (mfail = mret w) by eauto using interp_agree. }
+  destruct IH as (mw & m & Hinterp & ?); try done.
+  eapply interp_step in Hinterp as (mw' & m' & ? & ?); last done.
+  destruct mw, mw'; naive_solver.
+Qed.
+
+Lemma interp_complete_ret e1 e2 :
+  e1 -->* e2 → final e2 →
+  ∃ w m, interp m ∅ e1 = mret w ∧ e2 = val_to_expr w.
+Proof.
+  intros Hsteps Hfinal. apply interp_complete in Hsteps
+    as ([w|] & m & ? & ?); naive_solver eauto using final_nf.
+Qed.
+Lemma interp_complete_fail e1 e2 :
+  e1 -->* e2 → nf step e2 → ¬final e2 →
+  ∃ m, interp m ∅ e1 = mfail.
+Proof.
+  intros Hsteps Hnf Hforce.
+  apply interp_complete in Hsteps as ([w|] & m & ? & ?); simplify_eq/=; try by eauto.
+  destruct Hforce. apply val_final.
+Qed.
+
+Lemma interp_sound_open E e n mv :
+  interp n E e = Res mv →
+  ∃ e', subst_env E e -->* e' ∧
+    if mv is Some v then e' = val_to_expr v else stuck e'.
+Proof.
+  revert E e mv.
+  induction n as [|n IH]; intros E e mv Hinterp; first done.
+  rewrite subst_env_eq. rewrite interp_S in Hinterp.
+  destruct e; simplify_res.
+  - (* EString *) by eexists.
+  - (* EId *)
+    destruct (interp _ _ _) as [mv1|] eqn:Hinterp1; simplify_res.
+    apply IH in Hinterp1 as (e1' & Hsteps1 & He1').
+    destruct mv1 as [v1|]; simplify_res; last first.
+    { eexists; split; [by eapply SId_rtc|]. split; [|inv 1].
+      intros [??]. destruct He1' as [Hnf []].
+      inv_step; simpl; eauto. destruct Hnf; eauto. }
+    destruct (maybe VString _) as [x|] eqn:Hv1; simplify_res; last first.
+    { eexists; split; [by eapply SId_rtc|]. split; [|inv 1].
+      intros [??]. destruct v1; inv_step. }
+    destruct v1; simplify_eq/=.
+    assert (thunk_to_expr <$> (E !! x) ∪ (Thunk ∅ <$> ds !! x)
+      = ((thunk_to_expr <$> E) ∪ ds) !! x).
+    { rewrite lookup_union lookup_fmap.
+      repeat destruct (_ !! _); f_equal/=; by rewrite subst_env_empty. }
+    destruct (_ ∪ _) as [[E' e']|] eqn:Hx; simplify_res.
+    * apply IH in Hinterp as (e'' & Hsteps & He'').
+      exists e''; split; [|done]. etrans; [by eapply SId_rtc|].
+      eapply rtc_l; [|done]. by econstructor.
+    * eexists; split; [by eapply SId_rtc|]. split; [|inv 1].
+      intros [? Hstep]. inv_step; simplify_eq/=; congruence.
+  - (* EAbs *)
+    destruct (interp _ _ _) as [mv1|] eqn:Hinterp1; simplify_res.
+    apply IH in Hinterp1 as (e1' & Hsteps1 & He1').
+    destruct mv1 as [v1|]; simplify_res; last first.
+    { eexists; split; [by eapply SAbsL_rtc|]. split.
+      + intros [??]. destruct He1' as [Hnf []].
+        inv_step; simpl; eauto. destruct Hnf; eauto.
+      + intros ?. destruct He1' as [_ []]. by destruct e1'. }
+    eexists; split; [by eapply SAbsL_rtc|].
+    destruct (maybe VString _) as [x|] eqn:Hv1; simplify_res; last first.
+    { split; [|destruct v1; inv 1]. intros [??]. destruct v1; inv_step. }
+    by destruct v1; simplify_eq/=.
+  - (* EApp *) destruct (interp _ _ _) as [mv'|] eqn:Hinterp'; simplify_res.
+    apply IH in Hinterp' as (e' & Hsteps & He'); try done.
+    destruct mv' as [v'|]; simplify_res; last first.
+    { eexists; repeat split; [by apply SAppL_rtc| |inv 1].
+      intros [e'' Hstep]. destruct He' as [Hnf Hfinal].
+      inv Hstep; [by destruct Hfinal; constructor|]. destruct Hnf. eauto. }
+    destruct (maybe3 VClo v') eqn:?; simplify_res; last first.
+    { eexists; repeat split; [by apply SAppL_rtc| |inv 1].
+      intros [e'' Hstep]. inv Hstep; destruct v'; by repeat inv_step. }
+    destruct v'; simplify_res.
+    apply IH in Hinterp as (e'' & Hsteps' & He'').
+    eexists; split; [|done]. etrans; [by apply SAppL_rtc|].
+    eapply rtc_l; first by constructor.
+    rewrite subst_env_insert // in Hsteps'.
+Qed.
+
+Lemma interp_sound n e mv :
+  interp n ∅ e = Res mv →
+  ∃ e', e -->* e' ∧ if mv is Some v then e' = val_to_expr v else stuck e'.
+Proof.
+  intros Hsteps%interp_sound_open; try done.
+  by rewrite subst_env_empty in Hsteps.
+Qed.
+
+(** Final theorems *)
+Theorem interp_sound_complete_ret e v :
+  (∃ w n, interp n ∅ e = mret w ∧ val_to_expr v = val_to_expr w)
+  ↔ e -->* val_to_expr v.
+Proof.
+  split.
+  - by intros (n & w & (e' & ? & ->)%interp_sound & ->).
+  - intros Hsteps. apply interp_complete_ret in Hsteps as ([] & ? & ? & ?);
+      eauto using val_final.
+Qed.
+
+Theorem interp_sound_complete_ret_string e s :
+  (∃ n, interp n ∅ e = mret (VString s)) ↔ e -->* EString s.
+Proof.
+  split.
+  - by intros [n (e' & ? & ->)%interp_sound].
+  - intros Hsteps. apply interp_complete_ret in Hsteps as ([] & ? & ? & ?);
+      simplify_eq/=; eauto.
+Qed.
+
+Theorem interp_sound_complete_fail e :
+  (∃ n, interp n ∅ e = mfail) ↔ ∃ e', e -->* e' ∧ stuck e'.
+Proof.
+  split.
+  - by intros [n ?%interp_sound].
+  - intros (e' & Hsteps & Hnf & Hforced). by eapply interp_complete_fail.
+Qed.
+
+Theorem interp_sound_complete_no_fuel e :
+  (∀ n, interp n ∅ e = NoFuel) ↔ all_loop step e.
+Proof.
+  rewrite all_loop_alt. split.
+  - intros Hnofuel e' Hsteps.
+    destruct (red_final_interp e') as [|[|He']]; [done|..].
+    + apply interp_complete_ret in Hsteps as (w & m & Hinterp & _); last done.
+      by rewrite Hnofuel in Hinterp.
+    + apply interp_sound_complete_fail in He' as (e'' & ? & [Hnf _]).
+      destruct (interp_complete e e'') as (mv & n & Hinterp & _); [by etrans|done|].
+      by rewrite Hnofuel in Hinterp.
+  - intros Hred n. destruct (interp n ∅ e) as [mv|] eqn:Hinterp; [|done].
+    apply interp_sound in Hinterp as (e' & Hsteps%Hred & Hstuck).
+    destruct mv as [v|]; simplify_eq/=.
+    + apply final_nf in Hsteps as []. apply val_final.
+    + by destruct Hstuck as [[] ?].
+Qed.
+
+End dynlang.
diff --git a/theories/dynlang/operational.v b/theories/dynlang/operational.v
new file mode 100644
index 0000000..34cca7b
--- /dev/null
+++ b/theories/dynlang/operational.v
@@ -0,0 +1,41 @@
+From mininix Require Export utils.
+From stdpp Require Import options.
+
+Module Import dynlang.
+
+Inductive expr :=
+  | EString (s : string)
+  | EId (ds : gmap string expr) (ex : expr)
+  | EAbs (ex e : expr)
+  | EApp (e1 e2 : expr).
+
+Fixpoint subst (ds : gmap string expr) (e : expr) : expr :=
+  match e with
+  | EString s => EString s
+  | EId ds' e => EId (ds ∪ ds') (subst ds e)
+  | EAbs ex e => EAbs (subst ds ex) (subst ds e)
+  | EApp e1 e2 => EApp (subst ds e1) (subst ds e2)
+  end.
+
+Reserved Infix "-->" (right associativity, at level 55).
+Inductive step : expr → expr → Prop :=
+  | Sβ x e1 e2 : EApp (EAbs (EString x) e1) e2 --> subst {[x:=e2]} e1
+  | SIdString ds x e : ds !! x = Some e → EId ds (EString x) --> e
+  | SAbsL ex1 ex1' e : ex1 --> ex1' → EAbs ex1 e --> EAbs ex1' e
+  | SAppL e1 e1' e2 : e1 --> e1' → EApp e1 e2 --> EApp e1' e2
+  | SId ds e1 e1' : e1 --> e1' → EId ds e1 --> EId ds e1'
+where "e1 --> e2" := (step e1 e2).
+
+Infix "-->*" := (rtc step) (right associativity, at level 55).
+
+Definition final (e : expr) : Prop :=
+  match e with
+  | EString _ => True
+  | EAbs (EString _) _ => True
+  | _ => False
+  end.
+
+Definition stuck (e : expr) : Prop :=
+  nf step e ∧ ¬final e.
+
+End dynlang.
diff --git a/theories/dynlang/operational_props.v b/theories/dynlang/operational_props.v
new file mode 100644
index 0000000..9e8028c
--- /dev/null
+++ b/theories/dynlang/operational_props.v
@@ -0,0 +1,33 @@
+From mininix Require Export dynlang.operational.
+From stdpp Require Import options.
+
+Module Import dynlang.
+Export dynlang.
+
+(** Properties of operational semantics *)
+Lemma step_not_final e1 e2 : e1 --> e2 → ¬final e1.
+Proof. induction 1; simpl; repeat case_match; naive_solver. Qed.
+Lemma final_nf e : final e → nf step e.
+Proof. by intros ? [??%step_not_final]. Qed.
+
+Lemma SAbsL_rtc ex1 ex1' e : ex1 -->* ex1' → EAbs ex1 e -->* EAbs ex1' e.
+Proof. induction 1; econstructor; eauto using step. Qed.
+Lemma SAppL_rtc e1 e1' e2 : e1 -->* e1' → EApp e1 e2 -->* EApp e1' e2.
+Proof. induction 1; econstructor; eauto using step. Qed.
+Lemma SId_rtc ds e1 e1' : e1 -->* e1' → EId ds e1 -->* EId ds e1'.
+Proof. induction 1; econstructor; eauto using step. Qed.
+
+Ltac inv_step := repeat
+  match goal with H : ?e --> _ |- _ => assert_fails (is_var e); inv H end.
+
+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;
+    f_equal; by apply IHHred1.
+Qed.
+
+End dynlang.