From f011d03633f0570257b653e7aa1e869b1b06d06a Mon Sep 17 00:00:00 2001 From: Tekalign <152792726+tekuuu@users.noreply.github.com> Date: Tue, 13 Oct 2026 06:40:57 +0300 Subject: [PATCH] Audit PR626 owner boundaries and bridge omission sensitivity --- research/owner-boundary-audit/CLAIM.json | 24 ++ research/owner-boundary-audit/EXPECTED.json | 257 +++++++++++++ research/owner-boundary-audit/README.md | 123 +++++++ research/owner-boundary-audit/REVIEW.md | 192 ++++++++++ research/owner-boundary-audit/SOURCES.json | 20 + research/owner-boundary-audit/VALIDATION.json | 43 +++ research/owner-boundary-audit/verify.py | 346 ++++++++++++++++++ 7 files changed, 1005 insertions(+) create mode 100644 research/owner-boundary-audit/CLAIM.json create mode 100644 research/owner-boundary-audit/EXPECTED.json create mode 100644 research/owner-boundary-audit/README.md create mode 100644 research/owner-boundary-audit/REVIEW.md create mode 100644 research/owner-boundary-audit/SOURCES.json create mode 100644 research/owner-boundary-audit/VALIDATION.json create mode 100644 research/owner-boundary-audit/verify.py diff --git a/research/owner-boundary-audit/CLAIM.json b/research/owner-boundary-audit/CLAIM.json new file mode 100644 index 0000000000..6d455b894d --- /dev/null +++ b/research/owner-boundary-audit/CLAIM.json @@ -0,0 +1,24 @@ +{ + "track": "adversarial mathematical audit", + "assignment_seed": 60, + "seed_source": "Python secrets.randbelow(100), operating-system randomness", + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "selected_kappa": "51110230636731/31250000000000000", + "object": "PR626 whole-owner availability at local-call, bridge, and idle-completion boundaries", + "method": "Independent event traversal of the inherited physical controller; enumerate every owner-replica/child/call eligibility and check all 35,424 literal roles; boundary mutations and shared-call negative controls", + "deliverable": "Scoped mathematical audit note, standalone standard-library checker, source pins and deterministic receipt; no new kappa", + "expected_finish_utc": "2026-10-13T03:53:30Z", + "coordination": "No pinned issues returned by GitHub GraphQL; no open sprint issue found. Local claim used as instructed.", + "candidates": [ + "Cyclic inverse infinity-norm transfer: not selected; #621 review and #628/#663 overlap", + "Cold-helper restoration: not selected; #617/#633 and #663 overlap", + "Whole-owner boundary timing: selected; event-state method distinct from PR626's interval-reconstruction and PR553's historical formal instance" + ], + "scope_exclusions": "No native provider reconstruction, allocation optimization, global-frontier edits, or all-size/analytic proof", + "status": "completed", + "completed_at_utc": "2026-10-13T03:40:57.640413+00:00", + "result": "All 10,368 eligibility decisions and 35,424 selected roles pass; 2,736 roles use closing blocks. All 72 single bridge deletions preserve timing admission but break the normalized scalar identity. Added nine exact scalar witnesses and 956 rejection controls; no new kappa.", + "result_link": "https://github.com/tekuuu/integer-mult-bounds/tree/audit/seed60-owner-boundaries/research/owner-boundary-audit", + "overlap_refresh": "2026-10-13T03:38Z: no pinned coordination issue; PR553 historical proof remains credited, new PRs through671 do not duplicate this current-table timing/scalar comparison.", + "verification": "Normal and optimized standalone checks match EXPECTED byte-for-byte; selected-record-check and staged whitespace check pass; see VALIDATION.json." +} diff --git a/research/owner-boundary-audit/EXPECTED.json b/research/owner-boundary-audit/EXPECTED.json new file mode 100644 index 0000000000..8111e351fe --- /dev/null +++ b/research/owner-boundary-audit/EXPECTED.json @@ -0,0 +1,257 @@ +{ + "status": "PASS_PR626_NEXT_TOUCH_BOUNDARY_AUDIT", + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "assignment_seed": 60, + "replica_events": 240, + "idle_deadlines_including_zero_rank": 160, + "nonzero_windows": 144, + "eligibility_decisions": 10368, + "admitted_decisions": 2958, + "eligibility_sha256": "558ada03e26384a2068f9847473c881e3cfbbd9b27882f8b46e4c66d8d0f886f", + "roles": 35424, + "cross_replica_roles": 28404, + "occupied_owner_groups": 13913, + "closing_block_admitted_child_calls": 144, + "closing_block_helper_roles": 2736, + "valid_roles_rejected_if_borrower_replica_is_used": 12614, + "negative_controls": { + "deadline_before_call": 144, + "intervening_bridge_destination": 144, + "intervening_bridge_source": 144, + "same_family_disjoint_coordinates": 1, + "unknown_event": 1, + "window_endpoint_shift": 522 + }, + "bridge_deletion_sensitivity": { + "nonterminal_no_change": 48, + "terminal_no_change": 24 + }, + "scalar_bridge_omission_counterexamples": [ + { + "source_event": 3, + "input_basis_column": 0, + "actual_output": [ + 1, + 0, + 0, + 1, + 0, + 0, + 0, + 0 + ], + "expected_output": [ + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "changed_matrix_entries": 4 + }, + { + "source_event": 6, + "input_basis_column": 0, + "actual_output": [ + 1, + 0, + 0, + -1, + 0, + 0, + 0, + 0 + ], + "expected_output": [ + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "changed_matrix_entries": 3 + }, + { + "source_event": 9, + "input_basis_column": 1, + "actual_output": [ + 0, + 1, + 0, + 0, + 0, + -1, + 0, + 0 + ], + "expected_output": [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "changed_matrix_entries": 6 + }, + { + "source_event": 12, + "input_basis_column": 2, + "actual_output": [ + 0, + 0, + 1, + 0, + 0, + -1, + 0, + 0 + ], + "expected_output": [ + 0, + 0, + 1, + 0, + 0, + 0, + 0, + 0 + ], + "changed_matrix_entries": 3 + }, + { + "source_event": 15, + "input_basis_column": 1, + "actual_output": [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 1 + ], + "expected_output": [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "changed_matrix_entries": 8 + }, + { + "source_event": 18, + "input_basis_column": 4, + "actual_output": [ + 0, + 0, + 0, + 0, + 1, + 0, + 0, + -1 + ], + "expected_output": [ + 0, + 0, + 0, + 0, + 1, + 0, + 0, + 0 + ], + "changed_matrix_entries": 3 + }, + { + "source_event": 25, + "input_basis_column": 1, + "actual_output": [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + -1 + ], + "expected_output": [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "changed_matrix_entries": 6 + }, + { + "source_event": 26, + "input_basis_column": 1, + "actual_output": [ + 0, + 1, + 0, + 0, + 0, + 1, + 0, + 0 + ], + "expected_output": [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "changed_matrix_entries": 4 + }, + { + "source_event": 27, + "input_basis_column": 1, + "actual_output": [ + 0, + 1, + 0, + -1, + 0, + 0, + 0, + 0 + ], + "expected_output": [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "changed_matrix_entries": 2 + } + ], + "scope": "Finite pinned PR626 controller and literal owner roles; native widths, normalized residual semantics, atomic calls and all-size realization are inherited, not re-proved. No new kappa." +} diff --git a/research/owner-boundary-audit/README.md b/research/owner-boundary-audit/README.md new file mode 100644 index 0000000000..aaf6510a37 --- /dev/null +++ b/research/owner-boundary-audit/README.md @@ -0,0 +1,123 @@ +# PR626 owner boundaries and the bridge-omission blind spot + +**Adversarial mathematical audit; no new κ.** The selected whole-owner +allocation passes an independent event-state check. Its timing predicate +alone nevertheless cannot certify the presence of any of the 72 bridges: +deleting any one leaves all borrowing windows unchanged, while changing +the normalized scalar data map. The selected production audit separately +binds the full controller; this is **not** a reported acceptance bug in it. + +Prepared for **Tekalign / tekuuu** with substantial OpenAI Codex assistance, +including a separate agent's review. Apache-2.0. This is not independent +human peer review. + +## Reproduce + +From the repository root, using only Python's standard library: + +```sh +python3 -I -O -B research/owner-boundary-audit/verify.py +``` + +Expected status: `PASS_PR626_NEXT_TOUCH_BOUNDARY_AUDIT`. The deterministic +output must equal [EXPECTED.json](EXPECTED.json), including: + +| Check | Completed coverage / result | +| --- | --- | +| Controller | All 240 replica events; 160 idle deadlines, including 16 zero-rank deadlines | +| Nonzero pending children | 144 owner-replica/child windows | +| Eligibility | All 10,368 window/call decisions; 2,958 admitted | +| Literal allocation | All 35,424 helpers; 28,404 cross-replica roles | +| Same-block deadlines | All 144 deadline-block calls admitted; 2,736 actual roles use them | +| Wrong-replica diagnostic | Using the borrower's replica rejects 12,614 valid roles | +| Rejection controls | 522 endpoint changes, 144 moved deadlines, 288 inserted bridges (both endpoints), whole-family aliasing, unknown event | +| Omitted literal bridges | All 72 single deletions leave eligibility unchanged | +| Scalar counterexamples | All nine source bridge deletions change the exact eight-wire map; each applies independently to all eight replicas | + +The source pins are checked before any computation. Checks remain active +under `-O`. To regenerate a receipt after an intentional code change, use +`--write /absolute/path/to/receipt.json`, then inspect its difference from +the committed receipt. Normal verification writes no files. + +## Precise statement and method + +For the finite controller and owner table pinned below, every selected +helper role belongs to its owner's pending region strictly between that +region's last data touch and its idle deadline. No two helpers in one +complete invocation own the same physical family, no helper aliases the +active data pair, and their allocated pending coordinate sets are disjoint. + +The existing source audit reconstructs last-touch intervals. This checker +instead scans the explicit event stream backward. For each physical +replica/pair it records whether the next relevant event is an idle deadline +or a blocking data touch. A local event blocks its active pair before +sampling admissibility. It then compares the complete Boolean matrix with +the stored windows, and checks every literal owner against that matrix. +It imports no emitter, allocator, original audit, or scalar replay module. +See [REVIEW.md](REVIEW.md) for the induction and conditional timing argument. + +Strict event positions cannot be replaced by strict block times. For +owner replica 0, child 0 permits times `{0,1,2}`: its idle event follows the +local call of block 2. The same block's subsequent bridge releases child 1, +whose times are `{3,4,5}`. Actual selected roles exercise both closing +boundaries. The controls move deadlines before calls and insert physical +touches after formerly legal calls; they do not manufacture an impossible +call at the same event position as an idle or bridge. + +The bridge-deletion experiment is a scoped counterexample to the inference +“the borrowing windows agree, therefore the scalar controller is correct.” +It is not a counterexample to the selected certificate. In the inherited +normalized eight-wire contract, the full recipe is the identity. Removing +source bridge 3 maps input `(1,0,0,0,0,0,0,0)` to +`(1,0,0,1,0,0,0,0)`. The receipt gives an exact input/output witness for +each of the nine source bridges. Each matrix factor is invertible and each +bridge is nonidentity, so deleting a single bridge from an identity product +cannot preserve that product. This explains why source projection and +scalar checks must accompany a timing certificate. + +## Pins, selection and bounded coverage + +- Exact main base: `66849e1475c930fd7732b1a0067ffee7e1e95f60`. +- Selected at that base: #626 with #543, + `κ = 51110230636731/31250000000000000 = 0.001635527380375392`. +- Reviewed #626 source: `660de893d27bb7abd1d5b01b1640207528a5c851`. +- All consumed artifacts and semantic reference code: [SOURCES.json](SOURCES.json). + The inherited archived controller, phases, owner table and plan are bound + to `research/community-k492-audit/SELECTED-SOURCE.json`. The checker also + compares the archived controller's recipe, idle children and first 30 + events with the actual frozen558 input installed by `run_complex44.py`. + It does not identify those full parent templates, whose final bank events + differ, or pretend to cold-rebuild either supplier. +- Assignment seed **60**, drawn with OS-backed `secrets.randbelow(100)`: + adversarial audit. It also chooses the legal call used for each inserted + bridge control by index `60 % len(window)`. +- [CLAIM.json](CLAIM.json) records the three candidates and local claim. + No pinned coordination issue or open sprint issue was available. +- Stopping rule: finish this finite table, all its window/call combinations, + all single bridge deletions, and the stated controls; no parameter search, + supplier optimization, or additional speculative investigation. + +## Scope, credit and handoff + +This audits a necessary finite interface. It inherits the source supplier +widths, phase/frame identities, exact normalized residual and spectator +restoration, atomic execution, common labels, mutable-basis realization, +full invoice, all-size compiler, precision/tape/exact recovery and analytic +assumptions. It does not re-prove native local programs, price a new +recurrence, establish global optimality, or formally verify multiplication. + +Credit: chafreaky's #626 owner repair; jeremykothe2's #622/#623 constructions +and allocations; GamingPuzzled's #620 owner-map lead; DreamingOfClouds and +the earlier supplier lineage; icekylinx's inherited controller/scalar +replays, with their recorded AI assistance. Source notices remain intact. +Rohan Arun's open [#553](https://github.com/CrocSwap/integer-mult-bounds/pull/553) +at `0c3e5ee4719d705afd63fefd001091d70e55182b` already formalizes the historical +PR531 table's 144 strict windows. This contribution adds the current +492-helper data, a separate next-touch implementation, actual closing-block +usage counts, and the paired timing/scalar omission evidence. It claims no +priority for the strict-window principle or eight-wire identity. + +All changes are confined to this research package. `upstream/`, the selected +frontier and predecessor implementations remain unchanged. Reviewers can +run the command above and inspect the nine short exact counterexamples; +no expensive supplier replay is needed for this scoped addition. diff --git a/research/owner-boundary-audit/REVIEW.md b/research/owner-boundary-audit/REVIEW.md new file mode 100644 index 0000000000..a9b820ca8c --- /dev/null +++ b/research/owner-boundary-audit/REVIEW.md @@ -0,0 +1,192 @@ +# Event-boundary argument and independent review + +This is a finite review of the selected PR626 owner's timing interface at +base `66849e1475c930fd7732b1a0067ffee7e1e95f60`. It makes no new bound claim. + +## Review of the separate checker + +The checker uses a reverse scan, rather than importing the emitter or +reconstructing the source audit's last-touch intervals. The invariant is: +immediately before a position is sampled in reverse order, the state for +each `(replica, pair)` names the first future relevant event on that pair, +if that event is an idle deadline; otherwise it is blocked. An idle sweep +sets its two children. A bridge blocks both its source and destination. +A local sweep blocks its own data pair **before** sampling helper +eligibility. Terminal events conservatively block the replica. The reverse +induction follows directly from these cases, so the state sampled at a +local call includes exactly the pending children whose next data event is +their completion. On this pinned source there is a touch between distinct +positive-child sweeps on the same pair. Thus the invariant gives the same +strict event-position intervals as the source check. + +The checker received a separate OpenAI Codex agent review and an independent +run of `python3 -I -O research/owner-boundary-audit/verify.py`: it passed all 10,368 +eligibility comparisons and all 35,424 roles, including 28,404 +cross-replica roles. The optimized run confirms the checks are not disabled +by Python's assertion optimization. Its same-family mutation uses two +width-9 helpers at offsets 0 and 9 in a rank-32 child, so those residual +coordinate sets really are disjoint and within capacity; its rejection +tests the stronger whole-family requirement. + +The source-chain review also checked the frozen558 setup: +`run_complex44.py` installs `ROUND20-PARENT-TEMPLATE.json.gz`, then +`prepare_supplier_base.py` preserves `recipe`, `idle_children`, and the +first 30 schedule events and copies `DATA-PHASES.json`. Those three +controller fields equal the archived direct-delivery parent used here; +their schedules differ only in final bank events 30 and 31, which occur +after all sampled calls. The phase files are byte-identical. This equality is +necessary to justify using the small archived input without rebuilding +the native suppliers. It is not a claim that the complete archived +template equals the selected generated template. + +## What the interval condition establishes + +Fix an owner replica and a positive-rank idle child. Its physical pair and +side are read from that child's `idle_cover_sweep`. Let `d` be the position +of that sweep in the expanded controller, and let `a` be the most recent +position before `d` at which a local sweep uses that pair, or a bridge uses +it as either source or destination. Use `a = -1` if no such event exists. +The source audit accepts a borrower whose complete local sweep starts at +position `c` only when `a < c < d`. + +For the pinned controller, this condition is sufficient for the **timing +part** of whole-owner availability, subject to its inherited local +restoration and atomic-call contracts: + +1. Per-replica projection preserves all 30 source events, including both + endpoints of every bridge. Thus there is no source-data touch of the + owner's pair between `a` and `d`. Initial windows are already pending + before the first event. The positive children with later starts are + released by bridges in this selected controller. +2. Every local invocation completes, including its wrappers, before the + next controller event. Hence a borrow beginning strictly inside this + interval finishes before `d`, and cannot straddle another replica's + data event. +3. Distinct owner families within one invocation exclude both active-data + aliasing and simultaneous helper aliasing. Across invocations, exact + restoration of the spectator coordinates and disjoint paid residual + footprints are the separate obligations allowing repeated use of one + physical family. The interval check alone does not establish these. +4. Idle completion executes the remaining suffix only after those uses. + Source `terminal_Y_translations`, `terminal`, and whole-stock correction + occur after the positive-child deadlines. Omitting those event kinds + from the source audit's `last` table therefore creates no missing touch + inside this particular controller's borrowing intervals. This conclusion + must not be generalized to controllers that move such events earlier. + +Availability belongs to the **owner replica**. Testing it against the +invocation replica would be invalid for cross-replica borrows, even when +the stage numbers coincide. The source code correctly derives owner +replica, pair, side and port from the literal family identifier. + +## Event positions versus call times + +Strict inequalities above concern positions of individual controller +events. A block contains its local sweep first, then its replica-local +bridges and idle completions. Consequently the call at an idle completion's +block time is permitted; the call at a releasing bridge's block time is too +early. Treating both boundaries as open or both as closed in integer call +time changes the admitted set. + +The selected data make this distinction observable: + +| Owner replica / child | Release | Deadline | Admitted call times | +| --- | --- | --- | --- | +| 0 / 0 | Initial state | Event position 3, source event 2, block time 2 | 0, 1, 2 | +| 0 / 1 | Bridge at position 4, source event 3, block time 2 | Event position 10, source event 5, block time 5 | 3, 4, 5 | + +There are 112 actual child-0 helper roles at call time 2. One is stage 1, +invocation replica 0, helper 207, family 335, port 111, offset 7, width 9. +There are 111 actual child-1 helper roles at call time 5. Thus closing the +window before processing its deadline block's local call rejects selected +valid roles. Conversely opening child 1 at the beginning of block 2 admits +a call that precedes the bridge creating that pending region. + +No local sweep is literally the same event as a bridge or idle sweep. A +mutation from `<` to `<=` at those event-position boundaries cannot change +the finite set of local call positions on its own. Meaningful negative +controls must change event order, a release/deadline transition, or the +admitted call set. Rejection of an artificial equal-position call does not +establish an additional physical theorem. + +## Useful negative controls + +- Open a post-bridge child before its bridge, including the bridge's block + call. Child 1 at replica 0 / time 2 is a concrete witness. +- Close an initial child before the local call in its deadline block. + Child 0 at replica 0 / time 2 has actual selected roles as witnesses. +- Insert a bridge touching the owner pair between a formerly legal local + call and its idle deadline. The call must become inadmissible, whether + the owner is the source or destination. This exercises the barrier + transition directly. +- Use the borrower replica's state instead of the owner's state. This can + produce plausible windows while describing the wrong physical family. +- Use one physical family for two helper roles in the same call, including + disjoint residual offsets. A whole-family helper invocation still owns + its spectator coordinates; residual disjointness alone is insufficient. +- Present an unknown event kind. A standalone checker should fail closed, + rather than silently treating an unmodeled event as harmless. + +## A boundary test cannot establish bridge presence + +Deleting any **one of all 72 literal bridges** leaves the next-touch +admission matrix unchanged. This was checked separately during review. +At the call samples, an idle deadline immediately before the original +bridge, or a local barrier on the destination pair, already determines +the same admissibility. There is no intervening local call at which that +bridge alone changes the pending-child state. This is a concrete +limitation of the finite timing predicate, not a permission to remove +the bridge from the construction. + +The bridges implement the controller's data transformation, which is +outside the timing predicate. The exact source pins and preservation of +the source event projection remain necessary. The checker should retain +the unchanged-matrix deletion experiments as successful limitation +controls, and use inserted intervening bridges to test its source and +destination barrier transitions. A bridge-deletion experiment that +leaves this matrix unchanged is neither a construction improvement nor +a proof that the bridge is redundant. + +A small scalar check exposes the difference. Write the eight wires as +`(x_0,y_0,...,x_3,y_3)`. The retained interface has forward local action +`y_i += x_i`, reverse local action `x_i -= y_i`, bridge `(d,s,c)` action +`x_d += c*x_s; y_s -= c*y_d`, and terminal action +`(x_i,y_i) = (y_i,-x_i)`. These are the formulas already used in +`research/split-centres-global/code/complex_replay.py`; the scalar +identity and omission methodology are predecessor work, not new claims +of this audit. + +Composing the pinned recipe over the integers gives the identity matrix. +Deleting its first bridge instead makes entry `(0,2)` equal `-1` rather +than `0`: input `x_1 = 1`, all other wires zero, acquires an erroneous +`x_0 = -1`. Deleting each of the nine recipe bridges gives a nonidentity +matrix (the same calculation applies independently to each of the eight +replicas). This also follows algebraically: every event matrix is +invertible and every bridge `B` is nonidentity. If the original product +`QBP` is identity, the product `QP` obtained by deleting `B` cannot also +be identity, since multiplying `QP = QBP` by inverses would give `B = I`. +This is a finite scalar-interface fact; it does not validate the full +physical or all-size realization. + +## Predecessor and scope + +[PR553](https://github.com/CrocSwap/integer-mult-bounds/pull/553), inspected +at head `0c3e5ee4719d705afd63fefd001091d70e55182b`, already formalizes +strict interiors of 144 borrowing windows for the historical PR531 +504-helper ownership table and a projected 242-event controller. Its +description explicitly excludes physical implementation, atomic execution, +charts, exact scalar endpoints, and the uniform compiler. This audit does +not claim novelty for the strict-window principle, nor does it replace +those Lean certificates. Its distinct evidence targets the selected +PR626 492-helper table and checks the timing interface by a separate +event-state traversal and boundary controls. + +Credit: PR626 ownership repair by chafreaky with OpenAI Codex; PR622/PR623 +supplier and allocation work by jeremykothe2 and the credited Claude Code +agents; inherited PR531 ownership work by icekylinx; historical finite +formalization in PR553 by Rohan Arun with substantial OpenAI Codex +assistance. See the retained source packages' notices for the complete +ancestry. This review was prepared with substantial OpenAI Codex assistance +and is covered by the repository's Apache-2.0 license. It is an independent +reasoning pass within this automated contribution, not an independent +human audit or a formal proof of the multiplication theorem. diff --git a/research/owner-boundary-audit/SOURCES.json b/research/owner-boundary-audit/SOURCES.json new file mode 100644 index 0000000000..52e5220cf1 --- /dev/null +++ b/research/owner-boundary-audit/SOURCES.json @@ -0,0 +1,20 @@ +{ + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "reviewed_source_pr626": "660de893d27bb7abd1d5b01b1640207528a5c851", + "sha256": { + "research/community-k492-audit/SELECTED-SOURCE.json": "36e9e421230c4cb7b6a537d76a4bdfb6f667730d383e56062d4e45957484ab9e", + "research/direct-delivery504-global/inputs/data-base/split-centres/GLOBAL-TEMPLATE.json.gz": "5b913207775fcd87090cfa8776e8bd2bb872426923345fe1a1a4e1ea84bfae2c", + "research/direct-delivery504-global/inputs/data-base/work/complex-nine-native/DATA-PHASES.json": "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa", + "research/complex-k492-owner-repair/data/PLAN.json": "8c48ef6ce079916314126c5c3ff0003b32f24cf0fbfb2a033fc93e1e1949b5d5", + "research/complex-k492-owner-repair/data/OWNERS.json.gz": "251e82cec1f40e6c1289703667f403104b957f1254dc4f6baa6df9a3d0c751de", + "research/complex-k492-owner-repair/code/audit_allcold.py": "cea021ae79658ca7ca4d07f1e1a70bdb4947afaf95b362114c11032c0fef889a", + "research/complex-k492-owner-repair/code/emit_allcold.py": "fe26f10fe5d30ed407a37540a45ef94f44576dd241d09e19aef5db1efb072746", + "research/complex-k492-owner-repair/vendor/multicold/vendor/pr558/vendor/pr552/complex-global/vendor531/code/prepare_supplier_base.py": "f5eae94aca965d0008bc07cff8245ccb7509042ccad457d3bcb7d51c1e9409f0", + "research/community-k492-audit/pr626/replay/ASSEMBLY.json": "6127732e2fcdd470dab349c1c51d03cd9f0787ad0309b1b4a7c811a908028f4e", + "research/complex-k492-owner-repair/vendor/multicold/vendor/pr558/vendor/pr552/complex-global/vendor535/inputs/ROUND20-PARENT-TEMPLATE.json.gz": "025448abdf2012d327e50a009084e1501690d05e650300d2982836aa0350ae00", + "research/complex-k492-owner-repair/vendor/multicold/vendor/pr558/vendor/pr552/complex-global/run_complex44.py": "5533e9e29c66b11f8feb22a2d3d37551787200ea69eb3d04a984c0b1d22c49bc", + "research/split-centres-global/code/complex_replay.py": "be2dccce2d1ad2c4f5c01a851c9c3896cc88236b5aeae706aad2ab16d6bfdad9" + }, + "selected_record_sha256_at_base": "b3bf402f31a69bde0629936a9b569bed48281568d7b16d5fba120b5311ea1f53", + "selected_kappa_at_base": "51110230636731/31250000000000000" +} diff --git a/research/owner-boundary-audit/VALIDATION.json b/research/owner-boundary-audit/VALIDATION.json new file mode 100644 index 0000000000..fc4abdc70f --- /dev/null +++ b/research/owner-boundary-audit/VALIDATION.json @@ -0,0 +1,43 @@ +{ + "status": "PASS_SCOPED_AUDIT", + "verified_at_utc": "2026-10-13T03:39:57.655611+00:00", + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "python": "3.14.7", + "platform": "Linux-7.2.8-200.fc44.x86_64-x86_64-with-glibc2.43", + "commands": [ + { + "command": "python3 -I -B research/owner-boundary-audit/verify.py", + "exit_code": 0 + }, + { + "command": "python3 -I -O -B research/owner-boundary-audit/verify.py", + "exit_code": 0 + }, + { + "command": "cmp /tmp/owner-audit-normal.json /tmp/owner-audit-optimized.json && cmp /tmp/owner-audit-normal.json research/owner-boundary-audit/EXPECTED.json", + "exit_code": 0 + }, + { + "command": "make selected-record-check", + "exit_code": 0 + }, + { + "command": "git diff --exit-code -- upstream certificates/selected-result.json", + "exit_code": 0 + }, + { + "command": "git diff --cached --check", + "exit_code": 0 + } + ], + "negative_controls": 956, + "bridge_deletion_limitation_cases": 72, + "scalar_omission_witnesses": 9, + "sha256": { + "verify.py": "3568b93da28ecc87a81ef23e610fee0ad71c2b135c38de8258649026f7afd723", + "EXPECTED.json": "594a58226625e2a6804740f956e835a8ef8c471cd20d297b8f0e72591b197541", + "SOURCES.json": "ff72502264012ca7a81597da46efedeee4edcab1834627d725d98fc303c08d06", + "REVIEW.md": "3488b495234a68448bc1be4003261e258abf05ff2e4c09ef8bbafcf6b8173360" + }, + "not_run": "Repository-wide make verify and frontier626-verify were not run: no selected construction, provider, production checker, or inherited source changed. This package checks only the documented finite timing and scalar interface. Remote CI is separate." +} diff --git a/research/owner-boundary-audit/verify.py b/research/owner-boundary-audit/verify.py new file mode 100644 index 0000000000..bc2322098b --- /dev/null +++ b/research/owner-boundary-audit/verify.py @@ -0,0 +1,346 @@ +#!/usr/bin/env python3 +"""Finite PR626 ownership audit by next-touch traversal, without producer imports. + +Prepared for tekuuu with substantial OpenAI Codex assistance. Apache-2.0. +This checks the finite pinned controller, not its all-size physical realization. +""" +import argparse +from collections import Counter, defaultdict +import copy +import gzip +import hashlib +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +PACKAGE = "research/complex-k492-owner-repair/" +PARENT = "research/direct-delivery504-global/inputs/data-base/split-centres/GLOBAL-TEMPLATE.json.gz" +PHASES = "research/direct-delivery504-global/inputs/data-base/work/complex-nine-native/DATA-PHASES.json" +ROUND20 = PACKAGE + "vendor/multicold/vendor/pr558/vendor/pr552/complex-global/vendor535/inputs/ROUND20-PARENT-TEMPLATE.json.gz" + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def read(path): + data = path.read_bytes() + return json.loads(gzip.decompress(data) if path.suffix == ".gz" else data) + + +def digest(value): + return hashlib.sha256(json.dumps(value, sort_keys=True, separators=(",", ":")).encode()).hexdigest() + + +def expand(parent, order): + """Project each replica's source events, then merge complete call blocks.""" + source = parent["execution_schedule"][:30] + starts = [i for i, event in enumerate(source) if event["kind"] == "local_cover_sweep"] + need(len(starts) == 9, "nine source calls") + blocks = [source[a:b] for a, b in zip(starts, starts[1:] + [30])] + need(sorted(map(tuple, order)) == [(s, r) for s in range(9) for r in range(8)], "complete call order") + need(all([s for s, r in order if r == replica] == list(range(9)) for replica in range(8)), "replica source order") + events = [] + for time, (stage, replica) in enumerate(order): + for offset, event in enumerate(blocks[stage]): + events.append(dict(event, replica=replica, time=time, source_event=starts[stage] + offset)) + return events + + +def next_touch(events, stage_pair, child_geometry): + """Reverse state: first future touch of each family pair is an idle or a barrier. + + An active local call is a barrier BEFORE sampling its helper eligibility. + Idle deadlines after that call have already entered the reverse state. + """ + state = {(r, p): None for r in range(8) for p in range(4)} + admitted = defaultdict(set) + calls = {} + deadlines = {} + for position in range(len(events) - 1, -1, -1): + event = events[position] + replica, kind = event["replica"], event["kind"] + if kind == "idle_cover_sweep": + pair = event["pair"] + children = event["child_indices"] + need(len(children) == 2, "two idle sides") + state[replica, pair] = tuple(children) + for child in children: + need((replica, child) not in deadlines, "unique idle deadline") + deadlines[replica, child] = (position, event["time"]) + elif kind == "bridge": + state[replica, event["src"]] = None + state[replica, event["dst"]] = None + elif kind == "local_cover_sweep": + state[replica, stage_pair[event["stage"]]] = None + time = event["time"] + need(time not in calls, "one local event per call") + calls[time] = position + for (owner_replica, pair), children in state.items(): + if children is not None: + for child in children: + if child in child_geometry: + need(child_geometry[child][0] == pair, "idle pair") + admitted[owner_replica, child].add(time) + elif kind in ("terminal_Y_translations", "terminal"): + for pair in range(4): + state[replica, pair] = None + else: + raise ValueError("unknown controller event: " + kind) + need(set(calls) == set(range(72)), "72 event positions") + return admitted, calls, deadlines + + +def geometry(parent): + ranks = {} + for row in parent["idle_children"]: + child = row["child"] + need(child not in ranks or ranks[child] == row["rank"], "port-independent rank") + ranks[child] = row["rank"] + result = {} + for event in parent["execution_schedule"][:30]: + if event["kind"] == "idle_cover_sweep": + for side, child in enumerate(event["child_indices"]): + if child in ranks: + result[child] = (event["pair"], side, ranks[child]) + need(set(result) == set(range(18)), "18 nonzero idle children") + return result + + +def compare_windows(plan, admitted, geom): + need(set(plan["windows"]) == {f"{r},{c}" for r in range(8) for c in geom}, "144 windows") + for replica in range(8): + for child, (pair, side, rank) in geom.items(): + cap, window = plan["windows"][f"{replica},{child}"] + need(cap == rank and len(window) == len(set(window)), "window capacity and uniqueness") + need(set(window) == admitted[replica, child], "next-touch window mismatch") + need(plan["pairs"][str(child)] == pair and plan["sides"][str(child)] == side, "child geometry") + + +def check_roles(roles, plan, admitted, geom, stage_pair, phases): + families = defaultdict(set) + helpers = defaultdict(set) + cells = defaultdict(set) + dispatch = {c["time"]: c for c in plan["provider_calls"]} + need(set(dispatch) == set(range(72)), "complete dispatch") + cross = 0 + for row in roles: + t, helper = row["time"], row["helper"] + need(t in dispatch and 0 <= helper < 492, "call and helper domain") + stage, replica = plan["order"][t] + need((row["stage"], row["replica"]) == (stage, replica), "role call") + owner, child, port = row["owner_replica"], row["child"], row["port"] + need(0 <= owner < 8 and child in geom and 0 <= port < 112, "owner domain") + pair, side, cap = geom[child] + need(t in admitted[owner, child], "role outside next-touch window") + family = owner * 896 + (2 * pair + side) * 112 + port + need(row["family"] == family and row["copy"] == owner * 112 + port, "family identity") + need((owner, pair) != (replica, stage_pair[stage]), "helper aliases active data") + need(family not in families[t] and helper not in helpers[t], "same-call whole-family alias") + families[t].add(family) + helpers[t].add(helper) + width = plan["provider_registry"][dispatch[t]["provider"]]["widths"][helper] + off = row["offset"] + need(row["width"] == width and 0 < width <= 9 and 0 <= off and off + width <= cap, "width and footprint") + axes = phases["recipes"][port]["idle_children"][child]["orthogonal_axes"] + need(len(axes) == cap and len(set(axes)) == cap, "phase axes") + occupied = set(axes[off:off + width]) + key = owner, child, port + need(not occupied & cells[key], "reused pending coordinate") + cells[key].update(occupied) + cross += owner != replica + need(len(roles) == 35424 and all(helpers[t] == set(range(492)) for t in range(72)), "complete role census") + return {"roles": len(roles), "cross_replica_roles": cross, "occupied_owner_groups": len(cells)} + + +def scalar_columns(recipe): + """Apply the inherited normalized data contract to each input basis vector. + + The existing complex_replay.py composes matrix rows. This implementation + instead executes eight separate integer vectors; it imports no replay code. + Idle residuals and phase work have no additional data-shear action here. + """ + columns = [] + for basis in range(8): + x = [int(basis == 2 * p) for p in range(4)] + y = [int(basis == 2 * p + 1) for p in range(4)] + for event in recipe: + if event["kind"] == "local": + pair = event["pair"] + if event["reverse"]: + x[pair] -= y[pair] + else: + y[pair] += x[pair] + elif event["kind"] == "bridge": + src, dst, q = event["src"], event["dst"], event["coefficient"] + x[dst] += q * x[src] + y[src] -= q * y[dst] + elif event["kind"] == "terminal": + x, y = y, [-value for value in x] + else: + raise ValueError("unknown scalar recipe event") + columns.append([value for pair in zip(x, y) for value in pair]) + return columns + + +def audit(): + pins = read(HERE / "SOURCES.json") + for name, expected in pins["sha256"].items(): + need(hashlib.sha256((ROOT / name).read_bytes()).hexdigest() == expected, "source pin: " + name) + source_manifest = read(ROOT / "research/community-k492-audit/SELECTED-SOURCE.json")["files"] + for name in (PARENT, PHASES, PACKAGE + "data/PLAN.json", PACKAGE + "data/OWNERS.json.gz"): + need(source_manifest[name] == pins["sha256"][name], "selected source binding") + parent, plan = read(ROOT / PARENT), read(ROOT / (PACKAGE + "data/PLAN.json")) + installed_parent = read(ROOT / ROUND20) + for key in ("recipe", "idle_children"): + need(parent[key] == installed_parent[key], "installed controller " + key) + need(parent["execution_schedule"][:30] == installed_parent["execution_schedule"][:30], "installed replica controller") + roles, phases = read(ROOT / (PACKAGE + "data/OWNERS.json.gz")), read(ROOT / PHASES) + geom = geometry(parent) + stage_pair = {e["stage"]: e["pair"] for e in parent["recipe"] if e["kind"] == "local"} + events = expand(parent, plan["order"]) + admitted, calls, deadlines = next_touch(events, stage_pair, geom) + compare_windows(plan, admitted, geom) + census = check_roles(roles, plan, admitted, geom, stage_pair, phases) + # Enumerate the COMPLETE matrix, including all inadmissible entries. + matrix = [[r, c, t, int(t in admitted[r, c])] for r in range(8) for c in geom for t in range(72)] + need(len(matrix) == 10368, "complete eligibility matrix") + closing_block = [(r, c, tm) for (r, c), (pos, tm) in deadlines.items() + if c in geom and tm in admitted[r, c] and calls[tm] < pos] + closing_set = set(closing_block) + closing_roles = sum((z["owner_replica"], z["child"], z["time"]) in closing_set for z in roles) + controls = Counter() + + def rejects(label, function, expected): + try: + function() + except ValueError as error: + need(str(error) == expected, "unexpected control failure: " + str(error)) + controls[label] += 1 + else: + raise ValueError("accepted negative control: " + label) + + # Both one-call extensions of every nonempty window, and deleting either + # legal endpoint, model the two off-by-one errors in block-time bounds. + for r in range(8): + for c in geom: + values = admitted[r, c] + for t in sorted({min(values) - 1, min(values), max(values), max(values) + 1}): + if not 0 <= t < 72: + continue + mutant = {**plan, "windows": dict(plan["windows"])} + cap = plan["windows"][f"{r},{c}"][0] + mutant["windows"][f"{r},{c}"] = [cap, sorted(values ^ {t})] + rejects("window_endpoint_shift", lambda: compare_windows(mutant, admitted, geom), "next-touch window mismatch") + # Endpoint controls exercise the scanner rather than just frozen pin comparison. + # Move each idle event before the call of its own block: the deadline now + # precedes that call and must remove its eligibility, leaving all else valid. + swaps = 0 + for i, b in enumerate(events): + if b["kind"] == "idle_cover_sweep" and any(c in geom for c in b["child_indices"]): + call_position = calls[b["time"]] + a = events[call_position] + mutant = list(events) + mutant.pop(i) + mutant.insert(call_position, b) + changed, _, _ = next_touch(mutant, stage_pair, geom) + for c in b["child_indices"]: + if c in geom: + need(a["time"] in admitted[b["replica"], c], "positive closing-block control") + need(a["time"] not in changed[b["replica"], c], "deadline swap must remove call") + swaps += 1 + controls["deadline_before_call"] = swaps + identity = [[int(i == j) for i in range(8)] for j in range(8)] + need(scalar_columns(parent["recipe"]) == identity, "inherited scalar controller identity") + scalar_omissions = [] + source_bridges = [(i, e) for i, e in enumerate(parent["execution_schedule"][:30]) if e["kind"] == "bridge"] + recipe_bridges = [(i, e) for i, e in enumerate(parent["recipe"]) if e["kind"] == "bridge"] + need(len(source_bridges) == len(recipe_bridges) == 9, "nine scalar bridges") + for (source_index, source_event), (recipe_index, recipe_event) in zip(source_bridges, recipe_bridges): + need(source_event == recipe_event, "scalar bridge/controller binding") + mutated_recipe = parent["recipe"][:recipe_index] + parent["recipe"][recipe_index + 1:] + columns = scalar_columns(mutated_recipe) + need(columns != identity, "omitted bridge must change scalar map") + witness = next(j for j in range(8) if columns[j] != identity[j]) + scalar_omissions.append({ + "source_event": source_index, + "input_basis_column": witness, + "actual_output": columns[witness], + "expected_output": identity[witness], + "changed_matrix_entries": sum(a != b for col, expected in zip(columns, identity) for a, b in zip(col, expected)), + }) + # Deleting a bridge is invisible to this timing abstraction on THIS + # controller: adjacent idle/local barriers already delimit the windows. + # This is a limitation witness, not evidence that bridges may be deleted + # from the actual scalar program. Source/controller binding remains vital. + bridge_effects = Counter() + for i, event in enumerate(events): + if event["kind"] == "bridge": + mutant = events[:i] + events[i + 1:] + changed, _, _ = next_touch(mutant, stage_pair, geom) + difference = sum((t in changed[r, c]) != bool(ok) for r, c, t, ok in matrix) + need(difference == 0, "pinned bridge-deletion limitation changed") + bridge_effects["terminal_no_change" if event["source_event"] >= 25 else "nonterminal_no_change"] += 1 + # A NEW intervening physical touch is not redundant. For every window, + # insert a bridge just after a seed-selected legal call and require that + # this call loses eligibility for the touched owner pair. + for r in range(8): + for c, (pair, _, _) in geom.items(): + options = sorted(admitted[r, c]) + t = options[60 % len(options)] + other = (pair + 1) % 4 + for src, dst in ((pair, other), (other, pair)): + new_bridge = dict(kind="bridge", replica=r, src=src, dst=dst, time=t) + position = calls[t] + 1 + mutant = events[:position] + [new_bridge] + events[position:] + changed, _, _ = next_touch(mutant, stage_pair, geom) + need(t not in changed[r, c], "intervening bridge must invalidate the selected call") + rejects("intervening_bridge_source" if src == pair else "intervening_bridge_destination", + lambda: compare_windows(plan, changed, geom), "next-touch window mismatch") + mutant = copy.deepcopy(events) + mutant[0]["kind"] = "unrecognized_touch" + rejects("unknown_event", lambda: next_touch(mutant, stage_pair, geom), "unknown controller event: unrecognized_touch") + # Same call, same family, disjoint coordinates: scalar coordinate disjointness + # does NOT permit two simultaneously live whole helpers. + first = roles[0] + second_index = next(i for i, z in enumerate(roles) if z["time"] == first["time"] and z["helper"] != first["helper"]) + mutant = list(roles) + mutant[second_index] = dict(first, helper=roles[second_index]["helper"], offset=first["offset"] + first["width"]) + rejects("same_family_disjoint_coordinates", lambda: check_roles(mutant, plan, admitted, geom, stage_pair, phases), "same-call whole-family alias") + return { + "status": "PASS_PR626_NEXT_TOUCH_BOUNDARY_AUDIT", + "base_commit": pins["base_commit"], + "assignment_seed": 60, + "replica_events": len(events), + "idle_deadlines_including_zero_rank": len(deadlines), + "nonzero_windows": 144, + "eligibility_decisions": len(matrix), + "admitted_decisions": sum(row[3] for row in matrix), + "eligibility_sha256": digest(matrix), + **census, + "closing_block_admitted_child_calls": len(closing_block), + "closing_block_helper_roles": closing_roles, + "valid_roles_rejected_if_borrower_replica_is_used": sum(z["time"] not in admitted[z["replica"], z["child"]] for z in roles), + "negative_controls": dict(sorted(controls.items())), + "bridge_deletion_sensitivity": dict(sorted(bridge_effects.items())), + "scalar_bridge_omission_counterexamples": scalar_omissions, + "scope": "Finite pinned PR626 controller and literal owner roles; native widths, normalized residual semantics, atomic calls and all-size realization are inherited, not re-proved. No new kappa.", + } + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write", type=Path, help="write a deterministic receipt") + args = parser.parse_args() + result = audit() + if args.write: + args.write.write_text(json.dumps(result, indent=2) + "\n") + else: + need(result == read(HERE / "EXPECTED.json"), "receipt mismatch") + print(json.dumps(result, indent=2)) + + +if __name__ == "__main__": + main()