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