From e2e707fd99125ef0005ad16435d90e5d3a82f31e Mon Sep 17 00:00:00 2001 From: CubeJerry <80299683+CubeJerry@users.noreply.github.com> Date: Tue, 10 Nov 2026 00:25:03 +0800 Subject: [PATCH] research: execute current two-output arithmetic services as finite tables --- research/current-swap-flat-tables/.gitignore | 2 + .../DEPENDENCIES.json | 69 +++ research/current-swap-flat-tables/OVERLAP.md | 29 + .../PR-DESCRIPTION.md | 99 ++++ research/current-swap-flat-tables/PROOF.md | 267 +++++++++ research/current-swap-flat-tables/README.md | 119 ++++ research/current-swap-flat-tables/RESULT.json | 187 +++++++ .../current-swap-flat-tables/SOURCES.json | 36 ++ research/current-swap-flat-tables/TASK.json | 87 +++ .../current-swap-flat-tables/VERIFICATION.md | 122 ++++ research/current-swap-flat-tables/VERIFY.json | 108 ++++ .../check_controls.py | 129 +++++ .../evidence/initial-arithmetic.log | 2 + .../evidence/initial-binding.log | 2 + .../evidence/initial-controller.log | 2 + .../evidence/initial-controls.log | 2 + .../evidence/registered-replay.log | 25 + research/current-swap-flat-tables/fixtures.py | 89 +++ research/current-swap-flat-tables/physical.py | 136 +++++ .../source_binding.py | 35 ++ research/current-swap-flat-tables/tables.py | 150 +++++ .../vendor/current_caller.py | 175 ++++++ .../vendor/lifecycle/machine.py | 406 ++++++++++++++ .../vendor/lifecycle/source_ir.py | 522 ++++++++++++++++++ .../vendor/scalar_tables.py | 295 ++++++++++ .../current-swap-flat-tables/vendor/stack.py | 170 ++++++ research/current-swap-flat-tables/verify.py | 187 +++++++ 27 files changed, 3452 insertions(+) create mode 100644 research/current-swap-flat-tables/.gitignore create mode 100644 research/current-swap-flat-tables/DEPENDENCIES.json create mode 100644 research/current-swap-flat-tables/OVERLAP.md create mode 100644 research/current-swap-flat-tables/PR-DESCRIPTION.md create mode 100644 research/current-swap-flat-tables/PROOF.md create mode 100644 research/current-swap-flat-tables/README.md create mode 100644 research/current-swap-flat-tables/RESULT.json create mode 100644 research/current-swap-flat-tables/SOURCES.json create mode 100644 research/current-swap-flat-tables/TASK.json create mode 100644 research/current-swap-flat-tables/VERIFICATION.md create mode 100644 research/current-swap-flat-tables/VERIFY.json create mode 100644 research/current-swap-flat-tables/check_controls.py create mode 100644 research/current-swap-flat-tables/evidence/initial-arithmetic.log create mode 100644 research/current-swap-flat-tables/evidence/initial-binding.log create mode 100644 research/current-swap-flat-tables/evidence/initial-controller.log create mode 100644 research/current-swap-flat-tables/evidence/initial-controls.log create mode 100644 research/current-swap-flat-tables/evidence/registered-replay.log create mode 100644 research/current-swap-flat-tables/fixtures.py create mode 100644 research/current-swap-flat-tables/physical.py create mode 100644 research/current-swap-flat-tables/source_binding.py create mode 100644 research/current-swap-flat-tables/tables.py create mode 100644 research/current-swap-flat-tables/vendor/current_caller.py create mode 100644 research/current-swap-flat-tables/vendor/lifecycle/machine.py create mode 100644 research/current-swap-flat-tables/vendor/lifecycle/source_ir.py create mode 100644 research/current-swap-flat-tables/vendor/scalar_tables.py create mode 100644 research/current-swap-flat-tables/vendor/stack.py create mode 100644 research/current-swap-flat-tables/verify.py diff --git a/research/current-swap-flat-tables/.gitignore b/research/current-swap-flat-tables/.gitignore new file mode 100644 index 0000000000..7a60b85e14 --- /dev/null +++ b/research/current-swap-flat-tables/.gitignore @@ -0,0 +1,2 @@ +__pycache__/ +*.pyc diff --git a/research/current-swap-flat-tables/DEPENDENCIES.json b/research/current-swap-flat-tables/DEPENDENCIES.json new file mode 100644 index 0000000000..83ee005fd6 --- /dev/null +++ b/research/current-swap-flat-tables/DEPENDENCIES.json @@ -0,0 +1,69 @@ +{ + "schema_version": 1, + "files": [ + { + "repository": "CubeJerry/integer-mult-bounds", + "commit": "ab239cb6ee884e7a900dd9101c34448077fad0b0", + "original_path": "research/compiled-owned-bank-lifecycle/machine.py", + "local_path": "vendor/lifecycle/machine.py", + "git_blob": "acf475e4fccaff2fb64bd5b0b3f3fc0d246dc592", + "bytes": 14932, + "sha256": "ec597bce13275003ff30e4be481c936401826c1d4af642b55eec0c410774d1df" + }, + { + "repository": "CubeJerry/integer-mult-bounds", + "commit": "ab239cb6ee884e7a900dd9101c34448077fad0b0", + "original_path": "research/compiled-owned-bank-lifecycle/source_ir.py", + "local_path": "vendor/lifecycle/source_ir.py", + "git_blob": "79c95fa79439f3c893de52991173bd3a5eae2729", + "bytes": 27393, + "sha256": "54dd93bc50bd10e974c70794df1c13da27f0e3d8cdb6cfe6791a63280096f1b1" + }, + { + "repository": "CrocSwap/integer-mult-bounds", + "commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_path": "research/delimited-continuation-stack/stack.py", + "local_path": "vendor/stack.py", + "git_blob": "a5d6753b901901a5b2d1a4dd72134e53af70c666", + "bytes": 5657, + "sha256": "21a2213aa850c55e5eace4cd10b72b958d7ee84d83a014567902ce8ee9b3f4f2" + }, + { + "repository": "CubeJerry/integer-mult-bounds", + "commit": "13193a22b1070a74a8580c5d3ea27470443f815a", + "original_path": "research/current-scalar-flat-tables/physical.py", + "local_path": "physical.py", + "git_blob": "781a0fef1745effd9b6cfebac7ebdef982eec955", + "sha256": "506326b47469ad3f8d9731a09ae935778130b4a8e532a1adc8ae144742e81fe5", + "bytes": 4915 + }, + { + "repository": "CubeJerry/integer-mult-bounds", + "commit": "13193a22b1070a74a8580c5d3ea27470443f815a", + "original_path": "research/current-scalar-flat-tables/tables.py", + "local_path": "vendor/scalar_tables.py", + "git_blob": "1cc22f75fbe53d48b84be42782e581c04820cd49", + "sha256": "654e9734ef80a9394807ca508543b1bc164afb5768d23d0e5a88c790d2f13bac", + "bytes": 12650 + }, + { + "repository": "CrocSwap/integer-mult-bounds", + "commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_path": "research/p104-productive-controller/caller.py", + "local_path": "vendor/current_caller.py", + "usage": "reference-only; not imported", + "git_blob": "6ac5e735691555ecafe2afbcff71edd923178113", + "sha256": "300d40043953e4f6aecfde8f2d1004b8ad6dc5a79ec3c7666c9908c2466c91c8", + "bytes": 10267 + }, + { + "repository": "CubeJerry/integer-mult-bounds", + "commit": "13193a22b1070a74a8580c5d3ea27470443f815a", + "original_path": "research/current-scalar-flat-tables/source_binding.py", + "local_path": "source_binding.py", + "git_blob": "4b3812a7f4c87d7a9d62b16fed4ea68d8fa0e7ad", + "bytes": 1020, + "sha256": "6c64b140c4c9c4d58927a1b0f3f5e40b4b1657ea80fe6989e714ea295d18be31" + } + ] +} diff --git a/research/current-swap-flat-tables/OVERLAP.md b/research/current-swap-flat-tables/OVERLAP.md new file mode 100644 index 0000000000..cca7dfe085 --- /dev/null +++ b/research/current-swap-flat-tables/OVERLAP.md @@ -0,0 +1,29 @@ +# Bounded source-class overlap check + +Prepared for @CubeJerry with substantial OpenAI assistance. No novelty priority +is claimed for swapping, signed permutations or complement-plus-one negation. + +Canonical source base: `7c49fe32c55de02c2c873655c804b16e4c3fef0a`. +The lead's wave-2 assignment isolates the 10,920 original two-output services +omitted from the frozen ADD/SCALE package. Native phase/Gaussian/MOVE, Compact, +row, complete-Core, full-caller precision and κ work remain excluded. + +Inspected exact current `source_ir`, caller JSON and original `caller.py`. +Bounded GitHub PR-body searches used `SIGNED_SWAP`, `swap physical`, +`scalar table`, and the exact historical package slug. These identify nearby +work but are not an exhaustive novelty certificate; arbitrary unpublished +work and uninspected diffs remain limits. + +| Predecessor | Proved or implemented scope | Distinction here | +| --- | --- | --- | +| Frozen current ADD/SCALE tables | 366,842 current one-output arithmetic services on the coded ABI | Those tables are retained unchanged; only SWAP/SIGNED_SWAP are newly implemented | +| #3098, physical-scalar-stream | Older inherited recipes on aligned sequential packets | Actual current ordered source/table/lifecycle join is the scope here | +| #969, complex-swap-runs-seed37 | Deferred historical names, paid boundary materialization, 560 primitive saving | This executes every current swap physically and claims no primitive-count saving | +| #4516, pr4470-controller-replay | Exact Laurent signs and complete old p16 algebra | This supplies numerical all-width tables; its source is the newer productive controller | +| #6901 | Ideal common precision/temporary format | Geometry, common grid and source-cut range remain premises here | +| #5427 and #4621 search matches | Retained algebraic response/reuse and query-shear window questions | Neither supplies these current coded two-output transition tables | + +The source instruction census is not offered as a stand-alone research result. +The contribution is the executable source-class closure, exact signed success +domain, complete two-work-port lifecycle proof, and tested composition with +the retained scalar service registry. All five selected assumptions remain. diff --git a/research/current-swap-flat-tables/PR-DESCRIPTION.md b/research/current-swap-flat-tables/PR-DESCRIPTION.md new file mode 100644 index 0000000000..d62fbdcca3 --- /dev/null +++ b/research/current-swap-flat-tables/PR-DESCRIPTION.md @@ -0,0 +1,99 @@ +## Result and scope + +**No new κ.** This closes the current SWAP/SIGNED_SWAP source class on the +same two-work-port coded lifecycle ABI as the preceding ADD/SCALE provider. +The exact ordered operations are `(x,y) -> (y,x)` and `(x,y) -> (y,-x)`. +The all-width theorem gives exact final signed admission, whole-pair validation +before either public write, preserved complete shapes, head return and physical +work erasure through unchanged `execute_table` and `Controller.primitive`. + +SWAP always succeeds on its admitted common shape/grid. SIGNED_SWAP succeeds +exactly when no old first-operand component is most-negative in its original +width; the old second operand may be most-negative. There is no extra +intermediate-word headroom requirement. The 130-row and 171-row tables contain +only local branch/write/unit-move/goto/halt/reject instructions, with no +numerical callback or decoded field length. + +The source binder covers 10,920 current services: 2,808 right-boundary swaps, +3,120 left-boundary swaps and 4,992 outer signed swaps. Together with the frozen +scalar provider, this supplies tables for all 377,762 original +ADD/SCALE/SWAP/SIGNED_SWAP services in the exact 642,410-event caller. This is +one physical compiler/lifecycle implication; all five selected assumptions +remain globally, and conditional κ remains 0.003125804. + +## Novelty and exact dependencies + +CrocSwap/integer-mult-bounds#3098 supplies older aligned scalar-recipe +execution. CrocSwap/integer-mult-bounds#969 defers historical names and pays +boundary copies, explicitly excluding physical-array/current production +admission. CrocSwap/integer-mult-bounds#4516 verifies the older caller's exact +Laurent signs. This package executes every original current two-output service +on actual coded fields, keeps the current operand order, and proves its complete +two-work-port physical contract. Classical swapping and signed negation are +credited background, not new arithmetic discoveries or count improvements. + +- Canonical base: `7c49fe32c55de02c2c873655c804b16e4c3fef0a`. +- The exact original productive `caller.py`, selected word and controller have + Git blob/SHA256 pins in `SOURCES.json`; the original semantic source is also + retained unchanged as a reference-only file. +- The unchanged lifecycle/source compiler is pinned at + `ab239cb6ee884e7a900dd9101c34448077fad0b0`. +- The unchanged [preceding current scalar tables](https://github.com/CubeJerry/integer-mult-bounds/tree/13193a22b1070a74a8580c5d3ea27470443f815a/research/current-scalar-flat-tables) + are pinned at `13193a22b1070a74a8580c5d3ea27470443f815a` and retained for + the actual mixed right-boundary replay. No predecessor file is modified. + +## Reproduction and checks + +```sh +python3 -B scripts/research_package.py --package research/current-swap-flat-tables +``` + +Eight bounded normal/optimized commands check arithmetic, complete source +binding, real unchanged-controller blocks and controls against exact committed +receipts. The independent direct permutation/sign oracle covers all 2,728 +signed x,y pairs at widths 1–5 for both operations, plus 96 wider/mixed-width +fields up to width 129. Thirty-two boundary/failure controls include late +component overflow, signed minimum/zero cases, aliases, shape/source failures, +four code mutants, physical ordered inverse, dirty extra work and shrinking +retained backing. + +On all 13,444 public fields, the actual full 5,720-service right boundary +executes 11,015,757 physical actions and 1,493,648 table steps; the actual first +104-service signed block executes 216,813 actions and 28,912 steps. Every +public endpoint and spectator is checked. Receipts bind exact source cuts, +compiled code, executed tables, complete physical input/output bodies and +decoded outputs. These are explicit entry-cut fixtures, not execution of the +omitted preceding native services or the complete recursive caller. + +A separate lead AI mathematical review checked the exact original source +order, finite-carry identity, most-negative iff guard, staging induction and +full lifecycle/cost premises. Its independent integer enumeration checked all +8,190 first inputs at widths 1–12, with 8,178 admitted, without importing +table code. This review is distinct from physical executor replay and from +human or proof-kernel acceptance. + +## Limits and remaining obligations + +The complete positive bill is `O(V+D+Q)` and current work backing is +`2V+3+O(1)`, with erased historical backing retained as a maximum. Actual +matching coordinate shapes/grids, distinct owners, head origins and valid +dirty work remain premises. Rejection preserves both public contents but may +leave heads advanced and work occupied; no physical rollback is claimed. + +No native phase/Gaussian/MOVE service, row/recursive return, whole-caller +precision/error contract, global ownership theorem, complete historical +numerical allowance or analytic recovery is supplied. The new tables do not +alter paid jobs, productive targets or the selected certificate. + +## Credit and assistance + +Prepared for **@CubeJerry**, with substantial OpenAI assistance in mathematical +derivation, source analysis, implementation and verification. Preserve the +preceding scalar/lifecycle package, Jose Manuel/jmbarrancoml's +CrocSwap/integer-mult-bounds#3098 lineage, ToikY's +CrocSwap/integer-mult-bounds#969 package, the exact controller replay of +CrocSwap/integer-mult-bounds#4516, Ali Romman's productive caller and +CrocSwap/integer-mult-bounds#5356 continuation source, DreamingOfClouds' +CrocSwap/integer-mult-bounds#6030 selected word, and the retained native/compiler +lineage. Separate AI review does not establish independent human or formal +proof-kernel admission. diff --git a/research/current-swap-flat-tables/PROOF.md b/research/current-swap-flat-tables/PROOF.md new file mode 100644 index 0000000000..4ff87d3842 --- /dev/null +++ b/research/current-swap-flat-tables/PROOF.md @@ -0,0 +1,267 @@ +# Actual current SWAP and SIGNED_SWAP services on coded tapes + +Prepared for **@CubeJerry**, with substantial OpenAI assistance. Apache-2.0. +This is a source-bound implementation lemma. **No new κ.** + +## 1. Exact source and quantified claim + +Canonical base is `7c49fe32c55de02c2c873655c804b16e4c3fef0a`. The retained +`research/p104-productive-controller/caller.py`, function `replay`, defines +the two ordered operations exactly as + + SWAP(x,y): (x,y) <- (y,x), + SIGNED_SWAP(x,y): (x,y) <- (y,-x). + +In particular, the negated operand is the **old first operand**. Both fields +are outputs. This definition is pinned in SOURCES.json and in the unmodified, +reference-only `vendor/current_caller.py`; that file is not imported by the +new verifier. The current `source_ir.current_caller` emits each operation for +all 104 source columns, retaining its ordered actual fields and source token. + +For these two operations, `compile_swap` emits finite tables in the unchanged +published lifecycle `execute_table` grammar. Tables use only local-symbol +branch, local-symbol write, unit move, goto, halt and reject. Their ordered +ports are `(x,y,staged-x,guide)`. The two work ports are the **same inventory** +needed by the preceding current ADD/SCALE tables; no extra numerical tape or +runtime payload callback is introduced. + +The inputs are nonempty complete complex fields with the same ordered +component shapes and coordinate meanings. Each component is a nonempty +little-endian two's-complement word followed by virtual delimiter 2. The even +component count groups successive real/imaginary pairs into complex records. +Corresponding widths agree, but widths may vary between components. Matching +components use the same numerical grid. Each virtual symbol occupies the +inherited three raw nonblank binary bits. An actual physical blank immediately +follows the complete last component; there is no encoded logical blank or +hidden live tail in a public field. + +All public, work and context heads start at their current origins. The two +data tapes and two used work tapes are physically distinct; all other supplied +ports are nonaliasing. Every port retains its current owned segment and protected +ancestor boundary. Initially dirty work consists of contiguous raw binary +prefixes ending at a physical blank. These are the original lifecycle and +`retire` contracts, not facts inferred from numerical values. + +**Theorem.** On those inputs, SWAP always succeeds. SIGNED_SWAP succeeds if +and only if no component of x is the most-negative value of its original +signed width. Equivalently, the requested output pair fits the original +component widths. On success it returns the exact ordered pair above, +preserves both complete field extents, component boundaries and common grids, +returns every supplied head to its current origin, and returns all work +physically blank under the original primitive wrapper. It makes no write to +either public field before the complete pair has passed its checks. + +The time is `O(V+D+Q)`, with two used work tapes and current work backing +`2V+3+O(1)`. Here V is either public field's physical length, D is total +initially occupied work, and Q is the fixed supplied work/context inventory. +Erased historical backing remains counted as a coordinatewise maximum. + +## 2. Finite signed-word admission + +For SWAP the staged word is a literal copy of x. Its signed value and width +are unchanged, so its range condition is automatic. The second candidate is +the original complete y field, which remains untouched until installation. + +For SIGNED_SWAP the first pass computes the ordinary complement-plus-one +word into the separate staged field. Let x_i be a bit of x, with i increasing +from zero. Set c_0=1 and use + + u_i = 1-x_i+c_i, + z_i = u_i mod 2, + c_(i+1) = floor(u_i/2). + +Both carries and bits belong to `{0,1}`. These are finite transition choices, +not runtime host arithmetic. The generated table remembers the last input +and output bits sx,sz, then validates the complete component at its delimiter. +The width is never supplied or decoded by the routine. + +For a component of width w, write X and Z for the unsigned bit-word values. +Summing the digit equations yields + + Z = 2^w-X-2^w*c_w. + +If X=0, the carry remains one and Z=0. Otherwise the carry becomes zero at +the first one bit of X and remains zero, so Z=2^w-X. Consequently: + +* If the signed input x is zero, the signed output is zero. +* If x is positive, its sign is sx=0 and the output sign is sz=1; its signed + value is -x. +* If x is negative, sx=1 and `1 <= Z <= 2^(w-1)`. The output has sign sz=1 + exactly when `X=2^(w-1)`, meaning `x=-2^(w-1)`. That is the sole overflow. + Otherwise sz=0 and the signed output is -x. + +The final finite guard therefore rejects **exactly** `sx=sz=1` in signed +mode. This includes w=1: zero is the only admitted first input, while the +second input may be either -1 or zero. There is no negative-zero convention. +The old second operand may be most-negative at any width; it is copied, not +negated. Equal values on distinct tapes are allowed, with no independence or +uncorrelated-input hypothesis. + +For completeness, any representable -x passes this exact guard. For soundness, +the displayed identity proves that any passing staged word represents -x. +No intermediate signed sum, extra signed word or temporary-word headroom is +required. The table emits exactly one bit per input bit and one delimiter per +accepted component. Common numerical grids are preserved without division or +rounding. If the represented inputs already carry numerical errors, the +output error pair is the same signed permutation of those errors; absolute +componentwise bounds and every permutation-invariant norm are unchanged. + +## 3. Protecting both outputs with two work tapes + +The first pass reads x and y in lockstep. The staged work holds x or -x, and +the original y is the other candidate output. Neither public field is written. +A second work guide holds virtual marker 5 followed by one virtual 1 for +every consumed public symbol, including delimiters. Empty components, +mismatched boundaries/frontiers and an odd or empty component count reject. + +The table checks every component's signed guard, both final frontiers, and +the staged frontier before starting installation. In particular a failure in +the last component leaves **both** public contents unchanged. Under valid +geometry, the protected candidate pair at that point is `(original y, staged +signed x)`; it is unnecessary to duplicate y on a third work tape. + +Let L be the common virtual field length, so V=3L. The guide contains marker +5 followed by exactly L ones. Starting at its blank frontier, the table moves +the guide left and reads it. For each one, it moves x, y and the staged field +left once. On marker 5 they have each moved exactly L symbols to their current +origins. No numerical length or position query controls this rewind. It stops +before another public left move could cross an origin. + +The table then advances past the guide marker. For each guide one it reads +the old y symbol and the staged symbol into its finite control **before** +writing either public field. It writes the saved y symbol to x, the staged +symbol to y, and advances all four ports once. An induction on the installed +prefix proves that the prefix has the required two outputs while the unread +y suffix remains original and the staged field remains unchanged. Reading +before writing is possible with a fixed number of local symbols in control; +there is no unbounded source buffer or uncharged access. + +The two candidate symbols have matching delimiter positions. Installation +therefore preserves both complete shapes and ends exactly at their physical +frontiers. All supplied heads are then returned by the unmodified table +executor's raw-origin loops. The unmodified `Controller.primitive` retires +all work before and after a successful service, erasing actual raw bits +including coded guide markers. Writing a coded logical blank is not used as +physical erasure. Additional work is also retired; read-only binary contexts +and all other public spectators are preserved. + +The proof is by component and by consumed prefix and is independent of width, +record count, correlation between inputs, and the particular old contents of +the initially valid dirty work. Physical aliasing is excluded by the original +controller and by source binding; equality of numerical values is harmless. + +The signed operation can be undone by the same table with **reversed ordered +ports**. If its first call returns `(y,-x)`, a call on the ordered pair +`(-x,y)` returns `(y,x)` in that reversed naming, restoring the original +physical fields. The second negated input -x cannot be most-negative after a +successful first call. Four forward calls need not all be admitted when y +was most-negative; no such stronger same-domain assertion is made. + +On rejection the inherited executor raises immediately. Public contents have +not been written, but heads may be advanced and work occupied; success cleanup +has not run. No physical rollback or interruption recovery is claimed. +For otherwise well-formed inputs, arithmetic rejection stops in the first +pass. Its visited prefix and work are bounded by the corresponding complete +pass, so it also obeys the time/backing ceiling below without acquiring a +cleanup guarantee. + +## 4. Complete costs and retained backing + +The first pass consumes L actual input symbols and performs bounded work per +symbol on both sources, the staged output and guide. The negation carry and +all remaining state (last bits, component parity and initial-field flag) are +finite. The guide rewind and installation each make L iterations. Both +source access passes, writes of both outputs, every head movement and physical +retirement are included. + +A `CodedPort` read/write/unit move costs at most 13 physical cell actions. +Charging table-row fetches as well, conservative allowances are 128 per +first-pass symbol, 64 per rewind symbol, 128 per install symbol, and 96 per +symbol for final head restoration and work retirement, plus fixed entry/exit +cost below 256. A dirty initial raw prefix costs at most `5D+O(Q)` to retire; +untouched extra work/context ports add only fixed entry/exit work per port +because their heads start at their origins. Thus one explicit ceiling is + + physical cell actions + table-row steps + <= 1024*(L+1) + 8D + 32Q. + +The fixture observer counts table-row fetches separately without changing +the emitted rows or the original interpreter. The numerical runtime does not +inspect these counters. This ceiling is intentionally loose and does not +certify any complete historical numerical allowance or full supplier bill. + +The staged field has V raw bits; the guide has V+3. Current work backing is +therefore at most `2V+3+O(1)`, including the frontiers. A prior larger body is +physically erased before reuse. Later smaller calls stop at their current +blank frontiers and do not scan the old erased high-water range. For each work +tape the retained allocation is bounded by the maximum of its prior backing +and its current needed extent. Repeated calls pay their actual current volumes +and initial dirt, not a fictitious deletion of visited tape cells. + +All supplied source fields, descriptors, parked ancestor segments and separate +caller storage remain in the caller's full inventory. This lemma controls +the two used current work tapes; it does not remove those other storage terms. + +## 5. Exact current source binding and composition + +The original source and lowerer, with immutable pins in SOURCES.json and +DEPENDENCIES.json, give the following complete two-output class: + +| Original source region | Raw instructions | Emitted services | +| --- | ---: | ---: | +| Right-boundary SWAP | 27 | 2,808 | +| Left-boundary SWAP | 30 | 3,120 | +| Outer SIGNED_SWAP | 48 | 4,992 | +| Total | 105 | 10,920 | + +There are exactly two generated tables: 130 rows for SWAP and 171 for +SIGNED_SWAP. `source_literal` checks the exact boundary instruction or exact +outer source site, column, operation and ordered fields. For an unremapped +event it additionally checks the original `(104*x+j,104*y+j)` binding. +For the original compiler's remappings it follows the active final member +of each exact wrapper grammar. The separate issuing PAID token retained by +`product-right` is provenance, not an active scalar instruction. + +The remapped owner tuple is the tuple actually emitted by the authenticated +lowerer. Its geometric alignment and mapping theorem remain premises; merely +wrapping a forged tuple would not prove its provenance. The positive nested +product/unit-fragment check uses the unchanged original `IR.remap`. + +Combined with the byte-identical preceding ADD/SCALE tables, this covers all +**377,762 original ADD/SCALE/SWAP/SIGNED_SWAP service occurrences** of the +642,410-event selected caller. The two classes have disjoint source tokens, +compatible input formats and the same two work ports. COPY retains the +original lifecycle implementation. The new tables change no field assignment, +native operation, paid job, chronological order or paid histogram. + +Assume each actual source cut supplies matching complete coordinate shapes, +common grids, distinct owned ports and the exact signed range required at its +output. Substitution of the appropriate table at each of these original +arithmetic services preserves its numerical endpoint, geometry and successful +lifecycle contract. Induction over those actual sites proves the scalar +substitution implication. It does not prove the source geometry premises, +native/recursive entrance and return predicates, the full compiler/ownership +theorem, global precision/cost closure or analytic recovery. + +## 6. Prior work and remaining obligations + +The preceding current-scalar package supplies the authenticated coded +ADD/SCALE interface and its general rational finite-carry proof. This package +retains its `Builder`, physical fixture and current source maps unchanged; +those are credited dependencies, not new results. It completes the omitted +two-output source class on the same inventory and tests their real composition +on the entire original 5,720-service right boundary. + +The older #3098 `physical-scalar-stream` executes inherited scalar recipes on +aligned packets; its actual caller/owner join remains distinct. Historical +#969 `complex-swap-runs-seed37` defers scalar names and pays boundary copies in +PR626/PR696 words. It explicitly excludes physical array execution and current +production admission. The exact Laurent controller replay in #4516 checks +the algebraic swap signs, not these numerical tables. Classical swapping and +two's-complement negation are not claimed as new arithmetic discoveries. + +Current native phase/Gaussian maps, row/recursive services and their exact +error contracts, complete compiler/owned lifecycle composition, and the +whole-caller precision/full-cost/analytic join remain open. No native service +is replaced by an ordinary swap. All five selected assumptions remain in +force, and the selected conditional κ remains 0.003125804. diff --git a/research/current-swap-flat-tables/README.md b/research/current-swap-flat-tables/README.md new file mode 100644 index 0000000000..b4380cb43f --- /dev/null +++ b/research/current-swap-flat-tables/README.md @@ -0,0 +1,119 @@ +# Current two-output swaps as executable coded-tape tables + +Prepared for **@CubeJerry**, with substantial OpenAI assistance. **No new κ.** + +This package closes the current **SWAP/SIGNED_SWAP source class** on the same +two-work-port physical ABI as the preceding ADD/SCALE tables. The actual +ordered semantics are `(x,y) -> (y,x)` and `(x,y) -> (y,-x)`. The generated +130-row and 171-row tables execute through the unchanged published lifecycle +`execute_table` and `Controller.primitive`; they contain no runtime numerical +callback, decoded width or field-length parameter. + +For arbitrary nonempty complete complex fields with matching ordered shapes +and grids, SWAP always succeeds. SIGNED_SWAP succeeds exactly when the old +first operand has no most-negative component in its original signed width. +The second operand may be most-negative. This is exactly final-output signed +admission, with no intermediate-word headroom requirement. + +The routine stages x or -x and leaves y protected. After checking the **entire +pair**, it installs `(old y, staged signed x)`, reading each old y symbol before +overwriting it. There are no writes to either public field before full-field +admission, including when the last component fails. On success the original +wrapper returns all heads and physically erases work. An immediate rejection +can leave heads advanced and work occupied; physical rollback is not claimed. + +## Exact source closure + +Canonical base is `7c49fe32c55de02c2c873655c804b16e4c3fef0a`. The selected +certificate remains conditional at **κ = 0.003125804**, with all five assumptions. + +| Source region | Original instructions | Emitted current services | +| --- | ---: | ---: | +| Right-boundary SWAP | 27 | 2,808 | +| Left-boundary SWAP | 30 | 3,120 | +| Outer SIGNED_SWAP | 48 | 4,992 | +| Total | 105 | **10,920** | + +The original current source mapper expands each instruction across 104 +columns. The binder retains actual ordered owners through caller/product/ +unit-fragment wrappers and checks exact source instructions. It separates +active source tokens from issuing PAID provenance in chronological products. + +Combined with the frozen [current ADD/SCALE package](https://github.com/CubeJerry/integer-mult-bounds/tree/13193a22b1070a74a8580c5d3ea27470443f815a/research/current-scalar-flat-tables), +this supplies tables for all **377,762 original ADD/SCALE/SWAP/SIGNED_SWAP +services** in the 642,410-event selected caller. COPY keeps its original +lifecycle implementation. Native/phase, row/recursive, geometry, precision, +global ownership and analytic obligations retain their separate scope. + +## Complete costs + +The universal proof in [PROOF.md](PROOF.md) includes both source passes, +protected staging, guided rewinds, both output writes, head restoration and +literal erasure. With public length V, initially occupied work D and fixed +work/context inventory Q, time is **O(V+D+Q)**. The two used current work +bodies occupy **2V+3+O(1)** raw cells; historical visited backing remains their +coordinatewise maximum and is never treated as deleted. + +Matching coordinate meanings and widths, a common grid, distinct physical +ports, all supplied heads at current origins, and contiguous initially dirty +work prefixes remain explicit entry premises. Corresponding component widths +may vary along a field. No complete old numerical allowance, complete supplier +invoice, full multiplication improvement or unconditional theorem is claimed. + +## Executed finite evidence + +The direct permutation/sign oracle checks **2,728** physical cases: every +signed x,y pair at widths 1–5 for both operations, encoded as a complete +complex record with equal component pairs. It accepts 2,666 and rejects 62. +Another 96 wider/asymmetric/mixed-width fields reach width 129, with 70 accepts. +Thirty-two failure and boundary controls include most-negative first/last +components, minimum second operands, signed equal values on distinct tapes, +shape/alias/source failures, four transition mutants, physical ordered inverse, +dirty extra work, protected contexts, and shrinking retained backing. + +Two real unchanged-controller fixtures use all **13,444 public fields**: + +- The entire 5,720-service right boundary, joining the retained scalar tables + and new swap table, executes 11,015,757 physical cell actions and 1,493,648 + table steps. A separate interpretation of the original boundary program + checks every public endpoint and spectator. +- The actual first 104-service signed block executes 216,813 physical actions + and 28,912 table steps, including most-negative second operands. + +These are actual contiguous source blocks entered at explicit assumed cuts; +they do not execute preceding native entries or the complete recursive caller. +The finite tests challenge the implementation, while the written proof gives +the universal quantifiers. Details and exact receipts are in +[VERIFICATION.md](VERIFICATION.md) and [RESULT.json](RESULT.json). + +## Reproduce + +From the repository root with Python 3.12 and its standard library: + +```sh +python3 -B scripts/research_package.py --package research/current-swap-flat-tables +``` + +`VERIFY.json` registers eight bounded commands: normal and optimized execution +of arithmetic, complete source binding, actual controller blocks and controls. +Each checks exact immutable input/dependency bytes and committed receipts. + +## Predecessors and attribution + +[#3098](https://github.com/CrocSwap/integer-mult-bounds/pull/3098), Jose Manuel +(`jmbarrancoml`), supplies the earlier aligned scalar-recipe execution. +[#969](https://github.com/CrocSwap/integer-mult-bounds/pull/969), prepared for +ToikY, defers historical scalar names and pays boundary copies, while explicitly +leaving physical arrays/current production admission open. +[#4516](https://github.com/CrocSwap/integer-mult-bounds/pull/4516) checks the +older caller's exact Laurent signs. Classical permutation and negation are +not new claims. Ali Romman's productive caller and #5356 continuation source, +DreamingOfClouds' selected #6030 word, the current lifecycle/compiler source, +and the frozen current scalar provider retain their credit and exact pins. + +## Open next questions + +The next obligations are the still-uncovered native/recursive provider tokens +and the actual all-success geometry, precision, ownership, full-cost and +analytic join. [TASK.json](TASK.json) records these questions and the exact +canonical task card. No independent human or proof-kernel acceptance is claimed. diff --git a/research/current-swap-flat-tables/RESULT.json b/research/current-swap-flat-tables/RESULT.json new file mode 100644 index 0000000000..db07288489 --- /dev/null +++ b/research/current-swap-flat-tables/RESULT.json @@ -0,0 +1,187 @@ +{ + "arithmetic": { + "check": "arithmetic", + "counts": { + "accepted": 2666, + "cases": 2728, + "physical_actions": 7648264, + "rejected": 62, + "table_steps": 1020267, + "wide_or_mixed_accepted": 70, + "wide_or_mixed_fields": 96 + }, + "tables": [ + { + "negated_input": null, + "operation": "SWAP", + "public_ports": 2, + "rows": 130, + "states": 57, + "table_sha256": "89d35b82f57512a2c060e58035165b0ce51b064abc926c557688a65ed12a4ac8", + "work_ports": 2 + }, + { + "negated_input": 0, + "operation": "SIGNED_SWAP", + "public_ports": 2, + "rows": 171, + "states": 74, + "table_sha256": "888211fd1e0a9e326d4ce10be232d6ea580f7ab8bc35ef9511fcfbfb60b7746f", + "work_ports": 2 + } + ] + }, + "binding": { + "caller_events": 642410, + "check": "binding", + "combined_arithmetic_services": 377762, + "counts": { + "SIGNED_SWAP": 4992, + "SWAP": 5928 + }, + "excluded_services": { + "caller-local": 124308, + "central-square": 3328, + "idle-in": 3120, + "idle-out": 3120, + "local-entry": 13860, + "local-return": 13860, + "query-in": 1560, + "query-out": 1560, + "raw-whole-job-enter": 13444, + "raw-whole-job-return": 13444 + }, + "raw_paid": { + "1": 41502, + "2": 8226, + "3": 8928, + "4": 1800, + "5": 2934, + "6": 198, + "7": 108, + "8": 18, + "16": 416, + "24": 416, + "32": 416, + "40": 416, + "48": 416, + "56": 416, + "64": 416, + "72": 208 + }, + "retained_scalar_services": 366842, + "scopes": { + "boundary-left": 3120, + "boundary-right": 2808, + "outer": 4992 + }, + "source_receipt_sha256": "227bb8c99d4bbf68c664a5b86f471676601e3605ac532286a39e037ddb26c4ce", + "swap_services": 10920, + "tables": [ + { + "negated_input": 0, + "operation": "SIGNED_SWAP", + "public_ports": 2, + "rows": 171, + "states": 74, + "table_sha256": "888211fd1e0a9e326d4ce10be232d6ea580f7ab8bc35ef9511fcfbfb60b7746f", + "work_ports": 2 + }, + { + "negated_input": null, + "operation": "SWAP", + "public_ports": 2, + "rows": 130, + "states": 57, + "table_sha256": "89d35b82f57512a2c060e58035165b0ce51b064abc926c557688a65ed12a4ac8", + "work_ports": 2 + } + ] + }, + "controller": { + "check": "controller_blocks", + "first_signed_block": { + "body_receipt_format": "increasing field index: u64be index, u64be raw length, raw symbol bytes", + "component_width": 4, + "field_count": 13444, + "first_event": 50517, + "input_body_sha256": "cda59a1b9f4f96fa5c5e9f351fccb6d50abca6a41974093efe94a8c6d97abce6", + "last_event": 50620, + "output_body_sha256": "ff104c226540dac3b8035fbf50742d3103aec95f2bb05bb4409e800cdae1e1d5", + "output_sha256": "913b7453f2bf11e916ce7206388d63e69a629b6d5fcee17be9f181d06538c2c7", + "physical_actions": 216813, + "program_sha256": "653d021b8d987955dfc6243e8ed8344b8c50a8557ca66ec4754a81f52fa479d4", + "service_table_sha256s": [ + "888211fd1e0a9e326d4ce10be232d6ea580f7ab8bc35ef9511fcfbfb60b7746f" + ], + "services": 104, + "source_site": 2, + "table_steps": 28912 + }, + "right_boundary": { + "body_receipt_format": "increasing field index: u64be index, u64be raw length, raw symbol bytes", + "component_width": 4, + "field_count": 13444, + "first_event": 13444, + "input_body_sha256": "c3c13203b9b55df70cf58fc41ecaaa9e49a3a54511dfcd97597de8725f137c0b", + "last_event": 19163, + "maximum_absolute_fixture_value": 6, + "output_body_sha256": "030222ccdfa0efb4edef0ef075519587ee48defccf49c78bbddc43b64a978f4d", + "output_sha256": "3008de423ad8303df7382e2a6c2c9184813834682bcbf9c1081ebd6e16b0e996", + "physical_actions": 11015757, + "program_sha256": "b8c956fcc43e3ad60db14f38f1ad7f083b1f1de9c56620940dbcdbc6b4792655", + "service_table_sha256s": [ + "0246c68e796a6c570132b52729b144c04980849ce275f46a491cd8c4c27c59f0", + "3570a65c5c361567128ab3798007f1d49e82e7a72627c747be1eeeba6d653330", + "59d32519f754763c3a406cf5999d3518dfc672f945944a495b10a47e258d11ff", + "89d35b82f57512a2c060e58035165b0ce51b064abc926c557688a65ed12a4ac8" + ], + "services": 5720, + "table_steps": 1493648 + } + }, + "controls": { + "check": "controls", + "controls": [ + "first_component_most_negative", + "last_component_most_negative", + "width_one_swap", + "width_one_signed_zero", + "minimum_second_operand_allowed", + "equal_values_distinct_ports", + "matched_heterogeneous_widths", + "empty_fields", + "empty_components", + "missing_delimiters", + "odd_component_count", + "partial_physical_code", + "unequal_widths", + "unequal_record_counts", + "logical_owner_alias", + "physical_tape_alias", + "reversed_source_port_order", + "changed_source_opcode", + "wrong_source_site", + "malformed_wrapper", + "unsupported_operation", + "corrupt_sources", + "corrupt_dependencies", + "omitted_negation", + "wrong_output_order", + "omitted_overflow_guard", + "early_public_write", + "ordered_inverse_restores", + "dirty_work_extra_inventory_and_context", + "omitted_physical_retirement", + "shrinking_call_retained_backing", + "explicit_rejection_cleanup_boundary" + ], + "count": 32, + "retained_highwater": [ + 12713, + 12728 + ], + "small_fresh_actions": 1685, + "small_fresh_table_steps": 226 + } +} diff --git a/research/current-swap-flat-tables/SOURCES.json b/research/current-swap-flat-tables/SOURCES.json new file mode 100644 index 0000000000..23e4253344 --- /dev/null +++ b/research/current-swap-flat-tables/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "research/p104-helper470-twin-rung-removal/WORD.json.gz", + "usage": "input", + "git_blob": "22f9ab02d1b73ea0aa4b07ce445a14cc2602c760", + "sha256": "7834725d9e34ee846a9ccc615221ea81e0201613938afa185d2eda0c9a6c232f" + }, + { + "path": "research/p104-productive-controller/CONTROLLER.json", + "usage": "input", + "git_blob": "cc539db709cf7a6c42872c4380902736ad453af3", + "sha256": "a84f6bbd547379597464e56c420cc665f96bc43a9a1351eed4b7cd0fce3cc4b9" + }, + { + "path": "research/p104-productive-controller/caller.py", + "usage": "provenance", + "git_blob": "6ac5e735691555ecafe2afbcff71edd923178113", + "sha256": "300d40043953e4f6aecfde8f2d1004b8ad6dc5a79ec3c7666c9908c2466c91c8" + } + ] +} diff --git a/research/current-swap-flat-tables/TASK.json b/research/current-swap-flat-tables/TASK.json new file mode 100644 index 0000000000..0480065c2c --- /dev/null +++ b/research/current-swap-flat-tables/TASK.json @@ -0,0 +1,87 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Choose one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "native_all_columns", + "owned_erasure", + "compiler", + "precision_tape", + "analytic_recovery" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "refined", + "scope_change_reason": "Lead-assigned wave-2 refinement: close the remaining original SWAP/SIGNED_SWAP arithmetic SERVICE class after the frozen current ADD/SCALE tables, excluding all native and recursive providers.", + "actual_scope": "Prove and execute exact ordered SWAP/SIGNED_SWAP tables for all matched complete coded field shapes, with whole-pair validation before public writes, exact signed admission, the unchanged two-work inventory, complete costs and all 10920 current source bindings.", + "bottleneck_link": "Completes the original two-output arithmetic table premise and composes it with the frozen ADD/SCALE provider at 377762 exact source SERVICE occurrences; caller/native/recursive/analytic premises remain.", + "stop_rule": "Finish this two-output source class and independently verify it. Do not enter Gaussian/MOVE, whole-caller precision or new kappa work.", + "evidence": "PROOF.md and RESULT.json; exact permutation/sign oracle, full source census, two actual contiguous unchanged-controller blocks, negative controls and normal/optimized replay.", + "author": "@CubeJerry", + "ai_assistance": "Substantial OpenAI assistance in source analysis, mathematics, implementation and verification. Separate AI review is not independent human or proof-kernel acceptance.", + "outcome": "completed", + "open_questions": [ + { + "question": "Join the current native phase, Gaussian and recursive services to the same coded registry.", + "why_it_matters": "Original scalar arithmetic is only one part of the typed compiler provider closure.", + "first_step": "Bind the exact still-uncovered source service token, coordinate shape and complete numerical/error/cost contract.", + "blocked_by": "Native provider and recursive precision/ownership obligations remain." + }, + { + "question": "Prove the all-success actual caller geometry, precision and complete-cost join.", + "why_it_matters": "Universal primitive success domains do not prove that each native/recursive return enters them.", + "first_step": "Use exact current chronology and provider endpoints to establish every common-shape, grid and signed-range predicate; retain all caller inventories and positive work.", + "blocked_by": "Native/recursive return contracts, full lifecycle and analytic recovery." + } + ] +} diff --git a/research/current-swap-flat-tables/VERIFICATION.md b/research/current-swap-flat-tables/VERIFICATION.md new file mode 100644 index 0000000000..da0d26c989 --- /dev/null +++ b/research/current-swap-flat-tables/VERIFICATION.md @@ -0,0 +1,122 @@ +# Verification record and scope + +Prepared for **@CubeJerry**, with substantial OpenAI assistance. No new κ. + +## Proof versus finite evidence + +`PROOF.md` establishes the all-width, all-record-count signed admission, +protected pair construction, complete tape costs and source-substitution +implication. The deterministic tests below use the unchanged physical table +executor and a direct permutation/sign oracle that contains no negation carry +recurrence. They are bounded challenges to implementation, not universal +proofs or a complete supplier admission. + +`DEPENDENCIES.json` authenticates each retained executable/fixture/reference +file by Git blob and SHA256 before import. The current original caller source +is reference-only. `SOURCES.json` binds the two live canonical input files, +task card, selected record and exact original semantic source. Dependencies +from the preceding scalar package are frozen at its published commit; its +table builder, scalar services and source wrappers are unchanged. + +## Executed suites + +| Suite | Domain and method | Exact result | +| --- | --- | --- | +| `arithmetic` | SWAP/SIGNED_SWAP, w=1..5, every signed x,y pair, duplicated into the two components of a complete complex record | 2,728 cases; 2,666 accepts, 62 rejects | +| `arithmetic` | 96 asymmetric/wide/mixed-width complete fields, widths up to 129; deterministic seed 6030 | 70 accepts; complete signed/shape/control-cost checks | +| `binding` | Complete original 642,410-event current lowerer output, with retained ADD/SCALE classifier | 10,920 new two-output bindings; 377,762 combined original arithmetic services | +| `controller` | Original complete right boundary at emitted indices 13444..19163, 5,720 services, all 13,444 public fields | 11,015,757 physical cell actions; 1,493,648 table steps; every endpoint/spectator checked | +| `controller` | Original first SIGNED_SWAP block, source outer site 2, emitted indices 50517..50620 | 104 services, all 13,444 public fields; 216,813 physical actions and 28,912 steps | +| `controls` | 32 mathematical, source, format, ownership and lifecycle boundary/failure cases | All controls passed | + +The full right-boundary comparison interprets original `CONTROLLER.json` +instructions independently of lowered tokens, then compares every complete +field. The signed block includes most-negative second operands. Both fixtures +start with explicit complete numerical fields at their assumed entry cuts; +preceding native entries, later native services and recursion are not run. +Both block receipts include the exact compiled instruction digest, the +executed service-table digests, and input/output digests of **every physical +public body**. The body encoding records increasing field index, its raw +length and its actual symbol bytes, with unsigned 64-bit big-endian index and +length prefixes. These are block-entry/block-exit receipts, not a claim that +the omitted native prefixes produced those entries. + +The observer `CountedTable` adds one counter increment per original row fetch +and returns that exact emitted row. It does not inspect payloads or decide +transitions. Physical actions are counted by the retained tape fixture. The +runtime remains the original `execute_table` and `Controller.primitive`; no +host numerical function implements a SERVICE. + +All per-case success checks include exact output pairs, full component shapes, +public extents, all head origins, ancestor sentinels, physical work erasure, +the explicit physical-plus-control ceiling, and coordinatewise retained +backing. Arithmetic failure checks require zero writes to **both** public +fields, not only equal values afterward. + +## Controls and failure detection + +The current signed guard is tested at the first and last components, width +one, the most-negative second operand, equal signed values on distinct ports +and heterogeneous matching widths. Input controls reject empty fields, empty +components, missing delimiters, odd component counts, partial physical codes, +unequal widths and unequal record counts before any public write. + +Source controls reject duplicate owner labels, actual repeated physical tape +objects, reversed unremapped operand order, changed opcode, wrong source site, +malformed remap wrappers, unsupported operations and corrupted input/dependency +bytes. The positive nested product test separates the active operation from +the original issuing PAID token. + +Four independent injected code defects are detected by the same exact oracle: +omitted negation, reversed output order, omitted final overflow guard, and an +early public write before whole-field validation. The last is caught on a late +component overflow even when earlier components were valid. + +A literal second call with reversed ordered physical ports restores both +original signed-swap inputs, including a most-negative second operand. Other +controls check arbitrary binary dirt on used and extra work, a protected +read-only descriptor, missing raw retirement, and a shrinking call on retained +erased backing. Fresh and warm small calls have exactly the same 1,685 physical +actions and 226 table steps, while retaining the larger historical high-water +coordinates 12,713 and 12,728. + +An explicit rejection control confirms the stated cleanup boundary: a late +failure preserves both public contents while leaving advanced heads and +occupied work. No exception-safe physical rollback has been added or claimed. + +## Independent mathematical review + +A separate lead AI reviewer inspected the written proof, emitted-table +construction and exact original `caller.py` ordered semantics. The reviewer +independently checked the digit identity, the most-negative iff guard, the +staged read-before-two-writes induction, the signed inverse on reversed ports, +and the complete cost/lifecycle premises, finding no issue under the stated +aligned, distinct-port and contiguous-work hypotheses. + +Its separate direct integer enumeration at widths 1–12 checked all 8,190 +first inputs, with 8,178 admitted, verifying the signed endpoint and exact +rejection condition without importing table code. This is a separate +mathematical audit reported during the research session. It is not another +physical executor run, an independent human review or formal proof-kernel +acceptance, and the registered commands do not claim to replay that external +audit. + +## Reproduction and review gates + +```sh +python3 -B scripts/research_package.py --package research/current-swap-flat-tables +``` + +The manifest registers normal and optimized execution of all four suites, +each with a 120-second limit. Each command compares its complete deterministic +result with `RESULT.json`. No check depends on `assert`; missing receipts fail +rather than generating a replacement. All code is Python 3.12 standard library. +All eight final registered commands passed with identical exact receipts; +[registered-replay.log](evidence/registered-replay.log) records their markers +and the final `PASS_REGISTERED_RESEARCH_PACKAGE` result. + +The package retains exact source/commit pins and the actual canonical task +card. Committed-byte/mode and portable-export gates remain distinct from the +mathematical checks. No independent human or formal proof-kernel admission is +claimed. All selected framework assumptions remain beyond this explicitly +scoped scalar-source implication. diff --git a/research/current-swap-flat-tables/VERIFY.json b/research/current-swap-flat-tables/VERIFY.json new file mode 100644 index 0000000000..0505860a7b --- /dev/null +++ b/research/current-swap-flat-tables/VERIFY.json @@ -0,0 +1,108 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p104-helper470-twin-rung-removal/WORD.json.gz", + "research/p104-productive-controller/CONTROLLER.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "research/current-swap-flat-tables/verify.py", + "--suite", + "arithmetic" + ], + "timeout_seconds": 120, + "checks": "Normal arithmetic two-output source/physical/control-cost validation with exact receipts and declared scope." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "research/current-swap-flat-tables/verify.py", + "--suite", + "binding" + ], + "timeout_seconds": 120, + "checks": "Normal binding two-output source/physical/control-cost validation with exact receipts and declared scope." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "research/current-swap-flat-tables/verify.py", + "--suite", + "controller" + ], + "timeout_seconds": 120, + "checks": "Normal controller two-output source/physical/control-cost validation with exact receipts and declared scope." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "research/current-swap-flat-tables/check_controls.py" + ], + "timeout_seconds": 120, + "checks": "Normal controls two-output source/physical/control-cost validation with exact receipts and declared scope." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "research/current-swap-flat-tables/verify.py", + "--suite", + "arithmetic" + ], + "timeout_seconds": 120, + "checks": "Optimized arithmetic two-output source/physical/control-cost validation with exact receipts and declared scope." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "research/current-swap-flat-tables/verify.py", + "--suite", + "binding" + ], + "timeout_seconds": 120, + "checks": "Optimized binding two-output source/physical/control-cost validation with exact receipts and declared scope." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "research/current-swap-flat-tables/verify.py", + "--suite", + "controller" + ], + "timeout_seconds": 120, + "checks": "Optimized controller two-output source/physical/control-cost validation with exact receipts and declared scope." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "research/current-swap-flat-tables/check_controls.py" + ], + "timeout_seconds": 120, + "checks": "Optimized controls two-output source/physical/control-cost validation with exact receipts and declared scope." + } + ] +} diff --git a/research/current-swap-flat-tables/check_controls.py b/research/current-swap-flat-tables/check_controls.py new file mode 100644 index 0000000000..b36a3afe33 --- /dev/null +++ b/research/current-swap-flat-tables/check_controls.py @@ -0,0 +1,129 @@ +"""Failure controls and boundary cases for current two-output services. + +Prepared for @CubeJerry with substantial OpenAI assistance. Apache-2.0. +""" +from pathlib import Path +import json +import sys +import types + +sys.path.insert(0,str(Path(__file__).resolve().parent)) +from physical import A,IR,ROOT,Tape,encode_symbols +from source_binding import check_inputs,check_payload +from tables import compile_swap,source_literal,need +from fixtures import check_case,execute,encode_field,decode_field + + +def reject(call,fragment): + try:call() + except ValueError as exc: + need(fragment in str(exc),'named failure: '+str(exc));return + raise ValueError('negative control accepted: '+fragment) + + +def raw_failure(table,left,right,fragment): + public=[Tape(left,origin=17),Tape(right,origin=29)] + before=[t.body() for t in public];work=[Tape(origin=41),Tape(origin=53)] + reject(lambda:A.execute_table(table,tuple(public+work)),fragment) + need(all(t.writes==0 and t.body()==old for t,old in zip(public,before)), + 'malformed input rejection before public writes') + + +def main(): + check_inputs();done=[] + def record(name):done.append(name) + swap,_=compile_swap('SWAP');signed,_=compile_swap('SIGNED_SWAP') + for values,name in [((-8,0),'first_component_most_negative'),((0,-8),'last_component_most_negative')]: + allowed,result=check_case(signed,'SIGNED_SWAP',values,(2,3),(4,4)) + need(not allowed and 'overflow' in result['error'],'ordered first-operand signed guard') + record(name) + for op,table,xs,ys,widths,name in [ + ('SWAP',swap,(-1,0),(0,-1),(1,1),'width_one_swap'), + ('SIGNED_SWAP',signed,(0,0),(-1,-1),(1,1),'width_one_signed_zero'), + ('SIGNED_SWAP',signed,(1,-7),(-8,-8),(4,4),'minimum_second_operand_allowed'), + ('SIGNED_SWAP',signed,(-3,-3),(-3,-3),(4,4),'equal_values_distinct_ports'), + ('SIGNED_SWAP',signed,(0,-7,-1,-255),(-1,7,1,255),(1,4,2,9),'matched_heterogeneous_widths')]: + allowed,_=check_case(table,op,xs,ys,widths);need(allowed,'boundary positive control');record(name) + for left,right,fragment,name in [ + ((),(),'nonempty complex','empty_fields'), + (encode_symbols((2,)),encode_symbols((2,)),'positive component','empty_components'), + (encode_symbols((0,)),encode_symbols((0,)),'unterminated','missing_delimiters'), + (encode_symbols((0,2)),encode_symbols((0,2)),'nonempty complex','odd_component_count'), + ((0,1),(0,1),'codeword','partial_physical_code'), + (encode_field((0,0),(2,2)),encode_field((0,0),(1,1)),'component shape','unequal_widths'), + (encode_field((0,0),(2,2)),encode_field((0,0,0,0),(2,2,2,2)),'field frontier','unequal_record_counts')]: + raw_failure(swap,left,right,fragment);record(name) + caller=json.loads((ROOT.parents[1]/'research/p104-productive-controller/CONTROLLER.json').read_text()) + site=next(i for i,r in enumerate(caller['physical_events']) if r[0]=='SIGNED_SWAP') + raw=tuple(caller['physical_events'][site]);fields=(raw[1]*104,raw[2]*104) + event=IR.Event('SERVICE',fields,('outer',site,0,raw)) + need(source_literal(event,caller)[0]=='SIGNED_SWAP','actual signed source') + reject(lambda:source_literal(IR.Event('SERVICE',(fields[0],fields[0]),event.token),caller),'distinct ordered') + record('logical_owner_alias') + t=Tape();admin=[Tape(origin=101+10*i,marker=A.BASE) for i in range(4)] + reject(lambda:A.Controller((),2,(t,t),*admin,rows=None,services={},stack_class=object),'all physical ports distinct') + record('physical_tape_alias') + reject(lambda:source_literal(IR.Event('SERVICE',fields[::-1],event.token),caller),'ordered field binding') + record('reversed_source_port_order') + changed=('SWAP',)+raw[1:] + reject(lambda:source_literal(IR.Event('SERVICE',fields,('outer',site,0,changed)),caller),'exact outer') + record('changed_source_opcode') + reject(lambda:source_literal(IR.Event('SERVICE',fields,('outer',site+1,0,raw)),caller),'exact outer') + record('wrong_source_site') + reject(lambda:source_literal(IR.Event('SERVICE',fields,('unit-fragment',event.token,event.token)),caller),'wrapper grammar') + record('malformed_wrapper') + reject(lambda:compile_swap('ADD'),'two-output source operation');record('unsupported_operation') + for manifest,key,base in [('SOURCES.json','path',ROOT.parents[1]),('DEPENDENCIES.json','local_path',ROOT)]: + rows=json.loads((ROOT/manifest).read_text())['files'] + row=next(r for r in rows if manifest=='DEPENDENCIES.json' or r['usage']=='input') + data=(base/row[key]).read_bytes() + reject(lambda:check_payload(data+b'\n',row,row[key]),'source byte pin') + record('corrupt_'+manifest.split('.')[0].lower()) + source=(ROOT/'tables.py').read_text() + mutants=[ + ('omitted_negation',"negate = op == 'SIGNED_SWAP'",'negate = False','SIGNED_SWAP',(1,1),(2,2),'permutation/sign endpoint'), + ('wrong_output_order',"b.emit('write',0,y);b.emit('write',1,z)","b.emit('write',0,z);b.emit('write',1,y)",'SWAP',(1,1),(2,2),'permutation/sign endpoint'), + ('omitted_overflow_guard','failure = negate and sx==1 and sz==1','failure = False','SIGNED_SWAP',(0,-8),(2,3),'signed admission iff'), + ('early_public_write',"b.emit('write',2,z);b.emit('move',2,1)","b.emit('write',0,z);b.emit('write',2,z);b.emit('move',2,1)",'SIGNED_SWAP',(1,-8),(2,3),'rejection before either public write')] + for name,old,new,op,xs,ys,fragment in mutants: + need(source.count(old)==1,'unique controlled mutation') + module=types.ModuleType('swap_mutant_'+name) + exec(compile(source.replace(old,new),name,'exec'),module.__dict__) + table,_=module.compile_swap(op) + reject(lambda:check_case(table,op,xs,ys,(4,4)),fragment);record(name) + # A literal inverse uses the same signed table with reversed ordered ports. + original=((-7,3),(-8,7));result=execute(signed,*original,(4,4)) + need(result['error'] is None,'signed inverse first admission') + public,work=result['public'],result['work'] + for t in work:A.retire(t) + A.execute_table(signed,(public[1],public[0],*work)) + for t in work:A.retire(t) + need(tuple(decode_field(t.body())[0] for t in public)==original,'literal ordered inverse restores both sources') + record('ordered_inverse_restores') + # All extra work is retired; the descriptor is untouched at its origin. + work=[Tape((1,0)*10+(1,),origin=41),Tape((0,1)*7+(0,),origin=53),Tape((1,)*9,origin=67)] + context=Tape((0,1)*33,origin=79,readonly=True);before=context.body() + allowed,result=check_case(signed,'SIGNED_SWAP',(3,-7),(-8,7),(4,4),work=work,contexts=(context,)) + need(allowed and context.body()==before and context.writes==0,'complete dirty-work and protected-context contract') + record('dirty_work_extra_inventory_and_context') + # The unchanged table executor alone does not erase encoded work. + public=[Tape(encode_field(v,(4,4)),origin=17+12*i) for i,v in enumerate(((2,-2),(3,-3)))] + work=[Tape(origin=41),Tape(origin=53)];A.execute_table(swap,tuple(public+work)) + need(any(not t.blank() for t in work),'omitted retirement detected');record('omitted_physical_retirement') + warm=execute(swap,(1,-1)*64,(2,-2)*64,(32,)*128)['work'];old_backing=[t.highwater for t in warm] + _,small=check_case(signed,'SIGNED_SWAP',(0,-1),(-4,3),(3,3),work=warm) + _,fresh=check_case(signed,'SIGNED_SWAP',(0,-1),(-4,3),(3,3)) + need((small['actions'],small['steps'])==(fresh['actions'],fresh['steps']) + and [t.highwater for t in warm]==old_backing,'current-volume warm reuse without historical rescan') + record('shrinking_call_retained_backing') + result=execute(signed,(1,-8),(2,3),(4,4)) + need(result['error'] and any(t.pos!=t.origin for t in result['public']+result['work']) + and any(not t.blank() for t in result['work']),'immediate reject has no physical rollback') + record('explicit_rejection_cleanup_boundary') + result=dict(check='controls',count=len(done),controls=done,small_fresh_actions=fresh['actions'], + small_fresh_table_steps=fresh['steps'],retained_highwater=old_backing) + need(result==json.loads((ROOT/'RESULT.json').read_text())['controls'],'committed exact control receipt') + print(json.dumps(result,sort_keys=True));print('PASS_CURRENT_SWAP_FLAT_TABLES_CONTROLS') + + +if __name__=='__main__':main() diff --git a/research/current-swap-flat-tables/evidence/initial-arithmetic.log b/research/current-swap-flat-tables/evidence/initial-arithmetic.log new file mode 100644 index 0000000000..1e6c98250b --- /dev/null +++ b/research/current-swap-flat-tables/evidence/initial-arithmetic.log @@ -0,0 +1,2 @@ +{"check": "arithmetic", "counts": {"accepted": 2666, "cases": 2728, "physical_actions": 7648264, "rejected": 62, "table_steps": 1020267, "wide_or_mixed_accepted": 70, "wide_or_mixed_fields": 96}, "tables": [{"negated_input": null, "operation": "SWAP", "public_ports": 2, "rows": 130, "states": 57, "table_sha256": "89d35b82f57512a2c060e58035165b0ce51b064abc926c557688a65ed12a4ac8", "work_ports": 2}, {"negated_input": 0, "operation": "SIGNED_SWAP", "public_ports": 2, "rows": 171, "states": 74, "table_sha256": "888211fd1e0a9e326d4ce10be232d6ea580f7ab8bc35ef9511fcfbfb60b7746f", "work_ports": 2}]} +PASS_CURRENT_SWAP_FLAT_TABLES_ARITHMETIC diff --git a/research/current-swap-flat-tables/evidence/initial-binding.log b/research/current-swap-flat-tables/evidence/initial-binding.log new file mode 100644 index 0000000000..d5a3e9dc02 --- /dev/null +++ b/research/current-swap-flat-tables/evidence/initial-binding.log @@ -0,0 +1,2 @@ +{"caller_events": 642410, "check": "binding", "combined_arithmetic_services": 377762, "counts": {"SIGNED_SWAP": 4992, "SWAP": 5928}, "excluded_services": {"caller-local": 124308, "central-square": 3328, "idle-in": 3120, "idle-out": 3120, "local-entry": 13860, "local-return": 13860, "query-in": 1560, "query-out": 1560, "raw-whole-job-enter": 13444, "raw-whole-job-return": 13444}, "raw_paid": {"1": 41502, "2": 8226, "3": 8928, "4": 1800, "5": 2934, "6": 198, "7": 108, "8": 18, "16": 416, "24": 416, "32": 416, "40": 416, "48": 416, "56": 416, "64": 416, "72": 208}, "retained_scalar_services": 366842, "scopes": {"boundary-left": 3120, "boundary-right": 2808, "outer": 4992}, "source_receipt_sha256": "227bb8c99d4bbf68c664a5b86f471676601e3605ac532286a39e037ddb26c4ce", "swap_services": 10920, "tables": [{"negated_input": 0, "operation": "SIGNED_SWAP", "public_ports": 2, "rows": 171, "states": 74, "table_sha256": "888211fd1e0a9e326d4ce10be232d6ea580f7ab8bc35ef9511fcfbfb60b7746f", "work_ports": 2}, {"negated_input": null, "operation": "SWAP", "public_ports": 2, "rows": 130, "states": 57, "table_sha256": "89d35b82f57512a2c060e58035165b0ce51b064abc926c557688a65ed12a4ac8", "work_ports": 2}]} +PASS_CURRENT_SWAP_FLAT_TABLES_BINDING diff --git a/research/current-swap-flat-tables/evidence/initial-controller.log b/research/current-swap-flat-tables/evidence/initial-controller.log new file mode 100644 index 0000000000..bf1863cadf --- /dev/null +++ b/research/current-swap-flat-tables/evidence/initial-controller.log @@ -0,0 +1,2 @@ +{"check": "controller_blocks", "first_signed_block": {"body_receipt_format": "increasing field index: u64be index, u64be raw length, raw symbol bytes", "component_width": 4, "field_count": 13444, "first_event": 50517, "input_body_sha256": "cda59a1b9f4f96fa5c5e9f351fccb6d50abca6a41974093efe94a8c6d97abce6", "last_event": 50620, "output_body_sha256": "ff104c226540dac3b8035fbf50742d3103aec95f2bb05bb4409e800cdae1e1d5", "output_sha256": "913b7453f2bf11e916ce7206388d63e69a629b6d5fcee17be9f181d06538c2c7", "physical_actions": 216813, "program_sha256": "653d021b8d987955dfc6243e8ed8344b8c50a8557ca66ec4754a81f52fa479d4", "service_table_sha256s": ["888211fd1e0a9e326d4ce10be232d6ea580f7ab8bc35ef9511fcfbfb60b7746f"], "services": 104, "source_site": 2, "table_steps": 28912}, "right_boundary": {"body_receipt_format": "increasing field index: u64be index, u64be raw length, raw symbol bytes", "component_width": 4, "field_count": 13444, "first_event": 13444, "input_body_sha256": "c3c13203b9b55df70cf58fc41ecaaa9e49a3a54511dfcd97597de8725f137c0b", "last_event": 19163, "maximum_absolute_fixture_value": 6, "output_body_sha256": "030222ccdfa0efb4edef0ef075519587ee48defccf49c78bbddc43b64a978f4d", "output_sha256": "3008de423ad8303df7382e2a6c2c9184813834682bcbf9c1081ebd6e16b0e996", "physical_actions": 11015757, "program_sha256": "b8c956fcc43e3ad60db14f38f1ad7f083b1f1de9c56620940dbcdbc6b4792655", "service_table_sha256s": ["0246c68e796a6c570132b52729b144c04980849ce275f46a491cd8c4c27c59f0", "3570a65c5c361567128ab3798007f1d49e82e7a72627c747be1eeeba6d653330", "59d32519f754763c3a406cf5999d3518dfc672f945944a495b10a47e258d11ff", "89d35b82f57512a2c060e58035165b0ce51b064abc926c557688a65ed12a4ac8"], "services": 5720, "table_steps": 1493648}} +PASS_CURRENT_SWAP_FLAT_TABLES_CONTROLLER diff --git a/research/current-swap-flat-tables/evidence/initial-controls.log b/research/current-swap-flat-tables/evidence/initial-controls.log new file mode 100644 index 0000000000..d377f163c2 --- /dev/null +++ b/research/current-swap-flat-tables/evidence/initial-controls.log @@ -0,0 +1,2 @@ +{"check": "controls", "controls": ["first_component_most_negative", "last_component_most_negative", "width_one_swap", "width_one_signed_zero", "minimum_second_operand_allowed", "equal_values_distinct_ports", "matched_heterogeneous_widths", "empty_fields", "empty_components", "missing_delimiters", "odd_component_count", "partial_physical_code", "unequal_widths", "unequal_record_counts", "logical_owner_alias", "physical_tape_alias", "reversed_source_port_order", "changed_source_opcode", "wrong_source_site", "malformed_wrapper", "unsupported_operation", "corrupt_sources", "corrupt_dependencies", "omitted_negation", "wrong_output_order", "omitted_overflow_guard", "early_public_write", "ordered_inverse_restores", "dirty_work_extra_inventory_and_context", "omitted_physical_retirement", "shrinking_call_retained_backing", "explicit_rejection_cleanup_boundary"], "count": 32, "retained_highwater": [12713, 12728], "small_fresh_actions": 1685, "small_fresh_table_steps": 226} +PASS_CURRENT_SWAP_FLAT_TABLES_CONTROLS diff --git a/research/current-swap-flat-tables/evidence/registered-replay.log b/research/current-swap-flat-tables/evidence/registered-replay.log new file mode 100644 index 0000000000..b4a9ec92ba --- /dev/null +++ b/research/current-swap-flat-tables/evidence/registered-replay.log @@ -0,0 +1,25 @@ +CHECK Normal arithmetic two-output source/physical/control-cost validation with exact receipts and declared scope. +{"check": "arithmetic", "counts": {"accepted": 2666, "cases": 2728, "physical_actions": 7648264, "rejected": 62, "table_steps": 1020267, "wide_or_mixed_accepted": 70, "wide_or_mixed_fields": 96}, "tables": [{"negated_input": null, "operation": "SWAP", "public_ports": 2, "rows": 130, "states": 57, "table_sha256": "89d35b82f57512a2c060e58035165b0ce51b064abc926c557688a65ed12a4ac8", "work_ports": 2}, {"negated_input": 0, "operation": "SIGNED_SWAP", "public_ports": 2, "rows": 171, "states": 74, "table_sha256": "888211fd1e0a9e326d4ce10be232d6ea580f7ab8bc35ef9511fcfbfb60b7746f", "work_ports": 2}]} +PASS_CURRENT_SWAP_FLAT_TABLES_ARITHMETIC +CHECK Normal binding two-output source/physical/control-cost validation with exact receipts and declared scope. +{"caller_events": 642410, "check": "binding", "combined_arithmetic_services": 377762, "counts": {"SIGNED_SWAP": 4992, "SWAP": 5928}, "excluded_services": {"caller-local": 124308, "central-square": 3328, "idle-in": 3120, "idle-out": 3120, "local-entry": 13860, "local-return": 13860, "query-in": 1560, "query-out": 1560, "raw-whole-job-enter": 13444, "raw-whole-job-return": 13444}, "raw_paid": {"1": 41502, "2": 8226, "3": 8928, "4": 1800, "5": 2934, "6": 198, "7": 108, "8": 18, "16": 416, "24": 416, "32": 416, "40": 416, "48": 416, "56": 416, "64": 416, "72": 208}, "retained_scalar_services": 366842, "scopes": {"boundary-left": 3120, "boundary-right": 2808, "outer": 4992}, "source_receipt_sha256": "227bb8c99d4bbf68c664a5b86f471676601e3605ac532286a39e037ddb26c4ce", "swap_services": 10920, "tables": [{"negated_input": 0, "operation": "SIGNED_SWAP", "public_ports": 2, "rows": 171, "states": 74, "table_sha256": "888211fd1e0a9e326d4ce10be232d6ea580f7ab8bc35ef9511fcfbfb60b7746f", "work_ports": 2}, {"negated_input": null, "operation": "SWAP", "public_ports": 2, "rows": 130, "states": 57, "table_sha256": "89d35b82f57512a2c060e58035165b0ce51b064abc926c557688a65ed12a4ac8", "work_ports": 2}]} +PASS_CURRENT_SWAP_FLAT_TABLES_BINDING +CHECK Normal controller two-output source/physical/control-cost validation with exact receipts and declared scope. +{"check": "controller_blocks", "first_signed_block": {"body_receipt_format": "increasing field index: u64be index, u64be raw length, raw symbol bytes", "component_width": 4, "field_count": 13444, "first_event": 50517, "input_body_sha256": "cda59a1b9f4f96fa5c5e9f351fccb6d50abca6a41974093efe94a8c6d97abce6", "last_event": 50620, "output_body_sha256": "ff104c226540dac3b8035fbf50742d3103aec95f2bb05bb4409e800cdae1e1d5", "output_sha256": "913b7453f2bf11e916ce7206388d63e69a629b6d5fcee17be9f181d06538c2c7", "physical_actions": 216813, "program_sha256": "653d021b8d987955dfc6243e8ed8344b8c50a8557ca66ec4754a81f52fa479d4", "service_table_sha256s": ["888211fd1e0a9e326d4ce10be232d6ea580f7ab8bc35ef9511fcfbfb60b7746f"], "services": 104, "source_site": 2, "table_steps": 28912}, "right_boundary": {"body_receipt_format": "increasing field index: u64be index, u64be raw length, raw symbol bytes", "component_width": 4, "field_count": 13444, "first_event": 13444, "input_body_sha256": "c3c13203b9b55df70cf58fc41ecaaa9e49a3a54511dfcd97597de8725f137c0b", "last_event": 19163, "maximum_absolute_fixture_value": 6, "output_body_sha256": "030222ccdfa0efb4edef0ef075519587ee48defccf49c78bbddc43b64a978f4d", "output_sha256": "3008de423ad8303df7382e2a6c2c9184813834682bcbf9c1081ebd6e16b0e996", "physical_actions": 11015757, "program_sha256": "b8c956fcc43e3ad60db14f38f1ad7f083b1f1de9c56620940dbcdbc6b4792655", "service_table_sha256s": ["0246c68e796a6c570132b52729b144c04980849ce275f46a491cd8c4c27c59f0", "3570a65c5c361567128ab3798007f1d49e82e7a72627c747be1eeeba6d653330", "59d32519f754763c3a406cf5999d3518dfc672f945944a495b10a47e258d11ff", "89d35b82f57512a2c060e58035165b0ce51b064abc926c557688a65ed12a4ac8"], "services": 5720, "table_steps": 1493648}} +PASS_CURRENT_SWAP_FLAT_TABLES_CONTROLLER +CHECK Normal controls two-output source/physical/control-cost validation with exact receipts and declared scope. +{"check": "controls", "controls": ["first_component_most_negative", "last_component_most_negative", "width_one_swap", "width_one_signed_zero", "minimum_second_operand_allowed", "equal_values_distinct_ports", "matched_heterogeneous_widths", "empty_fields", "empty_components", "missing_delimiters", "odd_component_count", "partial_physical_code", "unequal_widths", "unequal_record_counts", "logical_owner_alias", "physical_tape_alias", "reversed_source_port_order", "changed_source_opcode", "wrong_source_site", "malformed_wrapper", "unsupported_operation", "corrupt_sources", "corrupt_dependencies", "omitted_negation", "wrong_output_order", "omitted_overflow_guard", "early_public_write", "ordered_inverse_restores", "dirty_work_extra_inventory_and_context", "omitted_physical_retirement", "shrinking_call_retained_backing", "explicit_rejection_cleanup_boundary"], "count": 32, "retained_highwater": [12713, 12728], "small_fresh_actions": 1685, "small_fresh_table_steps": 226} +PASS_CURRENT_SWAP_FLAT_TABLES_CONTROLS +CHECK Optimized arithmetic two-output source/physical/control-cost validation with exact receipts and declared scope. +{"check": "arithmetic", "counts": {"accepted": 2666, "cases": 2728, "physical_actions": 7648264, "rejected": 62, "table_steps": 1020267, "wide_or_mixed_accepted": 70, "wide_or_mixed_fields": 96}, "tables": [{"negated_input": null, "operation": "SWAP", "public_ports": 2, "rows": 130, "states": 57, "table_sha256": "89d35b82f57512a2c060e58035165b0ce51b064abc926c557688a65ed12a4ac8", "work_ports": 2}, {"negated_input": 0, "operation": "SIGNED_SWAP", "public_ports": 2, "rows": 171, "states": 74, "table_sha256": "888211fd1e0a9e326d4ce10be232d6ea580f7ab8bc35ef9511fcfbfb60b7746f", "work_ports": 2}]} +PASS_CURRENT_SWAP_FLAT_TABLES_ARITHMETIC +CHECK Optimized binding two-output source/physical/control-cost validation with exact receipts and declared scope. +{"caller_events": 642410, "check": "binding", "combined_arithmetic_services": 377762, "counts": {"SIGNED_SWAP": 4992, "SWAP": 5928}, "excluded_services": {"caller-local": 124308, "central-square": 3328, "idle-in": 3120, "idle-out": 3120, "local-entry": 13860, "local-return": 13860, "query-in": 1560, "query-out": 1560, "raw-whole-job-enter": 13444, "raw-whole-job-return": 13444}, "raw_paid": {"1": 41502, "2": 8226, "3": 8928, "4": 1800, "5": 2934, "6": 198, "7": 108, "8": 18, "16": 416, "24": 416, "32": 416, "40": 416, "48": 416, "56": 416, "64": 416, "72": 208}, "retained_scalar_services": 366842, "scopes": {"boundary-left": 3120, "boundary-right": 2808, "outer": 4992}, "source_receipt_sha256": "227bb8c99d4bbf68c664a5b86f471676601e3605ac532286a39e037ddb26c4ce", "swap_services": 10920, "tables": [{"negated_input": 0, "operation": "SIGNED_SWAP", "public_ports": 2, "rows": 171, "states": 74, "table_sha256": "888211fd1e0a9e326d4ce10be232d6ea580f7ab8bc35ef9511fcfbfb60b7746f", "work_ports": 2}, {"negated_input": null, "operation": "SWAP", "public_ports": 2, "rows": 130, "states": 57, "table_sha256": "89d35b82f57512a2c060e58035165b0ce51b064abc926c557688a65ed12a4ac8", "work_ports": 2}]} +PASS_CURRENT_SWAP_FLAT_TABLES_BINDING +CHECK Optimized controller two-output source/physical/control-cost validation with exact receipts and declared scope. +{"check": "controller_blocks", "first_signed_block": {"body_receipt_format": "increasing field index: u64be index, u64be raw length, raw symbol bytes", "component_width": 4, "field_count": 13444, "first_event": 50517, "input_body_sha256": "cda59a1b9f4f96fa5c5e9f351fccb6d50abca6a41974093efe94a8c6d97abce6", "last_event": 50620, "output_body_sha256": "ff104c226540dac3b8035fbf50742d3103aec95f2bb05bb4409e800cdae1e1d5", "output_sha256": "913b7453f2bf11e916ce7206388d63e69a629b6d5fcee17be9f181d06538c2c7", "physical_actions": 216813, "program_sha256": "653d021b8d987955dfc6243e8ed8344b8c50a8557ca66ec4754a81f52fa479d4", "service_table_sha256s": ["888211fd1e0a9e326d4ce10be232d6ea580f7ab8bc35ef9511fcfbfb60b7746f"], "services": 104, "source_site": 2, "table_steps": 28912}, "right_boundary": {"body_receipt_format": "increasing field index: u64be index, u64be raw length, raw symbol bytes", "component_width": 4, "field_count": 13444, "first_event": 13444, "input_body_sha256": "c3c13203b9b55df70cf58fc41ecaaa9e49a3a54511dfcd97597de8725f137c0b", "last_event": 19163, "maximum_absolute_fixture_value": 6, "output_body_sha256": "030222ccdfa0efb4edef0ef075519587ee48defccf49c78bbddc43b64a978f4d", "output_sha256": "3008de423ad8303df7382e2a6c2c9184813834682bcbf9c1081ebd6e16b0e996", "physical_actions": 11015757, "program_sha256": "b8c956fcc43e3ad60db14f38f1ad7f083b1f1de9c56620940dbcdbc6b4792655", "service_table_sha256s": ["0246c68e796a6c570132b52729b144c04980849ce275f46a491cd8c4c27c59f0", "3570a65c5c361567128ab3798007f1d49e82e7a72627c747be1eeeba6d653330", "59d32519f754763c3a406cf5999d3518dfc672f945944a495b10a47e258d11ff", "89d35b82f57512a2c060e58035165b0ce51b064abc926c557688a65ed12a4ac8"], "services": 5720, "table_steps": 1493648}} +PASS_CURRENT_SWAP_FLAT_TABLES_CONTROLLER +CHECK Optimized controls two-output source/physical/control-cost validation with exact receipts and declared scope. +{"check": "controls", "controls": ["first_component_most_negative", "last_component_most_negative", "width_one_swap", "width_one_signed_zero", "minimum_second_operand_allowed", "equal_values_distinct_ports", "matched_heterogeneous_widths", "empty_fields", "empty_components", "missing_delimiters", "odd_component_count", "partial_physical_code", "unequal_widths", "unequal_record_counts", "logical_owner_alias", "physical_tape_alias", "reversed_source_port_order", "changed_source_opcode", "wrong_source_site", "malformed_wrapper", "unsupported_operation", "corrupt_sources", "corrupt_dependencies", "omitted_negation", "wrong_output_order", "omitted_overflow_guard", "early_public_write", "ordered_inverse_restores", "dirty_work_extra_inventory_and_context", "omitted_physical_retirement", "shrinking_call_retained_backing", "explicit_rejection_cleanup_boundary"], "count": 32, "retained_highwater": [12713, 12728], "small_fresh_actions": 1685, "small_fresh_table_steps": 226} +PASS_CURRENT_SWAP_FLAT_TABLES_CONTROLS +PASS_REGISTERED_RESEARCH_PACKAGE research/current-swap-flat-tables outcome=completed diff --git a/research/current-swap-flat-tables/fixtures.py b/research/current-swap-flat-tables/fixtures.py new file mode 100644 index 0000000000..41f531946b --- /dev/null +++ b/research/current-swap-flat-tables/fixtures.py @@ -0,0 +1,89 @@ +"""Observer-only physical fixtures and an independent permutation/sign oracle. + +Prepared for @CubeJerry with substantial OpenAI assistance. Apache-2.0. +""" +from physical import A,Tape,encode_symbols,symbols_for +from vendor.scalar_tables import need + + +class CountedTable: + """Count row fetches without changing the emitted finite table or ports.""" + def __init__(self,table):self.table,self.steps=table,0 + def __getitem__(self,index): + self.steps+=1 + return self.table[index] + + +def encode_field(values,widths): + need(len(values)==len(widths),'fixture component count') + return encode_symbols(tuple(s for value,width in zip(values,widths) + for s in symbols_for((value,),width))) + + +def decode_field(body): + need(len(body)%3==0,'whole coded fixture') + symbols=[4*body[i]+2*body[i+1]+body[i+2] for i in range(0,len(body),3)] + values,widths,bits=[],[],[] + for s in symbols: + if s==2: + need(bits,'positive decoded component') + values.append(sum(x<= self.origin) + + def sentinel_ok(self): + return self.cells[self.origin-1] == self.marker and self.cells[self.origin-2] == 91 + + +def encode_symbols(symbols): + return tuple((s>>k)&1 for s in symbols for k in (2,1,0)) + + +def symbols_for(values, width): + if width < 1: + raise ValueError('positive fixture width') + out = [] + for value in values: + if not -(1<<(width-1)) <= value < (1<<(width-1)): + raise ValueError('fixture value outside signed width') + out.extend((value>>j)&1 for j in range(width)) + out.append(2) + return tuple(out) + + +def decode_body(body, width): + if len(body)%3: + raise ValueError('partial physical codeword') + syms = [4*body[i]+2*body[i+1]+body[i+2] for i in range(0,len(body),3)] + block = width+1 + if len(syms)%block: + raise ValueError('partial fixture component') + values = [] + for i in range(0,len(syms),block): + bits = syms[i:i+width] + if any(x not in (0,1) for x in bits) or syms[i+width] != 2: + raise ValueError('corrupt numeric component') + value = sum(x<>1 + need(c in (0,1),'finite negation carry') + b.emit('write',2,z);b.emit('move',2,1) + guide_one();inputs_forward();b.goto(('scan',c,x,z,parity)) + elif tag=='component-end': + _,carry,sx,sz,parity=key + failure = negate and sx==1 and sz==1 + target=('reject','signed first-operand overflow') if failure else ('accepted-end',parity) + b.branch(1,{2:target},('reject','same complete component shape')) + elif tag=='accepted-end': + b.emit('write',2,2);b.emit('move',2,1) + guide_one();inputs_forward();b.goto(('start',key[1]^1,True)) + elif tag=='finish-y': + b.branch(1,{4:('finish-staged',)},('reject','same complete field frontier')) + elif tag=='finish-staged': + b.branch(2,{4:('rewind-step',)},('reject','exact staged frontier')) + elif tag=='rewind-step': + b.emit('move',3,-1);b.goto(('rewind-read',)) + elif tag=='rewind-read': + b.branch(3,{1:('rewind-inputs',),5:('install-start',)},('reject','complete unary guide')) + elif tag=='rewind-inputs': + for port in (0,1,2):b.emit('move',port,-1) + b.goto(('rewind-step',)) + elif tag=='install-start': + b.emit('move',3,1);b.goto(('install-guide',)) + elif tag=='install-guide': + b.branch(3,{1:('install-y',),4:('installed-end',0)},('reject','install guide format')) + elif tag=='install-y': + b.branch(1,{s:('install-staged',s) for s in (0,1,2)},('reject','complete protected second field')) + elif tag=='install-staged': + y=key[1];symbols=(2,) if y==2 else (0,1) + b.branch(2,{z:('install-symbols',y,z) for z in symbols},('reject','aligned staged component shape')) + elif tag=='install-symbols': + _,y,z=key + b.emit('write',0,y);b.emit('write',1,z) + for port in (0,1,2,3):b.emit('move',port,1) + b.goto(('install-guide',)) + elif tag=='installed-end': + port=key[1] + target=('halt',) if port==2 else ('installed-end',port+1) + b.branch(port,{4:target},('reject','exact installed public frontier')) + elif tag=='halt':b.emit('halt') + elif tag=='reject':b.emit('reject',key[1]) + else:raise ValueError('unknown two-output compiler state') + table=b.finish() + digest=hashlib.sha256(json.dumps(table,separators=(',',':')).encode()).hexdigest() + return table,dict(operation=op,rows=len(b.rows),states=len(b.labels), + public_ports=2,work_ports=2,negated_input=0 if negate else None, + table_sha256=digest) + + +def source_literal(event,caller): + """Retain exact source order through the original remapping grammar.""" + need(event.op=='SERVICE','original two-output SERVICE') + need(len(event.fields)==2 and len(set(event.fields))==2,'distinct ordered field ports') + token=event.token;wrapped=False + wrappers={'caller-local':4,'product-left':4,'product-right':5,'unit-fragment':6} + while isinstance(token,(tuple,list)) and token: + if len(token)==1 and isinstance(token[0],(tuple,list)): + token=token[0];wrapped=True;continue + if isinstance(token[0],str) and token[0] in wrappers: + need(len(token)==wrappers[token[0]],'source remap wrapper grammar') + token=token[-1];wrapped=True;continue + break + need(isinstance(token,(tuple,list)) and token and isinstance(token[0],str), + 'two-output origin grammar') + tag=token[0] + if tag in ('boundary-right','boundary-left'): + need(len(token)==3,'boundary swap token grammar') + _,column,raw=token + rows=caller['boundaries'][tag.split('-')[1]+'_program'] + need(tuple(raw) in tuple(tuple(x) for x in rows),'exact boundary source instruction') + origin=(tag,column,raw[1],raw[2]) + elif tag=='outer': + need(len(token)==4,'outer swap token grammar') + _,site,column,raw=token + need(type(site) is int and 0<=site> shift) & 1) + for _ in range(3): + self.tape.move(-1) + + def move(self, direction): + need(direction in (-1, 1), "virtual unit move") + t = self.tape + if direction == 1: + if t.read() == BLANK: + self.write(4) + for _ in range(3): + t.move(1) + else: + t.move(-1) + if t.read() == LEFT: + t.move(1) + raise ValueError("native routine crossed its local origin") + t.move(-1) + t.move(-1) + + +class BinaryContextPort: + """Read-only raw binary descriptor, with its own physical alphabet. + + Unlike CodedPort, read returns physical BLANK=6 at the frontier. A table + may inspect that frontier but cannot pass it or the current LEFT marker. + This supplies runtime e/f/K/rho data through counted local operations. + """ + __slots__ = ("tape",) + + def __init__(self, tape): + self.tape = tape + + def read(self): + symbol = self.tape.read() + need(symbol in (ZERO, ONE, BLANK), "binary context alphabet") + return symbol + + def write(self, value): + raise ValueError("native context is read-only") + + def move(self, direction): + need(direction in (-1, 1), "binary context unit move") + t = self.tape + if direction == 1: + need(t.read() in (ZERO, ONE), "context frontier cannot be crossed") + t.move(1) + else: + t.move(-1) + if t.read() == LEFT: + t.move(1) + raise ValueError("native context crossed its local origin") + + +def read_code(tape): + """Consume a numeric-format code; physical frontier returns None.""" + if tape.read() == BLANK: + return None + value = 0 + for _ in range(3): + bit = tape.read() + need(bit in (ZERO, ONE), "numeric codeword") + value = 2 * value + bit + tape.move(1) + need(value < 7, "unused numeric codeword") + return value + + +def write_code(tape, value): + for shift in (2, 1, 0): + emit(tape, (value >> shift) & 1) + + +def initialize(target, shape): + """Dispose of arbitrary old bytes, then zero the complete common format.""" + need(target is not shape, "private initialization cannot destroy its guide") + retire(target) + origin(shape) + in_component = False + while (symbol := read_code(shape)) is not None: + need(symbol in (ZERO, ONE, COMPONENT), "canonical signed components") + if symbol == COMPONENT: + need(in_component, "positive component width") + write_code(target, COMPONENT) + in_component = False + else: + write_code(target, ZERO) + in_component = True + need(not in_component, "component terminator") + origin(shape) + origin(target) + + +def copy_as_add(target, source): + """Signed addition into the actual destination, including any residue. + + Components are little-endian two's complement followed by COMPONENT. + Carries reset at delimiters; equal-sign signed overflow rejects. + No ideal-zero test or exact-value overwrite substitutes for addition. + """ + need(target is not source, "distinct COPY/ADD ports") + origin(source) + origin(target) + carry = 0 + last_a = last_b = last_out = 0 + in_component = False + while True: + a = read_code(source) + b = read_code(target) + need((a is None) == (b is None), "same complete numerical extent") + if a is None: + need(not in_component, "complete signed component") + break + need(a in (ZERO, ONE, COMPONENT) and b in (ZERO, ONE, COMPONENT), + "canonical signed addition operands") + need((a == COMPONENT) == (b == COMPONENT), "same component boundaries") + if a == COMPONENT: + need(in_component, "positive signed component width") + need(last_a != last_b or last_out == last_a, "signed addition overflow") + carry = 0 + in_component = False + continue + value = a + b + carry + last_a, last_b, last_out = a, b, value & 1 + carry = value >> 1 + for _ in range(3): + target.move(-1) + write_code(target, last_out) + in_component = True + origin(source) + origin(target) + + +def execute_table(table, ports, readonly_context=()): + """Run a supplied finite native table with every port confined. + + These tables retain explicit semantics/time/space premises. Fixture + tables are not advertised as Gaussian implementations. + """ + views = (tuple(CodedPort(t) for t in ports) + + tuple(BinaryContextPort(t) for t in readonly_context)) + pc = 0 + while True: + row = table[pc] + op = row[0] + if op == "halt": + break + if op == "reject": + raise ValueError(row[1]) + if op == "goto": + pc = row[1] + continue + view = views[row[1]] + if op == "branch": + pc = dict(row[2]).get(view.read(), row[3]) + continue + if op == "write": + view.write(row[2]) + elif op == "move": + view.move(row[2]) + else: + raise ValueError("native table opcode") + pc += 1 + for tape in tuple(ports)+tuple(readonly_context): + origin(tape) + + +@dataclass(frozen=True) +class Instruction: + op: str + ports: tuple = () + token: tuple = () + + +class Controller: + """Fixed finite controller of a fixed flat compiled template. + + rows implements the separately priced row/shape interface; all its + dynamic state belongs on the supplied tapes. services contains fixed + finite transition tables. Payload ports include metadata and all scratch. + The only runtime continuation is the physical Stack. + """ + def __init__(self, program, public_count, payloads, control, descriptor, + bridge, child_header, rows, services, stack_class, protected_ports=(), + primitive_work=(), primitive_context=()): + self.program = tuple(program) + self.public_count = public_count + self.payloads = tuple(payloads) + self.control = control + self.descriptor = descriptor + self.bridge = bridge + self.child_header = child_header + self.rows = rows + self.services = services + need(len({id(t) for t in self.payloads+(control,descriptor,bridge,child_header)}) + == len(self.payloads)+4, "all physical ports distinct") + self.stack = stack_class(self.payloads, control, descriptor) + self.protected_ports = tuple(protected_ports) + owned = {e.ports[0] for e in self.program if e.op == "INIT"} + need(all(public_count <= i < len(self.payloads) for i in owned), "INIT only private physical slots") + need(owned.isdisjoint(self.protected_ports), "owned fields cannot be borrowed descriptors") + self.root_cleanup = tuple(i for i in range(public_count,len(self.payloads)) + if i not in self.protected_ports) + self.primitive_work = tuple(primitive_work) + self.primitive_context = tuple(primitive_context) + data_ports = {i for e in self.program for i in e.ports} + need(all(0 <= i < len(self.payloads) for i in data_ports), "compiled port range") + need(all(i >= public_count and i < len(self.payloads) and i not in data_ports + and i not in self.protected_ports for i in self.primitive_work), "separate primitive scratch") + need(len(set(self.primitive_work)) == len(self.primitive_work), "distinct primitive work ports") + need(len(set(self.primitive_context)) == len(self.primitive_context) + and all(i in self.protected_ports and 0 <= i < len(self.payloads) + and i not in data_ports for i in self.primitive_context), "borrowed binary context ports") + self.pc_bits = max(1, (len(self.program) - 1).bit_length()) + self.pc_words = tuple(tuple((pc >> j) & 1 for j in range(self.pc_bits)) + for pc in range(len(self.program))) + need(self.program and self.program[-1].op == "RET", "finite completed program") + + def save_pc(self, pc): + need(self.descriptor.read() == BLANK, "empty active PC descriptor") + for bit in self.pc_words[pc]: + emit(self.descriptor, bit) + origin(self.descriptor, BASE) + + def consume_pc(self): + pc = 0 + for shift in range(self.pc_bits): + bit = self.descriptor.read() + need(bit in (ZERO, ONE), "binary return PC") + pc |= bit << shift + emit(self.descriptor, BLANK) + need(self.descriptor.read() == BLANK, "exact fixed return PC width") + origin(self.descriptor, BASE) + need(pc < len(self.program) and pc > 0 and self.program[pc-1].op == "PAID", + "return PC designates a paid continuation") + return pc + + def has_parent(self): + self.control.move(-1) + symbol = self.control.read() + self.control.move(1) + need(symbol in (BASE, END), "complete continuation top") + return symbol == END + + def descend(self, pc): + event = self.program[pc] + source = self.payloads[event.ports[0]] + transfer(source, self.bridge, target_marker=BASE) + self.rows.prepare(event.token, self.child_header) + self.save_pc(pc + 1) + self.stack.push((True,) * len(self.payloads)) + self.rows.install(self.bridge, self.child_header, + self.payloads[:self.public_count]) + retire(self.bridge, BASE) + retire(self.child_header, BASE) + + def primitive(self, token, fields): + for i in self.primitive_work: + retire(self.payloads[i]) + execute_table(self.services[token], + tuple(self.payloads[i] for i in fields+self.primitive_work), + tuple(self.payloads[i] for i in self.primitive_context)) + for i in self.primitive_work: + retire(self.payloads[i]) + + def ascend(self): + self.rows.collect(self.payloads[:self.public_count], self.bridge) + for tape in self.payloads: + retire(tape) + self.stack.pop() # ignore observer sizes and heads + pc = self.consume_pc() + target = self.payloads[self.program[pc-1].ports[0]] + retire(target) + transfer(self.bridge, target, source_marker=BASE) + retire(self.bridge, BASE) + return pc + + def run(self, observe=None): + pc = 0 + while True: + event = self.program[pc] + if observe is not None: + observe("before", pc, event) # checker only; ignores return value + if event.op == "INIT": + initialize(self.payloads[event.ports[0]], self.payloads[0]) + pc += 1 + elif event.op == "CLEAR": + retire(self.payloads[event.ports[0]]) + pc += 1 + elif event.op == "COPY": + copy_as_add(self.payloads[event.ports[0]], self.payloads[event.ports[1]]) + pc += 1 + elif event.op == "SERVICE": + self.primitive(event.token,event.ports) + pc += 1 + elif event.op == "PAID": + if self.rows.is_leaf(event.token): + self.primitive(("leaf",)+event.token,event.ports) + pc += 1 + else: + self.descend(pc) + pc = 0 + elif event.op == "RET": + if not self.has_parent(): + for i in self.root_cleanup: + retire(self.payloads[i]) + break + pc = self.ascend() + else: + raise ValueError("compiled opcode") + if observe is not None: + observe("after", pc, event) + + +def boundary_actions(q, b, parent_total, child_total, input_length, + output_length, staged_header_length): + """Exact descend+ascend actions, excluding the three row-service calls. + + Also excludes caller leaf/top tests. All heads are at local origins. + Includes PC, all retirement, occupied-target replacement and both relays. + """ + return (4 * parent_total + 5 * child_total + 18 * input_length + + 13 * output_length + 5 * staged_header_length + + 38 * q + 27 * b + 103) diff --git a/research/current-swap-flat-tables/vendor/lifecycle/source_ir.py b/research/current-swap-flat-tables/vendor/lifecycle/source_ir.py new file mode 100644 index 0000000000..79c95fa794 --- /dev/null +++ b/research/current-swap-flat-tables/vendor/lifecycle/source_ir.py @@ -0,0 +1,522 @@ +"""Source-driven lifecycle IR and finite compiler lowering. + +All recursion/dictionaries here belong to template construction, before runtime +input size varies. machine.py executes the resulting fixed finite program. +Prepared for @CubeJerry with substantial OpenAI assistance. Apache-2.0. +""" +from collections import Counter +from dataclasses import dataclass +from fractions import Fraction + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +@dataclass(frozen=True) +class Event: + op: str + fields: tuple + token: tuple = () + rank: int = 0 + + +@dataclass(frozen=True) +class Unit: + name: str + roles: tuple + owned: tuple + events: tuple + + def check(self): + public = {name for name, rank in self.roles} + private = set(self.owned) + need(len(public) == len(self.roles) and len(private) == len(self.owned), "unique unit names") + need(public.isdisjoint(private), "public/private name separation") + need(all(type(r) is int and r >= 1 for _, r in self.roles), "positive target ranks") + live = set() + for e in self.events: + need(e.op in ("INIT", "CLEAR", "COPY", "SERVICE", "PAID"), "unit opcode") + if e.op == "INIT": + need(len(e.fields) == 1 and e.fields[0] in private and e.fields[0] not in live, "fresh private INIT") + live.add(e.fields[0]) + elif e.op == "CLEAR": + need(len(e.fields) == 1 and e.fields[0] in live, "CLEAR only own live bank") + live.remove(e.fields[0]) + else: + need(e.fields and all(f in public or f in live for f in e.fields), "use outside private lifetime") + if e.op == "COPY": + need(len(e.fields) == 2 and e.fields[0] in live + and e.fields[0] != e.fields[1], "private COPY ports") + if e.op == "PAID": + need(len(e.fields) == 1 and type(e.rank) is int and e.rank > 0, "positive whole paid job") + need(not live, "all private lifetimes end") + return self + + def pieces(self): + fragments, rounds = [[]], [] + for e in self.events: + if e.op == "PAID": + rounds.append(e) + fragments.append([]) + else: + fragments[-1].append(e) + return tuple(tuple(f) for f in fragments), tuple(rounds) + + +def remap(event, names, context=(), rank_factor=1): + return Event(event.op, tuple(names[f] for f in event.fields), + context + (event.token,), event.rank * rank_factor) + + +def product(left, right): + """p7-TENSOR chronological substitution; never tensor an operator sum.""" + left.check(); right.check() + lf, lr = left.pieces() + roles = tuple(((i,j),k*h) for i,k in left.roles for j,h in right.roles) + owned, maps, events = [], {}, [] + for j,h in right.roles: + maps[j] = {i:(i,j) for i,_ in left.roles} + for o in left.owned: + fresh = ("left",j,o) + owned.append(fresh); maps[j][o] = fresh + for j,h in right.roles: + for i,_ in left.roles: + events.append(Event("SERVICE",((i,j),),("product-left-enter",j,h,i))) + for ell in range(len(lr)+1): + for j,h in right.roles: + events += [remap(e,maps[j],("product-left",j,h)) for e in lf[ell]] + if ell == len(lr): + break + issuing = lr[ell] + names = {j:maps[j][issuing.fields[0]] for j,_ in right.roles} + need(len(set(names.values())) == len(names), "distinct product request owners") + for o in right.owned: + fresh = ("right",ell,o) + owned.append(fresh); names[o] = fresh + events += [Event("SERVICE",(names[j],),("product-enter",ell,j,issuing.token)) for j,_ in right.roles] + events += [remap(e,names,("product-right",ell,issuing.rank,issuing.token),issuing.rank) for e in right.events] + events += [Event("SERVICE",(names[j],),("product-return",ell,j,issuing.token)) for j,_ in right.roles] + for j,h in right.roles: + for i,_ in left.roles: + events.append(Event("SERVICE",((i,j),),("product-left-return",j,h,i))) + return Unit(left.name+"*"+right.name,roles,tuple(owned),tuple(events)).check() + + +def completion_split(unit, cutoff, floor): + unit.check() + need(0 < cutoff < floor <= max(k for _,k in unit.roles), "completion/splitting domain") + completed = [(name,k) for name,k in unit.roles if k < floor] + events = [Event("SERVICE",(name,),("whole-job-in",k,floor)) for name,k in completed] + extended = list(unit.events) + for name,k in completed: + extended.append(Event("PAID",(name,),("completion",k,floor),floor-k)) + for e in extended: + if e.op != "PAID": + events.append(e); continue + start = 0 + while start < e.rank: + size = min(cutoff,e.rank-start) + token = ("piece",start,size,e.rank,e.token) + events += [Event("SERVICE",e.fields,("piece-enter",)+token), + Event("PAID",e.fields,token,size), + Event("SERVICE",e.fields,("piece-return",)+token)] + start += size + events += [Event("SERVICE",(name,),("whole-job-out",k,floor)) for name,k in completed] + return Unit(unit.name+"/pass",tuple((name,max(k,floor)) for name,k in unit.roles), + unit.owned,tuple(events)).check() + + +def current_local(word): + """Retain every current #6030 operand, chart, lifetime and paid position. + + No all-column algebra is redone. MOVE ranks are the dimension differences + in the authenticated source rule, with their native meaning retained. + """ + p,o = word["public"],word["owned_fields"] + frames = word["frames"] + current = list(word["initial"])+[None]*o + live,untouched,starts,episodes = set(),set(),{},[] + events,moves,peak = [],Counter(),0 + for pc,raw in enumerate(word["program"]): + op,r = raw[:2] + need(type(r) is int and 0 <= r < p+o,"current local role") + token = ("local",pc,tuple(raw)) + if op == "INIT": + need(p <= r and r not in live,"current fresh private INIT") + live.add(r); untouched.add(r); starts[r] = pc + current[r] = raw[2]; peak = max(peak,len(live)) + events.append(Event("INIT",(r,),token)) + elif op == "CLEAR": + need(r in live and current[r] == raw[2],"current owned CLEAR chart") + live.remove(r); untouched.discard(r) + episodes.append((r,starts.pop(r),pc)); current[r] = None + events.append(Event("CLEAR",(r,),token)) + elif op == "MOVE": + need(len(raw) == 5 and type(raw[4]) is bool,"typed private MOVE flag") + need(current[r] == raw[2] and (r in live) == raw[4],"current MOVE owner and chart") + need(r < p or r in live,"live MOVE source") + rank = abs(len(frames[raw[3]])-len(frames[raw[2]])) + need(rank > 0,"current positive MOVE rank") + current[r] = raw[3]; moves[rank] += 1 + untouched.discard(r) + events += [Event("SERVICE",(r,),("move-in",)+token), + Event("PAID",(r,),token,rank), + Event("SERVICE",(r,),("move-out",)+token)] + else: + need(op in ("COPY","ADD","SCALE") and current[r] == raw[-1],"current scalar destination chart") + need(r < p or r in live,"live scalar destination") + coefficient = Fraction(raw[-2]) + need(coefficient != 0,"nonzero source coefficient") + if op == "SCALE": + fields = (r,) + else: + src = raw[2] + need(type(src) is int and 0 <= src < p+o and src != r,"current distinct scalar source") + need((src < p or src in live) and current[src] == raw[-1],"current common scalar chart") + fields = (r,src) + if op == "COPY": + need(r in untouched and coefficient == 1,"current COPY follows untouched INIT with coefficient one") + events.append(Event("COPY",fields,token)) + else: + events.append(Event("SERVICE",fields,token)) + untouched.discard(r) + need(not live and current[:p] == word["final"],"current complete local exit") + return tuple(events),dict(events=len(word["program"]),owned_labels=o, + owned_lifetimes=len(episodes),peak_live=peak, + episodes=episodes,paid=dict(sorted(moves.items()))) + + +def current_caller(word,caller): + """Exact outer/local field maps and explicit copied-query lifetimes. + + Named contact/normalizer/query services retain source endpoint meanings. + Every original scalar/MOVE token and its chronology are preserved. + """ + local_events,report = current_local(word) + ports = tuple(word["live"]) + need(len(ports) == len(set(ports)) == 104,"current 104 ports") + need((caller["kind"],caller["pairs"],caller["prefix_pairs"],caller["ambient_rank"]) + == ("complex",16,7,145),"current physical caller family") + main_local = set(ports)|{x+112 for x in ports} + helpers = sorted(set(range(word["public"]))-main_local) + locals_ = [e for e in caller["physical_events"] if e[0] == "LOCAL"] + need(len(locals_) == 18 and all(not e[3] for e in locals_),"current forward local sites") + public = 32*104+18*len(helpers) + own_first,query_first = public,public+18*word["owned_fields"] + owned = tuple(range(public,query_first+104)) + roles = [] + for i,term in enumerate(caller["diagonal"]): + stages = term[1:] + rank = (9 if stages[0] else 1)+8*sum(stages[1:]) + roles += [(i*104+j,rank) for j in range(104)] + events,local_sites,query_sites = [],[],[] + def scalar(raw,context): + for j in range(104): + fields = (raw[1]*104+j,) if raw[0] == "SCALE" else (raw[1]*104+j,raw[2]*104+j) + events.append(Event("SERVICE",fields,context+(j,tuple(raw)))) + for raw in caller["boundaries"]["right_program"]: + scalar(raw,("boundary-right",)) + local_number = 0 + for site,raw in enumerate(caller["physical_events"]): + op = raw[0] + if op == "LOCAL": + _,stage,pair,reverse = raw + need(not reverse,"all-forward local occurrence") + names = {} + for j,r in enumerate(ports): + names[r] = 2*pair*104+j; names[r+112] = (2*pair+1)*104+j + for j,r in enumerate(helpers): + field = 32*104+local_number*len(helpers)+j + names[r] = field + rank = len(word["frames"][word["final"][r]])-len(word["frames"][word["initial"][r]]) + roles.append((field,rank)) + for j in range(word["owned_fields"]): + names[word["public"]+j] = own_first+local_number*word["owned_fields"]+j + need(len(names) == len(set(names.values())) == word["public"]+word["owned_fields"], + "injective complete current local grant") + for r in range(word["public"]): + events.append(Event("SERVICE",(names[r],),("local-entry",site,stage,r))) + events += [remap(e,names,("caller-local",site,stage)) for e in local_events] + for r in range(word["public"]): + events.append(Event("SERVICE",(names[r],),("local-return",site,stage,r))) + local_sites.append((site,stage,tuple(sorted(names.items())))); local_number += 1 + elif op == "QUERY_SHEAR": + _,stage,pair,reverse = raw + need(not reverse,"current forward query") + for j in range(104): + x,y,z = 2*pair*104+j,(2*pair+1)*104+j,query_first+j + token = ("query",site,stage,j) + events += [Event("INIT",(z,),token),Event("COPY",(z,x),token), + Event("SERVICE",(z,),("query-in",)+token),Event("PAID",(z,),token,1), + Event("SERVICE",(z,),("query-out",)+token), + Event("SERVICE",(y,z),("query-add",)+token),Event("CLEAR",(z,),token)] + query_sites.append((site,j,x,y,z)) + elif op == "IDLE": + for side in (0,1): + for j in range(104): + field = (2*raw[1]+side)*104+j + token = ("idle",site,tuple(raw[2]),side,j) + events += [Event("SERVICE",(field,),("idle-in",)+token), + Event("PAID",(field,),token,8*len(raw[2])), + Event("SERVICE",(field,),("idle-out",)+token)] + elif op == "Q_POWER": + for j in range(104): + events.append(Event("SERVICE",(raw[1]*104+j,),("central-square",site,j,raw[2]))) + else: + need(op in ("ADD","SWAP","SIGNED_SWAP"),"current outer scalar opcode") + scalar(raw,("outer",site)) + for raw in caller["boundaries"]["left_program"]: + scalar(raw,("boundary-left",)) + roles = tuple(sorted(roles)) + need([r for r,_ in roles] == list(range(public)),"every productive field supplied once") + # The pinned occurrence theorem supplies the complete 145-coordinate + # whole-job canonicalizers. Each is a charged service, never a free name. + events = ([Event("SERVICE",(r,),("raw-whole-job-enter",r,k)) for r,k in roles] + +events+[Event("SERVICE",(r,),("raw-whole-job-return",r,k)) for r,k in roles]) + unit = Unit("selected6030",roles,owned,tuple(events)).check() + report.update(public_count=public,raw_owned=len(owned),local_sites=len(local_sites), + query_lifetimes=len(query_sites),total_lifetimes=18*report["owned_lifetimes"]+len(query_sites), + raw_paid=dict(sorted(Counter(e.rank for e in events if e.op=="PAID").items())), + raw_targets=dict(sorted(Counter(k for _,k in roles).items())),raw_events=len(events)) + return unit,report + + +def lower(unit,rank,source): + """Refine #5443's unchanged matching, with no partial/interface fallback. + + Insert all inter-round fragments before a class is suspended. Flatten + finite compiler substitutions; only rank-one leaves make runtime children. + """ + unit.check() + fragments,rounds = unit.pieces() + need(rounds,"nonempty paid word") + need(max(e.rank for e in rounds)= self.floor, 'ancestor prefix accessed') + return self.cells[self.head] if self.head < len(self.cells) else BLANK + + def write(self, value): + need(value in range(7), 'finite tape alphabet') + need(self.head >= self.floor, 'ancestor prefix overwritten') + self.counts.writes += 1 + while len(self.cells) <= self.head: + self.cells.append(BLANK) + self.cells[self.head] = value + + def move(self, direction): + need(direction in (-1, 1), 'unit move') + self.counts.moves += 1 + self.head += direction + need(self.head >= self.floor, 'ancestor prefix crossed') + + +def emit(tape, symbol): + tape.write(symbol) + tape.move(1) + + +def rewind(tape, marker): + tape.move(-1) + while tape.read() != marker: + tape.move(-1) + tape.move(1) + + +def clear_descriptor(tape): + """Entry and exit are at the descriptor origin.""" + while (symbol := tape.read()) != BLANK: + need(symbol in (ZERO, ONE), 'binary descriptor') + emit(tape, BLANK) + rewind(tape, BASE) + + +class Stack: + """No saved frame, parent pointer, frame size or origin is stored here.""" + def __init__(self, payloads, control, descriptor): + self.payloads = tuple(payloads) + self.control = control + self.descriptor = descriptor + + def push(self, present): + need(len(present) == len(self.payloads), 'fixed role bitmap') + c = self.control + need(c.read() == BLANK, 'control at free top') + emit(c, LEFT) + for tape, occupied in zip(self.payloads, present): + need(type(occupied) is bool, 'role presence bit') + emit(c, int(occupied)) + tape.move(-1) + while (symbol := tape.read()) != LEFT: + need(symbol in (ZERO, ONE), 'binary prefix before current head') + emit(c, ONE) + tape.move(-1) + emit(c, ZERO) + tape.move(1) + if not occupied: + need(tape.read() == BLANK, 'absent role is empty') + while (symbol := tape.read()) != BLANK: + need(symbol in (ZERO, ONE), 'binary parent payload') + tape.move(1) + emit(tape, LEFT) + emit(c, SEP) + d = self.descriptor + while (symbol := d.read()) != BLANK: + need(symbol in (ZERO, ONE), 'binary descriptor') + emit(c, symbol) + emit(d, BLANK) + rewind(d, BASE) + emit(c, END) + + def pop(self): + """Child payloads are empty at their origins; clear its descriptor. + + Returned sizes/heads are observer counts for the source API adapter. + No branch or tape move uses those counts. + """ + clear_descriptor(self.descriptor) + c = self.control + c.move(-1) + need(c.read() == END, 'complete control frame') + c.move(-1) + while (symbol := c.read()) != LEFT: + need(symbol in (ZERO, ONE, SEP), 'frame start before ancestor boundary') + c.move(-1) + emit(c, BLANK) + state = [] + for tape in self.payloads: + present = c.read() + need(present in (ZERO, ONE), 'role presence bit') + emit(c, BLANK) + need(tape.read() == BLANK, 'child payload is retired') + tape.move(-1) + need(tape.read() == LEFT, 'child delimiter') + tape.write(BLANK) + tape.move(-1) + size = 0 + while (symbol := tape.read()) != LEFT: + need(symbol in (ZERO, ONE), 'parked parent payload') + size += 1 + tape.move(-1) + tape.move(1) + if not present: + need(tape.read() == BLANK, 'absent parent role is empty') + head = 0 + while (symbol := c.read()) == ONE: + need(tape.read() in (ZERO, ONE), 'saved head is within payload') + tape.move(1) + head += 1 + emit(c, BLANK) + need(symbol == ZERO, 'terminated unary head') + emit(c, BLANK) + state.append((bool(present), size, head)) + need(c.read() == SEP, 'complete fixed-role header') + emit(c, BLANK) + d = self.descriptor + while (symbol := c.read()) != END: + need(symbol in (ZERO, ONE), 'binary saved descriptor') + emit(d, symbol) + emit(c, BLANK) + c.write(BLANK) + c.move(-1) + while c.read() == BLANK: + c.move(-1) + need(c.read() in (BASE, END), 'previous control top') + c.move(1) + rewind(d, BASE) + return state diff --git a/research/current-swap-flat-tables/verify.py b/research/current-swap-flat-tables/verify.py new file mode 100644 index 0000000000..af91691763 --- /dev/null +++ b/research/current-swap-flat-tables/verify.py @@ -0,0 +1,187 @@ +"""Exact signed-permutation, actual-source and unchanged-controller checks. + +Prepared for @CubeJerry with substantial OpenAI assistance. Apache-2.0. +""" +from pathlib import Path +from collections import Counter +from fractions import Fraction +import argparse +import gzip +import hashlib +import json +import random +import sys + +sys.path.insert(0,str(Path(__file__).resolve().parent)) +from physical import A,IR,ROOT,Tape,load_module +from source_binding import check_inputs +from vendor import scalar_tables as scalar +from tables import compile_swap,source_literal,bind_services,need +from fixtures import check_case,encode_field,decode_field,CountedTable + + +def inputs(): + check_inputs();repo=ROOT.parents[1] + word=json.loads(gzip.decompress((repo/'research/p104-helper470-twin-rung-removal/WORD.json.gz').read_bytes())) + caller=json.loads((repo/'research/p104-productive-controller/CONTROLLER.json').read_text()) + return word,caller + + +def arithmetic(): + counters=Counter();receipts=[] + for op in ('SWAP','SIGNED_SWAP'): + table,receipt=compile_swap(op);receipts.append(receipt) + for w in range(1,6): + values=range(-(1<<(w-1)),1<<(w-1)) + for x in values: + for y in values: + allowed,result=check_case(table,op,(x,x),(y,y),(w,w)) + counters['cases']+=1;counters['accepted']+=allowed + counters['rejected']+=1-allowed + counters['physical_actions']+=result['actions'];counters['table_steps']+=result['steps'] + rng=random.Random(6030) + for widths in ((1,1),(1,2),(5,5,16,16),(65,129),(129,65,1,2),(2,3,5,8,17,33)): + for k in range(8): + xs=tuple(rng.randrange(-(1<<(w-1)),1<<(w-1)) for w in widths) + ys=tuple(rng.randrange(-(1<<(w-1)),1<<(w-1)) for w in widths) + if k==0:xs=(0,)*len(widths) + elif k==1:xs=tuple(-(1<<(w-1)) for w in widths) + elif k==2:ys=xs + allowed,result=check_case(table,op,xs,ys,widths) + counters['wide_or_mixed_fields']+=1;counters['wide_or_mixed_accepted']+=allowed + counters['physical_actions']+=result['actions'];counters['table_steps']+=result['steps'] + need(counters['cases']==2728 and counters['accepted']==2666 and counters['rejected']==62, + 'closed full signed-domain census') + return dict(check='arithmetic',counts=dict(counters),tables=receipts) + + +def binding(): + word,caller=inputs();unit,summary=IR.current_caller(word,caller) + swaps=[];counts=Counter();scopes=Counter();scalar_count=0;excluded=Counter() + for event in unit.events: + if event.op!='SERVICE':continue + try:op,origin=source_literal(event,caller) + except ValueError: + try:scalar.source_literal(event,word,caller) + except ValueError:excluded[event.token[0]]+=1 + else:scalar_count+=1 + else:swaps.append(event);counts[op]+=1;scopes[origin[0]]+=1 + need(dict(counts)=={'SWAP':5928,'SIGNED_SWAP':4992},'exact current two-output census') + need(dict(scopes)=={'boundary-right':2808,'outer':4992,'boundary-left':3120},'exact source scope partition') + need(scalar_count==366842,'retained scalar class is unchanged') + services,receipts,origins=bind_services(swaps,caller) + need(len(origins)==10920 and len(receipts)==2,'full current swap catalogue') + original=next(e for e in swaps if e.token[0]=='outer') + issuing=next(e for e in IR.current_local(word)[0] if e.op=='PAID') + names={f:('actual-bank',j) for j,f in enumerate(original.fields)} + right=IR.remap(original,names,('product-right',2,issuing.rank,issuing.token)) + left=IR.remap(right,{f:f for f in right.fields},('product-left',5,3)) + nested=IR.remap(left,{f:f for f in left.fields},('unit-fragment',7,11,3,0)) + need(source_literal(nested,caller)==source_literal(original,caller),'active source semantics through wrappers') + need(nested.fields==tuple(names[f] for f in original.fields),'actual ordered remapped owners') + return dict(check='binding',caller_events=len(unit.events),swap_services=len(origins), + retained_scalar_services=scalar_count,combined_arithmetic_services=scalar_count+len(origins), + counts=dict(counts),scopes=dict(scopes),tables=receipts, + excluded_services=dict(excluded),raw_paid=summary['raw_paid'], + source_receipt_sha256=hashlib.sha256(json.dumps(origins,separators=(',',':')).encode()).hexdigest()) + + +def controller_run(events,services,values,width): + public=[Tape(encode_field(v,(width,width)),origin=17+5*i) for i,v in enumerate(values)] + def body_receipt(): + h=hashlib.sha256() + for i,t in enumerate(public): + body=t.body();h.update(i.to_bytes(8,'big'));h.update(len(body).to_bytes(8,'big'));h.update(bytes(body)) + return h.hexdigest() + input_receipt=body_receipt() + n=len(public);context=Tape((1,0,1,0,0,1),origin=500000,readonly=True) + work=[Tape((1,0,1,0,1),origin=510000),Tape((0,1,0,1,0,1,1),origin=520000)] + payloads=tuple(public+[context]+work) + stack=load_module('swap_retained_stack',ROOT/'vendor/stack.py') + program=tuple(A.Instruction('SERVICE',e.fields,e.token) for e in events)+(A.Instruction('RET'),) + counters={id(t):CountedTable(t) for t in services.values()} + counted={token:counters[id(t)] for token,t in services.items()} + admin=[Tape(origin=600000+100*i,marker=A.BASE) for i in range(4)] + controller=A.Controller(program,n,payloads,*admin,rows=None,services=counted, + stack_class=stack.Stack,protected_ports=(n,), + primitive_work=(n+1,n+2),primitive_context=(n,)) + controller.run() + observed=[decode_field(t.body()) for t in public] + need(all(row[1]==(width,width) for row in observed),'complete controller field shapes') + need(context.body()==(1,0,1,0,0,1),'borrowed context preserved') + need(all(t.blank() for t in work),'actual Controller scratch retirement') + need(all(t.pos==t.origin and t.sentinel_ok() for t in payloads+tuple(admin)), + 'actual Controller complete heads and ancestor ownership') + result=dict(field_count=n,component_width=width,services=len(events), + physical_actions=sum(t.actions for t in payloads+tuple(admin)), + table_steps=sum(t.steps for t in counters.values()), + program_sha256=hashlib.sha256(json.dumps([(e.op,e.ports,e.token) for e in program],separators=(',',':')).encode()).hexdigest(), + service_table_sha256s=sorted({hashlib.sha256(json.dumps(t.table,separators=(',',':')).encode()).hexdigest() for t in counters.values()}), + input_body_sha256=input_receipt,output_body_sha256=body_receipt(), + body_receipt_format='increasing field index: u64be index, u64be raw length, raw symbol bytes') + return [row[0] for row in observed],result + + +def controller_blocks(): + word,caller=inputs();unit,summary=IR.current_caller(word,caller) + n=len(unit.roles);width=4 + # The full original right-boundary block, after its native entry cut. + indexed=[(i,e) for i,e in enumerate(unit.events) if e.token[0]=='boundary-right'] + right=[e for _,e in indexed] + need(len(right)==5720 and indexed[-1][0]-indexed[0][0]+1==len(right), + 'actual uninterrupted right-boundary block') + swaps=[e for e in right if e.token[-1][0]=='SWAP'] + scalars=[e for e in right if e.token[-1][0] in ('ADD','SCALE')] + services,_,_=bind_services(swaps,caller) + earlier,_,_=scalar.bind_services(scalars,word,caller) + need(set(services).isdisjoint(earlier),'indivisible source class registries');services.update(earlier) + values=[((r//104+2*(r%104))%7-3,(3*(r//104)+(r%104))%5-2) for r in range(n)] + expected=[list(v) for v in values] + # Independent source-array interpretation; it does not read lowered tokens. + peak=3 + for raw in caller['boundaries']['right_program']: + for j in range(104): + x=raw[1]*104+j + if raw[0]=='SWAP': + y=raw[2]*104+j;expected[x],expected[y]=expected[y],expected[x] + elif raw[0]=='SCALE':expected[x]=[Fraction(raw[2])*z for z in expected[x]] + else: + need(raw[0]=='ADD','original boundary opcode') + y=raw[2]*104+j;expected[x]=[a+Fraction(raw[3])*b for a,b in zip(expected[x],expected[y])] + need(all(Fraction(z).denominator==1 and -8<=z<8 for z in expected[x]),'right boundary fixture admission') + peak=max(peak,*(abs(z) for z in expected[x])) + observed,r1=controller_run(right,services,values,width) + need(observed==[tuple(int(z) for z in row) for row in expected],'original full right-boundary endpoint') + r1.update(first_event=indexed[0][0],last_event=indexed[-1][0],maximum_absolute_fixture_value=int(peak), + output_sha256=hashlib.sha256(json.dumps(observed,separators=(',',':')).encode()).hexdigest()) + # A second actual contiguous block covers the first ordered signed swap. + site=next(i for i,raw in enumerate(caller['physical_events']) if raw[0]=='SIGNED_SWAP') + indexed=[(i,e) for i,e in enumerate(unit.events) if e.token[0]=='outer' and e.token[1]==site] + signed=[e for _,e in indexed] + need(len(signed)==104 and indexed[-1][0]-indexed[0][0]+1==104,'actual uninterrupted signed block') + services,_,_=bind_services(signed,caller) + values=[(r%5-2,r%7-3) for r in range(n)] + raw=caller['physical_events'][site] + for j in range(104): + values[raw[1]*104+j]=(-7+j%8,j%7-3) + values[raw[2]*104+j]=(-8,j%8) + expected=list(values) + for j in range(104): + x,y=raw[1]*104+j,raw[2]*104+j + expected[x],expected[y]=values[y],tuple(-v for v in values[x]) + observed,r2=controller_run(signed,services,values,width) + need(observed==expected,'original signed source order including minimum second operands') + r2.update(source_site=site,first_event=indexed[0][0],last_event=indexed[-1][0], + output_sha256=hashlib.sha256(json.dumps(observed,separators=(',',':')).encode()).hexdigest()) + return dict(check='controller_blocks',right_boundary=r1,first_signed_block=r2) + + +def main(): + parser=argparse.ArgumentParser();parser.add_argument('--suite',choices=['arithmetic','binding','controller'],required=True) + args=parser.parse_args();result={'arithmetic':arithmetic,'binding':binding,'controller':controller_blocks}[args.suite]() + expected=json.loads((ROOT/'RESULT.json').read_text())[args.suite] + need(json.loads(json.dumps(result))==expected,'committed exact suite receipt') + print(json.dumps(result,sort_keys=True));print('PASS_CURRENT_SWAP_FLAT_TABLES_'+args.suite.upper()) + + +if __name__=='__main__':main()