Changeset 3154


Ignore:
Timestamp:
Apr 17, 2013, 2:53:45 PM (4 years ago)
Author:
piccolo
Message:

1) changed block_of_call in order to prevent pre-main calls
2) StatusSimulationHelper? in place

Location:
src
Files:
1 added
3 edited

Legend:

Unmodified
Added
Removed
  • src/common/StatusSimulation.ma

    r3145 r3154  
    150150    ]
    151151; sim_final :
    152   ∀st1,st2.as_result S1 st1 = as_result S2 st2
     152  ∀st1,st2.sim_status_rel st1 st2 → as_result S1 st1 = as_result S2 st2
    153153}.
    154154
  • src/joint/StatusSimulationHelper.ma

    r3118 r3154  
    1313(**************************************************************************)
    1414
    15 include "joint/semanticsUtils.ma".
    16 include "joint/Traces.ma".
    17 include "common/StatusSimulation.ma".
    18 include "joint/semantics_blocks.ma".
    19 include "utilities/listb_extra.ma".
    20 include "utilities/lists.ma".
    21 
    22 lemma set_no_pc_eta:
    23  ∀P.∀st1: state_pc P. set_no_pc P st1 st1 = st1.
    24 #P * //
    25 qed.
    26 
    27 lemma pc_of_label_eq :
    28   ∀pars: sem_graph_params.
    29   ∀globals,ge,bl,i_fn,lbl.
    30   fetch_internal_function ? globals ge bl = return i_fn →
    31   pc_of_label pars globals ge bl lbl =
    32     OK ? (pc_of_point pars bl lbl).
    33 #p #globals #ge #bl #i_fn #lbl #EQf
    34 whd in match pc_of_label;
    35 normalize nodelta >EQf >m_return_bind %
    36 qed.
    37 
    38 
    39 lemma bind_new_bind_new_instantiates :
    40 ∀B,X : Type[0]. ∀ m : bind_new B X. ∀ x : X. ∀l : list B.∀P.
    41 bind_new_instantiates B X x m l → bind_new_P' ?? P m →
    42 P l x.
    43 #B #X #m elim m normalize nodelta
    44 [#x #y * normalize // #B #l' #P *
    45 | #f #IH #x #l elim l normalize [#P *] #hd #tl normalize #_ #P #H #Hr @(IH … H)
    46  @Hr
    47 ]
    48 qed.
    49 
    50 let rec bind_instantiate B X (b : bind_new B X) (l : list B) on b : (option X) ≝
    51   match b with
    52   [ bret B ⇒
    53     match l with
    54     [ nil ⇒ Some ? B
    55     | _ ⇒ None ?
    56     ]
    57   | bnew f ⇒
    58     match l with
    59     [ nil ⇒ None ?
    60     | cons r l' ⇒
    61       bind_instantiate B X (f r) l'
    62     ]
    63   ].
    64  
    65 lemma bind_instantiates_to_instantiate : ∀B,X.∀b : bind_new B X.
    66 ∀l : list B.∀x : X.
    67 bind_instantiate B X b l = Some ? x →
    68 bind_new_instantiates B X x b l.
    69 #B #X #b elim b
    70 [#x1 * [2: #hd #tl] #x whd in ⊢ (??%? → ?); #EQ destruct(EQ) %
    71 |#f #IH * [2: #hd #tl] #x whd in ⊢ (??%? → ?); [2: #EQ destruct(EQ)] #H
    72  whd @IH assumption
    73 ]
    74 qed.
    75 
    76 lemma bind_instantiate_instantiates : ∀B,X.∀b : bind_new B X.
    77 ∀l : list B.∀x : X.
    78 bind_new_instantiates B X x b l →
    79 bind_instantiate B X b l = Some ? x.
    80 #B #X #b elim b
    81 [ #x1 * [2: #hd #tl] #x whd in ⊢ (% → ?); [*] #EQ destruct(EQ) %
    82 | #f #IH * [2: #hd #tl] #x whd in ⊢ (% → ?); [2: *] #H whd in ⊢ (??%?); @IH @H
    83 ]
    84 qed.
    85 
    86 coercion bind_instantiate_instantiates : ∀B,X.∀b : bind_new B X.
    87 ∀l : list B.∀x : X.
    88 ∀prf : bind_new_instantiates B X x b l.
    89 bind_instantiate B X b l = Some ? x ≝
    90 bind_instantiate_instantiates
    91 on _prf : bind_new_instantiates ?????
    92 to eq (option ?) (bind_instantiate ????) (Some ??).
    93 
    94 definition lbl_funct_type ≝  block → label → (list label).
    95 definition regs_funct_type ≝ block → label → (list register).
    96 
    97 
    98 definition preamble_length ≝
    99 λP_in : sem_graph_params.λP_out : sem_graph_params.λprog : joint_program P_in.
    100 λstack_size : (ident → option ℕ).
    101 λinit : ∀globals.joint_closed_internal_function P_in globals
    102          →bound_b_graph_translate_data P_in P_out globals.
    103 λinit_regs : block → list register.
    104 λf_regs : regs_funct_type.λbl : block.λlbl : label.
    105 ! bl ← code_block_of_block bl ;
    106 ! 〈id,fn〉 ← res_to_opt … (fetch_internal_function …
    107                            (joint_globalenv P_in prog stack_size) bl);
    108 ! stmt ← stmt_at P_in … (joint_if_code … fn) lbl;
    109 ! data ← bind_instantiate ?? (init … fn) (init_regs bl);
    110 match stmt with
    111 [ sequential step nxt ⇒
    112     ! step_block ← bind_instantiate ?? (f_step … data lbl step) (f_regs bl lbl);
    113     return |\fst (\fst step_block)|
    114 | final fin ⇒
    115     ! fin_block ← bind_instantiate ?? (f_fin … data lbl fin) (f_regs bl lbl);
    116     return |\fst fin_block|
    117 | FCOND abs _ _ _ ⇒ Ⓧabs
    118 ].
    119 
    120 
    121 definition sigma_label : ∀p_in,p_out : sem_graph_params.
    122 joint_program p_in → (ident → option ℕ) →
    123 (∀globals.joint_closed_internal_function p_in globals
    124          →bound_b_graph_translate_data p_in p_out globals) →
    125 (block → list register) → lbl_funct_type → regs_funct_type →
    126 block → label → option label ≝
    127 λp_in,p_out,prog,stack_size,init,init_regs,f_lbls,f_regs,bl,searched.
    128 ! bl ← code_block_of_block bl ;
    129 ! 〈id,fn〉 ← res_to_opt … (fetch_internal_function …
    130                            (joint_globalenv p_in prog stack_size) bl);
    131 ! 〈res,s〉 ←
    132  find ?? (joint_if_code ?? fn)
    133   (λlbl.λ_.match preamble_length … prog stack_size init init_regs f_regs bl lbl with
    134              [ None ⇒ false
    135              | Some n ⇒ match nth_opt ? n (lbl::(f_lbls bl lbl)) with
    136                          [ None ⇒ false
    137                          | Some x ⇒ eq_identifier … searched x
    138                          ]
    139              ]);
    140 return res.
    141 
    142                                          
    143                          
    144 
    145 lemma partial_inj_sigma_label :
    146 ∀p_in,p_out,prog,stack_size,init,init_regs.
    147 ∀f_lbls : lbl_funct_type.∀f_regs,bl,lbl1,lbl2.
    148 sigma_label p_in p_out prog stack_size init init_regs f_lbls f_regs bl lbl1 ≠ None ?→
    149 sigma_label p_in p_out prog stack_size init init_regs f_lbls f_regs bl lbl1 =
    150 sigma_label p_in p_out prog stack_size init init_regs f_lbls f_regs bl lbl2 →
    151 lbl1 = lbl2.
    152 #p_in #p_out #prog #stack_size #init #init_regs #f_lbls #f_regs #bl #lbl1 #lbl2
    153 inversion(sigma_label ????????? lbl1)
    154 [ #_ * #H @⊥ @H %]
    155 #lbl1' #H @('bind_inversion H) -H #bl' #EQbl'
    156 #H @('bind_inversion H) -H * #f #fn #H lapply(res_eq_from_opt ??? H) -H
    157 #EQfn #H @('bind_inversion H) -H * #res #stmt #H1 whd in ⊢ (??%? → ?);
    158 #EQ destruct(EQ) #_ #H lapply(sym_eq ??? H) -H #H @('bind_inversion H) -H
    159 #bl'' >EQbl' #EQ destruct(EQ) >EQfn >m_return_bind #H @('bind_inversion H) -H
    160 * #lbl2' #stmt' #H2 whd in ⊢ (??%? → ?); #EQ destruct(EQ)
    161 lapply(find_predicate ?????? H1) lapply(find_predicate ?????? H2)
    162 cases (preamble_length ?????????) normalize nodelta [*] #n cases(nth_opt ???)
    163 normalize nodelta
    164 [*] #lbl @eq_identifier_elim [2: #_ *] #EQ destruct(EQ) #_ @eq_identifier_elim
    165 [2: #_ *] #EQ destruct(EQ) #_ %
    166 qed.
    167 
    168 definition sigma_pc_opt : 
    169 ∀p_in,p_out : sem_graph_params.
    170 joint_program p_in → (ident → option ℕ) →
    171 (∀globals.joint_closed_internal_function p_in globals
    172          →bound_b_graph_translate_data p_in p_out globals) →
    173 (block → list register) → lbl_funct_type → regs_funct_type →
    174 program_counter → option program_counter ≝
    175 λp_in,p_out,prog,stack_size,init,init_regs,f_lbls,f_regs,pc.
    176 let target_point ≝ point_of_pc p_out pc in
    177 if eqZb (block_id (pc_block pc)) (-1) then
    178  return pc
    179 else
    180  ! source_point ← sigma_label p_in p_out prog stack_size init init_regs
    181                    f_lbls f_regs (pc_block pc) target_point;
    182  return pc_of_point p_in (pc_block pc) source_point.
    183 
    184 lemma sigma_stored_pc_inj :
    185 ∀p_in,p_out,prog,stack_size,init,init_regs,f_lbls,f_regs,pc,pc'.
    186 sigma_pc_opt p_in p_out prog stack_size init init_regs f_lbls f_regs pc ≠ None ? →
    187 sigma_pc_opt p_in p_out prog stack_size init init_regs f_lbls f_regs pc =
    188 sigma_pc_opt p_in p_out prog stack_size init init_regs f_lbls f_regs pc' →
    189 pc = pc'.
    190 #p_in #p_out #prog #stack_size #init #init_regs #f_lbls #f_regs
    191 * #bl1 #p1 * #bl2 #p2
    192 inversion(sigma_pc_opt ??????) [#_ * #H @⊥ @H %] #pc1
    193 whd in match sigma_pc_opt in ⊢ (% → ?); normalize nodelta
    194 @eqZb_elim [2: *] normalize nodelta #Hbl
    195 [ #H @('bind_inversion H) -H * #pt1 #EQpt1]
    196 whd in ⊢ (??%? → ?); #EQ destruct(EQ)
    197 #_ #H lapply(sym_eq ??? H) -H whd in match sigma_pc_opt;
    198 normalize nodelta @eqZb_elim [2,4: *] #Hbl1 normalize nodelta
    199 [1,2: #H @('bind_inversion H) -H * #pt2 #EQpt2] whd in match pc_of_point;
    200 normalize nodelta whd in match (offset_of_point ??);
    201 whd in ⊢ (??%% → ?); #EQ destruct(EQ)
    202 [2,3: @⊥ [ >Hbl in Hbl1; | >Hbl1 in Hbl;] #H @H % |4: %]
    203 whd in match (offset_of_point ??) in EQpt2;
    204 <EQpt1 in EQpt2; #H lapply(partial_inj_sigma_label … (sym_eq ??? H))
    205 [ >EQpt1 % #EQ -prog destruct(EQ)] whd in match point_of_pc; normalize nodelta
    206 whd in match (point_of_offset ??); whd in match (point_of_offset ??);
    207 #EQ -prog destruct(EQ) %
    208 qed.
    209 
    210 lemma match_reg_elim : ∀ A : Type[0]. ∀ P : A → Prop. ∀ r : region.
    211 ∀f : (r = XData) → A. ∀g : (r = Code) → A. (∀ prf : r = XData.P (f prf)) →
    212 (∀ prf : r = Code.P (g prf)) →
    213 P ((match r return λx.(r = x → ?) with
    214     [XData ⇒ f | Code ⇒ g])(refl ? r)).
    215 #A #P * #f #g #H1 #H2 normalize nodelta [ @H1 | @H2]
    216 qed.
    217 
    218 definition sigma_stored_pc ≝
    219 λp_in,p_out,prog,stack_size,init,init_regs,f_lbls,f_regs,pc.
    220 match sigma_pc_opt p_in p_out prog stack_size init init_regs f_lbls f_regs pc with
    221       [None ⇒ null_pc (pc_offset … pc) | Some x ⇒ x].
    222      
    223 lemma code_block_of_block_eq : ∀bl : Σb.block_region b = Code.
    224 code_block_of_block bl = return bl.
    225 * #bl #prf whd in match code_block_of_block; normalize nodelta @match_reg_elim
    226 [ >prf in ⊢ (% → ?); #ABS destruct(ABS)] #prf1 %
    227 qed.
    228 
    229 (*TO BE MOVED*)
    230 lemma Exists_append1 : ∀A.∀l1,l2 : list A.∀P.Exists A P l1 → Exists A P (l1@l2).
    231 #A #l1 elim l1 [#l2 #P *] #hd #tl #IH *
    232 [#P normalize // ] #hd1 #tl1 #P normalize * [#H % assumption | #H %2 @IH assumption]
    233 qed.
    234 
    235 lemma Exists_append2 : ∀A.∀l1,l2 : list A.∀P.Exists A P l2 → Exists A P (l1@l2).
    236 #A #l1 #l2 lapply l1 -l1 elim l2 [#l1 #a *] #hd #tl #IH *
    237 [#a normalize // ] #hd1 #tl1 #a normalize *
    238 [ #H %2 >append_cons @Exists_append1 elim tl1 [% assumption] #hd2 #tl2 #H1 normalize %2 //
    239 | #H %2 >append_cons @IH assumption]
    240 qed.
    241 
    242 lemma seq_list_in_code_length : ∀p : params. ∀globals : list ident.
    243 ∀code : codeT p globals.∀src : code_point p.∀l1,l2,dst.
    244 seq_list_in_code p globals code src l1 l2 dst → |l1| = |l2|.
    245 #p #globals #code #src #l1 lapply src -src elim l1
    246 [ #src * [ #dst #_ %] #hd #tl #dst whd in ⊢ (% → ?); * #EQ destruct]
    247 #hd #tl #IH #src * [ #dst whd in ⊢ (% → ?); * #mid * #rest ** #EQ destruct]
    248 #hd1 #tl1 #dst whd in ⊢ (% → ?); * #mid * #rest ** #EQ destruct * #nxt1 * #EQstnt
    249 #EQsucc #H whd in ⊢ (??%%); @eq_f @(IH … H)
    250 qed.
    251 
    252 lemma fetch_stmt_ok_succ_ok : ∀p : sem_graph_params.
    253 ∀prog : joint_program p.∀stack_size,f,fn,stmt,pc,pc',lbl.
    254 In ? (stmt_labels p ? stmt) lbl→
    255 fetch_statement p … (joint_globalenv p prog stack_size) pc = return 〈f,fn,stmt〉 →
    256 pc' = pc_of_point p (pc_block pc) lbl →
    257 ∃stmt'.fetch_statement p … (joint_globalenv p prog stack_size) pc' = return 〈f,fn,stmt'〉.
    258 #p #prog #stack_size #f #fn #stmt #pc #pc' #lbl #Hlbl #EQfetch
    259 cases(fetch_statement_inv … EQfetch) #EQfn normalize nodelta #EQstmt
    260 #EQ destruct(EQ) lapply(code_is_closed … (pi2 ?? fn) … EQstmt) *
    261 cases(decidable_In ? (stmt_explicit_labels … stmt) lbl ?)
    262 [3: * cases lbl #x #y cases(decidable_eq_pos … x y)
    263     [#EQ destruct % % | * #H %2 % #H1 @H destruct %]
    264 | whd in ⊢ (% → ?); #H1 #H2 cases(Exists_All … H1 H2) #lbl1 * #EQ destruct
    265   whd in match code_has_label; whd in match code_has_point; normalize nodelta
    266   inversion(stmt_at ????) [#_ *] #stmt' #EQstmt' #_ #_ %{stmt'}
    267   whd in match fetch_statement; normalize nodelta >EQfn >m_return_bind
    268   >point_of_pc_of_point >EQstmt' %
    269 | #H lapply(In_all ??? H) -H cases(Exists_append … Hlbl)
    270   [ cases stmt [ #step #nxt | #fin | *] whd in match stmt_implicit_label;
    271     normalize nodelta [2: *] * [2: *] #EQ destruct(EQ) #_ #_
    272     whd in match stmt_forall_succ; whd in match code_has_point; normalize nodelta
    273     inversion(stmt_at ????) [#_ *] #stmt' #EQstmt' #_ %{stmt'}
    274     whd in match fetch_statement; normalize nodelta >EQfn >m_return_bind
    275     >point_of_pc_of_point >EQstmt' %
    276   | #H1 #H2 cases(Exists_All … H1 H2) #x * #EQ destruct * #H @⊥ @H %
    277   ]
    278 ]
    279 qed.
    280 
    281 
    282 lemma fetch_stmt_ok_nxt_ok : ∀p : sem_graph_params.
    283 ∀prog : joint_program p.∀stack_size,f,fn,stmt,bl,pt,nxt.
    284 fetch_internal_function … (joint_globalenv p prog stack_size) bl =
    285 return 〈f,fn〉→
    286 stmt_at p … (joint_if_code … fn) pt = return sequential p ? stmt nxt →
    287 ∃stmt'.
    288 stmt_at p … (joint_if_code … fn) nxt = return stmt'.
    289 #p #prog #stack_size #f #fn #stmt #bl #pt #nxt #EQfn #EQstmt
    290 cases(fetch_stmt_ok_succ_ok …
    291        prog stack_size f fn (sequential p … stmt nxt) (pc_of_point p bl pt)
    292        (pc_of_point p bl nxt) nxt ???)
    293 [ #stmt' #H cases(fetch_statement_inv … H) -H #_ >point_of_pc_of_point normalize nodelta
    294   #EQstmt' %{stmt'} assumption
    295 | whd in match stmt_labels; normalize nodelta % %
    296 | whd in match fetch_statement; normalize nodelta >EQfn >m_return_bind
    297   >point_of_pc_of_point >EQstmt %
    298 | %
    299 ]
    300 qed.
    301 
    302 
    303 lemma sigma_label_spec : ∀p_in,p_out,prog,stack_size,init,init_regs.
    304 ∀f_lbls : lbl_funct_type.∀f_regs.
    305 b_graph_transform_program_props p_in p_out stack_size init prog init_regs f_lbls f_regs →
    306 ∀id,fn.
    307 ∀bl:Σb.block_region b = Code. ∀pt,stmt.
    308 block_id … bl ≠ -1 →
    309 fetch_internal_function …
    310    (joint_globalenv p_in prog stack_size) bl = return 〈id,fn〉 →
    311 stmt_at p_in … (joint_if_code … fn) pt = return stmt → 
    312 ∃n.preamble_length … prog stack_size init init_regs f_regs bl pt = return n ∧
    313 match n with
    314 [ O ⇒ sigma_label p_in p_out prog stack_size init init_regs f_lbls f_regs bl pt = return pt
    315 | S m ⇒ ∃lbl.nth_opt ? m (f_lbls bl pt) = return lbl ∧
    316     sigma_label p_in p_out prog stack_size init init_regs f_lbls f_regs bl lbl = return pt     
    317 ].
    318 #p_in #p_out #prog #stack_size #init #init_regs #f_lbls #f_regs #good #id #fn
    319 #bl #pt #stmt * #Hbl #EQfn #EQstmt   
    320 lapply(b_graph_transform_program_fetch_internal_function … good … bl id fn)
    321 @eqZb_elim [ #EQ >EQ in Hbl; #H @⊥ @H %] #_ normalize nodelta #H cases(H EQfn) -H
    322 #data * #t_fn ** #EQt_fn #Hinit * #_ #_ #_ #pp_labs #_ #fresh_lab #_ #_ #_ #H
    323 lapply(H … EQstmt) -H normalize nodelta cases stmt in EQstmt; -stmt
    324 [ #j_step #nxt | #fin | * ] #EQstmt normalize nodelta **
    325 [ * #pre_instr #instr #post_instr | #pre_instr #instr] *
    326 [ cases(added_prologue ????) [2: #hd_instr #tl_instrs ] normalize nodelta
    327  [ @eq_identifier_elim #EQentry normalize nodelta
    328    [ whd in ⊢ (% → ?); inversion (f_regs ??) [2: #x #y #_ #_ *] #EQregs normalize nodelta
    329      whd in ⊢ (???% → ?); #EQ destruct(EQ)
    330    |*: #Hregs
    331    ]
    332  | #Hregs
    333  ]
    334 | #Hregs
    335 ]
    336 #syntax_spec
    337 [4: cases(added_prologue ????) [2: #hd_instr #tl_instrs ] normalize nodelta ] #_
    338 [1,2,4,5: %{(|pre_instr|)} | %{O}]
    339 cut(? : Prop)
    340 [3,6,9,12,15: #EQn %{EQn} whd in EQn; normalize nodelta
    341  [1,2,3,4: cases pre_instr in Hregs syntax_spec EQn; [2,4,6,8: #hd #tl] #Hregs #syntax_spec
    342            whd in match (length ??); #EQn whd in match (length ??); normalize nodelta]
    343  [5,6,7,8,9: whd in match sigma_label; normalize nodelta >code_block_of_block_eq
    344      >m_return_bind >EQfn >m_return_bind inversion(find ????)
    345      [1,3,5,7,9: #EQfind @⊥ lapply(find_none ?????? EQfind EQstmt) >EQn normalize nodelta
    346      @eq_identifier_elim [1,3,5,7,9: #_ *] * #H #_ @H % ] * #lbl1 #stmt1 #EQfind
    347      >m_return_bind @eq_f lapply(find_predicate ?????? EQfind) whd in match preamble_length;
    348      normalize nodelta >code_block_of_block_eq >m_return_bind >EQfn >m_return_bind
    349      whd in match (stmt_at ????); >(find_lookup ?????? EQfind) >m_return_bind >Hinit
    350      >m_return_bind cases stmt1 in EQfind; -stmt1
    351      [1,4,7,10,13: #j_step1 #nxt1 |2,5,8,11,14: #fin1 |*: *] #EQfind normalize nodelta
    352      cases(bind_instantiate ????) [1,3,5,7,9,11,13,15,17,19: *]
    353      [1,2,3,4,5: ** #pre_instr1 #instr1 #post_instr1 |*: * #pre_instr1 #instr1 ]
    354      >m_return_bind cases pre_instr1 -pre_instr1 [2,4,6,8,10,12,14,16,18,20: #hd #tl]
    355      whd in match (length ??); normalize nodelta
    356      [11,12,13,14,15,16,17,18,19,20: @eq_identifier_elim [2,4,6,8,10,12,14,16,18,20: #_ *]
    357      #EQ #_ >EQ %]
    358      whd in match (nth_opt ???); inversion(nth_opt ???) [1,3,5,7,9,11,13,15,17,19: #_ *]
    359      #lbl2 #EQlbl2 normalize nodelta @eq_identifier_elim [2,4,6,8,10,12,14,16,18,20: #_ *]
    360      #EQ lapply EQlbl2 destruct(EQ) #EQlbl2 @⊥
    361      cases(Exists_All … (nth_opt_Exists … EQlbl2) (fresh_lab lbl1)) #x * #EQ destruct(EQ)
    362      ** #H #_ @H  @(code_is_in_universe … (pi2 ?? fn)) whd in match code_has_label;
    363      whd in match code_has_point; normalize nodelta >EQstmt @I
    364  |*: cases syntax_spec -syntax_spec #pre * #mid1 [3,4: * #mid2 * #post] ** [1,2: *]
    365      cases pre -pre [1,3,5,7: #_ * #x * #y ** #ABS destruct(ABS)] #hd1 #tl1 whd in ⊢ (??%% → ?);
    366      #EQ destruct(EQ) -EQ #pre_spec whd in ⊢ (% → ?);
    367      [1,2: * #nxt1 * #EQt_stmt change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) #post_spec
    368      |*:   #EQt_stmt
    369      ]
    370      %{mid1} cut(? : Prop)
    371      [3,6,9,12: #EQnth_opt %{EQnth_opt} whd in match sigma_label; normalize nodelta
    372        >code_block_of_block_eq >m_return_bind >EQfn >m_return_bind inversion(find ????)
    373        [1,3,5,7: #EQfind @⊥ lapply(find_none ?????? EQfind EQstmt) >EQn normalize nodelta
    374          whd in match (nth_opt ???); >EQnth_opt normalize nodelta @eq_identifier_elim
    375          [1,3,5,7: #_ *] * #H #_ @H % ] * #lbl1 #stmt1 #EQfind >m_return_bind @eq_f
    376        lapply(find_predicate ?????? EQfind) whd in match preamble_length;
    377        normalize nodelta >code_block_of_block_eq >m_return_bind >EQfn >m_return_bind
    378        whd in match (stmt_at ????); >(find_lookup ?????? EQfind) >m_return_bind >Hinit
    379        >m_return_bind cases stmt1 in EQfind; -stmt1
    380        [1,4,7,10: #j_step1 #nxt1 |2,5,8,11: #fin1 |*: *] #EQfind normalize nodelta
    381        cases(bind_instantiate ????) [1,3,5,7,9,11,13,15: *]
    382        [1,2,3,4: ** #pre_instr1 #instr1 #post_instr1 |*: * #pre_instr1 #instr1]
    383        >m_return_bind cases pre_instr1 -pre_instr1 [2,4,6,8,10,12,14,16: #hd1 #tl1]
    384        whd in match (length ??); normalize nodelta whd in match (nth_opt ???);
    385        [1,2,3,4,5,6,7,8: inversion(nth_opt ???) [1,3,5,7,9,11,13,15: #_ *] #lbl2
    386          #EQlbl2 normalize nodelta @eq_identifier_elim [2,4,6,8,10,12,14,16: #_ *]
    387          #EQ lapply EQlbl2 destruct(EQ) #EQlbl2 #_  @(proj2 … pp_labs ?? lbl2)
    388          @Exists_memb [1,3,5,7,9,11,13,15: @(nth_opt_Exists … EQlbl2)]
    389          >e0 @Exists_append2 % %
    390        |*: @eq_identifier_elim [2,4,6,8,10,12,14,16: #_ *] #EQ destruct(EQ) @⊥
    391          lapply(fresh_lab hd1) >e0 #H cases(append_All … H) #_ * -H ** #H #_ #_ @H
    392          @(code_is_in_universe … (pi2 ?? fn)) whd in match code_has_label;
    393          whd in match code_has_point; normalize nodelta whd in match (stmt_at ????);
    394          >(find_lookup ?????? EQfind) @I
    395        ]   
    396      |2,5,8,11: >e0 cases pre_spec #fst * #rest ** #EQ destruct(EQ)
    397                 whd in ⊢ (% → ?); * #nxt1 * #_ change with nxt1 in ⊢ (??%? → ?);
    398                 #EQ destruct(EQ) #H lapply(seq_list_in_code_length … H)
    399                 [1,2: >length_map] -H #H >H >nth_opt_append_r cases(|rest|)
    400                 try % try( #n %) #n <minus_n_n %
    401      |*:
    402      ]
    403   ]
    404  |2,5,8,11,14: whd in match preamble_length; normalize nodelta >code_block_of_block_eq
    405    >m_return_bind >EQfn >m_return_bind >EQstmt >m_return_bind >Hinit >m_return_bind
    406    normalize nodelta
    407    [1,2,3,4: >Hregs %
    408    | >EQregs <EQentry in EQstmt; cases(entry_is_cost … (pi2 ?? fn)) #succ * #c
    409      #EQstmt >EQstmt whd in ⊢ (???% → ?); #EQ destruct(EQ) >(f_step_on_cost … data)
    410      whd in match (bind_instantiate ????); %
    411    ]
    412  |*:
    413  ]
    414 qed.
    415 
    416 lemma pc_block_eq : ∀p_in,p_out,prog,stack_sizes,init,init_regs,f_lbls,
    417 f_regs,pc.
    418 sigma_pc_opt p_in p_out prog stack_sizes init
    419    init_regs f_lbls f_regs pc ≠ None ? →
    420  pc_block … pc =
    421  pc_block … (sigma_stored_pc p_in p_out prog stack_sizes init
    422                                            init_regs f_lbls f_regs pc).
    423 #p_in #p_out #prog #stack_sizes #init #init_regs #f_lbls #f_regs #pc
    424 whd in match sigma_stored_pc; normalize nodelta
    425 inversion(sigma_pc_opt ?????????) [ #_ * #ABS @⊥ @ABS %] #pc1
    426 whd in match sigma_pc_opt; normalize nodelta @eqZb_elim #_ normalize nodelta
    427 [ whd in ⊢ (??%? → ?); #EQ destruct #_ %] #H @('bind_inversion H) -H
    428 #lbl #_ whd in ⊢ (??%? → ?); #EQ destruct #_ %
    429 qed.
    430 
    431 definition stmt_get_next : ∀p,globals.joint_statement p globals → option (succ p) ≝
    432 λp,globals,stmt.
    433 match stmt with
    434 [sequential stmt nxt ⇒ Some ? nxt
    435 | _ ⇒ None ?
    436 ].
    437 
    438 
    439 definition sigma_next : ∀p_in,p_out : sem_graph_params.
    440 joint_program p_in → (ident → option ℕ) →
    441 (∀globals.joint_closed_internal_function p_in globals
    442          →bound_b_graph_translate_data p_in p_out globals) →
    443 (block → list register) → lbl_funct_type → regs_funct_type →
    444 block → label → option label ≝
    445 λp_in,p_out,prog,stack_size,init,init_regs,f_lbls,f_regs,bl,searched.
    446 ! bl ← code_block_of_block bl ;
    447 ! 〈id,fn〉 ← res_to_opt … (fetch_internal_function …
    448                            (joint_globalenv p_in prog stack_size) bl);
    449 ! 〈res,s〉 ←
    450  find ?? (joint_if_code ?? fn)
    451   (λlbl.λstmt.match stmt_get_next … stmt with
    452     [ None ⇒ false
    453     | Some nxt ⇒
    454        match preamble_length … prog stack_size init init_regs f_regs bl lbl with
    455         [ None ⇒ false
    456         | Some n ⇒ match nth_opt ? n ((f_lbls bl lbl) @ [nxt]) with
    457                          [ None ⇒ false
    458                          | Some x ⇒ eq_identifier … searched x
    459                          ]
    460         ]
    461     ]);
    462 stmt_get_next … s.
    463 
    464 lemma fetch_statement_sigma_stored_pc :
    465 ∀p_in,p_out,prog,stack_sizes,
    466 init,init_regs,f_lbls,f_regs,pc,f,fn,stmt.
    467 b_graph_transform_program_props p_in p_out stack_sizes
    468   init prog init_regs f_lbls f_regs →
    469 block_id … (pc_block pc) ≠ -1 →
    470 let trans_prog ≝ b_graph_transform_program p_in p_out init prog in
    471 fetch_statement p_in … (joint_globalenv p_in prog stack_sizes) pc =
    472 return 〈f,fn,stmt〉 →
    473 ∃data.bind_instantiate ?? (init … fn) (init_regs (pc_block pc)) = return data ∧
    474 match stmt with
    475 [ sequential step nxt ⇒
    476     ∃step_block : step_block p_out (prog_names … trans_prog).
    477     bind_instantiate ?? (f_step … data (point_of_pc p_in pc) step)
    478                  (f_regs (pc_block pc) (point_of_pc p_in pc)) = return step_block ∧
    479     ∃pc'.sigma_stored_pc p_in p_out prog stack_sizes init
    480                                            init_regs f_lbls f_regs pc' = pc ∧
    481     ∃fn',nxt',l1,l2.
    482     fetch_statement p_out … (joint_globalenv p_out trans_prog stack_sizes) pc' =
    483     if not_emptyb … (added_prologue … data) ∧
    484        eq_identifier … (point_of_pc p_in pc) (joint_if_entry … fn)
    485     then OK ? 〈f,fn',sequential ?? (NOOP …) nxt'〉
    486     else OK ? 〈f,fn',sequential ?? ((\snd(\fst step_block)) (point_of_pc p_in pc')) nxt'〉 ∧
    487     seq_list_in_code p_out (prog_names … trans_prog) (joint_if_code … fn') (point_of_pc p_out pc)
    488      (map_eval … (\fst (\fst step_block)) (point_of_pc p_out pc'))
    489      l1 (point_of_pc p_out pc')
    490     ∧ seq_list_in_code p_out ? (joint_if_code … fn') nxt' (\snd step_block) l2 nxt
    491     ∧ sigma_next p_in p_out prog stack_sizes init init_regs f_lbls f_regs (pc_block pc) nxt' = return nxt
    492 | final fin ⇒
    493     ∃fin_block.bind_instantiate ?? (f_fin … data (point_of_pc p_in pc) fin)
    494                   (f_regs (pc_block pc) (point_of_pc p_in pc)) = return fin_block ∧
    495     ∃pc'.sigma_stored_pc p_in p_out prog stack_sizes init
    496                                            init_regs f_lbls f_regs pc' = pc ∧
    497     ∃fn'.fetch_statement p_out …
    498        (joint_globalenv p_out trans_prog stack_sizes) pc'
    499        = return 〈f,fn',final ?? (\snd fin_block)〉           
    500 | FCOND abs _ _ _ ⇒ Ⓧabs
    501 ].
    502 #p_in #p_out #prog #stack_sizes #init #init_regs #f_lbls #f_regs #pc #f #fn #stmt
    503 #good #Hbl #EQfetch cases(fetch_statement_inv … EQfetch) #EQfn normalize nodelta
    504 #EQstmt
    505 lapply(b_graph_transform_program_fetch_internal_function … good … (pc_block pc) f fn)
    506 @eqZb_elim [ #EQ >EQ in Hbl; * #H @⊥ @H %] #_ normalize nodelta #H cases(H EQfn) -H
    507 #data * #t_fn ** #EQt_fn #Hinit * #_ #_ #_ #pp_labs #_ #fresh_labs #_ #_ #_ #H
    508 lapply(H … EQstmt) -H normalize nodelta #H #_ %{data} >Hinit %{(refl …)}
    509 -EQfetch cases stmt in EQstmt H;
    510 [ #step #nxt | #fin | *] normalize nodelta #EQstmt -stmt
    511 [ cases(added_prologue ??? data) [2: #hd #tl] normalize nodelta
    512   [ @eq_identifier_elim #EQentry normalize nodelta ] ]
    513 * #block *
    514 [ whd in ⊢ (% → ?); inversion(f_regs ??) [2: #x #y #_ #_ *] #EQregs normalize nodelta
    515   #EQ destruct(EQ) whd in ⊢ (% → ?); * #pre * #mid1 * #mid2 * #post *** #EQmid1
    516   whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in ⊢ (% → ?); * #nxt1
    517   * #EQt_stmt change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ⊢ (% → ?);
    518   * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in EQmid1 : (??%%); destruct(EQmid1)
    519 |*: #Hregs #syntax_spec
    520 ]
    521 [ whd in match (point_of_pc ??) in EQstmt EQentry; <EQentry in EQstmt;
    522   cases(entry_is_cost … (pi2 ?? fn)) #nxt1 * #c #EQstmt >EQstmt #EQ destruct(EQ)
    523   % [2: % [ >(f_step_on_cost … data) in ⊢ (??%?); % ] |] %{pc}
    524   whd in match sigma_stored_pc; whd in match sigma_pc_opt; normalize nodelta
    525   @eqZb_elim normalize nodelta [#ABS >ABS in Hbl; * #H @⊥ @H %] #_
    526 |*: %{block} >Hregs %{(refl …)}
    527 ]
    528 cases(sigma_label_spec … good … Hbl EQfn EQstmt) * [2,4,6,8: #n ] * #EQpreamble
    529 normalize nodelta [1,2,3,4: * #lbl * #EQnth_opt] #EQsigma_lab
    530 [   whd in match (point_of_pc ??) in e0; <EQentry in e0; #e0 >e0 in EQnth_opt;
    531     whd in ⊢ (??%% → ?); #EQ destruct(EQ)
    532 |5: whd in match (point_of_pc ??); <EQentry >EQsigma_lab >m_return_bind
    533     normalize nodelta >EQentry % [ cases pc #bl #off %] %{t_fn} %{nxt} %{[ ]} %{[ ]}
    534     whd in match fetch_statement; normalize nodelta >EQt_fn >m_return_bind
    535     >EQt_stmt >m_return_bind %
    536     [ % [ % [ @eq_identifier_elim [#_ %] * #H @⊥ @H % | %{(refl …) (refl …)}] | %{(refl …) (refl …)}]]
    537     whd in match sigma_next; normalize nodelta >code_block_of_block_eq
    538     >m_return_bind >EQfn >m_return_bind inversion(find ????)
    539     [ #EQfind @⊥ lapply(find_none … EQfind EQstmt) normalize nodelta
    540     >EQpreamble normalize  nodelta >EQentry >e0 normalize nodelta
    541     @eq_identifier_elim [#_ *] * #H #_ @H %]
    542     * #lbl1 #stmt1 #EQfind >m_return_bind lapply(find_predicate ?????? EQfind)
    543     inversion(stmt_get_next … stmt1) [#_ *] #nxt1 #EQnxt1 normalize nodelta
    544     inversion(preamble_length ?????????) [#_ *] #m whd in match preamble_length;
    545     normalize nodelta >code_block_of_block_eq >m_return_bind >EQfn >m_return_bind
    546     whd in match (stmt_at ????); >(find_lookup ?????? EQfind) >m_return_bind
    547     >Hinit >m_return_bind cases stmt1 in EQfind; [#j_step #succ | #fin | *]
    548     #EQfind normalize nodelta cases(bind_instantiate ???)
    549     [1,3: whd in ⊢ (??%% → ?); #EQ destruct] #bl1 >m_return_bind whd in ⊢ (??%? → ?);
    550     #EQ destruct(EQ) inversion(nth_opt ???) [1,3: #_ *] #lbl2 #EQlbl2 normalize nodelta
    551     @eq_identifier_elim [2,4: #_ *] #EQ lapply EQlbl2 destruct(EQ) #EQlbl2
    552     cases(Exists_append … (nth_opt_Exists ???? EQlbl2)) [2,4: * [2,4: *] #EQ >EQ #_ %]
    553     #H @⊥ cases(Exists_All … H (fresh_labs lbl1)) #x * #EQ destruct(EQ) ** -H #H #_
    554     @H @(code_is_in_universe … (pi2 ?? fn)) whd in match code_has_label;
    555     whd in match code_has_point; normalize nodelta
    556     cases(fetch_stmt_ok_nxt_ok … EQfn EQstmt) #stmt2 #EQ >EQ @I
    557 |2,3,4: %{(pc_of_point p_out (pc_block pc) lbl)}
    558 |6,7,8: %{pc}
    559 ]
    560 whd in match sigma_stored_pc; whd in match sigma_pc_opt; normalize nodelta
    561 @eqZb_elim [1,3,5,7,9,11: #H >H in Hbl; * #H1 @⊥ @H1 %] #_ normalize nodelta
    562 [1,2,3: >point_of_pc_of_point] >EQsigma_lab >m_return_bind >(pc_of_point_of_pc … pc)
    563 %{(refl …)} %{t_fn} cases block in Hregs syntax_spec; -block
    564 [1,2,4,5: * #pre #instr #post |*: #pre #instr ] #Hregs *
    565 [1,2,3,4: #l1 * #mid1 * #mid2 * #l2 ***
    566 |*: #l1 * #mid **
    567 ]
    568 #EQmid #EQpre whd in ⊢ (% → ?);
    569 [1,2,3,4: * #nxt1 *] #EQt_stmt
    570 [1,2,3,4: change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) #EQpost %{mid2} %{l1} %{l2} %]
    571 [1,3,5,7,9,10: whd in match fetch_statement; normalize nodelta >EQt_fn >m_return_bind
    572  @('bind_inversion EQpreamble) #bl1 >code_block_of_block_eq whd in ⊢ (??%? → ?);
    573  #EQ destruct(EQ) >EQfn >m_return_bind >EQstmt >m_return_bind >Hinit >m_return_bind
    574  normalize nodelta >Hregs >m_return_bind cases pre in Hregs EQpre; -pre
    575  [1,3,6,8,9,12: [3,4,6: #x #y] #_ #_ whd in match (length ??); whd in ⊢ (??%? → ?);
    576     #EQ destruct(EQ)]
    577  [1,2,5: #hd1 #tl1 ] #Hregs cases l1 in EQmid;
    578  [1,3,5,8,10,12: [4,5,6: #x #y] #_ whd in ⊢ (% → ?); [1,2,3: * #EQ1 #EQ2 destruct]
    579     * #mid * #rest ** #EQ destruct(EQ)]
    580  [1,2,3: #hd2 #tl2] whd in ⊢ (??%% → ?); #EQ destruct(EQ) whd in ⊢ (% → ?);
    581  [4,5,6: * #_ #EQ #_ >EQ >EQt_stmt [2,3: % [ %{(refl …)} %{(refl …) (refl …)} ] assumption]
    582    @eq_identifier_elim [2: #_ % [ %{(refl …)} %{(refl …) (refl …)} | assumption] ]
    583    #EQ <EQ in EQentry; * #H @⊥ @H %]
    584  * #mid' * #rest ** #EQ1 destruct(EQ1) #H1 #H2 whd in match (length ??);
    585  whd in ⊢ (??%? → ?); #EQ1 destruct(EQ1) >e0 in EQnth_opt;
    586  lapply(seq_list_in_code_length … H2) [1,2: >length_map] #EQ1 >EQ1
    587  >nth_opt_append_r [2,4,6: %] cut(|rest|-|rest|=O) [1,3,5: cases(|rest|) //]
    588  #EQ2 >EQ2 whd in ⊢ (??%% → ?); #EQ3 -EQ2 -EQ1
    589  [1,2: destruct(EQ3) >point_of_pc_of_point >EQt_stmt
    590     [2: >point_of_pc_of_point % [%{(refl …)} whd %{mid'} %{rest} % [2: assumption] % [2: assumption] %]
    591        assumption]
    592     @eq_identifier_elim [#EQ4 <EQ4 in EQentry; * #H3 @⊥ @H3 %] #_ >point_of_pc_of_point %
    593     [ %{(refl …)} whd %{mid'} %{rest} % [ %{(refl …)} assumption ] assumption | assumption ] ]
    594  destruct(EQ3) >point_of_pc_of_point >EQt_stmt %]
    595 whd in match sigma_next; normalize nodelta >code_block_of_block_eq >m_return_bind
    596 >EQfn >m_return_bind inversion(find ????)
    597 [1,3,5,7: #EQfind @⊥ lapply(find_none … EQfind EQstmt) normalize nodelta >EQpreamble
    598   normalize nodelta cases post in Hregs EQpost;
    599   [1,3,5,7: #Hregs * #EQ1 #EQ2 destruct(EQ1 EQ2) @('bind_inversion EQpreamble)
    600     #bl' >code_block_of_block_eq whd in ⊢ (??%? → ?); #EQ destruct(EQ) >EQfn
    601     >m_return_bind >EQstmt >m_return_bind >Hinit >m_return_bind normalize nodelta
    602     >Hregs >m_return_bind cases pre in EQpre Hregs;
    603     [1,3,6,8: [3,4: #x #y] #_ #_ whd in match (length ??); whd in ⊢ (??%? → ?); #EQ destruct
    604     |2,4: #fst #remaining] *
    605     [1,2: #lab1 * #rest ** #EQ destruct(EQ) * #nxt' * #EQpc change with nxt' in ⊢ (??%? → ?);
    606       #EQ destruct(EQ) #Hrest #Hregs whd in match (length ??); whd in ⊢ (??%? → ?);
    607       #EQ destruct(EQ) whd in EQmid : (??%%); destruct(EQmid) >e0
    608       lapply(seq_list_in_code_length … Hrest) >length_map #EQ >EQ
    609       >nth_opt_append_r
    610       [2,4: >length_append whd in match (length ? [mid1]);
    611              whd in match (length ? [ ]); cases(|rest|) //]
    612       >length_append whd in match (length ? [mid1]); whd in match (length ? [ ]);
    613       cut(S (|rest|) - (|rest| + 1) = O)
    614       [1,3: cases(|rest|) // #m normalize cases m // #m1 normalize nodelta
    615             cut(m1 + 1 = S m1) [1,3: //] #EQ1 >EQ1 <minus_n_n % ]
    616       #EQ1 >EQ1 normalize nodelta @eq_identifier_elim [1,3: #_ *] * #H #_ @H %
    617     |*: #EQ1 #EQ2 destruct(EQ1 EQ2) #EQregs #_ whd in EQmid : (??%%); destruct(EQmid)
    618         >e0 normalize nodelta @eq_identifier_elim [1,3: #_ *] * #H #_ @H %
    619     ]
    620   |*: #fst #rems #Hregs * #lab1 * #rest ** #EQ destruct(EQ) * #nxt1 * #EQmid2
    621       change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) #EQrest @('bind_inversion EQpreamble)
    622     #bl' >code_block_of_block_eq whd in ⊢ (??%? → ?); #EQ destruct(EQ) >EQfn
    623       >m_return_bind >EQstmt >m_return_bind >Hinit >m_return_bind normalize nodelta
    624       >Hregs >m_return_bind cases pre in EQpre Hregs;
    625       [1,3,6,8: [3,4: #x #y] #_ #_ whd in ⊢ (??%? → ?); whd in match (length ??);
    626         #EQ destruct|2,4: #hd1 #tl1] *
    627       [1,2: #lab1 * #rest1 ** #EQ destruct(EQ) * #nxt1 * #EQpc
    628         change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) #EQrest1 #Hregs
    629         whd in match (length ??); whd in ⊢ (??%? → ?); #EQ destruct(EQ)
    630       |*: #EQ1 #EQ2 destruct(EQ1 EQ2) #Hregs #_
    631       ]
    632       whd in EQmid : (??%%); destruct(EQmid) >e0 normalize nodelta
    633       [3,4: @eq_identifier_elim [1,3: #_ *] * #H #_ @H %]
    634       lapply(seq_list_in_code_length … EQrest1) >length_map #EQ >EQ
    635       >nth_opt_append_l [2,4: >length_append whd in match (length ? (mid1::?));
    636       whd in match (length ? (mid2::rest)); cases(|rest1|) //] >append_cons
    637       >append_cons >nth_opt_append_l
    638       [2,4: >length_append >length_append whd in match (length ? [ ? ]);
    639             whd in match (length ? [ ]); cases(|rest1|) // ]
    640       >nth_opt_append_r
    641       [2,4: >length_append whd in match (length ? [ ? ]); whd in match (length ? [ ]);
    642             cases(|rest1|) // ]
    643       >length_append whd in match (length ? [ ? ]); whd in match (length ? [ ]);
    644       cut(S(|rest1|) - (|rest1|+1) = 0)
    645       [1,3: cases(|rest1|) // #m normalize cases m // #m1 normalize nodelta
    646             cut(m1 + 1 = S m1) [1,3: //] #EQ1 >EQ1 <minus_n_n % ] #EQ1 >EQ1
    647       normalize nodelta @eq_identifier_elim [1,3: #_ *] * #H #_ @H %
    648   ]
    649 |*: * #lab2 * [1,4,7,10: #j_step #nxt1 |2,5,8,11: #fin1 |*: *] #EQfind
    650     lapply(find_predicate ?????? EQfind) normalize nodelta [5,6,7,8: *]
    651     cases(preamble_length ?????????) normalize nodelta [1,3,5,7: *] #n
    652     inversion(nth_opt ???) normalize nodelta [1,3,5,7: #_ *] #lab1 #EQlab1
    653     @eq_identifier_elim [2,4,6,8: #_ *] #EQ destruct(EQ)
    654     cases(Exists_append … (nth_opt_Exists ???? EQlab1))
    655     [2,4,6,8: * [2,4,6,8: *] #EQ destruct(EQ) cases post in Hregs EQpost;
    656       [1,3,5,7: #Hregs * #EQ1 #EQ2 destruct(EQ1 EQ2) #_ %] #hd1 #tl1 #Hregs *
    657       #lab3 * #rest3 ** #EQ destruct(EQ) * #nxt2 * #EQt_lab1
    658       change with nxt2 in ⊢ (??%? → ?); #EQ destruct(EQ) #EQrest3
    659       @('bind_inversion EQpreamble) #bl' >code_block_of_block_eq
    660       whd in ⊢ (??%? → ?); #EQ destruct(EQ) >EQfn >m_return_bind >EQstmt
    661       >m_return_bind >Hinit >m_return_bind normalize nodelta >Hregs
    662       >m_return_bind cases pre in Hregs EQpre;
    663       [1,3,6,8: [3,4: #x #y] #_ #_ whd in match (length ??); whd in ⊢ (??%? → ?);
    664         #EQ destruct(EQ) |2,4: #hd1 #tl1] #Hregs *
    665       [1,2: #lab4 * #rest4 ** #EQ destruct(EQ) * #nxt2 * #EQpc
    666         change with nxt2 in ⊢ (??%? → ?); #EQ destruct(EQ) #EQrest4
    667         whd in match (length ??); whd in ⊢ (??%? → ?); #EQ destruct(EQ) #_
    668       |*: #EQ1 #EQ2 destruct(EQ1 EQ2) #_ #_
    669       ]
    670       whd in EQmid : (??%%); destruct(EQmid) @⊥ lapply(fresh_labs (point_of_pc p_in pc))
    671       >e0
    672       [1,2: #H cases(append_All … H) #_ * #_ *** -H #H #_ #_ @H
    673       |*: *** #H #_ #_ @H
    674       ]
    675       @(code_is_in_universe … (pi2 ?? fn)) whd in match code_has_label;
    676       whd in match code_has_point; normalize nodelta
    677       cases(fetch_stmt_ok_nxt_ok … EQfn (find_lookup ?????? EQfind))
    678       #stmt' #EQstmt' >EQstmt' @I
    679     |*: #Hlab2 cases post in Hregs EQpost;
    680         [1,3,5,7: #Hregs * #EQ1 #EQ2 destruct(EQ1 EQ2)
    681           cases(Exists_All … Hlab2 (fresh_labs lab2)) #x * #EQ destruct(EQ) ** #H
    682           @⊥ @H @(code_is_in_universe … (pi2 ?? fn)) whd in match code_has_label;
    683           whd in match code_has_point; normalize nodelta
    684           cases(fetch_stmt_ok_nxt_ok … EQfn EQstmt) #stmt' #EQstmt' >EQstmt' @I
    685         |*: #hd1 #tl1 #Hregs * #lab3 * #rest3 ** #EQ destruct(EQ) * #nxt2 *
    686           #EQt_lab1 change with nxt2 in ⊢ (??%? → ?); #EQ destruct(EQ) #EQrest3
    687           @('bind_inversion EQpreamble) #bl' >code_block_of_block_eq
    688           whd in ⊢ (??%? → ?); #EQ destruct(EQ) >EQfn >m_return_bind >EQstmt
    689           >m_return_bind >Hinit >m_return_bind normalize nodelta >Hregs
    690           >m_return_bind cases pre in Hregs EQpre;
    691           [1,3,6,8: [3,4: #x #y] #_ #_ whd in match (length ??); whd in ⊢ (??%? → ?);
    692              #EQ destruct(EQ)
    693           |2,4: #hd1 #tl1]
    694           #Hregs *
    695           [1,2: #lab4 * #rest4 ** #EQ destruct(EQ) * #nxt2 * #EQpc
    696             change with nxt2 in ⊢ (??%? → ?); #EQ destruct(EQ) #EQrest4
    697             whd in match (length ??); whd in ⊢ (??%? → ?); #EQ destruct(EQ) #_
    698           |*: #EQ1 #EQ2 destruct(EQ1 EQ2) #_ #_
    699           ]
    700           whd in EQmid : (??%%); destruct(EQmid) cases(pp_labs) #_ #H
    701           lapply(H lab2 (point_of_pc p_in pc) lab1 ? ?)
    702           [3,6,9,12: #EQ destruct(EQ) whd in match (stmt_at ????) in EQstmt;
    703              >(find_lookup ?????? EQfind) in EQstmt; #EQ destruct(EQ) %
    704           |1,4,7,10: >e0 [3,4: whd in match (memb ???); @eqb_elim
    705             [2,4: * #H @⊥ @H %] #_ @I] >memb_append_l2 [1,3: @I]
    706              whd in match (memb ???); @if_elim [1,3: #_ %] #_
    707              whd in match (memb ???); @eqb_elim [1,3: #_ %] * #H1 @⊥ @H1 %
    708           |*:  @Exists_memb assumption
    709           ]
    710         ]
    711      ]
    712 ]
    713 qed.
    714 
    715 
    716 definition make_is_relation_from_beval : (beval → beval → Prop) →
    717 internal_stack → internal_stack → Prop≝
    718 λR,is1,is2.
    719 match is1 with
    720 [ empty_is ⇒ match is2 with [ empty_is ⇒ True | _ ⇒ False]
    721 | one_is b ⇒ match is2 with [ one_is b' ⇒ R b b' | _ ⇒ False ]
    722 | both_is b1 b2 ⇒ match is2 with [ both_is b1' b2' ⇒ R b1 b1' ∧ R b2 b2' | _ ⇒ False ]
    723 ].
    724 
    725 lemma is_push_ok : ∀Rbeval : beval → beval → Prop.
    726 ∀Ristack1 : internal_stack → internal_stack → Prop.
    727 ∀Ristack2 : internal_stack → internal_stack → Prop.
    728 (∀is1,is2.Ristack1 is1 is2 → make_is_relation_from_beval Rbeval is1 is2) →
    729 (∀bv1,bv2.Ristack1 empty_is empty_is → Rbeval bv1 bv2 →
    730                                    Ristack2 (one_is bv1) (one_is bv2)) →
    731 (∀bv1,bv2,bv3,bv4.Rbeval bv1 bv2 → Rbeval bv3 bv4 →
    732                          Ristack2 (both_is bv3 bv1) (both_is bv4 bv2)) →
    733                          gen_preserving2 ?? gen_res_preserve …
    734                               Ristack1 Rbeval Ristack2 is_push is_push.
    735 #Rbeval #Ristack1 #Ristack2 #H #H1 #H2 #is1 #is2 #bv1 #bv2 #H3 #H4
    736 whd in match is_push; normalize nodelta cases is1 in H3; normalize nodelta
    737 [2:#x|3: #x #y #_ @res_preserve_error_gen]
    738 cases is2 normalize nodelta
    739  [1,3,5,6: [| #z #w | #z | #z #w] #H5 cases(H … H5) | #y] #H5 @m_gen_return
    740  [@H2 [assumption | @(H … H5) ] | @H1 assumption]
    741 qed.
    742 (*
    743 lemma is_push_ok : ∀R : beval → beval → Prop.
    744                gen_preserving2 ?? gen_res_preserve …
    745                        (make_is_relation_from_beval R) R
    746                        (make_is_relation_from_beval R)
    747                        is_push is_push.
    748 #R @is_push_ok_gen // #bv1 #bv2 #bv3 #bv4 #H #H1 %{H1 H}
    749 qed.
    750 *)
    751 lemma is_pop_ok: ∀Rbeval : beval → beval → Prop.
    752 ∀Ristack1 : internal_stack → internal_stack → Prop.
    753 ∀Ristack2 : internal_stack → internal_stack → Prop.
    754 (∀is1,is2.Ristack1 is1 is2 → make_is_relation_from_beval Rbeval is1 is2) →
    755 Ristack2 empty_is empty_is →
    756 (∀bv1,bv2.Rbeval bv1 bv2 → Ristack2 (one_is bv1) (one_is bv2)) →
    757           gen_preserving ?? gen_res_preserve …
    758                               Ristack1
    759                               (λx,y.Rbeval (\fst x) (\fst y) ∧
    760                                 Ristack2 (\snd x) (\snd y)) is_pop is_pop.
    761 #Rbeval #Ristack1 #Ristack2 #H #H1 #H2 #is1 #is2 whd in match is_pop; normalize nodelta
    762 cases is1 normalize nodelta [#_ @res_preserve_error_gen] #x [|#y] cases is2
    763 [1,3,4,5: [|#x #y||#x] #H3 cases(H … H3) | #y | #z #w] #H3 normalize nodelta
    764 @m_gen_return [ % [ @(H … H3) | assumption ] | cases(H … H3) #H4 #H5 %{H5} @(H2 … H4)
    765 qed.
    766 
    767 (*
    768 lemma is_pop_ok1 : ∀R : beval → beval → Prop.
    769            gen_preserving ?? gen_res_preserve …
    770                          (make_is_relation_from_beval R)
    771                          (λx,y.R (\fst x) (\fst y) ∧
    772                                (make_is_relation_from_beval R) (\snd x) (\snd y))
    773                          is_pop is_pop.
    774 #R @is_pop_ok //
    775 qed.
    776 
    777 
    778 definition make_weak_state_relation ≝
    779 λp_in,p_out.λR : (beval → beval → Prop).λst1 : state p_in.λst2 : state p_out.
    780 (make_is_relation_from_beval R) (istack … st1) (istack … st2).
    781 *)
    782 
    783 
    784 lemma push_ok : ∀p_in,p_out,Rbeval,Rstate1,Rstate2.
    785 (∀is1,is2,st1,st2.istack ? st1 = is1 → istack ? st2 = is2 → Rstate1 st1 st2 →
    786                   make_is_relation_from_beval Rbeval is1 is2) →
    787 (∀st1,st2,bv1,bv2. Rstate1 st1 st2 → Rbeval bv1 bv2 →
    788  Rstate2 (set_istack p_in (one_is bv1) st1) (set_istack p_out (one_is bv2) st2)) →
    789 (∀st1,st2,bv1,bv2,bv3,bv4.Rstate1 st1 st2 → Rbeval bv1 bv2 → Rbeval bv3 bv4 →
    790  Rstate2 (set_istack p_in (both_is bv1 bv3) st1) (set_istack p_out (both_is bv2 bv4) st2)) →
    791                     gen_preserving2 ?? gen_res_preserve … Rstate1 Rbeval Rstate2
    792                                    (push p_in) (push p_out).
    793 #p_in #p_out #Rbeval #Rstate1 #Rstate2 #H #H1 #H2 #st1 #st2 #bv1 #bv2 #H3 #H4
    794 whd in match push; normalize nodelta
    795 @(m_gen_bind_inversion … (make_is_relation_from_beval Rbeval))
    796 [ @(is_push_ok Rbeval (make_is_relation_from_beval Rbeval)) //
    797   [ #bv1 #bv2 #bv3 #bv4 #H5 #H6 whd %{H6 H5}
    798   | @(H … H3) %
    799   ]
    800 | * [|#x|#x1 #x2] * [1,4,7:|2,5,8: #y |*: #y1 #y2] #H5 #H6 whd in ⊢ (% → ?);
    801   [1,2,3,4,6,7,8,9: * [2: #H7 #H8] | #H7] @m_gen_return
    802   [ @(H2 … H3) assumption
    803   | cases(istack … st1) in H5; [2,3: #z [2: #w]] whd in ⊢ (??%% → ?);
    804     #EQ destruct(EQ)
    805   | @(H1 … H3) assumption
    806   ]
    807 ]
    808 qed.
    809 
    810 
    811 lemma pop_ok : ∀p_in,p_out,Rbeval,Rstate1,Rstate2.
    812 (∀is1,is2,st1,st2.istack ? st1 = is1 → istack ? st2 = is2 → Rstate1 st1 st2 →
    813                   make_is_relation_from_beval Rbeval is1 is2) →
    814 (∀st1,st2.Rstate1 st1 st2 →
    815  Rstate2 (set_istack p_in (empty_is) st1) (set_istack p_out (empty_is) st2)) →
    816 (∀st1,st2,bv1,bv2. Rstate1 st1 st2 → Rbeval bv1 bv2 →
    817  Rstate2 (set_istack p_in (one_is bv1) st1) (set_istack p_out (one_is bv2) st2)) →
    818                gen_preserving ?? gen_res_preserve …
    819                  Rstate1
    820                 (λx,y.Rbeval (\fst x) (\fst y) ∧
    821                  Rstate2(\snd x) (\snd y))
    822                 (pop p_in) (pop p_out).
    823 #p_in #p_out #Rbeval #Rstate1 #Rstate2 #H #H1 #H2 #st1 #st2 #H3
    824 whd in match pop; normalize nodelta
    825 @(m_gen_bind_inversion … (λx,y.Rbeval (\fst x) (\fst y) ∧
    826            (make_is_relation_from_beval Rbeval (\snd x) (\snd y)))) 
    827 [ @(is_pop_ok Rbeval (make_is_relation_from_beval Rbeval)) // @(H … H3) %
    828 | * #bv1 * [|#x|#x1 #x2] * #bv2 *
    829 [1,4,7:|2,5,8: #y
    830 |*: #y1 #y2 [1,2: #_ #_ * #_ *] cases(istack … st1) [|#z|#z #w] whd in ⊢ (??%% → ?); #EQ destruct ]
    831 #_ #_ * #H4 [2,3,4,6: *| #_ | whd in ⊢ (% → ?); #H5] @m_gen_return
    832 % // [ @(H1 … H3) | @(H2 … H3) assumption]
    833 qed.
    834 
    835 lemma fetch_internal_function_no_zero :
    836 ∀p,prog,stack_size,bl.
    837   block_id (pi1 … bl) = 0 →
    838   fetch_internal_function … (joint_globalenv p prog stack_size) bl =
    839   Error ? [MSG BadFunction].
    840 #p #prg #stack_size #bl #Hbl whd in match fetch_internal_function;
    841 whd in match fetch_function; normalize nodelta @eqZb_elim
    842 [ >Hbl #EQ @⊥ cases(not_eq_OZ_neg one) #H @H assumption ]
    843 #_ normalize nodelta cases(symbol_for_block ???) [%] #id >m_return_bind
    844 cases bl in Hbl; * #id #prf #EQ destruct(EQ)
    845 change with (mk_block OZ) in match (mk_block ?);
    846 cut(find_funct_ptr
    847     (fundef (joint_closed_internal_function p (prog_names p prg)))
    848     (joint_globalenv p prg stack_size) (mk_block OZ) = None ?) [%]
    849 #EQ >EQ %
    850 qed.
    851  
    852 lemma next_of_call_pc_ok : ∀P_in,P_out : sem_graph_params.
    853 ∀init,prog,stack_sizes,init_regs,f_lbls,f_regs.
    854 b_graph_transform_program_props P_in P_out stack_sizes
    855   init prog init_regs f_lbls f_regs →
    856 let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
    857 ∀bl :Σb.block_region b =Code.block_id bl ≠ -1 →
    858 ∀f,fn.
    859 fetch_internal_function … (joint_globalenv P_in prog stack_sizes) bl =
    860  return 〈f,fn〉 →
    861 (∀id,args,dest,lbl.
    862   bind_new_P' ??
    863   (λregs1.λdata.bind_new_P' ??
    864    (λregs2.λblp.
    865      ∀lbl.∃id',args',dest'.((\snd (\fst blp)) lbl) = CALL P_out ? id' args' dest')
    866    (f_step … data lbl (CALL P_in ? id args dest)))
    867   (init ? fn)) →
    868 gen_preserving ?? gen_res_preserve ????
    869  (λpc1,pc2 : Σpc.pc_block pc = bl.
    870            sigma_stored_pc P_in P_out prog stack_sizes init
    871                                            init_regs f_lbls f_regs pc2 = pc1)
    872  (λn1,n2.sigma_next P_in P_out prog stack_sizes init init_regs f_lbls f_regs bl n2 = return n1)
    873  (next_of_call_pc P_in … (joint_globalenv P_in prog stack_sizes))
    874  (next_of_call_pc P_out … (joint_globalenv P_out trans_prog stack_sizes)).
    875 #p_in #p_out #init #prog #stack_sizes #init_regs #f_lbls #f_regs #good #bl #Hbl
    876 #f #fn #EQfn #Hcall #pc1 #pc2 #Hpc1pc2 #lbl1 #H @('bind_inversion H) -H ** #f1 #fn1 *
    877 [ * [#c| #id #args #dest | #r #lb | #seq ] #nxt | #fin | *]
    878 whd in match fetch_statement; normalize nodelta >(pi2 ?? pc1) >EQfn >m_return_bind
    879 #H @('bind_inversion H) -H #stmt #H lapply(opt_eq_from_res ???? H) -H
    880 #EQstmt whd in ⊢ (??%% → ??%% → ?); #EQ1 #EQ2 destruct(EQ1 EQ2)
    881 cases(fetch_statement_sigma_stored_pc … pc1 f1 fn1 … good …)
    882 [3: >(pi2 ?? pc1) assumption
    883 |4: whd in match fetch_statement; normalize nodelta >(pi2 ?? pc1) in ⊢ (??%?);
    884     >EQfn in ⊢ (??%?); >m_return_bind in ⊢ (??%?); >EQstmt in ⊢ (??%?); % |2:]
    885 #data * #Hdata normalize nodelta * #st_bl * #Hst_bl * #pc' * #EQpc' * #t_fn
    886 * #nxt1 * #l1 * #l2 *** #EQt_fetch #_ #_ #nxt1rel %{nxt1} % [2: <(pi2 ?? pc1) assumption]
    887 whd in match next_of_call_pc; normalize nodelta <EQpc' in Hpc1pc2;
    888 #H lapply(sym_eq ??? H) -H whd in match sigma_stored_pc; normalize nodelta
    889 inversion(sigma_pc_opt ?????????)
    890 [ #ABS @⊥ whd in match sigma_stored_pc in EQpc'; normalize nodelta in EQpc';
    891   >ABS in EQpc'; normalize nodelta #EQ <(pi2 ?? pc1) in EQfn;
    892   >fetch_internal_function_no_zero [2: <EQ %] whd in ⊢ (???% → ?); #EQ1 destruct(EQ1) ]
    893 #sigma_pc' #EQsigma_pc' normalize nodelta inversion(sigma_pc_opt ?????????)
    894 [ #_ normalize nodelta #EQ destruct(EQ) @⊥ lapply EQt_fetch @if_elim #_ #EQf
    895   cases(fetch_statement_inv … EQf) >fetch_internal_function_no_zero [1,3: #EQ destruct]
    896   >(pc_block_eq p_in p_out prog stack_sizes init init_regs f_lbls f_regs)
    897   [1,3: whd in match sigma_stored_pc; normalize nodelta >EQsigma_pc' %
    898   |*: >EQsigma_pc' % #EQ destruct
    899   ]
    900 ]
    901 #pc3 #EQpc3 normalize nodelta #EQ destruct(EQ) <EQsigma_pc' in EQpc3; #H
    902 lapply(sym_eq ??? H) -H #EQp lapply(sigma_stored_pc_inj … EQp) [>EQsigma_pc' % #EQ destruct]
    903 #EQ destruct(EQ) >EQt_fetch @eq_identifier_elim
    904 [ #EQ1 >EQ1 in EQstmt; cases(entry_is_cost … (pi2 ?? fn1)) #nxt2 * #c #ABS >ABS #EQ1 destruct(EQ1) ]
    905 #_ cases(not_emptyb ??) normalize nodelta >m_return_bind normalize nodelta
    906 lapply(bind_new_bind_new_instantiates … (bind_instantiates_to_instantiate … Hst_bl)
    907        (bind_new_bind_new_instantiates … (bind_instantiates_to_instantiate … Hdata)
    908         (Hcall id args dest (point_of_pc p_in pc1))))
    909 #H cases(H (point_of_pc p_in pc2)) #id' * #args' * #dest' #EQ >EQ %
    910 qed.
    911 
    912 definition joint_state_relation ≝
    913 λP_in,P_out.program_counter → state P_in → state P_out → Prop.
    914 
    915 definition joint_state_pc_relation ≝ λP_in,P_out.state_pc P_in → state_pc P_out → Prop.
    916 
    917 record good_state_relation (P_in : sem_graph_params)
    918    (P_out : sem_graph_params) (prog : joint_program P_in)
    919    (stack_sizes : ident → option ℕ)
    920    (init : ∀globals.joint_closed_internal_function P_in globals
    921          →bound_b_graph_translate_data P_in P_out globals)
    922    (init_regs : block → list register) (f_lbls : lbl_funct_type)
    923    (f_regs : regs_funct_type)
    924    (st_no_pc_rel : joint_state_relation P_in P_out)
    925    (st_rel : joint_state_pc_relation P_in P_out) : Prop ≝
    926 { good_translation :> b_graph_transform_program_props P_in P_out stack_sizes init
    927                      prog init_regs f_lbls f_regs
    928 ; fetch_ok_sigma_state_ok :
    929    ∀st1,st2,f,fn. st_rel st1 st2 →
    930     fetch_internal_function …
    931      (joint_globalenv P_in prog stack_sizes) (pc_block (pc … st1)) 
    932      = return 〈f,fn〉 →
    933      st_no_pc_rel (pc … st1) (st_no_pc … st1) (st_no_pc … st2)
    934 ; fetch_ok_pc_ok :
    935   ∀st1,st2,f,fn.st_rel st1 st2 →
    936    fetch_internal_function …
    937      (joint_globalenv P_in prog stack_sizes) (pc_block (pc … st1)) 
    938      = return 〈f,fn〉 →
    939    pc … st1 = pc … st2
    940 ; fetch_ok_sigma_last_pop_ok :
    941   ∀st1,st2,f,fn.st_rel st1 st2 →
    942    fetch_internal_function …
    943      (joint_globalenv P_in prog stack_sizes) (pc_block (pc … st1)) 
    944      = return 〈f,fn〉 →
    945    (last_pop … st1) = sigma_stored_pc P_in P_out prog stack_sizes init init_regs
    946                        f_lbls f_regs (last_pop … st2)
    947 ; st_rel_def :
    948   ∀st1,st2,pc,lp1,lp2,f,fn.
    949   fetch_internal_function …
    950      (joint_globalenv P_in prog stack_sizes) (pc_block pc) = return 〈f,fn〉 →
    951    st_no_pc_rel pc st1 st2 →
    952    lp1 = sigma_stored_pc P_in P_out prog stack_sizes init init_regs
    953           f_lbls f_regs lp2 →
    954   st_rel (mk_state_pc ? st1 pc lp1) (mk_state_pc ? st2 pc lp2)
    955 ; as_label_ok_non_entry :
    956   let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
    957   ∀st1,st2,f,fn,stmt.
    958   fetch_statement …
    959   (joint_globalenv P_in prog stack_sizes) (pc … st1) = return〈f,fn,stmt〉 →
    960   st_rel st1 st2 → point_of_pc P_in (pc … st1) ≠ joint_if_entry … fn →
    961   as_label (joint_status P_in prog stack_sizes) st1 =
    962   as_label (joint_status P_out trans_prog stack_sizes) st2
    963 ; pre_main_ok :
    964   let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
    965     ∀st1,st1' : joint_abstract_status (mk_prog_params P_in prog stack_sizes) .
    966     ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes).
    967     block_id … (pc_block (pc … st1)) = -1 →
    968     st_rel st1 st2 →
    969     as_label (joint_status P_in prog stack_sizes) st1 =
    970     as_label (joint_status P_out trans_prog stack_sizes) st2 ∧
    971     joint_classify … (mk_prog_params P_in prog stack_sizes) st1 =
    972     joint_classify … (mk_prog_params P_out trans_prog stack_sizes) st2 ∧
    973     (eval_state P_in … (joint_globalenv P_in prog stack_sizes)
    974       st1 = return st1' →
    975     ∃st2'. st_rel st1' st2' ∧
    976     eval_state P_out …
    977      (joint_globalenv P_out trans_prog stack_sizes) st2 = return st2')
    978 ; cond_commutation :
    979     let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
    980     ∀st1 : joint_abstract_status (mk_prog_params P_in prog stack_sizes) .
    981     ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes).
    982     ∀f,fn,a,ltrue,lfalse,bv,b.
    983     block_id … (pc_block (pc … st1)) ≠ -1 →
    984     let cond ≝ (COND P_in ? a ltrue) in
    985     fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) =
    986     return 〈f, fn,  sequential … cond lfalse〉 → 
    987     acca_retrieve … P_in (st_no_pc … st1) a = return bv →
    988     bool_of_beval … bv = return b →
    989     st_rel st1 st2 →
    990     ∀t_fn.
    991     fetch_internal_function …
    992      (joint_globalenv P_out trans_prog stack_sizes) (pc_block (pc … st2)) =
    993      return 〈f,t_fn〉 →
    994     bind_new_P' ??
    995      (λregs1.λdata.bind_new_P' ??
    996      (λregs2.λblp.(\snd blp) = [ ] ∧
    997         ∀mid.
    998           stmt_at P_out … (joint_if_code ?? t_fn) mid
    999           = return sequential P_out ? ((\snd (\fst blp)) mid) lfalse→
    1000          ∃st2_pre_mid_no_pc.
    1001             repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f
    1002              (map_eval ?? (\fst (\fst blp)) mid) (st_no_pc ? st2)
    1003             = return st2_pre_mid_no_pc ∧
    1004             let new_pc ≝ if b then
    1005                            (pc_of_point P_in (pc_block (pc … st1)) ltrue)
    1006                          else
    1007                            (pc_of_point P_in (pc_block (pc … st1)) lfalse) in
    1008             st_no_pc_rel new_pc (st_no_pc … st1) (st2_pre_mid_no_pc) ∧
    1009             ∃a'. ((\snd (\fst blp)) mid)  = COND P_out ? a' ltrue ∧
    1010             ∃bv'. acca_retrieve … P_out st2_pre_mid_no_pc a' = return bv' ∧
    1011                   bool_of_beval … bv' = return b
    1012    )  (f_step … data (point_of_pc P_in (pc … st1)) cond)   
    1013   ) (init ? fn)
    1014 ; seq_commutation :
    1015   let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
    1016   ∀st1,st1' : joint_abstract_status (mk_prog_params P_in prog stack_sizes) .
    1017   ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes).
    1018   ∀f,fn,stmt,nxt.
    1019   block_id … (pc_block (pc … st1)) ≠ -1 →
    1020   let seq ≝ (step_seq P_in ? stmt) in
    1021   fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) =
    1022   return 〈f, fn,  sequential … seq nxt〉 → 
    1023   eval_state P_in … (joint_globalenv P_in prog stack_sizes)
    1024   st1 = return st1' →
    1025   st_rel st1 st2 →
    1026   ∀t_fn.
    1027   fetch_internal_function …
    1028      (joint_globalenv P_out trans_prog stack_sizes) (pc_block (pc … st2)) =
    1029   return 〈f,t_fn〉 →
    1030   bind_new_P' ??
    1031      (λregs1.λdata.bind_new_P' ??
    1032       (λregs2.λblp.
    1033        ∃l : list (joint_seq P_out (globals ? (mk_prog_params P_out trans_prog stack_sizes))).
    1034                             blp = (ensure_step_block ?? l) ∧
    1035        ∃st2_fin_no_pc.
    1036            repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f
    1037               l  (st_no_pc … st2)= return st2_fin_no_pc ∧
    1038            st_no_pc_rel (pc … st1') (st_no_pc … st1') st2_fin_no_pc
    1039       ) (f_step … data (point_of_pc P_in (pc … st1)) seq)
    1040      ) (init ? fn)
    1041 ;  call_is_call :∀f,fn,bl.
    1042   fetch_internal_function …
    1043      (joint_globalenv P_in prog stack_sizes) bl = return 〈f,fn〉 →
    1044    ∀id,args,dest,lbl.
    1045     bind_new_P' ??
    1046      (λregs1.λdata.bind_new_P' ??
    1047       (λregs2.λblp.
    1048         ∀lbl.∃id',args',dest'.((\snd (\fst blp)) lbl) = CALL P_out ? id' args' dest')
    1049       (f_step … data lbl (CALL P_in ? id args dest)))
    1050      (init ? fn)
    1051 ; cost_commutation :
    1052   let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
    1053   ∀st1,st2,pc.∀f,fn,c,nxt.
    1054   block_id … (pc_block pc) ≠ -1 →
    1055   st_no_pc_rel pc st1 st2 →
    1056   fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) pc =
    1057   return 〈f, fn,  sequential ?? (COST_LABEL ?? c) nxt〉 → 
    1058   st_no_pc_rel (pc_of_point P_in (pc_block pc) nxt) st1 st2
    1059 ; return_commutation :
    1060   let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
    1061   ∀st1 : joint_abstract_status (mk_prog_params P_in prog stack_sizes) .
    1062   ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes).
    1063   ∀f,fn.
    1064   block_id … (pc_block (pc … st1)) ≠ -1 →
    1065   fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) =
    1066   return 〈f, fn,  final P_in ? (RETURN …)〉 → 
    1067   ∀n. stack_sizes f = return n →
    1068   let curr_ret ≝ joint_if_result … fn in
    1069   ∀st_pop,pc_pop.
    1070   pop_frame ?? P_in ? (joint_globalenv P_in prog stack_sizes) f curr_ret
    1071    (st_no_pc … st1) = return 〈st_pop,pc_pop〉 →
    1072   ∀nxt.∀f1,fn1,id,args,dest.
    1073     fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) pc_pop  =
    1074     return 〈f1,fn1,sequential P_in … (CALL P_in ? id args dest) nxt〉 →
    1075   st_rel st1 st2 →
    1076   ∀t_fn.
    1077   fetch_internal_function …
    1078      (joint_globalenv P_out trans_prog stack_sizes) (pc_block (pc … st2)) =
    1079   return 〈f,t_fn〉 →
    1080   bind_new_P' ??
    1081      (λregs1.λdata.
    1082       bind_new_P' ??
    1083       (λregs2.λblp.
    1084        \snd blp = (RETURN …) ∧
    1085        ∃st_fin. repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f
    1086               (\fst blp)  (st_no_pc … st2)= return st_fin ∧
    1087         ∃t_st_pop,t_pc_pop.
    1088         pop_frame ?? P_out ? (joint_globalenv P_out trans_prog stack_sizes) f
    1089          (joint_if_result … t_fn) st_fin = return 〈t_st_pop,t_pc_pop〉 ∧
    1090         sigma_stored_pc P_in P_out prog stack_sizes init init_regs f_lbls f_regs
    1091          t_pc_pop = pc_pop ∧
    1092         if eqZb (block_id (pc_block pc_pop)) (-1) then
    1093             st_no_pc_rel (pc_of_point P_in (pc_block pc_pop) nxt)
    1094              (decrement_stack_usage ? n st_pop) (decrement_stack_usage ? n t_st_pop) (*pre_main*)
    1095         else
    1096             bind_new_P' ??
    1097             (λregs4.λdata1.
    1098                bind_new_P' ??
    1099                (λregs3.λblp1.
    1100                  ∃st2'. repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f1
    1101                       (\snd blp1) (decrement_stack_usage ? n t_st_pop) = return st2' ∧
    1102                       st_no_pc_rel (pc_of_point P_in (pc_block pc_pop) nxt)
    1103                        (decrement_stack_usage ? n st_pop) st2'
    1104                ) (f_step … data1 (point_of_pc P_in pc_pop) (CALL P_in ? id args dest))
    1105             ) (init ? fn1)
    1106           ) (f_fin … data (point_of_pc P_in (pc … st1)) (RETURN …))
    1107      ) (init ? fn)
    1108 ; call_commutation :
    1109   let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
    1110   ∀st1 : joint_abstract_status (mk_prog_params P_in prog stack_sizes) .
    1111   ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes).
    1112   ∀f,fn,id,arg,dest,nxt.
    1113   block_id … (pc_block (pc … st1)) ≠ -1 →
    1114   fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) =
    1115   return 〈f, fn,  sequential P_in ? (CALL P_in ? id arg dest) nxt〉 →
    1116   ∀bl.
    1117    block_of_call P_in … (joint_globalenv P_in prog stack_sizes) id (st_no_pc … st1)
    1118       = return bl →
    1119   ∀f1,fn1.
    1120    fetch_internal_function …
    1121     (joint_globalenv P_in prog stack_sizes) bl =  return 〈f1,fn1〉 →
    1122   ∀st1_pre.
    1123   save_frame … P_in (kind_of_call P_in id) dest st1 = return st1_pre →
    1124   ∀n.stack_sizes f1 = return n → 
    1125   ∀st1'.
    1126   setup_call ?? P_in n (joint_if_params … fn1) arg st1_pre = return st1' →
    1127   st_rel st1 st2 → 
    1128   ∀t_fn.
    1129   fetch_internal_function …
    1130   (joint_globalenv P_out trans_prog stack_sizes) (pc_block (pc … st2)) =
    1131   return 〈f,t_fn〉 →
    1132   ∀t_fn1.
    1133   fetch_internal_function … (joint_globalenv P_out trans_prog stack_sizes) bl =
    1134   return 〈f1,t_fn1〉 →
    1135   bind_new_P' ??
    1136     (λregs1.λdata.
    1137      bind_new_P' ??
    1138       (λregs2.λblp.
    1139         ∀mid,id',arg',dest',nxt1.
    1140           stmt_at P_out … (joint_if_code ?? t_fn) mid
    1141           = return sequential P_out ? ((\snd (\fst blp)) mid) nxt1→
    1142           ((\snd (\fst blp)) mid) = (CALL P_out ? id' arg' dest') → 
    1143        ∃st2_pre_call.
    1144         repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f
    1145           (map_eval ?? (\fst (\fst blp)) mid) (st_no_pc ? st2) = return st2_pre_call ∧
    1146        block_of_call P_out … (joint_globalenv P_out trans_prog stack_sizes) id'
    1147         st2_pre_call = return bl ∧
    1148        ∃st2_pre.
    1149         save_frame … P_out (kind_of_call P_out id') dest'
    1150          (mk_state_pc ? st2_pre_call (pc_of_point P_out (pc_block(pc … st2)) mid)
    1151           (last_pop … st2)) = return st2_pre ∧
    1152        ∃st2_after_call.
    1153          setup_call ?? P_out n (joint_if_params … t_fn1) arg' st2_pre
    1154           = return st2_after_call ∧
    1155        bind_new_P' ??
    1156          (λregs11.λdata1.
    1157           ∃st2'.
    1158            repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f1
    1159            (added_prologue … data1) (increment_stack_usage P_out n st2_after_call) =
    1160            return st2' ∧
    1161            st_no_pc_rel (pc_of_point P_in bl (joint_if_entry … fn1))
    1162             (increment_stack_usage P_in n st1') st2'
    1163                
    1164          ) (init ? fn1)
    1165      )
    1166      (f_step … data (point_of_pc P_in (pc … st1)) (CALL P_in ? id arg dest))
    1167     ) (init ? fn)
    1168 }.
    1169 
    1170 definition JointStatusSimulation :
    1171 ∀p_in,p_out : sem_graph_params.
    1172 ∀ prog.∀stack_sizes.
    1173 ∀ f_lbls, f_regs. ∀init_regs.∀init.∀st_no_pc_rel,st_rel.
    1174 good_state_relation p_in p_out prog stack_sizes init init_regs f_lbls f_regs
    1175                     st_no_pc_rel st_rel →
    1176 let trans_prog ≝ b_graph_transform_program p_in p_out init prog in
    1177 status_rel (joint_abstract_status (mk_prog_params p_in prog stack_sizes))
    1178            (joint_abstract_status (mk_prog_params p_out trans_prog stack_sizes)) ≝
    1179 λp_in,p_out,prog,stack_sizes,f_lbls,f_regs,init_regs,init,st_no_pc_rel,st_rel,good.
    1180    mk_status_rel ??
    1181     (* sem_rel ≝ *) (λs1 : (joint_abstract_status (mk_prog_params p_in ??)).
    1182                      λs2 : (joint_abstract_status (mk_prog_params p_out ??)).st_rel s1 s2)
    1183     (* call_rel ≝ *) 
    1184        (λs1:Σs: (joint_abstract_status (mk_prog_params p_in ??)).as_classifier ? s cl_call
    1185           .λs2:Σs:(joint_abstract_status (mk_prog_params p_out ??)).as_classifier ? s cl_call
    1186            .pc ? s1 =
    1187         sigma_stored_pc p_in p_out prog stack_sizes init init_regs f_lbls f_regs (pc ? s2)).
    1188 
    1189 (*
    1190 lemma fetch_stmt_ok_succs_ok : ∀p : sem_graph_params.
    1191 ∀prog : joint_program p.∀stack_size,f,fn,stmt,pc,pc',lbl.
    1192 In ? (stmt_labels p ? stmt) lbl→
    1193 fetch_statement p … (joint_globalenv p prog stack_size) pc = return 〈f,fn,stmt〉 →
    1194 pc' = pc_of_point p (pc_block pc) lbl →
    1195 ∃stmt'.fetch_statement p … (joint_globalenv p prog stack_size) pc' = return 〈f,fn,stmt'〉.
    1196 #p #prog #stack_size #f #fn #stmt #pc #pc' #lbl #Hlbl #EQfetch
    1197 cases(fetch_statement_inv … EQfetch) #EQfn normalize nodelta #EQstmt
    1198 #EQ destruct(EQ) lapply(code_is_closed … (pi2 ?? fn) … EQstmt) *
    1199 cases(decidable_In ? (stmt_explicit_labels … stmt) lbl ?)
    1200 [3: * cases lbl #x #y cases(decidable_eq_pos … x y)
    1201     [#EQ destruct % % | * #H %2 % #H1 @H destruct %]
    1202 | whd in ⊢ (% → ?); #H1 #H2 cases(Exists_All … H1 H2) #lbl1 * #EQ destruct
    1203   whd in match code_has_label; whd in match code_has_point; normalize nodelta
    1204   inversion(stmt_at ????) [#_ *] #stmt' #EQstmt' #_ #_ %{stmt'}
    1205   whd in match fetch_statement; normalize nodelta >EQfn >m_return_bind
    1206   >point_of_pc_of_point >EQstmt' %
    1207 | #H lapply(In_all ??? H) -H cases(Exists_append … Hlbl)
    1208   [ cases stmt [ #step #nxt | #fin | *] whd in match stmt_implicit_label;
    1209     normalize nodelta [2: *] * [2: *] #EQ destruct(EQ) #_ #_
    1210     whd in match stmt_forall_succ; whd in match code_has_point; normalize nodelta
    1211     inversion(stmt_at ????) [#_ *] #stmt' #EQstmt' #_ %{stmt'}
    1212     whd in match fetch_statement; normalize nodelta >EQfn >m_return_bind
    1213     >point_of_pc_of_point >EQstmt' %
    1214   | #H1 #H2 cases(Exists_All … H1 H2) #x * #EQ destruct * #H @⊥ @H %
    1215   ]
    1216 ]
    1217 qed.
    1218 *)
    1219 
     15include "joint/StatusSimulationUtils.ma".
    122016
    122117lemma fetch_stmt_ok_sigma_state_ok : ∀ P_in , P_out: sem_graph_params.
     
    127470qed.
    127571
    1276 (*
    1277 lemma fetch_stmt_ok_st_rel_def : ∀ P_in , P_out: sem_graph_params.
     72lemma as_label_ok_non_entry :  ∀ P_in , P_out: sem_graph_params.
    127873∀prog : joint_program P_in.
    127974∀stack_sizes.
    128075∀ f_lbls,f_regs.∀f_bl_r.∀init.
    1281 ∀good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs.
    128276∀st_no_pc_rel,st_rel.
    1283 ∀f,fn,stmt,st1,st2.
    1284 good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs good
     77let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
     78let trans_prog  ≝ b_graph_transform_program P_in P_out init prog in
     79let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
     80good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs
    128581                    st_no_pc_rel st_rel →
    1286 st_no_pc_rel (st_no_pc … st1) (st_no_pc … st2) → (pc … st1) = (pc … st2) →
    1287 (last_pop … st1) = sigma_stored_pc P_in P_out prog f_lbls (last_pop … st2) →
    1288 fetch_statement P_in … (ev_genv … (mk_prog_params P_in prog stack_sizes)) (pc … st1) =
    1289  return 〈f,fn,stmt〉 → st_rel st1 st2.
    1290 #P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #good #st_no_pc_rel
    1291 #st_rel #f #fn #stmt * #st1 #pc1 #lp1 * #st2 #pc2 #lp2 #goodR #Hno_pc #EQ destruct(EQ)
    1292 #EQlp1 #EQfetch cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt
    1293 @(st_rel_def … goodR … EQfn) assumption
     82∀st1,st2,f,fn,stmt.
     83fetch_statement …
     84 (joint_globalenv P_in prog stack_sizes) (pc … st1) = return〈f,fn,stmt〉 →
     85block_id … (pc_block (pc … st1)) ≠ -1 →
     86 st_rel st1 st2 → point_of_pc P_in (pc … st1) ≠ joint_if_entry … fn →
     87as_label (joint_status P_in prog stack_sizes) st1 =
     88 as_label (joint_status P_out trans_prog stack_sizes) st2.
     89#p_in #p_out #prog #stack_size #f_lbls #f_regs #init_regs #init #st_no_pc_rel #st_rel
     90#good #st1 #st2 #f #fn #stmt #EQfetch * #Hbl #Rst1st2 * #Hentry
     91whd in ⊢ (??%%); >EQfetch normalize nodelta
     92lapply(b_graph_transform_program_fetch_statement … good (pc … st1) f fn ?)
     93[2: @eqZb_elim [1: #ABS @⊥ >ABS in Hbl; #H @H %] #_ normalize nodelta
     94      #H cases(H EQfetch) -H |*:] #data * #t_fn ** #EQt_fn #Hdata #H
     95whd in match fetch_statement; normalize nodelta
     96>(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in EQt_fn; #EQt_fn >EQt_fn
     97>m_return_bind cases stmt in EQfetch H;
     98[ * [ #c | #id #args #dest | #r #lb | #seq] #nxt | * [ #lb | | #has #id #args ] | * ]
     99#EQfetch normalize nodelta * #bl
     100[1,2,3,4: @eq_identifier_elim
     101  [1,3,5,7: #EQ @⊥ @Hentry >EQ %
     102  |*: #_ cut(∀b.andb b false = false) [1,3,5,7: * %] #EQ >EQ -EQ normalize nodelta
     103  ]
     104]
     105*
     106[ >(f_step_on_cost … data) whd in ⊢ (% → ?); cases(f_regs ??) [2: # x #y *]
     107  normalize nodelta #EQ destruct(EQ) * #l1 * #mid1 * #mid2 * #l2 *** #EQmid1
     108  whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2) * #nxt1 * #EQcost
     109  change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) * #EQ1 #EQ2 destruct(EQ1 EQ2)
     110  >(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in EQcost; #EQcost >EQcost %
     111]
     112#Hregs *
     113[1,2,3: * [2,4,6: #hd #tl * #mid1 * #mid2 * #l2 *** #EQmid1 cases(\fst (\fst bl))
     114          [1,3,5: whd in ⊢ (% → ?); * #EQ destruct(EQ)] #hd1 #tl1 whd in ⊢ (% → ?);
     115          * #mid3 * #rest ** #EQ destruct(EQ) * #nxt1 * #EQ
     116          change with nxt1 in ⊢ (??%? → ?); #EQ1 destruct(EQ1) #_ #_ #_
     117          >(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in EQ; #EQ >EQ % ]
     118        * #mid1 * #mid2 * #l2 *** #_ cases bl in Hregs; **
     119        [2,4,6: #x #y #z #w #_ whd in ⊢ (% → ?); * #a * #b ** #EQ destruct(EQ)]
     120        #instr #post #Hregs whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2) *
     121        #nxt1 * #EQ change with nxt1 in ⊢ (??%? → ?); #EQ1 destruct(EQ1)
     122         >(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in EQ; #EQ #_ >EQ
     123        inversion(instr ?)
     124        [2,3,4,6,7,8,10,11,12: [1,4,7: #id1 #arg1 #dest1 |2,5,8: #r1 #lb1 |*: #seq]
     125          #EQ1 >EQ1 %] #c1 #EQc1
     126        lapply(bind_new_bind_new_instantiates … Hregs (cost_in_f_step … data … c1) …
     127             (jmeq_to_eq ??? EQc1)) #EQ destruct(EQ)
     128|*: * [2,4,6: #hd #tl * #mid ** #_ cases (\fst bl) [1,3,5: * #EQ destruct(EQ)]
     129      #hd1 #tl1 whd in ⊢ (% → ?); * #mid1 * #rest ** #EQ destruct(EQ) whd in ⊢ (% → ?);
     130      * #nxt1 * #EQ change with nxt1 in ⊢ (??%? → ?); #EQ1 destruct(EQ1) #_ #_         
     131      >(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in EQ; #EQ >EQ %
     132      |*: * #mid ** #_ cases bl in Hregs; * [2,4,6: #x #y #z #_ * #w * #a ** #EQ destruct]
     133          #instr #_ * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in ⊢ (% → ?);
     134          >(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) #EQ >EQ %
     135      ]   
     136]
     137qed.
     138 
     139
     140lemma eval_goto_ok : ∀ P_in , P_out: sem_graph_params.
     141∀prog : joint_program P_in.
     142∀stack_sizes.
     143∀ f_lbls,f_regs.∀f_bl_r.∀init.
     144∀st_no_pc_rel,st_rel.
     145let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
     146let trans_prog  ≝ b_graph_transform_program P_in P_out init prog in
     147let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
     148good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs
     149                    st_no_pc_rel st_rel →
     150∀st1,st1' : joint_abstract_status prog_pars_in.
     151∀st2 : joint_abstract_status prog_pars_out.
     152∀f : ident.
     153∀fn : joint_closed_internal_function P_in ?.
     154∀lbl.
     155block_id … (pc_block (pc … st1)) ≠ -1 →
     156st_rel st1 st2 →
     157 let goto ≝ (GOTO P_in lbl) in
     158  fetch_statement P_in ?
     159   (joint_globalenv P_in prog stack_sizes) (pc … st1) =
     160     return 〈f, fn, final … goto〉 →
     161 eval_state P_in …
     162  (joint_globalenv P_in prog stack_sizes) st1 = return st1' →
     163∃ st2'. st_rel st1' st2' ∧
     164∃taf : trace_any_any_free (joint_abstract_status prog_pars_out) st2 st2'.
     165bool_to_Prop (taaf_non_empty … taf) ∧
     166as_label (joint_abstract_status prog_pars_in) st1' =
     167as_label (joint_abstract_status prog_pars_out) st2'.
     168#p_in #p_out #prog #stack_size #f_lbls #f_regs #init_regs #init #st_no_pc_rel
     169#st_rel #good #st1 #st1' #st2 #f #fn #lbl * #Hbl #Rst1st2 #EQfetch
     170whd in match eval_state; normalize nodelta >EQfetch >m_return_bind
     171whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
     172whd in match eval_statement_advance; normalize nodelta whd in match goto;
     173normalize nodelta >pc_of_label_eq
     174[2: @(proj1 … (fetch_statement_inv … EQfetch)) |*: ]
     175>m_return_bind whd in match set_no_pc;
     176whd in match set_pc; normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ)
     177lapply(b_graph_transform_program_fetch_statement … good (pc … st1) f fn ?)
     178[2,4: @eqZb_elim [1,3: #ABS @⊥ >ABS in Hbl; #H @H %] #_ normalize nodelta
     179      #H cases(H EQfetch) -H |*:]
     180#data * #t_fn ** #EQt_fn #Hdata normalize nodelta ** #pre #instr * #Hregs
     181* #l1 * #mid ** #EQmid #EQl1 whd in ⊢ (% → ?); #EQfin
     182cases(bind_new_bind_new_instantiates' … Hregs
     183  (bind_new_bind_new_instantiates' … Hdata (goto_commutation … good …
     184       EQfetch Rst1st2 …)))
     185[2: % assumption
     186|4: <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in ⊢ (??%?); assumption
     187|3:
     188]
     189#st2_fin ** #EQst2_fin #EQ destruct(EQ) #Hfin_rel
     190%{(mk_state_pc ? st2_fin (pc_of_point p_out (pc_block (pc … st2)) lbl)
     191    (last_pop … st2))}
     192cut(? : Prop)
     193[3: #Rst1st2' %{Rst1st2'}
     194|
     195| <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) @(st_rel_def … good)
     196  [3: @(proj1 … (fetch_statement_inv … EQfetch)) |1,2:
     197  |5: @(fetch_stmt_ok_sigma_last_pop_ok … good … Rst1st2 EQfetch)
     198  | assumption
     199  ]
     200]
     201>(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in EQl1; #EQl1
     202lapply(taaf_to_taa … (produce_trace_any_any_free … st2 … … EQl1 … EQst2_fin) ?)
     203[ @if_elim #_ [2: @I] % whd in ⊢ (% → ?); * #H @H -H whd in ⊢ (??%?);
     204  whd in match (as_pc_of ??); whd in match fetch_statement; normalize nodelta
     205  <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) >EQt_fn >m_return_bind
     206  whd in match point_of_pc; normalize nodelta >point_of_offset_of_point
     207  >EQfin %
     208| <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) >EQt_fn %
     209]
     210#taa %{(taaf_step … taa …)}
     211[3: %{I}
     212|*: whd [ whd in ⊢ (??%?); | whd in match eval_state;] whd in match fetch_statement;
     213    normalize nodelta <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) >EQt_fn
     214    >m_return_bind >point_of_pc_of_point >EQfin [%] >m_return_bind
     215    whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
     216    whd in match eval_statement_advance; whd in match goto; normalize nodelta
     217    >pc_of_label_eq
     218    [2: whd in match (pc_block ?); >EQt_fn in ⊢ (??%?); % |3:] %
     219]
     220cases(fetch_stmt_ok_succ_ok … lbl … EQfetch) [4: %|3: % % |*:]
     221#stmt' #EQstmt'
     222@(as_label_ok_non_entry … good)
     223[4: <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in ⊢ (??%?); @EQstmt'
     224|1,2,3:
     225| <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) % assumption
     226| <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in ⊢ (?%?); assumption
     227| <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch)
     228  cases(entry_unused ??? (pi2 ?? fn) ?? (proj2 ?? (fetch_statement_inv … EQfetch)))
     229  * whd in match (point_of_label ????); * #H #_ #_ % >point_of_pc_of_point #EQ destruct(EQ)
     230  @H %
     231]
    1294232qed.
    1295 *)
    1296 
    1297 (*
    1298 (*CSC: Isn't this already proved somewhere else??? *)
    1299 lemma point_of_pc_pc_of_point:
    1300  ∀P_in: sem_graph_params.∀l,st.
    1301    point_of_pc P_in
    1302     (pc_of_point (mk_sem_graph_params (sgp_pars P_in) (sgp_sup P_in))
    1303      (pc_block (pc P_in st)) l) = l.
    1304  #P * //
    1305 qed.*)
    1306 
    1307 
    1308 lemma general_eval_cond_ok : ∀ P_in , P_out: sem_graph_params.
     233
     234lemma eval_goto_premain_ok : ∀ P_in , P_out: sem_graph_params.
     235∀prog : joint_program P_in.
     236∀stack_sizes.
     237∀ f_lbls,f_regs.∀f_bl_r.∀init.
     238∀st_no_pc_rel,st_rel.
     239let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
     240let trans_prog  ≝ b_graph_transform_program P_in P_out init prog in
     241let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
     242good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs
     243                    st_no_pc_rel st_rel →
     244∀st1,st1' : joint_abstract_status prog_pars_in.
     245∀st2 : joint_abstract_status prog_pars_out.
     246∀f : ident.
     247∀fn : joint_closed_internal_function P_in ?.
     248∀lbl.
     249block_id … (pc_block (pc … st1)) = -1 →
     250st_rel st1 st2 →
     251 let goto ≝ (GOTO P_in lbl) in
     252  fetch_statement P_in ?
     253   (joint_globalenv P_in prog stack_sizes) (pc … st1) =
     254     return 〈f, fn, final … goto〉 →
     255 eval_state P_in …
     256  (joint_globalenv P_in prog stack_sizes) st1 = return st1' →
     257∃ st2'. st_rel st1' st2' ∧
     258∃taf : trace_any_any_free (joint_abstract_status prog_pars_out) st2 st2'.
     259bool_to_Prop (taaf_non_empty … taf) ∧
     260as_label (joint_abstract_status prog_pars_in) st1' =
     261as_label (joint_abstract_status prog_pars_out) st2'.
     262#p_in #p_out #prog #stack_sizes #f_lbls #f_regs #init_regs #init #st_no_pc_rel
     263#st_rel #good #st1 #st1' #st2 #f #fn #lbl #EQbl #Rst1st2 #EQfetch #EQeval
     264cases(pre_main_ok … good … EQbl EQeval Rst1st2) #Hclass * #st2' ** #Rst1st2'
     265#EQst2' #Hlab %{st2'} % [assumption] %{(taaf_step … (taa_base …)…)}
     266[ whd change with (joint_classify ???) in ⊢ (??%?); <Hclass whd in match joint_classify;
     267  normalize nodelta >EQfetch %
     268| assumption ] %{I} assumption
     269qed.
     270
     271
     272lemma eval_tailcall_ok : ∀ P_in , P_out: sem_graph_params.
     273∀prog : joint_program P_in.
     274∀stack_sizes.
     275∀ f_lbls,f_regs.∀f_bl_r.∀init.
     276∀st_no_pc_rel,st_rel.
     277let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
     278let trans_prog  ≝ b_graph_transform_program P_in P_out init prog in
     279let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
     280good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs
     281                    st_no_pc_rel st_rel →
     282∀st1,st1' : joint_abstract_status prog_pars_in.
     283∀st2 : joint_abstract_status prog_pars_out.
     284∀f : ident.
     285∀fn : joint_closed_internal_function P_in ?.
     286∀has_tail,id,arg.
     287block_id … (pc_block (pc … st1)) ≠ -1 →
     288st_rel st1 st2 →
     289fetch_statement P_in ?
     290   (joint_globalenv P_in prog stack_sizes) (pc … st1) =
     291     return 〈f, fn, final … (TAILCALL P_in has_tail id arg)〉 →
     292 eval_state P_in …
     293  (joint_globalenv P_in prog stack_sizes) st1 = return st1' →
     294∃is_tail,st2_pre_call,t_is_tail.
     295as_tailcall_ident ? («st2_pre_call,t_is_tail») = as_tailcall_ident ? («st1, is_tail») ∧
     296∃st2_after_call,st2' : joint_abstract_status prog_pars_out.
     297∃taa2 : trace_any_any … st2 st2_pre_call.
     298∃taa2' : trace_any_any … st2_after_call st2'.
     299eval_state P_out … (joint_globalenv P_out trans_prog stack_sizes)
     300st2_pre_call = return st2_after_call ∧
     301st_rel st1' st2' ∧
     302as_label (joint_abstract_status prog_pars_in) st1' =
     303 as_label (joint_abstract_status prog_pars_out) st2_after_call.
     304#p_in #p_out #prog #stack_size #f_lbls #f_regs #init_regs #init #st_no_pc_rel #st_rel
     305#good #st1 #st1' #st2 #f #fn #has_tail #id #arg * #Hbl #Rst1st2 #EQfetch
     306whd in match eval_state in ⊢ (% → ?); normalize nodelta >EQfetch >m_return_bind
     307whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
     308whd in match eval_statement_advance; whd in match eval_tailcall; normalize nodelta
     309>set_no_pc_eta #H @('bind_inversion H) -H #bl #EQbl lapply(err_eq_from_io ????? EQbl)
     310-EQbl #EQbl #H @('bind_inversion H) -H
     311* #id1 * #fn1 #H lapply(err_eq_from_io ????? H) -H #EQfn1 normalize nodelta
     312[2: #H @('bind_inversion H) -H #x whd in match eval_external_call; normalize nodelta
     313    #H @('bind_inversion H) -H #y #_ #H @('bind_inversion H) -H #z #_
     314    #H @('bind_inversion H) -H #w whd in ⊢ (??%%→ ?); #ABS destruct(ABS) ]
     315whd in match (stack_sizes ????); #H lapply(err_eq_from_io ????? H) -H
     316#H @('bind_inversion H) -H #ssize_f #H lapply(opt_eq_from_res ???? H) -H #EQssize_f
     317#H @('bind_inversion H) -H #st1_fin whd in match eval_internal_call;
     318normalize nodelta whd in match (stack_sizes ????); #H @('bind_inversion H) -H
     319#ssize_f1 #H lapply(opt_eq_from_res ???? H) -H #EQssize_f1 #H @('bind_inversion H) -H
     320#st1_setup #EQst1_setup whd in ⊢ (??%% → ??%% → ?); #EQ1 #EQ2 destruct(EQ1 EQ2)
     321% [@hide_prf whd in ⊢ (??%?); >EQfetch %]
     322lapply(b_graph_transform_program_fetch_statement … good (pc … st1) f fn ?)
     323[2,4: @eqZb_elim [1,3: #ABS @⊥ >ABS in Hbl; #H @H %] #_ normalize nodelta
     324      #H cases(H EQfetch) -H |*:]
     325#data * #t_fn ** #EQt_fn #Hdata normalize nodelta ** #pre #instr * #Hregs *
     326#l1 * #mid ** #EQmid #EQpre whd in ⊢ (% → ?); #EQmid
     327cut(? : Prop)
     328[3: #EQint_fn1
     329    lapply(b_graph_transform_program_fetch_internal_function … good bl id1 fn1)
     330    @eqZb_elim [ #ABS cases(block_of_call_no_minus_one … EQbl) >ABS #H @⊥ @H % ]
     331    #_ normalize nodelta
     332    #H cases(H EQint_fn1) -H #data1 * #t_fn1 ** #EQt_fn1 #Hregs1 #good1
     333    cases(bind_new_bind_new_instantiates' … Hregs
     334    (bind_new_bind_new_instantiates' ?????? Hdata
     335     (tailcall_commutation ?????????? good ???????? EQfetch ? EQbl … EQint_fn1 …
     336       EQssize_f … EQssize_f1 … EQst1_setup … Rst1st2 … EQt_fn1))) [2: % assumption]
     337    #has_tail' * #id' * #arg' * #EQ destruct(EQ) * #st2_pre ** #EQst2_pre #EQt_bl
     338    * #st2_after * #EQst2_after #H cases(bind_new_bind_new_instantiates' … Hregs1 H)
     339    -H #st2' * #EQst2' #fin_sem_rel
     340|2: whd in match fetch_internal_function; normalize nodelta >EQfn1 %
     341|
     342]
     343%{(mk_state_pc ? st2_pre (pc_of_point p_out (pc_block … (pc … st2)) mid) (last_pop … st2))}
     344%
     345[ @hide_prf whd in ⊢ (??%?); whd in match fetch_statement; normalize nodelta
     346  <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) >EQt_fn >m_return_bind
     347  >point_of_pc_of_point >EQmid % ]
     348%
     349[ whd in ⊢ (??%%); >EQfetch in ⊢ (???(match % with [_ ⇒ ? | _ ⇒ ?]));
     350  whd in match fetch_statement; normalize nodelta
     351  <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in
     352     ⊢ (??(match % with [_ ⇒ ? | _ ⇒ ?])?);
     353  >EQt_fn in ⊢ (??(match % with [_ ⇒ ? | _ ⇒ ?])?);
     354  >m_return_bind in ⊢ (??(match % with [_ ⇒ ? | _ ⇒ ?])?);
     355  >point_of_pc_of_point in ⊢ (??(match % with [_ ⇒ ? | _ ⇒ ?])?);
     356  >EQmid in ⊢ (??(match % with [_ ⇒ ? | _ ⇒ ?])?); normalize nodelta
     357  >EQbl >EQt_bl >m_return_bind >m_return_bind >EQt_fn1 >EQint_fn1 %
     358]
     359%{(mk_state_pc ? (increment_stack_usage p_out ssize_f1 st2_after)
     360   (pc_of_point p_out bl (joint_if_entry … t_fn1)) (last_pop … st2))}
     361%{(mk_state_pc ? st2' (pc_of_point p_out bl (joint_if_entry … fn1)) (last_pop … st2))}
     362>(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in EQt_fn; #EQt_fn
     363>(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in EQpre; #EQpre
     364%{(taaf_to_taa … (produce_trace_any_any_free … st2 … EQt_fn … EQpre EQst2_pre) …)}
     365[ @if_elim #_ [2: @I] % whd in ⊢ (% → ?); * #H @H -H whd in ⊢ (??%?);
     366  whd in match fetch_statement; normalize nodelta >EQt_fn >m_return_bind
     367  >point_of_pc_of_point >EQmid % ]
     368cases good1 -good1 #_ #_ #_ #_ #_ #_ #_ #_ #_ cases(entry_is_cost … (pi2 ?? fn1))
     369#nxt1 * #c #EQin #H lapply(H … EQin) -H normalize nodelta >(f_step_on_cost … data1)
     370* #st_bl @eq_identifier_elim [2: * #H @⊥ @H % #_ ] #_
     371cases(added_prologue … data1) in EQst2';
     372[ whd in ⊢ (??%% → ?); #EQ destruct(EQ) normalize nodelta * whd in ⊢ (% → ?);
     373  inversion(f_regs ??) normalize nodelta [2: #x #y #_ #_ *] #EQregs #EQ destruct(EQ)
     374  * #l1 * #mid1 * #mid2 * #l2 *** #EQmid1 * #EQ1 #EQ2 destruct(EQ1 EQ2) *
     375  #nxt2 * #EQt_cost change with nxt2 in ⊢ (??%? → ?); #EQ destruct(EQ) *
     376  #EQ1 #EQ2 destruct(EQ1 EQ2) #EQentry >EQentry %{(taa_base …)}
     377| #hd #tl #EQst2' * normalize nodelta whd in ⊢ (% → ?); inversion(f_regs ??)
     378  [2: #x #y #_ #_ *] #EQregs normalize nodelta #EQ destruct(EQ) * #l1 * #mid1 * #mid2
     379  * #l2 *** #EQmid1 whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in ⊢ (% → ?);
     380  * #nxt2 * #EQnop change with nxt2 in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ⊢ (% → ?);
     381  * #EQ1 #EQ2 destruct(EQ1 EQ2) * #star * #_  whd in ⊢ (% → ?); * #l3 * #mid3 * #mid4
     382  * #l4 *** #_ * #EQ1 #EQ2 destruct(EQ1 EQ2) * #nxt2 * #EQt_cost
     383  change with nxt2 in ⊢ (??%? → ?); #EQ destruct(EQ) #EQl4
     384  letin trans_prog ≝ (b_graph_transform_program ????)
     385  lapply(taaf_to_taa …
     386   (produce_trace_any_any_free … (mk_prog_params p_out trans_prog stack_size)
     387    (mk_state_pc ? (increment_stack_usage p_out ssize_f1 st2_after)
     388     (pc_of_point p_out bl mid4) (last_pop … st2)) … EQt_fn1 … EQst2') ?)
     389  [4: >point_of_pc_of_point in ⊢ (????%???); assumption
     390  | @if_elim #_ [2: @I] % * #H @H -H whd in ⊢ (??%?); whd in match fetch_statement;
     391    normalize nodelta >EQt_fn1 >m_return_bind >point_of_pc_of_point >EQnop %
     392  |*:]
     393  #taa %{(taa_step … taa)}
     394  [ % * #H @H whd in ⊢ (??%?); whd in match fetch_statement; normalize nodelta
     395    >EQt_fn1 >m_return_bind >point_of_pc_of_point cases EQl4 #mid5 * #rest **
     396    #EQ destruct(EQ) * #nxt3 * #EQ #_ #_ >EQ %
     397  |2,3: whd [ whd in ⊢ (??%?); | whd in match eval_state; ]
     398    whd in match fetch_statement; normalize nodelta >EQt_fn1
     399    >m_return_bind >point_of_pc_of_point >EQt_cost [2: %] >m_return_bind %
     400  ]
     401]
     402%
     403[2,4: whd in ⊢ (??%%); whd in match (as_pc_of ??);  whd in match (as_pc_of ??);
     404      whd in match fetch_statement; normalize nodelta >EQint_fn1 >EQt_fn1
     405      >m_return_bind >m_return_bind whd in match point_of_pc; normalize nodelta
     406      >point_of_offset_of_point >point_of_offset_of_point >EQin >m_return_bind
     407      normalize nodelta >EQt_cost >m_return_bind normalize nodelta [ %]
     408      whd in match get_first_costlabel; normalize nodelta whd in ⊢ (??%%);
     409      whd in match (get_first_costlabel_next ???);
     410      generalize in match (refl ??);
     411      >EQin in ⊢ (∀e:???%. ???(??(???(match % return ? with [_ ⇒ ? | _ ⇒ ?]?))));
     412      #EQcost' normalize nodelta %
     413]
     414%
     415[1,3: whd in match eval_state; whd in match fetch_statement; normalize nodelta
     416      >EQt_fn >m_return_bind >point_of_pc_of_point >EQmid >m_return_bind
     417      whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
     418      whd in match eval_statement_advance; whd in match eval_tailcall;
     419      normalize nodelta >EQt_bl >m_return_bind @('bind_inversion EQt_fn1)
     420      * #id2 * #fn2 normalize nodelta #EQ whd in ⊢ (??%% → ?); #EQ1 destruct(EQ1)
     421      >EQ -EQ >m_return_bind normalize nodelta whd in match (stack_sizes ????);
     422      >EQssize_f >m_return_bind whd in match eval_internal_call; normalize nodelta
     423      whd in match (stack_sizes ????); >EQssize_f1 >m_return_bind >EQst2_after
     424      >m_return_bind [2: %] whd in match set_no_pc; normalize nodelta >EQentry %
     425|*: @(st_rel_def … good … fin_sem_rel …) [3,7: @EQint_fn1 |1,2,5,6:]
     426    @(fetch_stmt_ok_sigma_last_pop_ok … good … EQfetch) assumption
     427]
     428qed.
     429
     430lemma eval_tailcall_premain_ok : ∀ P_in , P_out: sem_graph_params.
     431∀prog : joint_program P_in.
     432∀stack_sizes.
     433∀ f_lbls,f_regs.∀f_bl_r.∀init.
     434∀st_no_pc_rel,st_rel.
     435let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
     436let trans_prog  ≝ b_graph_transform_program P_in P_out init prog in
     437let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
     438good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs
     439                    st_no_pc_rel st_rel →
     440∀st1,st1' : joint_abstract_status prog_pars_in.
     441∀st2 : joint_abstract_status prog_pars_out.
     442∀f : ident.
     443∀fn : joint_closed_internal_function P_in ?.
     444∀has_tail,id,arg.
     445block_id … (pc_block (pc … st1)) = -1 →
     446st_rel st1 st2 →
     447fetch_statement P_in ?
     448   (joint_globalenv P_in prog stack_sizes) (pc … st1) =
     449     return 〈f, fn, final … (TAILCALL P_in has_tail id arg)〉 →
     450 eval_state P_in …
     451  (joint_globalenv P_in prog stack_sizes) st1 = return st1' →
     452∃is_tail,st2_pre_call,t_is_tail.
     453as_tailcall_ident ? («st2_pre_call,t_is_tail») = as_tailcall_ident ? («st1, is_tail») ∧
     454∃st2_after_call,st2' : joint_abstract_status prog_pars_out.
     455∃taa2 : trace_any_any … st2 st2_pre_call.
     456∃taa2' : trace_any_any … st2_after_call st2'.
     457eval_state P_out … (joint_globalenv P_out trans_prog stack_sizes)
     458st2_pre_call = return st2_after_call ∧
     459st_rel st1' st2' ∧
     460as_label (joint_abstract_status prog_pars_in) st1' =
     461 as_label (joint_abstract_status prog_pars_out) st2_after_call.
     462#p_in #p_out #prog #stack_size #f_lbls #f_regs #init_regs #init #st_no_pc_rel
     463#st_rel #good #st1 #st1' #st2 #f #fn #has #id #arg #EQbl #Rst1st2 #EQfetch
     464#EQeval cases(pre_main_ok … good … EQbl EQeval Rst1st2) #Hclass * #st2' **
     465#Rst1st2' #EQst2' #Hlab % [ @hide_prf whd in ⊢ (??%?); >EQfetch %] %{st2}
     466% [ @hide_prf change with (joint_classify ???) in ⊢ (??%?); <Hclass
     467    whd in ⊢ (??%?); >EQfetch %]
     468%
     469[ letin trans_prog  ≝ (b_graph_transform_program p_in p_out init prog)
     470  cut(∃f',fn',has',id',arg'.
     471    fetch_statement p_out … (joint_globalenv p_out trans_prog stack_size)
     472     (pc … st2) = return 〈f',fn',final ?? (TAILCALL p_out has' id' arg')〉)
     473  [ lapply Hclass whd in ⊢ (??%? → ?); >EQfetch whd in match joint_classify_final;
     474    normalize nodelta whd in match joint_classify; normalize nodelta
     475    inversion (fetch_statement ????) [2: #e #_ normalize nodelta #EQ destruct(EQ)]
     476    ** #f' #fn' *
     477    [ * [ #c | #c_id #arg #dest | #r #lbl | #seq ] #nxt | * [ #lbl | | #has' #id' #arg' ] | *]
     478    #EQt_fetch normalize nodelta whd in ⊢ (???% → ?); #EQ destruct(EQ)
     479    %{f'} %{fn'} %{has'} %{id'} %{arg'} % ]
     480  * #f' * #fn' * #has' * #id' * #arg' #EQt_fetch
     481  @('bind_inversion EQeval) #x >EQfetch in ⊢ (% → ?); whd in ⊢ (??%% → ?);
     482  #EQ destruct(EQ) whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
     483  whd in match eval_statement_advance; whd in match eval_tailcall; normalize nodelta
     484  #H @('bind_inversion H) -H #bl #H lapply(err_eq_from_io ????? H) -H #EQbl
     485  #H @('bind_inversion H) -H * #f1 * #fn1 #H lapply(err_eq_from_io ????? H) -H
     486  #EQfn1 normalize nodelta
     487  [2: #H @('bind_inversion H) -H #st whd in match eval_external_call; normalize nodelta
     488    #H @('bind_inversion H) -H #x #_ #H @('bind_inversion H) -H #y #_
     489    #H @('bind_inversion H) -H #z whd in ⊢ (??%% → ?); #EQ destruct(EQ)
     490  ]
     491  #H lapply(err_eq_from_io ????? H) -H #H@('bind_inversion H) -H #f_ssize
     492  #H lapply(opt_eq_from_res ???? H) -H whd in match (stack_sizes ????); #EQf_ssize
     493  #H @('bind_inversion H) -H #st1_fin whd in match eval_internal_call; normalize nodelta
     494  #H @('bind_inversion H) -H #f1_ssize #H lapply(opt_eq_from_res ???? H) -H
     495  whd in match (stack_sizes ????); #EQf1_ssize #H @('bind_inversion H) -H
     496  #st1_setup #EQst1_setup whd in ⊢ (??%% → ??%% → ?); #EQ1 #EQ2 destruct(EQ1 EQ2)
     497  @('bind_inversion EQst2') #x >EQt_fetch in ⊢ (% → ?); whd in ⊢ (??%% → ?);
     498  #EQ destruct(EQ) whd in match eval_statement_no_pc; normalize nodelta
     499  >m_return_bind whd in match eval_statement_advance; whd in match eval_tailcall;
     500  normalize nodelta #H @('bind_inversion H) -H #bl' #H lapply(err_eq_from_io ????? H)
     501  -H #EQbl' #H @('bind_inversion H) -H * #f1' * #fn1' #H lapply(err_eq_from_io ????? H)
     502  -H #EQfn1' normalize nodelta
     503  [2: #H @('bind_inversion H) -H #st whd in match eval_external_call; normalize nodelta
     504    #H @('bind_inversion H) -H #x #_ #H @('bind_inversion H) -H #y #_
     505    #H @('bind_inversion H) -H #z whd in ⊢ (??%% → ?); #EQ destruct(EQ)
     506  ]
     507  #H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H #f_ssize'
     508  #H lapply(opt_eq_from_res ???? H) -H whd in match (stack_sizes ????); #EQf_ssize'
     509  #H @('bind_inversion H) -H #st2_fin whd in match eval_internal_call;
     510  normalize nodelta #H @('bind_inversion H) -H #f1_ssize' #H lapply(opt_eq_from_res ???? H)
     511  -H whd in match (stack_sizes ????); #EQf1_ssize' #H @('bind_inversion H) -H
     512  #st2_setup #EQst2_setup whd in ⊢ (??%% → ??%% → ?); #EQ1 #EQ2 destruct(EQ1 EQ2)
     513  whd in ⊢ (??%%); >EQfetch in ⊢ (???(match % with [ _ ⇒ ? | _ ⇒ ? ]));
     514      normalize nodelta >EQt_fetch in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? ])?);
     515     normalize nodelta >EQbl >EQbl' >m_return_bind >m_return_bind
     516     whd in match fetch_internal_function; normalize nodelta
     517     lapply(fetch_ok_pc_ok … good … Rst1st2' ?)
     518     [ whd in match fetch_internal_function; normalize nodelta >EQfn1 in ⊢ (??%?); %
     519     |*:
     520      ]
     521    whd in match pc_of_point in ⊢ (% → ?); normalize nodelta #EQ destruct(EQ)
     522    >EQfn1 >EQfn1' >m_return_bind >m_return_bind normalize nodelta
     523    lapply EQfn1 whd in match fetch_function; normalize nodelta
     524    @eqZb_elim [ #ABS @⊥ cases(block_of_call_no_minus_one …  EQbl) #H @H assumption]
     525    #Hbl' normalize nodelta #H lapply(opt_eq_from_res ???? H) -H #H @('bind_inversion H)
     526    #f2 #EQf2 #H @('bind_inversion H) -H #fn2 #_ whd in ⊢ (??%? → ?); -e0 -EQ
     527    #EQ destruct(EQ) -H lapply EQfn1' whd in match fetch_function; normalize nodelta
     528    @eqZb_elim [ #ABS >ABS in Hbl'; * #H @⊥ @H %] #_ normalize nodelta
     529    #H lapply(opt_eq_from_res ???? H) -H
     530    whd in match joint_globalenv in ⊢ (% → ?); normalize nodelta
     531    whd in match b_graph_transform_program in ⊢ (% → ?); normalize nodelta
     532    whd in match transform_joint_program; normalize nodelta
     533    >(symbol_for_block_transf ??? (λx.x) prog
     534      (λvars.transf_fundef ?? (λdef_in.b_graph_translate ??? (init ? def_in) def_in)) bl') in ⊢ (% → ?);
     535    >EQf2 >m_return_bind in ⊢ (% → ?); #H @('bind_inversion H) -H #fn2' #_
     536    whd in ⊢ (??%% → ?); #EQ destruct(EQ) %
     537]
     538%{st2'} %{st2'} %{(taa_base …)} %{(taa_base …)} % [2: assumption] %{EQst2' Rst1st2'}
     539qed.
     540 
     541
     542lemma eval_cond_ok : ∀ P_in , P_out: sem_graph_params.
    1309543∀prog : joint_program P_in.
    1310544∀stack_sizes.
     
    1332566∃ st2'. st_rel st1' st2' ∧
    1333567∃taf : trace_any_any_free (joint_abstract_status prog_pars_out) st2 st2'.
    1334 bool_to_Prop (taaf_non_empty … taf).
     568bool_to_Prop (taaf_non_empty … taf) ∧
     569as_label (joint_abstract_status prog_pars_in) st1' =
     570 as_label (joint_abstract_status prog_pars_out) st2'.
    1335571#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #st_no_pc_rel
    1336572#st_rel #goodR #st1 #st1' #st2 #f #fn #a #ltrue #lfalse * #Hbl #Rst1st2
     
    1362598#l1 * #mid1 * #mid2 * #l2 *** #EQmid1 whd in ⊢ (% → ?); #seq_pre_l whd in ⊢ (% → ?); * #nxt1
    1363599* #EQmid change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ)
    1364 cases(bind_new_bind_new_instantiates … EQbl (bind_new_bind_new_instantiates … Hinit
     600cases(bind_new_bind_new_instantiates' … EQbl (bind_new_bind_new_instantiates' … Hinit
    1365601               (cond_commutation … goodR … EQfetch EQbv EQbool Rst1st2 t_fn1 EQt_fn1)))
    1366602[2,4: % assumption]
     
    1396632      #H @H %
    1397633]
    1398 #taa_pre_mid %{(taaf_step_jump ? ??? taa_pre_mid ???) I}
    1399 [1,4: cases(fetch_stmt_ok_succ_ok … (pc … st1) (pc … st1') … EQfetch ?)
     634#taa_pre_mid %{(taaf_step_jump ? ??? taa_pre_mid ???)}
     635[1,5: cases(fetch_stmt_ok_succ_ok … (pc … st1) (pc … st1') … EQfetch ?)
    1400636      [2: @ltrue|3: %2 % % |4: % |6: @lfalse |7: % % |8: %] #stmt' #EQstmt'
    1401       whd <(as_label_ok_non_entry … goodR … EQstmt' H_fin)
    1402       [1,3: assumption
    1403       |2,4: cases(entry_unused … (pi2 ?? fn) … EQstmt)
     637      whd <(as_label_ok_non_entry … goodR … EQstmt' ? H_fin)
     638      [1,4: assumption
     639      |2,5: cases(entry_unused … (pi2 ?? fn) … EQstmt)
    1404640            [ whd in match stmt_forall_labels; whd in match stmt_labels;
    1405641              normalize nodelta #H cases(append_All … H) #_
     
    1412648              >point_of_offset_of_point %
    1413649            ]
     650      |*: % assumption
    1414651      ]
    1415 |2,5: whd whd in match (as_classify ??); whd in match fetch_statement; normalize nodelta
     652|2,6: whd whd in match (as_classify ??); whd in match fetch_statement; normalize nodelta
    1416653      >EQt_fn1 >m_return_bind >point_of_pc_of_point >EQmid normalize nodelta
    1417654      >EQt_cond %
    1418 |*: whd whd in match eval_state; whd in match fetch_statement; normalize nodelta
     655|3,7: whd whd in match eval_state; whd in match fetch_statement; normalize nodelta
    1419656    >EQt_fn1 >m_return_bind >point_of_pc_of_point >EQmid >m_return_bind >EQt_cond
    1420657    whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
     
    1423660    [ whd in match goto; normalize nodelta >(pc_of_label_eq … EQt_fn1)]
    1424661      >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 … EQfetch) %
    1425 ]
     662|*: %{I} cases(fetch_stmt_ok_succ_ok … (pc … st1') … EQfetch)
     663    [4,8: %
     664    |3: whd in match stmt_labels; normalize nodelta @Exists_append2
     665        whd in match stmt_explicit_labels; whd in match step_labels;
     666        normalize nodelta %1 //
     667    |7: @Exists_append1 %1 %
     668    |2,6:
     669    ]
     670    #stmt' #EQstmt' @(as_label_ok_non_entry … goodR)
     671    [4,11: @EQstmt'
     672    |1,2,3,8,9,10:
     673    |5,12: % assumption
     674    |6,13: assumption
     675    |*: cases(entry_unused ??? (pi2 ?? fn) ?? (proj2 ?? (fetch_statement_inv … EQfetch)))
     676        [ * #_ ** whd in match (point_of_label ????); #H #_ #_ % #H1 @H <H1
     677          >point_of_pc_of_point %
     678        | ** whd in match (point_of_label ????); #H #_ #_ % #H1 @H <H1
     679          >point_of_pc_of_point %
     680        ]
     681    ]
     682]
     683qed.
     684
     685lemma eval_cond_premain_ok : ∀ P_in , P_out: sem_graph_params.
     686∀prog : joint_program P_in.
     687∀stack_sizes.
     688∀ f_lbls,f_regs.∀f_bl_r.∀init.
     689∀st_no_pc_rel,st_rel.
     690let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
     691let trans_prog  ≝ b_graph_transform_program P_in P_out init prog in
     692let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
     693good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs
     694                    st_no_pc_rel st_rel →
     695∀st1,st1' : joint_abstract_status prog_pars_in.
     696∀st2 : joint_abstract_status prog_pars_out.
     697∀f : ident.
     698∀fn : joint_closed_internal_function P_in ?.
     699∀a,ltrue,lfalse.
     700block_id … (pc_block (pc … st1)) = -1 →
     701st_rel st1 st2 →
     702 let cond ≝ (COND P_in ? a ltrue) in
     703  fetch_statement P_in ?
     704   (joint_globalenv P_in prog stack_sizes) (pc … st1) =
     705     return 〈f, fn, sequential … cond lfalse〉 →
     706 eval_state P_in …
     707  (joint_globalenv P_in prog stack_sizes) st1 = return st1' →
     708as_costed (joint_abstract_status prog_pars_in) st1' →
     709∃ st2'. st_rel st1' st2' ∧
     710∃taf : trace_any_any_free (joint_abstract_status prog_pars_out) st2 st2'.
     711bool_to_Prop (taaf_non_empty … taf) ∧
     712as_label (joint_abstract_status prog_pars_in) st1' =
     713 as_label (joint_abstract_status prog_pars_out) st2'.
     714#p_in #p_out #prog #stack_size #f_lbls #f_regs #init_regs #init #st_no_pc_rel
     715#st_rel #good #st1 #st1' #st2 #f #fn #a #ltrue #lfalse #EQbl #Rst1st2 #EQfetch
     716#EQeval cases(pre_main_ok … good …  EQbl EQeval Rst1st2) #Hclass  * #st2'
     717** #Rst1st2' #EQst2' #Hlab whd in ⊢ (% → ?); * #ncost %{st2'} %{Rst1st2'}
     718%{(taaf_step_jump … (taa_base …) …)}
     719[ whd <Hlab % assumption
     720| whd change with (joint_classify ???) in ⊢ (??%?); <Hclass
     721  whd in match joint_classify; normalize nodelta >EQfetch %
     722| assumption
     723]
     724%{I} assumption
    1426725qed.
    1427726
     
    1453752 if taaf_non_empty … taf then True else  (*IT CAN BE SIMPLIFIED *)
    1454753(¬as_costed (joint_abstract_status (mk_prog_params P_in prog stack_sizes)) st1 ∨
    1455  ¬as_costed (joint_abstract_status (mk_prog_params P_in prog stack_sizes)) st1').
     754 ¬as_costed (joint_abstract_status (mk_prog_params P_in prog stack_sizes)) st1') ∧
     755as_label (joint_abstract_status prog_pars_in) st1' =
     756 as_label (joint_abstract_status prog_pars_out) st2'. 
    1456757#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #st_no_pc_rel #st_rel
    1457758#goodR #st1 #st1' #st2 #f #fn #stmt #nxt * #Hbl #Rst1st2 #EQfetch #EQeval
     
    1474775#_ <(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) #EQbl
    1475776>(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) #SBiC
    1476 cases(bind_new_bind_new_instantiates … EQbl (bind_new_bind_new_instantiates … Hinit
     777cases(bind_new_bind_new_instantiates' … EQbl (bind_new_bind_new_instantiates' … Hinit
    1477778               (seq_commutation … goodR … EQfetch EQeval Rst1st2 t_fn EQt_fn)))
    1478779               [2: % assumption]
     
    1480781%{(mk_state_pc ? st2_fin_no_pc (pc_of_point P_out (pc_block (pc … st2)) nxt) (last_pop … st2))}
    1481782cases(fetch_statement_inv … EQfetch) >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch)
    1482 #EQfn #_
    1483 %
    1484 [ @(st_rel_def ?????????? goodR … f fn)
     783#EQfn #_ cut(? : Prop) [3: #Hfin % [@Hfin] |1:
     784| @(st_rel_def ?????????? goodR … f fn)
    1485785      [ change with (pc_block (pc … st2)) in match (pc_block ?); assumption
    1486786      | <(fetch_stmt_ok_sigma_pc_ok … goodR … EQfetch) assumption
     
    1490790%{(produce_trace_any_any_free_coerced ? st2 f t_fn l ?? st2_fin_no_pc EQt_fn
    1491791                                      SBiC EQst2_fin_no_pc)}
    1492 @if_elim #_ [@I] % % whd in ⊢ (% → ?); * #H @H -H whd in ⊢ (??%?); >EQfetch %
     792% [ @if_elim #_ [@I] % % whd in ⊢ (% → ?); * #H @H -H whd in ⊢ (??%?); >EQfetch % ]
     793cases(fetch_stmt_ok_succ_ok … nxt … EQfetch) [4: % |3: % % |2:]
     794#stmt' #EQstmt'  @(as_label_ok_non_entry … goodR)
     795[4: <(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) in ⊢ (??%?); @EQstmt'
     796|1,2,3:
     797| % <(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) assumption
     798| assumption
     799| cases(entry_unused ??? (pi2 ?? fn) ?? (proj2 ?? (fetch_statement_inv … EQfetch)))
     800  * whd in match (point_of_label ????); * #H #_ #_ % #H1 @H <H1 whd in match succ_pc;
     801  whd in match point_of_pc; whd in match pc_of_point; normalize nodelta
     802  >point_of_offset_of_point %
     803]
    1493804qed.
    1494805
     806lemma general_eval_seq_no_call_premain_ok :∀ P_in , P_out: sem_graph_params.
     807∀prog : joint_program P_in.
     808∀stack_sizes.
     809∀ f_lbls,f_regs.∀f_bl_r.∀init.
     810∀st_no_pc_rel,st_rel.
     811let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
     812let trans_prog  ≝ b_graph_transform_program P_in P_out init prog in
     813let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
     814good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs
     815                    st_no_pc_rel st_rel →
     816∀st1,st1' : joint_abstract_status prog_pars_in.
     817∀st2 : joint_abstract_status prog_pars_out.
     818∀f.∀fn : joint_closed_internal_function P_in ?.
     819∀stmt,nxt.
     820block_id … (pc_block (pc … st1)) = -1 →
     821st_rel st1 st2 →
     822 let seq ≝ (step_seq P_in ? stmt) in
     823  fetch_statement P_in …
     824   (joint_globalenv P_in prog stack_sizes) (pc … st1) =
     825     return 〈f, fn,  sequential ?? seq nxt〉 →
     826 eval_state P_in … (joint_globalenv P_in prog stack_sizes)
     827  st1 = return st1' →
     828∃st2'. st_rel st1' st2' ∧           
     829∃taf : trace_any_any_free (joint_abstract_status prog_pars_out) st2 st2'.           
     830bool_to_Prop (taaf_non_empty … taf) ∧
     831as_label (joint_abstract_status prog_pars_in) st1' =
     832 as_label (joint_abstract_status prog_pars_out) st2'.
     833#p_in #p_out #prog #stack_size #f_lbls #f_regs #init_regs #init #st_no_pc_rel
     834#st_rel #good #st1 #st1' #st2 #f #fn #stmt #nxt #EQbl #Rst1st2 #EQfetch
     835#EQeval cases(pre_main_ok … good …  EQbl EQeval Rst1st2) #Hclass * #st2'
     836** #Rst1st2' #EQst2' #Hlab %{st2'} %{Rst1st2'} %{(taaf_step … (taa_base …) …)}
     837[ whd change with (joint_classify ???) in ⊢ (??%?); <Hclass whd in match joint_classify;
     838  normalize nodelta >EQfetch %
     839| assumption
     840]
     841%{I} assumption
     842qed.
    1495843
    1496844lemma general_eval_cost_ok :
     
    1521869        (joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes))
    1522870        st2 st2'.
    1523 bool_to_Prop (taaf_non_empty … taf).
     871bool_to_Prop (taaf_non_empty … taf) ∧
     872as_label (joint_abstract_status prog_pars_in) st1' =
     873 as_label (joint_abstract_status prog_pars_out) st2'.
    1524874#P_in #P_out #prog #stack_size #f_lbls #f_regs #f_bl_r #init #st_no_pc_rel
    1525875#st_rel #goodR #st1 #st1' #st2 #f #fn #c #nxt * #Hbl #Rst1st2 normalize nodelta
     
    1529879#EQ destruct(EQ)
    1530880%{(mk_state_pc ? (st_no_pc … st2) (pc_of_point P_out (pc_block (pc … st2)) nxt)
    1531                  (last_pop … st2))} %
    1532 [ cases(fetch_statement_inv … EQfetch) #EQfn #_
     881                 (last_pop … st2))}
     882cut(? : Prop) [3: #Hfin % [@Hfin] |
     883| cases(fetch_statement_inv … EQfetch) #EQfn #_
    1533884  <(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch)
    1534885  whd in match (succ_pc ???); whd in match (point_of_succ ???);
     
    1540891  | @(fetch_stmt_ok_sigma_last_pop_ok … goodR … Rst1st2 EQfetch)
    1541892  ]
    1542 | lapply(b_graph_transform_program_fetch_statement … goodR (pc … st1) f fn ?)
     893]
     894lapply(b_graph_transform_program_fetch_statement … goodR (pc … st1) f fn ?)
    1543895  [2: @eqZb_elim [ #ABS @⊥ >ABS in Hbl; #H @H %] #_ normalize nodelta
    1544896      #H cases(H EQfetch) -H |*:]
     
    1564916  ] 
    1565917  %{(taaf_step … (taa_base …) …)}
    1566   [3,6,9: @I
     918  [3,6,9: %{I}
    1567919  |*: whd whd in ⊢ (??%?); whd in match fetch_statement; normalize nodelta
    1568920     >EQt_fn >m_return_bind >EQt_stmt >m_return_bind %
    1569921  ]
     922cases(fetch_stmt_ok_succ_ok … nxt … EQfetch) [4,8,12: % |2,6,10: |3,7,11: % %]
     923#stmt' #EQstmt'  @(as_label_ok_non_entry … goodR)
     924[4,11,18: @EQstmt'
     925|1,2,3,8,9,10,15,16,17:
     926|5,12,19: % assumption
     927|6,13,20: assumption
     928|*: cases(entry_unused ??? (pi2 ?? fn) ?? (proj2 ?? (fetch_statement_inv … EQfetch)))
     929  * whd in match (point_of_label ????); * #H #_ #_ % #H1 @H <H1 whd in match succ_pc;
     930  whd in match point_of_pc; whd in match pc_of_point; normalize nodelta
     931  >point_of_offset_of_point %
    1570932]
    1571933qed.
    1572934
    1573 lemma next_of_call_pc_error : ∀pars.∀prog. ∀stack_size,pc.
    1574 block_id (pi1 … (pc_block pc)) = 0→
    1575 next_of_call_pc pars … (ev_genv … (mk_prog_params pars prog stack_size))
    1576   pc = Error ? [MSG BadFunction].
    1577 #pars #prg #init #pc #EQ whd in match next_of_call_pc; normalize nodelta
    1578 whd in match fetch_statement; normalize nodelta
    1579 >fetch_internal_function_no_zero //
     935lemma general_eval_cost_premain_ok :
     936∀ P_in , P_out: sem_graph_params.
     937∀prog : joint_program P_in.
     938∀stack_sizes.
     939∀ f_lbls,f_regs.∀f_bl_r.∀init.
     940∀st_no_pc_rel,st_rel.
     941let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
     942let trans_prog  ≝ b_graph_transform_program P_in P_out init prog in
     943let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
     944good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs
     945                    st_no_pc_rel st_rel →
     946∀st1,st1' : joint_abstract_status prog_pars_in.
     947∀st2 : joint_abstract_status prog_pars_out.
     948∀f.
     949∀fn : joint_closed_internal_function P_in ?.∀c,nxt.
     950block_id … (pc_block (pc … st1)) = -1 →
     951st_rel st1 st2 →
     952let cost ≝ COST_LABEL P_in ? c in
     953 fetch_statement P_in …
     954  (joint_globalenv P_in prog stack_sizes) (pc … st1) =
     955    return 〈f, fn,  sequential ?? cost nxt〉 →
     956 eval_state P_in … (ev_genv … prog_pars_in)
     957            st1 = return st1' →
     958∃ st2'. st_rel st1' st2' ∧
     959∃taf : trace_any_any_free
     960        (joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes))
     961        st2 st2'.
     962bool_to_Prop (taaf_non_empty … taf) ∧
     963as_label (joint_abstract_status prog_pars_in) st1' =
     964 as_label (joint_abstract_status prog_pars_out) st2'.
     965#p_in #p_out #prog #stack_size #f_lbls #f_regs #init_regs #init #st_no_pc_rel #st_rel
     966#good #st1 #st1' #st2 #f #fn #c #nxt #EQbl #Rst1st2 #EQfetch #EQeval
     967cases(pre_main_ok … good …  EQbl EQeval Rst1st2) #Hclass * #st2'
     968** #Rst1st2' #EQst2' #Hlab %{st2'} %{Rst1st2'} %{(taaf_step … (taa_base …) …)}
     969[ whd change with (joint_classify ???) in ⊢ (??%?); <Hclass
     970  whd in match joint_classify; normalize nodelta >EQfetch %
     971| assumption
     972]
     973%{I} assumption
    1580974qed.
    1581975
     
    1598992∀p_in,p_out,prog,stack_size,init,init_regs,f_lbls,f_regs,pc,pc'.
    1599993sigma_pc_opt p_in p_out prog stack_size init init_regs f_lbls f_regs pc ≠ None ? →
     994block_id (pc_block pc) ≠ OZ →
    1600995sigma_stored_pc p_in p_out prog stack_size init init_regs f_lbls f_regs pc =
    1601996sigma_stored_pc p_in p_out prog stack_size init init_regs f_lbls f_regs pc' →
    1602997pc = pc'.
    1603 #p_in #p_out #prog #stack_size #init #init_regs #f_lbls #f_regs #pc #pc' #H
     998#p_in #p_out #prog #stack_size #init #init_regs #f_lbls #f_regs #pc #pc' #H *#H1
    1604999whd in match sigma_stored_pc; normalize nodelta
    1605 inversion(sigma_pc_opt ?????????) [ #ABS >ABS in H; * #H @⊥ @H %] #pc1 #EQpc1
     1000 inversion(sigma_pc_opt ?????????) [ #ABS >ABS in H; * #H @⊥ @H %] #pc1 #EQpc1
    16061001normalize nodelta inversion(sigma_pc_opt ?????????)
    1607 [ #ABS normalize nodelta #EQ destruct(EQ) lapply EQpc1; whd in match sigma_pc_opt;
    1608   normalize nodelta @eqZb_elim
    1609   [ #ABS1 whd in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ABS1 : (??%%); destruct]
     1002[ #ABS normalize nodelta #EQ destruct(EQ) lapply EQpc1 whd in match sigma_pc_opt;
     1003  normalize nodelta @if_elim
     1004  [ #Hbl whd in ⊢ (??%? → ?); #EQ destruct(EQ) lapply(Hbl) -Hbl @eqZb_elim
     1005    [whd in ⊢ (??%% → ?); #EQ destruct(EQ)] @eqZb_elim [#ABS >ABS in H1; #H @⊥ @H %]
     1006    @⊥ @H1 %]
    16101007  #Hbl normalize nodelta #H @('bind_inversion H) -H #lbl whd in match sigma_label;
    16111008  normalize nodelta >code_block_of_block_eq >m_return_bind
     
    16171014[ assumption] >EQpc1 >EQpc2 %
    16181015qed.
    1619 
    1620 
    1621 
    1622 
    16231016
    16241017lemma eval_return_ok :
     
    16501043as_classifier … st2_ret cl_return ∧
    16511044        as_execute … st2_ret st2_after_ret ∧ st_rel st1' st2' ∧
    1652         ret_rel ?? (JointStatusSimulation … good) st1' st2_after_ret.
     1045        ret_rel ?? (JointStatusSimulation … good) st1' st2_after_ret ∧
     1046as_label (joint_abstract_status prog_pars_in) st1' =
     1047 as_label (joint_abstract_status prog_pars_out) st2'.
    16531048#p_in #p_out #prog #stack_size #f_lbls #f_regs #init_regs #init #st_no_pc_rel
    16541049#st_rel #good #st1 #st1' #st2 #f #fn #Hbl #Rst1st2 #EQfetch
     
    16691064cases(next_of_call_pc_inv … EQnext_of_call) #f1 * #fn1 * #id * #args * #dest #EQcall
    16701065<(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in Hregs; #Hregs
    1671 cases(bind_new_bind_new_instantiates … Hregs (bind_new_bind_new_instantiates … Hinit
     1066cases(bind_new_bind_new_instantiates' … Hregs (bind_new_bind_new_instantiates' … Hinit
    16721067 (return_commutation ?????????? good … Hbl EQfetch … EQssize … EQpop … EQcall …
    16731068   Rst1st2 t_fn EQt_fn))) #EQ destruct(EQ) * #st_fin * #EQst_fin * #t_st_pop * #t_pc_pop
    16741069** #EQt_pop #EQt_pc_pop @eqZb_elim #Hbl_pcpop normalize nodelta
    1675 [ #sem_rel (*premain case TODO *) cases daemon ]
     1070[ * #sem_rel #EQt_next
     1071  %{(mk_state_pc ? st_fin (pc_of_point p_out (pc_block (pc … st2)) mid) (last_pop … st2))}
     1072  %{(mk_state_pc ? (decrement_stack_usage p_out ssize t_st_pop)
     1073      (pc_of_point p_out (pc_block t_pc_pop) next_of_call) t_pc_pop)}
     1074  %{(mk_state_pc ? (decrement_stack_usage p_out ssize t_st_pop)
     1075      (pc_of_point p_out (pc_block t_pc_pop) next_of_call) t_pc_pop)}
     1076  %{((taaf_to_taa …
     1077     (produce_trace_any_any_free ? st2 f t_fn … EQt_fn EQpre EQst_fin) ?))}
     1078 [ @if_elim #_ [2: @I] % * #H @H -H whd in ⊢ (??%?); whd in match fetch_statement;
     1079 normalize nodelta >EQt_fn >m_return_bind >point_of_pc_of_point >EQt_stmt % ]
     1080 %{(taaf_base …)} cut(? : Prop)
     1081 [3: #Hfin % [ %
     1082 [ % [ % [%{I} ]
     1083       whd [whd in ⊢ (??%?); | whd in match eval_state;] whd in match fetch_statement;
     1084       normalize nodelta >EQt_fn >m_return_bind >point_of_pc_of_point >EQt_stmt [%]
     1085       >m_return_bind whd in match eval_statement_no_pc; normalize nodelta
     1086       >m_return_bind whd in match eval_statement_advance; whd in match eval_return;
     1087       normalize nodelta whd in match (stack_sizes ????); >EQssize >m_return_bind
     1088       >EQt_pop >m_return_bind >EQt_next >m_return_bind %
     1089     | @Hfin
     1090     ]
     1091 | whd * #s1_pre #s1_call cases (joint_classify_call … s1_call) * #calling_i
     1092   #calling * #id1 * #arg1 * #dest1 * #nxt' #EQfetch_call * #s2_pre #s2_call
     1093   whd in ⊢ (% → ?); >EQfetch_call normalize nodelta * #EQ destruct(EQ)
     1094   whd in ⊢ (??%% → ?); whd in match (point_of_succ ???);
     1095   whd in match (point_of_succ ???); #EQ cut(next_of_call =nxt')
     1096   [ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) cases next_of_call in e0; #x
     1097     normalize nodelta whd in match (offset_of_point ??); cases nxt' #y
     1098     normalize nodelta #EQ1 destruct(EQ1) % ]
     1099   -EQ #EQ destruct(EQ) whd in ⊢ (% → ?); <EQt_pc_pop #EQ1
     1100     lapply(stored_pc_inj … EQ1)
     1101     [2: % #ABS cases(fetch_statement_inv … EQcall) <EQt_pc_pop
     1102       >fetch_internal_function_no_zero [#EQ destruct] whd in match sigma_stored_pc;
     1103       normalize nodelta >ABS %
     1104     | % #ABS cases(next_of_call_pc_inv … EQt_next) #x * #y * #z * #w * #a
     1105       whd in match fetch_statement; normalize nodelta >fetch_internal_function_no_zero
     1106       [whd in ⊢ (??%% → ?); #EQ destruct(EQ) ] assumption
     1107     ] #EQ2 destruct(EQ2) whd
     1108     cases(next_of_call_pc_inv … EQt_next) #id'' * #fn'' * #c_id'' * #c_args''
     1109     * #c_dest'' #EQ3 >EQ3 normalize nodelta % [%] % ] ]
     1110  |2:  whd in match succ_pc; normalize nodelta whd in match (point_of_succ ???);
     1111       destruct(EQt_pc_pop) lapply(proj1 ?? (fetch_statement_inv … EQcall))
     1112       <pc_block_eq in Hbl_pcpop sem_rel ⊢ %;
     1113       [2: % #H cases(fetch_statement_inv … EQcall) >fetch_internal_function_no_zero
     1114       [ #EQ destruct] whd in match sigma_stored_pc; normalize nodelta >H %]
     1115       #Hbl_pcpop #sem_rel #EQ @(st_rel_def … good … sem_rel … ) [3: @EQ |1,2:] %
     1116  |
     1117  ]
     1118 cases(fetch_stmt_ok_succ_ok … next_of_call … EQcall) [4: % |3: % % |2:]
     1119 #stmt' #EQstmt' cases(decidable_eq_Z (block_id (pc_block pc_pop)) (neg one))
     1120 [ #Hbl @(as_label_premain_ok ?????????? good) [assumption | assumption ]
     1121 | #Hbl_pc_pop @(as_label_ok_non_entry … good)
     1122   [4: @EQstmt'
     1123   |1,2,3:
     1124   | assumption
     1125   | assumption
     1126   |  cases(entry_unused ??? (pi2 ?? fn1) ?? (proj2 ?? (fetch_statement_inv … EQcall)))
     1127     * whd in match (point_of_label ????); * #H #_ #_ % >point_of_pc_of_point
     1128     #H1 @H <H1 %
     1129   ]
     1130 ]
     1131]   
    16761132cases(fetch_statement_sigma_stored_pc … good … Hbl_pcpop … EQcall) #data1 * #Hinit1
    16771133normalize nodelta *** #pre_c #instr_c #post_c * #Hregs1 * #pc1 * destruct(EQt_pc_pop)
     
    16901146  cases(fetch_statement_inv … EQcall) #_ normalize nodelta >ABS #EQ destruct(EQ) ]
    16911147#_ cut(∀x : bool.andb x false = false) [* %] #EQ >EQ -EQ normalize nodelta ***
    1692 cases(bind_new_bind_new_instantiates … (bind_instantiates_to_instantiate … Hregs1)
    1693  (bind_new_bind_new_instantiates … (bind_instantiates_to_instantiate … Hinit1)
     1148cases(bind_new_bind_new_instantiates' … (bind_instantiates_to_instantiate … Hregs1)
     1149 (bind_new_bind_new_instantiates' … (bind_instantiates_to_instantiate … Hinit1)
    16941150  ((call_is_call … good … (proj1 … (fetch_statement_inv … EQcall))) id args dest ?)) (point_of_pc p_in pc1))
    16951151#id' * #args' * #dest' #EQ >EQ -EQ #EQt_call #EQpre_c #EQpost_c #EQnxt1 #H
    1696 cases(bind_new_bind_new_instantiates … (bind_instantiates_to_instantiate … Hregs1)
    1697       (bind_new_bind_new_instantiates … (bind_instantiates_to_instantiate … Hinit1) H))
     1152cases(bind_new_bind_new_instantiates' … (bind_instantiates_to_instantiate … Hregs1)
     1153      (bind_new_bind_new_instantiates' … (bind_instantiates_to_instantiate … Hinit1) H))
    16981154-H #st2' * #EQst2' #fin_sem_rel
    16991155%{(mk_state_pc ? st_fin (pc_of_point p_out (pc_block (pc … st2)) mid) (last_pop … st2))}
     
    17181174|*:
    17191175]
    1720 %
    1721 [ %
     1176cut(? : Prop)
     1177[3: #Hfin %
    17221178  [ %
    17231179    [ %
    1724       [ @if_elim [2: #_ @I] #H lapply(prf H) cases post_c in EQpost_c; [#_ *]
    1725         #hd #tl whd in ⊢ (% → ?); * #lab * #rest ** #EQ destruct(EQ) *
    1726         #succ * #EQnxt1 change with succ in ⊢ (??%? → ?); #EQ destruct(EQ)
    1727         #EQrest #_ % whd in ⊢ (% → ?); whd in match (as_label ??);
    1728         whd in match (as_pc_of ??); whd in match (point_of_succ ???);
    1729         change with (pc_block pc1) in match (pc_block ?);
    1730         whd in match fetch_statement; normalize nodelta
    1731         >(proj1 … (fetch_statement_inv … EQt_call)) >m_return_bind
    1732         whd in match point_of_pc; normalize nodelta >point_of_offset_of_point
    1733         >EQnxt1 >m_return_bind normalize nodelta whd in match cost_label_of_stmt;
    1734         normalize nodelta * #H @H % ]
     1180      [2: @Hfin
     1181      | %
     1182        [ %
     1183          [ @if_elim [2: #_ @I] #H lapply(prf H) cases post_c in EQpost_c; [#_ *]
     1184            #hd #tl whd in ⊢ (% → ?); * #lab * #rest ** #EQ destruct(EQ) *
     1185            #succ * #EQnxt1 change with succ in ⊢ (??%? → ?); #EQ destruct(EQ)
     1186            #EQrest #_ % whd in ⊢ (% → ?); whd in match (as_label ??);
     1187            whd in match (as_pc_of ??); whd in match (point_of_succ ???);
     1188            change with (pc_block pc1) in match (pc_block ?);
     1189            whd in match fetch_statement; normalize nodelta
     1190            >(proj1 … (fetch_statement_inv … EQt_call)) >m_return_bind
     1191            whd in match point_of_pc; normalize nodelta >point_of_offset_of_point
     1192            >EQnxt1 >m_return_bind normalize nodelta whd in match cost_label_of_stmt;
     1193            normalize nodelta * #H @H % ]
    17351194    ]
    17361195    whd [ whd in match (as_classify ??); | whd in match eval_state; normalize nodelta]
     
    17411200    >EQssize >m_return_bind >EQt_pop >m_return_bind whd in match next_of_call_pc;
    17421201    normalize nodelta >EQt_call >m_return_bind %
    1743   | whd in match succ_pc; normalize nodelta <(pc_block_eq) [2: >EQpc2 % #EQ destruct]
    1744     whd in match (point_of_succ ???); @(st_rel_def … good)
     1202    ]
     1203  ]
     1204]
     1205|
     1206| whd in match succ_pc; normalize nodelta <(pc_block_eq) [2: >EQpc2 % #EQ destruct]
     1207    whd in match (point_of_succ ???); @(st_rel_def … good)
    17451208    [3: change with (pc_block pc1) in match (pc_block ?);
    17461209        lapply(proj1 ?? (fetch_statement_inv … EQcall)) <pc_block_eq in ⊢ (% → ?);
     
    17511214    ]
    17521215  ]
    1753 ]   
    1754 whd * #s1_pre #s1_call cases (joint_classify_call … s1_call) * #calling_i
    1755 #calling * #call_spec * #arg * #dest * #nxt' #EQfetch_call * #s2_pre #s2_call
     1216[ whd * #s1_pre #s1_call cases (joint_classify_call … s1_call) * #calling_i 
     1217  #calling * #call_spec * #arg * #dest * #nxt' #EQfetch_call * #s2_pre #s2_call
    17561218whd in ⊢ (% → ?); >EQfetch_call normalize nodelta * #EQpc1_pc_s1_pre  #EQsucc_pc
    17571219whd in ⊢ (% → ?); #EQpc_s1_pre >EQpc_s1_pre in EQfetch_call; #EQfetch_call
     
    17601222#data2 * #EQdata2 normalize nodelta * #bl2 * #EQbl2 * #pc3 * #EQstored
    17611223lapply(stored_pc_inj … (sym_eq ??? EQstored))
    1762 [ % #ABS cases(fetch_statement_inv … EQfetch_call) >fetch_internal_function_no_zero
    1763   [ #EQ destruct(EQ)] whd in match sigma_stored_pc; normalize nodelta >ABS % ]
     1224[2: % #ABS cases(fetch_statement_inv … EQfetch_call) >fetch_internal_function_no_zero
     1225  [ #EQ destruct(EQ)] whd in match sigma_stored_pc; normalize nodelta >ABS %
     1226| % #ABS cases(fetch_statement_inv … EQfetch_call) >fetch_internal_function_no_zero
     1227  [2: <pc_block_eq [assumption] % #ABS1 cases(fetch_statement_inv … EQfetch_call)
     1228      whd in match sigma_stored_pc; normalize nodelta >ABS1
     1229      >fetch_internal_function_no_zero [2: %]  ] whd in ⊢ (??%% → ?); #EQ destruct
     1230]
    17641231#EQ destruct(EQ) * #fn' * #nxt'' * #l1 * #l2 @eq_identifier_elim
    17651232[ #EQentry cases(fetch_statement_inv … EQfetch_call) #_ >EQentry normalize nodelta
     
    17711238|2: @(stored_pc_inj p_in p_out prog stack_size init init_regs f_lbls f_regs … )
    17721239  [ % #ABS cases(fetch_statement_inv … EQcall) >fetch_internal_function_no_zero
    1773    [#EQ destruct] whd in match sigma_stored_pc; normalize nodelta >ABS % ]
    1774  >EQpc1_pc_s1_pre assumption
     1240   [#EQ destruct] whd in match sigma_stored_pc; normalize nodelta >ABS %
     1241  |3: >EQpc1_pc_s1_pre assumption
     1242  | % #ABS cases(fetch_statement_inv … EQt_call) >fetch_internal_function_no_zero
     1243    [2: assumption] #EQ destruct
     1244  ]
    17751245|]
    17761246destruct(H)
     
    17841254#EQ destruct(EQ) >EQcall in EQfetch_call; >EQt_call in EQt_fetch_call;
    17851255whd in ⊢ (? → ??%? → ?); #EQ1 #EQ2 lapply(eq_to_jmeq ??? EQ1) -EQ1 #EQ1 destruct(EQ1) %
     1256]
     1257cases(fetch_stmt_ok_succ_ok … next_of_call … EQcall) [4: % |3: % % |2:]
     1258 #stmt' #EQstmt' cases(decidable_eq_Z (block_id (pc_block pc1)) (neg one))
     1259 [ #Hbl  @(as_label_premain_ok ?????????? good)
     1260   [ change with (pc_block (sigma_stored_pc ?????????)) in match (pc_block ?);
     1261     <pc_block_eq [ assumption] % #ABS cases(fetch_statement_inv … EQstmt')
     1262     >fetch_internal_function_no_zero [#EQ destruct] whd in match sigma_stored_pc;
     1263     normalize nodelta >ABS %
     1264   | assumption
     1265   ]
     1266 | #Hbl_pc_pop @(as_label_ok_non_entry … good)
     1267   [4: @EQstmt'
     1268   |1,2,3:
     1269   | assumption
     1270   | assumption
     1271   |  cases(entry_unused ??? (pi2 ?? fn1) ?? (proj2 ?? (fetch_statement_inv … EQcall)))
     1272     * whd in match (point_of_label ????); * #H #_ #_ % >point_of_pc_of_point
     1273     #H1 @H <H1 %
     1274   ]
     1275]
    17861276qed.
    17871277
     1278lemma eval_call_ok : ∀ P_in , P_out: sem_graph_params.
     1279∀prog : joint_program P_in.
     1280∀stack_size.
     1281∀ f_lbls,f_regs.∀init_regs.∀init.
     1282∀st_no_pc_rel,st_rel.
     1283let prog_pars_in ≝ mk_prog_params P_in prog stack_size in
     1284let trans_prog  ≝ b_graph_transform_program P_in P_out init prog in
     1285let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_size in
     1286∀good : good_state_relation P_in P_out prog stack_size init init_regs f_lbls f_regs
     1287                    st_no_pc_rel st_rel.
     1288∀st1,st1' : joint_abstract_status prog_pars_in.
     1289∀st2 : joint_abstract_status prog_pars_out.
     1290∀f.
     1291∀fn : joint_closed_internal_function P_in ?.
     1292∀id,arg,dest,nxt.
     1293block_id … (pc_block (pc … st1)) ≠ -1 →
     1294st_rel st1 st2 →
     1295 fetch_statement P_in …
     1296  (joint_globalenv P_in prog stack_size) (pc … st1) =
     1297    return 〈f, fn,sequential P_in ? (CALL ?? id arg dest) nxt〉 →
     1298 eval_state P_in … (ev_genv … prog_pars_in)
     1299            st1 = return st1' →
     1300∃is_call,st2_pre_call,t_is_call.
     1301as_call_ident (joint_abstract_status prog_pars_in) «st1,is_call» =
     1302 as_call_ident (joint_abstract_status prog_pars_out) «st2_pre_call,t_is_call» ∧
     1303(pc … st1) = sigma_stored_pc P_in P_out prog stack_size
     1304 init init_regs f_lbls f_regs (pc … st2_pre_call) ∧
     1305∃st2_after_call,st2' : joint_abstract_status prog_pars_out.
     1306∃taa2 : trace_any_any … st2 st2_pre_call.
     1307∃taa2' : trace_any_any … st2_after_call st2'.
     1308eval_state P_out … (joint_globalenv P_out trans_prog stack_size) st2_pre_call =
     1309return st2_after_call ∧
     1310st_rel st1' st2' ∧
     1311as_label (joint_abstract_status prog_pars_in) st1' =
     1312as_label (joint_abstract_status prog_pars_out) st2_after_call.
     1313#p_in #p_out #prog #stack_size #f_lbls #f_regs #init_regs #init #st_no_pc_rel #st_rel
     1314#good #st1 #st1' #st2 #f #fn #id #arg #dest #nxt #Hbl #Rst1st2 #EQfetch
     1315whd in match eval_state in ⊢ (% → ?); normalize nodelta >EQfetch >m_return_bind
     1316whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
     1317#H @('bind_inversion H) -H #bl >set_no_pc_eta #H lapply(err_eq_from_io ????? H) -H
     1318#EQbl #H @('bind_inversion H) -H * #f1 *
     1319#fn1 #H lapply(err_eq_from_io ????? H) -H #EQfn1 normalize nodelta
     1320[2: #H @('bind_inversion H) -H #x whd in match eval_external_call; normalize nodelta
     1321    #H @('bind_inversion H) -H #y #_ #H @('bind_inversion H) -H #z #_
     1322    #H @('bind_inversion H) -H #w whd in ⊢ (??%% → ?); #ABS destruct(ABS) ]
     1323#H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H #st1_save #EQst1_save
     1324#H @('bind_inversion H) -H #st1_no_pc' whd in match eval_internal_call;
     1325normalize nodelta change with (stack_size ?) in match (stack_sizes ????); #H
     1326@('bind_inversion H) -H #ssize #H lapply(opt_eq_from_res ???? H) -H #EQssize
     1327#H @('bind_inversion H) -H #st1_no_pc'' #EQst1_no_pc'' whd in ⊢ (??%% → ?);
     1328#EQ destruct(EQ) whd in ⊢ (??%% → ?); #EQ destruct(EQ)
     1329% [@hide_prf whd in ⊢ (??%?); >EQfetch %]
     1330cases(fetch_statement_sigma_stored_pc … good … Hbl EQfetch)
     1331#data * #EQdata normalize nodelta *** #pre #instr #post * #Hregs * #pc' * #EQpc'
     1332* #t_fn * #nxt' * #l1 * #l2 @eq_identifier_elim
     1333[ #EQentry cases(fetch_statement_inv … EQfetch) #_ >EQentry normalize nodelta
     1334  cases(entry_is_cost … (pi2 ?? fn)) #nxt1 * #c #EQ >EQ #ABS destruct(ABS) ]
     1335#_ cut(∀b.andb b false = false) [* %] #EQ ** >EQ -EQ normalize nodelta *
     1336#EQt_call #EQpre #EQpost #_
     1337lapply(b_graph_transform_program_fetch_internal_function … good … bl f1 fn1)
     1338@eqZb_elim [ normalize nodelta #ABS @⊥ cases(block_of_call_no_minus_one … EQbl) >ABS #H @H %]
     1339#_ normalize nodelta #H cut(? : Prop)
     1340[3: #EQint_fn cases(H EQint_fn) -H
     1341|2: whd in match fetch_internal_function; normalize nodelta >EQfn1 %|*:]
     1342#data1 * #t_fn1 ** #EQt_fn1 #Hdata1 #good1
     1343cases(bind_new_bind_new_instantiates' …  (bind_instantiates_to_instantiate … Hregs)
     1344          (bind_new_bind_new_instantiates' …  (bind_instantiates_to_instantiate … EQdata)
     1345           (call_is_call … good … )) … (point_of_pc p_out pc'))
     1346[4: @(proj1 … (fetch_statement_inv … EQfetch)) |*:]
     1347#id' * #args' * #dest' #EQinstr
     1348cases(bind_new_bind_new_instantiates' … (bind_instantiates_to_instantiate … Hregs)
     1349  (bind_new_bind_new_instantiates' … (bind_instantiates_to_instantiate … EQdata)
     1350 (call_commutation … good … Hbl EQfetch bl EQbl … EQint_fn … EQst1_save … EQssize …
     1351   EQst1_no_pc'' … Rst1st2 … EQt_fn1)) … EQpc' EQt_call EQinstr)
     1352#st2_pre ** #EQst2_pre #EQt_bl * #st2_save * #EQst2_save * #st2_after * #EQst2_after
     1353#Hprologue
     1354%{(mk_state_pc ? st2_pre pc' (last_pop … st2))}
     1355%
     1356[ @hide_prf whd in ⊢ (??%?); >EQt_call >EQinstr %]
     1357%
     1358[ % [2: @sym_eq assumption] whd in ⊢ (??%%);
     1359  >EQfetch in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? ])?);
     1360  >EQt_call in ⊢ (???(match % with [ _ ⇒ ? | _ ⇒ ? ])); normalize nodelta >EQbl
     1361  >m_return_bind >EQint_fn normalize nodelta >EQinstr normalize nodelta
     1362  >EQt_bl >m_return_bind >EQt_fn1 % ]
     1363%{(mk_state_pc ? (increment_stack_usage p_out ssize st2_after)
     1364   (pc_of_point p_out bl (joint_if_entry … t_fn1)) (last_pop … st2))}
     1365cases(bind_new_bind_new_instantiates' … Hdata1 Hprologue) -Hprologue #st2' * #EQst2'
     1366#fin_sem_rel cases good1 #_ #_ #_ #_ #_ #_ #_ #_ #_ cases(entry_is_cost … (pi2 ?? fn1))
     1367#nxt1 * #c #EQcost #H lapply(H … EQcost) -H -good1 normalize nodelta
     1368>(f_step_on_cost … data1) *** #pre1 #instr1 #post1 @eq_identifier_elim [2: * #H @⊥ @H %]
     1369#_ cases(added_prologue … data1) in EQst2'; normalize nodelta
     1370[ whd in ⊢ (??%% → ?); #EQ destruct(EQ)
     1371| #hd #tl #EQst2'
     1372]
     1373* whd in ⊢ (% → ?); inversion(f_regs ??) normalize nodelta [2,4: #x #y #_ #_ *]
     1374#EQf_regs #EQ [2: whd in EQ : (???%);] destruct(EQ) * #l1 * #mid1 * #mid2 * #l2 ***
     1375#EQmid1 whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in ⊢ (% → ?); *
     1376#nxt2 * [ #EQnop | #EQt_cost ] change with nxt2 in ⊢ (??%? → ?); #EQ destruct(EQ)
     1377whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2)
     1378[ * #star_lab * #Hstar_lab * #l1 * #mid1 * #mid2 * #l2 *** #EQmid1' whd in ⊢ (% → ?);
     1379  * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in ⊢ (% → ?); * #nxt2 * #EQt_cost
     1380  change with nxt2 in ⊢ (??%? → ?); #EQ destruct(EQ) #EQl2
     1381| #EQentry
     1382]
     1383whd in EQmid1 : (??%%); destruct(EQmid1)
     1384%{(mk_state_pc ? ? (pc_of_point p_out bl (joint_if_entry … fn1)) (last_pop … st2))}
     1385[ @st2' |3: @(increment_stack_usage p_out ssize st2_after)]
     1386>(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in EQpre; #EQpre
     1387lapply(taaf_to_taa … (produce_trace_any_any_free … st2 f t_fn … EQpre … EQst2_pre) ?)
     1388[3,6: <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) <EQpc' <pc_block_eq
     1389      [2,4: inversion (sigma_pc_opt ?????????) [2,4: #x #_ % #ABS destruct(ABS) ]
     1390            #ABS cases(fetch_statement_inv … EQfetch) <EQpc'
     1391            >fetch_internal_function_no_zero [1,3: #EQ destruct]
     1392            whd in match sigma_stored_pc; normalize nodelta >ABS %]
     1393      >(pc_of_point_of_pc … pc') #taa1 %{taa1}
     1394|1,4: @if_elim #_ [2,4: @I] % whd in ⊢ (% → ?); * #H @H -H whd in ⊢ (??%?);
     1395      <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) <EQpc' <pc_block_eq
     1396      [2,4: inversion (sigma_pc_opt ?????????) [2,4: #x #_ % #ABS destruct(ABS) ]
     1397            #ABS cases(fetch_statement_inv … EQfetch) <EQpc'
     1398            >fetch_internal_function_no_zero [1,3: #EQ destruct]
     1399            whd in match sigma_stored_pc; normalize nodelta >ABS %]
     1400      >(pc_of_point_of_pc … pc') whd in match (as_pc_of ??); >EQt_call
     1401      >EQinstr %
     1402|2,5: <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) <EQpc' <pc_block_eq
     1403      [2,4: inversion (sigma_pc_opt ?????????) [2,4: #x #_ % #ABS destruct(ABS) ]
     1404            #ABS cases(fetch_statement_inv … EQfetch) <EQpc'
     1405            >fetch_internal_function_no_zero [1,3: #EQ destruct]
     1406            whd in match sigma_stored_pc; normalize nodelta >ABS %]
     1407      @(proj1 … (fetch_statement_inv … EQt_call))
     1408]
     1409-taa1
     1410[ letin trans_prog ≝ (b_graph_transform_program ????)
     1411  lapply(produce_trace_any_any_free (mk_prog_params p_out trans_prog stack_size)
     1412         (mk_state_pc ? (increment_stack_usage p_out ssize st2_after)
     1413           (pc_of_point p_out bl mid2) (last_pop … st2)) … EQst2')
     1414  [ >point_of_pc_of_point in ⊢ (????%???); @EQl2
     1415  | change with bl in match (pc_block ?); assumption
     1416  |*:
     1417  ]
     1418  #taaf %{(taaf_to_taa … (taa_append_taaf … (taa_step … (taa_base …) …) taaf) ?)}
     1419  [1,2: [ @if_elim #_ [2: @I] ] % whd in ⊢ (% → ?); * #H @H -H whd in ⊢ (??%?);
     1420        whd in match (as_pc_of ??); whd in match fetch_statement; normalize nodelta
     1421        >EQt_fn1 >m_return_bind whd in match point_of_pc; normalize nodelta
     1422        >point_of_offset_of_point  [ >EQnop %] cases EQl2 #mid * #rest **
     1423        #EQ destruct(EQ) * #nxt2 * #EQmid2 change with nxt2 in ⊢ (??%? → ?);
     1424        #EQ destruct(EQ) #_ >EQmid2 %
     1425  |3,4: whd [ whd in ⊢ (??%?); | whd in match eval_state; ]
     1426        whd in match fetch_statement; normalize nodelta
     1427        >EQt_fn1 >m_return_bind >point_of_pc_of_point >EQt_cost [%] >m_return_bind
     1428        whd in match eval_statement_no_pc; normalize nodelta >m_return_bind %
     1429  ]
     1430| >EQentry %{(taa_base …)}
     1431]
     1432%
     1433[2,4: whd in ⊢ (??%%); whd in match (as_pc_of ??);  whd in match (as_pc_of ??);
     1434      whd in match fetch_statement; normalize nodelta >EQint_fn >EQt_fn1
     1435      >m_return_bind >m_return_bind whd in match point_of_pc; normalize nodelta
     1436      >point_of_offset_of_point >point_of_offset_of_point >EQcost >m_return_bind
     1437      normalize nodelta >EQt_cost >m_return_bind [2: %] normalize nodelta
     1438      whd in match get_first_costlabel; normalize nodelta whd in ⊢ (??%%);
     1439      whd in match (get_first_costlabel_next ???);
     1440      generalize in match (refl ??);
     1441      >EQcost in ⊢ (∀e:???%. ???(??(???(match % return ? with [_ ⇒ ? | _ ⇒ ?]?))));
     1442      #EQcost' normalize nodelta %
     1443]
     1444%
     1445[1,3: whd in match eval_state; normalize nodelta >EQt_call >m_return_bind
     1446      whd in match eval_statement_no_pc; normalize nodelta >EQinstr normalize nodelta
     1447      >m_return_bind whd in match eval_statement_advance; whd in match eval_call;
     1448      normalize nodelta >EQt_bl >m_return_bind @('bind_inversion EQt_fn1)
     1449      * #f2 * #fn2 #EQ normalize nodelta whd in ⊢ (??%% → ?); #EQ1 destruct(EQ1)
     1450      >EQ -EQ >m_return_bind normalize nodelta >EQst2_save >m_return_bind
     1451      whd in match eval_internal_call; normalize nodelta whd in match (stack_sizes ????);
     1452      >EQssize >m_return_bind >EQst2_after >m_return_bind [%] >EQentry %
     1453|*: @(st_rel_def … good … fin_sem_rel …) [3,7: @EQint_fn |1,2,5,6:]
     1454    @(fetch_stmt_ok_sigma_last_pop_ok … good … EQfetch) assumption
     1455]
     1456qed.
     1457
     1458lemma eval_call_premain_ok : ∀ P_in , P_out: sem_graph_params.
     1459∀prog : joint_program P_in.
     1460∀stack_size.
     1461∀ f_lbls,f_regs.∀init_regs.∀init.
     1462∀st_no_pc_rel,st_rel.
     1463let prog_pars_in ≝ mk_prog_params P_in prog stack_size in
     1464let trans_prog  ≝ b_graph_transform_program P_in P_out init prog in
     1465let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_size in
     1466∀good : good_state_relation P_in P_out prog stack_size init init_regs f_lbls f_regs
     1467                    st_no_pc_rel st_rel.
     1468∀st1,st1' : joint_abstract_status prog_pars_in.
     1469∀st2 : joint_abstract_status prog_pars_out.
     1470∀f.
     1471∀fn : joint_closed_internal_function P_in ?.
     1472∀id,arg,dest,nxt.
     1473block_id … (pc_block (pc … st1)) = -1 →
     1474st_rel st1 st2 →
     1475 fetch_statement P_in …
     1476  (joint_globalenv P_in prog stack_size) (pc … st1) =
     1477    return 〈f, fn,sequential P_in ? (CALL ?? id arg dest) nxt〉 →
     1478 eval_state P_in … (ev_genv … prog_pars_in)
     1479            st1 = return st1' →
     1480∃is_call,st2_pre_call,t_is_call.
     1481as_call_ident (joint_abstract_status prog_pars_in) «st1,is_call» =
     1482 as_call_ident (joint_abstract_status prog_pars_out) «st2_pre_call,t_is_call» ∧
     1483(pc … st1) = sigma_stored_pc P_in P_out prog stack_size
     1484 init init_regs f_lbls f_regs (pc … st2_pre_call) ∧
     1485∃st2_after_call,st2' : joint_abstract_status prog_pars_out.
     1486∃taa2 : trace_any_any … st2 st2_pre_call.
     1487∃taa2' : trace_any_any … st2_after_call st2'.
     1488eval_state P_out … (joint_globalenv P_out trans_prog stack_size) st2_pre_call =
     1489return st2_after_call ∧
     1490st_rel st1' st2' ∧
     1491as_label (joint_abstract_status prog_pars_in) st1' =
     1492as_label (joint_abstract_status prog_pars_out) st2_after_call.
     1493#p_in #p_out #prog #stack_size #f_lbls #f_regs #init_regs #init #st_no_pc_rel #st_rel
     1494#good #st1 #st1' #st2  #f #fn #id #arg #dest #nxt #EQbl #Rst1st2 #EQfetch #EQeval
     1495% [ whd in ⊢ (??%?); >EQfetch %] %{st2} cases(pre_main_ok … good …  EQbl EQeval Rst1st2)
     1496#Hclass * #st2' ** #Rst1st2' #EQst2' #Hlab %
     1497[ change with (joint_classify ???) in ⊢ (??%?); <Hclass whd in ⊢ (??%?); >EQfetch %]
     1498% [ % [2: whd in match sigma_stored_pc; whd in match sigma_pc_opt; normalize nodelta
     1499          <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) >EQbl % ]
     1500  | %{st2'} %{st2'} %{(taa_base …)} %{(taa_base …)} % [%{EQst2' Rst1st2'}]
     1501    assumption
     1502  ]
     1503whd in ⊢ (??%%); >EQfetch in ⊢ (??(match % with [_ ⇒ ? | _ ⇒ ?])?); normalize nodelta
     1504lapply Hclass whd in ⊢ (??%% → ?); >EQfetch in ⊢ (% → ?); whd in match joint_classify_step;
     1505normalize nodelta inversion(fetch_statement ????) [2: #e #_ normalize nodelta #EQ destruct]
     1506** #f' #fn' *
     1507[ * [ #c | #id' #arg' #dest' | #r #lbl | #seq ] #nxt | * [ #lb || #h #id' #arg'] | *]
     1508#EQt_fetch whd in ⊢ (??%% → ?); #EQ destruct normalize nodelta @('bind_inversion EQeval)
     1509#x >EQfetch whd in ⊢ (??%% → ?); #EQ destruct(EQ) whd in match eval_statement_no_pc;
     1510normalize nodelta >m_return_bind whd in match eval_statement_advance;
     1511whd in match eval_call; normalize nodelta #H @('bind_inversion H) -H #bl #H
     1512lapply(err_eq_from_io ????? H) -H #EQbl #H @('bind_inversion H) -H * #f1
     1513* #fn1 #H lapply(err_eq_from_io ????? H) -H #EQfn1 normalize nodelta
     1514[2: #H @('bind_inversion H) -H #st whd in match eval_external_call; normalize nodelta
     1515   #H @('bind_inversion H) -H #x #_ #H @('bind_inversion H) -H #y #_
     1516   #H @('bind_inversion H) -H #z whd in ⊢ (??%% → ?); #EQ destruct(EQ) ]
     1517   #H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H #st1_save
     1518   #_ #H @('bind_inversion H) -H #st1_fin #_ whd in ⊢ (??%% → ?); #EQ destruct(EQ)
     1519   >EQbl >m_return_bind whd in match fetch_internal_function; normalize nodelta
     1520   >EQfn1 >m_return_bind normalize nodelta @('bind_inversion EQst2') #x
     1521   >EQt_fetch whd in ⊢ (??%% → ?); #EQ destruct(EQ) whd in match eval_statement_no_pc;
     1522   normalize nodelta >m_return_bind whd in match eval_statement_advance;
     1523   whd in match eval_call; normalize nodelta #H @('bind_inversion H) -H
     1524   #bl' >set_no_pc_eta #H lapply(err_eq_from_io ????? H) -H #EQbl'
     1525   #H @('bind_inversion H) -H * #f1' * #fn1' #H lapply(err_eq_from_io ????? H) -H
     1526   #EQfn1' normalize nodelta
     1527[2: #H @('bind_inversion H) -H #st whd in match eval_external_call; normalize nodelta
     1528   #H @('bind_inversion H) -H #x #_ #H @('bind_inversion H) -H #y #_
     1529   #H @('bind_inversion H) -H #z whd in ⊢ (??%% → ?); #EQ destruct(EQ) ]
     1530#H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H
     1531#st2_save #_ #H @('bind_inversion H) -H #st2_fin #_ whd in ⊢ (??%% → ?);
     1532#EQ destruct(EQ) >EQbl' >m_return_bind >EQfn1' >m_return_bind normalize nodelta
     1533lapply(fetch_ok_pc_ok … good … Rst1st2' ?)
     1534     [ whd in match fetch_internal_function; normalize nodelta >EQfn1 in ⊢ (??%?); %
     1535     |*:
     1536      ]
     1537    whd in match pc_of_point in ⊢ (% → ?); normalize nodelta #EQ destruct(EQ)
     1538    lapply EQfn1 whd in match fetch_function; normalize nodelta
     1539    @eqZb_elim [ #ABS @⊥ cases(block_of_call_no_minus_one …  EQbl) #H @H assumption]
     1540    #Hbl' normalize nodelta #H lapply(opt_eq_from_res ???? H) -H #H @('bind_inversion H)
     1541    #f2 #EQf2 #H @('bind_inversion H) -H #fn2 #_ whd in ⊢ (??%? → ?); -e0 -EQ
     1542    #EQ destruct(EQ) -H lapply EQfn1' whd in match fetch_function; normalize nodelta
     1543    @eqZb_elim [ #ABS >ABS in Hbl'; * #H @⊥ @H %] #_ normalize nodelta
     1544    #H lapply(opt_eq_from_res ???? H) -H
     1545    whd in match joint_globalenv in ⊢ (% → ?); normalize nodelta
     1546    whd in match b_graph_transform_program in ⊢ (% → ?); normalize nodelta
     1547    whd in match transform_joint_program; normalize nodelta
     1548    >(symbol_for_block_transf ??? (λx.x) prog
     1549      (λvars.transf_fundef ?? (λdef_in.b_graph_translate ??? (init ? def_in) def_in)) bl') in ⊢ (% → ?);
     1550    >EQf2 >m_return_bind in ⊢ (% → ?); #H @('bind_inversion H) -H #fn2' #_
     1551    whd in ⊢ (??%% → ?); #EQ destruct(EQ) %
     1552qed.
     1553
     1554
     1555lemma pair_dep_match_elim : ∀A,B,C : Type[0].∀P : C → Prop.∀t:A×B.
     1556∀c.
     1557(∀x,y,prf.P (c x y prf)) →
     1558P (let 〈x,y〉 as prf ≝ t in c x y prf).
     1559#A #B #C #P * // qed.
    17881560
    17891561theorem joint_correctness : ∀p_in,p_out : sem_graph_params.
     
    17961568good_state_relation p_in p_out prog stack_size init init_regs
    17971569 f_lbls f_regs st_no_pc_rel st_rel →
     1570good_init_relation p_in p_out prog stack_size init st_no_pc_rel →
    17981571let trans_prog ≝ b_graph_transform_program … init prog in
    17991572∀init_in.make_initial_state (mk_prog_params p_in prog stack_size) = OK ? init_in →
     
    18041577    (joint_abstract_status (mk_prog_params p_out trans_prog stack_size))
    18051578    R init_in init_out.
    1806 cases daemon
     1579#p_in #p_out #prog #stack_size #init #init_regs #f_lbls #f_regs #st_no_pc_rel
     1580#st_rel #good #good_init #init_in whd in match make_initial_state; normalize nodelta
     1581#H @('bind_inversion H) -H #init_m #EQinit_m @pair_dep_match_elim #m #bl #prf
     1582whd in ⊢ (??%% → ?); #EQ destruct(EQ)
     1583letin trans_prog ≝ (b_graph_transform_program ????)
     1584letin globals_size ≝ (globals_stacksize … trans_prog)
     1585letin spp ≝
     1586   («mk_pointer bl (mk_offset (bitvector_of_Z 16 (-S (globals_size)))),
     1587     pi2 … bl»)
     1588letin st ≝ (mk_state p_out
     1589    (* frames ≝ *)(Some ? (empty_framesT …))
     1590    (* internal_stack ≝ *) empty_is
     1591    (* carry ≝ *)(BBbit false)
     1592    (* regs ≝ *)(empty_regsT … spp)
     1593    (* mem ≝ *)m
     1594    (* stack_usage ≝ *)0)
     1595%{(mk_state_pc ? (set_sp … spp st) init_pc (null_pc one))} >init_mem_transf
     1596>EQinit_m >m_return_bind @pair_dep_match_elim #m1 #bl1 #prf' lapply prf
     1597lapply prf' lapply prf' <prf in ⊢ (%→?); #EQ destruct(EQ) -prf' #prf' #_
     1598%{(refl …)} %{(JointStatusSimulation … good)} %
     1599[ whd @(st_rel_def … good)
     1600  [3: % |1,2:
     1601  | lapply(good_empty ?????? good_init ? EQinit_m) <prf' normalize nodelta #H @H
     1602  | %
     1603  ]
     1604| whd whd in ⊢ (??%%); lapply(good_init_cost_label … good_init) normalize nodelta
     1605  cases(fetch_statement ????) normalize nodelta
     1606  [2: #e * [ *#e' #EQ >EQ % | * #x * #EQ #EQ1 >EQ normalize nodelta >EQ1 % ] ]
     1607  #x cases(cost_label_of_stmt ???) normalize nodelta
     1608  [ * [ * #e' #EQ >EQ % | * #y * #EQ1 #EQ2 >EQ1 normalize nodelta >EQ2 %]
     1609  | #c * #y * #EQ1 #EQ2 >EQ1 normalize nodelta >EQ2 %
     1610  ]
     1611]
     1612%
     1613[ #st1 #st1' #st2 whd in ⊢ (% → ?); #EQeval @('bind_inversion EQeval)
     1614  ** #f #fn #stmt #H lapply(err_eq_from_io ????? H) -H cases stmt -stmt
     1615  [ * [ #c | #id #arg #dest | #r #lb | #seq ] #nxt | #fin | * ] #EQfetch #_
     1616  whd in ⊢ (% → ?); #Rst1st2
     1617  change with (joint_classify ???) in
     1618                     ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]);
     1619  [ whd in match joint_classify; normalize nodelta >EQfetch normalize nodelta
     1620    cases(decidable_eq_Z (block_id (pc_block … (pc … st1))) (neg one)) #Hbl
     1621    [ cases(general_eval_cost_premain_ok … good … Hbl Rst1st2 EQfetch EQeval)
     1622    | cases(general_eval_cost_ok … good … Hbl Rst1st2 EQfetch EQeval)
     1623    ] #st2' * #Rst1st2' * #taaf * #H #H1 %{st2'} %{taaf} >H % [1,3: %{I} assumption]
     1624      assumption
     1625  | whd in match joint_classify; normalize nodelta >EQfetch normalize nodelta #prf
     1626    cases(decidable_eq_Z (block_id (pc_block … (pc … st1))) (neg one)) #Hbl
     1627    [ cases(eval_call_premain_ok … good … Hbl Rst1st2 EQfetch EQeval)
     1628    | cases(eval_call_ok … good … Hbl Rst1st2 EQfetch EQeval)
     1629    ]
     1630    #prf' * #st2_pre * #prf'' ** #EQ #EQ1 * #st2_after * #st2' * #taa * #taa1 ** #EQ2 #H #EQ3
     1631    %{st2_pre} [1,3: assumption] % [1,3: % [1,3: >EQ % |*: assumption ] ]
     1632    %{st2_after} %{st2'} %{taa} %{taa1} % [1,3: %{EQ2 H}] assumption
     1633  | whd in match joint_classify; normalize nodelta >EQfetch normalize nodelta
     1634    #ncost cases(decidable_eq_Z (block_id (pc_block … (pc … st1))) (neg one)) #Hbl
     1635    [ cases(eval_cond_premain_ok … good … Hbl Rst1st2 EQfetch EQeval ncost)
     1636    | cases(eval_cond_ok … good … Hbl Rst1st2 EQfetch EQeval ncost)
     1637    ]
     1638    #st2' * #H * #taaf * #H1 #H2 %{st2'} %{taaf} >H1 % [1,3: %{I} assumption]
     1639    assumption
     1640  | whd in match joint_classify; normalize nodelta >EQfetch normalize nodelta
     1641    cases(decidable_eq_Z (block_id (pc_block … (pc … st1))) (neg one)) #Hbl
     1642    [ cases(general_eval_seq_no_call_premain_ok … good … Hbl Rst1st2 EQfetch EQeval)
     1643    | cases(general_eval_seq_no_call_ok … good … Hbl Rst1st2 EQfetch EQeval)
     1644    ]
     1645    #st2' * #H * #taaf * #H1 #H2 %{st2'} %{taaf} % [ >H1 %{I H} |3: %{H1 H} ]
     1646    assumption
     1647    ]
     1648  | @(as_result_ok … good)
     1649  ]
     1650cases fin in EQfetch; -fin
     1651  [ #lb #EQfetch whd in match joint_classify; normalize nodelta >EQfetch
     1652    normalize nodelta
     1653    cases(decidable_eq_Z (block_id (pc_block … (pc … st1))) (neg one))
     1654    #Hbl
     1655    [ cases(eval_goto_premain_ok … good … Hbl Rst1st2 EQfetch EQeval)
     1656    | cases(eval_goto_ok … good … Hbl Rst1st2 EQfetch EQeval)
     1657    ]
     1658    #st2' * #H * #taaf * #H1 #H2 %{st2'} %{taaf} >H1 % [1,3: %{I H}] assumption
     1659 | #EQfetch whd in match joint_classify; normalize nodelta >EQfetch
     1660   normalize nodelta
     1661   cases(decidable_eq_Z (block_id (pc_block … (pc … st1))) (neg one))
     1662   #Hbl
     1663   [ @⊥ @(pre_main_no_return … good … Hbl … EQfetch) ]
     1664   cases(eval_return_ok … good … Hbl Rst1st2 EQfetch EQeval) #st2_pre * #st2_after
     1665   * #st2' * #taa * #taaf ***** #H #H1 #H2 #H3 #H4 #H5 %{st2_pre} %{st2_after}
     1666   %{st2'} %{taa} %{taaf} % [2: assumption] % [2: assumption] % [2: assumption]
     1667   % [2: assumption] %{H H1}
     1668 | #has #id #arg #EQfetch whd in match joint_classify; normalize nodelta
     1669   >EQfetch normalize nodelta
     1670   cases(decidable_eq_Z (block_id (pc_block … (pc … st1))) (neg one))
     1671   #Hbl
     1672   [ cases(eval_tailcall_premain_ok … good … Hbl Rst1st2 EQfetch EQeval)
     1673   | cases(eval_tailcall_ok … good … Hbl Rst1st2 EQfetch EQeval)
     1674   ]
     1675   #prf * #st2_pre * #t_is_call * #H * #st2_after * #st2' * #taa1 * #taa2
     1676   ** #H1 #H2 #H3 #prf' %{st2_pre} [1,3: assumption] %{H} %{st2_after} %{st2'}
     1677   %{taa1} %{taa2} % [2,4: assumption] %{H1 H2}
     1678 ]
    18071679qed.
    18081680
    1809 
  • src/joint/joint_semantics.ma

    r3037 r3154  
    516516  ! bl ← match f with
    517517    [ inl id ⇒
    518       opt_to_res … [MSG BadFunction; CTX … id]
    519         (find_symbol … ge id)
     518      !bl ← opt_to_res … [MSG BadFunction; CTX … id] (find_symbol … ge id) ;
     519      if eqZb (block_id bl) (-1) then
     520        Error … [MSG BadFunction; CTX … id]
     521      else return bl
    520522    | inr addr ⇒
    521523      ! addr_l ← dpl_arg_retrieve … st (\fst addr) ;
    522524      ! addr_h ← dph_arg_retrieve … st (\snd addr) ;
    523525      ! ptr ← pointer_of_bevals … [addr_l ; addr_h ] ;
    524       if eq_bv … (bv_zero …) (offv (poff ptr)) then
     526      if eq_bv … (bv_zero …) (offv (poff ptr)) ∧
     527         (notb (eqZb (block_id (pblock ptr)) (-1))) then
    525528        return pblock ptr
    526529      else
     
    529532  opt_to_res … [MSG BadFunction; MSG BadPointer]
    530533    (code_block_of_block bl).
     534
     535lemma match_reg_elim : ∀ A : Type[0]. ∀ P : A → Prop. ∀ r : region.
     536∀f : (r = XData) → A. ∀g : (r = Code) → A. (∀ prf : r = XData.P (f prf)) →
     537(∀ prf : r = Code.P (g prf)) →
     538P ((match r return λx.(r = x → ?) with
     539    [XData ⇒ f | Code ⇒ g])(refl ? r)).
     540#A #P * #f #g #H1 #H2 normalize nodelta [ @H1 | @H2]
     541qed.
     542
     543lemma block_of_call_no_minus_one : ∀p,globals,ge,f,st,bl.
     544block_of_call p globals ge f st = return bl →
     545block_id bl ≠ -1.
     546#p #globals #ge #f #st #bl whd in match block_of_call; normalize nodelta
     547#H cases(bind_inversion ????? H) #bl1 cases f -f normalize nodelta
     548[ #id * #H cases(bind_inversion ????? H) -H #bl2 * #_ @eqZb_elim #EQbl2
     549  normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ)
     550  #H lapply(opt_eq_from_res ???? H) -H whd in match code_block_of_block;
     551  normalize nodelta @match_reg_elim [ #_ #EQ destruct] #prf #EQ destruct(EQ)
     552  assumption
     553| * #dpl #dph * #H cases(bind_inversion ????? H) -H #bv1 * #_ #H
     554  cases(bind_inversion ????? H) -H #bv2 * #_ #H cases(bind_inversion ????? H) -H
     555  #ptr * #_ @eq_bv_elim #_ normalize nodelta [2: whd in ⊢ (??%% → ?); #EQ destruct]
     556  @eqZb_elim #EQptr normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct
     557  #H lapply(opt_eq_from_res ???? H) -H whd in match code_block_of_block;
     558  normalize nodelta @match_reg_elim [#_ #EQ destruct] #prf #EQ destruct
     559  assumption
     560]
     561qed.
     562
    531563
    532564definition eval_external_call ≝
Note: See TracChangeset for help on using the changeset viewer.