Changeset 1921 for src/ASM/CostsProof.ma


Ignore:
Timestamp:
May 8, 2012, 3:29:25 PM (8 years ago)
Author:
mulligan
Message:

Horror proof mostly finished (compiles all way until end of CostsProof?.ma).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CostsProof.ma

    r1919 r1921  
    594594(* XXX: here *)
    595595let rec compute_trace_label_return_using_paid_ok_with_trace
    596  (cm: ?) (total_program_size: nat) (good_program_witness: good_program cm total_program_size)
     596 (cm: ?) (total_program_size: nat) (total_program_size_limit: total_program_size ≤ 2^16)
     597 (good_program_witness: good_program cm total_program_size)
    597598 (cost_labels: BitVectorTrie costlabel 16)
    598599 (cost_map: identifier_map CostTag nat)
     
    601602 (codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k))
    602603 on trace:
     604 ∀unrepeating_witness: tlr_unrepeating … trace.
    603605 ∀dom_codom:(∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc cost_labels = Some … k →
    604606   ∃reachable_witness: reachable_program_counter cm total_program_size pc.
    605    pi1 … (block_cost cm pc total_program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres).
     607   pi1 … (block_cost cm pc total_program_size total_program_size_limit cost_labels reachable_witness good_program_witness) = lookup_present … k_pres).
    606608  let ctrace ≝ compute_cost_trace_label_return cm … trace in
    607609  compute_trace_label_return_cost_using_paid cm … trace =
     
    609611    ≝ ?
    610612and compute_trace_any_label_using_paid_ok_with_trace
    611  (cm: ?) (total_program_size: nat) (good_program_witness: good_program cm total_program_size)
     613 (cm: ?) (total_program_size: nat) (total_program_size_limit: total_program_size ≤ 2^16)
     614 (good_program_witness: good_program cm total_program_size)
    612615 (cost_labels: BitVectorTrie costlabel 16)
    613616 (trace_ends_flag: trace_ends_with_ret)
     
    618621 (dom_codom:(∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc cost_labels = Some … k →
    619622   ∃reachable_witness: reachable_program_counter cm total_program_size pc.
    620    pi1 … (block_cost cm pc total_program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres))
     623   pi1 … (block_cost cm pc total_program_size total_program_size_limit cost_labels reachable_witness good_program_witness) = lookup_present … k_pres))
    621624 on trace:
     625  ∀unrepeating_witness: tal_unrepeating … trace.
    622626  let ctrace ≝ compute_cost_trace_any_label … trace in
    623627  compute_trace_any_label_cost_using_paid … trace =
     
    625629    ≝ ?
    626630and compute_trace_label_label_using_paid_ok_with_trace
    627  (cm: ?) (total_program_size: nat) (good_program_witness: good_program cm total_program_size)
     631 (cm: ?) (total_program_size: nat) (total_program_size_limit: total_program_size ≤ 2^16)
     632 (good_program_witness: good_program cm total_program_size)
    628633 (cost_labels: BitVectorTrie costlabel 16)
    629634 (trace_ends_flag: trace_ends_with_ret)
     
    631636 (initial: Status cm) (final: Status cm)
    632637 (trace: trace_label_label (ASM_abstract_status cm cost_labels) trace_ends_flag initial final)
     638 (unrepeating_witness: tll_unrepeating … trace)
    633639 (codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k))
    634640 (dom_codom:(∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc cost_labels = Some … k →
    635641   ∃reachable_witness: reachable_program_counter cm total_program_size pc.
    636    pi1 … (block_cost cm pc total_program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres))
     642   pi1 … (block_cost cm pc total_program_size total_program_size_limit cost_labels reachable_witness good_program_witness) = lookup_present … k_pres))
    637643 on trace:
     644 ∀unrepeating_witness: tll_unrepeating … trace.
    638645  let ctrace ≝ compute_cost_trace_label_label … trace in
    639646  compute_trace_label_label_cost_using_paid … trace =
     
    641648    ≝ ?.
    642649  cases trace normalize nodelta
    643   [ #sb #sa #tr #dom_codom whd in ⊢ (??%?);
     650  [ #sb #sa #tr #unrepeating_witness #dom_codom whd in ⊢ (??%?);
    644651    whd in match (compute_cost_trace_label_return ?????);
    645     @(compute_trace_label_label_using_paid_ok_with_trace … good_program_witness) @dom_codom
    646   | #si #sl #sf #tr1 #tr2 #dom_codom
     652    @(compute_trace_label_label_using_paid_ok_with_trace … good_program_witness)
     653    assumption
     654  | #si #sl #sf #tr1 #tr2 #unrepeating_witness #dom_codom
    647655    whd in ⊢ (??%?);
    648656    whd in match (compute_cost_trace_label_return ?????);
    649657    >append_length >bigop_sum_rev >commutative_plus @eq_f2
    650     [ >(compute_trace_label_return_using_paid_ok_with_trace … good_program_witness … cost_map … codom_dom dom_codom)
     658    [ >(compute_trace_label_return_using_paid_ok_with_trace … good_program_witness … cost_map … codom_dom ? dom_codom)
    651659      -compute_trace_label_return_using_paid_ok_with_trace
    652       @same_bigop [//] #i #H #_ -dom_codom @tech_cost_of_label_shift //
     660      [1:
     661        @same_bigop [//] #i #H #_ -dom_codom @tech_cost_of_label_shift //
     662      |2:
     663        inversion unrepeating_witness
     664        #tll_unrepeating #tlr_unrepeating #_ assumption
     665      ]
    653666    | >(compute_trace_label_label_using_paid_ok_with_trace … good_program_witness … cost_map … codom_dom … dom_codom)
    654667      -compute_trace_label_label_using_paid_ok_with_trace
    655       @same_bigop [//] #i #H #_ @(tech_cost_of_label_prefix … H)
     668      [1:
     669        @same_bigop [//] #i #H #_ @(tech_cost_of_label_prefix … H)
     670      |2,3:
     671        inversion unrepeating_witness
     672        #tll_unrepeating #tlr_unrepeating #_ assumption
     673      ]
    656674    ]
    657675  |8:
    658676    #end_flag #start_status #end_status #trace_any_label #costed_assm
     677    #unrepeating_witness
    659678    whd in ⊢ (??%?); whd in ⊢ (??(?%?)?);
    660679    >(compute_trace_any_label_using_paid_ok_with_trace … good_program_witness … cost_map … codom_dom … dom_codom)
    661     >bigop_0 in ⊢ (???%); >commutative_plus @eq_f2
    662680    [1:
    663       @same_bigop [//] #i #H #_ -dom_codom >(plus_n_O i) >plus_n_Sm
    664       <(tech_cost_of_label_shift ??? [?] ? i) //
     681      >bigop_0 in ⊢ (???%); >commutative_plus @eq_f2
     682      [1:
     683        @same_bigop [//] #i #H #_ -dom_codom >(plus_n_O i) >plus_n_Sm
     684        <(tech_cost_of_label_shift ??? [?] ? i) //
     685      |2:
     686        change with (? = lookup_present ? ? ? ? ?)
     687        generalize in match (tech_cost_of_label0 ? ? ? ? ? ?);
     688        normalize in match (nth_safe ? ? ? ?);
     689        whd in costed_assm; lapply costed_assm -costed_assm   
     690        inversion (lookup_opt ? ? (program_counter … cm start_status) cost_labels)
     691        [1:
     692          #_ #absurd cases absurd
     693        |2:
     694          normalize nodelta #cost_label #Some_assm #_ #p
     695          cases (dom_codom ? p ? Some_assm)
     696          #reachable_witness #block_cost_assm <block_cost_assm
     697          cases (block_cost ???????)
     698          #cost -block_cost_assm #block_cost_assm
     699          cases (block_cost_assm ??? trace_any_label ???)
     700          try @refl
     701          [1:
     702            assumption
     703          |2:
     704            (* XXX: !!! *)
     705            cases daemon
     706          ]
     707        ]
     708      ]
    665709    |2:
    666       change with (? = lookup_present ? ? ? ? ?)
    667       generalize in match (tech_cost_of_label0 ? ? ? ? ? ?);
    668       normalize in match (nth_safe ? ? ? ?);
    669       whd in costed_assm; lapply costed_assm -costed_assm   
    670       inversion (lookup_opt ? ? (program_counter … cm start_status) cost_labels)
    671       [1:
    672         #_ #absurd cases absurd
    673       |2:
    674         normalize nodelta #cost_label #Some_assm #_ #p
    675         cases (dom_codom ? p ? Some_assm)
    676         #reachable_witness #block_cost_assm <block_cost_assm
    677         cases (block_cost ? ? ? ? ? ?)
    678         #cost -block_cost_assm #block_cost_assm
    679         cases (block_cost_assm ? ? ? trace_any_label ? (refl …))
    680         try % (* XXX: assumption about length of trace *) cases daemon
    681       ]
     710      assumption
    682711    ]
    683712  |3:
    684713    #start_status #final_status #execute_assm #classifier_assm #costed_assm
     714    #unrepeating_witness
    685715    %
    686716  |4:
    687     #start_status #final_status #execute_assm #classifier_assm %
     717    #start_status #final_status #execute_assm #classifier_assm #unrepeating_witness
     718    %
    688719  |5:
    689720    #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
    690     #classifier_assm #after_return_assm #trace_label_return #costed_assm
     721    #classifier_assm #after_return_assm #trace_label_return #costed_assm #unrepeating_witness
    691722    whd in ⊢ (??%?);
    692     @(compute_trace_label_return_using_paid_ok_with_trace … good_program_witness … cost_map … codom_dom dom_codom)
     723    @(compute_trace_label_return_using_paid_ok_with_trace … good_program_witness … cost_map … codom_dom ? dom_codom)
     724    assumption
    693725  |6:
    694726    #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
    695727    #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
    696     #costed_assm #trace_any_label
     728    #costed_assm #trace_any_label #unrepeating_witness
    697729    whd in ⊢ (??%?);
    698     >(compute_trace_label_return_using_paid_ok_with_trace … good_program_witness … cost_map … codom_dom dom_codom)
    699     >(compute_trace_any_label_using_paid_ok_with_trace … good_program_witness … cost_map … codom_dom … dom_codom)
    700     >length_append >bigop_sum_rev >commutative_plus @eq_f2
    701     [ @same_bigop [2: #i #H #_ -dom_codom @tech_cost_of_label_shift assumption
    702                   |1: #i #H % ]
    703     | @same_bigop [#i #H %] #i #H #_ @(tech_cost_of_label_prefix … H)
     730    >(compute_trace_label_return_using_paid_ok_with_trace … good_program_witness … cost_map … codom_dom ? dom_codom)
     731    [1:
     732      >(compute_trace_any_label_using_paid_ok_with_trace … good_program_witness … cost_map … codom_dom … dom_codom)
     733      [1:
     734        >length_append >bigop_sum_rev >commutative_plus @eq_f2
     735        [ @same_bigop [2: #i #H #_ -dom_codom @tech_cost_of_label_shift assumption
     736                      |1: #i #H % ]
     737        | @same_bigop [#i #H %] #i #H #_ @(tech_cost_of_label_prefix … H)
     738        ]
     739      |2:
     740        inversion unrepeating_witness
     741        * #memb_1 #tal_unrepeating #tlr_unrepeating #_ assumption
     742      ]
     743    |2:
     744      inversion unrepeating_witness
     745      * #memb_1 #tal_unrepeating #tlr_unrepeating #_ assumption
    704746    ]
    705747  |7:
    706748    #end_flag #status_pre_fun_call #status_start_fun_call #status_final
    707     #execute_assm #trace_any_label #classifier_assm #costed_assm
     749    #execute_assm #trace_any_label #classifier_assm #costed_assm #unrepeating_witness
    708750    whd in ⊢ (??%?);
    709751    @(compute_trace_any_label_using_paid_ok_with_trace … good_program_witness … cost_map … codom_dom … dom_codom)
     752    inversion unrepeating_witness
     753    #memb_1 #tal_unrepeating #_ assumption
    710754  ]
    711755qed.
     
    714758  ∀code_memory: BitVectorTrie Byte 16.
    715759  ∀total_program_size: nat.
     760  ∀total_program_size_limit: total_program_size ≤ 2^16.
    716761  ∀good_program_witness: good_program code_memory total_program_size.
    717762  ∀cost_labels: BitVectorTrie costlabel 16.
     
    720765  ∀final: Status code_memory.
    721766  ∀trace: trace_label_return (ASM_abstract_status code_memory cost_labels) initial final.
     767  ∀unrepeating_witness: tlr_unrepeating … trace.
    722768  ∀codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k).
    723769  ∀dom_codom: (∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc cost_labels = Some … k →
    724770    ∃reachable_witness: reachable_program_counter code_memory total_program_size pc.
    725       pi1 … (block_cost code_memory pc total_program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres).
     771      pi1 … (block_cost code_memory pc total_program_size total_program_size_limit cost_labels reachable_witness good_program_witness) = lookup_present … k_pres).
    726772        let ctrace ≝ compute_cost_trace_label_return code_memory … trace in
    727773          clock … code_memory … final =
    728774            clock … code_memory … initial + (Σ_{i < |ctrace|} (tech_cost_of_label cost_labels cost_map codom_dom ctrace i)).
    729   #code_memory #total_program_size #good_program_witness #cost_labels #cost_map
    730   #initial #final #trace #codom_dom #dom_codom normalize nodelta
     775  #code_memory #total_program_size #total_program_size_limit
     776  #good_program_witness #cost_labels #cost_map
     777  #initial #final #trace #unrepeating_witness #codom_dom #dom_codom normalize nodelta
    731778  <compute_trace_label_return_using_paid_ok_with_trace try assumption
    732779  >commutative_plus >compute_trace_label_return_cost_using_paid_ok //
     
    751798  ∀final: Status code_memory.
    752799  ∀trace: trace_label_return (ASM_abstract_status code_memory cost_labels) initial final.
     800  ∀unrepeating_witness: tlr_unrepeating … trace.
    753801    let cost_map ≝ traverse_code code_memory cost_labels cost_labels_injective total_program_size total_program_size_invariant
    754802      reachable_program_counter_witness good_program_witness in
     
    758806    #code_memory #total_program_size #total_program_size_invariant #good_program_witness
    759807    #cost_labels #cost_labels_injective #reachable_program_counter_witness #initial #final #trace
     808    #unrepeating_witness
    760809    @compute_max_trace_label_return_cost_ok_with_trace_aux try assumption
    761810  |2:
Note: See TracChangeset for help on using the changeset viewer.