[TheDarkLightX]

Fixes #871.

Editing a K file supplied through --require could trigger recompilation while leaving its previous copy in out/kompiled/requires, so the rebuilt definition still used old lemmas. Compare the required source files and their copies by content, and refresh missing or changed copies before regeneration and recompilation.

Invalidate the compiled-success timestamp before repairing required-file copies and before compilation. Remove it after failed or interrupted compilation, including when one backend has already completed, so retries rebuild. Preserve caching for unchanged inputs and Solidity-only changes. Only print the --regen message when that option was explicitly requested.

Add unit regressions for content changes with preserved source mtimes, stale and missing copies, unchanged inputs, generation and compilation failures followed by retries, and contract-digest changes. The integration regression compiles a lemma that evaluates to 0, edits it to evaluate to 1, and checks the new result without --regen or --rekompile. It also checks that unchanged and Solidity-only builds reuse the compiled definition.

Current validation for head 826e4c7ab176e4f03bad0f58c306e39706751387 (October 8, 2026):

• The reviewer-requested changes are present: symbol(lemmaValue), parametrized fresh-copy and cache cases, and removal of the redundant source-edit retry while retaining stale-copy failure/retry and generation retry.
• This head merges current master into the branch. The three files belonging to this PR are unchanged from 15b21d43; the additional changes in the historical comparison are upstream changes brought in by the merge.
• Test PR: all 9 jobs passed — Code Quality Checks, Unit Tests, End to End Sanity Tests, Integration Tests, CSE Tests, Profiling, Docker Tests, Nix Tests (MacM1), and Nix Tests (normal).
• Unit Tests: 101 passed, including all seven required-lemma regression cases.
• Integration Tests: 164 passed, 236 skipped. The log explicitly records test_foundry_kompile_updated_lemma passing with real compilation and Kore simplification.
• Lint Workflows: both jobs passed (zizmor and actionlint).
• CI checked out GitHub's PR merge commit 3196d45be44087f3407f97d29f79394966e54a06, which merges this head into base 1649663e7eaed4375fa674b9489875c074486e5f.
• Local review of the new head confirmed the reviewer changes remain intact and git diff --check passed. No additional source changes were made during this review.

The earlier workflow-approval blocker is resolved, and MacM1 Nix build/smoke validation has now passed in upstream CI. The results below are retained historical local validation for 99aa7e81.

Historical local validation at 99aa7e8

• make check and make pyupgrade: passed; pyupgrade made no changes.
• make test-unit: 99 passed, including all 8 required-lemma regression cases.
• Compiled-lemma regression: passed with real compilation and Kore simplification. The same test against base commit 75bb958d fails at the expected assertion: the edited lemma still evaluates to 0 instead of 1.
• Full suite: 334 passed, 6 failed, 252 skipped (exit 1). Four minimization assertions differed only in proof-version labels after earlier tests populated the shared fixtures; the same order-dependent behavior was reproduced on base. The other two failures, Identity.applyOp(uint256) and PreconditionTest.testPrecondition(uint256), logged SMT solver timeouts.
• Fresh CSE/minimization run using CI's selection and five pytest workers: 30 passed, including all four minimization failures and Identity. The focused Precondition end-to-end rerun also passed. Across the full run and these isolated reruns, all 340 non-skipped test cases recorded a pass, including profiling. No source files or expected outputs were changed for the reruns. CSE cases check stored outputs, including partial proof graphs; their passes do not imply that every underlying proof completed.
• Wheel build, installation with --no-deps, and installed-wheel CLI smoke: passed (--help, version, build, prove, show, and list), using prepared runtime dependencies and precompiled definitions. The fresh AssertTest.test_assert_true() proof passed with no pending or failing nodes. Installed package files match the PR sources.
• Fresh Docker build from the repository Dockerfile: passed, including all 13 registered K distribution targets. The Docker Tests command sequence passed with fresh fixtures and its pinned Forge dependencies: forge build, kontrol build -O2, kontrol prove, and kontrol show; kontrol list also passed. The fresh AssertTest.test_assert_true() proof passed with 5 nodes, no pending, failing, or vacuous nodes, and admitted=false.
• Installed-package tests against that fresh Docker image: 99 unit tests and the compiled-lemma regression passed, using the newly built native definitions. The image's fresh pip resolution selected eth-abi 6.0.0, compared with 5.2.0 in the locked full-suite environment. Only isolated test tooling (pytest-mock 3.15.1) was added; runtime distribution metadata and installed Kontrol Python source bytes were unchanged. Kontrol imports were verified to come from the installed image package.
• Linux Nix package packages.x86_64-linux.kontrol.solc_0_8_13: build passed with Nix 2.31.0 and the unchanged flake lock. A fresh package/test-package.sh run, followed by kontrol show and kontrol list, passed with GNU sed on PATH and FOUNDRY_SOLC selecting the package's Solc 0.8.13. The fresh proof passed with 3 nodes, no pending, failing, or vacuous nodes, and admitted=false. Installed Kontrol package files match the PR sources.
• git diff --check: passed.

The full pytest run and isolated CSE/Precondition reruns used the official runtimeverificationinc/kontrol:ubuntu-jammy-1.0.255 image (linux/amd64, under ARM emulation) with the PR Python sources, dependency versions from uv.lock, K 7.1.337, KEVM 1.0.921, Kore RPC 0.1.155, Z3 4.13.4, Forge 1.5.1, and Solc 0.8.13. KEVM Python sources came from its exact pinned commit archive; the archive's omitted native plugin sources were restored from the same-version image. The image's Kontrol semantic source files were byte-compared with the PR sources before reusing its precompiled definitions. Those runs used PYTHONHASHSEED=0 for consistent worker collection and --force-sequential as in CI. Branch coverage was collected from the full run and the isolated CSE/minimization run. The separate fresh Docker build installed dependencies through the unmodified Dockerfile and rebuilt the native definitions.

Local Nix validation targeted x86_64-linux from an official ARM Linux Nix container with --extra-platforms x86_64-linux, using Docker's x86 emulation. The initial container smoke failed during K's version check because GNU sed was absent from PATH. After adding sed, Forge's auto-selected SVM compiler failed because its ELF loader was absent from the container; selecting the installed Nix Solc through FOUNDRY_SOLC allowed the fresh smoke to pass. No source, fixture configuration, package output, or flake lock was edited for these retries. The default native ARM Linux target cannot evaluate because the pinned Solc input does not provide solc_0_8_13 for that platform; the Nix files are unchanged from the PR base. Native macOS Nix validation remains unrun locally.

[anvacaru]

I confirmed that 6/8 unit tests fail against the master's kompile.py. A few suggestions:

• test_foundry_kompile_failed_retry[source-edit] is redundant: with a source edit, the digest mismatch forces a rekompile on retry regardless of the except cleanup, so only the internal timestamp.exists() assertion distinguishes it. The stale-copy variant is the one that actually exercises the cleanup, so I'd keep only that one.
• The "rekompiles with a fresh copy" cases (updated_lemma, stale_copy, missing_copy) share the same shape and could be one @pytest.mark.parametrize table. Same for the "does not rekompile" cases (unchanged_lemma, contract_digest_change). That also makes adding a case a one-line change.
• contract_digest_change covers behavior that already existed and is also checked by the last step of the integration test. Perhaps it could fold into the "does not recompile" group above.

[TheDarkLightX]

Thanks for the review, @anvacaru. Commit 15b21d43 addresses the requested changes:

• Replaced deprecated klabel with symbol(lemmaValue).
• Parametrized the three fresh-copy cases and the two cached cases.
• Removed the redundant source-edit failure/retry case, retaining stale-copy failure/retry and generation retry.

The post-review delta changes only the two test files. Static review found no regressions in the retained assertions, and both files passed Python syntax checks. There are now seven required-lemma unit cases.

For clarity, the detailed validation in the PR description belongs to 99aa7e81. Production code and build inputs are unchanged, so those results remain relevant historical evidence. The revised tests and K fixture were not executed in this follow-up.

Could a maintainer approve both workflows for current head 15b21d43487f4d1705c0de234aade4ca78199271?

• [Test PR](https://github.com/runtimeverification/kontrol/actions/runs/37354613316)
• [Lint Workflows](https://github.com/runtimeverification/kontrol/actions/runs/37354613522)

Both report action_required with zero jobs executed. Approval is needed for current-head CI validation.