source: src/ASM/ASMCosts.ma @ 1938

Last change on this file since 1938 was 1938, checked in by sacerdot, 8 years ago

Definitions moved to the right places, now everything compiles again.

File size: 35.4 KB
RevLine 
[1486]1include "ASM/ASM.ma".
2include "ASM/Arithmetic.ma".
3include "ASM/Fetch.ma".
4include "ASM/Interpret.ma".
[1560]5include "common/StructuredTraces.ma".
[1648]6
[1938]7definition ASM_abstract_status: ∀code_memory. BitVectorTrie costlabel 16 → abstract_status ≝
8  λcode_memory.
9  λcost_labels.
10    mk_abstract_status
11      (Status code_memory)
12      (λs,s'. (execute_1 … s) = s')
13      word_deqset
14      (program_counter …)
15      (λs,class. ASM_classify … s = class)
16      (current_instruction_label code_memory cost_labels)
17      (next_instruction_properly_relates_program_counters code_memory)
18      ?.
19  cases daemon (* XXX: is final predicate *)
20qed.
21
[1929]22definition trace_any_label_length ≝
[1919]23  λcode_memory: BitVectorTrie Byte 16.
24  λcost_labels: BitVectorTrie costlabel 16.
25  λtrace_ends_flag: trace_ends_with_ret.
26  λstart_status: Status code_memory.
27  λfinal_status: Status code_memory.
28  λthe_trace: trace_any_label (ASM_abstract_status code_memory cost_labels) trace_ends_flag start_status final_status.
29    as_trace_any_label_length' … the_trace.
[1911]30
[1921]31let rec all_program_counter_list
32  (n: nat)
33    on n ≝
34  match n with
35  [ O ⇒ [ ]
36  | S n' ⇒ (bitvector_of_nat 16 n')::(all_program_counter_list n')
37  ].
38
39lemma all_program_counter_list_bound_eq:
40  ∀bound: nat.
41    |all_program_counter_list bound| = bound.
42  #bound elim bound try %
43  #bound' #inductive_hypothesis normalize
44  >inductive_hypothesis %
45qed.
46
47lemma mem_all_program_counter_list_lt_bound:
48  ∀bound: nat.
49  ∀bound_proof: bound ≤ 2^16.
50  ∀e: Word.
51    memb word_deqset e (all_program_counter_list bound) = true →
52      nat_of_bitvector … e < bound.
53  #bound elim bound
54  [1:
55    #bound_proof #e
56    normalize #absurd destruct(absurd)
57  |2:
58    #bound' #inductive_hypothesis
59    #bound_proof #e
60    change with (if eq_bv ??? then ? else ? = ? → ?)
61    @eq_bv_elim
62    [1:
63      #eq_assm
64      normalize nodelta destruct #_
65      >nat_of_bitvector_bitvector_of_nat_inverse try assumption
66      normalize %
67    |2:
68      #neq_assm normalize nodelta
69      #memb_assm %2 @inductive_hypothesis
70      try assumption
71      @(transitive_le bound' (S bound'))
72      try assumption %2 %
73    ]
74  ]
75qed.
76
77lemma lt_bound_mem_all_program_counter_list:
78  ∀bound: nat.
79  ∀bound_proof: bound ≤ 2^16.
80  ∀e: Word.
81    nat_of_bitvector … e < bound →
82      memb word_deqset e (all_program_counter_list bound) = true.
83  #bound elim bound
84  [1:
85    #bound_proof #e normalize
86    #absurd cases (lt_to_not_zero … absurd)
87  |2:
88    #bound' #inductive_hypothesis
89    #bound_proof #e
90    change with (? → if eq_bv ??? then ? else ? = ?)
91    #assm
92    cases (le_to_or_lt_eq … (nat_of_bitvector 16 e) bound' ?)
93    [1:
94      #e_lt_assm
95      @eq_bv_elim
96      [1:
97        #eq_assm normalize nodelta %
98      |2:
99        #neq_assm normalize nodelta
100        @inductive_hypothesis try assumption
101        @(transitive_le bound' (S bound')) try assumption
102        %2 %
103      ]
104    |2:
105      #relevant >eq_eq_bv normalize nodelta try %
106      destruct >bitvector_of_nat_inverse_nat_of_bitvector %
107    |3:
108      normalize in assm;
109      @le_S_S_to_le assumption
110    ]
111  ]
112qed.
113
114include alias "arithmetics/nat.ma".
115
116lemma execute_1_and_program_counter_after_other_in_lockstep:
117  ∀code_memory: BitVectorTrie Byte 16.
118  ∀start_status: Status code_memory.
119    ASM_classify code_memory start_status = cl_other →
120      let 〈instruction, pc, ticks〉 ≝ fetch code_memory (program_counter … start_status) in
121        program_counter ? ? (execute_1 … start_status) =
122          program_counter_after_other pc instruction.
123  #code_memory #start_status #classify_assm
124  whd in match execute_1; normalize nodelta
125  cases (execute_1' code_memory start_status) #the_status
126  * #_ whd in classify_assm:(??%?); whd in match (current_instruction ??) in classify_assm;
127  cases (fetch ? ?) in classify_assm; * #instruction #pc #ticks
128  #classify_assm #classify_assm' @classify_assm' assumption
129qed-.
130
[1929]131lemma nat_of_bitvector_lt_bound:
132  ∀n: nat.
133  ∀b: BitVector n.
134    nat_of_bitvector n b < 2^n.
135  #n #b cases daemon
136qed.
[1921]137
138lemma sublist_tal_pc_list_all_program_counter_list:
139  ∀code_memory: BitVectorTrie Byte 16.
140  ∀cost_labels: BitVectorTrie costlabel 16.
141  ∀start, final: Status code_memory.
142  ∀trace_ends_flag.
143  ∀the_trace: trace_any_label (ASM_abstract_status code_memory cost_labels) trace_ends_flag start final.
[1929]144    sublist ? (tal_pc_list … the_trace) (all_program_counter_list (2^16)).
145  #code_memory #cost_labels #start #final #trace_ends_flag #the_trace
[1921]146  whd in match (sublist ???); #pc #memb_assm
[1929]147  @lt_bound_mem_all_program_counter_list try %
148  @nat_of_bitvector_lt_bound
[1921]149qed.
150
151corollary tal_pc_list_length_leq_total_program_size:
152  ∀code_memory: BitVectorTrie Byte 16.
153  ∀cost_labels: BitVectorTrie costlabel 16.
154  ∀start, final: Status code_memory.
155  ∀trace_ends_flag.
156  ∀the_trace: trace_any_label (ASM_abstract_status code_memory cost_labels) trace_ends_flag start final.
157  ∀unrepeating_witness: tal_unrepeating (ASM_abstract_status code_memory cost_labels) trace_ends_flag start final the_trace.
[1929]158    |tal_pc_list … the_trace| ≤ 2^16.
159  #code_memory #cost_labels #start #final #trace_ends_flag #the_trace #unrepeating_witness
160  <(all_program_counter_list_bound_eq (2^16))
[1921]161  @sublist_length
162  [1:
163    @tal_unrepeating_uniqueb
164    assumption
165  |2:
166    @sublist_tal_pc_list_all_program_counter_list
167    assumption
168  ]
169qed.
170
[1658]171let rec compute_paid_trace_any_label
[1669]172  (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
173    (trace_ends_flag: trace_ends_with_ret) (start_status: Status code_memory)
174      (final_status: Status code_memory)
175        (the_trace: trace_any_label (ASM_abstract_status code_memory cost_labels) trace_ends_flag start_status final_status)
[1658]176       on the_trace: nat ≝
177  match the_trace with
[1669]178  [ tal_base_not_return the_status _ _ _ _ ⇒ current_instruction_cost … the_status
179  | tal_base_return the_status _ _ _ ⇒ current_instruction_cost … the_status
[1902]180  | tal_base_call pre_fun_call start_fun_call final _ _ _ _ call_trace ⇒ current_instruction_cost … pre_fun_call
[1658]181  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
[1902]182     _ _ _ call_trace _ final_trace ⇒
[1669]183      let current_instruction_cost ≝ current_instruction_cost … pre_fun_call in
184      let final_trace_cost ≝ compute_paid_trace_any_label … cost_labels end_flag … final_trace in
[1658]185        current_instruction_cost + final_trace_cost
186  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
[1669]187      let current_instruction_cost ≝ current_instruction_cost … status_pre in
[1658]188      let tail_trace_cost ≝
[1669]189       compute_paid_trace_any_label … cost_labels end_flag
[1658]190        status_init status_end tail_trace
191      in
192        current_instruction_cost + tail_trace_cost
193  ].
194
195definition compute_paid_trace_label_label ≝
[1669]196  λcode_memory: BitVectorTrie Byte 16.
197  λcost_labels: BitVectorTrie costlabel 16.
[1658]198  λtrace_ends_flag: trace_ends_with_ret.
[1669]199  λstart_status: Status code_memory.
200  λfinal_status: Status code_memory.
201  λthe_trace: trace_label_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
[1658]202  match the_trace with
203  [ tll_base ends_flag initial final given_trace labelled_proof ⇒
204      compute_paid_trace_any_label … given_trace
205  ].
206
[1684]207lemma trace_compute_paid_trace_cl_other:
[1669]208  ∀code_memory' : (BitVectorTrie Byte 16).
209  ∀program_counter' : Word.
210  ∀cost_labels : (BitVectorTrie costlabel 16).
211  ∀program_size' : ℕ.
212  ∀ticks : ℕ.
213  ∀instruction : instruction.
214  ∀program_counter'' : Word.
215  ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch code_memory' program_counter').
[1910]216  let program_counter''' ≝ program_counter_after_other program_counter'' instruction in
[1669]217  ∀start_status : (Status code_memory').
218  ∀final_status : (Status code_memory').
219  ∀trace_ends_flag : trace_ends_with_ret.
220  ∀the_trace : (trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status).
221  ∀program_counter_refl : (program_counter' = program_counter (BitVectorTrie Byte 16) code_memory' start_status).
[1929]222  ∀size_invariant : trace_any_label_length code_memory' cost_labels trace_ends_flag start_status final_status the_trace ≤S program_size'.
[1669]223  ∀classify_assm: ASM_classify0 instruction = cl_other.
224  ∀pi1 : ℕ.
[1910]225   (if match lookup_opt costlabel 16 program_counter''' cost_labels with 
[1669]226         [None ⇒ true
227         |Some _ ⇒ false
228         ] 
229    then
230      ∀start_status0:Status code_memory'.
231      ∀final_status0:Status code_memory'.
232      ∀trace_ends_flag0:trace_ends_with_ret.
233      ∀the_trace0:trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag0 start_status0 final_status0.
[1929]234        trace_any_label_length code_memory' cost_labels trace_ends_flag0
[1912]235          start_status0 final_status0 the_trace0 ≤ program_size' →
[1910]236        program_counter''' = program_counter (BitVectorTrie Byte 16) code_memory' start_status0 →
[1901]237                  pi1
[1669]238                    =compute_paid_trace_any_label code_memory' cost_labels
239                     trace_ends_flag0 start_status0 final_status0 the_trace0
240    else (pi1=O) )
[1906]241   → ticks+pi1
[1669]242     =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag
243      start_status final_status the_trace.
[1929]244  #code_memory' #program_counter' #cost_labels #program_size' #ticks #instruction
245  #program_counter'' #FETCH #start_status #final_status #trace_ends_flag #the_trace
246  #program_counter_refl #size_invariant #classify_assm #recursive_block_cost
[1692]247  #recursive_assm
248  @(trace_any_label_inv_ind … the_trace)
[1669]249    [5:
250      #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
251      #classifier_assm #costed_assm #trace_ends_refl #start_status_refl #final_status_refl
252      #the_trace_refl
253      destruct
254      whd in match (trace_any_label_length … (tal_step_default …));
255      whd in match (compute_paid_trace_any_label … (tal_step_default …));
256      whd in costed_assm:(?%);
257      generalize in match costed_assm;
258      generalize in match (refl … (lookup_opt … (program_counter … (execute_1 … status_pre)) cost_labels));
[1927]259      whd in match (as_label ??);
[1669]260      generalize in match (lookup_opt … (program_counter … (execute_1 … status_pre)) cost_labels)
[1927]261        in ⊢ (??%? → % → ?);
[1669]262      #lookup_assm cases lookup_assm
263      [1:
[1910]264        #None_lookup_opt_assm normalize nodelta #_
[1669]265        generalize in match recursive_assm;
[1910]266        lapply (execute_1_and_program_counter_after_other_in_lockstep code_memory' ? classifier_assm)
267        <FETCH normalize nodelta #rewrite_assm >rewrite_assm in None_lookup_opt_assm;
268        #None_lookup_opt_assm <None_lookup_opt_assm
269        normalize nodelta #new_recursive_assm
270        cases(new_recursive_assm (execute_1 code_memory' status_pre) status_end
[1929]271          end_flag trace_any_label ? ?) try (>rewrite_assm %)
[1910]272        whd in match (current_instruction_cost … status_pre);
273        cut(ticks = \snd (fetch code_memory'
274           (program_counter (BitVectorTrie Byte 16) code_memory' status_pre)))
[1929]275        [1,3:
[1910]276          <FETCH %
[1669]277        |2:
[1912]278          #ticks_refl_assm
279          >ticks_refl_assm %
[1910]280        |4:
281          #ticks_refl_assm
[1912]282          change with (S ? ≤ S ?) in size_invariant;
283          lapply (le_S_S_to_le … size_invariant) #assm
284          assumption
[1669]285        ]
286      |2:
[1927]287        #costlabel #Some_lookup_opt_assm <Some_lookup_opt_assm
288        #absurd
289        cases (not_Some_neq_None_to_False ?? absurd)
[1669]290      ]
291    |1:
292      #status_start #status_final #execute_assm #classifier_assm #costed_assm
293      #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
294      destruct
295      whd in match (trace_any_label_length … (tal_base_not_return …));
296      whd in match (compute_paid_trace_any_label … (tal_base_not_return …));
297      whd in costed_assm;
298      generalize in match costed_assm;
299      generalize in match (refl … (lookup_opt … (program_counter … (execute_1 … status_start)) cost_labels));
[1927]300      whd in match (as_label ??);
[1669]301      generalize in match (lookup_opt … (program_counter … (execute_1 code_memory' status_start)) cost_labels)
[1927]302        in ⊢ (??%? → % → ?);
[1669]303      #lookup_assm cases lookup_assm
304      [1:
[1927]305        #None_lookup_opt_assm
306        #absurd @⊥ cases absurd -absurd #absurd @absurd %
[1669]307      |2:
308        #costlabel #Some_lookup_opt_assm normalize nodelta #ignore
309        generalize in match recursive_assm;
[1910]310        cases classifier_assm
[1669]311        [1:
[1910]312          whd in ⊢ (% → ?);
313          whd in ⊢ (??%? → ?);
314          whd in match (current_instruction code_memory' status_start);
315          <FETCH generalize in match classify_assm;
316          cases instruction
317          [8:
318            #preinstruction normalize nodelta
319            whd in match ASM_classify0; normalize nodelta
320            #contradiction >contradiction #absurd destruct(absurd)
[1710]321          ]
[1910]322          try(#addr1 #addr2 normalize nodelta #ignore #absurd destruct(absurd))
323          try(#addr normalize nodelta #ignore #absurd destruct(absurd))
324          normalize in ignore; destruct(ignore)
[1669]325        |2:
[1910]326          -classifier_assm #classifier_assm
327          lapply (execute_1_and_program_counter_after_other_in_lockstep code_memory' ? classifier_assm)
328          <FETCH normalize nodelta #rewrite_assm >rewrite_assm in Some_lookup_opt_assm;
329          #Some_lookup_opt_assm <Some_lookup_opt_assm
[1906]330          normalize nodelta #new_recursive_assm >new_recursive_assm
331          cut(ticks = \snd (fetch code_memory'
332             (program_counter (BitVectorTrie Byte 16) code_memory' status_start)))
[1669]333          [1:
[1906]334            <FETCH %
[1669]335          |2:
[1906]336            #ticks_refl_assm >ticks_refl_assm
337            <plus_n_O %
[1669]338          ]
339        ]
340      ]
341    |2:
342      #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm
343      #start_status_refl #final_status_refl #the_trace_assm destruct @⊥
344    |3:
345      #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
346      #classifier_assm #after_return_assm #trace_label_return #costed_assm
347      #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
348      destruct @⊥
[1684]349    |4:
350      #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
351      #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
352      #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
353      #final_status_refl #the_trace_refl destruct @⊥
[1669]354    ]
[1684]355  change with (ASM_classify0 ? = ?) in classifier_assm;
356  whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
357  whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
358  <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd)
[1910]359qed.
[1669]360
[1684]361lemma trace_compute_paid_trace_cl_jump:
362  ∀code_memory': BitVectorTrie Byte 16.
363  ∀program_counter': Word.
364  ∀cost_labels: BitVectorTrie costlabel 16.
365  ∀first_time_around: bool.
366  ∀program_size': ℕ.
367  ∀ticks: ℕ.
368  ∀instruction: instruction.
369  ∀program_counter'': Word.
370  ∀FETCH: 〈instruction,program_counter'',ticks〉 = fetch code_memory' program_counter'.
371  ∀start_status: (Status code_memory').
372  ∀final_status: (Status code_memory').
373  ∀trace_ends_flag: trace_ends_with_ret.
374  ∀the_trace: (trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status).
375  ∀program_counter_refl: (program_counter' = program_counter (BitVectorTrie Byte 16) code_memory' start_status).
376  ∀classify_assm: ASM_classify0 instruction = cl_jump.
[1906]377    ticks
[1684]378     =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag
[1691]379      start_status final_status the_trace.
[1929]380  #code_memory' #program_counter' #cost_labels #first_time_around
[1912]381  #program_size' #ticks #instruction #program_counter'' #FETCH
[1691]382  #start_status #final_status
[1684]383  #trace_ends_flag #the_trace #program_counter_refl #classify_assm
384  @(trace_any_label_inv_ind … the_trace)
[1692]385  [5:
386    #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
387    #classifier_assm #costed_assm #trace_ends_refl #start_status_refl #final_status_refl
388    #the_trace_refl destruct @⊥
389  |1:
390    #status_start #status_final #execute_assm #classifier_assm #costed_assm
[1684]391    #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
392    destruct
393    whd in match (trace_any_label_length … (tal_base_not_return …));
[1906]394    whd in match (compute_paid_trace_any_label … (tal_base_not_return …));
395    <FETCH %
[1684]396  |2:
[1692]397    #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm
398    #start_status_refl #final_status_refl #the_trace_assm destruct @⊥
[1684]399  |3:
400    #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
401    #classifier_assm #after_return_assm #trace_label_return #costed_assm
[1692]402    #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
[1684]403    destruct @⊥
404  |4:
405    #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
406    #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
[1692]407    #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
[1684]408    #final_status_refl #the_trace_refl destruct @⊥
409  ]
410  change with (ASM_classify0 ? = ?) in classifier_assm;
411  whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
412  whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
413  <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd)
414qed.
415
416lemma trace_compute_paid_trace_cl_call:
417  ∀code_memory' : (BitVectorTrie Byte 16).
418  ∀program_counter' : Word.
419  ∀cost_labels : (BitVectorTrie costlabel 16).
420  ∀program_size' : ℕ.
421  ∀ticks : ℕ.
422  ∀instruction : instruction.
423  ∀program_counter'' : Word.
424  ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch code_memory' program_counter').
425  ∀start_status : (Status code_memory').
426  ∀final_status : (Status code_memory').
427  ∀trace_ends_flag : trace_ends_with_ret.
428  ∀the_trace : (trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status).
429  ∀program_counter_refl : (program_counter' = program_counter (BitVectorTrie Byte 16) code_memory' start_status).
[1929]430  ∀size_invariant : trace_any_label_length code_memory' cost_labels trace_ends_flag start_status final_status the_trace ≤S program_size'.
[1684]431  ∀classify_assm: ASM_classify0 instruction = cl_call.
[1692]432  (∀pi1:ℕ
433  .if match lookup_opt costlabel 16 program_counter'' cost_labels with 
434      [None ⇒ true | Some _ ⇒ false] 
[1684]435   then (∀start_status0:Status code_memory'
436             .∀final_status0:Status code_memory'
437              .∀trace_ends_flag0:trace_ends_with_ret
438               .∀the_trace0:trace_any_label
439                                        (ASM_abstract_status code_memory' cost_labels)
[1912]440                                        trace_ends_flag0 start_status0 final_status0.
[1929]441                trace_any_label_length code_memory' cost_labels trace_ends_flag0
[1912]442                  start_status0 final_status0 the_trace0
443                   ≤ program_size' →
444                program_counter''
[1684]445                 =program_counter (BitVectorTrie Byte 16) code_memory' start_status0
[1906]446                 → pi1
[1684]447                   =compute_paid_trace_any_label code_memory' cost_labels
448                    trace_ends_flag0 start_status0 final_status0 the_trace0) 
449   else (pi1=O) 
[1906]450   → ticks+pi1
[1684]451     =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag
[1692]452      start_status final_status the_trace).
[1929]453  #code_memory' #program_counter' #cost_labels #program_size'
[1912]454  #ticks #instruction #program_counter'' #FETCH
[1691]455  #start_status #final_status #trace_ends_flag
[1912]456  #the_trace #program_counter_refl #size_invariant #classify_assm
457  #recursive_block_cost #recursive_assm
[1684]458  @(trace_any_label_inv_ind … the_trace)
[1692]459  [5:
460    #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
461    #classifier_assm #costed_assm #trace_ends_refl #start_status_refl #final_status_refl
462    #the_trace_refl destruct @⊥
463  |1:
464    #status_start #status_final #execute_assm #classifier_assm #costed_assm
465    #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
466    destruct @⊥
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
[1902]473    #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
[1692]474    destruct
475    whd in match (trace_any_label_length … (tal_base_call …));
476    whd in match (compute_paid_trace_any_label … (tal_base_call …));
477    whd in costed_assm;
478    generalize in match costed_assm;
479    generalize in match (refl … (lookup_opt … (program_counter … status_final) cost_labels));
[1927]480    whd in match (as_label ??);
[1692]481    generalize in match (lookup_opt … (program_counter … status_final) cost_labels)
[1927]482      in ⊢ (??%? → % → ?);
[1692]483    #lookup_assm cases lookup_assm
484    [1:
485      #None_lookup_opt normalize nodelta #absurd cases absurd
[1927]486      -absurd #absurd @⊥ @absurd %
[1692]487    |2:
488      #costlabel #Some_lookup_opt normalize nodelta #ignore
489      generalize in match recursive_assm;
490      cut(program_counter'' = (program_counter (BitVectorTrie Byte 16) code_memory' status_final))
491      [1:
[1902]492        generalize in match after_return_assm;
[1901]493        whd in ⊢ (% → ?); <FETCH normalize nodelta #relevant <relevant %
[1692]494      |2:
495        #program_counter_assm >program_counter_assm <Some_lookup_opt
[1906]496        normalize nodelta #new_recursive_assm >new_recursive_assm
497        cut(ticks = \snd (fetch code_memory' (program_counter (BitVectorTrie Byte 16) code_memory' status_pre_fun_call)))
498        [1:
499          <FETCH %
[1692]500        |2:
[1906]501          #ticks_refl_assm >ticks_refl_assm
502          <plus_n_O %
[1692]503        ]
504      ]
505    ]
506  |4:
507    #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
508    #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
[1902]509    #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
510    #final_status_refl #the_trace_refl
[1901]511    generalize in match execute_assm; destruct #execute_assm
[1692]512    whd in match (trace_any_label_length … (tal_step_call …));
513    whd in match (compute_paid_trace_any_label … (tal_step_call …));
514    whd in costed_assm:(?%);
515    generalize in match costed_assm;
516    generalize in match (refl … (lookup_opt … (program_counter … status_after_fun_call) cost_labels));
[1927]517    whd in match (as_label ??);
[1692]518    generalize in match (lookup_opt … (program_counter … status_after_fun_call) cost_labels)
[1927]519      in ⊢ (??%? → % → ?);
[1692]520    #lookup_assm cases lookup_assm
521    [1:
522      #None_lookup_opt_assm normalize nodelta #ignore
523      generalize in match recursive_assm;
524      cut(program_counter'' = program_counter … status_after_fun_call)
525      [1:
[1902]526        generalize in match after_return_assm;
[1901]527        whd in ⊢ (% → ?); <FETCH normalize nodelta #relevant >relevant %
[1692]528      |2:
529        #program_counter_refl >program_counter_refl <None_lookup_opt_assm
[1906]530        normalize nodelta #new_recursive_assm
[1912]531        cases (new_recursive_assm … trace_any_label ? ?)
[1906]532        [1:
533          @plus_right_monotone whd in ⊢ (???%); <FETCH %
534        |2:
[1919]535          @le_S_S_to_le @size_invariant
[1912]536        |3:
[1692]537          %
538        ]
539      ]
540    |2:
[1927]541      #cost_label #Some_lookup_opt_assm #absurd
542      cases (not_Some_neq_None_to_False ?? absurd)
[1692]543    ]
544  ]
545  try (change with (ASM_classify0 ? = ? ∨ ASM_classify0 ? = ?) in classifier_assm;)
546  try (change with (ASM_classify0 ? = ?) in classifier_assm;)
547  whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
548  whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
549  <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd) cases absurd
550  #absurd destruct(absurd)
[1684]551qed.
552
[1710]553lemma trace_compute_paid_trace_cl_return:
554  ∀code_memory' : (BitVectorTrie Byte 16).
555  ∀program_counter' : Word.
556  ∀cost_labels : (BitVectorTrie costlabel 16).
557  ∀program_size' : ℕ.
558  ∀ticks : ℕ.
559  ∀instruction : instruction.
560  ∀program_counter'' : Word.
561  ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch code_memory' program_counter').
562  ∀start_status : (Status code_memory').
563  ∀final_status : (Status code_memory').
564  ∀trace_ends_flag : trace_ends_with_ret.
565  ∀the_trace : (trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status).
566  ∀program_counter_refl : (program_counter' = program_counter (BitVectorTrie Byte 16) code_memory' start_status).
567  ∀classify_assm: ASM_classify0 instruction = cl_return.
[1906]568    ticks
[1710]569     =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag
570      start_status final_status the_trace.
[1929]571  #code_memory' #program_counter' #cost_labels #program_size'
[1912]572  #ticks #instruction #program_counter'' #FETCH
[1710]573  #start_status #final_status #trace_ends_flag
574  #the_trace #program_counter_refl #classify_assm
575  @(trace_any_label_inv_ind … the_trace)
576  [1:
577    #start_status' #final_status' #execute_assm #classifier_assm #costed_assm
578    #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
579    destruct @⊥
580  |2:
581    #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_flag_refl
582    #start_status_refl #final_status_refl #the_trace_refl destruct
583    whd in match (trace_any_label_length … (tal_base_return …));
[1906]584    whd in match (compute_paid_trace_any_label … (tal_base_return …));
585    <FETCH %
[1710]586  |3:
587    #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
588    #classifier_assm #after_return_assm #trace_label_return #costed_assm
589    #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
590    destruct @⊥
591  |4:
592    #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
593    #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
594    #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
595    #final_status_refl #the_trace_refl
596    destruct @⊥
597  |5:
598    #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
599    #classifier_assm #costed_assm #trace_ends_flag_refl #start_status_refl
600    #final_status_refl #the_trace_refl destruct @⊥
601  ]
602  try (change with (ASM_classify0 ? = ? ∨ ASM_classify0 ? = ?) in classifier_assm;)
603  try (change with (ASM_classify0 ? = ?) in classifier_assm;)
604  whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
605  whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
606  <FETCH in classifier_assm; >classify_assm
607  #absurd try (destruct(absurd))
608  cases absurd
609  #absurd destruct(absurd)
610qed.
[1912]611
612lemma trace_any_label_length_leq_0_to_False:
613  ∀code_memory: BitVectorTrie Byte 16.
614  ∀cost_labels: BitVectorTrie costlabel 16.
615  ∀trace_ends_flag: trace_ends_with_ret.
616  ∀start_status: Status code_memory.
617  ∀final_status: Status code_memory.
618  ∀the_trace.
[1929]619  trace_any_label_length code_memory cost_labels trace_ends_flag start_status
[1912]620    final_status the_trace ≤ 0 → False.
621  #code_memory #cost_labels #trace_ends_flag #start_status #final_status
622  #the_trace
623  cases the_trace /2/
624qed.
[1710]625     
[1650]626let rec block_cost'
[1911]627  (code_memory': BitVectorTrie Byte 16) (program_counter': Word)
[1929]628    (program_size: nat) (cost_labels: BitVectorTrie costlabel 16)
629      (first_time_around: bool)
630        on program_size:
[1658]631          Σcost_of_block: nat.
[1669]632          if (match lookup_opt … program_counter' cost_labels with [ None ⇒ true | _ ⇒ first_time_around ]) then
633            ∀start_status: Status code_memory'.
634            ∀final_status: Status code_memory'.
[1658]635            ∀trace_ends_flag.
[1669]636            ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
[1929]637              trace_any_label_length … the_trace ≤ program_size →
[1669]638              program_counter' = program_counter … start_status →
[1906]639                cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace
[1669]640          else
641            (cost_of_block = 0) ≝
[1911]642  match program_size return λx. x = program_size → ? with
643  [ O ⇒ λbase_case. 0 (* XXX: dummy to be inserted here *)
644  | S program_size' ⇒ λstep_case.
[1663]645    let 〈instruction, program_counter'', ticks〉 as FETCH ≝ fetch code_memory' program_counter' in
[1650]646    let to_continue ≝
[1669]647      match lookup_opt … program_counter' cost_labels with
[1650]648      [ None ⇒ true
649      | Some _ ⇒ first_time_around
650      ]
651    in
[1669]652      ((if to_continue then
653       pi1 … (match instruction return λx. x = instruction → ? with
[1663]654        [ RealInstruction real_instruction ⇒ λreal_instruction_refl.
655          match real_instruction return λx. x = real_instruction →
656          Σcost_of_block: nat.
[1669]657            ∀start_status: Status code_memory'.
658            ∀final_status: Status code_memory'.
[1663]659            ∀trace_ends_flag.
[1669]660            ∀the_trace: trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status.
[1929]661              trace_any_label_length … the_trace ≤ S program_size' →
[1669]662              program_counter' = program_counter … start_status →
[1906]663                cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace with
[1663]664          [ RET                    ⇒ λinstr. ticks
[1710]665          | RETI                   ⇒ λinstr. ticks
[1663]666          | JC   relative          ⇒ λinstr. ticks
667          | JNC  relative          ⇒ λinstr. ticks
668          | JB   bit_addr relative ⇒ λinstr. ticks
669          | JNB  bit_addr relative ⇒ λinstr. ticks
670          | JBC  bit_addr relative ⇒ λinstr. ticks
671          | JZ   relative          ⇒ λinstr. ticks
672          | JNZ  relative          ⇒ λinstr. ticks
673          | CJNE src_trgt relative ⇒ λinstr. ticks
674          | DJNZ src_trgt relative ⇒ λinstr. ticks
675          | _                      ⇒ λinstr.
[1929]676              ticks + block_cost' code_memory' program_counter'' program_size' cost_labels false
[1663]677          ] (refl …)
678        | ACALL addr     ⇒ λinstr.
[1929]679            ticks + block_cost' code_memory' program_counter'' program_size' cost_labels false
[1909]680        | AJMP  addr     ⇒ λinstr.
[1910]681          let jump_target ≝ compute_target_of_unconditional_jump program_counter'' instruction in
[1929]682            ticks + block_cost' code_memory' jump_target program_size' cost_labels false
[1663]683        | LCALL addr     ⇒ λinstr.
[1929]684            ticks + block_cost' code_memory' program_counter'' program_size' cost_labels false
[1910]685        | LJMP  addr     ⇒ λinstr.
686          let jump_target ≝ compute_target_of_unconditional_jump program_counter'' instruction in
[1929]687            ticks + block_cost' code_memory' jump_target program_size' cost_labels false
[1910]688        | SJMP  addr     ⇒ λinstr.
689          let jump_target ≝ compute_target_of_unconditional_jump program_counter'' instruction in
[1929]690            ticks + block_cost' code_memory' jump_target program_size' cost_labels false
[1663]691        | JMP   addr     ⇒ λinstr. (* XXX: actually a call due to use with fptrs *)
[1929]692            ticks + block_cost' code_memory' program_counter'' program_size' cost_labels false
[1663]693        | MOVC  src trgt ⇒ λinstr.
[1929]694            ticks + block_cost' code_memory' program_counter'' program_size' cost_labels false
[1669]695        ] (refl …))
[1650]696      else
[1669]697        0)
698      : Σcost_of_block: nat.
699          match (match lookup_opt … program_counter' cost_labels with [ None ⇒ true | _ ⇒ first_time_around ]) with
700          [ true ⇒
701            ∀start_status: Status code_memory'.
702            ∀final_status: Status code_memory'.
703            ∀trace_ends_flag.
704            ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
[1929]705              trace_any_label_length … the_trace ≤ S program_size' →
[1669]706              program_counter' = program_counter … start_status →
[1906]707                cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace
[1669]708          | false ⇒
709            (cost_of_block = 0)
710          ])
[1911]711  ] (refl …).
[1910]712  [2:
713    change with (if to_continue then ? else (? = 0))
714    >p in ⊢ (match % return ? with [ _ ⇒ ? | _ ⇒ ? ]); normalize nodelta
715    @pi2
716  |1:
[1911]717    destruct
[1912]718    cases (lookup_opt ????) normalize nodelta
[1911]719    [1:
[1912]720      #start_status #final_status #trace_ends_flag #the_trace
721      #absurd
722      cases (trace_any_label_length_leq_0_to_False … absurd)
[1911]723    |2:
[1912]724      #cost cases first_time_around normalize nodelta try %
725      #start_status #final_status #trace_ends_flag #the_trace #absurd
726      cases (trace_any_label_length_leq_0_to_False … absurd)
[1911]727    ]
[1669]728  |3:
[1684]729    change with (if to_continue then ? else (0 = 0))
730    >p normalize nodelta %
[1929]731  |5,6:
[1912]732    #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl
[1929]733    @(trace_compute_paid_trace_cl_return … program_size' … FETCH … the_trace program_counter_refl)
[1710]734    destruct %
[1929]735  |42,46,47:
[1912]736    #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl
[1929]737    cases(block_cost' ?????) -block_cost'
738    @(trace_compute_paid_trace_cl_call … program_size' … FETCH … the_trace program_counter_refl size_invariant)
[1691]739    destruct %
[1929]740  |43,44,45: (* XXX: unconditional jumps *)
[1912]741    #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl
[1929]742    cases (block_cost' ?????) -block_cost'
743    lapply (trace_compute_paid_trace_cl_other … program_size' … FETCH … the_trace program_counter_refl size_invariant)
744    whd in match (program_counter_after_other ??); normalize nodelta destruct
745    whd in match (is_unconditional_jump ?); normalize nodelta #assm @assm %
746  |24,25,26,27,28,29,30,31,32:
[1912]747    #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl
[1929]748    @(trace_compute_paid_trace_cl_jump … first_time_around program_size' … FETCH … the_trace program_counter_refl)
[1691]749    destruct %
[1929]750  |*:
[1912]751    #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl
[1929]752    cases(block_cost' ?????) -block_cost'
753    lapply (trace_compute_paid_trace_cl_other … program_size' … FETCH … the_trace program_counter_refl size_invariant)     
754    destruct #assm @assm %
[1910]755  ]
[1642]756qed.
757
[1693]758definition block_cost:
759    ∀code_memory': BitVectorTrie Byte 16.
760    ∀program_counter': Word.
761    ∀cost_labels: BitVectorTrie costlabel 16.
762      Σcost_of_block: nat.
763        ∀start_status: Status code_memory'.
764        ∀final_status: Status code_memory'.
765        ∀trace_ends_flag.
766        ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
[1921]767        ∀unrepeating_witness: tal_unrepeating (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status the_trace.
[1693]768          program_counter' = program_counter … start_status →
[1906]769            cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace ≝
[1650]770  λcode_memory: BitVectorTrie Byte 16.
771  λprogram_counter: Word.
[1929]772  λcost_labels: BitVectorTrie costlabel 16. ?.
773  cases(block_cost' code_memory program_counter (2^16) cost_labels true)
[1913]774  #cost_of_block #block_cost_hyp
775  %{cost_of_block}
776  cases(lookup_opt … cost_labels) in block_cost_hyp;
777  [2: #cost_label] normalize nodelta
[1929]778  #hyp #start_status #final_status #trace_ends_flag #the_trace #unrepeating_witness
[1921]779  @hyp @tal_pc_list_length_leq_total_program_size try assumption
[1645]780qed.
Note: See TracBrowser for help on using the repository browser.