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