diff --git a/research/qq16-cut-operator-audit/PREDECESSORS.json b/research/qq16-cut-operator-audit/PREDECESSORS.json new file mode 100644 index 0000000000..532c0387fe --- /dev/null +++ b/research/qq16-cut-operator-audit/PREDECESSORS.json @@ -0,0 +1,26 @@ +[ + { + "pr": 2443, + "head": "545c05e17243c962b112b91e7f84b4c1a41de7b8", + "path": "research/qq16-coordinate-cut-decoder/README.md", + "sha256": "91d68f5d01d89ee78802ee5f76e8b901199a686aaa62341090eb70c458fd070e", + "git_blob": "1ae3d3eb976ed85f795da2c211b58577ed7e8a82", + "usage": "Reviewed source context; not imported at runtime" + }, + { + "pr": 2443, + "head": "545c05e17243c962b112b91e7f84b4c1a41de7b8", + "path": "research/qq16-coordinate-cut-decoder/verify.py", + "sha256": "7decbde0922eb8b1473e1cf4ad0b65eee69f040c40ad0bea3b415e82bd129dc7", + "git_blob": "e4bcea403a0db78115eba60ab8ec78294cea0c5c", + "usage": "Reviewed source context; not imported at runtime" + }, + { + "pr": 2432, + "head": "cbede349fc764aa38379aa533befe3215916cfcd", + "path": "research/qq16-eight-axis-readsets/README.md", + "sha256": "4dfcd20ded63c965bd6616a1226ea551d440723a320c447cd696b4960424aee1", + "git_blob": "b2100ddb6c28360605c88fc9fbd69488c8de7dc2", + "usage": "Reviewed source context; not imported at runtime" + } +] diff --git a/research/qq16-cut-operator-audit/PROOF.md b/research/qq16-cut-operator-audit/PROOF.md new file mode 100644 index 0000000000..30407973d7 --- /dev/null +++ b/research/qq16-cut-operator-audit/PROOF.md @@ -0,0 +1,99 @@ +# What the exact operator check establishes + +This is an audit of PR2443's retained-cut decoder, whose result and original +derivation remain credited there. We use exactly its granted observations. + +## Faithful expression representation + +Let G be the finite subgroup generated by the actual binary orthogonal owner +maps. For `g in G` and `a in F2^73`, the affine view acts on arbitrary arrays as + +``` +M(g,a) f(d,z_1,...,z_lambda) + = f(d g,z_1+d a,...,z_lambda+d a), lambda >= 1. +M(g,a) M(h,b) = M(g h,a+g b). +``` + +An expression is a finite rational sum of symbols `(input array, g, a)`. +The checker multiplies matrices over F2 and shifts by this semidirect law, +collecting exactly equal symbols. A zero expression is therefore a universal +operator identity, for arbitrary arrays and every positive tensor power. + +Conversely distinct `(g,a)` evaluate at `d=I` and every `z_i=0` at distinct +array addresses `(g,a,...,a)`. For a nonzero expression, select one nonzero +coefficient and set only that input array's value at that address to one. +All other input values are zero. The output residual at `(I,0,...,0)` is +exactly that coefficient. This gives an independently inspectable concrete +counterexample from each `negative_controls` entry in RESULT.json. No regular +cover enumeration or numerical rank estimate is needed. + +The logical chart in the inherited QQ16 formulas is `D=M(rho,0)`. Physical +alignment is `A=M(rho,delta)`, and the native boundary gauges relate them by +`A T = T_common D`. They cannot be substituted for one another in a logical +decoder. This audit inherits that bridge identity; it does not re-prove it. + +## Factorization avoids a finite input sampling assumption + +Write `H` for the map from arbitrary post-F0 `(x1,y1)` to the granted cut +observations. The source formulas used in H are only + +``` +y2_A = y1_A + P_(2,A) [B_2 y1_U + ell_(2,T) y1_T] +C = x2_U = x1_U - y1_U. +``` + +Together with the 32 selected post-F0 arrays and the 88 read ordinary arrays, +these are exactly 224 output arrays. Let `Hinv` be the audit's decoder on this +post-F0 state. From the selected logger difference it computes + +``` +v = ell_(2,A) (y2_A-y1_A) - ell_(2,T) y1_T + B_2 C + = B_2 x1_U. +rhs = v - B_(2,S) x1_S = R_J D_(2,J) x1_J. +x1_J = D_(2,J)^(-1) R_J^(-1) rhs. +y1_U = x1_U - C. +``` + +The scalar inverse is applied before each distinct port inverse. The selected +post-F0 state was retained directly. The checker verifies `Hinv H=I` on 224 +independent formal input arrays. Independently granting all 224 output arrays, +it verifies `H Hinv=I`. Thus no hidden consistency relation on the saved records +is used by either direction. + +It separately reconstructs the conserved forward F0 and its inverse from the +main source contract. Both `Finv F=I` and `F Finv=I` hold on 224 independent +formal arrays. Consequently the full observation transform is `H F`, with +two-sided inverse `Finv Hinv`. This establishes the audited arbitrary-input +identity under the inherited QQ16 local contract. It is not a proof of native +availability of H's records. + +## Payload-sensitive negative control + +In the decoder only, replace every logical stage-2 map and its inverse by the +actual corresponding native alignment and inverse. Keep the observed data +produced by H unchanged. The resulting output has a nonzero residual in the +full affine algebra; its explicit input-array/address/coefficient witness is +recorded under `native_alignment_for_logical_chart`. + +Now project every symbol `(v,g,a)` to `(v,g,0)`, combining coefficients again. +This projection is exactly restriction to payload-constant input arrays. The +entire faulty result becomes the identity after that projection. The checker +tests all 224 rows of this statement. Therefore the mutation is invisible to +all payload-constant fixtures, not merely to a chosen finite fixture set. + +This does not identify a bug in PR2443. Its code uses owner-only logical routes; +its proof invokes the proper inherited contract. The control provides a precise +failure mode for future physical lowering and a stronger regression target. + +## Source coverage and proof boundary + +R is independently reconstructed by propagating the source scalar prefix to +its centre boundary. Stage-1 and stage-2 owner routes and payload translations +are reconstructed from the retained phase geometry and compared with all 224 +registered entry/inverse pairs. The first two selected-template events are +bound to pair zero, with F0 followed directly by B1. The packet's selected +partition, K, selected and ordinary Grams, and unread minor are checked exactly. + +The proof applies to the granted two-cut logical interface. The audit does not +execute the whole backward native word, prove legal reads at mixed frames, +retain records through later calls, count native costs, or admit a supplier. diff --git a/research/qq16-cut-operator-audit/README.md b/research/qq16-cut-operator-audit/README.md new file mode 100644 index 0000000000..de6288549c --- /dev/null +++ b/research/qq16-cut-operator-audit/README.md @@ -0,0 +1,104 @@ +# QQ16 retained-cut decoder: independent exact operator audit + +**The ordered recovery in PR2443 passes an independent symbolic audit.** The +checker verifies both inverse orders on all 224 formal input arrays and all +224 independently specified observation arrays, using actual 73-dimensional +owner maps. No producer executable is imported. No new supplier or kappa is +claimed. + +The additional failure control separates logical and physical charts: replacing +the logical owner-only map `D=(rho,0)` in the decoder with the native alignment +`A=(rho,delta)` produces a nonzero exact arbitrary-payload residual. The same +fault passes after every payload shift is forgotten. Thus payload-constant +fixtures alone cannot distinguish this incorrect implementation. This is a +deliberately injected fault, **not a defect found in PR2443**, which correctly +uses the logical maps. + +## Audited contract and evidence + +The audited predecessor is [PR2443](https://github.com/CrocSwap/integer-mult-bounds/pull/2443) +at `545c05e17243c962b112b91e7f84b4c1a41de7b8`. Read source hashes are in +[PREDECESSORS.json](PREDECESSORS.json). Its unread ports are +`J=[1,2,3,4,5,6,8,12]`; the other 88 ordinary ports are read. With +`(x1,y1)=F0(x,y)` and `(x2,y2)=B_1_2(x1,y1)`, exactly these observations are +granted, without intervening changes: + +- `x1_A/T` and `y1_A/T`: 32 complete arrays at the F0 cut; +- `y2_A` and `C=x2_U`: 104 complete arrays at the B1 cut; +- `x1_(U\J)`: 88 complete arrays at the F0 cut. + +This is 224 arrays in total, not 88 total records. Each array includes arbitrary +owner and payload contents. The retained first two events operate on pair zero; +the other three pairs are not decoded. + +The [proof and audit interpretation](PROOF.md) explain the factorization into +F0 and the cut observation map. The checker reconstructs R from the immutable +predecessor's scalar prefix, rebuilds stage-1/stage-2 routes and translations +from its phase geometry, and compares all 224 entry/inverse pairs with the +emitted QQ16 packet. It checks the selected Grams, K, unread minor and both +minor inverse orders. Formal expressions retain independent array identifiers +and exact affine owner/payload operators, with rational coefficients. + +[RESULT.json](RESULT.json) records four complete inverse identities and seven +rejected faults, including a concrete point-supported input for each residual. +The six other controls omit the old A baseline, omit the future T term, reverse +the C sign, apply port inverses before the scalar inverse, discard the B1 A +cut, or discard initial Y dirt. Source-file corruption controls and optimized +replay are registered separately. No floating-point acceptance is used. + +## Reproduce + +Python 3.10+ and the standard library suffice for the direct checker. The +repository's registered environment is Python 3.12: + +```sh +python3 -I -B research/qq16-cut-operator-audit/verify.py +python3.12 -I -B scripts/research_package.py --package research/qq16-cut-operator-audit +``` + +Expected direct status: `PASS_QQ16_CUT_OPERATOR_AUDIT`. Replay is read-only and +compares the entire recomputed receipt with the committed file. Receipt creation +is explicit via `--write-result` and refuses to overwrite an existing file. +The source archive and frozen packages remain unchanged. Sources and Git +provenance are in [SOURCES.json](SOURCES.json); scope is in [TASK.json](TASK.json). + +## Limits + +This checks the mathematical decoder from PR2443's displayed formulas, not the +execution of its Python implementation. It imports no implementation from that +PR. The inherited QQ16 logical local contract, physical/logical conjugation, +and legal native kernels are not re-proved. The extra native-alignment mutation +is a diagnostic on the logical decoder; it does not execute a physical decoder. + +Neither the remaining 17 schedule events nor final endpoint availability is +checked. Retaining the two cuts, native read permissions, storage, cleanup, +hosting, addresses, precision, all-size transfer, and the complete invoice +remain open. Four operator identities are not a formal verification of the +full multiplication theorem. No full selected cold replay was needed or run. + +## Open next questions + +1. Can a physical implementation realize the decoder with the correct + input/output gauges? First trace each read in the pinned formula through + the bridge relation `A T = T_common D`. The missing work is the mixed + endpoint types and retention, not the scalar inverse. +2. Can the two retained cuts be reconstructed at final controller endpoints? + First propagate the 224 observation arrays through the complete remaining + schedule. A favorable scalar identity alone supplies no legal record. + +Both questions and their blockers are recorded in [TASK.json](TASK.json). + +## Credit + +`starship-s` / PR2443 supplies the audited arbitrary-input cut decoder and its +observation contract; Gareth Davidson / PR2432 supplies its unread basis and +coordinate-read lineage. commdata2338 / PR2174 supplies the earlier two-query +cut recovery. Ali Romman / PR1969 supplies the QQ16 local maps and native +contract; Adam Gall / PR2093, kyzer1023 / PR2354, PR2389 and PR2419 supply +the hidden-family and read-set work. The retained Rohan Arun, Jeremy Kothe, +DreamingOfClouds and other source contributors keep their attribution in +[the source notice](../joint-query/NOTICE.md). + +The independent reviewer code, exact operator audit, and diagnostic control +were prepared by ywz65 with substantial OpenAI Codex assistance. No independent +human or proof-assistant review is claimed. New work is Apache-2.0. diff --git a/research/qq16-cut-operator-audit/RESULT.json b/research/qq16-cut-operator-audit/RESULT.json new file mode 100644 index 0000000000..1f733e3b54 --- /dev/null +++ b/research/qq16-cut-operator-audit/RESULT.json @@ -0,0 +1,2340 @@ +{ + "R_J": [ + [ + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "1" + ], + [ + "1", + "1", + "1", + "1", + "1", + "1", + "1", + "0" + ], + [ + "1", + "0", + "0", + "0", + "0", + "1", + "0", + "1" + ], + [ + "0", + "0", + "1", + "1", + "1", + "0", + "-1", + "0" + ], + [ + "-1", + "0", + "-1", + "0", + "0", + "1", + "1", + "1" + ], + [ + "0", + "0", + "0", + "-1", + "1", + "0", + "0", + "0" + ], + [ + "0", + "1", + "1", + "0", + "0", + "0", + "1", + "1" + ], + [ + "-1", + "-1", + "0", + "-1", + "-1", + "1", + "0", + "0" + ] + ], + "R_J_inverse": [ + [ + "-1/4", + "0", + "1/2", + "-1/4", + "-1/4", + "0", + "0", + "-1/4" + ], + [ + "5/4", + "1/2", + "-1/2", + "-1/4", + "-1/4", + "0", + "-1/2", + "1/4" + ], + [ + "-1/4", + "0", + "0", + "1/4", + "-1/4", + "0", + "1/2", + "1/4" + ], + [ + "-1/4", + "0", + "0", + "1/4", + "1/4", + "-1/2", + "0", + "-1/4" + ], + [ + "-1/4", + "0", + "0", + "1/4", + "1/4", + "1/2", + "0", + "-1/4" + ], + [ + "1/2", + "1/2", + "0", + "0", + "0", + "0", + "-1/2", + "1/2" + ], + [ + "-3/4", + "0", + "0", + "-1/4", + "1/4", + "0", + "1/2", + "-1/4" + ], + [ + "-1/4", + "-1/2", + "1/2", + "1/4", + "1/4", + "0", + "1/2", + "-1/4" + ] + ], + "archive_members": { + "slots/local/CANONICAL-WORD.json.gz": "16bc0ebb04b4be6c0ade74badc6a0c0cdba4215eda86e4ff9f13abf8ecebd219", + "slots/local/LOCAL-PROGRAMS.json.gz": "241fde27d4e43f5a9cb6b128f9f76c5131a53d09f0371676163f914d0b0fef3a", + "t16/global/base/split-centres/GLOBAL-TEMPLATE.json.gz": "a179dad87651aba340a5a8ddbcd86a8e757cad87b8a1f8bad48106fbecd38518", + "t16/global/base/work/complex-nine-native/DATA-PHASES.json": "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa" + }, + "formal_input_arrays": 224, + "formal_observation_arrays": 224, + "identities": [ + "F0_inverse F0 = I", + "F0 F0_inverse = I", + "cut_decode cut_observe = I", + "cut_observe cut_decode = I" + ], + "logical_charts_have_zero_payload_shift": true, + "native_substitution_passes_payload_constant_projection": true, + "negative_controls": { + "discard_B1_A_cut": { + "block": 0, + "coefficient": "-1", + "input_array": 113, + "owner_columns": [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256, + 512, + 1024, + 2048, + 4096, + 8192, + 16384, + 32768, + 65536, + 131072, + 262144, + 524288, + 1048576, + 2097152, + 4194304, + 8388608, + 16777216, + 33554432, + 67108864, + 134217728, + 268435456, + 536870912, + 1073741824, + 2147483648, + 4294967296, + 8589934592, + 17179869184, + 34359738368, + 68719476736, + 137438953472, + 274877906944, + 549755813888, + 1099511627776, + 2199023255552, + 4398046511104, + 8796093022208, + 17592186044416, + 35184372088832, + 70368744177664, + 140737488355328, + 281474976710656, + 562949953421312, + 1125899906842624, + 2251799813685248, + 4503599627370496, + 9007199254740992, + 18014398509481984, + 36028797018963968, + 72057594037927936, + 144115188075855872, + 288230376151711744, + 576460752303423488, + 1152921504606846976, + 2305843009213693952, + 4611686018427387904, + 9223372036854775808, + 18446744073709551616, + 36893488147419103232, + 73786976294838206464, + 147573952589676412928, + 295147905179352825856, + 590295810358705651712, + 1180591620717411303424, + 2361183241434822606848, + 4722366482869645213696 + ], + "payload_shift": 0, + "port": 1, + "terms_in_residual_row": 73 + }, + "discard_initial_Y_dirt": { + "block": 1, + "coefficient": "1", + "input_array": 1, + "owner_columns": [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256, + 512, + 1024, + 2048, + 4096, + 8192, + 16384, + 32768, + 65536, + 131072, + 262144, + 524288, + 1048576, + 2097152, + 4194304, + 8388608, + 16777216, + 33554432, + 67108864, + 134217728, + 268435456, + 536870912, + 1073741824, + 2147483648, + 4294967296, + 8589934592, + 17179869184, + 34359738368, + 68719476736, + 137438953472, + 274877906944, + 549755813888, + 1099511627776, + 2199023255552, + 4398046511104, + 8796093022208, + 17592186044416, + 35184372088832, + 70368744177664, + 140737488355328, + 281474976710656, + 562949953421312, + 1125899906842624, + 2251799813685248, + 4503599627370496, + 9007199254740992, + 18014398509481984, + 36028797018963968, + 72057594037927936, + 144115188075855872, + 288230376151711744, + 576460752303423488, + 1152921504606846976, + 2305843009213693952, + 4611686018427387904, + 9223372036854775808, + 18446744073709551616, + 36893488147419103232, + 73786976294838206464, + 147573952589676412928, + 295147905179352825856, + 590295810358705651712, + 1180591620717411303424, + 2361183241434822606848, + 4722366482869645213696 + ], + "payload_shift": 0, + "port": 1, + "terms_in_residual_row": 2 + }, + "inverse_before_scalar": { + "block": 0, + "coefficient": "-1", + "input_array": 1, + "owner_columns": [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256, + 512, + 1024, + 2048, + 4096, + 8192, + 16384, + 32768, + 65536, + 131072, + 262144, + 524288, + 1048576, + 2097152, + 4194304, + 8388608, + 16777216, + 33554432, + 67108864, + 134217728, + 268435456, + 536870912, + 1073741824, + 2147483648, + 4294967296, + 8589934592, + 17179869184, + 34359738368, + 68719476736, + 137438953472, + 274877906944, + 549755813888, + 1099511627776, + 2199023255552, + 4398046511104, + 8796093022208, + 17592186044416, + 35184372088832, + 70368744177664, + 140737488355328, + 281474976710656, + 562949953421312, + 1125899906842624, + 2251799813685248, + 4503599627370496, + 9007199254740992, + 18014398509481984, + 36028797018963968, + 72057594037927936, + 144115188075855872, + 288230376151711744, + 576460752303423488, + 1152921504606846976, + 2305843009213693952, + 4611686018427387904, + 9223372036854775808, + 18446744073709551616, + 36893488147419103232, + 73786976294838206464, + 147573952589676412928, + 295147905179352825856, + 590295810358705651712, + 1180591620717411303424, + 2361183241434822606848, + 4722366482869645213696 + ], + "payload_shift": 0, + "port": 1, + "terms_in_residual_row": 20 + }, + "native_alignment_for_logical_chart": { + "block": 0, + "coefficient": "-1", + "input_array": 113, + "owner_columns": [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256, + 512, + 1024, + 2048, + 4096, + 8192, + 16384, + 32768, + 65536, + 131072, + 262144, + 524288, + 1048576, + 2097152, + 4194304, + 8388608, + 16777216, + 33554432, + 67108864, + 134217728, + 268435456, + 536870912, + 1073741824, + 2147483648, + 4294967296, + 8589934592, + 17179869184, + 34359738368, + 68719476736, + 137438953472, + 274877906944, + 549755813888, + 1099511627776, + 2199023255552, + 4398046511104, + 8796093022208, + 17592186044416, + 35184372088832, + 70368744177664, + 140737488355328, + 281474976710656, + 562949953421312, + 1125899906842624, + 2251799813685248, + 4503599627370496, + 9007199254740992, + 18014398509481984, + 36028797018963968, + 72057594037927936, + 144115188075855872, + 288230376151711744, + 576460752303423488, + 1152921504606846976, + 2305843009213693952, + 4611686018427387904, + 9223372036854775808, + 18446744073709551616, + 36893488147419103232, + 73786976294838206464, + 147573952589676412928, + 295147905179352825856, + 590295810358705651712, + 1180591620717411303424, + 2361183241434822606848, + 4722366482869645213696 + ], + "payload_shift": 0, + "port": 1, + "terms_in_residual_row": 328 + }, + "omit_T": { + "block": 0, + "coefficient": "-1/2", + "input_array": 149, + "owner_columns": [ + 274, + 17957127, + 22, + 8, + 17957141, + 32, + 64, + 128, + 17956882, + 512, + 1024, + 2048, + 4096, + 8192, + 16384, + 32768, + 65536, + 18087936, + 1441792, + 524288, + 17170432, + 2097152, + 4194304, + 8388608, + 19, + 33554432, + 67108864, + 134217728, + 268435456, + 536870912, + 1073741824, + 2147483648, + 4294967296, + 8589934592, + 17179869184, + 34359738368, + 68719476736, + 137438953472, + 274877906944, + 549755813888, + 1099511627776, + 2199023255552, + 4398046511104, + 8796093022208, + 17592186044416, + 35184372088832, + 70368744177664, + 140737488355328, + 281474976710656, + 562949953421312, + 1125899906842624, + 2251799813685248, + 4503599627370496, + 9007199254740992, + 18014398509481984, + 36028797018963968, + 72057594037927936, + 144115188075855872, + 288230376151711744, + 576460752303423488, + 1152921504606846976, + 2305843009213693952, + 4611686018427387904, + 9223372036854775808, + 18446744073709551616, + 36893488147419103232, + 73786976294838206464, + 147573952589676412928, + 295147905179352825856, + 590295810358705651712, + 1180591620717411303424, + 2361183241434822606848, + 4722366482869645213696 + ], + "payload_shift": 0, + "port": 1, + "terms_in_residual_row": 5 + }, + "omit_old_A": { + "block": 0, + "coefficient": "-1", + "input_array": 119, + "owner_columns": [ + 131089, + 4, + 131090, + 8, + 131075, + 32, + 64, + 128, + 256, + 512, + 1024, + 2048, + 4096, + 8192, + 16384, + 32768, + 65536, + 262144, + 19, + 524288, + 1048576, + 2097152, + 4194304, + 8388608, + 16777216, + 33554432, + 67108864, + 134217728, + 268435456, + 536870912, + 1073741824, + 2147483648, + 4294967296, + 8589934592, + 17179869184, + 34359738368, + 68719476736, + 137438953472, + 274877906944, + 549755813888, + 1099511627776, + 2199023255552, + 4398046511104, + 8796093022208, + 17592186044416, + 35184372088832, + 70368744177664, + 140737488355328, + 281474976710656, + 562949953421312, + 1125899906842624, + 2251799813685248, + 4503599627370496, + 9007199254740992, + 18014398509481984, + 36028797018963968, + 72057594037927936, + 144115188075855872, + 288230376151711744, + 576460752303423488, + 1152921504606846976, + 2305843009213693952, + 4611686018427387904, + 9223372036854775808, + 18446744073709551616, + 36893488147419103232, + 73786976294838206464, + 147573952589676412928, + 295147905179352825856, + 590295810358705651712, + 1180591620717411303424, + 2361183241434822606848, + 4722366482869645213696 + ], + "payload_shift": 0, + "port": 1, + "terms_in_residual_row": 5 + }, + "wrong_C_sign": { + "block": 0, + "coefficient": "-2", + "input_array": 1, + "owner_columns": [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256, + 512, + 1024, + 2048, + 4096, + 8192, + 16384, + 32768, + 65536, + 131072, + 262144, + 524288, + 1048576, + 2097152, + 4194304, + 8388608, + 16777216, + 33554432, + 67108864, + 134217728, + 268435456, + 536870912, + 1073741824, + 2147483648, + 4294967296, + 8589934592, + 17179869184, + 34359738368, + 68719476736, + 137438953472, + 274877906944, + 549755813888, + 1099511627776, + 2199023255552, + 4398046511104, + 8796093022208, + 17592186044416, + 35184372088832, + 70368744177664, + 140737488355328, + 281474976710656, + 562949953421312, + 1125899906842624, + 2251799813685248, + 4503599627370496, + 9007199254740992, + 18014398509481984, + 36028797018963968, + 72057594037927936, + 144115188075855872, + 288230376151711744, + 576460752303423488, + 1152921504606846976, + 2305843009213693952, + 4611686018427387904, + 9223372036854775808, + 18446744073709551616, + 36893488147419103232, + 73786976294838206464, + 147573952589676412928, + 295147905179352825856, + 590295810358705651712, + 1180591620717411303424, + 2361183241434822606848, + 4722366482869645213696 + ], + "payload_shift": 0, + "port": 1, + "terms_in_residual_row": 126 + } + }, + "route_bindings": [ + [ + 2, + 0, + "m89", + "m201" + ], + [ + 1, + 0, + "m1", + "m3" + ], + [ + 2, + 1, + "m90", + "m202" + ], + [ + 1, + 1, + "m313", + "m409" + ], + [ + 2, + 2, + "m91", + "m203" + ], + [ + 1, + 2, + "m314", + "m410" + ], + [ + 2, + 3, + "m92", + "m204" + ], + [ + 1, + 3, + "m315", + "m411" + ], + [ + 2, + 4, + "m93", + "m205" + ], + [ + 1, + 4, + "m316", + "m412" + ], + [ + 2, + 5, + "m94", + "m206" + ], + [ + 1, + 5, + "m317", + "m413" + ], + [ + 2, + 6, + "m95", + "m207" + ], + [ + 1, + 6, + "m318", + "m414" + ], + [ + 2, + 7, + "m96", + "m208" + ], + [ + 1, + 7, + "m15", + "m16" + ], + [ + 2, + 8, + "m97", + "m209" + ], + [ + 1, + 8, + "m319", + "m415" + ], + [ + 2, + 9, + "m98", + "m210" + ], + [ + 1, + 9, + "m320", + "m416" + ], + [ + 2, + 10, + "m99", + "m211" + ], + [ + 1, + 10, + "m321", + "m417" + ], + [ + 2, + 11, + "m100", + "m212" + ], + [ + 1, + 11, + "m322", + "m418" + ], + [ + 2, + 12, + "m101", + "m213" + ], + [ + 1, + 12, + "m323", + "m419" + ], + [ + 2, + 13, + "m102", + "m214" + ], + [ + 1, + 13, + "m324", + "m420" + ], + [ + 2, + 14, + "m103", + "m215" + ], + [ + 1, + 14, + "m325", + "m421" + ], + [ + 2, + 15, + "m104", + "m216" + ], + [ + 1, + 15, + "m326", + "m422" + ], + [ + 2, + 16, + "m105", + "m217" + ], + [ + 1, + 16, + "m327", + "m423" + ], + [ + 2, + 17, + "m106", + "m218" + ], + [ + 1, + 17, + "m328", + "m424" + ], + [ + 2, + 18, + "m107", + "m219" + ], + [ + 1, + 18, + "m329", + "m425" + ], + [ + 2, + 19, + "m108", + "m220" + ], + [ + 1, + 19, + "m330", + "m426" + ], + [ + 2, + 20, + "m109", + "m221" + ], + [ + 1, + 20, + "m25", + "m27" + ], + [ + 2, + 21, + "m110", + "m222" + ], + [ + 1, + 21, + "m26", + "m427" + ], + [ + 2, + 22, + "m111", + "m223" + ], + [ + 1, + 22, + "m331", + "m428" + ], + [ + 2, + 23, + "m112", + "m224" + ], + [ + 1, + 23, + "m332", + "m429" + ], + [ + 2, + 24, + "m113", + "m225" + ], + [ + 1, + 24, + "m333", + "m430" + ], + [ + 2, + 25, + "m114", + "m226" + ], + [ + 1, + 25, + "m334", + "m431" + ], + [ + 2, + 26, + "m115", + "m227" + ], + [ + 1, + 26, + "m335", + "m432" + ], + [ + 2, + 27, + "m116", + "m228" + ], + [ + 1, + 27, + "m39", + "m40" + ], + [ + 2, + 28, + "m117", + "m229" + ], + [ + 1, + 28, + "m336", + "m433" + ], + [ + 2, + 29, + "m118", + "m230" + ], + [ + 1, + 29, + "m337", + "m434" + ], + [ + 2, + 30, + "m119", + "m231" + ], + [ + 1, + 30, + "m338", + "m435" + ], + [ + 2, + 31, + "m120", + "m232" + ], + [ + 1, + 31, + "m339", + "m436" + ], + [ + 2, + 32, + "m121", + "m233" + ], + [ + 1, + 32, + "m340", + "m437" + ], + [ + 2, + 33, + "m122", + "m234" + ], + [ + 1, + 33, + "m341", + "m438" + ], + [ + 2, + 34, + "m123", + "m235" + ], + [ + 1, + 34, + "m342", + "m439" + ], + [ + 2, + 35, + "m124", + "m236" + ], + [ + 1, + 35, + "m343", + "m440" + ], + [ + 2, + 36, + "m125", + "m237" + ], + [ + 1, + 36, + "m49", + "m50" + ], + [ + 2, + 37, + "m126", + "m238" + ], + [ + 1, + 37, + "m29", + "m441" + ], + [ + 2, + 38, + "m127", + "m239" + ], + [ + 1, + 38, + "m344", + "m442" + ], + [ + 2, + 39, + "m128", + "m240" + ], + [ + 1, + 39, + "m345", + "m443" + ], + [ + 2, + 40, + "m129", + "m241" + ], + [ + 1, + 40, + "m346", + "m444" + ], + [ + 2, + 41, + "m130", + "m242" + ], + [ + 1, + 41, + "m347", + "m445" + ], + [ + 2, + 42, + "m131", + "m243" + ], + [ + 1, + 42, + "m348", + "m446" + ], + [ + 2, + 43, + "m132", + "m244" + ], + [ + 1, + 43, + "m349", + "m447" + ], + [ + 2, + 44, + "m133", + "m245" + ], + [ + 1, + 44, + "m350", + "m448" + ], + [ + 2, + 45, + "m134", + "m246" + ], + [ + 1, + 45, + "m351", + "m449" + ], + [ + 2, + 46, + "m135", + "m247" + ], + [ + 1, + 46, + "m59", + "m60" + ], + [ + 2, + 47, + "m136", + "m248" + ], + [ + 1, + 47, + "m31", + "m450" + ], + [ + 2, + 48, + "m137", + "m249" + ], + [ + 1, + 48, + "m352", + "m451" + ], + [ + 2, + 49, + "m138", + "m250" + ], + [ + 1, + 49, + "m353", + "m452" + ], + [ + 2, + 50, + "m139", + "m251" + ], + [ + 1, + 50, + "m354", + "m453" + ], + [ + 2, + 51, + "m140", + "m252" + ], + [ + 1, + 51, + "m355", + "m454" + ], + [ + 2, + 52, + "m141", + "m253" + ], + [ + 1, + 52, + "m356", + "m455" + ], + [ + 2, + 53, + "m142", + "m254" + ], + [ + 1, + 53, + "m357", + "m456" + ], + [ + 2, + 54, + "m143", + "m255" + ], + [ + 1, + 54, + "m358", + "m457" + ], + [ + 2, + 55, + "m144", + "m256" + ], + [ + 1, + 55, + "m359", + "m458" + ], + [ + 2, + 56, + "m145", + "m257" + ], + [ + 1, + 56, + "m360", + "m459" + ], + [ + 2, + 57, + "m146", + "m258" + ], + [ + 1, + 57, + "m69", + "m70" + ], + [ + 2, + 58, + "m147", + "m259" + ], + [ + 1, + 58, + "m361", + "m460" + ], + [ + 2, + 59, + "m148", + "m260" + ], + [ + 1, + 59, + "m362", + "m461" + ], + [ + 2, + 60, + "m149", + "m261" + ], + [ + 1, + 60, + "m363", + "m462" + ], + [ + 2, + 61, + "m150", + "m262" + ], + [ + 1, + 61, + "m364", + "m463" + ], + [ + 2, + 62, + "m151", + "m263" + ], + [ + 1, + 62, + "m365", + "m464" + ], + [ + 2, + 63, + "m152", + "m264" + ], + [ + 1, + 63, + "m366", + "m465" + ], + [ + 2, + 64, + "m153", + "m265" + ], + [ + 1, + 64, + "m367", + "m466" + ], + [ + 2, + 65, + "m154", + "m266" + ], + [ + 1, + 65, + "m368", + "m467" + ], + [ + 2, + 66, + "m155", + "m267" + ], + [ + 1, + 66, + "m369", + "m468" + ], + [ + 2, + 67, + "m156", + "m268" + ], + [ + 1, + 67, + "m370", + "m469" + ], + [ + 2, + 68, + "m157", + "m269" + ], + [ + 1, + 68, + "m371", + "m470" + ], + [ + 2, + 69, + "m158", + "m270" + ], + [ + 1, + 69, + "m372", + "m471" + ], + [ + 2, + 70, + "m159", + "m271" + ], + [ + 1, + 70, + "m373", + "m472" + ], + [ + 2, + 71, + "m160", + "m272" + ], + [ + 1, + 71, + "m374", + "m473" + ], + [ + 2, + 72, + "m161", + "m273" + ], + [ + 1, + 72, + "m375", + "m474" + ], + [ + 2, + 73, + "m162", + "m274" + ], + [ + 1, + 73, + "m376", + "m475" + ], + [ + 2, + 74, + "m163", + "m275" + ], + [ + 1, + 74, + "m377", + "m476" + ], + [ + 2, + 75, + "m164", + "m276" + ], + [ + 1, + 75, + "m378", + "m477" + ], + [ + 2, + 76, + "m165", + "m277" + ], + [ + 1, + 76, + "m2", + "m478" + ], + [ + 2, + 77, + "m166", + "m278" + ], + [ + 1, + 77, + "m379", + "m479" + ], + [ + 2, + 78, + "m167", + "m279" + ], + [ + 1, + 78, + "m380", + "m480" + ], + [ + 2, + 79, + "m168", + "m280" + ], + [ + 1, + 79, + "m381", + "m481" + ], + [ + 2, + 80, + "m169", + "m281" + ], + [ + 1, + 80, + "m382", + "m482" + ], + [ + 2, + 81, + "m170", + "m282" + ], + [ + 1, + 81, + "m5", + "m483" + ], + [ + 2, + 82, + "m171", + "m283" + ], + [ + 1, + 82, + "m383", + "m484" + ], + [ + 2, + 83, + "m172", + "m284" + ], + [ + 1, + 83, + "m384", + "m485" + ], + [ + 2, + 84, + "m173", + "m285" + ], + [ + 1, + 84, + "m385", + "m486" + ], + [ + 2, + 85, + "m174", + "m286" + ], + [ + 1, + 85, + "m386", + "m487" + ], + [ + 2, + 86, + "m175", + "m287" + ], + [ + 1, + 86, + "m387", + "m488" + ], + [ + 2, + 87, + "m176", + "m288" + ], + [ + 1, + 87, + "m7", + "m489" + ], + [ + 2, + 88, + "m177", + "m289" + ], + [ + 1, + 88, + "m388", + "m490" + ], + [ + 2, + 89, + "m178", + "m290" + ], + [ + 1, + 89, + "m389", + "m491" + ], + [ + 2, + 90, + "m179", + "m291" + ], + [ + 1, + 90, + "m390", + "m492" + ], + [ + 2, + 91, + "m180", + "m292" + ], + [ + 1, + 91, + "m391", + "m493" + ], + [ + 2, + 92, + "m181", + "m293" + ], + [ + 1, + 92, + "m9", + "m494" + ], + [ + 2, + 93, + "m182", + "m294" + ], + [ + 1, + 93, + "m392", + "m495" + ], + [ + 2, + 94, + "m183", + "m295" + ], + [ + 1, + 94, + "m393", + "m496" + ], + [ + 2, + 95, + "m184", + "m296" + ], + [ + 1, + 95, + "m394", + "m497" + ], + [ + 2, + 96, + "m185", + "m297" + ], + [ + 1, + 96, + "m395", + "m498" + ], + [ + 2, + 97, + "m186", + "m298" + ], + [ + 1, + 97, + "m396", + "m499" + ], + [ + 2, + 98, + "m187", + "m299" + ], + [ + 1, + 98, + "m397", + "m500" + ], + [ + 2, + 99, + "m188", + "m300" + ], + [ + 1, + 99, + "m398", + "m501" + ], + [ + 2, + 100, + "m189", + "m301" + ], + [ + 1, + 100, + "m399", + "m502" + ], + [ + 2, + 101, + "m190", + "m302" + ], + [ + 1, + 101, + "m400", + "m503" + ], + [ + 2, + 102, + "m191", + "m303" + ], + [ + 1, + 102, + "m401", + "m504" + ], + [ + 2, + 103, + "m192", + "m304" + ], + [ + 1, + 103, + "m402", + "m505" + ], + [ + 2, + 104, + "m193", + "m305" + ], + [ + 1, + 104, + "m403", + "m506" + ], + [ + 2, + 105, + "m194", + "m306" + ], + [ + 1, + 105, + "m404", + "m507" + ], + [ + 2, + 106, + "m195", + "m307" + ], + [ + 1, + 106, + "m405", + "m508" + ], + [ + 2, + 107, + "m196", + "m308" + ], + [ + 1, + 107, + "m406", + "m509" + ], + [ + 2, + 108, + "m197", + "m309" + ], + [ + 1, + 108, + "m407", + "m510" + ], + [ + 2, + 109, + "m198", + "m310" + ], + [ + 1, + 109, + "m408", + "m511" + ], + [ + 2, + 110, + "m199", + "m311" + ], + [ + 1, + 110, + "m33", + "m512" + ], + [ + 2, + 111, + "m200", + "m312" + ], + [ + 1, + 111, + "m79", + "m80" + ] + ], + "scope": "Exact ordered QQ16 retained two-cut algebra on arbitrary owner/payload arrays; native execution and final controller availability are not checked", + "selected_ordinary_partition": { + "A": [ + 0, + 7, + 20, + 27, + 36, + 46, + 57, + 111 + ], + "T": [ + 21, + 37, + 47, + 76, + 81, + 87, + 92, + 110 + ], + "U": [ + 1, + 2, + 3, + 4, + 5, + 6, + 8, + 9, + 10, + 11, + 12, + 13, + 14, + 15, + 16, + 17, + 18, + 19, + 22, + 23, + 24, + 25, + 26, + 28, + 29, + 30, + 31, + 32, + 33, + 34, + 35, + 38, + 39, + 40, + 41, + 42, + 43, + 44, + 45, + 48, + 49, + 50, + 51, + 52, + 53, + 54, + 55, + 56, + 58, + 59, + 60, + 61, + 62, + 63, + 64, + 65, + 66, + 67, + 68, + 69, + 70, + 71, + 72, + 73, + 74, + 75, + 77, + 78, + 79, + 80, + 82, + 83, + 84, + 85, + 86, + 88, + 89, + 90, + 91, + 93, + 94, + 95, + 96, + 97, + 98, + 99, + 100, + 101, + 102, + 103, + 104, + 105, + 106, + 107, + 108, + 109 + ], + "read": [ + 9, + 10, + 11, + 13, + 14, + 15, + 16, + 17, + 18, + 19, + 22, + 23, + 24, + 25, + 26, + 28, + 29, + 30, + 31, + 32, + 33, + 34, + 35, + 38, + 39, + 40, + 41, + 42, + 43, + 44, + 45, + 48, + 49, + 50, + 51, + 52, + 53, + 54, + 55, + 56, + 58, + 59, + 60, + 61, + 62, + 63, + 64, + 65, + 66, + 67, + 68, + 69, + 70, + 71, + 72, + 73, + 74, + 75, + 77, + 78, + 79, + 80, + 82, + 83, + 84, + 85, + 86, + 88, + 89, + 90, + 91, + 93, + 94, + 95, + 96, + 97, + 98, + 99, + 100, + 101, + 102, + 103, + 104, + 105, + 106, + 107, + 108, + 109 + ], + "unread": [ + 1, + 2, + 3, + 4, + 5, + 6, + 8, + 12 + ] + }, + "source_sha256": { + "research/community-frontier1042-audit/selected-replay.tar.gz": "22c3f4dce4b897a1d423d1388801933e288b6a6b1906cb15e1b16a5eb68db754", + "research/joint-query/certificate.json.gz": "a5ed85fac5ebf3c091482a113ab0d351eb5a7892fe2841a35e16017ec1ff49f7", + "research/joint-query/evidence/CONSERVED-QQ16.md": "60f0de3a7205ba5046b5ae7ffa8bf2b1ea42ea46b498face0a77966b59e7f3fb", + "research/joint-query/evidence/JOINT-QUERY-TRANSFER.md": "9e13e73ebf3192a6548798c2f1d13bd4d83957e8db0dc34de12b1a5311a52a75", + "research/joint-query/evidence/QQ16-COVER-ACTION-ADDENDUM.md": "4bb4a68d8b4811b6d8364150612056bc124d38f1974d6f603dae68a99c4682fb" + }, + "status": "PASS_QQ16_CUT_OPERATOR_AUDIT" +} diff --git a/research/qq16-cut-operator-audit/SOURCES.json b/research/qq16-cut-operator-audit/SOURCES.json new file mode 100644 index 0000000000..e9d7facc0b --- /dev/null +++ b/research/qq16-cut-operator-audit/SOURCES.json @@ -0,0 +1,48 @@ +{ + "schema_version": 1, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "e8870e5917057d59b730eb14721a778639eca050", + "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7" + }, + { + "path": "research/joint-query/certificate.json.gz", + "usage": "input", + "git_blob": "c6e876d8b48d768214deee265ade428f8983b566", + "sha256": "a5ed85fac5ebf3c091482a113ab0d351eb5a7892fe2841a35e16017ec1ff49f7" + }, + { + "path": "research/joint-query/evidence/CONSERVED-QQ16.md", + "usage": "input", + "git_blob": "4639583c1be02c2fb60ed8a8072c9969ef1569ce", + "sha256": "60f0de3a7205ba5046b5ae7ffa8bf2b1ea42ea46b498face0a77966b59e7f3fb" + }, + { + "path": "research/joint-query/evidence/JOINT-QUERY-TRANSFER.md", + "usage": "input", + "git_blob": "a6805c58f23132f9420efebf90f5b7e863c2e179", + "sha256": "9e13e73ebf3192a6548798c2f1d13bd4d83957e8db0dc34de12b1a5311a52a75" + }, + { + "path": "research/joint-query/evidence/QQ16-COVER-ACTION-ADDENDUM.md", + "usage": "input", + "git_blob": "3dd1a990d7b9d57cfb20cf8e8dd45548f043a944", + "sha256": "4bb4a68d8b4811b6d8364150612056bc124d38f1974d6f603dae68a99c4682fb" + }, + { + "path": "research/community-frontier1042-audit/selected-replay.tar.gz", + "usage": "input", + "git_blob": "6f4dc6fe7631d8aacf8081fcaecf32197181685b", + "sha256": "22c3f4dce4b897a1d423d1388801933e288b6a6b1906cb15e1b16a5eb68db754" + } + ] +} diff --git a/research/qq16-cut-operator-audit/TASK.json b/research/qq16-cut-operator-audit/TASK.json new file mode 100644 index 0000000000..94a6254235 --- /dev/null +++ b/research/qq16-cut-operator-audit/TASK.json @@ -0,0 +1,82 @@ +{ + "schema_version": 1, + "task_id": "joint-query-controller", + "priority_revision": 4, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "original_card": { + "id": "joint-query-controller", + "question": "Can one explicitly changed QQ16 interface recover the missing chart query and close a two-call controller within a favorable full budget?", + "starting_points": [ + "research/joint-query/README.md", + "research/joint-query/evidence/QQ16-SELECTED-WITNESS.md", + "research/joint-query/evidence/JOINT-QUERY-TRANSFER.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Add one explicitly priced ordinary-to-selected observation and derive the ordered two-call map and inverse.", + "Change the first local pair or retained state, then test the existing lost-observation witness and price all new operations." + ], + "acceptance_gate": "Name the changed premise of the fixed F0/B1 observation obstruction. Show exactly which query is recovered, legal native reads and restoration, and a full favorable budget including cover maps, helpers and endpoints. Local inverse identities alone do not close the global controller.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the fixed-first-pair QQ16 witness before designing a controller. The checked #1969 local words do not evade that witness or supply global placement.", + "scope": "Source-bound orientation only. Read the named package and review before relying on its local evidence; this command is not its replay or supplier admission." + }, + "first_experiment": "Apply the existing witness to one proposed extra observation or changed first pair. If it still loses the required record, stop. Otherwise derive one ordered two-call identity and charge the added read, chart maps and restoration before extending to more stages.", + "bottleneck_link": "The native local words exist; retained query information and its physical access are the missing link to a composed recursive interface.", + "allowed_variations": [ + "One paid query, one changed first pair, or one precisely specified affine helper state.", + "A counterexample or lower bound for that exact proposed repair." + ], + "scope_change_triggers": [ + "Retaining the fixed first pair and ordinary schedule while allowing only homogeneous selected-only control, already excluded by the witness.", + "Treating cover-map counts as zero-cost physical address operations." + ], + "overlap_terms": [ + "QQ16", + "joint-query", + "changing-chart controller", + "selected observation", + "1969" + ] + }, + "scope_status": "changed", + "actual_scope": "Independent exact group-algebra audit of PR2443 retained F0/B1 cut decoder, including both inverse orders and a payload-sensitive logical/native-map confusion control.", + "scope_change_reason": "The live overlap includes positive arbitrary-input recovery in PR2443 and many existing lost-query bounds. Audit the positive ordered implication with formal arrays instead of repeating a covered witness or claiming a complete favorable supplier budget.", + "bottleneck_link": "Checks the recovered-record implication needed before physical lowering. The new negative control separates correct logical charts from native alignments, a fault invisible to payload-constant fixtures.", + "budget_minutes": 60, + "stop_rule": "Stop after both operator inverse orders, source binding, meaningful controls and independent review. No larger controller or supplier claim in this round.", + "outcome": "completed", + "evidence": "PROOF.md; verify.py; RESULT.json; test_package.py. Four formal identities and seven semantic controls, plus source integrity and independent map-law tests.", + "author": "ywz65", + "ai_assistance": "Substantial OpenAI Codex assistance in derivation, implementation, validation and prose; no independent human review claimed.", + "open_questions": [ + { + "question": "Can a physical implementation realize the decoder at its mixed native endpoint types?", + "why_it_matters": "The exact logical decoder does not make its reads legal or inexpensive.", + "first_step": "Trace each queried array using A T = T_common D and supply native wrappers for each endpoint.", + "blocked_by": "Retention, native read access, storage and cleanup have not been supplied." + }, + { + "question": "Can the granted two-cut records be recovered at the final controller endpoints?", + "why_it_matters": "Cut access is an essential hypothesis of the recovery theorem.", + "first_step": "Propagate all224 observation arrays through the17 remaining schedule events with actual frame types.", + "blocked_by": "No full changing-chart controller or paid retention plan." + } + ], + "freshness": { + "canonical_main": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "checked_at_utc": "2026-10-15T10:51:00Z", + "priority_revision": 4, + "overlap_cache_checked_at_utc": "2026-10-15T10:48:58.337146+00:00", + "open_pr_records": 647, + "discussion_records": 1177, + "limitations": "Cached complete-title/body/Discussion coverage, not every diff; root publication review must refresh overlap and heads." + }, + "coordination": "https://github.com/CrocSwap/integer-mult-bounds/pull/2443#issuecomment-6190393131" +} diff --git a/research/qq16-cut-operator-audit/VERIFY.json b/research/qq16-cut-operator-audit/VERIFY.json new file mode 100644 index 0000000000..167a82f16b --- /dev/null +++ b/research/qq16-cut-operator-audit/VERIFY.json @@ -0,0 +1,46 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/joint-query/certificate.json.gz", + "research/joint-query/evidence/CONSERVED-QQ16.md", + "research/joint-query/evidence/JOINT-QUERY-TRANSFER.md", + "research/joint-query/evidence/QQ16-COVER-ACTION-ADDENDUM.md", + "research/community-frontier1042-audit/selected-replay.tar.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Both exact group-algebra cut inverse orders, F0 inverse orders, source reconstruction and seven semantic controls" + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Optimized replay reproduces complete committed receipt" + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/test_package.py" + ], + "timeout_seconds": 120, + "checks": "Every live-source corruption rejects; affine composition at nonidentity owner, transported inverse shift, singular minor boundary" + } + ] +} diff --git a/research/qq16-cut-operator-audit/test_package.py b/research/qq16-cut-operator-audit/test_package.py new file mode 100644 index 0000000000..1c68c46d2c --- /dev/null +++ b/research/qq16-cut-operator-audit/test_package.py @@ -0,0 +1,62 @@ +"""Focused source-integrity and operator-law controls, standard library only.""" +import importlib.util +from pathlib import Path +import unittest +from unittest.mock import patch + +PACKAGE = Path(__file__).resolve().parent +spec = importlib.util.spec_from_file_location("qq16_cut_reviewer", PACKAGE / "verify.py") +audit = importlib.util.module_from_spec(spec) +spec.loader.exec_module(audit) + + +class PackageChecks(unittest.TestCase): + def test_every_live_source_corruption_rejected(self): + raw = audit.source_bytes() + original = Path.read_bytes + for name in raw: + with self.subTest(path=name): + target = audit.ROOT / name + + def read(path, target=target): + value = original(path) + return value + b"corruption" if path == target else value + + with patch.object(Path, "read_bytes", read): + with self.assertRaisesRegex(ValueError, "source hash"): + audit.source_bytes() + + def test_affine_composition_at_nonidentity_owner(self): + # Independent evaluation of the two reads at one arbitrary owner. + columns = list(audit.E) + columns[0], columns[1] = columns[1], columns[0] + left = audit.intern(columns, 1) + right = audit.intern(audit.E, 2) + owner = tuple(columns) + point = 7 + g, a = audit.MAPS[left] + h, b = audit.MAPS[right] + owner_after_left = tuple(audit.act(owner, v) for v in g) + expected_owner = tuple(audit.act(owner_after_left, v) for v in h) + expected_point = point ^ audit.act(owner, a) ^ audit.act(owner_after_left, b) + composed_g, composed_a = audit.MAPS[audit.compose(left, right)] + self.assertEqual(tuple(audit.act(owner, v) for v in composed_g), expected_owner) + self.assertEqual(point ^ audit.act(owner, composed_a), expected_point) + self.assertNotEqual(a ^ b, composed_a) + + def test_inverse_requires_transported_shift(self): + columns = list(audit.E) + columns[0], columns[1] = columns[1], columns[0] + mapping = audit.intern(columns, 1) + inverse = audit.undo(mapping) + self.assertEqual(audit.MAPS[inverse][1], 2) + wrong = audit.intern(columns, 1) + self.assertNotEqual(audit.compose(mapping, wrong), 0) + + def test_singular_unread_minor_is_rejected(self): + with self.assertRaisesRegex(ValueError, "singular minor"): + audit.inverse([[1, 1], [1, 1]]) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/qq16-cut-operator-audit/verify.py b/research/qq16-cut-operator-audit/verify.py new file mode 100644 index 0000000000..ddd2dbec08 --- /dev/null +++ b/research/qq16-cut-operator-audit/verify.py @@ -0,0 +1,353 @@ +#!/usr/bin/env python3 +"""Independent exact operator audit of PR2443's retained QQ16 cut decoder. + +No predecessor executable is imported. Formal input variables carry exact +affine owner/payload operators; coefficients are rational. Apache-2.0. +By ywz65 with substantial OpenAI Codex assistance. +""" +import argparse +from fractions import Fraction as Q +from functools import lru_cache +import gzip +import hashlib +import io +import json +from pathlib import Path +import tarfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +A = (0, 7, 20, 27, 36, 46, 57, 111) +T = (21, 37, 47, 76, 81, 87, 92, 110) +U = tuple(p for p in range(112) if p not in A + T) +J = (1, 2, 3, 4, 5, 6, 8, 12) +S = tuple(p for p in U if p not in J) +E = tuple(1 << i for i in range(73)) +MEMBERS = { + "slots/local/CANONICAL-WORD.json.gz": "16bc0ebb04b4be6c0ade74badc6a0c0cdba4215eda86e4ff9f13abf8ecebd219", + "slots/local/LOCAL-PROGRAMS.json.gz": "241fde27d4e43f5a9cb6b128f9f76c5131a53d09f0371676163f914d0b0fef3a", + "t16/global/base/work/complex-nine-native/DATA-PHASES.json": "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa", + "t16/global/base/split-centres/GLOBAL-TEMPLATE.json.gz": "a179dad87651aba340a5a8ddbcd86a8e757cad87b8a1f8bad48106fbecd38518", +} + + +def need(ok, why): + if not ok: + raise ValueError(why) + + +def digest(raw): + return hashlib.sha256(raw).hexdigest() + + +def source_bytes(root=ROOT): + pins = json.loads((HERE / "SOURCES.json").read_text(encoding="utf-8")) + result = {} + for item in pins["files"]: + if item["usage"] == "input": + raw = (root / item["path"]).read_bytes() + need(digest(raw) == item["sha256"], "source hash: " + item["path"]) + result[item["path"]] = raw + return result + + +def act(columns, vector): + out = 0 + while vector: + bit = vector & -vector + out ^= columns[bit.bit_length() - 1] + vector ^= bit + return out + + +MAPS = [(E, 0)] +MAP_IDS = {MAPS[0]: 0} + + +def intern(columns, shift=0): + pair = (tuple(columns), shift) + if pair not in MAP_IDS: + MAP_IDS[pair] = len(MAPS) + MAPS.append(pair) + return MAP_IDS[pair] + + +@lru_cache(None) +def compose(left, right): + g, a = MAPS[left] + h, b = MAPS[right] + return intern(tuple(act(g, c) for c in h), a ^ act(g, b)) + + +@lru_cache(None) +def undo(index): + g, a = MAPS[index] + gt = tuple(sum(((g[j] >> i) & 1) << j for j in range(73)) for i in range(73)) + result = intern(gt, act(gt, a)) + need(compose(index, result) == compose(result, index) == 0, "orthogonal affine inverse") + return result + + +def combine(*weighted_rows): + out = {} + for coefficient, row in weighted_rows: + if coefficient: + for key, value in row.items(): + out[key] = out.get(key, Q(0)) + coefficient * value + return {key: value for key, value in out.items() if value} + + +def moved(index, row): + out = {} + for (variable, old), value in row.items(): + key = (variable, compose(index, old)) + out[key] = out.get(key, Q(0)) + value + return {key: value for key, value in out.items() if value} + + +def variable(index): + return {(index, 0): Q(1)} + + +def inverse(matrix): + n = len(matrix) + rows = [[Q(x) for x in row] + [Q(i == j) for j in range(n)] + for i, row in enumerate(matrix)] + for j in range(n): + pivot = next((i for i in range(j, n) if rows[i][j]), None) + need(pivot is not None, "singular minor") + rows[j], rows[pivot] = rows[pivot], rows[j] + scale = rows[j][j] + rows[j] = [v / scale for v in rows[j]] + for i in range(n): + if i != j: + scale = rows[i][j] + rows[i] = [v - scale * w for v, w in zip(rows[i], rows[j])] + return [row[n:] for row in rows] + + +def matmul(a, b): + return [[sum((x * y for x, y in zip(row, col)), Q(0)) for col in zip(*b)] for row in a] + + +def parse_sources(raw): + packet = json.loads(gzip.decompress(raw["research/joint-query/certificate.json.gz"])) + archive_raw = raw["research/community-frontier1042-audit/selected-replay.tar.gz"] + decoded = {} + with tarfile.open(fileobj=io.BytesIO(archive_raw), mode="r:gz") as archive: + for name, pin in MEMBERS.items(): + entries = [m for m in archive.getmembers() if m.name == name] + need(len(entries) == 1 and entries[0].isfile(), "unique archive member") + data = archive.extractfile(entries[0]).read() + need(digest(data) == pin, "member hash: " + name) + decoded[name.rsplit("/", 1)[-1]] = json.loads(gzip.decompress(data) if name.endswith("gz") else data) + word, programs = decoded["CANONICAL-WORD.json.gz"], decoded["LOCAL-PROGRAMS.json.gz"] + need((word["v"], 2 * word["v"] + word["R"]) == (112, 704), "source geometry") + # Reconstruct R directly from the retained scalar prefix; no QQ16 loader. + registers = [variable(i) for i in range(712)] + for event in programs["forward"]: + if event == ["phase", "centers"]: + break + if event[0] != "scalar": + continue + op = event[1] + at = op[1][1] + (704 if op[1][0] == "C" else 0) + if op[0] == "clear": + registers[at] = {} + elif op[0] == "scale": + registers[at] = combine((Q(op[2], op[3]), registers[at])) + else: + src = op[2][1] + (704 if op[2][0] == "C" else 0) + need(op[0] in ("copy", "add"), "known scalar prefix operation") + registers[at] = dict(registers[src]) if op[0] == "copy" else combine( + (1, registers[at]), (Q(op[3], op[4]), registers[src])) + else: + raise ValueError("missing centre boundary") + R = [[registers[c].get((p, 0), Q(0)) for p in range(112)] for c in word["centers"]] + need(R == [[Q(row.get(str(p), 0)) for p in range(112)] for row in packet["R_rows"]], "source-derived R") + need(tuple(packet["A_ports"]) == A and tuple(packet["T_ports"]) == T and tuple(packet["U_ports"]) == U, "partitions") + need(all(Q(packet["K_rows"][p].get(str(i), 0)) == R[i][p] / 4 for p in range(112) for i in range(8)), "source K") + need(decoded["GLOBAL-TEMPLATE.json.gz"]["recipe"][:2] == [ + {"kind": "local", "pair": 0, "reverse": False, "stage": 0}, + {"kind": "local", "pair": 0, "reverse": True, "stage": 1}], "consecutive pair-zero F0 B1") + phases, program = decoded["DATA-PHASES.json"], packet["programs"]["B_1_2"] + routes, native, bindings = {}, {}, [] + for p, recipe in enumerate(phases["recipes"]): + need(recipe["port"] == p, "source port identity") + basis = recipe["idle_children"][0]["orthogonal_axes"][:8] + maps = [e[2] for e in program if e[0] == "cover_map" and e[1] == ["L", 112 + p]] + need(len(maps) == 4, "four Y alignments") + for stage, offset in ((2, 0), (1, 2)): + swaps = [b ^ (1 << (9 + 8 * (stage - 1) + i)) for i, b in enumerate(basis)] + columns = tuple(e ^ act(swaps, sum(((e & s).bit_count() % 2) << i for i, s in enumerate(swaps))) for e in E) + beta = sum((((b.bit_count() - 1) // 2) % 2) << (9 + 8 * (stage - 1) + i) for i, b in enumerate(basis)) + shift = recipe["q"] ^ beta + entry = packet["map_registry"][maps[offset]] + back = packet["map_registry"][maps[offset + 1]] + need(tuple(entry["owner_right_matrix_columns"]) == columns, "route from phase geometry") + need(entry["payload_translation_at_identity_owner"] == shift, "native entry translation") + native[stage, p] = intern(columns, shift) + need(undo(native[stage, p]) == intern(back["owner_right_matrix_columns"], back["payload_translation_at_identity_owner"]), "registered native inverse") + routes[stage, p] = intern(columns) + bindings.append([stage, p, maps[offset], maps[offset + 1]]) + return R, routes, native, bindings + + +class Model: + def __init__(self, R, routes, native): + self.R, self.routes, self.native = R, routes, native + self.minor = [[row[p] for p in J] for row in R] + self.dual = inverse(self.minor) + identity = [[Q(i == j) for j in range(8)] for i in range(8)] + need(matmul(self.minor, self.dual) == matmul(self.dual, self.minor) == identity, "both minor inverse orders") + for ports, scale in ((A, 4), (T, 4), (U, 48)): + block = [[row[p] for p in ports] for row in R] + need(matmul(block, list(zip(*block))) == [[scale * x for x in row] for row in identity], "Gram identity") + + def route(self, stage, port, native=False): + return 0 if stage == 0 else (self.native if native else self.routes)[stage, port] + + def query(self, bank, ports, stage=0, native=False): + routed = {p: moved(self.route(stage, p, native), bank[p]) for p in ports} + return [combine(*[(row[p], routed[p]) for p in ports]) for row in self.R] + + def inject(self, query, ports, stage=0, native=False): + return {p: moved(undo(self.route(stage, p, native)), combine(*[(self.R[i][p] / 4, query[i]) for i in range(8)])) for p in ports} + + def forward(self, x, y): + f = self.query(x, range(112)) + correction = self.inject(f, U + T) + old_t = self.inject(self.query(x, T), A) + xx = {p: combine((1, x[p]), (-1, correction[p])) if p in U else old_t[p] if p in A else correction[p] for p in range(112)} + yy = {p: combine((1, y[p]), (1, xx[p])) if p in U else combine((1, x[p]), (1, y[p]), (-1, xx[p])) for p in range(112)} + return xx, yy + + def forward_inverse(self, xx, yy): + f, old_c = self.query(xx, T), self.query(xx, A) + kf = self.inject(f, U) + x = {p: combine((1, xx[p]), (1, kf[p])) for p in U} + x.update(self.inject(old_c, T)) + ordinary = self.query(x, U) + a = [combine((1, f[i]), (-1, ordinary[i]), (-1, old_c[i])) for i in range(8)] + x.update(self.inject(a, A)) + y = {p: combine((1, yy[p]), (-1, xx[p])) if p in U else combine((1, xx[p]), (1, yy[p]), (-1, x[p])) for p in range(112)} + return x, y + + def observe(self, x, y): + # These x,y are the arbitrary post-F0 state. Only B1's A logger and + # ordinary target subtraction appear in the observation contract. + delta = self.inject(self.query(y, U + T, 2), A, 2) + return ({p: x[p] for p in A + T}, {p: y[p] for p in A + T}, + {p: combine((1, y[p]), (1, delta[p])) for p in A}, + {p: combine((1, x[p]), (-1, y[p])) for p in U}, + {p: x[p] for p in S}) + + def decode_cut(self, observed, fault=None): + xs, ys, ya, c, reads = observed + use_native = fault == "native_alignment_for_logical_chart" + q = self.query({p: combine((1, ya[p]), (0 if fault == "omit_old_A" else -1, ys[p])) for p in A}, A, 2, use_native) + ct = self.query(ys, T, 2, use_native) + cc = self.query(c, U, 2, use_native) + known = self.query(reads, S, 2, use_native) + rhs = [combine((1, q[i]), (0 if fault == "omit_T" else -1, ct[i]), + (-1 if fault == "wrong_C_sign" else 1, cc[i]), (-1, known[i])) for i in range(8)] + if fault == "inverse_before_scalar": + rhs = [moved(undo(self.route(2, p)), row) for p, row in zip(J, rhs)] + solved = [combine(*list(zip(row, rhs))) for row in self.dual] + x = dict(xs) | dict(reads) + for p, row in zip(J, solved): + x[p] = row if fault == "inverse_before_scalar" else moved(undo(self.route(2, p, use_native)), row) + y = dict(ys) | {p: combine((1, x[p]), (-1, c[p])) for p in U} + return x, y + + +def independent_pair(start=0): + return ({p: variable(start + p) for p in range(112)}, {p: variable(start + 112 + p) for p in range(112)}) + + +def free_observations(): + blocks, next_id = [], 0 + for ports in (A + T, A + T, A, U, S): + blocks.append({p: variable(next_id + i) for i, p in enumerate(ports)}) + next_id += len(ports) + need(next_id == 224, "exact cut observation count") + return tuple(blocks) + + +def first_residual(want, actual): + for bank, (a, b) in enumerate(zip(want, actual)): + for p in a: + residual = combine((1, b[p]), (-1, a[p])) + if residual: + (v, index), coefficient = next(iter(sorted(residual.items()))) + g, shift = MAPS[index] + return {"block": bank, "port": p, "input_array": v, + "owner_columns": g, "payload_shift": shift, + "coefficient": str(coefficient), "terms_in_residual_row": len(residual)} + return None + + +def forget_payload(row): + return combine(*[(value, {(v, intern(MAPS[index][0])): Q(1)}) for (v, index), value in row.items()]) + + +def run(): + raw = source_bytes() + R, routes, native, bindings = parse_sources(raw) + model = Model(R, routes, native) + inputs = independent_pair() + need(model.forward_inverse(*model.forward(*inputs)) == inputs, "F0 inverse after forward") + need(model.forward(*model.forward_inverse(*inputs)) == inputs, "F0 forward after inverse") + observed = model.observe(*inputs) + need(model.decode_cut(observed) == inputs, "cut decoder after observation, all input arrays") + free = free_observations() + need(model.observe(*model.decode_cut(free)) == free, "cut observation after decoder, all observation arrays") + controls = {} + for fault in ("omit_old_A", "omit_T", "wrong_C_sign", "inverse_before_scalar", "native_alignment_for_logical_chart"): + changed = model.decode_cut(observed, fault) + witness = first_residual(inputs, changed) + need(witness is not None, "ineffective mutation: " + fault) + controls[fault] = witness + if fault == "native_alignment_for_logical_chart": + # Precisely demonstrate why payload-constant fixtures miss this fault. + need(all(forget_payload(changed[b][p]) == inputs[b][p] for b in range(2) for p in range(112)), "native confusion is invisible only after forgetting translations") + missing = list(observed) + missing[2] = {p: {} for p in A} + controls["discard_B1_A_cut"] = first_residual(inputs, model.decode_cut(tuple(missing))) + need(controls["discard_B1_A_cut"] is not None, "lost cut must fail") + dirty = model.forward_inverse(*model.decode_cut(observed)) + changed_dirty = (dirty[0], {p: {} if p in U else dirty[1][p] for p in range(112)}) + controls["discard_initial_Y_dirt"] = first_residual(dirty, changed_dirty) + need(controls["discard_initial_Y_dirt"] is not None, "arbitrary Y dirt control") + return { + "status": "PASS_QQ16_CUT_OPERATOR_AUDIT", + "source_sha256": {name: digest(data) for name, data in raw.items()}, + "archive_members": MEMBERS, "route_bindings": bindings, + "selected_ordinary_partition": {"A": A, "T": T, "U": U, "unread": J, "read": S}, + "R_J": model.minor, "R_J_inverse": model.dual, + "formal_input_arrays": 224, "formal_observation_arrays": 224, + "identities": ["F0_inverse F0 = I", "F0 F0_inverse = I", "cut_decode cut_observe = I", "cut_observe cut_decode = I"], + "logical_charts_have_zero_payload_shift": True, + "native_substitution_passes_payload_constant_projection": True, + "negative_controls": controls, + "scope": "Exact ordered QQ16 retained two-cut algebra on arbitrary owner/payload arrays; native execution and final controller availability are not checked", + } + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write-result", action="store_true", help="create new receipt; refuses overwrite") + args = parser.parse_args() + result = run() + encoded = json.dumps(result, sort_keys=True, indent=2, default=str) + "\n" + result_path = HERE / "RESULT.json" + if args.write_result: + with result_path.open("x", encoding="utf-8", newline="\n") as out: + out.write(encoded) + else: + need(result_path.read_text(encoding="utf-8") == encoded, "committed result differs or missing") + print(result["status"], "arrays=224 inverse_identities=4 registered_routes=224 controls=7 no_new_kappa") + + +if __name__ == "__main__": + main()