Changeset 2516


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!

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

    r2508 r2516  
    55
    66let rec traverse_code_internal
    7   (code_memory: BitVectorTrie Byte 16) (cost_labels: costlabel_map)
     7  (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
    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: costlabel_map.
     281  ∀cost_labels: BitVectorTrie costlabel 16.
    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: costlabel_map.
     291  λcost_labels: BitVectorTrie costlabel 16.
    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: costlabel_map.
     320  λcost_labels: BitVectorTrie costlabel 16.
    321321  λcost_labels_injective:
    322322    ∀pc, pc',l.
     
    327327      traverse_code code_memory cost_labels cost_labels_injective.
    328328
    329 (* JHM: moved to Fetch.ma *)
    330 (* definition object_code ≝ list Byte. *)
    331 (* definition costlabel_map ≝ BitVectorTrie costlabel 16.   *)
    332 
    333329(* use of this defn in ASM/CostsProof.ma is ill-typed *)
    334330definition ASM_cost_map :
    335   ∀p: object_code × costlabel_map.
     331  ∀p: (list Byte) × (BitVectorTrie costlabel 16).
    336332  let code_memory ≝ load_code_memory (\fst p) in
    337333  let a_s ≝ ASM_abstract_status code_memory (\snd p) in
  • src/ASM/AbstractStatus.ma

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

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

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

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

    r2498 r2516  
    1010let rec compute_max_trace_label_label_cost
    1111  (cm: ?)
    12   (cost_labels: costlabel_map)
     12  (cost_labels: BitVectorTrie costlabel 16)
    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: costlabel_map)
     23  (cost_labels: BitVectorTrie costlabel 16)
    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: costlabel_map)
     51  (cost_labels: BitVectorTrie costlabel 16)
    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: costlabel_map)
     67  (cost_labels: BitVectorTrie costlabel 16)
    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: costlabel_map)
     75  (cost_labels: BitVectorTrie costlabel 16)
    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: costlabel_map)
     83  (cost_labels: BitVectorTrie costlabel 16)
    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: costlabel_map)
     166  (cost_labels: BitVectorTrie costlabel 16)
    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: costlabel_map)
     178  (cost_labels: BitVectorTrie costlabel 16)
    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: costlabel_map)
     199  (cost_labels: BitVectorTrie costlabel 16)
    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: costlabel_map)
     213  (cost_labels: BitVectorTrie costlabel 16)
    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: costlabel_map)
     222  (cost_labels: BitVectorTrie costlabel 16)
    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: costlabel_map)
     232  (cost_labels: BitVectorTrie costlabel 16)
    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: costlabel_map)
     273  (cost_labels: BitVectorTrie costlabel 16)
    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: costlabel_map)
     290  (cost_labels: BitVectorTrie costlabel 16)
    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: costlabel_map)
     311  (cost_labels: BitVectorTrie costlabel 16)
    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: costlabel_map.
     388 ∀cost_labels: BitVectorTrie costlabel 16.
    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: costlabel_map.
     449 ∀cost_labels: BitVectorTrie costlabel 16.
    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: costlabel_map)
     503 (cm: ?) (cost_labels: BitVectorTrie costlabel 16)
    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: costlabel_map)
     517 (cm: ?) (cost_labels: BitVectorTrie costlabel 16)
    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: costlabel_map)
     532 (cm: ?) (cost_labels: BitVectorTrie costlabel 16)
    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: costlabel_map.
     651  ∀cost_labels: BitVectorTrie costlabel 16.
    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: costlabel_map.
     671  ∀cost_labels: BitVectorTrie costlabel 16.
    672672  ∀cost_labels_injective:
    673673   (∀pc,pc',l.
     
    697697 
    698698include "utilities/permutations.ma".
    699 (*
    700 lemma 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 ]
    720 qed.
    721 *)
     699
    722700lemma tech_cost_sum_eq_as_cost :
    723701  ∀code_memory: BitVectorTrie Byte 16.
    724   ∀cost_labels: costlabel_map.
     702  ∀cost_labels: BitVectorTrie costlabel 16.
    725703  ∀cost_map: identifier_map CostTag nat.
    726704  ∀codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k).
  • src/ASM/Fetch.ma

    r2498 r2516  
    3939definition label_map ≝ identifier_map ASMTag ℕ.
    4040
    41 definition costlabel_map ≝ BitVectorTrie costlabel 16. 
    42 
    4341(* The function that creates the label-to-address map *)
    4442definition create_label_cost_map0: ∀program:list labelled_instruction.
    45   (Σlabels_costs:label_map × costlabel_map. (* Both on ppcs *)
     43  (Σlabels_costs:label_map × (BitVectorTrie costlabel 16). (* Both on ppcs *)
    4644    let labels ≝ \fst labels_costs in
    4745    (∀l.occurs_exactly_once ?? l program →
     
    5250  λprogram.
    5351  \fst (pi1 ?? (foldl_strong (option Identifier × pseudo_instruction)
    54   (λprefix.Σlabels_costs_ppc:label_map × costlabel_map × ℕ.
     52  (λprefix.Σlabels_costs_ppc:label_map × (BitVectorTrie costlabel 16) × ℕ.
    5553    let 〈labels,costs,ppc〉 ≝ labels_costs_ppc in
    5654    ppc = |prefix| ∧
     
    109107(* The function that creates the label-to-address map *)
    110108definition create_label_cost_map: ∀program:list labelled_instruction.
    111   label_map × costlabel_map
     109  label_map × (BitVectorTrie costlabel 16)
    112110    λprogram.
    113111      pi1 … (create_label_cost_map0 program).
     
    169167(***** Object-code *******)
    170168
    171 definition object_code ≝ list Byte.
    172 
    173169definition bitvector_max_nat ≝
    174170  λlength: nat.
     
    186182
    187183definition load_code_memory0:
    188  ∀program: object_code. Σres: BitVectorTrie Byte 16.
     184 ∀program: list Byte. Σres: BitVectorTrie Byte 16.
    189185  let program_size ≝ |program| in
    190186   program_size ≤ 2^16 →
     
    224220qed.
    225221
    226 definition load_code_memory: object_code → BitVectorTrie Byte 16 ≝
     222definition load_code_memory: list Byte → BitVectorTrie Byte 16 ≝
    227223 λprogram.load_code_memory0 program.
    228224
    229225lemma load_code_memory_ok:
    230  ∀program: object_code.
     226 ∀program: list Byte.
    231227  let program_size ≝ |program| in
    232228   program_size ≤ 2^16 →
  • src/ASM/Interpret2.ma

    r2498 r2516  
    3838
    3939(*CSC: move this definition elsewhere *)
    40 definition object_code: Type[0] ≝ list Byte × costlabel_map.
     40definition object_code: Type[0] ≝ list Byte × (BitVectorTrie costlabel 16).
    4141
    42 definition make_global: object_code → costlabel_map ≝ \snd.
     42definition make_global: object_code → BitVectorTrie costlabel 16 ≝ \snd.
    4343
    4444definition execute_1_instruction:
    45  costlabel_map → Status → IO io_out io_in (trace × Status) ≝
     45 BitVectorTrie costlabel 16 → 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: costlabel_map → Status → option int.
     53axiom is_final: BitVectorTrie costlabel 16 → Status → option int.
    5454
    5555definition exec: trans_system io_out io_in ≝
Note: See TracChangeset for help on using the changeset viewer.