[20] | 1 | |
---|
| 2 | include "Csem.ma". |
---|
| 3 | |
---|
| 4 | include "extralib.ma". |
---|
[24] | 5 | include "IOMonad.ma". |
---|
[20] | 6 | |
---|
| 7 | include "Plogic/russell_support.ma". |
---|
| 8 | |
---|
| 9 | ndefinition P_to_P_option_res : ∀A:Type[0].∀P:A → CProp[0].option (res A) → CProp[0] ≝ |
---|
| 10 | λA,P,a.match a with [ None ⇒ False | Some y ⇒ match y return λ_.CProp[0] with [ Error ⇒ True | OK z ⇒ P z ]]. |
---|
| 11 | |
---|
| 12 | ndefinition err_inject : ∀A.∀P:A → Prop.∀a:option (res A).∀p:P_to_P_option_res A P a.res (sigma A P) ≝ |
---|
| 13 | λA.λP:A → Prop.λa:option (res A).λp:P_to_P_option_res A P a. |
---|
| 14 | (match a return λa'.a=a' → res (sigma A P) with |
---|
| 15 | [ None ⇒ λe1.? |
---|
| 16 | | Some b ⇒ λe1.(match b return λb'.b=b' → ? with |
---|
| 17 | [ Error ⇒ λ_. Error ? |
---|
| 18 | | OK c ⇒ λe2. OK ? (sig_intro A P c ?) |
---|
| 19 | ]) (refl ? b) |
---|
| 20 | ]) (refl ? a). |
---|
| 21 | ##[ nrewrite > e1 in p; nnormalize; *; |
---|
| 22 | ##| nrewrite > e1 in p; nrewrite > e2; nnormalize; // |
---|
| 23 | ##] nqed. |
---|
| 24 | |
---|
| 25 | ndefinition err_eject : ∀A.∀P: A → Prop. res (sigma A P) → res A ≝ |
---|
| 26 | λA,P,a.match a with [ Error ⇒ Error ? | OK b ⇒ |
---|
| 27 | match b with [ sig_intro w p ⇒ OK ? w] ]. |
---|
| 28 | |
---|
| 29 | ndefinition sig_eject : ∀A.∀P: A → Prop. sigma A P → A ≝ |
---|
| 30 | λA,P,a.match a with [ sig_intro w p ⇒ w]. |
---|
| 31 | |
---|
| 32 | ncoercion err_inject : |
---|
| 33 | ∀A.∀P:A → Prop.∀a.∀p:P_to_P_option_res ? P a.res (sigma A P) ≝ err_inject |
---|
| 34 | on a:option (res ?) to res (sigma ? ?). |
---|
| 35 | ncoercion err_eject : ∀A.∀P:A → Prop.∀c:res (sigma A P).res A ≝ err_eject |
---|
| 36 | on _c:res (sigma ? ?) to res ?. |
---|
| 37 | ncoercion sig_eject : ∀A.∀P:A → Prop.∀c:sigma A P.A ≝ sig_eject |
---|
| 38 | on _c:sigma ? ? to ?. |
---|
| 39 | |
---|
| 40 | ndefinition bool_of_val_3 : ∀v:val. ∀ty:type. res (Σr:bool. bool_of_val v ty (of_bool r)) ≝ |
---|
| 41 | λv,ty. match v in val with |
---|
| 42 | [ Vint i ⇒ match ty with |
---|
| 43 | [ Tint _ _ ⇒ Some ? (OK ? (¬eq i zero)) |
---|
[124] | 44 | | Tpointer _ _ ⇒ Some ? (OK ? (¬eq i zero)) |
---|
[20] | 45 | | _ ⇒ Some ? (Error ?) |
---|
| 46 | ] |
---|
| 47 | | Vfloat f ⇒ match ty with |
---|
| 48 | [ Tfloat _ ⇒ Some ? (OK ? (¬Fcmp Ceq f Fzero)) |
---|
| 49 | | _ ⇒ Some ? (Error ?) |
---|
| 50 | ] |
---|
[124] | 51 | | Vptr _ _ _ ⇒ match ty with |
---|
[20] | 52 | [ Tint _ _ ⇒ Some ? (OK ? true) |
---|
[124] | 53 | | Tpointer _ _ ⇒ Some ? (OK ? true) |
---|
[20] | 54 | | _ ⇒ Some ? (Error ?) |
---|
| 55 | ] |
---|
| 56 | | _ ⇒ Some ? (Error ?) |
---|
| 57 | ]. nwhd; //; |
---|
| 58 | ##[ ##1,2: nlapply (eq_spec c0 zero); nelim (eq c0 zero); |
---|
| 59 | ##[ ##1,3: #e; nrewrite > e; napply bool_of_val_false; //; |
---|
| 60 | ##| ##2,4: #ne; napply bool_of_val_true; /2/; |
---|
| 61 | ##] |
---|
| 62 | ##| nelim (eq_dec c0 Fzero); |
---|
| 63 | ##[ #e; nrewrite > e; nrewrite > (Feq_zero_true …); napply bool_of_val_false; //; |
---|
| 64 | ##| #ne; nrewrite > (Feq_zero_false …); //; napply bool_of_val_true; /2/; |
---|
| 65 | ##] |
---|
| 66 | ##| ##4,5: napply bool_of_val_true; // |
---|
| 67 | ##] nqed. |
---|
| 68 | |
---|
| 69 | ndefinition err_eq ≝ λA,P. λx:res (sigma A P). λy:A. |
---|
| 70 | match x with [ Error ⇒ False | OK x' ⇒ |
---|
| 71 | match x' with [ sig_intro x'' _ ⇒ x'' = y ]]. |
---|
| 72 | (* TODO: can I write a coercion for the above? *) |
---|
| 73 | |
---|
| 74 | (* Same as before, except we have to use a slightly different "equality". *) |
---|
| 75 | |
---|
| 76 | 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. |
---|
| 77 | #v ty r H; nelim H; #v t H'; nelim H'; |
---|
| 78 | ##[ #i is s ne; @ true; @; //; nwhd; nrewrite > (eq_false … ne); //; |
---|
[124] | 79 | ##| #p b i i0 s; @ true; @; // |
---|
| 80 | ##| #i p t ne; @ true; @; //; nwhd; nrewrite > (eq_false … ne); //; |
---|
| 81 | ##| #p b i p0 t0; @ true; @; // |
---|
[20] | 82 | ##| #f s ne; @ true; @; //; nwhd; nrewrite > (Feq_zero_false … ne); //; |
---|
| 83 | ##| #i s; @ false; @; //; (*nwhd; nrewrite > (eq_true …); //;*) |
---|
[124] | 84 | ##| #p t; @ false; @; //; (*nwhd; nrewrite > (eq_true …); //;*) |
---|
[20] | 85 | ##| #s; @ false; @; //; nwhd; nrewrite > (Feq_zero_true …); //; |
---|
| 86 | ##] |
---|
| 87 | nqed. |
---|
| 88 | |
---|
| 89 | (* Prove a few minor results to make proof obligations easy. *) |
---|
| 90 | |
---|
| 91 | nlemma bind_assoc_r: ∀A,B,C,e,f,g. |
---|
| 92 | bind B C (bind A B e f) g = bind A C e (λx.bind B C (f x) g). |
---|
| 93 | #A B C e f g; ncases e; nnormalize; //; nqed. |
---|
| 94 | |
---|
| 95 | nlemma bind_OK: ∀A,B,P,e,f. |
---|
| 96 | (∀v. e = OK A v → match f v with [ Error ⇒ True | OK v' ⇒ P v' ]) → |
---|
| 97 | match bind A B e f with [ Error ⇒ True | OK v ⇒ P v ]. |
---|
| 98 | #A B P e f; nelim e; /2/; nqed. |
---|
| 99 | |
---|
| 100 | nlemma sig_bind_OK: ∀A,B. ∀P:A → Prop. ∀P':B → Prop. ∀e:res (sigma A P). ∀f:sigma A P → res B. |
---|
[124] | 101 | (∀v:A. ∀p:P v. match f (sig_intro A P v p) with [ Error ⇒ True | OK v' ⇒ P' v'] ) → |
---|
[20] | 102 | match bind (sigma A P) B e f with [ Error ⇒ True | OK v' ⇒ P' v' ]. |
---|
[124] | 103 | #A B P P' e f; nelim e; |
---|
| 104 | ##[ #v0; nelim v0; #v Hv IH; napply IH; |
---|
| 105 | ##| #_; napply I; |
---|
| 106 | ##] nqed. |
---|
[20] | 107 | |
---|
| 108 | nlemma bind2_OK: ∀A,B,C,P,e,f. |
---|
| 109 | (∀v1,v2. e = OK ? 〈v1,v2〉 → match f v1 v2 with [ Error ⇒ True | OK v' ⇒ P v' ]) → |
---|
| 110 | match bind2 A B C e f with [ Error ⇒ True | OK v ⇒ P v ]. |
---|
| 111 | #A B C P e f; nelim e; //; #v; ncases v; /2/; nqed. |
---|
| 112 | |
---|
| 113 | 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. |
---|
| 114 | (∀v1:A.∀v2:B. P 〈v1,v2〉 → match f v1 v2 with [ Error ⇒ True | OK v' ⇒ P' v'] ) → |
---|
| 115 | match bind2 A B C e f with [ Error ⇒ True | OK v' ⇒ P' v' ]. |
---|
| 116 | #A B C P P' e f; nelim e; //; |
---|
| 117 | #v0; nelim v0; #v; nelim v; #v1 v2 Hv IH; napply IH; //; nqed. |
---|
| 118 | |
---|
| 119 | nlemma reinject: ∀A. ∀P,P':A → Prop. ∀e:res (sigma A P'). |
---|
| 120 | (∀v:A. err_eq A P' e v → P' v → P v) → |
---|
| 121 | match err_eject A P' e with [ Error ⇒ True | OK v' ⇒ P v' ]. |
---|
| 122 | #A P P' e; ncases e; //; |
---|
| 123 | #v0; nelim v0; #v Pv' IH; /2/; |
---|
| 124 | nqed. |
---|
| 125 | |
---|
| 126 | nlemma bool_val_distinct: Vtrue ≠ Vfalse. |
---|
| 127 | @; #H; nwhd in H:(??%%); ndestruct; napply (absurd ? e0 one_not_zero); |
---|
| 128 | nqed. |
---|
| 129 | |
---|
| 130 | nlemma bool_of: ∀v,ty,b. bool_of_val v ty (of_bool b) → |
---|
| 131 | if b then is_true v ty else is_false v ty. |
---|
| 132 | #v ty b; ncases b; #H; ninversion H; #v' ty' H' ev et ev; //; |
---|
| 133 | napply False_ind; napply (absurd ? ev ?); |
---|
| 134 | ##[ ##2: napply sym_neq ##] napply bool_val_distinct; |
---|
| 135 | nqed. |
---|
| 136 | |
---|
| 137 | ndefinition opt_to_res ≝ λA.λv:option A. match v with [ None ⇒ Error A | Some v ⇒ OK A v ]. |
---|
| 138 | nlemma opt_OK: ∀A,P,e. |
---|
| 139 | (∀v. e = Some ? v → P v) → |
---|
| 140 | match opt_to_res A e with [ Error ⇒ True | OK v ⇒ P v ]. |
---|
| 141 | #A P e; nelim e; /2/; |
---|
| 142 | nqed. |
---|
| 143 | |
---|
| 144 | nlemma opt_bind_OK: ∀A,B,P,e,f. |
---|
| 145 | (∀v. e = Some A v → match f v with [ Error ⇒ True | OK v' ⇒ P v' ]) → |
---|
| 146 | match bind A B (opt_to_res A e) f with [ Error ⇒ True | OK v ⇒ P v ]. |
---|
| 147 | #A B P e f; nelim e; nnormalize; /2/; nqed. |
---|
| 148 | |
---|
| 149 | nlemma extract_subset_pair: ∀A,B,C,P. ∀e:{e:A×B | P e}. ∀Q:A→B→res C. ∀R:C→Prop. |
---|
| 150 | (∀a,b. eject ?? e = 〈a,b〉 → P 〈a,b〉 → match Q a b with [ OK v ⇒ R v | Error ⇒ True]) → |
---|
| 151 | match match eject ?? e with [ mk_pair a b ⇒ Q a b ] with [ OK v ⇒ R v | Error ⇒ True ]. |
---|
| 152 | #A B C P e Q R; ncases e; #e'; ncases e'; nnormalize; |
---|
| 153 | ##[ #H; napply (False_ind … H); |
---|
| 154 | ##| #e''; ncases e''; #a b Pab H; nnormalize; /2/; |
---|
| 155 | ##] nqed. |
---|
| 156 | |
---|
| 157 | (* |
---|
| 158 | nremark err_later: ∀A,B. ∀e:res A. match e with [ Error ⇒ Error B | OK v ⇒ Error B ] = Error B. |
---|
| 159 | #A B e; ncases e; //; nqed. |
---|
| 160 | *) |
---|
| 161 | |
---|
[189] | 162 | 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') ≝ |
---|
[124] | 163 | match eq i zero with |
---|
| 164 | [ true ⇒ |
---|
| 165 | match ty with |
---|
| 166 | [ Tpointer _ _ ⇒ |
---|
| 167 | match ty' with |
---|
| 168 | [ Tpointer _ _ ⇒ Some ? (OK ? (Vint i)) |
---|
| 169 | | Tarray _ _ _ ⇒ Some ? (OK ? (Vint i)) |
---|
| 170 | | Tfunction _ _ ⇒ Some ? (OK ? (Vint i)) |
---|
| 171 | | _ ⇒ Some ? (Error ?) |
---|
| 172 | ] |
---|
| 173 | | Tarray _ _ _ ⇒ |
---|
| 174 | match ty' with |
---|
| 175 | [ Tpointer _ _ ⇒ Some ? (OK ? (Vint i)) |
---|
| 176 | | Tarray _ _ _ ⇒ Some ? (OK ? (Vint i)) |
---|
| 177 | | Tfunction _ _ ⇒ Some ? (OK ? (Vint i)) |
---|
| 178 | | _ ⇒ Some ? (Error ?) |
---|
| 179 | ] |
---|
| 180 | | Tfunction _ _ ⇒ |
---|
| 181 | match ty' with |
---|
| 182 | [ Tpointer _ _ ⇒ Some ? (OK ? (Vint i)) |
---|
| 183 | | Tarray _ _ _ ⇒ Some ? (OK ? (Vint i)) |
---|
| 184 | | Tfunction _ _ ⇒ Some ? (OK ? (Vint i)) |
---|
| 185 | | _ ⇒ Some ? (Error ?) |
---|
| 186 | ] |
---|
| 187 | | _ ⇒ Some ? (Error ?) |
---|
| 188 | ] |
---|
| 189 | | false ⇒ Some ? (Error ?) |
---|
| 190 | ]. nwhd; //; nlapply (eq_spec i zero); nrewrite > c0; #e; nrewrite > e; |
---|
| 191 | napply cast_pp_z; //; nqed. |
---|
| 192 | |
---|
[155] | 193 | ndefinition ms_eq_dec : ∀s1,s2:memory_space. (s1 = s2) + (s1 ≠ s2). |
---|
| 194 | #s1; ncases s1; #s2; ncases s2; /2/; @2; @; #H; ndestruct; nqed. |
---|
| 195 | |
---|
[189] | 196 | ndefinition exec_cast : ∀m:mem. ∀v:val. ∀ty:type. ∀ty':type. res (Σv':val. cast m v ty ty' v') ≝ |
---|
| 197 | λm:mem. λv:val. λty:type. λty':type. |
---|
[20] | 198 | match v with |
---|
| 199 | [ Vint i ⇒ |
---|
| 200 | match ty with |
---|
| 201 | [ Tint sz1 si1 ⇒ |
---|
| 202 | match ty' with |
---|
| 203 | [ Tint sz2 si2 ⇒ Some ? (OK ? (Vint (cast_int_int sz2 si2 i))) |
---|
| 204 | | Tfloat sz2 ⇒ Some ? (OK ? (Vfloat (cast_float_float sz2 (cast_int_float si1 i)))) |
---|
[189] | 205 | | Tpointer _ _ ⇒ Some (res val) (do r ← try_cast_null m i ty ty'; OK val r) |
---|
| 206 | | Tarray _ _ _ ⇒ Some (res val) (do r ← try_cast_null m i ty ty'; OK val r) |
---|
| 207 | | Tfunction _ _ ⇒ Some (res val) (do r ← try_cast_null m i ty ty'; OK val r) |
---|
[124] | 208 | | _ ⇒ Some ? (Error ?) |
---|
[20] | 209 | ] |
---|
[189] | 210 | | Tpointer _ _ ⇒ Some (res val) (do r ← try_cast_null m i ty ty'; OK val r) |
---|
| 211 | | Tarray _ _ _ ⇒ Some (res val) (do r ← try_cast_null m i ty ty'; OK val r) |
---|
| 212 | | Tfunction _ _ ⇒ Some (res val) (do r ← try_cast_null m i ty ty'; OK val r) |
---|
[124] | 213 | | _ ⇒ Some ? (Error ?) |
---|
[20] | 214 | ] |
---|
| 215 | | Vfloat f ⇒ |
---|
| 216 | match ty with |
---|
| 217 | [ Tfloat sz ⇒ |
---|
| 218 | match ty' with |
---|
| 219 | [ Tint sz' si' ⇒ Some ? (OK ? (Vint (cast_int_int sz' si' (cast_float_int si' f)))) |
---|
| 220 | | Tfloat sz' ⇒ Some ? (OK ? (Vfloat (cast_float_float sz' f))) |
---|
| 221 | | _ ⇒ Some ? (Error ?) |
---|
| 222 | ] |
---|
| 223 | | _ ⇒ Some ? (Error ?) |
---|
| 224 | ] |
---|
[124] | 225 | | Vptr p b ofs ⇒ |
---|
| 226 | Some ? ( |
---|
[189] | 227 | do s ← match ty with [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code | _ ⇒ Error ? ]; |
---|
| 228 | do u ← match ms_eq_dec p s with [ inl _ ⇒ OK ? something | inr _ ⇒ Error ? ]; |
---|
| 229 | do s' ← match ty' with |
---|
[127] | 230 | [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code |
---|
[189] | 231 | | _ ⇒ Error ? ]; |
---|
[125] | 232 | if is_pointer_compat (block_space m b) s' |
---|
| 233 | then OK ? (Vptr s' b ofs) |
---|
[124] | 234 | else Error ?) |
---|
[20] | 235 | | _ ⇒ Some ? (Error ?) |
---|
[124] | 236 | ]. nwhd; //; |
---|
| 237 | ##[ ##1,2,3,4,5,6: napply sig_bind_OK; #v'; #H; ndestruct; napply H; |
---|
[155] | 238 | ##| napply bind_OK; #s es; |
---|
| 239 | ncut (type_space ty s); |
---|
| 240 | ##[ ncases ty in es ⊢ %; |
---|
| 241 | ##[ #e; ##| ##3,9: #a e; ##| ##2,4,6,7,8: #a b e; ##| #a b c e; ##] nwhd in e:(??%?); ndestruct; //; |
---|
| 242 | ##| #Hty; |
---|
| 243 | napply bind_OK; #u1 eeq; |
---|
| 244 | napply bind_OK; #s' es'; |
---|
| 245 | ncut (type_space ty' s'); |
---|
| 246 | ##[ ncases ty' in es' ⊢ %; ##[ #e; ##| ##3,9: #a e; ##| ##2,4,6,7,8: #a b e; ##| #a b c e; ##] |
---|
| 247 | nwhd in e:(??%?); ndestruct; //; |
---|
| 248 | ##| #Hty'; |
---|
| 249 | ncut (s = c0). nelim (ms_eq_dec c0 s) in eeq; //; nnormalize; #_; #e; ndestruct. |
---|
| 250 | #e; nrewrite < e; |
---|
| 251 | nwhd in match (is_pointer_compat ??) in ⊢ %; |
---|
| 252 | ncases (pointer_compat_dec (block_space m c1) s'); #Hcompat; |
---|
| 253 | nwhd; /2/; |
---|
| 254 | ##] |
---|
[124] | 255 | ##] |
---|
[20] | 256 | ##] nqed. |
---|
| 257 | |
---|
[124] | 258 | ndefinition load_value_of_type' ≝ |
---|
[125] | 259 | λty,m,l. match l with [ mk_pair pl ofs ⇒ match pl with [ mk_pair psp loc ⇒ |
---|
| 260 | load_value_of_type ty m psp loc ofs ] ]. |
---|
[124] | 261 | |
---|
[20] | 262 | (* To make the evaluation of bare lvalue expressions invoke exec_lvalue with |
---|
| 263 | a structurally smaller value, we break out the surrounding Expr constructor |
---|
| 264 | and use exec_lvalue'. *) |
---|
| 265 | |
---|
[175] | 266 | 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)) ≝ |
---|
[20] | 267 | match e with |
---|
| 268 | [ Expr e' ty ⇒ |
---|
| 269 | match e' with |
---|
[175] | 270 | [ Econst_int i ⇒ Some ? (OK ? 〈Vint i, E0〉) |
---|
| 271 | | Econst_float f ⇒ Some ? (OK ? 〈Vfloat f, E0〉) |
---|
[20] | 272 | | Evar _ ⇒ Some ? ( |
---|
[189] | 273 | do 〈l,tr〉 ← exec_lvalue' ge en m e' ty; |
---|
| 274 | do v ← opt_to_res ? (load_value_of_type' ty m l); |
---|
[175] | 275 | OK ? 〈v,tr〉) |
---|
[20] | 276 | | Ederef _ ⇒ Some ? ( |
---|
[189] | 277 | do 〈l,tr〉 ← exec_lvalue' ge en m e' ty; |
---|
| 278 | do v ← opt_to_res ? (load_value_of_type' ty m l); |
---|
[175] | 279 | OK ? 〈v,tr〉) |
---|
[20] | 280 | | Efield _ _ ⇒ Some ? ( |
---|
[189] | 281 | do 〈l,tr〉 ← exec_lvalue' ge en m e' ty; |
---|
| 282 | do v ← opt_to_res ? (load_value_of_type' ty m l); |
---|
[175] | 283 | OK ? 〈v,tr〉) |
---|
[20] | 284 | | Eaddrof a ⇒ Some ? ( |
---|
[189] | 285 | do 〈plo,tr〉 ← exec_lvalue ge en m a; |
---|
[175] | 286 | OK ? 〈match plo with [ mk_pair pl ofs ⇒ match pl with [ mk_pair pcl loc ⇒ Vptr pcl loc ofs ] ], tr〉) |
---|
| 287 | | Esizeof ty' ⇒ Some ? (OK ? 〈Vint (repr (sizeof ty')), E0〉) |
---|
[20] | 288 | | Eunop op a ⇒ Some ? ( |
---|
[189] | 289 | do 〈v1,tr〉 ← exec_expr ge en m a; |
---|
| 290 | do v ← opt_to_res ? (sem_unary_operation op v1 (typeof a)); |
---|
[175] | 291 | OK ? 〈v,tr〉) |
---|
[20] | 292 | | Ebinop op a1 a2 ⇒ Some ? ( |
---|
[189] | 293 | do 〈v1,tr1〉 ← exec_expr ge en m a1; |
---|
| 294 | do 〈v2,tr2〉 ← exec_expr ge en m a2; |
---|
| 295 | do v ← opt_to_res ? (sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m); |
---|
[175] | 296 | OK ? 〈v,tr1⧺tr2〉) |
---|
[20] | 297 | | Econdition a1 a2 a3 ⇒ Some ? ( |
---|
[189] | 298 | do 〈v,tr1〉 ← exec_expr ge en m a1; |
---|
| 299 | do b ← bool_of_val_3 v (typeof a1); |
---|
| 300 | do 〈v',tr2〉 ← match b return λ_.res (val×trace) with |
---|
[175] | 301 | [ true ⇒ (exec_expr ge en m a2) |
---|
[189] | 302 | | false ⇒ (exec_expr ge en m a3) ]; |
---|
[175] | 303 | OK ? 〈v',tr1⧺tr2〉) |
---|
[20] | 304 | (* if b then exec_expr ge en m a2 else exec_expr ge en m a3)*) |
---|
| 305 | | Eorbool a1 a2 ⇒ Some ? ( |
---|
[189] | 306 | do 〈v1,tr1〉 ← exec_expr ge en m a1; |
---|
| 307 | do b1 ← bool_of_val_3 v1 (typeof a1); |
---|
[175] | 308 | match b1 return λ_.res (val×trace) with [ true ⇒ OK ? 〈Vtrue,tr1〉 | false ⇒ |
---|
[189] | 309 | do 〈v2,tr2〉 ← exec_expr ge en m a2; |
---|
| 310 | do b2 ← bool_of_val_3 v2 (typeof a2); |
---|
[175] | 311 | OK ? 〈of_bool b2, tr1⧺tr2〉 ]) |
---|
[20] | 312 | | Eandbool a1 a2 ⇒ Some ? ( |
---|
[189] | 313 | do 〈v1,tr1〉 ← exec_expr ge en m a1; |
---|
| 314 | do b1 ← bool_of_val_3 v1 (typeof a1); |
---|
[175] | 315 | match b1 return λ_.res (val×trace) with [ true ⇒ |
---|
[189] | 316 | do 〈v2,tr2〉 ← exec_expr ge en m a2; |
---|
| 317 | do b2 ← bool_of_val_3 v2 (typeof a2); |
---|
[175] | 318 | OK ? 〈of_bool b2, tr1⧺tr2〉 |
---|
| 319 | | false ⇒ OK ? 〈Vfalse,tr1〉 ]) |
---|
[20] | 320 | | Ecast ty' a ⇒ Some ? ( |
---|
[189] | 321 | do 〈v,tr〉 ← exec_expr ge en m a; |
---|
| 322 | do v' ← exec_cast m v (typeof a) ty'; |
---|
[175] | 323 | OK ? 〈(* XXX *)sig_eject ?? v',tr〉) |
---|
| 324 | | Ecost l a ⇒ Some ? ( |
---|
[189] | 325 | do 〈v,tr〉 ← exec_expr ge en m a; |
---|
[175] | 326 | OK ? 〈v,tr⧺(Echarge l)〉) |
---|
[20] | 327 | ] |
---|
| 328 | ] |
---|
[175] | 329 | 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)) ≝ |
---|
[20] | 330 | match e' with |
---|
| 331 | [ Evar id ⇒ |
---|
| 332 | match (get … id en) with |
---|
[189] | 333 | [ None ⇒ Some ? (do 〈sp,l〉 ← opt_to_res ? (find_symbol ? ? ge id); OK ? 〈〈〈sp,l〉,zero〉,E0〉) (* global *) |
---|
[175] | 334 | | Some loc ⇒ Some ? (OK ? 〈〈〈Any,loc〉,zero〉,E0〉) (* local *) |
---|
[20] | 335 | ] |
---|
| 336 | | Ederef a ⇒ Some ? ( |
---|
[189] | 337 | do 〈v,tr〉 ← exec_expr ge en m a; |
---|
[20] | 338 | match v with |
---|
[175] | 339 | [ Vptr sp l ofs ⇒ OK ? 〈〈〈sp,l〉,ofs〉,tr〉 |
---|
[20] | 340 | | _ ⇒ Error ? |
---|
| 341 | ]) |
---|
| 342 | | Efield a i ⇒ |
---|
| 343 | match (typeof a) with |
---|
| 344 | [ Tstruct id fList ⇒ Some ? ( |
---|
[189] | 345 | do 〈plofs,tr〉 ← exec_lvalue ge en m a; |
---|
| 346 | do delta ← field_offset i fList; |
---|
[175] | 347 | OK ? 〈〈\fst plofs,add (\snd plofs) (repr delta)〉,tr〉) |
---|
[20] | 348 | | Tunion id fList ⇒ Some ? ( |
---|
[189] | 349 | do 〈plofs,tr〉 ← exec_lvalue ge en m a; |
---|
[175] | 350 | OK ? 〈plofs,tr〉) |
---|
[20] | 351 | | _ ⇒ Some ? (Error ?) |
---|
| 352 | ] |
---|
| 353 | | _ ⇒ Some ? (Error ?) |
---|
| 354 | ] |
---|
[175] | 355 | 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)) ≝ |
---|
[20] | 356 | match e with [ Expr e' ty ⇒ exec_lvalue' ge en m e' ty ]. |
---|
[124] | 357 | nwhd; |
---|
[125] | 358 | ##[ ##1,2: // |
---|
[124] | 359 | ##| ##3,4: |
---|
[175] | 360 | napply sig_bind2_OK; nrewrite > c4; #x; ncases x; #y; ncases y; #sp loc ofs tr H; |
---|
| 361 | napply opt_bind_OK; #v ev; nwhd in ev:(??%?); napply (eval_Elvalue … H ev); |
---|
| 362 | ##| napply sig_bind2_OK; #x; ncases x; #y; ncases y; #sp loc ofs tr H; |
---|
[20] | 363 | nwhd; napply eval_Eaddrof; //; |
---|
[175] | 364 | ##| napply sig_bind2_OK; #v1 tr Hv1; |
---|
| 365 | napply opt_bind_OK; #v ev; |
---|
[20] | 366 | napply (eval_Eunop … Hv1 ev); |
---|
[175] | 367 | ##| napply sig_bind2_OK; #v1 tr1 Hv1; |
---|
| 368 | napply sig_bind2_OK; #v2 tr2 Hv2; |
---|
| 369 | napply opt_bind_OK; #v ev; |
---|
[20] | 370 | napply (eval_Ebinop … Hv1 Hv2 ev); |
---|
[175] | 371 | ##| napply sig_bind2_OK; #v tr Hv; |
---|
[124] | 372 | napply sig_bind_OK; #v' Hv'; |
---|
[20] | 373 | napply (eval_Ecast … Hv Hv'); |
---|
[175] | 374 | ##| napply sig_bind2_OK; #vb tr1 Hvb; |
---|
[20] | 375 | napply sig_bind_OK; #b; |
---|
[175] | 376 | ncases b; #Hb; napply sig_bind2_OK; #v tr Hv; |
---|
[20] | 377 | ##[ napply (eval_Econdition_true … Hvb ? Hv); napply (bool_of ??? Hb); |
---|
| 378 | ##| napply (eval_Econdition_false … Hvb ? Hv); napply (bool_of ??? Hb); |
---|
| 379 | ##] |
---|
[175] | 380 | ##| napply sig_bind2_OK; #v1 tr1 Hv1; |
---|
[124] | 381 | napply sig_bind_OK; #b1; ncases b1; #Hb1; |
---|
[175] | 382 | ##[ napply sig_bind2_OK; #v2 tr2 Hv2; |
---|
[124] | 383 | napply sig_bind_OK; #b2 Hb2; |
---|
[20] | 384 | napply (eval_Eandbool_2 … Hv1 … Hv2); |
---|
| 385 | ##[ napply (bool_of … Hb1); ##| napply Hb2; ##] |
---|
| 386 | ##| napply (eval_Eandbool_1 … Hv1); napply (bool_of … Hb1); |
---|
| 387 | ##] |
---|
[175] | 388 | ##| napply sig_bind2_OK; #v1 tr1 Hv1; |
---|
[124] | 389 | napply sig_bind_OK; #b1; ncases b1; #Hb1; |
---|
[20] | 390 | ##[ napply (eval_Eorbool_1 … Hv1); napply (bool_of … Hb1); |
---|
[175] | 391 | ##| napply sig_bind2_OK; #v2 tr2 Hv2; |
---|
[124] | 392 | napply sig_bind_OK; #b2 Hb2; |
---|
[20] | 393 | napply (eval_Eorbool_2 … Hv1 … Hv2); |
---|
| 394 | ##[ napply (bool_of … Hb1); ##| napply Hb2; ##] |
---|
| 395 | ##] |
---|
[124] | 396 | ##| // |
---|
[175] | 397 | ##| napply sig_bind2_OK; nrewrite > c5; #x; ncases x; #y; ncases y; #sp l ofs tr H; |
---|
| 398 | napply opt_bind_OK; #v ev; napply (eval_Elvalue … H ev); |
---|
| 399 | ##| napply sig_bind2_OK; #v tr1 H; napply (eval_Ecost … H); |
---|
[124] | 400 | ##| // |
---|
| 401 | ##| // |
---|
[125] | 402 | ##| napply opt_bind_OK; #sl; ncases sl; #sp l el; napply eval_Evar_global; /2/; |
---|
| 403 | ##| napply (eval_Evar_local … c3); |
---|
[175] | 404 | ##| napply sig_bind2_OK; #v; ncases v; //; #sp l ofs tr Hv; nwhd; |
---|
[20] | 405 | napply eval_Ederef; // |
---|
[175] | 406 | ##| ##20,21,22,23,24,25,26,27,28,29,30,31,32,33: // |
---|
[125] | 407 | ##| napply sig_bind2_OK; #x; ncases x; #sp l ofs H; |
---|
[20] | 408 | napply bind_OK; #delta Hdelta; |
---|
| 409 | napply (eval_Efield_struct … H c5 Hdelta); |
---|
[125] | 410 | ##| napply sig_bind2_OK; #x; ncases x; #sp l ofs H; |
---|
[20] | 411 | napply (eval_Efield_union … H c5); |
---|
[124] | 412 | ##| // |
---|
[175] | 413 | ##| // |
---|
[20] | 414 | ##] nqed. |
---|
| 415 | |
---|
| 416 | (* TODO: Can we do this sensibly with a map combinator? *) |
---|
[175] | 417 | 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)) ≝ |
---|
[20] | 418 | match l with |
---|
[175] | 419 | [ nil ⇒ Some ? (OK ? 〈nil val, E0〉) |
---|
[20] | 420 | | cons e1 es ⇒ Some ? ( |
---|
[189] | 421 | do 〈v,tr1〉 ← exec_expr ge e m e1; |
---|
| 422 | do 〈vs,tr2〉 ← exec_exprlist ge e m es; |
---|
[175] | 423 | OK ? 〈cons val v vs, tr1⧺tr2〉) |
---|
[20] | 424 | ]. nwhd; //; |
---|
[175] | 425 | napply sig_bind2_OK; #v tr1 Hv; |
---|
| 426 | napply sig_bind2_OK; #vs tr2 Hvs; |
---|
| 427 | nwhd; napply eval_Econs; //; |
---|
[20] | 428 | nqed. |
---|
| 429 | |
---|
| 430 | (* Don't really want to use subset rather than sigma here, but can't be bothered |
---|
| 431 | with *another* set of coercions. XXX: why do I have to get the recursive |
---|
| 432 | call's property manually? *) |
---|
| 433 | |
---|
| 434 | 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) } ≝ |
---|
| 435 | match l with |
---|
| 436 | [ nil ⇒ Some ? 〈en, m〉 |
---|
| 437 | | cons h vars ⇒ |
---|
| 438 | match h with [ mk_pair id ty ⇒ |
---|
[125] | 439 | match alloc m 0 (sizeof ty) Any with [ mk_pair m1 b1 ⇒ |
---|
| 440 | match exec_alloc_variables (set … id b1 en) m1 vars with |
---|
[20] | 441 | [ sig_intro r p ⇒ r ] |
---|
[125] | 442 | ]]]. nwhd; |
---|
| 443 | ##[ //; |
---|
| 444 | ##| nelim (exec_alloc_variables (set ident ? ? c3 c7 en) c6 c1); |
---|
| 445 | #H; nelim H; //; #H0; nelim H0; nnormalize; #en' m' IH; |
---|
[20] | 446 | napply (alloc_variables_cons … IH); /2/; |
---|
| 447 | nqed. |
---|
| 448 | |
---|
| 449 | (* TODO: can we establish that length params = length vs in advance? *) |
---|
| 450 | 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) ≝ |
---|
| 451 | match params with |
---|
| 452 | [ nil ⇒ match vs with [ nil ⇒ Some ? (OK ? m) | cons _ _ ⇒ Some ? (Error ?) ] |
---|
| 453 | | cons idty params' ⇒ match idty with [ mk_pair id ty ⇒ |
---|
| 454 | match vs with |
---|
| 455 | [ nil ⇒ Some ? (Error ?) |
---|
| 456 | | cons v1 vl ⇒ Some ? ( |
---|
[189] | 457 | do b ← opt_to_res ? (get … id e); |
---|
| 458 | do m1 ← opt_to_res ? (store_value_of_type ty m Any b zero v1); |
---|
[20] | 459 | err_eject ?? (exec_bind_parameters e m1 params' vl)) (* FIXME: don't want to have to eject here *) |
---|
| 460 | ] |
---|
| 461 | ] ]. |
---|
| 462 | nwhd; //; |
---|
[125] | 463 | napply opt_bind_OK; #b eb; |
---|
[20] | 464 | napply opt_bind_OK; #m1 em1; |
---|
| 465 | napply reinject; #m2 em2 Hm2; |
---|
| 466 | napply (bind_parameters_cons … eb em1 Hm2); |
---|
| 467 | nqed. |
---|
| 468 | |
---|
| 469 | ndefinition is_not_void : ∀t:type. res (Σu:unit. t ≠ Tvoid) ≝ |
---|
| 470 | λt. match t with |
---|
| 471 | [ Tvoid ⇒ Some ? (Error ?) |
---|
| 472 | | _ ⇒ Some ? (OK ??) |
---|
| 473 | ]. nwhd; //; @; #H; ndestruct; nqed. |
---|
| 474 | |
---|
| 475 | ninductive decide : Type ≝ |
---|
| 476 | | dy : decide | dn : decide. |
---|
| 477 | |
---|
| 478 | ndefinition dodecide : ∀P:Prop.∀d.∀p:(match d with [ dy ⇒ P | dn ⇒ ¬P ]).P + ¬P. |
---|
| 479 | #P d;ncases d;/2/; nqed. |
---|
| 480 | |
---|
| 481 | ncoercion decide_inject : |
---|
| 482 | ∀P:Prop.∀d.∀p:(match d with [ dy ⇒ P | dn ⇒ ¬P ]).P + ¬P ≝ dodecide |
---|
| 483 | on d:decide to ? + (¬?). |
---|
| 484 | |
---|
| 485 | ndefinition dodecide2 : ∀P:Prop.∀d.∀p:(match d with [ dy ⇒ P | dn ⇒ True ]).res P. |
---|
| 486 | #P d; ncases d; nnormalize; #p; ##[ napply (OK ? p); ##| napply Error ##] nqed. |
---|
| 487 | |
---|
| 488 | ncoercion decide_inject2 : |
---|
| 489 | ∀P:Prop.∀d.∀p:(match d with [ dy ⇒ P | dn ⇒ True ]).res P ≝ dodecide2 |
---|
| 490 | on d:decide to res ?. |
---|
| 491 | |
---|
| 492 | alias id "Tint" = "cic:/matita/c-semantics/Csyntax/type.con(0,2,0)". |
---|
| 493 | alias id "Tfloat" = "cic:/matita/c-semantics/Csyntax/type.con(0,3,0)". |
---|
| 494 | ndefinition sz_eq_dec : ∀s1,s2:intsize. (s1 = s2) + (s1 ≠ s2). |
---|
| 495 | #s1; ncases s1; #s2; ncases s2; /2/; @2; @; #H; ndestruct; nqed. |
---|
| 496 | ndefinition sg_eq_dec : ∀s1,s2:signedness. (s1 = s2) + (s1 ≠ s2). |
---|
| 497 | #s1; ncases s1; #s2; ncases s2; /2/; @2; @; #H; ndestruct; nqed. |
---|
| 498 | ndefinition fs_eq_dec : ∀s1,s2:floatsize. (s1 = s2) + (s1 ≠ s2). |
---|
| 499 | #s1; ncases s1; #s2; ncases s2; /2/; @2; @; #H; ndestruct; nqed. |
---|
| 500 | |
---|
| 501 | nlet rec assert_type_eq (t1,t2:type) : res (t1 = t2) ≝ |
---|
| 502 | match t1 with |
---|
| 503 | [ Tvoid ⇒ match t2 with [ Tvoid ⇒ dy | _ ⇒ dn ] |
---|
| 504 | | 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 ] |
---|
| 505 | | Tfloat f ⇒ match t2 with [ Tfloat f' ⇒ match fs_eq_dec f f' with [ inl _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ] |
---|
[124] | 506 | | Tpointer s t ⇒ match t2 with [ Tpointer s' t' ⇒ |
---|
| 507 | match ms_eq_dec s s' with [ inl _ ⇒ |
---|
| 508 | match assert_type_eq t t' with [ OK _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ] | _ ⇒ dn ] |
---|
| 509 | | Tarray s t n ⇒ match t2 with [ Tarray s' t' n' ⇒ |
---|
| 510 | match ms_eq_dec s s' with [ inl _ ⇒ |
---|
| 511 | match assert_type_eq t t' with [ OK _ ⇒ |
---|
| 512 | match decidable_eq_Z_Type n n' with [ inl _ ⇒ dy | inr _ ⇒ dn ] | _ ⇒ dn ] | _ ⇒ dn ] | _ ⇒ dn ] |
---|
[20] | 513 | | Tfunction tl t ⇒ match t2 with [ Tfunction tl' t' ⇒ match assert_typelist_eq tl tl' with [ OK _ ⇒ |
---|
| 514 | match assert_type_eq t t' with [ OK _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ] | _ ⇒ dn ] |
---|
| 515 | | Tstruct i fl ⇒ |
---|
| 516 | match t2 with [ Tstruct i' fl' ⇒ match ident_eq i i' with [ inl _ ⇒ |
---|
| 517 | match assert_fieldlist_eq fl fl' with [ OK _ ⇒ dy | _ ⇒ dn ] | inr _ ⇒ dn ] | _ ⇒ dn ] |
---|
| 518 | | Tunion i fl ⇒ |
---|
| 519 | match t2 with [ Tunion i' fl' ⇒ match ident_eq i i' with [ inl _ ⇒ |
---|
| 520 | match assert_fieldlist_eq fl fl' with [ OK _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ] | _ ⇒ dn ] |
---|
| 521 | | Tcomp_ptr i ⇒ match t2 with [ Tcomp_ptr i' ⇒ match ident_eq i i' with [ inl _ ⇒ dy | inr _ ⇒ dn ] | _ ⇒ dn ] |
---|
| 522 | ] |
---|
| 523 | and assert_typelist_eq (tl1,tl2:typelist) : res (tl1 = tl2) ≝ |
---|
| 524 | match tl1 with |
---|
| 525 | [ Tnil ⇒ match tl2 with [ Tnil ⇒ dy | _ ⇒ dn ] |
---|
| 526 | | Tcons t1 ts1 ⇒ match tl2 with [ Tnil ⇒ dn | Tcons t2 ts2 ⇒ |
---|
| 527 | match assert_type_eq t1 t2 with [ OK _ ⇒ |
---|
| 528 | match assert_typelist_eq ts1 ts2 with [ OK _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ] ] |
---|
| 529 | ] |
---|
| 530 | and assert_fieldlist_eq (fl1,fl2:fieldlist) : res (fl1 = fl2) ≝ |
---|
| 531 | match fl1 with |
---|
| 532 | [ Fnil ⇒ match fl2 with [ Fnil ⇒ dy | _ ⇒ dn ] |
---|
| 533 | | Fcons i1 t1 fs1 ⇒ match fl2 with [ Fnil ⇒ dn | Fcons i2 t2 fs2 ⇒ |
---|
| 534 | match ident_eq i1 i2 with [ inl _ ⇒ |
---|
| 535 | match assert_type_eq t1 t2 with [ OK _ ⇒ |
---|
| 536 | match assert_fieldlist_eq fs1 fs2 with [ OK _ ⇒ dy | _ ⇒ dn ] |
---|
| 537 | | _ ⇒ dn ] | _ ⇒ dn ] ] |
---|
| 538 | ]. |
---|
| 539 | (* A poor man's clear, otherwise automation picks up recursive calls without |
---|
| 540 | checking that the argument is smaller. *) |
---|
| 541 | ngeneralize in assert_type_eq; |
---|
| 542 | ngeneralize in assert_typelist_eq; |
---|
| 543 | ngeneralize in assert_fieldlist_eq; #avoid1; #_; #avoid2; #_; #avoid3; #_; nwhd; //; |
---|
| 544 | (* XXX: I have no idea why the first // didn't catch these. *) |
---|
| 545 | //; //; //; //; //; //; //; //; //; |
---|
| 546 | nqed. |
---|
| 547 | |
---|
| 548 | nlet rec is_is_call_cont (k:cont) : (is_call_cont k) + (¬is_call_cont k) ≝ |
---|
| 549 | match k with |
---|
| 550 | [ Kstop ⇒ dy |
---|
| 551 | | Kcall _ _ _ _ ⇒ dy |
---|
| 552 | | _ ⇒ dn |
---|
| 553 | ]. nwhd; //; @; #H; nelim H; nqed. |
---|
| 554 | |
---|
| 555 | nlet rec is_Sskip (s:statement) : (s = Sskip) + (s ≠ Sskip) ≝ |
---|
| 556 | match s with |
---|
| 557 | [ Sskip ⇒ dy |
---|
| 558 | | _ ⇒ dn |
---|
| 559 | ]. |
---|
| 560 | ##[ //; |
---|
| 561 | ##| ##*: @; #H; ndestruct; |
---|
| 562 | ##] nqed. |
---|
| 563 | |
---|
| 564 | (* IO monad *) |
---|
| 565 | |
---|
[24] | 566 | (* Interactions are function calls that return a value and do not change |
---|
| 567 | the rest of the Clight program's state. *) |
---|
[25] | 568 | ndefinition io_out ≝ (ident × (list eventval)). |
---|
[20] | 569 | |
---|
[25] | 570 | ndefinition do_io : ident → list eventval → IO eventval io_out eventval ≝ |
---|
| 571 | λfn,args. Interact ?? eventval 〈fn,args〉 (λres. Value ?? eventval res). |
---|
[20] | 572 | |
---|
[25] | 573 | ndefinition ret: ∀T. T → (IO eventval io_out T) ≝ |
---|
| 574 | λT,x.(Value ?? T x). |
---|
[20] | 575 | |
---|
[24] | 576 | (* Checking types of values given to / received from an external function call. *) |
---|
[20] | 577 | |
---|
| 578 | ndefinition check_eventval : ∀ev:eventval. ∀ty:typ. res (Σv:val. eventval_match ev ty v) ≝ |
---|
| 579 | λev,ty. |
---|
| 580 | match ty with |
---|
| 581 | [ Tint ⇒ match ev with [ EVint i ⇒ Some ? (OK ? (Vint i)) | _ ⇒ Some ? (Error ?) ] |
---|
| 582 | | Tfloat ⇒ match ev with [ EVfloat f ⇒ Some ? (OK ? (Vfloat f)) | _ ⇒ Some ? (Error ?) ] |
---|
| 583 | | _ ⇒ Some ? (Error ?) |
---|
| 584 | ]. nwhd; //; nqed. |
---|
| 585 | |
---|
| 586 | ndefinition check_eventval' : ∀v:val. ∀ty:typ. res (Σev:eventval. eventval_match ev ty v) ≝ |
---|
| 587 | λv,ty. |
---|
| 588 | match ty with |
---|
| 589 | [ Tint ⇒ match v with [ Vint i ⇒ Some ? (OK ? (EVint i)) | _ ⇒ Some ? (Error ?) ] |
---|
| 590 | | Tfloat ⇒ match v with [ Vfloat f ⇒ Some ? (OK ? (EVfloat f)) | _ ⇒ Some ? (Error ?) ] |
---|
| 591 | | _ ⇒ Some ? (Error ?) |
---|
| 592 | ]. nwhd; //; nqed. |
---|
| 593 | |
---|
| 594 | nlet rec check_eventval_list (vs: list val) (tys: list typ) : res (Σevs:list eventval. eventval_list_match evs tys vs) ≝ |
---|
| 595 | match vs with |
---|
| 596 | [ nil ⇒ match tys with [ nil ⇒ Some ? (OK ? (nil ?)) | _ ⇒ Some ? (Error ?) ] |
---|
| 597 | | cons v vt ⇒ |
---|
| 598 | match tys with |
---|
| 599 | [ nil ⇒ Some ? (Error ?) |
---|
| 600 | | cons ty tyt ⇒ Some ? ( |
---|
[189] | 601 | do ev ← check_eventval' v ty; |
---|
| 602 | do evt ← check_eventval_list vt tyt; |
---|
[20] | 603 | OK ? ((sig_eject ?? ev)::evt)) |
---|
| 604 | ] |
---|
| 605 | ]. nwhd; //; |
---|
[124] | 606 | napply sig_bind_OK; #ev Hev; |
---|
| 607 | napply sig_bind_OK; #evt Hevt; |
---|
[20] | 608 | nnormalize; /2/; |
---|
| 609 | nqed. |
---|
| 610 | |
---|
| 611 | (* execution *) |
---|
| 612 | |
---|
[124] | 613 | ndefinition store_value_of_type' ≝ |
---|
| 614 | λty,m,l,v. |
---|
| 615 | match l with [ mk_pair pl ofs ⇒ |
---|
| 616 | match pl with [ mk_pair pcl loc ⇒ |
---|
| 617 | store_value_of_type ty m pcl loc ofs v ] ]. |
---|
| 618 | |
---|
[25] | 619 | nlet rec exec_step (ge:genv) (st:state) on st : (IO eventval io_out (Σr:trace × state. step ge st (\fst r) (\snd r))) ≝ |
---|
[20] | 620 | match st with |
---|
| 621 | [ State f s k e m ⇒ |
---|
| 622 | match s with |
---|
| 623 | [ Sassign a1 a2 ⇒ Some ? ( |
---|
[208] | 624 | ! 〈l,tr1〉 ← exec_lvalue ge e m a1; |
---|
| 625 | ! 〈v2,tr2〉 ← exec_expr ge e m a2; |
---|
| 626 | ! m' ← store_value_of_type' (typeof a1) m l v2; |
---|
[175] | 627 | ret ? 〈tr1⧺tr2, State f Sskip k e m'〉) |
---|
[20] | 628 | | Scall lhs a al ⇒ Some ? ( |
---|
[208] | 629 | ! 〈vf,tr2〉 ← exec_expr ge e m a; |
---|
| 630 | ! 〈vargs,tr3〉 ← exec_exprlist ge e m al; |
---|
| 631 | ! fd ← find_funct ? ? ge vf; |
---|
| 632 | ! p ← err_to_io … (assert_type_eq (type_of_fundef fd) (typeof a)); |
---|
[20] | 633 | (* |
---|
| 634 | ! k' ← match lhs with |
---|
| 635 | [ None ⇒ ret ? (Kcall (None ?) f e k) |
---|
| 636 | | Some lhs' ⇒ |
---|
[208] | 637 | ! locofs ← exec_lvalue ge e m lhs'; |
---|
[20] | 638 | ret ? (Kcall (Some ? 〈sig_eject ?? locofs, typeof lhs'〉) f e k) |
---|
[208] | 639 | ]; |
---|
[20] | 640 | ret ? 〈E0, Callstate fd vargs k' m〉) |
---|
| 641 | *) |
---|
| 642 | match lhs with |
---|
[175] | 643 | [ None ⇒ ret ? 〈tr2⧺tr3, Callstate fd vargs (Kcall (None ?) f e k) m〉 |
---|
[20] | 644 | | Some lhs' ⇒ |
---|
[208] | 645 | ! 〈locofs,tr1〉 ← exec_lvalue ge e m lhs'; |
---|
[175] | 646 | ret ? 〈tr1⧺tr2⧺tr3, Callstate fd vargs (Kcall (Some ? 〈locofs, typeof lhs'〉) f e k) m〉 |
---|
[20] | 647 | ]) |
---|
| 648 | | Ssequence s1 s2 ⇒ Some ? (ret ? 〈E0, State f s1 (Kseq s2 k) e m〉) |
---|
| 649 | | Sskip ⇒ |
---|
| 650 | match k with |
---|
| 651 | [ Kseq s k' ⇒ Some ? (ret ? 〈E0, State f s k' e m〉) |
---|
| 652 | | Kstop ⇒ |
---|
| 653 | match fn_return f with |
---|
| 654 | [ Tvoid ⇒ Some ? (ret ? 〈E0, Returnstate Vundef k (free_list m (blocks_of_env e))〉) |
---|
[25] | 655 | | _ ⇒ Some ? (Wrong ???) |
---|
[20] | 656 | ] |
---|
| 657 | | Kcall _ _ _ _ ⇒ |
---|
| 658 | match fn_return f with |
---|
| 659 | [ Tvoid ⇒ Some ? (ret ? 〈E0, Returnstate Vundef k (free_list m (blocks_of_env e))〉) |
---|
[25] | 660 | | _ ⇒ Some ? (Wrong ???) |
---|
[20] | 661 | ] |
---|
| 662 | | Kwhile a s' k' ⇒ Some ? (ret ? 〈E0, State f (Swhile a s') k' e m〉) |
---|
| 663 | | Kdowhile a s' k' ⇒ Some ? ( |
---|
[208] | 664 | ! 〈v,tr〉 ← exec_expr ge e m a; |
---|
| 665 | ! b ← bool_of_val_3 v (typeof a); |
---|
[20] | 666 | match b with |
---|
[175] | 667 | [ true ⇒ ret ? 〈tr, State f (Sdowhile a s') k' e m〉 |
---|
| 668 | | false ⇒ ret ? 〈tr, State f Sskip k' e m〉 |
---|
[20] | 669 | ]) |
---|
| 670 | | Kfor2 a2 a3 s' k' ⇒ Some ? (ret ? 〈E0, State f a3 (Kfor3 a2 a3 s' k') e m〉) |
---|
| 671 | | Kfor3 a2 a3 s' k' ⇒ Some ? (ret ? 〈E0, State f (Sfor Sskip a2 a3 s') k' e m〉) |
---|
| 672 | | Kswitch k' ⇒ Some ? (ret ? 〈E0, State f Sskip k' e m〉) |
---|
[25] | 673 | | _ ⇒ Some ? (Wrong ???) |
---|
[20] | 674 | ] |
---|
| 675 | | Scontinue ⇒ |
---|
| 676 | match k with |
---|
| 677 | [ Kseq s' k' ⇒ Some ? (ret ? 〈E0, State f Scontinue k' e m〉) |
---|
| 678 | | Kwhile a s' k' ⇒ Some ? (ret ? 〈E0, State f (Swhile a s') k' e m〉) |
---|
| 679 | | Kdowhile a s' k' ⇒ Some ? ( |
---|
[208] | 680 | ! 〈v,tr〉 ← exec_expr ge e m a; |
---|
| 681 | ! b ← bool_of_val_3 v (typeof a); |
---|
[20] | 682 | match b with |
---|
[175] | 683 | [ true ⇒ ret ? 〈tr, State f (Sdowhile a s') k' e m〉 |
---|
| 684 | | false ⇒ ret ? 〈tr, State f Sskip k' e m〉 |
---|
[20] | 685 | ]) |
---|
| 686 | | Kfor2 a2 a3 s' k' ⇒ Some ? (ret ? 〈E0, State f a3 (Kfor3 a2 a3 s' k') e m〉) |
---|
| 687 | | Kswitch k' ⇒ Some ? (ret ? 〈E0, State f Scontinue k' e m〉) |
---|
[25] | 688 | | _ ⇒ Some ? (Wrong ???) |
---|
[20] | 689 | ] |
---|
| 690 | | Sbreak ⇒ |
---|
| 691 | match k with |
---|
| 692 | [ Kseq s' k' ⇒ Some ? (ret ? 〈E0, State f Sbreak k' e m〉) |
---|
| 693 | | Kwhile a s' k' ⇒ Some ? (ret ? 〈E0, State f Sskip k' e m〉) |
---|
| 694 | | Kdowhile a s' k' ⇒ Some ? (ret ? 〈E0, State f Sskip k' e m〉) |
---|
| 695 | | Kfor2 a2 a3 s' k' ⇒ Some ? (ret ? 〈E0, State f Sskip k' e m〉) |
---|
| 696 | | Kswitch k' ⇒ Some ? (ret ? 〈E0, State f Sskip k' e m〉) |
---|
[25] | 697 | | _ ⇒ Some ? (Wrong ???) |
---|
[20] | 698 | ] |
---|
| 699 | | Sifthenelse a s1 s2 ⇒ Some ? ( |
---|
[208] | 700 | ! 〈v,tr〉 ← exec_expr ge e m a; |
---|
| 701 | ! b ← bool_of_val_3 v (typeof a); |
---|
[175] | 702 | ret ? 〈tr, State f (if b then s1 else s2) k e m〉) |
---|
[20] | 703 | | Swhile a s' ⇒ Some ? ( |
---|
[208] | 704 | ! 〈v,tr〉 ← exec_expr ge e m a; |
---|
| 705 | ! b ← bool_of_val_3 v (typeof a); |
---|
[175] | 706 | ret ? 〈tr, if b then State f s' (Kwhile a s' k) e m |
---|
| 707 | else State f Sskip k e m〉) |
---|
[20] | 708 | | Sdowhile a s' ⇒ Some ? (ret ? 〈E0, State f s' (Kdowhile a s' k) e m〉) |
---|
| 709 | | Sfor a1 a2 a3 s' ⇒ |
---|
| 710 | match is_Sskip a1 with |
---|
| 711 | [ inl _ ⇒ Some ? ( |
---|
[208] | 712 | ! 〈v,tr〉 ← exec_expr ge e m a2; |
---|
| 713 | ! b ← bool_of_val_3 v (typeof a2); |
---|
[175] | 714 | ret ? 〈tr, State f (if b then s' else Sskip) (if b then (Kfor2 a2 a3 s' k) else k) e m〉) |
---|
[20] | 715 | | inr _ ⇒ Some ? (ret ? 〈E0, State f a1 (Kseq (Sfor Sskip a2 a3 s') k) e m〉) |
---|
| 716 | ] |
---|
| 717 | | Sreturn a_opt ⇒ |
---|
| 718 | match a_opt with |
---|
| 719 | [ None ⇒ match fn_return f with |
---|
| 720 | [ Tvoid ⇒ Some ? (ret ? 〈E0, Returnstate Vundef (call_cont k) (free_list m (blocks_of_env e))〉) |
---|
[25] | 721 | | _ ⇒ Some ? (Wrong ???) |
---|
[20] | 722 | ] |
---|
| 723 | | Some a ⇒ Some ? ( |
---|
[208] | 724 | ! u ← is_not_void (fn_return f); |
---|
| 725 | ! 〈v,tr〉 ← exec_expr ge e m a; |
---|
[175] | 726 | ret ? 〈tr, Returnstate v (call_cont k) (free_list m (blocks_of_env e))〉) |
---|
[20] | 727 | ] |
---|
| 728 | | Sswitch a sl ⇒ Some ? ( |
---|
[208] | 729 | ! 〈v,tr〉 ← exec_expr ge e m a; |
---|
[175] | 730 | match v with [ Vint n ⇒ ret ? 〈tr, State f (seq_of_labeled_statement (select_switch n sl)) (Kswitch k) e m〉 |
---|
[25] | 731 | | _ ⇒ Wrong ??? ]) |
---|
[20] | 732 | | Slabel lbl s' ⇒ Some ? (ret ? 〈E0, State f s' k e m〉) |
---|
| 733 | | Sgoto lbl ⇒ |
---|
| 734 | match find_label lbl (fn_body f) (call_cont k) with |
---|
| 735 | [ Some sk' ⇒ match sk' with [ mk_pair s' k' ⇒ Some ? (ret ? 〈E0, State f s' k' e m〉) ] |
---|
[25] | 736 | | None ⇒ Some ? (Wrong ???) |
---|
[20] | 737 | ] |
---|
[175] | 738 | | Scost lbl s' ⇒ Some ? (ret ? 〈Echarge lbl, State f s' k e m〉) |
---|
[20] | 739 | ] |
---|
| 740 | | Callstate f0 vargs k m ⇒ |
---|
| 741 | match f0 with |
---|
| 742 | [ Internal f ⇒ Some ? ( |
---|
| 743 | match exec_alloc_variables empty_env m ((fn_params f) @ (fn_vars f)) with [ mk_pair e m1 ⇒ |
---|
[208] | 744 | ! m2 ← exec_bind_parameters e m1 (fn_params f) vargs; |
---|
[20] | 745 | ret ? 〈E0, State f (fn_body f) k e m2〉 |
---|
| 746 | ]) |
---|
| 747 | | External f argtys retty ⇒ Some ? ( |
---|
[208] | 748 | ! evargs ← check_eventval_list vargs (typlist_of_typelist argtys); |
---|
| 749 | ! evres ← do_io f evargs; |
---|
| 750 | ! vres ← check_eventval evres (proj_sig_res (signature_of_type argtys retty)); |
---|
[20] | 751 | ret ? 〈(Eextcall f evargs evres), Returnstate vres k m〉) |
---|
| 752 | ] |
---|
| 753 | | Returnstate res k m ⇒ |
---|
| 754 | match k with |
---|
| 755 | [ Kcall r f e k' ⇒ |
---|
| 756 | match r with |
---|
| 757 | [ None ⇒ |
---|
| 758 | match res with |
---|
| 759 | [ Vundef ⇒ Some ? (ret ? 〈E0, (State f Sskip k' e m)〉) |
---|
[25] | 760 | | _ ⇒ Some ? (Wrong ???) |
---|
[20] | 761 | ] |
---|
| 762 | | Some r' ⇒ |
---|
[124] | 763 | match r' with [ mk_pair l ty ⇒ |
---|
| 764 | Some ? ( |
---|
[208] | 765 | ! m' ← store_value_of_type' ty m l res; |
---|
[20] | 766 | ret ? 〈E0, (State f Sskip k' e m')〉) |
---|
| 767 | ] |
---|
| 768 | ] |
---|
[25] | 769 | | _ ⇒ Some ? (Wrong ???) |
---|
[20] | 770 | ] |
---|
| 771 | ]. nwhd; //; |
---|
| 772 | ##[ nrewrite > c7; napply step_skip_call; //; napply c8; |
---|
| 773 | ##| napply step_skip_or_continue_while; @; //; |
---|
[175] | 774 | ##| napply sig_bindIO2_OK; #v tr Hv; |
---|
[20] | 775 | napply sig_bindIO_OK; #b; ncases b; #Hb; |
---|
| 776 | ##[ napply (step_skip_or_continue_dowhile_true … Hv); |
---|
| 777 | ##[ @; // ##| napply (bool_of … Hb); ##] |
---|
| 778 | ##| napply (step_skip_or_continue_dowhile_false … Hv); |
---|
| 779 | ##[ @; // ##| napply (bool_of … Hb); ##] |
---|
| 780 | ##] |
---|
| 781 | ##| napply step_skip_or_continue_for2; @; //; |
---|
| 782 | ##| napply step_skip_break_switch; @; //; |
---|
| 783 | ##| nrewrite > c11; napply step_skip_call; //; napply c12; |
---|
[175] | 784 | ##| napply sig_bindIO2_OK; #x; ncases x; #y; ncases y; #pcl loc ofs tr1 Hlval; |
---|
| 785 | napply sig_bindIO2_OK; #v2 tr2 Hv2; |
---|
[20] | 786 | napply opt_bindIO_OK; #m' em'; |
---|
| 787 | nwhd; napply (step_assign … Hlval Hv2 em'); |
---|
[175] | 788 | ##| napply sig_bindIO2_OK; #vf tr1 Hvf; |
---|
| 789 | napply sig_bindIO2_OK; #vargs tr2 Hvargs; |
---|
[20] | 790 | napply opt_bindIO_OK; #fd efd; |
---|
| 791 | napply bindIO_OK; #ety; |
---|
| 792 | ncases c6; nwhd; |
---|
| 793 | ##[ napply (step_call_none … Hvf Hvargs efd ety); |
---|
| 794 | ##| #lhs'; |
---|
[175] | 795 | napply sig_bindIO2_OK; #x; ncases x; #y; ncases y; #pcl loc ofs tr3 Hlocofs; |
---|
[20] | 796 | nwhd; napply (step_call_some … Hlocofs Hvf Hvargs efd ety); |
---|
| 797 | ##] |
---|
[175] | 798 | ##| napply sig_bindIO2_OK; #v tr Hv; |
---|
[20] | 799 | napply sig_bindIO_OK; #b; ncases b; #Hb; |
---|
| 800 | ##[ napply (step_ifthenelse_true … Hv); napply (bool_of … Hb); |
---|
| 801 | ##| napply (step_ifthenelse_false … Hv); napply (bool_of … Hb) |
---|
| 802 | ##] |
---|
[175] | 803 | ##| napply sig_bindIO2_OK; #v tr Hv; |
---|
[20] | 804 | napply sig_bindIO_OK; #b; ncases b; #Hb; |
---|
| 805 | ##[ napply (step_while_true … Hv); napply (bool_of … Hb); |
---|
| 806 | ##| napply (step_while_false … Hv); napply (bool_of … Hb); |
---|
| 807 | ##] |
---|
| 808 | ##| nrewrite > c11; |
---|
[175] | 809 | napply sig_bindIO2_OK; #v tr Hv; |
---|
[20] | 810 | napply sig_bindIO_OK; #b; ncases b; #Hb; |
---|
| 811 | ##[ napply (step_for_true … Hv); napply (bool_of … Hb); |
---|
| 812 | ##| napply (step_for_false … Hv); napply (bool_of … Hb); |
---|
| 813 | ##] |
---|
| 814 | ##| napply step_for_start; //; |
---|
| 815 | ##| napply step_skip_break_switch; @2; //; |
---|
| 816 | ##| napply step_skip_or_continue_while; @2; //; |
---|
[175] | 817 | ##| napply sig_bindIO2_OK; #v tr Hv; |
---|
[20] | 818 | napply sig_bindIO_OK; #b; ncases b; #Hb; |
---|
| 819 | ##[ napply (step_skip_or_continue_dowhile_true … Hv); |
---|
| 820 | ##[ @2; // ##| napply (bool_of … Hb); ##] |
---|
| 821 | ##| napply (step_skip_or_continue_dowhile_false … Hv); |
---|
| 822 | ##[ @2; // ##| napply (bool_of … Hb); ##] |
---|
| 823 | ##] |
---|
| 824 | ##| napply step_skip_or_continue_for2; @2; // |
---|
| 825 | ##| napply step_return_0; napply c9; |
---|
| 826 | ##| napply sig_bindIO_OK; #u Hnotvoid; |
---|
[175] | 827 | napply sig_bindIO2_OK; #v tr Hv; |
---|
[20] | 828 | nwhd; napply (step_return_1 … Hnotvoid Hv); |
---|
[175] | 829 | ##| napply sig_bindIO2_OK; #v; ncases v; //; #n tr Hv; |
---|
[20] | 830 | napply step_switch; //; |
---|
| 831 | ##| napply step_goto; nrewrite < c12; napply c9; |
---|
| 832 | ##| napply extract_subset_pair_io; #e m1 ealloc Halloc; |
---|
| 833 | napply sig_bindIO_OK; #m2 Hbind; |
---|
| 834 | nwhd; napply (step_internal_function … Halloc Hbind); |
---|
| 835 | ##| napply sig_bindIO_OK; #evs Hevs; |
---|
| 836 | napply bindIO_OK; #eres; |
---|
| 837 | napply sig_bindIO_OK; #res Hres; |
---|
| 838 | nwhd; napply step_external_function; @; ##[ napply Hevs; ##| napply Hres; ##] |
---|
[124] | 839 | ##| ncases c11; #x; ncases x; #pcl b ofs; |
---|
| 840 | napply opt_bindIO_OK; #m' em'; napply step_returnstate_1; nwhd in em':(??%?); //; |
---|
[20] | 841 | ##] |
---|
| 842 | nqed. |
---|
| 843 | |
---|
[25] | 844 | nlet rec make_initial_state (p:program) : IO eventval io_out (Σs:state. initial_state p s) ≝ |
---|
[20] | 845 | let ge ≝ globalenv Genv ?? p in |
---|
| 846 | let m0 ≝ init_mem Genv ?? p in |
---|
| 847 | Some ? ( |
---|
[208] | 848 | ! 〈sp,b〉 ← find_symbol ? ? ge (prog_main ?? p); |
---|
| 849 | ! u ← opt_to_io … (match ms_eq_dec sp Code with [ inl _ ⇒ Some ? something | inr _ ⇒ None ? ]); |
---|
| 850 | ! f ← find_funct_ptr ? ? ge b; |
---|
[20] | 851 | ret ? (Callstate f (nil ?) Kstop m0)). |
---|
| 852 | nwhd; |
---|
[125] | 853 | napply opt_bindIO2_OK; #sp b esb; |
---|
| 854 | napply opt_bindIO_OK; #u ecode; |
---|
[20] | 855 | napply opt_bindIO_OK; #f ef; |
---|
[156] | 856 | ncases sp in esb ecode; #esb ecode; nwhd in ecode:(??%%); ##[ ##1,2,3,4,5: ndestruct (ecode); ##] |
---|
[125] | 857 | nwhd; napply (initial_state_intro … esb ef); |
---|
[20] | 858 | nqed. |
---|
| 859 | |
---|
| 860 | ndefinition is_final_state : ∀st:state. (∃r. final_state st r) + (¬∃r. final_state st r). |
---|
| 861 | #st; nelim st; |
---|
| 862 | ##[ #f s k e m; @2; @;*; #r H; ninversion H; #i m e; ndestruct; |
---|
| 863 | ##| #f l k m; @2; @;*; #r H; ninversion H; #i m e; ndestruct; |
---|
| 864 | ##| #v k m; ncases k; |
---|
| 865 | ##[ ncases v; |
---|
| 866 | ##[ ##2: #i; @1; @ i; //; |
---|
| 867 | ##| ##1: @2; @; *; #r H; ninversion H; #i m e; ndestruct; |
---|
| 868 | ##| #f; @2; @; *; #r H; ninversion H; #i m e; ndestruct; |
---|
[124] | 869 | ##| #pcl b of; @2; @; *; #r H; ninversion H; #i m e; ndestruct; |
---|
[20] | 870 | ##] |
---|
| 871 | ##| #a b; @2; @; *; #r H; ninversion H; #i m e; ndestruct; |
---|
| 872 | ##| ##3,4: #a b c; @2; @; *; #r H; ninversion H; #i m e; ndestruct; |
---|
| 873 | ##| ##5,6,8: #a b c d; @2; @; *; #r H; ninversion H; #i m e; ndestruct; |
---|
| 874 | ##| #a; @2; @; *; #r H; ninversion H; #i m e; ndestruct; |
---|
| 875 | ##] |
---|
| 876 | ##] nqed. |
---|
| 877 | |
---|
| 878 | nlet rec exec_steps (n:nat) (ge:genv) (s:state) : |
---|
[25] | 879 | IO eventval io_out (Σts:trace×state. star (mk_transrel ?? step) ge s (\fst ts) (\snd ts)) ≝ |
---|
[20] | 880 | match is_final_state s with |
---|
| 881 | [ inl _ ⇒ Some ? (ret ? 〈E0, s〉) |
---|
| 882 | | inr _ ⇒ |
---|
| 883 | match n with |
---|
| 884 | [ O ⇒ Some ? (ret ? 〈E0, s〉) |
---|
| 885 | | S n' ⇒ Some ? ( |
---|
[208] | 886 | ! 〈t,s'〉 ← exec_step ge s; |
---|
[152] | 887 | (* ! 〈t,s'〉 ← match s with |
---|
| 888 | [ 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)) ] |
---|
| 889 | | 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)) ] |
---|
| 890 | | Returnstate r k m ⇒ match m with [ mk_mem c n p ⇒ exec_step ge (Returnstate r k (mk_mem c n p)) ] |
---|
[208] | 891 | ] ;*) |
---|
[152] | 892 | ! 〈t',s''〉 ← match s' with |
---|
| 893 | [ 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)) ] |
---|
| 894 | | 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)) ] |
---|
| 895 | | Returnstate r k m ⇒ match m with [ mk_mem c n p ⇒ exec_steps n' ge (Returnstate r k (mk_mem c n p)) ] |
---|
[208] | 896 | ] ; |
---|
| 897 | (* ! 〈t',s''〉 ← exec_steps n' ge s';*) |
---|
[20] | 898 | ret ? 〈t ⧺ t',s''〉) |
---|
| 899 | ] |
---|
| 900 | ]. nwhd; /2/; |
---|
[152] | 901 | napply sig_bindIO2_OK; #t s'; ncases s'; ##[ #f st k e m; ##| #fd args k m; ##| #r k m; ##] |
---|
| 902 | nwhd in ⊢ (? → ?????(??????%?)); |
---|
| 903 | ncases m; #mc mn mp; #H1; |
---|
| 904 | nwhd in ⊢ (?????(??????%?)); |
---|
[20] | 905 | napply sig_bindIO2_OK; #t' s'' IH; |
---|
| 906 | nwhd; napply (star_step … IH); //; |
---|
| 907 | nqed. |
---|
| 908 | (* |
---|
| 909 | nlet rec exec_steps_without_proof (n:nat) (ge:genv) (s:state) : |
---|
| 910 | res (trace×state) ≝ |
---|
| 911 | match is_final_state s with |
---|
| 912 | [ inl _ ⇒ OK ? 〈E0, s〉 |
---|
| 913 | | inr _ ⇒ |
---|
| 914 | match n with |
---|
| 915 | [ O ⇒ OK ? 〈E0, s〉 |
---|
| 916 | | S n' ⇒ |
---|
[208] | 917 | 〈t,s'〉 ← exec_step ge s; |
---|
| 918 | 〈t',s''〉 ← exec_steps_without_proof n' ge s'; |
---|
[20] | 919 | OK ? 〈t ⧺ t',s''〉 |
---|
| 920 | ] |
---|
| 921 | ]. |
---|
| 922 | *) |
---|
[174] | 923 | |
---|
| 924 | (* A (possibly non-terminating) execution. *) |
---|
| 925 | ncoinductive execution : Type ≝ |
---|
| 926 | | e_stop : trace → state → execution |
---|
| 927 | | e_step : trace → state → execution → execution |
---|
| 928 | | e_wrong : execution |
---|
| 929 | | e_interact : io_out → (eventval → execution) → execution. |
---|
| 930 | |
---|
| 931 | nlet corec exec_inf_aux (ge:genv) (s:IO eventval io_out (trace×state)) : execution ≝ |
---|
| 932 | match s with |
---|
| 933 | [ Wrong ⇒ e_wrong |
---|
| 934 | | Value v ⇒ match v with [ mk_pair t s' ⇒ |
---|
| 935 | match is_final_state s' with |
---|
| 936 | [ inl _ ⇒ e_stop t s' |
---|
| 937 | | inr _ ⇒ e_step t s' (exec_inf_aux ge (exec_step ge s')) ] ] |
---|
| 938 | | Interact out k' ⇒ e_interact out (λv. exec_inf_aux ge (k' v)) |
---|
| 939 | ]. |
---|
| 940 | |
---|
| 941 | ndefinition exec_inf : program → execution ≝ |
---|
[208] | 942 | λp. exec_inf_aux (globalenv Genv ?? p) (! s ← make_initial_state p; ret ? 〈E0,sig_eject ?? s〉). |
---|
[174] | 943 | |
---|