lemmas: booster-only gap fixes — widthOpCode, int/bytes simplifications, preserves-definedness#2849

Closed

ehildenb wants to merge 20 commits into

masterfrom

kevm-lemmas-booster

Commits on May 25, 2026

evm.md: add total to #widthOpCode, preserves-definedness to #computeValidJumpDests rules

ehildenb
and
claude
committed
lemmas/bytes-simplification.k: add preserves-definedness to lookup-as-asWord

ehildenb
and
claude
committed
lemmas: Round 2 Booster gap fixes
ehildenb
committed
lemmas/lemmas.k: Round 3 — add widthOpCode-lb (0 <=Int #widthOpCode(_) => true)
ehildenb
committed
lemmas: Round 4 — widthOpCode concat rules, asWord-range-buf
ehildenb
committed
evm.md, lemmas.k, CLAUDE.md: Round 5 — smtlib annotation for #widthOpCode, smt-lemma bounds

ehildenb
and
claude
committed
compute-valid-jump-dests-spec.k: add fast N=5 claim alongside perf N=1000 claim

ehildenb
and
claude
committed
lemmas/int-simplification.k: add minInt/maxInt comparison simplification rules

ehildenb
and
claude
committed
lemmas/evm-int-simplification.k: add bit-mask-asWord-m and bit-notmask-asWord-nm
ehildenb
committed
lemmas/int-simplification.k: normalize ==Int commutativity concrete-on-left

ehildenb
and
claude
committed
lemmas/{int-simplification,lemmas}.k: add arithmetic + Bool simplification lemmas

ehildenb
and
claude
committed
lemmas/int-simplification.k, lemmas/lemmas.k: fix two booster-only failing claims

ehildenb
and
claude
committed
lemmas/bytes-simplification.k: add concrete b"" concat identity rules

ehildenb
and
claude
committed
tests/specs/functional/set-dedup-spec.k, test_prove.py: add set-dedup functional spec

ehildenb
and
claude
committed
lemmas/lemmas.k: add KSet match limitation comments for permanently-dead booster rules
ehildenb
committed
CLAUDE.md: drop misplaced Group D sections; fix stale bench-prove.py refs

ehildenb
and
claude
committed
CLAUDE.md: document pyproject.toml local-pyk pointer and uv sync workflow

ehildenb
and
claude
committed
lemmas/lemmas.k: drop map-update-comm — breaks DSS implies checks

ehildenb
and
claude
committed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

lemmas: booster-only gap fixes — widthOpCode, int/bytes simplifications, preserves-definedness#2849

lemmas: booster-only gap fixes — widthOpCode, int/bytes simplifications, preserves-definedness#2849
ehildenb wants to merge 20 commits into
masterfrom
kevm-lemmas-booster

Commits on May 25, 2026

evm.md: add total to #widthOpCode, preserves-definedness to #computeValidJumpDests rules

lemmas/bytes-simplification.k: add preserves-definedness to lookup-as-asWord

lemmas: Round 2 Booster gap fixes

lemmas/lemmas.k: Round 3 — add widthOpCode-lb (0 <=Int #widthOpCode(_) => true)

lemmas: Round 4 — widthOpCode concat rules, asWord-range-buf

evm.md, lemmas.k, CLAUDE.md: Round 5 — smtlib annotation for #widthOpCode, smt-lemma bounds

compute-valid-jump-dests-spec.k: add fast N=5 claim alongside perf N=1000 claim

lemmas/int-simplification.k: add minInt/maxInt comparison simplification rules

lemmas/evm-int-simplification.k: add bit-mask-asWord-m and bit-notmask-asWord-nm

lemmas/int-simplification.k: normalize ==Int commutativity concrete-on-left

lemmas/{int-simplification,lemmas}.k: add arithmetic + Bool simplification lemmas

lemmas/int-simplification.k, lemmas/lemmas.k: fix two booster-only failing claims

lemmas/bytes-simplification.k: add concrete b"" concat identity rules

tests/specs/functional/set-dedup-spec.k, test_prove.py: add set-dedup functional spec

lemmas/lemmas.k: add KSet match limitation comments for permanently-dead booster rules

CLAUDE.md: drop misplaced Group D sections; fix stale bench-prove.py refs

CLAUDE.md: document pyproject.toml local-pyk pointer and uv sync workflow

lemmas/lemmas.k: drop map-update-comm — breaks DSS implies checks

Commits on May 26, 2026

tests/specs/mcd/verification.k: add [smt-lemma] to keccak inequality rule

Merge remote-tracking branch 'upstream/master' into kevm-lemmas-booster