source: extracted/aSMCosts.mli @ 2649

Last change on this file since 2649 was 2649, checked in by sacerdot, 7 years ago

...

File size: 2.0 KB
Line 
1open Preamble
2
3open String
4
5open LabelledObjects
6
7open Arithmetic
8
9open Integers
10
11open AST
12
13open CostLabel
14
15open Proper
16
17open PositiveMap
18
19open Deqsets
20
21open ErrorMessages
22
23open PreIdentifiers
24
25open Errors
26
27open Extralib
28
29open Setoids
30
31open Monad
32
33open Option
34
35open Lists
36
37open Positive
38
39open Identifiers
40
41open Extranat
42
43open Vector
44
45open Div_and_mod
46
47open Jmeq
48
49open Russell
50
51open Types
52
53open List
54
55open Util
56
57open FoldStuff
58
59open Bool
60
61open Hints_declaration
62
63open Core_notation
64
65open Pts
66
67open Logic
68
69open Relations
70
71open Nat
72
73open BitVector
74
75open ASM
76
77open BitVectorTrie
78
79open Fetch
80
81open StructuredTraces
82
83open AbstractStatus
84
85open Status
86
87open StatusProofs
88
89open Sets
90
91open Listb
92
93open Interpret
94
95val aSM_abstract_status :
96  BitVector.byte BitVectorTrie.bitVectorTrie -> CostLabel.costlabel
97  BitVectorTrie.bitVectorTrie -> StructuredTraces.abstract_status
98
99val trace_any_label_length :
100  BitVector.byte BitVectorTrie.bitVectorTrie -> CostLabel.costlabel
101  BitVectorTrie.bitVectorTrie -> StructuredTraces.trace_ends_with_ret ->
102  Status.status -> Status.status -> StructuredTraces.trace_any_label ->
103  Nat.nat
104
105val all_program_counter_list : Nat.nat -> BitVector.bitVector List.list
106
107val compute_paid_trace_any_label :
108  BitVector.byte BitVectorTrie.bitVectorTrie -> CostLabel.costlabel
109  BitVectorTrie.bitVectorTrie -> StructuredTraces.trace_ends_with_ret ->
110  Status.status -> Status.status -> StructuredTraces.trace_any_label ->
111  Nat.nat
112
113val compute_paid_trace_label_label :
114  BitVector.byte BitVectorTrie.bitVectorTrie -> CostLabel.costlabel
115  BitVectorTrie.bitVectorTrie -> StructuredTraces.trace_ends_with_ret ->
116  Status.status -> Status.status -> StructuredTraces.trace_label_label ->
117  Nat.nat
118
119val block_cost' :
120  BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word -> Nat.nat ->
121  CostLabel.costlabel BitVectorTrie.bitVectorTrie -> Bool.bool -> Nat.nat
122  Types.sig0
123
124val block_cost :
125  BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word ->
126  CostLabel.costlabel BitVectorTrie.bitVectorTrie -> Nat.nat Types.sig0
127
Note: See TracBrowser for help on using the repository browser.