include "Csem.ma".

include "extralib.ma".
include "IOMonad.ma".

include "Plogic/russell_support.ma".

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); //;
  ##| #p b i i0 s; @ true; @; //
  ##| #i p t ne; @ true; @; //; nwhd; nrewrite > (eq_false … ne); //;
  ##| #p b i p0 t0; @ true; @; //
  ##| #f s ne; @ true; @; //; nwhd; nrewrite > (Feq_zero_false … ne); //;
  ##| #i s; @ false; @; //; (*nwhd; nrewrite > (eq_true …); //;*)
  ##| #p 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. ∀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;
##| #_; napply I;
##] 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.

(*
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 try_cast_null (m:mem) (i:int) (ty:type) (ty':type) on i : res (Σv':val. cast m (Vint i) ty ty' v') ≝
match eq i zero with
[ true ⇒
  match ty with
  [ Tint _ _ ⇒
    match ty' with
    [ Tpointer _ _ ⇒ Some ? (OK ? (Vint i))
    | Tarray _ _ _ ⇒ Some ? (OK ? (Vint i))
    | Tfunction _ _ ⇒ Some ? (OK ? (Vint i))
    | _ ⇒ Some ? (Error ?)
    ]
  | Tpointer _ _ ⇒
    match ty' with
    [ Tpointer _ _ ⇒ Some ? (OK ? (Vint i))
    | Tarray _ _ _ ⇒ Some ? (OK ? (Vint i))
    | Tfunction _ _ ⇒ Some ? (OK ? (Vint i))
    | _ ⇒ Some ? (Error ?)
    ]
  | Tarray _ _ _ ⇒
    match ty' with
    [ Tpointer _ _ ⇒ Some ? (OK ? (Vint i))
    | Tarray _ _ _ ⇒ Some ? (OK ? (Vint i))
    | Tfunction _ _ ⇒ Some ? (OK ? (Vint i))
    | _ ⇒ Some ? (Error ?)
    ]
  | Tfunction _ _ ⇒
    match ty' with
    [ Tpointer _ _ ⇒ Some ? (OK ? (Vint i))
    | Tarray _ _ _ ⇒ Some ? (OK ? (Vint i))
    | Tfunction _ _ ⇒ Some ? (OK ? (Vint i))
    | _ ⇒ Some ? (Error ?)
    ]
  | _ ⇒ Some ? (Error ?)
  ]
| false ⇒ Some ? (Error ?)
]. nwhd; //; nlapply (eq_spec i zero); nrewrite > c0; #e; nrewrite > e;
   ##[ ##1,2,3: napply cast_ip_z ##| ##*: napply cast_pp_z ##] //; nqed. 

ndefinition ms_eq_dec : ∀s1,s2:memory_space. (s1 = s2) + (s1 ≠ s2).
#s1; ncases s1; #s2; ncases s2; /2/; @2; @; #H; ndestruct; nqed. 

ndefinition exec_cast : ∀m:mem. ∀v:val. ∀ty:type. ∀ty':type. res (Σv':val. cast m v ty ty' v') ≝
λm:mem. λv:val. λty:type. λty':type.
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))))
    | Tpointer _ _ ⇒ Some (res val) (do r ← try_cast_null m i ty ty'; OK val r)
    | Tarray _ _ _ ⇒ Some (res val) (do r ← try_cast_null m i ty ty'; OK val r)
    | Tfunction _ _ ⇒ Some (res val) (do r ← try_cast_null m i ty ty'; OK val r)
    | _ ⇒ Some ? (Error ?)
    ]
  | Tpointer _ _ ⇒ Some (res val) (do r ← try_cast_null m i ty ty'; OK val r)
  | Tarray _ _ _ ⇒ Some (res val) (do r ← try_cast_null m i ty ty'; OK val r)
  | Tfunction _ _ ⇒ Some (res val) (do r ← try_cast_null m i ty ty'; OK val r)
  | _ ⇒ Some ? (Error ?)
  ]
| 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 p b ofs ⇒
  Some ? (
    do s ← match ty with [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code | _ ⇒ Error ? ];
    do u ← match ms_eq_dec p s with [ inl _ ⇒ OK ? something | inr _ ⇒ Error ? ];
    do s' ← match ty' with
         [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code
         | _ ⇒ Error ? ];
    if is_pointer_compat (block_space m b) s'
    then OK ? (Vptr s' b ofs)
    else Error ?)
| _ ⇒ Some ? (Error ?)
]. nwhd; //;
##[ ##1,2,3,4,5,6: napply sig_bind_OK; #v'; #H; ndestruct; napply H;
##| napply bind_OK; #s es;
    ncut (type_space ty s);
    ##[ ncases ty in es ⊢ %; 
      ##[ #e; ##| ##3,9: #a e; ##| ##2,4,6,7,8: #a b e; ##| #a b c e; ##] nwhd in e:(??%?); ndestruct; //;
    ##| #Hty;
        napply bind_OK; #u1 eeq;
        napply bind_OK; #s' es';
        ncut (type_space ty' s');
        ##[ ncases ty' in es' ⊢ %; ##[ #e; ##| ##3,9: #a e; ##| ##2,4,6,7,8: #a b e; ##| #a b c e; ##]
            nwhd in e:(??%?); ndestruct; //;
        ##| #Hty'; 
            ncut (s = c0). nelim (ms_eq_dec c0 s) in eeq; //; nnormalize; #_; #e; ndestruct.
            #e; nrewrite < e;
            nwhd in match (is_pointer_compat ??) in ⊢ %;
            ncases (pointer_compat_dec (block_space m c1) s'); #Hcompat;
            nwhd; /2/;
        ##]
    ##]
##] nqed.

ndefinition load_value_of_type' ≝
λty,m,l. match l with [ mk_pair pl ofs ⇒ match pl with [ mk_pair psp loc ⇒
  load_value_of_type ty m psp loc ofs ] ].

(* 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×trace. eval_expr ge en m e (\fst r) (\snd r)) ≝
match e with
[ Expr e' ty ⇒
  match e' with
  [ Econst_int i ⇒ Some ? (OK ? 〈Vint i, E0〉)
  | Econst_float f ⇒ Some ? (OK ? 〈Vfloat f, E0〉)
  | Evar _ ⇒ Some ? (
      do 〈l,tr〉 ← exec_lvalue' ge en m e' ty;
      do v ← opt_to_res ? (load_value_of_type' ty m l);
      OK ? 〈v,tr〉)
  | Ederef _ ⇒ Some ? (
      do 〈l,tr〉 ← exec_lvalue' ge en m e' ty;
      do v ← opt_to_res ? (load_value_of_type' ty m l);
      OK ? 〈v,tr〉)
  | Efield _ _ ⇒ Some ? (
      do 〈l,tr〉 ← exec_lvalue' ge en m e' ty;
      do v ← opt_to_res ? (load_value_of_type' ty m l);
      OK ? 〈v,tr〉)
  | Eaddrof a ⇒ Some ? (
      do 〈plo,tr〉 ← exec_lvalue ge en m a;
      OK ? 〈match plo with [ mk_pair pl ofs ⇒ match pl with [ mk_pair pcl loc ⇒ Vptr pcl loc ofs ] ], tr〉)
  | Esizeof ty' ⇒ Some ? (OK ? 〈Vint (repr (sizeof ty')), E0〉)
  | Eunop op a ⇒ Some ? (
      do 〈v1,tr〉 ← exec_expr ge en m a;
      do v ← opt_to_res ? (sem_unary_operation op v1 (typeof a));
      OK ? 〈v,tr〉)
  | Ebinop op a1 a2 ⇒ Some ? (
      do 〈v1,tr1〉 ← exec_expr ge en m a1;
      do 〈v2,tr2〉 ← exec_expr ge en m a2;
      do v ← opt_to_res ? (sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m);
      OK ? 〈v,tr1⧺tr2〉)
  | Econdition a1 a2 a3 ⇒ Some ? (
      do 〈v,tr1〉 ← exec_expr ge en m a1;
      do b ← bool_of_val_3 v (typeof a1);
      do 〈v',tr2〉 ← match b return λ_.res (val×trace) with
                 [ true ⇒ (exec_expr ge en m a2)
                 | false ⇒ (exec_expr ge en m a3) ];
      OK ? 〈v',tr1⧺tr2〉)
(*      if b then exec_expr ge en m a2 else exec_expr ge en m a3)*)
  | Eorbool a1 a2 ⇒ Some ? (
      do 〈v1,tr1〉 ← exec_expr ge en m a1;
      do b1 ← bool_of_val_3 v1 (typeof a1);
      match b1 return λ_.res (val×trace) with [ true ⇒ OK ? 〈Vtrue,tr1〉 | false ⇒
        do 〈v2,tr2〉 ← exec_expr ge en m a2;
        do b2 ← bool_of_val_3 v2 (typeof a2);
        OK ? 〈of_bool b2, tr1⧺tr2〉 ])
  | Eandbool a1 a2 ⇒ Some ? (
      do 〈v1,tr1〉 ← exec_expr ge en m a1;
      do b1 ← bool_of_val_3 v1 (typeof a1);
      match b1 return λ_.res (val×trace) with [ true ⇒
        do 〈v2,tr2〉 ← exec_expr ge en m a2;
        do b2 ← bool_of_val_3 v2 (typeof a2);
        OK ? 〈of_bool b2, tr1⧺tr2〉
      | false ⇒ OK ? 〈Vfalse,tr1〉 ])
  | Ecast ty' a ⇒ Some ? (
      do 〈v,tr〉 ← exec_expr ge en m a;
      do v' ← exec_cast m v (typeof a) ty';
      OK ? 〈(* XXX *)sig_eject ?? v',tr〉)
  | Ecost l a ⇒ Some ? (
      do 〈v,tr〉 ← exec_expr ge en m a;
      OK ? 〈v,tr⧺(Echarge l)〉)
  ]
]
and exec_lvalue' (ge:genv) (en:env) (m:mem) (e':expr_descr) (ty:type) on e' : res (Σr:memory_space × block × int × trace. eval_lvalue ge en m (Expr e' ty) (\fst (\fst (\fst r))) (\snd (\fst (\fst r))) (\snd (\fst r)) (\snd r)) ≝
  match e' with
  [ Evar id ⇒ 
      match (get … id en) with
      [ None ⇒ Some ? (do 〈sp,l〉 ← opt_to_res ? (find_symbol ? ? ge id); OK ? 〈〈〈sp,l〉,zero〉,E0〉) (* global *)
      | Some loc ⇒ Some ? (OK ? 〈〈〈Any,loc〉,zero〉,E0〉) (* local *)
      ]
  | Ederef a ⇒ Some ? (
      do 〈v,tr〉 ← exec_expr ge en m a;
      match v with
      [ Vptr sp l ofs ⇒ OK ? 〈〈〈sp,l〉,ofs〉,tr〉
      | _ ⇒ Error ?
      ])
  | Efield a i ⇒
      match (typeof a) with
      [ Tstruct id fList ⇒ Some ? (
          do 〈plofs,tr〉 ← exec_lvalue ge en m a;
          do delta ← field_offset i fList;
          OK ? 〈〈\fst plofs,add (\snd plofs) (repr delta)〉,tr〉)
      | Tunion id fList ⇒ Some ? (
          do 〈plofs,tr〉 ← exec_lvalue ge en m a;
          OK ? 〈plofs,tr〉)
      | _ ⇒ Some ? (Error ?)
      ]
  | _ ⇒ Some ? (Error ?)
  ]
and exec_lvalue (ge:genv) (en:env) (m:mem) (e:expr) on e : res (Σr:memory_space × block × int × trace. eval_lvalue ge en m e (\fst (\fst (\fst r))) (\snd (\fst (\fst r))) (\snd (\fst r)) (\snd r)) ≝
match e with [ Expr e' ty ⇒ exec_lvalue' ge en m e' ty ].
nwhd; 
##[ ##1,2: //
##| ##3,4:
    napply sig_bind2_OK; nrewrite > c4; #x; ncases x; #y; ncases y; #sp loc ofs tr H;
    napply opt_bind_OK;  #v ev; nwhd in ev:(??%?); napply (eval_Elvalue … H ev);
##| napply sig_bind2_OK; #x; ncases x; #y; ncases y; #sp loc ofs tr H;
    nwhd; napply eval_Eaddrof; //;
##| napply sig_bind2_OK; #v1 tr Hv1;
    napply opt_bind_OK; #v ev;
    napply (eval_Eunop … Hv1 ev);
##| napply sig_bind2_OK; #v1 tr1 Hv1;
    napply sig_bind2_OK; #v2 tr2 Hv2;
    napply opt_bind_OK; #v ev;
    napply (eval_Ebinop … Hv1 Hv2 ev);
##| napply sig_bind2_OK; #v tr Hv;
    napply sig_bind_OK; #v' Hv';
    napply (eval_Ecast … Hv Hv');
##| napply sig_bind2_OK; #vb tr1 Hvb;
    napply sig_bind_OK; #b;
    ncases b; #Hb; napply sig_bind2_OK; #v tr Hv;
    ##[ napply (eval_Econdition_true … Hvb ? Hv);  napply (bool_of ??? Hb);
    ##| napply (eval_Econdition_false … Hvb ? Hv);  napply (bool_of ??? Hb);
    ##]
##| napply sig_bind2_OK; #v1 tr1 Hv1;
    napply sig_bind_OK; #b1; ncases b1; #Hb1;
    ##[ napply sig_bind2_OK; #v2 tr2 Hv2;
        napply sig_bind_OK; #b2 Hb2; 
        napply (eval_Eandbool_2 … Hv1 … Hv2);
        ##[ napply (bool_of … Hb1); ##| napply Hb2; ##]
    ##| napply (eval_Eandbool_1 … Hv1); napply (bool_of … Hb1);
    ##]
##| napply sig_bind2_OK; #v1 tr1 Hv1;
    napply sig_bind_OK; #b1; ncases b1; #Hb1;
    ##[ napply (eval_Eorbool_1 … Hv1); napply (bool_of … Hb1);
    ##| napply sig_bind2_OK; #v2 tr2 Hv2;
        napply sig_bind_OK; #b2 Hb2; 
        napply (eval_Eorbool_2 … Hv1 … Hv2);
        ##[ napply (bool_of … Hb1); ##| napply Hb2; ##]
    ##]
##| //
##| napply sig_bind2_OK; nrewrite > c5; #x; ncases x; #y; ncases y; #sp l ofs tr H;
    napply opt_bind_OK; #v ev; napply (eval_Elvalue … H ev);
##| napply sig_bind2_OK; #v tr1 H; napply (eval_Ecost … H);
##| //
##| //
##| napply opt_bind_OK; #sl; ncases sl; #sp l el; napply eval_Evar_global; /2/;
##| napply (eval_Evar_local … c3);
##| napply sig_bind2_OK; #v; ncases v; //; #sp l ofs tr Hv; nwhd;
    napply eval_Ederef; //
##| ##20,21,22,23,24,25,26,27,28,29,30,31,32,33: //
##| napply sig_bind2_OK; #x; ncases x; #sp l ofs H;
    napply bind_OK; #delta Hdelta;
    napply (eval_Efield_struct … H c5 Hdelta);
##| napply sig_bind2_OK; #x; ncases x; #sp 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 (Σvltr:list val×trace. eval_exprlist ge e m l (\fst vltr) (\snd vltr)) ≝
match l with
[ nil ⇒ Some ? (OK ? 〈nil val, E0〉)
| cons e1 es ⇒ Some ? (
  do 〈v,tr1〉 ← exec_expr ge e m e1;
  do 〈vs,tr2〉 ← exec_exprlist ge e m es;
  OK ? 〈cons val v vs, tr1⧺tr2〉)
]. nwhd; //;
napply sig_bind2_OK; #v tr1 Hv;
napply sig_bind2_OK; #vs tr2 Hvs;
nwhd; napply eval_Econs; //;
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) Any 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 ? ? 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 ? (
          do b ← opt_to_res ? (get … id e);
          do m1 ← opt_to_res ? (store_value_of_type ty m Any 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 s t ⇒ match t2 with [ Tpointer s' t' ⇒
    match ms_eq_dec s s' with [ inl _ ⇒
      match assert_type_eq t t' with [ OK _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ] | _ ⇒ dn ]
| Tarray s t n ⇒ match t2 with [ Tarray s' t' n' ⇒
    match ms_eq_dec s s' with [ inl _ ⇒
      match assert_type_eq t t' with [ OK _ ⇒
        match decidable_eq_Z_Type n n' with [ inl _ ⇒ dy | inr _ ⇒ dn ] | _ ⇒ 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 ? (
    do ev ← check_eventval' v ty;
    do evt ← check_eventval_list vt tyt;
    OK ? ((sig_eject ?? ev)::evt))
  ]
]. nwhd; //;
napply sig_bind_OK; #ev Hev;
napply sig_bind_OK; #evt Hevt;
nnormalize; /2/;
nqed.

(* execution *)

ndefinition store_value_of_type' ≝
λty,m,l,v.
match l with [ mk_pair pl ofs ⇒
  match pl with [ mk_pair pcl loc ⇒
    store_value_of_type ty m pcl loc ofs v ] ].

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 ? (
    ! 〈l,tr1〉 ← exec_lvalue ge e m a1;
    ! 〈v2,tr2〉 ← exec_expr ge e m a2;
    ! m' ← store_value_of_type' (typeof a1) m l v2;
    ret ? 〈tr1⧺tr2, State f Sskip k e m'〉)
  | Scall lhs a al ⇒ Some ? (
    ! 〈vf,tr2〉 ← exec_expr ge e m a;
    ! 〈vargs,tr3〉 ← 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 ? 〈tr2⧺tr3, Callstate fd vargs (Kcall (None ?) f e k) m〉
         | Some lhs' ⇒
           ! 〈locofs,tr1〉 ← exec_lvalue ge e m lhs';
           ret ? 〈tr1⧺tr2⧺tr3, Callstate fd vargs (Kcall (Some ? 〈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,tr〉 ← exec_expr ge e m a;
          ! b ← bool_of_val_3 v (typeof a);
          match b with
          [ true ⇒ ret ? 〈tr, State f (Sdowhile a s') k' e m〉
          | false ⇒ ret ? 〈tr, 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,tr〉 ← exec_expr ge e m a;
          ! b ← bool_of_val_3 v (typeof a);
          match b with
          [ true ⇒ ret ? 〈tr, State f (Sdowhile a s') k' e m〉
          | false ⇒ ret ? 〈tr, 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,tr〉 ← exec_expr ge e m a;
      ! b ← bool_of_val_3 v (typeof a);
      ret ? 〈tr, State f (if b then s1 else s2) k e m〉)
  | Swhile a s' ⇒ Some ? (
      ! 〈v,tr〉 ← exec_expr ge e m a;
      ! b ← bool_of_val_3 v (typeof a);
      ret ? 〈tr, 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,tr〉 ← exec_expr ge e m a2;
          ! b ← bool_of_val_3 v (typeof a2);
          ret ? 〈tr, 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,tr〉 ← exec_expr ge e m a;
        ret ? 〈tr, Returnstate v (call_cont k) (free_list m (blocks_of_env e))〉)
    ]
  | Sswitch a sl ⇒ Some ? (
      ! 〈v,tr〉 ← exec_expr ge e m a;
      match v with [ Vint n ⇒ ret ? 〈tr, 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 ???)
      ]
  | Scost lbl s' ⇒ Some ? (ret ? 〈Echarge lbl, State f s' k e m〉)
  ]
| 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 l ty ⇒
        Some ? (
          ! m' ← store_value_of_type' ty m l 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_bindIO2_OK; #v tr 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; #x; ncases x; #y; ncases y; #pcl loc ofs tr1 Hlval;
    napply sig_bindIO2_OK; #v2 tr2 Hv2;
    napply opt_bindIO_OK; #m' em';
    nwhd; napply (step_assign … Hlval Hv2 em');
##| napply sig_bindIO2_OK; #vf tr1 Hvf;
    napply sig_bindIO2_OK; #vargs tr2 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_bindIO2_OK; #x; ncases x; #y; ncases y; #pcl loc ofs tr3 Hlocofs;
        nwhd; napply (step_call_some … Hlocofs Hvf Hvargs efd ety);
    ##]
##| napply sig_bindIO2_OK; #v tr 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_bindIO2_OK; #v tr 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_bindIO2_OK; #v tr 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_bindIO2_OK; #v tr 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_bindIO2_OK; #v tr Hv;
    nwhd; napply (step_return_1 … Hnotvoid Hv);
##| napply sig_bindIO2_OK; #v; ncases v; //; #n tr 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; ##]  
##| ncases c11; #x; ncases x; #pcl b ofs;
    napply opt_bindIO_OK; #m' em'; napply step_returnstate_1; nwhd in em':(??%?); //;
##]
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 ? (
    ! 〈sp,b〉 ← find_symbol ? ? ge (prog_main ?? p);
    ! u ← opt_to_io … (match ms_eq_dec sp Code with [ inl _ ⇒ Some ? something | inr _ ⇒ None ? ]);
    ! f ← find_funct_ptr ? ? ge b;
    ret ? (Callstate f (nil ?) Kstop m0)).
nwhd;
napply opt_bindIO2_OK; #sp b esb;
napply opt_bindIO_OK; #u ecode;
napply opt_bindIO_OK; #f ef;
ncases sp in esb ecode; #esb ecode; nwhd in ecode:(??%%); ##[ ##1,2,3,4,5: ndestruct (ecode); ##]
nwhd; napply (initial_state_intro … esb 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;
    ##| #pcl 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'〉 ← match s with
                 [ State f s k e m ⇒ match m with [ mk_mem c n p ⇒ exec_step ge (State f s k e (mk_mem c n p)) ]
                 | Callstate fd args k m ⇒ match m with [ mk_mem c n p ⇒ exec_step ge (Callstate fd args k (mk_mem c n p)) ]
                 | Returnstate r k m ⇒ match m with [ mk_mem c n p ⇒ exec_step ge (Returnstate r k (mk_mem c n p)) ]
                 ] ;*)
      ! 〈t',s''〉 ← match s' with
                 [ State f s k e m ⇒ match m with [ mk_mem c n p ⇒ exec_steps n' ge (State f s k e (mk_mem c n p)) ]
                 | Callstate fd args k m ⇒ match m with [ mk_mem c n p ⇒ exec_steps n' ge (Callstate fd args k (mk_mem c n p)) ]
                 | Returnstate r k m ⇒ match m with [ mk_mem c n p ⇒ exec_steps n' ge (Returnstate r k (mk_mem c n p)) ]
                 ] ;
(*      ! 〈t',s''〉 ← exec_steps n' ge s';*)
      ret ? 〈t ⧺ t',s''〉)
  ]
]. nwhd; /2/;
napply sig_bindIO2_OK; #t s'; ncases s'; ##[ #f st k e m; ##| #fd args k m; ##| #r k m; ##]
nwhd in ⊢ (? → ?????(??????%?));
ncases m; #mc mn mp; #H1;
nwhd in ⊢ (?????(??????%?));
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''〉
  ]
].
*)

(* A (possibly non-terminating) execution. *)
ncoinductive execution : Type ≝
| e_stop : trace → state → execution
| e_step : trace → state → execution → execution
| e_wrong : execution
| e_interact : io_out → (eventval → execution) → execution.

nlet corec exec_inf_aux (ge:genv) (s:IO eventval io_out (trace×state)) : execution ≝
match s with
[ Wrong ⇒ e_wrong
| Value v ⇒ match v with [ mk_pair t s' ⇒ 
    match is_final_state s' with
    [ inl _ ⇒ e_stop t s'
    | inr _ ⇒ e_step t s' (exec_inf_aux ge (exec_step ge s')) ] ]
| Interact out k' ⇒ e_interact out (λv. exec_inf_aux ge (k' v))
].

ndefinition exec_inf : program → execution ≝
λp. exec_inf_aux (globalenv Genv ?? p) (! s ← make_initial_state p; ret ? 〈E0,sig_eject ?? s〉).