diff --git a/research/p104-async-first-hub-audit/NOTICE b/research/p104-async-first-hub-audit/NOTICE new file mode 100644 index 0000000000..f3c2f7136c --- /dev/null +++ b/research/p104-async-first-hub-audit/NOTICE @@ -0,0 +1,67 @@ +Asynchronous helper hubs +New work: Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. + +Retained native copies from PR5774 at 7d6ec0cdef31d0c37b7d2563e709979caa0d5eae. +All prior credit follows unchanged. + +Paid intermediate meetings and collective helper splits. +Ali Romman, with substantial OpenAI Codex assistance. Apache-2.0. +No subagents. All checks are author-side calculations. + +The complete PR5718 notice follows unchanged. + +Four paid interior public-basis changes. +Ali Romman, with substantial OpenAI Codex assistance. Apache-2.0. +No subagents. + +The following exact notice is retained from PR5660. + +New helper-subspace construction, proof and replay: +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +The same assistant performed the construction and author-side checks. + +Retained contributions: +flyingviper: PR5605 shared relay, PR5612 delayed relay, and the PR5608/PR5613 +relay/split compositions. +Scratch-net: PR5606 prepared-helper identities and target debit. +Pierre-Loic Doulcet (hexapode): PR5565 commuting-contact construction, used as the exact source. +Ali Romman: PR5602 fixed boundary relations, PR5601 three-contact frame +change, PR5580 contact step, +and PR5544/5545 complete P104 caller. +Joel Pulikkan (GamingPuzzled): PR5569 priced helper handoff. +DreamingOfClouds: PR5561 free helper endpoints and PR5568 search tools. +thu-nmrc: PR5551 contact improvements. +Gareth Davidson (bitplane): PR2305 source composition. +David Arias: PR2152 coalesced P104 word. +Cinna Davis: PR2219 private reuse and the controller lineage. +Jacob Alan Sussman: productive mixed-target recursion. +zxv and Cao Yifan: exact intervals, compiler and native/pricing lineage. +GamingPuzzled: PR5472 successor handoff, a predecessor to the split concept. +The retained source notices preserve earlier geometry, BIT and analytic credit. + +The elementary rank-one basis identity is not claimed as a new general +linear-algebra theorem. The contribution is its explicit independent-target +use on this P104 word and the complete conditional kappa improvement. + +New contribution: Ali Romman, with substantial OpenAI Codex assistance. +The four-gate source-version rewrite composes zxv PR5643 and Ali Romman PR5644. +The A2 method retains Chris R/Clear1nsight PR3998 and ToikY PR4019 credit. +The compensated triangle method retains Cinna Davis PR4692 credit. +No subagents were used for this contribution. Apache-2.0. + +Concurrent PR5650 by zxv publishes the PR5643/PR5644 composition. PR5651 by +Ali Romman corroborates it. This package credits that released composition +and contributes the further four-gate placement. + +New work: distributed scalar updates on an unobserved public field interval, the exact witness and complete conditional price. Prepared for Ali Romman with substantial OpenAI Codex assistance. No subagents. Apache-2.0. The source archive retains all predecessor notices. + +Two-boundary main-assisted helper split and early cleanup: flyingviper with substantial +OpenAI Codex assistance, including independent AI review agents. Apache-2.0. + +Retained native-copy construction +Prepared by Ali Romman with substantial OpenAI Codex assistance. No subagents. +The paid-meeting source is PR5751 by Ali Romman with OpenAI Codex assistance. +The dimension-four span [265,194,164,75] is from Joel Pulikkan / GamingPuzzled +PR5739, with Claude Opus 5.5 assistance. The R22 block edits are not included. +The retained-copy mechanism, exact constructor, source-specific verification, +new price and proof are the contribution of this package. Apache-2.0. diff --git a/research/p104-async-first-hub-audit/ORACLE.json b/research/p104-async-first-hub-audit/ORACLE.json new file mode 100644 index 0000000000..3b92e6dd10 --- /dev/null +++ b/research/p104-async-first-hub-audit/ORACLE.json @@ -0,0 +1,229 @@ +{ + "axes": 789, + "basis_commutes_with_literal_source": true, + "canonical_word_sha256": "75f429fc0c8b206f4439bfbda4b621fc62ea892e6e3008c17409f2d3ee0981bb", + "eligible_support": [ + 133, + 696, + 697, + 699, + 709, + 733 + ], + "individual_injections": [ + { + "delivered": { + "113": "1", + "118": "-1", + "120": "-1", + "122": "1", + "123": "1", + "124": "-1", + "127": "-1", + "129": "-1", + "132": "-1", + "133": "1", + "136": "1", + "138": "1", + "140": "1", + "143": "1", + "144": "1", + "147": "1", + "148": "-1", + "150": "1", + "153": "-1", + "154": "-1", + "157": "-1", + "158": "-1", + "159": "-1", + "160": "-1", + "164": "1", + "165": "1", + "168": "1", + "170": "-1", + "174": "-1", + "175": "-1", + "178": "1", + "179": "-1", + "182": "-1", + "183": "-1", + "187": "1", + "189": "1", + "192": "-1", + "194": "-1", + "197": "1", + "198": "1", + "200": "1", + "202": "1", + "203": "1", + "207": "-1", + "210": "-1", + "212": "-1", + "215": "-1", + "217": "1", + "218": "1", + "219": "-1", + "222": "-1", + "223": "-1", + "696": "1" + }, + "role": 696, + "time2": 27044 + }, + { + "delivered": { + "113": "1", + "118": "-1", + "120": "-1", + "122": "1", + "123": "1", + "124": "-1", + "127": "-1", + "129": "-1", + "132": "-1", + "133": "1", + "136": "1", + "138": "1", + "140": "1", + "143": "1", + "144": "1", + "147": "1", + "148": "-1", + "149": "-1", + "150": "1", + "153": "-1", + "154": "-1", + "157": "-1", + "158": "-1", + "159": "-1", + "160": "-1", + "164": "1", + "165": "1", + "168": "1", + "170": "-1", + "174": "-1", + "175": "-1", + "178": "1", + "179": "-1", + "182": "-1", + "183": "-1", + "187": "1", + "189": "1", + "192": "-1", + "194": "-1", + "197": "1", + "198": "1", + "200": "1", + "202": "1", + "203": "1", + "207": "-1", + "210": "-1", + "212": "-1", + "215": "-1", + "217": "1", + "218": "1", + "219": "-1", + "223": "-1", + "697": "1" + }, + "role": 697, + "time2": 27044 + }, + { + "delivered": { + "113": "-2", + "118": "2", + "120": "2", + "122": "-2", + "123": "-2", + "124": "2", + "127": "2", + "129": "2", + "132": "2", + "136": "-2", + "138": "-2", + "140": "-2", + "143": "-2", + "144": "-2", + "147": "-2", + "148": "2", + "149": "2", + "150": "-2", + "153": "2", + "154": "2", + "157": "2", + "158": "2", + "159": "2", + "160": "2", + "164": "-2", + "165": "-2", + "168": "-2", + "170": "2", + "174": "2", + "175": "2", + "178": "-2", + "179": "2", + "182": "2", + "183": "2", + "187": "-2", + "189": "-2", + "192": "2", + "194": "2", + "197": "-2", + "198": "-2", + "200": "-2", + "202": "-2", + "203": "-2", + "207": "2", + "210": "2", + "212": "2", + "215": "2", + "217": "-2", + "218": "-2", + "219": "2", + "222": "2", + "223": "2", + "695": "1", + "709": "1", + "733": "1" + }, + "role": 770, + "time2": 27501 + }, + { + "delivered": { + "149": "-1", + "222": "-1", + "695": "-1", + "699": "1" + }, + "role": 699, + "time2": 27516 + } + ], + "input_row": { + "696": "1" + }, + "output_column": { + "133": "2", + "696": "1", + "697": "1", + "699": "1", + "709": "1", + "733": "1" + }, + "plan_sha256": "2c4878f78dc393339f8cccf24441d9bfb50257784459c2f253ebcb27c964211c", + "scope": "Exact decoded temporal identities only; native phases, physical contact legality, full source endpoint and complete price remain separate obligations.", + "source_identity_columns": [ + 133, + 696, + 697, + 699, + 709, + 733 + ], + "source_identity_row": 696, + "source_word_sha256": "7c393444fa5b9a6941471d02047beb2aa8285e5614bb052fb85458b69236a38a", + "status": "PASS_P104_ASYNC_FIRST_HUB_ORACLE", + "unit_pairing": "1" +} diff --git a/research/p104-async-first-hub-audit/PROOF.md b/research/p104-async-first-hub-audit/PROOF.md new file mode 100644 index 0000000000..1cfe1125ac --- /dev/null +++ b/research/p104-async-first-hub-audit/PROOF.md @@ -0,0 +1,156 @@ +# One temporal helper split: scalar implication and source boundary + +This is an independent audit of **step 1 only** of Ali Romman's PR #5786 at +`6b936acd68a7e0f9062037900f0fe9bc4b6fdd25`, using its pinned PLAN and the +PR #5774 word at `7d6ec0cdef31d0c37b7d2563e709979caa0d5eae`. +The algebra below is quantified over arbitrary inputs. Its source instantiation +checks temporal scalar data and frames; it does not admit the complete caller. + +## Quantified temporal lemma + +Work over the rational scalars with the source's permitted dyadic operations. +Let a finite linear word have public input vector x and arbitrary dirty owned +input vector a. Under its charged INIT/CLEAR semantics its complete endpoint is +`(T x, 0_owned)`, independent of a. Let G be a set of independent public helper +coordinates with common zero entrance frame and common full exit frame V. +Require both rows and columns of T on G to be those of the identity: equivalently, +`T = I_G direct-sum T_rest` in this coordinate decomposition. In particular, an +admissible change of basis on G commutes with T. + +Fix h in G, an intermediate frame F, and a cut where the physical field h is +live at F. Suppose the following data are supplied and checked against the +actual word, including all public and dirty owned columns: + +1. Collection contacts, all at F and no later than the cut, have complete + prefix row c. Its support is in G; its dirty owned coefficients vanish. +2. Injection contacts, all at F and no earlier than the cut, have complete + suffix column d into all old outputs. Its support is in G, including zero + components on old owned outputs. Thus injecting a common scalar u adds d u. +3. `c d = 1`, and there is an admissible invertible dyadic basis Q on G with + `Q e_h = d` and `c Q = e_h^T`. Both boundary basis changes are legal at the + common entrance and exit frames. +4. A separately charged owned buffer can remain live at F from the first + collection through the last injection. Every interior contact is available + through a paid, admissible query subdivision; all required primitive costs + and owned storage are retained. These are hypotheses about implementation, + not consequences of the scalar pairing. + +Then one can replace helper h's old zero-to-V target by two independent public +targets, zero-to-F and F-to-V, while retaining every other prescribed public +output and zeroing every owned output under the same INIT/CLEAR semantics. +The target ranks become `dim(F)` and `dim(V)-dim(F)`. + +For completeness, when `d_h` is a unit in the dyadic ring, a concrete Q is +`B D A`, where + +``` +A = I - e_h sum_(j != h) c_j e_j^T, +D scales coordinate h by d_h, +B = I + sum_(j != h) (d_j/d_h) e_j e_h^T. +``` + +All factors are invertible and admissible under that unit hypothesis. +Immediately `B D A e_h = d`. The unit pairing gives +`c B D = e_h^T + sum_(j != h) c_j e_j^T`, so `c B D A = e_h^T`. +The present instance has `d_h = 1`. + +## Proof, with the buffer value retained + +Apply Q to the public helper inputs at their common entrance. Initialize the +new owned buffer b at the first collection. Its incoming value is arbitrary; +the inherited, charged INIT primitive removes its dependence on that value. +Accumulate the collection contacts without changing their source fields. +Their sum is `c Q x = x_h`, independently of every dirty owned input. +No inverse of a possibly singular prefix is used. + +At the cut write y for the old value of physical field h. Introduce a fresh, +independent public input z at F. Initially `(h,b,fresh) = (y,x_h,z)`. Perform + +``` +swap(h,b); swap(fresh,b); b <- b - h. +``` + +Each scalar swap is three ADDs and one SCALE by -1: on coordinates (p,q), use +`p<-p+q; q<-q-p; p<-p+q; q<--q`. Thus the displayed sequence leaves +`(h,b,fresh) = (x_h,z-x_h,y)`. Retire physical h at F. Rename **every** remaining +reference in its old trajectory to fresh, including its final boundary-basis +reference. The source continuation therefore begins with its original y; +there is no assumption that y equals x_h. + +Keep b at F and inject its unchanged value at the stated later contacts. +Linearity of the complete suffix histories makes the resulting correction +exactly `d(z-x_h)`, including zero correction on every old owned output. +The continuing old-coordinate output before the final basis inverse is + +``` +T Q x + d(z-x_h). +``` + +Since T commutes with Q and `Q^-1 d = e_h`, applying the legal terminal Q^-1 +gives `T x + e_h(z-x_h)`. Its h coordinate is z, every other old public output +is unchanged, and all old owned outputs remain zero. The retired physical +field holds x_h at F. These are the two independent targets asserted above. + +After its last injection **the buffer still contains `z-x_h` in general**. +Its final zero is supplied by the inherited, charged CLEAR primitive. This +argument does not derive reversible erasure of an arbitrary scalar, supply +free clean storage, or discharge the framework assumption behind INIT/CLEAR. + +## Exact first-step binding and limits + +For the pinned step, h is 696, F is frame 1031, and the cut time2 is 27044. +An even time2 denotes the boundary before event `time2/2`; an odd value is an +interior contact in the indexed MOVE. The collection is field 696 at 27026. +The injection contacts are fields 696 and 697 at 27044, owned field 770 at +27501, and field 699 at 27516. The complete row and column to check are + +``` +c = e_696^T, +d = e_696 + e_697 + e_699 + e_709 + e_733 + 2 e_133. +``` + +All six coordinates in d enter at frame 3 (the zero space) and exit at frame +127 (dimension nine). They belong to the identity block of the prescribed +source endpoint `I + sum_(r live) e_(r+112) e_r^T`. Thus `c d = 1`, `d_696 = 1`, +and the boundary-basis conditions hold. These support facts alone do not +establish the temporal rows: the verifier separately checks complete +prefix/suffix histories and the actual source contact frames and lifetime. + +The odd injection contact is inside source event 13750, +`MOVE 770 591 597 owned=true`. The actual frame dimensions are 8, 5, 1, and +the required descending inclusions are `591 > 1031 > 597`. Its paid ranks +are consequently `7 -> (3,4)`, with access-query cost change +`H3 + H4 - H7`, where `Hr = r^t`. This is a frame/rank audit of this single +subdivision, not the full step invoice. In particular, `2H1-H2` is not the +cost change for this first-step query. The split helper targets have ranks +5 and 4 instead of 9. + +The verifier also emits and replays this first split in an independent formal +namespace: old public labels 0 through 766 and owned labels 767 through 788 +are retained, fresh public input z is label 789, and the new owned buffer is +790. It emits the initial basis, collection, all nine cut operations, all four +injections, the two real-frame query segments with their intervening injection, +the charged buffer CLEAR, and the terminal basis inverse. All source references +to 696 at or after the cut are renamed to 789; the terminal inverse uses 789 +as well. This is not a byte-identity claim for the author's emitted word. + +The literal witness has 25,909 events, 25 owned lifetimes and peak 12 live +owned fields. Exact replay checks all `791^2 = 625,681` endpoint coefficient +positions, including every arbitrary dirty owned input axis. It restores all +old public values and zero owned outputs, retires 696 at frame 1031 and ends +789 at frame 127. Immediately before CLEAR the buffer row is exactly +`e_789^T - e_696^T`. Omitting that CLEAR and omitting the first swap's SCALE +are separately rejected by endpoint discrepancies. Thus the finite decoded +scalar/frame restoration and emitted owned-lifetime closure are checked; +their complete native implementation and price remain separate obligations. + +This audit does not check native maps or absolute phases, price all boundary +and lifetime operations, replay steps 2 or 3, verify the physical caller, +establish an ordinary compiler, or admit a full conditional kappa bound. +Static unit pairing without the checked temporal frames, complete histories, +legal bases, and funded owned lifetime cannot justify the target split. + +Credit: Ali Romman with OpenAI Codex assistance for the source temporal +construction, PLAN, PR #5774 word and retained predecessor lineage in NOTICE. +This scoped proof/audit was prepared by ToikY with substantial OpenAI Codex +assistance, using separate implementation and review contexts. Apache-2.0. diff --git a/research/p104-async-first-hub-audit/README.md b/research/p104-async-first-hub-audit/README.md new file mode 100644 index 0000000000..7d2dc484a9 --- /dev/null +++ b/research/p104-async-first-hub-audit/README.md @@ -0,0 +1,84 @@ +# Independent audit of the first asynchronous helper hub + +This checks one temporal implication in Ali Romman's PR #5786 at +`6b936acd68a7e0f9062037900f0fe9bc4b6fdd25`, on its exact PR #5774 source +`7d6ec0cdef31d0c37b7d2563e709979caa0d5eae`. It answers the first-step review +request in [Discussion #5600](https://github.com/CrocSwap/integer-mult-bounds/discussions/5600#discussioncomment-19202381). +The [audit claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/5600#discussioncomment-19203981) distinguishes this from the active different-output-owner construction. The new result is an independently implemented source-data audit and quantified +scalar implication, not a new construction or conditional bound. + +The fixed object is pivot 696, frame 1031, cut time2=27044. Collection reads +field 696 at 27026. Four injections read the retained difference buffer into +696/697 at 27044, owned 770 at 27501, and 699 at 27516. The odd time is inside +actual source query 13750; event numbers apply only to this frozen source. + +The complete temporal row is `c=e696^T`, and the complete delivery column is +`d=e696+e697+e699+e709+e733+2e133`, with `c*d=1`. Role 133 is an eligible +helper hole: main roles are derived from the actual live ports and their +offset 112 partners, rather than treating every role below 224 as main. +The independent oracle checks all 789 axes and establishes commutation of the +actual boundary basis with the literal source endpoint. Individual injection +contributions need not have helper-only support; their exact sum does. + +The actual owned query is `MOVE 770:591->597`. Frame dimensions are 8, 5, 1 +through the inserted frame 1031. Its descending subspaces give paid ranks +`7 -> (3,4)`, so the **access-query delta only** is `H3+H4-H7`, where +`Hr=r^t`. The helper target splits into ranks 5 and 4. The full step invoice +also owes boundary bases, scalar swaps, owned initialization/erasure and +routing. This package does not price that full invoice or claim a gain. + +[PROOF.md](PROOF.md) states the quantified hypotheses and the two-swap +difference-buffer argument. The buffer contains `z-x_h` before its charged +CLEAR; it is not asserted to vanish by reversible scalar algebra. INIT/CLEAR +retain the inherited owned-erasure assumption. A static pairing alone is not +a physical or chronological construction. + +## Reproduction and evidence + +Python 3.12 and the standard library suffice. The two implementations import +no predecessor implementation and do not import each other. + +```sh +python3.12 -I -W error -B research/p104-async-first-hub-audit/verify.py +python3.12 -I -O -W error -B research/p104-async-first-hub-audit/oracle.py +python3.12 -B scripts/research_package.py --package research/p104-async-first-hub-audit +``` + +`verify.py` uses complete rational prefix/suffix histories and an independently emitted first-step scalar/frame witness, with frame/lifetime checks and meaningful rejection controls. `oracle.py` uses +a reversed read functional and four separate forward perturbations, then +checks the necessary source identity columns and pivot output row. See +[RESULT.json](RESULT.json) and [ORACLE.json](ORACLE.json) for exact receipts. +The literal first-split witness checks all 625,681 endpoint positions on 791 formal inputs, 25 owned lifetimes and a peak of 12 live owned fields. It explicitly emits both swaps, buffer INIT/CLEAR and the query subdivision. It checks all 622,521 original source endpoint positions as a separate prerequisite. Seven controls reject omitted collection, owned injection, causal order, source binding, paid access, new buffer CLEAR and a swap sign. Default execution compares the entire canonical JSON RESULT/ORACLE receipts, including boolean/number type distinctions; `verify.py --emit` is an explicit candidate-generation mode and writes no files. + +The package vendors only the 122,348-byte source word and the 3,840-byte PLAN, +not a copy of either predecessor implementation. Both raw SHA256 and Git +blob identifiers are authenticated independently; the decoded word also has +a canonical JSON SHA256. [SOURCES.json](SOURCES.json) records exact origin +commits, paths and byte bindings. Generic provenance rows bind the main task +catalogue and selected context. The vendored-data checks do not establish +publication ancestry or imply that the predecessor's complete export ran. + +Main was refreshed to `de5ec2e7a6074068452f45b1a191b5c72832df4a`, priority 8. +[Task](TASK.json) records the explicit change from a formalization card to this +finite exact source-binding audit. No Lean build was run. The exact selected-source inputs were materialized and the current baseline passed `PASS_RESEARCH_BASELINE_BINDINGS_ONLY` on Python 3.12.14. This authenticates selected source bindings and metadata only; no native selected replay or supplier admission follows. + +## Open next questions + +- Independently check native maps and absolute phases for this subdivision, + and bind all scalar/buffer/route costs to the full first-step invoice. + Temporal equality and ranks alone do not prove that binding. +- Then audit steps 2/3 on their own exact input words; source event indices + change after each construction. The complete caller, ordinary compiler, + precision and analytic framework assumptions remain outside this audit. + +The structured next question and its blockers are in [TASK.json](TASK.json). +No all-size theorem, supplier admission, new kappa or frontier change follows. + +## Credit + +Ali Romman, with OpenAI Codex assistance, supplied the asynchronous +construction, plans and retained-copy source word. Retain flyingviper's +boundary bases, Joel Pulikkan/GamingPuzzled's basis work and every native, +controller, compiler and BIT predecessor in [NOTICE](NOTICE). New audit and +proof: ToikY with substantial OpenAI Codex assistance, using separate bounded +implementation and read-only proof/review contexts. Apache-2.0. diff --git a/research/p104-async-first-hub-audit/RESULT.json b/research/p104-async-first-hub-audit/RESULT.json new file mode 100644 index 0000000000..c1f9c8f762 --- /dev/null +++ b/research/p104-async-first-hub-audit/RESULT.json @@ -0,0 +1,160 @@ +{ + "collection_row": { + "696": "1" + }, + "contacts": [ + { + "actual_frame": 1031, + "coefficient": "1", + "kind": "collection", + "owned_live": false, + "role": 696, + "time2": 27026 + }, + { + "actual_frame": 1031, + "coefficient": "1", + "kind": "injection", + "owned_live": false, + "role": 696, + "time2": 27044 + }, + { + "actual_frame": 1031, + "coefficient": "1", + "kind": "injection", + "owned_live": false, + "role": 697, + "time2": 27044 + }, + { + "actual_frame": 1031, + "coefficient": "1", + "kind": "injection", + "owned_live": true, + "role": 770, + "time2": 27501 + }, + { + "actual_frame": 1031, + "coefficient": "1", + "kind": "injection", + "owned_live": false, + "role": 699, + "time2": 27516 + } + ], + "cut_time2": 27044, + "delivery_column": { + "133": "2", + "696": "1", + "697": "1", + "699": "1", + "709": "1", + "733": "1" + }, + "eligible_full_boundary_helpers": 388, + "erasure_scope": "INIT/CLEAR use the predecessor's charged owned-erasure semantics", + "failure_controls": [ + { + "name": "omitted_collection", + "reason": "complete temporal collection row", + "rejected": true + }, + { + "name": "omitted_owned_injection", + "reason": "complete temporal delivery column", + "rejected": true + }, + { + "name": "injection_before_cut", + "reason": "causal collection/cut/injection order", + "rejected": true + }, + { + "name": "wrong_source", + "reason": "step source binding", + "rejected": true + }, + { + "name": "unpaid_owned_interior_query", + "reason": "unpaid interior contact", + "rejected": true + }, + { + "name": "omitted_new_buffer_CLEAR", + "reason": "split arbitrary-input endpoint at role 790", + "rejected": true + }, + { + "name": "omitted_first_swap_SCALE", + "reason": "split arbitrary-input endpoint at role 113", + "rejected": true + } + ], + "frame": 1031, + "helper_133_is_eligible": true, + "literal_first_split": { + "before_clear_row": { + "696": "-1", + "789": "1" + }, + "coefficient_positions_checked": 625681, + "endpoint_sha256": "b8354146bda85ded4f6baef48b34fea08e055e720a4387acabe9a427db8bf5e0", + "event_stream_sha256": "62637d16db1ae4e9c777a9837877634cdb55d6d8f7967febf6a4db2a028e32c8", + "formal_input_axes": 791, + "fresh_final_frame": 127, + "fresh_public_label": 789, + "label_scope": "Independent namespace; not a byte-identity claim for the author's emitted word", + "new_buffer_clear_count": 1, + "new_buffer_init_count": 1, + "new_owned_buffer_label": 790, + "owned_lifetimes": 25, + "peak_live_owned": 12, + "program_events": 25909, + "retired_pivot_final_frame": 1031 + }, + "paid_access": [ + { + "event": [ + "MOVE", + 770, + 591, + 597, + true + ], + "frame_dimensions": [ + 8, + 5, + 1 + ], + "index": 13750, + "replaced_rank": 7, + "replacement_ranks": [ + 3, + 4 + ] + } + ], + "paid_access_delta": { + "3": 1, + "4": 1, + "7": -1 + }, + "pairing": "1", + "pivot": 696, + "plan_raw_sha256": "2c4878f78dc393339f8cccf24441d9bfb50257784459c2f253ebcb27c964211c", + "schema": "p104-async-first-hub-audit/1", + "scope": "Finite exact first-step temporal contacts and literal scalar/frame restoration; no native phase, full caller or kappa admission", + "source_canonical_sha256": "75f429fc0c8b206f4439bfbda4b621fc62ea892e6e3008c17409f2d3ee0981bb", + "source_endpoint": { + "coefficient_positions_checked": 622521, + "endpoint": "I + sum e_(r+112) e_r^T on public coordinates; zero owned outputs", + "endpoint_sha256": "377cd8e5aa4515a2fda585cfe1f180651a3800be0cdcd467b17aa53c1bc0cf52", + "input_columns": 789, + "output_rows": 789, + "owned_lifetimes": 24, + "peak_live_owned": 12 + }, + "source_raw_sha256": "7c393444fa5b9a6941471d02047beb2aa8285e5614bb052fb85458b69236a38a" +} diff --git a/research/p104-async-first-hub-audit/SOURCES.json b/research/p104-async-first-hub-audit/SOURCES.json new file mode 100644 index 0000000000..fb1ebd3a6f --- /dev/null +++ b/research/p104-async-first-hub-audit/SOURCES.json @@ -0,0 +1,41 @@ +{ + "schema_version": 1, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + } + ], + "vendored_inputs": [ + { + "path": "inputs/WORD.json.gz", + "repository": "aliromman/integer-mult-bounds", + "commit": "7d6ec0cdef31d0c37b7d2563e709979caa0d5eae", + "source_path": "research/p104-retained-native-copy/WORD.json.gz", + "git_blob": "3ae3c4ebc8fc92098784f717a3107e6fa958dd86", + "sha256": "7c393444fa5b9a6941471d02047beb2aa8285e5614bb052fb85458b69236a38a", + "bytes": 122348, + "usage": "Frozen package-local source data; verifier authenticates raw bytes and Git blob independently. No predecessor implementation import." + }, + { + "path": "inputs/PLAN.json", + "repository": "aliromman/integer-mult-bounds", + "commit": "6b936acd68a7e0f9062037900f0fe9bc4b6fdd25", + "source_path": "research/p104-asynchronous-helper-hubs/PLAN.json", + "git_blob": "9cf72d400fdb2adef54eca047c752a657a0d4a33", + "sha256": "2c4878f78dc393339f8cccf24441d9bfb50257784459c2f253ebcb27c964211c", + "bytes": 3840, + "usage": "Frozen package-local source data; verifier authenticates raw bytes and Git blob independently. No predecessor implementation import." + } + ], + "source_binding_scope": "Original source objects were read through public GitHub exact-commit resources and independently matched here. The generic provenance rows bind only current-main context; archived data authenticates itself in the verifier. No source-publication ancestry or predecessor full replay is inferred." +} diff --git a/research/p104-async-first-hub-audit/TASK.json b/research/p104-async-first-hub-audit/TASK.json new file mode 100644 index 0000000000..f3b17f9f80 --- /dev/null +++ b/research/p104-async-first-hub-audit/TASK.json @@ -0,0 +1,108 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 8, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Independent exact source-data audit of PR5786 step1 temporal helper split: pivot696,F1031,cut27044, actual collection/injection times including owned query13750. Independently emit and replay only this first split on791 formal coordinates, including the new dirty buffer lifetime and two scalar swaps; no native phase/full invoice.", + "scope_change_reason": "Follow explicit Discussion5600/1166 first-step review handoff. This is a finite exact temporal-interface proof/certificate audit, not a Lean formalization or a claim to close a selected framework assumption.", + "bottleneck_link": "Tests the temporal implication behind a changed productive helper inventory; a static pairing alone cannot justify independent target credit.", + "budget_minutes": 60, + "stop_rule": "Freeze by21:05:38UTC; stop or narrow if actual source contact/frame/liveness, unit pairing or arbitrary-input restoration fails. No broader search, source rewrite, native-phase or complete-price admission.", + "outcome": "completed", + "evidence": "RESULT.json:622521 source coefficient positions,625681 first-split positions/791 axes,25 owned lifetimes/peak12,seven specific rejection controls. ORACLE.json:independent temporal c/d and literal source basis commutation. Normal and optimized typed payloads agree; full route price/native phases/caller/compiler remain outside scope. Entire canonical JSON receipts reject boolean/number aliases; selected baseline source-binding report passes after exact input materialization.", + "author": "ToikY", + "ai_assistance": "Substantial OpenAI Codex assistance; separate bounded implementation and read-only review contexts.", + "open_questions": [ + { + "question": "Do the remaining two temporal splits and complete invoice bind to the physical caller?", + "why_it_matters": "This first-step temporal audit cannot establish full conditional admission.", + "first_step": "Audit exact step2/3 inputs and native/price binding in PR5786 without transferring event numbers.", + "blocked_by": "Outside this one-step scope; native all-column, caller/compiler/precision/analytic assumptions remain." + } + ], + "source_heads": { + "PR5786": "6b936acd68a7e0f9062037900f0fe9bc4b6fdd25", + "PR5774": "7d6ec0cdef31d0c37b7d2563e709979caa0d5eae" + }, + "claim_expires": "2026-10-26T22:20:00Z", + "started_at": "2026-10-26T20:20:38+00:00", + "science_cutoff": "2026-10-26T21:05:38+00:00", + "finish_by": "2026-10-26T21:20:38+00:00", + "selected_baseline": { + "status": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5", + "scope": "Source bindings and metadata only; no native replay or admission." + } +} diff --git a/research/p104-async-first-hub-audit/VERIFY.json b/research/p104-async-first-hub-audit/VERIFY.json new file mode 100644 index 0000000000..3aa4bfeedf --- /dev/null +++ b/research/p104-async-first-hub-audit/VERIFY.json @@ -0,0 +1,47 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact source/PLAN authentication; all789 source axes; first split791 formal axes/625681 coefficient positions; contact/frame/lifetime and7 specific controls; entire frozen RESULT comparison." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Optimized independent first-split replay with explicit guards and exact frozen receipt." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/oracle.py" + ], + "timeout_seconds": 120, + "checks": "Opposite-direction temporal oracle;6 source columns/pivot-row basis commutation; complete frozen ORACLE receipt." + } + ] +} diff --git a/research/p104-async-first-hub-audit/inputs/PLAN.json b/research/p104-async-first-hub-audit/inputs/PLAN.json new file mode 100644 index 0000000000..9cf72d400f --- /dev/null +++ b/research/p104-async-first-hub-audit/inputs/PLAN.json @@ -0,0 +1,193 @@ +{ + "source_canonical_sha256": "75f429fc0c8b206f4439bfbda4b621fc62ea892e6e3008c17409f2d3ee0981bb", + "steps": [ + { + "pivot": 696, + "frame": 1031, + "time2": 27044, + "buffer": 790, + "collection": [ + { + "time2": 27026, + "role": 696, + "coefficient": "1" + } + ], + "injection": [ + { + "time2": 27044, + "role": 696, + "coefficient": "1" + }, + { + "time2": 27044, + "role": 697, + "coefficient": "1" + }, + { + "time2": 27501, + "role": 770, + "coefficient": "1" + }, + { + "time2": 27516, + "role": 699, + "coefficient": "1" + } + ], + "input": { + "696": "1" + }, + "output": { + "733": "1", + "709": "1", + "696": "1", + "133": "2", + "699": "1", + "697": "1" + }, + "queries": [ + 13750 + ], + "source_sha256": "75f429fc0c8b206f4439bfbda4b621fc62ea892e6e3008c17409f2d3ee0981bb", + "query_events": [ + [ + "MOVE", + 770, + 591, + 597, + true + ] + ], + "output_sha256": "42b7418cdcd42c50a09ec8bd97cd42f4953802e16f179997643d8bde503735f1" + }, + { + "pivot": 623, + "frame": 117, + "time2": 26314, + "buffer": 792, + "collection": [ + { + "time2": 26314, + "role": 623, + "coefficient": "1" + } + ], + "injection": [ + { + "time2": 26318, + "role": 624, + "coefficient": "1" + }, + { + "time2": 26330, + "role": 627, + "coefficient": "-1/2" + }, + { + "time2": 26332, + "role": 629, + "coefficient": "-1/2" + }, + { + "time2": 26336, + "role": 629, + "coefficient": "1/2" + }, + { + "time2": 32701, + "role": 732, + "coefficient": "1/2" + } + ], + "input": { + "623": "1" + }, + "output": { + "732": "1/2", + "576": "2", + "549": "2", + "570": "4", + "558": "-4", + "575": "2", + "548": "2", + "569": "2", + "547": "2", + "546": "-2", + "568": "4", + "205": "1", + "625": "-1", + "623": "1", + "627": "-1/2", + "624": "1" + }, + "queries": [ + 16350 + ], + "source_sha256": "42b7418cdcd42c50a09ec8bd97cd42f4953802e16f179997643d8bde503735f1", + "query_events": [ + [ + "MOVE", + 732, + 594, + 222, + false + ] + ], + "output_sha256": "21b8911d58e6d7777dc7458ccf5b05f1da8669bc1044270909746ddd4abc5948" + }, + { + "pivot": 585, + "frame": 245, + "time2": 34391, + "buffer": 794, + "collection": [ + { + "time2": 31557, + "role": 438, + "coefficient": "-1" + }, + { + "time2": 34391, + "role": 585, + "coefficient": "1" + } + ], + "injection": [ + { + "time2": 34391, + "role": 585, + "coefficient": "1" + } + ], + "input": { + "585": "1" + }, + "output": { + "585": "1" + }, + "queries": [ + 15778, + 17195 + ], + "source_sha256": "21b8911d58e6d7777dc7458ccf5b05f1da8669bc1044270909746ddd4abc5948", + "query_events": [ + [ + "MOVE", + 438, + 911, + 127, + false + ], + [ + "MOVE", + 585, + 918, + 127, + false + ] + ], + "output_sha256": "45e3f8efd004f2a6d2c02a2ac2ebe3dd9ce04c887641ec9ab31e47f8c7f41e1b" + } + ] +} diff --git a/research/p104-async-first-hub-audit/inputs/WORD.json.gz b/research/p104-async-first-hub-audit/inputs/WORD.json.gz new file mode 100644 index 0000000000..3ae3c4ebc8 Binary files /dev/null and b/research/p104-async-first-hub-audit/inputs/WORD.json.gz differ diff --git a/research/p104-async-first-hub-audit/oracle.py b/research/p104-async-first-hub-audit/oracle.py new file mode 100644 index 0000000000..0cf57fb1ef --- /dev/null +++ b/research/p104-async-first-hub-audit/oracle.py @@ -0,0 +1,196 @@ +#!/usr/bin/env python3 +"""Independent forward-perturbation oracle for the first PR5786 hub. + +New audit: ToikY with substantial OpenAI Codex assistance in a separate +implementation context. Ali Romman supplied the asynchronous construction, +plan and retained-copy word. Apache-2.0; NOTICE retains predecessor credit. +No predecessor implementation or the package verifier is imported. +""" +from fractions import Fraction +from hashlib import sha1, sha256 +import gzip +import json +from pathlib import Path + + +HERE = Path(__file__).resolve().parent +WORD_SHA256 = "7c393444fa5b9a6941471d02047beb2aa8285e5614bb052fb85458b69236a38a" +WORD_BLOB = "3ae3c4ebc8fc92098784f717a3107e6fa958dd86" +CANONICAL_WORD = "75f429fc0c8b206f4439bfbda4b621fc62ea892e6e3008c17409f2d3ee0981bb" +PLAN_SHA256 = "2c4878f78dc393339f8cccf24441d9bfb50257784459c2f253ebcb27c964211c" +PLAN_BLOB = "9cf72d400fdb2adef54eca047c752a657a0d4a33" + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def authenticated(name, expected_sha256, expected_blob): + raw = (HERE / "inputs" / name).read_bytes() + require(sha256(raw).hexdigest() == expected_sha256, + "Exact oracle input SHA256: " + name) + blob = sha1(b"blob " + str(len(raw)).encode() + b"\0" + raw).hexdigest() + require(blob == expected_blob, "Exact oracle Git blob: " + name) + return raw + + +def sparse(vector): + return {str(i): str(value) for i, value in enumerate(vector) if value} + + +def role(event, position, size): + value = event[position] + require(type(value) is int and 0 <= value < size, "Oracle role range") + return value + + +def split_time(word, time2): + require(type(time2) is int and 0 <= time2 <= 2 * len(word["program"]), + "Oracle contact time range") + index, midpoint = divmod(time2, 2) + if midpoint: + require(index == 13750 and word["program"][index] + == ["MOVE", 770, 591, 597, True], + "Oracle actual paid interior query") + return index, midpoint + + +def prefix_functional(word, contact): + """Backpropagate one read functional, without inverting the prefix.""" + size = word["public"] + word["owned_fields"] + vector = [Fraction(0) for _ in range(size)] + source = contact["role"] + require(type(source) is int and 0 <= source < size, "Oracle collection role") + vector[source] = Fraction(contact["coefficient"]) + index, midpoint = split_time(word, contact["time2"]) + # A decoded MOVE is the identity, including either half of a subdivision. + for event in reversed(word["program"][:index]): + op = event[0] + dst = role(event, 1, size) + if op == "MOVE": + continue + if op in ("INIT", "CLEAR"): + vector[dst] = Fraction(0) + elif op == "SCALE": + vector[dst] *= Fraction(event[-2]) + else: + require(op in ("ADD", "COPY"), "Oracle prefix opcode") + src = role(event, 2, size) + require(src != dst, "Oracle distinct prefix operands") + vector[src] += Fraction(event[-2]) * vector[dst] + if op == "COPY": + vector[dst] = Fraction(0) + return vector + + +def forward_delivery(word, contact): + """Inject one perturbation, then execute the remaining decoded program.""" + size = word["public"] + word["owned_fields"] + vector = [Fraction(0) for _ in range(size)] + target = contact["role"] + require(type(target) is int and 0 <= target < size, "Oracle injection role") + vector[target] = Fraction(contact["coefficient"]) + index, midpoint = split_time(word, contact["time2"]) + for event in word["program"][index + midpoint:]: + op = event[0] + dst = role(event, 1, size) + if op == "MOVE": + continue + if op in ("INIT", "CLEAR"): + vector[dst] = Fraction(0) + elif op == "SCALE": + vector[dst] *= Fraction(event[-2]) + else: + require(op in ("ADD", "COPY"), "Oracle forward opcode") + src = role(event, 2, size) + require(src != dst, "Oracle distinct forward operands") + value = Fraction(event[-2]) * vector[src] + vector[dst] = value if op == "COPY" else vector[dst] + value + return vector + + +def run(): + raw = authenticated("WORD.json.gz", WORD_SHA256, WORD_BLOB) + word = json.loads(gzip.decompress(raw)) + plan = json.loads(authenticated("PLAN.json", PLAN_SHA256, PLAN_BLOB)) + canonical = json.dumps(word, sort_keys=True, separators=(",", ":")).encode() + require(sha256(canonical).hexdigest() == CANONICAL_WORD + == plan["source_canonical_sha256"], "Oracle canonical source word") + step = plan["steps"][0] + require((word["public"], word["owned_fields"], len(word["program"])) + == (767, 22, 25882), "Oracle fixed input inventory") + require((step["pivot"], step["frame"], step["time2"], step["queries"]) + == (696, 1031, 27044, [13750]), "Oracle fixed first-step scope") + require(step["source_sha256"] == CANONICAL_WORD, "Oracle step source pin") + require(step["collection"] == [{"time2": 27026, "role": 696, + "coefficient": "1"}], "Oracle fixed collection") + require([(c["time2"], c["role"], c["coefficient"]) + for c in step["injection"]] + == [(27044, 696, "1"), (27044, 697, "1"), + (27501, 770, "1"), (27516, 699, "1")], + "Oracle fixed injections") + size = word["public"] + word["owned_fields"] + collected = [Fraction(0) for _ in range(size)] + delivered = [Fraction(0) for _ in range(size)] + for contact in step["collection"]: + vector = prefix_functional(word, contact) + collected = [left + right for left, right in zip(collected, vector)] + individual = [] + for contact in step["injection"]: + vector = forward_delivery(word, contact) + delivered = [left + right for left, right in zip(delivered, vector)] + individual.append({"time2": contact["time2"], "role": contact["role"], + "delivered": sparse(vector)}) + require(sparse(collected) == {"696": "1"} == step["input"], + "Oracle exact collection on all input axes") + require(sparse(delivered) == step["output"], + "Oracle exact delivery on all output axes") + pairing = sum((a * b for a, b in zip(collected, delivered)), Fraction(0)) + require(pairing == 1 and delivered[696] == 1, "Oracle unit pairing and pivot") + main = set(word["live"]) | {r + 112 for r in word["live"]} + support = {i for i in range(size) if collected[i] or delivered[i]} + require(all(i < word["public"] and i not in main + and word["initial"][i] == 3 and word["final"][i] == 127 + for i in support), "Oracle independent full-boundary support") + require(133 in support and 133 not in main, + "Oracle derives helper eligibility without an ID cutoff") + # Here c=e_696 and d_696=1, so Q=I+(d-e_696)e_696^T. These + # literal source column/row checks establish TQ=QT without assuming a + # complete source endpoint theorem or replaying all its columns. + for index in sorted(support): + column = forward_delivery(word, {"time2": 0, "role": index, + "coefficient": "1"}) + require(sparse(column) == {str(index): "1"}, + "Oracle source identity column on basis support") + row = prefix_functional(word, {"time2": 2 * len(word["program"]), + "role": 696, "coefficient": "1"}) + require(sparse(row) == {"696": "1"}, + "Oracle source pivot row including arbitrary outside inputs") + return { + "status": "PASS_P104_ASYNC_FIRST_HUB_ORACLE", + "source_word_sha256": WORD_SHA256, + "canonical_word_sha256": CANONICAL_WORD, + "plan_sha256": PLAN_SHA256, + "axes": size, + "input_row": sparse(collected), + "output_column": sparse(delivered), + "individual_injections": individual, + "unit_pairing": str(pairing), + "eligible_support": sorted(support), + "source_identity_columns": sorted(support), + "source_identity_row": 696, + "basis_commutes_with_literal_source": True, + "scope": "Exact decoded temporal identities only; native phases, physical " + "contact legality, full source endpoint and complete price remain " + "separate obligations.", + } + + +if __name__ == "__main__": + result = run() + expected = json.loads((HERE / "ORACLE.json").read_bytes()) + require(json.dumps(result, sort_keys=True, separators=(",", ":")) + == json.dumps(expected, sort_keys=True, separators=(",", ":")), + "Frozen independent oracle receipt differs") + print(json.dumps(result, indent=2, sort_keys=True)) diff --git a/research/p104-async-first-hub-audit/verify.py b/research/p104-async-first-hub-audit/verify.py new file mode 100644 index 0000000000..f4ec32ee8f --- /dev/null +++ b/research/p104-async-first-hub-audit/verify.py @@ -0,0 +1,465 @@ +#!/usr/bin/env python3 +"""Independent data-only audit of PR5786's first temporal helper split. + +ToikY with substantial OpenAI Codex assistance. Apache-2.0. +The retained word and plan are Ali Romman's work; NOTICE preserves predecessors. +No predecessor Python code is imported or executed by this checker. +""" +from collections import Counter +from copy import deepcopy +from fractions import Fraction +from hashlib import sha256 +from pathlib import Path +import argparse +import gzip +import json + + +HERE = Path(__file__).resolve().parent +WORD_RAW = "7c393444fa5b9a6941471d02047beb2aa8285e5614bb052fb85458b69236a38a" +WORD_CANONICAL = "75f429fc0c8b206f4439bfbda4b621fc62ea892e6e3008c17409f2d3ee0981bb" +PLAN_RAW = "2c4878f78dc393339f8cccf24441d9bfb50257784459c2f253ebcb27c964211c" + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":")).encode() + + +def rational_map(value): + return {int(k): Fraction(v) for k, v in value.items() if Fraction(v)} + + +def encoded(vector): + return {str(k): str(v) for k, v in sorted(vector.items())} + + +def accumulate(destination, source, coefficient): + for key, value in source.items(): + new = destination.get(key, 0) + coefficient * value + if new: + destination[key] = new + else: + destination.pop(key, None) + + +def frame_spaces(word): + spaces = [] + for basis in word["frames"]: + values = {0} + for vector in basis: + require(type(vector) is int and 0 < vector < 512 and vector not in values, + "independent nine-bit frame basis") + values.update({old ^ vector for old in values}) + spaces.append(frozenset(values)) + return spaces + + +def forward_history(word, plan, spaces): + """Propagate every public and dirty-owned input, recording physical contacts.""" + public = word["public"] + size = public + word["owned_fields"] + rows = [{j: Fraction(1)} for j in range(size)] + frames = word["initial"][:] + [None] * word["owned_fields"] + live_owned = set() + wanted = {(item["time2"], item["role"]) + for kind in ("collection", "injection") for item in plan[kind]} + wanted.add((plan["time2"], plan["pivot"])) + snapshots = {} + lifetimes = peak = 0 + + def observe(time, middle=None): + for contact_time, role in wanted: + if contact_time != time: + continue + frame = plan["frame"] if middle and role == middle[1] else frames[role] + snapshots[time, role] = { + "row": rows[role].copy(), "frame": frame, + "owned_live": role in live_owned, + } + + for index, event in enumerate(word["program"]): + observe(2 * index) + opcode, target = event[:2] + require(type(target) is int and 0 <= target < size, "source target role") + if opcode == "MOVE": + _, _, entrance, exit_frame, private = event + require(frames[target] == entrance and (target in live_owned) == private, + "source MOVE frame and owned lifetime") + require(spaces[exit_frame] < spaces[entrance] if private + else spaces[entrance] < spaces[exit_frame], "source nested MOVE") + observe(2 * index + 1, event) + frames[target] = exit_frame + elif opcode == "INIT": + require(target >= public and target not in live_owned, + "source owned initialization") + live_owned.add(target) + lifetimes += 1 + peak = max(peak, len(live_owned)) + rows[target] = {} + frames[target] = event[2] + elif opcode == "CLEAR": + require(target in live_owned and frames[target] == event[2], + "source owned erasure frame") + # This models the predecessor's charged erasure operation. It does + # not assume the buffer was zero before CLEAR. + rows[target] = {} + frames[target] = None + live_owned.remove(target) + else: + coefficient = Fraction(event[-2]) + require(coefficient and frames[target] == event[-1], + "source scalar destination frame") + if opcode == "SCALE": + rows[target] = {key: coefficient * value + for key, value in rows[target].items()} + else: + require(opcode in ("ADD", "COPY"), "source scalar opcode") + source = event[2] + require(source != target and 0 <= source < size + and frames[source] == frames[target], "source common scalar frame") + if opcode == "COPY": + require(target in live_owned and not rows[target], + "source COPY into cleared owned field") + rows[target] = {} + accumulate(rows[target], rows[source], coefficient) + observe(2 * len(word["program"])) + require(not live_owned and frames[:public] == word["final"] + and frames[public:] == [None] * word["owned_fields"], "source boundary frames") + live = set(word["live"]) + for output, row in enumerate(rows): + expected = {output: Fraction(1)} if output < public else {} + if output - 112 in live: + expected[output - 112] = Fraction(1) + require(row == expected, "source full arbitrary-input endpoint") + return snapshots, { + "input_columns": size, "output_rows": size, + "coefficient_positions_checked": size * size, + "endpoint": "I + sum e_(r+112) e_r^T on public coordinates; zero owned outputs", + "endpoint_sha256": sha256(canonical([encoded(row) for row in rows])).hexdigest(), + "owned_lifetimes": lifetimes, "peak_live_owned": peak, + } + + +def suffix_columns(word, plan): + """Reverse-mode delivery propagation, independent of the forward row table.""" + size = word["public"] + word["owned_fields"] + effects = [{j: Fraction(1)} for j in range(size)] + wanted = {(item["time2"], item["role"]) for item in plan["injection"]} + snapshots = {} + + def observe(time): + for contact_time, role in wanted: + if contact_time == time: + snapshots[time, role] = effects[role].copy() + + observe(2 * len(word["program"])) + for index in range(len(word["program"]) - 1, -1, -1): + event = word["program"][index] + opcode, target = event[:2] + if opcode in ("INIT", "CLEAR"): + effects[target] = {} + elif opcode == "SCALE": + coefficient = Fraction(event[-2]) + effects[target] = {key: coefficient * value + for key, value in effects[target].items()} + elif opcode in ("ADD", "COPY"): + accumulate(effects[event[2]], effects[target], Fraction(event[-2])) + if opcode == "COPY": + effects[target] = {} + else: + require(opcode == "MOVE", "reverse source opcode") + observe(2 * index) + if opcode == "MOVE": + observe(2 * index + 1) + return snapshots + + +def audit_plan(word, plan, spaces, prefixes, suffixes): + require(plan["source_sha256"] == WORD_CANONICAL, "step source binding") + frame, cut = plan["frame"], plan["time2"] + queries = plan["queries"] + require(len(queries) == len(set(queries)), "distinct paid queries") + for kind in ("collection", "injection"): + for item in plan[kind]: + time, role = item["time2"], item["role"] + require(type(time) is int and 0 <= time <= 2 * len(word["program"]), + "contact time range") + require(type(role) is int and 0 <= role < word["public"] + word["owned_fields"] + and Fraction(item["coefficient"]), "contact operand") + require(time <= cut if kind == "collection" else cut <= time, + "causal collection/cut/injection order") + require(time % 2 == 0 or time // 2 in queries, "unpaid interior contact") + require(prefixes[time, role]["frame"] == frame, "actual contact frame") + require([word["program"][index] for index in sorted(queries)] == plan["query_events"], + "exact paid query binding") + require(prefixes[cut, plan["pivot"]]["frame"] == frame, "physical pivot at cut") + query_receipts = [] + delta = Counter() + for index in sorted(queries): + event = word["program"][index] + require(event[0] == "MOVE", "paid contact subdivides MOVE") + _, role, entrance, exit_frame, private = event + require(spaces[exit_frame] < spaces[frame] < spaces[entrance] if private + else spaces[entrance] < spaces[frame] < spaces[exit_frame], + "strict actual intermediate GF2 frame") + a, middle, b = (len(word["frames"][j]) for j in (entrance, frame, exit_frame)) + ranks = [abs(a - middle), abs(middle - b)] + delta.update(ranks) + delta[abs(a - b)] -= 1 + query_receipts.append({"index": index, "event": event, + "frame_dimensions": [a, middle, b], + "replacement_ranks": ranks, "replaced_rank": abs(a - b)}) + collection, delivery = {}, {} + for item in plan["collection"]: + accumulate(collection, prefixes[item["time2"], item["role"]]["row"], + Fraction(item["coefficient"])) + for item in plan["injection"]: + accumulate(delivery, suffixes[item["time2"], item["role"]], + Fraction(item["coefficient"])) + require(collection == rational_map(plan["input"]), "complete temporal collection row") + require(delivery == rational_map(plan["output"]), "complete temporal delivery column") + main = set(word["live"]) | {role + 112 for role in word["live"]} + eligible = {role for role in range(word["public"]) if role not in main + and word["initial"][role] == 3 and word["final"][role] == 127} + require(set(collection) | set(delivery) <= eligible, "actual independent full-boundary helpers") + pairing = sum(value * delivery.get(role, 0) for role, value in collection.items()) + require(pairing == 1 and delivery.get(plan["pivot"]), "unit pairing and physical pivot") + return { + "collection_row": encoded(collection), "delivery_column": encoded(delivery), + "pairing": str(pairing), "eligible_full_boundary_helpers": len(eligible), + "helper_133_is_eligible": 133 in eligible, + "paid_access": query_receipts, + "paid_access_delta": {str(rank): count for rank, count in sorted(delta.items()) if count}, + } + + +def split_replay(word, plan, spaces, omit_clear=False, omit_swap_scale=False): + """Emit and replay the first split on an independent formal label namespace.""" + original_size = word["public"] + word["owned_fields"] + fresh, buffer = original_size, original_size + 1 + size = original_size + 2 + pivot, frame, cut = plan["pivot"], plan["frame"], plan["time2"] + delivery = rational_map(plan["output"]) + require(rational_map(plan["input"]) == {pivot: Fraction(1)} + and delivery[pivot] == 1, "specialized first-step boundary basis") + basis = [(role, coefficient) for role, coefficient in sorted(delivery.items()) + if role != pivot] + events = [["ADD", role, pivot, str(coefficient), 3] for role, coefficient in basis] + first = min(item["time2"] for item in plan["collection"]) + last = max(item["time2"] for item in plan["injection"]) + + def renamed(event, time): + result = event[:] + for position in ((1, 2) if event[0] in ("ADD", "COPY") else (1,)): + if time >= cut and result[position] == pivot: + result[position] = fresh + return result + + def swap(left, right, first_swap=False): + events.extend([["ADD", left, right, "1", frame], + ["ADD", right, left, "-1", frame], + ["ADD", left, right, "1", frame]]) + if not (first_swap and omit_swap_scale): + events.append(["SCALE", right, "-1", frame]) + + def contact(time): + if time == first: + events.append(["INIT", buffer, frame]) + for item in plan["collection"]: + if item["time2"] == time: + events.append(["ADD", buffer, item["role"], item["coefficient"], frame]) + if time == cut: + swap(pivot, buffer, first_swap=True) + swap(fresh, buffer) + events.append(["ADD", buffer, pivot, "-1", frame]) + for item in plan["injection"]: + if item["time2"] == time: + role = fresh if item["role"] == pivot else item["role"] + events.append(["ADD", role, buffer, item["coefficient"], frame]) + if time == last and not omit_clear: + events.append(["CLEAR", buffer, frame]) + + for index, event in enumerate(word["program"]): + contact(2 * index) + if index in plan["queries"]: + _, role, entrance, exit_frame, private = event + events.append(renamed(["MOVE", role, entrance, frame, private], 2 * index)) + contact(2 * index + 1) + events.append(renamed(["MOVE", role, frame, exit_frame, private], 2 * index + 1)) + else: + events.append(renamed(event, 2 * index)) + contact(2 * len(word["program"])) + events.extend([["ADD", role, fresh, str(-coefficient), 127] + for role, coefficient in reversed(basis)]) + + rows = [{role: Fraction(1)} for role in range(size)] + frames = word["initial"][:] + [None] * word["owned_fields"] + [frame, None] + owned = set(range(word["public"], original_size)) | {buffer} + live_owned = set() + lifetimes = peak = buffer_inits = buffer_clears = 0 + before_clear = None + for event in events: + opcode, target = event[:2] + require(type(target) is int and 0 <= target < size, "split target role") + if opcode == "INIT": + require(target in owned and target not in live_owned, + "split owned initialization") + live_owned.add(target) + lifetimes += 1 + peak = max(peak, len(live_owned)) + buffer_inits += int(target == buffer) + rows[target] = {} + frames[target] = event[2] + elif opcode == "CLEAR": + require(target in live_owned and frames[target] == event[2], + "split owned erasure frame") + if target == buffer: + before_clear = rows[target].copy() + buffer_clears += 1 + rows[target] = {} + frames[target] = None + live_owned.remove(target) + elif opcode == "MOVE": + _, _, entrance, exit_frame, private = event + require(frames[target] == entrance and (target in live_owned) == private, + "split MOVE frame and ownership") + require(spaces[exit_frame] < spaces[entrance] if private + else spaces[entrance] < spaces[exit_frame], "split strict nested MOVE") + frames[target] = exit_frame + else: + coefficient = Fraction(event[-2]) + require(coefficient and frames[target] == event[-1], + "split scalar destination frame") + if opcode == "SCALE": + rows[target] = {key: coefficient * value + for key, value in rows[target].items()} + else: + require(opcode in ("ADD", "COPY"), "split scalar opcode") + source = event[2] + require(source != target and 0 <= source < size + and frames[source] == frames[target], "split common scalar frame") + if opcode == "COPY": + require(target in live_owned and not rows[target], + "split COPY into cleared owned field") + rows[target] = {} + accumulate(rows[target], rows[source], coefficient) + live = set(word["live"]) + for role, row in enumerate(rows): + expected = {role: Fraction(1)} if role < word["public"] or role == fresh else {} + if role - 112 in live: + expected[role - 112] = Fraction(1) + require(row == expected, "split arbitrary-input endpoint at role " + str(role)) + expected_frames = word["final"][:] + [None] * word["owned_fields"] + [127, None] + expected_frames[pivot] = frame + require(frames == expected_frames and not live_owned, "split final frames and owned closure") + require(before_clear == {fresh: Fraction(1), pivot: Fraction(-1)}, + "split retained buffer before charged erasure") + require(buffer_inits == buffer_clears == 1 and lifetimes == 25 and peak <= 13, + "split charged owned lifetime census") + return { + "formal_input_axes": size, "coefficient_positions_checked": size * size, + "fresh_public_label": fresh, "new_owned_buffer_label": buffer, + "retired_pivot_final_frame": frame, "fresh_final_frame": 127, + "program_events": len(events), "owned_lifetimes": lifetimes, + "peak_live_owned": peak, "new_buffer_init_count": buffer_inits, + "new_buffer_clear_count": buffer_clears, "before_clear_row": encoded(before_clear), + "endpoint_sha256": sha256(canonical([encoded(row) for row in rows])).hexdigest(), + "event_stream_sha256": sha256(canonical(events)).hexdigest(), + "label_scope": "Independent namespace; not a byte-identity claim for the author's emitted word", + } + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--emit", action="store_true", + help="emit a candidate result without comparing RESULT.json; never writes files") + args = parser.parse_args() + raw = (HERE / "inputs/WORD.json.gz").read_bytes() + plan_bytes = (HERE / "inputs/PLAN.json").read_bytes() + require(sha256(raw).hexdigest() == WORD_RAW, "raw source WORD authentication") + require(sha256(plan_bytes).hexdigest() == PLAN_RAW, "raw PLAN authentication") + word, plans = json.loads(gzip.decompress(raw)), json.loads(plan_bytes) + require(sha256(canonical(word)).hexdigest() == WORD_CANONICAL, + "canonical source WORD authentication") + require(plans["source_canonical_sha256"] == WORD_CANONICAL, "PLAN source binding") + require(word["public"] == 767 and word["owned_fields"] == 22 + and len(word["program"]) == 25882, "fixed source dimensions") + plan = plans["steps"][0] + require((plan["pivot"], plan["frame"], plan["time2"]) == (696, 1031, 27044), + "fixed first-step contact") + spaces = frame_spaces(word) + prefixes, endpoint = forward_history(word, plan, spaces) + suffixes = suffix_columns(word, plan) + result = audit_plan(word, plan, spaces, prefixes, suffixes) + require(result["collection_row"] == {"696": "1"}, "first-step exact input") + require(result["delivery_column"] == {"133": "2", "696": "1", "697": "1", + "699": "1", "709": "1", "733": "1"}, + "first-step exact output including helper hole") + require(result["paid_access_delta"] == {"3": 1, "4": 1, "7": -1}, + "first-step actual paid subdivision") + require(prefixes[27501, 770]["owned_live"], "owned injection is in its live interval") + controls = [] + changes = [ + ("omitted_collection", "complete temporal collection row", + lambda p: p.update(collection=[])), + ("omitted_owned_injection", "complete temporal delivery column", + lambda p: p["injection"].pop(2)), + ("injection_before_cut", "causal collection/cut/injection order", + lambda p: p["injection"][0].update(time2=27042)), + ("wrong_source", "step source binding", + lambda p: p.update(source_sha256="0" * 64)), + ("unpaid_owned_interior_query", "unpaid interior contact", + lambda p: p.update(queries=[])), + ] + for name, expected, change in changes: + bad = deepcopy(plan) + change(bad) + try: + audit_plan(word, bad, spaces, prefixes, suffixes) + except ValueError as error: + require(str(error) == expected, "control rejected for unintended reason: " + name) + controls.append({"name": name, "rejected": True, "reason": str(error)}) + else: + raise ValueError("control accepted: " + name) + split = split_replay(word, plan, spaces) + for name, options in (("omitted_new_buffer_CLEAR", {"omit_clear": True}), + ("omitted_first_swap_SCALE", {"omit_swap_scale": True})): + try: + split_replay(word, plan, spaces, **options) + except ValueError as error: + require(str(error).startswith("split arbitrary-input endpoint at role "), + "split control rejected for unintended reason: " + name) + controls.append({"name": name, "rejected": True, "reason": str(error)}) + else: + raise ValueError("split control accepted: " + name) + contacts = [] + for kind in ("collection", "injection"): + for item in plan[kind]: + physical = prefixes[item["time2"], item["role"]] + contacts.append({"kind": kind, **item, "actual_frame": physical["frame"], + "owned_live": physical["owned_live"]}) + output = { + "schema": "p104-async-first-hub-audit/1", + "scope": "Finite exact first-step temporal contacts and literal scalar/frame restoration; no native phase, full caller or kappa admission", + "source_raw_sha256": WORD_RAW, "source_canonical_sha256": WORD_CANONICAL, + "plan_raw_sha256": PLAN_RAW, "source_endpoint": endpoint, + "pivot": plan["pivot"], "frame": plan["frame"], "cut_time2": plan["time2"], + "contacts": contacts, **result, "literal_first_split": split, + "failure_controls": controls, + "erasure_scope": "INIT/CLEAR use the predecessor's charged owned-erasure semantics", + } + if not args.emit: + require(canonical(output) == canonical(json.loads( + (HERE / "RESULT.json").read_text(encoding="utf-8"))), + "frozen RESULT.json mismatch") + print(json.dumps(output, sort_keys=True, indent=2)) + print("PASS_P104_ASYNC_FIRST_HUB_AUDIT") + + +if __name__ == "__main__": + main()