Changeset 1929 for src/ASM/ASMCosts.ma


Ignore:
Timestamp:
May 9, 2012, 2:44:39 PM (8 years ago)
Author:
mulligan
Message:

Simplified proof by removing most of the invariants on the statements all together (reachable_program_counter, good_program), and fixing the size of the total_program_size to be constantly 216.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r1928 r1929  
    44include "ASM/Interpret.ma".
    55include "common/StructuredTraces.ma".
    6 
    7 (* XXX: alternative approach:
    8  * R : Word → Prop
    9  * TPS ≝ |R|
    10  * GP : ∀a. R(a) → R(next(a))
    11  *)
    12 
    13 let rec fetch_program_counter_n
    14   (n: nat) (code_memory: BitVectorTrie Byte 16) (program_counter: Word)
    15     on n: option Word ≝
    16   match n with
    17   [ O ⇒ Some … program_counter
    18   | S n ⇒
    19     match fetch_program_counter_n n code_memory program_counter with
    20     [ None ⇒ None …
    21     | Some tail_pc ⇒
    22       let 〈instr, program_counter, ticks〉 ≝ fetch code_memory tail_pc in
    23         if ltb (nat_of_bitvector … tail_pc) (nat_of_bitvector … program_counter) then
    24           Some … program_counter
    25         else
    26           None Word (* XXX: overflow! *)
    27     ]
    28   ].
    29    
    30 definition reachable_program_counter: BitVectorTrie Byte 16 → nat → Word → Prop ≝
    31   λcode_memory: BitVectorTrie Byte 16.
    32   λprogram_size: nat.
    33   λprogram_counter: Word.
    34     (∃n: nat. Some … program_counter = fetch_program_counter_n n code_memory (zero 16)) ∧
    35         nat_of_bitvector 16 program_counter < program_size.
    366   
    377definition well_labelling: BitVectorTrie costlabel 16 → Prop ≝
    388  λcost_labels.
    399    injective … (λx. lookup_opt … x cost_labels).
    40    
    41 definition good_program: ∀code_memory: BitVectorTrie Byte 16. ∀total_program_size: nat. Prop ≝
    42   λcode_memory: BitVectorTrie Byte 16.
    43   λtotal_program_size: nat.
    44   ∀program_counter: Word.
    45   ∀good_program_counter_witness: reachable_program_counter code_memory total_program_size program_counter.
    46   let 〈instruction, program_counter', ticks〉 ≝ fetch code_memory program_counter in
    47     match instruction with
    48     [ RealInstruction instr ⇒
    49       match instr with
    50       [ RET                    ⇒ True
    51       | JC   relative          ⇒ True (* XXX: see below *)
    52       | JNC  relative          ⇒ True (* XXX: see below *)
    53       | JB   bit_addr relative ⇒ True
    54       | JNB  bit_addr relative ⇒ True
    55       | JBC  bit_addr relative ⇒ True
    56       | JZ   relative          ⇒ True
    57       | JNZ  relative          ⇒ True
    58       | CJNE src_trgt relative ⇒ True
    59       | DJNZ src_trgt relative ⇒ True
    60       | _                      ⇒
    61         nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧
    62           nat_of_bitvector … program_counter' < total_program_size
    63       ]
    64     | LCALL addr         ⇒
    65       nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧
    66         nat_of_bitvector … program_counter' < total_program_size
    67     | ACALL addr         ⇒
    68       nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧
    69         nat_of_bitvector … program_counter' < total_program_size
    70     | AJMP  addr         ⇒
    71       let jump_target ≝ compute_target_of_unconditional_jump program_counter' instruction in
    72         reachable_program_counter code_memory total_program_size jump_target
    73     | LJMP  addr         ⇒
    74       let jump_target ≝ compute_target_of_unconditional_jump program_counter' instruction in
    75         reachable_program_counter code_memory total_program_size jump_target
    76     | SJMP  addr     ⇒
    77       let jump_target ≝ compute_target_of_unconditional_jump program_counter' instruction in
    78         reachable_program_counter code_memory total_program_size jump_target
    79     | JMP   addr     ⇒ (* XXX: JMP is used for fptrs and unconstrained *)
    80       nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧
    81         nat_of_bitvector … program_counter' < total_program_size
    82     | MOVC  src trgt ⇒
    83         nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧
    84           nat_of_bitvector … program_counter' < total_program_size
    85     ].
    8610
    8711definition current_instruction_label ≝
     
    12044qed.
    12145
    122 let rec trace_any_label_length
    123   (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
    124     (trace_ends_flag: trace_ends_with_ret) (start_status: Status code_memory)
    125       (final_status: Status code_memory)
    126       (the_trace: trace_any_label (ASM_abstract_status code_memory cost_labels) trace_ends_flag start_status final_status)
    127         on the_trace: nat ≝
    128   match the_trace with
    129   [ tal_base_not_return the_status _ _ _ _ ⇒ 0
    130   | tal_base_call pre_fun_call start_fun_call final _ _ _ _ call_trace ⇒ 0
    131   | tal_base_return the_status _ _ _ ⇒ 0
    132   | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final _ _ _ call_trace _ final_trace ⇒
    133       let tail_length ≝ trace_any_label_length … final_trace in
    134       let pc_difference ≝ nat_of_bitvector … (program_counter … after_fun_call) - nat_of_bitvector … (program_counter … pre_fun_call) in       
    135         pc_difference + tail_length
    136   | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
    137       let tail_length ≝ trace_any_label_length … tail_trace in
    138       let pc_difference ≝ nat_of_bitvector … (program_counter … status_init) - nat_of_bitvector … (program_counter … status_pre) in
    139         pc_difference + tail_length       
    140   ].
    141 
    142 definition trace_any_label_length' ≝
     46definition trace_any_label_length ≝
    14347  λcode_memory: BitVectorTrie Byte 16.
    14448  λcost_labels: BitVectorTrie costlabel 16.
     
    234138include alias "arithmetics/nat.ma".
    235139
    236 lemma fetch_program_counter_n_Sn:
    237   ∀instruction: instruction.
    238   ∀program_counter, program_counter': Word.
    239   ∀ticks, n: nat.
    240   ∀code_memory: BitVectorTrie Byte 16.
    241     Some … program_counter = fetch_program_counter_n n code_memory (zero 16) →
    242       〈instruction,program_counter',ticks〉 = fetch code_memory program_counter →
    243         nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' →
    244           Some … program_counter' = fetch_program_counter_n (S n) code_memory (zero …).
    245   #instruction #program_counter #program_counter' #ticks #n #code_memory
    246   #fetch_program_counter_n_hyp #fetch_hyp #lt_hyp
    247   whd in match (fetch_program_counter_n (S n) code_memory (zero …));
    248   <fetch_program_counter_n_hyp normalize nodelta
    249   <fetch_hyp normalize nodelta
    250   change with (
    251     leb (S (nat_of_bitvector … program_counter)) (nat_of_bitvector … program_counter')
    252   ) in match (ltb (nat_of_bitvector … program_counter) (nat_of_bitvector … program_counter'));
    253   >(le_to_leb_true … lt_hyp) %
    254 qed.
    255 
    256 (* XXX: indexing bug *)
    257140lemma execute_1_and_program_counter_after_other_in_lockstep:
    258141  ∀code_memory: BitVectorTrie Byte 16.
     
    270153qed-.
    271154
    272 let rec tal_pc_list_lt_total_program_size
    273   (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
    274     (total_program_size: nat) (total_program_size_invariant: total_program_size ≤ 2^16)
    275       (good_program_witness: good_program code_memory total_program_size)
    276         (start: Status code_memory) (final: Status code_memory) (trace_ends_flag: trace_ends_with_ret)
    277           (the_trace: trace_any_label (ASM_abstract_status code_memory cost_labels) trace_ends_flag start final)
    278             (pc: as_pc (ASM_abstract_status code_memory cost_labels))
    279               on the_trace:
    280   reachable_program_counter code_memory total_program_size (program_counter … start) →
    281     memb word_deqset pc (tal_pc_list (ASM_abstract_status code_memory cost_labels) trace_ends_flag start final the_trace) = true →
    282       nat_of_bitvector 16 pc<total_program_size ≝
    283   match the_trace with
    284   [ tal_base_not_return the_status _ _ _ _ ⇒ ?
    285   | tal_base_return the_status _ _ _ ⇒ ?
    286   | tal_base_call pre_fun_call start_fun_call final _ _ _ _ call_trace ⇒ ?
    287   | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
    288      _ classifier after_return call_trace _ final_trace ⇒ ?
    289   | tal_step_default end_flag status_pre status_init status_end execute tail_trace classifier _ ⇒ ?
    290   ].
    291   #reachable_program_counter_witness
    292   whd in ⊢ (??%? → ?); @(bool_inv_ind … (pc==as_pc_of (ASM_abstract_status code_memory cost_labels) ?))
    293   normalize nodelta #eq_assm cases reachable_program_counter_witness
    294   [1,3,5,7,9:
    295     >(eq_bv_eq … eq_assm) #_ #relevant #_
    296     assumption
    297   |2,4,6:
    298     #_ #_ #absurd
    299     normalize in absurd; destruct(absurd)
    300   |8:
    301     #Some_assm #tps_lt_assm @tal_pc_list_lt_total_program_size try assumption
    302     whd in after_return;
    303     lapply after_return
    304     @pair_elim * normalize nodelta #instruction #pc' #ticks
    305     #fetch_eq #pc_assm' >pc_assm'
    306     lapply (good_program_witness ? reachable_program_counter_witness)
    307     whd in classifier; whd in classifier:(??%?);
    308     whd in match (current_instruction ??) in classifier;
    309     whd in match current_instruction0 in classifier;
    310     >fetch_eq in classifier;
    311     normalize nodelta cases instruction
    312     normalize nodelta -tal_pc_list_lt_total_program_size
    313     [8:
    314       #preinstruction elim preinstruction
    315       normalize in match (? = cl_call);
    316     ]
    317     try (#assm1 #assm2 #absurd destruct(absurd) @I)
    318     try (#assm1 #absurd destruct(absurd) @I)
    319     try (#absurd destruct(absurd) @I)
    320     #_ #_ * #relevant #pc_tps_assm'
    321     whd cases reachable_program_counter_witness * #n
    322     #Some_assm #_ % try assumption
    323     %{(S n)}
    324     @(fetch_program_counter_n_Sn … Some_assm (sym_eq … fetch_eq))
    325     assumption
    326   |10:
    327     #Some_assm #tps_lt_assm @tal_pc_list_lt_total_program_size try assumption -tal_pc_list_lt_total_program_size
    328     lapply (execute_1_and_program_counter_after_other_in_lockstep … status_pre classifier)
    329     @pair_elim * #instruction #pc #ticks normalize nodelta
    330     #fetch_eq whd in match program_counter_after_other; normalize nodelta
    331     lapply (good_program_witness … reachable_program_counter_witness)
    332     whd in classifier; whd in classifier:(??%?);
    333     whd in match (current_instruction ??) in classifier;
    334     whd in match current_instruction0 in classifier;
    335     >fetch_eq in classifier; normalize nodelta cases instruction
    336     normalize nodelta
    337     [8:
    338       #preinstruction elim preinstruction
    339       normalize in match (? = cl_other);
    340     ]
    341     try (#assm1 #assm2 #absurd destruct(absurd) @I)
    342     try (#assm1 #absurd destruct(absurd) @I)
    343     try (#absurd destruct(absurd) @I) normalize nodelta
    344     [27,28,29:
    345       #addr #_ #reachable
    346       #program_counter_execute_1_refl
    347       whd in execute; <execute
    348       >program_counter_execute_1_refl assumption
    349     |*:
    350       try (#assm1 #assm2 #_ * #relevant #pc_lt_assm)
    351       try (#assm1 #_ * #relevant #pc_lt_assm)
    352       try (#_ * #relevant #pc_lt_assm) #pc_refl
    353       cases reachable_program_counter_witness * #n
    354       #Some_assm #tps_lt_assm
    355       whd in match reachable_program_counter; normalize nodelta %
    356       try %{(S n)}
    357       whd in execute; <execute
    358       try (@(fetch_program_counter_n_Sn instruction ?? ticks ?? Some_assm ?) >execute >fetch_eq <pc_refl >execute try %)
    359       <pc_refl in relevant; <execute #assm
    360       >pc_refl >pc_refl in assm; #assm assumption
    361     ]
    362   ]
    363 qed.
     155lemma nat_of_bitvector_lt_bound:
     156  ∀n: nat.
     157  ∀b: BitVector n.
     158    nat_of_bitvector n b < 2^n.
     159  #n #b cases daemon
     160qed.
    364161
    365162lemma sublist_tal_pc_list_all_program_counter_list:
    366163  ∀code_memory: BitVectorTrie Byte 16.
    367164  ∀cost_labels: BitVectorTrie costlabel 16.
    368   ∀total_program_size: nat.
    369   ∀total_program_size_invariant: total_program_size ≤ 2^16.
    370   ∀good_program_witness: good_program code_memory total_program_size.
    371165  ∀start, final: Status code_memory.
    372   ∀reachable_program_counter_witness: reachable_program_counter code_memory total_program_size
    373     (program_counter (BitVectorTrie Byte 16) code_memory start).
    374166  ∀trace_ends_flag.
    375167  ∀the_trace: trace_any_label (ASM_abstract_status code_memory cost_labels) trace_ends_flag start final.
    376     sublist ? (tal_pc_list … the_trace) (all_program_counter_list total_program_size).
    377   #code_memory #cost_labels #total_program_size #total_program_size_invariant
    378   #good_program_witness #start #final #reachable_program_counter_witness
    379   #trace_ends_flag #the_trace
     168    sublist ? (tal_pc_list … the_trace) (all_program_counter_list (2^16)).
     169  #code_memory #cost_labels #start #final #trace_ends_flag #the_trace
    380170  whd in match (sublist ???); #pc #memb_assm
    381   @lt_bound_mem_all_program_counter_list
    382   try assumption destruct
    383   lapply memb_assm -memb_assm
    384   @tal_pc_list_lt_total_program_size
    385   assumption
     171  @lt_bound_mem_all_program_counter_list try %
     172  @nat_of_bitvector_lt_bound
    386173qed.
    387174
     
    389176  ∀code_memory: BitVectorTrie Byte 16.
    390177  ∀cost_labels: BitVectorTrie costlabel 16.
    391   ∀total_program_size: nat.
    392   ∀total_program_size_invariant: total_program_size ≤ 2^16.
    393   ∀good_program_witness: good_program code_memory total_program_size.
    394178  ∀start, final: Status code_memory.
    395   ∀reachable_program_counter_witness: reachable_program_counter code_memory total_program_size
    396     (program_counter (BitVectorTrie Byte 16) code_memory start).
    397179  ∀trace_ends_flag.
    398180  ∀the_trace: trace_any_label (ASM_abstract_status code_memory cost_labels) trace_ends_flag start final.
    399181  ∀unrepeating_witness: tal_unrepeating (ASM_abstract_status code_memory cost_labels) trace_ends_flag start final the_trace.
    400     |tal_pc_list … the_trace| ≤ total_program_size.
    401   #code_memory #cost_labels #total_program_size #total_program_size_invariant
    402   #good_program_witness #start #final #reachable_program_counter_witness
    403   #trace_ends_flag #the_trace #unrepeating_witness
    404   <(all_program_counter_list_bound_eq total_program_size)
     182    |tal_pc_list … the_trace| ≤ 2^16.
     183  #code_memory #cost_labels #start #final #trace_ends_flag #the_trace #unrepeating_witness
     184  <(all_program_counter_list_bound_eq (2^16))
    405185  @sublist_length
    406186  [1:
     
    449229  ].
    450230
    451 lemma reachable_program_counter_to_0_lt_total_program_size:
    452   ∀code_memory: BitVectorTrie Byte 16.
    453   ∀program_counter: Word.
    454   ∀total_program_size: nat.
    455     reachable_program_counter code_memory total_program_size program_counter →
    456       0 < total_program_size.
    457   #code_memory #program_counter #total_program_size
    458   whd in match reachable_program_counter; normalize nodelta * * #some_n
    459   #_ cases (nat_of_bitvector 16 program_counter)
    460   [1:
    461     #assm assumption
    462   |2:
    463     #new_pc @ltn_to_ltO
    464   ]
    465 qed.
    466 
    467231lemma trace_compute_paid_trace_cl_other:
    468232  ∀code_memory' : (BitVectorTrie Byte 16).
    469233  ∀program_counter' : Word.
    470   ∀total_program_size : ℕ.
    471234  ∀cost_labels : (BitVectorTrie costlabel 16).
    472   ∀reachable_program_counter_witness : (reachable_program_counter code_memory' total_program_size program_counter').
    473   ∀good_program_witness : (good_program code_memory' total_program_size).
    474235  ∀program_size' : ℕ.
    475236  ∀ticks : ℕ.
     
    483244  ∀the_trace : (trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status).
    484245  ∀program_counter_refl : (program_counter' = program_counter (BitVectorTrie Byte 16) code_memory' start_status).
    485   ∀size_invariant : trace_any_label_length' code_memory' cost_labels trace_ends_flag start_status final_status the_trace ≤S program_size'.
     246  ∀size_invariant : trace_any_label_length code_memory' cost_labels trace_ends_flag start_status final_status the_trace ≤S program_size'.
    486247  ∀classify_assm: ASM_classify0 instruction = cl_other.
    487248  ∀pi1 : ℕ.
     
    495256      ∀trace_ends_flag0:trace_ends_with_ret.
    496257      ∀the_trace0:trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag0 start_status0 final_status0.
    497         trace_any_label_length' code_memory' cost_labels trace_ends_flag0
     258        trace_any_label_length code_memory' cost_labels trace_ends_flag0
    498259          start_status0 final_status0 the_trace0 ≤ program_size' →
    499260        program_counter''' = program_counter (BitVectorTrie Byte 16) code_memory' start_status0 →
     
    505266     =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag
    506267      start_status final_status the_trace.
    507   #code_memory' #program_counter' #total_program_size #cost_labels
    508   #reachable_program_counter_witness #good_program_witness
    509   #program_size' #ticks #instruction #program_counter'' #FETCH
    510   #start_status #final_status
    511   #trace_ends_flag #the_trace #program_counter_refl #size_invariant #classify_assm #recursive_block_cost
     268  #code_memory' #program_counter' #cost_labels #program_size' #ticks #instruction
     269  #program_counter'' #FETCH #start_status #final_status #trace_ends_flag #the_trace
     270  #program_counter_refl #size_invariant #classify_assm #recursive_block_cost
    512271  #recursive_assm
    513272  @(trace_any_label_inv_ind … the_trace)
     
    534293        normalize nodelta #new_recursive_assm
    535294        cases(new_recursive_assm (execute_1 code_memory' status_pre) status_end
    536           end_flag trace_any_label ? ?) try %
     295          end_flag trace_any_label ? ?) try (>rewrite_assm %)
    537296        whd in match (current_instruction_cost … status_pre);
    538297        cut(ticks = \snd (fetch code_memory'
    539298           (program_counter (BitVectorTrie Byte 16) code_memory' status_pre)))
    540         [1,3,5:
     299        [1,3:
    541300          <FETCH %
    542301        |2:
     
    548307          lapply (le_S_S_to_le … size_invariant) #assm
    549308          assumption
    550         |6:
    551           #ticks_refl_assm
    552           <rewrite_assm %
    553309        ]
    554310      |2:
     
    630386  ∀code_memory': BitVectorTrie Byte 16.
    631387  ∀program_counter': Word.
    632   ∀total_program_size: ℕ.
    633388  ∀cost_labels: BitVectorTrie costlabel 16.
    634   ∀reachable_program_counter_witness: reachable_program_counter code_memory' total_program_size program_counter'.
    635   ∀good_program_witness: good_program code_memory' total_program_size.
    636389  ∀first_time_around: bool.
    637390  ∀program_size': ℕ.
     
    649402     =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag
    650403      start_status final_status the_trace.
    651   #code_memory' #program_counter' #total_program_size #cost_labels
    652   #reachable_program_counter_witness #good_program_witness #first_time_around
     404  #code_memory' #program_counter' #cost_labels #first_time_around
    653405  #program_size' #ticks #instruction #program_counter'' #FETCH
    654406  #start_status #final_status
     
    689441  ∀code_memory' : (BitVectorTrie Byte 16).
    690442  ∀program_counter' : Word.
    691   ∀total_program_size : ℕ.
    692443  ∀cost_labels : (BitVectorTrie costlabel 16).
    693   ∀reachable_program_counter_witness : (reachable_program_counter code_memory' total_program_size program_counter').
    694   ∀good_program_witness : (good_program code_memory' total_program_size).
    695444  ∀program_size' : ℕ.
    696445  ∀ticks : ℕ.
     
    703452  ∀the_trace : (trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status).
    704453  ∀program_counter_refl : (program_counter' = program_counter (BitVectorTrie Byte 16) code_memory' start_status).
    705   ∀size_invariant : trace_any_label_length' code_memory' cost_labels trace_ends_flag start_status final_status the_trace ≤S program_size'.
     454  ∀size_invariant : trace_any_label_length code_memory' cost_labels trace_ends_flag start_status final_status the_trace ≤S program_size'.
    706455  ∀classify_assm: ASM_classify0 instruction = cl_call.
    707456  (∀pi1:ℕ
     
    714463                                        (ASM_abstract_status code_memory' cost_labels)
    715464                                        trace_ends_flag0 start_status0 final_status0.
    716                 trace_any_label_length' code_memory' cost_labels trace_ends_flag0
     465                trace_any_label_length code_memory' cost_labels trace_ends_flag0
    717466                  start_status0 final_status0 the_trace0
    718467                   ≤ program_size' →
     
    726475     =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag
    727476      start_status final_status the_trace).
    728   #code_memory' #program_counter' #total_program_size #cost_labels
    729   #reachable_program_counter_witness #good_program_witness #program_size'
     477  #code_memory' #program_counter' #cost_labels #program_size'
    730478  #ticks #instruction #program_counter'' #FETCH
    731479  #start_status #final_status #trace_ends_flag
     
    830578  ∀code_memory' : (BitVectorTrie Byte 16).
    831579  ∀program_counter' : Word.
    832   ∀total_program_size : ℕ.
    833580  ∀cost_labels : (BitVectorTrie costlabel 16).
    834   ∀reachable_program_counter_witness : (reachable_program_counter code_memory' total_program_size program_counter').
    835   ∀good_program_witness : (good_program code_memory' total_program_size).
    836581  ∀program_size' : ℕ.
    837582  ∀ticks : ℕ.
     
    848593     =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag
    849594      start_status final_status the_trace.
    850   #code_memory' #program_counter' #total_program_size #cost_labels
    851   #reachable_program_counter_witness #good_program_witness #program_size'
     595  #code_memory' #program_counter' #cost_labels #program_size'
    852596  #ticks #instruction #program_counter'' #FETCH
    853597  #start_status #final_status #trace_ends_flag
     
    897641  ∀final_status: Status code_memory.
    898642  ∀the_trace.
    899   trace_any_label_length' code_memory cost_labels trace_ends_flag start_status
     643  trace_any_label_length code_memory cost_labels trace_ends_flag start_status
    900644    final_status the_trace ≤ 0 → False.
    901645  #code_memory #cost_labels #trace_ends_flag #start_status #final_status
     
    906650let rec block_cost'
    907651  (code_memory': BitVectorTrie Byte 16) (program_counter': Word)
    908     (program_size: nat) (total_program_size: nat) (cost_labels: BitVectorTrie costlabel 16)
    909       (reachable_program_counter_witness: reachable_program_counter code_memory' total_program_size program_counter')
    910         (good_program_witness: good_program code_memory' total_program_size) (first_time_around: bool)
    911           on program_size:
     652    (program_size: nat) (cost_labels: BitVectorTrie costlabel 16)
     653      (first_time_around: bool)
     654        on program_size:
    912655          Σcost_of_block: nat.
    913656          if (match lookup_opt … program_counter' cost_labels with [ None ⇒ true | _ ⇒ first_time_around ]) then
     
    916659            ∀trace_ends_flag.
    917660            ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
    918               trace_any_label_length' … the_trace ≤ program_size →
     661              trace_any_label_length … the_trace ≤ program_size →
    919662              program_counter' = program_counter … start_status →
    920663                cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace
     
    940683            ∀trace_ends_flag.
    941684            ∀the_trace: trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status.
    942               trace_any_label_length' … the_trace ≤ S program_size' →
     685              trace_any_label_length … the_trace ≤ S program_size' →
    943686              program_counter' = program_counter … start_status →
    944687                cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace with
     
    955698          | DJNZ src_trgt relative ⇒ λinstr. ticks
    956699          | _                      ⇒ λinstr.
    957               ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false
     700              ticks + block_cost' code_memory' program_counter'' program_size' cost_labels false
    958701          ] (refl …)
    959702        | ACALL addr     ⇒ λinstr.
    960             ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false
     703            ticks + block_cost' code_memory' program_counter'' program_size' cost_labels false
    961704        | AJMP  addr     ⇒ λinstr.
    962705          let jump_target ≝ compute_target_of_unconditional_jump program_counter'' instruction in
    963             ticks + block_cost' code_memory' jump_target program_size' total_program_size cost_labels ? good_program_witness false
     706            ticks + block_cost' code_memory' jump_target program_size' cost_labels false
    964707        | LCALL addr     ⇒ λinstr.
    965             ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false
     708            ticks + block_cost' code_memory' program_counter'' program_size' cost_labels false
    966709        | LJMP  addr     ⇒ λinstr.
    967710          let jump_target ≝ compute_target_of_unconditional_jump program_counter'' instruction in
    968             ticks + block_cost' code_memory' jump_target program_size' total_program_size cost_labels ? good_program_witness false
     711            ticks + block_cost' code_memory' jump_target program_size' cost_labels false
    969712        | SJMP  addr     ⇒ λinstr.
    970713          let jump_target ≝ compute_target_of_unconditional_jump program_counter'' instruction in
    971             ticks + block_cost' code_memory' jump_target program_size' total_program_size cost_labels ? good_program_witness false
     714            ticks + block_cost' code_memory' jump_target program_size' cost_labels false
    972715        | JMP   addr     ⇒ λinstr. (* XXX: actually a call due to use with fptrs *)
    973             ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false
     716            ticks + block_cost' code_memory' program_counter'' program_size' cost_labels false
    974717        | MOVC  src trgt ⇒ λinstr.
    975             ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false
     718            ticks + block_cost' code_memory' program_counter'' program_size' cost_labels false
    976719        ] (refl …))
    977720      else
     
    984727            ∀trace_ends_flag.
    985728            ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
    986               trace_any_label_length' … the_trace ≤ S program_size' →
     729              trace_any_label_length … the_trace ≤ S program_size' →
    987730              program_counter' = program_counter … start_status →
    988731                cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace
     
    1010753    change with (if to_continue then ? else (0 = 0))
    1011754    >p normalize nodelta %
    1012   |6,7:
     755  |5,6:
    1013756    #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl
    1014     @(trace_compute_paid_trace_cl_return … reachable_program_counter_witness good_program_witness program_size' … FETCH … the_trace program_counter_refl)
     757    @(trace_compute_paid_trace_cl_return … program_size' … FETCH … the_trace program_counter_refl)
    1015758    destruct %
    1016   |69,77,79:
     759  |42,46,47:
    1017760    #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl
    1018     cases(block_cost' ????????) -block_cost'
    1019     @(trace_compute_paid_trace_cl_call … reachable_program_counter_witness good_program_witness program_size' … FETCH … the_trace program_counter_refl size_invariant)
     761    cases(block_cost' ?????) -block_cost'
     762    @(trace_compute_paid_trace_cl_call … program_size' … FETCH … the_trace program_counter_refl size_invariant)
    1020763    destruct %
    1021   |4,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,51,53,55,57,59,61,63,65,
    1022     67:
     764  |43,44,45: (* XXX: unconditional jumps *)
    1023765    #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl
    1024     cases(block_cost' ????????) -block_cost'
    1025     lapply (trace_compute_paid_trace_cl_other … reachable_program_counter_witness good_program_witness program_size' … FETCH … the_trace program_counter_refl size_invariant)     
    1026     destruct #assm @assm %
    1027   |42,43,44,45,46,47,48,49,50:
    1028     #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl
    1029     @(trace_compute_paid_trace_cl_jump … reachable_program_counter_witness good_program_witness … FETCH … the_trace program_counter_refl)
    1030     destruct %
    1031   |71,73,75: (* XXX: unconditional jumps *)
    1032     #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl
    1033     cases (block_cost' ????????) -block_cost'
    1034     lapply (trace_compute_paid_trace_cl_other … reachable_program_counter_witness good_program_witness program_size' … FETCH … the_trace program_counter_refl size_invariant)
     766    cases (block_cost' ?????) -block_cost'
     767    lapply (trace_compute_paid_trace_cl_other … program_size' … FETCH … the_trace program_counter_refl size_invariant)
    1035768    whd in match (program_counter_after_other ??); normalize nodelta destruct
    1036769    whd in match (is_unconditional_jump ?); normalize nodelta #assm @assm %
    1037   ]
    1038   -block_cost'
    1039   [29,30,31: (* XXX: unconditional jumps *)
    1040     normalize nodelta
    1041     cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    1042     lapply (good_program_witness program_counter' reachable_program_counter_witness)
    1043     <FETCH normalize nodelta <instr normalize nodelta #assm assumption
     770  |24,25,26,27,28,29,30,31,32:
     771    #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl
     772    @(trace_compute_paid_trace_cl_jump … first_time_around program_size' … FETCH … the_trace program_counter_refl)
     773    destruct %
    1044774  |*:
    1045     cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    1046     lapply(good_program_witness program_counter' reachable_program_counter_witness)
    1047     <FETCH normalize nodelta destruct normalize nodelta
    1048     * #program_counter_lt' #program_counter_lt_tps'
    1049     % try assumption
    1050     %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
    1051     <FETCH normalize nodelta whd in match ltb; normalize nodelta
    1052     >(le_to_leb_true … program_counter_lt') %
     775    #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl
     776    cases(block_cost' ?????) -block_cost'
     777    lapply (trace_compute_paid_trace_cl_other … program_size' … FETCH … the_trace program_counter_refl size_invariant)     
     778    destruct #assm @assm %
    1053779  ]
    1054780qed.
     
    1057783    ∀code_memory': BitVectorTrie Byte 16.
    1058784    ∀program_counter': Word.
    1059     ∀total_program_size: nat.
    1060     ∀total_program_size_invariant: total_program_size ≤ 2^16.
    1061785    ∀cost_labels: BitVectorTrie costlabel 16.
    1062     ∀reachable_program_counter_witness: reachable_program_counter code_memory' total_program_size program_counter'.
    1063     ∀good_program_witness: good_program code_memory' total_program_size.
    1064786      Σcost_of_block: nat.
    1065787        ∀start_status: Status code_memory'.
     
    1067789        ∀trace_ends_flag.
    1068790        ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
    1069         ∀reachable_program_counter_witness: reachable_program_counter code_memory' total_program_size (program_counter (BitVectorTrie Byte 16) code_memory' start_status).
    1070791        ∀unrepeating_witness: tal_unrepeating (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status the_trace.
    1071792          program_counter' = program_counter … start_status →
     
    1073794  λcode_memory: BitVectorTrie Byte 16.
    1074795  λprogram_counter: Word.
    1075   λtotal_program_size: nat.
    1076   λtotal_program_size_invariant: total_program_size ≤ 2^16.
    1077   λcost_labels: BitVectorTrie costlabel 16.
    1078   λreachable_program_counter_witness: reachable_program_counter code_memory total_program_size program_counter.
    1079   λgood_program_witness: good_program code_memory total_program_size. ?.
    1080   cases(block_cost' code_memory program_counter total_program_size total_program_size cost_labels
    1081     reachable_program_counter_witness good_program_witness true)
     796  λcost_labels: BitVectorTrie costlabel 16. ?.
     797  cases(block_cost' code_memory program_counter (2^16) cost_labels true)
    1082798  #cost_of_block #block_cost_hyp
    1083799  %{cost_of_block}
    1084800  cases(lookup_opt … cost_labels) in block_cost_hyp;
    1085801  [2: #cost_label] normalize nodelta
    1086   #hyp #start_status #final_status #trace_ends_flag #the_trace
    1087   #reachable_program_counter_witness #unrepeating_witness
     802  #hyp #start_status #final_status #trace_ends_flag #the_trace #unrepeating_witness
    1088803  @hyp @tal_pc_list_length_leq_total_program_size try assumption
    1089804qed.
Note: See TracChangeset for help on using the changeset viewer.