Changeset 1929 for src/ASM/CostsProof.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/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.