[2907] | 1 | include "ASM/Interpret.ma". |
---|
[1648] | 2 | |
---|
[2907] | 3 | definition ASMRegisterRets: list [[ acc_a; direct; registr ]] ≝ |
---|
[3028] | 4 | [ DIRECT (bitvector_of_nat 8 130); (* DPL *) |
---|
| 5 | DIRECT (bitvector_of_nat 8 131); (* DPH *) |
---|
[2907] | 6 | REGISTER [[ false; false; false ]]; (* Register00 *) |
---|
| 7 | REGISTER [[ false; false; true ]] ]. (* Register01 *) |
---|
| 8 | % qed. |
---|
[2498] | 9 | |
---|
[2907] | 10 | definition as_result_of_finaladdr: ∀T:Type[0]. ∀cm:T. PreStatus … cm → Word → option int ≝ |
---|
| 11 | λT,cm,st,finaladdr. |
---|
| 12 | if eq_bv ? (program_counter ?? st) finaladdr then |
---|
| 13 | let vals ≝ |
---|
| 14 | map [[acc_a;direct;registr]] ? (get_arg_8 ?? st false) (ASMRegisterRets⌈list ? ↦ ?⌉) in |
---|
| 15 | let dummy ≝ zero ? in |
---|
| 16 | let first_byte ≝ λl. match l with [ nil ⇒ 〈dummy,[]〉 | cons hd tl ⇒ 〈hd,tl〉] in |
---|
| 17 | let 〈b1,tl1〉 ≝ first_byte vals in |
---|
| 18 | let 〈b2,tl2〉 ≝ first_byte tl1 in |
---|
| 19 | let 〈b3,tl3〉 ≝ first_byte tl2 in |
---|
| 20 | let 〈b4,tl4〉 ≝ first_byte tl3 in |
---|
| 21 | Some ? (b4 @@ b3 @@ b2 @@ b1) |
---|
| 22 | else |
---|
| 23 | None ?. |
---|
| 24 | [ @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % | % ] |
---|
| 25 | qed. |
---|
[2573] | 26 | |
---|
[2910] | 27 | definition OC_as_call_ident: |
---|
| 28 | ∀prog:labelled_object_code.∀cm. (Σs:Status cm. OC_classify … s = cl_call) → ident |
---|
| 29 | ≝ |
---|
| 30 | λprog,cm,s0. |
---|
| 31 | let pc ≝ program_counter ?? (execute_1' cm s0) in |
---|
| 32 | match lookup_opt ?? pc (symboltable prog) with |
---|
| 33 | [ None ⇒ ⊥ | Some id ⇒ id ]. |
---|
| 34 | cases daemon (*CSC: we need a specification of the symboltable for this *) |
---|
| 35 | qed. |
---|
| 36 | |
---|
[2907] | 37 | definition OC_abstract_status: labelled_object_code → abstract_status ≝ |
---|
| 38 | λprog. |
---|
[1938] | 39 | mk_abstract_status |
---|
[2999] | 40 | (Status (cm prog)) |
---|
[2760] | 41 | (λs1,s2. execute_1 … s1 = s2) |
---|
[1938] | 42 | word_deqset |
---|
[2999] | 43 | (program_counter …) |
---|
| 44 | (OC_classify …) |
---|
[2907] | 45 | (λpc.lookup_opt … pc (costlabels prog)) |
---|
[2999] | 46 | (next_instruction_properly_relates_program_counters …) |
---|
| 47 | (λst. as_result_of_finaladdr … st (final_pc prog)) |
---|
| 48 | (OC_as_call_ident prog …) |
---|
[1938] | 49 | ?. |
---|
[2910] | 50 | * #st whd in ⊢ (??%? → ?); cases current_instruction [7: *] normalize |
---|
| 51 | try (#x #y #abs) try (#x #abs) try #abs destruct |
---|
[1938] | 52 | qed. |
---|
| 53 | |
---|
[1929] | 54 | definition trace_any_label_length ≝ |
---|
[2907] | 55 | λprog: labelled_object_code. |
---|
[1919] | 56 | λtrace_ends_flag: trace_ends_with_ret. |
---|
[2999] | 57 | λstart_status: Status (cm prog). |
---|
| 58 | λfinal_status: Status (cm prog). |
---|
[2907] | 59 | λthe_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status. |
---|
[1919] | 60 | as_trace_any_label_length' … the_trace. |
---|
[1911] | 61 | |
---|
[1921] | 62 | let rec all_program_counter_list |
---|
| 63 | (n: nat) |
---|
| 64 | on n ≝ |
---|
| 65 | match n with |
---|
| 66 | [ O ⇒ [ ] |
---|
| 67 | | S n' ⇒ (bitvector_of_nat 16 n')::(all_program_counter_list n') |
---|
| 68 | ]. |
---|
| 69 | |
---|
| 70 | lemma all_program_counter_list_bound_eq: |
---|
| 71 | ∀bound: nat. |
---|
| 72 | |all_program_counter_list bound| = bound. |
---|
| 73 | #bound elim bound try % |
---|
| 74 | #bound' #inductive_hypothesis normalize |
---|
| 75 | >inductive_hypothesis % |
---|
| 76 | qed. |
---|
| 77 | |
---|
| 78 | lemma mem_all_program_counter_list_lt_bound: |
---|
| 79 | ∀bound: nat. |
---|
| 80 | ∀bound_proof: bound ≤ 2^16. |
---|
| 81 | ∀e: Word. |
---|
| 82 | memb word_deqset e (all_program_counter_list bound) = true → |
---|
| 83 | nat_of_bitvector … e < bound. |
---|
| 84 | #bound elim bound |
---|
| 85 | [1: |
---|
| 86 | #bound_proof #e |
---|
| 87 | normalize #absurd destruct(absurd) |
---|
| 88 | |2: |
---|
| 89 | #bound' #inductive_hypothesis |
---|
| 90 | #bound_proof #e |
---|
| 91 | change with (if eq_bv ??? then ? else ? = ? → ?) |
---|
| 92 | @eq_bv_elim |
---|
| 93 | [1: |
---|
| 94 | #eq_assm |
---|
| 95 | normalize nodelta destruct #_ |
---|
| 96 | >nat_of_bitvector_bitvector_of_nat_inverse try assumption |
---|
| 97 | normalize % |
---|
| 98 | |2: |
---|
| 99 | #neq_assm normalize nodelta |
---|
| 100 | #memb_assm %2 @inductive_hypothesis |
---|
| 101 | try assumption |
---|
| 102 | @(transitive_le bound' (S bound')) |
---|
| 103 | try assumption %2 % |
---|
| 104 | ] |
---|
| 105 | ] |
---|
| 106 | qed. |
---|
| 107 | |
---|
| 108 | lemma lt_bound_mem_all_program_counter_list: |
---|
| 109 | ∀bound: nat. |
---|
| 110 | ∀bound_proof: bound ≤ 2^16. |
---|
| 111 | ∀e: Word. |
---|
| 112 | nat_of_bitvector … e < bound → |
---|
| 113 | memb word_deqset e (all_program_counter_list bound) = true. |
---|
| 114 | #bound elim bound |
---|
| 115 | [1: |
---|
| 116 | #bound_proof #e normalize |
---|
| 117 | #absurd cases (lt_to_not_zero … absurd) |
---|
| 118 | |2: |
---|
| 119 | #bound' #inductive_hypothesis |
---|
| 120 | #bound_proof #e |
---|
| 121 | change with (? → if eq_bv ??? then ? else ? = ?) |
---|
| 122 | #assm |
---|
| 123 | cases (le_to_or_lt_eq … (nat_of_bitvector 16 e) bound' ?) |
---|
| 124 | [1: |
---|
| 125 | #e_lt_assm |
---|
| 126 | @eq_bv_elim |
---|
| 127 | [1: |
---|
| 128 | #eq_assm normalize nodelta % |
---|
| 129 | |2: |
---|
| 130 | #neq_assm normalize nodelta |
---|
| 131 | @inductive_hypothesis try assumption |
---|
| 132 | @(transitive_le bound' (S bound')) try assumption |
---|
| 133 | %2 % |
---|
| 134 | ] |
---|
| 135 | |2: |
---|
| 136 | #relevant >eq_eq_bv normalize nodelta try % |
---|
| 137 | destruct >bitvector_of_nat_inverse_nat_of_bitvector % |
---|
| 138 | |3: |
---|
| 139 | normalize in assm; |
---|
| 140 | @le_S_S_to_le assumption |
---|
| 141 | ] |
---|
| 142 | ] |
---|
| 143 | qed. |
---|
| 144 | |
---|
| 145 | include alias "arithmetics/nat.ma". |
---|
| 146 | |
---|
[2573] | 147 | lemma execute_1_and_program_counter_after_other_in_lockstep00: |
---|
[1921] | 148 | ∀code_memory: BitVectorTrie Byte 16. |
---|
| 149 | ∀start_status: Status code_memory. |
---|
[2573] | 150 | let 〈instruction, pc, ticks〉 ≝ fetch code_memory (program_counter … start_status) in |
---|
| 151 | ASM_classify0 instruction = cl_other → |
---|
| 152 | program_counter ? ? (execute_1 … start_status) = |
---|
| 153 | program_counter_after_other pc instruction. |
---|
| 154 | #code_memory #start_status |
---|
| 155 | whd in match execute_1; normalize nodelta |
---|
| 156 | cases (execute_1' code_memory start_status) #the_status; * #_ |
---|
| 157 | cases (fetch ? ?); * #instruction #pc #ticks |
---|
| 158 | #classify_assm #classify_assm0 @classify_assm assumption |
---|
| 159 | qed. |
---|
| 160 | |
---|
| 161 | lemma execute_1_and_program_counter_after_other_in_lockstep0: |
---|
| 162 | ∀code_memory: BitVectorTrie Byte 16. |
---|
| 163 | ∀start_status: Status code_memory. |
---|
[2899] | 164 | OC_classify … start_status = cl_other → |
---|
[1921] | 165 | let 〈instruction, pc, ticks〉 ≝ fetch code_memory (program_counter … start_status) in |
---|
| 166 | program_counter ? ? (execute_1 … start_status) = |
---|
| 167 | program_counter_after_other pc instruction. |
---|
| 168 | #code_memory #start_status #classify_assm |
---|
| 169 | whd in match execute_1; normalize nodelta |
---|
| 170 | cases (execute_1' code_memory start_status) #the_status |
---|
| 171 | * #_ whd in classify_assm:(??%?); whd in match (current_instruction ??) in classify_assm; |
---|
| 172 | cases (fetch ? ?) in classify_assm; * #instruction #pc #ticks |
---|
| 173 | #classify_assm #classify_assm' @classify_assm' assumption |
---|
[1962] | 174 | qed. |
---|
[1921] | 175 | |
---|
[2573] | 176 | lemma execute_1_and_program_counter_after_other_in_lockstep: |
---|
[2907] | 177 | ∀prog: labelled_object_code. |
---|
[2999] | 178 | ∀start_status: Status (cm prog). |
---|
[2907] | 179 | as_classifier (OC_abstract_status prog) start_status cl_other → |
---|
[2999] | 180 | let 〈instruction, pc, ticks〉 ≝ fetch (cm prog) (program_counter … start_status) in |
---|
[2573] | 181 | program_counter ? ? (execute_1 … start_status) = |
---|
| 182 | program_counter_after_other pc instruction. |
---|
[2907] | 183 | #prog #start_status #classify_assm |
---|
[2756] | 184 | change with (ASM_classify0 ? = ?) in classify_assm; |
---|
[2573] | 185 | destruct (classify_assm) |
---|
| 186 | @execute_1_and_program_counter_after_other_in_lockstep0 assumption. |
---|
| 187 | qed. |
---|
| 188 | |
---|
[1921] | 189 | lemma sublist_tal_pc_list_all_program_counter_list: |
---|
[2907] | 190 | ∀prog: labelled_object_code. |
---|
[2999] | 191 | ∀start, final: Status (cm prog). |
---|
[1921] | 192 | ∀trace_ends_flag. |
---|
[2907] | 193 | ∀the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start final. |
---|
[1929] | 194 | sublist ? (tal_pc_list … the_trace) (all_program_counter_list (2^16)). |
---|
[2907] | 195 | #prog #start #final #trace_ends_flag #the_trace |
---|
[1921] | 196 | whd in match (sublist ???); #pc #memb_assm |
---|
[1929] | 197 | @lt_bound_mem_all_program_counter_list try % |
---|
| 198 | @nat_of_bitvector_lt_bound |
---|
[1921] | 199 | qed. |
---|
| 200 | |
---|
| 201 | corollary tal_pc_list_length_leq_total_program_size: |
---|
[2907] | 202 | ∀prog: labelled_object_code. |
---|
[2999] | 203 | ∀start, final: Status (cm prog). |
---|
[1921] | 204 | ∀trace_ends_flag. |
---|
[2907] | 205 | ∀the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start final. |
---|
[2575] | 206 | ∀unrepeating_witness: tal_unrepeating … the_trace. |
---|
[1929] | 207 | |tal_pc_list … the_trace| ≤ 2^16. |
---|
[2907] | 208 | #prog #start #final #trace_ends_flag #the_trace #unrepeating_witness |
---|
[1929] | 209 | <(all_program_counter_list_bound_eq (2^16)) |
---|
[1921] | 210 | @sublist_length |
---|
| 211 | [1: |
---|
| 212 | @tal_unrepeating_uniqueb |
---|
| 213 | assumption |
---|
| 214 | |2: |
---|
| 215 | @sublist_tal_pc_list_all_program_counter_list |
---|
| 216 | assumption |
---|
| 217 | ] |
---|
| 218 | qed. |
---|
| 219 | |
---|
[1658] | 220 | let rec compute_paid_trace_any_label |
---|
[2907] | 221 | (prog: labelled_object_code) (trace_ends_flag: trace_ends_with_ret) |
---|
[2999] | 222 | (start_status: Status (cm prog)) |
---|
| 223 | (final_status: Status (cm prog)) |
---|
[2907] | 224 | (the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status) |
---|
[1658] | 225 | on the_trace: nat ≝ |
---|
| 226 | match the_trace with |
---|
[1669] | 227 | [ tal_base_not_return the_status _ _ _ _ ⇒ current_instruction_cost … the_status |
---|
| 228 | | tal_base_return the_status _ _ _ ⇒ current_instruction_cost … the_status |
---|
[2656] | 229 | | tal_base_call pre_fun_call start_fun_call final _ _ _ _ _ ⇒ current_instruction_cost … pre_fun_call |
---|
| 230 | | tal_base_tailcall pre_fun_call start_fun_call final _ _ _ ⇒ current_instruction_cost … pre_fun_call |
---|
[1658] | 231 | | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final |
---|
[1902] | 232 | _ _ _ call_trace _ final_trace ⇒ |
---|
[1669] | 233 | let current_instruction_cost ≝ current_instruction_cost … pre_fun_call in |
---|
[2907] | 234 | let final_trace_cost ≝ compute_paid_trace_any_label prog end_flag … final_trace in |
---|
[1658] | 235 | current_instruction_cost + final_trace_cost |
---|
| 236 | | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒ |
---|
[1669] | 237 | let current_instruction_cost ≝ current_instruction_cost … status_pre in |
---|
[1658] | 238 | let tail_trace_cost ≝ |
---|
[2907] | 239 | compute_paid_trace_any_label prog end_flag |
---|
[1658] | 240 | status_init status_end tail_trace |
---|
| 241 | in |
---|
| 242 | current_instruction_cost + tail_trace_cost |
---|
[2656] | 243 | ]. |
---|
[1658] | 244 | |
---|
| 245 | definition compute_paid_trace_label_label ≝ |
---|
[2907] | 246 | λprog: labelled_object_code. |
---|
[1658] | 247 | λtrace_ends_flag: trace_ends_with_ret. |
---|
[2999] | 248 | λstart_status: Status (cm prog). |
---|
| 249 | λfinal_status: Status (cm prog). |
---|
[2907] | 250 | λthe_trace: (trace_label_label (OC_abstract_status prog) trace_ends_flag start_status final_status). |
---|
[1658] | 251 | match the_trace with |
---|
| 252 | [ tll_base ends_flag initial final given_trace labelled_proof ⇒ |
---|
| 253 | compute_paid_trace_any_label … given_trace |
---|
| 254 | ]. |
---|
| 255 | |
---|
[1684] | 256 | lemma trace_compute_paid_trace_cl_other: |
---|
[2907] | 257 | ∀prog : labelled_object_code. |
---|
[1669] | 258 | ∀program_counter' : Word. |
---|
| 259 | ∀program_size' : ℕ. |
---|
| 260 | ∀ticks : ℕ. |
---|
| 261 | ∀instruction : instruction. |
---|
| 262 | ∀program_counter'' : Word. |
---|
[2999] | 263 | ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch (cm prog) program_counter'). |
---|
[1910] | 264 | let program_counter''' ≝ program_counter_after_other program_counter'' instruction in |
---|
[2999] | 265 | ∀start_status : (Status (cm prog)). |
---|
| 266 | ∀final_status : (Status (cm prog)). |
---|
[1669] | 267 | ∀trace_ends_flag : trace_ends_with_ret. |
---|
[2907] | 268 | ∀the_trace : (trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status). |
---|
[2573] | 269 | ∀program_counter_refl : (program_counter' = program_counter … start_status). |
---|
[2575] | 270 | ∀size_invariant : trace_any_label_length … the_trace ≤S program_size'. |
---|
[1669] | 271 | ∀classify_assm: ASM_classify0 instruction = cl_other. |
---|
| 272 | ∀pi1 : ℕ. |
---|
[2907] | 273 | (if match lookup_opt costlabel 16 program_counter''' (costlabels prog) with |
---|
[1669] | 274 | [None ⇒ true |
---|
| 275 | |Some _ ⇒ false |
---|
| 276 | ] |
---|
| 277 | then |
---|
[2999] | 278 | ∀start_status0:Status (cm prog). |
---|
| 279 | ∀final_status0:Status (cm prog). |
---|
[1669] | 280 | ∀trace_ends_flag0:trace_ends_with_ret. |
---|
[2907] | 281 | ∀the_trace0:trace_any_label (OC_abstract_status prog) trace_ends_flag0 start_status0 final_status0. |
---|
[2575] | 282 | trace_any_label_length … the_trace0 ≤ program_size' → |
---|
[2573] | 283 | program_counter''' = program_counter … start_status0 → |
---|
[1901] | 284 | pi1 |
---|
[2575] | 285 | =compute_paid_trace_any_label … the_trace0 |
---|
[1669] | 286 | else (pi1=O) ) |
---|
[1906] | 287 | → ticks+pi1 |
---|
[2575] | 288 | =compute_paid_trace_any_label … the_trace. |
---|
[2907] | 289 | #prog #program_counter' #program_size' #ticks #instruction |
---|
[1929] | 290 | #program_counter'' #FETCH #start_status #final_status #trace_ends_flag #the_trace |
---|
| 291 | #program_counter_refl #size_invariant #classify_assm #recursive_block_cost |
---|
[1692] | 292 | #recursive_assm |
---|
| 293 | @(trace_any_label_inv_ind … the_trace) |
---|
[2575] | 294 | [2: |
---|
| 295 | #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm |
---|
| 296 | #start_status_refl #final_status_refl #the_trace_assm destruct @⊥ |
---|
| 297 | |3: |
---|
| 298 | #status_pre_fun_call #status_start_fun_call #status_final #execute_assm |
---|
| 299 | #classifier_assm #after_return_assm #trace_label_return #costed_assm |
---|
| 300 | #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl |
---|
| 301 | destruct @⊥ |
---|
[2656] | 302 | |4: |
---|
| 303 | #status_pre_fun_call #status_start_fun_call #status_final #execute_assm |
---|
| 304 | #classifier_assm #trace_label_return |
---|
| 305 | #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl |
---|
| 306 | destruct @⊥ |
---|
[2575] | 307 | |5: |
---|
| 308 | #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call |
---|
| 309 | #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return |
---|
| 310 | #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl |
---|
| 311 | #final_status_refl #the_trace_refl destruct @⊥ |
---|
| 312 | |6: |
---|
[1669] | 313 | #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label |
---|
| 314 | #classifier_assm #costed_assm #trace_ends_refl #start_status_refl #final_status_refl |
---|
| 315 | #the_trace_refl |
---|
| 316 | destruct |
---|
| 317 | whd in match (trace_any_label_length … (tal_step_default …)); |
---|
| 318 | whd in match (compute_paid_trace_any_label … (tal_step_default …)); |
---|
| 319 | whd in costed_assm:(?%); |
---|
| 320 | generalize in match costed_assm; |
---|
[2907] | 321 | generalize in match (refl … (lookup_opt … (program_counter … (execute_1 … status_pre)) (costlabels prog))); |
---|
[1927] | 322 | whd in match (as_label ??); |
---|
[2907] | 323 | generalize in match (lookup_opt … (program_counter … (execute_1 … status_pre)) (costlabels prog)) |
---|
[1927] | 324 | in ⊢ (??%? → % → ?); |
---|
[1669] | 325 | #lookup_assm cases lookup_assm |
---|
| 326 | [1: |
---|
[1910] | 327 | #None_lookup_opt_assm normalize nodelta #_ |
---|
[1669] | 328 | generalize in match recursive_assm; |
---|
[2573] | 329 | lapply (execute_1_and_program_counter_after_other_in_lockstep … classifier_assm) |
---|
[1910] | 330 | <FETCH normalize nodelta #rewrite_assm >rewrite_assm in None_lookup_opt_assm; |
---|
| 331 | #None_lookup_opt_assm <None_lookup_opt_assm |
---|
| 332 | normalize nodelta #new_recursive_assm |
---|
[2907] | 333 | cases(new_recursive_assm (execute_1 ? status_pre) status_end |
---|
[1929] | 334 | end_flag trace_any_label ? ?) try (>rewrite_assm %) |
---|
[1910] | 335 | whd in match (current_instruction_cost … status_pre); |
---|
[2999] | 336 | cut(ticks = \snd (fetch (cm prog) (program_counter … status_pre))) |
---|
[1929] | 337 | [1,3: |
---|
[1910] | 338 | <FETCH % |
---|
[1669] | 339 | |2: |
---|
[1912] | 340 | #ticks_refl_assm |
---|
| 341 | >ticks_refl_assm % |
---|
[1910] | 342 | |4: |
---|
| 343 | #ticks_refl_assm |
---|
[1912] | 344 | change with (S ? ≤ S ?) in size_invariant; |
---|
| 345 | lapply (le_S_S_to_le … size_invariant) #assm |
---|
| 346 | assumption |
---|
[1669] | 347 | ] |
---|
| 348 | |2: |
---|
[1927] | 349 | #costlabel #Some_lookup_opt_assm <Some_lookup_opt_assm |
---|
| 350 | #absurd |
---|
| 351 | cases (not_Some_neq_None_to_False ?? absurd) |
---|
[1669] | 352 | ] |
---|
| 353 | |1: |
---|
| 354 | #status_start #status_final #execute_assm #classifier_assm #costed_assm |
---|
| 355 | #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl |
---|
| 356 | destruct |
---|
| 357 | whd in match (trace_any_label_length … (tal_base_not_return …)); |
---|
| 358 | whd in match (compute_paid_trace_any_label … (tal_base_not_return …)); |
---|
| 359 | whd in costed_assm; |
---|
| 360 | generalize in match costed_assm; |
---|
[2907] | 361 | generalize in match (refl … (lookup_opt … (program_counter … (execute_1 … status_start)) ?)); |
---|
[1927] | 362 | whd in match (as_label ??); |
---|
[2907] | 363 | generalize in match (lookup_opt … (program_counter … (execute_1 … status_start)) (costlabels prog)) |
---|
[1927] | 364 | in ⊢ (??%? → % → ?); |
---|
[1669] | 365 | #lookup_assm cases lookup_assm |
---|
| 366 | [1: |
---|
[1927] | 367 | #None_lookup_opt_assm |
---|
| 368 | #absurd @⊥ cases absurd -absurd #absurd @absurd % |
---|
[1669] | 369 | |2: |
---|
| 370 | #costlabel #Some_lookup_opt_assm normalize nodelta #ignore |
---|
| 371 | generalize in match recursive_assm; |
---|
[2593] | 372 | cases classifier_assm -classifier_assm #classifier_assm |
---|
[2575] | 373 | [2: |
---|
| 374 | lapply (execute_1_and_program_counter_after_other_in_lockstep … classifier_assm) |
---|
| 375 | <FETCH normalize nodelta #rewrite_assm >rewrite_assm in Some_lookup_opt_assm; |
---|
| 376 | #Some_lookup_opt_assm <Some_lookup_opt_assm |
---|
| 377 | normalize nodelta #new_recursive_assm >new_recursive_assm |
---|
[2999] | 378 | cut(ticks = \snd (fetch (cm prog) (program_counter … status_start))) |
---|
[2575] | 379 | [1: |
---|
| 380 | <FETCH % |
---|
| 381 | |2: |
---|
| 382 | #ticks_refl_assm >ticks_refl_assm |
---|
| 383 | <plus_n_O % |
---|
| 384 | ] |
---|
[2593] | 385 | |1: |
---|
[2899] | 386 | (* JHM: wicked failure because Some prevent previous unfolding of OC_classify here *) |
---|
[2593] | 387 | @⊥ |
---|
| 388 | (* *** (* previously: unnecessary case analysis on instruction *) |
---|
| 389 | change with ((Some ? (ASM_classify0 ?) = ?) → ?); |
---|
[1910] | 390 | whd in match (current_instruction code_memory' status_start); |
---|
| 391 | <FETCH generalize in match classify_assm; |
---|
| 392 | cases instruction |
---|
| 393 | [8: |
---|
| 394 | #preinstruction normalize nodelta |
---|
| 395 | whd in match ASM_classify0; normalize nodelta |
---|
| 396 | #contradiction >contradiction #absurd destruct(absurd) |
---|
[1710] | 397 | ] |
---|
[1910] | 398 | try(#addr1 #addr2 normalize nodelta #ignore #absurd destruct(absurd)) |
---|
| 399 | try(#addr normalize nodelta #ignore #absurd destruct(absurd)) |
---|
| 400 | normalize in ignore; destruct(ignore) |
---|
[2593] | 401 | *** *) |
---|
[2575] | 402 | ] |
---|
| 403 | ] |
---|
| 404 | ] |
---|
[2760] | 405 | change with (ASM_classify0 ? = ?) in classifier_assm; |
---|
[2575] | 406 | whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm; |
---|
| 407 | whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm; |
---|
| 408 | <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd) |
---|
[1910] | 409 | qed. |
---|
[1669] | 410 | |
---|
[1684] | 411 | lemma trace_compute_paid_trace_cl_jump: |
---|
[2907] | 412 | ∀prog: labelled_object_code. |
---|
[1684] | 413 | ∀program_counter': Word. |
---|
| 414 | ∀first_time_around: bool. |
---|
| 415 | ∀program_size': ℕ. |
---|
| 416 | ∀ticks: ℕ. |
---|
| 417 | ∀instruction: instruction. |
---|
| 418 | ∀program_counter'': Word. |
---|
[2999] | 419 | ∀FETCH: 〈instruction,program_counter'',ticks〉 = fetch (cm prog) program_counter'. |
---|
| 420 | ∀start_status: (Status (cm prog)). |
---|
| 421 | ∀final_status: (Status (cm prog)). |
---|
[1684] | 422 | ∀trace_ends_flag: trace_ends_with_ret. |
---|
[2907] | 423 | ∀the_trace: (trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status). |
---|
[2573] | 424 | ∀program_counter_refl: (program_counter' = program_counter … start_status). |
---|
[1684] | 425 | ∀classify_assm: ASM_classify0 instruction = cl_jump. |
---|
[1906] | 426 | ticks |
---|
[2575] | 427 | =compute_paid_trace_any_label … the_trace. |
---|
[2999] | 428 | #prog #program_counter' #first_time_around |
---|
[1912] | 429 | #program_size' #ticks #instruction #program_counter'' #FETCH |
---|
[1691] | 430 | #start_status #final_status |
---|
[1684] | 431 | #trace_ends_flag #the_trace #program_counter_refl #classify_assm |
---|
| 432 | @(trace_any_label_inv_ind … the_trace) |
---|
[2573] | 433 | [6: |
---|
[1692] | 434 | #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label |
---|
| 435 | #classifier_assm #costed_assm #trace_ends_refl #start_status_refl #final_status_refl |
---|
| 436 | #the_trace_refl destruct @⊥ |
---|
| 437 | |1: |
---|
| 438 | #status_start #status_final #execute_assm #classifier_assm #costed_assm |
---|
[1684] | 439 | #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl |
---|
| 440 | destruct |
---|
| 441 | whd in match (trace_any_label_length … (tal_base_not_return …)); |
---|
[1906] | 442 | whd in match (compute_paid_trace_any_label … (tal_base_not_return …)); |
---|
| 443 | <FETCH % |
---|
[1684] | 444 | |2: |
---|
[1692] | 445 | #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm |
---|
| 446 | #start_status_refl #final_status_refl #the_trace_assm destruct @⊥ |
---|
[1684] | 447 | |3: |
---|
| 448 | #status_pre_fun_call #status_start_fun_call #status_final #execute_assm |
---|
| 449 | #classifier_assm #after_return_assm #trace_label_return #costed_assm |
---|
[1692] | 450 | #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl |
---|
[1684] | 451 | destruct @⊥ |
---|
[2656] | 452 | |4: |
---|
| 453 | #status_pre_fun_call #status_start_fun_call #status_final #execute_assm |
---|
| 454 | #classifier_assm #trace_label_return |
---|
| 455 | #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl |
---|
| 456 | destruct @⊥ |
---|
[2573] | 457 | |5: |
---|
[1684] | 458 | #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call |
---|
| 459 | #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return |
---|
[1692] | 460 | #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl |
---|
[1684] | 461 | #final_status_refl #the_trace_refl destruct @⊥ |
---|
| 462 | ] |
---|
[2760] | 463 | change with (ASM_classify0 ? = ?) in classifier_assm; |
---|
[1684] | 464 | whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm; |
---|
| 465 | whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm; |
---|
| 466 | <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd) |
---|
| 467 | qed. |
---|
| 468 | |
---|
| 469 | lemma trace_compute_paid_trace_cl_call: |
---|
[2907] | 470 | ∀prog: labelled_object_code. |
---|
[1684] | 471 | ∀program_counter' : Word. |
---|
| 472 | ∀program_size' : ℕ. |
---|
| 473 | ∀ticks : ℕ. |
---|
| 474 | ∀instruction : instruction. |
---|
| 475 | ∀program_counter'' : Word. |
---|
[2999] | 476 | ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch (cm prog) program_counter'). |
---|
| 477 | ∀start_status : (Status (cm prog)). |
---|
| 478 | ∀final_status : (Status (cm prog)). |
---|
[1684] | 479 | ∀trace_ends_flag : trace_ends_with_ret. |
---|
[2907] | 480 | ∀the_trace : trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status. |
---|
[2573] | 481 | ∀program_counter_refl : (program_counter' = program_counter … start_status). |
---|
[2575] | 482 | ∀size_invariant : trace_any_label_length … the_trace ≤S program_size'. |
---|
[1684] | 483 | ∀classify_assm: ASM_classify0 instruction = cl_call. |
---|
[1692] | 484 | (∀pi1:ℕ |
---|
[2907] | 485 | .if match lookup_opt costlabel 16 program_counter'' (costlabels prog) with |
---|
[1692] | 486 | [None ⇒ true | Some _ ⇒ false] |
---|
[2999] | 487 | then (∀start_status0:Status (cm prog) |
---|
| 488 | .∀final_status0:Status (cm prog) |
---|
[1684] | 489 | .∀trace_ends_flag0:trace_ends_with_ret |
---|
| 490 | .∀the_trace0:trace_any_label |
---|
[2907] | 491 | (OC_abstract_status prog) |
---|
[1912] | 492 | trace_ends_flag0 start_status0 final_status0. |
---|
[2575] | 493 | trace_any_label_length … the_trace0 |
---|
[1912] | 494 | ≤ program_size' → |
---|
| 495 | program_counter'' |
---|
[2573] | 496 | =program_counter … start_status0 |
---|
[1906] | 497 | → pi1 |
---|
[2575] | 498 | =compute_paid_trace_any_label … the_trace0) |
---|
[1684] | 499 | else (pi1=O) |
---|
[1906] | 500 | → ticks+pi1 |
---|
[2575] | 501 | =compute_paid_trace_any_label … the_trace). |
---|
[2999] | 502 | #prog #program_counter' #program_size' |
---|
[1912] | 503 | #ticks #instruction #program_counter'' #FETCH |
---|
[1691] | 504 | #start_status #final_status #trace_ends_flag |
---|
[1912] | 505 | #the_trace #program_counter_refl #size_invariant #classify_assm |
---|
| 506 | #recursive_block_cost #recursive_assm |
---|
[1684] | 507 | @(trace_any_label_inv_ind … the_trace) |
---|
[2573] | 508 | [6: |
---|
[1692] | 509 | #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label |
---|
| 510 | #classifier_assm #costed_assm #trace_ends_refl #start_status_refl #final_status_refl |
---|
| 511 | #the_trace_refl destruct @⊥ |
---|
| 512 | |1: |
---|
| 513 | #status_start #status_final #execute_assm #classifier_assm #costed_assm |
---|
| 514 | #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl |
---|
| 515 | destruct @⊥ |
---|
| 516 | |2: |
---|
| 517 | #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm |
---|
| 518 | #start_status_refl #final_status_refl #the_trace_assm destruct @⊥ |
---|
| 519 | |3: |
---|
| 520 | #status_pre_fun_call #status_start_fun_call #status_final #execute_assm |
---|
| 521 | #classifier_assm #after_return_assm #trace_label_return #costed_assm |
---|
[1902] | 522 | #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl |
---|
[1692] | 523 | destruct |
---|
| 524 | whd in match (trace_any_label_length … (tal_base_call …)); |
---|
| 525 | whd in match (compute_paid_trace_any_label … (tal_base_call …)); |
---|
| 526 | whd in costed_assm; |
---|
| 527 | generalize in match costed_assm; |
---|
[2907] | 528 | generalize in match (refl … (lookup_opt … (program_counter … status_final) (costlabels prog))); |
---|
[1927] | 529 | whd in match (as_label ??); |
---|
[2907] | 530 | generalize in match (lookup_opt … (program_counter … status_final) ?) |
---|
[1927] | 531 | in ⊢ (??%? → % → ?); |
---|
[1692] | 532 | #lookup_assm cases lookup_assm |
---|
| 533 | [1: |
---|
| 534 | #None_lookup_opt normalize nodelta #absurd cases absurd |
---|
[1927] | 535 | -absurd #absurd @⊥ @absurd % |
---|
[1692] | 536 | |2: |
---|
| 537 | #costlabel #Some_lookup_opt normalize nodelta #ignore |
---|
| 538 | generalize in match recursive_assm; |
---|
[2573] | 539 | cut(program_counter'' = (program_counter … status_final)) |
---|
[1692] | 540 | [1: |
---|
[1902] | 541 | generalize in match after_return_assm; |
---|
[1901] | 542 | whd in ⊢ (% → ?); <FETCH normalize nodelta #relevant <relevant % |
---|
[1692] | 543 | |2: |
---|
| 544 | #program_counter_assm >program_counter_assm <Some_lookup_opt |
---|
[1906] | 545 | normalize nodelta #new_recursive_assm >new_recursive_assm |
---|
[2999] | 546 | cut(ticks = \snd (fetch (cm prog) (program_counter … status_pre_fun_call))) |
---|
[1906] | 547 | [1: |
---|
| 548 | <FETCH % |
---|
[1692] | 549 | |2: |
---|
[1906] | 550 | #ticks_refl_assm >ticks_refl_assm |
---|
| 551 | <plus_n_O % |
---|
[1692] | 552 | ] |
---|
| 553 | ] |
---|
| 554 | ] |
---|
[2656] | 555 | |4: |
---|
| 556 | #status_pre_fun_call #status_start_fun_call #status_final #execute_assm |
---|
| 557 | #classifier_assm #trace_label_return |
---|
| 558 | #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl |
---|
| 559 | destruct @⊥ |
---|
[2573] | 560 | |5: |
---|
[1692] | 561 | #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call |
---|
| 562 | #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return |
---|
[1902] | 563 | #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl |
---|
| 564 | #final_status_refl #the_trace_refl |
---|
[1901] | 565 | generalize in match execute_assm; destruct #execute_assm |
---|
[1692] | 566 | whd in match (trace_any_label_length … (tal_step_call …)); |
---|
| 567 | whd in match (compute_paid_trace_any_label … (tal_step_call …)); |
---|
| 568 | whd in costed_assm:(?%); |
---|
| 569 | generalize in match costed_assm; |
---|
[2907] | 570 | generalize in match (refl … (lookup_opt … (program_counter … status_after_fun_call) (costlabels ?))); |
---|
[1927] | 571 | whd in match (as_label ??); |
---|
[2907] | 572 | generalize in match (lookup_opt … (program_counter … status_after_fun_call) (costlabels prog)) |
---|
[1927] | 573 | in ⊢ (??%? → % → ?); |
---|
[1692] | 574 | #lookup_assm cases lookup_assm |
---|
| 575 | [1: |
---|
| 576 | #None_lookup_opt_assm normalize nodelta #ignore |
---|
| 577 | generalize in match recursive_assm; |
---|
| 578 | cut(program_counter'' = program_counter … status_after_fun_call) |
---|
| 579 | [1: |
---|
[1902] | 580 | generalize in match after_return_assm; |
---|
[1901] | 581 | whd in ⊢ (% → ?); <FETCH normalize nodelta #relevant >relevant % |
---|
[1692] | 582 | |2: |
---|
| 583 | #program_counter_refl >program_counter_refl <None_lookup_opt_assm |
---|
[1906] | 584 | normalize nodelta #new_recursive_assm |
---|
[1912] | 585 | cases (new_recursive_assm … trace_any_label ? ?) |
---|
[1906] | 586 | [1: |
---|
| 587 | @plus_right_monotone whd in ⊢ (???%); <FETCH % |
---|
| 588 | |2: |
---|
[1919] | 589 | @le_S_S_to_le @size_invariant |
---|
[1912] | 590 | |3: |
---|
[1692] | 591 | % |
---|
| 592 | ] |
---|
| 593 | ] |
---|
| 594 | |2: |
---|
[1927] | 595 | #cost_label #Some_lookup_opt_assm #absurd |
---|
| 596 | cases (not_Some_neq_None_to_False ?? absurd) |
---|
[1692] | 597 | ] |
---|
| 598 | ] |
---|
[2760] | 599 | try (change with (ASM_classify0 ? = ? ∨ ASM_classify0 ? = ?) in classifier_assm;) |
---|
| 600 | try (change with (ASM_classify0 ? = ?) in classifier_assm;) |
---|
[1692] | 601 | whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm; |
---|
| 602 | whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm; |
---|
| 603 | <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd) cases absurd |
---|
| 604 | #absurd destruct(absurd) |
---|
[1684] | 605 | qed. |
---|
| 606 | |
---|
[1710] | 607 | lemma trace_compute_paid_trace_cl_return: |
---|
[2907] | 608 | ∀prog: labelled_object_code. |
---|
[1710] | 609 | ∀program_counter' : Word. |
---|
| 610 | ∀program_size' : ℕ. |
---|
| 611 | ∀ticks : ℕ. |
---|
| 612 | ∀instruction : instruction. |
---|
| 613 | ∀program_counter'' : Word. |
---|
[2999] | 614 | ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch (cm prog) program_counter'). |
---|
| 615 | ∀start_status : (Status (cm prog)). |
---|
| 616 | ∀final_status : (Status (cm prog)). |
---|
[1710] | 617 | ∀trace_ends_flag : trace_ends_with_ret. |
---|
[2907] | 618 | ∀the_trace : trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status. |
---|
[2573] | 619 | ∀program_counter_refl : (program_counter' = program_counter … start_status). |
---|
[1710] | 620 | ∀classify_assm: ASM_classify0 instruction = cl_return. |
---|
[1906] | 621 | ticks |
---|
[2575] | 622 | =compute_paid_trace_any_label … the_trace. |
---|
[2999] | 623 | #prog #program_counter' #program_size' |
---|
[1912] | 624 | #ticks #instruction #program_counter'' #FETCH |
---|
[1710] | 625 | #start_status #final_status #trace_ends_flag |
---|
| 626 | #the_trace #program_counter_refl #classify_assm |
---|
| 627 | @(trace_any_label_inv_ind … the_trace) |
---|
| 628 | [1: |
---|
| 629 | #start_status' #final_status' #execute_assm #classifier_assm #costed_assm |
---|
| 630 | #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl |
---|
| 631 | destruct @⊥ |
---|
| 632 | |2: |
---|
| 633 | #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_flag_refl |
---|
| 634 | #start_status_refl #final_status_refl #the_trace_refl destruct |
---|
| 635 | whd in match (trace_any_label_length … (tal_base_return …)); |
---|
[1906] | 636 | whd in match (compute_paid_trace_any_label … (tal_base_return …)); |
---|
| 637 | <FETCH % |
---|
[1710] | 638 | |3: |
---|
| 639 | #status_pre_fun_call #status_start_fun_call #status_final #execute_assm |
---|
| 640 | #classifier_assm #after_return_assm #trace_label_return #costed_assm |
---|
| 641 | #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl |
---|
| 642 | destruct @⊥ |
---|
[2664] | 643 | |4: |
---|
| 644 | #status_pre_fun_call #status_start_fun_call #status_final #execute_assm |
---|
| 645 | #classifier_assm |
---|
[2676] | 646 | destruct @⊥ |
---|
[2760] | 647 | change with (ASM_classify0 ? = ?) in classifier_assm; |
---|
[2679] | 648 | cases (current_instruction ??) in classifier_assm; |
---|
[2710] | 649 | [7: #preinstruction cases preinstruction ] |
---|
[2760] | 650 | try(#addr1 #addr2 #absurd normalize in absurd; destruct(absurd)) |
---|
| 651 | try(#addr #absurd normalize in absurd; destruct(absurd)) |
---|
| 652 | #absurd normalize in absurd; destruct(absurd) |
---|
[2573] | 653 | |5: |
---|
[1710] | 654 | #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call |
---|
| 655 | #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return |
---|
| 656 | #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl |
---|
| 657 | #final_status_refl #the_trace_refl |
---|
| 658 | destruct @⊥ |
---|
[2573] | 659 | |6: |
---|
[1710] | 660 | #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label |
---|
| 661 | #classifier_assm #costed_assm #trace_ends_flag_refl #start_status_refl |
---|
| 662 | #final_status_refl #the_trace_refl destruct @⊥ |
---|
| 663 | ] |
---|
[2760] | 664 | try (change with (ASM_classify0 ? = ? ∨ ASM_classify0 ? = ?) in classifier_assm;) |
---|
| 665 | try (change with (ASM_classify0 ? = ?) in classifier_assm;) |
---|
[1710] | 666 | whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm; |
---|
| 667 | whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm; |
---|
| 668 | <FETCH in classifier_assm; >classify_assm |
---|
| 669 | #absurd try (destruct(absurd)) |
---|
| 670 | cases absurd |
---|
| 671 | #absurd destruct(absurd) |
---|
| 672 | qed. |
---|
[1912] | 673 | |
---|
| 674 | lemma trace_any_label_length_leq_0_to_False: |
---|
[2907] | 675 | ∀prog: labelled_object_code. |
---|
[1912] | 676 | ∀trace_ends_flag: trace_ends_with_ret. |
---|
[2999] | 677 | ∀start_status: Status (cm prog). |
---|
| 678 | ∀final_status: Status (cm prog). |
---|
[2907] | 679 | ∀the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status. |
---|
[2575] | 680 | trace_any_label_length … the_trace ≤ 0 → False. |
---|
[2907] | 681 | #prog #trace_ends_flag #start_status #final_status #the_trace |
---|
| 682 | cases the_trace /2 by absurd/ |
---|
[1912] | 683 | qed. |
---|
[1710] | 684 | |
---|
[1650] | 685 | let rec block_cost' |
---|
[2907] | 686 | (prog: labelled_object_code) (program_counter': Word) |
---|
| 687 | (program_size: nat) |
---|
[1929] | 688 | (first_time_around: bool) |
---|
| 689 | on program_size: |
---|
[1658] | 690 | Σcost_of_block: nat. |
---|
[2907] | 691 | if (match lookup_opt … program_counter' (costlabels prog) with [ None ⇒ true | _ ⇒ first_time_around ]) then |
---|
[2999] | 692 | ∀start_status,final_status: Status (cm prog). |
---|
[1658] | 693 | ∀trace_ends_flag. |
---|
[2907] | 694 | ∀the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status. |
---|
[1929] | 695 | trace_any_label_length … the_trace ≤ program_size → |
---|
[1669] | 696 | program_counter' = program_counter … start_status → |
---|
[2575] | 697 | cost_of_block = compute_paid_trace_any_label … the_trace |
---|
[1669] | 698 | else |
---|
| 699 | (cost_of_block = 0) ≝ |
---|
[1911] | 700 | match program_size return λx. x = program_size → ? with |
---|
| 701 | [ O ⇒ λbase_case. 0 (* XXX: dummy to be inserted here *) |
---|
| 702 | | S program_size' ⇒ λstep_case. |
---|
[2999] | 703 | let 〈instruction, program_counter'', ticks〉 as FETCH ≝ fetch (cm prog) program_counter' in |
---|
[1650] | 704 | let to_continue ≝ |
---|
[2907] | 705 | match lookup_opt … program_counter' (costlabels prog) with |
---|
[1650] | 706 | [ None ⇒ true |
---|
| 707 | | Some _ ⇒ first_time_around |
---|
| 708 | ] |
---|
| 709 | in |
---|
[1669] | 710 | ((if to_continue then |
---|
| 711 | pi1 … (match instruction return λx. x = instruction → ? with |
---|
[1663] | 712 | [ RealInstruction real_instruction ⇒ λreal_instruction_refl. |
---|
| 713 | match real_instruction return λx. x = real_instruction → |
---|
| 714 | Σcost_of_block: nat. |
---|
[2999] | 715 | ∀start_status,final_status: Status (cm prog). |
---|
[1663] | 716 | ∀trace_ends_flag. |
---|
[2907] | 717 | ∀the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status. |
---|
[1929] | 718 | trace_any_label_length … the_trace ≤ S program_size' → |
---|
[1669] | 719 | program_counter' = program_counter … start_status → |
---|
[2575] | 720 | cost_of_block = compute_paid_trace_any_label … the_trace with |
---|
[1663] | 721 | [ RET ⇒ λinstr. ticks |
---|
[1710] | 722 | | RETI ⇒ λinstr. ticks |
---|
[1663] | 723 | | JC relative ⇒ λinstr. ticks |
---|
| 724 | | JNC relative ⇒ λinstr. ticks |
---|
| 725 | | JB bit_addr relative ⇒ λinstr. ticks |
---|
| 726 | | JNB bit_addr relative ⇒ λinstr. ticks |
---|
| 727 | | JBC bit_addr relative ⇒ λinstr. ticks |
---|
| 728 | | JZ relative ⇒ λinstr. ticks |
---|
| 729 | | JNZ relative ⇒ λinstr. ticks |
---|
| 730 | | CJNE src_trgt relative ⇒ λinstr. ticks |
---|
| 731 | | DJNZ src_trgt relative ⇒ λinstr. ticks |
---|
[2710] | 732 | | JMP addr ⇒ λinstr. (* XXX: actually a call due to use with fptrs *) |
---|
[2907] | 733 | ticks + block_cost' prog program_counter'' program_size' false |
---|
[1663] | 734 | | _ ⇒ λinstr. |
---|
[2907] | 735 | ticks + block_cost' prog program_counter'' program_size' false |
---|
[1663] | 736 | ] (refl …) |
---|
| 737 | | ACALL addr ⇒ λinstr. |
---|
[2907] | 738 | ticks + block_cost' prog program_counter'' program_size' false |
---|
[1909] | 739 | | AJMP addr ⇒ λinstr. |
---|
[1910] | 740 | let jump_target ≝ compute_target_of_unconditional_jump program_counter'' instruction in |
---|
[2907] | 741 | ticks + block_cost' prog jump_target program_size' false |
---|
[1663] | 742 | | LCALL addr ⇒ λinstr. |
---|
[2907] | 743 | ticks + block_cost' prog program_counter'' program_size' false |
---|
[1910] | 744 | | LJMP addr ⇒ λinstr. |
---|
| 745 | let jump_target ≝ compute_target_of_unconditional_jump program_counter'' instruction in |
---|
[2907] | 746 | ticks + block_cost' prog jump_target program_size' false |
---|
[1910] | 747 | | SJMP addr ⇒ λinstr. |
---|
| 748 | let jump_target ≝ compute_target_of_unconditional_jump program_counter'' instruction in |
---|
[2907] | 749 | ticks + block_cost' prog jump_target program_size' false |
---|
[1663] | 750 | | MOVC src trgt ⇒ λinstr. |
---|
[2907] | 751 | ticks + block_cost' prog program_counter'' program_size' false |
---|
[1669] | 752 | ] (refl …)) |
---|
[1650] | 753 | else |
---|
[1669] | 754 | 0) |
---|
| 755 | : Σcost_of_block: nat. |
---|
[2907] | 756 | match (match lookup_opt … program_counter' (costlabels prog) with [ None ⇒ true | _ ⇒ first_time_around ]) with |
---|
[1669] | 757 | [ true ⇒ |
---|
[2999] | 758 | ∀start_status: Status (cm prog). |
---|
| 759 | ∀final_status: Status (cm prog). |
---|
[1669] | 760 | ∀trace_ends_flag. |
---|
[2907] | 761 | ∀the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status. |
---|
[1929] | 762 | trace_any_label_length … the_trace ≤ S program_size' → |
---|
[1669] | 763 | program_counter' = program_counter … start_status → |
---|
[2575] | 764 | cost_of_block = compute_paid_trace_any_label … the_trace |
---|
[1669] | 765 | | false ⇒ |
---|
| 766 | (cost_of_block = 0) |
---|
| 767 | ]) |
---|
[1911] | 768 | ] (refl …). |
---|
[1910] | 769 | [2: |
---|
| 770 | change with (if to_continue then ? else (? = 0)) |
---|
| 771 | >p in ⊢ (match % return ? with [ _ ⇒ ? | _ ⇒ ? ]); normalize nodelta |
---|
| 772 | @pi2 |
---|
| 773 | |1: |
---|
[1911] | 774 | destruct |
---|
[1912] | 775 | cases (lookup_opt ????) normalize nodelta |
---|
[1911] | 776 | [1: |
---|
[1912] | 777 | #start_status #final_status #trace_ends_flag #the_trace |
---|
| 778 | #absurd |
---|
| 779 | cases (trace_any_label_length_leq_0_to_False … absurd) |
---|
[1911] | 780 | |2: |
---|
[1912] | 781 | #cost cases first_time_around normalize nodelta try % |
---|
| 782 | #start_status #final_status #trace_ends_flag #the_trace #absurd |
---|
| 783 | cases (trace_any_label_length_leq_0_to_False … absurd) |
---|
[1911] | 784 | ] |
---|
[1669] | 785 | |3: |
---|
[1684] | 786 | change with (if to_continue then ? else (0 = 0)) |
---|
| 787 | >p normalize nodelta % |
---|
[2710] | 788 | |6,7: |
---|
[1912] | 789 | #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl |
---|
[1929] | 790 | @(trace_compute_paid_trace_cl_return … program_size' … FETCH … the_trace program_counter_refl) |
---|
[1710] | 791 | destruct % |
---|
[2710] | 792 | |4,46,47: |
---|
[1912] | 793 | #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl |
---|
[2907] | 794 | cases(block_cost' ???) -block_cost' |
---|
[1929] | 795 | @(trace_compute_paid_trace_cl_call … program_size' … FETCH … the_trace program_counter_refl size_invariant) |
---|
[1691] | 796 | destruct % |
---|
[1929] | 797 | |43,44,45: (* XXX: unconditional jumps *) |
---|
[1912] | 798 | #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl |
---|
[2907] | 799 | cases (block_cost' ???) -block_cost' |
---|
[1929] | 800 | lapply (trace_compute_paid_trace_cl_other … program_size' … FETCH … the_trace program_counter_refl size_invariant) |
---|
| 801 | whd in match (program_counter_after_other ??); normalize nodelta destruct |
---|
| 802 | whd in match (is_unconditional_jump ?); normalize nodelta #assm @assm % |
---|
[2710] | 803 | |25,26,27,28,29,30,31,32,33: |
---|
[2907] | 804 | #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl |
---|
| 805 | @(trace_compute_paid_trace_cl_jump prog … first_time_around program_size' … FETCH … the_trace program_counter_refl) |
---|
| 806 | destruct % |
---|
[2710] | 807 | |4,33: |
---|
[1929] | 808 | |*: |
---|
[1912] | 809 | #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl |
---|
[2907] | 810 | cases(block_cost' ???) -block_cost' |
---|
[1929] | 811 | lapply (trace_compute_paid_trace_cl_other … program_size' … FETCH … the_trace program_counter_refl size_invariant) |
---|
| 812 | destruct #assm @assm % |
---|
[1910] | 813 | ] |
---|
[1642] | 814 | qed. |
---|
| 815 | |
---|
[1693] | 816 | definition block_cost: |
---|
[2907] | 817 | ∀prog: labelled_object_code. |
---|
[1693] | 818 | ∀program_counter': Word. |
---|
| 819 | Σcost_of_block: nat. |
---|
[2999] | 820 | ∀start_status: Status (cm prog). |
---|
| 821 | ∀final_status: Status (cm prog). |
---|
[1693] | 822 | ∀trace_ends_flag. |
---|
[2907] | 823 | ∀the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status. |
---|
[2573] | 824 | ∀unrepeating_witness: tal_unrepeating … the_trace. |
---|
[1693] | 825 | program_counter' = program_counter … start_status → |
---|
[2907] | 826 | cost_of_block = compute_paid_trace_any_label … the_trace. |
---|
| 827 | #prog #program_counter |
---|
| 828 | cases(block_cost' prog program_counter (2^16) true) |
---|
[1913] | 829 | #cost_of_block #block_cost_hyp |
---|
| 830 | %{cost_of_block} |
---|
[2907] | 831 | cases(lookup_opt … (costlabels prog)) in block_cost_hyp; |
---|
[1913] | 832 | [2: #cost_label] normalize nodelta |
---|
[1929] | 833 | #hyp #start_status #final_status #trace_ends_flag #the_trace #unrepeating_witness |
---|
[1921] | 834 | @hyp @tal_pc_list_length_leq_total_program_size try assumption |
---|
[2999] | 835 | qed. |
---|