Changeset 2590


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

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

Location:
src
Files:
8 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/semantics.ma

    r2566 r2590  
    33include alias "common/Identifiers.ma".
    44
    5 record ertl_psd_env : Type[0] ≝
    6   { psd_regs : register_env beval
    7   (* this tells what pseudo-registers should have their value corrected by spilled_no *)
    8   ; need_spilled_no : identifier_set RegisterTag
    9   }.
    10 
    11 definition set_psd_regs ≝ λx,env.mk_ertl_psd_env x (need_spilled_no env).
    12 definition add_need_spilled_no ≝
    13   λr,env.mk_ertl_psd_env (psd_regs env) (add_set … (need_spilled_no env) r).
    14 definition rm_need_spilled_no ≝
    15   λr,env.mk_ertl_psd_env (psd_regs env) (need_spilled_no env ∖  {(r)}).
    16 
    17 definition ertl_reg_env ≝ ertl_psd_env × hw_register_env.
     5definition ertl_reg_env ≝ register_env beval × hw_register_env.
    186
    197definition ps_reg_store: ? → ? → ? → res ? ≝
    208 λr,v.λlocal_env : ertl_reg_env.
    21   do res ← reg_store r v (psd_regs (\fst local_env)) ;
    22   let psd_env ≝ set_psd_regs res (\fst local_env) in
    23   OK … 〈rm_need_spilled_no r psd_env, \snd local_env〉.
     9  do res ← reg_store r v (\fst local_env) ;
     10  OK … 〈res, \snd local_env〉.
    2411
    2512definition ps_reg_retrieve ≝
    26  λlocal_env:ertl_reg_env. reg_retrieve … (psd_regs (\fst local_env)).
     13 λlocal_env:ertl_reg_env. reg_retrieve … (\fst local_env).
    2714
    2815definition hw_reg_store ≝
     
    4229  ].
    4330
     31definition get_hwsp : ertl_reg_env → res xpointer ≝
     32 λst.hwreg_retrieve_sp (\snd st).
    4433
     34definition set_hwsp : ertl_reg_env → xpointer → ertl_reg_env ≝
     35 λst,sp.〈\fst st, hwreg_store_sp (\snd st) sp〉.
    4536
    4637definition ERTL_state : sem_state_params ≝
    4738  mk_sem_state_params
    48  (* framesT ≝ *) (list ertl_psd_env)
     39 (* framesT ≝ *) (list (register_env beval × ident))
    4940 (* empty_framesT ≝ *) [ ]
    5041 (* regsT ≝ *) ertl_reg_env
    51  (* empty_regsT ≝ *) (λsp.〈mk_ertl_psd_env (empty_map …) ∅,init_hw_register_env sp〉)
    52  (*load_sp ≝ *) ?
    53   (*save_sp ≝ *) ?. cases daemon qed.
     42 (* empty_regsT ≝ *) (λsp.〈empty_map …,init_hw_register_env sp〉)
     43 (*load_sp ≝ *) get_hwsp
     44 (*save_sp ≝ *) set_hwsp.
    5445
    5546(* we ignore need_spilled_no as we never move framesize based values around in the
     
    7162definition ertl_allocate_local ≝
    7263  λreg.λlenv : ertl_reg_env.
    73   〈set_psd_regs (add … (psd_regs (\fst lenv)) reg BVundef) (\fst lenv), \snd lenv〉.
     64  〈 add … (\fst lenv) reg BVundef, \snd lenv〉.
     65
    7466
    7567definition ertl_save_frame:
    76  call_kind → unit → state_pc ERTL_state → res (state … ERTL_state) ≝
    77  λ_.λ_.λst.
     68 call_kind → unit → ident → state_pc ERTL_state → res (state … ERTL_state) ≝
     69 λ_.λ_.λid.λst.
    7870  do st ← push_ra … st (pc … st) ;
    7971  OK …
    80    (set_frms ERTL_state (\fst (regs ERTL_state st) :: (st_frms … st))
    81     (set_regs ERTL_state 〈mk_ertl_psd_env (empty_map …) ∅,\snd (regs … st)〉 st)).
     72   (set_frms ERTL_state (〈\fst (regs ERTL_state st),id〉 :: (st_frms … st))
     73    (set_regs ERTL_state 〈empty_map …,\snd (regs … st)〉 st)).
    8274
    8375(*CSC: XXXX, for external functions only*)
     
    9385  return (set_regs ERTL_state 〈\fst (regs … st), env'〉 st).*)
    9486
    95 definition xdata_pointer_of_address: address → res xpointer ≝
    96 λp.let 〈v1,v2〉 ≝ p in
    97 ! p ← pointer_of_bevals [v1;v2] ;
    98 match ptype p return λpty. ptype p = pty → res (Σp:pointer. ptype p = XData) with
    99 [ XData ⇒ λE.OK ? (mk_Sig … p E)
    100 | _ ⇒ λ_.Error … [MSG BadPointer]
    101 ] (refl …).
    102 
    103 definition address_of_xdata_pointer: xpointer → address ≝
    104 λp.list_to_pair … (bevals_of_pointer p) ?. % qed.
    105 
    106 definition get_hwsp : state ERTL_state → res xpointer ≝
    107  λst.
    108   let spl ≝ hwreg_retrieve (\snd (regs … st)) RegisterSPL in
    109   let sph ≝ hwreg_retrieve (\snd (regs … st)) RegisterSPH in
    110   xdata_pointer_of_address 〈spl,sph〉.
    111 
    112 definition set_hwsp : xpointer → state ERTL_state → state ERTL_state ≝
    113  λsp,st.
    114   let 〈spl,sph〉 ≝ address_of_xdata_pointer sp in
    115   let hwregs ≝ hwreg_store RegisterSPL spl (\snd (regs … st)) in
    116   let hwregs ≝ hwreg_store RegisterSPH sph hwregs in
    117   set_regs ERTL_state 〈\fst (regs … st),hwregs〉 st.
    118 
    11987axiom FunctionNotFound: errmsg.
    12088
     
    12694  let env ≝ regs … st in
    12795  ! env' ← ps_reg_store dst v env ;
    128   let env'' ≝ 〈add_need_spilled_no dst (\fst env'), \snd env'〉 in
    129   return set_regs ERTL_state env'' st.
     96  return set_regs ERTL_state env' st.
    13097
    13198definition eval_ertl_seq:
     
    138105  match stm with
    139106   [ ertl_new_frame ⇒
    140       ! sp ← get_hwsp st ;
     107      ! sp ← sp … st ;
    141108      let newsp ≝ shift_pointer … sp framesize in
    142       return set_hwsp newsp st
     109      return set_sp … newsp st
    143110   | ertl_del_frame ⇒
    144       ! sp ← get_hwsp st ;
     111      ! sp ← sp … st ;
    145112      let newsp ≝ shift_pointer … sp framesize in
    146       return set_hwsp newsp st
     113      return set_sp … newsp st
    147114   | ertl_frame_size dst ⇒ ps_reg_store_status dst (BVByte framesize) st
    148115   ]. @hide_prf whd in match newsp; cases sp #ptr #EQ <EQ % qed. 
    149 
    150 definition ertl_post_op2 ≝
    151   λop,dst,arg1,arg2,st.
    152   let local_env ≝ regs ERTL_state st in
    153   let f ≝ λarg,st.match arg with
    154      [ Reg r ⇒
    155        if r ∈ need_spilled_no (\fst local_env) then
    156          set_regs ERTL_state 〈add_need_spilled_no dst (\fst local_env),\snd local_env〉 st
    157        else
    158          st
    159      | _ ⇒ st
    160      ] in
    161   match op with
    162   [ Add ⇒ f arg1 (f arg2 st) (* won't happen both *)
    163   | Addc ⇒ f arg1 (f arg2 st) (* we have to think about what should we do with carry bit *)
    164   | Sub ⇒ f arg1 st
    165   | _ ⇒ st].
    166116         
    167117definition ERTL_semantics ≝
  • 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
  • src/ERTLptr/semantics.ma

    r2566 r2590  
    22include "ERTLptr/ERTLptr.ma". (* CSC: syntax.ma in RTLabs *)
    33include "ERTL/semantics.ma".
    4 include "common/extraGlobalenvs.ma".
    54include alias "common/Identifiers.ma".
    6 (*
    7 record ertl_psd_env : Type[0] ≝
    8   { psd_regs : register_env beval
    9   (* this tells what pseudo-registers should have their value corrected by spilled_no *)
    10   ; need_spilled_no : identifier_set RegisterTag
    11   }.
    12 
    13 definition set_psd_regs ≝ λx,env.mk_ertl_psd_env x (need_spilled_no env).
    14 definition add_need_spilled_no ≝
    15   λr,env.mk_ertl_psd_env (psd_regs env) (add_set … (need_spilled_no env) r).
    16 definition rm_need_spilled_no ≝
    17   λr,env.mk_ertl_psd_env (psd_regs env) (need_spilled_no env ∖  {(r)}).
    18 
    19 definition ertl_reg_env ≝ ertl_psd_env × hw_register_env.
    20 
    21 definition ps_reg_store: ? → ? → ? → res ? ≝
    22  λr,v.λlocal_env : ertl_reg_env.
    23   do res ← reg_store r v (psd_regs (\fst local_env)) ;
    24   let psd_env ≝ set_psd_regs res (\fst local_env) in
    25   OK … 〈rm_need_spilled_no r psd_env, \snd local_env〉.
    26 
    27 definition ps_reg_retrieve ≝
    28  λlocal_env:ertl_reg_env. reg_retrieve … (psd_regs (\fst local_env)).
    29 
    30 definition hw_reg_store ≝
    31  λr,v.λlocal_env:ertl_reg_env.
    32   OK … 〈\fst local_env,hwreg_store r v (\snd local_env)〉.
    33 
    34 definition hw_reg_retrieve ≝
    35  λlocal_env:ertl_reg_env.λreg.
    36   OK … (hwreg_retrieve … (\snd local_env) reg).
    37 
    38 
    39 definition ps_arg_retrieve : ertl_reg_env → argument ? → res beval ≝
    40   λlocal_env,a.
    41   match a with
    42   [ Reg r ⇒ ps_reg_retrieve local_env r
    43   | Imm b ⇒ return BVByte b
    44   ].
    45 
    46 
    47 
    48 definition ERTL_state : sem_state_params ≝
    49   mk_sem_state_params
    50  (* framesT ≝ *) (list ertl_psd_env)
    51  (* empty_framesT ≝ *) [ ]
    52  (* regsT ≝ *) ertl_reg_env
    53  (* empty_regsT ≝ *) (λsp.〈mk_ertl_psd_env (empty_map …) ∅,init_hw_register_env sp〉)
    54  (*load_sp ≝ *) ?
    55   (*save_sp ≝ *) ?. cases daemon qed.
    56 
    57 (* we ignore need_spilled_no as we never move framesize based values around in the
    58    translation *)
    59 definition ertl_eval_move ≝ λenv,pr.
    60       ! v ←
    61         match \snd pr with
    62         [ Reg src ⇒
    63           match src with
    64           [ PSD r ⇒ ps_reg_retrieve env r
    65           | HDW r ⇒ hw_reg_retrieve env r
    66           ]
    67         | Imm b ⇒ return BVByte b ] ;
    68       match \fst pr with
    69       [ PSD r ⇒ ps_reg_store r v env
    70       | HDW r ⇒ hw_reg_store r v env
    71       ].
    72 
    73 definition ertl_allocate_local ≝
    74   λreg.λlenv : ertl_reg_env.
    75   〈set_psd_regs (add … (psd_regs (\fst lenv)) reg BVundef) (\fst lenv), \snd lenv〉.
    76 *)
    775
    786definition ertlptr_save_frame:
    79  call_kind → unit → state_pc ERTL_state → res (state … ERTL_state) ≝
    80  λk.λ_.λst.
     7 call_kind → unit → ident → state_pc ERTL_state → res (state … ERTL_state) ≝
     8 λk.λ_.λid.λst.
    819 do st ← match k with [ID ⇒ push_ra … st (pc … st) |
    8210 PTR ⇒ return (st_no_pc … st)] ; OK …
    83    (set_frms ERTL_state (\fst (regs ERTL_state st) :: (st_frms … st))
    84     (set_regs ERTL_state 〈mk_ertl_psd_env (empty_map …) ∅,\snd (regs … st)〉 st)).
    85 
    86 (*
    87 (*CSC: XXXX, for external functions only*)
    88 axiom ertl_fetch_external_args: external_function → state ERTL_state → call_args ERTL → res (list val).
    89 axiom ertl_set_result : list val → unit → state ERTL_state → res (state ERTL_state).
    90 (* I think there should be a list beval in place of list val here
    91   λvals.λ_.λst.
    92   (* set all RegisterRets to 0 *)
    93   let reset ≝ λenv,r.hwreg_store r (BVByte (bv_zero …)) env in
    94   let env ≝ foldl … reset (\snd (regs … st)) RegisterRets in
    95   let set_vals ≝ λenv,pr.hwreg_store (\fst pr) (\snd pr) env in ?.
    96   let env' ≝ foldl … set_vals env (zip_pottier … RegisterRets vals) in
    97   return (set_regs ERTL_state 〈\fst (regs … st), env'〉 st).*)
    98 
    99 definition xdata_pointer_of_address: address → res xpointer ≝
    100 λp.let 〈v1,v2〉 ≝ p in
    101 ! p ← pointer_of_bevals [v1;v2] ;
    102 match ptype p return λpty. ptype p = pty → res (Σp:pointer. ptype p = XData) with
    103 [ XData ⇒ λE.OK ? (mk_Sig … p E)
    104 | _ ⇒ λ_.Error … [MSG BadPointer]
    105 ] (refl …).
    106 
    107 definition address_of_xdata_pointer: xpointer → address ≝
    108 λp.list_to_pair … (bevals_of_pointer p) ?. % qed.
    109 
    110 definition get_hwsp : state ERTL_state → res xpointer ≝
    111  λst.
    112   let spl ≝ hwreg_retrieve (\snd (regs … st)) RegisterSPL in
    113   let sph ≝ hwreg_retrieve (\snd (regs … st)) RegisterSPH in
    114   xdata_pointer_of_address 〈spl,sph〉.
    115 
    116 definition set_hwsp : xpointer → state ERTL_state → state ERTL_state ≝
    117  λsp,st.
    118   let 〈spl,sph〉 ≝ address_of_xdata_pointer sp in
    119   let hwregs ≝ hwreg_store RegisterSPL spl (\snd (regs … st)) in
    120   let hwregs ≝ hwreg_store RegisterSPH sph hwregs in
    121   set_regs ERTL_state 〈\fst (regs … st),hwregs〉 st.
    122 
    123 axiom FunctionNotFound: errmsg.*)
     11   (set_frms ERTL_state (〈\fst (regs ERTL_state st),id〉 :: (st_frms … st))
     12    (set_regs ERTL_state 〈empty_map …,\snd (regs … st)〉 st)).
    12413
    12514definition eval_ertlptr_seq:
     
    13019  match stm with
    13120   [ ertlptr_ertl seq ⇒ eval_ertl_seq F globals ge seq id st
    132    | LOW_ADDRESS r l ⇒  ! pc_lab ←  (pc_of_label ?? ? (block_of_funct … ge id) l);
    133                         let 〈addrl,addrh〉 ≝  beval_pair_of_pc pc_lab in
     21   | LOW_ADDRESS r l ⇒  ! pc_lab ← get_pc_from_label … ge id l;
     22                        let 〈addrl,addrh〉 ≝ beval_pair_of_pc pc_lab in
    13423                        ps_reg_store_status r addrl st
    135    | HIGH_ADDRESS r l ⇒ ! pc_lab ←  (pc_of_label ?? ? (block_of_funct … ge id) l);
     24   | HIGH_ADDRESS r l ⇒ ! pc_lab ← get_pc_from_label … ge id l;
    13625                        let 〈addrl,addrh〉 ≝  beval_pair_of_pc pc_lab in
    13726                        ps_reg_store_status r addrh st
    13827   ].
    139  [3,8: (* PAOLO, HELP: we should pass ge, but the type is abstracted over F! *)
    140        cases daemon
    141  |4,5,9,10: cases daemon (* Closed by side effect for 3,8 *)
    142  |1,6: (* PAOLO, HELP: this should be an hypothesis that needs to propagate
    143           a long way and then be discarded in Joint/semantics.ma *)
    144        cases daemon
    145  |2,7: @block_of_funct_ident_is_code ]
    146 qed.
    147 
    148 (*
    149 definition ertl_post_op2 ≝
    150   λop,dst,arg1,arg2,st.
    151   let local_env ≝ regs ERTL_state st in
    152   let f ≝ λarg,st.match arg with
    153      [ Reg r ⇒
    154        if r ∈ need_spilled_no (\fst local_env) then
    155          set_regs ERTL_state 〈add_need_spilled_no dst (\fst local_env),\snd local_env〉 st
    156        else
    157          st
    158      | _ ⇒ st
    159      ] in
    160   match op with
    161   [ Add ⇒ f arg1 (f arg2 st) (* won't happen both *)
    162   | Addc ⇒ f arg1 (f arg2 st) (* we have to think about what should we do with carry bit *)
    163   | Sub ⇒ f arg1 st
    164   | _ ⇒ st].
    165 *)
    166 
     28   
    16729definition ERTLptr_semantics ≝
    16830  make_sem_graph_params ERTLptr
  • src/common/ExtraMonads.ma

    r2570 r2590  
    6363  ; 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
    6464  }.
     65 
     66record MonadFunctRel1 (M1 : Monad) (M2 : Monad) : Type[1] ≝
     67{ m_frel1  :5> ∀X,Y.(Y → X) → (M1 X → M2 Y → Prop)
     68; mfr_return1 : ∀X,Y,F,y.m_frel1 X Y F (return (F y)) (return y)
     69; mfr_bind1 : ∀X,Y,Z,W,F,G,m,n. m_frel1 X Y F m n →
     70       ∀f,g.(∀x.m_frel1 Z W G (f (F x)) (g x)) → m_frel1 ?? G (m_bind … m f) (m_bind … n g)
     71; m_frel_ext1 : ∀X,Y,F,G.(∀x.F  x = G x) → ∀ u,v.m_frel1 X Y F u v → m_frel1 X Y G u v
     72}.
     73
    6574
    6675definition res_preserve : MonadFunctRel Res Res ≝
     
    7887qed.
    7988
     89definition res_preserve1 : MonadFunctRel1 Res Res ≝
     90mk_MonadFunctRel1 ??
     91(λX,Y,F,m,n.∀y.m = return y → ∃ x. n = return x ∧ y = F x)
     92???.
     93[ #X #Y #F #y #x normalize #EQ destruct(EQ) %{y} % //
     94| #X #Y #Z #W #F #G * [#x | #e] #n #H #f #g #H1 #z whd in ⊢ (??%% → ?); #EQ destruct
     95  cases(H x (refl …)) #y * #n_spec #x_spec
     96  cases(H1 y z ?) [2: <x_spec whd in ⊢ (???%); assumption] #w * #w_spec #z_spec %{w}
     97  >n_spec <w_spec % //
     98| #X #Y #F #G #ext #u #v #K #x #u_spec cases(K x u_spec) #y * #v_spec #y_spec %{y}
     99  % //
     100]
     101qed.
     102
    80103definition opt_preserve : MonadFunctRel Option Option ≝
    81104  mk_MonadFunctRel ??
     
    92115qed.
    93116
     117definition opt_preserve1 : MonadFunctRel1 Option Option ≝
     118  mk_MonadFunctRel1 ??
     119  (λX,Y,F,m,n.∀y.m = return y → ∃ x. n = return x ∧ y = F x)
     120???.
     121[ #X #Y #F #y #x normalize #EQ destruct(EQ) %{y} % //
     122| #X #Y #Z #W #F #G * [| #x] #n #H #f #g #H1 #z whd in ⊢ (??%% → ?); #EQ destruct
     123  cases(H x (refl …)) #y * #n_spec #x_spec
     124  cases(H1 y z ?) [2: <x_spec whd in ⊢ (???%); assumption] #w * #w_spec #z_spec %{w}
     125  >n_spec <w_spec % //
     126| #X #Y #F #G #ext #u #v #K #x #u_spec cases(K x u_spec) #y * #v_spec #y_spec %{y}
     127  % //
     128]
     129qed.
     130
    94131definition io_preserve : ∀O,I.MonadFunctRel (IOMonad O I) (IOMonad O I) ≝
    95132  λO,I.mk_MonadFunctRel ??
     
    103140| #X #Y #P #F #G #H #u #v #K #x #EQ
    104141  cases (K … EQ) #prf #EQ' %{prf} >EQ' >H try %
     142]
     143qed.
     144
     145definition io_preserve1 :  ∀O,I.MonadFunctRel1 (IOMonad O I) (IOMonad O I) ≝
     146  λO,I.mk_MonadFunctRel1 ??
     147  (λX,Y,F,m,n.∀y.m = return y → ∃ x. n = return x ∧ y = F x)
     148???.
     149[ #X #Y #F #y #x normalize #EQ destruct(EQ) %{y} % //
     150| #X #Y #Z #W #F #G * [#o #r | #x | #e] #n #H #f #g #H1 #z whd in ⊢ (??%% → ?); #EQ destruct
     151  cases(H x (refl …)) #y * #n_spec #x_spec
     152  cases(H1 y z ?) [2: <x_spec whd in ⊢ (???%); assumption] #w * #w_spec #z_spec %{w}
     153  >n_spec <w_spec % //
     154| #X #Y #F #G #ext #u #v #K #x #u_spec cases(K x u_spec) #y * #v_spec #y_spec %{y}
     155  % //
    105156]
    106157qed.
     
    118169  FR … G
    119170    (f x) (g (F x prf)).
     171
     172definition preserving1 ≝   
     173  λM1,M2.λFR : MonadFunctRel1 M1 M2.
     174  λX,Y,A,B : Type[0].
     175  λF : Y → X.
     176  λG : B → A.
     177  λf : X → M1 A.
     178  λg : Y → M2 B.
     179  ∀ y.
     180  FR ?? G (f (F y)) (g y).
    120181
    121182definition preserving2 ≝
     
    133194  FR … H
    134195    (f x y) (g (F x prf1) (G y prf2)).
    135 
     196   
     197definition preserving21 ≝
     198   λM1,M2.λFR : MonadFunctRel1 M1 M2.
     199   λX,Y,Z,W,A,B : Type[0].
     200   λF : Z → X.
     201   λG : W → Y.
     202   λH : B → A.
     203   λf : X → Y → M1 A.
     204   λg : Z → W → M2 B.
     205   ∀z,w. FR ?? H (f (F z) (G w)) (g z w).
     206   
    136207lemma res_preserve_error : ∀X,Y,P,F,e,n.res_preserve X Y P F (Error … e) n.
    137208#X #Y #P #F #e #n #x whd in ⊢ (??%%→?); #EQ destruct(EQ) qed.
     209
     210lemma res_preserve_error1 : ∀X,Y,F,e,n.res_preserve1 X Y F (Error … e) n.
     211#X #Y #F #e #n #x whd in ⊢ (??%%→?); #EQ destruct(EQ) qed.
    138212
    139213lemma mfr_return_eq : ∀M1,M2.∀FR : MonadFunctRel M1 M2.
     
    143217#M1 #M2 #FR #X #Y #P #F #v #n #prf #EQ >EQ @mfr_return qed.
    144218
     219lemma mfr_return_eq1 :∀M1,M2.∀FR : MonadFunctRel1 M1 M2.
     220∀X,Y,F,v,n.
     221n = return F v →
     222FR X Y F n (return v).
     223#M1 #M2 #FR #X #Y #F #v #n #EQ >EQ @mfr_return1
     224qed.
     225
    145226lemma opt_safe_eq : ∀A,m,x,prf.m = Some A x → opt_safe A m prf = x.
    146227#A #m #x #prf @opt_safe_elim #x' #EQ >EQ #EQ' destruct % qed.
     
    148229lemma opt_preserve_none : ∀X,Y,P,F,n.opt_preserve X Y P F (None ?) n.
    149230#X #Y #P #F #n #x whd in ⊢ (??%%→?); #EQ destruct(EQ) qed.
     231
     232lemma opt_preserve_none1 :  ∀X,Y,F,n.opt_preserve1 X Y F (None ?) n.
     233#X #Y #F #n #x whd in ⊢ (???% → ?); #EQ destruct qed.
    150234
    151235lemma m_list_map_All_ok :
     
    176260qed.
    177261
     262lemma res_to_opt__preserve : ∀X,Y,F,m,n.
     263  res_preserve1 X Y F m n → opt_preserve1 X Y F (res_to_opt … m) (res_to_opt … n).
     264#X #Y #F #m #n #H #x #EQ
     265whd in H; cases (H x ?)
     266[ #y * #y_spec #x_spec %{y} % [ >y_spec %|assumption]
     267| cases m in EQ; normalize #x #EQ destruct %
     268]
     269qed.
     270
    178271lemma opt_to_res_preserve : ∀X,Y,P,F,m,n,e1,e2.
    179272       opt_preserve X Y P F m n →
     
    184277qed.
    185278
     279lemma opt_to_res_preserve1 :  ∀X,Y,F,m,n,e1,e2.
     280       opt_preserve1 X Y F m n →
     281       res_preserve1 X Y F (opt_to_res … e1 m) (opt_to_res … e2 n).
     282#X #Y #F #m #n #e1 #e2 #H #x #EQ
     283cases(H x ?)
     284[ #y * #y_spec #x_spec %{y} % [>y_spec %|assumption]
     285| cases m in EQ; normalize [2: #x1] #EQ destruct %
     286]
     287qed.
     288
    186289lemma err_eq_from_io : ∀O,I,X,m,v.
    187290  err_to_io O I X m = return v → m = return v.
     
    196299qed.
    197300
     301lemma res_to_io_preserve1 : ∀O,I,X,Y,F,m,n.
     302       res_preserve1 X Y F m n →
     303       io_preserve1 O I X Y F m n.
     304#O #I #X #Y #F #m #n #H #v #EQ cases(H v (err_eq_from_io ????? EQ))
     305#y * #y_spec #v_spec %{y} % // >y_spec %
     306qed.
  • src/common/PositiveMap.ma

    r2541 r2590  
    458458  [ pm_leaf ⇒ map_opt ?? (λx.choice (Some ? x) (None ?)) a
    459459  | pm_node o' l' r' ⇒
    460     pm_node ? (choice o o')
     460    match (choice o o') with 
     461    [None ⇒
     462      match (merge … choice l l') with
     463      [pm_leaf ⇒ match (merge … choice r r') with
     464          [pm_leaf ⇒ pm_leaf ?
     465          |_ ⇒ pm_node ? (None ?) (merge … choice l l') (merge … choice r r')
     466          ]
     467      |_ ⇒ pm_node ? (None ?) (merge … choice l l') (merge … choice r r')
     468      ]
     469   |Some x ⇒
     470    pm_node ? (Some ? x)
    461471      (merge … choice l l')
    462472      (merge … choice r r')
    463473  ]
    464 ].
     474]].
    465475
    466476lemma lookup_opt_merge : ∀A,B,C,choice,a,b,p.
     
    470480 #A#B#C#choice#a elim a
    471481[ normalize #b
    472 | #o#l#r#Hil#Hir * [2: #o'#l'#r' * normalize /2 by /]
    473 ]
    474 #p#choice_good >lookup_opt_map
     482| #o#l#r#Hil#Hir * [2: #o'#l'#r' * [2,3: #x] normalize cases(choice o o') normalize /2 by /
     483  [3: cases (merge A B C choice l l') normalize /2 by / cases(merge A B C choice r r')
     484      normalize /2 by /
     485  |*: #H [<Hir|<Hil] /2 by / cases(merge A B C choice l l') normalize /2 by /
     486      cases (merge A B C choice r r') normalize /2 by /
     487  ]
     488]]
     489#p #choice_good >lookup_opt_map
    475490elim (lookup_opt ???)
    476491normalize //
    477 qed.
     492qed. 
    478493
    479494let rec domain_size (A : Type[0]) (b : positive_map A) on b : ℕ ≝
  • src/common/extraGlobalenvs.ma

    r2570 r2590  
    2121    In ? (prog_vars ?? p) 〈〈id, r〉, v〉 →
    2222    ∃b. find_symbol ? (globalenv ?? init p) id = Some ? b.
    23 *)
    2423
    2524definition is_function ≝ λF.λge : genv_t F.
     
    4746| None ⇒ λ_.None ?
    4847] (refl …).
     48*)
    4949
    5050lemma symbol_of_function_block_ok :
     
    6161qed.
    6262
     63(*
    6364definition funct_of_block : ∀F,ge.
    6465  block → option  (Σi.is_function F ge i) ≝
     
    193194>(find_funct_ptr_transf … EQfunct) #EQ'' destruct %
    194195qed.
    195 
     196*)
    196197
    197198include alias "common/PositiveMap.ma".
     
    234235qed.
    235236
    236 
    237 
     237lemma globalenv_no_zero :
     238 ∀F,V,i,p.
     239  find_funct_ptr … (globalenv F V i p) (mk_block Code OZ) = None ?. //
     240qed.
     241
  • src/joint/Traces.ma

    r2562 r2590  
    4747λpars.
    4848let p ≝ prog pars in
     49let spars ≝ prog_spars pars in
     50let genv ≝ globalenv_noinit ? p in
     51let get_pc_lbl ≝ λid,lbl.
     52  ! bl ← block_of_funct_id … spars genv id ;
     53  pc_of_label … genv bl lbl in
    4954mk_evaluation_params
    5055  (prog_var_names … p)
    51   (prog_spars pars)
    52   (mk_genv_gen ?? (globalenv_noinit ? p) ? (stack_sizes pars))
     56  spars
     57  (mk_genv_gen ?? genv ? (stack_sizes pars) get_pc_lbl)
    5358 (* (prog_io pars) *).
    5459#s #H
     
    7984  (* use exit_pc as ra and call_dest_for_main as dest *)
    8085  let st0' ≝ mk_state_pc … (set_sp … spp st0) exit_pc exit_pc in
    81   ! st0_no_pc ← save_frame ?? sem_globals ID (call_dest_for_main … pars) st0' ;
     86  ! st0_no_pc ← save_frame ?? sem_globals ID (call_dest_for_main … pars) (prog_main … p) st0' ;
    8287  let st0'' ≝ set_no_pc … st0_no_pc st0' in
    8388  ! bl ← block_of_call … ge (inl … main) st0'';
  • src/joint/semantics.ma

    r2570 r2590  
    1717; find_symbol_in_globals : ∀s.In … globals s → find_symbol … ge s ≠ None ?
    1818; stack_sizes : ident → option ℕ
     19; get_pc_from_label : ident (* current function *) → label → res program_counter
    1920}.
    2021
     
    7576definition exit_pc : program_counter ≝
    7677  mk_program_counter «mk_block Code (-1), refl …» one.
     78
     79definition null_pc : program_counter ≝
     80    mk_program_counter «mk_block Code OZ, refl …» one.
    7781
    7882definition set_m: ∀p. bemem → state p → state p ≝
     
    194198  (* Paolo: save_frame separated from call_setup to factorize tailcall code *)
    195199  ; allocate_locals_ : localsT uns_pars → regsT st_pars → regsT st_pars
    196   ; save_frame: call_kind → call_dest uns_pars → state_pc st_pars → res (state st_pars)
     200  ; save_frame: call_kind → call_dest uns_pars → ident → state_pc st_pars → res (state st_pars)
    197201   (*CSC: setup_call returns a res only because we can call a function with the wrong number and
    198202     type of arguments. To be fixed using a dependent type *)
     
    484488  ] (refl …).
    485489
    486 (* to be used in implementations *)
    487 definition block_of_call_id ≝  λF.λsp:sem_state_params.
    488   λge: genv_t F.λid.λst:state sp.
     490definition block_of_funct_id ≝  λF.λsp:sem_state_params.
     491  λge: genv_t F.λid.
    489492  opt_to_res … [MSG BadFunction; CTX … id] (
    490493    ! bl ← find_symbol … ge id;
     
    530533definition is_inl : ∀A,B.A+B → bool ≝ λA,B,x.match x with [ inl _ ⇒ true | _ ⇒ false ].
    531534
     535
    532536definition eval_call ≝
    533537λp : sem_params.λglobals : list ident.λge : genv p globals.λf,args,dest,nxt.
     
    537541match fd with
    538542[ Internal ifd ⇒
    539   ! st' ← save_frame … (kind_of_call … f) dest st ;
     543  let ident ≝ ? in
     544  ! st' ← save_frame … (kind_of_call … f) dest ident st ;
    540545  ! st'' ← eval_internal_call p globals ge i ifd args st' ;
    541546  let pc ≝ pc_of_point p bl (joint_if_entry … ifd) in
     
    544549  ! st' ← eval_external_call … efd args dest st ;
    545550  return mk_state_pc … st' (succ_pc p (pc … st) nxt) (last_pop … st)
    546 ].
     551]. cases daemon qed. (*TODO*)
    547552
    548553definition eval_statement_no_pc :
Note: See TracChangeset for help on using the changeset viewer.