Changeset 1929


Ignore:
Timestamp:
May 9, 2012, 2:44:39 PM (7 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.

Location:
src/ASM
Files:
3 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.
  • src/ASM/ASMCostsSplit.ma

    r1928 r1929  
    66let rec traverse_code_internal
    77  (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
    8     (program_counter: Word) (fixed_program_size: nat) (program_size: nat)
    9       (reachable_program_counter_witness:
    10           ∀lbl: costlabel.
    11           ∀program_counter: Word. Some … lbl = lookup_opt … program_counter cost_labels →
    12             reachable_program_counter code_memory fixed_program_size program_counter)
    13         (good_program_witness: good_program code_memory fixed_program_size)
    14         (program_size_invariant: program_size = 0 ∨ nat_of_bitvector … program_counter + program_size = fixed_program_size)
    15         (fixed_program_size_limit: fixed_program_size ≤ 2^16)
     8    (program_counter: Word) (program_size: nat)
     9      (program_size_invariant: program_size = 0 ∨ nat_of_bitvector … program_counter + program_size = 2^16)
    1610        on program_size:
    1711          Σcost_map: identifier_map CostTag nat.
    1812            (∀pc,k. nat_of_bitvector … program_counter ≤ nat_of_bitvector 16 pc → nat_of_bitvector … pc < program_size + nat_of_bitvector … program_counter → lookup_opt … pc cost_labels = Some … k → present … cost_map k) ∧
    1913            (∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k ∧
    20               ∃reachable_witness: reachable_program_counter code_memory fixed_program_size pc.
    21                 pi1 … (block_cost code_memory pc fixed_program_size fixed_program_size_limit cost_labels reachable_witness good_program_witness) = lookup_present … k_pres) ≝
     14               pi1 … (block_cost code_memory pc cost_labels) = lookup_present … k_pres) ≝
    2215  match program_size return λx. x = program_size → Σcost_map: ?. ? with
    2316  [ O ⇒ λprogram_size_refl. empty_map CostTag nat
    2417  | S program_size' ⇒ λprogram_size_refl.
    2518    deplet 〈carry, new_program_counter'〉 as NEW_PC' ≝ half_add 16 (bitvector_of_nat 16 1) program_counter in
    26     let cost_mapping ≝ traverse_code_internal code_memory cost_labels new_program_counter' fixed_program_size program_size' ? good_program_witness ? fixed_program_size_limit in
     19    let cost_mapping ≝ traverse_code_internal code_memory cost_labels new_program_counter' program_size' ? in
    2720    match lookup_opt … program_counter cost_labels return λx. x = lookup_opt … program_counter cost_labels → Σcost_map: ?. ? with
    2821    [ None ⇒ λlookup_refl. pi1 … cost_mapping
    2922    | Some lbl ⇒ λlookup_refl.
    30       let cost ≝ block_cost code_memory program_counter fixed_program_size fixed_program_size_limit cost_labels ? good_program_witness in
     23      let cost ≝ block_cost code_memory program_counter cost_labels in
    3124        add … cost_mapping lbl cost
    3225    ] (refl … (lookup_opt … program_counter cost_labels))
    3326  ] (refl … program_size).
    34   [5:
    35     assumption
    36   |4:
    37     @(reachable_program_counter_witness lbl)
    38     @lookup_refl
    39   |3:
     27  [3:
    4028    cases program_size_invariant
    4129    [1:
     
    8068              @succ_nat_of_bitvector_half_add_1
    8169              @le_plus_to_minus_r
    82               @(transitive_le … fixed_program_size_limit)
    8370              change with (S ? ≤ ?) >plus_n_Sm
     71              <program_size_invariant'
    8472              @monotonic_le_plus_r
    8573              @le_S_S @le_S_S @le_O_n
     
    128116            >eq_assm >lookup_refl %
    129117          |2:
    130             %{(reachable_program_counter_witness …)} try assumption
    131118            >eq_assm in k_pres ⊢ (???%); #k_pres >lookup_present_add_hit %
    132119          ]
     
    142129              cases ind_hyp' #assm #_ assumption
    143130            |2:
    144               cases ind_hyp' #lookup_opt_assm * #reachable_witness'
    145               #ind_hyp'' %{reachable_witness'} >ind_hyp''
     131              cases ind_hyp' #lookup_opt_assm #ind_hyp'' >ind_hyp''
    146132              @sym_eq @lookup_present_add_miss assumption
    147133            ]
     
    207193                  @succ_nat_of_bitvector_half_add_1
    208194                  @le_plus_to_minus_r
    209                   @(transitive_le … fixed_program_size_limit)
    210195                  change with (S ? ≤ ?) >plus_n_Sm
     196                  <program_size_invariant
    211197                  @monotonic_le_plus_r
    212198                  @le_S_S @le_S_S @le_O_n
     
    228214              @succ_nat_of_bitvector_half_add_1
    229215              @le_plus_to_minus_r
    230               @(transitive_le … fixed_program_size_limit)
    231216              change with (S ? ≤ ?) >plus_n_Sm
     217              <program_size_invariant
    232218              @monotonic_le_plus_r
    233219              @le_S_S @le_S_S @le_O_n
     
    244230      assumption
    245231    ]
    246   |6:
     232  |4:
    247233    inversion program_size'
    248234    [1:
     
    262248          @succ_nat_of_bitvector_half_add_1
    263249          @le_plus_to_minus_r
    264           @(transitive_le … fixed_program_size_limit)
    265250          change with (S ? ≤ ?) >plus_n_Sm
     251          <relevant
    266252          @monotonic_le_plus_r
    267253          @le_S_S @le_S_S @le_O_n
     
    288274qed.
    289275
     276(* XXX:
     277 * At the moment we do a full traversal of the code memory, however we could do
     278 * a fold over the domain of the cost labels map.
     279 *
     280 *)
    290281definition traverse_code:
    291282  ∀code_memory: BitVectorTrie Byte 16.
     
    295286      lookup_opt … pc cost_labels = Some … l → lookup_opt … pc' cost_labels = Some … l →
    296287        pc = pc'.
    297   ∀program_size: nat.
    298   ∀program_size_limit: program_size ≤ 2^16.
    299   ∀reachable_program_counter_witness:
    300     ∀lbl: costlabel.
    301     ∀program_counter: Word. Some … lbl = lookup_opt … program_counter cost_labels →
    302       reachable_program_counter code_memory program_size program_counter.
    303   ∀good_program_witness: good_program code_memory program_size.
    304288    Σcost_map: identifier_map CostTag nat.
    305       (∀pc,k. nat_of_bitvector … pc < program_size → lookup_opt … pc cost_labels = Some … k → present … cost_map k) ∧
     289      (∀pc,k. nat_of_bitvector … pc < 2^16 → lookup_opt … pc cost_labels = Some … k → present … cost_map k) ∧
    306290      (∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc cost_labels = Some … k →
    307         ∃reachable_witness: reachable_program_counter code_memory program_size pc.
    308           pi1 … (block_cost code_memory pc program_size program_size_limit cost_labels reachable_witness good_program_witness) = lookup_present … k_pres) ≝
     291          pi1 … (block_cost code_memory pc cost_labels) = lookup_present … k_pres) ≝
    309292  λcode_memory: BitVectorTrie Byte 16.
    310293  λcost_labels: BitVectorTrie costlabel 16.
    311294  λcost_labels_injective.
    312   λprogram_size: nat.
    313   λprogram_size_limit: program_size ≤ 2^16.
    314   λreachable_program_counter_witness:
    315           ∀lbl: costlabel.
    316           ∀program_counter: Word. Some … lbl = lookup_opt … program_counter cost_labels →
    317             reachable_program_counter code_memory program_size program_counter.
    318   λgood_program_witness: good_program code_memory program_size.
    319     pi1 ? ? (traverse_code_internal code_memory cost_labels (zero …) program_size program_size reachable_program_counter_witness good_program_witness ? program_size_limit).
     295    pi1 ? ? (traverse_code_internal code_memory cost_labels (zero …) (2^16) ?).
    320296  [1:
    321297    @or_intror %
    322298  |2:
    323     cases (traverse_code_internal ? ? ? ? ? ? ? ? ?)
     299    cases (traverse_code_internal ?????)
    324300    #cost_mapping * #inductive_hypothesis1 #inductive_hypothesis2 %
    325301    [1:
     
    335311      #k #k_pres #pc #lookup_opt_assm
    336312      cases (inductive_hypothesis2 ? k_pres)
    337       #program_counter' * #lookup_opt_assm' * #reachable_witness
    338       #block_cost_assm
     313      #program_counter' * #lookup_opt_assm' #block_cost_assm
    339314      >(cost_labels_injective … lookup_opt_assm lookup_opt_assm')
    340       %{reachable_witness} assumption
     315      assumption
    341316    ]
    342317  ]
     
    350325      lookup_opt … pc cost_labels = Some … l → lookup_opt … pc' cost_labels = Some … l →
    351326        pc = pc'.
    352   λreachable_program_witness.
    353   λgood_program_witness: good_program (load_code_memory program) (|program|).
    354   λprogram_size_limit: |program| ≤ 2^16.
    355327    let program_size ≝ |program| in
    356328    let code_memory ≝ load_code_memory program in
    357       traverse_code code_memory cost_labels cost_labels_injective program_size program_size_limit reachable_program_witness good_program_witness.
     329      traverse_code code_memory cost_labels cost_labels_injective.
  • src/ASM/CostsProof.ma

    r1928 r1929  
    526526   
    527527let rec compute_trace_label_return_using_paid_ok_with_trace
    528  (cm: ?) (total_program_size: nat) (total_program_size_limit: total_program_size ≤ 2^16)
    529  (good_program_witness: good_program cm total_program_size)
    530  (cost_labels: BitVectorTrie costlabel 16)
     528 (cm: ?) (cost_labels: BitVectorTrie costlabel 16)
    531529 (cost_map: identifier_map CostTag nat)
    532530 (initial: Status cm) (final: Status cm)
     
    536534 ∀unrepeating_witness: tlr_unrepeating … trace.
    537535 ∀dom_codom:(∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc cost_labels = Some … k →
    538    ∃reachable_witness: reachable_program_counter cm total_program_size pc.
    539    pi1 … (block_cost cm pc total_program_size total_program_size_limit cost_labels reachable_witness good_program_witness) = lookup_present … k_pres).
     536   pi1 … (block_cost cm pc cost_labels) = lookup_present … k_pres).
    540537  let ctrace ≝ compute_cost_trace_label_return cm … trace in
    541538  compute_trace_label_return_cost_using_paid cm … trace =
     
    543540    ≝ ?
    544541and compute_trace_any_label_using_paid_ok_with_trace
    545  (cm: ?) (total_program_size: nat) (total_program_size_limit: total_program_size ≤ 2^16)
    546  (good_program_witness: good_program cm total_program_size)
    547  (cost_labels: BitVectorTrie costlabel 16)
     542 (cm: ?) (cost_labels: BitVectorTrie costlabel 16)
    548543 (trace_ends_flag: trace_ends_with_ret)
    549544 (cost_map: identifier_map CostTag nat)
     
    552547 (codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k))
    553548 (dom_codom:(∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc cost_labels = Some … k →
    554    ∃reachable_witness: reachable_program_counter cm total_program_size pc.
    555    pi1 … (block_cost cm pc total_program_size total_program_size_limit cost_labels reachable_witness good_program_witness) = lookup_present … k_pres))
     549   pi1 … (block_cost cm pc cost_labels) = lookup_present … k_pres))
    556550 on trace:
    557551  ∀unrepeating_witness: tal_unrepeating … trace.
     
    561555    ≝ ?
    562556and compute_trace_label_label_using_paid_ok_with_trace
    563  (cm: ?) (total_program_size: nat) (total_program_size_limit: total_program_size ≤ 2^16)
    564  (good_program_witness: good_program cm total_program_size)
    565  (cost_labels: BitVectorTrie costlabel 16)
     557 (cm: ?) (cost_labels: BitVectorTrie costlabel 16)
    566558 (trace_ends_flag: trace_ends_with_ret)
    567559 (cost_map: identifier_map CostTag nat)
     
    571563 (codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k))
    572564 (dom_codom:(∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc cost_labels = Some … k →
    573    ∃reachable_witness: reachable_program_counter cm total_program_size pc.
    574    pi1 … (block_cost cm pc total_program_size total_program_size_limit cost_labels reachable_witness good_program_witness) = lookup_present … k_pres))
     565   pi1 … (block_cost cm pc cost_labels) = lookup_present … k_pres))
    575566 on trace:
    576567 ∀unrepeating_witness: tll_unrepeating … trace.
     
    582573  [ #sb #sa #tr #unrepeating_witness #dom_codom whd in ⊢ (??%?);
    583574    whd in match (compute_cost_trace_label_return ?????);
    584     @(compute_trace_label_label_using_paid_ok_with_trace … good_program_witness)
     575    @compute_trace_label_label_using_paid_ok_with_trace
    585576    assumption
    586577  | #si #sl #sf #tr1 #tr2 #unrepeating_witness #dom_codom
     
    588579    whd in match (compute_cost_trace_label_return ?????);
    589580    >append_length >bigop_sum_rev >commutative_plus @eq_f2
    590     [ >(compute_trace_label_return_using_paid_ok_with_trace … good_program_witness … cost_map … codom_dom ? dom_codom)
     581    [ >(compute_trace_label_return_using_paid_ok_with_trace … cost_map … codom_dom ? dom_codom)
    591582      -compute_trace_label_return_using_paid_ok_with_trace
    592583      [1:
     
    596587        #tll_unrepeating #tlr_unrepeating #_ assumption
    597588      ]
    598     | >(compute_trace_label_label_using_paid_ok_with_trace … good_program_witness … cost_map … codom_dom … dom_codom)
     589    | >(compute_trace_label_label_using_paid_ok_with_trace … cost_map … codom_dom … dom_codom)
    599590      -compute_trace_label_label_using_paid_ok_with_trace
    600591      [1:
     
    609600    #unrepeating_witness'
    610601    whd in ⊢ (??%?); whd in ⊢ (??(?%?)?);
    611     >(compute_trace_any_label_using_paid_ok_with_trace … good_program_witness … cost_map … codom_dom … dom_codom)
     602    >(compute_trace_any_label_using_paid_ok_with_trace … cost_map … codom_dom … dom_codom)
    612603    [1:
    613604      >bigop_0 in ⊢ (???%); >commutative_plus @eq_f2
     
    626617          normalize nodelta #cost_label #Some_assm #_ #p
    627618          cases (dom_codom ? p ? Some_assm)
    628           #reachable_witness #block_cost_assm <block_cost_assm
    629           cases (block_cost ???????)
    630           #cost -block_cost_assm #block_cost_assm
    631           cases (block_cost_assm ??? trace_any_label ???)
     619          cases (block_cost ???)
     620          #cost #block_cost_assm
     621          cases (block_cost_assm ??? trace_any_label ??)
    632622          try @refl assumption
    633623        ]
     
    647637    #classifier_assm #after_return_assm #trace_label_return #costed_assm #unrepeating_witness
    648638    whd in ⊢ (??%?);
    649     @(compute_trace_label_return_using_paid_ok_with_trace … good_program_witness … cost_map … codom_dom ? dom_codom)
     639    @(compute_trace_label_return_using_paid_ok_with_trace … cost_map … codom_dom ? dom_codom)
    650640    assumption
    651641  |6:
     
    654644    #costed_assm #trace_any_label #unrepeating_witness
    655645    whd in ⊢ (??%?);
    656     >(compute_trace_label_return_using_paid_ok_with_trace … good_program_witness … cost_map … codom_dom ? dom_codom)
     646    >(compute_trace_label_return_using_paid_ok_with_trace … cost_map … codom_dom ? dom_codom)
    657647    [1:
    658       >(compute_trace_any_label_using_paid_ok_with_trace … good_program_witness … cost_map … codom_dom … dom_codom)
     648      >(compute_trace_any_label_using_paid_ok_with_trace … cost_map … codom_dom … dom_codom)
    659649      [1:
    660650        >length_append >bigop_sum_rev >commutative_plus @eq_f2
     
    675665    #execute_assm #trace_any_label #classifier_assm #costed_assm #unrepeating_witness
    676666    whd in ⊢ (??%?);
    677     @(compute_trace_any_label_using_paid_ok_with_trace … good_program_witness … cost_map … codom_dom … dom_codom)
     667    @(compute_trace_any_label_using_paid_ok_with_trace … cost_map … codom_dom … dom_codom)
    678668    inversion unrepeating_witness
    679669    #memb_1 #tal_unrepeating #_ assumption
     
    683673lemma compute_max_trace_label_return_cost_ok_with_trace_aux:
    684674  ∀code_memory: BitVectorTrie Byte 16.
    685   ∀total_program_size: nat.
    686   ∀total_program_size_limit: total_program_size ≤ 2^16.
    687   ∀good_program_witness: good_program code_memory total_program_size.
    688675  ∀cost_labels: BitVectorTrie costlabel 16.
    689676  ∀cost_map: identifier_map CostTag nat.
     
    694681  ∀codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k).
    695682  ∀dom_codom: (∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc cost_labels = Some … k →
    696     ∃reachable_witness: reachable_program_counter code_memory total_program_size pc.
    697       pi1 … (block_cost code_memory pc total_program_size total_program_size_limit cost_labels reachable_witness good_program_witness) = lookup_present … k_pres).
     683      pi1 … (block_cost code_memory pc cost_labels) = lookup_present … k_pres).
    698684        let ctrace ≝ compute_cost_trace_label_return code_memory … trace in
    699685          clock … code_memory … final =
    700686            clock … code_memory … initial + (Σ_{i < |ctrace|} (tech_cost_of_label cost_labels cost_map codom_dom ctrace i)).
    701   #code_memory #total_program_size #total_program_size_limit
    702   #good_program_witness #cost_labels #cost_map
     687  #code_memory #cost_labels #cost_map
    703688  #initial #final #trace #unrepeating_witness #codom_dom #dom_codom normalize nodelta
    704689  <compute_trace_label_return_using_paid_ok_with_trace try assumption
     
    708693theorem compute_max_trace_label_return_cost_ok_with_trace:
    709694  ∀code_memory: BitVectorTrie Byte 16.
    710   ∀total_program_size: nat.
    711   ∀total_program_size_invariant: total_program_size ≤ 2^16.
    712   ∀good_program_witness: good_program code_memory total_program_size.
    713695  ∀cost_labels: BitVectorTrie costlabel 16.
    714696  ∀cost_labels_injective:
     
    716698     lookup_opt costlabel 16 pc cost_labels=Some costlabel l
    717699      →lookup_opt costlabel 16 pc' cost_labels=Some costlabel l→pc=pc').
    718   ∀reachable_program_counter_witness:
    719     ∀lbl: costlabel.
    720     ∀program_counter: Word.
    721       Some costlabel lbl=lookup_opt costlabel 16 program_counter cost_labels →
    722         reachable_program_counter code_memory total_program_size program_counter.
    723700  ∀initial: Status code_memory.
    724701  ∀final: Status code_memory.
    725702  ∀trace: trace_label_return (ASM_abstract_status code_memory cost_labels) initial final.
    726703  ∀unrepeating_witness: tlr_unrepeating … trace.
    727     let cost_map ≝ traverse_code code_memory cost_labels cost_labels_injective total_program_size total_program_size_invariant
    728       reachable_program_counter_witness good_program_witness in
     704    let cost_map ≝ traverse_code code_memory cost_labels cost_labels_injective in
    729705    let ctrace ≝ compute_cost_trace_label_return code_memory … trace in
    730706      clock … code_memory … final = clock … code_memory … initial + (Σ_{i < |ctrace|} (tech_cost_of_label cost_labels cost_map ? ctrace i)).
    731707  [1:
    732     #code_memory #total_program_size #total_program_size_invariant #good_program_witness
    733     #cost_labels #cost_labels_injective #reachable_program_counter_witness #initial #final #trace
    734     #unrepeating_witness
     708    #code_memory #cost_labels #cost_labels_injective #initial #final #trace #unrepeating_witness
    735709    @compute_max_trace_label_return_cost_ok_with_trace_aux try assumption
    736710  |2:
     
    738712  ]
    739713  normalize nodelta
    740   cases (traverse_code ? ? ? ? ? ? ?)
     714  cases (traverse_code ???)
    741715  #cost_map * #dom_codom #codom_dom try assumption
    742716  #pc #k #lookup_opt_assm @(dom_codom … lookup_opt_assm)
    743717  lapply (sym_eq ? ? ? lookup_opt_assm)
    744718  -lookup_opt_assm #lookup_opt_assm
    745   cases (reachable_program_counter_witness … lookup_opt_assm)
    746   #fetch_n_assm #relevant assumption
    747 qed.
     719  @nat_of_bitvector_lt_bound
     720qed.
Note: See TracChangeset for help on using the changeset viewer.