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