source: C-semantics/Cexec.ma @ 5

include "Csem.ma".

include "extralib.ma".

(* Some experimental definitions for an executable semantics. *)

ndefinition bool_of_val_1 : val → type → res val ≝
  λv,ty. match v with
  [ Vint i ⇒ match ty with
    [ Tint _ _ ⇒ OK ? (of_bool (¬eq i zero))
    | Tpointer _ ⇒ OK ? (of_bool (¬eq i zero))
    | _ ⇒ Error ?
    ]
  | Vfloat f ⇒ match ty with
    [ Tfloat _ ⇒ OK ? (of_bool (¬Fcmp Ceq f Fzero))
    | _ ⇒ Error ?
    ]
  | Vptr _ _ ⇒ match ty with
    [ Tint _ _ ⇒ OK ? Vtrue
    | Tpointer _ ⇒ OK ? Vtrue
    | _ ⇒ Error ?
    ]
  | _ ⇒ Error ?
  ].

(* There's a lot more repetition than I'd like here, in large part because
   there's no way to introduce different numbers of hypotheses when doing the
   case distinctions. *)

nlemma bool_of_val_1_ok : ∀v,ty,r. bool_of_val_1 v ty = OK ? r ↔ bool_of_val v ty r.
#v ty r; @;
##[
  nelim v; ##[ #H; nnormalize in H; ndestruct; ##| ##2,3: #x; ##| ##4: #x y; ##]
  ncases ty;
  ##[ ##1,10,19: #H; nnormalize in H; ndestruct;
  ##| #i s; nwhd in ⊢ (??%? → ?); nelim (eq_dec x zero); #H;
    ##[ nrewrite > H; nrewrite > (eq_true …); #H';
        ncut (r = Vfalse); ##[ nwhd in H':(??(??%)?); ndestruct;//;##]
        #H''; nrewrite > H''; /2/;
    ##| nrewrite > (eq_false …); //; #H';
        ncut (r = Vtrue); ##[ nwhd in H':(??(??%)?); ndestruct;//;##]
        #H''; nrewrite > H''; /3/;
    ##]
  ##|##3,9,13,18,21,27: #x H; nnormalize in H; ndestruct;
  ##| #t; nwhd in ⊢ (??%? → ?); nelim (eq_dec x zero); #H;
    ##[ nrewrite > H; nrewrite > (eq_true …); #H';
        ncut (r = Vfalse); ##[ nwhd in H':(??(??%)?); ndestruct;//;##]
        #H''; nrewrite > H''; /2/;
    ##| nrewrite > (eq_false …); //; #H';
        ncut (r = Vtrue); ##[ nwhd in H':(??(??%)?); ndestruct;//;##]
        #H''; nrewrite > H''; /3/;
    ##]
  ##| ##5,6,7,8,11,14,15,16,17,23,24,25,26: #a b H; nnormalize in H; ndestruct;
  ##| #f; nwhd in ⊢ (??%? → ?); nelim (eq_dec x Fzero); #H;
    ##[ nrewrite > H; nrewrite > (Feq_zero_true …); #H';
        ncut (r = Vfalse); ##[ nwhd in H':(??(??%)?); ndestruct;//;##]
        #H''; nrewrite > H''; /2/;
    ##| nrewrite > (Feq_zero_false …); //; #H';
        ncut (r = Vtrue); ##[ nwhd in H':(??(??%)?); ndestruct;//;##]
        #H''; nrewrite > H''; /3/;
    ##]
  ##| #i s H; nwhd in H:(??%?);
      ncut (r = Vtrue); ##[ nwhd in H:(??(??%)?); ndestruct;//;##]
      #H'; nrewrite > H'; /2/;
  ##| #t H; nwhd in H:(??%?);
      ncut (r = Vtrue); ##[ nwhd in H:(??(??%)?); ndestruct;//;##]
      #H'; nrewrite > H'; /2/;
  ##]
##| #H; nelim H; #v t H'; nelim H';
  ##[ #i is s ne; nwhd in ⊢ (??%?); nrewrite > (eq_false … ne); //;
  ##| ##2,4: //
  ##| #i t ne; nwhd in ⊢ (??%?); nrewrite > (eq_false … ne); //;
  ##| #f s ne; nwhd in ⊢ (??%?); nrewrite > (Feq_zero_false … ne); //;
  ##| #i s; nwhd in ⊢ (??%?); nrewrite > (eq_true …); //;
  ##| #t; nwhd in ⊢ (??%?); nrewrite > (eq_true …); //;
  ##| #s; nwhd in ⊢ (??%?); nrewrite > (Feq_zero_true …); //;
  ##]
##] nqed.

include "Plogic/russell_support.ma".

(* Nicer - we still have to deal with all of the cases, but only need to
   introduce the result value, so there's a single case for getting rid of
   all the Error goals. *)

ndefinition bool_of_val_2 : ∀v:val. ∀ty:type. { r : res bool | ∀r'. r = OK ? r' → bool_of_val v ty (of_bool r') } ≝
  λv,ty. match v in val with
  [ Vint i ⇒ match ty with
    [ Tint _ _ ⇒ Some ? (OK ? (¬eq i zero))
    | Tpointer _ ⇒ Some ? (OK ? (¬eq i zero))
    | _ ⇒ Some ? (Error ?)
    ]
  | Vfloat f ⇒ match ty with
    [ Tfloat _ ⇒ Some ? (OK ? (¬Fcmp Ceq f Fzero))
    | _ ⇒ Some ? (Error ?)
    ]
  | Vptr _ _ ⇒ match ty with
    [ Tint _ _ ⇒ Some ? (OK ? true)
    | Tpointer _ ⇒ Some ? (OK ? true)
    | _ ⇒ Some ? (Error ?)
    ]
  | _ ⇒ Some ? (Error ?)
  ]. nwhd;
##[ ##3,5: #r; nlapply (eq_spec c0 zero); nelim (eq c0 zero);
  ##[ ##1,3: #e H; nrewrite > (?:of_bool r=Vfalse); ##[ ##2,4: ndestruct; // ##] nrewrite > e; /3/;
  ##| ##2,4: #ne H; nrewrite > (?:of_bool r=Vtrue);  ##[ ##2,4: ndestruct; // ##] /3/;
  ##]
##| ##13: #r; nelim (eq_dec c0 Fzero);
  ##[ #e; nrewrite > e; nrewrite > (Feq_zero_true …); #H; nrewrite > (?:of_bool r=Vfalse); ##[ ##2: ndestruct; // ##] /2/;
  ##| #ne; nrewrite > (Feq_zero_false …); //; #H;
      nrewrite > (?:of_bool r=Vtrue);  ##[ ##2: ndestruct; // ##] /3/;
  ##]
##| ##21,23: #r H; nrewrite > (?:of_bool r = Vtrue); ##[ ##2,4: ndestruct; // ##] /2/
##| ##*: #a b; ndestruct;
##] nqed.

(* Same as before, except we have to write eject in because the type for the 
   equality is left implied, so the coercion isn't used. *)

nlemma bool_of_val_2_complete : ∀v,ty,r.
  bool_of_val v ty r →
  ∃b. r = of_bool b ∧ eject ?? (bool_of_val_2 v ty) = OK ? b.
#v ty r H; nelim H; #v t H'; nelim H';
  ##[ #i is s ne; @ true; @; //; nwhd in ⊢ (??%?); nrewrite > (eq_false … ne); //;
  ##| #b i i0 s; @ true; @; //
  ##| #i t ne; @ true; @; //; nwhd in ⊢ (??%?); nrewrite > (eq_false … ne); //;
  ##| #b i t0; @ true; @; //
  ##| #f s ne; @ true; @; //; nwhd in ⊢ (??%?); nrewrite > (Feq_zero_false … ne); //;
  ##| #i s; @ false; @; //; nwhd in ⊢ (??%?); nrewrite > (eq_true …); //;
  ##| #t; @ false; @; //; nwhd in ⊢ (??%?); nrewrite > (eq_true …); //;
  ##| #s; @ false; @; //; nwhd in ⊢ (??%?); nrewrite > (Feq_zero_true …); //;
  ##]
nqed.


(* Nicer again (after the extra definitions).  Just use sigma type rather than
   the subset, but take into account the error monad.  The error cases all
   become trivial and we don't have to muck around to get the result. *)

ndefinition P_to_P_option_res : ∀A:Type[0].∀P:A → CProp[0].option (res A) → CProp[0] ≝
  λA,P,a.match a with [ None ⇒ False | Some y ⇒ match y return λ_.CProp[0] with [ Error ⇒ True | OK z ⇒ P z ]].

ndefinition err_inject : ∀A.∀P:A → Prop.∀a:option (res A).∀p:P_to_P_option_res A P a.res (sigma A P) ≝ 
  λA.λP:A → Prop.λa:option (res A).λp:P_to_P_option_res A P a. 
  (match a return λa'.a=a' → res (sigma A P) with
   [ None ⇒ λe1.?
   | Some b ⇒ λe1.(match b return λb'.b=b' → ? with
     [ Error ⇒ λ_. Error ?
     | OK c ⇒ λe2. OK ? (sig_intro A P c ?)
     ]) (refl ? b)
   ]) (refl ? a).
##[ nrewrite > e1 in p; nnormalize; *;
##| nrewrite > e1 in p; nrewrite > e2; nnormalize; //
##] nqed.

ndefinition err_eject : ∀A.∀P: A → Prop. res (sigma A P) → res A ≝ 
  λA,P,a.match a with [ Error ⇒ Error ? | OK b ⇒
    match b with [ sig_intro w p ⇒ OK ? w] ].

ndefinition sig_eject : ∀A.∀P: A → Prop. sigma A P → A ≝ 
  λA,P,a.match a with [ sig_intro w p ⇒ w].

ncoercion err_inject : 
  ∀A.∀P:A → Prop.∀a.∀p:P_to_P_option_res ? P a.res (sigma A P) ≝ err_inject 
  on a:option (res ?) to res (sigma ? ?).
ncoercion err_eject : ∀A.∀P:A → Prop.∀c:res (sigma A P).res A ≝ err_eject 
  on _c:res (sigma ? ?) to res ?.
ncoercion sig_eject : ∀A.∀P:A → Prop.∀c:sigma A P.A ≝ sig_eject 
  on _c:sigma ? ? to ?.

ndefinition bool_of_val_3 : ∀v:val. ∀ty:type. res (Σr:bool. bool_of_val v ty (of_bool r)) ≝
  λv,ty. match v in val with
  [ Vint i ⇒ match ty with
    [ Tint _ _ ⇒ Some ? (OK ? (¬eq i zero))
    | Tpointer _ ⇒ Some ? (OK ? (¬eq i zero))
    | _ ⇒ Some ? (Error ?)
    ]
  | Vfloat f ⇒ match ty with
    [ Tfloat _ ⇒ Some ? (OK ? (¬Fcmp Ceq f Fzero))
    | _ ⇒ Some ? (Error ?)
    ]
  | Vptr _ _ ⇒ match ty with
    [ Tint _ _ ⇒ Some ? (OK ? true)
    | Tpointer _ ⇒ Some ? (OK ? true)
    | _ ⇒ Some ? (Error ?)
    ]
  | _ ⇒ Some ? (Error ?)
  ]. nwhd; //;
##[ ##1,2: nlapply (eq_spec c0 zero); nelim (eq c0 zero);
  ##[ ##1,3: #e; nrewrite > e; napply bool_of_val_false; //;
  ##| ##2,4: #ne; napply bool_of_val_true; /2/;
  ##]
##| nelim (eq_dec c0 Fzero);
  ##[ #e; nrewrite > e; nrewrite > (Feq_zero_true …); napply bool_of_val_false; //;
  ##| #ne; nrewrite > (Feq_zero_false …); //; napply bool_of_val_true; /2/;
  ##]
##| ##4,5: napply bool_of_val_true; //
##] nqed.

ndefinition err_eq ≝ λA,P. λx:res (sigma A P). λy:A.
  match x with [ Error ⇒ False | OK x' ⇒
    match x' with [ sig_intro x'' _ ⇒ x'' = y ]].
(* TODO: can I write a coercion for the above? *)

(* Same as before, except we have to use a slightly different "equality". *)

nlemma bool_of_val_3_complete : ∀v,ty,r. bool_of_val v ty r → ∃b. r = of_bool b ∧ err_eq ?? (bool_of_val_3 v ty) b.
#v ty r H; nelim H; #v t H'; nelim H';
  ##[ #i is s ne; @ true; @; //; nwhd; nrewrite > (eq_false … ne); //;
  ##| #b i i0 s; @ true; @; //
  ##| #i t ne; @ true; @; //; nwhd; nrewrite > (eq_false … ne); //;
  ##| #b i t0; @ true; @; //
  ##| #f s ne; @ true; @; //; nwhd; nrewrite > (Feq_zero_false … ne); //;
  ##| #i s; @ false; @; //; nwhd; nrewrite > (eq_true …); //;
  ##| #t; @ false; @; //; nwhd; nrewrite > (eq_true …); //;
  ##| #s; @ false; @; //; nwhd; nrewrite > (Feq_zero_true …); //;
  ##]
nqed.

(* Prove a few minor results to make proof obligations easy. *)

nlemma bind_OK: ∀A,B,P,e,f.
  (∀v. e = OK A v → match f v with [ Error ⇒ True | OK v' ⇒ P v' ]) →
  match bind A B e f with [ Error ⇒ True | OK v ⇒ P v ].
#A B P e f; nelim e; /2/; nqed.

nlemma sig_bind_OK: ∀A,B. ∀P:A → Prop. ∀P':B → Prop. ∀e:res (sigma A P). ∀f:sigma A P → res B.
  (∀v:A. err_eq A P e v → ∀p:P v. match f (sig_intro A P v p) with [ Error ⇒ True | OK v' ⇒ P' v'] ) →
  match bind (sigma A P) B e f with [ Error ⇒ True | OK v' ⇒ P' v' ].
#A B P P' e f; nelim e; //;
#v0; nelim v0; #v Hv IH; napply IH; //; nqed.

nlemma bind2_OK: ∀A,B,C,P,e,f.
  (∀v1,v2. e = OK ? 〈v1,v2〉 → match f v1 v2 with [ Error ⇒ True | OK v' ⇒ P v' ]) →
  match bind2 A B C e f with [ Error ⇒ True | OK v ⇒ P v ].
#A B C P e f; nelim e; //; #v; ncases v; /2/; nqed.

nlemma sig_bind2_OK: ∀A,B,C. ∀P:A×B → Prop. ∀P':C → Prop. ∀e:res (sigma (A×B) P). ∀f:A → B → res C.
  (∀v1:A.∀v2:B. P 〈v1,v2〉 → match f v1 v2 with [ Error ⇒ True | OK v' ⇒ P' v'] ) →
  match bind2 A B C e f with [ Error ⇒ True | OK v' ⇒ P' v' ].
#A B C P P' e f; nelim e; //;
#v0; nelim v0; #v; nelim v; #v1 v2 Hv IH; napply IH; //; nqed.

nlemma reinject: ∀A. ∀P,P':A → Prop. ∀e:res (sigma A P').
  (∀v:A. err_eq A P' e v → P' v → P v) →
  match err_eject A P' e with [ Error ⇒ True | OK v' ⇒ P v' ].
#A P P' e; ncases e; //;
#v0; nelim v0; #v Pv' IH; /2/;
nqed.

nlemma bool_val_distinct: Vtrue ≠ Vfalse.
@; #H; nwhd in H:(??%%); ndestruct; napply (absurd ? e0 one_not_zero);
nqed.

nlemma bool_of: ∀v,ty,b. bool_of_val v ty (of_bool b) →
  if b then is_true v ty else is_false v ty.
#v ty b; ncases b; #H; ninversion H; #v' ty' H' ev et ev; //;
napply False_ind; napply (absurd ? ev ?);
##[ ##2: napply sym_neq ##] napply bool_val_distinct;
nqed.

ndefinition opt_to_res ≝ λA.λv:option A. match v with [ None ⇒ Error A | Some v ⇒ OK A v ].
nlemma opt_OK: ∀A,P,e.
  (∀v. e = Some ? v → P v) →
  match opt_to_res A e with [ Error ⇒ True | OK v ⇒ P v ].
#A P e; nelim e; /2/;
nqed.

nlemma opt_bind_OK: ∀A,B,P,e,f.
  (∀v. e = Some A v → match f v with [ Error ⇒ True | OK v' ⇒ P v' ]) →
  match bind A B (opt_to_res A e) f with [ Error ⇒ True | OK v ⇒ P v ].
#A B P e f; nelim e; nnormalize; /2/; nqed.

nlemma extract_subset_pair: ∀A,B,C,P. ∀e:{e:A×B | P e}. ∀Q:A→B→res C. ∀R:C→Prop.
  (∀a,b. eject ?? e = 〈a,b〉 → P 〈a,b〉 → match Q a b with [ OK v ⇒ R v | Error ⇒ True]) →
  match match eject ?? e with [ mk_pair a b ⇒ Q a b ] with [ OK v ⇒ R v | Error ⇒ True ].
#A B C P e Q R; ncases e; #e'; ncases e'; nnormalize;
##[ #H; napply (False_ind … H);
##| #e''; ncases e''; #a b Pab H; nnormalize; /2/;
##] nqed.

(* To make the evaluation of bare lvalue expressions invoke exec_lvalue with
   a structurally smaller value, we break out the surrounding Expr constructor
   and use exec_lvalue'. *)

nlet rec exec_expr (ge:genv) (en:env) (m:mem) (e:expr) on e : res (Σr:val. eval_expr ge en m e r) ≝
match e with
[ Expr e' ty ⇒
  match e' with
  [ Econst_int i ⇒ Some ? (OK ? (Vint i))
  | Evar _ ⇒ Some ? (
      〈loc, ofs〉 ← exec_lvalue' ge en m e' ty;:
      opt_to_res ? (load_value_of_type ty m loc ofs))
  | Eaddrof a ⇒ Some ? (
      〈loc, ofs〉 ← exec_lvalue ge en m a;:
      OK ? (Vptr loc ofs))
  | Eunop op a ⇒ Some ? (
      v1 ← exec_expr ge en m a;:
      opt_to_res ? (sem_unary_operation op v1 (typeof a)))
  | Econdition a1 a2 a3 ⇒ Some ? (
      v ← exec_expr ge en m a1;:
      b ← bool_of_val_3 v (typeof a1);:
      match b return λ_.res val with [ true ⇒ (exec_expr ge en m a2) | false ⇒ (exec_expr ge en m a3) ])
(*      if b then exec_expr ge en m a2 else exec_expr ge en m a3)*)
  | _ ⇒ Some ? (Error ?)
  ]
]
and exec_lvalue' (ge:genv) (en:env) (m:mem) (e':expr_descr) (ty:type) on e' : res (Σr:block × int. eval_lvalue ge en m (Expr e' ty) (\fst r) (\snd r)) ≝
  match e' with
  [ Evar id ⇒ Some ? (
      l ← opt_to_res ? (get ? PTree ? id en);:
      OK ? 〈l, zero〉)
  | _ ⇒ Some ? (Error ?)
  ]
and exec_lvalue (ge:genv) (en:env) (m:mem) (e:expr) on e : res (Σr:block × int. eval_lvalue ge en m e (\fst r) (\snd r)) ≝
match e with [ Expr e' ty ⇒ exec_lvalue' ge en m e' ty ].
nwhd; //;
##[ napply sig_bind2_OK; nrewrite > c2; nrewrite > c4; #loc ofs H;
    napply opt_OK;  #v ev; /2/;
##| napply sig_bind2_OK; #loc ofs H;
    nwhd; napply eval_Eaddrof; //;
##| napply sig_bind_OK; #v1 ev1 Hv1;
    napply opt_OK; #v ev;
    napply (eval_Eunop … Hv1 ev);
##| napply sig_bind_OK; #vb evb Hvb;
    napply sig_bind_OK; #b;
    ncases b; #eb Hb; napply reinject; #v ev Hv;
    ##[ napply (eval_Econdition_true … Hvb ? Hv);  napply (bool_of ??? Hb);
    ##| napply (eval_Econdition_false … Hvb ? Hv);  napply (bool_of ??? Hb);
    ##]
##| napply opt_bind_OK; #l el; napply eval_Evar_local; // 
##] nqed.

(* Don't really want to use subset rather than sigma here, but can't be bothered
   with *another* set of coercions. XXX: why do I have to get the recursive
   call's property manually? *)

nlet rec exec_alloc_variables (en:env) (m:mem) (l:list (ident × type)) on l : { r:env × mem | alloc_variables en m l (\fst r) (\snd r) } ≝
match l with
[ nil ⇒ Some ? 〈en, m〉
| cons h vars ⇒
  match h with [ mk_pair id ty ⇒
    match alloc m 0 (sizeof ty) with [ mk_pair m1 b1 ⇒
      match exec_alloc_variables (set ? PTree ? id b1 en) m1 vars with
      [ sig_intro r p ⇒ r ]
]]]. nwhd; //;
nelim (exec_alloc_variables (set ident PTree block c3 c7 en) c6 c1);
#H; nelim H; //; #H0; nelim H0; nnormalize; #en' m' IH;
napply (alloc_variables_cons … IH); /2/;
nqed.

(* TODO: can we establish that length params = length vs in advance? *)
nlet rec exec_bind_parameters (e:env) (m:mem) (params:list (ident × type)) (vs:list val) on params : res (Σm2:mem. bind_parameters e m params vs m2) ≝
  match params with
  [ nil ⇒ match vs with [ nil ⇒ Some ? (OK ? m) | cons _ _ ⇒ Some ? (Error ?) ]
  | cons idty params' ⇒ match idty with [ mk_pair id ty ⇒
      match vs with
      [ nil ⇒ Some ? (Error ?)
      | cons v1 vl ⇒ Some ? (
          b ← opt_to_res ? (get ? PTree ? id e);:
          m1 ← opt_to_res ? (store_value_of_type ty m b zero v1);:
          err_eject ?? (exec_bind_parameters e m1 params' vl)) (* FIXME: don't want to have to eject here *)
      ]
  ] ].
nwhd; //;
napply opt_bind_OK; #b eb;
napply opt_bind_OK; #m1 em1;
napply reinject; #m2 em2 Hm2;
napply (bind_parameters_cons … eb em1 Hm2);
nqed.

ndefinition is_not_void : ∀t:type. res (Σu:unit. t ≠ Tvoid) ≝
λt. match t with
[ Tvoid ⇒ Some ? (Error ?)
| _ ⇒ Some ? (OK ??)
]. nwhd; //; @; #H; ndestruct; nqed.

nlet rec exec_step (ge:genv) (st:state) on st : res (Σr:trace × state. step ge st (\fst r) (\snd r)) ≝
match st with
[ State f s k e m ⇒
  match s with
  [ Sassign a1 a2 ⇒ Some ? (
    〈loc, ofs〉 ← exec_lvalue ge e m a1;:
    v2 ← exec_expr ge e m a2;:
    m' ← opt_to_res ? (store_value_of_type (typeof a1) m loc ofs v2);:
    OK ? 〈E0, State f Sskip k e m'〉)
  | Sreturn a_opt ⇒
    match a_opt with
    [ None ⇒ match fn_return f with
      [ Tvoid ⇒ Some ? (OK ? 〈E0, Returnstate Vundef (call_cont k) (free_list m (blocks_of_env e))〉)
      | _ ⇒ Some ? (Error ?)
      ]
    | Some a ⇒ Some ? (
        u ← is_not_void (fn_return f);:
        v ← exec_expr ge e m a;:
        OK ? 〈E0, Returnstate v (call_cont k) (free_list m (blocks_of_env e))〉)
    ]
  | _ ⇒ Some ? (Error ?)
  ]
| Callstate f0 vargs k m ⇒
  match f0 with
  [ Internal f ⇒ Some ? (
    match exec_alloc_variables empty_env m ((fn_params f) @ (fn_vars f)) with [ mk_pair e m1 ⇒
      m2 ← exec_bind_parameters e m1 (fn_params f) vargs;:
      OK ? 〈E0, State f (fn_body f) k e m2〉
    ])
  | _ ⇒ Some ? (Error ?)
  ]
| _ ⇒ Some ? (Error ?)
]. nwhd; //;
##[ napply sig_bind2_OK; #loc ofs Hlval;
    napply sig_bind_OK; #v2 ev2 Hv2;
    napply opt_bind_OK; #m' em';
    nwhd; napply (step_assign … Hlval Hv2 em');
##| napply step_return_0; napply c9;
##| napply sig_bind_OK; #u eu Hnotvoid;
    napply sig_bind_OK; #v ev Hv;
    nwhd; napply (step_return_1 … Hnotvoid Hv);
##| napply extract_subset_pair; #e m1 ealloc Halloc;
    napply sig_bind_OK; #m2 em1 Hbind;
    nwhd; napply (step_internal_function … Halloc Hbind);
##]
nqed.

nlet rec make_initial_state (p:program) : res (Σs:state. initial_state p s) ≝
  let ge ≝ globalenv Genv ?? p in
  let m0 ≝ init_mem Genv ?? p in
  Some ? (
    b ← opt_to_res ? (find_symbol Genv ? ge (prog_main ?? p));:
    f ← opt_to_res ? (find_funct_ptr Genv ? ge b);:
    OK ? (Callstate f (nil ?) Kstop m0)).
nwhd;
napply opt_bind_OK; #b eb;
napply opt_bind_OK; #f ef;
nwhd; napply (initial_state_intro … eb ef);
nqed.