extracted/aSMCosts.mli

   1 open Preamble
   2
   3 open Fetch
   4
   5 open Hide
   6
   7 open Division
   8
   9 open Z
  10
  11 open BitVectorZ
  12
  13 open Pointers
  14
  15 open Coqlib
  16
  17 open Values
  18
  19 open Events
  20
  21 open IOMonad
  22
  23 open IO
  24
  25 open Sets
  26
  27 open Listb
  28
  29 open StructuredTraces
  30
  31 open AbstractStatus
  32
  33 open BitVectorTrie
  34
  35 open String
  36
  37 open Exp
  38
  39 open Arithmetic
  40
  41 open Vector
  42
  43 open FoldStuff
  44
  45 open BitVector
  46
  47 open Extranat
  48
  49 open Integers
  50
  51 open AST
  52
  53 open LabelledObjects
  54
  55 open Proper
  56
  57 open PositiveMap
  58
  59 open Deqsets
  60
  61 open ErrorMessages
  62
  63 open PreIdentifiers
  64
  65 open Errors
  66
  67 open Extralib
  68
  69 open Setoids
  70
  71 open Monad
  72
  73 open Option
  74
  75 open Div_and_mod
  76
  77 open Util
  78
  79 open List
  80
  81 open Lists
  82
  83 open Bool
  84
  85 open Relations
  86
  87 open Nat
  88
  89 open Positive
  90
  91 open Identifiers
  92
  93 open CostLabel
  94
  95 open ASM
  96
  97 open Types
  98
  99 open Hints_declaration
 100
 101 open Core_notation
 102
 103 open Pts
 104
 105 open Logic
 106
 107 open Jmeq
 108
 109 open Russell
 110
 111 open Status
 112
 113 open StatusProofs
 114
 115 open Interpret
 116
 117 val aSMRegisterRets : ASM.subaddressing_mode List.list
 118
 119 val as_result_of_finaladdr :
 120   'a1 -> 'a1 Status.preStatus -> BitVector.word -> Integers.int Types.option
 121
 122 val oC_as_call_ident :
 123   ASM.labelled_object_code -> BitVector.byte BitVectorTrie.bitVectorTrie ->
 124   Status.status Types.sig0 -> AST.ident
 125
 126 val oC_abstract_status :
 127   ASM.labelled_object_code -> StructuredTraces.abstract_status
 128
 129 val trace_any_label_length :
 130   ASM.labelled_object_code -> StructuredTraces.trace_ends_with_ret ->
 131   Status.status -> Status.status -> StructuredTraces.trace_any_label ->
 132   Nat.nat
 133
 134 val all_program_counter_list : Nat.nat -> BitVector.bitVector List.list
 135
 136 val compute_paid_trace_any_label :
 137   ASM.labelled_object_code -> StructuredTraces.trace_ends_with_ret ->
 138   Status.status -> Status.status -> StructuredTraces.trace_any_label ->
 139   Nat.nat
 140
 141 val compute_paid_trace_label_label :
 142   ASM.labelled_object_code -> StructuredTraces.trace_ends_with_ret ->
 143   Status.status -> Status.status -> StructuredTraces.trace_label_label ->
 144   Nat.nat
 145
 146 val block_cost' :
 147   ASM.labelled_object_code -> BitVector.word -> Nat.nat -> Bool.bool ->
 148   Nat.nat Types.sig0
 149
 150 val block_cost :
 151   ASM.labelled_object_code -> BitVector.word -> Nat.nat Types.sig0
 152