Changeset 1558 for src/ASM


Ignore:
Timestamp:
Nov 24, 2011, 6:47:44 PM (8 years ago)
Author:
sacerdot
Message:

Snapshot before moving things to ASMCosts.ma.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CostsProof.ma

    r1556 r1558  
    579579qed.
    580580
     581(* ??????????????????????? *)
     582axiom block_cost_static_dynamic_ok:
     583 ∀cost_labels: BitVectorTrie costlabel 16.
     584 ∀trace_ends_flag.
     585 ∀start_status: Status.
     586 ∀final_status: Status.
     587 ∀the_trace:
     588  trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag
     589   start_status final_status.
     590 let mem ≝ code_memory … start_status in
     591 let pc ≝ program_counter … start_status in
     592 let program_size ≝ 2^16 in
     593  block_cost mem cost_labels pc program_size =
     594  compute_paid_trace_label_label cost_labels trace_ends_flag
     595   start_status final_status the_trace.
     596
    581597include "arithmetics/bigops.ma".
    582598
    583599lemma foo:
    584  ∀cost_label: BitVectorTrie costlabel 16.
     600 ∀cost_labels: BitVectorTrie costlabel 16.
     601 ∀cost_labels_inv: identifier_map CostTag Word.
    585602 ∀initial,final.
    586  ∀trace: trace_label_return (ASM_abstract_status cost_label) initial final.
     603 ∀trace: trace_label_return (ASM_abstract_status cost_labels) initial final.
     604  let dummy ≝ an_identifier ? one in
    587605  let ctrace ≝ compute_cost_trace_label_return … trace in
    588606  compute_max_trace_label_return_cost … trace =
    589    \big [ plus, 0 ]_{ i < |ctrace| } (? (nth i ? ctrace ?)).
    590  
    591   compute_cost_trace_label_return trace =
    592  
    593  
    594 
     607   \big [ plus, 0 ]_{ i < |ctrace| }
     608    (block_cost (code_memory … initial) cost_labels
     609     (lookup_present … cost_labels_inv (nth i ? ctrace dummy) ?) 2^16).
     610 [2: cases daemon (* ALL LABELS MUST BE PRESENT *)
     611 | #cost_labels #cost_labels_inv #initial #final #trace
     612   letin dummy ≝ (an_identifier CostTag one) normalize nodelta
     613   whd in match
    595614
    596615lemma
Note: See TracChangeset for help on using the changeset viewer.