[639] | 1 | |
---|
| 2 | (* XXX NB: I haven't checked all of these semantics against the prototype |
---|
| 3 | compilers yet! *) |
---|
| 4 | |
---|
[766] | 5 | include "utilities/lists.ma". |
---|
| 6 | |
---|
[702] | 7 | include "common/Errors.ma". |
---|
| 8 | include "common/Globalenvs.ma". |
---|
[731] | 9 | include "common/IO.ma". |
---|
[702] | 10 | include "common/SmallstepExec.ma". |
---|
[639] | 11 | |
---|
[762] | 12 | include "RTLabs/syntax.ma". |
---|
[751] | 13 | |
---|
[639] | 14 | definition genv ≝ (genv_t Genv) (fundef internal_function). |
---|
| 15 | |
---|
| 16 | record frame : Type[0] ≝ |
---|
[693] | 17 | { func : internal_function |
---|
[750] | 18 | ; locals : register_env val |
---|
[639] | 19 | ; next : label |
---|
[1535] | 20 | ; next_ok: present ?? (f_graph func) next |
---|
[639] | 21 | ; sp : block |
---|
[750] | 22 | ; retdst : option register |
---|
[639] | 23 | }. |
---|
| 24 | |
---|
[1535] | 25 | definition adv : ∀l:label. ∀f:frame. present ?? (f_graph (func f)) l → frame ≝ |
---|
| 26 | λl,f,p. mk_frame (func f) (locals f) l p (sp f) (retdst f). |
---|
[639] | 27 | |
---|
| 28 | inductive state : Type[0] ≝ |
---|
[693] | 29 | | State : |
---|
| 30 | ∀ f : frame. |
---|
| 31 | ∀ fs : list frame. |
---|
| 32 | ∀ m : mem. |
---|
| 33 | state |
---|
[639] | 34 | | Callstate : |
---|
| 35 | ∀ fd : fundef internal_function. |
---|
| 36 | ∀args : list val. |
---|
[750] | 37 | ∀ dst : option register. |
---|
[639] | 38 | ∀ stk : list frame. |
---|
| 39 | ∀ m : mem. |
---|
| 40 | state |
---|
| 41 | | Returnstate : |
---|
[765] | 42 | ∀ rtv : option val. |
---|
[750] | 43 | ∀ dst : option register. |
---|
[639] | 44 | ∀ stk : list frame. |
---|
| 45 | ∀ m : mem. |
---|
| 46 | state. |
---|
| 47 | |
---|
[693] | 48 | definition mem_of_state : state → mem ≝ |
---|
| 49 | λs. match s with [ State _ _ m ⇒ m | Callstate _ _ _ _ m ⇒ m | Returnstate _ _ _ m ⇒ m ]. |
---|
| 50 | |
---|
[1535] | 51 | definition build_state ≝ λf.λfs.λm.λn.λp. State (adv n f p) fs m. |
---|
[639] | 52 | |
---|
[887] | 53 | definition init_locals : list (register × typ) → register_env val ≝ |
---|
| 54 | foldr ?? (λidt,en. let 〈id,ty〉 ≝ idt in add RegisterTag val en id Vundef) (empty_map ??). |
---|
[761] | 55 | |
---|
[639] | 56 | definition reg_store ≝ |
---|
[750] | 57 | λreg,v,locals. |
---|
[761] | 58 | update RegisterTag val locals reg v. |
---|
[639] | 59 | |
---|
[797] | 60 | axiom WrongNumberOfParameters : String. |
---|
| 61 | |
---|
[887] | 62 | let rec params_store (rs:list (register × typ)) (vs:list val) (locals : register_env val) : res (register_env val) ≝ |
---|
[639] | 63 | match rs with |
---|
[797] | 64 | [ nil ⇒ match vs with [ nil ⇒ OK ? locals | _ ⇒ Error ? (msg WrongNumberOfParameters)] |
---|
[887] | 65 | | cons rt rst ⇒ match vs with [ nil ⇒ Error ? (msg WrongNumberOfParameters) | cons v vst ⇒ |
---|
| 66 | let 〈r,ty〉 ≝ rt in |
---|
[761] | 67 | let locals' ≝ add RegisterTag val locals r v in |
---|
[639] | 68 | params_store rst vst locals' |
---|
| 69 | ] ]. |
---|
| 70 | |
---|
[797] | 71 | axiom BadRegister : String. |
---|
| 72 | |
---|
[750] | 73 | definition reg_retrieve : register_env ? → register → res val ≝ |
---|
[797] | 74 | λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup ?? locals reg). |
---|
[639] | 75 | |
---|
[797] | 76 | axiom FailedOp : String. |
---|
| 77 | axiom MissingSymbol : String. |
---|
| 78 | |
---|
| 79 | axiom MissingStatement : String. |
---|
| 80 | axiom FailedConstant : String. |
---|
| 81 | axiom FailedLoad : String. |
---|
| 82 | axiom FailedStore : String. |
---|
| 83 | axiom BadFunction : String. |
---|
| 84 | axiom BadJumpTable : String. |
---|
| 85 | axiom BadJumpValue : String. |
---|
| 86 | axiom FinalState : String. |
---|
| 87 | axiom ReturnMismatch : String. |
---|
[639] | 88 | |
---|
[693] | 89 | definition eval_statement : genv → state → IO io_out io_in (trace × state) ≝ |
---|
| 90 | λge,st. |
---|
[639] | 91 | match st with |
---|
| 92 | [ State f fs m ⇒ |
---|
[1535] | 93 | let s ≝ lookup_present ?? (f_graph (func f)) (next f) (next_ok f) in |
---|
| 94 | match s return λs. labels_present ? s → ? with |
---|
| 95 | [ St_skip l ⇒ λH. ret ? 〈E0, build_state f fs m l ?〉 |
---|
| 96 | | St_cost cl l ⇒ λH. ret ? 〈Echarge cl, build_state f fs m l ?〉 |
---|
| 97 | | St_const r cst l ⇒ λH. |
---|
[797] | 98 | ! v ← opt_to_res … (msg FailedConstant) (eval_constant (find_symbol … ge) (sp f) cst); |
---|
[750] | 99 | ! locals ← reg_store r v (locals f); |
---|
[1535] | 100 | ret ? 〈E0, State (mk_frame (func f) locals l ? (sp f) (retdst f)) fs m〉 |
---|
| 101 | | St_op1 _ _ op dst src l ⇒ λH. |
---|
[639] | 102 | ! v ← reg_retrieve (locals f) src; |
---|
[1369] | 103 | ! v' ← opt_to_res … (msg FailedOp) (eval_unop ?? op v); |
---|
[639] | 104 | ! locals ← reg_store dst v' (locals f); |
---|
[1535] | 105 | ret ? 〈E0, State (mk_frame (func f) locals l ? (sp f) (retdst f)) fs m〉 |
---|
| 106 | | St_op2 op dst src1 src2 l ⇒ λH. |
---|
[639] | 107 | ! v1 ← reg_retrieve (locals f) src1; |
---|
| 108 | ! v2 ← reg_retrieve (locals f) src2; |
---|
[797] | 109 | ! v' ← opt_to_res … (msg FailedOp) (eval_binop op v1 v2); |
---|
[639] | 110 | ! locals ← reg_store dst v' (locals f); |
---|
[1535] | 111 | ret ? 〈E0, State (mk_frame (func f) locals l ? (sp f) (retdst f)) fs m〉 |
---|
| 112 | | St_load chunk addr dst l ⇒ λH. |
---|
[887] | 113 | ! vaddr ← reg_retrieve (locals f) addr; |
---|
[797] | 114 | ! v ← opt_to_res … (msg FailedLoad) (loadv chunk m vaddr); |
---|
[639] | 115 | ! locals ← reg_store dst v (locals f); |
---|
[1535] | 116 | ret ? 〈E0, State (mk_frame (func f) locals l ? (sp f) (retdst f)) fs m〉 |
---|
| 117 | | St_store chunk addr src l ⇒ λH. |
---|
[887] | 118 | ! vaddr ← reg_retrieve (locals f) addr; |
---|
[639] | 119 | ! v ← reg_retrieve (locals f) src; |
---|
[797] | 120 | ! m' ← opt_to_res … (msg FailedStore) (storev chunk m vaddr v); |
---|
[1535] | 121 | ret ? 〈E0, build_state f fs m' l ?〉 |
---|
| 122 | | St_call_id id args dst l ⇒ λH. |
---|
[797] | 123 | ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id); |
---|
| 124 | ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b); |
---|
[639] | 125 | ! vs ← mmap ?? (reg_retrieve (locals f)) args; |
---|
[1535] | 126 | ret ? 〈E0, Callstate fd vs dst (adv l f ?::fs) m〉 |
---|
| 127 | | St_call_ptr frs args dst l ⇒ λH. |
---|
[639] | 128 | ! fv ← reg_retrieve (locals f) frs; |
---|
[797] | 129 | ! fd ← opt_to_res … (msg BadFunction) (find_funct ?? ge fv); |
---|
[639] | 130 | ! vs ← mmap ?? (reg_retrieve (locals f)) args; |
---|
[1535] | 131 | ret ? 〈E0, Callstate fd vs dst (adv l f ?::fs) m〉 |
---|
| 132 | | St_tailcall_id id args ⇒ λH. |
---|
[797] | 133 | ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id); |
---|
| 134 | ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b); |
---|
[639] | 135 | ! vs ← mmap ?? (reg_retrieve (locals f)) args; |
---|
| 136 | ret ? 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉 |
---|
[1535] | 137 | | St_tailcall_ptr frs args ⇒ λH. |
---|
[639] | 138 | ! fv ← reg_retrieve (locals f) frs; |
---|
[797] | 139 | ! fd ← opt_to_res … (msg BadFunction) (find_funct ?? ge fv); |
---|
[639] | 140 | ! vs ← mmap ?? (reg_retrieve (locals f)) args; |
---|
| 141 | ret ? 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉 |
---|
| 142 | |
---|
[1535] | 143 | | St_cond src ltrue lfalse ⇒ λH. |
---|
[888] | 144 | ! v ← reg_retrieve (locals f) src; |
---|
[751] | 145 | ! b ← eval_bool_of_val v; |
---|
[1535] | 146 | ret ? 〈E0, build_state f fs m (if b then ltrue else lfalse) ?〉 |
---|
[639] | 147 | |
---|
[1535] | 148 | | St_jumptable r ls ⇒ λH. |
---|
[750] | 149 | ! v ← reg_retrieve (locals f) r; |
---|
[639] | 150 | match v with |
---|
[961] | 151 | [ Vint _ i ⇒ |
---|
[1535] | 152 | match nth_opt ? (nat_of_bitvector ? i) ls return λx. nth_opt ??? = x → ? with |
---|
| 153 | [ None ⇒ λ_. Wrong ??? (msg BadJumpTable) |
---|
| 154 | | Some l ⇒ λE. ret ? 〈E0, build_state f fs m l ?〉 |
---|
| 155 | ] (refl ??) |
---|
[797] | 156 | | _ ⇒ Wrong ??? (msg BadJumpValue) |
---|
[639] | 157 | ] |
---|
| 158 | |
---|
[1535] | 159 | | St_return ⇒ λH. |
---|
[765] | 160 | ! v ← match f_result (func f) with |
---|
| 161 | [ None ⇒ ret ? (None ?) |
---|
[887] | 162 | | Some rt ⇒ |
---|
| 163 | let 〈r,ty〉 ≝ rt in |
---|
| 164 | ! v ← reg_retrieve (locals f) r; |
---|
| 165 | ret ? (Some ? v) |
---|
[765] | 166 | ]; |
---|
[639] | 167 | ret ? 〈E0, Returnstate v (retdst f) fs (free m (sp f))〉 |
---|
[1535] | 168 | ] (f_closed (func f) (next f) s ?) |
---|
[639] | 169 | | Callstate fd params dst fs m ⇒ |
---|
| 170 | match fd with |
---|
| 171 | [ Internal fn ⇒ |
---|
[761] | 172 | ! locals ← params_store (f_params fn) params (init_locals (f_locals fn)); |
---|
[1123] | 173 | (* CSC: XXX alignment call (concrete_stacksize in OCaml) is missing |
---|
| 174 | here *) |
---|
[639] | 175 | let 〈m', sp〉 ≝ alloc m 0 (f_stacksize fn) Any in |
---|
[1535] | 176 | ret ? 〈E0, State (mk_frame fn locals (f_entry fn) ? sp dst) fs m'〉 |
---|
[639] | 177 | | External fn ⇒ |
---|
| 178 | ! evargs ← check_eventval_list params (sig_args (ef_sig fn)); |
---|
[879] | 179 | ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn)); |
---|
[765] | 180 | ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), Returnstate (Some ? (mk_val ? evres) (*FIXME should allow None *)) dst fs m〉 |
---|
[639] | 181 | ] |
---|
| 182 | | Returnstate v dst fs m ⇒ |
---|
| 183 | match fs with |
---|
[797] | 184 | [ nil ⇒ Error ? (msg FinalState) (* Already in final state *) |
---|
[639] | 185 | | cons f fs' ⇒ |
---|
[765] | 186 | ! locals ← match dst with |
---|
| 187 | [ None ⇒ match v with [ None ⇒ OK ? (locals f) |
---|
[797] | 188 | | _ ⇒ Error ? (msg ReturnMismatch) ] |
---|
| 189 | | Some d ⇒ match v with [ None ⇒ Error ? (msg ReturnMismatch) |
---|
[765] | 190 | | Some v' ⇒ reg_store d v' (locals f) ] ]; |
---|
[1535] | 191 | ret ? 〈E0, State (mk_frame (func f) locals (next f) ? (sp f) (retdst f)) fs' m〉 |
---|
[639] | 192 | ] |
---|
[1535] | 193 | ]. try @(next_ok f) try @lookup_lookup_present try @H |
---|
| 194 | [ cases b [ @(proj1 ?? H) | @(proj2 ?? H) ] |
---|
| 195 | | whd in H; @(All_nth … H ? E) |
---|
| 196 | | cases (f_entry fn) // |
---|
| 197 | ] qed. |
---|
[693] | 198 | |
---|
[1559] | 199 | definition RTLabs_is_final : state → option int ≝ |
---|
[693] | 200 | λs. match s with |
---|
| 201 | [ State _ _ _ ⇒ None ? |
---|
| 202 | | Callstate _ _ _ _ _ ⇒ None ? |
---|
| 203 | | Returnstate v _ fs _ ⇒ |
---|
[961] | 204 | match fs with [ nil ⇒ |
---|
| 205 | match v with [ Some v' ⇒ |
---|
| 206 | match v' with |
---|
| 207 | [ Vint sz i ⇒ intsize_eq_elim ? sz I32 ? i (λi. Some ? i) (None ?) |
---|
| 208 | | _ ⇒ None ? ] |
---|
| 209 | | None ⇒ None ? ] |
---|
| 210 | | cons _ _ ⇒ None ? ] |
---|
[693] | 211 | ]. |
---|
| 212 | |
---|
[1238] | 213 | definition RTLabs_exec : trans_system io_out io_in ≝ |
---|
[1559] | 214 | mk_trans_system … ? (λ_.RTLabs_is_final) eval_statement. |
---|
[702] | 215 | |
---|
[1238] | 216 | definition make_global : RTLabs_program → genv ≝ |
---|
| 217 | λp. globalenv Genv ?? (λx.[Init_space x]) p. |
---|
| 218 | |
---|
| 219 | definition make_initial_state : RTLabs_program → res state ≝ |
---|
[702] | 220 | λp. |
---|
[1238] | 221 | let ge ≝ make_global p in |
---|
[1139] | 222 | do m ← init_mem Genv ?? (λx.[Init_space x]) p; |
---|
[797] | 223 | let main ≝ prog_main ?? p in |
---|
| 224 | do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol ? ? ge main); |
---|
| 225 | do f ← opt_to_res ? [MSG BadFunction; CTX ? main] (find_funct_ptr ? ? ge b); |
---|
[1238] | 226 | OK ? (Callstate f (nil ?) (None ?) (nil ?) m). |
---|
[702] | 227 | |
---|
[731] | 228 | definition RTLabs_fullexec : fullexec io_out io_in ≝ |
---|
[1238] | 229 | mk_fullexec … RTLabs_exec make_global make_initial_state. |
---|
[731] | 230 | |
---|
[1583] | 231 | |
---|
| 232 | (* Some lemmas about the semantics. *) |
---|
| 233 | |
---|
| 234 | (* Note parts of frames and states that are preserved. *) |
---|
| 235 | |
---|
| 236 | inductive frame_rel : frame → frame → Prop ≝ |
---|
| 237 | | mk_frame_rel : |
---|
| 238 | ∀func,locals,next,next_ok,sp,retdst,locals',next',next_ok'. frame_rel |
---|
| 239 | (mk_frame func locals next next_ok sp retdst) |
---|
| 240 | (mk_frame func locals' next' next_ok' sp retdst) |
---|
| 241 | . |
---|
| 242 | |
---|
| 243 | inductive state_rel : genv → state → state → Prop ≝ |
---|
| 244 | | normal : ∀ge,f,f',fs,m,m'. frame_rel f f' → state_rel ge (State f fs m) (State f' fs m') |
---|
| 245 | | to_call : ∀ge,f,fs,m,fd,args,f',dst. frame_rel f f' → ∀b. find_funct_ptr ?? ge b = Some ? fd → state_rel ge (State f fs m) (Callstate fd args dst (f'::fs) m) |
---|
| 246 | | tail_call : ∀ge,f,fs,m,fd,args,dst,m'. ∀b. find_funct_ptr ?? ge b = Some ? fd → state_rel ge (State f fs m) (Callstate fd args dst fs m') |
---|
| 247 | | from_call : ∀ge,fn,locals,next,nok,sp,fs,m,args,dst,m'. state_rel ge (Callstate (Internal ? fn) args dst fs m) (State (mk_frame fn locals next nok sp dst) fs m') |
---|
| 248 | | to_ret : ∀ge,f,fs,m,rtv,dst,m'. state_rel ge (State f fs m) (Returnstate rtv dst fs m') |
---|
| 249 | | from_ret : ∀ge,f,fs,rtv,dst,f',m. frame_rel f f' → state_rel ge (Returnstate rtv dst (f::fs) m) (State f' fs m) |
---|
| 250 | . |
---|
| 251 | |
---|
| 252 | lemma bindIO_value : ∀O,I,A,B,e,f,v. ∀P:B → Prop. |
---|
| 253 | (∀a. e = Value ??? a → f a = Value ??? v → P v) → |
---|
| 254 | (bindIO O I A B e f = Value ??? v → P v). |
---|
| 255 | #O #I #A #B * |
---|
| 256 | [ #o #k #f #v #P #H #E whd in E:(??%?); destruct |
---|
| 257 | | #a #f #v #P #H #E @H [ @a | @refl | @E ] |
---|
| 258 | | #m #f #v #P #H #E whd in E:(??%?); destruct |
---|
| 259 | ] qed. |
---|
| 260 | |
---|
| 261 | lemma eval_perserves : ∀ge,s,tr,s'. |
---|
| 262 | eval_statement ge s = Value ??? 〈tr,s'〉 → |
---|
| 263 | state_rel ge s s'. |
---|
| 264 | #ge * |
---|
| 265 | [ * #func #locals #next #next_ok #sp #retdst #fs #m |
---|
| 266 | #tr #s' |
---|
| 267 | whd in ⊢ (??%? → ?); |
---|
| 268 | generalize in ⊢ (??(?%)? → ?); |
---|
| 269 | cases (lookup_present LabelTag statement (f_graph func) next next_ok) |
---|
| 270 | [ #l #LP whd in ⊢ (??%? → ?); #E destruct % % |
---|
| 271 | | #c #l #LP whd in ⊢ (??%? → ?); #E destruct % % |
---|
| 272 | | #r #c #l #LP whd in ⊢ (??%? → ?); @bindIO_value #v #Ev @bindIO_value #locals' #Eloc #E whd in E:(??%?); destruct % % |
---|
| 273 | | #t1 #t2 #op #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bindIO_value #v #Ev @bindIO_value #v' #Ev' @bindIO_value #loc #Eloc #E whd in E:(??%?); destruct % % |
---|
| 274 | | #op #r1 #r2 #r3 #l #LP whd in ⊢ (??%? → ?); @bindIO_value #v1 #Ev1 @bindIO_value #v2 #Ev2 @bindIO_value #v' #Ev' @bindIO_value #loc #Eloc #E whd in E:(??%?); destruct % % |
---|
| 275 | | #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bindIO_value #v #Ev @bindIO_value #v' #Ev' @bindIO_value #loc #Eloc #E whd in E:(??%?); destruct % % |
---|
| 276 | | #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bindIO_value #v #Ev @bindIO_value #v' #Ev' @bindIO_value #loc #Eloc #E whd in E:(??%?); destruct % % |
---|
| 277 | | #id #rs #or #l #LP whd in ⊢ (??%? → ?); @bindIO_value #b #Eb @bindIO_value #fd #Efd @bindIO_value #vs #Evs #E whd in E:(??%?); destruct %2 [ % | @b | cases (find_funct_ptr ????) in Efd ⊢ %; normalize [2:#fd'] #E' destruct @refl ] |
---|
| 278 | | #r #rs #or #l #LP whd in ⊢ (??%? → ?); @bindIO_value #v #Ev @bindIO_value #fd #Efd @bindIO_value #vs #Evs #E whd in E:(??%?); destruct cases (find_funct_find_funct_ptr ?? v ??) [ #r * #b * #c * #Ev' #Efn %2 [ % | @b | @Efn ] | ||| cases (find_funct ????) in Efd ⊢ %; [2:#x] normalize #E' destruct @refl ] |
---|
| 279 | | #id #rs #LP whd in ⊢ (??%? → ?); @bindIO_value #b #Eb @bindIO_value #fd #Efd @bindIO_value #vs #Evs #E whd in E:(??%?); destruct %3 [ @b | cases (find_funct_ptr ????) in Efd ⊢ %; [2:#x] normalize #E' destruct @refl ] |
---|
| 280 | | #r #rs #LP whd in ⊢ (??%? → ?); @bindIO_value #v #Ev @bindIO_value #fd #Efd @bindIO_value #vs #Evs #E whd in E:(??%?); destruct cases (find_funct_find_funct_ptr ?? v ??) [ #r * #b * #c * #Ev' #Efn %3 [ @b | @Efn ] | ||| cases (find_funct ????) in Efd ⊢ %; [2:#x] normalize #E' destruct @refl ] |
---|
| 281 | | #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bindIO_value #v #Ev @bindIO_value #b #Eb #E whd in E:(??%?); destruct % % |
---|
| 282 | | #r #ls #LP whd in ⊢ (??%? → ?); @bindIO_value #v #Ev cases v [ #E whd in E:(??%?); destruct | #sz #i whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?); cases (nth_opt ?? ls) in ⊢ (∀e:???%. ??(match % with [_ ⇒ ?|_ ⇒ ?]?)? → ?); [ #e #E whd in E:(??%?); destruct | #l' #e #E whd in E:(??%?); destruct % % ] | *: #vl #E whd in E:(??%?); destruct ] |
---|
| 283 | | #LP whd in ⊢ (??%? → ?); @bindIO_value #v cases (f_result func) [ 2: * #r #t whd in ⊢ (??%? → ?); @bindIO_value #v0 #Ev0 ] #E whd in E:(??%?); #E' whd in E':(??%?); destruct %5 |
---|
| 284 | ] |
---|
| 285 | | * #fn #args #retdst #stk #m #tr #s' |
---|
| 286 | whd in ⊢ (??%? → ?); |
---|
| 287 | [ @bindIO_value #loc #Eloc cases (alloc m O ??) #m' #b whd in ⊢ (??%? → ?); |
---|
| 288 | #E destruct %4 |
---|
| 289 | | @bindIO_value #evargs #Eargs @bindIO_value #evres #Eres whd in Eres:(??%?); |
---|
| 290 | destruct |
---|
| 291 | ] |
---|
| 292 | | #v #r * [2: #f #fs ] #m #tr #s' |
---|
| 293 | whd in ⊢ (??%? → ?); |
---|
| 294 | [ @bindIO_value #loc #Eloc #E whd in E:(??%?); destruct |
---|
| 295 | %6 cases f #func #locals #next #next_ok #sp #retdst % |
---|
| 296 | | #E destruct |
---|
| 297 | ] |
---|
| 298 | ] qed. |
---|
| 299 | |
---|