diff --git a/research/continuation-retained-backing/.gitattributes b/research/continuation-retained-backing/.gitattributes new file mode 100644 index 0000000000..66a5224c92 --- /dev/null +++ b/research/continuation-retained-backing/.gitattributes @@ -0,0 +1 @@ +vendor/** -text diff --git a/research/continuation-retained-backing/EVIDENCE.md b/research/continuation-retained-backing/EVIDENCE.md new file mode 100644 index 0000000000..50f0f4b860 --- /dev/null +++ b/research/continuation-retained-backing/EVIDENCE.md @@ -0,0 +1,107 @@ +# Source, verification and scope record + +Canonical main: `1ec1119972c9aefe42525172d07b332fcff81cb4`, task priority +revision 7. The selected record, source manifest and review were resolved: +κ remains .0030217758 under its five inherited framework assumptions; +its reproduction command is `make frontier4610-verify`. No selected data or +shared code is changed, and no selected cold replay was needed or run. + +New work is confined to `research/continuation-retained-backing/` on the +isolated `codex/continuation-retained-storage` branch. Pending source bytes are +retained verbatim with original notices. EXPORTS.json records their GitHub +heads/paths and SHA256 hashes; load.py authenticates every export before any +predecessor source is compiled. Runtime loading compiles captured bytes rather +than trusting bytecode caches. No unmerged Git object is needed to execute. + +Source exports were obtained from the GitHub contents API with `ref` equal +to the pinned PR head; canonical source exports use `git show BASE:path`. +The proof and bodies of the source PRs were read alongside the code. + +## Executed checks + +Environment: macOS 26.5.1 arm64, CPython 3.12.8, standard library only. + +```sh +python3.12 -B scripts/research_package.py --package research/continuation-retained-backing --check-only +python3.12 -B scripts/research_package.py --package research/continuation-retained-backing +``` + +Both pass. The manifest executes the full verifier normally and under `-O`, +isolated with warnings treated as errors. The registered pair ran serially +under a 180-second wall guard and sampled 1-GiB descendant-RSS guard (0.5-second +sampling). It completed in 3.739 seconds with sampled peak 88,784 KiB. These +resource observations are not an algorithmic memory bound. RESOURCE.json +retains the exact command and measurement. Each manifest command also has +its own 60-second limit. No Lean, Docker or concurrent heavy replay was run. + +RESULT.json records: + +* 648 declared small call trees with independently predicted exact per-tape + capacities, every source write guarded before allocation, full parent bytes, + heads, prefixes and descriptor checked after return. +* Mixed-role warm histories, sixteen capacity-rotation invocations, erased + interiors with identical boundary sizes, nesting through depth31, unequal + sibling/nested descriptors and offsets, empty frames and descriptor copying. +* A shared 128-cell relay with unchanged capacity at depths1,2,8. +* Six actual compact-source calls, two field orders and prefix lengths0,257,4096, + sixteen occupied parents, complete128-record/1024-bit output, independent + endpoint permutation, complete physical return state and unchanged24388-action + return bill. The source-derived per-Role1920-cell local grant is guarded. +* Seven rejecting/probing controls: actual one-cell-short grant, allocating + blank write versus nonallocating reads/moves, omitted actual-source keys, + omitted relay, and three malformed peak/head models. + +The source compact body theorem and the complete tree/history formula received +separate assisted source/proof reviews with shared context. The latter reviewer +also ran both complete modes. An initially overbroad exact online-prefix +sentence was corrected: a mid-push prefix needs a partial-frame model; final +successful-history grants still bound every interior. There is no independent +human or proof-kernel acceptance claim. + +The literal source calibration retains its inherited weak-reference allocator, +logical counters and bulk/control facade. The modeled nineteen tape arrays are +all charged, but that does not compile the facade or prove all-size slot success. +The arbitrary-tree proof is a written induction; finite tests do not substitute +for the production local peak/descriptor/summability obligations. + +## Overlap coverage and unrun obligations + +At 2026-10-23 22:23 UTC the overlap helper reported complete pagination for +350 open PR bodies and 4,684 Discussion records. Its sparse local search covered +zero of7,267 tracked top-level notes; that absence is not novelty evidence. +The live Discussion5012 continuation handoff, start-here and handoff hub were +read separately. Targeted cached text searches and exact source inspection +distinguish the older coefficient stacks, the alternative continuation encoding, +the literal-interchange history theorem and this physical bank. Arbitrary +diffs and unpublished work remain outside coverage. No public claim post was +made during this donor's local-draft checkpoint. + +Primary pending heads: + +* [#5356](https://github.com/CrocSwap/integer-mult-bounds/pull/5356): + `ef1cc26e1e9a08c11cf382de948ee433bebab16d`. +* [#5368](https://github.com/CrocSwap/integer-mult-bounds/pull/5368): + `a2b809f7e000750bc487ad34d3ffc452080e2058`. + +Distinct inspected work includes +[#5286](https://github.com/CrocSwap/integer-mult-bounds/pull/5286), +[#5274](https://github.com/CrocSwap/integer-mult-bounds/pull/5274), +[#5364](https://github.com/CrocSwap/integer-mult-bounds/pull/5364) and +[#5401](https://github.com/CrocSwap/integer-mult-bounds/pull/5401). +The first supplies the prior history-accounting principle; none is imported +as proof of the present tree formula. Pending primitive contracts remain +premises. No full production rectangle, production recursive C, full caller +stock/precision, scientific frontier update or physical allocator is claimed. + +Full source-history preflight requires a non-shallow checkout and is unavailable +here. Metadata/source pins, direct base ancestry, committed-byte checks and +portable export checks are separate from that unavailable history check. + +Final transport checks passed at scientific-code commit +`668d3bb200587de389ec9ede20fb5c1a630a15fc`: committed-byte verification, +official19-file export and integrity validation, and an isolated optimized +Git-free replay from the export with empty PATH. Every exported file remained +byte-identical after replay. Direct base ancestry passes; the optional full +history command reports `source-history check requires full Git history`. +The final canonical-main fetch still returned the pinned base, and both pending +source heads remained unchanged. Subsequent changes only record these checks. diff --git a/research/continuation-retained-backing/EXPORTS.json b/research/continuation-retained-backing/EXPORTS.json new file mode 100644 index 0000000000..dee10235c1 --- /dev/null +++ b/research/continuation-retained-backing/EXPORTS.json @@ -0,0 +1,45 @@ +{ + "schema_version": 1, + "exports": [ + { + "file": "vendor/stack.py", + "pr": 5356, + "head": "ef1cc26e1e9a08c11cf382de948ee433bebab16d", + "path": "research/delimited-continuation-stack/stack.py", + "sha256": "21a2213aa850c55e5eace4cd10b72b958d7ee84d83a014567902ce8ee9b3f4f2", + "author": "aliromman" + }, + { + "file": "vendor/adapter.py", + "pr": 5356, + "head": "ef1cc26e1e9a08c11cf382de948ee433bebab16d", + "path": "research/delimited-continuation-stack/adapter.py", + "sha256": "e13823e4124caa4b25050ddd9ac960db59c81e2db369b9ec7b201aca7efbebb8", + "author": "aliromman" + }, + { + "file": "vendor/return_output.py", + "pr": 5368, + "head": "a2b809f7e000750bc487ad34d3ffc452080e2058", + "path": "research/continuation-output-return/return_output.py", + "sha256": "fbf3167da26c7887b769689075e5dc3afcea2ef668496975bc9e6afec8c85751", + "author": "aliromman" + }, + { + "file": "vendor/streams.py", + "base_path": "research/complex-segment-boundary/source/streams.py", + "sha256": "718a582a50aee8f1f04945ed942be1d4162962fe47dbf05c6ff37b7fb8c61257" + }, + { + "file": "vendor/compact.py", + "base_path": "research/complex-segment-boundary/source/compact.py", + "sha256": "0e1027a60f38c21cfd808c8ce44dcc2423810efdab0e15f02b07f261ad48fc3c" + }, + { + "file": "vendor/NOTICE.md", + "base_path": "research/complex-segment-boundary/source/NOTICE.md", + "sha256": "74a9f03e9ce467c75f5f7cf1b8465d349ea38ef114afad261824c3bcf13da00f" + } + ], + "scope": "Byte-exact exports; pending predecessor theorems remain explicit premises. No pending Git commit required to execute." +} diff --git a/research/continuation-retained-backing/PROOF.md b/research/continuation-retained-backing/PROOF.md new file mode 100644 index 0000000000..179f4726a8 --- /dev/null +++ b/research/continuation-retained-backing/PROOF.md @@ -0,0 +1,207 @@ +# Complete retained backing of the nineteen-tape continuation bank + +## Source and quantified domain + +Fix the unchanged `Stack` of [#5356](https://github.com/CrocSwap/integer-mult-bounds/pull/5356) +and `return_output` of [#5368](https://github.com/CrocSwap/integer-mult-bounds/pull/5368). +Their exact heads and byte exports are in EXPORTS.json. There are k payload +tapes, one control tape, one descriptor tape and one relay; k=16 gives nineteen. +These pending predecessor implementations and their successful-call contracts +remain explicit premises, not independent supplier admission. + +Consider any finite history of successful, properly nested calls in this bank. +Use its contiguous binary-segment ABI. Work appends binary symbols, reads and +moves within its current segment, and erases previously written body cells; +it does not write arbitrary blanks at remote addresses, change an ancestor, +replace a Tape, or shorten cells. Descriptor production obeys the same rule. +Each output return has the reserved empty parent role and distinct empty relay +required by the predecessor. Interrupted calls are outside the theorem. + +The quantity counted is **the sum of lengths of all k+3 Tape.cells arrays**, +including initial prefixes, markers, parked words, erased tails and blank entry +history. It is neither nonblank content nor Python list allocator capacity, +object/heap memory, maximum visited address, physical allocation-controller +correctness or a complete recursive multiplication caller's stock. Reads and +moves in the literal Tape do not allocate; a write, even of BLANK, does. + +For tape j let b_j be its initial origin, just after its fixed initial marker. +The marker and any dirty prefix occupy b_j cells. Let K_j be its entry backing +length, with K_j>=b_j; all cells after the initial current body are blank. +Warm blank tails are allowed. We state root entry with empty current bodies; +initial data loading is part of the history. Initial prefixes never change. + +## Exact path and history formula + +A node v is one current lexical segment. For payload role i, let a_i(v) be +the maximum binary body length reached *anywhere during that node*, including +work later erased and outputs delivered by its children. Let D(v) be the +maximum descriptor length reached, including erased interior production. +Exact maxima give equality below; proved upper bounds give a sufficient grant. + +At a call edge e from parent u, write s_i(e) for each parked body length, +h_i(e) for its head offset, and d(e) for its descriptor length. Thus +0<=h_i<=s_i<=a_i(u) and d(e)<=D(u). Define relative payload origins by + +```text +o_i(root) = 0 +o_i(child) = o_i(parent) + s_i(e) + 1 +f(e) = sum_i h_i(e) + 2k + d(e) + 3. +``` + +Every successful push creates a child node, including a child that does no +work. This convention accounts for the new payload LEFT delimiters even when +both bodies are empty. Let L(e) be the result length actually delivered along +an edge. For a forest of root invocations on the same bank, take all maxima +over the **entire history**, restarting o at zero for each root. Put + +```text +E_i = max_v (o_i(v) + a_i(v)) payload role i +E_c = max_root_path sum_e f(e) complete control frames +E_d = max_v D(v) shared descriptor +E_r = max_return_edge L(e) shared relay. + +retained_j = max(K_j, b_j + E_j) +retained_total = sum_j retained_j. +``` + +Empty edge maxima are zero. This is a complete formula for every one of the +k+3 modeled tape arrays, not an extra space term to be added to an uncounted +continuation stack. Equality refers to the completed successful history (or +a history ending at a completed boundary). Its final historical maxima give +prospective grants that also bound every partial push/pop interior. A prefix +ending mid-push would need a partial-frame model for an exact online identity. + +The coordinatewise history principle already appears for another implementation +in [#5286](https://github.com/CrocSwap/integer-mult-bounds/pull/5286). The new +source-specific content here is the nested payload-origin recurrence, the exact +unary-frame frontier, the descriptor/relay sharing and their composition through +the actual output-return schedule. The older coefficient evaluator's stack +backing results concern a different representation. + +## Proof at individual operations + +Tape.write extends cells exactly to max(old length, head+1); it never shrinks. +Its read and move methods do not extend cells. Thus capacity is its entry +length or one past its largest written address, whichever is greater. + +At node v, its initial payload marker is at b_i+o_i(v)-1. Appending an a-symbol +word writes no farther than b_i+o_i(v)+a-1, giving capacity b_i+o_i(v)+a. +Erasure writes only within the previous word. A push scans the parent word +and writes LEFT at its end: the new capacity is b_i+o_i(parent)+s_i+1, +which is exactly b_i+o_i(child) even for an empty child. Partial pushes are +dominated by that completed child boundary. Pop clears existing delimiters +and words; it does not add a farther write. Output installation is a binary +append in the resumed parent node and is included in that node's a_i. +This proves the payload coordinates by induction on the nested calls. + +The control push emits one complete f(e)-symbol frame at the previous top. +All older active frames form a contiguous prefix. Partial pushes write a +prefix of the completed frame. Pop only clears that existing frame and +restores the earlier top; the largest control address is therefore exactly +the largest active path sum. Different siblings reuse its erased tail. + +The descriptor always has its single initial BASE, and push erases it before +child production. Pop erases the child descriptor and restores the parent's +saved word. Each restored word was already produced earlier, so restoration +cannot exceed the maximum D. This includes the original and restored copies +without charging a new descriptor tape at each depth. + +The relay is empty between returns. Each return writes L symbols at its fixed +origin and erases them after copying to the parent. Hence its history maximum +is max L, with no depth sum. During the first copy the child output and relay +are both present; during installation the parent's output is included in its +payload coordinate. All these arrays are counted simultaneously in the sum. +Taking max with K preserves arbitrary erased entry capacity. All coordinate +maxima remain allocated even if attained on different branches or invocations. + +If the supplied a,D are exact, each nonzero maximum is attained by an actual +binary write or delimiter/frame write. Therefore equality holds. If they are +only upper bounds, the same argument proves a prospective sufficient grant. + +## Convenient complete grants and the missing production premise + +Let V be a history-wide upper bound, at every node, for the sum of parked +ancestor payload extents plus the sum of that node's local role peaks. Let h +bound active edges, P the maximum path sum of parked descriptor lengths, +dmax=max D and Lmax=max L. Then E_i<=V+h, E_c<=V+(2k+3)h+P, +E_d<=dmax and E_r<=Lmax. Since K_j>=b_j, + +```text +total <= K0 + (k+1)V + (3k+3)h + P + dmax + Lmax + = K0 + 17V + 51h + P + dmax + Lmax when k=16. +``` + +This grant is independent of the number of calls and includes historical +role rotation. The exact vector formula is usually much tighter. + +Alternatively define G(v)=sum_i a_i(v)+D(v)+2k+3. If every root-to-node path +has sum_v G(v)<=B, each of the k+3 extents is at most B. Thus +**total<=K0+19B**. A proved geometric bound G(v)<=C*rho^depth*Vroot, +0<=rho<1, gives total<=K0+19*C*Vroot/(1-rho). The constant marker/header +term is already in G and cannot be omitted at small nodes. + +These are conditional composition statements. A production proof must derive +the actual local peaks and descriptor/path summability, and charge K0. The +fixed-tape ABI alone does not imply O(Vroot). At depth D, parking M symbols in +one role at each level leaves D(M+1) cells in that role and D(2k+3) control +symbols even with zero head offsets and empty descriptors. All-empty nodes +still accumulate k payload delimiters and 2k+3 control symbols per edge. +Shrinking payload alone is insufficient if every frame copies a root-sized +descriptor. These are counterexamples to unsupported composition arguments, +not objections to the predecessor local-time theorems. + +## A source-derived local peak for compact work + +For unchanged successful `compact.execute`, let a valid complete binary layout +have b address bits, R=2^b records and positive record width w. Then every +lexical payload Role body has length at most **R(w+b)**, throughout execution: + +| Source operation | Maximum body of any one Role | +| --- | ---: | +| ordinary digit exchange, digit permutation, flip | Rw | +| rotate left/right/output | Rw | +| repair good and output | Rw | +| repair holes | R | +| repair keyed bad, radix bucket/output | R(w+b) | + +For rotation and digit operations each buffer receives only portions of one +complete rectangle, and output has R records. Repair emits at most one key +plus payload per exceptional record. Radix passes partition and concatenate +the same J<=R complete (b+w)-bit records; they do not duplicate records into +one buffer. All writes are append-only and erase resets the logical body. +This proves the bound for any number of valid passes. Successful slot reuse +places successive empty Role bodies in the same physical segment, so its +local high-water obeys the same bound. If b<=w, this is at most 2Rw; without +such a relation, the address-key cost cannot be discarded as a constant. + +Erasure does not release a lexical owner: radix loop variables and repair +locals can retain erased Roles. This lemma does not prove sixteen-slot +sufficiency. The inherited weak-reference allocator, logical length facade, +source bulk read arrays, layout/control/descriptor production and a compiled +physical allocator remain outside the modeled tape-capacity theorem. + +## Discriminating implementation evidence + +The verifier authenticates all exports before compilation and executes the +unchanged methods. A checker-only guard rejects an insufficient coordinate +grant **before** each Tape.write can grow its array. It also checks literal +monotone write semantics. Declared small call trees predict capacities before +execution; endpoint snapshots and final array lengths are checked separately. + +With k=16, sixteen root invocations each use a 64-cell child temporary in a +different role. Every fresh owner retains 142 cells, but one reused owner +retains **142,206,...,1102**. Taking the maximum standalone total would grant +142 and fail. A child that writes/erases 4096 cells before returning one bit +retains 4175 versus 80 for the same boundary sizes and a one-cell interior. +Those erased writes must be in a(v), not inferred from endpoint W or L. + +The six compact-source calibrations execute both layouts with preserved +prefixes of lengths 0,257,4096, sixteen occupied parent roles and a complete +128-record, 1024-bit child output. The independently checked permutation and +complete return state agree; the predecessor's return bill remains 24388. +The source-derived local grant is R(w+b)=128*(8+7)=1920 per payload role. +These finite observations corroborate the source induction, not full +production recursion, selected-source admission or formal-kernel verification. + +New proof/checker by zxv with substantial OpenAI Codex assistance. Predecessor +notices and contributor credit are retained in README.md and vendor/NOTICE.md. diff --git a/research/continuation-retained-backing/README.md b/research/continuation-retained-backing/README.md new file mode 100644 index 0000000000..befaca36f5 --- /dev/null +++ b/research/continuation-retained-backing/README.md @@ -0,0 +1,95 @@ +# Retained backing across physical continuation histories + +This package closes the modeled-tape backing calculation for the nineteen-tape +continuation of [#5356](https://github.com/CrocSwap/integer-mult-bounds/pull/5356) +and [#5368](https://github.com/CrocSwap/integer-mult-bounds/pull/5368). +[PROOF.md](PROOF.md) derives every payload coordinate from nested segment +origins, adds the exact unary control-frame frontier, and accounts for shared +descriptor and relay backing. It includes prefixes, markers, erased tails, +arbitrary blank entry history and outputs delivered into resumed parents. + +The complete capacity is a **sum of coordinatewise historical maxima**. +Sixteen 64-cell child temporaries, each placed in a different role, use 142 +cells per fresh owner but **1102 cells in one reused bank**. A child returning +one bit after writing and erasing 4096 cells retains 4175 versus 80 cells for +the same boundary sizes and a one-cell interior. Neither a fixed number of +tapes nor a local linear time bill supplies a recursive space bound. + +For k payload roles, K0 total entry backing, historical path payload envelope V, +maximum depth h, parked descriptor path sum P, descriptor maximum dmax and +maximum delivered output Lmax, a sufficient complete grant is + +```text +K0 + (k+1)V + (3k+3)h + P + dmax + Lmax. +``` + +For k=16 this is `K0+17V+51h+P+dmax+Lmax`. The exact vector formula in the proof +is tighter. A conditional `K0+19B` corollary states the path-summability premise +needed to prove an O(root volume) reserve, including descriptor and marker terms. +That production premise is left open, rather than inferred from proper nesting. + +The unchanged compact-source routines supply a useful local input: a complete +rectangle with R records, b address bits and w payload bits per record has at +most **R(w+b)** binary symbols in any one lexical payload Role, including +repair keys and radix buffers. This is a source-derived local bound, not a +proof of sixteen-slot allocation success or complete recursive caller stock. + +## Reproduce + +Python 3.12, standard library only: + +```sh +python3.12 -B scripts/research_package.py --package research/continuation-retained-backing --check-only +python3.12 -B scripts/research_package.py --package research/continuation-retained-backing +python3.12 -B scripts/check_research_commit.py --package research/continuation-retained-backing +``` + +The registered normal and optimized commands authenticate package-local source +exports before execution and compare the full typed deterministic RESULT.json. +`verify.py --emit` prints a fresh receipt without editing the committed receipt. +Prospective per-tape guards check capacity before each source write; declared +trees predict exact final lengths. Source calibration checks the complete +independent compact permutation and preserved parent state, not only lengths. +See [EVIDENCE.md](EVIDENCE.md) for environment and coverage. + +Only this package is added; frozen inputs and the selected frontier are unchanged. +The result counts all nineteen modeled Tape.cells arrays. It excludes Python +heap/list allocator capacity, source bulk arrays, the weak-reference allocation +facade, logical counter compilation, descriptor production, full recursive C, +stock/precision admission and the full multiplication theorem. + +## Attribution + +[@aliromman](https://github.com/aliromman) supplied the unchanged physical stack +and output return in [#5356](https://github.com/CrocSwap/integer-mult-bounds/pull/5356) +and [#5368](https://github.com/CrocSwap/integer-mult-bounds/pull/5368). +[@JoyboyBrian](https://github.com/JoyboyBrian)'s +[#5329](https://github.com/CrocSwap/integer-mult-bounds/pull/5329) supplies the +segment/source boundary; [#5041](https://github.com/CrocSwap/integer-mult-bounds/pull/5041) +supplies locality context. [#5286](https://github.com/CrocSwap/integer-mult-bounds/pull/5286) +by [@kumagi](https://github.com/kumagi) supplies earlier coordinatewise history +accounting for a different bank, retaining the prior numerical/packet-backing +work's credit for that accounting principle. +[@jmbarrancoml](https://github.com/jmbarrancoml) supplied sequential compact +primitives through [#2250](https://github.com/CrocSwap/integer-mult-bounds/pull/2250). +Douglas Colkitt, Cinna Davis, [@Matarener](https://github.com/Matarener), the +guard/repair/carry/native lineage and original source notices retain their credit. +The alternative stack [#5364](https://github.com/CrocSwap/integer-mult-bounds/pull/5364) +by [@mihir-s-05](https://github.com/mihir-s-05) is a distinct encoding, not +audited or replaced here. New work by [@zxv](https://github.com/zxv), with +substantial OpenAI Codex assistance in proof, implementation and assisted review. +Review shares source context; no independent human or formal-kernel acceptance +is claimed. Apache-2.0; see vendor/NOTICE.md and retained module notices. + +## Open next questions + +1. Prove a production path envelope for actual parked payloads and generated + descriptors. Start at one literal recursive call and derive G(v), including + erased interiors and markers. The production recursive-C/descriptor compiler + and common-cut bounds remain blockers; a local time tariff is insufficient. +2. Compile lexical allocation and logical counters physically. Start with + repair/stable_radix and its erased-but-retained owners. The per-Role length + bound does not prove slot reuse or allocation success. +3. Integrate the complete vector grant into a caller reserve. First bind each + actual role's local peak and inherited K_j. External caller banks, source + bulk-array lowering, numeric stock and placement remain separate obligations. diff --git a/research/continuation-retained-backing/RESOURCE.json b/research/continuation-retained-backing/RESOURCE.json new file mode 100644 index 0000000000..81bc30e4f0 --- /dev/null +++ b/research/continuation-retained-backing/RESOURCE.json @@ -0,0 +1,13 @@ +{ + "exit_code": 0, + "elapsed_seconds": 3.739, + "peak_descendant_rss_kib": 88784, + "resource_stop": null, + "command": [ + "/opt/local/bin/python3.12", + "-B", + "scripts/research_package.py", + "--package", + "research/continuation-retained-backing" + ] +} diff --git a/research/continuation-retained-backing/RESULT.json b/research/continuation-retained-backing/RESULT.json new file mode 100644 index 0000000000..be19834122 --- /dev/null +++ b/research/continuation-retained-backing/RESULT.json @@ -0,0 +1,782 @@ +{ + "census": { + "cases": 648, + "writes": 34344 + }, + "controls": [ + "one_cell_short", + "blank_write_is_not_free_storage", + "omitted_actual_source_keys", + "omitted_relay", + "malformed_model", + "malformed_model", + "malformed_model" + ], + "discriminators": { + "chains": [ + { + "capacities": [ + 2, + 66, + 2, + 2, + 2, + 2, + 2, + 2, + 2, + 2, + 2, + 2, + 2, + 2, + 2, + 2, + 71, + 33, + 6 + ], + "depth": 1, + "total": 206 + }, + { + "capacities": [ + 3, + 131, + 3, + 3, + 3, + 3, + 3, + 3, + 3, + 3, + 3, + 3, + 3, + 3, + 3, + 3, + 138, + 33, + 6 + ], + "depth": 2, + "total": 353 + }, + { + "capacities": [ + 9, + 521, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 540, + 33, + 6 + ], + "depth": 8, + "total": 1235 + }, + { + "capacities": [ + 32, + 2016, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 2081, + 33, + 6 + ], + "depth": 31, + "total": 4616 + } + ], + "descriptor_copy": { + "capacities": [ + 2, + 2, + 2, + 2, + 2, + 2, + 2, + 2, + 2, + 2, + 2, + 2, + 2, + 2, + 2, + 2, + 2087, + 2049, + 6 + ], + "growth": [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 2083, + 2048, + 0 + ], + "totals": [ + 4174 + ], + "writes": 12390 + }, + "empty_frame": { + "capacities": [ + 2, + 2, + 2, + 2, + 2, + 2, + 2, + 2, + 2, + 2, + 2, + 2, + 2, + 2, + 2, + 2, + 39, + 1, + 6 + ], + "growth": [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 35, + 0, + 0 + ], + "totals": [ + 78 + ], + "writes": 102 + }, + "erased_interior": { + "capacities": [ + 2, + 4098, + 2, + 2, + 2, + 2, + 2, + 2, + 2, + 2, + 2, + 2, + 2, + 2, + 2, + 2, + 39, + 1, + 7 + ], + "growth": [ + 1, + 4097, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 35, + 0, + 1 + ], + "totals": [ + 4175 + ], + "writes": 8300 + }, + "fresh_totals": [ + 142, + 142, + 142, + 142, + 142, + 142, + 142, + 142, + 142, + 142, + 142, + 142, + 142, + 142, + 142, + 142 + ], + "rotation": { + "capacities": [ + 66, + 66, + 66, + 66, + 66, + 66, + 66, + 66, + 66, + 66, + 66, + 66, + 66, + 66, + 66, + 66, + 39, + 1, + 6 + ], + "growth": [ + 65, + 65, + 65, + 65, + 65, + 65, + 65, + 65, + 65, + 65, + 65, + 65, + 65, + 65, + 65, + 65, + 35, + 0, + 0 + ], + "totals": [ + 142, + 206, + 270, + 334, + 398, + 462, + 526, + 590, + 654, + 718, + 782, + 846, + 910, + 974, + 1038, + 1102 + ], + "writes": 3680 + }, + "same_boundary_tiny_interior": { + "capacities": [ + 2, + 3, + 2, + 2, + 2, + 2, + 2, + 2, + 2, + 2, + 2, + 2, + 2, + 2, + 2, + 2, + 39, + 1, + 7 + ], + "growth": [ + 1, + 2, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 35, + 0, + 1 + ], + "totals": [ + 80 + ], + "writes": 110 + }, + "shared_relay_capacities": [ + 134, + 134, + 134 + ], + "unequal_siblings": { + "capacities": [ + 32, + 53, + 37, + 76, + 30, + 37 + ], + "growth": [ + 8, + 29, + 13, + 49, + 29, + 8 + ], + "totals": [ + 265 + ], + "writes": 584 + }, + "warm_entry": { + "capacities": [ + 501, + 501, + 501, + 501, + 501, + 501, + 501, + 501, + 501, + 501, + 501, + 501, + 501, + 501, + 501, + 501, + 504, + 501, + 506 + ], + "growth": [ + 1, + 2, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 35, + 0, + 1 + ], + "totals": [ + 9527 + ], + "writes": 110 + } + }, + "source": [ + { + "capacities": [ + 1026, + 1029, + 774, + 1927, + 1032, + 1929, + 1930, + 1931, + 1932, + 973, + 14, + 15, + 16, + 17, + 18, + 19, + 138, + 44, + 1030 + ], + "grants": [ + 1922, + 1925, + 1926, + 1927, + 1928, + 1929, + 1930, + 1931, + 1932, + 1933, + 1934, + 1935, + 1936, + 1937, + 1938, + 1939, + 138, + 44, + 1030 + ], + "late": false, + "output_sha256": "4af9929ff7e3d8e72146e260c7e007e975b7c17ef26c0271355333fe64072a48", + "per_role_local_bound": 1920, + "prefix": 0, + "record_bits": 8, + "records": 128, + "return_steps": 24388, + "writes": 102501 + }, + { + "capacities": [ + 1283, + 1286, + 1031, + 2184, + 1289, + 2186, + 2187, + 2188, + 2189, + 1230, + 271, + 272, + 273, + 274, + 275, + 276, + 395, + 44, + 1287 + ], + "grants": [ + 2179, + 2182, + 2183, + 2184, + 2185, + 2186, + 2187, + 2188, + 2189, + 2190, + 2191, + 2192, + 2193, + 2194, + 2195, + 2196, + 395, + 44, + 1287 + ], + "late": false, + "output_sha256": "4af9929ff7e3d8e72146e260c7e007e975b7c17ef26c0271355333fe64072a48", + "per_role_local_bound": 1920, + "prefix": 257, + "record_bits": 8, + "records": 128, + "return_steps": 24388, + "writes": 102501 + }, + { + "capacities": [ + 5122, + 5125, + 4870, + 6023, + 5128, + 6025, + 6026, + 6027, + 6028, + 5069, + 4110, + 4111, + 4112, + 4113, + 4114, + 4115, + 4234, + 44, + 5126 + ], + "grants": [ + 6018, + 6021, + 6022, + 6023, + 6024, + 6025, + 6026, + 6027, + 6028, + 6029, + 6030, + 6031, + 6032, + 6033, + 6034, + 6035, + 4234, + 44, + 5126 + ], + "late": false, + "output_sha256": "4af9929ff7e3d8e72146e260c7e007e975b7c17ef26c0271355333fe64072a48", + "per_role_local_bound": 1920, + "prefix": 4096, + "record_bits": 8, + "records": 128, + "return_steps": 24388, + "writes": 102501 + }, + { + "capacities": [ + 1026, + 1029, + 1030, + 1927, + 1032, + 1929, + 1930, + 1931, + 1932, + 973, + 14, + 15, + 16, + 17, + 18, + 19, + 138, + 44, + 1030 + ], + "grants": [ + 1922, + 1925, + 1926, + 1927, + 1928, + 1929, + 1930, + 1931, + 1932, + 1933, + 1934, + 1935, + 1936, + 1937, + 1938, + 1939, + 138, + 44, + 1030 + ], + "late": true, + "output_sha256": "9b6381e2a8cffec1c0d499b50909c409c9dc178584321a9a6e73fafbdbfaf547", + "per_role_local_bound": 1920, + "prefix": 0, + "record_bits": 8, + "records": 128, + "return_steps": 24388, + "writes": 159845 + }, + { + "capacities": [ + 1283, + 1286, + 1287, + 2184, + 1289, + 2186, + 2187, + 2188, + 2189, + 1230, + 271, + 272, + 273, + 274, + 275, + 276, + 395, + 44, + 1287 + ], + "grants": [ + 2179, + 2182, + 2183, + 2184, + 2185, + 2186, + 2187, + 2188, + 2189, + 2190, + 2191, + 2192, + 2193, + 2194, + 2195, + 2196, + 395, + 44, + 1287 + ], + "late": true, + "output_sha256": "9b6381e2a8cffec1c0d499b50909c409c9dc178584321a9a6e73fafbdbfaf547", + "per_role_local_bound": 1920, + "prefix": 257, + "record_bits": 8, + "records": 128, + "return_steps": 24388, + "writes": 159845 + }, + { + "capacities": [ + 5122, + 5125, + 5126, + 6023, + 5128, + 6025, + 6026, + 6027, + 6028, + 5069, + 4110, + 4111, + 4112, + 4113, + 4114, + 4115, + 4234, + 44, + 5126 + ], + "grants": [ + 6018, + 6021, + 6022, + 6023, + 6024, + 6025, + 6026, + 6027, + 6028, + 6029, + 6030, + 6031, + 6032, + 6033, + 6034, + 6035, + 4234, + 44, + 5126 + ], + "late": true, + "output_sha256": "9b6381e2a8cffec1c0d499b50909c409c9dc178584321a9a6e73fafbdbfaf547", + "per_role_local_bound": 1920, + "prefix": 4096, + "record_bits": 8, + "records": 128, + "return_steps": 24388, + "writes": 159845 + } + ], + "status": "PASS_CONTINUATION_RETAINED_BACKING" +} diff --git a/research/continuation-retained-backing/SOURCES.json b/research/continuation-retained-backing/SOURCES.json new file mode 100644 index 0000000000..987398f0e4 --- /dev/null +++ b/research/continuation-retained-backing/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "1ec1119972c9aefe42525172d07b332fcff81cb4", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b288ae44032fd84dd5564243422836cbcd29835e", + "sha256": "f9ed52bb642cd1e1486cf2743557ac5fa23cf1514a3277d786a644e39a565038" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/complex-segment-boundary/source/compact.py", + "usage": "provenance", + "git_blob": "60bc206c78150f23563a4775800b0dd32025843d", + "sha256": "0e1027a60f38c21cfd808c8ce44dcc2423810efdab0e15f02b07f261ad48fc3c" + }, + { + "path": "research/complex-segment-boundary/source/streams.py", + "usage": "provenance", + "git_blob": "61542ce4c9eb51bfc113475b4f98649cb90a853e", + "sha256": "718a582a50aee8f1f04945ed942be1d4162962fe47dbf05c6ff37b7fb8c61257" + }, + { + "path": "research/complex-segment-boundary/source/NOTICE.md", + "usage": "provenance", + "git_blob": "e82bfef53054bd753ba0aa8a966f84427faa2293", + "sha256": "74a9f03e9ce467c75f5f7cf1b8465d349ea38ef114afad261824c3bcf13da00f" + } + ] +} diff --git a/research/continuation-retained-backing/TASK.json b/research/continuation-retained-backing/TASK.json new file mode 100644 index 0000000000..bf29ba75dc --- /dev/null +++ b/research/continuation-retained-backing/TASK.json @@ -0,0 +1,79 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "1ec1119972c9aefe42525172d07b332fcff81cb4", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Prove one missing implication with explicit quantified hypotheses.", + "Find an exact counterexample at the claimed interface boundary." + ], + "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_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": [ + "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller." + ], + "scope_change_triggers": [ + "Replacing a quantified obligation with another finite smoke test.", + "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses." + ], + "overlap_terms": [ + "uniform transfer", + "all-size", + "precision", + "4100", + "unconditional-batched-crt" + ], + "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_status": "refined", + "actual_scope": "Complete modeled nineteen-tape retained-backing formula for the physical continuation bank across nested mixed histories, with source-derived compact local peaks.", + "scope_change_reason": "Explicit donor-assigned second contribution; join pending physical stack/output-return scope to historical erased backing without implementing another continuation encoding.", + "bottleneck_link": "Per-boundary action invoices omit the history and summability needed for a recursive backing grant.", + "stop_rule": "Complete this scoped theorem, prospective capacity checks and a local proposed PR; wait for donor confirmation before publication and Task3.", + "outcome": "partial", + "evidence": "PROOF.md complete tree/history induction; RESULT.json exact predicted capacities, negative budget witnesses and six unchanged compact-source returns.", + "author": "zxv with OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance in proof, implementation, source audit and separate assisted reviews sharing source context.", + "open_questions": [ + { + "question": "Do production parked payloads and descriptors satisfy the path-summability premise?", + "why_it_matters": "A fixed bank and a local linear bill do not imply an O(root volume) reserve.", + "first_step": "Bind one actual recursive call to the source local peaks, descriptor sizes and inherited blank history.", + "blocked_by": "Production recursive C/descriptor compilation and common-cut path envelope remain open." + }, + { + "question": "Can lexical role allocation and source counters be compiled physically?", + "why_it_matters": "Erased Roles can retain owners; per-Role length bounds do not establish sixteen-slot success.", + "first_step": "Audit repair/stable_radix retained lexical references and replace its weak-reference facade.", + "blocked_by": "Physical allocation and counter/slot operations remain predecessor premises." + } + ] +} diff --git a/research/continuation-retained-backing/VERIFY.json b/research/continuation-retained-backing/VERIFY.json new file mode 100644 index 0000000000..ca8bd2f68a --- /dev/null +++ b/research/continuation-retained-backing/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Exact predicted backing across648smallcases, nested/sibling histories, erased/warm/relay/control cases, prospective quota failures, six full actual-source compact returns and full deterministic receipt." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Same complete source and capacity verification with assertions disabled." + } + ] +} diff --git a/research/continuation-retained-backing/capacity.py b/research/continuation-retained-backing/capacity.py new file mode 100644 index 0000000000..09b0584a60 --- /dev/null +++ b/research/continuation-retained-backing/capacity.py @@ -0,0 +1,70 @@ +"""Source-specific retained extents of the physical continuation bank. + +Checker arithmetic, not a physical allocator. Local peaks must include erased +interiors and delivered outputs. A virtual empty child counts push delimiters. +""" +from dataclasses import dataclass + + +def need(ok,message): + if not ok:raise ValueError(message) + + +@dataclass(frozen=True) +class Cut: + sizes: tuple + heads: tuple + descriptor: int + child: object + + +@dataclass(frozen=True) +class Node: + peaks: tuple + descriptor_peak: int + cuts: tuple = () + output: int = 0 + + +def extents(root,k): + """Return payload k-vector, control, descriptor and relay written extents.""" + payload=[0]*k;control=descriptor=relay=0 + def visit(node,offset,stack): + nonlocal control,descriptor,relay + need(len(node.peaks)==k and all(type(x) is int and x>=0 for x in node.peaks),'Local nonnegative role peaks') + need(type(node.descriptor_peak) is int and node.descriptor_peak>=0,'Descriptor interior peak') + need(type(node.output) is int and 0<=node.output<=max(node.peaks,default=0),'Output inside local peak') + payload[:]=[max(old,start+peak) for old,start,peak in zip(payload,offset,node.peaks)] + control=max(control,stack);descriptor=max(descriptor,node.descriptor_peak) + for cut in node.cuts: + need(len(cut.sizes)==len(cut.heads)==k,'Complete parked role vectors') + need(all(type(s) is int and type(h) is int and 0<=h<=s<=a + for s,h,a in zip(cut.sizes,cut.heads,node.peaks)),'Parked extents and heads within local peaks') + need(type(cut.descriptor) is int and 0<=cut.descriptor<=node.descriptor_peak,'Parked descriptor within local peak') + following=tuple(o+s+1 for o,s in zip(offset,cut.sizes)) + frame=sum(cut.heads)+2*k+cut.descriptor+3 + visit(cut.child,following,stack+frame) + relay=max(relay,cut.child.output) + visit(root,(0,)*k,0) + return tuple(payload)+(control,descriptor,relay) + + +def capacities(origins,entry,extra): + need(len(origins)==len(entry)==len(extra),'All k+3 tape coordinates') + need(all(type(b) is int and type(x) is int and b>=1 and x>=b for b,x in zip(origins,entry)),'Entry backing includes initial marker/prefix') + need(all(type(x) is int and x>=0 for x in extra),'Nonnegative written extents') + return tuple(max(old,base+growth) for base,old,growth in zip(origins,entry,extra)) + + +def coarse_grant(k,entry_total,volume,depth,descriptor_path,descriptor_max,output_max): + """Sufficient history envelope; volume includes each node's local peaks.""" + need(type(k) is int and k>=1,'Fixed positive role count') + need(all(type(x) is int and x>=0 for x in (entry_total,volume,depth,descriptor_path,descriptor_max,output_max)), + 'Nonnegative historical envelopes') + return entry_total+(k+1)*volume+(3*k+3)*depth+descriptor_path+descriptor_max+output_max + + +def compact_peak(address_bits,record_bits): + need(type(address_bits) is int and address_bits>=0 and type(record_bits) is int and record_bits>=1, + 'Compact rectangle bit widths') + return (1<>=width + return out + + def encode(self,state): + out=0 + for name,width in self.fields: + need(0<=state[name]<1<=1 and self.K>=1 and self.G>=1 and 0<=self.rholayout.names.index(self.target))==self.late, + "declared source order") + else:need(not self.late,"constant toggle uses early routine") + + def select(self,value): + return sum(((value>>(self.rho+i*self.K))&1)<<(i*self.G) for i in range(self.n)) + + def mask(self,value,compact=False): + return sum(((value>>(i*self.G if compact else self.rho+i*self.K))&1) + <<(self.rho+i*self.K) for i in range(self.n)) + + def operations(self): + ops=[] + def rot(target,controls,kind,sign=1):ops.append(("rotate",target,controls,kind,sign)) + def load(front,controls,kind,sign=1): + ops.append(("swap",front,"b"));rot("b",controls,kind,sign);ops.append(("swap",front,"b")) + def flip(control,is_compact=False): + tag="compact" if is_compact else "wide" + controls=(() if control is None else (control,))+("t",) + rot(self.target,controls,"first_"+tag) + load("t",(self.target,),"selected_y") + rot(self.target,controls,"second_"+tag) + controls=(() if control is None else (control,))+(self.target,) + load("t",controls,"original_"+tag,-1) + if self.late: + flip("u",True);load("u",(self.source,),"selected_x") + flip("u",True);load("u",(self.source,),"selected_x",-1) + else:flip(self.source) + return tuple(ops) + + def offset(self,state,operation): + _,target,controls,kind,sign=operation + if kind=="selected_y":return sign*self.select(state[self.target]) + if kind=="selected_x":return sign*self.select(state[self.source]) + compact=kind.endswith("compact") + control="u" if compact else self.source + bits=[1 if control is None else (state[control]>>(i*self.G if compact else self.rho+i*self.K))&1 + for i in range(self.n)] + if kind.startswith("original"): + value=state[self.target]^sum(b<<(self.rho+i*self.K) for i,b in enumerate(bits)) + return sign*self.select(value) + B=1<>(i*self.G))&(B-1)) if kind.startswith("first") + else 1-2*((state["t"]>>(i*self.G))&(B-1))) + <<(self.rho+i*self.K) for i in range(self.n)) + + def execute(self,state,layout,inverse=False): + out=dict(state) + for op in reversed(self.operations()) if inverse else self.operations(): + if op[0]=="swap":out[op[1]],out[op[2]]=out[op[2]],out[op[1]] + else:out[op[1]]=(out[op[1]]+(-1 if inverse else 1)*self.offset(out,op))%(1<>(self.rho+i*self.K))&1)<<(self.rho+i*self.K) for i in range(n))) + out[self.target]^=value + return out + + def bad(self,state): + B=1<>(i*self.G))&(B-1))==B-1 or + not 2*B<=((state[self.target]>>(self.rho+i*self.K+1))&mask)>(i*self.G))&(B-1))==B-1) + for i in range(self.n)) + + +def ordinary(source,layout,first,second): + """Completed elementary supplier used in tests; retain the abstract call bill.""" + width=layout.width(first);need(width==layout.width(second),"equal ordinary chunks") + source.meter.ordinary_calls.append({"width":width,"volume":len(source.data)}) + for bit in range(width): + a,b=sorted((layout.position(first,bit),layout.position(second,bit))) + source=digit_permutation(source,layout.bits,a,b,layout.record_bits,(0,2,1,3)) + return source + + +def rotate(source,layout,word,op): + _,target,controls,_,_=op;at=layout.names.index(target) + need(all(layout.names.index(name)= self.floor, 'ancestor prefix accessed') + return self.cells[self.head] if self.head < len(self.cells) else BLANK + + def write(self, value): + need(value in range(7), 'finite tape alphabet') + need(self.head >= self.floor, 'ancestor prefix overwritten') + self.counts.writes += 1 + while len(self.cells) <= self.head: + self.cells.append(BLANK) + self.cells[self.head] = value + + def move(self, direction): + need(direction in (-1, 1), 'unit move') + self.counts.moves += 1 + self.head += direction + need(self.head >= self.floor, 'ancestor prefix crossed') + + +def emit(tape, symbol): + tape.write(symbol) + tape.move(1) + + +def rewind(tape, marker): + tape.move(-1) + while tape.read() != marker: + tape.move(-1) + tape.move(1) + + +def clear_descriptor(tape): + """Entry and exit are at the descriptor origin.""" + while (symbol := tape.read()) != BLANK: + need(symbol in (ZERO, ONE), 'binary descriptor') + emit(tape, BLANK) + rewind(tape, BASE) + + +class Stack: + """No saved frame, parent pointer, frame size or origin is stored here.""" + def __init__(self, payloads, control, descriptor): + self.payloads = tuple(payloads) + self.control = control + self.descriptor = descriptor + + def push(self, present): + need(len(present) == len(self.payloads), 'fixed role bitmap') + c = self.control + need(c.read() == BLANK, 'control at free top') + emit(c, LEFT) + for tape, occupied in zip(self.payloads, present): + need(type(occupied) is bool, 'role presence bit') + emit(c, int(occupied)) + tape.move(-1) + while (symbol := tape.read()) != LEFT: + need(symbol in (ZERO, ONE), 'binary prefix before current head') + emit(c, ONE) + tape.move(-1) + emit(c, ZERO) + tape.move(1) + if not occupied: + need(tape.read() == BLANK, 'absent role is empty') + while (symbol := tape.read()) != BLANK: + need(symbol in (ZERO, ONE), 'binary parent payload') + tape.move(1) + emit(tape, LEFT) + emit(c, SEP) + d = self.descriptor + while (symbol := d.read()) != BLANK: + need(symbol in (ZERO, ONE), 'binary descriptor') + emit(c, symbol) + emit(d, BLANK) + rewind(d, BASE) + emit(c, END) + + def pop(self): + """Child payloads are empty at their origins; clear its descriptor. + + Returned sizes/heads are observer counts for the source API adapter. + No branch or tape move uses those counts. + """ + clear_descriptor(self.descriptor) + c = self.control + c.move(-1) + need(c.read() == END, 'complete control frame') + c.move(-1) + while (symbol := c.read()) != LEFT: + need(symbol in (ZERO, ONE, SEP), 'frame start before ancestor boundary') + c.move(-1) + emit(c, BLANK) + state = [] + for tape in self.payloads: + present = c.read() + need(present in (ZERO, ONE), 'role presence bit') + emit(c, BLANK) + need(tape.read() == BLANK, 'child payload is retired') + tape.move(-1) + need(tape.read() == LEFT, 'child delimiter') + tape.write(BLANK) + tape.move(-1) + size = 0 + while (symbol := tape.read()) != LEFT: + need(symbol in (ZERO, ONE), 'parked parent payload') + size += 1 + tape.move(-1) + tape.move(1) + if not present: + need(tape.read() == BLANK, 'absent parent role is empty') + head = 0 + while (symbol := c.read()) == ONE: + need(tape.read() in (ZERO, ONE), 'saved head is within payload') + tape.move(1) + head += 1 + emit(c, BLANK) + need(symbol == ZERO, 'terminated unary head') + emit(c, BLANK) + state.append((bool(present), size, head)) + need(c.read() == SEP, 'complete fixed-role header') + emit(c, BLANK) + d = self.descriptor + while (symbol := c.read()) != END: + need(symbol in (ZERO, ONE), 'binary saved descriptor') + emit(d, symbol) + emit(c, BLANK) + c.write(BLANK) + c.move(-1) + while c.read() == BLANK: + c.move(-1) + need(c.read() in (BASE, END), 'previous control top') + c.move(1) + rewind(d, BASE) + return state diff --git a/research/continuation-retained-backing/vendor/streams.py b/research/continuation-retained-backing/vendor/streams.py new file mode 100644 index 0000000000..61542ce4c9 --- /dev/null +++ b/research/continuation-retained-backing/vendor/streams.py @@ -0,0 +1,115 @@ +"""Sequential bit-stream simulator with charged contiguous transfers. + +Bulk methods abbreviate consecutive tape transitions; they charge each bit. +Payload destinations are append-only. Random lookup is confined to controls. +""" +from dataclasses import dataclass,field + + +def need(condition,message): + if not condition: + raise ValueError(message) + + +@dataclass +class Meter: + reads: int=0 + writes: int=0 + moves: int=0 + erases: int=0 + control_evaluations: int=0 + digit_passes: int=0 + rotation_passes: int=0 + radix_passes: int=0 + repair_records: int=0 + ordinary_calls: list=field(default_factory=list) + + +class Tape: + def __init__(self,meter,data=b""): + self.meter=meter;self.data=bytearray(data);self.head=0 + + def read(self,size): + need(0<=size<=len(self.data)-self.head,"sequential read boundary") + value=self.data[self.head:self.head+size];self.head+=size + self.meter.reads+=size;self.meter.moves+=size + return value + + def write(self,value): + need(self.head==len(self.data),"append-only output") + self.data.extend(value);self.head+=len(value) + self.meter.writes+=len(value);self.meter.moves+=len(value) + + def rewind(self): + self.meter.moves+=self.head;self.head=0 + + def finish(self): + need(self.head==len(self.data),"complete sequential consumption") + + def erase(self): + self.rewind();size=len(self.data) + self.meter.erases+=size;self.meter.moves+=2*size + self.data.clear();self.head=0 + + +def copy(source,target,size): + target.write(source.read(size)) + + +def bit_key(value,width): + need(0<=value<1<>i)&1 for i in range(width)) + + +def key_value(bits): + need(all(b in (0,1) for b in bits),"binary control encoding") + return sum(b<max(fresh),'Reject maximum standalone total') + need(rotated['totals']==sorted(set(rotated['totals'])),'Each rotated role retains additional backing') + tiny=root_for(k,child(k,1,1,output_len=1)) + erased=root_for(k,child(k,1,4096,output_len=1)) + tiny_row=history([tiny]);erased_row=history([erased]) + need(erased_row['totals'][0]>tiny_row['totals'][0]+4000,'Erased child interior is not a boundary extent') + warm=history([tiny],warm=(500,)*(k+3)) + need(warm['totals'][0]>=19*500,'Entry backing cannot be discarded') + chain=[] + for depth in (1,2,8,31): + node=child(k,1,0) + for _ in range(depth):node=Case((0,64)+(0,)*14,(0,)*k,32,(node,)) + row=history([node]);chain.append({'depth':depth,'total':row['totals'][0],'capacities':row['capacities']}) + need(chain[-1]['total']>10*chain[0]['total'],'Local linear bills do not bound recursive backing') + zero=root_for(k,child(k,1,0)) + zero_row=history([zero]) + need(sum(zero_row['growth'])==k+2*k+3,'Empty frame still needs payload delimiters and complete control header') + descriptor_only=root_for(k,child(k,1,0),descriptor=2048) + descriptor_row=history([descriptor_only]) + need(descriptor_row['growth'][-3]==2*k+3+2048 and descriptor_row['growth'][-2]==2048, + 'Control copy and descriptor backing are separate coordinates') + unequal=Case((0,7,2),(0,5,1),11,( + Case((0,3,9),(0,2,7),5,(child(3,1,17,13,6),),output=4,slot=2), + child(3,1,21,7,8)),output=3,slot=1,descriptor_scratch=29) + nested_unequal=history([unequal],prefix=23) + leaf=child(k,1,128,output_len=128) + relay=[] + for depth in (1,2,8): + node=leaf + for _ in range(depth):node=Case((0,)*k,(0,)*k,children=(node,),output=128) + row=history([node]);need(row['growth'][-1]==128,'Shared relay uses history maximum, not depth sum');relay.append(row['capacities'][-1]) + return {'rotation':rotated,'fresh_totals':fresh,'erased_interior':erased_row, + 'same_boundary_tiny_interior':tiny_row,'warm_entry':warm, + 'chains':chain,'empty_frame':zero_row,'descriptor_copy':descriptor_row, + 'unequal_siblings':nested_unequal,'shared_relay_capacities':relay} + + +def source_case(prefix,late,peak_override=None): + k=16;a=adapter.Arena([bits(prefix,j) for j in range(k)],bits(prefix+3)) + relay=Tape(bits(prefix+5),BASE,a.counts);tapes=(*a.payloads,a.control,a.descriptor,relay) + origins=tuple(t.head for t in tapes);entry=tuple(len(t.cells) for t in tapes) + fields=(('u',1),('t',1))+((('y',2),('x',2)) if late else (('x',2),('y',2)))+(('b',1),) + layout=compact.Layout(fields,8);word=compact.Compact(1,1,1,0,'x','y',late) + maximum=compact_peak(layout.bits,layout.record_bits) + if peak_override is not None:maximum=peak_override + sizes=(0,)+tuple(j+2 for j in range(1,k));heads=(0,)+tuple(j//2 for j in range(1,k)) + leaf=Node((maximum,)*k,17,output=1024) + model=Node((1024,)+sizes[1:],43,(Cut(sizes,heads,43,leaf),)) + limits=capacities(origins,entry,extents(model,k));guard=Guard(tapes,limits) + saved=(streams.Tape,compact.Tape) + streams.Tape=compact.Tape=a.tape + try: + with guard.installed(): + parents=[a.tape(streams.Meter(),bits(n,j)) for j,n in enumerate(sizes)] + for j,role in enumerate(parents):role.read(heads[j]) + a.set_descriptor(bits(43));before=[snapshot(t) for t in tapes] + a.stack.push(a.present);a.present=[False]*k;a.sizes=[0]*k;a.heads=[0]*k;a.depth+=1 + raw=bytes(b for i in range(layout.records) for b in streams.bit_key(i,8)) + source=a.tape(streams.Meter(),raw);result=compact.execute(source,layout,word) + expected=bytearray(len(raw)) + for i in range(layout.records): + j=layout.encode(word.ideal(layout.decode(i),True)) + expected[j*8:(j+1)*8]=raw[i*8:(i+1)*8] + need(bytes(result.data)==expected,'Independent complete compact endpoint') + a.set_descriptor(bits(17));start=a.counts.total + output.return_output(a.payloads,a.control,a.descriptor,relay,result.slot,0) + need(a.counts.total-start==24388,'Unchanged complete source return invoice') + wanted=list(before);old,h=wanted[0];wanted[0]=(old+list(expected),h) + need([snapshot(t) for t in tapes]==wanted,'Complete source return state') + finally:streams.Tape,compact.Tape=saved + return {'prefix':prefix,'late':late,'records':layout.records,'record_bits':8, + 'per_role_local_bound':maximum,'capacities':[len(t.cells) for t in tapes], + 'grants':list(limits),'writes':guard.writes,'return_steps':24388, + 'output_sha256':hashlib.sha256(expected).hexdigest()} + + +def controls(): + rejected=[] + # An actual too-small grant rejects before its offending source write. + case=root_for(2,child(2,1,17));tapes,origins,_=bank(2) + caps=list(capacities(origins,origins,extents(case.model(),2)));caps[1]-=1 + try: + with Guard(tapes,caps).installed():execute(case,tapes) + except ValueError as e:need(str(e)=='Prospective per-tape backing grant','Specific quota rejection');rejected.append('one_cell_short') + else:raise ValueError('short grant accepted') + # read and move do not allocate, including well beyond the written end. + t=Tape();old=len(t.cells) + for _ in range(100):t.move(1);t.read() + need(len(t.cells)==old,'Reads/moves do not allocate') + t.write(BLANK);need(len(t.cells)==t.head+1,'Blank writes allocate') + rejected.append('blank_write_is_not_free_storage') + try:source_case(0,False,1024) + except ValueError as e: + need(str(e)=='Prospective per-tape backing grant','Keyed source exceeds payload-only grant') + rejected.append('omitted_actual_source_keys') + else:raise ValueError('payload-only compact grant accepted') + case=root_for(2,child(2,1,7,output_len=7));tapes,origins,_=bank(2) + caps=list(capacities(origins,origins,extents(case.model(),2)));caps[-1]=origins[-1] + try: + with Guard(tapes,caps).installed():execute(case,tapes) + except ValueError as e: + need(str(e)=='Prospective per-tape backing grant','Relay is separately allocated') + rejected.append('omitted_relay') + else:raise ValueError('relay-free grant accepted') + for bad in (Node((-1,0),0),Node((0,0),-1),Node((0,0),0,(Cut((0,0),(1,0),0,Node((0,0),0)),))): + try:extents(bad,2) + except ValueError:rejected.append('malformed_model') + else:raise ValueError('bad model accepted') + return rejected + + +def run(): + source=[source_case(prefix,late) for late in (False,True) for prefix in (0,257,4096)] + return {'status':'PASS_CONTINUATION_RETAINED_BACKING','census':census(), + 'discriminators':discriminators(),'source':source,'controls':controls()} + + +if __name__=='__main__': + p=argparse.ArgumentParser(description=__doc__);p.add_argument('--emit',action='store_true');args=p.parse_args() + result=run() + if not args.emit: + expected=json.loads((HERE/'RESULT.json').read_text()) + need(json.dumps(result,sort_keys=True,separators=(',',':'))==json.dumps(expected,sort_keys=True,separators=(',',':')), + 'Complete typed deterministic receipt') + print(json.dumps(result,indent=2,sort_keys=True))