Ignore:
Timestamp:
Jan 24, 2013, 7:52:38 PM (8 years ago)
Author:
piccolo
Message:

added monad machineary for ERTL to ERTLptr translation
eval_seq_no_pc case in place in ERTLptr translation

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/ERTLptr/ERTLtoERTLptrOK.ma

    r2570 r2590  
     1
    12(**************************************************************************)
    23(*       ___                                                              *)
    … …  
    1920include "common/ExtraMonads.ma".
    2021
     22axiom getLocalsFromId : ident → list register.
     23
    2124definition ERTL_status ≝
    2225λprog : ertl_program.λstack_sizes.
    … …  
    2730joint_abstract_status (mk_prog_params ERTLptr_semantics prog stack_sizes).
    2831
    29 definition sigma_map ≝ λ prog : ertl_program.
    30 joint_closed_internal_function ERTL (prog_var_names … prog) → label → option label.
     32definition sigma_map ≝ λ prog : ertlptr_program.
     33joint_closed_internal_function ERTLptr (prog_var_names … prog) → label → option label.
    3134
    3235definition sigma_pc_opt :
    33 ∀ prog : ertl_program.
     36∀ prog : ertlptr_program.
    3437sigma_map prog → program_counter → option program_counter ≝
    3538λprog,sigma,pc.
    … …  
    4346    ERTLptr_semantics (pc_block pc) ertl_ptr_point.
    4447
    45 definition well_formed_pc ≝
    46 λprog,sigma,pc.sigma_pc_opt prog sigma pc ≠ None ?.
    47 
    48 definition sigma_pc ≝
    49 λprog,sigma,pc.λprf : well_formed_pc prog sigma pc. opt_safe … prf.
    50 
    51 definition sigma_beval_opt :
    52  ∀prog : ertl_program.
     48
     49definition sigma_stored_pc ≝
     50λprog,sigma,pc. match sigma_pc_opt prog sigma pc with
     51      [None ⇒ null_pc | Some x ⇒ x].
     52     
     53     
     54definition sigma_beval :
     55 ∀prog : ertlptr_program.
    5356  sigma_map prog →
    54   beval → option beval ≝
     57  beval → beval ≝
    5558λprog,sigma,bv.
    5659match bv with
    57 [ BVpc pc prt ⇒ ! pc' ← sigma_pc_opt prog sigma pc ; return BVpc pc' prt
    58 | _ ⇒ return bv
     60[ BVpc pc prt ⇒ match sigma_pc_opt prog sigma pc with
     61                 [None ⇒ BVundef | Some x ⇒ BVpc x prt]
     62| _ ⇒ bv
    5963].
    6064
     65(*
    6166definition sigma_beval :
    6267 ∀prog,sigma,bv.
    6368 sigma_beval_opt prog sigma bv ≠ None ? → beval ≝
    6469 λprog,sigma,bv.opt_safe ….
    65 
    66 definition sigma_is_opt :
    67  ∀prog : ertl_program.
     70*)
     71definition sigma_is :
     72 ∀prog : ertlptr_program.
    6873  sigma_map prog →
    69   internal_stack → option internal_stack ≝
     74  internal_stack → internal_stack ≝
    7075λprog,sigma,is.
    7176match is with
    72 [ empty_is ⇒ return empty_is
    73 | one_is bv ⇒ ! bv' ← sigma_beval_opt … sigma bv ; return one_is bv'
     77[ empty_is ⇒ empty_is
     78| one_is bv ⇒ one_is (sigma_beval prog sigma bv)
    7479| both_is bv1 bv2 ⇒
    75   ! bv1' ← sigma_beval_opt … sigma bv1 ;
    76   ! bv2' ← sigma_beval_opt … sigma bv2 ;
    77   return both_is bv1' bv2'
     80  both_is (sigma_beval prog sigma bv1) (sigma_beval prog sigma bv2)
    7881].
    7982
    80 definition sigma_is :
    81  ∀prog,sigma,is.
    82  sigma_is_opt prog sigma is ≠ None ? → internal_stack ≝
    83  λprog,sigma,is.opt_safe ….
     83lemma sigma_is_empty : ∀prog,sigma.
     84  sigma_is prog sigma empty_is = empty_is.
     85#prog #sigma %
     86qed.
     87
     88(*
     89lemma sigma_is_pop_commute :
     90 ∀prog,sigma,is,bv,is'.
     91 is_pop (sigma_is prog sigma is) =
     92       return 〈sigma_beval prog sigma bv,sigma_is prog sigma is'〉 →
     93 is_pop is = return 〈bv,is'〉.
    8494 
    85 lemma sigma_is_empty : ∀prog,sigma.
    86   ∀prf.sigma_is prog sigma empty_is prf = empty_is.
    87 #prog #sigma #prf whd in match sigma_is; normalize nodelta
    88 @opt_safe_elim #is' whd in ⊢ (??%%→?); #EQ destruct(EQ) % qed.
    89 
    90 lemma sigma_is_pop_commute :
    91  ∀prog,sigma,is.
     95 
    9296 ∀prf : sigma_is_opt prog sigma is ≠ None ?.
    9397 res_preserve …
    … …  
    122126∀b,z.block_id b < nextblock m → low_bound m b ≤ z → z < high_bound m b →
    123127  sigma_beval_opt prog sigma (contents (blocks m b) z) ≠ None ?.
    124 
     128*)
    125129
    126130
    127131definition sigma_mem :
    128  ∀prog,sigma,m.
    129  well_formed_mem prog sigma m →
    130  bemem ≝
    131  λprog,sigma,m,prf.
     132 ∀prog : ertlptr_program . sigma_map prog → bemem → bemem ≝
     133 λprog,sigma,m.
    132134 mk_mem
    133135  (λb.
    … …  
    137139      mk_block_contents l h
    138140      (λz.If Zleb l z ∧ Zltb z h then with prf'' do
    139         sigma_beval prog sigma (contents (blocks m b) z) ?
     141        sigma_beval prog sigma (contents (blocks m b) z)
    140142      else BVundef)
    141143    else empty_block OZ OZ)
    142144  (nextblock m)
    143145  (nextblock_pos m).
     146(*
    144147@hide_prf
    145148lapply prf'' lapply prf' -prf' -prf''
    … …  
    150153#zh #zl * @(prf … bid_ok zl zh)
    151154qed.
    152 
     155*)
    153156
    154157(*DOPPIONI DEI CORRISPONDENTI LEMMI IN LINEARISE_PROOF.MA *)
    155 lemma andb_false : ∀b1,b2.andb b1 b2 = false → b1 = false ∨ b2 = false.
     158(*lemma andb_false : ∀b1,b2.andb b1 b2 = false → b1 = false ∨ b2 = false.
    156159** /2 by or_introl, or_intror/ normalize #ABS destruct(ABS) qed.
     160*)
    157161
    158162axiom mem_ext_eq :
    … …  
    163167      ∀z.contents bc1 z = contents bc2 z) →
    164168  nextblock m1 = nextblock m2 → m1 = m2.
     169
     170(*
    165171
    166172lemma beloadv_sigma_commute:
    … …  
    295301qed.
    296302
     303lemma ext_map_inf_eq : ∀A , B : Type[0].
     304  ∀ m : positive_map A.
     305  ∀ F, F' :  (∀a:A.(Σp:Pos. lookup_opt A p m = Some ? a) → B).
     306  (∀a',id',id'',prf,prf'. F a' «id',prf» = F' a' «id'',prf'») →
     307  map_inf A B m F = map_inf A B m F'.
     308#A #B #m elim m [#F #F' #eqFF' %] * [2:#a] normalize nodelta #l #r #Hl #Hr #F #F'
     309#eqFF' normalize [>(eqFF' a one one (refl ? (Some A a)) (refl ? (Some A a)))]
     310@eq_f2 [1,3: @Hl |*: @Hr] #a' #id' #id'' #prf' #prf'' @eqFF'
     311qed.
     312 
     313
     314lemma map_inf_add : ∀ A, B : Type[0].
     315  ∀tag : String.
     316  ∀m: identifier_map tag A.
     317  ∀F :(∀a:A.(Σid. lookup tag A m id = Some A a) → B).
     318  ∀a,id.
     319  let m' ≝ (add tag A m id a) in
     320  ∀F' :(∀a:A.(Σid. lookup tag A m' id = Some A a) → B).
     321  (∀a',id',id'',prf,prf'. F a' «id',prf» = F' a' «id'',prf'») →
     322  ∃ prf.
     323  map_inf1 A B tag m' F' =
     324  add tag B (map_inf1 A B tag m F) id (F' a «id,prf»).
     325#A #B #tag #m #F #a #id normalize nodelta #F' #eqFF' %
     326[@hide_prf @(lookup_add_hit tag A m ? ?)]
     327lapply eqFF' -eqFF' lapply F' -F' lapply id -id lapply a -a lapply F -F
     328cases m -m #m elim m
     329[ #F #a * #id elim id [#F' #eqFF' %] #x #Hx #F' #eqFF' whd in ⊢ (??%%);
     330  normalize nodelta @eq_f whd in match insert; normalize nodelta
     331  whd in ⊢ (??%%); normalize nodelta @eq_f2 try %
     332  lapply(Hx ??)
     333    [2,5: #a1 ** #id1 #prf1 @F' [1,3: @a1]
     334          [%{(an_identifier tag (p1 id1))} |%{(an_identifier tag (p0 id1))}] @prf1
     335    |1,4: #a' * #id' * #id'' #prf #prf' normalize nodelta @eqFF'
     336    |*: normalize nodelta whd in ⊢ (??%% → ?); normalize nodelta #EQ destruct(EQ)
     337      lapply e0 -e0 whd in ⊢ (??%% → ?); normalize nodelta normalize in ⊢ (??(???%?)? → ?);
     338      #EQ <EQ %
     339    ]
     340|  #opt_a #l1 #r1 #Hl1 #Hr1 #F #a ** [|*: #x] #F' #eqFF'
     341  [ normalize @eq_f @eq_f2 @ext_map_inf_eq #a' #id' #id'' #prf' #prf'' >eqFF' [1,4:%|*:]
     342  |*: normalize @eq_f lapply eqFF' -eqFF' lapply F' -F' lapply F -F cases opt_a
     343      [2,4: #a1] normalize nodelta #F #F' #eqFF'
     344      [3,4: @eq_f2|*: >(eqFF' a1 (an_identifier tag one) (an_identifier tag one)
     345                     (refl (option A) (Some A a1)) (refl (option A) (Some A a1)))
     346                    @eq_f2]
     347          [1,4,5,8: @ext_map_inf_eq #a' #id' #id'' #prf' #prf'' >eqFF' [1,4,7,10:%|*:]
     348          |2,6: lapply (Hr1 ? a (an_identifier tag x) ? ?)
     349          |*: lapply (Hl1 ? a (an_identifier tag x) ? ?)
     350          ]
     351          [2,3,6,7,10,11,14,15: #a ** #id #prf [2,4,6,8: @F |*: @F'] try @a %
     352                   [1,3,9,11: % @(p1 id) |5,7,13,15: % @(p0 id) |*: @hide_prf <prf %]
     353          |1,5,9,13: #a * #id' * #id'' #prf #prf' normalize nodelta @eqFF'
     354          |*: normalize in ⊢ (%→ ?); #EQ destruct(EQ) >e0 %
     355          ]
     356  ]
     357]
     358qed.
     359*)
     360
     361
    297362inductive id_is_in (A : Type[0]) : Pos →  positive_map A → Prop ≝
    298363| is_in_root : ∀l,r,opt_a. id_is_in A (one) (pm_node … opt_a l r)
    … …  
    308373                              [an_id_map p ⇒ id_is_in A x p]
    309374     ].
    310 
     375(*
    311376lemma lookup_map : ∀A,B : Type[0].
    312377  ∀tag : String.
    … …  
    355420qed.*)
    356421
     422*)
    357423
    358424lemma lookup_eq : ∀ A : Type[0].
    … …  
    387453qed.
    388454
    389 lemma update_lookup_previous : ∀ A : Type[0].
     455include alias "common/Identifiers.ma".
     456include alias "common/PositiveMap.ma".
     457
     458
     459lemma p0_neq_one : ∀x: Pos. p0 x ≠ one.
     460#x /3/
     461qed.
     462
     463lemma p1_neq_one : ∀x: Pos. p1 x ≠ one.
     464#x /3/
     465qed.
     466
     467lemma lookup_ok_to_update : ∀ A : Type[0].
    390468∀ tag : String.
    391469∀m,m' : identifier_map tag A. ∀id,a.
    392 update tag A m id a = return m' ↔
    393 (lookup tag A m' id = Some ? a) ∧ lookup tag A m id ≠ None ? ∧
     470(lookup tag A m' id = Some ? a)  → lookup tag A m id ≠ None ? →
    394471(∀ id'. id ≠ id' → (lookup tag A m id' = lookup tag A m' id') ∧
    395      (id_is_in A tag m id' ↔ id_is_in A tag m' id')).
    396 #A #tag * #m * #m' * #id #a %
    397   [ whd in ⊢ (??%% →  ?); inversion(update A ???) normalize nodelta [#_ #ABS destruct]
    398     #m1 #m1_spec #EQ destruct % [%]
    399     [  normalize @(update_lookup_opt_same … m1_spec)
    400     |3: * #id' * #id_spec' normalize %
    401         [@(update_lookup_opt_other … m1_spec ??) % #EQ @id_spec' >EQ %]
    402         lapply id_spec' lapply m1_spec -id_spec' -m1_spec
    403         (*cases id [|*:#x] -id normalize*) lapply m' -m' lapply id lapply id' -id -id'
    404         elim m [#id' #id #m' cases id [|*: #x] normalize #EQ destruct]
    405         #opt_a #l #r #Hl #Hr #id' #id #m' cases id [|*:#x] -id normalize
    406         [ cases opt_a [2:#a] normalize #EQ destruct cases id' [#H @⊥ @H %]
    407           #x #_ normalize % #H [1,2: %3 |*: %2]
    408           inversion H #l1 #r1 #opt_a1
    409           [1,4,7,10: #EQ lapply(jmeq_to_eq ??? EQ) #EQ1 @⊥
    410                      [1,2: cut(p1 x ≠ one) [1,3: @(pos_elim … x) /3/]
    411                      |*:   cut(p0 x ≠ one) [1,3: @(pos_elim … x) /3/]
    412                      ]
    413                      * #H @H >EQ1 //   
    414           |*:        #pos #H1 #_ #EQ lapply(jmeq_to_eq ??? EQ) #EQ1 destruct(EQ1)
    415                      #EQ lapply(jmeq_to_eq ??? EQ) #EQ1 destruct(EQ1) #_ assumption
    416           ]
    417         |*: inversion(update A x a ?) normalize [1,3: #_ #EQ destruct] #pos_map
    418             #pos_map_spec #EQ destruct #id_spec' % #H
    419             inversion H #l1 #l2 #opt_a1
    420             [1,4,7,10: #EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQ
    421                        #EQ1 lapply(jmeq_to_eq ??? EQ1) -EQ1 #EQ1 destruct(EQ1)
    422                        #H1 %
    423             |*: #pos #H1 #_ #EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQ
    424                 #EQ1 lapply(jmeq_to_eq ??? EQ1) -EQ1 #EQ1 destruct(EQ1)
    425                 #H2 try %2 try %3 try assumption
    426                 [ @(proj1 … (Hr ? ? pos_map pos_map_spec ?)) [#EQ1 destruct @id_spec' %]
    427                 | @(proj2 … (Hr ? ? l2 pos_map_spec ?)) [#EQ1 destruct @id_spec' %]
    428                 | @(proj1 … (Hl ? ? pos_map pos_map_spec ?)) [#EQ1 destruct @id_spec' %]
    429                 | @(proj2 … (Hl ? ? l1 pos_map_spec ?)) [#EQ1 destruct @id_spec' %]
    430                 ]
    431                 assumption
    432             ]
    433          ]     
    434     | % normalize lapply m1_spec lapply id lapply m' -id -m' elim m
    435       [#m' * [|*: #x] normalize #EQ destruct] #opt_a #l #r #Hl #Hr #m' * [|*: #x]
    436       normalize [ cases opt_a [2:#a] normalize #EQ1 #EQ2 destruct]
    437       inversion (update A x a ?) [1,3: #_ normalize #EQ destruct]
    438       #pos_map #EQpos_map normalize #EQ destruct [@Hr|@Hl] assumption
    439     ]
    440   | ** normalize in ⊢ (%→%→?); lapply id -id lapply m' -m' elim m
     472     (id_is_in A tag m id' ↔ id_is_in A tag m' id')) →
     473update tag A m id a = return m'.
     474#A #tag * #m * #m' * #id #a
     475normalize in ⊢ (%→%→?); lapply id -id lapply m' -m' elim m
    441476    [ #m' #id #m_spec' normalize in ⊢ (% → ?); * #EQ @⊥ @EQ %] #opt_a #l #r #Hl #Hr
    442477    #m' * [|*: #x] normalize in ⊢ (%→%→?); #m_spec'
    … …  
    494529            ]
    495530      ]
    496    ]
    497 qed.   
     531qed.
     532
     533
     534lemma update_ok_to_lookup : ∀ A : Type[0].
     535∀ tag : String.
     536∀m,m' : identifier_map tag A. ∀id,a.
     537update tag A m id a = return m' →
     538(lookup tag A m' id = Some ? a) ∧ lookup tag A m id ≠ None ? ∧
     539(∀ id'. id ≠ id' → (lookup tag A m id' = lookup tag A m' id') ∧
     540     (id_is_in A tag m id' ↔ id_is_in A tag m' id')).
     541#A #tag * #m * #m' * #id #a
     542whd in ⊢ (??%% →  ?); inversion(update A ???) normalize nodelta [#_ #ABS destruct]
     543    #m1 #m1_spec #EQ destruct % [%]
     544    [  normalize @(update_lookup_opt_same … m1_spec)
     545    |3: * #id' * #id_spec' normalize %
     546        [@(update_lookup_opt_other … m1_spec ??) % #EQ @id_spec' >EQ %]
     547        lapply id_spec' lapply m1_spec -id_spec' -m1_spec
     548        (*cases id [|*:#x] -id normalize*) lapply m' -m' lapply id lapply id' -id -id'
     549        elim m [#id' #id #m' cases id [|*: #x] normalize #EQ destruct]
     550        #opt_a #l #r #Hl #Hr #id' #id #m' cases id [|*:#x] -id normalize
     551        [ cases opt_a [2:#a] normalize #EQ destruct cases id' [#H @⊥ @H %]
     552          #x #_ normalize % #H [1,2: %3 |*: %2]
     553          inversion H #l1 #r1 #opt_a1
     554          [1,4,7,10: #EQ lapply(jmeq_to_eq ??? EQ) #EQ1 @⊥
     555                     [1,2: cut(p1 x ≠ one) [1,3: @(pos_elim … x) /3/]
     556                     |*:   cut(p0 x ≠ one) [1,3: @(pos_elim … x) /3/]
     557                     ]
     558                     * #H @H >EQ1 //   
     559          |*:        #pos #H1 #_ #EQ lapply(jmeq_to_eq ??? EQ) #EQ1 destruct(EQ1)
     560                     #EQ lapply(jmeq_to_eq ??? EQ) #EQ1 destruct(EQ1) #_ assumption
     561          ]
     562        |*: inversion(update A x a ?) normalize [1,3: #_ #EQ destruct] #pos_map
     563            #pos_map_spec #EQ destruct #id_spec' % #H
     564            inversion H #l1 #l2 #opt_a1
     565            [1,4,7,10: #EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQ
     566                       #EQ1 lapply(jmeq_to_eq ??? EQ1) -EQ1 #EQ1 destruct(EQ1)
     567                       #H1 %
     568            |*: #pos #H1 #_ #EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQ
     569                #EQ1 lapply(jmeq_to_eq ??? EQ1) -EQ1 #EQ1 destruct(EQ1)
     570                #H2 try %2 try %3 try assumption
     571                [ @(proj1 … (Hr ? ? pos_map pos_map_spec ?)) [#EQ1 destruct @id_spec' %]
     572                | @(proj2 … (Hr ? ? l2 pos_map_spec ?)) [#EQ1 destruct @id_spec' %]
     573                | @(proj1 … (Hl ? ? pos_map pos_map_spec ?)) [#EQ1 destruct @id_spec' %]
     574                | @(proj2 … (Hl ? ? l1 pos_map_spec ?)) [#EQ1 destruct @id_spec' %]
     575                ]
     576                assumption
     577            ]
     578         ]     
     579    | % normalize lapply m1_spec lapply id lapply m' -id -m' elim m
     580      [#m' * [|*: #x] normalize #EQ destruct] #opt_a #l #r #Hl #Hr #m' * [|*: #x]
     581      normalize [ cases opt_a [2:#a] normalize #EQ1 #EQ2 destruct]
     582      inversion (update A x a ?) [1,3: #_ normalize #EQ destruct]
     583      #pos_map #EQpos_map normalize #EQ destruct [@Hr|@Hl] assumption
     584    ]
     585qed.
     586(*
    498587               
    499                    
    500        
    501 (*
    502      
    503      
    504      
    505        -EQ
    506       lapply H -H
    507       [ lapply l1 -l1 elim l
    508         [#l1 #H lapply (H (an_identifier tag (p0 one)) ?) [% #EQ destruct] *
    509          normalize in ⊢ (%→?); cases l1 normalize [#_ #_ %] #opt_a #l2 #r2
    510          #EQ <EQ * #H1 #H2 lapply (H2 ?) [%2 %] #h inversion h #l3 #r3 #opt_a3
    511          [  #EQ lapply(jmeq_to_eq ??? EQ) #EQ1 @⊥ cut(p0 one ≠ one) [@(pos_elim … one) /3/]
    512          * #H @H >EQ1 //
    513          |*: #pos #H1 #_ #EQ lapply(jmeq_to_eq ??? EQ) #EQ1 destruct(EQ1)
    514               #EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQ1 -H destruct(EQ1) #_
    515               -h -H2 inversion H1 #l4 #r4 #opt_a4
    516               [ #_ #EQ1 lapply(jmeq_to_eq ??? EQ1) -EQ1 #EQ1 destruct(EQ1)
    517               |*: #pos #H2 #_ #_ #EQ1 lapply(jmeq_to_eq ??? EQ1) -EQ1 #EQ1
    518                   destruct(EQ1)
    519               ]
    520          ]
    521       |
    522              -EQ1 #EQ1
    523       [ #_ %
    524       |#opt_a2 #r2 #l2 #H lapply
    525          
    526 qed.
    527 *)
    528588lemma update_lookup_after : ∀ A : Type[0].
    529589∀ tag : String.
    … …  
    608668qed.
    609669
     670(*
    610671definition well_formed_register_env :
    611672∀prog : ertl_program .∀sigma : (sigma_map prog).
    … …  
    613674λprog,sigma,psd_reg.∀id,bv. lookup ?? psd_reg id = Some ? bv →
    614675sigma_beval_opt prog sigma bv ≠ None ?.
    615 
     676*)
     677*)
     678
     679definition map : ∀tag,A,B. identifier_map tag A → (A → B) → identifier_map tag B ≝
     680λtag,A,B,m,f.match m with
     681[an_id_map p ⇒ an_id_map … (map ?? f p)].
     682
     683lemma lookup_map : ∀A,B : Type[0].
     684  ∀tag : String.
     685  ∀m : identifier_map tag A.
     686  ∀ f:A → B.
     687  ∀ id.
     688lookup tag B (map tag A B m f) id =
     689! a ← lookup tag A m id; return f a.
     690#A #B #tag * #m #f * #id normalize >lookup_opt_map %
     691qed.
     692
     693lemma update_leaf_fail: ∀tag,A,i,v.
     694 update tag A (empty_map ??) i v = Error ? [MSG MissingId; CTX … i].
     695#ta #A ** [|*: #x] #v normalize %
     696qed.
     697
     698lemma update_def : ∀tag,A,m,i,v.
     699  update tag A m i v =
     700  match lookup tag A m i with
     701  [ Some _ ⇒ OK ? (add tag A m i v)
     702  | None ⇒ Error ? [MSG MissingId; CTX … i]
     703  ].
     704#tag #A #m #i #v inversion(update tag A m i v)
     705[ #m' #EQm' cases(update_ok_to_lookup ?????? EQm') * #_
     706 #H #_ elim H cases(lookup tag A m i) [#H @⊥ @H %]
     707 #x #_ normalize <EQm' lapply EQm' cases i cases m cases m' -m -m' -i
     708 normalize #m' #m #i inversion(update A i v m) normalize [#_ #ABS destruct]
     709 #m'' #EQm'' #EQ destruct(EQ) @eq_f @eq_f lapply EQm'' -EQm'' lapply i -i
     710 lapply m' -m' elim m [#m' * [2,3: #z] normalize #EQ destruct]
     711 #opt_a #l #r #Hl #Hr #m' * [2,3: #z] normalize
     712 [3: cases opt_a normalize [2: #y] #EQ destruct %
     713 |*: inversion(update A z v ?) [2,4: #m'']  #EQm'' normalize #EQ destruct
     714     [<(Hr … EQm'') | <(Hl … EQm'')] %
     715 ]
     716| #err cases m -m cases i -i #i #m normalize inversion(update A i v m) [2:#m']
     717  #EQerr normalize #EQ destruct lapply EQerr lapply i elim m
     718  [ normalize #x #_ %] #opt_a #l #r #Hl #Hr * [2,3:#z] normalize
     719 [3: cases opt_a [2:#w] normalize #EQ destruct %
     720 |*: inversion(update A z v ?) [2,4: #m'] #EQm' normalize #EQ destruct
     721     [lapply(Hr … EQm') | lapply(Hl … EQm')] cases(lookup_opt A z ?) [2,4: #a]
     722     normalize #EQ destruct %
     723 ]
     724]
     725qed.
     726
     727lemma map_add : ∀tag : String.∀A,B : Type[0].∀ f: A → B.∀m,id,v.
     728map tag A B (add tag A m id v) f = add tag B (map tag A B m f) id (f v).
     729#tag #A #B #f * #m * #id #v normalize @eq_f lapply v -v lapply id -id elim m
     730[ #id elim id [#v %] #x #IH #id normalize >IH %
     731| #opt_a #l #r #Hl #Hr * [2,3: #x| #v normalize @eq_f2 %] #v normalize @eq_f2
     732  try % [@Hr|@Hl]
     733]
     734qed.
     735
     736
     737definition restrict : ∀tag.∀A,B.
     738identifier_map tag A → identifier_map tag B → identifier_map tag A ≝
     739λtag,A,B,m1,m2.an_id_map …
     740           (merge A B A (λo,o'.match o' with [None ⇒ None ? | Some _ ⇒ o])
     741                  (match m1 with [an_id_map p1 ⇒ p1])
     742                  (match m2 with [an_id_map p2 ⇒ p2])).
     743
     744interpretation "identifier map restriction" 'intersects a b = (restrict ??? a b).
     745
     746unification hint 0 ≔ tag ; R ≟ identifier tag ⊢ list R ≡ list (identifier tag).
     747 
     748lemma map_update_commute : ∀tag : String.∀A,B : Type[0].∀f : A → B. ∀m,id,v.
     749update tag B (map tag A B m f) id (f v) =
     750!m' ← update tag A m id v; return map tag A B m' f.
     751#tag #A #B #f #m #id #v >update_def >update_def >lookup_map
     752cases (lookup tag A m id) [%] #a >m_return_bind >m_return_bind normalize nodelta
     753whd in ⊢ (???%); @eq_f @sym_eq @map_add
     754qed.
     755
     756definition is_leaf ≝ λA.λpm : positive_map A.
     757match pm with [ pm_leaf ⇒ true | _ ⇒ false ].
     758(*
     759let rec pm_clean A (pm : positive_map A) on pm : positive_map A ≝
     760match pm with
     761[ pm_leaf ⇒ pm_leaf ?
     762| pm_node o l r ⇒
     763  let l' ≝ pm_clean … l in
     764  let r' ≝ pm_clean … r in
     765  match o with
     766  [ Some _ ⇒ pm_node … o l' r'
     767  | None ⇒
     768    if is_leaf … l' ∧ is_leaf … r' then pm_leaf ? else
     769    pm_node … o l' r'
     770  ]
     771].
     772 
     773definition clean ≝ λtag,A.λm : identifier_map tag A.
     774  match m with [ an_id_map pm ⇒ an_id_map tag A (pm_clean … pm) ].
     775*)
    616776
    617777definition sigma_register_env :
    618 ∀prog : ertl_program.∀sigma : (sigma_map prog).
    619 ∀psd_env : register_env beval.
    620 well_formed_register_env prog sigma psd_env → register_env beval ≝
    621 λprog,sigma,psd_env,prf.
    622 map_inf1 ?? ?  psd_env (λbv,prf1.sigma_beval prog sigma bv ?).
    623 @hide_prf @prf cases prf1 #pi1 #H assumption
    624 qed.
    625 
    626 
     778∀prog : ertlptr_program.∀sigma : (sigma_map prog).
     779register_env beval → list register →  register_env beval ≝
     780λprog,sigma,psd_env,ids.
     781let m' ≝  map ??? psd_env (λbv.sigma_beval prog sigma bv) in
     782m' ∩ ids.
     783
     784(*
    627785definition well_formed_ertl_psd_env :
    628786∀prog : ertl_program. ∀sigma : (sigma_map prog).
    629787ertl_psd_env → Prop≝
    630788λprog,sigma,psd_env.well_formed_register_env prog sigma (psd_regs psd_env).
    631 
    632 definition sigma_ertl_psd_env :
    633 ∀prog : ertl_program. ∀ sigma : (sigma_map prog).
    634 ∀psd : ertl_psd_env.
    635 well_formed_ertl_psd_env prog sigma psd → ertl_psd_env ≝
    636 λprog,sigma,psd_env,prf.
    637 mk_ertl_psd_env
    638   (sigma_register_env …  prf)
    639   (need_spilled_no psd_env).
    640 
     789*)
     790(*
    641791let rec well_formed_frames
    642792(prog : ertl_program) (sigma : (sigma_map prog))
    … …  
    646796  | cons a tl ⇒ well_formed_ertl_psd_env prog sigma a ∧
    647797               well_formed_frames prog sigma tl
    648   ].
    649 
    650 
    651 let rec sigma_frames (prog : ertl_program) (sigma : (sigma_map prog))
    652 (l : list ertl_psd_env) (prf : well_formed_frames prog sigma l)
    653 on l : list ertl_psd_env ≝
    654 (match l with
    655   [nil ⇒ λ_ : (l = nil ?) .nil ?
    656   |cons a tl ⇒
    657      λx : (l = cons ? a tl).
    658        (sigma_ertl_psd_env prog sigma a ?)::
    659                                    (sigma_frames prog sigma tl ?)
    660      
    661   ]) (refl ? l).
    662 @hide_prf >x in prf; whd in match (well_formed_frames ???); * //
    663 qed.
    664 
     798  ].                           
     799*)
     800
     801
     802lemma lookup_restrict : ∀tag,A,B.∀a : identifier_map tag A.∀b : identifier_map tag B.
     803∀i.lookup ?? (a ∩ b) i = if i ∈ b then lookup … a i else None ?.
     804#tag #A #B * #a * #b * #i normalize >lookup_opt_merge [2: %] cases (lookup_opt B i b)
     805[2: #b] normalize % qed.
     806
     807
     808(*
     809lemma clean_add : ∀tag,A,m,i,v.clean … (add tag A m i v) = add tag A (clean … m) i v.
     810#tag #A * #m * #i #v normalize @eq_f
     811lapply m -m
     812elim i -i
     813[ * [%]
     814  * [2: #x] #l #r [%] normalize
     815  cases (pm_clean A l) normalize // cases (pm_clean A r) //
     816|*: #i #IH * normalize
     817  [1,3: >IH cases i // ]
     818  * [2,4: #x] #l #r normalize
     819  [1,2: >IH % ]
     820  >IH cases i cases (pm_clean A l) cases (pm_clean A r) normalize //
     821]
     822qed.
     823
     824lemma clean_lookup : ∀tag,A,m,i.lookup … (clean tag A m) i = lookup … m i.
     825#tag #A * #m * #i normalize lapply i -i elim m
     826[#i %] * [2: #a] #l #r #Hl #Hr * [2,3,5,6: #x] normalize in ⊢ (???%);
     827[1,3:<Hr|2,4:<Hl] normalize try % [3: @if_elim #_ %]
     828cases(pm_clean A l) in Hl; normalize
     829[2: #opt_a1 #l1 #r1 #_ %
     830|3: #H cases(pm_clean A r) normalize //
     831| #H cases(pm_clean A r) in Hr; normalize //
     832| #opt_a1 #l1 #r1 #H cases x normalize //
     833]
     834qed.   
     835
     836 
     837lemma clean_update : ∀tag,A,m,i,v.
     838! m' ← update tag A m i v; return clean … m' =
     839update tag A (clean … m) i v.
     840#tag #A #m #i #v
     841>update_def >update_def >clean_lookup cases (lookup tag A m i)
     842[ % ]
     843#m' >m_return_bind normalize nodelta >clean_add %
     844qed.
     845*)
     846lemma lookup_eq_id_map : ∀tag : String. ∀ A : Type[0].
     847∀m,m' : identifier_map tag A.
     848(∀id. lookup … m id = lookup … m' id
     849      ∧ (id_is_in A tag m id ↔ id_is_in A tag m' id)) → m=m'.
     850#tag #A * #m * #m' #H @eq_f @lookup_eq #id lapply(H (an_identifier tag id))
     851* #H1 #H2 % // assumption
     852qed.
     853
     854(*
     855lemma clean_leaf : ∀tag : String . ∀ A : Type[0].
     856∀m : identifier_map tag A. (∀ id. lookup … m id = None ?) →
     857clean ?? m = empty_map ??.
     858#tag #A * #m elim m [#_ %] #opt_a #l #r #Hl #Hr #H normalize @eq_f
     859lapply(H (an_identifier tag one)) normalize #EQ >EQ -EQ normalize
     860lapply(Hl ?) [2: lapply(Hr ?)]
     861  [1,3: * #id [lapply(H (an_identifier tag (p1 id))) | lapply(H (an_identifier tag (p0 id)))]
     862       #H assumption
     863  | normalize #EQ #EQ1 destruct >e0 >e1 normalize %
     864  ]
     865qed.
     866*)
     867lemma id_is_in_lookup : ∀tag,A,m,id,v.
     868 lookup tag A m id = Some ? v → id_is_in A tag m id.
     869#tag #A * #m * #id #a normalize lapply m -m elim id
     870[|*: #x #IH] * normalize [1,3,5: #EQ destruct] #opt_a #l #r [ #_ %] #H [%3 |%2]
     871@IH assumption
     872qed.
     873(*
     874lemma pm_clean_leaf : ∀ A : Type[0].
     875∀m : positive_map A. (∀ id. lookup_opt … id m = None ?) →
     876pm_clean ? m = pm_leaf ….
     877#A #m elim m [ #id %] #opt_a #l #r #Hl #Hr #H normalize lapply(H one) normalize
     878#EQ >EQ normalize >Hl [normalize >Hr [ %]] #id [@(H (p1 id))|@(H (p0 id))]
     879qed.
     880
     881
     882lemma pm_clean_canonic : ∀A,m,n.(∀i.lookup_opt A i m = lookup_opt A i n) →
     883  pm_clean ? m = pm_clean ? n.
     884#A #m #n lapply m -m elim n
     885[ @pm_clean_leaf ]
     886* [2: #x] #l #r #IHl #IHr *
     887  [1,3: #H @sym_eq @pm_clean_leaf #id @sym_eq @H ] #opt #l' #r' #H
     888 lapply (H one) normalize in ⊢ (%→?); #EQ destruct
     889 whd in ⊢ (??%%);
     890 >(IHl l') [1,3: >(IHr r') [1,3 : % ]] #i
     891 [1,2: @(H (p1 i)) |*: @(H (p0 i)) ] qed.
     892
     893
     894lemma clean_canonic : ∀tag,A,m,n.(∀i.lookup tag A m i = lookup tag A n i) →
     895  clean ?? m = clean ?? n.
     896#tag #A * #m * #n #H normalize @eq_f @pm_clean_canonic #i
     897lapply(H (an_identifier tag i))
     898normalize //
     899qed.
     900*)
     901lemma update_fail_lookup : ∀tag,A,m,i,v,e.update tag A m i v = Error … e → 
     902  e = [MSG MissingId; CTX … i] ∧ lookup … m i = None ?.
     903#tag #A #m #i #v #errmsg >update_def cases(lookup tag A m i) [2: #a] normalize
     904#EQ destruct % //
     905qed.
     906
     907lemma lookup_hit_update : ∀tag,A,m,i,v.i ∈ m → 
     908  ∃m'.update tag A m i v = OK ? m'.
     909#tag #A #m #i #v #H % [2: >update_def lapply(in_map_domain … m i) >H * #v #EQ >EQ
     910normalize %|]
     911qed.
     912
     913lemma lookup_miss_update : ∀tag,A,m,i,v.lookup tag A m i = None ? → 
     914  update … m i v = Error … [MSG MissingId; CTX … i].
     915#tag #A #m #i #v #EQ >update_def >EQ normalize %
     916qed.
     917
     918lemma update_ok_old_lookup : ∀tag,A,m,i,v,m'.update tag A m i v = OK ? m' →
     919  i ∈ m.
     920#tag #A #m #i #v #m' >update_def inversion(lookup tag A m i) [2: #a] #EQ normalize
     921#EQ destruct >EQ normalize @I
     922qed.
     923
     924lemma lookup_update_ok : ∀tag,A,m,i,v,m',i'.update tag A m i v = OK ? m' →
     925  lookup … m' i' = if eq_identifier ? i' i then Some ? v else lookup … m i'.
     926#tag #A #m #i #v #m' #i' >update_def inversion(lookup tag A m i) [2: #a] #EQ
     927normalize nodelta #EQ1 destruct @eq_identifier_elim
     928[ #H normalize nodelta >H @lookup_add_hit
     929| #H normalize nodelta @lookup_add_miss assumption
     930]
     931qed.
     932
     933lemma mem_set_restrict : ∀tag,A,B.∀a : identifier_map tag A.∀b : identifier_map tag B.
     934∀i.i ∈ a ∩ b = (i ∈ a ∧ i ∈ b).
     935#tag #A #B * #a * #b  * #i normalize >lookup_opt_merge [2: %] cases(lookup_opt B i b)
     936[2: #a1] normalize [2: @if_elim #_ %] cases(lookup_opt A i a) [2: #a2] normalize %
     937qed.
     938(*
     939lemma merge_eq : ∀A.∀p : positive_map A.∀choice. merge
     940*)
     941lemma add_restrict : ∀tag,A,B.∀a : identifier_map tag A. ∀b : identifier_map tag B.
     942∀i,v.i∈b → add tag A (a ∩ b) i v = (add tag A a i v) ∩ b.
     943#tag #A #B * #a * #b * #i #v normalize inversion(lookup_opt B i b) normalize [#_ *]
     944#v1 #EQv1 * @eq_f lapply EQv1 lapply v1 lapply a lapply b -a -b -v1 elim i normalize
     945[ * normalize [#b #v #EQ destruct] #opt_a #l #r *
     946  [#v #EQ destruct normalize %] #opt_b #l1 #r1 #v #EQ destruct normalize cases opt_b
     947  normalize [2: #x %] cases(merge A B A ? l1 l) normalize [2: #opt_a2 #l2 #r2 %]
     948  cases(merge A B A ? r1 r) //
     949|*: #x #IH * [2,4: #opt_b #l1 #r1] #p1 normalize [3,4: #i #EQ destruct] cases p1 -p1
     950    [2,4: #opt_a #l2 #r2] normalize #v #H cases opt_b [2,4,6,8: #b] normalize
     951    [1,2,5,6: <IH try assumption [1,2: cases opt_a [2,4: #a] normalize try %]
     952     cases(merge A B A ? l2 l1) normalize // lapply H [1,4: cases r1 |*: cases l1]
     953     normalize [1,3,5,7,9,11: #EQ destruct] #opt_b4 #l4 #r4 cases x normalize
     954     [1,4,7,10,13,16: #EQ destruct normalize // cases(merge A B A ? ? ?) normalize //]
     955     #x #H normalize cases(merge A B A ? ? ?) normalize //
     956    |*: <IH try assumption
     957       [1,3: cases(map_opt ? ? ? l1) normalize // lapply H cases r1 normalize
     958            [1,3: #EQ destruct] #opt_b2 #l2 #r2 cases x [1,4: //] #x normalize //
     959       |*: lapply H cases x normalize [2,3,5,6: #y] cases l1 normalize
     960          [1,3,5,7,9,11: #EQ destruct] #opt_b2 #l2 #r2 #H //
     961       ]
     962   ]
     963]
     964qed.
     965
     966lemma update_restrict : ∀tag,A,B.∀a : identifier_map tag A.∀b : identifier_map tag B.
     967∀i,v.i ∈ b → update ?? (a ∩ b) i v =
     968  ! a' ← update ?? a i v ; return a' ∩ b.
     969#tag #A #B #a #b #id #v #H
     970lapply (in_map_domain … b id) >H * #ignore #EQ_lookup_b
     971(*<clean_update*)
     972inversion (update tag A a id v)
     973[2: #e #EQ cases (update_fail_lookup ?????? EQ) #EQ1 #EQ2 destruct
     974  >lookup_miss_update [%]
     975  >lookup_restrict >H assumption ]
     976#m' #EQ >m_return_bind
     977cases (lookup_hit_update ?? (a∩b) id v ?)
     978[2: >mem_set_restrict >H >(update_ok_old_lookup ?????? EQ) % ]
     979#m'' >update_def >update_def in EQ; >lookup_restrict >H normalize nodelta
     980cases(lookup tag A a id) normalize nodelta [#ABS destruct] #v1 #EQ #EQ'' destruct
     981whd in ⊢ (??%%); @eq_f @add_restrict assumption
     982qed.
     983
     984definition sigma_frames : ∀prog : ertlptr_program.sigma_map prog →
     985list (register_env beval × ident) → list (register_env beval × ident) ≝
     986λprog,sigma,frms.map ??
     987(λx.〈sigma_register_env prog sigma (\fst x) (getLocalsFromId (\snd x)),\snd x〉) frms.
     988
     989(*
    665990lemma sigma_empty_frames_commute :
    666991∀prog : ertl_program. ∀ sigma : (sigma_map prog).
    … …  
    6881013hw_register_env → Prop ≝
    6891014λprog,sigma,regs.sigma_bit_vector_trie_opt prog sigma 6 (reg_env … regs) ≠ None ?.
     1015*)
     1016
     1017
     1018include "common/BitVectorTrieMap.ma".
    6901019
    6911020definition sigma_hw_register_env :
    692 ∀prog: ertl_program. ∀sigma : (sigma_map prog).
    693 ∀h_reg : hw_register_env. well_formed_hw_register_env prog sigma h_reg →
    694 hw_register_env ≝
    695 λprog,sigma,h_reg,prf.mk_hw_register_env
    696 (opt_safe … prf) (other_bit … h_reg).
    697 
    698 definition well_formed_regs :
    699 ∀prog : ertl_program. ∀ sigma : (sigma_map prog).
    700 ertl_psd_env×hw_register_env → Prop ≝
    701 λprog,sigma,regs. let 〈x,y〉 ≝ regs in
    702 well_formed_ertl_psd_env prog sigma x ∧ well_formed_hw_register_env prog sigma y.
     1021∀prog: ertlptr_program. ∀sigma : (sigma_map prog).
     1022hw_register_env → hw_register_env ≝
     1023λprog,sigma,h_reg.mk_hw_register_env
     1024(map ? ? (sigma_beval prog sigma) 6 (reg_env … h_reg)) (other_bit … h_reg).
     1025
    7031026
    7041027definition sigma_regs :
    705 ∀prog : ertl_program. ∀sigma : (sigma_map prog).
    706 ∀regs: ertl_psd_env×hw_register_env.well_formed_regs prog sigma regs →
    707 ertl_psd_env×hw_register_env ≝
    708 λprog,sigma,regs.let 〈x,y〉≝ regs in
    709 λprf : well_formed_regs prog sigma 〈x,y〉.
    710       〈sigma_ertl_psd_env prog sigma x (proj1 … prf),
    711        sigma_hw_register_env prog sigma y (proj2 … prf)〉.
    712 
     1028∀prog : ertlptr_program. ∀sigma : (sigma_map prog).
     1029(register_env beval)×hw_register_env→ list register →
     1030(register_env beval)×hw_register_env ≝
     1031λprog,sigma,regs,ids.let 〈x,y〉≝ regs in
     1032      〈sigma_register_env prog sigma x ids,
     1033       sigma_hw_register_env prog sigma y〉.
     1034(*
    7131035lemma sigma_empty_regsT_commute :
    7141036∀prog : ertl_program. ∀sigma : (sigma_map prog).
    … …  
    7461068well_formed_regs prog sigma (regs … st) ∧
    7471069well_formed_mem prog sigma (m … st).
     1070*)
    7481071
    7491072definition sigma_state :
    750  ∀prog : ertl_program.
     1073 ∀prog : ertlptr_program.
    7511074 ∀sigma : sigma_map prog.
    752  ∀st : state ERTL_semantics.
    753  well_formed_state prog sigma st →
    754  state ERTLptr_semantics ≝
    755 λprog,sigma,st,prf.
    756 mk_state …
    757   (sigma_frames prog sigma (st_frms … st) ?)
    758   (sigma_is prog sigma (istack … st) ?)
     1075 state ERTLptr_semantics → list register →
     1076 state ERTL_semantics ≝
     1077λprog,sigma,st,ids.
     1078mk_state ?
     1079  (sigma_frames prog sigma (st_frms … st))
     1080  (sigma_is prog sigma (istack … st))
    7591081  (carry … st)
    760   (sigma_regs prog sigma (regs … st) ?)
    761   (sigma_mem prog sigma (m … st) ?).
    762 @hide_prf cases prf ** //
    763 qed.
    764 
    765 definition well_formed_state_pc :
    766 ∀prog : ertl_program .∀ sigma : sigma_map prog.
    767   state_pc ERTL_semantics → Prop ≝
    768  λprog,sigma,st.
    769  well_formed_pc prog sigma (last_pop … st) ∧
    770  well_formed_state prog sigma st.
     1082  (sigma_regs prog sigma (regs … st) ids)
     1083  (sigma_mem prog sigma (m … st)).
     1084
     1085definition dummy_state : state ERTL_semantics ≝
     1086mk_state ERTL_semantics
     1087   [ ] empty_is BBundef 〈empty_map ? ?,mk_hw_register_env … (Stub …) BBundef〉 empty.
     1088 
     1089definition dummy_state_pc : state_pc ERTL_semantics ≝
     1090mk_state_pc ? dummy_state null_pc null_pc.
     1091
     1092check fetch_internal_function
    7711093
    7721094definition sigma_state_pc :
    773 ∀prog : ertl_program. ∀sigma : sigma_map prog.
    774 ∀ st : state_pc ERTL_semantics. well_formed_state_pc prog sigma st →
    775 state_pc ERTLptr_semantics ≝
    776 λprog,sigma,st,prf.
    777 mk_state_pc ? (sigma_state … (proj2 … prf)) (pc … st)
    778               (sigma_pc … (proj1 … prf)).
    779 
     1095∀prog : ertl_program.
     1096let trans_prog ≝ ertl_to_ertlptr prog in
     1097∀sigma : sigma_map trans_prog.
     1098state_pc ERTLptr_semantics →
     1099 state_pc ERTL_semantics ≝
     1100λprog,sigma,st.
     1101  let trans_prog ≝ ertl_to_ertlptr prog in
     1102  let ge ≝ globalenv_noinit … prog in
     1103  if eqZb       (block_id (pc_block (pc … st))) (-1) then (* check for dummy pc *)
     1104    dummy_state_pc
     1105  else
     1106  match    (fetch_internal_function (joint_closed_internal_function ERTL
     1107                (prog_var_names (joint_function ERTL) ℕ prog)) ge (pc_block (pc … st))) with
     1108   [OK x ⇒ let 〈i,fd〉 ≝ x in
     1109      mk_state_pc ? (sigma_state trans_prog sigma st (joint_if_locals … fd))
     1110       (pc … st) (sigma_stored_pc trans_prog sigma (last_pop … st))
     1111   |Error msg ⇒ dummy_state_pc].
     1112
     1113(*
    7801114lemma reg_store_sigma_commute :
    7811115∀ prog : ertl_program. ∀sigma : (sigma_map prog).
    … …  
    8921226qed.
    8931227
    894 
    895 
    896 
    897        
     1228lemma ertl_allocate_local_commute : ∀prog : ertl_program.
     1229∀sigma : sigma_map prog.∀reg,regs,prf1. ∃ prf2.
     1230ertl_allocate_local reg (sigma_regs prog sigma regs prf1) =
     1231sigma_regs prog sigma (ertl_allocate_local reg regs) prf2.
     1232#prog #sigma * #r ** #psd_r #sp #hw_regs #prf1 %
     1233whd in match ertl_allocate_local; normalize nodelta
     1234[ @hide_prf % [2: cases prf1 #_ #x assumption] ]
     1235whd in match set_psd_regs; normalize nodelta
     1236[ whd in match well_formed_ertl_psd_env; whd in match well_formed_register_env;
     1237  normalize nodelta * #id #bv cases(decidable_eq_pos id r)
     1238  [ #EQ >EQ >lookup_add_hit #EQ1 destruct(EQ1) normalize % #EQ2 destruct
     1239  | * #EQ
     1240  >(lookup_add_miss ?? (psd_r) (an_identifier ? id) (an_identifier RegisterTag r) BVundef ?)
     1241   [2: % #EQ1 @EQ destruct %] cases prf1 whd in match well_formed_ertl_psd_env;
     1242   whd in match well_formed_register_env; normalize nodelta #H1 #_ #H @H1
     1243   [% @id|assumption]
     1244  ]
     1245| whd in match sigma_regs; whd in match sigma_ertl_psd_env; normalize nodelta
     1246 @eq_f2 [2: %] @eq_f2 [2: %] whd in match sigma_register_env; normalize nodelta
     1247 cases(map_inf_add beval beval RegisterTag psd_r ? BVundef (an_identifier ? r) ? ?)
     1248 [ #prf2 #EQ >EQ @eq_f % ||
     1249 | #bv #id' #id'' #prf #prf' %
     1250 ]
     1251]
     1252qed.
     1253
     1254lemma is_push_sigma_commute :
     1255∀ prog : ertl_program. ∀ sigma : sigma_map prog.
     1256preserving2 … res_preserve …
     1257  (sigma_is prog sigma)
     1258  (sigma_beval prog sigma) 
     1259  (sigma_is prog sigma)
     1260  is_push
     1261  is_push.
     1262#prog #sigma *
     1263[ | #bv1 | #bv1 #bv2 ] #val #prf1 #prf2 #is'
     1264whd in ⊢ (??%%→?); #EQ destruct(EQ)
     1265whd in match sigma_beval; normalize nodelta
     1266@opt_safe_elim #val' #EQsigma_val
     1267%
     1268[1,3: @hide_prf %
     1269|*: whd in match sigma_is in ⊢ (???%); normalize nodelta
     1270  @opt_safe_elim #is''
     1271] whd in match sigma_is_opt; normalize nodelta
     1272[2,4:
     1273  inversion (sigma_beval_opt ???)
     1274  [1,3: #EQ whd in prf1 : (?(??%?)); @⊥ >EQ in prf1;
     1275    normalize nodelta * #H @H % ]
     1276  #bv1' #EQ_bv1' >m_return_bind ]
     1277>EQsigma_val
     1278whd in ⊢ (??%%→?); #EQ destruct(EQ)
     1279whd in match sigma_is; normalize nodelta
     1280@opt_safe_elim #is1
     1281whd in match sigma_is_opt; normalize nodelta
     1282[ #H @('bind_inversion H) #bv1''
     1283  >EQ_bv1' #EQ destruct(EQ) ]
     1284whd in ⊢ (??%%→?); #EQ destruct(EQ) %
     1285qed.
     1286
     1287check internal_stack
     1288check BVpc
     1289
     1290definition sigma_is_not_head_opt : ∀ prog : ertl_program.
     1291sigma_map prog → internal_stack → option internal_stack ≝
     1292λprog,sigma,is.
     1293     match is with
     1294[ empty_is ⇒ return empty_is
     1295| one_is bv ⇒ return one_is bv
     1296| both_is bv1 bv2 ⇒
     1297  ! bv2' ← sigma_beval_opt … sigma bv2 ;
     1298  return both_is bv1 bv2'
     1299].
     1300
     1301
     1302lemma ertlptr_save_frame_commute : ∀prog: ertl_program.
     1303∀sigma : sigma_map prog. ∀kind.
     1304    preserving … res_preserve …
     1305         (sigma_state_pc prog sigma)
     1306         (sigma_state prog sigma)
     1307         (ertl_save_frame kind it)
     1308         (ertlptr_save_frame kind it).
     1309#prog #sigma * whd in match ertl_save_frame; whd in match ertlptr_save_frame;
     1310normalize nodelta * #st #pc #lp * #wf_lp #wf_st
     1311  [2: @mfr_bind
     1312    [3: whd in match push_ra; normalize nodelta @mfr_bind
     1313      [3: whd in match sigma_state_pc; whd in match push; whd in match sigma_state;
     1314          normalize nodelta @mfr_bind
     1315        [#is @(sigma_is_not_head_opt prog sigma is ≠ None ?)
     1316        |#is #prf @(opt_safe … prf)
     1317        |
     1318 
     1319 
     1320  #x #x_spec @mfr_bind
     1321[ @(λ_.True) | #st * @(sigma_state prog sigma st) |
     1322  [3: cases kind normalize nodelta whd in match push_ra; normalize nodelta
     1323    [ whd in match sigma_state_pc; normalize nodelta #st #st_spec
     1324*)
     1325
    8981326definition ERTLptrStatusSimulation :
    8991327∀ prog : ertl_program.
    9001328let trans_prog ≝ ertl_to_ertlptr prog in
    9011329∀stack_sizes.
    902 sigma_map prog →
     1330sigma_map trans_prog →
    9031331status_rel (ERTL_status prog stack_sizes) (ERTLptr_status trans_prog stack_sizes) ≝
    904 λprog,stack_sizes,sigma.mk_status_rel …
    905     (* sem_rel ≝ *) (λ
     1332λprog,stack_sizes,sigma.let trans_prog ≝ ertl_to_ertlptr prog in mk_status_rel ??
     1333    (* sem_rel ≝ *) (λs1:ERTL_status prog stack_sizes
     1334       .λs2:ERTLptr_status trans_prog stack_sizes
     1335        .s1=sigma_state_pc prog sigma s2)
     1336    (* call_rel ≝ *)  (λs1:Σs:ERTL_status prog stack_sizes
     1337               .as_classifier (ERTL_status prog stack_sizes) s cl_call
     1338       .λs2:Σs:ERTLptr_status trans_prog stack_sizes
     1339                .as_classifier (ERTLptr_status trans_prog stack_sizes) s cl_call
     1340        .pc (mk_prog_params ERTL_semantics prog stack_sizes) s1
     1341         =sigma_stored_pc trans_prog sigma
     1342          (pc
     1343           (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_sizes)
     1344           s2))
     1345    (* sim_final ≝ *) ?.
     1346cases daemon
     1347qed.
     1348
     1349lemma fetch_function_no_minus_one :
     1350  ∀F,V,i,p,bl.
     1351  block_id (pi1 … bl) = -1 →
     1352  fetch_function … (globalenv (λvars.fundef (F vars)) V i p)
     1353    bl = Error … [MSG BadFunction].
     1354 #F#V#i#p ** #r #id #EQ1 #EQ2 destruct
     1355  whd in match fetch_function; normalize nodelta
     1356  >globalenv_no_minus_one
     1357  cases (symbol_for_block ???) normalize //
     1358qed.
     1359 
     1360lemma fetch_function_no_zero :
     1361 ∀F,V,i,p,bl.
     1362  block_id (pi1 … bl) = 0 →
     1363  fetch_function … (globalenv (λvars.fundef (F vars)) V i p)
     1364    bl = Error … [MSG BadFunction].
     1365 #F#V#i#p ** #r #id #EQ1 #EQ2 destruct
     1366  whd in match fetch_function; normalize nodelta
     1367  >globalenv_no_zero
     1368  cases (symbol_for_block ???) normalize //
     1369qed.
     1370
     1371(*DOPPIONI dei LEMMI in LINEARISE_PROOF*)
     1372lemma symbol_for_block_match:
     1373    ∀M:matching.∀initV,initW.
     1374     (∀v,w. match_var_entry M v w →
     1375      size_init_data_list (initV (\snd v)) = size_init_data_list (initW (\snd w))) →
     1376    ∀p: program (m_A M) (m_V M). ∀p': program (m_B M) (m_W M).
     1377    ∀MATCH:match_program … M p p'.
     1378    ∀b: block.
     1379    symbol_for_block … (globalenv … initW p') b =
     1380    symbol_for_block … (globalenv … initV p) b.
     1381* #A #B #V #W #match_fn #match_var #initV #initW #H
     1382#p #p' * #Mvars #Mfn #Mmain
     1383#b
     1384whd in match symbol_for_block; normalize nodelta
     1385whd in match globalenv in ⊢ (???%); normalize nodelta
     1386whd in match (globalenv_allocmem ????);
     1387change with (add_globals ?????) in match (foldl ?????);
     1388>(proj1 … (add_globals_match … initW … Mvars))
     1389[ % |*:]
     1390[ * #idr #v * #idr' #w #MVE %
     1391  [ inversion MVE
     1392    #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 destruct %
     1393  | @(H … MVE)
     1394  ]
     1395| @(matching_fns_get_same_blocks … Mfn)
     1396  #f #g @match_funct_entry_id
     1397]
     1398qed.
     1399
     1400lemma symbol_for_block_transf :
     1401 ∀A,B,V,init.∀prog_in : program A V.
     1402 ∀trans : ∀vars.A vars → B vars.
     1403 let prog_out ≝ transform_program … prog_in trans in
     1404 ∀bl.
     1405 symbol_for_block … (globalenv … init prog_out) bl =
     1406 symbol_for_block … (globalenv … init prog_in) bl.
     1407#A #B #V #iV #p #tf @(symbol_for_block_match … (transform_program_match … tf ?))
     1408#v0 #w0 * //
     1409qed.
     1410
     1411lemma fetch_function_transf :
     1412 ∀A,B,V,init.∀prog_in : program A V.
     1413 ∀trans : ∀vars.A vars → B vars.
     1414 let prog_out ≝ transform_program … prog_in trans in
     1415 ∀bl,i,f.
     1416 fetch_function … (globalenv … init prog_in) bl =
     1417  return 〈i, f〉
     1418→ fetch_function … (globalenv … init prog_out) bl =
     1419  return 〈i, trans … f〉.
     1420#A #B #V #init #prog_in #trans #bl #i #f
     1421 whd in match fetch_function; normalize nodelta
     1422 #H lapply (opt_eq_from_res ???? H) -H
     1423 #H @('bind_inversion H) -H #id #eq_symbol_for_block
     1424 #H @('bind_inversion H) -H #fd #eq_find_funct
     1425 whd in ⊢ (??%?→?); #EQ destruct(EQ)
     1426 >(symbol_for_block_transf … trans) >eq_symbol_for_block >m_return_bind
     1427 >(find_funct_ptr_transf A B …  eq_find_funct) %
     1428qed.
     1429
     1430
     1431lemma fetch_internal_function_transf :
     1432 ∀A,B.∀prog_in : program (λvars.fundef (A vars)) ℕ.
     1433 ∀trans : ∀vars.A vars → B vars.
     1434 let prog_out ≝ transform_program … prog_in (λvars.transf_fundef … (trans vars)) in
     1435 ∀bl,i,f.
     1436 fetch_internal_function … (globalenv_noinit … prog_in) bl =
     1437  return 〈i, f〉
     1438→ fetch_internal_function … (globalenv_noinit … prog_out) bl =
     1439  return 〈i, trans … f〉.
     1440#A #B #prog #trans #bl #i #f
     1441 whd in match fetch_internal_function; normalize nodelta
     1442 #H @('bind_inversion H) * #id * #fd normalize nodelta #EQfetch
     1443 whd in ⊢ (??%%→?); #EQ destruct(EQ)
     1444 >(fetch_function_transf … EQfetch) %
     1445qed.
     1446
     1447(*
     1448definition good_local_sigma :
     1449  ∀globals.
     1450  ∀g:codeT ERTLptr globals.
     1451  (Σl.bool_to_Prop (code_has_label … g l)) →
     1452  codeT ERTL globals →
     1453  (label → option label) → Prop ≝
     1454  λglobals,g,c,sigma.
     1455    ∀l,l'.sigma l = Some ? l' →
     1456      ∃s. stmt_at … g l = Some ? s ∧
     1457          All ? (λl.sigma l ≠ None ?) (stmt_labels … s) ∧
     1458          (match s with
     1459           [ sequential s' nxt ⇒
     1460             match s' with
     1461             [ step_seq _ ⇒
     1462               (stmt_at … c n = Some ? (sequential … s' it)) ∧
     1463                  ((sigma nxt = Some ? (S n)) ∨
     1464                   (stmt_at … c (S n) = Some ? (GOTO … nxt)))
     1465             | COND a ltrue ⇒
     1466               (stmt_at … c n = Some ? (sequential … s' it) ∧ sigma nxt = Some ? (S n)) ∨
     1467               (stmt_at … c n = Some ? (FCOND … I a ltrue nxt))
     1468             ]
     1469           | final s' ⇒
     1470             stmt_at … c n = Some ? (final … s')
     1471           | FCOND abs _ _ _ ⇒ Ⓧabs
     1472           ]).
     1473 
     1474*)
     1475
     1476lemma ps_reg_retrieve_ok :  ∀prog : ertlptr_program.
     1477∀sigma : sigma_map prog. ∀r,restr.
     1478preserving1 ?? res_preserve1 …
     1479     (λregs.sigma_regs prog sigma regs restr)
     1480     (sigma_beval prog sigma)
     1481     (λregs.ps_reg_retrieve regs r)
     1482     (λregs.ps_reg_retrieve regs r).
     1483#prog #sigma #r #restr * #psd_r #hw_r whd in match ps_reg_retrieve;
     1484whd in match reg_retrieve; normalize nodelta @opt_to_res_preserve1
     1485whd in match sigma_regs; whd in match sigma_register_env; normalize nodelta
     1486>lookup_restrict @if_elim [2: #_ @opt_preserve_none1] #id_r_in
     1487>(lookup_map ?? RegisterTag ???) #bv #H @('bind_inversion H) -H #bv1
     1488#bv1_spec whd in ⊢ (??%? → ?); #EQ destruct %{bv1} % // >bv1_spec %
     1489qed.
     1490
     1491lemma hw_reg_retrieve_ok : ∀prog : ertlptr_program.
     1492∀sigma : sigma_map prog. ∀r,restr.
     1493preserving1 ?? res_preserve1 …
     1494    (λregs.sigma_regs prog sigma regs restr)
     1495    (sigma_beval prog sigma)
     1496    (λregs.hw_reg_retrieve regs r)
     1497    (λregs.hw_reg_retrieve regs r).
     1498#prog #sigma #r #restr * #psd_r * #hw_r #b whd in match hw_reg_retrieve;
     1499whd in match hwreg_retrieve; normalize nodelta whd in match sigma_regs;
     1500whd in match sigma_hw_register_env; normalize nodelta
     1501change with (sigma_beval prog sigma BVundef) in ⊢ (???????(??(?????%))?);
     1502#bv >lookup_map whd in ⊢ (???% → ?); #EQ destruct
     1503%{(lookup beval 6 (bitvector_of_register r) hw_r BVundef)}
     1504% //
     1505qed.
     1506
     1507
     1508lemma ps_reg_store_ok : ∀prog : ertlptr_program.
     1509∀sigma : sigma_map prog. ∀r,restr.
     1510preserving21 ?? res_preserve1 …
     1511   (sigma_beval prog sigma)
     1512   (λregs.sigma_regs prog sigma regs restr)
     1513   (λregs.sigma_regs prog sigma regs restr)
     1514   (ps_reg_store r)
     1515   (ps_reg_store r).
     1516#prog #sigma #r #restr whd in match ps_reg_store; normalize nodelta
     1517#bv * #psd_r #hw_r @mfr_bind1
     1518[ @(λr.sigma_register_env prog sigma r restr)
     1519| whd in match reg_store; whd in match sigma_regs; normalize nodelta
     1520  #x #x_spec lapply(update_ok_to_lookup ?????? x_spec) * * #_ #EQpsd #_
     1521  lapply x_spec -x_spec lapply EQpsd -EQpsd whd in match sigma_register_env;
     1522  normalize nodelta >lookup_restrict @if_elim [2: #_ * #H @⊥ @H %]
     1523  #id_in #_ >update_restrict [2: assumption] #H @('bind_inversion H) -H
     1524  #x0 >map_update_commute #H @('bind_inversion H) -H #x1 #x1_spec
     1525  whd in ⊢ (??%% → ??%% → ?); #EQ1 #EQ2 destruct %{x1} % //
     1526| #x * #psd_r' #hw_r' whd in match sigma_regs; normalize nodelta
     1527  whd in ⊢ (???% → ?); #EQ destruct %{〈x,hw_r〉} % //
     1528]
     1529qed.
     1530
     1531
     1532lemma hw_reg_store_ok : ∀prog : ertlptr_program.
     1533∀sigma : sigma_map prog. ∀r,restr.
     1534preserving21 ?? res_preserve1 …
     1535   (sigma_beval prog sigma)
     1536   (λregs.sigma_regs prog sigma regs restr)
     1537   (λregs.sigma_regs prog sigma regs restr)
     1538   (hw_reg_store r)
     1539   (hw_reg_store r).
     1540#prog #sigma #r #restr whd in match hw_reg_store; normalize nodelta
     1541#bv * #psd_r * #hw_r #b whd in match hwreg_store; whd in match sigma_regs; normalize nodelta
     1542whd in match sigma_hw_register_env; normalize nodelta <insert_map * #psd_r'
     1543* #hw_r' #b' whd in ⊢ (???% → ?); #EQ destruct % [2: % [%] % |]
     1544qed.
     1545
     1546
     1547lemma ertl_eval_move_ok : ∀prog : ertlptr_program.
     1548∀sigma : sigma_map prog. ∀ restr,pm.
     1549preserving1 ?? res_preserve1 …
     1550     (λregs.sigma_regs prog sigma regs restr)
     1551     (λregs.sigma_regs prog sigma regs restr)
     1552     (λregs.ertl_eval_move regs pm)
     1553     (λregs.ertl_eval_move regs pm).
     1554#prog #sigma #restr * #mv_dst #arg_dst #pm whd in match ertl_eval_move;
     1555normalize nodelta @mfr_bind1 [@(sigma_beval prog sigma)
     1556| cases arg_dst normalize nodelta
     1557  [2: #b change with (return sigma_beval prog sigma (BVByte b)) in ⊢ (???????%?);
     1558      @mfr_return1]
     1559  * #r normalize nodelta [@ps_reg_retrieve_ok| @hw_reg_retrieve_ok]
     1560| #bv cases mv_dst #r normalize nodelta [@ps_reg_store_ok | @hw_reg_store_ok]
     1561]
     1562qed.
     1563
     1564lemma ps_arg_retrieve_ok : ∀prog : ertlptr_program.
     1565∀sigma : sigma_map prog. ∀a,restr.
     1566preserving1 ?? res_preserve1 …
     1567    (λregs.sigma_regs prog sigma regs restr)
     1568    (sigma_beval prog sigma)
     1569    (λregs.ps_arg_retrieve regs a)
     1570    (λregs.ps_arg_retrieve regs a).
     1571#prog #sigma #a #restr whd in match ps_arg_retrieve; normalize nodelta cases a -a
     1572normalize nodelta [#r | #b ] #regs
     1573[ @ps_reg_retrieve_ok
     1574| change with (return sigma_beval prog sigma (BVByte b)) in ⊢ (???????%?);
     1575  @mfr_return1
     1576]
     1577qed.
     1578
     1579lemma pop_ok :
     1580∀prog : ertl_program.
     1581  let trans_prog ≝ ertl_to_ertlptr prog in
     1582∀sigma : sigma_map trans_prog.
     1583∀stack_size.
     1584∀fn : (joint_closed_internal_function ERTL (globals (mk_prog_params ERTL_semantics prog stack_size))).
     1585preserving1 ?? res_preserve1 ????
     1586   (λst.sigma_state trans_prog sigma st (joint_if_locals ERTL ? fn))
     1587   (λx.let 〈bv,st〉 ≝ x in
     1588      〈sigma_beval trans_prog sigma bv,
     1589       sigma_state trans_prog sigma st (joint_if_locals ERTL ? fn) 〉)
     1590   (pop ERTL_semantics)
     1591   (pop ERTLptr_semantics).
     1592#prog #sigma #stack_size #fn whd in match pop; normalize nodelta #st @mfr_bind1
     1593[@(λx.let 〈bv,is〉 ≝ x in
     1594     〈sigma_beval (ertl_to_ertlptr prog) sigma bv,
     1595      sigma_is (ertl_to_ertlptr prog) sigma is 〉)
     1596| whd in match is_pop; normalize nodelta whd in match sigma_state; normalize nodelta
     1597  cases(istack ? st) normalize nodelta
     1598  [@res_preserve_error1
     1599  |2,3: #bv1 [2: #bv2] * #bv3 #is1 whd in ⊢ (??%% → ?); #EQ destruct
     1600        % [2,4: % [1,3: %|*: %] |*:]
     1601  ]
     1602| * #bv #is * #bv1 #st whd in ⊢ (??%% → ?); #EQ destruct % [2: % [%] %|]
     1603]
     1604qed.
     1605
     1606lemma push_ok :
     1607∀prog : ertl_program.
     1608  let trans_prog ≝ ertl_to_ertlptr prog in
     1609∀sigma : sigma_map trans_prog.
     1610∀stack_size.
     1611∀fn : (joint_closed_internal_function ERTL (globals (mk_prog_params ERTL_semantics prog stack_size))).
     1612preserving21 ?? res_preserve1 …
     1613     (λst.sigma_state trans_prog sigma st (joint_if_locals ERTL ? fn))
     1614     (sigma_beval trans_prog sigma)
     1615     (λst.sigma_state trans_prog sigma st (joint_if_locals ERTL ? fn))
     1616     (push ERTL_semantics)
     1617     (push ERTLptr_semantics).
     1618cases daemon
     1619qed.
     1620
     1621lemma be_opaccs_ok :
     1622∀prog : ertlptr_program. ∀sigma : sigma_map prog.
     1623∀ op.
     1624preserving21 ?? res_preserve1 ??????
     1625    (sigma_beval prog sigma)
     1626    (sigma_beval prog sigma)
     1627    (λx.let 〈bv1,bv2〉 ≝ x in
     1628           〈sigma_beval prog sigma bv1,
     1629            sigma_beval prog sigma bv2〉)
     1630    (be_opaccs op)
     1631    (be_opaccs op).
     1632cases daemon
     1633qed.
     1634
     1635lemma be_op1_ok : ∀prog : ertlptr_program. ∀sigma : sigma_map prog.
     1636∀ op.
     1637preserving1 ?? res_preserve1 …
     1638     (sigma_beval prog sigma)
     1639     (sigma_beval prog sigma)
     1640     (be_op1 op)
     1641     (be_op1 op).
     1642cases daemon
     1643qed.
     1644
     1645lemma be_op2_ok : ∀prog : ertlptr_program. ∀sigma : sigma_map prog.
     1646∀ b,op.
     1647preserving21 ?? res_preserve1 …
     1648     (sigma_beval prog sigma)
     1649     (sigma_beval prog sigma)
     1650     (λx.let 〈bv,b〉≝ x in 〈sigma_beval prog sigma bv,b〉)
     1651     (be_op2 b op)
     1652     (be_op2 b op).
     1653cases daemon
     1654qed.
     1655
     1656lemma pointer_of_address_ok : ∀prog : ertlptr_program. ∀sigma : sigma_map prog.
     1657preserving1 … res_preserve1 …
     1658     (λx.let 〈bv1,bv2〉 ≝ x in〈sigma_beval prog sigma bv1,
     1659           sigma_beval prog sigma bv2〉)
     1660     (λx.x)
     1661     pointer_of_address pointer_of_address.
     1662cases daemon
     1663qed.
     1664
     1665lemma beloadv_ok : ∀prog : ertlptr_program. ∀sigma : sigma_map prog.
     1666∀ptr.
     1667preserving1 … opt_preserve1 …
     1668     (sigma_mem prog sigma)
     1669     (sigma_beval prog sigma)
     1670     (λm.beloadv m ptr)
     1671     (λm.beloadv m ptr).
     1672cases daemon
     1673qed.
     1674
     1675lemma bestorev_ok : ∀prog : ertlptr_program.∀sigma : sigma_map prog.
     1676∀ptr.
     1677preserving21 … opt_preserve1 …
     1678    (sigma_mem prog sigma)
     1679    (sigma_beval prog sigma)
     1680    (sigma_mem prog sigma)
     1681    (λm.bestorev m ptr)
     1682    (λm.bestorev m ptr).
     1683cases daemon
     1684qed.
     1685
     1686lemma eval_seq_no_pc_no_call_ok :
     1687∀prog : ertl_program.
     1688  let trans_prog ≝ ertl_to_ertlptr prog in
     1689∀stack_size.∀sigma : sigma_map trans_prog.
     1690∀id. ∀fn : (joint_closed_internal_function ??) .∀seq.
     1691   preserving1 ?? res_preserve1 ????
     1692      (λst.sigma_state trans_prog sigma st (joint_if_locals ERTL ? fn))
     1693      (λst.sigma_state trans_prog sigma st (joint_if_locals ERTL ? fn))
     1694      (eval_seq_no_pc (mk_prog_params ERTL_semantics prog stack_size)
     1695             (globals (mk_prog_params ERTL_semantics prog stack_size))
     1696             (ev_genv (mk_prog_params ERTL_semantics prog stack_size)) id fn seq)
     1697      (eval_seq_no_pc (mk_prog_params ERTLptr_semantics trans_prog stack_size)
     1698  (globals (mk_prog_params ERTLptr_semantics trans_prog stack_size))
     1699  (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_size)) id (translate_internal … fn) (translate_step_seq … seq)).
     1700#prog #stack_size #sigma #f #fn *
     1701whd in match eval_seq_no_pc; normalize nodelta
     1702[ #c #st @mfr_return1
     1703| #c #st @mfr_return1
     1704| #pm #st whd in match pair_reg_move; normalize nodelta
     1705  @mfr_bind1
     1706  [ @(λregs.sigma_regs (ertl_to_ertlptr prog) sigma regs (joint_if_locals ERTL ? fn))
     1707  | change with (ertl_eval_move ??) in ⊢ (???????%%); @ertl_eval_move_ok
     1708  | #regs #st whd in ⊢ (??%% → ?); #EQ destruct % [2: % [%] % |]
     1709  ]
     1710| #r #st @mfr_bind1
     1711  [@(λx.let 〈bv,st〉 ≝ x in
     1712      〈sigma_beval (ertl_to_ertlptr prog) sigma bv,
     1713       sigma_state (ertl_to_ertlptr prog) sigma st (joint_if_locals ERTL ? fn) 〉)
     1714  | @pop_ok
     1715  | * #bv #st whd in match acca_store; normalize nodelta @mfr_bind1
     1716    [@(λregs.sigma_regs (ertl_to_ertlptr prog) sigma regs (joint_if_locals ERTL ? fn))
     1717    | @ps_reg_store_ok
     1718    | #regs #x whd in ⊢ (??%% → ?); #EQ destruct % [2: % [%] % |]
     1719    ]
     1720  ]
     1721| #r #st @mfr_bind1
     1722  [@(λbv.sigma_beval (ertl_to_ertlptr prog) sigma bv)
     1723  | whd in match acca_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok
     1724  | #bv @push_ok
     1725  ]
     1726| #i
     1727  change with (member ? ? ? (((prog_var_names (joint_function ERTL)) ℕ prog)) → ?)
     1728  #i_spec
     1729  change with ((dpl_reg ERTL) → ?)
     1730  #dpl
     1731  change with ((dph_reg ERTL) → ?)
     1732  #dph #st @mfr_bind1
     1733  [@(λst.sigma_state (ertl_to_ertlptr prog) sigma st (joint_if_locals ERTL ? fn))
     1734  | whd in match dpl_store; normalize nodelta @mfr_bind1
     1735    [ @(λregs.sigma_regs (ertl_to_ertlptr prog) sigma regs (joint_if_locals ERTL ? fn))
     1736    | @opt_safe_elim #bl #EQbl
     1737      @opt_safe_elim #bl'
     1738       >(find_symbol_transf …
     1739          (λvars.transf_fundef … (λfn.(translate_internal … fn))) prog i) in ⊢ (%→?);
     1740       >EQbl #EQ destruct whd in match sigma_state; normalize nodelta       
     1741       change with (sigma_beval (ertl_to_ertlptr prog) sigma (BVptr …))
     1742                                               in ⊢ (???????(?????%?)?);
     1743       @ps_reg_store_ok
     1744    | #regs #st1 whd in match set_regs; whd in match sigma_state; normalize nodelta;
     1745      whd in ⊢(??%% → ?); #EQ destruct % [2: % [%] %|]
     1746    ]
     1747  | #st1 @opt_safe_elim #bl #EQbl @opt_safe_elim #bl'   
     1748    >(find_symbol_transf …
     1749          (λvars.transf_fundef … (λfn.(translate_internal … fn))) prog i) in ⊢ (%→?);
     1750    >EQbl #EQ destruct whd in match dph_store; normalize nodelta @mfr_bind1
     1751    [ @(λregs.sigma_regs (ertl_to_ertlptr prog) sigma regs (joint_if_locals ERTL ? fn))
     1752    | whd in match sigma_state; normalize nodelta       
     1753      change with (sigma_beval (ertl_to_ertlptr prog) sigma (BVptr …))
     1754                                               in ⊢ (???????(?????%?)?);
     1755      @ps_reg_store_ok
     1756    | #regs #st1 whd in match set_regs; whd in match sigma_state; normalize nodelta;
     1757      whd in ⊢(??%% → ?); #EQ destruct % [2: % [%] %|]
     1758    ]
     1759  ]
     1760| #op #a #b #arg1 #arg2 #st @mfr_bind1
     1761  [@(sigma_beval (ertl_to_ertlptr prog) sigma)
     1762  | whd in match acca_arg_retrieve; whd in match sigma_state; normalize nodelta
     1763    @ps_arg_retrieve_ok
     1764  | #bv1 @mfr_bind1
     1765   [ @(sigma_beval (ertl_to_ertlptr prog) sigma)
     1766   | whd in match accb_arg_retrieve; whd in match sigma_state; normalize nodelta
     1767     @ps_arg_retrieve_ok
     1768   | #bv2 @mfr_bind1
     1769     [@(λx.let 〈bv1,bv2〉 ≝ x in
     1770           〈sigma_beval (ertl_to_ertlptr prog) sigma bv1,
     1771            sigma_beval (ertl_to_ertlptr prog) sigma bv2〉)
     1772     | @be_opaccs_ok
     1773     | * #bv3 #bv4 normalize nodelta @mfr_bind1
     1774       [ @(λst.sigma_state (ertl_to_ertlptr prog) sigma st (joint_if_locals ERTL ? fn))
     1775       | whd in match acca_store; normalize nodelta @mfr_bind1
     1776         [  @(λregs.sigma_regs (ertl_to_ertlptr prog) sigma regs (joint_if_locals ERTL ? fn))
     1777         | @ps_reg_store_ok
     1778         | #regs #st1 whd in match set_regs; whd in match sigma_state; normalize nodelta;
     1779            whd in ⊢(??%% → ?); #EQ destruct % [2: % [%] %|]
     1780         ]
     1781       | #st1 whd in match accb_store; normalize nodelta @mfr_bind1
     1782         [  @(λregs.sigma_regs (ertl_to_ertlptr prog) sigma regs (joint_if_locals ERTL ? fn))
     1783         |  whd in match sigma_state; normalize nodelta
     1784            @ps_reg_store_ok
     1785         | #regs #st1 whd in match set_regs; whd in match sigma_state; normalize nodelta;
     1786            whd in ⊢(??%% → ?); #EQ destruct % [2: % [%] %|]
     1787         ]
     1788       ]
     1789     ]
     1790   ]
     1791  ] 
     1792| #op #r1 #r2 #st @mfr_bind1
     1793  [ @(sigma_beval (ertl_to_ertlptr prog) sigma)
     1794  | whd in match acca_retrieve; normalize nodelta @ps_reg_retrieve_ok
     1795  | #bv1 @mfr_bind1
     1796    [ @(sigma_beval (ertl_to_ertlptr prog) sigma)
     1797    | @be_op1_ok
     1798    | #bv2 whd in match acca_store; normalize nodelta @mfr_bind1
     1799      [ @(λregs.sigma_regs (ertl_to_ertlptr prog) sigma regs (joint_if_locals ERTL ? fn))
     1800      | whd in match sigma_state; normalize nodelta @ps_reg_store_ok
     1801      | #regs #st1 whd in match set_regs; whd in match sigma_state; normalize nodelta;
     1802            whd in ⊢(??%% → ?); #EQ destruct % [2: % [%] %|]
     1803      ]
     1804    ]
     1805  ]
     1806| #op2 #r1 #r2 #arg #st @mfr_bind1
     1807  [ @(sigma_beval (ertl_to_ertlptr prog) sigma)
     1808  | whd in match acca_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok
     1809  | #bv @mfr_bind1
     1810    [ @(sigma_beval (ertl_to_ertlptr prog) sigma)
     1811    | whd in match snd_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok
     1812    | #bv1 @mfr_bind1
     1813      [@(λx.let 〈bv,b〉≝ x in 〈sigma_beval (ertl_to_ertlptr prog) sigma bv,b〉)
     1814      | @be_op2_ok
     1815      | * #bv2 #b @mfr_bind1
     1816        [ @(λst.sigma_state (ertl_to_ertlptr prog) sigma st (joint_if_locals ERTL ? fn))
     1817        | whd in match acca_store; normalize nodelta @mfr_bind1
     1818          [  @(λregs.sigma_regs (ertl_to_ertlptr prog) sigma regs (joint_if_locals ERTL ? fn))
     1819          | whd in match sigma_state; normalize nodelta @ps_reg_store_ok
     1820          | #regs #st1 whd in match set_regs; whd in match sigma_state; normalize nodelta;
     1821            whd in ⊢(??%% → ?); #EQ destruct % [2: % [%] %|]
     1822          ]
     1823        | #st1 #st2 whd in match set_carry; whd in match sigma_state; normalize nodelta
     1824           whd in ⊢ (??%% → ?); #EQ destruct % [2: % [%] % |] 
     1825        ]
     1826      ]
     1827    ]
     1828  ]
     1829| #st whd in match set_carry; whd in match sigma_state; normalize nodelta
     1830  #st1 whd in ⊢ (??%% → ?); #EQ destruct % [2: % [%] % |]
     1831| #st #st1 whd in match set_carry; whd in match sigma_state; normalize nodelta
     1832   whd in ⊢ (??%% → ?); #EQ destruct % [2: % [%] % |]
     1833| #r1 #dpl #dph #st @mfr_bind1
     1834  [ @(sigma_beval (ertl_to_ertlptr prog) sigma)
     1835  | whd in match dph_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok
     1836  | #bv @mfr_bind1
     1837    [ @(sigma_beval (ertl_to_ertlptr prog) sigma)
     1838    | whd in match dpl_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok
     1839    | #bv1 @mfr_bind1
     1840      [ @(λx.x)
     1841      | @(pointer_of_address_ok ? sigma 〈bv1,bv〉)
     1842      | #ptr @mfr_bind1
     1843        [ @(sigma_beval (ertl_to_ertlptr prog) sigma)
     1844        | @opt_to_res_preserve1 @beloadv_ok
     1845        | #bv2 whd in match acca_store; normalize nodelta @mfr_bind1
     1846          [ @(λregs.sigma_regs (ertl_to_ertlptr prog) sigma regs (joint_if_locals ERTL ? fn))
     1847          |  whd in match sigma_state; normalize nodelta @ps_reg_store_ok
     1848          | #regs #st1 whd in match set_regs; whd in match sigma_state; normalize nodelta;
     1849            whd in ⊢(??%% → ?); #EQ destruct % [2: % [%] %|]
     1850          ]
     1851        ] 
     1852      ]
     1853    ]
     1854  ] 
     1855| #dpl #dph #r #st @mfr_bind1
     1856  [  @(sigma_beval (ertl_to_ertlptr prog) sigma)
     1857  | whd in match dph_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok
     1858  | #bv @mfr_bind1
     1859    [ @(sigma_beval (ertl_to_ertlptr prog) sigma)
     1860    |  whd in match dpl_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok
     1861    | #bv1 @mfr_bind1
     1862      [ @(λx.x)
     1863      |  @(pointer_of_address_ok ? sigma 〈bv1,bv〉)
     1864      | #ptr @mfr_bind1
     1865        [ @(sigma_beval (ertl_to_ertlptr prog) sigma)
     1866        | whd in match acca_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok
     1867        | #bv2 @mfr_bind1
     1868          [ @(sigma_mem (ertl_to_ertlptr prog) sigma)
     1869          | @opt_to_res_preserve1 @bestorev_ok
     1870          | #m #st1 whd in ⊢ (??%% → ?); whd in match set_m; whd in match sigma_state;
     1871            normalize nodelta #EQ destruct % [2: % [%] %|]
     1872          ]
     1873        ]
     1874      ]
     1875    ]
     1876  ]
     1877| #ext #st cases daemon
     1878]
     1879qed.
     1880       
     1881inductive ex_Type1 (A:Type[1]) (P:A → Prop) : Prop ≝
     1882    ex1_intro: ∀ x:A. P x →  ex_Type1 A P.
     1883(*interpretation "exists in Type[1]" 'exists x = (ex_Type1 ? x).*)
     1884
     1885lemma linearise_ok:
     1886 ∀prog.
     1887  let trans_prog ≝ ertl_to_ertlptr prog in
     1888 ∀stack_sizes. sigma_map trans_prog →
     1889   ex_Type1 … (λR.
     1890   status_simulation
     1891    (ERTL_status prog stack_sizes) (ERTLptr_status trans_prog stack_sizes) R).
     1892#prog #stack_size #sigma % [@ERTLptrStatusSimulation assumption]
     1893whd in match status_simulation; normalize nodelta
     1894whd in match ERTL_status; whd in match ERTLptr_status; normalize nodelta
     1895whd in ⊢ (% → % → % → % → ?); #st1 #st1' #st2
     1896whd in match eval_state; normalize nodelta @('bind_inversion) ** #id #fn #stmt
     1897#H lapply (err_eq_from_io ????? H) -H #EQfetch @('bind_inversion) #st #EQst
     1898#EQst1' whd in match ERTLptrStatusSimulation; normalize nodelta
     1899#EQsim whd in match joint_abstract_status in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]);
     1900normalize nodelta whd in match joint_classify; normalize nodelta >EQfetch
     1901>m_return_bind cases stmt in EQst EQst1'; -stmt normalize nodelta
     1902[ * [#called #c_arg #c_dest | #reg #lbl | #seq ] #succ_pc | #fin_step | (*FCOND absurd*) cases daemon]
     1903[3: whd in match joint_classify_step; normalize nodelta whd in match eval_statement_no_pc;
     1904   normalize nodelta #H1 whd in match eval_statement_advance; normalize nodelta
     1905   whd in match set_no_pc; whd in match next; whd in match set_pc; normalize nodelta
     1906   #EQtobdest >EQsim in H1; #H1 cases(eval_seq_no_pc_no_call_ok ????????? H1)
     1907     [2: cases daemon (*TODO*)] #st' * #st_spec' #st_sim %
     1908         [% [ @st'| @(pc … st1') | @(last_pop … st1')]]
     1909         check taa_base
     1910         %{(taaf_step ???? (taa_base … st2) ? ?)}
     1911          [(*dalla commutazione del fetch TODO*) cases daemon
     1912          | whd in match (as_execute ???); whd in match eval_state; normalize nodelta
     1913           cases daemon (*dalla commutazione del fetch + st_spec' TODO *)
     1914          ] normalize nodelta % [% // cases daemon (*facile TODO *)] whd in match label_rel;
     1915           normalize nodelta (*specifica di sigma TODO *) cases daemon
     1916|       
     1917   
     1918
     1919
     1920>EQsim in EQfetch; whd in match sigma_state_pc in ⊢ (%→ ?);
     1921whd in match fetch_statement; normalize nodelta #H @('bind_inversion H) -H
     1922* #id1 #fn1 whd in match fetch_internal_function; normalize nodelta
     1923#H @('bind_inversion H) -H * #id2 #fn2 @if_elim #block_st2_spec
     1924[whd in match dummy_state_pc; whd in match null_pc; normalize nodelta
     1925 lapply(fetch_function_no_zero ??????)
     1926 [2: @(«mk_block Code OZ,refl region Code»)|%|@prog|7: #EQ >EQ |*:]
     1927 whd in ⊢ (???% → ?); #ABS destruct]
     1928 inversion(fetch_function
     1929          (fundef
     1930           (joint_closed_internal_function ERTLptr
     1931            (prog_var_names (joint_function ERTLptr) ℕ (ertl_to_ertlptr prog))))
     1932          (globalenv_noinit (joint_function ERTLptr) (ertl_to_ertlptr prog))
     1933          (pc_block (pc ERTLptr_semantics st2)))
     1934[2: #err #_ normalize nodelta whd in match dummy_state_pc; whd in match null_pc; normalize nodelta
     1935 lapply(fetch_function_no_zero ??????)
     1936 [2: @(«mk_block Code OZ,refl region Code»)|%|@prog|7: #EQ >EQ |*:]
     1937 whd in ⊢ (???% → ?); #ABS destruct] * #id3 #fn3 #EQ  lapply(jmeq_to_eq ??? EQ) -EQ
     1938 #EQffst2 >m_return_bind cases fn3 in EQffst2; -fn3 [2: #ext #_ normalize nodelta
     1939 whd in match dummy_state_pc; whd in match null_pc; normalize nodelta
     1940 lapply(fetch_function_no_zero ??????)
     1941 [2: @(«mk_block Code OZ,refl region Code»)|%|@prog|7: #EQ >EQ |*:]
     1942 whd in ⊢ (???% → ?); #ABS destruct] #fn3 #fn3_spec normalize nodelta
     1943 #fn2_spec >(fetch_function_transf ??????????) in fn3_spec; [2: @fn2_spec|*:]
     1944 cases fn2 in fn2_spec; -fn2 #fn2 #fn2_spec whd in match transf_fundef;
     1945 normalize nodelta whd in ⊢ (??%? → ?); #EQ destruct whd in ⊢ (??%% → ?); #EQ destruct
     1946 #H @('bind_inversion H) -H #stmt1 #H lapply(opt_eq_from_res ???? H) -H #stmt1_spec
     1947 whd in ⊢ (??%% → ?); #EQ destruct cases stmt in stmt1_spec EQst1' EQst; -stmt
     1948 [* [#called #c_arg #c_dest | #reg #lbl | #seq ] #succ_pc | #fin_step | (*FCOND absurd*) cases daemon]
     1949 #stmt_spec whd in match eval_statement_advance; normalize nodelta whd in match eval_call;
     1950 normalize nodelta #EQst1' whd in match eval_statement_no_pc; normalize nodelta
     1951[3: #H cases(eval_seq_no_pc_no_call_ok ????????? H) [2: whd in match fetch_internal_function;
     1952    normalize nodelta whd in match sigma_state_pc; normalize nodelta @if_elim
     1953    [ #H1 >H1 in block_st2_spec; *] #_ whd in match fetch_internal_function; normalize nodelta
     1954    >(fetch_function_transf ??????????) [2: @fn2_spec |*: ] whd in match transf_fundef;
     1955    normalize nodelta >fn2_spec >m_return_bind %] #st3 * #st3_spec #sem_rel
     1956    % [ % [ @st3 | @(pc … st1') | @(last_pop … st2)]] % [%2 [2: %1|1:|4: whd in match as_classifier; normalize nodelta whd in match (as_classify ??); normalize nodelta
     1957   
     1958    %{(taaf_step … (taa_base …) …) I}
     1959 
     1960 
     1961 [1,2,4: whd in ⊢ (??%% → ?); #EQ destruct
     1962 |3: whd in EQst1' : (??%%); whd in match set_no_pc in EQst1'; normalize nodelta in EQst1';
     1963    whd in match sigma_state_pc in EQst1'; normalize nodelta in EQst1';
     1964    >block_st2_spec in EQst1'; @if_elim [ #H >H in block_st2_spec; *] #_
     1965    whd in match fetch_internal_function; normalize nodelta >(fetch_function_transf ??????????) [2: @fn2_spec|*:]
     1966    >m_return_bind whd in match transf_fundef; normalize nodelta whd in match next;
     1967    normalize nodelta whd in match set_pc; normalize nodelta #EQ destruct #H
     1968
     1969   
     1970
     1971   
     1972    whd ;in match  in EQst1';
     1973    destruct #EQst
     1974 #EQst normalize nodelta
     1975 [ whd in match joint_classify_step; normalize nodelta
     1976 
     1977 
     1978 
     1979 lapply(fetch_function_no_zero ??????) [2: @(«mk_block Code OZ,refl region Code»)
     1980 |2: % | %|7: #EQ >EQ *: try assumption
     1981
     1982 normalize in ⊢ (%→ ?);
     1983normalize in as_ex;
     1984
     1985
     1986
Note: See TracChangeset for help on using the changeset viewer.