[2559] | 1 | (**************************************************************************) |
---|
[2442] | 2 | (* ___ *) |
---|
| 3 | (* ||M|| *) |
---|
| 4 | (* ||A|| A project by Andrea Asperti *) |
---|
| 5 | (* ||T|| *) |
---|
| 6 | (* ||I|| Developers: *) |
---|
| 7 | (* ||T|| The HELM team. *) |
---|
| 8 | (* ||A|| http://helm.cs.unibo.it *) |
---|
| 9 | (* \ / *) |
---|
| 10 | (* \ / This file is distributed under the terms of the *) |
---|
| 11 | (* v GNU General Public License Version 2 *) |
---|
| 12 | (* *) |
---|
| 13 | (**************************************************************************) |
---|
| 14 | |
---|
| 15 | include "joint/linearise.ma". |
---|
| 16 | include "common/StatusSimulation.ma". |
---|
| 17 | include "joint/Traces.ma". |
---|
[2464] | 18 | include "joint/semanticsUtils.ma". |
---|
[2570] | 19 | include "common/ExtraMonads.ma". |
---|
[2442] | 20 | |
---|
[3371] | 21 | check mk_sem_graph_params |
---|
[2559] | 22 | |
---|
[3371] | 23 | definition graph_prog_params ≝ |
---|
| 24 | λp,p',pre_main,prog,stack_sizes. |
---|
| 25 | mk_prog_params (mk_sem_graph_params p p' pre_main) prog stack_sizes. |
---|
[2559] | 26 | |
---|
[3371] | 27 | check mk_sem_graph_params |
---|
[2559] | 28 | |
---|
[2442] | 29 | definition graph_abstract_status: |
---|
[3371] | 30 | ∀p:uns_params. |
---|
[2443] | 31 | (∀F.sem_unserialized_params p F) → |
---|
[3371] | 32 | (∀prog : joint_program (mk_graph_params p). |
---|
| 33 | joint_closed_internal_function (mk_graph_params p) (prog_names … prog)) → |
---|
[2464] | 34 | ∀prog : joint_program (mk_graph_params p). |
---|
[2529] | 35 | (ident → option ℕ) → |
---|
[2442] | 36 | abstract_status |
---|
[3371] | 37 | ≝ |
---|
| 38 | λp,p',pre_main,prog,stack_sizes. |
---|
| 39 | joint_abstract_status (graph_prog_params ? p' pre_main prog stack_sizes). |
---|
[2442] | 40 | |
---|
[2464] | 41 | definition lin_prog_params ≝ |
---|
[3371] | 42 | λp,p',pre_main,prog,stack_sizes. |
---|
| 43 | mk_prog_params (mk_sem_lin_params p p' pre_main) prog stack_sizes. |
---|
[2464] | 44 | |
---|
[2442] | 45 | definition lin_abstract_status: |
---|
[3371] | 46 | ∀p:uns_params. |
---|
[2443] | 47 | (∀F.sem_unserialized_params p F) → |
---|
[3371] | 48 | (∀prog : joint_program (mk_lin_params p). |
---|
| 49 | joint_closed_internal_function (mk_lin_params p) (prog_names … prog)) → |
---|
[2464] | 50 | ∀prog : joint_program (mk_lin_params p). |
---|
[2529] | 51 | (ident → option ℕ) → |
---|
[2442] | 52 | abstract_status |
---|
| 53 | ≝ |
---|
[3371] | 54 | λp,p',pre_main,prog,stack_sizes. |
---|
| 55 | joint_abstract_status (lin_prog_params ? p' pre_main prog stack_sizes). |
---|
[2442] | 56 | |
---|
[2476] | 57 | (* |
---|
| 58 | axiom P : |
---|
| 59 | ∀A,B,prog.A (prog_var_names (λvars.fundef (A vars)) B prog) → Prop. |
---|
| 60 | |
---|
| 61 | check (λpars.let pars' ≝ make_global pars in λx :joint_closed_internal_function pars' (globals pars'). P … x) |
---|
| 62 | (* |
---|
| 63 | unification hint 0 ≔ p, prog, stack_sizes ; |
---|
| 64 | pars ≟ mk_prog_params p prog stack_sizes , |
---|
| 65 | pars' ≟ make_global pars, |
---|
| 66 | A ≟ λvars.joint_closed_internal_function p vars, |
---|
| 67 | B ≟ ℕ |
---|
| 68 | ⊢ |
---|
| 69 | A (prog_var_names (λvars.fundef (A vars)) B prog) ≡ |
---|
| 70 | joint_closed_internal_function pars' (globals pars'). |
---|
| 71 | *) |
---|
| 72 | axiom T : ∀A,B,prog.genv_t (fundef (A (prog_var_names (λvars:list ident.fundef (A vars)) B prog))) → Prop. |
---|
| 73 | (*axiom Q : ∀A,B,init,prog. |
---|
| 74 | T … (globalenv (λvars:list ident.fundef (A vars)) B |
---|
| 75 | init prog) → Prop. |
---|
| 76 | |
---|
| 77 | lemma pippo : |
---|
| 78 | ∀p,p',prog,stack_sizes. |
---|
| 79 | let pars ≝ graph_prog_params p p' prog stack_sizes in |
---|
| 80 | let ge ≝ ev_genv pars in T ?? prog ge → Prop. |
---|
| 81 | |
---|
| 82 | #H1 #H2 #H3 #H4 |
---|
| 83 | #H5 |
---|
| 84 | whd in match (ev_genv ?) in H5; |
---|
| 85 | whd in match (globalenv_noinit) in H5; normalize nodelta in H5; |
---|
| 86 | whd in match (prog ?) in H5; |
---|
| 87 | whd in match (joint_function ?) in H5; |
---|
| 88 | @(Q … H5) |
---|
| 89 | λx:T ??? ge.Q ???? x) |
---|
| 90 | *) |
---|
| 91 | axiom Q : ∀A,B,init,prog,i. |
---|
| 92 | is_internal_function |
---|
| 93 | (A |
---|
| 94 | (prog_var_names (λvars:list ident.fundef (A vars)) B |
---|
| 95 | prog)) |
---|
| 96 | (globalenv (λvars:list ident.fundef (A vars)) B |
---|
| 97 | init prog) |
---|
| 98 | i → Prop. |
---|
| 99 | |
---|
| 100 | check |
---|
| 101 | (λp,p',prog,stack_sizes,i. |
---|
| 102 | let pars ≝ graph_prog_params p p' prog stack_sizes in |
---|
| 103 | let ge ≝ ev_genv pars in |
---|
| 104 | λx:is_internal_function (joint_closed_internal_function pars (globals pars)) |
---|
| 105 | ge i.Q ??? prog ? x) |
---|
| 106 | *) |
---|
| 107 | |
---|
[2529] | 108 | definition sigma_map ≝ λp.λgraph_prog : joint_program (mk_graph_params p). |
---|
| 109 | joint_closed_internal_function (mk_graph_params p) (prog_var_names … graph_prog) → |
---|
| 110 | label → option ℕ. |
---|
[2551] | 111 | |
---|
[2464] | 112 | definition sigma_pc_opt: |
---|
[2529] | 113 | ∀p,p'.∀graph_prog. |
---|
| 114 | sigma_map p graph_prog → |
---|
[2476] | 115 | program_counter → option program_counter |
---|
[2464] | 116 | ≝ |
---|
[2481] | 117 | λp,p',prog,sigma,pc. |
---|
[2808] | 118 | let pars ≝ mk_sem_graph_params p p' in |
---|
[2481] | 119 | let ge ≝ globalenv_noinit … prog in |
---|
[2551] | 120 | if eqZb (block_id (pc_block pc)) (-1) then (* check for dummy exit pc *) |
---|
| 121 | return pc |
---|
| 122 | else |
---|
| 123 | ! 〈i, fd〉 ← res_to_opt … (fetch_internal_function … ge (pc_block pc)) ; |
---|
| 124 | ! lin_point ← sigma fd (point_of_pc pars pc) ; |
---|
| 125 | return pc_of_point |
---|
[2808] | 126 | (mk_sem_lin_params ? p') (pc_block pc) lin_point. |
---|
[2445] | 127 | |
---|
[2464] | 128 | definition well_formed_pc: |
---|
[2481] | 129 | ∀p,p',graph_prog. |
---|
[2529] | 130 | sigma_map p graph_prog → |
---|
[2476] | 131 | program_counter → Prop |
---|
[2445] | 132 | ≝ |
---|
[2481] | 133 | λp,p',prog,sigma,pc. |
---|
| 134 | sigma_pc_opt p p' prog sigma pc |
---|
[2445] | 135 | ≠ None …. |
---|
| 136 | |
---|
[2484] | 137 | definition sigma_beval_opt : |
---|
| 138 | ∀p,p'.∀graph_prog : joint_program (mk_graph_params p). |
---|
[2529] | 139 | sigma_map p graph_prog → |
---|
[2484] | 140 | beval → option beval ≝ |
---|
| 141 | λp,p',graph_prog,sigma,bv. |
---|
| 142 | match bv with |
---|
| 143 | [ BVpc pc prt ⇒ ! pc' ← sigma_pc_opt p p' graph_prog sigma pc ; return BVpc pc' prt |
---|
| 144 | | _ ⇒ return bv |
---|
| 145 | ]. |
---|
[2446] | 146 | |
---|
[2484] | 147 | definition sigma_beval : |
---|
| 148 | ∀p,p',graph_prog,sigma,bv. |
---|
| 149 | sigma_beval_opt p p' graph_prog sigma bv ≠ None ? → beval ≝ |
---|
| 150 | λp,p',graph_prog,sigma,bv.opt_safe …. |
---|
| 151 | |
---|
[2495] | 152 | definition sigma_is_opt : |
---|
| 153 | ∀p,p'.∀graph_prog : joint_program (mk_graph_params p). |
---|
[2529] | 154 | sigma_map p graph_prog → |
---|
[2495] | 155 | internal_stack → option internal_stack ≝ |
---|
| 156 | λp,p',graph_prog,sigma,is. |
---|
| 157 | match is with |
---|
| 158 | [ empty_is ⇒ return empty_is |
---|
| 159 | | one_is bv ⇒ ! bv' ← sigma_beval_opt p p' … sigma bv ; return one_is bv' |
---|
| 160 | | both_is bv1 bv2 ⇒ |
---|
| 161 | ! bv1' ← sigma_beval_opt p p' … sigma bv1 ; |
---|
| 162 | ! bv2' ← sigma_beval_opt p p' … sigma bv2 ; |
---|
| 163 | return both_is bv1' bv2' |
---|
| 164 | ]. |
---|
| 165 | |
---|
| 166 | definition sigma_is : |
---|
| 167 | ∀p,p',graph_prog,sigma,is. |
---|
| 168 | sigma_is_opt p p' graph_prog sigma is ≠ None ? → internal_stack ≝ |
---|
| 169 | λp,p',graph_prog,sigma,is.opt_safe …. |
---|
[2547] | 170 | |
---|
| 171 | lemma sigma_is_empty : ∀p,p',graph_prog,sigma. |
---|
| 172 | ∀prf.sigma_is p p' graph_prog sigma empty_is prf = empty_is. |
---|
| 173 | #p #p' #graph_prog #sigma #prf whd in match sigma_is; normalize nodelta |
---|
| 174 | @opt_safe_elim #is' whd in ⊢ (??%%→?); #EQ destruct(EQ) % qed. |
---|
[2495] | 175 | |
---|
[2570] | 176 | (* spostato in ExtraMonads.ma |
---|
| 177 | |
---|
[2547] | 178 | lemma res_preserve_error : ∀X,Y,P,F,e,n.res_preserve X Y P F (Error … e) n. |
---|
| 179 | #X #Y #P #F #e #n #x whd in ⊢ (??%%→?); #EQ destruct(EQ) qed. |
---|
| 180 | |
---|
| 181 | lemma mfr_return_eq : ∀M1,M2.∀FR : MonadFunctRel M1 M2. |
---|
| 182 | ∀X,Y,P,F,v,n. |
---|
| 183 | ∀prf.n = return F v prf → |
---|
| 184 | FR X Y P F (return v) n. |
---|
| 185 | #M1 #M2 #FR #X #Y #P #F #v #n #prf #EQ >EQ @mfr_return qed. |
---|
| 186 | |
---|
| 187 | lemma opt_safe_eq : ∀A,m,x,prf.m = Some A x → opt_safe A m prf = x. |
---|
| 188 | #A #m #x #prf @opt_safe_elim #x' #EQ >EQ #EQ' destruct % qed. |
---|
[2570] | 189 | *) |
---|
[2547] | 190 | |
---|
[2495] | 191 | lemma sigma_is_pop_commute : |
---|
[2547] | 192 | ∀p,p',graph_prog,sigma,is. |
---|
[2495] | 193 | ∀prf : sigma_is_opt p p' graph_prog sigma is ≠ None ?. |
---|
[2547] | 194 | res_preserve … |
---|
| 195 | (λpr.sigma_beval_opt p p' graph_prog sigma (\fst pr) ≠ None ? ∧ |
---|
| 196 | sigma_is_opt p p' graph_prog sigma (\snd pr) ≠ None ?) |
---|
| 197 | (λpr,prf.〈sigma_beval … (proj1 … prf), sigma_is … (proj2 … prf)〉) |
---|
| 198 | (is_pop is) (is_pop (sigma_is … prf)). |
---|
| 199 | #p #p' #graph_prog #sigma * [|#bv1|#bv1 #bv2] #prf |
---|
| 200 | [ @res_preserve_error |
---|
| 201 | |*: |
---|
| 202 | whd in match sigma_is in ⊢ (?????????%); normalize nodelta |
---|
| 203 | @opt_safe_elim #is' |
---|
| 204 | #H @('bind_inversion H) -H #bv1' #EQ1 |
---|
| 205 | [2: #H @('bind_inversion H) -H #bv2' #EQ2 ] |
---|
| 206 | whd in ⊢ (??%%→?); #EQ destruct(EQ) |
---|
| 207 | @mfr_return_eq |
---|
| 208 | [1,3: @hide_prf %% |
---|
| 209 | |*: whd in match sigma_beval; whd in match sigma_is; |
---|
| 210 | normalize nodelta @opt_safe_elim #bv1'' @opt_safe_elim #is'' |
---|
| 211 | ] |
---|
| 212 | [2,4,5,6: whd in match sigma_is_opt; normalize nodelta [1,3: >EQ1 ] |
---|
| 213 | whd in ⊢ (??%%→?); #EQ destruct(EQ) ] |
---|
| 214 | [1,3: >EQ2 |*: >EQ1 ] #EQ' destruct(EQ') % |
---|
| 215 | ] |
---|
| 216 | qed. |
---|
[2495] | 217 | |
---|
[2547] | 218 | (* lemma opt_to_res_preserve : ∀X,Y.∀P : X → Y → Prop.∀e,u,v. |
---|
| 219 | opt_preserve P u v → res_preserve P (opt_to_res … e u) (opt_to_res … e v). |
---|
| 220 | #X #Y #P #e #u #v #H #x #EQ lapply (opt_eq_from_res ???? EQ) -EQ #EQ |
---|
| 221 | lapply (H … EQ) cases v [ * ] #y #K @K qed. |
---|
| 222 | |
---|
| 223 | lemma err_eq_from_io : ∀O,I,X,m,v. |
---|
| 224 | err_to_io O I X m = return v → m = return v. |
---|
| 225 | #O #I #X * #x #v normalize #EQ destruct % qed. |
---|
| 226 | |
---|
| 227 | lemma res_to_io_preserve : ∀X,Y.∀P : X → Y → Prop.∀O,I,u,v. |
---|
| 228 | res_preserve P u v → IO_preserve O I P u v. |
---|
| 229 | #X #Y #P #O #I #u #v #H #x #EQ lapply (err_eq_from_io ????? EQ) -EQ #EQ |
---|
| 230 | lapply (H … EQ) cases v [2: #e * ] #y #K @K qed. |
---|
| 231 | |
---|
| 232 | lemma preserve_opt_to_res : ∀X,Y.∀P : X → Y → Prop.∀e,u,v. |
---|
| 233 | res_preserve P (opt_to_res … e u) (opt_to_res … e v) → opt_preserve P u v. |
---|
| 234 | #X #Y #P #e #u #v #H #x #EQ |
---|
| 235 | lapply (H x) >EQ -H #H lapply (H (refl …)) cases v [ * ] |
---|
| 236 | #y #K @K qed. |
---|
| 237 | |
---|
| 238 | lemma preserve_res_to_io : ∀X,Y.∀P : X → Y → Prop.∀O,I,u,v. |
---|
| 239 | IO_preserve O I P (err_to_io … u) (err_to_io … v) → res_preserve P u v. |
---|
| 240 | #X #Y #P #O #I #u #v #H #x #EQ |
---|
| 241 | lapply (H x) >EQ -H #H lapply (H (refl …)) cases v [2: #e * ] |
---|
| 242 | #y #K @K qed. *) |
---|
| 243 | |
---|
[2495] | 244 | definition well_formed_mem : |
---|
| 245 | ∀p,p'.∀graph_prog : joint_program (mk_graph_params p). |
---|
[2529] | 246 | sigma_map p graph_prog → |
---|
[2495] | 247 | bemem → Prop ≝ |
---|
| 248 | λp,p',graph_prog,sigma,m. |
---|
| 249 | ∀b,z.block_id b < nextblock m → low_bound m b ≤ z → z < high_bound m b → |
---|
| 250 | sigma_beval_opt p p' graph_prog sigma (contents (blocks m b) z) ≠ None ?. |
---|
| 251 | |
---|
| 252 | definition sigma_mem : |
---|
| 253 | ∀p,p',graph_prog,sigma,m. |
---|
| 254 | well_formed_mem p p' graph_prog sigma m → |
---|
| 255 | bemem ≝ |
---|
| 256 | λp,p',graph_prog,sigma,m,prf. |
---|
| 257 | mk_mem |
---|
| 258 | (λb. |
---|
| 259 | If Zltb (block_id b) (nextblock m) then with prf' do |
---|
| 260 | let l ≝ low_bound m b in |
---|
| 261 | let h ≝ high_bound m b in |
---|
| 262 | mk_block_contents l h |
---|
| 263 | (λz.If Zleb l z ∧ Zltb z h then with prf'' do |
---|
| 264 | sigma_beval p p' graph_prog sigma (contents (blocks m b) z) ? |
---|
| 265 | else BVundef) |
---|
| 266 | else empty_block OZ OZ) |
---|
| 267 | (nextblock m) |
---|
| 268 | (nextblock_pos m). |
---|
| 269 | @hide_prf |
---|
| 270 | lapply prf'' lapply prf' -prf' -prf'' |
---|
| 271 | @Zltb_elim_Type0 [2: #_ * ] |
---|
| 272 | #bid_ok * |
---|
| 273 | @Zleb_elim_Type0 [2: #_ * ] |
---|
| 274 | @Zltb_elim_Type0 [2: #_ #_ * ] |
---|
| 275 | #zh #zl * @(prf … bid_ok zl zh) |
---|
| 276 | qed. |
---|
| 277 | |
---|
[2501] | 278 | lemma andb_false : ∀b1,b2.andb b1 b2 = false → b1 = false ∨ b2 = false. |
---|
| 279 | ** /2 by or_introl, or_intror/ normalize #ABS destruct(ABS) qed. |
---|
| 280 | |
---|
| 281 | axiom mem_ext_eq : |
---|
| 282 | ∀m1,m2 : mem. |
---|
| 283 | (∀b.let bc1 ≝ blocks m1 b in |
---|
| 284 | let bc2 ≝ blocks m2 b in |
---|
| 285 | low bc1 = low bc2 ∧ high bc1 = high bc2 ∧ |
---|
| 286 | ∀z.contents bc1 z = contents bc2 z) → |
---|
| 287 | nextblock m1 = nextblock m2 → m1 = m2. |
---|
[2570] | 288 | (* spostato in ExtraMonads.ma |
---|
[2501] | 289 | |
---|
[2547] | 290 | lemma opt_preserve_none : ∀X,Y,P,F,n.opt_preserve X Y P F (None ?) n. |
---|
| 291 | #X #Y #P #F #n #x whd in ⊢ (??%%→?); #EQ destruct(EQ) qed. |
---|
[2570] | 292 | *) |
---|
[2547] | 293 | |
---|
[2495] | 294 | lemma beloadv_sigma_commute: |
---|
[2547] | 295 | ∀p,p',graph_prog,sigma,ptr. |
---|
| 296 | preserving … opt_preserve … |
---|
| 297 | (sigma_mem p p' graph_prog sigma) |
---|
| 298 | (sigma_beval p p' graph_prog sigma) |
---|
| 299 | (λm.beloadv m ptr) |
---|
| 300 | (λm.beloadv m ptr). |
---|
| 301 | #p #p' #graph_prog #sigma #ptr #m #prf #bv |
---|
[2501] | 302 | whd in match beloadv; |
---|
| 303 | whd in match do_if_in_bounds; |
---|
| 304 | whd in match sigma_mem; |
---|
| 305 | normalize nodelta |
---|
| 306 | @If_elim #block_ok >block_ok normalize nodelta |
---|
| 307 | [2: whd in ⊢ (???%→?); #ABS destruct(ABS) ] |
---|
| 308 | @If_elim #H |
---|
| 309 | [ elim (andb_true … H) |
---|
| 310 | #H1 #H2 |
---|
| 311 | whd in match sigma_beval; normalize nodelta |
---|
| 312 | @opt_safe_elim #bv' #EQ_bv' >H1 >H2 normalize nodelta |
---|
| 313 | whd in ⊢ (???%→?); #EQ' destruct |
---|
| 314 | >EQ_bv' % [ % #ABS destruct(ABS) ] @opt_to_opt_safe |
---|
| 315 | | elim (andb_false … H) -H #H >H |
---|
| 316 | [2: >commutative_andb ] normalize nodelta |
---|
| 317 | whd in ⊢ (???%→?); #ABS destruct(ABS) |
---|
| 318 | ] |
---|
| 319 | qed. |
---|
[2495] | 320 | |
---|
[2559] | 321 | include alias "common/GenMem.ma". |
---|
| 322 | |
---|
[2495] | 323 | lemma bestorev_sigma_commute : |
---|
[2547] | 324 | ∀p,p',graph_prog,sigma,ptr. |
---|
| 325 | preserving2 ?? opt_preserve … |
---|
| 326 | (sigma_mem p p' graph_prog sigma) |
---|
| 327 | (sigma_beval p p' graph_prog sigma) |
---|
| 328 | (sigma_mem p p' graph_prog sigma) |
---|
| 329 | (λm.bestorev m ptr) |
---|
| 330 | (λm.bestorev m ptr). |
---|
| 331 | #p #p' #graph_prog #sigma #ptr #m #bv #prf1 #prf2 #m' |
---|
[2501] | 332 | whd in match bestorev; |
---|
| 333 | whd in match do_if_in_bounds; |
---|
| 334 | whd in match sigma_mem; |
---|
| 335 | whd in match update_block; |
---|
| 336 | normalize nodelta |
---|
| 337 | @If_elim #block_ok >block_ok normalize nodelta |
---|
| 338 | [2: whd in ⊢ ((???%) → ?); #ABS destruct(ABS)] |
---|
| 339 | @Zleb_elim_Type0 #H1 |
---|
| 340 | [ @Zltb_elim_Type0 #H2 ] |
---|
| 341 | [2,3: #ABS normalize in ABS; destruct(ABS) ] |
---|
| 342 | normalize nodelta whd in ⊢ (???%→?); #EQ destruct(EQ) |
---|
| 343 | % |
---|
| 344 | [2: whd in ⊢ (???%); |
---|
[2551] | 345 | @eq_f |
---|
[2501] | 346 | @mem_ext_eq [2: % ] |
---|
| 347 | #b @if_elim |
---|
| 348 | [2: #B |
---|
| 349 | @If_elim #prf1 @If_elim #prf2 |
---|
| 350 | [2,3: @⊥ >prf1 in prf2; * /2 by I/ ] [2: % [%%] #z % ] |
---|
| 351 | whd in match low_bound; whd in match high_bound; |
---|
| 352 | normalize nodelta |
---|
| 353 | cut (Not (bool_to_Prop (eq_block b (pblock ptr)))) |
---|
| 354 | [ % #ABS >ABS in B; * ] |
---|
| 355 | -B #B % [ >B %% ] #z |
---|
| 356 | @If_elim #prf3 |
---|
| 357 | @If_elim #prf4 |
---|
| 358 | [2,3: @⊥ >B in prf4; normalize nodelta >prf3 * /2 by I/ |4: % ] |
---|
| 359 | whd in match sigma_beval in ⊢ (??%%); normalize nodelta |
---|
| 360 | @opt_safe_elim @opt_safe_elim #bv1 #EQ1 #bv2 #EQ2 >B in EQ1; |
---|
| 361 | >EQ2 #EQ destruct(EQ) % |
---|
| 362 | | #B cut (b = pblock ptr) [ lapply B @eq_block_elim // #_ * ] |
---|
| 363 | #EQ destruct(EQ) |
---|
| 364 | @If_elim whd in match low_bound; whd in match high_bound; |
---|
| 365 | normalize nodelta |
---|
| 366 | [2: >block_ok * #ABS elim (ABS I) ] |
---|
| 367 | #prf3 % [ >B %% ] |
---|
| 368 | #z whd in match update; normalize nodelta |
---|
| 369 | @eqZb_elim normalize nodelta #prf4 |
---|
| 370 | [2: @If_elim #prf5 @If_elim #prf6 |
---|
| 371 | [2,3: @⊥ >B in prf6; >prf5 * /2 by I/ |4: % ] |
---|
| 372 | whd in match sigma_beval in ⊢ (??%%); normalize nodelta |
---|
| 373 | @opt_safe_elim @opt_safe_elim #bv1 #EQ1 #bv2 #EQ2 >B in EQ1; |
---|
| 374 | normalize nodelta >(eqZb_false … prf4) >EQ2 |
---|
| 375 | #EQ destruct(EQ) % |
---|
| 376 | | @If_elim #prf5 |
---|
| 377 | [2: >B in prf5; normalize nodelta |
---|
| 378 | >prf4 >(Zle_to_Zleb_true … H1) >(Zlt_to_Zltb_true … H2) * #ABS elim (ABS I) ] |
---|
| 379 | whd in match sigma_beval in ⊢ (??%%); normalize nodelta |
---|
| 380 | @opt_safe_elim @opt_safe_elim #bv1 #EQ1 #bv2 #EQ2 >B in EQ1; |
---|
| 381 | normalize nodelta >prf4 >eqZb_z_z >EQ2 #EQ destruct(EQ) % |
---|
| 382 | ] |
---|
| 383 | ] |
---|
| 384 | | whd #b #z #h1 whd in match low_bound; whd in match high_bound; normalize nodelta |
---|
| 385 | @eq_block_elim #H normalize nodelta destruct |
---|
| 386 | #h2 #h3 whd in match update; normalize nodelta |
---|
| 387 | [ @eqZb_elim #H destruct normalize nodelta [ assumption ]] |
---|
| 388 | @prf1 assumption |
---|
| 389 | ] |
---|
| 390 | qed. |
---|
[2495] | 391 | |
---|
| 392 | record good_sem_state_sigma |
---|
| 393 | (p : unserialized_params) |
---|
| 394 | (p' : ∀F.sem_unserialized_params p F) (graph_prog : ?) |
---|
[2529] | 395 | (sigma : sigma_map p graph_prog) : Type[0] ≝ |
---|
[2808] | 396 | { well_formed_frames : framesT (mk_sem_graph_params p p') → Prop |
---|
| 397 | ; sigma_frames : ∀frms.well_formed_frames frms → framesT (mk_sem_lin_params p p') |
---|
[2495] | 398 | ; sigma_empty_frames_commute : |
---|
| 399 | ∃prf. |
---|
[2808] | 400 | empty_framesT (mk_sem_lin_params p p') = |
---|
| 401 | sigma_frames (empty_framesT (mk_sem_graph_params p p')) prf |
---|
[2495] | 402 | |
---|
[2808] | 403 | ; well_formed_regs : regsT (mk_sem_graph_params p p') → Prop |
---|
| 404 | ; sigma_regs : ∀regs.well_formed_regs regs → regsT (mk_sem_lin_params p p') |
---|
[2495] | 405 | ; sigma_empty_regsT_commute : |
---|
| 406 | ∀ptr.∃ prf. |
---|
[2808] | 407 | empty_regsT (mk_sem_lin_params p p') ptr = |
---|
| 408 | sigma_regs (empty_regsT (mk_sem_graph_params p p') ptr) prf |
---|
[2495] | 409 | ; sigma_load_sp_commute : |
---|
[2547] | 410 | preserving … res_preserve … |
---|
| 411 | (λ_.True) |
---|
| 412 | … |
---|
| 413 | sigma_regs |
---|
| 414 | (λx.λ_.x) |
---|
[2808] | 415 | (load_sp (mk_sem_graph_params p p')) |
---|
| 416 | (load_sp (mk_sem_lin_params p p')) |
---|
[2495] | 417 | ; sigma_save_sp_commute : |
---|
| 418 | ∀reg,ptr,prf1. ∃prf2. |
---|
[2808] | 419 | save_sp (mk_sem_lin_params p p') (sigma_regs reg prf1) ptr = |
---|
| 420 | sigma_regs (save_sp (mk_sem_graph_params p p') reg ptr) prf2 |
---|
[2495] | 421 | }. |
---|
| 422 | |
---|
| 423 | definition well_formed_state : |
---|
| 424 | ∀p,p'.∀graph_prog : joint_program (mk_graph_params p). |
---|
[2529] | 425 | ∀sigma. |
---|
[2495] | 426 | good_sem_state_sigma p p' graph_prog sigma → |
---|
[2808] | 427 | state (mk_sem_graph_params p p') → Prop ≝ |
---|
[2495] | 428 | λp,p',graph_prog,sigma,gsss,st. |
---|
| 429 | well_formed_frames … gsss (st_frms … st) ∧ |
---|
| 430 | sigma_is_opt p p' graph_prog sigma (istack … st) ≠ None ? ∧ |
---|
| 431 | well_formed_regs … gsss (regs … st) ∧ |
---|
| 432 | well_formed_mem p p' graph_prog sigma (m … st). |
---|
| 433 | |
---|
| 434 | definition sigma_state : |
---|
| 435 | ∀p,p'.∀graph_prog : joint_program (mk_graph_params p). |
---|
[2529] | 436 | ∀sigma. |
---|
[2495] | 437 | ∀gsss : good_sem_state_sigma p p' graph_prog sigma. |
---|
[2808] | 438 | ∀st : state (mk_sem_graph_params p p'). |
---|
[2495] | 439 | well_formed_state … gsss st → |
---|
[2808] | 440 | state (mk_sem_lin_params p p') ≝ |
---|
[2495] | 441 | λp,p',graph_prog,sigma,gsss,st,prf. |
---|
| 442 | mk_state … |
---|
[2528] | 443 | (sigma_frames p p' graph_prog sigma gsss (st_frms … st) ?) |
---|
| 444 | (sigma_is p p' graph_prog sigma (istack … st) ?) |
---|
[2495] | 445 | (carry … st) |
---|
[2528] | 446 | (sigma_regs … gsss (regs … st) ?) |
---|
| 447 | (sigma_mem p p' graph_prog sigma (m … st) ?). |
---|
[2547] | 448 | @hide_prf cases prf ** // |
---|
[2528] | 449 | qed. |
---|
[2495] | 450 | |
---|
| 451 | |
---|
| 452 | (* |
---|
| 453 | lemma sigma_is_pop_wf : |
---|
| 454 | ∀p,p',graph_prog,sigma,is,bv,is'. |
---|
| 455 | is_pop is = return 〈bv, is'〉 → |
---|
| 456 | sigma_is_opt p p' graph_prog sigma is ≠ None ? → |
---|
| 457 | sigma_beval_opt p p' graph_prog sigma bv ≠ None ? ∧ |
---|
| 458 | sigma_is_opt p p' graph_prog sigma is' ≠ None ?. |
---|
| 459 | cases daemon qed. |
---|
| 460 | *) |
---|
| 461 | |
---|
[2464] | 462 | (* |
---|
| 463 | lemma prova : ∀p,s,st,prf.sigma_pc_of_status p s st prf = ?. |
---|
| 464 | [ #p #s #st #prf |
---|
| 465 | whd in match sigma_pc_of_status; normalize nodelta |
---|
| 466 | @opt_safe_elim |
---|
| 467 | #n |
---|
| 468 | lapply (refl … (int_funct_of_block (joint_closed_internal_function p) (globals p) |
---|
| 469 | (ev_genv p) (pblock (pc p st)))) |
---|
| 470 | elim (int_funct_of_block (joint_closed_internal_function p) (globals p) |
---|
| 471 | (ev_genv p) (pblock (pc p st))) in ⊢ (???%→%); |
---|
| 472 | [ #_ #ABS normalize in ABS; destruct(ABS) ] |
---|
| 473 | #f #EQ >m_return_bind |
---|
| 474 | *) |
---|
| 475 | |
---|
| 476 | |
---|
| 477 | (* |
---|
| 478 | lemma wf_status_to_wf_pc : |
---|
| 479 | ∀p,p',graph_prog,stack_sizes. |
---|
| 480 | ∀sigma : ((Σi.is_internal_function_of_program … graph_prog i) → |
---|
| 481 | code_point (mk_graph_params p) → option ℕ). |
---|
| 482 | ∀st. |
---|
| 483 | well_formed_status p p' graph_prog stack_sizes sigma st → |
---|
| 484 | well_formed_pc p p' graph_prog stack_sizes sigma (pc ? st). |
---|
| 485 | #p #p' #graph_prog #stack_sizes #sigma #st whd in ⊢ (% → ?); * #H #_ @H |
---|
| 486 | qed. |
---|
[2467] | 487 | *) |
---|
[2501] | 488 | definition sigma_pc : |
---|
[2481] | 489 | ∀p,p',graph_prog. |
---|
[2529] | 490 | ∀sigma. |
---|
[2464] | 491 | ∀pc. |
---|
[2481] | 492 | ∀prf : well_formed_pc p p' graph_prog sigma pc. |
---|
[2476] | 493 | program_counter ≝ |
---|
[2481] | 494 | λp,p',graph_prog,sigma,st.opt_safe …. |
---|
[2467] | 495 | |
---|
[2484] | 496 | lemma sigma_pc_ok: |
---|
[2481] | 497 | ∀p,p',graph_prog. |
---|
[2467] | 498 | ∀sigma. |
---|
| 499 | ∀pc. |
---|
[2481] | 500 | ∀prf:well_formed_pc p p' graph_prog sigma pc. |
---|
| 501 | sigma_pc_opt p p' graph_prog sigma pc = |
---|
| 502 | Some … (sigma_pc p p' graph_prog sigma pc prf). |
---|
| 503 | #p #p' #graph_prog #sigma #st #prf @opt_to_opt_safe qed. |
---|
[2464] | 504 | |
---|
[2556] | 505 | lemma sigma_pc_irr : |
---|
| 506 | ∀p,p',graph_prog,sigma,pc1,pc2,prf1,prf2. |
---|
| 507 | pc1 = pc2 → |
---|
| 508 | sigma_pc p p' graph_prog sigma pc1 prf1 = |
---|
| 509 | sigma_pc p p' graph_prog sigma pc2 prf2. |
---|
| 510 | #p #p' #graph_prog #sigma #pc1 #pc2 #prf1 #prf2 |
---|
| 511 | #EQ destruct(EQ) % qed. |
---|
| 512 | |
---|
[2495] | 513 | definition well_formed_state_pc : |
---|
| 514 | ∀p,p',graph_prog,sigma. |
---|
| 515 | good_sem_state_sigma p p' graph_prog sigma → |
---|
[2808] | 516 | state_pc (mk_sem_graph_params p p') → Prop ≝ |
---|
[2495] | 517 | λp,p',prog,sigma,gsss,st. |
---|
[2556] | 518 | well_formed_pc p p' prog sigma (last_pop … st) ∧ |
---|
| 519 | well_formed_pc p p' prog sigma (pc … st) ∧ |
---|
| 520 | well_formed_state … gsss st. |
---|
[2495] | 521 | |
---|
| 522 | definition sigma_state_pc : |
---|
| 523 | ∀p. |
---|
| 524 | ∀p':∀F.sem_unserialized_params p F. |
---|
| 525 | ∀graph_prog. |
---|
| 526 | ∀sigma. |
---|
| 527 | (* let lin_prog ≝ linearise ? graph_prog in *) |
---|
| 528 | ∀gsss : good_sem_state_sigma p p' graph_prog sigma. |
---|
[2808] | 529 | ∀s:state_pc (mk_sem_graph_params p p'). (* = graph_abstract_status p p' graph_prog stack_sizes *) |
---|
[2495] | 530 | well_formed_state_pc p p' graph_prog sigma gsss s → |
---|
[2808] | 531 | state_pc (mk_sem_lin_params p p') (* = lin_abstract_status p p' lin_prog ? *) |
---|
[2495] | 532 | ≝ |
---|
| 533 | λp,p',graph_prog,sigma,gsss,s,prf. |
---|
[2556] | 534 | let last_pop' ≝ sigma_pc … (proj1 … (proj1 … prf)) in |
---|
| 535 | let pc' ≝ sigma_pc … (proj2 … (proj1 … prf)) in |
---|
[2495] | 536 | let st' ≝ sigma_state … (proj2 … prf) in |
---|
[2556] | 537 | mk_state_pc ? st' pc' last_pop'. |
---|
[2529] | 538 | (* |
---|
[2484] | 539 | definition sigma_function_name : |
---|
| 540 | ∀p,graph_prog. |
---|
| 541 | let lin_prog ≝ linearise p graph_prog in |
---|
| 542 | (Σf.is_internal_function_of_program … graph_prog f) → |
---|
| 543 | (Σf.is_internal_function_of_program … lin_prog f) ≝ |
---|
| 544 | λp,graph_prog,f.«f, if_propagate … (pi2 … f)». |
---|
[2529] | 545 | *) |
---|
[2570] | 546 | |
---|
| 547 | (* spostato in ExtraMonads.ma |
---|
| 548 | |
---|
[2495] | 549 | lemma m_list_map_All_ok : |
---|
| 550 | ∀M : MonadProps.∀X,Y,f,l. |
---|
| 551 | All X (λx.∃y.f x = return y) l → ∃l'.m_list_map M X Y f l = return l'. |
---|
[2556] | 552 | #M #X #Y #f #l elim l -l |
---|
| 553 | [ * %{[ ]} % |
---|
| 554 | | #hd #tl #IH * * #y #EQ #H cases (IH H) #ys #EQ' |
---|
| 555 | %{(y :: ys)} |
---|
| 556 | change with (! y ← ? ; ? = ?) |
---|
| 557 | >EQ >m_return_bind |
---|
| 558 | change with (! acc ← m_list_map ????? ; ? = ?) >EQ' |
---|
| 559 | @m_return_bind |
---|
| 560 | qed. |
---|
[2570] | 561 | *) |
---|
[2495] | 562 | |
---|
| 563 | definition helper_def_store__commute : |
---|
| 564 | ∀p,p',graph_prog,sigma. |
---|
| 565 | ∀X : ? → Type[0]. |
---|
| 566 | ∀gsss : good_sem_state_sigma p p' graph_prog sigma. |
---|
| 567 | ∀store : ∀p,F.∀p' : sem_unserialized_params p F. |
---|
| 568 | X p → beval → regsT p' → |
---|
| 569 | res (regsT p'). |
---|
| 570 | Prop ≝ |
---|
| 571 | λp,p',graph_prog,sigma,X,gsss,store. |
---|
[2547] | 572 | ∀a : X p.preserving2 … res_preserve … |
---|
| 573 | (sigma_beval p p' graph_prog sigma) |
---|
| 574 | (sigma_regs … gsss) |
---|
| 575 | (sigma_regs … gsss) |
---|
| 576 | (store … a) |
---|
| 577 | (store … a). |
---|
| 578 | |
---|
[2495] | 579 | definition helper_def_retrieve__commute : |
---|
| 580 | ∀p,p',graph_prog,sigma. |
---|
| 581 | ∀X : ? → Type[0]. |
---|
| 582 | ∀gsss : good_sem_state_sigma p p' graph_prog sigma. |
---|
| 583 | ∀retrieve : ∀p,F.∀p' : sem_unserialized_params p F. |
---|
| 584 | regsT p' → X p → res beval. |
---|
| 585 | Prop ≝ |
---|
| 586 | λp,p',graph_prog,sigma,X,gsss,retrieve. |
---|
[2547] | 587 | ∀a : X p. |
---|
| 588 | preserving … res_preserve … |
---|
| 589 | (sigma_regs … gsss) |
---|
| 590 | (sigma_beval p p' graph_prog sigma) |
---|
| 591 | (λr.retrieve … r a) |
---|
| 592 | (λr.retrieve … r a). |
---|
[2536] | 593 | |
---|
[2495] | 594 | record good_state_sigma |
---|
| 595 | (p : unserialized_params) |
---|
[2484] | 596 | (p' : ∀F.sem_unserialized_params p F) (graph_prog : ?) |
---|
[2529] | 597 | (sigma : sigma_map p graph_prog) |
---|
[2484] | 598 | : Type[0] ≝ |
---|
[2495] | 599 | { gsss :> good_sem_state_sigma p p' graph_prog sigma |
---|
[2484] | 600 | |
---|
[2495] | 601 | ; acca_store__commute : helper_def_store__commute … gsss acca_store_ |
---|
| 602 | ; acca_retrieve_commute : helper_def_retrieve__commute … gsss acca_retrieve_ |
---|
[2501] | 603 | ; acca_arg_retrieve_commute : helper_def_retrieve__commute … gsss acca_arg_retrieve_ |
---|
| 604 | ; accb_store_commute : helper_def_store__commute … gsss accb_store_ |
---|
| 605 | ; accb_retrieve_commute : helper_def_retrieve__commute … gsss accb_retrieve_ |
---|
| 606 | ; accb_arg_retrieve_commute : helper_def_retrieve__commute … gsss accb_arg_retrieve_ |
---|
| 607 | ; dpl_store_commute : helper_def_store__commute … gsss dpl_store_ |
---|
| 608 | ; dpl_retrieve_commute : helper_def_retrieve__commute … gsss dpl_retrieve_ |
---|
| 609 | ; dpl_arg_retrieve_commute : helper_def_retrieve__commute … gsss dpl_arg_retrieve_ |
---|
| 610 | ; dph_store_commute : helper_def_store__commute … gsss dph_store_ |
---|
| 611 | ; dph_retrieve_commute : helper_def_retrieve__commute … gsss dph_retrieve_ |
---|
| 612 | ; dph_arg_retrieve_commute : helper_def_retrieve__commute … gsss dph_arg_retrieve_ |
---|
| 613 | ; snd_arg_retrieve_commute : helper_def_retrieve__commute … gsss snd_arg_retrieve_ |
---|
[2547] | 614 | ; pair_reg_move_commute : ∀mv. |
---|
| 615 | preserving … res_preserve … (sigma_regs … gsss) (sigma_regs … gsss) |
---|
| 616 | (λr.pair_reg_move_ ? ? (p' ?) r mv) |
---|
| 617 | (λr.pair_reg_move_ ? ? (p' ?) r mv) |
---|
| 618 | ; save_frame_commute : |
---|
| 619 | ∀dest,fl. |
---|
| 620 | preserving … res_preserve … |
---|
[2556] | 621 | (sigma_state_pc … gsss) |
---|
[2547] | 622 | (sigma_state … gsss) |
---|
| 623 | (save_frame ?? (p' ?) fl dest) |
---|
| 624 | (save_frame ?? (p' ?) fl dest) |
---|
[2501] | 625 | ; eval_ext_seq_commute : |
---|
| 626 | let lin_prog ≝ linearise p graph_prog in |
---|
[2536] | 627 | ∀ stack_sizes. |
---|
[2547] | 628 | ∀ext,i,fn. |
---|
| 629 | preserving … res_preserve … |
---|
| 630 | (sigma_state … gsss) |
---|
| 631 | (sigma_state … gsss) |
---|
| 632 | (eval_ext_seq ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes)) |
---|
| 633 | ext i fn) |
---|
| 634 | (eval_ext_seq ?? (p' ?) … (ev_genv (lin_prog_params … lin_prog stack_sizes)) |
---|
| 635 | ext i (\fst (linearise_int_fun … fn))) |
---|
[2501] | 636 | ; setup_call_commute : |
---|
[2551] | 637 | ∀ n , parsT, call_args. |
---|
| 638 | preserving … res_preserve … |
---|
| 639 | (sigma_state … gsss) |
---|
| 640 | (sigma_state … gsss) |
---|
| 641 | (setup_call ?? (p' ?) n parsT call_args) |
---|
| 642 | (setup_call ?? (p' ?) n parsT call_args) |
---|
[2501] | 643 | ; fetch_external_args_commute : (* TO BE CHECKED *) |
---|
| 644 | ∀ex_fun,st1,prf1,call_args. |
---|
| 645 | fetch_external_args ?? (p' ?) ex_fun st1 call_args = |
---|
| 646 | fetch_external_args ?? (p' ?) ex_fun (sigma_state p p' graph_prog sigma gsss st1 prf1) call_args |
---|
| 647 | ; set_result_commute : |
---|
[2551] | 648 | ∀ l , call_dest. |
---|
| 649 | preserving … res_preserve … |
---|
| 650 | (sigma_state … gsss) |
---|
| 651 | (sigma_state … gsss) |
---|
| 652 | (set_result ?? (p' ?) l call_dest) |
---|
| 653 | (set_result ?? (p' ?) l call_dest) |
---|
[2501] | 654 | ; read_result_commute : |
---|
| 655 | let lin_prog ≝ linearise p graph_prog in |
---|
[2529] | 656 | ∀stack_sizes. |
---|
[2551] | 657 | ∀call_dest. |
---|
| 658 | preserving … res_preserve … |
---|
| 659 | (sigma_state … gsss) |
---|
| 660 | (λl,prf.opt_safe ? (m_list_map … (sigma_beval_opt p p' graph_prog sigma) l) prf) |
---|
| 661 | (read_result ?? (p' ?) ? (ev_genv (graph_prog_params … graph_prog stack_sizes)) |
---|
| 662 | call_dest) |
---|
| 663 | (read_result ?? (p' ?) … (ev_genv (lin_prog_params … lin_prog stack_sizes)) |
---|
| 664 | call_dest) |
---|
[2501] | 665 | ; pop_frame_commute : |
---|
| 666 | let lin_prog ≝ linearise p graph_prog in |
---|
[2551] | 667 | ∀stack_sizes, curr_id , curr_fn. |
---|
| 668 | preserving … res_preserve … |
---|
| 669 | (sigma_state … gsss) |
---|
[2556] | 670 | (sigma_state_pc … gsss) |
---|
[2551] | 671 | (pop_frame ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes)) |
---|
| 672 | curr_id curr_fn) |
---|
| 673 | (pop_frame ?? (p' ?) … (ev_genv (lin_prog_params … lin_prog stack_sizes)) |
---|
| 674 | curr_id (\fst (linearise_int_fun … curr_fn))) |
---|
[2495] | 675 | }. |
---|
| 676 | |
---|
[2556] | 677 | lemma wf_set_regs : ∀p,p',graph_prog,sigma,gss,st,r. |
---|
| 678 | well_formed_state p p' graph_prog sigma gss st → |
---|
| 679 | well_formed_regs … gss r → |
---|
| 680 | well_formed_state … gss (set_regs … r st). |
---|
| 681 | #p #p' #graph_prog #sigma #gss #st #r |
---|
| 682 | *** #H1 #H2 #_ #H4 #H3 |
---|
| 683 | %{H4} %{H3} %{H2} @H1 |
---|
| 684 | qed. |
---|
| 685 | |
---|
| 686 | lemma allocate_locals_def : |
---|
| 687 | ∀p,F,p',loc,locs,st. |
---|
| 688 | allocate_locals p F p' (loc::locs) st = |
---|
| 689 | (let st' ≝ allocate_locals p F p' locs st in |
---|
| 690 | set_regs … (allocate_locals_ p F p' loc (regs … st')) st'). |
---|
| 691 | #p #F #p' #loc #locs #st % qed. |
---|
| 692 | |
---|
| 693 | lemma allocate_locals_commute : |
---|
| 694 | ∀p,p',graph_prog,sigma. |
---|
| 695 | ∀gss : good_state_sigma p p' graph_prog sigma. |
---|
| 696 | ∀locs, st1, prf1. ∃ prf2. |
---|
| 697 | allocate_locals ? ? (p' ?) locs (sigma_state … gss st1 prf1) = |
---|
| 698 | sigma_state … gss (allocate_locals ? ? (p' ?) locs st1) prf2. |
---|
| 699 | #p #p' #gp #sigma #gss #locs elim locs -locs |
---|
| 700 | [ #st1 #prf1 %{prf1} % ] |
---|
| 701 | #loc #tl #IH #st1 #prf1 |
---|
| 702 | letin st2 ≝ (sigma_state … st1 prf1) |
---|
| 703 | cases (IH st1 prf1) |
---|
| 704 | letin st1' ≝ (allocate_locals ??? tl st1) |
---|
| 705 | letin st2' ≝ (allocate_locals ??? tl st2) |
---|
| 706 | #prf' #EQ' |
---|
| 707 | cases (allocate_locals__commute … gss loc (regs … st1') ?) |
---|
| 708 | [2: @hide_prf cases prf' ** // ] |
---|
| 709 | #prf'' #EQ'' |
---|
| 710 | % [ @hide_prf @wf_set_regs assumption ] |
---|
| 711 | change with (set_regs ? (allocate_locals_ ??? loc (regs ? st1')) st1') |
---|
| 712 | in match (allocate_locals ??? (loc::tl) st1); |
---|
| 713 | change with (set_regs ? (allocate_locals_ ??? loc (regs ? st2')) st2') |
---|
| 714 | in match (allocate_locals ??? (loc::tl) st2); |
---|
| 715 | >EQ' >EQ'' % |
---|
| 716 | qed. |
---|
| 717 | |
---|
[2495] | 718 | lemma store_commute : |
---|
| 719 | ∀p,p',graph_prog,sigma. |
---|
| 720 | ∀X : ? → Type[0]. |
---|
| 721 | ∀store. |
---|
[2547] | 722 | ∀gsss : good_state_sigma p p' graph_prog sigma. |
---|
[2495] | 723 | ∀H : helper_def_store__commute … gsss store. |
---|
[2547] | 724 | ∀a : X p. |
---|
| 725 | preserving2 … res_preserve … |
---|
| 726 | (sigma_beval p p' graph_prog sigma) |
---|
| 727 | (sigma_state … gsss) |
---|
| 728 | (sigma_state … gsss) |
---|
| 729 | (helper_def_store ? store … a) |
---|
| 730 | (helper_def_store ? store … a). |
---|
| 731 | #p #p' #graph_prog #sigma #X #store #gsss #H #a |
---|
| 732 | #bv #st #prf1 #prf2 |
---|
| 733 | @(mfr_bind … (sigma_regs … gsss)) [@H] |
---|
| 734 | #r #prf3 @mfr_return cases st in prf2; |
---|
| 735 | #frms #is #carry #r' #m *** #H1 #H2 #H3 #H4 %{H4} % [%{H1 H2}] assumption |
---|
[2501] | 736 | qed. |
---|
[2495] | 737 | |
---|
| 738 | lemma retrieve_commute : |
---|
| 739 | ∀p,p',graph_prog,sigma. |
---|
| 740 | ∀X : ? → Type[0]. |
---|
| 741 | ∀retrieve. |
---|
| 742 | ∀gsss : good_sem_state_sigma p p' graph_prog sigma. |
---|
| 743 | ∀H : helper_def_retrieve__commute … gsss retrieve. |
---|
[2547] | 744 | ∀a : X p . |
---|
| 745 | preserving … res_preserve … |
---|
| 746 | (sigma_state … gsss) |
---|
| 747 | (sigma_beval p p' graph_prog sigma) |
---|
| 748 | (λst.helper_def_retrieve ? retrieve … st a) |
---|
| 749 | (λst.helper_def_retrieve ? retrieve … st a). |
---|
| 750 | #p #p' #graph_prog #sigma #X #retrieve #gsss #H #a #st #prf @H qed. |
---|
[2495] | 751 | |
---|
| 752 | (* |
---|
| 753 | definition acca_store_commute : |
---|
| 754 | ∀p,p',graph_prog,sigma. |
---|
| 755 | ∀gss : good_state_sigma p p' graph_prog sigma. |
---|
| 756 | ∀a : acc_a_reg p.∀bv,st,st',prf1,prf1'. |
---|
| 757 | acca_store … a bv st = return st' → |
---|
| 758 | ∃prf2. |
---|
| 759 | acca_store … a |
---|
| 760 | (sigma_beval p p' graph_prog sigma bv prf1') |
---|
| 761 | (sigma_state … gss st prf1) = return sigma_state … gss st' prf2 |
---|
| 762 | ≝ |
---|
| 763 | λp,p',graph_prog,sigma. |
---|
| 764 | λgss : good_state_sigma p p' graph_prog sigma. |
---|
[2501] | 765 | store_commute … gss (acca_store__commute … gss). |
---|
[2495] | 766 | |
---|
[2501] | 767 | *) |
---|
[2484] | 768 | |
---|
| 769 | (* restano: |
---|
| 770 | ; setup_call : nat → paramsT … uns_pars → call_args uns_pars → |
---|
| 771 | state st_pars → res (state st_pars) |
---|
| 772 | ; fetch_external_args: external_function → state st_pars → call_args … uns_pars → |
---|
| 773 | res (list val) |
---|
| 774 | ; set_result: list val → call_dest uns_pars → state st_pars → res (state st_pars) |
---|
| 775 | |
---|
| 776 | (* from now on, parameters that use the type of functions *) |
---|
| 777 | ; read_result: ∀globals.genv_gen F globals → call_dest uns_pars → state st_pars → res (list beval) |
---|
| 778 | (* change of pc must be left to *_flow execution *) |
---|
| 779 | ; pop_frame: ∀globals.∀ge : genv_gen F globals. |
---|
| 780 | (Σi.is_internal_function … ge i) (* current *) → state st_pars → res (state st_pars) |
---|
| 781 | *) |
---|
| 782 | |
---|
| 783 | (* |
---|
[2464] | 784 | lemma sigma_pc_commute: |
---|
[2484] | 785 | ∀p,p',graph_prog,sigma,gss,st. |
---|
| 786 | ∀prf : well_formed_state_pc p p' graph_prog sigma gss st. |
---|
[2464] | 787 | sigma_pc … (pc ? st) (proj1 … prf) = |
---|
[2484] | 788 | pc ? (sigma_state_pc … st prf). // qed. |
---|
| 789 | *) |
---|
[2446] | 790 | |
---|
[2529] | 791 | (* |
---|
[2467] | 792 | lemma if_of_function_commute: |
---|
[2481] | 793 | ∀p. |
---|
| 794 | ∀graph_prog : joint_program (mk_graph_params p). |
---|
| 795 | ∀graph_fun : Σi.is_internal_function_of_program … graph_prog i. |
---|
| 796 | let graph_fd ≝ if_of_function … graph_fun in |
---|
| 797 | let lin_fun ≝ sigma_function_name … graph_fun in |
---|
[2467] | 798 | let lin_fd ≝ if_of_function … lin_fun in |
---|
[2476] | 799 | lin_fd = \fst (linearise_int_fun ?? graph_fd). |
---|
[2481] | 800 | #p #graph_prog #graph_fun whd |
---|
| 801 | @prog_if_of_function_transform % qed. |
---|
[2529] | 802 | *) |
---|
[2551] | 803 | lemma pc_block_sigma_commute : |
---|
[2467] | 804 | ∀p,p',graph_prog. |
---|
| 805 | let lin_prog ≝ linearise p graph_prog in |
---|
[2476] | 806 | ∀sigma,pc. |
---|
[2481] | 807 | ∀prf : well_formed_pc p p' graph_prog sigma pc. |
---|
| 808 | pc_block (sigma_pc ? p' graph_prog sigma pc prf) = |
---|
[2476] | 809 | pc_block pc. |
---|
[2481] | 810 | #p #p' #graph_prog #sigma #pc #prf |
---|
[2551] | 811 | whd in match sigma_pc; whd in match sigma_pc_opt; normalize nodelta |
---|
| 812 | @opt_safe_elim #x |
---|
| 813 | @if_elim #_ |
---|
| 814 | [2: #H @('bind_inversion H) -H * #i #fn #_ |
---|
| 815 | #H @('bind_inversion H) -H #n #_ ] |
---|
| 816 | whd in ⊢ (??%?→?); |
---|
[2529] | 817 | #EQ destruct % |
---|
[2467] | 818 | qed. |
---|
| 819 | |
---|
[2481] | 820 | (* |
---|
[2476] | 821 | lemma bind_opt_non_none : ∀A,B : Type[0] . ∀ m : option A . ∀g : A → option B. |
---|
| 822 | (! x ← m ; g x) ≠ None ? → m ≠ None ?. |
---|
| 823 | #A #B #m #g #H % #m_eq_none cases m >m_eq_none in H; normalize |
---|
| 824 | [ #abs elim abs -abs #abs @abs % |
---|
| 825 | | #abs elim abs -abs #abs #v @abs % |
---|
| 826 | ] |
---|
| 827 | qed. |
---|
| 828 | |
---|
| 829 | lemma match_option_non_none : ∀A ,B, C : Type[0]. ∀m : option A. ∀ x : A. |
---|
| 830 | ∀ b : B .∀ f : A → B. ∀g : B → option C. |
---|
| 831 | g (match m with [None ⇒ b | Some x ⇒ f x])≠ None ? → g b = None ? → m ≠ None ?. |
---|
| 832 | #A #B #C #m #x #b #f #g #H1 #H2 % #m_eq_none >m_eq_none in H1; normalize #H elim H -H #H @H assumption |
---|
| 833 | qed. |
---|
[2481] | 834 | *) |
---|
[2476] | 835 | |
---|
[2529] | 836 | (* |
---|
[2481] | 837 | lemma funct_of_block_transf : |
---|
| 838 | ∀A,B.∀progr : program (λvars .fundef (A vars)) ℕ. |
---|
| 839 | ∀transf : ∀vars. A vars → B vars. ∀bl,f,prf. |
---|
| 840 | let progr' ≝ transform_program … progr (λvars.transf_fundef … (transf vars)) in |
---|
| 841 | funct_of_block … (globalenv_noinit … progr) bl = return f → |
---|
| 842 | funct_of_block … (globalenv_noinit … progr') bl = return «pi1 … f,prf». |
---|
| 843 | #A #B #progr #transf #bl #f #prf whd |
---|
| 844 | whd in match funct_of_block in ⊢ (%→?); normalize nodelta |
---|
| 845 | cut (∀A,B : Type[0].∀Q : option A → Prop.∀P : B → Prop. |
---|
| 846 | ∀o.∀prf : Q o. |
---|
| 847 | ∀f1,f2. |
---|
| 848 | (∀x,prf.P (f1 x prf)) → (∀prf.P(f2 prf)) → |
---|
| 849 | P (match o return λx.Q x → B with [ Some x ⇒ f1 x | None ⇒ f2 ] prf)) |
---|
| 850 | [ #A #B #Q #P * /2/ ] #aux |
---|
| 851 | @aux [2: #_ change with (?=Some ??→?) #ABS destruct(ABS) ] |
---|
| 852 | #fd #EQfind whd in ⊢ (??%%→?); |
---|
| 853 | generalize in ⊢ (??(??(????%))?→?); #e #EQ destruct(EQ) |
---|
| 854 | whd in match funct_of_block; normalize nodelta |
---|
| 855 | @aux [ # fd' ] |
---|
| 856 | [2: >(find_funct_ptr_transf … EQfind) #ABS destruct(ABS) ] |
---|
| 857 | #prf' cases daemon qed. |
---|
| 858 | |
---|
| 859 | lemma description_of_function_transf : |
---|
| 860 | ∀A,B.∀progr : program (λvars .fundef (A vars)) ℕ. |
---|
| 861 | ∀transf : ∀vars. A vars → B vars. |
---|
| 862 | let progr' ≝ transform_program … progr (λvars.transf_fundef … (transf vars)) in |
---|
| 863 | ∀f_out,prf. |
---|
| 864 | description_of_function … |
---|
| 865 | (globalenv_noinit … progr') f_out = |
---|
| 866 | transf_fundef … (transf ?) (description_of_function … (globalenv_noinit … progr) |
---|
| 867 | «pi1 … f_out, prf»). |
---|
| 868 | #A #B #progr #transf #f_out #prf |
---|
| 869 | whd in match description_of_function in ⊢ (???%); |
---|
| 870 | normalize nodelta |
---|
| 871 | cut (∀A,B : Type[0].∀Q : option A → Prop.∀P : B → Prop. |
---|
| 872 | ∀o.∀prf : Q o. |
---|
| 873 | ∀f1,f2. |
---|
| 874 | (∀x,prf.o = Some ? x → P (f1 x prf)) → (∀prf.o = None ? → P(f2 prf)) → |
---|
| 875 | P (match o return λx.Q x → B with [ Some x ⇒ f1 x | None ⇒ f2 ] prf)) |
---|
| 876 | [ #A #B #Q #P * /2/ ] #aux |
---|
| 877 | @aux |
---|
| 878 | [ #fd' ] * #fd #EQ destruct (EQ) |
---|
| 879 | inversion (find_symbol ???) [ #_ whd in ⊢ (??%?→?); #ABS destruct(ABS) ] |
---|
| 880 | #bl #EQfind >m_return_bind #EQfindf |
---|
| 881 | whd in match description_of_function; normalize nodelta |
---|
| 882 | @aux |
---|
| 883 | [ #fdo' ] * #fdo #EQ destruct (EQ) |
---|
| 884 | >find_symbol_transf >EQfind >m_return_bind |
---|
| 885 | >(find_funct_ptr_transf … EQfindf) #EQ destruct(EQ) % |
---|
| 886 | qed. |
---|
| 887 | |
---|
| 888 | |
---|
| 889 | lemma match_int_fun : |
---|
| 890 | ∀A,B : Type[0].∀P : B → Prop. |
---|
| 891 | ∀Q : fundef A → Prop. |
---|
| 892 | ∀m : fundef A. |
---|
| 893 | ∀f1 : ∀fd.Q (Internal \ldots fd) → B. |
---|
| 894 | ∀f2 : ∀fd.Q (External … fd) → B. |
---|
| 895 | ∀prf : Q m. |
---|
| 896 | (∀fd,prf.P (f1 fd prf)) → |
---|
| 897 | (∀fd,prf.P (f2 fd prf)) → |
---|
| 898 | P (match m |
---|
| 899 | return λx.Q x → ? |
---|
| 900 | with |
---|
| 901 | [ Internal fd ⇒ f1 fd |
---|
| 902 | | External fd ⇒ f2 fd |
---|
| 903 | ] prf). |
---|
| 904 | #A #B #P #Q * // qed. |
---|
| 905 | (*) |
---|
| 906 | lemma match_int_fun : |
---|
| 907 | ∀A,B : Type[0].∀P : B → Prop. |
---|
| 908 | ∀m : fundef A. |
---|
| 909 | ∀f1 : ∀fd.m = Internal … fd → B. |
---|
| 910 | ∀f2 : ∀fd.m = External … fd → B. |
---|
| 911 | (∀fd,prf.P (f1 fd prf)) → |
---|
| 912 | (∀fd,prf.P (f2 fd prf)) → |
---|
| 913 | P (match m |
---|
| 914 | return λx.m = x → ? |
---|
| 915 | with |
---|
| 916 | [ Internal fd ⇒ f1 fd |
---|
| 917 | | External fd ⇒ f2 fd |
---|
| 918 | ] (refl …)). |
---|
| 919 | #A #B #P * // qed. |
---|
| 920 | *) |
---|
| 921 | (* |
---|
| 922 | lemma prova : |
---|
| 923 | ∀ A.∀progr : program (λvars. fundef (A vars)) ℕ. |
---|
| 924 | ∀ M : fundef (A (prog_var_names (λvars:list ident.fundef (A vars)) ℕ progr)). |
---|
| 925 | ∀ f,g,prf1. |
---|
| 926 | match M return λx.M = x → option (Σi.is_internal_function_of_program ?? progr i) with |
---|
| 927 | [Internal fn ⇒ λ prf.return «g,prf1 fn prf» | |
---|
| 928 | External fn ⇒ λprf.None ? ] (refl ? M) = return f → |
---|
| 929 | ∃ fn. ∃ prf : M = Internal ? fn . f = «g, prf1 fn prf». |
---|
| 930 | #H1 #H2 #H3 #H4 #H5 #H6 |
---|
| 931 | @match_int_fun |
---|
| 932 | #fd #EQ #EQ' whd in EQ' : (??%%); destruct |
---|
| 933 | %[|%[| % ]] qed. |
---|
| 934 | *) |
---|
| 935 | |
---|
[2484] | 936 | lemma int_funct_of_block_transf: |
---|
[2476] | 937 | ∀A,B.∀progr: program (λvars. fundef (A vars)) ℕ. |
---|
| 938 | ∀transf: ∀vars. A vars → B vars. ∀bl,f,prf. |
---|
| 939 | let progr' ≝ transform_program … progr (λvars.transf_fundef … (transf vars)) in |
---|
| 940 | int_funct_of_block ? (globalenv_noinit … progr) bl = return f → |
---|
| 941 | int_funct_of_block ? (globalenv_noinit … progr') bl = return «pi1 … f,prf». |
---|
[2481] | 942 | #A #B #progr #transf #bl #f #prf |
---|
| 943 | whd whd in match int_funct_of_block in ⊢ (??%?→?); normalize nodelta |
---|
[2529] | 944 | @'bind_inversion #x #x_spec |
---|
[2481] | 945 | @match_int_fun [2: #fd #_ #ABS destruct(ABS) ] |
---|
| 946 | #fd #EQdescr change with (Some ?? = ? → ?) #EQ destruct(EQ) |
---|
| 947 | whd in match int_funct_of_block; normalize nodelta |
---|
| 948 | >(funct_of_block_transf … (internal_function_is_function … prf) … x_spec) |
---|
| 949 | >m_return_bind |
---|
| 950 | @match_int_fun #fd' #prf' [ % ] |
---|
| 951 | @⊥ cases x in prf EQdescr prf'; -x #x #x_prf #prf #EQdescr |
---|
| 952 | >(description_of_function_transf) [2: @x_prf ] |
---|
| 953 | >EQdescr whd in ⊢ (??%%→?); #ABS destruct qed. |
---|
[2529] | 954 | *) |
---|
[2476] | 955 | |
---|
[2553] | 956 | lemma symbol_for_block_match: |
---|
| 957 | ∀M:matching.∀initV,initW. |
---|
| 958 | (∀v,w. match_var_entry M v w → |
---|
| 959 | size_init_data_list (initV (\snd v)) = size_init_data_list (initW (\snd w))) → |
---|
| 960 | ∀p: program (m_A M) (m_V M). ∀p': program (m_B M) (m_W M). |
---|
| 961 | ∀MATCH:match_program … M p p'. |
---|
| 962 | ∀b: block. |
---|
| 963 | symbol_for_block … (globalenv … initW p') b = |
---|
| 964 | symbol_for_block … (globalenv … initV p) b. |
---|
| 965 | * #A #B #V #W #match_fn #match_var #initV #initW #H |
---|
| 966 | #p #p' * #Mvars #Mfn #Mmain |
---|
| 967 | #b |
---|
| 968 | whd in match symbol_for_block; normalize nodelta |
---|
| 969 | whd in match globalenv in ⊢ (???%); normalize nodelta |
---|
| 970 | whd in match (globalenv_allocmem ????); |
---|
| 971 | change with (add_globals ?????) in match (foldl ?????); |
---|
| 972 | >(proj1 … (add_globals_match … initW … Mvars)) |
---|
| 973 | [ % |*:] |
---|
| 974 | [ * #idr #v * #idr' #w #MVE % |
---|
| 975 | [ inversion MVE |
---|
| 976 | #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 destruct % |
---|
| 977 | | @(H … MVE) |
---|
| 978 | ] |
---|
| 979 | | @(matching_fns_get_same_blocks … Mfn) |
---|
| 980 | #f #g @match_funct_entry_id |
---|
| 981 | ] |
---|
| 982 | qed. |
---|
| 983 | |
---|
| 984 | lemma symbol_for_block_transf : |
---|
[2529] | 985 | ∀A,B,V,init.∀prog_in : program A V. |
---|
| 986 | ∀trans : ∀vars.A vars → B vars. |
---|
| 987 | let prog_out ≝ transform_program … prog_in trans in |
---|
[2553] | 988 | ∀bl. |
---|
| 989 | symbol_for_block … (globalenv … init prog_out) bl = |
---|
| 990 | symbol_for_block … (globalenv … init prog_in) bl. |
---|
| 991 | #A #B #V #iV #p #tf @(symbol_for_block_match … (transform_program_match … tf ?)) |
---|
| 992 | #v0 #w0 * // |
---|
| 993 | qed. |
---|
[2481] | 994 | |
---|
[2529] | 995 | lemma fetch_function_transf : |
---|
| 996 | ∀A,B,V,init.∀prog_in : program A V. |
---|
| 997 | ∀trans : ∀vars.A vars → B vars. |
---|
| 998 | let prog_out ≝ transform_program … prog_in trans in |
---|
| 999 | ∀bl,i,f. |
---|
| 1000 | fetch_function … (globalenv … init prog_in) bl = |
---|
| 1001 | return 〈i, f〉 |
---|
| 1002 | → fetch_function … (globalenv … init prog_out) bl = |
---|
| 1003 | return 〈i, trans … f〉. |
---|
| 1004 | #A #B #V #init #prog_in #trans #bl #i #f |
---|
[2476] | 1005 | whd in match fetch_function; normalize nodelta |
---|
[2529] | 1006 | #H lapply (opt_eq_from_res ???? H) -H |
---|
[2547] | 1007 | #H @('bind_inversion H) -H #id #eq_symbol_for_block |
---|
| 1008 | #H @('bind_inversion H) -H #fd #eq_find_funct |
---|
[2529] | 1009 | whd in ⊢ (??%?→?); #EQ destruct(EQ) |
---|
[2553] | 1010 | >(symbol_for_block_transf … trans) >eq_symbol_for_block >m_return_bind |
---|
[2547] | 1011 | >(find_funct_ptr_transf A B … eq_find_funct) % |
---|
[2476] | 1012 | qed. |
---|
[2529] | 1013 | |
---|
| 1014 | lemma fetch_internal_function_transf : |
---|
| 1015 | ∀A,B.∀prog_in : program (λvars.fundef (A vars)) ℕ. |
---|
| 1016 | ∀trans : ∀vars.A vars → B vars. |
---|
| 1017 | let prog_out ≝ transform_program … prog_in (λvars.transf_fundef … (trans vars)) in |
---|
| 1018 | ∀bl,i,f. |
---|
| 1019 | fetch_internal_function … (globalenv_noinit … prog_in) bl = |
---|
| 1020 | return 〈i, f〉 |
---|
| 1021 | → fetch_internal_function … (globalenv_noinit … prog_out) bl = |
---|
| 1022 | return 〈i, trans … f〉. |
---|
| 1023 | #A #B #prog #trans #bl #i #f |
---|
| 1024 | whd in match fetch_internal_function; normalize nodelta |
---|
[2547] | 1025 | #H @('bind_inversion H) * #id * #fd normalize nodelta #EQfetch |
---|
[2529] | 1026 | whd in ⊢ (??%%→?); #EQ destruct(EQ) |
---|
| 1027 | >(fetch_function_transf … EQfetch) % |
---|
| 1028 | qed. |
---|
[2476] | 1029 | |
---|
| 1030 | (* |
---|
[2467] | 1031 | #H elim (bind_opt_inversion ????? H) -H |
---|
| 1032 | #x * whd in match funct_of_block in ⊢ (%→?); normalize nodelta |
---|
| 1033 | @match_opt_prf_elim |
---|
| 1034 | #H #H1 whd in H : (??%?); |
---|
| 1035 | cases ( find_funct_ptr |
---|
| 1036 | (fundef |
---|
| 1037 | (joint_closed_internal_function |
---|
| 1038 | (graph_prog_params p p' graph_prog |
---|
[2808] | 1039 | (stack_sizes_lift (mk_sem_graph_params p p') (mk_sem_lin_params p p') |
---|
[2467] | 1040 | (linearise_int_fun p) graph_prog stack_sizes)) |
---|
| 1041 | (globals |
---|
| 1042 | (graph_prog_params p p' graph_prog |
---|
[2808] | 1043 | (stack_sizes_lift (mk_sem_graph_params p p') (mk_sem_lin_params p p') |
---|
[2467] | 1044 | (linearise_int_fun p) graph_prog stack_sizes))))) |
---|
| 1045 | (ev_genv |
---|
| 1046 | (graph_prog_params p p' graph_prog |
---|
[2808] | 1047 | (stack_sizes_lift (mk_sem_graph_params p p') (mk_sem_lin_params p p') |
---|
[2467] | 1048 | (linearise_int_fun p) graph_prog stack_sizes))) |
---|
[2808] | 1049 | (pblock (pc (mk_sem_graph_params p p') st))) in H; [ 2: normalize #abs destruct |
---|
[2467] | 1050 | |
---|
| 1051 | |
---|
| 1052 | normalize nodelta |
---|
| 1053 | #H #H1 |
---|
| 1054 | cases ( find_funct_ptr |
---|
| 1055 | (fundef |
---|
| 1056 | (joint_closed_internal_function |
---|
| 1057 | (graph_prog_params p p' graph_prog |
---|
[2808] | 1058 | (stack_sizes_lift (mk_sem_graph_params p p') (mk_sem_lin_params p p') |
---|
[2467] | 1059 | (linearise_int_fun p) graph_prog stack_sizes)) |
---|
| 1060 | (globals |
---|
| 1061 | (graph_prog_params p p' graph_prog |
---|
[2808] | 1062 | (stack_sizes_lift (mk_sem_graph_params p p') (mk_sem_lin_params p p') |
---|
[2467] | 1063 | (linearise_int_fun p) graph_prog stack_sizes))))) |
---|
| 1064 | (ev_genv |
---|
| 1065 | (graph_prog_params p p' graph_prog |
---|
[2808] | 1066 | (stack_sizes_lift (mk_sem_graph_params p p') (mk_sem_lin_params p p') |
---|
[2467] | 1067 | (linearise_int_fun p) graph_prog stack_sizes))) |
---|
[2808] | 1068 | (pblock (pc (mk_sem_graph_params p p') st))) in H; |
---|
[2467] | 1069 | |
---|
| 1070 | |
---|
| 1071 | check find_funct_ptr_transf |
---|
| 1072 | whd in match int_funct_of_block; normalize nodelta |
---|
| 1073 | #H elim (bind_inversion ????? H) |
---|
| 1074 | |
---|
| 1075 | .. sigma_int_funct_of_block |
---|
| 1076 | |
---|
| 1077 | |
---|
| 1078 | |
---|
| 1079 | whd in match int_funct_of_block; normalize nodelta |
---|
| 1080 | elim (bind_inversion ????? H) |
---|
| 1081 | whd in match int_funct_of_block; normalize nodelta |
---|
[2464] | 1082 | #H elim (bind_inversion ????? H) -H #fn * |
---|
| 1083 | #H lapply (opt_eq_from_res ???? H) -H |
---|
| 1084 | #H >(find_funct_ptr_transf … (λglobals.transf_fundef … (linearise_int_fun … globals)) … H) |
---|
| 1085 | -H #H >m_return_bind cases fn in H; normalize nodelta #arg #EQ whd in EQ:(??%%); |
---|
[2476] | 1086 | destruct // |
---|
[2464] | 1087 | cases daemon |
---|
[2476] | 1088 | qed. *) |
---|
[2446] | 1089 | |
---|
[2464] | 1090 | lemma stmt_at_sigma_commute: |
---|
[2529] | 1091 | ∀p,globals,graph_code,entry,lin_code,lbl,pt,sigma. |
---|
| 1092 | good_local_sigma p globals graph_code entry lin_code sigma → |
---|
[2551] | 1093 | code_closed … lin_code → |
---|
[2529] | 1094 | sigma lbl = return pt → |
---|
[2476] | 1095 | ∀stmt. |
---|
[2529] | 1096 | stmt_at … graph_code |
---|
[2476] | 1097 | lbl = return stmt → |
---|
[2529] | 1098 | All … (λl.sigma l ≠ None ?) (stmt_labels … stmt) ∧ |
---|
| 1099 | match stmt with |
---|
[2543] | 1100 | [ final s' ⇒ stmt_at … lin_code pt = Some ? (final … s') |
---|
| 1101 | | sequential s' nxt ⇒ |
---|
| 1102 | match s' with |
---|
| 1103 | [ step_seq _ ⇒ |
---|
| 1104 | (stmt_at … lin_code pt = Some ? (sequential … s' it)) ∧ |
---|
| 1105 | ((sigma nxt = Some ? (S pt)) ∨ |
---|
[2551] | 1106 | (stmt_at … lin_code (S pt) = Some ? (GOTO … nxt) ∧ |
---|
| 1107 | point_of_label … lin_code nxt = sigma nxt) ) |
---|
[2543] | 1108 | | COND a ltrue ⇒ |
---|
| 1109 | (stmt_at … lin_code pt = Some ? (sequential … s' it) ∧ |
---|
| 1110 | sigma nxt = Some ? (S pt)) ∨ |
---|
[2551] | 1111 | (stmt_at … lin_code pt = Some ? (FCOND … I a ltrue nxt) ∧ |
---|
| 1112 | point_of_label … lin_code nxt = sigma nxt) |
---|
[2543] | 1113 | ] |
---|
| 1114 | | FCOND abs _ _ _ ⇒ Ⓧabs |
---|
[2529] | 1115 | ]. |
---|
| 1116 | #p #globals #graph_code #entry #lin_code #lbl #pt #sigma |
---|
[2551] | 1117 | ** #_ #all_labels_in #lin_stmt_spec #lin_code_closed #prf |
---|
[2543] | 1118 | elim (lin_stmt_spec … prf) -lin_stmt_spec #stmt1 ** #stmt1_spec |
---|
[2529] | 1119 | #All_succs_in #next_spec |
---|
[2543] | 1120 | #stmt >stmt1_spec #EQ whd in EQ : (???%); destruct(EQ) |
---|
| 1121 | % [assumption] |
---|
[2551] | 1122 | cases stmt in next_spec; -stmt |
---|
| 1123 | [ * [ #s | #a #lbl ] #nxt | #s | * ] |
---|
| 1124 | normalize nodelta |
---|
| 1125 | [ * #H #G %{H} |
---|
| 1126 | cases G -G #G |
---|
| 1127 | [ %1{G} ] |
---|
| 1128 | | * [ #H %1{H} ] #G |
---|
| 1129 | | // |
---|
| 1130 | ] %2 %{G} |
---|
| 1131 | lapply (refl … (point_of_label … lin_code nxt)) |
---|
| 1132 | change with (If ? then with prf do ? else ?) in ⊢ (???%→?); |
---|
| 1133 | @If_elim <(lin_code_has_label … (mk_lin_params p)) |
---|
| 1134 | [1,3: #_ #EQ >EQ >(all_labels_in … EQ) % ] |
---|
| 1135 | * #H cases (H ?) -H |
---|
| 1136 | lapply (lin_code_closed … G) ** [2: #_ * ] // |
---|
[2484] | 1137 | qed. |
---|
[2547] | 1138 | |
---|
[2484] | 1139 | (* |
---|
| 1140 | |
---|
| 1141 | >(if_of_function_commute … graph_fun) |
---|
| 1142 | |
---|
| 1143 | check opt_Exists |
---|
| 1144 | check linearise_int_fun |
---|
| 1145 | check |
---|
[2464] | 1146 | whd in match (stmt_at ????); |
---|
| 1147 | whd in match (stmt_at ????); |
---|
| 1148 | cases (linearise_code_spec … p' graph_prog graph_fun |
---|
| 1149 | (joint_if_entry … graph_fun)) |
---|
| 1150 | * #lin_code_closed #sigma_entry_is_zero #sigma_spec |
---|
| 1151 | lapply (sigma_spec |
---|
| 1152 | (point_of_pointer ? (graph_prog_params … p' graph_prog) (pc … s1))) |
---|
| 1153 | -sigma_spec #sigma_spec cases (sigma_spec ??) [3: @(sigma_pc_of_status_ok … prf) |2: skip ] |
---|
| 1154 | -sigma_spec #graph_stmt * #graph_lookup_ok >graph_lookup_ok -graph_lookup_ok |
---|
| 1155 | whd in ⊢ (? → ???%); #sigma_spec whd in sigma_spec; |
---|
| 1156 | inversion (nth_opt ???) in sigma_spec; [ #H whd in ⊢ (% → ?); #abs cases abs ] |
---|
| 1157 | * #optlabel #lin_stm #lin_lookup_ok whd in ⊢ (% → ?); ** #_ |
---|
| 1158 | #related_lin_stm_graph_stm #_ <related_lin_stm_graph_stm -related_lin_stm_graph_stm |
---|
| 1159 | <sigma_pc_commute >lin_lookup_ok // *) |
---|
| 1160 | |
---|
[2529] | 1161 | definition good_sigma : |
---|
| 1162 | ∀p.∀graph_prog : joint_program (mk_graph_params p). |
---|
| 1163 | (joint_closed_internal_function ? (prog_var_names … graph_prog) → |
---|
| 1164 | label → option ℕ) → Prop ≝ |
---|
| 1165 | λp,graph_prog,sigma. |
---|
| 1166 | ∀fn : joint_closed_internal_function (mk_graph_params p) ?. |
---|
| 1167 | good_local_sigma ?? (joint_if_code … fn) (joint_if_entry … fn) |
---|
| 1168 | (joint_if_code … (\fst (linearise_int_fun … fn))) (sigma fn). |
---|
| 1169 | |
---|
| 1170 | lemma pc_of_label_sigma_commute : |
---|
[2547] | 1171 | ∀p,p',graph_prog,bl,lbl,i,fn. |
---|
[2529] | 1172 | let lin_prog ≝ linearise ? graph_prog in |
---|
| 1173 | ∀sigma.good_sigma p graph_prog sigma → |
---|
| 1174 | fetch_internal_function … |
---|
[2547] | 1175 | (globalenv_noinit … graph_prog) bl = return 〈i, fn〉 → |
---|
[2808] | 1176 | let pc' ≝ pc_of_point (mk_sem_graph_params p p') … bl lbl in |
---|
[2529] | 1177 | code_has_label … (joint_if_code … (\fst (linearise_int_fun … fn))) lbl → |
---|
[2808] | 1178 | ∃prf'.pc_of_label (mk_sem_lin_params p p') … (globalenv_noinit … lin_prog) |
---|
[2547] | 1179 | bl lbl = |
---|
[2529] | 1180 | return sigma_pc p p' graph_prog sigma pc' prf'. |
---|
[2547] | 1181 | #p #p' #graph_prog #bl #lbl #i #fn |
---|
[2529] | 1182 | #sigma #good cases (good fn) -good * #_ #all_labels_in |
---|
[2547] | 1183 | #good #fetchfn >lin_code_has_label #lbl_in |
---|
[2529] | 1184 | whd in match pc_of_label; normalize nodelta |
---|
| 1185 | > (fetch_internal_function_transf … fetchfn) >m_return_bind |
---|
| 1186 | inversion (point_of_label ????) |
---|
| 1187 | [ (* |
---|
| 1188 | change with (If ? then with prf do ? else ? = ? → ?) |
---|
| 1189 | @If_elim [ #prf' whd in ⊢ (??%?→?); #ABS destruct(ABS) | #ABS >ABS in lbl_in; * ] |
---|
| 1190 | *) whd in ⊢ (??%?→?); >lbl_in whd in ⊢ (??%?→?); #ABS destruct(ABS) |
---|
| 1191 | | #pt #H lapply (all_labels_in … H) #EQsigma >m_return_bind |
---|
| 1192 | % |
---|
| 1193 | [ @hide_prf whd % |
---|
| 1194 | | whd in match sigma_pc; normalize nodelta |
---|
| 1195 | @opt_safe_elim #pc' |
---|
| 1196 | ] |
---|
[2551] | 1197 | whd in match sigma_pc_opt; normalize nodelta |
---|
| 1198 | @eqZb_elim #Hbl normalize nodelta |
---|
| 1199 | [1,3: >(fetch_internal_function_no_minus_one … Hbl) in fetchfn; |
---|
| 1200 | |*: >fetchfn >m_return_bind |
---|
| 1201 | >point_of_pc_of_point |
---|
| 1202 | >EQsigma |
---|
| 1203 | ] whd in ⊢ (??%%→?); #EQ destruct(EQ) % |
---|
[2529] | 1204 | ] |
---|
| 1205 | qed. |
---|
| 1206 | |
---|
| 1207 | lemma graph_pc_of_label : |
---|
| 1208 | ∀p,p'.let pars ≝ make_sem_graph_params p p' in |
---|
| 1209 | ∀globals,ge,bl,i_fn,lbl. |
---|
| 1210 | fetch_internal_function ? ge bl = return i_fn → |
---|
| 1211 | pc_of_label pars globals ge bl lbl = |
---|
| 1212 | OK ? (pc_of_point pars bl lbl). |
---|
| 1213 | #p #p' #globals #ge #bl #fn #lbl #fetchfn |
---|
| 1214 | whd in match pc_of_label; normalize nodelta |
---|
| 1215 | >fetchfn % |
---|
| 1216 | qed. |
---|
| 1217 | |
---|
[2551] | 1218 | lemma point_of_pc_sigma_commute : |
---|
| 1219 | ∀p,p',graph_prog. |
---|
| 1220 | let lin_prog ≝ linearise p graph_prog in |
---|
| 1221 | ∀sigma,pc,f,fn,n. |
---|
| 1222 | ∀prf : well_formed_pc p p' graph_prog sigma pc. |
---|
| 1223 | fetch_internal_function … (globalenv_noinit … graph_prog) (pc_block pc) = return 〈f, fn〉 → |
---|
[2808] | 1224 | sigma fn (point_of_pc (mk_sem_graph_params p p') pc) = return n → |
---|
| 1225 | point_of_pc (mk_sem_lin_params p p') (sigma_pc … pc prf) = n. |
---|
[2551] | 1226 | #p #p' #graph_prog #sigma #pc #f #fn #n #prf #EQfetch #EQsigma |
---|
| 1227 | whd in match sigma_pc; normalize nodelta |
---|
| 1228 | @opt_safe_elim #pc' whd in match sigma_pc_opt; |
---|
| 1229 | normalize nodelta @eqZb_elim #Hbl |
---|
| 1230 | [ >(fetch_internal_function_no_minus_one … Hbl) in EQfetch; |
---|
| 1231 | whd in ⊢ (???%→?); #ABS destruct(ABS) ] |
---|
| 1232 | >EQfetch >m_return_bind >EQsigma |
---|
| 1233 | whd in ⊢ (??%%→?); #EQ destruct(EQ) |
---|
| 1234 | @point_of_offset_of_point |
---|
| 1235 | qed. |
---|
| 1236 | |
---|
[2529] | 1237 | lemma graph_succ_pc : |
---|
| 1238 | ∀p,p'.let pars ≝ make_sem_graph_params p p' in |
---|
| 1239 | ∀pc,lbl. |
---|
| 1240 | succ_pc pars pc lbl = pc_of_point pars (pc_block pc) lbl. |
---|
| 1241 | normalize // |
---|
| 1242 | qed. |
---|
[2553] | 1243 | |
---|
[2464] | 1244 | lemma fetch_statement_sigma_commute: |
---|
[2529] | 1245 | ∀p,p',graph_prog,pc,f,fn,stmt. |
---|
[2464] | 1246 | let lin_prog ≝ linearise ? graph_prog in |
---|
[2476] | 1247 | ∀sigma.good_sigma p graph_prog sigma → |
---|
[2481] | 1248 | ∀prf : well_formed_pc p p' graph_prog sigma pc. |
---|
[2808] | 1249 | fetch_statement (mk_sem_graph_params p p') … |
---|
[2529] | 1250 | (globalenv_noinit ? graph_prog) pc = return 〈f, fn,stmt〉 → |
---|
[2553] | 1251 | All ? (λlbl.∃prf:well_formed_pc p p' graph_prog sigma |
---|
[2808] | 1252 | (pc_of_point (mk_sem_graph_params p p') (pc_block pc) lbl). |
---|
| 1253 | pc_of_label (mk_sem_lin_params p p') … |
---|
[2548] | 1254 | (globalenv_noinit … lin_prog) |
---|
| 1255 | (pc_block pc) |
---|
| 1256 | lbl = return sigma_pc … prf) |
---|
[2553] | 1257 | (stmt_explicit_labels … stmt) ∧ |
---|
[2529] | 1258 | match stmt with |
---|
[2543] | 1259 | [ sequential s nxt ⇒ |
---|
| 1260 | match s with |
---|
| 1261 | [ step_seq x ⇒ |
---|
[2808] | 1262 | fetch_statement (mk_sem_lin_params p p') … |
---|
[2543] | 1263 | (globalenv_noinit … lin_prog) (sigma_pc … pc prf) = |
---|
| 1264 | return 〈f, \fst (linearise_int_fun … fn), |
---|
| 1265 | sequential (mk_lin_params p) … (step_seq … x ) it〉 ∧ |
---|
| 1266 | ∃prf'. |
---|
[2808] | 1267 | let sigma_nxt ≝ sigma_pc p p' graph_prog sigma (succ_pc (mk_sem_graph_params p p') pc nxt) prf' in |
---|
| 1268 | let nxt_pc ≝ succ_pc (mk_sem_lin_params p p') (sigma_pc … pc prf) it in |
---|
[2548] | 1269 | (nxt_pc = sigma_nxt ∨ |
---|
[2808] | 1270 | (fetch_statement (mk_sem_lin_params p p') … |
---|
[2548] | 1271 | (globalenv_noinit … lin_prog) nxt_pc = |
---|
| 1272 | return 〈f, \fst (linearise_int_fun … fn), |
---|
| 1273 | final (mk_lin_params p) … (GOTO … nxt)〉 ∧ |
---|
[2808] | 1274 | (pc_of_label (mk_sem_lin_params p p') … |
---|
[2548] | 1275 | (globalenv_noinit … lin_prog) |
---|
| 1276 | (pc_block pc) |
---|
| 1277 | nxt = return sigma_nxt))) |
---|
[2543] | 1278 | | COND a ltrue ⇒ |
---|
[2548] | 1279 | ∃prf'. |
---|
[2808] | 1280 | let sigma_nxt ≝ sigma_pc p p' graph_prog sigma (succ_pc (mk_sem_graph_params p p') pc nxt) prf' in |
---|
[2548] | 1281 | (let nxt_pc ≝ succ_pc (make_sem_lin_params p p') (sigma_pc … pc prf) it in |
---|
[2808] | 1282 | (fetch_statement (mk_sem_lin_params p p') … |
---|
[2543] | 1283 | (globalenv_noinit … lin_prog) (sigma_pc … pc prf) = |
---|
| 1284 | return 〈f, \fst (linearise_int_fun … fn), |
---|
| 1285 | sequential (mk_lin_params p) … (COND … a ltrue) it〉 ∧ |
---|
[2548] | 1286 | nxt_pc = sigma_nxt)) ∨ |
---|
[2808] | 1287 | (fetch_statement (mk_sem_lin_params p p') … (globalenv_noinit … lin_prog) (sigma_pc … pc prf) |
---|
[2543] | 1288 | = |
---|
[2548] | 1289 | return 〈f, \fst (linearise_int_fun … fn), FCOND (mk_lin_params p) … I a ltrue nxt〉 ∧ |
---|
[2808] | 1290 | pc_of_label (mk_sem_lin_params p p') … |
---|
[2548] | 1291 | (globalenv_noinit … lin_prog) |
---|
| 1292 | (pc_block pc) |
---|
| 1293 | nxt = return sigma_nxt) |
---|
[2543] | 1294 | ] |
---|
[2808] | 1295 | | final z ⇒ fetch_statement (mk_sem_lin_params p p') … |
---|
[2543] | 1296 | (globalenv_noinit … lin_prog) (sigma_pc … pc prf) = |
---|
| 1297 | return 〈f, \fst (linearise_int_fun … fn), final (mk_lin_params p) … z〉 |
---|
| 1298 | | FCOND abs _ _ _ ⇒ Ⓧabs |
---|
[2529] | 1299 | ]. |
---|
[2543] | 1300 | #p #p' #graph_prog #pc #f #fn #stmt #sigma |
---|
| 1301 | #good elim (good fn) * #_ #all_labels_in #good_local #wfprf |
---|
| 1302 | #H elim (fetch_statement_inv … H) #fetchfn #graph_stmt |
---|
| 1303 | whd in match well_formed_pc in wfprf; normalize nodelta in wfprf; |
---|
| 1304 | inversion(sigma_pc_opt p p' graph_prog sigma pc) |
---|
| 1305 | [#ABS @⊥ >ABS in wfprf; * #H @H %] |
---|
[2551] | 1306 | #lin_pc |
---|
| 1307 | whd in match sigma_pc_opt in ⊢ (%→?); normalize nodelta in ⊢ (%→?); |
---|
| 1308 | @eqZb_elim #Hbl |
---|
| 1309 | [ >(fetch_internal_function_no_minus_one … Hbl) in fetchfn; #ABS destruct(ABS) ] |
---|
| 1310 | normalize nodelta >fetchfn >m_return_bind |
---|
| 1311 | #H @('bind_inversion H) -H |
---|
[2543] | 1312 | #lin_pt #lin_pt_spec #EQ whd in EQ : (??%?); destruct(EQ) |
---|
[2551] | 1313 | lapply(stmt_at_sigma_commute ???????? (good fn) ??? graph_stmt) |
---|
[2553] | 1314 | [@lin_pt_spec|@(pi2 … (\fst (linearise_int_fun … fn)))|] * #H1 #H2 % |
---|
| 1315 | [ cases stmt in H2; |
---|
| 1316 | [ * [#s|#a#lbl]#nxt | #s | *] |
---|
| 1317 | normalize nodelta |
---|
| 1318 | [ * #stmt_at_EQ #_ | ** #stmt_at_EQ #_ | #stmt_at_EQ ] |
---|
| 1319 | cases (pi2 … (\fst (linearise_int_fun … fn)) … stmt_at_EQ) |
---|
| 1320 | #H #_ |
---|
| 1321 | [1,2,4: @(All_mp … H) #lbl @(pc_of_label_sigma_commute … good … fetchfn) |
---|
| 1322 | |3: cases H -H #H #_ %{I} @(pc_of_label_sigma_commute … good … fetchfn) @H |
---|
| 1323 | ] |
---|
| 1324 | ] |
---|
| 1325 | cases (stmt) in H1 H2; [ * [ #s | #a #ltrue ] #nxt | #s | * ] normalize nodelta |
---|
[2543] | 1326 | #all_labels_spec #H3 whd in match fetch_statement; normalize nodelta |
---|
[2551] | 1327 | >pc_block_sigma_commute |
---|
[2529] | 1328 | >(fetch_internal_function_transf … fetchfn) >m_return_bind |
---|
[2551] | 1329 | >(point_of_pc_sigma_commute … fetchfn lin_pt_spec) |
---|
[2543] | 1330 | [ % |
---|
[2551] | 1331 | [ >(proj1 … H3) % |
---|
| 1332 | | % [ @hide_prf % |
---|
| 1333 | | change with (opt_safe ???) in match (sigma_pc ???? (succ_pc ???) ?); |
---|
| 1334 | @opt_safe_elim #pc1 |
---|
| 1335 | ] whd in match sigma_pc_opt; |
---|
| 1336 | normalize nodelta >(eqZb_false … Hbl) >fetchfn |
---|
| 1337 | >m_return_bind |
---|
| 1338 | >graph_succ_pc >point_of_pc_of_point |
---|
| 1339 | cases(proj2 … H3) |
---|
| 1340 | [1,3: #EQ >EQ |
---|
| 1341 | |*: * cases all_labels_spec #Z #_ #sn |
---|
| 1342 | >(opt_to_opt_safe … Z) #EQpoint_of_label |
---|
| 1343 | ] whd in ⊢ (??%?→?); #EQ destruct(EQ) |
---|
| 1344 | [ %1 |
---|
| 1345 | whd in match (point_of_succ ???) ; |
---|
| 1346 | whd in match point_of_pc; normalize nodelta |
---|
| 1347 | whd in match sigma_pc; whd in match sigma_pc_opt; normalize nodelta |
---|
| 1348 | @opt_safe_elim >(eqZb_false … Hbl) >fetchfn >m_return_bind |
---|
| 1349 | >lin_pt_spec #pc' whd in ⊢ (??%%→?); #EQ destruct(EQ) |
---|
| 1350 | whd in match succ_pc; whd in match point_of_pc; normalize nodelta |
---|
[2543] | 1351 | >point_of_offset_of_point % |
---|
[2551] | 1352 | | %2 whd in match (pc_block ?); >pc_block_sigma_commute |
---|
| 1353 | >(fetch_internal_function_transf … fetchfn) >m_return_bind |
---|
| 1354 | whd in match sigma_pc; whd in match sigma_pc_opt; normalize nodelta |
---|
| 1355 | @opt_safe_elim >(eqZb_false … Hbl) normalize nodelta |
---|
| 1356 | #pc_lin >fetchfn >m_return_bind >lin_pt_spec >m_return_bind |
---|
| 1357 | whd in match pc_of_point; normalize nodelta #EQ whd in EQ : (??%?); destruct |
---|
| 1358 | whd in match point_of_pc; whd in match succ_pc; normalize nodelta |
---|
| 1359 | whd in match point_of_pc; normalize nodelta >point_of_offset_of_point |
---|
| 1360 | whd in match pc_of_point; normalize nodelta >point_of_offset_of_point |
---|
| 1361 | >sn >m_return_bind % [%] whd in match pc_of_label; normalize nodelta |
---|
| 1362 | >(fetch_internal_function_transf … fetchfn) >m_return_bind |
---|
| 1363 | >EQpoint_of_label % |
---|
| 1364 | ] |
---|
[2543] | 1365 | ] |
---|
[2551] | 1366 | | % [ @hide_prf % whd in match sigma_pc_opt; normalize nodelta |
---|
| 1367 | >(eqZb_false … Hbl) normalize nodelta whd in match (pc_block ?); >fetchfn |
---|
| 1368 | >m_return_bind whd in match point_of_pc; whd in match succ_pc; normalize nodelta |
---|
| 1369 | whd in match pc_of_point; whd in match point_of_pc; normalize nodelta |
---|
| 1370 | >point_of_offset_of_point cases all_labels_spec #H >(opt_to_opt_safe … H) #_ |
---|
| 1371 | >m_return_bind #ABS whd in ABS : (??%?); destruct(ABS)] |
---|
| 1372 | cases H3 * #nxt_spec #point_of_lab_spec >nxt_spec >m_return_bind |
---|
| 1373 | [%1 % [%] whd in match sigma_pc; whd in match sigma_pc_opt; normalize nodelta |
---|
| 1374 | @opt_safe_elim #lin_pc1 @opt_safe_elim #lin_pc2 |
---|
| 1375 | >(eqZb_false … Hbl) normalize nodelta >fetchfn >m_return_bind |
---|
| 1376 | >m_return_bind in ⊢ (? → % → ?); whd in match point_of_pc; whd in match succ_pc; |
---|
| 1377 | normalize nodelta whd in match pc_of_point; whd in match point_of_pc; normalize nodelta |
---|
| 1378 | >point_of_offset_of_point >point_of_lab_spec >m_return_bind #EQ |
---|
| 1379 | whd in EQ : (??%?); destruct(EQ) >lin_pt_spec >m_return_bind #EQ |
---|
| 1380 | whd in EQ : (??%?); destruct(EQ) >point_of_offset_of_point % |
---|
| 1381 | |%2 >m_return_bind >nxt_spec >m_return_bind %[%] whd in match pc_of_label; |
---|
| 1382 | normalize nodelta >(fetch_internal_function_transf … fetchfn) |
---|
| 1383 | >m_return_bind >point_of_lab_spec cases all_labels_spec #H #INUTILE |
---|
| 1384 | >(opt_to_opt_safe … H) in ⊢ (??%?); >m_return_bind |
---|
| 1385 | normalize in ⊢ (??%?); |
---|
| 1386 | whd in match sigma_pc; whd in match sigma_pc_opt; normalize nodelta |
---|
| 1387 | @opt_safe_elim >(eqZb_false … Hbl) normalize nodelta whd in match (pc_block ?); |
---|
[2543] | 1388 | >fetchfn >m_return_bind whd in match point_of_pc; whd in match succ_pc; |
---|
[2551] | 1389 | normalize nodelta whd in match point_of_pc; whd in match pc_of_point; |
---|
| 1390 | normalize nodelta >point_of_offset_of_point cases (sigma fn nxt) in H; |
---|
| 1391 | [ * #ABS @⊥ @ABS %] #linear_point * #INUTILE1 #linear_pc >m_return_bind |
---|
| 1392 | #EQ whd in EQ : (??%?); destruct(EQ) normalize nodelta % |
---|
| 1393 | ] |
---|
| 1394 | | >H3 >m_return_bind % |
---|
| 1395 | ] |
---|
[2553] | 1396 | qed. |
---|
[2464] | 1397 | |
---|
[2570] | 1398 | (* |
---|
| 1399 | spostato in ExtraMonads.ma |
---|
[2551] | 1400 | |
---|
| 1401 | lemma res_eq_from_opt : ∀A,m,a. |
---|
| 1402 | res_to_opt A m = return a → m = return a. |
---|
| 1403 | #A #m #a cases m #x normalize #EQ destruct(EQ) % |
---|
[2484] | 1404 | qed. |
---|
| 1405 | |
---|
[2553] | 1406 | lemma res_to_opt_preserve : ∀X,Y,P,F,m,n. |
---|
| 1407 | res_preserve X Y P F m n → opt_preserve X Y P F (res_to_opt … m) (res_to_opt … n). |
---|
| 1408 | #X #Y #P #F #m #n #H #x #EQ |
---|
| 1409 | cases (H x ?) |
---|
| 1410 | [ #prf #EQ' %{prf} >EQ' % |
---|
| 1411 | | cases m in EQ; normalize #x #EQ destruct % |
---|
| 1412 | ] |
---|
| 1413 | qed. |
---|
[2570] | 1414 | *) |
---|
[2553] | 1415 | lemma sigma_pc_exit : |
---|
| 1416 | ∀p,p',graph_prog,sigma,pc,prf. |
---|
| 1417 | let exit ≝ mk_program_counter «mk_block Code (-1), refl …» one in |
---|
| 1418 | pc = exit → |
---|
| 1419 | sigma_pc p p' graph_prog sigma pc prf = exit. |
---|
| 1420 | #p #p' #graph_prog #sigma #pc #prf |
---|
| 1421 | whd in match sigma_pc; normalize nodelta @opt_safe_elim #pc' |
---|
| 1422 | #EQ1 #EQ2 destruct |
---|
| 1423 | whd in match sigma_pc_opt in EQ1; whd in EQ1 : (??%?); |
---|
| 1424 | destruct % |
---|
| 1425 | qed. |
---|
| 1426 | |
---|
| 1427 | (* this should make things easier for ops using memory (where pc cant happen) *) |
---|
| 1428 | definition bv_no_pc : beval → Prop ≝ |
---|
| 1429 | λbv.match bv with [ BVpc _ _ ⇒ False | _ ⇒ True ]. |
---|
| 1430 | |
---|
| 1431 | lemma bv_pc_other : |
---|
| 1432 | ∀P : beval → Prop. |
---|
| 1433 | (∀pc,p.P (BVpc pc p)) → |
---|
| 1434 | (∀bv.bv_no_pc bv → P bv) → |
---|
| 1435 | ∀bv.P bv. |
---|
| 1436 | #P #H1 #H2 * /2/ qed. |
---|
| 1437 | |
---|
| 1438 | lemma sigma_bv_no_pc : ∀p,p',graph_prog,sigma,bv,prf. |
---|
| 1439 | bv_no_pc bv → |
---|
| 1440 | sigma_beval p p' graph_prog sigma bv prf = bv. |
---|
| 1441 | #p #p' #graph_prog #sigma * |
---|
| 1442 | [|| #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc #p ] |
---|
| 1443 | #prf * whd in match sigma_beval; normalize nodelta |
---|
| 1444 | @opt_safe_elim #bv' normalize #EQ destruct(EQ) % |
---|
| 1445 | qed. |
---|
| 1446 | |
---|
| 1447 | lemma bv_no_pc_wf : ∀p,p',graph_prog,sigma,bv. |
---|
| 1448 | bv_no_pc bv → sigma_beval_opt p p' graph_prog sigma bv ≠ None ?. |
---|
| 1449 | #p #p' #graph_prog #sigma * |
---|
| 1450 | [|| #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc #p ] * |
---|
| 1451 | % whd in ⊢ (??%?→?); #ABS destruct(ABS) qed. |
---|
| 1452 | |
---|
| 1453 | lemma Byte_of_val_inv : ∀bv,e,by.Byte_of_val e bv = return by → bv = BVByte by. |
---|
| 1454 | * [|| #a #b #c |#p | #p | #p #pa | #p #pa ] #e #by |
---|
| 1455 | whd in ⊢ (??%%→?); #EQ destruct(EQ) % qed. |
---|
| 1456 | |
---|
| 1457 | lemma sigma_pc_no_exit : |
---|
| 1458 | ∀p,p',graph_prog,sigma,pc,prf. |
---|
| 1459 | let exit ≝ mk_program_counter «mk_block Code (-1), refl …» one in |
---|
| 1460 | pc ≠ exit → |
---|
| 1461 | sigma_pc p p' graph_prog sigma pc prf ≠ exit. |
---|
| 1462 | #p #p' #graph_prog #sigma #pc #prf |
---|
| 1463 | @(eqZb_elim (block_id (pc_block pc)) (-1)) |
---|
| 1464 | [ #Hbl |
---|
| 1465 | whd in match sigma_pc; normalize nodelta @opt_safe_elim #pc' |
---|
| 1466 | whd in match sigma_pc_opt; normalize nodelta |
---|
| 1467 | >Hbl whd in ⊢ (??%?→?); #EQ destruct(EQ) // ] |
---|
| 1468 | #NEQ #_ inversion (sigma_pc ??????) |
---|
| 1469 | ** #r #id #EQr #off #EQ |
---|
| 1470 | lapply (pc_block_sigma_commute …prf) >EQ #EQ' >EQ' |
---|
| 1471 | % #ABS destruct(ABS) cases NEQ #H @H -H |
---|
| 1472 | cases (pc_block ?) in e0; * #r #id' #EQ'' >EQ'' #EQ''' destruct(EQ''') % |
---|
| 1473 | qed. |
---|
| 1474 | |
---|
[2442] | 1475 | definition linearise_status_rel: |
---|
| 1476 | ∀p,p',graph_prog. |
---|
[2464] | 1477 | let lin_prog ≝ linearise p graph_prog in |
---|
[2529] | 1478 | ∀stack_sizes. |
---|
[2551] | 1479 | ∀sigma. ∀ gss : good_state_sigma p p' graph_prog sigma. |
---|
[2476] | 1480 | good_sigma p graph_prog sigma → |
---|
[2442] | 1481 | status_rel |
---|
[2529] | 1482 | (graph_abstract_status p p' graph_prog stack_sizes) |
---|
[2464] | 1483 | (lin_abstract_status p p' lin_prog stack_sizes) |
---|
[2484] | 1484 | ≝ λp,p',graph_prog,stack_sizes,sigma,gss,good. |
---|
[2464] | 1485 | mk_status_rel … |
---|
| 1486 | (* sem_rel ≝ *) (λs1,s2. |
---|
[2484] | 1487 | ∃prf: well_formed_state_pc p p' graph_prog sigma gss s1. |
---|
| 1488 | s2 = sigma_state_pc … s1 prf) |
---|
[2464] | 1489 | (* call_rel ≝ *) (λs1,s2. |
---|
[2484] | 1490 | ∃prf:well_formed_state_pc p p' graph_prog sigma gss s1. |
---|
[2556] | 1491 | pc ? s2 = sigma_pc … (pc ? s1) (proj2 … (proj1 … prf))) |
---|
[2464] | 1492 | (* sim_final ≝ *) ?. |
---|
| 1493 | #st1 #st2 * #prf #EQ2 |
---|
[2551] | 1494 | % [2: cases daemon] |
---|
| 1495 | >EQ2 |
---|
[2464] | 1496 | whd in ⊢ (%→%); |
---|
| 1497 | #H lapply (opt_to_opt_safe … H) |
---|
[2551] | 1498 | @opt_safe_elim -H #res #_ whd in match is_final; normalize nodelta |
---|
| 1499 | #H lapply(res_eq_from_opt ??? H) -H |
---|
[2543] | 1500 | #H @('bind_inversion H) -H |
---|
[2551] | 1501 | ** #id #int_f #stmt |
---|
[2556] | 1502 | #stmt_spec cases (fetch_statement_sigma_commute ???????? good (proj2 … (proj1 … prf)) stmt_spec) |
---|
[2551] | 1503 | cases stmt in stmt_spec; -stmt normalize nodelta |
---|
[2553] | 1504 | [1,3: [ #a #b #_| #a #b #c #d #e] #_ #_ #ABS whd in ABS : (???%); destruct(ABS)] |
---|
| 1505 | * normalize nodelta |
---|
| 1506 | [1,3: [#l| #a #b #c] #_ #_ #_ #ABS whd in ABS: (???%); destruct(ABS)] |
---|
| 1507 | #fetch_graph_spec #_ #fetch_lin_spec |
---|
[2551] | 1508 | #H >fetch_lin_spec >m_return_bind normalize nodelta |
---|
[2553] | 1509 | letin graph_ge ≝ (ev_genv (graph_prog_params p p' graph_prog stack_sizes)) |
---|
| 1510 | letin lin_ge ≝ (ev_genv (lin_prog_params p p' (linearise p graph_prog) stack_sizes)) |
---|
| 1511 | cut (preserving … res_preserve … |
---|
| 1512 | (sigma_state … gss) |
---|
| 1513 | (λl.λ_ : True.l) |
---|
| 1514 | (λst. |
---|
| 1515 | do st' ← pop_frame … graph_ge id int_f st; |
---|
| 1516 | if eq_program_counter (pc … st') exit_pc then |
---|
| 1517 | do vals ← read_result … graph_ge (joint_if_result … int_f) st ; |
---|
| 1518 | Word_of_list_beval vals |
---|
| 1519 | else |
---|
| 1520 | Error ? [ ]) |
---|
| 1521 | (λst. |
---|
| 1522 | do st' ← pop_frame … lin_ge id (\fst (linearise_int_fun … int_f)) st; |
---|
| 1523 | if eq_program_counter (pc … st') exit_pc then |
---|
| 1524 | do vals ← read_result … lin_ge (joint_if_result … (\fst (linearise_int_fun … int_f))) st ; |
---|
| 1525 | Word_of_list_beval vals |
---|
| 1526 | else |
---|
| 1527 | Error ? [ ])) |
---|
| 1528 | [ #st #prf @mfr_bind [3: @pop_frame_commute |*:] |
---|
| 1529 | #st' #prf' @eq_program_counter_elim |
---|
[2556] | 1530 | [ #EQ_pc normalize nodelta |
---|
| 1531 | change with (sigma_pc ??????) in match (pc ??); |
---|
| 1532 | >(sigma_pc_exit … EQ_pc) normalize nodelta |
---|
[2553] | 1533 | @mfr_bind [3: @read_result_commute |*:] |
---|
| 1534 | #lbv #prf_lbv @opt_safe_elim #lbv' #EQ_lbv' |
---|
| 1535 | @(mfr_bind … (λpr,prf.〈\fst pr, opt_safe … |
---|
| 1536 | (m_list_map … (sigma_beval_opt p p' graph_prog sigma) (\snd pr)) prf〉)) |
---|
| 1537 | [ |
---|
| 1538 | | * -lbv -lbv' #by1 #lbv #lbv_prf |
---|
| 1539 | @(mfr_bind … (λpr,prf.〈\fst pr, opt_safe … |
---|
| 1540 | (m_list_map … (sigma_beval_opt p p' graph_prog sigma) (\snd pr)) prf〉)) |
---|
| 1541 | [ @opt_safe_elim #lbv' #EQ_lbv' |
---|
| 1542 | |* -lbv #by2 #lbv #lbv_prf |
---|
| 1543 | @(mfr_bind … (λpr,prf.〈\fst pr, opt_safe … |
---|
| 1544 | (m_list_map … (sigma_beval_opt p p' graph_prog sigma) (\snd pr)) prf〉)) |
---|
| 1545 | [ @opt_safe_elim #lbv' #EQ_lbv' |
---|
| 1546 | |* -lbv #by3 #lbv #lbv_prf |
---|
| 1547 | @(mfr_bind … (λpr,prf.〈\fst pr, opt_safe … |
---|
| 1548 | (m_list_map … (sigma_beval_opt p p' graph_prog sigma) (\snd pr)) prf〉)) |
---|
| 1549 | [ @opt_safe_elim #lbv' #EQ_lbv' |
---|
| 1550 | |* -lbv #by4 * [2: #by5 #tl #lbv_prf @res_preserve_error ] |
---|
| 1551 | #lbv_prf @mfr_return % |
---|
| 1552 | ]]]] |
---|
| 1553 | cases lbv in EQ_lbv'; |
---|
| 1554 | try (#H @res_preserve_error) |
---|
| 1555 | -lbv #by1 #lbv #H @('bind_inversion H) -H #by1' #EQby1' |
---|
| 1556 | #H @('bind_inversion H) -H #tl' #EQtl' |
---|
| 1557 | whd in ⊢ (??%?→?); #EQ destruct(EQ) |
---|
| 1558 | @(mfr_bind … (λby.λ_:True.by)) |
---|
| 1559 | [1,3,5,7: #by #EQ %{I} >(Byte_of_val_inv … EQ) in EQby1'; |
---|
| 1560 | whd in ⊢ (??%%→?); #EQ destruct(EQ) % |
---|
| 1561 | |*: #by1 * @mfr_return_eq |
---|
| 1562 | change with (m_list_map ????? = ?) in EQtl'; |
---|
| 1563 | [1,3,5,7: % |
---|
| 1564 | |*: @opt_safe_elim #lbv'' |
---|
| 1565 | ] >EQtl' #EQ destruct % |
---|
| 1566 | ] |
---|
| 1567 | | #_ @res_preserve_error |
---|
| 1568 | ] |
---|
| 1569 | ] |
---|
| 1570 | #PRESERVE |
---|
| 1571 | cases (PRESERVE … (proj2 … prf) … H) * |
---|
| 1572 | #EQ >EQ % whd in ⊢ (??%?→?); #ABS destruct(ABS) |
---|
[2442] | 1573 | qed. |
---|
| 1574 | |
---|
[2556] | 1575 | lemma as_label_sigma_commute : |
---|
| 1576 | ∀p,p',graph_prog,stack_sizes,sigma,gss.good_sigma p graph_prog sigma → |
---|
| 1577 | ∀st,prf. |
---|
| 1578 | as_label (lin_abstract_status p p' (linearise … graph_prog) stack_sizes) |
---|
| 1579 | (sigma_state_pc p p' graph_prog sigma gss st prf) = |
---|
| 1580 | as_label (graph_abstract_status p p' graph_prog stack_sizes) st. |
---|
| 1581 | #p #p' #graph_prog #stack_sizes #sigma #gss #good * #st #pc #popped |
---|
| 1582 | ** #prf1 #prf2 #prf3 |
---|
| 1583 | change with (as_label_of_pc ?? = as_label_of_pc ??) |
---|
| 1584 | change with (sigma_pc ??????) in match (as_pc_of ??); |
---|
| 1585 | change with pc in match (as_pc_of ??); |
---|
| 1586 | whd in match sigma_pc; normalize nodelta |
---|
| 1587 | @opt_safe_elim #pc' |
---|
| 1588 | whd in match sigma_pc_opt; normalize nodelta |
---|
| 1589 | @eqZb_elim #Hbl normalize nodelta |
---|
| 1590 | [ whd in ⊢ (??%%→??%%); #EQ destruct(EQ) |
---|
| 1591 | whd in match fetch_statement; normalize nodelta |
---|
| 1592 | >(fetch_internal_function_no_minus_one … graph_prog … Hbl) |
---|
| 1593 | >(fetch_internal_function_no_minus_one … (linearise … graph_prog) … Hbl) % |
---|
| 1594 | | #H @('bind_inversion H) * #i #f -H |
---|
| 1595 | inversion (fetch_internal_function … (pc_block pc)) |
---|
| 1596 | [2: #e #_ whd in ⊢ (??%%→?); #ABS destruct(ABS) ] |
---|
| 1597 | * #i' #f' #EQfetch whd in ⊢ (??%%→?); #EQ destruct(EQ) |
---|
| 1598 | #H @('bind_inversion H) #n #EQsigma whd in ⊢ (??%%→?); #EQ destruct(EQ) |
---|
| 1599 | whd in ⊢ (??%%); |
---|
| 1600 | whd in match fetch_statement; normalize nodelta >EQfetch |
---|
| 1601 | >(fetch_internal_function_transf … graph_prog |
---|
| 1602 | (λvars,fn.\fst (linearise_int_fun … fn)) … EQfetch) |
---|
| 1603 | >m_return_bind >m_return_bind |
---|
| 1604 | cases (good f) * #_ #all_labels_in #spec |
---|
| 1605 | cases (spec … EQsigma) #s ** cases s -s |
---|
| 1606 | [ * [#s|#a#lbl]#nxt|#s|*] normalize nodelta #EQstmt_at #_ |
---|
| 1607 | [ * #EQstmt_at' #_ | * [ * #EQstmt_at' #_ | #EQstmt_at' ] | #EQstmt_at' ] |
---|
| 1608 | whd in match point_of_pc; normalize nodelta >point_of_offset_of_point |
---|
| 1609 | >EQstmt_at >EQstmt_at' normalize nodelta % |
---|
| 1610 | qed. |
---|
| 1611 | |
---|
[2507] | 1612 | lemma set_istack_sigma_commute : |
---|
[2547] | 1613 | ∀p,p',graph_prog,sigma,gss,st,is,prf1,prf2,prf3. |
---|
| 1614 | set_istack ? (sigma_is p p' graph_prog sigma is prf1) (sigma_state p p' graph_prog sigma gss st prf2) = |
---|
| 1615 | sigma_state ???? gss (set_istack ? is st) prf3. |
---|
| 1616 | #p #p' #graph_prog #sigma #gss * |
---|
| 1617 | #frms #is' #carry #r #m #is #prf1 #prf2 #prf3 % qed. |
---|
| 1618 | (* #st #is #sigmais #prf1 #prf2 #H |
---|
[2507] | 1619 | whd in match set_istack; normalize nodelta |
---|
| 1620 | whd in match sigma_state; normalize nodelta |
---|
| 1621 | whd in match sigma_is; normalize nodelta |
---|
| 1622 | @opt_safe_elim #x #H1 |
---|
| 1623 | cut(x = sigmais) [>H1 in H; #EQ whd in EQ : (???%); destruct(EQ) %] |
---|
| 1624 | #EQ >EQ // |
---|
[2547] | 1625 | qed.*) |
---|
[2507] | 1626 | |
---|
[2528] | 1627 | lemma is_push_sigma_commute : |
---|
[2547] | 1628 | ∀ p, p', graph_prog,sigma. |
---|
| 1629 | preserving2 … res_preserve … |
---|
| 1630 | (sigma_is p p' graph_prog sigma) |
---|
| 1631 | (sigma_beval p p' graph_prog sigma) |
---|
| 1632 | (sigma_is p p' graph_prog sigma) |
---|
| 1633 | is_push is_push. |
---|
[2536] | 1634 | #p #p' #graph_prog #sigma * |
---|
[2547] | 1635 | [ | #bv1 | #bv1 #bv2 ] #val #prf1 #prf2 #is' |
---|
[2536] | 1636 | whd in ⊢ (??%%→?); #EQ destruct(EQ) |
---|
| 1637 | whd in match sigma_beval; normalize nodelta |
---|
| 1638 | @opt_safe_elim #val' #EQsigma_val |
---|
[2528] | 1639 | % |
---|
[2536] | 1640 | [1,3: @hide_prf % |
---|
| 1641 | |*: whd in match sigma_is in ⊢ (???%); normalize nodelta |
---|
| 1642 | @opt_safe_elim #is'' |
---|
| 1643 | ] whd in match sigma_is_opt; normalize nodelta |
---|
| 1644 | [2,4: |
---|
| 1645 | inversion (sigma_beval_opt ?????) |
---|
| 1646 | [1,3: #EQ whd in prf1 : (?(??%?)); @⊥ >EQ in prf1; |
---|
| 1647 | normalize nodelta * #H @H % ] |
---|
| 1648 | #bv1' #EQ_bv1' >m_return_bind ] |
---|
| 1649 | >EQsigma_val |
---|
| 1650 | whd in ⊢ (??%%→?); #EQ destruct(EQ) |
---|
| 1651 | whd in match sigma_is; normalize nodelta |
---|
| 1652 | @opt_safe_elim #is1 |
---|
[2528] | 1653 | whd in match sigma_is_opt; normalize nodelta |
---|
[2536] | 1654 | [ #H @('bind_inversion H) #bv1'' |
---|
| 1655 | >EQ_bv1' #EQ destruct(EQ) ] |
---|
| 1656 | whd in ⊢ (??%%→?); #EQ destruct(EQ) % |
---|
[2528] | 1657 | qed. |
---|
| 1658 | |
---|
[2553] | 1659 | lemma Bit_of_val_inv : |
---|
[2547] | 1660 | ∀e,bb,v.Bit_of_val e bb = return v → bb = BBbit v. |
---|
| 1661 | #e * |
---|
| 1662 | [ #b || #b #ptr #p #o ] #v |
---|
| 1663 | whd in ⊢ (??%%→?); #EQ destruct(EQ) % qed. |
---|
| 1664 | |
---|
[2528] | 1665 | lemma beopaccs_sigma_commute : |
---|
[2547] | 1666 | ∀p,p',graph_prog,sigma,op. |
---|
| 1667 | preserving2 … res_preserve … |
---|
| 1668 | (sigma_beval p p' graph_prog sigma) |
---|
| 1669 | (sigma_beval p p' graph_prog sigma) |
---|
| 1670 | (λpr,prf.〈sigma_beval p p' graph_prog sigma (\fst pr) (proj1 ?? prf), |
---|
| 1671 | sigma_beval p p' graph_prog sigma (\snd pr) (proj2 ?? prf)〉) |
---|
| 1672 | (be_opaccs op) (be_opaccs op). |
---|
[2536] | 1673 | #p #p' #graph_prog #sigma #op |
---|
[2547] | 1674 | #bv1 #bv2 #prf1 #prf2 |
---|
| 1675 | @mfr_bind [ @(λ_.True) | @(λx.λ_.x) ] |
---|
| 1676 | [2: #by1 * @mfr_bind [ @(λ_.True) | @(λx.λ_.x) ] |
---|
| 1677 | [2: #by2 * cases (opaccs ????) #by1' #by2' |
---|
| 1678 | @mfr_return %% whd in ⊢ (??%%→?); #EQ destruct(EQ) |
---|
| 1679 | ] |
---|
| 1680 | ] |
---|
| 1681 | #v #EQ %{I} |
---|
| 1682 | >sigma_bv_no_pc try assumption |
---|
[2553] | 1683 | >(Byte_of_val_inv … EQ) % |
---|
[2536] | 1684 | qed. |
---|
| 1685 | |
---|
[2547] | 1686 | lemma beop1_sigma_commute : |
---|
| 1687 | ∀p,p',graph_prog,sigma,op. |
---|
| 1688 | preserving … res_preserve … |
---|
| 1689 | (sigma_beval p p' graph_prog sigma) |
---|
| 1690 | (sigma_beval p p' graph_prog sigma) |
---|
| 1691 | (be_op1 op) (be_op1 op). |
---|
| 1692 | #p #p' #graph_prog #sigma #op |
---|
| 1693 | #bv #prf |
---|
| 1694 | @mfr_bind [ @(λ_.True) | @(λx.λ_.x) ] |
---|
| 1695 | [2: #by * @mfr_return % whd in ⊢ (??%%→?); #EQ destruct(EQ) ] |
---|
| 1696 | #v #EQ %{I} >sigma_bv_no_pc try assumption |
---|
[2553] | 1697 | >(Byte_of_val_inv … EQ) % |
---|
[2547] | 1698 | qed. |
---|
| 1699 | |
---|
| 1700 | |
---|
[2536] | 1701 | lemma sigma_ptr_commute : |
---|
[2547] | 1702 | ∀ p, p', graph_prog , sigma. |
---|
| 1703 | preserving … res_preserve … |
---|
| 1704 | (λpr,prf.〈sigma_beval p p' graph_prog sigma (\fst pr) (proj1 ?? prf), |
---|
| 1705 | sigma_beval p p' graph_prog sigma (\snd pr) (proj2 ?? prf)〉) |
---|
| 1706 | (λx.λ_ : True.x) |
---|
| 1707 | pointer_of_address pointer_of_address. |
---|
| 1708 | #p #p' #graph_prog #sigma * #val1 #val2 * #prf1 #prf2 |
---|
| 1709 | #ptr whd in ⊢ (??%?→?); |
---|
| 1710 | cases val1 in prf1; |
---|
| 1711 | [|| #ptr1 #ptr2 #p | #by | #p | #ptr1 #p1 | #pc #p ] |
---|
| 1712 | #prf1 whd in ⊢ (??%%→?); #EQ destruct(EQ) |
---|
| 1713 | cases val2 in prf2 EQ; |
---|
| 1714 | [|| #ptr1 #ptr2 #p | #by | #p | #ptr2 #p2 | #pc #p ] |
---|
| 1715 | #prf2 normalize nodelta #EQ destruct(EQ) |
---|
| 1716 | %{I} |
---|
| 1717 | >sigma_bv_no_pc [2: %] |
---|
| 1718 | >sigma_bv_no_pc [2: %] @EQ |
---|
| 1719 | qed. |
---|
| 1720 | |
---|
| 1721 | lemma beop2_sigma_commute : |
---|
| 1722 | ∀p,p',graph_prog,sigma,carry,op. |
---|
| 1723 | preserving2 … res_preserve … |
---|
| 1724 | (sigma_beval p p' graph_prog sigma) |
---|
| 1725 | (sigma_beval p p' graph_prog sigma) |
---|
| 1726 | (λpr,prf.〈sigma_beval p p' graph_prog sigma (\fst pr) prf, \snd pr〉) |
---|
| 1727 | (be_op2 carry op) (be_op2 carry op). |
---|
| 1728 | #p #p' #graph_prog #sigma #carry #op |
---|
| 1729 | @bv_pc_other |
---|
| 1730 | [ #pc1 #p1 #bv2 |
---|
| 1731 | | #bv1 #bv1_no_pc |
---|
| 1732 | @bv_pc_other |
---|
| 1733 | [ #pc2 #p2 |
---|
| 1734 | | #bv2 #bv2_no_pc |
---|
| 1735 | ] |
---|
| 1736 | ] #prf1 #prf2 |
---|
| 1737 | * #res #carry' |
---|
| 1738 | [1,2: |
---|
| 1739 | [2: cases bv1 in prf1; |
---|
| 1740 | [|| #ptr11 #ptr12 #p1 | #by1 | #p1 | #ptr1 #p1 | #pc1 #p1 ] #prf1 ] |
---|
| 1741 | whd in ⊢ (??%%→?); |
---|
| 1742 | #EQ destruct(EQ) ] |
---|
| 1743 | #EQ |
---|
| 1744 | cut (bv_no_pc res) |
---|
| 1745 | [ -prf1 -prf2 |
---|
| 1746 | cases bv1 in bv1_no_pc EQ; |
---|
| 1747 | [|| #ptr11 #ptr12 #p1 | #by1 | #p1 | #ptr1 #p1 | #pc1 #p1 ] * |
---|
| 1748 | cases bv2 in bv2_no_pc; |
---|
| 1749 | [3,10,17,24,31,38: #ptr21 #ptr22 #p2 |
---|
| 1750 | |4,11,18,25,32,39: #by2 |
---|
| 1751 | |5,12,19,26,33,40: #p2 |
---|
| 1752 | |6,13,20,27,34,41: #ptr2 #p2 |
---|
| 1753 | |7,14,21,28,35,42: #pc2 #p2 |
---|
| 1754 | ] * |
---|
| 1755 | cases op |
---|
| 1756 | whd in match be_op2; whd in ⊢ (???%→?); |
---|
| 1757 | normalize nodelta |
---|
| 1758 | #EQ destruct(EQ) try % |
---|
| 1759 | try (whd in EQ : (??%?); destruct(EQ) %) |
---|
| 1760 | lapply EQ -EQ |
---|
| 1761 | [ @if_elim #_ [ @if_elim #_ ] whd in ⊢ (??%%→?); #EQ destruct(EQ) % |
---|
| 1762 | |2,12,13,16,18: @if_elim #_ whd in ⊢ (??%%→?); #EQ destruct(EQ) % |
---|
| 1763 | |3,4,5,6,7,8: #H @('bind_inversion H) #bit #EQ |
---|
| 1764 | cases (op2 eval bit ???) #res' #bit' |
---|
| 1765 | whd in ⊢ (??%%→?); #EQ destruct(EQ) % |
---|
| 1766 | |17: cases (ptype ptr1) normalize nodelta |
---|
| 1767 | [ @if_elim #_ |
---|
| 1768 | [ #H @('bind_inversion H) #bit #EQbit |
---|
| 1769 | cases (op2 eval bit ???) #res' #bit' |
---|
[2536] | 1770 | ] |
---|
[2547] | 1771 | ] |
---|
| 1772 | whd in ⊢ (??%%→?); #EQ destruct(EQ) % |
---|
| 1773 | |*: whd in ⊢ (??%?→?); |
---|
| 1774 | cases (ptype ?) normalize nodelta |
---|
| 1775 | try (#EQ destruct(EQ) @I) |
---|
| 1776 | cases (part_no ?) normalize nodelta |
---|
| 1777 | try (#n lapply (refl ℕ n) #_) |
---|
| 1778 | try (#EQ destruct(EQ) @I) |
---|
| 1779 | try (#H @('bind_inversion H) -H * #EQbit |
---|
| 1780 | whd in ⊢ (??%%→?);) |
---|
| 1781 | try (#EQ destruct(EQ) @I) |
---|
| 1782 | [1,2,4,6,7: cases (op2 eval ????) #res' #bit' whd in ⊢ (??%%→?); |
---|
| 1783 | #EQ destruct(EQ) @I |
---|
| 1784 | |*: cases carry normalize nodelta |
---|
| 1785 | try (#b lapply (refl bool b) #_) |
---|
| 1786 | try (#ptr lapply (refl pointer ptr) #_ #p #o) |
---|
| 1787 | try (#EQ destruct(EQ) @I) |
---|
| 1788 | @if_elim #_ |
---|
| 1789 | try (#EQ destruct(EQ) @I) |
---|
| 1790 | @If_elim #prf |
---|
| 1791 | try (#EQ destruct(EQ) @I) |
---|
| 1792 | cases (op2_bytes ?????) |
---|
| 1793 | #res' #bit' whd in ⊢ (??%%→?); |
---|
| 1794 | #EQ destruct(EQ) @I |
---|
| 1795 | ] |
---|
[2536] | 1796 | ] |
---|
[2547] | 1797 | ] #res_no_pc |
---|
| 1798 | %{(bv_no_pc_wf … res_no_pc)} |
---|
| 1799 | >(sigma_bv_no_pc … bv1_no_pc) |
---|
| 1800 | >(sigma_bv_no_pc … bv2_no_pc) |
---|
| 1801 | >(sigma_bv_no_pc … res_no_pc) |
---|
| 1802 | assumption |
---|
[2528] | 1803 | qed. |
---|
| 1804 | |
---|
[2547] | 1805 | definition combine_strong : |
---|
| 1806 | ∀A,B,C,D : Type[0]. |
---|
| 1807 | ∀P : A → Prop.∀Q : C → Prop. |
---|
| 1808 | (∀x.P x → B) → (∀x.Q x → D) → |
---|
| 1809 | (∀pr.(P (\fst pr) ∧ Q (\snd pr)) → B × D) ≝ |
---|
| 1810 | λA,B,C,D,P,Q,f,g,pr,prf.〈f ? (proj1 … prf), g ? (proj2 … prf)〉. |
---|
| 1811 | |
---|
| 1812 | lemma wf_set_is : ∀p,p',graph_prog,sigma,gss,st,is. |
---|
| 1813 | well_formed_state p p' graph_prog sigma gss st → |
---|
| 1814 | sigma_is_opt p p' graph_prog sigma is ≠ None ? → |
---|
| 1815 | well_formed_state … gss (set_istack … is st). |
---|
| 1816 | #p #p' #graph_prog #sigma #gss #st #is |
---|
| 1817 | *** #H1 #H2 #H3 #H4 #H5 |
---|
| 1818 | %{H4} %{H3} %{H5} @H1 |
---|
| 1819 | qed. |
---|
| 1820 | |
---|
| 1821 | lemma wf_set_m : ∀p,p',graph_prog,sigma,gss,st,m. |
---|
| 1822 | well_formed_state p p' graph_prog sigma gss st → |
---|
| 1823 | well_formed_mem p p' graph_prog sigma m → |
---|
| 1824 | well_formed_state … gss (set_m … m st). |
---|
| 1825 | #p #p' #graph_prog #sigma #gss #st #m |
---|
| 1826 | *** #H1 #H2 #H3 #H4 #H5 |
---|
| 1827 | %{H5} %{H3} %{H2} @H1 |
---|
| 1828 | qed. |
---|
[2570] | 1829 | (* spostato in ExtraMonads.ma |
---|
[2547] | 1830 | lemma opt_to_res_preserve : ∀X,Y,P,F,m,n,e1,e2. |
---|
| 1831 | opt_preserve X Y P F m n → |
---|
| 1832 | res_preserve X Y P F (opt_to_res … e1 m) (opt_to_res … e2 n). |
---|
| 1833 | #X #Y #P #F #m #n #e1 #e2 #H #v #prf |
---|
| 1834 | cases (H … (opt_eq_from_res ???? prf)) #prf' #EQ %{prf'} |
---|
| 1835 | >EQ % |
---|
| 1836 | qed. |
---|
| 1837 | |
---|
| 1838 | lemma err_eq_from_io : ∀O,I,X,m,v. |
---|
| 1839 | err_to_io O I X m = return v → m = return v. |
---|
| 1840 | #O #I #X * #x #v normalize #EQ destruct % qed. |
---|
| 1841 | |
---|
| 1842 | lemma res_to_io_preserve : ∀O,I,X,Y,P,F,m,n. |
---|
| 1843 | res_preserve X Y P F m n → |
---|
| 1844 | io_preserve O I X Y P F m n. |
---|
| 1845 | #O #I #X #Y #P #F #m #n #H #v #prf |
---|
| 1846 | cases (H … (err_eq_from_io ????? prf)) #prf' #EQ %{prf'} |
---|
| 1847 | >EQ % |
---|
| 1848 | qed. |
---|
[2570] | 1849 | *) |
---|
[2484] | 1850 | lemma eval_seq_no_pc_sigma_commute : |
---|
| 1851 | ∀p,p',graph_prog. |
---|
| 1852 | let lin_prog ≝ linearise p graph_prog in |
---|
[2529] | 1853 | ∀stack_sizes. |
---|
| 1854 | ∀sigma.∀gss : good_state_sigma p p' graph_prog sigma. |
---|
[2547] | 1855 | ∀f,fn,stmt. |
---|
| 1856 | preserving … res_preserve … |
---|
| 1857 | (sigma_state … gss) |
---|
| 1858 | (sigma_state … gss) |
---|
| 1859 | (eval_seq_no_pc … (ev_genv … (graph_prog_params … graph_prog stack_sizes)) |
---|
| 1860 | f fn stmt) |
---|
| 1861 | (eval_seq_no_pc … (ev_genv … (lin_prog_params … lin_prog stack_sizes)) |
---|
| 1862 | f (\fst (linearise_int_fun … fn)) stmt). |
---|
[2536] | 1863 | #p #p' #graph_prog #stack_sizes #sigma #gss #f |
---|
[2547] | 1864 | #fn #stmt |
---|
[2536] | 1865 | whd in match eval_seq_no_pc; |
---|
[2484] | 1866 | cases stmt normalize nodelta |
---|
[2547] | 1867 | [1,2: (* COMMENT, COST_LABEL *) #_ @mfr_return |
---|
| 1868 | | (* MOVE *) #mv_sig #st #prf' |
---|
[2556] | 1869 | @mfr_bind [3: @pair_reg_move_commute |*:] |
---|
| 1870 | #r #prf @mfr_return @wf_set_regs assumption |
---|
[2495] | 1871 | | (* POP *) |
---|
[2547] | 1872 | #a #st #prf |
---|
| 1873 | @(mfr_bind … (combine_strong … (sigma_beval p p' graph_prog sigma) (sigma_state … gss))) |
---|
| 1874 | [ @(mfr_bind … (sigma_is_pop_commute …)) * #bv #is' * #prf1' #prf2' |
---|
| 1875 | @mfr_return %{prf1'} @wf_set_is assumption |
---|
| 1876 | | * #bv #st' * #prf1' #prf2' |
---|
| 1877 | @mfr_bind [3: @acca_store__commute |*:] |
---|
| 1878 | #r #prf3' @mfr_return @wf_set_regs assumption |
---|
[2501] | 1879 | ] |
---|
[2507] | 1880 | | (* PUSH *) |
---|
[2547] | 1881 | #a #st #prf |
---|
[2556] | 1882 | @mfr_bind [3: @acca_arg_retrieve_commute |*:] |
---|
| 1883 | #bv #prf_bv |
---|
| 1884 | @mfr_bind [3: @is_push_sigma_commute |*:] |
---|
| 1885 | #is #prf_is @mfr_return @wf_set_is assumption |
---|
[2528] | 1886 | | (*C_ADDRESS*) |
---|
[2536] | 1887 | #sy |
---|
| 1888 | change with ((member ? ? ? (prog_var_names (joint_function (mk_graph_params p)) ℕ graph_prog)) → ?) |
---|
[2528] | 1889 | #sy_prf |
---|
| 1890 | change with ((dpl_reg p) → ?) #dpl |
---|
| 1891 | change with ((dph_reg p) → ?) #dph |
---|
[2547] | 1892 | #st #prf |
---|
| 1893 | @(mfr_bind … (sigma_state … gss)) |
---|
| 1894 | [ @(mfr_bind … (sigma_regs … gss)) |
---|
| 1895 | [2: #r #prf' @mfr_return @wf_set_regs assumption ] |
---|
| 1896 | ] |
---|
| 1897 | @opt_safe_elim #bl #EQbl |
---|
| 1898 | @opt_safe_elim #bl' |
---|
| 1899 | >(find_symbol_transf … |
---|
| 1900 | (λvars.transf_fundef … (λfn.\fst (linearise_int_fun … fn))) graph_prog sy) in ⊢ (%→?); |
---|
| 1901 | >EQbl in ⊢ (%→?); #EQ destruct(EQ) |
---|
| 1902 | [ @dpl_store_commute |
---|
| 1903 | | #st' #st_prf' |
---|
| 1904 | @mfr_bind [3: @dph_store_commute |*:] |
---|
| 1905 | [2: #r #prf' @mfr_return @wf_set_regs assumption |
---|
| 1906 | ] |
---|
| 1907 | ] @bv_no_pc_wf % |
---|
[2528] | 1908 | | (*C_OPACCS*) |
---|
[2547] | 1909 | #op #a #b #arg1 #arg2 #st #prf |
---|
[2556] | 1910 | @mfr_bind [3: @acca_arg_retrieve_commute |*: ] |
---|
[2547] | 1911 | #bv1 #bv1_prf |
---|
[2556] | 1912 | @mfr_bind [3: @accb_arg_retrieve_commute |*: ] |
---|
[2547] | 1913 | #bv2 #bv2_prf |
---|
[2556] | 1914 | @mfr_bind [3: @beopaccs_sigma_commute |*: ] |
---|
[2547] | 1915 | * #res1 #res2 * #res1_prf #res2_prf |
---|
| 1916 | @(mfr_bind … (sigma_state … gss)) |
---|
| 1917 | [ @mfr_bind [3: @acca_store__commute |*: ] |
---|
| 1918 | #r #r_prf @mfr_return @wf_set_regs assumption |
---|
| 1919 | ] |
---|
| 1920 | #st' #st_prf' |
---|
| 1921 | @mfr_bind [3: @accb_store_commute |*: ] |
---|
| 1922 | #r #r_prf @mfr_return @wf_set_regs assumption |
---|
[2528] | 1923 | | (*C_OP1*) |
---|
[2547] | 1924 | #op #a #arg #st #prf |
---|
[2556] | 1925 | @mfr_bind [3: @acca_retrieve_commute |*: ] |
---|
[2547] | 1926 | #bv #bv_prf |
---|
[2556] | 1927 | @mfr_bind [3: @beop1_sigma_commute |*: ] |
---|
[2547] | 1928 | #res #res_prf |
---|
| 1929 | @mfr_bind [3: @acca_store__commute |*: ] |
---|
| 1930 | #r #r_prf @mfr_return @wf_set_regs assumption |
---|
[2536] | 1931 | | (*C_OP2*) |
---|
[2547] | 1932 | #op #a #arg1 #arg2 #st #prf |
---|
[2556] | 1933 | @mfr_bind [3: @acca_arg_retrieve_commute |*: ] |
---|
[2547] | 1934 | #bv1 #bv1_prf |
---|
[2556] | 1935 | @mfr_bind [3: @snd_arg_retrieve_commute |*: ] |
---|
[2547] | 1936 | #bv2 #bv2_prf |
---|
[2556] | 1937 | @mfr_bind [3: @beop2_sigma_commute |*: ] |
---|
[2547] | 1938 | * #res1 #carry' #res1_prf |
---|
| 1939 | @(mfr_bind … (sigma_state … gss)) |
---|
| 1940 | [ @mfr_bind [3: @acca_store__commute |*: ] |
---|
| 1941 | #r #r_prf @mfr_return @wf_set_regs assumption |
---|
| 1942 | ] |
---|
| 1943 | #st' #st_prf' @mfr_return |
---|
[2536] | 1944 | | (*C_CLEAR_CARRY*) |
---|
[2547] | 1945 | #st #prf @mfr_return |
---|
[2536] | 1946 | | (*C_SET_CARRY*) |
---|
[2547] | 1947 | #st #prf @mfr_return |
---|
[2536] | 1948 | | (*C_LOAD*) |
---|
[2547] | 1949 | #a #dpl #dph #st #prf |
---|
| 1950 | @mfr_bind [3: @dph_arg_retrieve_commute |*:] |
---|
| 1951 | #bv1 #bv1_prf |
---|
| 1952 | @mfr_bind [3: @dpl_arg_retrieve_commute |*:] |
---|
| 1953 | #bv2 #bv2_prf |
---|
| 1954 | @mfr_bind [3: @sigma_ptr_commute |*:] |
---|
| 1955 | [ % assumption ] |
---|
| 1956 | #ptr * |
---|
| 1957 | @mfr_bind |
---|
| 1958 | [3: |
---|
| 1959 | @opt_to_res_preserve @beloadv_sigma_commute |
---|
| 1960 | |*:] |
---|
| 1961 | #res #res_prf |
---|
| 1962 | @mfr_bind [3: @acca_store__commute |*: ] |
---|
| 1963 | #r #r_prf @mfr_return @wf_set_regs assumption |
---|
| 1964 | | (*C_STORE*) |
---|
| 1965 | #dpl #dph #a #st #prf |
---|
| 1966 | @mfr_bind [3: @dph_arg_retrieve_commute |*:] |
---|
| 1967 | #bv1 #bv1_prf |
---|
| 1968 | @mfr_bind [3: @dpl_arg_retrieve_commute |*:] |
---|
| 1969 | #bv2 #bv2_prf |
---|
| 1970 | @mfr_bind [3: @sigma_ptr_commute |*:] |
---|
| 1971 | [ % assumption ] |
---|
| 1972 | #ptr * |
---|
| 1973 | @mfr_bind |
---|
| 1974 | [3: @acca_arg_retrieve_commute |*:] |
---|
| 1975 | #res #res_prf |
---|
| 1976 | @mfr_bind |
---|
| 1977 | [3: |
---|
| 1978 | @opt_to_res_preserve @bestorev_sigma_commute |
---|
| 1979 | |*:] |
---|
| 1980 | #mem #wf_mem |
---|
| 1981 | @mfr_return |
---|
| 1982 | @wf_set_m assumption |
---|
| 1983 | | (*CALL*) |
---|
| 1984 | #f #args #dest #st #prf @mfr_return |
---|
[2536] | 1985 | | (*C_EXT*) |
---|
[2547] | 1986 | #s_ext #st #prf @eval_ext_seq_commute |
---|
[2536] | 1987 | ] |
---|
| 1988 | qed. |
---|
| 1989 | |
---|
[2556] | 1990 | lemma eval_seq_no_call_ok : |
---|
[2548] | 1991 | ∀p,p',graph_prog. |
---|
| 1992 | let lin_prog ≝ linearise p graph_prog in |
---|
| 1993 | ∀stack_sizes. |
---|
[2556] | 1994 | ∀sigma.good_sigma p graph_prog sigma → |
---|
| 1995 | ∀gss : good_state_sigma p p' graph_prog sigma. |
---|
[2548] | 1996 | ∀st,st',f,fn,stmt,nxt.no_call ?? stmt → |
---|
| 1997 | ∀prf : well_formed_state_pc … gss st. |
---|
[2808] | 1998 | fetch_statement (mk_sem_graph_params p p') … |
---|
[2556] | 1999 | (globalenv_noinit ? graph_prog) (pc … st) = |
---|
| 2000 | return 〈f, fn, sequential … (step_seq (mk_graph_params p) … stmt) nxt〉 → |
---|
| 2001 | eval_state … (ev_genv … (graph_prog_params … graph_prog stack_sizes)) st = |
---|
| 2002 | return st' → |
---|
| 2003 | ∃prf'. |
---|
[2548] | 2004 | ∃taf : trace_any_any_free (lin_abstract_status p p' lin_prog stack_sizes) |
---|
| 2005 | (sigma_state_pc … gss st prf) |
---|
[2556] | 2006 | (sigma_state_pc … gss st' prf'). |
---|
[2548] | 2007 | bool_to_Prop (taaf_non_empty … taf). |
---|
[2556] | 2008 | #p #p' #graph_prog #stack_sizes #sigma #good #gss #st #st' #f #fn #stmt #nxt #stmt_no_call |
---|
| 2009 | #prf #EQfetch |
---|
| 2010 | whd in match eval_state; normalize nodelta >EQfetch |
---|
| 2011 | >m_return_bind whd in match eval_statement_no_pc; |
---|
| 2012 | whd in match eval_statement_advance; normalize nodelta |
---|
| 2013 | @'bind_inversion #st_no_pc' #EQeval |
---|
| 2014 | >no_call_advance [2: assumption] |
---|
| 2015 | whd in ⊢ (??%%→?); #EQ destruct(EQ) |
---|
| 2016 | cases (fetch_statement_sigma_commute … good … (proj2 … (proj1 … prf)) … EQfetch) |
---|
| 2017 | normalize nodelta #_ * #EQfetch' * |
---|
| 2018 | #prf_nxt #nxt_spec |
---|
| 2019 | lapply (err_eq_from_io ????? EQeval) -EQeval #EQeval |
---|
| 2020 | cases (eval_seq_no_pc_sigma_commute … gss … (proj2 … prf) … EQeval) |
---|
| 2021 | #st_no_pc_prf |
---|
| 2022 | #EQeval' |
---|
| 2023 | %{(hide_prf …)} [ %{st_no_pc_prf} %{prf_nxt} cases st in prf; -st #st #pc #popped ** // ] |
---|
| 2024 | cases nxt_spec -nxt_spec |
---|
| 2025 | [ #nxt_spec %{(taaf_step … (taa_base …) …) I} |
---|
| 2026 | | * #nxt_spec #pc_of_label_spec %{(taaf_step … (taa_step … (taa_base …))…) I} |
---|
[2548] | 2027 | ] |
---|
[2556] | 2028 | [1,6: |
---|
| 2029 | whd whd in ⊢ (??%?); >EQfetch' normalize nodelta |
---|
[2548] | 2030 | whd in match joint_classify_step; normalize nodelta |
---|
[2553] | 2031 | >no_call_other try % assumption |
---|
[2556] | 2032 | |2,5: |
---|
| 2033 | whd whd in match eval_state; normalize nodelta |
---|
| 2034 | change with (sigma_pc ??????) in match (pc ??); |
---|
| 2035 | try >EQfetch' in ⊢ (??%?); >m_return_bind in ⊢ (??%?); |
---|
[2548] | 2036 | whd in match eval_statement_no_pc; normalize nodelta |
---|
[2556] | 2037 | try >EQeval' in ⊢ (??%?); >m_return_bind in ⊢ (??%?); |
---|
[2548] | 2038 | whd in match eval_statement_advance; normalize nodelta |
---|
[2556] | 2039 | >no_call_advance try assumption |
---|
[2553] | 2040 | whd in match (next ???) in ⊢ (??%?); |
---|
[2556] | 2041 | [ >nxt_spec % |
---|
| 2042 | | % |
---|
| 2043 | ] |
---|
| 2044 | |3: |
---|
| 2045 | whd whd in ⊢ (??%?); >nxt_spec normalize nodelta % |
---|
| 2046 | |4: |
---|
| 2047 | whd whd in match eval_state; normalize nodelta |
---|
| 2048 | >nxt_spec >m_return_bind >m_return_bind |
---|
| 2049 | whd in match eval_statement_advance; normalize nodelta |
---|
| 2050 | whd in match goto; normalize nodelta |
---|
[2553] | 2051 | whd in match (pc_block ?); >pc_block_sigma_commute |
---|
[2556] | 2052 | >pc_of_label_spec % |
---|
| 2053 | |7: %* #H @H -H |
---|
| 2054 | whd in ⊢ (??%?); >nxt_spec % |
---|
| 2055 | |8: |
---|
[2548] | 2056 | ] |
---|
| 2057 | qed. |
---|
| 2058 | |
---|
[2555] | 2059 | lemma block_of_call_sigma_commute : |
---|
| 2060 | ∀p,p',graph_prog,sigma. |
---|
| 2061 | ∀gss : good_state_sigma p p' graph_prog sigma.∀cl. |
---|
| 2062 | preserving … res_preserve … |
---|
| 2063 | (sigma_state p p' graph_prog sigma gss) |
---|
| 2064 | (λx.λ_ : True .x) |
---|
[2808] | 2065 | (block_of_call (mk_sem_graph_params p p') … |
---|
[2555] | 2066 | (globalenv_noinit ? graph_prog) cl) |
---|
[2808] | 2067 | (block_of_call (mk_sem_lin_params p p') … |
---|
[2555] | 2068 | (globalenv_noinit ? (linearise ? graph_prog)) cl). |
---|
| 2069 | #p #p' #graph_prog #sigma #gss #cl #st #prf |
---|
| 2070 | @mfr_bind |
---|
| 2071 | [3: cases cl |
---|
| 2072 | [ #id normalize nodelta @opt_to_res_preserve |
---|
| 2073 | >(find_symbol_transf … |
---|
| 2074 | (λvars.transf_fundef … (λfn.\fst (linearise_int_fun … fn))) graph_prog id) |
---|
| 2075 | #s #EQs %{I} >EQs in ⊢ (??%?); % |
---|
| 2076 | | * #dpl #dph normalize nodelta |
---|
| 2077 | @mfr_bind [3: @dpl_arg_retrieve_commute |*:] |
---|
| 2078 | #bv1 #bv1_prf |
---|
| 2079 | @mfr_bind [3: @dph_arg_retrieve_commute |*:] |
---|
| 2080 | #bv2 #bv2_prf |
---|
| 2081 | @(mfr_bind … (λptr.λ_:True.ptr)) |
---|
[2556] | 2082 | [ change with (pointer_of_address 〈?,?〉) in |
---|
| 2083 | match (pointer_of_bevals ?); |
---|
| 2084 | change with (pointer_of_address 〈?,?〉) in |
---|
| 2085 | match (pointer_of_bevals [sigma_beval ??????;?]); |
---|
| 2086 | @sigma_ptr_commute % assumption |
---|
| 2087 | ] #ptr * |
---|
| 2088 | @if_elim #_ [ @mfr_return | @res_preserve_error ] % |
---|
[2555] | 2089 | ] |
---|
| 2090 | |4: #bl * @opt_to_res_preserve #x #EQ %{I} @EQ |
---|
| 2091 | |*: |
---|
| 2092 | ] |
---|
| 2093 | qed. |
---|
| 2094 | |
---|
[2556] | 2095 | lemma fetch_function_no_minus_one : |
---|
| 2096 | ∀F,V,i,p,bl. |
---|
| 2097 | block_id (pi1 … bl) = -1 → |
---|
| 2098 | fetch_function … (globalenv (λvars.fundef (F vars)) V i p) |
---|
| 2099 | bl = Error … [MSG BadFunction]. |
---|
| 2100 | #F#V#i#p ** #r #id #EQ1 #EQ2 destruct |
---|
| 2101 | whd in match fetch_function; normalize nodelta |
---|
| 2102 | >globalenv_no_minus_one |
---|
| 2103 | cases (symbol_for_block ???) normalize // |
---|
| 2104 | qed. |
---|
| 2105 | |
---|
[2559] | 2106 | lemma entry_sigma_commute: |
---|
| 2107 | ∀ p,p',graph_prog,sigma.good_sigma p graph_prog sigma → |
---|
| 2108 | ∀bl,f1,fn1. |
---|
| 2109 | (fetch_function ? (globalenv_noinit … graph_prog) bl = |
---|
| 2110 | return 〈f1,Internal ? fn1〉) → |
---|
| 2111 | ∃prf. |
---|
| 2112 | sigma_pc p p' graph_prog sigma |
---|
[2808] | 2113 | (pc_of_point (mk_sem_graph_params p p') bl (joint_if_entry ?? fn1)) prf = |
---|
| 2114 | pc_of_point (mk_sem_lin_params p p') bl 0. |
---|
[2559] | 2115 | #p #p' #graph_prog #sigma #good #bl #f1 #fn1 #fn1_spec |
---|
| 2116 | cases (good fn1) * #entry_in #_ #_ |
---|
| 2117 | % [ @hide_prf % | whd in match sigma_pc; normalize nodelta @opt_safe_elim #pc ] |
---|
| 2118 | whd in match sigma_pc_opt; normalize nodelta |
---|
| 2119 | >eqZb_false whd in match (pc_block ?); |
---|
| 2120 | [2,4: % #EQbl |
---|
| 2121 | >(fetch_function_no_minus_one … graph_prog … EQbl) in fn1_spec; |
---|
| 2122 | whd in ⊢ (???%→?); #ABS destruct(ABS) ] |
---|
| 2123 | normalize nodelta whd in match fetch_internal_function; |
---|
| 2124 | normalize nodelta >fn1_spec >m_return_bind >point_of_pc_of_point |
---|
| 2125 | >entry_in whd in ⊢ (??%%→?); #EQ destruct(EQ) % |
---|
| 2126 | qed. |
---|
| 2127 | |
---|
[2553] | 2128 | lemma eval_call_ok : |
---|
| 2129 | ∀p,p',graph_prog. |
---|
| 2130 | let lin_prog ≝ linearise p graph_prog in |
---|
| 2131 | ∀stack_sizes. |
---|
[2555] | 2132 | ∀sigma. good_sigma p graph_prog sigma → |
---|
| 2133 | ∀gss : good_state_sigma p p' graph_prog sigma. |
---|
[2553] | 2134 | ∀st,st',f,fn,called,args,dest,nxt. |
---|
| 2135 | ∀prf : well_formed_state_pc … gss st. |
---|
[2808] | 2136 | fetch_statement (mk_sem_graph_params p p') … |
---|
[2555] | 2137 | (globalenv_noinit ? graph_prog) (pc … st) = |
---|
| 2138 | return 〈f, fn, |
---|
| 2139 | sequential … (CALL (mk_graph_params p) … called args dest ) nxt〉 → |
---|
[2556] | 2140 | eval_state … (ev_genv … (graph_prog_params … graph_prog stack_sizes)) st = |
---|
| 2141 | return st' → |
---|
[2553] | 2142 | (* let st_pc' ≝ mk_state_pc ? st' |
---|
[2808] | 2143 | (succ_pc (mk_sem_graph_params p p') … |
---|
[2553] | 2144 | (pc … st) nxt) in |
---|
| 2145 | ∀prf'. |
---|
[2808] | 2146 | fetch_statement (mk_sem_lin_params p p') … |
---|
[2553] | 2147 | (globalenv_noinit … lin_prog) |
---|
[2808] | 2148 | (succ_pc (mk_sem_lin_params p p') (sigma_pc … (pc … st) (proj1 … prf)) it) = |
---|
[2553] | 2149 | return 〈f, \fst (linearise_int_fun … fn), final (mk_lin_params p) … (GOTO … nxt)〉 → |
---|
[2808] | 2150 | pc_of_label (mk_sem_lin_params p p') ? |
---|
[2553] | 2151 | (globalenv_noinit ? (linearise p … graph_prog)) |
---|
| 2152 | (pc_block (pc … st)) |
---|
| 2153 | nxt = return sigma_pc p p' graph_prog sigma |
---|
[2808] | 2154 | (succ_pc (mk_sem_graph_params p p') (pc … st) nxt) prf' →*) |
---|
[2553] | 2155 | let st2_pre_call ≝ sigma_state_pc … gss st prf in |
---|
| 2156 | ∃is_call, is_call'. |
---|
| 2157 | ∃prf'. |
---|
| 2158 | let st2_after_call ≝ sigma_state_pc … gss st' prf' in |
---|
| 2159 | joint_call_ident (lin_prog_params … (linearise … graph_prog) stack_sizes) «st2_pre_call, is_call'» = |
---|
| 2160 | joint_call_ident (graph_prog_params … graph_prog stack_sizes) «st, is_call» ∧ |
---|
| 2161 | eval_state … (ev_genv … (lin_prog_params … (linearise … graph_prog) stack_sizes)) |
---|
| 2162 | st2_pre_call = return st2_after_call. |
---|
[2555] | 2163 | #p #p' #graph_prog #stack_sizes #sigma #good #gss #st #st1 #f #fn |
---|
| 2164 | #called #args #dest #nxt #prf #fetch_spec |
---|
[2556] | 2165 | cases(fetch_statement_sigma_commute … good (proj2 … (proj1 … prf)) … fetch_spec) #_ |
---|
[2555] | 2166 | normalize nodelta * #lin_fetch_spec #_ |
---|
[2556] | 2167 | whd in match eval_state in ⊢ (%→?); normalize nodelta >fetch_spec |
---|
| 2168 | >m_return_bind >m_return_bind whd in match eval_statement_advance; |
---|
[2555] | 2169 | whd in match eval_seq_advance; whd in match eval_seq_call; normalize nodelta |
---|
| 2170 | @('bind_inversion) #bl #H lapply (err_eq_from_io ????? H) -H #bl_spec |
---|
| 2171 | @('bind_inversion) * #id #int_f #H lapply (err_eq_from_io ????? H) -H |
---|
| 2172 | cases int_f -int_f [ #fn | #ext_f] #int_f_spec normalize nodelta |
---|
| 2173 | [2:#H @('bind_inversion H) -H #st' #H #_ @('bind_inversion H) -H #vals #_ |
---|
| 2174 | @'bind_inversion #vals' #_ whd in ⊢ (??%%→?); #ABS destruct(ABS) ] |
---|
[2556] | 2175 | #H lapply (err_eq_from_io ????? H) -H |
---|
| 2176 | #H @('bind_inversion H) -H #st_no_pc #save_frame_spec |
---|
| 2177 | >m_bind_bind |
---|
| 2178 | #H @('bind_inversion H) -H #stack_size #H lapply (opt_eq_from_res ???? H) -H |
---|
| 2179 | whd in match (stack_sizes ?); |
---|
| 2180 | #stack_size_spec |
---|
| 2181 | >m_bind_bind |
---|
| 2182 | #H @('bind_inversion H) -H #st_no_pc' #set_call_spec |
---|
| 2183 | >m_return_bind whd in ⊢ (??%%→?); |
---|
| 2184 | whd in match set_no_pc; normalize nodelta #EQ destruct(EQ) |
---|
| 2185 | % |
---|
[2555] | 2186 | [ @hide_prf |
---|
| 2187 | whd in match joint_classify; normalize nodelta >fetch_spec >m_return_bind |
---|
| 2188 | normalize nodelta whd in match joint_classify_step; |
---|
| 2189 | whd in match joint_classify_seq; normalize nodelta |
---|
| 2190 | >bl_spec >m_return_bind >int_f_spec normalize nodelta % |
---|
[2556] | 2191 | | cases(block_of_call_sigma_commute p p' graph_prog sigma gss ?? (proj2 … prf) ? |
---|
| 2192 | bl_spec) |
---|
| 2193 | * #lin_bl_spec |
---|
| 2194 | generalize in match (fetch_function_transf … graph_prog … |
---|
| 2195 | (λvars.transf_fundef … (λf_in.\fst(linearise_int_fun ?? f_in))) |
---|
| 2196 | … int_f_spec : fetch_function … (globalenv_noinit … (linearise … graph_prog)) bl = ?) in ⊢ ?; |
---|
| 2197 | #lin_int_f_spec |
---|
| 2198 | % |
---|
[2555] | 2199 | [ @hide_prf whd in match joint_classify; normalize nodelta >lin_fetch_spec |
---|
| 2200 | >m_return_bind normalize nodelta whd in match joint_classify_step; |
---|
| 2201 | whd in match joint_classify_seq; normalize nodelta |
---|
[2556] | 2202 | >lin_bl_spec >m_return_bind |
---|
| 2203 | >lin_int_f_spec % |
---|
| 2204 | | cases (save_frame_commute … gss … save_frame_spec) in ⊢ ?; |
---|
| 2205 | [2: @hide_prf cases st in prf; // ] |
---|
| 2206 | #st_no_pc_wf #lin_save_frame_spec |
---|
| 2207 | cases (setup_call_commute … gss … st_no_pc_wf … set_call_spec) in ⊢ ?; |
---|
| 2208 | #st_no_pc_wf' #lin_set_call_spec |
---|
| 2209 | cases (allocate_locals_commute … gss … (joint_if_locals … fn) … st_no_pc_wf') |
---|
| 2210 | #st_no_pc_wf'' #lin_allocate_locals_spec |
---|
[2559] | 2211 | cases(entry_sigma_commute p p' graph_prog sigma good … int_f_spec) |
---|
| 2212 | #entry_prf #entry_spec |
---|
[2556] | 2213 | % [ @hide_prf %{st_no_pc_wf''} %{entry_prf} @(proj1 … (proj1 … prf)) ] |
---|
| 2214 | % [ whd in match joint_call_ident; normalize nodelta |
---|
| 2215 | >lin_fetch_spec in ⊢ (??match % with [ _ ⇒ ? | _ ⇒ ?]?); |
---|
| 2216 | >fetch_spec in ⊢ (???match % with [ _ ⇒ ? | _ ⇒ ?]); |
---|
| 2217 | normalize nodelta |
---|
| 2218 | >lin_bl_spec >bl_spec >m_return_bind >m_return_bind |
---|
| 2219 | whd in match fetch_internal_function; normalize nodelta |
---|
| 2220 | >lin_int_f_spec >int_f_spec % |
---|
| 2221 | | whd in match eval_state; normalize nodelta |
---|
| 2222 | >lin_fetch_spec in ⊢ (??%?); >m_return_bind in ⊢ (??%?); |
---|
| 2223 | whd in match eval_statement_no_pc; normalize nodelta |
---|
| 2224 | whd in match eval_seq_no_pc; normalize nodelta |
---|
| 2225 | >m_return_bind in ⊢ (??%?); |
---|
| 2226 | whd in match eval_statement_advance; whd in match eval_seq_advance; |
---|
| 2227 | whd in match eval_seq_call; normalize nodelta |
---|
| 2228 | >lin_bl_spec in ⊢ (??%?); >m_return_bind in ⊢ (??%?); |
---|
| 2229 | >lin_int_f_spec in ⊢ (??%?); >m_return_bind in ⊢ (??%?); |
---|
| 2230 | normalize nodelta |
---|
| 2231 | >lin_save_frame_spec >m_return_bind |
---|
| 2232 | >m_bind_bind whd in match (stack_sizes ?); |
---|
| 2233 | >stack_size_spec >m_return_bind |
---|
| 2234 | >lin_set_call_spec >m_return_bind |
---|
| 2235 | >lin_allocate_locals_spec |
---|
| 2236 | <entry_spec % |
---|
[2555] | 2237 | ] |
---|
[2556] | 2238 | ] |
---|
| 2239 | ] |
---|
| 2240 | qed. |
---|
| 2241 | |
---|
| 2242 | lemma eval_goto_ok : |
---|
| 2243 | ∀p,p',graph_prog. |
---|
| 2244 | let lin_prog ≝ linearise p graph_prog in |
---|
| 2245 | ∀stack_sizes. |
---|
| 2246 | ∀sigma.good_sigma p graph_prog sigma → |
---|
| 2247 | ∀gss : good_state_sigma p p' graph_prog sigma. |
---|
| 2248 | ∀st,st',f,fn,nxt. |
---|
| 2249 | ∀prf : well_formed_state_pc … gss st. |
---|
[2808] | 2250 | fetch_statement (mk_sem_graph_params p p') … |
---|
[2556] | 2251 | (globalenv_noinit ? graph_prog) (pc … st) = |
---|
| 2252 | return 〈f, fn, final … (GOTO (mk_graph_params p) … nxt)〉 → |
---|
| 2253 | eval_state … (ev_genv … (graph_prog_params … graph_prog stack_sizes)) st = |
---|
| 2254 | return st' → |
---|
| 2255 | ∃prf'. |
---|
| 2256 | ∃taf : trace_any_any_free (lin_abstract_status p p' lin_prog stack_sizes) |
---|
| 2257 | (sigma_state_pc … gss st prf) |
---|
| 2258 | (sigma_state_pc … gss st' prf'). |
---|
| 2259 | bool_to_Prop (taaf_non_empty … taf). |
---|
| 2260 | #p #p' #graph_prog #stack_sizes #sigma #good #gss #st #st' #f #fn |
---|
| 2261 | #nxt #prf #EQfetch |
---|
| 2262 | whd in match eval_state; normalize nodelta >EQfetch |
---|
| 2263 | >m_return_bind >m_return_bind |
---|
| 2264 | whd in match eval_statement_advance; normalize nodelta |
---|
| 2265 | whd in match goto; normalize nodelta |
---|
| 2266 | #H lapply (err_eq_from_io ????? H) -H |
---|
| 2267 | #H @('bind_inversion H) #pc' |
---|
| 2268 | @('bind_inversion EQfetch) * #curr_i #curr_fn #EQfetchfn |
---|
| 2269 | #H @('bind_inversion H) -H #stmt' #_ whd in ⊢ (??%%→?); |
---|
| 2270 | #EQ destruct(EQ) |
---|
| 2271 | >(graph_pc_of_label … EQfetchfn) whd in ⊢ (??%%→??%%→?); |
---|
| 2272 | #EQ1 #EQ2 destruct |
---|
| 2273 | cases (fetch_statement_sigma_commute … good … (proj2 … (proj1 … prf)) … EQfetch) |
---|
| 2274 | normalize nodelta ** #prf' #EQpc_of_label' * |
---|
| 2275 | #EQfetch' |
---|
| 2276 | -H |
---|
| 2277 | % |
---|
| 2278 | [ @hide_prf cases st in prf prf'; -st #st #pc #popped ** #H1 #H2 #H3 |
---|
| 2279 | #H4 %{H3} %{H1 H4} ] |
---|
| 2280 | %{(taaf_step … (taa_base …) …) I} |
---|
| 2281 | [ whd whd in ⊢ (??%?); >EQfetch' % |
---|
| 2282 | | whd whd in match eval_state; normalize nodelta |
---|
| 2283 | >EQfetch' >m_return_bind >m_return_bind |
---|
| 2284 | whd in match eval_statement_advance; whd in match goto; |
---|
| 2285 | normalize nodelta >pc_block_sigma_commute >EQpc_of_label' |
---|
| 2286 | >m_return_bind % |
---|
[2555] | 2287 | ] |
---|
[2556] | 2288 | qed. |
---|
| 2289 | |
---|
| 2290 | lemma eval_cond_ok : |
---|
| 2291 | ∀p,p',graph_prog. |
---|
| 2292 | let lin_prog ≝ linearise p graph_prog in |
---|
| 2293 | ∀stack_sizes. |
---|
| 2294 | ∀sigma.good_sigma p graph_prog sigma → |
---|
| 2295 | ∀gss : good_state_sigma p p' graph_prog sigma. |
---|
| 2296 | ∀st,st',f,fn,a,ltrue,lfalse. |
---|
| 2297 | ∀prf : well_formed_state_pc … gss st. |
---|
[2808] | 2298 | fetch_statement (mk_sem_graph_params p p') … |
---|
[2556] | 2299 | (globalenv_noinit ? graph_prog) (pc … st) = |
---|
| 2300 | return 〈f, fn, sequential … (COND (mk_graph_params p) … a ltrue) lfalse〉 → |
---|
| 2301 | eval_state … (ev_genv … (graph_prog_params … graph_prog stack_sizes)) st = |
---|
| 2302 | return st' → |
---|
| 2303 | as_costed (joint_abstract_status (graph_prog_params p p' graph_prog stack_sizes)) |
---|
| 2304 | st' → |
---|
| 2305 | ∃prf'. |
---|
| 2306 | ∃taf : trace_any_any_free (lin_abstract_status p p' lin_prog stack_sizes) |
---|
| 2307 | (sigma_state_pc … gss st prf) |
---|
| 2308 | (sigma_state_pc … gss st' prf'). |
---|
| 2309 | bool_to_Prop (taaf_non_empty … taf). |
---|
| 2310 | #p #p' #graph_prog #stack_sizes #sigma #good #gss #st #st' #f #fn |
---|
| 2311 | #a #ltrue #lfalse #prf #EQfetch |
---|
| 2312 | whd in match eval_state; normalize nodelta >EQfetch |
---|
| 2313 | >m_return_bind >m_return_bind |
---|
| 2314 | whd in match eval_statement_advance; normalize nodelta |
---|
| 2315 | #H @('bind_inversion (err_eq_from_io ????? H)) |
---|
| 2316 | @bv_pc_other [ #pc' #p #_ whd in ⊢ (??%%→?); #ABS destruct(ABS) ] |
---|
| 2317 | #bv #bv_no_pc #EQretrieve |
---|
| 2318 | cut |
---|
| 2319 | (∃prf'.acca_retrieve ?? (p' ?) (sigma_state_pc p p' graph_prog sigma gss st prf) a = |
---|
| 2320 | return sigma_beval p p' graph_prog sigma bv prf') |
---|
| 2321 | [ @acca_retrieve_commute assumption ] |
---|
| 2322 | * #bv_prf >(sigma_bv_no_pc … bv_no_pc) #EQretrieve' |
---|
| 2323 | -H #H @('bind_inversion H) * |
---|
| 2324 | #EQbool normalize nodelta -H |
---|
| 2325 | [ whd in match goto; normalize nodelta |
---|
| 2326 | #H @('bind_inversion H) -H #pc' |
---|
| 2327 | @('bind_inversion EQfetch) * #curr_i #curr_fn #EQfetchfn |
---|
| 2328 | #H @('bind_inversion H) -H #stmt' #_ whd in ⊢ (??%%→?); |
---|
| 2329 | #EQ destruct(EQ) |
---|
| 2330 | >(graph_pc_of_label … EQfetchfn) whd in ⊢ (??%%→??%%→?); |
---|
| 2331 | #EQ1 #EQ2 destruct |
---|
| 2332 | | whd in ⊢ (??%%→?); |
---|
| 2333 | #EQ destruct(EQ) |
---|
[2555] | 2334 | ] |
---|
[2556] | 2335 | #ncost |
---|
| 2336 | cases (fetch_statement_sigma_commute … good … (proj2 … (proj1 … prf)) … EQfetch) |
---|
| 2337 | normalize nodelta ** #prf' #EQpc_of_label' ** #prf'' ** |
---|
| 2338 | #EQfetch' #nxt_spec |
---|
| 2339 | % [1,3,5,7: @hide_prf |
---|
| 2340 | cases st in prf prf' prf''; |
---|
| 2341 | -st #st #pc #popped ** #H1 #H2 #H3 #H4 #H5 |
---|
| 2342 | %{H3} %{H1} assumption ] |
---|
| 2343 | %{(taaf_step_jump … (taa_base …) …) I} |
---|
| 2344 | [1,4,7,10: whd |
---|
| 2345 | >(as_label_sigma_commute … good) assumption |
---|
| 2346 | |2,5,8,11: whd whd in ⊢ (??%?); |
---|
| 2347 | >EQfetch' % |
---|
| 2348 | |*: whd whd in match eval_state; normalize nodelta >EQfetch' |
---|
| 2349 | >m_return_bind >m_return_bind |
---|
| 2350 | whd in match eval_statement_advance; normalize nodelta >EQretrieve' |
---|
| 2351 | >m_return_bind >EQbool >m_return_bind normalize nodelta |
---|
| 2352 | [1,2: whd in match goto; normalize nodelta |
---|
| 2353 | >pc_block_sigma_commute >EQpc_of_label' % |
---|
| 2354 | |3: whd in match next; normalize nodelta >nxt_spec % |
---|
| 2355 | |4: whd in match goto; normalize nodelta |
---|
| 2356 | >pc_block_sigma_commute >nxt_spec % |
---|
| 2357 | ] |
---|
[2555] | 2358 | ] |
---|
[2556] | 2359 | qed. |
---|
| 2360 | |
---|
| 2361 | lemma eval_return_ok : |
---|
| 2362 | ∀p,p',graph_prog. |
---|
| 2363 | let lin_prog ≝ linearise p graph_prog in |
---|
| 2364 | ∀stack_sizes. |
---|
| 2365 | ∀sigma.∀good : good_sigma p graph_prog sigma. |
---|
| 2366 | ∀gss : good_state_sigma p p' graph_prog sigma. |
---|
| 2367 | ∀st,st',f,fn. |
---|
| 2368 | ∀prf : well_formed_state_pc … gss st. |
---|
[2808] | 2369 | fetch_statement (mk_sem_graph_params p p') … |
---|
[2556] | 2370 | (globalenv_noinit ? graph_prog) (pc … st) = |
---|
| 2371 | return 〈f, fn, final … (RETURN (mk_graph_params p) … )〉 → |
---|
| 2372 | eval_state … (ev_genv … (graph_prog_params … graph_prog stack_sizes)) st = |
---|
| 2373 | return st' → |
---|
| 2374 | joint_classify (lin_prog_params … (linearise … graph_prog) stack_sizes) |
---|
| 2375 | (sigma_state_pc … st prf) = Some ? cl_return ∧ |
---|
| 2376 | ∃prf'. |
---|
| 2377 | ∃st2_after_ret. |
---|
| 2378 | ∃taf : trace_any_any_free (lin_abstract_status p p' lin_prog stack_sizes) |
---|
| 2379 | st2_after_ret |
---|
| 2380 | (sigma_state_pc … gss st' prf'). |
---|
| 2381 | (if taaf_non_empty … taf then |
---|
| 2382 | ¬as_costed (joint_abstract_status (lin_prog_params p p' (linearise … graph_prog) stack_sizes)) |
---|
| 2383 | st2_after_ret |
---|
| 2384 | else True) ∧ |
---|
| 2385 | eval_state … (ev_genv … (lin_prog_params … (linearise … graph_prog) stack_sizes)) |
---|
| 2386 | (sigma_state_pc … st prf) = |
---|
| 2387 | return st2_after_ret ∧ |
---|
| 2388 | ret_rel … (linearise_status_rel … gss good) st' st2_after_ret. |
---|
| 2389 | #p #p' #graph_prog #stack_sizes #sigma #good #gss #st #st' #f #fn |
---|
| 2390 | #prf #EQfetch |
---|
| 2391 | whd in match eval_state; normalize nodelta >EQfetch |
---|
| 2392 | >m_return_bind >m_return_bind |
---|
| 2393 | whd in match eval_statement_advance; normalize nodelta |
---|
| 2394 | #H lapply (err_eq_from_io ????? H) -H |
---|
| 2395 | #H @('bind_inversion H) -H #st1' #EQpop |
---|
| 2396 | cut (∃prf'. |
---|
| 2397 | (pop_frame … (ev_genv (lin_prog_params ? p' (linearise ? graph_prog) stack_sizes)) |
---|
| 2398 | f (\fst (pi1 ?? (linearise_int_fun ?? fn))) (sigma_state … gss st (proj2 … prf))) |
---|
| 2399 | = return sigma_state_pc … gss st1' prf') |
---|
| 2400 | [ @pop_frame_commute assumption ] |
---|
| 2401 | * #prf' #EQpop' >m_bind_bind |
---|
| 2402 | #H @('bind_inversion H) ** #call_i #call_fn |
---|
| 2403 | * [ * [ #s | #a #lbl ] #nxt | #s | * ] normalize nodelta |
---|
| 2404 | #EQfetch_ret -H |
---|
| 2405 | whd in ⊢ (??%%→?); #EQ destruct(EQ) whd in match (next ???); >graph_succ_pc |
---|
| 2406 | cases (fetch_statement_sigma_commute … good … (proj2 … (proj1 … prf)) … EQfetch) |
---|
| 2407 | #_ normalize nodelta #EQfetch' |
---|
| 2408 | cases (fetch_statement_sigma_commute … good … (proj2 … (proj1 … prf')) … EQfetch_ret) |
---|
| 2409 | normalize nodelta |
---|
| 2410 | #all_labels_in |
---|
| 2411 | * #EQfetch_ret' * #prf'' * [2: * ] #nxt_spec [2:| #EQpc_of_label'] |
---|
| 2412 | % [1,3: whd in match joint_classify; normalize nodelta |
---|
| 2413 | >EQfetch' >m_return_bind % ] |
---|
| 2414 | % [1,3: @hide_prf cases prf' * #_ #H1 #H2 %{H2} %{H1 prf''} ] |
---|
| 2415 | [ % [2: %{(taaf_base …)} |] |
---|
| 2416 | % [ %{I} ] |
---|
| 2417 | [ >EQfetch' >m_return_bind >m_return_bind normalize nodelta |
---|
| 2418 | whd in match eval_return; normalize nodelta |
---|
| 2419 | >EQpop' >m_return_bind |
---|
| 2420 | whd in match next_of_pc; normalize nodelta |
---|
| 2421 | >EQfetch_ret' >m_return_bind whd in match next; normalize nodelta |
---|
| 2422 | >nxt_spec % |
---|
| 2423 | | * #s1_pre #s1_call |
---|
| 2424 | cases (joint_classify_call … s1_call) |
---|
| 2425 | * #calling_i #calling * #call_spec * #arg * #dest * #nxt * #bl |
---|
| 2426 | * #called_i * #called ** #EQfetch_call #EQbl #EQfetch_called |
---|
| 2427 | * #s2_pre #s2_call |
---|
| 2428 | whd in ⊢ (%→?); >EQfetch_call * #EQ #_ |
---|
| 2429 | * #s1_pre_prf #EQpc_s2_pre |
---|
| 2430 | whd >EQpc_s2_pre |
---|
| 2431 | <(sigma_pc_irr … EQ) [2: @hide_prf @(proj2 … (proj1 … prf')) ] |
---|
| 2432 | >EQfetch_ret' % [ % | >nxt_spec % ] |
---|
[2555] | 2433 | ] |
---|
[2556] | 2434 | | % [2: %{(taaf_step … (taa_base …) …)} |*:] |
---|
| 2435 | [3: % [ % normalize nodelta ] |
---|
| 2436 | [2: >EQfetch' in ⊢ (??%?); |
---|
| 2437 | >m_return_bind in ⊢ (??%?); >m_return_bind in ⊢ (??%?); |
---|
| 2438 | normalize nodelta |
---|
| 2439 | whd in match eval_return; normalize nodelta |
---|
| 2440 | >EQpop' in ⊢ (??%?); >m_return_bind in ⊢ (??%?); |
---|
| 2441 | whd in match next_of_pc; normalize nodelta |
---|
| 2442 | >EQfetch_ret' in ⊢ (??%?); >m_return_bind in ⊢ (??%?); |
---|
| 2443 | whd in match next; normalize nodelta % |
---|
| 2444 | |1: normalize nodelta %* #H @H -H |
---|
| 2445 | whd in ⊢ (??%?); >nxt_spec % |
---|
| 2446 | |3: * #s1_pre #s1_call |
---|
| 2447 | cases (joint_classify_call … s1_call) |
---|
| 2448 | * #calling_i #calling * #call_spec * #arg * #dest * #nxt' * #bl |
---|
| 2449 | * #called_i * #called ** #EQfetch_call #EQbl #EQfetch_called |
---|
| 2450 | * #s2_pre #s2_call |
---|
| 2451 | whd in ⊢ (%→?); >EQfetch_call * #EQ #_ |
---|
| 2452 | * #s1_pre_prf #EQpc_s2_pre |
---|
| 2453 | whd >EQpc_s2_pre |
---|
| 2454 | <(sigma_pc_irr … EQ) [2: @hide_prf @(proj2 … (proj1 … prf')) ] |
---|
| 2455 | >EQfetch_ret' %% |
---|
[2555] | 2456 | ] |
---|
[2556] | 2457 | |1: whd whd in ⊢ (??%?); >nxt_spec % |
---|
| 2458 | |2: whd whd in match eval_state; normalize nodelta |
---|
| 2459 | >nxt_spec >m_return_bind >m_return_bind |
---|
| 2460 | whd in match eval_statement_advance; whd in match goto; normalize nodelta |
---|
| 2461 | whd in match (pc_block ?); >pc_block_sigma_commute |
---|
| 2462 | >EQpc_of_label' >m_return_bind % whd in match (set_pc ???); % |
---|
| 2463 | |*: |
---|
| 2464 | ] |
---|
[2555] | 2465 | ] |
---|
[2556] | 2466 | qed. |
---|
[2548] | 2467 | |
---|
[2559] | 2468 | |
---|
| 2469 | lemma eval_tailcall_ok : |
---|
[2556] | 2470 | ∀p,p',graph_prog. |
---|
| 2471 | let lin_prog ≝ linearise p graph_prog in |
---|
| 2472 | ∀stack_sizes. |
---|
| 2473 | ∀sigma.good_sigma p graph_prog sigma → |
---|
| 2474 | ∀gss : good_state_sigma p p' graph_prog sigma. |
---|
| 2475 | ∀st,st',f,fn,fl,called,args. |
---|
| 2476 | ∀prf : well_formed_state_pc … gss st. |
---|
[2808] | 2477 | fetch_statement (mk_sem_graph_params p p') … |
---|
[2556] | 2478 | (globalenv_noinit ? graph_prog) (pc … st) = |
---|
| 2479 | return 〈f, fn, final … (TAILCALL (mk_graph_params p) … fl called args)〉 → |
---|
| 2480 | eval_state … (ev_genv … (graph_prog_params … graph_prog stack_sizes)) st = |
---|
| 2481 | return st' → |
---|
| 2482 | let st2_pre_call ≝ sigma_state_pc … gss st prf in |
---|
| 2483 | ∃is_tailcall, is_tailcall'. |
---|
| 2484 | ∃prf'. |
---|
| 2485 | let st2_after_call ≝ sigma_state_pc … gss st' prf' in |
---|
| 2486 | joint_tailcall_ident (lin_prog_params … (linearise … graph_prog) stack_sizes) «st2_pre_call, is_tailcall'» = |
---|
| 2487 | joint_tailcall_ident (graph_prog_params … graph_prog stack_sizes) «st, is_tailcall» ∧ |
---|
| 2488 | eval_state … (ev_genv … (lin_prog_params … (linearise … graph_prog) stack_sizes)) |
---|
| 2489 | st2_pre_call = return st2_after_call. |
---|
[2559] | 2490 | #p #p' #graph_prog #stack_sizes #sigma #good #gss #st #st' #f #fn #fl #called #args |
---|
| 2491 | #prf #fetch_spec |
---|
| 2492 | cases(fetch_statement_sigma_commute … good (proj2 … (proj1 … prf)) … fetch_spec) * |
---|
| 2493 | normalize nodelta #lin_fetch_spec |
---|
| 2494 | whd in match eval_state; normalize nodelta >fetch_spec |
---|
| 2495 | >m_return_bind whd in match eval_statement_no_pc; normalize nodelta |
---|
| 2496 | >m_return_bind whd in match eval_statement_advance; whd in match eval_tailcall; |
---|
| 2497 | normalize nodelta @('bind_inversion) #bl #bl_spec |
---|
| 2498 | lapply (err_eq_from_io ????? bl_spec) -bl_spec |
---|
| 2499 | whd in match set_no_pc; normalize nodelta #bl_spec |
---|
| 2500 | cases(block_of_call_sigma_commute p p' graph_prog sigma gss ?? (proj2 … prf) ? |
---|
| 2501 | bl_spec) * #lin_bl_spec @('bind_inversion) |
---|
| 2502 | * #f1 #fn1 cases fn1 normalize nodelta -fn1 |
---|
| 2503 | [2: #ext_f #_ whd in match eval_external_call; normalize nodelta @('bind_inversion) |
---|
| 2504 | #st @('bind_inversion) #list_val #_ @('bind_inversion) #le #_ |
---|
| 2505 | whd in ⊢ (??%% → ?); #ABS destruct(ABS)] |
---|
| 2506 | #fn1 #fn1_spec lapply(err_eq_from_io ????? fn1_spec) -fn1_spec #fn1_spec |
---|
| 2507 | generalize in match (fetch_function_transf … graph_prog … |
---|
| 2508 | (λvars.transf_fundef … (λf_in.\fst(linearise_int_fun ?? f_in))) |
---|
| 2509 | … fn1_spec : fetch_function … (globalenv_noinit … (linearise … graph_prog)) bl = ?) in ⊢ ?; |
---|
| 2510 | #lin_fn1_spec |
---|
| 2511 | whd in match eval_internal_call; normalize nodelta |
---|
| 2512 | #H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H |
---|
| 2513 | #st1 #H @('bind_inversion H) -H #dim_s #dim_s_spec |
---|
| 2514 | #H @('bind_inversion H) -H #st2 #st2_spec whd in ⊢ (??%% → ??%% → ?); |
---|
| 2515 | #EQ1 #EQ2 destruct % |
---|
| 2516 | [ @hide_prf | % [@hide_prf]] |
---|
| 2517 | [1,2: whd in match joint_classify; normalize nodelta [>fetch_spec | >lin_fetch_spec] |
---|
| 2518 | >m_return_bind normalize nodelta whd in match joint_classify_final; |
---|
| 2519 | normalize nodelta [>bl_spec|>lin_bl_spec] >m_return_bind |
---|
| 2520 | [>fn1_spec|>lin_fn1_spec] % |
---|
| 2521 | | cases (setup_call_commute … gss … (proj2 … prf) … st2_spec) #wf_st2 #lin_st2_spec |
---|
| 2522 | cases (allocate_locals_commute … gss … (joint_if_locals … fn1) ? wf_st2) |
---|
| 2523 | #wf_all_st2 #all_st2_spec |
---|
| 2524 | cases(entry_sigma_commute p p' graph_prog sigma good … fn1_spec) #wf_pc |
---|
| 2525 | #pc_spec |
---|
| 2526 | % |
---|
| 2527 | [ @hide_prf % |
---|
| 2528 | [ % [@(proj1 … (proj1 … prf)) | @(wf_pc)] |
---|
| 2529 | | @(wf_all_st2) |
---|
| 2530 | ] |
---|
| 2531 | | % |
---|
| 2532 | [ whd in match joint_tailcall_ident; normalize nodelta |
---|
| 2533 | >lin_fetch_spec in ⊢ (??match % with [ _ ⇒ ? | _ ⇒ ?]?); |
---|
| 2534 | >fetch_spec in ⊢ (???match % with [ _ ⇒ ? | _ ⇒ ?]); |
---|
| 2535 | normalize nodelta >lin_bl_spec >bl_spec >m_return_bind >m_return_bind |
---|
| 2536 | whd in match fetch_internal_function; normalize nodelta |
---|
| 2537 | >fn1_spec >lin_fn1_spec % |
---|
| 2538 | | >lin_fetch_spec in ⊢ (??%?); >m_return_bind in ⊢ (??%?); |
---|
| 2539 | normalize nodelta >m_return_bind in ⊢ (??%?); |
---|
| 2540 | >lin_bl_spec in ⊢ (??%?); >m_return_bind in ⊢ (??%?); |
---|
| 2541 | >lin_fn1_spec in ⊢ (??%?); >m_return_bind in ⊢ (??%?); |
---|
| 2542 | normalize nodelta >dim_s_spec in ⊢ (??%?); >m_return_bind in ⊢ (??%?); |
---|
| 2543 | >lin_st2_spec in ⊢ (??%?); >m_return_bind in ⊢ (??%?); |
---|
| 2544 | >all_st2_spec in ⊢ (??%?); whd in ⊢ (??%%); @eq_f @eq_f2 [2: %] |
---|
| 2545 | >pc_spec % |
---|
| 2546 | ] |
---|
| 2547 | ] |
---|
| 2548 | ] |
---|
| 2549 | qed. |
---|
| 2550 | |
---|
[2445] | 2551 | |
---|
[2442] | 2552 | lemma linearise_ok: |
---|
| 2553 | ∀p,p',graph_prog. |
---|
| 2554 | let lin_prog ≝ linearise ? graph_prog in |
---|
[2529] | 2555 | ∀stack_sizes. |
---|
| 2556 | (∀sigma.good_state_sigma p p' graph_prog sigma) → |
---|
[2808] | 2557 | ∃[1] R. |
---|
[2442] | 2558 | status_simulation |
---|
[2529] | 2559 | (graph_abstract_status p p' graph_prog stack_sizes) |
---|
| 2560 | (lin_abstract_status p p' lin_prog stack_sizes) R). |
---|
[2464] | 2561 | #p #p' #graph_prog |
---|
[2529] | 2562 | letin sigma ≝ (λfn.\snd (linearise_int_fun … fn) : sigma_map … graph_prog) |
---|
| 2563 | cut (∀fn.good_local_sigma … (sigma fn)) |
---|
| 2564 | [6: #fn @(pi2 … (linearise_int_fun … fn)) |*:] |
---|
| 2565 | #good |
---|
| 2566 | #stack_sizes |
---|
[2484] | 2567 | #gss lapply (gss sigma) -gss #gss |
---|
[2529] | 2568 | %{(linearise_status_rel p p' graph_prog stack_sizes sigma gss good)} |
---|
[2484] | 2569 | whd in match graph_abstract_status; |
---|
| 2570 | whd in match lin_abstract_status; |
---|
| 2571 | whd in match graph_prog_params; |
---|
| 2572 | whd in match lin_prog_params; |
---|
| 2573 | normalize nodelta |
---|
| 2574 | whd |
---|
| 2575 | whd in ⊢ (%→%→%→?); |
---|
| 2576 | whd in ⊢ (?(?%)→?(?%)→?(?%)→?); |
---|
| 2577 | whd in ⊢ (?%→?%→?%→?); |
---|
| 2578 | #st1 #st1' #st2 |
---|
| 2579 | whd in ⊢ (%→?); |
---|
| 2580 | change with |
---|
[2808] | 2581 | (eval_state (mk_sem_graph_params p p') (prog_var_names ???) ?? = ? → ?) |
---|
[2556] | 2582 | #EQeval |
---|
| 2583 | @('bind_inversion EQeval) |
---|
| 2584 | ** #curr_f #curr_fn #stmt #H lapply (err_eq_from_io ????? H) -H #EQfetch |
---|
| 2585 | #_ * #prf #EQst2 |
---|
| 2586 | cases stmt in EQfetch; -stmt |
---|
[2547] | 2587 | [ @cond_call_other |
---|
| 2588 | [ #a #ltrue | #f #args #dest | #s #s_no_call ] #nxt | #s | * ] |
---|
| 2589 | normalize nodelta |
---|
[2556] | 2590 | #EQfetch |
---|
| 2591 | change with (joint_classify ??) in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]); |
---|
| 2592 | [ (* COND *) |
---|
| 2593 | whd in match joint_classify; normalize nodelta; |
---|
| 2594 | >EQfetch in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]); |
---|
[2547] | 2595 | normalize nodelta |
---|
[2556] | 2596 | #ncost |
---|
| 2597 | cases (eval_cond_ok … good … prf EQfetch EQeval ncost) |
---|
| 2598 | #prf' * #taf #taf_ne |
---|
| 2599 | destruct(EQst2) |
---|
| 2600 | % [2: %{taf} |*:] |
---|
| 2601 | >taf_ne normalize nodelta |
---|
| 2602 | % [ %{I} %{prf'} % ] |
---|
| 2603 | whd >(as_label_sigma_commute … good) % |
---|
| 2604 | | (* CALL *) |
---|
| 2605 | cases (eval_call_ok … good … prf EQfetch EQeval) |
---|
| 2606 | #is_call * #is_call' * |
---|
| 2607 | #prf' * #eq_call #EQeval' |
---|
| 2608 | destruct(EQst2) |
---|
| 2609 | >is_call in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]); normalize nodelta |
---|
| 2610 | #ignore %{«?, is_call'»} |
---|
| 2611 | % [ %{eq_call} %{prf} % ] |
---|
| 2612 | % [2: % [2: %{(taa_base …)} %{(taa_base …)} % [ %{EQeval'} %{prf'} % ]] |*:] |
---|
| 2613 | whd >(as_label_sigma_commute … good) % |
---|
[2547] | 2614 | | (* SEQ *) |
---|
[2556] | 2615 | whd in match joint_classify; normalize nodelta; |
---|
| 2616 | >EQfetch in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]); |
---|
[2547] | 2617 | normalize nodelta |
---|
[2556] | 2618 | whd in match joint_classify_step; normalize nodelta |
---|
| 2619 | >no_call_other [2: assumption ] normalize nodelta |
---|
| 2620 | cases (eval_seq_no_call_ok … good … prf EQfetch EQeval) [2: assumption ] |
---|
| 2621 | #prf' * #taf #taf_ne |
---|
| 2622 | destruct(EQst2) |
---|
| 2623 | % [2: %{taf} |*:] |
---|
| 2624 | >taf_ne normalize nodelta % [ %{I} ] |
---|
| 2625 | [ %{prf'} % | whd >(as_label_sigma_commute … good) % ] |
---|
| 2626 | | (* FIN *) cases s in EQfetch; |
---|
| 2627 | [ (* GOTO *) #lbl #EQfetch |
---|
| 2628 | whd in match joint_classify; normalize nodelta; |
---|
| 2629 | >EQfetch in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]); |
---|
[2529] | 2630 | normalize nodelta |
---|
[2556] | 2631 | cases (eval_goto_ok … good … prf EQfetch EQeval) |
---|
| 2632 | #prf' * #taf #taf_ne |
---|
| 2633 | destruct(EQst2) |
---|
| 2634 | % [2: %{taf} |*:] |
---|
| 2635 | >taf_ne normalize nodelta % [ %{I} ] |
---|
| 2636 | [ %{prf'} % | whd >(as_label_sigma_commute … good) % ] |
---|
| 2637 | | (* RETURN *) #EQfetch |
---|
| 2638 | whd in match joint_classify; normalize nodelta; |
---|
| 2639 | >EQfetch in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]); |
---|
| 2640 | normalize nodelta |
---|
| 2641 | cases (eval_return_ok … good … prf EQfetch EQeval) |
---|
| 2642 | #is_ret' * |
---|
| 2643 | #prf' * #after_ret * #taf ** #taf_prf #EQeval' #ret_prf |
---|
| 2644 | destruct(EQst2) |
---|
| 2645 | % [2: % [2: % [2: %{(taa_base …)} %{taf} ]] |*:] |
---|
| 2646 | % [2: whd >(as_label_sigma_commute … good) % ] |
---|
| 2647 | %{ret_prf} |
---|
| 2648 | % [2: %{prf'} % ] |
---|
| 2649 | %{EQeval'} |
---|
| 2650 | %{taf_prf is_ret'} |
---|
| 2651 | | (* TAILCALL *) #fl #called #args #EQfetch |
---|
| 2652 | cases (eval_tailcall_ok … good … prf EQfetch EQeval) |
---|
| 2653 | #is_tailcall * #is_tailcall' * |
---|
| 2654 | #prf' * #eq_call #EQeval' |
---|
| 2655 | destruct(EQst2) |
---|
| 2656 | >is_tailcall in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]); normalize nodelta |
---|
| 2657 | #ignore %{«?, is_tailcall'»} |
---|
| 2658 | %{eq_call} |
---|
| 2659 | % [2: % [2: %{(taa_base …)} %{(taa_base …)} % [ %{EQeval'} %{prf'} % ]] |*:] |
---|
| 2660 | whd >(as_label_sigma_commute … good) % |
---|
[2484] | 2661 | ] |
---|
| 2662 | ] |
---|
[2447] | 2663 | qed. |
---|