Changeset 1938 for src/ASM


Ignore:
Timestamp:
May 14, 2012, 10:05:36 AM (8 years ago)
Author:
sacerdot
Message:

Definitions moved to the right places, now everything compiles again.

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r1935 r1938  
    44include "ASM/Interpret.ma".
    55include "common/StructuredTraces.ma".
     6
     7definition ASM_abstract_status: ∀code_memory. BitVectorTrie costlabel 16 → abstract_status ≝
     8  λcode_memory.
     9  λcost_labels.
     10    mk_abstract_status
     11      (Status code_memory)
     12      (λs,s'. (execute_1 … s) = s')
     13      word_deqset
     14      (program_counter …)
     15      (λs,class. ASM_classify … s = class)
     16      (current_instruction_label code_memory cost_labels)
     17      (next_instruction_properly_relates_program_counters code_memory)
     18      ?.
     19  cases daemon (* XXX: is final predicate *)
     20qed.
    621
    722definition trace_any_label_length ≝
  • src/ASM/Interpret.ma

    r1935 r1938  
    22include "ASM/StatusProofs.ma".
    33include "ASM/Fetch.ma".
     4include "common/StructuredTraces.ma".
    45
    56definition sign_extension: Byte → Word ≝
     
    119120include alias "arithmetics/nat.ma".
    120121include alias "ASM/BitVectorTrie.ma".
    121 
    122 inductive status_class : Type[0] ≝
    123 | cl_return : status_class
    124 | cl_jump   : status_class
    125 | cl_call   : status_class
    126 | cl_other : status_class.
    127122
    128123definition ASM_classify00: ∀a. preinstruction a → status_class ≝
Note: See TracChangeset for help on using the changeset viewer.