Changeset 1935 for src/ASM/Interpret.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/Interpret.ma

    r1928 r1935  
     1include "basics/lists/listb.ma".
    12include "ASM/StatusProofs.ma".
    2 include "common/StructuredTraces.ma".
    33include "ASM/Fetch.ma".
    44
     
    120120include alias "ASM/BitVectorTrie.ma".
    121121
     122inductive status_class : Type[0] ≝
     123| cl_return : status_class
     124| cl_jump   : status_class
     125| cl_call   : status_class
     126| cl_other : status_class.
     127
    122128definition ASM_classify00: ∀a. preinstruction a → status_class ≝
    123129  λa, pre.
     
    159165  λs: Status code_memory.
    160166    current_instruction0 code_memory (program_counter … s).
     167   
     168definition current_instruction_label ≝
     169  λcode_memory.
     170  λcost_labels: BitVectorTrie costlabel 16.
     171  λs: Status code_memory.
     172  let pc ≝ program_counter … code_memory s in
     173    lookup_opt … pc cost_labels.
     174
     175definition next_instruction_properly_relates_program_counters ≝
     176  λcode_memory.
     177  λbefore: Status code_memory.
     178  λafter : Status code_memory.
     179    let program_counter_before ≝ program_counter ? code_memory before in
     180    let 〈instruction, program_counter_after, ticks〉 ≝ fetch code_memory program_counter_before in
     181      program_counter ? code_memory after = program_counter_after.
     182
     183definition word_deqset: DeqSet ≝
     184  mk_DeqSet Word (eq_bv 16) ?.
     185  @refl_iff_eq_bv_true
     186qed.
    161187   
    162188definition ASM_classify: ∀code_memory. Status code_memory → status_class ≝
Note: See TracChangeset for help on using the changeset viewer.