Behavior-preserving refactor claims

Behavior-preserving refactors are Exhibit A’s second claim type. The first deterministic unit compares a trusted behavioral contract executed repeatedly before and after a refactor. It does not call a model and does not reuse or weaken the bug-reproduction flip_check.

The judge compares contract outcomes rather than pytest’s raw stdout, which contains paths, timing, and other non-behavioral noise. Application outputs belong in explicit contract assertions. Its default is three runs per state, and callers cannot lower the requirement below two because one execution cannot establish determinism.

Observation Verdict Execution truth Goal truth
Contract passes deterministically in both states VERIFIED COMPLETED VERIFIED
Stable outcome or failure signature changes between states FAILED COMPLETED FAILED
The same complete, parseable failure fingerprint occurs in both states PARTIAL COMPLETED PARTIAL
Missing reruns, flakiness, or inconsistent failures UNCERTAIN NOT_RUN or COMPLETED UNCERTAIN
Timeout, import, collection, syntax, or harness failure UNCERTAIN FAILED UNCERTAIN

FAILED therefore has a narrow, evidence-backed meaning: the preservation goal was deterministically disproved. A broken environment is never FAILED; it is UNCERTAIN. Opaque failures that cannot be fingerprinted are also UNCERTAIN, never assumed equal. For the initial pytest contract runner, only exit code 1 is a behavioral test failure; internal, usage, collection, timeout, signal, and no-tests outcomes are infrastructure. Release truth remains NOT_ASSESSED for every result because passing a selected contract does not establish that a refactor is safe to ship.

The fixed-shape runner injects only test_refactor_contract.py, invokes only that test, disables network requests in its execution specification, and prepares each code state once before the repeated runs. DockerExecutor supplies the production containment boundary; LocalExecutor is intentionally limited to trusted fixtures and development because it inherits host network and credentials. The counterexample fixture is excluded from the innocent-pair self-audit manifest and exists only to prove that observable changes produce FAILED.

behavior-refactor-evidence/v2 is the machine-readable result shape. It links every raw base and target run to one validated connector evidence ID, includes the deterministic truth assessment, binds every receipt to the same contract artifact, and retains the bounded local image handle needed to recompute each request digest. A single invalid receipt aborts collection before a verdict is returned.

EEF v2 can archive this evidence with both source states. Offline integrity verification checks the signature, tree digests, exact run-to-receipt linkage, and independently re-derives the recorded truth. Executable verification then rebuilds and repeats both archived states and compares the complete fresh result with the recorded one. A stable FAILED result can therefore be successfully replay-verified: replay truth means “the record is reproducible,” not “the refactor passed.” exhibit-a passport can now project this machine evidence into a credential-free public JSON passport; source snapshots, raw execution logs, and opaque executor metadata remain only in the private EEF because they may contain sensitive data.

The CLI collector uses the same resource-bounded, network-disabled Docker harness as EEF replay rather than the host-local development runner:

python3 -m exhibit_a.cli refactor-bundle \
  --base-source /path/to/before --target-source /path/to/after \
  --contract /path/to/test_contract.py \
  --signing-key /secure/eef.key --out refactor.eef

The command rejects identical source paths, keys or outputs inside a source tree, and any key aliased to the contract or output. It then materializes each checkout once through EEF’s no-symlink, race-safe source reader and uses those exact snapshots for every execution and for the archive. Collection and replay share the byte-exact Dockerfile, fixed pytest argv, offline build, 64 KiB per-stream output cap, and CPU/memory/PID/time limits. Contracts are capped at 1 MiB so the complete repeated evidence remains one valid EEF entry. The contract file is injected at the fixed test_refactor_contract.py path in both states; it is not copied from either checkout. The command closes the executor on success or failure.