Changeset 1898


Ignore:
Timestamp:
Apr 23, 2012, 4:36:19 PM (7 years ago)
Author:
mulligan
Message:

Ported changes from ASMCosts.ma into CostsProof?.ma and got everything compiling again

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CostsProof.ma

    r1695 r1898  
    1 include "ASM/ASMCosts.ma".
     1include "ASM/ASMCostsSplit.ma".
    22include "ASM/WellLabeled.ma".
    33include "ASM/Status.ma".
    44include "common/StructuredTraces.ma".
    55include "arithmetics/bigops.ma".
     6
    67include alias "arithmetics/nat.ma".
    78include alias "basics/logic.ma".
     
    6263include alias "arithmetics/nat.ma".
    6364
     65lemma execute_1_ok_clock:
     66  ∀cm.
     67  ∀s.
     68    clock ?? (execute_1 cm s) = current_instruction_cost … s + clock … s.
     69  #cm #s cases (execute_1_ok cm s) #clock_assm #_ assumption
     70qed-.
     71
    6472let rec compute_max_trace_label_label_cost_is_ok
    6573  (cm: ?)
     
    94102      #start_status #final_status #is_next #is_not_return try (#is_costed)
    95103      change with (current_instruction_cost cm start_status) in ⊢ (???(?%?));
    96       cases(is_next) @execute_1_ok
     104      cases(is_next) @execute_1_ok_clock
    97105    |3:
    98106      #status_pre_fun_call #status_start_fun_call #status_final #is_next
     
    101109      >(compute_max_trace_label_return_cost_is_ok … call_trace)
    102110      >associative_plus @eq_f cases(is_next)
    103       >execute_1_ok %
     111      @execute_1_ok_clock
    104112    |4:
    105113      #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
     
    116124        status_after_fun_call call_trace)
    117125      cases(is_next) in match (clock … cm status_start_fun_call);
    118       >(execute_1_ok … status_pre_fun_call)
     126      >(execute_1_ok_clock cm status_pre_fun_call)
    119127      <associative_plus in ⊢ (??%?);
    120128      <commutative_plus in match (
     
    138146         status_init status_end trace_any_label)
    139147      cases(is_next) in match (clock … cm status_init);
    140       >(execute_1_ok cm status_pre)
     148      >(execute_1_ok_clock … status_pre)
    141149      >commutative_plus >associative_plus >associative_plus @eq_f
    142150      @commutative_plus
     
    689697qed.
    690698 
    691 lemma compute_max_trace_label_return_cost_ok_with_trace:
     699lemma compute_max_trace_label_return_cost_ok_with_trace_aux:
    692700  ∀code_memory: BitVectorTrie Byte 16.
    693701  ∀total_program_size: nat.
     
    710718  >commutative_plus >compute_trace_label_return_cost_using_paid_ok //
    711719qed.
     720
     721theorem compute_max_trace_label_return_cost_ok_with_trace:
     722  ∀code_memory: BitVectorTrie Byte 16.
     723  ∀total_program_size: nat.
     724  ∀total_program_size_invariant: total_program_size ≤ 2^16.
     725  ∀good_program_witness: good_program code_memory total_program_size.
     726  ∀cost_labels: BitVectorTrie costlabel 16.
     727  ∀reachable_program_counter_witness:
     728    ∀lbl: costlabel.
     729    ∀program_counter: Word.
     730      Some costlabel lbl=lookup_opt costlabel 16 program_counter cost_labels →
     731        reachable_program_counter code_memory total_program_size program_counter.
     732  ∀initial: Status code_memory.
     733  ∀final: Status code_memory.
     734  ∀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
     736      reachable_program_counter_witness good_program_witness in
     737    let ctrace ≝ compute_cost_trace_label_return code_memory … trace in
     738      clock … code_memory … final = clock … code_memory … initial + (Σ_{i < |ctrace|} (tech_cost_of_label cost_labels cost_map ? ctrace i)).
     739  [1:
     740    #code_memory #total_program_size #total_program_size_invariant #good_program_witness
     741    #cost_labels #reachable_program_counter_witness #initial #final #trace
     742    @compute_max_trace_label_return_cost_ok_with_trace_aux try assumption
     743  |2:
     744    skip
     745  ]
     746  normalize nodelta
     747  cases (traverse_code ? ? ? ? ? ?)
     748  #cost_map * #dom_codom #codom_dom try assumption
     749  #pc #k #lookup_opt_assm @(dom_codom … lookup_opt_assm)
     750  lapply (sym_eq ? ? ? lookup_opt_assm)
     751  -lookup_opt_assm #lookup_opt_assm
     752  cases (reachable_program_counter_witness … lookup_opt_assm)
     753  #fetch_n_assm #relevant assumption
     754qed.
Note: See TracChangeset for help on using the changeset viewer.