From fc1426353de3389409a27e5b9bc146a95edf811c Mon Sep 17 00:00:00 2001 From: Chris R Date: Mon, 19 Oct 2026 19:56:11 +1100 Subject: [PATCH] Replace repeated child-program admission seeks with linear record cursors --- .../r437-source-preparation-bound/PROOF.md | 217 +++ .../r437-source-preparation-bound/README.md | 110 ++ .../r437-source-preparation-bound/REPLAY.log | 7 + .../r437-source-preparation-bound/RESULT.json | 1335 +++++++++++++++++ .../r437-source-preparation-bound/REVIEW.md | 30 + .../SOURCES.json | 72 + .../SOURCE_PROJECTION.json | 28 + .../r437-source-preparation-bound/TASK.json | 89 ++ .../VALIDATION.json | 23 + .../r437-source-preparation-bound/VERIFY.json | 47 + .../r437-source-preparation-bound/check.py | 145 ++ .../forward_fields.py | 97 ++ .../test_export.py | 57 + .../r437-source-preparation-bound/verify.py | 53 + 14 files changed, 2310 insertions(+) create mode 100644 research/r437-source-preparation-bound/PROOF.md create mode 100644 research/r437-source-preparation-bound/README.md create mode 100644 research/r437-source-preparation-bound/REPLAY.log create mode 100644 research/r437-source-preparation-bound/RESULT.json create mode 100644 research/r437-source-preparation-bound/REVIEW.md create mode 100644 research/r437-source-preparation-bound/SOURCES.json create mode 100644 research/r437-source-preparation-bound/SOURCE_PROJECTION.json create mode 100644 research/r437-source-preparation-bound/TASK.json create mode 100644 research/r437-source-preparation-bound/VALIDATION.json create mode 100644 research/r437-source-preparation-bound/VERIFY.json create mode 100644 research/r437-source-preparation-bound/check.py create mode 100644 research/r437-source-preparation-bound/forward_fields.py create mode 100644 research/r437-source-preparation-bound/test_export.py create mode 100644 research/r437-source-preparation-bound/verify.py diff --git a/research/r437-source-preparation-bound/PROOF.md b/research/r437-source-preparation-bound/PROOF.md new file mode 100644 index 0000000000..93ef84fcbc --- /dev/null +++ b/research/r437-source-preparation-bound/PROOF.md @@ -0,0 +1,217 @@ +# A monotone admission pass for the actual child-program producer + +## Claim and source boundary + +This is a source-bound optimization of `SelectedBinding.child_program` in the +retained physical caller. It executes the real `Callback` constructor, prime-power +and root-unit validation, chronological step arithmetic, `children.extend`, and +normal cleanup. The package-local adapter changes only admission's sequential +Program/Fields access. Frozen sources are unchanged; adoption is a separate decision. +It supplies a source-bound tape/word action ledger and candidate optimization for +this producer component of PR3983's Pi, not all preparation, coefficient +evaluation, payload execution, stock admission, or the complete multiplication bound. + +The accepted-domain theorem assumes finite well-formed Program/field record tapes, +canonical fixed-width words with arithmetic margin, a fixed finite source vocabulary, +sufficient numerical slots, and valid child request labels supplied by the caller. +The field payload may be arbitrary: neither original nor adapted admission checks +all high digits or prepares matrices. Full raw-field shape, canonical digit values, +and actual selected specification supply remain upstream premises. The numerical +producer still performs its original prime-power, unit, history and code checks. + +Write I,L for index/residue word bit widths, Q for the fixed source-code width, +h for parent history depth, and n=h+1 for internal admission. A root record has +r=2I+L+5 symbols; one step has c=Q+2I+90 symbols; a full 64-by-64 raw field has +F=Q+2+4096(L+1) symbols. Let P=r+hc and D=r+(h+1)c. Lengths exclude LEFT and the +adjacent blank. All formulas below count actual calls to Tape/Word read, write +and unit step, including rewind. They do not equate Python runtime, AST execution, +object allocation, or a macro dispatch with a primitive finite-state transition. + +## Why the original admission is quadratic + +`Program.step(j)` invokes `seek_record` from LEFT through the root and j-1 steps; +`Fields.check_code(k)` invokes the same procedure through k full fields. Every +call returns the tape head to position 1. Callback admission requests program +steps 1,...,h and field slots 0,...,h, then separately checks the end positions. +No coefficient evaluation or payload is needed for this repeated work to occur. + +For the complete original child-program producer the Program tape invoice is + + reads = 8r+1 + h(3r+2I) + c[3h(h+1)/2+5h] - h(h+1)/2 + writes = 0 + moves = 6r+10 + h(2r+2) + c(h²+5h). + +The Fields tape invoice is + + reads = (3F-1)n(n+1)/2 + n(2Q+4) + 3 + writes = 0 + moves = F*n(n+1) + n(2Q+6) + 4. + +For example, seeking field k, decoding its code and rewinding costs +(3kF-k+2Q+4, 0, 2kF+2Q+6). The final end check costs +(3nF-n+3, 0, 2nF+4). Their sums give the Fields formula. +For Program, `root` costs (3r-4,0,2r+2), step j costs +(3r+(3j-1)c+2I+1-j,0,2r+2jc+2), final end checking costs +(3P-h+2,0,2P+4), and extension's source copy costs +(2r+3hc+3,0,2P+4). These sum to the stated complete invoice. + +Thus a claim of linear work in serialized input length for this original admission +is false when history is a variable. This is a statement about this producer's +repeated scans, not a universal lower bound on source validation or multiplication. + +## Adapter and semantic invariant + +`forward_fields.py` authenticates the complete normalized ASTs of the admission +method and Program.root/step, in addition to the verifier's full source hashes. +Its exact transformations are: + +1. Each of the two chronological `Fields.check_code` call sites consumes the next + field; the two leaf/internal `end` sites check the current blank and rewind. +2. Program.root parses the original root body and advances across its final + RECORD_END instead of rewinding. Program.step retains positive-level checking, + its exact finite/word parsers and final delimiter check, removes the initial + seek, and advances across its final delimiter instead of rewinding. +3. The final program seek is removed; its original BLANK assertion and rewind + remain. A temporary Program view is installed only around admission and restored + in `finally`. Subsequent `weight`, `extend` and random-access operations see the + original Program object. No borrowed tape or numerical word is copied into a + Python integer as part of the adapter's execution. + +After j historical iterations, the program cursor stands immediately after step +j (after ROOT for j=0), and the fields cursor immediately after field j-1 (at the +first field for j=0). The unchanged encoded `count`/`depth` loop selects the next +step and supplies the expected field code. The original step arithmetic, chronology, +rank, branch, reversal and proper-size predicates see exactly the same decoded +words as before. The next iteration preserves the invariant. At termination the +existing exact-program-depth assertion sees the same blank; leaf admission checks +h fields, while internal admission additionally consumes current field h and +checks h+1 fields. Both public heads return to 1. The root/program view is restored +on every exit; the original Callback abort path restores borrowed heads and words. + +Induction therefore gives the same accepted relation and, after successful +child_program, the same returned bytes and numerical ownership. It is not a claim +of identical exception timing on every malformed tape. For malformed records an +adapter may discover missing termination earlier. The finite negative controls +check their named rejection and cleanup observations; they are not a proof of +transactional recovery under arbitrary interruption or allocation failure. + +## Exact improved record bill and lifetime backing + +The adapted complete producer has Program invoice + + reads = 5P+2hI+1, writes = 0, moves = 4P+8, + +and Fields invoice + + reads = n(3F-Q-2)+3, writes = 0, moves = 2nF+4. + +The new Program admission alone costs (3r+2hc+2hI-2,0,2P+4); +the unchanged extension source copy supplies the remainder. Each adapted field +check reads its Q-bit code, skips the rest through RECORD_END exactly once, and +the final rewind visits the complete prefix once. For leaf-only admission use +n=h in the Fields formula and omit extension/output from the Program invoice. + +For both producers, creating the output costs exactly +(2D+1,D,2D+2). The two empty pending/value stacks contribute two reads and four unit moves to +Callback.close: each `empty()` performs one read and two moves on its top tape. +Their two reverse tapes remain at their initial positions. +All actual empty-stack work is explicitly measured; it is independent of h. +The verifier includes all seven record tapes in lifetime backing: parent Program +P+2, Fields nF+2, returned Program D+2, and four stack tapes of two visited cells. +Hence the producer record footprint is exactly + + P + D + nF + 14 cells. + +The adapter adds no tape and no numerical word. This lifetime bound counts LEFT, +the adjacent blank, and cells visited after erasure; it is not live occupancy. +The returned Program remains owned by the caller. Its later copying and erasure +are separate preparation charges already exposed in PR3983. + +## Numerical work and root/history coupling + +Numerical context and chronological checks remain essential. A deliberately loose +source-derived envelope, valid for either producer's normal successful path, is + + U = 100000[(h+2)²(I+1) + (h+2)(I+1)² + (L+1)³] + +Word read/write/unit-move actions. This is not a timing extrapolation. The following +sufficient bounds follow by counting the fixed-width loops in `words.py`: +zero/free/copy/compare/add/subtract or any fitting literal cost at most 100(b+1); +divmod at most 1000(b+1)²; times_small by <=128 at most 2000(b+1); +ring multiply at most 1000(b+1)²; inverse at most 10000(b+1)³. +The binary division loop has exactly b iterations. The Euclidean inverse has at +most 2b+1 quotient iterations, since every two nonterminal remainders decrease +by at least a factor two. The prime-power check has at most L quotient reductions. +These bounds include allocation initialization, operand rewinds, and freeing. + +There are (h+1)(h+2) original seek-counter decrement iterations and 2h+3 seek +invocations. A seek's fixed numeric overhead costs at most 500(I+1), and each +counter decrement/zero-test/free costs at most 300(I+1). Thus all seek counters +cost at most 2000(h+2)²(I+1). These are absent in adapted admission. + +One historical step has at most two index divisions, one <=128 multiplication, +two parsed index words, and fewer than twenty further linear word operations +(including the outer loop's count compare/increment, chronology compare and frees). +Using the displayed bounds, it costs at most 10000(I+1)². Root parsing, three +index literals, the outer loop's terminal test, extension (at most two divisions, +one bounded multiplication), five index append/read word scans, and final frees +cost at most 20000(I+1)². Therefore the entire non-seek index bill is bounded by +20000(h+2)(I+1)². Read/append word scans here charge their Word side; their record +Tape side is already priced above, so neither side is omitted or conflated. + +The residue side consists of the root-word parse/compare/unit inverse plus +prime-power validation and normal freeing. The latter uses at most L divisions, +linear comparisons, one literal of the fitting fixed prime q, copies and frees. +The displayed primitive bounds give at most 20000(L+1)³ for this entire side. +Consequently the sharper aggregate bound + + 2000(h+2)²(I+1) + 20000(h+2)(I+1)² + 20000(L+1)³ + +is already sufficient; U above leaves additional margin and is the bound checked +in the receipt. This argument counts loops from source rather than fitting U to +finite measurements. The adapter removes seek-related numerical work; unchanged +residue counts and chronological parsed-word traces are checked, not identical +index action counts. +Finite vocabulary checking and object/slot bookkeeping are not Word actions; +a finite-state implementation must add its fixed-source dispatch/slot tariff. + +Inspection of the straight-line owned-word lifetimes gives a conservative bound +of 64 additional index words and 64 additional residue words above protected +entry ownership. This covers the root/depth/current words, two parsed step words, +division's quotient/remainder/scan/shifted temporaries, Euclid's live pairs and +multiply temporaries; these inner loops do not stack recursively. Four record +stack tapes remain empty during admission. For a reused arena with B already +created slots and p protected live slots, created slots never exceed max(B,p+64), +because free slots are reused before allocation. Include its template separately: +(max(B,p+64)+1)(b+2) backing cells, plus slot metadata and finite code tables. +This is an upper bound, not a claimed sharp physical reserve coefficient. + +Every accepted history step shrinks its parent by at least a factor 21/32: +good rank <=42 yields child <=42*parent/64; pair/unit/half shrink further. +Since (21/32)²<1/2 and canonical root_size<2^(I-1), a positive h-step final size +implies h<2(I-1). For a successful extension final_size>=64, so h<2(I-7). +This is actual root/history coupling, not the assumption that a unit resets +serialized history. With fixed codec widths it absorbs the original quadratic +scan in an O(I²F+I³+L³) polynomial; the adapter improves the record component +to O(IF+I²+IQ+L), while the conservative arithmetic envelope remains O(I³+L³). +It does not alone compare this preparation bill to the original-width stock. + +## Remaining obligations and credit + +A completed caller bill must still add child_extents, read_prefix and actual raw +field/directory generation, geometry/context construction, coefficient weight +and matrix preparation, full physical role maxima, ownership/refinement tariffs, +and actual original-width stock. This package supplies no generated R437 catalogue +or GL64 production payload; its theorem applies to the actual generic producer +under admitted source specifications, and its synthetic and explicitly peer-derived projected-definition fixtures exercise +that acceptance path. The projected Q=6507 code/tag/low identities are checked +with canonical LowCodes, but source-plan/good-class reconstruction is not repeated. The new adapter is a candidate for adoption, not an installed shared change. + +Credit Jose Manuel / jmbarrancoml for SelectedBinding and the physical caller; +David Arias/PR2753 and the retained controller, Program, Fields and child grammar +authors, including Nick Petalas and the encoded-word/continuation lineage. +PR3983 supplies the prior checkpoint and explicit Pi boundary. PR3936/3950/3967 +and the R437/OQ4 source lineage supply the motivating caller context. New source +analysis, forward-only admission adapter and evidence: Chris R / Clear1nsight +with substantial OpenAI Codex assistance. Same-session AI review is distinct +from independent human or formal-kernel verification. Apache-2.0. diff --git a/research/r437-source-preparation-bound/README.md b/research/r437-source-preparation-bound/README.md new file mode 100644 index 0000000000..a13e187884 --- /dev/null +++ b/research/r437-source-preparation-bound/README.md @@ -0,0 +1,110 @@ +# Linear record admission for the physical child-program producer + +This package derives the actual `SelectedBinding.child_program` record invoice +and supplies a package-local forward-only admission adapter. The unchanged +producer repeatedly scans earlier Program and raw-field records. The adapter +uses the existing encoded chronological loop to visit each record once, preserves +its arithmetic predicates, then restores the original random-access Program. +Frozen/shared sources and the selected frontier are unchanged. + +For history h, index/residue widths I/L, source-code width Q, define +`n=h+1`, `r=2I+L+5`, `c=Q+2I+90`, `F=Q+2+4096(L+1)`, and `P=r+h*c`. +The complete adapted producer's record scans, including original-history copying +into the returned program, cost: + +| Tape | Reads | Writes | Unit moves | +|---|---:|---:|---:| +| Parent Program | `5P+2hI+1` | 0 | `4P+8` | +| Fields | `n(3F-Q-2)+3` | 0 | `2nF+4` | +| Returned Program, `D=r+(h+1)c` | `2D+1` | D | `2D+2` | +| Empty continuation tapes | 2 | 0 | 4 | + +The original Fields scans alone cost +`(3F-1)n(n+1)/2+n(2Q+4)+3` reads and +`F*n(n+1)+n(2Q+6)+4` moves. The full original Program invoice, numeric work +bound, root/history coupling and semantic induction are in [PROOF.md](PROOF.md). +This is a linear **record scan** improvement; binary arithmetic retains its +separate polynomial cost. No wall-clock measurement is substituted for tape work. + +Both versions use exactly `P+D+nF+14` visited record cells, including LEFT, +adjacent blanks, returned output and four empty continuation tapes. The adapter +adds no numerical word or tape. A conservative numerical component bound and +64 additional words per bank are stated with source-loop derivations; backing, +slot metadata and fixed vocabulary control remain explicitly separate. + +## Evidence and limits + +`check.py` authenticates and executes the unchanged word/record/controller/child +implementations and the exact extracted `SelectedBinding.child_program` method. +Only the candidate adapter changes admission's monotone record access. +Six normal/adapted producer pairs exercise good, pair, unit and half children at +history depths 0,1,2,3,4,6, varying word/code widths. Three leaf-only pairs check +that leaf admission consumes h fields, while internal admission consumes h+1. +The variable-history pairs check exact source-derived record counts, identical output bytes or +leaf state, chronological decoded-word traces, unchanged residue counts, decreased +index work, preserved borrowed bytes/heads, ownership cleanup and visited spans. +Seven malformed-admission controls compare rejection and cleanup. A changed-admission-AST control fails closed. Exact source, +AST and receipt corruption controls remain active under optimized Python. + +The six variable-history cases use synthetic admitted rank-seven source +projections. An additional source-shaped pair uses the exact 6,507-bit GL codes +and low hashes supplied by the same-session residual lane for current rank26 +IDLE27776 and rank7 COPY1603 (PR3967 source identity). Canonical LowCodes decoding +checks both request/view tags and full low hashes, then the actual producer +builds 2048→832→91 at modulus9 with nonzero high fields. SOURCE_PROJECTION.json +retains the peer-derived metadata and provenance. This package does **not** +independently reconstruct those source plans or establish their good-class status; +that is an explicit fixture premise, not a hidden new admission certificate. They execute the actual generic producer and Callback acceptance, +not a generated R437 GL64 catalogue or payload. The uniform theorem is about +that source method under admitted specifications; it does not independently prove +matrix/low-class admission, high-digit validity, or the full selected source. +The adapter is opt-in research code, not installed into the shared physical caller. + +Reproduce the bounded registered suite: + +```sh +python3 -B scripts/research_package.py --package research/r437-source-preparation-bound +``` + +The direct verifier also works in a Git-free export with its declared inputs. +`RESULT.json` is an exact deterministic receipt, not a timing-derived bound. +`VALIDATION.json` and `REPLAY.log` record the frozen local replay. Hosted CI is +reported separately after publication. No full GL64 payload, historical cold +suite, Lean, Docker, new κ, independent human review or formal proof is claimed. + +## Scope and coordination + +Explicit donor assignment refines `selected-stock-envelope`: close a substantive +actual preparation component from [PR3983](https://github.com/CrocSwap/integer-mult-bounds/pull/3983). +This pairs amortized sequential-tape accounting with grammar/automata cursor +invariants. It extends PR3983's serialization-only experiment by executing +Callback admission and supplies a concrete removal of repeated producer work. +The remaining Pi components are stated in the proof and TASK.json. + +Base canonical main is `20ecf2891d80b5acf18d980b2164fb44ea7faa90`, priority revision6. +Canonical team claim: https://github.com/CrocSwap/integer-mult-bounds/pull/3967#issuecomment-6263066320. +The local overlap helper had no remote cache; live PR search was additionally +checked. Adjacent PR3999 addresses interruption/abort recovery, and PR3995 pools +finite IR; this package optimizes normal unpooled source-program admission. +Neither result is treated as a prerequisite or a stock/cost theorem. + +## Open next questions + +See TASK.json for structured questions. Integrate the cursor at an actual complete +caller only after comparing its successful admission relation and physical +implementation tariff. Price the remaining child_extents/read_prefix/directory +producer, geometry/context and coefficient evaluation contributions. Combine +those charges with full lifetime role maxima and original-width stock before +claiming a complete reserve or caller recurrence. The history inequality alone +is not stock admission. + +## Credit + +Jose Manuel/jmbarrancoml: physical caller, SelectedBinding, encoded primitives. +David Arias/PR2753 and the retained Nick Petalas/controller/record/continuation +lineage: source grammar and callback. PR3983: checkpoint/serialization invoice +and explicit Pi gap. R437/OQ4 context retains ai-nanachi/3647, zxv/3690, +Ali Romman/1043, Sagar Thakrar/3700, the selected/native authors and +PR3936/3950/3967 attribution. New adapter, analysis and packaging by +Chris R/Clear1nsight with substantial OpenAI Codex assistance and same-session +AI review. Apache-2.0; predecessor results are not claimed as new. diff --git a/research/r437-source-preparation-bound/REPLAY.log b/research/r437-source-preparation-bound/REPLAY.log new file mode 100644 index 0000000000..894bc48d26 --- /dev/null +++ b/research/r437-source-preparation-bound/REPLAY.log @@ -0,0 +1,7 @@ +CHECK Exact legacy/adapted producer bills, bytes, predicates, cleanup, visited backing and rejection controls. +PASS_ACTUAL_CHILD_PROGRAM_FORWARD_ADMISSION 6 original/adapted pairs; 8 admission controls +CHECK Same scientific checks under optimized Python. +PASS_ACTUAL_CHILD_PROGRAM_FORWARD_ADMISSION 6 original/adapted pairs; 8 admission controls +CHECK Actual Git-free optimized positive plus every declared source mutation and receipt corruption reject. +PASS Git-free optimized positive; 9 source mutations and changed receipt reject +PASS_REGISTERED_RESEARCH_PACKAGE research/r437-source-preparation-bound outcome=completed diff --git a/research/r437-source-preparation-bound/RESULT.json b/research/r437-source-preparation-bound/RESULT.json new file mode 100644 index 0000000000..004a42143c --- /dev/null +++ b/research/r437-source-preparation-bound/RESULT.json @@ -0,0 +1,1335 @@ +{ + "projected_definition_cases": [ + { + "output_sha256": "2ed93ced5a80ba50469d3d1a0fb86ed48e6535a42034302f964469315c2e8b2d", + "field_actions": 518355, + "chronological_trace": [ + [ + [ + 0, + 604848721530721697539487379705034380531570091590346852410014854870049127477091837420548254543558928700537782474030983099265772898786484561658672039002674943788356974448480167989712472937378137734872581751125032155023521202244360721993222072523977739543653591953683293812551409907416647511995961735681638374807622627410003798353983700993669622737223586362459766352505503774865958639115302572221908467878108173097447035287393747028869649736810758914187267350284918075176025302816628316361997807384213724173581237958116462112401206074574823258468878762036996586571899716710674478781993767927526355892327885956500722844237812582140459941801209346740929562827531494137850959463787661607855917543008170179905559737373943869577155866617419342778195002780097910278884325698645725577245189492852885854559432060533644818605407087721349481104662466143289512136243380648898174197715414324090784182568252247355993913180445679334919527157847750811294048026069417536676490176977022041495756596892946999560964163299565932217921995199633376197191541862186006520125648773805993704552599640619398512270345954127323410267448327887289246459440417681462237415921075341911631458032407611066110251330192661809392774318877281922429718993387030527979150687558675434329318594750074886723224237320589252975487739191276432926054057449432467083678216742271226271570515079137147760393527405102191925749365236273167150630221734450851283698474361935760283619892972036177439036229770432719581350364100847527868386737499196770357741900240295263990797570020481236264500513451122811330738193428587098964617696675660714178050691938956958718562283337614586418257437427481696634056300204631612751247875914451294724833127551827990872564593998489976815661114613500460485745582428222501288016732457040952725345621322451847016233368709200547623885306890627565070870260288578303904102064971295165813021156951226494158041409632507811717475498971097060551105653728648410318527664334741374250877410471121484, + 26, + 0, + 0, + 0 + ], + 2048, + 832, + 32 + ] + ], + "source_projection_sha256": "ba4786b29dc7dc9a052fd094e9f16e7914b4b43fc72e5547feefad4b73f42968", + "source_plan_independently_reconstructed": false, + "code_bits": 6507, + "root": 2048, + "parent": 832, + "child": 91 + }, + { + "output_sha256": "2ed93ced5a80ba50469d3d1a0fb86ed48e6535a42034302f964469315c2e8b2d", + "field_actions": 297839, + "chronological_trace": [ + [ + [ + 0, + 604848721530721697539487379705034380531570091590346852410014854870049127477091837420548254543558928700537782474030983099265772898786484561658672039002674943788356974448480167989712472937378137734872581751125032155023521202244360721993222072523977739543653591953683293812551409907416647511995961735681638374807622627410003798353983700993669622737223586362459766352505503774865958639115302572221908467878108173097447035287393747028869649736810758914187267350284918075176025302816628316361997807384213724173581237958116462112401206074574823258468878762036996586571899716710674478781993767927526355892327885956500722844237812582140459941801209346740929562827531494137850959463787661607855917543008170179905559737373943869577155866617419342778195002780097910278884325698645725577245189492852885854559432060533644818605407087721349481104662466143289512136243380648898174197715414324090784182568252247355993913180445679334919527157847750811294048026069417536676490176977022041495756596892946999560964163299565932217921995199633376197191541862186006520125648773805993704552599640619398512270345954127323410267448327887289246459440417681462237415921075341911631458032407611066110251330192661809392774318877281922429718993387030527979150687558675434329318594750074886723224237320589252975487739191276432926054057449432467083678216742271226271570515079137147760393527405102191925749365236273167150630221734450851283698474361935760283619892972036177439036229770432719581350364100847527868386737499196770357741900240295263990797570020481236264500513451122811330738193428587098964617696675660714178050691938956958718562283337614586418257437427481696634056300204631612751247875914451294724833127551827990872564593998489976815661114613500460485745582428222501288016732457040952725345621322451847016233368709200547623885306890627565070870260288578303904102064971295165813021156951226494158041409632507811717475498971097060551105653728648410318527664334741374250877410471121484, + 26, + 0, + 0, + 0 + ], + 2048, + 832, + 32 + ] + ], + "source_projection_sha256": "ba4786b29dc7dc9a052fd094e9f16e7914b4b43fc72e5547feefad4b73f42968", + "source_plan_independently_reconstructed": false, + "code_bits": 6507, + "root": 2048, + "parent": 832, + "child": 91 + } + ], + "status": "PASS_ACTUAL_CHILD_PROGRAM_FORWARD_ADMISSION", + "cases": [ + { + "original": { + "chronological_trace": [], + "record_visited_cells": 24794, + "adapted": false, + "output_sha256": "3a81acd3330fb70498a48f119a97a0181f43fcd701c8cf89d9ab7a7e5d936fbf", + "numerical_actions": 23905, + "numerical_upper": 72600000, + "h": 0, + "I": 14, + "L": 5, + "Q": 4, + "kind": "unit", + "half": false, + "r": 38, + "c": 122, + "F": 24582, + "program": { + "reads": 305, + "writes": 0, + "moves": 238 + }, + "fields": { + "reads": 73760, + "writes": 0, + "moves": 49182 + }, + "output": { + "reads": 321, + "writes": 160, + "moves": 322 + }, + "index": { + "reads": 6981, + "writes": 1515, + "moves": 6874 + }, + "residue": { + "reads": 3840, + "writes": 749, + "moves": 3946 + }, + "index_backing": 11, + "residue_backing": 12, + "output_cells": 161 + }, + "adapted": { + "chronological_trace": [], + "record_visited_cells": 24794, + "adapted": true, + "output_sha256": "3a81acd3330fb70498a48f119a97a0181f43fcd701c8cf89d9ab7a7e5d936fbf", + "numerical_actions": 21032, + "numerical_upper": 72600000, + "h": 0, + "I": 14, + "L": 5, + "Q": 4, + "kind": "unit", + "half": false, + "r": 38, + "c": 122, + "F": 24582, + "program": { + "reads": 191, + "writes": 0, + "moves": 160 + }, + "fields": { + "reads": 73743, + "writes": 0, + "moves": 49168 + }, + "output": { + "reads": 321, + "writes": 160, + "moves": 322 + }, + "index": { + "reads": 5719, + "writes": 1202, + "moves": 5576 + }, + "residue": { + "reads": 3840, + "writes": 749, + "moves": 3946 + }, + "index_backing": 11, + "residue_backing": 12, + "output_cells": 161 + } + }, + { + "original": { + "chronological_trace": [ + [ + [ + 2, + 0, + 7, + 0, + 0, + 0 + ], + 262144, + 4096, + 4096 + ] + ], + "record_visited_cells": 49680, + "adapted": false, + "output_sha256": "a3f071508fcb849b9c710416bad35d80717b8fcda3a6483a2826a5798b714cdb", + "numerical_actions": 60099, + "numerical_upper": 172800000, + "h": 1, + "I": 20, + "L": 5, + "Q": 4, + "kind": "good", + "half": false, + "r": 50, + "c": 134, + "F": 24582, + "program": { + "reads": 1662, + "writes": 0, + "moves": 1216 + }, + "fields": { + "reads": 221262, + "writes": 0, + "moves": 147524 + }, + "output": { + "reads": 637, + "writes": 318, + "moves": 638 + }, + "index": { + "reads": 23583, + "writes": 5025, + "moves": 22956 + }, + "residue": { + "reads": 3840, + "writes": 749, + "moves": 3946 + }, + "index_backing": 14, + "residue_backing": 12, + "output_cells": 319 + }, + "adapted": { + "chronological_trace": [ + [ + [ + 2, + 0, + 7, + 0, + 0, + 0 + ], + 262144, + 4096, + 4096 + ] + ], + "record_visited_cells": 49680, + "adapted": true, + "output_sha256": "a3f071508fcb849b9c710416bad35d80717b8fcda3a6483a2826a5798b714cdb", + "numerical_actions": 51690, + "numerical_upper": 172800000, + "h": 1, + "I": 20, + "L": 5, + "Q": 4, + "kind": "good", + "half": false, + "r": 50, + "c": 134, + "F": 24582, + "program": { + "reads": 961, + "writes": 0, + "moves": 744 + }, + "fields": { + "reads": 147483, + "writes": 0, + "moves": 98332 + }, + "output": { + "reads": 637, + "writes": 318, + "moves": 638 + }, + "index": { + "reads": 19865, + "writes": 4128, + "moves": 19162 + }, + "residue": { + "reads": 3840, + "writes": 749, + "moves": 3946 + }, + "index_backing": 14, + "residue_backing": 12, + "output_cells": 319 + } + }, + { + "original": { + "chronological_trace": [ + [ + [ + 2, + 0, + 7, + 0, + 0, + 0 + ], + 16777216, + 262144, + 262144 + ], + [ + [ + 2, + 0, + 7, + 0, + 0, + 0 + ], + 262144, + 4096, + 4096 + ] + ], + "record_visited_cells": 86912, + "adapted": false, + "output_sha256": "08d52d55df6078e3a809917b8cb276edf53768ed0361d56325aea2667bbb777c", + "numerical_actions": 122044, + "numerical_upper": 369100000, + "h": 2, + "I": 26, + "L": 6, + "Q": 5, + "kind": "pair", + "half": false, + "r": 63, + "c": 147, + "F": 28679, + "program": { + "reads": 3777, + "writes": 0, + "moves": 2702 + }, + "fields": { + "reads": 516261, + "writes": 0, + "moves": 344200 + }, + "output": { + "reads": 1009, + "writes": 504, + "moves": 1010 + }, + "index": { + "reads": 50129, + "writes": 10427, + "moves": 48458 + }, + "residue": { + "reads": 5892, + "writes": 1154, + "moves": 5984 + }, + "index_backing": 14, + "residue_backing": 12, + "output_cells": 505 + }, + "adapted": { + "chronological_trace": [ + [ + [ + 2, + 0, + 7, + 0, + 0, + 0 + ], + 16777216, + 262144, + 262144 + ], + [ + [ + 2, + 0, + 7, + 0, + 0, + 0 + ], + 262144, + 4096, + 4096 + ] + ], + "record_visited_cells": 86912, + "adapted": true, + "output_sha256": "08d52d55df6078e3a809917b8cb276edf53768ed0361d56325aea2667bbb777c", + "numerical_actions": 103927, + "numerical_upper": 369100000, + "h": 2, + "I": 26, + "L": 6, + "Q": 5, + "kind": "pair", + "half": false, + "r": 63, + "c": 147, + "F": 28679, + "program": { + "reads": 1890, + "writes": 0, + "moves": 1436 + }, + "fields": { + "reads": 258093, + "writes": 0, + "moves": 172078 + }, + "output": { + "reads": 1009, + "writes": 504, + "moves": 1010 + }, + "index": { + "reads": 42087, + "writes": 8522, + "moves": 40288 + }, + "residue": { + "reads": 5892, + "writes": 1154, + "moves": 5984 + }, + "index_backing": 14, + "residue_backing": 12, + "output_cells": 505 + } + }, + { + "original": { + "chronological_trace": [ + [ + [ + 2, + 0, + 7, + 0, + 0, + 0 + ], + 1073741824, + 16777216, + 16777216 + ], + [ + [ + 2, + 0, + 7, + 0, + 0, + 0 + ], + 16777216, + 262144, + 262144 + ], + [ + [ + 2, + 0, + 7, + 0, + 0, + 0 + ], + 262144, + 4096, + 4096 + ] + ], + "record_visited_cells": 99596, + "adapted": false, + "output_sha256": "2d036ebc91bb21fad67ca87e156998e8cc899f37efb05e6264e532a680fb7fd4", + "numerical_actions": 250143, + "numerical_upper": 648600000, + "h": 3, + "I": 32, + "L": 5, + "Q": 4, + "kind": "unit", + "half": true, + "r": 74, + "c": 158, + "F": 24582, + "program": { + "reads": 6659, + "writes": 0, + "moves": 4696 + }, + "fields": { + "reads": 737501, + "writes": 0, + "moves": 491700 + }, + "output": { + "reads": 1413, + "writes": 706, + "moves": 1414 + }, + "index": { + "reads": 111523, + "writes": 22931, + "moves": 107154 + }, + "residue": { + "reads": 3840, + "writes": 749, + "moves": 3946 + }, + "index_backing": 14, + "residue_backing": 12, + "output_cells": 707 + }, + "adapted": { + "chronological_trace": [ + [ + [ + 2, + 0, + 7, + 0, + 0, + 0 + ], + 1073741824, + 16777216, + 16777216 + ], + [ + [ + 2, + 0, + 7, + 0, + 0, + 0 + ], + 16777216, + 262144, + 262144 + ], + [ + [ + 2, + 0, + 7, + 0, + 0, + 0 + ], + 262144, + 4096, + 4096 + ] + ], + "record_visited_cells": 99596, + "adapted": true, + "output_sha256": "2d036ebc91bb21fad67ca87e156998e8cc899f37efb05e6264e532a680fb7fd4", + "numerical_actions": 217030, + "numerical_upper": 648600000, + "h": 3, + "I": 32, + "L": 5, + "Q": 4, + "kind": "unit", + "half": true, + "r": 74, + "c": 158, + "F": 24582, + "program": { + "reads": 2933, + "writes": 0, + "moves": 2200 + }, + "fields": { + "reads": 294963, + "writes": 0, + "moves": 196660 + }, + "output": { + "reads": 1413, + "writes": 706, + "moves": 1414 + }, + "index": { + "reads": 96785, + "writes": 19486, + "moves": 92224 + }, + "residue": { + "reads": 3840, + "writes": 749, + "moves": 3946 + }, + "index_backing": 14, + "residue_backing": 12, + "output_cells": 707 + } + }, + { + "original": { + "chronological_trace": [ + [ + [ + 2, + 0, + 7, + 0, + 0, + 0 + ], + 68719476736, + 1073741824, + 1073741824 + ], + [ + [ + 2, + 0, + 7, + 0, + 0, + 0 + ], + 1073741824, + 16777216, + 16777216 + ], + [ + [ + 2, + 0, + 7, + 0, + 0, + 0 + ], + 16777216, + 262144, + 262144 + ], + [ + [ + 2, + 0, + 7, + 0, + 0, + 0 + ], + 262144, + 4096, + 4096 + ] + ], + "record_visited_cells": 124682, + "adapted": false, + "output_sha256": "31871227866b94791b2ef43215ce1f2fd256a614b2a058025dbed64927b85ae7", + "numerical_actions": 358749, + "numerical_upper": 1074600000, + "h": 4, + "I": 38, + "L": 5, + "Q": 8, + "kind": "good", + "half": false, + "r": 86, + "c": 174, + "F": 24586, + "program": { + "reads": 10715, + "writes": 0, + "moves": 7486 + }, + "fields": { + "reads": 1106458, + "writes": 0, + "moves": 737694 + }, + "output": { + "reads": 1913, + "writes": 956, + "moves": 1914 + }, + "index": { + "reads": 161673, + "writes": 33405, + "moves": 155136 + }, + "residue": { + "reads": 3840, + "writes": 749, + "moves": 3946 + }, + "index_backing": 14, + "residue_backing": 12, + "output_cells": 957 + }, + "adapted": { + "chronological_trace": [ + [ + [ + 2, + 0, + 7, + 0, + 0, + 0 + ], + 68719476736, + 1073741824, + 1073741824 + ], + [ + [ + 2, + 0, + 7, + 0, + 0, + 0 + ], + 1073741824, + 16777216, + 16777216 + ], + [ + [ + 2, + 0, + 7, + 0, + 0, + 0 + ], + 16777216, + 262144, + 262144 + ], + [ + [ + 2, + 0, + 7, + 0, + 0, + 0 + ], + 262144, + 4096, + 4096 + ] + ], + "record_visited_cells": 124682, + "adapted": true, + "output_sha256": "31871227866b94791b2ef43215ce1f2fd256a614b2a058025dbed64927b85ae7", + "numerical_actions": 304236, + "numerical_upper": 1074600000, + "h": 4, + "I": 38, + "L": 5, + "Q": 8, + "kind": "good", + "half": false, + "r": 86, + "c": 174, + "F": 24586, + "program": { + "reads": 4215, + "writes": 0, + "moves": 3136 + }, + "fields": { + "reads": 368743, + "writes": 0, + "moves": 245864 + }, + "output": { + "reads": 1913, + "writes": 956, + "moves": 1914 + }, + "index": { + "reads": 137363, + "writes": 27780, + "moves": 130558 + }, + "residue": { + "reads": 3840, + "writes": 749, + "moves": 3946 + }, + "index_backing": 14, + "residue_backing": 12, + "output_cells": 957 + } + }, + { + "original": { + "chronological_trace": [ + [ + [ + 2, + 0, + 7, + 0, + 0, + 0 + ], + 281474976710656, + 4398046511104, + 4398046511104 + ], + [ + [ + 2, + 0, + 7, + 0, + 0, + 0 + ], + 4398046511104, + 68719476736, + 68719476736 + ], + [ + [ + 2, + 0, + 7, + 0, + 0, + 0 + ], + 68719476736, + 1073741824, + 1073741824 + ], + [ + [ + 2, + 0, + 7, + 0, + 0, + 0 + ], + 1073741824, + 16777216, + 16777216 + ], + [ + [ + 2, + 0, + 7, + 0, + 0, + 0 + ], + 16777216, + 262144, + 262144 + ], + [ + [ + 2, + 0, + 7, + 0, + 0, + 0 + ], + 262144, + 4096, + 4096 + ] + ], + "record_visited_cells": 232258, + "adapted": false, + "output_sha256": "a8951cc276375b70c3fc1e80c74160d980289b6f5c39d26bb918a641000450ba", + "numerical_actions": 805059, + "numerical_upper": 2458400000, + "h": 6, + "I": 50, + "L": 7, + "Q": 8, + "kind": "unit", + "half": false, + "r": 112, + "c": 198, + "F": 32778, + "program": { + "reads": 21906, + "writes": 0, + "moves": 15106 + }, + "fields": { + "reads": 2753467, + "writes": 0, + "moves": 1835726 + }, + "output": { + "reads": 2997, + "writes": 1498, + "moves": 2998 + }, + "index": { + "reads": 363897, + "writes": 74523, + "moves": 347722 + }, + "residue": { + "reads": 8588, + "writes": 1687, + "moves": 8642 + }, + "index_backing": 14, + "residue_backing": 12, + "output_cells": 1499 + }, + "adapted": { + "chronological_trace": [ + [ + [ + 2, + 0, + 7, + 0, + 0, + 0 + ], + 281474976710656, + 4398046511104, + 4398046511104 + ], + [ + [ + 2, + 0, + 7, + 0, + 0, + 0 + ], + 4398046511104, + 68719476736, + 68719476736 + ], + [ + [ + 2, + 0, + 7, + 0, + 0, + 0 + ], + 68719476736, + 1073741824, + 1073741824 + ], + [ + [ + 2, + 0, + 7, + 0, + 0, + 0 + ], + 1073741824, + 16777216, + 16777216 + ], + [ + [ + 2, + 0, + 7, + 0, + 0, + 0 + ], + 16777216, + 262144, + 262144 + ], + [ + [ + 2, + 0, + 7, + 0, + 0, + 0 + ], + 262144, + 4096, + 4096 + ] + ], + "record_visited_cells": 232258, + "adapted": true, + "output_sha256": "a8951cc276375b70c3fc1e80c74160d980289b6f5c39d26bb918a641000450ba", + "numerical_actions": 684070, + "numerical_upper": 2458400000, + "h": 6, + "I": 50, + "L": 7, + "Q": 8, + "kind": "unit", + "half": false, + "r": 112, + "c": 198, + "F": 32778, + "program": { + "reads": 7101, + "writes": 0, + "moves": 5208 + }, + "fields": { + "reads": 688271, + "writes": 0, + "moves": 458896 + }, + "output": { + "reads": 2997, + "writes": 1498, + "moves": 2998 + }, + "index": { + "reads": 309799, + "writes": 62186, + "moves": 293168 + }, + "residue": { + "reads": 8588, + "writes": 1687, + "moves": 8642 + }, + "index_backing": 14, + "residue_backing": 12, + "output_cells": 1499 + } + } + ], + "leaf_cases": [ + { + "original": { + "h": 0, + "state": [ + 4096, + 1, + 0, + 4096 + ], + "trace": [], + "fields": { + "reads": 3, + "writes": 0, + "moves": 4 + }, + "program": { + "reads": 226, + "writes": 0, + "moves": 158 + } + }, + "adapted": { + "h": 0, + "state": [ + 4096, + 1, + 0, + 4096 + ], + "trace": [], + "fields": { + "reads": 3, + "writes": 0, + "moves": 4 + }, + "program": { + "reads": 112, + "writes": 0, + "moves": 80 + } + } + }, + { + "original": { + "h": 2, + "state": [ + 16777216, + 1, + 2, + 4096 + ], + "trace": [ + [ + [ + 2, + 0, + 7, + 0, + 0, + 0 + ], + 16777216, + 262144, + 262144 + ], + [ + [ + 2, + 0, + 7, + 0, + 0, + 0 + ], + 262144, + 4096, + 4096 + ] + ], + "fields": { + "reads": 221275, + "writes": 0, + "moves": 147534 + }, + "program": { + "reads": 2754, + "writes": 0, + "moves": 1976 + } + }, + "adapted": { + "h": 2, + "state": [ + 16777216, + 1, + 2, + 4096 + ], + "trace": [ + [ + [ + 2, + 0, + 7, + 0, + 0, + 0 + ], + 16777216, + 262144, + 262144 + ], + [ + [ + 2, + 0, + 7, + 0, + 0, + 0 + ], + 262144, + 4096, + 4096 + ] + ], + "fields": { + "reads": 147487, + "writes": 0, + "moves": 98336 + }, + "program": { + "reads": 876, + "writes": 0, + "moves": 716 + } + } + }, + { + "original": { + "h": 4, + "state": [ + 68719476736, + 1, + 4, + 4096 + ], + "trace": [ + [ + [ + 2, + 0, + 7, + 0, + 0, + 0 + ], + 68719476736, + 1073741824, + 1073741824 + ], + [ + [ + 2, + 0, + 7, + 0, + 0, + 0 + ], + 1073741824, + 16777216, + 16777216 + ], + [ + [ + 2, + 0, + 7, + 0, + 0, + 0 + ], + 16777216, + 262144, + 262144 + ], + [ + [ + 2, + 0, + 7, + 0, + 0, + 0 + ], + 262144, + 4096, + 4096 + ] + ], + "fields": { + "reads": 737539, + "writes": 0, + "moves": 491728 + }, + "program": { + "reads": 8338, + "writes": 0, + "moves": 5834 + } + }, + "adapted": { + "h": 4, + "state": [ + 68719476736, + 1, + 4, + 4096 + ], + "trace": [ + [ + [ + 2, + 0, + 7, + 0, + 0, + 0 + ], + 68719476736, + 1073741824, + 1073741824 + ], + [ + [ + 2, + 0, + 7, + 0, + 0, + 0 + ], + 1073741824, + 16777216, + 16777216 + ], + [ + [ + 2, + 0, + 7, + 0, + 0, + 0 + ], + 16777216, + 262144, + 262144 + ], + [ + [ + 2, + 0, + 7, + 0, + 0, + 0 + ], + 262144, + 4096, + 4096 + ] + ], + "fields": { + "reads": 294971, + "writes": 0, + "moves": 196668 + }, + "program": { + "reads": 1928, + "writes": 0, + "moves": 1544 + } + } + } + ], + "negative_controls": { + "wrong_field_code": "original global raw-field code", + "extra_field": "exact frozen/current field prefix", + "truncated_field": "record exists at global slot", + "wrong_root_tag": "root record", + "wrong_current_code": "original global raw-field code", + "extra_program_step": "exact program depth", + "nonunit_root": "root coefficient unit", + "changed_admission_AST": "exact reviewed admission AST" + }, + "physical_payload_executed": false, + "full_Pi_closed": false +} diff --git a/research/r437-source-preparation-bound/REVIEW.md b/research/r437-source-preparation-bound/REVIEW.md new file mode 100644 index 0000000000..bd7afb5538 --- /dev/null +++ b/research/r437-source-preparation-bound/REVIEW.md @@ -0,0 +1,30 @@ +# Same-session read-only AI cross-review + +A separately assigned Codex reviewer inspected the evolving source/proof and final +scientific snapshot. This is same-session AI review, not independent human or +formal-kernel approval. + +The reviewer checked the monotone Program/Fields cursor invariant, restoration of +the original random-access Program object, the successful-path cost/space claims, +root/history coupling, and the numerical loop decomposition. It requested explicit +leaf admission tests, clearer exception-order limits, any-fitting-literal wording, +an aggregate numerical bound and precise action-model scope; these were adopted. + +Read-only verification authenticated all nine live source inputs. The reviewer +ran a separate mixed q=3 history with good7, reversed pair26, half unit26, good7 +in both leaf/internal and original/adapted modes, including post-admission random +access to step2 and ownership/head restoration. These additional reviewer fixtures +were not independently source-plan reconstructed and are not part of the committed +six-pair receipt. + +The reviewer also reran the projected Q=6507 pair: root2048→832→91, legacy Fields +518355 actions versus adapted297839, identical output SHA256 +`2ed93ced5a80ba50469d3d1a0fb86ed48e6535a42034302f964469315c2e8b2d` and +chronological trace. It found no blocking issue under the declared scope. + +Reviewed core hashes: +- forward_fields.py: `4b6cb4b8a20c920c32dbad7b8e99a728d75681b0b4cdc876f4bd60730302a83b` +- PROOF.md: `efa49f0e692c6230589e76df9d9c202f71b6d6103b4893f40db3f1299ee30f27` + +The producer lane separately runs the full registered frozen replay. Local replay, +exact publication-byte checks and hosted CI are distinct evidence levels. diff --git a/research/r437-source-preparation-bound/SOURCES.json b/research/r437-source-preparation-bound/SOURCES.json new file mode 100644 index 0000000000..dff3558cc6 --- /dev/null +++ b/research/r437-source-preparation-bound/SOURCES.json @@ -0,0 +1,72 @@ +{ + "schema_version": 1, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/children.py", + "usage": "input", + "git_blob": "ce4935f838516e2b08d13bec767cb803786fbc6b", + "sha256": "a78866939631214c1d1659203b2b5fc062e3c6255e9f11f975c310046b010bd6" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/controller.py", + "usage": "input", + "git_blob": "c631a9e77fbcccf0e8f448adc22978728aed7b60", + "sha256": "fa09146991f6c04e6f4b6eb9bf0c8e103e70e90a0e402ff3d69814e6aac8ff8c" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/matrices.py", + "usage": "input", + "git_blob": "5d497353efbb9eeaaf4facd96ab40ffb0f3aa20d", + "sha256": "00b687434039b54529ee092e34f9435cfcd66e0816eb3bd2a6688c73f4e01459" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/plan.py", + "usage": "input", + "git_blob": "48255d5454308c07635fae4e7eb4873b0bd2a4f8", + "sha256": "d9c8dc93762db4d3a449814aa51e2211460648694469854d89cb48cb04188cf3" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/records.py", + "usage": "input", + "git_blob": "4f00467a0ff580954ad2fd0c7380240c753ddef3", + "sha256": "0c9c4b23e998597fb877bb1a29da69ac869b68262abe635b162b4dba9c69b372" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/words.py", + "usage": "input", + "git_blob": "8d4ba37e2778acb35b34e0719df2caf138fbeb50", + "sha256": "5c37f57708ba3131bdcb03139f9dbc29886bee44569c09cbba51b68f75acd7f9" + }, + { + "path": "research/selected-bit-physical-caller/macro_binding.py", + "usage": "input", + "git_blob": "c197eb6458be9374cb4684c654bfc99e619dcaf0", + "sha256": "9ef31765d03d2c54fad9296f2ff0707a190ce169e44de4f0f45214e3c410c01a" + }, + { + "path": "research/selected-bit-physical-caller/macro_machine.py", + "usage": "input", + "git_blob": "5a032e8923f7f8b22bb98f3e39b804beb9906c16", + "sha256": "7bc6e42072a09a08ac961e05c3da01cde012d740d4b4c605f298d994f2ad7c5a" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/low_codes.py", + "usage": "input", + "git_blob": "737edfc4a10f4b7b3b97a7cef4b40864efd806e6", + "sha256": "f657e17f6088c840e3f7783e662257630f6d2c1e71c217721ffbca4d6ac93e87" + } + ] +} diff --git a/research/r437-source-preparation-bound/SOURCE_PROJECTION.json b/research/r437-source-preparation-bound/SOURCE_PROJECTION.json new file mode 100644 index 0000000000..abb3cc943d --- /dev/null +++ b/research/r437-source-preparation-bound/SOURCE_PROJECTION.json @@ -0,0 +1,28 @@ +{ + "origin_adapter_commit": "32af060614fefa9729c86370524c2e72265acd76", + "r437_source_commit": "a24f9ff95c12fd0b6792e3f710569237efd72db2", + "request_digest": "cbfea55f5cd0b74a2a0d4292ad0139d2b5bb73127951127698030bc90c73c532", + "code_bits": 6507, + "definitions": [ + { + "label": "ancestor", + "request_id": 27776, + "code": 604848721530721697539487379705034380531570091590346852410014854870049127477091837420548254543558928700537782474030983099265772898786484561658672039002674943788356974448480167989712472937378137734872581751125032155023521202244360721993222072523977739543653591953683293812551409907416647511995961735681638374807622627410003798353983700993669622737223586362459766352505503774865958639115302572221908467878108173097447035287393747028869649736810758914187267350284918075176025302816628316361997807384213724173581237958116462112401206074574823258468878762036996586571899716710674478781993767927526355892327885956500722844237812582140459941801209346740929562827531494137850959463787661607855917543008170179905559737373943869577155866617419342778195002780097910278884325698645725577245189492852885854559432060533644818605407087721349481104662466143289512136243380648898174197715414324090784182568252247355993913180445679334919527157847750811294048026069417536676490176977022041495756596892946999560964163299565932217921995199633376197191541862186006520125648773805993704552599640619398512270345954127323410267448327887289246459440417681462237415921075341911631458032407611066110251330192661809392774318877281922429718993387030527979150687558675434329318594750074886723224237320589252975487739191276432926054057449432467083678216742271226271570515079137147760393527405102191925749365236273167150630221734450851283698474361935760283619892972036177439036229770432719581350364100847527868386737499196770357741900240295263990797570020481236264500513451122811330738193428587098964617696675660714178050691938956958718562283337614586418257437427481696634056300204631612751247875914451294724833127551827990872564593998489976815661114613500460485745582428222501288016732457040952725345621322451847016233368709200547623885306890627565070870260288578303904102064971295165813021156951226494158041409632507811717475498971097060551105653728648410318527664334741374250877410471121484, + "q": 3, + "rank": 26, + "good": true, + "low_sha256": "c52a0c62fe9bedfe3e514ea8908795b71faacfb2dfa9869e8a55e420b5b5d661", + "low_construction": "H B^-1 modulo3, H identity with [[1,1],[1,2]] block at axes0/rank" + }, + { + "label": "good", + "request_id": 1603, + "code": 34926850680108068992933807421762475870225005164761236601047629425661373630604977412705826564523707256025409368701030353271401454614040333781537708280745112405305401668348477482466380353987753725267193515551698158660453724525995403745235446893437579701773580022176347862996679944602051584084888263934840424048029773142203720002417974876485217770608285259256956392007746549304413205661877544376401244540185038280027330929752085164426439753822067999863954534218047708275687075598356170135176307767217034119652877131885744266734654773953544157769206568827662342996841496270798987648824768859458245962260226488427955360141153543371284697575614424162570266446693924541938269796166338494612018288378872660244063078947632663657156499355148381988362736356643322849148377442857245260922913575613751758110075286283434035690453147194376372501483925286059205941942845394105106347840584241187587271864752016845669615625349072104377891641403856009079839476474573907200694253098642531940361453604956398367040791381548217296526504773718482428936483197067933707707515158711246206105164517481783385634488180343497996281611489661214911315443922149029317542899183716710224366887304800522168777050664224857251641778715974657058400745625370575436177824558064650086949098360336560854952474459656212946009469535643519025648164461295996115580432892852191260522953598681290003624379918596006274553951445616767576261909348273144740505854085854113560937575309693368631355610958741372879056986126517227791855007237039541566747150243340607577963134352216070095097199238102258655275101635908595778397805683035525654052933134213833421022796014361267044842671224329448574953659886231517465375831849430640035811415490801525499147507056719124005728120306769260816664401134999379784174255211011888062888664478003236609207124586791050826589229244333620885647723134725876877206104089161297245049040276190950742554999093593630920817381362600115947947931633931649451558193809739223500606604598361196, + "q": 3, + "rank": 7, + "good": true, + "low_sha256": "ea16353f7c79e9c0af55cbb42c2092b631f7a9c44ae0989b731c43e53133de99", + "low_construction": "H B^-1 modulo3, H identity with [[1,1],[1,2]] block at axes0/rank" + } + ] +} diff --git a/research/r437-source-preparation-bound/TASK.json b/research/r437-source-preparation-bound/TASK.json new file mode 100644 index 0000000000..e985f5bd73 --- /dev/null +++ b/research/r437-source-preparation-bound/TASK.json @@ -0,0 +1,89 @@ +{ + "schema_version": 1, + "task_id": "selected-stock-envelope", + "priority_revision": 6, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "original_card": { + "id": "selected-stock-envelope", + "question": "What explicit uniform stock envelope does the actual selected stopped producer supply at one bootstrap stage?", + "starting_points": [ + "research/selected-bootstrap-stock-audit/README.md", + "research/bootstrap-cutoff-time-space-split/README.md", + "certificates/selected-result.json", + "docs/research/community-efficient1000-review.md", + "research/stock-margin-chain/README.md" + ], + "methods": [ + "Derive a source-bound reserve recurrence at the actual selected atom widths, separating parent stock from completed inner borrowing.", + "Find an exact missing implication or counterexample to a proposed selected-stage stock envelope." + ], + "acceptance_gate": "Bind every coefficient and depth factor to the selected producer and state the width domain. Compare a proved envelope with the sufficient cutoff guard; a large numerical headroom or a historical m=120 coefficient is not a selected m=73 proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read #2972 stock-margin chain and the selected stock audit. The new source archive reports the remaining cutoff comparisons, but leaves every actual stock coefficient unresolved; it is not an independently validated reserve envelope.", + "scope": "Source-bound orientation only. Read the named package and review before relying on its local evidence; this command is not its replay or supplier admission." + }, + "first_experiment": "Choose one actual selected producer/stage and derive its parent reserve and depth coefficient from source. Check whether newer handoffs already cover that exact obligation. Stop with the missing implementation lemma if it cannot be bounded; do not rerun #2972 cutoff/headroom arithmetic as a new contribution.", + "bottleneck_link": "This reduces a concrete inherited implementation obligation without confusing unchanged kappa arithmetic with a completed theorem.", + "allowed_variations": [ + "One stage or one explicit reserve/depth implication.", + "An independently checked same-domain proof repair, retaining all remaining assumptions." + ], + "scope_change_triggers": [ + "Importing the historical 57604 or 252 allowance without a selected-producer binding.", + "Calling a conditional fit lemma a full outer-proof adoption.", + "Replacing an actual selected stock coefficient with cutoff comparisons or a conditional fit inequality." + ], + "overlap_terms": [ + "selected stock", + "stock envelope", + "bootstrap cutoff", + "1956", + "1965", + "1990", + "2972", + "stock-margin-chain", + "actual_stock_coefficient" + ], + "existing_checks": [ + { + "scope": "Retained stock audit identifies missing actual selected-stage coefficients; later cutoff-chain arithmetic does not supply them.", + "evidence": "docs/research/research-family-status.md#revision-6-handoffs-source-archives-awaiting-independent-validation", + "remaining": "Derive one actual reserve/depth coefficient from the selected producer.", + "status": "reviewed", + "source_commit": "836b19bfa309ceafbc8ee32a15e8c4b10dde7e11", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "refined", + "actual_scope": "Exact actual child_program admission bill and package-local monotone Program/Fields optimization, with lifetime backing and root/history coupling.", + "scope_change_reason": "Explicit donor/parent assignment supplies an actual producer action ledger and candidate optimization for PR3983 Pi rather than restating cutoff arithmetic.", + "bottleneck_link": "Removes real repeated history/raw-field scans in the retained physical caller, exposing preparation work and backing for later stock composition.", + "budget_minutes": 60, + "stop_rule": "Stop at normal child-program admission; do not claim full Pi, GL64 payload or complete stock coefficient. Reserve final quarter for replay and exact-head publication.", + "outcome": "completed", + "evidence": "PROOF.md, RESULT.json, registered normal/optimized/Git-free replay.", + "author": "Chris R / Clear1nsight with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex analysis, code and same-session cross-agent review; no independent human/formal review.", + "open_questions": [ + { + "question": "Can the adapter be composed with complete current-source physical preparation?", + "why_it_matters": "The completed producer component does not price all of Pi or establish stock fit.", + "first_step": "Price child_extents, read_prefix, source-directory generation and context/geometry operations at actual widths.", + "blocked_by": "Full source/stock/root contract and remaining producer tariffs." + }, + { + "question": "Can the coefficient consumer reuse monotone admission safely?", + "why_it_matters": "Leaf coefficient passes repeatedly validate histories.", + "first_step": "Apply the adapter only around admission; preserve later random-access weight and verify complete leaf consumer.", + "blocked_by": "Coefficient evaluation, fallback and full physical stream tariffs remain separate." + } + ], + "coordination": "https://github.com/CrocSwap/integer-mult-bounds/pull/3967#issuecomment-6263066320" +} diff --git a/research/r437-source-preparation-bound/VALIDATION.json b/research/r437-source-preparation-bound/VALIDATION.json new file mode 100644 index 0000000000..72e7f179f2 --- /dev/null +++ b/research/r437-source-preparation-bound/VALIDATION.json @@ -0,0 +1,23 @@ +{ + "status": "PASS", + "started_utc": "2026-10-19T08:50:18.548109+00:00", + "elapsed_seconds": 226.1094460230015, + "python": "3.12.3 (main, Aug 31 2026, 10:18:26) [GCC 13.3.0]", + "exit_code": 0, + "all_frozen_files_unchanged": true, + "command": [ + "/usr/bin/python3", + "-B", + "scripts/research_package.py", + "--package", + "research/r437-source-preparation-bound" + ], + "replay_sha256": "a92dfccb96d4e06123fe7ac5b7ab22e7bf586ebf49474e4329c6be8730e6da46", + "submission_checkpoint": { + "canonical_main": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "priority_revision": 6, + "fetched_utc": "2026-10-19 08:50 UTC", + "unchanged": true, + "overlap": "Local helper partial/no remote cache; live updated open-PR search checked through4003. Adjacent3993/3999 lease/abort,3995 pooledIR and4000dyadic fusion are different scopes. Discussion coverage parent-coordinated, partial." + } +} diff --git a/research/r437-source-preparation-bound/VERIFY.json b/research/r437-source-preparation-bound/VERIFY.json new file mode 100644 index 0000000000..f56eaf8afb --- /dev/null +++ b/research/r437-source-preparation-bound/VERIFY.json @@ -0,0 +1,47 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/children.py", + "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/controller.py", + "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/matrices.py", + "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/plan.py", + "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/records.py", + "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/words.py", + "research/selected-bit-physical-caller/macro_binding.py", + "research/selected-bit-physical-caller/macro_machine.py", + "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/low_codes.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Exact legacy/adapted producer bills, bytes, predicates, cleanup, visited backing and rejection controls." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Same scientific checks under optimized Python." + }, + { + "argv": [ + "{python}", + "-B", + "{package}/test_export.py" + ], + "timeout_seconds": 300, + "checks": "Actual Git-free optimized positive plus every declared source mutation and receipt corruption reject." + } + ] +} diff --git a/research/r437-source-preparation-bound/check.py b/research/r437-source-preparation-bound/check.py new file mode 100644 index 0000000000..ea91547b5e --- /dev/null +++ b/research/r437-source-preparation-bound/check.py @@ -0,0 +1,145 @@ +"""Pinned real Callback and SelectedBinding.child_program; no payload execution.""" +import ast, importlib.util, json, sys +from pathlib import Path +from types import SimpleNamespace as NS +from hashlib import sha256 +HERE=Path(__file__).resolve().parent; ROOT=HERE.parents[1] +CALLER=ROOT/'research/selected-bit-physical-caller'; V=CALLER/'inputs/pr2753/predecessor/vendor' +def need(x,m): + if not x: raise ValueError(m) +def authenticate(): + for r in json.loads((HERE/'SOURCES.json').read_text())['files']: + if r['usage']=='input':need(sha256((ROOT/r['path']).read_bytes()).hexdigest()==r['sha256'],'changed source: '+r['path']) +def load(name): + s=importlib.util.spec_from_file_location(name,V/(name+'.py'));m=importlib.util.module_from_spec(s);sys.modules[name]=m;exec(compile((V/(name+'.py')).read_bytes(),str(V/(name+'.py')),'exec'),m.__dict__);return m +def setup(adapted=False): + authenticate();w=load('words');r=load('records');load('matrices');c=load('controller');ch=load('children');p=load('plan') + class ObservedTape(r.Tape): + created=[] + def __init__(self): + super().__init__();self.visited={0,1};self.created.append(self) + def read(self):self.visited.add(self.head);return super().read() + def write(self,x):self.visited.add(self.head);return super().write(x) + def step(self,x): + self.visited.add(self.head);super().step(x);self.visited.add(self.head) + r.Tape=ObservedTape + c.semantic_trace=[] + original_step=c.Callback.step + def observed_step(self,level): + result=original_step(self,level) + metadata,parent,child,f=result + c.semantic_trace.append([list(metadata),parent.inspect(),child.inspect(),f.inspect()]) + return result + c.Callback.step=observed_step + if adapted: + import forward_fields + c.Callback=forward_fields.install(c.Callback,r,V/'controller.py',vars(c)) + tree=ast.parse((CALLER/'macro_binding.py').read_text());cls=next(x for x in tree.body if isinstance(x,ast.ClassDef) and x.name=='SelectedBinding') + nodes=[next(x for x in tree.body if isinstance(x,ast.FunctionDef) and x.name=='view'),next(x for x in cls.body if isinstance(x,ast.FunctionDef) and x.name=='child_program')] + env=dict(Callback=c.Callback,Fields=r.Fields,extend=ch.extend,Request=p.Request) + exec(compile(ast.Module(nodes,type_ignores=[]),'','exec'),env) + return w,r,c,env['child_program'] +def meter(m):return {k:getattr(m,k) for k in ('reads','writes','moves')} +def case(h,kind='unit',half=False,Q=4,L=5,adapted=False,mutation=None): + w,r,c,producer=setup(adapted);root=64**(h+2);I=root.bit_length()+1 + ia=w.Arena(I,128);ra=w.Arena(L,128);mod=ra.input(1<<(L-2));ring=w.Ring(mod) + specs={0:NS(code=0,good=False,template=NS(q=2,rank=7)),1:NS(code=1,good=True,template=NS(q=2,rank=7))} + history=[(2,0,7,0,False,False)]*h + program=r.Program.fixture(ia,ra,root,1,history,Q) + code=int(kind=='good');high=[[0]*64 for _ in range(64)] + fields=r.Fields.fixture(ia,ra,[(0,high)]*h+[(code,high)],Q) + if mutation is not None:mutation(w,r,program,fields) + original=(bytes(program.tape.cells),bytes(fields.tape.cells));live=(set(ia.live),set(ra.live)) + ia.meter=w.Meter();ra.meter=w.Meter();program.tape.meter=w.Meter();fields.tape.meter=w.Meter() + for tape in r.Tape.created:tape.visited={tape.head} + runtime=NS(indices=ia,arena=ra,context=NS(ring=ring),program=program,binding=NS(codes=NS(bits=Q))) + binding=NS(specifications=specs);event=NS(child_kind=kind,field=0,reverse=False,half=half) + try:out=producer(binding,runtime,NS(code=code),event,fields.tape) + except ValueError as error: + need(live==(set(ia.live),set(ra.live)),'rejected admission numerical cleanup') + need(program.tape.head==fields.tape.head==1,'rejected admission restored heads') + if mutation is not None:return dict(rejected=str(error),unchanged=original==(bytes(program.tape.cells),bytes(fields.tape.cells))) + raise + need(mutation is None,'malformed admission unexpectedly accepted') + need(original==(bytes(program.tape.cells),bytes(fields.tape.cells)),'borrowed program/fields unchanged') + need(live==(set(ia.live),set(ra.live)),'all temporary numerical words freed') + need(program.tape.head==fields.tape.head==out.head==1,'all public tape heads restored') + rr=2*I+L+5;cc=Q+2*I+90;ff=Q+2+4096*(L+1) + need(len(out.cells)==1+rr+(h+1)*cc,'actual child program exact extent') + n=h+1;D=rr+n*cc + expected_program=dict(reads=8*rr+1+h*(3*rr+2*I)+cc*(3*h*(h+1)//2+5*h)-h*(h+1)//2,writes=0,moves=6*rr+10+h*(2*rr+2)+cc*(h*h+5*h)) + expected_fields=(dict(reads=n*(3*ff-Q-2)+3,writes=0,moves=2*n*ff+4) if adapted else dict(reads=(3*ff-1)*n*(n+1)//2+n*(2*Q+4)+3,writes=0,moves=ff*n*(n+1)+n*(2*Q+6)+4)) + if adapted:expected_program=dict(reads=5*(rr+h*cc)+2*h*I+1,writes=0,moves=4*(rr+h*cc)+8) + need(meter(program.tape.meter)==expected_program,'exact complete program scans') + need(meter(fields.tape.meter)==expected_fields,'exact complete field scans') + need(meter(out.meter)==dict(reads=2*D+1,writes=D,moves=2*D+2),'exact output construction') + numerical=sum(meter(ia.meter).values())+sum(meter(ra.meter).values()) + upper=100000*((h+2)**2*(I+1)+(h+2)*(I+1)**2+(L+1)**3) + need(numerical<=upper,'source-derived conservative numerical action envelope') + need(len(ia.words)<=64 and len(ra.words)<=len(live[1])+64,'conservative numerical backing') + need(h<2*(I-1),'accepted root-history shrink coupling') + need(program.tape.visited==set(range(rr+h*cc+2)),'program lifetime visited span') + need(fields.tape.visited==set(range(n*ff+2)),'fields lifetime visited span') + need(out.visited==set(range(D+2)),'output lifetime visited span') + need(len(r.Tape.created)==7,'exact record tape inventory') + need(sum(len(t.visited) for t in r.Tape.created)==rr+h*cc+D+n*ff+14,'complete producer record footprint') + return dict(chronological_trace=c.semantic_trace,record_visited_cells=sum(len(t.visited) for t in r.Tape.created),adapted=adapted,output_sha256=sha256(bytes(out.cells)).hexdigest(),numerical_actions=numerical,numerical_upper=upper,h=h,I=I,L=L,Q=Q,kind=kind,half=half,r=rr,c=cc,F=ff,program=meter(program.tape.meter),fields=meter(fields.tape.meter),output=meter(out.meter),index=meter(ia.meter),residue=meter(ra.meter),index_backing=len(ia.words),residue_backing=len(ra.words),output_cells=len(out.cells)) +if __name__=='__main__': + print(json.dumps([case(h) for h in range(5)],indent=2)) + +def leaf_case(h,adapted): + w,r,c,_=setup(adapted);Q,L=5,5;root=64**(h+2);I=root.bit_length()+1 + ia=w.Arena(I,128);ra=w.Arena(L,128);mod=ra.input(8);ring=w.Ring(mod) + specs={0:NS(code=0,good=False,template=NS(q=2,rank=7))} + program=r.Program.fixture(ia,ra,root,1,[(2,0,7,0,False,False)]*h,Q) + fields=r.Fields.fixture(ia,ra,[(0,[[0]*64 for _ in range(64)])]*h,Q) + before=bytes(program.tape.cells),bytes(fields.tape.cells);live=set(ia.live),set(ra.live) + program.tape.meter=w.Meter();fields.tape.meter=w.Meter() + cb=c.Callback(ring,ia,program,fields,specs,0,allow_fallback=True,leaf=True) + need(cb.program is program,'original random-access Program identity restored') + state=[cb.root_size.inspect(),cb.root_unit.inspect(),cb.depth.inspect(),cb.final_size.inspect()] + cb.close();need(live==(set(ia.live),set(ra.live)),'leaf admission cleanup') + need(before==(bytes(program.tape.cells),bytes(fields.tape.cells)),'leaf borrowed bytes') + need(program.tape.head==fields.tape.head==1,'leaf restored public heads') + rr=2*I+L+5;cc=Q+2*I+90;F=Q+2+4096*(L+1);P=rr+h*cc;n=h + fm=(dict(reads=n*(3*F-Q-2)+3,writes=0,moves=2*n*F+4) if adapted else dict(reads=(3*F-1)*n*(n+1)//2+n*(2*Q+4)+3,writes=0,moves=F*n*(n+1)+n*(2*Q+6)+4)) + need(meter(fields.tape.meter)==fm,'leaf h-field exact scan') + if adapted:need(meter(program.tape.meter)==dict(reads=3*rr+2*h*cc+2*h*I-2,writes=0,moves=2*P+4),'leaf program scan') + return dict(h=h,state=state,trace=c.semantic_trace,fields=meter(fields.tape.meter),program=meter(program.tape.meter)) + +def projected_case(adapted): + """Peer-derived exact definition projection; no source-plan reconstruction.""" + w,r,c,producer=setup(adapted);low=load('low_codes');codes=low.LowCodes(3,64,28233) + projection=json.loads((HERE/'SOURCE_PROJECTION.json').read_text()) + need(codes.bits==projection['code_bits']==6507,'current GL code width') + defs=projection['definitions'];specs={} + for d in defs: + ident,common,matrix=codes.decode(d['code']) + need((ident,common)==(d['request_id'],d['label']=='good'),'projected exact source/view code') + digest=sha256(json.dumps(matrix,sort_keys=True,separators=(',',':')).encode()).hexdigest() + need(digest==d['low_sha256'],'projected GL low identity') + specs[d['code']]=NS(code=d['code'],good=d['good'],template=NS(q=d['q'],rank=d['rank'])) + a,b=defs;I,L,Q=13,5,codes.bits;h=1;n=2 + ia=w.Arena(I,128);ra=w.Arena(L,128);ring=w.Ring(ra.input(9)) + program=r.Program.fixture(ia,ra,2048,2,[(0,a['code'],26,0,False,False)],Q) + high=[[int(i==j) for j in range(64)] for i in range(64)] + fields=r.Fields.fixture(ia,ra,[(a['code'],high),(b['code'],high)],Q) + before=bytes(program.tape.cells),bytes(fields.tape.cells);live=set(ia.live),set(ra.live) + for tape in r.Tape.created:tape.meter=w.Meter();tape.visited={tape.head} + ia.meter=w.Meter();ra.meter=w.Meter() + runtime=NS(indices=ia,arena=ra,context=NS(ring=ring),program=program,binding=NS(codes=NS(bits=Q))) + out=producer(NS(specifications=specs),runtime,NS(code=b['code']),NS(child_kind='good',field=0,reverse=False,half=False),fields.tape) + need(before==(bytes(program.tape.cells),bytes(fields.tape.cells)),'projected borrowed bytes') + need(live==(set(ia.live),set(ra.live)),'projected numerical ownership') + need(program.tape.head==fields.tape.head==out.head==1,'projected heads') + rr=2*I+L+5;cc=Q+2*I+90;F=Q+2+4096*(L+1);P=rr+h*cc;D=rr+n*cc + fm=(dict(reads=n*(3*F-Q-2)+3,writes=0,moves=2*n*F+4) if adapted else dict(reads=(3*F-1)*n*(n+1)//2+n*(2*Q+4)+3,writes=0,moves=F*n*(n+1)+n*(2*Q+6)+4)) + need(meter(fields.tape.meter)==fm,'projected complete Fields invoice') + need(len(out.cells)==D+1,'projected serialized extent') + returned=object.__new__(r.Program);returned.index_arena=ia;returned.residue_arena=ra;returned.code_bits=Q;returned.tape=out + level=ia.input(2);metadata,parent,child=returned.step(level) + need(metadata==(0,b['code'],7,0,0,0) and parent.inspect()==832 and child.inspect()==91,'actual projected 2048->832->91 history') + ia.free_many(level,parent,child) + return dict(output_sha256=sha256(bytes(out.cells)).hexdigest(),field_actions=sum(fm.values()),chronological_trace=c.semantic_trace, + source_projection_sha256=sha256((HERE/'SOURCE_PROJECTION.json').read_bytes()).hexdigest(), + source_plan_independently_reconstructed=False,code_bits=Q,root=2048,parent=832,child=91) diff --git a/research/r437-source-preparation-bound/forward_fields.py b/research/r437-source-preparation-bound/forward_fields.py new file mode 100644 index 0000000000..45dcf2467f --- /dev/null +++ b/research/r437-source-preparation-bound/forward_fields.py @@ -0,0 +1,97 @@ +"""Package-local monotone field validator for Callback admission only. + +Not a replacement for arbitrary Fields.read/check_code. Its caller must issue +one next() for each chronological history step, then the current field unless +leaf=True, followed by finish(). The unchanged encoded Callback loop does this. +""" +import ast +from hashlib import sha256 + +def adapted_callback(base, records): + class ForwardFields: + def __init__(self, fields): + self.fields=fields + fields.tape.rewind() + def next(self, code): + tape=self.fields.tape + observed=records.read_finite(tape,self.fields.code_bits) + records.need(observed==code,'original global raw-field code') + while tape.read()!=records.RECORD_END: + records.need(tape.read()!=records.BLANK,'record exists at global slot') + tape.step(1) + tape.step(1) + def finish(self): + tape=self.fields.tape + complete=tape.read()==records.BLANK + tape.rewind() + records.need(complete,'exact frozen/current field prefix') + class ForwardCallback(base): pass + return ForwardCallback,ForwardFields + +def install(base,records,path,namespace): + tree=ast.parse(path.read_text()) + cls=next(x for x in tree.body if isinstance(x,ast.ClassDef) and x.name=='Callback') + method=next(x for x in cls.body if isinstance(x,ast.FunctionDef) and x.name=='_validate_program') + records.need(sha256(ast.dump(method).encode()).hexdigest()=='182c3b095d95d7ccf98d6f5e881aa58f0619621fc17b8e77030cdc4c086967b6','exact reviewed admission AST') + class Rewrite(ast.NodeTransformer): + def __init__(self):self.checks=self.ends=self.program_seeks=0 + def visit_Expr(self,node): + if isinstance(node.value,ast.Call) and isinstance(node.value.func,ast.Name) and node.value.func.id=='seek_record': + records.need(ast.unparse(node.value)=='seek_record(self.program.tape, after)','exact terminal program seek') + self.program_seeks+=1 + return ast.Pass() + return self.generic_visit(node) + def visit_Call(self,node): + if isinstance(node.func,ast.Attribute) and ast.dump(node.func.value)==ast.dump(ast.parse('self.fields',mode='eval').body): + if node.func.attr=='check_code': + records.need(len(node.args)==2 and not node.keywords,'exact check_code shape') + self.checks+=1 + return ast.Call(ast.Attribute(ast.Name('cursor',ast.Load()),'next',ast.Load()),[node.args[1]],[]) + if node.func.attr=='end': + records.need(len(node.args)==1 and not node.keywords,'exact end shape') + self.ends+=1 + return ast.Call(ast.Attribute(ast.Name('cursor',ast.Load()),'finish',ast.Load()),[],[]) + raise ValueError('unreviewed field use in admission') + return self.generic_visit(node) + edit=Rewrite();method=edit.visit(method) + records.need((edit.checks,edit.ends,edit.program_seeks)==(2,2,1),'exact monotone admission sites') + method.body.insert(0,ast.parse('cursor = ForwardFields(self.fields)').body[0]) + cls,cursor=adapted_callback(base,records) + env=dict(namespace,ForwardFields=cursor) + exec(compile(ast.fix_missing_locations(ast.Module([method],type_ignores=[])),str(path),'exec'),env) + forward_program=program_cursor(records,path.with_name('records.py')) + admitted=env['_validate_program'] + def validate(self): + original=self.program + self.program=forward_program(original) + try:admitted(self) + finally:self.program=original + cls._validate_program=validate + return cls + + +def program_cursor(records,path): + tree=ast.parse(path.read_text()) + cls=next(x for x in tree.body if isinstance(x,ast.ClassDef) and x.name=='Program') + methods=[] + for name in ('root','step'): + method=next(x for x in cls.body if isinstance(x,ast.FunctionDef) and x.name==name) + records.need(sha256(ast.dump(method).encode()).hexdigest()==PROGRAM_AST[name],'exact reviewed Program AST') + records.need(ast.unparse(method.body[-2])=='self.tape.rewind()','terminal Program rewind') + method.body[-2]=ast.parse('self.tape.step(1)').body[0] + if name=='step': + records.need(ast.unparse(method.body[1])=='seek_record(self.tape, level)','initial Program seek') + method.body.pop(1) + methods.append(method) + env=dict(vars(records)) + exec(compile(ast.fix_missing_locations(ast.Module(methods,type_ignores=[])),str(path),'exec'),env) + class ForwardProgram: + def __init__(self,program): + self.tape=program.tape + self.code_bits=program.code_bits + self.index_arena=program.index_arena + self.residue_arena=program.residue_arena + ForwardProgram.root=env['root'];ForwardProgram.step=env['step'] + return ForwardProgram + +PROGRAM_AST={'root': 'f1ce38c0bab29ef74f2f0d60373d08cfae69cbbd6b1539914d10ea4001909c02', 'step': 'a1358d976440865d1dff2c410874b89426949c3123350dd132e8eb9a7867af39'} diff --git a/research/r437-source-preparation-bound/test_export.py b/research/r437-source-preparation-bound/test_export.py new file mode 100644 index 0000000000..45b9ea4aa9 --- /dev/null +++ b/research/r437-source-preparation-bound/test_export.py @@ -0,0 +1,57 @@ +"""Git-free positive replay and exact-source/receipt rejection under -O.""" +from pathlib import Path +import json +import os +import shutil +import subprocess +import sys +import tempfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +PACKAGE = HERE.relative_to(ROOT) + + +def need(ok, message): + if not ok: raise ValueError(message) + + +def main(): + pins = [r for r in json.loads((HERE/'SOURCES.json').read_text())['files'] if r['usage']=='input'] + with tempfile.TemporaryDirectory(prefix='r437-producer-export-') as directory: + root = Path(directory) + package = root/PACKAGE + shutil.copytree(HERE, package, ignore=shutil.ignore_patterns('__pycache__', '*.pyc')) + for row in pins: + target = root/row['path'] + target.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(ROOT/row['path'], target) + env = dict(os.environ) + env.pop('PYTHONPATH', None) + env.pop('PYTHONOPTIMIZE', None) + def run(): + return subprocess.run([sys.executable,'-O','-B','-X',f'pycache_prefix={root}/private-cache',str(package/'verify.py')], + cwd=root, env=env, capture_output=True, text=True, timeout=180) + positive = run() + need(positive.returncode == 0, 'Git-free optimized positive: '+positive.stderr) + rejected = 0 + for row in pins: + target = root/row['path'] + before = target.read_bytes() + target.write_bytes(before+b'\n# intentional corruption control\n') + result = run() + need(result.returncode != 0 and 'changed source: '+row['path'] in result.stderr, + 'exact source mutation rejected before import: '+row['path']) + target.write_bytes(before) + rejected += 1 + receipt = package/'RESULT.json' + value = json.loads(receipt.read_text()) + value['status'] = 'intentional receipt corruption' + receipt.write_text(json.dumps(value)) + result = run() + need(result.returncode != 0 and 'committed exact receipt' in result.stderr, + 'changed mathematical receipt rejects under optimization') + print('PASS Git-free optimized positive;', rejected, 'source mutations and changed receipt reject') + + +if __name__ == '__main__': main() diff --git a/research/r437-source-preparation-bound/verify.py b/research/r437-source-preparation-bound/verify.py new file mode 100644 index 0000000000..6749de14a7 --- /dev/null +++ b/research/r437-source-preparation-bound/verify.py @@ -0,0 +1,53 @@ +"""Bounded exact producer tariff, monotone-adapter equivalence and controls.""" +import json +from pathlib import Path +import check +HERE=Path(__file__).resolve().parent + +def run(): + pairs=[] + for h,kind,half,Q,L in [(0,'unit',False,4,5),(1,'good',False,4,5),(2,'pair',False,5,6),(3,'unit',True,4,5),(4,'good',False,8,5),(6,'unit',False,8,7)]: + a=check.case(h,kind,half,Q,L,False);b=check.case(h,kind,half,Q,L,True) + check.need(a['output_sha256']==b['output_sha256'],'byte-identical actual child program') + for label in ('output','residue','record_visited_cells','chronological_trace'): + check.need(a[label]==b[label],'unchanged non-field component '+label) + check.need(b['numerical_actions']