diff --git a/research/selected-header-cutoff/DEPENDENCY-METADATA.json b/research/selected-header-cutoff/DEPENDENCY-METADATA.json new file mode 100644 index 0000000000..bd6c970335 --- /dev/null +++ b/research/selected-header-cutoff/DEPENDENCY-METADATA.json @@ -0,0 +1,18 @@ +[ + { + "path": "research/selected-rank-control/controller_reference.py", + "local": "inputs/controller_reference.py", + "git_blob": "3ab6d0361f35038ffcdf0cf81a157f7a17b40e72", + "size": 5938, + "repository": "CubeJerry/integer-mult-bounds", + "commit": "9dfe6747b8553fd11b408f2b045c5954ef1e6eaa" + }, + { + "path": "research/selected-rank-control/selected_control.py", + "local": "inputs/selected_control.py", + "git_blob": "b3ffa7c4ac74715c3c9f45d21eb2bcc84e336828", + "size": 4332, + "repository": "CubeJerry/integer-mult-bounds", + "commit": "9dfe6747b8553fd11b408f2b045c5954ef1e6eaa" + } +] diff --git a/research/selected-header-cutoff/PEER-REVIEW.md b/research/selected-header-cutoff/PEER-REVIEW.md new file mode 100644 index 0000000000..36ebde3c6e --- /dev/null +++ b/research/selected-header-cutoff/PEER-REVIEW.md @@ -0,0 +1,134 @@ +# Independent proof, source, and cost review of the cutoff prefix + +**Result: PASS for the stated interface and added control costs.** This is a +proof/source review complementary to the root reviewer's separately implemented +dense CPU. I did not run the author's `verify.py` or use its machine execution as +independent evidence. No author files were changed. + +## Reviewed snapshot + +Canonical source base: `e54523517d0f03e58352e647c403a5af3e525a57`. +The input controller is the published CubeJerry fork package at +`9dfe6747b8553fd11b408f2b045c5954ef1e6eaa`. + +| File | SHA-256 | +| --- | --- | +| `cutoff_prefix.py` | `1f67f85d14f472e94e05072c4d9840ff9b79ee7d944e2fb1699c44e4b9b8687d` | +| `PROOF.md` | `5cfa6f6c0a3c3eca790c7c155dcdff3b769dc320d3a5a9a31c7356cfe2d72262` | +| `SOURCES.json` | `aa19dd4d24a2d760fbc2d5168bc44dddb221276b09fecef1278b2b5a5aa00830` | +| `inputs/controller_reference.py` | `e664a748e6b6797d4b60f60a7a7dd68b59a5608acf56b9c5d8b466f363755f73` | +| `inputs/selected_control.py` | `1c977e9f4864d338f874aa4943d9f3422d964c3ab0cc2f877d9bc4c2d9e20237` | + +## Actual source binding + +I read the pinned `FULL-RESULT.json` and `interval_gate.py`, not merely this +package's interpretation. The claim/tested fractions differ by +`7/100000000000000`; the gate divides that difference by seven and sets +`ep=1-g`, `stop=g`. Thus `Q=100000000000000`, stopping exponent `1/Q`, and +`epsilon=1-1/Q` are the actual coupled values. `be=1-3*g` is a different +parameter. The stopping formulas in `notes/batched-complex-rows.tex` identify +the exponent through both the internal and leaf costs and require the strict +leaf test `e=p+2`, and has volume `V=2*M*r*w`. I also checked the actual +Gamma convention in `02-streams.tex` and the selected application review's +reserved-axis treatment in its section 5. The supplied WIDTH is consequently +a retained premise; this prefix does not produce or validate the reserved-axis +calculation. All six mathematical source files used here match their recorded +Git blobs and SHA-256 values. The local preexisting copy of the complex note +has one extra terminal newline; removing exactly that extra byte gives the +recorded 6,085-byte blob `e13bd96eb29bdc6526f10dc32e0a146bc17848a4`. + +## Saturation and trial proof + +For positive operand lengths `a,b<=d`, write `z=min(a*b,d)`. The literal +multiply loop increments D and PRODUCT once per emitted symbol, so it emits +exactly `z` symbols. Testing D before the factor-end branch correctly stops +even at a row boundary. No input symbol is changed. Each operand head is at +an inspected prefix when its rewind starts. + +An independent instruction recount gives a sharper exact helper count: + +* If `d>a*b`, the count is `16*z+11*a+13`. +* If `d<=a*b`, put `r=floor((z-1)/b)`; the count is `16*z+11*r+14`. + +The branches include the final failed read and all four rewinds. Since +`z>=max(a,b)` and `r=1`. Saturation is compatible with successive +squares and multiplies because truncation at d commutes with multiplication +of positive integers followed by truncation. Reading the fixed binary +expansion of Q therefore produces exactly `min(t^Q,d)`. + +The Gamma decoder implements `v <- 2*v+delta`; the preceding binary prefix +values have sum less than d. Its unary work is consequently O(d), not +O(d log d). The length guide is consumed exactly, and TRACE records every +HEADER right move. Reversing TRACE restores the borrowed header head without +reading the following field or the region preceding the first Gamma code. + +The candidate test reads CUTOFF before WIDTH. Equal length is tested by the +power routine, while exhaustion of WIDTH first is exactly the `e+1` +sentinel. Failed candidates increase by one, hence the accepted value is +`C=min(ceil(d^(1/Q)),e+1)`. There are at most C power tests. Since the positive +integer d itself has `d^Q>=d`, `C<=ceil(d^(1/Q))<=d`; thus `C^2<=d*C` pays for +the growing trial scans. At every descendant `x<=e`, capping the cutoff at +`e+1` leaves `x=2*(p+2)`, which pays this as an O_Q(V) root setup charge. The +prefix runs once around the complete recursion, not once per visited node. +The inequality would not follow from an arbitrary `epsilon<1`; the exact +coupling just checked is necessary for this particular budget argument. + +This supplies a literal control prefix for the promised valid header and +already produced positive active WIDTH. It does not produce the final +astronomical native manifest, root row grants, payload/remainder consumers, +or the analytic/native services. The five foundational assumptions and the +accepted conditional kappa remain unchanged. No new complete kappa and no +unconditional multiplication theorem are claimed. + +Prepared independently by the compiler research worker for CubeJerry with +substantial OpenAI assistance. The precursor selected-controller review and +the root's independent joined-machine test are complementary evidence, +not replacements for the source and universal cost arguments above. diff --git a/research/selected-header-cutoff/PR-DESCRIPTION.md b/research/selected-header-cutoff/PR-DESCRIPTION.md new file mode 100644 index 0000000000..2dcddc4d49 --- /dev/null +++ b/research/selected-header-cutoff/PR-DESCRIPTION.md @@ -0,0 +1,108 @@ +## What changed and why + +The published selected rank controller received a supplied unary stopping +cutoff. This package implements that input edge from the actual retained +Gamma(p)Gamma(d) header, links the producer to the unchanged controller, and +retires the generated cutoff after the completed call. + +The selected gate uses stop=g=1/10^14, distinct from its outer be=1-3g. +The producer preserves this source distinction and constructs +`C=min(ceil(d^(1/Q)),e+1)`, Q=10^14. Because every descendant width is at +most root width e, the cap preserves all source stopping decisions and +remainder hooks. + +## Exact result and complete costs + +The emitted machine has eleven fixed tapes and the predecessor's finite +alphabet. It reads the header symbol by symbol, skips Gamma(p), converts +Gamma(d) to unary by paid doubling, performs saturated unary multiplications +for fixed-Q powers, and compares successive trials with the active WIDTH. +All private guard markers are physically established and retired. No runtime +host arithmetic, callback or host recursion chooses machine actions. + +With `h=|Gamma(p)Gamma(d)|` and `R_Q=bit_length(Q)+popcount(Q)`, the complete +controller and prefix satisfy + +```text +T <= 200(P+1) sum_v e_v + 1000(R_Q+1)(h+dC+1) +S <= K0+(5+N/(N-1))e+5d+4h+40. +``` + +Every copied symbol, failed trial, head return, input access and erasure is +paid. Unary d leaves O(d) historical backing after erasure; it is not hidden +in a root-width-only bound. For the actual selected epsilon=1-1/Q, +`dC=O(p^(1-1/Q^2))=O(p)`. Thus the prefix and retirement fit O_Q(V) using +the admitted nonempty record and w>=p+2. No new supplier rate is assumed. + +The selected-Q prefix has 5,649 instruction locations. The N=3,P=2 joined +demonstrator has 5,951 locations and six symbols. The general fixed-N/P +composition is proved; the enormous actual selected final template is not +materialized. + +## Sources, novelty and credit + +Scientific base: `e54523517d0f03e58352e647c403a5af3e525a57`. +The two frozen executable inputs are unchanged copies from the +[published selected-rank-control package](https://github.com/CubeJerry/integer-mult-bounds/tree/9dfe6747b8553fd11b408f2b045c5954ef1e6eaa/research/selected-rank-control), +with exact Git blob and SHA256 pins. Linking relocates fixed jump targets and +replaces only its completed halt edge. + +Retained outer setup already supplies ordinary exact rational-power +comparisons. No novelty is claimed for integer-root arithmetic. The advance +is this source-specific finite-symbol producer and exact completed-call +composition. #5158 supplies earlier fixed-bank recursion; #6719/#6739 supply +richer natural-root/grant work from supplied depth. #5515 studies the +different historical QQ16 root cutoff. #2310/#2386 retain their paid control +preparation credit. + +## Reproduction and checks + +```sh +python3 -B research/selected-header-cutoff/verify.py +python3 -O -B research/selected-header-cutoff/verify.py +``` + +Expected: `PASS_SELECTED_HEADER_CUTOFF_PREFIX`. Normal and optimized receipts +are identical. The replay covers 357 parameter cases, 27 exact-power boundary +cases, seven selected-Q cases, 204 saturated products and six separate dense +CPU runs. Main cases execute 3,573,948 transitions and 1,324 controller nodes. +Thirteen controls exercise invalid exponents, header/head restoration, cap +equality, strict power boundaries, decoder and saturation faults, retirement, +wrong exponent, false time/space bills and source corruption. Hostile ancestor +prefixes and shifted origins are preserved. + +The all-input theorem is the written loop/stack proof. Finite executions are +corroboration, not extrapolated universal correctness or formal-kernel proof. + +## Limitations and kappa status + +**No new kappa; all five selected foundational assumptions remain.** The +selected conditional kappa stays 0.00363005817. Header validity, active WIDTH +from the Q0 reservation, actual final paid/owner manifest, complete row grants +and payload/remainder consumers remain inherited. This closes the cutoff +input edge of that admitted interface, not the entire external-root dispatcher. +No complete multiplier, selected cold replay, native payload execution, +independent human review or formal-kernel acceptance is claimed. + +Prepared for @CubeJerry with substantial OpenAI assistance. Credit the +published predecessor and the retained physical/native/compiler contributors, +including JoyboyBrian, thu-nmrc, ToikY, commdata2338, Ali Romman, David Arias +and Jose Manuel. New work is Apache-2.0; frozen notices are retained. + +## Independent acceptance checks + +[REVIEW.md](REVIEW.md) records the orchestrator's universal-loop and source +review plus a fresh dense eleven-tape CPU and direct integer-root oracle. +It passes 117 cases and 1,015,704 transitions, including long p headers, tiny +d, shifted origins, hostile exterior, the actual fixed Q, completed cleanup +and three semantic mutants. [PEER-REVIEW.md](PEER-REVIEW.md) independently +checks all source pins, the symbolic control proof, exact helper instruction +counts, and the complete time and historical-space sums without executing +the author verifier. These are separate AI reviews, not human or formal-kernel +acceptance. All reviewed scientific hashes are recorded in the evidence. + +```sh +python3 -I -W error -B research/selected-header-cutoff/independent_check.py +``` + +The full Markdown PR description is committed in `PR-DESCRIPTION.md`. diff --git a/research/selected-header-cutoff/PR-TITLE.txt b/research/selected-header-cutoff/PR-TITLE.txt new file mode 100644 index 0000000000..4992db0071 --- /dev/null +++ b/research/selected-header-cutoff/PR-TITLE.txt @@ -0,0 +1 @@ +Construct the selected complex stopping cutoff from Gamma headers with paid unary arithmetic and preserved caller tapes diff --git a/research/selected-header-cutoff/PROOF.md b/research/selected-header-cutoff/PROOF.md new file mode 100644 index 0000000000..1448119bb4 --- /dev/null +++ b/research/selected-header-cutoff/PROOF.md @@ -0,0 +1,295 @@ +# A paid Gamma-header prefix for the selected complex stopping cutoff + +Prepared for @CubeJerry with substantial OpenAI assistance. Apache-2.0. +This is a written all-input machine proof with finite corroboration, not a +formal-kernel proof. No new kappa or full framework-assumption discharge. + +## 1. Actual source parameters and the remaining input edge + +Scientific base: `e54523517d0f03e58352e647c403a5af3e525a57`. +The exact selected `research/shared-wire-split-composition/FULL-RESULT.json` +records claim 363005817/100000000000, tested 363005817007/100000000000000, +and gap g=(tested-claim)/7=1/100000000000000. Its `interval_gate.py` uses + + epsilon = 1-g; stop = g; + internal = tau+(1-stop)*max(sig-tau,0); + leaf = sig+stop*(1-sig). + +These last two formulas identify the stopping exponent in +`notes/batched-complex-rows.tex`. The different variable `be=1-3g` is an +outer exponent and must not be substituted for the stopping exponent. Put + + Q=100000000000000, beta_stop=1/Q, epsilon=1-1/Q. + +The retained formal layer input in `upstream/build/sections/05-layers.tex` +has the descriptor + + E=Gamma(p)Gamma(d)Gamma(r)Gamma(D_total)Gamma(P)Gamma(S) + Gamma(K)Gamma(rho+1)Gamma(w). + +The code, from `02-streams.tex`, is + + b_v=floor(log_2 v)+1, + Gamma(v)=0^(b_v-1) bin_(b_v)(v), |Gamma(v)|=2b_v-1. + +The promises include |E|<=C_desc*p, d<=b_d*p^epsilon, 1<=D_total<=d, +w>=p+2, and a nonempty complete array of volume V=2Mrw. The selected +application review section 5 retains this root boundary. Its reserved-axis +step either processes the layer individually or leaves active width +e=D_total-Q0, with 1<=e<=d. This prefix receives that already produced +marked unary WIDTH. It does not construct Q0, row grants or the full root +payload. The header validity and WIDTH/root correspondence remain premises. + +The predecessor [published selected controller](https://github.com/CubeJerry/integer-mult-bounds/tree/9dfe6747b8553fd11b408f2b045c5954ef1e6eaa/research/selected-rank-control) +receives a supplied unary cutoff L. The present result implements its +missing cutoff-production edge from the actual header. The predecessor +sources are copied unchanged and authenticated. Neither main's selected +record nor the predecessor package is modified. + +## 2. Exact theorem and machine domain + +For every fixed N>=2, paid-site count P>=1 and root denominator Q>=2, the +literal program takes valid positive Gamma(p)Gamma(d) followed by any untouched +suffix, positive unary WIDTH e with e<=d, and the predecessor's marked +empty CHILD and suspended STACK inputs. It produces + + C=min(ceil(d^(1/Q)), e+1), + +executes the unchanged selected controller with cutoff C, then retires C. +Every initial input cell and head is restored. For actual selected source +use, Q is the fixed value above and the complete retained header obeys all +its source promises. Smaller Q and syntactically encoded headers in tests are +functional analogues, not changed selected parameters or complete source-family +admission claims. + +Tapes 0..3 are WIDTH, CHILD, STACK, CUTOFF. Tape 4 is borrowed HEADER. +Six private tapes are TRACE, LENGTH, D, ACC, FACTOR and PRODUCT. The HEADER +head initially addresses the first symbol of Gamma(p). Each new private bank +(including CUTOFF) has a blank owned guard cell one step left of its entry +head and a blank suffix. Arbitrary preserved ancestors may begin below that +guard cell. The program physically writes each guard delimiter before use, +and physically erases it before returning. These constant marker operations +are included, rather than assumed free. WIDTH/CHILD/STACK retain their +published entry markers and arbitrary permitted suspended prefixes. + +K0 includes all retained entry backing, including warm blank capacity. New +backing below is additional historical capacity; erasure never subtracts it. +The valid-input theorem need not roll back malformed input. + +Only local-symbol read, symbol write, unit head move, goto, emit and halt +instructions execute. Compile-time loops unroll fixed Q and fixed ports. +There is no runtime host integer, decoded descriptor, stack callback, dynamic +tape selection or input-dependent alphabet. Emit labels are stationary +finite-control edges; Python transcripts are verifier observations. + +Let R_Q=bit_length(Q)+popcount(Q). The prefix has exactly 273+84R_Q +instruction locations. The retirement segment has 14. The unchanged selected +controller has 30N+42+P(69+3N), giving total + + 329+84R_Q+30N+P(69+3N). + +There are eleven tapes and P+4 symbols. For selected Q, R_Q=64. The prefix +alone has 5649 locations; the N=3,P=2 joined example has 5951 locations and +six symbols. This example does not materialize the enormous actual final +selected N,P or their owner manifest. + +## 3. Header decoder and local restoration + +While skipping Gamma(p), every leading zero appends one unary LENGTH token. +The first one ends that phase. For each saved token the machine consumes +exactly one following header bit, erases the token, and moves LENGTH left. +It stops on its own marker and restores that head. Thus the next header +symbol is precisely the start of Gamma(d), without knowing p at runtime. + +The same leading-zero phase for Gamma(d) records b_d-1 remaining bits and +initializes unary D to one. For a following bit delta, the machine emits two +PRODUCT symbols per D symbol, then delta additional symbols; it clears old +D and moves PRODUCT back into D. Hence the updated unary value is 2v+delta. +Induction on the binary prefix proves D=d after all tail bits are consumed. +The LENGTH tokens control this loop symbolically; no host counter is read. + +Every right move of HEADER appends exactly one TRACE token. At the end, TRACE +has h=|Gamma(p)Gamma(d)| symbols. A backward scan erases each token and moves +HEADER left once, then returns TRACE to its start. HEADER is never written, +never moves left of its original entry, and never reads later header fields. +Its final cells and head are exact. The trace and length guide are empty. +Each unary doubling has linear cost in its old/new values. Earlier binary +prefix values sum to less than d, so their total work is O(d), not O(d log d). + +## 4. Saturated product and exact fixed power + +The primitive starts with positive unary a,b,d, a,b<=d, and empty PRODUCT. +Its outer head scans ACC, its inner head scans FACTOR. Every pair emits one +PRODUCT symbol and advances the D head once. The D head reaching its first +blank stops production immediately, including partway through an inner scan. +Otherwise an inner completion rewinds FACTOR and advances ACC. Thus exactly +z=min(ab,d) symbols are emitted. Every input and output head rewinds locally. +ACC, FACTOR and D are preserved. No prior ancestor is scanned. + +Because 1<=a,b<=d, z>=max(a,b). Consequently complete rewinds of input +streams also cost O(z). Saturation does not leave an uncharged long operand. +This is why positivity and the operand bound are part of the primitive's +contract. + +A power step copies one source into FACTOR, computes the saturated product, +clears old ACC and FACTOR, and moves PRODUCT into ACC. For squaring the source +is ACC; for multiplication by the current trial t it is CUTOFF. Distinct tapes +hold the two multiplicands, including when squaring. + +For positive integers, saturation satisfies + + min(min(a,d)*min(b,d),d)=min(ab,d). + +Start ACC at one and process the compile-time binary digits of Q: square at +each digit, and multiply by t at each one digit. After the digits representing +nu, the invariant is ACC=min(t^nu,d). After R_Q power steps it is therefore +min(t^Q,d). Exact equality of the ACC and D unary lengths is equivalent to +t^Q>=d, including perfect-power equality. All operands stay positive and at +most d. FACTOR and PRODUCT are empty at each step boundary. + +## 5. Trial cap, exact stopping law and source composition + +CUTOFF first contains t=1. Before a power test, the machine compares CUTOFF +and WIDTH in lockstep, reading CUTOFF first. Exhausting CUTOFF means t<=e, +including equality. Exhausting WIDTH first means t=e+1, the sentinel. Both +heads rewind over only the inspected prefixes. WIDTH is never written. + +At a nonsentinel trial, t<=e<=d, so the saturated-power operand contract holds. +If t^Q=d, +ACC is cleared and the cutoff is accepted. A sentinel is accepted without +performing its power. Thus the first accepted value is exactly +C=min(ceil(d^(1/Q)),e+1). D is then cleared, the six private arithmetic/guide +markers are erased, and READY is emitted. All tapes except the newly created +marked CUTOFF already have their original cells and heads. + +Put L=ceil(d^(1/Q)). Every descendant width x of the published controller +satisfies x<=e. If L<=e+1, C=L. If L>e+1, both x 2v+delta costs at most 47v+35. Summing earlier prefixes +gives at most 82d for these updates. The remaining decode, length-guide, +access-trace and header-return work fits 200(d+h+1), h=|Gamma(p)Gamma(d)|. +Each cap comparison and its two rewinds cost at most 11t+9. A failed trial's +increment costs at most 6t+10. Final power comparison, its two rewinds and ACC +clear cost O(d), with the direct loops bounded by 30d+20. + +There are at most C power trials and C cap comparisons. Since the positive +integer d itself satisfies d^Q>=d, C<=ceil(d^(1/Q))<=d and C^2<=dC. +Include all initial marker writes, retirement marker erasures, +D cleanup, both linking jumps and final halt. The resulting conservative +all-input additional bill is + + T_prefix+T_retirement <= 1000(R_Q+1)(h+dC+1). + +With e_v the selected tree widths, complete control time is therefore + + T_total <= 200(P+1) sum_v e_v + 1000(R_Q+1)(h+dC+1). + +Neither erased arithmetic nor head returns are omitted. The failed trials, +not just the successful power, are charged. No sparse table access is used. + +WIDTH and CHILD visit at most e+2 cells each. CUTOFF visits at most C+2. +The published stack occupies at most e/(1-1/N)+depth+2, with depth<=e-1. +HEADER visits h+1 cells, TRACE at most h+2, and LENGTH at most h+2. +Each of D, ACC, FACTOR and PRODUCT visits at most d+2. Adding these intervals +and the preexisting history K0 gives, in particular, + + S <= K0+(5+N/(N-1))*e+5d+4h+40. + +This deliberately loose bound counts all eleven tapes and all retired unary d +storage. It is not the predecessor's root-width-only descriptor bound: when +d is much larger than e, an O(d) history term remains and must be paid. +Repeated multiplication stages, trials and completed outer calls reuse the +same fixed origins; their erased capacity is counted by the largest visited +prefix, not reset to zero. + +## 7. Why the actual selected source pays this implementation + +The ordinary rational-root arithmetic is not a novelty claim: retained +`08-assembly.tex` already describes exact power comparisons. The explicit +prefix above instead admits a particularly simple unary lowering because +the actual selected exponents satisfy a useful full-budget inequality. + +Since C<=d^(1/Q)+1 and d<=b_d*p^epsilon, + + dC <= d^(1+1/Q)+d + = O(p^(epsilon*(1+1/Q))) + = O(p^(1-1/Q^2)) = O(p). + +Also h<=|E|=O(p), e<=d=O(p), and R_Q is fixed. Thus the prefix and complete +retirement cost O_Q(p), with additional historical backing O(d+log p)=O(p). +The actual retained array has V=2Mrw>=2(p+2). A single nonempty record already +pays this O_Q(V) root fee. No new BIT supplier, logarithmic improvement, +superpolynomial-fiber allowance or uncharged arithmetic model is needed. + +The time implication is source-specific. The functional machine works for +other fixed Q and valid integer inputs, but O(p) would not follow merely from +epsilon<1 if epsilon*(1+1/Q)>1. This proof uses the selected coupled values, +not an unstated inequality for arbitrary beta. Q's immense constant and all +existing eventual source thresholds remain finite; no practicality claim is +made. + +## 8. Novelty, predecessors and remaining obligations + +The immediate predecessor supplied the literal rank-one controller but +explicitly left its cutoff production open. This package adds the actual +Gamma-header reader, cutoff producer, retained cutoff and cleanup, and an +exact fixed-table link. Its source-specific unary budget avoids presenting +a standard integer-root algorithm as novel. + +[#5158](https://github.com/CrocSwap/integer-mult-bounds/pull/5158) already proves +dyadic fixed-bank recursion. +[#6719](https://github.com/CrocSwap/integer-mult-bounds/pull/6719) and +[#6739](https://github.com/CrocSwap/integer-mult-bounds/pull/6739) construct/review +richer delayed-cover natural-root grants from supplied binary T/R_body/w and +unary depth. Their root/payload work is not re-proved. +[#5515](https://github.com/CrocSwap/integer-mult-bounds/pull/5515) studies a +different historical QQ16 global-root cutoff and its parking/divisibility +law. [#2310](https://github.com/CrocSwap/integer-mult-bounds/pull/2310) and +[#2386](https://github.com/CrocSwap/integer-mult-bounds/pull/2386) retain credit +for earlier charged control preparation and polynomial-absorption work. + +The actual selected N,P/owner manifest, WIDTH from Q0/root reservation, header +validity, grants, full payload/remainder consumers, native semantics and +analytic/numerical endpoints remain obligations. This is a literal closure +of the cutoff input edge under that admitted root interface. All five +foundational assumptions remain retained; kappa stays 0.00363005817. +Classical unary arithmetic, binary exponentiation and depth-first techniques +retain their ordinary credit. No independent human or formal-kernel review +is claimed by the author. diff --git a/research/selected-header-cutoff/README.md b/research/selected-header-cutoff/README.md new file mode 100644 index 0000000000..49c6eadf25 --- /dev/null +++ b/research/selected-header-cutoff/README.md @@ -0,0 +1,139 @@ +# Generate the selected cutoff from its actual encoded root header + +This package closes one input edge of the published fixed-tape complex +controller: it reads **Gamma(p)Gamma(d)** from the retained layer header, +produces the exact capped cutoff, executes the unchanged controller, and +retires the generated cutoff. Every header/WIDTH input and all eleven tape +heads are restored; marker preparation, arithmetic, copies, erasures and +returns are literal counted instructions. + +The selected stopping exponent is **1/Q with Q=10^14**. It is the `stop=g` +parameter in the accepted gate, distinct from the outer exponent `be=1-3g`. +For existing unary active width e, the generated cutoff is + +\[ +C=\min\!\left(\left\lceil d^{1/Q}\right\rceil,e+1\right). +\] + +All descendants have width at most e, so this cap preserves every stopping +decision, paid-child order and remainder hook of the source controller. +**No new kappa; all five foundational assumptions remain retained.** + +## Literal implementation and complete budget + +`cutoff_prefix.py` emits only local-symbol read/write, unit head moves, goto, +stationary event labels and halt. Its execution uses no host integer or host +recursion. It skips Gamma(p), converts Gamma(d) to unary by local doubling, +then tests t=1,2,... up to the first t^Q>=d or sentinel e+1. Binary exponentiation +is unrolled for fixed Q at compile time; each multiplication is a physically +streamed unary product saturated at d. The program initializes its own private +guard markers and erases them before complete return. + +Let h=|Gamma(p)Gamma(d)| and R_Q=bit_length(Q)+popcount(Q). The [all-input +proof](PROOF.md) gives + +\[ +T_{\rm total}\le 200(P+1)\sum_v e_v ++1000(R_Q+1)(h+dC+1). +\] + +Additional historical backing is bounded by + +\[ +(5+N/(N-1))e+5d+4h+40 +\] + +beyond entry history K0. **Unary d leaves O(d) retained backing after +erasure, even when e is small.** This storage is explicitly charged. + +The actual selected gate also has epsilon=1-1/Q and d=O(p^epsilon). Hence +dC=O(p^(1-1/Q^2))=O(p). The complete prefix and retirement fit O_Q(p)=O_Q(V), +since the admitted nonempty record already has w>=p+2 and V=2Mrw. This uses +the coupled selected parameters; epsilon<1 alone would not justify this +unary implementation for every possible cutoff exponent. + +For selected Q the prefix has 5,649 instruction locations on eleven tapes. +Its composition with N=3,P=2 has 5,951 locations and six symbols. N=3,P=2 is +a bounded demonstrator; the actual final selected N/P and owner manifest are +not materialized. The theorem is uniform over fixed N,P under the published +controller contract. + +## Reproduction + +Python 3.10+ and the standard library, from the repository root: + +```sh +python3 -B research/selected-header-cutoff/verify.py +python3 -O -B research/selected-header-cutoff/verify.py +``` + +Expected status: `PASS_SELECTED_HEADER_CUTOFF_PREFIX`. Normal and optimized +receipts agree exactly. The bounded replay contains 357 parameter cases, +27 exact-power boundary cases, seven selected-Q cases, 204 direct saturated +product checks and six runs with a separately implemented dense interpreter. +The main cases execute 3,573,948 transitions and 1,324 selected-control nodes. +Thirteen controls reject wrong header return, cap equality, perfect-power +strictness, decoder arithmetic, saturation, retirement, exponent, time bill, +forgotten unary-d history and corrupted frozen source, plus invalid fixed +exponents. Translated origins carry opaque hostile ancestors. + +Finite tests corroborate written loop invariants and all-input cost bounds. +They are not a formal proof kernel or full selected-payload replay. Test +fixtures construct encoded inputs outside the executing machine; no fixture +integer is read by a machine instruction. + +## Source and dependency boundary + +The base is `e54523517d0f03e58352e647c403a5af3e525a57`. `SOURCES.json` records +canonical source blob/length/SHA256 pins and exact predecessor code pins. +The two files under `inputs/` are unchanged copies from +[CubeJerry commit 9dfe6747b8553fd11b408f2b045c5954ef1e6eaa](https://github.com/CubeJerry/integer-mult-bounds/tree/9dfe6747b8553fd11b408f2b045c5954ef1e6eaa/research/selected-rank-control). +Their hashes are checked before import. Their selected program is relocated +and linked only at its completed halt edge. + +The retained source already describes ordinary rational-power comparisons; +this is not a claim to invent integer roots. The new result is an explicit +source-bound prefix and completed-call composition with the actual encoded +header, complete costs and retained history. +[#6719](https://github.com/CrocSwap/integer-mult-bounds/pull/6719) and +[#6739](https://github.com/CrocSwap/integer-mult-bounds/pull/6739) retain credit +for richer natural-root grant/payload production from supplied depth. +[#5515](https://github.com/CrocSwap/integer-mult-bounds/pull/5515) treats a +different QQ16 root-dependent cutoff. +[#5158](https://github.com/CrocSwap/integer-mult-bounds/pull/5158), +[#2310](https://github.com/CrocSwap/integer-mult-bounds/pull/2310) and +[#2386](https://github.com/CrocSwap/integer-mult-bounds/pull/2386) retain their +fixed-bank and paid-controller credit. + +## Remaining obligations and credit + +Header validity, the already supplied active WIDTH from Q0 reservation, row +grants, the actual final paid-site/owner manifest, and payload/remainder +consumers remain inherited. The prefix does not implement the entire root +dispatcher or discharge native_all_columns, owned_erasure, compiler, +precision_tape or analytic_recovery. The selected conditional kappa remains +0.00363005817. + +Prepared for @CubeJerry with substantial OpenAI assistance. Credit the +published selected-rank-control authors and the retained physical lineage, +including JoyboyBrian, thu-nmrc, ToikY, commdata2338, Ali Romman, David Arias +and Jose Manuel. New material is Apache-2.0; frozen source headers are +preserved. Independent human or formal-kernel acceptance is not claimed. + +## Independent acceptance checks + +[REVIEW.md](REVIEW.md) records the orchestrator's universal-loop and source +review plus a fresh dense eleven-tape CPU and direct integer-root oracle. +It passes 117 cases and 1,015,704 transitions, including long p headers, tiny +d, shifted origins, hostile exterior, the actual fixed Q, completed cleanup +and three semantic mutants. [PEER-REVIEW.md](PEER-REVIEW.md) independently +checks all source pins, the symbolic control proof, exact helper instruction +counts, and the complete time and historical-space sums without executing +the author verifier. These are separate AI reviews, not human or formal-kernel +acceptance. All reviewed scientific hashes are recorded in the evidence. + +```sh +python3 -I -W error -B research/selected-header-cutoff/independent_check.py +``` + +The full Markdown PR description is committed in `PR-DESCRIPTION.md`. diff --git a/research/selected-header-cutoff/REVIEW.md b/research/selected-header-cutoff/REVIEW.md new file mode 100644 index 0000000000..83cd6cca01 --- /dev/null +++ b/research/selected-header-cutoff/REVIEW.md @@ -0,0 +1,84 @@ +# Independent root review of the header/cutoff prefix + +**PASS at the declared control-interface scope.** The root independently +read the complete source and proof, inspected the selected exponent/header +sources, derived the loop invoices and ran a separate dense CPU. Prepared +for Jerry Chen / @CubeJerry with substantial OpenAI assistance; independent +AI review does not establish human or formal-kernel acceptance. Apache-2.0. + +## Frozen snapshot + +Scientific base: `e54523517d0f03e58352e647c403a5af3e525a57`. + +- `cutoff_prefix.py` SHA256: + `1f67f85d14f472e94e05072c4d9840ff9b79ee7d944e2fb1699c44e4b9b8687d`. +- `PROOF.md` SHA256: + `5cfa6f6c0a3c3eca790c7c155dcdff3b769dc320d3a5a9a31c7356cfe2d72262`. +- Unchanged controller dependency: + `9dfe6747b8553fd11b408f2b045c5954ef1e6eaa`, with exact file pins retained. + +## Source, loop and cost review + +The selected gate assigns stop=g and epsilon=1-g, g=1/10^14. Its different +outer variable be is not the stopping exponent. The retained layer provides +Gamma(p)Gamma(d), d<=b_d*p^epsilon and V=2Mrw>=2(p+2). The claimed budget +therefore uses actual source parameters rather than a generic epsilon<1. + +The Gamma decoder consumes exactly the tail length recorded by its leading +zeros. Unary updates v -> 2v+delta decode d; earlier prefix values have total +below d. TRACE logs every header move and reverses exactly that distance. +Private guard cells begin owned and blank, and their establishment and +retirement are literal instructions. HEADER is never written. + +For the saturated product z=min(ab,d), positivity and a,b<=d imply +z>=max(a,b). Thus even terminal rewinds of operands are O(z). Direct loop +counting supports 40z+40; copying, product, two erasures and transfer give +77z+62<=160d per power step. The saturation identity proves the fixed binary +power chain for all inputs, including equality. The sentinel e+1 is accepted +without a power; all actual power operands satisfy t<=e<=d. C<=d then gives +C^2<=dC, paying all failed-trial scans and increments. Marker work, all head +returns, arithmetic retirement and cutoff cleanup fit the stated complete +1000(R_Q+1)(h+dC+1) envelope. Historical backing includes the unary d banks +after erasure, as well as the trace, guides, cutoff and suspended stack. + +Fixed jump relocation preserves every selected instruction except replacing +its completed HALT by one cleanup jump. That program accesses only tapes +0..3; HEADER and restored private banks remain stationary. Its completed-call +restoration supplies exactly the cleanup entry. READY/RETIRED are finite +control edges, not runtime callbacks or a stored transcript. + +Finally epsilon*(1+1/Q)=1-1/Q^2. Hence dC=O(p), with b_d incorporated into +the fixed constant, and h<=|E|=O(p). The nonempty retained array pays O_Q(V) +for the complete root prefix and retirement. Additional O(d+log p) history +also fits O(p). This uses the selected coupled exponents; it is not a claim +for arbitrary epsilon and stopping beta. No new supplier rate is introduced. + +## Independent executable evidence + +From this directory: + +```sh +python3 -I -W error -B independent_check.py . +``` + +The JSON report records **117 cases and 1,015,704 transitions, PASS**. This +checker imports the compile-time builder and uses its own dense eleven-tape +CPU, input encoder and exact integer-root oracle. It never calls the author's +Machine, input constructor, verifier or expected-event function. Selected-Q +fixtures explicitly have d<2^Q, so their exact ceiling root is one or two; +the universal written invariant, not those tests, covers larger d. + +Coverage includes Q=2,3,5 and the selected Q, perfect-power neighborhoods, +caps, long Gamma(p) with tiny d, shifted origins, hostile inaccessible +exterior cells and joined cleanup. Wrong header return, skipped retirement +and a substituted exponent each fail at the expected semantic boundary. +The frozen receipt is `evidence/independent.json`. Tests corroborate the +written theorem; they do not establish it by extrapolation. + +## Residual obligations + +Header validity and active WIDTH after Q0 reservation remain premises. The +actual final N/P/owner manifest, row grants, chronological scalar/frame and +payload/remainder consumers, native contracts and analytic endpoints remain. +The result closes this cutoff input edge; all five selected assumptions and +kappa are unchanged. No complete multiplier or native payload run is claimed. diff --git a/research/selected-header-cutoff/SOURCES.json b/research/selected-header-cutoff/SOURCES.json new file mode 100644 index 0000000000..5845296cf5 --- /dev/null +++ b/research/selected-header-cutoff/SOURCES.json @@ -0,0 +1,125 @@ +{ + "base": "e54523517d0f03e58352e647c403a5af3e525a57", + "selected_kappa": "0.00363005817", + "references": [ + { + "path": "upstream/build/sections/02-streams.tex", + "size": 11311, + "git_blob": "088fceea1867abc76271d7efe7532b779fee9039", + "sha256": "606c80db61cad13aa0c3b6060dc4b88dbbe7ac60cdd831aa93f28d908fd09dab", + "repository": "CrocSwap/integer-mult-bounds", + "commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "role": "source statement and exact parameter/interface pin; not imported executable" + }, + { + "path": "upstream/build/sections/05-layers.tex", + "size": 46811, + "git_blob": "5ce8b3c83c455f221bb84858a97230b0285644aa", + "sha256": "20cfc8d12099d4e4ed9e3e7eeb6162edd9b6e0e076f24693364cd24377252594", + "repository": "CrocSwap/integer-mult-bounds", + "commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "role": "source statement and exact parameter/interface pin; not imported executable" + }, + { + "path": "upstream/build/sections/08-assembly.tex", + "size": 46444, + "git_blob": "337810a1d9a58a2ecf14123420923c039ba322a6", + "sha256": "763d7945b1e1ec4ebae9b799bcefcc45fa9bae6e2ffad799868a9c3d513dbd4a", + "repository": "CrocSwap/integer-mult-bounds", + "commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "role": "source statement and exact parameter/interface pin; not imported executable" + }, + { + "path": "research/shared-wire-split-composition/interval_gate.py", + "size": 6886, + "git_blob": "e24dc46079b4c25152f5afc096dda2ce8ee58ff5", + "sha256": "60a743d13f668ef86db4b8215b4d5d04430a671ba6f1fe06d9c1c4c3dfe86da5", + "repository": "CrocSwap/integer-mult-bounds", + "commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "role": "source statement and exact parameter/interface pin; not imported executable" + }, + { + "path": "research/shared-wire-split-composition/FULL-RESULT.json", + "size": 25225, + "git_blob": "ff3256f0d3ffbfc56b062f9ec0fdbbc7b30e76d5", + "sha256": "d9ba709fa5dcefffe3f3abdcf34600ce188224703cfd743e6db8b58ba4816cb7", + "repository": "CrocSwap/integer-mult-bounds", + "commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "role": "source statement and exact parameter/interface pin; not imported executable" + }, + { + "path": "research/delayed-cover-physical-batch-routing/README.md", + "size": 5233, + "git_blob": "b305a4f70a38a2ee6838c2331ca597b378d37d07", + "sha256": "1e437dcaa0db134e3c4ac6957e61237f144784e3e576e19a28eda48ad4493065", + "repository": "CrocSwap/integer-mult-bounds", + "commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "role": "source statement and exact parameter/interface pin; not imported executable" + }, + { + "path": "docs/research/pr-intake-evidence/pr7000-application/PROOF-REVIEW.md", + "size": 25533, + "git_blob": "3dd1af2285e597676725e85ad4f65e7ad326d695", + "sha256": "4501502c2ceb9759b20372435fe4beb51082c5a5e2910c1fd5dbe6edca415055", + "repository": "CrocSwap/integer-mult-bounds", + "commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "role": "credited reference text, not imported executable" + }, + { + "path": "notes/batched-complex-rows.tex", + "size": 6085, + "git_blob": "e13bd96eb29bdc6526f10dc32e0a146bc17848a4", + "sha256": "64c70926a8705874f1c9b42a2f703e42cad4e90f927f544458cfdf729540236c", + "repository": "CrocSwap/integer-mult-bounds", + "commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "role": "source law and cutoff/remainder specification; no imported executable" + } + ], + "executable_inputs": [ + { + "path": "research/selected-rank-control/controller_reference.py", + "local": "inputs/controller_reference.py", + "git_blob": "3ab6d0361f35038ffcdf0cf81a157f7a17b40e72", + "size": 5938, + "repository": "CubeJerry/integer-mult-bounds", + "commit": "9dfe6747b8553fd11b408f2b045c5954ef1e6eaa", + "sha256": "e664a748e6b6797d4b60f60a7a7dd68b59a5608acf56b9c5d8b466f363755f73", + "role": "unchanged executable input, authenticated before import" + }, + { + "path": "research/selected-rank-control/selected_control.py", + "local": "inputs/selected_control.py", + "git_blob": "b3ffa7c4ac74715c3c9f45d21eb2bcc84e336828", + "size": 4332, + "repository": "CubeJerry/integer-mult-bounds", + "commit": "9dfe6747b8553fd11b408f2b045c5954ef1e6eaa", + "sha256": "1c977e9f4864d338f874aa4943d9f3422d964c3ab0cc2f877d9bc4c2d9e20237", + "role": "unchanged executable input, authenticated before import" + } + ], + "selected_parameters": { + "Q": "100000000000000", + "stop": "1/100000000000000", + "epsilon": "99999999999999/100000000000000", + "outer_be_is_different": "99999999999997/100000000000000", + "gap_source": "FULL-RESULT.json/gate/compiler_gap and interval_gate.py/gate" + }, + "inherited_scope": "valid retained header, already supplied post-Q0 WIDTH, row grants, final N/P/owner manifest and payload consumers; all five assumptions retained", + "overlap": [ + { + "pr": 5515, + "head": "a3be1f66a44e1e6d7fc798b238fea8470edd0a63", + "scope": "historical QQ16 root cutoff and parking/divisibility law" + }, + { + "pr": 6719, + "head": "e4e52d6ba2c805fa78bb57778c3b7bbc064edba5", + "scope": "delayed-cover natural-root grants from supplied depth" + }, + { + "pr": 6739, + "head": "d4f7d625b2a5fa71f2c9c276b9ea503c28dcee4b", + "scope": "independent natural-root descriptor production review" + } + ] +} diff --git a/research/selected-header-cutoff/VALIDATION.json b/research/selected-header-cutoff/VALIDATION.json new file mode 100644 index 0000000000..6dc42b3c49 --- /dev/null +++ b/research/selected-header-cutoff/VALIDATION.json @@ -0,0 +1,92 @@ +{ + "status": "Author normal/optimized replay and independent dense CPU passed; root and separate proof/source/cost reviews accepted at frozen scientific hashes", + "base": "e54523517d0f03e58352e647c403a5af3e525a57", + "python": "3.12.14", + "commands": [ + "python3 -B research/selected-header-cutoff/verify.py", + "python3 -O -B research/selected-header-cutoff/verify.py", + "python3 -I -W error -B research/selected-header-cutoff/independent_check.py" + ], + "normal_optimized_byte_equal": true, + "receipt": "evidence/normal.json", + "receipt_scope": "357 parameter cases + 27 exact-power boundary cases + 7 selected-Q cases; counted transitions only for these main cases; 204 product checks and six dense CPU cases separately", + "finite_coverage": { + "alphabet_size_n3_sites2": 6, + "control_names": [ + "invalid-fixed-exponent", + "invalid-fixed-exponent", + "invalid-fixed-exponent", + "borrowed-header-return", + "sentinel-equality", + "perfect-power-strictness", + "Gamma-d-doubling", + "cutoff-retirement", + "product-saturation", + "wrong-cutoff-exponent", + "undercharged-total-time", + "false-root-width-only-space", + "frozen-source-corruption" + ], + "counted_selected_nodes": 1324, + "counted_transitions": 3573948, + "direct_saturated_products": 204, + "exact_power_boundary_cases": 27, + "finite_cases": 357, + "formal_kernel": "not_run", + "independent_dense_cases": 6, + "kappa": "unchanged", + "n3_sites2_instruction_count": 5951, + "negative_controls": 13, + "scope": "literal header/cutoff/control composition; payload and Q0 producer retained", + "selected_Q": 100000000000000, + "selected_Q_cases": 7, + "selected_Q_power_stages": 64, + "source_sha256": "1f67f85d14f472e94e05072c4d9840ff9b79ee7d944e2fb1699c44e4b9b8687d", + "status": "PASS_SELECTED_HEADER_CUTOFF_PREFIX", + "tapes": 11 + }, + "root_independent_execution": { + "source_sha256": "1f67f85d14f472e94e05072c4d9840ff9b79ee7d944e2fb1699c44e4b9b8687d", + "cases": 117, + "transitions": 1015704, + "scope": "separate dense CPU/direct integer-root oracle, long Gamma(p), tiny d, hostile exterior, selected Q, cleanup and three semantic mutants", + "external_receipts": [ + "independent_check.py", + "evidence/independent.json" + ], + "status": "PASS; portable checker and receipt included" + }, + "scientific_limitations": [ + "written universal proof, no formal kernel", + "unchanged published control dependency; final selected N/P not materialized", + "header validity, post-Q0 WIDTH, root/row grants and payload consumers retained", + "unary d requires O(d+log p) additional historical backing; erased regions stay charged", + "selected source time absorption uses epsilon=(Q-1)/Q and stop=1/Q" + ], + "kappa": "No new kappa; 0.00363005817 remains conditional", + "sha256": { + "DEPENDENCY-METADATA.json": "056e02f3d2b60e02c6de39fa6f46fca92f27e8ab2343cb39611f269836d59597", + "PEER-REVIEW.md": "82c87434df5569c940124fba4b56d19dfc1002627946478aac0c0ed05eb30682", + "PR-DESCRIPTION.md": "812366b955621e58d0670f767cf1a5abeb678197d9de66f1cf11802d209cc74d", + "PR-TITLE.txt": "1978bc8193f8aec16d4362f8b473055270fb22b06342e1e8a9ce5520e5c73069", + "PROOF.md": "5cfa6f6c0a3c3eca790c7c155dcdff3b769dc320d3a5a9a31c7356cfe2d72262", + "README.md": "ebd8c4eaa4f1bd426529d172e50de97595c3e669777134ee19be5621880c3785", + "REVIEW.md": "726b6b16e55a6ce0df557c77a5648789af367c65eaec18bf750377f5b6be9e51", + "SOURCES.json": "aa19dd4d24a2d760fbc2d5168bc44dddb221276b09fecef1278b2b5a5aa00830", + "cutoff_prefix.py": "1f67f85d14f472e94e05072c4d9840ff9b79ee7d944e2fb1699c44e4b9b8687d", + "evidence/independent.json": "890f3a0b8b5663ea1bab28461d847c20919f0fb68eab541e6dd3ea941534564c", + "evidence/normal.json": "83fa8943a91584158aecc2507dddd4c49e23e3f140f0bfd0cd5394068d02b5e9", + "evidence/optimized.json": "83fa8943a91584158aecc2507dddd4c49e23e3f140f0bfd0cd5394068d02b5e9", + "evidence/peer-proof.json": "8a6f43c936c49c2ba1954c9deb2f8d23846487953770b2bb99ba3865ae360d24", + "independent_check.py": "aea68f9ffba55df568240620da606321d17bbda0f2f61af88722230c43f78604", + "inputs/controller_reference.py": "e664a748e6b6797d4b60f60a7a7dd68b59a5608acf56b9c5d8b466f363755f73", + "inputs/selected_control.py": "1c977e9f4864d338f874aa4943d9f3422d964c3ab0cc2f877d9bc4c2d9e20237", + "verify.py": "f41b960becf637af4bcc4d92b33f0cffcc063991224370e8dfb6e8950fb905a2" + }, + "separate_proof_review": { + "status": "PASS", + "review": "PEER-REVIEW.md", + "receipt": "evidence/peer-proof.json", + "method": "Separate source/universal proof and cost review; no author verifier replay" + } +} diff --git a/research/selected-header-cutoff/cutoff_prefix.py b/research/selected-header-cutoff/cutoff_prefix.py new file mode 100644 index 0000000000..250229c45f --- /dev/null +++ b/research/selected-header-cutoff/cutoff_prefix.py @@ -0,0 +1,307 @@ +"""Literal Gamma-header cutoff prefix joined to the published controller. + +Apache-2.0. Prepared for CubeJerry with substantial OpenAI assistance. +All arithmetic below that chooses program edges is compile-time arithmetic. +The executing machine has only its program counter and scanned tape symbols. +""" +import hashlib +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent +INPUTS = HERE / "inputs" +PINS = { + "controller_reference.py": "e664a748e6b6797d4b60f60a7a7dd68b59a5608acf56b9c5d8b466f363755f73", + "selected_control.py": "1c977e9f4864d338f874aa4943d9f3422d964c3ab0cc2f877d9bc4c2d9e20237", +} +for name, expected in PINS.items(): + if hashlib.sha256((INPUTS / name).read_bytes()).hexdigest() != expected: + raise ValueError("frozen controller dependency hash: " + name) +sys.path.insert(0, str(INPUTS)) +from controller_reference import Builder, Machine, Tape, BLANK, ONE, MARK +from selected_control import compile_selected + +WIDTH, CHILD, STACK, CUTOFF, HEADER, TRACE, LENGTH, D, ACC, FACTOR, PRODUCT = range(11) +SELECTED_Q = 100000000000000 +NEW_BANKS = (CUTOFF, TRACE, LENGTH, D, ACC, FACTOR, PRODUCT) + + +def fresh(a, stem): + a.serial += 1 + return stem + str(a.serial) + + +def clear(a, tape): + """Erase one marked unary stream and return its head; initial head at start.""" + k = fresh(a, "clear") + a.mark(k) + a.op("read", tape, {ONE: k + "bit", BLANK: k + "done"}) + a.mark(k + "bit") + a.op("write", tape, BLANK) + a.op("move", tape, 1) + a.op("goto", k) + a.mark(k + "done") + a.rewind(tape, (BLANK,)) + + +def copy_unary(a, source, target, *, erase=False, repeat=1, extra=0): + """Emit repeat copies per input symbol and extra ones, all fixed constants.""" + k = fresh(a, "copy") + a.mark(k) + a.op("read", source, {ONE: k + "bit", BLANK: k + "done"}) + a.mark(k + "bit") + for _ in range(repeat): + a.op("write", target, ONE) + a.op("move", target, 1) + if erase: + a.op("write", source, BLANK) + a.op("move", source, 1) + a.op("goto", k) + a.mark(k + "done") + for _ in range(extra): + a.op("write", target, ONE) + a.op("move", target, 1) + a.rewind(source, (BLANK,) if erase else (ONE,)) + a.rewind(target, (ONE,)) + + +def header_step(a): + """One borrowed-header right move, logged locally for exact restoration.""" + a.op("write", TRACE, ONE) + a.op("move", TRACE, 1) + a.op("move", HEADER, 1) + + +def decode_header(a): + """Skip Gamma(p), decode Gamma(d) to unary D, then restore HEADER.""" + a.mark("p_scan") + a.op("read", HEADER, {"0": "p_zero", ONE: "p_one"}) + a.mark("p_zero") + a.op("write", LENGTH, ONE) + a.op("move", LENGTH, 1) + header_step(a) + a.op("goto", "p_scan") + a.mark("p_one") + header_step(a) + a.op("move", LENGTH, -1) + a.mark("p_tail") + a.op("read", LENGTH, {ONE: "p_tail_bit", MARK: "p_done"}) + a.mark("p_tail_bit") + a.op("write", LENGTH, BLANK) + a.op("read", HEADER, {"0": "p_tail_valid", ONE: "p_tail_valid"}) + a.mark("p_tail_valid") + header_step(a) + a.op("move", LENGTH, -1) + a.op("goto", "p_tail") + a.mark("p_done") + a.op("move", LENGTH, 1) + a.mark("d_scan") + a.op("read", HEADER, {"0": "d_zero", ONE: "d_one"}) + a.mark("d_zero") + a.op("write", LENGTH, ONE) + a.op("move", LENGTH, 1) + header_step(a) + a.op("goto", "d_scan") + a.mark("d_one") + header_step(a) + a.op("write", D, ONE) + a.op("move", LENGTH, -1) + a.mark("d_tail") + a.op("read", LENGTH, {ONE: "d_tail_bit", MARK: "header_rewind"}) + a.mark("d_tail_bit") + a.op("write", LENGTH, BLANK) + a.op("read", HEADER, {"0": "double_zero", ONE: "double_one"}) + for bit in (0, 1): + a.mark("double_one" if bit else "double_zero") + copy_unary(a, D, PRODUCT, repeat=2, extra=bit) + clear(a, D) + copy_unary(a, PRODUCT, D, erase=True) + header_step(a) + a.op("move", LENGTH, -1) + a.op("goto", "d_tail") + a.mark("header_rewind") + a.op("move", LENGTH, 1) + a.op("move", TRACE, -1) + a.mark("header_back") + a.op("read", TRACE, {ONE: "header_back_bit", MARK: "header_back_done"}) + a.mark("header_back_bit") + a.op("write", TRACE, BLANK) + a.op("move", HEADER, -1) + a.op("move", TRACE, -1) + a.op("goto", "header_back") + a.mark("header_back_done") + a.op("move", TRACE, 1) + + +def saturated_multiply(a): + """PRODUCT=min(ACC*FACTOR,D); positive inputs <=D; preserve all inputs.""" + k = fresh(a, "mul") + a.mark(k) + a.op("read", ACC, {ONE: k + "inner", BLANK: k + "done"}) + a.mark(k + "inner") + a.op("read", D, {ONE: k + "factor", BLANK: k + "done"}) + a.mark(k + "factor") + a.op("read", FACTOR, {ONE: k + "emit", BLANK: k + "next"}) + a.mark(k + "emit") + a.op("write", PRODUCT, ONE) + a.op("move", PRODUCT, 1) + a.op("move", D, 1) + a.op("move", FACTOR, 1) + a.op("goto", k + "inner") + a.mark(k + "next") + a.rewind(FACTOR, (ONE,)) + a.op("move", ACC, 1) + a.op("goto", k) + a.mark(k + "done") + for tape in (ACC, FACTOR, D, PRODUCT): + a.rewind(tape, (ONE,)) + + +def power_step(a, source): + """Replace ACC by its saturated product with source (ACC or CUTOFF).""" + copy_unary(a, source, FACTOR) + saturated_multiply(a) + clear(a, ACC) + clear(a, FACTOR) + copy_unary(a, PRODUCT, ACC, erase=True) + + +def compile_prefix(q=SELECTED_Q): + if type(q) is not int or q < 2: + raise ValueError("fixed root denominator must be an integer at least two") + a = Builder() + # Each private bank's guard cell is initially owned and blank. + # Establish its delimiter physically; no supplied marker oracle is used. + for tape in NEW_BANKS: + a.op("move", tape, -1) + a.op("write", tape, MARK) + a.op("move", tape, 1) + decode_header(a) + a.op("write", CUTOFF, ONE) + a.mark("cap_compare") + a.op("read", CUTOFF, {BLANK: "within_cap", ONE: "cap_width"}) + a.mark("cap_width") + a.op("read", WIDTH, {BLANK: "at_sentinel", ONE: "cap_step"}) + a.mark("cap_step") + a.op("move", CUTOFF, 1) + a.op("move", WIDTH, 1) + a.op("goto", "cap_compare") + a.mark("at_sentinel") + a.rewind(CUTOFF, (ONE,)) + a.rewind(WIDTH, (ONE,)) + a.op("goto", "cutoff_ready") + a.mark("within_cap") + a.rewind(CUTOFF, (ONE,)) + a.rewind(WIDTH, (ONE,)) + a.op("write", ACC, ONE) + for bit in bin(q)[2:]: + power_step(a, ACC) + if bit == "1": + power_step(a, CUTOFF) + a.mark("power_compare") + a.op("read", D, {BLANK: "power_equal", ONE: "power_acc"}) + a.mark("power_acc") + a.op("read", ACC, {BLANK: "power_short", ONE: "power_compare_step"}) + a.mark("power_compare_step") + a.op("move", D, 1) + a.op("move", ACC, 1) + a.op("goto", "power_compare") + a.mark("power_equal") + a.op("read", ACC, {BLANK: "power_equal_valid"}) + a.mark("power_equal_valid") + a.rewind(D, (ONE,)) + a.rewind(ACC, (ONE,)) + clear(a, ACC) + a.op("goto", "cutoff_ready") + a.mark("power_short") + a.rewind(D, (ONE,)) + a.rewind(ACC, (ONE,)) + clear(a, ACC) + a.mark("increment_trial") + a.op("read", CUTOFF, {ONE: "increment_scan", BLANK: "increment_end"}) + a.mark("increment_scan") + a.op("move", CUTOFF, 1) + a.op("goto", "increment_trial") + a.mark("increment_end") + a.op("write", CUTOFF, ONE) + a.op("move", CUTOFF, 1) + a.rewind(CUTOFF, (ONE,)) + a.op("goto", "cap_compare") + a.mark("cutoff_ready") + clear(a, D) + for tape in NEW_BANKS[1:]: + a.op("move", tape, -1) + a.op("write", tape, BLANK) + a.op("move", tape, 1) + a.op("emit", "READY") + a.op("halt") + return a.finish((BLANK, "0", ONE, MARK)) + + +def relocate(code, offset, halt_target=None): + result = [] + for ins in code: + if ins[0] == "goto": + result.append(("goto", offset + ins[1])) + elif ins[0] == "read": + result.append(("read", ins[1], {s: offset + pc for s, pc in ins[2].items()})) + elif ins[0] == "halt" and halt_target is not None: + result.append(("goto", halt_target)) + else: + result.append(ins) + return tuple(result) + + +def compile_joined(n, sites, q=SELECTED_Q): + prefix, _ = compile_prefix(q) + selected, alphabet = compile_selected(n, sites) + a = Builder() + clear(a, CUTOFF) + a.op("move", CUTOFF, -1) + a.op("write", CUTOFF, BLANK) + a.op("move", CUTOFF, 1) + a.op("emit", "RETIRED") + a.op("halt") + cleanup, _ = a.finish(alphabet) + core_at = len(prefix) + cleanup_at = core_at + len(selected) + if sum(ins[0] == "halt" for ins in prefix) != 1 or sum(ins[0] == "halt" for ins in selected) != 1: + raise ValueError("single completed-call link required") + code = (relocate(prefix, 0, core_at) + + relocate(selected, core_at, cleanup_at) + + relocate(cleanup, cleanup_at)) + return code, alphabet, {"prefix": core_at, "selected": len(selected), + "cleanup": len(cleanup), "cleanup_at": cleanup_at, + "power_stages": q.bit_length() + q.bit_count()} + + +def gamma(value): + """Verifier input encoding; never called by Machine.step.""" + if type(value) is not int or value < 1: + raise ValueError("positive Gamma input") + bits = bin(value)[2:] + return "0" * (len(bits) - 1) + bits + + +def initial(p, d, e, origins=None, ancestors=None, tail=None): + """Build a finite input fixture, outside the literal machine execution.""" + if type(e) is not int or not 1 <= e <= d: + raise ValueError("positive active width at most global d") + origins = (0,) * 11 if origins is None else tuple(origins) + if len(origins) != 11: + raise ValueError("eleven tape origins") + if ancestors is None: + ancestors = ("1", "0", "t0", MARK, BLANK, "1") + if tail is None: + tail = "".join(gamma(v) for v in (1, e, 1, 1, 1, 1, max(p + 2, 3))) + text = gamma(p) + gamma(d) + tail + tapes = [] + for j, origin in enumerate(origins): + cells = {} if j in NEW_BANKS else {origin - 1: MARK} + cells.update({origin - 2 - k: s for k, s in enumerate(ancestors) if s != BLANK}) + if j == WIDTH: + cells.update({origin + k: ONE for k in range(e)}) + elif j == HEADER: + cells.update({origin + k: s for k, s in enumerate(text)}) + tapes.append(Tape(cells, origin)) + return tapes diff --git a/research/selected-header-cutoff/evidence/independent.json b/research/selected-header-cutoff/evidence/independent.json new file mode 100644 index 0000000000..3c653ec8f5 --- /dev/null +++ b/research/selected-header-cutoff/evidence/independent.json @@ -0,0 +1,1184 @@ +{ + "status": "PASS", + "method": "independent dense CPU and exact integer-root oracle", + "cases": 117, + "transitions": 1015704, + "negative_controls": [ + "header return", + "cutoff retirement", + "wrong exponent" + ], + "source_sha256": "1f67f85d14f472e94e05072c4d9840ff9b79ee7d944e2fb1699c44e4b9b8687d", + "rows": [ + { + "p_bits": 74, + "d": 1, + "e": 1, + "q": 2, + "joined": false, + "cutoff": 1, + "steps": 2223, + "visited": 394 + }, + { + "p_bits": 2, + "d": 2, + "e": 1, + "q": 2, + "joined": false, + "cutoff": 2, + "steps": 585, + "visited": 41 + }, + { + "p_bits": 2, + "d": 2, + "e": 2, + "q": 2, + "joined": false, + "cutoff": 2, + "steps": 1020, + "visited": 44 + }, + { + "p_bits": 74, + "d": 3, + "e": 1, + "q": 2, + "joined": false, + "cutoff": 2, + "steps": 2409, + "visited": 403 + }, + { + "p_bits": 74, + "d": 3, + "e": 3, + "q": 2, + "joined": false, + "cutoff": 2, + "steps": 2911, + "visited": 407 + }, + { + "p_bits": 2, + "d": 4, + "e": 1, + "q": 2, + "joined": false, + "cutoff": 2, + "steps": 736, + "visited": 50 + }, + { + "p_bits": 2, + "d": 4, + "e": 4, + "q": 2, + "joined": false, + "cutoff": 2, + "steps": 1284, + "visited": 55 + }, + { + "p_bits": 2, + "d": 8, + "e": 1, + "q": 2, + "joined": false, + "cutoff": 2, + "steps": 995, + "visited": 63 + }, + { + "p_bits": 2, + "d": 8, + "e": 8, + "q": 2, + "joined": false, + "cutoff": 3, + "steps": 2419, + "visited": 75 + }, + { + "p_bits": 74, + "d": 9, + "e": 1, + "q": 2, + "joined": false, + "cutoff": 2, + "steps": 2819, + "visited": 423 + }, + { + "p_bits": 74, + "d": 9, + "e": 9, + "q": 2, + "joined": false, + "cutoff": 3, + "steps": 4289, + "visited": 436 + }, + { + "p_bits": 74, + "d": 15, + "e": 1, + "q": 2, + "joined": false, + "cutoff": 2, + "steps": 3083, + "visited": 435 + }, + { + "p_bits": 74, + "d": 15, + "e": 15, + "q": 2, + "joined": false, + "cutoff": 4, + "steps": 5850, + "visited": 457 + }, + { + "p_bits": 2, + "d": 16, + "e": 1, + "q": 2, + "joined": false, + "cutoff": 2, + "steps": 1470, + "visited": 84 + }, + { + "p_bits": 2, + "d": 16, + "e": 16, + "q": 2, + "joined": false, + "cutoff": 4, + "steps": 4283, + "visited": 107 + }, + { + "p_bits": 74, + "d": 17, + "e": 1, + "q": 2, + "joined": false, + "cutoff": 2, + "steps": 3294, + "visited": 443 + }, + { + "p_bits": 74, + "d": 17, + "e": 17, + "q": 2, + "joined": false, + "cutoff": 5, + "steps": 7584, + "visited": 470 + }, + { + "p_bits": 2, + "d": 24, + "e": 1, + "q": 2, + "joined": false, + "cutoff": 2, + "steps": 1872, + "visited": 100 + }, + { + "p_bits": 2, + "d": 24, + "e": 24, + "q": 2, + "joined": false, + "cutoff": 5, + "steps": 6495, + "visited": 134 + }, + { + "p_bits": 74, + "d": 25, + "e": 1, + "q": 2, + "joined": false, + "cutoff": 2, + "steps": 3696, + "visited": 459 + }, + { + "p_bits": 74, + "d": 25, + "e": 25, + "q": 2, + "joined": false, + "cutoff": 5, + "steps": 8365, + "visited": 494 + }, + { + "p_bits": 2, + "d": 26, + "e": 1, + "q": 2, + "joined": false, + "cutoff": 2, + "steps": 1950, + "visited": 104 + }, + { + "p_bits": 2, + "d": 26, + "e": 26, + "q": 2, + "joined": false, + "cutoff": 6, + "steps": 8609, + "visited": 143 + }, + { + "p_bits": 74, + "d": 31, + "e": 1, + "q": 2, + "joined": false, + "cutoff": 2, + "steps": 3960, + "visited": 471 + }, + { + "p_bits": 74, + "d": 31, + "e": 31, + "q": 2, + "joined": false, + "cutoff": 6, + "steps": 10860, + "visited": 515 + }, + { + "p_bits": 2, + "d": 32, + "e": 1, + "q": 2, + "joined": false, + "cutoff": 2, + "steps": 2377, + "visited": 121 + }, + { + "p_bits": 2, + "d": 32, + "e": 32, + "q": 2, + "joined": false, + "cutoff": 6, + "steps": 9323, + "visited": 166 + }, + { + "p_bits": 74, + "d": 33, + "e": 1, + "q": 2, + "joined": false, + "cutoff": 2, + "steps": 4201, + "visited": 479 + }, + { + "p_bits": 74, + "d": 33, + "e": 33, + "q": 2, + "joined": false, + "cutoff": 6, + "steps": 11193, + "visited": 525 + }, + { + "p_bits": 74, + "d": 63, + "e": 1, + "q": 2, + "joined": false, + "cutoff": 2, + "steps": 5701, + "visited": 539 + }, + { + "p_bits": 74, + "d": 63, + "e": 63, + "q": 2, + "joined": false, + "cutoff": 8, + "steps": 19890, + "visited": 621 + }, + { + "p_bits": 2, + "d": 64, + "e": 1, + "q": 2, + "joined": false, + "cutoff": 2, + "steps": 4148, + "visited": 190 + }, + { + "p_bits": 2, + "d": 64, + "e": 64, + "q": 2, + "joined": false, + "cutoff": 8, + "steps": 18383, + "visited": 273 + }, + { + "p_bits": 74, + "d": 65, + "e": 1, + "q": 2, + "joined": false, + "cutoff": 2, + "steps": 5972, + "visited": 547 + }, + { + "p_bits": 74, + "d": 65, + "e": 65, + "q": 2, + "joined": false, + "cutoff": 9, + "steps": 24288, + "visited": 634 + }, + { + "p_bits": 74, + "d": 1, + "e": 1, + "q": 3, + "joined": false, + "cutoff": 1, + "steps": 2312, + "visited": 394 + }, + { + "p_bits": 2, + "d": 2, + "e": 1, + "q": 3, + "joined": false, + "cutoff": 2, + "steps": 684, + "visited": 41 + }, + { + "p_bits": 2, + "d": 2, + "e": 2, + "q": 3, + "joined": false, + "cutoff": 2, + "steps": 1261, + "visited": 44 + }, + { + "p_bits": 74, + "d": 3, + "e": 1, + "q": 3, + "joined": false, + "cutoff": 2, + "steps": 2508, + "visited": 403 + }, + { + "p_bits": 74, + "d": 3, + "e": 3, + "q": 3, + "joined": false, + "cutoff": 2, + "steps": 3198, + "visited": 407 + }, + { + "p_bits": 2, + "d": 4, + "e": 1, + "q": 3, + "joined": false, + "cutoff": 2, + "steps": 835, + "visited": 50 + }, + { + "p_bits": 2, + "d": 4, + "e": 4, + "q": 3, + "joined": false, + "cutoff": 2, + "steps": 1606, + "visited": 55 + }, + { + "p_bits": 2, + "d": 8, + "e": 1, + "q": 3, + "joined": false, + "cutoff": 2, + "steps": 1094, + "visited": 63 + }, + { + "p_bits": 2, + "d": 8, + "e": 8, + "q": 3, + "joined": false, + "cutoff": 2, + "steps": 2081, + "visited": 72 + }, + { + "p_bits": 74, + "d": 9, + "e": 1, + "q": 3, + "joined": false, + "cutoff": 2, + "steps": 2918, + "visited": 423 + }, + { + "p_bits": 74, + "d": 9, + "e": 9, + "q": 3, + "joined": false, + "cutoff": 3, + "steps": 5254, + "visited": 436 + }, + { + "p_bits": 74, + "d": 15, + "e": 1, + "q": 3, + "joined": false, + "cutoff": 2, + "steps": 3182, + "visited": 435 + }, + { + "p_bits": 74, + "d": 15, + "e": 15, + "q": 3, + "joined": false, + "cutoff": 3, + "steps": 5826, + "visited": 454 + }, + { + "p_bits": 2, + "d": 16, + "e": 1, + "q": 3, + "joined": false, + "cutoff": 2, + "steps": 1569, + "visited": 84 + }, + { + "p_bits": 2, + "d": 16, + "e": 16, + "q": 3, + "joined": false, + "cutoff": 3, + "steps": 4270, + "visited": 104 + }, + { + "p_bits": 74, + "d": 17, + "e": 1, + "q": 3, + "joined": false, + "cutoff": 2, + "steps": 3393, + "visited": 443 + }, + { + "p_bits": 74, + "d": 17, + "e": 17, + "q": 3, + "joined": false, + "cutoff": 3, + "steps": 6140, + "visited": 464 + }, + { + "p_bits": 2, + "d": 24, + "e": 1, + "q": 3, + "joined": false, + "cutoff": 2, + "steps": 1971, + "visited": 100 + }, + { + "p_bits": 2, + "d": 24, + "e": 24, + "q": 3, + "joined": false, + "cutoff": 3, + "steps": 5062, + "visited": 128 + }, + { + "p_bits": 74, + "d": 25, + "e": 1, + "q": 3, + "joined": false, + "cutoff": 2, + "steps": 3795, + "visited": 459 + }, + { + "p_bits": 74, + "d": 25, + "e": 25, + "q": 3, + "joined": false, + "cutoff": 3, + "steps": 6943, + "visited": 488 + }, + { + "p_bits": 2, + "d": 26, + "e": 1, + "q": 3, + "joined": false, + "cutoff": 2, + "steps": 2049, + "visited": 104 + }, + { + "p_bits": 2, + "d": 26, + "e": 26, + "q": 3, + "joined": false, + "cutoff": 3, + "steps": 5243, + "visited": 134 + }, + { + "p_bits": 74, + "d": 31, + "e": 1, + "q": 3, + "joined": false, + "cutoff": 2, + "steps": 4059, + "visited": 471 + }, + { + "p_bits": 74, + "d": 31, + "e": 31, + "q": 3, + "joined": false, + "cutoff": 4, + "steps": 10087, + "visited": 509 + }, + { + "p_bits": 2, + "d": 32, + "e": 1, + "q": 3, + "joined": false, + "cutoff": 2, + "steps": 2476, + "visited": 121 + }, + { + "p_bits": 2, + "d": 32, + "e": 32, + "q": 3, + "joined": false, + "cutoff": 4, + "steps": 8550, + "visited": 160 + }, + { + "p_bits": 74, + "d": 33, + "e": 1, + "q": 3, + "joined": false, + "cutoff": 2, + "steps": 4300, + "visited": 479 + }, + { + "p_bits": 74, + "d": 33, + "e": 33, + "q": 3, + "joined": false, + "cutoff": 4, + "steps": 10431, + "visited": 519 + }, + { + "p_bits": 74, + "d": 63, + "e": 1, + "q": 3, + "joined": false, + "cutoff": 2, + "steps": 5800, + "visited": 539 + }, + { + "p_bits": 74, + "d": 63, + "e": 63, + "q": 3, + "joined": false, + "cutoff": 4, + "steps": 13388, + "visited": 609 + }, + { + "p_bits": 2, + "d": 64, + "e": 1, + "q": 3, + "joined": false, + "cutoff": 2, + "steps": 4247, + "visited": 190 + }, + { + "p_bits": 2, + "d": 64, + "e": 64, + "q": 3, + "joined": false, + "cutoff": 4, + "steps": 11881, + "visited": 261 + }, + { + "p_bits": 74, + "d": 65, + "e": 1, + "q": 3, + "joined": false, + "cutoff": 2, + "steps": 6071, + "visited": 547 + }, + { + "p_bits": 74, + "d": 65, + "e": 65, + "q": 3, + "joined": false, + "cutoff": 5, + "steps": 18544, + "visited": 622 + }, + { + "p_bits": 74, + "d": 1, + "e": 1, + "q": 5, + "joined": false, + "cutoff": 1, + "steps": 2401, + "visited": 394 + }, + { + "p_bits": 2, + "d": 2, + "e": 1, + "q": 5, + "joined": false, + "cutoff": 2, + "steps": 783, + "visited": 41 + }, + { + "p_bits": 2, + "d": 2, + "e": 2, + "q": 5, + "joined": false, + "cutoff": 2, + "steps": 1502, + "visited": 44 + }, + { + "p_bits": 74, + "d": 3, + "e": 1, + "q": 5, + "joined": false, + "cutoff": 2, + "steps": 2607, + "visited": 403 + }, + { + "p_bits": 74, + "d": 3, + "e": 3, + "q": 5, + "joined": false, + "cutoff": 2, + "steps": 3492, + "visited": 408 + }, + { + "p_bits": 2, + "d": 4, + "e": 1, + "q": 5, + "joined": false, + "cutoff": 2, + "steps": 934, + "visited": 50 + }, + { + "p_bits": 2, + "d": 4, + "e": 4, + "q": 5, + "joined": false, + "cutoff": 2, + "steps": 1953, + "visited": 57 + }, + { + "p_bits": 2, + "d": 8, + "e": 1, + "q": 5, + "joined": false, + "cutoff": 2, + "steps": 1193, + "visited": 63 + }, + { + "p_bits": 2, + "d": 8, + "e": 8, + "q": 5, + "joined": false, + "cutoff": 2, + "steps": 2579, + "visited": 74 + }, + { + "p_bits": 74, + "d": 9, + "e": 1, + "q": 5, + "joined": false, + "cutoff": 2, + "steps": 3017, + "visited": 423 + }, + { + "p_bits": 74, + "d": 9, + "e": 9, + "q": 5, + "joined": false, + "cutoff": 2, + "steps": 4506, + "visited": 435 + }, + { + "p_bits": 74, + "d": 15, + "e": 1, + "q": 5, + "joined": false, + "cutoff": 2, + "steps": 3281, + "visited": 435 + }, + { + "p_bits": 74, + "d": 15, + "e": 15, + "q": 5, + "joined": false, + "cutoff": 2, + "steps": 5300, + "visited": 453 + }, + { + "p_bits": 2, + "d": 16, + "e": 1, + "q": 5, + "joined": false, + "cutoff": 2, + "steps": 1668, + "visited": 84 + }, + { + "p_bits": 2, + "d": 16, + "e": 16, + "q": 5, + "joined": false, + "cutoff": 2, + "steps": 3768, + "visited": 103 + }, + { + "p_bits": 74, + "d": 17, + "e": 1, + "q": 5, + "joined": false, + "cutoff": 2, + "steps": 3492, + "visited": 443 + }, + { + "p_bits": 74, + "d": 17, + "e": 17, + "q": 5, + "joined": false, + "cutoff": 2, + "steps": 5659, + "visited": 463 + }, + { + "p_bits": 2, + "d": 24, + "e": 1, + "q": 5, + "joined": false, + "cutoff": 2, + "steps": 2070, + "visited": 100 + }, + { + "p_bits": 2, + "d": 24, + "e": 24, + "q": 5, + "joined": false, + "cutoff": 2, + "steps": 4592, + "visited": 127 + }, + { + "p_bits": 74, + "d": 25, + "e": 1, + "q": 5, + "joined": false, + "cutoff": 2, + "steps": 3894, + "visited": 459 + }, + { + "p_bits": 74, + "d": 25, + "e": 25, + "q": 5, + "joined": false, + "cutoff": 2, + "steps": 6473, + "visited": 487 + }, + { + "p_bits": 2, + "d": 26, + "e": 1, + "q": 5, + "joined": false, + "cutoff": 2, + "steps": 2148, + "visited": 104 + }, + { + "p_bits": 2, + "d": 26, + "e": 26, + "q": 5, + "joined": false, + "cutoff": 2, + "steps": 4773, + "visited": 133 + }, + { + "p_bits": 74, + "d": 31, + "e": 1, + "q": 5, + "joined": false, + "cutoff": 2, + "steps": 4158, + "visited": 471 + }, + { + "p_bits": 74, + "d": 31, + "e": 31, + "q": 5, + "joined": false, + "cutoff": 2, + "steps": 7046, + "visited": 505 + }, + { + "p_bits": 2, + "d": 32, + "e": 1, + "q": 5, + "joined": false, + "cutoff": 2, + "steps": 2575, + "visited": 121 + }, + { + "p_bits": 2, + "d": 32, + "e": 32, + "q": 5, + "joined": false, + "cutoff": 2, + "steps": 5509, + "visited": 156 + }, + { + "p_bits": 74, + "d": 33, + "e": 1, + "q": 5, + "joined": false, + "cutoff": 2, + "steps": 4399, + "visited": 479 + }, + { + "p_bits": 74, + "d": 33, + "e": 33, + "q": 5, + "joined": false, + "cutoff": 3, + "steps": 11270, + "visited": 522 + }, + { + "p_bits": 74, + "d": 63, + "e": 1, + "q": 5, + "joined": false, + "cutoff": 2, + "steps": 5899, + "visited": 539 + }, + { + "p_bits": 74, + "d": 63, + "e": 63, + "q": 5, + "joined": false, + "cutoff": 3, + "steps": 15343, + "visited": 612 + }, + { + "p_bits": 2, + "d": 64, + "e": 1, + "q": 5, + "joined": false, + "cutoff": 2, + "steps": 4346, + "visited": 190 + }, + { + "p_bits": 2, + "d": 64, + "e": 64, + "q": 5, + "joined": false, + "cutoff": 3, + "steps": 13893, + "visited": 264 + }, + { + "p_bits": 74, + "d": 65, + "e": 1, + "q": 5, + "joined": false, + "cutoff": 2, + "steps": 6170, + "visited": 547 + }, + { + "p_bits": 74, + "d": 65, + "e": 65, + "q": 5, + "joined": false, + "cutoff": 3, + "steps": 15798, + "visited": 622 + }, + { + "p_bits": 128, + "d": 1, + "e": 1, + "q": 100000000000000, + "joined": false, + "cutoff": 1, + "steps": 9002, + "visited": 664 + }, + { + "p_bits": 128, + "d": 2, + "e": 2, + "q": 100000000000000, + "joined": false, + "cutoff": 2, + "steps": 18871, + "visited": 674 + }, + { + "p_bits": 128, + "d": 3, + "e": 3, + "q": 100000000000000, + "joined": false, + "cutoff": 2, + "steps": 22083, + "visited": 678 + }, + { + "p_bits": 128, + "d": 9, + "e": 9, + "q": 100000000000000, + "joined": false, + "cutoff": 2, + "steps": 40734, + "visited": 710 + }, + { + "p_bits": 128, + "d": 17, + "e": 17, + "q": 100000000000000, + "joined": false, + "cutoff": 2, + "steps": 65403, + "visited": 746 + }, + { + "p_bits": 128, + "d": 65, + "e": 65, + "q": 100000000000000, + "joined": false, + "cutoff": 2, + "steps": 209745, + "visited": 946 + }, + { + "p_bits": 7, + "d": 16, + "e": 16, + "q": 2, + "joined": true, + "cutoff": 4, + "steps": 6899, + "visited": 171 + }, + { + "p_bits": 7, + "d": 17, + "e": 2, + "q": 2, + "joined": true, + "cutoff": 3, + "steps": 2283, + "visited": 115 + }, + { + "p_bits": 7, + "d": 27, + "e": 27, + "q": 3, + "joined": true, + "cutoff": 3, + "steps": 11001, + "visited": 236 + }, + { + "p_bits": 7, + "d": 28, + "e": 7, + "q": 3, + "joined": true, + "cutoff": 4, + "steps": 8924, + "visited": 180 + }, + { + "p_bits": 7, + "d": 33, + "e": 33, + "q": 5, + "joined": true, + "cutoff": 3, + "steps": 15854, + "visited": 280 + }, + { + "p_bits": 7, + "d": 17, + "e": 17, + "q": 100000000000000, + "joined": true, + "cutoff": 2, + "steps": 64849, + "visited": 187 + } + ] +} diff --git a/research/selected-header-cutoff/evidence/normal.json b/research/selected-header-cutoff/evidence/normal.json new file mode 100644 index 0000000000..29ace36952 --- /dev/null +++ b/research/selected-header-cutoff/evidence/normal.json @@ -0,0 +1,35 @@ +{ + "alphabet_size_n3_sites2": 6, + "control_names": [ + "invalid-fixed-exponent", + "invalid-fixed-exponent", + "invalid-fixed-exponent", + "borrowed-header-return", + "sentinel-equality", + "perfect-power-strictness", + "Gamma-d-doubling", + "cutoff-retirement", + "product-saturation", + "wrong-cutoff-exponent", + "undercharged-total-time", + "false-root-width-only-space", + "frozen-source-corruption" + ], + "counted_selected_nodes": 1324, + "counted_transitions": 3573948, + "direct_saturated_products": 204, + "exact_power_boundary_cases": 27, + "finite_cases": 357, + "formal_kernel": "not_run", + "independent_dense_cases": 6, + "kappa": "unchanged", + "n3_sites2_instruction_count": 5951, + "negative_controls": 13, + "scope": "literal header/cutoff/control composition; payload and Q0 producer retained", + "selected_Q": 100000000000000, + "selected_Q_cases": 7, + "selected_Q_power_stages": 64, + "source_sha256": "1f67f85d14f472e94e05072c4d9840ff9b79ee7d944e2fb1699c44e4b9b8687d", + "status": "PASS_SELECTED_HEADER_CUTOFF_PREFIX", + "tapes": 11 +} diff --git a/research/selected-header-cutoff/evidence/optimized.json b/research/selected-header-cutoff/evidence/optimized.json new file mode 100644 index 0000000000..29ace36952 --- /dev/null +++ b/research/selected-header-cutoff/evidence/optimized.json @@ -0,0 +1,35 @@ +{ + "alphabet_size_n3_sites2": 6, + "control_names": [ + "invalid-fixed-exponent", + "invalid-fixed-exponent", + "invalid-fixed-exponent", + "borrowed-header-return", + "sentinel-equality", + "perfect-power-strictness", + "Gamma-d-doubling", + "cutoff-retirement", + "product-saturation", + "wrong-cutoff-exponent", + "undercharged-total-time", + "false-root-width-only-space", + "frozen-source-corruption" + ], + "counted_selected_nodes": 1324, + "counted_transitions": 3573948, + "direct_saturated_products": 204, + "exact_power_boundary_cases": 27, + "finite_cases": 357, + "formal_kernel": "not_run", + "independent_dense_cases": 6, + "kappa": "unchanged", + "n3_sites2_instruction_count": 5951, + "negative_controls": 13, + "scope": "literal header/cutoff/control composition; payload and Q0 producer retained", + "selected_Q": 100000000000000, + "selected_Q_cases": 7, + "selected_Q_power_stages": 64, + "source_sha256": "1f67f85d14f472e94e05072c4d9840ff9b79ee7d944e2fb1699c44e4b9b8687d", + "status": "PASS_SELECTED_HEADER_CUTOFF_PREFIX", + "tapes": 11 +} diff --git a/research/selected-header-cutoff/evidence/peer-proof.json b/research/selected-header-cutoff/evidence/peer-proof.json new file mode 100644 index 0000000000..bbebed216d --- /dev/null +++ b/research/selected-header-cutoff/evidence/peer-proof.json @@ -0,0 +1,60 @@ +{ + "status": "PASS_PROOF_SOURCE_COST_REVIEW", + "method": "manual independent control-flow and universal cost derivation; exact source-byte and rational checks; no author machine/verifier execution", + "source_checks": [ + { + "source": "upstream/build/sections/02-streams.tex", + "sha256": "606c80db61cad13aa0c3b6060dc4b88dbbe7ac60cdd831aa93f28d908fd09dab", + "git_blob": "088fceea1867abc76271d7efe7532b779fee9039", + "size": 11311, + "removed_known_extra_terminal_newline": false + }, + { + "source": "upstream/build/sections/05-layers.tex", + "sha256": "20cfc8d12099d4e4ed9e3e7eeb6162edd9b6e0e076f24693364cd24377252594", + "git_blob": "5ce8b3c83c455f221bb84858a97230b0285644aa", + "size": 46811, + "removed_known_extra_terminal_newline": false + }, + { + "source": "upstream/build/sections/08-assembly.tex", + "sha256": "763d7945b1e1ec4ebae9b799bcefcc45fa9bae6e2ffad799868a9c3d513dbd4a", + "git_blob": "337810a1d9a58a2ecf14123420923c039ba322a6", + "size": 46444, + "removed_known_extra_terminal_newline": false + }, + { + "source": "research/shared-wire-split-composition/interval_gate.py", + "sha256": "60a743d13f668ef86db4b8215b4d5d04430a671ba6f1fe06d9c1c4c3dfe86da5", + "git_blob": "e24dc46079b4c25152f5afc096dda2ce8ee58ff5", + "size": 6886, + "removed_known_extra_terminal_newline": false + }, + { + "source": "research/shared-wire-split-composition/FULL-RESULT.json", + "sha256": "d9ba709fa5dcefffe3f3abdcf34600ce188224703cfd743e6db8b58ba4816cb7", + "git_blob": "ff3256f0d3ffbfc56b062f9ec0fdbbc7b30e76d5", + "size": 25225, + "removed_known_extra_terminal_newline": false + }, + { + "source": "notes/batched-complex-rows.tex", + "sha256": "64c70926a8705874f1c9b42a2f703e42cad4e90f927f544458cfdf729540236c", + "git_blob": "e13bd96eb29bdc6526f10dc32e0a146bc17848a4", + "size": 6085, + "removed_known_extra_terminal_newline": true + } + ], + "selected_gap": "1/100000000000000", + "epsilon": "99999999999999/100000000000000", + "added_dC_exponent": "9999999999999999999999999999/10000000000000000000000000000", + "fixed_power_stages": 64, + "reviewed": { + "cutoff_prefix.py": "1f67f85d14f472e94e05072c4d9840ff9b79ee7d944e2fb1699c44e4b9b8687d", + "PROOF.md": "5cfa6f6c0a3c3eca790c7c155dcdff3b769dc320d3a5a9a31c7356cfe2d72262", + "SOURCES.json": "aa19dd4d24a2d760fbc2d5168bc44dddb221276b09fecef1278b2b5a5aa00830", + "inputs/controller_reference.py": "e664a748e6b6797d4b60f60a7a7dd68b59a5608acf56b9c5d8b466f363755f73", + "inputs/selected_control.py": "1c977e9f4864d338f874aa4943d9f3422d964c3ab0cc2f877d9bc4c2d9e20237" + }, + "review_sha256": "82c87434df5569c940124fba4b56d19dfc1002627946478aac0c0ed05eb30682" +} diff --git a/research/selected-header-cutoff/independent_check.py b/research/selected-header-cutoff/independent_check.py new file mode 100644 index 0000000000..8b269efca1 --- /dev/null +++ b/research/selected-header-cutoff/independent_check.py @@ -0,0 +1,103 @@ +"""Independent dense tape CPU for the header/cutoff prefix. +No author input builder, interpreter, or verifier is called. +Prepared for CubeJerry with substantial OpenAI assistance. Apache-2.0. +""" +from pathlib import Path +from importlib.util import module_from_spec,spec_from_file_location +from hashlib import sha256 +import json,sys +PKG=Path(sys.argv[1]).resolve() if len(sys.argv)>1 else Path(__file__).resolve().parent +spec=spec_from_file_location('checked_cutoff',PKG/'cutoff_prefix.py') +C=module_from_spec(spec);spec.loader.exec_module(C) +def need(ok,reason): + if not ok:raise ValueError(reason) +def gamma(v): + s=format(v,'b');return '0'*(len(s)-1)+s +def run(p,d,e,q,joined=False,mutate=None): + code=C.compile_joined(3,2,q)[0] if joined else C.compile_prefix(q)[0] + if mutate is not None:code=mutate(list(code)) + cutoff=next(t for t in range(1,e+2) if t==e+1 or (t**q>=d if q<100 else d==1 or t>=2)) + need(q<100 or d.bit_length()<=q,'selected-Q oracle range') + header=gamma(p)+gamma(d)+'01001101110101' + margin=9;limit=max(6*d+100,len(header)+100) + tapes=[['_']*(margin+limit+10) for _ in range(11)] + origins=[13*i-71 for i in range(11)] + heads=origins[:];low=heads[:];high=heads[:] + for a in tapes: + a[margin-5:margin]=['1','t0','0','1','|'] + a[margin+limit:margin+limit+3]=['t0','1','|'] + for i in (3,5,6,7,8,9,10):tapes[i][margin-1]='_' + tapes[0][margin:margin+e]=['1']*e + tapes[4][margin:margin+len(header)]=list(header) + before=[a[:] for a in tapes];seen=[];pc=steps=0 + stage_count=q.bit_length()+q.bit_count() + allowance=1000*(stage_count+1)*(len(gamma(p)+gamma(d))+d*cutoff+1) + if joined: + pending=[e];mass=0 + while pending: + x=pending.pop();mass+=x + if x>=max(3,cutoff):pending.extend([x//3,x//3]) + allowance+=200*3*mass + while steps=o-(i!=4) for i,(lo,o) in enumerate(zip(low,origins))),'ancestor locality') + return dict(p_bits=p.bit_length(),d=d,e=e,q=q,joined=joined,cutoff=cutoff,steps=steps, + visited=sum(hi-lo+1 for hi,lo in zip(high,low))) + +def main(): + rows=[] + for q in (2,3,5): + for d in (1,2,3,4,8,9,15,16,17,24,25,26,31,32,33,63,64,65): + for e in sorted({1,d}): + p=(1<<73)+5 if d%2 else 3 + rows.append(run(p,d,e,q)) + for d in (1,2,3,9,17,65): + rows.append(run((1<<127)+19,d,d,C.SELECTED_Q)) + for q,d,e in ((2,16,16),(2,17,2),(3,27,27),(3,28,7), + (5,33,33),(C.SELECTED_Q,17,17)): + rows.append(run(97,d,e,q,joined=True)) + controls=[] + def wrong_header(code): + i=code.index(('move',4,-1));code[i]=('move',4,1);return code + def skipped_retirement(code): + at=C.compile_joined(3,2,2)[2]['cleanup_at'] + code[at]=('goto',len(code)-2);return code + fixtures=[('header return',lambda:run(16,9,9,2,mutate=wrong_header),'prefix boundary'), + ('cutoff retirement',lambda:run(16,9,9,2,joined=True,mutate=skipped_retirement),'full endpoint'), + ('wrong exponent',lambda:run(16,16,8,2,mutate=lambda _:C.compile_prefix(3)[0]),'prefix boundary')] + for name,fn,want in fixtures: + try:fn() + except ValueError as error: + need(str(error)==want,'expected semantic rejection');controls.append(name) + else:raise ValueError('mutant survived') + print(json.dumps(dict(status='PASS',method='independent dense CPU and exact integer-root oracle', + cases=len(rows),transitions=sum(r['steps'] for r in rows),negative_controls=controls, + source_sha256=sha256((PKG/'cutoff_prefix.py').read_bytes()).hexdigest(),rows=rows),indent=2)) + +if __name__=='__main__':main() diff --git a/research/selected-header-cutoff/inputs/controller_reference.py b/research/selected-header-cutoff/inputs/controller_reference.py new file mode 100644 index 0000000000..3ab6d0361f --- /dev/null +++ b/research/selected-header-cutoff/inputs/controller_reference.py @@ -0,0 +1,112 @@ +"""Finite three-tape online rank-recursion control; Apache-2.0. +Only PC and local symbols affect execution. Metrics/event logs are observers. +""" +from dataclasses import dataclass, field +BLANK, ONE, MARK = '_', '1', '|' +WIDTH, CHILD, STACK = range(3) + +class Builder: + def __init__(self): self.code, self.labels, self.serial = [], {}, 0 + def mark(self,n): + if n in self.labels: raise ValueError('duplicate label') + self.labels[n]=len(self.code) + def op(self,*x): self.code.append(x) + def rewind(self,t,symbols): + self.serial+=1; loop=f'rw{self.serial}'; done=loop+'done' + self.op('move',t,-1); self.mark(loop) + self.op('read',t,{s:loop+'step' for s in symbols}|{MARK:done}) + self.mark(loop+'step'); self.op('move',t,-1); self.op('goto',loop) + self.mark(done); self.op('move',t,1) + def finish(self,alphabet): + result=[] + for op,*a in self.code: + if op=='goto': a[0]=self.labels[a[0]] + elif op=='read': a[1]={s:self.labels[n] for s,n in a[1].items()} + result.append((op,*a)) + return tuple(result),tuple(alphabet) + +def compile_controller(m,ranks): + """Parameters are compile-time constants, absent from run-time state.""" + if type(m) is not int or m<2 or not ranks: raise ValueError('bad fixed profile') + if any(type(r) is not int or not 1<=r=budget: raise ValueError('finite verifier budget') + self.step() + return self + +def initial_tapes(width,origins=(0,0,0),ancestor=('0','1','t0','_','|','0')): + if width<1: raise ValueError('positive width') + u,c,p=origins + return [Tape({u-1:MARK,**{u+i:ONE for i in range(width)}},u),Tape({c-1:MARK},c), + Tape({p-1:MARK,**{p-2-i:s for i,s in enumerate(ancestor) if s!=BLANK}},p)] diff --git a/research/selected-header-cutoff/inputs/selected_control.py b/research/selected-header-cutoff/inputs/selected_control.py new file mode 100644 index 0000000000..b3ffa7c4ac --- /dev/null +++ b/research/selected-header-cutoff/inputs/selected_control.py @@ -0,0 +1,59 @@ +"""Final rank-one control with supplied cutoff and explicit remainder hooks. + +The credited frozen Builder/interpreter performs literal local tape steps. +No payload or external cutoff producer is included. Apache-2.0. +""" +from controller_reference import Builder,Machine,Tape,initial_tapes,BLANK,ONE,MARK,WIDTH,CHILD,STACK +CUTOFF=3 + +def remainder(a,m,prefix,event,next_state): + a.mark(prefix);a.op('goto',prefix+'r0') + for r in range(m): + a.mark(prefix+f'r{r}');a.op('read',WIDTH,{ONE:prefix+f'b{r}',BLANK:prefix+f'e{r}'}) + a.mark(prefix+f'b{r}');a.op('move',WIDTH,1);a.op('goto',prefix+f'r{(r+1)%m}') + a.mark(prefix+f'e{r}');a.rewind(WIDTH,(ONE,));a.op('emit',event+str(r));a.op('goto',next_state) + +def compile_selected(m,sites): + if type(m) is not int or m<2 or type(sites) is not int or sites<1:raise ValueError('invalid fixed template') + tags=tuple(f't{i}' for i in range(sites));a=Builder();a.mark('enter');a.op('read',WIDTH,{ONE:'probe0'}) + for k in range(m): + a.mark(f'probe{k}');a.op('read',WIDTH,{ONE:f'advance{k}',BLANK:f'leaf{k}'}) + a.mark(f'advance{k}');a.op('move',WIDTH,1);a.op('goto',f'probe{k+1}' if k+1= d) + + +def events(n, sites, e, cutoff): + if e < max(n, cutoff): + return [("L", e), ("X", e)], e, 1, 0 + remainder = e % n + out = [("E", e), ("B" + str(remainder), e)] + mass, nodes, depth = e, 1, 0 + for i in range(sites): + child = e // n + ev, cm, cn, cd = events(n, sites, child, cutoff) + out += [("D" + str(i), child)] + ev + [("U" + str(i), e)] + mass += cm + nodes += cn + depth = max(depth, cd + 1) + return out + [("A" + str(remainder), e), ("X", e)], mass, nodes, depth + + +def inspect_run(code, tapes, origins, cutoff, expected, bound): + saved = [(t.cells.copy(), t.head) for t in tapes] + machine = C.Machine(code, tapes) + observed = [] + ready = False + while not machine.halted: + need(machine.steps < bound, "complete transition budget") + ins = code[machine.pc] + if ins[0] == "emit": + name = ins[1] + if name == "READY": + need(not ready, "unique prefix handoff") + ready = True + need(unary(tapes[C.CUTOFF], origins[C.CUTOFF]) == cutoff, "generated cutoff") + for j, t in enumerate(tapes): + if j != C.CUTOFF: + need((t.cells, t.head) == saved[j], "prefix input/scratch restoration") + need(tapes[C.CUTOFF].head == origins[C.CUTOFF], "cutoff handoff head") + elif name == "RETIRED": + need(ready, "retirement after ready") + need(all((t.cells, t.head) == s for t, s in zip(tapes, saved)), "cutoff retirement") + else: + need(ready, "selected control before prefix") + need(unary(tapes[C.CUTOFF], origins[C.CUTOFF]) == cutoff, "retained cutoff") + need(tapes[C.CUTOFF].head == origins[C.CUTOFF], "retained cutoff head") + observed.append((name, unary(tapes[C.WIDTH], origins[C.WIDTH]))) + machine.step() + need(observed == expected, "exact composed event/width contour") + need(machine.events[0] == "READY" and machine.events[-1] == "RETIRED", "handoff edges") + need(all((t.cells, t.head) == s for t, s in zip(tapes, saved)), "complete endpoint") + for j, tape in enumerate(tapes): + floor = origins[j] if j == C.HEADER else origins[j] - 1 + need(tape.low >= floor, "ancestor visit") + return machine + + +def one(n, sites, q, p, d, e, origins=None, supplied_code=None): + origins = (0,) * 11 if origins is None else tuple(origins) + code, alphabet, meta = C.compile_joined(n, sites, q) + need(meta["prefix"] == 273 + 84 * meta["power_stages"], "prefix instruction census") + need(meta["cleanup"] == 14, "retirement instruction census") + need(len(code) == 329 + 84 * meta["power_stages"] + 30 * n + sites * (69 + 3 * n), + "joined instruction census") + if supplied_code is not None: + code = supplied_code + cutoff = root_cutoff(d, e, q) + expected, mass, nodes, depth = events(n, sites, e, cutoff) + h = len(C.gamma(p) + C.gamma(d)) + prep_bill = 1000 * (meta["power_stages"] + 1) * (h + d * cutoff + 1) + bill = prep_bill + 200 * (sites + 1) * mass + ts = C.initial(p, d, e, origins) + machine = inspect_run(code, ts, origins, cutoff, expected, bill) + span = sum(t.high - t.low + 1 for t in ts) + backing_bill = (5 + Fraction(n, n - 1)) * e + 5 * d + 4 * h + 40 + need(span <= backing_bill, "historical backing bill") + need(ts[C.HEADER].high <= origins[C.HEADER] + h, "header prefix access") + need(len(alphabet) == sites + 4, "fixed alphabet") + return machine.steps, nodes, cutoff, span, expected + + +def dense(code, original, limit): + """Separately implemented dense interpreter; no Machine/Tape methods.""" + low = min(t.head for t in original) - 40 + high = max(t.head for t in original) + 10000 + arrays = [[C.BLANK] * (high - low + 1) for _ in original] + heads = [t.head for t in original] + for j, t in enumerate(original): + for at, symbol in t.cells.items(): + arrays[j][at - low] = symbol + pc = steps = 0 + emitted = [] + while steps < limit: + ins = code[pc] + op = ins[0] + steps += 1 + if op == "halt": + return steps, emitted, heads, arrays, low + if op == "goto": + pc = ins[1] + continue + if op == "read": + pc = ins[2][arrays[ins[1]][heads[ins[1]] - low]] + continue + if op == "write": + arrays[ins[1]][heads[ins[1]] - low] = ins[2] + elif op == "move": + heads[ins[1]] += ins[2] + elif op == "emit": + emitted.append(ins[1]) + else: + raise ValueError("unknown dense opcode") + pc += 1 + raise ValueError("dense transition limit") + + +def rejects(mutated, q, p, d, e, factor=3): + n, sites = 2, 1 + baseline = one(n, sites, q, p, d, e)[0] + cutoff = root_cutoff(d, e, q) + expected = events(n, sites, e, cutoff)[0] + try: + inspect_run(mutated, C.initial(p, d, e), (0,) * 11, cutoff, + expected, factor * baseline + 100) + except (ValueError, KeyError): + return + raise ValueError("mutated program escaped detection") + + +def main(): + cases = steps = nodes = 0 + for q in (2, 3, 5): + for d in range(1, 33): + for e in sorted({1, d, max(1, d // 2), min(d, 3)}): + st, no, _, _, _ = one(3, 2, q, 2 * d + 1, d, e) + cases += 1 + steps += st + nodes += no + boundaries = 0 + for q in (2, 3, 5): + for t in range(2, 5): + for delta in (-1, 0, 1): + d = t ** q + delta + e = min(d, t + 1) + st, no, _, _, _ = one(2, 1, q, 2 * d + 1, d, e) + boundaries += 1 + steps += st + nodes += no + selected_cases = 0 + for d, e in ((1, 1), (2, 1), (2, 2), (7, 7), (31, 2), (257, 2), (4097, 1)): + st, no, _, _, _ = one(3, 2, C.SELECTED_Q, 2 * d + 1, d, e) + selected_cases += 1 + steps += st + nodes += no + + # Saturated multiplication is checked directly against min(a*b,d). + a = C.Builder() + C.saturated_multiply(a) + a.op("halt") + mul_code, _ = a.finish((C.BLANK, "0", C.ONE, C.MARK)) + products = 0 + for d in range(1, 9): + for x in range(1, d + 1): + for y in range(1, d + 1): + ts = C.initial(1, d, 1) + for j in (C.D, C.ACC, C.FACTOR, C.PRODUCT): + ts[j].cells[-1] = C.MARK + for j, size in ((C.D, d), (C.ACC, x), (C.FACTOR, y)): + ts[j].cells.update({k: C.ONE for k in range(size)}) + before = [(t.cells.copy(), t.head) for t in ts] + z = C.Machine(mul_code, ts).run(40 * min(x * y, d) + 40) + need(unary(ts[C.PRODUCT], 0) == min(x * y, d), "literal saturated product") + for j, tape in enumerate(ts): + if j != C.PRODUCT: + need((tape.cells, tape.head) == before[j], "multiplication inputs") + need(ts[C.PRODUCT].head == 0, "product head return") + products += 1 + + dense_cases = 0 + shifted = tuple(23 - 7 * j for j in range(11)) + for q, p, d, e in ((2, 31, 16, 5), (3, 37, 28, 4), (C.SELECTED_Q, 17, 7, 2)): + for origin in ((0,) * 11, shifted): + code, _, _ = C.compile_joined(3, 2, q) + st, _, _, _, _ = one(3, 2, q, p, d, e, origin) + original = C.initial(p, d, e, origin) + ds, de, dh, da, lo = dense(code, C.initial(p, d, e, origin), st + 1) + oracle_events = ["READY"] + [x[0] for x in events(3, 2, e, root_cutoff(d, e, q))[0]] + ["RETIRED"] + need((ds, de, dh) == (st, oracle_events, list(origin)), "independent dense CPU") + for j, tape in enumerate(original): + need({k + lo: v for k, v in enumerate(da[j]) if v != C.BLANK} == tape.cells, + "dense complete restoration") + dense_cases += 1 + + controls = [] + for q in (0, 1, True): + try: + C.compile_prefix(q) + except ValueError: + controls.append("invalid-fixed-exponent") + else: + raise ValueError("invalid exponent accepted") + code, _, meta = C.compile_joined(2, 1, 2) + bad = list(code) + j = next(i for i, ins in enumerate(bad) if ins == ("move", C.HEADER, -1)) + bad[j] = ("move", C.HEADER, 0) + rejects(tuple(bad), 2, 17, 4, 4) + controls.append("borrowed-header-return") + bad = list(code) + j = next(i for i, ins in enumerate(bad[:meta["prefix"] - 1]) + if ins[0] == "read" and ins[1] == C.CUTOFF and + bad[i + 1][0:2] == ("read", C.WIDTH)) + targets = dict(bad[j][2]) + targets[C.BLANK] = bad[j + 1][2][C.BLANK] + bad[j] = ("read", C.CUTOFF, targets) + rejects(tuple(bad), 2, 17, 9, 2) + controls.append("sentinel-equality") + bad = list(code) + j = next(i for i, ins in enumerate(bad[:meta["prefix"] - 1]) + if ins[0:2] == ("read", C.D) and bad[i + 1][0:2] == ("read", C.ACC)) + targets = dict(bad[j][2]) + targets[C.BLANK] = bad[j + 1][2][C.BLANK] + bad[j] = ("read", C.D, targets) + rejects(tuple(bad), 2, 17, 4, 4) + controls.append("perfect-power-strictness") + bad = list(code) + j = next(i for i, ins in enumerate(bad) if ins == ("write", C.PRODUCT, C.ONE)) + bad[j] = ("write", C.PRODUCT, C.BLANK) + rejects(tuple(bad), 2, 17, 4, 4) + controls.append("Gamma-d-doubling") + bad = list(code) + bad[meta["cleanup_at"]] = ("goto", len(bad) - 2) + rejects(tuple(bad), 2, 17, 4, 4) + controls.append("cutoff-retirement") + # Skipping one final multiplication saturation permits a too-long result. + bad = list(code) + mul_limits = [i for i, ins in enumerate(bad[:meta["prefix"] - 1]) + if ins[0:2] == ("read", C.D) and bad[i + 1][0:2] == ("read", C.FACTOR)] + j = mul_limits[-1] + targets = dict(bad[j][2]) + targets[C.BLANK] = targets[C.ONE] + bad[j] = ("read", C.D, targets) + rejects(tuple(bad), 2, 17, 3, 3) + controls.append("product-saturation") + wrong, _, _ = C.compile_joined(2, 1, 3) + rejects(wrong, 2, 17, 8, 4) + controls.append("wrong-cutoff-exponent") + baseline = one(2, 1, 2, 17, 4, 4)[0] + try: + C.Machine(code, C.initial(17, 4, 4)).run(baseline - 1) + except ValueError: + controls.append("undercharged-total-time") + else: + raise ValueError("undercharged execution passed") + _, _, _, span, _ = one(2, 1, 2, 4099, 2049, 1) + need(span > 100, "unary-d historical backing control") + controls.append("false-root-width-only-space") + with tempfile.TemporaryDirectory() as tmp: + target = Path(tmp) + (target / "inputs").mkdir() + (target / "cutoff_prefix.py").write_bytes(Path(C.__file__).read_bytes()) + for name in C.PINS: + data = (C.INPUTS / name).read_bytes() + if name == "selected_control.py": + data += b"\n# changed source\n" + (target / "inputs" / name).write_bytes(data) + process = subprocess.run([sys.executable, "-B", "-c", "import cutoff_prefix"], + cwd=target, capture_output=True, text=True, timeout=20) + need(process.returncode != 0 and "frozen controller dependency hash" in process.stderr, + "source corruption rejection") + controls.append("frozen-source-corruption") + + selected_code, selected_abc, selected_meta = C.compile_joined(3, 2) + source = Path(C.__file__).read_bytes() + print(json.dumps({ + "status": "PASS_SELECTED_HEADER_CUTOFF_PREFIX", + "finite_cases": cases, + "exact_power_boundary_cases": boundaries, + "selected_Q_cases": selected_cases, + "counted_transitions": steps, + "counted_selected_nodes": nodes, + "direct_saturated_products": products, + "independent_dense_cases": dense_cases, + "negative_controls": len(controls), + "control_names": controls, + "selected_Q": C.SELECTED_Q, + "selected_Q_power_stages": selected_meta["power_stages"], + "n3_sites2_instruction_count": len(selected_code), + "tapes": 11, + "alphabet_size_n3_sites2": len(selected_abc), + "source_sha256": hashlib.sha256(source).hexdigest(), + "scope": "literal header/cutoff/control composition; payload and Q0 producer retained", + "kappa": "unchanged", + "formal_kernel": "not_run", + }, sort_keys=True, indent=2)) + + +if __name__ == "__main__": + main()