Changeset 1935 for src/ASM/ASMCosts.ma


Ignore:
Timestamp:
May 10, 2012, 5:13:34 PM (8 years ago)
Author:
mulligan
Message:

Generalized some lemma in ASM/CostsProof.ma to work on abstract statuses, moving the abstract version in to common/StructuredTraces.ma. Ported rest of proof in ASM/CostsProof.ma to use new, generalized lemma.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r1929 r1935  
    44include "ASM/Interpret.ma".
    55include "common/StructuredTraces.ma".
    6    
    7 definition well_labelling: BitVectorTrie costlabel 16 → Prop ≝
    8   λcost_labels.
    9     injective … (λx. lookup_opt … x cost_labels).
    10 
    11 definition current_instruction_label ≝
    12   λcode_memory.
    13   λcost_labels: BitVectorTrie costlabel 16.
    14   λs: Status code_memory.
    15   let pc ≝ program_counter … code_memory s in
    16     lookup_opt … pc cost_labels.
    17 
    18 definition next_instruction_properly_relates_program_counters ≝
    19   λcode_memory.
    20   λbefore: Status code_memory.
    21   λafter : Status code_memory.
    22     let program_counter_before ≝ program_counter ? code_memory before in
    23     let 〈instruction, program_counter_after, ticks〉 ≝ fetch code_memory program_counter_before in
    24       program_counter ? code_memory after = program_counter_after.
    25 
    26 definition word_deqset: DeqSet ≝
    27   mk_DeqSet Word (eq_bv 16) ?.
    28   @refl_iff_eq_bv_true
    29 qed.
    30 
    31 definition ASM_abstract_status: ∀code_memory. BitVectorTrie costlabel 16 → abstract_status ≝
    32   λcode_memory.
    33   λcost_labels.
    34     mk_abstract_status
    35       (Status code_memory)
    36       (λs,s'. (execute_1 … s) = s')
    37       word_deqset
    38       (program_counter …)
    39       (λs,class. ASM_classify … s = class)
    40       (current_instruction_label code_memory cost_labels)
    41       (next_instruction_properly_relates_program_counters code_memory)
    42       ?.
    43   cases daemon (* XXX: is final predicate *)
    44 qed.
    456
    467definition trace_any_label_length ≝
Note: See TracChangeset for help on using the changeset viewer.