Skip to content

feat(testing): bake order-sensitive determinism check into fill - #906

Merged
tcoratger merged 1 commit into
leanEthereum:mainfrom
tcoratger:feat/bake-determinism-check-into-fill
Jun 10, 2026
Merged

feat(testing): bake order-sensitive determinism check into fill#906
tcoratger merged 1 commit into
leanEthereum:mainfrom
tcoratger:feat/bake-determinism-check-into-fill

Conversation

@tcoratger

Copy link
Copy Markdown
Collaborator

Motivation

The order_sensitive marker docstring claimed "the determinism check generates this vector twice and diffs the output", but no such logic existed in the pytest plugin — it only registered the marker. The only real gate lived in the fill-determinism justfile recipe, invoked once by CI.

Consequences:

  • A plain uv run fill never verified determinism.
  • The guarantee fired only after push, on CI, on a machine the contributor isn't watching — the wrong feedback loop for a property that's produced locally.
  • The marker docstring was misleading (described an in-process gate that didn't exist).

The hazard being guarded: Python randomizes str/bytes hashing per process (PYTHONHASHSEED), so set/dict-iteration order varies run-to-run. A vector whose emitted bytes depend on that order is not reproducible across clients.

What this does

Bake the two-seed check into fill. After a successful fill, the command regenerates the order_sensitive subset under PYTHONHASHSEED=1 and =2 into throwaway directories and byte-diffs them. A difference fails the command and lists the offending fixtures.

  • Independent of the parent process's seed — runs two fresh seeds and compares them (a true hash-seed check fundamentally needs ≥2 processes, since PYTHONHASHSEED is frozen per interpreter).
  • Forces the mocked prover so proof bytes stay deterministic; single process pins each seed cleanly.
  • --no-check-determinism opts out for fast local iteration.
  • Exit-code 5 (no marked test selected) is handled as a clean skip.
  • Real fixtures are never touched (temp dirs only).

Drop the redundant CI step. just fill-ci runs fill, which now performs the identical subset check by default.

Repurpose the fill-determinism recipe as the standalone, wide-scope audit the baked-in check cannot provide: it runs without a full fill and can cover the whole tree (just fill-determinism tests/consensus) to catch a filler that should be marked order_sensitive but isn't — the safety net for the opt-in marker model's blind spot. Its fill calls now pass --no-check-determinism so the recipe (which is the check) doesn't nest the per-fill gate.

Net result

Baked-in fill check just fill-determinism
Runs automatically every fill manual
Scope marked subset arbitrary, incl. whole tree
Needs a full fill part of it standalone
Purpose per-commit gate audit for unmarked nondeterministic fillers

The determinism gate no longer depends on CI. No emitted vectors change; the existing emission paths were already deterministic by construction (the coverage picker tie-breaks by encoded bytes; the builders use insertion-ordered dict/list).

Testing

  • just check passes (lint, format, ty, codespell, mdformat).
  • Smoke: uv run fill ... -m order_sensitive runs the main fill plus two seeded re-runs, all byte-identical; the check reports pass.
  • Verified --no-check-determinism skips the check and the repurposed recipe runs exactly two fill invocations (no nesting).
  • Verified the tree comparator flags both differing content and missing files, and returns empty for identical trees.

🤖 Generated with Claude Code

The order_sensitive marker docstring claimed the determinism check
"generates this vector twice and diffs the output", but no such logic
existed in the plugin.
The only real gate lived in a justfile recipe invoked by CI, so a plain
`uv run fill` never verified determinism and contributors relied on CI.

Bake the two-seed check into the fill command itself.
After a successful fill, regenerate the order_sensitive subset under
PYTHONHASHSEED=1 and =2 in throwaway directories and byte-diff them.
The mocked prover is forced so proof bytes stay deterministic, and a
single process pins each seed cleanly.
A difference fails the command and lists the offending fixtures.
Add --no-check-determinism to opt out for fast local iteration.

Drop the now-redundant CI step: `just fill-ci` runs fill, which performs
the identical subset check by default.

Repurpose the fill-determinism recipe as the standalone, wide-scope audit
the baked-in check cannot give: it runs without a full fill and can cover
the whole tree to catch a filler that should be marked but is not.
Pass --no-check-determinism in the recipe so its own fill calls do not
nest the per-fill gate.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
@tcoratger
tcoratger merged commit fe89d8e into leanEthereum:main Jun 10, 2026
13 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant