Changeset 2498 for src/ASM/ASMCosts.ma


Ignore:
Timestamp:
Nov 27, 2012, 6:01:50 PM (7 years ago)
Author:
mckinna
Message:

Refactor:
Typedefs object_code and costlabel_map lifted out from ASMCostsSplit.ma
Dependencies simplified.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r2475 r2498  
    55include "common/StructuredTraces.ma".
    66
    7 definition ASM_abstract_status: ∀code_memory. BitVectorTrie costlabel 16 → abstract_status ≝
     7(* moved to Fetch.ma *)
     8(* definition costlabel_map ≝ BitVectorTrie costlabel 16.   *)
     9
     10definition ASM_abstract_status: ∀code_memory. costlabel_map → abstract_status ≝
    811  λcode_memory.
    912  λcost_labels.
     
    2326definition trace_any_label_length ≝
    2427  λcode_memory: BitVectorTrie Byte 16.
    25   λcost_labels: BitVectorTrie costlabel 16.
     28  λcost_labels: costlabel_map.
    2629  λtrace_ends_flag: trace_ends_with_ret.
    2730  λstart_status: Status code_memory.
     
    139142lemma sublist_tal_pc_list_all_program_counter_list:
    140143  ∀code_memory: BitVectorTrie Byte 16.
    141   ∀cost_labels: BitVectorTrie costlabel 16.
     144  ∀cost_labels: costlabel_map.
    142145  ∀start, final: Status code_memory.
    143146  ∀trace_ends_flag.
     
    152155corollary tal_pc_list_length_leq_total_program_size:
    153156  ∀code_memory: BitVectorTrie Byte 16.
    154   ∀cost_labels: BitVectorTrie costlabel 16.
     157  ∀cost_labels: costlabel_map.
    155158  ∀start, final: Status code_memory.
    156159  ∀trace_ends_flag.
     
    171174
    172175let rec compute_paid_trace_any_label
    173   (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
     176  (code_memory: BitVectorTrie Byte 16) (cost_labels: costlabel_map)
    174177    (trace_ends_flag: trace_ends_with_ret) (start_status: Status code_memory)
    175178      (final_status: Status code_memory)
     
    196199definition compute_paid_trace_label_label ≝
    197200  λcode_memory: BitVectorTrie Byte 16.
    198   λcost_labels: BitVectorTrie costlabel 16.
     201  λcost_labels: costlabel_map.
    199202  λtrace_ends_flag: trace_ends_with_ret.
    200203  λstart_status: Status code_memory.
     
    209212  ∀code_memory' : (BitVectorTrie Byte 16).
    210213  ∀program_counter' : Word.
    211   ∀cost_labels : (BitVectorTrie costlabel 16).
     214  ∀cost_labels : costlabel_map.
    212215  ∀program_size' : ℕ.
    213216  ∀ticks : ℕ.
     
    363366  ∀code_memory': BitVectorTrie Byte 16.
    364367  ∀program_counter': Word.
    365   ∀cost_labels: BitVectorTrie costlabel 16.
     368  ∀cost_labels: costlabel_map.
    366369  ∀first_time_around: bool.
    367370  ∀program_size': ℕ.
     
    418421  ∀code_memory' : (BitVectorTrie Byte 16).
    419422  ∀program_counter' : Word.
    420   ∀cost_labels : (BitVectorTrie costlabel 16).
     423  ∀cost_labels : costlabel_map.
    421424  ∀program_size' : ℕ.
    422425  ∀ticks : ℕ.
     
    555558  ∀code_memory' : (BitVectorTrie Byte 16).
    556559  ∀program_counter' : Word.
    557   ∀cost_labels : (BitVectorTrie costlabel 16).
     560  ∀cost_labels : costlabel_map.
    558561  ∀program_size' : ℕ.
    559562  ∀ticks : ℕ.
     
    613616lemma trace_any_label_length_leq_0_to_False:
    614617  ∀code_memory: BitVectorTrie Byte 16.
    615   ∀cost_labels: BitVectorTrie costlabel 16.
     618  ∀cost_labels: costlabel_map.
    616619  ∀trace_ends_flag: trace_ends_with_ret.
    617620  ∀start_status: Status code_memory.
     
    627630let rec block_cost'
    628631  (code_memory': BitVectorTrie Byte 16) (program_counter': Word)
    629     (program_size: nat) (cost_labels: BitVectorTrie costlabel 16)
     632    (program_size: nat) (cost_labels: costlabel_map)
    630633      (first_time_around: bool)
    631634        on program_size:
     
    760763    ∀code_memory': BitVectorTrie Byte 16.
    761764    ∀program_counter': Word.
    762     ∀cost_labels: BitVectorTrie costlabel 16.
     765    ∀cost_labels: costlabel_map.
    763766      Σcost_of_block: nat.
    764767        ∀start_status: Status code_memory'.
     
    771774  λcode_memory: BitVectorTrie Byte 16.
    772775  λprogram_counter: Word.
    773   λcost_labels: BitVectorTrie costlabel 16. ?.
     776  λcost_labels: costlabel_map. ?.
    774777  cases(block_cost' code_memory program_counter (2^16) cost_labels true)
    775778  #cost_of_block #block_cost_hyp
Note: See TracChangeset for help on using the changeset viewer.