diff --git a/research/bit2234-callee-substitution/NOTICE.md b/research/bit2234-callee-substitution/NOTICE.md new file mode 100644 index 0000000000..7cd0caac49 --- /dev/null +++ b/research/bit2234-callee-substitution/NOTICE.md @@ -0,0 +1,33 @@ +# Credit and retained source scope + +New work is under the repository's Apache-2.0 license. + +Prepared for commdata2338 (@commdata2338), with substantial OpenAI Codex assistance. +No independent human or formal-kernel review is claimed. + +Jose Manuel (@jmbarrancoml), PR2234 at +`d047ef86fbc5b1614d3d8e2b8d3441413beab73f`, supplies the weighted leaf, +fixed dyadic header implementation, proper-width caller, and coarse moment +point. His source notice is retained in `sources/pr-2234/NOTICE.md`, including +the source527 factorization, ordinary borrowing, selected PR589/555 lineage +and earlier adapter, descriptor and parking credits. Retained files are +byte-for-byte copies authenticated before use. None is changed here. + +Adam Gall, PR2087 at `b5ffc48e3dd5c92f591bdb4fabafa2c8e8b33970`, supplies the +conditional stopped-time lift and uniform cost hypotheses. Its README is +retained unchanged. The recurrence and exponent formula are inherited. + +This contribution supplies completed-binary-callee substitution at two +PR2234 APIs: temporary two-field padding, its conditional all-width bound, +leaf/header cost binding, and source-authenticated endpoint checks. The +small binary callback executes elementary digit buckets; it does not +implement the faster pending recursive supplier. The second-round +corollary retains the pending callee and caller contracts. + +PR2289/2295 (Gareth Davidson / bitplane) formalize the recurrence and moment. +PR2310 (Jose Manuel) and this account's PR2332 address control and coefficient +preparation. PR2324 (Aakash Thakkar) and PR2343 (Sagar Thakrar) study distinct +borrowing thresholds. PR2364 (`b9293bb14d40f8e820ce5efd99939278e5871c56`) now supplies generic +joined full-ring packet dispatch. Discussion2319 continues with canonical +prefix decoding and coefficient-site composition, explicitly separate from +this audit. Those results are neither rerun nor claimed as new here. diff --git a/research/bit2234-callee-substitution/README.md b/research/bit2234-callee-substitution/README.md new file mode 100644 index 0000000000..445f445d19 --- /dev/null +++ b/research/bit2234-callee-substitution/README.md @@ -0,0 +1,292 @@ +# Completed-callee substitution at the selected BIT leaves and headers + +This is a **conditional compiler-interface proof and finite endpoint audit**. +At the two ordinary-interchange APIs in Jose Manuel's +[PR2234](https://github.com/CrocSwap/integer-mult-bounds/pull/2234), a completed +binary interchange of saving `a` can replace a whole radix-`q` field exchange +with cost `O(V u^(1-a))`. Only the exchanged fields are padded, their joint +volume grows by less than four, and padding closes before the next operation +in the original ring. Prefix, gap and suffix fields are never padded. + +Applying the substitution to **both** weighted leaves and reversed header +ADDs changes their width toll from `w` to `w^(1-a)`. Under the remaining +PR2234 physical and moment contracts, the source stopped recurrence then has +local toll `C V(n+w^(1-a))`. This supplies one specific implementation premise +of [Adam Gall's PR2087](https://github.com/CrocSwap/integer-mult-bounds/pull/2087) +conditional time lift. Improving leaves alone does not justify removing +PR2234's header `O(Vw)` toll. + +The conditional second-round ordinary saving at the unchanged coarse point +`c=17/10000` is `c(1-c)+c[c(1-c)] = 1699995087/10^12`. +This is an instantiation of the inherited bootstrap formula, **not** a new +selected supplier or multiplication exponent. It remains below the selected +BIT rate. The contribution is the concrete substitution and its proof +obligations, not another evaluation of that formula. + +Prepared for commdata2338 (@commdata2338), with substantial OpenAI Codex assistance. + +## Exact scope and sources + +Base: `0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2`, priority revision 4. +The claim is in [Discussion #2209](https://github.com/CrocSwap/integer-mult-bounds/discussions/2209#discussioncomment-18942787). +The card and refinement are in [TASK.json](TASK.json). + +The implementation predecessor is PR2234 head +`d047ef86fbc5b1614d3d8e2b8d3441413beab73f`, specifically `leaf.py`, +`header_streams.py`, `low_update` in `vendor/qadic_streams.py`, and +`PROOF.md` sections 4–8. PR2087 head +`b5ffc48e3dd5c92f591bdb4fabafa2c8e8b33970` is a contextual proof predecessor. +[SOURCES.json](SOURCES.json) binds exact Git blobs and SHA256 values of unchanged +copies. No pending branch must be checked out to replay this package. + +The two-field adapter lemma works for every integer `q>=2`. The source +dyadic headers require odd `q`; the whole-node and second-round corollaries +retain the source's fixed prime `q>2^80`. Small `q=3,5` fixtures test local +identities, not the large-prime fallback fraction. + +The following are **assumptions**, not conclusions from the finite tests: + +1. For fixed `0<=a<1`, the earlier binary algorithm `B_a` is completed at + **every** positive binary width `E`, with cost at most `C_b V E^(1-a)`. + It exchanges two ordered complete `2^E` ranges while preserving arbitrary + complete prefix, intervening and suffix fields, and arbitrary correlated + Boolean payload. Its constant is uniform in their cardinalities and + contents. Its endpoint is an ordinary exchange, not a reversed exchange + or merely a clean return. +2. `B_a` restores borrowed row/spectator coordinates, caller parking and head + positions, and clears local work. It requires no reserve from the caller: + internal borrowing is part of its completed contract. The fixed-tape + parking/locality contract remains in force. +3. Retained ordered shifts, fixed dyadic scales, signs, selectors and + coefficient preparation have their stated uniform stream costs. For + the whole-node corollary retain PR2234's causal generated expressions, + complete high packets, chronological endpoint/hosting argument, fresh + stock, proper child descent, uniform preparation amortization and moments. + +These hypotheses explicitly include nonbinary spectator cardinalities. +A theorem only for binary-complete spectators needs an additional adapter. +Padding every ancestor field is not part of this result. The instantiated +`B_a` from PR2234 is itself pending mathematical review. + +## Two-field substitution lemma + +Fix integer radix `q>=2`, integer `u>=1` and positive integers `P,G,S`. +An input stream has lexicographic shape + +``` +[P] x [Q] x [G] x [Q] x [S], Q=q^u, V=P Q^2 G S. +``` + +`S` may include all following spectators and the payload block length. +Put `E=ceil(log2 Q)` and `L=2^E`. Pad the two `[Q]` fields separately to +`[L]`: scan the enlarged lexicographic shape, copying the next genuine +payload exactly when both field coordinates are below `Q`, and writing an +owned zero otherwise. Call `B_a` **once on the entire padded stream** with +the same `P,G,S`. At its completed return, restrict to those inequalities. + +**Endpoint.** Let `J` exchange the two fields. The genuine rectangle +`R={x=1`, the +whole cost is at most `(4 C_b b_q+C_pad) V u^p`, with constants independent +of `u,P,G,S`. This written bound is not inferred from Python timings. + +The adapter closes padding for **each exchange** and does not change the +coefficient ring. At `q=3`, `D<-D+H` on `(H,D)=(1,2)` gives target `0` +modulo 3 but `3` modulo the padded size 4. Keeping padding live across that +original-ring ADD is an invalid shortcut. + +## Binding the two source APIs + +`adapter.py` supplies the two-field wrapper and a completed slow binary +reference callee using four sequential buckets per digit position. +`verify.py` compares its full permutation with a separate address oracle. +Distinct symbolic tokens certify arbitrary Boolean payload for these +value-oblivious permutations; tokens are not an expanded physical alphabet +claimed for the machine. + +**Weighted stopped leaf.** `leaf.py:execute_leaf` has, for each of its +`n<64` reversed pairs, the exact chronological word + +``` +J, L(a_i), J, L(-a_i^-1), J, L(a_i), J, sign_D, +``` + +where `L(t)` updates the later field by `D<-D+tH` in `Z/q^w`. +For frozen unit `a_i` this sends `(H,D)` to `(a_i D,a_i^-1 H)`: +just before the final sign the pair is `(a_i D,-a_i^-1 H)`. +The unit may depend on earlier frozen ancestors, but not either changing +field. The reversed pairs are disjoint and compose to +`F_A(H,D)=(A C_n D,C_n A^-1 H)`. + +The successor uses four whole-field calls at `u=w`, three retained shifts +and one sign per pair. Its cost is a fixed multiple of `Vw^p`, uniformly +for `0<=n<64`; a peeled leaf of at most 63 pairs has the same bound. +Its returned coordinates and private work match the original leaf. +The original `4nw` digit-swap meter is specific to its elementary backend; +it is not silently disabled. A separate successor checks `4n` completed +calls and their padded volumes/widths. The verifier authenticates and +checks the source operation sequence, then checks the successor endpoint. + +**Fixed dyadic headers.** `header_streams.py:add` uses `ordinary_fields` +before and after the forward update when the fields are reversed, at +`u=w-1`. At `w=1` the high fields disappear and no call is made. Otherwise +preceding complete high coordinates enter `P`, intervening fields enter +`G`, and trailing coordinates enter `S`; neither call is split by a high +matrix value. Each costs `O(V(w-1)^p)<=O(Vw^p)`. + +The unchanged middle operations scale, rotate and inverse-scale in +`Z/q^(w-1)` with the original carry. For `c=A/B` and new low target `y0'`, +the carry is `(B y0+A x0-B y0')/q`; the high target is +`B^-1(B y_high+A x_high+carry)`. This is the original full-ring update. +The fixed coefficient alphabet is `+-1/4,+-1/2,+-1,+-2,+-4`, so the number +of monotone scale pieces is bounded independently of `w`. Other fixed +header operations retain their `O(V)` charge. Each fixed route consequently +costs `O(Vw^p)`. + +The header replay executes the **unchanged source bodies** of `add`, its +scale/rotate helpers and `low_update`, replacing only `ordinary_fields`. +Hashes are checked before extracting these function definitions. The +symbolic tape interpreter checks append/read positions, consumed inputs +and scratch erasure; it is not a full transition-table audit. Callback +return flags state obligations: a flag cannot prove an arbitrary callee's +parking trace. + +## Conditional node and second-round consequence + +Retain the source caller and its uniform cost decomposition. There are +`O(n)` ordered atom passes, a fixed number of header routes, one peeled +leaf and a fixed number of selections/parking operations. The two changed +sites cost `O(Vw^p)`; other charges remain `O(Vn)` or `O(V)`. Hence one +width-independent `C` gives `C V(n+w^p)`, including preparation and parking. +No coarse recursive children are added: the **earlier completed** algorithm +is included in the local toll. Its own borrowing does not consume the +current caller's reserve, by its full restoration contract. + +Retain PR2234's exact profile, fallback maximum and inequalities +`mu_1<199/200`, `mu_(1-c)<9999/10000`. The same proper-width induction gives + +``` +T(n,w) <= 200 C n + 10000 C n^(1-c) w^p, n>=1. +``` + +The linear margin pays `Cn`; the power margin pays +`C n^(1-c) w^p >= Cw^p`. At a leaf `n^(1-c)>=1` pays the leaf bound. +The fallback maximum is bounded by the increasing comparison function, +without assuming actual `T` is monotone. `n=0` is identity. This is inherited +recurrence algebra from PR2234/PR2087 and PR2289/2295. The fractional moment +is not independently recertified here. + +For the next round take `a=c(1-c)`, keep `w=ceil(e^c)` and the original-width +reserve `K(w)^D(e)`. A completed old callee needs no extra parent-stock +factor. The borrowing/fit argument and two-call ordinary wrapper apply +under the retained row-restoration contract. With `n<=e/w`, +`e^c<=w<=2e^c` and `0= 1, "positive binary width") + need(len(source.data) == before * (1 << (2 * bits)) * middle * suffix, + "complete binary rectangle") + for position in range(bits): + source = digit_exchange( + source, + before * (1 << position), + (1 << (bits - 1)) * middle, + suffix * (1 << (bits - position - 1)), + 2, meter, + ) + return BinaryReturn(source) + + +def pad(source, radix, enlarged, before, middle, suffix, meter): + need(source.head == 0, "padding entry origin") + need(1 <= radix <= enlarged and min(before, middle, suffix) >= 1, + "positive complete field extents") + need(len(source.data) == before * radix**2 * middle * suffix, + "complete genuine rectangle") + out = Stream([]) + for _ in range(before): + for x in range(enlarged): + for _gap in range(middle): + for y in range(enlarged): + for _ in range(suffix): + if x < radix and y < radix: + out.write(source.read()) + meter.pad_reads += 1 + else: + out.write(0) # owned zero bits, also for an actual binary callee + meter.pad_writes += 1 + source.close_input() + return out + + +def restrict(source, radix, enlarged, before, middle, suffix, meter): + need(source.head == 0, "restriction entry origin") + need(len(source.data) == before * enlarged**2 * middle * suffix, + "complete returned binary rectangle") + out = Stream([]) + for _ in range(before): + for x in range(enlarged): + for _gap in range(middle): + for y in range(enlarged): + for _ in range(suffix): + value = source.read() + meter.crop_reads += 1 + if x < radix and y < radix: + out.write(value) + meter.crop_writes += 1 + else: + need(value == 0, "payload escaped genuine rectangle") + source.close_input() + return out + + +def qadic_exchange(source, q, width, before, middle, suffix, meter, + callee=binary_reference): + """Replace a whole q-adic field swap by exactly one completed binary call. + + Prefix/gap/suffix cardinalities are passed through verbatim. The caller + must supply a callee with the *swap* endpoint, not just a clean return. + Runtime boundary checks cannot certify that semantic premise for it. + """ + need(type(q) is int and q >= 2 and type(width) is int and width >= 0, + "radix/width domain") + radix = q**width + need(all(type(x) is int and x >= 1 for x in (before, middle, suffix)) and source.head == 0 and + len(source.data) == before * radix**2 * middle * suffix, + "whole q-adic exchange domain") + if width == 0: + meter.zero_width += 1 + return source + bits = (radix - 1).bit_length() + enlarged = 1 << bits + original_volume = len(source.data) + source = pad(source, radix, enlarged, before, middle, suffix, meter) + padded_volume = len(source.data) + need(original_volume <= padded_volume < 4 * original_volume, + "two-field volume bound") + meter.calls.append({"q": q, "width": width, "binary_width": bits, + "before": before, "middle": middle, "suffix": suffix, + "volume": original_volume, "padded_volume": padded_volume}) + result = callee(source, bits, before, middle, suffix, meter) + need(isinstance(result, BinaryReturn), "completed callee return type") + need(result.scratch_empty and result.parking_restored, "callee cleanup/locality boundary") + need(result.stream.head == 0, "callee return origin") + return restrict(result.stream, radix, enlarged, before, middle, suffix, meter) + + +def field_exchange(source, radices, first, second, q, width, meter): + need(0 <= first < second < len(radices), "ordered equal-width fields") + need(radices[first] == radices[second] == q**width, "field radix binding") + return qadic_exchange(source, q, width, prod(radices[:first]), + prod(radices[first + 1:second]), prod(radices[second + 1:]), meter) + + +def later_shift(source, radices, first, second, coefficient): + """Sequential rotation of complete later-target fibres; source unchanged.""" + need(first < second and radices[first] == radices[second], "later shift fields") + radix = radices[first] + before, middle, suffix = (prod(radices[:first]), prod(radices[first + 1:second]), + prod(radices[second + 1:])) + need(len(source.data) == prod(radices) and source.head == 0, "complete shift stream") + out = Stream([]) + for prefix in range(before): + for x in range(radix): + c = coefficient(prefix) % radix + for _gap in range(middle): + left, right = Stream([]), Stream([]) + cut = (c * x) % radix + copy(source, left, (radix - cut) * suffix) + copy(source, right, cut * suffix) + copy(right, out, cut * suffix) + copy(left, out, (radix - cut) * suffix) + left.close_input() + right.close_input() + source.close_input() + return out + + +def sign(source, radices, axis): + """Reverse the nonzero target blocks, retaining each block's internal order. + + Python lists model two sequential reversal scratch tapes here. This code + makes no stronger physical cost claim than the inherited sign primitive. + """ + radix, before, suffix = radices[axis], prod(radices[:axis]), prod(radices[axis + 1:]) + need(len(source.data) == prod(radices), "complete sign stream") + out = Stream([]) + for _ in range(before): + copy(source, out, suffix) + blocks = [] + for _ in range(radix - 1): + blocks.append([source.read() for _ in range(suffix)]) + for block in reversed(blocks): + for value in block: + out.write(value) + source.close_input() + return out + + +def weighted_leaf(raw, q, width, weights, gap=1, suffix=1, wrong_inverse=False, + omit_sign=False): + """Successor of the PR2234 leaf schedule, using completed whole-field calls. + + weights[parent][i] is a unit independent of this node's changing fields. + Arbitrary legal descriptors may provide these values; their realization + and cost are separate premises, not inferred from this finite fixture. + """ + need(bool(weights) and width >= 1, "nonempty ancestor domain") + n = len(weights[0]) + radix = q**width + need(0 <= n < 64 and all(len(row) == n for row in weights), "stopped leaf width") + need(all(gcd(value, radix) == 1 for row in weights for value in row), "unit weights") + radices = [len(weights)] + [radix] * n + [gap] + [radix] * n + [suffix] + need(len(raw) == prod(radices), "complete leaf payload") + source, meter = Stream(list(raw)), Meter() + for i in range(n): + first, second = 1 + i, 2 * n + 1 - i + parent_divisor = prod(radices[1:first]) + def coefficient(prefix, inverse=False): + a = weights[prefix // parent_divisor][i] + return -pow(a, -1, radix) if inverse and not wrong_inverse else (-a if inverse else a) + source = field_exchange(source, radices, first, second, q, width, meter) + source = later_shift(source, radices, first, second, coefficient) + source = field_exchange(source, radices, first, second, q, width, meter) + source = later_shift(source, radices, first, second, lambda p: coefficient(p, True)) + source = field_exchange(source, radices, first, second, q, width, meter) + source = later_shift(source, radices, first, second, coefficient) + source = field_exchange(source, radices, first, second, q, width, meter) + if not omit_sign: + source = sign(source, radices, second) + need(len(meter.calls) == 4 * n, "completed leaf call count") + need(source.head == 0 and len(source.data) == len(raw), "leaf return boundary") + return source.data, meter diff --git a/research/bit2234-callee-substitution/sources/pr-2087/README.md b/research/bit2234-callee-substitution/sources/pr-2087/README.md new file mode 100644 index 0000000000..0ab96ab833 --- /dev/null +++ b/research/bit2234-callee-substitution/sources/pr-2087/README.md @@ -0,0 +1,264 @@ +# A cutoff-independent time bill for the selected bootstrap + +This package proves a **conditional uniform lifting lemma** for the time +hypothesis (H2) in [Josie Elliston's PR1965](https://github.com/CrocSwap/integer-mult-bounds/pull/1965). +It separates the uniform recurrence and completed-wrapper premises from the +conclusion instead of promoting an asymptotic estimate to an all-width one. +For the **native first stage** of selected PR1094, the inherited paid moment +certificate gives an explicit bound + +``` +K = C * max(401501, 2*sigma) +``` + +when every named primitive coefficient below is at most C. This is a bound in +unknown implementation and stock constants, **not** their measurement. No +stock coefficient is supplied, no cutoff is changed, and no new supplier, +kappa, full all-size implementation or formal-kernel theorem is claimed. + +PR1956 identified the carried-time-constant problem; PR1965 proved that time +constants can be absorbed after H2 is available; [ToikY's PR1990](https://github.com/CrocSwap/integer-mult-bounds/pull/1990) +explicitly retained both H2 uniformity and the unknown H3 stock coefficient. +The contribution here is the uniform implication with a complete bill and a +source-bound rational constant. It does not repeat their fourteen stock +headrooms or import the historical m=120 reserve coefficient. + +## Precise premises + +Fix q >= 2, 0 <= a <= s < 1 with s > 0, p = 1-a and tau = 1-s. All widths +are positive integers. The radix and primitive implementations are fixed +before widths and any bootstrap cutoff are chosen. Write a' = (1-s)s+s*a. + +1. **Uniform stopped primitive.** For nonnegative coefficients c_r on integers + 1 <= r < m and m >= 2, normalized time T(n,w) satisfies, for every w >= 1, + + ``` + T(0,w) = 0 + T(n,w) <= Cleaf*w^p (1 <= n < m) + T(n,w) <= sum_r c_r*T(r*floor(n/m),w) + + Cadapt*n + Cpeel*w^p (n >= m). + ``` + + The constants are nonnegative, independent of n, w and the cutoff, and + uniform over the allowed complete spectators and generated prefix controls. + The same normalized recurrence is stated in `notes/stopped-product-interface.tex`, + lines 31-53. The uniform primitive implementation, especially the logical + volume normalization, remains an inherited premise; the finite word does + not prove it. Let g1 and gt be certified positive lower bounds on + `1-sum c_r*(r/m)` and `1-sum c_r*(r/m)^tau`. +2. **Completed endpoints and wrapper tolls.** Each reversed call restores its + row, preserves complete spectators, and has the stated endpoint. Each of + the three ordinary-wrapper shifts costs at most Cshift*n per unit logical + volume. One outer row padding/unpadding, including its scans and bookkeeping, + costs at most Cpad*V, and the padded volume is less than 2V. The completed + old algorithm exchanges residual digits for at most Crem*V*w^p and the + high parts for at most Chi*V*k^p. These are actual charge hypotheses, not + free operations. The constants include radix-to-binary conversions inside + old leaves, their fixed multiplicities, and permitted spectator handling. + PR185's reviewed contract and the retained `three-stage-cover-rows.tex` + explain these calls and restore their rows before reuse. +3. **Fit and stock.** At the particular width e under consideration, set + `w=ceil(e^s)`, take an integer `0 <= k < e/2`, and require + `k <= ceil(sigma*w*(1+log2(e)))`, for fixed sigma >= 0. The actual borrowed + width `ceil(log_q S(e,w))` satisfies this implication if H3 holds. We do not + derive H3 or assume its historical 252 or 57604 constants. Put + `n=floor((e-k)/w)`; the residual contains fewer than w digits. + +These premises are stronger than an eventual big-O statement. A finite spike +in a leaf's cost can satisfy an eventual estimate while violating a proposed +all-width coefficient. The verifier includes such a counterexample. No +unknown spike is silently placed below the selected recorded cutoff. + +## Uniform lifting lemma and proof + +Define + +``` +A = Cadapt/g1 +B = max(Cleaf, Cpeel/gt). +``` + +Strong induction on n proves `T(n,w) <= A*n+B*n^tau*w^p` for every w and n. +At a non-leaf, `r*floor(n/m) <= (r/m)*n < n`. The linear term leaves at +least `g1*A*n = Cadapt*n`. The stopped term leaves at least +`gt*B*n^tau*w^p >= Cpeel*w^p`. For 1 <= n < m, `n^tau >= 1` and B >= Cleaf; +n=0 is the empty body. This is the inherited weighted induction with its +constants and all-width quantifiers made explicit; it is not a new recurrence. + +The complete normalized bill, before estimating powers, is + +``` +(4*A + 6*Cshift)*n + 4*B*n^tau*w^p + + Cpad + Crem*w^p + Chi*k^p. (1) +``` + +The factor four pays **two** reversed calls on a row volume less than **twice** +the original volume. The factor six pays three shifts on that padded volume. +Padding occurs once outside the recursion. The residual and high-part calls +are completed ordinary calls after restriction to the genuine row range; +their internal borrowing is included in Crem and Chi. The five-operation +ordinary wrapper is chronological, not a raw reversed call substituted for +an ordinary one. Nothing in (1) changes recursive child multiplicities. + +For every e >= 1, `e^s <= w <= 2*e^s`, `n <= e/w <= e^(1-s)`, and + +``` +n^tau*w^p <= e^tau*w^(s-a) + <= 2^(s-a)*e^(tau+s*(s-a)) + <= 2*e^(1-a'). +``` + +The nonnegative exponent s-a is a stated premise. For integer k >= 1, +`k^p <= k`; for k=0 both are zero. Thus + +``` +k^p <= 2*sigma*e^s*(1+log2(e)) + 1. +``` + +The ceiling's extra one and Cpad are absorbed by `e^(1-s) >= 1`, not omitted. +Consequently (1) is at most + +``` +K * [e^(1-s) + e^(1-a') + e^s*(1+log2(e)) + w^(1-a)], + +K = max(4*A+6*Cshift+Cpad+Chi, 8*B, 2*sigma*Chi, Crem). (2) +``` + +This is H2 on **every width where the named primitive contracts and stock fit +hold**, with no occurrence of a cutoff L or a carried factor `2^(L*Delta a)`. +The inequality is a mathematical implication, not a proof that all selected +primitive implementations meet its premises. It even handles an empty atom +body, which a purely large-width derivation need not discuss. + +For a binary width E, numerical padding to `q^e`, where +`e=ceil(E/log2(q))`, increases logical volume by less than q^2 and has e <= E. +Thus the same conclusion follows with `q^2*K` and powers of E whenever the +radix-width premises hold; fixed conversion scans must be included in Cpad. +This does not assert that a cutoff stated for radix width e is automatically +the same cutoff for binary width E. + +## Polynomial descriptor preparation without another cutoff + +There is one common source of an implicit extra width threshold. The retained +bit proof, lines 136-145, amortizes polynomial generated-descriptor preparation +against a **complete** q^w target fiber. Suppose its work per prefix is bounded +uniformly by `Cdesc*e^d*w^b`, with fixed nonnegative integer d,b. Put +`D=b+ceil(d/s)`. Since e^s <= w, + +``` +Cdesc*e^d*w^b/q^w <= Cdesc*w^D/2^w <= Cdesc*2^D*D! (3) +``` + +for every integer w >= 1. For D >= 1, +`w^D <= D!*binom(w+D-1,D)`, and the positive generating series gives +`sum_(w>=1) binom(w+D-1,D)/2^w = 2^D`; one summand is no larger than the sum. +For D=0 the bound is immediate. This exact factorial overcharge can be folded +into the relevant Cadapt, Cpeel or Cshift coefficient, multiplied by the number +of charged preparation sites. It adds no new cutoff or unit-cost arithmetic +assumption. A separate uniform bound on d,b,Cdesc and the number of sites is +still required. An incomplete fiber cannot use (3); that failure is an exact +negative control, not an assertion about the selected implementation. + +## Native selected first-stage binding + +All source pins are in [SOURCES.json](SOURCES.json), on main +`564148b82ae9df72163f22106f15e73efca8aff2`, priority revision 4. The chooser's +independent seed is `3c6ed534c7c882d069b0dc2c8cd99397` ([SELECTION.json](SELECTION.json)). +The selected record binds the assembly and its PR589 BIT supplier. The latter +has **m=64**, W=28416, maximum child 42 and the paid profile in `EXPECTED.json`. +The selected complex m=73 producer is not substituted for it. + +The frozen PR1087 assembler specifies the surcharge +`10^-16 * 32*m^2*sum(H_r)/W` additional rank-one children and + +``` +s = min(bit_lower, (1-10^-24)*complex_lower) - 10^-27, +a = 384599/10^10. +``` + +The selected receipt certifies the surcharged moment at bit_lower; both +retained exact upper endpoints are strictly below one. **We authenticate and +reuse that certificate, not recalculate another moment root or claim an +independent supplier replay.** The first-stage exponent is checked against +its recorded value. Exact rational arithmetic gives + +``` +g1 = 16326904278023 / 2890625000000000, +gt = (11/32)*(bit_lower-s) + = 25504319623965913202561177203577795565550087 + / 1280000000000000000000000000000000000000000000000. +``` + +Here gt is a new explicit **sufficient gap transfer**, not an estimated moment: +for x <= rho=42/64 and d=bit_lower-s in (0,1), concavity gives +`x^d <= 1-d*(1-x) <= 1-d*(1-rho)` (the tangent at one). Multiplying the inherited +moment terms at exponent `1-bit_lower` yields `mu_(1-s) < 1-gt`. All coefficients, +including the rank-one surcharge, are nonnegative. Hence `A <= C/g1` and +`B <= C/gt` if all seven coefficients in the premises are at most C. Exact +cross multiplication certifies + +``` +4/g1+8 < 717, +8/gt < 401501, +``` + +so (2) follows with `K=C*max(401501,2*sigma)`. This conservatively pays every +term in (1). It proves no bound on C or sigma and does not assert favorable +practical constants. For example, descriptor degree d=1,b=0 alone becomes +D=597 in (3); that remains a fixed finite time constant, not a stock charge. + +## Reproduction and evidence boundary + +``` +uv run --python 3.12 --no-project python -I -B research/selected-bootstrap-uniform-time/verify.py +uv run --python 3.12 --no-project python scripts/research_package.py --package research/selected-bootstrap-uniform-time +``` + +The registered replay runs the exact checker both normally and under `-O`. +Source hashes are checked before data are consumed; archived Python is read, +never executed. The checker compares the canonical regenerated JSON object +with [RESULT.json](RESULT.json). The finite evidence includes independent +recursion-tree sums versus dynamic programming, exact square comparisons for +rational specializations of the all-width bound, charged padding and complete +endpoint fixtures, factorial inequalities, and semantic/source controls. The +padding, incomplete-fiber and finite-spike fixtures are mathematical countermodels +to weakened hypotheses, not reports of bugs in the selected implementation. +The universal claim rests on the written induction and inequalities, not the +finite sample. No full selected cold replay or hosted CI success is claimed. + +Observed with CPython 3.12: the scientific smoke and registered normal/optimized +replays pass. Each replay checks 6,156 recurrence cases, 539 complete wrapper +bills, 1,664 descriptor inequalities and 1,458 padded endpoints; all 16 controls +reject. The output includes `PASS_SELECTED_BOOTSTRAP_UNIFORM_TIME` and +`PASS_REGISTERED_RESEARCH_PACKAGE`. This evidence does not measure C or sigma. + +## Open next questions + +- Bind each actual selected primitive implementation to the uniform constants + and preparation-site counts in the premises. First inspect logical-volume + normalization, fixed-tape parking and generated prefix work; the inherited + all-size/compiler and tape contracts still block unconditional adoption. +- Derive the actual selected stock envelope sigma with a same-domain producer + and depth argument. This is the separate H3 obligation and is not solved by + a large coefficient cap or by the explicit time constant above. +- Apply the lemma at later stages only after their preceding completed ordinary + contract is established; C may grow with the fixed stage, but must not hide + a width- or cutoff-dependent premise. The result here binds native stage one. + +[Task metadata](TASK.json) records the initial question, complete optimistic +bill, bounded overlap coverage and limits. Claims are confined to this package +and its PR; no discussion post is required. + +## Credit + +Josie Elliston supplied PR1956's carry audit and PR1965's time/space separation; +ToikY supplied PR1990's independent stock-fit audit and explicit H2/H3 limits. +Rohan Arun supplied the reviewed PR185 completed-leaf argument and selected +PR1094 assembly; Jeremy Kothe supplied PR1087's frozen selected producer. +The stopped recurrence and three-stage row/weighted-atom proofs retain their +original repository lineage; DreamingOfClouds's PR589 BIT supplier, on eumemic's +PR555 base, is used through its authenticated selected receipt. These constructions and the +weighted-induction method are not claimed as new. + +Prepared by Adam Gall with substantial OpenAI Codex assistance. Apache-2.0. +No independent human or formal-kernel review is claimed. diff --git a/research/bit2234-callee-substitution/sources/pr-2234/NOTICE.md b/research/bit2234-callee-substitution/sources/pr-2234/NOTICE.md new file mode 100644 index 0000000000..a5ccfbecbd --- /dev/null +++ b/research/bit2234-callee-substitution/sources/pr-2234/NOTICE.md @@ -0,0 +1,54 @@ +# Attribution and source scope + +Jose Manuel (`jmbarrancoml`) prepared this contribution with substantial +OpenAI Codex assistance in mathematical analysis, code, tests and writing. +We use the repository's Apache-2.0 license and retain source notices in the +eight unchanged vendored Python files. `SOURCES.json` records their original +paths, commits and SHA256 values; we checked byte equality against those +Git objects before publication. + +We credit the following predecessors: + +* OpenAI's retained framework and Douglas Colkitt: the stream, ordinary + interchange, row-volume and tape contracts, with their source notices. +* DreamingOfClouds: selected PR589 tuning, on eumemic's PR555 base word. + The lineage includes Dugongue's PR541/548 and rohanarun's PR542. +* alephnan: PR1627, retained as `research/pr589-five-helper-hosting`, for the + literal word, whole-call dirty-helper cancellation and chronological proof. +* eumemic: PR490's whole-owner GL local-ring argument. +* The source527 contributors: retained normal forms, weighted leaf + factorization and ordinary borrowing method, with the existing notices. +* commdata2338: PR2160 selected good normal form, PR2188 mixed descriptor + grammar, and PR1379 unequal-buffer parking boundary. We vendor PR2188's + `descriptor.py` unchanged at `77bb4e8cfe3e8c89f6e281eaf948454ee487796a`. +* RossRichardson: PR2159 full-ring fallback topology, covariance and charge, + at `9022b980917b7a9dd0bf1e9cb8012a16ea30293b`. +* Jose Manuel: PR2157 fixed dyadic routes (`eb1bf93950e9b14f7fadca7892866e9f29a26ad3`), + PR2171 controlled streams (`416aac58960660edced905dc7d914c126d357290`), + PR2195 GL packet integration (`3a1cf78a1ba6322129e42d80c50d21765524d612`), + and PR2207 fallback continuation (`149d55d90d3c0877ed3d78e1deca8eb2f72e0d00`). +* The authors of the retained `moment.py` and `base_two_moment.py` engines: + we reuse their rational arithmetic at one coarse point, with input pins. +* 1337isnot1337: adjacent PR2212 route inventory, at + `cd37bdf943876f81a60522e13cf838a464ed3104`; we do not reproduce that census. + +The new work binds the remaining actual residual labels, gives causal symbolic +field references and completed leaf/header bases, and composes the weighted +caller by strong induction. We derive the resulting ordinary-interchange +saving with the elementary base. We claim neither a new generic weighted +factorization nor a new generic parking lemma. + +The retained `physical_stream.py` contains an explicit weighted-child test +oracle and `qadic_streams.py` contains an ordinary test oracle. We retain +those files unchanged for their sequential primitives and arithmetic. The +new completed leaf/header paths never call those oracles; the replay replaces +them with rejecting functions. Their presence does not implement recursive +children. PROOF.md supplies that separate construction. + +The pending predecessor PRs remain subject to review. We have not merged or +closed them. The repository's selected result remains unchanged. + +For the exact written premises, see the pinned +[PR2195 packet proof](https://github.com/CrocSwap/integer-mult-bounds/blob/3a1cf78a1ba6322129e42d80c50d21765524d612/research/selected-bit-local-ring-sweeps/PROOF.md), +[PR2171 adapter proof](https://github.com/CrocSwap/integer-mult-bounds/blob/416aac58960660edced905dc7d914c126d357290/research/selected-bit-controlled-streams/PROOF.md) +and [PR2207 fallback proof](https://github.com/CrocSwap/integer-mult-bounds/blob/149d55d90d3c0877ed3d78e1deca8eb2f72e0d00/research/selected-bit-fallback-streams/PROOF.md). diff --git a/research/bit2234-callee-substitution/sources/pr-2234/PROOF.md b/research/bit2234-callee-substitution/sources/pr-2234/PROOF.md new file mode 100644 index 0000000000..6c410cab57 --- /dev/null +++ b/research/bit2234-callee-substitution/sources/pr-2234/PROOF.md @@ -0,0 +1,433 @@ +# Recursive closure of the selected BIT interchange + +We give a written construction on a fixed number of finite-alphabet multitape +streams. We retain the sequential stream model of `02-streams.tex`: complete +address ranges, arbitrary Boolean payload, charged scans, counters, rewinds and +scratch erasure. We prove an ordinary binary chunk-interchange bound + + O(V E^(1-a)), a = 169711/100000000 = 0.00169711, + +for two complete E-bit address chunks and arbitrary complete spectators, where +V counts payload bits. The machine restores spectators and clears its work. +We fix one odd prime q>2^80 throughout; constants and the fixed tape count may +depend on q and the selected word. We make no practical runtime claim. + +We supply a mathematical algorithm and finite interface checks. We have not +translated the entire recursive machine into transition tables or a proof +assistant. Reviewers must assess the composition argument below. The selected +finite certificate and the multiplication theorem have further interfaces, +including the complex supplier and analytic transfer; we leave their status +unchanged. + +## 1. Sources and the recursive contract + +We use DreamingOfClouds' selected PR589 word, building on eumemic's PR555 word, +and alephnan's PR1627 literal/chronological proof. We reuse the GL local-ring +packet integration of PR2195, the good adapters of PR2171, the fallback word +of PR2159/PR2207, and commdata2338's PR2188 weight grammar. Source527 already +gives the weighted factorization and outer borrowing method. PR1379 supplies +the unequal-buffer parking boundary. `SOURCES.json` pins the executable inputs; +`NOTICE.md` identifies the pending source commits and mathematical reuse. + +Fix an original radix-q width e, c=17/10000, and w=ceil(e^c). Put B=q^w and +R=Z/B. We keep w fixed throughout one coarse recursion. Let C_n reverse n +atom positions. For a diagonal unit vector A, we construct + + F_A(H,D) = (A C_n D, C_n A^-1 H). + +We quantify over any two ordered complete n-atom chunks, with arbitrary +complete preceding, intervening and following fields. This includes two +subchunks of one former bank, which we need for fallback reversals. We allow +arbitrary correlated dirty payload values. + +We generate A from a constant unit by the Good and FallbackPair expressions +below. A may read earlier frozen matrix fields; it may not read this node's +fresh family, matrix or unused stock. A unit child starts a new constant +expression but retains its global generation depth. We bound that depth by +the original root width, including after such a reset. + +At return we require the specified address permutation on I/O, pointwise +restoration of row and spectator coordinates, empty local work and restored +head positions. For a parking top h, we visit no cell below h-1 and write no +cell below h. We require a time bound uniform in parked contents and h. + +## 2. Actual residuals and full-ring preparation + +PR1627 reconstructs 636 rational frame projectors and proves the nesting +identities used by both selected literal programs. Their entries lie in +Z[1/2]. For an idempotent P0 of rational rank r, its characteristic polynomial +is T^(64-r)(T-1)^r. Reduction modulo an odd q preserves this identity and +idempotent diagonalizability, hence rank r, including when q divides r. + +Choose independent image columns of P0 and kernel columns of I-P0 modulo q. +Their lifts form a unit matrix B0 over R and satisfy + + P0 = B0 diag(I_r,0) B0^-1. + +We compute this identity in control arithmetic. We do not move payload through +B0. For the actual owner chart sigma and raw physical header g, the provider +passes g sigma B0 to the retained coordinate normalizer. It therefore computes +exactly P=g sigma P0 sigma^-1 g^-1. + +For MOVE, we use the positive nested frame difference and the actual owner +sigma. The common stage projector cancels. The reflected orientation gives +the same positive residual. For COPY, we first copy and align the source +packet to d=g sigma. Its private header is d and its projector label is P0; +we set its additional chart to I. Applying sigma again would change the +operator. ERASE retains the literal transported-source equality guard. + +For an idle remainder, we subtract the actual hosted slots from its pending +axes and use the fixed family chart. We skip the zero remainder. The provider +binds 28,278 canonical requests and 32 replicas, giving + + H_1=381024, H_2=400416, H_3=22752, H_4=26880, + H_5=29376, H_6=17376, H_7=26784, H_42=288. + +We obtain 541 distinct base labels and 1,235 assembled charts. The finite +checks verify image/kernel bases over Z/9 and Z/25 for each label, and 120 +full 128-coordinate operators from selected MOVE, COPY and idle requests. +These cases supplement the identities; they do not enumerate GL64(R). + +## 3. One schedule per complete low packet + +Write g=g0+qG with g0 in GL64(F_q) and G in [q^(w-1)]^4096. For a fixed +request, call g0 good when the first r northeast pivots of PC are units. +Equivalently, require the leading k principal minors of P to be nonzero +modulo q for 1<=k<=r. Unit tests depend only on g0. The full coefficients +still depend on G. + +For each k, multiply its minor by det(g)^k to obtain a polynomial of degree +at most 64k in the entries of g. Conjugating the fixed split rank-r projector +to diag(I_r,0) gives a nonzero witness. The union of these zero sets has +fraction at most 64r(r+1)/(2q) in all matrices. Since + + |GL64(F_q)|/q^4096 = product_(i=1)^64 (1-q^-i) > 1/2, + +the bad fraction for this request is at most 2*64^3/q<10^-16. We use this +bound separately for each paid edge. We do not require one matrix to be good +for every label or multiply the bound by the number of labels. + +On a good packet, unweighted northeast elimination gives unit-lower matrices +L,R0 and a pivot vector delta. Split rank and a unit rank-r minor force the +remaining Schur block to vanish over R itself. We retain q-multiples in the +arithmetic; reduction modulo q alone would not establish that conclusion. +The normal-form factorization in source527/PR2171 uses ordered head, tail +and cross ADDs, one weighted child, and the inverse adapters. For n=64f, + + A_child[k f+j] = A[k f+j] delta_k, 0<=k=1. Recompute on split and merge rather than retaining +an array indexed by the high fibre. Ripple counters have amortized linear +movement cost; initialize them once per scan and do not reread unrelated +spectator counters per fibre. Fixed low tables and finite labels depend on +q, not e. Thus these scans have the stated uniform bounds. For independently +chosen n,w,d, retain the preparation quotient instead of this absorption. + +The selected word has fixed length. Good and bad bodies use O(n) ordered +atom passes; header routes use O(Vw) each; selections, XORs, erasure and +parking use O(V) each. We include their finite q-dependent multiplicities +in a constant C. The local nonrecursive charge is C V(n+w), including the +remainder leaf. This is an asymptotic accounting, not an explicit optimized +finite invoice for the selected multiplier. PR2212 prices the separate +same-family route inventory and leaves further whole-invocation charges. + +Normalize by logical volume and bound the worst generated call by T(n,w). +For positive widths below 64, T<=Cw. The bad fraction is at most epsilon=10^-16 +for each request, and each fallback has at most 32*64^2 children of width at +most f=floor(n/64). We may overcount good calls on bad classes, obtaining + + T(n,w) <= sum_r (H_r/W) T(r f,w) + + epsilon F/W * max_(1<=j<=f) T(j,w) + C(n+w), + F=32*64^2*sum_r H_r=118606528512. + +We prove a monotone upper bound, so the maximum causes no extra factor. +Define mu_t=(sum H_r(r/64)^t + epsilon F(1/64)^t)/W. The two retained outward +rational engines independently give + + mu_1 = 2874298095721977/2890625000000000 < 199/200, + mu_(1-c) < 9999/10000. + +Induct on n and use f<=n/64. Increasing C to cover the leaf constants gives + + T(n,w) <= 200 C n + 10000 C n^(1-c) w. + +Indeed the first term leaves at least Cn after the recursive linear mass, +and the second leaves at least C n^(1-c)w>=Cw. We treat n=0 separately. +The resulting constants are independent of ancestor contents, stack top, +row multiplicity and original e. + +## 8. Internal borrowing and binary interchange + +Choose the sufficient stock S=K(w)^D(e) from the original width e, before +choosing a body width. Since M=64: + f=n//64 + for child in [r*f for r in range(1,43)]+[f//2]: + if child: + need(depth(child)<=d-1,"fresh stock exponent sufficient") + need(0=1 and gcd(integer,radix)==1,"fixed integer unit") + need(len(source.bits)==radix*block*fibres,"complete fixed-scale fibres") + if integer==1 or radix==1: + need(source.head==0,"identity scale origin") + return source + pieces=[Tape(meter.movement) for _ in range(integer)];out=Tape(meter.movement) + source.rewind();inv=pow(radix,-1,integer) + lengths=[((j+1)*radix+integer-1)//integer-(j*radix+integer-1)//integer + for j in range(integer)] + if not inverse: + for _ in range(fibres): + for j,length in enumerate(lengths): + copy_bits(source,pieces[j],length*block) + for piece in pieces:piece.rewind() + for _ in range(fibres): + for value in range(radix): + copy_bits(pieces[(-value*inv)%integer],out,block) + else: + for _ in range(fibres): + for value in range(radix): + copy_bits(source,pieces[(-value*inv)%integer],block) + for piece in pieces:piece.rewind() + for _ in range(fibres): + for j,length in enumerate(lengths): + copy_bits(pieces[j],out,length*block) + source.finished() + for piece in pieces:piece.finished();piece.erase() + source.erase();out.rewind() + meter.max_bucket_tapes=max(meter.max_bucket_tapes,integer) + return out + + +def negate(source,radix,block,fibres,meter): + need(len(source.bits)==radix*block*fibres,"complete header sign fibres") + source.rewind();out,reverse,small=(Tape(meter.movement) for _ in range(3)) + for _ in range(fibres): + copy_bits(source,out,block) + copy_bits(source,reverse,(radix-1)*block) + for _value in range(radix-1): + for _bit in range(block):small.write(pop_bit(reverse)) + for _bit in range(block):out.write(pop_bit(small)) + need(not reverse.bits and not small.bits,"header sign scratch closure") + source.finished();source.erase();out.rewind();meter.fixed_signs+=1 + return out + + +def scale(source,radix,block,fibres,coefficient,meter): + coefficient=F(coefficient);a,b=abs(coefficient.numerator),coefficient.denominator + need(a>0 and a&(a-1)==0 and b&(b-1)==0,"fixed dyadic route alphabet") + if coefficient<0:source=negate(source,radix,block,fibres,meter) + source=multiply_fixed(source,radix,block,fibres,a,meter) + return multiply_fixed(source,radix,block,fibres,b,meter,True) + + +def ordinary_fields(source,q,width,before,middle,suffix,meter): + radix=q**width + need(len(source.bits)==before*radix*middle*radix*suffix,"header ordinary extent") + if width==0: + return source + radices=(q,)*width+(middle,)+(q,)*width + for position in range(width): + source=digit_swap(source,radices,position,width+1+position,suffix,q,meter) + meter.ordinary_atom_swaps+=1 + return source + + +def add(source,q,width,low_x,low_y,coefficient,before,middle,suffix,meter, + reversed_fields=False,omit_carry=False): + coefficient=F(coefficient);radix=q**(width-1) + new,carry=low_update(low_x,low_y,coefficient,q) + if omit_carry:carry=0 + if radix==1: + return source,new + if reversed_fields: + source=ordinary_fields(source,q,width-1,before,middle,suffix,meter) + fibres=before*radix*middle + source=scale(source,radix,suffix,fibres,F(coefficient.denominator),meter) + source=rotate(source,radix,suffix,fibres, + lambda prefix:coefficient.numerator*((prefix//middle)%radix)+carry,meter) + source=scale(source,radix,suffix,fibres,F(1,coefficient.denominator),meter) + if reversed_fields: + source=ordinary_fields(source,q,width-1,before,middle,suffix,meter) + return source,new + + +def finite_classes(source,before,classes,block,permutation,meter): + need(sorted(permutation)==list(range(classes)),"fixed low-class permutation") + need(len(source.bits)==before*classes*block,"low-class packet extent") + pieces=[Tape(meter.movement) for _ in range(classes)];out=Tape(meter.movement) + source.rewind() + for _ in range(before): + for old in range(classes):copy_bits(source,pieces[permutation[old]],block) + source.finished() + for piece in pieces:piece.rewind() + for _ in range(before): + for piece in pieces:copy_bits(piece,out,block) + for piece in pieces:piece.finished();piece.erase() + source.erase();out.rewind();meter.max_bucket_tapes=max(meter.max_bucket_tapes,classes) + return out + + +def scale_affine(source,q,width,low,coefficient,before,suffix,meter): + coefficient=F(coefficient);radix=q**(width-1) + new,carry=low_update(0,low,coefficient,q,True) + if radix==1:return source,new + source=scale(source,radix,suffix,before,F(coefficient.numerator),meter) + source=rotate(source,radix,suffix,before,lambda _p:carry,meter) + source=scale(source,radix,suffix,before,F(1,coefficient.denominator),meter) + return source,new diff --git a/research/bit2234-callee-substitution/sources/pr-2234/leaf.py b/research/bit2234-callee-substitution/sources/pr-2234/leaf.py new file mode 100644 index 0000000000..1b20c0ad44 --- /dev/null +++ b/research/bit2234-callee-substitution/sources/pr-2234/leaf.py @@ -0,0 +1,139 @@ +"""Completed weighted leaves from sequential digit swaps, ADDs and a sign. + +The source527 factorization is inherited. No weighted-child or ordinary-swap +oracle is accepted by this implementation. +""" +from dataclasses import dataclass, field +from math import prod + +from controlled_stream import Tape, Meter, copy_bits, controlled_add +from physical_stream import Layout, Execution, sign_pass +from provider import need, build_weights + + +@dataclass +class LeafMeter: + movement: Meter = field(default_factory=Meter) + digit_swaps: int = 0 + ordinary_atom_swaps: int = 0 + ordered_shifts: int = 0 + fixed_signs: int = 0 + opaque_child_calls: int = 0 + max_bucket_tapes: int = 0 + + +def digit_swap(source,radices,first,second,payload,q,meter): + """Swap two radix-q digits using q^2 sequential bucket streams.""" + need(0<=first=n) + for position in range(width): + if omit_digit and position==width-1: + continue + source=digit_swap(source,digits,axis(first_atom,position),axis(second_atom,position), + layout.payload,q,meter) + meter.ordinary_atom_swaps+=1 + return source + + +def shift(source,recipes,layout,first_atom,second_atom,index,inverse,meter, + wrong_inverse=False,low_ancestors=False): + first,second=layout.axis(first_atom),layout.axis(second_atom) + before=layout.unused*prod(layout.radices[:first]) + middle=prod(layout.radices[first+1:second]) + suffix=layout.payload*prod(layout.radices[second+1:]) + def evaluate(recipe): + weights,arithmetic=build_weights(recipe,low_ancestors) + a=weights.value(index) + arithmetic.counts["leaf_weight_requests"]+=1 + c=-(a if wrong_inverse else arithmetic.inv(a))%layout.modulus if inverse else a + return c,arithmetic + output=controlled_add(source,recipes,before,layout.modulus,middle,suffix,evaluate) + source.erase();meter.ordered_shifts+=1 + return output + + +def execute_leaf(raw,recipes,count,offset=0,unused=1,gap=1,payload=1, + wrong_inverse=False,low_ancestors=False,omit_digit=False): + need(bool(recipes) and 0<=count<64 and offset>=0,"stopped leaf domain") + q,width=recipes[0].q,recipes[0].width + need(all((r.q,r.width)==(q,width) for r in recipes),"one leaf atom ring") + layout=Layout(count,1,q**width,unused,gap,payload) + need(len(raw)==len(recipes)*unused*layout.rows*payload,"complete weighted leaf payload") + if count: + for recipe in recipes: + weights,_=build_weights(recipe) + need(offset+count<=weights.size,"leaf weight slice extent") + meter=LeafMeter();source=Tape(meter.movement,raw) + for i in range(count): + first,second=i,2*count-1-i + source=ordinary_swap(source,layout,q,width,first,second,meter,omit_digit) + source=shift(source,recipes,layout,first,second,offset+i,False,meter, + wrong_inverse,low_ancestors) + source=ordinary_swap(source,layout,q,width,first,second,meter,omit_digit) + source=shift(source,recipes,layout,first,second,offset+i,True,meter, + wrong_inverse,low_ancestors) + source=ordinary_swap(source,layout,q,width,first,second,meter,omit_digit) + source=shift(source,recipes,layout,first,second,offset+i,False,meter, + wrong_inverse,low_ancestors) + source=ordinary_swap(source,layout,q,width,first,second,meter,omit_digit) + sign_execution=Execution(meter.movement) + source=sign_pass(source,layout,layout.axis(second),sign_execution) + meter.fixed_signs+=sign_execution.fixed_sign_passes + need(source.head==0 and len(source.bits)==len(raw),"completed leaf return boundary") + need(meter.ordinary_atom_swaps==4*count and meter.ordered_shifts==3*count and + meter.fixed_signs==count and meter.opaque_child_calls==0,"literal leaf call inventory") + if not omit_digit: + need(meter.digit_swaps==4*count*width,"elementary ordinary implementation bill") + return source.bits,meter,layout + + +def direct_leaf(raw,recipes,layout,offset=0): + """Independent direct F_A address permutation; no factor execution.""" + out=[None]*len(raw);n=layout.dimension;modulus=layout.modulus + for parent,recipe in enumerate(recipes): + descriptor,_=build_weights(recipe) + weights=[descriptor.value(offset+i) for i in range(n)] + for stock in range(layout.unused): + for row in range(layout.rows): + values=layout.decode(row);new=values[:] + for i,a in enumerate(weights): + first,second=layout.axis(i),layout.axis(2*n-1-i) + new[first]=a*values[second]%modulus + new[second]=pow(a,-1,modulus)*values[first]%modulus + destination=layout.encode(new) + src=((parent*layout.unused+stock)*layout.rows+row)*layout.payload + dst=((parent*layout.unused+stock)*layout.rows+destination)*layout.payload + need(out[dst] is None,"direct leaf address bijection") + out[dst:dst+layout.payload]=raw[src:src+layout.payload] + need(all(x is not None for x in out),"direct leaf full coverage") + return out diff --git a/research/bit2234-callee-substitution/sources/pr-2234/qadic_streams.py b/research/bit2234-callee-substitution/sources/pr-2234/qadic_streams.py new file mode 100644 index 0000000000..dd50529326 --- /dev/null +++ b/research/bit2234-callee-substitution/sources/pr-2234/qadic_streams.py @@ -0,0 +1,240 @@ +"""Sequential stream lowering with a charged completed-interchange oracle. + +The split/merge operations instantiate the retained ordered-affine stream lemma. +Jose Manuel, with substantial OpenAI Codex assistance. Apache-2.0. +""" + +from collections import Counter +from dataclasses import dataclass, field +from fractions import Fraction as F +from math import gcd + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +@dataclass +class Meter: + reads: int = 0 + writes: int = 0 + moves: int = 0 + primitives: Counter = field(default_factory=Counter) + ordinary: list = field(default_factory=list) + + +class Tape: + """Append-only output or sequential input; no seek operation.""" + def __init__(self, meter, bits=()): + self.meter, self.bits, self.head = meter, list(bits), 0 + + def read(self): + need(self.head < len(self.bits), "read beyond stream") + value = self.bits[self.head] + self.head += 1 + self.meter.reads += 1 + self.meter.moves += 1 + return value + + def write(self, value): + need(self.head == len(self.bits), "output must append") + need(value in (0,1), "bit alphabet") + self.bits.append(value) + self.head += 1 + self.meter.writes += 1 + self.meter.moves += 1 + + def rewind(self): + self.meter.moves += self.head + self.head = 0 + + def finished(self): + need(self.head == len(self.bits), "unconsumed stream suffix") + + +def copy_bits(source, target, count): + for _ in range(count): + target.write(source.read()) + + +def rotate_fibers(source, qpower, block, fibers, offset): + """Move data from coordinate y to y+offset(prefix), modulo qpower.""" + need(qpower>=1 and block>=1 and fibers>=1, "complete fiber dimensions") + need(len(source.bits)==qpower*block*fibers, "fiber volume") + meter=source.meter;meter.primitives["ordered_shift"]+=1 + left,right,out=(Tape(meter) for _ in range(3)) + source.rewind() + for prefix in range(fibers): + a=offset(prefix)%qpower + copy_bits(source,left,(qpower-a)*block) + copy_bits(source,right,a*block) + source.finished();left.rewind();right.rewind() + for prefix in range(fibers): + a=offset(prefix)%qpower + copy_bits(right,out,a*block) + copy_bits(left,out,(qpower-a)*block) + left.finished();right.finished() + return out + + +def multiply_fibers(source, qpower, block, fibers, c, inverse=False): + """Fixed positive integer unit, implemented by monotone pieces.""" + need(c>=1 and gcd(c,qpower)==1, "fixed unit multiplier") + need(len(source.bits)==qpower*block*fibers, "scaling volume") + meter=source.meter;meter.primitives["inverse_integer_scale" if inverse else "integer_scale"]+=1 + if c==1 or qpower==1: + return source + source.rewind() + pieces=[Tape(meter) for _ in range(c)];out=Tape(meter) + lengths=[((j+1)*qpower+c-1)//c-(j*qpower+c-1)//c for j in range(c)] + inv=pow(qpower,-1,c) + if not inverse: + for _ in range(fibers): + for j,length in enumerate(lengths):copy_bits(source,pieces[j],length*block) + for tape in pieces:tape.rewind() + for _ in range(fibers): + for y in range(qpower):copy_bits(pieces[(-y*inv)%c],out,block) + else: + for _ in range(fibers): + for y in range(qpower):copy_bits(source,pieces[(-y*inv)%c],block) + for tape in pieces:tape.rewind() + for _ in range(fibers): + for j,length in enumerate(lengths):copy_bits(pieces[j],out,length*block) + source.finished() + for tape in pieces:tape.finished() + return out + + +def negate_fibers(source,qpower,block,fibers): + """Reverse blocks1..Q-1, restoring the bit order inside each block.""" + need(len(source.bits)==qpower*block*fibers,"negation volume") + meter=source.meter;meter.primitives["negation"]+=1 + source.rewind();out=Tape(meter) + for _ in range(fibers): + copy_bits(source,out,block) + stack=[] + for _ in range((qpower-1)*block): + stack.append(source.read());meter.writes+=1;meter.moves+=1 + for _ in range(qpower-1): + temporary=[] + for _ in range(block): + temporary.append(stack.pop());meter.reads+=1;meter.writes+=1;meter.moves+=2 + for _ in range(block): + out.write(temporary.pop());meter.reads+=1;meter.moves+=1 + need(not stack,"local stack restored") + source.finished() + return out + + +def unit_scale(source,qpower,block,fibers,c): + c=F(c);need(c and gcd(c.numerator*c.denominator,qpower)==1,"rational unit") + if c<0:source=negate_fibers(source,qpower,block,fibers) + if abs(c.numerator)!=1:source=multiply_fibers(source,qpower,block,fibers,abs(c.numerator)) + if c.denominator!=1:source=multiply_fibers(source,qpower,block,fibers,c.denominator,True) + return source + + +def completed_swap_oracle(source,qpower,before,middle,suffix): + """Pad, invoke the assumed complete binary swap, and unpad. + + Random access occurs only inside the declared ordinary-callee oracle. + Its time is charged as T_old, never as a linear stream primitive. + """ + need(len(source.bits)==before*qpower*middle*qpower*suffix,"swap volume") + if qpower==1:return source + u=(qpower-1).bit_length();power=1<=3 and q%2 and width>=1,"odd radix and positive width") + high=q**(width-1);c=F(c);new,carry=low_update(low_x,low_y,c,q) + if omit_carry:carry=0 + return add_high(source,high,c,lambda _:carry,before,middle,suffix,reversed_fields),new + + +def physical_scale(source,q,width,low,c,before=1,suffix=1): + high=q**(width-1);c=F(c);new,carry=low_update(0,low,c,q,True) + return scale_high(source,high,c,lambda _:carry,before,suffix),new diff --git a/research/bit2234-callee-substitution/test_integrity.py b/research/bit2234-callee-substitution/test_integrity.py new file mode 100644 index 0000000000..2caf075465 --- /dev/null +++ b/research/bit2234-callee-substitution/test_integrity.py @@ -0,0 +1,62 @@ +#!/usr/bin/env python3 +"""Public CLI positive relocation and source/receipt rejection controls.""" +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile + +HERE = Path(__file__).resolve().parent + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def execute(directory, optimized=False): + args = [sys.executable, "-I", "-B"] + if optimized: + args.append("-O") + args.append(str(directory / "verify.py")) + return subprocess.run(args, cwd=directory, text=True, stdout=subprocess.PIPE, + stderr=subprocess.PIPE, timeout=90) + + +def main(): + # The system temporary directory is provided by the running environment. + # No source file in the live package is ever changed by these controls. + with tempfile.TemporaryDirectory(prefix="bit2234-callee-") as temporary: + copy = Path(temporary) / "export" + shutil.copytree(HERE, copy, ignore=shutil.ignore_patterns("__pycache__")) + result = execute(copy) + need(result.returncode == 0 and "PASS_BIT2234_CALLEE_SUBSTITUTION" in result.stdout, + "relocated Git-free replay: " + result.stderr) + source = copy / "sources/pr-2234/header_streams.py" + original = source.read_bytes() + source.write_bytes(original.replace(b"width-1", b"width+1", 1)) + result = execute(copy, True) + need(result.returncode != 0 and "vendored source SHA256" in result.stderr, + "source corruption must reject before executing code") + source.write_bytes(original) + receipt = copy / "RESULT.json" + original_receipt = receipt.read_text() + for key, change in [("adapter", lambda x: x.update(cases=x["cases"] + 1)), + ("adapter", lambda x: x.update(binary_calls=True)), + ("adapter", lambda x: x.update(cases=float(x["cases"])) )]: + data = json.loads(original_receipt) + change(data[key]) + receipt.write_text(json.dumps(data)) + result = execute(copy, True) + need(result.returncode != 0 and "exact typed receipt comparison" in result.stderr, + "changed typed receipt must reject") + receipt.write_text(original_receipt.replace('"source_files": 8', '"source_files": 8, "source_files": 8')) + result = execute(copy) + need(result.returncode != 0 and "duplicate JSON key" in result.stderr, + "duplicate receipt key must reject") + print("PASS_BIT2234_CALLEE_INTEGRITY relocated=1 source_faults=1 receipt_faults=4") + + +if __name__ == "__main__": + main() diff --git a/research/bit2234-callee-substitution/verify.py b/research/bit2234-callee-substitution/verify.py new file mode 100644 index 0000000000..0cd7b5f0f6 --- /dev/null +++ b/research/bit2234-callee-substitution/verify.py @@ -0,0 +1,372 @@ +#!/usr/bin/env python3 +"""Exact endpoint and source-API checks; written proof is in README.md.""" +import argparse +import ast +from fractions import Fraction as F +from hashlib import sha256, sha1 +from itertools import product +from math import gcd, prod +from pathlib import Path +import json +import sys + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +import adapter as a + + +def unique_object(pairs): + out = {} + for key, value in pairs: + a.need(key not in out, "duplicate JSON key") + out[key] = value + return out + + +def read_json(path): + return json.loads(path.read_text(), object_pairs_hook=unique_object) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":"), allow_nan=False) + + +def authenticate(): + sources = read_json(HERE / "SOURCES.json") + for item in sources["vendored_files"]: + data = (HERE / item["path"]).read_bytes() + a.need(sha256(data).hexdigest() == item["sha256"], "vendored source SHA256: " + item["path"]) + blob = b"blob " + str(len(data)).encode() + b"\0" + data + a.need(sha1(blob).hexdigest() == item["git_blob"], "vendored Git blob: " + item["path"]) + return len(sources["vendored_files"]) + + +def decode(index, radices): + result = [] + for radix in reversed(radices): + index, value = divmod(index, radix) + result.append(value) + a.need(index == 0, "address extent") + return result[::-1] + + +def encode(values, radices): + out = 0 + for value, radix in zip(values, radices, strict=True): + a.need(0 <= value < radix, "coordinate extent") + out = out * radix + value + return out + + +def direct(raw, radices, change): + """Independent address-scatter oracle, used only by verification.""" + out = [None] * len(raw) + for index, label in enumerate(raw): + values = decode(index, radices) + change(values) + target = encode(values, radices) + a.need(out[target] is None, "oracle injectivity") + out[target] = label + a.need(all(x is not None for x in out), "oracle surjectivity") + return out + + +def swap_oracle(raw, q, width, before, middle, suffix): + def change(v): + v[1], v[3] = v[3], v[1] + return direct(raw, [before, q**width, middle, q**width, suffix], change) + + +def check_adapters(): + count = volume = calls = 0 + digest = sha256() + for q, width, shape in product((3, 5), range(4), + ((1, 1, 1), (2, 1, 1), (1, 3, 1), (1, 1, 2), (2, 3, 2))): + before, middle, suffix = shape + size = before * q**(2 * width) * middle * suffix + raw = list(range(size)) + source, meter = a.Stream(raw[:]), a.Meter() + out = a.qadic_exchange(source, q, width, before, middle, suffix, meter) + a.need(out.data == swap_oracle(raw, q, width, before, middle, suffix) and out.head == 0, + "padded swap endpoint") + a.need(len(meter.calls) == int(width > 0), "exactly one completed call, except width zero") + if width: + call = meter.calls[0] + a.need(not source.data and source.head == 0, "consumed original input") + a.need((call["before"], call["middle"], call["suffix"]) == shape, "spectators not padded") + a.need(meter.pad_reads == meter.crop_writes == size, "genuine copy counts") + a.need(meter.pad_writes == meter.crop_reads == call["padded_volume"], "dummy scan counts") + a.need(call["binary_width"] <= (q - 1).bit_length() * width, "integer binary-width bound") + else: + a.need(out is source and meter.zero_width == 1, "zero-width identity") + digest.update(canonical([q, width, shape, out.data]).encode()) + count += 1 + volume += size + calls += len(meter.calls) + # Exhaust every genuine Boolean payload at Q=3; the callback checks that + # padding introduced only actual bits, not a sentinel alphabet extension. + for bits in product((0, 1), repeat=9): + def binary_only(source, *args): + a.need(all(type(v) is int and v in (0, 1) for v in source.data), "binary-only callee input") + return a.binary_reference(source, *args) + result = a.qadic_exchange(a.Stream(list(bits)), 3, 1, 1, 1, 1, a.Meter(), binary_only) + a.need(result.data == swap_oracle(list(bits), 3, 1, 1, 1, 1), "Boolean payload padding") + return {"cases": count, "coordinates": volume, "binary_calls": calls, + "exhaustive_boolean_inputs": 512, "sha256": digest.hexdigest()} + + +def check_leaves(): + count = coordinates = calls = 0 + digest = sha256() + for q, width, n in [(3, 1, 0), (3, 1, 1), (3, 2, 1), (5, 1, 1), + (5, 2, 1), (3, 1, 2), (3, 2, 2)]: + radix = q**width + units = [v for v in range(1, radix) if gcd(v, radix) == 1] + weights = [[units[(2 * p + i + 1) % len(units)] for i in range(n)] for p in range(2)] + radices = [2] + [radix] * n + [2] + [radix] * n + [2] + raw = list(range(prod(radices))) + out, meter = a.weighted_leaf(raw, q, width, weights, gap=2, suffix=2) + def change(v): + old = v[:] + for i, weight in enumerate(weights[v[0]]): + first, second = 1 + i, 2 * n + 1 - i + v[first] = weight * old[second] % radix + v[second] = pow(weight, -1, radix) * old[first] % radix + a.need(out == direct(raw, radices, change), "weighted leaf full endpoint") + a.need(len(meter.calls) == 4 * n, "leaf completed call inventory") + digest.update(canonical([q, width, weights, out]).encode()) + count += 1 + coordinates += len(raw) + calls += len(meter.calls) + return {"cases": count, "coordinates": coordinates, "binary_calls": calls, "sha256": digest.hexdigest()} + + +class Tape: + """Symbolic interpreter for source headers; real heads and consumed scratch. + + Distinct integer tokens prove the whole position permutation in one run. + Source functions never inspect tokens, so this also checks arbitrary bits. + """ + def __init__(self, meter, bits=()): + self.meter, self.bits, self.head = meter, list(bits), 0 + def read(self): + a.need(self.head < len(self.bits), "source header read extent") + value = self.bits[self.head] + self.head += 1 + return value + def write(self, value): + a.need(self.head == len(self.bits), "source header append") + self.bits.append(value) + self.head += 1 + def rewind(self): + self.head = 0 + def finished(self): + a.need(self.head == len(self.bits), "source header consumed") + def erase(self): + self.bits.clear() + self.head = 0 + + +class HeaderMeter: + def __init__(self): + self.movement = None + self.ordered_shifts = self.fixed_signs = self.max_bucket_tapes = 0 + self.adapters = a.Meter() + + +def source_functions(path, names, namespace): + tree = ast.parse(path.read_text()) + chosen = [node for node in tree.body if isinstance(node, ast.FunctionDef) and node.name in names] + a.need({node.name for node in chosen} == set(names), "all selected source functions present") + exec(compile(ast.Module(body=chosen, type_ignores=[]), str(path), "exec"), namespace) + + +def load_header(omit_return=False): + def copy_bits(source, target, count): + for _ in range(count): + target.write(source.read()) + def pop_bit(tape): + a.need(bool(tape.bits) and tape.head == len(tape.bits), "stack pop at end") + tape.head -= 1 + return tape.bits.pop() + def ordinary_fields(source, q, width, before, middle, suffix, meter): + if omit_return and meter.adapters.calls: + return source + a.need(source.head == 0, "source header adapter entry") + result = a.qadic_exchange(a.Stream(source.bits[:]), q, width, before, middle, suffix, meter.adapters) + source.erase() + return Tape(meter.movement, result.data) + ns = {"F": F, "gcd": gcd, "Tape": Tape, "copy_bits": copy_bits, + "need": a.need, "pop_bit": pop_bit, "ordinary_fields": ordinary_fields} + source_functions(HERE / "sources/pr-2234/qadic_streams.py", ["low_update"], ns) + source_functions(HERE / "sources/pr-2234/header_streams.py", + ["rotate", "multiply_fixed", "negate", "scale", "add", "scale_affine"], ns) + return ns + + +def header_case(ns, q, width, low_x, low_y, coefficient, reverse, omit_carry=False): + radix = q**(width - 1) + radices = [2, radix, 2, radix, 2] + raw = list(range(prod(radices))) + meter = HeaderMeter() + result, new_low = ns["add"](Tape(None, raw), q, width, low_x, low_y, + coefficient, 2, 2, 2, meter, reversed_fields=reverse, + omit_carry=omit_carry) + cmod = coefficient.numerator * pow(coefficient.denominator, -1, q**width) % (q**width) + def change(v): + xi, yi = (3, 1) if reverse else (1, 3) + x = low_x + q * v[xi] + y = low_y + q * v[yi] + target = (y + cmod * x) % (q**width) + a.need(target % q == new_low, "header low/high agreement") + v[yi] = target // q + a.need(result.head == 0 and result.bits == direct(raw, radices, change), + "source header endpoint with substituted callee") + a.need(len(meter.adapters.calls) == (2 if reverse and width > 1 else 0), + "two high-field calls in reversed header ADD") + return len(raw), len(meter.adapters.calls), result.bits + + +def check_headers(): + ns = load_header() + count = coordinates = calls = 0 + digest = sha256() + alphabet = [F(sign * numerator, denominator) for sign in (-1, 1) + for numerator, denominator in ((1, 4), (1, 2), (1, 1), (2, 1), (4, 1))] + for q, width, coefficient, reverse in product((3, 5), (1, 2, 3), alphabet, (False, True)): + lows = product(range(q), repeat=2) if width < 3 else [(0, 0), (1, q - 1), (q - 1, 1)] + for low_x, low_y in lows: + size, used, result = header_case(ns, q, width, low_x, low_y, coefficient, reverse) + digest.update(canonical([q, width, low_x, low_y, str(coefficient), reverse, result]).encode()) + count += 1 + coordinates += size + calls += used + return {"cases": count, "coordinates": coordinates, "binary_calls": calls, + "coefficient_alphabet": list(map(str, alphabet)), "sha256": digest.hexdigest()} + + +def source_inventory(): + tree = ast.parse((HERE / "sources/pr-2234/leaf.py").read_text()) + function = next(x for x in tree.body if isinstance(x, ast.FunctionDef) and x.name == "execute_leaf") + loop = next(x for x in function.body if isinstance(x, ast.For) and isinstance(x.target, ast.Name) and x.target.id == "i") + calls = [] + for statement in loop.body: + if isinstance(statement, ast.Assign) and isinstance(statement.value, ast.Call): + name = getattr(statement.value.func, "id", None) + if name in ("ordinary_swap", "shift", "sign_pass"): + calls.append(name) + a.need(calls == ["ordinary_swap", "shift", "ordinary_swap", "shift", "ordinary_swap", + "shift", "ordinary_swap", "sign_pass"], "exact source weighted-leaf schedule") + header = ast.parse((HERE / "sources/pr-2234/header_streams.py").read_text()) + add = next(x for x in header.body if isinstance(x, ast.FunctionDef) and x.name == "add") + swaps = [x for x in ast.walk(add) if isinstance(x, ast.Call) and getattr(x.func, "id", None) == "ordinary_fields"] + a.need(len(swaps) == 2, "source reversed header has two ordinary sites") + for call in swaps: + a.need(ast.dump(call.args[2]) == ast.dump(ast.parse("width-1", mode="eval").body), "high-field width is w-1") + recursion = ast.parse((HERE / "sources/pr-2234/check_recursion.py").read_text()) + moments = next(x for x in recursion.body if isinstance(x, ast.FunctionDef) and x.name == "moments") + point = next(x.value for x in moments.body if isinstance(x, ast.Assign) + and any(isinstance(t, ast.Name) and t.id == "c" for t in x.targets)) + a.need(isinstance(point, ast.Call) and isinstance(point.func, ast.Name) and point.func.id == "F", + "source coarse point constructor") + a.need([ast.literal_eval(x) for x in point.args] == [17, 10000], "actual source coarse point") + return {"leaf_schedule": calls, "header_ordinary_sites": len(swaps), "header_width": "w-1", + "source_coarse_point": "17/10000"} + + +def exponent_corollary(): + c = F(17, 10000) + first = c * (1 - c) + second = c * (1 - c) + c * first + a.need(second == c * (1 - c**2) and first < second < c, "one fixed bootstrap arithmetic") + a.need(1 - second > c and c - first > 0, "positive borrowing and atom exponent gaps") + return {"c": str(c), "old_saving": str(first), "conditional_second_saving": str(second), + "linear_coefficient": 200, "power_coefficient": 10000, + "moment_hypotheses": ["mu_1<199/200", "mu_(1-c)<9999/10000"], + "scope": "Conditional primitive-substitution corollary; moment and physical caller premises retained."} + + +def controls(): + names = [] + def rejects(name, run): + try: + run() + except (a.ContractError, ValueError): + names.append(name) + return + raise a.ContractError("control unexpectedly accepted: " + name) + def wrong_endpoint(kind): + def bad(source, bits, before, middle, suffix, meter): + result = a.binary_reference(source, bits, before, middle, suffix, meter) + if kind == "return_head": + result.stream.head = 1 + elif kind == "scratch": + result.scratch_empty = False + elif kind == "parking": + result.parking_restored = False + elif kind == "spectator": + d = result.stream.data + for j in range(0, len(d), 2): + d[j], d[j + 1] = d[j + 1], d[j] + elif kind == "dummy_leak": + # (x,gap,y,suffix)=(0,0,3,0) is outside Q=3 in the L=4 cube. + j = 3 * suffix + result.stream.data[j], result.stream.data[1] = result.stream.data[1], result.stream.data[j] + return result + raw = list(range(54)) + result = a.qadic_exchange(a.Stream(raw[:]), 3, 1, 1, 3, 2, a.Meter(), bad) + a.need(result.data == swap_oracle(raw, 3, 1, 1, 3, 2), "semantic callee mismatch") + for name in ("return_head", "scratch", "parking", "spectator", "dummy_leak"): + rejects(name, lambda name=name: wrong_endpoint(name)) + def clean_identity(): + raw = list(range(9)) + result = a.qadic_exchange(a.Stream(raw[:]), 3, 1, 1, 1, 1, a.Meter(), + lambda source, *_args: a.BinaryReturn(source)) + a.need(result.data == swap_oracle(raw, 3, 1, 1, 1, 1), "clean return is not the swap endpoint") + rejects("clean_identity_is_not_swap", clean_identity) + rejects("incomplete_genuine_rectangle", lambda: a.qadic_exchange(a.Stream([1]), 3, 1, 1, 1, 1, a.Meter())) + rejects("invalid_width", lambda: a.qadic_exchange(a.Stream([]), 3, -1, 1, 1, 1, a.Meter())) + rejects("nonunit_weight", lambda: a.weighted_leaf(list(range(81)), 3, 2, [[3]])) + raw = list(range(81)) + expected, _ = a.weighted_leaf(raw, 3, 2, [[2]]) + for flag in ("wrong_inverse", "omit_sign"): + def changed(flag=flag): + result, _ = a.weighted_leaf(raw, 3, 2, [[2]], **{flag: True}) + a.need(result == expected, "changed weighted endpoint") + rejects(flag, changed) + rejects("omit_header_return_swap", lambda: header_case(load_header(True), 3, 2, 1, 2, F(1, 2), True)) + rejects("omit_header_carry", lambda: header_case(load_header(), 3, 2, 1, 2, F(1, 2), False, True)) + rejects("duplicate_receipt_key", lambda: json.loads('{"x":1,"x":2}', object_pairs_hook=unique_object)) + rejects("boolean_integer_receipt", lambda: a.need(canonical({"n": True}) == canonical({"n": 1}), "typed receipt")) + # Padding must close before an operation in the original ring: otherwise + # the genuine pair (1,2) goes to target3 mod4, instead of target0 mod3. + a.need((2 + 1) % 4 == 3 and (2 + 1) % 3 == 0, "wrong-modulus intermediate witness") + names.append("padding_must_close_before_original_ring_add") + return names + + +def run(): + pins = authenticate() + return {"status": "PASS_BIT2234_CALLEE_SUBSTITUTION", "source_files": pins, + "source_inventory": source_inventory(), "adapter": check_adapters(), + "leaf": check_leaves(), "headers": check_headers(), + "conditional_corollary": exponent_corollary(), "controls": controls()} + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument("--emit", type=Path, help="write a new receipt; never overwrite") + args = parser.parse_args() + result = run() + if args.emit: + with args.emit.open("x") as output: + output.write(json.dumps(result, indent=2, sort_keys=True) + "\n") + else: + a.need(canonical(result) == canonical(read_json(HERE / "RESULT.json")), "exact typed receipt comparison") + print(result["status"], "adapter_cases=" + str(result["adapter"]["cases"]), + "leaf_cases=" + str(result["leaf"]["cases"]), "header_cases=" + str(result["headers"]["cases"]), + "controls=" + str(len(result["controls"]))) + + +if __name__ == "__main__": + main()