Skip to content

Latest commit

 

History

History
173 lines (116 loc) · 13.7 KB

kprove-tutorial.md

File metadata and controls

173 lines (116 loc) · 13.7 KB
Raw

Disclaimer

This tutorial is not meant to be complete or even correct. It is a work in progress technical reference.

Installation

  • Checkout repositories k, evm-semantics and verified-smart-contracts, all with branch gnosis (at the moment of writing). DO NOT follow build instructions in evm-semantics projects as they are known to be incomplete.

Right now these 3 projects depend on each other in git level, like evm-smart-contracts has a git submodule for evm-semantics wich have a git submodule for k, but it's better not to use these dependencies but have them checked out separately. This way there are less chances you'll have issues when one of them gets updated on git.

  • Add $K_HOME to $PATH as specified in K installation manual.

Let's consider you have 3 path variables for home dir of the 3 projects: $K_HOME, $KEVM, $VSC.

  • To build a new version of K, whenever you need it:
  $ cd $K_HOME
  $ mvn package -DskipTests
  • To kompile kevm:
  $ cd $KEVM
  $ make tangle-deps  #only needed first time
  $ make defn
  $ kompile --debug --backend java -I .build/java -d .build/java --main-module ETHEREUM-SIMULATION --syntax-module ETHEREUM-SIMULATION .build/java/driver.k
  • To run a spec:
  $ cd $VSC
  $ make all
    # or `make <specific project>`, like `make hobby-erc20`. Look into Makefile for available commands.
  $ kprove <spec file> -d $KEVM/.build/java -m VERIFICATION &> <out_file>
    # where <spec file> is some file named `*-spec.k` inside $VSC/specs, generated by make above

This will write all the generated output, both stdout and stderr to <out_file>, so that you can easily open and analyze it in a text editor. Now there is a number of extra options for kprove that output debug-related information, to help you debug a specification when it does not get proved. A more basic option is --log-stmts-only, It outputs a subset of cells from the configuration at each step when an EVM statement is executed. Note that not all K steps represent a new EVM statement. A more advanced option is --debug-z3. It outputs a lot more information, in particular all the conjunctive formulas that kprove tries to prove at various steps, including those that involve z3. There are a number of other useful options. Run kprove --help and look at all options starting with --log or --debug.

Logs generated by kprove can be very big, in the sometimes in the GBs range. You might want to use a file editor tha supports large files.

Rule types

There are 3 types of rules available to kprove:

  • Regular rules (or semantics rules)
  • Spec rules.
  • Function rules

Regular rules are regular K rules of the language semantics over which specification is defined. KEVM rules in our case. They can match configuration cells.

Spec rules are similar to regular rules but they are defined in modules imported by the specification, not in the semantics. The specification to be proved is a spec rule, and rules defined in abstract-semantics.k in this project. They have slightly different execution "rules" than regular rules (see below). The spec rules that don't have to be proved are annotated with [trusted]

Function rules are rules matching function terms (e.g. terms with [function]). These rules cannot match configuration cells and are evaluated in place, without access to their surrounding context. There's no difference between function rules defined in the semantics vs those defined in the spec. We often define helper function rules in the spec that help evaluating certain symbolic expressions. We also call them lemmas. Usually we place lemmas in lemmas.md and verification.k.

Overview of kprove

Kprove generally proceeds with the following algorithm:

The rule to be proved is processed into an initial term and a target term. The goal of kprove is to evaluate symbolically initial term until it matches the target term. Both these terms are "constrained terms" - they have a "proper term" that represents the whole configuration, and a constraint (or path condition) - a boolean formula that is represented by class ConjunctiveFormula in the code.

Initial term is the LHS of the rule, with constraint being the requires clause. Target term is the RHS with constraint = the ensures clause (if it is present). Both terms are fully evaluated in the context of the requires clause at the beginning of execution (see later what this means).

Then kprove continues by evaluating the initial term. At each evaluation step the following happens:

  • First it checks if current term matches the target term. If true, execution of current path finishes.
  • It tries to apply a spec rule.
  • If no spec rule matches, it tries to apply a regular rule.
  • After applying a rule, function rules are applied as much as possible until no further rewrite is possible. Thus, during one step, one spec or regular rule is applied, plus any number of function rules.

Spec and regular rules are matched in different ways. A spec rule, in order to match, should "fully match", e.g. match all possible values of symbolic terms. Thus if you nave an unconstrained symbolic term A, and 2 spec rules:

rule A => B requires A >Int 0 [trusted]
rule A => C requires A <=Int 0 [trusted]

none of them will match, because none match all possible values of A.

A regular rule is allowed to match only a subset of instantiations of symbolic terms. Thus it is possible for several regular rules to match the current term. In this case a "branching" will occur. Several successor terms will be generated, one for each regular rule that matches. The path condition of successor terms will have additional conditions that constrain the symbolic terms on this branch. Each successor term will be executed independently on its path and can have more branchings down the line.

Thus, in order for a spec to be proved, it should be proved on all branches.

If a function rule cannot match all possible symbolic values, then it won't apply, and symbolic term will be carried on to the next step until the end or until some additional path condition after a branching makes the evaluation possible. Thus only regular rules can cause branchings.

There's another difference between spec rules and regular rules. The side condition of rules (of all 3 kinds) is allowed to match the path condition only during a "spec rule" step, but not during a "regular rule" step.

Execution of a path ends when when it either:

  • Matches the implication
  • No other spec/regular rule can match.
  • <k> cell matches the <k> cell of the target term (but only for cases when initial term was not matching the target <k>). This is a customization in gnosis branch of K, to avoid further evaluation when it is clear that this path cannot be proved.

In the 2nd and 3rd case specification failed for this particular path.

When evaluation of all paths finishes, kprove will output either #True if proof succeeded, or the list of paths that failed. Paths on which proof succeeded won't be displayed.

The high-level algorithm of kprove is implemented in SymbolicRewriter.proveRule(): https://github.com/kframework/k/blob/809409e4086529229cdc02fc8dcf68fbeb985f3a/java-backend/src/main/java/org/kframework/backend/java/symbolic/SymbolicRewriter.java#L607 You might want to study this class at some point.

Evaluation of side conditions

The side condition of a proof can be evaluated in one of 3 ways:

  • The side condition is concrete (no symbolic terms), thus it can be evaluated by applying function rules from the semantics, using regular concrete execution mechanism.
  • The side condition contains symbolic expressions that can be matched by lemmas (helper function rules) from the specification.

Note that lemmas match syntactically, as regular K rules, and cannot perform any logical transformations.

Thus, if side condition is A andBool B, and the lemma is rule B andBool A => true, the lemma won't match. You can add an additional lemma that does rule B andBool A => B andBool A requires..., but carefully chose the requires clauses to avoid an infinite loop.

  • The side condition is a logical expression implied by the path condition. If it is not matched directly by a subset of path conditions, Z3 theorem prover will be used to prove the implication. As stated above, this 3rd option is available only during steps where a spec rule was applied.

kprove logging options

In K branch gnosis, there are a number of command-line options for debugging K proofs. Here are the most common ones:

--log-stmts-only. Prints a subset of configuration at each step that corresponds to an EVM statement (opcode). Not all steps represent new statements. Most of them are some auxiliary operations, like substracting gas or checking whether an error occurred. Only the most important cells are prited to keep the log of reasonable size. You can customize the set of printed cells, and the format, by using the option --log-cells.

--log-basic The most basic log messages. Prints config extract only for steps where branching or some other interesting event happens. Also prints all debug messages discussed in this tutorial.

--log As above, but all steps are printed.

--debug-z3. Includes --log-stmts-only and also prints all attempts to prove logical formulas as part of symbolic execution. These proof attempts happen in many cotexts: proving final implication, matching rule side condition and others. We don't have a definitive guide of where this happens. In most cases these formulas are proved by a fixed set of simplifications inside K. When these are not enough, the formula is translated into a z3 query and passed to z3. A good default option.

--debug-z3-queries As above, but in addition prints the generated Z3 queries.

To see all the options run kprove --help and loog at options that start with --log and --debug. The simple option --debug is not recommended.

--log-rules Log all applied rules.

Debugging tips

Non-map format error

The error <localMem> non-map format, aborting happens when a certain function that is part of writing to memory gets stuck due to some symbolic term inside. Then the content of <localMem> gets stuck in a state that is not a map. Look at the content of <localMem>, particularly unevaluated functions.

Z3 error

This means Z3 query was generated, but it was not correct and Z3 threw an error. Run again with --debug-z3-queries and see what caused the error. Often this happens when a SPEC variable is not constraint to expected bounds or is of incorrect K sort.

Z3 Warning

These are most often not an issue. These happen when a certain term cannot be encoded into Z3, the query is not built for that formula and formula is considered not proved. In most cases we don't want that formula to be proved in the first place.

Debugging branchings

Look at the number of execution paths, on line Execution paths: in the summary box at the end of the log.

If they are more than expected, that means some functional term could not be evaluated and caused additional branchings and infeasible paths later on. Search the word Branching and look at the content of <k> on the step before branching. You should see the term that got stuck there.

If there are less paths than expected, then maybe you are executing something else. Check again the content of callData:. If it does not match any Solidity/Vyper function in your code, execution will end with one path with status EVMC_SUCCESS.

Debugging final implication

There are 3 ways in which final implication could fail:

  1. Concrete terms are not matching in current term and target term. For example gas value, or status code. In this case search for warnings Final implication term not matching. You'll see several such messages for each failing final implication, because they are printed recursively on the whole path from the inner-most mismatching term to the entire configuration, to help you figure out the context.

  2. Z3 warning. Query not generated. Usually query should not have been generated in the first place, and concrete term matching should have happened. Look at RHS of conjunctive formula generated for this final implication. Something is mismatching there. Most likely some function is not fully evaluated.

  3. Z3 implication fails. Check the conjunctive formula generated for this implication, and the branchings. Maybe this is an infeasible path? Or you missed some requires clause, and your spec covers more execution paths than intended?

How to solve stuck functional formulas

This is a frequent problem with kprove. Evaluation generates a functional formula that you know can be reduced to something simpler, but kprove cannot evaluate it any further, due to limitations of branching mechanism or of Z3.

There are 2 general approaches to solve this:

  • Introduce a lemma that matches the formula. For reference look at other lemmas in lemmas.md and verification.k Make sure to carefully chose side conditions, to avoid making it too general and unsound. Also, make sure it cannot generate an infinite loop either alone or in combination with other lemmas. If you get StackOverFlowError, you'll know why.

  • Break the spec into 2 separate specifications that have an extra side condition. This side condition should help evaluate the stuck formula. Use EDSL inheritance mechanism to avoid duplication. Example:

verified-smart-contracts/gnosis/gnosis-spec.ini

Lines 280 to 349 in 6bcc9eb

; output = bytes32(32) bytes32(66) bytes1(0x19) bytes1(0x1) bytes32(DOMAIN_SEPARATOR) bytes32(SAFE_TX_HASH) bytes30(0)
; size = 160
output: _ => #encodeArgs( #bytes(
#parseHexWord("0x19") : #parseHexWord("0x1")
: #encodeArgs(#bytes32(DOMAIN_SEPARATOR), #bytes32(SAFE_TX_HASH))
))
statusCode: _ => EVMC_SUCCESS
code: {MASTER_COPY_CODE}
this: PROXY_ID
msg_sender: MSG_SENDER
callData: #abiCallData("encodeTransactionData", (
#address(TO),
#uint256(VALUE),
#toBytes(DATA, DATA_LEN),
; Enum.Operation operation, represented as uint8
#uint8(OPERATION),
#uint256(SAFE_TX_GAS),
#uint256(DATA_GAS),
#uint256(GAS_PRICE),
#address(GAS_TOKEN),
#address(REFUND_RECEIVER),
#uint256(NONCE) ))
callValue: 0
proxy_storage:
(#hashedLocation({COMPILER}, {MASTER_COPY}, .IntList) |-> MASTER_COPY_ID)
(#hashedLocation({COMPILER}, {DOMAIN_SEPARATOR}, .IntList) |-> DOMAIN_SEPARATOR)
_:Map
+requires:
// Range
andBool #rangeAddress(PROXY_ID)
andBool #rangeAddress(MSG_SENDER)
andBool #rangeAddress( TO)
andBool #rangeUInt( 256, VALUE)
andBool #rangeUInt( 256, DATA_LEN)
andBool #rangeBytes( DATA_LEN, DATA)
andBool #rangeUInt( 8, OPERATION)
; enum Enum.Operation, 3 possible values encoded to 0-2.
andBool OPERATION <=Int 2
andBool #rangeUInt( 256, SAFE_TX_GAS)
andBool #rangeUInt( 256, DATA_GAS)
andBool #rangeUInt( 256, GAS_PRICE)
andBool #rangeAddress( GAS_TOKEN)
andBool #rangeAddress( REFUND_RECEIVER)
andBool #rangeUInt( 256, NONCE)
andBool #rangeAddress( MASTER_COPY_ID)
andBool #rangeBytes( 32, DOMAIN_SEPARATOR)
andBool SAFE_TX_HASH ==Int keccak( #encodeArgs(
#bytes32(#parseHexWord({SAFE_TX_TYPEHASH})),
#address(TO),
#uint256(VALUE),
#bytes32(keccak(#asByteStackInWidth(DATA, DATA_LEN))),
#uint8(OPERATION),
#uint256(SAFE_TX_GAS),
#uint256(DATA_GAS),
#uint256(GAS_PRICE),
#address(GAS_TOKEN),
#address(REFUND_RECEIVER),
#uint256(NONCE) ))
; symbolic values for all parameters including DATA. Fixed DATA length.
[encodeTransactionData-data32]
+requires:
andBool DATA_LEN ==Int 32
[encodeTransactionData-data33]
+requires:
andBool DATA_LEN ==Int 33

Other debug messages

Look at various strings logged to System.err in classes SymbolicRewriter and FormulaContext. Alternatively, to see all possible debug messages, look at usages of fields logBasic and debugZ3 from class GlobalOptions: https://github.com/kframework/k/blob/gnosis/kernel/src/main/java/org/kframework/main/GlobalOptions.java

It's better to navigate this code from an IDE, like Intellij Idea.