interpreter.v

    (* If the interpreter fails otherwise (due to running out of fuel or an
    unsupported prophecy variable operation), then it provides no guarantees. *)
    True
  end.
Proof.
  rewrite /exec /interp_monad.run.
  destruct (interpret fuel e init_interp_state) as [r s] eqn:Hinterpret.
  destruct r as [v | [msg|msg|] ]; simpl; auto.
  - apply interpret_sound in Hinterpret;
      eauto using init_interp_state_wf.
  - apply interpret_complete in Hinterpret;
      auto using init_interp_state_wf.
    destruct Hinterpret as (e' & Hexec & Hstuck); eauto.
Qed.