From 9570df6e69824dd32bf58b6d66a8e57a790e3b85 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Fri, 16 Oct 2026 12:42:10 +0100 Subject: [PATCH] feat(research): tighten continuation backing bounds --- .../selected-continuation-backing/PROOF.md | 133 ++++++++ .../selected-continuation-backing/README.md | 128 ++++++++ .../selected-continuation-backing/RESULT.json | 234 +++++++++++++ .../SOURCES.json | 66 ++++ .../selected-continuation-backing/TASK.json | 151 +++++++++ .../VALIDATION.md | 69 ++++ .../selected-continuation-backing/VERIFY.json | 53 +++ .../test_verify.py | 99 ++++++ .../selected-continuation-backing/verify.py | 309 ++++++++++++++++++ 9 files changed, 1242 insertions(+) create mode 100644 research/selected-continuation-backing/PROOF.md create mode 100644 research/selected-continuation-backing/README.md create mode 100644 research/selected-continuation-backing/RESULT.json create mode 100644 research/selected-continuation-backing/SOURCES.json create mode 100644 research/selected-continuation-backing/TASK.json create mode 100644 research/selected-continuation-backing/VALIDATION.md create mode 100644 research/selected-continuation-backing/VERIFY.json create mode 100644 research/selected-continuation-backing/test_verify.py create mode 100644 research/selected-continuation-backing/verify.py diff --git a/research/selected-continuation-backing/PROOF.md b/research/selected-continuation-backing/PROOF.md new file mode 100644 index 0000000000..2c7f8c6686 --- /dev/null +++ b/research/selected-continuation-backing/PROOF.md @@ -0,0 +1,133 @@ +# A separate value-stack allowance + +The scientific source is unchanged Jose Manuel/jmbarrancoml PR2697, +`a53fdf4bcbe33c6732f0bec1badc8c023380f9d1`, authenticated through the +[PR2758 exports](../selected-continuation-storage/SNAPSHOT.json). +This proof refines PR2758's retained-array allowance. Its live-symbol bound, +stack grammar, successful arithmetic and source contracts remain predecessor +results. This is a written source argument, not a formal-kernel proof. + +## Quantified contract + +Fix a successfully initialized Callback, a valid coordinate, ancestor depth +`h >= 0`, and fixed index/residue digit lengths `I,R >= 2`. Assume a successful +`Callback.weight` execution satisfying the pinned source's chronological, +unit-denominator and fixed-word preconditions. Both stacks are private, empty, +with all four heads at one on entry. Observers do not mutate them. Their arrays +are the only four arrays counted here. Input programs, fields, numerical Words, +Python metadata, physical placement and other caller objects are excluded. + +Write + +```text +A = 2I + 4 +B = R + 3 +T = max(A,B) +F(h) = (h+1)T + hB. +``` + +In order pending main, pending reverse, values main, values reverse, define + +```text +c(0) = (A+1, A, B+1, B) +c(h) = (F(h)+1, T, (h+1)B+1, B), h >= 1. +``` + +For fresh arrays, each retained length is at most its coordinate of c. +For arbitrary erased, restored-head entry arrays with lengths `K_0,...,K_3`, +the coordinate bounds are `max(K_j,c_j)`. This includes warm history explicitly; +an aggregate entry bound alone is insufficient to infer the coordinate bounds. +Repeated successful calls with identical h,I,R keep the same coordinate bounds. + +Thus for fresh arrays, or earlier successful calls bounded coordinatewise, + +```text +retained backing at h=0 = 2A + 2B + 2 +retained backing at h>=1 <= F(h) + (h+1)B + T + B + 2. +``` + +The latter improves PR2758's `2F(h)+T+B+2` by `(h+1)T-B` cells. +The depth-zero formula is exact even if B>A. For h>=1 the stated improvement +is strictly positive. All counts include the four LEFT cells and erased tails. +They describe lengths of Tape.cells, not bytearray allocator capacity or heap +memory. No claim of caller success follows from this successful-call contract. + +## Value main stack invariant + +Every record pushed onto `values` by `weight` has tag RETURN and exactly B +symbols. Let k RETURN records precede the active request, and let its remaining +ancestor depth be d. Evaluation of that request adds at most d+1 records above +those k throughout its execution, including partial stack instructions. + +At depth zero, the root VALUE is removed from pending before one RETURN is +pushed. CONSTANT and UNIT also finish by pushing one RETURN. GOOD leaves one +MULTIPLY on pending and evaluates a child of depth at most d-1. It adds at most +d records. MULTIPLY pops that result before pushing its replacement, so it +cannot increase the maximum beyond k+d+1. + +For PAIR, the first child executes above k existing returns and adds at most +d records. It finishes with one additional return. The second child executes +above k+1 and adds at most d records, for at most k+d+1. Two CONSTANT children +instead reach k+2, which fits since d>=1. At combination PAIR pops both results +before pushing one replacement. Mixed children and unit resets only reduce the +remaining depth. These are the literal push/pop orders in +[controller.py](../selected-continuation-storage/vendor/controller.py). + +Apply the induction with k=0,d=h. The value main stack has at most h+1 complete +RETURN records and its partial push never exceeds the extent of the completed +record. Each pop overwrites existing cells and moves its main head backwards. +Its maximum written address is therefore at most `(h+1)B`, and its array length +at most `(h+1)B+1`. The +1 counts LEFT. + +## The other arrays and statement interiors + +PR2758 proves the combined live-symbol bound F(h), including partial pushes +and Stack.pop's copy-before-erase interior. In particular pending main has at +most F(h) contiguous symbols, so its array length is at most F(h)+1. + +A pending record has length A or B. Stack.pop first erases RECORD_END, then +copies exactly the other L-1 symbols into reverse. Hence pending reverse writes +at most T-1 positions above LEFT and has length at most T. Values contains only +RETURN, so its reverse has length at most B. At h=0 pending receives only the +initial VALUE; its two lengths are A+1 and A, even when B>A. + +Tape.write extends an array only through the address it writes. Erasure and +rewind never shorten an array, and do not extend it beyond these maxima. The +bounds thus hold at every write, including transient reversal. Arrays have no +constructor replacement overlap in this category: the same four Tape objects +are retained throughout weight. Arbitrary warm lengths are carried through by +the coordinatewise maximum with K. At successful return all non-LEFT content +is erased and heads restored; retained lengths remain. + +## Sharpness boundary + +If A>=B, a successful complete depth-h binary trace with two real ancestor +requests per PAIR reaches every coordinate maximum. The first descent has +h PAIR records and h+1 VALUE records on pending, reaching F(h). A leaf on the +last descent coexists with h completed first-sibling results on values, +reaching h+1 RETURNs. Popping a VALUE reaches A cells of pending reverse; +popping a RETURN reaches B cells of values reverse. The retained arrays +preserve all these maxima even though they occur at different cuts. +Their final total is exactly `(h+2)A+(2h+2)B+2`. + +This is conditional grammar sharpness. A fixed word length need not admit +arbitrarily deep numerical extents, and the finite fixtures are not assertions +of selected-catalogue membership. The literal GL64 depth-two fixture has +I=20,R=3,A=44,B=6, and reaches lengths `(145,44,19,6)`. Their sum is 214. +PR2758 already observed 214; this contribution supplies the directional +all-depth proof that makes that observation attain a certified upper bound, +rather than its previous allowance 340. + +For B>A and h>=1 the bound is conservative. For example the binary synthetic +h=2,I=14,R=32 trace reaches 343 below the new allowance 352. No general +optimality result is claimed in that regime. + +## Consequence and unresolved work + +This replaces one continuation backing component in a successful coefficient +call. It neither lowers the unchanged live-symbol bound nor changes executed +operations. It does not join numerical arenas, retained forms, program/field +arrays, native counters or suspended parent callers. A complete private reserve +must account for those objects at common cuts, then prove physical reuse, +movement, recursive grants and the outer contract. The selected frontier and +supplier admission remain unchanged. diff --git a/research/selected-continuation-backing/README.md b/research/selected-continuation-backing/README.md new file mode 100644 index 0000000000..0dbb6bcacb --- /dev/null +++ b/research/selected-continuation-backing/README.md @@ -0,0 +1,128 @@ +# Sharper retained backing for the selected coefficient continuation stacks + +The unchanged PR2697 coefficient evaluator's value stack stores at most +`h+1` RETURN records. This gives a smaller all-depth retained-array allowance +than PR2758's conservative symmetric bound. For the known literal GL64 +depth-two fixture, the certified allowance falls from 340 to 214 cells, +matching its already published observation. Execution and the selected +frontier are unchanged. + +For ancestor depth h, index/residue digit lengths I,R, set + +```text +A = 2I+4, B = R+3, T = max(A,B), F(h) = (h+1)T+hB + + pending main pending reverse values main values reverse +h = 0 A+1 A B+1 B +h >= 1 F(h)+1 T (h+1)B+1 B +``` + +The new total for h>=1 is `F(h)+(h+1)B+T+B+2`, improving +`2F(h)+T+B+2` by `(h+1)T-B`. At depth zero it is exactly `2A+2B+2`, +including when B>A. For arbitrary erased warm entry arrays with lengths K_j, +use the sum of `max(K_j,c_j)` over the four listed limits c_j. +[PROOF.md](PROOF.md) gives the quantified successful-call contract, source +induction, statement interiors and exact warm-history qualification. + +A successful complete binary real-child trace attains the bounds when A>=B. +This is conditional grammar sharpness. The general h>=1 bound is conservative +when B>A; no universal optimality claim is made for that regime. + +## Sources and added evidence + +Scientific source Jose Manuel/jmbarrancoml's +[PR2697](https://github.com/CrocSwap/integer-mult-bounds/pull/2697), exact +`a53fdf4bcbe33c6732f0bec1badc8c023380f9d1`, is authenticated through the +unchanged [PR2758 package](../selected-continuation-storage/README.md). +[SOURCES.json](SOURCES.json) pins the predecessor fixture, proof, snapshot, +four runtime modules and source notice. All nonstandard inputs are authenticated +before any module is executed, and loading compiles source bytes directly. +No predecessor export is copied or changed. + +The new verifier reuses PR2758's fixture recipes and literal algorithms. It +adds a separate per-array length observer at every actual Tape.write, with +quotas checked before growth. Its census covers 524 level-homogeneous branch +histories: GOOD, two-real-child PAIR, either mixed PAIR, two-constant PAIR and +UNIT through depth three, plus binary stress through depth six. Those fixtures +replace only step/preparation with finite unit tables; they are control tests. +Three additional fixtures execute actual GL64 matrix preparation/fallback at +depths 0,1,2 and return the predecessor's literal expected coefficients. +The depth-two retained lengths are exactly 145,44,19,6, totaling 214. + +[RESULT.json](RESULT.json) records 914240 synthetic tape writes, eight attaining +request-dominant binary/root fixtures, both scalar-dominant and request-dominant +stress cases, successful repeated calls and arbitrary 700-cell warm history. +Three embedded controls reject an actual one-cell-short value quota, use of +live content as backing, and omission of warm history. Nine behavioral tests +also check the B>A slack example 343 versus 352, source corruption, input limits, +and method restoration after both interior and context-entry quota rejection. +Acceptance remains enabled under `-O`. + +The warm fixture extends only the predecessor test's fresh-entry acceptance +allowance to the explicit entry history. Runtime source stays unchanged. +This is author-checked evidence with a separate internal source/proof review; +no independent human review or formal-kernel proof is claimed. The all-depth +conclusion rests on the written induction, not finite enumeration. + +## Reproduce + +Python 3.12, standard library only, from the repository root: + +```sh +python3.12 -I -Werror -B scripts/research_package.py \ + --package research/selected-continuation-backing +``` + +The registered replay authenticates inputs and runs normal/optimized checks +and behavioral tests. Direct replay is read-only and compares the complete +typed receipt. `verify.py --emit` prints a new receipt without replacing it. +Exact environment and final commands/results are in [VALIDATION.md](VALIDATION.md). + +## Scope and research decision + +The adversarial-audit draw supplied `uniform-transfer-audit`, refined to this +one selected-implementation storage implication under priority revision 5. +[TASK.json](TASK.json) records the nonce, source pins, overlap coverage, +[canonical claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/2319#discussioncomment-18972137) +and bounded stopping rule. PR2758's existing live-symbol proof and 214-cell +observation retain their credit; the addition is the directional all-depth +backing theorem and executable per-tape rejection controls. + +Decision: finish this component and hand it off. The proof assumes successful +private weight execution and preserves all arithmetic/chronology/termination +premises. Numerical arenas, retained forms, program/field arrays, other caller +objects, physical reuse and movement, recursive grants, complete private +reserve, supplier admission and a new kappa remain unproved here. +The selected cold supplier replay is not required for this independent package +and was not rerun. No hosted-CI pass is claimed. + +Build the Lever led to the authenticated per-tape checker. Prove It Works led +to literal lengths, returned coefficients, cleanup and real quota failures. +Test Behavior, Not Implementation led to the nine execution-based tests. +The managed-runtime and observation deviations from Power of Ten, bounded +fixture domain, cleanup and source constraints are recorded in TASK.json. + +## Open next questions + +1. Can the B>A allowance be made optimal? Derive a joint historical-maximum + recurrence from the 343 versus 352 example. The possible incompatibility of + separate stack maxima is the blocker; this matters for a tighter component + in residue-dominant regimes. +2. Join the continuation component to numerical, program/field and native-action + backing at common cuts, starting with one pinned actual Callback and its + entry history. Complete object inventory, physical mapping/movement and + outer recursive grants block a total reserve conclusion. + +Both questions have structured first steps and blockers in TASK.json. + +## Credit + +Nick Petalas. New work is Apache-2.0. Jose Manuel/jmbarrancoml supplied the +unchanged callback, tape algorithms and retained implementation lineage. +PR2758 supplies the prior live/backing argument and fixture recipes. The +unchanged predecessor [NOTICE.md](../selected-continuation-storage/vendor/NOTICE.md) +retains its full source credit. PR2770's numerical lifetime component, +Ross Richardson's PR2831 arena backing, and the separate PR2923 native ADD +numerical/countdown join remain distinct contributions. +Substantial automated assistance was used for analysis, proof drafting, +implementation and internal review. diff --git a/research/selected-continuation-backing/RESULT.json b/research/selected-continuation-backing/RESULT.json new file mode 100644 index 0000000000..cf843ce48e --- /dev/null +++ b/research/selected-continuation-backing/RESULT.json @@ -0,0 +1,234 @@ +{ + "controls": [ + "one_value_cell_short", + "live_content_used_as_backing", + "warm_history_omitted" + ], + "largest_binary": [ + { + "I": 38, + "R": 4, + "backing": 740, + "bound": 740, + "entry": [ + 1, + 1, + 1, + 1 + ], + "lengths": [ + 603, + 80, + 50, + 7 + ], + "limits": [ + 603, + 80, + 50, + 7 + ], + "literal_gl64": false, + "live_peak": 602, + "modes": "BBBBBB", + "old_bound": 1293, + "pops": 317, + "repeats": 1, + "writes": 45326 + }, + { + "I": 38, + "R": 128, + "backing": 2527, + "bound": 2884, + "entry": [ + 1, + 1, + 1, + 1 + ], + "lengths": [ + 1347, + 131, + 918, + 131 + ], + "limits": [ + 1704, + 131, + 918, + 131 + ], + "literal_gl64": false, + "live_peak": 1703, + "modes": "BBBBBB", + "old_bound": 3670, + "pops": 317, + "repeats": 1, + "writes": 139566 + } + ], + "literal_gl64": [ + { + "I": 8, + "R": 3, + "backing": 54, + "bound": 54, + "entry": [ + 1, + 1, + 1, + 1 + ], + "lengths": [ + 21, + 20, + 7, + 6 + ], + "limits": [ + 21, + 20, + 7, + 6 + ], + "literal_gl64": true, + "live_peak": 20, + "modes": "", + "old_bound": 68, + "pops": 2, + "repeats": 1, + "writes": 100 + }, + { + "I": 14, + "R": 3, + "backing": 122, + "bound": 122, + "entry": [ + 1, + 1, + 1, + 1 + ], + "lengths": [ + 71, + 32, + 13, + 6 + ], + "limits": [ + 71, + 32, + 13, + 6 + ], + "literal_gl64": true, + "live_peak": 70, + "modes": "B", + "old_bound": 180, + "pops": 7, + "repeats": 1, + "writes": 466 + }, + { + "I": 20, + "R": 3, + "backing": 214, + "bound": 214, + "entry": [ + 1, + 1, + 1, + 1 + ], + "lengths": [ + 145, + 44, + 19, + 6 + ], + "limits": [ + 145, + 44, + 19, + 6 + ], + "literal_gl64": true, + "live_peak": 144, + "modes": "BB", + "old_bound": 340, + "pops": 17, + "repeats": 1, + "writes": 1438 + } + ], + "observed_writes": 914240, + "repeated": { + "I": 14, + "R": 4, + "backing": 172, + "bound": 172, + "entry": [ + 1, + 1, + 1, + 1 + ], + "lengths": [ + 111, + 32, + 22, + 7 + ], + "limits": [ + 111, + 32, + 22, + 7 + ], + "literal_gl64": false, + "live_peak": 110, + "modes": "BB", + "old_bound": 261, + "pops": 34, + "repeats": 2, + "writes": 2284 + }, + "scope": "Four continuation arrays; successful private weight calls. No complete reserve or supplier admission.", + "sharp_cases": 8, + "source_head": "a53fdf4bcbe33c6732f0bec1badc8c023380f9d1", + "status": "PASS_SELECTED_CONTINUATION_BACKING", + "synthetic_cases": 524, + "warm": { + "I": 14, + "R": 4, + "backing": 700, + "bound": 700, + "entry": [ + 500, + 70, + 90, + 40 + ], + "lengths": [ + 500, + 70, + 90, + 40 + ], + "limits": [ + 500, + 70, + 90, + 40 + ], + "literal_gl64": false, + "live_peak": 110, + "modes": "BB", + "old_bound": 261, + "pops": 34, + "repeats": 2, + "writes": 2284 + } +} diff --git a/research/selected-continuation-backing/SOURCES.json b/research/selected-continuation-backing/SOURCES.json new file mode 100644 index 0000000000..c0dccac10b --- /dev/null +++ b/research/selected-continuation-backing/SOURCES.json @@ -0,0 +1,66 @@ +{ + "schema_version": 1, + "base_commit": "a7482490b4ca256db67d767a33fa6f7553060807", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "889b95d936746df124872133ae1e7cc339adcb92", + "sha256": "7d185cd8c2af35988d638d969748ad7b670f902606444dbfc748e4402c340df6" + }, + { + "path": "research/selected-continuation-storage/README.md", + "usage": "input", + "git_blob": "6360ea865650a245fcce874da0607fca2cb11381", + "sha256": "a37f748127416c5ad5ba87631d2ec94ebdf153d23ef11ad824f014a97a7fadda" + }, + { + "path": "research/selected-continuation-storage/SNAPSHOT.json", + "usage": "input", + "git_blob": "f438fe3d2565b2ac8c60c5013b4f0e2b754ccab2", + "sha256": "e987e015f7ae9ed5fd97efdffde3b4d179723b8facc433b33fbf6e3af771c9b8" + }, + { + "path": "research/selected-continuation-storage/vendor/NOTICE.md", + "usage": "input", + "git_blob": "ef9f81510db86eaf2f0a7191d85e92a6db30ddc0", + "sha256": "c446b32b8a621844fb2fbe654810c8122035bdd43fed2132f1137d98cb6f9943" + }, + { + "path": "research/selected-continuation-storage/vendor/controller.py", + "usage": "input", + "git_blob": "c631a9e77fbcccf0e8f448adc22978728aed7b60", + "sha256": "fa09146991f6c04e6f4b6eb9bf0c8e103e70e90a0e402ff3d69814e6aac8ff8c" + }, + { + "path": "research/selected-continuation-storage/vendor/matrices.py", + "usage": "input", + "git_blob": "5d497353efbb9eeaaf4facd96ab40ffb0f3aa20d", + "sha256": "00b687434039b54529ee092e34f9435cfcd66e0816eb3bd2a6688c73f4e01459" + }, + { + "path": "research/selected-continuation-storage/vendor/records.py", + "usage": "input", + "git_blob": "4f00467a0ff580954ad2fd0c7380240c753ddef3", + "sha256": "0c9c4b23e998597fb877bb1a29da69ac869b68262abe635b162b4dba9c69b372" + }, + { + "path": "research/selected-continuation-storage/vendor/words.py", + "usage": "input", + "git_blob": "8d4ba37e2778acb35b34e0719df2caf138fbeb50", + "sha256": "5c37f57708ba3131bdcb03139f9dbc29886bee44569c09cbba51b68f75acd7f9" + }, + { + "path": "research/selected-continuation-storage/verify.py", + "usage": "input", + "git_blob": "b05612fb867a58751dbb39cb9d821fbdd9dcfdf6", + "sha256": "5af517298df18677cf391dc83173774472c0db434ccd9f41160fcb1e970288f0" + } + ] +} diff --git a/research/selected-continuation-backing/TASK.json b/research/selected-continuation-backing/TASK.json new file mode 100644 index 0000000000..a5e850eb0b --- /dev/null +++ b/research/selected-continuation-backing/TASK.json @@ -0,0 +1,151 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 5, + "base_commit": "a7482490b4ca256db67d767a33fa6f7553060807", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Can one exact all-size/compiler, precision, hosting or restoration implication be proved or falsified?", + "starting_points": [ + "certificates/selected-result.json", + "docs/audit.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 the selected review scope and choose one exact all-size or precision implication.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write its quantified inputs and conclusion; find a missing hypothesis or construct a minimal exact adversarial instance.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": [ + "Choose one tape, precision, hosting or restoration lemma." + ], + "scope_change_triggers": [ + "Replacing a quantified obligation with another finite smoke test." + ], + "overlap_terms": [ + "uniform transfer", + "all-size", + "precision" + ] + }, + "scope_status": "refined", + "actual_scope": "Prove a source-bound directional retained-backing envelope for the four PR2697 Callback.weight continuation arrays, including the value-stack h+1 RETURN bound, depth zero, arbitrary warm history and conditional request-dominant grammar sharpness.", + "scope_change_reason": "The drawn adversarial-audit suggestions include uniform-transfer-audit. The current numerical capacity-prefix question is already covered by newer work; this distinct quantified continuation storage implication sharpens PR2758 without repeating its known 214-cell measurement.", + "bottleneck_link": "A source-bound retained-backing allowance is one component of the selected BIT implementation reserve. This strengthens its explicit storage ledger without a supplier or kappa claim.", + "budget_minutes": 60, + "stop_rule": "Stop after one all-depth source proof, bounded literal/synthetic replay, meaningful quota failures, independent internal review and a focused upstream PR; do not expand into total reserve or physical reuse.", + "outcome": "completed", + "evidence": "PROOF.md; RESULT.json; per-write verify.py; nine behavioral groups in test_verify.py", + "author": "Nick Petalas", + "ai_assistance": "Substantial automated assistance was used for source analysis, proof drafting, implementation and internal review. No independent human or formal-kernel review is claimed.", + "open_questions": [ + { + "question": "Can the B>A retained-backing allowance be made optimal for the admitted grammar?", + "why_it_matters": "The per-stack maximum sum can be conservative in the residue-dominant regime.", + "first_step": "Derive a joint pending/value historical-maximum recurrence, starting with the explicit h=2,I=14,R=32 trace of 343 versus the allowance 352.", + "blocked_by": "Individual maximum attainability does not establish their joint attainability for one admitted trace." + }, + { + "question": "How does this actual continuation component join the numerical, program/field and native-action backing at common cuts?", + "why_it_matters": "A component bound alone cannot certify total private reserve or physical reuse.", + "first_step": "Use this c(h) with the pinned actual numerical-arena and native ADD backing contracts, including caller entry history and callback ownership.", + "blocked_by": "The complete inventory, physical mapping/movement and outer recursive grants remain separate obligations." + } + ], + "chooser_nonce": "418fa91bf4817bc4cafab75ace5f4772", + "drawn_track": "adversarial-audit", + "scientific_source_head": "a53fdf4bcbe33c6732f0bec1badc8c023380f9d1", + "canonical_claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2319#discussioncomment-18972137", + "scope_limitations": [ + "Successful private Callback.weight calls only; capacity/termination and arithmetic contracts remain assumptions.", + "The A>=B sharpness is a conditional grammar statement, not membership in the selected catalogue.", + "Numerical arenas, program/fields, other caller objects, physical reuse/movement, total reserve, supplier admission and new kappa are not established." + ], + "overlap_entry": { + "searched_at": "2026-10-16T11:29:28.062228+00:00", + "coverage": { + "open_prs": { + "fetched_at": "2026-10-16T11:26:11.942484+00:00", + "complete_pagination": true, + "records": 498 + }, + "discussions": { + "fetched_at": "2026-10-16T11:26:37.637090+00:00", + "complete_pagination": true, + "records": 1598 + }, + "closed_prs": { + "fetched_at": "2026-10-16T11:29:27.901701+00:00", + "complete_pagination": true, + "records": 2119 + } + }, + "limitations": "Remote PR scope includes open and closed/merged titles and bodies, with separate coverage and timestamps. State changes are deduplicated by latest PR update; snapshots are not atomic. No code diffs or arbitrary package files are searched. Recheck relevant heads before submission.", + "nearest": [ + "PR2758 continuation live/backing proof, retained immutable on main", + "PR2770 callback numerical live-word bound, different arrays", + "PR2831 numerical arena high-water backing, different category", + "PR2923 native ADD numerical/countdown join, leaves actual continuation backing separate" + ], + "novelty_statement": "Metadata and local-note searches found no matching directional value-stack theorem. They do not search every code diff or unpublished work." + }, + "engineering": { + "principles": [ + "Build the Lever: authenticated per-write, per-tape replay instead of a new observation-only note.", + "Prove It Works: actual returned coefficients, tape lengths, erasure/head restoration and one-cell-short rejection.", + "Test Behavior, Not Implementation: literal array extents and actual quota errors are asserted." + ], + "power_of_ten_deviations": [ + { + "rules": [ + 3, + 8, + 9 + ], + "location": "verify.py predecessor loading and scoped observers", + "reason": "Python allocates heap objects; source-authenticated runtime modules and temporary fixed-method instrumentation are required to execute the retained source.", + "scope": "One sequential standard-library fixture process; h<=6, digit lengths<=128, four entry tapes<=1024 cells each, existing fixture arenas fixed at 256 numerical slots or literal source capacity.", + "compensating_control": "Eight declared predecessor inputs are SHA256/Git-blob checked before compilation, all method changes restored on success or failure including context entry, source modules reject preload, and registered subprocesses have explicit timeouts.", + "verification": "test_verify.py invalid-input/source/quota/restoration controls and registered normal/optimized replay.", + "follow_up": "Revisit managed allocation and observation seams when replacing the model with a physical allocator/compiler." + } + ], + "predecessor_policy": "Retained scientific code and original fixture code are immutable inputs. Their bounded fixture loops are reused; no source rewrite or selected compiler replacement is performed." + }, + "submission_refresh": { + "canonical_main": "3bee87dc2bbb012623ecece9df6b27c6d15706fb", + "priority_revision": 5, + "overlap_checked_at": "2026-10-16T11:39:02.037766+00:00", + "coverage": { + "open_prs": { + "fetched_at": "2026-10-16T11:38:13.861611+00:00", + "complete_pagination": true, + "records": 495 + }, + "discussions": { + "fetched_at": "2026-10-16T11:38:40.451698+00:00", + "complete_pagination": true, + "records": 1601 + }, + "closed_prs": { + "fetched_at": "2026-10-16T11:39:01.917550+00:00", + "complete_pagination": true, + "records": 2122 + } + }, + "warnings": [], + "relevant_changed_paths": [], + "decision": "Retain exact initial scientific baseline. New main review/navigation/reconciliation changes do not alter consumed sources, priorities, selected record or replay runner; review1900 leaves all earlier unresolved obligations separate." + } +} diff --git a/research/selected-continuation-backing/VALIDATION.md b/research/selected-continuation-backing/VALIDATION.md new file mode 100644 index 0000000000..38885cbb5f --- /dev/null +++ b/research/selected-continuation-backing/VALIDATION.md @@ -0,0 +1,69 @@ +# Local verification and review + +Environment: macOS 27.0.1 arm64, CPython 3.12.15. Standard library only. +The configured Python 3.12 executable was +`/Users/nick/.local/share/uv/python/cpython-3.12-macos-aarch64-none/bin/python3.12`. +A separate optimized compatibility run used Homebrew CPython 3.14.8. + +From the repository root: + +```sh +python3.12 -I -Werror -B scripts/research_package.py \ + --package research/selected-continuation-backing --check-only +python3.12 -I -Werror -B scripts/research_package.py \ + --package research/selected-continuation-backing +python3.14 -I -O -Werror -B research/selected-continuation-backing/verify.py +python3.14 -I -O -Werror -B research/selected-continuation-backing/test_verify.py +python3.12 -I -Werror -B -m unittest discover -s tests -p 'test_research_*.py' +uvx ruff check research/selected-continuation-backing --select E4,E7,E9,F,I,UP,B,RUF +uvx ruff format --check research/selected-continuation-backing +``` + +Registered metadata/source-pin check passes. Normal and optimized registered +replays compare the complete typed RESULT.json; nine behavioral tests pass. +The research workflow suite passes 144 tests with seven platform-specific skips. +Scoped Ruff checks and formatting pass. No hosted-CI pass is claimed. + +The initial arbitrary-warm fixture failed the reused predecessor's fresh-entry +backing assertion. The fixture adapter now explicitly permits the independent +warm-entry allowance while preserving the old live-symbol check and unchanged +runtime. A rejecting context entry also required explicit restoration of the +observers, since Python does not call `__exit__` when `__enter__` raises. Real +quota failure followed by a successful fresh replay tests that cleanup. + +A separate internal reviewer derived the h+1 RETURN bound from the literal +source, checked partial pushes/reversal and sharpness, independently ran the +complete fixed receipt and the original eight tests on CPython 3.12.15, and +identified the warm-history and fixture-label qualifications now enforced. +The ninth test checks the latter: literal fixtures accept only binary modes, +R=3 and one call. Repeated and arbitrary-warm evidence uses the explicitly +synthetic step/preparation fixtures. This is internal review, not independent +human review or formal verification. + +All new functions fit below 60 physical lines after standard formatting. The +new fixture loops have explicit domain bounds: six branch modes, depths 0..3 +for the complete 524-history census, binary stress depths 4..6, two word regimes, +three literal fixtures, one/two evaluations and four entry extents <=1024. +The numerical and source tables are bounded predecessor fixtures. Existing +runtime loops and managed allocations retain their source contracts; no fixed +physical-heap implementation is inferred. The exact managed-runtime/source- +loading/observer deviations and compensating controls are in TASK.json. + +Initial main was a7482490b4ca256db67d767a33fa6f7553060807. Submission refresh +found 3bee87dc2bbb012623ecece9df6b27c6d15706fb, with unchanged consumed +scientific inputs, priority revision 5, selected record and registered runner. +The changed current-status/review1900 navigation retains the frontier and +separates pending follow-ups. Complete refreshed metadata coverage at +11:38 through 11:39 UTC includes 495 open PRs, 2122 closed/merged PRs and 1601 Discussion +records, with no warning. Arbitrary diffs and unpublished work remain outside +that coverage. TASK.json preserves the exact timestamps and compatibility +comparison. Frozen inputs and the selected frontier are unchanged. + +## Attention + +Review capability: a separate read-only internal source/proof and verifier +review. Its concrete qualifications were incorporated. The local decision +trail records the failed warm test and metadata checks. No remaining blocking +flag was identified. The important scientific limits remain successful-call +premises, conditional grammar sharpness, B>A slack and the unjoined physical +reserve. No full selected supplier replay or formal-kernel proof was run. diff --git a/research/selected-continuation-backing/VERIFY.json b/research/selected-continuation-backing/VERIFY.json new file mode 100644 index 0000000000..9f6ffe2cb5 --- /dev/null +++ b/research/selected-continuation-backing/VERIFY.json @@ -0,0 +1,53 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/selected-continuation-storage/README.md", + "research/selected-continuation-storage/SNAPSHOT.json", + "research/selected-continuation-storage/vendor/NOTICE.md", + "research/selected-continuation-storage/vendor/controller.py", + "research/selected-continuation-storage/vendor/matrices.py", + "research/selected-continuation-storage/vendor/records.py", + "research/selected-continuation-storage/vendor/words.py", + "research/selected-continuation-storage/verify.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-Werror", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "524 bounded branch histories; actual per-tape write lengths; GL64 depth0..2; warm/repeated backing, three real quota failures and fixed typed receipt" + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Identical source/length/receipt acceptance with assertions disabled" + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 30, + "checks": "Nine behavior groups including literal sharp/slack regimes, quota/entry failure restoration, warm history, source corruption and fixture boundaries" + } + ] +} diff --git a/research/selected-continuation-backing/test_verify.py b/research/selected-continuation-backing/test_verify.py new file mode 100644 index 0000000000..af3bfbe92a --- /dev/null +++ b/research/selected-continuation-backing/test_verify.py @@ -0,0 +1,99 @@ +#!/usr/bin/env python3 +"""Behavioral checks of literal tape lengths and actual quota failures.""" + +from __future__ import annotations + +import importlib.util +import json +import tempfile +import unittest +from pathlib import Path +from unittest.mock import patch + +SPEC = importlib.util.spec_from_file_location( + "backing_check", Path(__file__).with_name("verify.py") +) +CHECK = importlib.util.module_from_spec(SPEC) +SPEC.loader.exec_module(CHECK) + + +class BackingTests(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.predecessor = CHECK.authenticate() + cls.modules = cls.predecessor.load_source() + + def run_case(self, modes="BB", bits=4, **options): + return CHECK.execute(self.predecessor, self.modules, modes, bits, **options) + + def test_binary_tape_lengths(self): + result = self.run_case() + self.assertEqual(result["lengths"], (111, 32, 22, 7)) + self.assertEqual(result["backing"], 172) + + def test_depth_zero_scalar_dominant_exactness(self): + result = self.run_case("", 32) + self.assertEqual(result["lengths"], (21, 20, 36, 35)) + self.assertEqual(result["backing"], 112) + + def test_scalar_dominant_bound_is_conservative(self): + result = self.run_case("BB", 32) + self.assertEqual(result["lengths"], (167, 35, 106, 35)) + self.assertEqual((result["backing"], result["bound"]), (343, 352)) + + def test_one_cell_short_rejects_and_methods_restore(self): + write, pop = self.modules[1].Tape.write, self.modules[1].Stack.pop + weight = self.modules[2].Callback.weight + with self.assertRaisesRegex(ValueError, "directional tape capacity"): + self.run_case(short=1) + self.assertIs(self.modules[1].Tape.write, write) + self.assertIs(self.modules[1].Stack.pop, pop) + self.assertIs(self.modules[2].Callback.weight, weight) + self.assertEqual(self.run_case()["backing"], 172) + + def test_erased_backing_outlives_live_content(self): + with self.assertRaisesRegex(ValueError, "joint tape capacity"): + self.run_case(total_quota=114) + self.assertEqual(self.run_case()["live_peak"], 110) + self.assertEqual(self.run_case()["backing"], 172) + + def test_warm_history_and_repeated_evaluation(self): + self.assertEqual(self.run_case(repeats=2)["backing"], 172) + result = self.run_case(warm=(500, 70, 90, 40), repeats=2) + self.assertEqual(result["lengths"], (500, 70, 90, 40)) + self.assertEqual(result["backing"], 700) + with self.assertRaisesRegex(ValueError, "joint tape capacity"): + self.run_case(warm=(500, 70, 90, 40), total_quota=172) + self.assertEqual(self.run_case()["backing"], 172) + + def test_bad_manifest_fails_before_source_execution(self): + manifest = json.loads((CHECK.PACKAGE / "SOURCES.json").read_text()) + item = next(item for item in manifest["files"] if item["usage"] == "input") + item["sha256"] = "0" * 64 + with tempfile.TemporaryDirectory() as directory: + temporary = Path(directory) + (temporary / "SOURCES.json").write_text(json.dumps(manifest)) + with patch.object(CHECK, "PACKAGE", temporary): + with self.assertRaisesRegex(ValueError, "predecessor SHA256"): + CHECK.authenticate() + + def test_invalid_fixture_boundary(self): + for modes, bits, options in ( + ("BBBBBBB", 4, {}), + ("X", 4, {}), + ("BB", True, {}), + ("BB", 4, {"repeats": 3}), + ): + with self.assertRaisesRegex(ValueError, "bounded fixture"): + self.run_case(modes, bits, **options) + self.assertEqual(self.run_case()["backing"], 172) + + def test_literal_fixture_rejects_mislabelled_parameters(self): + for modes, bits, repeats in (("G", 3, 1), ("BB", 4, 1), ("BB", 3, 2)): + with self.assertRaisesRegex(ValueError, "literal GL64 fixture"): + self.run_case(modes, bits, literal=True, repeats=repeats) + self.assertEqual(self.run_case()["backing"], 172) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/selected-continuation-backing/verify.py b/research/selected-continuation-backing/verify.py new file mode 100644 index 0000000000..b244c7ff2d --- /dev/null +++ b/research/selected-continuation-backing/verify.py @@ -0,0 +1,309 @@ +#!/usr/bin/env python3 +"""Check directional backing bounds on authenticated PR2697 continuation tapes.""" + +from __future__ import annotations + +import argparse +import hashlib +import itertools +import json +from pathlib import Path +from types import ModuleType + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +PREDECESSOR = ROOT / "research/selected-continuation-storage" +HEAD = "a53fdf4bcbe33c6732f0bec1badc8c023380f9d1" + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def capacities(depth, index_bits, residue_bits): + need(type(depth) is int and 0 <= depth <= 1_000_000, "bounded nonnegative depth") + need( + all(type(b) is int and 2 <= b <= 1_000_000 for b in (index_bits, residue_bits)), + "bounded fixed word lengths", + ) + request, scalar = 2 * index_bits + 4, residue_bits + 3 + if depth == 0: + return (request + 1, request, scalar + 1, scalar) + largest = max(request, scalar) + live = (depth + 1) * largest + depth * scalar + return (live + 1, largest, (depth + 1) * scalar + 1, scalar) + + +def authenticate(): + manifest = json.loads((PACKAGE / "SOURCES.json").read_text()) + inputs = [item for item in manifest["files"] if item["usage"] == "input"] + expected = {"README.md", "verify.py", "SNAPSHOT.json"} | { + "vendor/" + name + for name in ( + "words.py", + "records.py", + "matrices.py", + "controller.py", + "NOTICE.md", + ) + } + need(len(inputs) == len(expected), "closed predecessor input inventory") + for item in inputs: + path = Path(item["path"]) + need( + path.as_posix().startswith("research/selected-continuation-storage/"), + "canonical predecessor path", + ) + relative = path.relative_to("research/selected-continuation-storage").as_posix() + need(relative in expected, "declared predecessor input") + expected.remove(relative) + source = ROOT / path + need(not source.is_symlink() and source.is_file(), "regular source input") + raw = source.read_bytes() + need(hashlib.sha256(raw).hexdigest() == item["sha256"], "predecessor SHA256") + blob = hashlib.sha1(b"blob " + str(len(raw)).encode() + b"\0" + raw).hexdigest() + need(blob == item["git_blob"], "predecessor Git blob") + need(not expected, "complete predecessor inputs") + snapshot = json.loads((PREDECESSOR / "SNAPSHOT.json").read_text()) + need(snapshot["head"] == HEAD, "scientific source head") + module = ModuleType("continuation_predecessor") + path = PREDECESSOR / "verify.py" + module.__file__ = str(path) + # The bytes and every nonstandard dependency were authenticated above. + exec( + compile(path.read_bytes(), str(path), "exec", dont_inherit=True), + module.__dict__, + ) + return module + + +def observer_type(predecessor, limits, collected, warm, total_quota): + class Directional(predecessor.Census): + """Observe each actual Tape.write and enforce before any growing write.""" + + def __init__(self, records, stacks, direct=False): + super().__init__(records, stacks, direct) + for tape, length in zip(self.tapes, warm, strict=True): + tape.cells.extend([records.BLANK] * (length - len(tape.cells))) + self.entry = tuple(len(tape.cells) for tape in self.tapes) + self.limits = tuple( + max(k, c) for k, c in zip(self.entry, limits, strict=True) + ) + self.lengths = self.entry + collected.append(self) + + def __enter__(self): + try: + return super().__enter__() + except Exception: + # Python does not call __exit__ when __enter__ rejects. + super().__exit__() + raise + + def scan(self): + super().scan() + actual = tuple(len(tape.cells) for tape in self.tapes) + need( + all(k <= c for k, c in zip(actual, self.limits, strict=True)), + "directional tape capacity", + ) + self.lengths = actual + if total_quota is not None: + need(sum(actual) <= total_quota, "joint tape capacity") + + def write(self, tape, symbol): + if id(tape) in self.identities: + position = self.tapes.index(tape) + proposed = max(len(tape.cells), tape.head + 1) + need(proposed <= self.limits[position], "directional tape capacity") + if total_quota is not None: + other = sum(len(t.cells) for t in self.tapes if t is not tape) + need(other + proposed <= total_quota, "joint tape capacity") + super().write(tape, symbol) + self.scan() + + return Directional + + +def fixture_limits(modes, residue_bits, literal, short, warm, repeats): + depth = len(modes) + need( + depth <= 6 and all(mode in "GBLRTU" for mode in modes), "bounded fixture modes" + ) + need(type(repeats) is int and repeats in (1, 2), "bounded fixture repetitions") + need( + type(residue_bits) is int and 2 <= residue_bits <= 128 and short in (0, 1), + "bounded fixture word/quota", + ) + need( + type(literal) is bool + and ( + not literal or (set(modes) <= {"B"} and residue_bits == 3 and repeats == 1) + ), + "literal GL64 fixture uses binary modes, three residue bits and one call", + ) + need( + len(warm) == 4 and all(type(k) is int and 1 <= k <= 1024 for k in warm), + "four bounded entry tape extents", + ) + index_bits = 6 * (depth + 1) + 2 if literal else max(8, 6 * depth + 2) + limits = list(capacities(depth, index_bits, residue_bits)) + limits[2] -= short + return limits + + +def execute( + predecessor, + modules, + modes, + residue_bits, + *, + literal=False, + short=0, + warm=(1, 1, 1, 1), + repeats=1, + total_quota=None, +): + limits = fixture_limits(modes, residue_bits, literal, short, warm, repeats) + depth = len(modes) + collected = [] + census, weight = predecessor.Census, modules[2].Callback.weight + original_bound = predecessor.bound + + def warm_bound(h, i, r): + live, backing = original_bound(h, i, r) + # Extend only the predecessor fixture's fresh-entry acceptance to our + # explicit warm-entry theorem. The literal scientific code is unchanged. + return live, max( + backing, sum(max(k, c) for k, c in zip(warm, limits, strict=True)) + ) + + def repeated(callback, coordinate): + for _ in range(repeats - 1): + result = weight(callback, coordinate) + callback.residue.free(result) + need( + callback.pending.empty() and callback.values.empty(), + "repeat entry restored", + ) + return weight(callback, coordinate) + + predecessor.Census = observer_type( + predecessor, limits, collected, warm, total_quota + ) + predecessor.bound = warm_bound + modules[2].Callback.weight = repeated + try: + result = ( + predecessor.literal_case(modules, depth) + if literal + else predecessor.run_case(modules, modes, residue_bits) + ) + finally: + predecessor.Census = census + predecessor.bound = original_bound + modules[2].Callback.weight = weight + need(len(collected) == 1, "one private callback census") + observed = collected[0] + return observation(result, observed, modes, literal, repeats, original_bound) + + +def observation(result, observed, modes, literal, repeats, original_bound): + return { + "modes": modes, + "I": result["I"], + "R": result["R"], + "literal_gl64": literal, + "repeats": repeats, + "entry": observed.entry, + "lengths": observed.lengths, + "limits": observed.limits, + "backing": observed.backing_peak, + "bound": sum(observed.limits), + "old_bound": original_bound(len(modes), result["I"], result["R"])[1], + "live_peak": observed.peak, + "writes": observed.writes, + "pops": observed.pops, + } + + +def controls(predecessor, modules): + rejected = [] + for name, options in ( + ("one_value_cell_short", {"short": 1}), + ("live_content_used_as_backing", {"total_quota": 112}), + ("warm_history_omitted", {"warm": (500, 70, 90, 40), "total_quota": 214}), + ): + try: + execute(predecessor, modules, "BB", 3, **options) + except ValueError as error: + need("tape capacity" in str(error), "actual quota rejection") + rejected.append(name) + else: + raise ValueError("invalid capacity accepted: " + name) + need( + execute(predecessor, modules, "BB", 3)["backing"] == 166, + "observer methods restored after entry rejection", + ) + return rejected + + +def verify(): + predecessor = authenticate() + modules = predecessor.load_source() + cases = [] + for depth in range(4): + for modes in itertools.product("GBLRTU", repeat=depth): + for bits in (4, 32): + cases.append(execute(predecessor, modules, "".join(modes), bits)) + for depth in (4, 5, 6): + for bits in (4, 128): + cases.append(execute(predecessor, modules, "B" * depth, bits)) + sharp = [ + c + for c in cases + if (not c["modes"] or set(c["modes"]) == {"B"}) and 2 * c["I"] + 4 >= c["R"] + 3 + ] + need( + all(c["lengths"] == c["limits"] for c in sharp), + "sharp request-dominant envelope", + ) + literal = [ + execute(predecessor, modules, "B" * h, 3, literal=True) for h in range(3) + ] + need(literal[2]["lengths"] == (145, 44, 19, 6), "literal GL64 depth-two backing") + repeated = execute(predecessor, modules, "BB", 4, repeats=2) + warm = execute(predecessor, modules, "BB", 4, warm=(500, 70, 90, 40), repeats=2) + need(warm["lengths"] == (500, 70, 90, 40), "warm backing retained through reuse") + return { + "status": "PASS_SELECTED_CONTINUATION_BACKING", + "source_head": HEAD, + "synthetic_cases": len(cases), + "sharp_cases": len(sharp), + "observed_writes": sum(c["writes"] for c in cases), + "largest_binary": [c for c in cases if c["modes"] == "BBBBBB"], + "literal_gl64": literal, + "repeated": repeated, + "warm": warm, + "controls": controls(predecessor, modules), + "scope": "Four continuation arrays; successful private weight calls. No complete reserve or supplier admission.", + } + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--emit", action="store_true") + args = parser.parse_args() + result = verify() + if not args.emit: + expected = json.loads((PACKAGE / "RESULT.json").read_text()) + need( + json.dumps(result, sort_keys=True) == json.dumps(expected, sort_keys=True), + "fixed typed receipt", + ) + print(json.dumps(result, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()