source: src/ASM/ASMCosts.ma @ 2531

Last change on this file since 2531 was 2531, checked in by mckinna, 7 years ago

Trivial tweaks.

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