Changeset 2556


Ignore:
Timestamp:
Dec 14, 2012, 2:54:06 PM (7 years ago)
Author:
tranquil
Message:

in joint semantics and traces: added a last popped calling address to state_pc, in order to have a strong enough as_after_return in joint (due to graph languages having one-to-many predecessors)
in lineariseProof: one axiom left (tailcall case)

Location:
src/joint
Files:
3 edited

Legend:

Unmodified
Added
Removed

  • src/joint/Traces.ma

    r2553 r2556  
    55 { globals: list ident
    66 ; sparams:> sem_params
    7  ; exit: program_counter
    87 ; ev_genv: genv sparams globals
    98(* ; io_env : state sparams → ∀o:io_out.res (io_in o) *)
    … …  
    4746≝
    4847λpars.
    49 (* Invariant: a -1 block is unused in common/Globalenvs *)
    50 let b ≝ mk_block Code (-1) in
    51 let ptr ≝ mk_program_counter «b, refl …» one in
    5248let p ≝ prog pars in
    5349mk_evaluation_params
    5450  (prog_var_names … p)
    5551  (prog_spars pars)
    56   ptr
    5752  (mk_genv_gen ?? (globalenv_noinit ? p) ? (stack_sizes pars))
    5853 (* (prog_io pars) *).
    … …  
    7671  let m ≝ alloc_mem … p in
    7772  let 〈m,spb〉 ≝ alloc … m 0 external_ram_size XData in
    78   let 〈m,ispb〉 ≝ alloc … m 0 internal_ram_size XData in
    79   let dummy_pc ≝ mk_program_counter «mk_block Code (-1), refl …» one in
    8073  let spp : xpointer ≝
    8174    «mk_pointer spb (mk_offset (bitvector_of_Z ? external_ram_size)),
    … …  
    8477  let main ≝ prog_main … p in
    8578  let st0 ≝ mk_state pars (empty_framesT …) empty_is (BBbit false) (empty_regsT … spp) m in
    86   (* use exit sem_globals as ra and call_dest_for_main as dest *)
    87   let st0' ≝ mk_state_pc … (set_sp … spp st0) (exit sem_globals) in
    88   ! st0'' ← save_frame ?? sem_globals true (call_dest_for_main … pars) st0' ;
    89   let st_pc0 ≝ mk_state_pc ? st0'' dummy_pc in
    90   ! bl ← block_of_call … ge (inl … main) st_pc0;
     79  (* use exit_pc as ra and call_dest_for_main as dest *)
     80  let st0' ≝ mk_state_pc … (set_sp … spp st0) exit_pc exit_pc in
     81  ! st0_no_pc ← save_frame ?? sem_globals true (call_dest_for_main … pars) st0' ;
     82  let st0'' ≝ set_no_pc … st0_no_pc st0' in
     83  ! bl ← block_of_call … ge (inl … main) st0'';
    9184  ! 〈i, fn〉 ← fetch_function … ge bl ;
    9285  match fn with
    9386  [ Internal ifn ⇒
    94     ! st' ← eval_internal_call … ge i ifn (call_args_for_main … pars) st_pc0 ;
     87    ! st' ← eval_internal_call … ge i ifn (call_args_for_main … pars) st0'' ;
    9588    let pc' ≝ pc_of_point … bl (joint_if_entry … ifn) in
    96     return mk_state_pc … st' pc'
     89    return mk_state_pc … st' pc' exit_pc
    9790  | External _ ⇒ Error … [MSG BadMain; CTX ? main] (* External main not supported: why? *)
    9891  ].
    … …  
    231224  match \snd x with
    232225  [ sequential s next ⇒
     226    last_pop … s2 = pc … s1 ∧
    233227    pc … s2 = succ_pc p (pc … s1) next
    234228  | _ ⇒ False (* never happens *)
    … …  
    374368      ])
    375369   (* as_after_return ≝ *) (joint_after_ret p)
    376    (* as_final ≝ *) (λs.is_final p  (globals ?) (ev_genv p) (exit p) s ≠ None ?)
     370   (* as_final ≝ *) (λs.is_final p  (globals ?) (ev_genv p) exit_pc s ≠ None ?)
    377371   (* as_call_ident ≝ *) (joint_call_ident p)
    378372   (* as_tailcall_ident ≝ *) (joint_tailcall_ident p).

  • src/joint/lineariseProof.ma

    r2555 r2556  
    627627    #p #p' #graph_prog #sigma #st #prf @opt_to_opt_safe qed.
    628628
     629lemma sigma_pc_irr :
     630  ∀p,p',graph_prog,sigma,pc1,pc2,prf1,prf2.
     631  pc1 = pc2 →
     632  sigma_pc p p' graph_prog sigma pc1 prf1 =
     633  sigma_pc p p' graph_prog sigma pc2 prf2.
     634#p #p' #graph_prog #sigma #pc1 #pc2 #prf1 #prf2
     635#EQ destruct(EQ) % qed.
     636
    629637definition well_formed_state_pc :
    630638 ∀p,p',graph_prog,sigma.
    … …  
    632640  state_pc (make_sem_graph_params p p') → Prop ≝
    633641 λp,p',prog,sigma,gsss,st.
    634  well_formed_pc p p' prog sigma (pc … st) ∧ well_formed_state … gsss st.
     642 well_formed_pc p p' prog sigma (last_pop … st) ∧
     643 well_formed_pc p p' prog sigma (pc … st) ∧
     644 well_formed_state … gsss st.
    635645 
    636646definition sigma_state_pc :
    … …  
    646656≝
    647657 λp,p',graph_prog,sigma,gsss,s,prf.
    648  let pc' ≝ sigma_pc … (proj1 … prf) in
     658 let last_pop' ≝ sigma_pc … (proj1 … (proj1 … prf)) in
     659 let pc' ≝ sigma_pc … (proj2 … (proj1 … prf)) in
    649660 let st' ≝ sigma_state … (proj2 … prf) in
    650  mk_state_pc ? st' pc'.
     661 mk_state_pc ? st' pc' last_pop'.
    651662(*
    652663definition sigma_function_name :
    … …  
    660671  ∀M : MonadProps.∀X,Y,f,l.
    661672  All X (λx.∃y.f x = return y) l → ∃l'.m_list_map M X Y f l = return l'.
    662   cases daemon qed.
     673  #M #X #Y #f #l elim l -l
     674  [ * %{[ ]} %
     675  | #hd #tl #IH * * #y #EQ #H cases (IH H) #ys #EQ'
     676    %{(y :: ys)}
     677    change with (! y ← ? ;  ? = ?)
     678    >EQ >m_return_bind
     679    change with (! acc ← m_list_map ????? ; ? = ?) >EQ'
     680    @m_return_bind
     681qed.
    663682
    664683definition helper_def_store__commute :
    … …  
    717736    (λr.pair_reg_move_ ? ? (p' ?) r mv)
    718737    (λr.pair_reg_move_ ? ? (p' ?) r mv)
    719 ; allocate_locals_commute :
     738; allocate_locals__commute :
    720739  ∀loc, r1, prf1. ∃ prf2.
    721740  allocate_locals_ ? ? (p' ?) loc (sigma_regs p p' graph_prog sigma gsss r1 prf1) =
    … …  
    724743  ∀dest,fl.
    725744  preserving … res_preserve …
    726     (λst : state_pc ?.λprf.
    727       mk_state_pc …
    728         (sigma_state … gsss st (proj2 ?? prf))
    729         (sigma_pc p p' graph_prog sigma (pc … st) (proj1 ?? prf)))
     745    (sigma_state_pc … gsss)
    730746    (sigma_state … gsss)
    731747    (save_frame ?? (p' ?) fl dest)
    … …  
    776792  preserving … res_preserve …
    777793    (sigma_state … gsss)
    778     (λst : state_pc ?.λprf.
    779       mk_state_pc …
    780         (sigma_state … gsss st (proj2 ?? prf))
    781         (sigma_pc p p' graph_prog sigma (pc … st) (proj1 ?? prf)))
     794    (sigma_state_pc … gsss)
    782795  (pop_frame ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes))
    783796            curr_id curr_fn)
    … …  
    785798            curr_id (\fst (linearise_int_fun … curr_fn)))
    786799}.
     800
     801lemma wf_set_regs : ∀p,p',graph_prog,sigma,gss,st,r.
     802well_formed_state p p' graph_prog sigma gss st →
     803well_formed_regs … gss r →
     804well_formed_state … gss (set_regs … r st).
     805#p #p' #graph_prog #sigma #gss #st #r
     806*** #H1 #H2 #_ #H4 #H3
     807%{H4} %{H3} %{H2} @H1
     808qed.
     809
     810lemma allocate_locals_def :
     811  ∀p,F,p',loc,locs,st.
     812  allocate_locals p F p' (loc::locs) st =
     813  (let st' ≝ allocate_locals p F p' locs st in
     814   set_regs … (allocate_locals_ p F p' loc (regs … st')) st').
     815#p #F #p' #loc #locs #st % qed.
     816
     817lemma allocate_locals_commute :
     818  ∀p,p',graph_prog,sigma.
     819  ∀gss : good_state_sigma p p' graph_prog sigma.
     820  ∀locs, st1, prf1. ∃ prf2.
     821  allocate_locals ? ? (p' ?) locs (sigma_state … gss st1 prf1) =
     822  sigma_state … gss (allocate_locals ? ? (p' ?) locs st1) prf2.
     823#p #p' #gp #sigma #gss #locs elim locs -locs
     824[ #st1 #prf1 %{prf1} % ]
     825#loc #tl #IH #st1 #prf1
     826letin st2 ≝ (sigma_state … st1 prf1)
     827cases (IH st1 prf1)
     828letin st1' ≝ (allocate_locals ??? tl st1)
     829letin st2' ≝ (allocate_locals ??? tl st2)
     830#prf' #EQ'
     831cases (allocate_locals__commute … gss loc (regs … st1') ?)
     832[2: @hide_prf cases prf' ** // ]
     833#prf'' #EQ''
     834% [ @hide_prf @wf_set_regs assumption ]
     835change with (set_regs ? (allocate_locals_ ??? loc (regs ? st1')) st1')
     836  in match (allocate_locals ??? (loc::tl) st1);
     837change with (set_regs ? (allocate_locals_ ??? loc (regs ? st2')) st2')
     838  in match (allocate_locals ??? (loc::tl) st2);
     839>EQ' >EQ'' %
     840qed.
    787841
    788842lemma store_commute :
    … …  
    15571611    (* call_rel ≝ *) (λs1,s2.
    15581612      ∃prf:well_formed_state_pc p p' graph_prog sigma gss s1.
    1559       pc ? s2 = sigma_pc … (pc ? s1) (proj1 … prf))
     1613      pc ? s2 = sigma_pc … (pc ? s1) (proj2 … (proj1 … prf)))
    15601614    (* sim_final ≝ *) ?.
    15611615#st1 #st2 * #prf #EQ2
    … …  
    15631617>EQ2
    15641618whd in ⊢ (%→%);
    1565 whd in match (exit ?);
    1566 letin exit_pc ≝ (mk_program_counter «mk_block Code (-1), refl …» one)
    15671619#H lapply (opt_to_opt_safe … H)
    15681620@opt_safe_elim -H #res #_ whd in match is_final; normalize nodelta
    … …  
    15701622#H  @('bind_inversion H) -H
    15711623** #id #int_f #stmt
    1572 #stmt_spec cases (fetch_statement_sigma_commute ???????? good (proj1 … prf) stmt_spec)
     1624#stmt_spec cases (fetch_statement_sigma_commute ???????? good (proj2 … (proj1 … prf)) stmt_spec)
    15731625cases stmt in stmt_spec; -stmt normalize nodelta
    15741626[1,3: [ #a #b #_| #a #b #c #d #e] #_ #_ #ABS whd in ABS : (???%); destruct(ABS)]
    … …  
    15981650[ #st #prf @mfr_bind [3: @pop_frame_commute |*:]
    15991651  #st' #prf' @eq_program_counter_elim 
    1600   [ #EQ_pc >(sigma_pc_exit … EQ_pc) normalize nodelta
     1652  [ #EQ_pc normalize nodelta
     1653    change with (sigma_pc ??????) in match (pc ??);
     1654    >(sigma_pc_exit … EQ_pc) normalize nodelta
    16011655    @mfr_bind [3: @read_result_commute |*:]
    16021656    #lbv #prf_lbv @opt_safe_elim #lbv' #EQ_lbv'
    … …  
    16411695qed.
    16421696
     1697lemma as_label_sigma_commute :
     1698  ∀p,p',graph_prog,stack_sizes,sigma,gss.good_sigma p graph_prog sigma →
     1699  ∀st,prf.
     1700  as_label (lin_abstract_status p p' (linearise … graph_prog) stack_sizes)
     1701    (sigma_state_pc p p' graph_prog sigma gss st prf) =
     1702  as_label (graph_abstract_status p p' graph_prog stack_sizes) st.
     1703#p #p' #graph_prog #stack_sizes #sigma #gss #good * #st #pc #popped
     1704** #prf1 #prf2 #prf3
     1705change with (as_label_of_pc ?? = as_label_of_pc ??)
     1706change with (sigma_pc ??????) in match (as_pc_of ??);
     1707change with pc in match (as_pc_of ??);
     1708whd in match sigma_pc; normalize nodelta
     1709@opt_safe_elim #pc'
     1710whd in match sigma_pc_opt; normalize nodelta
     1711@eqZb_elim #Hbl normalize nodelta
     1712[ whd in ⊢ (??%%→??%%); #EQ destruct(EQ)
     1713  whd in match fetch_statement; normalize nodelta
     1714  >(fetch_internal_function_no_minus_one … graph_prog … Hbl)
     1715  >(fetch_internal_function_no_minus_one … (linearise … graph_prog) … Hbl) %
     1716| #H @('bind_inversion H) * #i #f -H
     1717  inversion (fetch_internal_function … (pc_block pc))
     1718  [2: #e #_ whd in ⊢ (??%%→?); #ABS destruct(ABS) ]
     1719  * #i' #f' #EQfetch whd in ⊢ (??%%→?); #EQ destruct(EQ)
     1720  #H @('bind_inversion H) #n #EQsigma whd in ⊢ (??%%→?); #EQ destruct(EQ)
     1721  whd in ⊢ (??%%);
     1722  whd in match fetch_statement; normalize nodelta >EQfetch
     1723  >(fetch_internal_function_transf … graph_prog
     1724    (λvars,fn.\fst (linearise_int_fun … fn)) … EQfetch)
     1725  >m_return_bind >m_return_bind
     1726  cases (good f) * #_ #all_labels_in #spec
     1727  cases (spec … EQsigma) #s ** cases s -s
     1728  [ * [#s|#a#lbl]#nxt|#s|*] normalize nodelta #EQstmt_at #_
     1729  [ * #EQstmt_at' #_ | * [ * #EQstmt_at' #_ | #EQstmt_at' ] | #EQstmt_at' ]
     1730  whd in match point_of_pc; normalize nodelta >point_of_offset_of_point
     1731  >EQstmt_at >EQstmt_at' normalize nodelta %
     1732qed.
     1733 
    16431734lemma set_istack_sigma_commute :
    16441735∀p,p',graph_prog,sigma,gss,st,is,prf1,prf2,prf3.
    … …  
    18411932λA,B,C,D,P,Q,f,g,pr,prf.〈f ? (proj1 … prf), g ? (proj2 … prf)〉.
    18421933
    1843 lemma wf_set_regs : ∀p,p',graph_prog,sigma,gss,st,r.
    1844 well_formed_state p p' graph_prog sigma gss st →
    1845 well_formed_regs … gss r →
    1846 well_formed_state … gss (set_regs … r st).
    1847 #p #p' #graph_prog #sigma #gss #st #r
    1848 *** #H1 #H2 #_ #H4 #H3
    1849 %{H4} %{H3} %{H2} @H1
    1850 qed.
    1851 
    18521934lemma wf_set_is : ∀p,p',graph_prog,sigma,gss,st,is.
    18531935well_formed_state p p' graph_prog sigma gss st →
    … …  
    19071989  [1,2: (* COMMENT, COST_LABEL *) #_ @mfr_return
    19081990  | (* MOVE *) #mv_sig #st #prf'
    1909     @(mfr_bind … (sigma_regs … gss))
    1910     [ @pair_reg_move_commute
    1911     | #r #prf @mfr_return @wf_set_regs assumption
    1912     ]
     1991    @mfr_bind [3: @pair_reg_move_commute |*:]
     1992    #r #prf @mfr_return @wf_set_regs assumption
    19131993  | (* POP *)
    19141994    #a #st #prf
    … …  
    19222002  | (* PUSH *)
    19232003     #a #st #prf
    1924      @(mfr_bind … (sigma_beval p p' graph_prog sigma))
    1925      [ @acca_arg_retrieve_commute
    1926      | #bv #prf_bv
    1927        @(mfr_bind … (sigma_is p p' graph_prog sigma))
    1928        [ @is_push_sigma_commute
    1929        | #is #prf_is @mfr_return @wf_set_is assumption
    1930        ]
    1931      ]
     2004     @mfr_bind [3: @acca_arg_retrieve_commute |*:]
     2005     #bv #prf_bv
     2006     @mfr_bind [3: @is_push_sigma_commute |*:]
     2007     #is #prf_is @mfr_return @wf_set_is assumption
    19322008  | (*C_ADDRESS*)
    19332009    #sy
    … …  
    19542030  | (*C_OPACCS*)
    19552031    #op #a #b #arg1 #arg2 #st #prf
    1956     @(mfr_bind … (sigma_beval p p' graph_prog sigma))
    1957     [ @acca_arg_retrieve_commute ]
     2032    @mfr_bind [3: @acca_arg_retrieve_commute |*: ]
    19582033    #bv1 #bv1_prf
    1959     @(mfr_bind … (sigma_beval p p' graph_prog sigma))
    1960     [ @accb_arg_retrieve_commute ]
     2034    @mfr_bind [3: @accb_arg_retrieve_commute |*: ]
    19612035    #bv2 #bv2_prf
    1962     @(mfr_bind … (combine_strong …
    1963         (sigma_beval p p' graph_prog sigma)
    1964         (sigma_beval p p' graph_prog sigma)))
    1965     [ @beopaccs_sigma_commute ]
     2036    @mfr_bind [3: @beopaccs_sigma_commute |*: ]
    19662037    * #res1 #res2 * #res1_prf #res2_prf
    19672038    @(mfr_bind … (sigma_state … gss))
    … …  
    19742045  | (*C_OP1*)
    19752046    #op #a #arg #st #prf
    1976     @(mfr_bind … (sigma_beval p p' graph_prog sigma))
    1977     [ @acca_retrieve_commute ]
     2047    @mfr_bind [3: @acca_retrieve_commute |*: ]
    19782048    #bv #bv_prf
    1979     @(mfr_bind … (sigma_beval p p' graph_prog sigma))
    1980     [ @beop1_sigma_commute ]
     2049    @mfr_bind [3: @beop1_sigma_commute |*: ]
    19812050    #res #res_prf
    19822051    @mfr_bind [3: @acca_store__commute |*: ]
    … …  
    19842053  | (*C_OP2*)
    19852054    #op #a #arg1 #arg2 #st #prf
    1986     @(mfr_bind … (sigma_beval p p' graph_prog sigma))
    1987     [ @acca_arg_retrieve_commute ]
     2055    @mfr_bind [3: @acca_arg_retrieve_commute |*: ]
    19882056    #bv1 #bv1_prf
    1989     @(mfr_bind … (sigma_beval p p' graph_prog sigma))
    1990     [ @snd_arg_retrieve_commute ]
     2057    @mfr_bind [3: @snd_arg_retrieve_commute |*: ]
    19912058    #bv2 #bv2_prf
    1992     @mfr_bind
    1993     [3: @beop2_sigma_commute |*: ]
     2059    @mfr_bind [3: @beop2_sigma_commute |*: ]
    19942060    * #res1 #carry' #res1_prf
    19952061    @(mfr_bind … (sigma_state … gss))
    … …  
    20442110 qed.
    20452111
    2046 lemma eval_seq_no_call_no_goto_ok :
     2112lemma eval_seq_no_call_ok :
    20472113 ∀p,p',graph_prog.
    20482114 let lin_prog ≝ linearise p graph_prog in
    20492115 ∀stack_sizes.
    2050  ∀sigma.∀gss : good_state_sigma p p' graph_prog sigma.
     2116 ∀sigma.good_sigma p graph_prog sigma →
     2117 ∀gss : good_state_sigma p p' graph_prog sigma.
    20512118 ∀st,st',f,fn,stmt,nxt.no_call ?? stmt →
    20522119 ∀prf : well_formed_state_pc … gss st.
    2053    fetch_statement (make_sem_lin_params p p') …
    2054     (globalenv_noinit ? lin_prog) (pc … (sigma_state_pc … st prf)) =
    2055       return 〈f, \fst (linearise_int_fun … fn),
    2056         sequential … (step_seq (mk_lin_params p) … stmt) it〉 →
    2057    eval_seq_no_pc … (ev_genv … (graph_prog_params … graph_prog stack_sizes))
    2058       f fn stmt st = return st' →
    2059  let st_pc' ≝ mk_state_pc ? st'
    2060   (succ_pc (make_sem_graph_params p p') …
    2061     (pc … st) nxt) in
    2062  ∀prf'.
    2063  succ_pc (make_sem_lin_params p p') (sigma_pc … (pc … st) (proj1 … prf)) it =
    2064    sigma_pc p p' graph_prog sigma
    2065     (succ_pc (make_sem_graph_params p p') (pc … st) nxt) prf' →
    2066  ∃prf''.
     2120   fetch_statement (make_sem_graph_params p p') …
     2121    (globalenv_noinit ? graph_prog) (pc … st) =
     2122      return 〈f, fn,  sequential … (step_seq (mk_graph_params p) … stmt) nxt〉 →
     2123   eval_state … (ev_genv … (graph_prog_params … graph_prog stack_sizes)) st =
     2124    return st' →
     2125 ∃prf'.
    20672126 ∃taf : trace_any_any_free (lin_abstract_status p p' lin_prog stack_sizes)
    20682127  (sigma_state_pc … gss st prf)
    2069   (sigma_state_pc … gss st_pc' prf'').
     2128  (sigma_state_pc … gss st' prf').
    20702129 bool_to_Prop (taaf_non_empty … taf).
    2071 #p #p' #graph_prog #stack_sizes #sigma #gss #st #st' #f #fn #stmt #nxt #stmt_no_call
    2072 #prf #EQfetch' #EQeval #prf' #EQsucc_pc
    2073 cases (eval_seq_no_pc_sigma_commute … gss … EQeval) [2: @(proj2 … prf)]
    2074 #prf'' #EQeval'
    2075 % [ @hide_prf % assumption ]
    2076 %{(taaf_step … (taa_base …) …)} [3: % ]
    2077 [ whd whd in ⊢ (??%?); >EQfetch' normalize nodelta
     2130#p #p' #graph_prog #stack_sizes #sigma #good #gss #st #st' #f #fn #stmt #nxt #stmt_no_call
     2131#prf #EQfetch
     2132whd in match eval_state; normalize nodelta >EQfetch
     2133>m_return_bind whd in match eval_statement_no_pc;
     2134whd in match eval_statement_advance; normalize nodelta
     2135@'bind_inversion #st_no_pc' #EQeval
     2136>no_call_advance [2: assumption]
     2137whd in ⊢ (??%%→?); #EQ destruct(EQ)
     2138cases (fetch_statement_sigma_commute … good … (proj2 … (proj1 … prf)) … EQfetch)
     2139normalize nodelta #_ * #EQfetch' *
     2140#prf_nxt #nxt_spec
     2141lapply (err_eq_from_io ????? EQeval) -EQeval #EQeval
     2142cases (eval_seq_no_pc_sigma_commute … gss … (proj2 … prf) … EQeval)
     2143#st_no_pc_prf
     2144#EQeval'
     2145%{(hide_prf …)} [ %{st_no_pc_prf} %{prf_nxt} cases st in prf; -st #st #pc #popped ** // ]
     2146cases nxt_spec -nxt_spec
     2147[ #nxt_spec %{(taaf_step … (taa_base …) …) I}
     2148| * #nxt_spec #pc_of_label_spec %{(taaf_step … (taa_step … (taa_base …))…) I}
     2149]
     2150[1,6:
     2151  whd whd in ⊢ (??%?); >EQfetch' normalize nodelta
    20782152  whd in match joint_classify_step; normalize nodelta
    20792153  >no_call_other try % assumption
    2080 | whd whd in match eval_state; normalize nodelta >EQfetch' >m_return_bind
     2154|2,5:
     2155  whd whd in match eval_state; normalize nodelta
     2156  change with (sigma_pc ??????) in match (pc ??);
     2157  try >EQfetch' in ⊢ (??%?); >m_return_bind in ⊢ (??%?);
    20812158  whd in match eval_statement_no_pc; normalize nodelta
    2082   >EQeval' >m_return_bind
     2159  try >EQeval' in ⊢ (??%?); >m_return_bind in ⊢ (??%?);
    20832160  whd in match eval_statement_advance; normalize nodelta
    2084   >no_call_advance [2: assumption ]
    2085   whd in match (next ???);
    2086   >EQsucc_pc %
    2087 ]
    2088 qed.
    2089 
    2090 lemma eval_seq_no_call_goto_ok :
    2091  ∀p,p',graph_prog.
    2092  let lin_prog ≝ linearise p graph_prog in
    2093  ∀stack_sizes.
    2094  ∀sigma.∀gss : good_state_sigma p p' graph_prog sigma.
    2095  ∀st,st',f,fn,stmt,nxt.no_call ?? stmt →
    2096  ∀prf : well_formed_state_pc … gss st.
    2097   fetch_statement (make_sem_lin_params p p') …
    2098     (globalenv_noinit ? lin_prog) (pc … (sigma_state_pc … st prf)) =
    2099       return 〈f, \fst (linearise_int_fun … fn),
    2100         sequential … (step_seq (mk_lin_params p) … stmt) it〉 →
    2101    eval_seq_no_pc … (ev_genv … (graph_prog_params … graph_prog stack_sizes))
    2102       f fn stmt st = return st' →
    2103  let st_pc' ≝ mk_state_pc ? st'
    2104   (succ_pc (make_sem_graph_params p p') …
    2105     (pc … st) nxt) in
    2106  ∀prf'.
    2107  fetch_statement (make_sem_lin_params p p') …
    2108    (globalenv_noinit … lin_prog)
    2109      (succ_pc (make_sem_lin_params p p') (sigma_pc … (pc … st) (proj1 … prf)) it) =
    2110    return 〈f, \fst (linearise_int_fun … fn), final (mk_lin_params p) … (GOTO … nxt)〉 →
    2111  pc_of_label (make_sem_lin_params p p') ?
    2112                 (globalenv_noinit ? (linearise p … graph_prog))
    2113                 (pc_block (pc … st))
    2114                 nxt = return sigma_pc p p' graph_prog sigma
    2115     (succ_pc (make_sem_graph_params p p') (pc … st) nxt) prf' →
    2116  ∃prf''.
    2117  ∃taf : trace_any_any_free (lin_abstract_status p p' lin_prog stack_sizes)
    2118   (sigma_state_pc … gss st prf)
    2119   (sigma_state_pc … gss st_pc' prf'').
    2120  bool_to_Prop (taaf_non_empty … taf).
    2121 #p #p' #graph_prog #stack_sizes #sigma #gss #st #st' #f #fn #stmt #nxt #stmt_no_call
    2122 #prf #EQfetch' #EQeval #prf' #EQsucc_pc #EQ_pc_of_label
    2123 cases (eval_seq_no_pc_sigma_commute … gss … EQeval) [2: @(proj2 … prf)]
    2124 #prf'' #EQeval'
    2125 % [ @hide_prf % assumption ]
    2126 %{(taaf_step … (taa_step … (taa_base …)) …)} [7: % ]
    2127 [4: whd whd in ⊢ (??%?); >EQfetch' normalize nodelta
    2128   whd in match joint_classify_step; normalize nodelta
    2129   >no_call_other try % assumption
    2130 |3: whd whd in match eval_state; normalize nodelta >EQfetch' in ⊢ (??%?);
    2131   >m_return_bind in ⊢ (??%?);
    2132   whd in match eval_statement_no_pc; normalize nodelta
    2133   >EQeval' in ⊢ (??%?); >m_return_bind in ⊢ (??%?);
     2161  >no_call_advance try assumption
     2162  whd in match (next ???) in ⊢ (??%?);
     2163  [ >nxt_spec %
     2164  | %
     2165  ]
     2166|3:
     2167  whd whd in ⊢ (??%?); >nxt_spec normalize nodelta %
     2168|4:
     2169  whd whd in match eval_state; normalize nodelta
     2170  >nxt_spec >m_return_bind >m_return_bind
    21342171  whd in match eval_statement_advance; normalize nodelta
    2135   >no_call_advance in ⊢ (??%?); [2: assumption ]
    2136   whd in match (next ???) in ⊢ (??%?);
    2137   >EQsucc_pc in ⊢ (??%?); %
    2138 |1: whd whd in ⊢ (??%?); >EQsucc_pc %
    2139 |5: %* #H @H -H whd in ⊢ (??%?);  >EQsucc_pc %
    2140 |2: whd whd in match eval_state; normalize nodelta
    2141   >EQsucc_pc >m_return_bind >m_return_bind whd in match eval_statement_advance;
    2142   normalize nodelta whd in match goto; normalize nodelta
     2172  whd in match goto; normalize nodelta
    21432173  whd in match (pc_block ?); >pc_block_sigma_commute
    2144   >EQ_pc_of_label %
    2145 |*:
     2174  >pc_of_label_spec %
     2175|7: %* #H @H -H
     2176  whd in ⊢ (??%?); >nxt_spec %
     2177|8:
    21462178]
    21472179qed.
    … …  
    21702202    #bv2 #bv2_prf
    21712203    @(mfr_bind … (λptr.λ_:True.ptr))
    2172     [ lapply bv2_prf lapply bv2 lapply bv1_prf lapply bv1
    2173       @bv_pc_other
    2174       [ #pc1 #p #bv1_prf #bv2 #bv2_prf @res_preserve_error ]
    2175       #bv1 #bv1_no_pc #bv1_prf
    2176       @bv_pc_other
    2177       [ cases bv1 in bv1_prf;
    2178         [||#a #b #c| #a | #a | #a #b | #a #b ] #bv1_prf
    2179         #pc2 #p #bv2_prf @res_preserve_error ]
    2180       #bv2 #bv2_no_pc #bv2_prf
    2181       >sigma_bv_no_pc try assumption
    2182       >sigma_bv_no_pc try assumption
    2183       whd #ptr #EQ %{I EQ}
    2184    ] #ptr *
    2185    @if_elim #_ [ @mfr_return | @res_preserve_error ] %
     2204    [ change with (pointer_of_address 〈?,?〉) in
     2205      match (pointer_of_bevals ?);
     2206      change with (pointer_of_address 〈?,?〉) in
     2207      match (pointer_of_bevals [sigma_beval ??????;?]);
     2208      @sigma_ptr_commute % assumption
     2209    ] #ptr *
     2210    @if_elim #_ [ @mfr_return | @res_preserve_error ] %
    21862211 ]
    21872212|4: #bl * @opt_to_res_preserve #x #EQ %{I} @EQ
    … …  
    21902215qed.
    21912216
    2192    
     2217lemma fetch_function_no_minus_one :
     2218  ∀F,V,i,p,bl.
     2219  block_id (pi1 … bl) = -1 →
     2220  fetch_function … (globalenv (λvars.fundef (F vars)) V i p)
     2221    bl = Error … [MSG BadFunction].
     2222 #F#V#i#p ** #r #id #EQ1 #EQ2 destruct
     2223  whd in match fetch_function; normalize nodelta
     2224  >globalenv_no_minus_one
     2225  cases (symbol_for_block ???) normalize //
     2226qed.
     2227
    21932228lemma eval_call_ok :
    21942229 ∀p,p',graph_prog.
    … …  
    22032238      return 〈f, fn,
    22042239        sequential … (CALL (mk_graph_params p) … called args dest ) nxt〉 →
    2205    eval_seq_advance ?? (ev_genv … (graph_prog_params … graph_prog stack_sizes))
    2206       (CALL … called args dest) nxt st = return st' →
     2240   eval_state … (ev_genv … (graph_prog_params … graph_prog stack_sizes)) st =
     2241    return st' →
    22072242(* let st_pc' ≝ mk_state_pc ? st'
    22082243  (succ_pc (make_sem_graph_params p p') …
    … …  
    22282263#p #p' #graph_prog #stack_sizes #sigma #good #gss #st #st1 #f #fn
    22292264#called #args #dest #nxt #prf #fetch_spec
    2230 cases(fetch_statement_sigma_commute … good (proj1 … prf) … fetch_spec) #_
     2265cases(fetch_statement_sigma_commute … good (proj2 … (proj1 … prf)) … fetch_spec) #_
    22312266normalize nodelta * #lin_fetch_spec #_
     2267whd in match eval_state in ⊢ (%→?); normalize nodelta >fetch_spec
     2268>m_return_bind >m_return_bind whd in match eval_statement_advance;
    22322269whd in match eval_seq_advance; whd in match eval_seq_call; normalize nodelta
    22332270@('bind_inversion) #bl #H lapply (err_eq_from_io ????? H) -H #bl_spec
    … …  
    22362273[2:#H @('bind_inversion H) -H #st' #H #_ @('bind_inversion H) -H #vals #_
    22372274  @'bind_inversion #vals' #_ whd in ⊢ (??%%→?); #ABS destruct(ABS) ]
    2238 #H %
     2275#H lapply (err_eq_from_io ????? H) -H
     2276#H @('bind_inversion H) -H #st_no_pc #save_frame_spec
     2277>m_bind_bind
     2278#H @('bind_inversion H) -H #stack_size #H lapply (opt_eq_from_res ???? H) -H
     2279whd in match (stack_sizes ?);
     2280#stack_size_spec
     2281>m_bind_bind
     2282#H @('bind_inversion H) -H #st_no_pc' #set_call_spec
     2283>m_return_bind whd in ⊢ (??%%→?);
     2284whd in match set_no_pc; normalize nodelta #EQ destruct(EQ)
     2285%
    22392286[  @hide_prf
    22402287  whd in match joint_classify; normalize nodelta >fetch_spec >m_return_bind
    … …  
    22422289  whd in match joint_classify_seq; normalize nodelta
    22432290  >bl_spec >m_return_bind >int_f_spec normalize nodelta %
    2244 | %
     2291| cases(block_of_call_sigma_commute p p' graph_prog sigma gss ?? (proj2 … prf) ?
     2292            bl_spec)
     2293  * #lin_bl_spec
     2294  generalize in match (fetch_function_transf … graph_prog …
     2295      (λvars.transf_fundef … (λf_in.\fst(linearise_int_fun ?? f_in)))
     2296      … int_f_spec : fetch_function … (globalenv_noinit … (linearise … graph_prog)) bl = ?) in ⊢ ?;
     2297  #lin_int_f_spec
     2298  %
    22452299  [ @hide_prf whd in match joint_classify; normalize nodelta >lin_fetch_spec
    22462300    >m_return_bind normalize nodelta whd in match joint_classify_step;
    22472301    whd in match joint_classify_seq; normalize nodelta
    2248     cases bl in bl_spec int_f_spec; #reg #reg_prf -bl #reg_spec #int_f_spec
    2249     cases(block_of_call_sigma_commute p p' graph_prog sigma gss ?? (proj2 … prf) ?
    2250             reg_spec)
    2251     * #EQ >EQ -EQ >m_return_bind
    2252     lapply(fetch_function_transf ?????
    2253       (λvars.transf_fundef … (λf_in.\fst(linearise_int_fun ?? f_in))) ????)
    2254         [
    2255         | @(Internal ? fn)
    2256         | @id
    2257         | assumption assumption
    2258         |
    2259         |
    2260         | %
    2261           [@(prog_vars … graph_prog) 
    2262           |@(prog_funct … graph_prog)
    2263           |@(prog_main … graph_prog)
    2264           ]
    2265         ]
    2266       [>int_f_spec % | | |] #EQ >EQ normalize nodelta %
    2267    | %
    2268      [2: %
    2269          [  change with ((λx.joint_call_ident (lin_prog_params p p' (linearise p graph_prog) stack_sizes)
    2270               (mk_Sig ? ? ? x)) ? = (λx.joint_call_ident ? (mk_Sig ? ? ? x)) ?)
    2271             whd in match joint_call_ident in ⊢ (??(%?)?); normalize nodelta in ⊢ (??(%?)?);
    2272             whd in match (pc ?); >lin_fetch_spec in ⊢ (??(%?)?); normalize nodelta in ⊢ (??%?);
    2273             whd in match joint_call_ident in ⊢ (???(%?)); normalize nodelta in ⊢ (???(%?));
    2274             >fetch_spec in ⊢ (???(%?)); normalize nodelta >bl_spec in ⊢ (???%);
    2275             >m_return_bind in ⊢ (???%);
    2276          |  whd in match eval_state; normalize nodelta
    2277             >lin_fetch_spec in ⊢ (??%?); >m_return_bind in ⊢ (??%?);
    2278              whd in match eval_statement_no_pc; normalize nodelta
    2279              whd in match eval_seq_no_pc; normalize nodelta
    2280              >m_return_bind in ⊢ (??%?);
    2281              whd in match eval_statement_advance; whd in match eval_seq_advance;
    2282              whd in match eval_seq_call; normalize nodelta
     2302    >lin_bl_spec >m_return_bind
     2303    >lin_int_f_spec %
     2304   | cases (save_frame_commute … gss … save_frame_spec) in ⊢ ?;
     2305    [2: @hide_prf cases st in prf; // ]
     2306    #st_no_pc_wf #lin_save_frame_spec
     2307     cases (setup_call_commute … gss … st_no_pc_wf … set_call_spec) in ⊢ ?;
     2308     #st_no_pc_wf' #lin_set_call_spec
     2309     cases (allocate_locals_commute … gss … (joint_if_locals … fn) … st_no_pc_wf')
     2310     #st_no_pc_wf'' #lin_allocate_locals_spec
     2311     cut
     2312      (∃prf.sigma_pc p p' graph_prog sigma (pc_of_point (make_sem_graph_params p p') bl (joint_if_entry ?? fn)) prf =
     2313      pc_of_point (make_sem_lin_params p p') bl 0)
     2314     [ cases (good fn) * #entry_in #_ #_
     2315       % [ @hide_prf % | whd in match sigma_pc; normalize nodelta @opt_safe_elim #pc ]
     2316       whd in match sigma_pc_opt; normalize nodelta
     2317       >eqZb_false whd in match (pc_block ?);
     2318       [2,4: % #EQbl
     2319        >(fetch_function_no_minus_one … graph_prog … EQbl) in int_f_spec;
     2320        whd in ⊢ (???%→?); #ABS destruct(ABS) ]
     2321       normalize nodelta whd in match fetch_internal_function;
     2322       normalize nodelta >int_f_spec >m_return_bind >point_of_pc_of_point
     2323       >entry_in whd in ⊢ (??%%→?); #EQ destruct(EQ) %
     2324     ] * #entry_prf #entry_spec
     2325      % [ @hide_prf %{st_no_pc_wf''} %{entry_prf} @(proj1 … (proj1 … prf)) ]
     2326      % [ whd in match joint_call_ident; normalize nodelta
     2327          >lin_fetch_spec in ⊢ (??match % with [ _ ⇒ ? | _ ⇒ ?]?);
     2328          >fetch_spec in ⊢ (???match % with [ _ ⇒ ? | _ ⇒ ?]);
     2329          normalize nodelta
     2330          >lin_bl_spec >bl_spec >m_return_bind >m_return_bind
     2331          whd in match fetch_internal_function; normalize nodelta
     2332          >lin_int_f_spec >int_f_spec %
     2333        | whd in match eval_state; normalize nodelta
     2334          >lin_fetch_spec in ⊢ (??%?); >m_return_bind in ⊢ (??%?);
     2335           whd in match eval_statement_no_pc; normalize nodelta
     2336           whd in match eval_seq_no_pc; normalize nodelta
     2337           >m_return_bind in ⊢ (??%?);
     2338           whd in match eval_statement_advance; whd in match eval_seq_advance;
     2339           whd in match eval_seq_call; normalize nodelta
     2340           >lin_bl_spec in ⊢ (??%?); >m_return_bind in ⊢ (??%?);
     2341           >lin_int_f_spec in ⊢ (??%?); >m_return_bind in ⊢ (??%?);
     2342           normalize nodelta
     2343           >lin_save_frame_spec >m_return_bind
     2344           >m_bind_bind whd in match (stack_sizes ?);
     2345           >stack_size_spec >m_return_bind
     2346           >lin_set_call_spec >m_return_bind
     2347           >lin_allocate_locals_spec
     2348           <entry_spec %
    22832349         ]
    2284          cases(block_of_call_sigma_commute p p' graph_prog sigma gss ?? (proj2 … prf) ?
    2285              bl_spec) * #EQ >EQ in ⊢ (??%?); >m_return_bind in ⊢ (??%?); -EQ
    2286          [ whd in match fetch_internal_function; normalize nodelta >int_f_spec in ⊢ (???%);
    2287            >m_return_bind in ⊢ (???%); normalize nodelta ]
    2288          lapply(fetch_function_transf ?????
    2289                 (λvars.transf_fundef … (λf_in.\fst(linearise_int_fun ?? f_in))) ????)
    2290             [
    2291             | 2,12: @(Internal ? fn)
    2292             | 3,13: @id
    2293             | 4,14: assumption assumption
    2294             | 5,15:
    2295             | 6,16:
    2296             |7,17: %
    2297                [1,4: @(prog_vars … graph_prog) 
    2298                |2,5: @(prog_funct … graph_prog)
    2299                |3,6: @(prog_main … graph_prog)
    2300                ]
    2301             ]
    2302          [1,5: >int_f_spec % |*:] #EQ >EQ in ⊢ (??%?); -EQ
    2303           >m_return_bind in ⊢ (??%?); normalize nodelta [ %]
    2304       ]
    2305   ]
    2306 ]
    2307 [2: @hide_prf]
    2308 lapply (err_eq_from_io ????? H) -H #H @('bind_inversion H)
    2309 #st' #st_spec' #H @('bind_inversion H) -H #st'' #st_spec''
    2310 whd in ⊢ (??%% → ?); #EQ destruct(EQ) [ % ]
    2311 [2,3: elim(save_frame_commute p p' graph_prog sigma gss … prf … st_spec')
    2312       #wf_st' #sigma_st_spec' [2: >sigma_st_spec' in ⊢ (??%?); >m_return_bind in ⊢ (??%?);]
    2313       lapply st_spec'' -st_spec''  whd in match eval_internal_call; normalize nodelta
    2314       #H @('bind_inversion H) -H #dim_s #dim_s_spec #H
    2315       [ >dim_s_spec in ⊢ (??%?); >m_return_bind in ⊢ (??%?);]
    2316       elim(bind_inversion ????? H) -H #st''' * #st_spec'''
    2317       elim(setup_call_commute p p' graph_prog sigma gss … wf_st' … st_spec''')
    2318       #wf_st''' #sigma_st_spec''' whd in ⊢ (??%% → ?);
    2319       whd in match allocate_locals; whd in match set_regs; normalize nodelta
    2320       #EQ destruct(EQ)
    2321 ]
    2322 [  >sigma_st_spec''' in ⊢ (??%?); >m_return_bind in ⊢ (??%?);
    2323    whd in match sigma_state_pc; normalize nodelta
    2324    change with (return mk_state_pc (make_sem_lin_params p p') ? ? = ?)
    2325    cut(∀A,semp,pc,pc',st,st'.∀ f : ? → A.pc = pc' ∧ st = st' →
    2326           f(mk_state_pc semp st pc) = f(mk_state_pc semp st' pc'))
    2327    [#A #H1 #H2 #H3 #H4 #H5 #f * #H8 #H9 //]
    2328    #APP @APP %
    2329 ]
    2330 [1,4: [whd in match sigma_pc; normalize nodelta @opt_safe_elim #lin_pc | whd in match well_formed_pc;]
    2331       whd in match sigma_pc_opt; normalize nodelta @if_elim
    2332       [1,3: @eqZb_elim [2,4: #_ *] #EQbl cases bl in EQbl int_f_spec; *
    2333             #reg #pos #reg_prf normalize in ⊢ (% → ?);
    2334             #EQbl whd in match fetch_function; normalize nodelta
    2335             >EQbl cases(symbol_for_block ???)
    2336             [1,3: whd in ⊢ (??%% → ?); #ABS destruct(ABS)]
    2337             #id1 >m_return_bind inversion(find_funct_ptr ???)
    2338             [1,3:#_ whd in ⊢ (??%% → ?); #ABS destruct(ABS)]
    2339             #z lapply(globalenv_no_minus_one ??? graph_prog) [1,3: @(λn.[Init_space n])]
    2340             #EQ 
    2341             change with ((find_funct_ptr ? (globalenv_noinit ? graph_prog) ? = ?) → ?)
    2342             change with ((find_funct_ptr ? (globalenv_noinit ? graph_prog) ? = ?)) in EQ;
    2343             cases reg in ⊢ (% → ?);
    2344             [1,3: whd in match find_funct_ptr; normalize nodelta #ABS destruct(ABS)
    2345             |2,4: >EQ #ABS destruct(ABS)
    2346             ]
    2347       |2,4: #_ whd in match fetch_internal_function; normalize nodelta
    2348             whd in match (pc_block ?); >int_f_spec >m_return_bind
    2349              >point_of_pc_of_point lapply(good fn) ** #EQ #_ #_ >EQ -EQ
    2350               >m_return_bind [2:%] whd in ⊢ (??%? → ?); #EQ destruct(EQ)
    2351               %
    2352       ]
    2353 | whd in match sigma_state; normalize nodelta
    2354   cut(∀A,semp,fr,fr',is,is',c,c',r,r',m,m'.∀ f : ? → A.
    2355       fr = fr' ∧ is = is' ∧ c = c' ∧ r = r' ∧ m = m'→
    2356           f(mk_state semp fr is c r m) = f(mk_state semp fr' is' c' r' m'))
    2357   [#A #semp #fr #fr' #is #is' #c #c' #r #r' #m #m' #f **** //]
    2358   #APP @APP % [% [% [% [%]]]] // [whd in match sigma_is; normalize nodelta % |3:
    2359   whd in match sigma_mem; normalize nodelta %]
    2360 |  % [2:  @(proj2 … wf_st')] % [  %  [ @(proj1 … (proj1 … (proj1 … wf_st'))) |
    2361           @(proj2 … (proj1 … (proj1 … wf_st')))] ]
    2362 ]
    2363 [ change with (? = (λx.sigma_regs ? ? ? ? ? (foldr ? ? ? ? x) ?)?)
    2364   [ cut((joint_if_locals (lin_prog_params p p' (linearise p graph_prog) stack_sizes)
    2365    (globals (lin_prog_params p p' (linearise p graph_prog) stack_sizes))
    2366    (\fst  (linearise_int_fun p
    2367                 (globals (graph_prog_params p p' graph_prog stack_sizes)) fn))) = (joint_if_locals (graph_prog_params p p' graph_prog stack_sizes)
    2368    (globals (graph_prog_params p p' graph_prog stack_sizes)) fn))
    2369    [%] #EQ >EQ
    2370     elim(joint_if_locals (graph_prog_params p p' graph_prog stack_sizes)
    2371      (globals (graph_prog_params p p' graph_prog stack_sizes)) fn) in ⊢ (??%(?%));
    2372   | @hide_prf elim x
    2373   ]
    2374 | @hide_prf elim(joint_if_locals (graph_prog_params p p' graph_prog stack_sizes)
    2375      (globals (graph_prog_params p p' graph_prog stack_sizes)) fn)
    2376 ]
    2377 [3,5: whd in match (foldr ? ? ???); @(proj2 … (proj1 … wf_st'))
    2378 |4,6: #locs_t #tl_list #wf_regs_tail whd in match (foldr ? ? ???);
    2379       elim(allocate_locals_commute p p' graph_prog sigma gss locs_t
    2380                ? wf_regs_tail) #wf_regs_locs_t #_ assumption
    2381 |*: normalize nodelta
    2382     [  whd in match (foldr ? ? ???) in ⊢ (??%%); %
    2383     | #locs_t #tl_list #EQtl whd in match (foldr ?????) in ⊢ (??%%);
    2384       >EQtl
    2385       lapply(allocate_locals_commute p p' graph_prog sigma gss locs_t
    2386         (foldr (localsT ?) (regsT ?) (allocate_locals_ ???) (regs ? st') tl_list) ?)
    2387       [2: * #x #H >H % |]
    2388     ]
    2389 ]
     2350       ]
     2351     ]
    23902352qed.         
    23912353               
    23922354lemma eval_goto_ok :
    2393 lemma eval_tailcall_ok
    2394  :
    2395 lemma eval_cond_cond_ok :
    2396 lemma eval_cond_fcond_ok :
     2355 ∀p,p',graph_prog.
     2356 let lin_prog ≝ linearise p graph_prog in
     2357 ∀stack_sizes.
     2358 ∀sigma.good_sigma p graph_prog sigma →
     2359 ∀gss : good_state_sigma p p' graph_prog sigma.
     2360 ∀st,st',f,fn,nxt.
     2361 ∀prf : well_formed_state_pc … gss st.
     2362   fetch_statement (make_sem_graph_params p p') …
     2363    (globalenv_noinit ? graph_prog) (pc … st) =
     2364      return 〈f, fn,  final … (GOTO (mk_graph_params p) … nxt)〉 →
     2365   eval_state … (ev_genv … (graph_prog_params … graph_prog stack_sizes)) st =
     2366    return st' →
     2367 ∃prf'.
     2368 ∃taf : trace_any_any_free (lin_abstract_status p p' lin_prog stack_sizes)
     2369  (sigma_state_pc … gss st prf)
     2370  (sigma_state_pc … gss st' prf').
     2371 bool_to_Prop (taaf_non_empty … taf).
     2372#p #p' #graph_prog #stack_sizes #sigma #good #gss #st #st' #f #fn
     2373#nxt #prf #EQfetch
     2374whd in match eval_state; normalize nodelta >EQfetch
     2375>m_return_bind >m_return_bind
     2376whd in match eval_statement_advance; normalize nodelta
     2377whd in match goto; normalize nodelta
     2378#H lapply (err_eq_from_io ????? H) -H
     2379#H @('bind_inversion H) #pc'
     2380@('bind_inversion EQfetch) * #curr_i #curr_fn #EQfetchfn
     2381#H @('bind_inversion H) -H #stmt' #_ whd in ⊢ (??%%→?);
     2382#EQ destruct(EQ)
     2383>(graph_pc_of_label … EQfetchfn) whd in ⊢ (??%%→??%%→?);
     2384#EQ1 #EQ2 destruct
     2385cases (fetch_statement_sigma_commute … good … (proj2 … (proj1 … prf)) … EQfetch)
     2386normalize nodelta ** #prf' #EQpc_of_label' *
     2387#EQfetch'
     2388-H
     2389%
     2390[ @hide_prf cases st in prf prf'; -st #st #pc #popped ** #H1 #H2 #H3
     2391  #H4 %{H3} %{H1 H4} ]
     2392%{(taaf_step … (taa_base …) …) I}
     2393[ whd whd in ⊢ (??%?); >EQfetch' %
     2394| whd whd in match eval_state; normalize nodelta
     2395  >EQfetch' >m_return_bind >m_return_bind
     2396  whd in match eval_statement_advance; whd in match goto;
     2397  normalize nodelta >pc_block_sigma_commute >EQpc_of_label'
     2398  >m_return_bind %
     2399]
     2400qed.
     2401
     2402lemma eval_cond_ok :
     2403∀p,p',graph_prog.
     2404let lin_prog ≝ linearise p graph_prog in
     2405∀stack_sizes.
     2406∀sigma.good_sigma p graph_prog sigma →
     2407∀gss : good_state_sigma p p' graph_prog sigma.
     2408∀st,st',f,fn,a,ltrue,lfalse.
     2409∀prf : well_formed_state_pc … gss st.
     2410 fetch_statement (make_sem_graph_params p p') …
     2411  (globalenv_noinit ? graph_prog) (pc … st) =
     2412    return 〈f, fn,  sequential … (COND (mk_graph_params p) … a ltrue) lfalse〉 →
     2413 eval_state … (ev_genv … (graph_prog_params … graph_prog stack_sizes)) st =
     2414  return st' →
     2415as_costed (joint_abstract_status (graph_prog_params p p' graph_prog stack_sizes))
     2416  st' →
     2417∃prf'.
     2418∃taf : trace_any_any_free (lin_abstract_status p p' lin_prog stack_sizes)
     2419(sigma_state_pc … gss st prf)
     2420(sigma_state_pc … gss st' prf').
     2421bool_to_Prop (taaf_non_empty … taf).
     2422#p #p' #graph_prog #stack_sizes #sigma #good #gss #st #st' #f #fn
     2423#a #ltrue #lfalse #prf #EQfetch
     2424whd in match eval_state; normalize nodelta >EQfetch
     2425>m_return_bind >m_return_bind
     2426whd in match eval_statement_advance; normalize nodelta
     2427#H @('bind_inversion (err_eq_from_io ????? H))
     2428@bv_pc_other [ #pc' #p #_ whd in ⊢ (??%%→?); #ABS destruct(ABS) ]
     2429#bv #bv_no_pc #EQretrieve
     2430cut
     2431  (∃prf'.acca_retrieve ?? (p' ?) (sigma_state_pc p p' graph_prog sigma gss st prf) a =
     2432    return sigma_beval p p' graph_prog sigma bv prf')
     2433[ @acca_retrieve_commute assumption ]
     2434* #bv_prf >(sigma_bv_no_pc … bv_no_pc) #EQretrieve'
     2435-H #H @('bind_inversion H) *
     2436#EQbool normalize nodelta -H
     2437[ whd in match goto; normalize nodelta
     2438  #H @('bind_inversion H) -H #pc'
     2439  @('bind_inversion EQfetch) * #curr_i #curr_fn #EQfetchfn
     2440  #H @('bind_inversion H) -H #stmt' #_ whd in ⊢ (??%%→?);
     2441  #EQ destruct(EQ)
     2442  >(graph_pc_of_label … EQfetchfn) whd in ⊢ (??%%→??%%→?);
     2443  #EQ1 #EQ2 destruct
     2444| whd in ⊢ (??%%→?);
     2445  #EQ destruct(EQ)
     2446]
     2447#ncost
     2448cases (fetch_statement_sigma_commute … good … (proj2 … (proj1 … prf)) … EQfetch)
     2449normalize nodelta ** #prf' #EQpc_of_label' ** #prf'' **
     2450#EQfetch' #nxt_spec
     2451% [1,3,5,7: @hide_prf
     2452  cases st in prf prf' prf'';
     2453  -st #st #pc #popped ** #H1 #H2 #H3 #H4 #H5
     2454  %{H3} %{H1} assumption ]
     2455%{(taaf_step_jump … (taa_base …) …) I}
     2456[1,4,7,10: whd
     2457  >(as_label_sigma_commute … good) assumption
     2458|2,5,8,11: whd whd in ⊢ (??%?);
     2459  >EQfetch' %
     2460|*: whd whd in match eval_state; normalize nodelta >EQfetch'
     2461  >m_return_bind >m_return_bind
     2462  whd in match eval_statement_advance; normalize nodelta >EQretrieve'
     2463  >m_return_bind >EQbool >m_return_bind normalize nodelta
     2464  [1,2: whd in match goto; normalize nodelta
     2465    >pc_block_sigma_commute >EQpc_of_label' %
     2466  |3: whd in match next; normalize nodelta >nxt_spec %
     2467  |4: whd in match goto; normalize nodelta
     2468    >pc_block_sigma_commute >nxt_spec %
     2469  ]
     2470]
     2471qed.
     2472
    23972473lemma eval_return_ok :
     2474∀p,p',graph_prog.
     2475let lin_prog ≝ linearise p graph_prog in
     2476∀stack_sizes.
     2477∀sigma.∀good : good_sigma p graph_prog sigma.
     2478∀gss : good_state_sigma p p' graph_prog sigma.
     2479∀st,st',f,fn.
     2480∀prf : well_formed_state_pc … gss st.
     2481 fetch_statement (make_sem_graph_params p p') …
     2482  (globalenv_noinit ? graph_prog) (pc … st) =
     2483    return 〈f, fn,  final … (RETURN (mk_graph_params p) … )〉 →
     2484 eval_state … (ev_genv … (graph_prog_params … graph_prog stack_sizes)) st =
     2485  return st' →
     2486joint_classify (lin_prog_params … (linearise … graph_prog) stack_sizes)
     2487  (sigma_state_pc … st prf) = Some ? cl_return ∧
     2488∃prf'.
     2489∃st2_after_ret.
     2490∃taf : trace_any_any_free (lin_abstract_status p p' lin_prog stack_sizes)
     2491st2_after_ret
     2492(sigma_state_pc … gss st' prf').
     2493(if taaf_non_empty … taf then
     2494  ¬as_costed (joint_abstract_status (lin_prog_params p p' (linearise … graph_prog) stack_sizes))
     2495    st2_after_ret
     2496 else True) ∧
     2497eval_state … (ev_genv …  (lin_prog_params … (linearise … graph_prog) stack_sizes))
     2498  (sigma_state_pc … st prf) =
     2499return st2_after_ret ∧
     2500ret_rel … (linearise_status_rel … gss good) st' st2_after_ret.
     2501#p #p' #graph_prog #stack_sizes #sigma #good #gss #st #st' #f #fn
     2502#prf #EQfetch
     2503whd in match eval_state; normalize nodelta >EQfetch
     2504>m_return_bind >m_return_bind
     2505whd in match eval_statement_advance; normalize nodelta
     2506#H lapply (err_eq_from_io ????? H) -H
     2507#H @('bind_inversion H) -H #st1' #EQpop
     2508cut (∃prf'.
     2509  (pop_frame … (ev_genv (lin_prog_params ? p' (linearise ? graph_prog) stack_sizes))
     2510    f (\fst (pi1 ?? (linearise_int_fun ?? fn))) (sigma_state … gss st (proj2 … prf)))
     2511   = return sigma_state_pc … gss st1' prf')
     2512[ @pop_frame_commute assumption ]
     2513* #prf' #EQpop' >m_bind_bind
     2514#H @('bind_inversion H) ** #call_i #call_fn
     2515* [ * [ #s | #a #lbl ] #nxt | #s | * ] normalize nodelta
     2516#EQfetch_ret -H
     2517whd in ⊢ (??%%→?); #EQ destruct(EQ) whd in match (next ???); >graph_succ_pc
     2518cases (fetch_statement_sigma_commute … good … (proj2 … (proj1 … prf)) … EQfetch)
     2519#_ normalize nodelta #EQfetch'
     2520cases (fetch_statement_sigma_commute … good … (proj2 … (proj1 … prf')) … EQfetch_ret)
     2521normalize nodelta
     2522#all_labels_in
     2523* #EQfetch_ret' * #prf'' * [2: * ] #nxt_spec [2:| #EQpc_of_label']
     2524% [1,3: whd in match joint_classify; normalize nodelta
     2525  >EQfetch' >m_return_bind % ]
     2526% [1,3: @hide_prf cases prf' * #_ #H1 #H2 %{H2} %{H1 prf''} ]
     2527[ % [2: %{(taaf_base …)} |]
     2528  % [ %{I} ]
     2529  [ >EQfetch' >m_return_bind >m_return_bind normalize nodelta
     2530    whd in match eval_return; normalize nodelta
     2531    >EQpop' >m_return_bind
     2532    whd in match next_of_pc; normalize nodelta
     2533    >EQfetch_ret' >m_return_bind whd in match next; normalize nodelta
     2534    >nxt_spec %
     2535  | * #s1_pre #s1_call
     2536    cases (joint_classify_call … s1_call)
     2537    * #calling_i #calling * #call_spec * #arg * #dest * #nxt * #bl
     2538    * #called_i * #called ** #EQfetch_call #EQbl #EQfetch_called
     2539    * #s2_pre #s2_call
     2540    whd in ⊢ (%→?); >EQfetch_call * #EQ #_
     2541    * #s1_pre_prf #EQpc_s2_pre
     2542    whd >EQpc_s2_pre
     2543    <(sigma_pc_irr … EQ) [2: @hide_prf @(proj2 … (proj1 … prf')) ]
     2544    >EQfetch_ret' % [ % | >nxt_spec % ]
     2545  ]
     2546| % [2: %{(taaf_step … (taa_base …) …)} |*:]
     2547  [3: % [ % normalize nodelta ]
     2548    [2: >EQfetch' in ⊢ (??%?);
     2549      >m_return_bind in ⊢ (??%?); >m_return_bind in ⊢ (??%?);
     2550      normalize nodelta
     2551      whd in match eval_return; normalize nodelta
     2552      >EQpop' in ⊢ (??%?); >m_return_bind in ⊢ (??%?);
     2553      whd in match next_of_pc; normalize nodelta
     2554      >EQfetch_ret' in ⊢ (??%?); >m_return_bind in ⊢ (??%?);
     2555      whd in match next; normalize nodelta %
     2556    |1: normalize nodelta %* #H @H -H
     2557      whd in ⊢ (??%?); >nxt_spec %
     2558    |3: * #s1_pre #s1_call
     2559      cases (joint_classify_call … s1_call)
     2560      * #calling_i #calling * #call_spec * #arg * #dest * #nxt' * #bl
     2561      * #called_i * #called ** #EQfetch_call #EQbl #EQfetch_called
     2562      * #s2_pre #s2_call
     2563      whd in ⊢ (%→?); >EQfetch_call * #EQ #_
     2564      * #s1_pre_prf #EQpc_s2_pre
     2565      whd >EQpc_s2_pre
     2566      <(sigma_pc_irr … EQ) [2: @hide_prf @(proj2 … (proj1 … prf')) ]
     2567      >EQfetch_ret' %%
     2568    ]
     2569  |1: whd whd in ⊢ (??%?); >nxt_spec %
     2570  |2: whd whd in match eval_state; normalize nodelta
     2571    >nxt_spec >m_return_bind >m_return_bind
     2572    whd in match eval_statement_advance; whd in match goto; normalize nodelta
     2573    whd in match (pc_block ?); >pc_block_sigma_commute
     2574    >EQpc_of_label' >m_return_bind % whd in match (set_pc ???); %
     2575  |*:
     2576  ]
     2577]
     2578qed.
     2579
     2580(* TODO *)
     2581axiom eval_tailcall_ok :
     2582∀p,p',graph_prog.
     2583let lin_prog ≝ linearise p graph_prog in
     2584∀stack_sizes.
     2585∀sigma.good_sigma p graph_prog sigma →
     2586∀gss : good_state_sigma p p' graph_prog sigma.
     2587∀st,st',f,fn,fl,called,args.
     2588∀prf : well_formed_state_pc … gss st.
     2589 fetch_statement (make_sem_graph_params p p') …
     2590  (globalenv_noinit ? graph_prog) (pc … st) =
     2591    return 〈f, fn,  final … (TAILCALL (mk_graph_params p) … fl called args)〉 →
     2592 eval_state … (ev_genv … (graph_prog_params … graph_prog stack_sizes)) st =
     2593  return st' →
     2594  let st2_pre_call ≝ sigma_state_pc … gss st prf in
     2595  ∃is_tailcall, is_tailcall'.
     2596  ∃prf'.
     2597  let st2_after_call ≝ sigma_state_pc … gss st' prf' in
     2598  joint_tailcall_ident (lin_prog_params … (linearise … graph_prog) stack_sizes) «st2_pre_call, is_tailcall'» =
     2599  joint_tailcall_ident (graph_prog_params … graph_prog stack_sizes) «st, is_tailcall» ∧
     2600  eval_state … (ev_genv … (lin_prog_params … (linearise … graph_prog) stack_sizes))
     2601    st2_pre_call = return st2_after_call.
    23982602
    23992603
    … …  
    24322636change with
    24332637  (eval_state (make_sem_graph_params p p') (prog_var_names ???) ?? = ? → ?)
    2434 whd in match eval_state in ⊢ (%→?); normalize nodelta
    2435 @'bind_inversion
    2436 ** #curr_f #curr_fn #stmt #H lapply (err_eq_from_io ????? H) -H #EQfetch_stmt
    2437 cases (fetch_statement_inv … EQfetch_stmt) #EQfetchfn #_
    2438 @'bind_inversion
    2439 #st1_no_pc' #ex lapply (err_eq_from_io ????? ex) -ex #ex #ex_advance
    2440 * #wf_prf #st2_EQ
    2441 
    2442 cases (fetch_statement_sigma_commute … good … (hide_prf … (proj1 … wf_prf)) EQfetch_stmt)
    2443 cases stmt in EQfetch_stmt ex ex_advance; -stmt
     2638#EQeval
     2639@('bind_inversion EQeval)
     2640** #curr_f #curr_fn #stmt #H lapply (err_eq_from_io ????? H) -H #EQfetch
     2641#_ * #prf #EQst2
     2642cases stmt in EQfetch; -stmt
    24442643[ @cond_call_other
    24452644  [ #a #ltrue | #f #args #dest | #s #s_no_call ] #nxt | #s | * ]
    24462645normalize nodelta
    2447 #EQfetch_stmt
    2448 whd in match eval_statement_no_pc in ⊢ (%→?); normalize nodelta
    2449 #ex
    2450 [| whd in match eval_statement_advance in ⊢ (%→?);
    2451   whd in match eval_seq_advance in ⊢ (%→?);
     2646#EQfetch
     2647change with (joint_classify ??) in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]);
     2648[ (* COND *)
     2649  whd in match joint_classify; normalize nodelta;
     2650  >EQfetch in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]);
    24522651  normalize nodelta
    2453 | whd in match eval_statement_advance in ⊢ (%→?);
     2652  #ncost
     2653  cases (eval_cond_ok … good … prf EQfetch EQeval ncost)
     2654  #prf' * #taf #taf_ne
     2655  destruct(EQst2)
     2656  % [2: %{taf} |*:]
     2657  >taf_ne normalize nodelta
     2658  % [ %{I} %{prf'} % ]
     2659  whd >(as_label_sigma_commute … good) %
     2660|  (* CALL *)
     2661  cases (eval_call_ok … good … prf EQfetch EQeval)
     2662  #is_call * #is_call' *
     2663  #prf' * #eq_call #EQeval'
     2664  destruct(EQst2)
     2665  >is_call in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]); normalize nodelta
     2666  #ignore %{«?, is_call'»}
     2667  % [ %{eq_call} %{prf} % ]
     2668  % [2: % [2: %{(taa_base …)} %{(taa_base …)} % [ %{EQeval'} %{prf'} % ]] |*:]
     2669  whd >(as_label_sigma_commute … good) %
     2670| (* SEQ *)
     2671  whd in match joint_classify; normalize nodelta;
     2672  >EQfetch in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]);
    24542673  normalize nodelta
    2455   >(no_call_advance (mk_prog_params (make_sem_graph_params p p')
    2456     graph_prog stack_sizes))   in ⊢ (%→?); try assumption
    2457 ]
    2458 #ex_advance
    2459 #all_labels_in
    2460 letin lin_prog ≝ (linearise … graph_prog)
    2461 lapply (refl … (eval_state …  (ev_genv (mk_prog_params (make_sem_lin_params p p') lin_prog stack_sizes)) st2))
    2462 whd in match eval_state in ⊢ (???%→?);
    2463 >st2_EQ in ⊢ (???%→?); normalize nodelta
    2464 [ (* COND *)
    2465 | (* CALL *)
    2466 | (* SEQ *)
    2467   #ex'
    2468   * #lin_fetch_stmt #next_spec
    2469   whd in match (as_classify ??) in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]);
    2470   >EQfetch_stmt in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]);
    2471   normalize nodelta
    2472   whd in match joint_classify_step;
    2473   normalize nodelta
    2474   >no_call_other in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]);
    2475   try assumption
    2476   normalize nodelta
    2477   >lin_fetch_stmt in ex' : (???%) ⊢ ?; >m_return_bind in ⊢ (???%→?);
    2478   whd in match eval_statement_no_pc in ⊢ (???%→?);
    2479   normalize nodelta
    2480   cases (eval_seq_no_pc_sigma_commute … gss … ex) in ⊢ ?;
    2481   [2: @hide_prf @(proj2 … wf_prf) ]
    2482   #st1_no_pc_wf #EQ >EQ in ⊢ (???%→?); -EQ
    2483    >m_return_bind in ⊢ (???%→?);
    2484   whd in match eval_statement_advance in ⊢ (%→?);
    2485   normalize nodelta
    2486   >(no_call_advance (mk_prog_params (make_sem_lin_params p p')
    2487     lin_prog stack_sizes))   in ⊢ (%→?); try assumption
    2488   whd in match (next ???) in ⊢ (%→?);
    2489   change with (sigma_pc ????? (hide_prf ??)) in match (pc ??) in ⊢ (%→?);
    2490   #ex'
    2491   cases next_spec
    2492   #succ_pc_nxt_wf *
    2493   [ #succ_pc_commute >succ_pc_commute in ex' ⊢ ?;
    2494     #ex'
    2495     % [2: %{(taaf_step … (taa_base …) …)} [2: @ex' ] |*:]
    2496     whd
    2497     [ whd in ⊢ (??%?);
    2498       >lin_fetch_stmt normalize nodelta
    2499       whd in match joint_classify_step; normalize nodelta
    2500       @no_call_other assumption
    2501     | normalize nodelta
    2502       cut (? : Prop)
    2503       [3: #H % [ % [ % | @H ]] |*:]
    2504       [ (* TODO lemma : sem_rel → label_rel *)
    2505         cases daemon
    2506       | whd in ex_advance : (??%%); destruct(ex_advance)
    2507         % [ % assumption | % ]
    2508       ]
    2509     ]
    2510   | #fetch_GOTO
    2511     cases (all_labels_in) #wf_next #_
    2512     cases (pc_of_label_sigma_commute … p' … good … EQfetchfn ?)
    2513     [2: @nxt |3: cases daemon ]
    2514     #wf_next' #EQ
    2515     % [2: %{(taaf_step … (taa_step … (taa_base …) …) …)}
    2516       [3: @ex'
    2517       |2: whd
    2518         whd in match eval_state; normalize nodelta
    2519         >fetch_GOTO in ⊢ (??%?); >m_return_bind in ⊢ (??%?);
    2520          >m_return_bind in ⊢ (??%?);
    2521         whd in match eval_statement_advance; normalize nodelta
    2522         whd in match goto; normalize nodelta
    2523         whd in match (pc_block ?);
    2524         >sigma_pblock_eq_lemma >EQ in ⊢ (??%?); %
    2525       |7: normalize nodelta
    2526         cut (? : Prop)
    2527         [3: #H % [ % [ % | @H ]] |*:]
    2528         [ (* TODO lemma : sem_rel → label_rel *)
    2529           cases daemon
    2530         | whd in ex_advance : (??%%); destruct(ex_advance)
    2531           % [ % assumption | % ]
    2532         ]
    2533       |5: % * #H @H -H whd in ⊢ (??%?); >fetch_GOTO %
    2534       |4: whd whd in ⊢ (??%?);
    2535         >lin_fetch_stmt normalize nodelta
    2536         whd in match joint_classify_step; normalize nodelta
    2537         @no_call_other assumption
    2538       |1: whd whd in ⊢ (??%?);
    2539         >fetch_GOTO normalize nodelta %
    2540       |*:
    2541       ]
    2542     |*:
    2543     ]
    2544   ]
    2545 | (* FIN *)
    2546 ]
    2547 
    2548 #stmt_spec
    2549 
    2550 
    2551 cases (eval_statement_no_pc_sigma_commute … gss … (hide_prf … (proj2 … wf_prf)) ex) in ⊢ ?;
    2552 #wf_st1_no_pc_prf #ex' >ex' in ⊢ (???%→?); >m_return_bind in ⊢ (???%→?);
    2553 
    2554 whd in match (as_classify ??) in ⊢ (?→?→match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]);
    2555 >EQfetch_stmt in ⊢ (?→?→match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]);
    2556 normalize nodelta
    2557 
    2558 normalize nodelta
    2559 [ whd in match joint_classify_step; @cond_call_other
    2560   [ (* COND *) #a #lbltrue #nxt
    2561     #ex whd in match eval_statement_advance in ⊢ (%→%→?); normalize nodelta
    2562     #H @('bind_inversion (err_eq_from_io ????? H)) -H @bv_pc_other
    2563     [ #bv_pc #p #bv whd in ⊢ (??%%→?); #ABS destruct(ABS) ]
    2564     #bv #bv_no_pc #EQretrieve
    2565     cases (retrieve_commute … (acca_retrieve_commute … gss) … wf_st1_no_pc_prf … EQretrieve)
    2566     #ignore >(sigma_bv_no_pc … bv_no_pc)
    2567     change with (acca_retrieve ?? (make_sem_lin_params p p') ?? = ? → ?)
    2568     #EQretrieve' >EQretrieve' in ⊢ (?→%→?); >m_return_bind in ⊢ (?→%→?);
    2569     #H @('bind_inversion H) -H * normalize nodelta #EQbool_of_bv
    2570     >EQbool_of_bv in ⊢ (?→%→?); >m_return_bind in ⊢ (?→%→?); normalize nodelta
    2571     [ whd in match goto; normalize nodelta
    2572       >(graph_pc_of_label … EQfetchfn) whd in ⊢ (??%%→?);
    2573       #EQ destruct(EQ) #ex_advance #ex_advance'
    2574       % [2: %{(tal_base_not_return …)} [3: @ex_advance'
    2575   | (* CALL *) #f #args #dest #nxt
    2576   | (* other *) #stmt #no_call #nxt
    2577   ] normalize nodelta
    2578   [ #ex
    2579     #ex_advance #ex_advance'
    2580   | whd in ⊢ (??%%→?); #EQ destruct(EQ)
    2581     #H @('bind_inversion H) -H #called_block
    2582     #H lapply (err_eq_from_io ????? H) -H #EQcalled_block
    2583     #H @('bind_inversion H) -H * #called * #called_fn
    2584     #H lapply (err_eq_from_io ????? H) -H #EQcalled
     2674  whd in match joint_classify_step; normalize nodelta
     2675  >no_call_other [2: assumption ] normalize nodelta
     2676  cases (eval_seq_no_call_ok … good … prf EQfetch EQeval) [2: assumption ]
     2677  #prf' * #taf #taf_ne
     2678  destruct(EQst2)
     2679  % [2: %{taf} |*:]
     2680  >taf_ne normalize nodelta % [ %{I} ]
     2681  [ %{prf'} % | whd >(as_label_sigma_commute … good) % ]
     2682| (* FIN *) cases s in EQfetch;
     2683  [ (* GOTO *) #lbl #EQfetch
     2684    whd in match joint_classify; normalize nodelta;
     2685    >EQfetch in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]);
    25852686    normalize nodelta
    2586     [ #H lapply (err_eq_from_io ????? H) -H ]
    2587     #H @('bind_inversion H) -H
    2588      | @('bind_inversion H) ] -H #st1_no_pc'' #save_frame_EQ ]
    2589     #ex_advance #ex_advance'
    2590     whd in match joint_classify_seq; normalize nodelta
    2591     >EQcalled_block in ⊢ (?→match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]);
    2592    
    2593     cut (∀p,p',graph_prog,sigma,gss,st,f,bl.
    2594         ∀prf : well_formed_state p p' graph_prog sigma gss st.
    2595         block_of_call (make_sem_graph_params p p') ?
    2596           (globalenv_noinit ? graph_prog) st f = return bl →
    2597         block_of_call (make_sem_lin_params p p') ?
    2598           (globalenv_noinit ? (linearise … graph_prog))
    2599           (sigma_state … st prf) f = return bl)
    2600       [1,3: (*TODO lemma *) cases daemon ] #block_of_call_sigma_commute
    2601       whd in match eval_seq_advance; normalize nodelta
    2602       >(block_of_call_sigma_commute … EQcalled_block) in ⊢ (???%→?);
    2603       >m_return_bind in ⊢ (???%→?);
    2604       >(fetch_function_transf … EQcalled :
    2605         fetch_function … (globalenv_noinit … lin_prog) called_block = ?) in ⊢ (???%→?);
    2606       >m_return_bind in ⊢ (???%→?);
    2607       whd in match (transf_fundef); normalize nodelta
    2608        
    2609        
    2610       #block_of_call_sigma_commute
    2611     @match_int_fun #called_descr #EQcalled_descr
    2612     [ #H @('bind_inversion H) -H #st1_frame_saved #EQ_frame_saved ]
    2613     #ex_advance
    2614     cut
    2615       (∀A,B.∀prog : program (λvars.fundef (A vars)) ℕ.
    2616       ∀trans : ∀vars.A vars → B vars.
    2617       let prog_out : program (λvars.fundef (B vars)) ℕ ≝
    2618         transform_program ??? prog (λvars.transf_fundef … (trans vars)) in
    2619       ∀i.is_function … (globalenv_noinit … prog) i →
    2620        is_function … (globalenv_noinit … prog_out) i) [1,3: (* TODO lemma *) cases daemon ]
    2621     #f_propagate
    2622     letin sigma_function ≝ (λA,B,prog,trans.
    2623       λf : Σi.is_function ? (globalenv_noinit ? prog) i.
    2624       «pi1 ?? f, f_propagate A B prog trans ? (pi2 ?? f)») in ⊢ ?; (* TODO def *)
    2625     cut (∀p,p',graph_prog.
    2626       let lin_prog ≝ linearise ? graph_prog in
    2627       ∀sigma.∀gss : good_state_sigma … graph_prog sigma.
    2628       ∀f,st,fn.
    2629       ∀prf : well_formed_state … gss st.
    2630       function_of_call (make_sem_graph_params p p') … (globalenv_noinit … graph_prog)
    2631         st f = return fn →
    2632       function_of_call (make_sem_lin_params p p') … (globalenv_noinit … lin_prog)
    2633         (sigma_state … gss st prf) f = return sigma_function … fn)
    2634         [1,3: (* TODO lemma *) cases daemon ]
    2635     #function_of_call_sigma_commute
    2636     whd in match joint_classify_step; whd in match joint_classify_seq;
    2637     normalize nodelta #next_spec
    2638     >(function_of_call_sigma_commute … EQcalled) in ⊢ (%→?);
    2639     >m_return_bind in ⊢ (%→?);
    2640     @match_int_fun
    2641     [2,3: #EQdescr' lapply EQdescr'
    2642       >description_of_function_transf in EQdescr';
    2643      
    2644    
    2645     whd in match sigma_beval; normalize nodelta
    2646     cases bv
    2647     [|| #ptr1 #ptr2 #p | #by | #p | #ptr #p | #bv_pc #p ]
    2648     whd in match (sigma_beval_opt ?????) in ⊢ (%→%→?);
    2649     [7: #ignore #_
    2650     #ignore whd in match (opt_safe ???) in ⊢ (%→?); #EQretrieve
    2651     whd in match (bool_of_beval ?) in ⊢ (% → ?);
    2652     3: >no_call_advance [2: @no_call]
    2653  
    2654 
    2655 
    2656 generalize in match wf_pc in ⊢ ?;
    2657 whd in ⊢ (%→?);
    2658 inversion (sigma_pc_opt ?????) in ⊢ (%→?); [ #_ * #ABS elim (ABS ?) % ]
    2659 #lin_pc
    2660 whd in match (sigma_pc_opt) in ⊢ (%→?); normalize nodelta
    2661 >EQfunc_of_block in ⊢ (%→?); >m_return_bind in ⊢ (%→?);
    2662 #H elim (bind_opt_inversion ????? H) in ⊢ ?; -H #lin_pt *
    2663 #EQsigma whd in ⊢ (??%?→?); #EQ destruct(EQ) #_
    2664 elim (good_local … EQsigma) -good_local
    2665 #stmt' *
    2666 change with (stmt_at ?? (joint_if_code ?? graph_fun) ? = ? → ?)
    2667 >EQstmt_at #EQ lapply (sym_eq ??? EQ) -EQ #EQ destruct(EQ)
    2668 #H elim (opt_Exists_elim … H) -H * #lbl_opt #lin_stmt normalize nodelta
    2669 >(prog_if_of_function_transform … fn) in ⊢ (%→?); [2: % ]
    2670 change with graph_fun in match (if_of_function ?? fn) in ⊢ (%→?);
    2671 letin lin_fun ≝ (\fst  (linearise_int_fun p globals graph_fun))
    2672 change with globals in match (prog_var_names ?? graph_prog) in ⊢ (%→?);
    2673 *
    2674 #EQnth_opt ** #opt_lbl_spec #EQ destruct(EQ) #next_spec
    2675 destruct(EQst2)
    2676 whd in match eval_state in ⊢ (???%→?); normalize nodelta
    2677 (* resolve classifier *)
    2678 [ *
    2679   [ #stmt #nxt
    2680     whd in match eval_statement in ⊢ (?→%→?); normalize nodelta
    2681     #EQfetch #EQeval #EQstmt_at #EQnth_opt #next_spec
    2682     whd in match (graph_to_lin_statement ???) in ⊢ (%→?);
    2683     whd in match eval_statement in ⊢ (%→?); normalize nodelta
    2684     elim (IO_bind_inversion ??????? EQeval) #st1_no_pc *
    2685     #EQeval_no_pc #EQeval_pc
    2686     >(eval_seq_no_pc_sigma_commute … EQeval_no_pc)
    2687     [2: (*TODO lemma eval_seq_no_pc_wf *) @hide_prf cases daemon ]
    2688         >m_return_bind
    2689     cases stmt in EQfetch EQeval_no_pc EQeval_pc EQstmt_at EQnth_opt next_spec;
    2690     [14: #f #args #dest
    2691     | #c
    2692     | #lbl
    2693     | #move_sig
    2694     | #a
    2695     | #a
    2696     | #sy #sy_prf #dpl #dph
    2697     | #op #a #b #arg1 #arg2
    2698     | #op #a #arg
    2699     | #op #a #arg1 #arg2
    2700     ||
    2701     | #a #dpl #dph
    2702     | #dpl #dph #a
    2703     | #s_ext
    2704     ]
    2705     [ (* CALL *)
    2706     |(*:*)
    2707       normalize nodelta
    2708       #EQfetch #EQeval_no_pc #EQeval_pc #EQstmt_at #EQnth_opt #next_spec
    2709       whd in match eval_seq_pc; normalize nodelta
    2710       #ex1
    2711       cases next_spec
    2712       [ #EQnext_sigma
    2713         %[2: %{(taaf_step … (taa_base …) ex1 ?)}
    2714          [ cases daemon (* TODO lemma joint_classify_sigma_commute *) ]|]
    2715         normalize nodelta
    2716         cut (? : Prop) [3: #R' % [ %{I R'} ] |*:]
    2717         [ cases daemon (* TODO lemma joint_label_sigma_commute *)
    2718         | %
    2719           [ (* TODO lemma well_formed_state_pc_preserve? *) @hide_prf cases daemon
    2720           | whd in match eval_seq_pc in EQeval_pc;
    2721             whd in EQeval_pc : (??%%); whd in EQeval_pc : (??(????%)?);
    2722             destruct (EQeval_pc)
    2723             whd in ⊢ (??%%);
    2724             change with (sigma_pc ??????) in match
    2725               (pc ? (sigma_state_pc ???????));
    2726             whd in match (succ_pc ????) in ⊢ (??%%);
    2727             whd in match (point_of_succ ???) in ⊢ (??%%);
    2728             >(point_of_pc_sigma_commute … EQfunc_of_block EQsigma)
    2729             whd in match sigma_pc in ⊢ (???%);
    2730             whd in match sigma_pc_opt in ⊢ (???%); normalize nodelta
    2731             @opt_safe_elim #pc'
    2732             >EQfunc_of_block >m_return_bind
    2733             whd in match point_of_pc; normalize nodelta
    2734             >point_of_offset_of_point
    2735             >EQnext_sigma whd in ⊢ (??%?→?);
    2736             whd in match pc_of_point; normalize nodelta
    2737             #EQ destruct(EQ)
    2738             >sigma_pblock_eq_lemma %
    2739           ]
    2740         ]
    2741       | -next_spec #next_spec
    2742         %
    2743      
    2744      
    2745         whd in ⊢ (?→???%→?);
    2746         generalize in ⊢ (??%? → ???(????%) → ?); |*: skip]  | #a #lbltrue #next
    2747   ] #next change with label in next;
    2748 | *
    2749   [ #lbl
    2750   |
    2751   | #fl #f #args
     2687    cases (eval_goto_ok … good … prf EQfetch EQeval)
     2688    #prf' * #taf #taf_ne
     2689    destruct(EQst2)
     2690    % [2: %{taf} |*:]
     2691    >taf_ne normalize nodelta % [ %{I} ]
     2692    [ %{prf'} % | whd >(as_label_sigma_commute … good) % ]
     2693  | (* RETURN *) #EQfetch
     2694    whd in match joint_classify; normalize nodelta;
     2695    >EQfetch in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]);
     2696    normalize nodelta
     2697    cases (eval_return_ok … good … prf EQfetch EQeval)
     2698    #is_ret' *
     2699    #prf' * #after_ret * #taf ** #taf_prf #EQeval' #ret_prf
     2700    destruct(EQst2)
     2701    % [2: % [2: % [2: %{(taa_base …)} %{taf} ]] |*:]
     2702    % [2: whd >(as_label_sigma_commute … good) % ]
     2703    %{ret_prf}
     2704    % [2: %{prf'} % ]
     2705    %{EQeval'}
     2706    %{taf_prf is_ret'}
     2707  | (* TAILCALL *) #fl #called #args #EQfetch
     2708    cases (eval_tailcall_ok … good … prf EQfetch EQeval)
     2709    #is_tailcall * #is_tailcall' *
     2710    #prf' * #eq_call #EQeval'
     2711    destruct(EQst2)
     2712    >is_tailcall in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]); normalize nodelta
     2713    #ignore %{«?, is_tailcall'»}
     2714    %{eq_call}
     2715    % [2: % [2: %{(taa_base …)} %{(taa_base …)} % [ %{EQeval'} %{prf'} % ]] |*:]
     2716    whd >(as_label_sigma_commute … good) %
    27522717  ]
    27532718]
    2754 whd in match eval_statement in ⊢ (?→%→?); normalize nodelta
    2755 #EQfetch #EQeval #EQstmt_at #EQnth_opt #next_spec
    2756 normalize nodelta
    2757 whd in match (graph_to_lin_statement ???) in ⊢ (%→?);
    2758 whd in match eval_statement in ⊢ (%→?); normalize nodelta
    2759 [ >m_return_bind in ⊢ (%→?);
    2760   >m_return_bind in EQeval;
    2761 
    2762 
    2763 
    2764   (* common for all non-call seq *)
    2765   >m_return_bind in ⊢ (%→?);
    2766   whd in ⊢ (??%%→?); #EQ destruct(EQ)
    2767   >m_return_bind in ⊢ (%→?);
    2768 
    2769  
    2770   #ex1
    2771 lapply (refl … (eval_state ? globals (ev_genv (lin_prog_params p p' lin_prog lin_stack_sizes)) st2))
    2772 
    2773 whd in match (point_of_pc ???);
    2774 whd in match (point_of_succ ???);
    2775 whd in match sigma_pc in ⊢ (???%); normalize nodelta @opt_safe_elim
    2776 #pc' #H
    2777 elim (bind_opt_inversion ????? H) #fn * #EQbl
    2778 -H #H 
    2779 elim (bind_opt_inversion ????? H) -H #n * #EQsigma whd in ⊢ (??%?→?);
    2780 #EQ destruct(EQ)
    2781 whd in match (succ_pc ????);
    2782 whd in match (point_of_succ ???);
    2783 change with (point_of_offset ???) in match (point_of_pc ???);
    2784 >point_of_offset_of_point
    2785 whd in match sigma_pc; normalize nodelta @opt_safe_elim
    2786 #pc' whd in match sigma_pc_opt; normalize nodelta
    2787 
    2788  
    2789  
    2790         whd in match (succ_pc ????);
    2791                
    2792         change with next in match (offset_of_point ???) in ⊢ (???%);
    2793 whd in fetch_statement_spec : (??()%);
    2794 cases cl in classified_st1_cl; -cl #classified_st1_cl whd
    2795 [4:
    2796  >rel_st1_st2 -st2 letin lin_prog ≝ (linearise ? graph_prog)
    2797  cases (good (pi1 ?? fn)) [2: cases daemon (* TODO *) ]
    2798  #sigma_entry_is_zero #sigma_spec
    2799  lapply (sigma_spec (point_of_pc … (make_sem_graph_params … p') (pc … st1)))
    2800  -sigma_spec #sigma_spec cases (sigma_spec ??) [3: @opt_to_opt_safe cases daemon (* TO REDO *) |2: skip ]
    2801  -sigma_spec #graph_stmt * #graph_lookup_ok #sigma_spec
    2802  cases (opt_Exists_elim … sigma_spec) in ⊢ ?;
    2803  * #optlabel #lin_stm * #lin_lookup_ok whd in ⊢ (% → ?); ** #labels_preserved
    2804  #related_lin_stm_graph_stm
    2805  
    2806  inversion (stmt_implicit_label ???)
    2807  [ whd in match (opt_All ???); #stmt_implicit_spec #_
    2808    letin st2_opt' ≝ (eval_state …
    2809                (ev_genv (lin_prog_params … lin_prog lin_stack_sizes))
    2810                (sigma_state_pc … wf_st1))
    2811    cut (∃st2': lin_abstract_status p p' lin_prog lin_stack_sizes. st2_opt' = return st2')
    2812    [cases daemon (* TODO, needs lemma? *)] * #st2' #st2_spec'
    2813    normalize nodelta in st2_spec'; -st2_opt'
    2814    %{st2'} %{(taaf_step … (taa_base …) …)}
    2815    [ cases daemon (* TODO, together with the previous one? *)
    2816    | @st2_spec' ]
    2817    %[%] [%]
    2818    [ whd whd in match eval_state in st2_spec'; normalize nodelta in st2_spec';
    2819      >(fetch_statement_sigma_commute … good … fetch_statement_spec) in st2_spec';
    2820      >m_return_bind
    2821      (* Case analysis over the possible statements *)
    2822      inversion graph_stmt in stmt_implicit_spec; normalize nodelta
    2823      [ #stmt #lbl #_ #abs @⊥ normalize in abs; destruct(abs) ]
    2824      XXXXXXXXXX siamo qua, caso GOTO e RETURN
    2825    | cases daemon (* TODO, after the definition of label_rel, trivial *) ]
    2826    ]
    2827  | ....
    2828 qed.
    2829 
    2830 
    2831 
    2832 
    2833 
    2834 [ *
    2835   [ *
    2836     [ letin C_COMMENT ≝ 0 in ⊢ ?; #c
    2837     | letin C_COST_LABEL ≝ 0 in ⊢ ?; #lbl
    2838     | letin C_MOVE       ≝ 0 in ⊢ ?; #move_sig
    2839     | letin C_POP        ≝ 0 in ⊢ ?; #a
    2840     | letin C_PUSH       ≝ 0 in ⊢ ?; #a
    2841     | letin C_ADDRESS    ≝ 0 in ⊢ ?; #sy #sy_prf #dpl #dph
    2842     | letin C_OPACCS     ≝ 0 in ⊢ ?; #op #a #b #arg1 #arg2
    2843     | letin C_OP1        ≝ 0 in ⊢ ?; #op #a #arg
    2844     | letin C_OP2        ≝ 0 in ⊢ ?; #op #a #arg1 #arg2
    2845     | letin C_CLEAR_CARRY ≝ 0 in ⊢ ?;
    2846     | letin C_SET_CARRY  ≝ 0 in ⊢ ?;
    2847     | letin C_LOAD       ≝ 0 in ⊢ ?; #a #dpl #dph
    2848     | letin C_STORE      ≝ 0 in ⊢ ?; #dpl #dph #a
    2849     | letin C_CALL       ≝ 0 in ⊢ ?; #f #args #dest
    2850     | letin C_EXT        ≝ 0 in ⊢ ?; #s_ext
    2851     ]
    2852   | letin C_COND ≝ 0 in ⊢ ?; #a #lbltrue
    2853   ] #next change with label in next;
    2854 | *
    2855   [ letin C_GOTO ≝ 0 in ⊢ ?; #lbl
    2856   | letin C_RETURN ≝ 0 in ⊢ ?;
    2857   | letin C_TAILCALL ≝ 0 in ⊢ ?; #fl #f #args
    2858   ]
    2859 ]
     2719qed.

  • src/joint/semantics.ma

    r2551 r2556  
    6868  { st_no_pc :> state semp
    6969  ; pc : program_counter
     70  (* for correctness reasons: pc of last popped calling address (exit_pc at the start) *)
     71  ; last_pop : program_counter
    7072  }.
     73
     74(* special program counter that is guaranteed to not correspond to anything *)
     75definition exit_pc : program_counter ≝
     76  mk_program_counter «mk_block Code (-1), refl …» one.
    7177
    7278definition set_m: ∀p. bemem → state p → state p ≝
    … …  
    8793
    8894definition set_pc: ∀p. ? → state_pc p → state_pc p ≝
    89  λp,pc,st. mk_state_pc … (st_no_pc … st) pc.
     95 λp,pc,st. mk_state_pc … (st_no_pc … st) pc (last_pop … st).
    9096
    9197definition set_no_pc: ∀p. ? → state_pc p → state_pc p ≝
    92  λp,s,st. mk_state_pc … s (pc … st).
     98 λp,s,st. mk_state_pc … s (pc … st) (last_pop … st).
     99
     100definition set_last_pop: ∀p. ? → state_pc p → state_pc p ≝
     101 λp,s,st. mk_state_pc … (st_no_pc … st) (pc … st) s.
    93102
    94103definition set_frms: ∀p:sem_state_params. framesT p → state p → state p ≝
    … …  
    356365 λp,globals,ge,l,st.
    357366  ! newpc ← pc_of_label … ge (pc_block (pc … st)) l ;
    358   return mk_state_pc … st newpc.
     367  return set_pc … newpc st.
    359368
    360369(*
    … …  
    366375 λp,l,st.
    367376 let newpc ≝ succ_pc … (pc … st) l in
    368  mk_state_pc … st newpc.
     377 set_pc … newpc st.
    369378
    370379axiom NoSuccessor : String.
    … …  
    374383  ! 〈id_fn, stmt〉 ← fetch_statement … ge pc ;
    375384  match stmt with
    376   [ sequential _ nxt ⇒ return nxt
     385  [ sequential s nxt ⇒
     386    match s with
     387    [ step_seq _ => return nxt
     388    | COND _ _ => Error … [MSG NoSuccessor]
     389    ]
    377390  | _ ⇒ Error … [MSG NoSuccessor]
    378391  ].
    … …  
    493506! stack_size ← opt_to_res … [MSG MissingStackSize; CTX … i] (stack_sizes … ge i) ;
    494507! st' ← setup_call … stack_size (joint_if_params … globals fn) args st ;
    495 return allocate_locals … p (joint_if_locals … fn) st.
     508return allocate_locals … p (joint_if_locals … fn) st'.
    496509
    497510definition is_inl : ∀A,B.A+B → bool ≝ λA,B,x.match x with [ inl _ ⇒ true | _ ⇒ false ].
    … …  
    507520  ! st'' ← eval_internal_call p globals ge i ifd args st' ;
    508521  let pc ≝ pc_of_point p bl (joint_if_entry … ifd) in
    509   return mk_state_pc … st'' pc
     522  return mk_state_pc … st'' pc (last_pop … st)
    510523| External efd ⇒
    511524  ! st' ← eval_external_call … efd args dest st ;
    512   return mk_state_pc … st' (succ_pc p (pc … st) nxt)
     525  return mk_state_pc … st' (succ_pc p (pc … st) nxt) (last_pop … st)
    513526].
    514527
    … …  
    544557! st' ← pop_frame … ge curr_id curr_fn st ;
    545558! nxt ← next_of_pc … ge (pc … st') ;
    546 return next … nxt st' (* now address pushed on stack are calling ones! *).
     559return
     560  set_last_pop … (pc … st') (next … nxt st') (* now address pushed on stack are calling ones! *).
    547561
    548562definition eval_tailcall ≝
    … …  
    556570  ! st' ← eval_internal_call p globals ge i ifd args st ;
    557571  let pc ≝ pc_of_point p bl (joint_if_entry … ifd) in
    558   return mk_state_pc … st' pc
     572  return mk_state_pc … st' pc (last_pop … st)
    559573| External efd ⇒
    560574  let curr_dest ≝ joint_if_result ?? curr_fn in
    … …  
    604618  ! 〈id,fn,s〉 ← fetch_statement … ge (pc … st) : IO ???;
    605619  ! st' ← eval_statement_no_pc … ge id fn s st : IO ???;
    606   let st'' ≝ mk_state_pc … st' (pc … st) in
     620  let st'' ≝ set_no_pc … st' st in
    607621  eval_statement_advance … ge id fn s st''.
    608622
Note: See TracChangeset for help on using the changeset viewer.