diff --git a/research/inverse-certificate-bit-bounds/PROOF.md b/research/inverse-certificate-bit-bounds/PROOF.md new file mode 100644 index 0000000000..553005f225 --- /dev/null +++ b/research/inverse-certificate-bit-bounds/PROOF.md @@ -0,0 +1,260 @@ +# Rational size and bit cost of complete inverse-circuit certificates + +Ali Romman, with substantial OpenAI Codex assistance. Apache-2.0. +This is a written proof with exact finite corroboration, not proof-kernel or +independent human acceptance. + +## 1. Contract and result + +Use the complete register grammar of Krzysztof Wójt's +[PR #5262](https://github.com/CrocSwap/integer-mult-bounds/pull/5262), pinned at +`6f92ccf1e61c4668c8ee687bd1df8b42932b8759`. Its code and proof are retained +unchanged in vendor. There are r independent input roles, s named invertible +operators and q unary occurrences across both programs. Put D=r+q. Every +output role is retained. Queries read the old source, including aliases. +Only named-generator inverse relations are imposed. + +Coefficients are explicit rational numbers. The executable budget interface +accepts JSON integers and strings of the form signed-integer or +signed-integer/positive-integer. It rejects decimal and exponent strings +before the source parser expands them. Fractions need not be reduced. +Input size counts the original numerators, denominators, instruction and +name encoding. An external conversion from a compressed scalar syntax is +separate work. This restriction does not change the retained source parser. + +**Theorem.** On these inputs, the unchanged rational producer and its separate +checker, applied to the produced certificate, take polynomial bit time and +space. Both an equality certificate and a shortest nonzero coefficient word +have polynomial encoding size. Explicit rational-height bounds and a coarse +operation bound are given below. No unit-cost rational-arithmetic assumption +is needed. This closes a stated limitation of the source; weighted-automata +equivalence and determinant bounds are classical. + +Python's decimal integer-string limit must be disabled for unrestricted +explicit coefficients. The registered process uses the standard option +`-X int_max_str_digits=0`. This changes neither arithmetic nor source code. +The result is a mathematical complexity bound, not a runtime or optimality +claim. It does not support inverses of sums, additional native relations, +physical tapes, suppliers or a new complete kappa. + +## 2. Integer parameters + +Reduce each input coefficient c to n_c/d_c with d_c positive. Count each +written coefficient occurrence, including zero and repeated occurrences. +Set Q to the product of all d_c; an empty product is one. For an instruction, +set beta=max(1,sum |n_c|) for a scalar linear assignment, beta=1+|n_c| for +a query, and beta=1 for an apply. Let G be the product of all beta over both +programs. Thus Q,G are positive integers. Define + + R = Q^D, + K = (1+D G)^D, + M = 2 D G K R, + Z = R^(D+1), + N = D^D M^(D+1), + Delta = D! N^D. (1) + +All these integers have polynomial binary length in the explicit input. +They are proof quantities; the budget calculator returns logarithmic bounds +and does not allocate N, Z or Delta. + +For a rational x in lowest terms, its height is the maximum binary length of +its numerator's absolute value and positive denominator. Zero has height one. +The calculator uses integer bit_length as a strict upper bound on log2 for +positive integers. With bD=bit_length(D), bQ=bit_length(Q), bG=bit_length(G), +it returns + + bM = 1+bD+bG+D(1+bD+bG)+D bQ, + bN = D bD+(D+1)bM+1, + bDelta = D(bD+bN)+1, + bCoeff = (D+1)bD+(D+2)bM+1. (2) + +These bound, respectively, model entries, candidate path rows, stored +normalized rows and coordinates, and nonzero projected coefficients. +They are sufficient bounds, not minimal lengths. + +## 3. Scalar compilation and the common denominator + +The source represents each register by a row in r+q atoms. A unary call adds +one atom. A scalar instruction takes a linear combination of prior rows; +an apply replaces a row by a unit row; a query adds one coefficient times a +new unit row. Induction with the instruction beta factors bounds each +register or dependency row's absolute row sum by G. A final difference row +has absolute row sum at most 2G. In each scalar dependency path, a written +coefficient occurrence is used at most once. Therefore every denominator +in the dependency rows and final rows divides Q. Sums preserve divisibility +by this common denominator. This argument allows repeated source terms and +self-source assignments. + +Use the source proof's strictly lower triangular dependency matrix E and +unary matrices A_a. Entries of E and A_a have magnitude at most G and +denominator dividing Q; inverse feedback contributes the integer -1. +The constant solve and compiled model are + + H=(I-E)^(-1)=I+E+...+E^(D-1), + V=H V0, T_a=H A_a, U=left_final-right_final. + +Each H entry has magnitude at most sum_(j=0)^(D-1)(DG)^j <= K and denominator +dividing Q^(D-1). It follows that all U,T_a,V entries have denominator +dividing R. Their magnitudes are at most max(2G,DKG,K). Thus RU,RT_a,RV are +integer matrices with entries of magnitude at most M. This also covers +intermediate completed rows of the source's triangular recurrence. No +Gaussian elimination or inverse of a matrix with variable entries occurs +in this compilation step. + +The independent checker constructs E,H and A_a separately. The same bounds +apply to that reconstruction. The new audit compares both models and checks +the common denominator by exact modular powers; it does not replace either +compiler. + +## 4. Path rows and output coefficients + +The breadth-first search accepts at most D independent path rows U_o T_w. +Their lengths are less than D. Every candidate successor has length at most +D. These are the source's reachability facts; they are not new shortest-word +claims. A length-k row has denominator dividing R^(k+1). After scaling all +candidate rows by Z, it is integral with entries bounded by + + R^(D-k) D^k M^(k+1) <= D^D M^(D+1) = N, 0<=k<=D. (3) + +Here M>=R. Hence each reduced path-row numerator and denominator is at most +N, since Z<=N. This proves the bN bound. + +A projected coefficient U_o T_w V_i uses one more matrix. Its common +denominator and integer numerator are bounded by + + R^(k+2), D^(k+1) M^(k+2). + +The bCoeff bound in (2) is sufficient for every accepted path and the emitted +nonzero coefficient. Infinite inverse-series tails do not change these +finite path lengths. No expansion of all words is required. + +## 5. Exact elimination does not hide exponential bit growth + +Scale every accepted and candidate path row by the same Z. Each integer +entry now has magnitude at most N. Consider the first j independent rows +and their chosen pivot columns, in the order used by the source. Their +j by j integer pivot matrix P_j has nonzero determinant. Every minor of +size at most D is bounded in absolute value by Delta, by the permutation +formula for a determinant. Pivot columns need not be in increasing order. + +For a candidate row z/Z, elimination against these j rows solves the pivot +coordinates by Cramer's rule: + + removed = z[pivots] P_j^(-1). + +Its numerators and denominator are j by j determinants, bounded by Delta. +For j0. Use the exact special-orthogonal Cayley +matrices O_a(t) of [PR #5315](https://github.com/CrocSwap/integer-mult-bounds/pull/5315). +Give one chosen input role e_(d-1), and give all other roles zero. Let f be +coordinate zero of any chosen output difference. This concrete input does +not change the universal grammar's independent-role contract. + +Let C be the product of the positive reduced denominators of **every** scalar +coefficient occurrence in both programs. Include query coefficients and every +term of a linear assignment, even repeated roles or zero coefficients. Then + + f != 0 implies |f| >= eta = 1/[C (3B)^(dq)]. (1) + +A dyadic implementation below computes fhat with |fhat-f|<=eta/4. Hence + + f=0 iff |fhat|<=eta/4, + f!=0 implies |fhat|>=3eta/4. + +The threshold eta/2 therefore decides this selected endpoint exactly. It +does not need an exact endpoint replay or coefficient certificate as its +decision oracle. A false universal program identity still needs the source +producer's distinguishing word/input/output, or another search for one. +A zero at one chosen tuple is not a universal equality certificate. + +## 1. Integer denominators + +For each path label a, write K_a for its skew adjacency matrix and + + M_a = 2B I - A K_a, P_a = 2B I + A K_a, + O_a = M_a^-1 P_a. + +M_a and P_a have integer entries. Each column has squared Euclidean norm at +most 4B^2+2A^2 <9B^2. Hadamard's determinant bound gives + + 1 <= D_a = det(M_a) <= (3B)^d. + +The determinant is positive: M_a is invertible on the real parameter line, +its determinant is continuous, and at A=0 it is (2B)^d>0. Also P_a=M_a^T, +so its determinant is the same D_a. The adjugate formula shows that every +entry of O_a and O_a^-1 is an integer divided by D_a. Cancellation can only +reduce a reduced denominator. + +Maintain one common integer denominator for all registers on one program +side. At a linear assignment multiply it by the product of the denominators +of that assignment's coefficients. At an apply multiply it by D_a. At a +query multiply it by D_a times the scalar denominator. The unchanged +registers and old destination can use this same denominator. Old source +values also have it before the assignment, including on alias. This proves +by induction that a common denominator for the two endpoint vectors divides + + C product_(all q occurrences) D_(label). + +The endpoint difference has the same divisibility property after the two +side denominators are multiplied. A nonzero numerator is a nonzero integer. +The displayed product is at most C(3B)^(dq), which proves (1). The actual +common denominator need not divide the larger numeric bound C(3B)^(dq); +only this inequality is used. + +For the source witness grid with cap t0=a/b and L=dq, its rational points +have reduced denominator B<=b(L+1). Thus a uniform separation bound over the +whole grid follows by replacing B in (1) with b(dq+1). No floating root +separation or generic numerical noncancellation premise is needed. + +## 2. Complete register gains + +Use the maximum absolute coordinate over the entire r-register bank. Every +entry of an orthogonal matrix has absolute value at most one, so its row +absolute sum is at most d. Assign each instruction the following two bounds: + +| Instruction | beta | gamma | +|---|---:|---:| +| linear dst = sum c_j src_j | max(1, sum abs(c_j)) | 0 | +| apply G_a or G_a^-1 | d | d | +| query dst += c G_a^(+/-1) src | 1+d abs(c) | d abs(c) | + +Beta bounds the exact map on the whole bank; beta>=1 also covers unchanged +roles. Gamma bounds the effect of rounding each operator entry by at most h. +Define G as the product of all beta values in both programs, and Gamma as +the largest gamma (zero for no calls). G>=1. + +Truncate each exact forward matrix entry toward zero to the h=2^-p grid. +Use the transpose of that integer table for its inverse call. Since exact +inverse equals transpose, this is the same entrywise truncation of the +actual inverse. Each stored entry still has absolute value at most one. +Read all instruction sources before writing the destination. Multiply and +sum exactly, keep scalar coefficients exact, then truncate each new data +coordinate once toward zero to the same grid. + +This operation does not increase the absolute value of a coordinate. By +induction each computed bank has norm at most the product of its previous +beta values, hence at most G. This bound includes arbitrary scalar gains, +all helper roles, and self-source queries. It does not assume that a rounded +map is linear or that its stored inverse undoes its stored forward map. + +Let E_i be the bank error on one program side after instruction i. The exact +map contributes at most beta_i E_(i-1). Entry quantization on the computed +input contributes at most gamma_i h G. The final data truncation adds at +most h. Thus + + E_i <= beta_i E_(i-1) + (gamma_i G+1)h. + +Every suffix product of beta values is at most G. Sum both program errors, +using their combined instruction count m. Every returned coordinate of the +endpoint difference therefore has error at most + + E = m G (Gamma G+1) h. (2) + +Choose an integer p>=0 with + + 2^p >= 4 max(1, m G (Gamma G+1)) C(3B)^(dq). + +Then E<=eta/4. This also covers an empty program pair, where m=0 and its +endpoint difference is exactly zero. Equations (1) and (2) prove the +threshold decision and the claimed separation between its two cases. + +## 3. Executable and arithmetic boundary + +`detector.py` uses no exact endpoint or Magnus producer. It takes the program, +word, parameter, input role and output role. It forms each rational Cayley +matrix from the retained tridiagonal basis action, quantizes the entries, +and replays both complete programs with integers. A query computes its old +sum before one final division. A linear assignment uses exact rational +scalar arithmetic before one truncation. Every dirty output is retained. + +For alphabet size s the code stores 2sd^2 matrix-entry slots. The dense +replay pays qd^2 integer matrix products and md coordinate truncations, +plus all linear/query scalar products and additions. Matrix formation, +source parsing, gain/denominator calculation, allocation and returned banks +are additional work. There is no claim that this dense numerical method is +faster than exact rational replay or an admitted native primitive. + +After the word is supplied, the required fractional precision satisfies + + p = O(log C + dq(1+log B) + log(m+1) + + log G + log(Gamma G+1)). + +This is polynomial in the explicit program/word lengths and scalar/parameter +binary input sizes. Exact scalar sums and products give polynomial-size +representations of C, G and Gamma. Integer path matrices have entry size +O(log B); their minors have O(d(1+log B+log d)) bits. The tridiagonal basis +solves use ratios of these minors and polynomially many exact operations. +The stored data have magnitude at most G, so their integers use at most +p+O(log G) bits. Dot products add at most O(log d) bits; exact scalar sums +use coefficient denominators whose product divides C. This bounds the +arithmetic bit sizes in the supplied detector polynomially as well. +This statement is for this detector after a word is given. It is not a new +bit-complexity analysis of the upstream coefficient producer. + +## Evidence and limits + +The verifier uses the exact tridiagonal endpoint and a separately transcribed +dense Gaussian-inverse interpreter only as test oracles. It compares every +returned coordinate with (2), not just the threshold verdict. Equal programs, +exact cancelling grid points and failed identities are separate cases. Tiny +parameters, a scalar discrepancy 2^-80, scalar gains 2^100, dirty returns, +aliased queries and a delayed inverse series test different terms in the +bound. Corrupted code tests remove scalar denominators, parameter denominator +size, cumulative gains or the inverse transpose. + +The guard is deliberately conservative. It is not a least precision, an +IEEE floating-point guarantee, or a proof that an unspecified numerical +library respects these rounding rules. It adds no finite native alphabet, +Clifford relation, physical tape tariff, supplier admission or complete kappa +improvement. The selected frontier and inherited native/analytic obligations +remain unchanged. No independent human or proof-kernel review is claimed. + +## Attribution + +Ali Romman's [PR #5315](https://github.com/CrocSwap/integer-mult-bounds/pull/5315), +consumed at `9bebc267c4608e51fcc94a543b8e0d66077cdfbb`, supplies the rational +orthogonal realization, literal action and tests retained in `vendor/`. +Krzysztof Wójt (@krzysztofwojt) supplies the inverse compiler and shortest-word +proof in [PR #5262](https://github.com/CrocSwap/integer-mult-bounds/pull/5262). +The retained notices credit zxv's +[PR #5235](https://github.com/CrocSwap/integer-mult-bounds/pull/5235), the +dirty-echo/tensor/phase lineage and classical rational-series methods. +Cayley transforms, Hadamard's determinant inequality and forward-error +propagation are classical. This result binds their explicit constants to +this complete register grammar and one literal dyadic consumer. diff --git a/research/inverse-certificate-bit-bounds/vendor/UPSTREAM-PROOF.md b/research/inverse-certificate-bit-bounds/vendor/UPSTREAM-PROOF.md new file mode 100644 index 0000000000..d2433c24ca --- /dev/null +++ b/research/inverse-certificate-bit-bounds/vendor/UPSTREAM-PROOF.md @@ -0,0 +1,246 @@ +# Compact certificates with actual inverse calls + +This is a scoped written proof for the register grammar below. The implementation +and finite tests corroborate it; there is no proof-assistant or independent human +verification claim. The contribution answers the inverse-frontend question in +[zxv's PR5235](https://github.com/CrocSwap/integer-mult-bounds/pull/5235), pinned at +`48976daa4dce59b4867ef046da72a370e389925d`. That package supplies the +independent-operator register bridge, invariant certificates and unipotent +witness method. Here inverse occurrences denote the **actual inverse of the +same generator**, and therefore need a different, cyclic realization and a +sound passage from formal series to arbitrary invertible substitutions. + +Recognizable rational series, the Magnus substitution and weighted-automata +equivalence are classical. See Stefan Kiefer, +[Notes on Equivalence and Minimization of Weighted Automata](https://arxiv.org/abs/2009.01217), +and Retakh, Reutenauer and Vaintrob, +[Noncommutative rational functions and Farber's invariants of boundary links](https://arxiv.org/abs/math/0004112), +Remark 2.3 and Proposition 2.4, which recall the Magnus embedding and the +Schutzenberger/Fliess characterization. We claim a project-specific interface, +explicit state bound and executable certificate bridge, not a new general +automata/PIT algorithm or a new Magnus theorem. The argument below is +self-contained and does not require the injectivity theorem for the group +algebra embedding. + +## 1. Grammar and statement + +Fix a field K, a finite alphabet of independently chosen invertible operators +G_a on a common finite-dimensional K-vector space, and r >= 1 named registers. +All r initial vectors are independent; no dirty helper is assumed zero. +A program is a finite sequence of: + +1. scalar linear assignment to a register, with all sources read before the + assignment, including when the destination is also a source; +2. `dst <- G_a^s dst`, where s is +1 or -1; +3. `dst <- dst + c G_a^s src`, with the old source and destination, also when + `src == dst`. + +All scalar coefficients lie in K. Compare two such programs on the same +ordered roles and alphabet, returning **every** final register. Let q be the +total number of unary occurrences in both programs, including queries, inverse +occurrences, and queries with coefficient zero. Put D = r + q. + +**Theorem.** There are effectively constructed scalar matrices +U in K^(r x D), V in K^(D x r), and T_a in K^(D x D) such that: + +- the complete endpoint difference, expanded at G_a = I + Y_a, has coefficient + matrix U T_a1 ... T_ak V at every word a1...ak, including k=0; +- the programs have equal complete endpoints for every payload dimension and + every invertible substitution if and only if all these coefficients vanish; +- equality has a finite certificate consisting of at most D path rows, their + initial-span coordinates and transition-closure coordinates; +- failure has a nonzero coefficient word of length k < D and an explicit + simultaneous unipotent substitution in dimension k+1 <= D witnessing it. + +The search below finds a shortest nonzero coefficient word. The independent +certificate checker certifies its nonzeroness, **not shortestness**. It does +not claim a least-dimensional witness among arbitrary invertible matrices. + +The executable supports K=Q and prime fields F_p with p <= 2^31-1. Rational +input denominators must be nonzero in F_p. The written theorem holds over any +field. There are no commutation, involution, Clifford, adjoint or other +relations; a failure need not persist after imposing such extra relations. +Only inverses of named generators are in the grammar, not inverses of arbitrary +operator sums or matrices of operators. + +## 2. One atom per unary occurrence + +Create r leaf atoms x_i. Maintain each register as a scalar row in the atom +list. Each linear instruction updates that row. Each unary occurrence with +pre-instruction source row e creates a fresh atom z_j = G_a^s (e z). +An apply instruction replaces the destination by z_j; a query adds c z_j to +the old destination. Even a self-source query takes e before the update. + +Compile the two programs with separate mutable register tables but the same r +leaf atoms. Append all unary atoms from both sides to one list. Their source +rows use earlier atoms only. Thus there are exactly D atoms. U is the +left-minus-right matrix of all final role expressions; it retains each input +role and each output role independently. An atom is an algebraic compiler +record, not a clean physical register or a free allocation. + +Work in noncommutative formal series K<> and put G_a=1+Y_a. Its inverse +is the formal geometric series, well-defined over every characteristic. For a +forward occurrence and an inverse occurrence, respectively, the defining +equations are + + z_j = e z + Y_a e z, + z_j = e z - Y_a z_j. + +The second equation follows by multiplying z_j=(1+Y_a)^(-1)e z by 1+Y_a. +It is the inverse-aware step: a negative diagonal feedback term, not a new +independent operator label and not a truncated polynomial expansion. + +Let E have row e at every unary atom and zero leaf rows. Let V0 embed the r +input roles at the leaf rows. For each a, let A_a have row e at a forward +a-occurrence, row -unit_j at an inverse a-occurrence, and zero elsewhere. +Then, with scalar matrices commuting entrywise with the series letters, + + z = E z + V0 x + sum_a Y_a A_a z. + +E is strictly lower triangular. Consequently H=(I-E)^(-1) is the finite +scalar matrix I+E+...+E^(D-1). Set V=H V0 and T_a=H A_a. The equations become + + z = V x + sum_a Y_a T_a z. + +This system has a unique formal solution: each coefficient of positive length +is determined by shorter coefficients. Iterating gives exactly + + [a1 ... ak](U z) = U T_a1 ... T_ak V. + +Word order is matrix-product order: `[B,A]` means BA and applies A first. +The inverse feedback means T_a need not be nilpotent. Infinite nonzero tails +are allowed even though D is finite. + +The producer uses the equivalent triangular recurrences + + V_j = e V, + (T_b)_j = e T_b + 1_(b=a) e (forward), + (T_b)_j = e T_b - 1_(b=a) unit_j (inverse), + +where e only reads earlier rows. The checker instead reconstructs E,A_a and +the triangular inverse H. These are separately transcribed compilers. + +## 3. Finite closure certificates + +A positive certificate provides b <= D path rows B_l=U_o T_w and scalar +coordinate matrices L and C_a satisfying + + U = L B, B T_a = C_a B for every a, B V = 0. + +These finite equations imply U T_w V=0 for every word by induction. +Independence, minimality and reachability of B are unnecessary for soundness; +the supplied paths merely specify B compactly and bind it to the program. + +Conversely, if every coefficient is zero, the reachable space +R=span{U_o T_w} has dimension at most D, is transition-stable and annihilates V. +Choose a basis from reachable path rows. Its initial and closure coordinates +give the displayed certificate. A basis of paths shorter than D exists: +R_k, the span of paths of length at most k, cannot stop increasing and later +increase again, since R_(k+1)=R_k+sum_a R_k T_a. If R_0=0, everything is zero; +otherwise at most D-1 strict increases are possible. + +Breadth-first search tests output projections of accepted independent path +rows and appends their independent successors. Rejected dependent rows add no +possible earlier distinguishing length: their expression uses accepted rows +of no greater length, whose successors span their successors. Hence a first +nonzero projection occurs at a shortest coefficient word, of length < D. +Exact elimination is in the producer only. The checker rebuilds the path rows +and verifies the displayed equations, or verifies one claimed nonzero +coefficient on failure. No acceptance check relies on Python `assert`. + +With alphabet size s, dense production takes polynomially many field +operations (O(s D^3) for reachable-space search and coordinates, plus parsing +and compilation). Coordinate storage is O(s D^2+rD), with at most O(D^2) +path letters. The simple checker may rebuild each path from scratch, costing +O(D^4+sD^3) field operations. These are arithmetic bounds, not bounds on +rational coefficient bit lengths or a practical scaling guarantee. + +## 4. Why zero series implies every invertible substitution + +Formal series cannot be evaluated directly at arbitrary matrices by summing an +infinite series. The following argument supplies the missing step. + +Fix any dimension n and any tuple of invertible matrices M_a over K. Introduce +one central indeterminate t and substitute + + G_a(t) = I + t(M_a-I). + +Each G_a(t) has determinant with constant term 1, so is invertible over K(t) +and its inverse has a well-defined expansion in K[[t]]. The program endpoint +is therefore a matrix of rational functions regular at t=0. Its formal +expansion is precisely the specialization Y_a -> t(M_a-I) of the series from +Section 2: in each degree there are only finitely many words, so substitution +is legitimate. + +If the noncommutative endpoint series is zero, this matrix has identically +zero power series at t=0. A rational function regular at zero with zero formal +expansion is zero in K(t): multiply by its denominator, whose constant term is +nonzero. Finally every inverse occurrence is regular at t=1, since +det G_a(1)=det M_a != 0. Evaluating the zero rational endpoint at t=1 proves +equality for this arbitrary invertible tuple M_a. This is valid over finite +fields as well; it uses a formal indeterminate, not sampling field elements. + +Thus a finite closure certificate proves the complete universal invertible +endpoint claim, without assuming convergence, generic numerical invertibility +or an infinite-field polynomial identity heuristic. + +## 5. Nonzero series gives an explicit invertible witness + +Suppose c=(U T_a1 ... T_ak V)_(o,i) is nonzero. On the basis e_0,...,e_k let + + N_a = sum_(j=0 to k-1, a_(j+1)=a) E_(j,j+1), + G_a = I + N_a. + +All N_a share the same strictly upper-triangular flag. All products of more +than k such matrices vanish, and each inverse G_a^(-1) is the finite sum +I-N_a+N_a^2-...+(-N_a)^k. Therefore the formal-series substitution now really +is a finite calculation, also for programs containing inverse calls. + +In matrix entry (0,k), shorter words give zero, longer words give zero, and a +word of length k gives one exactly when its labels are a1,...,ak in order. +The literal endpoint difference in block (o,i), entry (0,k), equals c. +Use input e_k in role i and zero vectors in other roles to exhibit a concrete +failure. The universal check had kept all roles independent; this choice of +one witness input imposes no clean-state assumption on the theorem. +For k=0 take dimension one and all G_a=I. + +This proves the converse in Section 1 and the constructive dimension bound. +The literal matrix oracle computes inverses by Gaussian elimination and +executes the original instructions; it does not reuse T_a or the producer. + +## 6. Boundaries and discriminating examples + +The dirty-sandwich example has roles x,h,y, all arbitrary. It temporarily +changes h to h+A x, adds B h to y, restores h, and subtracts B h. Its complete +endpoint is (x,h,y+B A x). The reference program temporarily applies A to x, +queries B x into y, and applies A^(-1) to x. Both full endpoints agree. +Deleting any one of the eight left-side instructions yields a detectable +failure in each tested field. This example certifies the stated algebraic +boundary; it is not a proposed faster physical implementation or a new echo +construction. + +A false commutator identity B^(-1)A^(-1)BA=I has a nonzero degree-two +coefficient. Scalar/one-dimensional substitutions cannot reveal that error; +the certificate's unipotent witness does. Self-source queries, omitted helper +returns and wrong inverse signs have distinct rejecting fixtures. + +The family G^(-1)(I-G)^d expands to (-Y)^d/(1+Y), so its first coefficient +occurs at degree d and its tail continues indefinitely. The replay checks +coefficients beyond the program's number of unary occurrences. In F_p, +G^p-I=Y^p supplies a characteristic-sensitive delayed witness. + +The stress example computes (A+B)^64 x, which has 2^64 distinct noncommutative +words, on both sides, and inserts a C^(-1),C cancellation on one side. +The complete two-role comparison uses D=260 states and no expanded words. +The helper is explicitly overwritten on both sides in this stress program; +the separate dirty-sandwich example tests actual helper restoration. + +For a termwise tensor substitution choose the new generators G_a^(tensor f) +and their actual inverses. The theorem then applies at the enlarged payload +dimension. Scalar coefficients stay scalar; no tensor power of a sum or of +the whole register-role matrix is taken. This is only an algebraic interface +lemma. Native realizations, phases, rounding, rectangular typing, precision, +stock, hosting, fixed-tape cost, complete paid invoices and supplier admission +are not proved here. No selected frontier or kappa changes. + +Prepared by Krzysztof Wójt with substantial OpenAI Codex assistance. Apache-2.0. diff --git a/research/inverse-certificate-bit-bounds/vendor/UPSTREAM-README.md b/research/inverse-certificate-bit-bounds/vendor/UPSTREAM-README.md new file mode 100644 index 0000000000..1f895da660 --- /dev/null +++ b/research/inverse-certificate-bit-bounds/vendor/UPSTREAM-README.md @@ -0,0 +1,151 @@ +# Compact certificates for dirty circuits with actual inverse calls + +A name such as `A_inverse` is an independent symbol unless the verifier +implements its relation to `A`. This package closes that specific gap in +[zxv's PR5235](https://github.com/CrocSwap/integer-mult-bounds/pull/5235), exact +head `48976daa4dce59b4867ef046da72a370e389925d`. + +For two linear register programs with r independent input roles and q total +unary occurrences, **D=r+q states** suffice to certify equality of **every +returned role** under all invertible operator substitutions and all payload +dimensions. Forward and inverse occurrences share the same generator. A failed +identity yields explicit unipotent matrices and an input in dimension at most +D. No expansion of reduced words or infinite series is needed. + +The [written proof](PROOF.md) constructs a finite feedback realization at +`G=I+Y`, proves the passage to arbitrary invertible matrices using a central +indeterminate, and gives sound/complete closure certificates. These are a new +repository interface and implementation of classical rational-series ideas, +not a new general weighted-automata or Magnus theorem. This is author-checked +scoped algebra, not supplier admission or a new kappa. + +## Interface and use + +Programs are JSON with `field: 0` for Q or a prime p <= 2^31-1 for F_p, an +ordered list of `roles`, named `operators`, and `left`/`right` instruction lists. +Every role starts as a separate arbitrary vector and every role is compared at +exit. Scalar coefficients are integers or exact fraction strings; denominators +must be invertible in the selected field. See the three [examples](examples). + +| Instruction | Exact semantics | +|---|---| +| `linear`, `dst`, `terms: [[role,c], ...]` | Replace dst by the scalar sum, reading all old values. | +| `apply`, `dst`, `operator`, `direction: 1` or `-1` | Apply G or its actual inverse to dst. | +| `query`, `dst`, `src`, `operator`, `direction`, `coefficient` | Add c G^direction(src) to dst, reading the old source even when src=dst. | + +The [dirty-sandwich example](examples/dirty-sandwich.json) compares two complete +programs with endpoint `(x,h,y+B A x)` and restores arbitrary dirty h. The +[wrong-order example](examples/wrong-order.json) produces a three-dimensional +counterexample; its [literal matrices and input](examples/wrong-order.witness.json) +make the noncommutation failure directly inspectable. The +[binary inverse-tail example](examples/binary-inverse-tail.json) needs a +degree-five coefficient and has a genuinely infinite formal tail. + +Generate and check a certificate from the repository root: + +```sh +python3.12 -B research/inverse-dirty-certificates/certify.py \ + research/inverse-dirty-certificates/examples/dirty-sandwich.json \ + --output /tmp/dirty-sandwich-certificate.json +python3.12 -B research/inverse-dirty-certificates/check_certificate.py \ + research/inverse-dirty-certificates/examples/dirty-sandwich.json \ + /tmp/dirty-sandwich-certificate.json +``` + +For a false identity, `certify.py` also accepts `--witness /tmp/witness.json`, +which writes the actual invertible matrices, all initial role vectors and the +endpoint discrepancy. A valid negative certificate is successfully checked +with verdict `different`; CLI exit success means valid evidence, not equality. + +`check_certificate.py` imports neither `algebra.py` nor the producer. It +reconstructs the feedback equations separately and performs no elimination or +search. It shares only strict syntax and exact field arithmetic. The literal +free-group and matrix oracles are a separate implementation in `oracles.py`. +All were prepared in the same assisted research session; this is not an +independent scientific review claim. + +## Evidence and scope + +The deterministic replay checks: + +- 504 signed-word cancellation/deletion cases over Q, F2 and F5; +- 160 scalar/apply/query differential programs against literal reduced words; +- 64 dirty-boundary, order, self-source and characteristic controls; +- 36 delayed/infinite-tail cases, including positive-characteristic witnesses; +- 324 literal invertible-matrix substitutions of the full dirty boundary; +- 16 malformed/false certificate rejections and 15 invalid-program rejections; +- three committed example certificates and two explicit matrix witnesses. + +The `(A+B)^64` stress endpoint contains **2^64 distinct words** before +comparison. Its inverse-aware certificate uses **260 states and 64 invariant +rows**. It overwrites a helper identically on both sides; actual dirty-helper +restoration is checked separately. This is a compact-representation example, +not a claim about performance on every existing supplier. + +The proof permits arbitrary fields. This executable supports Q and prime +fields only. Inverse calls are exact square linear operations. Extra operator +relations, rectangular types, nonlinear or rounded leaves, native realization, +phase conventions, precision, stock, hosting, tapes and the complete paid/outer +bill remain outside scope. A negative result for independently invertible +generators may disappear under additional relations. The checker does not +certify shortestness of a failure word or a minimum matrix dimension. + +Normal and optimized registered replays, source/history checks and the +Git-free export are recorded in [VALIDATION.json](VALIDATION.json). Finite tests +corroborate the universal written proof; no Lean or independent human review is +claimed. No selected record or predecessor source is changed. + +## Reproduce + +Python 3.12, standard library only. From the repository root: + +```sh +python3.12 -B scripts/research_package.py --package research/inverse-dirty-certificates --check-only +python3.12 scripts/research_package.py --package research/inverse-dirty-certificates +python3.12 -W error -B research/inverse-dirty-certificates/verify.py +python3.12 -W error -O -B research/inverse-dirty-certificates/verify.py +``` + +One direct replay took about 16 seconds on the recorded host. Default replay +does not write package files. `--write-examples` is an explicit regeneration +mode; `--quick` is a development smoke test and is not the registered replay. +The direct verifier is standalone and works in a Git-free package export. +The registered runner additionally validates the pinned Git provenance. + +## Open next questions + +1. Bind one existing inverse-bearing native word to this grammar while + preserving every input and returned helper. Compare against its existing + reduced-word oracle at an exact source head. The remaining blocker is the + adapter's source/type/phase contract; this package does not infer it. +2. Add one other explicitly named relation model, such as commuting pairs. + Start with a normalization theorem and a noncommuting rejection fixture. + Quotienting the present transition matrices without a new proof is unsound. +3. Reduce checker path recomputation on a larger real adapter. Compare identical + closure equations and complete endpoints before changing representation; + exact rational coefficient growth remains an unmeasured scaling constraint. + +These are released questions, not claims on further work. Details and the scope +change from the generic formal-interface card are in [TASK.json](TASK.json). + +## Credit + +Prepared by **Krzysztof Wójt (@krzysztofwojt)** with substantial **OpenAI Codex +assistance**, including a separately delegated exact-oracle implementation. +Apache-2.0. Classical sources are cited in [PROOF.md](PROOF.md). + +Credit **zxv's PR5235** for the compact independent-operator register bridge, +invariant certificates, unipotent witnesses and the explicit inverse-frontend +question. Its dirty-echo lineage (**androolloyd**, **Chafik Boukhalfa/chafreaky +#628**, **Ali Romman #621**), **Cinna Davis #4100/#4088**, **ToikY**'s free-word +tensor audit, **Sagar Thakrar #3687**, **roger-sato #3693**, and the dirty-phase +audit following **Charles Bethin #1278** retain their results and attribution. +No predecessor source code or archived artifact is copied or modified. + +The fresh main base is `ff3cc58e370d0f678e529246f8c73e8094e18fcf`, priority +revision 7. [SOURCES.json](SOURCES.json) distinguishes ancestor provenance from +the contextual pending predecessor, which is not a replay dependency. +The [canonical claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/5236#discussioncomment-19147346) +records live overlap and status. The checked corpus and targeted searches are +evidence of due diligence, not coverage of unpublished work or arbitrary +historical diffs. diff --git a/research/inverse-certificate-bit-bounds/vendor/algebra.py b/research/inverse-certificate-bit-bounds/vendor/algebra.py new file mode 100644 index 0000000000..a9e9c8d6f1 --- /dev/null +++ b/research/inverse-certificate-bit-bounds/vendor/algebra.py @@ -0,0 +1,153 @@ +"""Compact feedback realization and exact reachable-space search. + +This is the producer implementation; check_certificate.py does not import it. +Prepared for Krzysztof Wójt with OpenAI Codex assistance. Apache-2.0. +""" + +from collections import deque + +from syntax import fingerprint, validate + + +def add_scaled(dst, src, scalar, field): + if scalar: + for j, value in enumerate(src): + if value: + dst[j] = field.add(dst[j], field.mul(scalar, value)) + + +def row_times(row, matrix, field): + result = [field.zero] * len(matrix[0]) + for scalar, source in zip(row, matrix): + add_scaled(result, source, scalar, field) + return result + + +def compile_program(program): + """Return U,T,V with coefficients U T_word V after G=I+Y. + + Both sides share the original leaf atoms. Each unary occurrence creates + exactly one further atom, including inverse and zero-coefficient queries. + """ + f = validate(program) + roles = program["roles"] + r = len(roles) + q = sum(ins["op"] != "linear" for side in ("left", "right") for ins in program[side]) + d = r + q + atoms = [] + finals = [] + for side in ("left", "right"): + regs = {name: [f.one if j == i else f.zero for j in range(d)] + for i, name in enumerate(roles)} + for ins in program[side]: + dst = ins["dst"] + if ins["op"] == "linear": + result = [f.zero] * d + for name, coefficient in ins["terms"]: + add_scaled(result, regs[name], f.parse(coefficient), f) + regs[dst] = result + continue + source = dst if ins["op"] == "apply" else ins["src"] + dependency = regs[source][:] + j = r + len(atoms) + atoms.append((ins["operator"], ins["direction"], dependency)) + if ins["op"] == "apply": + regs[dst] = [f.one if k == j else f.zero for k in range(d)] + else: + result = regs[dst][:] + result[j] = f.add(result[j], f.parse(ins["coefficient"])) + regs[dst] = result + finals.append([regs[name] for name in roles]) + u = [[f.sub(x, y) for x, y in zip(a, b)] for a, b in zip(*finals)] + v = [[f.one if i == j else f.zero for j in range(r)] for i in range(d)] + transitions = {a: [[f.zero] * d for _ in range(d)] for a in program["operators"]} + for j, (symbol, direction, dependency) in enumerate(atoms, r): + v[j] = row_times(dependency[:j], v[:j], f) + for a, matrix in transitions.items(): + matrix[j] = row_times(dependency[:j], matrix[:j], f) + if a == symbol: + if direction == 1: + add_scaled(matrix[j], dependency, f.one, f) + else: + matrix[j][j] = f.sub(matrix[j][j], f.one) + return {"field": f, "dimension": d, "U": u, "T": transitions, "V": v} + + +class ReachableBasis: + """Echelon rows with exact coordinates in the original path rows.""" + + def __init__(self, field): + self.field = field + self.rows = [] + self.echelon = [] + + def reduce(self, row): + f = self.field + residual = row[:] + coefficients = [f.zero] * len(self.rows) + for pivot, normalized, coordinates in self.echelon: + scalar = residual[pivot] + if scalar: + add_scaled(residual, normalized, f.neg(scalar), f) + add_scaled(coefficients, coordinates, scalar, f) + return residual, coefficients + + def append(self, row): + f = self.field + residual, removed = self.reduce(row) + pivot = next((j for j, x in enumerate(residual) if x), None) + if pivot is None: + return False + scale = residual[pivot] + normalized = [f.div(x, scale) for x in residual] + coordinates = [f.div(f.neg(x), scale) for x in removed] + [f.div(f.one, scale)] + self.rows.append(row[:]) + self.echelon.append((pivot, normalized, coordinates)) + return True + + def coordinates(self, row): + remainder, coefficients = self.reduce(row) + if any(remainder): + raise ValueError("row is outside the claimed span") + return coefficients + + +def produce(program): + model = compile_program(program) + f, u, t, v = (model[k] for k in ("field", "U", "T", "V")) + basis = ReachableBasis(f) + paths = [] + queue = deque() + for output, row in enumerate(u): + if basis.append(row): + path = {"output": output, "word": []} + paths.append(path) + queue.append((row, path)) + while queue: + row, path = queue.popleft() + projected = row_times(row, v, f) + if any(projected): + i = next(i for i, value in enumerate(projected) if value) + return { + "schema": "inverse-dirty-certificate/v1", + "program_sha256": fingerprint(program), + "verdict": "different", + "output": path["output"], "input": i, "word": path["word"], + "coefficient": f.dump(projected[i]), + } + for symbol, matrix in t.items(): + successor = row_times(row, matrix, f) + if basis.append(successor): + successor_path = {"output": path["output"], "word": path["word"] + [symbol]} + paths.append(successor_path) + queue.append((successor, successor_path)) + encode = lambda rows: [[f.dump(x) for x in row] for row in rows] + return { + "schema": "inverse-dirty-certificate/v1", + "program_sha256": fingerprint(program), + "verdict": "equal", + "paths": paths, + "initial": encode([basis.coordinates(row) for row in u]), + "closure": {a: encode([basis.coordinates(row_times(b, matrix, f)) + for b in basis.rows]) for a, matrix in t.items()}, + } diff --git a/research/inverse-certificate-bit-bounds/vendor/check_certificate.py b/research/inverse-certificate-bit-bounds/vendor/check_certificate.py new file mode 100644 index 0000000000..1117bf61f8 --- /dev/null +++ b/research/inverse-certificate-bit-bounds/vendor/check_certificate.py @@ -0,0 +1,163 @@ +"""Check finite equations with a separate feedback compiler and no elimination. + +Imports only shared syntax/exact arithmetic, never the producer. A verified +failure word proves difference, not that its length is minimal. +Prepared for Krzysztof Wójt with OpenAI Codex assistance. Apache-2.0. +""" + +import argparse +import json +from pathlib import Path + +from syntax import exact_keys, fingerprint, validate + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def reconstruct(program): + """Build sparse constant/unary equations, then forward-solve I-E. + + This deliberately differs from the producer's per-row recurrence. + """ + f = validate(program) + roles, alphabet = program["roles"], program["operators"] + r = len(roles) + definitions = [None] * r + endpoints = [] + + def combine(pairs): + result = {} + for scalar, expression in pairs: + for j, value in expression.items(): + result[j] = f.add(result.get(j, f.zero), f.mul(scalar, value)) + if not result[j]: + del result[j] + return result + + for side in ("left", "right"): + registers = {name: {i: f.one} for i, name in enumerate(roles)} + for operation in program[side]: + destination = operation["dst"] + if operation["op"] == "linear": + registers[destination] = combine( + (f.parse(c), registers[name]) for name, c in operation["terms"]) + continue + source = operation.get("src", destination) + index = len(definitions) + definitions.append((registers[source].copy(), operation["operator"], operation["direction"])) + if operation["op"] == "apply": + registers[destination] = {index: f.one} + else: + registers[destination] = combine([ + (f.one, registers[destination]), + (f.parse(operation["coefficient"]), {index: f.one})]) + endpoints.append([registers[name] for name in roles]) + d = len(definitions) + # H = (I-E)^-1, obtained by an exact triangular solve; no matrix inverse. + h = [[f.one if i == j else f.zero for j in range(d)] for i in range(d)] + for i in range(r, d): + dependency, _, _ = definitions[i] + for j, coefficient in dependency.items(): + require(j < i, "noncausal constant dependency") + for k in range(d): + h[i][k] = f.add(h[i][k], f.mul(coefficient, h[j][k])) + transitions = {a: [[f.zero] * d for _ in range(d)] for a in alphabet} + for j in range(r, d): + dependency, a, sign = definitions[j] + unary = dependency if sign == 1 else {j: f.neg(f.one)} + for i in range(d): + if h[i][j]: + for k, coefficient in unary.items(): + transitions[a][i][k] = f.add(transitions[a][i][k], f.mul(h[i][j], coefficient)) + u = [] + for left, right in zip(*endpoints): + delta = combine([(f.one, left), (f.neg(f.one), right)]) + u.append([delta.get(j, f.zero) for j in range(d)]) + return f, u, transitions, [row[:r] for row in h] + + +def multiply(row, matrix, f, columns): + answer = [f.zero] * columns + for i, coefficient in enumerate(row): + if coefficient: + for j in range(columns): + if matrix[i][j]: + answer[j] = f.add(answer[j], f.mul(coefficient, matrix[i][j])) + return answer + + +def index(value, size): + require(type(value) is int and 0 <= value < size, "index outside declared boundary") + return value + + +def check(program, certificate): + f, u, t, v = reconstruct(program) + r, d = len(u), len(v) + require(isinstance(certificate, dict), "certificate must be an object") + require(certificate.get("schema") == "inverse-dirty-certificate/v1", "unknown certificate schema") + require(certificate.get("program_sha256") == fingerprint(program), "certificate belongs to another program") + + def path_row(output, word): + row = u[index(output, r)][:] + require(isinstance(word, list) and len(word) < d, "path exceeds the state bound") + for symbol in word: + require(isinstance(symbol, str) and symbol in t, "unknown path symbol") + row = multiply(row, t[symbol], f, d) + return row + + verdict = certificate.get("verdict") + common = {"schema", "program_sha256", "verdict"} + if verdict == "different": + exact_keys(certificate, common | {"output", "input", "word", "coefficient"}) + row = path_row(certificate["output"], certificate["word"]) + value = multiply(row, v, f, r)[index(certificate["input"], r)] + require(value != f.zero and value == f.parse(certificate["coefficient"]), "invalid distinguishing coefficient") + return {"verdict": "different", "states": d, "witness_dimension": len(certificate["word"]) + 1} + require(verdict == "equal", "unknown verdict") + exact_keys(certificate, common | {"paths", "initial", "closure"}) + paths = certificate["paths"] + require(isinstance(paths, list) and len(paths) <= d, "too many basis rows") + rows = [] + for path in paths: + exact_keys(path, {"output", "word"}) + rows.append(path_row(path["output"], path["word"])) + b = len(rows) + + def scalar_matrix(value, height, width): + require(isinstance(value, list) and len(value) == height, "coordinate matrix height") + result = [] + for row in value: + require(isinstance(row, list) and len(row) == width, "coordinate matrix width") + result.append([f.parse(x) for x in row]) + return result + + initial = scalar_matrix(certificate["initial"], r, b) + exact_keys(certificate["closure"], set(t)) + for i in range(r): + require(multiply(initial[i], rows, f, d) == u[i], "initial rows not in certified span") + for row in rows: + require(not any(multiply(row, v, f, r)), "basis row has a nonzero input projection") + for symbol, transition in t.items(): + coordinates = scalar_matrix(certificate["closure"][symbol], b, b) + for i, row in enumerate(rows): + require(multiply(row, transition, f, d) == multiply(coordinates[i], rows, f, d), + "span is not transition-closed") + return {"verdict": "equal", "states": d, "invariant_rows": b} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("program", type=Path) + parser.add_argument("certificate", type=Path) + args = parser.parse_args() + program = json.loads(args.program.read_text(encoding="utf-8")) + certificate = json.loads(args.certificate.read_text(encoding="utf-8")) + print(json.dumps(check(program, certificate), sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/inverse-certificate-bit-bounds/vendor/dirty-sandwich.json b/research/inverse-certificate-bit-bounds/vendor/dirty-sandwich.json new file mode 100644 index 0000000000..c1254508e7 --- /dev/null +++ b/research/inverse-certificate-bit-bounds/vendor/dirty-sandwich.json @@ -0,0 +1,105 @@ +{ + "schema": "inverse-dirty-program/v1", + "field": 0, + "roles": [ + "x", + "h", + "y" + ], + "operators": [ + "A", + "B" + ], + "left": [ + { + "op": "apply", + "dst": "h", + "operator": "A", + "direction": -1 + }, + { + "op": "linear", + "dst": "h", + "terms": [ + [ + "h", + 1 + ], + [ + "x", + 1 + ] + ] + }, + { + "op": "apply", + "dst": "h", + "operator": "A", + "direction": 1 + }, + { + "op": "query", + "dst": "y", + "src": "h", + "operator": "B", + "direction": 1, + "coefficient": 1 + }, + { + "op": "apply", + "dst": "h", + "operator": "A", + "direction": -1 + }, + { + "op": "linear", + "dst": "h", + "terms": [ + [ + "h", + 1 + ], + [ + "x", + -1 + ] + ] + }, + { + "op": "apply", + "dst": "h", + "operator": "A", + "direction": 1 + }, + { + "op": "query", + "dst": "y", + "src": "h", + "operator": "B", + "direction": 1, + "coefficient": -1 + } + ], + "right": [ + { + "op": "apply", + "dst": "x", + "operator": "A", + "direction": 1 + }, + { + "op": "query", + "dst": "y", + "src": "x", + "operator": "B", + "direction": 1, + "coefficient": 1 + }, + { + "op": "apply", + "dst": "x", + "operator": "A", + "direction": -1 + } + ] +} diff --git a/research/inverse-certificate-bit-bounds/vendor/fields.py b/research/inverse-certificate-bit-bounds/vendor/fields.py new file mode 100644 index 0000000000..2442625a15 --- /dev/null +++ b/research/inverse-certificate-bit-bounds/vendor/fields.py @@ -0,0 +1,67 @@ +"""Exact Q / prime-field arithmetic shared by the two implementations. + +Prepared for Krzysztof Wójt with OpenAI Codex assistance. Apache-2.0. +""" + +from fractions import Fraction +from functools import lru_cache +from math import isqrt + + +@lru_cache(maxsize=64) +def prime(p): + if p < 2 or p > 2**31 - 1: + return False + if p % 2 == 0: + return p == 2 + return all(p % d for d in range(3, isqrt(p) + 1, 2)) + + +class Field: + def __init__(self, characteristic=0): + if type(characteristic) is not int or ( + characteristic != 0 and not prime(characteristic) + ): + raise ValueError("field must be 0 (Q) or a prime at most 2^31-1") + self.characteristic = characteristic + self.zero = 0 if characteristic else Fraction(0) + self.one = 1 if characteristic else Fraction(1) + + def parse(self, value): + if type(value) not in (int, str, Fraction): + raise ValueError("scalar must be an integer or an exact fraction string") + try: + value = Fraction(value) + except (ValueError, ZeroDivisionError) as error: + raise ValueError("invalid exact scalar") from error + p = self.characteristic + if not p: + return value + if value.denominator % p == 0: + raise ValueError("scalar denominator is zero in the field") + return value.numerator * pow(value.denominator, -1, p) % p + + def add(self, x, y): + return (x + y) % self.characteristic if self.characteristic else x + y + + def sub(self, x, y): + return (x - y) % self.characteristic if self.characteristic else x - y + + def mul(self, x, y): + return (x * y) % self.characteristic if self.characteristic else x * y + + def neg(self, x): + return -x % self.characteristic if self.characteristic else -x + + def div(self, x, y): + if not y: + raise ValueError("division by zero") + if self.characteristic: + return x * pow(y, -1, self.characteristic) % self.characteristic + return x / y + + def dump(self, x): + return str(x) + + def is_zero(self, x): + return x == 0 diff --git a/research/inverse-certificate-bit-bounds/vendor/oracles.py b/research/inverse-certificate-bit-bounds/vendor/oracles.py new file mode 100644 index 0000000000..ad52010688 --- /dev/null +++ b/research/inverse-certificate-bit-bounds/vendor/oracles.py @@ -0,0 +1,390 @@ +"""Independent exact endpoint oracles for inverse-dirty register programs. + +The free-group oracle expands operator words literally and is limited by its +support cap. The matrix oracle checks one supplied finite-dimensional operator +assignment; neither oracle compiles or validates certificates. Witness vectors +corroborate an endpoint calculation and do not establish shortestness. + +Prepared for Krzysztof Wójt with OpenAI Codex assistance. Apache-2.0. +""" + +from __future__ import annotations + +from typing import Any + +try: + from .fields import Field +except ImportError: # Also support running sibling research scripts directly. + from fields import Field + + +WordKey = tuple[int, tuple[int, ...]] + + +def _field(program: dict[str, Any]) -> Field: + return Field(program["field"]) + + +def _prepend(symbol: int, word: tuple[int, ...]) -> tuple[int, ...]: + """Prepend a newly applied generator and reduce the free-group word.""" + if word and word[0] == -symbol: + return word[1:] + return (symbol,) + word + + +def _add_word_term( + target: dict[WordKey, Any], + key: WordKey, + value: Any, + field: Field, +) -> None: + total = field.add(target.get(key, field.zero), value) + if field.is_zero(total): + target.pop(key, None) + else: + target[key] = total + + +def _word_endpoint_side( + program: dict[str, Any], instructions: list[dict[str, Any]], field: Field, support_cap: int +) -> list[dict[WordKey, Any]]: + roles = program["roles"] + operators = {name: index for index, name in enumerate(program["operators"], start=1)} + registers: list[dict[WordKey, Any]] = [ + {(index, ()): field.one} for index in range(len(roles)) + ] + role_index = {role: index for index, role in enumerate(roles)} + + def check_support() -> None: + count = sum(len(register) for register in registers) + if count > support_cap: + raise ValueError( + f"literal free-group support {count} exceeds support_cap={support_cap}" + ) + + check_support() + for instruction in instructions: + op = instruction["op"] + dst = role_index[instruction["dst"]] + if op == "linear": + updated: dict[WordKey, Any] = {} + for source_role, raw_coefficient in instruction["terms"]: + coefficient = field.parse(raw_coefficient) + for key, value in registers[role_index[source_role]].items(): + _add_word_term( + updated, key, field.mul(coefficient, value), field + ) + registers[dst] = updated + elif op == "apply": + symbol = operators[instruction["operator"]] * instruction["direction"] + updated = {} + for (input_index, word), value in registers[dst].items(): + updated[(input_index, _prepend(symbol, word))] = value + registers[dst] = updated + elif op == "query": + source = role_index[instruction["src"]] + symbol = operators[instruction["operator"]] * instruction["direction"] + coefficient = field.parse(instruction["coefficient"]) + updated = dict(registers[dst]) + for (input_index, word), value in registers[source].items(): + key = (input_index, _prepend(symbol, word)) + _add_word_term( + updated, key, field.mul(coefficient, value), field + ) + registers[dst] = updated + else: # The input contract says programs are already validated. + raise ValueError(f"unknown instruction op {op!r}") + check_support() + return registers + + +def reduced_word_endpoint( + program: dict[str, Any], support_cap: int = 100_000 +) -> list[dict[WordKey, Any]]: + """Return each left-minus-right role as an exact reduced free-group sum. + + Keys are ``(input_role_index, signed_generator_word)``. Generator indices + follow ``program["operators"]`` starting at 1. A positive symbol means the + named operator and a negative symbol its inverse. Every role starts as an + independent input register. Expansion is literal and raises ``ValueError`` + if the combined live support exceeds ``support_cap``. + """ + if support_cap < 0: + raise ValueError("support_cap must be nonnegative") + field = _field(program) + left = _word_endpoint_side(program, program["left"], field, support_cap) + right = _word_endpoint_side(program, program["right"], field, support_cap) + result: list[dict[WordKey, Any]] = [] + for left_role, right_role in zip(left, right): + difference = dict(left_role) + for key, value in right_role.items(): + _add_word_term(difference, key, field.neg(value), field) + result.append(difference) + if sum(len(register) for register in result) > support_cap: + raise ValueError( + f"literal free-group support exceeds support_cap={support_cap}" + ) + return result + + +def _parse_matrix(raw: list[list[Any]], field: Field, name: str) -> list[list[Any]]: + if not isinstance(raw, list) or any(not isinstance(row, list) for row in raw): + raise ValueError(f"operator {name!r} must be a square list matrix") + size = len(raw) + if any(len(row) != size for row in raw): + raise ValueError(f"operator {name!r} must be square") + return [[field.parse(value) for value in row] for row in raw] + + +def _inverse(matrix: list[list[Any]], field: Field) -> list[list[Any]]: + """Invert a square matrix by exact Gauss-Jordan elimination.""" + size = len(matrix) + augmented = [ + list(row) + + [field.one if row_index == column else field.zero for column in range(size)] + for row_index, row in enumerate(matrix) + ] + width = 2 * size + for column in range(size): + pivot = next( + (row for row in range(column, size) if not field.is_zero(augmented[row][column])), + None, + ) + if pivot is None: + raise ValueError("operator matrix is singular and cannot be inverted") + if pivot != column: + augmented[column], augmented[pivot] = augmented[pivot], augmented[column] + pivot_value = augmented[column][column] + augmented[column] = [field.div(value, pivot_value) for value in augmented[column]] + for row in range(size): + if row == column: + continue + factor = augmented[row][column] + if field.is_zero(factor): + continue + augmented[row] = [ + field.sub(augmented[row][entry], field.mul(factor, augmented[column][entry])) + for entry in range(width) + ] + return [row[size:] for row in augmented] + + +def _zero_matrix(size: int, field: Field) -> list[list[Any]]: + return [[field.zero for _ in range(size)] for _ in range(size)] + + +def _matrix_add_scaled( + left: list[list[Any]], right: list[list[Any]], coefficient: Any, field: Field +) -> list[list[Any]]: + return [ + [field.add(a, field.mul(coefficient, b)) for a, b in zip(left_row, right_row)] + for left_row, right_row in zip(left, right) + ] + + +def _matrix_scale( + matrix: list[list[Any]], coefficient: Any, field: Field +) -> list[list[Any]]: + return [[field.mul(coefficient, value) for value in row] for row in matrix] + + +def _matrix_multiply( + left: list[list[Any]], right: list[list[Any]], field: Field +) -> list[list[Any]]: + size = len(left) + return [ + [ + _dot(left[row], [right[index][column] for index in range(size)], field) + for column in range(size) + ] + for row in range(size) + ] + + +def _dot(left: list[Any], right: list[Any], field: Field) -> Any: + total = field.zero + for a, b in zip(left, right): + total = field.add(total, field.mul(a, b)) + return total + + +def _matrix_is_zero(matrix: list[list[Any]], field: Field) -> bool: + return all(field.is_zero(value) for row in matrix for value in row) + + +def _literal_endpoint_side( + program: dict[str, Any], + instructions: list[dict[str, Any]], + matrices: dict[str, list[list[Any]]], + inverse_cache: dict[str, list[list[Any]]], + size: int, + field: Field, +) -> list[dict[int, list[list[Any]]]]: + roles = program["roles"] + role_index = {role: index for index, role in enumerate(roles)} + identity = [ + [field.one if row == column else field.zero for column in range(size)] + for row in range(size) + ] + registers: list[dict[int, list[list[Any]]]] = [ + {index: [row[:] for row in identity]} for index in range(len(roles)) + ] + + for instruction in instructions: + op = instruction["op"] + dst = role_index[instruction["dst"]] + if op == "linear": + updated: dict[int, list[list[Any]]] = {} + for source_role, raw_coefficient in instruction["terms"]: + coefficient = field.parse(raw_coefficient) + for input_index, block in registers[role_index[source_role]].items(): + total = _matrix_add_scaled( + updated.get(input_index, _zero_matrix(size, field)), + block, + coefficient, + field, + ) + if _matrix_is_zero(total, field): + updated.pop(input_index, None) + else: + updated[input_index] = total + registers[dst] = updated + elif op == "apply": + name = instruction["operator"] + if instruction["direction"] == 1: + operator_matrix = matrices[name] + else: + if name not in inverse_cache: + inverse_cache[name] = _inverse(matrices[name], field) + operator_matrix = inverse_cache[name] + registers[dst] = { + input_index: _matrix_multiply(operator_matrix, block, field) + for input_index, block in registers[dst].items() + } + elif op == "query": + name = instruction["operator"] + if instruction["direction"] == 1: + operator_matrix = matrices[name] + else: + if name not in inverse_cache: + inverse_cache[name] = _inverse(matrices[name], field) + operator_matrix = inverse_cache[name] + coefficient = field.parse(instruction["coefficient"]) + updated = dict(registers[dst]) + for input_index, block in registers[role_index[instruction["src"]]].items(): + transformed = _matrix_multiply(operator_matrix, block, field) + total = _matrix_add_scaled( + updated.get(input_index, _zero_matrix(size, field)), + transformed, + coefficient, + field, + ) + if _matrix_is_zero(total, field): + updated.pop(input_index, None) + else: + updated[input_index] = total + registers[dst] = updated + else: # The input contract says programs are already validated. + raise ValueError(f"unknown instruction op {op!r}") + return registers + + +def literal_endpoint( + program: dict[str, Any], operators: dict[str, list[list[Any]]] +) -> list[list[list[list[Any]]]]: + """Return all exact left-minus-right matrix blocks for one operator choice. + + The result is indexed ``[output_role][input_role][row][column]``. Missing + blocks are returned as full zero matrices. If the program has no operators + and ``operators`` is empty, the otherwise-undetermined matrix dimension is + taken to be 1. Inverses use exact Gauss-Jordan elimination over the program + field; singular matrices raise ``ValueError``. + """ + field = _field(program) + matrices = { + name: _parse_matrix(raw, field, name) for name, raw in operators.items() + } + named_operators = program["operators"] + missing = [name for name in named_operators if name not in matrices] + if missing: + raise ValueError(f"missing matrices for named operators: {missing!r}") + + dimensions = {len(matrix) for matrix in matrices.values()} + if len(dimensions) > 1: + raise ValueError("all operator matrices must have the same dimension") + size = next(iter(dimensions), 1) + inverse_cache: dict[str, list[list[Any]]] = {} + left = _literal_endpoint_side( + program, program["left"], matrices, inverse_cache, size, field + ) + right = _literal_endpoint_side( + program, program["right"], matrices, inverse_cache, size, field + ) + zero = _zero_matrix(size, field) + minus_one = field.neg(field.one) + result: list[list[list[list[Any]]]] = [] + for left_blocks, right_blocks in zip(left, right): + output: list[list[list[Any]]] = [] + for input_index in range(len(program["roles"])): + output.append( + _matrix_add_scaled( + left_blocks.get(input_index, zero), + right_blocks.get(input_index, zero), + minus_one, + field, + ) + ) + result.append(output) + return result + + +def unipotent_operators( + program: dict[str, Any], word: list[str] +) -> dict[str, list[list[Any]]]: + """Build the standard upper-shift unipotent assignment for ``word``.""" + field = _field(program) + names = program["operators"] + unknown = [name for name in word if name not in names] + if unknown: + raise ValueError(f"word contains operators absent from the program: {unknown!r}") + size = len(word) + 1 + result: dict[str, list[list[Any]]] = {} + for name in names: + matrix = [ + [field.one if row == column else field.zero for column in range(size)] + for row in range(size) + ] + for index, symbol in enumerate(word): + if symbol == name: + matrix[index][index + 1] = field.one + result[name] = matrix + return result + + +def apply_witness( + program: dict[str, Any], word: list[str], input_role: str +) -> list[list[Any]]: + """Apply the unipotent endpoint difference to ``e_last`` in one role. + + This is a concrete witness calculation for corroboration only; it does not + prove a shortest witness or a universal endpoint distinction. + """ + if input_role not in program["roles"]: + raise ValueError(f"unknown input role {input_role!r}") + operators = unipotent_operators(program, word) + endpoint = literal_endpoint(program, operators) + input_index = program["roles"].index(input_role) + last_column = len(word) + return [ + [endpoint[output_index][input_index][row][last_column] + for row in range(last_column + 1)] + for output_index in range(len(program["roles"])) + ] + + +__all__ = [ + "reduced_word_endpoint", + "literal_endpoint", + "unipotent_operators", + "apply_witness", +] diff --git a/research/inverse-certificate-bit-bounds/vendor/syntax.py b/research/inverse-certificate-bit-bounds/vendor/syntax.py new file mode 100644 index 0000000000..5a91dd1921 --- /dev/null +++ b/research/inverse-certificate-bit-bounds/vendor/syntax.py @@ -0,0 +1,71 @@ +"""Strict syntax and byte-independent binding, not an algebraic compiler. + +Prepared for Krzysztof Wójt with OpenAI Codex assistance. Apache-2.0. +""" + +import hashlib +import json + +from fields import Field + + +def exact_keys(obj, keys): + if not isinstance(obj, dict) or set(obj) != set(keys): + raise ValueError(f"expected exactly these keys: {sorted(keys)}") + + +def names(values, nonempty=False): + if not isinstance(values, list) or (nonempty and not values): + raise ValueError("expected a list of names") + if any(not isinstance(x, str) or not x for x in values): + raise ValueError("names must be nonempty strings") + if len(set(values)) != len(values): + raise ValueError("duplicate name") + + +def validate(program): + exact_keys(program, {"schema", "field", "roles", "operators", "left", "right"}) + if program["schema"] != "inverse-dirty-program/v1": + raise ValueError("unknown program schema") + field = Field(program["field"]) + names(program["roles"], nonempty=True) + names(program["operators"]) + roles, operators = set(program["roles"]), set(program["operators"]) + for side in ("left", "right"): + if not isinstance(program[side], list): + raise ValueError("instruction sequence must be a list") + for ins in program[side]: + if not isinstance(ins, dict): + raise ValueError("instruction must be an object") + op = ins.get("op") + if op == "linear": + exact_keys(ins, {"op", "dst", "terms"}) + if not isinstance(ins["terms"], list): + raise ValueError("linear terms must be a list") + for term in ins["terms"]: + if not isinstance(term, list) or len(term) != 2 or term[0] not in roles: + raise ValueError("invalid linear term or undeclared source") + field.parse(term[1]) + elif op in ("apply", "query"): + keys = {"op", "dst", "operator", "direction"} + if op == "query": + keys |= {"src", "coefficient"} + exact_keys(ins, keys) + if ins["operator"] not in operators: + raise ValueError("undeclared operator") + if type(ins["direction"]) is not int or ins["direction"] not in (-1, 1): + raise ValueError("direction must be exactly +1 or -1") + if op == "query": + if ins["src"] not in roles: + raise ValueError("undeclared query source") + field.parse(ins["coefficient"]) + else: + raise ValueError("unknown instruction") + if ins["dst"] not in roles: + raise ValueError("undeclared destination") + return field + + +def fingerprint(program): + payload = json.dumps(program, sort_keys=True, separators=(",", ":"), ensure_ascii=True) + return hashlib.sha256(payload.encode("ascii")).hexdigest() diff --git a/research/inverse-certificate-bit-bounds/vendor/wrong-order.json b/research/inverse-certificate-bit-bounds/vendor/wrong-order.json new file mode 100644 index 0000000000..3beca6f4b1 --- /dev/null +++ b/research/inverse-certificate-bit-bounds/vendor/wrong-order.json @@ -0,0 +1,38 @@ +{ + "schema": "inverse-dirty-program/v1", + "field": 0, + "roles": [ + "x" + ], + "operators": [ + "A", + "B" + ], + "left": [ + { + "op": "apply", + "dst": "x", + "operator": "A", + "direction": 1 + }, + { + "op": "apply", + "dst": "x", + "operator": "B", + "direction": 1 + }, + { + "op": "apply", + "dst": "x", + "operator": "A", + "direction": -1 + }, + { + "op": "apply", + "dst": "x", + "operator": "B", + "direction": -1 + } + ], + "right": [] +} diff --git a/research/inverse-certificate-bit-bounds/verify.py b/research/inverse-certificate-bit-bounds/verify.py new file mode 100644 index 0000000000..d89036f03d --- /dev/null +++ b/research/inverse-certificate-bit-bounds/verify.py @@ -0,0 +1,132 @@ +"""Check the rational-size proof against exact, independently checked programs. + +Ali Romman, with substantial OpenAI Codex assistance. Apache-2.0. +Retained source oracles have their original author and license notices. +""" +import argparse +from copy import deepcopy +from fractions import Fraction as Q +import hashlib +import json +from pathlib import Path +import random +import sys + +ROOT=Path(__file__).resolve().parent +sys.path.insert(0,str(ROOT)) +from budget import audit, bounds, check_size, height, need, ReachableBasis +from fields import Field +from oracles import reduced_word_endpoint, apply_witness + + +def apply(a='A',direction=1,dst='x'): + return dict(op='apply',dst=dst,operator=a,direction=direction) + + +def query(dst='x',src='x',a='A',c=-1,direction=1): + return dict(op='query',dst=dst,src=src,operator=a,direction=direction,coefficient=c) + + +def linear(dst,terms): + return dict(op='linear',dst=dst,terms=[[name,c] for name,c in terms]) + + +def program(left=(),right=(),roles=('x',),operators=('A','B')): + return dict(schema='inverse-dirty-program/v1',field=0,roles=list(roles), + operators=list(operators),left=list(left),right=list(right)) + + +def reject(call): + try:call() + except ValueError:return + raise ValueError('invalid case accepted') + + +def run(small): + need(sys.get_int_max_str_digits()==0,'run with -X int_max_str_digits=0 for explicit large rationals') + for source in json.loads((ROOT/'SOURCES.json').read_text())['files']: + if source['path'].startswith('research/inverse-certificate-bit-bounds/'): + need(hashlib.sha256((ROOT.parents[1]/source['path']).read_bytes()).hexdigest()==source['sha256'],'source bytes') + rows=[];dense=0;word_checks=0 + + def inspect(name,p,expected=None,literal=True): + nonlocal dense,word_checks + record=audit(p);cert=record.pop('certificate') + if expected:need(cert['verdict']==expected,'expected verdict') + if literal: + need((not any(reduced_word_endpoint(p)))==(cert['verdict']=='equal'),'reduced group-word oracle');word_checks+=1 + if cert['verdict']=='different': + value=apply_witness(p,cert['word'],p['roles'][cert['input']]) + need(value[cert['output']][0]==Q(cert['coefficient']),'independent unipotent matrix witness');dense+=1 + record.update(name=name,certificate_digest=hashlib.sha256(json.dumps(cert,sort_keys=True).encode()).hexdigest()) + rows.append(record) + return p,cert,record + + inspect('empty',program(), 'equal') + for name in ('dirty-sandwich','wrong-order'): + inspect(name,json.loads((ROOT/'vendor'/(name+'.json')).read_text())) + huge=str(2**16000+1) + _,_,raw=inspect('large-reducible-input',program([linear('x',[('x',huge+'/'+huge)])]),'equal') + need(raw['bounds']['explicit_scalar_bits']==32002,'unreduced input size is charged') + inspect('explicit-16001-bit-scalar',program([linear('x',[('x',huge)])]),'different') + for degree in ((1,4) if small else (1,2,4,8,16)): + p=program([query()]*degree+[apply(direction=-1)],[linear('x',[])],operators=('A',)) + _,cert,_=inspect('inverse-tail-'+str(degree),p,'different') + need(len(cert['word'])==degree,'delayed shortest word') + for denominator in (3,101,2**127-1): + steps=[linear('x',[('x','1/'+str(denominator))]),query(a='A',c='2/7'),apply('B',-1)]*3 + inspect('coprime-denominators-'+str(denominator),program(steps,roles=('x',)),'different') + for bits in (20,160,1024): + delta=Q(1,2**bits+1) + rowspec=[(1,1,1),(1,1+delta,1),(1,1,1+delta)] + p=program([linear('y'+str(i),list(zip(('x0','x1','x2'),map(str,row)))) for i,row in enumerate(rowspec)], + [linear('y'+str(i),[]) for i in range(3)],roles=('x0','x1','x2','y0','y1','y2')) + inspect('nearly-dependent-'+str(bits),p,'different') + # This isolates determinant amplification from large endpoint magnitude. + basis=ReachableBasis(Field());scale=2**1024+1 + need(basis.append([Q(1),Q(1)]) and basis.append([Q(1),Q(1)+Q(1,scale)]),'independent close rows') + coordinates=basis.coordinates([Q(0),Q(1)]) + need(coordinates==[-scale,scale] and max(map(height,coordinates))==1025,'minor denominator amplification') + rng=random.Random(5343) + coefficients=['0','1','-1','2/3','-5/7',str(2**80+1),'1/'+str(2**80+7)] + for index in range(12 if small else 80): + roles=('x','h','y');steps=[] + for _ in range(9): + dst=rng.choice(roles);typ=rng.randrange(3) + if typ==0:steps.append(linear(dst,[(rng.choice(roles),rng.choice(coefficients)) for j in range(3)])) + elif typ==1:steps.append(apply(rng.choice(('A','B')),rng.choice((-1,1)),dst)) + else:steps.append(query(dst,rng.choice(roles),rng.choice(('A','B')),rng.choice(coefficients),rng.choice((-1,1)))) + if index%3==0:right=steps+[apply('A',-1,'h'),apply('A',1,'h')] + else:right=steps[:-1] + inspect('random-'+str(index),program(steps,right,roles)) + stages=8 if small else 64;steps=[] + for _ in range(stages): + steps.extend([linear('h',[('x','1/3')]),apply(),query(src='h',a='B',c='2/5')]) + _,_,stress=inspect('weighted-exponential-word-stress',program(steps+[apply('C',-1),apply('C')],steps, + roles=('x','h'),operators=('A','B','C')),'equal',False) + stress['unexpanded_x_endpoint_words']=str(2**stages) + controls=0 + for scalar in ('1e200','0e1000000000','0.125'): + reject(lambda:bounds(program([linear('x',[('x',scalar)])])));controls+=1 + p=program([apply()]);p['field']=2;reject(lambda:bounds(p));controls+=1 + p=program([query(c='1/0')]);reject(lambda:bounds(p));controls+=1 + p=program([query(c=True)]);reject(lambda:bounds(p));controls+=1 + p,cert,r=inspect('size-contract-control',program([apply()]),'different') + bad=deepcopy(cert);bad['word']=['A']*r['bounds']['states'];reject(lambda:check_size(r['bounds'],bad));controls+=1 + bad=deepcopy(cert);bad['coefficient']=str(1<