[639] | 1 | |
---|
| 2 | (* XXX NB: I haven't checked all of these semantics against the prototype |
---|
| 3 | compilers yet! *) |
---|
| 4 | |
---|
[1601] | 5 | include "basics/lists/list.ma". |
---|
[766] | 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. |
---|
[1655] | 91 | match st return λ_. IO ??? with |
---|
[639] | 92 | [ State f fs m ⇒ |
---|
[1535] | 93 | let s ≝ lookup_present ?? (f_graph (func f)) (next f) (next_ok f) in |
---|
[1655] | 94 | match s return λs. labels_present ? s → IO ??? with |
---|
| 95 | [ St_skip l ⇒ λH. return 〈E0, build_state f fs m l ?〉 |
---|
| 96 | | St_cost cl l ⇒ λH. return 〈Echarge cl, build_state f fs m l ?〉 |
---|
[1535] | 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); |
---|
[1655] | 100 | return 〈E0, State (mk_frame (func f) locals l ? (sp f) (retdst f)) fs m〉 |
---|
[1535] | 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); |
---|
[1655] | 105 | return 〈E0, State (mk_frame (func f) locals l ? (sp f) (retdst f)) fs m〉 |
---|
[1535] | 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); |
---|
[1655] | 111 | return 〈E0, State (mk_frame (func f) locals l ? (sp f) (retdst f)) fs m〉 |
---|
[1535] | 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); |
---|
[1655] | 116 | return 〈E0, State (mk_frame (func f) locals l ? (sp f) (retdst f)) fs m〉 |
---|
[1535] | 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); |
---|
[1655] | 121 | return 〈E0, build_state f fs m' l ?〉 |
---|
[1535] | 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); |
---|
[1655] | 125 | ! vs ← m_mmap … (reg_retrieve (locals f)) args; |
---|
| 126 | return 〈E0, Callstate fd vs dst (adv l f ?::fs) m〉 |
---|
[1535] | 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); |
---|
[1655] | 130 | ! vs ← m_mmap … (reg_retrieve (locals f)) args; |
---|
| 131 | return 〈E0, Callstate fd vs dst (adv l f ?::fs) m〉 |
---|
[1680] | 132 | (* |
---|
[1535] | 133 | | St_tailcall_id id args ⇒ λH. |
---|
[797] | 134 | ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id); |
---|
| 135 | ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b); |
---|
[1655] | 136 | ! vs ← m_mmap … (reg_retrieve (locals f)) args; |
---|
| 137 | return 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉 |
---|
[1535] | 138 | | St_tailcall_ptr frs args ⇒ λH. |
---|
[639] | 139 | ! fv ← reg_retrieve (locals f) frs; |
---|
[797] | 140 | ! fd ← opt_to_res … (msg BadFunction) (find_funct ?? ge fv); |
---|
[1655] | 141 | ! vs ← m_mmap … (reg_retrieve (locals f)) args; |
---|
| 142 | return 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉 |
---|
[1680] | 143 | *) |
---|
[1535] | 144 | | St_cond src ltrue lfalse ⇒ λH. |
---|
[888] | 145 | ! v ← reg_retrieve (locals f) src; |
---|
[751] | 146 | ! b ← eval_bool_of_val v; |
---|
[1655] | 147 | return 〈E0, build_state f fs m (if b then ltrue else lfalse) ?〉 |
---|
[639] | 148 | |
---|
[1535] | 149 | | St_jumptable r ls ⇒ λH. |
---|
[750] | 150 | ! v ← reg_retrieve (locals f) r; |
---|
[639] | 151 | match v with |
---|
[961] | 152 | [ Vint _ i ⇒ |
---|
[1535] | 153 | match nth_opt ? (nat_of_bitvector ? i) ls return λx. nth_opt ??? = x → ? with |
---|
[1655] | 154 | [ None ⇒ λ_. Error ? (msg BadJumpTable) |
---|
| 155 | | Some l ⇒ λE. return 〈E0, build_state f fs m l ?〉 |
---|
[1535] | 156 | ] (refl ??) |
---|
[1655] | 157 | | _ ⇒ Error ? (msg BadJumpValue) |
---|
[639] | 158 | ] |
---|
| 159 | |
---|
[1535] | 160 | | St_return ⇒ λH. |
---|
[765] | 161 | ! v ← match f_result (func f) with |
---|
[1655] | 162 | [ None ⇒ return (None ?) |
---|
[887] | 163 | | Some rt ⇒ |
---|
| 164 | let 〈r,ty〉 ≝ rt in |
---|
| 165 | ! v ← reg_retrieve (locals f) r; |
---|
[1655] | 166 | return (Some ? v) |
---|
[765] | 167 | ]; |
---|
[1655] | 168 | return 〈E0, Returnstate v (retdst f) fs (free m (sp f))〉 |
---|
[1535] | 169 | ] (f_closed (func f) (next f) s ?) |
---|
[639] | 170 | | Callstate fd params dst fs m ⇒ |
---|
[1655] | 171 | match fd return λ_. IO ??? with |
---|
[639] | 172 | [ Internal fn ⇒ |
---|
[761] | 173 | ! locals ← params_store (f_params fn) params (init_locals (f_locals fn)); |
---|
[1123] | 174 | (* CSC: XXX alignment call (concrete_stacksize in OCaml) is missing |
---|
| 175 | here *) |
---|
[639] | 176 | let 〈m', sp〉 ≝ alloc m 0 (f_stacksize fn) Any in |
---|
[1655] | 177 | return 〈E0, State (mk_frame fn locals (f_entry fn) ? sp dst) fs m'〉 |
---|
[639] | 178 | | External fn ⇒ |
---|
[1655] | 179 | ! evargs ← err_to_io … (check_eventval_list params (sig_args (ef_sig fn))); |
---|
[879] | 180 | ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn)); |
---|
[1655] | 181 | return 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), Returnstate (Some ? (mk_val ? evres) (*FIXME should allow None *)) dst fs m〉 |
---|
[639] | 182 | ] |
---|
| 183 | | Returnstate v dst fs m ⇒ |
---|
| 184 | match fs with |
---|
[797] | 185 | [ nil ⇒ Error ? (msg FinalState) (* Already in final state *) |
---|
[639] | 186 | | cons f fs' ⇒ |
---|
[765] | 187 | ! locals ← match dst with |
---|
| 188 | [ None ⇒ match v with [ None ⇒ OK ? (locals f) |
---|
[797] | 189 | | _ ⇒ Error ? (msg ReturnMismatch) ] |
---|
| 190 | | Some d ⇒ match v with [ None ⇒ Error ? (msg ReturnMismatch) |
---|
[765] | 191 | | Some v' ⇒ reg_store d v' (locals f) ] ]; |
---|
[1655] | 192 | return 〈E0, State (mk_frame (func f) locals (next f) ? (sp f) (retdst f)) fs' m〉 |
---|
[639] | 193 | ] |
---|
[1535] | 194 | ]. try @(next_ok f) try @lookup_lookup_present try @H |
---|
| 195 | [ cases b [ @(proj1 ?? H) | @(proj2 ?? H) ] |
---|
| 196 | | whd in H; @(All_nth … H ? E) |
---|
| 197 | | cases (f_entry fn) // |
---|
| 198 | ] qed. |
---|
[693] | 199 | |
---|
[1559] | 200 | definition RTLabs_is_final : state → option int ≝ |
---|
[693] | 201 | λs. match s with |
---|
| 202 | [ State _ _ _ ⇒ None ? |
---|
| 203 | | Callstate _ _ _ _ _ ⇒ None ? |
---|
| 204 | | Returnstate v _ fs _ ⇒ |
---|
[961] | 205 | match fs with [ nil ⇒ |
---|
| 206 | match v with [ Some v' ⇒ |
---|
| 207 | match v' with |
---|
| 208 | [ Vint sz i ⇒ intsize_eq_elim ? sz I32 ? i (λi. Some ? i) (None ?) |
---|
| 209 | | _ ⇒ None ? ] |
---|
| 210 | | None ⇒ None ? ] |
---|
| 211 | | cons _ _ ⇒ None ? ] |
---|
[693] | 212 | ]. |
---|
| 213 | |
---|
[1238] | 214 | definition RTLabs_exec : trans_system io_out io_in ≝ |
---|
[1559] | 215 | mk_trans_system … ? (λ_.RTLabs_is_final) eval_statement. |
---|
[702] | 216 | |
---|
[1238] | 217 | definition make_global : RTLabs_program → genv ≝ |
---|
| 218 | λp. globalenv Genv ?? (λx.[Init_space x]) p. |
---|
| 219 | |
---|
| 220 | definition make_initial_state : RTLabs_program → res state ≝ |
---|
[702] | 221 | λp. |
---|
[1238] | 222 | let ge ≝ make_global p in |
---|
[1139] | 223 | do m ← init_mem Genv ?? (λx.[Init_space x]) p; |
---|
[797] | 224 | let main ≝ prog_main ?? p in |
---|
| 225 | do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol ? ? ge main); |
---|
| 226 | do f ← opt_to_res ? [MSG BadFunction; CTX ? main] (find_funct_ptr ? ? ge b); |
---|
[1238] | 227 | OK ? (Callstate f (nil ?) (None ?) (nil ?) m). |
---|
[702] | 228 | |
---|
[731] | 229 | definition RTLabs_fullexec : fullexec io_out io_in ≝ |
---|
[1238] | 230 | mk_fullexec … RTLabs_exec make_global make_initial_state. |
---|
[731] | 231 | |
---|
[1583] | 232 | |
---|
| 233 | (* Some lemmas about the semantics. *) |
---|
| 234 | |
---|
| 235 | (* Note parts of frames and states that are preserved. *) |
---|
| 236 | |
---|
| 237 | inductive frame_rel : frame → frame → Prop ≝ |
---|
| 238 | | mk_frame_rel : |
---|
| 239 | ∀func,locals,next,next_ok,sp,retdst,locals',next',next_ok'. frame_rel |
---|
| 240 | (mk_frame func locals next next_ok sp retdst) |
---|
| 241 | (mk_frame func locals' next' next_ok' sp retdst) |
---|
| 242 | . |
---|
| 243 | |
---|
| 244 | inductive state_rel : genv → state → state → Prop ≝ |
---|
| 245 | | normal : ∀ge,f,f',fs,m,m'. frame_rel f f' → state_rel ge (State f fs m) (State f' fs m') |
---|
| 246 | | 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) |
---|
[1681] | 247 | (* |
---|
[1583] | 248 | | 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') |
---|
[1681] | 249 | *) |
---|
[1583] | 250 | | 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') |
---|
| 251 | | to_ret : ∀ge,f,fs,m,rtv,dst,m'. state_rel ge (State f fs m) (Returnstate rtv dst fs m') |
---|
| 252 | | 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) |
---|
| 253 | . |
---|
| 254 | |
---|
[1655] | 255 | lemma bind_ok : ∀A,B,e,f,v. ∀P:B → Prop. |
---|
| 256 | (∀a. e = OK A a → f a = OK ? v → P v) → |
---|
| 257 | (match e with [ OK v ⇒ f v | Error m ⇒ Error ? m ] = OK ? v → P v). |
---|
| 258 | #A #B * |
---|
| 259 | [ #a #f #v #P #H #E whd in E:(??%?); @(H a) // |
---|
| 260 | | #m #f #v #P #H #E whd in E:(??%?); destruct |
---|
| 261 | ] qed. |
---|
| 262 | |
---|
| 263 | lemma bind_value : ∀O,I,A,B,e,f,v. ∀P:B → Prop. |
---|
| 264 | (∀a. e = OK A a → f a = OK B v → P v) → |
---|
| 265 | (match e »= f with [ OK v ⇒ Value … v | Error m ⇒ Wrong … m ] = Value O I B v → P v). |
---|
| 266 | #O #I #A #B * |
---|
| 267 | [ #a #f #v #P #H #E @H [ @a | @refl | normalize in E; cases (f a) in E ⊢ %; |
---|
| 268 | [ #v' #E normalize in E; destruct @refl | #m #E normalize in E; destruct ] ] |
---|
| 269 | | #m #f #v #P #H #E whd in E:(??%?); destruct |
---|
| 270 | ] qed. |
---|
| 271 | |
---|
[1583] | 272 | lemma bindIO_value : ∀O,I,A,B,e,f,v. ∀P:B → Prop. |
---|
| 273 | (∀a. e = Value ??? a → f a = Value ??? v → P v) → |
---|
| 274 | (bindIO O I A B e f = Value ??? v → P v). |
---|
| 275 | #O #I #A #B * |
---|
| 276 | [ #o #k #f #v #P #H #E whd in E:(??%?); destruct |
---|
| 277 | | #a #f #v #P #H #E @H [ @a | @refl | @E ] |
---|
| 278 | | #m #f #v #P #H #E whd in E:(??%?); destruct |
---|
| 279 | ] qed. |
---|
| 280 | |
---|
| 281 | lemma eval_perserves : ∀ge,s,tr,s'. |
---|
| 282 | eval_statement ge s = Value ??? 〈tr,s'〉 → |
---|
| 283 | state_rel ge s s'. |
---|
| 284 | #ge * |
---|
| 285 | [ * #func #locals #next #next_ok #sp #retdst #fs #m |
---|
| 286 | #tr #s' |
---|
| 287 | whd in ⊢ (??%? → ?); |
---|
| 288 | generalize in ⊢ (??(?%)? → ?); |
---|
| 289 | cases (lookup_present LabelTag statement (f_graph func) next next_ok) |
---|
| 290 | [ #l #LP whd in ⊢ (??%? → ?); #E destruct % % |
---|
| 291 | | #c #l #LP whd in ⊢ (??%? → ?); #E destruct % % |
---|
[1655] | 292 | | #r #c #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #locals' #Eloc #E whd in E:(??%?); destruct % % |
---|
| 293 | | #t1 #t2 #op #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #v' #Ev' @bind_ok #loc #Eloc #E whd in E:(??%?); destruct % % |
---|
| 294 | | #op #r1 #r2 #r3 #l #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev' @bind_ok #loc #Eloc #E whd in E:(??%?); destruct % % |
---|
| 295 | | #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #v' #Ev' @bind_ok #loc #Eloc #E whd in E:(??%?); destruct % % |
---|
| 296 | | #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #v' #Ev' @bind_ok #loc #Eloc #E whd in E:(??%?); destruct % % |
---|
| 297 | | #id #rs #or #l #LP whd in ⊢ (??%? → ?); @bind_value #b #Eb @bind_ok #fd #Efd @bind_ok #vs #Evs #E whd in E:(??%?); destruct %2 [ % | @b | cases (find_funct_ptr ????) in Efd ⊢ %; normalize [2:#fd'] #E' destruct @refl ] |
---|
| 298 | | #r #rs #or #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #fd #Efd @bind_ok #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 ] |
---|
[1680] | 299 | (* |
---|
[1655] | 300 | | #id #rs #LP whd in ⊢ (??%? → ?); @bind_value #b #Eb @bind_ok #fd #Efd @bind_ok #vs #Evs #E whd in E:(??%?); destruct %3 [ @b | cases (find_funct_ptr ????) in Efd ⊢ %; [2:#x] normalize #E' destruct @refl ] |
---|
| 301 | | #r #rs #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #fd #Efd @bind_ok #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 ] |
---|
[1680] | 302 | *) |
---|
[1655] | 303 | | #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #b #Eb #E whd in E:(??%?); destruct % % |
---|
| 304 | | #r #ls #LP whd in ⊢ (??%? → ?); @bind_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 ] |
---|
[1681] | 305 | | #LP whd in ⊢ (??%? → ?); @bind_value #v cases (f_result func) [ 2: * #r #t whd in ⊢ (??%? → ?); @bind_ok #v0 #Ev0 ] #E whd in E:(??%?); #E' whd in E':(??%?); destruct %4 |
---|
[1583] | 306 | ] |
---|
| 307 | | * #fn #args #retdst #stk #m #tr #s' |
---|
| 308 | whd in ⊢ (??%? → ?); |
---|
[1655] | 309 | [ @bind_value #loc #Eloc cases (alloc m O ??) #m' #b whd in ⊢ (??%? → ?); |
---|
[1681] | 310 | #E destruct %3 |
---|
[1655] | 311 | | @bindIO_value #evargs #Eargs whd in ⊢ (??%? → ?); #E destruct |
---|
[1583] | 312 | ] |
---|
| 313 | | #v #r * [2: #f #fs ] #m #tr #s' |
---|
| 314 | whd in ⊢ (??%? → ?); |
---|
[1655] | 315 | [ @bind_value #loc #Eloc #E whd in E:(??%?); destruct |
---|
[1681] | 316 | %5 cases f #func #locals #next #next_ok #sp #retdst % |
---|
[1583] | 317 | | #E destruct |
---|
| 318 | ] |
---|
| 319 | ] qed. |
---|
| 320 | |
---|