source: src/ASM/ASMCosts.ma @ 1919

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

Fixes to get everything compiling again

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