Changeset 1900


Ignore:
Timestamp:
Apr 23, 2012, 6:22:28 PM (7 years ago)
Author:
mulligan
Message:

CostProof? complete, modulo some daemons and axioms in earlier files

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CostsProof.ma

    r1898 r1900  
    601601 (codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k))
    602602 on trace:
    603  ∀dom_codom:(∀k. ∀k_pres:present … cost_map k. pc. lookup_opt … pc cost_labels = Some … k →
     603 ∀dom_codom:(∀k. ∀k_pres:present … cost_map k. pc. lookup_opt … pc cost_labels = Some … k →
    604604   ∃reachable_witness: reachable_program_counter cm total_program_size pc.
    605605   pi1 … (block_cost cm pc total_program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres).
     
    616616 (trace: trace_any_label (ASM_abstract_status cm cost_labels) trace_ends_flag initial final)
    617617 (codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k))
    618  (dom_codom:(∀k. ∀k_pres:present … cost_map k. pc. lookup_opt … pc cost_labels = Some … k →
     618 (dom_codom:(∀k. ∀k_pres:present … cost_map k. pc. lookup_opt … pc cost_labels = Some … k →
    619619   ∃reachable_witness: reachable_program_counter cm total_program_size pc.
    620620   pi1 … (block_cost cm pc total_program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres))
     
    632632 (trace: trace_label_label (ASM_abstract_status cm cost_labels) trace_ends_flag initial final)
    633633 (codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k))
    634  (dom_codom:(∀k. ∀k_pres:present … cost_map k. pc. lookup_opt … pc cost_labels = Some … k →
     634 (dom_codom:(∀k. ∀k_pres:present … cost_map k. pc. lookup_opt … pc cost_labels = Some … k →
    635635   ∃reachable_witness: reachable_program_counter cm total_program_size pc.
    636636   pi1 … (block_cost cm pc total_program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres))
     
    664664      <(tech_cost_of_label_shift ??? [?] ? i) //
    665665    |2:
    666       whd in ⊢ (???%); (* XXX: should be easy *)
    667       cases daemon
     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        #_ #assm >assm %
     681      ]
    668682    ]
    669683  |3:
     
    707721  ∀trace: trace_label_return (ASM_abstract_status code_memory cost_labels) initial final.
    708722  ∀codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k).
    709   ∀dom_codom: (∀k. ∀k_pres:present … cost_map k. pc. lookup_opt … pc cost_labels = Some … k →
     723  ∀dom_codom: (∀k. ∀k_pres:present … cost_map k. pc. lookup_opt … pc cost_labels = Some … k →
    710724    ∃reachable_witness: reachable_program_counter code_memory total_program_size pc.
    711725      pi1 … (block_cost code_memory pc total_program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres).
     
    725739  ∀good_program_witness: good_program code_memory total_program_size.
    726740  ∀cost_labels: BitVectorTrie costlabel 16.
     741  ∀cost_labels_injective:
     742   (∀pc,pc',l.
     743     lookup_opt costlabel 16 pc cost_labels=Some costlabel l
     744      →lookup_opt costlabel 16 pc' cost_labels=Some costlabel l→pc=pc').
    727745  ∀reachable_program_counter_witness:
    728746    ∀lbl: costlabel.
     
    733751  ∀final: Status code_memory.
    734752  ∀trace: trace_label_return (ASM_abstract_status code_memory cost_labels) initial final.
    735     let cost_map ≝ traverse_code code_memory cost_labels total_program_size total_program_size_invariant
     753    let cost_map ≝ traverse_code code_memory cost_labels cost_labels_injective total_program_size total_program_size_invariant
    736754      reachable_program_counter_witness good_program_witness in
    737755    let ctrace ≝ compute_cost_trace_label_return code_memory … trace in
     
    739757  [1:
    740758    #code_memory #total_program_size #total_program_size_invariant #good_program_witness
    741     #cost_labels #reachable_program_counter_witness #initial #final #trace
     759    #cost_labels #cost_labels_injective #reachable_program_counter_witness #initial #final #trace
    742760    @compute_max_trace_label_return_cost_ok_with_trace_aux try assumption
    743761  |2:
     
    745763  ]
    746764  normalize nodelta
    747   cases (traverse_code ? ? ? ? ? ?)
     765  cases (traverse_code ? ? ? ? ? ? ?)
    748766  #cost_map * #dom_codom #codom_dom try assumption
    749767  #pc #k #lookup_opt_assm @(dom_codom … lookup_opt_assm)
Note: See TracChangeset for help on using the changeset viewer.