diff --git a/research/bit-r438-source-code/ADAPTATIONS.json b/research/bit-r438-source-code/ADAPTATIONS.json new file mode 100644 index 0000000000..510eb2b34d --- /dev/null +++ b/research/bit-r438-source-code/ADAPTATIONS.json @@ -0,0 +1,56 @@ +[ + { + "path": "producer/bit_transvection.py", + "original_sha256": "97cb9f6bd3c29fc509e929fbeaec503defe3584da5736786719b2641e096f2fd", + "adapted_sha256": "4706d7e03fd9194e89914e0ee92b1d009ef25a2c14e45ddc6226ef181e68a52b", + "changes": "Repo default made relative; registered driver explicitly binds actual repo and fresh output." + }, + { + "path": "producer/bit_section_code.py", + "original_sha256": "4b35d963e07e062eddd093854d34c449d720d5140480f0c1ddd6fefef8c3472c", + "adapted_sha256": "4b35d963e07e062eddd093854d34c449d720d5140480f0c1ddd6fefef8c3472c", + "changes": "Exact original research source; module output binding supplied by registered driver." + }, + { + "path": "producer/bit_scalar_invoice.py", + "original_sha256": "8ed16fd022ba8f57cac1d1962fa845794181c308ffd9ed5bedb1b91fa3cb7c24", + "adapted_sha256": "8ed16fd022ba8f57cac1d1962fa845794181c308ffd9ed5bedb1b91fa3cb7c24", + "changes": "Exact original research source; module output binding supplied by registered driver." + }, + { + "path": "producer/bit_signed_lift.py", + "original_sha256": "e5e7bc86255c3a6c8f6eef7bc4bb759b9ac66a394fe87894ab43eb14b7853e36", + "adapted_sha256": "e5e7bc86255c3a6c8f6eef7bc4bb759b9ac66a394fe87894ab43eb14b7853e36", + "changes": "Exact original research source; module output binding supplied by registered driver." + }, + { + "path": "native_caps.py", + "original_sha256": "6e9ca1eb905d769716c009904f45d6849b225e48cd119f18b50c0379f35313cb", + "adapted_sha256": "cd1772b0780d5882b5ae50c268732848f102108b9f02a564c86773eba7916e72", + "changes": "Exact AST-selected local function bodies: need, canonical, rank, identity, multiply, exchange, address_identities. Global controller and unused main removed." + }, + { + "path": "signed_rows.py", + "original_sha256": "376356696663021693c0e2c9adf37f371675fe8837fb88232b8767a8b90793e8", + "adapted_sha256": "16dff88980ab3043ae9d51c3109e8e284e031da5332af2cd9b2e8244afdc8292", + "changes": "Exact AST-selected local function bodies: identity, add, parity. Global controller and unused main removed." + }, + { + "path": "check.py", + "original_sha256": "d284714fd65054279c180454b73eb717382e402669d5a04e3f373d0d7f54bc06", + "changes": "Exact independent projected and execute function bodies retained. Portable main derives actual raw R/K/J and final A, compares the complete projected word/boundaries, verifies all651 integer/F2 columns, native caps and seven defect controls. No producer imports.", + "adapted_sha256": "110f0eaa897b83daa223aec038f7ef40ff785e9fb730eeb8d670b5b95132ea5e" + }, + { + "path": "producer/build_support_code.py", + "original_sha256": "4b3e1ae12194f3f1a2294ffa8f92b0cf02c8c3163bf530987081a08406f9475e", + "adapted_sha256": "dd24cd8cbce7aa8cf4c13e51afe202a460f827b2b7b97f63d609d4f8dc7e8415", + "changes": "Fresh output binding; remove sys.path insertion; replace fixed regenerated gzip pin with caller-supplied complete semantic ancestry authentication. Construction, support checks and defect controls unchanged." + }, + { + "path": "producer/prune.py", + "original_sha256": "3532caa0c7ed88401234f86a8aa3e5bab7e5640a737b2ec08a19635444832cdf", + "adapted_sha256": "4a555dbd3154caa853a9b327fff4aa8ddcc938c2af4dfb1f540c1c35ad359c1f", + "changes": "Fresh-output binding; remove sys.path insertion; replace regenerated fixed-gzip guard by complete semantic predecessor authentication. Projection, original integer endpoint equality and negative control unchanged." + } +] diff --git a/research/bit-r438-source-code/ARTIFACTS.json b/research/bit-r438-source-code/ARTIFACTS.json new file mode 100644 index 0000000000..ba048927b8 --- /dev/null +++ b/research/bit-r438-source-code/ARTIFACTS.json @@ -0,0 +1,24 @@ +{ + "format": "complete-package-sha256-v1", + "files": { + "ADAPTATIONS.json": "a4325f122f4da020bf54060b5d33fb048df6f31fc3be232930ae78e904eab43c", + "EXPECTED.json": "f078222ab4e99aff085262c00ba77520cc62eb02003d8e0582ab6ad7dab7f402", + "PROOF.md": "ebcc91e74938b525b28e46bf03ec09d42d24ab02070dc96f4f0a51cee2cfb83d", + "README.md": "f1033297e1156f9fb154a4319bee394a82476195cd2a53d01d93ef7332536d27", + "SOURCES.json": "adaa3aa444f224590ba152fe16dd76ccd8ff8bd8a0b19477076c4d79ce4b94cb", + "TASK.json": "fa2dd91db03f05e78d909ddf9c96e5cc000fbecfb80a6c074521215c8b9c8553", + "VERIFY.json": "3a8b8559683d5f8a61f8a34cf0cd54513892f2543345d7ba478470d02a1377b7", + "WORD.json.gz": "1a6841fccba51fa922993c77b4b296e659c2c538252e5e06113d0438c5edb870", + "check.py": "110f0eaa897b83daa223aec038f7ef40ff785e9fb730eeb8d670b5b95132ea5e", + "native_caps.py": "cd1772b0780d5882b5ae50c268732848f102108b9f02a564c86773eba7916e72", + "producer/bit_scalar_invoice.py": "8ed16fd022ba8f57cac1d1962fa845794181c308ffd9ed5bedb1b91fa3cb7c24", + "producer/bit_section_code.py": "4b35d963e07e062eddd093854d34c449d720d5140480f0c1ddd6fefef8c3472c", + "producer/bit_signed_lift.py": "e5e7bc86255c3a6c8f6eef7bc4bb759b9ac66a394fe87894ab43eb14b7853e36", + "producer/bit_transvection.py": "4706d7e03fd9194e89914e0ee92b1d009ef25a2c14e45ddc6226ef181e68a52b", + "producer/build_support_code.py": "dd24cd8cbce7aa8cf4c13e51afe202a460f827b2b7b97f63d609d4f8dc7e8415", + "producer/prune.py": "4a555dbd3154caa853a9b327fff4aa8ddcc938c2af4dfb1f540c1c35ad359c1f", + "reconstruct.py": "12ea8141d609bfc49166bff2bb3f24f477d69fca4260d3523491c8b614cd4929", + "signed_rows.py": "16dff88980ab3043ae9d51c3109e8e284e031da5332af2cd9b2e8244afdc8292", + "verify.py": "3bcec1c1c29eb0348960679b70706f77c70a4faa2a6e58533c9d2059ea27ab1f" + } +} diff --git a/research/bit-r438-source-code/EXPECTED.json b/research/bit-r438-source-code/EXPECTED.json new file mode 100644 index 0000000000..1ad8df8143 --- /dev/null +++ b/research/bit-r438-source-code/EXPECTED.json @@ -0,0 +1,54 @@ +{ + "source_word": "research/bit-r438-transport-rehost/words/r438-t154.json.gz", + "source_sha256": "a353999bceac4ac957f540adfd3e5f8768297138b27132eeb83332e2ea4b1022", + "canonical_word_sha256": "ebc33ee086f610c1fd540fa56bb99b2b96a768e4aed4a18defcb0e1f507fca89", + "frozen_gzip_sha256": "1a6841fccba51fa922993c77b4b296e659c2c538252e5e06113d0438c5edb870", + "semantic_word_sha256": "e5fa1dbcb80f61c7c728bad7cc166f368ec73c673828273bea091caba8708892", + "six_copy_semantic_sha256": "f44b26376769580295293b1e782568d81ed297647106450a13bd82ecf086dd1b", + "unsigned_section_semantic_sha256": "a50fcbbec51830f84f7368bc6153fe3340ef345849a6cf9ea287d624a753cea4", + "original_six_copy_canonical_sha256": "6448fb2b201c6be722087fc547064ec7c3135af5a72ed363434822212a9b2afc", + "normalized_fields": [ + "source_word", + "signed_from", + "parent_word_gzip_sha256" + ], + "normalization_contract": "The final word omits only checked source location and validated same-run parent compressed identity in semantic comparison. Signed ancestry also normalizes its validated same-run parent hash. All schemas, frames, signed records, deleted physical indices, register counts and original source hashes are compared completely. Immutable frozen inputs retain exact byte hashes.", + "profile": { + "1": 1298, + "2": 1342, + "3": 79, + "4": 44, + "5": 93, + "6": 11, + "7": 9 + }, + "counts": { + "0": 2873, + "1": 13223, + "2": 3, + "3": 3 + }, + "rank_mass": 4989, + "rank_saving": 132, + "source_matrix_sha256": "0ab35dade762a3050b6fc15f653041134f8d5a8015cbdbdc049be0528659240b", + "source_code_ADDs": 1499, + "prefix_row_l1": { + "forward": 34285, + "inverse": 5839860 + }, + "support_semantic_sha256": "c281439e7e78c74c8223e5adfebf34c2be945f308b0f7e53b928c700151cbd74", + "support_canonical_sha256": "3541eab8057c8cebadbd46775ff2d8e759fd592d8a1b9aebde834821d96c051b", + "public_registers": 651, + "dirty_helpers": 429, + "deleted_original_families": [ + 471, + 472, + 473, + 474, + 475, + 476, + 477, + 478, + 479 + ] +} diff --git a/research/bit-r438-source-code/PROOF.md b/research/bit-r438-source-code/PROOF.md new file mode 100644 index 0000000000..1fbd2cad0e --- /dev/null +++ b/research/bit-r438-source-code/PROOF.md @@ -0,0 +1,202 @@ +# Three copied source pivots for the actual R438 local word + +This is a finite, source-pinned local construction over F2, an exact signed +integer lift, and a conditional native cap calculation. It is neither a formal +kernel proof nor a complete recursive supplier or multiplication theorem. + +## Registers, frames and endpoint + +The final word has 111 sources x, 111 arbitrary targets y, 429 arbitrary dirty +helpers h and one owned private copied field. All 651 public input columns are +independent. Its construction first uses the 438-helper, 660-column source +word and then deletes nine literally unread physical families as proved below. The private field is zero outside its immutable snapshot +lifetimes. Sources enter at their actual port lines P_p, targets and helpers at +frame zero. Sources and helpers finish at FULL; target p finishes at its actual +cap K_p=P_p-perp. These are the original R438 boundary frames. + +For the explicit invertible binary matrix A constructed below, the new forward +endpoint is `(x,y,h) -> (Ax,y+Ax,h)`. Its literal inverse is +`(x,y,h) -> (A^-1 x,y+x,h)`. The source endpoint is changed. Original theorems +requiring an unchanged source cannot be applied without proving the new caller +contract. Complemented physical backward-call interpretation and the complete +compiler remain separate obligations. + +## Delete centres and rebuild the zero-frame compensation + +Replay D then A of the actual pinned word. The nine retained helper totals are +`R x+T h`, with R of shape 9-by-111. Let K be the actual 111-by-9 scatter matrix. +No original gate reads a target. The complete row masks of M=RK are +`507,135,238,349,185,437,205,503,425`. Both M and R have rank 9, while +N=I+M has rank 6. + +Delete the nine centre COPY/ERASE episodes and their target scatters. Over F2, +this changes the original target `y+x` by `KR x+KT h`. Replace its original +zero-frame compensation by `D_new=D_old+KT`. Duplicate helper-to-target gates +cancel at frame zero: 5,758 ADDs replace 18,030. Every original public frame +visit is retained, including empty-source visits. The resulting clean-centre +word has endpoint `(x,y,h) -> (x,y+Jx,h)`, where J=I+KR and rank(J)=108. +The verifier derives R,K,J from the literal original word and checks every +public input column; it does not assume a model scatter matrix. + +## An invertible source code with three actual repaired target rows + +Let C0 be a basis of the left nullspace of N, with emitted row masks +`39,193,272`. Let P select physical target coordinates 0,1,2 and S=RP. +The 3-by-3 matrix C0 S is invertible. Define + +``` +B0 = (C0 S)^-1 C0. +``` + +Thus B0 S=I and B0 N=0. Let D be rows 0,1,2 of K. Delete these rows +from K to form W=K+PD, and define + +``` +Y = N + S D, A = I + W R, Q = P B0 R. +``` + +The actual row masks of Y are `10,373,282,165,176,405,356,145,166`, of rank 9. +A fixes kernel(R) and induces the invertible map Y on the quotient identified +by R: RA=YR. Thus A is invertible. Equivalently, if Ax=0 then YRx=0, so +Rx=0 and Ax=x=0. Both matrix inverse identities are also checked finitely. +Rows 0,1,2 of A are exactly their identity rows. Since B0Y=D, + +``` +QA = P B0 R A = P B0 Y R = P D R, +(I+Q)A = I + (K+PD)R + PDR = I+KR = J. +``` + +After the full-frame source code, z=Ax and the target is y+Jx. Adding Qz +therefore gives y+Ax over F2. Q has exactly three nonzero physical rows, +0,1,2. The actual source-code rank is rank(A-I)=9; small target support does +not imply small source-code rank. + +Three repaired target rows are minimal in this declared class. For any +invertible A, rank(A+J) >= rank(A)-rank(J)=3. A correction supported on r +physical target rows has rank at most r. This excludes r<3 for this fixed +clean-centre J and invertible source recoding, not arbitrary suppliers. + +## Literal source code and one snapshot per repaired row + +Normalize R on actual source coordinates `0,1,2,4,8,9,14,30,59`. Commuting +CNOTs replace those coordinates by a query basis. In this basis A has an +invertible 9-by-9 query block and fanout to the other source coordinates. +Gaussian elimination synthesizes the small block with 47 CNOTs. The ordered +code uses `474 prepare + 504 fanout + 47 quotient + 474 inverse prepare`, +or 1,499 ADDs, all at FULL. It uses no extra helper or private field. + +For each nonzero row q=Q[p], choose a source index t with q[t]=1. All source +fields are at FULL. Add each z_i with i!=t and q[i]=1 to z_t. The prepared +field is exactly `sum_i q[i] z_i` over the integers: its original z_t is one +of the required terms, not an unknown extra offset. Copy this actual source +into the cleared private field at target p's cap, add it to target p, and +ERASE the copy while the physical source is unchanged. Undo the preparation +in reverse order with negated ADD coefficients. Every source is restored +exactly to its value before this episode. + +The chosen pivots are 0,1,2. Their preparations use 59,53,60 ADDs; their inverse +preparations use the same counts. Including three scatters gives 347 repair +ADDs. Only one private snapshot is live at a time. No dirty helper is touched +by these three repair episodes. The six-copy dirty-helper variant is retained +only as explicit reconstruction ancestry; it is not the final construction. + +## Integer and native boundaries + +The signed word negates the actual factory cleanup, source unpreparation and +repair unpreparation ADDs. Literal reversal negates every ADD coefficient. +The complete 651-column integer replay establishes source `A_Z x`, every +helper exactly h and the private field zero. The target is +`y+T_Z x+E_Z h`, where `T_Z mod2=A` and E_Z is even. Target correctness is +asserted modulo 2, not as integer equality to y+A_Z x. The reverse source is +`A_Z^-1 x`. Full integer roundtrip is checked separately; A is not assumed +involutive. Wrong unpreparation signs preserve parity but change the integer +source, and are rejected independently. + +For each actual rational E8 line vector u with squared norm 4, the checker +constructs P=uu^t/4 and K=I-P. It binds the actual entrance frame to P and +target frame to K, including all 222 bindings. For +`D_U=[[I-U,U],[U,I-U]]`, exact rational multiplication proves +`D_I D_P=D_K` and `D_P^2=I` on all 16 columns, for all 111 ports (3,552 checked +columns). Hence the FULL-to-cap copied-total residual is D_P of rank one, +under the inherited native ADDRESS/copied-total interface. Source and target +port labels need not agree: the physical source is FULL at the cut. + +The independent ordered-word audit checks common frames for every ADD, +monotone containment and rank for every MOVE, actual source COPY, immutable +source throughout each snapshot, exact ERASE and endpoint frames, in both +directions. These local identities do not establish a full physical native +compiler, rounded implementation or recursive hosting theorem. + +## Delete nine literally unread physical families + +In the signed three-copy word, precisely the old helper indices 471 through +479 are never read as ADD sources or COPY/ERASE sources. The independent +checker discovers this set by scanning every record. The only operations on +these fields are 72 ADD destinations and 36 MOVEs, with paid profile +`27 e1+9 e5`. The same no-read property holds in the literal inverse. + +Delete these nine physical input/output families, discard their destination +operations, and renumber every remaining operand in order, including the +private field from 660 to 651. No remaining value or frame depends on a +removed family. Induction through the literal word therefore identifies the +new execution with projection of the original execution, forward and inverse. +The constructor also checks exact integer endpoint projection, and the +independent checker compares the entire projected record list and both +boundary arrays before replaying all 651 independent columns. Every one of +the remaining 429 arbitrary helpers is restored exactly. The deleted families +are absent from the contract; they are not retained with unpaid endpoints. +A mutant that reads a discarded field is rejected before projection. + +This removes another 72 local rank units and 72 ADDs. It does not establish a +72-unit hosted saving: under the incumbent width-8 whole-family accounting, +returning nine families to idle-owner children adds `9*8=72` rank units per +local call at beta=0 (648 across nine calls). Thus that returned idle obligation +cancels the pruning reduction at this mass level. Changed chronological owners, +stock and complete higher moments remain outside this package. The local +132-unit reduction below must not be read as a net global gain. + +## Complete local invoice + +| Item | Pinned R438 | This word | +|---|---:|---:| +| Sources / targets / dirty helpers | 111 / 111 / 438 | 111 / 111 / 429 | +| Owned private fields / maximum live copies | 1 / 1 | 1 / 1 | +| ADDs | 24,248 | 13,223 | +| MOVE children | 2,909 | 2,873 | +| COPY / ERASE pairs | 9 | 3 | +| COPY ranks | 9 times 7 | 3 times 1 | +| Paid children | 2,918 | 2,876 | +| Rank mass | 5,121 | 4,989 | + +The complete profile is `{1:1298,2:1342,3:79,4:44,5:93,6:11,7:9}`. +Its exact change is `-9 e7-24 e1-9 e5`, saving 132 rank units per local invocation. +The ADD invoice is `5758 compensation + 5619 clean factory/cleanup + 1499 +source code + 347 repair`. No chronological owners, native allocation, +private reservation, code restoration or final decoder cost is removed from +a global bill by this local calculation. + +The exact signed prefix row norms are 34,285 forward and 5,839,860 inverse. +They are checked local arithmetic facts only. A new global perturbation/rounding +proof and precision reserve are required before using them in a supplier. + +## Verification and remaining conditions + +`reconstruct.py` regenerates the complete ordered word from the two pinned live +sources through the declared section and signed ancestry. The registered +verifier compares the full decompressed payload with `WORD.json.gz`. Only +validated source-location metadata and validated same-run compressed-parent +identities in signed/pruned ancestry are normalized. Every record, sign, frame, schema and register count +is compared. Immutable source and frozen word files retain exact byte hashes. + +`check.py` imports no producer. Its separate sparse integer interpreter checks +all 651 columns in both directions and the roundtrip, actual R/K/J, source +inverse, all dirty restoration, all target parity, complete profile and exact +rational native caps. Eleven ancestry fault checks and seven independent controls +cover missing compensation/unpreparation, mutable snapshots, wrong inverse +code, wrong integer signs, FULL-copy rank, a corrupt section query and a read of a deleted family. + +Open global obligations include composition of the changed source interface, +terminal code removal at the actual caps, physical helper/owner/access and +storage schedules, rounded cleanup and precision, recursive caller contracts, +and a full joint complex/BIT outer transfer. This local result supplies none +of those admissions and claims no new kappa. diff --git a/research/bit-r438-source-code/README.md b/research/bit-r438-source-code/README.md new file mode 100644 index 0000000000..e501165027 --- /dev/null +++ b/research/bit-r438-source-code/README.md @@ -0,0 +1,88 @@ +# Three source snapshots replace nine R438 centres + +This source-pinned local BIT construction replaces nine rank-7 copied centres +with three rank-1 snapshots of prepared actual source fields. Deleting nine subsequently unread physical helper families gives a +complete +local rank mass of **4,989 instead of 5,121**, **13,223 instead of 24,248 ADDs**, +and **429 instead of 438 arbitrary dirty helpers**, with one owned private field. + +The changed F2 contract is `(x,y,h) -> (Ax,y+Ax,h)`, with an explicit invertible +111-by-111 source code A. Its literal inverse is `(A^-1 x,y+x,h)`. A has +rank(A-I)=9. Three actual repaired target rows are minimal for the fixed +clean-centre map J and invertible source recoding. This is a finite local +construction and written proof, **not a new kappa or global supplier claim**. + +The 132-unit reduction is local only. Under incumbent width-8 family +accounting, returned idle-owner children add 72 rank units per local call at +beta=0, cancelling the extra 72-unit pruning reduction. Full owner and moment +accounting remain open; this is not a net global 132-unit saving. + +The signed integer lift restores every dirty helper exactly and maps the +source to A_Z x. The target formula is only asserted modulo 2. The separate +native audit verifies exact rational cap ADDRESS identities under the +copied-total interface; it is not a new physical compiler theorem. +[PROOF.md](PROOF.md) gives the section derivation, source-pivot word, full bill, +integer distinction and remaining hypotheses. + +## Reproduce + +Use Python 3.12 and the two live source paths declared in [VERIFY.json](VERIFY.json): + +```sh +python3.12 scripts/research_package.py --package research/bit-r438-source-code +# Direct replay also works in the committed Git-free package export: +python3.12 -I -O -B -Werror research/bit-r438-source-code/verify.py --out /tmp/r438-fresh-result +``` + +The output path must be fresh and outside the package. The standard-library +replay regenerates the entire word, compares complete decompressed contents, +then independently checks all 651 integer/F2 columns forward and inverse, +all 429 dirty helpers, the roundtrip, all frame/rank events, 111 rational cap +projectors and 3,552 ADDRESS columns. Eleven construction-ancestry and seven +independent defect controls execute. Verification reads source files and writes +only external runtime output. The registered cap is 600 seconds. + +[WORD.json.gz](WORD.json.gz) has full canonical SHA256 +`ebc33ee086f610c1fd540fa56bb99b2b96a768e4aed4a18defcb0e1f507fca89`. +[EXPECTED.json](EXPECTED.json) specifies the complete semantic comparison. +Gzip container bytes produced by different zlib implementations are not a +regenerated-word acceptance criterion. Only checked source-location and +same-run compressed-parent provenance fields are normalized; scientific +contents are compared in full. The frozen input itself has an exact byte pin. + +[SOURCES.json](SOURCES.json) binds both live main inputs and historical task +provenance at `20ecf2891d80b5acf18d980b2164fb44ea7faa90`. +[ADAPTATIONS.json](ADAPTATIONS.json) identifies the new research producer and +independent audit source hashes and the precise portability/extraction changes. +The six-copy and unpruned three-copy intermediates exist only inside reconstruction +ancestry. The public result and proof describe the final three-copy word consistently. +[VALIDATION.json](VALIDATION.json) records actual local validation separately +from hosted CI. + +## Open next questions + +- Can the coded source interface be composed and its terminal code removed at + the actual capped target endpoints for a fully priced global supplier? +- Can that complete word obtain a rigorous rounded cleanup/precision bound + and a physical owner, access and tape schedule within a useful joint budget? + +[TASK.json](TASK.json) gives concrete first steps and blockers. Local prefix +norms and the rank saving do not settle these obligations. Existing family +ceilings apply only under their original hypotheses; this change does not +establish a new coverage law or authorize an unbounded construction round. + +## Sources and credit + +The live R438 word and baseline replay retain Ali Romman's construction and +boundary-persistence work, Sagar Thakrar's transport/rehosting work, and the +DreamingOfClouds/eumemic/PR589/PR555/PR543/PR545/PR510 lineage credited by those sources. +Ali Romman's [PR1862](https://github.com/CrocSwap/integer-mult-bounds/pull/1862) +(`bb29ea73ad9be9a0c3d53cdcb1d22b2ee9ffe42f`) +provides the prior ordered-ring source-code/unit-transfer motif. Hanson +Sun/bbMisk's [PR1522](https://github.com/CrocSwap/integer-mult-bounds/pull/1522) +provides related restored mutable-source-query tours. These are conceptual +predecessors, not runtime imports or claims that generic source coding is new. + +Ross Richardson, with substantial OpenAI Codex assistance in construction, +independent agent audit, proof and packaging. The audit is a separate AI +implementation, not human review or formal-kernel verification. Apache-2.0. diff --git a/research/bit-r438-source-code/SOURCES.json b/research/bit-r438-source-code/SOURCES.json new file mode 100644 index 0000000000..716a784d21 --- /dev/null +++ b/research/bit-r438-source-code/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + }, + { + "path": "research/bit-boundary-persistence/build.py", + "usage": "input", + "git_blob": "074d045cf6a5de84f67bd772ae422edc051d3c6e", + "sha256": "58f402c365eb18b9c3dd736523999676f1d1652e40c1a9b4f6967c1b7acb72df" + }, + { + "path": "research/bit-r438-transport-rehost/words/r438-t154.json.gz", + "usage": "input", + "git_blob": "e12a566658a4b2c8b6ae0ecc34fd41290f68f5e8", + "sha256": "a353999bceac4ac957f540adfd3e5f8768297138b27132eeb83332e2ea4b1022" + } + ] +} diff --git a/research/bit-r438-source-code/TASK.json b/research/bit-r438-source-code/TASK.json new file mode 100644 index 0000000000..b9cc1450ed --- /dev/null +++ b/research/bit-r438-source-code/TASK.json @@ -0,0 +1,71 @@ +{ + "schema_version": 1, + "task_id": "coverage-law-change", + "priority_revision": 6, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "original_card": { + "id": "coverage-law-change", + "question": "Can a template or call contract leave two or more unpaid coordinates per live family?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/idle-axis-hosting/PROOF.md", + "certificates/selected-result.json" + ], + "methods": [ + "State a replacement for the coverage identity (mass = 72W + 64N) and the contract change that realizes it, with its implementation cost.", + "Find an obstruction: show which data-endpoint obligation forces exactly one unpaid coordinate in the current template." + ], + "acceptance_gate": "An explicit replacement identity, verified on a small complete instance with dirty inputs, priced with ceiling.ceiling(unpaid=...). A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Explain where the single unpaid coordinate per family comes from in the hosted template; propose one change and price it. Ideal budget: two unpaid coordinates per family is 3.77x (levers.py).", + "bottleneck_link": "The deficit is one coordinate per family minus the centre charge; doubling unpaid coordinates per family scales it directly.", + "allowed_variations": [ + "One template change or one endpoint-contract change.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Counting a coordinate as unpaid while leaving it unadvanced in the data endpoint.", + "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts." + ], + "overlap_terms": [ + "coverage identity", + "unpaid coordinate", + "deficit law", + "W - 64N" + ] + }, + "scope_status": "changed", + "actual_scope": "Source-pinned R438 local source-code replacement with three actual target repairs and deletion of nine unread physical families, giving 429 dirty helpers; exact signed restoration and complete local frame/rank invoice.", + "scope_change_reason": "The original card asks for a new full coverage law. This scoped contribution changes the local source contract and prices its literal word; it does not claim an all-family law or global supplier. The priority-6 family gate permits independently useful local results without global expansion.", + "bottleneck_link": "Nine rank-7 copied centres become three rank-1 source snapshots; nine subsequently unread helpers are deleted. Local mass 5121->4989. Returning those nine width-8 families to idle-owner children cancels 72 of the local reduction at beta=0 under incumbent accounting. The source endpoint changes, and terminal decoding plus all global implementation costs remain open.", + "budget_minutes": 240, + "stop_rule": "Stop after one source-closed local construction and independent replay; no global supplier or kappa admission without complete caller, native, precision, owner, tape and joint outer obligations.", + "outcome": "partial", + "evidence": "PROOF.md; WORD.json.gz; registered verify.py regenerates and independently checks the complete local result.", + "author": "Ross Richardson, with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance, including separate producer and independent audit agents; no human or formal-kernel review claimed.", + "open_questions": [ + { + "question": "Can the changed source code be composed and its terminal code removed at the actual cap endpoints?", + "why_it_matters": "A local source-code saving is not a global supplier saving until the caller interface and decoder costs are paid.", + "first_step": "Write the exact global source/target code and price a literal cap-compatible terminal decoder, including dirty restoration.", + "blocked_by": "No full endpoint/decoder construction is admitted by this package." + }, + { + "question": "Does a fully composed word meet rounded precision, owner, access and physical tape bounds in a useful joint budget?", + "why_it_matters": "The local signed prefix norms and frame invoice do not establish the recursive implementation contract.", + "first_step": "After a concrete global word exists, derive complete perturbation weights and chronological physical storage/call bounds before any outer transfer.", + "blocked_by": "The global word and complete caller/decoder contract are unresolved here." + } + ] +} diff --git a/research/bit-r438-source-code/VALIDATION.json b/research/bit-r438-source-code/VALIDATION.json new file mode 100644 index 0000000000..00220476fd --- /dev/null +++ b/research/bit-r438-source-code/VALIDATION.json @@ -0,0 +1,83 @@ +{ + "status": "PASS_LOCAL_REGISTERED_SCOPE", + "scientific_result": { + "address_columns": 3552, + "ancestry_controls": 11, + "canonical_frozen_word_sha256": "ebc33ee086f610c1fd540fa56bb99b2b96a768e4aed4a18defcb0e1f507fca89", + "columns": 651, + "counts": { + "0": 2873, + "1": 13223, + "2": 3, + "3": 3 + }, + "dirty_helpers": 429, + "frame_bindings": 222, + "independent_controls": [ + "wrong_integer_unprepare_sign", + "omit_pivot_unprepare", + "FULL_to_FULL_copy", + "mutate_live_source", + "reuse_noninvolutive_code_as_inverse", + "wrong_section_query", + "read_deleted_family" + ], + "native_projectors": 111, + "no_new_kappa": true, + "profile": { + "1": 1298, + "2": 1342, + "3": 79, + "4": 44, + "5": 93, + "6": 11, + "7": 9 + }, + "python": "3.12.12 (main, Oct 9 2025, 11:07:00) [Clang 17.0.0 (clang-1700.6.3.2)]", + "rank_mass": 4989, + "rank_saving": 132, + "scope": "Exact local signed and F2 operators, complete common-frame/rank invoice and rational cap ADDRESS identities; no global compiler, precision, owner or kappa admission", + "seconds": 14.474679999999353, + "semantic_word_sha256": "e5fa1dbcb80f61c7c728bad7cc166f368ec73c673828273bea091caba8708892", + "stages": [ + "reconstruct", + "check" + ], + "status": "PASS_R438_THREE_SOURCE_COPIES_LOCAL_ONLY" + }, + "command": [ + "python3.12", + "-I", + "-O", + "-B", + "-Werror", + "research/bit-r438-source-code/verify.py", + "--out", + "FRESH_EXTERNAL_OUTPUT" + ], + "separate_ai_audit": { + "source_sha256": "d284714fd65054279c180454b73eb717382e402669d5a04e3f373d0d7f54bc06", + "receipt_sha256": "4efc043e71ba125bacfcdb1e2ed638dee685479846f70b2d863e889a5c075ec9", + "support_audit_source_sha256": "1c2687271b96b8e3bee1da9572b1af7596b4e506d8d803293af5b974ba057272", + "support_audit_receipt_sha256": "feb4e3ae776afad07802ef277d022f8bac6aeb177d7fe2057c35d75a03574164", + "scope": "Separate audit of exact unread-family projection, all651 signed/F2 columns,429 helpers and full invoice. Public check.py retains its exact projected/execute function bodies and adds direct original-word matrix derivation, native cap identities and seven fault controls. No human/formal review implied." + }, + "metadata": "PASS_PACKAGE_METADATA_AND_PINS", + "committed_byte_source_history": "pending final commit", + "committed_git_free_export": "pending final commit", + "hosted_ci": "not yet published", + "limitations": [ + "No global controller, terminal decoder, precision, owner/tape or kappa admission.", + "Two live source inputs are ancestral canonical20ec bytes; full original Git history required only by metadata/source-history gates." + ], + "registered_runner": { + "status": "PASS_REGISTERED_RESEARCH_PACKAGE", + "seconds": 14.44879658300124, + "command": [ + "python3.12", + "scripts/research_package.py", + "--package", + "research/bit-r438-source-code" + ] + } +} diff --git a/research/bit-r438-source-code/VERIFY.json b/research/bit-r438-source-code/VERIFY.json new file mode 100644 index 0000000000..bafb74f7ce --- /dev/null +++ b/research/bit-r438-source-code/VERIFY.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/bit-boundary-persistence/build.py", + "research/bit-r438-transport-rehost/words/r438-t154.json.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "-Werror", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Complete live-source regeneration and literal dead-family projection, decompressed word equality, independent 651-column integer/F2 forward and inverse, all 429 helper restoration, 111 exact native cap identities, full frame/rank invoice, eleven ancestry and seven independent defect controls." + } + ] +} diff --git a/research/bit-r438-source-code/WORD.json.gz b/research/bit-r438-source-code/WORD.json.gz new file mode 100644 index 0000000000..672c415346 Binary files /dev/null and b/research/bit-r438-source-code/WORD.json.gz differ diff --git a/research/bit-r438-source-code/check.py b/research/bit-r438-source-code/check.py new file mode 100644 index 0000000000..9da42bb5ff --- /dev/null +++ b/research/bit-r438-source-code/check.py @@ -0,0 +1,232 @@ +#!/usr/bin/env python3 +"""Independent sparse integer / F2 endpoint and rational native-cap replay. + +No producer module is imported. Every public input is an independent column. +""" +from collections import Counter +import argparse +import gzip +import hashlib +import json +from pathlib import Path +import types + +HERE = Path(__file__).resolve().parent + +def load(name): + path = HERE / (name + ".py") + module = types.ModuleType(name) + exec(compile(path.read_bytes(), str(path), "exec"), module.__dict__) + return module + +cap, scalar = load("native_caps"), load("signed_rows") +need = cap.need + +def projected(program): + dead = [h for h in range(222,660) + if all(not(op == 1 and s == h or op in (2,3) and d == h) + for op,d,s,c,f,p in program['records'])] + need(dead == list(range(471,480)),'unread physical helper classification') + dead_set = set(dead) + keep = [p for p in range(660) if p not in dead_set] + mapping = {old:new for new,old in enumerate(keep)} + mapping[660] = len(keep) + records = [] + removed = Counter() + for op,d,s,c,f,p in program['records']: + if d in dead_set: + need(op in (0,1),'discarded helper has an owned snapshot role') + if op == 0: + removed[f] += 1 + continue + need(op == 0 or s not in dead_set,'remaining record reads discarded input') + records.append([op,mapping[d],s if op == 0 else mapping[s],c,f,p]) + return keep,records,dict(sorted(removed.items())) + +def execute(word,keep,records,backward=False,initial=None): + n = len(keep) + rows = ([{i:1} for i in range(n)]+[{}]) if initial is None else [r.copy() for r in initial] + frames = [word['final' if backward else 'start'][i] for i in keep]+[None] + dims = [cap.rank(word['lines'][j] for j in f) for f in word['frames']] + masks = [sum(1 << j for j in f) for f in word['frames']] + opened,copies,prefix = None,0,1 + profile,counts = Counter(),Counter() + for op,d,s,c,f,p in reversed(records) if backward else records: + counts[op] += 1 + if op == 0: + old,new = (c,s) if backward else (s,c) + lo,hi = (new,old) if backward else (old,new) + need(frames[d] == old and not masks[lo] & ~masks[hi] and dims[hi]-dims[lo] == f > 0,'projected MOVE frame/rank') + frames[d] = new + profile[f] += 1 + elif op == 1: + need(d < n and d != s and frames[d] == frames[s] == f and d != opened,'projected common-frame ADD or snapshot source mutation') + rows[d] = scalar.add(rows[d],rows[s],-c if backward else c) + prefix = max(prefix,sum(abs(v) for v in rows[d].values())) + elif op == (3 if backward else 2): + need(opened is None and s == n and not rows[n] and frames[n] is None,'projected fresh private field') + need(d < 111 and frames[d] == c == 1 and not masks[f] & ~masks[c] and dims[c]-dims[f] == 1,'projected actual source cap COPY') + rows[n],frames[n],opened = rows[d].copy(),f,d + profile[1] += 1 + copies += 1 + else: + need(op == (2 if backward else 3) and opened == d and s == n and rows[n] == rows[d] and frames[d] == c and frames[n] == f,'projected immutable snapshot ERASE') + rows[n],frames[n],opened = {},None,None + need(opened is None and not rows[n] and frames[n] is None and copies == 3,'projected private endpoint') + need(frames[:n] == [word['start' if backward else 'final'][i] for i in keep],'retained physical endpoint frames') + need(profile == Counter({1:1298,2:1342,3:79,4:44,5:93,6:11,7:9}),'projected paid profile') + need(counts == Counter({0:2873,1:13223,2:3,3:3}),'projected literal record counts') + return rows,{'prefix_row_l1':prefix,'profile':dict(sorted(profile.items())), + 'rank_mass':sum(k*v for k,v in profile.items()),'copies':copies, + 'counts':dict(sorted(counts.items()))} + +def binary_rank(rows): + basis = {} + for row in rows: + while row: + p = row.bit_length() - 1 + if p not in basis: + basis[p] = row + break + row ^= basis[p] + return len(basis) + +def binary_product(a, b): + output = [] + for row in a: + value = 0 + for i, other in enumerate(b): + if row >> i & 1: + value ^= other + output.append(value) + return output + +def matrices(raw, meta): + rows = [1 << i for i in range(660)] + for phase in ("D", "A"): + for _, dst, sources in raw[phase]: + for src in sources: + rows[dst] ^= rows[src] + mask = (1 << 111) - 1 + need(all(not(rows[j] & (((1 << 111)-1) << 111)) for j in raw["ret"]), "retained target dependency") + R = [rows[j] & mask for j in raw["ret"]] + K = [sum(1 << j for j in subset) for subset in raw["scatter"]] + M = binary_product(R, K) + J = [(1 << i) ^ r for i, r in enumerate(binary_product(K, R))] + need((R, K, M, J) == tuple(meta[k] for k in ("R", "K", "M", "J")), "actual raw R/K/J binding") + need(M == [507,135,238,349,185,437,205,503,425], "actual quotient matrix") + need(binary_rank(R) == binary_rank(M) == 9 and binary_rank(J) == 108, "actual ranks") + eye = [1 << i for i in range(111)] + A, inv, Q = (meta[k] for k in ("H", "Hinv", "Q")) + direct_A = [eye[i] if i < 3 else J[i] for i in range(111)] + need(A == direct_A and A[:3] == [1,2,4], "actual row-deletion source code") + N = [(1 << i) ^ row for i,row in enumerate(M)] + S = [sum(((row >> p) & 1) << p for p in range(3)) for row in R] + D = K[:3] + Y = [a ^ b for a,b in zip(N,binary_product(S,D))] + B0 = meta["B0"] + need(Y == [10,373,282,165,176,405,356,145,166] and binary_rank(Y) == 9, "invertible actual quotient") + need(binary_product(B0,N) == [0]*3 and binary_product(B0,S) == [1,2,4], "left-null section") + need(binary_product(B0,Y) == D and meta["Y"] == Y and meta["D"] == D, "quotient repair identity") + need(binary_product(A, inv) == binary_product(inv, A) == eye, "source-code inverse") + need(binary_product(J, inv) == [a ^ b for a,b in zip(eye,Q)], "section equation") + need([i for i,r in enumerate(Q) if r] == [0,1,2] and binary_rank(Q) == 3, "three actual target rows") + need(binary_rank([a ^ b for a,b in zip(A,eye)]) == 9, "source-code rank") + return A, inv + +def source_code(records): + code = [r for r in records if r[0] == 1 and r[5] in (21,22,23,24)] + need(len(code) == 1499, "complete source-code gates") + forward, reverse = scalar.identity(111), scalar.identity(111) + for _, x, y, c, frame, phase in code: + need(x < 111 and y < 111 and frame == 1, "source-only code") + forward[x] = scalar.add(forward[x], forward[y], c) + for _, x, y, c, frame, phase in reversed(code): + reverse[x] = scalar.add(reverse[x], reverse[y], -c) + return forward[:111], reverse[:111] + +def endpoints(forward, reverse, records, A, inv): + az, azi = source_code(records) + need(forward[:111] == az and reverse[:111] == azi, "exact integer source and inverse") + need(scalar.parity(az) == A and scalar.parity(azi) == inv, "source parity binding") + n = len(forward) - 1 + eye = scalar.identity(n) + for i in range(222,n): + need(forward[i] == reverse[i] == eye[i], "arbitrary dirty helper restoration") + for rows in (forward, reverse): + for p in range(111): + need({j:c for j,c in rows[111+p].items() if 111 <= j < 222} == {111+p:1}, "target identity block") + need(all(c % 2 == 0 for j,c in rows[111+p].items() if j >= 222), "target even helper leakage") + expected_f = [1 << i for i in range(n)] + [0] + expected_r = expected_f[:] + for i in range(111): + expected_f[i], expected_f[111+i] = A[i], expected_f[111+i] ^ A[i] + expected_r[i], expected_r[111+i] = inv[i], expected_r[111+i] ^ (1 << i) + need(scalar.parity(forward) == expected_f and scalar.parity(reverse) == expected_r, "all 651 F2 endpoint columns") + +def rejection(label, fn): + try: + fn() + except ValueError: + return label + raise ValueError("Defect control escaped: " + label) + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument("--repo", type=Path, required=True) + parser.add_argument("--out", type=Path, required=True) + args = parser.parse_args() + expected = json.loads((HERE / "EXPECTED.json").read_bytes()) + source = args.repo / expected["source_word"] + need(hashlib.sha256(source.read_bytes()).hexdigest() == expected["source_sha256"], "original native source hash") + raw = json.loads(gzip.decompress(source.read_bytes())) + word = json.loads(gzip.decompress((args.out / "BIT-PRUNED-WORD.json.gz").read_bytes())) + support = json.loads(gzip.decompress((args.out / "support/BIT-SUPPORT-WORD.json.gz").read_bytes())) + keep, projected_records, removed = projected(support) + need(len(keep) == 651 and removed == {1:27,5:9}, "complete unread-family projection") + need(word["records"] == projected_records and word["public_registers"] == word["private_register"] == 651, "complete literal projected word") + need(word["deleted_public_families"] == list(range(471,480)), "deleted physical identities") + need(word["start"] == [raw["start"][i] for i in keep] and word["final"] == [raw["final"][i] for i in keep], "projected actual boundary frames") + meta = json.loads((args.out / "support/BIT-SUPPORT.json").read_bytes())["matrices"] + need(hashlib.sha256(cap.canonical(meta)).hexdigest() == expected["source_matrix_sha256"], "complete final matrix payload") + A, inv = matrices(raw, meta) + records = word["records"] + forward, fwd = execute(raw, keep, records) + reverse, rev = execute(raw, keep, records, True) + endpoints(forward, reverse, records, A, inv) + roundtrip, _ = execute(raw, keep, records, True, forward) + need(roundtrip == scalar.identity(651), "full integer roundtrip") + projectors = cap.address_identities(raw) + need([r[1] for r in records if r[0] == 2] == [0,1,2], "actual source pivots") + need(fwd["prefix_row_l1"] == 34285 and rev["prefix_row_l1"] == 5839860, "exact local integer prefix norms") + sign_records = [r[:3]+[-r[3]]+r[4:] if r[0] == 1 and r[5] == 33 else r[:] for r in records] + bad_sign, _ = execute(raw, keep, sign_records) + need(scalar.parity(bad_sign) == scalar.parity(forward) and bad_sign[:111] != forward[:111], "sign defect distinguished beyond parity") + controls = ["wrong_integer_unprepare_sign"] + controls.append(rejection("omit_pivot_unprepare", lambda: execute(raw,keep,[r for r in records if not(r[0] == 1 and r[5] == 33)]))) + bad = [r[:] for r in records] + position = next(i for i,r in enumerate(bad) if r[0] == 2) + bad[position][4] = 1 + controls.append(rejection("FULL_to_FULL_copy", lambda: execute(raw,keep,bad))) + bad = [r[:] for r in records] + position = next(i for i,r in enumerate(bad) if r[0] == 2) + pivot = bad[position][1] + bad.insert(position+1,[1,pivot,(pivot+1)%111,1,1,99]) + controls.append(rejection("mutate_live_source", lambda: execute(raw,keep,bad))) + controls.append(rejection("reuse_noninvolutive_code_as_inverse", lambda: endpoints(forward, reverse, records, A, A))) + wrong = dict(meta) + wrong["Q"] = meta["Q"][:] + wrong["Q"][0] ^= 1 + controls.append(rejection("wrong_section_query", lambda: matrices(raw,wrong))) + bad_support = dict(support, records=support["records"]+[[1,111,471,1,0,99]]) + controls.append(rejection("read_deleted_family", lambda: projected(bad_support))) + result = {"status":"PASS_INDEPENDENT_LOCAL_SIGNED_NATIVE", "columns":651, "dirty_helpers":429, + "source_code_rank":9, "clean_target_rank":108, "minimal_repair_rows_in_fixed_class":3, + "forward":fwd, "inverse":rev, "projectors":len(projectors), "address_columns":3552, + "frame_bindings":222, "deleted_original_families":list(range(471,480)), "removed_profile":removed, "projector_hashes":projectors, "controls":controls, + "integer_target_contract":"y+T_Z x+E_Z h; T_Z mod2=A and E_Z even", "no_new_kappa":True} + (args.out / "INDEPENDENT.json").write_text(json.dumps(result,indent=2,sort_keys=True)+"\n") + print(json.dumps({k:result[k] for k in ("status","columns","dirty_helpers","source_code_rank","projectors","controls","no_new_kappa")},sort_keys=True)) + +if __name__ == "__main__": + main() diff --git a/research/bit-r438-source-code/native_caps.py b/research/bit-r438-source-code/native_caps.py new file mode 100644 index 0000000000..5fdd309b4c --- /dev/null +++ b/research/bit-r438-source-code/native_caps.py @@ -0,0 +1,56 @@ +"""Independent exact rational E8 cap ADDRESS identities; no controller.""" +from fractions import Fraction as Q +from hashlib import sha256 +import json + +def need(ok, message): + if not ok: + raise ValueError(message) + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(',', ':')).encode() + +def rank(rows): + basis = {} + for row in rows: + row = list(map(Q, row)) + for j, old in sorted(basis.items()): + c = row[j] + row = [x-c*y for x,y in zip(row,old)] + j = next((j for j,x in enumerate(row) if x), None) + if j is not None: + c = row[j] + basis[j] = [x/c for x in row] + return len(basis) + +def identity(n): + return [[Q(i == j) for j in range(n)] for i in range(n)] + +def multiply(a, b): + return [[sum(x*y for x,y in zip(row,col)) for col in zip(*b)] for row in a] + +def exchange(u): + c = [[Q(i == j)-u[i][j] for j in range(8)] for i in range(8)] + return [c[i]+u[i] for i in range(8)]+[u[i]+c[i] for i in range(8)] + +def address_identities(word): + ident = identity(8) + out = [] + for p, q in enumerate(word['lines']): + need(sum(x*x for x in q) == 4, 'actual E8 root norm') + start = [word['lines'][j] for j in word['frames'][word['start'][p]]] + cap = [word['lines'][j] for j in word['frames'][word['final'][111+p]]] + need(rank(start) == 1 and all(all(4*x == sum(a*b for a,b in zip(row,q))*y + for x,y in zip(row,q)) for row in start), 'actual entrance is not P_p') + need(rank(cap) == 7 and all(sum(x*y for x,y in zip(row,q)) == 0 for row in cap), + 'actual target cap is not K_p') + proj = [[Q(x*y,4) for y in q] for x in q] + complement = [[ident[i][j]-proj[i][j] for j in range(8)] for i in range(8)] + need(multiply(proj,proj) == proj and rank(proj) == 1, 'actual P_p projector') + need(multiply(exchange(ident),exchange(proj)) == exchange(complement), + 'D_I D_P differs from D_K') + need(multiply(exchange(proj),exchange(proj)) == identity(16), 'D_P squared differs from I') + encoded = [[[v.numerator,v.denominator] for v in row] for row in proj] + out.append(sha256(canonical(encoded)).hexdigest()) + need(len(out) == 111, 'actual punctured root count') + return out diff --git a/research/bit-r438-source-code/producer/bit_scalar_invoice.py b/research/bit-r438-source-code/producer/bit_scalar_invoice.py new file mode 100644 index 0000000000..97d7559df0 --- /dev/null +++ b/research/bit-r438-source-code/producer/bit_scalar_invoice.py @@ -0,0 +1,147 @@ +#!/usr/bin/env python3 +"""Literal scalar/integer prefix invoice of the three-target R438 producer. + +No native operator lowering is assumed here. The ordered integer lift uses +the emitted forward ADD coefficients +1; its inverse reverses the exact word +and uses -1. Only reduction modulo2 has the declared coded BIT endpoint. +""" +from collections import Counter +import gzip +import hashlib +import json +from pathlib import Path +import sys + +sys.dont_write_bytecode = True +import bit_transvection as base + +HERE = Path(__file__).resolve().parent +N = 660 + + +def eye(n): + return [[int(i == j) for j in range(n)] for i in range(n)] + [[0]*n] + + +def digest(rows): + h = hashlib.sha256() + for row in rows: + h.update((','.join(map(str,row))+'\n').encode()) + return h.hexdigest() + + +def execute(records, initial, reverse=False, invert_sign=True): + rows = [row[:] for row in initial] + live, copies, maximum, phase_max = None, 0, 1, {} + for number,(op,dst,src,coefficient,frame,phase) in enumerate( + reversed(records) if reverse else records): + if op == 1: + sign = coefficient * (-1 if reverse and invert_sign else 1) + rows[dst] = [a+sign*b for a,b in zip(rows[dst],rows[src])] + value = sum(abs(x) for x in rows[dst]) + maximum = max(maximum,value) + phase_max[str(phase)] = max(phase_max.get(str(phase),0),value) + elif op == (3 if reverse else 2): + base.require(live is None and not any(rows[N]), 'Integer COPY overwrites private dirt') + rows[N], live = rows[dst][:], dst + maximum = max(maximum,sum(abs(x) for x in rows[N])) + copies += 1 + elif op == (2 if reverse else 3): + base.require(live == dst and rows[N] == rows[dst], + f'Integer ERASE snapshot changed at record{number}') + rows[N], live = [0]*N, None + else: + base.require(op == 0, 'Unknown integer operation') + base.require(live is None and not any(rows[N]), 'Integer private buffer not clear') + return rows,dict(maximum_exact_prefix_row_l1=maximum, + phase_exact_prefix_row_l1=phase_max,copies=copies, + endpoint_matrix_sha256=digest(rows), + endpoint_max_row_l1=max(sum(abs(x) for x in row) for row in rows)) + + +def parity(rows): + return [sum((x & 1) << j for j,x in enumerate(row)) for row in rows] + + +def small_bounds(records): + selected = [r for r in records if r[0] == 1 and 21 <= r[5] <= 24] + bounds, exact = [], [] + for reverse in (False,True): + values = [1]*111 + for op,dst,src,coefficient,frame,phase in reversed(selected) if reverse else selected: + values[dst] += abs(coefficient)*values[src] + bounds.append(max(values)) + rows = [[int(i == j) for j in range(111)] for i in range(111)] + maximum = 1 + for op,dst,src,coefficient,frame,phase in reversed(selected) if reverse else selected: + sign = coefficient * (-1 if reverse else 1) + rows[dst] = [a+sign*b for a,b in zip(rows[dst],rows[src])] + maximum = max(maximum,sum(abs(x) for x in rows[dst])) + exact.append(maximum) + return dict(adds=len(selected),forward_positive=bounds[0],reverse_positive=bounds[1], + forward_exact_prefix_l1=exact[0],reverse_exact_prefix_l1=exact[1], + extra_helpers=0,extra_private_fields=0) + + +def main(): + meta = json.loads((HERE/'BIT-THREE-ROW.json').read_text()) + blob = (HERE/'BIT-THREE-ROW-WORD.json.gz').read_bytes() + base.require(hashlib.sha256(blob).hexdigest() == meta['output_gzip_sha256'], + 'Three-row word pin changed') + word = json.loads(gzip.decompress(blob)) + records = word['records'] + start = eye(N) + forward,fwd = execute(records,start) + inverse,rev = execute(records,start,reverse=True) + roundtrip,rt = execute(records,forward,reverse=True) + base.require(roundtrip == start, 'Ordered integer inverse failed all660 columns') + bad,bad_stats = execute(records,forward,reverse=True,invert_sign=False) + base.require(bad != start, 'Wrong integer inverse sign control escaped') + expected_forward = [1 << j for j in range(N)] + [0] + expected_inverse = expected_forward[:] + for p in range(111): + expected_forward[p] = meta['matrices']['H'][p] + expected_forward[111+p] ^= meta['matrices']['H'][p] + expected_inverse[p] = meta['matrices']['Hinv'][p] + expected_inverse[111+p] ^= 1 << p + base.require(parity(forward) == expected_forward, 'Integer forward reduction differs') + base.require(parity(inverse) == expected_inverse, 'Integer inverse reduction differs') + positive = base.positive_bounds(records,N) + base.require(fwd['maximum_exact_prefix_row_l1'] == positive['forward'], + 'Forward positive envelope is not the exact nonnegative norm') + base.require(rev['maximum_exact_prefix_row_l1'] <= positive['reverse'], + 'Reverse triangle envelope failed') + counts = Counter(r[0] for r in records) + phase_adds = Counter(str(r[5]) for r in records if r[0] == 1) + copy_ranks = Counter(r[5] for r in records if r[0] == 2) + boundary = Counter(r[4] for r in records if r[0] == 0) + output = dict(status='PASS_LITERAL_SCALAR_INTEGER_LIFT_AND_INVERSE_NO_GLOBAL_TRANSFER', + source_word_gzip_sha256=meta['output_gzip_sha256'], + covered_integer_columns=N,covered_integer_endpoint_coefficients=N*N, + forward=fwd,reverse_signed=rev,roundtrip_signed=rt, + source_code=small_bounds(records),positive=positive, + scalar_invoice=dict(ADD=counts[1],MOVE_children=counts[0],COPY=counts[2],ERASE=counts[3], + ADDs_per_phase=dict(sorted(phase_adds.items())), + COPY_rank_histogram=dict(sorted(copy_ranks.items())), + MOVE_rank_histogram=dict(sorted(boundary.items())), + owned_private_fields=1,max_live_immutable_snapshots=1, + public_source_fields=111,public_target_fields=111, + public_dirty_helper_fields=438, + new_source_code_helpers=0,new_source_code_private_fields=0, + extra_repair_helper_fields=0,reused_repair_helper=222), + negative_control=dict(wrong_reverse_integer_sign_detected=True, + bad_roundtrip_sha256=bad_stats['endpoint_matrix_sha256'], + F2_signs_cannot_detect_this_control=True), + exact_lift_statement='The emitted integer forward matrix reduces modulo2 to(Ax,y+Ax,h). Its exact inverse is the reversed word with negative ADD coefficients; all660 input columns restore overZ. The forward helper rows are NOT claimed to be identity overZ.', + precision_statement='F and reverse triangleR are exact ordered scalar envelopes for inputs with absolute value at most1, scaling linearly for larger bounds. Historical104/192 bit guards fail;173/320 are numerical sufficient exponents for the old scalar formulas, with applicability to a changed native/global interface still owed.', + unresolved=['Native field/address transport and actual integer normalization', + '63 extra global code bridges, their signed integer lift and full prefix bounds', + 'Terminal N E^-1 N, chronological owner and physical stock', + 'Complete payload/numerical scratch and all-size recurrence repricing']) + (HERE/'BIT-SCALAR-INVOICE.json').write_text(json.dumps(output,indent=2,sort_keys=True)+'\n') + print(json.dumps({k:output[k] for k in ('status','forward','reverse_signed','source_code','scalar_invoice')}, + indent=2,sort_keys=True)) + + +if __name__ == '__main__': + main() diff --git a/research/bit-r438-source-code/producer/bit_section_code.py b/research/bit-r438-source-code/producer/bit_section_code.py new file mode 100644 index 0000000000..71c0e4d4ba --- /dev/null +++ b/research/bit-r438-source-code/producer/bit_section_code.py @@ -0,0 +1,246 @@ +#!/usr/bin/env python3 +"""R438 source coding with three actual repaired target rows over F2. + +The source code is invertible and generally not an involution. Its literal +inverse is used on the backward local call. This is a local changed interface, +with native/global/precision admission left to independent work. +""" +from collections import Counter +import gzip +import hashlib +import json +from pathlib import Path +import sys + +sys.dont_write_bytecode = True +import bit_transvection as base + +HERE = Path(__file__).resolve().parent +need, prod, inv, bits, rank = base.require, base.product, base.inverse, base.bits, base.rank + + +def transpose(rows, n): + return [sum(((row >> j) & 1) << i for i, row in enumerate(rows)) for j in range(n)] + + +def kernel(rows, n): + rows, pivots, used = rows[:], [], 0 + for j in range(n): + p = next((i for i in range(used, len(rows)) if rows[i] >> j & 1), None) + if p is None: + continue + rows[used], rows[p] = rows[p], rows[used] + for i in range(len(rows)): + if i != used and rows[i] >> j & 1: + rows[i] ^= rows[used] + pivots.append(j) + used += 1 + result = [] + for j in range(n): + if j not in pivots: + value = 1 << j + for i, p in enumerate(pivots): + if rows[i] >> j & 1: + value |= 1 << p + result.append(value) + need(prod(rows, transpose(result, n)) == [0] * len(rows), 'Kernel failed') + return result + + +def particular(left, right): + """Solve left X=right with all nonpivot variables zero.""" + n = len(left) + rows = [a | (b << n) for a, b in zip(left, right)] + pivots, used = [], 0 + for j in range(n): + p = next((i for i in range(used, n) if rows[i] >> j & 1), None) + if p is None: + continue + rows[used], rows[p] = rows[p], rows[used] + for i in range(n): + if i != used and rows[i] >> j & 1: + rows[i] ^= rows[used] + pivots.append(j) + used += 1 + need(all(row >> n == 0 for row in rows[used:]), 'Inconsistent right-hand side') + result = [0] * n + for i, p in enumerate(pivots): + result[p] = rows[i] >> n + need(prod(left, result) == right, 'Particular solution failed') + return result + + +def cnot_word(matrix): + """A literal row-ADD circuit for an invertible binary square matrix.""" + rows, ops = matrix[:], [] + n = len(rows) + def add(dst, src): + rows[dst] ^= rows[src] + ops.append((dst, src)) + for j in range(n): + p = next((i for i in range(j, n) if rows[i] >> j & 1), None) + need(p is not None, 'Singular CNOT matrix') + if p != j: + add(j, p) + add(p, j) + add(j, p) + for i in range(n): + if i != j and rows[i] >> j & 1: + add(i, j) + need(rows == [1 << i for i in range(n)], 'CNOT elimination failed') + rows = [1 << i for i in range(n)] + result = list(reversed(ops)) + for dst, src in result: + rows[dst] ^= rows[src] + need(rows == matrix, 'CNOT circuit order failed') + return result + + +def section(data): + R, K, M, J = (data[k] for k in ('R', 'K', 'M', 'J')) + N = [(1 << i) ^ row for i, row in enumerate(M)] + C0 = kernel(transpose(N, 9), 9) + need(len(C0) == 3, 'Wrong left-nullity') + C = prod(C0, R) + selected, columns = [], [] + for p in range(111): + column = sum(((row >> p) & 1) << j for j, row in enumerate(C)) + if rank(columns + [column]) > len(columns): + selected.append(p) + columns.append(column) + if len(selected) == 3: + break + S = [sum(((row >> p) & 1) << j for j, p in enumerate(selected)) for row in R] + B0 = prod(inv(prod(C0, S)), C0) + need(prod(B0, S) == [1 << j for j in range(3)], 'Bad rank3 section') + F9 = [(1 << j) ^ row for j, row in enumerate(prod(S, B0))] + X0 = particular(N, F9) + T = transpose(kernel(N, 9), 9) + X = [a ^ b for a, b in zip(X0, prod(T, B0))] + need(rank(X) == 9 and prod(N, X) == F9, 'Invertible quotient lift failed') + PB = [0] * 111 + for j, p in enumerate(selected): + PB[p] = B0[j] + W = [a ^ b for a, b in zip(prod(K, X), PB)] + Hinv = [(1 << p) ^ row for p, row in enumerate(prod(W, R))] + need(rank(Hinv) == 111, 'Source inverse code singular') + H = inv(Hinv) + Q = prod(PB, R) + need(prod(J, Hinv) == [(1 << p) ^ row for p, row in enumerate(Q)], 'JHinv residual failed') + need([a ^ b for a,b in zip(J, prod(Q, H))] == H, 'Coded target identity failed') + need(prod(H, Hinv) == [1 << p for p in range(111)], 'Source code inverse failed') + need([p for p,row in enumerate(Q) if row] == selected, 'Wrong target support') + return dict(R=R, K=K, M=M, J=J, N=N, C0=C0, C=C, selected=selected, + S=S, B0=B0, F9=F9, X0=X0, T=T, X=X, W=W, + H=H, Hinv=Hinv, Q=Q) + + +def compact_code(data, pivots): + # Replace nine physical pivot coordinates by a normalized query basis. + R = data['R'] + S = [sum(((row >> p) & 1) << j for j,p in enumerate(pivots)) for row in R] + query = prod(inv(S), R) + B = [1 << p for p in range(111)] + prepare = [] + for j, p in enumerate(pivots): + B[p] = query[j] + for src in bits(query[j] ^ (1 << p)): + need(src not in pivots, 'Normalized query still mixes pivots') + prepare.append([1, p, src, 1, 1, 21]) + need(prod(B, B) == [1 << p for p in range(111)], 'Query change not involutive') + middle = prod(prod(B, data['H']), B) + pivot_set = set(pivots) + D = [sum(((middle[p] >> q) & 1) << j for j,q in enumerate(pivots)) for p in pivots] + fanout = [] + for p in range(111): + allowed = sum(1 << q for q in pivots) | ((1 << p) if p not in pivot_set else 0) + need(middle[p] & ~allowed == 0, 'Source code has a non-query middle term') + if p not in pivot_set: + need(middle[p] >> p & 1, 'Nonpivot identity diagonal missing') + for src in bits(middle[p] ^ (1 << p)): + fanout.append([1, p, src, 1, 1, 22]) + small = [[1, pivots[d], pivots[s], 1, 1, 23] for d,s in cnot_word(D)] + unprepare = [rec[:5] + [24] for rec in reversed(prepare)] + records = prepare + fanout + small + unprepare + rows = [1 << p for p in range(111)] + for op, dst, src, coefficient, frame, phase in records: + rows[dst] ^= rows[src] + need(rows == data['H'], 'Compact source word differs from its code') + return records, dict(query=query, pivots=pivots, B=B, middle=middle, D=D, + prepare_adds=len(prepare), fanout_adds=len(fanout), + quotient_adds=len(small), unprepare_adds=len(unprepare)) + + +def main(): + word, builder, baseline, old_records = base.load() + old_data = base.matrices(word) + _, old_parts = base.construct(word, old_records, old_data) + data = section(old_data) + code, code_data = compact_code(data, old_data['selected']) + repair = [] + b, count, v = 222, 660, 111 + for p in data['selected']: + cap = word['final'][v+p] + episode = [[2,b,count,1,cap,1], [1,v+p,count,1,cap,15], [3,b,count,1,cap,0]] + gather = [[1,b,src,1,1,16] for src in bits(data['Q'][p])] + repair.extend(episode + gather + episode + [rec[:5]+[17] for rec in gather]) + records = old_parts['prefix'] + old_parts['clean'] + code + repair + forward = base.replay(word, builder, records, data) + reverse = base.replay(word, builder, records, data, reverse=True) + expect = Counter({int(k):n for k,n in baseline['profile'].items()}) + expect[7] -= 9 + expect[1] += 6 + need(forward['profile'] == dict(sorted(expect.items())), 'Profile differs') + need(reverse['profile'] == forward['profile'], 'Reverse profile differs') + need(forward['rank_mass'] == 5064 and forward['copies'] == 6, 'Wrong paid bill') + controls = [ + base.must_fail('omit_changed_D', lambda: base.replay( + word,builder,records[len(old_parts['prefix']):],data)), + base.must_fail('omit_query_unprepare', lambda: base.replay( + word,builder,[r for r in records if not(r[0] == 1 and r[5] == 24)],data)), + base.must_fail('omit_dirty_repair_restore', lambda: base.replay( + word,builder,[r for r in records if not(r[0] == 1 and r[5] == 17)],data)), + base.must_fail('mutate_copied_snapshot', lambda: base.replay( + word,builder,records,data,mutate_snapshot=True)), + base.must_fail('use_same_noninvolutive_code_in_reverse', lambda: base.replay( + word,builder,records,{**data,'Hinv':data['H']},reverse=True)), + ] + container = dict(format='coded-r438-three-row-local-records-v1', + public_registers=660,private_register=660, + source_word=str(base.WORD),source_gzip_sha256=base.WORD_SHA, + start=word['start'],final=word['final'],records=records, + copy_schema='[2,physical_source,660,sourceframe,privateframe,rank]', + erase_schema='[3,physical_source,660,sourceframe,privateframe,0]') + raw = base.canonical(container) + outword = HERE/'BIT-THREE-ROW-WORD.json.gz' + outword.write_bytes(gzip.compress(raw,mtime=0)) + output = dict(status='PASS_LOCAL_THREE_TARGET_ROWS_NO_GLOBAL_SUPPLIER_NO_NEW_KAPPA', + source_pin=base.MAIN_PIN,source_word=str(base.WORD),source_gzip_sha256=base.WORD_SHA, + baseline_builder_sha256=base.BUILDER_SHA, + output_word=str(outword),output_canonical_sha256=hashlib.sha256(raw).hexdigest(), + output_gzip_sha256=hashlib.sha256(outword.read_bytes()).hexdigest(), + matrices=data,source_code=code_data,forward=forward,reverse=reverse, + source_code_rank=rank([row^(1<(Ax,y+Ax,h)', + literal_inverse='(x,y,h)->(A^-1 x,y+x,h)', + matrix_names='H=A, Hinv=A^-1; J Hinv=I+Q', + initial_frames='source Pp; target0; helper0', + final_frames='source FULL; target Pp-perp; helper FULL', + copied_snapshots='Two unchanged arbitrary-helper snapshots per each of three target rows'), + scope='Finite660-column F2 proof and complete literal local frame/rank invoice; no native global admission', + unresolved=['Actual native operator lift and complementary backward frame interpretation', + 'Signed integer lift, new precision reserve, and physical scalar scratch', + 'Global19-event code and terminal cap decoder', + 'Chronological owners, unused remainders, full recursive supplier contract']) + (HERE/'BIT-THREE-ROW.json').write_text(json.dumps(output,indent=2,sort_keys=True)+'\n') + print(json.dumps({k:output[k] for k in ('status','forward','adds','part_adds','source_code_rank','positive')}, + indent=2,sort_keys=True)) + + +if __name__ == '__main__': + main() diff --git a/research/bit-r438-source-code/producer/bit_signed_lift.py b/research/bit-r438-source-code/producer/bit_signed_lift.py new file mode 100644 index 0000000000..6160f4540e --- /dev/null +++ b/research/bit-r438-source-code/producer/bit_signed_lift.py @@ -0,0 +1,151 @@ +#!/usr/bin/env python3 +"""Choose real signed cleanup for the unchanged three-row BIT construction. + +The coded BIT endpoint is modulo2. Unlike the original all-positive integer +lift, this forward lift restores all438 dirty helpers exactly overZ, and its +source code acts only on x. No native/global admission is inferred. +""" +from collections import Counter +import gzip +import hashlib +import json +from pathlib import Path +import sys + +sys.dont_write_bytecode = True +import bit_transvection as base +import bit_scalar_invoice as scalar + +HERE = Path(__file__).resolve().parent +N,V = 660,111 + + +def source_integer_code(records): + code = [r for r in records if r[0] == 1 and 21 <= r[5] <= 24] + rows = [[int(i == j) for j in range(V)] for i in range(V)] + for op,dst,src,c,frame,phase in code: + rows[dst] = [a+c*b for a,b in zip(rows[dst],rows[src])] + inverse = [[int(i == j) for j in range(V)] for i in range(V)] + for op,dst,src,c,frame,phase in reversed(code): + inverse[dst] = [a-c*b for a,b in zip(inverse[dst],inverse[src])] + trial = [row[:] for row in rows] + for op,dst,src,c,frame,phase in reversed(code): + trial[dst] = [a-c*b for a,b in zip(trial[dst],trial[src])] + base.require(trial == [[int(i == j) for j in range(V)] for i in range(V)], + 'Integer source code and inverse fail') + return rows,inverse + + +def column_control(records, input_column, bad_phase): + values = [int(i == input_column) for i in range(N)] + [0] + for op,dst,src,c,frame,phase in records: + if op == 1: + values[dst] += (1 if phase == bad_phase else c)*values[src] + elif op == 2: + values[N] = values[dst] + elif op == 3: + base.require(values[N] == values[dst], 'Control snapshot failed before endpoint') + values[N] = 0 + differences = [dict(row=i,value=values[i],expected=int(i == input_column)) + for i in range(2*V,N) if values[i] != int(i == input_column)] + base.require(differences, 'Bad cleanup sign control escaped') + return dict(input_column=input_column,bad_phase=bad_phase,first_difference=differences[0]) + + +def main(): + old_meta = json.loads((HERE/'BIT-THREE-ROW.json').read_text()) + old_blob = (HERE/'BIT-THREE-ROW-WORD.json.gz').read_bytes() + base.require(hashlib.sha256(old_blob).hexdigest() == old_meta['output_gzip_sha256'], + 'Raw three-row source changed') + word = json.loads(gzip.decompress(old_blob)) + records = [r[:] for r in word['records']] + copy_number = -1 + changes = Counter() + for r in records: + op,dst,src,c,frame,phase = r + if op == 2: + copy_number += 1 + if op != 1: + continue + if phase in (5,24,17) or (phase == 15 and copy_number%2 == 0): + r[3] = -1 + changes[str(phase)] += 1 + base.require(copy_number+1 == 6, 'Wrong snapshot episode count') + forward,fwd = scalar.execute(records,scalar.eye(N)) + inverse,rev = scalar.execute(records,scalar.eye(N),reverse=True) + roundtrip,rt = scalar.execute(records,forward,reverse=True) + base.require(roundtrip == scalar.eye(N), 'Signed integer roundtrip failed') + A,Ainv = source_integer_code(records) + for p in range(V): + base.require(forward[p] == A[p]+[0]*(N-V), + 'Forward integer source code depends on a target/helper') + base.require(inverse[p] == Ainv[p]+[0]*(N-V), + 'Inverse integer source code depends on a target/helper') + for h in range(2*V,N): + base.require(forward[h] == [int(j == h) for j in range(N)], + f'Actual forward integer helper{h} not restored') + base.require(inverse[h] == [int(j == h) for j in range(N)], + f'Actual inverse integer helper{h} not restored') + for p in range(V): + base.require(forward[V+p][V:2*V] == [int(j == p) for j in range(V)], + 'Integer target self-block changed') + base.require(all(x%2 == 0 for x in forward[V+p][2*V:]), + 'Integer target has odd dirty-helper leakage') + expected_forward = [1 << j for j in range(N)] + [0] + expected_inverse = expected_forward[:] + for p in range(V): + expected_forward[p] = old_meta['matrices']['H'][p] + expected_forward[V+p] ^= old_meta['matrices']['H'][p] + expected_inverse[p] = old_meta['matrices']['Hinv'][p] + expected_inverse[V+p] ^= 1 << p + base.require(scalar.parity(forward) == expected_forward, 'Signed forward parity differs') + base.require(scalar.parity(inverse) == expected_inverse, 'Signed inverse parity differs') + # The ordinary all-input frame audit treats +/-1 equally overF2, but now + # consumes this actual signed record list, with the original source bytes. + raw_word,builder,baseline,_ = base.load() + native_scalar_forward = base.replay(raw_word,builder,records,old_meta['matrices']) + native_scalar_reverse = base.replay(raw_word,builder,records,old_meta['matrices'],reverse=True) + controls = [column_control(records,0,5),column_control(records,0,17)] + word['format'] = 'coded-r438-three-row-signed-local-records-v1' + word['records'] = records + word['signed_from'] = old_meta['output_gzip_sha256'] + raw = base.canonical(word) + outword = HERE/'BIT-SIGNED-WORD.json.gz' + outword.write_bytes(gzip.compress(raw,mtime=0)) + F,R = fwd['maximum_exact_prefix_row_l1'],rev['maximum_exact_prefix_row_l1'] + output = dict(status='PASS_SIGNED_LIFT_ACTUAL_FORWARD_DIRTY_RESTORATION_NO_GLOBAL_TRANSFER', + raw_word_gzip_sha256=old_meta['output_gzip_sha256'], + output_word=str(outword),output_gzip_sha256=hashlib.sha256(outword.read_bytes()).hexdigest(), + output_canonical_sha256=hashlib.sha256(raw).hexdigest(), + matrices_sha256=hashlib.sha256(base.canonical(old_meta['matrices'])).hexdigest(), + signed_changes=dict(sorted(changes.items())), + forward=fwd,reverse_signed=rev,roundtrip_signed=rt, + source_code=scalar.small_bounds(records), + source_integer_matrix_sha256=scalar.digest(A), + source_integer_inverse_sha256=scalar.digest(Ainv), + public_integer_input_columns=N, + actual_forward_integer_equalities=dict(source='A_Z x, independent of all targets/helpers', + dirty_helpers='all438 exactly h',private='exactly zero', + target='y+T_Z x+E_Z h, with T_Z mod2=A and E_Z even'), + actual_inverse_integer_equalities=dict(source='A_Z^-1 x',dirty_helpers='all438 exactly h',private='exactly zero'), + signed_prefix_F=F,signed_prefix_R=R, + old_formula_screen_with_exact_signed_norms=dict(local_bits=(64*F**3*R**2).bit_length(), + nine_bits=((1<<18)*F**5*R**4).bit_length(), + applicability='Requires new proof that exact signed coefficient norms meet the native rounded-network contract'), + cancellation_free=base.positive_bounds(records,N), + local_frame_invoice=native_scalar_forward, + local_reverse_frame_invoice=native_scalar_reverse, + ADDs=sum(r[0] == 1 for r in records), + negative_controls=controls, + scope='Exact full660-column integer forward, inverse, parity and helper restoration. The target/source coded BIT identity is modulo2, not equality overZ.', + unresolved=['Native/global63-code-bridge invoice and its signed source code', + 'Complete rounded-network perturbation weights and precision/payload reserve', + 'Terminal N E^-1 N, chronological owner and all-size physical supplier']) + (HERE/'BIT-SIGNED-LIFT.json').write_text(json.dumps(output,indent=2,sort_keys=True)+'\n') + print(json.dumps({k:output[k] for k in ('status','signed_changes','signed_prefix_F','signed_prefix_R', + 'old_formula_screen_with_exact_signed_norms','source_code','ADDs')}, + indent=2,sort_keys=True)) + + +if __name__ == '__main__': + main() diff --git a/research/bit-r438-source-code/producer/bit_transvection.py b/research/bit-r438-source-code/producer/bit_transvection.py new file mode 100644 index 0000000000..1c951d55fe --- /dev/null +++ b/research/bit-r438-source-code/producer/bit_transvection.py @@ -0,0 +1,350 @@ +#!/usr/bin/env python3 +"""Exact R438 local replacement with a coded source and literal dirty repairs. + +This is a changed local interface, not an admitted nine-stage supplier. All +660 public scalar input columns are independent over F2. The native operator +and integer-lift/controller obligations are independently owned by the sibling +recursive specialist. No source checkout is modified. +""" +from collections import Counter +import gzip +import hashlib +import importlib.util +import json +from pathlib import Path +import sys + +sys.dont_write_bytecode = True +HERE = Path(__file__).resolve().parent +REPO = HERE.parents[2] # rebound explicitly by reconstruct.py +WORD = REPO / 'research/bit-r438-transport-rehost/words/r438-t154.json.gz' +BUILDER = REPO / 'research/bit-boundary-persistence/build.py' +MAIN_PIN = '20ecf2891d80b5acf18d980b2164fb44ea7faa90' +WORD_SHA = 'a353999bceac4ac957f540adfd3e5f8768297138b27132eeb83332e2ea4b1022' +BUILDER_SHA = '58f402c365eb18b9c3dd736523999676f1d1652e40c1a9b4f6967c1b7acb72df' + + +def require(value, message): + if not value: + raise ValueError(message) + + +def bits(mask): + while mask: + low = mask & -mask + yield low.bit_length() - 1 + mask ^= low + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(',', ':')).encode() + + +def rank(rows): + pivots = {} + for row in rows: + while row: + pivot = row.bit_length() - 1 + if pivot in pivots: + row ^= pivots[pivot] + else: + pivots[pivot] = row + break + return len(pivots) + + +def product(left, right): + """Rows of left times rows of right, both bit-packed over F2.""" + return [sum_xor(right[j] for j in bits(row)) for row in left] + + +def sum_xor(values): + result = 0 + for value in values: + result ^= value + return result + + +def inverse(rows): + n = len(rows) + aug = [row | (1 << (n + j)) for j, row in enumerate(rows)] + for j in range(n): + pivot = next((i for i in range(j, n) if aug[i] >> j & 1), None) + require(pivot is not None, 'Singular section') + aug[j], aug[pivot] = aug[pivot], aug[j] + for i in range(n): + if i != j and aug[i] >> j & 1: + aug[i] ^= aug[j] + require([row & ((1 << n) - 1) for row in aug] == [1 << j for j in range(n)], + 'Inverse left block failed') + return [row >> n for row in aug] + + +def load(): + require(hashlib.sha256(WORD.read_bytes()).hexdigest() == WORD_SHA, + 'R438 source gzip pin changed') + require(hashlib.sha256(BUILDER.read_bytes()).hexdigest() == BUILDER_SHA, + 'Baseline replay source pin changed') + word = json.loads(gzip.decompress(WORD.read_bytes())) + require((word['v'], word['R'], word['h']) == (111, 438, 8), 'Wrong dimensions') + spec = importlib.util.spec_from_file_location('pinned_boundary_builder', BUILDER) + builder = importlib.util.module_from_spec(spec) + spec.loader.exec_module(builder) + baseline, records = builder.replay(word) + return word, builder, baseline, records + + +def matrices(word): + v, count = word['v'], 2 * word['v'] + word['R'] + rows = [1 << j for j in range(count)] + for phase in ('D', 'A'): + for _, dst, sources in word[phase]: + for src in sources: + rows[dst] ^= rows[src] + ret_rows = [rows[j] for j in word['ret']] + source_mask = (1 << v) - 1 + helper_mask = ((1 << count) - 1) ^ ((1 << (2 * v)) - 1) + require(all(row & ~ (source_mask | helper_mask) == 0 for row in ret_rows), + 'A retained total reads an arbitrary target') + R = [row & source_mask for row in ret_rows] + T = [row & helper_mask for row in ret_rows] + K = [sum(1 << j for j in subset) for subset in word['scatter']] + M = product(R, K) + require(M == [507, 135, 238, 349, 185, 437, 205, 503, 425], 'RK changed') + require(rank(M) == 9 and rank(R) == 9, 'Wrong query rank') + selected, columns = [], [] + for p in range(v): + column = sum(((row >> p) & 1) << j for j, row in enumerate(R)) + if rank(columns + [column]) > len(columns): + selected.append(p) + columns.append(column) + if len(selected) == 9: + break + S = [sum(((row >> p) & 1) << j for j, p in enumerate(selected)) for row in R] + Sinv = inverse(S) + L = product(Sinv, M) + U = [0] * v + for j, p in enumerate(selected): + U[p] = L[j] + W = [k ^ u for k, u in zip(K, U)] + Q = product(U, R) + H = [(1 << p) ^ row for p, row in enumerate(product(W, R))] + J = [(1 << p) ^ row for p, row in enumerate(product(K, R))] + require(product(R, W) == [0] * 9, 'RW is not zero') + require(product(H, H) == [1 << p for p in range(v)], 'H is not involutive') + require(product(R, H) == R, 'RH differs from R') + require(product(J, H) == [(1 << p) ^ Q[p] for p in range(v)], 'JH residual failed') + require(product(Q, H) == Q, 'Repair query changes under H') + require([p for p, row in enumerate(Q) if row] == selected, 'Repair support changed') + return dict(R=R, T=T, K=K, M=M, selected=selected, S=S, Sinv=Sinv, + L=L, U=U, W=W, H=H, Q=Q, J=J) + + +def construct(word, baseline_records, data): + v, count = word['v'], 2 * word['v'] + word['R'] + require(all(f == 0 for f in word['start'][v:]), 'Initial target/helper frames differ') + require(all(f == 1 for f in word['final'][:v] + word['final'][2*v:]), + 'A source/helper is not FULL at the new H cut') + require(not any(v <= s < 2*v for phase in ('D', 'A', 'B', 'C') + for _, _, ss in word[phase] for s in ss), 'Target read in original word') + old_comp = [0] * v + for frame, dst, sources in word['D']: + require(frame == 0 and v <= dst < 2*v, 'Original D is not a zero-frame target shear') + for src in sources: + require(src >= 2*v, 'Original D reads data instead of a dirty helper') + old_comp[dst-v] ^= 1 << src + # The original D and extra KT compensation commute at frame zero. + # Cancel their duplicate parity gates before emitting the changed D. + comp = [old ^ extra for old, extra in zip(old_comp, product(data['K'], data['T']))] + prefix = [[1, v+p, src, 1, 0, 10] + for p, row in enumerate(comp) for src in bits(row)] + # Keep every original public-register frame visit, including empty-source + # visits. Only the nine owned copied totals and their scatter are removed. + clean = [rec[:] for rec in baseline_records + if rec[0] not in (2, 3) and not (rec[0] == 1 and (rec[2] == count or rec[5] == 1))] + borrow = list(range(2*v, 2*v+9)) + # Four simultaneous banks of CNOTs implement x -> (I+WR)x while every + # arbitrary dirty z_j is restored. RW=0 is checked above. + phase1 = [[1, p, borrow[j], 1, 1, 11] + for p, row in enumerate(data['W']) for j in bits(row)] + phase2 = [[1, borrow[j], p, 1, 1, 12] + for j, row in enumerate(data['R']) for p in bits(row)] + phase3 = [[1, p, borrow[j], 1, 1, 13] + for p, row in enumerate(data['W']) for j in bits(row)] + phase4 = [[1, borrow[j], p, 1, 1, 14] + for j, row in enumerate(data['R']) for p in bits(row)] + repairs = [] + b = borrow[0] + for p in data['selected']: + cap = word['final'][v+p] + # Each episode reads one physical unchanged dirty register b. The + # private field is zero before COPY and exactly equals b at ERASE. + # No zero-initialized query register or second simultaneous copy is used. + episode = [[2, b, count, 1, cap, 1], + [1, v+p, count, 1, cap, 15], + [3, b, count, 1, cap, 0]] + gather = [[1, b, src, 1, 1, 16] for src in bits(data['Q'][p])] + repairs.extend(episode) + repairs.extend(gather) + repairs.extend(episode) + repairs.extend([rec[:4] + [1, 17] for rec in gather]) + records = prefix + clean + phase1 + phase2 + phase3 + phase4 + repairs + parts = dict(prefix=prefix, clean=clean, H1=phase1, H2=phase2, H3=phase3, + H4=phase4, repairs=repairs) + return records, parts + + +def replay(word, builder, records, data, reverse=False, mutate_snapshot=False): + v, count = word['v'], 2 * word['v'] + word['R'] + values = [1 << j for j in range(count)] + [0] + current = (word['final'] if reverse else word['start'])[:] + masks = [sum(1 << j for j in frame) for frame in word['frames']] + dims = [builder.rank(word['lines'][j] for j in frame) for frame in word['frames']] + profile, live, snapshots, paths = Counter(), None, 0, [[f] for f in current] + old_private, changed = None, False + for number, rec in enumerate(reversed(records) if reverse else records): + op, dst, src, coefficient, frame, phase = rec + if op == 0: + old, new, paid = src, coefficient, frame + if reverse: + old, new = new, old + require(current[dst] == old, f'Wrong climb start at {number}') + require((masks[new] & ~masks[old] == 0) if reverse else + (masks[old] & ~masks[new] == 0), f'Non-nested move {number}') + require(abs(dims[new]-dims[old]) == paid, f'Wrong climb rank {number}') + current[dst] = new + paths[dst].append(new) + profile[paid] += 1 + elif op == 1: + require(current[dst] == frame, f'Wrong ADD destination frame {number}') + require((old_private if src == count else current[src]) == frame, + f'Wrong ADD source frame {number}') + require(src != count or live is not None, 'Read from erased private field') + values[dst] ^= values[src] + if mutate_snapshot and live is not None and not changed: + values[live] ^= 1 + changed = True + elif op == (3 if reverse else 2): + require(live is None and values[count] == 0, 'COPY overwrites live dirt') + require(current[dst] == coefficient, 'COPY source frame differs') + require(masks[frame] & ~masks[coefficient] == 0, 'COPY goes upward') + paid = dims[coefficient]-dims[frame] + require(paid > 0, 'Nonpositive COPY rank') + profile[paid] += 1 + values[count] = values[dst] + old_private, live = frame, dst + snapshots += 1 + elif op == (2 if reverse else 3): + require(live == dst and old_private == frame, 'ERASE mismatched source/frame') + require(current[dst] == coefficient, 'ERASE source frame differs') + require(values[count] == values[dst], f'ERASE snapshot changed at {number}') + values[count], old_private, live = 0, None, None + else: + raise ValueError(f'Unknown operation {op}') + require(live is None and values[count] == 0, 'Private field not clear') + require(current == (word['start'] if reverse else word['final']), 'Final frames differ') + expected = [1 << j for j in range(count)] + [0] + for p in range(v): + expected[p] = data.get('Hinv', data['H'])[p] if reverse else data['H'][p] + expected[v+p] ^= (1 << p) if reverse else data['H'][p] + require(values == expected, f'Wrong {"reverse" if reverse else "forward"} dirty map') + return dict(public_columns=count, nonzero_output_rows=sum(bool(x) for x in values), + endpoint_sha256=hashlib.sha256(canonical(values)).hexdigest(), + profile=dict(sorted(profile.items())), + rank_mass=sum(k*n for k,n in profile.items()), copies=snapshots, + max_live_copies=1, dirty_helpers_restored=word['R'], + paths_sha256=hashlib.sha256(canonical(paths)).hexdigest()) + + +def positive_bounds(records, count): + bounds = [] + for reverse in (False, True): + values, maximum = [1] * count + [0], 1 + for op, dst, src, coefficient, frame, phase in reversed(records) if reverse else records: + if op == 1: + values[dst] += values[src] + maximum = max(maximum, values[dst]) + elif op == (3 if reverse else 2): + values[count] = values[dst] + maximum = max(maximum, values[count]) + elif op == (2 if reverse else 3): + values[count] = 0 + bounds.append(maximum) + F, R = bounds + local, nine = 64*F**3*R**2, (1 << 18)*F**5*R**4 + return dict(forward=F, reverse=R, local_bits=local.bit_length(), nine_bits=nine.bit_length(), + historical_local_guard_pass=local < 1 << 104, + historical_nine_guard_pass=nine < 1 << 192, + applicability='Numerical screen only; changed source-code interface not admitted') + + +def must_fail(name, thunk): + try: + thunk() + except (ValueError, AssertionError) as error: + return dict(name=name, detected=True, message=str(error)) + raise ValueError(f'Negative control escaped: {name}') + + +def main(): + word, builder, baseline, old_records = load() + data = matrices(word) + records, parts = construct(word, old_records, data) + forward = replay(word, builder, records, data) + reverse = replay(word, builder, records, data, reverse=True) + expect = Counter({int(k): n for k,n in baseline['profile'].items()}) + expect[7] -= 9 + expect[1] += 18 + require(forward['profile'] == dict(sorted(expect.items())), 'Unexpected profile delta') + require(reverse['profile'] == forward['profile'], 'Reverse profile differs') + require(forward['rank_mass'] == 5076 and forward['copies'] == 18, 'Wrong local bill') + controls = [ + must_fail('omit_changed_dirty_compensation', lambda: replay( + word, builder, records[len(parts['prefix']):], data)), + must_fail('omit_first_bulk_H_phase', lambda: replay( + word, builder, [r for r in records if not (r[0] == 1 and r[5] == 11)], data)), + must_fail('omit_repair_dirty_restore', lambda: replay( + word, builder, [r for r in records if not (r[0] == 1 and r[5] == 17)], data)), + must_fail('mutate_live_snapshot_source', lambda: replay( + word, builder, records, data, mutate_snapshot=True)), + ] + container = dict(format='coded-r438-local-records-v1', register_order='X0..110,Y0..110,H0..437,C', + public_registers=660, private_register=660, word_path=str(WORD), + word_gzip_sha256=WORD_SHA, start=word['start'], final=word['final'], + record_schema='[op,dst,src,coefficient/sourceframe,frame/privateframe,phase/rank]', + copy_schema='[2,physical_source,660,sourceframe,privateframe,rank]', + erase_schema='[3,physical_source,660,sourceframe,privateframe,0]', + records=records) + raw = canonical(container) + outword = HERE / 'BIT-TRANSVECTION-WORD.json.gz' + outword.write_bytes(gzip.compress(raw, mtime=0)) + output = dict(status='PASS_CHANGED_LOCAL_GF2_INTERFACE_NO_GLOBAL_SUPPLIER_NO_NEW_KAPPA', + source_pin=MAIN_PIN, source_word=str(WORD), source_gzip_sha256=WORD_SHA, + source_builder=str(BUILDER), builder_sha256=hashlib.sha256(BUILDER.read_bytes()).hexdigest(), + output_word=str(outword), output_canonical_sha256=hashlib.sha256(raw).hexdigest(), + output_gzip_sha256=hashlib.sha256(outword.read_bytes()).hexdigest(), + matrices=data, source_query_supports=[r.bit_count() for r in data['R']], + helper_query_supports=[r.bit_count() for r in data['T']], + baseline={k:v for k,v in baseline.items() if k != 'paths'}, + forward=forward, reverse=reverse, + adds=sum(r[0] == 1 for r in records), records=len(records), + part_adds={k:sum(r[0] == 1 for r in rows) for k,rows in parts.items()}, + positive=positive_bounds(records, 660), negative_controls=controls, + contract=dict(forward='(x,y,h)->(Hx,y+Hx,h)', + literal_inverse='(x,y,h)->(Hx,y+x,h)', + initial_frames='source Pp; target0; every helper0', + final_frames='source FULL; target Pp-perp; every helper FULL', + private='One live immutable copied snapshot; zero between episodes', + changed_original_hypotheses=['H4: appended source H and helpers restored by a new word', + 'End source is coded Hx, not x']), + unresolved=['Independent exact native operator lift including complementary backward cuts', + 'Ordered signed integer lift and applicable precision theorem', + 'Whole9-stage controller code removal at actual cap queries', + 'Chronological owner/stock and complete outer recurrence admission']) + (HERE / 'BIT-TRANSVECTION.json').write_text(json.dumps(output, indent=2, sort_keys=True)+'\n') + print(json.dumps({k:output[k] for k in ('status','forward','adds','records','part_adds','positive')}, + indent=2, sort_keys=True)) + + +if __name__ == '__main__': + main() diff --git a/research/bit-r438-source-code/producer/build_support_code.py b/research/bit-r438-source-code/producer/build_support_code.py new file mode 100644 index 0000000000..c4c5605e6b --- /dev/null +++ b/research/bit-r438-source-code/producer/build_support_code.py @@ -0,0 +1,131 @@ +#!/usr/bin/env python3 +"""R438 source code that only deletes support from each K column. + +Three actual source rows remain identity. Target repair is still three direct +source-pivot snapshots. A matched native global decoder is NOT supplied. +Apache-2.0; substantial OpenAI Codex assistance. +""" +from collections import Counter +import gzip +import hashlib +import json +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent +SOURCE = HERE # rebound to fresh signed ancestry by reconstruct.py +sys.dont_write_bytecode = True +import bit_transvection as base +import bit_section_code as section +import bit_scalar_invoice as scalar +import bit_signed_lift as signed + + +def authenticate_predecessor(packed): + raise ValueError('Use reconstruct.py to authenticate the regenerated predecessor payload') + + +def main(): + old_blob = (SOURCE/'BIT-SIGNED-WORD.json.gz').read_bytes() + authenticate_predecessor(old_blob) + old_word = json.loads(gzip.decompress(old_blob)) + original,builder,baseline,_ = base.load() + raw = base.matrices(original) + data = section.section(raw) + selected = data['selected'] + pk = [raw['K'][p] for p in selected] + y = [a^b for a,b in zip(data['N'],base.product(data['S'],pk))] + base.require(base.rank(y) == 9,'Support-preserving quotient is singular') + wprime = [0 if p in selected else row for p,row in enumerate(raw['K'])] + a = [(1<