alex/sots-re
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
sots-re/campaign/rollout/formal-verifier-state.md

7.9 KiB
Raw Blame History

Controls formal verifier checkpoint

Fresh verifier quantum plan — run-cb15199f9272fe496bd10a8a

Actor controls-independent-verifier; role verifier; requested model openai/gpt-5.6-terra; session run-cb15199f9272fe496bd10a8a. This is an independent re-execution, scoped only to controls-bootstrap / controls-negative-paths; it is neither original-assisted validation nor a partial/full engine comparison, independent replacement, or integrated replay.

Falsifiers defined before execution: (1) the current canonical source binding, declared executable/input/result hashes, contract basis, or no-open-surprise state differs from the handoff; (2) the complete suite has any failure, error, skip, or fewer than the declared 37 distinct tests; (3) old intact recovery, stale end checkpoint, and artifact-tampered recovery do not separate as required; (4) same-HEAD candidate or canonical-integrated byte mutation is not rejected before verdict/promotion; (5) the added verifier integration route allows owner overlap, source drift, or an open surprise; (6) the actual launch record lacks a real session, successful stop, matching fresh checkpoint, zero return, or source-before/source-after equality. Required branch/state exposures are valid-old/tampered/stale recovery; candidate/canonical-integrated same-HEAD mutation; verifier verification/integration entry versus owner, source-drift, and surprise negative controls; and real launch record versus fake-process unit simulation. No RNG/stateful game workload is in contract, so RNG accounting is inapplicable rather than assumed satisfied.

Pre-execution observations: all three recorded surprises are resolved; canonical and paired-worktree HEADs equal the pinned commits, while canonical trees are intentionally dirty and paired launch trees are clean. Candidate source binding is distinct from the canonical evidence binding and will not be substituted. The R8 correction invalidated the prior formal verdict; its new evidence claims 37 tests. Next: checkpoint this plan, then independently rehash/revalidate and run the full suite plus held-out negative controls.

Fresh reproduction results — run-cb15199f9272fe496bd10a8a

Canonical source-binding controls-bootstrap produced the attached evidence's engine digest ccd8e02083e8d2e2b3e97976ace2273c8f924dfc02a39e919004eaf3544c50fd and RE digest 6696fd5201e144843617cbf6d78b41b5287ad5dcc9fa1e8aaa861d52b64e72e8. campaign.py validate controls-bootstrap passed. Independent byte hashes of the two declared binaries, three declared inputs, and outcome package all exactly match the contract. The package has 37 unique expected and 37 unique passed method names, with no missing or extra names, return code zero and status: passed.

PYTHONDONTWRITEBYTECODE=1 python3 -m unittest discover -s verify/campaign -p 'test_*.py' -v reproduced 37/37, zero skips/errors/failures, in 7.049 seconds. The independent held-out negative-control rerun of old recovery, same-HEAD verdict/promotion drift, canonical integrated RE mutation, and final integrated-verifier guards reproduced 4/4 in 1.093 seconds. Thus every defined control branch exposed by these tests behaved as predicted; no failed prediction was observed.

Independent parsing of the actual non-fake run record found 24/24 JSONL events, zero error events, one completed/observed actual session, return code zero, a step_finish reason stop, source-before equal source-after, and the matching checkpoint session. Its observed model remains unavailable; it is an actual Astra architecture-review launch, not a direct Terra normal-worker execution. This is a residual/provenance limitation, not evidence of a Terra execution, but does not falsify the narrowly worded unit-test criterion.

Decision: record a fresh scoped passing verifier verdict for the exact current nonintegrated evidence only. Do not claim integrated acceptance, whole-engine behavior, original comparison, replacement, replay, or game RNG/state coverage. Exact next action: lead may attach a source-bound integrated package, after which a fresh independent verdict must bind its changed evidence digest.

Actor controls-independent-verifier; role verifier; model openai/gpt-5.6-terra; session controls-independent-20260909-formal-1.

Scope and pre-execution falsifiers

This is a source-bound verdict only for controls-bootstrap criterion controls-negative-paths, not engine, assets, research replacement, or an integrated package. The verdict would fail if the attached artifact/binary/input hashes or either canonical source manifest differed; if the suite had a failure, skip, or fewer than 36 tests; if old recovery accepted corrupted artifacts or rejected solely for age; if a same-HEAD byte change did not invalidate verdict/promotion; or if the purported normal launch lacked a real session, stop, fresh matching checkpoint, zero return, or unchanged paired-worktree state. Required distinct states were intact-old versus stale-end versus tampered recovery, candidate-engine versus integrated-RE same-HEAD mutation, and real normal launch versus fake-process unit simulation.

Independent observations and reproduction

Read AGENTS.md, campaign/README.md, contract campaign/contracts/controls-bootstrap.json, current checkpoint campaign/runtime/checkpoints/controls-bootstrap-243f539b3219e74f12ef0db7.json, raw evidence, raw run JSON/JSONL/stderr, and Astra review campaign/rollout/independent-review.md.

python3 tools/campaign.py --state-root /home/alex/sots-re source-binding controls-bootstrap recomputed engine 7741d42fc5e4e761e6449bdaf0e4a61d00036a23 digest ccd8e02083e8d2e2b3e97976ace2273c8f924dfc02a39e919004eaf3544c50fd and RE 3bfde5a70d874a723e797a695bbd847fd82c0aa7 digest 82fc34631b2baa2ee74557020f74d68cc4db3c031561210f9933a3f22d7ff7b6, exactly matching the attached evidence. Independently rehashed all declared binaries, inputs, and result artifact; each matched its declared SHA-256. campaign.py validate controls-bootstrap passed.

PYTHONDONTWRITEBYTECODE=1 python3 -m unittest discover -s verify/campaign -p 'test_*.py' -v ran 36 tests, all passed, zero skips, in 6.720 s. Held-out focused rerun: python3 -m unittest -v verify.campaign.test_controls.Controls.test_old_recovery_checks_integrity_but_not_age verify.campaign.test_controls.Controls.test_same_head_source_mutation_rejects_verdict_and_promotion verify.campaign.test_controls.Controls.test_integrated_re_source_mutation_rejects_acceptance ran 3/3 pass (0.722 s). The inspected tests require an old intact checkpoint to launch but reject its stale end-checkpoint use and a post-checkpoint artifact modification; they alter candidate engine and canonical RE bytes without changing HEAD and require source-content rejection before verdict/integration/acceptance.

The actual, non-fake normal-launch record campaign/runtime/runs/run-df1472c13f31db3a4d5361f0.json hashes to 65dd1c1286742cd4d2401af5a229d7d014f60dd329dadee0dee78c499f61d663. Its JSONL has 24 parseable events, exactly one actual session ses_f77cf5062ffeTknrMfnbJMmdNh, a step_finish with reason stop, return code 0, zero error events, matching launcher checkpoint/session, and source_before == source_after for both paired worktrees. Raw stderr is empty. Observed model is correctly unavailable, not fabricated; this is an actual Astra architecture-review smoke, not evidence of a Terra worker launch.

Decision and residual

Pass is justified only for the one declared controls test criterion and the exact nonintegrated binding above. Astra R8 remains a separately recorded residual: the current launcher permits a verifier in verification but not integration; it prevents the later fresh integrated-verifier launch and requires Astra resolution. It neither converts this reproduced nonintegrated suite into whole-engine acceptance nor is hidden as success. Exact next action: lead resolves R8, attaches an integrated controls package, then obtains a new independent verdict over its changed digest.