Skip to content

Commit 1697109

Browse files
StevengreStevengre
committed
draft for kontrol.toml
1 parent 9d13c4a commit 1697109

File tree

1 file changed

+306
-0
lines changed

1 file changed

+306
-0
lines changed

‎glossary/kontrol-toml.md‎

Lines changed: 306 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,306 @@
1+
# Configuration Options for Kontrol TOML file
2+
3+
The following is a kontrol.toml file with all configuration options set.
4+
5+
```toml
6+
[build.default]
7+
foundry-project-root = '.'
8+
regen = false
9+
rekompile = false
10+
verbose = false
11+
debug = false
12+
require = 'lemmas.k'
13+
module-import = 'TestBase:KONTROL-LEMMAS'
14+
auxiliary-lemmas = true
15+
16+
# ? definition_dir = None
17+
# ? spec_module = None
18+
19+
[build]
20+
# Directories to lookup K definitions in.
21+
# include = []
22+
# Name of the main module.
23+
# main-module = None
24+
# Name of the syntax module.
25+
# syntax-module = None
26+
# Code selector expression to use when reading markdown.
27+
md-selector = 'k'
28+
# Maximum depth to execute to.
29+
# depth = None
30+
# Path to kompile definition to.
31+
# output-definition = # Cannot find the default value
32+
# K backend to target with compilation.
33+
# backend = # Cannot find the default value
34+
# Mode for doing K rule type inference in.
35+
# type-inference-mode =
36+
# Mode for doing K rule type inference in.
37+
emit-json = true
38+
# Additional arguments to pass to llvm-kompile.
39+
ccopt = []
40+
# Do not run llvm-kompile process.
41+
no-llvm-kompile = false
42+
# Make kompile generate a dynamic llvm library.
43+
with-llvm-library = false
44+
# Make kompile generate debug symbols for llvm.
45+
enable-llvm-debug = false
46+
# Mode to kompile LLVM backend in.
47+
# llvm-kompile-type = None
48+
# Location to put kompiled LLVM backend at.
49+
# llvm-kompile-output = None
50+
# Generated a kompiled directory that K will not attempt to write to afterwards.
51+
read-only-kompiled-directory = false
52+
# Optimization level 0-3
53+
O0 = false
54+
O1 = false
55+
O2 = false
56+
O3 = false
57+
# Enable search mode on LLVM backend krun.
58+
enable-search = false
59+
# Enable logging semantic rule coverage measurement.
60+
coverage = false
61+
# Generate standalone Bison parser for program sort.
62+
gen-bison-parser = false
63+
# Generate standalone GLR Bison parser for program sort.
64+
gen-glr-bison-parser = false
65+
# Disable List{Sort} parsing to make grammar LR(1) for Bison parser.
66+
bison-lists = false
67+
# Enable proof hint generation in LLVM backend kompilation.
68+
llvm-proof-hint-instrumentation = false
69+
# Enable additional proof hint debugging information in LLVM backend kompilation.
70+
llvm-proof-hint-debugging = false
71+
# Do not wrap the output on the CLI.
72+
no-exc-wrap = false
73+
# Ignore provided warnings
74+
ignore-warnings = []
75+
# Add constraints for enum function arguments and storage slots.
76+
enum-constraints = false
77+
# Target to compile to.
78+
target = 'haskell'
79+
# Path to Pyk config file.
80+
# config-file =
81+
# Config profile to be used.
82+
config-profile = 'default'
83+
# Do not call 'forge build' during kompilation.
84+
no-forge-build = false
85+
# Do not silence K compiler warnings.
86+
no-silence-warnings = false
87+
# Do not append cbor or bytecode_hash metadata to bytecode.
88+
no-metadata = false
89+
# Do not include assumptions on keccak properties.
90+
no-keccak-lemmas = false
91+
92+
[prove.default]
93+
foundry-project-root = '.'
94+
verbose = false
95+
debug = false
96+
# Maximum number of K steps before the state is saved in a new node in the CFG.
97+
# Branching will cause this to happen earlier.
98+
max-depth = 25000
99+
# Reinitialize CFGs even if they already exist.
100+
reinit = false
101+
# Use Compositional Symbolic Execution
102+
cse = false
103+
# Number of processes to run in parallel.
104+
workers = 4
105+
# Show failure summary for all failing tests (default).
106+
failure-information = true
107+
# Show models for failing nodes (default).
108+
counterexample-information = true
109+
# Minimize obtained KCFGs
110+
minimize-proofs = false
111+
# Stop execution on other branches if a failing node is detected (default).
112+
fail-fast = true
113+
# Timeout in ms to use for SMT queries.
114+
smt-timeout = 1000
115+
# Store a node for every EVM opcode step (expensive).
116+
break-every-step = false
117+
# Store a node for every EVM jump opcode.
118+
break-on-jumpi = false
119+
# Store a node for every EVM call made.
120+
break-on-calls = false
121+
# Store a node for every EVM SSTORE/SLOAD made.
122+
break-on-storage = false
123+
# Store a node for every EVM basic block (implies --break-on-calls).
124+
break-on-basic-blocks = false
125+
# Break on all Foundry rules.
126+
break-on-cheatcodes = false
127+
# Include the contract constructor in the test execution.
128+
run-constructor = false
129+
# Optimize KEVM execution by removing stack overflow/underflow checks.Assumes
130+
# running Solidity-compiled bytecode cannot result in a stack overflow/underflow.
131+
no-stack-checks = true
132+
133+
[prove]
134+
-I INCLUDES Directories to lookup K definitions in.
135+
--main-module MAIN_MODULE
136+
Name of the main module.
137+
--syntax-module SYNTAX_MODULE
138+
Name of the syntax module.
139+
--md-selector MD_SELECTOR
140+
Code selector expression to use when reading markdown.
141+
# Maximum depth to execute to.
142+
depth = # DEPTH
143+
# Comma-separated list of equations to debug.
144+
debug-equations = [] # DEBUG_EQUATIONS
145+
# Use fast-check on k-cell to determine subsumption (experimental).
146+
fast-check-subsumption = false
147+
# For passing subproofs, construct lemmas directly from initial to target state.
148+
direct-subproof-rules = false
149+
# The number of proof iterations performed between two writes to disk and status bar updates. Note that setting to >1 may result in work being discarded if proof is interrupted.
150+
maintenance-rate = 1 # MAINTENANCE_RATE
151+
# Use the implication check of the Booster (experimental).
152+
assume-defined = false
153+
# Number of times to retry SMT queries with scaling timeouts.
154+
smt-retry-limit = 10 # SMT_RETRY_LIMIT
155+
# Z3 tactic to use when checking satisfiability. Example: (check-sat-using smt)
156+
smt-tactic = # SMT_TACTIC
157+
--no-log-rewrites Do not log traces of any simplification and rewrite rule application.
158+
# log_succ_rewrites = true
159+
# Log traces of all simplification and rewrite rule applications.
160+
log-fail-rewrites = false
161+
# Custom command to start RPC server.
162+
kore-rpc-command = # KORE_RPC_COMMAND
163+
# Use the booster RPC server instead of kore-rpc (default).
164+
use-booster = true
165+
--no-use-booster Do not use the booster RPC server instead of kore-rpc.
166+
# Use existing RPC server on named port.
167+
port = # PORT
168+
# Use existing Maude RPC server on named port.
169+
maude-port = # MAUDE_PORT
170+
# Generate bug report with given name
171+
bug-report = # BUG_REPORT
172+
--symbolic-immutables
173+
Enable support for symbolic immutable variables in Solidity code.
174+
# Number of times to expand the next pending node in the CFG.
175+
# max-iterations = # MAX_ITERATIONS
176+
# Automatically extract gas cell when infinite gas is enabled.
177+
auto-abstract-gas = false
178+
# Use sequential, single-threaded proof loop.
179+
force-sequential = false
180+
# Add constraints for enum function arguments and storage slots.
181+
enum-constraints = false
182+
# schedule to use for execution [DEFAULT|FRONTIER|HOMESTEAD|TANGERINE_WHISTLE|SPURIOUS_DRAGON|BYZANTIUM|CONSTANTINOPLE|PETERSBURG|ISTANBUL|BERLIN|LONDON|MERGE|SHANGHAI|CANCUN].
183+
schedule = 'SHANGHAI' # {DEFAULT,FRONTIER,HOMESTEAD,TANGERINE_WHISTLE,SPURIOUS_DRAGON,BYZANTIUM,CONSTANTINOPLE,PETERSBURG,ISTANBUL,BERLIN,LONDON,MERGE,SHANGHAI,CANCUN}
184+
# chain ID to use for execution.
185+
chainid = 1 # CHAINID
186+
# execution mode to use [{'|'.join(modes)}].
187+
mode = 'NORMAL' # {NORMAL,VMTESTS}
188+
--no-gas omit gas cost computations.
189+
# Path to Pyk config file.
190+
# config-file = # CONFIG_FILE
191+
# Config profile to be used.
192+
config-profile = 'default' # CONFIG_PROFILE
193+
# Specify contract function(s) to test using a regular expression. This will match functions based on their full signature, e.g., 'ERC20Test.testTransfer(address,uint256)'. This option can be used multiple times to add more functions to test.
194+
# match-test = []
195+
# Instead of reinitializing the test setup together with the test proof, select the setup version to be reused during the proof.
196+
setup-version = # SETUP_VERSION
197+
# Maximum worker threads to use on a single proof to explore separate branches in parallel.
198+
max-frontier-parallel = 1 # MAX_FRONTIER_PARALLEL
199+
# Enables bounded model checking. Specifies the maximum depth to unroll all loops to.
200+
bmc-depth = # BMC_DEPTH
201+
# Enables gas computation in KEVM.
202+
use-gas = false
203+
# Config type
204+
config-type = 'TEST_CONFIG' # {ConfigType.TEST_CONFIG,ConfigType.SUMMARY_CONFIG}
205+
# Disables the proof status bar.
206+
hide-status-bar = false
207+
# Path to JSON file produced by vm.stopAndReturnStateDiff.
208+
init-node-from-diff = # RECORDED_DIFF_STATE_PATH
209+
# Path to JSON file produced by vm.dumpState.
210+
init-node-from-dump = # RECORDED_DUMP_STATE_PATH
211+
# Specify a summary to include as a lemma.
212+
include-summary = [] # INCLUDE_SUMMARIES
213+
# Flag used by Simbolik to initialise the state of a non test function as if it was a test function.
214+
with-non-general-state = false
215+
# Generate a JUnit XML report
216+
xml-test-report = false
217+
# Use hevm success predicate instead of foundry to determine if a test is passing
218+
hevm = false
219+
# Trace opcode execution and store it in the configuration
220+
evm-tracing = false
221+
# If tracing is active, avoid storing storage information.
222+
no-trace-storage = true
223+
# If tracing is active, avoid storing wordstack information.
224+
no-trace-wordstack = true
225+
# If tracing is active, avoid storing memory information.
226+
no-trace-memory = true
227+
# Remove all outdated KCFGs.
228+
remove-old-proofs = false
229+
# Optimize performance for proof execution. Takes the number of parallel threads to be used.Will overwrite other settings of 'assume-defined', 'log-success-rewrites', 'max-frontier-parallel','maintenance-rate', 'smt-timeout', 'smt-retry-limit', 'max-depth', 'max-iterations', and 'no-stack-checks'.
230+
optimize-performance = # OPTIMIZE_PERFORMANCE
231+
232+
233+
[show.default]
234+
foundry-project-root = '.'
235+
verbose = false
236+
debug = false
237+
use-hex-encoding = false
238+
239+
[show]
240+
# ??? 'version': None --- FoundryTestOptions
241+
# Name of the main module.
242+
# main-module = # MAIN_MODULE
243+
# Name of the syntax module.
244+
# syntax-module = # SYNTAX_MODULE
245+
# Code selector expression to use when reading markdown.
246+
md-selector = 'k' # MD_SELECTOR
247+
# Maximum depth to execute to.
248+
depth = # DEPTH
249+
# List of nodes to display as well.
250+
node = [] # NODES
251+
# List of nodes to display delta for.
252+
node-delta = [] # NODE_DELTAS
253+
# Show failure summary for cfg.
254+
failure-information = false
255+
# Do not show failure summary for cfg.
256+
no-failure-information = false
257+
# Output edges as a K module.
258+
to-module = false
259+
--pending Also display pending nodes.
260+
--failing Also display failing nodes.
261+
# Show models for failing nodes. Should be called with the '--failure-information' flag.
262+
counterexample-information = true
263+
# Minimize output.
264+
minimize = true
265+
# Do not minimize output.
266+
no-minimize = false
267+
# Sort collections before outputting term.
268+
sort-collections = false
269+
# Add constraints for enum function arguments and storage slots.
270+
enum-constraints = false
271+
# Path to Pyk config file.
272+
config-file = # CONFIG_FILE
273+
# Config profile to be used.
274+
config-profile = 'default' # CONFIG_PROFILE
275+
# Strip output that is likely to change without the contract logic changing
276+
omit-unstable-output = false
277+
# Generate a K module which can be run directly as KEVM claims for the given KCFG(best-effort).
278+
to-kevm-claims = false
279+
# Generate a K module which can be used to optimize KEVM execution (best-effort).
280+
to-kevm-rules = false
281+
# Path to write KEVM claim files at.
282+
kevm-claim-dir = # KEVM_CLAIM_DIR
283+
# When printing nodes, always show full bytecode in code and program cells, and do not hide jumpDests cell.
284+
expand-config = false
285+
# Run KCFG minimization routine before displaying it.
286+
minimize-kcfg = false
287+
288+
289+
[view-kcfg.default]
290+
foundry-project-root = '.'
291+
use-hex-encoding = false
292+
293+
[view-kcfg]
294+
# Version of the test to use
295+
version = # VERSION
296+
# Verbose output.
297+
verbose = false
298+
# Debug output.
299+
debug = false
300+
# Add constraints for enum function arguments and storage slots.
301+
enum-constraints = false
302+
# Path to Pyk config file.
303+
config-file = # CONFIG_FILE
304+
# Config profile to be used.
305+
config-profile = 'default' # CONFIG_PROFILE
306+
```

0 commit comments

Comments
 (0)