diff --git a/research/p104-prefix-tail-independent-audit/CERTIFICATE-ORIGIN.json b/research/p104-prefix-tail-independent-audit/CERTIFICATE-ORIGIN.json new file mode 100644 index 0000000000..6007076d0d --- /dev/null +++ b/research/p104-prefix-tail-independent-audit/CERTIFICATE-ORIGIN.json @@ -0,0 +1,8 @@ +{ + "pr": "https://github.com/CrocSwap/integer-mult-bounds/pull/2358", + "head": "e8950db523c9682518049a42cfc28642224292ff", + "path": "research/p104-prefix-tail/WITNESS.json", + "sha256": "8abbe9564e19ac966bf97480d7c00891289f9b1d6be13cfa9a2d604b97bc0a5c", + "license": "Apache-2.0", + "credit": "AAAmirinu with substantial OpenAI Codex assistance; cut2646 witness inherited from PR2345 at2a5fa34a967e7567abf01611f92a6ab69e8c901a" +} diff --git a/research/p104-prefix-tail-independent-audit/PROOF.md b/research/p104-prefix-tail-independent-audit/PROOF.md new file mode 100644 index 0000000000..f831a35537 --- /dev/null +++ b/research/p104-prefix-tail-independent-audit/PROOF.md @@ -0,0 +1,268 @@ +# Independent mathematical audit of the PR2358 rank certificates + +Run: `trial-20261015-0634`. Scope: the rational pooled-snapshot model stated +in PR2358 at `e8950db523c9682518049a42cfc28642224292ff`, with its README, certificate and source inspected. This is an AI-assisted independent written +mathematical audit, not human review or a formal-kernel proof. No source +trace replay is claimed in this note; that independent finite obligation +belongs to the parent trial. No code outside this note was changed. + +**Finding:** the stated reduction and the two determinant arguments are +correct under the stated trace premises. The explicit cut-2754 residual +has rank exactly two. I found no algebraic counterexample to the stated +rational theorem. Availability and complete pool coverage remain finite +source-bound obligations, rather than consequences of these identities. + +## Model and necessary projection hypotheses + +Work over Q. Let V=X direct-sum Z, with X=Q^104 the source coordinates +and Z=Q^176 the independent initial target/helper nuisance coordinates. +For target t, let z_t denote its own target dirt coordinate. The trace +premises needed for the projection are: + +1. Every eligible donor has zero z_t coefficient. +2. All 175 coordinate units in Z other than z_t lie in S_t(0), hence + in the monotone pooled space S_t(c). +3. Every source projection of an eligible donor lies in row(R), where + R is the stated 8-by-104 rational matrix satisfying RR^T=104 I_8. +4. Correction rows C_t lie in X, with C=I_104-R^T R/8. + +These hypotheses use all independent dirty columns, not clean-input +specialization. For any s in S_t(c), its nuisance component belongs to +span{z_j:j != t}, which is contained in S_t(c). Subtracting that component +proves pi_X(s) in S_t(c) intersect X. The reverse containment follows by +projection, so pi_X(S_t)=S_t intersect X. + +If C_t=s_t+h_t with h_t in a shared space H, projection gives +C_t=pi_X(s_t)+pi_X(h_t). Therefore pi_X(H) serves the same rows, lies in X, +and has dimension at most dim H. Conversely source-only H is allowed in +the original optimization. Thus optimization over all 280 coordinates is +exactly optimization over source-only shared spaces. This explicitly covers +arbitrary nuisance components in the original H. + +The implementation's initial-state construction gives independent nuisance +unit rows. Its initial-frame checks put all 176 nuisance registers together +in the zero frame and all source registers in rank-one frames; hence for +each Y_t the other 175 nuisance units are eligible at cut zero. Its donor +checks test absence of the target's own dirt. These are the right checks; +the parent's independent replay must establish them on the actual pins. + +## Minimum-rank reduction, including signs and factors + +Put L_t={a in Q^8 : aR in S_t intersect X}. Since RR^T=104 I_8, +the coefficient a of any projected row v=aR is unique and equals +v R^T/104. This agrees with the WITNESS contact convention. + +For any choices a_t in L_t, form A with rows a_t. The rows of +K=C+12 AR serve C because K_t-C_t belongs to S_t. Conversely, for any +serving source-only H choose C_t=s_t+h_t; write s_t=b_t R, and choose +a_t=-b_t/12. Then K_t=h_t. Taking row spans in both directions proves + + h(c) = min_{a_t in L_t(c)} rank(C+12 AR). + +The factor -1/12 is legitimate because L_t is a rational linear space. +There is no clean-state, positivity, integrality or bounded-coefficient +restriction in this model. If one added such restrictions, this step would +require a different argument. + +Set D=R^T/8-12 A. Then K=I_104-DR and + + RD=13 I_8-12 RA, + I_8-RD=-12(I_8-RA). + +For any rectangular D,R, the maps R and D restrict to inverse linear maps +between ker(I_104-DR) and ker(I_8-RD): if DRx=x then RD(Rx)=Rx and +D(Rx)=x; the reverse direction is identical. Hence + + rank K = 104-nullity(I_8-RD) + = 96+rank(I_8-RD) + = 96+rank(I_8-RA). + +Writing r_t for column t of R, RA=sum_t r_t a_t. Independent choices of +the rows a_t imply that the set of attainable RA is exactly +E(c)=sum_t r_t L_t(c), also described as the span of all pool generators. +Thus the stated minimum-rank formula follows for every rational A, not +merely the two supplied witnesses. The optimization minimum exists: the +attainable set is nonempty and ranks take finitely many integer values. + +## Universal compression lower bounds + +Use the vectors p,q,w,a,b,k stated in the README. For a generator +M=r_t alpha, each functional factors exactly as + + left^T M right = (left^T r_t)(alpha right). + +Consequently checking its vanishing on every generator proves vanishing +on all of E(c), including arbitrary rational linear combinations. + +For N=I-M, the three persistent equalities give the compression + + [p^T; q^T] N [a b] = [[0,-1],[-1,s]], + +whose determinant is -1 for every rational s. Multiplication by the two +compression matrices cannot increase rank. Therefore rank N >= 2. + +At cut 2753 the three additional k equalities imply + + [p^T; q^T; w^T] N [a b k] + = [[0,-1,0],[-1,s,0],[u,v,2]], + +whose determinant is -2 for all rational s,u,v. Thus rank N >= 3. +There is no requirement that either compression matrix be square or +invertible; the exhibited nonsingular compressed minor suffices. + +Because pools are monotone, the second bound holds at every earlier cut, +and the persistent bound holds through 2823. With the cut-2646 rank-99 +witness available thereafter and the cut-2754 rank-98 witness available +thereafter, these imply 99 on [2646,2753] and 98 on [2754,2823], conditional +on those witnesses' exact membership and rank. The advertised [2718,2753] +is a weaker subinterval. In particular no earlier cut can have h<=98. + +## Explicit new residual and sharpness of the third constraint + +Let x=-e2+e3+e7 and alpha=e1+2e7. The displayed matrix + + N=x alpha^T-e1 e2^T + +is a sum of two rank-one matrices, so rank N<=2. Direct multiplication +with the stated vectors gives + + [p^T; q^T; w^T] N [a b k] + = [[0,-1,0],[-1,0,-2],[1,0,2]]. + +Its upper-left 2-by-2 determinant is -1, so rank N=2; its full determinant +is zero. In particular q^T N k=-2 and q^T M k=2, while p^T N k=0 and +w^T N k=2. The cut-2753 third-column condition cannot extend to this N. + +The README expression, the code's outer-product expression (using -e1 as +the second left vector), and this calculation have identical signs and +index conventions. The 46 contact terms must still independently sum to +this expression on the pinned original trace; this note does not infer +that membership from the expression alone. + +## Independent arithmetic checks and useful defect controls + +A standalone Python calculation using only fractions.Fraction and explicit +8-vectors, with no imports from the source package, recomputed the displayed +3-by-3 compression exactly and its determinants (-1 for the leading minor, +0 for the whole new compression). The general determinant formulas above +are written algebraic proofs; checking several rational free entries was +only an arithmetic sanity check, not their quantified justification. + +The following are exact premise-sensitive controls: + +* Delete the fixed zero in the 2-by-2 compression: N=(e1+e2-e7)(-e0)^T + has compression [[-1,-1],[-1,-1]] and rank one. The two fixed off-diagonal + entries alone do not certify rank two. +* Delete the q^T N k=0 premise in the 3-by-3 argument: the actual new N above + satisfies every other displayed fixed entry but has rank two. +* Delete the fixed nonzero third diagonal entry: N=x e1^T-e1 e2^T has + compression [[0,-1,0],[-1,0,0],[1,0,0]] and rank two. +* Delete nuisance-unit availability or allow own-target dirt in donors: + already with X=Qx, Z=Qz, S=span(x+z), one has pi_X(S)=Qx but + S intersect X=0. For C=x, projected local availability would incorrectly + predict h=0, whereas the original space needs h>=1. This proves why + projection cannot be assumed solely from source-row containment. + +## Exact scope and unresolved implications + +The algebra above is an all-rational written proof under explicitly listed +premises. It is not a formal-kernel proof. The finite source obligations are: +the exact root ordering and tight-frame identity, every eligible snapshot's +source-row membership and own-target-dirt absence, all pool generators for +the two lower endpoints, and all fixed witness contacts and their residual +sum. Source inspection shows checks for these obligations, but inspection +does not replace the parent's independent source-bound replay. + +There is no precision or coefficient-height admission claim here. Rational +pooling allows free basis changes and access across different times. It does +not establish chronological execution, source-read charges, preservation of +later snapshots after insertions, creation/restoration of complement rows, +ownership or hosting, transport costs, an all-size supplier, or a new kappa. + +Although arbitrary rational minimum-rank problems need not have the same +minimum over larger fields, these particular intervals would also have the +same values over any characteristic-zero field extension, if the model is +defined by scalar extension of these same rational pools: the compression +lower bounds still apply and the attaining rational witnesses remain valid. +This observation is conditional on the same finite trace premises; no +positive-characteristic or changed-construction claim is made. + +## Addendum: independent review of the parent's audit implementation + +Reviewed +`trial-20261015-0634/research/p104-prefix-tail-independent-audit/verify.py` +after the parent reported a passing pinned full replay (4,059 cuts, 280 +columns, 110,814 target/snapshot pairs, pools 324/427, upper ranks 99/98). +This addendum reviews mathematical coverage of that implementation; the +reported full rank/certificate execution belongs to the parent. I separately +executed its trace replay to check the contact coefficient types below. +**No mathematical blocker found for its fixed pinned inputs and certificate.** + +* `rank()` is a correct exact forward row-echelon algorithm. Each stored + row has zero entries strictly before its stored pivot. The existing rows + are used in increasing pivot order, so eliminating a pivot never + reintroduces an earlier pivot. The new row is zero at every existing + pivot, hence its first nonzero coordinate, if any, is a new pivot. This + remains true when pivots are inserted out of order. Normalization and + backward elimination are unnecessary for counting rank. All actual + caller matrices have fixed rectangular widths (8 or 104), so the lack of + a generic ragged-input guard does not affect this pinned computation. +* `frame()` first constructs a binary echelon basis with distinct highest + bits. Its ascending pivot cleanup removes each lower pivot from every + higher pivot row. Lower rows have already been cleaned at that point, + so this gives the unique reduced basis of the binary subspace, returned + in descending pivot order. `inside()` then correctly reduces against + that descending basis. Exact frame equality is therefore equality of + binary subspaces, not equality of an arbitrary presentation. +* Every event checks scalar donors against the destination and the event's + declared binary frame. Source-code membership is a separate condition + checked in `projection()`; the implementation does not confuse scalar + common-frame eligibility with membership of a source row in row(R). +* `inspect()` rebuilds current frame groups at every cut and visits every + eligible donor before considering `(target,row_id)` reuse. A row ID + represents the complete immutable rational row, including all nuisance + columns. Own-target-dirt absence and source projection depend only on + that row, so reusing an already inspected pair cannot skip a changed + mathematical value. A changed frame can affect present eligibility, + but cannot create a new pooled row when the same target/full-row pair + was already eligible at an earlier cut. This use of reuse is exact. +* All initial nuisance rows are independent units in the common empty + frame, so nuisance lifting is justified. Every requested contact's + exact-cut eligibility is checked separately. It was also visited by + that cut's generic inspection, which either checks its own-target dirt + directly or reuses the same previously checked full row. Thus the + contact-specific path need not duplicate the dirt assertion. +* Root reconstruction and the exact tight-frame identity fix the source + coefficient map. The upper witness forms A from the replayed contacts, + checks both small and full ranks, and checks the exact displayed new + residual. The lower routine tests the required generator functionals + and constant compression entries. The SHA256 certificate pin fixes + the intended cuts, target indices, vector lengths and witness entries; + this code is a fixed-evidence auditor, not a general certificate-schema + validator. Source-file hash verification supplies its other fixed inputs. + +Independent small arithmetic controls were executed against the parent's +`frame`, `inside`, and `rank` routines, with reference results constructed +without those routines: 2,746 ordered independent binary frame fixtures in +four bits, all 66 subspaces of dimension at most three and all their +containment pairs, dependent fixtures rejected, and all 729 two-by-three +matrices over {-1,0,1} ranked by an independent exact-minor criterion in +both row orders. All passed. These controls supplement the written +all-dimension echelon arguments; they do not exhaust nine-bit frames or +104-dimensional matrix ranks. + +One harmless arithmetic detail: a row having no source entries yields +floating zero coefficients through Python's `0/104`; any row with a +source entry yields Fractions in every coordinate. These floating values +are exactly zero, fail `any(alpha)`, and cannot enter a nonzero projected +pool. I independently executed the parent trace replay and checked that +all 49 distinct fixed upper contacts have nonzero source projections and +every coordinate is a Fraction; hence the fixed upper calculation cannot +encounter these floating zero tuples. Their arithmetic cannot introduce +rounding error into this result. For a changed certificate, a zero-projected +contact following a nonzero contribution to the same target could coerce a +nonzero Fraction sum to float, so generic acceptance would require attention. +Using `Q(0)` as the sum initializer enforces a uniform exact representation, +but is not a correctness gate for these fixed pinned contacts. + +Parent repair after review: the projection sum now starts with Fraction(0), so source-empty rows also retain exact Fraction coordinates. The final registered replay and controls were rerun after this repair. diff --git a/research/p104-prefix-tail-independent-audit/README.md b/research/p104-prefix-tail-independent-audit/README.md new file mode 100644 index 0000000000..cc74b23cce --- /dev/null +++ b/research/p104-prefix-tail-independent-audit/README.md @@ -0,0 +1,101 @@ +# Independent audit of the P104 tail-prefix certificate + +A separate exact interpreter corroborates [AAAmirinu's PR2358](https://github.com/CrocSwap/integer-mult-bounds/pull/2358), +head `e8950db523c9682518049a42cfc28642224292ff`, in its **rational pooled-snapshot model**. +The shared correction dimension is 99 on cuts 2718–2753 and 98 on cuts 2754–2823; +2754 is the earliest cut attaining 98. These are the predecessor's results, +not new minima. The contribution is separately implemented finite evidence and +an independent written check of the rank reduction and its required premises. + +The interpreter imports no predecessor Python code. It uses Fraction-valued +sparse rows, canonical binary row elimination and an every-cut scan, instead +of the predecessor's integer/8 rows, enumerated binary subspaces and changed-group +collector. The parent inspected predecessor mathematics/interfaces/code before +implementation: this is a separate implementation, not a blind audit. The +specialist independently checked the written algebra and then reviewed the new +interpreter. Neither is independent human review or a formal proof assistant. + +## Evidence and scope + +The replay reconstructs the punctured E8 root ordering and `RR^T=104I`, carries +all 280 independent target/source/dirty columns through all 4,058 original +events and 4,059 cuts, checks scalar common frames, nested paid transports, +private-copy lifetimes, all endpoints and the unchanged local profile. +It scans every cut's matching donor/target frames. Full-row interning removes +only duplicate algebra, and recovers exactly 110,814 distinct target/snapshot +pairs and 324/427 nonzero target/coefficient pairs through cuts 2753/2823. + +Every eligible donor has zero own-target dirt and source part in row(R). +The other 175 nuisance units are available at cut zero. These premises justify +projecting arbitrary serving spaces in all 280 columns into source space. +The proof then gives + +``` +h(c) = min rank(C+12AR) = 96 + min rank(I8-RA), +C = I104 - R^T R/8, A_t in L_t(c). +``` + +All generators satisfy the six/three required annihilator functionals. +The compressed residual determinants are fixed at −2/−1, proving the universal +rational lower bounds. All 18/46 upper contacts are replayed at their exact +cuts; direct rational ranks of the 104-by-104 corrections are 99/98. The small +residual ranks are 3/2; the cut-2754 residual also matches its explicit two-term +factorization. Monotonicity joins these lower and upper certificates. +[PROOF.md](PROOF.md) spells out the rank-nullity derivation and projection premises. +[RESULT.json](RESULT.json) is the exact finite receipt. + +There is **no chronological correction, paid transport-cost bound, global owner +map/moment, native Gaussian regeneration, recursive precision/all-size proof, +selected cold replay, admitted supplier or new kappa**. Pooling combines original +snapshots at different times and grants nuisance subtraction for free. Inserting +contacts into an actual circuit need not preserve those later snapshots. +The evidence is finite exhaustive trace replay plus a written all-rational +conditional argument, not a formal-kernel proof of multiplication. + +## Reproduce + +Python 3.12 standard library, no network for direct replay: + +```sh +python3.12 -I -O -B research/p104-prefix-tail-independent-audit/verify.py +python3.12 -I -O -B research/p104-prefix-tail-independent-audit/test_verify.py +python3.12 scripts/research_package.py --package research/p104-prefix-tail-independent-audit +``` + +The verifier checks immutable inputs and the byte-identical predecessor +certificate. `--out NEW.json` refuses an occupied path. Eight control groups +cover equivalent frame bases/contact order, wrong coefficient, future/self +contacts, nonzero compensation/cleanup faults, illegal scalar/private frames, +a forbidden lower generator, and explicit low-rank matrices when compression +premises are dropped. All mathematical guards remain enabled with `-O`. +The registered hook includes the tests and exact source pins. Local CPython +3.12 optimized registered replay passed all eight groups after the zero-row +Fraction hardening; a Git-free CPython 3.14 optimized export passed unchanged, +and source-pin/occupied-output controls rejected. Selected-record integrity +passed; hosted CI remains separate. + +## Open next questions + +Realize and fully price one complement under actual lifetimes, including source +reads, creation/restoration, frames and chronological owners. Begin from the +separately claimed 41-contact lift rather than duplicating it. This is blocked +by the difference between pooled access and executable access; even a valid +local lift does not supply the missing shared complement or a full moment. +[TASK.json](TASK.json) records the concrete next step and limits. + +## Attribution + +The copied certificate's exact origin, hash and Apache-2.0 attribution are in +[CERTIFICATE-ORIGIN.json](CERTIFICATE-ORIGIN.json). AAAmirinu/#2358 supplies the +six/three annihilator certificates and 46-contact witness; AAAmirinu/#2345 +supplies the reduction and 18-contact rank-99 witness. Gonzalo Mier/#2173 +supplies the pooled model, Gareth Davidson/#2251 the full-pool complement, +and @josecarlosgonzalezroque-design the late-prefix handoff. Rohan Arun/#1972 +supplies the frozen scalar/frame channel; Chafik Boukhalfa/#1991 its native +package; Adam Gall/#1940 the schedule; Josie Elliston/#1071 the fixture, with +Ali Romman/#1125 and the retained PR968/717/446/595/620 lineage. + +Prepared for Ross with substantial OpenAI Codex assistance in proof, code, +controls and writing. Independent exact-circuit specialist proof/code review +is AI-assisted. Apache-2.0. Existing source files/notices and selected records +are unchanged. The manual trial tests the saved prompt's lifecycle, not the scheduler. diff --git a/research/p104-prefix-tail-independent-audit/RESULT.json b/research/p104-prefix-tail-independent-audit/RESULT.json new file mode 100644 index 0000000000..0860001148 --- /dev/null +++ b/research/p104-prefix-tail-independent-audit/RESULT.json @@ -0,0 +1,23 @@ +{ + "status": "PASS_INDEPENDENT_P104_TAIL_AUDIT", + "cuts": 4059, + "columns": 280, + "target_snapshots": 110814, + "pool_pairs": [ + 324, + 427 + ], + "uppers": [ + [ + 2646, + 3, + 99 + ], + [ + 2754, + 2, + 98 + ] + ], + "scope": "Rational pooled availability only; no chronological or paid-cost claim" +} diff --git a/research/p104-prefix-tail-independent-audit/SOURCES.json b/research/p104-prefix-tail-independent-audit/SOURCES.json new file mode 100644 index 0000000000..3bb2451581 --- /dev/null +++ b/research/p104-prefix-tail-independent-audit/SOURCES.json @@ -0,0 +1,30 @@ +{ + "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/p104-native-channel/inputs/LOWRANK-WITNESS.json", + "usage": "input", + "git_blob": "86beaf424e9f0f800ae3a62797d94ec9386b7706", + "sha256": "0f541bef7f19fdeffd67157684e9f03d785f42c89973632f508fc1a0452b580e" + }, + { + "path": "research/p104-native-channel/inputs/P104-FIXTURE.json", + "usage": "input", + "git_blob": "2e16f99b295bb386fd13bd8fbd57b42ef54143a9", + "sha256": "516c06f6ec3cb84be588c546108de897650288576dd5fbf5fe44b9c5546ad8a4" + } + ] +} diff --git a/research/p104-prefix-tail-independent-audit/TASK.json b/research/p104-prefix-tail-independent-audit/TASK.json new file mode 100644 index 0000000000..f75b4d4b4a --- /dev/null +++ b/research/p104-prefix-tail-independent-audit/TASK.json @@ -0,0 +1,117 @@ +{ + "schema_version": 1, + "task_id": "p104-side-correction", + "priority_revision": 4, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "original_card": { + "id": "p104-side-correction", + "question": "Can the native P104 low-rank channel be completed with a legal, fully charged I-G/2 side correction?", + "starting_points": [ + "research/p104-native-channel/README.md", + "research/p104-native-channel/PROOF.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Construct one side-correction word at an explicit chronological cut with the needed frames still available.", + "Derive a lower bound on the side correction and hosting costs that decides whether this channel can beat the selected budget." + ], + "acceptance_gate": "An exact arbitrary-input identity, source/target frame availability and restoration at the chosen cut, plus the complete channel+correction+idle/hosting bill or an explicit favorable bound. The native channel alone is not a supplier.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the P104 open next questions and its fixed local histogram; inspect why appending I-G/2 after source completion is not justified. #1991 supplies the checked native channel, not the missing correction.", + "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": "Choose one exact side-correction cut and bound its allowed cost from a favorable completed moment at a declared target. Stop or hand off if the necessary source/target access cannot be justified or even the optimistic total misses the target.", + "bottleneck_link": "Completing an already realized changed channel tests a concrete construction opportunity, instead of refining the incumbent packing. A positive local result still needs global and all-size admission.", + "allowed_variations": [ + "One correction factorization, one chronological cut, or one explicit hosting obstruction.", + "A changed correction schedule with an updated full bill and native frame contract." + ], + "scope_change_triggers": [ + "Recompiling the already certified low-rank channel without closing a new obligation.", + "Treating a pending ancestor, local histogram or unpriced side correction as an admitted global supplier." + ], + "overlap_terms": [ + "P104", + "I-G/2", + "side correction", + "native channel", + "1972", + "1991" + ] + }, + "scope_status": "changed", + "actual_scope": "Independent exact audit of PR2358 rational pooled prefix lower certificates and contact witnesses, not a chronological correction construction", + "scope_change_reason": "Fresh live overlap shows completed PR2358 and an active chronological lift. Audit the published implication with a different exact interpreter instead of duplicating either task.", + "bottleneck_link": "Availability dimension is an input to correction design, but cannot be treated as paid transport price. This audit establishes a prerequisite only.", + "budget_minutes": 60, + "stop_rule": "One fixed certificate and original4058-event trace; stop after exact audit and controls or publish a specific defect. No second search round.", + "outcome": "completed", + "evidence": "verify.py, test_verify.py, RESULT.json and PROOF.md", + "author": "Ross, with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance in parent implementation/writing and separate exact-circuit specialist proof/code review; no independent human or formal-kernel review", + "open_questions": [ + { + "question": "Can the complement be acquired and used chronologically with a favorable complete cost?", + "why_it_matters": "Pooled dimension alone gives no supplier or saving.", + "first_step": "Use the separately active chronological-lift result, then price complement creation, dirty restoration and actual owners.", + "blocked_by": "Snapshots may occur at different cuts, and insertions can change later values; physical transport, native wrappers, precision/all-size obligations remain." + } + ], + "selection_seed": "5408892b1482ac15ba39f518eba3d34b", + "run_id": "trial-20261015-0634", + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2245#discussioncomment-18942680", + "audited_pr": { + "number": 2358, + "head": "e8950db523c9682518049a42cfc28642224292ff" + }, + "upstream_freshness": { + "checked_at_utc": "2026-10-15T06:40:31.543499+00:00", + "canonical_url": "https://github.com/CrocSwap/integer-mult-bounds.git", + "repository": "/Users/ross/git/math/integer-mult-bounds", + "upstream_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "primary_head": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "priority_revision": 4, + "guidance_sha256": { + "AGENTS.md": "5378ffbf3a119fcd0c23bcce20f34e5dd2fa792a00a0033e47667aeba72bbc37", + "autoresearch.md": "79d0c8be61d90dd6c46b6e7250e0c88713d29854128d8d1361b6343682dad1d8", + "CONTRIBUTING.md": "df5b5646602f42cb5da5844f04ac925182ddcd0f627b9de1c96a5095bb7a277a", + "docs/research/agent-task-catalog.json": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7", + "certificates/selected-result.json": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + } + }, + "overlap_entry": { + "coverage": { + "open_prs": 572, + "discussion_records": 1086 + }, + "complete_pagination": true, + "warnings": [], + "pr_fetched_at": "2026-10-15T06:34:16.432990+00:00", + "discussions_fetched_at": "2026-10-15T06:37:02.457371+00:00", + "limitations": "All open PR bodies incl drafts, Discussion bodies/comments/replies, local package README/TASK and PR ledger; not every code diff or nested source; no novelty guarantee." + }, + "overlap_final": { + "searched_at": "2026-10-15T06:43:33.228516+00:00", + "coverage": { + "open_prs": { + "fetched_at": "2026-10-15T06:40:39.762700+00:00", + "complete_pagination": true, + "records": 573 + }, + "discussions": { + "fetched_at": "2026-10-15T06:43:33.135110+00:00", + "complete_pagination": true, + "records": 1088 + } + }, + "warnings": [], + "limits": "Remote PR scope is open PRs including drafts. Closed work is searched through local READMEs, TASK metadata and ledger only. No code diffs or arbitrary package files are searched. Recheck relevant heads before submission.", + "interpretation": "Matching tail-prefix evidence is PR2358 and its canonical discussion; this is explicitly independent verification, not novelty. Source head freshly read unchanged." + } +} diff --git a/research/p104-prefix-tail-independent-audit/VERIFY.json b/research/p104-prefix-tail-independent-audit/VERIFY.json new file mode 100644 index 0000000000..713d1c0c72 --- /dev/null +++ b/research/p104-prefix-tail-independent-audit/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p104-native-channel/inputs/LOWRANK-WITNESS.json", + "research/p104-native-channel/inputs/P104-FIXTURE.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Every cut, arbitrary-input endpoint, frame/private lifetime, full pool generator census, contact witnesses and exact rational ranks" + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 300, + "checks": "Equivalent bases/contact order; wrong weights/future/self contacts, nonzero dirty compensation/cleanup, private lifetime/scalar-frame faults and omitted-compression-premise controls" + } + ] +} diff --git a/research/p104-prefix-tail-independent-audit/WITNESS.json b/research/p104-prefix-tail-independent-audit/WITNESS.json new file mode 100644 index 0000000000..6f948ed2dd --- /dev/null +++ b/research/p104-prefix-tail-independent-audit/WITNESS.json @@ -0,0 +1,465 @@ +{ + "schema": "p104-prefix-tail/1", + "upper_witnesses": [ + { + "cut": 2646, + "terms": [ + [ + 7, + 2526, + "D5", + "-1/2" + ], + [ + 8, + 2528, + "Y7", + "2" + ], + [ + 10, + 2530, + "Y7", + "2" + ], + [ + 15, + 2534, + "Y7", + "2" + ], + [ + 14, + 2552, + "D8", + "-1/2" + ], + [ + 66, + 2554, + "Y14", + "-2" + ], + [ + 70, + 2560, + "Y14", + "2" + ], + [ + 0, + 2572, + "D12", + "-3/4" + ], + [ + 2, + 2574, + "Y0", + "-2" + ], + [ + 6, + 2576, + "Y0", + "1" + ], + [ + 11, + 2578, + "Y0", + "1" + ], + [ + 19, + 2582, + "Y0", + "1" + ], + [ + 5, + 2606, + "Y3", + "2" + ], + [ + 24, + 2608, + "Y3", + "2" + ], + [ + 32, + 2616, + "Y3", + "2" + ], + [ + 43, + 2618, + "Y3", + "2" + ], + [ + 22, + 2638, + "D20", + "-1/2" + ], + [ + 31, + 2646, + "Y22", + "2" + ] + ], + "minimum": 99, + "origin": "PR2345 commit2a5fa34a967e7567abf01611f92a6ab69e8c901a" + }, + { + "cut": 2754, + "terms": [ + [ + 7, + 2526, + "D5", + "1/4" + ], + [ + 13, + 2532, + "Y7", + "1" + ], + [ + 15, + 2534, + "Y7", + "1" + ], + [ + 33, + 2542, + "Y7", + "-2" + ], + [ + 66, + 2554, + "Y14", + "-4" + ], + [ + 68, + 2556, + "Y14", + "-2" + ], + [ + 70, + 2560, + "Y14", + "2" + ], + [ + 72, + 2562, + "Y14", + "2" + ], + [ + 0, + 2572, + "D12", + "-1/4" + ], + [ + 2, + 2574, + "Y0", + "-4" + ], + [ + 6, + 2576, + "Y0", + "3" + ], + [ + 11, + 2578, + "Y0", + "-4" + ], + [ + 12, + 2580, + "Y0", + "1" + ], + [ + 19, + 2582, + "Y0", + "3" + ], + [ + 36, + 2586, + "Y0", + "-3" + ], + [ + 63, + 2592, + "Y0", + "1" + ], + [ + 3, + 2604, + "D16", + "3/4" + ], + [ + 5, + 2606, + "Y3", + "-1" + ], + [ + 24, + 2608, + "Y3", + "2" + ], + [ + 25, + 2610, + "Y3", + "-1" + ], + [ + 32, + 2616, + "Y3", + "2" + ], + [ + 43, + 2618, + "Y3", + "-1" + ], + [ + 50, + 2620, + "Y3", + "3" + ], + [ + 22, + 2638, + "D20", + "1/4" + ], + [ + 23, + 2640, + "Y22", + "2" + ], + [ + 28, + 2642, + "Y22", + "2" + ], + [ + 29, + 2644, + "Y22", + "-2" + ], + [ + 31, + 2646, + "Y22", + "-1" + ], + [ + 41, + 2648, + "Y22", + "-4" + ], + [ + 1, + 2672, + "D23", + "1/2" + ], + [ + 4, + 2674, + "Y1", + "2" + ], + [ + 9, + 2676, + "Y1", + "-2" + ], + [ + 17, + 2678, + "Y1", + "4" + ], + [ + 26, + 2680, + "Y1", + "-2" + ], + [ + 45, + 2684, + "Y1", + "-2" + ], + [ + 59, + 2698, + "Y1", + "-2" + ], + [ + 80, + 2718, + "D27", + "1/4" + ], + [ + 81, + 2720, + "Y80", + "1" + ], + [ + 82, + 2722, + "Y80", + "1" + ], + [ + 85, + 2724, + "Y80", + "1" + ], + [ + 14, + 2735, + "D5", + "1/4" + ], + [ + 66, + 2737, + "Y14", + "2" + ], + [ + 0, + 2746, + "D0", + "-1/2" + ], + [ + 2, + 2748, + "Y0", + "2" + ], + [ + 11, + 2752, + "Y0", + "4" + ], + [ + 19, + 2754, + "Y0", + "-4" + ] + ], + "minimum": 98, + "origin": "New explicit rank-two residual" + } + ], + "lower_vectors": { + "p": [ + -1, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "q": [ + -1, + 0, + 1, + 0, + 0, + 0, + 0, + 0 + ], + "w": [ + 0, + 0, + 1, + 1, + 1, + 1, + -1, + 1 + ], + "a": [ + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "b": [ + 1, + 0, + 1, + 0, + 0, + 0, + 0, + 0 + ], + "k": [ + 0, + 0, + 0, + 0, + 0, + 0, + -1, + 1 + ] + } +} diff --git a/research/p104-prefix-tail-independent-audit/test_verify.py b/research/p104-prefix-tail-independent-audit/test_verify.py new file mode 100644 index 0000000000..4de5a4ed35 --- /dev/null +++ b/research/p104-prefix-tail-independent-audit/test_verify.py @@ -0,0 +1,105 @@ +"""Defect-sensitive controls for the independent audit; standard library only.""" +from copy import deepcopy +from fractions import Fraction as Q +from importlib.util import module_from_spec, spec_from_file_location +from pathlib import Path +import json +import unittest + +HERE = Path(__file__).resolve().parent +spec = spec_from_file_location('independent_audit', HERE/'verify.py') +v = module_from_spec(spec) +spec.loader.exec_module(v) + + +class AuditControls(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.raw = v.inputs() + cls.word = cls.raw['LOWRANK-WITNESS.json'] + cls.cert = json.loads((HERE/'WITNESS.json').read_text()) + cls.ports = v.roots(cls.raw['P104-FIXTURE.json']['section4_explicit_P104']) + cls.collected = v.replay(cls.word,cls.ports,cls.cert) + + def test_equivalent_frame_presentations(self): + self.assertEqual(v.replay(self.word,self.ports,self.cert,reverse_basis=True),self.collected) + # Same two-space via a shear, not merely a basis permutation. + self.assertEqual(v.frame((1,2)),v.frame((3,2))) + with self.assertRaisesRegex(ValueError,'dependent frame'): + v.frame((1,2,3)) + + def test_wrong_contact_coefficient(self): + bad = deepcopy(self.cert['upper_witnesses'][1]) + bad['terms'][-1][-1] = '-3' + with self.assertRaisesRegex(ValueError,'upper rank|explicit residual'): + v.upper(bad,self.collected[1],self.ports) + # Reordering and cancelling two presentation-only terms remain legal. + good = deepcopy(self.cert['upper_witnesses'][1]) + good['terms'].reverse() + self.assertEqual(v.upper(good,self.collected[1],self.ports),[2754,2,98]) + + def test_future_and_self_contact(self): + bad = deepcopy(self.cert['upper_witnesses'][1]) + bad['cut'] = 2753 + with self.assertRaisesRegex(ValueError,'future contact'): + v.upper(bad,self.collected[1],self.ports) + bad = deepcopy(self.cert) + bad['upper_witnesses'][0]['terms'][0][2] = 'Y7' + with self.assertRaisesRegex(ValueError,'contact frame'): + v.replay(self.word,self.ports,bad) + + def test_nonzero_dirty_compensation_fault(self): + bad = deepcopy(self.word) + bad['program'][0][3] = '-1/8' + with self.assertRaisesRegex(ValueError,'complete endpoint|own target dirt'): + v.replay(bad,self.ports,self.cert) + + def test_nonzero_cleanup_fault(self): + bad = deepcopy(self.word) + bad['program'][-1][3] = -1 + with self.assertRaisesRegex(ValueError,'complete endpoint Q7'): + v.replay(bad,self.ports,self.cert) + + def test_scalar_frame_and_private_lifetime_fault(self): + bad = deepcopy(self.word) + bad['program'][0][-1] = [1] + with self.assertRaisesRegex(ValueError,'scalar frame'): + v.replay(bad,self.ports,self.cert) + bad = deepcopy(self.word) + event = next(x for x in bad['program'] if x[0]=='erase') + event[-1] = [] + with self.assertRaisesRegex(ValueError,'private discard'): + v.replay(bad,self.ports,self.cert) + + def test_violated_lower_generator(self): + pools = deepcopy(self.collected[0][2753]) + # A concrete forbidden generator, with target factor p.r_t != 0. + p = self.cert['lower_vectors']['p'] + t = next(t for t,r in enumerate(self.ports) if v.dot(p,r)) + pools[t].add(tuple(map(Q,[1,0,0,0,0,0,0,0]))) + with self.assertRaisesRegex(ValueError,'lower functional'): + v.lower(pools,self.ports,self.cert['lower_vectors'],True) + + def test_omitted_compression_premises(self): + z = self.cert['lower_vectors'] + def outer(a,b): + return [[x*y for y in b] for x in a] + def compressed(n): + return [[sum(l[i]*n[i][j]*r[j] for i in range(8) for j in range(8)) + for r in (z['a'],z['b'],z['k'])] for l in (z['p'],z['q'],z['w'])] + n = outer([0,1,1,0,0,0,0,-1],[-1,0,0,0,0,0,0,0]) + self.assertEqual(v.rank(n),1) + self.assertEqual([r[:2] for r in compressed(n)[:2]],[[-1,-1],[-1,-1]]) + # All other rank-three fixed entries survive, but dropping q.N.k=0 + # admits the actual rank-two new witness. + n = outer([0,0,-1,1,0,0,0,1],[0,1,0,0,0,0,0,2]) + n[1][2] -= 1 + self.assertEqual(compressed(n),[[0,-1,0],[-1,0,-2],[1,0,2]]) + self.assertEqual(v.rank(n),2) + # Missing nuisance availability invalidates projection already in Q^2: + # span(x+z) has projected rank1 but intersects the x-axis only at0. + self.assertEqual(v.rank([[1,1],[1,0]]),2) + + +if __name__=='__main__': + unittest.main() diff --git a/research/p104-prefix-tail-independent-audit/verify.py b/research/p104-prefix-tail-independent-audit/verify.py new file mode 100644 index 0000000000..32ab3c90a9 --- /dev/null +++ b/research/p104-prefix-tail-independent-audit/verify.py @@ -0,0 +1,257 @@ +"""Independent rational trace and compression audit. Ross / OpenAI Codex. +Apache-2.0. No predecessor Python imports. Explicit Fraction rows and +canonical binary elimination replace the integer/8 changed-group collector. +""" +from collections import Counter, defaultdict +from fractions import Fraction as Q +from functools import lru_cache +from itertools import combinations, product +from pathlib import Path +import argparse +import hashlib +import json + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +@lru_cache(None) +def frame(vectors): + basis = {} + for value in vectors: + need(type(value) is int and 0 < value < 512, 'frame label') + while value: + bit = value.bit_length()-1 + if bit in basis: + value ^= basis[bit] + else: + basis[bit] = value + break + need(value != 0, 'dependent frame') + for bit in sorted(basis): + for other in basis: + if other > bit and (basis[other] >> bit) & 1: + basis[other] ^= basis[bit] + return tuple(basis[i] for i in sorted(basis, reverse=True)) + + +def inside(a, b): + for value in a: + for pivot in b: + if value >> (pivot.bit_length()-1) & 1: + value ^= pivot + if value: + return False + return True + + +def dot(a,b): + return sum(x*y for x,y in zip(a,b)) + + +def rank(matrix): + basis = {} + for row in matrix: + row = list(map(Q,row)) + for pivot,old in sorted(basis.items()): + if row[pivot]: + scale = row[pivot]/old[pivot] + row = [x-scale*y for x,y in zip(row,old)] + pivot = next((i for i,x in enumerate(row) if x),None) + if pivot is not None: + basis[pivot] = row + return len(basis) + + +def inputs(): + answer = {} + for pin in json.loads((HERE/'SOURCES.json').read_text())['files']: + if pin['usage'] == 'input': + data = (ROOT/pin['path']).read_bytes() + need(hashlib.sha256(data).hexdigest() == pin['sha256'],'source pin') + answer[Path(pin['path']).name] = json.loads(data) + return answer + + +def roots(fixture): + result = set() + for i,j in combinations(range(8),2): + for sign in [-1,1]: + row = [0]*8 + row[i],row[j] = 2,2*sign + result.add(tuple(row)) + result.update((1,*s) for s in product([-1,1],repeat=7) if sum(x<0 for x in s)%2 == 0) + removed = set(map(tuple,fixture['F0']+fixture['C'])) + need(len(result)==120 and len(removed)==16 and removed<=result,'puncture') + result = sorted(result-removed) + need(all(sum(r[i]*r[j] for r in result)==104*(i==j) for i in range(8) for j in range(8)),'RRt') + return result + + +def replay(word,ports,certificate,reverse_basis=False): + names = [f'{s}{i}' for s,n in [('X',104),('Y',104),('Q',8),('G',32),('D',32)] for i in range(n)] + need(set(word['initial_frames'])==set(word['final_frames'])==set(names),'boundary names') + need(len(word['program'])==4058,'4058 events') + def chart(v): + return frame(tuple(reversed(v)) if reverse_basis else tuple(v)) + frames = {r:chart(word['initial_frames'][r]) for r in names} + values = {r:{i:Q(1)} for i,r in enumerate(names)} + ids,frozen,row_ids = {},[],{} + def intern(r): + key = tuple(sorted(values[r].items())) + if key not in ids: + ids[key] = len(frozen) + frozen.append(key) + row_ids[r] = ids[key] + for r in names: + intern(r) + need(all(frames[r]==() for r in names[104:]),'175 nuisance units per target') + wants = {(t,c,r) for w in certificate['upper_witnesses'] for t,c,r,weight in w['terms']} + requested = defaultdict(list) + for t,c,r in wants: + requested[c].append((t,r)) + captures,projected,seen = {},{},set() + pools = [set() for _ in range(104)] + checkpoints,profile,events = {},Counter(),Counter() + copied = False + def projection(row_id): + if row_id not in projected: + row = dict(frozen[row_id]) + alpha = tuple(sum((value*ports[i][j] for i,value in row.items() if i<104),Q(0))/104 for j in range(8)) + need(all(dot(alpha,r)==row.get(i,0) for i,r in enumerate(ports)),'source row outside code') + projected[row_id] = alpha + return projected[row_id] + def inspect(cut): + groups = defaultdict(list) + for r in values: + groups[frames[r]].append(r) + # Every cut is visited. Full-row interning avoids repeated arithmetic, + # without depending on a changed-frame-group notification algorithm. + for t in range(104): + target = f'Y{t}' + for r in groups[frames[target]]: + if r==target: + continue + pair = t,row_ids[r] + if pair in seen: + continue + seen.add(pair) + need(values[r].get(104+t,0)==0,'own target dirt') + alpha = projection(row_ids[r]) + if any(alpha): + pools[t].add(alpha) + if cut in (2753,2823): + checkpoints[cut] = [set(p) for p in pools] + for t,r in requested[cut]: + need(r in values and r!=f'Y{t}' and frames[r]==frames[f'Y{t}'],'contact frame') + captures[t,cut,r] = projection(row_ids[r]) + inspect(0) + for cut,event in enumerate(word['program'],1): + op,dst = event[:2] + events[op] += 1 + if op=='transport': + before,after = chart(event[2]),chart(event[3]) + need(frames[dst]==before,'transport entry') + need(before!=after and (inside(before,after) or inside(after,before)),'nested frame') + need(event[4]==abs(len(after)-len(before)),'paid rank') + frames[dst] = after + profile[event[4]] += 1 + elif op=='zero': + need(dst=='C' and dst not in values and len(chart(event[2]))==8,'private allocation') + values[dst],frames[dst],copied = {},chart(event[2]),False + intern(dst) + elif op=='erase': + need(dst=='C' and copied and frames[dst]==chart(event[2]) and len(frames[dst])==1,'private discard') + del values[dst],frames[dst],row_ids[dst] + elif op in ('add','copy'): + src = event[2] + need(src!=dst and frames[src]==frames[dst]==chart(event[-1]),'scalar frame') + if op=='copy': + need(dst=='C' and not values[dst] and not copied,'private copy') + values[dst],copied = dict(values[src]),True + else: + weight = Q(event[3]) + need(weight!=0,'zero scalar') + new = dict(values[dst]) + for col,value in values[src].items(): + new[col] = new.get(col,0)+weight*value + if not new[col]: + del new[col] + values[dst] = new + intern(dst) + else: + raise ValueError('unknown event') + inspect(cut) + need(set(values)==set(names),'private closure') + for i,r in enumerate(names): + expected = {i:Q(1)} + if r.startswith('Y'): + t = int(r[1:]) + expected.update({s:Q(dot(ports[t],root),8) for s,root in enumerate(ports) if dot(ports[t],root)}) + need(values[r]==expected,'complete endpoint '+r) + need(frames[r]==chart(word['final_frames'][r]),'endpoint frame') + need(dict(profile)=={1:1074,2:58,3:86,4:104,5:48,6:24,7:8,8:8},'profile') + need(dict(events)=={'add':2624,'transport':1410,'zero':8,'copy':8,'erase':8},'event inventory') + need(set(captures)==wants,'contact coverage') + return checkpoints,captures,len(seen) + + +def lower(pool,ports,v,three): + pairs = [('p','a'),('p','b'),('q','a')] + if three: + pairs += [('p','k'),('q','k'),('w','k')] + for t,rows in enumerate(pool): + for alpha in rows: + need(all(dot(v[l],ports[t])*dot(alpha,v[r])==0 for l,r in pairs),'lower functional') + need([dot(v['p'],v['a']),dot(v['p'],v['b']),dot(v['q'],v['a'])]==[0,-1,-1],'fixed 2x2 entries') + if three: + need([dot(v[x],v['k']) for x in ('p','q','w')]==[0,0,2],'fixed 3x3 entries') + return sum(map(len,pool)) + + +def upper(w,captures,ports): + a = [[Q(0)]*8 for _ in ports] + for t,c,r,weight in w['terms']: + need(c<=w['cut'],'future contact') + a[t] = [x+Q(weight)*y for x,y in zip(a[t],captures[t,c,r])] + n = [[Q(i==j)-sum(ports[t][i]*a[t][j] for t in range(104)) for j in range(8)] for i in range(8)] + k = [[Q(t==s)-Q(dot(ports[t],ports[s]),8)+12*dot(a[t],ports[s]) for s in range(104)] for t in range(104)] + small,big = rank(n),rank(k) + need(big==96+small==w['minimum'],'upper rank') + if w['cut']==2754: + x,u,e1,e2 = [0,0,-1,1,0,0,0,1],[0,1,0,0,0,0,0,2],[0,1,0,0,0,0,0,0],[0,0,1,0,0,0,0,0] + need(n==[[x[i]*u[j]-e1[i]*e2[j] for j in range(8)] for i in range(8)],'explicit residual') + return [w['cut'],small,big] + + +def run(): + raw = inputs() + payload = (HERE/'WITNESS.json').read_bytes() + need(hashlib.sha256(payload).hexdigest()=='8abbe9564e19ac966bf97480d7c00891289f9b1d6be13cfa9a2d604b97bc0a5c','certificate pin') + cert = json.loads(payload) + ports = roots(raw['P104-FIXTURE.json']['section4_explicit_P104']) + pools,captures,seen = replay(raw['LOWRANK-WITNESS.json'],ports,cert) + sizes = [lower(pools[c],ports,cert['lower_vectors'],c==2753) for c in (2753,2823)] + need(sizes==[324,427] and seen==110814,'pool and snapshot census') + return dict(status='PASS_INDEPENDENT_P104_TAIL_AUDIT',cuts=4059,columns=280,target_snapshots=seen, + pool_pairs=sizes,uppers=[upper(w,captures,ports) for w in cert['upper_witnesses']], + scope='Rational pooled availability only; no chronological or paid-cost claim') + + +if __name__=='__main__': + parser = argparse.ArgumentParser() + parser.add_argument('--out',type=Path) + args = parser.parse_args() + need(args.out is None or not args.out.exists(),'occupied output') + result = run() + need(result==json.loads((HERE/'RESULT.json').read_text()),'receipt mismatch') + if args.out: + with args.out.open('x') as f: + json.dump(result,f,indent=2) + f.write('\n') + print(json.dumps(result,sort_keys=True))