Changeset 3118


Ignore:
Timestamp:
Apr 10, 2013, 6:45:40 PM (7 years ago)
Author:
piccolo
Message:

1) finished return case in StatusSimulationHelper?

2) started to write Deliverable D4.4

Files:
2 added
1 edited

Legend:

Unmodified
Added
Removed

  • src/joint/StatusSimulationHelper.ma

    r3050 r3118  
    140140return res.
    141141
    142 lemma partial_inj_sigma :
     142                                         
     143                         
     144
     145lemma partial_inj_sigma_label :
    143146∀p_in,p_out,prog,stack_size,init,init_regs.
    144147∀f_lbls : lbl_funct_type.∀f_regs,bl,lbl1,lbl2.
    … …  
    199202[2,3: @⊥ [ >Hbl in Hbl1; | >Hbl1 in Hbl;] #H @H % |4: %]
    200203whd in match (offset_of_point ??) in EQpt2;
    201 <EQpt1 in EQpt2; #H lapply(partial_inj_sigma … (sym_eq ??? H))
     204<EQpt1 in EQpt2; #H lapply(partial_inj_sigma_label … (sym_eq ??? H))
    202205[ >EQpt1 % #EQ -prog destruct(EQ)] whd in match point_of_pc; normalize nodelta
    203206whd in match (point_of_offset ??); whd in match (point_of_offset ??);
    … …  
    246249#EQsucc #H whd in ⊢ (??%%); @eq_f @(IH … H)
    247250qed.
     251
     252lemma fetch_stmt_ok_succ_ok : ∀p : sem_graph_params.
     253∀prog : joint_program p.∀stack_size,f,fn,stmt,pc,pc',lbl.
     254In ? (stmt_labels p ? stmt) lbl→
     255fetch_statement p … (joint_globalenv p prog stack_size) pc = return 〈f,fn,stmt〉 →
     256pc' = 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
     259cases(fetch_statement_inv … EQfetch) #EQfn normalize nodelta #EQstmt
     260#EQ destruct(EQ) lapply(code_is_closed … (pi2 ?? fn) … EQstmt) *
     261cases(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]
     279qed.
     280
     281
     282lemma fetch_stmt_ok_nxt_ok : ∀p : sem_graph_params.
     283∀prog : joint_program p.∀stack_size,f,fn,stmt,bl,pt,nxt.
     284fetch_internal_function … (joint_globalenv p prog stack_size) bl =
     285return 〈f,fn〉→
     286stmt_at p … (joint_if_code … fn) pt = return sequential p ? stmt nxt →
     287∃stmt'.
     288stmt_at p … (joint_if_code … fn) nxt = return stmt'.
     289#p #prog #stack_size #f #fn #stmt #bl #pt #nxt #EQfn #EQstmt
     290cases(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]
     300qed.
     301
    248302
    249303lemma sigma_label_spec : ∀p_in,p_out,prog,stack_size,init,init_regs.
    … …  
    260314[ O ⇒ sigma_label p_in p_out prog stack_size init init_regs f_lbls f_regs bl pt = return pt
    261315| S m ⇒ ∃lbl.nth_opt ? m (f_lbls bl pt) = return lbl ∧
    262     sigma_label p_in p_out prog stack_size init init_regs f_lbls f_regs bl lbl = return pt
     316    sigma_label p_in p_out prog stack_size init init_regs f_lbls f_regs bl lbl = return pt     
    263317].
    264318#p_in #p_out #prog #stack_size #init #init_regs #f_lbls #f_regs #good #id #fn
    … …  
    288342           whd in match (length ??); #EQn whd in match (length ??); normalize nodelta]
    289343 [5,6,7,8,9: whd in match sigma_label; normalize nodelta >code_block_of_block_eq
    290    >m_return_bind >EQfn >m_return_bind inversion(find ????)
    291    [1,3,5,7,9: #EQfind @⊥ lapply(find_none ?????? EQfind EQstmt) >EQn normalize nodelta
     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
    292346     @eq_identifier_elim [1,3,5,7,9: #_ *] * #H #_ @H % ] * #lbl1 #stmt1 #EQfind
    293    >m_return_bind @eq_f lapply(find_predicate ?????? EQfind) whd in match preamble_length;
    294    normalize nodelta >code_block_of_block_eq >m_return_bind >EQfn >m_return_bind
    295    whd in match (stmt_at ????); >(find_lookup ?????? EQfind) >m_return_bind >Hinit
    296    >m_return_bind cases stmt1 in EQfind; -stmt1
    297    [1,4,7,10,13: #j_step1 #nxt1 |2,5,8,11,14: #fin1 |*: *] #EQfind normalize nodelta
    298    cases(bind_instantiate ????) [1,3,5,7,9,11,13,15,17,19: *]
    299    [1,2,3,4,5: ** #pre_instr1 #instr1 #post_instr1 |*: * #pre_instr1 #instr1 ]
    300    >m_return_bind cases pre_instr1 -pre_instr1 [2,4,6,8,10,12,14,16,18,20: #hd #tl]
    301    whd in match (length ??); normalize nodelta
    302    [11,12,13,14,15,16,17,18,19,20: @eq_identifier_elim [2,4,6,8,10,12,14,16,18,20: #_ *] #EQ #_ >EQ %]
    303    whd in match (nth_opt ???); inversion(nth_opt ???) [1,3,5,7,9,11,13,15,17,19: #_ *]
    304    #lbl2 #EQlbl2 normalize nodelta @eq_identifier_elim [2,4,6,8,10,12,14,16,18,20: #_ *]
    305    #EQ lapply EQlbl2 destruct(EQ) #EQlbl2 @⊥
    306    cases(Exists_All … (nth_opt_Exists … EQlbl2) (fresh_lab lbl1)) #x * #EQ destruct(EQ) **
    307    #H #_ @H  @(code_is_in_universe … (pi2 ?? fn)) whd in match code_has_label;
    308    whd in match code_has_point; normalize nodelta >EQstmt @I
     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
    309364 |*: cases syntax_spec -syntax_spec #pre * #mid1 [3,4: * #mid2 * #post] ** [1,2: *]
    310365     cases pre -pre [1,3,5,7: #_ * #x * #y ** #ABS destruct(ABS)] #hd1 #tl1 whd in ⊢ (??%% → ?);
    … …  
    374429qed.
    375430
     431definition stmt_get_next : ∀p,globals.joint_statement p globals → option (succ p) ≝
     432λp,globals,stmt.
     433match stmt with
     434[sequential stmt nxt ⇒ Some ? nxt
     435| _ ⇒ None ?
     436].
     437
     438
     439definition sigma_next : ∀p_in,p_out : sem_graph_params.
     440joint_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 →
     444block → 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    ]);
     462stmt_get_next … s.
     463
    376464lemma fetch_statement_sigma_stored_pc :
    377465∀p_in,p_out,prog,stack_sizes,
    … …  
    386474match stmt with
    387475[ sequential step nxt ⇒
    388     ∃step_block. bind_instantiate ?? (f_step … data (point_of_pc p_in pc) step)
     476    ∃step_block : step_block p_out (prog_names … trans_prog).
     477    bind_instantiate ?? (f_step … data (point_of_pc p_in pc) step)
    389478                 (f_regs (pc_block pc) (point_of_pc p_in pc)) = return step_block ∧
    390479    ∃pc'.sigma_stored_pc p_in p_out prog stack_sizes init
    391480                                           init_regs f_lbls f_regs pc' = pc ∧
    392     ∃fn',nxt'.
     481    ∃fn',nxt',l1,l2.
    393482    fetch_statement p_out … (joint_globalenv p_out trans_prog stack_sizes) pc' =
    394483    if not_emptyb … (added_prologue … data) ∧
    395484       eq_identifier … (point_of_pc p_in pc) (joint_if_entry … fn)
    396     then return 〈f,fn',sequential ?? (NOOP …) nxt'〉
    397     else return 〈f,fn',sequential ?? ((\snd(\fst step_block)) (point_of_pc p_in pc')) nxt'〉
     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
    398492| final fin ⇒
    399493    ∃fin_block.bind_instantiate ?? (f_fin … data (point_of_pc p_in pc) fin)
    … …  
    407501].
    408502#p_in #p_out #prog #stack_sizes #init #init_regs #f_lbls #f_regs #pc #f #fn #stmt
    409 #good #Hbl #EQfetch
    410 lapply(b_graph_transform_program_fetch_statement … good pc f fn ?)
    411 [2: @eqZb_elim [1,3: #ABS @⊥ >ABS in Hbl; * #H @H %] #_ normalize nodelta
    412       #H cases(H EQfetch) -H |*:]
    413 #data * #t_fn ** #EQt_fn #Hinit #H %{data} >Hinit %{(refl …)} cases stmt in EQfetch H;
    414 [ #step #nxt | #fin | *] normalize nodelta #EQfetch -stmt
     503#good #Hbl #EQfetch cases(fetch_statement_inv … EQfetch) #EQfn normalize nodelta
     504#EQstmt
     505lapply(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
     508lapply(H … EQstmt) -H normalize nodelta #H #_ %{data} >Hinit %{(refl …)}
     509-EQfetch cases stmt in EQstmt H;
     510[ #step #nxt | #fin | *] normalize nodelta #EQstmt -stmt
    415511[ cases(added_prologue ??? data) [2: #hd #tl] normalize nodelta
    416512  [ @eq_identifier_elim #EQentry normalize nodelta ] ]
    … …  
    423519|*: #Hregs #syntax_spec
    424520]
    425 cases(fetch_statement_inv … EQfetch) #EQfn normalize nodelta #EQstmt
    426521[ whd in match (point_of_pc ??) in EQstmt EQentry; <EQentry in EQstmt;
    427522  cases(entry_is_cost … (pi2 ?? fn)) #nxt1 * #c #EQstmt >EQstmt #EQ destruct(EQ)
    … …  
    436531    whd in ⊢ (??%% → ?); #EQ destruct(EQ)
    437532|5: whd in match (point_of_pc ??); <EQentry >EQsigma_lab >m_return_bind
    438     normalize nodelta >EQentry % [ cases pc #bl #off %] %{t_fn} %{nxt}
     533    normalize nodelta >EQentry % [ cases pc #bl #off %] %{t_fn} %{nxt} %{[ ]} %{[ ]}
    439534    whd in match fetch_statement; normalize nodelta >EQt_fn >m_return_bind
    440     >EQt_stmt >m_return_bind @eq_identifier_elim [#_ %] * #H @⊥ @H %
     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
    441557|2,3,4: %{(pc_of_point p_out (pc_block pc) lbl)}
    442558|6,7,8: %{pc}
    … …  
    452568#EQmid #EQpre whd in ⊢ (% → ?);
    453569[1,2,3,4: * #nxt1 *] #EQt_stmt
    454 [1,2,3,4: change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) #EQpost %{mid2}]
    455 whd in match fetch_statement; normalize nodelta >EQt_fn >m_return_bind
    456 @('bind_inversion EQpreamble) #bl1 >code_block_of_block_eq whd in ⊢ (??%? → ?);
    457 #EQ destruct(EQ) >EQfn >m_return_bind >EQstmt >m_return_bind >Hinit >m_return_bind
    458 normalize nodelta >Hregs >m_return_bind cases pre in Hregs EQpre; -pre
    459 [1,3,6,8,9,12: [3,4,6: #x #y] #_ #_ whd in match (length ??); whd in ⊢ (??%? → ?);
    460    #EQ destruct(EQ)]
    461 [1,2,5: #hd1 #tl1 ] #Hregs cases l1 in EQmid;
    462 [1,3,5,8,10,12: [4,5,6: #x #y] #_ whd in ⊢ (% → ?); [1,2,3: * #EQ1 #EQ2 destruct]
    463    * #mid * #rest ** #EQ destruct(EQ)]
    464 [1,2,3: #hd2 #tl2] whd in ⊢ (??%% → ?); #EQ destruct(EQ) whd in ⊢ (% → ?);
    465 [4,5,6: * #_ #EQ #_ >EQ >EQt_stmt [2,3: %] @eq_identifier_elim [2: #_ %]
    466         #EQ <EQ in EQentry; * #H @⊥ @H %]
    467 * #mid' * #rest ** #EQ1 destruct(EQ1) #H1 #H2 whd in match (length ??);
    468 whd in ⊢ (??%? → ?); #EQ1 destruct(EQ1) >e0 in EQnth_opt;
    469 lapply(seq_list_in_code_length … H2) [1,2: >length_map] #EQ1 >EQ1
    470 >nth_opt_append_r [2,4,6: %] cut(|rest|-|rest|=O) [1,3,5: cases(|rest|) //]
    471 #EQ2 >EQ2 whd in ⊢ (??%% → ?); #EQ3 -EQ2 -EQ1
    472 [1,2: destruct(EQ3) >point_of_pc_of_point >EQt_stmt [2: >point_of_pc_of_point %]
    473       @eq_identifier_elim [#EQ4 <EQ4 in EQentry; * #H3 @⊥ @H3 %] #_
    474       >point_of_pc_of_point %]
    475 destruct(EQ3) >point_of_pc_of_point >EQt_stmt %
    476 qed.
     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 %]
     595whd 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]
     713qed.
     714
    477715
    478716definition make_is_relation_from_beval : (beval → beval → Prop) →
    … …  
    595833qed.
    596834
     835lemma 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;
     841whd 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
     844cases bl in Hbl; * #id #prf #EQ destruct(EQ)
     845change with (mk_block OZ) in match (mk_block ?);
     846cut(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 %
     850qed.
     851 
     852lemma next_of_call_pc_ok : ∀P_in,P_out : sem_graph_params.
     853∀init,prog,stack_sizes,init_regs,f_lbls,f_regs.
     854b_graph_transform_program_props P_in P_out stack_sizes
     855  init prog init_regs f_lbls f_regs →
     856let 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.
     859fetch_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)) →
     868gen_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 | *]
     878whd 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)
     881cases(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]
     887whd 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
     889inversion(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
     902lapply(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
     906lapply(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 %
     910qed.
    597911
    598912definition joint_state_relation ≝
    … …  
    600914
    601915definition joint_state_pc_relation ≝ λP_in,P_out.state_pc P_in → state_pc P_out → Prop.
    602 
    603916
    604917record good_state_relation (P_in : sem_graph_params)
    … …  
    6971010            ∃bv'. acca_retrieve … P_out st2_pre_mid_no_pc a' = return bv' ∧
    6981011                  bool_of_beval … bv' = return b
    699             (*let st2_pre_mid ≝  mk_state_pc P_out st2_pre_mid_no_pc
    700                                (pc_of_point P_out (pc_block (pc … st2)) mid) (last_pop … st2) in
    701             let st2' ≝ mk_state_pc P_out st2_pre_mid_no_pc (pc … st1') (last_pop … st2) in
    702             eval_statement_advance P_out (prog_var_names … trans_prog)
    703              (joint_globalenv P_out trans_prog stack_sizes) f t_fn
    704              (sequential P_out ? ((\snd (\fst blp)) mid) lfalse) st2_pre_mid = return st2'*)
    7051012   )  (f_step … data (point_of_pc P_in (pc … st1)) cond)   
    7061013  ) (init ? fn)
    … …  
    7321039      ) (f_step … data (point_of_pc P_in (pc … st1)) seq)
    7331040     ) (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)
    7341051; cost_commutation :
    7351052  let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
    … …  
    7401057  return 〈f, fn,  sequential ?? (COST_LABEL ?? c) nxt〉 → 
    7411058  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)
    7421168}.
    7431169
    744 lemma fetch_stmt_ok_succ_ok : ∀p : sem_graph_params.
     1170definition 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.
     1174good_state_relation p_in p_out prog stack_sizes init init_regs f_lbls f_regs
     1175                    st_no_pc_rel st_rel →
     1176let trans_prog ≝ b_graph_transform_program p_in p_out init prog in
     1177status_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(*
     1190lemma fetch_stmt_ok_succs_ok : ∀p : sem_graph_params.
    7451191∀prog : joint_program p.∀stack_size,f,fn,stmt,pc,pc',lbl.
    7461192In ? (stmt_labels p ? stmt) lbl→
    … …  
    7701216]
    7711217qed.
    772 
     1218*)
    7731219
    7741220
    … …  
    11251571qed.
    11261572
    1127 (*
     1573lemma next_of_call_pc_error : ∀pars.∀prog. ∀stack_size,pc.
     1574block_id (pi1 … (pc_block pc)) = 0→
     1575next_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
     1578whd in match fetch_statement; normalize nodelta
     1579>fetch_internal_function_no_zero //
     1580qed.
     1581
     1582lemma next_of_call_pc_inv :  ∀pars.∀prog. ∀stack_size.
     1583∀pc,nxt.
     1584next_of_call_pc pars … (ev_genv … (mk_prog_params pars prog stack_size)) pc
     1585= return nxt →
     1586∃id,fn,c_id,c_args,c_dest.
     1587fetch_statement pars
     1588    … (ev_genv … (mk_prog_params pars prog stack_size)) pc =
     1589    return 〈id,fn, sequential ? ?(CALL pars ? c_id c_args c_dest) nxt〉.
     1590#pars #prog #init #pc #nxt whd in match next_of_call_pc; normalize nodelta
     1591#H @('bind_inversion H) -H ** #id #fn *
     1592[ *[ #c | #c_id #c_arg #c_dest | #reg #lbl | #seq ] #prox | #fin | #H #r #l #l ]
     1593#EQfetch normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ)
     1594%{id} %{fn} %{c_id} %{c_arg} %{c_dest} assumption
     1595qed.
     1596
     1597lemma stored_pc_inj :
     1598∀p_in,p_out,prog,stack_size,init,init_regs,f_lbls,f_regs,pc,pc'.
     1599sigma_pc_opt p_in p_out prog stack_size init init_regs f_lbls f_regs pc ≠ None ? →
     1600sigma_stored_pc p_in p_out prog stack_size init init_regs f_lbls f_regs pc =
     1601sigma_stored_pc p_in p_out prog stack_size init init_regs f_lbls f_regs pc' →
     1602pc = pc'.
     1603#p_in #p_out #prog #stack_size #init #init_regs #f_lbls #f_regs #pc #pc' #H
     1604whd in match sigma_stored_pc; normalize nodelta
     1605inversion(sigma_pc_opt ?????????) [ #ABS >ABS in H; * #H @⊥ @H %] #pc1 #EQpc1
     1606normalize 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]
     1610  #Hbl normalize nodelta #H @('bind_inversion H) -H #lbl whd in match sigma_label;
     1611  normalize nodelta >code_block_of_block_eq >m_return_bind
     1612  >fetch_internal_function_no_zero [ whd in ⊢ (??%% → ?); #EQ destruct(EQ)]
     1613  >(pc_block_eq … H) whd in match sigma_stored_pc; normalize nodelta >EQpc1 %
     1614]
     1615#pc2 #EQpc2 normalize nodelta #EQ destruct(EQ)
     1616@(sigma_stored_pc_inj p_in p_out prog stack_size init init_regs f_lbls f_regs …)
     1617[ assumption] >EQpc1 >EQpc2 %
     1618qed.
     1619
     1620
     1621
     1622
     1623
    11281624lemma eval_return_ok :
    11291625∀ P_in , P_out: sem_graph_params.
    … …  
    11311627∀stack_sizes.
    11321628∀ f_lbls,f_regs.∀f_bl_r.∀init.
    1133 ∀good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs.
    11341629∀st_no_pc_rel,st_rel.
    11351630let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
    11361631let trans_prog  ≝ b_graph_transform_program P_in P_out init prog in
    11371632let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
    1138 good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs good
    1139                     st_no_pc_rel st_rel →
    1140 ∀st1,st1' :  joint_abstract_status prog_pars_in.
     1633∀good : good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs
     1634                    st_no_pc_rel st_rel.
     1635∀st1,st1' : joint_abstract_status prog_pars_in.
    11411636∀st2 : joint_abstract_status prog_pars_out.
    11421637∀f.
    1143 ∀fn : joint_closed_internal_function P_in (prog_var_names … prog).
    1144 *)
    1145 
     1638∀fn : joint_closed_internal_function P_in ?.
     1639block_id … (pc_block (pc … st1)) ≠ -1 →
     1640st_rel st1 st2 →
     1641 fetch_statement P_in …
     1642  (joint_globalenv P_in prog stack_sizes) (pc … st1) =
     1643    return 〈f, fn,final P_in ? (RETURN …)〉 →
     1644 eval_state P_in … (ev_genv … prog_pars_in)
     1645            st1 = return st1' →
     1646∃st2_ret,st2_after_ret,st2' : joint_abstract_status prog_pars_out.
     1647∃taa2 : trace_any_any … st2 st2_ret.
     1648∃taa2' : trace_any_any_free … st2_after_ret st2'.
     1649(if taaf_non_empty … taa2' then ¬as_costed … st2_after_ret else True) ∧
     1650as_classifier … st2_ret cl_return ∧
     1651        as_execute … st2_ret st2_after_ret ∧ st_rel st1' st2' ∧
     1652        ret_rel ?? (JointStatusSimulation … good) st1' st2_after_ret.
     1653#p_in #p_out #prog #stack_size #f_lbls #f_regs #init_regs #init #st_no_pc_rel
     1654#st_rel #good #st1 #st1' #st2 #f #fn #Hbl #Rst1st2 #EQfetch
     1655whd in match eval_state; normalize nodelta >EQfetch >m_return_bind
     1656whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
     1657whd in match eval_statement_advance; whd in match eval_return; normalize nodelta
     1658#H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H #ssize
     1659#H lapply(opt_eq_from_res ???? H) -H change with (stack_size f) in ⊢ (??%? → ?);
     1660#EQssize #H @('bind_inversion H) -H * #st_pop #pc_pop #EQpop #H @('bind_inversion H)
     1661-H #next_of_call #EQnext_of_call whd in ⊢ (??%% → ?); whd in match next;
     1662whd in match set_last_pop; whd in match set_pc; normalize nodelta #EQ destruct(EQ)
     1663lapply(b_graph_transform_program_fetch_statement … good (pc … st1) f fn ?)
     1664[2: @eqZb_elim [ #ABS @⊥ >ABS in Hbl; * #H @H %] #_ normalize nodelta
     1665      #H cases(H EQfetch) -H |*:]
     1666#data * #t_fn ** #EQt_fn >(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in EQt_fn;
     1667#EQt_fn #Hinit normalize nodelta ** #pre #fin_s * #Hregs * #pre * #mid
     1668** #EQmid #EQpre whd in ⊢ (% → ?); #EQt_stmt
     1669cases(next_of_call_pc_inv … EQnext_of_call) #f1 * #fn1 * #id * #args * #dest #EQcall
     1670<(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in Hregs; #Hregs
     1671cases(bind_new_bind_new_instantiates … Hregs (bind_new_bind_new_instantiates … Hinit
     1672 (return_commutation ?????????? good … Hbl EQfetch … EQssize … EQpop … EQcall …
     1673   Rst1st2 t_fn EQt_fn))) #EQ destruct(EQ) * #st_fin * #EQst_fin * #t_st_pop * #t_pc_pop
     1674** #EQt_pop #EQt_pc_pop @eqZb_elim #Hbl_pcpop normalize nodelta
     1675[ #sem_rel (*premain case TODO *) cases daemon ]
     1676cases(fetch_statement_sigma_stored_pc … good … Hbl_pcpop … EQcall) #data1 * #Hinit1
     1677normalize nodelta *** #pre_c #instr_c #post_c * #Hregs1 * #pc1 * destruct(EQt_pc_pop)
     1678whd in match sigma_stored_pc in ⊢ (% → ?); normalize nodelta
     1679inversion(sigma_pc_opt ???????? t_pc_pop)
     1680[ #ABS cases(fetch_statement_inv … EQcall) >fetch_internal_function_no_zero [#EQ destruct(EQ)]
     1681  whd in match sigma_stored_pc; normalize nodelta >ABS %]
     1682#pc2 #EQpc2 normalize nodelta inversion(sigma_pc_opt ?????????)
     1683[ #_ normalize nodelta #EQ destruct(EQ) cases(fetch_statement_inv … EQcall)
     1684  >fetch_internal_function_no_zero [2: whd in match sigma_stored_pc; normalize nodelta >EQpc2 %]
     1685  #EQ destruct(EQ) ]
     1686#pc3 #EQpc3 normalize nodelta #EQ destruct(EQ) <EQpc2 in EQpc3; #H lapply(sym_eq ??? H) -H #H
     1687lapply(sigma_stored_pc_inj … H) [ >EQpc2 % #EQ destruct] #EQ destruct(EQ) * #t_fn1 * #nxt1
     1688* #pre * #post @eq_identifier_elim
     1689[ #EQentry cases(entry_is_cost … (pi2 ?? fn1)) #nxt1 * #c <EQentry #ABS
     1690  cases(fetch_statement_inv … EQcall) #_ normalize nodelta >ABS #EQ destruct(EQ) ]
     1691#_ cut(∀x : bool.andb x false = false) [* %] #EQ >EQ -EQ normalize nodelta ***
     1692cases(bind_new_bind_new_instantiates … (bind_instantiates_to_instantiate … Hregs1)
     1693 (bind_new_bind_new_instantiates … (bind_instantiates_to_instantiate … Hinit1)
     1694  ((call_is_call … good … (proj1 … (fetch_statement_inv … EQcall))) id args dest ?)) (point_of_pc p_in pc1))
     1695#id' * #args' * #dest' #EQ >EQ -EQ #EQt_call #EQpre_c #EQpost_c #EQnxt1 #H
     1696cases(bind_new_bind_new_instantiates … (bind_instantiates_to_instantiate … Hregs1)
     1697      (bind_new_bind_new_instantiates … (bind_instantiates_to_instantiate … Hinit1) H))
     1698-H #st2' * #EQst2' #fin_sem_rel
     1699%{(mk_state_pc ? st_fin (pc_of_point p_out (pc_block (pc … st2)) mid) (last_pop … st2))}
     1700%{(next p_out nxt1
     1701   (set_last_pop p_out (decrement_stack_usage ? ssize t_st_pop) pc1))}
     1702%{(mk_state_pc ? st2' (pc_of_point p_out (pc_block pc1) next_of_call) pc1)}
     1703%{((taaf_to_taa …
     1704     (produce_trace_any_any_free ? st2 f t_fn … EQt_fn EQpre EQst_fin) ?))}
     1705[ @if_elim #_ [2: @I] % whd in ⊢ (% → ?); whd in match (as_label ??);
     1706  whd in match fetch_statement; normalize nodelta >EQt_fn >m_return_bind
     1707  >point_of_pc_of_point >EQt_stmt >m_return_bind normalize nodelta * #H @H % ]
     1708letin trans_prog ≝ (b_graph_transform_program p_in p_out init prog)
     1709lapply(produce_trace_any_any_free (mk_prog_params p_out trans_prog stack_size) ??????????)
     1710[11: * #taaf * #_ #prf %{taaf}
     1711|3: change with (pc_block pc1) in match (pc_block ?);
     1712    @(proj1 … (fetch_statement_inv … EQt_call))
     1713|2: whd in match next; whd in match succ_pc; whd in match set_pc;
     1714    whd in match point_of_pc; normalize nodelta whd in match pc_of_point;
     1715    normalize nodelta >point_of_offset_of_point in ⊢ (????%???);
     1716    whd in match (point_of_succ ???); @EQpost_c
     1717|1: assumption
     1718|*:
     1719]
     1720%
     1721[ %
     1722  [ %
     1723    [ %
     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 % ]
     1735    ]
     1736    whd [ whd in match (as_classify ??); | whd in match eval_state; normalize nodelta]
     1737    whd in match fetch_statement; normalize nodelta >EQt_fn >m_return_bind
     1738    >point_of_pc_of_point >EQt_stmt [%] >m_return_bind whd in match eval_statement_no_pc;
     1739    normalize nodelta >m_return_bind whd in match eval_statement_advance;
     1740    whd in match eval_return; normalize nodelta whd in match (stack_sizes ????);
     1741    >EQssize >m_return_bind >EQt_pop >m_return_bind whd in match next_of_call_pc;
     1742    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)
     1745    [3: change with (pc_block pc1) in match (pc_block ?);
     1746        lapply(proj1 ?? (fetch_statement_inv … EQcall)) <pc_block_eq in ⊢ (% → ?);
     1747        [2: >EQpc2 % #EQ destruct] #H @H
     1748    |1,2:
     1749    | <pc_block_eq in fin_sem_rel; [2: >EQpc2 % #EQ destruct] #H @H
     1750    | %
     1751    ]
     1752  ]
     1753]   
     1754whd * #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
     1756whd in ⊢ (% → ?); >EQfetch_call normalize nodelta * #EQpc1_pc_s1_pre  #EQsucc_pc
     1757whd in ⊢ (% → ?); #EQpc_s1_pre >EQpc_s1_pre in EQfetch_call; #EQfetch_call
     1758cases(fetch_statement_sigma_stored_pc … good … EQfetch_call)
     1759[2: <EQpc_s1_pre % #ABS elim Hbl_pcpop #H @H -H >EQpc1_pc_s1_pre assumption ]
     1760#data2 * #EQdata2 normalize nodelta * #bl2 * #EQbl2 * #pc3 * #EQstored
     1761lapply(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 % ]
     1764#EQ destruct(EQ) * #fn' * #nxt'' * #l1 * #l2 @eq_identifier_elim
     1765[ #EQentry cases(fetch_statement_inv … EQfetch_call) #_ >EQentry normalize nodelta
     1766  cases(entry_is_cost … (pi2 ?? calling)) #nxt1 * #c #EQ >EQ #EQ1 destruct]
     1767#_ cut(∀b : bool.andb b false = false) [ * //] #EQ >EQ -EQ normalize nodelta
     1768*** #EQt_fetch_call #_ #_ #EQnxt' whd >EQt_fetch_call normalize nodelta
     1769cut(? : Prop)
     1770[3: whd in match (last_pop ??); #H %{H}
     1771|2: @(stored_pc_inj p_in p_out prog stack_size init init_regs f_lbls f_regs … )
     1772  [ % #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
     1775|]
     1776destruct(H)
     1777cut(nxt'' = nxt1) [2: #EQ destruct whd in ⊢ (??%%); % ]
     1778cut(nxt' = next_of_call)
     1779[ lapply EQsucc_pc whd in match (succ_pc); normalize nodelta
     1780  whd in match (point_of_succ ???); whd in match (point_of_succ ???);
     1781  whd in ⊢ (??%% → ?); cases next_of_call #x cases nxt' #y
     1782  whd in match (offset_of_point ??); whd in match (offset_of_point ??);
     1783  #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) % ]
     1784#EQ destruct(EQ) >EQcall in EQfetch_call; >EQt_call in EQt_fetch_call;
     1785whd in ⊢ (? → ??%? → ?); #EQ1 #EQ2 lapply(eq_to_jmeq ??? EQ1) -EQ1 #EQ1 destruct(EQ1) %
     1786qed.
     1787
     1788
     1789theorem joint_correctness : ∀p_in,p_out : sem_graph_params.
     1790∀prog : joint_program p_in.∀stack_size : ident → option ℕ.
     1791∀init : (∀globals.joint_closed_internal_function p_in globals →
     1792         bound_b_graph_translate_data p_in p_out globals).
     1793∀init_regs : block → list register.∀f_lbls : lbl_funct_type.
     1794∀f_regs : regs_funct_type.∀st_no_pc_rel : joint_state_relation p_in p_out.
     1795∀st_rel : joint_state_pc_relation p_in p_out.
     1796good_state_relation p_in p_out prog stack_size init init_regs
     1797 f_lbls f_regs st_no_pc_rel st_rel →
     1798let trans_prog ≝ b_graph_transform_program … init prog in
     1799∀init_in.make_initial_state (mk_prog_params p_in prog stack_size) = OK ? init_in →
     1800∃init_out.make_initial_state (mk_prog_params p_out trans_prog stack_size) = OK ? init_out ∧
     1801∃[1] R.
     1802  status_simulation_with_init
     1803    (joint_abstract_status (mk_prog_params p_in prog stack_size))
     1804    (joint_abstract_status (mk_prog_params p_out trans_prog stack_size))
     1805    R init_in init_out.
     1806cases daemon
     1807qed.
     1808
     1809
Note: See TracChangeset for help on using the changeset viewer.