Writing Kontrol Lemmas

Writing Kontrol Lemmas

Overview

A K simplification lemma is a rewrite rule tagged [simplification] that Kontrol/KEVM applies during proof search. When kontrol prove gets stuck, the usual cure is a rule that discharges a side condition or collapses a composite term (bitwise algebra, keccak disjointness, Map lookups, bool2Word predicates, symbolic +Bytes blobs, etc.).

Core principle: Never commit a lemma whose reduction you haven't verified on the actual stuck term. Pair every candidate rule with a unit test under a runLemma/doneLemma scaffolding that runs against a minimal stand-alone kompiled definition — not the full Solidity build.

Why a separate definition. kontrol build takes minutes and is invalidated by any .k change. A lemma-test definition is just EVM + lemmas.k + the scaffolding — orthogonal to whatever state out/kompiled is in, so you can iterate on lemmas while an in-flight kontrol prove runs.

When to Use

Symptoms that a new lemma is needed:

• kontrol prove finishes with "pending" leaves in the KCFG
• A proof times out during simplification
• A branch splits where the path condition is already decidable but K can't see it
• The stuck term involves &Int, |Int, xorInt, >>Int, <<Int, keccak, Map:lookup / _Map_[_], in_keys, bool2Word, #lookup, #asWord, composite _+Bytes_ blobs, modInt pow256 wrappers
• A test_* proof fails with Matching failed or unreduced predicates in <k>

When NOT to Use

Symptoms where a lemma is NOT the right answer — see flag-fixes.md:

• EVMC_BAD_JUMP_DESTINATION inside a constructor with a symbolic immutable → use --symbolic-immutables
• Enum branches not pruned → --enum-constraints
• Coarse KCFG around external calls → --break-on-calls
• Real constructor behavior matters for storage layout → --run-constructor

Skim kontrol prove --help once per stuck proof before committing to algebra. Flags are cheap, sounder, and invisible in the KCFG.

Also out of scope:

• Debugging Z3 / SMT encoding details — this skill edits K simplification rules, not the solver. (See lessons-learned.md for the bitwise-ops- as-uninterpreted consequence and how to work around it.)
• Running the production kontrol prove end-to-end — this skill produces a rule + probe spec; the final re-run is the user's.
• Rewriting kontrol build or Solidity artifacts — lemmas operate on the K semantics, not the compiled bytecode.

Scope boundaries

• In scope: Diagnosing stuck KCFG leaves as algebra vs. flag/config, writing [simplification] rules, scaffolding probe specs under a separate lemma-tests kompiled definition, checking soundness with the asymmetric +Int wrap, and minimizing the resulting rule set.
• Out of scope: Modifying kontrol.toml's require = target beyond the project's existing lemmas file, changing out/kompiled (the production build), and authoring lemmas that require new sorts beyond Int | Bool | Bytes | Map without extending run-lemma.k's StepSort.

Usage

The user reports a pending or stuck KCFG leaf from kontrol prove and wants a lemma to close it. Work through the gating checklist ("Before writing a lemma"), then the Workflow section.

Example user request: `kontrol prove` on Foo.testFuzz_bar left a pending
leaf at node 42 — the <k> cell shows bool2Word(L ==Int 0) unreduced and
the path condition has 0 <Int L. Please write a lemma to close it.

Inputs and Assumptions

Requires:

• Kontrol project with kontrol.toml, a lemmas file listed under [build.default] require = … (often test/kontrol/lemmas.k), and a working kontrol + kevm install. The wrapper resolves kevm from kontrol's nix-store closure, so nix-store must be on PATH.
• A stuck / pending KCFG leaf identified via kontrol show <Contract>.<method> --no-minimize, with the offending subterm and the path condition known.
• Write access to the project's lemmas file and permission to create a lemma-tests directory (e.g. test/kontrol/lemma-tests/) and a scripts/ (or script/) entry for the wrapper.

Optional:

• Pre-existing test/kontrol/lemma-tests/ and scripts/ directories — the scaffolding and wrapper are dropped in next to whatever the project already uses.
• auxiliary-lemmas = true under [build.default] in kontrol.toml (pulls in Kontrol's upstream helper lemmas; check before writing a duplicate).

Outputs (task contract)

• Produces:
  • New [simplification] rules in the project's lemmas file, each paired with a firing claim and a soundness claim (asymmetric +Int wrap — see lemma-testing.md) in a <name>-spec.k file under the lemma-tests directory.
  • A PROOF PASSED run from scripts/kontrol-lemma-test.sh <stem> confirming the rules fire on the stuck shape against a minimal EVM + lemmas definition (no Solidity build).
  • Optionally, a minimized rule set after running scripts/minimize-lemmas.py, with a per-run $TMPDIR/minimize-lemmas-XXXXXX/results.tsv log classifying each rule as necessary or removable.
• Hands off to: Re-running the original kontrol prove --match-test <Contract>.<method> to confirm the previously-pending leaf closes.

Before writing a lemma: is this really an algebra problem?

pending in a KCFG leaf does not mean "the theory cannot simplify this". It means "the prover has not driven this leaf to a terminal state yet". A pending leaf can be any of:

1. Algebra-stuck — the term genuinely needs a new simplification. This is what the rest of this skill addresses.
2. Iteration-exhausted — the prover hit its per-node step budget. Bump max-iterations in kontrol.toml (or pass --max-iterations) and re-run before writing anything.
3. Fail-fast-truncated — fail-fast is on by default, so the runner stops as soon as any leaf fails. Sibling leaves that were pending when the runner exited are pending because they never got worked on, not because they're stuck. Check sibling statuses before treating any leaf as algebra-stuck; pass --no-fail-fast (or set fail-fast = false in kontrol.toml) to drive all branches to completion when you need the full picture.
4. Flag-curable — see flag-fixes.md. A stuck symbolic-immutable JUMPDEST looks exactly like an algebra problem from the outside.

Diagnosis order: (a) sibling statuses, (b) max-iterations, (c) flags in flag-fixes.md, (d) algebra. Writing a lemma skips that ladder and wastes one kompile cycle per attempt.

Workflow

1. Diagnose. kontrol show <Contract>.<method> --no-minimize | less. Note the stuck node id, the path condition at each pending/failing leaf, and the unreduced term in the leaf's <k> cell.
2. Gate it. Work through the "is this really algebra?" checklist above — sibling statuses, max-iterations, flag-fixes.md. Only proceed past this point if the pending leaf's term is genuinely one the existing theory can't simplify.
3. Pick the subterm to probe. The <k> cell typically has a whole chain (JUMPI D I ~> #pc[JUMPI] ~> #execute ~> ...). You only need to wrap the one subterm the theory is failing to reduce, not the whole chain. See "KCFG → runLemma recipes" below for the common shapes. Reproduce variables with Kontrol's KV<N>_<argName>:<Sort> naming verbatim so any concrete(...) / symbolic(...) attributes on lemmas line up with the actual ground/symbolic split.
4. Set up scaffolding (once per project):
   • Locate the project's lemmas file — it's whatever appears under require = in kontrol.toml's [build.default] (often test/kontrol/lemmas.k, sometimes lemmas.k at the repo root).
   • Create a lemma-tests directory (e.g. test/kontrol/lemma-tests/ if not already present).
   • Copy run-lemma.k into the lemma-tests directory. Edit its requires "lemmas.k" line if the project's lemmas file has a different basename — the include resolves via the wrapper's -I path.
   • Copy kontrol-lemma-test.sh into a scripts/ (or script/, match the project) directory. Edit the four path variables at the top: SPEC_DIR, LEMMAS_DIR, DEFN_DIR, PROOFS_DIR. LEMMAS_DIR must be the directory containing the lemmas file (not the file itself).
5. Write a probe spec FIRST — no new lemmas yet. At <lemma-tests-dir>/<name>-spec.k:

   requires "run-lemma.k"
   
   module <NAME>-SPEC
       imports VERIFICATION
       claim [probe]:
           <k> runLemma ( <stuck subterm> ) => doneLemma ( <expected RHS> ) ... </k>
           requires <path condition constraints from the pending leaf>
   endmodule

   VERIFICATION re-exports the project's lemmas via run-lemma.k's imports KONTROL-LEMMAS, so whatever is already in lemmas.k (plus auxiliary-lemmas if enabled in kontrol.toml) is in scope.
6. Run the wrapper on the probe spec — in the background. Kompile alone is ~60 s per invocation, so synchronous foreground runs freeze the conversation:

   Bash(run_in_background: true, command: "scripts/kontrol-lemma-test.sh <spec-stem>")
   BashOutput(<shell id>)               # poll until the shell exits

   Never invoke the wrapper with run_in_background: false — the same rule applies to minimize-lemmas.py, which internally calls the wrapper once per rule and takes N × one kompile cycle. Once the shell has exited, read the tail of the output to conclude:
   • PROOF PASSED → the existing theory already simplifies this shape. The proof's pending leaf is NOT an algebra problem — return to the gating checklist (step 2) and look at iteration budget, fail-fast, or a flag.
   • PROOF FAILED → inspect the stuck KCFG node (out/proofs-lemma-tests/<spec>/kcfg/ or kontrol view-kcfg) and the K_CELL: doneLemma(LHS' #Implies RHS) diff. LHS' is how far the booster got; the gap between LHS' and RHS tells you what rule is missing.
7. Add candidate rules to the project's lemmas file. Every rule must satisfy the four requirements below (concise, sound, maintainable, readable). Re-run the wrapper; iterate until the probe spec passes.
8. Check soundness with an asymmetric claim — see lemma-testing.md. A rule that passes runLemma(E) => doneLemma(E) is not a soundness test; wrap in +Int so an unsound step surfaces as a numeric diff.
9. Integrate. Once the spec passes, the rules are already in the project's lemmas file and flow into the next kontrol build.
10. Re-run the original proof to confirm the previously-pending leaf closes.
11. Minimize with the driver in minimize-lemmas.md. Intuition overestimates what's load-bearing; dead simplification rules widen the search space and slow every future proof.

KCFG → runLemma recipes

Common stuck-term shapes and how to wrap them. Pick the recipe that matches the leaf's <k> cell.

For anything else, copy the exact subterm from the leaf's <k> and the exact constraints from the pending leaf's path condition. Keep the wrapped subterm as narrow as possible — wrapping too much just slows kompile and obscures the failure diff.