From 9a8e88c87c1d639d61b9789370288c5efbde2d6f Mon Sep 17 00:00:00 2001 From: ToikY <27568617+ToikY@users.noreply.github.com> Date: Wed, 11 Nov 2026 01:32:13 -0800 Subject: [PATCH 1/3] Reuse selected replay navigation for hosted checks Reuse the exact documentation blob carried by #7161 at bb36fc65ee0b161229169505f4840c436c5ca2b9, following #7147 and #7156. --- docs/ci-verification.md | 19 ++++++++++++++++++- 1 file changed, 18 insertions(+), 1 deletion(-) diff --git a/docs/ci-verification.md b/docs/ci-verification.md index 63ba3e9aa8..52b62d0481 100644 --- a/docs/ci-verification.md +++ b/docs/ci-verification.md @@ -1,8 +1,25 @@ # CI verification -## Current selected-family replay: #6030 +## Current selected-family replay: #7000 with #7001 The [selected record](../certificates/selected-result.json) binds conditional +κ = 0.00363005817 to the [application review](research/pr-intake-evidence/pr7000-application/PROOF-REVIEW.md), +[validation receipts](research/pr-intake-evidence/pr7000-application/VALIDATION.json), +and [explicit source closure](../certificates/frontier7000-source.json). +`make frontier7000-verify` follows that exact-source selected replay. The review +reuses eleven authenticated preceding executions and records seven fresh serial +application, scalar and complete native-catalogue executions. The earlier +monolithic timeout is retained separately and is not completed coverage. +Consult the receipts for exact commands, source heads and limits. + +The five inherited framework assumptions remain. No complete uniform word, +literal multiplier execution, independent human proof or formal-kernel proof +is asserted. Routine research submissions do not need to rerun this +selected-family replay. The sections below preserve historical checkpoints. + +## Historical selected-family replay: #6030 + +The [historical checkpoint](../certificates/checkpoints/frontier6030.json) binds conditional κ = 0.003125804 to the [proof review](research/pr-intake-evidence/pr6030-audit/PROOF-REVIEW.md), [validation receipts](research/pr-intake-evidence/pr6030-audit/VALIDATION.json), and [explicit source closure](../certificates/frontier6030-source.json). From caa737a86611333b029edbe5ca1e5f3d7f395955 Mon Sep 17 00:00:00 2001 From: ToikY <27568617+ToikY@users.noreply.github.com> Date: Wed, 11 Nov 2026 01:32:21 -0800 Subject: [PATCH 2/3] Bound lane-wise paired BIT IDLE regrouping --- .../NONUNIFORM-AUDIT.json | 38 + .../NONUNIFORM.json | 61 ++ .../NONUNIFORM.md | 58 ++ .../paired-bit-lanewise-idle-bound/PROOF.md | 85 +++ .../paired-bit-lanewise-idle-bound/README.md | 27 + .../RESULT.json | 688 ++++++++++++++++++ .../SOURCES.json | 42 ++ .../SOURCES.tsv | 4 + .../paired-bit-lanewise-idle-bound/TASK.json | 64 ++ .../VERIFY.json | 24 + .../nonuniform.py | 102 +++ .../nonuniform_audit.py | 88 +++ .../paired-bit-lanewise-idle-bound/replay.py | 53 ++ .../paired-bit-lanewise-idle-bound/verify.py | 251 +++++++ 14 files changed, 1585 insertions(+) create mode 100644 research/paired-bit-lanewise-idle-bound/NONUNIFORM-AUDIT.json create mode 100644 research/paired-bit-lanewise-idle-bound/NONUNIFORM.json create mode 100644 research/paired-bit-lanewise-idle-bound/NONUNIFORM.md create mode 100644 research/paired-bit-lanewise-idle-bound/PROOF.md create mode 100644 research/paired-bit-lanewise-idle-bound/README.md create mode 100644 research/paired-bit-lanewise-idle-bound/RESULT.json create mode 100644 research/paired-bit-lanewise-idle-bound/SOURCES.json create mode 100644 research/paired-bit-lanewise-idle-bound/SOURCES.tsv create mode 100644 research/paired-bit-lanewise-idle-bound/TASK.json create mode 100644 research/paired-bit-lanewise-idle-bound/VERIFY.json create mode 100644 research/paired-bit-lanewise-idle-bound/nonuniform.py create mode 100644 research/paired-bit-lanewise-idle-bound/nonuniform_audit.py create mode 100644 research/paired-bit-lanewise-idle-bound/replay.py create mode 100644 research/paired-bit-lanewise-idle-bound/verify.py diff --git a/research/paired-bit-lanewise-idle-bound/NONUNIFORM-AUDIT.json b/research/paired-bit-lanewise-idle-bound/NONUNIFORM-AUDIT.json new file mode 100644 index 0000000000..968b507a09 --- /dev/null +++ b/research/paired-bit-lanewise-idle-bound/NONUNIFORM-AUDIT.json @@ -0,0 +1,38 @@ +{ + "adjacent_K27_upper": [ + "-904206464049119748441522887503/100000000000000000000000000000", + "-9042064640491197484415228073/1000000000000000000000000000" + ], + "adjacent_K29_upper": [ + "-913587964502015460806911571031/100000000000000000000000000000", + "-228396991125503865201727872671/25000000000000000000000000000" + ], + "delta": [ + "1926687975213076849110197913/50000000000000000000000000000", + "3853375950426153698220395829/100000000000000000000000000000" + ], + "excess_penalty_lower": [ + "151192534742538651581564685863/100000000000000000000000000000", + "37798133685634662895391171473/25000000000000000000000000000" + ], + "maximizing_K": 28, + "minimum_cross_credit_growth_before_K28": [ + "5780063925639230547330593739/3125000000000000000000000000", + "11560127851278461094661187487/6250000000000000000000000000" + ], + "old_target_margin": [ + "-1502597480478683846599820945199/25000000000000000000000000000", + "-3005194960957367693199641852889/50000000000000000000000000000" + ], + "optimistic_target_upper": [ + "-408208301993217588716623543637/50000000000000000000000000000", + "-816416603986435177433247006927/100000000000000000000000000000" + ], + "source_sha256": "a46b6c6040f75184cab5467656811ad988c216e3bc8e44d595a5015b6e49620b", + "status": "PASS_NONUNIFORM_TARGET_PRICE", + "target": "10018846261809/2500000000000000", + "within_half_body_floor_per_excess_incidence": [ + "171468229574093508716387062081/25000000000000000000000000000", + "342936459148187017432774124163/50000000000000000000000000000" + ] +} diff --git a/research/paired-bit-lanewise-idle-bound/NONUNIFORM.json b/research/paired-bit-lanewise-idle-bound/NONUNIFORM.json new file mode 100644 index 0000000000..e5e0d6c880 --- /dev/null +++ b/research/paired-bit-lanewise-idle-bound/NONUNIFORM.json @@ -0,0 +1,61 @@ +{ + "base_head_capacity": 444, + "directed_K_cases_checked": 223, + "directed_max_margin": [ + "-40820830199321758871662351651614849876654734852001541372228422066907537357564699/5000000000000000000000000000000000000000000000000000000000000000000000000000000", + "-102052075498304397179155879129037124691636837130003853430571055167268843388786267/12500000000000000000000000000000000000000000000000000000000000000000000000000000" + ], + "directed_max_margin_K": 28, + "extra_body_moment_lower_per_incidence": [ + "342936459148187017432774124162284201321629034498162550064453886866480498422595933/50000000000000000000000000000000000000000000000000000000000000000000000000000000", + "17146822957409350871638706208114210066081451724908127503222694343324024921129993/2500000000000000000000000000000000000000000000000000000000000000000000000000000" + ], + "ignore_extra_cross_rank_positive_control": [ + "47618076698153012516100828464838152487400363113652308863484600443379951021833403/2500000000000000000000000000000000000000000000000000000000000000000000000000000", + "238090383490765062580504142324190762437001815568261544317423002216899755114292209/12500000000000000000000000000000000000000000000000000000000000000000000000000000" + ], + "input_sha256": { + "bit/EFREE-CALLER.json.gz": "757b3523798f840bdb02028b23708c3416627a99ea09e7a3c4bcdc5cd0c7ce4b", + "bit/EFREE-RESULT.json": "a46b6c6040f75184cab5467656811ad988c216e3bc8e44d595a5015b6e49620b", + "bit/independent/interval_gate.py": "8dc2bc4c64cba3f83c664373984a075f1a14b4d53958084091345c8cab189dec", + "bit/retained/inputs/BIT-NATIVE-WORD.json.gz": "51203e7fc75ba10bd3ac3f8e675759f47e13d262bea66b6600d1e515095cad78" + }, + "larger_K_have_nonincreasing_upper": true, + "max_cross_credit_per_two_incidents": [ + "1926687975213076849110197913443204328483647910554739858834675985502137520955849/50000000000000000000000000000000000000000000000000000000000000000000000000000000", + "1926687975213076849110197913443204328483647910554739858834675985502137520956759/50000000000000000000000000000000000000000000000000000000000000000000000000000000" + ], + "minimum_physical_idles_incidence": 15984, + "native_calls": 36, + "net_loss_lower_per_extra_incidence": [ + "37798133685634662895391171470647681182638101651584945667470901498480630366992551/25000000000000000000000000000000000000000000000000000000000000000000000000000000", + "75596267371269325790782342941295362365276203303169891334941802996961260733997219/50000000000000000000000000000000000000000000000000000000000000000000000000000000" + ], + "old_paid_and_productive_match": true, + "opposite_support_checks": 81, + "sample_directed_margins": { + "0": [ + "-617359077503841058424423731244591959409737856718042953005173135346049304195229941/12500000000000000000000000000000000000000000000000000000000000000000000000000000", + "-617359077503841058424423731244591959409737856718042953005173135346049304190508787/12500000000000000000000000000000000000000000000000000000000000000000000000000000" + ], + "27": [ + "-904206464049119748441522833304429499877415114907618985199418281008740875802583139/100000000000000000000000000000000000000000000000000000000000000000000000000000000", + "-226051616012279937110380708326107374969353778726904746299854570252185218940416327/25000000000000000000000000000000000000000000000000000000000000000000000000000000" + ], + "28": [ + "-40820830199321758871662351651614849876654734852001541372228422066907537357564699/5000000000000000000000000000000000000000000000000000000000000000000000000000000", + "-102052075498304397179155879129037124691636837130003853430571055167268843388786267/12500000000000000000000000000000000000000000000000000000000000000000000000000000" + ], + "29": [ + "-114198495562751932600863939598739580768334057618351366110153294577589966436185269/12500000000000000000000000000000000000000000000000000000000000000000000000000000", + "-913587964502015460806911516789916646146672460946810928881226356620719731448476823/100000000000000000000000000000000000000000000000000000000000000000000000000000000" + ], + "222": [ + "-1228374765768205517788435586562596671209461843535569876487431052315204581195940591/6250000000000000000000000000000000000000000000000000000000000000000000000000000", + "-307093691442051379447108896640649167802365460883892469121857763078801145298344221/1562500000000000000000000000000000000000000000000000000000000000000000000000000" + ] + }, + "scope": "Fixed #7001 productive profile and 36 native LOCALs, individually charged rank-seven-per-stage lane-wise masks, separate body-free heads, arbitrary rectangular scalar contexts. All extra body incidence covered.", + "status": "PROVED_NEGATIVE_DECLARED_LANEWISE_IDLE_MODEL", + "target": "10018846261809/2500000000000000" +} diff --git a/research/paired-bit-lanewise-idle-bound/NONUNIFORM.md b/research/paired-bit-lanewise-idle-bound/NONUNIFORM.md new file mode 100644 index 0000000000..3cc9728239 --- /dev/null +++ b/research/paired-bit-lanewise-idle-bound/NONUNIFORM.md @@ -0,0 +1,58 @@ +# Lane-wise IDLE regrouping at the paired BIT target + +**NO VERIFIED GAIN.** With all 36 old LOCAL calls and productive targets fixed, the complete optimistic BIT moment is strictly below **−8.16416603986435** at the exact target 10018846261809/2500000000000000. This covers nonuniform, separately charged IDLE masks even with arbitrary copy and port mixing and extra body incidences. + +## Contract + +Use the formal independent q and body variables of exact #7001, specialized at one. On the 38N root coordinates, N=111, the desired q derivative is identity and the desired body derivative T_s is the literal diagonal stage projector. Fresh productive helper inputs are set to zero for this necessary condition. Across every opposite-half pair the support intersection is the common 2N-plane E (roles 0 and 19). The two other 18-role blocks belong to separate halves. Each old LOCAL's constant shear C and q derivative M satisfy that MC⁻¹ is square-zero of rank N. Arbitrary rectangular scalar preparation, recovery, cross-copy mixing and scratch preserve the transported body and q factorizations shown in the [uniform special case](PROOF.md). The old paid and productive helper channels are retained. + +Each paid IDLE mask may vary from lane to lane and contributes one common rank-at-most-one derivative in every included stage. Its tariff is H(7ℓ) for ℓ included stages, with H(r)=r^(1−κ*) and H(0)=0. Additional head operations are body-free and each derivative rank is at most its paid rank. Setup, scalar routing, restoration, precision and tape charges are granted free in the upper bound. A job supplying distinct derivative directions across its stages or coupled head/body action under one charge is outside this model. + +## Head rank with excess body incidences + +At stage s, write T_s=U_sV_s with latent dimension m_s and excess e_s=m_s−rank(T_s). Rank of the block matrix with identities on the diagonal and U_s,V_s off-diagonal, eliminated in either order, gives + +```text +rank(I−V_sU_s) = m_s−d + rank(I−T_s) = e_s. +``` + +Thus (I−T_s)U_s and V_s(I−T_s) each have rank at most e_s. The two retained LOCAL head factors X_s,Y_s inherit these bounds on output and input leakage. A rank-one mask shared by multiple stages can use the same abstract rank factorization at each stage because its embedded derivative is common. A zero mask derivative may be represented with zero factors. + +For stages s,t in opposite halves, let P denote the q shared factor positions. Since V_PU_P differs from I_q by a submatrix of each stage's rank-e defect, rank(V_P) and rank(U_P) are each at least q−min(e_s,e_t). The literal target projectors commute and satisfy T_sT_t=E, the common 2N-plane. From + +```text +I−E = (I−T_s)+T_s(I−T_t) +``` + +and commutation, rank(V_P(I−E))≤e_s+e_t. This gives rank(V_PE)≥q−min(e_s,e_t)−e_s−e_t. The off-diagonal LOCAL-to-IDLE block gives rank(V_PX_s)≤e_s, hence rank(V_PEX_s)≤2e_s+e_t. Decomposing E X_s through the kernel of V_P on E gives + +```text +rank(E X_s) ≤ 2N−q+min(e_s,e_t)+3e_s+2e_t. +``` + +Finally rank(Y_t(I−E)X_s)≤e_s+e_t by writing I−E=(I−T_t)+T_t(I−T_s). Hence rank(Y_tX_s)≤2N−q+4(e_s+e_t). Both inequalities permit arbitrary oblique and rectangular contexts. + +In A=I+YX each stage's 2N×2N principal diagonal differs from identity by rank at most e_s. This follows by replacing V_sU_s by identity and using the old LOCAL internal square-zero factors' K_iJ_i=0. Correcting the two diagonal blocks to identity loses at most e_s+e_t in the lower rank bound. Schur elimination on the corrected principal block gives rank at least 2N+q−4(e_s+e_t). The full correction rank is therefore at least 4N+q−5(e_s+e_t). For K=max q over the 8×8 active opposite pairs and e=sum e_s, this implies 444+K−5e, with a zero lower bound allowed if the expression is negative. + +## Complete optimistic tariff + +Let d_s be the minimum physical IDLE count at stage s. Its actual count is d_s+e_s. Separate every cross mask into its two half-masks. Remove e_s incidences from each stage to recover all d_s exactly. Within a half, each removal costs at least H(63)−H(56), by concavity and the nine-stage length cap. The residual within-half bill is at least the old majorizing bill. + +For a cross mask with a,b positive incidences in the two halves, its saving relative to separation is at most δ(a+b)/2≤δ ab, with δ=2H(7)−H(14). Indeed a balanced real split maximizes the saving at fixed a+b, yielding δ((a+b)/2)^(1−κ*), at most δ(a+b)/2. The sum of ab over masks counts opposite-stage pairs with multiplicity. Active pairs contribute at most 64K and each inactive incidence creates at most nine pairs. The inactive stages have d_s=0, so total cross savings are at most δ(64K+9e). + +For a fixed active stage s, let q_s count its cross masks. Their output factor has rank at least q_s−e_s. Assign each mask to one opposite partner t, keeping its common output factor. The exterior part (I−E)U_P is a sum of (I−T_s)U_P of rank at most e_s and grouped T_s(I−T_t)U_{P,t} terms of total rank at most e_otherHalf. Thus q_s≤2N+2e_s+e_otherHalf. Summing the 16 active stages, then adding inactive incidences, yields total cross incidence at most 3552+10e. Consequently the alternate saving bound is δ(1776+5e). + +Because H increases by at most one per added integer rank, packed head cost is at least H(444+K)−5e even if the earlier correction-rank bound is negative. Relative to the old full invoice the directed upper is therefore + +```text +old_margin + 444 − H(444+K) + δ min(64K,1776) +− e (H(63)−H(56)−5−9δ). +``` + +Independent Fraction arithmetic proves δ≈0.038533759504261536 and excess penalty >1.51192534742538. Hence e=0 maximizes the relaxed upper. As K increases from 0 to 28 the minimum credit increment is 48δ>1.8496, exceeding every head increment. At and after 28 the credit is flat and head price strictly increases. Therefore the global optimum over nonnegative integer K is 28. Its upper interval lies strictly below −8.16416603986435. The adjacent K=27 and K=29 values are approximately −9.04206464049120 and −9.13587964502015. + +## Replay and credit + +Use CPython 3.12 with assertions. The four canonical inputs and their exact hashes are listed in SOURCES.tsv. The clean repository replay in README.md regenerates both the uniform and nonuniform results and independently checks the lane-wise price using directed rational arithmetic. Omitting the extra cross-mask head debit gives a positive relaxed upper, an explicit negative control for that pricing error. + +Credit [#7001](https://github.com/CrocSwap/integer-mult-bounds/pull/7001), [#6726](https://github.com/CrocSwap/integer-mult-bounds/pull/6726), [#6834](https://github.com/CrocSwap/integer-mult-bounds/pull/6834), [#6980](https://github.com/CrocSwap/integer-mult-bounds/pull/6980), and [#7160](https://github.com/CrocSwap/integer-mult-bounds/pull/7160) for the paired word, caller, ledger and earlier head-rank scope. [#7177](https://github.com/CrocSwap/integer-mult-bounds/pull/7177) supplies a distinct formal caller identity requiring a changed LOCAL. OpenAI Codex and subagents materially assisted. No admitted supplier or complete bound changes. diff --git a/research/paired-bit-lanewise-idle-bound/PROOF.md b/research/paired-bit-lanewise-idle-bound/PROOF.md new file mode 100644 index 0000000000..d0e138bf12 --- /dev/null +++ b/research/paired-bit-lanewise-idle-bound/PROOF.md @@ -0,0 +1,85 @@ +# Cross-copy rank excludes uniform IDLE regrouping at the paired BIT target + +**NO VERIFIED GAIN.** Keep the complete productive profile and all 36 native calls of CubeJerry's paired E-free BIT caller, with two old LOCALs per stage. Give the candidate arbitrary cross-copy and cross-port scalar mixing, rectangular scalar contexts and scratch. The exact target `10018846261809/2500000000000000` remains out of reach under uniform IDLE regrouping and the inherited rank tariff for separate body-free head correction. The proof concerns the formal first-order necessary condition and the complete optimistic raw invoice at this target. It does not require a search over embeddings. + +## Declared model + +Work over F₂, with the same q and independent D_s body symbols as the literal caller. At q=D_s=1, the desired specialized map is identity on 38 role blocks of N=111 lanes each. The desired q derivative is I on those 38N public coordinates. Its body derivative T_s is a diagonal projector on all role blocks whose target body monomials contain D_s. Roles 0–18 are one copy and 19–37 are the other. Stages 1–9 use roles 0 and 19 plus the corresponding private prefixes. Stages 10–18 use roles 0 and 19 plus the corresponding private suffixes. The authenticated literal diagonal checks every one of the 81 opposite-half pairs. For each such pair T_sT_t=T_tT_s=E, the coordinate projection onto roles 0 and 19 of dimension 2N. + +Keep the old LOCAL operator and all its paid and productive helper charges. On its 2N native lanes its constant part C is the binary shear, and its q derivative M has only the source-to-destination block I_N. Thus M C⁻¹ is square-zero of rank N. Its body coefficient is C. Allow arbitrary scalar routing, mixing and rectangular preparation and recovery around the old operator. These contexts enter at their specialization in the product-rule term. Body derivatives come from the two retained LOCALs and the uniform IDLEs. Each uniform mask consumes one logical incidence in every included stage and contributes the same rank-at-most-N body derivative to every included stage. All extra q derivative comes from body-free head primitives, with each derivative rank at most its charged rank. Other scalar actions have zero q and body derivative in this gate. The model allows first-order interactions through the specialized linear contexts and grants ordinary work, ownership overhead and restoration for free in the price upper bound. + +## Saturation and the shared projector + +At a LOCAL, let A map public inputs to its two native blocks before the specialized operation and B map a perturbation after the operation to the public output. Its body term is B C A=U V with U=B and V=C A. Its q term is B M A=U (M C⁻¹) V. For IDLE use a rank factorization through N lanes, padding if necessary. Each stage s has T_s=U_s V_s, where U_s concatenates its two LOCAL output factors and all its IDLE output factors, and V_s stacks their matching input factors. Rectangular contexts are permitted. + +Let n_s count its logical IDLE incidences. Rank(T_s)≤(4+n_s)N. The literal target gives the lower bounds 0,2,…,16 and 16,…,2,0, totaling 144. At exactly 144 every stage is saturated, meaning its total factor dimension equals rank(T_s). Then U_s is injective, V_s surjective and V_sU_s=I by T_s²=T_s. Consequently each block projector P_i=U_iV_i satisfies T_sP_i=P_iT_s=P_i, and P_iP_j=P_jP_i=0 for different blocks of that stage. This is algebraic annihilation. None of the projectors needs to be orthogonal for an inner product. + +If one uniform mask serves stages s and t in opposite halves, its embedded derivative P is the same in both. Saturation makes P an idempotent of rank N. The two stage support identities give EP=PE=P, so P acts on E and vanishes outside E. Both its image and covector support matter. Any shared masks at the same stage are pairwise annihilating and have images in E, so at most two can occur in that stage. + +## First-order head obstruction + +For each LOCAL factor the internal square-zero rank-N matrix as J_iK_i with J_i injective and K_i surjective. Square-zero then implies K_iJ_i=0. Concatenate its transported factors X_i=U_iJ_i in X and stack Y_i=K_iV_i in Y. The complete old-LOCAL head term is XY and the extra correction is I_(38N)+XY. Eliminate either diagonal identity block in the block matrix with off-diagonal X and Y to obtain + +```text +rank(I_(38N)+XY) = 2N + rank(I_(36N)+YX). +``` + +In A=I_(36N)+YX, the 2N-dimensional principal diagonal of any saturated stage is I_(2N). In fact V_iU_j=0 for different factors in that stage and K_iJ_i=0 on each native diagonal. A single saturated stage therefore forces 4N=444 extra head rank. + +Now let a cross-half mask P occur at saturated opposite stages s,t. The transported native factors for stage s satisfy T_s X_s=X_s, Y_s T_s=Y_s and P X_s=Y_s P=0. The opposite stage supports give + +```text +Y_t X_s = Y_t E X_s. +``` + +Since P E X_s=P X_s=0, the image of E X_s is in the N-dimensional kernel of P on E. The off-diagonal block Y_t X_s thus has rank at most N. The other block obeys the same bound. The principal block of A on (s,t) has rank + +```text +rank [ I_(2N) Y_s X_t ] = 2N + rank(I_(2N)+(Y_t X_s)(Y_s X_t)) ≥ 3N. + [ Y_t X_s I_(2N) ] +``` + +The inequality uses rank(I+R)≥2N−rank(R). Any cross-half mask forces at least 5N=555 aggregate extra head rank. If two cross-half masks occupy the same stage s, their projectors are complementary on E. Their common kernel on E is zero, so E X_s=0. Pairing s with any opposite saturated stage now gives principal rank at least 4N and total correction rank at least 6N=666. + +This conclusion uses no independence of the two copies or the 111 individual ports. It holds for oblique projectors and arbitrary linear scalar contexts in the declared model. + +## Complete optimistic price cases + +Write p=1−κ*. Rank subadditivity and the inherited head tariff require total charged head rank at least the residual rank. The concavity and monotonicity of r^p permit charging all of that rank as one job to lower the price, even where such a packed job lacks a physical realization. + +At 144 incidences, the verified within-half majorant has four masks of each length 1–8. When cross-half masks are permitted, the majorant has two length-16 masks and four masks of each length 1–7. For any k selected masks, if c are shared and a,b are internal, the stage capacities are at most min(d_s,a+min(c,2)) and min(d_s,b+min(c,2)) on the two halves. A c greater than two can be reduced to two and the excess assigned internally in this upper bound. The verifier checks all relevant prefix maxima over c=0,1,2 and the allocations a+b=k−c. The majorizing length sequence minimizes the sum of increasing concave body prices at fixed incidence. Changed LOCAL embeddings do not invalidate the capacity bound. + +At 145 incidences at least one stage is saturated, so charge 444 head units. Let every IDLE mask cover all 18 stages to lower its price. The most favorable partition is eight length-18 masks and one length-one mask. At 146 or more, grant head work free. Eight length-18 masks and one length-two mask give a lower body bill at 146, and the same bound holds for larger incidence since r^p increases. + +| Logical IDLE scope | Optimistic minimum head rank | Directed raw target margin upper, approximate | +|---|---:|---:| +| 144, no cross-half mask | 444 | −49.38872620030728 | +| 144, any cross-half mask | 555 | −89.35779527059788 | +| 144, two cross-half masks at one stage | 666 | −197.10789988018968 | +| 145 | 444 | −271.8484172928302 | +| 146 or more | 0 | −605.2506210567519 | + +The verifier reconstructs both complete literal P and T from the native MOVE frames, native helper endpoint ranks, and 798 caller events. Its directed intervals give all five strict negative signs. The row for two shared masks at a stage strengthens the any-cross case. These cases exhaust the declared uniform model at the target. This does not exclude per-port nonuniform masks, a shared operation with different body derivative images in its included stages, head-body coupled primitives, a change to the paid native operator, or a changed productive profile. + +## Clean replay and controls + +Python 3.10 or later, tested on CPython 3.12.14. From the directory containing `verify.py` and `SOURCES.tsv`, stage the four public immutable inputs into a fresh directory. The verifier authenticates each path internally. + +```bash +set -e +scripts="$PWD" +data="$(mktemp -d)" +py="$(command -v python3)" +while IFS=$'\t' read -r path hash url; do + mkdir -p "$data/$(dirname "$path")" + curl -LfsS "$url" -o "$data/$path" + printf '%s %s\n' "$hash" "$data/$path" | shasum -a 256 -c - +done < SOURCES.tsv +mkdir "$data/empty" +cd "$data/empty" +env -i PATH=/usr/bin:/bin "$py" -I -B "$scripts/verify.py" "$data" +``` + +I ran this verifier twice on a newly staged root of exact canonical Git blobs with an empty cwd and environment. Both runs exited zero with byte-identical JSON and empty stderr. The 24 exact rectangular controls cover all six rank-one common-plane projections over F₂ and four arrangements with one or two shared masks. They verify the block rank and head residual identity, including oblique projectors. The image-only control rejects a projector whose covector leaks into a private role. Appending one byte to the invoice fails its path-keyed hash with exit 1 before scientific stdout. The optional predecessor audit authenticates four sealed local Round 13 files and checks overlap with their matching directed intervals. That audit is independent of the core replay. + +Credit CubeJerry's [#7001 paired E-free caller](https://github.com/CrocSwap/integer-mult-bounds/pull/7001), its #6726 native and #6834/#6980 caller lineage, and Round 13's fixed-embedding and separate-star work for the earlier rank-444 and uniform-incidence bounds. The opposite-stage Schur rank argument is the new step. It removes the earlier restriction to independent copies or literal head stars. OpenAI Codex materially assisted. The separate lane-wise extension is in NONUNIFORM.md. diff --git a/research/paired-bit-lanewise-idle-bound/README.md b/research/paired-bit-lanewise-idle-bound/README.md new file mode 100644 index 0000000000..792b4bf3fb --- /dev/null +++ b/research/paired-bit-lanewise-idle-bound/README.md @@ -0,0 +1,27 @@ +# Bound lane-wise BIT IDLE regrouping + +**κ change 0%.** Keep the exact #7001 paired BIT endpoint, all 36 old LOCAL calls and the productive targets. Allow arbitrary copy and port mixing, rectangular scalar contexts and separately charged IDLE masks that vary by lane. The complete optimistic raw target margin is strictly below **−8.16416603986435** at **10018846261809/2500000000000000**. + +The [lane-wise proof](NONUNIFORM.md) ties the body saving to the head correction. If `K` is the greatest number of common masks between an opposite active stage pair and `e` is the total excess body incidence, the head correction has rank at least `444 + K − 5e`. Separating cross-half masks bounds their best compression credit, including every possible excess incidence. Directed arithmetic maximizes the relaxed price at `K = 28, e = 0`. Giving cross-mask credit without the corresponding head debit yields a positive false control. The [uniform case](PROOF.md) gives sharper rank bounds when a common mask spans all 111 lanes. + +## Relation to earlier work + +[#7160](https://github.com/CrocSwap/integer-mult-bounds/pull/7160) derives the original-body QUERY rank floor. [#7162](https://github.com/CrocSwap/integer-mult-bounds/pull/7162) varies LOCAL multiplicities on the 38-role model with whole-layer masks and their uniform 111-job tariffs. Here the 36 LOCALs are fixed. Mask incidence and rank are counted on the full 4,218 root coordinates, permitting nonuniform masks and arbitrary rectangular cross-port context. The new inequality charges the head cost of actual shared body lanes and bounds leakage at nonsaturated stages. [#7177](https://github.com/CrocSwap/integer-mult-bounds/pull/7177) changes the LOCAL operator itself, which is outside this proof. + +## Clean replay + +From a clean checkout, with CPython 3.12 and assertions enabled: + +~~~sh +python3.12 -B scripts/research_package.py --package research/paired-bit-lanewise-idle-bound +~~~ + +The registered replay authenticates four exact in-tree sources from canonical commit e54523517d0f03e58352e647c403a5af3e525a57. It reconstructs the complete paid and productive histograms, verifies all 81 opposite-stage supports and 24 oblique and rectangular rank controls, evaluates the directed price and independently confirms the maximum with rational arithmetic. It compares three receipts byte for byte. A changed invoice byte and an image-only false sharing projector are rejected. + +## Open next questions + +Can a new paid operation carry different mask directions across its lanes under one concave charge, or couple head and body at a lower complete price? Start with two lanes and distinct masks. Specify the exact arbitrary-input signed action, charge its native, ordinary and tape costs, and show both lane returns. Such a changed primitive, changed productive stock and changed native operators remain open. This proof concerns the fixed formal and tariff model. A complete supplier or multiplication theorem is not asserted. + +## Credit + +Credit [#7001](https://github.com/CrocSwap/integer-mult-bounds/pull/7001), [#6726](https://github.com/CrocSwap/integer-mult-bounds/pull/6726), [#6834](https://github.com/CrocSwap/integer-mult-bounds/pull/6834) and [#6980](https://github.com/CrocSwap/integer-mult-bounds/pull/6980) for the retained word, caller and paid invoice. Credit #7160 and #7162 for prior stage-rank and uniform price arguments. OpenAI Codex and subagents materially assisted. Apache-2.0. diff --git a/research/paired-bit-lanewise-idle-bound/RESULT.json b/research/paired-bit-lanewise-idle-bound/RESULT.json new file mode 100644 index 0000000000..a8bc5f928a --- /dev/null +++ b/research/paired-bit-lanewise-idle-bound/RESULT.json @@ -0,0 +1,688 @@ +{ + "common_role_coordinates": [ + 0, + 19 + ], + "directed_optimistic_target_margins": { + "144_any_cross_mask": [ + "-8935779527059788205096626258036625946034356390403664523089112050504305317871866619/100000000000000000000000000000000000000000000000000000000000000000000000000000000", + "-8935779527059788205096626258036625946034356390403664523089112050504305317834112261/100000000000000000000000000000000000000000000000000000000000000000000000000000000" + ], + "144_no_cross_mask": [ + "-617359077503841058424423731244591959409737856718042953005173135346049304195229941/12500000000000000000000000000000000000000000000000000000000000000000000000000000", + "-617359077503841058424423731244591959409737856718042953005173135346049304190508787/12500000000000000000000000000000000000000000000000000000000000000000000000000000" + ], + "144_two_cross_masks_same_stage": [ + "-1231924374251185532869973813836736541399113052646590404181583978500970066716677421/6250000000000000000000000000000000000000000000000000000000000000000000000000000", + "-153990546781398191608746726729592067674889131580823800522697997312621258339289661/781250000000000000000000000000000000000000000000000000000000000000000000000000" + ], + "145_incidences": [ + "-13592420864641511951585554530804010997172027506208679734689402557736475909008717751/50000000000000000000000000000000000000000000000000000000000000000000000000000000", + "-271848417292830239031711090616080219943440550124173594693788051154729518179791923/1000000000000000000000000000000000000000000000000000000000000000000000000000000" + ], + "146_or_more_incidences": [ + "-30262531052837597575979245954468209444176430776894579285748924460362703513260416889/50000000000000000000000000000000000000000000000000000000000000000000000000000000", + "-30262531052837597575979245954468209444176430776894579285748924460362703513241285631/50000000000000000000000000000000000000000000000000000000000000000000000000000000" + ] + }, + "exact_opposite_intersections": 81, + "finite_controls": { + "image_only_false_sharing_rejected": true, + "oblique_and_orthogonal_cases": [ + { + "E_form": 1, + "E_image": 1, + "head_residual_rank": 11, + "offdiagonal_rank": 1, + "principal_rank": 3, + "shared_each_side": [ + 1, + 1 + ] + }, + { + "E_form": 1, + "E_image": 1, + "head_residual_rank": 12, + "offdiagonal_rank": 0, + "principal_rank": 4, + "shared_each_side": [ + 2, + 1 + ] + }, + { + "E_form": 1, + "E_image": 1, + "head_residual_rank": 12, + "offdiagonal_rank": 0, + "principal_rank": 4, + "shared_each_side": [ + 1, + 2 + ] + }, + { + "E_form": 1, + "E_image": 1, + "head_residual_rank": 12, + "offdiagonal_rank": 0, + "principal_rank": 4, + "shared_each_side": [ + 2, + 2 + ] + }, + { + "E_form": 3, + "E_image": 1, + "head_residual_rank": 11, + "offdiagonal_rank": 1, + "principal_rank": 3, + "shared_each_side": [ + 1, + 1 + ] + }, + { + "E_form": 3, + "E_image": 1, + "head_residual_rank": 12, + "offdiagonal_rank": 0, + "principal_rank": 4, + "shared_each_side": [ + 2, + 1 + ] + }, + { + "E_form": 3, + "E_image": 1, + "head_residual_rank": 12, + "offdiagonal_rank": 0, + "principal_rank": 4, + "shared_each_side": [ + 1, + 2 + ] + }, + { + "E_form": 3, + "E_image": 1, + "head_residual_rank": 12, + "offdiagonal_rank": 0, + "principal_rank": 4, + "shared_each_side": [ + 2, + 2 + ] + }, + { + "E_form": 2, + "E_image": 2, + "head_residual_rank": 11, + "offdiagonal_rank": 1, + "principal_rank": 3, + "shared_each_side": [ + 1, + 1 + ] + }, + { + "E_form": 2, + "E_image": 2, + "head_residual_rank": 12, + "offdiagonal_rank": 0, + "principal_rank": 4, + "shared_each_side": [ + 2, + 1 + ] + }, + { + "E_form": 2, + "E_image": 2, + "head_residual_rank": 12, + "offdiagonal_rank": 0, + "principal_rank": 4, + "shared_each_side": [ + 1, + 2 + ] + }, + { + "E_form": 2, + "E_image": 2, + "head_residual_rank": 12, + "offdiagonal_rank": 0, + "principal_rank": 4, + "shared_each_side": [ + 2, + 2 + ] + }, + { + "E_form": 3, + "E_image": 2, + "head_residual_rank": 11, + "offdiagonal_rank": 1, + "principal_rank": 3, + "shared_each_side": [ + 1, + 1 + ] + }, + { + "E_form": 3, + "E_image": 2, + "head_residual_rank": 12, + "offdiagonal_rank": 0, + "principal_rank": 4, + "shared_each_side": [ + 2, + 1 + ] + }, + { + "E_form": 3, + "E_image": 2, + "head_residual_rank": 12, + "offdiagonal_rank": 0, + "principal_rank": 4, + "shared_each_side": [ + 1, + 2 + ] + }, + { + "E_form": 3, + "E_image": 2, + "head_residual_rank": 12, + "offdiagonal_rank": 0, + "principal_rank": 4, + "shared_each_side": [ + 2, + 2 + ] + }, + { + "E_form": 1, + "E_image": 3, + "head_residual_rank": 11, + "offdiagonal_rank": 1, + "principal_rank": 3, + "shared_each_side": [ + 1, + 1 + ] + }, + { + "E_form": 1, + "E_image": 3, + "head_residual_rank": 12, + "offdiagonal_rank": 0, + "principal_rank": 4, + "shared_each_side": [ + 2, + 1 + ] + }, + { + "E_form": 1, + "E_image": 3, + "head_residual_rank": 12, + "offdiagonal_rank": 0, + "principal_rank": 4, + "shared_each_side": [ + 1, + 2 + ] + }, + { + "E_form": 1, + "E_image": 3, + "head_residual_rank": 12, + "offdiagonal_rank": 0, + "principal_rank": 4, + "shared_each_side": [ + 2, + 2 + ] + }, + { + "E_form": 2, + "E_image": 3, + "head_residual_rank": 11, + "offdiagonal_rank": 1, + "principal_rank": 3, + "shared_each_side": [ + 1, + 1 + ] + }, + { + "E_form": 2, + "E_image": 3, + "head_residual_rank": 12, + "offdiagonal_rank": 0, + "principal_rank": 4, + "shared_each_side": [ + 2, + 1 + ] + }, + { + "E_form": 2, + "E_image": 3, + "head_residual_rank": 12, + "offdiagonal_rank": 0, + "principal_rank": 4, + "shared_each_side": [ + 1, + 2 + ] + }, + { + "E_form": 2, + "E_image": 3, + "head_residual_rank": 12, + "offdiagonal_rank": 0, + "principal_rank": 4, + "shared_each_side": [ + 2, + 2 + ] + } + ], + "rectangular_dimension": [ + 12, + 6 + ] + }, + "head_rank_lower_no_cross_any_cross_two_same_stage": [ + 444, + 555, + 666 + ], + "input_sha256": { + "bit/EFREE-CALLER.json.gz": "757b3523798f840bdb02028b23708c3416627a99ea09e7a3c4bcdc5cd0c7ce4b", + "bit/EFREE-RESULT.json": "a46b6c6040f75184cab5467656811ad988c216e3bc8e44d595a5015b6e49620b", + "bit/independent/interval_gate.py": "8dc2bc4c64cba3f83c664373984a075f1a14b4d53958084091345c8cab189dec", + "bit/retained/inputs/BIT-NATIVE-WORD.json.gz": "51203e7fc75ba10bd3ac3f8e675759f47e13d262bea66b6600d1e515095cad78" + }, + "literal_P": { + "1": 50340, + "2": 45108, + "3": 2232, + "4": 1692, + "5": 324, + "6": 3744, + "7": 804, + "14": 444, + "21": 444, + "28": 444, + "35": 444, + "42": 444, + "49": 444, + "56": 444 + }, + "literal_T": { + "2": 36, + "4": 900, + "6": 36, + "8": 15204, + "15": 444, + "22": 444, + "29": 444, + "36": 444, + "43": 444, + "50": 444, + "57": 444, + "64": 444, + "127": 222 + }, + "literal_moves_per_native": 2871, + "logical_idle_degrees": [ + 0, + 2, + 4, + 6, + 8, + 10, + 12, + 14, + 16, + 16, + 14, + 12, + 10, + 8, + 6, + 4, + 2, + 0 + ], + "optimistic_cross_lengths": [ + 16, + 16, + 7, + 7, + 7, + 7, + 6, + 6, + 6, + 6, + 5, + 5, + 5, + 5, + 4, + 4, + 4, + 4, + 3, + 3, + 3, + 3, + 2, + 2, + 2, + 2, + 1, + 1, + 1, + 1 + ], + "optimistic_no_cross_lengths": [ + 8, + 8, + 8, + 8, + 7, + 7, + 7, + 7, + 6, + 6, + 6, + 6, + 5, + 5, + 5, + 5, + 4, + 4, + 4, + 4, + 3, + 3, + 3, + 3, + 2, + 2, + 2, + 2, + 1, + 1, + 1, + 1 + ], + "per_stage_public_support": [ + [ + 0, + 1, + 19, + 20 + ], + [ + 0, + 1, + 2, + 19, + 20, + 21 + ], + [ + 0, + 1, + 2, + 3, + 19, + 20, + 21, + 22 + ], + [ + 0, + 1, + 2, + 3, + 4, + 19, + 20, + 21, + 22, + 23 + ], + [ + 0, + 1, + 2, + 3, + 4, + 5, + 19, + 20, + 21, + 22, + 23, + 24 + ], + [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 19, + 20, + 21, + 22, + 23, + 24, + 25 + ], + [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 19, + 20, + 21, + 22, + 23, + 24, + 25, + 26 + ], + [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 19, + 20, + 21, + 22, + 23, + 24, + 25, + 26, + 27 + ], + [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 19, + 20, + 21, + 22, + 23, + 24, + 25, + 26, + 27, + 28 + ], + [ + 0, + 10, + 11, + 12, + 13, + 14, + 15, + 16, + 17, + 18, + 19, + 29, + 30, + 31, + 32, + 33, + 34, + 35, + 36, + 37 + ], + [ + 0, + 11, + 12, + 13, + 14, + 15, + 16, + 17, + 18, + 19, + 30, + 31, + 32, + 33, + 34, + 35, + 36, + 37 + ], + [ + 0, + 12, + 13, + 14, + 15, + 16, + 17, + 18, + 19, + 31, + 32, + 33, + 34, + 35, + 36, + 37 + ], + [ + 0, + 13, + 14, + 15, + 16, + 17, + 18, + 19, + 32, + 33, + 34, + 35, + 36, + 37 + ], + [ + 0, + 14, + 15, + 16, + 17, + 18, + 19, + 33, + 34, + 35, + 36, + 37 + ], + [ + 0, + 15, + 16, + 17, + 18, + 19, + 34, + 35, + 36, + 37 + ], + [ + 0, + 16, + 17, + 18, + 19, + 35, + 36, + 37 + ], + [ + 0, + 17, + 18, + 19, + 36, + 37 + ], + [ + 0, + 18, + 19, + 37 + ] + ], + "scope": "Retain all 36 old native calls with two per stage, the target diagonal, uniform IDLE masks over 111 ports with a common rank-111 body derivative for each included stage, body-free head correction under inherited rank tariff, and otherwise derivative-free scalar adapters. Arbitrary linear copy/port mixing, rectangular contexts, and oblique projectors allowed.", + "status": "PROVED_NEGATIVE_DECLARED_UNIFORM_IDLE_REGROUPING", + "target": "10018846261809/2500000000000000" +} diff --git a/research/paired-bit-lanewise-idle-bound/SOURCES.json b/research/paired-bit-lanewise-idle-bound/SOURCES.json new file mode 100644 index 0000000000..08ead28e85 --- /dev/null +++ b/research/paired-bit-lanewise-idle-bound/SOURCES.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8", + "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/paired-query-only-bit/EFREE-CALLER.json.gz", + "usage": "input", + "git_blob": "f022272a8d51ede841778dec76e2bfb24b614d04", + "sha256": "757b3523798f840bdb02028b23708c3416627a99ea09e7a3c4bcdc5cd0c7ce4b" + }, + { + "path": "research/paired-query-only-bit/EFREE-RESULT.json", + "usage": "input", + "git_blob": "575f76487f9999ecc3e7b1b70f9f71bc582ef8a8", + "sha256": "a46b6c6040f75184cab5467656811ad988c216e3bc8e44d595a5015b6e49620b" + }, + { + "path": "research/paired-query-only-bit/independent/interval_gate.py", + "usage": "input", + "git_blob": "6d5a751dde7554b2bb3ccb9a958a3508d74ea155", + "sha256": "8dc2bc4c64cba3f83c664373984a075f1a14b4d53958084091345c8cab189dec" + }, + { + "path": "research/paired-query-only-bit/retained/inputs/BIT-NATIVE-WORD.json.gz", + "usage": "input", + "git_blob": "b718d6b2848215ad785022106dfa9f871a3d1c0c", + "sha256": "51203e7fc75ba10bd3ac3f8e675759f47e13d262bea66b6600d1e515095cad78" + } + ] +} diff --git a/research/paired-bit-lanewise-idle-bound/SOURCES.tsv b/research/paired-bit-lanewise-idle-bound/SOURCES.tsv new file mode 100644 index 0000000000..237377a23b --- /dev/null +++ b/research/paired-bit-lanewise-idle-bound/SOURCES.tsv @@ -0,0 +1,4 @@ +bit/EFREE-CALLER.json.gz 757b3523798f840bdb02028b23708c3416627a99ea09e7a3c4bcdc5cd0c7ce4b https://raw.githubusercontent.com/CrocSwap/integer-mult-bounds/e54523517d0f03e58352e647c403a5af3e525a57/research/paired-query-only-bit/EFREE-CALLER.json.gz +bit/EFREE-RESULT.json a46b6c6040f75184cab5467656811ad988c216e3bc8e44d595a5015b6e49620b https://raw.githubusercontent.com/CrocSwap/integer-mult-bounds/e54523517d0f03e58352e647c403a5af3e525a57/research/paired-query-only-bit/EFREE-RESULT.json +bit/retained/inputs/BIT-NATIVE-WORD.json.gz 51203e7fc75ba10bd3ac3f8e675759f47e13d262bea66b6600d1e515095cad78 https://raw.githubusercontent.com/CrocSwap/integer-mult-bounds/e54523517d0f03e58352e647c403a5af3e525a57/research/paired-query-only-bit/retained/inputs/BIT-NATIVE-WORD.json.gz +bit/independent/interval_gate.py 8dc2bc4c64cba3f83c664373984a075f1a14b4d53958084091345c8cab189dec https://raw.githubusercontent.com/CrocSwap/integer-mult-bounds/e54523517d0f03e58352e647c403a5af3e525a57/research/paired-query-only-bit/independent/interval_gate.py diff --git a/research/paired-bit-lanewise-idle-bound/TASK.json b/research/paired-bit-lanewise-idle-bound/TASK.json new file mode 100644 index 0000000000..0557536737 --- /dev/null +++ b/research/paired-bit-lanewise-idle-bound/TASK.json @@ -0,0 +1,64 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json", + "research/bit-gl3-mixed-targets-length10/README.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Construct the smallest exact identity in a newly specified legal operation alphabet.", + "Derive a target-specific relaxation bound for that same explicit alphabet." + ], + "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.", + "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.", + "allowed_variations": [ + "Choose a fixed larger register count or a specified nonabelian operation family." + ], + "scope_change_triggers": [ + "Remaining inside the already-excluded three-register abelian model.", + "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "changed", + "actual_scope": "The #7001 paired BIT caller with all 36 native LOCALs and all productive targets fixed, separately tariffed nonuniform IDLE masks, and arbitrary cross-copy and cross-port scalar context.", + "scope_change_reason": "The comparison changes the stage masks and their embedded lanes rather than the original card's register alphabet. It tests whether rearranging the existing body action can clear the BIT target.", + "bottleneck_link": "A shared body mask saves concave paid cost but restricts how much of the old q head can pass between opposite halves. The full invoice includes the residual head rank and all excess body incidence.", + "budget_minutes": 60, + "stop_rule": "Certify the full optimistic price over all extra body incidence and shared-stage counts. Stop on a strictly negative upper at the exact target.", + "outcome": "negative-result", + "evidence": "Exact all-81 opposite-stage support intersections, rectangular rank controls, full old invoice reconstruction, directed lane-wise tariff and independent rational interval confirmation.", + "author": "ToikY", + "ai_assistance": "OpenAI Codex and subagents materially assisted proof, implementation and independent verification.", + "open_questions": [ + { + "question": "Can a new shared primitive carry different body masks under one paid job while preserving the all-width endpoint?", + "why_it_matters": "The lane-wise theorem assumes a single separately charged common derivative for each mask.", + "first_step": "Specify a two-lane primitive with two different stage masks and derive its exact signed action, body and q rank accounting, paid charge, and restoration before extending it.", + "blocked_by": "No admitted coupled primitive, changed provider or complete application proof is available." + } + ] +} diff --git a/research/paired-bit-lanewise-idle-bound/VERIFY.json b/research/paired-bit-lanewise-idle-bound/VERIFY.json new file mode 100644 index 0000000000..b66d7a539b --- /dev/null +++ b/research/paired-bit-lanewise-idle-bound/VERIFY.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/paired-query-only-bit/EFREE-CALLER.json.gz", + "research/paired-query-only-bit/EFREE-RESULT.json", + "research/paired-query-only-bit/independent/interval_gate.py", + "research/paired-query-only-bit/retained/inputs/BIT-NATIVE-WORD.json.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/replay.py" + ], + "timeout_seconds": 120, + "checks": "Authenticate four exact sources, reconstruct the complete invoice and verify uniform and lane-wise rank prices, including independent arithmetic and failure controls." + } + ] +} diff --git a/research/paired-bit-lanewise-idle-bound/nonuniform.py b/research/paired-bit-lanewise-idle-bound/nonuniform.py new file mode 100644 index 0000000000..262c3c1528 --- /dev/null +++ b/research/paired-bit-lanewise-idle-bound/nonuniform.py @@ -0,0 +1,102 @@ +"""Directed price for arbitrary separately charged lane-wise BIT IDLE masks.""" + +from collections import Counter +from fractions import Fraction +from importlib.util import module_from_spec, spec_from_file_location +import json +from pathlib import Path +import sys + + +def module(path): + spec = spec_from_file_location(path.stem, path) + loaded = module_from_spec(spec) + spec.loader.exec_module(loaded) + return loaded + + +def run(root): + assert __debug__ + uniform = module(Path(__file__).with_name("verify.py")) + caller = uniform.load_json(root, "bit/EFREE-CALLER.json.gz") + result = uniform.load_json(root, "bit/EFREE-RESULT.json") + native = uniform.load_json(root, "bit/retained/inputs/BIT-NATIVE-WORD.json.gz") + gate_key = "bit/independent/interval_gate.py" + uniform.auth(root, gate_key) + gate = module(root / gate_key) + support = [{i for i, d in enumerate(caller["diagonal"]) if s in d["stages"]} + for s in range(1, 19)] + assert all(a & b == {0, 19} for a in support[:9] for b in support[9:]) + degrees = [len(a) - 4 for a in support] + T, P, native_paid, old_masks = uniform.literal_invoice(caller, result, native) + assert degrees == [sum(s in m for m in old_masks) for s in range(1, 19)] + N, body = caller["ports"], caller["body_rank"] + assert (caller["roles"], N, body, len(old_masks), sum(degrees)) == (38, 111, 7, 32, 144) + assert degrees == list(range(0, 18, 2)) + list(range(16, -2, -2)) + + ideal_lengths = sorted(map(len, old_masks), reverse=True) + uniform.majorant(degrees[:9], degrees[9:], 0, ideal_lengths) + # For scaled degrees each prefix capacity is linear between multiples + # of N. Thus repeating each original majorant row N times is exact. + half_bill = Counter({body * k: N * count for k, count in Counter(ideal_lengths).items()}) + paid_without_head = native_paid + half_bill + assert P == paid_without_head + Counter({1: 4 * N}) + signed = T.copy() + signed.subtract(paid_without_head) + + target = uniform.TARGET + + def H(rank): + return gate.power(rank, target) + + old_free_head = gate.moment(signed, target) + delta = gate.sub(gate.smul(H(body), 2), H(2 * body)) + assert delta[0] > 0 + min_extra_body = gate.sub(H(9 * body), H(8 * body)) + slack_penalty = gate.sub(min_extra_body, gate.add(gate.exact(5), gate.smul(delta, 9))) + assert slack_penalty[0] > 0 + + active_opposite_pairs = 8 * 8 + shared_per_stage = 2 * N + saturated_cross_budget = 16 * N + rank_at_K_zero = 4 * N + bounds = [] + for K in range(shared_per_stage + 1): + cross_credit = gate.smul(delta, min(active_opposite_pairs*K, saturated_cross_budget)) + bound = gate.sub(gate.add(old_free_head, cross_credit), H(rank_at_K_zero+K)) + assert bound[1] < 0 + bounds.append((K, bound)) + best_K, best_bound = max(bounds, key=lambda item:item[1][1]) + assert best_K == 28 + assert all(bound[1] < best_bound[0] for K,bound in bounds if K != best_K) + assert H(rank_at_K_zero+shared_per_stage+1)[0] > H(rank_at_K_zero+shared_per_stage)[1] + + # Positive baseline price control. Giving all cross-mask credit without + # any extra head-rank debit makes the relaxed upper positive. + free_sharing = gate.add(gate.sub(old_free_head, H(rank_at_K_zero)), + gate.smul(delta,saturated_cross_budget)) + assert free_sharing[0] > 0 + return { + "status": "PROVED_NEGATIVE_DECLARED_LANEWISE_IDLE_MODEL", + "input_sha256": uniform.PINS, + "target": str(target), + "native_calls": 36, + "minimum_physical_idles_incidence": sum(degrees)*N, + "opposite_support_checks": 81, + "extra_body_moment_lower_per_incidence": gate.show(min_extra_body), + "max_cross_credit_per_two_incidents": gate.show(delta), + "net_loss_lower_per_extra_incidence": gate.show(slack_penalty), + "base_head_capacity": rank_at_K_zero, + "old_paid_and_productive_match": True, + "directed_max_margin_K": best_K, + "directed_max_margin": gate.show(best_bound), + "directed_K_cases_checked": len(bounds), + "sample_directed_margins": {K: gate.show(bound) for K,bound in bounds if K in (0, 27, 28, 29, 222)}, + "larger_K_have_nonincreasing_upper": True, + "ignore_extra_cross_rank_positive_control": gate.show(free_sharing), + "scope": "Fixed #7001 productive profile and 36 native LOCALs, individually charged rank-seven-per-stage lane-wise masks, separate body-free heads, arbitrary rectangular scalar contexts. All extra body incidence covered.", + } + + +if __name__ == "__main__": + print(json.dumps(run(Path(sys.argv[1])), sort_keys=True, indent=2)) diff --git a/research/paired-bit-lanewise-idle-bound/nonuniform_audit.py b/research/paired-bit-lanewise-idle-bound/nonuniform_audit.py new file mode 100644 index 0000000000..c14710ebe3 --- /dev/null +++ b/research/paired-bit-lanewise-idle-bound/nonuniform_audit.py @@ -0,0 +1,88 @@ +"""Independent directed arithmetic for the separately tariffed nonuniform mask bound.""" +from collections import Counter +from fractions import Fraction as Q +from functools import cache +from hashlib import sha256 +import json +from pathlib import Path +import sys + +TARGET=Q(10018846261809,2500000000000000) +RESULT_SHA="a46b6c6040f75184cab5467656811ad988c216e3bc8e44d595a5015b6e49620b" +SCALE=10**29 + + +def directed(x,up): + n,d=(x*SCALE).as_integer_ratio() + return Q(-(-n//d) if up else n//d,SCALE) + + +@cache +def log_unit(x): + z=(x-1)/(x+1) + lo=2*sum(z**(2*j+1)/Q(2*j+1) for j in range(34)) + return lo,lo+2*z**69/(69*(1-z*z)) + + +@cache +def h(r): + e=r.bit_length()-1 + a,b=log_unit(Q(r,1<=0 else (x[1]*k,x[0]*k) + + +def run(source): + blob=source.read_bytes() + assert sha256(blob).hexdigest()==RESULT_SHA + r=json.loads(blob) + signed=Counter({int(k):n for k,n in r["targets"].items()}) + signed.subtract({int(k):n for k,n in r["paid"].items()}) + margin=Q(0),Q(0) + for rank,c in signed.items(): + margin=plus(margin,times(h(rank),c)) + delta=plus(times(h(7),2),times(h(14),-1)) + body_floor=plus(h(63),times(h(56),-1)) + penalty=plus(plus(body_floor,(Q(-5),Q(-5))),times(delta,-9)) + assert delta[0]>0 and 48*delta[0]>1 + assert penalty[0]>Q("1.51") + head_free=plus(margin,(Q(444),Q(444))) + + def bound(k): + return plus(plus(head_free,times(h(444+k),-1)),times(delta,min(64*k,1776))) + + k=28 + best=bound(k) + assert best[1]<0 + left,right=bound(k-1),bound(k+1) + assert left[1]>i&1 else 0 for i in range(size)] + + +def columns_to_rows(columns,size): + return [sum(1<>i&1) for i in range(size)] + + +def inverse(a): + size=len(a) + rows=[r|(1<<(i+size)) for i,r in enumerate(a)] + for i in range(size): + j=next(j for j in range(i,size) if rows[j]>>i&1) + rows[i],rows[j]=rows[j],rows[i] + for j in range(size): + if i!=j and rows[j]>>i&1: + rows[j]^=rows[i] + return [r>>size for r in rows] + + +def toy_stage(full_size, private, k, u, number_shared): + a,b,c,d=[1< Date: Wed, 11 Nov 2026 16:16:32 -0800 Subject: [PATCH 3/3] Reuse the pinned historical replay repair The guide already includes the #7000/#7001 navigation from #7147/#7156. Reuse d2e54af81f9dda6487636b79d4964a2385d89b2b from #7257, also verified in #7339, to run the historical audit at its inspected snapshot. Credit to unpaidmoon for the audit, Dennis for the historical gate, and Matarener for the pinned snapshot precedent. --- .../historical-selected-replay-gap/README.md | 6 +- .../SOURCES.json | 60 +++++++++--------- .../VERIFY.json | 31 +-------- .../historical-selected-replay-gap/verify.py | 63 ++++++++++++++----- 4 files changed, 82 insertions(+), 78 deletions(-) diff --git a/research/historical-selected-replay-gap/README.md b/research/historical-selected-replay-gap/README.md index 55d8cc3b49..36d9a873ca 100644 --- a/research/historical-selected-replay-gap/README.md +++ b/research/historical-selected-replay-gap/README.md @@ -69,7 +69,11 @@ python3 -B scripts/research_package.py --package research/historical-selected-re The direct command prints `PASS_HISTORICAL_SELECTED_REPLAY_GAP`. A registered replay prints `PASS_REGISTERED_RESEARCH_PACKAGE`. Both require Git history -containing the two inspected commits. +containing the two inspected commits and the source and manifest objects at +`2485805a6d47f36ea83ddde6327d453ac82d44dc`. The verifier uses a temporary +sparse checkout of that commit, checks the declared source digests there, and +uses its planner and manifest inventory. The recorded rejections and selection +therefore remain reproducible after later changes to the live Makefile or CI guide. ## Open next questions diff --git a/research/historical-selected-replay-gap/SOURCES.json b/research/historical-selected-replay-gap/SOURCES.json index c1010eec95..62bb8b3950 100644 --- a/research/historical-selected-replay-gap/SOURCES.json +++ b/research/historical-selected-replay-gap/SOURCES.json @@ -4,13 +4,13 @@ "files": [ { "path": "Makefile", - "usage": "input", + "usage": "provenance", "git_blob": "0d683a06b9e7ee162496108ce9a7c5d2ee94fccf", "sha256": "4f2d4f2dcd15139ec82658a975f85ed300897385f85799218539f4c8d60567da" }, { "path": "certificates/partial-swap-network.json", - "usage": "input", + "usage": "provenance", "git_blob": "eccafa830c16170c36faf93045ddf1f638f7bcd4", "sha256": "4c0b9d37e1034b2076e30a70f8e514416298c462d9ee98bc87fe6556b14df786" }, @@ -22,7 +22,7 @@ }, { "path": "docs/ci-verification.md", - "usage": "input", + "usage": "provenance", "git_blob": "63ba3e9aa8bdc5e942b56e34244b92b16f854085", "sha256": "c7d3027e9ad8bcbff68f07aa9576b30fb2f3c76c44d876d40c7fdbf4a3e2228a" }, @@ -34,163 +34,163 @@ }, { "path": "research/clifford-state-performance/SOURCE.json", - "usage": "input", + "usage": "provenance", "git_blob": "6f98a0061a5104dfab82c9e806f819b41811f684", "sha256": "396d0f08df24952248140d5c65c51b8c902ef1c580892ff7ea182890530f67ee" }, { "path": "research/community-batch1047-audit/CONTENT-COVERAGE.json", - "usage": "input", + "usage": "provenance", "git_blob": "5e0f92af463ec12c5e1dcc3effd44081a88af647", "sha256": "07a9daeaf2bda308a92e9a4684f13d5fc766c7772d74801fceb7f4599fdab226" }, { "path": "research/community-batch1099-audit/CONTENT-COVERAGE.json", - "usage": "input", + "usage": "provenance", "git_blob": "9e13266bf85e627f1b7dc225e9530ea69fd2c7f0", "sha256": "421e1211fb1897c45621dc6801c276e53f2e6f335583c9c9049e535f87c0a3b1" }, { "path": "research/community-batch932-audit/CONTENT-COVERAGE.json", - "usage": "input", + "usage": "provenance", "git_blob": "cc4d03eb59b9ab3f952735f7e88ff18c2d15d7af", "sha256": "184629cac91a5cfaca50330a88596008b824221433867dcf8117539c913c284a" }, { "path": "research/community-batch970-audit/CONTENT-COVERAGE.json", - "usage": "input", + "usage": "provenance", "git_blob": "8b9f4111badf7de5d97684799560b55110e9da79", "sha256": "23188ed920e38a54006cb883e181585620821c63bf7e8b5e05d32719417cc37e" }, { "path": "research/community-frontier741-audit/CONTENT-COVERAGE.json", - "usage": "input", + "usage": "provenance", "git_blob": "a5300d4e7a5381a3f443fc54c768ca6f0f236d68", "sha256": "3c820fb30e1b4d9bcfc6a7ab524375e5b2abd66b940af2c509146104f0bcd79c" }, { "path": "research/community-frontier890-audit/CONTENT-COVERAGE.json", - "usage": "input", + "usage": "provenance", "git_blob": "d7ff6d777b01d69b6ce84caf25d3b7e4a4d2f211", "sha256": "6b185a9902652f893f3ebd8ada92d2f11b6de6533a9a4d11718a8a4496101128" }, { "path": "research/community-hyperplane599-audit/SOURCE.json", - "usage": "input", + "usage": "provenance", "git_blob": "546f37d326d10a99910ae8f908e71ef768524d98", "sha256": "65099d764bfcc39bda5e4d9966783611b094c3522dbdd1435cd498d657a8ef8e" }, { "path": "research/community-k492-audit/SOURCE.json", - "usage": "input", + "usage": "provenance", "git_blob": "e538481e4cb16ed936d3195f2dfb5b5a9ca0a76b", "sha256": "2c0f4fa5bc150d05658af2e7c54c4d2c337dd52b7efd3d69530ae73bcbdf452a" }, { "path": "research/community-reconciliation92-audit/MANIFEST.json", - "usage": "input", + "usage": "provenance", "git_blob": "2a2e93685173d5f13cbb5abe740f5d90352e0228", "sha256": "5f501f3c118131e7d069f30ad77186eb2ad6961f9680a0ef105f4514ed41808a" }, { "path": "research/partial-swap-digest/baseline.py", - "usage": "input", + "usage": "provenance", "git_blob": "a2f0190704db83bd8ef48e46e723c49b925804fe", "sha256": "81e9af92cdf38243a540cdcff2062778e449467848d444da37a9553c12ca4c34" }, { "path": "research/r420-two-sided-basis/SOURCES.json", - "usage": "input", + "usage": "provenance", "git_blob": "5d718e11e62f4bcadecf1e02d6b61f87dbe190b0", "sha256": "d9810b0d139c5a1211fd2c1f0d142187cc1fca30026e1e7bc4f9ecfacf1596d1" }, { "path": "research/skip-clones/SOURCE.json", - "usage": "input", + "usage": "provenance", "git_blob": "8d1bb3b9c8189e35e5d8bfdfa632d7473e8be0d5", "sha256": "0b68e63e35a97ce6b0cdb6e291b88ebaa8f2dd4afb70b2498f10ee89428258dc" }, { "path": "research/split-skip/SOURCE.json", - "usage": "input", + "usage": "provenance", "git_blob": "2ab610b6ea2edd2865fda793ef2168b0c76afb4f", "sha256": "7c2b4646a3ecfef6f881da5c43e4bd0fa9a4d1b00548b8ab458d897e16735134" }, { "path": "scripts/historical-ci-inputs/Makefile", - "usage": "input", + "usage": "provenance", "git_blob": "aff68409021c9d401a6f8013b9dfd7dbcc30f2a8", "sha256": "ea8830dd79da493e2d75baf753d733ff7efbcf2b4794afe41fae0ac8f3055646" }, { "path": "scripts/historical-ci-inputs/ledger-batch932-run_isolated_tests.py", - "usage": "input", + "usage": "provenance", "git_blob": "65db599ab0b1dea0312c4ca048e0bd0f44c3736f", "sha256": "96ea543e6c707424afe247e77bd86c82152f90fc76a0773c4232145da5cdf8d1" }, { "path": "scripts/historical-ci-inputs/ledger-batch932-test_isolated_test_runner.py", - "usage": "input", + "usage": "provenance", "git_blob": "34820a8f24678f918f4d0e7a35380d8013fc3495", "sha256": "628391b6abfbc8674ceec1751867a4392f2cc0b5b66886243e139af86cf355ac" }, { "path": "scripts/historical-ci-inputs/ledger-batch970-verify_selected_result.py", - "usage": "input", + "usage": "provenance", "git_blob": "c755b76e0d44ba4917aa94440ebe54daefce5b2a", "sha256": "d7fd929726b326aeeaf0a3996475adec88eee9aac09ae0bebeeaa0bc1fc8f199" }, { "path": "scripts/historical-ci-inputs/ledger-frontier741-ci-verification.md", - "usage": "input", + "usage": "provenance", "git_blob": "7f3c012504187917a728b9fe87043f0fc8cd006a", "sha256": "a854022e0e1d5d4db4d60e586be3ea56005013ef14a1fc06d02bc06e8529c4b0" }, { "path": "scripts/historical-ci-inputs/partial-swap-context.json", - "usage": "input", + "usage": "provenance", "git_blob": "ad65114886bf34a4fd27e79f3be502389e689faa", "sha256": "833a9642f33aeab2ffea17ec9c6b82e0a953f90192b2c82e10bef21538dccba9" }, { "path": "scripts/historical-ci-inputs/partial-swap-network.json", - "usage": "input", + "usage": "provenance", "git_blob": "52075f2463f60af5e16571347f24274fce73a1ea", "sha256": "f3c4be597b2f2136da4ae2cc80c7454f63c90aa01f84e5b8131cee4dd55de815" }, { "path": "scripts/partial_swap/shared.py", - "usage": "input", + "usage": "provenance", "git_blob": "44a0e454c70f9c4b98e258b8443612e6a119904b", "sha256": "5a0646a50b9f3e8ea55168620a78e8853b0ab810517cefc8cfb8696aedee278a" }, { "path": "scripts/replay_historical_check.py", - "usage": "input", + "usage": "provenance", "git_blob": "1e92fff2782970ef71378f594f2350d245a4db26", "sha256": "5467619c78183d3adc82b0cb55af28e5c1a01fca2b0588677816244b53e2bafd" }, { "path": "scripts/research_package.py", - "usage": "input", + "usage": "provenance", "git_blob": "091b4c8f58bac9a9580d76025b887dc5c873d05f", "sha256": "e1256016e7f51827d04fa2179255989f639ae1d97afaa9c16265f85a0c6abd70" }, { "path": "scripts/run_isolated_tests.py", - "usage": "input", + "usage": "provenance", "git_blob": "a96ab35b315ce492e7fbbfd6c5ae211aa066b541", "sha256": "49eb56dd0fc0d8d8ffdb209970a7adf2176223580646f575d5c22e59543b381c" }, { "path": "scripts/verify_selected_result.py", - "usage": "input", + "usage": "provenance", "git_blob": "6882a4700e410dec569b51ae2eaf1a19cc019195", "sha256": "d6b305eac5b9bdb8172c469ad30a1655a60fa0aceac8b1bf610e1b73f51babd8" }, { "path": "tests/test_isolated_test_runner.py", - "usage": "input", + "usage": "provenance", "git_blob": "343b24abf6719b81805eba5a84c74e57634c8288", "sha256": "3a5470d0b139828b90e19bf9583ddeafcd69f8e34f2824664eb3a2958a52e34d" } diff --git a/research/historical-selected-replay-gap/VERIFY.json b/research/historical-selected-replay-gap/VERIFY.json index 98553e72ed..ab7efa3471 100644 --- a/research/historical-selected-replay-gap/VERIFY.json +++ b/research/historical-selected-replay-gap/VERIFY.json @@ -4,36 +4,7 @@ "python": "3.12", "requirements": [], "inputs": [ - "Makefile", - "certificates/partial-swap-network.json", - "docs/ci-verification.md", - "research/clifford-state-performance/SOURCE.json", - "research/community-batch1047-audit/CONTENT-COVERAGE.json", - "research/community-batch1099-audit/CONTENT-COVERAGE.json", - "research/community-batch932-audit/CONTENT-COVERAGE.json", - "research/community-batch970-audit/CONTENT-COVERAGE.json", - "research/community-frontier741-audit/CONTENT-COVERAGE.json", - "research/community-frontier890-audit/CONTENT-COVERAGE.json", - "research/community-hyperplane599-audit/SOURCE.json", - "research/community-k492-audit/SOURCE.json", - "research/community-reconciliation92-audit/MANIFEST.json", - "research/partial-swap-digest/baseline.py", - "research/r420-two-sided-basis/SOURCES.json", - "research/skip-clones/SOURCE.json", - "research/split-skip/SOURCE.json", - "scripts/historical-ci-inputs/Makefile", - "scripts/historical-ci-inputs/ledger-batch932-run_isolated_tests.py", - "scripts/historical-ci-inputs/ledger-batch932-test_isolated_test_runner.py", - "scripts/historical-ci-inputs/ledger-batch970-verify_selected_result.py", - "scripts/historical-ci-inputs/ledger-frontier741-ci-verification.md", - "scripts/historical-ci-inputs/partial-swap-context.json", - "scripts/historical-ci-inputs/partial-swap-network.json", - "scripts/partial_swap/shared.py", - "scripts/replay_historical_check.py", - "scripts/research_package.py", - "scripts/run_isolated_tests.py", - "scripts/verify_selected_result.py", - "tests/test_isolated_test_runner.py" + "scripts/research_package.py" ], "commands": [ { diff --git a/research/historical-selected-replay-gap/verify.py b/research/historical-selected-replay-gap/verify.py index 83b995941a..9d266c5a4e 100644 --- a/research/historical-selected-replay-gap/verify.py +++ b/research/historical-selected-replay-gap/verify.py @@ -6,8 +6,10 @@ """ import hashlib import importlib.util +import json import subprocess import sys +import tempfile from pathlib import Path ROOT = Path(__file__).resolve().parents[2] @@ -61,31 +63,47 @@ def require(ok, message): raise SystemExit(message) -def load_checker(): - path = ROOT / "scripts/replay_historical_check.py" - spec = importlib.util.spec_from_file_location("historical_selected_replay_gap_checker", path) +def load_module(path): + spec = importlib.util.spec_from_file_location(path.stem, path) module = importlib.util.module_from_spec(spec) spec.loader.exec_module(module) return module +def checkout_snapshot(snapshot, sources, runner, env): + paths = [runner.canonical_relative_path(row["path"]) for row in sources["files"]] + git = ["git", "-c", "maintenance.auto=false", "-c", "gc.auto=0", + "-c", "core.autocrlf=false"] + subprocess.run([*git, "clone", "--quiet", "--shared", "--no-tags", "--no-checkout", + "--", str(ROOT), str(snapshot)], cwd=ROOT, env=env, check=True) + subprocess.run([*git, "update-ref", "--no-deref", "HEAD", INSPECTED], + cwd=snapshot, env=env, check=True) + # The pinned planner reads omitted manifests from the sparse HEAD/index. + patterns = "".join(f"/{path.as_posix()}\n" for path in paths) + subprocess.run([*git, "sparse-checkout", "set", "--no-cone", "--stdin"], + cwd=snapshot, env=env, input=patterns.encode("utf-8"), check=True) + subprocess.run([*git, "read-tree", "-mu", "HEAD"], cwd=snapshot, env=env, check=True) + for path, row in zip(paths, sources["files"], strict=True): + require(hashlib.sha256((snapshot / path).read_bytes()).hexdigest() == row["sha256"], + "historical checkout source digest changed: " + path.as_posix()) + + def entries(checker): for name, config in checker.CONFIG.items(): for entry in [config, *config.get("additional_inputs", [])]: yield name, entry -def reject(checker, entry): +def reject(root, checker, entry): try: - checker.authenticated_input(ROOT, entry) + checker.authenticated_input(root, entry) except ValueError as exc: return str(exc) raise SystemExit("historical input was admitted: " + entry["path"]) -def main(): - require(not sys.flags.optimize, "assertions must stay enabled") - checker = load_checker() +def check_snapshot(root, env): + checker = load_module(root / "scripts/replay_historical_check.py") selected = [entry for name, entry in entries(checker) if name == "tooling-ledger" and entry["path"] == SELECTED_PATH] require(len(selected) == 1, "selected-result checker overlay is not unique") @@ -94,7 +112,7 @@ def main(): require(entry["accepted_live_sha256"] == [SELECTED_ACCEPTED], "accepted selected-checker successors changed") frozen = (checker.INPUTS / entry["input"]).read_bytes() - live = (ROOT / SELECTED_PATH).read_bytes() + live = (root / SELECTED_PATH).read_bytes() require(hashlib.sha256(frozen).hexdigest() == SELECTED_PIN, "frozen selected checker bytes changed") require(hashlib.sha256(live).hexdigest() == SELECTED_LIVE, "live selected checker digest changed") require(SELECTED_LIVE not in (SELECTED_PIN, SELECTED_ACCEPTED), "live checker was already admitted") @@ -102,7 +120,7 @@ def main(): # live successor, not a broken comparison. require(SELECTED_PIN in (SELECTED_PIN, *entry["accepted_live_sha256"]), "pin membership control failed") - require(reject(checker, entry) == REJECTIONS[SELECTED_PATH][1], + require(reject(root, checker, entry) == REJECTIONS[SELECTED_PATH][1], "selected checker rejection text changed") counts = {path: 0 for path in REJECTIONS} @@ -110,7 +128,7 @@ def main(): for _name, item in entries(checker): if item["path"] not in REJECTIONS: continue - message = reject(checker, item) + message = reject(root, checker, item) counts[item["path"]] += 1 messages.setdefault(item["path"], message) for path, (count, message) in REJECTIONS.items(): @@ -118,20 +136,31 @@ def main(): require(messages[path] == message, "rejection text changed for " + path) require(sum(counts.values()) == 19, "rejection total changed") ci = [item for _name, item in entries(checker) if item["path"] == CI_PATH] - require(len(ci) == 1 and hashlib.sha256((ROOT / CI_PATH).read_bytes()).hexdigest() == CI_LIVE, + require(len(ci) == 1 and hashlib.sha256((root / CI_PATH).read_bytes()).hexdigest() == CI_LIVE, "selected CI note digest changed") diff = subprocess.check_output( - ["git", "diff", "--name-only", PARENT, INSPECTED], cwd=ROOT, text=True) + ["git", "diff", "--name-only", PARENT, INSPECTED], cwd=root, env=env, text=True) changed = sorted(name for name in diff.splitlines() if name) require(changed == CHANGED, "inspected commit diff changed") - sys.path.insert(0, str(ROOT / "scripts")) - from research_package import plan_details - details = plan_details(ROOT, set(changed)) + planner = load_module(root / "scripts/research_package.py") + details = planner.plan_details(root, set(changed)) require([row["package"] for row in details] == PLAN_PACKAGES, "helper plan selection changed") matched = {name for row in details for names in row["causes"].values() for name in names} require(sorted(set(changed) - matched) == UNMATCHED, "unmatched plan paths changed") - require(plan_details(ROOT, set()) == [], "empty change set selected a package") + require(planner.plan_details(root, set()) == [], "empty change set selected a package") + + +def main(): + require(not sys.flags.optimize, "assertions must stay enabled") + sources = json.loads(Path(__file__).with_name("SOURCES.json").read_bytes()) + require(sources["base_commit"] == INSPECTED, "historical checkout base changed") + runner = load_module(ROOT / "scripts/research_package.py") + env = runner.git_source_env() + with tempfile.TemporaryDirectory(prefix="historical-selected-replay-") as temporary: + snapshot = Path(temporary) / "snapshot" + checkout_snapshot(snapshot, sources, runner, env) + check_snapshot(snapshot, env) print("PASS_HISTORICAL_SELECTED_REPLAY_GAP") print("selected_checker_live=" + SELECTED_LIVE) print("rejections=19 distinct_paths=7 plan_packages=9")