source: src/ASM/ASMCosts.ma @ 1911

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

Changed statement of block_cost' to start on new termination argument

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