source: C-semantics/CexecIOcomplete.ma @ 226

include "CexecIO.ma".
include "Plogic/connectives.ma".

ndefinition yields : ∀A,P. res (Σx:A. P x) → A → Prop ≝
λA,P,e,v. match e with [ OK v' ⇒ match v' with [ sig_intro v'' _ ⇒ v = v'' ] | _ ⇒ False].
ndefinition yieldsIO : ∀A,P. IO eventval io_out (Σx:A. P x) → A → Prop ≝
λA,P,e,v. match e with [ Value v' ⇒ match v' with [ sig_intro v'' _ ⇒ v = v'' ] | _ ⇒ False].
(*
ndefinition yields : ∀A.∀P:A → Prop. res (sigma A P) → A → Prop ≝
λA,P,e,v. err_eject A P e = OK ? v.
*)
nlemma is_pointer_compat_true: ∀m,b,sp.
  pointer_compat (block_space m b) sp →
  is_pointer_compat (block_space m b) sp = true.
#m b sp H; nwhd in ⊢ (??%?);
nelim (pointer_compat_dec (block_space m b) sp);
##[ //
##| #H'; napply False_ind; napply (absurd … H H');
##] nqed.

nlemma ms_eq_dec_true: ∀s. ms_eq_dec s s = inl ???.
##[ #s; ncases s; napply refl;
##| ##skip
##] nqed.

notation < "vbox( e break ↓ break e')" with precedence 99 for @{'yields ${e} ${e'}}.
interpretation "yields" 'yields e e' = (yields ?? e e').
interpretation "yields IO" 'yields e e' = (yieldsIO ?? e e').
(*
(*notation < "vbox( ident v ← e;: break e' )" with precedence 40 for @{'bindnat ${e} (\lambda ${ident v} : ${ty}. ${e'})}.*)
notation < "vbox( e ;: break e' )" with precedence 40 for @{'binde ${e} ${e'}}.
notation < "vbox( ident v ← e ;: break e' )" with precedence 40 for @{'binde ${e} (λ${ident v}. ${e'})}.
notation < "vbox( ident v : ty ← e ;: break e' )" with precedence 40 for @{'binde ${e} (λ${ident v} : ${ty}. ${e'})}.
interpretation "error monad bind" 'binde e f = (bind ? ? e f).
(*interpretation "error monad bind" 'bindnat e f = (bind nat nat e f).*)

nlemma foo: ∀e:res nat. ∀f: nat → res nat. (x ← e;: f x) = OK ? 5.
*)
(*interpretation "error monad bind" 'bind e f = (bind ? ? e f).*)

ntheorem is_det: ∀p,s,s'.
initial_state p s → initial_state p s' → s = s'.
#p s s' H1 H2;
ninversion H1; #b1 f1 e11 e12 e13;
ninversion H2; #b2 f2 e21 e22 e23;
nrewrite > e11 in e21;
#e1; nrewrite > (?:b1 = b2) in e12;
##[ nrewrite > e22; #e2; nrewrite > (?:f2 = f1);
  ##[ //;
  ##| ndestruct (e2) skip (e22 e23); //;
  ##]
##| ndestruct (e1) skip (e11); // 
##] nqed.

ndefinition yieldsIObare ≝ λA.λa:IO eventval io_out A.λv':A.
match a with [ Value v ⇒ v' = v | _ ⇒ False ].

nlemma remove_io_sig: ∀A. ∀P:A → Prop. ∀a,v',p.
yieldsIObare A a v' →
yieldsIO A P (io_inject eventval io_out A (λx.P x) (Some ? a) p) v'.
#A P a; ncases a;
##[ #a b c d; *;
##| #v v' p H; napply H;
##| #a b; *;
##] nqed.


ntheorem the_initial_state:
  ∀p,s. initial_state p s → yieldsIO ?? (make_initial_state p) s.
#p s; ncases p; #fns main globs H;
napply remove_io_sig;
ninversion H;
#b f e1 e2 e3;
nrewrite > e1;
nwhd in ⊢ (??%?);
nrewrite > e2;
nwhd; napply refl;
nqed.

ndefinition yieldsbare ≝ λA.λa:res A.λv':A.
match a with [ OK v ⇒ v' = v | _ ⇒ False ].

nlemma remove_res_sig: ∀A. ∀P:A → Prop. ∀a,v',p.
yieldsbare A a v' →
yields A P (err_inject A (λx.P x) (Some ? a) p) v'.
#A P a; ncases a;
##[ #v v' p H; napply H;
##| #a b; *;
##] nqed.

nlemma cast_complete: ∀m,v,ty,ty',v'.
  cast m v ty ty' v' → yields ?? (exec_cast m v ty ty') v'.
#m v ty ty' v' H;
nelim H;
##[ #m i sz1 sz2 sg1 sg2; napply refl;
##| #m f sz szi sg; napply refl;
##| #m i sz sz' sg; napply refl;
##| #m f sz sz'; napply refl;
##| #m sp sp' ty ty' b ofs H1 H2 H3; napply remove_res_sig;
    nelim H1; ##[ #sp1 ty1 ##| #sp1 ty1 n1 ##| #tys1 ty1; nletin sp1 ≝ Code ##]
    nwhd in ⊢ (??%?);
    ##[ ##1,2: nrewrite > (ms_eq_dec_true …); nwhd in ⊢ (??%?); ##]
    nelim H2 in H3 ⊢ %; ##[ ##1,4,7: #sp2 ty2 ##| ##2,5,8: #sp2 ty2 n2 ##| ##3,6,9: #tys2 ty2; nletin sp2 ≝ Code ##]
    #H3; nwhd in ⊢ (??%?);
    nrewrite > (is_pointer_compat_true …); //;
##| #m sz si ty'' H; ncases H; ##[ #sp1 ty1 ##| #sp1 ty1 n1 ##| #args rty ##] napply refl;
##| #m t t' H H'; ncases H; ncases H'; //;
##] nqed.

nlemma yields_eq: ∀A,P,e,v. yields A P e v → ∃p. e = OK ? (sig_intro … v p).
#A P e v; ncases e;
##[ #vp; ncases vp; #v' p H; nwhd in H; nrewrite > H; @ p; napply refl;
##| *;
##] nqed.
(*
nlemma lvalue_complete_cond: ∀ge,env,m.
(∀e,v,tr. eval_expr ge env m e v tr → yields ?? (exec_expr ge env m e) (〈v,tr〉)) →
(∀e,sp,l,off,tr. eval_lvalue ge env m e sp l off tr → yields ?? (exec_lvalue ge env m e) (〈〈〈sp,l〉,off〉,tr〉)).
#ge env m IH;
#e sp l off tr H; napply (eval_lvalue_ind … H);
##[ #id l ty H1; nwhd in ⊢ (???%?);
    nrewrite > H1;
    napply refl;
##| #id sp l ty H1 H2; nwhd in ⊢ (???%?); 
    nrewrite > H1; nwhd nodelta in ⊢ (???%?); napply remove_res_sig;
    nrewrite > H2;
*)

(* Use to narrow down the choice of expression to just the lvalues. *)
nlemma lvalue_expr: ∀ge,env,m,e,ty,sp,l,ofs,tr. ∀P:expr_descr → Prop.
  eval_lvalue ge env m (Expr e ty) sp l ofs tr → 
  (∀id. P (Evar id)) → (∀e'. P (Ederef e')) → (∀e',id. P (Efield e' id)) →
  P e.
#ge env m e ty sp l ofs tr P H; napply (eval_lvalue_inv_ind … H);
##[ #id l ty e1 e2 e3 e4 e5 e6; ndestruct; //
##| #id sp l ty e1 e2 e3 e4 e5 e6 e7; ndestruct; //
##| #e ty sp l ofs tr H e1 e2 e3 e4 e5; ndestruct; //
##| #e id ty sp l ofs id' fs d tr H e1 e2;(* bogus? *) #_; #e3 e4 e5 e6 e7; ndestruct; //
##| #e id ty sp l ofs id' fs tr H e1;(* bogus? *) #_; #e2 e3 e4 e5 e6; ndestruct; //
##] nqed.

nlemma bool_of_val_3_complete : ∀v,ty,r. bool_of_val v ty r → ∃b. r = of_bool b ∧ yields ?? (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; @; //;
  ##| #p t; @ false; @; //;
  ##| #s; @ false; @; //; nwhd; nrewrite > (Feq_zero_true …); //;
  ##]
nqed.

nlemma bool_of_true: ∀v,ty. is_true v ty → yields ?? (bool_of_val_3 v ty) true.
#v ty H; nelim H;
  ##[ #i is s ne; nwhd; nrewrite > (eq_false … ne); //;
  ##| #p b i i0 s; //
  ##| #i p t ne; nwhd; nrewrite > (eq_false … ne); //;
  ##| #p b i p0 t0; //
  ##| #f s ne; nwhd; nrewrite > (Feq_zero_false … ne); //;
  ##]
nqed.

nlemma bool_of_false: ∀v,ty. is_false v ty → yields ?? (bool_of_val_3 v ty) false.
#v ty H; nelim H;
  ##[ #i s; //;
  ##| #p t; //;
  ##| #s; nwhd; nrewrite > (Feq_zero_true …); //;
  ##]
nqed.

nremark eq_to_jmeq: ∀A. ∀a,b:A. a = b → a ≃ b.
#A a b H; nrewrite > H; //; nqed.

nlemma dep_option_rewrite: ∀A,B:Type. ∀e:option A. ∀r:B. ∀P:B → Prop. ∀Q:e ≃ None A → res (Σx:B. P x). ∀R:∀v. e ≃ Some A v → res (Σx:B. P x). ∀h: e = None A.
 yields ?? (Q (eq_to_jmeq ??? h)) r →
 yields ?? ((match e return λe'.e ≃ e' → ? with [ None ⇒ λp.Q p | Some v ⇒ λp.R v p ]) (refl_jmeq (option A) e)) r.
#A B e; ncases e;
##[ #r P Q R h; nwhd in ⊢ (? → ???%?);
napply (streicherKjmeq ?? (λe. yields ?? (Q e) r → yields ?? (Q (refl_jmeq (option A) (None A))) r));
//;
##| #v r P Q R h; ndestruct (h);
##] nqed. 

nlemma expr_complete: ∀ge,env,m.
(∀e,v,tr. eval_expr ge env m e v tr → yields ?? (exec_expr ge env m e) (〈v,tr〉)) ∧
(∀e,sp,l,off,tr. eval_lvalue ge env m e sp l off tr → yields ?? (exec_lvalue ge env m e) (〈〈〈sp,l〉,off〉,tr〉)).
#ge env m;
napply (combined_expr_lvalue_ind ge env m
  (λe,v,tr,H. yields ?? (exec_expr ge env m e) (〈v,tr〉))
  (λe,sp,l,off,tr,H. yields ?? (exec_lvalue ge env m e) (〈〈〈sp,l〉,off〉,tr〉)));
##[ #i ty; napply refl;
##| #f ty; napply refl;
##| #e ty sp l off v tr H1 H2; napply (lvalue_expr … H1);
    ##[ #id ##| #e' ##| #e' id ##] #H3;
    nelim (yields_eq ???? H3);
    #p3 e3; napply remove_res_sig; nwhd in ⊢ (??%?); nwhd in e3:(??%?); nrewrite > e3;
    nwhd in ⊢ (??%?); nrewrite > H2; napply refl;
##| #e ty sp l off tr H1 H2; 
    nelim (yields_eq ???? H2); ncases e; #e' ty';
    #p2 e2; napply remove_res_sig; nrewrite > e2;
    napply refl;
##| #ty' ty; napply refl;
##| #op e ty v1 v tr H1 H2 H3; napply remove_res_sig;
    nelim (yields_eq ???? H3); #p3 e3; nrewrite > e3;
    nwhd in ⊢ (??%?); nrewrite > H2; napply refl;
##| #op e1 e2 ty v1 v2 v tr1 tr2 H1 H2 e3 H4 H5; napply remove_res_sig;
    nelim (yields_eq ???? H4); #p4 e4; nrewrite > e4;
    nwhd in ⊢ (??%?);
    nelim (yields_eq ???? H5); #p5 e5; nrewrite > e5;
    nwhd in ⊢ (??%?);
    nrewrite > e3; napply refl;
##| #e1 e2 e3 ty v1 v2 tr1 tr2 H1 H2 H3 H4 H5; napply remove_res_sig;
    nelim (yields_eq ???? H4); #p4 e4; nrewrite > e4; nwhd in ⊢ (??%?);
    nelim (yields_eq ???? (bool_of_true ?? H2)); #p2 e2; nrewrite > e2;
    nelim (yields_eq ???? H5); #p5 e5; nrewrite > e5;
    napply refl;
##| #e1 e2 e3 ty v1 v2 tr1 tr2 H1 H2 H3 H4 H5; napply remove_res_sig;
    nelim (yields_eq ???? H4); #p4 e4; nrewrite > e4; nwhd in ⊢ (??%?);
    nelim (yields_eq ???? (bool_of_false ?? H2)); #p2 e2; nrewrite > e2;
    nelim (yields_eq ???? H5); #p5 e5; nrewrite > e5;
    napply refl;
##| #e1 e2 ty v1 tr H1 H2 H3; napply remove_res_sig;
    nelim (yields_eq ???? H3); #p3 e3; nrewrite > e3; nwhd in ⊢ (??%?);
    nelim (yields_eq ???? (bool_of_true ?? H2)); #p2 e2; nrewrite > e2;
    napply refl;    
##| #e1 e2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 H5 H6; napply remove_res_sig;
    nelim (yields_eq ???? H5); #p5 e5; nrewrite > e5; nwhd in ⊢ (??%?);
    nelim (yields_eq ???? (bool_of_false ?? H2)); #p2 e2; nrewrite > e2;
    nelim (yields_eq ???? H6); #p6 e6; nrewrite > e6; nwhd in ⊢ (??%?);
    nelim (bool_of_val_3_complete … H4); #b; *; #evb Hb;
    nelim (yields_eq ???? Hb); #pb eb; nrewrite > eb; nwhd in ⊢ (??%?); nrewrite < evb;
    napply refl;    
##| #e1 e2 ty v1 tr H1 H2 H3; napply remove_res_sig;
    nelim (yields_eq ???? H3); #p3 e3; nrewrite > e3; nwhd in ⊢ (??%?);
    nelim (yields_eq ???? (bool_of_false ?? H2)); #p2 e2; nrewrite > e2;
    napply refl;    
##| #e1 e2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 H5 H6; napply remove_res_sig;
    nelim (yields_eq ???? H5); #p5 e5; nrewrite > e5; nwhd in ⊢ (??%?);
    nelim (yields_eq ???? (bool_of_true ?? H2)); #p2 e2; nrewrite > e2;
    nelim (yields_eq ???? H6); #p6 e6; nrewrite > e6; nwhd in ⊢ (??%?);
    nelim (bool_of_val_3_complete … H4); #b; *; #evb Hb;
    nelim (yields_eq ???? Hb); #pb eb; nrewrite > eb; nwhd in ⊢ (??%?); nrewrite < evb;
    napply refl;
##| #e ty ty' v1 v tr H1 H2 H3; napply remove_res_sig;
    nelim (yields_eq ???? H3); #p3 e3; nrewrite > e3; nwhd in ⊢ (??%?);
    nelim (yields_eq ???? (cast_complete … H2)); #p2 e2; nrewrite > e2;
    napply refl;
##| #e ty v l tr H1 H2; napply remove_res_sig;
    nelim (yields_eq ???? H2); #p2 e2; nrewrite > e2; nwhd in ⊢ (??%?);
    napply refl;
  (* lvalues *)
 
 
 (* FIXME: next two cases produce type checking failures at nqed. *) 
##|napply daemon; (* #id l ty e1; nwhd in ⊢ (???%?); nrewrite > e1; napply refl;*)
##|napply daemon; (*#id sp l ty e1 e2; nwhd in ⊢ (???%?); napply (dep_option_rewrite ??????? e1);
    nrewrite > e2; napply refl;*)
##| #e ty sp l ofs tr H1 H2; napply remove_res_sig;
    nelim (yields_eq ???? H2); #p2 e2; nrewrite > e2; nwhd in ⊢ (??%?);
    napply refl;
##| (* careful!  Make sure we do the H2 rewrite before unfolding, or we end up
       in trouble because there's an equality proof floating around. *)
    #e i ty sp l ofs id fList delta tr H1 H2 H3 H4; ncases e in H2 H4 ⊢ %;
    #e' ty' H2; nwhd in H2:(??%?); nrewrite > H2; #H4; napply remove_res_sig;
    nelim (yields_eq ???? H4); #p4 e4; nrewrite > e4; nwhd in ⊢ (??%?);
    nrewrite > H3; napply refl;
##| #e i ty sp l ofs id fList tr; ncases e; #e' ty' H1 H2;
    nwhd in H2:(??%?); nrewrite > H2; #H3; napply remove_res_sig;
    nelim (yields_eq ???? H3); #p3 e3; nrewrite > e3; napply refl;
##] nqed.