source: src/ASM/ASMCosts.ma @ 1916

Last change on this file since 1916 was 1916, checked in by mulligan, 8 years ago

Closed remaining daemons in block_cost'. Rest of file now typechecks to end.

File size: 60.0 KB
Line 
1include "ASM/ASM.ma".
2include "ASM/Arithmetic.ma".
3include "ASM/Fetch.ma".
4include "ASM/Interpret.ma".
5include "common/StructuredTraces.ma".
6
7let rec fetch_program_counter_n
8  (n: nat) (code_memory: BitVectorTrie Byte 16) (program_counter: Word)
9    on n: option Word ≝
10  match n with
11  [ O ⇒ Some … program_counter
12  | S n ⇒
13    match fetch_program_counter_n n code_memory program_counter with
14    [ None ⇒ None …
15    | Some tail_pc ⇒
16      let 〈instr, program_counter, ticks〉 ≝ fetch code_memory tail_pc in
17        if ltb (nat_of_bitvector … tail_pc) (nat_of_bitvector … program_counter) then
18          Some … program_counter
19        else
20          None Word (* XXX: overflow! *)
21    ]
22  ].
23   
24definition reachable_program_counter: BitVectorTrie Byte 16 → nat → Word → Prop ≝
25  λcode_memory: BitVectorTrie Byte 16.
26  λprogram_size: nat.
27  λprogram_counter: Word.
28    (∃n: nat. Some … program_counter = fetch_program_counter_n n code_memory (zero 16)) ∧
29        nat_of_bitvector 16 program_counter < program_size.
30   
31definition well_labelling: BitVectorTrie costlabel 16 → Prop ≝
32  λcost_labels.
33    injective … (λx. lookup_opt … x cost_labels).
34   
35definition good_program: ∀code_memory: BitVectorTrie Byte 16. ∀total_program_size: nat. Prop ≝
36  λcode_memory: BitVectorTrie Byte 16.
37  λtotal_program_size: nat.
38  ∀program_counter: Word.
39  ∀good_program_counter_witness: reachable_program_counter code_memory total_program_size program_counter.
40  let 〈instruction, program_counter', ticks〉 ≝ fetch code_memory program_counter in
41    match instruction with
42    [ RealInstruction instr ⇒
43      match instr with
44      [ RET                    ⇒ True
45      | JC   relative          ⇒ True (* XXX: see below *)
46      | JNC  relative          ⇒ True (* XXX: see below *)
47      | JB   bit_addr relative ⇒ True
48      | JNB  bit_addr relative ⇒ True
49      | JBC  bit_addr relative ⇒ True
50      | JZ   relative          ⇒ True
51      | JNZ  relative          ⇒ True
52      | CJNE src_trgt relative ⇒ True
53      | DJNZ src_trgt relative ⇒ True
54      | _                      ⇒
55        nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧
56          nat_of_bitvector … program_counter' < total_program_size
57      ]
58    | LCALL addr         ⇒
59      match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Prop with
60      [ ADDR16 addr ⇒ λaddr16: True.
61          reachable_program_counter code_memory total_program_size addr ∧
62            nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧
63              nat_of_bitvector … program_counter' < total_program_size
64      | _ ⇒ λother: False. ⊥
65      ] (subaddressing_modein … addr)
66    | ACALL addr         ⇒
67      match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Prop with
68      [ ADDR11 addr ⇒ λaddr11: True.
69        let 〈pc_bu, pc_bl〉 ≝ split … 8 8 program_counter' in
70        let 〈thr, eig〉 ≝ split … 3 8 addr in
71        let 〈fiv, thr'〉 ≝ split … 5 3 pc_bu in
72        let new_program_counter ≝ (fiv @@ thr) @@ pc_bl in
73          reachable_program_counter code_memory total_program_size new_program_counter ∧
74            nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧
75              nat_of_bitvector … program_counter' < total_program_size
76      | _ ⇒ λother: False. ⊥
77      ] (subaddressing_modein … addr)
78    | AJMP  addr         ⇒
79      let jump_target ≝ compute_target_of_unconditional_jump program_counter' instruction in
80        reachable_program_counter code_memory total_program_size jump_target
81      (*match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Prop with
82      [ ADDR11 addr ⇒ λaddr11: True.
83        let 〈pc_bu, pc_bl〉 ≝ split … 8 8 program_counter' in
84        let 〈nu, nl〉 ≝ split … 4 4 pc_bu in
85        let bit ≝ get_index' … O ? nl in
86        let 〈relevant1, relevant2〉 ≝ split … 3 8 addr in
87        let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in
88        let 〈carry, new_program_counter〉 ≝ half_add 16 program_counter new_addr in
89          reachable_program_counter code_memory total_program_size new_program_counter
90      | _ ⇒ λother: False. ⊥
91      ] (subaddressing_modein … addr) *)
92    | LJMP  addr         ⇒
93      let jump_target ≝ compute_target_of_unconditional_jump program_counter' instruction in
94        reachable_program_counter code_memory total_program_size jump_target
95      (*match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Prop with
96      [ ADDR16 addr ⇒ λaddr16: True.
97          reachable_program_counter code_memory total_program_size addr
98      | _ ⇒ λother: False. ⊥
99      ] (subaddressing_modein … addr)*)
100    | SJMP  addr     ⇒
101      let jump_target ≝ compute_target_of_unconditional_jump program_counter' instruction in
102        reachable_program_counter code_memory total_program_size jump_target
103      (*match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → Prop with
104      [ RELATIVE addr ⇒ λrelative: True.
105        let 〈carry, new_program_counter〉 ≝ half_add … program_counter' (sign_extension addr) in
106          reachable_program_counter code_memory total_program_size new_program_counter
107      | _ ⇒ λother: False. ⊥
108      ] (subaddressing_modein … addr)*)
109    | JMP   addr     ⇒ (* XXX: JMP is used for fptrs and unconstrained *)
110      nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧
111        nat_of_bitvector … program_counter' < total_program_size
112    | MOVC  src trgt ⇒
113        nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧
114          nat_of_bitvector … program_counter' < total_program_size
115    ].
116  cases other
117qed.
118
119definition current_instruction_is_labelled ≝
120  λcode_memory.
121  λcost_labels: BitVectorTrie costlabel 16.
122  λs: Status code_memory.
123  let pc ≝ program_counter … code_memory s in
124    match lookup_opt … pc cost_labels with
125    [ None ⇒ False
126    | _    ⇒ True
127    ].
128
129definition next_instruction_properly_relates_program_counters ≝
130  λcode_memory.
131  λbefore: Status code_memory.
132  λafter : Status code_memory.
133    let program_counter_before ≝ program_counter ? code_memory before in
134    let 〈instruction, program_counter_after, ticks〉 ≝ fetch code_memory program_counter_before in
135      program_counter ? code_memory after = program_counter_after.
136(* XXX: why defined like this?
137  let size ≝ current_instruction_cost code_memory before in
138  let pc_before ≝ program_counter … code_memory before in
139  let pc_after ≝ program_counter … code_memory after in
140  let sum ≝ \snd (half_add … pc_before (bitvector_of_nat … size)) in
141    sum = pc_after.
142*)
143
144definition ASM_abstract_status: ∀code_memory. BitVectorTrie costlabel 16 → abstract_status ≝
145  λcode_memory.
146  λcost_labels.
147    mk_abstract_status
148      (Status code_memory)
149      (λs,s'. (execute_1 … s) = s')
150      (λs,class. ASM_classify … s = class)
151      (current_instruction_is_labelled … cost_labels)
152      (next_instruction_properly_relates_program_counters code_memory).
153
154let rec trace_any_label_length
155  (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
156    (trace_ends_flag: trace_ends_with_ret) (start_status: Status code_memory)
157      (final_status: Status code_memory)
158      (the_trace: trace_any_label (ASM_abstract_status code_memory cost_labels) trace_ends_flag start_status final_status)
159        on the_trace: nat ≝
160  match the_trace with
161  [ tal_base_not_return the_status _ _ _ _ ⇒ 0
162  | tal_base_call pre_fun_call start_fun_call final _ _ _ _ call_trace ⇒ 0
163  | tal_base_return the_status _ _ _ ⇒ 0
164  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final _ _ _ call_trace _ final_trace ⇒
165      let tail_length ≝ trace_any_label_length … final_trace in
166      let pc_difference ≝ nat_of_bitvector … (program_counter … after_fun_call) - nat_of_bitvector … (program_counter … pre_fun_call) in       
167        pc_difference + tail_length
168  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
169      let tail_length ≝ trace_any_label_length … tail_trace in
170      let pc_difference ≝ nat_of_bitvector … (program_counter … status_init) - nat_of_bitvector … (program_counter … status_pre) in
171        pc_difference + tail_length       
172  ].
173
174let rec trace_any_label_length'
175  (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
176    (trace_ends_flag: trace_ends_with_ret) (start_status: Status code_memory)
177      (final_status: Status code_memory)
178      (the_trace: trace_any_label (ASM_abstract_status code_memory cost_labels) trace_ends_flag start_status final_status)
179        on the_trace: nat ≝
180  match the_trace with
181  [ tal_base_not_return the_status _ _ _ _ ⇒ 1
182  | tal_base_call pre_fun_call start_fun_call final _ _ _ _ call_trace ⇒ 1
183  | tal_base_return the_status _ _ _ ⇒ 1
184  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final _ _ _ call_trace _ final_trace ⇒
185      let tail_length ≝ trace_any_label_length' … final_trace in
186        S tail_length
187  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
188      let tail_length ≝ trace_any_label_length' … tail_trace in
189        S tail_length       
190  ].
191
192let rec compute_paid_trace_any_label
193  (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
194    (trace_ends_flag: trace_ends_with_ret) (start_status: Status code_memory)
195      (final_status: Status code_memory)
196        (the_trace: trace_any_label (ASM_abstract_status code_memory cost_labels) trace_ends_flag start_status final_status)
197       on the_trace: nat ≝
198  match the_trace with
199  [ tal_base_not_return the_status _ _ _ _ ⇒ current_instruction_cost … the_status
200  | tal_base_return the_status _ _ _ ⇒ current_instruction_cost … the_status
201  | tal_base_call pre_fun_call start_fun_call final _ _ _ _ call_trace ⇒ current_instruction_cost … pre_fun_call
202  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
203     _ _ _ call_trace _ final_trace ⇒
204      let current_instruction_cost ≝ current_instruction_cost … pre_fun_call in
205      let final_trace_cost ≝ compute_paid_trace_any_label … cost_labels end_flag … final_trace in
206        current_instruction_cost + final_trace_cost
207  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
208      let current_instruction_cost ≝ current_instruction_cost … status_pre in
209      let tail_trace_cost ≝
210       compute_paid_trace_any_label … cost_labels end_flag
211        status_init status_end tail_trace
212      in
213        current_instruction_cost + tail_trace_cost
214  ].
215
216definition compute_paid_trace_label_label ≝
217  λcode_memory: BitVectorTrie Byte 16.
218  λcost_labels: BitVectorTrie costlabel 16.
219  λtrace_ends_flag: trace_ends_with_ret.
220  λstart_status: Status code_memory.
221  λfinal_status: Status code_memory.
222  λthe_trace: trace_label_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
223  match the_trace with
224  [ tll_base ends_flag initial final given_trace labelled_proof ⇒
225      compute_paid_trace_any_label … given_trace
226  ].
227
228include alias "arithmetics/nat.ma".
229include alias "basics/logic.ma".
230
231lemma plus_right_monotone:
232  ∀m, n, o: nat.
233    m = n → m + o = n + o.
234  #m #n #o #refl >refl %
235qed.
236
237lemma plus_left_monotone:
238  ∀m, n, o: nat.
239    m = n → o + m = o + n.
240  #m #n #o #refl destruct %
241qed.
242
243lemma minus_plus_cancel:
244  ∀m, n : nat.
245  ∀proof: n ≤ m.
246    (m - n) + n = m.
247  #m #n #proof /2 by plus_minus/
248qed.
249
250(* XXX: indexing bug *)
251lemma execute_1_and_program_counter_after_other_in_lockstep:
252  ∀code_memory: BitVectorTrie Byte 16.
253  ∀start_status: Status code_memory.
254    ASM_classify code_memory start_status = cl_other →
255      let 〈instruction, pc, ticks〉 ≝ fetch code_memory (program_counter … start_status) in
256        program_counter ? ? (execute_1 … start_status) =
257          program_counter_after_other pc instruction.
258  #code_memory #start_status #classify_assm
259  whd in match execute_1; normalize nodelta
260  cases (execute_1' code_memory start_status) #the_status
261  * #_ whd in classify_assm:(??%?); whd in match (current_instruction ??) in classify_assm;
262  cases (fetch ? ?) in classify_assm; * #instruction #pc #ticks
263  #classify_assm #classify_assm' @classify_assm' assumption
264qed-.
265
266lemma reachable_program_counter_to_0_lt_total_program_size:
267  ∀code_memory: BitVectorTrie Byte 16.
268  ∀program_counter: Word.
269  ∀total_program_size: nat.
270    reachable_program_counter code_memory total_program_size program_counter →
271      0 < total_program_size.
272  #code_memory #program_counter #total_program_size
273  whd in match reachable_program_counter; normalize nodelta * * #some_n
274  #_ cases (nat_of_bitvector 16 program_counter)
275  [1:
276    #assm assumption
277  |2:
278    #new_pc @ltn_to_ltO
279  ]
280qed.
281
282lemma trace_compute_paid_trace_cl_other:
283  ∀code_memory' : (BitVectorTrie Byte 16).
284  ∀program_counter' : Word.
285  ∀total_program_size : ℕ.
286  ∀cost_labels : (BitVectorTrie costlabel 16).
287  ∀reachable_program_counter_witness : (reachable_program_counter code_memory' total_program_size program_counter').
288  ∀good_program_witness : (good_program code_memory' total_program_size).
289  ∀program_size' : ℕ.
290  ∀ticks : ℕ.
291  ∀instruction : instruction.
292  ∀program_counter'' : Word.
293  ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch code_memory' program_counter').
294  let program_counter''' ≝ program_counter_after_other program_counter'' instruction in
295  ∀start_status : (Status code_memory').
296  ∀final_status : (Status code_memory').
297  ∀trace_ends_flag : trace_ends_with_ret.
298  ∀the_trace : (trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status).
299  ∀program_counter_refl : (program_counter' = program_counter (BitVectorTrie Byte 16) code_memory' start_status).
300  ∀size_invariant : trace_any_label_length' code_memory' cost_labels trace_ends_flag start_status final_status the_trace ≤S program_size'.
301  ∀classify_assm: ASM_classify0 instruction = cl_other.
302  ∀pi1 : ℕ.
303   (if match lookup_opt costlabel 16 program_counter''' cost_labels with 
304         [None ⇒ true
305         |Some _ ⇒ false
306         ] 
307    then
308      ∀start_status0:Status code_memory'.
309      ∀final_status0:Status code_memory'.
310      ∀trace_ends_flag0:trace_ends_with_ret.
311      ∀the_trace0:trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag0 start_status0 final_status0.
312        trace_any_label_length' code_memory' cost_labels trace_ends_flag0
313          start_status0 final_status0 the_trace0 ≤ program_size' →
314        program_counter''' = program_counter (BitVectorTrie Byte 16) code_memory' start_status0 →
315                  pi1
316                    =compute_paid_trace_any_label code_memory' cost_labels
317                     trace_ends_flag0 start_status0 final_status0 the_trace0
318    else (pi1=O) )
319   → ticks+pi1
320     =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag
321      start_status final_status the_trace.
322  #code_memory' #program_counter' #total_program_size #cost_labels
323  #reachable_program_counter_witness #good_program_witness
324  #program_size' #ticks #instruction #program_counter'' #FETCH
325  #start_status #final_status
326  #trace_ends_flag #the_trace #program_counter_refl #size_invariant #classify_assm #recursive_block_cost
327  #recursive_assm
328  @(trace_any_label_inv_ind … the_trace)
329    [5:
330      #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
331      #classifier_assm #costed_assm #trace_ends_refl #start_status_refl #final_status_refl
332      #the_trace_refl
333      destruct
334      whd in match (trace_any_label_length … (tal_step_default …));
335      whd in match (compute_paid_trace_any_label … (tal_step_default …));
336      whd in costed_assm:(?%);
337      generalize in match costed_assm;
338      generalize in match (refl … (lookup_opt … (program_counter … (execute_1 … status_pre)) cost_labels));
339      generalize in match (lookup_opt … (program_counter … (execute_1 … status_pre)) cost_labels)
340        in ⊢ (??%? → ?(match % with [ _ ⇒ ? | _ ⇒ ? ]) → ?);
341      #lookup_assm cases lookup_assm
342      [1:
343        #None_lookup_opt_assm normalize nodelta #_
344        generalize in match recursive_assm;
345        lapply (execute_1_and_program_counter_after_other_in_lockstep code_memory' ? classifier_assm)
346        <FETCH normalize nodelta #rewrite_assm >rewrite_assm in None_lookup_opt_assm;
347        #None_lookup_opt_assm <None_lookup_opt_assm
348        normalize nodelta #new_recursive_assm
349        cases(new_recursive_assm (execute_1 code_memory' status_pre) status_end
350          end_flag trace_any_label ? ?) try %
351        whd in match (current_instruction_cost … status_pre);
352        cut(ticks = \snd (fetch code_memory'
353           (program_counter (BitVectorTrie Byte 16) code_memory' status_pre)))
354        [1,3,5:
355          <FETCH %
356        |2:
357          #ticks_refl_assm
358          >ticks_refl_assm %
359        |4:
360          #ticks_refl_assm
361          change with (S ? ≤ S ?) in size_invariant;
362          lapply (le_S_S_to_le … size_invariant) #assm
363          assumption
364        |6:
365          #ticks_refl_assm
366          <rewrite_assm %
367        ]
368      |2:
369        #costlabel #Some_lookup_opt_assm <Some_lookup_opt_assm normalize nodelta
370        #absurd cases absurd #absurd cases(absurd I)
371      ]
372    |1:
373      #status_start #status_final #execute_assm #classifier_assm #costed_assm
374      #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
375      destruct
376      whd in match (trace_any_label_length … (tal_base_not_return …));
377      whd in match (compute_paid_trace_any_label … (tal_base_not_return …));
378      whd in costed_assm;
379      generalize in match costed_assm;
380      generalize in match (refl … (lookup_opt … (program_counter … (execute_1 … status_start)) cost_labels));
381      generalize in match (lookup_opt … (program_counter … (execute_1 code_memory' status_start)) cost_labels)
382        in ⊢ (??%? → (match % with [ _ ⇒ ? | _ ⇒ ? ]) → ?);
383      #lookup_assm cases lookup_assm
384      [1:
385        #None_lookup_opt_assm normalize nodelta >None_lookup_opt_assm
386        #absurd cases absurd
387      |2:
388        #costlabel #Some_lookup_opt_assm normalize nodelta #ignore
389        generalize in match recursive_assm;
390        cases classifier_assm
391        [1:
392          whd in ⊢ (% → ?);
393          whd in ⊢ (??%? → ?);
394          whd in match (current_instruction code_memory' status_start);
395          <FETCH generalize in match classify_assm;
396          cases instruction
397          [8:
398            #preinstruction normalize nodelta
399            whd in match ASM_classify0; normalize nodelta
400            #contradiction >contradiction #absurd destruct(absurd)
401          ]
402          try(#addr1 #addr2 normalize nodelta #ignore #absurd destruct(absurd))
403          try(#addr normalize nodelta #ignore #absurd destruct(absurd))
404          normalize in ignore; destruct(ignore)
405        |2:
406          -classifier_assm #classifier_assm
407          lapply (execute_1_and_program_counter_after_other_in_lockstep code_memory' ? classifier_assm)
408          <FETCH normalize nodelta #rewrite_assm >rewrite_assm in Some_lookup_opt_assm;
409          #Some_lookup_opt_assm <Some_lookup_opt_assm
410          normalize nodelta #new_recursive_assm >new_recursive_assm
411          cut(ticks = \snd (fetch code_memory'
412             (program_counter (BitVectorTrie Byte 16) code_memory' status_start)))
413          [1:
414            <FETCH %
415          |2:
416            #ticks_refl_assm >ticks_refl_assm
417            <plus_n_O %
418          ]
419        ]
420      ]
421    |2:
422      #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm
423      #start_status_refl #final_status_refl #the_trace_assm destruct @⊥
424    |3:
425      #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
426      #classifier_assm #after_return_assm #trace_label_return #costed_assm
427      #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
428      destruct @⊥
429    |4:
430      #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
431      #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
432      #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
433      #final_status_refl #the_trace_refl destruct @⊥
434    ]
435  change with (ASM_classify0 ? = ?) in classifier_assm;
436  whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
437  whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
438  <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd)
439qed.
440
441lemma trace_compute_paid_trace_cl_jump:
442  ∀code_memory': BitVectorTrie Byte 16.
443  ∀program_counter': Word.
444  ∀total_program_size: ℕ.
445  ∀cost_labels: BitVectorTrie costlabel 16.
446  ∀reachable_program_counter_witness: reachable_program_counter code_memory' total_program_size program_counter'.
447  ∀good_program_witness: good_program code_memory' total_program_size.
448  ∀first_time_around: bool.
449  ∀program_size': ℕ.
450  ∀ticks: ℕ.
451  ∀instruction: instruction.
452  ∀program_counter'': Word.
453  ∀FETCH: 〈instruction,program_counter'',ticks〉 = fetch code_memory' program_counter'.
454  ∀start_status: (Status code_memory').
455  ∀final_status: (Status code_memory').
456  ∀trace_ends_flag: trace_ends_with_ret.
457  ∀the_trace: (trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status).
458  ∀program_counter_refl: (program_counter' = program_counter (BitVectorTrie Byte 16) code_memory' start_status).
459  ∀classify_assm: ASM_classify0 instruction = cl_jump.
460    ticks
461     =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag
462      start_status final_status the_trace.
463  #code_memory' #program_counter' #total_program_size #cost_labels
464  #reachable_program_counter_witness #good_program_witness #first_time_around
465  #program_size' #ticks #instruction #program_counter'' #FETCH
466  #start_status #final_status
467  #trace_ends_flag #the_trace #program_counter_refl #classify_assm
468  @(trace_any_label_inv_ind … the_trace)
469  [5:
470    #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
471    #classifier_assm #costed_assm #trace_ends_refl #start_status_refl #final_status_refl
472    #the_trace_refl destruct @⊥
473  |1:
474    #status_start #status_final #execute_assm #classifier_assm #costed_assm
475    #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
476    destruct
477    whd in match (trace_any_label_length … (tal_base_not_return …));
478    whd in match (compute_paid_trace_any_label … (tal_base_not_return …));
479    <FETCH %
480  |2:
481    #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm
482    #start_status_refl #final_status_refl #the_trace_assm destruct @⊥
483  |3:
484    #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
485    #classifier_assm #after_return_assm #trace_label_return #costed_assm
486    #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
487    destruct @⊥
488  |4:
489    #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
490    #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
491    #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
492    #final_status_refl #the_trace_refl destruct @⊥
493  ]
494  change with (ASM_classify0 ? = ?) in classifier_assm;
495  whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
496  whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
497  <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd)
498qed.
499
500lemma trace_compute_paid_trace_cl_call:
501  ∀code_memory' : (BitVectorTrie Byte 16).
502  ∀program_counter' : Word.
503  ∀total_program_size : ℕ.
504  ∀cost_labels : (BitVectorTrie costlabel 16).
505  ∀reachable_program_counter_witness : (reachable_program_counter code_memory' total_program_size program_counter').
506  ∀good_program_witness : (good_program code_memory' total_program_size).
507  ∀program_size' : ℕ.
508  ∀ticks : ℕ.
509  ∀instruction : instruction.
510  ∀program_counter'' : Word.
511  ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch code_memory' program_counter').
512  ∀start_status : (Status code_memory').
513  ∀final_status : (Status code_memory').
514  ∀trace_ends_flag : trace_ends_with_ret.
515  ∀the_trace : (trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status).
516  ∀program_counter_refl : (program_counter' = program_counter (BitVectorTrie Byte 16) code_memory' start_status).
517  ∀size_invariant : trace_any_label_length' code_memory' cost_labels trace_ends_flag start_status final_status the_trace ≤S program_size'.
518  ∀classify_assm: ASM_classify0 instruction = cl_call.
519  (∀pi1:ℕ
520  .if match lookup_opt costlabel 16 program_counter'' cost_labels with 
521      [None ⇒ true | Some _ ⇒ false] 
522   then (∀start_status0:Status code_memory'
523             .∀final_status0:Status code_memory'
524              .∀trace_ends_flag0:trace_ends_with_ret
525               .∀the_trace0:trace_any_label
526                                        (ASM_abstract_status code_memory' cost_labels)
527                                        trace_ends_flag0 start_status0 final_status0.
528                trace_any_label_length' code_memory' cost_labels trace_ends_flag0
529                  start_status0 final_status0 the_trace0
530                   ≤ program_size' →
531                program_counter''
532                 =program_counter (BitVectorTrie Byte 16) code_memory' start_status0
533                 → pi1
534                   =compute_paid_trace_any_label code_memory' cost_labels
535                    trace_ends_flag0 start_status0 final_status0 the_trace0) 
536   else (pi1=O) 
537   → ticks+pi1
538     =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag
539      start_status final_status the_trace).
540  #code_memory' #program_counter' #total_program_size #cost_labels
541  #reachable_program_counter_witness #good_program_witness #program_size'
542  #ticks #instruction #program_counter'' #FETCH
543  #start_status #final_status #trace_ends_flag
544  #the_trace #program_counter_refl #size_invariant #classify_assm
545  #recursive_block_cost #recursive_assm
546  @(trace_any_label_inv_ind … the_trace)
547  [5:
548    #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
549    #classifier_assm #costed_assm #trace_ends_refl #start_status_refl #final_status_refl
550    #the_trace_refl destruct @⊥
551  |1:
552    #status_start #status_final #execute_assm #classifier_assm #costed_assm
553    #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
554    destruct @⊥
555  |2:
556    #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm
557    #start_status_refl #final_status_refl #the_trace_assm destruct @⊥
558  |3:
559    #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
560    #classifier_assm #after_return_assm #trace_label_return #costed_assm
561    #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
562    destruct
563    whd in match (trace_any_label_length … (tal_base_call …));
564    whd in match (compute_paid_trace_any_label … (tal_base_call …));
565    whd in costed_assm;
566    generalize in match costed_assm;
567    generalize in match (refl … (lookup_opt … (program_counter … status_final) cost_labels));
568    generalize in match (lookup_opt … (program_counter … status_final) cost_labels)
569      in ⊢ (??%? → (match % with [ _ ⇒ ? | _ ⇒ ? ]) → ?);
570    #lookup_assm cases lookup_assm
571    [1:
572      #None_lookup_opt normalize nodelta #absurd cases absurd
573    |2:
574      #costlabel #Some_lookup_opt normalize nodelta #ignore
575      generalize in match recursive_assm;
576      cut(program_counter'' = (program_counter (BitVectorTrie Byte 16) code_memory' status_final))
577      [1:
578        generalize in match after_return_assm;
579        whd in ⊢ (% → ?); <FETCH normalize nodelta #relevant <relevant %
580      |2:
581        #program_counter_assm >program_counter_assm <Some_lookup_opt
582        normalize nodelta #new_recursive_assm >new_recursive_assm
583        cut(ticks = \snd (fetch code_memory' (program_counter (BitVectorTrie Byte 16) code_memory' status_pre_fun_call)))
584        [1:
585          <FETCH %
586        |2:
587          #ticks_refl_assm >ticks_refl_assm
588          <plus_n_O %
589        ]
590      ]
591    ]
592  |4:
593    #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
594    #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
595    #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
596    #final_status_refl #the_trace_refl
597    generalize in match execute_assm; destruct #execute_assm
598    whd in match (trace_any_label_length … (tal_step_call …));
599    whd in match (compute_paid_trace_any_label … (tal_step_call …));
600    whd in costed_assm:(?%);
601    generalize in match costed_assm;
602    generalize in match (refl … (lookup_opt … (program_counter … status_after_fun_call) cost_labels));
603    generalize in match (lookup_opt … (program_counter … status_after_fun_call) cost_labels)
604      in ⊢ (??%? → ?(match % with [ _ ⇒ ? | _ ⇒ ? ]) → ?);
605    #lookup_assm cases lookup_assm
606    [1:
607      #None_lookup_opt_assm normalize nodelta #ignore
608      generalize in match recursive_assm;
609      cut(program_counter'' = program_counter … status_after_fun_call)
610      [1:
611        generalize in match after_return_assm;
612        whd in ⊢ (% → ?); <FETCH normalize nodelta #relevant >relevant %
613      |2:
614        #program_counter_refl >program_counter_refl <None_lookup_opt_assm
615        normalize nodelta #new_recursive_assm
616        cases (new_recursive_assm … trace_any_label ? ?)
617        [1:
618          @plus_right_monotone whd in ⊢ (???%); <FETCH %
619        |2:
620          normalize in size_invariant;
621          lapply (le_S_S_to_le … size_invariant)
622          #assm assumption
623        |3:
624          %
625        ]
626      ]
627    |2:
628      #cost_label #Some_lookup_opt_assm normalize nodelta #absurd
629      cases absurd #absurd cases (absurd I)
630    ]
631  ]
632  try (change with (ASM_classify0 ? = ? ∨ ASM_classify0 ? = ?) in classifier_assm;)
633  try (change with (ASM_classify0 ? = ?) in classifier_assm;)
634  whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
635  whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
636  <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd) cases absurd
637  #absurd destruct(absurd)
638qed.
639
640lemma trace_compute_paid_trace_cl_return:
641  ∀code_memory' : (BitVectorTrie Byte 16).
642  ∀program_counter' : Word.
643  ∀total_program_size : ℕ.
644  ∀cost_labels : (BitVectorTrie costlabel 16).
645  ∀reachable_program_counter_witness : (reachable_program_counter code_memory' total_program_size program_counter').
646  ∀good_program_witness : (good_program code_memory' total_program_size).
647  ∀program_size' : ℕ.
648  ∀ticks : ℕ.
649  ∀instruction : instruction.
650  ∀program_counter'' : Word.
651  ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch code_memory' program_counter').
652  ∀start_status : (Status code_memory').
653  ∀final_status : (Status code_memory').
654  ∀trace_ends_flag : trace_ends_with_ret.
655  ∀the_trace : (trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status).
656  ∀program_counter_refl : (program_counter' = program_counter (BitVectorTrie Byte 16) code_memory' start_status).
657  ∀classify_assm: ASM_classify0 instruction = cl_return.
658    ticks
659     =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag
660      start_status final_status the_trace.
661  #code_memory' #program_counter' #total_program_size #cost_labels
662  #reachable_program_counter_witness #good_program_witness #program_size'
663  #ticks #instruction #program_counter'' #FETCH
664  #start_status #final_status #trace_ends_flag
665  #the_trace #program_counter_refl #classify_assm
666  @(trace_any_label_inv_ind … the_trace)
667  [1:
668    #start_status' #final_status' #execute_assm #classifier_assm #costed_assm
669    #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
670    destruct @⊥
671  |2:
672    #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_flag_refl
673    #start_status_refl #final_status_refl #the_trace_refl destruct
674    whd in match (trace_any_label_length … (tal_base_return …));
675    whd in match (compute_paid_trace_any_label … (tal_base_return …));
676    <FETCH %
677  |3:
678    #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
679    #classifier_assm #after_return_assm #trace_label_return #costed_assm
680    #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
681    destruct @⊥
682  |4:
683    #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
684    #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
685    #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
686    #final_status_refl #the_trace_refl
687    destruct @⊥
688  |5:
689    #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
690    #classifier_assm #costed_assm #trace_ends_flag_refl #start_status_refl
691    #final_status_refl #the_trace_refl destruct @⊥
692  ]
693  try (change with (ASM_classify0 ? = ? ∨ ASM_classify0 ? = ?) in classifier_assm;)
694  try (change with (ASM_classify0 ? = ?) in classifier_assm;)
695  whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
696  whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
697  <FETCH in classifier_assm; >classify_assm
698  #absurd try (destruct(absurd))
699  cases absurd
700  #absurd destruct(absurd)
701qed.
702
703lemma trace_any_label_length_leq_0_to_False:
704  ∀code_memory: BitVectorTrie Byte 16.
705  ∀cost_labels: BitVectorTrie costlabel 16.
706  ∀trace_ends_flag: trace_ends_with_ret.
707  ∀start_status: Status code_memory.
708  ∀final_status: Status code_memory.
709  ∀the_trace.
710  trace_any_label_length' code_memory cost_labels trace_ends_flag start_status
711    final_status the_trace ≤ 0 → False.
712  #code_memory #cost_labels #trace_ends_flag #start_status #final_status
713  #the_trace
714  cases the_trace /2/
715qed.
716     
717let rec block_cost'
718  (code_memory': BitVectorTrie Byte 16) (program_counter': Word)
719    (program_size: nat) (total_program_size: nat) (cost_labels: BitVectorTrie costlabel 16)
720      (reachable_program_counter_witness: reachable_program_counter code_memory' total_program_size program_counter')
721        (good_program_witness: good_program code_memory' total_program_size) (first_time_around: bool)
722          on program_size:
723          Σcost_of_block: nat.
724          if (match lookup_opt … program_counter' cost_labels with [ None ⇒ true | _ ⇒ first_time_around ]) then
725            ∀start_status: Status code_memory'.
726            ∀final_status: Status code_memory'.
727            ∀trace_ends_flag.
728            ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
729              trace_any_label_length' … the_trace ≤ program_size →
730              program_counter' = program_counter … start_status →
731                cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace
732          else
733            (cost_of_block = 0) ≝
734  match program_size return λx. x = program_size → ? with
735  [ O ⇒ λbase_case. 0 (* XXX: dummy to be inserted here *)
736  | S program_size' ⇒ λstep_case.
737    let 〈instruction, program_counter'', ticks〉 as FETCH ≝ fetch code_memory' program_counter' in
738    let to_continue ≝
739      match lookup_opt … program_counter' cost_labels with
740      [ None ⇒ true
741      | Some _ ⇒ first_time_around
742      ]
743    in
744      ((if to_continue then
745       pi1 … (match instruction return λx. x = instruction → ? with
746        [ RealInstruction real_instruction ⇒ λreal_instruction_refl.
747          match real_instruction return λx. x = real_instruction →
748          Σcost_of_block: nat.
749            ∀start_status: Status code_memory'.
750            ∀final_status: Status code_memory'.
751            ∀trace_ends_flag.
752            ∀the_trace: trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status.
753              trace_any_label_length' … the_trace ≤ S program_size' →
754              program_counter' = program_counter … start_status →
755                cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace with
756          [ RET                    ⇒ λinstr. ticks
757          | RETI                   ⇒ λinstr. ticks
758          | JC   relative          ⇒ λinstr. ticks
759          | JNC  relative          ⇒ λinstr. ticks
760          | JB   bit_addr relative ⇒ λinstr. ticks
761          | JNB  bit_addr relative ⇒ λinstr. ticks
762          | JBC  bit_addr relative ⇒ λinstr. ticks
763          | JZ   relative          ⇒ λinstr. ticks
764          | JNZ  relative          ⇒ λinstr. ticks
765          | CJNE src_trgt relative ⇒ λinstr. ticks
766          | DJNZ src_trgt relative ⇒ λinstr. ticks
767          | _                      ⇒ λinstr.
768              ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false
769          ] (refl …)
770        | ACALL addr     ⇒ λinstr.
771            ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false
772        | AJMP  addr     ⇒ λinstr.
773          let jump_target ≝ compute_target_of_unconditional_jump program_counter'' instruction in
774            ticks + block_cost' code_memory' jump_target program_size' total_program_size cost_labels ? good_program_witness false
775        | LCALL addr     ⇒ λinstr.
776            ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false
777        | LJMP  addr     ⇒ λinstr.
778          let jump_target ≝ compute_target_of_unconditional_jump program_counter'' instruction in
779            ticks + block_cost' code_memory' jump_target program_size' total_program_size cost_labels ? good_program_witness false
780        | SJMP  addr     ⇒ λinstr.
781          let jump_target ≝ compute_target_of_unconditional_jump program_counter'' instruction in
782            ticks + block_cost' code_memory' jump_target program_size' total_program_size cost_labels ? good_program_witness false
783        | JMP   addr     ⇒ λinstr. (* XXX: actually a call due to use with fptrs *)
784            ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false
785        | MOVC  src trgt ⇒ λinstr.
786            ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false
787        ] (refl …))
788      else
789        0)
790      : Σcost_of_block: nat.
791          match (match lookup_opt … program_counter' cost_labels with [ None ⇒ true | _ ⇒ first_time_around ]) with
792          [ true ⇒
793            ∀start_status: Status code_memory'.
794            ∀final_status: Status code_memory'.
795            ∀trace_ends_flag.
796            ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
797              trace_any_label_length' … the_trace ≤ S program_size' →
798              program_counter' = program_counter … start_status →
799                cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace
800          | false ⇒
801            (cost_of_block = 0)
802          ])
803  ] (refl …).
804  [2:
805    change with (if to_continue then ? else (? = 0))
806    >p in ⊢ (match % return ? with [ _ ⇒ ? | _ ⇒ ? ]); normalize nodelta
807    @pi2
808  |1:
809    destruct
810    cases (lookup_opt ????) normalize nodelta
811    [1:
812      #start_status #final_status #trace_ends_flag #the_trace
813      #absurd
814      cases (trace_any_label_length_leq_0_to_False … absurd)
815    |2:
816      #cost cases first_time_around normalize nodelta try %
817      #start_status #final_status #trace_ends_flag #the_trace #absurd
818      cases (trace_any_label_length_leq_0_to_False … absurd)
819    ]
820  |3:
821    change with (if to_continue then ? else (0 = 0))
822    >p normalize nodelta %
823  |6,7:
824    #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl
825    @(trace_compute_paid_trace_cl_return … reachable_program_counter_witness good_program_witness program_size' … FETCH … the_trace program_counter_refl)
826    destruct %
827  |69,77,79:
828    #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl
829    cases(block_cost' ????????) -block_cost'
830    @(trace_compute_paid_trace_cl_call … reachable_program_counter_witness good_program_witness program_size' … FETCH … the_trace program_counter_refl size_invariant)
831    destruct %
832  |4,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,51,53,55,57,59,61,63,65,
833    67:
834    #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl
835    cases(block_cost' ????????) -block_cost'
836    lapply (trace_compute_paid_trace_cl_other … reachable_program_counter_witness good_program_witness program_size' … FETCH … the_trace program_counter_refl size_invariant)     
837    destruct #assm @assm %
838  |42,43,44,45,46,47,48,49,50:
839    #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl
840    @(trace_compute_paid_trace_cl_jump … reachable_program_counter_witness good_program_witness … FETCH … the_trace program_counter_refl)
841    destruct %
842  |71,73,75: (* XXX: unconditional jumps *)
843    #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl
844    cases (block_cost' ????????) -block_cost'
845    lapply (trace_compute_paid_trace_cl_other … reachable_program_counter_witness good_program_witness program_size' … FETCH … the_trace program_counter_refl size_invariant)
846    whd in match (program_counter_after_other ??); normalize nodelta destruct
847    whd in match (is_unconditional_jump ?); normalize nodelta #assm @assm %
848  ]
849  -block_cost'
850  [32:
851    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
852    lapply(good_program_witness program_counter' reachable_program_counter_witness)
853    <FETCH normalize nodelta <instr normalize nodelta
854    @(subaddressing_mode_elim … [[addr16]] … [[addr16]]) [1: // ] #new_addr
855    * * * * #n'
856    #_ #_ #program_counter_lt' #program_counter_lt_tps'
857    %
858    [1:
859      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
860      <FETCH normalize nodelta whd in match ltb; normalize nodelta
861      >(le_to_leb_true … program_counter_lt') %
862    |2:
863      assumption
864    ]
865  |33:
866    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
867    lapply(good_program_witness program_counter' reachable_program_counter_witness)
868    <FETCH normalize nodelta <instr normalize nodelta
869    @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ] #new_addr
870    cases (split … 8 8 program_counter'') #pc_bu #pc_bl normalize nodelta
871    cases (split … 3 8 new_addr) #thr #eig normalize nodelta
872    cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta * * * * #n'
873    #_ #_ #program_counter_lt' #program_counter_lt_tps'
874    %
875    [1:
876      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
877      <FETCH normalize nodelta whd in match ltb; normalize nodelta
878      >(le_to_leb_true … program_counter_lt') %
879    |2:
880      assumption
881    ]
882  |27,28:
883    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
884    lapply(good_program_witness program_counter' reachable_program_counter_witness)
885    <FETCH normalize nodelta <instr normalize nodelta *
886    #program_counter_lt' #program_counter_lt_tps' %
887    [1,3:
888      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
889      <FETCH normalize nodelta whd in match ltb; normalize nodelta
890      >(le_to_leb_true … program_counter_lt') %
891    |2,4:
892      assumption
893    ]
894  |1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26:
895    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
896    lapply(good_program_witness program_counter' reachable_program_counter_witness)
897    <FETCH normalize nodelta <real_instruction_refl <instr normalize nodelta *
898    #program_counter_lt' #program_counter_lt_tps' %
899    try assumption
900    %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
901    <FETCH normalize nodelta whd in match ltb; normalize nodelta
902    >(le_to_leb_true … program_counter_lt') %
903  |29,30,31: (* XXX: unconditional jumps *)
904    normalize nodelta
905    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
906    lapply (good_program_witness program_counter' reachable_program_counter_witness)
907    <FETCH normalize nodelta <instr normalize nodelta #assm assumption
908  ]
909qed.
910
911definition block_cost:
912    ∀code_memory': BitVectorTrie Byte 16.
913    ∀program_counter': Word.
914    ∀total_program_size: nat.
915    ∀cost_labels: BitVectorTrie costlabel 16.
916    ∀reachable_program_counter_witness: reachable_program_counter code_memory' total_program_size program_counter'.
917    ∀good_program_witness: good_program code_memory' total_program_size.
918      Σcost_of_block: nat.
919        ∀start_status: Status code_memory'.
920        ∀final_status: Status code_memory'.
921        ∀trace_ends_flag.
922        ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
923          trace_any_label_length' code_memory' cost_labels trace_ends_flag start_status final_status the_trace
924            ≤ total_program_size →
925          program_counter' = program_counter … start_status →
926            cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace ≝
927  λcode_memory: BitVectorTrie Byte 16.
928  λprogram_counter: Word.
929  λtotal_program_size: nat.
930  λcost_labels: BitVectorTrie costlabel 16.
931  λreachable_program_counter_witness: reachable_program_counter code_memory total_program_size program_counter.
932  λgood_program_witness: good_program code_memory total_program_size. ?.
933  cases(block_cost' code_memory program_counter total_program_size total_program_size cost_labels
934    reachable_program_counter_witness good_program_witness true)
935  #cost_of_block #block_cost_hyp
936  %{cost_of_block}
937  cases(lookup_opt … cost_labels) in block_cost_hyp;
938  [2: #cost_label] normalize nodelta
939  #hyp assumption
940qed.
941
942lemma fetch_program_counter_n_Sn:
943  ∀instruction: instruction.
944  ∀program_counter, program_counter': Word.
945  ∀ticks, n: nat.
946  ∀code_memory: BitVectorTrie Byte 16.
947    Some … program_counter = fetch_program_counter_n n code_memory (zero 16) →
948      〈instruction,program_counter',ticks〉 = fetch code_memory program_counter →
949        nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' →
950          Some … program_counter' = fetch_program_counter_n (S n) code_memory (zero …).
951  #instruction #program_counter #program_counter' #ticks #n #code_memory
952  #fetch_program_counter_n_hyp #fetch_hyp #lt_hyp
953  whd in match (fetch_program_counter_n (S n) code_memory (zero …));
954  <fetch_program_counter_n_hyp normalize nodelta
955  <fetch_hyp normalize nodelta
956  change with (
957    leb (S (nat_of_bitvector … program_counter)) (nat_of_bitvector … program_counter')
958  ) in match (ltb (nat_of_bitvector … program_counter) (nat_of_bitvector … program_counter'));
959  >(le_to_leb_true … lt_hyp) %
960qed.
961
962(* XXX: to be moved into common/Identifiers.ma *)
963lemma lookup_present_add_hit:
964  ∀tag, A, map, k, v, k_pres.
965    lookup_present tag A (add … map k v) k k_pres = v.
966  #tag #a #map #k #v #k_pres
967  lapply (lookup_lookup_present … (add … map k v) … k_pres)
968  >lookup_add_hit #Some_assm destruct(Some_assm)
969  <e0 %
970qed.
971
972lemma lookup_present_add_miss:
973  ∀tag, A, map, k, k', v, k_pres', k_pres''.
974    k' ≠ k →
975      lookup_present tag A (add … map k v) k' k_pres' = lookup_present tag A map k' k_pres''.
976  #tag #A #map #k #k' #v #k_pres' #k_pres'' #neq_assm
977  lapply (lookup_lookup_present … (add … map k v) ? k_pres')
978  >lookup_add_miss try assumption
979  #Some_assm
980  lapply (lookup_lookup_present … map k') >Some_assm #Some_assm'
981  lapply (Some_assm' k_pres'') #Some_assm'' destruct assumption
982qed.
983
984(* XXX: to be moved into basics/types.ma *)
985lemma not_None_to_Some:
986  ∀A: Type[0].
987  ∀o: option A.
988    o ≠ None A → ∃v: A. o = Some A v.
989  #A #o cases o
990  [1:
991    #absurd cases absurd #absurd' cases (absurd' (refl …))
992  |2:
993    #v' #ignore /2/
994  ]
995qed.
996
997lemma present_add_present:
998  ∀tag, a, map, k, k', v.
999    k' ≠ k →
1000      present tag a (add tag a map k v) k' →
1001        present tag a map k'.
1002  #tag #a #map #k #k' #v #neq_hyp #present_hyp
1003  whd in match present; normalize nodelta
1004  whd in match present in present_hyp; normalize nodelta in present_hyp;
1005  cases (not_None_to_Some a … present_hyp) #v' #Some_eq_hyp
1006  lapply (lookup_add_cases tag ?????? Some_eq_hyp) *
1007  [1:
1008    * #k_eq_hyp @⊥ /2/
1009  |2:
1010    #Some_eq_hyp' /2/
1011  ]
1012qed.
1013
1014lemma present_add_hit:
1015  ∀tag, a, map, k, v.
1016    present tag a (add tag a map k v) k.
1017  #tag #a #map #k #v
1018  whd >lookup_add_hit
1019  % #absurd destruct
1020qed.
1021
1022lemma present_add_miss:
1023  ∀tag, a, map, k, k', v.
1024    k' ≠ k → present tag a map k' → present tag a (add tag a map k v) k'.
1025  #tag #a #map #k #k' #v #neq_assm #present_assm
1026  whd >lookup_add_miss assumption
1027qed.
1028
1029lemma lt_to_le_to_le:
1030  ∀n, m, p: nat.
1031    n < m → m ≤ p → n ≤ p.
1032  #n #m #p #H #H1
1033  elim H
1034  [1:
1035    @(transitive_le n m p) /2/
1036  |2:
1037    /2/
1038  ]
1039qed.
1040
1041lemma eqb_decidable:
1042  ∀l, r: nat.
1043    (eqb l r = true) ∨ (eqb l r = false).
1044  #l #r //
1045qed.
1046
1047lemma r_Sr_and_l_r_to_Sl_r:
1048  ∀r, l: nat.
1049    (∃r': nat. r = S r' ∧ l = r') → S l = r.
1050  #r #l #exists_hyp
1051  cases exists_hyp #r'
1052  #and_hyp cases and_hyp
1053  #left_hyp #right_hyp
1054  destruct %
1055qed.
1056
1057lemma eqb_Sn_to_exists_n':
1058  ∀m, n: nat.
1059    eqb (S m) n = true → ∃n': nat. n = S n'.
1060  #m #n
1061  cases n
1062  [1:
1063    normalize #absurd
1064    destruct(absurd)
1065  |2:
1066    #n' #_ %{n'} %
1067  ]
1068qed.
1069
1070lemma eqb_true_to_eqb_S_S_true:
1071  ∀m, n: nat.
1072    eqb m n = true → eqb (S m) (S n) = true.
1073  #m #n normalize #assm assumption
1074qed.
1075
1076lemma eqb_S_S_true_to_eqb_true:
1077  ∀m, n: nat.
1078    eqb (S m) (S n) = true → eqb m n = true.
1079  #m #n normalize #assm assumption
1080qed.
1081
1082lemma eqb_true_to_refl:
1083  ∀l, r: nat.
1084    eqb l r = true → l = r.
1085  #l
1086  elim l
1087  [1:
1088    #r cases r
1089    [1:
1090      #_ %
1091    |2:
1092      #l' normalize
1093      #absurd destruct(absurd)
1094    ]
1095  |2:
1096    #l' #inductive_hypothesis #r
1097    #eqb_refl @r_Sr_and_l_r_to_Sl_r
1098    %{(pred r)} @conj
1099    [1:
1100      cases (eqb_Sn_to_exists_n' … eqb_refl)
1101      #r' #S_assm >S_assm %
1102    |2:
1103      cases (eqb_Sn_to_exists_n' … eqb_refl)
1104      #r' #refl_assm destruct normalize
1105      @inductive_hypothesis
1106      normalize in eqb_refl; assumption
1107    ]
1108  ]
1109qed.
1110
1111lemma r_O_or_exists_r_r_Sr_and_l_neq_r_to_Sl_neq_r:
1112  ∀r, l: nat.
1113    r = O ∨ (∃r': nat. r = S r' ∧ l ≠ r') → S l ≠ r.
1114  #r #l #disj_hyp
1115  cases disj_hyp
1116  [1:
1117    #r_O_refl destruct @nmk
1118    #absurd destruct(absurd)
1119  |2:
1120    #exists_hyp cases exists_hyp #r'
1121    #conj_hyp cases conj_hyp #left_conj #right_conj
1122    destruct @nmk #S_S_refl_hyp
1123    elim right_conj #hyp @hyp //
1124  ]
1125qed.
1126
1127lemma neq_l_r_to_neq_Sl_Sr:
1128  ∀l, r: nat.
1129    l ≠ r → S l ≠ S r.
1130  #l #r #l_neq_r_assm
1131  @nmk #Sl_Sr_assm cases l_neq_r_assm
1132  #assm @assm //
1133qed.
1134
1135lemma eqb_false_to_not_refl:
1136  ∀l, r: nat.
1137    eqb l r = false → l ≠ r.
1138  #l
1139  elim l
1140  [1:
1141    #r cases r
1142    [1:
1143      normalize #absurd destruct(absurd)
1144    |2:
1145      #r' #_ @nmk
1146      #absurd destruct(absurd)
1147    ]
1148  |2:
1149    #l' #inductive_hypothesis #r
1150    cases r
1151    [1:
1152      #eqb_false_assm
1153      @r_O_or_exists_r_r_Sr_and_l_neq_r_to_Sl_neq_r
1154      @or_introl %
1155    |2:
1156      #r' #eqb_false_assm
1157      @neq_l_r_to_neq_Sl_Sr
1158      @inductive_hypothesis
1159      assumption
1160    ]
1161  ]
1162qed.
1163
1164lemma le_to_lt_or_eq:
1165  ∀m, n: nat.
1166    m ≤ n → m = n ∨ m < n.
1167  #m #n #le_hyp
1168  cases le_hyp
1169  [1:
1170    @or_introl %
1171  |2:
1172    #m' #le_hyp'
1173    @or_intror
1174    normalize
1175    @le_S_S assumption
1176  ]
1177qed.
1178
1179lemma le_neq_to_lt:
1180  ∀m, n: nat.
1181    m ≤ n → m ≠ n → m < n.
1182  #m #n #le_hyp #neq_hyp
1183  cases neq_hyp
1184  #eq_absurd_hyp
1185  generalize in match (le_to_lt_or_eq m n le_hyp);
1186  #disj_assm cases disj_assm
1187  [1:
1188    #absurd cases (eq_absurd_hyp absurd)
1189  |2:
1190    #assm assumption
1191  ]
1192qed.
1193
1194inverter nat_jmdiscr for nat.
1195
1196(* XXX: this is false in the general case.  For instance, if n = 0 then the
1197        base case requires us prove 1 = 0, as it is the carry bit that holds
1198        the result of the addition. *)
1199axiom succ_nat_of_bitvector_half_add_1:
1200  ∀n: nat.
1201  ∀bv: BitVector n.
1202  ∀power_proof: nat_of_bitvector … bv < 2^n - 1.
1203    S (nat_of_bitvector … bv) = nat_of_bitvector …
1204      (\snd (half_add n (bitvector_of_nat … 1) bv)).
1205
1206lemma plus_lt_to_lt:
1207  ∀m, n, o: nat.
1208    m + n < o → m < o.
1209  #m #n #o
1210  elim n
1211  [1:
1212    <(plus_n_O m) in ⊢ (% → ?);
1213    #assumption assumption
1214  |2:
1215    #n' #inductive_hypothesis
1216    <(plus_n_Sm m n') in ⊢ (% → ?);
1217    #assm @inductive_hypothesis
1218    normalize in assm; normalize
1219    /2 by lt_S_to_lt/
1220  ]
1221qed.
1222
1223include "arithmetics/div_and_mod.ma".
1224
1225lemma n_plus_1_n_to_False:
1226  ∀n: nat.
1227    n + 1 = n → False.
1228  #n elim n
1229  [1:
1230    normalize #absurd destruct(absurd)
1231  |2:
1232    #n' #inductive_hypothesis normalize
1233    #absurd @inductive_hypothesis /2/
1234  ]
1235qed.
1236
1237lemma one_two_times_n_to_False:
1238  ∀n: nat.
1239    1=2*n→False.
1240  #n cases n
1241  [1:
1242    normalize #absurd destruct(absurd)
1243  |2:
1244    #n' normalize #absurd
1245    lapply (injective_S … absurd) -absurd #absurd
1246    /2/
1247  ]
1248qed.
1249
1250lemma generalized_nat_cases:
1251  ∀n: nat.
1252    n = 0 ∨ n = 1 ∨ ∃m: nat. n = S (S m).
1253  #n
1254  cases n
1255  [1:
1256    @or_introl @or_introl %
1257  |2:
1258    #n' cases n'
1259    [1:
1260      @or_introl @or_intror %
1261    |2:
1262      #n'' @or_intror %{n''} %
1263    ]
1264  ]
1265qed.
1266
1267let rec odd_p
1268  (n: nat)
1269    on n ≝
1270  match n with
1271  [ O ⇒ False
1272  | S n' ⇒ even_p n'
1273  ]
1274and even_p
1275  (n: nat)
1276    on n ≝
1277  match n with
1278  [ O ⇒ True
1279  | S n' ⇒ odd_p n'
1280  ].
1281
1282let rec n_even_p_to_n_plus_2_even_p
1283  (n: nat)
1284    on n: even_p n → even_p (n + 2) ≝
1285  match n with
1286  [ O ⇒ ?
1287  | S n' ⇒ ?
1288  ]
1289and n_odd_p_to_n_plus_2_odd_p
1290  (n: nat)
1291    on n: odd_p n → odd_p (n + 2) ≝
1292  match n with
1293  [ O ⇒ ?
1294  | S n' ⇒ ?
1295  ].
1296  [1,3:
1297    normalize #assm assumption
1298  |2:
1299    normalize @n_odd_p_to_n_plus_2_odd_p
1300  |4:
1301    normalize @n_even_p_to_n_plus_2_even_p
1302  ]
1303qed.
1304
1305let rec two_times_n_even_p
1306  (n: nat)
1307    on n: even_p (2 * n) ≝
1308  match n with
1309  [ O ⇒ ?
1310  | S n' ⇒ ?
1311  ]
1312and two_times_n_plus_one_odd_p
1313  (n: nat)
1314    on n: odd_p ((2 * n) + 1) ≝
1315  match n with
1316  [ O ⇒ ?
1317  | S n' ⇒ ?
1318  ].
1319  [1,3:
1320    normalize @I
1321  |2:
1322    normalize
1323    >plus_n_Sm
1324    <(associative_plus n' n' 1)
1325    >(plus_n_O (n' + n'))
1326    cut(n' + n' + 0 + 1 = 2 * n' + 1)
1327    [1:
1328      //
1329    |2:
1330      #refl_assm >refl_assm
1331      @two_times_n_plus_one_odd_p     
1332    ]
1333  |4:
1334    normalize
1335    >plus_n_Sm
1336    cut(n' + (n' + 1) + 1 = (2 * n') + 2)
1337    [1:
1338      normalize /2/
1339    |2:
1340      #refl_assm >refl_assm
1341      @n_even_p_to_n_plus_2_even_p
1342      @two_times_n_even_p
1343    ]
1344  ]
1345qed.
1346
1347let rec even_p_to_not_odd_p
1348  (n: nat)
1349    on n: even_p n → ¬ odd_p n ≝
1350  match n with
1351  [ O ⇒ ?
1352  | S n' ⇒ ?
1353  ]
1354and odd_p_to_not_even_p
1355  (n: nat)
1356    on n: odd_p n → ¬ even_p n ≝
1357  match n with
1358  [ O ⇒ ?
1359  | S n' ⇒ ?
1360  ].
1361  [1:
1362    normalize #_
1363    @nmk #assm assumption
1364  |3:
1365    normalize #absurd
1366    cases absurd
1367  |2:
1368    normalize
1369    @odd_p_to_not_even_p
1370  |4:
1371    normalize
1372    @even_p_to_not_odd_p
1373  ]
1374qed.
1375
1376lemma even_p_odd_p_cases:
1377  ∀n: nat.
1378    even_p n ∨ odd_p n.
1379  #n elim n
1380  [1:
1381    normalize @or_introl @I
1382  |2:
1383    #n' #inductive_hypothesis
1384    normalize
1385    cases inductive_hypothesis
1386    #assm
1387    try (@or_introl assumption)
1388    try (@or_intror assumption)
1389  ]
1390qed.
1391
1392lemma two_times_n_plus_one_refl_two_times_n_to_False:
1393  ∀m, n: nat.
1394    2 * m + 1 = 2 * n → False.
1395  #m #n
1396  #assm
1397  cut (even_p (2 * n) ∧ even_p ((2 * m) + 1))
1398  [1:
1399    >assm
1400    @conj
1401    @two_times_n_even_p
1402  |2:
1403    * #_ #absurd
1404    cases (even_p_to_not_odd_p … absurd)
1405    #assm @assm
1406    @two_times_n_plus_one_odd_p
1407  ]
1408qed.
1409
1410lemma nat_of_bitvector_aux_injective:
1411  ∀n: nat.
1412  ∀l, r: BitVector n.
1413  ∀acc_l, acc_r: nat.
1414    nat_of_bitvector_aux n acc_l l = nat_of_bitvector_aux n acc_r r →
1415      acc_l = acc_r ∧ l ≃ r.
1416  #n #l
1417  elim l #r
1418  [1:
1419    #acc_l #acc_r normalize
1420    >(BitVector_O r) normalize /2/
1421  |2:
1422    #hd #tl #inductive_hypothesis #r #acc_l #acc_r
1423    normalize normalize in inductive_hypothesis;
1424    cases (BitVector_Sn … r)
1425    #r_hd * #r_tl #r_refl destruct normalize
1426    cases hd cases r_hd normalize
1427    [1:
1428      #relevant
1429      cases (inductive_hypothesis … relevant)
1430      #acc_assm #tl_assm destruct % //
1431      lapply (injective_plus_l ? ? ? acc_assm)
1432      -acc_assm #acc_assm
1433      change with (2 * acc_l = 2 * acc_r) in acc_assm;
1434      lapply (injective_times_r ? ? ? ? acc_assm) /2/
1435    |4:
1436      #relevant
1437      cases (inductive_hypothesis … relevant)
1438      #acc_assm #tl_assm destruct % //
1439      change with (2 * acc_l = 2 * acc_r) in acc_assm;
1440      lapply(injective_times_r ? ? ? ? acc_assm) /2/
1441    |2:
1442      #relevant 
1443      change with ((nat_of_bitvector_aux r (2 * acc_l + 1) tl) =
1444        (nat_of_bitvector_aux r (2 * acc_r) r_tl)) in relevant;
1445      cases (eqb_decidable … (2 * acc_l + 1) (2 * acc_r))
1446      [1:
1447        #eqb_true_assm
1448        lapply (eqb_true_to_refl … eqb_true_assm)
1449        #refl_assm
1450        cases (two_times_n_plus_one_refl_two_times_n_to_False … refl_assm)
1451      |2:
1452        #eqb_false_assm
1453        lapply (eqb_false_to_not_refl … eqb_false_assm)
1454        #not_refl_assm cases not_refl_assm #absurd_assm
1455        cases (inductive_hypothesis … relevant) #absurd
1456        cases (absurd_assm absurd)
1457      ]
1458    |3:
1459      #relevant 
1460      change with ((nat_of_bitvector_aux r (2 * acc_l) tl) =
1461        (nat_of_bitvector_aux r (2 * acc_r + 1) r_tl)) in relevant;
1462      cases (eqb_decidable … (2 * acc_l) (2 * acc_r + 1))
1463      [1:
1464        #eqb_true_assm
1465        lapply (eqb_true_to_refl … eqb_true_assm)
1466        #refl_assm
1467        lapply (sym_eq ? (2 * acc_l) (2 * acc_r + 1) refl_assm)
1468        -refl_assm #refl_assm
1469        cases (two_times_n_plus_one_refl_two_times_n_to_False … refl_assm)
1470      |2:
1471        #eqb_false_assm
1472        lapply (eqb_false_to_not_refl … eqb_false_assm)
1473        #not_refl_assm cases not_refl_assm #absurd_assm
1474        cases (inductive_hypothesis … relevant) #absurd
1475        cases (absurd_assm absurd)
1476      ]
1477    ]
1478  ]
1479qed.
1480
1481lemma nat_of_bitvector_destruct:
1482  ∀n: nat.
1483  ∀l_hd, r_hd: bool.
1484  ∀l_tl, r_tl: BitVector n.
1485    nat_of_bitvector (S n) (l_hd:::l_tl) = nat_of_bitvector (S n) (r_hd:::r_tl) →
1486      l_hd = r_hd ∧ nat_of_bitvector n l_tl = nat_of_bitvector n r_tl.
1487  #n #l_hd #r_hd #l_tl #r_tl
1488  normalize
1489  cases l_hd cases r_hd
1490  normalize
1491  [4:
1492    /2/
1493  |1:
1494    #relevant
1495    cases (nat_of_bitvector_aux_injective … relevant)
1496    #_ #l_r_tl_refl destruct /2/
1497  |2,3:
1498    #relevant
1499    cases (nat_of_bitvector_aux_injective … relevant)
1500    #absurd destruct(absurd)
1501  ]
1502qed.
1503
1504lemma BitVector_cons_injective:
1505  ∀n: nat.
1506  ∀l_hd, r_hd: bool.
1507  ∀l_tl, r_tl: BitVector n.
1508    l_hd = r_hd → l_tl = r_tl → l_hd:::l_tl = r_hd:::r_tl.
1509  #l #l_hd #r_hd #l_tl #r_tl
1510  #l_refl #r_refl destruct %
1511qed.
1512
1513lemma refl_nat_of_bitvector_to_refl:
1514  ∀n: nat.
1515  ∀l, r: BitVector n.
1516    nat_of_bitvector n l = nat_of_bitvector n r → l = r.
1517  #n
1518  elim n
1519  [1:
1520    #l #r
1521    >(BitVector_O l)
1522    >(BitVector_O r)
1523    #_ %
1524  |2:
1525    #n' #inductive_hypothesis #l #r
1526    lapply (BitVector_Sn ? l) #l_hypothesis
1527    lapply (BitVector_Sn ? r) #r_hypothesis
1528    cases l_hypothesis #l_hd #l_tail_hypothesis
1529    cases r_hypothesis #r_hd #r_tail_hypothesis
1530    cases l_tail_hypothesis #l_tl #l_hd_tl_refl
1531    cases r_tail_hypothesis #r_tl #r_hd_tl_refl
1532    destruct #cons_refl
1533    cases (nat_of_bitvector_destruct n' l_hd r_hd l_tl r_tl cons_refl)
1534    #hd_refl #tl_refl
1535    @BitVector_cons_injective try assumption
1536    @inductive_hypothesis assumption
1537  ]
1538qed.
Note: See TracBrowser for help on using the repository browser.