Tooling: verify T37 stage-log coverage with omission controls

research/t37-log-coverage-seed86/CERTIFICATE.json

@@ -0,0 +1,17 @@
+{
+  "coverage_sha256": "b5fa760daf68386f0f833ddeac78089827aa131bc6fcea8788e356ba58af0249",
+  "rejected_control_names_sha256": "5366ce50d5ba4a70393bea3407241e206ef6f6d805049a38347ec4189c17f807",
+  "frozen_native_predicate_lines": [194, 196],
+  "native_omissions_accepted_by_frozen_component": [
+    "native/barch.log",
+    "native/barch-controls.log",
+    "native/layer-end-controls.log",
+    "native/native.log",
+    "native/ledgers.log",
+    "native/local-replay.log",
+    "native/wrappers.log",
+    "native/phases.log"
+  ],
+  "native_content_changes_observed_without_rejection": 8,
+  "synthetic_cold_log_count": 35
+}

research/t37-log-coverage-seed86/CLAIM.md

@@ -0,0 +1,75 @@
+# T37 execution-log coverage claim
+
+Claimed 2026-10-13 17:24 UTC. OS-random seed 86 selects verification
+engineering under the user's 85-94 mapping. Cycle began 17:17:25 UTC;
+verification and handoff start by 17:47:25 UTC; finish by 17:57:25 UTC.
+Base main: `2921874911956718fcaaaf9396fe8267b3cfa9f0`, fetched and confirmed
+fast-forwarded from CrocSwap. Prior checkout and branches are preserved.
+Branch: `research/cycle04-seed86-t37-log-coverage`.
+
+Three candidates were considered:
+
+1. Check all T37 stage logs, including the eight native logs whose existence
+   is not checked by the frozen final binder. Chosen.
+2. Audit receipt scalar types in isolation. Deferred; type checks belong to
+   the concrete stage-evidence admission boundary in the chosen scope.
+3. Reduce repeated source hashing. Rejected without a demonstrated bottleneck.
+
+Exact object: the four stage indexes and 34 logs in
+`research/community-frontier942-audit/t37-replay.tar.gz`, produced by
+Jonathan Capalbo's selected PR942 T37 construction and its pinned U8 ancestry.
+Hypothesis: a portable supplementary evidence check can reject every omitted
+log, including native omissions that the frozen native-stage predicates do
+not inspect, while accepting the unchanged archived stage evidence.
+
+Method: inspect the actual producers and final binder; bind their exact source
+bytes; verify complete ordered indexes, exact integer success codes, required
+log presence and each digest that the producer records. Demonstrate the
+native omission boundary using the unmodified source predicates, with a
+clearly stated component-level scope. Exhaust all single-log omissions and
+run changed-log, sequence, type and source-pin controls. Do not equate a
+receipt or a log with authenticated execution or a full theorem proof.
+
+Deliverable: a small standard-library checker, reproducible archive audit and
+exact control receipt, source pins, scope/credit/license documentation and
+handoff. No mathematical improvement is proposed. The optimistic effect on
+the complete selected invoice and kappa is zero. No stronger supplier or
+kappa is assumed. No selected record, source package, or upstream file changes.
+
+Coordination: immediately before this claim, checked all 753 open PR bodies
+through #1058, recent repository comments and pinned issues. No pinned issue
+or matching active claim exists, so this claim is local. Relevant existing
+work includes #865's PR799 evidence contract, #851's bridge coverage, #991's
+different T37 witness/payload controls and #1006's owner-audit bitmap speedup.
+None covers this current T37 log inventory. The review ledger and retained
+negative scopes were read; no closed mathematical search is reopened.
+
+Stopping rule: finish the declared archive and control census; if useful
+evidence or relevant checks fail, preserve the patch and an honest handoff.
+At most one focused PR; refresh metadata and overlap before submission.
+
+Prepared for Sagar Thakrar with substantial OpenAI Codex assistance.
+New files are Apache-2.0; predecessor notices and source licenses remain.
+
+## Completed result, 2026-10-13 17:42 UTC
+
+Published one focused PR: https://github.com/CrocSwap/integer-mult-bounds/pull/1073
+and attached it to the originating chat. The archive passes at 34 logs,
+26 producer-recorded digests and eight native presence-only logs. All 80
+declared negative controls reject. The original native-stage source slice
+admits all eight native-log omissions; native content changes deliberately
+remain accepted by the supplementary checker while changing its observation.
+This is scoped evidence-coverage work, not a mathematical counterexample.
+
+Both tested Python runtimes, optimized workers, relocated minimal closure,
+public CLI controls, 25 selected-record tests, three replay-coverage tests and
+the selected-record check pass. Full receipt SHA-256 is
+`e834d7037dee9071f14b0c0a3194c84c8f036d1160ca512f84d2a578992170c0`.
+Final overlap checked 739 open PRs through #1072 and recent comments.
+Refreshed upstream `abdc6a7002abdbcd9e21bfc5e1a795784deacfdf` retains all
+12 consumed/context pins. No pinned sprint issue exists, and neither requested
+Codex label is available. This is the claim's single result update.
+
+No full supplier or invoice replay, full make verify, Linux CI result or new
+kappa is asserted. Selected sources, prior branches and upstream are unchanged.
+Verification and handoff began by 17:30 UTC, before the reserved final interval.

research/t37-log-coverage-seed86/README.md

@@ -0,0 +1,143 @@
+# T37 execution-log coverage
+
+The selected T37 archive contains 34 stage logs. The frozen native-stage
+admission predicates read `native/STEPS.json`, check its eight stage names and
+compare each exit code with zero. They do not inspect the eight native logs.
+This package supplies a supplementary, read-only coverage check for the four
+execution indexes and every corresponding log. It changes no selected files.
+
+The exact result is limited to evidence admission. The replay below executes
+the original three source statements at `final_binding.py:194-196`, with no
+rewrites, against the archived native index. Each of the eight native-log
+deletions leaves those predicates passing. The new check rejects all eight.
+This is a component-level counterexample to log completeness. The complete
+original final binder is not executed by this package, and no counterexample
+to the mathematical construction is claimed.
+
+## Reproduce
+
+From the repository root, with Python 3.11 or newer and no third-party packages:
+
+```sh
+rtk proxy python3.11 -I -B research/t37-log-coverage-seed86/verify.py
+```
+
+Expected output:
+
+```text
+PASS_T37_LOG_COVERAGE_CONTROLS 34 logs; 80 rejections; 8 native omissions admitted by frozen slice
+```
+
+The verifier checks five immutable source/archive SHA-256 pins, derives the
+stage order from the three actual producer programs, copies only the indexes
+and logs into a temporary directory, and runs the complete declared controls.
+It compares the canonical coverage and ordered control-name digests with
+`CERTIFICATE.json`. Canonical JSON uses sorted keys and separators `,` and `:`.
+The temporary directory is removed. The committed archive stays unchanged.
+The source pins apply to immutable inputs, not to regenerated gzip containers.
+
+Append `--out /new/path/receipt.json` to write the full report, including every
+log digest and control name. Its parent must exist. Output is created only
+after success, with exclusive creation; existing files are not overwritten.
+Both ordinary and optimized Python execute all new checks. The original
+native predicates are explicitly compiled with assertions enabled.
+
+The public CLI controls exercise source drift, safe output handling, missing
+logs, an escaping symlink, a minimal relocated checkout with spaces, and full
+receipt equality between ordinary and optimized workers:
+
+```sh
+rtk proxy python3.11 -I -B research/t37-log-coverage-seed86/test_cli.py
+```
+
+Expected: `PASS_T37_LOG_CLI_CONTROLS` with receipt SHA-256
+`e834d7037dee9071f14b0c0a3194c84c8f036d1160ca512f84d2a578992170c0`.
+The test driver uses assertions and rejects optimized execution itself.
+
+For a completed T37 replay directory:
+
+```sh
+rtk proxy python3.11 -I -B research/t37-log-coverage-seed86/audit.py --work /path/to/t37/replay
+```
+
+For the archived reuse mode, the success line is:
+
+```text
+PASS_T37_STAGE_LOG_COVERAGE 34 logs; 26 producer digests; 8 presence-only
+```
+
+The actual producer also supports a cold-baseline mode. That mode requires its
+additional first stage and log, giving 35 logs and 27 producer digest checks.
+The control suite exercises that branch with a synthetic log, explicitly not
+with a cold supplier execution. `audit.py` checks the fixed T37 log contract;
+it does not establish source identity, inspect the rest of the replay, or
+substitute for `make frontier942-verify`.
+
+## Coverage and limits
+
+| Layer | Logs | Producer-recorded digests checked |
+|---|---:|---:|
+| Top-level T37, reused baseline | 13 | 13 |
+| Native U8 | 8 | 0 |
+| Discovery | 6 | 6 |
+| Strict replay | 7 | 7 |
+| Total | 34 | 26 |
+
+All four ordered indexes must be complete and have integer zero exit codes.
+Every expected log must be a regular file contained in the replay directory.
+An empty log is valid; the actual `build-parent.log` is empty. There is no
+heuristic success-text check.
+
+The 80 negative controls cover every single-log omission, every changed log
+with a producer-recorded digest, and five mutations of each index: omission
+of its final stage, reversal, failure status 1, boolean false and floating zero.
+The verifier restores and rechecks the original evidence after the mutations.
+All 34 archived logs must be accounted for. This finite census is complete for
+that declared class; arbitrary multi-file changes are outside the census.
+
+The eight native logs have no producer-recorded digests. The checker records
+their current hashes but does not claim to validate those bytes against an
+earlier commitment. Eight native-content changes deliberately remain accepted
+while changing the observed hashes. This positive limitation control prevents
+claiming stronger coverage than the format supplies. A forged self-consistent
+receipt is not authenticated execution. Archive integrity, receipt consistency,
+fresh execution and mathematical proof are separate claims.
+
+No new kappa, supplier improvement, cost reduction, or broad search result is
+proposed. The selected conditional value remains
+`1661960547713947/1000000000000000000`. The optimistic change to the complete
+selected cost invoice is zero. The all-size/compiler, realization, hosting,
+precision/tape, analytic and bit-interface assumptions remain. No full
+supplier replay, invoice recomputation, Lean proof or Linux CI is claimed here.
+
+## Sources and credit
+
+The base is `2921874911956718fcaaaf9396fe8267b3cfa9f0`. The reviewed source
+head is `1960cfa919a0945d0ca4cb14ea96237000037903`, PR942, integrated in
+`3825dc0ea1317629864ebeb6929719cc4bbf525f`. `SOURCES.json` distinguishes the
+five consumed inputs from historical context pins. Context pins describe the
+base commit only; a later change to the moving selected pointer does not
+invalidate this fixed archive audit.
+
+Jonathan Capalbo supplied the T37 construction, producers and final binder.
+Chafik Boukhalfa supplied the T21 construction, and Hao Yan supplied the T16
+and independent owner-audit lineage. The native producer is retained through
+the PR869/870 U8 work and Jeremy Kothe's PR799 X4 ancestry. Its notices retain
+NewBArch, ColdWitness/icekylinx and the earlier factory, gauge and controller
+credits. Douglas Colkitt supplied the maintainer coverage wrapper and archived
+review. Lucas, @ljste, supplied the preceding ancestor audit. Stephen Shore,
+@nightangelflowerwin-ops, supplied PR865's source-versioned coverage work, and
+Adem Vessell supplied PR851's bridge controls. Their packages and notices
+remain unchanged.
+
+This scope extends the evidence-coverage idea from #865 to the current T37 log
+inventory. It does not repeat #991's alternate owner schedule and payload
+controls, #1006's bitmap owner audit, or the T37 arithmetic audits #1051/#1052.
+The local `CLAIM.md` records the random assignment, coordination scan, rejected
+candidates and fixed stopping rule.
+
+Prepared for Sagar Thakrar with substantial OpenAI Codex assistance in design,
+implementation, analysis and documentation. No independent human review is
+claimed. New files are Apache-2.0 under the repository root license. The source
+predicate slice is executed from the pinned original file; predecessor
+copyright, license and AI-assistance notices remain in force.

research/t37-log-coverage-seed86/SOURCES.json

@@ -0,0 +1,23 @@
+{
+  "base_commit": "2921874911956718fcaaaf9396fe8267b3cfa9f0",
+  "selected_kappa": "1661960547713947/1000000000000000000",
+  "selected_source_head": "1960cfa919a0945d0ca4cb14ea96237000037903",
+  "integration_commit": "3825dc0ea1317629864ebeb6929719cc4bbf525f",
+  "runtime": "Python 3.11 or newer, standard library only",
+  "consumed_sha256": {
+    "research/community-frontier942-audit/t37-replay.tar.gz": "48285025105210b56a32d3d4d57a21b7591760acc709d38073e4dca339eb06fe",
+    "research/complex-t37-owners/verify.py": "4d880a6237c2f5d4f4e08374e2a4ddbe7bdcc972fe4ee0e879e9a547754f5fd0",
+    "research/complex-t37-owners/replay.py": "7834f469861df4a8ed82550762e7d1640123f547a715b55a937dea0cb381cedd",
+    "research/complex-t37-owners/final_binding.py": "61e8a8856ebc36feee11cbf6e60f2ace3b9b89195c3282f565a651488cf947f7",
+    "research/complex-t21-owners/vendor/pr870/construction/barch/reproduce_barch.py": "19bc970aa6af25ab0e7fa96fb65c64dd0c5243976d8f2cb733cba839155482c1"
+  },
+  "context_sha256_at_base_only": {
+    "certificates/selected-result.json": "1d35283cb0ce3f8db1f285683933517f9e87475d295e2b6316399ad9928c81c3",
+    "research/complex-t37-owners/DEPENDENCY-PINS.json": "0160ea2677cc9ceeb0f861dc2774d470a27cbaa58b8fd6c064cf0683d18f3e87",
+    "research/complex-t37-owners/MANIFEST.json": "38907d05fddac9be6bf7a7aff47fae43114a055d2259cead5651a08f9b983820",
+    "research/complex-t37-owners/NOTICE.md": "78887899d460a21fc6bf6e6021fea7f6864a93e079b639e7c92d4dc77ca30c1e",
+    "scripts/verify_frontier942.py": "27c6713532d9f53f55dfff4884d55a2d9ae74b68156e37a44596c0418fbed5b7",
+    "docs/research/community-batch952-review.md": "04db59dfc2c31453229b6061bbf59547e71ce3abdc0ce0f6779144bb0dde127b",
+    "LICENSE": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4"
+  }
+}

research/t37-log-coverage-seed86/VALIDATION.json

@@ -0,0 +1,53 @@
+{
+  "verified_at_utc": "2026-10-13T17:36:15Z",
+  "base_commit": "2921874911956718fcaaaf9396fe8267b3cfa9f0",
+  "pre_submission_upstream": "abdc6a7002abdbcd9e21bfc5e1a795784deacfdf",
+  "pre_submission_consumed_and_context_pins": "All 12 remain byte-identical on refreshed main",
+  "pre_submission_overlap": "739 open PR bodies checked through #1072 at 17:41 UTC, plus recent coordination comments; no matching T37 log-coverage scope. Neither codex nor codex-automation label exists.",
+  "platform": "macOS 26.5.2 arm64",
+  "runtimes": [
+    "CPython 3.11.15, Clang 22.1.3",
+    "CPython 3.14.8, Clang 21.0.0 clang-2100.1.1.101"
+  ],
+  "dependencies": "Python standard library only",
+  "implementation_sha256": {
+    "audit.py": "629cb5535e470596e4e69b706179bc83c0b099226cd97788bcecee33feb3db9e",
+    "verify.py": "9f072f56a9744a0dc488c46432adddeccf6c66aadb796fbacaa0548805c36eb4",
+    "test_cli.py": "f32762774369d983c341e1c6d0371db4431d0f471cef092fb28ae85ba73a3c9a",
+    "SOURCES.json": "ea2909baee224375a67908a7de861518c0d18f5c5e0f01731557380e4aec2485",
+    "CERTIFICATE.json": "e53a9cb25e44b5f01f620375f53a0c00f2dc567e907532d2e0808fd9140420c2"
+  },
+  "commands": [
+    "rtk proxy python3.11 -I -B research/t37-log-coverage-seed86/verify.py",
+    "rtk proxy python3 -I -B -O research/t37-log-coverage-seed86/verify.py",
+    "rtk proxy python3.11 -I -B research/t37-log-coverage-seed86/test_cli.py",
+    "rtk proxy python3 -I -B research/t37-log-coverage-seed86/test_cli.py",
+    "rtk proxy python3.11 -I -B -m unittest discover -s tests -p 'test_selected*.py'",
+    "rtk proxy python3.11 -I -B -m unittest discover -s tests -p 'test_replay_coverage.py'",
+    "rtk proxy python3.11 -I -B scripts/verify_selected_result.py"
+  ],
+  "results": {
+    "archive_log_count": 34,
+    "producer_digest_checks": 26,
+    "native_presence_only_logs": 8,
+    "negative_controls_rejected": 80,
+    "native_omissions_accepted_by_original_source_component": 8,
+    "native_content_mutations_accepted_but_digest_changed": 8,
+    "full_receipt_sha256": "e834d7037dee9071f14b0c0a3194c84c8f036d1160ca512f84d2a578992170c0",
+    "receipt_identical_across_runtimes_optimized_and_relocated": true,
+    "cli_source_pin_output_safety_missing_log_symlink_controls": "PASS",
+    "existing_selected_tests_passed": 25,
+    "existing_replay_coverage_tests_passed": 3,
+    "selected_record_check": "PASS",
+    "context_pins_at_recorded_base": "PASS"
+  },
+  "initial_failure_and_resolution": "The first archive projection rejected the macOS /var temporary path because it resolves through /private/var. Resolving the temporary root before containment comparison fixed the checker itself. Both runtime replays then passed without altering source evidence.",
+  "not_executed": [
+    "complete original T37 final binder",
+    "native supplier reconstruction or cold ancestry replay",
+    "full invoices, exact moments or outer assembly",
+    "full make verify",
+    "Linux CI or formal multiplication proof"
+  ],
+  "scope": "Supplementary stage/log evidence admission. No execution authentication, mathematical counterexample, supplier cost improvement or new kappa. Selected sources and upstream remain unchanged. Substantial OpenAI Codex assistance; Apache-2.0."
+}