Changeset 1938


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
Files:
3 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 ≝
  • src/common/StructuredTraces.ma

    r1935 r1938  
    44include "common/CostLabel.ma".
    55include "utilities/option.ma".
     6include "basics/lists/listb.ma".
    67include "ASM/Util.ma".
    7 include "ASM/Interpret.ma".
     8
     9inductive status_class : Type[0] ≝
     10| cl_return : status_class
     11| cl_jump   : status_class
     12| cl_call   : status_class
     13| cl_other : status_class.
    814
    915record abstract_status : Type[1] ≝
     
    1824  ; as_final: as_status → Prop
    1925}.
    20 
    21 definition ASM_abstract_status: ∀code_memory. BitVectorTrie costlabel 16 → abstract_status ≝
    22   λcode_memory.
    23   λcost_labels.
    24     mk_abstract_status
    25       (Status code_memory)
    26       (λs,s'. (execute_1 … s) = s')
    27       word_deqset
    28       (program_counter …)
    29       (λs,class. ASM_classify … s = class)
    30       (current_instruction_label code_memory cost_labels)
    31       (next_instruction_properly_relates_program_counters code_memory)
    32       ?.
    33   cases daemon (* XXX: is final predicate *)
    34 qed.
    3526
    3627(* temporary alias for backward compatibility *)
     
    442433  ].
    443434
    444 include "ASM/BitVectorTrie.ma".
    445 include "ASM/Status.ma".
    446 include "ASM/Fetch.ma".
    447 
    448435let rec as_compute_cost_trace_label_label
    449436  (S: abstract_status) (trace_ends_flag: trace_ends_with_ret)
Note: See TracChangeset for help on using the changeset viewer.