Changeset 2516 for src/ASM/ASMCosts.ma


Ignore:
Timestamp:
Dec 2, 2012, 5:45:36 PM (7 years ago)
Author:
mckinna
Message:

removed typedefs; restored older versions; moved typedefs to compiler.ma
AssemblyProofSplit? *still* doesn't typecheck: disambiguation errors!

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r2504 r2516  
    88(* definition costlabel_map ≝ BitVectorTrie costlabel 16.   *)
    99
    10 definition ASM_abstract_status: ∀code_memory. costlabel_map → abstract_status ≝
     10definition ASM_abstract_status: ∀code_memory. BitVectorTrie costlabel 16 → abstract_status ≝
    1111  λcode_memory.
    1212  λcost_labels.
     
    2626definition trace_any_label_length ≝
    2727  λcode_memory: BitVectorTrie Byte 16.
    28   λcost_labels: costlabel_map.
     28  λcost_labels: BitVectorTrie costlabel 16.
    2929  λtrace_ends_flag: trace_ends_with_ret.
    3030  λstart_status: Status code_memory.
     
    142142lemma sublist_tal_pc_list_all_program_counter_list:
    143143  ∀code_memory: BitVectorTrie Byte 16.
    144   ∀cost_labels: costlabel_map.
     144  ∀cost_labels: BitVectorTrie costlabel 16.
    145145  ∀start, final: Status code_memory.
    146146  ∀trace_ends_flag.
     
    155155corollary tal_pc_list_length_leq_total_program_size:
    156156  ∀code_memory: BitVectorTrie Byte 16.
    157   ∀cost_labels: costlabel_map.
     157  ∀cost_labels: BitVectorTrie costlabel 16.
    158158  ∀start, final: Status code_memory.
    159159  ∀trace_ends_flag.
     
    174174
    175175let rec compute_paid_trace_any_label
    176   (code_memory: BitVectorTrie Byte 16) (cost_labels: costlabel_map)
     176  (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
    177177    (trace_ends_flag: trace_ends_with_ret) (start_status: Status code_memory)
    178178      (final_status: Status code_memory)
     
    199199definition compute_paid_trace_label_label ≝
    200200  λcode_memory: BitVectorTrie Byte 16.
    201   λcost_labels: costlabel_map.
     201  λcost_labels: BitVectorTrie costlabel 16.
    202202  λtrace_ends_flag: trace_ends_with_ret.
    203203  λstart_status: Status code_memory.
     
    212212  ∀code_memory' : (BitVectorTrie Byte 16).
    213213  ∀program_counter' : Word.
    214   ∀cost_labels : costlabel_map.
     214  ∀cost_labels : BitVectorTrie costlabel 16.
    215215  ∀program_size' : ℕ.
    216216  ∀ticks : ℕ.
     
    366366  ∀code_memory': BitVectorTrie Byte 16.
    367367  ∀program_counter': Word.
    368   ∀cost_labels: costlabel_map.
     368  ∀cost_labels: BitVectorTrie costlabel 16.
    369369  ∀first_time_around: bool.
    370370  ∀program_size': ℕ.
     
    421421  ∀code_memory' : (BitVectorTrie Byte 16).
    422422  ∀program_counter' : Word.
    423   ∀cost_labels : costlabel_map.
     423  ∀cost_labels : BitVectorTrie costlabel 16.
    424424  ∀program_size' : ℕ.
    425425  ∀ticks : ℕ.
     
    558558  ∀code_memory' : (BitVectorTrie Byte 16).
    559559  ∀program_counter' : Word.
    560   ∀cost_labels : costlabel_map.
     560  ∀cost_labels : BitVectorTrie costlabel 16.
    561561  ∀program_size' : ℕ.
    562562  ∀ticks : ℕ.
     
    616616lemma trace_any_label_length_leq_0_to_False:
    617617  ∀code_memory: BitVectorTrie Byte 16.
    618   ∀cost_labels: costlabel_map.
     618  ∀cost_labels: BitVectorTrie costlabel 16.
    619619  ∀trace_ends_flag: trace_ends_with_ret.
    620620  ∀start_status: Status code_memory.
     
    630630let rec block_cost'
    631631  (code_memory': BitVectorTrie Byte 16) (program_counter': Word)
    632     (program_size: nat) (cost_labels: costlabel_map)
     632    (program_size: nat) (cost_labels: BitVectorTrie costlabel 16)
    633633      (first_time_around: bool)
    634634        on program_size:
     
    763763    ∀code_memory': BitVectorTrie Byte 16.
    764764    ∀program_counter': Word.
    765     ∀cost_labels: costlabel_map.
     765    ∀cost_labels: BitVectorTrie costlabel 16.
    766766      Σcost_of_block: nat.
    767767        ∀start_status: Status code_memory'.
     
    774774  λcode_memory: BitVectorTrie Byte 16.
    775775  λprogram_counter: Word.
    776   λcost_labels: costlabel_map. ?.
     776  λcost_labels: BitVectorTrie costlabel 16. ?.
    777777  cases(block_cost' code_memory program_counter (2^16) cost_labels true)
    778778  #cost_of_block #block_cost_hyp
Note: See TracChangeset for help on using the changeset viewer.