diff --git a/research/first-face-reference-join/PROOF.md b/research/first-face-reference-join/PROOF.md new file mode 100644 index 0000000000..dd35fbaf22 --- /dev/null +++ b/research/first-face-reference-join/PROOF.md @@ -0,0 +1,334 @@ +# A complete sparse transport/consumer/return interface + +## 1. Result and hypotheses + +This note composes the separately pinned +[first-face tape transport](../sparse-halo-tape-transaction/PROOF.md) and +[shrinking-reference halo consumer](../shrinking-reference-halo/PROOF.md). +The composition itself is the result: a sorted saved stream enters the +consumer without host regrouping; its output returns to exactly the dense +boundary coordinates; every codec operation and its storage are priced. +The retained #4100 first-face geometry and #6880 numerical splice are +predecessor mechanisms, not new claims here. + +Let `L=2^ell`, `N_i=2^(k_i+ell)`, `k_i>=1`, `L>4A`, and `0<=b=1`, `b_i=(J_i-1)W_i<=b`, a common grid +`2^-q`, radius `R`, and dyadic normalizers `a_i=2^u_i` satisfying +`a_i delta_i>=1` and `q>=u_i`. The incoming dense values are exactly on that +grid and have component-l1 radius at most R. Their two sign-magnitude +components have the consumer's exact width `q+R.bit_length()+1`; the +transport payload is their concatenation, of width P. There is no free +precision conversion at the interface. A finer common grid may be supplied +before entry, with that caller work and radius accounted separately. + +For target intervals of lengths `m_i`, each consumer rectangle is the +expansion by `b_i`. The transport may save the larger common-b expansion. +Both expanded lengths are below `N_i`, because `L+2b<2L<=N_i`. +Thus each local offset has one unambiguous periodic coordinate. The +canonical input layout and dyadic descriptor remain transport premises. + +**Composed interface theorem.** Under these hypotheses and the two pinned +component theorems, the sequential codec in `join.py` preserves the exact +saved incoming numerical values and gives every discarded target exactly +the value produced by the consumer's global-reference rounded recurrence. +It preserves the current dense core value at every kept coordinate. The +complete movement and scalar-macro bill is the one in Section 5. This is +not an unconditional multiplication theorem: an actual same-reference +numerical core and the outer caller still require their own admission. + +## 2. Rectangle grouping, crop, and exact input identity + +For core c, first face f and side s, let the target local intervals be + +```text +i < f: [A,L-A) +i = f: [0,A) or [L-A,L) +i > f: [0,L). +``` + +Write their lower endpoints and lengths as `lo_i,m_i`, and absolute target +lower endpoints as `t_i=c_i L+lo_i`. The transport sorts complete keys + +```text +spectator || core fields || one-hot face || side + || common-b expanded local offsets || canonical source address. +``` + +All fields have fixed declared widths. Hence a rectangle is a contiguous +stream block, ordered lexicographically by its local offsets. A source +address is redundant after the full offset tuple because the expanded +intervals have no periodic aliases. One-hot binary ordering may place +larger face indices earlier; the codec requires contiguous grouping, not +increasing numerical face index. + +`Codec.run` reads the next prefix through actual transport tape reads and +unit moves. If it differs from the current prefix, the previous rectangle +is consumed and cleared before the new descriptor is constructed. Strictly +increasing prefixes are checked. No dictionary, indexed payload lookup, +array of rectangle bodies, or host sort performs the grouping. Live tuples +hold only the current encoded geometry/control fields. In particular, +payloads are never stored in a host container by the codec. + +For a common-b offset `u_i`, keep the record precisely when + +```text +b-b_i <= u_i < m_i+b+b_i, +``` + +then recode it as `v_i=u_i-(b-b_i)`. This selects exactly the smaller +consumer domain and preserves lexicographic order. The coordinate identity + +```text +(t_i-b_i)+v_i = (t_i-b)+u_i +``` + +holds over the integers, including when either side is outside the chosen +canonical period. The codec additionally checks the supplied canonical +source suffix against the right-hand side reduced modulo `N_i`. + +An odometer validates every full common-b offset exactly once before the +optional crop. The declared rectangle volume must match the observed +record count. The cropped count must match the consumer's volume. These +checks reject a missing/duplicated offset, a malformed prefix, or a foreign +source suffix on the admitted fixed-width schema. They are executable +boundary checks; the transport theorem already guarantees completeness +for its own output. + +The consumer's shorter offset fields receive the recoded unsigned key. +Each of the P payload bits is read from its current transport head and +written to the current consumer head with an explicit unit step. The codec +does not decode/re-encode the numeric payload. Therefore it neither changes +rounding nor silently normalizes a noncanonical negative zero. The +consumer's existing signed-word reader rejects that representation. + +## 3. Consumer chronology and exact return identity + +The transport saves the entire common-b input before core mutation. Its +saved role remains unchanged throughout consumer execution. One +`TensorWorkspace` is allocated before the first rectangle and reused for +all rectangles. Its eight physical roles return blank after each output +has been consumed; the same protected reference archive supplies every +local page. The generic proof charges the whole archive scan, including +other axes, and does not substitute a unit-cost coefficient oracle. + +The consumer retains the immutable input of each tensor axis until all +lines of that axis finish. Its shrinking-domain theorem establishes exact +agreement with the corresponding restriction of the full-period rounded +recurrence. This full dense recurrence is a proof/oracle device; the +production composition evaluates only the saved rectangles. + +An output key contains offsets relative to the consumer's original +expanded lower endpoints. A target coordinate has offset `b_i+r_i`, with +`0<=r_i1-epsilon`, and the other retained strict inequalities. The many +long sides of a rectangle then absorb repeated full archive scans. That +absorption is conditional on those growing-group inequalities; generic +fixed-dimensional calls retain the term in (2). Offline source production +is separately `2^o(p)=o(V)` for full bit volume `V=MP`. + +Across `O(d/g)` balanced groups, dense gather/return costs `O(Vd/g)`. +Transport and codec's sparse charge is `O(VdAp/L)`, while the complete +consumer charge is `O(VdgAp^6/L)`. Thus the combined additional charge is + +\[ + O(Vd/g+VdgAp^6/L)+2^{o(p)}, +\] + +inside the inherited conservative sparse halo allowance. With `A=p^48` +and `L>=p^400`, the second exponent is at most +`epsilon+beta+54-400<0`. This does not improve κ or establish the core, +all-column maps, full precision interface, compiler or outer recovery. +It replaces two named sparse-interface implementation premises with a +concrete composition and a complete conditional bill. + +## 7. Executed evidence and its limits + +The source-bound fixture is the retained original +`Reference(61,3,2,1,8,32)`, with period 64. The separate oracle checks all +4,096 original H entries, a certified gap `6255/8192`, cyclic bandwidth 4, +identity-hole rows 11/32/53, and nonzero across-period entries `(0,63)` and +`(63,0)`. Plans use `J=2`, `q=28`, `R=1`, and normalizer 2. Transport uses +`L=32`, `A=5`, `b=4`: four rectangles, 52 saved inputs, 20 targets. + +Three distinct numerical checks are retained. The streamed codec output +matches a separately loaded rectangle consumer bit for bit. A separately +written whole-grid recurrence, with independent toward-zero arithmetic and +global axis indexing, matches all target bits. Finally, exact Gaussian +elimination solves the original `Hy=x/2` with both complex components and +checks every residual; the actual target error is below the consumer bound. +The bound is deliberately loose for J=2, so it alone would not be an adequate +codec corruption control; exact bit equality is also required. + +Independent signed fixtures additionally cover a spectator coordinate, +two axes with unequal halos `(1,0)` and `(1,2)`, partial crops, irregular +identity holes and real wrap interactions. During codec/merge/erase the +independent review disables tape constructors and diagnostic `inspect`/ +`snapshot` calls. It checks the same fixed roles, current and historical +erasure invariants, and the unchanged protected archive. Raw negative +zero and a changed canonical source suffix are rejected. + +The joined controls also reject offset corruption, omitted wrap handling, +a missing saved input and a wrong return key. A payload-magnitude mutation +that remains within the fixture's radius is detected by exact delivery +comparison. Source pins, normal/optimized replays and the independent +review are reproducibility evidence. They do not constitute independent +human or formal proof-kernel acceptance. All five selected assumptions +remain; **No new κ**. diff --git a/research/first-face-reference-join/README.md b/research/first-face-reference-join/README.md new file mode 100644 index 0000000000..4f9830826e --- /dev/null +++ b/research/first-face-reference-join/README.md @@ -0,0 +1,179 @@ +# Source-bound first-face halo transaction + +**Result:** a complete, explicitly priced interface joining the new physical +first-face transport to the new shrinking-reference numerical consumer. +Original halo values are copied before core mutation, streamed into the +consumer through a checked coordinate codec, and returned exactly once to +the discarded dense coordinates. An actual retained Gaussian reference +exercises the whole interface, including identity holes and a period cut. + +**No new κ.** This supplies the sparse transport/consumer/return implication +that the component proofs require. An actual same-reference core and the +full outer multiplication proof remain separate obligations; all five +selected assumptions remain. + +## What the integrated contribution adds + +The two component packages are retained intact: + +- [Sparse halo tape transaction](../sparse-halo-tape-transaction/README.md) + supplies the 30-role finite-alphabet enumerator, complete sparse-key sort, + pre-copy chronology and unique return left open by #4870. +- [Shrinking reference halo](../shrinking-reference-halo/README.md) supplies + the numerical rectangle consumer from global reference band entries, + with shrinking domains, actual-input rounding bounds, paid page exposure, + eight reused local roles, and explicitly priced scalar/source arithmetic. + +The composition in [PROOF.md](PROOF.md) verifies their exact common +contract. A sorted rectangle prefix is consumed as one contiguous block; +there is no host dictionary or payload-array regrouping. A common saved +radius may be cropped to unequal numerical radii in one sparse pass. The +codec checks complete offsets and their canonical source suffixes, copies +payload cells unchanged, and converts only target keys back to canonical +global coordinates. The numerical payload grid, signed-word convention, +periodic coordinates, reference identity and dyadic normalizers agree. + +The inherited first-face combinatorics and copy-volume formula are not +reproved as new discoveries. The direct-Neumann degree `16p^4` was already +available in #6880. The new result is the implemented, proved and tested +composition, including its full physical and scalar-macro accounting. + +## Complete cost and scientific scope + +Let M be dense scalars, P their bit width, B their full coordinate width, +`C_B` all common-radius copies, `C_r` a cropped consumer rectangle's volume, +`R_rect` the number of rectangles, `G=sum_i N_i(2W_i+1)` the group archive +size, and w the complete encoded data/control width. The generic bound is + +```text +T_ref + O(M(P+B) + w^2 [C_B + R_rect g G + + sum_r C_r sum_i(J_i(2W_i+1)+K_r+1)]). +``` + +It retains source production `T_ref`, every repeated archive scan, all +common-radius copies, descriptor/key conversion, radix work, output copies, +returns and erasures. It does not charge a dense scan per numerical axis. +All retained backing, including erased temporary tables and bucket tails, +stays in the space bill. A fixed number of physical data/control roles +suffices; no role is allocated per rectangle or tensor dimension. + +The transport's reported tape actions use a 14-symbol alphabet and have a +constant-factor binary simulation. The consumer's reported data moves are +binary; its bounded integer arithmetic and the codec's sparse metadata +arithmetic use a separate ordinary quadratic bit tariff. The complete +composition is not advertised as a fully emitted binary transition table. +The descriptor width includes `log J` even when bandwidth is zero, and +includes cumulative record counters. + +Under the pinned balanced-group caller hypotheses, the complete additional +charge is `O(V d/g + V d g A p^6/L) + 2^o(p)`. This fits the inherited +conservative sparse halo allowance. It is a conditional implementation +substitution, not a stronger selected exponent or proof of the missing +core/outer premises. The generic formula remains necessary when a finite +instance does not satisfy the archive-amortization conditions. + +## Reproduce the complete contribution + +Canonical upstream base: +`7c49fe32c55de02c2c873655c804b16e4c3fef0a`. +The exact remote component tree parents are +`a2f3ce7358e8103f6eccd404e594276e9ccc04d8` (consumer) and +`630c9c2a5d6373ca103c55108bb606b4868bc6fd` (both components). +`SOURCES.json` pins live imported files by Git blob, SHA256 and these +heads; the final contribution descends from the combined parent. + +With Python 3.12 and the standard library, from the repository root: + +```sh +python3 -B research/first-face-reference-join/replay_all.py +``` + +Expected final line: `PASS_COMPLETE_FIRST_FACE_HALO_PACKAGE`. +The wrapper sequentially runs the registered checks for transport, +consumer, and join. It does not run unrelated repository suites. For only +the join, use: + +```sh +python3 -B scripts/research_package.py --package research/first-face-reference-join +``` + +Expected: `PASS_REGISTERED_RESEARCH_PACKAGE`. The join registers normal +and optimized (`-O`) runs of the actual-reference transaction and the +independent whole-grid review. Failures use explicit exceptions, not +assertions. No third-party dependencies are required. + +## Evidence + +The actual source is `Reference(61,3,2,1,8,32)`, period 64. Its 4,096 +original entries give a certified row gap `6255/8192`, identity-hole rows +11, 32 and 53, and nonzero coefficients across `0 <-> 63`. The fixture uses +`L=32`, `A=5`, saved radius 4, numerical half-bandwidth 4, two terms, +28-bit grid, radius one and normalizer two. + +Four rectangles save 52 inputs and return 20 targets. Three complementary +checks establish what those outputs mean: + +1. The streamed codec matches a separately loaded rectangle consumer + bit for bit, detecting changes too small for a loose error bound. +2. A separately written whole-period recurrence with independent arithmetic + and global indexing matches every returned bit. +3. Exact rational elimination solves the original `H y=x/2` and checks + every residual. Maximum target error is about `0.0003996004385`, below + the proved `0.036611087107` bound. These decimals summarize exact + rational comparisons; two terms are a finite interface fixture, not an + asymptotic precision allocation. + +The positive transaction executes 3,753,372 transport symbol actions and +1,055,928 consumer binary actions. The displayed conservative binary-tape +primitive bound is `10*B_actions+C_actions=38,589,648`, before scalar/control +macros and their fixed control compilation factor. It retains 21,740 +transport symbol cells and 41,978 consumer binary cells, including blank +backing after cleanup. Source production and coefficient arithmetic have +their separate retained bills; these figures are not a Python memory or +runtime benchmark. + +The separately assigned whole-grid review also checks a spectator fixture +and two signed two-axis fixtures with unequal numerical radii `(1,0)` and +`(1,2)`. The two-axis cases return 448 and 624 targets and crop 288 and 432 +saved records respectively. During codec, return and erase, it disables +tape constructors and diagnostic `inspect`/`snapshot` access, checks the +same eight consumer roles and unchanged archive, and checks full blank +backing afterward. The 1D and 2D numerical oracle does not use the codec's +grouping, local layouts or shrinking implementation. + +Controls reject a changed offset, omitted period wrap, missing saved +record, wrong return key, foreign source suffix and raw negative zero. +An in-radius payload magnitude mutation is detected by exact comparison. +The core in these fixtures is a bit-complementing test double. Kept +interior values are checked as opaque current-core bits and are never +interpreted as a validated Gaussian numerical output. + +`RESULT.json` records the exact actual-reference receipt. The component +receipts and full independently reviewable programs remain in their own +directories. Separate source-aware AI review is disclosed; independent +human or proof-kernel acceptance is not claimed. + +## Open next questions + +1. Admit a concrete rounded core on the same global reference, input grid + and dyadic normalizers. The splice then gives error + `max(E_keep,E_halo)` with no new codec defect. Start with one actual + caller core and its complete all-input contract. +2. Bind canonical group-layout production, ordinary child calls, source + transforms and all recovery scales into the selected outer proof. + The local time substitution and finite actual-reference fixture do not + discharge these global assumptions. Preserve the generic repeated-page + bill whenever the balanced-group absorption cannot yet be applied. + +Structured questions, first steps and blockers are in `TASK.json`. + +## Attribution + +Prepared for **@CubeJerry** with substantial OpenAI Codex assistance in +the transport, source-bound numerical consumer, composition, exact oracles +and separately assigned adversarial AI review. Credit Cinna Davis (#4100), +@codyw912's Astra/OpenAI-assisted #4870 enumeration package, Nick Petalas (#4217), +Jose Manuel (#4205/#4253), Ryanson Jonathan (#4517), JoyboyBrian (#5081), +the #6880 splice contribution, and their retained Gaussian/tape lineage. +The predecessor claims and attributions remain in both component packages. +Apache-2.0. diff --git a/research/first-face-reference-join/RESULT.json b/research/first-face-reference-join/RESULT.json new file mode 100644 index 0000000000..08a275465d --- /dev/null +++ b/research/first-face-reference-join/RESULT.json @@ -0,0 +1,107 @@ +{ + "binary_tape_primitive_upper_bound_before_scalar_macros": 38589648, + "codec": { + "control_carrier_units": 197, + "cropped_records": 0, + "cumulative_counter_bits": 20, + "encoded_plan_descriptor_bits": 93, + "quadratic_codec_tariff_units": 2949484, + "rectangles": 4, + "returned_records": 20, + "saved_records": 52, + "tariff_scope": "The complete encoded control block is O(control_carrier_units); an O(1) multiple of reported quadratic units covers sparse geometry/key macros. These are not measured binary transitions. Numeric source/consumer scalar macros remain separately charged.", + "transport_record_width": 84 + }, + "consumer_bill": { + "additions": 360, + "control_steps": 5868, + "maximum_single_tape_extent": 17280, + "moves": 707472, + "page_scans": 6, + "peak_scalar_bits": 54, + "products": 360, + "reads": 173912, + "roundings": 144, + "setup_divisions": 576, + "setup_entries": 576, + "source_shifts": 144, + "writes": 174544 + }, + "consumer_binary_actions": 1055928, + "consumer_data_roles_including_prepared_table": 10, + "consumer_retained_binary_cells": 41978, + "controls": [ + "offset", + "omit_wrap", + "drop_saved", + "return_key", + "payload_magnitude_exact_mismatch" + ], + "exact_delivery_match": true, + "final_sha256": "7b30e970a161bde5c7e35b8caba1b42063a8f5deef83628dceda6d8177da3dcf", + "maximum_original_inverse_error": [ + 827359109817392248798678000910818035802286303493738330288378207692097799147777735211442634813028519979204257177757246669511377410209076815399891254027152423134087507837884515052517038982214728551165310534364969914074521173026695476712503771487214898184159032862954708861356024875381268435011841407439204583226756030661807804434986984797968102285497033537378927825790801801771008272279354331434529334879098338757982379609320609009897816405177970743021044384254694603568495233063550319579917349615143207430285493734412545214764554721618974345354908406745879634498904338764910507698162301327263393284279638423381184148102797031456262660119385165587186079208489650916496382060254548520035648467444108509028369850513811325607206912378529871509919181918922470094398386252033537015059373761755542318366132336495714184767781577135628947871135788644502998205270021119514242922845428080390878453472650466265026071870366959914516240073750386789495645204649057799109550944010363343422012340525836624507048832315952477321646801679020355095245575486055091815439803801911905090641526213972660533346548585181007206680398842501464764892200323779539265634617404770188481324305076554143209531, + 2070465970912148396618734812346158841642385406471591226562308769346667041090487190222986810756111086506156570768230328898561059679572819345812740368548765689157482405953612075441566751926603568716532235718295868452717076124609132830801721762067740436730461226543322059734001755774653573312886732956556867023523524043696457494313825744305190122422625202506313669133947400847097839395532241493700337406441878004419970734927538613332775587531096410499109785713930409441290199790152373002455603497125910955473346928848316669893441586396046031512559015012073434526228438979101199896912638965270294174607960962283459128017626139200078924751309626030413466820883976848931162897588718349273994268940422287966510054153877835859072297965920198296507433084632314139788324946985658215429336415473999621806458236204495442257770137201423755547411206898172378391949242434053553964595646701546353222439458627406341020109150982102036154019869024771763748687804661904002962539875093064180694639492815103484657289952910558565335885287037093782783775888796410821760035118446815987040634071446317207797338295879693258223031474520244163383451873187288559732281800960678865739318194852711148803850240 + ], + "proved_error_bound": [ + 7503949, + 204963840 + ], + "returned_targets": 20, + "scope": "Actual-reference sparse codec/consumer/return; core is destructive test double, source/consumer scalar macros explicitly priced; no new kappa", + "source": { + "gap": [ + 6255, + 8192 + ], + "identity_holes": [ + 11, + 32, + 53 + ], + "original_entries": 4096, + "parameters": [ + 61, + 3, + 2, + 1, + 8, + 32 + ], + "period": 64, + "periodic_nonzero_coordinates": [ + [ + 0, + 63 + ], + [ + 63, + 0 + ] + ], + "source_sha256": "1ed3587347dc841604ce67dac8090d5a4f403e71a0037fe453835649886a1b7a" + }, + "source_height": 268, + "source_setup": { + "kernel_error_bits": 68, + "maximum_rational_height": 437, + "parameters": [ + 61, + 3, + 2, + 1, + 8, + 32 + ], + "reference_sha256": "1ed3587347dc841604ce67dac8090d5a4f403e71a0037fe453835649886a1b7a", + "stored_entries": 576, + "stored_kernels": 1, + "stored_weights": 61, + "weight_precision": 202 + }, + "transport": { + "finite_alphabet_actions": 3753372, + "retained_finite_alphabet_cells": 21740, + "roles": 30 + } +} diff --git a/research/first-face-reference-join/REVIEW.md b/research/first-face-reference-join/REVIEW.md new file mode 100644 index 0000000000..163902f47e --- /dev/null +++ b/research/first-face-reference-join/REVIEW.md @@ -0,0 +1,64 @@ +# Independent first-face Reference join review + +Separately assigned source-aware OpenAI Codex review for @CubeJerry. Read-only component and composition review; not human or proof-kernel certification. + +## Source pins and verdict + +No blocking composition error found in the tested version. SHA256 pins: + +| Source under research/ | SHA256 | +|---|---| +| first-face-reference-join/join.py | 2631e4c41bd923230a57d723e4f903b1f38b1a3d9772ff87b76d5e1d7f2dc1e8 | +| shrinking-reference-halo/engine.py | 38ca22b213a0291cc7ba821baf513db289c1c3e7c24c579c5eff3349280484b2 | +| shrinking-reference-halo/tensor.py | b3cfe3c18988a89d4a639e8104db7a87f7029d556c74c2e0f60d687ec6be5e80 | +| sparse-halo-tape-transaction/tapes.py | 80b246fafae0adf53af7561e1be59f4374e6294d66bb7a12ef9524b9ef4f2a78 | + +Final receipt revision: `join.py` SHA256 `8a9c2796207a03bda3881494c5b87d8076831a070ca05f9c492b7e6d0c60c1bf`. The numerical path is unchanged. The new receipt explicitly includes encoded plan parameters (including arbitrarily large J at W=0 and gap numerator/denominator) and monotone counters in its control carrier. Reviewed the changed receipt and reran the complete1D spectator fixture successfully against this hash. A zero-band descriptor with J=2^400 produced459metadata bits and517carrier units, confirming J is not bounded accidentally by the halo. Full two-axis replays were against the earlier positive-path hash; B separately reruns both modes of the portable oracle on the final package. + +## All-size compatibility + +For target interval [t,t+m), common saved halo b, and consumer halo b_i<=b, the codec keeps offsets b-b_i<=u0,'signed quotient') + q=abs(n)//d + return -q if n<0 else q + + +def coefficient(x,bits): + x=Fraction(x) + return trunc(x.numerator*(2**bits),x.denominator) + + +def full_grid(matrices,plans,original): + periods=tuple(p.period for p in plans) + need(len(original)==prod(periods),'full-grid cardinality') + current=tuple(original) + for axis,p in enumerate(plans): + n=periods[axis];stride=prod(periods[axis+1:]);block=n*stride + a=tuple(tuple(coefficient(x,p.bits) for x in row) for row in matrices[axis]) + need(len(a)==n and all(len(row)==n for row in a),'dense matrix') + result=[None]*len(current) + for prefix in range(len(current)//block): + base=prefix*block + for remainder in range(stride): + source=tuple(current[base+r*stride+remainder] for r in range(n)) + iterate=((0,0),)*n + for _ in range(p.terms): + following=[] + for row in range(n): + pair=[] + for component in (0,1): + total=source[row][component]*(2**(p.bits-p.normalizer_shift)) + total+=sum(a[row][column]*iterate[column][component] for column in range(n)) + pair.append(trunc(total,2**p.bits)) + following.append(tuple(pair)) + iterate=tuple(following) + for row,value in enumerate(iterate): + result[base+row*stride+remainder]=value + need(all(value is not None for value in result),'all global rows filled') + current=tuple(result) + return current + + +def decode_global(address,periods): + result=[] + for period in reversed(periods): + result.append(address%period);address//=period + need(address==0,'address range') + return tuple(reversed(result)) + + +def sigmag(value,width): + need(type(value) is int and abs(value)<2**(width-1),'word carrier') + return str(int(value<0))+format(abs(value),'0'+str(width-1)+'b') + + +def encoded(pair,width): + return ''.join(sigmag(value,width) for value in pair) + + +def expected_after_core(matrices,plans,original,ell,boundary,spectators=1): + periods=tuple(p.period for p in plans);size=prod(periods) + need(len(original)==spectators*size,'spectator source cardinality') + width=plans[0].data_width;side=2**ell;result=[];targets=0 + for spectator in range(spectators): + source=original[spectator*size:(spectator+1)*size] + rounded=full_grid(matrices,plans,source) + for address,pair in enumerate(source): + point=decode_global(address,periods) + boundary_point=any(x%side=side-boundary for x in point) + if boundary_point: + result.append(encoded(rounded[address],width));targets+=1 + else: + result.append(''.join('1' if bit=='0' else '0' for bit in encoded(pair,width))) + return ''.join(value+'#' for value in result),targets diff --git a/research/first-face-reference-join/independent_review.py b/research/first-face-reference-join/independent_review.py new file mode 100644 index 0000000000..a9c6dbe21a --- /dev/null +++ b/research/first-face-reference-join/independent_review.py @@ -0,0 +1,178 @@ +"""Independent global-grid review of the streamed B/C codec. + +External test fixture/oracle only; no production payload regrouping is used. +Prepared for @CubeJerry with separate source-aware OpenAI Codex assistance. +""" +from fractions import Fraction as Q +from hashlib import sha256 +import importlib.util +import json +from math import prod +from pathlib import Path +import sys +from time import perf_counter + +ROOT = Path(sys.argv[1]).resolve() if len(sys.argv) > 1 else Path(__file__).resolve().parent + + +def load(name, path): + spec = importlib.util.spec_from_file_location(name, path) + module = importlib.util.module_from_spec(spec) + sys.modules[name] = module + spec.loader.exec_module(module) + return module + + +O = load('independent_join_full_grid_oracle', ROOT / 'full_grid_oracle.py') +encoded, expected_after_core, full_grid, need = O.encoded, O.expected_after_core, O.full_grid, O.need +J = load('independent_join_under_review', ROOT / 'join.py') +B, M, T = J.B, J.M, J.T + + +def synthetic_matrix(n, axis): + holes = {4, 11, n - 10} + rows = [[Q(0) for _ in range(n)] for _ in range(n)] + for r in range(n): + for offset, value in ( + (-1, Q(1 if (r + axis) % 2 else -1, 10)), + (0, Q((r + axis) % 3 - 1, 16)), + (1, Q(-1 if (r + axis) % 3 else 1, 11)), + ): + c = (r + offset) % n + if r not in holes and c not in holes: + rows[r][c] = value + need(rows[0][n - 1] and rows[n - 1][0], 'genuine wrap interaction') + return tuple(tuple(row) for row in rows) + + +def original_words(size, bits): + unit = 2 ** max(0, bits - 9) + return tuple((((17 * r + 3) % 201 - 100) * unit, + ((29 * r + 7) % 151 - 75) * unit) for r in range(size)) + + +def forbidden(*args, **kwargs): + raise RuntimeError('production used forbidden diagnostic or allocated a new tape') + + +def fixture(ell, ks, spectator_width, boundary, halo, terms, *, fault=None): + start = perf_counter() + plans = tuple(M.Plan(2 ** (ell + k), 1, 9, j, 1, Q(1, 2), 1) + for k, j in zip(ks, terms)) + need(len(plans) == len(ks), 'complete plan fixture') + matrices = tuple(synthetic_matrix(p.period, axis) for axis, p in enumerate(plans)) + size = (2 ** spectator_width) * prod(p.period for p in plans) + words = original_words(size, plans[0].bits) + if fault == 'negative_zero': + words = ((0, words[0][1]),) + words[1:] + expected, target_count = expected_after_core(matrices, plans, words, ell, boundary, 2 ** spectator_width) + source = ''.join(encoded(pair, plans[0].data_width) + '#' for pair in words) + if fault == 'negative_zero': + source = '1' + source[1:] + coordinate_tape = '0' * spectator_width + '&' + ''.join('@' + '0' * k + '#' + '0' * ell + ';' for k in ks) + width = ell + 2 + transport = B.Program(source, coordinate_tape, + format(2 ** ell, '0' + str(width) + 'b'), + format(boundary, '0' + str(width) + 'b'), + format(halo, '0' + str(width) + 'b')) + transport.gather(); transport.sort(transport.saved) + shape = J.Shape(ell, ks, spectator_width, boundary, halo, 2 * plans[0].data_width) + if fault == 'source_suffix': + B.home(transport.saved) + for _ in range(shape.prefix_width + shape.g * (ell + 2) + shape.coordinate_width - 1): + transport.saved.move(1) + bit = transport.saved.read() + need(bit in '01', 'source suffix mutation site') + transport.saved.write('1' if bit == '0' else '0') + B.home(transport.saved) + saved_before = transport.saved.inspect() + transport.core_complement_test_double() + need(transport.source.inspect() == ''.join('#' if x == '#' else ('1' if x == '0' else '0') for x in source), 'core really destroyed original payloads') + bill = M.Bill() + old_tables = [] + def tables(): + for axis, plan in enumerate(plans): + table, _ = M.prepare_table(plan, lambda r, c, axis=axis: matrices[axis][r][c], 'independent synthetic axis ' + str(axis), bill) + old_tables.append(table) + yield table + archive = T.pack_tables(tables(), bill) + archive_before = archive.tape.snapshot() + pool = T.TensorWorkspace.create(bill) + ids_before = tuple(map(id, pool.roles)) + codec = J.Codec(transport, shape, archive, pool, bill) + old = B.Tape.__init__, B.Tape.inspect, M.Tape.__init__, M.Tape.snapshot + B.Tape.__init__ = B.Tape.inspect = M.Tape.__init__ = M.Tape.snapshot = forbidden + try: + codec.run() + need(old[1](transport.saved) == saved_before, 'saved payloads and keys preserved by codec') + transport.merge_returns() + transport.erase_work() + finally: + B.Tape.__init__, B.Tape.inspect, M.Tape.__init__, M.Tape.snapshot = old + need(transport.final.inspect() == expected, 'whole-grid rounded oracle differs') + need(codec.returned_records == target_count, 'boundary target cardinality') + need(codec.rectangles == (2 ** (spectator_width + sum(ks))) * 2 * len(ks), 'all first-face rectangles consumed exactly once') + need(tuple(map(id, pool.roles)) == ids_before, 'fixed pool identity') + need(all(t.head == 0 and t.live_bits == 0 and not t.readonly and not any(t.snapshot()) for t in pool.roles), 'all eight local roles erased at origin') + need(archive.tape.head == 0 and archive.tape.readonly and archive.tape.snapshot() == archive_before, 'archive preserved at origin') + need(all(t.tape.head == 0 and t.tape.live_bits == 0 and not any(t.tape.snapshot()) for t in old_tables), 'prepared table erasure') + need(all(t is transport.final or t.inspect() == '' for t in transport.roles), 'all nonoutput transport roles erased') + archive.tape.readonly = False; archive.tape.clear() + need(not any(archive.tape.snapshot()), 'archive erasure') + receipt = codec.receipt() + receipt.update(periods=[p.period for p in plans], terms=list(terms), halo=halo, + consumer_halos=[p.halo for p in plans], spectator_width=spectator_width, + source_records=size, checked_returned_bits=target_count * shape.payload_width, + exact_full_grid_match=True, constructors_and_observers_disabled=True, + consumer_bit_actions=bill.reads + bill.writes + bill.moves, + transport_finite_alphabet_actions=sum(t.actions[k] for t in transport.roles for k in ('read', 'write', 'move')), + seconds=round(perf_counter() - start, 3)) + return receipt + + +def actual_reference(): + oracle = load('independent_source_fixture', ROOT / 'oracle.py') + _, raw, h, gap, source_receipt = oracle.source_fixture() + matrix = tuple(tuple(Q(int(r == c)) - h[r][c] for c in range(64)) for r in range(64)) + words = oracle.fixture_words(64, 28) + actual, plan, receipt = J.execute(raw, gap, words) + expected = full_grid((matrix,), (plan,), words) + need(all(actual[row] == expected[row] for row in actual), 'actual reference exact full-grid rounding mismatch') + need(set(actual) == {r for r in range(64) if r % 32 < 5 or r % 32 >= 27}, 'actual target set') + holes = source_receipt['identity_holes'] + need(holes and source_receipt['periodic_nonzero_coordinates'], 'actual holes and wrap') + return dict(actual_reference=True, checked_targets=len(actual), holes=holes, + periodic_nonzeros=len(source_receipt['periodic_nonzero_coordinates']), + exact_full_grid_match=True, codec=receipt['codec']) + + +def main(): + cases = [] + for parameters in ((4, (1,), 1, 2, 1, (2,)), + (4, (1, 1), 0, 2, 1, (2, 1)), + (4, (1, 1), 0, 3, 2, (2, 3))): + result = fixture(*parameters) + cases.append(result) + print(json.dumps(result, sort_keys=True), flush=True) + controls = [] + for fault, message in (('negative_zero', 'noncanonical negative zero'), + ('source_suffix', 'canonical source suffix binds saved offset')): + try: + fixture(4, (1,), 0, 2, 1, (2,), fault=fault) + except ValueError as e: + need(str(e) == message, 'wrong control failure: ' + str(e)) + controls.append(fault) + else: + raise ValueError('mutation escaped: ' + fault) + actual = actual_reference() + print(json.dumps(actual, sort_keys=True), flush=True) + print('PASS_INDEPENDENT_JOIN_FULL_GRID') + print(json.dumps(dict(cases=len(cases), controls=controls, + files={str(path.relative_to(ROOT.parent)): sha256(path.read_bytes()).hexdigest() + for path in (ROOT / 'join.py', ROOT.parent / 'shrinking-reference-halo/engine.py', + ROOT.parent / 'shrinking-reference-halo/tensor.py', + ROOT.parent / 'sparse-halo-tape-transaction/tapes.py')}), sort_keys=True)) + + +if __name__ == '__main__': + main() diff --git a/research/first-face-reference-join/join.py b/research/first-face-reference-join/join.py new file mode 100644 index 0000000000..356d595298 --- /dev/null +++ b/research/first-face-reference-join/join.py @@ -0,0 +1,423 @@ +#!/usr/bin/env python3 +"""Stream first-face transport through a source-bound shrinking halo consumer. + +Actual reads/writes/unit moves are executed across both tape representations. +Sparse control-word arithmetic is an explicit O(w^2) macro tariff, as in the +consumer; this composed program does NOT claim transport's finite-local-only +control boundary. There is no host regrouping of saved payloads. +""" + +from dataclasses import dataclass +from fractions import Fraction as Q +from hashlib import sha256 +import importlib.util +import json +from pathlib import Path +import sys + + +PACKAGE = Path(__file__).resolve().parent +RESEARCH = PACKAGE.parent + + +def load(name, path): + spec = importlib.util.spec_from_file_location(name, path) + module = importlib.util.module_from_spec(spec) + sys.modules[name] = module + spec.loader.exec_module(module) + return module + + +B = load("join_transport", RESEARCH / "sparse-halo-tape-transaction/tapes.py") +M = load("shrinking_halo_engine", RESEARCH / "shrinking-reference-halo/engine.py") +T = load("join_tensor", RESEARCH / "shrinking-reference-halo/tensor.py") +S = load("join_source", RESEARCH / "shrinking-reference-halo/source.py") + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +@dataclass(frozen=True) +class Shape: + ell: int + ks: tuple + spectator_width: int + boundary: int + halo: int + payload_width: int + + def __post_init__(self): + need(self.ell >= 1 and self.ks and all(k >= 1 for k in self.ks), "dyadic shape") + need(0 <= self.halo < self.boundary and self.length > 4 * self.boundary, "first-face geometry") + + @property + def length(self): + return 1 << self.ell + + @property + def g(self): + return len(self.ks) + + @property + def coordinate_width(self): + return self.spectator_width + sum(k + self.ell for k in self.ks) + + @property + def prefix_width(self): + return self.spectator_width + sum(self.ks) + self.g + 1 + + @property + def saved_key_width(self): + return 2 * self.coordinate_width + 3 * self.g + 1 + + +def read_unsigned(tape, width): + """Read each B cell; reconstruct one bounded scalar control field.""" + value = 0 + for _ in range(width): + bit = tape.read() + need(bit in "01", "truncated or nonbinary saved key") + value = 2 * value + (bit == "1") + tape.move(1) + return value + + +def write_unsigned(tape, value, width): + need(0 <= value < 1 << width, "canonical return carrier") + for shift in range(width - 1, -1, -1): + B.append(tape, "1" if (value >> shift) & 1 else "0") + + +def delimiter(tape): + need(tape.read() == "#", "saved field delimiter") + tape.move(1) + + +class Codec: + """One current rectangle, one pending prefix, no host payload container. + + Tuples here contain only encoded geometry/control words, total O(w) bits. + Their arithmetic is priced separately from executed tape primitives. + """ + + def __init__(self, transport, shape, archive, pool, bill, fault=None): + self.transport = transport + self.shape = shape + self.archive = archive + self.pool = pool + self.bill = bill + self.fault = fault + self.prefix = None + self.previous_prefix = -1 + self.copied_records = 0 + self.returned_records = 0 + self.rectangles = 0 + self.cropped_records = 0 + self._fault_used = False + need(len(archive.plans) == shape.g, "one reference plan per active axis") + need(all(p.period == 1 << (k + shape.ell) for p, k in zip(archive.plans, shape.ks)), "shared periodic coordinates") + need(all(p.halo <= shape.halo for p in archive.plans), "saved domain covers every consumer halo") + need(all(2 * p.data_width == shape.payload_width for p in archive.plans), "common exact payload codec") + B.home(transport.saved) + B.end(transport.returns) + + def begin_rectangle(self, prefix): + s = self.shape + need(prefix > self.previous_prefix, "strictly ordered unique rectangle prefixes") + self.prefix = self.previous_prefix = prefix + side = prefix & 1 + onehot = (prefix >> 1) & ((1 << s.g) - 1) + need(onehot != 0 and onehot & (onehot - 1) == 0, "one-hot first face") + face = s.g - onehot.bit_length() + prefix >>= s.g + 1 + core = [0] * s.g + for i in range(s.g - 1, -1, -1): + core[i] = prefix & ((1 << s.ks[i]) - 1) + prefix >>= s.ks[i] + self.spectator = prefix + need(prefix < 1 << s.spectator_width, "spectator prefix width") + targets = [] + for i, c in enumerate(core): + if i < face: + lo, length = s.boundary, s.length - 2 * s.boundary + elif i == face: + lo, length = (0 if side == 0 else s.length - s.boundary), s.boundary + else: + lo, length = 0, s.length + targets.append((c * s.length + lo, length)) + self.targets = tuple(targets) + self.full_lengths = tuple(length + 2 * s.halo for _, length in targets) + self.expected_offsets = [0] * s.g + self.full_count = 1 + for length in self.full_lengths: + self.full_count *= length + self.read_count = self.kept_count = 0 + self.layout = T.Layout.make(self.archive.plans, self.targets) + self.input = self.pool.rectangles[0] + need(all(t.head == 0 and t.live_bits == 0 and not t.readonly for t in self.pool.roles), "one reused blank consumer workspace") + + def advance_offsets(self): + axis = self.shape.g - 1 + while axis >= 0: + self.expected_offsets[axis] += 1 + if self.expected_offsets[axis] < self.full_lengths[axis]: + break + self.expected_offsets[axis] = 0 + axis -= 1 + + def canonical_key(self, coordinates): + key = self.spectator + for x, k in zip(coordinates, self.shape.ks): + axis_width = k + self.shape.ell + key = (key << axis_width) | (x & ((1 << axis_width) - 1)) + return key + + def accept_record(self): + s = self.shape + tape = self.transport.saved + offsets = tuple(read_unsigned(tape, s.ell + 2) for _ in s.ks) + if self.fault == "offset" and not self._fault_used: + offsets = (offsets[0] + 1,) + offsets[1:] + self._fault_used = True + need(self.read_count < self.full_count and offsets == tuple(self.expected_offsets), "complete ordered saved offsets") + source_key = read_unsigned(tape, s.coordinate_width) + coordinates = tuple(lo - s.halo + off for (lo, _), off in zip(self.targets, offsets)) + expected_source = self.canonical_key(coordinates) + if self.fault == "omit_wrap" and not self._fault_used and any(x < 0 for x in coordinates): + expected_source = self.canonical_key(tuple(max(0, x) for x in coordinates)) + self._fault_used = True + need(source_key == expected_source, "canonical source suffix binds saved offset") + delimiter(tape) + delta = tuple(s.halo - p.halo for p in self.archive.plans) + keep = all(d <= off < length - d for off, d, length in zip(offsets, delta, self.full_lengths)) + if keep: + recoded = tuple(off - d for off, d in zip(offsets, delta)) + key = self.layout.key(recoded) + dropping = self.fault == "drop_saved" and not self._fault_used + if dropping: + self._fault_used = True + else: + T.put_unsigned(self.input, key, self.layout.key_width) + else: + dropping = False + for place in range(s.payload_width): + bit = tape.read() + need(bit in "01", "complete saved payload") + tape.move(1) + if self.fault == "payload_magnitude" and place == 2: + bit = "0" if bit == "1" else "1" + self._fault_used = True + if keep and not dropping: + self.input.write(1 if bit == "1" else 0) + self.input.step(1) + delimiter(tape) + self.read_count += 1 + self.copied_records += 1 + if keep and not dropping: + self.kept_count += 1 + else: + self.cropped_records += 1 + self.advance_offsets() + + def finish_rectangle(self): + if self.prefix is None: + return + need(self.read_count == self.full_count, "complete common-halo rectangle") + need(self.kept_count == self.layout.volume, "complete consumer-halo rectangle") + self.input.rewind() + output = T.apply_tensor(self.archive, self.targets, self.input, self.bill, workspace=self.pool) + prior = -1 + for _ in range(output.count): + local_key = T.get_unsigned(output.tape, output.layout.key_width) + need(local_key > prior, "ordered unique consumer targets") + prior = local_key + coordinates = tuple(output.layout.lowers[i] + output.layout.coordinate(local_key, i) for i in range(self.shape.g)) + need(all(lo <= x < lo + length for x, (lo, length) in zip(coordinates, self.targets)), "consumer target-only coordinate") + key = self.canonical_key(coordinates) + if self.fault == "return_key" and not self._fault_used: + key ^= 1 + self._fault_used = True + write_unsigned(self.transport.returns, key, self.shape.coordinate_width) + B.append(self.transport.returns, "#") + # Copy the exact C payload cells. No host decoded numeric word is + # substituted into the production return stream. + for _ in range(self.shape.payload_width): + bit = output.tape.read() + output.tape.step(1) + B.append(self.transport.returns, "1" if bit else "0") + B.append(self.transport.returns, "#") + self.returned_records += 1 + output.tape.clear() + need(all(t.live_bits == 0 and t.head == 0 for t in self.pool.roles), "consumer roles cleaned between rectangles") + self.rectangles += 1 + + def run(self): + tape = self.transport.saved + while tape.read() != "!": + prefix = read_unsigned(tape, self.shape.prefix_width) + if prefix != self.prefix: + self.finish_rectangle() + self.begin_rectangle(prefix) + self.accept_record() + self.finish_rectangle() + self.prefix = None + + def receipt(self): + # Observer-only tariff description. Include the full encoded plan, + # especially arbitrary J when W=0, and monotone history counters. + record_width = self.shape.saved_key_width + self.shape.payload_width + self.shape.coordinate_width + 2 + metadata = [self.shape.ell, self.shape.spectator_width, + self.shape.boundary, self.shape.halo, self.shape.payload_width, + self.shape.g, *self.shape.ks] + for plan in self.archive.plans: + metadata.extend((plan.period, plan.halfwidth, plan.bits, plan.terms, + plan.normalizer_shift, plan.radius, + Q(plan.gap).numerator, Q(plan.gap).denominator)) + metadata_bits = sum(abs(value).bit_length() + 2 for value in metadata) + counter_bits = sum(value.bit_length() + 2 for value in + (self.copied_records, self.returned_records, self.rectangles)) + carrier_units = record_width + metadata_bits + counter_bits + return { + "saved_records": self.copied_records, "returned_records": self.returned_records, + "rectangles": self.rectangles, "cropped_records": self.cropped_records, + "transport_record_width": record_width, + "encoded_plan_descriptor_bits": metadata_bits, + "cumulative_counter_bits": counter_bits, + "control_carrier_units": carrier_units, + "quadratic_codec_tariff_units": (self.copied_records + self.returned_records + self.rectangles) * carrier_units * carrier_units, + "tariff_scope": "The complete encoded control block is O(control_carrier_units); an O(1) multiple of reported quadratic units covers sparse geometry/key macros. These are not measured binary transitions. Numeric source/consumer scalar macros remain separately charged.", + } + + +def sigmag(n, width): + need(abs(n) < 1 << (width - 1), "fixture sign-magnitude carrier") + return str(int(n < 0)) + format(abs(n), f"0{width - 1}b") + + +def decode_word(word, width): + need(len(word) == 2 * width, "observer payload width") + pair = [] + for part in (word[:width], word[width:]): + magnitude = int(part[1:], 2) + need(part[0] == "0" or magnitude, "observer negative zero") + pair.append(-magnitude if part[0] == "1" else magnitude) + return tuple(pair) + + +def literal_totals(transport): + rows = transport.ledger().values() + return {"finite_alphabet_actions": sum(row.get(k, 0) for row in rows for k in ("read", "write", "move")), + "retained_finite_alphabet_cells": sum(row["retained_cells"] for row in transport.ledger().values()), + "roles": len(transport.roles)} + + +def execute(raw, gap, words, *, saved_halo=4, fault=None): + """Execute one complete actual-reference transaction; observers come last.""" + plan = M.Plan(64, 4, 28, 2, 1, gap, 1) + shape = Shape(5, (1,), 0, 5, saved_halo, 2 * plan.data_width) + source = "".join("".join(sigmag(value, plan.data_width) for value in pair) + "#" for pair in words) + transport = B.Program(source, "&@0#00000;", "0100000", "0000101", format(saved_halo, "07b")) + transport.gather() + transport.sort(transport.saved) + saved_before = transport.saved.inspect() # Passive ownership observer. + transport.core_complement_test_double() + bill = M.Bill() + producer = S.make_reference(raw, (61, 3, 2, 1, 8, 32)) + producer.require_narrow_gap() + table, height = M.prepare_table(plan, lambda r, c: S.source_entry(producer, r, c), producer.description_hash, bill) + archive = T.pack_tables((table,), bill) + pool = T.TensorWorkspace.create(bill) + codec = Codec(transport, shape, archive, pool, bill, fault=fault) + codec.run() + need(transport.saved.inspect() == saved_before, "numeric consumer changed original saved copies") + source_setup = S.source_receipt(producer) + S.clear_reference(producer) + archive.tape.readonly = False + archive.tape.clear() + transport.merge_returns() + final = transport.final.inspect().split("#")[:-1] + targets = {r for r in range(64) if r % 32 < 5 or r % 32 >= 27} + actual = {r: decode_word(final[r], plan.data_width) for r in targets} + for row in range(64): + if row not in targets: + original = source.split("#")[row] + need(final[row] == "".join("0" if bit == "1" else "1" for bit in original), "current opaque core interior preserved") + before_erase = literal_totals(transport) + transport.erase_work() + after_erase = literal_totals(transport) + need(after_erase["retained_finite_alphabet_cells"] >= before_erase["retained_finite_alphabet_cells"], "retained B backing after erase") + need(all(t.live_bits == 0 and t.head == 0 for t in pool.roles), "all local consumer roles blank") + c_roles = pool.roles + (archive.tape, table.tape) + receipt = { + "codec": codec.receipt(), "transport": after_erase, + "consumer_binary_actions": bill.reads + bill.writes + bill.moves, + "consumer_bill": bill.record(), + "consumer_retained_binary_cells": sum(t.extent for t in c_roles), + "consumer_data_roles_including_prepared_table": len(c_roles), + "binary_tape_primitive_upper_bound_before_scalar_macros": 10 * after_erase["finite_alphabet_actions"] + bill.reads + bill.writes + bill.moves, + "source_setup": source_setup, "source_height": height, + "final_sha256": sha256(transport.final.inspect().encode()).hexdigest(), + } + return actual, plan, receipt + + +def standalone_consumer(raw, gap, words): + """Independent delivery oracle, explicitly outside the production codec.""" + plan = M.Plan(64, 4, 28, 2, 1, gap, 1) + bill = M.Bill() + source = S.make_reference(raw, (61, 3, 2, 1, 8, 32)) + table, _ = M.prepare_table(plan, lambda r, c: S.source_entry(source, r, c), source.description_hash, bill) + archive = T.pack_tables((table,), bill) + pool = T.TensorWorkspace.create(bill) + answers = {} + for lower in (0, 27, 32, 59): + targets = ((lower, 5),) + layout = T.Layout.make(archive.plans, targets) + external_values = (words[x % 64] for x in range(layout.lowers[0], layout.lowers[0] + layout.lengths[0])) + input_tape = T.rectangle_input(layout, external_values, bill, tape=pool.rectangles[0]) + output = T.apply_tensor(archive, targets, input_tape, bill, workspace=pool) + for _ in range(output.count): + key, value = T.get_record(output.tape, output.layout) + canonical = (output.layout.lowers[0] + output.layout.coordinate(key, 0)) % 64 + need(canonical not in answers, "oracle target uniqueness") + answers[canonical] = value + output.tape.clear() + return answers + + +def main(): + oracle = load("join_independent_source_oracle", PACKAGE / "oracle.py") + _, raw, matrix, gap, source_receipt = oracle.source_fixture() + words = oracle.fixture_words(64, 28) + expected_bits = standalone_consumer(raw, gap, words) + expected_inverse = oracle.exact_inverse_action(matrix, words, 28, 2) + actual, plan, receipt = execute(raw, gap, words) + need(actual == expected_bits, "streamed codec differs bitwise from independent rectangle delivery") + maximum = max(sum(abs(Q(actual[row][j], 1 << plan.bits) - expected_inverse[row][j]) for j in range(2)) for row in actual) + bound = plan.numeric_error + plan.tail_error + need(maximum <= bound, "actual original-reference inverse error") + controls = [] + for fault in ("offset", "omit_wrap", "drop_saved", "return_key"): + try: + execute(raw, gap, words, fault=fault) + except (ValueError, B.Reject): + controls.append(fault) + else: + raise ValueError("joined control failed to reject: " + fault) + wrong, _, _ = execute(raw, gap, words, fault="payload_magnitude") + need(wrong != expected_bits, "wrong saved payload magnitude escaped exact delivery oracle") + controls.append("payload_magnitude_exact_mismatch") + receipt.update(source=source_receipt, returned_targets=len(actual), + exact_delivery_match=True, + maximum_original_inverse_error=[maximum.numerator, maximum.denominator], + proved_error_bound=[bound.numerator, bound.denominator], + controls=controls, + scope="Actual-reference sparse codec/consumer/return; core is destructive test double, source/consumer scalar macros explicitly priced; no new kappa") + print("PASS_FIRST_FACE_REFERENCE_JOIN") + print(json.dumps(receipt, sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/first-face-reference-join/oracle.py b/research/first-face-reference-join/oracle.py new file mode 100644 index 0000000000..5f8049bcbe --- /dev/null +++ b/research/first-face-reference-join/oracle.py @@ -0,0 +1,149 @@ +"""Independent dense original-reference solve for the B/C join fixture. + +Fixture/oracle helper, not a physical tape codec or production cost claim. +Prepared for @CubeJerry with substantial OpenAI Codex assistance. Apache-2.0. +""" +from fractions import Fraction as Q +from hashlib import sha256 +import importlib.util +import json +from pathlib import Path +import sys + +PACKAGE = Path(__file__).resolve().parent.parent / 'shrinking-reference-halo' +PARAMETERS = (61, 3, 2, 1, 8, 32) + + +def load(name, path): + spec = importlib.util.spec_from_file_location(name, path) + module = importlib.util.module_from_spec(spec) + sys.modules[name] = module + spec.loader.exec_module(module) + return module + + +def fixture_words(n, q): + """Actual grid integers, component-l1 norm below1/2 at every row.""" + if q < 9: + raise ValueError('fixture grid') + unit = 1 << (q - 9) + return tuple((((37 * r + 11) % 241 - 120) * unit, + ((53 * r + 7) % 181 - 90) * unit) for r in range(n)) + + +def exact_inverse_action(matrix, words, bits, normalizer): + """Solve original H y=x/a by exact rational elimination, two RHS.""" + n = len(matrix) + if len(words) != n or any(len(row) != n for row in matrix): + raise ValueError('exact solve dimensions') + scale = (1 << bits) * normalizer + augmented = [list(row) + [Q(words[i][j], scale) for j in range(2)] + for i, row in enumerate(matrix)] + for column in range(n): + pivot = next((r for r in range(column, n) if augmented[r][column]), None) + if pivot is None: + raise ValueError('singular original reference') + augmented[column], augmented[pivot] = augmented[pivot], augmented[column] + value = augmented[column][column] + augmented[column] = [entry / value for entry in augmented[column]] + for r in range(column + 1, n): + value = augmented[r][column] + if value: + augmented[r] = [x - value * y + for x, y in zip(augmented[r], augmented[column])] + result = [[Q(0), Q(0)] for _ in range(n)] + for row in range(n - 1, -1, -1): + for part in range(2): + result[row][part] = augmented[row][n + part] - sum( + augmented[row][column] * result[column][part] + for column in range(row + 1, n)) + for row in range(n): + for part in range(2): + if sum(matrix[row][c] * result[c][part] for c in range(n)) != Q(words[row][part], scale): + raise ValueError('exact original-reference solve residual') + return tuple(tuple(pair) for pair in result) + + +def source_fixture(package=PACKAGE): + source = load('join_source_oracle', package / 'source.py') + raw = source.authenticated_inputs(package) + reference = source.make_reference(raw, PARAMETERS) + reference.require_narrow_gap() + n = reference.target_size + matrix = tuple(tuple(reference.entry('narrow', r, c).value for c in range(n)) + for r in range(n)) + E = tuple(tuple(Q(int(r == c)) - matrix[r][c] for c in range(n)) + for r in range(n)) + rho = max(sum(map(abs, row)) for row in E) + gap = Q(int((1 - rho) * (1 << 16)), 1 << 16) + if gap <= Q(1, 2): + raise ValueError('fixture normalizer not funded') + if any(E[r][c] for r in range(n) for c in range(n) + if min((r-c) % n, (c-r) % n) > 4): + raise ValueError('actual reference not W4 banded') + holes = [r for r in range(n) if not any(E[r])] + wraps = [(r, c) for r in range(n) for c in range(n) + if E[r][c] and abs(r-c) > 4] + return source, raw, matrix, gap, dict( + parameters=PARAMETERS, period=n, original_entries=n*n, + source_sha256=reference.description_hash, + gap=[gap.numerator, gap.denominator], identity_holes=holes, + periodic_nonzero_coordinates=wraps) + + +def main(): + source, raw, matrix, gap, receipt = source_fixture() + engine = load('shrinking_halo_engine', PACKAGE / 'engine.py') + tensor = load('join_tensor_oracle', PACKAGE / 'tensor.py') + plan = engine.Plan(64, 4, 28, 2, 1, gap, 1) + words = fixture_words(64, plan.bits) + expected = exact_inverse_action(matrix, words, plan.bits, 2) + bill = engine.Bill() + producer = source.make_reference(raw, PARAMETERS) + table, height = engine.prepare_table( + plan, lambda r,c: source.source_entry(producer,r,c), + producer.description_hash, bill) + archive = tensor.pack_tables((table,), bill) + pool = tensor.TensorWorkspace.create(bill) + actual = {} + rectangles = [] + for lower in (0, 27, 32, 59): + targets = ((lower, 5),) + layout = tensor.Layout.make(archive.plans, targets) + # External fixture load only; B's streamed physical codec replaces it. + data = (words[x % 64] for x in range(layout.lowers[0], + layout.lowers[0] + layout.lengths[0])) + tape = tensor.rectangle_input(layout, data, bill, tape=pool.rectangles[0]) + output = tensor.apply_tensor(archive, targets, tape, bill, workspace=pool) + for _ in range(output.count): + key, pair = tensor.get_record(output.tape, output.layout) + coordinate = (output.layout.lowers[0] + output.layout.coordinate(key,0)) % 64 + if coordinate in actual: + raise ValueError('overlapping first-face return') + actual[coordinate] = pair + output.tape.clear() + rectangles.append(dict(lower=lower, copies=layout.volume, targets=output.count)) + if set(actual) != {r for r in range(64) if r % 32 < 5 or r % 32 >= 27}: + raise ValueError('incomplete first-face return') + maximum = max(sum(abs(Q(actual[r][j],1 << plan.bits) - expected[r][j]) + for j in range(2)) for r in actual) + bound = plan.numeric_error + plan.tail_error + if maximum > bound: + raise ValueError('original inverse error exceeds proved bound') + shifted = max(sum(abs(Q(actual[r][j],1 << plan.bits) - expected[(r+1)%64][j]) + for j in range(2)) for r in actual) + if shifted <= bound: + raise ValueError('wrong-return control not separated') + receipt.update(rectangles=rectangles, checked_targets=len(actual), + maximum_inverse_error=float(maximum), proved_error_bound=float(bound), + wrong_return_error=float(shifted), source_height=height, + setup_source=source.source_receipt(producer), + physical_bit_actions=bill.reads+bill.writes+bill.moves, + program_sha256={name:sha256((PACKAGE/name).read_bytes()).hexdigest() + for name in ('engine.py','tensor.py','source.py')}) + print('PASS_PRIME_REFERENCE64_DIRECT_SOLVE') + print(json.dumps(receipt,sort_keys=True)) + + +if __name__ == '__main__': + main() diff --git a/research/first-face-reference-join/replay_all.py b/research/first-face-reference-join/replay_all.py new file mode 100644 index 0000000000..baaab33974 --- /dev/null +++ b/research/first-face-reference-join/replay_all.py @@ -0,0 +1,19 @@ +#!/usr/bin/env python3 +"""Run the three registered component/composition packages sequentially.""" +from pathlib import Path +import subprocess +import sys + +ROOT = Path(__file__).resolve().parents[2] +PACKAGES = ( + "research/sparse-halo-tape-transaction", + "research/shrinking-reference-halo", + "research/first-face-reference-join", +) + +for package in PACKAGES: + subprocess.run( + [sys.executable, "-B", str(ROOT / "scripts/research_package.py"), + "--package", package], cwd=ROOT, check=True, timeout=1200, + ) +print("PASS_COMPLETE_FIRST_FACE_HALO_PACKAGE") diff --git a/research/shrinking-reference-halo/OVERLAP.json b/research/shrinking-reference-halo/OVERLAP.json new file mode 100644 index 0000000000..aabbd93b28 --- /dev/null +++ b/research/shrinking-reference-halo/OVERLAP.json @@ -0,0 +1,292 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "checked_utc": "2026-11-08 16:11:04 UTC", + "scope": "Original-reference band production and sequential shrinking-domain local tensor consumer; direct degree specialization, generic Horner stability, whole-period host service and outer recovery joins excluded.", + "queries": [ + { + "query": "\"shrinking\" \"halo\"", + "topn": 30, + "results": [] + }, + { + "query": "\"Horner\" \"halo\"", + "topn": 30, + "results": [] + }, + { + "query": "\"periodic\" \"inverse\" \"tape\"", + "topn": 30, + "results": [ + { + "number": 6788, + "title": "Prove the sharp inverse envelope under a column cap (no κ)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/6788" + }, + { + "number": 6542, + "title": "Realize the sparse correction as a reversible nearest-grid map", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/6542" + }, + { + "number": 6438, + "title": "Construct optimal unbiased reversible phase rounding (no κ)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/6438" + }, + { + "number": 6426, + "title": "Prove necessary square-root degree growth for cyclic inverses (no κ)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/6426" + }, + { + "number": 6072, + "title": "Joint denominator-13 decisions need fewer expected fair bits than separate calls", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/6072" + }, + { + "number": 5859, + "title": "Prove the sharp inverse envelope with forbidden diagonals (no new κ)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5859" + }, + { + "number": 5260, + "title": "Replace 119 periodic inverse updates with a certified direct solve", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5260" + }, + { + "number": 5255, + "title": "Prove the sharp graph-support inverse norm envelope", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5255" + }, + { + "number": 5284, + "title": "Prove variable-gap precision and linear storage for cyclic band solves", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5284" + }, + { + "number": 5207, + "title": "Prove exact real Gaussian Schur fill signs for t <= 1/3 (no new κ)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5207" + }, + { + "number": 5216, + "title": "Prove weighted periodic Gaussian power bound and reduce complete inverse to120 terms", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5216" + }, + { + "number": 5159, + "title": "Complete the same-reference periodic rounded inverse service", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5159" + }, + { + "number": 4959, + "title": "Prove routing and Fourier component results with exact checks", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4959" + }, + { + "number": 4870, + "title": "Audit source-driven Gaussian halo copy enumeration (no new kappa)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4870" + }, + { + "number": 4217, + "title": "Audit #4100's HALO locality witness: exact error identity and sharp (2J-1)W radius (no new κ)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4217" + }, + { + "number": 1038, + "title": "Construction: reversible quadratic phases for the dirty stride solver (no new kappa)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1038" + }, + { + "number": 2313, + "title": "Research: execute certified Gaussian resampling through exact integer recovery", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/2313" + }, + { + "number": 486, + "title": "Build binary compression halo boxes with fused streaming and sparse repair", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/486" + }, + { + "number": 929, + "title": "Research: four grouped cyclic inverse calls with one dirty connector (no new kappa)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/929" + } + ] + } + ], + "verified_pr_metadata": [ + { + "number": 1430, + "title": "Audit: quadratic rounding accumulation and linear-error Neumann evaluation (no new kappa)", + "state": "closed", + "merged": true, + "head": "1655c721a1c2aa92f584523afc93a192137cf910", + "base": "410026dc5513b87db92ae98571d1d5984c69a983", + "user": "bbMisk", + "updated_at": "2026-10-14T06:48:19Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1430" + }, + { + "number": 3851, + "title": "Implement normalized Gaussian compression cores on fixed tapes", + "state": "closed", + "merged": true, + "head": "7ab67b4a84d28cd562b9711aa315ca5b47822b37", + "base": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "user": "jmbarrancoml", + "updated_at": "2026-10-20T05:22:44Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/3851" + }, + { + "number": 4100, + "title": "Propose unconditional κ = 0.00173097911567079247276057 via batched CRT", + "state": "closed", + "merged": true, + "head": "337d04939571a637aeab54a0f58f54fde811663a", + "base": "bb4bccbf42844d2801487450727c2f63e10d1d0f", + "user": "1337isnot1337", + "updated_at": "2026-10-20T11:36:03Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4100" + }, + { + "number": 4205, + "title": "Execute rounded Gaussian words against shared finite-core references", + "state": "closed", + "merged": true, + "head": "78c72e563173f3822fcb4efed9ceeccf05630258", + "base": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "user": "jmbarrancoml", + "updated_at": "2026-10-21T19:22:10Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4205" + }, + { + "number": 4253, + "title": "Lower rational FFT and conditioned Toeplitz programs to fixed Hadamard stages", + "state": "closed", + "merged": true, + "head": "ac14c1409c261d64d9856a5a473d8b7f2be8c302", + "base": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "user": "jmbarrancoml", + "updated_at": "2026-10-21T19:24:13Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4253" + }, + { + "number": 4415, + "title": "Answer #4371's open question 1: one coefficient's error path through #4100's transforms carries one factor of T (m = 1), so C = 5 suffices for b >= 13 (no new κ)", + "state": "closed", + "merged": true, + "head": "ebfa9588f5a1ca4c595b3ff837f24917d5dd7caf", + "base": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "user": "pinterbanget", + "updated_at": "2026-10-21T19:27:52Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4415" + }, + { + "number": 4870, + "title": "Audit source-driven Gaussian halo copy enumeration (no new kappa)", + "state": "closed", + "merged": true, + "head": "43a87adb92a25da168073280b206e15b70fbe42c", + "base": "624de9dc66858af0945e5f8a0942488d62280d43", + "user": "codyw912", + "updated_at": "2026-10-23T01:45:56Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4870" + }, + { + "number": 5159, + "title": "Complete the same-reference periodic rounded inverse service", + "state": "closed", + "merged": true, + "head": "ba435a39f69436f2f7ce5cc02f18879c8d8790f5", + "base": "a5df48c55ea806d7952b65acc9c76d878ff09b13", + "user": "JoyboyBrian", + "updated_at": "2026-10-23T11:56:46Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5159" + }, + { + "number": 5216, + "title": "Prove weighted periodic Gaussian power bound and reduce complete inverse to120 terms", + "state": "closed", + "merged": true, + "head": "1ea9efdc1d1d36757a5491bf7fdaa93597dcea67", + "base": "ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c", + "user": "JoyboyBrian", + "updated_at": "2026-10-23T13:09:35Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5216" + }, + { + "number": 5260, + "title": "Replace 119 periodic inverse updates with a certified direct solve", + "state": "closed", + "merged": true, + "head": "65cdd6b36e002ce9d13bd96dbc504da90f77f2c9", + "base": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "user": "aliromman", + "updated_at": "2026-10-23T18:37:53Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5260" + }, + { + "number": 5284, + "title": "Prove variable-gap precision and linear storage for cyclic band solves", + "state": "closed", + "merged": true, + "head": "72269696a9c5ae5b1c0b469afdd3db08080635cf", + "base": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "user": "aliromman", + "updated_at": "2026-10-23T18:37:53Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5284" + }, + { + "number": 5325, + "title": "Join Tensor error bounds through compression and final restoration", + "state": "closed", + "merged": true, + "head": "bea42af24ee9850949a4b48d329a7dc85de72b11", + "base": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "user": "aliromman", + "updated_at": "2026-10-23T18:37:52Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5325" + }, + { + "number": 5986, + "title": "Reduce Gaussian inverse locality degree from p^42 to p^22 (no new κ)", + "state": "closed", + "merged": true, + "head": "31bbc7b22ea697437660a0af4c006e114b90710b", + "base": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "user": "petalas", + "updated_at": "2026-10-28T00:24:32Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5986" + }, + { + "number": 6490, + "title": "Reduce Horner oracle precision volume with increasing grids (no κ)", + "state": "open", + "merged": false, + "head": "4307d3a0cb8921b58ec2f229fdad41db25849932", + "base": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "user": "petalas", + "updated_at": "2026-11-03T01:01:48Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/6490" + }, + { + "number": 6880, + "title": "Prove a rounded finite-core and sparse-halo composition bound (no new κ)", + "state": "open", + "merged": false, + "head": "e212af981b49c299de515f8c23dfb0e5b73e2e95", + "base": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "user": "CubeJerry", + "updated_at": "2026-11-08T15:01:00Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/6880" + } + ], + "coverage_limits": [ + "Focused live title/body queries and cited predecessor source packages; not all historical diffs or unpublished work.", + "Search results omit status fields; cited status/head metadata were separately fetched by PR endpoint.", + "Lead surveyed canonical research-directory metadata and broader dependency landscape. This worker did not repeat a repository-wide archive survey.", + "Discussion posting unavailable to the lead; scope is recorded in the lead's local allocation manifest. No public advance reservation is asserted." + ] +} diff --git a/research/shrinking-reference-halo/PROOF.md b/research/shrinking-reference-halo/PROOF.md new file mode 100644 index 0000000000..c47fc7013b --- /dev/null +++ b/research/shrinking-reference-halo/PROOF.md @@ -0,0 +1,578 @@ +# A source-bound shrinking-domain Gaussian halo consumer + +Prepared for @CubeJerry with substantial OpenAI Codex assistance. Apache-2.0. + +## 1. Result, scope and predecessor boundary + +This is a constructive local tensor result under a certified fixed-reference +row gap. It supplies the numerical consumer and its sequential data/page +protocol on one saved sparse rectangle. It does not prove the complete outer +Gaussian construction, admit the selected suppliers, or change kappa. + +The fixed-source Horner identity is classical. In this repository, #1430 already +uses it to control rounding under a fixed approximate oracle with norm at most +0.42; #6490 allocates precision across that oracle's calls. #5159 implements a +rounded whole-period action on one actual rational Gaussian Reference, with +coefficient error, data error and storage charged at a host-array interface. +#5216 improves its tail and #5260/#5284 supply direct-solve alternatives, also +without a complete physical sparse caller. #3851 implements a different +principal-core/Schur interface, with its own source parameters and gap. + +#6880 already proves direct row-gap locality, normalized nonlinear core/halo +composition, inward-rounded polynomial rows, and the specialization J=16p^4. +Those are not new claims here. That package leaves production of the global +polynomial coefficient pages and their physical access unpriced. #4100's HALO +argument permits a polynomial-time local correction but does not implement +the present recurrence, shrinking domains, or table/line schedule. + +The contribution is an explicit replacement for that remaining polynomial-row +interface: store only the original reference band, shrink the dependency +interval after every iteration, expose axes by sorting only sparse records, +reuse one page across every spectator line, and use eight fixed local tape +roles plus one protected coefficient archive. Its quantified all-size bill +includes reference production, repeated full archive scans, encoded controls, +scalar arithmetic, copies, head returns and retained blank backing. A full-axis +scan is retained explicitly in the generic theorem; it is absorbed only in the +specified balanced growing-group regime. + +The universal argument below is a written proof. The executable fixtures +corroborate it; neither finite traces nor separate AI review are formal-kernel +or independent human acceptance. + +## 2. Exact input contract + +For axis i, let H_i=I-E_i be a real rational matrix of period N_i. Let W_i be a +nonnegative integer with 2W_i=1, and choose an integer u_i>=0 with +a_i=2^u_i and a_i delta_i>=1. Choose one data/coefficient grid h=2^-q with +q>=max_i u_i. The incoming complex array has components on this grid and + + ||x||_* = max_r (|Re x_r| + |Im x_r|) <= R, + +where the executable interface takes an integer R>=1. A complex-modulus unit +disk input fits this interface with R=2. Every actual incoming line is checked +against its stated bound. The theorem does not infer an outer caller's input +radius merely from an exact ideal map. + +An output interval T_i=[t_i,t_i+m_i) is interpreted on the integer lift of the +physical circle. Set b_i=(J_i-1)W_i and + + D_i = [t_i-b_i, t_i+m_i+b_i), d_i = m_i+2b_i. + +Require d_i=u_i is required. The absolute component-l1 sum +of any partial accumulator is at most R*2^(2q): it is bounded by the source +term plus a partial sum of coefficient absolute values times R. A signed +carrier of 2q+ceil(log2(R+1))+2 bits is ample. Coefficient and data carriers +have q+O(log(R+1)) bits. The code checks the actual partial accumulator bound, +not just the final rounded result. + +Write y_k=(1/a_i) sum_(j=0)^(k-1) E_i^j x. Its norm is also at most R. +Subtract its recurrence from (1), evaluating the perturbation at the *actual* +z_k. If e_k=||z_k-y_k||_*, then + + e_(k+1) <= rho_i e_k + s_i h R + 2h, e_0=0. + +Therefore + + ||z_(J_i) - P_i x/a_i||_* <= nu_i, + P_i=sum_(j=0)^(J_i-1) E_i^j, + nu_i=(s_i R+2) h/delta_i. (2) + +The sharper finite geometric factor could be retained; (2) is sufficient. +The exact normalized polynomial and inverse both have induced norm at most +one, and the tail is + + ||P_i/a_i-H_i^-1/a_i||_infinity + <= tau_i = rho_i^J_i/(a_i delta_i). (3) + +These numerical estimates retain standard Neumann/Horner reasoning and the +whole-period predecessor's coefficient/data accounting. Their role here is +to certify the actual finite-precision sequential local program. + +## 4. The shrinking domain is exactly sufficient + +Define + + D_i^(k) = T_i + [-(J_i-k)W_i, (J_i-k)W_i], + 1 <= k <= J_i, + +where the notation denotes the corresponding half-open integer interval. +Compute z_1=Q_q(x/a_i) on D_i^(1)=D_i. To compute z_(k+1) on D_i^(k+1), +read its source x there and every previous neighbor within distance W_i. +Those neighbors lie in D_i^(k). The global coefficient for the corresponding +canonical row and offset is obtained from the already fixed band page. + +Induction on k now proves equality, bit for bit, with the restriction of the +full-period rounded recurrence (1). This statement does not require linearity +of rounding. It follows because each local update sees exactly the same +coefficient numerators, source numerator and prior neighbor numerators as the +global update. At k=J_i the returned interval is precisely T_i. + +This is not the polynomial of E restricted to T_i or to the eventual returned +rectangle. Such a restriction loses paths that leave and reenter it. The +program retains D_i^(k) until its use at the next step, then discards only the +two already unnecessary boundary strips. The initial padding is exactly the +maximum dependency distance of the degree J_i-1 polynomial. + +For h_axes axes processed in order, after completing axis i the maintained +rectangle is + + S_i = T_0 x ... x T_i x D_(i+1) x ... x D_(h_axes-1). (4) + +At the next axis, every needed neighbor differs only in that next coordinate. +The earlier coordinates therefore need no padding after their axes have +completed. The later coordinates must retain their complete original D_j. +Applying the one-axis induction to every spectator line proves exact agreement +with the corresponding restriction of the full-period nonlinear tensor +recurrence. That full-period recurrence is an analysis device, not an executed +dense algorithm. + +Compare this global rounded composition first with the product of P_i/a_i. +Each local error bound (2) holds at the actual incoming state, which has radius +R. Each exact P_i/a_i is a contraction. Telescoping against these exact maps +gives numerical error at most sum_i nu_i. Telescoping (3), using contraction +of both factors, then gives the complete inverse-tensor guarantee + + ||returned - [product_i (H_i^-1/a_i)] x |_T||_* + <= sum_i nu_i + R sum_i tau_i. (5) + +No factor depending on the global tensor dimension occurs in (5). No +assumption that the rounded program itself is additive or nonexpansive is +made. The proof applies to every global extension of the saved input with +radius at most R, since all omitted inverse dependence is explicitly funded +by (3). + +## 5. One sequential line and its exact invoice + +The global band table is ordered by canonical row, then by offsets -W_i to +W_i. A local page is ordered by lifted row, then by the same offsets. If D_i +wraps, one complete table scan emits its final-period part, and a second +complete scan emits its initial-period part. All skipped coefficients are +read and both complete scans return to the origin. No constant-cost global +row query, arbitrary seek or hidden page cache is assumed. + +`apply_line` uses the immutable source, immutable page, and two owned iterate +tapes. It forms z_1 by one source scan. During an update, a row reads the +2W_i+1 adjacent previous records in increasing order. Before the next output +row, the previous-state head walks back exactly 2W_i records. Thus the next +window advances by one. At the final row the head is at the end of the prior +live body. The source and page also make explicit forward skips and complete +returns. Before reusing an iterate role, the program clears its complete +previous live body, including all rows that existed before the next shrink. +It never substitutes the smaller newly produced length for that old length. + +Each role maintains a live-body length and a separate historical extent. All +cells at or beyond the live length are already zero. The invariant is true +on a fresh blank tape. A write extends the live length through its position; +the formerly unoccupied gap and remaining suffix were already blank. Clearing +the complete previous live body makes the live length zero and leaves the +invariant true. Thus a historical blank suffix remains paid in space without +being rescanned at every later reuse. Program transitions use this invariant +and encoded lengths, not an uncharged host inspection of the backing array. + +This distinction is necessary for the claimed tariff. A long L-sized line +followed by an A-sized face line must not pay L cells per clear on each short +line. That alternative adds a factor L/A and can consume the sparse volume +saving. The verifier executes a long-line/short-face/long-line history on the +same roles, checks actual blank suffixes independently, and compares an +executed counterfactual that clears the historical extent on every reuse. + +For target length m, the live lengths after k terms are +n_k=m+2(J_i-k)W_i. A complex line performs exactly + + 2s_i sum_(k=2)^J_i n_k + = 2s_i[(J_i-1)m + W_i(J_i-1)(J_i-2)] + +integer products and the same number of accumulator additions. It performs + + 2 sum_(k=1)^J_i n_k = 2[J_i m + W_i J_i(J_i-1)] + +component roundings. The fixed-source shifts, reads, output writes, +initialization, complete old-live-body erasure and all head motion are separately +counted. J_i=1 and W_i=0 are allowed by these formulas. + +Let w bound the numerical carriers and the entire encoded descriptor/control +block, including signed absolute origins, lengths, periods, iteration counts, +loop counters and local keys. A decoded scalar integer addition, shift, +comparison, multiplication or division is implemented by ordinary fixed-tape +binary arithmetic. Schoolbook multiplication/division costs O(w^2). Even +charging O(w^2) for each scalar encode/decode, rather than treating a host +integer shift as unit time, a line costs + + O(J_i d_i s_i w^2) bit operations. (6) + +Its source plus two iterate roles occupy at most 6d_i times the component +carrier width; its page occupies d_i s_i(q+2) bits. Add O(w) scalar/control +storage and the separately retained global archive. A returned output occupies +one of those two iterate roles, so it is not omitted from the space count. +Unused suffixes can remain allocated but are blank and are included in this +bound. `maximum_single_tape_extent` is only the largest individual tape; +the verifier separately sums every retained local role. + +The Python program executes every binary tape read/write and one-cell head +move. Its integer operations implement scalar-macro semantics; its elapsed +Python time is not asserted to equal the asymptotic bit bound (6). The proof +supplies the fixed-tape implementation and cost of those scalar macros. + +## 6. Complete local rectangle schedule and generic cost + +The payload has a fixed-width key comprising the nonnegative offsets within +the original D_i, followed by signed fixed-width real/imaginary numerators. +Let K=sum_i max(1,ceil(log2 d_i)); unused field encodings are not valid +coordinates. An initial lexicographic stream is encoded in one charged pass. +The same fixed key fields remain valid after an axis shrinks. Return converts +offsets back to lifted coordinates; the outer caller may reduce them modulo +the periods in another explicitly charged pass. + +To expose axis i, perform stable least-significant-bit distribution into two +fixed buckets. Process the bits of field i first, then the bits of the other +fields in reverse natural order. Concatenation of the zero and one buckets +after each pass leaves the other fields in natural lexicographic order, with +axis i innermost. Each pass scans and clears the entire live owned sparse body +and both live buckets; already blank retained tails obey the same invariant. +It never scans the dense +global data array. There are exactly K passes per axis. The conservative +scalar encode/decode convention above charges O(K C_i w^2) bit work for a +body with C_i records, rather than hiding key operations in a unit-cost word. + +After exposure, each complete spectator line is copied into one reusable +immutable line role, evaluated by Section 5, and emitted with target-only +keys into the alternate rectangle role. The local band page is produced +once per rectangle/axis, before its first line, and reused across all of those +lines. Only after the entire axis output is complete is the previous rectangle +cleared. Equation (4) gives the next live shape. After the final axis, natural +lexicographic order is already restored. + +There are eight local roles: current/next rectangles, two radix buckets, +one line source, two iterates and one local page. Their count is independent +of J_i, the number of lines, rectangles and axes. `tensor.py` creates the pool +once in `TensorWorkspace`, passes the same iterate roles to every line, and +clears every nonreturn role. After the caller consumes and clears the returned +rectangle, the same workspace accepts the next rectangle through the explicit +`rectangle_input(..., tape=...)` and `apply_tensor(..., workspace=...)` interfaces. +The verifier seals all tape constructors across a long/short/long sequence of +complete rectangle calls and checks that the identical eight role objects +return blank. Across such a history, space is the sum of the eight historical +extents, bounded by the largest admitted body for each role; time depends on +the currently occupied lengths, by the invariant in Section 5. +The global tables are concatenated in one protected archive; `pack_tables` +consumes and clears one temporary table before requesting the next from its +generator. Thus a growing number of axes does not require a growing number of +physical tapes. Descriptor tuples in the Python reference represent one +encoded control block. Scan/selection costs on that block are bounded by w +and included in the w^2 allowances; indexed metadata is not free access to +payload or coefficients. + +Let C=product_i d_i and G=sum_i N_i s_i be the total band coefficient count in +the current group's archive. The executable scans the *entire concatenated +archive* once or twice for each axis page, including other axes' coefficients. +If T_ref denotes reference production and quantization, the complete generic +local bill is + + T_ref + O(w^2 [h_axes G + C sum_i (J_i s_i + K + 1)]). (7) + +Input codec, all source/data/page transfers, output copying, sorting, +arithmetic, head returns and erasure are included. T_ref is a separately +amortized group setup if the archive is reused for several rectangles. The +term h_axes G remains present for each rectangle; it is not automatically a +local polynomial merely because d_i is polynomial. + +With eight local roles, their total retained extent is + + O(Cw + max_i d_i s_i q), + +plus O(w) control/scalar storage and the protected archive G(q+2). At most a +constant number of old/new rectangle bodies coexist. The producer's setup +scratch is additional, as quantified next. The code's physical action counts +and full retained extents are evidence for this schedule, not a byte-exact +claim about Python's object allocator or secure memory zeroization. + +## 7. Binding to the actual retained Gaussian entry producer + +The live source is `research/rational-unitary-fft/gaussian_reference.py` at +the exact base in SOURCES.json. Its original geometry and proof are retained +in `RAW-GAUSSIAN-PROOF.md`. `source.py` authenticates all source bytes before +execution. It rebinds the original import dependencies and extracts only the +unchanged `rational`/`load_intervals` helpers from `gaussian.py`, avoiding an +unused full-circuit compiler import. It changes no executed numerical function +body. `Reference.for_cap` is not called by this adapter; its use would require +the larger compiler dependency closure. + +For original source size S, excess K0, target period N=S+K0, and +theta=K0/S, the source fixes + + c_j=floor(theta*j+1/2), q_j=j+c_j, beta_j=theta*j-c_j. + +The narrow reference has identity holes and zero selected/hole cross entries. +For a source halfwidth w0 with 2w0=2w0+2 +therefore contains every nonzero entry of E=I-H. Our table loops over every +canonical target row and every physical offset, calls that exact entry rule, +checks the original row mass and truncates the resulting rational toward zero. +Holes and genuine period crossings use the same rule as all other entries. + +The source's relative-weight construction avoids silently replacing tiny +positive weights by zero. With entry precision b_e its weight precision is + + P_weight=ceil(2 alpha^2/theta)+b_e+7, + +and its kernel precision adds O(alpha^2 w0). Under the retained caller's +theta in [1/(4p^2),1/p^2], alpha^2=O(log p), b_e=O(p), and W= 1/(16p^2), W_i4A, b_i<=A and N_i>=2L. Then every first-face expanded side has +length at most L+2b_i=F_in, max_i u_i, where F_in is the actual incoming grid, and +fund, for a desired local group allowance 2^-Cp, + + q >= Cp + ceil(log2(4 h_axes max_i[(s_i R+2)/delta_i])). (9) + +This makes sum_i nu_i<=2^-Cp/4. Since rho_i^J_i<=exp(-p^2), the tail term in +(5) is also below 2^-Cp/4 eventually for fixed C and polynomial R. The chosen +q is O(p) whenever F_in=O(p) and R is polynomial. No exact incoming bits are +discarded: q is at least F_in. One may choose a_i between delta_i^-1 and +2delta_i^-1, or use the caller's larger existing dyadic p^100 normalization. +The same normalizer must be used by any core route with which these outputs +are spliced. The total outer compensation is O(d log p)=o(p), and must be +paid/restored by the existing caller; it is not canceled for free here. + +For completeness, implement the source's “balanced groups” explicitly. With +d>=g>=2, put m=ceil(d/g) and split the d axes into m groups of sizes +floor(d/m) or ceil(d/m). Every group has at most g axes and at least +floor(g/2) axes. Thus there is no exceptional final one-axis remainder to +which a growing-group amortization has been incorrectly applied. + +The source has ell=Theta(p^(1-epsilon)), axis periods at most 2^ell, +d=Theta(p^epsilon), and g=Theta(p^beta), with beta>1-epsilon. A first-face +rectangle has at least h_axes-1 long sides of length L-2A, so its volume C +satisfies + + log2 C >= (h_axes-1) log2(L-2A). + +Because h_axes=Omega(p^beta), the right side dominates +ell + c log p for every fixed c. Therefore even a complete concatenated +axis archive scan, of size 2^O(ell) poly(p), repeated once or twice per local +axis, is eventually bounded by C. This proves absorption of the repeated +scan term in (7). It is stronger than simply saying local setup is polynomial +in p. For arbitrary fixed h_axes, or any failed finite comparison, retain +the full h_axes G w^2 term. The effective comparison can be made with integer +bit lengths before adopting the asymptotic branch. + +Offline production across all d axes costs +d*2^O(ell)*poly(p)=2^o(p)=o(V), using (8), where V=T_total*p is the source's +full bit volume. This is a different charge from repeated per-rectangle +archive scans. Preparing each group's archive once as it is reached gives +the same summed bound and uses a constant physical tape pool. + +In the actual balanced regime, all control/coordinate fields fit O(p) bits: +h_axes log L=o(p), h_axes ell=o(p), and the source uses beta+1-epsilon<1. +Numerical carriers have O(p) bits by (9). Thus w=O(p), J_i=O(p^4), s_i=O(p), +and K=O(p). Equation (7) gives the deliberately conservative local bound + + O(C h_axes p^7) bit work, plus the explicit offline setup. (10) + +There are O(h_axes A/L) copied records per original full-array record in a +group. Summing (10) over all rectangles and O(d/g) balanced groups gives + + O(V d g A p^6 / L) (11) + +for this numerical consumer, with sparse layout, pages and arithmetic +included. It is inside the older allowance O(V d g A^3/L polylog p). +With A=p^48 and L>=p^400 its exponent is at most +epsilon+beta+54-400<0. The dense gather/return scans remain the separate +O(V d/g) row of the outer ledger; this package does not invoke a dense scan +per numerical axis. The existing first-face copy producer and unique-return +transaction must provide those operations. Formula (11) is not a new kappa +claim; it establishes that this explicit consumer does not exhaust the +already reserved conservative halo budget. + +## 9. Evidence, limits and remaining composition + +The verifier uses exact integers and Fractions for every acceptance decision. +It checks 32 signed nonstationary cyclic-band lines, including identity holes, +negative/positive coefficients and wrapping targets. Its independent dense +polynomial evaluator forms successive powers and their sum. A second global +rounded evaluator checks exact bit equality, while the written proof supplies +the universal quantifiers. + +Two synthetic tensors execute the complete sparse tape schedule in two and +three dimensions. A second history executes three differently shaped rectangles +with the same eight roles and no new tape construction permitted. The actual source fixture is +Reference(32,8,2,1,8,32), with period 40 and eight identity holes. All 1,600 +original entries are checked, including omitted entries and genuine wraps. +Three local lines and a 756-record two-axis saved rectangle are executed; +the latter returns exactly twelve target records. Its source-certified gap, +numerical bound, tail bound, complete products/roundings, page scan count, +radix count and summed retained extents are recorded in RESULT.json. + +These finite source parameters are legal for the retained Reference API but +are not an execution of the eventual outer production regime. The all-size +parameter substitution rests on Sections 7–8 and the explicitly retained +source hypotheses, not on extrapolation from forty rows. + +Controls reject wrong normalization, insufficient source grid, ambiguous band +offsets, missing row gap, oversized actual data, aliased page intervals, +incorrect dependency crops and negative-zero records. Actual consumer code +mutations exercise wrong recurrence sign, wrong neighbor rewind and omitted +erasure, wrong sparse-axis exposure, stale axis pages and shifted return keys; +a dropped actual periodic branch changes the returned source answer. The +long-short-long history and counterfactual high-water tariff guard the +physical reuse obligation that is invisible to a numerical-only comparison. +Normal and optimized replay do not rely on Python assertions. + +Two additional checks were independently developed during adversarial review. +Neither imports verify.py, the dense-power oracle, or its expected outputs. +The first solves four rows of the original forty-by-forty H inverse by exact +rational elimination of H^T. Every computed row satisfies its exact inverse +equations. Tensoring these rows then gives an independent original-inverse +answer at four two-axis targets, against which the physical consumer has +maximum component-l1 error below 5.252e-9, within (5)'s 8.213e-8 allowance. +Its nested target has identical returned bits, all eight tape roles are reused +with constructors sealed, and the reference archive stays unchanged. A shifted +target control has error greater than 0.109. + +The second executes every singleton output of one forty-row input, computes +the original-reference residual r=x/a-Hy, and uses +||H^-1||_infinity<=1/delta to certify ||y-H^-1 x/a||<=||r||/delta. +This gives error below 7.667e-9 without using a polynomial oracle. For a +cyclically shifted returned vector, ||r||/||H||_infinity gives an error lower +bound greater than 0.543. Every acceptance decision is exact rational +arithmetic. Both scripts run normally and with assertions disabled as +registered checks; their decimal output is only a readable summary. +The independent method and implementation provenance concern a separate AI +reviewer in the same research effort, not external mathematical acceptance. + +No arbitrary native implementation, complete finite-core adoption, dense +first-face copy/return protocol, broad Gaussian map, all-depth supplier, +outer tensor/CRT algorithm or exact integer-recovery theorem is established +here. The source H, its certified row gap and ideal-Gaussian comparison remain +named dependencies. #5325 and #4415 already address other error-join/suffix +questions; their results are not duplicated or silently assumed compatible +with a different rounded reference. A complete join must verify that the +core, this consumer, normalizers and the eventual outer recovery use the same +source interface and actual grid/radius contracts. All five selected +framework assumptions remain in force. No new kappa. diff --git a/research/shrinking-reference-halo/README.md b/research/shrinking-reference-halo/README.md new file mode 100644 index 0000000000..e9809decb1 --- /dev/null +++ b/research/shrinking-reference-halo/README.md @@ -0,0 +1,201 @@ +# Compute sparse Gaussian inverse halos from the original band + +**Scoped constructive result, with a written all-size proof and exact finite +corroboration. No new κ.** + +This package replaces an unpriced global polynomial-row oracle with an +explicit local numerical consumer. It evaluates the normalized inverse +polynomial from the original rational reference band, shrinking the saved +dependency interval after each step. The full local tensor program includes +sparse axis exposure, absolute-coordinate coefficient pages, actual rounding, +immutable fixed-source lines, physical head returns and cleanup. + +The contribution is the source-bound sequential interface and complete bill. +The Neumann/Horner identities, the direct row-gap locality degree, and generic +rounded core/halo composition were already available. The comparison below +is part of the novelty boundary, not a claim of general literature priority. + +## Technical result + +For real cyclic band matrices `H_i=I-E_i` with row gap `delta_i>0`, bandwidth +`W_i`, and a shared q grid, choose dyadic `a_i` with `a_i delta_i>=1`. The +program uses `J_i` fixed-source updates and a saved halo of +`b_i=(J_i-1)W_i`. It returns the target rectangle with error at most + + sum_i [(2W_i+1)R+2] * 2^-q/delta_i + + R sum_i (1-delta_i)^J_i/(a_i delta_i). + +Every actual intermediate remains on the same grid and within the original +component-l1 radius `R`. Each source line is preserved through its complete +update sequence. The program never forms the dense polynomial coefficient +rows, and it never assumes translation invariance of the reference entries. + +The numerical tensor uses eight reusable local tape roles and one protected +concatenated reference archive. Each local page takes at most two **complete +archive scans per rectangle/axis**, and is reused across all spectator lines. +Sorting touches only the sparse saved rectangle. A live-body/blank-suffix +invariant prevents repeated erasure of old large buffers from introducing an +unfunded `L/A` factor on a later short face. + +For copied volume `C`, key width `K`, arithmetic/control width `w`, and +archive coefficient count `G`, the complete generic bit bill is + + T_reference + O(w^2 [h_axes G + C sum_i(J_i(2W_i+1)+K+1)]). + +The full archive term is explicit. In the exact balanced growing-group regime +of the pinned #4100 route, a rectangle's many long sides absorb the repeated +archive scans. The original source producer has separately charged +`d*2^O(ell)*poly(p)=2^o(p)` setup. The resulting numerical consumer costs +`O(V d g A p^6/L)`, inside the route's older conservative halo allowance. +This substitution does not admit that archived outer proof or change the +selected conditional frontier. + +The complete definitions, no-alias domain, fixed-role implementation, +coefficient producer, scalar arithmetic and production substitution are in +[PROOF.md](PROOF.md). Exact base and source hashes are in +[SOURCES.json](SOURCES.json). + +## What was already proved + +| Source | Existing result | Present distinction | +|---|---|---| +| #1430 and #6490 | Stable fixed-source Horner evaluation and its oracle precision allocation | Original reference entries, local shrinking domains and sequential producer/consumer cost | +| #5159 and #5216 | Complete rounded whole-period service on one rational Gaussian Reference | Sparse local tensor, variable certified gaps, fixed tape roles and production-group substitution | +| #5260 and #5284 | Host-array direct solves and variable-gap cyclic-band precision | Different iterative mechanism; includes the sparse physical page/layout interface | +| #3851 | Physical normalized principal-window compression core | Complements that core; does not reprove its Schur/q-convolution mechanism or use its different gap as this caller's gap | +| #6880 | Direct row-gap polynomial, `J=16p^4`, inward-rounded polynomial rows and nonlinear core/halo composition | Eliminates the polynomial-row oracle using the original band and prices its production/access | +| #4870 | First-face source-copy enumeration | Receives one completed saved rectangle; dense-source copy generation and final unique return remain outside this consumer | + +#5325's tensor error join, #4415's outer suffix accounting, and #4205/#4253's +finite-core circuit theorem are not claimed as new work. A future integration +must check their source/reference versions and actual grids before composing +them with this consumer. + +## Exact evidence and reproduction + +From the repository root, with CPython 3.12 and the standard library: + +```sh +python3 -I -B research/shrinking-reference-halo/verify.py +``` + +Expected marker: `PASS_SHRINKING_REFERENCE_HALO`, with 32 finite lines, +40 Gaussian rows, 1,600 original source entries, 17 rejection controls, +and `no_new_kappa: true`. + +The registered replay runs the author verifier and two separately developed +mathematical checks, each in normal and optimized Python: + +```sh +python3 -B scripts/research_package.py --package research/shrinking-reference-halo +``` + +[RESULT.json](RESULT.json) is generated by the verifier and required by normal +read-only replay. It records: + +- Thirty-two signed, nonstationary cyclic-band lines and ninety-six returned + target coordinates, with exact dense-polynomial and full rounded-period + comparators. +- Complete two- and three-axis synthetic tensor executions, followed by a + long/short/long rectangle history with all tape constructors disabled. +- The actual retained `Reference(32,8,2,1,8,32)`, including every one of its + 1,600 entries, all eight identity holes, and genuine across-period entries. +- Three actual-reference lines and a two-axis, 756-record saved rectangle + returning twelve target records, with the complete product, rounding, + archive-scan, radix, head-action and retained-space counts. +- Seventeen explicit rejection/code-mutation controls. Separate executed + comparisons detect dropping the actual periodic branch and the unfavorable + high-water-clearing tariff, even though the latter leaves numerical answers + unchanged. + +The matrix-power oracle forms successive exact powers and their sum; it does +not import the numerical recurrence's implementation. The global rounded +comparator additionally checks bit-for-bit locality. + +The separately developed [independent_inverse.py](independent_inverse.py) +solves four rows of the **original rational inverse** by exact elimination, +checks their exact matrix residuals, and uses those rows to evaluate the +two-axis inverse independently of the polynomial recurrence. The physical +consumer's four outputs have maximum error below `5.252e-9`, within the +proved `8.213e-8` allowance. A second nested target returns identical bits, +reuses the same eight roles with tape creation disabled, and preserves the +archive. A wrong-target control produces error greater than `0.109`. + +[independent_residual.py](independent_residual.py) runs all forty physical +singleton outputs and bounds their inverse error directly from the original +matrix residual and its exact row gap. The certified error is below +`7.667e-9`, while a cyclically misreturned output has error greater than +`0.543`. Neither check imports the author verifier or its expected output. +Their expected markers are `PASS_LEAD_EXACT_TENSOR_INVERSE` and +`PASS_LEAD_ORIGINAL_REFERENCE_RESIDUAL`. + +These checks were developed by a separate AI reviewer within this contribution, +using different mathematical mechanisms. All acceptance comparisons use +exact rational arithmetic; displayed decimal summaries are diagnostic. The +all-size claims rest on the written proof. No external human or formal-kernel +acceptance is asserted. + +## Scope and limitations + +The source-bound forty-row example is a legal finite Reference fixture, not +an execution of the asymptotic outer production parameters. Its all-input +same-reference numerical error is funded below `2^-20` per axis, while the +source's ideal-Gaussian perturbation and global gap proof remain inherited. +The generic theorem explicitly requires zero outside the stated cyclic band; +checking stored row mass alone does not prove support. + +Binary tape movement is executed. Scalar integer macros are exact in the +reference and are priced by a written ordinary schoolbook arithmetic +implementation. Source cache serialization and its conservative polynomial +setup bound are proved, not claimed as a measured fast Python producer. +Retained blank backing is included in space; Python allocator zeroization +and byte-exact host heap accounting are not claimed. + +The saved rectangle must come from original values before any core mutation. +This package consumes that saved copy and returns its target; it does not +implement the full dense-source first-face gather or final dense unique-key +merge. It supplies no new native supplier, core admission, complete broad +Gaussian map, all-depth compiler, CRT join or exact integer multiplier. All +five selected framework assumptions remain. **No new κ.** + +## Provenance and credit + +Scientific base: `7c49fe32c55de02c2c873655c804b16e4c3fef0a`. +The selected conditional frontier at that base is +`781451/250000000 = 0.003125804`; it is unchanged. + +The compatible, concurrently published #6880 proof was read at +`e212af981b49c299de515f8c23dfb0e5b73e2e95`. This package is self-contained for +its local theorem and has no executable dependency on that unmerged commit. +The exact retained Gaussian implementation and source proof are pinned at +the canonical base in SOURCES.json; no predecessor file is changed. + +Prepared for **@CubeJerry**, with substantial OpenAI Codex assistance in +mathematics, source analysis, implementation, verification and prose. Credit +Cinna Davis (#4100), Jose Manuel / jmbarrancoml (#3851, #4205/#4253), +JoyboyBrian (#5159/#5216), Hanson Sun / bbMisk (#1430), Ali Romman +(#5260/#5284), @codyw912 (#4870), Nick Petalas (#4217/#5986), and the inherited work of +Vlado Vojdanovski, Jeremy Kothe, Mason Hale and Chafik Boukhalfa. Classical +Neumann iteration, Horner evaluation, diagonal dominance, stable radix +distribution and ordinary binary arithmetic retain their original credit. +The source's Harvey–van der Hoeven, OpenAI manuscript and Douglas Colkitt +lineage and Apache-2.0 notices are retained in the declared sources. + +## Open next questions + +The former first-face transaction join question is resolved within the +explicit source/plan hypotheses by [the integrated reference +transaction](../first-face-reference-join/README.md). Its source-bound +streamed codec preserves the common grid and original values, canonicalizes +only target returns, and proves the complete group bill. Actual-reference +wrap/hole execution and independent unequal-halo full-grid checks are +retained there. This does not admit the accelerated core or outer caller. + +1. **Use the same rounded reference at the actual finite core and outer + recovery.** The local result does not permit substituting a similarly named + Gaussian matrix. First pin the core's exact reference/normalizers and its + all-input error, then insert (5) in its existing recovery ledger. Source + compatibility and complete outer admission remain open. + +The quantified questions, overlap coverage and stopping rule are also retained +in [TASK.json](TASK.json). No further optimization is reserved by this package. diff --git a/research/shrinking-reference-halo/RESULT.json b/research/shrinking-reference-halo/RESULT.json new file mode 100644 index 0000000000..2e546fe9ab --- /dev/null +++ b/research/shrinking-reference-halo/RESULT.json @@ -0,0 +1,3662 @@ +{ + "backing_reuse": { + "correct": [ + { + "moves": 61264, + "output": [ + [ + -768, + -393 + ], + [ + -704, + -366 + ], + [ + -640, + -339 + ], + [ + -576, + -312 + ], + [ + -512, + -285 + ], + [ + -448, + -257 + ], + [ + -384, + -230 + ], + [ + -320, + -203 + ], + [ + -257, + -176 + ], + [ + -193, + -149 + ], + [ + -129, + -122 + ], + [ + -65, + -95 + ], + [ + -1, + -68 + ], + [ + 62, + -41 + ], + [ + 125, + -14 + ], + [ + 189, + 13 + ], + [ + 253, + 40 + ], + [ + 317, + 67 + ], + [ + 381, + 94 + ], + [ + 445, + 121 + ], + [ + 509, + 148 + ], + [ + 572, + 175 + ], + [ + 636, + 202 + ], + [ + 700, + 229 + ], + [ + 764, + 257 + ], + [ + 764, + 284 + ], + [ + 572, + 311 + ], + [ + -515, + 338 + ], + [ + -707, + 365 + ], + [ + -707, + 392 + ], + [ + -643, + 387 + ], + [ + -579, + 287 + ], + [ + -516, + -261 + ], + [ + -452, + -362 + ], + [ + -388, + -367 + ], + [ + -324, + -340 + ], + [ + -260, + -313 + ] + ], + "retained_bits": 5110, + "saved_length": 41, + "target_length": 37, + "writes": 12292 + }, + { + "moves": 12880, + "output": [ + [ + 505, + 12 + ] + ], + "retained_bits": 5110, + "saved_length": 5, + "target_length": 1, + "writes": 1204 + }, + { + "moves": 69748, + "output": [ + [ + -8, + -341 + ], + [ + 55, + -313 + ], + [ + 118, + -286 + ], + [ + 182, + -259 + ], + [ + 246, + -232 + ], + [ + 310, + -205 + ], + [ + 374, + -178 + ], + [ + 438, + -151 + ], + [ + 502, + -124 + ], + [ + 565, + -96 + ], + [ + 629, + -69 + ], + [ + 693, + -42 + ], + [ + 757, + -15 + ], + [ + 757, + 11 + ], + [ + 565, + 38 + ], + [ + -522, + 65 + ], + [ + -714, + 92 + ], + [ + -714, + 119 + ], + [ + -650, + 146 + ], + [ + -586, + 173 + ], + [ + -523, + 201 + ], + [ + -459, + 228 + ], + [ + -395, + 255 + ], + [ + -331, + 282 + ], + [ + -267, + 309 + ], + [ + -203, + 336 + ], + [ + -139, + 363 + ], + [ + -75, + 390 + ], + [ + -12, + 386 + ], + [ + 13, + 283 + ], + [ + -76, + -272 + ], + [ + -703, + -406 + ], + [ + -793, + -418 + ], + [ + -768, + -393 + ], + [ + -704, + -366 + ], + [ + -640, + -339 + ], + [ + -576, + -312 + ] + ], + "retained_bits": 5110, + "saved_length": 41, + "target_length": 37, + "writes": 12292 + } + ], + "counterfactual": [ + { + "moves": 61488, + "output": [ + [ + -768, + -393 + ], + [ + -704, + -366 + ], + [ + -640, + -339 + ], + [ + -576, + -312 + ], + [ + -512, + -285 + ], + [ + -448, + -257 + ], + [ + -384, + -230 + ], + [ + -320, + -203 + ], + [ + -257, + -176 + ], + [ + -193, + -149 + ], + [ + -129, + -122 + ], + [ + -65, + -95 + ], + [ + -1, + -68 + ], + [ + 62, + -41 + ], + [ + 125, + -14 + ], + [ + 189, + 13 + ], + [ + 253, + 40 + ], + [ + 317, + 67 + ], + [ + 381, + 94 + ], + [ + 445, + 121 + ], + [ + 509, + 148 + ], + [ + 572, + 175 + ], + [ + 636, + 202 + ], + [ + 700, + 229 + ], + [ + 764, + 257 + ], + [ + 764, + 284 + ], + [ + 572, + 311 + ], + [ + -515, + 338 + ], + [ + -707, + 365 + ], + [ + -707, + 392 + ], + [ + -643, + 387 + ], + [ + -579, + 287 + ], + [ + -516, + -261 + ], + [ + -452, + -362 + ], + [ + -388, + -367 + ], + [ + -324, + -340 + ], + [ + -260, + -313 + ] + ], + "retained_bits": 5110, + "saved_length": 41, + "target_length": 37, + "writes": 12404 + }, + { + "moves": 24192, + "output": [ + [ + 505, + 12 + ] + ], + "retained_bits": 5110, + "saved_length": 5, + "target_length": 1, + "writes": 6860 + }, + { + "moves": 69972, + "output": [ + [ + -8, + -341 + ], + [ + 55, + -313 + ], + [ + 118, + -286 + ], + [ + 182, + -259 + ], + [ + 246, + -232 + ], + [ + 310, + -205 + ], + [ + 374, + -178 + ], + [ + 438, + -151 + ], + [ + 502, + -124 + ], + [ + 565, + -96 + ], + [ + 629, + -69 + ], + [ + 693, + -42 + ], + [ + 757, + -15 + ], + [ + 757, + 11 + ], + [ + 565, + 38 + ], + [ + -522, + 65 + ], + [ + -714, + 92 + ], + [ + -714, + 119 + ], + [ + -650, + 146 + ], + [ + -586, + 173 + ], + [ + -523, + 201 + ], + [ + -459, + 228 + ], + [ + -395, + 255 + ], + [ + -331, + 282 + ], + [ + -267, + 309 + ], + [ + -203, + 336 + ], + [ + -139, + 363 + ], + [ + -75, + 390 + ], + [ + -12, + 386 + ], + [ + 13, + 283 + ], + [ + -76, + -272 + ], + [ + -703, + -406 + ], + [ + -793, + -418 + ], + [ + -768, + -393 + ], + [ + -704, + -366 + ], + [ + -640, + -339 + ], + [ + -576, + -312 + ] + ], + "retained_bits": 5110, + "saved_length": 41, + "target_length": 37, + "writes": 12404 + } + ], + "counterfactual_detected": true, + "retained_extent_ratio": "41/5" + }, + "claim": "scoped written proof and finite tape corroboration", + "control_count": 17, + "controls": [ + "unfunded normalization", + "lost normalized-source precision", + "nonunique cyclic offsets", + "missing contraction gap", + "bad original row gap", + "oversized actual input", + "repeated canonical page coordinate", + "immutable coefficient page", + "immutable fixed source", + "prematurely cropped dependency interval", + "noncanonical negative zero", + "wrong recurrence sign", + "wrong neighbor rewind", + "missing scratch erasure", + "wrong sparse axis exposure", + "stale axis coefficient page", + "shifted returned tensor key" + ], + "finite": [ + { + "bill": { + "additions": 0, + "control_steps": 183, + "maximum_single_tape_extent": 495, + "moves": 3828, + "page_scans": 2, + "peak_scalar_bits": 10, + "products": 0, + "reads": 1122, + "roundings": 6, + "setup_divisions": 45, + "setup_entries": 45, + "source_shifts": 6, + "writes": 792 + }, + "bits": 9, + "gap": "1/8", + "length": 3, + "lower": -2, + "nonzero_error": true, + "output": [ + [ + -43, + -1 + ], + [ + 15, + 40 + ], + [ + 43, + -17 + ] + ], + "period": 15, + "resident_extents": [ + 66, + 99, + 66, + 0 + ], + "terms": 1, + "width": 1 + }, + { + "bill": { + "additions": 30, + "control_steps": 385, + "maximum_single_tape_extent": 1200, + "moves": 11376, + "page_scans": 2, + "peak_scalar_bits": 19, + "products": 30, + "reads": 3252, + "roundings": 20, + "setup_divisions": 100, + "setup_entries": 100, + "source_shifts": 20, + "writes": 2268 + }, + "bits": 10, + "gap": "1/4", + "length": 3, + "lower": 17, + "nonzero_error": true, + "output": [ + [ + -85, + 93 + ], + [ + -139, + 145 + ], + [ + 166, + -5 + ] + ], + "period": 20, + "resident_extents": [ + 168, + 420, + 72, + 168 + ], + "terms": 2, + "width": 2 + }, + { + "bill": { + "additions": 48, + "control_steps": 207, + "maximum_single_tape_extent": 819, + "moves": 8944, + "page_scans": 1, + "peak_scalar_bits": 22, + "products": 48, + "reads": 2223, + "roundings": 30, + "setup_divisions": 63, + "setup_entries": 63, + "source_shifts": 30, + "writes": 2054 + }, + "bits": 11, + "gap": "3/8", + "length": 3, + "lower": 9, + "nonzero_error": true, + "output": [ + [ + 115, + -111 + ], + [ + 300, + 200 + ], + [ + 337, + 193 + ] + ], + "period": 21, + "resident_extents": [ + 182, + 273, + 182, + 130 + ], + "terms": 3, + "width": 1 + }, + { + "bill": { + "additions": 210, + "control_steps": 681, + "maximum_single_tape_extent": 2100, + "moves": 32928, + "page_scans": 2, + "peak_scalar_bits": 23, + "products": 210, + "reads": 9702, + "roundings": 72, + "setup_divisions": 150, + "setup_entries": 150, + "source_shifts": 72, + "writes": 5586 + }, + "bits": 12, + "gap": "1/8", + "length": 3, + "lower": 1, + "nonzero_error": true, + "output": [ + [ + 230, + 6 + ], + [ + 486, + -58 + ], + [ + -385, + -17 + ] + ], + "period": 30, + "resident_extents": [ + 420, + 1050, + 308, + 420 + ], + "terms": 4, + "width": 2 + }, + { + "bill": { + "additions": 0, + "control_steps": 231, + "maximum_single_tape_extent": 627, + "moves": 4620, + "page_scans": 2, + "peak_scalar_bits": 10, + "products": 0, + "reads": 1386, + "roundings": 6, + "setup_divisions": 57, + "setup_entries": 57, + "source_shifts": 6, + "writes": 924 + }, + "bits": 9, + "gap": "1/4", + "length": 3, + "lower": -2, + "nonzero_error": true, + "output": [ + [ + -40, + -63 + ], + [ + -90, + -31 + ], + [ + 1, + 122 + ] + ], + "period": 19, + "resident_extents": [ + 66, + 99, + 66, + 0 + ], + "terms": 1, + "width": 1 + }, + { + "bill": { + "additions": 30, + "control_steps": 367, + "maximum_single_tape_extent": 1140, + "moves": 11016, + "page_scans": 2, + "peak_scalar_bits": 19, + "products": 30, + "reads": 3132, + "roundings": 20, + "setup_divisions": 95, + "setup_entries": 95, + "source_shifts": 20, + "writes": 2208 + }, + "bits": 10, + "gap": "3/8", + "length": 3, + "lower": 16, + "nonzero_error": true, + "output": [ + [ + 129, + -2 + ], + [ + -211, + 51 + ], + [ + -206, + 13 + ] + ], + "period": 19, + "resident_extents": [ + 168, + 420, + 72, + 168 + ], + "terms": 2, + "width": 2 + }, + { + "bill": { + "additions": 48, + "control_steps": 199, + "maximum_single_tape_extent": 780, + "moves": 8788, + "page_scans": 1, + "peak_scalar_bits": 21, + "products": 48, + "reads": 2184, + "roundings": 30, + "setup_divisions": 60, + "setup_entries": 60, + "source_shifts": 30, + "writes": 2015 + }, + "bits": 11, + "gap": "1/8", + "length": 3, + "lower": 9, + "nonzero_error": true, + "output": [ + [ + -208, + 165 + ], + [ + 194, + -23 + ], + [ + 327, + -150 + ] + ], + "period": 20, + "resident_extents": [ + 182, + 273, + 182, + 130 + ], + "terms": 3, + "width": 1 + }, + { + "bill": { + "additions": 210, + "control_steps": 663, + "maximum_single_tape_extent": 2030, + "moves": 32508, + "page_scans": 2, + "peak_scalar_bits": 23, + "products": 210, + "reads": 9562, + "roundings": 72, + "setup_divisions": 145, + "setup_entries": 145, + "source_shifts": 72, + "writes": 5516 + }, + "bits": 12, + "gap": "1/4", + "length": 3, + "lower": 1, + "nonzero_error": true, + "output": [ + [ + -452, + -551 + ], + [ + 471, + -200 + ], + [ + -718, + -37 + ] + ], + "period": 29, + "resident_extents": [ + 420, + 1050, + 308, + 420 + ], + "terms": 4, + "width": 2 + }, + { + "bill": { + "additions": 0, + "control_steps": 219, + "maximum_single_tape_extent": 594, + "moves": 4422, + "page_scans": 2, + "peak_scalar_bits": 10, + "products": 0, + "reads": 1320, + "roundings": 6, + "setup_divisions": 54, + "setup_entries": 54, + "source_shifts": 6, + "writes": 891 + }, + "bits": 9, + "gap": "3/8", + "length": 3, + "lower": -2, + "nonzero_error": true, + "output": [ + [ + 3, + 24 + ], + [ + 22, + -46 + ], + [ + 1, + 118 + ] + ], + "period": 18, + "resident_extents": [ + 66, + 99, + 66, + 0 + ], + "terms": 1, + "width": 1 + }, + { + "bill": { + "additions": 30, + "control_steps": 439, + "maximum_single_tape_extent": 1380, + "moves": 12456, + "page_scans": 2, + "peak_scalar_bits": 17, + "products": 30, + "reads": 3612, + "roundings": 20, + "setup_divisions": 115, + "setup_entries": 115, + "source_shifts": 20, + "writes": 2448 + }, + "bits": 10, + "gap": "1/8", + "length": 3, + "lower": 20, + "nonzero_error": true, + "output": [ + [ + 22, + 5 + ], + [ + 1, + 43 + ], + [ + -11, + -2 + ] + ], + "period": 23, + "resident_extents": [ + 168, + 420, + 72, + 168 + ], + "terms": 2, + "width": 2 + }, + { + "bill": { + "additions": 48, + "control_steps": 191, + "maximum_single_tape_extent": 741, + "moves": 8632, + "page_scans": 1, + "peak_scalar_bits": 22, + "products": 48, + "reads": 2145, + "roundings": 30, + "setup_divisions": 57, + "setup_entries": 57, + "source_shifts": 30, + "writes": 1976 + }, + "bits": 11, + "gap": "1/4", + "length": 3, + "lower": 8, + "nonzero_error": true, + "output": [ + [ + -448, + -86 + ], + [ + 55, + 179 + ], + [ + 673, + -56 + ] + ], + "period": 19, + "resident_extents": [ + 182, + 273, + 182, + 130 + ], + "terms": 3, + "width": 1 + }, + { + "bill": { + "additions": 210, + "control_steps": 645, + "maximum_single_tape_extent": 1960, + "moves": 32088, + "page_scans": 2, + "peak_scalar_bits": 24, + "products": 210, + "reads": 9422, + "roundings": 72, + "setup_divisions": 140, + "setup_entries": 140, + "source_shifts": 72, + "writes": 5446 + }, + "bits": 12, + "gap": "3/8", + "length": 3, + "lower": 1, + "nonzero_error": true, + "output": [ + [ + 675, + 430 + ], + [ + -876, + 67 + ], + [ + 205, + 399 + ] + ], + "period": 28, + "resident_extents": [ + 420, + 1050, + 308, + 420 + ], + "terms": 4, + "width": 2 + }, + { + "bill": { + "additions": 0, + "control_steps": 207, + "maximum_single_tape_extent": 561, + "moves": 4224, + "page_scans": 2, + "peak_scalar_bits": 10, + "products": 0, + "reads": 1254, + "roundings": 6, + "setup_divisions": 51, + "setup_entries": 51, + "source_shifts": 6, + "writes": 858 + }, + "bits": 9, + "gap": "1/8", + "length": 3, + "lower": -2, + "nonzero_error": true, + "output": [ + [ + 53, + 5 + ], + [ + 56, + 5 + ], + [ + 48, + -1 + ] + ], + "period": 17, + "resident_extents": [ + 66, + 99, + 66, + 0 + ], + "terms": 1, + "width": 1 + }, + { + "bill": { + "additions": 30, + "control_steps": 421, + "maximum_single_tape_extent": 1320, + "moves": 12096, + "page_scans": 2, + "peak_scalar_bits": 20, + "products": 30, + "reads": 3492, + "roundings": 20, + "setup_divisions": 110, + "setup_entries": 110, + "source_shifts": 20, + "writes": 2388 + }, + "bits": 10, + "gap": "1/4", + "length": 3, + "lower": 19, + "nonzero_error": true, + "output": [ + [ + 33, + 288 + ], + [ + -111, + 57 + ], + [ + -143, + -92 + ] + ], + "period": 22, + "resident_extents": [ + 168, + 420, + 72, + 168 + ], + "terms": 2, + "width": 2 + }, + { + "bill": { + "additions": 48, + "control_steps": 223, + "maximum_single_tape_extent": 897, + "moves": 9256, + "page_scans": 1, + "peak_scalar_bits": 22, + "products": 48, + "reads": 2301, + "roundings": 30, + "setup_divisions": 69, + "setup_entries": 69, + "source_shifts": 30, + "writes": 2132 + }, + "bits": 11, + "gap": "3/8", + "length": 3, + "lower": 10, + "nonzero_error": true, + "output": [ + [ + -309, + 183 + ], + [ + 54, + 277 + ], + [ + 570, + -127 + ] + ], + "period": 23, + "resident_extents": [ + 182, + 273, + 182, + 130 + ], + "terms": 3, + "width": 1 + }, + { + "bill": { + "additions": 210, + "control_steps": 627, + "maximum_single_tape_extent": 1890, + "moves": 31668, + "page_scans": 2, + "peak_scalar_bits": 23, + "products": 210, + "reads": 9282, + "roundings": 72, + "setup_divisions": 135, + "setup_entries": 135, + "source_shifts": 72, + "writes": 5376 + }, + "bits": 12, + "gap": "1/8", + "length": 3, + "lower": 1, + "nonzero_error": true, + "output": [ + [ + -641, + -19 + ], + [ + 564, + 128 + ], + [ + 110, + 23 + ] + ], + "period": 27, + "resident_extents": [ + 420, + 1050, + 308, + 420 + ], + "terms": 4, + "width": 2 + }, + { + "bill": { + "additions": 0, + "control_steps": 195, + "maximum_single_tape_extent": 528, + "moves": 4026, + "page_scans": 2, + "peak_scalar_bits": 10, + "products": 0, + "reads": 1188, + "roundings": 6, + "setup_divisions": 48, + "setup_entries": 48, + "source_shifts": 6, + "writes": 825 + }, + "bits": 9, + "gap": "1/4", + "length": 3, + "lower": -2, + "nonzero_error": true, + "output": [ + [ + -29, + 39 + ], + [ + 52, + 56 + ], + [ + -86, + 7 + ] + ], + "period": 16, + "resident_extents": [ + 66, + 99, + 66, + 0 + ], + "terms": 1, + "width": 1 + }, + { + "bill": { + "additions": 30, + "control_steps": 403, + "maximum_single_tape_extent": 1260, + "moves": 11736, + "page_scans": 2, + "peak_scalar_bits": 19, + "products": 30, + "reads": 3372, + "roundings": 20, + "setup_divisions": 105, + "setup_entries": 105, + "source_shifts": 20, + "writes": 2328 + }, + "bits": 10, + "gap": "3/8", + "length": 3, + "lower": 18, + "nonzero_error": true, + "output": [ + [ + -66, + -131 + ], + [ + 185, + 83 + ], + [ + -52, + 69 + ] + ], + "period": 21, + "resident_extents": [ + 168, + 420, + 72, + 168 + ], + "terms": 2, + "width": 2 + }, + { + "bill": { + "additions": 48, + "control_steps": 215, + "maximum_single_tape_extent": 858, + "moves": 9100, + "page_scans": 1, + "peak_scalar_bits": 20, + "products": 48, + "reads": 2262, + "roundings": 30, + "setup_divisions": 66, + "setup_entries": 66, + "source_shifts": 30, + "writes": 2093 + }, + "bits": 11, + "gap": "1/8", + "length": 3, + "lower": 10, + "nonzero_error": true, + "output": [ + [ + -84, + 0 + ], + [ + -198, + -14 + ], + [ + 104, + -128 + ] + ], + "period": 22, + "resident_extents": [ + 182, + 273, + 182, + 130 + ], + "terms": 3, + "width": 1 + }, + { + "bill": { + "additions": 210, + "control_steps": 699, + "maximum_single_tape_extent": 2170, + "moves": 33348, + "page_scans": 2, + "peak_scalar_bits": 24, + "products": 210, + "reads": 9842, + "roundings": 72, + "setup_divisions": 155, + "setup_entries": 155, + "source_shifts": 72, + "writes": 5656 + }, + "bits": 12, + "gap": "1/4", + "length": 3, + "lower": 1, + "nonzero_error": true, + "output": [ + [ + -384, + 105 + ], + [ + 223, + -620 + ], + [ + 486, + 31 + ] + ], + "period": 31, + "resident_extents": [ + 420, + 1050, + 308, + 420 + ], + "terms": 4, + "width": 2 + }, + { + "bill": { + "additions": 0, + "control_steps": 183, + "maximum_single_tape_extent": 495, + "moves": 3828, + "page_scans": 2, + "peak_scalar_bits": 10, + "products": 0, + "reads": 1122, + "roundings": 6, + "setup_divisions": 45, + "setup_entries": 45, + "source_shifts": 6, + "writes": 792 + }, + "bits": 9, + "gap": "3/8", + "length": 3, + "lower": -2, + "nonzero_error": true, + "output": [ + [ + 119, + 0 + ], + [ + 79, + 36 + ], + [ + -27, + 58 + ] + ], + "period": 15, + "resident_extents": [ + 66, + 99, + 66, + 0 + ], + "terms": 1, + "width": 1 + }, + { + "bill": { + "additions": 30, + "control_steps": 385, + "maximum_single_tape_extent": 1200, + "moves": 11376, + "page_scans": 2, + "peak_scalar_bits": 18, + "products": 30, + "reads": 3252, + "roundings": 20, + "setup_divisions": 100, + "setup_entries": 100, + "source_shifts": 20, + "writes": 2268 + }, + "bits": 10, + "gap": "1/8", + "length": 3, + "lower": 17, + "nonzero_error": true, + "output": [ + [ + -21, + 42 + ], + [ + -69, + 54 + ], + [ + -39, + -23 + ] + ], + "period": 20, + "resident_extents": [ + 168, + 420, + 72, + 168 + ], + "terms": 2, + "width": 2 + }, + { + "bill": { + "additions": 48, + "control_steps": 207, + "maximum_single_tape_extent": 819, + "moves": 8944, + "page_scans": 1, + "peak_scalar_bits": 22, + "products": 48, + "reads": 2223, + "roundings": 30, + "setup_divisions": 63, + "setup_entries": 63, + "source_shifts": 30, + "writes": 2054 + }, + "bits": 11, + "gap": "1/4", + "length": 3, + "lower": 9, + "nonzero_error": true, + "output": [ + [ + 297, + -225 + ], + [ + -171, + 132 + ], + [ + -13, + -46 + ] + ], + "period": 21, + "resident_extents": [ + 182, + 273, + 182, + 130 + ], + "terms": 3, + "width": 1 + }, + { + "bill": { + "additions": 210, + "control_steps": 681, + "maximum_single_tape_extent": 2100, + "moves": 32928, + "page_scans": 2, + "peak_scalar_bits": 24, + "products": 210, + "reads": 9702, + "roundings": 72, + "setup_divisions": 150, + "setup_entries": 150, + "source_shifts": 72, + "writes": 5586 + }, + "bits": 12, + "gap": "3/8", + "length": 3, + "lower": 1, + "nonzero_error": true, + "output": [ + [ + 206, + 445 + ], + [ + 419, + -532 + ], + [ + 300, + -519 + ] + ], + "period": 30, + "resident_extents": [ + 420, + 1050, + 308, + 420 + ], + "terms": 4, + "width": 2 + }, + { + "bill": { + "additions": 0, + "control_steps": 231, + "maximum_single_tape_extent": 627, + "moves": 4620, + "page_scans": 2, + "peak_scalar_bits": 10, + "products": 0, + "reads": 1386, + "roundings": 6, + "setup_divisions": 57, + "setup_entries": 57, + "source_shifts": 6, + "writes": 924 + }, + "bits": 9, + "gap": "1/8", + "length": 3, + "lower": -2, + "nonzero_error": true, + "output": [ + [ + -60, + -1 + ], + [ + -63, + 0 + ], + [ + 48, + 8 + ] + ], + "period": 19, + "resident_extents": [ + 66, + 99, + 66, + 0 + ], + "terms": 1, + "width": 1 + }, + { + "bill": { + "additions": 30, + "control_steps": 367, + "maximum_single_tape_extent": 1140, + "moves": 11016, + "page_scans": 2, + "peak_scalar_bits": 20, + "products": 30, + "reads": 3132, + "roundings": 20, + "setup_divisions": 95, + "setup_entries": 95, + "source_shifts": 20, + "writes": 2208 + }, + "bits": 10, + "gap": "1/4", + "length": 3, + "lower": 16, + "nonzero_error": true, + "output": [ + [ + 225, + 22 + ], + [ + 184, + 15 + ], + [ + 198, + 11 + ] + ], + "period": 19, + "resident_extents": [ + 168, + 420, + 72, + 168 + ], + "terms": 2, + "width": 2 + }, + { + "bill": { + "additions": 48, + "control_steps": 199, + "maximum_single_tape_extent": 780, + "moves": 8788, + "page_scans": 1, + "peak_scalar_bits": 22, + "products": 48, + "reads": 2184, + "roundings": 30, + "setup_divisions": 60, + "setup_entries": 60, + "source_shifts": 30, + "writes": 2015 + }, + "bits": 11, + "gap": "3/8", + "length": 3, + "lower": 9, + "nonzero_error": true, + "output": [ + [ + 383, + 172 + ], + [ + 20, + -235 + ], + [ + 323, + -222 + ] + ], + "period": 20, + "resident_extents": [ + 182, + 273, + 182, + 130 + ], + "terms": 3, + "width": 1 + }, + { + "bill": { + "additions": 210, + "control_steps": 663, + "maximum_single_tape_extent": 2030, + "moves": 32508, + "page_scans": 2, + "peak_scalar_bits": 23, + "products": 210, + "reads": 9562, + "roundings": 72, + "setup_divisions": 145, + "setup_entries": 145, + "source_shifts": 72, + "writes": 5516 + }, + "bits": 12, + "gap": "1/8", + "length": 3, + "lower": 1, + "nonzero_error": true, + "output": [ + [ + 488, + 4 + ], + [ + 462, + -41 + ], + [ + -136, + 106 + ] + ], + "period": 29, + "resident_extents": [ + 420, + 1050, + 308, + 420 + ], + "terms": 4, + "width": 2 + }, + { + "bill": { + "additions": 0, + "control_steps": 219, + "maximum_single_tape_extent": 594, + "moves": 4422, + "page_scans": 2, + "peak_scalar_bits": 10, + "products": 0, + "reads": 1320, + "roundings": 6, + "setup_divisions": 54, + "setup_entries": 54, + "source_shifts": 6, + "writes": 891 + }, + "bits": 9, + "gap": "1/4", + "length": 3, + "lower": -2, + "nonzero_error": true, + "output": [ + [ + -25, + -98 + ], + [ + -38, + 37 + ], + [ + 42, + 54 + ] + ], + "period": 18, + "resident_extents": [ + 66, + 99, + 66, + 0 + ], + "terms": 1, + "width": 1 + }, + { + "bill": { + "additions": 30, + "control_steps": 439, + "maximum_single_tape_extent": 1380, + "moves": 12456, + "page_scans": 2, + "peak_scalar_bits": 19, + "products": 30, + "reads": 3612, + "roundings": 20, + "setup_divisions": 115, + "setup_entries": 115, + "source_shifts": 20, + "writes": 2448 + }, + "bits": 10, + "gap": "3/8", + "length": 3, + "lower": 20, + "nonzero_error": true, + "output": [ + [ + -200, + -33 + ], + [ + -39, + 138 + ], + [ + -165, + -32 + ] + ], + "period": 23, + "resident_extents": [ + 168, + 420, + 72, + 168 + ], + "terms": 2, + "width": 2 + }, + { + "bill": { + "additions": 48, + "control_steps": 191, + "maximum_single_tape_extent": 741, + "moves": 8632, + "page_scans": 1, + "peak_scalar_bits": 21, + "products": 48, + "reads": 2145, + "roundings": 30, + "setup_divisions": 57, + "setup_entries": 57, + "source_shifts": 30, + "writes": 1976 + }, + "bits": 11, + "gap": "1/8", + "length": 3, + "lower": 8, + "nonzero_error": true, + "output": [ + [ + -38, + -416 + ], + [ + -142, + -20 + ], + [ + 300, + 45 + ] + ], + "period": 19, + "resident_extents": [ + 182, + 273, + 182, + 130 + ], + "terms": 3, + "width": 1 + }, + { + "bill": { + "additions": 210, + "control_steps": 645, + "maximum_single_tape_extent": 1960, + "moves": 32088, + "page_scans": 2, + "peak_scalar_bits": 23, + "products": 210, + "reads": 9422, + "roundings": 72, + "setup_divisions": 140, + "setup_entries": 140, + "source_shifts": 72, + "writes": 5446 + }, + "bits": 12, + "gap": "1/4", + "length": 3, + "lower": 1, + "nonzero_error": true, + "output": [ + [ + -313, + 436 + ], + [ + -419, + -45 + ], + [ + -133, + 210 + ] + ], + "period": 28, + "resident_extents": [ + 420, + 1050, + 308, + 420 + ], + "terms": 4, + "width": 2 + } + ], + "finite_lines": 32, + "finite_target_outputs": 96, + "gaussian": { + "checked_off_band_entries": 1240, + "dropped_wrap_detected": true, + "gap": "65413/65536", + "holes": [ + 2, + 7, + 12, + 17, + 22, + 27, + 32, + 37 + ], + "lines": [ + { + "bill": { + "additions": 702, + "control_steps": 1219, + "maximum_single_tape_extent": 7830, + "moves": 166440, + "page_scans": 2, + "peak_scalar_bits": 55, + "products": 702, + "reads": 57570, + "roundings": 136, + "setup_divisions": 0, + "setup_entries": 0, + "source_shifts": 136, + "writes": 17730 + }, + "lower": -2, + "nonzero_error": true, + "output": [ + [ + 44823113, + 19209557 + ], + [ + -44739418, + -19173813 + ], + [ + -44739242, + 19173961 + ], + [ + 44739406, + -19174022 + ], + [ + 44739259, + 19173950 + ] + ], + "resident_extents": [ + 1740, + 7830, + 1260, + 1740 + ] + }, + { + "bill": { + "additions": 702, + "control_steps": 1219, + "maximum_single_tape_extent": 7830, + "moves": 166440, + "page_scans": 2, + "peak_scalar_bits": 55, + "products": 702, + "reads": 57570, + "roundings": 136, + "setup_divisions": 0, + "setup_entries": 0, + "source_shifts": 136, + "writes": 17730 + }, + "lower": 5, + "nonzero_error": true, + "output": [ + [ + 44739285, + -19173933 + ], + [ + -44739449, + 19173994 + ], + [ + 44739302, + -19173922 + ], + [ + 44822858, + 19209723 + ], + [ + -44739475, + -19173978 + ] + ], + "resident_extents": [ + 1740, + 7830, + 1260, + 1740 + ] + }, + { + "bill": { + "additions": 702, + "control_steps": 819, + "maximum_single_tape_extent": 7830, + "moves": 144840, + "page_scans": 1, + "peak_scalar_bits": 55, + "products": 702, + "reads": 46770, + "roundings": 136, + "setup_divisions": 0, + "setup_entries": 0, + "source_shifts": 136, + "writes": 17730 + }, + "lower": 18, + "nonzero_error": true, + "output": [ + [ + -44822943, + 19209668 + ], + [ + 44739247, + -19173923 + ], + [ + 44739412, + 19173851 + ], + [ + -44739577, + -19173912 + ], + [ + 44739429, + 19173840 + ] + ], + "resident_extents": [ + 1740, + 7830, + 1260, + 1740 + ] + } + ], + "nonzero_wrap_entries": 2, + "numerical_bound": "11/267931648", + "original_matrix_entries": 1600, + "period": 40, + "setup": { + "band_source_calls": 360, + "kernel_error_bits": 68, + "maximum_rational_height": 175, + "parameters": [ + 32, + 8, + 2, + 1, + 8, + 32 + ], + "production_bill": { + "additions": 0, + "control_steps": 400, + "maximum_single_tape_extent": 10800, + "moves": 21600, + "page_scans": 0, + "peak_scalar_bits": 0, + "products": 0, + "reads": 0, + "roundings": 0, + "setup_divisions": 360, + "setup_entries": 360, + "source_shifts": 0, + "writes": 10800 + }, + "reference_sha256": "1c9678360096d96f71a01153d8ef51ce2b53b5fe2b1f2d35f7b0f6de9d1f9a85", + "stored_coefficient_height": 140, + "stored_entries": 360, + "stored_kernels": 1, + "stored_weights": 32, + "table_bits": 10800, + "weight_precision": 71 + }, + "tail_bound": "228886641/36824245303148281856", + "target_bits": 20, + "tensor": { + "axis_receipts": [ + { + "axis": 0, + "input_lines": 27, + "line_length": 28, + "output_records": 108, + "page_scans": 2, + "products": 17496, + "radix_passes": 10, + "target_length": 4 + }, + { + "axis": 1, + "input_lines": 4, + "line_length": 27, + "output_records": 12, + "page_scans": 2, + "products": 2376, + "radix_passes": 10, + "target_length": 3 + } + ], + "bill": { + "additions": 19872, + "control_steps": 39124, + "maximum_single_tape_extent": 52920, + "moves": 11240280, + "page_scans": 4, + "peak_scalar_bits": 54, + "products": 19872, + "reads": 2398440, + "roundings": 3936, + "setup_divisions": 720, + "setup_entries": 720, + "source_shifts": 3936, + "writes": 2976180 + }, + "copied_records": 756, + "dimensions": 2, + "fixed_local_tape_roles": 8, + "key_width": 10, + "label": "actual-reference-2d", + "nonzero_error": true, + "numerical_bound": "11/133965824", + "output": [ + [ + [ + -1, + 5 + ], + [ + -16563329, + -11064879 + ] + ], + [ + [ + -1, + 6 + ], + [ + -16561022, + -11063579 + ] + ], + [ + [ + -1, + 7 + ], + [ + -16558485, + -11062163 + ] + ], + [ + [ + 0, + 5 + ], + [ + -16770857, + -11181245 + ] + ], + [ + [ + 0, + 6 + ], + [ + -16768550, + -11179945 + ] + ], + [ + [ + 0, + 7 + ], + [ + -16766014, + -11178529 + ] + ], + [ + [ + 1, + 5 + ], + [ + -16770410, + -11180988 + ] + ], + [ + [ + 1, + 6 + ], + [ + -16768103, + -11179688 + ] + ], + [ + [ + 1, + 7 + ], + [ + -16765566, + -11178272 + ] + ], + [ + [ + 2, + 5 + ], + [ + -16769819, + -11180663 + ] + ], + [ + [ + 2, + 6 + ], + [ + -16767512, + -11179363 + ] + ], + [ + [ + 2, + 7 + ], + [ + -16764976, + -11177947 + ] + ] + ], + "protected_archive_bits": 21600, + "role_extents": [ + [ + "rectangle current", + 52920 + ], + [ + "rectangle next", + 7560 + ], + [ + "radix zero", + 31360 + ], + [ + "radix one", + 26460 + ], + [ + "fixed borrowed line", + 1680 + ], + [ + "fixed iterate zero", + 1680 + ], + [ + "fixed iterate one", + 1200 + ], + [ + "fixed local band page", + 7560 + ] + ], + "saved_lengths": [ + 28, + 27 + ], + "source_setup": { + "kernel_error_bits": 68, + "maximum_rational_height": 175, + "parameters": [ + 32, + 8, + 2, + 1, + 8, + 32 + ], + "reference_sha256": "1c9678360096d96f71a01153d8ef51ce2b53b5fe2b1f2d35f7b0f6de9d1f9a85", + "stored_entries": 360, + "stored_kernels": 1, + "stored_weights": 32, + "weight_precision": 71 + }, + "target_records": 12, + "total_retained_local_bits": 130420 + } + }, + "no_new_kappa": true, + "nonzero_rounding_lines": 32, + "program_sha256": { + "engine.py": "38ca22b213a0291cc7ba821baf513db289c1c3e7c24c579c5eff3349280484b2", + "source.py": "20c0fb2e4aa95de976ef6ce74ded4bf1cb9073732eca7eda8f61e45d239afa2c", + "tensor.py": "b3cfe3c18988a89d4a639e8104db7a87f7029d556c74c2e0f60d687ec6be5e80", + "verify.py": "9263a65f31d75f0f53d6acb2219781ee3b48a56fe08963716f104890ea5945f5" + }, + "rectangle_reuse": { + "constructors_sealed_during_calls": true, + "fixed_role_count": 8, + "history": [ + { + "archive_scans": 3, + "copied_records": 81, + "moves": 582456, + "output": [ + [ + [ + -1, + 4 + ], + [ + 12, + -25 + ] + ], + [ + [ + -1, + 5 + ], + [ + 20, + -23 + ] + ], + [ + [ + -1, + 6 + ], + [ + 28, + -20 + ] + ], + [ + [ + -1, + 7 + ], + [ + 39, + -28 + ] + ], + [ + [ + -1, + 8 + ], + [ + 50, + -27 + ] + ], + [ + [ + 0, + 4 + ], + [ + -32, + -27 + ] + ], + [ + [ + 0, + 5 + ], + [ + -24, + -25 + ] + ], + [ + [ + 0, + 6 + ], + [ + -16, + -23 + ] + ], + [ + [ + 0, + 7 + ], + [ + -8, + -22 + ] + ], + [ + [ + 0, + 8 + ], + [ + 0, + -22 + ] + ], + [ + [ + 1, + 4 + ], + [ + -35, + -19 + ] + ], + [ + [ + 1, + 5 + ], + [ + -27, + -17 + ] + ], + [ + [ + 1, + 6 + ], + [ + -19, + -15 + ] + ], + [ + [ + 1, + 7 + ], + [ + -10, + -13 + ] + ], + [ + [ + 1, + 8 + ], + [ + -3, + -12 + ] + ], + [ + [ + 2, + 4 + ], + [ + -31, + -10 + ] + ], + [ + [ + 2, + 5 + ], + [ + -23, + -8 + ] + ], + [ + [ + 2, + 6 + ], + [ + -15, + -6 + ] + ], + [ + [ + 2, + 7 + ], + [ + -7, + -4 + ] + ], + [ + [ + 2, + 8 + ], + [ + 0, + -3 + ] + ], + [ + [ + 3, + 4 + ], + [ + -28, + -1 + ] + ], + [ + [ + 3, + 5 + ], + [ + -19, + 0 + ] + ], + [ + [ + 3, + 6 + ], + [ + -11, + 1 + ] + ], + [ + [ + 3, + 7 + ], + [ + -3, + 3 + ] + ], + [ + [ + 3, + 8 + ], + [ + 4, + 6 + ] + ], + [ + [ + 4, + 4 + ], + [ + -24, + 6 + ] + ], + [ + [ + 4, + 5 + ], + [ + -16, + 8 + ] + ], + [ + [ + 4, + 6 + ], + [ + -8, + 10 + ] + ], + [ + [ + 4, + 7 + ], + [ + 0, + 13 + ] + ], + [ + [ + 4, + 8 + ], + [ + 8, + 16 + ] + ], + [ + [ + 5, + 4 + ], + [ + -20, + 15 + ] + ], + [ + [ + 5, + 5 + ], + [ + -12, + 17 + ] + ], + [ + [ + 5, + 6 + ], + [ + -4, + 19 + ] + ], + [ + [ + 5, + 7 + ], + [ + 3, + 22 + ] + ], + [ + [ + 5, + 8 + ], + [ + 12, + 25 + ] + ] + ], + "retained_bits": 8988, + "saved_lengths": [ + 9, + 9 + ], + "target_records": 35, + "writes": 181088 + }, + { + "archive_scans": 3, + "copied_records": 18, + "moves": 66468, + "output": [ + [ + [ + 8, + -1 + ], + [ + -44, + -7 + ] + ], + [ + [ + 8, + 0 + ], + [ + -33, + 28 + ] + ] + ], + "retained_bits": 8988, + "saved_lengths": [ + 3, + 6 + ], + "target_records": 2, + "writes": 18956 + }, + { + "archive_scans": 3, + "copied_records": 77, + "moves": 472446, + "output": [ + [ + [ + 1, + 9 + ], + [ + 4, + -10 + ] + ], + [ + [ + 1, + 10 + ], + [ + 13, + -7 + ] + ], + [ + [ + 1, + 11 + ], + [ + 21, + -5 + ] + ], + [ + [ + 1, + 12 + ], + [ + 29, + -3 + ] + ], + [ + [ + 1, + 13 + ], + [ + 37, + -1 + ] + ], + [ + [ + 1, + 14 + ], + [ + 45, + 0 + ] + ], + [ + [ + 1, + 15 + ], + [ + 52, + 2 + ] + ], + [ + [ + 2, + 9 + ], + [ + 8, + 0 + ] + ], + [ + [ + 2, + 10 + ], + [ + 16, + 0 + ] + ], + [ + [ + 2, + 11 + ], + [ + 24, + 2 + ] + ], + [ + [ + 2, + 12 + ], + [ + 32, + 5 + ] + ], + [ + [ + 2, + 13 + ], + [ + 40, + 6 + ] + ], + [ + [ + 2, + 14 + ], + [ + 48, + 8 + ] + ], + [ + [ + 2, + 15 + ], + [ + 56, + 10 + ] + ], + [ + [ + 3, + 9 + ], + [ + 12, + 7 + ] + ], + [ + [ + 3, + 10 + ], + [ + 20, + 9 + ] + ], + [ + [ + 3, + 11 + ], + [ + 28, + 11 + ] + ], + [ + [ + 3, + 12 + ], + [ + 36, + 13 + ] + ], + [ + [ + 3, + 13 + ], + [ + 44, + 15 + ] + ], + [ + [ + 3, + 14 + ], + [ + 52, + 17 + ] + ], + [ + [ + 3, + 15 + ], + [ + 61, + 19 + ] + ], + [ + [ + 4, + 9 + ], + [ + 16, + 16 + ] + ], + [ + [ + 4, + 10 + ], + [ + 23, + 18 + ] + ], + [ + [ + 4, + 11 + ], + [ + 31, + 20 + ] + ], + [ + [ + 4, + 12 + ], + [ + 39, + 21 + ] + ], + [ + [ + 4, + 13 + ], + [ + 48, + 24 + ] + ], + [ + [ + 4, + 14 + ], + [ + 55, + 26 + ] + ], + [ + [ + 4, + 15 + ], + [ + 72, + 20 + ] + ], + [ + [ + 5, + 9 + ], + [ + 19, + 26 + ] + ], + [ + [ + 5, + 10 + ], + [ + 27, + 19 + ] + ], + [ + [ + 5, + 11 + ], + [ + 35, + 21 + ] + ], + [ + [ + 5, + 12 + ], + [ + 43, + 23 + ] + ], + [ + [ + 5, + 13 + ], + [ + 51, + 25 + ] + ], + [ + [ + 5, + 14 + ], + [ + 60, + 31 + ] + ], + [ + [ + 5, + 15 + ], + [ + 60, + -30 + ] + ] + ], + "retained_bits": 9204, + "saved_lengths": [ + 7, + 11 + ], + "target_records": 35, + "writes": 145378 + } + ] + }, + "schema_version": 1, + "seed": 72, + "source_sha256": { + "research/certified-gaussian-recovery/NOTICE.md": "10acae9e78402ca70c6afd0e8d6da8fefc0da519c646cf43d93f923aba85b86d", + "research/certified-gaussian-recovery/intervals.py": "159d2a7d32a8cc7c8f56632a8ef127308b984a0a6753c9d6bdccacc6e7d6d4df", + "research/rational-unitary-fft/RAW-GAUSSIAN-PROOF.md": "3f683643a0c0b45d58ec09ebe511e4006cd103e38753f82a4ce21a8570383358", + "research/rational-unitary-fft/exact.py": "c9b89d7357210af69865690ba12e695366961f8b501a8fab9d0fefe3fb30c479", + "research/rational-unitary-fft/gaussian.py": "08155357fd39b5fd7959f51f1d205b6511b8577b51520d793c89f92368b399ab", + "research/rational-unitary-fft/gaussian_reference.py": "ed4d0908646e391d4a0ea32c988a0301a1793a72294ac7058a664ed3283ca3c3", + "research/unconditional-batched-crt/GAUSSIAN.md": "2f63c91c58f2d1cf31294812c75970ea390c61866a8da7ed700d4316a033a242", + "research/unconditional-batched-crt/HALO.md": "a2adcf18614983e9255def6d3f5e59be0018a392e418d65e94323722838289cc", + "research/unconditional-batched-crt/PROOF.md": "689fc7b01c5f04f77019ff02d1b79cb4f7020bd98e05b1052020bad295dec060" + }, + "tensors": [ + { + "axis_receipts": [ + { + "axis": 0, + "input_lines": 6, + "line_length": 4, + "output_records": 12, + "page_scans": 2, + "products": 72, + "radix_passes": 5, + "target_length": 2 + }, + { + "axis": 1, + "input_lines": 2, + "line_length": 6, + "output_records": 4, + "page_scans": 2, + "products": 72, + "radix_passes": 5, + "target_length": 2 + } + ], + "bill": { + "additions": 144, + "control_steps": 1226, + "maximum_single_tape_extent": 792, + "moves": 103200, + "page_scans": 4, + "peak_scalar_bits": 18, + "products": 144, + "reads": 19976, + "roundings": 120, + "setup_divisions": 66, + "setup_entries": 66, + "source_shifts": 120, + "writes": 30904 + }, + "copied_records": 24, + "dimensions": 2, + "fixed_local_tape_roles": 8, + "key_width": 5, + "label": "signed-2d", + "nonzero_error": true, + "numerical_bound": "25/768", + "output": [ + [ + [ + -1, + 9 + ], + [ + 23, + -9 + ] + ], + [ + [ + -1, + 10 + ], + [ + -16, + 9 + ] + ], + [ + [ + 0, + 9 + ], + [ + -11, + 8 + ] + ], + [ + [ + 0, + 10 + ], + [ + 1, + 6 + ] + ] + ], + "protected_archive_bits": 792, + "role_extents": [ + [ + "rectangle current", + 696 + ], + [ + "rectangle next", + 348 + ], + [ + "radix zero", + 464 + ], + [ + "radix one", + 348 + ], + [ + "fixed borrowed line", + 144 + ], + [ + "fixed iterate zero", + 144 + ], + [ + "fixed iterate one", + 96 + ], + [ + "fixed local band page", + 216 + ] + ], + "saved_lengths": [ + 4, + 6 + ], + "target_records": 4, + "total_retained_local_bits": 2456 + }, + { + "axis_receipts": [ + { + "axis": 0, + "input_lines": 24, + "line_length": 4, + "output_records": 48, + "page_scans": 2, + "products": 288, + "radix_passes": 7, + "target_length": 2 + }, + { + "axis": 1, + "input_lines": 8, + "line_length": 6, + "output_records": 16, + "page_scans": 2, + "products": 288, + "radix_passes": 7, + "target_length": 2 + }, + { + "axis": 2, + "input_lines": 4, + "line_length": 4, + "output_records": 8, + "page_scans": 2, + "products": 48, + "radix_passes": 7, + "target_length": 2 + } + ], + "bill": { + "additions": 624, + "control_steps": 5151, + "maximum_single_tape_extent": 2976, + "moves": 559200, + "page_scans": 6, + "peak_scalar_bits": 18, + "products": 624, + "reads": 102260, + "roundings": 528, + "setup_divisions": 99, + "setup_entries": 99, + "source_shifts": 528, + "writes": 174220 + }, + "copied_records": 96, + "dimensions": 3, + "fixed_local_tape_roles": 8, + "key_width": 7, + "label": "signed-3d", + "nonzero_error": true, + "numerical_bound": "65/1536", + "output": [ + [ + [ + -1, + 9, + -1 + ], + [ + -3, + 0 + ] + ], + [ + [ + -1, + 9, + 0 + ], + [ + -1, + 0 + ] + ], + [ + [ + -1, + 10, + -1 + ], + [ + -1, + -1 + ] + ], + [ + [ + -1, + 10, + 0 + ], + [ + 3, + 0 + ] + ], + [ + [ + 0, + 9, + -1 + ], + [ + -1, + 2 + ] + ], + [ + [ + 0, + 9, + 0 + ], + [ + 2, + -2 + ] + ], + [ + [ + 0, + 10, + -1 + ], + [ + 6, + 1 + ] + ], + [ + [ + 0, + 10, + 0 + ], + [ + -3, + 1 + ] + ] + ], + "protected_archive_bits": 1188, + "role_extents": [ + [ + "rectangle current", + 2976 + ], + [ + "rectangle next", + 1488 + ], + [ + "radix zero", + 1984 + ], + [ + "radix one", + 1488 + ], + [ + "fixed borrowed line", + 144 + ], + [ + "fixed iterate zero", + 144 + ], + [ + "fixed iterate one", + 96 + ], + [ + "fixed local band page", + 216 + ] + ], + "saved_lengths": [ + 4, + 6, + 4 + ], + "target_records": 8, + "total_retained_local_bits": 8536 + } + ] +} diff --git a/research/shrinking-reference-halo/SOURCES.json b/research/shrinking-reference-halo/SOURCES.json new file mode 100644 index 0000000000..2e7ea79dae --- /dev/null +++ b/research/shrinking-reference-halo/SOURCES.json @@ -0,0 +1,72 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "research/rational-unitary-fft/exact.py", + "usage": "input", + "git_blob": "aae41e6acfb2e5a4fafdd85727891eb746b57b42", + "sha256": "c9b89d7357210af69865690ba12e695366961f8b501a8fab9d0fefe3fb30c479" + }, + { + "path": "research/rational-unitary-fft/gaussian.py", + "usage": "input", + "git_blob": "52ad2e1d605f5f7d669234567c25bc087306dd44", + "sha256": "08155357fd39b5fd7959f51f1d205b6511b8577b51520d793c89f92368b399ab" + }, + { + "path": "research/rational-unitary-fft/gaussian_reference.py", + "usage": "input", + "git_blob": "92addfabde50655cea7ad5a84cca9cff5457adee", + "sha256": "ed4d0908646e391d4a0ea32c988a0301a1793a72294ac7058a664ed3283ca3c3" + }, + { + "path": "research/rational-unitary-fft/RAW-GAUSSIAN-PROOF.md", + "usage": "input", + "git_blob": "1fb549d24a419abb50f5b772437d87e48c65fe06", + "sha256": "3f683643a0c0b45d58ec09ebe511e4006cd103e38753f82a4ce21a8570383358" + }, + { + "path": "research/certified-gaussian-recovery/intervals.py", + "usage": "input", + "git_blob": "91d458865aa026bdf0d59653a4ecbfe3a178ecbc", + "sha256": "159d2a7d32a8cc7c8f56632a8ef127308b984a0a6753c9d6bdccacc6e7d6d4df" + }, + { + "path": "research/certified-gaussian-recovery/NOTICE.md", + "usage": "input", + "git_blob": "5e3269b5afe5e11f044ffae45216c4731b42c7af", + "sha256": "10acae9e78402ca70c6afd0e8d6da8fefc0da519c646cf43d93f923aba85b86d" + }, + { + "path": "research/unconditional-batched-crt/HALO.md", + "usage": "input", + "git_blob": "5f601b3c8ac368aa79aa1007effe5933a360237b", + "sha256": "a2adcf18614983e9255def6d3f5e59be0018a392e418d65e94323722838289cc" + }, + { + "path": "research/unconditional-batched-crt/PROOF.md", + "usage": "input", + "git_blob": "406eb561cc8d6041ea3fba1a849653b654f2198c", + "sha256": "689fc7b01c5f04f77019ff02d1b79cb4f7020bd98e05b1052020bad295dec060" + }, + { + "path": "research/unconditional-batched-crt/GAUSSIAN.md", + "usage": "input", + "git_blob": "adfb28c93e6b06178c901caaac39ede41a9e541b", + "sha256": "2f63c91c58f2d1cf31294812c75970ea390c61866a8da7ed700d4316a033a242" + } + ] +} diff --git a/research/shrinking-reference-halo/TASK.json b/research/shrinking-reference-halo/TASK.json new file mode 100644 index 0000000000..e86759a09a --- /dev/null +++ b/research/shrinking-reference-halo/TASK.json @@ -0,0 +1,93 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Choose one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "native_all_columns", + "owned_erasure", + "compiler", + "precision_tape", + "analytic_recovery" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "refined", + "actual_scope": "A source-bound local shrinking-domain normalized inverse tensor consumer on fixed sequential tape roles, with coefficient/data error, original reference-band production, full archive access, physical sparse axis exposure and complete generic/production cost.", + "scope_change_reason": "Direct degree specialization and generic Horner stability are already proved. Follow the remaining global coefficient-page and physical local consumer obligation of #6880 and the host-array service boundary of #5159; retain all original Gaussian and outer assumptions.", + "bottleneck_link": "Constructs one analytic_recovery/precision_tape component using the actual rational Gaussian Reference without a global polynomial-row oracle. Does not discharge either complete selected assumption.", + "budget_minutes": 180, + "stop_rule": "Stop at the verified local consumer and its complete cost. No scalar degree retuning, source analytic reproof, independent supplier admission or speculative outer theorem claim.", + "outcome": "completed", + "evidence": "PROOF.md; engine.py/source.py/tensor.py; exact typed RESULT.json; independently developed original-inverse rational elimination and all-row residual certificates; six successful normal and optimized registered replays; predecessor overlap sources.", + "author": "CubeJerry", + "ai_assistance": "Substantial OpenAI Codex assistance in mathematics, source analysis, implementation, exact verification and separate adversarial AI review.", + "open_questions": [ + { + "question": "Can the same fixed reference and normalizer be admitted at the finite core and outer recovery?", + "why_it_matters": "Similar Gaussian terminology does not make different rounded matrices or all-input error contracts interchangeable.", + "first_step": "Pin the exact core reference and actual-input theorem, then substitute the complete tensor error in the existing recovery ledger.", + "blocked_by": "Finite core adoption, source compatibility and full outer multiplier admission remain unproved here." + } + ], + "resolved_questions": [ + { + "question": "Can this local consumer be joined to the actual first-face gather and unique-return transaction?", + "why_it_matters": "Its saved rectangle must contain original values before core mutation, and every returned target key must be consumed exactly once.", + "first_step": "Bind one wrapping/hole rectangle codec and q-grid on both sides, then prove and execute the complete group transaction.", + "blocked_by": "The dense-source copy/return chronology and actual outer ownership interface are outside this package.", + "resolution": "Resolved under the explicit source/plan hypotheses by research/first-face-reference-join: universal codec/chronology/cost composition, actual Reference64 transaction, independent whole-grid unequal-halo/spectator checks. Actual core and complete outer admission remain open." + } + ], + "integration_package": "research/first-face-reference-join" +} diff --git a/research/shrinking-reference-halo/VERIFY.json b/research/shrinking-reference-halo/VERIFY.json new file mode 100644 index 0000000000..1345ca68ab --- /dev/null +++ b/research/shrinking-reference-halo/VERIFY.json @@ -0,0 +1,82 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/rational-unitary-fft/exact.py", + "research/rational-unitary-fft/gaussian.py", + "research/rational-unitary-fft/gaussian_reference.py", + "research/rational-unitary-fft/RAW-GAUSSIAN-PROOF.md", + "research/certified-gaussian-recovery/intervals.py", + "research/certified-gaussian-recovery/NOTICE.md", + "research/unconditional-batched-crt/HALO.md", + "research/unconditional-batched-crt/PROOF.md", + "research/unconditional-batched-crt/GAUSSIAN.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Exact source-band line/tensor proof obligations, all forty-row reference entries, fixed-role history, complete physical invoices and negative controls; typed mandatory receipt." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "The identical exact source-bound consumer, ownership histories and rejection controls with assertions disabled." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/independent_inverse.py" + ], + "timeout_seconds": 180, + "checks": "Separate exact original-matrix inverse-row elimination and physical two-axis tensor execution, sealed fixed-role reuse and wrong-target control. Normal replay." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/independent_inverse.py" + ], + "timeout_seconds": 180, + "checks": "Separate exact original-matrix inverse-row elimination and physical two-axis tensor execution, sealed fixed-role reuse and wrong-target control. Assertions-disabled replay." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/independent_residual.py" + ], + "timeout_seconds": 120, + "checks": "Separate all-forty-row original-reference residual certificate and wrong-return-order lower bound, without the author polynomial verifier. Normal replay." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/independent_residual.py" + ], + "timeout_seconds": 120, + "checks": "Separate all-forty-row original-reference residual certificate and wrong-return-order lower bound, without the author polynomial verifier. Assertions-disabled replay." + } + ] +} diff --git a/research/shrinking-reference-halo/engine.py b/research/shrinking-reference-halo/engine.py new file mode 100644 index 0000000000..984dffee3f --- /dev/null +++ b/research/shrinking-reference-halo/engine.py @@ -0,0 +1,385 @@ +"""Sequential shrinking-domain normalized inverse action. + +Prepared for @CubeJerry with substantial OpenAI Codex assistance. Apache-2.0. +Classical fixed-source Horner iteration is inherited; this file supplies the +local shrinking domains, sequential band-page extraction and ownership trace. +Bit-tape movement is executed. Bounded integer arithmetic is a declared scalar +macro, with its ordinary schoolbook bit cost established in PROOF.md. +""" +from dataclasses import dataclass, field +from fractions import Fraction as Q +from hashlib import sha256 + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def trunc(n, denominator): + need(type(n) is int and type(denominator) is int and denominator > 0, + "integer truncation domain") + return (-1 if n < 0 else 1) * (abs(n) // denominator) + + +def inward(value, bits): + value = Q(value) + return trunc(value.numerator << bits, value.denominator) + + +@dataclass +class Bill: + reads: int = 0 + writes: int = 0 + moves: int = 0 + products: int = 0 + additions: int = 0 + roundings: int = 0 + source_shifts: int = 0 + control_steps: int = 0 + peak_scalar_bits: int = 0 + setup_entries: int = 0 + setup_divisions: int = 0 + page_scans: int = 0 + maximum_single_tape_extent: int = 0 + + def scalar(self, *values): + self.peak_scalar_bits = max(self.peak_scalar_bits, + *(abs(x).bit_length() + 1 for x in values)) + + def record(self): + return {name: getattr(self, name) for name in self.__dataclass_fields__} + + +class Tape: + """Binary tape; data may be accessed only at the current head. + + The host list implements tape cells, not a program-visible indexed array. + snapshot() is an independent diagnostic, never a transition primitive. + Blank cells are zero. Every cell beyond live_bits is already blank. Clear + erases the complete current live body; retained blank backing stays paid + in space but need not be erased again for every later shorter line. + """ + def __init__(self, bill, name): + self._cells = [] + self.head = 0 + self.live_bits = 0 + self.bill = bill + self.name = name + self.readonly = False + + @property + def extent(self): + return len(self._cells) + + def read(self): + need(self.head < self.live_bits, "read beyond live encoded body") + self.bill.reads += 1 + return self._cells[self.head] if self.head < self.extent else 0 + + def write(self, bit): + need(not self.readonly, "write to borrowed immutable tape") + need(type(bit) is int and bit in (0, 1), "binary cell") + if self.head >= self.extent: + self._cells.extend([0] * (self.head + 1 - self.extent)) + self._cells[self.head] = bit + self.live_bits = max(self.live_bits, self.head + 1) + self.bill.writes += 1 + self.bill.maximum_single_tape_extent = max(self.bill.maximum_single_tape_extent, self.extent) + + def step(self, direction): + need(type(direction) is int and direction in (-1, 1), "one-cell head move") + need(self.head + direction >= 0, "left tape boundary") + self.head += direction + self.bill.moves += 1 + + def walk(self, distance): + need(type(distance) is int, "encoded head displacement") + direction = -1 if distance < 0 else 1 + for _ in range(abs(distance)): + self.step(direction) + + def rewind(self): + self.walk(-self.head) + + def clear(self): + need(not self.readonly, "clear borrowed immutable tape") + self.rewind() + occupied = self.live_bits + for _ in range(occupied): + self.write(0) + self.step(1) + self.rewind() + self.live_bits = 0 + + def snapshot(self): + return bytes(self._cells) + + +def put_int(tape, value, width): + need(type(value) is int and type(width) is int and width >= 2, + "fixed-width integer") + need(abs(value) < (1 << (width - 1)), "integer carrier overflow") + tape.write(int(value < 0)); tape.step(1) + for shift in range(width - 2, -1, -1): + tape.write((abs(value) >> shift) & 1); tape.step(1) + + +def get_int(tape, width): + sign = tape.read(); tape.step(1) + magnitude = 0 + for _ in range(width - 1): + magnitude = 2 * magnitude + tape.read(); tape.step(1) + need(not (sign and magnitude == 0), "noncanonical negative zero") + return -magnitude if sign else magnitude + + +def put_complex(tape, value, width): + need(type(value) is tuple and len(value) == 2, "signed complex pair") + put_int(tape, value[0], width); put_int(tape, value[1], width) + + +def get_complex(tape, width): + return get_int(tape, width), get_int(tape, width) + + +@dataclass(frozen=True) +class Plan: + period: int + halfwidth: int + bits: int + terms: int + normalizer_shift: int + gap: Q + radius: int = 1 + + def __post_init__(self): + need(all(type(x) is int for x in (self.period, self.halfwidth, self.bits, + self.terms, self.normalizer_shift, self.radius)), "integer plan parameters") + need(self.period > 0 and self.halfwidth >= 0 + and 2 * self.halfwidth < self.period, "unique cyclic band offsets") + need(self.bits >= self.normalizer_shift >= 0 and self.terms >= 1 + and self.radius >= 1, "precision, iteration and radius domain") + need(type(self.gap) in (int, Q) and 0 < self.gap <= 1, "positive rational gap") + need((1 << self.normalizer_shift) * self.gap >= 1, "funded normalization") + + @property + def band(self): + return 2 * self.halfwidth + 1 + + @property + def halo(self): + return (self.terms - 1) * self.halfwidth + + @property + def coefficient_width(self): + return self.bits + 2 + + @property + def data_width(self): + return self.bits + self.radius.bit_length() + 1 + + @property + def numeric_error(self): + return Q(self.band * self.radius + 2, 1 << self.bits) / self.gap + + @property + def tail_error(self): + return self.radius * (1 - self.gap) ** self.terms / ( + (1 << self.normalizer_shift) * self.gap) + + +@dataclass(frozen=True) +class Table: + tape: Tape + plan: Plan + source_id: str + + +@dataclass(frozen=True) +class Page: + tape: Tape + plan: Plan + lower: int + length: int + source_id: str + + +@dataclass(frozen=True) +class Output: + tape: Tape + lower: int + length: int + width: int + blank_scratch: tuple = field(repr=False) + + +def prepare_table(plan, entry, source_id, bill): + """entry(row, column) returns the exact fixed E=I-H coefficient. + + Generic entry-production cost remains explicit; source.py provides the + authenticated Gaussian instantiation and its separately charged setup. + All offsets, including zero entries, are generated and stored. + """ + tape = Tape(bill, "global band table") + largest_height = 0 + for row in range(plan.period): + mass = Q(0) + for offset in range(-plan.halfwidth, plan.halfwidth + 1): + value = Q(entry(row, (row + offset) % plan.period)) + largest_height = max(largest_height, abs(value.numerator).bit_length(), + value.denominator.bit_length()) + mass += abs(value) + coefficient = inward(value, plan.bits) + need(abs(Q(coefficient, 1 << plan.bits)) <= abs(value), "inward coefficient") + need(abs(value - Q(coefficient, 1 << plan.bits)) < Q(1, 1 << plan.bits), + "coefficient error") + put_int(tape, coefficient, plan.coefficient_width) + bill.setup_entries += 1 + bill.setup_divisions += 1 + need(mass <= 1 - plan.gap, "actual source row gap") + bill.control_steps += plan.band + 1 + tape.rewind(); tape.readonly = True + return Table(tape, plan, source_id), largest_height + + +def extract_page(table, lower, length, bill, page_tape=None): + """At most two COMPLETE ordered scans, including all skipped records. + + The lifted interval has length less than the physical period, so each + canonical coordinate appears at most once. A wrapping tail is emitted + before its head. No random seek into the global table is used. + """ + plan = table.plan + need(type(lower) is int and type(length) is int and 0 < length < plan.period, + "nonaliasing lifted page interval") + need(table.tape.head == 0, "global table origin") + # Accounting ownership can change between calls; it is not encoded data. + # Charge the repeated complete scan to THIS call, not to old preparation. + table.tape.bill = bill + start = lower % plan.period + first = min(length, plan.period - start) + spans = [(start, start + first)] + if first < length: + spans.append((0, length - first)) + page = page_tape if page_tape is not None else Tape(bill, "local band page") + need(page.head == 0 and not page.readonly and page.live_bits == 0, + "blank local page role") + page.bill = bill + for begin, end in spans: + for row in range(plan.period): + for _ in range(plan.band): + value = get_int(table.tape, plan.coefficient_width) + if begin <= row < end: + put_int(page, value, plan.coefficient_width) + bill.control_steps += plan.band + 1 + table.tape.rewind() + bill.page_scans += 1 + need(page.head == length * plan.band * plan.coefficient_width, + "complete ordered page") + page.rewind(); page.readonly = True + return Page(page, plan, lower, length, table.source_id) + + +def input_tape(plan, values, bill): + tape = Tape(bill, "borrowed input") + for value in values: + need(type(value) is tuple and len(value) == 2 and + all(type(x) is int for x in value), "integer grid input") + need(abs(value[0]) + abs(value[1]) <= plan.radius * (1 << plan.bits), + "input radius") + put_complex(tape, value, plan.data_width) + tape.rewind(); tape.readonly = True + return tape + + +def apply_line(page, source, target_lower, target_length, bill, workspace=None): + """Return only the target; preserve borrowed input/page and both origins. + + source contains the entire saved dependency interval. All arithmetic is + performed on encoded integer numerators; no Fraction or matrix oracle is + used by the online recurrence. Other tensor coordinates are spectators. + """ + p = page.plan + need(type(target_lower) is int and type(target_length) is int and target_length > 0, + "nonempty target interval") + lower, length = target_lower - p.halo, target_length + 2 * p.halo + need(page.lower == lower and page.length == length, "exact saved dependency domain") + need(length < p.period, "no repeated canonical input coordinate") + need(source.readonly and page.tape.readonly and source.head == page.tape.head == 0, + "immutable origin-aligned input and page") + source.bill = page.tape.bill = bill + record_bits = 2 * p.data_width + need(source.live_bits == length * record_bits, "complete input shape") + if workspace is None: + current, following = Tape(bill, "current iterate"), Tape(bill, "next iterate") + else: + need(type(workspace) is tuple and len(workspace) == 2 + and workspace[0] is not workspace[1], "two distinct fixed iterate roles") + current, following = workspace + need(all(t.head == 0 and not t.readonly and t.live_bits == 0 for t in workspace), + "blank fixed iterate roles") + current.bill = following.bill = bill + scale = 1 << p.bits + # First term z_1=trunc_q(x/a); no E row is needed for this term. + for _ in range(length): + x = get_complex(source, p.data_width) + need(abs(x[0]) + abs(x[1]) <= p.radius * scale, "actual incoming radius") + z = tuple(trunc(v, 1 << p.normalizer_shift) for v in x) + put_complex(current, z, p.data_width) + bill.roundings += 2; bill.source_shifts += 2; bill.control_steps += 1 + bill.scalar(*x, *z) + source.rewind(); current.rewind() + active_lower, active_length = lower, length + for _ in range(1, p.terms): + out_lower, out_length = active_lower + p.halfwidth, active_length - 2 * p.halfwidth + source.walk((out_lower - lower) * record_bits) + page.tape.walk((out_lower - lower) * p.band * p.coefficient_width) + for row in range(out_length): + x = get_complex(source, p.data_width) + real = x[0] << (p.bits - p.normalizer_shift) + imag = x[1] << (p.bits - p.normalizer_shift) + bill.source_shifts += 2 + for _ in range(p.band): + coefficient = get_int(page.tape, p.coefficient_width) + z = get_complex(current, p.data_width) + product_real, product_imag = coefficient * z[0], coefficient * z[1] + real += product_real; imag += product_imag + bill.products += 2; bill.additions += 2; bill.control_steps += 1 + bill.scalar(coefficient, *z, product_real, product_imag, real, imag) + need(abs(real) + abs(imag) <= p.radius * scale * scale, + "partial exact accumulator radius") + result = trunc(real, scale), trunc(imag, scale) + need(abs(result[0]) + abs(result[1]) <= p.radius * scale, + "actual rounded iterate radius") + put_complex(following, result, p.data_width) + bill.roundings += 2; bill.control_steps += 1 + if row + 1 < out_length: + current.walk(-2 * p.halfwidth * record_bits) + need(current.head == active_length * record_bits, "complete neighbor-window traversal") + source.rewind(); page.tape.rewind() + current.clear(); following.rewind() + current, following = following, current + active_lower, active_length = out_lower, out_length + need((active_lower, active_length) == (target_lower, target_length), "target-only return") + need(source.head == page.tape.head == current.head == following.head == 0, + "return origins") + need(following.live_bits == 0, "cleared alternate iterate") + return Output(current, active_lower, active_length, p.data_width, (following,)) + + +def consume(output): + """Caller read, clear and origin restoration; reads only the live prefix. + + An iterate buffer can retain a larger previously occupied blank suffix. + The complete live body is cleared; the suffix is blank by invariant. + """ + need(output.tape.head == 0, "output origin") + result = tuple(get_complex(output.tape, output.width) for _ in range(output.length)) + output.tape.clear() + need(output.tape.head == 0 and output.tape.live_bits == 0, "consumed output cleanup") + return result + + +def tape_digest(tape): + return sha256(tape.snapshot()).hexdigest() diff --git a/research/shrinking-reference-halo/independent_inverse.py b/research/shrinking-reference-halo/independent_inverse.py new file mode 100644 index 0000000000..81f2729b24 --- /dev/null +++ b/research/shrinking-reference-halo/independent_inverse.py @@ -0,0 +1,147 @@ +"""Independent exact inverse-row check of the physical tensor consumer. + +The oracle solves the original rational matrix by Gaussian elimination; +it does not evaluate a Neumann polynomial or a Horner recurrence. +""" +from fractions import Fraction as F +from hashlib import sha256 +import importlib.util +import itertools +import json +from pathlib import Path +import random +import sys + +PACKAGE = Path(__file__).resolve().parent + + +def load(name, file): + spec = importlib.util.spec_from_file_location(name, file) + module = importlib.util.module_from_spec(spec) + sys.modules[name] = module + spec.loader.exec_module(module) + return module + + +def inverse_rows(matrix, which): + """Solve H^T v=e_r, with exact rational elimination and residual checks.""" + n = len(matrix) + targets = tuple(sorted(set(which))) + a = [[matrix[j][i] for j in range(n)] + + [F(int(i == r)) for r in targets] for i in range(n)] + for column in range(n): + pivot = next(r for r in range(column, n) if a[r][column]) + a[column], a[pivot] = a[pivot], a[column] + divisor = a[column][column] + a[column] = [v / divisor for v in a[column]] + for row in range(column + 1, n): + factor = a[row][column] + if factor: + a[row] = [x - factor * y for x, y in zip(a[row], a[column])] + result = {} + for index, target in enumerate(targets): + row = [F(0)] * n + for r in range(n - 1, -1, -1): + row[r] = a[r][n + index] - sum(a[r][j] * row[j] for j in range(r + 1, n)) + for c in range(n): + if sum(row[j] * matrix[j][c] for j in range(n)) != int(c == target): + raise AssertionError('exact inverse-row residual') + result[target] = row + return result + + +def main(): + engine = load('shrinking_halo_engine', PACKAGE / 'engine.py') + tensor = load('lead_tensor', PACKAGE / 'tensor.py') + source = load('lead_source', PACKAGE / 'source.py') + raw = source.authenticated_inputs(PACKAGE) + reference = source.make_reference(raw, (32, 8, 2, 1, 8, 32)) + reference.require_narrow_gap() + n = reference.target_size + matrix = [[reference.entry('narrow', r, c).value for c in range(n)] for r in range(n)] + rho = max(sum(abs(F(int(r == c)) - matrix[r][c]) for c in range(n)) for r in range(n)) + gap = F(int((1 - rho) * (1 << 16)), 1 << 16) + shift = 0 + while (1 << shift) * gap < 1: + shift += 1 + plan = engine.Plan(n, 2 * reference.spec.source_halfwidth + 2, 28, 4, shift, gap) + targets = ((-3, 2), (39, 2)) + rows = inverse_rows(matrix, [x % n for lo, count in targets for x in range(lo, lo + count)]) + scale = 1 << plan.bits + rng = random.Random(2026110875) + values = [[(rng.randrange(-8, 9) * (scale // 32), + rng.randrange(-8, 9) * (scale // 32)) for _ in range(n)] for _ in range(n)] + exact = {} + for r, s in itertools.product(*(range(lo, lo + count) for lo, count in targets)): + exact[r, s] = tuple( + sum(rows[r % n][u] * sum(rows[s % n][v] * values[u][v][part] + for v in range(n)) for u in range(n)) / + (scale * (1 << (2 * shift))) for part in (0, 1)) + bill = engine.Bill() + production = source.make_reference(raw, (32, 8, 2, 1, 8, 32)) + + def prepared(): + for _ in range(2): + table, _ = engine.prepare_table( + plan, lambda r, c: source.source_entry(production, r, c), + production.description_hash, bill) + yield table + + archive = tensor.pack_tables(prepared(), bill) + before_archive = engine.tape_digest(archive.tape) + pool = tensor.TensorWorkspace.create(bill) + role_ids = tuple(map(id, pool.roles)) + original_init = engine.Tape.__init__ + + def no_new_tapes(*_args, **_kwargs): + raise AssertionError('new physical role during tensor work or reuse') + + engine.Tape.__init__ = no_new_tapes + observations = [] + outputs = [] + try: + for target in (targets, ((-3, 1), (39, 1))): + layout = tensor.Layout.make(archive.plans, target) + payloads = (values[u % n][v % n] for u, v in itertools.product( + *(range(lo, lo + count) for lo, count in zip(layout.lowers, layout.lengths)))) + incoming = tensor.rectangle_input(layout, payloads, bill, tape=pool.rectangles[0]) + result = tensor.apply_tensor(archive, target, incoming, bill, workspace=pool) + outputs.append(dict(tensor.consume_tensor(result))) + observations.append({'saved_records': layout.volume, 'target_records': result.count, + 'retained_bits': sum(t.extent for t in pool.roles)}) + if tuple(map(id, pool.roles)) != role_ids: + raise AssertionError('workspace roles changed') + if not all(t.head == 0 and t.live_bits == 0 and not any(t.snapshot()) for t in pool.roles): + raise AssertionError('nonblank workspace after return') + if engine.tape_digest(archive.tape) != before_archive or archive.tape.head: + raise AssertionError('borrowed archive changed') + finally: + engine.Tape.__init__ = original_init + bound = 2 * (plan.numeric_error + plan.tail_error) + errors = {} + for key, actual in outputs[0].items(): + error = sum(abs(F(actual[p], scale) - exact[key][p]) for p in (0, 1)) + if error > bound: + raise AssertionError(('exact original tensor inverse', key, str(error), str(bound))) + errors[key] = error + if outputs[1][(-3, 39)] != outputs[0][(-3, 39)]: + raise AssertionError('nested-target or retained-history dependence') + actual = outputs[0][(-3, 39)] + wrong = sum(abs(F(actual[p], scale) - exact[(-2, 40)][p]) for p in (0, 1)) + if wrong <= bound: + raise AssertionError('wrong canonical target key not distinguished') + print('PASS_LEAD_EXACT_TENSOR_INVERSE') + print(json.dumps({'period': n, 'original_entries': n * n, + 'exact_inverse_rows': sorted(rows), 'checked_outputs': len(outputs[0]), + 'maximum_inverse_error': float(max(errors.values())), + 'proved_inverse_error_bound': float(bound), + 'wrong_target_error': float(wrong), + 'fixed_tape_roles': len(pool.roles), 'runs': observations, + 'actual_bit_actions': bill.reads + bill.writes + bill.moves, + 'source_entries': len(production.entries), + 'sha256': {p: sha256((PACKAGE / p).read_bytes()).hexdigest() + for p in ('engine.py', 'tensor.py', 'source.py')}}, sort_keys=True)) + + +if __name__ == '__main__': + main() diff --git a/research/shrinking-reference-halo/independent_residual.py b/research/shrinking-reference-halo/independent_residual.py new file mode 100644 index 0000000000..e68b361a43 --- /dev/null +++ b/research/shrinking-reference-halo/independent_residual.py @@ -0,0 +1,91 @@ +"""Independent residual certification of the actual Gaussian consumer. + +Uses the author's numerical consumer, but no author's verifier or expected +outputs. The mathematical oracle is an exact original-reference residual. +""" +from fractions import Fraction as F +from hashlib import sha256 +import importlib.util +import json +from pathlib import Path +import random +import sys + +PACKAGE = Path(__file__).resolve().parent + + +def load(name, file): + spec = importlib.util.spec_from_file_location(name, file) + module = importlib.util.module_from_spec(spec) + sys.modules[name] = module + spec.loader.exec_module(module) + return module + + +def main(): + engine = load('lead_halo_engine', PACKAGE/'engine.py') + source = load('lead_halo_source', PACKAGE/'source.py') + raw = source.authenticated_inputs(PACKAGE) + reference = source.make_reference(raw, (32,8,2,1,8,32)) + reference.require_narrow_gap() + n = reference.target_size + H = [[reference.entry('narrow',r,c).value for c in range(n)] for r in range(n)] + E = [[F(int(r==c))-H[r][c] for c in range(n)] for r in range(n)] + rho = max(sum(map(abs,row)) for row in E) + gap = F(int((1-rho)*(1<<16)),1<<16) + shift = 0 + while (1<", + "exec", optimize=0), module.__dict__) + return module + + +def reference_class(raw): + """Rebind only imports, leaving every executed numerical body unchanged. + + gaussian.py also imports a full circuit compiler unused by Reference's + explicit constructor/entry interface. Extract exactly its three named + helpers; no numerical source expression or loop is changed. for_cap is + outside this adapter's domain and is not invoked. + """ + exact_tree = ast.parse(raw[EXACT]) + exact = _module("_shrinking_source_exact", exact_tree.body) + gaussian_tree = ast.parse(raw[GAUSSIAN]) + wanted = {"rational", "load_intervals"} + helpers = [node for node in gaussian_tree.body + if isinstance(node, ast.FunctionDef) and node.name in wanted] + need({node.name for node in helpers} == wanted, "retained Gaussian helper shape") + gaussian = _module("_shrinking_source_gaussian", helpers, + {"Q": Q, "need": need, "sha256": sha256, "sys": sys, + "ModuleType": ModuleType}) + tree = ast.parse(raw[REFERENCE]) + body = [node for node in tree.body if not ( + isinstance(node, ast.ImportFrom) and node.module in ("exact", "gaussian"))] + reference = _module("_shrinking_source_reference", body, + {"Mat": exact.Mat, "ceil_log2": exact.ceil_log2, + "need": exact.need, "INTERVALS": INTERVALS, + "load_intervals": gaussian.load_intervals, + "rational": gaussian.rational}) + return reference.Reference + + +def make_reference(raw, parameters): + return reference_class(raw)(raw, *parameters) + + +def source_entry(reference, row, column): + return Q(int(row == column)) - reference.entry("narrow", row, column).value + + +def source_receipt(reference): + """Diagnostic setup inventory; not an asserted exact Python heap count.""" + values = [entry.value for entry in reference.entries.values()] + weight_values = [value for receipt in reference.weights.values() + for value in receipt.values() if type(value) is Q] + height = max([1] + [max(abs(x.numerator).bit_length(), x.denominator.bit_length()) + for x in values + weight_values]) + return dict(reference_sha256=reference.description_hash, + parameters=list(reference.spec.__dict__.values()), + stored_entries=len(reference.entries), stored_weights=len(reference.weights), + stored_kernels=len(reference.kernel), maximum_rational_height=height, + weight_precision=reference.weight_precision, + kernel_error_bits=reference.kernel_error_bits) + + +def clear_reference(reference): + """Release setup caches; physical erasure is separately charged in proof. + + This does not claim secure zeroization of Python immutable integers. + """ + reference.entries.clear(); reference.weights.clear(); reference.kernel.clear() + for name in ("pi_interval", "root_of_unity"): + function = getattr(reference.exp.oracle, name, None) + if function is not None and hasattr(function, "cache_clear"): + function.cache_clear() diff --git a/research/shrinking-reference-halo/tensor.py b/research/shrinking-reference-halo/tensor.py new file mode 100644 index 0000000000..40e84c41bf --- /dev/null +++ b/research/shrinking-reference-halo/tensor.py @@ -0,0 +1,343 @@ +"""One local sparse rectangle on a fixed pool of sequential tape roles. + +Prepared for @CubeJerry with substantial OpenAI Codex assistance. Apache-2.0. +The full-source gather and the final dense unique-return merge are separate. +""" +from dataclasses import dataclass +import shrinking_halo_engine as M + + +def put_unsigned(tape, value, width): + M.need(type(value) is int and 0 <= value < (1 << width), "unsigned key carrier") + for shift in range(width - 1, -1, -1): + tape.write((value >> shift) & 1); tape.step(1) + + +def get_unsigned(tape, width): + value = 0 + for _ in range(width): + value = 2 * value + tape.read(); tape.step(1) + return value + + +@dataclass(frozen=True) +class Archive: + tape: M.Tape + plans: tuple + source_ids: tuple + + +def pack_tables(tables, bill): + """Consume one prepared axis table at a time into ONE protected archive. + + A generator is sufficient: no simultaneous family of physical axis tapes + is required. Each old table body is erased before advancing the iterator. + The finite tuple of descriptors is charged as an encoded control block. + """ + archive = M.Tape(bill, "global band archive") + plans, source_ids = [], [] + bits = None + for table in tables: + if bits is None: + bits = table.plan.bits + M.need(table.plan.bits == bits and table.tape.head == 0, "common archive grid/origin") + table.tape.bill = bill + for _ in range(table.plan.period * table.plan.band): + coefficient = M.get_int(table.tape, table.plan.coefficient_width) + M.put_int(archive, coefficient, table.plan.coefficient_width) + bill.control_steps += 1 + table.tape.readonly = False; table.tape.clear() + plans.append(table.plan); source_ids.append(table.source_id) + M.need(plans, "nonempty band archive") + archive.rewind(); archive.readonly = True + return Archive(archive, tuple(plans), tuple(source_ids)) + + +def archive_page(archive, axis, lower, length, page_tape, bill): + """One/two full ARCHIVE scans per local axis, never per spectator line.""" + M.need(type(axis) is int and 0 <= axis < len(archive.plans), "archive axis") + p = archive.plans[axis] + M.need(type(lower) is int and type(length) is int and 0 < length < p.period, + "nonaliasing local page") + M.need(archive.tape.head == 0 and archive.tape.readonly, "protected archive origin") + M.need(page_tape.head == 0 and not page_tape.readonly and page_tape.live_bits == 0, + "reusable blank local page") + archive.tape.bill = page_tape.bill = bill + begin = lower % p.period + first = min(length, p.period - begin) + spans = [(begin, begin + first)] + if first < length: + spans.append((0, length - first)) + for begin, end in spans: + for catalog_axis, pp in enumerate(archive.plans): + for row in range(pp.period): + emit = catalog_axis == axis and begin <= row < end + for _ in range(pp.band): + coefficient = M.get_int(archive.tape, pp.coefficient_width) + if emit: + M.put_int(page_tape, coefficient, pp.coefficient_width) + bill.control_steps += pp.band + 1 + archive.tape.rewind(); bill.page_scans += 1 + M.need(page_tape.live_bits == length * p.band * p.coefficient_width, "complete local page") + page_tape.rewind(); page_tape.readonly = True + return M.Page(page_tape, p, lower, length, archive.source_ids[axis]) + + +@dataclass(frozen=True) +class Layout: + targets: tuple + lowers: tuple + lengths: tuple + field_widths: tuple + field_shifts: tuple + key_width: int + data_width: int + bits: int + radius: int + + @classmethod + def make(cls, plans, targets): + M.need(len(plans) == len(targets) and plans, "complete tensor axis metadata") + bits, radius = plans[0].bits, plans[0].radius + M.need(all(p.bits == bits and p.radius == radius for p in plans), + "one incoming/output tensor grid and radius") + lowers, lengths, widths = [], [], [] + for p, target in zip(plans, targets): + M.need(type(target) is tuple and len(target) == 2 and + all(type(x) is int for x in target) and target[1] > 0, "target axis interval") + lo, length = target[0] - p.halo, target[1] + 2 * p.halo + M.need(length < p.period, "each saved axis has unique canonical coordinates") + lowers.append(lo); lengths.append(length); widths.append(max(1, (length - 1).bit_length())) + shifts, total = [0] * len(plans), 0 + for i in range(len(plans) - 1, -1, -1): + shifts[i] = total; total += widths[i] + return cls(tuple(targets), tuple(lowers), tuple(lengths), tuple(widths), tuple(shifts), + total, plans[0].data_width, bits, radius) + + @property + def record_bits(self): + return self.key_width + 2 * self.data_width + + @property + def volume(self): + result = 1 + for length in self.lengths: + result *= length + return result + + def key(self, offsets): + M.need(len(offsets) == len(self.lengths), "complete coordinate tuple") + key = 0 + for offset, length, shift in zip(offsets, self.lengths, self.field_shifts): + M.need(type(offset) is int and 0 <= offset < length, "local coordinate range") + key += offset << shift + return key + + def coordinate(self, key, axis): + return (key >> self.field_shifts[axis]) & ((1 << self.field_widths[axis]) - 1) + + def without_axis(self, key, axis): + mask = ((1 << self.field_widths[axis]) - 1) << self.field_shifts[axis] + return key & ~mask + + +def put_record(tape, key, value, layout): + put_unsigned(tape, key, layout.key_width) + M.put_complex(tape, value, layout.data_width) + + +def get_record(tape, layout): + return get_unsigned(tape, layout.key_width), M.get_complex(tape, layout.data_width) + + +def coordinate_odometer(lengths): + """Metadata convenience; encoded carries are explicitly charged in proof.""" + coordinate = [0] * len(lengths) + while True: + yield tuple(coordinate) + axis = len(lengths) - 1 + while axis >= 0 and coordinate[axis] + 1 == lengths[axis]: + coordinate[axis] = 0; axis -= 1 + if axis < 0: + return + coordinate[axis] += 1 + + +def rectangle_input(layout, values, bill, tape=None): + """Charged codec from lexicographic payload stream, no indexed data lookup.""" + tape = tape if tape is not None else M.Tape(bill, "rectangle current") + M.need(tape.head == 0 and tape.live_bits == 0 and not tape.readonly, "blank reusable rectangle role") + tape.bill = bill + stream = iter(values) + for offsets in coordinate_odometer(layout.lengths): + try: + value = next(stream) + except StopIteration as error: + raise ValueError("incomplete saved rectangle") from error + M.need(type(value) is tuple and len(value) == 2 and all(type(x) is int for x in value) + and abs(value[0]) + abs(value[1]) <= layout.radius * (1 << layout.bits), + "saved rectangle data/radius") + put_record(tape, layout.key(offsets), value, layout) + bill.control_steps += len(layout.lengths) + 1 + try: + next(stream) + except StopIteration: + pass + else: + raise ValueError("extra saved rectangle payload") + tape.rewind() + return tape + + +def expose_axis(current, count, axis, layout, buckets, bill): + """Stable LSD distribution into two fixed buckets, then full concatenation.""" + M.need(current.head == 0 and not current.readonly, "owned rectangle origin") + M.need(current.live_bits == count * layout.record_bits, "complete sparse body") + order = (axis,) + tuple(j for j in range(len(layout.lengths) - 1, -1, -1) if j != axis) + passes = 0 + for field in order: + for bit in range(layout.field_widths[field]): + M.need(all(t.head == 0 and t.live_bits == 0 for t in buckets), + "blank fixed radix buckets") + sizes = [0, 0] + position = layout.field_shifts[field] + bit + for _ in range(count): + key, value = get_record(current, layout) + destination = (key >> position) & 1 + put_record(buckets[destination], key, value, layout) + sizes[destination] += 1 + bill.control_steps += 1 + current.clear() + for bucket, size in zip(buckets, sizes): + bucket.rewind() + for _ in range(size): + key, value = get_record(bucket, layout) + put_record(current, key, value, layout) + bill.control_steps += 1 + bucket.clear() + current.rewind(); passes += 1 + return passes + + +@dataclass(frozen=True) +class TensorOutput: + tape: M.Tape + count: int + layout: Layout + role_extents: tuple + axis_receipts: tuple + blank_roles: tuple + + +@dataclass(frozen=True) +class TensorWorkspace: + rectangles: tuple + buckets: tuple + line_source: M.Tape + iterates: tuple + page: M.Tape + + @classmethod + def create(cls, bill, first_rectangle=None): + first = first_rectangle if first_rectangle is not None else M.Tape(bill, "rectangle current") + return cls((first, M.Tape(bill, "rectangle next")), + (M.Tape(bill, "radix zero"), M.Tape(bill, "radix one")), + M.Tape(bill, "fixed borrowed line"), + (M.Tape(bill, "fixed iterate zero"), M.Tape(bill, "fixed iterate one")), + M.Tape(bill, "fixed local band page")) + + @property + def roles(self): + return self.rectangles + self.buckets + (self.line_source,) + self.iterates + (self.page,) + + +def apply_tensor(archive, targets, source, bill, workspace=None): + """Consume one saved rectangle; return its complete target in lex order. + + There are eight local tape roles, independent of axis count and iteration + count, plus the one protected global archive and bounded scalar/control + tapes. No source/table preparation is repeated inside a spectator line. + """ + layout = Layout.make(archive.plans, targets) + M.need(source.head == 0 and not source.readonly + and source.live_bits == layout.volume * layout.record_bits, "owned complete rectangle") + pool = workspace if workspace is not None else TensorWorkspace.create(bill, source) + roles = pool.roles + M.need(len({id(t) for t in roles}) == 8 and any(t is source for t in pool.rectangles), + "eight distinct fixed roles with designated input") + M.need(all(t is source or (t.head == 0 and t.live_bits == 0 and not t.readonly) for t in roles), + "all noninput fixed roles blank and reusable") + for tape in roles: + tape.bill = bill + current = source + following = pool.rectangles[1] if source is pool.rectangles[0] else pool.rectangles[0] + buckets, line_source, iterates, page_tape = pool.buckets, pool.line_source, pool.iterates, pool.page + count = layout.volume + receipts = [] + for axis, p in enumerate(archive.plans): + start_products, start_scans = bill.products, bill.page_scans + page = archive_page(archive, axis, layout.lowers[axis], layout.lengths[axis], page_tape, bill) + passes = expose_axis(current, count, axis, layout, buckets, bill) + line_length = layout.lengths[axis] + M.need(count % line_length == 0, "complete spectator lines") + lines = count // line_length + target_lower, target_length = layout.targets[axis] + previous_spectator = -1 + for _ in range(lines): + spectator = None + for position in range(line_length): + key, value = get_record(current, layout) + other = layout.without_axis(key, axis) + if spectator is None: + spectator = other + M.need(spectator > previous_spectator, "unique ordered spectator line") + previous_spectator = spectator + M.need(other == spectator and layout.coordinate(key, axis) == position, + "full ordered local dependency line") + M.put_complex(line_source, value, p.data_width) + bill.control_steps += len(layout.lengths) + 1 + line_source.rewind(); line_source.readonly = True + output = M.apply_line(page, line_source, target_lower, target_length, bill, + workspace=iterates) + for offset in range(target_length): + value = M.get_complex(output.tape, p.data_width) + coordinate = target_lower - layout.lowers[axis] + offset + key = spectator | (coordinate << layout.field_shifts[axis]) + put_record(following, key, value, layout) + bill.control_steps += len(layout.lengths) + 1 + output.tape.clear() + line_source.readonly = False; line_source.clear() + current.clear(); following.rewind() + current, following = following, current + page_tape.readonly = False; page_tape.clear() + count = lines * target_length + M.need(current.live_bits == count * layout.record_bits, "exact next tensor rectangle") + receipts.append(dict(axis=axis, input_lines=lines, line_length=line_length, + target_length=target_length, radix_passes=passes, + page_scans=bill.page_scans - start_scans, + products=bill.products - start_products, output_records=count)) + blank = tuple(t for t in roles if t is not current) + M.need(all(t.head == 0 and t.live_bits == 0 for t in blank), + "all nonreturn fixed roles erased") + M.need(current.head == archive.tape.head == 0, "tensor/archive return origins") + return TensorOutput(current, count, layout, + tuple((t.name, t.extent) for t in roles), tuple(receipts), blank) + + +def consume_tensor(output): + """Return lifted coordinates, payloads; consume and clear the live output.""" + layout = output.layout + result = [] + previous = -1 + for _ in range(output.count): + key, value = get_record(output.tape, layout) + M.need(key > previous, "unique lexicographic target key") + previous = key + coordinates = tuple(layout.lowers[i] + layout.coordinate(key, i) + for i in range(len(layout.lengths))) + M.need(all(lo <= x < lo + length for x, (lo, length) in zip(coordinates, layout.targets)), + "target-only tensor output") + result.append((coordinates, value)) + output.tape.clear() + M.need(output.tape.head == 0 and output.tape.live_bits == 0, "tensor return cleanup") + return tuple(result) diff --git a/research/shrinking-reference-halo/verify.py b/research/shrinking-reference-halo/verify.py new file mode 100644 index 0000000000..bde34700a9 --- /dev/null +++ b/research/shrinking-reference-halo/verify.py @@ -0,0 +1,554 @@ +"""Exact, read-only normal/optimized corroboration of the scoped theorem. + +Prepared for @CubeJerry with substantial OpenAI Codex assistance. Apache-2.0. +The dense polynomial oracle forms separate powers, not the online recurrence. +""" +import argparse +from dataclasses import replace +from fractions import Fraction as Q +from hashlib import sha256 +import importlib.util +import itertools +import json +from pathlib import Path +import random +import sys +import types + +PACKAGE = Path(__file__).resolve().parent + + +def load_local(name, path): + spec = importlib.util.spec_from_file_location(name, path) + module = importlib.util.module_from_spec(spec) + sys.modules[name] = module + spec.loader.exec_module(module) + return module + + +M = load_local("shrinking_halo_engine", PACKAGE / "engine.py") +S = load_local("shrinking_halo_source", PACKAGE / "source.py") +T = load_local("shrinking_halo_tensor", PACKAGE / "tensor.py") + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def rejected(function, label): + try: + function() + except (ValueError, IndexError): + return label + raise ValueError("negative control accepted: " + label) + + +def pair_norm(value): + return abs(value[0]) + abs(value[1]) + + +def dense_polynomial(matrix, data, terms, normalizer): + """Independent exact mechanism: explicit successive powers and sum.""" + n = len(data) + power = tuple((Q(z[0]), Q(z[1])) for z in data) + total = [list(z) for z in power] + for _ in range(1, terms): + following = [] + for row in range(n): + following.append(tuple(sum((matrix[row][column] * power[column][part] + for column in range(n)), Q(0)) + for part in (0, 1))) + power = tuple(following) + for row in range(n): + for part in (0, 1): + total[row][part] += power[row][part] + return tuple(tuple(value / normalizer for value in z) for z in total) + + +def rounded_global(matrix, data, plan): + """Full-period host comparator, solely to verify exact rounded conformance.""" + n, scale = len(data), 1 << plan.bits + coefficients = [[M.inward(value, plan.bits) for value in row] for row in matrix] + current = [(0, 0)] * n + for _ in range(plan.terms): + current = [tuple(M.trunc((data[row][part] << (plan.bits - plan.normalizer_shift)) + + sum(coefficients[row][column] * current[column][part] + for column in range(n)), scale) + for part in (0, 1)) for row in range(n)] + return tuple(current) + + +def run_line(matrix, data, plan, lower, length, engine=M, table=None, bill=None): + bill = bill or engine.Bill() + table = table or engine.prepare_table(plan, lambda r, c: matrix[r][c], "finite exact E", bill)[0] + before_table = engine.tape_digest(table.tape) + saved_lower, saved_length = lower - plan.halo, length + 2 * plan.halo + page = engine.extract_page(table, saved_lower, saved_length, bill) + values = tuple(data[row % plan.period] for row in range(saved_lower, saved_lower + saved_length)) + source = engine.input_tape(plan, values, bill) + before_source, before_page = engine.tape_digest(source), engine.tape_digest(page.tape) + output = engine.apply_line(page, source, lower, length, bill) + require(output.tape.head == 0 and output.length == length, "owned exact output extent") + physical_extents = (source.extent, page.tape.extent, output.tape.extent, + sum(t.extent for t in output.blank_scratch)) + actual = engine.consume(output) + require(before_source == engine.tape_digest(source) and source.head == 0, + "borrowed input bytes/origin") + require(before_page == engine.tape_digest(page.tape) and page.tape.head == 0, + "borrowed page bytes/origin") + require(before_table == engine.tape_digest(table.tape) and table.tape.head == 0, + "global table bytes/origin") + require(all(t.head == 0 and not any(t.snapshot()) for t in output.blank_scratch), + "alternate backing cleanup") + expected = rounded_global(matrix, data, plan) + require(actual == tuple(expected[row % plan.period] for row in range(lower, lower + length)), + "exact full-period rounded conformance") + rational_data = tuple(tuple(Q(v, 1 << plan.bits) for v in z) for z in data) + exact = dense_polynomial(matrix, rational_data, plan.terms, 1 << plan.normalizer_shift) + error = max(pair_norm(tuple(Q(actual[j][part], 1 << plan.bits) - + exact[(lower + j) % plan.period][part] for part in (0, 1))) + for j in range(length)) + require(error <= plan.numeric_error, "proved coefficient/data bound") + n0 = saved_length + output_counts = [length + 2 * (plan.terms - k) * plan.halfwidth + for k in range(2, plan.terms + 1)] + expected_products = 2 * plan.band * sum(output_counts) + expected_roundings = 2 * (n0 + sum(output_counts)) + require(bill.products == expected_products, "complete multiply invoice") + require(bill.additions == expected_products, "complete accumulation invoice") + require(bill.roundings == expected_roundings, "all completed data roundings") + return actual, error, bill, physical_extents + + +def matrix_cases(): + rng = random.Random(72) + cases = [] + for case in range(32): + width = 1 + case % 2 + terms = 1 + case % 4 + n = 2 * (terms - 1) * width + 15 + case % 5 + gap = Q(1 + case % 3, 8) + bits = 9 + case % 4 + shift = 0 + while (1 << shift) * gap < 1: + shift += 1 + plan = M.Plan(n, width, bits, terms, shift, gap) + matrix = [[Q(0) for _ in range(n)] for _ in range(n)] + holes = {n // 2} + for row in range(n): + if row in holes: + continue + support = [((row + offset) % n, rng.choice((-1, 1)), rng.randint(1, 7)) + for offset in range(-width, width + 1) + if offset and (row + offset) % n not in holes] + denominator = sum(weight for _, _, weight in support) + for column, sign, weight in support: + matrix[row][column] = sign * (1 - gap) * Q(weight, denominator) + data = [] + for _ in range(n): + real = rng.randint(-(1 << bits), 1 << bits) + imag = rng.randint(-((1 << bits) - abs(real)), (1 << bits) - abs(real)) + data.append((real, imag)) + lower = (-2, n - 3, n // 2 - 1, 1)[case % 4] + cases.append((matrix, tuple(data), plan, lower, 3)) + return cases + + +def finite_cases(): + receipts, nonzero_errors = [], 0 + for matrix, data, plan, lower, length in matrix_cases(): + output, error, bill, extents = run_line(matrix, data, plan, lower, length) + nonzero_errors += int(error > 0) + receipts.append(dict(period=plan.period, width=plan.halfwidth, terms=plan.terms, + bits=plan.bits, lower=lower, length=length, gap=str(plan.gap), + output=list(output), nonzero_error=error > 0, + bill=bill.record(), resident_extents=list(extents))) + require(nonzero_errors >= 24, "nontrivial rounding fixtures") + return receipts, nonzero_errors + + +def tensor_oracle(matrices, plans, data, rounded): + """Full canonical tensor, including coordinates outside every local box.""" + sizes = tuple(p.period for p in plans) + current = dict(data) + if not rounded: + current = {key: tuple(Q(v, 1 << plans[0].bits) for v in z) + for key, z in current.items()} + for axis, (matrix, plan) in enumerate(zip(matrices, plans)): + following = {} + others = tuple(i for i in range(len(plans)) if i != axis) + for spectator in itertools.product(*(range(sizes[i]) for i in others)): + keys = [] + for coordinate in range(sizes[axis]): + key, other = [], 0 + for i in range(len(plans)): + if i == axis: + key.append(coordinate) + else: + key.append(spectator[other]); other += 1 + keys.append(tuple(key)) + line = tuple(current[key] for key in keys) + values = rounded_global(matrix, line, plan) if rounded else dense_polynomial( + matrix, line, plan.terms, 1 << plan.normalizer_shift) + following.update(zip(keys, values)) + current = following + return current + + +def tensor_case(matrices, plans, targets, label, tensor_module=T, entry_services=None, source_ids=None): + bill = M.Bill() + def prepared(): + for axis, (matrix, plan) in enumerate(zip(matrices, plans)): + entry = entry_services[axis] if entry_services is not None else ( + lambda r, c, matrix=matrix: matrix[r][c]) + source_id = source_ids[axis] if source_ids is not None else label + "/axis/" + str(axis) + yield M.prepare_table(plan, entry, source_id, bill)[0] + archive = T.pack_tables(prepared(), bill) + archive_before = M.tape_digest(archive.tape) + layout = T.Layout.make(plans, targets) + scale = 1 << plans[0].bits + full_data = {} + for key in itertools.product(*(range(p.period) for p in plans)): + code = sum((i + 3) * (x + 1) ** 2 for i, x in enumerate(key)) + real = (code * 173 % (scale // 2)) - scale // 4 + imag = (code * 97 % (scale // 3)) - scale // 6 + full_data[key] = real, imag + def local_values(): + for offsets in T.coordinate_odometer(layout.lengths): + canonical = tuple((lo + x) % p.period for lo, x, p in zip(layout.lowers, offsets, plans)) + yield full_data[canonical] + source = T.rectangle_input(layout, local_values(), bill) + start_products, start_scans = bill.products, bill.page_scans + output = tensor_module.apply_tensor(archive, targets, source, bill) + values = tensor_module.consume_tensor(output) + require(archive_before == M.tape_digest(archive.tape) and archive.tape.head == 0, + "tensor preserves global source archive") + exact = tensor_oracle(matrices, plans, full_data, rounded=False) + rounded = tensor_oracle(matrices, plans, full_data, rounded=True) + errors = [] + for key, value in values: + canonical = tuple(x % p.period for x, p in zip(key, plans)) + require(value == rounded[canonical], "full rounded tensor equality") + errors.append(pair_norm(tuple(Q(value[part], scale) - exact[canonical][part] + for part in (0, 1)))) + error = max(errors) + require(error <= sum(p.numeric_error for p in plans), "complete normalized tensor bound") + require(error > 0, "nonzero tensor rounding defect") + expected_count = 1 + for _, length in targets: + expected_count *= length + require(len(values) == expected_count, "complete target tensor") + require(len(output.role_extents) == 8, "fixed local physical role count") + products, scans, live_count = 0, 0, layout.volume + for axis, (plan, target, receipt) in enumerate(zip(plans, targets, output.axis_receipts)): + lines = live_count // layout.lengths[axis] + n = target[1] + per_line = 2 * plan.band * ((plan.terms - 1) * n + + plan.halfwidth * (plan.terms - 1) * (plan.terms - 2)) + require(receipt["products"] == lines * per_line, "tensor complete product invoice") + expected_scans = 1 + int((layout.lowers[axis] % plan.period) + layout.lengths[axis] > plan.period) + require(receipt["page_scans"] == expected_scans, "one page production per axis, not per line") + require(receipt["radix_passes"] == layout.key_width, "complete sparse radix exposure") + products += lines * per_line; scans += expected_scans + live_count = lines * n + require(bill.products - start_products == products and bill.page_scans - start_scans == scans, + "complete tensor invoice totals") + return dict(label=label, dimensions=len(plans), saved_lengths=list(layout.lengths), + copied_records=layout.volume, target_records=len(values), + key_width=layout.key_width, fixed_local_tape_roles=8, + role_extents=list(output.role_extents), total_retained_local_bits=sum(n for _, n in output.role_extents), + protected_archive_bits=archive.tape.extent, axis_receipts=list(output.axis_receipts), + output=list(values), numerical_bound=str(sum(p.numeric_error for p in plans)), + nonzero_error=True, bill=bill.record()) + + +def synthetic_tensors(tensor_module=T): + result = [] + for dimensions in (2, 3): + matrices, plans, targets = [], [], [] + for axis in range(dimensions): + n, width, terms = 11, 1, 2 + axis % 2 + gap = Q(axis + 2, 8) + plan = M.Plan(n, width, 10, terms, 2, gap) + matrix = [[Q(0) for _ in range(n)] for _ in range(n)] + for row in range(n): + if row == n // 2: + continue + for offset in (-1, 1): + column = (row + offset) % n + if column != n // 2: + matrix[row][column] = (-1 if (row + axis + offset) % 2 else 1) * (1 - gap) / 2 + matrices.append(matrix); plans.append(plan) + targets.append((-1 if axis % 2 == 0 else n - 2, 2)) + result.append(tensor_case(tuple(matrices), tuple(plans), tuple(targets), + "signed-" + str(dimensions) + "d", tensor_module)) + return result + + +def reuse_history(engine=M): + """Long line, short face, long line on exactly the same physical roles.""" + bill = engine.Bill() + plan = engine.Plan(101, 1, 12, 3, 1, Q(1, 2)) + matrix = [[Q(1, 4) if (c-r) % 101 in (1, 100) else Q(0) + for c in range(101)] for r in range(101)] + data = tuple(((r * 73) % 2048 - 1024, (r * 31) % 1024 - 512) for r in range(101)) + table, _ = engine.prepare_table(plan, lambda r, c: matrix[r][c], "reused source", bill) + page_role = engine.Tape(bill, "reused page") + source_role = engine.Tape(bill, "reused source") + iterates = (engine.Tape(bill, "reused iterate 0"), engine.Tape(bill, "reused iterate 1")) + records = [] + exact = rounded_global(matrix, data, plan) + for lower, length in ((2, 37), (50, 1), (70, 37)): + before = bill.record() + page = engine.extract_page(table, lower-plan.halo, length+2*plan.halo, bill, page_role) + for row in range(lower-plan.halo, lower+length+plan.halo): + engine.put_complex(source_role, data[row % 101], plan.data_width) + source_role.rewind(); source_role.readonly = True + output = engine.apply_line(page, source_role, lower, length, bill, workspace=iterates) + values = engine.consume(output) + require(values == tuple(exact[r % 101] for r in range(lower, lower+length)), + "long-short-long exact returned values") + source_role.readonly = False; source_role.clear() + page_role.readonly = False; page_role.clear() + roles = (source_role, page_role) + iterates + require(all(t.head == 0 and t.live_bits == 0 and not any(t.snapshot()) for t in roles), + "long-short-long retained blank suffix invariant") + after = bill.record() + records.append(dict(target_length=length, saved_length=length+2*plan.halo, + output=list(values), retained_bits=sum(t.extent for t in roles), + writes=after["writes"]-before["writes"], + moves=after["moves"]-before["moves"])) + return records + + +def backing_history_control(): + correct = reuse_history() + text = (PACKAGE / "engine.py").read_text() + require(text.count("occupied = self.live_bits") == 1, "unique historical clear site") + module = types.ModuleType("_shrinking_counterfactual_highwater") + sys.modules[module.__name__] = module + exec(compile(text.replace("occupied = self.live_bits", "occupied = self.extent"), + "", "exec"), module.__dict__) + counterfactual = reuse_history(module) + require([x["output"] for x in correct] == [x["output"] for x in counterfactual], + "counterfactual preserves numerical result") + require(counterfactual[1]["writes"] > 3 * correct[1]["writes"], + "historical backing creates a real short-face tariff") + return dict(correct=correct, counterfactual=counterfactual, + retained_extent_ratio="41/5", counterfactual_detected=True) + + +def rectangle_reuse_history(): + bill = M.Bill() + plans = (M.Plan(17, 1, 10, 2, 1, Q(3, 4)), M.Plan(17, 1, 10, 3, 1, Q(7, 8))) + matrices = tuple([[Q((1 if axis == 0 else -1), 8 << axis) + if (c-r) % 17 in (1, 16) and r != 8 and c != 8 else Q(0) + for c in range(17)] for r in range(17)] for axis in range(2)) + def prepared(): + for axis, plan in enumerate(plans): + yield M.prepare_table(plan, lambda r, c, axis=axis: matrices[axis][r][c], + "rectangle reuse axis " + str(axis), bill)[0] + archive = T.pack_tables(prepared(), bill) + workspace = T.TensorWorkspace.create(bill) + role_ids = {id(t) for t in workspace.roles} + data = {key: ((13*key[0]+29*key[1]) % 512-256, (31*key[0]+7*key[1]) % 256-128) + for key in itertools.product(range(17), repeat=2)} + expected = tensor_oracle(matrices, plans, data, rounded=True) + history = [] + original_constructor = M.Tape.__init__ + def forbidden_constructor(*args, **kwargs): + raise ValueError("new tape role inside rectangle reuse history") + M.Tape.__init__ = forbidden_constructor + try: + for targets in (((-1, 7), (4, 5)), ((8, 1), (-1, 2)), ((1, 5), (9, 7))): + layout = T.Layout.make(plans, targets) + values = (data[tuple((lo+x) % 17 for lo, x in zip(layout.lowers, offsets))] + for offsets in T.coordinate_odometer(layout.lengths)) + before = bill.record() + source = T.rectangle_input(layout, values, bill, workspace.rectangles[0]) + output = T.apply_tensor(archive, targets, source, bill, workspace=workspace) + require({id(output.tape)} | {id(t) for t in output.blank_roles} == role_ids, + "same eight roles across completed rectangles") + answer = T.consume_tensor(output) + require(all(value == expected[tuple(x % 17 for x in key)] for key, value in answer), + "long-short-long rectangle exact output") + require(all(t.head == 0 and t.live_bits == 0 and not any(t.snapshot()) + for t in workspace.roles), "reused rectangle complete restoration") + after = bill.record() + history.append(dict(saved_lengths=list(layout.lengths), copied_records=layout.volume, + target_records=len(answer), output=list(answer), + retained_bits=sum(t.extent for t in workspace.roles), + writes=after["writes"]-before["writes"], + moves=after["moves"]-before["moves"], + archive_scans=after["page_scans"]-before["page_scans"])) + finally: + M.Tape.__init__ = original_constructor + return dict(fixed_role_count=8, constructors_sealed_during_calls=True, history=history) + + +def gaussian_cases(raw): + reference = S.make_reference(raw, (32, 8, 2, 1, 8, 32)) + reference.require_narrow_gap() + gap = Q((reference.narrow_gap * (1 << 16)).numerator // + (reference.narrow_gap * (1 << 16)).denominator, 1 << 16) + shift = 0 + while (1 << shift) * gap < 1: + shift += 1 + plan = M.Plan(reference.target_size, 2 * reference.spec.source_halfwidth + 2, + 28, 4, shift, gap) + require(plan.numeric_error + plan.tail_error < Q(1, 1 << 20), + "uniform same-reference inverse target") + prep_bill = M.Bill() + table, height = M.prepare_table(plan, lambda r, c: S.source_entry(reference, r, c), + reference.description_hash, prep_bill) + setup = S.source_receipt(reference) + setup["band_source_calls"] = prep_bill.setup_entries + setup["stored_coefficient_height"] = height + setup["table_bits"] = table.tape.extent + setup["production_bill"] = prep_bill.record() + # All original source entries, not just the producer's asserted band. + matrix = [[S.source_entry(reference, r, c) for c in range(plan.period)] + for r in range(plan.period)] + omissions, wrap_entries = 0, 0 + holes = tuple(reference.holes) + for r in range(plan.period): + for c in range(plan.period): + distance = min((r - c) % plan.period, (c - r) % plan.period) + if distance > plan.halfwidth: + require(matrix[r][c] == 0, "actual complete off-band support") + omissions += 1 + if abs(r - c) > plan.period // 2 and matrix[r][c]: + wrap_entries += 1 + if r in holes or c in holes: + require(matrix[r][c] == 0, "actual identity holes") + require(wrap_entries > 0 and holes, "actual wrap and holes exercised") + scale = 1 << plan.bits + data = tuple(((1 if r % 3 else -1) * (scale // 3 + 17 * r), + (-1 if r % 2 else 1) * (scale // 7 - 11 * r)) + for r in range(plan.period)) + receipts = [] + for lower in (-2, 5, 18): + output, error, bill, extents = run_line(matrix, data, plan, lower, 5, + table=table, bill=M.Bill()) + require(error > 0, "actual source nonzero numerical error") + receipts.append(dict(lower=lower, output=list(output), bill=bill.record(), + resident_extents=list(extents), nonzero_error=True)) + # An executed wrong branch: suppress genuine across-period E entries. + dropped = [[Q(0) if abs(r - c) > plan.period // 2 else matrix[r][c] + for c in range(plan.period)] for r in range(plan.period)] + wrong, _, _, _ = run_line(dropped, data, plan, -2, 5) + require(wrong != tuple(map(tuple, receipts[0]["output"])), "dropped-wrap control discriminates") + # Fresh retained producers, not the dense checker's indexed matrix, supply + # both actual tensor band tables. They share the same immutable spec. + producer_reference = S.make_reference(raw, (32, 8, 2, 1, 8, 32)) + producer = lambda r, c: S.source_entry(producer_reference, r, c) + tensor = tensor_case((matrix, matrix), (plan, plan), ((-1, 4), (5, 3)), "actual-reference-2d", + entry_services=(producer, producer), + source_ids=(producer_reference.description_hash,) * 2) + tensor["source_setup"] = S.source_receipt(producer_reference) + S.clear_reference(producer_reference) + S.clear_reference(reference) + require(not reference.entries and not reference.weights and not reference.kernel, + "setup cache release") + return dict(setup=setup, period=plan.period, gap=str(gap), holes=list(holes), + original_matrix_entries=plan.period ** 2, checked_off_band_entries=omissions, + nonzero_wrap_entries=wrap_entries, target_bits=20, + numerical_bound=str(plan.numeric_error), tail_bound=str(plan.tail_error), + lines=receipts, tensor=tensor, dropped_wrap_detected=True) + + +def negative_controls(): + controls = [] + p = M.Plan(29, 1, 10, 3, 3, Q(1, 8)) + controls.append(rejected(lambda: replace(p, normalizer_shift=2), "unfunded normalization")) + controls.append(rejected(lambda: replace(p, bits=2), "lost normalized-source precision")) + controls.append(rejected(lambda: replace(p, halfwidth=15), "nonunique cyclic offsets")) + controls.append(rejected(lambda: replace(p, gap=0), "missing contraction gap")) + controls.append(rejected(lambda: M.prepare_table(p, lambda r, c: Q(1, 2), + "invalid row", M.Bill()), "bad original row gap")) + controls.append(rejected(lambda: M.input_tape(p, ((1024, 1),), M.Bill()), "oversized actual input")) + table, _ = M.prepare_table(p, lambda r, c: Q(1, 4) if c == (r + 1) % p.period else Q(0), + "control", M.Bill()) + controls.append(rejected(lambda: M.extract_page(table, 0, p.period, M.Bill()), + "repeated canonical page coordinate")) + page = M.extract_page(table, 0, 7, M.Bill()) + source = M.input_tape(p, ((100, -100),) * 7, M.Bill()) + controls.append(rejected(lambda: page.tape.write(1), "immutable coefficient page")) + controls.append(rejected(lambda: source.write(1), "immutable fixed source")) + controls.append(rejected(lambda: M.apply_line(page, source, 3, 3, M.Bill()), + "prematurely cropped dependency interval")) + bad = M.input_tape(p, ((0, 0),) * 7, M.Bill()) + bad.readonly = False; bad.write(1); bad.rewind(); bad.readonly = True + controls.append(rejected(lambda: M.apply_line(page, bad, 2, 3, M.Bill()), + "noncanonical negative zero")) + # Real source-text changes of the consumer, tested against the independent oracle. + text = (PACKAGE / "engine.py").read_text() + mutations = [ + ("real += product_real; imag += product_imag", "real -= product_real; imag -= product_imag", "wrong recurrence sign"), + ("current.walk(-2 * p.halfwidth * record_bits)", "current.walk(-(2 * p.halfwidth + 1) * record_bits)", "wrong neighbor rewind"), + ("current.clear(); following.rewind()", "current.rewind(); following.rewind()", "missing scratch erasure"), + ] + case = matrix_cases()[3] + for old, new, name in mutations: + require(text.count(old) == 1, "unique mutation site") + module = types.ModuleType("_shrinking_mutation_" + str(len(controls))) + sys.modules[module.__name__] = module + exec(compile(text.replace(old, new), "", "exec"), module.__dict__) + # Reconstruct the plan in the mutated module; other data stay exact. + matrix, data, p0, lower, length = case + pp = module.Plan(**p0.__dict__) + controls.append(rejected(lambda: run_line(matrix, data, pp, lower, length, module), name)) + tensor_text = (PACKAGE / "tensor.py").read_text() + for old, new, name in [ + ("order = (axis,) + tuple(j for j in range(len(layout.lengths) - 1, -1, -1) if j != axis)", + "order = tuple(range(len(layout.lengths)))", "wrong sparse axis exposure"), + ("emit = catalog_axis == axis and begin <= row < end", + "emit = catalog_axis == 0 and begin <= row < end", "stale axis coefficient page"), + ("coordinate = target_lower - layout.lowers[axis] + offset", + "coordinate = target_lower - layout.lowers[axis] + offset + 1", "shifted returned tensor key"), + ]: + require(tensor_text.count(old) == 1, "unique tensor mutation site") + module = types.ModuleType("_shrinking_tensor_mutation_" + str(len(controls))) + sys.modules[module.__name__] = module + exec(compile(tensor_text.replace(old, new), "", "exec"), module.__dict__) + controls.append(rejected(lambda: synthetic_tensors(module), name)) + return controls + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument("--write-receipt", action="store_true") + args = parser.parse_args() + raw = S.authenticated_inputs(PACKAGE) + finite, nonzero = finite_cases() + tensors = synthetic_tensors() + gaussian = gaussian_cases(raw) + controls = negative_controls() + history = backing_history_control() + rectangle_history = rectangle_reuse_history() + result = dict(schema_version=1, seed=72, claim="scoped written proof and finite tape corroboration", + no_new_kappa=True, finite_lines=len(finite), finite_target_outputs=3 * len(finite), + nonzero_rounding_lines=nonzero, finite=finite, tensors=tensors, gaussian=gaussian, + controls=controls, control_count=len(controls), + backing_reuse=history, rectangle_reuse=rectangle_history, + program_sha256={name: sha256((PACKAGE/name).read_bytes()).hexdigest() + for name in ("engine.py", "source.py", "tensor.py", "verify.py")}, + source_sha256={path: sha256(content).hexdigest() for path, content in sorted(raw.items())}) + encoded = json.dumps(result, sort_keys=True, indent=2) + "\n" + receipt = PACKAGE / "RESULT.json" + if args.write_receipt: + receipt.write_text(encoded) + else: + require(receipt.is_file(), "mandatory exact receipt") + # Canonical serialization distinguishes booleans from integers recursively. + require(json.dumps(json.loads(receipt.read_text()), sort_keys=True, separators=(",", ":")) == + json.dumps(result, sort_keys=True, separators=(",", ":")), "exact typed receipt") + print("PASS_SHRINKING_REFERENCE_HALO " + json.dumps( + dict(finite_lines=len(finite), gaussian_rows=gaussian["period"], + controls=len(controls), source_entries=gaussian["original_matrix_entries"], + receipt_sha256=sha256(encoded.encode()).hexdigest(), no_new_kappa=True), sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/sparse-halo-tape-transaction/EXPECTED.json b/research/sparse-halo-tape-transaction/EXPECTED.json new file mode 100644 index 0000000000..9b2fe8ab73 --- /dev/null +++ b/research/sparse-halo-tape-transaction/EXPECTED.json @@ -0,0 +1,159 @@ +{ + "arithmetic_pairs": 1364, + "claim": "physical gather/sort/return only; numerical halo consumer is an explicit contract; no new kappa", + "controls": [ + "missing_target", + "duplicate_target", + "kept_row_return", + "core_before_copy", + "return_before_core", + "nonunit_head_jump", + "reversed_bucket_order_detected", + "duplicate_key_stability", + "copy_after_core_detected", + "no_observer_call_in_program" + ], + "fixtures": [ + { + "B": 5, + "C": 16, + "K": 14, + "M": 32, + "Q": 8, + "after_erase": { + "actions": 356848, + "moves": 141644, + "retained_cells": 2077, + "roles": 30 + }, + "before_erase": { + "actions": 350261, + "moves": 138849, + "retained_cells": 2077, + "roles": 30 + }, + "gather": { + "actions": 50995, + "moves": 19768, + "retained_cells": 970, + "roles": 30 + }, + "gather_and_sparse_sort": { + "actions": 296152, + "moves": 117816, + "retained_cells": 1776, + "roles": 30 + }, + "geometry": { + "P": 8, + "a": 2, + "b": 1, + "ell": 4, + "ks": [ + 1 + ], + "spectator_width": 0 + }, + "maximum_fanout": 2, + "output_sha256": "37197df41278fb5df945780e0e7c928ff7e52bb29672b78faeb914ddc44d9339", + "zero_copy_sources": 20 + }, + { + "B": 10, + "C": 1024, + "K": 27, + "M": 1024, + "Q": 448, + "after_erase": { + "actions": 55924621, + "moves": 22322760, + "retained_cells": 124785, + "roles": 30 + }, + "before_erase": { + "actions": 55530902, + "moves": 22154055, + "retained_cells": 124785, + "roles": 30 + }, + "gather": { + "actions": 3764179, + "moves": 1479250, + "retained_cells": 56287, + "roles": 30 + }, + "gather_and_sparse_sort": { + "actions": 50076447, + "moves": 20004132, + "retained_cells": 115551, + "roles": 30 + }, + "geometry": { + "P": 8, + "a": 2, + "b": 1, + "ell": 4, + "ks": [ + 1, + 1 + ], + "spectator_width": 0 + }, + "maximum_fanout": 4, + "output_sha256": "86ee13722bf69bdc41109add08e1df31b8a99afcd81ef1f72bb7039fe8b00c32", + "zero_copy_sources": 400 + }, + { + "B": 10, + "C": 448, + "K": 27, + "M": 1024, + "Q": 448, + "after_erase": { + "actions": 28502162, + "moves": 11345158, + "retained_cells": 70305, + "roles": 30 + }, + "before_erase": { + "actions": 28257705, + "moves": 11240422, + "retained_cells": 70305, + "roles": 30 + }, + "gather": { + "actions": 2597732, + "moves": 1010032, + "retained_cells": 34959, + "roles": 30 + }, + "gather_and_sparse_sort": { + "actions": 22860400, + "moves": 9115074, + "retained_cells": 61071, + "roles": 30 + }, + "geometry": { + "P": 8, + "a": 1, + "b": 0, + "ell": 3, + "ks": [ + 1, + 2 + ], + "spectator_width": 1 + }, + "maximum_fanout": 1, + "output_sha256": "068ca865a3002e52455f2406829f94fbc4c56bf9cae91fc27ba44eb3581739e0", + "zero_copy_sources": 576 + } + ], + "python": "3.12.14", + "source_bindings": [ + "research/halo-copy-enumeration/README.md", + "research/unconditional-batched-crt/HALO.md", + "research/unconditional-batched-crt/GAUSSIAN.md" + ], + "status": "PASS" +} diff --git a/research/sparse-halo-tape-transaction/OVERLAP.json b/research/sparse-halo-tape-transaction/OVERLAP.json new file mode 100644 index 0000000000..8d2268e0fa --- /dev/null +++ b/research/sparse-halo-tape-transaction/OVERLAP.json @@ -0,0 +1,33 @@ +{ + "checked_on": "2026-11-08", + "canonical_base": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "source_scope": "Bounded lead archive synthesis and scoped PR searches; no exhaustive novelty claim. Discussion posting/access limitations retained in README.", + "contextual_sources": [ + { + "path": "research/rounded-core-halo-splice/PROOF.md", + "usage": "provenance", + "pin": "head:e212af981b49c299de515f8c23dfb0e5b73e2e95:research/rounded-core-halo-splice/PROOF.md", + "git_blob": "d9440b8c90f8663057c3266ccbfe348cfcc52140", + "sha256": "dc8b3d58086bbe208320ece31a19080afecd687ac3be554935db3f091b423f24" + } + ], + "contextual_source_policy": "Exact nonexecuted source pins for attribution and compatibility discussion. These are not live runtime inputs or claims of canonical-base ancestry.", + "new_obligation": "#4870 first Open next question: fixed-role physical first-face copy enumeration, full-key radix, paid rewind/erasure and unique return.", + "predecessors": [ + { + "pr": 4100, + "path": "research/unconditional-batched-crt/HALO.md", + "credit": "Cinna Davis; original source-driven halo schedule and tariff." + }, + { + "pr": 4870, + "path": "research/halo-copy-enumeration/README.md", + "credit": "Astra/OpenAI-assisted contribution; exact source membership and volume, physical implementation left open." + }, + { + "pr": 6880, + "head": "e212af981b49c299de515f8c23dfb0e5b73e2e95", + "credit": "CubeJerry/OpenAI-assisted common-reference core/halo splice; pre-copy and unique-return chronology." + } + ] +} diff --git a/research/sparse-halo-tape-transaction/PROOF.md b/research/sparse-halo-tape-transaction/PROOF.md new file mode 100644 index 0000000000..2f69b5b082 --- /dev/null +++ b/research/sparse-halo-tape-transaction/PROOF.md @@ -0,0 +1,427 @@ +# A sequential tape transaction for first-face halo copies + +## 1. Statement, input contract, and contribution boundary + +This note supplies the physical enumeration/sort/return obligation left open +in [the first open question of #4870](../halo-copy-enumeration/README.md). +The first-face partition, its source-membership predicates, and its volume +formula are inherited results. The new object is the fixed-role sequential +program in `tapes.py`, with the complete dense and sparse movement bill below. +It uses no numerical inverse oracle. An independently supplied halo consumer +remains responsible for producing correct returned *values*. + +Fix integers + +\[ + g\ge1,\quad \ell\ge1,\quad k_i\ge1,\quad E\ge0,\quad P\ge1, + \qquad L=2^\ell,\quad S_i=2^{k_i}L, +\] + +and integers \(0\le b4A\). There are \(2^E\) independent +spectator blocks. In a block, a point has coordinates +\(x_i=q_iL+r_i\), with \(0\le q_i<2^{k_i}\), \(0\le r_i