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