(* iris_unstable/heap_lang/interpreter.v *)
From stdpp Require Import gmap
From iris.heap_lang Require Export lang
From iris.heap_lang Require Import tactics pretty
From iris.prelude Require Import options

Local Ltacinvc H := inversion H; subst; clear H.

Inductive Error:=
| Stuck (s:string)
| Unsupported (s:string)
| OutOfFuel.

Global Instanceerror_pretty : Pretty Error :=
  λ err, match err with
         | Stuck s => "stuck: " +:+ s
         | Unsupported s => "unsupported operation: " +:+ s
         | OutOfFuel => "out of fuel"
         end.

Record interp_state:=
    InterpState { lang_state : state; next_loc : Z; forked_threads : list expr; }.
  Add Printing Constructor interp_state.

Definition modify_lang_state(f: state → state): interp_state → interp_state :=
    λ s, InterpState (f s.(lang_state)) s.(next_loc) (s.(forked_threads)).

Definition add_forked_thread(e: expr) : interp_state → interp_state :=
    λ s, InterpState s.(lang_state) s.(next_loc) (s.(forked_threads) ++ [e]).

Definition interp_state_alloc(n: Z) : interp_state → interp_state :=
    λ s, InterpState s.(lang_state) (n + s.(next_loc)) s.(forked_threads).

Inductive state_wf(s: interp_state): Prop :=
    { state_wf_holds (l: loc) : (s.(next_loc) ≤ l.(loc_car))%Z →
                                s.(lang_state).(heap) !! l = None; }.

Definition InterpretM(A:Type) : Type :=
    interp_state → (A+Error) * interp_state.

Definition init_state: state := {| heap := ∅; used_proph_id := ∅ |}.

Definition init_interp_state: interp_state :=
    InterpState init_state 1 [].

Local Definitionrun {A} (f: InterpretM A) : A + Error :=
    (f init_interp_state).1.

Lemma init_interp_state_wf: state_wf init_interp_state.
  Proof. constructor; rewrite /init_interp_state //=. Qed.

Global Instanceinterp_ret : MRet InterpretM := λ A (x:A), λ s, (inl x, s).

Global Instanceinterp_bind : MBind InterpretM :=
    λ A B (f: A → InterpretM B) (x: InterpretM A),
    λ s, let (r, s') := x s in
        match r with
        | inl x' => f x' s'
        | inr e => (inr e, s')
        end.

Global Instanceinterp_fmap : FMap InterpretM :=
    λ A B (f: A → B) (x: InterpretM A),
    λ s, let (r, s') := x s in
        match r with
        | inl x' => (inl (f x'), s')
        | inr e => (inr e, s')
        end.

Definition interp_modify(f: interp_state → interp_state): InterpretM () :=
    λ s, (inl (), f s).

Definition interp_modify_state(f: state → state): InterpretM () :=
    interp_modify (modify_lang_state f).

Definition interp_read{A} (f: state → A): InterpretM A :=
    λ s, (inl (f s.(lang_state)), s).

Definition interp_error{A} (msg: string) : InterpretM A := λ s, (inr (Stuck msg), s).

Definition interp_alloc(n:Z): InterpretM loc :=
    λ s, (inl {| loc_car := s.(next_loc)|}, interp_state_alloc n s).

Definition read_loc(method: string) (vl: val) : InterpretM (loc*val) :=
      match vl with
      | LitV (LitLoc l) =>
        mv ← interp_read (λ σ, σ.(heap) !! l);
        match mv with
        | Some (Some v) => mret (l, v)
        | Some None =>
          interp_error $ method +:+ ": use after free at location: " +:+ pretty l
        | None =>
          interp_error $ method +:+ ": unallocated location: " +:+ pretty l
        end
      | _ => interp_error $ method +:+ ": applied to non-loc " +:+ pretty vl
      end.

Lemma error_not_inl{A} {msg s} {v: A} {s'} :
    interp_error msg s = (inl v, s') → False.
  Proof. by inversion 1. Qed.

Lemma mret_inv{A} (v: A) s v' s' :
    (mret v : InterpretM A) s = (inl v', s') → v = v' ∧ s = s'.
  Proof. by inversion 1. Qed.

Lemma interp_bind_invA B (x: InterpretM A) (f: A → InterpretM B) r s s' :
    (x ≫= f) s = (r, s') →
    (∃ e, x s = (inr e, s') ∧ r = inr e) ∨
    (∃ s0 x', x s = (inl x', s0) ∧
              f x' s0 = (r, s')).
  Proof.
    rewrite /mbind /interp_bind.
    repeat case_match; inversion 1; subst; eauto.
  Qed.

Lemma interp_bind_inl_invA B (x: InterpretM A) (f: A → InterpretM B) (r: B) s s' :
    (x ≫= f) s = (inl r, s') →
    ∃ s0 x', x s = (inl x', s0) ∧
             f x' s0 = (inl r, s').
  Proof.
    intros [(e & ? & ?) | (s0 & x' & H1 & H2)]%interp_bind_inv.
    - congruence.
    - rewrite H1.
      eexists _, _; eauto.
  Qed.

Lemma interp_fmap_inv{A B} (f: A → B) x s v s' :
    (fmap f x : InterpretM B) s = (inl v, s') →
    ∃ v0, v = f v0 ∧ x s = (inl v0, s').
  Proof.
    rewrite /fmap /interp_fmap.
    repeat case_match; inversion 1; subst; eauto.
  Qed.

Lemma read_loc_invmethod vl s l v s' :
    read_loc method vl s = (inl (l, v), s') →
    vl = LitV (LitLoc l) ∧
    s' = s ∧
    s.(lang_state).(heap) !! l = Some (Some v).
  Proof.
    rewrite /read_loc.
    destruct vl as [l' | | | | ]; try by inversion 1.
    destruct l' as [| | | | l' |]; intro H; try by inversion H.
    apply interp_bind_inl_inv in H as (s0 & mv & Heq1 & Heq2).
    destruct mv as [mv|]; try by inversion Heq2.
    destruct mv; inversion Heq2; subst; clear Heq2.
    inversion Heq1; subst; clear Heq1.
    eauto.
  Qed.

Ltac errored:=
    lazymatch goal with
    | H: interp_error _ _ = (inl _, _) |- _ => solve [ exfalso; apply (error_not_inl H) ]
    | H: (inr _, _) = (inl _, _) |- _ => solve [ exfalso; inversion H ]
    end.

Ltac success:=
    repeat
      lazymatch goal with
      | H: mret _ _ = (inl _, _) |- _ =>
        let Heqv := fresh "Heqv" in
        let Heqs := fresh "Heqs" in
        apply mret_inv in H as [Heqv Heqs]; subst
      | H: (_ ≫= (λ x, _)) _ = (inl _, _) |- _ =>
        let s := fresh "s" in
        let x := fresh x in
        let Heq1 := fresh "Heq" in
        let Heq2 := fresh "Heq" in
        apply interp_bind_inl_inv in H as (s & x & Heq1 & Heq2); subst
      | H: (_ <$> _) _ = (inl ?v, _) |- _ =>
        let s := fresh "s" in
        let v_tmp := fresh "v" in
        rename v into v_tmp;
        apply interp_fmap_inv in H as (v & -> & H)
      | H: interp_modify _ _ = (inl _, _) |- _ => invc H
      | H: interp_modify_state _ _ = (inl _, _) |- _ => invc H
      | H: interp_read _ _ = (inl _, _) |- _ => invc H
      | H: read_loc _ _ _ = (inl _, _) |- _ =>
        apply read_loc_inv in H as (-> & -> & H)
      end; subst.

Lemma interp_bind_inr_inv{A B} (x: InterpretM A) (f: A → InterpretM B) r s s' :
    (x ≫= f) s = (inr r, s') →
    (x s = (inr r, s')) ∨
    (∃ s0 x', x s = (inl x', s0) ∧ f x' s0 = (inr r, s')).
  Proof.
    rewrite /mbind /interp_bind.
    repeat case_match; intros; simplify_eq/=; eauto.
  Qed.

Lemma interp_fmap_inr_inv{A B} (f: A → B) (x: InterpretM A) s e s' :
    (fmap f x : InterpretM B) s = (inr e, s') →
    x s = (inr e, s').
  Proof.
    rewrite /fmap /interp_fmap.
    repeat case_match; intros; simplify_eq/=; auto.
  Qed.

Lemma read_loc_inr_invmethod vl s err s' :
    read_loc method vl s = (inr err, s') →
    s = s' ∧ match vl with
             | LitV (LitLoc l) => ∀ v, s.(lang_state).(heap) !! l ≠ Some (Some v)
             | _ => True
             end.
  Proof.
    rewrite /read_loc.
    repeat case_match; subst; try solve [ inversion 1; subst; auto ].
    intros H.
    apply interp_bind_inr_inv in H as [H|(s0&x& Hexec1 & Hexec2)]; success.
    - invc H.
    - repeat case_match; invc Hexec2.
      + intuition congruence.
      + intuition congruence.
  Qed.

Ltac failure:=
    repeat
      match goal with
      | H: (_ ≫= _) _ = (inr _, _) |- _ =>
        let s := fresh "s" in
        let x := fresh "x" in
        let Heq := fresh "Heq" in
        apply interp_bind_inr_inv in H as [H | (s & x & Heq & H)]
      | H: interp_error _ _ = (inr _, _) |- _ => invc H
      | H: mret _ _ = (inr _, _) |- _ => solve [ inversion H ]
      | H: interp_modify _ _ = (inr _, _) |- _ => solve [ inversion H ]
      | H: interp_modify_state _ _ = (inr _, _) |- _ => solve [ inversion H ]
      | H: (_ <$> _) _ = (inr _, _) |- _ =>
        apply interp_fmap_inr_inv in H
      | H: read_loc _ _ _ = (inr _, _) |- _ =>
        apply read_loc_inr_inv in H as [-> H]
      end; subst.

Local Instancepretty_string : Pretty string := λ s, s.

Local Definitionpretty_app (s: string) {A} `{Pretty A} (x:A) : string :=
    s +:+ pretty x.
  Infix "+" := pretty_app.

Definition option_opposites{A B} (m1 : option A) (m2 : option B) :=
    is_Some m1 ↔ m2 = None.

Lemma option_opposites_alt{A B} (m1 : option A) (m2 : option B) :
    option_opposites m1 m2 ↔ match m1, m2 with
                             | Some _, None   => True
                             | None  , Some _ => True
                             | _     , _      => False
                             end.
  Proof.
    rewrite /option_opposites is_Some_alt.
    repeat case_match; intuition congruence.
  Qed.

Definition explain_un_op_failop v : option string :=
    match op with
    | NegOp => match v with
               | LitV (LitInt _) => None
               | LitV (LitBool _) => None
               | _ => Some $ "~ (NegOp) can only be applied to integers and booleans, got " + v
               end
    | MinusUnOp =>
      match v with
      | LitV (LitInt _) => None
      | _ => Some $ "unary - (MinusUnOp) can only be applied to integers, got " + v
      end
    end.

Lemma explain_un_op_fail_wfop v :
    option_opposites (explain_un_op_fail op v) (un_op_eval op v).
  Proof.
    apply option_opposites_alt.
    rewrite /explain_un_op_fail /un_op_eval.
    repeat case_match; simplify_eq/=; auto.
  Qed.

Definition explain_unboxedv : option string :=
    match v with
    | LitV l | InjLV (LitV l) | InjRV (LitV l) =>
      match l with
      | LitPoison => Some "poison values (from erasing prophecies) cannot be compared"
      | LitProphecy _ => Some "prophecies cannot be compared"
      | _ => None
      end
    | InjLV _ | InjRV _ => Some "sum values can only be compared if they contain literals"
    | PairV _ _ => Some "pairs are large and considered boxed, must compare by field"
    | RecV _ _ _ => Some "closures are large and cannot be compared"
    end.

Lemma explain_unboxed_wfv :
    match explain_unboxed v with
    | Some _ => ~val_is_unboxed v
    | None   => val_is_unboxed v
    end.
  Proof.
    rewrite /explain_unboxed /val_is_unboxed /lit_is_unboxed.
    repeat case_match; intuition congruence.
  Qed.

Definition explain_vals_compare_safe_failv1 v2 : option string :=
    match explain_unboxed v1, explain_unboxed v2 with
    | Some msg1, Some msg2 =>
      Some $ "one of " + v1 + " and " + v2 + " must be unboxed to compare: "
      + v1 + ": " + msg1 + ", "
      + v2 + ": " + msg2
    | _, _ => None
    end.

Lemma explain_vals_compare_safe_fail_wfv1 v2 :
    is_Some (explain_vals_compare_safe_fail v1 v2) ↔ ~vals_compare_safe v1 v2.
  Proof.
    cut (explain_vals_compare_safe_fail v1 v2 = None ↔ vals_compare_safe v1 v2).
    { rewrite is_Some_alt.
      destruct (explain_vals_compare_safe_fail _ _); intuition congruence. }
    rewrite /explain_vals_compare_safe_fail /vals_compare_safe.
    pose proof (explain_unboxed_wf v1).
    pose proof (explain_unboxed_wf v2).
    destruct (explain_unboxed v1), (explain_unboxed v2); intuition congruence.
  Qed.

Definition explain_bin_op_failop v1 v2 : option string :=
    if decide (op = EqOp)
    then (explain_vals_compare_safe_fail v1 v2)
    else match v1, v2 with
         | LitV (LitInt _), LitV (LitInt _) =>
           match op with
           | OffsetOp => Some $ "cannot add to integer " + v1 + " with +ₗ (only locations)"
           | _ => None
           end
         | LitV (LitBool b1), LitV (LitBool b2) =>
           match bin_op_eval_bool op b1 b2 with
           | Some _ => None
           | None => Some $ "non-boolean operator applied to booleans " + op
           end
         | LitV (LitLoc _), _ =>
           match op, v2 with
           | OffsetOp, LitV (LitInt _) => None
           | OffsetOp, _ => Some $ "can only call +ₗ on integers, got " + v2
           | LeOp, LitV (LitLoc _) => None
           | LeOp, _ => Some $ "cannot use ≤ on location " + v1 + " and " + v2
           | LtOp, LitV (LitLoc _) => None
           | LtOp, _ => Some $ "cannot use < on location " + v1 + " and " + v2
           | _, _ => Some $ "the only supported operations on locations are " +
                            " +ₗ #i, ≤ #l and < #l; got " + op + " " + v2
           end
         | _, _ => Some $ "mismatched types of values " + v1 + " and " + v2
         end.

Lemma explain_bin_op_fail_wfop v1 v2 :
    option_opposites (explain_bin_op_fail op v1 v2) (bin_op_eval op v1 v2).
  Proof.
    apply option_opposites_alt.
    rewrite /explain_bin_op_fail /bin_op_eval
            /bin_op_eval_int /bin_op_eval_bool /bin_op_eval_loc.
    repeat (case_match; simplify_eq/=; auto).
    - pose proof (explain_vals_compare_safe_fail_wf v1 v2).
      intuition eauto.
    - pose proof (explain_vals_compare_safe_fail_wf v1 v2) as Hwf.
      replace (explain_vals_compare_safe_fail v1 v2) in Hwf.
      rewrite -> is_Some_alt in Hwf.
      intuition eauto.
  Qed.

Local Notationerror := interp_error.

Fixpoint interpret(fuel:nat) (e: expr) {struct fuel} : InterpretM val :=
    match fuel with
    | 0 => λ s, (inr OutOfFuel, s)
    | S fuel' => let interp := interpret fuel' in
    match e with

Lemma atomic_stepe σ e' σ' :
  base_step e σ [] e' σ' [] →
  ∀ tp, rtc erased_step (e :: tp, σ) (e' :: tp, σ').
Proof.
  intros ? tp.
  apply rtc_once.
  exists [].
  eapply (step_atomic e σ e' σ' [] [] tp); simpl; auto.
  - rewrite app_nil_r //.
  - eapply (Ectx_step []); eauto.
Qed.

Lemma step_invts1 σ1 κ ts2 σ2 :
  step (Λ:=heap_lang) (ts1, σ1) κ (ts2, σ2) →
  ∃ (t1 : list expr) (e1 : expr) (t2 : list expr) (e2 : expr) (efs: list expr),
    ts1 = t1 ++ e1 :: t2 ∧
    ts2 = t1 ++ e2 :: t2 ++ efs ∧
    prim_step e1 σ1 κ e2 σ2 efs.
Proof.
  inversion 1.
  simplify_eq.
  eauto 10.
Qed.

Lemma fill_stepK (e: expr) σ tp κ e' σ' tp' :
  step (e :: tp, σ) κ (e' :: tp', σ') →
  step (fill K e :: tp, σ) κ (fill K e' :: tp', σ').
Proof.
  intros Hstep.
  apply step_inv in Hstep as (t1 & e1 & t2 & e2 & efs & Heq1 & Heq2 & Hprim_step).
  pose proof Hprim_step as H.
  apply (fill_prim_step K) in H.
  simpl in H.
  destruct t1 as [|e0 t1].
  - simplify_eq/=.
    eapply (step_atomic _ _ _ _ efs [] t2); eauto.
  - simplify_eq/=.
    eapply (step_atomic _ _ _ _ efs (fill K e0 :: t1) t2); eauto.
Qed.

Lemma fill_erased_step(e: expr) σ tp e' σ' tp' K :
  erased_step (e :: tp, σ) (e' :: tp', σ') →
  erased_step (fill K e :: tp, σ) (fill K e' :: tp', σ').
Proof.
  rewrite /erased_step.
  intros [κ Hstep].
  exists κ.
  apply fill_step; auto.
Qed.

Lemma step_cons_no_destroy(e: expr) tp σ κ ρ2 :
  step (e :: tp, σ) κ ρ2 →
  ∃ e' tp' σ', ρ2 = (e' :: tp', σ').
Proof.
  destruct ρ2 as [ts' σ'].
  intros (t1&?&?&?&?&?&?&?)%step_inv; subst.
  destruct t1; simplify_eq/=; eauto.
Qed.

Lemma language_nsteps_inv_r(Λ: language) n ρ1 κs ρ2 :
  language.nsteps (Λ:=Λ) (S n) ρ1 κs ρ2 →
  ∃ ρ' κ κs', step ρ1 κ ρ' ∧ κs = κ ++ κs' ∧
              language.nsteps n ρ' κs' ρ2.
Proof. inversion 1; subst; eauto 10. Qed.

Lemma fill_erased_steps(e: expr) σ tp e' σ' tp' K :
  rtc erased_step (e :: tp, σ) (e' :: tp', σ') →
  rtc erased_step (fill K e :: tp, σ) (fill K e' :: tp', σ').
Proof.
  rewrite !erased_steps_nsteps.
  destruct 1 as (n & κs & Hsteps).
  generalize dependent e.
  generalize dependent tp.
  generalize dependent σ.
  generalize dependent e'.
  generalize dependent tp'.
  generalize dependent σ'.
  generalize dependent κs.
  induction n as [|n IHn]; intros ??????? Hsteps.
  - invc Hsteps.
    exists 0, [].
    constructor.
  - apply language_nsteps_inv_r in Hsteps as (ρ2 & κ & κs' & (Hstep & -> & Hsteps)).

Ltac change_to_fille :=
    reshape_expr e ltac:(fun K e' =>

Ltac step_ctx:=
    lazymatch goal with
    | |- rtc erased_step (?e :: _, _) _ =>
      change_to_fill e;
      step by (apply fill_erased_steps; eauto)
    end.

Ltac step_atomic:=
    step by (apply atomic_step; eauto using base_step);
    try reflexivity.

Lemma state_wf_init_alloc(v0 : val) (s : interp_state) (n : Z) :
    (0 ≤ n)%Z →
    state_wf s →
    state_wf
      (modify_lang_state
          (λ σ : state, state_init_heap {| loc_car := next_loc s |} n v0 σ)
          (interp_state_alloc n s)).
  Proof.
    intros Hn.
    constructor; rewrite /modify_lang_state /interp_state_alloc /=; intros l ?.
    apply fin_maps.lookup_union_None; split.
    - destruct (heap_array _ _ !! l) eqn:Hlookup; auto.
      apply heap_array_lookup in Hlookup as (j & w & Hle & ? & ? & Hlookup); subst.
      apply lookup_replicate in Hlookup as [? ?]; subst.
      simpl in *.
      lia.
    - apply state_wf_holds; auto.
      lia.
  Qed.

Lemma state_wf_same_doms f :
    (dom (f s.(lang_state)).(heap) = dom s.(lang_state).(heap)) →
    state_wf s →
    state_wf (modify_lang_state f s).
  Proof.
    intros Hdom_eq Hwf.
    constructor; rewrite /modify_lang_state /= => l ?.
    apply (fin_map_dom.not_elem_of_dom (D:=gset loc)).
    rewrite Hdom_eq.
    apply fin_map_dom.not_elem_of_dom.
    apply state_wf_holds; auto.
  Qed.

Lemma state_wf_upds l mv0 v' :
    state_wf s →
    heap (lang_state s) !! l = Some mv0 →
    state_wf (modify_lang_state (λ σ : state, state_upd_heap <[l:=v']> σ) s).
  Proof.
    intros Hwf Heq.
    apply state_wf_same_dom; auto.
    rewrite fin_map_dom.dom_insert_L.
    apply (fin_map_dom.elem_of_dom_2 (D:=gset loc)) in Heq.
    set_solver.
  Qed.

Lemma interpret_wffuel (e: expr) s v s' :
    state_wf s →
    interpret fuel e s = (inl v, s') →
    state_wf s'.
  Proof.
    revert e s v s'.
    induction fuel as [|fuel]; simpl; intros e s v s' **; [ errored | ].
    destruct e; try errored; success; eauto;
      (repeat case_match; subst; try errored;
       success;
       eauto using state_wf_upd).
    - match goal with
      | H: interp_alloc _ _ = (_, _) |- _ => invc H
      end.
      apply state_wf_init_alloc; eauto.
      lia.
    - apply state_wf_same_dom; eauto.
    - constructor; intros.
      simpl.
      apply state_wf_holds; auto.
  Qed.

Local HintResolve interpret_wf : core.

Lemma interpret_soundfuel e s v s' :
    state_wf s →
    interpret fuel e s = (inl v, s') →
    rtc erased_step (e :: s.(forked_threads), s.(lang_state)) (Val v :: s'.(forked_threads), s'.(lang_state)).
  Proof.
    revert e s v s'.
    induction fuel as [|fuel]; simpl; intros e s v s' **; [ errored | ].
    destruct e; try errored; success; cbn [forked_threads lang_state];
      repeat match goal with
             | H: (match ?x with
                   | _ => _
                   end _ = (inl _, _)) |- _ =>
               let Heqn := fresh "Heqn" in
               destruct x eqn:Heqn; try errored; [idtac]
             | _ => progress success
             | _ => step_ctx
             | _ => step_atomic
             end.
    -
      reflexivity.
    -
      eauto.
    -
      lazymatch goal with
      | |- context[LitBool ?b] => destruct b; step_atomic; eauto
      end.
    -
      lazymatch goal with
      | |- context[Case (Val ?v)] => destruct v; try errored; step_atomic; eauto
      end.
    -
      lazymatch goal with
      | H: interp_alloc _ _ = _ |- _ => invc H
      end.
      eapply atomic_step. constructor; auto; intros.
      simpl. apply state_wf_holds; eauto.
      simpl; lia.
    -
      eapply rtc_once. exists [].
      lazymatch goal with

Definition eventually_stuck(e: expr) tp σ tp' σ' :=
    ∃ e'', rtc erased_step (e :: tp, σ) (e'':: tp', σ') ∧ stuck e'' σ'.

Lemma eventually_stuck_now(e: expr) tp σ :
    stuck e σ →
    eventually_stuck e tp σ tp σ.
  Proof.
    intros.
    exists e.
    split; [ reflexivity | auto ].
  Qed.

Lemma eventually_stuck_stepse tp σ tp0 σ0 e' tp' σ' :
    rtc erased_step (e :: tp, σ) (e' :: tp0, σ0) →
    eventually_stuck e' tp0 σ0 tp' σ' →
    eventually_stuck e tp σ tp' σ'.
  Proof.
    intros Hsteps (e'' & Hsteps' & Hstuck).
    eexists. split; [ etrans; eauto | eauto ].
  Qed.

Lemma eventually_stuck_fillK e tp σ tp' σ' :
    eventually_stuck e tp σ tp' σ' →
    eventually_stuck (fill K e) tp σ tp' σ'.
  Proof.
    intros (e' & Hsteps & Hstuck).
    eexists (fill K e'). split.
    - apply fill_erased_steps; auto.
    - apply stuck_fill; auto.
  Qed.

Local HintResolve interpret_sound : core.

Ltac stuck_steps:=
    eapply eventually_stuck_steps;
    [ repeat step_ctx; (step_atomic || reflexivity)
    |].

Ltac stuck_fill:=
    lazymatch goal with
    | |- eventually_stuck ?e _ _ _ _ =>
      change_to_fill e; apply eventually_stuck_fill; solve [ eauto ]
    end.

Definition terminal_expre :=
    ∀ K e', to_val e' = None →
            e = fill K e' →
            K = [] ∧ e' = e.

Lemma stuck_not_vale σ :
    to_val e = None →
    (∀ (κs: list observation) (e': expr) (σ': state) (efs: list expr),
        prim_step e σ κs e' σ' efs → False) →
    stuck e σ.
  Proof.
    rewrite /stuck /irreducible.
    intuition.
  Qed.

Local HintResolve val_base_stuck : core.

Lemma terminal_expr_stucke σ :
    to_val e = None →
    terminal_expr e →
    (∀ κ e' σ' efs, base_step e σ κ e' σ' efs → False) →
    stuck e σ.
  Proof.
    intros Hnot_val Hterminal Hno_base_step.
    apply stuck_not_val; first done; intros * Hstep.
    invc Hstep; simpl in *.
    lazymatch type of Hnot_val with
    | to_val (fill ?K ?e1') = None => edestruct (Hterminal K e1') as [-> ?]; eauto
    end.
  Qed.

Lemma fill_not_val'K e v :
    to_val e = None →
    Val v = fill K e →
    False.
  Proof.
    intros H Hfill.
    apply (fill_not_val K) in H; simpl in *.
    rewrite -Hfill /= in H.
    congruence.
  Qed.

Lemma list_rev_case{A} (l: list A) :
    l = [] ∨ ∃ x l', l = l' ++ [x].
  Proof.
    induction l using rev_ind; eauto.
  Qed.

Ltac ctx_caseK Ki :=
    let K' := fresh "K" in
    destruct (list_rev_case K) as [->| (Ki & K' & ->)]; [by auto|];
    rewrite ?fill_app /=.

Ltac prove_terminal:=
    lazymatch goal with
    | |- terminal_expr _ =>
      let K := fresh "K" in
      let e := fresh "e" in
      let Ki := fresh "Ki" in
      intros K e; ctx_case K Ki;
      destruct Ki;
      let H := fresh in
      intros ? H; invc H;
      solve [ exfalso; eauto using fill_not_val' ]
    | _ => fail "not a terminal_expr goal"
    end.

Lemma fill_app_invv1 v2 :
    terminal_expr (App (Val v1) (Val v2)).
  Proof. prove_terminal. Qed.

Ltac stuck_now:=
    apply eventually_stuck_now, terminal_expr_stuck;
    [done
    |prove_terminal
    |let H := fresh "Hstep" in
     intros * H;
     try (inversion H; congruence) ].

Lemma interpret_completefuel : ∀ e s msg s',
    ∀ (Hwf: state_wf s),
      interpret fuel e s = (inr (Stuck msg), s') →
      eventually_stuck e s.(forked_threads) s.(lang_state) s'.(forked_threads) s'.(lang_state).
  Proof.
    induction fuel as [|fuel]; simpl; intros e s msg s' **; [congruence|].
    destruct e; failure; stuck_steps; try stuck_fill;
      try (repeat case_match; failure; try stuck_now;
           let n := numgoals in guard n <= 1);
      simplify_eq.
    -
      stuck_steps.
      eauto.
    -
      repeat case_match; failure; try stuck_now.
      + stuck_steps; eauto.
      + stuck_steps; eauto.
    -
      repeat case_match; failure; try stuck_now.
      + stuck_steps; eauto.
      + stuck_steps; eauto.
    -
      success. stuck_now.
    -
      lazymatch goal with
      | H: read_loc _ _ _ = (inl ?p, _) |- _ => destruct p as [l v]
      end.
      success.
      repeat case_match; failure; stuck_now.
  Qed.

Definition exec(fuel:nat) (e: expr) : val + Error :=
  interp_monad.run (interpret fuel e).

Theorem exec_specfuel e :
  match exec fuel e with
  | inl v =>