Changeset 2498 for src/ASM


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.

Location:
src/ASM
Files:
9 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
  • src/ASM/ASMCostsSplit.ma

    r2475 r2498  
    55
    66let rec traverse_code_internal
    7   (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
     7  (code_memory: BitVectorTrie Byte 16) (cost_labels: costlabel_map)
    88    (program_counter: Word) (program_size: nat)
    99      (program_size_invariant: program_size = 0 ∨ nat_of_bitvector … program_counter + program_size = 2^16)
     
    279279definition traverse_code:
    280280  ∀code_memory: BitVectorTrie Byte 16.
    281   ∀cost_labels: BitVectorTrie costlabel 16.
     281  ∀cost_labels: costlabel_map.
    282282  ∀cost_labels_injective:
    283283    ∀pc, pc',l.
     
    289289          pi1 … (block_cost code_memory pc cost_labels) = lookup_present … k_pres) ≝
    290290  λcode_memory: BitVectorTrie Byte 16.
    291   λcost_labels: BitVectorTrie costlabel 16.
     291  λcost_labels: costlabel_map.
    292292  λcost_labels_injective.
    293293    pi1 ? ? (traverse_code_internal code_memory cost_labels (zero …) (2^16) ?).
     
    318318definition compute_costs ≝
    319319  λprogram: list Byte.
    320   λcost_labels: BitVectorTrie costlabel 16.
     320  λcost_labels: costlabel_map.
    321321  λcost_labels_injective:
    322322    ∀pc, pc',l.
     
    327327      traverse_code code_memory cost_labels cost_labels_injective.
    328328
    329 definition object_code ≝ list Byte.
    330 definition costlabel_map ≝ BitVectorTrie costlabel 16.     
     329(* definition object_code ≝ list Byte. *)
    331330
     331(* use of this defn in ASM/CostsProof.ma is ill-typed *)
    332332definition ASM_cost_map :
    333333  ∀p.let code_memory ≝ load_code_memory (\fst p) in
  • src/ASM/AbstractStatus.ma

    r1944 r2498  
    4848definition current_instruction_label ≝
    4949  λcode_memory.
    50   λcost_labels: BitVectorTrie costlabel 16.
     50  λcost_labels: costlabel_map.
    5151  λs: Status code_memory.
    5252  let pc ≝ program_counter … code_memory s in
  • src/ASM/Assembly.ma

    r2316 r2498  
    783783    ∀sigma: Word → Word.
    784784    ∀policy: Word → bool.
    785       Σres:list Byte × (BitVectorTrie costlabel 16).
     785      Σres:list Byte × costlabel_map.
    786786       sigma_policy_specification p sigma policy →
    787787       let 〈preamble,instr_list〉 ≝ p in
  • src/ASM/AssemblyProof.ma

    r2284 r2498  
    192192  ∀sigma_policy_witness: sigma_policy_specification program sigma policy.
    193193  ∀assembled.
    194   ∀costs': BitVectorTrie costlabel 16.
     194  ∀costs': costlabel_map.
    195195  let 〈preamble, instr_list〉 ≝ program in
    196196  let 〈labels, costs〉 ≝ create_label_cost_map instr_list in
  • src/ASM/AssemblyProofSplit.ma

    r2301 r2498  
    113113  ∀EQppc: ppc = program_counter pseudo_assembly_program cm ps.
    114114  ∀labels: label_map.
    115   ∀costs: BitVectorTrie costlabel 16.
     115  ∀costs: costlabel_map.
    116116  ∀create_label_cost_refl: create_label_cost_map instr_list = 〈labels, costs〉.
    117117  ∀newppc: Word.
  • src/ASM/CostsProof.ma

    r2057 r2498  
    1010let rec compute_max_trace_label_label_cost
    1111  (cm: ?)
    12   (cost_labels: BitVectorTrie costlabel 16)
     12  (cost_labels: costlabel_map)
    1313   (trace_ends_flag: trace_ends_with_ret)
    1414    (start_status: Status cm) (final_status: Status cm)
     
    2121and compute_max_trace_any_label_cost
    2222  (cm: ?)
    23   (cost_labels: BitVectorTrie costlabel 16)
     23  (cost_labels: costlabel_map)
    2424  (trace_ends_flag: trace_ends_with_ret)
    2525   (start_status: Status cm) (final_status: Status cm)
     
    4949and compute_max_trace_label_return_cost
    5050  (cm: ?)
    51   (cost_labels: BitVectorTrie costlabel 16)
     51  (cost_labels: costlabel_map)
    5252  (start_status: Status cm) (final_status: Status cm)
    5353    (the_trace: trace_label_return (ASM_abstract_status cm cost_labels) start_status final_status)
     
    6565let rec compute_max_trace_label_label_cost_is_ok
    6666  (cm: ?)
    67   (cost_labels: BitVectorTrie costlabel 16)
     67  (cost_labels: costlabel_map)
    6868   (trace_ends_flag: trace_ends_with_ret)
    6969    (start_status: Status cm) (final_status: Status cm)
     
    7373and compute_max_trace_any_label_cost_is_ok
    7474  (cm: ?)
    75   (cost_labels: BitVectorTrie costlabel 16)
     75  (cost_labels: costlabel_map)
    7676  (trace_ends_flag: trace_ends_with_ret)
    7777   (start_status: Status cm) (final_status: Status cm)
     
    8181and compute_max_trace_label_return_cost_is_ok
    8282  (cm: ?)
    83   (cost_labels: BitVectorTrie costlabel 16)
     83  (cost_labels: costlabel_map)
    8484  (start_status: Status cm) (final_status: Status cm)
    8585    (the_trace: trace_label_return (ASM_abstract_status cm cost_labels) start_status final_status)
     
    164164let rec compute_trace_label_label_cost_using_paid
    165165  (cm: ?)
    166   (cost_labels: BitVectorTrie costlabel 16)
     166  (cost_labels: costlabel_map)
    167167   (trace_ends_flag: trace_ends_with_ret)
    168168    (start_status: Status cm) (final_status: Status cm)
     
    176176and compute_trace_any_label_cost_using_paid
    177177  (cm: ?)
    178   (cost_labels: BitVectorTrie costlabel 16)
     178  (cost_labels: costlabel_map)
    179179  (trace_ends_flag: trace_ends_with_ret)
    180180   (start_status: Status cm) (final_status: Status cm)
     
    197197and compute_trace_label_return_cost_using_paid
    198198  (cm: ?)
    199   (cost_labels: BitVectorTrie costlabel 16)
     199  (cost_labels: costlabel_map)
    200200  (start_status: Status cm) (final_status: Status cm)
    201201    (the_trace: trace_label_return (ASM_abstract_status cm cost_labels) start_status final_status)
     
    211211let rec compute_trace_label_label_cost_using_paid_ok
    212212  (cm: ?)
    213   (cost_labels: BitVectorTrie costlabel 16)
     213  (cost_labels: costlabel_map)
    214214   (trace_ends_flag: trace_ends_with_ret)
    215215    (start_status: Status cm) (final_status: Status cm)
     
    220220and compute_trace_any_label_cost_using_paid_ok
    221221  (cm: ?)
    222   (cost_labels: BitVectorTrie costlabel 16)
     222  (cost_labels: costlabel_map)
    223223  (trace_ends_flag: trace_ends_with_ret)
    224224   (start_status: Status cm) (final_status: Status cm)
     
    230230and compute_trace_label_return_cost_using_paid_ok
    231231  (cm: ?)
    232   (cost_labels: BitVectorTrie costlabel 16)
     232  (cost_labels: costlabel_map)
    233233  (start_status: Status cm) (final_status: Status cm)
    234234    (the_trace: trace_label_return (ASM_abstract_status cm cost_labels)
     
    271271let rec compute_cost_trace_label_label
    272272  (cm: BitVectorTrie Byte 16)
    273   (cost_labels: BitVectorTrie costlabel 16)
     273  (cost_labels: costlabel_map)
    274274   (trace_ends_flag: trace_ends_with_ret)
    275275    (start_status: Status cm) (final_status: Status cm)
     
    288288and compute_cost_trace_any_label
    289289  (cm: BitVectorTrie Byte 16)
    290   (cost_labels: BitVectorTrie costlabel 16)
     290  (cost_labels: costlabel_map)
    291291  (trace_ends_flag: trace_ends_with_ret)
    292292   (start_status: Status cm) (final_status: Status cm)
     
    309309and compute_cost_trace_label_return
    310310  (cm: BitVectorTrie Byte 16)
    311   (cost_labels: BitVectorTrie costlabel 16)
     311  (cost_labels: costlabel_map)
    312312  (start_status: Status cm) (final_status: Status cm)
    313313    (the_trace: trace_label_return (ASM_abstract_status cm cost_labels) start_status final_status)
     
    386386
    387387definition tech_cost_of_label0:
    388  ∀cost_labels: BitVectorTrie costlabel 16.
     388 ∀cost_labels: costlabel_map.
    389389 ∀cost_map: identifier_map CostTag nat.
    390390 ∀codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k).
     
    447447
    448448definition tech_cost_of_label:
    449  ∀cost_labels: BitVectorTrie costlabel 16.
     449 ∀cost_labels: costlabel_map.
    450450 ∀cost_map: identifier_map CostTag nat.
    451451 ∀codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k).
     
    501501   
    502502let rec compute_trace_label_return_using_paid_ok_with_trace
    503  (cm: ?) (cost_labels: BitVectorTrie costlabel 16)
     503 (cm: ?) (cost_labels: costlabel_map)
    504504 (cost_map: identifier_map CostTag nat)
    505505 (initial: Status cm) (final: Status cm)
     
    515515    ≝ ?
    516516and compute_trace_any_label_using_paid_ok_with_trace
    517  (cm: ?) (cost_labels: BitVectorTrie costlabel 16)
     517 (cm: ?) (cost_labels: costlabel_map)
    518518 (trace_ends_flag: trace_ends_with_ret)
    519519 (cost_map: identifier_map CostTag nat)
     
    530530    ≝ ?
    531531and compute_trace_label_label_using_paid_ok_with_trace
    532  (cm: ?) (cost_labels: BitVectorTrie costlabel 16)
     532 (cm: ?) (cost_labels: costlabel_map)
    533533 (trace_ends_flag: trace_ends_with_ret)
    534534 (cost_map: identifier_map CostTag nat)
     
    649649lemma compute_max_trace_label_return_cost_ok_with_trace_aux:
    650650  ∀code_memory: BitVectorTrie Byte 16.
    651   ∀cost_labels: BitVectorTrie costlabel 16.
     651  ∀cost_labels: costlabel_map.
    652652  ∀cost_map: identifier_map CostTag nat.
    653653  ∀initial: Status code_memory.
     
    669669theorem compute_max_trace_label_return_cost_ok_with_trace:
    670670  ∀code_memory: BitVectorTrie Byte 16.
    671   ∀cost_labels: BitVectorTrie costlabel 16.
     671  ∀cost_labels: costlabel_map.
    672672  ∀cost_labels_injective:
    673673   (∀pc,pc',l.
     
    697697 
    698698include "utilities/permutations.ma".
    699 
     699(*
     700lemma tech_cost_sum_eq_as_cost :
     701  ∀code_memory: object_code.
     702  ∀cost_labels: costlabel_map.
     703  ∀cost_map: identifier_map CostTag nat.
     704  ∀codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k).
     705  ∀trace.
     706  (Σ_{i < |trace|}(tech_cost_of_label cost_labels cost_map codom_dom trace i)) =
     707  (Σ_{l ∈ trace}(ASM_cost_map 〈code_memory, cost_labels〉 … codom_dom l)).
     708#cmem #clab #cmap #codom_dom #trace
     709@(list_elim_left … trace)
     710[ %
     711| #tl #hd #IH >append_length >commutative_plus
     712  >(fold_permute … (hd@[tl]) (tl::hd)) [2: @perm_swap_append ]
     713  whd in ⊢ (??%%); <IH
     714  <tech_cost_of_label_shift [2: %]
     715  cut (∀x,y,z,w.x = y → z = w → x + z = y + w) [ // ] #APP @APP -APP
     716  [ %
     717  | @sym_eq @same_bigop /2 by tech_cost_of_label_prefix/
     718  ]
     719]
     720qed.
     721*)
    700722lemma tech_cost_sum_eq_as_cost :
    701723  ∀code_memory: BitVectorTrie Byte 16.
    702   ∀cost_labels: BitVectorTrie costlabel 16.
     724  ∀cost_labels: costlabel_map.
    703725  ∀cost_map: identifier_map CostTag nat.
    704726  ∀codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k).
  • src/ASM/Fetch.ma

    r2264 r2498  
    3939definition label_map ≝ identifier_map ASMTag ℕ.
    4040
     41definition costlabel_map ≝ BitVectorTrie costlabel 16. 
     42
    4143(* The function that creates the label-to-address map *)
    4244definition create_label_cost_map0: ∀program:list labelled_instruction.
    43   (Σlabels_costs:label_map × (BitVectorTrie costlabel 16). (* Both on ppcs *)
     45  (Σlabels_costs:label_map × costlabel_map. (* Both on ppcs *)
    4446    let labels ≝ \fst labels_costs in
    4547    (∀l.occurs_exactly_once ?? l program →
     
    5052  λprogram.
    5153  \fst (pi1 ?? (foldl_strong (option Identifier × pseudo_instruction)
    52   (λprefix.Σlabels_costs_ppc:label_map × (BitVectorTrie costlabel 16) × ℕ.
     54  (λprefix.Σlabels_costs_ppc:label_map × costlabel_map × ℕ.
    5355    let 〈labels,costs,ppc〉 ≝ labels_costs_ppc in
    5456    ppc = |prefix| ∧
     
    107109(* The function that creates the label-to-address map *)
    108110definition create_label_cost_map: ∀program:list labelled_instruction.
    109   label_map × (BitVectorTrie costlabel 16)
     111  label_map × costlabel_map
    110112    λprogram.
    111113      pi1 … (create_label_cost_map0 program).
     
    167169(***** Object-code *******)
    168170
     171definition object_code ≝ list Byte.
     172
    169173definition bitvector_max_nat ≝
    170174  λlength: nat.
     
    182186
    183187definition load_code_memory0:
    184  ∀program: list Byte. Σres: BitVectorTrie Byte 16.
     188 ∀program: object_code. Σres: BitVectorTrie Byte 16.
    185189  let program_size ≝ |program| in
    186190   program_size ≤ 2^16 →
     
    220224qed.
    221225
    222 definition load_code_memory: list Byte → BitVectorTrie Byte 16 ≝
     226definition load_code_memory: object_code → BitVectorTrie Byte 16 ≝
    223227 λprogram.load_code_memory0 program.
    224228
    225229lemma load_code_memory_ok:
    226  ∀program: list Byte.
     230 ∀program: object_code.
    227231  let program_size ≝ |program| in
    228232   program_size ≤ 2^16 →
  • src/ASM/Interpret2.ma

    r1996 r2498  
    3838
    3939(*CSC: move this definition elsewhere *)
    40 definition object_code: Type[0] ≝ list Byte × (BitVectorTrie costlabel 16).
     40definition object_code: Type[0] ≝ list Byte × costlabel_map.
    4141
    42 definition make_global: object_code → BitVectorTrie costlabel 16 ≝ \snd.
     42definition make_global: object_code → costlabel_map ≝ \snd.
    4343
    4444definition execute_1_instruction:
    45  BitVectorTrie costlabel 16 → Status → IO io_out io_in (trace × Status) ≝
     45 costlabel_map → Status → IO io_out io_in (trace × Status) ≝
    4646λcosts,s.
    4747 let 〈instr_pc,ticks〉 ≝ fetch (code_memory … s) (program_counter … s) in
     
    5151 | Some cst ⇒ ret … 〈Echarge cst, execute_1 s〉 ].
    5252
    53 axiom is_final: BitVectorTrie costlabel 16 → Status → option int.
     53axiom is_final: costlabel_map → Status → option int.
    5454
    5555definition exec: trans_system io_out io_in ≝
Note: See TracChangeset for help on using the changeset viewer.