diff --git a/CLAUDE.md b/CLAUDE.md index 7e30554dea..40c62d4889 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -178,6 +178,104 @@ To register a new spec, add one line to `KOMPILE_MAIN_FILE` in The glob `spec_files('functional', '*-spec.k')` picks it up automatically. `KOMPILE_MAIN_MODULE` defaults to `'VERIFICATION'`; only override it if your spec uses a different top module name. +## Diagnosing slow Haskell backend (`simplify` / `execute`) + +The booster server (`kore-rpc-booster`) reads the `KORE_RPC_OPTS` environment variable at startup and prepends its words to the CLI args. +Set it before any `kevm prove` invocation to inject diagnostic flags without changing Python code: + +```bash +KORE_RPC_OPTS="" uv --project kevm-pyk/ run kevm prove ... +``` + +Use `--log-file /tmp/booster.log` to write to a file; `--log-timestamps` adds wall-clock timestamps per line. + +For a full reference — log levels, source locations, and `contextLoggingEnabled` behaviour — see [`docs/kore-rpc-booster-logging.md`](docs/kore-rpc-booster-logging.md). +To test a local haskell-backend build, see [`docs/kup-override.md`](docs/kup-override.md). +To file a bug or performance report with the haskell-backend team, see [`docs/submitting-test-cases-to-haskell-backend.md`](docs/submitting-test-cases-to-haskell-backend.md). + +Key facts to keep in mind: + +- The **`simplify` endpoint always calls kore** after booster — unconditionally, not a fallback. + `-l Aborts` will not show this call; only a diff appears if kore actually changes something. +- **Kore has no LLVM**; it evaluates K functions via axiom rewriting only. + When booster has already fully evaluated a term via LLVM, kore's simplify pass is pure overhead. +- **`-l SimplifyKore` must be paired with a booster-side level** (e.g. `-l Timing`) to ensure `contextLoggingEnabled = True`; otherwise kore entries may not be emitted. + See `docs/kore-rpc-booster-logging.md` for the `contextLoggingEnabled` mechanism. +- **`-l Timing` is NOT a low-overhead flag for large terms.** + Any level with a `levelToContext` entry (including `Timing`) sets `contextLoggingEnabled = True`, + which enables ALL kore log entry types — including `DebugTerm`, which pretty-prints the full term at every step. + For terms with large concrete byte literals, this can add orders-of-magnitude overhead. + Use pyk's INFO timestamps (no `-l` flags) for true baseline measurements. +- **`booster-dev`** (`kevm prove --use-booster-dev`) runs pure booster with no kore proxy. + When the kore step is pure overhead for your proof, this is the right backend to use. + +### Quick log-level cheat sheet + +| Goal | Flags | Overhead | +|---|---|---| +| True per-request timing (pyk timestamps) | no `-l` flags | None | +| Booster/kore split per request | `-l Timing` | **Moderate — enables all kore log types; kore time 10× higher at large N** | +| Does kore change anything? | `-l Aborts` + grep `"Kore simplification: Diff"` | Moderate | +| Which booster rules fire / break? | `-l Simplify` (small N only) | 10–14× | +| What equations is kore attempting? | `-l SimplifyKore -l Timing` (small N) | High | +| Is SMT a bottleneck? | `-l SMT` | Low | +| Is LLVM being used? | grep `llvm` in log | None | + +### Interpreting `[failure][break]` vs `[failure][continue]` + +- `[failure][continue]` — rule did not match (pattern mismatch); booster moves to the next candidate. + Normal and fast. +- `[failure][break]` — rule matched but booster cannot confirm RHS is defined (non-total sub-symbols). + Booster stops trying to evaluate this term entirely. + This is the key signal that `[preserves-definedness]` or `total` annotations are needed. + +## Testing a local Haskell backend build + +Use `kup` to install K with a local haskell-backend checkout substituted for the upstream one. +This lets you test backend changes against full kevm proofs without modifying the project's Nix flake. + +```bash +# Check the current input tree (shows which haskell-backend hash is pinned): +kup list k.openssl.procps --inputs + +# Install the same K version with a local haskell-backend override: +kup install k.openssl.procps \ + --version v7.1.323 \ + --override haskell-backend ~/src/haskell-backend + +# Revert to the upstream backend: +kup install k.openssl.procps --version v7.1.323 +``` + +After installing, the kdist cache is stale — rebuild before running proofs: + +```bash +uv --project kevm-pyk/ run kevm-kdist build evm-semantics.haskell +``` + +When installing K from a local source checkout, also update `pyproject.toml` to point at the matching local pyk: + +```toml +# kevm-pyk/pyproject.toml +"kframework @ file:///home/dev/src/k-testing/pyk", +``` + +Then run `uv --project kevm-pyk/ sync` to install the local pyk. +Revert by restoring `"kframework=="` and re-syncing. + +For full details on how `--override` works and what kup does internally, see [`docs/kup-override.md`](docs/kup-override.md). + +## Updating local pyk vs local K + +When `kevm-pyk/pyproject.toml` points at `kframework @ file:///home/dev/src/k-testing/pyk`: + +- **pyk-only change** (Python code in `~/src/k-testing/pyk`): resync pyk only — no rebuild needed. + ```bash + uv --project kevm-pyk/ sync --reinstall-package kframework + ``` +- **K/Haskell backend change** (C++/Haskell in `~/src/k-testing` or `~/src/haskell-backend`): + run the full `kup install` + `kevm-kdist build` flow (see "Testing a local Haskell backend build"). + ## Commit discipline - Every commit must be **atomic and self-contained** — the project must build and fast tests must pass at each commit. diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md index aa0e14fd92..9d6f89933b 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md @@ -1750,10 +1750,10 @@ The various `CALL*` (and other inter-contract control flow) operations will be d syntax Bytes ::= #computeValidJumpDests(Bytes) [symbol(computeValidJumpDests), function, memo, total] | #computeValidJumpDests(Bytes, Int, Bytes, Int) [symbol(computeValidJumpDestsAux), function ] // ------------------------------------------------------------------------------------------------------------------------- - rule #computeValidJumpDests(PGM) => #computeValidJumpDests(PGM, 0, padRightBytes(.Bytes, lengthBytes(PGM), 0), lengthBytes(PGM)) - rule #computeValidJumpDests( _, I, RESULT, LEN) => RESULT requires I >=Int LEN - rule #computeValidJumpDests(PGM, I, RESULT, LEN) => #computeValidJumpDests(PGM, I +Int 1, RESULT[I <- 1], LEN) requires I #computeValidJumpDests(PGM, I +Int #widthOpCode(PGM [ I ]), RESULT, LEN) requires I #computeValidJumpDests(PGM, 0, padRightBytes(.Bytes, lengthBytes(PGM), 0), lengthBytes(PGM)) [preserves-definedness] + rule #computeValidJumpDests( _, I, RESULT, LEN) => RESULT requires I >=Int LEN [preserves-definedness] + rule #computeValidJumpDests(PGM, I, RESULT, LEN) => #computeValidJumpDests(PGM, I +Int 1, RESULT[I <- 1], LEN) requires I #computeValidJumpDests(PGM, I +Int #widthOpCode(PGM [ I ]), RESULT, LEN) requires I W -Int 94 requires W >=Int 96 andBool W <=Int 127 rule #widthOpCode(_) => 1 [owise] diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k index 392a50c6e9..571f024104 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k @@ -29,6 +29,10 @@ module BYTES-SIMPLIFICATION [symbolic] rule [bytes-concat-empty-right]: B:Bytes +Bytes .Bytes => B [simplification] rule [bytes-concat-empty-left]: .Bytes +Bytes B:Bytes => B [simplification] + // b"" is a Kore domain value (\dv{Bytes}("")) distinct from the .Bytes constructor; + // LLVM hooks (e.g. #encodeArgs base case) return b"", not .Bytes, so we need both forms. + rule [bytes-concat-empty-right-concrete]: B:Bytes +Bytes b"" => B [simplification, preserves-definedness] + rule [bytes-concat-empty-left-concrete]: b"" +Bytes B:Bytes => B [simplification, preserves-definedness] rule [bytes-concat-right-assoc-symb-l]: (B1:Bytes +Bytes B2:Bytes) +Bytes B3:Bytes => B1 +Bytes (B2 +Bytes B3) [symbolic(B1), simplification(40)] rule [bytes-concat-right-assoc-symb-r]: (B1:Bytes +Bytes B2:Bytes) +Bytes B3:Bytes => B1 +Bytes (B2 +Bytes B3) [symbolic(B2), simplification(40)] @@ -267,8 +271,8 @@ module BYTES-SIMPLIFICATION [symbolic] rule [lengthBytes-geq-zero]: 0 <=Int lengthBytes ( _ ) => true [simplification, smt-lemma] rule [lengthBytes-geq-nonPos]: X <=Int lengthBytes ( _ ) => true requires X <=Int 0 [simplification, concrete(X)] rule [lengthBytes-concat]: lengthBytes(BUF1 +Bytes BUF2) => lengthBytes(BUF1) +Int lengthBytes(BUF2) [simplification] - rule [lengthBytes-buf]: lengthBytes(#buf(S, _)) => S requires 0 <=Int S [simplification] - rule [lengthBytes-range]: lengthBytes(#range(_, S:Int, W:Int)) => maxInt(0, W) requires 0 <=Int S [simplification] + rule [lengthBytes-buf]: lengthBytes(#buf(S, _)) => S requires 0 <=Int S [simplification, preserves-definedness] + rule [lengthBytes-range]: lengthBytes(#range(_, S:Int, W:Int)) => maxInt(0, W) requires 0 <=Int S [simplification, preserves-definedness] rule [lengthBytes-prtw]: lengthBytes(#padRightToWidth(W:Int, B:Bytes)) => maxInt(lengthBytes(B), W) [simplification] rule [lengthBytes-leq-zero]: lengthBytes(B:Bytes) <=Int 0 => B ==K .Bytes [simplification] @@ -306,5 +310,5 @@ module BYTES-SIMPLIFICATION [symbolic] rule [lookup-as-asWord]: B:Bytes [ I:Int ] => #asWord ( #range ( B, I, 1 ) ) requires 0 <=Int I andBool I X + requires #rangeUInt ( 256, X ) + [simplification, preserves-definedness] + + // General reduction: #asWord of a range extracted from a buf. + // #buf(N, X) is the big-endian N-byte encoding of X. Taking W bytes + // starting at byte S gives (X >> (8*(N-S-W))) & (2^(8*W)-1). + // Activated with concrete N, S, W so Booster can evaluate the arithmetic. + rule [asWord-range-buf]: + #asWord ( #range ( #buf ( N:Int, X:Int ), S:Int, W:Int ) ) => + X /Int ( 2 ^Int ( 8 *Int ( N -Int S -Int W ) ) ) modInt ( 2 ^Int ( 8 *Int W ) ) + requires 0 <=Int S andBool 0 >Int N => #asWord ( #range ( BA, 0, lengthBytes( BA ) -Int ( N /Int 8 ) ) ) @@ -137,6 +156,30 @@ module EVM-INT-SIMPLIFICATION andBool lengthBytes ( BA1 +Bytes BA2 ) <=Int 32 [simplification, concrete(BA2, X), preserves-definedness] + // Masking `#asWord(BA)` with a byte-aligned maxUIntN mask (= 2^N-1) gives + // the lower N/8 bytes as a new `#asWord`. Fires before `multimask-b-and` + // (priority 50) to avoid an intermediate form that Booster cannot close. + rule [bit-mask-asWord-m]: + MASK:Int &Int #asWord(BA:Bytes) => + #asWord(#range(BA, 32 -Int (log2Int(MASK +Int 1) /Int 8), log2Int(MASK +Int 1) /Int 8)) + requires 0 + #asWord(#range(BA, 0, 32 -Int (log2Int(pow256 -Int MASK) /Int 8)) +Bytes #buf(log2Int(pow256 -Int MASK) /Int 8, 0)) + requires 0 <=Int MASK + andBool MASK Int C +Int D => A -Int C >Int D -Int B [concrete(B, D), symbolic(A, C), simplification(45)] rule A +Int B >=Int C +Int D => A -Int C >=Int D -Int B [concrete(B, D), symbolic(A, C), simplification(45)] + rule [int-eq-comm-concrete]: + N:Int ==Int X:Int => X ==Int N + [simplification(30), concrete(N), symbolic(X)] + rule A +Int B ==Int A => B ==Int 0 [simplification(40)] rule A +Int B ==Int B => A ==Int 0 [simplification(40)] rule A +Int B ==Int C +Int B => A ==Int C [simplification(40)] @@ -101,6 +105,11 @@ module INT-SIMPLIFICATION-HASKELL [symbolic] rule A -Int B A A <=Int B [simplification, symbolic(A, B)] + // Mixed range contradictions: A < B /\ C <= A where B <= C (all concrete B, C) + // Requires is purely concrete (both B and C are concrete), so no circular self-application. + rule A:Int false requires B <=Int C [simplification, concrete(B, C)] + rule C:Int <=Int A:Int andBool A:Int false requires B <=Int C [simplification, concrete(B, C)] + endmodule module INT-SIMPLIFICATION-COMMON @@ -133,6 +142,7 @@ module INT-SIMPLIFICATION-COMMON rule (A +Int B) +Int (C -Int B) => A +Int C [simplification] rule (A -Int B) -Int (C -Int B) => A -Int C [simplification] rule ((A -Int B) -Int C) +Int B => A -Int C [simplification] + rule A +Int ((B -Int A) +Int C) => B +Int C [simplification] // 5 terms // NOTE: required for `tests/specs/functional/infinite-gas-spec.k.prove` (haskell) @@ -232,6 +242,35 @@ module INT-SIMPLIFICATION-COMMON rule [maxInt-factor-left]: maxInt ( A:Int +Int B:Int, A:Int +Int C:Int ) => A +Int maxInt ( B, C ) [simplification] rule [maxInt-factor-right]: maxInt ( A:Int +Int B:Int, C:Int +Int B:Int ) => maxInt ( A, C ) +Int B [simplification] + // minInt true + requires A true + requires A true + requires B <=Int D + [simplification(40), preserves-definedness] + rule [minint-leq-maxint-shift-b]: + minInt(_A:Int +Int E:Int, B:Int +Int E:Int) <=Int maxInt(_C:Int +Int F:Int, D:Int +Int F:Int) => true + requires B <=Int D andBool E <=Int F + [simplification(40), preserves-definedness] + // Factored forms: after minInt-factor-{left,right} + maxInt-factor-{left,right} (priority 50) have fired, + // the non-linear shift rules above no longer match; these linear rules catch the result. + rule [minint-lt-maxint-shift-a-factored]: + E:Int +Int minInt(A:Int, _B:Int) true + requires A true + requires B <=Int D andBool E <=Int F + [simplification(40), preserves-definedness] + // ########################################################################### // inequality // ########################################################################### @@ -241,6 +280,14 @@ module INT-SIMPLIFICATION-COMMON rule A false requires 0 <=Int B [simplification] + rule A:Int <=Int A:Int => true [simplification] + + // Higher-priority: short-circuit to true directly when path condition already has 0 <=Int B. + rule A:Int <=Int A:Int +Int B:Int => true requires 0 <=Int B [simplification(40)] + rule A:Int <=Int A:Int +Int B:Int => 0 <=Int B [simplification] + + rule A:Int false [simplification] + rule 0 true requires 0 <=Int A [simplification, preserves-definedness] // inequality sign normalization diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k index d6ae1bb695..45a6cfefc3 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k @@ -36,12 +36,29 @@ module LEMMAS-WITHOUT-SLOT-UPDATES [symbolic] // Set Reasoning // ######################## + // Membership in the concat (_Set_) form — fires in both kore and booster. rule X in (SetItem(Y) _ ) => true requires X ==Int Y [simplification] rule X in (SetItem(Y) REST) => X in REST requires notBool ( X ==Int Y ) [simplification] + // NOTE: the two non-linear rules below fire in kore but are INDETERMINATE in booster. + // Booster internalises SetItem(X) as KSet{def,[X],None}; matchSets() returns addIndeterminate + // for any non-empty KSet (Match.hs:673-676). Backend change required to fix. rule ( S:Set |Set SetItem ( X ) ) |Set SetItem( X ) => ( S:Set |Set SetItem ( X ) ) [simplification] rule ( ( S:Set |Set SetItem ( X ) ) |Set SetItem ( Y ) ) |Set SetItem( X ) => ( ( S:Set |Set SetItem ( X ) ) |Set SetItem ( Y ) ) [simplification] + // Membership in the |Set (union) form — fires in kore only (same matchSets limitation). + // Kore uses these to discharge the requires-clause of the dedup rule below. + rule X:Int in (REST:Set |Set SetItem(Y:Int)) => true requires X ==Int Y [simplification] + rule X:Int in (REST:Set |Set SetItem(Y:Int)) => X in REST requires notBool ( X ==Int Y ) [simplification] + + // Deduplication of repeated concrete Int elements in a symbolic |Set expression. + // Required in normal mode (where kore's simplify step fires it) but INDETERMINATE in booster. + // Booster cannot match SetItem(X) in the pattern: matchSets() is unimplemented for non-empty + // KSets (booster/Match.hs:673-676). Cannot be fixed from K source; requires backend change. + // Context: #touchAccounts in evm.md adds addresses via |Set; when the same address is added + // twice to a symbolic touchedAccounts, this rule is needed to normalize back to a 2-element form. + rule S:Set |Set SetItem(X:Int) => S requires X in S [simplification] + // ######################## // Word Reasoning // ######################## @@ -245,6 +262,30 @@ module LEMMAS-HASKELL [symbolic] requires notBool ( I1 ==Int I2 ) [simplification] + // ######################## + // #widthOpCode range + // ######################## + + // #widthOpCode always returns 1..33 (PUSH ops 2..33, everything else 1). + // smtlib(widthOpCode) on the declaration lets smt-lemma encode these as + // universally-quantified bounds so the solver can discharge side conditions + // containing #widthOpCode without needing to evaluate it concretely. + rule [widthOpCode-lb]: 0 <=Int #widthOpCode(_:Int) => true [simplification, smt-lemma] + rule [widthOpCode-ub]: #widthOpCode(_:Int) <=Int 33 => true [simplification, smt-lemma] + + // Booster's equation engine does not descend inside #widthOpCode(...) to + // apply bytes-concat-lookup-{left,right}. These rules compose the two + // steps so the full concrete-prefix lookup can be reduced in one go. + rule [widthOpCode-concat-left]: + #widthOpCode ( ( B1:Bytes +Bytes _B2:Bytes ) [ I:Int ] ) => #widthOpCode ( B1 [ I ] ) + requires 0 <=Int I andBool I #widthOpCode ( B2 [ I -Int lengthBytes ( B1 ) ] ) + requires lengthBytes ( B1 ) <=Int I + [simplification, preserves-definedness] + // ######################## // Boolean Logic // ######################## @@ -259,4 +300,9 @@ module LEMMAS-HASKELL [symbolic] rule [notBool-or]: notBool ( A orBool B ) => ( notBool A ) andBool ( notBool B ) [simplification(60)] rule [notBool-and]: notBool ( A andBool B ) => ( notBool A ) orBool ( notBool B ) [simplification(60)] + rule [bool-or-not-self]: B:Bool orBool notBool B:Bool => true [simplification] + rule [bool-not-or-self]: notBool B:Bool orBool B:Bool => true [simplification] + rule [bool-and-not-self]: B:Bool andBool notBool B:Bool => false [simplification] + rule [bool-not-and-self]: notBool B:Bool andBool B:Bool => false [simplification] + endmodule diff --git a/kevm-pyk/src/tests/integration/test_prove.py b/kevm-pyk/src/tests/integration/test_prove.py index f0c0b8b590..00ece262cd 100644 --- a/kevm-pyk/src/tests/integration/test_prove.py +++ b/kevm-pyk/src/tests/integration/test_prove.py @@ -115,6 +115,7 @@ def exclude_list(exclude_file: Path) -> list[Path]: 'functional/slot-updates-spec.k': 'slot-updates-spec.k', 'functional/storageRoot-spec.k': 'storageRoot-spec.k', 'functional/compute-valid-jump-dests-spec.k': 'compute-valid-jump-dests-spec.k', + 'functional/set-dedup-spec.k': 'set-dedup-spec.k', 'mcd/functional-spec.k': 'functional-spec.k', 'mcd-structured/functional-spec.k': 'functional-spec.k', } diff --git a/tests/specs/functional/compute-valid-jump-dests-spec.k b/tests/specs/functional/compute-valid-jump-dests-spec.k index a415944537..61d055c96a 100644 --- a/tests/specs/functional/compute-valid-jump-dests-spec.k +++ b/tests/specs/functional/compute-valid-jump-dests-spec.k @@ -18,10 +18,17 @@ endmodule module COMPUTE-VALID-JUMP-DESTS-SPEC imports VERIFICATION - // Performance benchmark: concrete prefix, one JUMPDEST, concrete suffix, then 32 symbolic - // bytes. The #buf(32, INT_VAR) tail forces Haskell-backend symbolic evaluation rather - // than pure LLVM concrete evaluation, exposing the O(N) overhead of re-evaluating - // lengthBytes(PGM) on every loop iteration with the old definition. + // Fast smoke test: small concrete prefix + one JUMPDEST + small concrete suffix + + // 32 symbolic bytes. Use this for quick iteration during development. + claim [compute-valid-jump-dests-fast]: + runLemma(#computeValidJumpDests(padRightBytes(.Bytes, 5, 0) +Bytes (91 : .Bytes) +Bytes padRightBytes(.Bytes, 5, 0) +Bytes #buf(32, INT_VAR))) + => doneLemma(?_:Bytes) + ... + requires #rangeUInt(256, INT_VAR) + + // Performance benchmark: large concrete prefix exposes O(N) overhead in any + // per-iteration re-evaluation of lengthBytes(PGM). Run without --haskell-logging + // for true baseline timing. claim [compute-valid-jump-dests-perf]: runLemma(#computeValidJumpDests(padRightBytes(.Bytes, 1000, 0) +Bytes (91 : .Bytes) +Bytes padRightBytes(.Bytes, 1000, 0) +Bytes #buf(32, INT_VAR))) => doneLemma(?_:Bytes) diff --git a/tests/specs/functional/set-dedup-spec.k b/tests/specs/functional/set-dedup-spec.k new file mode 100644 index 0000000000..d33b84ea18 --- /dev/null +++ b/tests/specs/functional/set-dedup-spec.k @@ -0,0 +1,48 @@ +requires "evm.md" +requires "lemmas/lemmas.k" + +module VERIFICATION + imports LEMMAS + imports EVM + + syntax StepSort ::= Int | Bool | Set + // ------------------------------------- + + syntax KItem ::= runLemma ( StepSort ) [symbol(runLemma)] + | doneLemma( StepSort ) + // -------------------------------------- + rule runLemma( T ) => doneLemma( T ) ... + +endmodule + +module SET-DEDUP-SPEC + imports VERIFICATION + + // Set deduplication via |Set and membership + // ------------------------------------------ + // These claims test the rule: + // rule S:Set |Set SetItem(X:Int) => S requires X in S [simplification] + // together with the supporting membership rules that let the `X in S` side + // condition discharge when S is written in |Set form. + + // Basic: one duplicate concrete element + claim [set-dedup-01]: + runLemma ( A:Set |Set SetItem(1) |Set SetItem(1) ) + => doneLemma ( A:Set |Set SetItem(1) ) ... + + // Two distinct elements, one of which is duplicated + claim [set-dedup-02]: + runLemma ( A:Set |Set SetItem(1) |Set SetItem(2) |Set SetItem(1) ) + => doneLemma ( A:Set |Set SetItem(1) |Set SetItem(2) ) ... + + // Both elements are duplicated + claim [set-dedup-03]: + runLemma ( A:Set |Set SetItem(1) |Set SetItem(2) |Set SetItem(1) |Set SetItem(2) ) + => doneLemma ( A:Set |Set SetItem(1) |Set SetItem(2) ) ... + + // Duplicate appears after other elements (tests deeper membership check) + claim [set-dedup-04]: + runLemma ( A:Set |Set SetItem(1) |Set SetItem(2) |Set SetItem(3) |Set SetItem(1) ) + => doneLemma ( A:Set |Set SetItem(1) |Set SetItem(2) |Set SetItem(3) ) ... + +endmodule diff --git a/tests/specs/mcd/verification.k b/tests/specs/mcd/verification.k index cf400bac8b..2bcc3e0045 100644 --- a/tests/specs/mcd/verification.k +++ b/tests/specs/mcd/verification.k @@ -139,7 +139,7 @@ module LEMMAS-MCD [symbolic] // Keccak // ######################## - rule keccak(_) ==Int I => false requires #rangeSmall(I) [simplification] + rule keccak(_) ==Int I => false requires #rangeSmall(I) [simplification, smt-lemma] rule keccak(_) +Int I1 ==Int I2 => false requires #rangeSmall(I1) andBool #rangeSmall(I2) [simplification]