[700] | 1 | include "Clight/Cexec.ma". |
---|
[226] | 2 | |
---|
[487] | 3 | definition yields ≝ λA.λa:res A.λv':A. |
---|
[399] | 4 | match a with [ OK v ⇒ v' = v | _ ⇒ False ]. |
---|
[239] | 5 | |
---|
[399] | 6 | (* This tells us that some execution of a results in v'. |
---|
[239] | 7 | (There may be many possible executions due to I/O, but we're trying to prove |
---|
| 8 | that one particular one exists corresponding to a derivation in the inductive |
---|
| 9 | semantics.) *) |
---|
[487] | 10 | let rec yieldsIO (A:Type[0]) (a:IO io_out io_in A) (v':A) on a : Prop ≝ |
---|
[399] | 11 | match a with [ Value v ⇒ v' = v | Interact _ k ⇒ ∃r.yieldsIO A (k r) v' | _ ⇒ False ]. |
---|
| 12 | |
---|
[487] | 13 | definition yields_sig : ∀A,P. res (Sig A P) → A → Prop ≝ |
---|
[1603] | 14 | λA,P,e,v. match e with [ OK v' ⇒ match v' with [ mk_Sig v'' _ ⇒ v = v'' ] | _ ⇒ False]. |
---|
[399] | 15 | |
---|
[487] | 16 | let rec yieldsIO_sig (A:Type[0]) (P:A → Prop) (e:IO io_out io_in (Sig A P)) (v:A) on e : Prop ≝ |
---|
[239] | 17 | match e with |
---|
[1603] | 18 | [ Value v' ⇒ match v' with [ mk_Sig v'' _ ⇒ v = v'' ] |
---|
[399] | 19 | | Interact _ k ⇒ ∃r.yieldsIO_sig A P (k r) v |
---|
[239] | 20 | | _ ⇒ False]. |
---|
| 21 | |
---|
[487] | 22 | lemma remove_io_sig: ∀A. ∀P:A → Prop. ∀a,v',p. |
---|
[399] | 23 | yieldsIO A a v' → |
---|
[487] | 24 | yieldsIO_sig A P (io_inject io_out io_in A P (Some ? a) p) v'. |
---|
| 25 | #A #P #a elim a; |
---|
| 26 | [ #a #k #IH #v' #p #H whd in H ⊢ %; elim H; #r #H' %{ r} @IH @H' |
---|
| 27 | | #v #v' #p #H @H |
---|
[797] | 28 | | #a #b #c *; |
---|
[487] | 29 | ] qed. |
---|
[399] | 30 | |
---|
[487] | 31 | lemma yields_eq: ∀A,a,v'. yields A a v' → a = OK ? v'. |
---|
[1516] | 32 | #A #a #v' cases a; // #m whd in ⊢ (% → ?); *; |
---|
[487] | 33 | qed. |
---|
[399] | 34 | |
---|
[1603] | 35 | lemma yields_sig_eq: ∀A,P,e,v. yields_sig A P e v → ∃p. e = OK ? (mk_Sig … v p). |
---|
[487] | 36 | #A #P #e #v cases e; |
---|
| 37 | [ #vp cases vp; #v' #p #H whd in H; >H %{ p} @refl |
---|
[797] | 38 | | #m *; |
---|
[487] | 39 | ] qed. |
---|
[399] | 40 | |
---|
[499] | 41 | lemma is_pointer_compat_true: ∀b,sp. |
---|
| 42 | pointer_compat b sp → |
---|
| 43 | is_pointer_compat b sp = true. |
---|
| 44 | #b #sp #H whd in ⊢ (??%?); |
---|
| 45 | elim (pointer_compat_dec b sp); |
---|
[487] | 46 | [ // |
---|
| 47 | | #H' @False_ind @(absurd … H H') |
---|
| 48 | ] qed. |
---|
[226] | 49 | |
---|
[500] | 50 | lemma dec_true: ∀P:Prop.∀f:P + ¬P.∀p:P.∀Q:(P + ¬P) → Type[0]. (∀p'.Q (inl ?? p')) → Q f. |
---|
| 51 | #P #f #p #Q #H cases f; |
---|
| 52 | [ @H |
---|
| 53 | | #np cut False [ @(absurd ? p np) | * ] |
---|
[487] | 54 | ] qed. |
---|
[226] | 55 | |
---|
[500] | 56 | lemma dec_false: ∀P:Prop.∀f:P + ¬P.∀p:¬P.∀Q:(P + ¬P) → Type[0]. (∀p'.Q (inr ?? p')) → Q f. |
---|
| 57 | #P #f #p #Q #H cases f; |
---|
| 58 | [ #np cut False [ @(absurd ? np p) | * ] |
---|
| 59 | | @H |
---|
| 60 | ] qed. |
---|
| 61 | |
---|
[487] | 62 | theorem is_det: ∀p,s,s'. |
---|
[226] | 63 | initial_state p s → initial_state p s' → s = s'. |
---|
[487] | 64 | #p #s #s' #H1 #H2 |
---|
[1510] | 65 | inversion H1; #b1 #f1 #ge1 #m1 #e11 #e12 #e13 #e14 #e15 #e16 |
---|
| 66 | inversion H2; #b2 #f2 #ge2 #m2 #e21 #e22 #e23 #e24 #e25 #e26 |
---|
[1516] | 67 | >e11 in e21; #e1 >(?:ge1 = ge2) in e13 e14; |
---|
[487] | 68 | [ 2: destruct (e1) skip (e11); @refl ] |
---|
| 69 | #e13 #e14 |
---|
[485] | 70 | |
---|
[1516] | 71 | >e12 in e22; #e2 destruct (e2) skip (e12); |
---|
[485] | 72 | |
---|
[1516] | 73 | >e13 in e23; #e3 >(?:b1 = b2) in e14; |
---|
[487] | 74 | [ >e24 #e4 >(?:f2 = f1) |
---|
| 75 | [ //; |
---|
| 76 | | destruct (e4) skip (e24 e25); //; |
---|
| 77 | ] |
---|
| 78 | | destruct (e3) skip (e13); // |
---|
| 79 | ] qed. |
---|
[226] | 80 | |
---|
| 81 | |
---|
[487] | 82 | theorem the_initial_state: |
---|
[1244] | 83 | ∀p,s. initial_state p s → yields ? (make_initial_state p) s. |
---|
| 84 | #p #s cases p; #globs #fns #main #H |
---|
[487] | 85 | inversion H; |
---|
[1510] | 86 | #b #f #ge #m #e1 #e2 #e3 #e4 #e5 #e6 |
---|
[487] | 87 | whd in ⊢ (??%?); |
---|
| 88 | >e2 |
---|
| 89 | whd in ⊢ (??%?); |
---|
[1521] | 90 | change with (make_global (mk_program ?? globs fns main)) in e1:(??%?); |
---|
[1244] | 91 | >e1 |
---|
[487] | 92 | >e3 |
---|
| 93 | whd in ⊢ (??%?); |
---|
| 94 | >e4 |
---|
| 95 | whd; @refl |
---|
| 96 | qed. |
---|
[385] | 97 | |
---|
[487] | 98 | lemma cast_complete: ∀m,v,ty,ty',v'. |
---|
[399] | 99 | cast m v ty ty' v' → yields ? (exec_cast m v ty ty') v'. |
---|
[487] | 100 | #m #v #ty #ty' #v' #H |
---|
| 101 | elim H; |
---|
[1516] | 102 | [ #m #sz1 #sz2 #sg1 #sg2 #i whd in ⊢ (??%?); >intsize_eq_elim_true @refl |
---|
[487] | 103 | | #m #f #sz #szi #sg @refl |
---|
[1516] | 104 | | #m #sz #sz' #sg #i whd in ⊢ (??%?); >intsize_eq_elim_true @refl |
---|
[487] | 105 | | #m #f #sz #sz' @refl |
---|
[1545] | 106 | | #m #ty #ty' * #r #b #pc #ofs #r' #H1 #H2 #pc' |
---|
[1516] | 107 | elim H1 in pc ⊢ %; [ #r1 #ty1 #pc | #r1 #ty1 #n1 #pc | #tys1 #ty1 #pc letin r1 ≝ Code ] |
---|
| 108 | whd in ⊢ (??%?); |
---|
| 109 | [ 1,2: @(dec_true ? (eq_region_dec r1 r1) (refl ??) …) #H0 whd in ⊢ (??%?); ] |
---|
[500] | 110 | elim H2 in pc' ⊢ %; [ 1,4,7: #sp2 #ty2 | 2,5,8: #sp2 #ty2 #n2 | 3,6,9: #tys2 #ty2 letin sp2 ≝ Code ] |
---|
[1516] | 111 | #pc' whd in ⊢ (??%?); |
---|
[500] | 112 | @(dec_true ? (pointer_compat_dec b sp2) pc') // |
---|
[1516] | 113 | | #m #sz #si #ty'' #r #H cases H; [ #s #t | #s #t #n | #tys #ty0 ] whd in ⊢ (??%?); |
---|
| 114 | >intsize_eq_elim_true whd in ⊢ (??%?); cases sz //; |
---|
[487] | 115 | | #m #t #t' #r #r' #H #H' cases H; try #a try #b try #c cases H'; try #d try #e try #f |
---|
[500] | 116 | whd in ⊢ (??%?); try @refl @(dec_true ? (eq_region_dec a a) (refl ??)) #H0 @refl |
---|
[487] | 117 | ] qed. |
---|
[226] | 118 | |
---|
| 119 | (* Use to narrow down the choice of expression to just the lvalues. *) |
---|
[498] | 120 | lemma lvalue_expr: ∀ge,env,m,e,ty,l,ofs,tr. ∀P:expr_descr → Prop. |
---|
| 121 | eval_lvalue ge env m (Expr e ty) l ofs tr → |
---|
[226] | 122 | (∀id. P (Evar id)) → (∀e'. P (Ederef e')) → (∀e',id. P (Efield e' id)) → |
---|
| 123 | P e. |
---|
[498] | 124 | #ge #env #m #e #ty #l #ofs #tr #P #H @(eval_lvalue_inv_ind … H) |
---|
[1566] | 125 | [ #id #l' #ty' #e1 #e2 #e3 #e4 #e5 #e6 destruct; // |
---|
| 126 | | #id #sp #l' #ty' #e1 #e2 #e3 #e4 #e5 #e6 #e7 destruct; // |
---|
| 127 | | #e' #ty' #sp #l' #ofs #tr #H #e1 #e2 #e3 #e4 #e5 destruct; // |
---|
| 128 | | #e' #id #ty' #l' #ofs #id' #fs #d #tr #H #e1 #e2 (* bogus? *) #_ #e3 #e4 #e5 #e6 #e7 destruct; // |
---|
| 129 | | #e' #id #ty' #l' #ofs #id' #fs #tr #H #e1 (* bogus? *) #_ #e2 #e3 #e4 #e5 #e6 destruct; // |
---|
[487] | 130 | ] qed. |
---|
[226] | 131 | |
---|
[487] | 132 | 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. |
---|
| 133 | #v #ty #r #H elim H; #v #t #H' elim H'; |
---|
[1516] | 134 | [ #sz #sg #i #ne %{ true} % //; whd in ⊢ (??%?); >intsize_eq_elim_true |
---|
[961] | 135 | >(eq_bv_false … ne) // |
---|
[1545] | 136 | | * #r #b #pc #i #i0 #s %{ true} % // |
---|
[487] | 137 | | #f #s #ne %{ true} % //; whd; >(Feq_zero_false … ne) //; |
---|
[1516] | 138 | | #sz #sg %{ false} % // whd in ⊢ (??%?); >intsize_eq_elim_true >eq_bv_true // |
---|
[487] | 139 | | #r #r' #t %{ false} % //; |
---|
| 140 | | #s %{ false} % //; whd; >(Feq_zero_true …) //; |
---|
| 141 | ] |
---|
| 142 | qed. |
---|
[226] | 143 | |
---|
[487] | 144 | lemma bool_of_true: ∀v,ty. is_true v ty → yields ? (exec_bool_of_val v ty) true. |
---|
| 145 | #v #ty #H elim H; |
---|
[1516] | 146 | [ #i #is #s #ne whd in ⊢ (??%?); >intsize_eq_elim_true >(eq_bv_false … ne) //; |
---|
[1545] | 147 | | * #p #b #i #i0 #s // |
---|
[487] | 148 | | #f #s #ne whd; >(Feq_zero_false … ne) //; |
---|
| 149 | ] |
---|
| 150 | qed. |
---|
[226] | 151 | |
---|
[487] | 152 | lemma bool_of_false: ∀v,ty. is_false v ty → yields ? (exec_bool_of_val v ty) false. |
---|
| 153 | #v #ty #H elim H; |
---|
[1516] | 154 | [ #sz #sg whd in ⊢ (??%?); >intsize_eq_elim_true >eq_bv_true //; |
---|
[487] | 155 | | #r #r' #t //; |
---|
| 156 | | #s whd; >(Feq_zero_true …) //; |
---|
| 157 | ] |
---|
| 158 | qed. |
---|
[226] | 159 | |
---|
[487] | 160 | lemma expr_lvalue_complete: ∀ge,env,m. |
---|
[399] | 161 | (∀e,v,tr. eval_expr ge env m e v tr → yields ? (exec_expr ge env m e) (〈v,tr〉)) ∧ |
---|
[498] | 162 | (∀e,l,off,tr. eval_lvalue ge env m e l off tr → yields ? (exec_lvalue ge env m e) (〈〈l,off〉,tr〉)). |
---|
[487] | 163 | #ge #env #m |
---|
| 164 | @(combined_expr_lvalue_ind ge env m |
---|
[399] | 165 | (λe,v,tr,H. yields ? (exec_expr ge env m e) (〈v,tr〉)) |
---|
[498] | 166 | (λe,l,off,tr,H. yields ? (exec_lvalue ge env m e) (〈〈l,off〉,tr〉))); |
---|
[1516] | 167 | [ #sz #sg #i whd in ⊢ (??%?); >eq_intsize_true @refl |
---|
[487] | 168 | | #f #ty @refl |
---|
[498] | 169 | | #e #ty #l #off #v #tr #H1 #H2 @(lvalue_expr … H1) |
---|
[487] | 170 | [ #id | #e' | #e' #id ] #H3 |
---|
[1516] | 171 | whd in ⊢ (??%?); |
---|
[1521] | 172 | [ change with (exec_lvalue' ge env m (Evar id) ty) in H3:(??%?); |
---|
| 173 | | change with (exec_lvalue' ge env m (Ederef e') ty) in H3:(??%?); |
---|
| 174 | | change with (exec_lvalue' ge env m (Efield e' id) ty) in H3:(??%?); |
---|
[891] | 175 | ] |
---|
[487] | 176 | >(yields_eq ??? H3) |
---|
[1521] | 177 | whd in ⊢ (??%?); change with (load_value_of_type' ty m 〈l,off〉) in H2:(??%?); |
---|
[891] | 178 | >H2 @refl |
---|
[500] | 179 | | #e #ty #r #l #pc #off #tr #H1 #H2 whd in ⊢ (??%?); |
---|
[1516] | 180 | >(yields_eq ??? H2) whd in ⊢ (??%?); |
---|
[500] | 181 | @(dec_true ? (pointer_compat_dec l r) pc) #pc' whd |
---|
[487] | 182 | @refl |
---|
[961] | 183 | | #ty' #sz #sg @refl |
---|
[487] | 184 | | #op #e #ty #v1 #v #tr #H1 #H2 #H3 whd in ⊢ (??%?); |
---|
| 185 | >(yields_eq ??? H3) |
---|
| 186 | whd in ⊢ (??%?); >H2 @refl |
---|
| 187 | | #op #e1 #e2 #ty #v1 #v2 #v #tr1 #tr2 #H1 #H2 #e3 #H4 #H5 whd in ⊢ (??%?); |
---|
| 188 | >(yields_eq ??? H4) whd in ⊢ (??%?); |
---|
| 189 | >(yields_eq ??? H5) whd in ⊢ (??%?); |
---|
| 190 | >e3 @refl |
---|
| 191 | | #e1 #e2 #e3 #ty #v1 #v2 #tr1 #tr2 #H1 #H2 #H3 #H4 #H5 whd in ⊢ (??%?); |
---|
| 192 | >(yields_eq ??? H4) whd in ⊢ (??%?); |
---|
| 193 | >(yields_eq ??? (bool_of_true ?? H2)) |
---|
| 194 | >(yields_eq ??? H5) |
---|
| 195 | @refl |
---|
| 196 | | #e1 #e2 #e3 #ty #v1 #v2 #tr1 #tr2 #H1 #H2 #H3 #H4 #H5 whd in ⊢ (??%?); |
---|
| 197 | >(yields_eq ??? H4) whd in ⊢ (??%?); |
---|
| 198 | >(yields_eq ??? (bool_of_false ?? H2)) |
---|
| 199 | >(yields_eq ??? H5) |
---|
| 200 | @refl |
---|
| 201 | | #e1 #e2 #ty #v1 #tr #H1 #H2 #H3 whd in ⊢ (??%?); |
---|
| 202 | >(yields_eq ??? H3) whd in ⊢ (??%?); |
---|
| 203 | >(yields_eq ??? (bool_of_true ?? H2)) |
---|
| 204 | @refl |
---|
| 205 | | #e1 #e2 #ty #v1 #v2 #v #tr1 #tr2 #H1 #H2 #H3 #H4 #H5 #H6 whd in ⊢ (??%?); |
---|
| 206 | >(yields_eq ??? H5) whd in ⊢ (??%?); |
---|
| 207 | >(yields_eq ??? (bool_of_false ?? H2)) |
---|
| 208 | >(yields_eq ??? H6) whd in ⊢ (??%?); |
---|
| 209 | elim (bool_of_val_3_complete … H4); #b *; #evb #Hb |
---|
| 210 | >(yields_eq ??? Hb) whd in ⊢ (??%?); <evb |
---|
| 211 | @refl |
---|
| 212 | | #e1 #e2 #ty #v1 #tr #H1 #H2 #H3 whd in ⊢ (??%?); |
---|
| 213 | >(yields_eq ??? H3) whd in ⊢ (??%?); |
---|
| 214 | >(yields_eq ??? (bool_of_false ?? H2)) |
---|
| 215 | @refl |
---|
| 216 | | #e1 #e2 #ty #v1 #v2 #v #tr1 #tr2 #H1 #H2 #H3 #H4 #H5 #H6 whd in ⊢ (??%?); |
---|
| 217 | >(yields_eq ??? H5) whd in ⊢ (??%?); |
---|
| 218 | >(yields_eq ??? (bool_of_true ?? H2)) |
---|
| 219 | >(yields_eq ??? H6) whd in ⊢ (??%?); |
---|
| 220 | elim (bool_of_val_3_complete … H4); #b *; #evb #Hb |
---|
| 221 | >(yields_eq ??? Hb) whd in ⊢ (??%?); <evb |
---|
| 222 | @refl |
---|
| 223 | | #e #ty #ty' #v1 #v #tr #H1 #H2 #H3 whd in ⊢ (??%?); |
---|
| 224 | >(yields_eq ??? H3) whd in ⊢ (??%?); |
---|
| 225 | >(yields_eq ??? (cast_complete … H2)) |
---|
| 226 | @refl |
---|
| 227 | | #e #ty #v #l #tr #H1 #H2 whd in ⊢ (??%?); |
---|
| 228 | >(yields_eq ??? H2) whd in ⊢ (??%?); |
---|
| 229 | @refl |
---|
[253] | 230 | |
---|
[226] | 231 | (* lvalues *) |
---|
[487] | 232 | | #id #l #ty #e1 whd in ⊢ (??%?); >e1 @refl |
---|
[498] | 233 | | #id #l #ty #e1 #e2 whd in ⊢ (??%?); >e1 |
---|
[487] | 234 | >e2 @refl |
---|
[500] | 235 | | #e #ty #r #l #pc #ofs #tr #H1 #H2 whd in ⊢ (??%?); |
---|
[487] | 236 | >(yields_eq ??? H2) |
---|
| 237 | @refl |
---|
[498] | 238 | | #e #i #ty #l #ofs #id #fList #delta #tr #H1 #H2 #H3 #H4 cases e in H2 H4 ⊢ %; |
---|
[487] | 239 | #e' #ty' #H2 whd in H2:(??%?); >H2 #H4 whd in ⊢ (??%?); |
---|
| 240 | >(yields_eq ??? H4) whd in ⊢ (??%?); |
---|
| 241 | >H3 @refl |
---|
[498] | 242 | | #e #i #ty #l #ofs #id #fList #tr cases e; #e' #ty' #H1 #H2 |
---|
[487] | 243 | whd in H2:(??%?); >H2 #H3 whd in ⊢ (??%?); |
---|
| 244 | >(yields_eq ??? H3) @refl |
---|
| 245 | ] qed. |
---|
[226] | 246 | |
---|
[487] | 247 | theorem expr_complete: ∀ge,env,m. |
---|
[399] | 248 | ∀e,v,tr. eval_expr ge env m e v tr → yields ? (exec_expr ge env m e) (〈v,tr〉). |
---|
[487] | 249 | #ge #env #m elim (expr_lvalue_complete ge env m); /2/; qed. |
---|
[226] | 250 | |
---|
[487] | 251 | theorem exprlist_complete: ∀ge,env,m,es,vs,tr. |
---|
[399] | 252 | eval_exprlist ge env m es vs tr → yields ? (exec_exprlist ge env m es) (〈vs,tr〉). |
---|
[487] | 253 | #ge #env #m #es #vs #tr #H elim H; |
---|
| 254 | [ @refl |
---|
| 255 | | #e #et #v #vt #tr #trt #H1 #H2 #H3 whd in ⊢ (??%?); |
---|
| 256 | >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?); |
---|
| 257 | >(yields_eq ??? H3) |
---|
| 258 | @refl |
---|
| 259 | ] qed. |
---|
[239] | 260 | |
---|
[487] | 261 | theorem lvalue_complete: ∀ge,env,m. |
---|
[498] | 262 | ∀e,l,off,tr. eval_lvalue ge env m e l off tr → yields ? (exec_lvalue ge env m e) (〈〈l,off〉,tr〉). |
---|
[487] | 263 | #ge #env #m elim (expr_lvalue_complete ge env m); /2/; qed. |
---|
[239] | 264 | |
---|
[487] | 265 | let rec P_typelist (P:type → Prop) (l:typelist) on l : Prop ≝ |
---|
[239] | 266 | match l with |
---|
| 267 | [ Tnil ⇒ True |
---|
| 268 | | Tcons h t ⇒ P h ∧ P_typelist P t |
---|
| 269 | ]. |
---|
| 270 | |
---|
[487] | 271 | let rec type_ind2l |
---|
[239] | 272 | (P:type → Prop) (Q:typelist → Prop) |
---|
| 273 | (vo:P Tvoid) |
---|
| 274 | (it:∀i,s. P (Tint i s)) |
---|
| 275 | (fl:∀f. P (Tfloat f)) |
---|
| 276 | (pt:∀s,t. P t → P (Tpointer s t)) |
---|
| 277 | (ar:∀s,t,n. P t → P (Tarray s t n)) |
---|
| 278 | (fn:∀tl,t. Q tl → P t → P (Tfunction tl t)) |
---|
| 279 | (st:∀i,fl. P (Tstruct i fl)) |
---|
| 280 | (un:∀i,fl. P (Tunion i fl)) |
---|
[481] | 281 | (cp:∀r,i. P (Tcomp_ptr r i)) |
---|
[239] | 282 | (nl:Q Tnil) |
---|
| 283 | (cs:∀t,tl. P t → Q tl → Q (Tcons t tl)) |
---|
| 284 | (t:type) on t : P t ≝ |
---|
| 285 | match t return λt'.P t' with |
---|
| 286 | [ Tvoid ⇒ vo |
---|
| 287 | | Tint i s ⇒ it i s |
---|
| 288 | | Tfloat s ⇒ fl s |
---|
| 289 | | Tpointer s t' ⇒ pt s t' (type_ind2l P Q vo it fl pt ar fn st un cp nl cs t') |
---|
| 290 | | Tarray s t' n ⇒ ar s t' n (type_ind2l P Q vo it fl pt ar fn st un cp nl cs t') |
---|
| 291 | | 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') |
---|
| 292 | | Tstruct i fs ⇒ st i fs |
---|
| 293 | | Tunion i fs ⇒ un i fs |
---|
[481] | 294 | | Tcomp_ptr r i ⇒ cp r i |
---|
[239] | 295 | ] |
---|
| 296 | and typelist_ind2l |
---|
| 297 | (P:type → Prop) (Q:typelist → Prop) |
---|
| 298 | (vo:P Tvoid) |
---|
| 299 | (it:∀i,s. P (Tint i s)) |
---|
| 300 | (fl:∀f. P (Tfloat f)) |
---|
| 301 | (pt:∀s,t. P t → P (Tpointer s t)) |
---|
| 302 | (ar:∀s,t,n. P t → P (Tarray s t n)) |
---|
| 303 | (fn:∀tl,t. Q tl → P t → P (Tfunction tl t)) |
---|
| 304 | (st:∀i,fl. P (Tstruct i fl)) |
---|
| 305 | (un:∀i,fl. P (Tunion i fl)) |
---|
[481] | 306 | (cp:∀r,i. P (Tcomp_ptr r i)) |
---|
[239] | 307 | (nl:Q Tnil) |
---|
| 308 | (cs:∀t,tl. P t → Q tl → Q (Tcons t tl)) |
---|
| 309 | (ts:typelist) on ts : Q ts ≝ |
---|
| 310 | match ts return λts'.Q ts' with |
---|
| 311 | [ Tnil ⇒ nl |
---|
| 312 | | Tcons t tl ⇒ cs t tl (type_ind2l P Q vo it fl pt ar fn st un cp nl cs t) |
---|
| 313 | (typelist_ind2l P Q vo it fl pt ar fn st un cp nl cs tl) |
---|
| 314 | ]. |
---|
| 315 | |
---|
[487] | 316 | lemma assert_type_eq_true: ∀t. ∃p.assert_type_eq t t = OK ? p. |
---|
| 317 | #t whd in ⊢ (??(λ_.??%?)); cases (type_eq_dec t t); #E |
---|
| 318 | [ %{ E} // |
---|
| 319 | | @False_ind @(absurd ?? E) // |
---|
| 320 | ] qed. |
---|
[239] | 321 | |
---|
[487] | 322 | lemma alloc_vars_complete: ∀env,m,l,env',m'. |
---|
[239] | 323 | alloc_variables env m l env' m' → |
---|
[487] | 324 | exec_alloc_variables env m l = 〈env', m'〉. |
---|
| 325 | #env #m #l #env' #m' #H elim H; |
---|
| 326 | [ #env'' #m'' % |
---|
| 327 | | #env1 #m1 #id #ty #l1 #m2 #loc #m3 #env2 #H1 #H2 #H3 |
---|
[1516] | 328 | < H3 whd in H1:(??%?) ⊢ (??%?); |
---|
[1058] | 329 | < (pair_eq1 ?????? H1) < (pair_eq2 ?????? H1) |
---|
| 330 | @refl |
---|
[487] | 331 | ] qed. |
---|
[239] | 332 | |
---|
[487] | 333 | lemma bind_params_complete: ∀e,m,params,vs,m2. |
---|
[239] | 334 | bind_parameters e m params vs m2 → |
---|
[487] | 335 | yields ? (exec_bind_parameters e m params vs) m2. |
---|
| 336 | #e #m #params #vs #m2 #H elim H; |
---|
| 337 | [ //; |
---|
| 338 | | #env1 #m1 #id #ty #l #v #tl #loc #m2 #m3 #H1 #H2 #H3 #H4 |
---|
[1516] | 339 | whd in ⊢ (??%?); |
---|
[487] | 340 | >H1 whd in ⊢ (??%?); |
---|
| 341 | >H2 whd in ⊢ (??%?); |
---|
| 342 | @H4 |
---|
| 343 | ] qed. |
---|
[239] | 344 | |
---|
[487] | 345 | lemma eventval_match_complete': ∀ev,ty,v. |
---|
| 346 | eventval_match ev ty v → yields ? (check_eventval' v ty) ev. |
---|
[1516] | 347 | #ev #ty #v #H elim H; // #sz #sg #i whd in ⊢ (??%?); >eq_intsize_true @refl qed. |
---|
[239] | 348 | |
---|
[487] | 349 | lemma eventval_list_match_complete: ∀vs,tys,evs. |
---|
| 350 | eventval_list_match evs tys vs → yields ? (check_eventval_list vs tys) evs. |
---|
| 351 | #vs #tys #evs #H elim H; |
---|
| 352 | [ // |
---|
[1516] | 353 | | #e #etl #ty #tytl #v #vtl #H1 #H2 #H3 whd in ⊢ (??%?); |
---|
| 354 | >(yields_eq ??? (eventval_match_complete' … H1)) whd in ⊢ (??%?); |
---|
| 355 | >(yields_eq ??? H3) whd in ⊢ (??%?); // |
---|
[487] | 356 | ] qed. |
---|
[239] | 357 | |
---|
[487] | 358 | theorem step_complete: ∀ge,s,tr,s'. |
---|
[399] | 359 | step ge s tr s' → yieldsIO ? (exec_step ge s) 〈tr,s'〉. |
---|
[487] | 360 | #ge #s #tr #s' #H elim H; |
---|
[498] | 361 | [ #f #e #e1 #k #e2 #m #loc #ofs #v #m' #tr1 #tr2 #H1 #H2 #H3 whd in ⊢ (??%?); |
---|
[1516] | 362 | >(yields_eq ??? (lvalue_complete … H1)) whd in ⊢ (??%?); |
---|
| 363 | >(yields_eq ??? (expr_complete … H2)) whd in ⊢ (??%?); |
---|
[1521] | 364 | change with (store_value_of_type' (typeof e) m 〈loc,ofs〉 v) in H3:(??%?); |
---|
[487] | 365 | >H3 @refl |
---|
| 366 | | #f #e #eargs #k #ef #m #vf #vargs #f' #tr1 #tr2 #H1 #H2 #H3 #H4 whd in ⊢ (??%?); |
---|
| 367 | >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?); |
---|
| 368 | >(yields_eq ??? (exprlist_complete … H2)) whd in ⊢ (??%?); |
---|
| 369 | >H3 whd in ⊢ (??%?); |
---|
| 370 | >H4 elim (assert_type_eq_true (fun_typeof e)); #pty #ety >ety |
---|
| 371 | @refl |
---|
[498] | 372 | | #f #el #ef #eargs #k #env #m #loc #ofs #vf #vargs #f' #tr1 #tr2 #tr3 #H1 #H2 #H3 #H4 #H5 whd in ⊢ (??%?); |
---|
[487] | 373 | >(yields_eq ??? (expr_complete … H2)) whd in ⊢ (??%?); |
---|
| 374 | >(yields_eq ??? (exprlist_complete … H3)) whd in ⊢ (??%?); |
---|
| 375 | >H4 whd in ⊢ (??%?); |
---|
| 376 | >H5 elim (assert_type_eq_true (fun_typeof ef)); #pty #ety >ety |
---|
| 377 | whd in ⊢ (??%?); |
---|
| 378 | >(yields_eq ??? (lvalue_complete … H1)) whd in ⊢ (??%?); |
---|
| 379 | @refl |
---|
| 380 | | #f #s1 #s2 #k #env #m @refl |
---|
| 381 | | 5,6,7: #f #s #k #env #m @refl |
---|
| 382 | | #f #e #s1 #s2 #k #env #m #v #tr #H1 #H2 whd in ⊢ (??%?); |
---|
| 383 | >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?); |
---|
| 384 | >(yields_eq ??? (bool_of_true ?? H2)) |
---|
| 385 | @refl |
---|
| 386 | | #f #e #s1 #s2 #k #env #m #v #tr #H1 #H2 whd in ⊢ (??%?); |
---|
| 387 | >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?); |
---|
| 388 | >(yields_eq ??? (bool_of_false ?? H2)) |
---|
| 389 | @refl |
---|
| 390 | | #f #e #s #k #env #m #v #tr #H1 #H2 whd in ⊢ (??%?); |
---|
| 391 | >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?); |
---|
| 392 | >(yields_eq ??? (bool_of_false ?? H2)) |
---|
| 393 | @refl |
---|
| 394 | | #f #e #s #k #env #m #v #tr #H1 #H2 whd in ⊢ (??%?); |
---|
| 395 | >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?); |
---|
| 396 | >(yields_eq ??? (bool_of_true ?? H2)) |
---|
| 397 | @refl |
---|
| 398 | | #f #s1 #e #s2 #k #env #m #H cases H; #es1 >es1 @refl |
---|
| 399 | | 13,14: #f #e #s #k #env #m @refl |
---|
| 400 | | #f #s1 #e #s2 #k #env #m #v #tr *; #es1 >es1 #H1 #H2 whd in ⊢ (??%?); |
---|
| 401 | >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?); |
---|
| 402 | >(yields_eq ??? (bool_of_false ?? H2)) |
---|
| 403 | @refl |
---|
| 404 | | #f #s1 #e #s2 #k #env #m #v #tr *; #es1 >es1 #H1 #H2 whd in ⊢ (??%?); |
---|
| 405 | >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?); |
---|
| 406 | >(yields_eq ??? (bool_of_true ?? H2)) |
---|
| 407 | @refl |
---|
| 408 | | #f #e #s #k #env #m @refl |
---|
| 409 | | #f #s1 #e #s2 #s3 #k #env #m #nskip whd in ⊢ (??%?); cases (is_Sskip s1); |
---|
| 410 | [ #H @False_ind @(absurd ? H nskip) |
---|
| 411 | | #H whd in ⊢ (??%?); @refl ] |
---|
| 412 | | #f #e #s1 #s2 #k #env #m #v #tr #H1 #H2 whd in ⊢ (??%?); |
---|
| 413 | >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?); |
---|
| 414 | >(yields_eq ??? (bool_of_false ?? H2)) |
---|
| 415 | @refl |
---|
| 416 | | #f #e #s1 #s2 #k #env #m #v #tr #H1 #H2 whd in ⊢ (??%?); |
---|
| 417 | >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?); |
---|
| 418 | >(yields_eq ??? (bool_of_true ?? H2)) |
---|
| 419 | @refl |
---|
| 420 | | #f #s1 #e #s2 #s3 #k #env #m *; #es1 >es1 @refl |
---|
| 421 | | 22,23: #f #e #s1 #s2 #k #env #m @refl |
---|
| 422 | | #f #k #env #m #H whd in ⊢ (??%?); >H @refl |
---|
| 423 | | #f #e #k #env #m #v #tr #H1 #H2 whd in ⊢ (??%?); |
---|
| 424 | @(dec_false ? (type_eq_dec (fn_return f) Tvoid) H1) #pf' |
---|
| 425 | whd in ⊢ (??%?); |
---|
| 426 | >(yields_eq ??? (expr_complete … H2)) whd in ⊢ (??%?); |
---|
| 427 | @refl |
---|
| 428 | | #f #k #env #m cases k; |
---|
| 429 | [ #H1 #H2 whd in ⊢ (??%?); >H2 @refl |
---|
| 430 | | #s' #k' whd in ⊢ (% → ?); *; |
---|
| 431 | | 3,4: #e' #s' #k' whd in ⊢ (% → ?); *; |
---|
| 432 | | 5,6: #e' #s1' #s2' #k' whd in ⊢ (% → ?); *; |
---|
| 433 | | #k' whd in ⊢ (% → ?); *; |
---|
| 434 | | #r #f' #env' #k' #H1 #H2 whd in ⊢ (??%?); >H2 @refl |
---|
| 435 | ] |
---|
[961] | 436 | | #f #e #s #k #env #m #sz #i #tr #H1 whd in ⊢ (??%?); |
---|
[487] | 437 | >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?); |
---|
| 438 | @refl |
---|
| 439 | | #f #s #k #env #m *; #es >es @refl |
---|
| 440 | | #f #k #env #m @refl |
---|
| 441 | | #f #l #s #k #env #m @refl |
---|
| 442 | | #f #l #k #env #m #s #k' #H1 whd in ⊢ (??%?); >H1 @refl |
---|
| 443 | | #f #args #k #m1 #env #m2 #m3 #H1 #H2 whd in ⊢ (??%?); |
---|
| 444 | >(alloc_vars_complete … H1) whd in ⊢ (??%?); |
---|
| 445 | >(yields_eq ??? (bind_params_complete … H2)) |
---|
| 446 | // |
---|
| 447 | | #id #tys #rty #args #k #m #rv #tr #H whd in ⊢ (??%?); |
---|
[1516] | 448 | inversion H; #f' #args' #rv' #eargs #erv #H1 #H2 #e1 #e2 #e3 #e4 #e5 <e1 in H1 H2; |
---|
[487] | 449 | #H1 #H2 |
---|
| 450 | >(yields_eq ??? (eventval_list_match_complete … H1)) whd in ⊢ (??%?); |
---|
[1510] | 451 | whd; inversion H2; [ #sz #sg #x | #x #sz ] #e5 #e6 #e7 #e8 %{ x} whd in ⊢ (??%?); |
---|
[487] | 452 | @refl |
---|
| 453 | | #v #f #env #k #m @refl |
---|
[891] | 454 | | #v #f #env #k #m1 #m2 #loc #ofs #ty |
---|
[1521] | 455 | change with (store_value_of_type' ty m1 〈loc,ofs〉 v) in ⊢ (??%? → ?); |
---|
[1516] | 456 | #H whd in ⊢ (??%?); >H @refl |
---|
[487] | 457 | | #f #l #s #k #env #m @refl |
---|
| 458 | ] qed. |
---|
[708] | 459 | |
---|
| 460 | lemma is_final_complete : ∀s,r. final_state s r → is_final s = Some ? r. |
---|
| 461 | #s0 #r0 * #r #m @refl qed. |
---|
| 462 | |
---|