source: src/ASM/ASMCosts.ma @ 1912

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

Patches to get block_cost' and dependencies working again after change to termination argument. Six goals remain, currently closed by daemons, corresponding to two goals for each unconditional jump.

File size: 58.8 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          program_counter' = program_counter … start_status →
913            cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace ≝
914  λcode_memory: BitVectorTrie Byte 16.
915  λprogram_counter: Word.
916  λtotal_program_size: nat.
917  λcost_labels: BitVectorTrie costlabel 16.
918  λreachable_program_counter_witness: reachable_program_counter code_memory total_program_size program_counter.
919  λgood_program_witness: good_program code_memory total_program_size. ?.
920  cases(block_cost' code_memory program_counter [ ] total_program_size total_program_size cost_labels
921    reachable_program_counter_witness good_program_witness true ?)
922  [1:
923    #cost_of_block #block_cost_hyp
924    %{cost_of_block}
925    cases(lookup_opt … cost_labels) in block_cost_hyp;
926    [2: #cost_label] normalize nodelta
927    #hyp assumption
928  |2:
929    @le_plus_n_r
930  ]
931qed.
932
933lemma fetch_program_counter_n_Sn:
934  ∀instruction: instruction.
935  ∀program_counter, program_counter': Word.
936  ∀ticks, n: nat.
937  ∀code_memory: BitVectorTrie Byte 16.
938    Some … program_counter = fetch_program_counter_n n code_memory (zero 16) →
939      〈instruction,program_counter',ticks〉 = fetch code_memory program_counter →
940        nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' →
941          Some … program_counter' = fetch_program_counter_n (S n) code_memory (zero …).
942  #instruction #program_counter #program_counter' #ticks #n #code_memory
943  #fetch_program_counter_n_hyp #fetch_hyp #lt_hyp
944  whd in match (fetch_program_counter_n (S n) code_memory (zero …));
945  <fetch_program_counter_n_hyp normalize nodelta
946  <fetch_hyp normalize nodelta
947  change with (
948    leb (S (nat_of_bitvector … program_counter)) (nat_of_bitvector … program_counter')
949  ) in match (ltb (nat_of_bitvector … program_counter) (nat_of_bitvector … program_counter'));
950  >(le_to_leb_true … lt_hyp) %
951qed.
952
953(* XXX: to be moved into common/Identifiers.ma *)
954lemma lookup_present_add_hit:
955  ∀tag, A, map, k, v, k_pres.
956    lookup_present tag A (add … map k v) k k_pres = v.
957  #tag #a #map #k #v #k_pres
958  lapply (lookup_lookup_present … (add … map k v) … k_pres)
959  >lookup_add_hit #Some_assm destruct(Some_assm)
960  <e0 %
961qed.
962
963lemma lookup_present_add_miss:
964  ∀tag, A, map, k, k', v, k_pres', k_pres''.
965    k' ≠ k →
966      lookup_present tag A (add … map k v) k' k_pres' = lookup_present tag A map k' k_pres''.
967  #tag #A #map #k #k' #v #k_pres' #k_pres'' #neq_assm
968  lapply (lookup_lookup_present … (add … map k v) ? k_pres')
969  >lookup_add_miss try assumption
970  #Some_assm
971  lapply (lookup_lookup_present … map k') >Some_assm #Some_assm'
972  lapply (Some_assm' k_pres'') #Some_assm'' destruct assumption
973qed.
974
975(* XXX: to be moved into basics/types.ma *)
976lemma not_None_to_Some:
977  ∀A: Type[0].
978  ∀o: option A.
979    o ≠ None A → ∃v: A. o = Some A v.
980  #A #o cases o
981  [1:
982    #absurd cases absurd #absurd' cases (absurd' (refl …))
983  |2:
984    #v' #ignore /2/
985  ]
986qed.
987
988lemma present_add_present:
989  ∀tag, a, map, k, k', v.
990    k' ≠ k →
991      present tag a (add tag a map k v) k' →
992        present tag a map k'.
993  #tag #a #map #k #k' #v #neq_hyp #present_hyp
994  whd in match present; normalize nodelta
995  whd in match present in present_hyp; normalize nodelta in present_hyp;
996  cases (not_None_to_Some a … present_hyp) #v' #Some_eq_hyp
997  lapply (lookup_add_cases tag ?????? Some_eq_hyp) *
998  [1:
999    * #k_eq_hyp @⊥ /2/
1000  |2:
1001    #Some_eq_hyp' /2/
1002  ]
1003qed.
1004
1005lemma present_add_hit:
1006  ∀tag, a, map, k, v.
1007    present tag a (add tag a map k v) k.
1008  #tag #a #map #k #v
1009  whd >lookup_add_hit
1010  % #absurd destruct
1011qed.
1012
1013lemma present_add_miss:
1014  ∀tag, a, map, k, k', v.
1015    k' ≠ k → present tag a map k' → present tag a (add tag a map k v) k'.
1016  #tag #a #map #k #k' #v #neq_assm #present_assm
1017  whd >lookup_add_miss assumption
1018qed.
1019
1020lemma lt_to_le_to_le:
1021  ∀n, m, p: nat.
1022    n < m → m ≤ p → n ≤ p.
1023  #n #m #p #H #H1
1024  elim H
1025  [1:
1026    @(transitive_le n m p) /2/
1027  |2:
1028    /2/
1029  ]
1030qed.
1031
1032lemma eqb_decidable:
1033  ∀l, r: nat.
1034    (eqb l r = true) ∨ (eqb l r = false).
1035  #l #r //
1036qed.
1037
1038lemma r_Sr_and_l_r_to_Sl_r:
1039  ∀r, l: nat.
1040    (∃r': nat. r = S r' ∧ l = r') → S l = r.
1041  #r #l #exists_hyp
1042  cases exists_hyp #r'
1043  #and_hyp cases and_hyp
1044  #left_hyp #right_hyp
1045  destruct %
1046qed.
1047
1048lemma eqb_Sn_to_exists_n':
1049  ∀m, n: nat.
1050    eqb (S m) n = true → ∃n': nat. n = S n'.
1051  #m #n
1052  cases n
1053  [1:
1054    normalize #absurd
1055    destruct(absurd)
1056  |2:
1057    #n' #_ %{n'} %
1058  ]
1059qed.
1060
1061lemma eqb_true_to_eqb_S_S_true:
1062  ∀m, n: nat.
1063    eqb m n = true → eqb (S m) (S n) = true.
1064  #m #n normalize #assm assumption
1065qed.
1066
1067lemma eqb_S_S_true_to_eqb_true:
1068  ∀m, n: nat.
1069    eqb (S m) (S n) = true → eqb m n = true.
1070  #m #n normalize #assm assumption
1071qed.
1072
1073lemma eqb_true_to_refl:
1074  ∀l, r: nat.
1075    eqb l r = true → l = r.
1076  #l
1077  elim l
1078  [1:
1079    #r cases r
1080    [1:
1081      #_ %
1082    |2:
1083      #l' normalize
1084      #absurd destruct(absurd)
1085    ]
1086  |2:
1087    #l' #inductive_hypothesis #r
1088    #eqb_refl @r_Sr_and_l_r_to_Sl_r
1089    %{(pred r)} @conj
1090    [1:
1091      cases (eqb_Sn_to_exists_n' … eqb_refl)
1092      #r' #S_assm >S_assm %
1093    |2:
1094      cases (eqb_Sn_to_exists_n' … eqb_refl)
1095      #r' #refl_assm destruct normalize
1096      @inductive_hypothesis
1097      normalize in eqb_refl; assumption
1098    ]
1099  ]
1100qed.
1101
1102lemma r_O_or_exists_r_r_Sr_and_l_neq_r_to_Sl_neq_r:
1103  ∀r, l: nat.
1104    r = O ∨ (∃r': nat. r = S r' ∧ l ≠ r') → S l ≠ r.
1105  #r #l #disj_hyp
1106  cases disj_hyp
1107  [1:
1108    #r_O_refl destruct @nmk
1109    #absurd destruct(absurd)
1110  |2:
1111    #exists_hyp cases exists_hyp #r'
1112    #conj_hyp cases conj_hyp #left_conj #right_conj
1113    destruct @nmk #S_S_refl_hyp
1114    elim right_conj #hyp @hyp //
1115  ]
1116qed.
1117
1118lemma neq_l_r_to_neq_Sl_Sr:
1119  ∀l, r: nat.
1120    l ≠ r → S l ≠ S r.
1121  #l #r #l_neq_r_assm
1122  @nmk #Sl_Sr_assm cases l_neq_r_assm
1123  #assm @assm //
1124qed.
1125
1126lemma eqb_false_to_not_refl:
1127  ∀l, r: nat.
1128    eqb l r = false → l ≠ r.
1129  #l
1130  elim l
1131  [1:
1132    #r cases r
1133    [1:
1134      normalize #absurd destruct(absurd)
1135    |2:
1136      #r' #_ @nmk
1137      #absurd destruct(absurd)
1138    ]
1139  |2:
1140    #l' #inductive_hypothesis #r
1141    cases r
1142    [1:
1143      #eqb_false_assm
1144      @r_O_or_exists_r_r_Sr_and_l_neq_r_to_Sl_neq_r
1145      @or_introl %
1146    |2:
1147      #r' #eqb_false_assm
1148      @neq_l_r_to_neq_Sl_Sr
1149      @inductive_hypothesis
1150      assumption
1151    ]
1152  ]
1153qed.
1154
1155lemma le_to_lt_or_eq:
1156  ∀m, n: nat.
1157    m ≤ n → m = n ∨ m < n.
1158  #m #n #le_hyp
1159  cases le_hyp
1160  [1:
1161    @or_introl %
1162  |2:
1163    #m' #le_hyp'
1164    @or_intror
1165    normalize
1166    @le_S_S assumption
1167  ]
1168qed.
1169
1170lemma le_neq_to_lt:
1171  ∀m, n: nat.
1172    m ≤ n → m ≠ n → m < n.
1173  #m #n #le_hyp #neq_hyp
1174  cases neq_hyp
1175  #eq_absurd_hyp
1176  generalize in match (le_to_lt_or_eq m n le_hyp);
1177  #disj_assm cases disj_assm
1178  [1:
1179    #absurd cases (eq_absurd_hyp absurd)
1180  |2:
1181    #assm assumption
1182  ]
1183qed.
1184
1185inverter nat_jmdiscr for nat.
1186
1187(* XXX: this is false in the general case.  For instance, if n = 0 then the
1188        base case requires us prove 1 = 0, as it is the carry bit that holds
1189        the result of the addition. *)
1190axiom succ_nat_of_bitvector_half_add_1:
1191  ∀n: nat.
1192  ∀bv: BitVector n.
1193  ∀power_proof: nat_of_bitvector … bv < 2^n - 1.
1194    S (nat_of_bitvector … bv) = nat_of_bitvector …
1195      (\snd (half_add n (bitvector_of_nat … 1) bv)).
1196
1197lemma plus_lt_to_lt:
1198  ∀m, n, o: nat.
1199    m + n < o → m < o.
1200  #m #n #o
1201  elim n
1202  [1:
1203    <(plus_n_O m) in ⊢ (% → ?);
1204    #assumption assumption
1205  |2:
1206    #n' #inductive_hypothesis
1207    <(plus_n_Sm m n') in ⊢ (% → ?);
1208    #assm @inductive_hypothesis
1209    normalize in assm; normalize
1210    /2 by lt_S_to_lt/
1211  ]
1212qed.
1213
1214include "arithmetics/div_and_mod.ma".
1215
1216lemma n_plus_1_n_to_False:
1217  ∀n: nat.
1218    n + 1 = n → False.
1219  #n elim n
1220  [1:
1221    normalize #absurd destruct(absurd)
1222  |2:
1223    #n' #inductive_hypothesis normalize
1224    #absurd @inductive_hypothesis /2/
1225  ]
1226qed.
1227
1228lemma one_two_times_n_to_False:
1229  ∀n: nat.
1230    1=2*n→False.
1231  #n cases n
1232  [1:
1233    normalize #absurd destruct(absurd)
1234  |2:
1235    #n' normalize #absurd
1236    lapply (injective_S … absurd) -absurd #absurd
1237    /2/
1238  ]
1239qed.
1240
1241lemma generalized_nat_cases:
1242  ∀n: nat.
1243    n = 0 ∨ n = 1 ∨ ∃m: nat. n = S (S m).
1244  #n
1245  cases n
1246  [1:
1247    @or_introl @or_introl %
1248  |2:
1249    #n' cases n'
1250    [1:
1251      @or_introl @or_intror %
1252    |2:
1253      #n'' @or_intror %{n''} %
1254    ]
1255  ]
1256qed.
1257
1258let rec odd_p
1259  (n: nat)
1260    on n ≝
1261  match n with
1262  [ O ⇒ False
1263  | S n' ⇒ even_p n'
1264  ]
1265and even_p
1266  (n: nat)
1267    on n ≝
1268  match n with
1269  [ O ⇒ True
1270  | S n' ⇒ odd_p n'
1271  ].
1272
1273let rec n_even_p_to_n_plus_2_even_p
1274  (n: nat)
1275    on n: even_p n → even_p (n + 2) ≝
1276  match n with
1277  [ O ⇒ ?
1278  | S n' ⇒ ?
1279  ]
1280and n_odd_p_to_n_plus_2_odd_p
1281  (n: nat)
1282    on n: odd_p n → odd_p (n + 2) ≝
1283  match n with
1284  [ O ⇒ ?
1285  | S n' ⇒ ?
1286  ].
1287  [1,3:
1288    normalize #assm assumption
1289  |2:
1290    normalize @n_odd_p_to_n_plus_2_odd_p
1291  |4:
1292    normalize @n_even_p_to_n_plus_2_even_p
1293  ]
1294qed.
1295
1296let rec two_times_n_even_p
1297  (n: nat)
1298    on n: even_p (2 * n) ≝
1299  match n with
1300  [ O ⇒ ?
1301  | S n' ⇒ ?
1302  ]
1303and two_times_n_plus_one_odd_p
1304  (n: nat)
1305    on n: odd_p ((2 * n) + 1) ≝
1306  match n with
1307  [ O ⇒ ?
1308  | S n' ⇒ ?
1309  ].
1310  [1,3:
1311    normalize @I
1312  |2:
1313    normalize
1314    >plus_n_Sm
1315    <(associative_plus n' n' 1)
1316    >(plus_n_O (n' + n'))
1317    cut(n' + n' + 0 + 1 = 2 * n' + 1)
1318    [1:
1319      //
1320    |2:
1321      #refl_assm >refl_assm
1322      @two_times_n_plus_one_odd_p     
1323    ]
1324  |4:
1325    normalize
1326    >plus_n_Sm
1327    cut(n' + (n' + 1) + 1 = (2 * n') + 2)
1328    [1:
1329      normalize /2/
1330    |2:
1331      #refl_assm >refl_assm
1332      @n_even_p_to_n_plus_2_even_p
1333      @two_times_n_even_p
1334    ]
1335  ]
1336qed.
1337
1338let rec even_p_to_not_odd_p
1339  (n: nat)
1340    on n: even_p n → ¬ odd_p n ≝
1341  match n with
1342  [ O ⇒ ?
1343  | S n' ⇒ ?
1344  ]
1345and odd_p_to_not_even_p
1346  (n: nat)
1347    on n: odd_p n → ¬ even_p n ≝
1348  match n with
1349  [ O ⇒ ?
1350  | S n' ⇒ ?
1351  ].
1352  [1:
1353    normalize #_
1354    @nmk #assm assumption
1355  |3:
1356    normalize #absurd
1357    cases absurd
1358  |2:
1359    normalize
1360    @odd_p_to_not_even_p
1361  |4:
1362    normalize
1363    @even_p_to_not_odd_p
1364  ]
1365qed.
1366
1367lemma even_p_odd_p_cases:
1368  ∀n: nat.
1369    even_p n ∨ odd_p n.
1370  #n elim n
1371  [1:
1372    normalize @or_introl @I
1373  |2:
1374    #n' #inductive_hypothesis
1375    normalize
1376    cases inductive_hypothesis
1377    #assm
1378    try (@or_introl assumption)
1379    try (@or_intror assumption)
1380  ]
1381qed.
1382
1383lemma two_times_n_plus_one_refl_two_times_n_to_False:
1384  ∀m, n: nat.
1385    2 * m + 1 = 2 * n → False.
1386  #m #n
1387  #assm
1388  cut (even_p (2 * n) ∧ even_p ((2 * m) + 1))
1389  [1:
1390    >assm
1391    @conj
1392    @two_times_n_even_p
1393  |2:
1394    * #_ #absurd
1395    cases (even_p_to_not_odd_p … absurd)
1396    #assm @assm
1397    @two_times_n_plus_one_odd_p
1398  ]
1399qed.
1400
1401lemma nat_of_bitvector_aux_injective:
1402  ∀n: nat.
1403  ∀l, r: BitVector n.
1404  ∀acc_l, acc_r: nat.
1405    nat_of_bitvector_aux n acc_l l = nat_of_bitvector_aux n acc_r r →
1406      acc_l = acc_r ∧ l ≃ r.
1407  #n #l
1408  elim l #r
1409  [1:
1410    #acc_l #acc_r normalize
1411    >(BitVector_O r) normalize /2/
1412  |2:
1413    #hd #tl #inductive_hypothesis #r #acc_l #acc_r
1414    normalize normalize in inductive_hypothesis;
1415    cases (BitVector_Sn … r)
1416    #r_hd * #r_tl #r_refl destruct normalize
1417    cases hd cases r_hd normalize
1418    [1:
1419      #relevant
1420      cases (inductive_hypothesis … relevant)
1421      #acc_assm #tl_assm destruct % //
1422      lapply (injective_plus_l ? ? ? acc_assm)
1423      -acc_assm #acc_assm
1424      change with (2 * acc_l = 2 * acc_r) in acc_assm;
1425      lapply (injective_times_r ? ? ? ? acc_assm) /2/
1426    |4:
1427      #relevant
1428      cases (inductive_hypothesis … relevant)
1429      #acc_assm #tl_assm destruct % //
1430      change with (2 * acc_l = 2 * acc_r) in acc_assm;
1431      lapply(injective_times_r ? ? ? ? acc_assm) /2/
1432    |2:
1433      #relevant 
1434      change with ((nat_of_bitvector_aux r (2 * acc_l + 1) tl) =
1435        (nat_of_bitvector_aux r (2 * acc_r) r_tl)) in relevant;
1436      cases (eqb_decidable … (2 * acc_l + 1) (2 * acc_r))
1437      [1:
1438        #eqb_true_assm
1439        lapply (eqb_true_to_refl … eqb_true_assm)
1440        #refl_assm
1441        cases (two_times_n_plus_one_refl_two_times_n_to_False … refl_assm)
1442      |2:
1443        #eqb_false_assm
1444        lapply (eqb_false_to_not_refl … eqb_false_assm)
1445        #not_refl_assm cases not_refl_assm #absurd_assm
1446        cases (inductive_hypothesis … relevant) #absurd
1447        cases (absurd_assm absurd)
1448      ]
1449    |3:
1450      #relevant 
1451      change with ((nat_of_bitvector_aux r (2 * acc_l) tl) =
1452        (nat_of_bitvector_aux r (2 * acc_r + 1) r_tl)) in relevant;
1453      cases (eqb_decidable … (2 * acc_l) (2 * acc_r + 1))
1454      [1:
1455        #eqb_true_assm
1456        lapply (eqb_true_to_refl … eqb_true_assm)
1457        #refl_assm
1458        lapply (sym_eq ? (2 * acc_l) (2 * acc_r + 1) refl_assm)
1459        -refl_assm #refl_assm
1460        cases (two_times_n_plus_one_refl_two_times_n_to_False … refl_assm)
1461      |2:
1462        #eqb_false_assm
1463        lapply (eqb_false_to_not_refl … eqb_false_assm)
1464        #not_refl_assm cases not_refl_assm #absurd_assm
1465        cases (inductive_hypothesis … relevant) #absurd
1466        cases (absurd_assm absurd)
1467      ]
1468    ]
1469  ]
1470qed.
1471
1472lemma nat_of_bitvector_destruct:
1473  ∀n: nat.
1474  ∀l_hd, r_hd: bool.
1475  ∀l_tl, r_tl: BitVector n.
1476    nat_of_bitvector (S n) (l_hd:::l_tl) = nat_of_bitvector (S n) (r_hd:::r_tl) →
1477      l_hd = r_hd ∧ nat_of_bitvector n l_tl = nat_of_bitvector n r_tl.
1478  #n #l_hd #r_hd #l_tl #r_tl
1479  normalize
1480  cases l_hd cases r_hd
1481  normalize
1482  [4:
1483    /2/
1484  |1:
1485    #relevant
1486    cases (nat_of_bitvector_aux_injective … relevant)
1487    #_ #l_r_tl_refl destruct /2/
1488  |2,3:
1489    #relevant
1490    cases (nat_of_bitvector_aux_injective … relevant)
1491    #absurd destruct(absurd)
1492  ]
1493qed.
1494
1495lemma BitVector_cons_injective:
1496  ∀n: nat.
1497  ∀l_hd, r_hd: bool.
1498  ∀l_tl, r_tl: BitVector n.
1499    l_hd = r_hd → l_tl = r_tl → l_hd:::l_tl = r_hd:::r_tl.
1500  #l #l_hd #r_hd #l_tl #r_tl
1501  #l_refl #r_refl destruct %
1502qed.
1503
1504lemma refl_nat_of_bitvector_to_refl:
1505  ∀n: nat.
1506  ∀l, r: BitVector n.
1507    nat_of_bitvector n l = nat_of_bitvector n r → l = r.
1508  #n
1509  elim n
1510  [1:
1511    #l #r
1512    >(BitVector_O l)
1513    >(BitVector_O r)
1514    #_ %
1515  |2:
1516    #n' #inductive_hypothesis #l #r
1517    lapply (BitVector_Sn ? l) #l_hypothesis
1518    lapply (BitVector_Sn ? r) #r_hypothesis
1519    cases l_hypothesis #l_hd #l_tail_hypothesis
1520    cases r_hypothesis #r_hd #r_tail_hypothesis
1521    cases l_tail_hypothesis #l_tl #l_hd_tl_refl
1522    cases r_tail_hypothesis #r_tl #r_hd_tl_refl
1523    destruct #cons_refl
1524    cases (nat_of_bitvector_destruct n' l_hd r_hd l_tl r_tl cons_refl)
1525    #hd_refl #tl_refl
1526    @BitVector_cons_injective try assumption
1527    @inductive_hypothesis assumption
1528  ]
1529qed.
Note: See TracBrowser for help on using the repository browser.