source: Deliverables/D3.1/C-semantics/Cexec.ma @ 481

Last change on this file since 481 was 481, checked in by campbell, 9 years ago

Tcomp_ptr should take the memory region and use that to calculate its size.

File size: 33.1 KB
Line 
1
2include "Csem.ma".
3
4include "extralib.ma".
5include "IOMonad.ma".
6
7include "Plogic/russell_support.ma".
8
9ndefinition 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
12ndefinition 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
25ndefinition 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
29ndefinition sig_eject : ∀A.∀P: A → Prop. sigma A P → A ≝
30  λA,P,a.match a with [ sig_intro w p ⇒ w].
31
32ncoercion 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 ? ?).
35ncoercion err_eject : ∀A.∀P:A → Prop.∀c:res (sigma A P).res A ≝ err_eject
36  on _c:res (sigma ? ?) to res ?.
37ncoercion sig_eject : ∀A.∀P:A → Prop.∀c:sigma A P.A ≝ sig_eject
38  on _c:sigma ? ? to ?.
39
40ndefinition P_res: ∀A.∀P:A → Prop.res A → Prop ≝
41  λA,P,a. match a with [ Error ⇒ True | OK v ⇒ P v ].
42
43ndefinition exec_bool_of_val : ∀v:val. ∀ty:type. res bool ≝
44  λv,ty. match v in val with
45  [ Vint i ⇒ match ty with
46    [ Tint _ _ ⇒ OK ? (¬eq i zero)
47    | Tpointer _ _ ⇒ OK ? (¬eq i zero)
48    | _ ⇒ Error ?
49    ]
50  | Vfloat f ⇒ match ty with
51    [ Tfloat _ ⇒ OK ? (¬Fcmp Ceq f Fzero)
52    | _ ⇒ Error ?
53    ]
54  | Vptr _ _ _ ⇒ match ty with
55    [ Tint _ _ ⇒ OK ? true
56    | Tpointer _ _ ⇒ OK ? true
57    | _ ⇒ Error ?
58    ]
59  | _ ⇒ Error ?
60  ].
61
62nlemma bool_of_val_complete : ∀v,ty,r. bool_of_val v ty r → ∃b. r = of_bool b ∧ exec_bool_of_val v ty = OK ? b.
63#v ty r H; nelim H; #v t H'; nelim H';
64  ##[ #i is s ne; @ true; @; //; nwhd in ⊢ (??%?); nrewrite > (eq_false … ne); //;
65  ##| #p b i i0 s; @ true; @; //
66  ##| #i p t ne; @ true; @; //; nwhd in ⊢ (??%?); nrewrite > (eq_false … ne); //;
67  ##| #p b i p0 t0; @ true; @; //
68  ##| #f s ne; @ true; @; //; nwhd in ⊢ (??%?); nrewrite > (Feq_zero_false … ne); //;
69  ##| #i s; @ false; @; //;
70  ##| #p t; @ false; @; //;
71  ##| #s; @ false; @; //; nwhd in ⊢ (??%?); nrewrite > (Feq_zero_true …); //;
72  ##]
73nqed.
74
75(* Prove a few minor results to make proof obligations easy. *)
76
77nlemma bind_OK: ∀A,B,P,e,f.
78  (∀v. e = OK A v → match f v with [ Error ⇒ True | OK v' ⇒ P v' ]) →
79  match bind A B e f with [ Error ⇒ True | OK v ⇒ P v ].
80#A B P e f; nelim e; /2/; nqed.
81
82nlemma sig_bind_OK: ∀A,B. ∀P:A → Prop. ∀P':B → Prop. ∀e:res (sigma A P). ∀f:sigma A P → res B.
83  (∀v:A. ∀p:P v. match f (sig_intro A P v p) with [ Error ⇒ True | OK v' ⇒ P' v'] ) →
84  match bind (sigma A P) B e f with [ Error ⇒ True | OK v' ⇒ P' v' ].
85#A B P P' e f; nelim e;
86##[ #v0; nelim v0; #v Hv IH; napply IH;
87##| #_; napply I;
88##] nqed.
89
90nlemma bind2_OK: ∀A,B,C,P,e,f.
91  (∀v1,v2. e = OK ? 〈v1,v2〉 → match f v1 v2 with [ Error ⇒ True | OK v' ⇒ P v' ]) →
92  match bind2 A B C e f with [ Error ⇒ True | OK v ⇒ P v ].
93#A B C P e f; nelim e; //; #v; ncases v; /2/; nqed.
94
95nlemma sig_bind2_OK: ∀A,B,C. ∀P:A×B → Prop. ∀P':C → Prop. ∀e:res (sigma (A×B) P). ∀f:A → B → res C.
96  (∀v1:A.∀v2:B. P 〈v1,v2〉 → match f v1 v2 with [ Error ⇒ True | OK v' ⇒ P' v'] ) →
97  match bind2 A B C e f with [ Error ⇒ True | OK v' ⇒ P' v' ].
98#A B C P P' e f; nelim e; //;
99#v0; nelim v0; #v; nelim v; #v1 v2 Hv IH; napply IH; //; nqed.
100
101ndefinition opt_to_res ≝ λA.λv:option A. match v with [ None ⇒ Error A | Some v ⇒ OK A v ].
102nlemma opt_OK: ∀A,P,e.
103  (∀v. e = Some ? v → P v) →
104  match opt_to_res A e with [ Error ⇒ True | OK v ⇒ P v ].
105#A P e; nelim e; /2/;
106nqed.
107
108nlemma opt_bind_OK: ∀A,B,P,e,f.
109  (∀v. e = Some A v → match f v with [ Error ⇒ True | OK v' ⇒ P v' ]) →
110  match bind A B (opt_to_res A e) f with [ Error ⇒ True | OK v ⇒ P v ].
111#A B P e f; nelim e; nnormalize; /2/; nqed.
112
113nlemma extract_subset_pair: ∀A,B,C,P. ∀e:{e:A×B | P e}. ∀Q:A→B→res C. ∀R:C→Prop.
114  (∀a,b. eject ?? e = 〈a,b〉 → P 〈a,b〉 → match Q a b with [ OK v ⇒ R v | Error ⇒ True]) →
115  match match eject ?? e with [ mk_pair a b ⇒ Q a b ] with [ OK v ⇒ R v | Error ⇒ True ].
116#A B C P e Q R; ncases e; #e'; ncases e'; nnormalize;
117##[ #H; napply (False_ind … H);
118##| #e''; ncases e''; #a b Pab H; nnormalize; /2/;
119##] nqed.
120
121(*
122nremark err_later: ∀A,B. ∀e:res A. match e with [ Error ⇒ Error B | OK v ⇒ Error B ] = Error B.
123#A B e; ncases e; //; nqed.
124*)
125
126ndefinition try_cast_null : ∀m:mem. ∀i:int. ∀ty:type. ∀ty':type. res val  ≝
127λm:mem. λi:int. λty:type. λty':type.
128match eq i zero with
129[ true ⇒
130  match ty with
131  [ Tint _ _ ⇒
132    match ty' with
133    [ Tpointer _ _ ⇒ OK ? (Vint i)
134    | Tarray _ _ _ ⇒ OK ? (Vint i)
135    | Tfunction _ _ ⇒ OK ? (Vint i)
136    | _ ⇒ Error ?
137    ]
138  | Tpointer _ _ ⇒
139    match ty' with
140    [ Tpointer _ _ ⇒ OK ? (Vint i)
141    | Tarray _ _ _ ⇒ OK ? (Vint i)
142    | Tfunction _ _ ⇒ OK ? (Vint i)
143    | _ ⇒ Error ?
144    ]
145  | Tarray _ _ _ ⇒
146    match ty' with
147    [ Tpointer _ _ ⇒ OK ? (Vint i)
148    | Tarray _ _ _ ⇒ OK ? (Vint i)
149    | Tfunction _ _ ⇒ OK ? (Vint i)
150    | _ ⇒ Error ?
151    ]
152  | Tfunction _ _ ⇒
153    match ty' with
154    [ Tpointer _ _ ⇒ OK ? (Vint i)
155    | Tarray _ _ _ ⇒ OK ? (Vint i)
156    | Tfunction _ _ ⇒ OK ? (Vint i)
157    | _ ⇒ Error ?
158    ]
159  | _ ⇒ Error ?
160  ]
161| false ⇒ Error ?
162].
163
164ndefinition ms_eq_dec : ∀s1,s2:region. (s1 = s2) + (s1 ≠ s2).
165#s1; ncases s1; #s2; ncases s2; /2/; @2; @; #H; ndestruct; nqed.
166
167ndefinition exec_cast : ∀m:mem. ∀v:val. ∀ty:type. ∀ty':type. res val ≝
168λm:mem. λv:val. λty:type. λty':type.
169match v with
170[ Vint i ⇒
171  match ty with
172  [ Tint sz1 si1 ⇒
173    match ty' with
174    [ Tint sz2 si2 ⇒ OK ? (Vint (cast_int_int sz2 si2 i))
175    | Tfloat sz2 ⇒ OK ? (Vfloat (cast_float_float sz2 (cast_int_float si1 i)))
176    | Tpointer _ _ ⇒ do r ← try_cast_null m i ty ty'; OK val r
177    | Tarray _ _ _ ⇒ do r ← try_cast_null m i ty ty'; OK val r
178    | Tfunction _ _ ⇒ do r ← try_cast_null m i ty ty'; OK val r
179    | _ ⇒ Error ?
180    ]
181  | Tpointer _ _ ⇒ do r ← try_cast_null m i ty ty'; OK val r
182  | Tarray _ _ _ ⇒ do r ← try_cast_null m i ty ty'; OK val r
183  | Tfunction _ _ ⇒ do r ← try_cast_null m i ty ty'; OK val r
184  | _ ⇒ Error ?
185  ]
186| Vfloat f ⇒
187  match ty with
188  [ Tfloat sz ⇒
189    match ty' with
190    [ Tint sz' si' ⇒ OK ? (Vint (cast_int_int sz' si' (cast_float_int si' f)))
191    | Tfloat sz' ⇒ OK ? (Vfloat (cast_float_float sz' f))
192    | _ ⇒ Error ?
193    ]
194  | _ ⇒ Error ?
195  ]
196| Vptr p b ofs ⇒
197    do s ← match ty with [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code | _ ⇒ Error ? ];
198    do u ← match ms_eq_dec p s with [ inl _ ⇒ OK ? something | inr _ ⇒ Error ? ];
199    do s' ← match ty' with
200         [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code
201         | _ ⇒ Error ? ];
202    if is_pointer_compat (block_space m b) s'
203    then OK ? (Vptr s' b ofs)
204    else Error ?
205| _ ⇒ Error ?
206].
207
208ndefinition load_value_of_type' ≝
209λty,m,l. match l with [ mk_pair pl ofs ⇒ match pl with [ mk_pair psp loc ⇒
210  load_value_of_type ty m psp loc ofs ] ].
211
212(* To make the evaluation of bare lvalue expressions invoke exec_lvalue with
213   a structurally smaller value, we break out the surrounding Expr constructor
214   and use exec_lvalue'. *)
215
216nlet rec exec_expr (ge:genv) (en:env) (m:mem) (e:expr) on e : res (val×trace) ≝
217match e with
218[ Expr e' ty ⇒
219  match e' with
220  [ Econst_int i ⇒ OK ? 〈Vint i, E0〉
221  | Econst_float f ⇒ OK ? 〈Vfloat f, E0〉
222  | Evar _ ⇒
223      do 〈l,tr〉 ← exec_lvalue' ge en m e' ty;
224      do v ← opt_to_res ? (load_value_of_type' ty m l);
225      OK ? 〈v,tr〉
226  | Ederef _ ⇒
227      do 〈l,tr〉 ← exec_lvalue' ge en m e' ty;
228      do v ← opt_to_res ? (load_value_of_type' ty m l);
229      OK ? 〈v,tr〉
230  | Efield _ _ ⇒
231      do 〈l,tr〉 ← exec_lvalue' ge en m e' ty;
232      do v ← opt_to_res ? (load_value_of_type' ty m l);
233      OK ? 〈v,tr〉
234  | Eaddrof a ⇒
235      do 〈plo,tr〉 ← exec_lvalue ge en m a;
236      OK ? 〈match plo with [ mk_pair pl ofs ⇒ match pl with [ mk_pair pcl loc ⇒ Vptr pcl loc ofs ] ], tr〉
237  | Esizeof ty' ⇒ OK ? 〈Vint (repr (sizeof ty')), E0〉
238  | Eunop op a ⇒
239      do 〈v1,tr〉 ← exec_expr ge en m a;
240      do v ← opt_to_res ? (sem_unary_operation op v1 (typeof a));
241      OK ? 〈v,tr〉
242  | Ebinop op a1 a2 ⇒
243      do 〈v1,tr1〉 ← exec_expr ge en m a1;
244      do 〈v2,tr2〉 ← exec_expr ge en m a2;
245      do v ← opt_to_res ? (sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m);
246      OK ? 〈v,tr1⧺tr2〉
247  | Econdition a1 a2 a3 ⇒
248      do 〈v,tr1〉 ← exec_expr ge en m a1;
249      do b ← exec_bool_of_val v (typeof a1);
250      do 〈v',tr2〉 ← match b return λ_.res (val×trace) with
251                 [ true ⇒ (exec_expr ge en m a2)
252                 | false ⇒ (exec_expr ge en m a3) ];
253      OK ? 〈v',tr1⧺tr2〉
254(*      if b then exec_expr ge en m a2 else exec_expr ge en m a3)*)
255  | Eorbool a1 a2 ⇒
256      do 〈v1,tr1〉 ← exec_expr ge en m a1;
257      do b1 ← exec_bool_of_val v1 (typeof a1);
258      match b1 return λ_.res (val×trace) with [ true ⇒ OK ? 〈Vtrue,tr1〉 | false ⇒
259        do 〈v2,tr2〉 ← exec_expr ge en m a2;
260        do b2 ← exec_bool_of_val v2 (typeof a2);
261        OK ? 〈of_bool b2, tr1⧺tr2〉 ]
262  | Eandbool a1 a2 ⇒
263      do 〈v1,tr1〉 ← exec_expr ge en m a1;
264      do b1 ← exec_bool_of_val v1 (typeof a1);
265      match b1 return λ_.res (val×trace) with [ true ⇒
266        do 〈v2,tr2〉 ← exec_expr ge en m a2;
267        do b2 ← exec_bool_of_val v2 (typeof a2);
268        OK ? 〈of_bool b2, tr1⧺tr2〉
269      | false ⇒ OK ? 〈Vfalse,tr1〉 ]
270  | Ecast ty' a ⇒
271      do 〈v,tr〉 ← exec_expr ge en m a;
272      do v' ← exec_cast m v (typeof a) ty';
273      OK ? 〈v',tr〉
274  | Ecost l a ⇒
275      do 〈v,tr〉 ← exec_expr ge en m a;
276      OK ? 〈v,tr⧺(Echarge l)〉
277  ]
278]
279and exec_lvalue' (ge:genv) (en:env) (m:mem) (e':expr_descr) (ty:type) on e' : res (region × block × int × trace) ≝
280  match e' with
281  [ Evar id ⇒
282      match (get … id en) with
283      [ None ⇒ do 〈sp,l〉 ← opt_to_res ? (find_symbol ? ? ge id); OK ? 〈〈〈sp,l〉,zero〉,E0〉 (* global *)
284      | Some loc ⇒ OK ? 〈〈〈Any,loc〉,zero〉,E0〉 (* local *)
285      ]
286  | Ederef a ⇒
287      do 〈v,tr〉 ← exec_expr ge en m a;
288      match v with
289      [ Vptr sp l ofs ⇒ OK ? 〈〈〈sp,l〉,ofs〉,tr〉
290      | _ ⇒ Error ?
291      ]
292  | Efield a i ⇒
293      match (typeof a) with
294      [ Tstruct id fList ⇒
295          do 〈plofs,tr〉 ← exec_lvalue ge en m a;
296          do delta ← field_offset i fList;
297          OK ? 〈〈\fst plofs,add (\snd plofs) (repr delta)〉,tr〉
298      | Tunion id fList ⇒
299          do 〈plofs,tr〉 ← exec_lvalue ge en m a;
300          OK ? 〈plofs,tr〉
301      | _ ⇒ Error ?
302      ]
303  | _ ⇒ Error ?
304  ]
305and exec_lvalue (ge:genv) (en:env) (m:mem) (e:expr) on e : res (region × block × int × trace) ≝
306match e with [ Expr e' ty ⇒ exec_lvalue' ge en m e' ty ].
307
308nlemma P_res_to_P: ∀A,P,e,v.  P_res A P e → e = OK A v → P v.
309#A P e v H1 H2; nrewrite > H2 in H1; nwhd in ⊢ (% → ?); //; nqed.
310
311(* We define a special induction principle tailored to the recursive definition
312   above. *)
313
314ndefinition is_not_lvalue: expr_descr → Prop ≝
315λe. match e with [ Evar _ ⇒ False | Ederef _ ⇒ False | Efield _ _ ⇒ False | _ ⇒ True ].
316
317ndefinition Plvalue ≝ λP:(expr → Prop).λe,ty.
318match e return λ_.Prop with [ Evar _ ⇒ P (Expr e ty) | Ederef _ ⇒ P (Expr e ty) | Efield _ _ ⇒ P (Expr e ty) | _ ⇒ True ].
319
320(* TODO: Can we do this sensibly with a map combinator? *)
321nlet rec exec_exprlist (ge:genv) (e:env) (m:mem) (l:list expr) on l : res (list val×trace) ≝
322match l with
323[ nil ⇒ OK ? 〈nil val, E0〉
324| cons e1 es ⇒
325  do 〈v,tr1〉 ← exec_expr ge e m e1;
326  do 〈vs,tr2〉 ← exec_exprlist ge e m es;
327  OK ? 〈cons val v vs, tr1⧺tr2〉
328].
329
330(* Don't really want to use subset rather than sigma here, but can't be bothered
331   with *another* set of coercions. XXX: why do I have to get the recursive
332   call's property manually? *)
333
334nlet 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) } ≝
335match l with
336[ nil ⇒ Some ? 〈en, m〉
337| cons h vars ⇒
338  match h with [ mk_pair id ty ⇒
339    match alloc m 0 (sizeof ty) Any with [ mk_pair m1 b1 ⇒
340      match exec_alloc_variables (set … id b1 en) m1 vars with
341      [ sig_intro r p ⇒ r ]
342]]]. nwhd;
343##[ //;
344##| nelim (exec_alloc_variables (set ident ? ? c3 c7 en) c6 c1);
345    #H; nelim H; //; #H0; nelim H0; nnormalize; #en' m' IH;
346napply (alloc_variables_cons … IH); /2/;
347nqed.
348
349(* TODO: can we establish that length params = length vs in advance? *)
350nlet 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) ≝
351  match params with
352  [ nil ⇒ match vs with [ nil ⇒ Some ? (OK ? m) | cons _ _ ⇒ Some ? (Error ?) ]
353  | cons idty params' ⇒ match idty with [ mk_pair id ty ⇒
354      match vs with
355      [ nil ⇒ Some ? (Error ?)
356      | cons v1 vl ⇒ Some ? (
357          do b ← opt_to_res ? (get … id e);
358          do m1 ← opt_to_res ? (store_value_of_type ty m Any b zero v1);
359          err_eject ?? (exec_bind_parameters e m1 params' vl)) (* FIXME: don't want to have to eject here *)
360      ]
361  ] ].
362nwhd; //;
363napply opt_bind_OK; #b eb;
364napply opt_bind_OK; #m1 em1;
365napply sig_bind_OK; #m2 Hm2;
366napply (bind_parameters_cons … eb em1 Hm2);
367nqed.
368
369alias id "Tint" = "cic:/matita/c-semantics/Csyntax/type.con(0,2,0)".
370alias id "Tfloat" = "cic:/matita/c-semantics/Csyntax/type.con(0,3,0)".
371ndefinition sz_eq_dec : ∀s1,s2:intsize. (s1 = s2) + (s1 ≠ s2).
372#s1; ncases s1; #s2; ncases s2; /2/; @2; @; #H; ndestruct; nqed.
373ndefinition sg_eq_dec : ∀s1,s2:signedness. (s1 = s2) + (s1 ≠ s2).
374#s1; ncases s1; #s2; ncases s2; /2/; @2; @; #H; ndestruct; nqed.
375ndefinition fs_eq_dec : ∀s1,s2:floatsize. (s1 = s2) + (s1 ≠ s2).
376#s1; ncases s1; #s2; ncases s2; /2/; @2; @; #H; ndestruct; nqed.
377
378nlet rec type_eq_dec (t1,t2:type) : (t1 = t2) + (t1 ≠ t2) ≝
379match t1 return λt'. (t' = t2) + (t' ≠ t2) with
380[ Tvoid ⇒ match t2 return λt'. (Tvoid = t') + (Tvoid ≠ t') with [ Tvoid ⇒ inl ?? (refl ??) | _ ⇒ inr ?? (nmk ? (λH.?)) ]
381| Tint sz sg ⇒ match t2 return λt'. (Tint ?? = t') + (Tint ?? ≠ t')  with [ Tint sz' sg' ⇒
382    match sz_eq_dec sz sz' with [ inl e1 ⇒
383    match sg_eq_dec sg sg' with [ inl e2 ⇒ inl ???
384    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
385    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
386    | _ ⇒ inr ?? (nmk ? (λH.?)) ]
387| Tfloat f ⇒ match t2 return λt'. (Tfloat ? = t') + (Tfloat ? ≠ t')  with [ Tfloat f' ⇒
388    match fs_eq_dec f f' with [ inl e1 ⇒ inl ???
389    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
390    | _ ⇒ inr ?? (nmk ? (λH.?)) ]
391| Tpointer s t ⇒ match t2 return λt'. (Tpointer ?? = t') + (Tpointer ?? ≠ t')  with [ Tpointer s' t' ⇒
392    match ms_eq_dec s s' with [ inl e1 ⇒
393      match type_eq_dec t t' with [ inl e2 ⇒ inl ???
394      | inr e2 ⇒ inr ?? (nmk ? (λH.match e2 with [ nmk e' ⇒ e' ? ])) ]
395    | inr e1 ⇒ inr ?? (nmk ? (λH.match e1 with [ nmk e' ⇒ e' ? ])) ] | _ ⇒ inr ?? (nmk ? (λH.?)) ]
396| Tarray s t n ⇒ match t2 return λt'. (Tarray ??? = t') + (Tarray ??? ≠ t')  with [ Tarray s' t' n' ⇒
397    match ms_eq_dec s s' with [ inl e1 ⇒
398      match type_eq_dec t t' with [ inl e2 ⇒
399        match decidable_eq_Z_Type n n' with [ inl e3 ⇒ inl ???
400        | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
401        | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
402        | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
403        | _ ⇒ inr ?? (nmk ? (λH.?)) ]
404| Tfunction tl t ⇒ match t2 return λt'. (Tfunction ?? = t') + (Tfunction ?? ≠ t')  with [ Tfunction tl' t' ⇒
405    match typelist_eq_dec tl tl' with [ inl e1 ⇒
406    match type_eq_dec t t' with [ inl e2 ⇒ inl ???
407    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
408    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
409  | _ ⇒ inr ?? (nmk ? (λH.?)) ]
410| Tstruct i fl ⇒
411    match t2 return λt'. (Tstruct ?? = t') + (Tstruct ?? ≠ t')  with [ Tstruct i' fl' ⇒
412    match ident_eq i i' with [ inl e1 ⇒
413    match fieldlist_eq_dec fl fl' with [ inl e2 ⇒ inl ???
414    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
415    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
416    | _ ⇒ inr ?? (nmk ? (λH.?)) ]
417| Tunion i fl ⇒
418    match t2 return λt'. (Tunion ?? = t') + (Tunion ?? ≠ t')  with [ Tunion i' fl' ⇒
419    match ident_eq i i' with [ inl e1 ⇒
420    match fieldlist_eq_dec fl fl' with [ inl e2 ⇒ inl ???
421    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
422    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
423    |  _ ⇒ inr ?? (nmk ? (λH.?)) ]
424| Tcomp_ptr r i ⇒ match t2 return λt'. (Tcomp_ptr ? ? = t') + (Tcomp_ptr ? ? ≠ t')  with [ Tcomp_ptr r' i' ⇒
425    match ms_eq_dec r r' with [ inl e1 ⇒
426      match ident_eq i i' with [ inl e2 ⇒ inl ???
427      | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
428    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
429    | _ ⇒ inr ?? (nmk ? (λH.?)) ]
430]
431and typelist_eq_dec (tl1,tl2:typelist) : (tl1 = tl2) + (tl1 ≠ tl2) ≝
432match tl1 return λtl'. (tl' = tl2) + (tl' ≠ tl2) with
433[ Tnil ⇒ match tl2 return λtl'. (Tnil = tl') + (Tnil ≠ tl') with [ Tnil ⇒ inl ?? (refl ??) | _ ⇒ inr ?? (nmk ? (λH.?)) ]
434| Tcons t1 ts1 ⇒ match tl2 return λtl'. (Tcons ?? = tl') + (Tcons ?? ≠ tl') with [ Tnil ⇒ inr ?? (nmk ? (λH.?)) | Tcons t2 ts2 ⇒
435    match type_eq_dec t1 t2 with [ inl e1 ⇒
436    match typelist_eq_dec ts1 ts2 with [ inl e2 ⇒ inl ???
437    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
438    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ] ]
439]
440and fieldlist_eq_dec (fl1,fl2:fieldlist) : (fl1 = fl2) + (fl1 ≠ fl2) ≝
441match fl1 return λfl'. (fl' = fl2) + (fl' ≠ fl2) with
442[ Fnil ⇒ match fl2 return λfl'. (Fnil = fl') + (Fnil ≠ fl') with [ Fnil ⇒ inl ?? (refl ??) | _ ⇒ inr ?? (nmk ? (λH.?)) ]
443| Fcons i1 t1 fs1 ⇒ match fl2 return λfl'. (Fcons ??? = fl') + (Fcons ??? ≠ fl') with [ Fnil ⇒ inr ?? (nmk ? (λH.?)) | Fcons i2 t2 fs2 ⇒
444    match ident_eq i1 i2 with [ inl e1 ⇒
445      match type_eq_dec t1 t2 with [ inl e2 ⇒
446        match fieldlist_eq_dec fs1 fs2 with [ inl e3 ⇒ inl ???
447        | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
448        | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
449        | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ] ]
450]. ndestruct; //; nqed.
451
452ndefinition assert_type_eq : ∀t1,t2:type. res (t1 = t2) ≝
453λt1,t2. match type_eq_dec t1 t2 with [ inl p ⇒ OK ? p | inr _ ⇒ Error ? ].
454
455nlet rec is_is_call_cont (k:cont) : (is_call_cont k) + (¬is_call_cont k) ≝
456match k return λk'.(is_call_cont k') + (¬is_call_cont k') with
457[ Kstop ⇒ ?
458| Kcall _ _ _ _ ⇒ ?
459| _ ⇒ ?
460].
461##[ ##1,8: @1; //
462##| ##*: @2; /2/
463##] nqed.
464
465ndefinition is_Sskip : ∀s:statement. (s = Sskip) + (s ≠ Sskip) ≝
466λs.match s return λs'.(s' = Sskip) + (s' ≠ Sskip) with
467[ Sskip ⇒ inl ?? (refl ??)
468| _ ⇒ inr ?? (nmk ? (λH.?))
469]. ndestruct;
470nqed.
471
472(* Checking types of values given to / received from an external function call. *)
473
474ndefinition eventval_type : ∀ty:typ. Type ≝
475λty. match ty with [ ASTint ⇒ int | ASTfloat ⇒ float ].
476
477ndefinition mk_eventval: ∀ty:typ. eventval_type ty → eventval ≝
478λty:typ. match ty return λty'.eventval_type ty' → eventval with [ ASTint ⇒ λv.EVint v | ASTfloat ⇒ λv.EVfloat v ].
479
480ndefinition mk_val: ∀ty:typ. eventval_type ty → val ≝
481λty:typ. match ty return λty'.eventval_type ty' → val with [ ASTint ⇒ λv.Vint v | ASTfloat ⇒ λv.Vfloat v ].
482
483nlemma mk_val_correct: ∀ty:typ. ∀v:eventval_type ty.
484  eventval_match (mk_eventval ty v) ty (mk_val ty v).
485#ty; ncases ty; nnormalize; //; nqed.
486
487ndefinition convert_eventval : ∀ev:eventval. ∀ty:typ. res (Σv:val. eventval_match ev ty v) ≝
488λev,ty.
489match ty with
490[ ASTint ⇒ match ev with [ EVint i ⇒ Some ? (OK ? (Vint i)) | _ ⇒ Some ? (Error ?) ]
491| ASTfloat ⇒ match ev with [ EVfloat f ⇒ Some ? (OK ? (Vfloat f)) | _ ⇒ Some ? (Error ?) ]
492| _ ⇒ Some ? (Error ?)
493]. nwhd; //; nqed.
494
495ndefinition check_eventval' : ∀v:val. ∀ty:typ. res (Σev:eventval. eventval_match ev ty v) ≝
496λv,ty.
497match ty with
498[ ASTint ⇒ match v with [ Vint i ⇒ Some ? (OK ? (EVint i)) | _ ⇒ Some ? (Error ?) ]
499| ASTfloat ⇒ match v with [ Vfloat f ⇒ Some ? (OK ? (EVfloat f)) | _ ⇒ Some ? (Error ?) ]
500| _ ⇒ Some ? (Error ?)
501]. nwhd; //; nqed.
502
503nlet rec check_eventval_list (vs: list val) (tys: list typ) : res (Σevs:list eventval. eventval_list_match evs tys vs) ≝
504match vs with
505[ nil ⇒ match tys with [ nil ⇒ Some ? (OK ? (nil ?)) | _ ⇒ Some ? (Error ?) ]
506| cons v vt ⇒
507  match tys with
508  [ nil ⇒ Some ? (Error ?)
509  | cons ty tyt ⇒ Some ? (
510    do ev ← check_eventval' v ty;
511    do evt ← check_eventval_list vt tyt;
512    OK ? ((sig_eject ?? ev)::evt))
513  ]
514]. nwhd; //;
515napply sig_bind_OK; #ev Hev;
516napply sig_bind_OK; #evt Hevt;
517nnormalize; /2/;
518nqed.
519
520(* IO monad *)
521
522(* Interactions are function calls that return a value and do not change
523   the rest of the Clight program's state. *)
524nrecord io_out : Type ≝
525{ io_function: ident
526; io_args: list eventval
527; io_in_typ: typ
528}.
529
530ndefinition io_in ≝ λo. eventval_type (io_in_typ o).
531
532ndefinition do_io : ident → list eventval → ∀t:typ. IO io_out io_in (eventval_type t) ≝
533λfn,args,t. Interact ??? (mk_io_out fn args t) (λres. Value ??? res).
534
535ndefinition ret: ∀T. T → (IO io_out io_in T) ≝
536λT,x.(Value ?? T x).
537
538(* execution *)
539
540ndefinition store_value_of_type' ≝
541λty,m,l,v.
542match l with [ mk_pair pl ofs ⇒
543  match pl with [ mk_pair pcl loc ⇒
544    store_value_of_type ty m pcl loc ofs v ] ].
545
546nlet rec exec_step (ge:genv) (st:state) on st : (IO io_out io_in (trace × state)) ≝
547match st with
548[ State f s k e m ⇒
549  match s with
550  [ Sassign a1 a2 ⇒
551    ! 〈l,tr1〉 ← exec_lvalue ge e m a1;
552    ! 〈v2,tr2〉 ← exec_expr ge e m a2;
553    ! m' ← store_value_of_type' (typeof a1) m l v2;
554    ret ? 〈tr1⧺tr2, State f Sskip k e m'〉
555  | Scall lhs a al ⇒
556    ! 〈vf,tr2〉 ← exec_expr ge e m a;
557    ! 〈vargs,tr3〉 ← exec_exprlist ge e m al;
558    ! fd ← find_funct ? ? ge vf;
559    ! p ← err_to_io … (assert_type_eq (type_of_fundef fd) (fun_typeof a));
560(* requires associativity of IOMonad, so rearrange it below
561    ! k' ← match lhs with
562         [ None ⇒ ret ? (Kcall (None ?) f e k)
563         | Some lhs' ⇒
564           ! locofs ← exec_lvalue ge e m lhs';
565           ret ? (Kcall (Some ? 〈sig_eject ?? locofs, typeof lhs'〉) f e k)
566         ];
567    ret ? 〈E0, Callstate fd vargs k' m〉)
568*)
569    match lhs with
570         [ None ⇒ ret ? 〈tr2⧺tr3, Callstate fd vargs (Kcall (None ?) f e k) m〉
571         | Some lhs' ⇒
572           ! 〈locofs,tr1〉 ← exec_lvalue ge e m lhs';
573           ret ? 〈tr1⧺tr2⧺tr3, Callstate fd vargs (Kcall (Some ? 〈locofs, typeof lhs'〉) f e k) m〉
574         ]
575  | Ssequence s1 s2 ⇒ ret ? 〈E0, State f s1 (Kseq s2 k) e m〉
576  | Sskip ⇒
577      match k with
578      [ Kseq s k' ⇒ ret ? 〈E0, State  f s k' e m〉
579      | Kstop ⇒
580          match fn_return f with
581          [ Tvoid ⇒ ret ? 〈E0, Returnstate Vundef k (free_list m (blocks_of_env e))〉
582          | _ ⇒ Wrong ???
583          ]
584      | Kcall _ _ _ _ ⇒
585          match fn_return f with
586          [ Tvoid ⇒ ret ? 〈E0, Returnstate Vundef k (free_list m (blocks_of_env e))〉
587          | _ ⇒ Wrong ???
588          ]
589      | Kwhile a s' k' ⇒ ret ? 〈E0, State f (Swhile a s') k' e m〉
590      | Kdowhile a s' k' ⇒
591          ! 〈v,tr〉 ← exec_expr ge e m a;
592          ! b ← err_to_io … (exec_bool_of_val v (typeof a));
593          match b with
594          [ true ⇒ ret ? 〈tr, State f (Sdowhile a s') k' e m〉
595          | false ⇒ ret ? 〈tr, State f Sskip k' e m〉
596          ]
597      | Kfor2 a2 a3 s' k' ⇒ ret ? 〈E0, State f a3 (Kfor3 a2 a3 s' k') e m〉
598      | Kfor3 a2 a3 s' k' ⇒ ret ? 〈E0, State f (Sfor Sskip a2 a3 s') k' e m〉
599      | Kswitch k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
600      | _ ⇒ Wrong ???
601      ]
602  | Scontinue ⇒
603      match k with
604      [ Kseq s' k' ⇒ ret ? 〈E0, State f Scontinue k' e m〉
605      | Kwhile a s' k' ⇒ ret ? 〈E0, State f (Swhile a s') k' e m〉
606      | Kdowhile a s' k' ⇒
607          ! 〈v,tr〉 ← exec_expr ge e m a;
608          ! b ← err_to_io … (exec_bool_of_val v (typeof a));
609          match b with
610          [ true ⇒ ret ? 〈tr, State f (Sdowhile a s') k' e m〉
611          | false ⇒ ret ? 〈tr, State f Sskip k' e m〉
612          ]
613      | Kfor2 a2 a3 s' k' ⇒ ret ? 〈E0, State f a3 (Kfor3 a2 a3 s' k') e m〉
614      | Kswitch k' ⇒ ret ? 〈E0, State f Scontinue k' e m〉
615      | _ ⇒ Wrong ???
616      ]
617  | Sbreak ⇒
618      match k with
619      [ Kseq s' k' ⇒ ret ? 〈E0, State f Sbreak k' e m〉
620      | Kwhile a s' k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
621      | Kdowhile a s' k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
622      | Kfor2 a2 a3 s' k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
623      | Kswitch k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
624      | _ ⇒ Wrong ???
625      ]
626  | Sifthenelse a s1 s2 ⇒
627      ! 〈v,tr〉 ← exec_expr ge e m a;
628      ! b ← err_to_io … (exec_bool_of_val v (typeof a));
629      ret ? 〈tr, State f (if b then s1 else s2) k e m〉
630  | Swhile a s' ⇒
631      ! 〈v,tr〉 ← exec_expr ge e m a;
632      ! b ← err_to_io … (exec_bool_of_val v (typeof a));
633      ret ? 〈tr, if b then State f s' (Kwhile a s' k) e m
634                      else State f Sskip k e m〉
635  | Sdowhile a s' ⇒ ret ? 〈E0, State f s' (Kdowhile a s' k) e m〉
636  | Sfor a1 a2 a3 s' ⇒
637      match is_Sskip a1 with
638      [ inl _ ⇒
639          ! 〈v,tr〉 ← exec_expr ge e m a2;
640          ! b ← err_to_io … (exec_bool_of_val v (typeof a2));
641          ret ? 〈tr, State f (if b then s' else Sskip) (if b then (Kfor2 a2 a3 s' k) else k) e m〉
642      | inr _ ⇒ ret ? 〈E0, State f a1 (Kseq (Sfor Sskip a2 a3 s') k) e m〉
643      ]
644  | Sreturn a_opt ⇒
645    match a_opt with
646    [ None ⇒ match fn_return f with
647      [ Tvoid ⇒ ret ? 〈E0, Returnstate Vundef (call_cont k) (free_list m (blocks_of_env e))〉
648      | _ ⇒ Wrong ???
649      ]
650    | Some a ⇒
651        match type_eq_dec (fn_return f) Tvoid with
652        [ inl _ ⇒ Wrong ???
653        | inr _ ⇒
654          ! 〈v,tr〉 ← exec_expr ge e m a;
655          ret ? 〈tr, Returnstate v (call_cont k) (free_list m (blocks_of_env e))〉
656        ]
657    ]
658  | Sswitch a sl ⇒
659      ! 〈v,tr〉 ← exec_expr ge e m a;
660      match v with [ Vint n ⇒ ret ? 〈tr, State f (seq_of_labeled_statement (select_switch n sl)) (Kswitch k) e m〉
661                   | _ ⇒ Wrong ??? ]
662  | Slabel lbl s' ⇒ ret ? 〈E0, State f s' k e m〉
663  | Sgoto lbl ⇒
664      match find_label lbl (fn_body f) (call_cont k) with
665      [ Some sk' ⇒ match sk' with [ mk_pair s' k' ⇒ ret ? 〈E0, State f s' k' e m〉 ]
666      | None ⇒ Wrong ???
667      ]
668  | Scost lbl s' ⇒ ret ? 〈Echarge lbl, State f s' k e m〉
669  ]
670| Callstate f0 vargs k m ⇒
671  match f0 with
672  [ Internal f ⇒
673    match exec_alloc_variables empty_env m ((fn_params f) @ (fn_vars f)) with [ mk_pair e m1 ⇒
674      ! m2 ← err_to_io_sig … (exec_bind_parameters e m1 (fn_params f) vargs);
675      ret ? 〈E0, State f (fn_body f) k e m2〉
676    ]
677  | External f argtys retty ⇒
678      ! evargs ← err_to_io_sig … (check_eventval_list vargs (typlist_of_typelist argtys));
679      ! evres ← do_io f evargs (proj_sig_res (signature_of_type argtys retty));
680      ret ? 〈Eextcall f evargs (mk_eventval ? evres), Returnstate (mk_val ? evres) k m〉
681  ]
682| Returnstate res k m ⇒
683  match k with
684  [ Kcall r f e k' ⇒
685    match r with
686    [ None ⇒ ret ? 〈E0, (State f Sskip k' e m)〉
687    | Some r' ⇒
688      match r' with [ mk_pair l ty ⇒
689       
690          ! m' ← store_value_of_type' ty m l res;
691          ret ? 〈E0, (State f Sskip k' e m')〉
692      ]
693    ]
694  | _ ⇒ Wrong ???
695  ]
696].
697
698nlet rec make_initial_state (p:clight_program) : res state ≝
699  let ge ≝ globalenv Genv ?? p in
700  let m0 ≝ init_mem Genv ?? p in
701    do 〈sp,b〉 ← opt_to_res ? (find_symbol ? ? ge (prog_main ?? p));
702    do u ← opt_to_res ? (match ms_eq_dec sp Code with [ inl _ ⇒ Some ? something | inr _ ⇒ None ? ]);
703    do f ← opt_to_res ? (find_funct_ptr ? ? ge b);
704    OK ? (Callstate f (nil ?) Kstop m0).
705
706ndefinition is_final_state : ∀st:state. (Σr. final_state st r) + (¬∃r. final_state st r).
707#st; nelim st;
708##[ #f s k e m; @2; @;*; #r H; ninversion H; #i m e; ndestruct;
709##| #f l k m; @2; @;*; #r H; ninversion H; #i m e; ndestruct;
710##| #v k m; ncases k;
711  ##[ ncases v;
712    ##[ ##2: #i; @1; @ i; //;
713    ##| ##1: @2; @; *;   #r H; ninversion H; #i m e; ndestruct;
714    ##| #f; @2; @; *;   #r H; ninversion H; #i m e; ndestruct;
715    ##| #pcl b of; @2; @; *;   #r H; ninversion H; #i m e; ndestruct;
716    ##]
717  ##| #a b; @2; @; *; #r H; ninversion H; #i m e; ndestruct;
718  ##| ##3,4: #a b c; @2; @; *; #r H; ninversion H; #i m e; ndestruct;
719  ##| ##5,6,8: #a b c d; @2; @; *; #r H; ninversion H; #i m e; ndestruct;
720  ##| #a; @2; @; *; #r H; ninversion H; #i m e; ndestruct;
721  ##]
722##] nqed.
723
724nlet rec exec_steps (n:nat) (ge:genv) (s:state) :
725 IO io_out io_in (trace×state) ≝
726match is_final_state s with
727[ inl _ ⇒ ret ? 〈E0, s〉
728| inr _ ⇒
729  match n with
730  [ O ⇒ ret ? 〈E0, s〉
731  | S n' ⇒
732      ! 〈t,s'〉 ← exec_step ge s;
733(*      ! 〈t,s'〉 ← match s with
734                 [ 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)) ]
735                 | 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)) ]
736                 | Returnstate r k m ⇒ match m with [ mk_mem c n p ⇒ exec_step ge (Returnstate r k (mk_mem c n p)) ]
737                 ] ;*)
738      ! 〈t',s''〉 ← match s' with
739                 [ 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)) ]
740                 | 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)) ]
741                 | Returnstate r k m ⇒ match m with [ mk_mem c n p ⇒ exec_steps n' ge (Returnstate r k (mk_mem c n p)) ]
742                 ] ;
743(*      ! 〈t',s''〉 ← exec_steps n' ge s';*)
744      ret ? 〈t ⧺ t',s''〉
745  ]
746].
747
748(* A (possibly non-terminating) execution.   *)
749ncoinductive execution : Type ≝
750| e_stop : trace → int → mem → execution
751| e_step : trace → state → execution → execution
752| e_wrong : execution
753| e_interact : ∀o:io_out. (io_in o → execution) → execution.
754
755ndefinition mem_of_state : state → mem ≝
756λs.match s with [ State f s k e m ⇒ m | Callstate f a k m ⇒ m | Returnstate r k m ⇒ m ].
757
758(* This definition is slightly awkward because of the need to provide resumptions.
759   It records the last trace/state passed in, then recursively processes the next
760   state. *)
761
762nlet corec exec_inf_aux (ge:genv) (s:IO io_out io_in (trace×state)) : execution ≝
763match s with
764[ Wrong ⇒ e_wrong
765| Value v ⇒ match v with [ mk_pair t s' ⇒
766    match is_final_state s' with
767    [ inl r ⇒ e_stop t (sig_eject … r) (mem_of_state s')
768    | inr _ ⇒ e_step t s' (exec_inf_aux ge (exec_step ge s')) ] ]
769| Interact out k' ⇒ e_interact out (λv. exec_inf_aux ge (k' v))
770].
771
772
773ndefinition exec_inf : clight_program → execution ≝
774λp. exec_inf_aux (globalenv Genv ?? p) (! s ← make_initial_state p; ret ? 〈E0,s〉).
775
776nremark execution_cases: ∀e.
777 e = match e with [ e_stop tr r m ⇒ e_stop tr r m | e_step tr s e ⇒ e_step tr s e
778 | e_wrong ⇒ e_wrong | e_interact o k ⇒ e_interact o k ].
779#e; ncases e; //; nqed.
780
781nlemma exec_inf_aux_unfold: ∀ge,s. exec_inf_aux ge s =
782match s with
783[ Wrong ⇒ e_wrong
784| Value v ⇒ match v with [ mk_pair t s' ⇒
785    match is_final_state s' with
786    [ inl r ⇒ e_stop t (sig_eject … r) (mem_of_state s')
787    | inr _ ⇒ e_step t s' (exec_inf_aux ge (exec_step ge s')) ] ]
788| Interact out k' ⇒ e_interact out (λv. exec_inf_aux ge (k' v))
789].
790#ge s; nrewrite > (execution_cases (exec_inf_aux …)); ncases s;
791##[ #o k
792##| #x; ncases x; #tr s'; ncases s';
793  ##[ #fn st k env m
794  ##| #fd args k mem
795  ##| #v k mem; (* for final state check *) ncases k;
796    ##[ ncases v; ##[ ##2,3: #v' ##| ##4: #sp loc off ##]
797    ##| #s' k' ##| ##3,4: #e s' k' ##| ##5,6: #e s' s'' k' ##| #k' ##| #a b c d ##]
798  ##]
799##| ##]
800nwhd in ⊢ (??%%); //;
801nqed.
802
Note: See TracBrowser for help on using the repository browser.