source: src/ASM/ASMCosts.ma @ 1910

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

Finished proof modulo termination argument

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