root/src/ASM/ASMCosts.ma @ 1909

Revision 1909, 58.8 KB (checked in by mulligan, 13 months ago)

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