From bdeda4e8c71d947bbda0c339b19a66f765dedbe0 Mon Sep 17 00:00:00 2001 From: Aaron Wang Date: Tue, 13 Oct 2026 18:24:55 -0400 Subject: [PATCH 1/2] Research audit: X2 acceptance boundary for the selected CrocSwap/integer-mult-bounds#1094 owner map (no new kappa) One named selected supplier obligation (X2, pending-axis disjointness across idle children of one physical family) traced through every checker on the reproduce path. X2 is enforced only by the review-time composition research/community-batch1099-audit/check_frontier1094.py; make frontier1094-verify and the community-batch1099 CI job do not re-run it for the selected supplier. A one-integer DATA-PHASES mutation preserves every role-level aggregate, is accepted by the complete R1-R7/X1 rule set, and is rejected only at X2; first X2-directed rejection controls included. Contributed by Navinor with help from opencode. X2 rule and owner audit by Josie Elliston (CrocSwap/integer-mult-bounds#1091), owner map by Rohan Arun (CrocSwap/integer-mult-bounds#1094), frozen verifier chain from Hao Yan's CrocSwap/integer-mult-bounds#858 lineage, batch1099 composition by Douglas Colkitt. --- .../owner-x2-acceptance-boundary/README.md | 182 +++++++++ .../owner-x2-acceptance-boundary/RESULT.json | 145 ++++++++ .../owner-x2-acceptance-boundary/SOURCES.json | 24 ++ .../owner-x2-acceptance-boundary/TASK.json | 72 ++++ .../owner-x2-acceptance-boundary/VERIFY.json | 20 + .../owner-x2-acceptance-boundary/verify.py | 348 ++++++++++++++++++ 6 files changed, 791 insertions(+) create mode 100644 research/owner-x2-acceptance-boundary/README.md create mode 100644 research/owner-x2-acceptance-boundary/RESULT.json create mode 100644 research/owner-x2-acceptance-boundary/SOURCES.json create mode 100644 research/owner-x2-acceptance-boundary/TASK.json create mode 100644 research/owner-x2-acceptance-boundary/VERIFY.json create mode 100644 research/owner-x2-acceptance-boundary/verify.py diff --git a/research/owner-x2-acceptance-boundary/README.md b/research/owner-x2-acceptance-boundary/README.md new file mode 100644 index 0000000000..1243092d56 --- /dev/null +++ b/research/owner-x2-acceptance-boundary/README.md @@ -0,0 +1,182 @@ +# X2 acceptance boundary for the selected CrocSwap/integer-mult-bounds#1094 owner map + +**Adversarial audit of one selected supplier obligation; no new κ.** Navinor, +with help from opencode. Apache-2.0. + +This package answers one question from the `supplier-boundary-audit` card +(adversarial-audit track, task catalogue revision 2): does one selected +supplier obligation follow from its actual source-bound checks? + +**Object.** The frozen owner map of the selected complex supplier: CrocSwap/integer-mult-bounds#1094's +`data/OWNERS.json.gz` / `PLAN.json` / `SPEC.json` in +`research/complex-t16-rare-pattern-exchanges/`, at audited head +`0fc329d0bec93ca7cd288eaea1295172e8789810` (recorded in +`certificates/selected-result.json`, κ = 836330098538459/500000000000000000). + +**Obligation (named X2).** Pending axes of distinct idle children of one +physical family are disjoint, so a family's hosts on different children never +share a cell. X2 is stated and checked in Josie Elliston's independent owner +audit (`research/t16-owner-audit-seed67/verify.py`, `geometry()`). + +**Answer.** No. X2's acceptance does not follow from the selected record's +reproduce command. It depends on the review-time maintainer composition +`research/community-batch1099-audit/check_frontier1094.py`, which is pinned in +the record's `proof_supplements` but is executed neither by +`make frontier1094-verify` nor by the `community-batch1099.yml` CI job. Every +checker that the reproduce path does execute is structurally blind to X2. + +## Task card + +```text +Task ID / proposed scope key: supplier-boundary-audit / dcdb0fa8e49b08a958d0 + (refined to the selected CrocSwap/integer-mult-bounds#1094 owner map, obligation X2) +Base commit; exact predecessor and dependency heads: + bce54fb3f895cbe5cd4c0eb477c3afeed100190f; audited source head + 0fc329d0bec93ca7cd288eaea1295172e8789810 (CrocSwap/integer-mult-bounds#1094); owner audit CrocSwap/integer-mult-bounds#1091 + as composed by research/community-batch1099-audit/check_frontier1094.py + (sha256 2608ef213260a43d09a40b3429742f7a5f280861b54acae66400a7c29a123f51) +Concrete object and question: + one named condition, X2, of the selected supplier's hosting soundness: + does its acceptance follow from the actual source-bound checks? +Scope status: unchanged (one named current condition audited with a new + semantic counterexample, as the card allows) +Existing restriction being changed (or exact claim being audited): + audited claim: the selected composition's owner/hosting acceptance +Method; explicit parameter ranges/candidate alphabet: + enforcement trace of every checker on the reproduce path; then one exact + one-integer mutation of the pinned DATA-PHASES pending axes (children 0 and + 1 at port 0) with rejection testing and a colliding-cell witness +Nearest overlapping PRs and why this adds something: + CrocSwap/integer-mult-bounds#1277 (the reuse replay discards its ancestry + recheck) — same replay-coverage class, different obligation; this package + covers owner-rule X2 and supplies the missing rejection controls. + CrocSwap/integer-mult-bounds#1209 audits pending-axis independence of the + selected data semantically; this package tests which checkers reject a + corrupted fixture at all. Josie Elliston's CrocSwap/integer-mult-bounds#1091 + owns the X2 rule and the 11-control battery; this package adds the first + X2-directed mutants and the acceptance trace for CrocSwap/integer-mult-bounds#1094. +Optimistic full cost budget; required observable improvement: + stdlib-only replay of the pinned audit on pinned inputs; no construction +Success evidence; falsification test; time/compute cap: + RESULT.json from one command; falsified if geometry() accepts M1 or if any + executed checker on the reproduce path rejects M1; minutes on one core +Predecessor authors; intended artifact and reproduction command: + Josie Elliston (X2 rule, owner audit), Rohan Arun (CrocSwap/integer-mult-bounds#1094 owner map), + Jeremy Kothe (T16 owner-map lineage), Hao Yan (CrocSwap/integer-mult-bounds#858 controller/indep16), + Sagar Thakrar (independent pricing), Douglas Colkitt (batch1099 + composition); artifact research/owner-x2-acceptance-boundary/; + python3 -B research/owner-x2-acceptance-boundary/verify.py +``` + +## What the trace shows + +| Path | Executes the CrocSwap/integer-mult-bounds#1094 owner composition (`check_frontier1094.py`) | Sees X2 | +| --- | --- | --- | +| `make frontier1094-verify` (the record's `reproduce`) | no — stages: `historical-source`, `baseline1042-cold` (or reuse), `rare-pattern-exchanges` | no | +| `scripts/verify_selected_result.py` (CI + target dependency) | no — validates the record and `proof_supplements` hashes; imports no subprocess module | hashes only | +| `.github/workflows/community-batch1099.yml` | no — runs `research/t16-owner-audit-seed67/verify.py --fetch` and `check_pr1048_counterexample.py` | yes, but only for its pinned claim list (CrocSwap/integer-mult-bounds#1022 through CrocSwap/integer-mult-bounds#1087), which excludes the selected supplier | +| frozen `upstream1087.tar.gz` chain (`verify_t16.py` → `lift16`/`audit_allcold`/`indep16`) | n/a | no — `indep16.py` keys cells per `(owner, child, port)`; `audit_allcold.py` asserts only `len(pending) == rank` per child | +| `research/community-batch1099-audit/check_frontier1094.py` (batch1099 review time) | — | **yes**, via `geometry()`; its result is pinned evidence in `docs/research/community-batch1099-integration.json` | + +So the obligation is real and currently checked exactly once, at review time, +by a composition that neither the reproduce command nor CI re-runs for CrocSwap/integer-mult-bounds#1094. +The construction-time receipts in `hosting/expand_owners.py` and +`hosting/reuse_owners.py` record `all_footprints_disjoint_compacted_prefixes: +True` as a flag; the flag is not independently enforced on the reproduce path. + +## Minimal adversarial instance + +One integer in the pinned `DATA-PHASES.json` pending axes: child 1's +`orthogonal_axes[0]` at port 0, value 131072, replaced by 13, which is already +pending for child 0. Children 0 and 1 are distinct idle children of the same +physical family place (pair 1, side 0). This preserves every rank, window, +role count, width and profile aggregate (exactly one differing integer), and: + +- `geometry()` rejects it: `X2: children [0, 1, 14] share axes at port 0`. +- With only the X2 `need()` suppressed, `geometry()` returns a byte-identical + geometry object and the complete R1–R7/X1 rule set accepts the fixture — + the X2 rule is the only rule that reads pending axes. +- The concrete damage: roles at time 3 and time 6 (both helper 476, owner + replica 0, family 224, port 0, offset 0, width 8) resolve the same + pending axis 13 of family 224 — one physical cell written twice — while + every role-level rule accepts both. + +A second mutation (one axis duplicated inside a single child's list) is +rejected at X2 as well; both are failure controls in `verify.py`. + +## Controls coverage added + +The existing rejection batteries contain no X2-directed mutant: the owner +audit's 11 controls (`drop_role`, `narrow_width`, `duplicate_helper`, +`private_family`, `active_pair`, `family_collision`, `past_idle_sweep`, +`overlap`, `prefix_gap`, `claimed_idle_tampered`, `plan_window_truncated`) +and the frozen verifier's 6 independent-t16 controls +(`private_namespace_collision`, `copy_replica_alias`, `missing_whole_helper`, +`split_whole_helper`, `truncated_helper_width`, `cross_idle_boundary`). +This package supplies the first two X2-directed mutants with single-locus, +rank-preservation and null-mutation guards. + +## Reproduce + +```sh +python3 -B research/owner-x2-acceptance-boundary/verify.py +``` + +Expected status: `PASS_PR1094_X2_ACCEPTANCE_BOUNDARY_AUDIT`. The deterministic +record is [RESULT.json](RESULT.json) with exact input pins (template +`025448ab…`, DATA-PHASES `c5916ff3…`, word `c2b29430…`, OWNERS `87902c52…`, +PLAN `7bd786ba…`, SPEC `8cb51f25…`, owner audit `f6e27f76…`, composition +`2608ef21…`, upstream1087 archive `d4acf04d…`). + +## Open next questions + +- Should `scripts/verify_frontier1094.py` execute the pinned + `check_frontier1094.py` composition (or a source-bound X2 recount) so the + record's reproduce command enforces X2 for CrocSwap/integer-mult-bounds#1094? Why it matters: the + selected record's hosting soundness currently rests on a review-time run + that the reproduce path does not repeat. First step: add the composition as + a `verify_frontier1094.py` stage and measure replay time. Blocker: needs + maintainer authorization to change the selected reproduction path; this + package does not change it. +- Does the same boundary hold for the other T16 claims' X1/X2 checks (the + `--fetch` claim list, CrocSwap/integer-mult-bounds#1022 through + CrocSwap/integer-mult-bounds#1087, is audited in CI, but its composition with + the pricing audit is not)? First step: enumerate which obligations of + `docs/research/community-batch1099-review.md` are enforced where, one rule + per table row. Blocker: none; this is a natural continuation. +- Would the frozen `indep16` chain accept the M1 fixture end to end? Why it + matters: it would close the code-trace claim by execution. First step: run + `make frontier1094-verify` with `--baseline1042` reuse and the mutated + phases overlaid. Blocker: the published frontier1042 baseline artifacts and cold + replay time were outside this session's budget; the acceptance of M1 by the + frozen chain is established by code trace only. + +## Limitations and unrun obligations + +- This is a checker-coverage audit of one named obligation. It is not a + construction, not a supplier change, and not a κ claim; the selected record + and `upstream/` are unchanged. +- The full `make frontier1094-verify` cold replay with the mutated phases was + not run (see above); frozen-chain blindness is code-trace evidence. +- No claim other than the selected CrocSwap/integer-mult-bounds#1094 inputs was re-audited; the + historical `research/owner-boundary-audit/` package was used as an example + of the method only and was not rerun. +- A finite rejection test is not a proof of hosting soundness; X2 itself is + proved by enumeration over the pinned phases, not universally. + +## Attribution and coordination + +The X2 rule, its wording, and the independent owner audit are Josie +Elliston's (`JosieElliston`, CrocSwap/integer-mult-bounds#1091), reused here +unchanged as a library. The selected owner map is Rohan Arun's +CrocSwap/integer-mult-bounds#1094 on Jeremy Kothe's T16 owner-map lineage; +the frozen verifier chain is Hao Yan's (`FanPUYen`) +CrocSwap/integer-mult-bounds#858 lineage; the batch1099 composition and +review are Douglas Colkitt's; independent endpoint pricing is Sagar +Thakrar's CrocSwap/integer-mult-bounds#1069. The nearest concurrent finding +is CrocSwap/integer-mult-bounds#1277 (ancestry recheck dropped by the reuse +replay), credited for the replay-coverage direction; this package adds the +X2 boundary and its first rejection controls. Audit work by Navinor with +help from opencode. Tasks selected with +`scripts/choose_research_task.py` (track `adversarial-audit`, OS-random +nonce `ca8debca8488dd850dd6c0afb7398632`). diff --git a/research/owner-x2-acceptance-boundary/RESULT.json b/research/owner-x2-acceptance-boundary/RESULT.json new file mode 100644 index 0000000000..10e8e19be1 --- /dev/null +++ b/research/owner-x2-acceptance-boundary/RESULT.json @@ -0,0 +1,145 @@ +{ + "status": "PASS_PR1094_X2_ACCEPTANCE_BOUNDARY_AUDIT", + "scope": { + "obligation": "X2: pending axes of distinct idle children of one physical family are disjoint", + "object": "selected CrocSwap/integer-mult-bounds#1094 frozen OWNERS/PLAN/SPEC data (research/complex-t16-rare-pattern-exchanges/data)", + "audited_head": "0fc329d0bec93ca7cd288eaea1295172e8789810", + "selected_kappa": "836330098538459/500000000000000000" + }, + "pins": { + "template_sha256": "025448abdf2012d327e50a009084e1501690d05e650300d2982836aa0350ae00", + "data_phases_sha256": "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa", + "word_content_sha256": "c2b294300760e1fd6eeab8c22c4d13e4633dca40e52cac8da0d68163a76e3ca8", + "owners_sha256": "87902c528dfab7d503dcf8a784260e3ab6fb7424c418a1820f7261f25be7b6bc", + "plan_sha256": "7bd786ba8e66408f02aa9ef446eaf20c1bfe981ea2e4dd1e5a929f0aa7767bc0", + "spec_sha256": "8cb51f25a5da4a29d3783853025b73ff1f452429d4fdb30c599e598bcab0e71d", + "owner_audit_sha256": "f6e27f76c9ccb87b3ce6c5e673588338a09847d22771da7b3f28579661c9404b", + "composition_sha256": "2608ef213260a43d09a40b3429742f7a5f280861b54acae66400a7c29a123f51", + "upstream1087_sha256": "d4acf04daef85d4514f80ec5fcd2492d0c60e5d6c49fa71b3e6523f8db2dea86" + }, + "positive_control": { + "idle": { + "1": 2276, + "3": 377, + "7": 7, + "48": 4866 + }, + "profile": { + "1": 349604, + "2": 60192, + "3": 62585, + "4": 20448, + "5": 11808, + "7": 7, + "8": 1152, + "48": 4866 + }, + "rank_mass": 1041408, + "deficit": 5120, + "calls": 144, + "roles": 69120, + "windows": 288, + "x2_child_ports": 2016 + }, + "minimal_adversarial_instance": { + "mutation": "one integer in DATA-PHASES pending axes", + "locus": { + "where": [ + 1, + 0 + ], + "children": [ + 0, + 1 + ], + "port": 0, + "replaced_index_in_c2": 0, + "old_value": 131072, + "new_value": 13, + "taken_from_child": 0, + "index_in_c1": 0 + }, + "mutated_differing_integers": 1, + "rejected_by": { + "M1_cross_child_axis": "X2: children [0, 1, 14] share axes at port 0", + "M2_within_child_duplicate": "X2: children [0, 1, 14] share axes at port 0" + }, + "cell_collision_witness": { + "owner_replica": 0, + "family": 224, + "shared_axis": 13, + "role_a": { + "time": 3, + "stage": 0, + "replica": 9, + "helper": 476, + "child": 0, + "port": 0, + "offset": 0, + "width": 8 + }, + "role_b": { + "time": 6, + "stage": 0, + "replica": 2, + "helper": 476, + "child": 1, + "port": 0, + "offset": 0, + "width": 8 + }, + "note": "Both roles resolve pending-axis 13 of family 224 at port 0; the R1-R7/X1 rule set keys cells per (owner, child, port) and accepts both." + } + }, + "blindness": { + "method": "X2 need() suppressed only to measure what the remaining rule set sees", + "geometry_identical": true, + "rule_set_accepts": true, + "rule_set": "R1-R7 plus X1 (owner-audit rule bodies)" + }, + "control_inventory": { + "owner_audit_controls": [ + "drop_role", + "narrow_width", + "duplicate_helper", + "private_family", + "active_pair", + "family_collision", + "past_idle_sweep", + "overlap", + "prefix_gap", + "claimed_idle_tampered", + "plan_window_truncated" + ], + "frozen_independent_t16_controls": [ + "private_namespace_collision", + "copy_replica_alias", + "missing_whole_helper", + "split_whole_helper", + "truncated_helper_width", + "cross_idle_boundary" + ], + "x2_directed_mutants_before_this_package": 0 + }, + "enforcement_trace": { + "reproduce_target": [ + "frontier1094-verify: selected-record-check", + "\t@work=$$(mktemp -d \"$${TMPDIR:-/tmp}/integer-mult-frontier1094.XXXXXX\"); \\", + "\tpython3 -B scripts/verify_frontier1094.py --work \"$$work/replay\"" + ], + "reproduce_stages": [ + "historical-source", + "baseline1042-cold (or baseline reuse)", + "rare-pattern-exchanges" + ], + "selected_record_check": "scripts/verify_selected_result.py validates the selected record and its proof_supplement hashes; it imports no subprocess module and executes no composition", + "ci_workflow": ".github/workflows/community-batch1099.yml runs research/t16-owner-audit-seed67/verify.py --fetch (its pinned claim list excludes the selected supplier) and check_pr1048_counterexample.py; it does not run check_frontier1094.py", + "x2_checked_by": "research/t16-owner-audit-seed67/verify.py geometry(), composed on CrocSwap/integer-mult-bounds#1094 by research/community-batch1099-audit/check_frontier1094.py at batch1099 review time", + "frozen_chain": "upstream1087.tar.gz verify_t16.py stages lift16/audit_allcold/indep16; indep16 keys cells per (owner, child, port); audit_allcold asserts only len(pending) == rank per child" + }, + "unrun_obligations": [ + "Full make frontier1094-verify cold replay with the M1-mutated DATA-PHASES (needs the frontier1042 cold baseline; out of session budget). Acceptance of M1 by the frozen chain is established by code trace, not by execution.", + "No T8/T16 claim other than CrocSwap/integer-mult-bounds#1094 was re-audited; the historical owner-boundary-audit package was not rerun.", + "No kappa, supplier adoption, or multiplication-theorem claim is made or tested here." + ] +} diff --git a/research/owner-x2-acceptance-boundary/SOURCES.json b/research/owner-x2-acceptance-boundary/SOURCES.json new file mode 100644 index 0000000000..34046ba92a --- /dev/null +++ b/research/owner-x2-acceptance-boundary/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "bce54fb3f895cbe5cd4c0eb477c3afeed100190f", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "c05fafaa25ba95b2d5af86b1800427198e3d20eb", + "sha256": "89b5928bc92c81e2647b6d702a7ad85a6795b8f44e2eb267b2ff3145d8f2b2ce" + }, + { + "path": "research/community-batch1099-audit/check_frontier1094.py", + "usage": "input", + "git_blob": "1c171898e4f58fbdeca81424c9932ec2c6bbb9c8", + "sha256": "2608ef213260a43d09a40b3429742f7a5f280861b54acae66400a7c29a123f51" + } + ] +} diff --git a/research/owner-x2-acceptance-boundary/TASK.json b/research/owner-x2-acceptance-boundary/TASK.json new file mode 100644 index 0000000000..611b137d8e --- /dev/null +++ b/research/owner-x2-acceptance-boundary/TASK.json @@ -0,0 +1,72 @@ +{ + "schema_version": 1, + "task_id": "supplier-boundary-audit", + "priority_revision": 2, + "base_commit": "bce54fb3f895cbe5cd4c0eb477c3afeed100190f", + "original_card": { + "id": "supplier-boundary-audit", + "question": "Does one selected supplier obligation follow from its actual source-bound checks?", + "starting_points": [ + "certificates/selected-result.json", + "research/owner-boundary-audit/README.md" + ], + "methods": [ + "Trace one hypothesis through the source, checker and complete caller.", + "Construct one semantically invalid but superficially well-formed fixture and test rejection." + ], + "acceptance_gate": "Pin the current sources and one obligation; the historical owner audit is an example, not evidence of a current bug.", + "first_step": { + "command": [ + "python3", + "-B", + "research/owner-boundary-audit/verify.py" + ], + "expected": "PASS_PR626_NEXT_TOUCH_BOUNDARY_AUDIT", + "inspect": "Identify why the timing-only omission passes but the full production controller still rejects it.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Choose one current supplier obligation and trace whether its acceptance depends on an independent check.", + "bottleneck_link": "Closing a current acceptance gap or proof obligation strengthens reliability even without changing kappa.", + "allowed_variations": [ + "Audit one named current condition using a new semantic counterexample." + ], + "scope_change_triggers": [ + "Reporting the historical timing-only diagnostic as a new current acceptance bug." + ], + "overlap_terms": [ + "owner boundary", + "bridge omission", + "hosting" + ] + }, + "scope_status": "unchanged", + "actual_scope": "One named selected supplier obligation (X2: pending axes of distinct idle children of one physical family are disjoint) on the selected CrocSwap/integer-mult-bounds#1094 frozen OWNERS/PLAN/SPEC at audited head 0fc329d0bec93ca7cd288eaea1295172e8789810: does its acceptance follow from the actual source-bound checks?", + "scope_change_reason": null, + "bottleneck_link": "Closing a current acceptance gap or proof obligation strengthens reliability even without changing kappa; the selected supplier is complex-bound and its hosting soundness supports every downstream packing claim.", + "budget_minutes": 60, + "stop_rule": "One obligation, one minimal one-integer counterexample battery, one enforcement trace; kill if the reproduce path already enforces X2 or if the mutation cannot be made single-locus.", + "outcome": "completed", + "evidence": "research/owner-x2-acceptance-boundary/RESULT.json (PASS_PR1094_X2_ACCEPTANCE_BOUNDARY_AUDIT): X2 is enforced only by the review-time composition check_frontier1094.py; make frontier1094-verify and community-batch1099.yml CI do not re-run it for CrocSwap/integer-mult-bounds#1094; a one-integer DATA-PHASES mutation (child 1 port 0 axis 131072 -> 13) preserves all aggregates, is accepted by the complete R1-R7/X1 rule set, and is rejected only at X2; first X2-directed rejection controls supplied.", + "author": "Navinor", + "ai_assistance": "Substantial AI assistance: task selection, trace, harness and text drafted with help from opencode (OpenCode agent harness).", + "open_questions": [ + { + "question": "Should scripts/verify_frontier1094.py execute the pinned check_frontier1094.py composition so the record reproduce command enforces X2 for CrocSwap/integer-mult-bounds#1094?", + "why_it_matters": "Selected hosting soundness currently rests on a review-time run the reproduce path does not repeat.", + "first_step": "Add the composition as a verify_frontier1094.py stage and measure replay time.", + "blocked_by": "Maintainer authorization to change the selected reproduction path." + }, + { + "question": "Which other batch1099 obligations are enforced only at review time?", + "why_it_matters": "Same replay-coverage class as CrocSwap/integer-mult-bounds#1277 (ancestry); an obligation-by-obligation table would localize every gap.", + "first_step": "Enumerate rules R1-R7/X1/X2 and the pricing identities against each checker on the reproduce path.", + "blocked_by": null + }, + { + "question": "Does the frozen upstream1087 chain accept the M1 fixture end to end?", + "why_it_matters": "Would replace the code-trace blindness claim with execution.", + "first_step": "Run make frontier1094-verify with --baseline1042 reuse and the mutated phases overlaid.", + "blocked_by": "Published frontier1042 baseline artifacts and cold replay time were outside this session budget." + } + ] +} \ No newline at end of file diff --git a/research/owner-x2-acceptance-boundary/VERIFY.json b/research/owner-x2-acceptance-boundary/VERIFY.json new file mode 100644 index 0000000000..818f8251e3 --- /dev/null +++ b/research/owner-x2-acceptance-boundary/VERIFY.json @@ -0,0 +1,20 @@ +{ + "schema_version": 1, + "status": "passing", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/community-batch1099-audit/check_frontier1094.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Positive control: pinned CrocSwap/integer-mult-bounds#1094 inputs pass the full R1-R7/X1/X2 owner audit. Failure controls: M1 one-integer cross-child axis mutation rejected at X2 with single-locus and rank-preservation guards; M2 within-child duplicate rejected at X2; M1/M2 loci differ. Blindness: X2 need() suppressed, geometry identical and R1-R7/X1 accept M1. Coverage: 11 owner-audit and 6 frozen indep16 controls inventoried, zero X2-directed mutants before this package. Trace: reproduce target, verify_frontier1094.py, verify_selected_result.py, community-batch1099.yml, claim list 1022-1087 and frozen indep16/audit_allcold keying asserted as recorded." + } + ] +} \ No newline at end of file diff --git a/research/owner-x2-acceptance-boundary/verify.py b/research/owner-x2-acceptance-boundary/verify.py new file mode 100644 index 0000000000..b9c82219e5 --- /dev/null +++ b/research/owner-x2-acceptance-boundary/verify.py @@ -0,0 +1,348 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""X2 acceptance-boundary audit for the selected CrocSwap/integer-mult-bounds#1094 supplier owner map. + +Navinor, with help from opencode. Apache-2.0. + +One named obligation of the selected complex supplier (certificates/selected-result.json, +CrocSwap/integer-mult-bounds#1094 frozen OWNERS/PLAN/SPEC at audited head 0fc329d0bec93ca7cd288eaea1295172e8789810): + + X2 pending axes of distinct idle children of one physical family are disjoint, + so a family's hosts on different children never share a cell. + +X2 is checked by geometry() in Josie Elliston's independent owner audit +(research/t16-owner-audit-seed67/verify.py, CrocSwap/integer-mult-bounds#1091), composed onto CrocSwap/integer-mult-bounds#1094 by +research/community-batch1099-audit/check_frontier1094.py. This package traces +where that check actually executes, and builds the smallest semantic +counterexample it rejects: a one-integer mutation of the pinned DATA-PHASES +pending axes that preserves every role-level and window-level aggregate. + +Checks in this file: + 1. Positive control: the pinned inputs pass the complete R1-R7/X1/X2 audit. + 2. M1 (minimal adversarial instance): one pending axis of one idle child is + replaced by an axis already pending for a distinct idle child of the same + physical family at the same port. Superficial aggregates (ranks, windows, + role counts, widths, profile) are unchanged. geometry() must reject at X2. + 2b. Witness: under M1, exhibit the exact physical cell written twice (family, + axis) by two roles that every role-level rule accepts. + 3. M2 failure control: one axis duplicated inside a single child's pending + list. geometry() must reject at X2 as well. + 4. Blindness: with only the X2 need() suppressed, geometry() returns an + identical geometry object and the complete R1-R7/X1 rule set accepts the + M1 fixture. The X2 rule is the only rule that reads pending axes. + 5. Coverage inventory: the existing 11 owner-audit controls and the frozen + verifier's 6 independent-t16 controls contain no X2-directed mutant. + 6. Enforcement trace (static, recorded with exact excerpts): the selected + reproduce command and the CI workflow do not execute the CrocSwap/integer-mult-bounds#1094 owner + composition, and the frozen CrocSwap/integer-mult-bounds#1087 verifier chain keys hosted cells per + (owner, child, port), so cross-child cell sharing is outside its rule set. + +Unrun obligations are listed in RESULT.json and the README. +""" +import copy +import gzip +import hashlib +import importlib.util +import json +import re +import sys +import tarfile +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + + +def read(path): + path = Path(path) + return json.loads(gzip.decompress(path.read_bytes()) if path.suffix == '.gz' else path.read_bytes()) + + +def text(path): + return Path(path).read_text(encoding='utf-8') + + +def sha(path): + return hashlib.sha256(Path(path).read_bytes()).hexdigest() + + +def require(ok, message): + if not ok: + raise ValueError('X2 boundary audit: ' + message) + + +def load_module(name, path): + spec = importlib.util.spec_from_file_location(name, path) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +# ---------------------------------------------------------------- inputs + +a = load_module('owner_audit', ROOT / 'research/t16-owner-audit-seed67/verify.py') +pins = read(ROOT / 'research/t16-owner-audit-seed67/SOURCES.json')['inputs'] +require(sha(ROOT / a.TEMPLATE) == pins['template_sha256'], 'template pin') +require(sha(ROOT / a.PHASES) == pins['data_phases_sha256'], 'DATA-PHASES pin') +require(hashlib.sha256(gzip.decompress(a.WORD.read_bytes())).hexdigest() == pins['word_content_sha256'], + 'seven-slot word pin') + +word = read(a.WORD) +template = read(ROOT / a.TEMPLATE) +phases = read(ROOT / a.PHASES) +widths = a.word_widths(word) +local = a.as_profile(word['report']['local_profile']) + +pkg = ROOT / 'research/complex-t16-rare-pattern-exchanges' +spec = read(pkg / 'data/SPEC.json') +plan = read(pkg / 'data/PLAN.json') +roles = read(pkg / 'data/OWNERS.json.gz') +expected_idle = a.as_profile(spec['expected']['idle_remainder_profile']) +T = 16 + +# ---------------------------------------------------------------- 1. positive control + +geo0 = a.geometry(template, phases) +owned0 = a.audit(geo0, widths, local, roles, plan, expected_idle, T) +require(owned0['roles'] == len(roles), 'positive control role count') + +# ---------------------------------------------------------------- M1 fixture + +place, rank = geo0['place'], geo0['rank'] +children = sorted(rank) + + +def axes_lists(ph): + """Yield mutable (recipe_index, child_key, list) pending-axis lists.""" + for ri, recipe in enumerate(ph['recipes']): + kids = recipe['idle_children'] + items = enumerate(kids) if isinstance(kids, list) else ((int(k), v) for k, v in kids.items()) + for child, item in items: + yield ri, child, item['orthogonal_axes'] + + +axes_map = {} +for ri, child, raw in axes_lists(phases): + axes_map[child, phases['recipes'][ri]['port']] = [int(x) for x in raw] + +groups = {} +for child in children: + groups.setdefault(place[child], []).append(child) + +candidate = None +for where, siblings in sorted(groups.items()): + for i, c1 in enumerate(siblings): + for c2 in siblings[i + 1:]: + for port in range(112): + l1 = axes_map.get((c1, port)) + l2 = axes_map.get((c2, port)) + if not l1 or not l2: + continue + shared = [x for x in l1 if x not in l2] + if not shared: + continue + for k in range(len(l2)): + if l2[k] not in l1: + candidate = dict(where=where, c1=c1, c2=c2, port=port, + value=shared[0], c1_index=l1.index(shared[0]), c2_index=k) + break + if candidate: + break + if candidate: + break + if candidate: + break + if candidate: + break +require(candidate is not None, 'no cross-child axis locus found') + +phases_m1 = copy.deepcopy(phases) +port_index = next(ri for ri, r in enumerate(phases_m1['recipes']) if r['port'] == candidate['port']) +kids = phases_m1['recipes'][port_index]['idle_children'] +entry = kids[candidate['c2']] if isinstance(kids, list) else kids[str(candidate['c2'])] +before = int(entry['orthogonal_axes'][candidate['c2_index']]) +entry['orthogonal_axes'][candidate['c2_index']] = candidate['value'] + +# Single-locus and superficial-aggregate guards. +raw_delta = sum(1 for (_, _, old), (_, _, new) in zip(axes_lists(phases), axes_lists(phases_m1)) + for u, v in zip(old, new) if int(u) != int(v)) +require(raw_delta == 1, 'M1 must be a one-integer mutation') +geo_m1_x2suppressed = None + +rejects = {} +for name, ph in (('M1_cross_child_axis', phases_m1),): + try: + a.geometry(template, ph) + except a.Reject as exc: + rejects[name] = str(exc) +require(rejects.get('M1_cross_child_axis', '').startswith('X2:'), + 'M1 must be rejected at X2, got: ' + rejects.get('M1_cross_child_axis')) + +# ---------------------------------------------------------------- 2b. cell-collision witness + +c1, c2, port = candidate['c1'], candidate['c2'], candidate['port'] +pair, side = place[c1] +require(place[c2] == (pair, side), 'witness children must share the physical family') +value = candidate['value'] +axis_index_in_bases = None + + +def covers(role, child, port_, index): + return (role['child'] == child and role['port'] == port_ + and role['offset'] <= index < role['offset'] + role['width']) + + +witness = None +for owner in range(T): + left = [z for z in roles if z['owner_replica'] == owner and covers(z, c1, port, candidate['c1_index'])] + right = [z for z in roles if z['owner_replica'] == owner and covers(z, c2, port, candidate['c2_index'])] + if left and right: + z1, z2 = left[0], right[0] + family = owner * a.FAMILIES_PER_REPLICA + (2 * pair + side) * a.V + port + require(z1['family'] == family and z2['family'] == family, 'witness family identity') + witness = dict(owner_replica=owner, family=family, shared_axis=value, + role_a={k: z1[k] for k in ('time', 'stage', 'replica', 'helper', 'child', 'port', 'offset', 'width')}, + role_b={k: z2[k] for k in ('time', 'stage', 'replica', 'helper', 'child', 'port', 'offset', 'width')}, + note='Both roles resolve pending-axis %d of family %d at port %d; the R1-R7/X1 rule set ' + 'keys cells per (owner, child, port) and accepts both.' % (value, family, port)) + break +require(witness is not None, 'no colliding role pair found for M1') + +# ---------------------------------------------------------------- 3. M2 failure control + +phases_m2 = copy.deepcopy(phases) +m2 = None +for ri, child, raw in axes_lists(phases_m2): + vals = [int(x) for x in raw] + if len(vals) >= 2: + duplicate = vals[0] + if duplicate not in vals[1:]: + kids = phases_m2['recipes'][ri]['idle_children'] + entry = kids[child] if isinstance(kids, list) else kids[str(child)] + entry['orthogonal_axes'][-1] = duplicate + m2 = dict(recipe_index=ri, child=child, index=len(vals) - 1, + port=phases_m2['recipes'][ri]['port'], value=duplicate) + break +require(m2 is not None, 'no within-child duplicate locus found') +require((m2['recipe_index'], m2['child'], m2['index']) + != (port_index, candidate['c2'], candidate['c2_index']), 'M1 and M2 must use different loci') +try: + a.geometry(template, phases_m2) +except a.Reject as exc: + rejects['M2_within_child_duplicate'] = str(exc) +require(rejects.get('M2_within_child_duplicate', '').startswith('X2:'), + 'M2 must be rejected at X2, got: ' + rejects.get('M2_within_child_duplicate')) + +# ---------------------------------------------------------------- 4. blindness of R1-R7/X1 + +original_need = a.need + + +def need_x2_suppressed(ok, rule, msg): + if rule == 'X2': + return + original_need(ok, rule, msg) + + +a.need = need_x2_suppressed +try: + geo_m1_x2suppressed = a.geometry(template, phases_m1) + owned_m1 = a.audit(geo_m1_x2suppressed, widths, local, roles, plan, expected_idle, T) +finally: + a.need = original_need +require(geo_m1_x2suppressed == geo0, 'geometry object must not depend on pending axes') +require(owned_m1 == owned0, 'R1-R7/X1 must be blind to the X2 violation') + +# ---------------------------------------------------------------- 5. control inventory + +controls = a.controls(geo0, widths, local, roles, plan, expected_idle, T) +control_names = [c['name'] for c in controls] +require(len(control_names) == 11 and all(c['rejected_by'] != 'X2' or c['name'] == 'plan_window_truncated' + for c in controls), 'unexpected owner-audit control battery') + +tar_path = pkg / 'upstream1087.tar.gz' +frozen = {} +with tarfile.open(tar_path) as tar: + for name in ('verify_t16.py', 't16/indep16.py', 'code/audit_allcold.py', 'code/emit_allcold.py'): + frozen[name] = tar.extractfile(name).read().decode('utf-8') +indep_controls = re.findall(r"candidates\.append\(\('([a-z0-9_]+)'", frozen['t16/indep16.py']) +require(len(indep_controls) == 6, 'frozen independent-t16 control battery size') +require('X2' not in ''.join(frozen.values()), 'frozen verifier unexpectedly mentions X2') + +# ---------------------------------------------------------------- 6. enforcement trace + +makefile = text(ROOT / 'Makefile') +m = re.search(r'frontier1094-verify:.*?(?=\n\S)', makefile, re.S) +require(m is not None, 'frontier1094-verify target missing') +target = m.group(0) +verify_frontier = text(ROOT / 'scripts/verify_frontier1094.py') +selected_record_check = text(ROOT / 'scripts/verify_selected_result.py') +ci = text(ROOT / '.github/workflows/community-batch1099.yml') +claim_prs = [c['pr'] for c in read(ROOT / 'research/t16-owner-audit-seed67/SOURCES.json')['claims']] +require('check_frontier1094' not in target and 'check_frontier1094' not in verify_frontier + and 'check_frontier1094' not in selected_record_check, 'reproduce path unexpectedly runs the composition') +require('check_frontier1094' not in ci, 'CI unexpectedly runs the composition') +require('research/t16-owner-audit-seed67/verify.py --fetch' in ci, 'CI owner-audit step missing') +require(1094 not in claim_prs, 'CrocSwap/integer-mult-bounds#1094 unexpectedly inside the owner-audit claim list') +require('bin_key = (owner, child, port)' in frozen['t16/indep16.py'], 'indep16 bin keying changed') +require('orthogonal_axes' in frozen['code/audit_allcold.py'] + and 'len(pend)==prank[i]' in frozen['code/audit_allcold.py'], 'audit_allcold pending-axis read changed') + +# ---------------------------------------------------------------- result + +result = dict( + status='PASS_PR1094_X2_ACCEPTANCE_BOUNDARY_AUDIT', + scope=dict( + obligation='X2: pending axes of distinct idle children of one physical family are disjoint', + object='selected CrocSwap/integer-mult-bounds#1094 frozen OWNERS/PLAN/SPEC data (research/complex-t16-rare-pattern-exchanges/data)', + audited_head='0fc329d0bec93ca7cd288eaea1295172e8789810', + selected_kappa='836330098538459/500000000000000000', + ), + pins=dict(template_sha256=pins['template_sha256'], data_phases_sha256=pins['data_phases_sha256'], + word_content_sha256=pins['word_content_sha256'], + owners_sha256=sha(pkg / 'data/OWNERS.json.gz'), plan_sha256=sha(pkg / 'data/PLAN.json'), + spec_sha256=sha(pkg / 'data/SPEC.json'), + owner_audit_sha256=sha(ROOT / 'research/t16-owner-audit-seed67/verify.py'), + composition_sha256=sha(ROOT / 'research/community-batch1099-audit/check_frontier1094.py'), + upstream1087_sha256=sha(tar_path)), + positive_control=dict(idle=owned0['idle'], profile=owned0['profile'], rank_mass=owned0['rank_mass'], + deficit=owned0['deficit'], calls=owned0['calls'], roles=owned0['roles'], + windows=owned0['windows'], x2_child_ports=geo0['x2_child_ports']), + minimal_adversarial_instance=dict( + mutation='one integer in DATA-PHASES pending axes', + locus=dict(where=list(candidate['where']), children=[c1, c2], port=port, + replaced_index_in_c2=candidate['c2_index'], old_value=before, new_value=value, + taken_from_child=c1, index_in_c1=candidate['c1_index']), + mutated_differing_integers=raw_delta, + rejected_by=rejects, + cell_collision_witness=witness), + blindness=dict( + method='X2 need() suppressed only to measure what the remaining rule set sees', + geometry_identical=geo_m1_x2suppressed == geo0, + rule_set_accepts=owned_m1 == owned0, + rule_set='R1-R7 plus X1 (owner-audit rule bodies)'), + control_inventory=dict(owner_audit_controls=control_names, + frozen_independent_t16_controls=indep_controls, + x2_directed_mutants_before_this_package=0), + enforcement_trace=dict( + reproduce_target=target.strip().splitlines(), + reproduce_stages=['historical-source', 'baseline1042-cold (or baseline reuse)', 'rare-pattern-exchanges'], + selected_record_check='scripts/verify_selected_result.py validates the selected record and its ' + 'proof_supplement hashes; it imports no subprocess module and executes no composition', + ci_workflow='.github/workflows/community-batch1099.yml runs research/t16-owner-audit-seed67/verify.py --fetch ' + '(its pinned claim list excludes the selected supplier) and check_pr1048_counterexample.py; ' + 'it does not run check_frontier1094.py', + x2_checked_by='research/t16-owner-audit-seed67/verify.py geometry(), composed on CrocSwap/integer-mult-bounds#1094 by ' + 'research/community-batch1099-audit/check_frontier1094.py at batch1099 review time', + frozen_chain='upstream1087.tar.gz verify_t16.py stages lift16/audit_allcold/indep16; indep16 keys cells per ' + '(owner, child, port); audit_allcold asserts only len(pending) == rank per child', + ), + unrun_obligations=[ + 'Full make frontier1094-verify cold replay with the M1-mutated DATA-PHASES (needs the frontier1042 cold baseline; ' + 'out of session budget). Acceptance of M1 by the frozen chain is established by code trace, not by execution.', + 'No T8/T16 claim other than CrocSwap/integer-mult-bounds#1094 was re-audited; the historical owner-boundary-audit package was not rerun.', + 'No kappa, supplier adoption, or multiplication-theorem claim is made or tested here.', + ], +) +(HERE / 'RESULT.json').write_text(json.dumps(result, indent=2) + '\n', encoding='utf-8') +print(result['status'], 'M1 rejected at', rejects['M1_cross_child_axis'][:60]) From 1948edd970b2c300c304577adb814dda6da7b3b2 Mon Sep 17 00:00:00 2001 From: Aaron Wang Date: Wed, 14 Oct 2026 04:26:07 -0400 Subject: [PATCH 2/2] Narrow the X2 blindness claim to the semantic layer and execute the source-bound hash-pin path --- .../owner-x2-acceptance-boundary/README.md | 87 +++++++-- .../owner-x2-acceptance-boundary/RESULT.json | 93 ++++++++- .../owner-x2-acceptance-boundary/SOURCES.json | 24 +++ .../owner-x2-acceptance-boundary/TASK.json | 18 +- .../owner-x2-acceptance-boundary/VERIFY.json | 11 +- .../owner-x2-acceptance-boundary/verify.py | 183 +++++++++++++++++- 6 files changed, 374 insertions(+), 42 deletions(-) diff --git a/research/owner-x2-acceptance-boundary/README.md b/research/owner-x2-acceptance-boundary/README.md index 1243092d56..fe6261929a 100644 --- a/research/owner-x2-acceptance-boundary/README.md +++ b/research/owner-x2-acceptance-boundary/README.md @@ -22,8 +22,13 @@ audit (`research/t16-owner-audit-seed67/verify.py`, `geometry()`). reproduce command. It depends on the review-time maintainer composition `research/community-batch1099-audit/check_frontier1094.py`, which is pinned in the record's `proof_supplements` but is executed neither by -`make frontier1094-verify` nor by the `community-batch1099.yml` CI job. Every -checker that the reproduce path does execute is structurally blind to X2. +`make frontier1094-verify` nor by the `community-batch1099.yml` CI job. No +checker that the reproduce path does execute recomputes X2 semantically. That +is a missing-semantic-recomputation gap, not demonstrated end-to-end +acceptance of a mutated pinned input: the source-hash layers reject the +mutated fixture before the semantic rules ever run (executed evidence below), +and full mutated-chain acceptance was not executed. Which layer catches what +is recorded in `RESULT.json` under `source_bound_acceptance`. ## Task card @@ -38,8 +43,9 @@ Base commit; exact predecessor and dependency heads: Concrete object and question: one named condition, X2, of the selected supplier's hosting soundness: does its acceptance follow from the actual source-bound checks? -Scope status: unchanged (one named current condition audited with a new - semantic counterexample, as the card allows) +Scope status: refined (one named current condition audited with a new + semantic counterexample, as the card allows; wording refined to the + selected CrocSwap/integer-mult-bounds#1094 owner map and obligation X2) Existing restriction being changed (or exact claim being audited): audited claim: the selected composition's owner/hosting acceptance Method; explicit parameter ranges/candidate alphabet: @@ -59,7 +65,8 @@ Optimistic full cost budget; required observable improvement: stdlib-only replay of the pinned audit on pinned inputs; no construction Success evidence; falsification test; time/compute cap: RESULT.json from one command; falsified if geometry() accepts M1 or if any - executed checker on the reproduce path rejects M1; minutes on one core + executed semantic rule on the reproduce path rejects M1 (source-hash pin + rejections do not count as semantic detection); minutes on one core Predecessor authors; intended artifact and reproduction command: Josie Elliston (X2 rule, owner audit), Rohan Arun (CrocSwap/integer-mult-bounds#1094 owner map), Jeremy Kothe (T16 owner-map lineage), Hao Yan (CrocSwap/integer-mult-bounds#858 controller/indep16), @@ -78,11 +85,42 @@ Predecessor authors; intended artifact and reproduction command: | frozen `upstream1087.tar.gz` chain (`verify_t16.py` → `lift16`/`audit_allcold`/`indep16`) | n/a | no — `indep16.py` keys cells per `(owner, child, port)`; `audit_allcold.py` asserts only `len(pending) == rank` per child | | `research/community-batch1099-audit/check_frontier1094.py` (batch1099 review time) | — | **yes**, via `geometry()`; its result is pinned evidence in `docs/research/community-batch1099-integration.json` | -So the obligation is real and currently checked exactly once, at review time, -by a composition that neither the reproduce command nor CI re-runs for CrocSwap/integer-mult-bounds#1094. -The construction-time receipts in `hosting/expand_owners.py` and -`hosting/reuse_owners.py` record `all_footprints_disjoint_compacted_prefixes: -True` as a flag; the flag is not independently enforced on the reproduce path. +So the obligation is real and currently checked semantically exactly once, at +review time, by a composition that neither the reproduce command nor CI +re-runs for CrocSwap/integer-mult-bounds#1094. The construction-time receipts in +`hosting/expand_owners.py` and `hosting/reuse_owners.py` record +`all_footprints_disjoint_compacted_prefixes: True` as a flag; the flag is not +independently enforced on the reproduce path. + +## Hash/pin layer vs semantic layer (executed) + +Review follow-up: missing semantic recomputation is not the same as acceptance +of mutated pinned inputs, because the source-hash layers can reject the +mutation first. The source-bound acceptance path has three layers, and each +one's relation to the M1 fixture is measured: + +| Layer | Checker | M1-mutated pinned `DATA-PHASES.json` | +| --- | --- | --- | +| record/manifest hashes | `scripts/verify_selected_result.py` (record, `SELECTED-SOURCE.json` package inventory, `proof_supplements`) | the top-level audit fixture is outside the manifest's package roots, so this layer alone neither accepts nor rejects it; the three vendored `DATA-PHASES.json` copies are pinned at `c5916ff3…` and a mutation of those is rejected | +| source input pins, before any semantic rule | `check_frontier1094.py` line 19; `t16-owner-audit-seed67/verify.py` line 359 | **rejected** at the sha256 pin (`SOURCES.json` `inputs.data_phases_sha256`) | +| semantic rules | R1–R7/X1, X2 (`geometry()`); frozen `indep16`/`audit_allcold` | R1–R7/X1 accept (executed, in-memory); X2 rejects (executed); frozen chain carries no cross-child rule (code trace) | + +Executed evidence (verify.py section 7, recorded in `RESULT.json` +`source_bound_acceptance.executed`): the one-integer M1 edit is applied to a +copy of the pinned fixture bytes in a scratch tree (byte delta 4; parsing the +edited bytes yields exactly the in-memory M1 fixture; tracked files are +untouched and the scratch tree is deleted), and the real source-bound +entrypoints are run against it. With the mutation, +`check_frontier1094.py` stops at its DATA-PHASES hash require (line 19, +before `geometry()` at line 21) and the owner audit stops at +`FAIL input: DATA-PHASES hash` (line 359, before `geometry()` at line 362). +With intact bytes, both entrypoints pass the pins and reach later code: the +composition stops only at the intentionally absent scratch dependency past +`geometry()`, and the owner audit reaches its claim loop and stops only on the +absent git blob store. So the demonstrated gap is that no executed checker +recomputes X2 semantically on the reproduce path; a mutated pinned input is +rejected by the source-hash layer before the semantic rules, and end-to-end +acceptance of the mutated chain was not executed. ## Minimal adversarial instance @@ -95,7 +133,10 @@ role count, width and profile aggregate (exactly one differing integer), and: - `geometry()` rejects it: `X2: children [0, 1, 14] share axes at port 0`. - With only the X2 `need()` suppressed, `geometry()` returns a byte-identical geometry object and the complete R1–R7/X1 rule set accepts the fixture — - the X2 rule is the only rule that reads pending axes. + the X2 rule is the only rule that reads pending axes. This is a + semantic-layer measurement on in-memory mutated bytes: the source-bound + entrypoints never deliver mutated pinned bytes to these rules (hash layer, + above). - The concrete damage: roles at time 3 and time 6 (both helper 476, owner replica 0, family 224, port 0, offset 0, width 8) resolve the same pending axis 13 of family 224 — one physical cell written twice — while @@ -144,12 +185,18 @@ PLAN `7bd786ba…`, SPEC `8cb51f25…`, owner audit `f6e27f76…`, composition the pricing audit is not)? First step: enumerate which obligations of `docs/research/community-batch1099-review.md` are enforced where, one rule per table row. Blocker: none; this is a natural continuation. -- Would the frozen `indep16` chain accept the M1 fixture end to end? Why it - matters: it would close the code-trace claim by execution. First step: run - `make frontier1094-verify` with `--baseline1042` reuse and the mutated - phases overlaid. Blocker: the published frontier1042 baseline artifacts and cold - replay time were outside this session's budget; the acceptance of M1 by the - frozen chain is established by code trace only. +- Would the frozen `indep16` chain accept a mutated fixture end to end below + the hash pins? Why it matters: it would close the remaining code-trace claim + (the frozen chain carries no cross-child pending-axis rule) by execution. + First step: run `make frontier1094-verify` with `--baseline1042` reuse and + the mutated phases re-pinned consistently at generation time. Blocker: the + published frontier1042 baseline artifacts and cold replay time were outside + this session's budget. What is already executed: the source-bound + entrypoints reject the mutated pinned bytes at their hash pins before any + semantic rule runs, so the mutated pinned input never reaches the frozen + chain; the chain's own DATA-PHASES hash handling is an emit-time + self-consistency binding (`emit_allcold.py` `source_artifacts` ↔ + `audit_allcold.py` `exact_data_phase_recipe_sha256`), not an external pin. ## Limitations and unrun obligations @@ -157,7 +204,11 @@ PLAN `7bd786ba…`, SPEC `8cb51f25…`, owner audit `f6e27f76…`, composition construction, not a supplier change, and not a κ claim; the selected record and `upstream/` are unchanged. - The full `make frontier1094-verify` cold replay with the mutated phases was - not run (see above); frozen-chain blindness is code-trace evidence. + not run (see above); frozen-chain blindness is code-trace evidence, and + end-to-end acceptance of a mutated pinned input is not claimed anywhere in + this package. The executed evidence covers the semantic layer (in-memory + mutation) and the hash/pin layer (real entrypoints run against a scratch + copy of the mutated bytes). - No claim other than the selected CrocSwap/integer-mult-bounds#1094 inputs was re-audited; the historical `research/owner-boundary-audit/` package was used as an example of the method only and was not rerun. diff --git a/research/owner-x2-acceptance-boundary/RESULT.json b/research/owner-x2-acceptance-boundary/RESULT.json index 10e8e19be1..8faf6fe63a 100644 --- a/research/owner-x2-acceptance-boundary/RESULT.json +++ b/research/owner-x2-acceptance-boundary/RESULT.json @@ -92,10 +92,95 @@ } }, "blindness": { - "method": "X2 need() suppressed only to measure what the remaining rule set sees", + "method": "X2 need() suppressed only to measure what the remaining semantic rule set sees; in-memory mutated bytes, not an end-to-end acceptance claim for a mutated pinned input", "geometry_identical": true, "rule_set_accepts": true, - "rule_set": "R1-R7 plus X1 (owner-audit rule bodies)" + "rule_set": "R1-R7 plus X1 (owner-audit rule bodies), semantic layer only" + }, + "source_bound_acceptance": { + "claim_scope": "Missing semantic recomputation on the reproduce path is demonstrated; end-to-end acceptance of a mutated pinned input is not. The semantic rule set does not reject M1 (executed in memory), but the source-hash layer rejects the mutated pinned bytes before any semantic rule runs (executed at both source-bound entrypoints). Full mutated-chain acceptance was not executed.", + "layer_order": [ + "record/manifest hashes (scripts/verify_selected_result.py)", + "source input pins (check_frontier1094.py, t16-owner-audit-seed67/verify.py)", + "semantic rules (R1-R7/X1, X2; frozen indep16/audit_allcold)" + ], + "record_manifest_layer": { + "script": "scripts/verify_selected_result.py", + "fixture_covered_by_package_roots": false, + "fixture_note": "the top-level audit fixture is outside the record manifest package roots, so this layer alone neither accepts nor rejects it; it is pinned separately by research/t16-owner-audit-seed67/SOURCES.json inputs.data_phases_sha256", + "vendored_phase_copies_pinned": [ + "research/complex-sw4-frame8/vendor/main/research/community-k492-audit/pr622/replay/baseline558/complex-global/base/work/complex-nine-native/DATA-PHASES.json", + "research/complex-sw4-frame8/vendor/main/research/complex-k492-owner-repair/vendor/multicold/vendor/pr558/vendor/pr552/complex-global/vendor531/inputs/data-base/work/complex-nine-native/DATA-PHASES.json", + "research/direct-delivery504-global/inputs/data-base/work/complex-nine-native/DATA-PHASES.json" + ], + "vendored_phase_copies_digest": "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa", + "composition_pinned_by_proof_supplements": true + }, + "input_pin_layer": { + "pins_from": "research/t16-owner-audit-seed67/SOURCES.json inputs.data_phases_sha256", + "composition": { + "script": "research/community-batch1099-audit/check_frontier1094.py", + "pin_line": 19, + "geometry_line": 21, + "order": "hash pin before geometry()/X2" + }, + "owner_audit": { + "script": "research/t16-owner-audit-seed67/verify.py", + "pin_line": 359, + "geometry_line": 362, + "order": "hash pin before geometry()/X2" + } + }, + "executed": { + "mutation": "one integer token 131072 -> 13 at byte offset 1153 (recipes[0].idle_children[1].orthogonal_axes[0]); equals the in-memory M1 fixture; tracked files untouched, scratch tree deleted", + "byte_delta": 4, + "runs": [ + { + "label": "composition_m1_mutated_pinned_input", + "entrypoint": "research/community-batch1099-audit/check_frontier1094.py", + "exit_code": 1, + "traceback_frames": [ + 12, + 19 + ], + "fail_marker": [] + }, + { + "label": "owner_audit_m1_mutated_pinned_input", + "entrypoint": "research/t16-owner-audit-seed67/verify.py", + "exit_code": 1, + "traceback_frames": [], + "fail_marker": [ + "FAIL input: DATA-PHASES hash" + ] + }, + { + "label": "composition_intact_control", + "entrypoint": "research/community-batch1099-audit/check_frontier1094.py", + "exit_code": 1, + "traceback_frames": [ + 14, + 22 + ], + "fail_marker": [] + }, + { + "label": "owner_audit_intact_control", + "entrypoint": "research/t16-owner-audit-seed67/verify.py", + "exit_code": 1, + "traceback_frames": [ + 74, + 376, + 428 + ], + "fail_marker": [] + } + ] + }, + "frozen_chain_layer": { + "binding": "emit_allcold.py records source_artifacts sha at emit time; audit_allcold.py asserts template exact_data_phase_recipe_sha256 equals the current file sha (self-consistency binding, not an external pin to the frozen digest)", + "semantic_gap": "no cross-child pending-axis rule (code trace)" + } }, "control_inventory": { "owner_audit_controls": [ @@ -132,13 +217,13 @@ "baseline1042-cold (or baseline reuse)", "rare-pattern-exchanges" ], - "selected_record_check": "scripts/verify_selected_result.py validates the selected record and its proof_supplement hashes; it imports no subprocess module and executes no composition", + "selected_record_check": "scripts/verify_selected_result.py validates the selected record, its certificate, the SELECTED-SOURCE package inventory and its proof_supplement hashes; it imports no subprocess module and executes no composition; the top-level audit fixture is outside its package roots (see source_bound_acceptance.record_manifest_layer)", "ci_workflow": ".github/workflows/community-batch1099.yml runs research/t16-owner-audit-seed67/verify.py --fetch (its pinned claim list excludes the selected supplier) and check_pr1048_counterexample.py; it does not run check_frontier1094.py", "x2_checked_by": "research/t16-owner-audit-seed67/verify.py geometry(), composed on CrocSwap/integer-mult-bounds#1094 by research/community-batch1099-audit/check_frontier1094.py at batch1099 review time", "frozen_chain": "upstream1087.tar.gz verify_t16.py stages lift16/audit_allcold/indep16; indep16 keys cells per (owner, child, port); audit_allcold asserts only len(pending) == rank per child" }, "unrun_obligations": [ - "Full make frontier1094-verify cold replay with the M1-mutated DATA-PHASES (needs the frontier1042 cold baseline; out of session budget). Acceptance of M1 by the frozen chain is established by code trace, not by execution.", + "Full make frontier1094-verify cold replay with the M1-mutated DATA-PHASES (needs the frontier1042 cold baseline; out of session budget), so end-to-end acceptance of a mutated pinned input is not claimed and the structural-blindness claim is limited to missing semantic recomputation. What is executed: the semantic layer accepts M1 in memory (R1-R7/X1) and rejects at X2, and the source-bound entrypoints reject the mutated pinned bytes at their source-hash pins before any semantic rule runs. The frozen chain carries no cross-child pending-axis rule (code trace); its DATA-PHASES hash handling is an emit-time self-consistency binding, not an external pin.", "No T8/T16 claim other than CrocSwap/integer-mult-bounds#1094 was re-audited; the historical owner-boundary-audit package was not rerun.", "No kappa, supplier adoption, or multiplication-theorem claim is made or tested here." ] diff --git a/research/owner-x2-acceptance-boundary/SOURCES.json b/research/owner-x2-acceptance-boundary/SOURCES.json index 34046ba92a..cb31ac87b5 100644 --- a/research/owner-x2-acceptance-boundary/SOURCES.json +++ b/research/owner-x2-acceptance-boundary/SOURCES.json @@ -19,6 +19,30 @@ "usage": "input", "git_blob": "1c171898e4f58fbdeca81424c9932ec2c6bbb9c8", "sha256": "2608ef213260a43d09a40b3429742f7a5f280861b54acae66400a7c29a123f51" + }, + { + "path": "research/t16-owner-audit-seed67/verify.py", + "usage": "input", + "git_blob": "3ff276c3040ec4a52db932e0bcdd31df5a3cf0a4", + "sha256": "f6e27f76c9ccb87b3ce6c5e673588338a09847d22771da7b3f28579661c9404b" + }, + { + "path": "research/t16-owner-audit-seed67/SOURCES.json", + "usage": "input", + "git_blob": "92b80c5f45c16a43f56a8ce51147cb5bd14c5e6a", + "sha256": "d3d71303dcd25fe84a3e026c4ad53535607ba6b288fd144736ad2a5376390396" + }, + { + "path": "research/community-k492-audit/pr622/replay/baseline558/complex-global/base/work/complex-nine-native/DATA-PHASES.json", + "usage": "input", + "git_blob": "d9a4f84211182ca200c081ea061d724c8a2cfb70", + "sha256": "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa" + }, + { + "path": "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "usage": "provenance", + "git_blob": "6a75493790b4eff9c4a98051ef8b01d6aad0d5a8", + "sha256": "79b3de5db3dbcb9829789ba58e9e45758926031e2a7d80667a08429d369be53b" } ] } diff --git a/research/owner-x2-acceptance-boundary/TASK.json b/research/owner-x2-acceptance-boundary/TASK.json index 611b137d8e..6c05b3bf67 100644 --- a/research/owner-x2-acceptance-boundary/TASK.json +++ b/research/owner-x2-acceptance-boundary/TASK.json @@ -39,20 +39,20 @@ "hosting" ] }, - "scope_status": "unchanged", + "scope_status": "refined", "actual_scope": "One named selected supplier obligation (X2: pending axes of distinct idle children of one physical family are disjoint) on the selected CrocSwap/integer-mult-bounds#1094 frozen OWNERS/PLAN/SPEC at audited head 0fc329d0bec93ca7cd288eaea1295172e8789810: does its acceptance follow from the actual source-bound checks?", - "scope_change_reason": null, + "scope_change_reason": "Card question refined to one named condition (X2) of one selected supplier (CrocSwap/integer-mult-bounds#1094 owner map), matching the card's allowed variation of auditing one named current condition with a new semantic counterexample; the obligation and its rule wording are unchanged from CrocSwap/integer-mult-bounds#1091.", "bottleneck_link": "Closing a current acceptance gap or proof obligation strengthens reliability even without changing kappa; the selected supplier is complex-bound and its hosting soundness supports every downstream packing claim.", "budget_minutes": 60, "stop_rule": "One obligation, one minimal one-integer counterexample battery, one enforcement trace; kill if the reproduce path already enforces X2 or if the mutation cannot be made single-locus.", "outcome": "completed", - "evidence": "research/owner-x2-acceptance-boundary/RESULT.json (PASS_PR1094_X2_ACCEPTANCE_BOUNDARY_AUDIT): X2 is enforced only by the review-time composition check_frontier1094.py; make frontier1094-verify and community-batch1099.yml CI do not re-run it for CrocSwap/integer-mult-bounds#1094; a one-integer DATA-PHASES mutation (child 1 port 0 axis 131072 -> 13) preserves all aggregates, is accepted by the complete R1-R7/X1 rule set, and is rejected only at X2; first X2-directed rejection controls supplied.", + "evidence": "research/owner-x2-acceptance-boundary/RESULT.json (PASS_PR1094_X2_ACCEPTANCE_BOUNDARY_AUDIT): X2 is not recomputed semantically by make frontier1094-verify or community-batch1099.yml CI for CrocSwap/integer-mult-bounds#1094; it is checked only by the review-time composition check_frontier1094.py. A one-integer DATA-PHASES mutation (child 1 port 0 axis 131072 -> 13) preserves all aggregates, is accepted by the complete R1-R7/X1 semantic rule set (in-memory) and is rejected semantically only at X2. This is a missing-semantic-recomputation gap, not demonstrated end-to-end acceptance of a mutated pinned input: executed against the real source-bound entrypoints, the mutated pinned bytes are rejected at the source-hash pins before any semantic rule runs (check_frontier1094.py line 19, owner audit line 359), and full mutated-chain acceptance was not executed. First X2-directed rejection controls supplied.", "author": "Navinor", "ai_assistance": "Substantial AI assistance: task selection, trace, harness and text drafted with help from opencode (OpenCode agent harness).", "open_questions": [ { "question": "Should scripts/verify_frontier1094.py execute the pinned check_frontier1094.py composition so the record reproduce command enforces X2 for CrocSwap/integer-mult-bounds#1094?", - "why_it_matters": "Selected hosting soundness currently rests on a review-time run the reproduce path does not repeat.", + "why_it_matters": "Selected hosting soundness currently rests on a review-time run the reproduce path does not repeat; the hash pins stop mutated pinned inputs, but a defect introduced at generation time and re-pinned self-consistently would need semantic recomputation to catch.", "first_step": "Add the composition as a verify_frontier1094.py stage and measure replay time.", "blocked_by": "Maintainer authorization to change the selected reproduction path." }, @@ -60,13 +60,13 @@ "question": "Which other batch1099 obligations are enforced only at review time?", "why_it_matters": "Same replay-coverage class as CrocSwap/integer-mult-bounds#1277 (ancestry); an obligation-by-obligation table would localize every gap.", "first_step": "Enumerate rules R1-R7/X1/X2 and the pricing identities against each checker on the reproduce path.", - "blocked_by": null + "blocked_by": "Nothing; this is a natural continuation." }, { - "question": "Does the frozen upstream1087 chain accept the M1 fixture end to end?", - "why_it_matters": "Would replace the code-trace blindness claim with execution.", - "first_step": "Run make frontier1094-verify with --baseline1042 reuse and the mutated phases overlaid.", - "blocked_by": "Published frontier1042 baseline artifacts and cold replay time were outside this session budget." + "question": "Would the frozen upstream1087 chain accept a mutated fixture end to end below the hash pins?", + "why_it_matters": "Would replace the remaining code-trace claim (frozen indep16/audit_allcold carry no cross-child pending-axis rule) with execution; note the mutated pinned input itself is already rejected at the source-hash pins before the semantic rules run.", + "first_step": "Run make frontier1094-verify with --baseline1042 reuse and the mutated phases re-pinned consistently at generation time.", + "blocked_by": "Published frontier1042 baseline artifacts and cold replay time were outside this session budget; full mutated-chain acceptance remains unexecuted." } ] } \ No newline at end of file diff --git a/research/owner-x2-acceptance-boundary/VERIFY.json b/research/owner-x2-acceptance-boundary/VERIFY.json index 818f8251e3..c2da318ee2 100644 --- a/research/owner-x2-acceptance-boundary/VERIFY.json +++ b/research/owner-x2-acceptance-boundary/VERIFY.json @@ -1,10 +1,13 @@ { "schema_version": 1, - "status": "passing", + "status": "ready", "python": "3.12", "requirements": [], "inputs": [ - "research/community-batch1099-audit/check_frontier1094.py" + "research/community-batch1099-audit/check_frontier1094.py", + "research/t16-owner-audit-seed67/verify.py", + "research/t16-owner-audit-seed67/SOURCES.json", + "research/community-k492-audit/pr622/replay/baseline558/complex-global/base/work/complex-nine-native/DATA-PHASES.json" ], "commands": [ { @@ -14,7 +17,7 @@ "{package}/verify.py" ], "timeout_seconds": 600, - "checks": "Positive control: pinned CrocSwap/integer-mult-bounds#1094 inputs pass the full R1-R7/X1/X2 owner audit. Failure controls: M1 one-integer cross-child axis mutation rejected at X2 with single-locus and rank-preservation guards; M2 within-child duplicate rejected at X2; M1/M2 loci differ. Blindness: X2 need() suppressed, geometry identical and R1-R7/X1 accept M1. Coverage: 11 owner-audit and 6 frozen indep16 controls inventoried, zero X2-directed mutants before this package. Trace: reproduce target, verify_frontier1094.py, verify_selected_result.py, community-batch1099.yml, claim list 1022-1087 and frozen indep16/audit_allcold keying asserted as recorded." + "checks": "Positive control: pinned CrocSwap/integer-mult-bounds#1094 inputs pass the full R1-R7/X1/X2 owner audit. Failure controls: M1 one-integer cross-child axis mutation rejected at X2 with single-locus and rank-preservation guards; M2 within-child duplicate rejected at X2; M1/M2 loci differ. Blindness (semantic layer only, in-memory): X2 need() suppressed, geometry identical and R1-R7/X1 accept M1. Source-bound acceptance path (executed): the M1 mutation applied to a scratch copy of the pinned bytes is rejected by both source-bound entrypoints at their DATA-PHASES hash pins (check_frontier1094.py line 19, owner audit line 359) before geometry()/X2 runs, while intact bytes pass the pins and reach later code; record-manifest coverage of the vendored DATA-PHASES copies and frozen-chain emit-time hash binding asserted as recorded. Coverage: 11 owner-audit and 6 frozen indep16 controls inventoried, zero X2-directed mutants before this package. Trace: reproduce target, verify_frontier1094.py, verify_selected_result.py, community-batch1099.yml, claim list 1022-1087 and frozen indep16/audit_allcold keying asserted as recorded." } ] -} \ No newline at end of file +} diff --git a/research/owner-x2-acceptance-boundary/verify.py b/research/owner-x2-acceptance-boundary/verify.py index b9c82219e5..acc319bb27 100644 --- a/research/owner-x2-acceptance-boundary/verify.py +++ b/research/owner-x2-acceptance-boundary/verify.py @@ -29,13 +29,24 @@ list. geometry() must reject at X2 as well. 4. Blindness: with only the X2 need() suppressed, geometry() returns an identical geometry object and the complete R1-R7/X1 rule set accepts the - M1 fixture. The X2 rule is the only rule that reads pending axes. + M1 fixture. The X2 rule is the only rule that reads pending axes. This is + a semantic-layer measurement on in-memory mutated bytes; it is not an + end-to-end acceptance claim for a mutated pinned input (see 7). 5. Coverage inventory: the existing 11 owner-audit controls and the frozen verifier's 6 independent-t16 controls contain no X2-directed mutant. 6. Enforcement trace (static, recorded with exact excerpts): the selected reproduce command and the CI workflow do not execute the CrocSwap/integer-mult-bounds#1094 owner composition, and the frozen CrocSwap/integer-mult-bounds#1087 verifier chain keys hosted cells per (owner, child, port), so cross-child cell sharing is outside its rule set. + 7. Source-bound acceptance path (executed): the hash/pin layer and the + semantic layer are distinguished. The M1 mutation is applied to a copy of + the pinned DATA-PHASES bytes in a scratch tree and the real source-bound + entrypoints are run against it: both reject the mutated pinned input at + their source-hash pins before any semantic rule runs, while intact bytes + pass the pins and reach the semantic layer. Missing semantic + recomputation on the reproduce path is therefore not the same as + end-to-end acceptance of a mutated pinned input; full mutated-chain + acceptance remains unexecuted (RESULT.json, README). Unrun obligations are listed in RESULT.json and the README. """ @@ -44,9 +55,13 @@ import hashlib import importlib.util import json +import os import re +import shutil +import subprocess import sys import tarfile +import tempfile from pathlib import Path HERE = Path(__file__).resolve().parent @@ -288,6 +303,115 @@ def need_x2_suppressed(ok, rule, msg): require('orthogonal_axes' in frozen['code/audit_allcold.py'] and 'len(pend)==prank[i]' in frozen['code/audit_allcold.py'], 'audit_allcold pending-axis read changed') +# ------------------------------------------------- 7. source-bound acceptance path + +# 7a. Code order: both source-bound entrypoints that read the fixture hash-pin +# its bytes before any semantic rule can see them. +cf_text = text(ROOT / 'research/community-batch1099-audit/check_frontier1094.py') +cf_lines = cf_text.splitlines() +cf_pin = next(i for i, line in enumerate(cf_lines, 1) if 'data_phases_sha256' in line) +cf_geo = next(i for i, line in enumerate(cf_lines, 1) if 'a.geometry(' in line) +cf_spec = next(i for i, line in enumerate(cf_lines, 1) if "'data/SPEC.json'" in line) +require(cf_pin < cf_geo, 'composition must pin DATA-PHASES before geometry') + +audit_text = text(ROOT / 'research/t16-owner-audit-seed67/verify.py') +audit_lines = audit_text.splitlines() +audit_pin = next(i for i, line in enumerate(audit_lines, 1) if 'data_phases_sha256' in line) +audit_geo = next(i for i, line in enumerate(audit_lines, 1) if 'geo = geometry(' in line) +audit_blob = next(i for i, line in enumerate(audit_lines, 1) if "'cat-file'" in line) +audit_claims = next(i for i, line in enumerate(audit_lines, 1) if 'get = {name: load(blob(' in line) +require(audit_pin < audit_geo, 'owner audit must pin DATA-PHASES before geometry') + +# 7b. Record/manifest layer: what scripts/verify_selected_result.py covers. +selected = read(ROOT / 'certificates/selected-result.json') +source_manifest = read(ROOT / selected['source_manifest']) +fixture_under_root = any(a.PHASES.startswith(root + '/') for root in source_manifest['package_roots']) +phase_copies = sorted((name, digest) for name, digest in source_manifest['files'].items() + if name.endswith('DATA-PHASES.json')) +require(not fixture_under_root, 'audit fixture unexpectedly covered by the record package roots') +require(phase_copies and all(digest == pins['data_phases_sha256'] for _, digest in phase_copies), + 'vendored DATA-PHASES copies must be pinned at the fixture digest') +require(selected['proof_supplements']['research/community-batch1099-audit/check_frontier1094.py'] + == sha(ROOT / 'research/community-batch1099-audit/check_frontier1094.py'), + 'proof_supplements must pin the composition bytes') + +# 7c. Frozen chain: emit-time self-consistency binding, not an external pin. +require('source_artifacts' in frozen['code/emit_allcold.py'] + and 'exact_data_phase_recipe_sha256' in frozen['code/audit_allcold.py'], + 'frozen chain DATA-PHASES binding changed') + +# 7d. Executed: run the real source-bound entrypoints against the M1-mutated +# pinned bytes (one integer token replaced in a scratch copy; tracked files +# untouched) and against intact bytes. The mutated run must stop at the hash +# pin before geometry(); the intact run must pass the pins and reach later code. +raw_phases = (ROOT / a.PHASES).read_bytes() +text_phases = raw_phases.decode('utf-8') +require(candidate['c2_index'] == 0, 'text-locus search assumes the first axes slot') +anchor = '{"orthogonal_axes":[' + str(before) +anchor_at = text_phases.find(anchor, text_phases.find('"recipes":')) +require(anchor_at > 0, 'M1 text locus not found') +token_at = anchor_at + len('{"orthogonal_axes":[') +require(text_phases[token_at:token_at + len(str(before))] == str(before), 'M1 text token') +mut_phases = (text_phases[:token_at] + str(value) + text_phases[token_at + len(str(before)):]).encode('utf-8') +require(json.loads(mut_phases) == phases_m1, 'text mutation must equal the in-memory M1 fixture') +require(len(raw_phases) - len(mut_phases) == len(str(before)) - len(str(value)), 'M1 text byte delta') + +scratch = Path(tempfile.mkdtemp(prefix='x2-boundary-')) +run_receipts = [] +try: + def stage(relative, data): + target = scratch / relative + target.parent.mkdir(parents=True, exist_ok=True) + target.write_bytes(data) + + stage('research/t16-owner-audit-seed67/verify.py', audit_text.encode('utf-8')) + stage('research/t16-owner-audit-seed67/SOURCES.json', + (ROOT / 'research/t16-owner-audit-seed67/SOURCES.json').read_bytes()) + stage('research/t16-owner-audit-seed67/inputs/k8-seven-slot-word.json.gz', a.WORD.read_bytes()) + stage(a.TEMPLATE, (ROOT / a.TEMPLATE).read_bytes()) + stage('research/community-batch1099-audit/check_frontier1094.py', cf_text.encode('utf-8')) + + def run(label, entry, argv, phases_bytes): + stage(a.PHASES, phases_bytes) + env = dict(os.environ, PYTHONUTF8='1', PYTHONDONTWRITEBYTECODE='1') + env.pop('PYTHONOPTIMIZE', None) + proc = subprocess.run([sys.executable, '-B', str(scratch / entry), *argv], cwd=scratch, + capture_output=True, env=env) + out = (proc.stdout + proc.stderr).decode('utf-8', 'replace').replace(str(scratch), '') + basename = entry.rsplit('/', 1)[-1] + frames = [int(line) for file_, line in + re.findall(r'File "[^"]*[/\\]([^"\\/]+\.py)", line (\d+)', out) if file_ == basename] + require(proc.returncode != 0, label + ' must fail') + run_receipts.append(dict(label=label, entrypoint=entry, exit_code=proc.returncode, + traceback_frames=sorted(set(frames)), + fail_marker=[line for line in out.splitlines() if line.startswith('FAIL ')])) + return out, frames + + composition = 'research/community-batch1099-audit/check_frontier1094.py' + owner_audit = 'research/t16-owner-audit-seed67/verify.py' + require('DATA-PHASES hash' in audit_lines[audit_pin - 1], 'pin line must carry the FAIL marker') + + out1, frames1 = run('composition_m1_mutated_pinned_input', composition, ['x.json', 'y.json'], mut_phases) + require('Independent PR1094 check failed' in out1 and cf_pin in frames1 and cf_geo not in frames1 + and all(line <= cf_pin for line in frames1), + 'composition must reject M1 at the DATA-PHASES hash pin before geometry, frames: %s' % frames1) + + out2, frames2 = run('owner_audit_m1_mutated_pinned_input', owner_audit, ['--repo', str(scratch)], mut_phases) + require('FAIL input: DATA-PHASES hash' in out2 and 'PASS' not in out2, + 'owner audit must reject M1 at the DATA-PHASES hash pin, output: ' + out2) + + out3, frames3 = run('composition_intact_control', composition, ['x.json', 'y.json'], raw_phases) + require('FileNotFoundError' in out3 and cf_spec in frames3 + and 'Independent PR1094 check failed' not in out3, + 'intact composition control must pass the pins and geometry, frames: %s' % frames3) + + out4, frames4 = run('owner_audit_intact_control', owner_audit, ['--repo', str(scratch)], raw_phases) + require('CalledProcessError' in out4 and audit_blob in frames4 + and 'FAIL input: DATA-PHASES hash' not in out4, + 'intact owner-audit control must pass the pins and geometry, frames: %s' % frames4) +finally: + shutil.rmtree(scratch, ignore_errors=True) + # ---------------------------------------------------------------- result result = dict( @@ -317,18 +441,58 @@ def need_x2_suppressed(ok, rule, msg): rejected_by=rejects, cell_collision_witness=witness), blindness=dict( - method='X2 need() suppressed only to measure what the remaining rule set sees', + method='X2 need() suppressed only to measure what the remaining semantic rule set sees; ' + 'in-memory mutated bytes, not an end-to-end acceptance claim for a mutated pinned input', geometry_identical=geo_m1_x2suppressed == geo0, rule_set_accepts=owned_m1 == owned0, - rule_set='R1-R7 plus X1 (owner-audit rule bodies)'), + rule_set='R1-R7 plus X1 (owner-audit rule bodies), semantic layer only'), + source_bound_acceptance=dict( + claim_scope='Missing semantic recomputation on the reproduce path is demonstrated; end-to-end ' + 'acceptance of a mutated pinned input is not. The semantic rule set does not reject M1 ' + '(executed in memory), but the source-hash layer rejects the mutated pinned bytes before ' + 'any semantic rule runs (executed at both source-bound entrypoints). Full mutated-chain ' + 'acceptance was not executed.', + layer_order=['record/manifest hashes (scripts/verify_selected_result.py)', + 'source input pins (check_frontier1094.py, t16-owner-audit-seed67/verify.py)', + 'semantic rules (R1-R7/X1, X2; frozen indep16/audit_allcold)'], + record_manifest_layer=dict( + script='scripts/verify_selected_result.py', + fixture_covered_by_package_roots=fixture_under_root, + fixture_note='the top-level audit fixture is outside the record manifest package roots, so this ' + 'layer alone neither accepts nor rejects it; it is pinned separately by ' + 'research/t16-owner-audit-seed67/SOURCES.json inputs.data_phases_sha256', + vendored_phase_copies_pinned=[name for name, _ in phase_copies], + vendored_phase_copies_digest=pins['data_phases_sha256'], + composition_pinned_by_proof_supplements=True), + input_pin_layer=dict( + pins_from='research/t16-owner-audit-seed67/SOURCES.json inputs.data_phases_sha256', + composition=dict(script='research/community-batch1099-audit/check_frontier1094.py', + pin_line=cf_pin, geometry_line=cf_geo, + order='hash pin before geometry()/X2'), + owner_audit=dict(script='research/t16-owner-audit-seed67/verify.py', + pin_line=audit_pin, geometry_line=audit_geo, + order='hash pin before geometry()/X2')), + executed=dict( + mutation='one integer token %d -> %d at byte offset %d (recipes[0].idle_children[1].' + 'orthogonal_axes[0]); equals the in-memory M1 fixture; tracked files untouched, ' + 'scratch tree deleted' % (before, value, token_at), + byte_delta=len(raw_phases) - len(mut_phases), + runs=run_receipts), + frozen_chain_layer=dict( + binding='emit_allcold.py records source_artifacts sha at emit time; audit_allcold.py asserts ' + 'template exact_data_phase_recipe_sha256 equals the current file sha (self-consistency ' + 'binding, not an external pin to the frozen digest)', + semantic_gap='no cross-child pending-axis rule (code trace)')), control_inventory=dict(owner_audit_controls=control_names, frozen_independent_t16_controls=indep_controls, x2_directed_mutants_before_this_package=0), enforcement_trace=dict( reproduce_target=target.strip().splitlines(), reproduce_stages=['historical-source', 'baseline1042-cold (or baseline reuse)', 'rare-pattern-exchanges'], - selected_record_check='scripts/verify_selected_result.py validates the selected record and its ' - 'proof_supplement hashes; it imports no subprocess module and executes no composition', + selected_record_check='scripts/verify_selected_result.py validates the selected record, its certificate, ' + 'the SELECTED-SOURCE package inventory and its proof_supplement hashes; it imports no ' + 'subprocess module and executes no composition; the top-level audit fixture is outside ' + 'its package roots (see source_bound_acceptance.record_manifest_layer)', ci_workflow='.github/workflows/community-batch1099.yml runs research/t16-owner-audit-seed67/verify.py --fetch ' '(its pinned claim list excludes the selected supplier) and check_pr1048_counterexample.py; ' 'it does not run check_frontier1094.py', @@ -338,8 +502,13 @@ def need_x2_suppressed(ok, rule, msg): '(owner, child, port); audit_allcold asserts only len(pending) == rank per child', ), unrun_obligations=[ - 'Full make frontier1094-verify cold replay with the M1-mutated DATA-PHASES (needs the frontier1042 cold baseline; ' - 'out of session budget). Acceptance of M1 by the frozen chain is established by code trace, not by execution.', + 'Full make frontier1094-verify cold replay with the M1-mutated DATA-PHASES (needs the frontier1042 cold ' + 'baseline; out of session budget), so end-to-end acceptance of a mutated pinned input is not claimed and ' + 'the structural-blindness claim is limited to missing semantic recomputation. What is executed: the semantic ' + 'layer accepts M1 in memory (R1-R7/X1) and rejects at X2, and the source-bound entrypoints reject the ' + 'mutated pinned bytes at their source-hash pins before any semantic rule runs. The frozen chain carries no ' + 'cross-child pending-axis rule (code trace); its DATA-PHASES hash handling is an emit-time self-consistency ' + 'binding, not an external pin.', 'No T8/T16 claim other than CrocSwap/integer-mult-bounds#1094 was re-audited; the historical owner-boundary-audit package was not rerun.', 'No kappa, supplier adoption, or multiplication-theorem claim is made or tested here.', ],