Proof search timeouts

[MrChico]

I've been running into the scenario where I try to prove something which ends up taking a lot of time, (>15 minutes) and eat up a lot of memory. Sometimes the process ends with the following output:

./../evm-semantics/kevm prove dappsys/exp-success-spec.k
[Error] Internal: Uncaught exception thrown of type OutOfMemoryError.
Please rerun your program with the --debug flag to generate a stack trace, and
file a bug report at https://github.com/kframework/k/issues (GC overhead limit
exceeded)
[Warning] Critical: missing SMTLib translation for #memoryUsageUpdate (missing
SMTLib translation for #memoryUsageUpdate)
[Warning] Critical: missing SMTLib translation for #rangeAux (missing SMTLib
translation for #rangeAux)
...

From a user perspective, it's not a very pleasant experience having K consume my computer. From a provers perspective, I would like to know how I can construct lemmas to limit the proof search space.

[ehildenb]

In the run_proof function in script kevm, you can change K_OPTS=-Xmx5G to a lower amount than 5G to make it fail sooner (this is the memory allocated to the JVM before it will die).

When you get missing SMTLib translation errors (eg for #memoryUsageUpdate), you can try adding the attribute smtlib(memoryUsageUpdate) to the production for #memoryUsageUpdate. It will give "uninterpreted function" semantics to that production when making queries to Z3.

When the other people working on proving things with K are going about it, they usually fire up the prover in IntelliJ and step through debug points to have access to state information that the prover is holding in memory. It' not a very good approach user-experience wise :/

Another option is passing the --debug flag to the ./kevm prove path-to-spec.k --debug command. It may print out more information about queries being passed to Z3 and such.

I'm going to leave this issue open so that @daejunpark and @iustines have a chance to weigh in and provide advice about how to prove things.

[daejunpark]

There are many reasons for the out of memory, and I cannot pin-point one of them without looking at the spec.

As a general advice of debugging the spec (and k prover), here is a pointer to some important part of source code of the kprover so that you can navigate using the IntelliJ debugger.

• starting point: https://github.com/kframework/k5/blob/master/java-backend/src/main/java/org/kframework/backend/java/symbolic/SymbolicRewriter.java#L579
• you can set a breakpoint here to see each step of KEVM execution: https://github.com/kframework/k5/blob/master/java-backend/src/main/java/org/kframework/backend/java/symbolic/SymbolicRewriter.java#L597
• this is a function where each semantic step is made: https://github.com/kframework/k5/blob/master/java-backend/src/main/java/org/kframework/backend/java/symbolic/SymbolicRewriter.java#L630
• inside fastComputeRewriteStep, this is the main loop that iterates each semantic rule and try to apply: https://github.com/kframework/k5/blob/master/java-backend/src/main/java/org/kframework/backend/java/symbolic/SymbolicRewriter.java#L164 You can check if only the correct rules are applied here. If a spec is wrong or too weak, wrong rules may be applied (meaning that infeasible or undesirable execution paths are being explored), which could be the reason for out-of-memory or long-running process issues.

[MrChico]

@ehildenb how about if I do know the SMTLib translation of a function? For example, I get the error message:

[Warning] Critical: missing SMTLib translation for _^Int__INT (missing SMTLib translation for _^Int__INT)

and would like to tell Z3 that this should be translated to exponentiation?

[ehildenb]

@MrChico we have an "smt-prelude". In the EVM directory, look at .build/k/k-distribution/include/z3. The file basic.smt2 shows what a basic SMT prelude can look like (in Z3 syntax).

You can specify your smt prelude using --smt_prelude PATH/TO/FILE.smt2. I can't find what the default value is, but I think it was basic.smt2 IIRC. @daejunpark can you provide more info?

[ehildenb]

But basically, you can have your own prelude which you specify for KEVM.

I think though, you should be able to achieve the same thing using the concrete attribute on the rules which are causing trouble, and adding lemmas in K directly. You can look at file tests/proofs/resources/lemmas.md for an example of an abstraction (eg. nthbyteof). Basically, you block usage of certain rules in symbolic mode by adding the concrete attribute, then provide other rules which give the correct symbolic semantics to use for simplification.

Note that these extra lemmas are never passed to Z3 directly, the simplification is done in K itself. This has the advantage that it will be slightly quicker, and in the same readable format as the rest of the definition.

If you do come up with good abstractions + lemmas for more of the operators in KEVM which make proofs faster/more robust, I'm happy to add them to mainline KEVM.

Also note, the missing SMTLIB translation errors look scary, but they aren't as bad as you might think. Have you added the --debug flag to your invocation of krun? That will print out the actual queries being made to Z3, which can be very informative.

[norbeyandresg]

@MrChico I have the same error

[Warning] Critical: missing SMTLib translation for _^Int__INT (missing SMTLib translation for _^Int__INT)

could you solve it?

[MrChico]

@norbeyandresg I've not yet solved that particular warning, but this will not cause z3 to throw. If your issue is still that (error "line 20 column 206: unknown function/constant smt_seq_elem"), then you should be able to resolve it by adding that smt-prelude as described above. The smt_seq_elem function is defined in evm-semantics/.build/k/k-distribution/include/z3/basic.smt2

[norbeyandresg]

@MrChico I ran the prove whit the smt-prelude but the the flag seems doesn't work because I still get the same error. I'm using this: ./kevm prove tests/proofs/resources/pow-of-two-spec.k --smt_prelud .build/k/k-distribution/include/z3/basic.smt2. Am I doing something wrong?