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

Last change on this file since 502 was 500, checked in by campbell, 10 years ago

Use dependent pointer type to ensure that the representation is always
compatible with the memory region used.
Add a couple of missing checks as a result...

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