[2590] | 1 | |
---|
[2570] | 2 | (**************************************************************************) |
---|
| 3 | (* ___ *) |
---|
| 4 | (* ||M|| *) |
---|
| 5 | (* ||A|| A project by Andrea Asperti *) |
---|
| 6 | (* ||T|| *) |
---|
| 7 | (* ||I|| Developers: *) |
---|
| 8 | (* ||T|| The HELM team. *) |
---|
| 9 | (* ||A|| http://helm.cs.unibo.it *) |
---|
| 10 | (* \ / *) |
---|
| 11 | (* \ / This file is distributed under the terms of the *) |
---|
| 12 | (* v GNU General Public License Version 2 *) |
---|
| 13 | (* *) |
---|
| 14 | (**************************************************************************) |
---|
| 15 | |
---|
[2898] | 16 | |
---|
| 17 | include "joint/StatusSimulationHelper.ma". |
---|
[2785] | 18 | include "ERTL/ERTLtoERTLptrUtils.ma". |
---|
[2570] | 19 | |
---|
| 20 | |
---|
| 21 | |
---|
[2783] | 22 | (* |
---|
| 23 | lemma get_internal_function_from_ident_ok : |
---|
| 24 | ∀p : sem_params. ∀globals : list ident. ∀ge : genv_t (joint_function p globals). |
---|
| 25 | ∀bl,f,fn. fetch_internal_function ? ge bl = return 〈f,fn〉 → |
---|
| 26 | get_internal_function_from_ident p globals ge f= return fn. |
---|
| 27 | #p #globals #ge #bl #f #fn #EQf |
---|
| 28 | @('bind_inversion EQf) * #f1 * #fn1 whd in match fetch_function; |
---|
| 29 | normalize nodelta #H lapply(opt_eq_from_res ???? H) -H #H @('bind_inversion H) -H |
---|
| 30 | #f2 #EQf2 #H @('bind_inversion H) -H #fn2 #EQfn2 whd in ⊢ (??%% → ??%% → ?); |
---|
| 31 | #EQ1 #EQ2 destruct whd in match get_internal_function_from_ident; normalize nodelta |
---|
| 32 | >(symbol_of_block_rev … EQf2) >m_return_bind |
---|
| 33 | cut(code_block_of_block bl = return bl) |
---|
| 34 | [ whd in match code_block_of_block; normalize nodelta @match_reg_elim |
---|
| 35 | [ >(pi2 ?? bl) #ABS destruct] elim bl #bl1 #EQ #prf % ] #EQbl >EQbl |
---|
| 36 | >m_return_bind >EQf % |
---|
| 37 | qed. |
---|
| 38 | *) |
---|
| 39 | |
---|
| 40 | |
---|
[2570] | 41 | |
---|
[2783] | 42 | |
---|
| 43 | (* |
---|
| 44 | whd in match sigma_frames_opt; whd in match m_list_map; normalize nodelta |
---|
| 45 | whd in match sigma_state in ⊢ (???????%%); normalize nodelta |
---|
| 46 | cases(st_frms … st) normalize nodelta [ @res_preserve_error1] |
---|
| 47 | * #loc_mem #bl #tl inversion(sigma_frames ????) |
---|
| 48 | [ #_ normalize nodelta @res_preserve_error1] * #loc_mem1 #bl1 #tl1 |
---|
| 49 | whd in match sigma_frames; normalize nodelta inversion(sigma_frames_opt ????) |
---|
| 50 | [ #_ normalize nodelta #_ #ABS destruct] #l whd in match sigma_frames_opt; |
---|
| 51 | whd in match m_list_map; normalize nodelta whd in match (foldr ?????); |
---|
| 52 | normalize nodelta inversion(fetch_internal_function ???) |
---|
| 53 | [2: #e #_ whd in ⊢ (??%% → ?); #ABS destruct] * #id1 #fn1 #EQfn1 >m_return_bind |
---|
| 54 | normalize nodelta #H @('bind_inversion H) -H #l1 |
---|
| 55 | change with (sigma_frames_opt ???? = ? → ?) #EQl1 |
---|
| 56 | cut (sigma_frames prog f_lbls f_regs tl = l1) |
---|
| 57 | [whd in match sigma_frames; normalize nodelta >EQl1 %] #EQl11 |
---|
| 58 | cases l [ whd in ⊢ (??%? → ?); #EQ destruct] #x #y |
---|
| 59 | whd in ⊢ (??%? → ?); #EQ1 #_ #EQ2 destruct @mfr_bind1 |
---|
| 60 | [2: whd in match set_regs; whd in match set_frms; normalize nodelta |
---|
| 61 | >EQl1 in ⊢ (???????%?); normalize nodelta |
---|
| 62 | cut(sigma_regs prog f_lbls (added_registers ERTL (prog_var_names … prog) fn1 (f_regs bl1)) |
---|
| 63 | 〈loc_mem,\snd (regs … st)〉 = 〈map RegisterTag beval beval loc_mem |
---|
| 64 | (λbv:beval.sigma_beval prog f_lbls bv)∖ |
---|
| 65 | added_registers ERTL (prog_var_names … prog) fn1 (f_regs bl1), |
---|
| 66 | \snd (sigma_regs prog f_lbls restr (regs ERTLptr_semantics st))〉) |
---|
| 67 | [ whd in match sigma_regs; normalize nodelta @eq_f2 [ %] cases(regs ? st) |
---|
| 68 | #x #y %] #EQ <EQ -EQ |
---|
| 69 | change with (sigma_state ???? (set_regs ERTL_semantics 〈loc_mem,\snd (regs … st)〉 |
---|
| 70 | (set_frms ERTL_semantics tl st))) in ⊢ (???????(??%)?); |
---|
| 71 | @pop_ra_ok | |
---|
| 72 | | * #st1 #pc1 @if_elim [2: #_ @res_preserve_error1] normalize nodelta |
---|
| 73 | @eq_block_elim [2: #_ *] #EQbl1 * @if_elim |
---|
| 74 | [2: >EQbl1 @eq_block_elim [#_ *] * #H @⊥ @H <pc_block_eq [%] % |
---|
| 75 | cases bl1 in EQbl1 EQfn1; #p1 #p2 #EQ destruct lapply p2 |
---|
| 76 | whd in match sigma_stored_pc; normalize nodelta cases(sigma_pc_opt ???) |
---|
| 77 | normalize nodelta [2: #pc2] #p2 [#_ #EQ destruct] |
---|
| 78 | >fetch_internal_function_no_zero [2: %] #EQ destruct |
---|
| 79 | ] @eq_block_elim [2: #_ *] #EQbl11 * @mfr_return_eq1 normalize nodelta |
---|
| 80 | cases bl1 in EQbl11 EQfn1; #p1 #p2 #EQ destruct |
---|
| 81 | lapply p2 cases(pc_block pc1) #p11 #p22 #e #EQfn1 >EQfn1 |
---|
| 82 | % |
---|
| 83 | ] |
---|
| 84 | qed. |
---|
| 85 | *) |
---|
| 86 | |
---|
| 87 | |
---|
| 88 | definition ERTLptrStatusSimulation : |
---|
| 89 | ∀ prog : ertl_program. |
---|
| 90 | let trans_prog ≝ ertl_to_ertlptr prog in |
---|
| 91 | ∀stack_sizes.∀ f_lbls : lbl_funct. ∀ f_regs : regs_funct. |
---|
| 92 | ∀f_bl_r. |
---|
| 93 | b_graph_transform_program_props ERTL_semantics ERTLptr_semantics |
---|
| 94 | translate_data prog f_bl_r f_lbls f_regs → |
---|
| 95 | status_rel (ERTL_status prog stack_sizes) (ERTLptr_status trans_prog stack_sizes) ≝ |
---|
| 96 | λprog,stack_sizes,f_lbls,f_regs,f_lb_r,good. |
---|
| 97 | let trans_prog ≝ ertl_to_ertlptr prog in |
---|
| 98 | mk_status_rel ?? |
---|
| 99 | (* sem_rel ≝ *) (λs1:ERTL_status prog stack_sizes |
---|
| 100 | .λs2:ERTLptr_status trans_prog stack_sizes |
---|
| 101 | .s1=sigma_state_pc prog f_lbls f_regs s2) |
---|
| 102 | (* call_rel ≝ *) |
---|
| 103 | (λs1:Σs:ERTL_status prog stack_sizes |
---|
| 104 | .as_classifier (ERTL_status prog stack_sizes) s cl_call |
---|
| 105 | .λs2:Σs:ERTLptr_status trans_prog stack_sizes |
---|
| 106 | .as_classifier (ERTLptr_status trans_prog stack_sizes) s cl_call |
---|
| 107 | . |
---|
| 108 | pc (mk_prog_params ERTL_semantics prog stack_sizes) s1 |
---|
| 109 | =sigma_stored_pc prog f_lbls |
---|
| 110 | (pc |
---|
| 111 | (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_sizes) |
---|
| 112 | s2)) |
---|
| 113 | (* sim_final ≝ *) ?. |
---|
| 114 | cases daemon |
---|
| 115 | qed. |
---|
| 116 | |
---|
[2662] | 117 | include "joint/semantics_blocks.ma". |
---|
| 118 | |
---|
| 119 | |
---|
[2666] | 120 | |
---|
[2783] | 121 | lemma as_label_ok : ∀ prog : ertl_program. |
---|
| 122 | let trans_prog ≝ ertl_to_ertlptr prog in |
---|
| 123 | ∀ f_lbls,f_regs,stack_sizes. |
---|
| 124 | ∀f_bl_r. |
---|
| 125 | b_graph_transform_program_props ERTL_semantics ERTLptr_semantics |
---|
[2843] | 126 | (λglobals,fn.«translate_data globals fn,(refl …)») prog f_bl_r f_lbls f_regs → |
---|
[2783] | 127 | ∀st,fn,id,stmt. |
---|
| 128 | fetch_statement ERTL_semantics (prog_var_names … prog) |
---|
| 129 | (globalenv_noinit … prog) (pc … (sigma_state_pc prog f_lbls f_regs st)) = |
---|
| 130 | return 〈id,fn,stmt〉 → |
---|
| 131 | as_label (ERTLptr_status trans_prog stack_sizes) st = as_label |
---|
| 132 | (ERTL_status prog stack_sizes) (sigma_state_pc prog f_lbls f_regs st). |
---|
| 133 | #prog #f_lbls #f_regs #stack_size #f_lb_r #good #st #fn #id #stmt #EQfetch |
---|
| 134 | whd in match as_label; normalize nodelta change with (pc ? ?) in ⊢ (??(??%)(??%)); |
---|
| 135 | cases(b_graph_transform_program_fetch_statement … good … EQfetch) |
---|
| 136 | #init_data * #t_fn ** #EQt_fn whd in ⊢ (% → ?); cases(f_lb_r ?) |
---|
| 137 | normalize nodelta [2: #r #tl *] #EQinit destruct(EQinit) * #l_labs * #l_regs ** |
---|
| 138 | #_ #_ cases stmt in EQfetch; |
---|
| 139 | [ * [ #c | * [ #c_id | #c_ptr ] #c_arg #c_dest | #reg #lbl | #s ] #nxt | #fin | * ] |
---|
| 140 | #EQfetch normalize nodelta * #bl * [1,2,3,4,5: >if_merge_right in ⊢ (% → ?); try %] |
---|
| 141 | whd in ⊢ (%→?); cases l_regs normalize nodelta [2,4,5,8,10,12: [3: *] #x #y *] |
---|
| 142 | [1,2,4,5,6:| #r #tl whd in ⊢ (% → ?); cases tl -tl normalize nodelta [2: #r1 #tl1 *]] |
---|
| 143 | #EQ destruct(EQ) |
---|
| 144 | [1,2,3,4,6: * #pre_l * #mid1 * #mid2 * #post_l *** #EQmid1 |
---|
| 145 | whd in match map_eval in ⊢ (% → ?); normalize nodelta |
---|
| 146 | whd in ⊢ (?????%?? → ?); |
---|
| 147 | whd in match (seq_list_in_code ???????) in ⊢ (%→?); * |
---|
| 148 | [1,2,3,4: #EQ1 #EQ2 destruct(EQ1 EQ2) whd in EQmid1 : (???%); |
---|
| 149 | destruct(EQmid1) * #nxt1 * #EQt_stmt #_ #_ |
---|
| 150 | | * #lbl1 * #rest ** #EQ destruct(EQ) * #nxt1 * |
---|
| 151 | #EQt_stmt #_ #_ #_ #_ |
---|
| 152 | ] |
---|
| 153 | | * #pre_l * #mid ** #EQmid whd in ⊢ (% → ?); * #EQ destruct(EQ) |
---|
| 154 | whd in EQmid : (???%); destruct(EQmid) #EQ destruct(EQ) |
---|
| 155 | whd in ⊢ (% → ?); #EQt_stmt |
---|
| 156 | ] |
---|
| 157 | whd in ⊢ (??%%); >EQfetch normalize nodelta whd in match fetch_statement; |
---|
| 158 | normalize nodelta >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in EQt_fn; |
---|
| 159 | #EQt_fn >EQt_fn >m_return_bind >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in EQt_stmt; |
---|
| 160 | #EQt_stmt >EQt_stmt % |
---|
| 161 | qed. |
---|
| 162 | |
---|
[2891] | 163 | include alias "basics/lists/listb.ma". |
---|
[2883] | 164 | |
---|
[2898] | 165 | definition state_rel ≝ λprog : ertl_program.λf_lbls. |
---|
| 166 | λf_regs : (block → label → list register). |
---|
[2940] | 167 | λbl.λ_:label.λst1,st2.∃f,fn. |
---|
[2898] | 168 | fetch_internal_function ? (globalenv_noinit … prog) bl = return 〈f,fn〉 ∧ |
---|
| 169 | let added ≝ added_registers ERTL (prog_var_names … prog) fn (f_regs bl) in |
---|
| 170 | st1 = (sigma_state prog f_lbls f_regs added st2). |
---|
| 171 | |
---|
[2883] | 172 | lemma make_ERTL_To_ERTLptr_good_state_relation : |
---|
| 173 | ∀prog : ertl_program. |
---|
| 174 | let p_out ≝ ertl_to_ertlptr prog in |
---|
| 175 | ∀stack_sizes. |
---|
| 176 | ∃init_regs : block → list register. |
---|
| 177 | ∃f_lbls : block → label → list label. |
---|
| 178 | ∃f_regs : block → label → list register. |
---|
| 179 | ∃good : b_graph_transform_program_props ERTL_semantics ERTLptr_semantics |
---|
| 180 | (λglobals,fn.«translate_data globals fn,(refl …)») |
---|
| 181 | prog init_regs f_lbls f_regs. |
---|
| 182 | good_state_relation ERTL_semantics ERTLptr_semantics prog stack_sizes |
---|
[2898] | 183 | (λglobals,fn.«translate_data globals fn,(refl …)») init_regs f_lbls f_regs |
---|
| 184 | good (state_rel prog f_lbls f_regs) |
---|
| 185 | (sem_rel … (ERTLptrStatusSimulation prog … stack_sizes … good)). |
---|
[2883] | 186 | #prog #stack_sizes |
---|
| 187 | cases(make_b_graph_transform_program_props ERTL_semantics ERTLptr_semantics |
---|
| 188 | (λglobals,fn.«translate_data globals fn,(refl …)») prog) |
---|
| 189 | #init_regs * #f_lbls * #f_regs #good %{init_regs} %{f_lbls} %{f_regs} %{good} |
---|
| 190 | % |
---|
[2898] | 191 | [ #st1 #st2 #f #fn whd in ⊢ (% → ?); #EQ destruct(EQ) #EQfn whd %{f} %{fn} |
---|
| 192 | >EQfn %{(refl …)} whd in match sigma_state_pc; normalize nodelta |
---|
| 193 | lapply EQfn >(fetch_ok_sigma_pc_ok … EQfn) #EQfn1 >EQfn1 % |
---|
| 194 | | #st1 #st2 #f #fn whd in ⊢ (% → ?); #EQ destruct(EQ) #EQfn @fetch_ok_sigma_pc_ok |
---|
| 195 | assumption |
---|
| 196 | | #st1 #st2 #f #fn whd in ⊢ (% → ?); #EQ destruct(EQ) #EQfn |
---|
| 197 | >(fetch_ok_sigma_last_pop_ok … f fn st2 EQfn) % |
---|
| 198 | | #st1 #st2 #pc #lp1 #lp2 #f #fn #EQfn * #f1 * #fn1 * >EQfn whd in ⊢ (??%% → ?); |
---|
| 199 | #EQ destruct(EQ) normalize nodelta #EQ destruct(EQ) #EQ destruct(EQ) whd |
---|
| 200 | whd in match sigma_state_pc; normalize nodelta >EQfn % |
---|
[2883] | 201 | | #st1 #st2 #f #fn #stmt #EQfetch whd in ⊢ (% → ?); #EQ destruct(EQ) |
---|
[2898] | 202 | lapply(as_label_ok … stack_sizes … good st2 … EQfetch) #EQ <EQ in ⊢ (??%?); % |
---|
[2883] | 203 | | normalize nodelta whd in ⊢ (% → % → % → ?); #st1 #st1' #st2 #f #fn |
---|
| 204 | #a #ltrue #lfalse #EQfetch cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt |
---|
| 205 | whd in match eval_state; whd in match eval_statement_no_pc; |
---|
| 206 | normalize nodelta >EQfetch >m_return_bind normalize nodelta >m_return_bind |
---|
| 207 | whd in match eval_statement_advance; normalize nodelta |
---|
| 208 | change with (ps_reg_retrieve ??) in match (acca_retrieve ?????); |
---|
| 209 | #H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H |
---|
| 210 | #bv whd in match set_no_pc; normalize nodelta #EQbv |
---|
| 211 | #H @('bind_inversion H) -H * #EQbool normalize nodelta |
---|
| 212 | [whd in match goto; normalize nodelta >(pc_of_label_eq … EQfn) |
---|
| 213 | >m_return_bind] whd in ⊢ (??%% → ?); #EQ destruct(EQ) |
---|
[2898] | 214 | whd in ⊢ (% → ?); #EQ destruct(EQ) |
---|
| 215 | >(fetch_stmt_ok_sigma_state_ok … EQfetch) in EQbv; |
---|
[2883] | 216 | whd in match sigma_state; normalize nodelta #EQbv |
---|
| 217 | cases(ps_reg_retrieve_ok ?????? EQbv) #bv1 * #EQbv1 #EQ destruct(EQ) |
---|
| 218 | cases(bool_of_beval_ok … EQbool) #b * #EQb #EQ destruct(EQ) #t_fn #EQt_fn |
---|
[2898] | 219 | whd %{(refl …)} #mid #EQt_stmt %{(st_no_pc … st2)} % |
---|
| 220 | [1,3: % |
---|
| 221 | [1,3: % |
---|
| 222 | [1,3: %{(refl …)} |
---|
| 223 | |*: % |
---|
| 224 | ] |
---|
| 225 | |*: % |
---|
| 226 | ] |
---|
| 227 | |*: normalize nodelta |
---|
| 228 | change with (ps_reg_retrieve ??) in match (acca_retrieve ?????); |
---|
| 229 | >EQbv1 >m_return_bind >EQb >m_return_bind normalize nodelta |
---|
| 230 | [ >(pc_of_label_eq … EQt_fn) >m_return_bind] |
---|
| 231 | >(fetch_stmt_ok_sigma_pc_ok … EQfetch) % |
---|
| 232 | ] |
---|
| 233 | whd %{f} %{fn} >EQfn %{(refl …)} >(fetch_stmt_ok_sigma_pc_ok … EQfetch) |
---|
| 234 | cases st2 * #frms #is #b #regs #m #pc2 #lp2 % |
---|
[2891] | 235 | | #st1 #st1' #st2 #f #fn #stmt #nxt #EQfetch whd in match eval_state; |
---|
| 236 | whd in match eval_statement_no_pc; normalize nodelta >EQfetch >m_return_bind |
---|
| 237 | normalize nodelta #H @('bind_inversion H) -H #st1_no_pc' #EQst1_no_pc' |
---|
[2940] | 238 | whd in ⊢ (??%% → ?); #EQ destruct(EQ) |
---|
| 239 | whd in match (succ_pc ???); normalize nodelta |
---|
| 240 | whd in match (set_no_pc ???); normalize nodelta |
---|
| 241 | whd in ⊢ (%→?); #EQ destruct(EQ) |
---|
[2891] | 242 | whd in match sigma_state_pc in EQst1_no_pc'; normalize nodelta in EQst1_no_pc'; |
---|
| 243 | cases(fetch_statement_inv … EQfetch) >(fetch_stmt_ok_sigma_pc_ok … EQfetch) |
---|
| 244 | #EQfn #EQstmt >EQfn in EQst1_no_pc'; normalize nodelta #EQst1_no_pc' |
---|
| 245 | #t_fn #EQt_fn whd % [2: %{(refl …)} |] lapply(err_eq_from_io ????? EQst1_no_pc') |
---|
| 246 | -EQst1_no_pc' #EQst1_no_pc' |
---|
| 247 | cases(eval_seq_no_pc_no_call_ok prog f_lbls f_regs ???????? EQst1_no_pc') |
---|
[2898] | 248 | [ #st2_no_pc' * #EQst2_no_pc' #EQ destruct(EQ) %{st2_no_pc'} % |
---|
| 249 | [ whd in ⊢ (??%?); >EQst2_no_pc' % |
---|
| 250 | | whd %{f} %{fn} >EQfn %{(refl …)} whd in match sigma_state_pc; normalize nodelta |
---|
| 251 | >EQfn % |
---|
| 252 | ] |
---|
[2891] | 253 | | #lbl whd in match code_has_label; whd in match code_has_point; normalize nodelta |
---|
| 254 | inversion(stmt_at ????) [#_ *] #stmt1 #EQstmt1 #_ |
---|
| 255 | cut(fetch_statement ERTL_semantics (prog_var_names … prog) (globalenv_noinit … prog) |
---|
| 256 | (pc_of_point ERTL_semantics (pc_block (pc … st2)) lbl) = |
---|
| 257 | return 〈f,fn,stmt1〉) |
---|
| 258 | [ whd in ⊢ (??%?); >EQfn normalize nodelta >point_of_pc_of_point >EQstmt1 %] #EQf_stmt1 |
---|
| 259 | cases(b_graph_transform_program_fetch_statement_plus … good … EQf_stmt1) |
---|
| 260 | #init * #t_fn' ** #EQt_fn' whd in ⊢ (% → ?); cases(init_regs ?) [2: #x #y *] |
---|
| 261 | normalize nodelta #EQ destruct(EQ) * #labels * #registers |
---|
| 262 | ******* #EQlabels >point_of_pc_of_point change with (pc_block (pc … st2)) in match (pc_block ?); |
---|
| 263 | #EQregisters #_ #_ #_ #_ #fresh_regs #_ >EQregisters |
---|
| 264 | cases(excluded_middle_list ? (λreg.bool_to_Prop(¬(reg∈registers))) |
---|
| 265 | (get_used_registers_from_seq … (functs ERTL) stmt) ?) |
---|
| 266 | [3: #a #_ cases(¬a∈registers) // |1: #H assumption] #H @⊥ |
---|
| 267 | cases(Exists_All … H (regs_are_in_univers … (pi2 ?? fn) … EQstmt)) |
---|
| 268 | #reg ** #H1 #H2 @H1 -H1 @notb_Prop % #H1 lapply(fresh_regs … lbl) >EQregisters |
---|
| 269 | #H3 lapply(All_memb … H3 H1) ** #H4 #_ @H4 assumption |
---|
| 270 | ] |
---|
[2883] | 271 | ] |
---|
| 272 | qed. |
---|
| 273 | |
---|
[2785] | 274 | include alias "basics/lists/listb.ma". |
---|
[2783] | 275 | |
---|
| 276 | lemma eval_seq_no_call_ok : |
---|
| 277 | ∀prog. |
---|
| 278 | let trans_prog ≝ ertl_to_ertlptr prog in |
---|
| 279 | ∀ f_lbls,f_regs,stack_sizes. |
---|
| 280 | ∀f_bl_r. |
---|
| 281 | b_graph_transform_program_props ERTL_semantics ERTLptr_semantics |
---|
[2843] | 282 | (λglobals,fn.«translate_data globals fn,(refl …)») prog f_bl_r f_lbls f_regs → |
---|
[2783] | 283 | ∀st2 : state_pc ERTLptr_semantics. |
---|
| 284 | let st1 ≝ sigma_state_pc prog f_lbls f_regs st2 in |
---|
| 285 | ∀st1' : state_pc ERTL_semantics. |
---|
| 286 | ∀f,fn,stmt,nxt. |
---|
| 287 | fetch_statement ERTL_semantics |
---|
| 288 | (prog_var_names (joint_function ERTL_semantics) ℕ prog) |
---|
| 289 | (ev_genv (mk_prog_params ERTL_semantics prog stack_sizes)) |
---|
| 290 | (pc … st1) = |
---|
| 291 | return 〈f, fn, sequential … (step_seq ERTL … stmt) nxt〉 → |
---|
| 292 | eval_state ERTL_semantics |
---|
| 293 | (prog_var_names (joint_function ERTL_semantics) ℕ prog) |
---|
| 294 | (ev_genv … (mk_prog_params ERTL_semantics prog stack_sizes)) |
---|
| 295 | st1 = |
---|
| 296 | return st1' → |
---|
| 297 | ∃st2'. st1' = sigma_state_pc prog f_lbls f_regs st2' ∧ |
---|
| 298 | ∃taf : trace_any_any_free (ERTLptr_status trans_prog stack_sizes) |
---|
| 299 | st2 |
---|
| 300 | st2'. |
---|
| 301 | if taaf_non_empty … taf then True else |
---|
| 302 | (¬as_costed (ERTL_status prog stack_sizes) st1 ∨ |
---|
| 303 | ¬as_costed (ERTL_status prog stack_sizes) st1'). |
---|
| 304 | #prog #f_lbls #f_regs #stack_size #f_bl_r #good #st2 #st1' #f #fn #stmt #nxt |
---|
| 305 | #EQfetch whd in match eval_state; normalize nodelta >EQfetch >m_return_bind |
---|
| 306 | #H @('bind_inversion H)-H #st_no_pc |
---|
| 307 | whd in match eval_statement_no_pc; normalize nodelta #EQnopc |
---|
| 308 | whd in match eval_statement_advance; normalize nodelta |
---|
| 309 | whd in match set_no_pc; whd in match next; whd in match set_pc; |
---|
| 310 | normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ) lapply EQfetch |
---|
| 311 | >(fetch_stmt_ok_sigma_pc_ok … EQfetch) #EQfetch' |
---|
[2843] | 312 | cases(b_graph_transform_program_fetch_statement_plus … good … EQfetch') |
---|
[2783] | 313 | #init_data * #t_fn1 ** #EQt_fn1 whd in ⊢ (% → ?); cases (f_bl_r ?) normalize nodelta |
---|
[2843] | 314 | [2: #r #tl *] #EQ destruct(EQ) * #labs * #regs ******* #EQlabs #EQregs #_ #_ #_ #_ |
---|
| 315 | #fresh_regs * #bl * >if_merge_right in ⊢ (% → ?); [2: %] |
---|
| 316 | whd in ⊢ (% → ?); cases regs in EQregs; normalize nodelta [2: #x #y #_ *] #EQregs |
---|
| 317 | #EQ destruct(EQ) #eval_spec |
---|
[2783] | 318 | lapply(err_eq_from_io ????? EQnopc) -EQnopc >(fetch_stmt_ok_sigma_state_ok … EQfetch) |
---|
| 319 | #EQnopc |
---|
[2843] | 320 | cases(eval_seq_no_pc_no_call_ok prog f_lbls f_regs ???????? EQnopc) |
---|
| 321 | [ #stnopc'' * #EQstnopc'' #EQsem % |
---|
[2783] | 322 | [ % [@stnopc'' | @(succ_pc ERTL_semantics (pc … st2) nxt) | @(last_pop … st2)]] |
---|
| 323 | % |
---|
| 324 | [ whd in match sigma_state_pc; normalize nodelta @('bind_inversion EQfetch) |
---|
| 325 | * #f1 #fn1 >(fetch_stmt_ok_sigma_pc_ok … EQfetch) #EQfn1 |
---|
| 326 | #H @('bind_inversion H) -H #stmt1 #_ whd in ⊢ (??%% → ?); #EQ destruct(EQ) |
---|
| 327 | >EQfn1 normalize nodelta >EQsem % ] |
---|
| 328 | % [ @(produce_trace_any_any_free_coerced) [ @f | @t_fn1 |6: @eval_spec ||| @EQt_fn1] |
---|
| 329 | whd in match repeat_eval_seq_no_pc; normalize nodelta whd in ⊢ (??%?); |
---|
| 330 | >EQstnopc'' %] @if_elim [#_ @I] #_ %1 % whd in match as_costed; |
---|
| 331 | normalize nodelta * #H @H whd in ⊢ (??%?); >EQfetch % |
---|
| 332 | | #lbl whd in match code_has_label; whd in match code_has_point; normalize nodelta |
---|
[2843] | 333 | inversion(stmt_at ????) [#_ *] #stmt1 #EQstmt1 #_ |
---|
| 334 | cut(fetch_statement ERTL_semantics (prog_var_names … prog) (globalenv_noinit … prog) |
---|
| 335 | (pc_of_point ERTL_semantics (pc_block (pc … st2)) lbl) = |
---|
| 336 | return 〈f,fn,stmt1〉) |
---|
| 337 | [ lapply(fetch_statement_inv … EQfetch') * #EQfn #_ whd in ⊢ (??%?); |
---|
| 338 | >EQfn normalize nodelta >point_of_pc_of_point >EQstmt1 %] #EQf_stmt1 |
---|
| 339 | cases(b_graph_transform_program_fetch_statement_plus … good … EQf_stmt1) |
---|
| 340 | #init * #t_fn' ** #EQt_fn' whd in ⊢ (% → ?); cases(f_bl_r ?) [2: #x #y *] |
---|
| 341 | normalize nodelta #EQ destruct(EQ) * #labels * #registers |
---|
| 342 | ******* #EQlabels >point_of_pc_of_point change with (pc_block (pc … st2)) in match (pc_block ?); |
---|
| 343 | #EQregisters #_ #_ #_ #_ #_ #_ >EQregisters |
---|
[2801] | 344 | cases(excluded_middle_list ? (λreg.bool_to_Prop(¬(reg∈registers))) |
---|
[2843] | 345 | (get_used_registers_from_seq … (functs ERTL) stmt) ?) |
---|
| 346 | [3: #a #_ cases(¬a∈registers) // |1: #H assumption] #H @⊥ |
---|
| 347 | lapply(fetch_statement_inv … EQfetch') * #_ normalize nodelta #EQstmt |
---|
[2783] | 348 | cases(Exists_All … H (regs_are_in_univers … (pi2 ?? fn) … EQstmt)) |
---|
[2843] | 349 | #reg ** #H1 #H2 @H1 -H1 @notb_Prop % #H1 lapply(fresh_regs … lbl) >EQregisters |
---|
[2783] | 350 | whd in ⊢ (% → ?); #H3 lapply(All_memb … H3 H1) ** #H4 #_ @H4 assumption |
---|
| 351 | ] |
---|
| 352 | qed. |
---|
| 353 | |
---|
| 354 | lemma eval_goto_ok : |
---|
| 355 | ∀prog : ertl_program. |
---|
| 356 | let trans_prog ≝ ertl_to_ertlptr prog in |
---|
| 357 | ∀ f_lbls,f_regs,stack_sizes. |
---|
| 358 | ∀f_bl_r. |
---|
| 359 | b_graph_transform_program_props ERTL_semantics ERTLptr_semantics |
---|
[2843] | 360 | (λglobals,fn.«translate_data globals fn,(refl …)») prog f_bl_r f_lbls f_regs → |
---|
[2783] | 361 | ∀st2. |
---|
| 362 | let st1 ≝ (sigma_state_pc prog f_lbls f_regs st2) in |
---|
| 363 | ∀st1',f,fn,nxt. |
---|
| 364 | fetch_statement ERTL_semantics … |
---|
| 365 | (globalenv_noinit ? prog) (pc … st1) = |
---|
| 366 | return 〈f, fn, final … (GOTO ERTL … nxt)〉 → |
---|
| 367 | eval_state ERTL_semantics |
---|
| 368 | (prog_var_names (joint_function ERTL_semantics) ℕ prog) |
---|
| 369 | (ev_genv … (mk_prog_params ERTL_semantics prog stack_sizes)) |
---|
| 370 | st1 = |
---|
| 371 | return st1' → |
---|
| 372 | ∃ st2'. st1' = sigma_state_pc prog f_lbls f_regs st2' ∧ |
---|
| 373 | ∃taf : trace_any_any_free (ERTLptr_status trans_prog stack_sizes) |
---|
| 374 | st2 |
---|
| 375 | st2'. |
---|
| 376 | bool_to_Prop (taaf_non_empty … taf). |
---|
| 377 | #prog #f_lbls #f_regs #stack_size #f_bl_r #good #st2 #st1' #f #fn #nxt #EQfetch |
---|
| 378 | whd in match eval_state; normalize nodelta >EQfetch >m_return_bind |
---|
| 379 | whd in match eval_statement_no_pc; normalize nodelta |
---|
| 380 | >m_return_bind whd in match eval_statement_advance; whd in match set_no_pc; |
---|
| 381 | whd in match goto; normalize nodelta #H lapply(err_eq_from_io ????? H) -H |
---|
| 382 | #H @('bind_inversion H) -H #new_pc lapply(fetch_statement_inv … EQfetch) * |
---|
| 383 | #EQfn #_ >(pc_of_label_eq … EQfn) whd in ⊢ (??%% → ??%% → ?); |
---|
| 384 | #EQ1 #EQ2 destruct(EQ1 EQ2) |
---|
| 385 | % [ % [ @st2 | @(mk_program_counter (pc_block (pc … st2)) |
---|
| 386 | (offset_of_point ERTL_semantics nxt)) | @(last_pop … st2)]] |
---|
| 387 | % [ >(fetch_stmt_ok_sigma_state_ok … EQfetch) >(fetch_stmt_ok_sigma_pc_ok … EQfetch) |
---|
| 388 | >(fetch_stmt_ok_sigma_last_pop_ok … EQfetch) whd in match sigma_state_pc; |
---|
| 389 | normalize nodelta >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in EQfn; #EQfn |
---|
| 390 | >EQfn %] |
---|
| 391 | cases(b_graph_transform_program_fetch_statement … good … EQfetch) |
---|
| 392 | #init_data * #t_fn1 ** #EQt_fn1 whd in ⊢ (% → ?); cases (f_bl_r ?) normalize nodelta |
---|
| 393 | [2: #r #tl *] #EQ destruct(EQ) * #labs ** |
---|
| 394 | [2: #hd #tl ** #_ #_ ** #pre #inst * whd in ⊢ (%→?); *] ** #EQlabs #EQf_regs |
---|
| 395 | whd in match translate_fin_step; normalize nodelta * #bl * |
---|
| 396 | whd in ⊢ (% → ?); #EQ destruct(EQ) ** |
---|
| 397 | [2: #lb #tl * #mid ** #EQmid whd in ⊢ (% → ?); * #ABS destruct(ABS)] * #mid ** |
---|
| 398 | whd in ⊢ (???% → ?); #EQ destruct(EQ) * #_ #_ change with (stmt_at ???? = ? → ?) |
---|
| 399 | #EQstmt >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in EQt_fn1; #EQt_fn1 |
---|
| 400 | >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in EQstmt; #EQstmt |
---|
| 401 | %{(taaf_step … (taa_base …) …)} |
---|
| 402 | [ whd in match as_classifier; normalize nodelta whd in ⊢ (??%?); |
---|
| 403 | whd in match fetch_statement; normalize nodelta |
---|
| 404 | >EQt_fn1 >m_return_bind >EQstmt % |
---|
| 405 | | whd whd in match eval_state; normalize nodelta whd in match fetch_statement; |
---|
| 406 | normalize nodelta >EQt_fn1 >m_return_bind >EQstmt >m_return_bind |
---|
| 407 | whd in match eval_statement_no_pc; normalize nodelta >m_return_bind |
---|
| 408 | whd in match eval_statement_advance; normalize nodelta |
---|
| 409 | whd in match goto; normalize nodelta >(pc_of_label_eq … EQt_fn1) % |
---|
| 410 | ] @I |
---|
| 411 | qed. |
---|
| 412 | |
---|
| 413 | |
---|
[2785] | 414 | |
---|
[2783] | 415 | (* |
---|
| 416 | lemma list_elim_on_last : ∀A : Type[0].∀ P : (list A) → Prop. ∀ l. |
---|
| 417 | P ([ ]) → (∀pre,last. P (pre@[last])) → P l. |
---|
| 418 | #A #P #l #H1 #H2 cut(∀A.∀l : list A.l = [ ] ∨ ∃pre,last. l = pre@[last]) |
---|
| 419 | [ #A #l elim l [ %1 % | #a #tl * [ #EQ destruct %2 %{([ ])} %{a} %] |
---|
| 420 | * #l1 * #a1 #EQ destruct %2 %{(a::l1)} %{a1} %]] #APP1 |
---|
| 421 | lapply(APP1 … l) * [ #EQ >EQ assumption] |
---|
| 422 | * #pre * #last #EQ >EQ @H2 |
---|
| 423 | qed.*) |
---|
| 424 | |
---|
| 425 | |
---|
| 426 | |
---|
| 427 | lemma eval_return_ok : |
---|
| 428 | ∀prog : ertl_program. |
---|
| 429 | let trans_prog ≝ ertl_to_ertlptr prog in |
---|
| 430 | ∀ f_lbls,f_regs,stack_sizes. |
---|
| 431 | ∀f_bl_r. |
---|
| 432 | ∀ good :b_graph_transform_program_props ERTL_semantics ERTLptr_semantics |
---|
| 433 | translate_data prog f_bl_r f_lbls f_regs. |
---|
| 434 | ∀st2, st1',f,fn. |
---|
| 435 | let st1 ≝ sigma_state_pc prog f_lbls f_regs st2 in |
---|
| 436 | fetch_statement ERTL_semantics … |
---|
| 437 | (globalenv_noinit ? prog) (pc … st1) = |
---|
| 438 | return 〈f, fn, final … (RETURN ERTL … )〉 → |
---|
| 439 | eval_state ERTL_semantics |
---|
| 440 | (prog_var_names (joint_function ERTL_semantics) ℕ prog) |
---|
| 441 | (ev_genv … (mk_prog_params ERTL_semantics prog stack_sizes)) |
---|
| 442 | st1 = |
---|
| 443 | return st1' → |
---|
| 444 | joint_classify (mk_prog_params ERTLptr_semantics trans_prog stack_sizes) |
---|
| 445 | st2 = cl_return ∧ |
---|
| 446 | ∃st2'. st1' = sigma_state_pc prog f_lbls f_regs st2' ∧ |
---|
| 447 | ∃st2_after_ret. |
---|
| 448 | ∃taf : trace_any_any_free (ERTLptr_status trans_prog stack_sizes) (* always empty in this case *) |
---|
| 449 | st2_after_ret |
---|
| 450 | st2'. |
---|
| 451 | (if taaf_non_empty … taf then |
---|
| 452 | ¬as_costed (ERTLptr_status trans_prog stack_sizes) |
---|
| 453 | st2_after_ret |
---|
| 454 | else True) ∧ |
---|
| 455 | eval_state … (ev_genv … (mk_prog_params ERTLptr_semantics trans_prog stack_sizes)) st2 = |
---|
| 456 | return st2_after_ret ∧ |
---|
| 457 | ret_rel ?? (ERTLptrStatusSimulation prog stack_sizes ??? good) st1' st2_after_ret. |
---|
| 458 | #prog #f_lbls #f_regs #stack_size #f_bl_r #good #st2 #st1' #f #fn #EQfetch |
---|
| 459 | whd in match eval_state; normalize nodelta >EQfetch >m_return_bind |
---|
| 460 | #H @('bind_inversion H) -H #st1_tmp whd in ⊢ (??%%→?); #EQ destruct |
---|
| 461 | whd in match set_no_pc in ⊢ (%→?); whd in match eval_statement_advance in ⊢ (%→?); |
---|
| 462 | whd in match eval_return; normalize nodelta #H lapply(err_eq_from_io ????? H) -H |
---|
| 463 | #H @('bind_inversion H) -H * #n_st #n_pc change with (ertl_pop_frame ? = ? → ?) |
---|
| 464 | >(fetch_stmt_ok_sigma_state_ok … EQfetch) #EQpop_frame |
---|
| 465 | cases(pop_frame_ok ?????? EQpop_frame) * #t_n_st #t_n_pc * #EQt_pop_frame |
---|
| 466 | normalize nodelta |
---|
| 467 | inversion (fetch_internal_function ??) normalize nodelta |
---|
| 468 | [ * #id1 #fn1 | #err ] normalize nodelta #EQfetch_fn1 #EQ destruct(EQ) |
---|
| 469 | #H @('bind_inversion H) -H #next_of_n_pc |
---|
| 470 | [2: >next_of_call_pc_error [2: % %] whd in ⊢ (???% → ?); #EQ destruct(EQ)] |
---|
| 471 | #EQnext_of_n_pc cases(next_of_call_pc_ok … good … EQnext_of_n_pc) |
---|
| 472 | #pc1 * #EQpc1 cut(pc1 = t_n_pc) |
---|
| 473 | [ @(sigma_stored_pc_inj prog f_lbls) |
---|
| 474 | lapply EQnext_of_n_pc; <EQpc1 whd in match sigma_stored_pc; normalize nodelta |
---|
| 475 | inversion(sigma_pc_opt ???) [1,3: #_ >next_of_call_pc_error [2,4: % %] |
---|
| 476 | whd in ⊢ (???% → ?); #EQ destruct| #x #_ #_ % #EQ destruct] #x #EQx #_ |
---|
| 477 | lapply EQnext_of_n_pc whd in match sigma_stored_pc; normalize nodelta |
---|
| 478 | inversion (sigma_pc_opt ???) [ #_ >next_of_call_pc_error [2: % %] |
---|
| 479 | whd in ⊢ (???% → ?); #EQ destruct] #y #EQy #_ lapply EQpc1 |
---|
| 480 | whd in match sigma_stored_pc; normalize nodelta >EQx >EQy normalize nodelta |
---|
| 481 | #EQ destruct % |
---|
| 482 | ] #EQ destruct(EQ) #EQnxt whd in match next; whd in match set_last_pop; |
---|
| 483 | whd in match set_pc; normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ) |
---|
| 484 | cases(b_graph_transform_program_fetch_statement … good … EQfetch) |
---|
| 485 | #init_data * #t_fn1 ** #EQt_fn1 whd in ⊢ (% → ?); cases (f_bl_r ?) normalize nodelta |
---|
| 486 | [2: #r #tl *] #EQ destruct(EQ) * #labs ** |
---|
| 487 | [2: #hd #tl ** #_ #_ * #ibl * whd in ⊢ (%→?); *] ** #EQlabs #EQf_regs |
---|
| 488 | whd in match translate_fin_step; normalize nodelta * #bl * |
---|
| 489 | whd in ⊢ (% → ?); #EQ destruct(EQ) ** |
---|
| 490 | [2: #lb #tl * #mid ** #EQmid whd in ⊢ (% → ?); * #ABS destruct(ABS)] * #mid ** |
---|
| 491 | whd in ⊢ (???% → ?); #EQ destruct(EQ) * #_ #_ change with (stmt_at ???? = ? → ?) |
---|
| 492 | #EQstmt % |
---|
| 493 | [ whd in match joint_classify; normalize nodelta whd in match fetch_statement; |
---|
| 494 | normalize nodelta <(fetch_stmt_ok_sigma_pc_ok … EQfetch) >EQt_fn1 >m_return_bind |
---|
| 495 | >EQstmt % |
---|
| 496 | | % |
---|
| 497 | [ % |
---|
| 498 | [ @t_n_st |
---|
| 499 | | @(succ_pc ERTL_semantics (sigma_stored_pc prog f_lbls t_n_pc) next_of_n_pc) |
---|
| 500 | | @t_n_pc] |
---|
| 501 | ] |
---|
| 502 | % |
---|
| 503 | [ whd in match sigma_state_pc; normalize nodelta |
---|
| 504 | lapply(next_of_call_pc_inv … EQnext_of_n_pc) * #id2 * #fn2 * #c_id * #c_arg |
---|
| 505 | * #c_dest #EQfetch1 whd in match (succ_pc ???); |
---|
| 506 | >(fetch_stmt_ok_sigma_pc_block_ok … EQfetch1) >EQfetch_fn1 |
---|
| 507 | normalize nodelta % |
---|
| 508 | ] |
---|
| 509 | % |
---|
| 510 | [ % |
---|
| 511 | [ @t_n_st |
---|
| 512 | | @(succ_pc ERTL_semantics (sigma_stored_pc prog f_lbls t_n_pc) next_of_n_pc) |
---|
| 513 | | @t_n_pc] |
---|
| 514 | ] |
---|
| 515 | %{(taaf_base … )} normalize nodelta % [% [@I]] |
---|
| 516 | [ whd in match fetch_statement; normalize nodelta <(fetch_stmt_ok_sigma_pc_ok … EQfetch) |
---|
| 517 | >EQt_fn1 >m_return_bind >EQstmt >m_return_bind whd in match eval_statement_no_pc; |
---|
| 518 | normalize nodelta >m_return_bind whd in match eval_statement_advance; |
---|
| 519 | whd in match eval_return; normalize nodelta |
---|
| 520 | change with (ertl_pop_frame ?) in match (pop_frame ????????); |
---|
| 521 | >EQt_pop_frame >m_return_bind >EQnxt >m_return_bind whd in match next; |
---|
| 522 | whd in match set_pc; whd in match set_last_pop; whd in match succ_pc; |
---|
| 523 | normalize nodelta lapply(next_of_call_pc_inv … EQnext_of_n_pc) |
---|
| 524 | * #id2 * #fn2 * #c_id * #c_arg * #c_dest #EQfetch1 whd in match (succ_pc ???); |
---|
| 525 | >(fetch_stmt_ok_sigma_pc_block_ok … EQfetch1) % |
---|
| 526 | | whd * #s1_pre #s1_call |
---|
| 527 | cases (joint_classify_call … s1_call) |
---|
| 528 | * #calling_i #calling * #call_spec * #arg * #dest * #nxt' #EQfetch_call |
---|
| 529 | * #s2_pre #s2_call whd in ⊢ (% → ?); >EQfetch_call normalize nodelta |
---|
| 530 | * #s1_pre_prf #EQpc_s2_pre whd in ⊢ (% → ?); #EQ1 |
---|
| 531 | >EQ1 in EQfetch_call; #EQfetch_call |
---|
| 532 | cases(fetch_call_commute … good … EQfetch_call) #calling' * #pc1 * |
---|
| 533 | #EQ1 cut(pc … s2_pre = pc1) |
---|
| 534 | [ @(sigma_stored_pc_inj prog f_lbls) lapply(EQfetch_call) |
---|
| 535 | whd in match sigma_stored_pc; normalize nodelta inversion(sigma_pc_opt ???) |
---|
| 536 | [1,3: #_ >fetch_statement_no_zero [2,4: %] #EQ destruct(EQ)| #x #_ #_ % #EQ destruct] |
---|
| 537 | #pc2 #EQpc2 #_ lapply EQ1 whd in match sigma_stored_pc; |
---|
| 538 | normalize nodelta >EQpc2 normalize nodelta cases(sigma_pc_opt ???) |
---|
| 539 | [2: #x normalize nodelta #EQ >EQ %] normalize nodelta #EQ <EQ in EQpc2; |
---|
| 540 | #EQ1 lapply EQfetch_call >fetch_statement_no_zero [ #ABS destruct(ABS)] |
---|
| 541 | whd in match sigma_stored_pc; normalize nodelta >EQ1 % |
---|
| 542 | ] #EQ2 destruct(EQ2) #EQt_fetch_call whd >EQt_fetch_call normalize nodelta % |
---|
| 543 | [ >EQ1 in s1_pre_prf; #EQ @(sigma_stored_pc_inj prog f_lbls) |
---|
| 544 | lapply EQnext_of_n_pc whd in match sigma_stored_pc; normalize nodelta |
---|
| 545 | inversion(sigma_pc_opt ???) [1,3: #_ >next_of_call_pc_error [2,4: % %] |
---|
| 546 | whd in ⊢ (???% → ?); #EQ destruct] #pc1 #EQpc1 #_ [ % #EQ destruct] |
---|
| 547 | lapply EQ whd in match sigma_stored_pc; normalize nodelta |
---|
| 548 | >EQpc1 normalize nodelta inversion(sigma_pc_opt ???) |
---|
| 549 | [2: #pc2 #_ normalize nodelta #EQ >EQ %] normalize nodelta |
---|
| 550 | #ABS #ABS1 lapply EQnext_of_n_pc whd in match sigma_stored_pc; |
---|
| 551 | normalize nodelta >EQpc1 >ABS1 normalize nodelta |
---|
| 552 | >next_of_call_pc_error [2: % %] whd in ⊢ (???% → ?); #EQ destruct |
---|
| 553 | | whd in match succ_pc; normalize nodelta |
---|
| 554 | change with next_of_n_pc in match (point_of_succ ???); |
---|
| 555 | change with nxt' in match (point_of_succ ???); |
---|
| 556 | lapply EQpc_s2_pre whd in match succ_pc; normalize nodelta |
---|
| 557 | change with next_of_n_pc in match (point_of_succ ???); |
---|
| 558 | change with nxt' in match (point_of_succ ???); #EQ >EQ |
---|
| 559 | cut(pc_block (pc … s1_pre) = pc_block (pc … s2_pre)) |
---|
| 560 | [2: #EQ >EQ %] >EQ1 <(pc_block_eq prog f_lbls …) [%] |
---|
| 561 | lapply EQfetch_call whd in match sigma_stored_pc; normalize nodelta |
---|
| 562 | cases(sigma_pc_opt ???) [ >fetch_statement_no_zero [2: %] #EQ destruct] |
---|
| 563 | #x #_ % #EQ destruct |
---|
| 564 | ] |
---|
| 565 | ] |
---|
| 566 | ] |
---|
| 567 | qed. |
---|
| 568 | |
---|
| 569 | |
---|
[2785] | 570 | |
---|
[2783] | 571 | lemma eval_cond_ok : |
---|
| 572 | ∀prog. |
---|
| 573 | let trans_prog ≝ ertl_to_ertlptr prog in |
---|
| 574 | ∀ f_lbls,f_regs,stack_sizes. |
---|
| 575 | ∀f_bl_r. |
---|
| 576 | ∀ good :b_graph_transform_program_props ERTL_semantics ERTLptr_semantics |
---|
[2843] | 577 | (λglobals,fn.«translate_data globals fn,(refl …)») prog f_bl_r f_lbls f_regs. |
---|
[2783] | 578 | ∀st2,st1',f,fn,a,ltrue,lfalse. |
---|
| 579 | let st1 ≝ sigma_state_pc prog f_lbls f_regs st2 in |
---|
| 580 | fetch_statement ERTL_semantics … |
---|
| 581 | (globalenv_noinit ? prog) (pc … st1) = |
---|
| 582 | return 〈f, fn, sequential … (COND ERTL … a ltrue) lfalse〉 → |
---|
| 583 | eval_state ERTL_semantics |
---|
| 584 | (prog_var_names (joint_function ERTL_semantics) ℕ prog) |
---|
| 585 | (ev_genv … (mk_prog_params ERTL_semantics prog stack_sizes)) |
---|
| 586 | st1 = return st1' → |
---|
| 587 | as_costed (ERTL_status prog stack_sizes) st1' → |
---|
| 588 | ∃ st2'. st1' = sigma_state_pc prog f_lbls f_regs st2' ∧ |
---|
| 589 | ∃taf : trace_any_any_free (ERTLptr_status trans_prog stack_sizes) |
---|
| 590 | st2 st2'. |
---|
| 591 | bool_to_Prop (taaf_non_empty … taf). |
---|
| 592 | #prog #f_lbls #f_regs #stack_size #f_bl_r #good #st2 #st1' #f #fn #a #ltrue #lfalse |
---|
| 593 | #EQfetch whd in match eval_state; normalize nodelta >EQfetch >m_return_bind |
---|
| 594 | whd in match eval_statement_no_pc; normalize nodelta >m_return_bind |
---|
| 595 | whd in match eval_statement_advance; normalize nodelta |
---|
| 596 | change with (ps_reg_retrieve ??) in match (acca_retrieve ?????); |
---|
| 597 | #H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H |
---|
| 598 | #bv >(fetch_stmt_ok_sigma_state_ok … EQfetch) in ⊢ (% → ?); whd in match set_no_pc; |
---|
| 599 | normalize nodelta #EQbv #H @('bind_inversion H) -H * #EQbool normalize nodelta |
---|
| 600 | lapply(fetch_statement_inv … EQfetch) * #EQfn #_ |
---|
| 601 | [ whd in match goto; normalize nodelta >(pc_of_label_eq ??????? EQfn) >m_return_bind |
---|
| 602 | | whd in match next; normalize nodelta |
---|
| 603 | ] whd in match set_pc; normalize nodelta |
---|
| 604 | >(fetch_stmt_ok_sigma_state_ok … EQfetch) whd in match set_no_pc; normalize nodelta |
---|
| 605 | >(fetch_stmt_ok_sigma_pc_ok … EQfetch) >(fetch_stmt_ok_sigma_last_pop_ok … EQfetch) |
---|
| 606 | whd in ⊢ (??%% → ?); #EQ destruct #n_cost |
---|
| 607 | %{(mk_state_pc ? (st_no_pc … st2) |
---|
| 608 | (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) ?) |
---|
| 609 | (last_pop … st2))} [ @ltrue |3: @lfalse] |
---|
| 610 | % [1,3: whd in match sigma_state_pc; normalize nodelta |
---|
| 611 | >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in EQfn; #EQfn >EQfn %] |
---|
| 612 | cases(b_graph_transform_program_fetch_statement … good … EQfetch) |
---|
| 613 | #init_data * #t_fn1 ** #EQt_fn1 whd in ⊢ (% → ?); cases (f_bl_r ?) normalize nodelta |
---|
| 614 | [2,4: #r #tl *] #EQ destruct(EQ) >if_merge_right in ⊢ (% → ?); [2,4: %] * #labs ** |
---|
| 615 | [2,4: #hd #tl ** #_ #_ *** #pre #inst #post * whd in ⊢ (%→?); *] ** #EQlabs #EQf_regs |
---|
| 616 | whd in match translate_step; normalize nodelta * #bl * |
---|
| 617 | whd in ⊢ (% → ?); #EQ destruct(EQ) whd in ⊢ (% → ?); * #l1 * #mid1 * #mid2 * #l2 |
---|
| 618 | *** #EQmid1 whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in ⊢ (% → ?); * |
---|
| 619 | #nxt1 * #EQcond #EQ destruct(EQ) whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2) |
---|
| 620 | whd in EQmid1 : (??%%); destruct(EQmid1) |
---|
| 621 | %{(taaf_step_jump … (taa_base …) …) I} |
---|
| 622 | [2,5: whd whd in ⊢ (??%?); whd in match fetch_statement; normalize nodelta |
---|
| 623 | <(fetch_stmt_ok_sigma_pc_ok … EQfetch) >EQt_fn1 >m_return_bind |
---|
| 624 | >EQcond % |
---|
| 625 | |3,6: whd whd in match eval_state; normalize nodelta whd in match eval_statement_no_pc; |
---|
| 626 | normalize nodelta whd in match fetch_statement; normalize nodelta |
---|
| 627 | <(fetch_stmt_ok_sigma_pc_ok … EQfetch) >EQt_fn1 >m_return_bind |
---|
| 628 | >EQcond >m_return_bind normalize nodelta >m_return_bind |
---|
| 629 | whd in match eval_statement_advance; normalize nodelta |
---|
| 630 | change with (ps_reg_retrieve ??) in match (acca_retrieve ?????); |
---|
| 631 | cases(ps_reg_retrieve_ok … EQbv) #bv1 * #EQbv1 #EQsem >EQbv1 |
---|
| 632 | >m_return_bind >EQsem in EQbool; #EQbool cases(bool_of_beval_ok … EQbool) |
---|
| 633 | #bool1 * #EQbool1 #EQ destruct(EQ) >EQbool1 >m_return_bind normalize nodelta |
---|
| 634 | >(fetch_stmt_ok_sigma_pc_ok … EQfetch) [2: %] whd in match goto; |
---|
| 635 | normalize nodelta >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in EQt_fn1; #EQt_fn1 |
---|
| 636 | >(pc_of_label_eq … EQt_fn1) >m_return_bind % |
---|
| 637 | |*: lapply n_cost whd in match as_costed; normalize nodelta |
---|
| 638 | [ cut((mk_state_pc ERTL_semantics |
---|
| 639 | (sigma_state prog f_lbls f_regs |
---|
| 640 | (added_registers ERTL (prog_var_names (joint_function ERTL) ℕ prog) fn |
---|
| 641 | (f_regs (pc_block (pc ERTLptr_semantics st2)))) st2) |
---|
| 642 | (pc_of_point ERTL_semantics (pc_block (pc ERTLptr_semantics st2)) ltrue) |
---|
| 643 | (sigma_stored_pc prog f_lbls (last_pop ERTLptr_semantics st2))) = |
---|
| 644 | sigma_state_pc prog f_lbls f_regs (mk_state_pc ERTLptr_semantics st2 |
---|
| 645 | (pc_of_point ERTLptr_semantics (pc_block (pc ERTLptr_semantics st2)) ltrue) |
---|
| 646 | (last_pop ERTLptr_semantics st2))) [ whd in match sigma_state_pc; normalize nodelta |
---|
| 647 | >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in EQfn; #EQfn >EQfn %] |
---|
| 648 | #EQ >EQ >(as_label_ok … good … (mk_state_pc ERTLptr_semantics st2 |
---|
| 649 | (pc_of_point ERTLptr_semantics (pc_block (pc ERTLptr_semantics st2)) ltrue) |
---|
| 650 | (last_pop ERTLptr_semantics st2))) [#H @H] cases daemon (*needs lemma see below *) |
---|
| 651 | | cut((mk_state_pc ERTL_semantics |
---|
| 652 | (sigma_state prog f_lbls f_regs |
---|
| 653 | (added_registers ERTL (prog_var_names (joint_function ERTL) ℕ prog) fn |
---|
| 654 | (f_regs (pc_block (pc ERTLptr_semantics st2)))) st2) |
---|
| 655 | (succ_pc ERTL_semantics (pc ERTLptr_semantics st2) |
---|
| 656 | (point_of_succ ERTLptr_semantics |
---|
| 657 | (point_of_pc ERTLptr_semantics |
---|
| 658 | (pc ERTL_semantics (sigma_state_pc prog f_lbls f_regs st2))) nxt1)) |
---|
| 659 | (sigma_stored_pc prog f_lbls (last_pop ERTLptr_semantics st2))) = |
---|
| 660 | sigma_state_pc prog f_lbls f_regs (mk_state_pc ERTLptr_semantics st2 |
---|
| 661 | (pc_of_point ERTLptr_semantics (pc_block (pc ERTLptr_semantics st2)) |
---|
| 662 | (point_of_succ ERTLptr_semantics |
---|
| 663 | (point_of_pc ERTLptr_semantics |
---|
| 664 | (pc ERTL_semantics (sigma_state_pc prog f_lbls f_regs st2))) nxt1)) |
---|
| 665 | (last_pop ERTLptr_semantics st2))) [ whd in match sigma_state_pc; normalize nodelta |
---|
| 666 | >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in EQfn; #EQfn >EQfn %] #EQ >EQ |
---|
| 667 | >(as_label_ok … good … (mk_state_pc ERTLptr_semantics st2 |
---|
| 668 | (pc_of_point ERTLptr_semantics (pc_block (pc ERTLptr_semantics st2)) |
---|
| 669 | (point_of_succ ERTLptr_semantics |
---|
| 670 | (point_of_pc ERTLptr_semantics |
---|
| 671 | (pc ERTL_semantics (sigma_state_pc prog f_lbls f_regs st2))) nxt1)) |
---|
| 672 | (last_pop ERTLptr_semantics st2))) [#H @H] cases daemon (*needs lemma see below ! *) |
---|
| 673 | ] |
---|
| 674 | qed. |
---|
| 675 | |
---|
| 676 | lemma eval_cost_ok : |
---|
| 677 | ∀prog. |
---|
| 678 | let trans_prog ≝ ertl_to_ertlptr prog in |
---|
| 679 | ∀ f_lbls,f_regs,stack_sizes. |
---|
| 680 | ∀f_bl_r. |
---|
| 681 | ∀ good :b_graph_transform_program_props ERTL_semantics ERTLptr_semantics |
---|
[2843] | 682 | (λglobals,fn.«translate_data globals fn,(refl …)») prog f_bl_r f_lbls f_regs. |
---|
[2783] | 683 | ∀st2,st1',f,fn,c,nxt. |
---|
| 684 | let st1 ≝ sigma_state_pc prog f_lbls f_regs st2 in |
---|
| 685 | fetch_statement ERTL_semantics … |
---|
| 686 | (globalenv_noinit ? prog) (pc … st1) = |
---|
| 687 | return 〈f, fn, sequential … (COST_LABEL ERTL … c) nxt〉 → |
---|
| 688 | eval_state ERTL_semantics |
---|
| 689 | (prog_var_names (joint_function ERTL_semantics) ℕ prog) |
---|
| 690 | (ev_genv … (mk_prog_params ERTL_semantics prog stack_sizes)) |
---|
| 691 | st1 = return st1' → |
---|
| 692 | ∃ st2'. st1' = sigma_state_pc prog f_lbls f_regs st2' ∧ |
---|
| 693 | ∃taf : trace_any_any_free (ERTLptr_status trans_prog stack_sizes) |
---|
| 694 | st2 st2'. |
---|
| 695 | bool_to_Prop (taaf_non_empty … taf). |
---|
| 696 | #prog #f_lbls #f_regs #stack_Size #f_bl_r #good #st2 #st1' #f #fn #c #nxt |
---|
| 697 | #EQfetch whd in match eval_state; normalize nodelta >EQfetch >m_return_bind |
---|
| 698 | whd in match eval_statement_no_pc; normalize nodelta >m_return_bind |
---|
| 699 | whd in match eval_statement_advance; normalize nodelta |
---|
| 700 | >(fetch_stmt_ok_sigma_state_ok … EQfetch) whd in match set_no_pc; |
---|
| 701 | normalize nodelta >(fetch_stmt_ok_sigma_pc_ok … EQfetch) |
---|
| 702 | >(fetch_stmt_ok_sigma_last_pop_ok … EQfetch) whd in match next; |
---|
| 703 | whd in match set_pc; normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ) |
---|
| 704 | %{(set_pc ? (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) nxt) st2)} |
---|
| 705 | % [ whd in match sigma_state_pc; normalize nodelta |
---|
| 706 | lapply(fetch_statement_inv … EQfetch) >(fetch_stmt_ok_sigma_pc_ok … EQfetch) * |
---|
| 707 | #EQfn #_ >EQfn %] lapply EQfetch >(fetch_stmt_ok_sigma_pc_ok … EQfetch) |
---|
| 708 | #EQfetch' |
---|
| 709 | cases(b_graph_transform_program_fetch_statement … good … EQfetch') |
---|
| 710 | #init_data * #t_fn ** #EQt_fn whd in ⊢ (% → ?); cases(f_bl_r ?) [2: #x #y *] |
---|
| 711 | normalize nodelta #EQ destruct(EQ) * #lbls * #regs ** #_ #_ whd in ⊢ (% → ?); |
---|
| 712 | * #bl * >if_merge_right [2: %] whd in ⊢ (% → ?); cases regs [2: #x #y *] |
---|
| 713 | normalize nodelta #EQ destruct(EQ) whd in ⊢ (% → ?); * #l1 * #mid1 * #mid2 * #l2 |
---|
| 714 | *** #EQmid whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in EQmid : (???%); |
---|
| 715 | destruct(EQmid) whd in ⊢ (% → ?); * #nxt1 * #EQstmt #EQ destruct(EQ) |
---|
| 716 | whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2) %{(taaf_step … (taa_base …) …)} |
---|
| 717 | [1,2: whd [ whd in ⊢ (??%?); | whd in match eval_state; ] |
---|
| 718 | whd in match fetch_statement; normalize nodelta >EQt_fn >m_return_bind |
---|
| 719 | >EQstmt [%] >m_return_bind whd in match eval_statement_no_pc; |
---|
| 720 | normalize nodelta >m_return_bind %] @I |
---|
| 721 | qed. |
---|
| 722 | |
---|
| 723 | |
---|
| 724 | lemma eval_call_ok : |
---|
| 725 | ∀prog : ertl_program. |
---|
| 726 | let trans_prog ≝ ertl_to_ertlptr prog in |
---|
| 727 | ∀ f_lbls,f_regs,stack_sizes. |
---|
| 728 | ∀f_bl_r. |
---|
| 729 | ∀ good :b_graph_transform_program_props ERTL_semantics ERTLptr_semantics |
---|
[2843] | 730 | (λglobals,fn.«translate_data globals fn,(refl …)») prog f_bl_r f_lbls f_regs. |
---|
[2783] | 731 | ∀st2,st1',f,fn,called,args,dest,nxt. |
---|
| 732 | let st1 ≝ sigma_state_pc prog f_lbls f_regs st2 in |
---|
| 733 | fetch_statement ERTL_semantics … |
---|
| 734 | (globalenv_noinit ? prog) (pc … st1) = |
---|
| 735 | return 〈f, fn, |
---|
| 736 | sequential … (CALL ERTL … called args dest ) nxt〉 → |
---|
| 737 | eval_state … (ev_genv … (mk_prog_params ERTL_semantics prog stack_sizes)) st1 = |
---|
| 738 | return st1' → |
---|
| 739 | ∃is_call,st2_pre_call,is_call'. |
---|
| 740 | as_call_ident (ERTLptr_status trans_prog stack_sizes) |
---|
| 741 | («st2_pre_call,is_call'») = as_call_ident (ERTL_status prog stack_sizes) |
---|
| 742 | («st1, is_call») ∧ |
---|
| 743 | (pc … st1) = sigma_stored_pc prog f_lbls (pc … st2_pre_call) ∧ |
---|
| 744 | ∃taa2 : trace_any_any (ERTLptr_status trans_prog stack_sizes) st2 st2_pre_call. |
---|
| 745 | ∃ st2'. st1' = sigma_state_pc prog f_lbls f_regs st2' ∧ |
---|
| 746 | eval_state ERTLptr_semantics … |
---|
| 747 | (ev_genv … (mk_prog_params ERTLptr_semantics trans_prog stack_sizes)) st2_pre_call |
---|
| 748 | =return st2'. |
---|
[2843] | 749 | #prog #f_lbls #f_regs #stack_size #f_bl_r #good #st2 #st1' #f #fn * [#c_id | * #c_ptr1 #c_ptr2 ] |
---|
[2801] | 750 | #args #dest #nxt #EQfetch whd in match eval_state; normalize nodelta >EQfetch |
---|
| 751 | >m_return_bind whd in match eval_statement_no_pc; normalize nodelta >m_return_bind |
---|
| 752 | whd in match eval_statement_advance; whd in match eval_call; normalize nodelta |
---|
| 753 | >(fetch_stmt_ok_sigma_state_ok … EQfetch) >(fetch_stmt_ok_sigma_pc_ok … EQfetch) |
---|
| 754 | >(fetch_stmt_ok_sigma_last_pop_ok … EQfetch) #H @('bind_inversion H) -H |
---|
| 755 | #c_bl whd in match set_no_pc; normalize nodelta #H lapply(err_eq_from_io ????? H) -H |
---|
| 756 | #EQc_bl cases(block_of_call_ok ??????? EQc_bl) #c_bl' * #EQc_bl' #EQ destruct(EQ) |
---|
| 757 | #H @('bind_inversion H) -H * #f1 * [1,3: #fn1 |*: #ext_f] #H |
---|
| 758 | lapply(err_eq_from_io ????? H) -H #EQfn1 normalize nodelta |
---|
| 759 | [3,4: #H @('bind_inversion H) -H #st whd in match eval_external_call; normalize nodelta |
---|
| 760 | #H @('bind_inversion H) -H #list_val #_ #H @('bind_inversion H) -H #x |
---|
| 761 | #_ #H @('bind_inversion H) -H #y whd in match do_io; normalize nodelta |
---|
| 762 | whd in ⊢ (???% → ?); #ABS destruct(ABS) ] #H lapply(err_eq_from_io ????? H) -H |
---|
| 763 | #H @('bind_inversion H) -H #st1'' >(fetch_stmt_ok_sigma_pc_ok … EQfetch) |
---|
| 764 | >(fetch_stmt_ok_sigma_last_pop_ok … EQfetch) whd in match kind_of_call; |
---|
| 765 | normalize nodelta change with (ertl_save_frame ? it ?) in ⊢ (??%? → ?); |
---|
| 766 | [2: @ID |4: @PTR] #EQst1'' #H @('bind_inversion H) -H #st1''' |
---|
| 767 | whd in match eval_internal_call; normalize nodelta #H @('bind_inversion H) -H |
---|
| 768 | #s_size #H lapply(opt_eq_from_res ???? H) -H |
---|
| 769 | change with (stack_size ?) in ⊢ (??%? → ?); #EQs_size whd in ⊢ (??%? → ?); |
---|
| 770 | whd in ⊢ (???% → ??%% → ?); #EQ #EQ1 destruct(EQ EQ1) |
---|
| 771 | lapply EQfetch >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in ⊢ (% → ?); |
---|
[2783] | 772 | #EQfetch' lapply(fetch_statement_inv … EQfetch') * #EQfn normalize nodelta #EQstmt |
---|
[2843] | 773 | cases(b_graph_transform_program_fetch_statement_plus … good … EQfetch') |
---|
[2783] | 774 | #init_data * #calling' ** #EQcalling' whd in ⊢ (% → ?); cases(f_bl_r ?) |
---|
[2843] | 775 | [2,4: #x #y *] normalize nodelta #EQ destruct(EQ) * #labels * #registers |
---|
| 776 | ******* #EQlabels #EQregisters #_ #_ #_ #_ #fresh_regs |
---|
| 777 | normalize nodelta >if_merge_right [2,4: %] whd in match translate_step; |
---|
| 778 | normalize nodelta * #bl * cases registers in EQregisters; -registers |
---|
| 779 | normalize nodelta [2,3: [ #x #y] #_ *|4: #r #tl] #EQregisters |
---|
[2783] | 780 | [ whd in ⊢ (% → ?); cases tl in EQregisters; -tl [2: #x #y #_ *] normalize nodelta |
---|
[2801] | 781 | #EQregisters | whd in ⊢ (% → ?);] #EQ destruct(EQ) |
---|
| 782 | * #pre_l * #mid1 * #mid2 * #post_l *** #EQmid1 #m_fetch_pre whd in ⊢ (% → ?); |
---|
| 783 | * #nxt1 * #EQcall change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) |
---|
| 784 | whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2) cases(pre_l) in m_fetch_pre EQmid1; |
---|
| 785 | [* #x * #y ** #ABS destruct(ABS) |
---|
| 786 | |4: #lab #tl * #ABS destruct(ABS) |
---|
| 787 | | #l1 #tl #m_fetch_pre whd in ⊢ (???% → ?); #EQ destruct(EQ) |
---|
| 788 | | * #_ #EQ destruct(EQ) whd in ⊢ (???% → ?); #EQ destruct(EQ) |
---|
| 789 | ] |
---|
| 790 | % |
---|
| 791 | [1,3: @hide_prf whd in ⊢ (??%?); >EQfetch %] |
---|
| 792 | cases(ertl_save_frame_ok prog f_lbls f_regs ? |
---|
[2843] | 793 | (added_registers ERTL (prog_var_names … prog) fn1 (f_regs c_bl')) ? st1''' ?) |
---|
[2801] | 794 | [2: @PTR |
---|
| 795 | |3,7: [ %{(mk_state_pc ? (st_no_pc … st2) |
---|
| 796 | (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) mid1) |
---|
| 797 | (last_pop … st2))} |
---|
| 798 | |%{(st2)} |
---|
| 799 | ] @hide_prf whd in match sigma_pc_opt; normalize nodelta @if_elim |
---|
| 800 | [1,3: @eqZb_elim [2,4: #_ *] #EQbl >fetch_internal_function_no_minus_one in EQfn; |
---|
| 801 | [1,3: #EQ destruct(EQ) |*: assumption]] |
---|
| 802 | #_ [>point_of_pc_of_point >(get_sigma_last … good … EQfn EQstmt EQlabels) |
---|
| 803 | | >(get_sigma_idempotent … good … EQfn EQstmt EQlabels) |
---|
| 804 | ] >m_return_bind % whd in ⊢ (??%? → ?); #ABS destruct(ABS) |
---|
| 805 | |6: @ID |
---|
| 806 | |4,8: [change with (pc_block (pc … st2)) in match (pc_block ?); |
---|
| 807 | >EQfn in ⊢ (??(???match % with [_ ⇒ ?| _ ⇒ ?])?); |
---|
| 808 | |>EQfn in ⊢ (??(???match % with [_ ⇒ ?| _ ⇒ ?])?); |
---|
| 809 | ] normalize nodelta whd in match (st_no_pc ??); |
---|
| 810 | whd in match sigma_stored_pc in ⊢ (??(???(???%?))?); |
---|
| 811 | whd in match sigma_pc_opt; normalize nodelta @if_elim |
---|
| 812 | [1,3: @eqZb_elim [2,4: #_ *] #EQbl >fetch_internal_function_no_minus_one in EQfn; |
---|
| 813 | [1,3: #EQ destruct(EQ) |*: assumption]] |
---|
| 814 | #_ [>point_of_pc_of_point >(get_sigma_last … good … EQfn EQstmt EQlabels) |
---|
| 815 | | >(get_sigma_idempotent … good … EQfn EQstmt EQlabels) |
---|
| 816 | ] >m_return_bind normalize nodelta |
---|
| 817 | change with (pc_block (pc … st2)) in match (pc_block ?); |
---|
| 818 | >pc_of_point_of_pc assumption |
---|
| 819 | ] #st_no_pc_after_call normalize nodelta * |
---|
| 820 | [ #H @('bind_inversion H) -H #st_no_pc_pre_call #EQst_no_pc_pre_call |
---|
| 821 | whd in match set_no_pc; normalize nodelta] |
---|
| 822 | #EQst_no_pc_after_call #EQ destruct(EQ) |
---|
[2843] | 823 | [ letin pairpc ≝ (beval_pair_of_pc |
---|
| 824 | (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) mid1)) |
---|
| 825 | %{(mk_state_pc ? (set_regs ERTL_state |
---|
| 826 | (〈add ?? (\fst (regs … st2)) r (\snd pairpc),\snd(regs … st2)〉) |
---|
| 827 | st_no_pc_pre_call) |
---|
[2801] | 828 | (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) mid1) |
---|
| 829 | (last_pop … st2))} |
---|
| 830 | | %{st2} |
---|
| 831 | ] |
---|
| 832 | % |
---|
| 833 | [1,3: @hide_prf whd in ⊢ (??%?); whd in match fetch_statement; normalize nodelta |
---|
| 834 | >EQcalling' >m_return_bind [>point_of_pc_of_point ] >EQcall >m_return_bind %] |
---|
| 835 | % |
---|
| 836 | [1,3: % |
---|
| 837 | [1,3: whd in ⊢ (??%%); whd in match fetch_statement in ⊢ (??%?); |
---|
| 838 | normalize nodelta >EQcalling' in ⊢ (??(match % with [_ ⇒ ? | _ ⇒ ?])?); |
---|
| 839 | >m_return_bind in ⊢ (??(match % with [_ ⇒ ? | _ ⇒ ?])?); |
---|
| 840 | [ >point_of_pc_of_point in ⊢ (??(match % with [_ ⇒ ? | _ ⇒ ?])?);] |
---|
| 841 | >EQcall in ⊢ (??(match % with [_ ⇒ ? | _ ⇒ ?])?); normalize nodelta |
---|
| 842 | >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in ⊢ (???(match % with [_ ⇒ ? | _ ⇒ ?])); |
---|
[2940] | 843 | >EQfetch' in ⊢ (???(match % with [_ ⇒ ? | _ ⇒ ?])); normalize nodelta |
---|
[2943] | 844 | cases daemon (* CSC: The proof used to be %, why did it change? *) |
---|
| 845 | (* |
---|
| 846 | XXX |
---|
[2940] | 847 | |
---|
| 848 | [cut (block_of_call |
---|
| 849 | (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_size) |
---|
| 850 | (globals |
---|
| 851 | (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_size)) |
---|
| 852 | (ev_genv |
---|
| 853 | (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_size)) |
---|
| 854 | (inr ident … 〈c_ptr1,c_ptr2〉) |
---|
| 855 | (set_regs ERTL_state |
---|
| 856 | 〈add RegisterTag beval (\fst (regs ERTLptr_semantics st2)) r |
---|
| 857 | (\snd (beval_pair_of_pc |
---|
| 858 | (pc_of_point ERTLptr_semantics |
---|
| 859 | (pc_block (pc ERTLptr_semantics st2)) mid1))), |
---|
| 860 | \snd (regs ERTLptr_semantics st2)〉 |
---|
| 861 | st_no_pc_pre_call) = |
---|
| 862 | block_of_call (mk_prog_params ERTL_semantics prog stack_size) |
---|
| 863 | (globals (mk_prog_params ERTL_semantics prog stack_size)) |
---|
| 864 | (ev_genv (mk_prog_params ERTL_semantics prog stack_size)) |
---|
| 865 | (inr ident … 〈c_ptr1,c_ptr2〉) |
---|
| 866 | (sigma_state_pc prog f_lbls f_regs st2)) |
---|
[2942] | 867 | |
---|
[2943] | 868 | [2: #URCA <URCA cases block_of_call #xyz |
---|
| 869 | [2: whd in ⊢ (??%%); %] |
---|
| 870 | >m_return_bind >m_return_bind |
---|
| 871 | whd in match fetch_internal_function; normalize nodelta |
---|
| 872 | whd in match fetch_function; normalize nodelta |
---|
[2942] | 873 | XXX |
---|
[2943] | 874 | %*) |
---|
[2801] | 875 | |*: whd in match sigma_stored_pc; whd in match sigma_pc_opt; normalize nodelta |
---|
| 876 | @if_elim change with (pc_block(pc … st2)) in match (pc_block ?); |
---|
| 877 | [1,3: @eqZb_elim [2,4: #_ *] #EQbl #_ |
---|
| 878 | >fetch_internal_function_no_minus_one in EQcalling'; [2,4: assumption] |
---|
| 879 | whd in ⊢ (???% → ?); #ABS destruct(ABS) ] #_ |
---|
| 880 | [ >point_of_pc_of_point >(get_sigma_last … good … EQfn EQstmt EQlabels) |
---|
| 881 | | >(get_sigma_idempotent … good … EQfn EQstmt EQlabels) |
---|
| 882 | ] |
---|
| 883 | >m_return_bind >pc_of_point_of_pc % |
---|
| 884 | ] |
---|
| 885 | |4: %{(taa_base …)} |
---|
[2843] | 886 | | %{(taaf_to_taa ??? |
---|
| 887 | (produce_trace_any_any_free |
---|
| 888 | (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_size) |
---|
[2801] | 889 | st2 ????? |
---|
[2843] | 890 | (mk_state_pc ? |
---|
| 891 | (set_regs ERTL_state |
---|
| 892 | (〈add ?? (\fst (regs … st2)) r (\snd pairpc),\snd(regs … st2)〉) |
---|
| 893 | st_no_pc_pre_call) |
---|
| 894 | (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) mid1) |
---|
| 895 | (last_pop … st2)) |
---|
| 896 | EQcalling' m_fetch_pre ?) ?)} |
---|
| 897 | [ @if_elim [2: #_ @I] #_ % whd in ⊢ (% → ?); whd in match (as_label ??); |
---|
| 898 | whd in match (as_pc_of ??); whd in match fetch_statement; normalize nodelta |
---|
| 899 | >EQcalling' >m_return_bind whd in match point_of_pc; normalize nodelta |
---|
| 900 | >point_of_offset_of_point >EQcall >m_return_bind normalize nodelta |
---|
| 901 | whd in match cost_label_of_stmt; normalize nodelta * #H @H % |
---|
| 902 | | whd in match repeat_eval_seq_no_pc; normalize nodelta whd in ⊢ (??%?); |
---|
| 903 | whd in match eval_seq_no_pc in ⊢ (??match % with [_ ⇒ ?| _ ⇒ ?]?); |
---|
| 904 | normalize nodelta whd in match (eval_ext_seq ????????); |
---|
| 905 | whd in match (get_pc_from_label ?????); whd in match block_of_funct_id; |
---|
| 906 | normalize nodelta @('bind_inversion EQfn) * #f2 * #fn2 |
---|
| 907 | whd in match fetch_function; normalize nodelta #H |
---|
| 908 | lapply(opt_eq_from_res ???? H) -H #H @('bind_inversion H) -H #f3 #EQf3 |
---|
| 909 | #H @('bind_inversion H) -H #fn4 #_ whd in ⊢ (??%%→ ??%% → ?); #EQ1 #EQ2 |
---|
| 910 | destruct(EQ1 EQ2) |
---|
| 911 | >(find_symbol_transf … |
---|
| 912 | (λvars.transf_fundef … (λfn.(b_graph_translate … fn))) prog f) |
---|
| 913 | >(symbol_of_block_rev … EQf3) >m_return_bind >code_block_of_block_eq |
---|
| 914 | normalize nodelta >(pc_of_label_eq … EQcalling') normalize nodelta |
---|
| 915 | whd in ⊢ (??%?); |
---|
| 916 | whd in match eval_seq_no_pc in ⊢ (??match % with [_ ⇒ ?| _ ⇒ ?]?); |
---|
| 917 | normalize nodelta whd in match (eval_ext_seq ????????); |
---|
| 918 | whd in match acca_arg_retrieve; normalize nodelta |
---|
| 919 | change with (ps_reg_retrieve ??) in match (acca_arg_retrieve_ ?????); |
---|
| 920 | whd in match ps_reg_retrieve; whd in match reg_retrieve; normalize nodelta |
---|
| 921 | >lookup_add_hit >m_return_bind whd in match set_regs; normalize nodelta |
---|
| 922 | @('bind_inversion EQst_no_pc_pre_call) #new_st whd in match push in ⊢ (%→ ?); |
---|
| 923 | normalize nodelta #H @('bind_inversion H) -H #is1 #EQis1 whd in ⊢ (??%% → ?); |
---|
| 924 | #EQ destruct(EQ) #H @('bind_inversion H) -H #is2 #EQis2 whd in match set_istack; |
---|
| 925 | normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ) whd in match push; |
---|
| 926 | normalize nodelta >EQis1 >m_return_bind whd in match set_istack; normalize nodelta |
---|
| 927 | whd in ⊢ (??%?); whd in match eval_seq_no_pc in ⊢ (??match % with [_ ⇒ ?| _ ⇒ ?]?); |
---|
| 928 | normalize nodelta whd in match (eval_ext_seq ????????); |
---|
| 929 | whd in match (get_pc_from_label ?????); whd in match block_of_funct_id; |
---|
| 930 | normalize nodelta |
---|
| 931 | >(find_symbol_transf … |
---|
| 932 | (λvars.transf_fundef … (λfn.(b_graph_translate … fn))) prog f) |
---|
| 933 | >(symbol_of_block_rev … EQf3) >m_return_bind >code_block_of_block_eq |
---|
| 934 | normalize nodelta >(pc_of_label_eq … EQcalling') normalize nodelta |
---|
| 935 | whd in ⊢ (??%?); |
---|
| 936 | whd in match eval_seq_no_pc in ⊢ (??match % with [_ ⇒ ?| _ ⇒ ?]?); |
---|
| 937 | normalize nodelta whd in match (eval_ext_seq ????????); |
---|
| 938 | whd in match acca_arg_retrieve; normalize nodelta |
---|
| 939 | change with (ps_reg_retrieve ??) in match (acca_arg_retrieve_ ?????); |
---|
| 940 | whd in match ps_reg_retrieve; whd in match reg_retrieve; normalize nodelta |
---|
| 941 | >lookup_add_hit >m_return_bind whd in match set_regs; normalize nodelta |
---|
| 942 | whd in match push; normalize nodelta >EQis2 >m_return_bind normalize nodelta |
---|
| 943 | whd in ⊢ (??%?); @eq_f whd in match set_istack; normalize nodelta |
---|
| 944 | whd in match reg_store; normalize nodelta >add_idempotent % |
---|
| 945 | | cut(∀st,st',kind.ertlptr_save_frame kind it st = return st' → |
---|
| 946 | ∃hd,tl.st_frms … st' = return (cons ? hd tl) ∧ |
---|
| 947 | \snd hd = pc_block (pc … st)) |
---|
| 948 | [ #st * #frms #is #b #regs #m * whd in match ertlptr_save_frame; |
---|
| 949 | normalize nodelta [ >m_return_bind | #H @('bind_inversion H) -H #st'' #EQst''] |
---|
| 950 | #H @('bind_inversion H) -H #frames #H lapply(opt_eq_from_res ???? H) -H |
---|
| 951 | #EQframes whd in ⊢ (??%% → ?); whd in match set_frms; whd in match set_regs; |
---|
| 952 | normalize nodelta #EQ destruct(EQ) %{(〈\fst (regs ERTLptr_semantics ?),pc_block (pc … st)〉)} |
---|
| 953 | [2,4: %{frames} % [1,3: %] |1,3:] %] |
---|
| 954 | ] #save_frame_non_empty cases(save_frame_non_empty … EQst_no_pc_after_call) |
---|
| 955 | * #fst_hd #snd_hd * #rest * #EQrest #EQhd |
---|
| 956 | ] |
---|
| 957 | cases(b_graph_transform_program_fetch_internal_function … good c_bl' f1 fn1 ?) |
---|
| 958 | [2,4: whd in match fetch_internal_function; normalize nodelta >EQfn1 %] |
---|
| 959 | #init * #t_fn1 ** #EQt_fn1 #_ * #_ #_ #_ #EQentry #_ #_ #_ #_ #_ #_ #_ |
---|
| 960 | [ %{(mk_state_pc ? st_no_pc_after_call |
---|
| 961 | (pc_of_point |
---|
| 962 | (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_size) |
---|
| 963 | c_bl' (joint_if_entry … t_fn1)) |
---|
| 964 | (last_pop … st2))} |
---|
| 965 | | |
---|
| 966 | %{(mk_state_pc ? (set_frms ERTL_state (〈(add ?? (fst_hd) r (\snd pairpc)),snd_hd〉 |
---|
| 967 | :: rest) |
---|
| 968 | st_no_pc_after_call) |
---|
| 969 | (pc_of_point |
---|
| 970 | (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_size) |
---|
| 971 | c_bl' (joint_if_entry … t_fn1)) |
---|
| 972 | (last_pop … st2))} |
---|
| 973 | ] |
---|
[2783] | 974 | % |
---|
[2843] | 975 | [1,3: whd in match sigma_state_pc; normalize nodelta |
---|
| 976 | whd in match pc_of_point in ⊢ (???%); normalize nodelta |
---|
| 977 | whd in match fetch_internal_function; normalize nodelta >EQfn1 |
---|
| 978 | >m_return_bind normalize nodelta @eq_f3 |
---|
| 979 | [1,3,6: % |2,5: >EQentry %] |
---|
| 980 | whd in match sigma_state; normalize nodelta |
---|
| 981 | cut(∀ a1,a2,b1,b2,c1,c2,d1,d2,e1,e2. |
---|
| 982 | a1=a2 → b1 = b2 → c1 = c2 → d1 = d2 → e1 = e2 → |
---|
| 983 | mk_state ERTL_semantics a1 b1 c1 d1 e1 = |
---|
| 984 | mk_state ERTL_semantics a2 b2 c2 d2 e2) |
---|
| 985 | [1,3: #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 |
---|
| 986 | #H15 //] #APP @APP try % |
---|
| 987 | whd in match set_frms; normalize nodelta >EQrest |
---|
| 988 | whd in match sigma_frames; normalize nodelta >m_return_bind |
---|
| 989 | >m_return_bind whd in match sigma_frames_opt; whd in match m_list_map; |
---|
| 990 | normalize nodelta whd in match (foldr ?????) in ⊢ (???%); |
---|
| 991 | normalize nodelta >EQhd >EQfn >m_return_bind normalize nodelta |
---|
| 992 | whd in match (foldr ?????); normalize nodelta |
---|
| 993 | >EQfn >m_return_bind normalize nodelta |
---|
| 994 | change with (sigma_frames_opt prog f_lbls f_regs ?) |
---|
| 995 | in match (foldr ?????); |
---|
| 996 | change with (sigma_frames_opt prog f_lbls f_regs ?) |
---|
| 997 | in match (foldr ?????); |
---|
| 998 | cases(sigma_frames_opt ????) [%] #t_rest >m_return_bind >m_return_bind |
---|
| 999 | @eq_f @eq_f2 [2: %] @eq_f2 [2: %] |
---|
| 1000 | change with (pc_block (pc … st2)) in match (pc_block ?); |
---|
| 1001 | change with (pc_block (pc … st2)) in match (pc_block ?); |
---|
| 1002 | whd in match sigma_register_env; normalize nodelta |
---|
| 1003 | >map_add >set_minus_add [%] @list_as_set_mem @in_added_registers |
---|
| 1004 | [@(point_of_pc ERTL_semantics (pc ERTLptr_semantics st2)) |
---|
| 1005 | | whd in match code_has_label; whd in match code_has_point; normalize nodelta |
---|
| 1006 | >EQstmt % | >EQregisters % % ] |
---|
| 1007 | |*: whd in match fetch_statement; normalize nodelta; >EQcalling' >m_return_bind |
---|
| 1008 | [2: >point_of_pc_of_point ] >EQcall >m_return_bind normalize nodelta |
---|
| 1009 | >m_return_bind |
---|
| 1010 | [2: >EQc_bl' >m_return_bind |
---|
| 1011 | | whd in match block_of_call; normalize nodelta |
---|
| 1012 | @('bind_inversion EQst_no_pc_pre_call) #st3 #H @('bind_inversion H) -H |
---|
| 1013 | #is3 inversion(istack … st2) [2: #bv |3: #bv1 #bv2] #EQis3 |
---|
| 1014 | whd in match is_push; normalize nodelta whd in ⊢ (??%% → ??%% → ?); |
---|
| 1015 | #EQ1 #EQ2 destruct(EQ1 EQ2) #H @('bind_inversion H) -H #is3 |
---|
| 1016 | whd in ⊢ (??%% → ??%% → ?); #EQ1 #EQ2 destruct(EQ1 EQ2) |
---|
| 1017 | whd in match set_regs; whd in match dpl_arg_retrieve; normalize nodelta |
---|
| 1018 | change with (ps_arg_retrieve ??) in match (dpl_arg_retrieve_ ?????); |
---|
| 1019 | @('bind_inversion EQc_bl') #c_bl'' whd in match dpl_arg_retrieve; normalize nodelta |
---|
| 1020 | change with (ps_arg_retrieve ??) in match (dpl_arg_retrieve_ ?????); |
---|
| 1021 | #H @('bind_inversion H) -H #bv_ptr1 whd in match ps_arg_retrieve; |
---|
| 1022 | normalize nodelta cases (c_ptr1) in EQstmt; [#r_ptr1 | #b_ptr1] #EQstmt |
---|
| 1023 | normalize nodelta |
---|
| 1024 | [ whd in match ps_reg_retrieve; whd in match reg_retrieve; normalize nodelta |
---|
| 1025 | #H lapply(opt_eq_from_res ???? H) -H #EQbv_ptr1 |
---|
| 1026 | | whd in ⊢ (??%% → ?); #EQ destruct(EQ) |
---|
| 1027 | ] |
---|
| 1028 | whd in match dph_arg_retrieve; normalize nodelta |
---|
| 1029 | change with (ps_arg_retrieve ??) in match (dph_arg_retrieve_ ?????); |
---|
| 1030 | whd in match ps_arg_retrieve; normalize nodelta cases c_ptr2 in EQstmt; |
---|
| 1031 | [1,3: #r_ptr2 |*: #b_ptr2] #EQstmt normalize nodelta |
---|
| 1032 | [1,2: whd in match ps_reg_retrieve; whd in match reg_retrieve; |
---|
| 1033 | normalize nodelta #H @('bind_inversion H) -H |
---|
| 1034 | #bv_ptr2 #H lapply(opt_eq_from_res ???? H) -H #EQbv_ptr2 |
---|
| 1035 | |*: >m_return_bind |
---|
| 1036 | ] #H @('bind_inversion H) -H #ptr #EQptr @if_elim #ptr_ok whd in ⊢ (??%% → ?); |
---|
| 1037 | #EQ destruct(EQ) #H lapply(opt_eq_from_res ???? H) -H #EQptr_code |
---|
| 1038 | [2,4: >m_return_bind |
---|
| 1039 | |*: >lookup_add_miss |
---|
| 1040 | [1,3: >EQbv_ptr1 >m_return_bind |
---|
| 1041 | |*: % #ABS destruct(ABS) |
---|
| 1042 | lapply(fresh_regs (point_of_pc ERTL_semantics (pc … st2))) |
---|
| 1043 | >EQregisters whd in ⊢ (% → ?); *** #ABS #_ #_ @ABS |
---|
| 1044 | lapply(regs_are_in_univers … (pi2 ?? fn) … EQstmt) whd in match stmt_registers; |
---|
| 1045 | whd in match get_used_registers_from_step; normalize nodelta |
---|
| 1046 | whd in ⊢ (???% → ?); * // |
---|
| 1047 | ] |
---|
| 1048 | ] |
---|
| 1049 | change with (ps_arg_retrieve ??) in match (dph_arg_retrieve_ ?????); |
---|
| 1050 | whd in match ps_arg_retrieve; normalize nodelta |
---|
| 1051 | [2,4: >m_return_bind |
---|
| 1052 | |*: whd in match ps_reg_retrieve; whd in match reg_retrieve; |
---|
| 1053 | normalize nodelta >lookup_add_miss |
---|
| 1054 | [1,3: >EQbv_ptr2 >m_return_bind |
---|
| 1055 | |*: % #ABS destruct(ABS) |
---|
| 1056 | lapply(fresh_regs (point_of_pc ERTL_semantics (pc … st2))) |
---|
| 1057 | >EQregisters whd in ⊢ (% → ?); *** #ABS #_ #_ @ABS |
---|
| 1058 | lapply(regs_are_in_univers … (pi2 ?? fn) … EQstmt) whd in match stmt_registers; |
---|
| 1059 | whd in match get_used_registers_from_step; normalize nodelta |
---|
| 1060 | whd in ⊢ (???% → ?); * // #_ * // |
---|
| 1061 | ] |
---|
| 1062 | ] |
---|
| 1063 | >EQptr >m_return_bind @if_elim [2,4,6,8: >ptr_ok *] #_ >m_return_bind |
---|
| 1064 | >EQptr_code >m_return_bind |
---|
[2783] | 1065 | ] |
---|
[2843] | 1066 | @('bind_inversion EQt_fn1) * #f2 * #fn2 #EQfn2 normalize nodelta |
---|
| 1067 | whd in ⊢ (??%% → ?); #EQ destruct(EQ) >EQfn2 >m_return_bind normalize nodelta |
---|
| 1068 | [ change with (ertlptr_save_frame ? it ?) in match (save_frame ??????); |
---|
| 1069 | cut(st2 = mk_state_pc ? st2 (pc … st2) (last_pop … st2)) |
---|
| 1070 | [ cases st2 #H1 #H2 #H3 %] #EQ <EQ -EQ >EQst_no_pc_after_call |
---|
| 1071 | >m_return_bind |
---|
| 1072 | |*: change with (ertlptr_save_frame PTR it ?) in match (save_frame ??????); |
---|
| 1073 | @('bind_inversion EQst_no_pc_after_call) #st4 whd in ⊢ (??%% → ?); |
---|
| 1074 | #EQ destruct(EQ) #H @('bind_inversion H) -H #frms4 #H |
---|
| 1075 | lapply(opt_eq_from_res ???? H) -H #EQfrms4 whd in ⊢ (??%% → ?); |
---|
| 1076 | #EQ destruct(EQ) whd in match ertlptr_save_frame; normalize nodelta |
---|
| 1077 | >m_return_bind whd in EQrest : (???%); destruct(EQrest) >EQfrms4 |
---|
| 1078 | >m_return_bind |
---|
[2783] | 1079 | ] |
---|
[2843] | 1080 | change with (stack_size ?) in match (stack_sizes ????); >EQs_size |
---|
| 1081 | >m_return_bind % |
---|
[2783] | 1082 | ] |
---|
[2843] | 1083 | qed. |
---|
| 1084 | |
---|
[2783] | 1085 | |
---|
| 1086 | inductive ex_Type1 (A:Type[1]) (P:A → Prop) : Prop ≝ |
---|
| 1087 | ex1_intro: ∀ x:A. P x → ex_Type1 A P. |
---|
| 1088 | (*interpretation "exists in Type[1]" 'exists x = (ex_Type1 ? x).*) |
---|
| 1089 | |
---|
| 1090 | lemma ertl_to_ertlptr_ok: |
---|
[2843] | 1091 | ∀prog.∀stack_sizes. |
---|
[2783] | 1092 | let trans_prog ≝ ertl_to_ertlptr prog in |
---|
| 1093 | ex_Type1 … (λR. |
---|
| 1094 | status_simulation |
---|
| 1095 | (ERTL_status prog stack_sizes) (ERTLptr_status trans_prog stack_sizes) R). |
---|
[2843] | 1096 | #prog #stack_size |
---|
| 1097 | cases(make_b_graph_transform_program_props ERTL_semantics ERTLptr_semantics |
---|
| 1098 | (λglobals,fn.«translate_data globals fn,(refl …)») prog) |
---|
| 1099 | #fregs * #f_lbls * #f_bl_r #good % |
---|
[2783] | 1100 | [@ERTLptrStatusSimulation assumption] |
---|
| 1101 | whd in match status_simulation; normalize nodelta |
---|
| 1102 | whd in match ERTL_status; whd in match ERTLptr_status; normalize nodelta |
---|
| 1103 | whd in ⊢ (% → % → % → % → ?); #st1 #st1' #st2 |
---|
| 1104 | change with |
---|
| 1105 | (eval_state ERTL_semantics (prog_var_names ???) ?? = ? → ?) |
---|
| 1106 | #EQeval @('bind_inversion EQeval) |
---|
| 1107 | ** #id #fn #stmt #H lapply (err_eq_from_io ????? H) -H #EQfetch |
---|
| 1108 | #_ whd in match ERTLptrStatusSimulation; normalize nodelta #EQst2 destruct |
---|
| 1109 | cases stmt in EQfetch; -stmt |
---|
| 1110 | [ * [ #cost | #called_id #args #dest| #reg #lbl | #seq] #nxt | #fin_step | *] |
---|
| 1111 | #EQfetch |
---|
[2843] | 1112 | change with (joint_classify ??) in |
---|
| 1113 | ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]); |
---|
| 1114 | [ (*COST*) whd in match joint_classify; normalize nodelta >EQfetch normalize nodelta |
---|
[2783] | 1115 | cases(eval_cost_ok … good … EQfetch EQeval) #st2' * #EQst2' * #taf #tafne |
---|
| 1116 | %{st2'} %{taf} >tafne normalize nodelta % [ % [@I | assumption]] |
---|
| 1117 | whd >EQst2' >(as_label_ok … good … st2') [%] cases daemon (* needs lemma see below!! *) |
---|
[2843] | 1118 | | (*CALL*) whd in match joint_classify; normalize nodelta >EQfetch |
---|
[2783] | 1119 | normalize nodelta #is_call_st1 |
---|
| 1120 | cases(eval_call_ok … good … EQfetch EQeval) #is_call_st1' |
---|
| 1121 | * #st2_pre_call * #is_call_st2_pre_call * * #Hcall |
---|
| 1122 | #call_rel * #taa * #st2' * #sem_rel #eval_rel |
---|
| 1123 | %{(«st2_pre_call,is_call_st2_pre_call»)} % [ % assumption] |
---|
| 1124 | %{st2'} %{st2'} %{taa} %{(taa_base …)} % [ % assumption] |
---|
| 1125 | whd >sem_rel >(as_label_ok … good … st2') [%] cases daemon (*TODO*) |
---|
[2843] | 1126 | | (*COND*) whd in match joint_classify; normalize nodelta >EQfetch |
---|
[2783] | 1127 | normalize nodelta #n_costed |
---|
| 1128 | cases(eval_cond_ok … good … EQfetch EQeval) [2: @n_costed] |
---|
| 1129 | #st2' * #EQst2' * #taf #tafne %{st2'} %{taf} >tafne % [% [@I|assumption]] |
---|
| 1130 | whd >EQst2' >(as_label_ok … good … st2') [%] cases daemon (*TODO*) |
---|
[2843] | 1131 | | (*seq*) whd in match joint_classify; normalize nodelta >EQfetch |
---|
[2783] | 1132 | normalize nodelta |
---|
| 1133 | cases (eval_seq_no_call_ok … good … EQfetch EQeval) |
---|
| 1134 | #st3 * #EQ destruct * #taf #taf_spec %{st3} %{taf} |
---|
| 1135 | % [% //] whd >(as_label_ok … good … st3) [%] |
---|
| 1136 | cases daemon (*needs lemma about preservation of fetch_statement *) |
---|
| 1137 | | cases fin_step in EQfetch; |
---|
| 1138 | [ (*GOTO*) #lbl #EQfetch whd in match joint_classify; normalize nodelta |
---|
[2843] | 1139 | >EQfetch normalize nodelta |
---|
[2783] | 1140 | cases (eval_goto_ok … good … EQfetch EQeval) |
---|
| 1141 | #st3 * #EQ destruct * #taf #tarne %{st3} %{taf} >tarne normalize nodelta |
---|
| 1142 | % [% //] whd >(as_label_ok … good … st3) [%] |
---|
| 1143 | cases daemon (*needs lemma about preservation of fetch_statement *) |
---|
| 1144 | | (*RETURN*) #EQfetch |
---|
| 1145 | whd in match joint_classify; normalize nodelta |
---|
[2843] | 1146 | >EQfetch normalize nodelta |
---|
[2783] | 1147 | cases (eval_return_ok … good … EQfetch EQeval) #is_ret |
---|
| 1148 | * #st3 * #EQ destruct * #after_ret * #taf ** #taf_prf #EQeval' #ret_prf |
---|
| 1149 | % [2: % [2: % [2: %{(taa_base …)} %{taf}] |*: ] |*:] |
---|
| 1150 | % [2: whd >(as_label_ok … good … st3) [%] cases daemon (*needs lemma *)] |
---|
| 1151 | % [2: assumption] % [2: %] % [2: assumption] % assumption |
---|
| 1152 | | (*TAILCALL*) * |
---|
| 1153 | ] |
---|
| 1154 | ] |
---|
| 1155 | qed. |
---|
| 1156 | |
---|
| 1157 | (* |
---|
[2662] | 1158 | lemma foo : |
---|
| 1159 | ∀P1_unser,P2_unser: unserialized_params. |
---|
| 1160 | ∀P1_sem_unser,P2_sem_unser. |
---|
| 1161 | let P1_sem ≝ make_sem_graph_params P1_unser P1_sem_unser in |
---|
| 1162 | let P2_sem ≝ make_sem_graph_params P2_unser P2_sem_unser in |
---|
| 1163 | ∀init,translate_step. |
---|
| 1164 | ∀translate_fin_step. |
---|
| 1165 | ∀closed_graph_translate. |
---|
| 1166 | let translate_internal : |
---|
| 1167 | ∀globals. |
---|
| 1168 | joint_closed_internal_function P1_sem globals → |
---|
| 1169 | joint_closed_internal_function P2_sem globals |
---|
| 1170 | ≝ |
---|
| 1171 | λglobals,fun. |
---|
| 1172 | «b_graph_translate (mk_graph_params P1_sem) (mk_graph_params P2_sem) globals |
---|
| 1173 | (init globals) |
---|
| 1174 | (translate_step globals) |
---|
| 1175 | (translate_fin_step globals) |
---|
| 1176 | (pi1 … fun), closed_graph_translate globals fun» in |
---|
| 1177 | ∀prog. |
---|
| 1178 | let trans_prog ≝ transform_program ??? prog (λvarnames. transf_fundef ?? (translate_internal varnames)) in |
---|
| 1179 | ∀stack_size. |
---|
| 1180 | ∀sigma_state_pc. |
---|
| 1181 | (∀s. pc_block (pc … (sigma_state_pc s)) = pc_block … (pc … s)) → |
---|
| 1182 | ∀st : state_pc P2_sem. |
---|
| 1183 | ∀st' : state_pc P1_sem. |
---|
| 1184 | ∀f. |
---|
| 1185 | ∀fn: joint_closed_internal_function P1_sem (globals (mk_prog_params P1_sem prog stack_size)). |
---|
| 1186 | luniverse_ok … fn → |
---|
| 1187 | ∀stmt,nxt. |
---|
[2666] | 1188 | ∀P : (state_pc P2_sem) → Prop. |
---|
[2662] | 1189 | (∀pre_Instrs',last_Instrs',dst. |
---|
| 1190 | ∃st''.∃st'''.∃st''''. |
---|
| 1191 | repeat_eval_seq_no_pc (mk_prog_params P2_sem trans_prog stack_size) |
---|
| 1192 | f (translate_internal ? fn) (map_eval ?? pre_Instrs' dst) st = return st''' ∧ |
---|
| 1193 | eval_seq_no_pc ? (prog_var_names … trans_prog) (ev_genv … (mk_prog_params P2_sem trans_prog stack_size)) |
---|
| 1194 | f (translate_internal … fn) (last_Instrs' dst) st''' = return st'''' ∧ |
---|
| 1195 | st'' = (mk_state_pc (mk_prog_params P2_sem trans_prog stack_size) |
---|
| 1196 | st'''' (pc_of_point P2_sem (pc_block (pc … (sigma_state_pc st))) dst) (last_pop … st)) ∧ |
---|
[2666] | 1197 | P st'' (*st' = sigma_state_pc st''*) ∧ |
---|
[2662] | 1198 | let P2_prog_params ≝ mk_prog_params P2_sem trans_prog stack_size in |
---|
| 1199 | let P2_globals ≝ globals P2_prog_params in |
---|
| 1200 | All |
---|
| 1201 | (joint_seq … P2_globals) |
---|
| 1202 | (no_cost_label … P2_globals) |
---|
| 1203 | (map_eval (code_point P2_sem) (joint_seq … P2_globals) pre_Instrs' dst)) → |
---|
| 1204 | fetch_statement … |
---|
| 1205 | (prog_var_names (joint_function P1_sem) ℕ prog) |
---|
| 1206 | (ev_genv (mk_prog_params P1_sem prog stack_size)) |
---|
| 1207 | (pc … (sigma_state_pc st)) = |
---|
| 1208 | return 〈f, fn, sequential … (step_seq P1_sem … stmt) nxt〉 → |
---|
| 1209 | eval_state … |
---|
| 1210 | (prog_var_names (joint_function P1_sem) ℕ prog) |
---|
| 1211 | (ev_genv … (mk_prog_params P1_sem prog stack_size)) |
---|
| 1212 | (sigma_state_pc st) = return st' → |
---|
| 1213 | ∃st''. (*CSC: this needs to be linked back again st' = sigma_state_pc ? good st'' ∧*) |
---|
[2666] | 1214 | P st'' ∧ |
---|
[2662] | 1215 | ∃taf : trace_any_any_free (joint_abstract_status (mk_prog_params P2_sem trans_prog stack_size)) st st''. |
---|
[2666] | 1216 | (if taaf_non_empty … taf then True else |
---|
| 1217 | (¬as_costed (joint_abstract_status (mk_prog_params P1_sem prog stack_size)) (sigma_state_pc st) ∨ |
---|
| 1218 | ¬as_costed (joint_abstract_status (mk_prog_params P1_sem prog stack_size)) st')) |
---|
| 1219 | (* the length of taf is the same of the length of ??? *). |
---|
[2662] | 1220 | #P1_unser #P2_unser #P1_sem_unser #P2_sem_unser |
---|
| 1221 | letin P1_sem ≝ (make_sem_graph_params P1_unser P1_sem_unser) |
---|
| 1222 | letin P2_sem ≝ (make_sem_graph_params P2_unser P2_sem_unser) |
---|
| 1223 | #init #translate_step #translate_fin_step #closed_graph_translate. |
---|
| 1224 | letin translate_internal ≝ |
---|
| 1225 | (λglobals,fun. |
---|
| 1226 | «b_graph_translate (mk_graph_params P1_sem) (mk_graph_params P2_sem) globals |
---|
| 1227 | (init globals) |
---|
| 1228 | (translate_step globals) |
---|
| 1229 | (translate_fin_step globals) |
---|
| 1230 | (pi1 … fun), closed_graph_translate globals fun») |
---|
| 1231 | #prog |
---|
| 1232 | letin trans_prog ≝ (transform_program ??? prog (λvarnames. transf_fundef ?? (translate_internal varnames))) |
---|
[2666] | 1233 | #stack_size #sigma_state_pc #sigma_state_pc_ok #st #st' #f #fn #fn_universe_ok #stmt #nxt #P |
---|
| 1234 | #Hpass #EQfetch lapply(fetch_statement_inv … EQfetch) * #EQfn #EQstmt |
---|
[2662] | 1235 | cases |
---|
| 1236 | (b_graph_translate_ok … (init …) (translate_step …) (translate_fin_step …) … fn_universe_ok) |
---|
| 1237 | #_ * #MK_fresh_labels * #MK_fresh_registers **** #_ #_ #_ #_ (*CSC: useful things thrown out here *) |
---|
| 1238 | #MULTI_FETCH_OK cases (MULTI_FETCH_OK … EQstmt) |
---|
| 1239 | #list_b_last * #fresh_registers ** #EQlist_b_last #EQfresh_registers |
---|
| 1240 | normalize nodelta * #Instrs * #fresh_registers_spec whd in ⊢ (% → ?); |
---|
| 1241 | @pair_elim #pre_Instrs #last_Instrs #EQInstrs * #dst * #Multi_fetch #STEP_in_code |
---|
| 1242 | #EQeval |
---|
| 1243 | cut((list |
---|
| 1244 | (code_point P2_sem |
---|
| 1245 | →joint_seq P2_sem (prog_var_names (joint_function P1_sem) ℕ prog)))) [ cases daemon (*Paolo should fix the lemma*)] |
---|
| 1246 | #pre_Instrs' |
---|
| 1247 | cut((code_point P2_sem |
---|
| 1248 | →joint_seq P2_sem (prog_var_names (joint_function P1_sem) ℕ prog))) [ cases daemon (*Paolo should fix the lemma*)] |
---|
| 1249 | #last_Instrs' |
---|
| 1250 | cases (Hpass pre_Instrs' last_Instrs' dst (* MANY MORE HERE *)) |
---|
| 1251 | #st'' * #st''' * #st'''' **** #REPEAT #EVAL_NO_PC_Last #EQst'' #EQst' #NO_COSTED |
---|
| 1252 | lapply(produce_trace_any_any_free … NO_COSTED … REPEAT) |
---|
| 1253 | [ cases daemon (* should be @Multi_fetch *) |
---|
| 1254 | | <sigma_state_pc_ok @(fetch_internal_function_transf … (λvars.translate_internal vars)) |
---|
| 1255 | assumption |
---|
| 1256 | | @dst |
---|
| 1257 | | @list_b_last (*wrong, should dst be destination or the last of list_b_last *) |
---|
| 1258 | ] #TAAF |
---|
| 1259 | lapply |
---|
| 1260 | (produce_step_trace (mk_prog_params P2_sem trans_prog stack_size) |
---|
| 1261 | (mk_state_pc (mk_prog_params P2_sem trans_prog stack_size) |
---|
| 1262 | st''' (pc_of_point P2_sem (pc_block (pc … st)) dst) (last_pop … st)) |
---|
| 1263 | f (translate_internal ? fn) (last_Instrs' dst) nxt st'''' … EVAL_NO_PC_Last) |
---|
| 1264 | [ cases daemon (* should be @STEP_In_code *) |
---|
| 1265 | | <sigma_state_pc_ok |
---|
| 1266 | @(fetch_internal_function_transf … (λvars. translate_internal vars) … EQfn) ] |
---|
| 1267 | #LAST_STEP |
---|
[2663] | 1268 | cases daemon |
---|
| 1269 | qed. |
---|
[2662] | 1270 | |
---|
| 1271 | lemma eval_seq_no_call_ok : |
---|
| 1272 | ∀prog. |
---|
| 1273 | let trans_prog ≝ ertl_to_ertlptr prog in |
---|
| 1274 | ∀good : (∀fn.good_state_transformation prog fn). |
---|
| 1275 | ∀stack_sizes. |
---|
| 1276 | (*? →*) |
---|
| 1277 | ∀st : state_pc ERTLptr_semantics. |
---|
| 1278 | ∀st' : state_pc ERTL_semantics. |
---|
| 1279 | ∀f,fn,stmt,nxt. |
---|
| 1280 | fetch_statement ERTL_semantics |
---|
| 1281 | (prog_var_names (joint_function ERTL_semantics) ℕ prog) |
---|
| 1282 | (ev_genv (mk_prog_params ERTL_semantics prog stack_sizes)) |
---|
| 1283 | (pc … (sigma_state_pc ? good st)) = |
---|
| 1284 | return 〈f, fn, sequential … (step_seq ERTL … stmt) nxt〉 → |
---|
| 1285 | eval_state ERTL_semantics |
---|
| 1286 | (prog_var_names (joint_function ERTL_semantics) ℕ prog) |
---|
| 1287 | (ev_genv … (mk_prog_params ERTL_semantics prog stack_sizes)) |
---|
| 1288 | (sigma_state_pc ? good st) = |
---|
| 1289 | return st' → |
---|
| 1290 | ∃st''. st' = sigma_state_pc ? good st'' ∧ |
---|
| 1291 | ∃taf : trace_any_any_free (ERTLptr_status trans_prog stack_sizes) |
---|
| 1292 | st |
---|
| 1293 | st''. |
---|
| 1294 | bool_to_Prop (taaf_non_empty … taf). |
---|
[2663] | 1295 | #prog #good #stack_size #st #st' #f #fn #stmt #nxt #EQfetch #EQeval |
---|
| 1296 | cases (foo … translate_step translate_fin_step … EQfetch EQeval) |
---|
| 1297 | [2,3: cases daemon (* first one, take out init definition from ERTLtoERTLptr; |
---|
| 1298 | second one to be taken from somewhere *) |
---|
| 1299 | |4: #x cases daemon (* TO BE DONE, EASY *) |
---|
[2666] | 1300 | |5: cases daemon (* to be taken in input *) |
---|
| 1301 | |6: @(λst''.st' = sigma_state_pc ? good st'') |
---|
| 1302 | |7: cases daemon |
---|
| 1303 | | #st'' * #EQ destruct * change with ERTL_uns in match (mk_unserialized_params ???????????????); |
---|
[2663] | 1304 | change with ERTLptr_uns in match (mk_unserialized_params ???????????????); |
---|
[2666] | 1305 | (* change with ERTL_semantics in match (make_sem_graph_params ??); |
---|
| 1306 | change with ERTLptr_semantics in match (make_sem_graph_params ??); *) |
---|
| 1307 | #taaf #Htaaf %{st''} |
---|
| 1308 | % [%] cases daemon |
---|
[2783] | 1309 | qed. *) |
---|