include "Clight/Cexec.ma". definition yields ≝ λA.λa:res A.λv':A. match a with [ OK v ⇒ v' = v | _ ⇒ False ]. (* This tells us that some execution of a results in v'. (There may be many possible executions due to I/O, but we're trying to prove that one particular one exists corresponding to a derivation in the inductive semantics.) *) let rec yieldsIO (A:Type[0]) (a:IO io_out io_in A) (v':A) on a : Prop ≝ match a with [ Value v ⇒ v' = v | Interact _ k ⇒ ∃r.yieldsIO A (k r) v' | _ ⇒ False ]. definition yields_sig : ∀A,P. res (Sig A P) → A → Prop ≝ λA,P,e,v. match e with [ OK v' ⇒ match v' with [ dp v'' _ ⇒ v = v'' ] | _ ⇒ False]. let rec yieldsIO_sig (A:Type[0]) (P:A → Prop) (e:IO io_out io_in (Sig A P)) (v:A) on e : Prop ≝ match e with [ Value v' ⇒ match v' with [ dp v'' _ ⇒ v = v'' ] | Interact _ k ⇒ ∃r.yieldsIO_sig A P (k r) v | _ ⇒ False]. lemma remove_io_sig: ∀A. ∀P:A → Prop. ∀a,v',p. yieldsIO A a v' → yieldsIO_sig A P (io_inject io_out io_in A P (Some ? a) p) v'. #A #P #a elim a; [ #a #k #IH #v' #p #H whd in H ⊢ %; elim H; #r #H' %{ r} @IH @H' | #v #v' #p #H @H | #a #b #c *; ] qed. lemma yields_eq: ∀A,a,v'. yields A a v' → a = OK ? v'. #A #a #v' cases a; // #m whd in ⊢ (% → ?) *; qed. lemma yields_sig_eq: ∀A,P,e,v. yields_sig A P e v → ∃p. e = OK ? (dp … v p). #A #P #e #v cases e; [ #vp cases vp; #v' #p #H whd in H; >H %{ p} @refl | #m *; ] qed. lemma is_pointer_compat_true: ∀b,sp. pointer_compat b sp → is_pointer_compat b sp = true. #b #sp #H whd in ⊢ (??%?); elim (pointer_compat_dec b sp); [ // | #H' @False_ind @(absurd … H H') ] qed. lemma dec_true: ∀P:Prop.∀f:P + ¬P.∀p:P.∀Q:(P + ¬P) → Type[0]. (∀p'.Q (inl ?? p')) → Q f. #P #f #p #Q #H cases f; [ @H | #np cut False [ @(absurd ? p np) | * ] ] qed. lemma dec_false: ∀P:Prop.∀f:P + ¬P.∀p:¬P.∀Q:(P + ¬P) → Type[0]. (∀p'.Q (inr ?? p')) → Q f. #P #f #p #Q #H cases f; [ #np cut False [ @(absurd ? np p) | * ] | @H ] qed. theorem is_det: ∀p,s,s'. initial_state p s → initial_state p s' → s = s'. #p #s #s' #H1 #H2 inversion H1; #b1 #f1 #ge1 #m1 #e11 #e12 #e13 #e14 #e15 inversion H2; #b2 #f2 #ge2 #m2 #e21 #e22 #e23 #e24 #e25 >e11 in e21 #e1 >(?:ge1 = ge2) in e13 e14 [ 2: destruct (e1) skip (e11); @refl ] #e13 #e14 >e12 in e22 #e2 destruct (e2) skip (e12); >e13 in e23 #e3 >(?:b1 = b2) in e14 [ >e24 #e4 >(?:f2 = f1) [ //; | destruct (e4) skip (e24 e25); //; ] | destruct (e3) skip (e13); // ] qed. theorem the_initial_state: ∀p,s. initial_state p s → ∃ge. yields ? (make_initial_state p) 〈ge,s〉. #p #s cases p; #fns #main #globs #H inversion H; #b #f #ge #m #e1 #e2 #e3 #e4 #e5 %{ge} whd in ⊢ (??%?); >e1 whd in ⊢ (??%?); >e2 whd in ⊢ (??%?); >e3 whd in ⊢ (??%?); >e4 whd; @refl qed. lemma 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 elim H; [ #m #i #sz1 #sz2 #sg1 #sg2 @refl | #m #f #sz #szi #sg @refl | #m #i #sz #sz' #sg @refl | #m #f #sz #sz' @refl | #m #r #r' #ty #ty' #b #pc #ofs #H1 #H2 #pc' elim H1 in pc ⊢ % [ #r1 #ty1 #pc | #r1 #ty1 #n1 #pc | #tys1 #ty1 #pc letin r1 ≝ Code ] whd in ⊢ (??%?) [ 1,2: @(dec_true ? (eq_region_dec r1 r1) (refl ??) …) #H0 whd in ⊢ (??%?) ] elim H2 in pc' ⊢ %; [ 1,4,7: #sp2 #ty2 | 2,5,8: #sp2 #ty2 #n2 | 3,6,9: #tys2 #ty2 letin sp2 ≝ Code ] #pc' whd in ⊢ (??%?) @(dec_true ? (pointer_compat_dec b sp2) pc') // | #m #sz #si #ty'' #r #H cases H; //; | #m #t #t' #r #r' #H #H' cases H; try #a try #b try #c cases H'; try #d try #e try #f whd in ⊢ (??%?); try @refl @(dec_true ? (eq_region_dec a a) (refl ??)) #H0 @refl ] qed. (* Use to narrow down the choice of expression to just the lvalues. *) lemma lvalue_expr: ∀ge,env,m,e,ty,l,ofs,tr. ∀P:expr_descr → Prop. eval_lvalue ge env m (Expr e ty) l ofs tr → (∀id. P (Evar id)) → (∀e'. P (Ederef e')) → (∀e',id. P (Efield e' id)) → P e. #ge #env #m #e #ty #l #ofs #tr #P #H @(eval_lvalue_inv_ind … H) [ #id #l #ty #e1 #e2 #e3 #e4 #e5 #e6 destruct; // | #id #sp #l #ty #e1 #e2 #e3 #e4 #e5 #e6 #e7 destruct; // | #e #ty #sp #l #ofs #tr #H #e1 #e2 #e3 #e4 #e5 destruct; // | #e #id #ty #l #ofs #id' #fs #d #tr #H #e1 #e2 (* bogus? *) #_ #e3 #e4 #e5 #e6 #e7 destruct; // | #e #id #ty #l #ofs #id' #fs #tr #H #e1 (* bogus? *) #_ #e2 #e3 #e4 #e5 #e6 destruct; // ] qed. lemma bool_of_val_3_complete : ∀v,ty,r. bool_of_val v ty r → ∃b. r = of_bool b ∧ yields ? (exec_bool_of_val v ty) b. #v #ty #r #H elim H; #v #t #H' elim H'; [ #i #is #s #ne %{ true} % //; whd; >(eq_false … ne) //; | #r #b #pc #i #i0 #s %{ true} % // | #f #s #ne %{ true} % //; whd; >(Feq_zero_false … ne) //; | #i #s %{ false} % //; | #r #r' #t %{ false} % //; | #s %{ false} % //; whd; >(Feq_zero_true …) //; ] qed. lemma bool_of_true: ∀v,ty. is_true v ty → yields ? (exec_bool_of_val v ty) true. #v #ty #H elim H; [ #i #is #s #ne whd; >(eq_false … ne) //; | #p #b #i #i0 #s // | #f #s #ne whd; >(Feq_zero_false … ne) //; ] qed. lemma bool_of_false: ∀v,ty. is_false v ty → yields ? (exec_bool_of_val v ty) false. #v #ty #H elim H; [ #i #s //; | #r #r' #t //; | #s whd; >(Feq_zero_true …) //; ] qed. lemma expr_lvalue_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,l,off,tr. eval_lvalue ge env m e l off tr → yields ? (exec_lvalue ge env m e) (〈〈l,off〉,tr〉)). #ge #env #m @(combined_expr_lvalue_ind ge env m (λe,v,tr,H. yields ? (exec_expr ge env m e) (〈v,tr〉)) (λe,l,off,tr,H. yields ? (exec_lvalue ge env m e) (〈〈l,off〉,tr〉))); [ #i #ty @refl | #f #ty @refl | #e #ty #l #off #v #tr #H1 #H2 @(lvalue_expr … H1) [ #id | #e' | #e' #id ] #H3 whd in ⊢ (??%?); >(yields_eq ??? H3) whd in ⊢ (??%?); >H2 @refl | #e #ty #r #l #pc #off #tr #H1 #H2 whd in ⊢ (??%?); >(yields_eq ??? H2) whd in ⊢ (??%?) @(dec_true ? (pointer_compat_dec l r) pc) #pc' whd @refl | #ty' #ty @refl | #op #e #ty #v1 #v #tr #H1 #H2 #H3 whd in ⊢ (??%?); >(yields_eq ??? H3) whd in ⊢ (??%?); >H2 @refl | #op #e1 #e2 #ty #v1 #v2 #v #tr1 #tr2 #H1 #H2 #e3 #H4 #H5 whd in ⊢ (??%?); >(yields_eq ??? H4) whd in ⊢ (??%?); >(yields_eq ??? H5) whd in ⊢ (??%?); >e3 @refl | #e1 #e2 #e3 #ty #v1 #v2 #tr1 #tr2 #H1 #H2 #H3 #H4 #H5 whd in ⊢ (??%?); >(yields_eq ??? H4) whd in ⊢ (??%?); >(yields_eq ??? (bool_of_true ?? H2)) >(yields_eq ??? H5) @refl | #e1 #e2 #e3 #ty #v1 #v2 #tr1 #tr2 #H1 #H2 #H3 #H4 #H5 whd in ⊢ (??%?); >(yields_eq ??? H4) whd in ⊢ (??%?); >(yields_eq ??? (bool_of_false ?? H2)) >(yields_eq ??? H5) @refl | #e1 #e2 #ty #v1 #tr #H1 #H2 #H3 whd in ⊢ (??%?); >(yields_eq ??? H3) whd in ⊢ (??%?); >(yields_eq ??? (bool_of_true ?? H2)) @refl | #e1 #e2 #ty #v1 #v2 #v #tr1 #tr2 #H1 #H2 #H3 #H4 #H5 #H6 whd in ⊢ (??%?); >(yields_eq ??? H5) whd in ⊢ (??%?); >(yields_eq ??? (bool_of_false ?? H2)) >(yields_eq ??? H6) whd in ⊢ (??%?); elim (bool_of_val_3_complete … H4); #b *; #evb #Hb >(yields_eq ??? Hb) whd in ⊢ (??%?); (yields_eq ??? H3) whd in ⊢ (??%?); >(yields_eq ??? (bool_of_false ?? H2)) @refl | #e1 #e2 #ty #v1 #v2 #v #tr1 #tr2 #H1 #H2 #H3 #H4 #H5 #H6 whd in ⊢ (??%?); >(yields_eq ??? H5) whd in ⊢ (??%?); >(yields_eq ??? (bool_of_true ?? H2)) >(yields_eq ??? H6) whd in ⊢ (??%?); elim (bool_of_val_3_complete … H4); #b *; #evb #Hb >(yields_eq ??? Hb) whd in ⊢ (??%?); (yields_eq ??? H3) whd in ⊢ (??%?); >(yields_eq ??? (cast_complete … H2)) @refl | #e #ty #v #l #tr #H1 #H2 whd in ⊢ (??%?); >(yields_eq ??? H2) whd in ⊢ (??%?); @refl (* lvalues *) | #id #l #ty #e1 whd in ⊢ (??%?); >e1 @refl | #id #l #ty #e1 #e2 whd in ⊢ (??%?); >e1 >e2 @refl | #e #ty #r #l #pc #ofs #tr #H1 #H2 whd in ⊢ (??%?); >(yields_eq ??? H2) @refl | #e #i #ty #l #ofs #id #fList #delta #tr #H1 #H2 #H3 #H4 cases e in H2 H4 ⊢ %; #e' #ty' #H2 whd in H2:(??%?); >H2 #H4 whd in ⊢ (??%?); >(yields_eq ??? H4) whd in ⊢ (??%?); >H3 @refl | #e #i #ty #l #ofs #id #fList #tr cases e; #e' #ty' #H1 #H2 whd in H2:(??%?); >H2 #H3 whd in ⊢ (??%?); >(yields_eq ??? H3) @refl ] qed. theorem 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〉). #ge #env #m elim (expr_lvalue_complete ge env m); /2/; qed. theorem exprlist_complete: ∀ge,env,m,es,vs,tr. eval_exprlist ge env m es vs tr → yields ? (exec_exprlist ge env m es) (〈vs,tr〉). #ge #env #m #es #vs #tr #H elim H; [ @refl | #e #et #v #vt #tr #trt #H1 #H2 #H3 whd in ⊢ (??%?); >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?); >(yields_eq ??? H3) @refl ] qed. theorem lvalue_complete: ∀ge,env,m. ∀e,l,off,tr. eval_lvalue ge env m e l off tr → yields ? (exec_lvalue ge env m e) (〈〈l,off〉,tr〉). #ge #env #m elim (expr_lvalue_complete ge env m); /2/; qed. let rec P_typelist (P:type → Prop) (l:typelist) on l : Prop ≝ match l with [ Tnil ⇒ True | Tcons h t ⇒ P h ∧ P_typelist P t ]. let rec type_ind2l (P:type → Prop) (Q:typelist → Prop) (vo:P Tvoid) (it:∀i,s. P (Tint i s)) (fl:∀f. P (Tfloat f)) (pt:∀s,t. P t → P (Tpointer s t)) (ar:∀s,t,n. P t → P (Tarray s t n)) (fn:∀tl,t. Q tl → P t → P (Tfunction tl t)) (st:∀i,fl. P (Tstruct i fl)) (un:∀i,fl. P (Tunion i fl)) (cp:∀r,i. P (Tcomp_ptr r i)) (nl:Q Tnil) (cs:∀t,tl. P t → Q tl → Q (Tcons t tl)) (t:type) on t : P t ≝ match t return λt'.P t' with [ Tvoid ⇒ vo | Tint i s ⇒ it i s | Tfloat s ⇒ fl s | Tpointer s t' ⇒ pt s t' (type_ind2l P Q vo it fl pt ar fn st un cp nl cs t') | Tarray s t' n ⇒ ar s t' n (type_ind2l P Q vo it fl pt ar fn st un cp nl cs t') | Tfunction tl t' ⇒ fn tl t' (typelist_ind2l P Q vo it fl pt ar fn st un cp nl cs tl) (type_ind2l P Q vo it fl pt ar fn st un cp nl cs t') | Tstruct i fs ⇒ st i fs | Tunion i fs ⇒ un i fs | Tcomp_ptr r i ⇒ cp r i ] and typelist_ind2l (P:type → Prop) (Q:typelist → Prop) (vo:P Tvoid) (it:∀i,s. P (Tint i s)) (fl:∀f. P (Tfloat f)) (pt:∀s,t. P t → P (Tpointer s t)) (ar:∀s,t,n. P t → P (Tarray s t n)) (fn:∀tl,t. Q tl → P t → P (Tfunction tl t)) (st:∀i,fl. P (Tstruct i fl)) (un:∀i,fl. P (Tunion i fl)) (cp:∀r,i. P (Tcomp_ptr r i)) (nl:Q Tnil) (cs:∀t,tl. P t → Q tl → Q (Tcons t tl)) (ts:typelist) on ts : Q ts ≝ match ts return λts'.Q ts' with [ Tnil ⇒ nl | Tcons t tl ⇒ cs t tl (type_ind2l P Q vo it fl pt ar fn st un cp nl cs t) (typelist_ind2l P Q vo it fl pt ar fn st un cp nl cs tl) ]. lemma assert_type_eq_true: ∀t. ∃p.assert_type_eq t t = OK ? p. #t whd in ⊢ (??(λ_.??%?)); cases (type_eq_dec t t); #E [ %{ E} // | @False_ind @(absurd ?? E) // ] qed. lemma alloc_vars_complete: ∀env,m,l,env',m'. alloc_variables env m l env' m' → exec_alloc_variables env m l = 〈env', m'〉. #env #m #l #env' #m' #H elim H; [ #env'' #m'' % | #env1 #m1 #id #ty #l1 #m2 #loc #m3 #env2 #H1 #H2 #H3 < H3 whd in H1:(??%?) ⊢ (??%?) destruct (H1) @refl ] qed. lemma bind_params_complete: ∀e,m,params,vs,m2. bind_parameters e m params vs m2 → yields ? (exec_bind_parameters e m params vs) m2. #e #m #params #vs #m2 #H elim H; [ //; | #env1 #m1 #id #ty #l #v #tl #loc #m2 #m3 #H1 #H2 #H3 #H4 whd in ⊢ (??%?) >H1 whd in ⊢ (??%?); >H2 whd in ⊢ (??%?); @H4 ] qed. lemma eventval_match_complete': ∀ev,ty,v. eventval_match ev ty v → yields ? (check_eventval' v ty) ev. #ev #ty #v #H elim H; //; qed. lemma eventval_list_match_complete: ∀vs,tys,evs. eventval_list_match evs tys vs → yields ? (check_eventval_list vs tys) evs. #vs #tys #evs #H elim H; [ // | #e #etl #ty #tytl #v #vtl #H1 #H2 #H3 whd in ⊢ (??%?) >(yields_eq ??? (eventval_match_complete' … H1)) whd in ⊢ (??%?) >(yields_eq ??? H3) whd in ⊢ (??%?) // ] qed. theorem step_complete: ∀ge,s,tr,s'. step ge s tr s' → yieldsIO ? (exec_step ge s) 〈tr,s'〉. #ge #s #tr #s' #H elim H; [ #f #e #e1 #k #e2 #m #loc #ofs #v #m' #tr1 #tr2 #H1 #H2 #H3 whd in ⊢ (??%?); >(yields_eq ??? (lvalue_complete … H1)) whd in ⊢ (??%?); >(yields_eq ??? (expr_complete … H2)) whd in ⊢ (??%?); >H3 @refl | #f #e #eargs #k #ef #m #vf #vargs #f' #tr1 #tr2 #H1 #H2 #H3 #H4 whd in ⊢ (??%?); >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?); >(yields_eq ??? (exprlist_complete … H2)) whd in ⊢ (??%?); >H3 whd in ⊢ (??%?); >H4 elim (assert_type_eq_true (fun_typeof e)); #pty #ety >ety @refl | #f #el #ef #eargs #k #env #m #loc #ofs #vf #vargs #f' #tr1 #tr2 #tr3 #H1 #H2 #H3 #H4 #H5 whd in ⊢ (??%?); >(yields_eq ??? (expr_complete … H2)) whd in ⊢ (??%?); >(yields_eq ??? (exprlist_complete … H3)) whd in ⊢ (??%?); >H4 whd in ⊢ (??%?); >H5 elim (assert_type_eq_true (fun_typeof ef)); #pty #ety >ety whd in ⊢ (??%?); >(yields_eq ??? (lvalue_complete … H1)) whd in ⊢ (??%?); @refl | #f #s1 #s2 #k #env #m @refl | 5,6,7: #f #s #k #env #m @refl | #f #e #s1 #s2 #k #env #m #v #tr #H1 #H2 whd in ⊢ (??%?); >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?); >(yields_eq ??? (bool_of_true ?? H2)) @refl | #f #e #s1 #s2 #k #env #m #v #tr #H1 #H2 whd in ⊢ (??%?); >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?); >(yields_eq ??? (bool_of_false ?? H2)) @refl | #f #e #s #k #env #m #v #tr #H1 #H2 whd in ⊢ (??%?); >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?); >(yields_eq ??? (bool_of_false ?? H2)) @refl | #f #e #s #k #env #m #v #tr #H1 #H2 whd in ⊢ (??%?); >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?); >(yields_eq ??? (bool_of_true ?? H2)) @refl | #f #s1 #e #s2 #k #env #m #H cases H; #es1 >es1 @refl | 13,14: #f #e #s #k #env #m @refl | #f #s1 #e #s2 #k #env #m #v #tr *; #es1 >es1 #H1 #H2 whd in ⊢ (??%?); >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?); >(yields_eq ??? (bool_of_false ?? H2)) @refl | #f #s1 #e #s2 #k #env #m #v #tr *; #es1 >es1 #H1 #H2 whd in ⊢ (??%?); >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?); >(yields_eq ??? (bool_of_true ?? H2)) @refl | #f #e #s #k #env #m @refl | #f #s1 #e #s2 #s3 #k #env #m #nskip whd in ⊢ (??%?); cases (is_Sskip s1); [ #H @False_ind @(absurd ? H nskip) | #H whd in ⊢ (??%?); @refl ] | #f #e #s1 #s2 #k #env #m #v #tr #H1 #H2 whd in ⊢ (??%?); >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?); >(yields_eq ??? (bool_of_false ?? H2)) @refl | #f #e #s1 #s2 #k #env #m #v #tr #H1 #H2 whd in ⊢ (??%?); >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?); >(yields_eq ??? (bool_of_true ?? H2)) @refl | #f #s1 #e #s2 #s3 #k #env #m *; #es1 >es1 @refl | 22,23: #f #e #s1 #s2 #k #env #m @refl | #f #k #env #m #H whd in ⊢ (??%?); >H @refl | #f #e #k #env #m #v #tr #H1 #H2 whd in ⊢ (??%?); @(dec_false ? (type_eq_dec (fn_return f) Tvoid) H1) #pf' whd in ⊢ (??%?); >(yields_eq ??? (expr_complete … H2)) whd in ⊢ (??%?); @refl | #f #k #env #m cases k; [ #H1 #H2 whd in ⊢ (??%?); >H2 @refl | #s' #k' whd in ⊢ (% → ?); *; | 3,4: #e' #s' #k' whd in ⊢ (% → ?); *; | 5,6: #e' #s1' #s2' #k' whd in ⊢ (% → ?); *; | #k' whd in ⊢ (% → ?); *; | #r #f' #env' #k' #H1 #H2 whd in ⊢ (??%?); >H2 @refl ] | #f #e #s #k #env #m #i #tr #H1 whd in ⊢ (??%?); >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?); @refl | #f #s #k #env #m *; #es >es @refl | #f #k #env #m @refl | #f #l #s #k #env #m @refl | #f #l #k #env #m #s #k' #H1 whd in ⊢ (??%?); >H1 @refl | #f #args #k #m1 #env #m2 #m3 #H1 #H2 whd in ⊢ (??%?); >(alloc_vars_complete … H1) whd in ⊢ (??%?); >(yields_eq ??? (bind_params_complete … H2)) // | #id #tys #rty #args #k #m #rv #tr #H whd in ⊢ (??%?); inversion H; #f' #args' #rv' #eargs #erv #H1 #H2 #e1 #e2 #e3 #e4 (yields_eq ??? (eventval_list_match_complete … H1)) whd in ⊢ (??%?); whd; inversion H2; #x #e5 #e6 #e7 %{ x} whd in ⊢ (??%?); @refl | #v #f #env #k #m @refl | #v #f #env #k #m1 #m2 #loc #ofs #ty #H whd in ⊢ (??%?); >H @refl | #f #l #s #k #env #m @refl ] qed. lemma is_final_complete : ∀s,r. final_state s r → is_final s = Some ? r. #s0 #r0 * #r #m @refl qed.