source: C-semantics/CexecIO.ma @ 82

include "Csem.ma".

include "extralib.ma".
include "IOMonad.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_assoc_r: ∀A,B,C,e,f,g.
  bind B C (bind A B e f) g = bind A C e (λx.bind B C (f x) g).
#A B C e f g; ncases e; nnormalize; //; nqed.

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.

nlet rec is_neutral_cast (ty:type) : res (Σu:unit.neutral_for_cast ty) ≝
match ty with
[ Tint sz _ ⇒ match sz with [ I32 ⇒ Some ? (OK ? something) | _ ⇒ Some ? (Error ?) ]
| Tpointer _ ⇒ Some ? (OK ? something)
| Tarray _ _ ⇒ Some ? (OK ? something)
| Tfunction _ _ ⇒ Some ? (OK ? something)
| _ ⇒ Some ? (Error ?)
]. nwhd; //; nqed.
(*
nremark err_later: ∀A,B. ∀e:res A. match e with [ Error ⇒ Error B | OK v ⇒ Error B ] = Error B.
#A B e; ncases e; //; nqed.
*)

nlet rec exec_cast (v:val) (ty:type) (ty':type) : res (Σv':val. cast v ty ty' v') ≝
match v with
[ Vint i ⇒
  match ty with
  [ Tint sz1 si1 ⇒
    match ty' with
    [ Tint sz2 si2 ⇒ Some ? (OK ? (Vint (cast_int_int sz2 si2 i)))
    | Tfloat sz2 ⇒ Some ? (OK ? (Vfloat (cast_float_float sz2 (cast_int_float si1 i))))
    (* no change in data repr *)
    | _ ⇒ Some ? (u ← is_neutral_cast ty;: u' ← is_neutral_cast ty';: OK ? (Vint i))
    ]
  | _ ⇒ Some ? (u ← is_neutral_cast ty;: u' ← is_neutral_cast ty';: OK ? (Vint i))
  ]
| Vfloat f ⇒
  match ty with
  [ Tfloat sz ⇒
    match ty' with
    [ Tint sz' si' ⇒ Some ? (OK ? (Vint (cast_int_int sz' si' (cast_float_int si' f))))
    | Tfloat sz' ⇒ Some ? (OK ? (Vfloat (cast_float_float sz' f)))
    | _ ⇒ Some ? (Error ?)
    ]
  | _ ⇒ Some ? (Error ?)
  ]
| Vptr b ofs ⇒ Some ? (u ← is_neutral_cast ty;: u' ← is_neutral_cast ty';: OK ? (Vptr b ofs))
| _ ⇒ Some ? (Error ?)
]. ndestruct; /2/;
##[ ##1,2,3: ncases c2; //; napply cast_nn_i; //
##| ##4,5,6: napply sig_bind_OK; #u;#_;#H; napply cast_nn_i; //;
##| napply sig_bind_OK; #u;#_;#H; napply sig_bind_OK; #u';#_;#H';
    napply cast_nn_p; //
##] 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))
  | Econst_float f ⇒ Some ? (OK ? (Vfloat f))
  | Evar _ ⇒ Some ? (
      〈loc, ofs〉 ← exec_lvalue' ge en m e' ty;:
      opt_to_res ? (load_value_of_type ty m loc ofs))
  | Ederef _ ⇒ Some ? (
      〈loc, ofs〉 ← exec_lvalue' ge en m e' ty;:
      opt_to_res ? (load_value_of_type ty m loc ofs))
  | Efield _ _ ⇒ 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))
  | Esizeof ty' ⇒ Some ? (OK ? (Vint (repr (sizeof ty'))))
  | Eunop op a ⇒ Some ? (
      v1 ← exec_expr ge en m a;:
      opt_to_res ? (sem_unary_operation op v1 (typeof a)))
  | Ebinop op a1 a2 ⇒ Some ? (
      v1 ← exec_expr ge en m a1;:
      v2 ← exec_expr ge en m a2;:
      opt_to_res ? (sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m))
  | 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)*)
  | Eorbool a1 a2 ⇒ Some ? (
      v1 ← exec_expr ge en m a1;:
      b1 ← bool_of_val_3 v1 (typeof a1);:
      match b1 return λ_.res val with [ true ⇒ OK ? Vtrue | false ⇒
        v2 ← exec_expr ge en m a2;:
        b2 ← bool_of_val_3 v2 (typeof a2);:
        OK ? (of_bool b2) ])
  | Eandbool a1 a2 ⇒ Some ? (
      v1 ← exec_expr ge en m a1;:
      b1 ← bool_of_val_3 v1 (typeof a1);:
      match b1 return λ_.res val with [ true ⇒
        v2 ← exec_expr ge en m a2;:
        b2 ← bool_of_val_3 v2 (typeof a2);:
        OK ? (of_bool b2)
      | false ⇒ OK ? Vfalse ])
  | Ecast ty' a ⇒ Some ? (
      v ← exec_expr ge en m a;:
      exec_cast v (typeof a) ty')
  ]
]
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 ⇒ 
      match (get … id en) with
      [ None ⇒ Some ? (l ← opt_to_res ? (find_symbol ? ? ge id);: OK ? 〈l,zero〉) (* global *)
      | Some l ⇒ Some ? (OK ? 〈l,zero〉) (* local *)
      ]
  | Ederef a ⇒ Some ? (
      v ← exec_expr ge en m a;:
      match v with
      [ Vptr l ofs ⇒ OK ? 〈l,ofs〉
      | _ ⇒ Error ?
      ])
  | Efield a i ⇒
      match (typeof a) with
      [ Tstruct id fList ⇒ Some ? (
          〈l,ofs〉 ← exec_lvalue ge en m a;:
          delta ← field_offset i fList;:
          OK ? 〈l,add ofs (repr delta)〉)
      | Tunion id fList ⇒ Some ? (
          〈l,ofs〉 ← exec_lvalue ge en m a;:
          OK ? 〈l,ofs〉)
      | _ ⇒ Some ? (Error ?)
      ]
  | _ ⇒ 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 > c4; #loc ofs H;
    napply opt_OK;  #v ev; /2/;
##| napply sig_bind2_OK; 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; #v1 ev1 Hv1;
    napply sig_bind_OK; #v2 ev2 Hv2;
    napply opt_OK; #v ev;
    napply (eval_Ebinop … Hv1 Hv2 ev);
##| napply sig_bind_OK; #v ev Hv;
    napply sig_bind_OK; #v' ev' Hv';
    napply (eval_Ecast … Hv Hv');
##| 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 sig_bind_OK; #v1 ev1 Hv1;
    napply sig_bind_OK; #b1; ncases b1; #eb1 Hb1;
    ##[ napply sig_bind_OK; #v2 ev2 Hv2;
        napply sig_bind_OK; #b2 eb2 Hb2; 
        napply (eval_Eandbool_2 … Hv1 … Hv2);
        ##[ napply (bool_of … Hb1); ##| napply Hb2; ##]
    ##| napply (eval_Eandbool_1 … Hv1); napply (bool_of … Hb1);
    ##]
##| napply sig_bind_OK; #v1 ev1 Hv1;
    napply sig_bind_OK; #b1; ncases b1; #eb1 Hb1;
    ##[ napply (eval_Eorbool_1 … Hv1); napply (bool_of … Hb1);
    ##| napply sig_bind_OK; #v2 ev2 Hv2;
        napply sig_bind_OK; #b2 eb2 Hb2; 
        napply (eval_Eorbool_2 … Hv1 … Hv2);
        ##[ napply (bool_of … Hb1); ##| napply Hb2; ##]
    ##]
##| napply sig_bind2_OK; nrewrite > c5; #l ofs H;
    napply opt_OK; #v ev; /2/;
##| napply opt_bind_OK; #l el; napply eval_Evar_global; /2/;
##| napply eval_Evar_local; /2/
##| napply sig_bind_OK; #v; ncases v; //; #l ofs ev Hv; nwhd;
    napply eval_Ederef; //
##| napply sig_bind2_OK; #l ofs H;
    napply bind_OK; #delta Hdelta;
    napply (eval_Efield_struct … H c5 Hdelta);
##| napply sig_bind2_OK; #l ofs H;
    napply (eval_Efield_union … H c5);
##] nqed.

(* TODO: Can we do this sensibly with a map combinator? *)
nlet rec exec_exprlist (ge:genv) (e:env) (m:mem) (l:list expr) on l : res (Σvl:list val. eval_exprlist ge e m l vl) ≝
match l with
[ nil ⇒ Some ? (OK ? (nil val))
| cons e1 es ⇒ Some ? (
  v ← exec_expr ge e m e1;:
  vs ← exec_exprlist ge e m es;:
  OK ? (cons val v vs))
]. nwhd; //;
napply sig_bind_OK; #v ev Hv;
napply sig_bind_OK; #vs evs Hvs;
nnormalize; /2/;
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 … id b1 en) m1 vars with
      [ sig_intro r p ⇒ r ]
]]]. nwhd; //;
nelim (exec_alloc_variables (set ident ? 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 … 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.

ninductive decide : Type ≝
| dy : decide | dn : decide.

ndefinition dodecide : ∀P:Prop.∀d.∀p:(match d with [ dy ⇒ P | dn ⇒ ¬P ]).P + ¬P.
#P d;ncases d;/2/; nqed.

ncoercion decide_inject :
  ∀P:Prop.∀d.∀p:(match d with [ dy ⇒ P | dn ⇒ ¬P ]).P + ¬P ≝ dodecide
  on d:decide to ? + (¬?).

ndefinition dodecide2 : ∀P:Prop.∀d.∀p:(match d with [ dy ⇒ P | dn ⇒ True ]).res P.
#P d; ncases d; nnormalize; #p; ##[ napply (OK ? p); ##| napply Error ##] nqed. 

ncoercion decide_inject2 :
  ∀P:Prop.∀d.∀p:(match d with [ dy ⇒ P | dn ⇒ True ]).res P ≝ dodecide2
  on d:decide to res ?.

alias id "Tint" = "cic:/matita/c-semantics/Csyntax/type.con(0,2,0)".
alias id "Tfloat" = "cic:/matita/c-semantics/Csyntax/type.con(0,3,0)".
ndefinition sz_eq_dec : ∀s1,s2:intsize. (s1 = s2) + (s1 ≠ s2).
#s1; ncases s1; #s2; ncases s2; /2/; @2; @; #H; ndestruct; nqed.
ndefinition sg_eq_dec : ∀s1,s2:signedness. (s1 = s2) + (s1 ≠ s2).
#s1; ncases s1; #s2; ncases s2; /2/; @2; @; #H; ndestruct; nqed.
ndefinition fs_eq_dec : ∀s1,s2:floatsize. (s1 = s2) + (s1 ≠ s2).
#s1; ncases s1; #s2; ncases s2; /2/; @2; @; #H; ndestruct; nqed.

nlet rec assert_type_eq (t1,t2:type) : res (t1 = t2) ≝
match t1 with
[ Tvoid ⇒ match t2 with [ Tvoid ⇒ dy | _ ⇒ dn ]
| Tint sz sg ⇒ match t2 with [ Tint sz' sg' ⇒ match sz_eq_dec sz sz' with [ inl _ ⇒ match sg_eq_dec sg sg' with [ inl _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ] | _ ⇒ dn ]
| Tfloat f ⇒ match t2 with [ Tfloat f' ⇒ match fs_eq_dec f f' with [ inl _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ]
| Tpointer t ⇒ match t2 with [ Tpointer t' ⇒ match assert_type_eq t t' with [ OK _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ]
| Tarray t n ⇒ match t2 with [ Tarray t' n' ⇒
    match assert_type_eq t t' with [ OK _ ⇒
      match decidable_eq_Z_Type n n' with [ inl _ ⇒ dy | inr _ ⇒ dn ] | _ ⇒ dn ] | _ ⇒ dn ]
| Tfunction tl t ⇒ match t2 with [ Tfunction tl' t' ⇒ match assert_typelist_eq tl tl' with [ OK _ ⇒ 
    match assert_type_eq t t' with [ OK _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ] | _ ⇒ dn ]
| Tstruct i fl ⇒
    match t2 with [ Tstruct i' fl' ⇒ match ident_eq i i' with [ inl _ ⇒
      match assert_fieldlist_eq fl fl' with [ OK _ ⇒ dy | _ ⇒ dn ] | inr _ ⇒ dn ] |  _ ⇒ dn ]
| Tunion i fl ⇒
    match t2 with [ Tunion i' fl' ⇒ match ident_eq i i' with [ inl _ ⇒
      match assert_fieldlist_eq fl fl' with [ OK _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ] |  _ ⇒ dn ]
| Tcomp_ptr i ⇒ match t2 with [ Tcomp_ptr i' ⇒ match ident_eq i i' with [ inl _ ⇒ dy | inr _ ⇒ dn ] | _ ⇒ dn ]
]
and assert_typelist_eq (tl1,tl2:typelist) : res (tl1 = tl2) ≝
match tl1 with
[ Tnil ⇒ match tl2 with [ Tnil ⇒ dy | _ ⇒ dn ]
| Tcons t1 ts1 ⇒ match tl2 with [ Tnil ⇒ dn | Tcons t2 ts2 ⇒ 
    match assert_type_eq t1 t2 with [ OK _ ⇒
      match assert_typelist_eq ts1 ts2 with [ OK _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ] ]
]
and assert_fieldlist_eq (fl1,fl2:fieldlist) : res (fl1 = fl2) ≝
match fl1 with
[ Fnil ⇒ match fl2 with [ Fnil ⇒ dy | _ ⇒ dn ]
| Fcons i1 t1 fs1 ⇒ match fl2 with [ Fnil ⇒ dn | Fcons i2 t2 fs2 ⇒ 
    match ident_eq i1 i2 with [ inl _ ⇒
      match assert_type_eq t1 t2 with [ OK _ ⇒
        match assert_fieldlist_eq fs1 fs2 with [ OK _ ⇒ dy | _ ⇒ dn ]
        | _ ⇒ dn ] | _ ⇒ dn ] ]
].
(* A poor man's clear, otherwise automation picks up recursive calls without
   checking that the argument is smaller. *)
ngeneralize in assert_type_eq;
ngeneralize in assert_typelist_eq;
ngeneralize in assert_fieldlist_eq; #avoid1; #_; #avoid2; #_; #avoid3; #_; nwhd; //;
(* XXX: I have no idea why the first // didn't catch these. *)
//; //; //; //; //; //; //; //; //;
nqed.

nlet rec is_is_call_cont (k:cont) : (is_call_cont k) + (¬is_call_cont k) ≝
match k with
[ Kstop ⇒ dy
| Kcall _ _ _ _ ⇒ dy
| _ ⇒ dn
]. nwhd; //; @; #H; nelim H; nqed.

nlet rec is_Sskip (s:statement) : (s = Sskip) + (s ≠ Sskip) ≝
match s with
[ Sskip ⇒ dy
| _ ⇒ dn
].
##[ //;
##| ##*: @; #H; ndestruct;
##] nqed.

(* IO monad *)

(* Interactions are function calls that return a value and do not change
   the rest of the Clight program's state. *)
ndefinition io_out ≝ (ident × (list eventval)).

ndefinition do_io : ident → list eventval → IO eventval io_out eventval ≝
λfn,args. Interact ?? eventval 〈fn,args〉 (λres. Value ?? eventval res).

ndefinition ret: ∀T. T → (IO eventval io_out T) ≝
λT,x.(Value ?? T x).

(* Checking types of values given to / received from an external function call. *)

ndefinition check_eventval : ∀ev:eventval. ∀ty:typ. res (Σv:val. eventval_match ev ty v) ≝
λev,ty.
match ty with
[ Tint ⇒ match ev with [ EVint i ⇒ Some ? (OK ? (Vint i)) | _ ⇒ Some ? (Error ?) ]
| Tfloat ⇒ match ev with [ EVfloat f ⇒ Some ? (OK ? (Vfloat f)) | _ ⇒ Some ? (Error ?) ]
| _ ⇒ Some ? (Error ?)
]. nwhd; //; nqed.

ndefinition check_eventval' : ∀v:val. ∀ty:typ. res (Σev:eventval. eventval_match ev ty v) ≝
λv,ty.
match ty with
[ Tint ⇒ match v with [ Vint i ⇒ Some ? (OK ? (EVint i)) | _ ⇒ Some ? (Error ?) ]
| Tfloat ⇒ match v with [ Vfloat f ⇒ Some ? (OK ? (EVfloat f)) | _ ⇒ Some ? (Error ?) ]
| _ ⇒ Some ? (Error ?)
]. nwhd; //; nqed.

nlet rec check_eventval_list (vs: list val) (tys: list typ) : res (Σevs:list eventval. eventval_list_match evs tys vs) ≝
match vs with
[ nil ⇒ match tys with [ nil ⇒ Some ? (OK ? (nil ?)) | _ ⇒ Some ? (Error ?) ]
| cons v vt ⇒
  match tys with
  [ nil ⇒ Some ? (Error ?)
  | cons ty tyt ⇒ Some ? (
    ev ← check_eventval' v ty;:
    evt ← check_eventval_list vt tyt;:
    OK ? ((sig_eject ?? ev)::evt))
  ]
]. nwhd; //;
napply sig_bind_OK; #ev eev Hev;
napply sig_bind_OK; #evt eevt Hevt;
nnormalize; /2/;
nqed.

(* execution *)

nlet rec exec_step (ge:genv) (st:state) on st : (IO eventval io_out (Σ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' ← store_value_of_type (typeof a1) m loc ofs v2;:
    ret ? 〈E0, State f Sskip k e m'〉)
  | Scall lhs a al ⇒ Some ? (
    ! vf ← exec_expr ge e m a;:
    ! vargs ← exec_exprlist ge e m al;:
    ! fd ← find_funct ? ? ge vf;:
    ! p ← err_to_io … (assert_type_eq (type_of_fundef fd) (typeof a));:
(*
    ! k' ← match lhs with
         [ None ⇒ ret ? (Kcall (None ?) f e k)
         | Some lhs' ⇒
           ! locofs ← exec_lvalue ge e m lhs';:
           ret ? (Kcall (Some ? 〈sig_eject ?? locofs, typeof lhs'〉) f e k)
         ];:
    ret ? 〈E0, Callstate fd vargs k' m〉)
*)
    match lhs with
         [ None ⇒ ret ? 〈E0, Callstate fd vargs (Kcall (None ?) f e k) m〉
         | Some lhs' ⇒
           ! locofs ← exec_lvalue ge e m lhs';:
           ret ? 〈E0, Callstate fd vargs (Kcall (Some ? 〈sig_eject ?? locofs, typeof lhs'〉) f e k) m〉
         ])
  | Ssequence s1 s2 ⇒ Some ? (ret ? 〈E0, State f s1 (Kseq s2 k) e m〉)
  | Sskip ⇒
      match k with
      [ Kseq s k' ⇒ Some ? (ret ? 〈E0, State  f s k' e m〉)
      | Kstop ⇒
          match fn_return f with
          [ Tvoid ⇒ Some ? (ret ? 〈E0, Returnstate Vundef k (free_list m (blocks_of_env e))〉)
          | _ ⇒ Some ? (Wrong ???)
          ]
      | Kcall _ _ _ _ ⇒
          match fn_return f with
          [ Tvoid ⇒ Some ? (ret ? 〈E0, Returnstate Vundef k (free_list m (blocks_of_env e))〉)
          | _ ⇒ Some ? (Wrong ???)
          ]
      | Kwhile a s' k' ⇒ Some ? (ret ? 〈E0, State f (Swhile a s') k' e m〉)
      | Kdowhile a s' k' ⇒ Some ? (
          ! v ← exec_expr ge e m a;:
          ! b ← bool_of_val_3 v (typeof a);:
          match b with
          [ true ⇒ ret ? 〈E0, State f (Sdowhile a s') k' e m〉
          | false ⇒ ret ? 〈E0, State f Sskip k' e m〉
          ])
      | Kfor2 a2 a3 s' k' ⇒ Some ? (ret ? 〈E0, State f a3 (Kfor3 a2 a3 s' k') e m〉)
      | Kfor3 a2 a3 s' k' ⇒ Some ? (ret ? 〈E0, State f (Sfor Sskip a2 a3 s') k' e m〉)
      | Kswitch k' ⇒ Some ? (ret ? 〈E0, State f Sskip k' e m〉)
      | _ ⇒ Some ? (Wrong ???)
      ]
  | Scontinue ⇒
      match k with
      [ Kseq s' k' ⇒ Some ? (ret ? 〈E0, State f Scontinue k' e m〉)
      | Kwhile a s' k' ⇒ Some ? (ret ? 〈E0, State f (Swhile a s') k' e m〉)
      | Kdowhile a s' k' ⇒ Some ? (
          ! v ← exec_expr ge e m a;:
          ! b ← bool_of_val_3 v (typeof a);:
          match b with
          [ true ⇒ ret ? 〈E0, State f (Sdowhile a s') k' e m〉
          | false ⇒ ret ? 〈E0, State f Sskip k' e m〉
          ])
      | Kfor2 a2 a3 s' k' ⇒ Some ? (ret ? 〈E0, State f a3 (Kfor3 a2 a3 s' k') e m〉)
      | Kswitch k' ⇒ Some ? (ret ? 〈E0, State f Scontinue k' e m〉)
      | _ ⇒ Some ? (Wrong ???)
      ]
  | Sbreak ⇒
      match k with
      [ Kseq s' k' ⇒ Some ? (ret ? 〈E0, State f Sbreak k' e m〉)
      | Kwhile a s' k' ⇒ Some ? (ret ? 〈E0, State f Sskip k' e m〉)
      | Kdowhile a s' k' ⇒ Some ? (ret ? 〈E0, State f Sskip k' e m〉)
      | Kfor2 a2 a3 s' k' ⇒ Some ? (ret ? 〈E0, State f Sskip k' e m〉)
      | Kswitch k' ⇒ Some ? (ret ? 〈E0, State f Sskip k' e m〉)
      | _ ⇒ Some ? (Wrong ???)
      ]
  | Sifthenelse a s1 s2 ⇒ Some ? (
      ! v ← exec_expr ge e m a;:
      ! b ← bool_of_val_3 v (typeof a);:
      ret ? 〈E0, State f (if b then s1 else s2) k e m〉)
  | Swhile a s' ⇒ Some ? (
      ! v ← exec_expr ge e m a;:
      ! b ← bool_of_val_3 v (typeof a);:
      ret ? 〈E0, if b then State f s' (Kwhile a s' k) e m
                     else State f Sskip k e m〉)
  | Sdowhile a s' ⇒ Some ? (ret ? 〈E0, State f s' (Kdowhile a s' k) e m〉)
  | Sfor a1 a2 a3 s' ⇒
      match is_Sskip a1 with
      [ inl _ ⇒ Some ? (
          ! v ← exec_expr ge e m a2;:
          ! b ← bool_of_val_3 v (typeof a2);:
          ret ? 〈E0, State f (if b then s' else Sskip) (if b then (Kfor2 a2 a3 s' k) else k) e m〉)
      | inr _ ⇒ Some ? (ret ? 〈E0, State f a1 (Kseq (Sfor Sskip a2 a3 s') k) e m〉)
      ]
  | Sreturn a_opt ⇒
    match a_opt with
    [ None ⇒ match fn_return f with
      [ Tvoid ⇒ Some ? (ret ? 〈E0, Returnstate Vundef (call_cont k) (free_list m (blocks_of_env e))〉)
      | _ ⇒ Some ? (Wrong ???)
      ]
    | Some a ⇒ Some ? (
        ! u ← is_not_void (fn_return f);:
        ! v ← exec_expr ge e m a;:
        ret ? 〈E0, Returnstate v (call_cont k) (free_list m (blocks_of_env e))〉)
    ]
  | Sswitch a sl ⇒ Some ? (
      ! v ← exec_expr ge e m a;:
      match v with [ Vint n ⇒ ret ? 〈E0, State f (seq_of_labeled_statement (select_switch n sl)) (Kswitch k) e m〉
                   | _ ⇒ Wrong ??? ])
  | Slabel lbl s' ⇒ Some ? (ret ? 〈E0, State f s' k e m〉)
  | Sgoto lbl ⇒
      match find_label lbl (fn_body f) (call_cont k) with
      [ Some sk' ⇒ match sk' with [ mk_pair s' k' ⇒ Some ? (ret ? 〈E0, State f s' k' e m〉) ]
      | None ⇒ Some ? (Wrong ???)
      ]
  ]
| 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;:
      ret ? 〈E0, State f (fn_body f) k e m2〉
    ])
  | External f argtys retty ⇒ Some ? (
      ! evargs ← check_eventval_list vargs (typlist_of_typelist argtys);:
      ! evres ← do_io f evargs;:
      ! vres ← check_eventval evres (proj_sig_res (signature_of_type argtys retty));:
      ret ? 〈(Eextcall f evargs evres), Returnstate vres k m〉)
  ]
| Returnstate res k m ⇒
  match k with
  [ Kcall r f e k' ⇒
    match r with
    [ None ⇒
      match res with
      [ Vundef ⇒ Some ? (ret ? 〈E0, (State f Sskip k' e m)〉)
      | _ ⇒ Some ? (Wrong ???)
      ]
    | Some r' ⇒
      match r' with [ mk_pair locofs ty ⇒
        match locofs with [ mk_pair loc ofs ⇒ Some ? (
          ! m' ← store_value_of_type ty m loc ofs res;:
          ret ? 〈E0, (State f Sskip k' e m')〉)
        ]
      ]
    ]
  | _ ⇒ Some ? (Wrong ???)
  ]
]. nwhd; //;
##[ nrewrite > c7; napply step_skip_call; //; napply c8;
##| napply step_skip_or_continue_while; @; //;
##| napply sig_bindIO_OK; #v Hv;
    napply sig_bindIO_OK; #b; ncases b; #Hb;
    ##[ napply (step_skip_or_continue_dowhile_true … Hv);
      ##[ @; // ##| napply (bool_of … Hb); ##]
    ##| napply (step_skip_or_continue_dowhile_false … Hv);
      ##[ @; // ##| napply (bool_of … Hb); ##]
    ##]
##| napply step_skip_or_continue_for2; @; //;
##| napply step_skip_break_switch; @; //;
##| nrewrite > c11; napply step_skip_call; //; napply c12;
##| napply sig_bindIO2_OK; #loc ofs Hlval;
    napply sig_bindIO_OK; #v2 Hv2;
    napply opt_bindIO_OK; #m' em';
    nwhd; napply (step_assign … Hlval Hv2 em');
##| napply sig_bindIO_OK; #vf Hvf;
    napply sig_bindIO_OK; #vargs Hvargs;
    napply opt_bindIO_OK; #fd efd;
    napply bindIO_OK; #ety;
    ncases c6; nwhd;
    ##[ napply (step_call_none … Hvf Hvargs efd ety);
    ##| #lhs'; 
        napply sig_bindIO_OK; #locofs; ncases locofs; #loc ofs Hlocofs;
        nwhd; napply (step_call_some … Hlocofs Hvf Hvargs efd ety);
    ##]
##| napply sig_bindIO_OK; #v Hv;
    napply sig_bindIO_OK; #b; ncases b; #Hb;
    ##[ napply (step_ifthenelse_true … Hv); napply (bool_of … Hb); 
    ##| napply (step_ifthenelse_false … Hv); napply (bool_of … Hb)
    ##]
##| napply sig_bindIO_OK; #v Hv;
    napply sig_bindIO_OK; #b; ncases b; #Hb;
    ##[ napply (step_while_true … Hv); napply (bool_of … Hb);
    ##| napply (step_while_false … Hv); napply (bool_of … Hb);
    ##]
##| nrewrite > c11;
    napply sig_bindIO_OK; #v Hv;
    napply sig_bindIO_OK; #b; ncases b; #Hb;
    ##[ napply (step_for_true … Hv); napply (bool_of … Hb);
    ##| napply (step_for_false … Hv); napply (bool_of … Hb);
    ##]
##| napply step_for_start; //;
##| napply step_skip_break_switch; @2; //;
##| napply step_skip_or_continue_while; @2; //;
##| napply sig_bindIO_OK; #v Hv;
    napply sig_bindIO_OK; #b; ncases b; #Hb;
    ##[ napply (step_skip_or_continue_dowhile_true … Hv);
      ##[ @2; // ##| napply (bool_of … Hb); ##]
    ##| napply (step_skip_or_continue_dowhile_false … Hv);
      ##[ @2; // ##| napply (bool_of … Hb); ##]
    ##]
##| napply step_skip_or_continue_for2; @2; //
##| napply step_return_0; napply c9;
##| napply sig_bindIO_OK; #u Hnotvoid;
    napply sig_bindIO_OK; #v Hv;
    nwhd; napply (step_return_1 … Hnotvoid Hv);
##| napply sig_bindIO_OK; #v; ncases v; //; #n Hv;
    napply step_switch; //;
##| napply step_goto; nrewrite < c12; napply c9;
##| napply extract_subset_pair_io; #e m1 ealloc Halloc;
    napply sig_bindIO_OK; #m2 Hbind;
    nwhd; napply (step_internal_function … Halloc Hbind);
##| napply sig_bindIO_OK; #evs Hevs;
    napply bindIO_OK; #eres;
    napply sig_bindIO_OK; #res Hres;
    nwhd; napply step_external_function; @; ##[ napply Hevs; ##| napply Hres; ##]  
##| napply opt_bindIO_OK; #m' em'; napply step_returnstate_1; //;
##]
nqed.

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

ndefinition is_final_state : ∀st:state. (∃r. final_state st r) + (¬∃r. final_state st r).
#st; nelim st;
##[ #f s k e m; @2; @;*; #r H; ninversion H; #i m e; ndestruct;
##| #f l k m; @2; @;*; #r H; ninversion H; #i m e; ndestruct;
##| #v k m; ncases k; 
  ##[ ncases v;
    ##[ ##2: #i; @1; @ i; //;
    ##| ##1: @2; @; *;   #r H; ninversion H; #i m e; ndestruct;
    ##| #f; @2; @; *;   #r H; ninversion H; #i m e; ndestruct;
    ##| #b of; @2; @; *;   #r H; ninversion H; #i m e; ndestruct;
    ##]
  ##| #a b; @2; @; *; #r H; ninversion H; #i m e; ndestruct;
  ##| ##3,4: #a b c; @2; @; *; #r H; ninversion H; #i m e; ndestruct;
  ##| ##5,6,8: #a b c d; @2; @; *; #r H; ninversion H; #i m e; ndestruct;
  ##| #a; @2; @; *; #r H; ninversion H; #i m e; ndestruct;
  ##]
##] nqed.

nlet rec exec_steps (n:nat) (ge:genv) (s:state) :
 IO eventval io_out (Σts:trace×state. star (mk_transrel ?? step) ge s (\fst ts) (\snd ts)) ≝
match is_final_state s with
[ inl _ ⇒ Some ? (ret ? 〈E0, s〉)
| inr _ ⇒
  match n with
  [ O ⇒ Some ? (ret ? 〈E0, s〉)
  | S n' ⇒ Some ? (
      ! 〈t,s'〉 ← exec_step ge s;:
      ! 〈t',s''〉 ← exec_steps n' ge s';:
      ret ? 〈t ⧺ t',s''〉)
  ]
]. nwhd; /2/;
napply sig_bindIO2_OK; #t s' H1;
napply sig_bindIO2_OK; #t' s'' IH;
nwhd; napply (star_step … IH); //;
nqed.
(*
nlet rec exec_steps_without_proof (n:nat) (ge:genv) (s:state) :
 res (trace×state) ≝
match is_final_state s with
[ inl _ ⇒ OK ? 〈E0, s〉
| inr _ ⇒
  match n with
  [ O ⇒ OK ? 〈E0, s〉
  | S n' ⇒
      〈t,s'〉 ← exec_step ge s;:
      〈t',s''〉 ← exec_steps_without_proof n' ge s';:
      OK ? 〈t ⧺ t',s''〉
  ]
].
*)