source: src/ASM/ASMCosts.ma @ 1913

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

Got the rest of the file to typecheck as before.

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