diff --git a/research/compact-rounded-add/ARITHMETIC.json b/research/compact-rounded-add/ARITHMETIC.json new file mode 100644 index 0000000000..66b5895406 --- /dev/null +++ b/research/compact-rounded-add/ARITHMETIC.json @@ -0,0 +1,172 @@ +{ + "exhaustive": [ + { + "accepted": 340, + "cases": 340, + "coefficient": "0", + "rejected": 0, + "widths": [ + 1, + 4 + ] + }, + { + "accepted": 298, + "cases": 340, + "coefficient": "1/2", + "rejected": 42, + "widths": [ + 1, + 4 + ] + }, + { + "accepted": 282, + "cases": 340, + "coefficient": "-2/3", + "rejected": 58, + "widths": [ + 1, + 4 + ] + }, + { + "accepted": 116, + "cases": 340, + "coefficient": "3", + "rejected": 224, + "widths": [ + 1, + 4 + ] + }, + { + "accepted": 267, + "cases": 340, + "coefficient": "-5/6", + "rejected": 73, + "widths": [ + 1, + 4 + ] + }, + { + "accepted": 14, + "cases": 84, + "coefficient": "-14729531/163840", + "rejected": 70, + "widths": [ + 1, + 3 + ] + }, + { + "accepted": 18, + "cases": 84, + "coefficient": "-1379/250", + "rejected": 66, + "widths": [ + 1, + 3 + ] + }, + { + "accepted": 30, + "cases": 84, + "coefficient": "1085645/393216", + "rejected": 54, + "widths": [ + 1, + 3 + ] + } + ], + "extra_endpoint_cases": [ + { + "accepted": true, + "coefficient": "1/32", + "width": 2, + "x": -2, + "y": -2 + }, + { + "accepted": true, + "coefficient": "1/32", + "width": 2, + "x": 1, + "y": 1 + }, + { + "accepted": true, + "coefficient": "1/32", + "width": 2, + "x": 0, + "y": -1 + }, + { + "accepted": false, + "coefficient": "-31/16", + "width": 2, + "x": -2, + "y": -2 + }, + { + "accepted": true, + "coefficient": "-31/16", + "width": 2, + "x": 1, + "y": 1 + }, + { + "accepted": false, + "coefficient": "-31/16", + "width": 2, + "x": 0, + "y": -1 + }, + { + "accepted": false, + "coefficient": "-14729531/163840", + "width": 8, + "x": -128, + "y": -128 + }, + { + "accepted": false, + "coefficient": "-14729531/163840", + "width": 8, + "x": 127, + "y": 127 + }, + { + "accepted": true, + "coefficient": "-14729531/163840", + "width": 8, + "x": 0, + "y": -1 + }, + { + "accepted": false, + "coefficient": "1085645/393216", + "width": 4, + "x": -8, + "y": -8 + }, + { + "accepted": false, + "coefficient": "1085645/393216", + "width": 4, + "x": 7, + "y": 7 + }, + { + "accepted": true, + "coefficient": "1085645/393216", + "width": 4, + "x": 0, + "y": -1 + } + ], + "oracle": "direct signed integers and mathematical floor; no transition arithmetic imported", + "total_cases": 1952 +} diff --git a/research/compact-rounded-add/CONTROLS.json b/research/compact-rounded-add/CONTROLS.json new file mode 100644 index 0000000000..ad5be0f798 --- /dev/null +++ b/research/compact-rounded-add/CONTROLS.json @@ -0,0 +1,14 @@ +{ + "detected_mutants": [ + "lost-leading", + "lost-negative", + "tie-down", + "unsigned-residue", + "omit-high" + ], + "extra_controls": [ + "positive_negative_even_ties", + "floor_not_truncation", + "odd_divisor_domain" + ] +} diff --git a/research/compact-rounded-add/DEPENDENCIES.json b/research/compact-rounded-add/DEPENDENCIES.json new file mode 100644 index 0000000000..33d15813b5 --- /dev/null +++ b/research/compact-rounded-add/DEPENDENCIES.json @@ -0,0 +1,59 @@ +{ + "schema_version": 1, + "files": [ + { + "local_path": "data/word.json.gz", + "repository": "DreamingOfClouds/integer-mult-bounds", + "commit": "03626137d0bd57f09b0bf9597376183ce6fa9683", + "original_path": "research/p104-main-wire-native/data/word.json.gz", + "bytes": 349022, + "git_blob": "d93e67ca7628bf5531ae6e369da4dd7b7907b88f", + "sha256": "273e81f176f001684b1fa3eb857992bf58b54748004fcfe806b83adb48d2cc00" + }, + { + "local_path": "vendor/machine.py", + "repository": "CubeJerry/integer-mult-bounds", + "commit": "ab239cb6ee884e7a900dd9101c34448077fad0b0", + "original_path": "research/compiled-owned-bank-lifecycle/machine.py", + "bytes": 14932, + "git_blob": "acf475e4fccaff2fb64bd5b0b3f3fc0d246dc592", + "sha256": "ec597bce13275003ff30e4be481c936401826c1d4af642b55eec0c410774d1df" + }, + { + "local_path": "vendor/exact_scalar_tables.py", + "repository": "CubeJerry/integer-mult-bounds", + "commit": "13193a22b1070a74a8580c5d3ea27470443f815a", + "original_path": "research/current-scalar-flat-tables/tables.py", + "bytes": 12650, + "git_blob": "1cc22f75fbe53d48b84be42782e581c04820cd49", + "sha256": "654e9734ef80a9394807ca508543b1bc164afb5768d23d0e5a88c790d2f13bac" + }, + { + "local_path": "reference/PRECISION-PROOF.md", + "repository": "CubeJerry/integer-mult-bounds", + "commit": "56bc9383594a3efc303148e00bb746851abd1ed5", + "original_path": "research/query-only-precision-envelope/PROOF.md", + "bytes": 26757, + "git_blob": "465a5dddd83bdea5db09f1030f99dffe698fe600", + "sha256": "8ddafd9a4c5b51d4c0e3f9b4a9eba27712335a16de1868ba156557344af86e63" + }, + { + "local_path": "vendor/physical_fixture.py", + "repository": "CubeJerry/integer-mult-bounds", + "commit": "6476455a1cf7cd29d6a2a81c3b6f02fd3a3bbf57", + "upstream_path": "research/current-rounded-scalar-tables/physical.py", + "bytes": 6183, + "sha256": "b0eb6f2db2deff9104cdf786a8ae84b0d4864b09a1f9b99178cb08c1666d014e", + "git_blob": "027b563887fd748438d0d0dc7a75f356b29986bd" + }, + { + "local_path": "reference/ROUNDED-SCALAR-PROOF.md", + "repository": "CubeJerry/integer-mult-bounds", + "commit": "6476455a1cf7cd29d6a2a81c3b6f02fd3a3bbf57", + "upstream_path": "research/current-rounded-scalar-tables/PROOF.md", + "bytes": 17726, + "sha256": "ebf8634a004ef9371831171ae5ed1bcbe55e9c2931b56d8113556f27f8ded830", + "git_blob": "498145c6ac72b3c2ef7a0adf166570f4073b68ca" + } + ] +} diff --git a/research/compact-rounded-add/HISTORY.json b/research/compact-rounded-add/HISTORY.json new file mode 100644 index 0000000000..eb593de2d6 --- /dev/null +++ b/research/compact-rounded-add/HISTORY.json @@ -0,0 +1,65 @@ +{ + "failed_work_reused": true, + "failure_scope": "public field unchanged; heads and private scratch may remain dirty/repositioned", + "history": [ + { + "actions": 552506, + "bound": 6250268, + "components": 8, + "historical_backing": [ + 4500, + 6000 + ], + "old_backing": 10500, + "table_rows": 89988, + "width": 19 + }, + { + "actions": 50798, + "bound": 999424, + "components": 2, + "historical_backing": [ + 4500, + 6000 + ], + "old_backing": 0, + "table_rows": 10436, + "width": 2 + }, + { + "actions": 158348, + "bound": 2441216, + "components": 4, + "historical_backing": [ + 4500, + 6000 + ], + "old_backing": 0, + "table_rows": 30800, + "width": 9 + }, + { + "actions": 46738, + "bound": 966656, + "components": 2, + "historical_backing": [ + 4500, + 6000 + ], + "old_backing": 0, + "table_rows": 9726, + "width": 1 + } + ], + "late_failure_public_unchanged": true, + "malformed_controls": [ + "empty", + "odd_record", + "empty_component", + "foreign_symbol", + "unterminated", + "unequal_shapes" + ], + "preserved_contexts": 3, + "signed_equal_distinct_sources": true +} diff --git a/research/compact-rounded-add/OVERLAP.md b/research/compact-rounded-add/OVERLAP.md new file mode 100644 index 0000000000..80d9fc4fa4 --- /dev/null +++ b/research/compact-rounded-add/OVERLAP.md @@ -0,0 +1,44 @@ +# Bounded predecessor and freshness review + +Canonical source: `7c49fe32c55de02c2c873655c804b16e4c3fef0a`. +This targeted review does not establish absence of all earlier related work. + +* `research/current-rounded-scalar-tables` at CubeJerry public + `6476455a1cf7cd29d6a2a81c3b6f02fd3a3bbf57` already proves literal fixed-q + SCALE/ADD by direct carry, builds the 52-SCALE class, and explicitly leaves + large ADD numerical carry graphs and full source inventory open. We reuse + its unchanged physical fixture and lifecycle, and replace the numerator + stage with coefficient-bit Horner passes and a new two-bank marker layout. +* `upstream/build/sections/02-streams.tex`, full-file Git blob + `088fceea1867abc76271d7efe7532b779fee9039`, supplies signed linear stream + arithmetic, fixed power-of-two operations, guard bits and charged reversals. + The reviewed excerpt was lines185..215; we do not present an excerpt's + hash as that full-file blob or claim a newly invented arithmetic principle. +* `research/rank7-one-carry-scalars/README.md`, blob + `0a15051fa99b1e7e8af27a1169583fc0691654ef`, NickPetalas/#3094, uses one + clean Boolean carry for selected dyadic/sign ADD circuits with borrowed + source restoration. Its circuit model is distinct from this sequential + numeric numerator/division table; it remains credited. +* `research/scalar-fused-dyadic/README.md`, blob + `87ff8713a47320af0157146c5f3b5a4fb85c1085`, optimizes host rational/bitplane + audit normalization, not this literal lifecycle primitive. +* `research/gaussian-scalar-backend-audit/README.md`, blob + `35d8acdec29207a95dca69f1403c70acd9a307fc`, is an offline interval oracle + and explicitly not the required physical coefficient producer. +* `research/copy-floor-arithmetic/README.md`, blob + `5ba5198aa4496d88df88902624a2ab39569d2ad6`, concerns source COPY/rank + arithmetic, not a rounded binary payload codec. +* DreamingOfClouds' #6937 total RDiv automaton is already credited by the + rounded-scalar predecessor. Our claim is not first existence of total + fixed-rational rounded division. + +The source census/source witnesses retain #6936 head +`03626137d0bd57f09b0bf9597376183ce6fa9683`. The lead's exact 20:11 UTC +refresh reports head `d360b1182b6d21b1ee2354856abcb50646ad618b`, whose +only delta is the VERIFY.json timeout, with unchanged actual word/claims. +#6937 remains `a98df73ddae1d1ea85a62b6bdf2714b28cb7b359`. + +Allocation is complementary to the native worker's variable-g rounded +positive leaf. This package has a fixed coefficient and fixed d per table; +it does not implement a runtime-variable shift, divisor or leaf header. +The lead's three-QUERY rank lower bound is likewise a different claim. diff --git a/research/compact-rounded-add/PR-DESCRIPTION.md b/research/compact-rounded-add/PR-DESCRIPTION.md new file mode 100644 index 0000000000..1bf11860c6 --- /dev/null +++ b/research/compact-rounded-add/PR-DESCRIPTION.md @@ -0,0 +1,106 @@ +## Summary + +The literal rounded scalar predecessor leaves the current large-numerator +ADD class unbuilt because its direct carry graph grows with numerical +coefficient size. This package supplies a compact two-bank fixed-rational +ADD table, an all-size signed/cancellation/lifecycle proof, and three exact +current source witnesses. **No new kappa and no complete caller admission.** + +For fixed reduced q=a/b, b=2^d o, L=max(bitlength|a|,bitlength b), K=L+2, +the table forms the signed widened numerator b*x+a*y+floor(b/2) by L +binary Horner passes. Each pass has carry bounded by 4. A signed residue +scan, exact odd quotient and low-bit discard implement total nearest-up +rounding. The graph has O(LK+o²+Ko) states/rows, with the explicit current +restriction o<=125. This is not a logarithmic-size arbitrary-divisor claim. + +The complete sum is checked after division, preserving cancellation even +when the separate product exceeds the public width. Per-component numerator +markers provide rewind geometry, so the service needs exactly the existing +two private work roles. All components are staged before public installation. + +## Exact result and source pins + +Canonical parent: `7c49fe32c55de02c2c873655c804b16e4c3fef0a`. + +The source is DreamingOfClouds' CrocSwap/integer-mult-bounds#6936 at tested +head `03626137d0bd57f09b0bf9597376183ce6fa9683`. Its later +`d360b1182b6d21b1ee2354856abcb50646ad618b` changes only VERIFY.json timeout; +the tested word pin remains unchanged. Six immutable dependencies have +exact commit/path/Git-blob/SHA-256 receipts in `DEPENDENCIES.json`. + +The current coefficient census contains 61,052 ADD and one COPY event, +4,462 reduced coefficients, L<=24 and o<=125. Only three exact local ADD +tokens are constructed and registered: + +| Event | Coefficient | Rows | Actual cancellation check | +|---|---|---:|---| +| 252 | -14729531/163840 | 100,033 | W8: 100 + Round(q·2) = -80 | +| 1103 | -1379/250 | 187,806 | W4: 7 + Round(q·2) = -4 | +| 2798 | 1085645/393216 | 76,560 | W4: -7 + Round(q·3) = 1 | + +These represent the largest coefficient, odd denominator and denominator +two-adic power. The old direct carry bound at 252 would be 14,975,296; +that large graph is not instantiated. COPY's caller zero-target contract +is not inferred from generic ADD and no COPY token is installed here. + +## Complete primitive bill and limits + +For R components, S=sum(w_i+1), U=1+S+(K+1)R, initial contiguous dirty +lengths A_N,A_O and borrowed context charge Q_c, the proof gives + + 512(L+8)U + 7(A_N+A_O) + 16Q_c + +for physical tape actions plus executed control rows. Every source reread, +reversal, widening, staging, copying, head reset and retirement is retained. +Historical private backing is max(H_N,3U)+max(H_O,3S), plus inherited +public/context/ancestor and finite-controller storage. Positive finite +coefficient/table/source setup is separate. No exchange rate to an old +supplier tariff or optimistic rounded-scan margin is asserted. + +Canonical encoding, matched common-grid shapes, physically distinct tapes, +public origin heads and contiguous old private bodies are explicit premises. +Successful calls preserve source/contexts, restore heads and retire private +history. Detected failure before installation protects the whole public +field but may leave work and heads dirty. This is an actual unchanged +`Controller.primitive`/`execute_table` service, not host arithmetic on +runtime payloads, but it does not execute the complete recursive Controller. + +## Reproduction and verification + +```bash +python3 -I -B research/compact-rounded-add/verify.py --suite all +python3 -I -O -B research/compact-rounded-add/verify.py --suite all +``` + +Expected: four PASS_COMPACT_ROUNDED_ADD_* lines. Registered attempts have +120-second caps; standard library only and no runtime Git/network/solver. +The independent direct-floor oracle covers 1,952 exhaustive pairs plus +signed endpoints and W0, and write b=2^d o with o odd. This package +supports o<=125. Let L=max(bitlength(|a|),bitlength(b)) and K=L+2. The +constructor `compile_compact(a/b)` emits a fixed finite flat table, before +runtime numerical inputs are supplied. Its four coded ports are ordered +(target, source, numerator work, staged-output work). It uses only the +unchanged executor's branch, write, unit move, goto, halt and reject rows. + +For every positive even number R of components, every matching sequence of +positive signed widths w_i, every common grid 2^-F, and arbitrary independent +signed integers x_i,y_i in those widths, the service succeeds exactly when + + z_i = x_i + floor((a*y_i + floor(b/2))/b) + +fits the original signed width for every i. On success it installs the z_i, +preserves the complete source and borrowed contexts, restores all local heads, +and erases the current and previously used private bodies. This quantifies +all widths and component/column multiplicities. No condition that a*y_i or +its rounded quotient separately fits the public width is imposed. + +The four data tapes and any context tapes are physically distinct. Public +numeric bodies use canonical three-bit codes for little-endian two's-complement +bits 0/1 and delimiter 2, and end at an actual physical blank. Component +boundaries match. Public heads begin at their local origins. Work heads may +start anywhere from their origins through their contiguous old binary body +frontiers. No hidden old nonblank cells may lie after a blank frontier. +All bodies are behind protected local LEFT markers and ancestor backing. +Contexts are read-only binary bodies with confined starting heads. The +common grid, tape distinctness and canonical physical frontier are admission +premises; this table is not a universal decoder for arbitrary corrupt codes. + +On detected shape, grammar or final-range failure, no public cell has yet +been written. Work and heads may remain dirty or displaced; there is no +failure cleanup or automatic public-head restoration claim. A subsequent +call may retire failed private work after its public heads are re-established. + +The unchanged lifecycle implementation is public commit +`ab239cb6ee884e7a900dd9101c34448077fad0b0`, +`research/compiled-owned-bank-lifecycle/machine.py`. The immutable physical +fixture comes from rounded scalar commit +`6476455a1cf7cd29d6a2a81c3b6f02fd3a3bbf57`. The exact scalar Builder is +`13193a22b1070a74a8580c5d3ea27470443f815a`. `DEPENDENCIES.json` pins every +vendored byte by origin commit/path, Git blob, SHA-256 and length. Only the +Builder is reused from the exact scalar constructor; runtime carries and +passes below are newly emitted. The proof does not assume a host arithmetic +callback for the payload or a modified executor. + +The source witness is DreamingOfClouds' #6936 word at +`03626137d0bd57f09b0bf9597376183ce6fa9683`, Git blob +`d93e67ca7628bf5531ae6e369da4dd7b7907b88f`, SHA-256 +`273e81f176f001684b1fa3eb857992bf58b54748004fcfe806b83adb48d2cc00`. +It has 71,144 events. The coefficient census contains 61,052 ADD events +and one COPY (`COPY,1485,770,1,115`), collectively 4,462 reduced coefficients, L<=24 and o<=125. The three actual constructed +source tokens are `(local, pc, original_event)` for pc 252, 1103, 2798, +with ordered target/source indices retained in `SOURCE.json`. All three +are ADD. The coefficient census does not install COPY or transfer its +caller zero-target contract from a generic ADD theorem. +This is a finite three-occurrence registry, not an installed full recursive +caller or construction of all 4,462 coefficient tables. + +## 2. Widened Horner numerator, with cancellation retained + +Consider one width W component. Put M=W+K, and let A=2^(W-1). The private +numerator begins at zero. Read the fixed coefficients' bits from most +significant to least significant, padding both to L bits. If beta_i is the +bit of b and alpha_i is the bit of |a| multiplied by sign(a), perform + + N <- 2N + beta_i*x + alpha_i*y. + +After j passes, N=B_j*x+A_j*y, where B_j and A_j are the corresponding +binary prefixes. In particular 0<=B_j<=b, |A_j|<=|a|, and the signs of A_j +are consistent with a. Therefore every prefix satisfies + + |N| <= (b+|a|) A < 2^(W+L). + +The final offset c=floor(b/2)<2^(L-1) gives + + |b*x+a*y+c| < 2^(W+L)+2^(L-1) < 2^(W+L+1)=2^(M-1) + +for W>=1. Thus all prefixes and the offset result fit width M. K=L+2 is a +uniform sufficient extra width; the proof does not assert it is minimal. +For a=0 the same construction works. No separate same-width multiplication, +negation of a most-negative public input, or premature product-range guard +appears. This is why large terms that cancel remain admitted. + +Each Horner pass is in place on N and uses a bounded finite carry k. For +old numerator bit n and public bits x_bit,y_bit set + + v = 2n + beta*x_bit + alpha*y_bit + k, + z = v mod 2, k' = floor(v/2). + +The table writes z over n after reading n. The preceding old bits are no +longer needed: the recurrence carries exactly their contribution. Starting +at k=0, [-4,4] is closed because n,x_bit,y_bit are bits, beta in {0,1}, and +alpha in {-1,0,1}. This constant carry range is independent of the numerical +magnitude of a and b. Some constructed source tables use only [-2,2]. + +After W public bits, the public heads stay at their delimiters. Their last +bits sx,sy are retained in finite control and supplied for the K high +numerator positions. This is signed extension, including W=1 and a +most-negative source. Let sn be the old numerator's final bit and sz the +new final bit. Summing the bit recurrence with powers of two shows that +width-M signed arithmetic is exact precisely when + + k_M = 2sn + beta*sx + alpha*sy - sz. + +Indeed, replacing unsigned values by signed values adds their sign times +2^M, and the telescoping carry contributes k_M*2^M. The guard is both +necessary and sufficient. The preceding range proof guarantees it on +admitted inputs at every Horner prefix. It is never a guard on a separate +public-width product. + +A further in-place binary pass adds c. Its fixed coefficient bit index caps +at L, after which all offset bits are zero; M>=L+3. With v=n+c_bit+k and +z=v mod2, k'=floor(v/2), its signed terminal guard is k_M=sn-sz. Its carry +is bounded independently of a. The result is exactly N=b*x+a*y+c. + +## 3. Two banks, markers and all rewinds + +The numerator work tape contains a global logical marker 5, followed for +each component by logical marker 6, its M numerator bits, and delimiter 2. +The output work tape holds just W output bits and delimiter 2. Encoded +logical 6 is three nonblank physical bits and cannot prematurely stop +physical retirement. No third guide bank is allocated. + +Initialization scans the matched public component, creates W zero bits, +then adds K zero high bits while the public heads stay at delimiters. To +return for another Horner pass, the table moves numerator left K times +from its delimiter, then repeatedly moves left across a numerator bit and +moves both public heads left once. Encountering marker 6 ends the rewind; +the numerator head moves right once. Thus all three heads are at their +current first bits, including W=1, and no head crosses its local origin. +K is fixed in the table. Each later Horner pass uses this same rewind. + +The offset and residue passes do not move public heads. Their numerator-only +rewinds move left until marker 6 and then right. Neither this marker nor +any input-dependent length is examined by host code. At the quotient end, +all public heads are at their component delimiters and N at its delimiter; +advancing these heads and the output head starts the next component. +Finite parity/seen flags require a nonempty even component count. + +After every component has passed its range checks, the heads are at the +field frontiers. A reverse numerator scan recognizes each delimiter 2, +moves the two public heads and output head left once over their delimiter, +skips K numerator high bits, and moves the other heads left once for each +of the W remaining bits. It ignores marker 6 and continues to the previous +component. The global marker 5 terminates this procedure exactly at all +public/output origins, leaving the numerator at its origin. This works +without a runtime width counter and permits different matching widths in +different components. + +Only now does the output-to-target copy run. It copies coded bits and +delimiters to the target without changing the source. No branch before +this copy writes the target. Well-formed staged output has exactly the +public extent, so the target physical frontier is reached simultaneously. +The unchanged executor resets all data/context heads, and unchanged +`Controller.primitive` retires both private banks on successful return. + +## 4. Signed residue, exact odd quotient and final admission + +To divide the signed M-bit numerator, first compute its residue r modulo o. +For o>1, a least-significant-bit scan retains rho and power modulo o, +starting at 0 and 1. Each bit n contributes n*power; then power doubles. +At the terminal sign bit s, the unsigned value U differs from N by s*2^M. +The correct residue is therefore + + r = (rho - s*power) mod o = N mod o, 0<=r=1, +Q=(N-r)/o=floor(N/o) already fits signed width M. + +The first d quotient bits are discarded, without moving public or output +heads. The next W bits are staged, advancing the two public heads over +W input positions. The remaining K-d quotient bits must all equal the +last staged sign bit sz, and the final carry must satisfy k_M=s-o*sz. +Since d<=L-1, K-d>=3; these counts remain valid even when W=6 positions. The quotient's ordinary +staged positions use at most 59, while drop/high positions use at most 17. +These counts include reverse traversal and no unmetered data access. + +For `retire`, starting at displacement p<=A, the first origin scan costs +2p+3, the erase scan costs 3A+1, and its return costs 2A+3. Thus entry +retirement costs at most 7A+7 per old bank. After the service, the bodies +are contiguous and current lengths are at most 3U,3S. Origin scans and +exit retirement are covered above. The fixed entry/exit rows and constants +are absorbed because U>=1. A conservative combined bound is + + 512 (L+8) U + 7(A_N+A_O) + 16Q_c. + +This retains all L rereads, every marker, widening, copying, head return, +entry and exit erasure, finite control, and old dirty backing. On detected +failure before installation, execution is a prefix of these passes and +uses no more than the same bound, but omits success cleanup. The bound is +not identified with any earlier one-unit linear primitive tariff. + +If H_N,H_O are already allocated historical private capacities, the new +private physical backing is bounded by + + max(H_N,3U) + max(H_O,3S), + +not merely the currently nonblank bytes. Add the unchanged public/source, +context, ancestor and controller backing. Retirement turns old cells blank; +it does not reclaim or forget their historical capacity. Repeated calls +sum their positive costs and keep the maximum widths/extents of each bank. +No arbitrary workspace is silently restored by destruction: these two +roles are explicitly owned scratch authorized for retirement by the +retained primitive interface. + +## 6. Finite construction size and actual source coverage + +There are O(LK) Horner/high/reset states: carry and signs have constant +ranges, with fixed coefficient index and fixed high-bit count. Offset +states contribute O(L), residue states O(o^2), and quotient/drop/high states +O(Ko), since d240 seconds; word and claims unchanged, per lead targeted GitHub refresh 2026-11-09 20:11 UTC.", + "rounded_scalar_predecessor": "6476455a1cf7cd29d6a2a81c3b6f02fd3a3bbf57", + "precision_predecessor": "56bc9383594a3efc303148e00bb746851abd1ed5", + "scope": "Three source-token graphs and generic fixed-coefficient theorem; no whole caller/cap/kappa claim", + "all_sources_local_authentication": "DEPENDENCIES.json" +} diff --git a/research/compact-rounded-add/README.md b/research/compact-rounded-add/README.md new file mode 100644 index 0000000000..e10734f0b2 --- /dev/null +++ b/research/compact-rounded-add/README.md @@ -0,0 +1,110 @@ +# Compact literal rounded ADD for current large coefficients + +**Result:** a two-private-bank flat table computes total nearest-up rounded +ADD with a controller graph of size `O(LK+o^2+Ko)`, where `L` is coefficient +bit length, `K=L+2`, and `o<=125` is the fixed odd denominator part. It forms +the complete widened numerator before dividing, so valid cancellation is +preserved. The table runs through the unchanged lifecycle executor and +retains all copying, reversals, old backing and retirement costs. +**No new kappa or complete caller admission.** + +The current #6936 source has 61,052 ADD events and one COPY, 4,462 reduced +coefficients, `L<=24`, and `o<=125`. We construct and register three exact +local source witnesses, representing the largest numerical coefficient, +largest odd divisor, and largest denominator power of two. We do not +instantiate or install the complete catalogue or infer COPY's caller +zero-target contract from ADD arithmetic. + +| Source event | Coefficient | Flat rows | Cancellation witness | +|---|---|---:|---| +| 252 | -14729531/163840 | 100,033 | W8: 100 + Round(q·2) = -80 | +| 1103 | -1379/250 | 187,806 | W4: 7 + Round(q·2) = -4 | +| 2798 | 1085645/393216 | 76,560 | W4: -7 + Round(q·3) = 1 | + +In each example the separate rounded product would overflow the public +width. The old direct-carry bound at event252 is 14,975,296; that graph +is never constructed. The new Horner carry is bounded by 4 independently +of coefficient magnitude. The explicit `o^2` term is retained: this is not +a logarithmic-size arbitrary-divisor result. + +## Scope and physical contract + +`compile_compact(q)` emits immutable branch/write/unit-move/goto/halt/reject +rows for `(target, source, numerator_work, output_work)`. Fixed coefficient +bits determine successive `N <- 2N + beta*x + alpha*y` passes at width +`W+K`, followed by the rounding offset, a signed residue scan, exact odd +quotient and low-bit discard. Per-component numerator markers also guide +rewinds, so only two owned work banks are used. + +For all positive widths and all complete fields with matching component +shapes on a common grid, success is exactly final signed representability. +Every component is staged before any target write. The source and contexts +are preserved and successful heads returned; both private historical bodies +are retired. Detected failure before installation protects the public +field but may leave heads and private work dirty. Canonical actual physical +frontiers, distinct tapes, origin markers, and contiguous old scratch are +explicit premises. + +Put `S=sum(w_i+1)`, `U=1+S+(K+1)R`, with `R` components. Including finite +control and physical tape actions, the positive per-invocation bound is + + 512(L+8)U + 7(A_N+A_O) + 16Q_c. + +`A_N,A_O` are old contiguous dirty physical lengths. Historical capacities, +source/table setup and all ancestor/public backing remain charged separately. +This bound is not converted into the previous supplier tariff or optimistic +rounded-scan margin. + +## Reproduction + +```bash +python3 -I -B research/compact-rounded-add/verify.py --suite all +python3 -I -O -B research/compact-rounded-add/verify.py --suite all +``` + +Expected: four `PASS_COMPACT_ROUNDED_ADD_*` lines, for SOURCE, ARITHMETIC, +HISTORY and CONTROLS. Every registered attempt has a 120-second limit; +standard library only, with no Git, network or solver needed for replay. + +The independent direct-floor oracle checks 1,952 exhaustive pairs plus +endpoints, including W=1`, `p,h>=0` be integers, with one common component grid +`Delta=2^-F`. Every real and imaginary component of every arbitrary public +input is on this grid and has absolute value less than `2^h` at the stated +raw/root boundary. Owned INIT produces exact zero. Public inputs include +every helper, independently; no correlation or cancellation is assumed. +For the outer-wrapper extension below, D is the total selected factor +`D=q+R`: the q preprocessed coordinates and the remaining reference factor +R. Establishing the input p,h domain at the chosen external boundary is +separately paid. The q kernels must precede the later R-fibre computation, +as stipulated by the retained wrapper contract; the proof converts once +from the D-fibre norm to the R-fibre norm in the safe direction. + +For a selected set of `X` binary coordinates use the supremum, over complete +`X`-fibres, of the Euclidean norm on that fibre's `2^X` complex entries. +Write this as `||z||_X`. For complete nested factors, `||z||_R<=||z||_D` when +`R` is contained in `D`. If every component has error at most `Delta/2`, +then the error in this norm is at most + + eta_X = 2^((X-1)/2) Delta. + +An input with the component bound above has fibre norm less than + + B_root = 2^(h+(D+1)/2). + +The norm contracts are explicit: + +* Each completed native frame change, Q query and D-mask job is the intended + complete-fibre unitary, with the absolute phases and column multiplicities + required by the inherited source. This is a semantic premise, not a + consequence of the finite frame-span check. +* Q and the D_j commute where the frozen exact endpoint uses that identity, + and `Q^4=I`. Therefore + + Lambda_s = ((1+s i) I + (1-s i) Q^2)/2, s in {-1,+1}, + + is unitary: the unitary involution Q^2 has eigenvalues ±1, and Lambda_s + has eigenvalues 1 and s i. In particular it is not `(I+Q^2)/2`. +* A completed primitive with ideal map T has a **total** contract on every + input in its declared grid/radius domain: it returns a grid value differing + from T of that actual input by at most its declared epsilon. The contract + may be nonlinear and its residual may depend adversarially on the input. + It must cover actual inputs to each recursive child, not just ideal ones. +* Scalar rounding, when invoked, is the total function + + RDiv_(a/b)(m) = floor((a m + floor(b/2))/b), gcd(a,b)=1, b>0. + + Its scalar residual has absolute value at most 1/2. Integer coefficients + are exact. For ADD, round the product and then add the old target exactly; + equivalently add the integer `b*old_target` inside the numerator. Negative + values use mathematical floor. Upward ties mean RDiv is not an odd map. +* Lambda needs its own completed primitive with residual at most eta_X, + for example exact formation of its common denominator-two numerator + followed by one rounding per component, with an exact Q^2 monomial + service. This is an explicit contract; no such physical table is installed + here. An implementation which rounds twice must supply the resulting + larger residual instead. + +For the local estimates take `epsilon>=eta_X`, and bound each completed +child, QUERY, IDLE and Lambda residual by epsilon. Arithmetic and native +operations must run to their completed source cut before another field +reads them. No assertion that partially constructed Clifford outputs are +Clifford vectors is used. Scalar numerator temporaries are handled separately +in section 6; arbitrary internals of a native provider are inherited +obligations, not unnamed source cuts certified by this package. + +**Why this is uniform in column multiplicity.** Tensor products of unitary +complete-fibre maps have norm one. Rational scalar coefficients are applied +once and are not raised to a tensor power. The only dimension factor is the +single conversion `eta_X` at a componentwise rounding site. These facts hold +for every positive column multiplicity under the complete-fibre premise. +Coordinate supremum norms do not have this property: the exact Gaussian row +`((1+i)/2,(1-i)/2)` sends `(1,i)` to `1+i`, of modulus sqrt(2). A phase error +may preserve norm one, so a norm certificate cannot certify native phase +correctness. + +## 3. Native prefix and suffix certificate + +For each live native register r carry two nonnegative rational numbers +`m_r,e_r`. Initially m=1 on every public input and m=0 on owned labels; +e=0 everywhere. At each source event use: + +| Source event | Mass update | Defect update | +|---|---|---| +| MOVE r | m_r unchanged | e_r <- e_r+1 | +| ADD/COPY r,s,q | m_r <- m_r+abs(q)m_s | e_r <- e_r+abs(q)e_s+1_(q noninteger) | +| SCALE r,q | m_r <- abs(q)m_r | e_r <- abs(q)e_r+1_(q noninteger) | +| INIT/CLEAR r | m_r <- 0 | e_r <- 0 | + +COPY in this source is additive COPY into freshly initialized zero. The +checker proves that source precondition. It does not erase an arbitrary +target's earlier residual by fiat. Register frames agree at scalar contacts; +each MOVE starts at its declared current frame and uses the declared public +or owned direction. A separate exact span/lifetime scan checks all of these +syntactic premises and the final public frame list. + +By chronological induction, at every source cut the exact ideal value has +norm at most `m_r B`, and the realized-minus-ideal value has norm at most +`e_r epsilon`, for input norms at most B. MOVE preserves norms by the stated +unitary contract. ADD and SCALE use the triangle inequality. INIT/CLEAR kill +all earlier error channels. Also track the product `abs(q)m_s` and its defect +bound before every ADD/COPY; rounded product residuals are bounded by the +corresponding final target bound, whose other summands are nonnegative. + +This positive propagation deliberately forgets all cancellations. It is a +valid, loose bound rather than a claim that these extrema are attained by a +choice of actual unitary inputs. In particular the large constants below do +not contradict the smaller cancellation-aware exact-grid row estimates. + +The exact rational scan of all 71,144 events gives: + +| Bound | Meaning | Strict bound | +|---|---|---:| +| M_W | all stored fields and pre-ADD products | 2^237 | +| Sigma_W | all-cut propagated unit residual mass | 2^235 | +| Gamma_W | returned public residual mass | 2^235 | + +The maximum prefix is register 1443 after event 71119; the returned defect +maximum is the same register after the whole word. `ENVELOPES.json` records +the exact rational values and witnesses, not floating logarithms. There are +6,323 MOVE sites and 25,923 noninteger scalar sites, including 4,143 odd +scalar divisions. There is no multiplication by the number of public fields +because the contract takes a maximum over fields. + +**Separate critical check.** `native_adjoint` starts a covector at each +reported maximum and runs the transpose recurrence backwards. Reverse ADD +adds `abs(q)*lambda_target` to the source covector; reverse SCALE multiplies +its covector; reverse INIT/CLEAR zeros it. A residual site contributes the +current target covector. The sum on initial public inputs reproduces M_W, +and the sum on residual sites reproduces Sigma_W/Gamma_W. There are 24,507 +nonzero residual-site contributions at the worst witness. This is a +separately coded reverse calculation, not an independent physical execution +or formal proof-kernel check. The forward induction is the mathematical +reason a finite exact source scan proves a statement about all inputs. + +## 4. Full caller and every expanded native cut + +Caller scalar operations use the same positive recurrence. SWAP permutes the +two pairs of bounds. LAMBDA and IDLE leave mass unchanged and add one unit +of residual. QUERY adds the source mass/error to the target and adds one +residual. This uses the complete query contract, including restoration; +it does not treat the query copy/erase lifecycle as free. + +For a J contact, the frozen exact local endpoint on the six symbolic main +roles is, with unitary factors suppressed in the positive bound, + + A: (u,v,x,y) -> (u, v+Q^-1 u, x-Q y, y), then D_j; + B: (s,t) -> (s-Q t, (Q^-1 s+t)/2), then D_j. + +Use the positive endpoint matrix + + (u,v,x,y,s,t) -> (u, v+u, x+y, y, s+t, (s+t)/2) + +on old mass/error values simultaneously, then add Gamma_W to each returned +main's defect coefficient. Helpers return their own unitary-transformed +input plus at most Gamma_W epsilon. Each helper family belongs to exactly +one joint stage, so it starts with mass bound 1 and no prior raw-caller +defect. This does not identify distinct helpers or suppose they vanish. + +At that J entrance let `m_in=max(1, the six main mass bounds)` and +`e_in=max(the six main defect bounds)`. Every internal native cut obeys + + ideal norm <= M_W m_in B; + defect norm <= (M_W e_in + Sigma_W) epsilon. + +These inequalities include prior caller errors arriving at a native call; +restarting the native word with zero error on its mains would be invalid. +They also include all fresh arbitrary helper inputs. The source scan checks +J stages 1 through 18 in order, type-local six-role bindings and 400 actual +main fields/1,061 helper fields at each contact. + +For the actual 3,095-event caller, the results are: + +| Bound | Strict bound | +|---|---:| +| Caller-only mass | 2^121 | +| Caller-only all-cut defect coefficient | 2^342 | +| Largest J entrance mass | 2^119 | +| Largest J entrance defect coefficient | 2^340 | +| **M_ctx**, including native interior products | **2^355** | +| **Sigma_ctx**, including native interior products | **2^576** | +| **Gamma_ctx**, all returned public fields | **2^337** | + +The worst J entrance is stage 18, caller event 2958. The caller-only peak is +role 38 at event 3049; the final defect maximum is role 75. Full exact +fractions, cuts and separate caller-adjoint identities are in the receipt. +The reverse J rule adds `sum(lambda_r)*Gamma_W` and transposes the six-role +positive endpoint matrix. It independently reproduces the caller peak, +entrance and final coefficients, separating J residuals from primitive +residuals. No old 67,079-event or previous-caller constant is reused. + +Thus this concrete expanded raw context has the all-input contract + + output defect <= Gamma_ctx epsilon; + every certified source cut <= M_ctx B + Sigma_ctx epsilon. + +The statement is uniform for all positive columns under section 2's operator +and completion premises. It is not a physical tape execution of the caller. + +## 5. Retained recursive precision guard, explicitly conditional + +This section proves a replacement-constant implication for the structural +organization S1--S5 of the pinned rounded note. It does **not** independently +establish those compiler, whole-job, ownership or normalization premises. +In particular retain the following: at most K_star unfinished raw contexts +per ordinary level; at most ell ordinary levels; at most K_star/v flow +classes; at most m(H+1) two-job frames; complete sequential splitting and +completion on disjoint axes with norm-one suffixes; a rank-e sequential base +with e=1, using `ell<=D/N`. + +The inherited split/completion sizes have `R<=153^v`, `J=11^v`, `L=12^v`. +Exactly, + + (R/J+1)(L/J+2) < 2^(6v). + +For example `(153/11)^v+1<2*16^v` and +`(12/11)^v+2<3*2^v`, and `6*32^v<64^v` for v>=3. The verifier also checks +the integer inequality without logarithms. Since Gamma_ctx<2^337, the +per-context equivalent gain after this charge has logarithm less than 343. +The positive noncontext overhead + + m(H+1)+H+log2(m) <= K_star + +follows from the checked stronger bound with `log2(m)<8v`. Since +`log2(M_ctx+1)<356`, the retained path accounting yields + + X(D) = 2 log2(D+3) + 344 t, + L(D) = 1 + 357 t, + E_root <= 2^((D-1)/2 - F + X(D)), + admitted input radius <= B_root * 2^L(D). + +These are convenient strict upper envelopes, not optimal constants. + +**Admission is not circular.** Keep raw contexts as individual nodes in +the defect tree; do not collapse their all-cut coefficients into a silently +larger unreported Sigma. A split/completion node has unitary prefixes and +at most `m+2` sequential child residuals. A frame has two; a base has fewer +than m; a remainder fewer than N. The wrapper, if grouped, has at most D+3. +Therefore for D>=N a valid coarse bound is + + max Sigma_node <= N (D+3). + +This deliberately retains the wrapper's D dependence. A wrapper cannot in +general be bounded by N merely because the local remainder is below N. +For every node the chronological argument is: if earlier child contracts +held, its local error term is at most `Sigma_node E_root`; if this is at +most 1<=B_root, the next child lies in the advertised enlarged radius. +Its total contract applies, allowing the induction to continue. + +Take g=0 for D>=19 and g=5 for 1<=D<19, and set + + F=p+D+g, J=h+D+2, W=F+J+1=p+h+2D+3+g. + +For D>=N, `344t=16, its left side is less +than `4k+7<=2^(k-3)<=D/8`; the elementary integer induction is recorded. +Hence + + X(D)+H+log2(D+3) < D/4 <= (D-1)/2. + +It follows that `E_root*N*(D+3)<=2^(-p-1)<=1`, closing the admission guard, +and in particular `E_root<=2^(-p-1)`. The radius exponent satisfies + + h+(D+1)/2+L(D) < h+D+2 = J, + +so every certified signed component lies strictly inside the W-bit range +on grid 2^-F. + +If ell=0, the retained structure has no raw contexts or upper ordinary +frames; only the sequential base/wrapper estimate remains. The guard is +equivalent to + + (D+3)^4 <= 2^(D+2g-1). + +The verifier checks D=1,...,19 exactly. It continues for D>=19 because +`((D+4)/(D+3))^4<2` there and decreases. The control g=4 at D=3 fails. +Moreover `(D+3)/2<=2^((D+1)/2)`, so the direct sequential stored bound is +at most `2 B_root`, again strictly inside 2^J. This concludes the conditional +common-grid, error and signed-admission implication for all D>=1. + +The output error is a complex-modulus bound because the fibre norm bounds +each coordinate modulus. It does not preserve a strict unit-disk boundary: +the outer shrink/quantizer and analytic recovery changes discussed in the +rounded note still need their own full source and cost admission. + +## 6. Integer temporaries and complete cost boundary + +The actual native source has maximum numerator 14,729,531, at event 252, +and maximum denominator 393,216, at event 2798. It has 864 coefficients +whose numerators exceed 40,864. Thus the old rounded note's 16-bit numerator +premise is false for this source. The new safe bound is + + abs(a)<2^24, b<2^19, temporary signed width W+26. + +Indeed a signed W-bit input has absolute value at most 2^(W-1), so +`abs(a*m)<2^(W+23)`. The rounding offset is below 2^18. Even forming an +ADD numerator `b*target+a*source+floor(b/2)` has absolute value below +`2^(W+25)`, the signed magnitude limit of W+26 bits, with room for sign +extension/carry. Lambda's denominator-two numerator uses fewer such bits. +An output width check is justified by section 5's source-cut bound, not by +merely enlarging its temporary. Variable power-of-two normalization divisors +can be implemented by a bit drop and carry, but their actual service and +schedule remain inherited contracts. + +This width calculation is not a construction of total RDiv on the retained +machine. The existing exact table has different rejection semantics. +The rounded note outlines multiply/offset, a most-significant-first signed +division pass and possible reversals; a literal table must still account +for all those passes, head resets, full source and target access, staging, +restoration, owned allocation/return and erasure of initially dirty and +historically longer backing. Old parked ancestors and simultaneous children +remain live. None of them is removed by a source norm proof. + +An optimistic positive tariff screen is nevertheless useful. Starting from +the published QUERY-only conditional total 826,265,904, keep its 2,734,992 +exact 1125-conversion charge conservatively even though the unscaled rounded +mode does not use it. Declare the additional arithmetic model + + per noninteger a/b: + 4 (bit_length(b)+1) [1 + 3*1_(oddpart(b)>1)]. + +This prices one offset scan at every noninteger scalar and three extra +scans at an odd divisor, in the prior raw tariff's scan unit. It is a +declared model, not a measured physical guarantee. Use it also for outer +caller scalars and once for each denominator-two Lambda offset. The exact +current census is: + +| Positive item | Charge in this declared model | +|---|---:| +| Native surcharge per call | 941,128 | +| All 18 native calls | 16,940,304 | +| Outer scalar offsets at all actual ports | 51,520 | +| Outer Lambda offsets at all actual ports | 173,760 | +| Total extra | 17,165,584 | +| Baseline plus extra | 843,431,488 | +| Remaining below inherited 10^9 cap | 156,568,512 | + +There is no omitted field-replication factor in this **model census**. QUERY +and IDLE completed-child charges are already in the baseline, and the +18 native words, 416 outer QUERY lifetimes, 54 local owned lifetimes per +call and peak 43 local owned banks remain. Their complete positive costs +must remain in an actual implementation invoice. A finite table/code +construction, authenticated source decoding and any denominator setup are +additional fixed-template work, with positive finite constants; they are +not charged as zero by this package. The complete physical runtime has the +form of those fixed setup costs plus the actual full scans and historical +backing terms, each on width W+26. We do not have their certified coefficient +and therefore do **not** infer the cap, recurrence or a new kappa for the +rounded implementation from this optimistic table. + +## 7. An actual source cut where the exact service cannot implement the contract + +The five consecutive zero-based native events are authenticated literally: + + 37476 MOVE 697 1042 -> 591 public + 37477 MOVE 1334 1042 -> 1046 public + 37478 MOVE 901 565 -> 591 public + 37479 SCALE 1334 1/2 frame1046 + 37480 SCALE 697 -2/3 frame591 + +Start all arbitrary public inputs at zero and every earlier primitive +residual at zero. The ideal execution is zero. At the completed MOVE37476, +allow the child to return one quantum Delta in one real component of field +697; all other components and all subsequent child residuals are zero. +This is an allowed format output under a total child contract with +epsilon>=Delta and adequate radius. Such a contract is allowed by the +eta_X model for X>=1. The three intervening events do not access field697. + +At SCALE37480 its numerator is 1. The exact result would have numerator +`-2/3`, which is not an integer. Therefore **for every common grid precision +F**, the retained checked exact SCALE rejects this permitted input. Making +Delta smaller reduces the absolute defect but never removes the +divisibility obstruction. This is a countermodel to an implication from +the abstract rounded-child contract to exact-service admission. It is +**not evidence that a retained MOVE implementation actually produces this +one-quantum defect**. + +The total RDiv alternative returns numerator -1, whose residual is -1/3 +quantum; that is within its half-quantum contract. An exact child, by +contrast, returns zero here and the checked exact scalar succeeds. Thus +the countermodel does not refute the ideal exact-grid theorem or the +S=1125 prefix proof; it locates the extra interface premise needed to move +between exact and rounded modes. + +`boundary.py` compiles the frozen generic `SCALE(-2/3)` finite table and +executes it through the unchanged lifecycle `execute_table`. On widths +3 through 9 it checks zero, ±3, 1, and a late-component `(3,1)` failure: +35 cases, 21 accepts and 14 rejects, with a separate integer +divisibility/range oracle. Rejections leave every public component +unchanged; success restores all heads and erases initially dirty private +work. Rejected work/head positions may be dirty/unrestored: no rollback or +successful caller continuation is claimed. This bounded physical check +tests the existing generic kernel's semantics, not all current native +MOVEs or an installed #6936 occurrence-token binder. + +## 8. Verification, limits and next obligations + +Run `python3 -I -B research/query-only-precision-envelope/verify.py --suite all`. +Expected output is four `PASS_QUERY_ONLY_PRECISION_*` lines followed by +`AUTHENTICATED_SOURCE_FILES 11`. Registered normal and `-O` suites compare +all deterministic receipts. Source guards reject wrong MOVE source/owner, +a dependent frame basis, a public CLEAR, a changed J order and QSELF +reintroduction. Exact norm controls reject coordinate-sup contraction, +the false projector Lambda and omission of the Q^4 premise. A unitary Q +of `(3+4i)/5` gives Lambda squared norm 49/25, so unitarity of Q alone +does not justify the Lambda step. RDiv tie and residual-erasure controls +test other critical distinctions. + +The independent methods here are induction plus exact positive source +propagation, reverse covector checks, exact integer guard inequalities and +a direct integer oracle against an unchanged physical scalar executor. +All were prepared with AI assistance. They are not independent human review +or kernel-checked proofs. A separately supplied lead review, when present, +is recorded with its actual scope and file hashes in `REVIEW.md`. + +Open next questions: + +* Construct and install a total signed RDiv service with the actual source + token/header binding, W+26 temporaries, full lifecycle and historical + backing costs. Checked exact division is not that service. +* Bind all complete-fibre norm/error contracts, including Lambda's chosen + one-rounding semantics and native absolute phases, to literal all-column + providers. A phase error can escape every norm check here. +* Independently discharge the retained compiler S1--S5 and ownership + interfaces, or replace them with verified source-to-physical composition. +* Complete the actual physical tariff and outer shrink/analytic recovery + changes before using a rounded implementation in a complete bound. + +This package closes a source-specific numerical-envelope calculation and +reduces the precision seam to explicit total-service and inherited compiler +premises. It does not claim those premises are established. diff --git a/research/compact-rounded-add/reference/ROUNDED-SCALAR-PROOF.md b/research/compact-rounded-add/reference/ROUNDED-SCALAR-PROOF.md new file mode 100644 index 0000000000..498145c6ac --- /dev/null +++ b/research/compact-rounded-add/reference/ROUNDED-SCALAR-PROOF.md @@ -0,0 +1,329 @@ +# Literal total rounded scalars on the retained lifecycle ABI + +Prepared for **@CubeJerry**, with substantial OpenAI assistance. Canonical +base `7c49fe32c55de02c2c873655c804b16e4c3fef0a`. This is a physical scalar +service lemma and current finite-source binding. **No new kappa, no full +caller admission, and no unconditional multiplication theorem.** + +## 1. Exact scope and predecessor boundary + +The unchanged predecessor scalar compiler is published at +[`13193a22b1070a74a8580c5d3ea27470443f815a`](https://github.com/CubeJerry/integer-mult-bounds/tree/13193a22b1070a74a8580c5d3ea27470443f815a/research/current-scalar-flat-tables). +The unchanged lifecycle `Controller.primitive`, `execute_table`, CodedPort +and retirement code are published at +[`ab239cb6ee884e7a900dd9101c34448077fad0b0`](https://github.com/CubeJerry/integer-mult-bounds/tree/ab239cb6ee884e7a900dd9101c34448077fad0b0/research/compiled-owned-bank-lifecycle). +The old scalar divider is checked **exact** division. Its finite-state +builder is reused unmodified; its quotient transition is replaced, not +relabelled as rounding. + +The concrete word is DreamingOfClouds' +[CrocSwap/integer-mult-bounds#6936](https://github.com/CrocSwap/integer-mult-bounds/pull/6936), +head `03626137d0bd57f09b0bf9597376183ce6fa9683`, 71,144 events. +Its 3,660 SCALE occurrences use 52 fixed rational coefficients. All 52 +tables are constructed and registered under the exact local token +`(local, pc, original_event)`, retaining source position, coefficient, +register and frame. The caller must supply that instruction's ordered +numeric field and the premises below; an entire caller/recursive source +exporter is not installed here. + +DreamingOfClouds' `ROUNDED-DIVISION.md` in +[CrocSwap/integer-mult-bounds#6937](https://github.com/CrocSwap/integer-mult-bounds/pull/6937), +head `a98df73ddae1d1ea85a62b6bdf2714b28cb7b359`, defines nearest-up RDiv, +gives an abstract LSF multiply/MSF odd division construction, and reports +285,870 small automaton cases. It explicitly leaves tape-level recounting +and physical services open. Its sole shipped `check.py`, blob +`cebc2062a3939e5b2e415fe5aa6d3d8ce1d6cdac`, does not contain that +automaton or lifecycle join. Here a signed residue prepass is followed by +an LSF exact odd quotient and low-bit discard, using the existing two work +banks and no new reversal buffer. + +The preceding precision package at +[`56bc9383594a3efc303148e00bb746851abd1ed5`](https://github.com/CubeJerry/integer-mult-bounds/tree/56bc9383594a3efc303148e00bb746851abd1ed5/research/query-only-precision-envelope) +locates a permitted one-grid defect before SCALE37480 by -2/3 that the +exact service rejects. This package closes that arithmetic seam and +constructs the whole current SCALE class. The remaining 4,079 odd ADD +occurrences are not instantiated here. + +Six unchanged files have exact commit/path/blob/SHA-256 pins in +`DEPENDENCIES.json`. Runtime tables contain only branch, write, unit move, +goto, halt and reject. Python arithmetic occurs only in fixed table +construction; there is no runtime payload callback or host division. +These are the proposed RDiv numerical semantics, not the source's +exact-child mode or an unannounced change to the selected rule. + +## 2. All-size theorem and domain + +Fix `a/b` in lowest terms, a integer and b>0, before runtime sizes vary. +Write `b=2^d o`, o odd, and `c=floor(b/2)`. +Define `Round(m)=floor((a*m+c)/b)`. SCALE sends m to Round(m); ADD sends +target x and source y to `x+Round(y)` and preserves the source. ADD shares +the proof; only small ADD coefficients are physically instantiated here. + +The tape premises are: + +* A field has a finite, nonempty even number R of signed components, each + with positive width w_i, LSF two's-complement bits and delimiter2. The + current format specializes to common W. ADD has matching shapes and a + common grid on distinct tapes. Equal values are permitted; physical + target/source alias is outside this contract. +* Numeric symbols0,1,2 use canonical three-nonblank-bit physical codes, + followed by a **physical** BLANK frontier. Encoded virtual4 cannot + masquerade as a frontier. CodedPort identifies those two cases, so this + table is not a validator of arbitrary noncanonical encodings. +* Public and borrowed context heads start at their protected local origins. + Each work head is inside its old contiguous binary body or at its + frontier. All field/work tapes are distinct and mutation is sequential. +* Work may initially be dirty and longer than the new field. Historically + allocated cells beyond its contiguous body must already be blank. + Hidden dirt after a blank is outside the retirement invariant. Protected + parent/ancestor segments stay live and are not scratch. +* The unchanged lifecycle retires both work banks on entry, executes the + table, resets successful heads and retires both banks on success. + +**Theorem.** Every such input terminates and succeeds iff every rounded +output fits its original signed width. Success installs the exact rounded +result, preserves source/context data, restores all heads and blanks both +work bodies, including previously written tails. A detected pre-installation +grammar error or overflow leaves the entire public target unchanged, +including earlier staged components. On rejection, work and heads may be +dirty/unrestored; no automatic rollback or successful continuation is claimed. + +This is total rounding subject to representable output, not an assertion +that every coefficient/input pair fits a fixed output width. + +## 3. Signed residue prepass + +For a w-bit component with bits x_j and sign s, write +`U=sum x_j 2^j`, `m=U-s 2^w`. The prepass keeps finite states + + rho = c + a sum_(j=2 + +For q=-2/3, `Round(m)=floor((-2m+1)/3)`. Put A=2^(W-1). At input -A, +the largest output is `floor((2A+1)/3)`. If W>=2 then A>=2 and +`2A+1<3A`, so this is at most A-1. At the largest input A-1, the result is +`floor((-2A+3)/3)>=-A`. Monotonicity covers every intermediate input. +Thus the table succeeds on every signed W-bit input for every W>=2 and +every finite complete field in the theorem's domain. + +At source SCALE37480 on register697, numerator1 maps to -1, with residual +-1/3 quantum; the old exact table rejected it. W=1 is correctly exceptional: +input -1 would round to +1, outside [-1,0]. Grid precision does not change +this integer statement. + +## 6. Whole-field staging, preservation and history + +No public write occurs during residue measurement, quotient generation, +shape checking or per-component range checks. Candidate components go to +the output bank. A parity state requires a positive even component count +at the frontier; ADD checks input bits, delimiters and frontiers in lockstep. +Only after every component passes does the global unary guide rewind the +inputs and protected output. Installation then copies the validated whole +field to the target. + +Under the geometry premises this installation cannot encounter a new +arithmetic/shape failure: the work streams were generated by the table and +have the consumed target's length. The ADD source is never written. No +table row addresses extra borrowed contexts; the executor only resets their +already-origin heads. Every ancestor remains behind its protected marker. + +Fixtures execute the unchanged `Controller.primitive` method, supplying +the exact attributes it reads. They do not claim a full recursive +Controller constructor, row provider or stack execution. Tables are immutable +tuples, and integer oracles inspect outputs only outside runtime. +Three separate cost fixtures wrap only table lookup in a transparent +counter that returns the unchanged immutable row. It receives no tape or +numerical payload and cannot influence the instruction stream; it counts +control steps alongside the physical Tape observer. + +The executor resets success heads; unchanged retirement erases both +contiguous work bodies. Guide marker6 is encoded as three nonblank physical +bits and cannot hide a suffix from retirement. Older longer tails were +erased at entry and remain blank. Shorter reuse therefore preserves all +historical cells. A rejected run can leave contiguous dirt and an interior +head; a subsequent explicitly started primitive retires it. Rejected public +heads are not automatically restored. + +## 7. Complete positive primitive cost and storage + +Let R be the component count and `S=sum_i(w_i+1)` the numeric virtual +extent of a public field, delimiters included. Let A_0,A_1 be the old +contiguous physical work-body lengths, with heads inside those bodies or +at their frontiers. Let Q_c count untouched borrowed binary contexts at +their origins. Count each physical read, write, unit head move and each +executed flat-table row as one finite-control action. A conservative +complete successful primitive bound is + + 512(S+1) + 64 d R + 7(A_0+A_1) + 16 Q_c. (3) + +Detected pre-installation failures use only a prefix of these phases, for +their scanned extents. This is a bound in stated physical/finite-control +units, not a conversion into the supplier's raw tariff. + +A valid CodedPort nonblank read costs at most 10 physical actions, a write9 +and a unit move4. Every forward move is from a written/data symbol: the +table does not allocate an extra virtual word by moving from a blank +frontier. Including the control row, each instruction costs at most 11. + +| Table phase | Upper bound on executed rows | +|---|---:| +| Arithmetic and delimiter checks | 10 S + 3 d R | +| Odd residue scan and component rewind | 13 S | +| Global guide rewind | 7 S | +| Validated installation | 7 S | +| Fixed entry/frontier/marker branches | 32 | + +The residue phase is absent when o=1. The table therefore costs at most +`407S+33dR+352` including its physical actions. Executor head resets cost +at most `18S+18`. Entry retirement of work bank i costs +`5A_i+2h_i+7<=7A_i+7`, where h_i is its initial displacement. Final +retirement of physical lengths 3S and3(S+1) costs `30S+29`. Their sum is +at most `455S+33dR+413+7(A_0+A_1)`. The remaining allowance in (3) covers +the fixed two-bank/at-most-two-public-port wrapper bookkeeping (at most 64 +control steps under this convention) and context resets. The latter cost 3 +physical actions each plus linear bookkeeping; 16 Q_c is positive slack. +Since R>=2 and w_i>=1, S>=4, so this slack is sufficient. Every source +read, copy, rewind, head return and retirement remains in the bill. + +Runtime output uses at most3S physical cells and guide 3(S+1). No multiply +or reversal array is allocated. The carry is bounded by C and residue/power +by o; those are fixed finite controller states. The generic W+26 numerator +budget from the precision package is compatible but is not a hidden third +array here. If a coefficient or d is itself a runtime variable, this fixed +template theorem does not provide a uniform variable-divisor service. + +If prior backing capacities are H_0,H_1, resident private storage remains + + max(H_0,3S) + max(H_1,3(S+1)), + +in addition to public fields, all borrowed metadata, protected ancestors +and fixed controller storage. For repeated calls i, sum (3) with actual +S_i,R_i and initial dirty lengths A_(j,i). After success these dirty lengths +are zero on the next use; resident capacities still retain historical +maxima. This charges initial dirt/failure leftovers and does not pretend +that an erased longer tail ceases to occupy backing. + +**Construction.** There are at most 2C+1 carry values, finite residue/power +states and phase counters bounded by d. A coarse finite graph bound is a +fixed constant times `(d+1)^2(C+1)+(o+1)^2`, with positive coefficient-bit +arithmetic and label-resolution cost. Authentication, source reading, token +registration, graph construction and storage contribute C_setup independent +of runtime field sizes. They are not priced as zero. + +The instantiated 52-SCALE catalogue has 92,113 rows, at most 20,401 in one +table, with d<=8, o<=15 and C<=278. Only 64 occurrences per local word use +the residue prepass, hence 1,152 in an 18-call raw caller. `SOURCE.json` +records every coefficient and occurrence count. No additional bank is +introduced. + +The previous precision package's optimistic extra-scan margin is not an +admitted exchange rate between (3) and the inherited 10^9 raw tariff. +The complete current ADD class, source/row exporter, other providers, +recursive children, setup and normalization interfaces still need a common +physical invoice. This package makes no tariff-cap or kappa conclusion. + +## 8. Verification and remaining obligations + +The physical oracle computes mathematical integer floor and final signed +range directly, without replaying table transitions. Bounded coverage is: + +* all 52 current SCALE coefficients, all signed inputs at widths 1..5: + 3,224 cases, 1,998 accepts and1,226 correct overflow rejections; +* seven small ADD coefficients, all input pairs at widths 1..4: + 2,380 cases, 1,706 accepts and 674 correct overflow rejections; +* every -2/3 input at widths 2..9:1,020 successes; +* work initially dirty for 1,800 and 2,400 cells, arbitrary interior/frontier + heads, long-to-short reuse, late-component overflow, explicit retirement + after failure including a live residue marker6, three borrowed contexts, + detected malformed grammars and combined table/physical cost samples; +* separately compiled mutants omitting signed residue correction, omitting + the upward rounding offset, and changing the final signed guard. + +Physical attempts have a 120-second cap. The proof, rather than finite +width coverage, establishes universality. Tests do not monkey-patch the +executor/CodedPort or use numerical payload callbacks. The primitive +fixture is not a recursive tape computation or independent human review. + +Open next questions: construct and price uninstantiated current ADD +tables; bind recursive occurrence/row formats; establish the remaining +native/Lambda/error/ownership contracts; and assemble the full physical +tariff and rounded outer recovery. The source precision implication at +56bc938 remains conditional on those interfaces. No selected certificate +or predecessor source is changed here. diff --git a/research/compact-rounded-add/review/compact-add-lead-check.py b/research/compact-rounded-add/review/compact-add-lead-check.py new file mode 100644 index 0000000000..9178035eb8 --- /dev/null +++ b/research/compact-rounded-add/review/compact-add-lead-check.py @@ -0,0 +1,82 @@ +"""Independent mixed-width/source-extreme oracle for compact literal ADD. + +Drives unchanged primitive directly, using only immutable checker hardware. +Prepared for @CubeJerry with substantial OpenAI assistance. +""" +from fractions import Fraction as F +import hashlib,json +from pathlib import Path +from random import Random +import sys +from types import SimpleNamespace + +PKG=Path(sys.argv[1] if len(sys.argv)>1 else '/workspace/scratch/a365d332d434/worker-compact-add/research/compact-rounded-add').resolve() +sys.path.insert(0,str(PKG)) +from tables import compile_compact +from source_binding import vendor +H=vendor('lead_compact_physical','vendor/physical_fixture.py') + +def encode(values,widths): + out=[] + for v,w in zip(values,widths): + for s in [(v>>j)&1 for j in range(w)]+[2]:out.extend(((s>>2)&1,(s>>1)&1,s&1)) + return out +def decode(bits,widths): + s=[4*bits[i]+2*bits[i+1]+bits[i+2] for i in range(0,len(bits),3)] + out=[];offset=0 + for w in widths: + b=s[offset:offset+w];assert len(b)==w and all(v in (0,1) for v in b) and s[offset+w]==2 + out.append(sum(v<>j)&1,sign*((abs(a)>>j)&1)) for j in range(L-1,-1,-1)] + if mutant=='lost-negative':coeff=[(x,abs(y)) for x,y in coeff] + if mutant=='lost-leading':coeff[0]=(0,0) + b=B.Builder();b.request(('entry',));maxcarry=0 + reject=('reject',) + def go(k):b.goto(k) + def branch(port,cases):b.branch(port,cases,reject) + def move(port,n): + for _ in range(abs(n)):b.emit('move',port,1 if n>0 else -1) + def publics():move(0,1);move(1,1) + def reset(nextkey):go(('reset',K,nextkey)) + def rewind(nextkey):go(('rewind',nextkey)) + def hstep(i,k,sx,sy,x,y,n,remaining,parity): + nonlocal maxcarry + beta,alpha=coeff[i];v=2*n+beta*x+alpha*y+k;z=v&1;kk=v//2 + need(abs(kk)<=4,'closed Horner carry');maxcarry=max(maxcarry,abs(kk)) + b.emit('write',2,z);move(2,1) + if remaining is None: + publics();go(('hscan',i,kk,x,y,parity)) + elif remaining>1:go(('hhigh',i,remaining-1,kk,sx,sy,parity)) + elif kk==2*n+beta*sx+alpha*sy-z: + go(('hfinish',i,parity)) + else:go(reject) + def qdigit(n,k): + v=n+k;z=v&1;kk=(v-o*z)//2 + need(-o<=kk<=0,'closed quotient carry');return z,kk + while b.pending: + key=b.pending.popleft();b.mark(key);tag=key[0] + if tag=='reject':b.emit('reject','compact rounded ADD format/range') + elif tag=='entry':branch(2,{4:('entry-o',)}) + elif tag=='entry-o':branch(3,{4:('begin',)}) + elif tag=='begin': + b.emit('write',2,5);move(2,1);go(('start',0,False)) + elif tag=='start': + _,parity,seen=key;cases={x:('record',parity) for x in (0,1)} + if seen and parity==0:cases[4]=('source-end',) + branch(0,cases) + elif tag=='source-end':branch(1,{4:('global-back',)}) + elif tag=='record': + _,parity=key;b.emit('write',2,6);move(2,1);go(('init',parity)) + elif tag=='init': + _,parity=key;branch(0,{0:('init-y',parity),1:('init-y',parity),2:('init-end',parity)}) + elif tag=='init-y': + _,parity=key;branch(1,{0:('init-zero',parity),1:('init-zero',parity)}) + elif tag=='init-zero': + _,parity=key;b.emit('write',2,0);move(2,1);publics();go(('init',parity)) + elif tag=='init-end': + _,parity=key;branch(1,{2:('init-high',parity)}) + elif tag=='init-high': + _,parity=key + for _ in range(K):b.emit('write',2,0);move(2,1) + b.emit('write',2,2);reset(('hscan',0,0,2,2,parity)) + elif tag=='reset': + _,left,nxt=key + if left:move(2,-1);go(('reset',left-1,nxt)) + else:go(('reset-back',nxt)) + elif tag=='reset-back': + _,nxt=key;move(2,-1);branch(2,{0:('reset-public',nxt),1:('reset-public',nxt),6:('reset-ready',nxt)}) + elif tag=='reset-public': + _,nxt=key;move(0,-1);move(1,-1);go(('reset-back',nxt)) + elif tag=='reset-ready': + _,nxt=key;move(2,1);go(nxt) + elif tag=='hscan': + _,i,k,sx,sy,parity=key;cases={x:('hy',i,k,x,parity) for x in (0,1)} + if sx in (0,1):cases[2]=('hend-y',i,k,sx,sy,parity) + branch(0,cases) + elif tag=='hy': + _,i,k,x,parity=key;branch(1,{y:('hn',i,k,x,y,parity) for y in (0,1)}) + elif tag=='hn': + _,i,k,x,y,parity=key;branch(2,{n:('hdigit',i,k,x,y,n,parity) for n in (0,1)}) + elif tag=='hdigit': + _,i,k,x,y,n,parity=key;hstep(i,k,x,y,x,y,n,None,parity) + elif tag=='hend-y': + _,i,k,sx,sy,parity=key;branch(1,{2:('hhigh',i,K,k,sx,sy,parity)}) + elif tag=='hhigh': + _,i,left,k,sx,sy,parity=key;branch(2,{n:('hhigh-digit',i,left,k,sx,sy,n,parity) for n in (0,1)}) + elif tag=='hhigh-digit': + _,i,left,k,sx,sy,n,parity=key;hstep(i,k,sx,sy,sx,sy,n,left,parity) + elif tag=='hfinish': + _,i,parity=key + nxt=('hscan',i+1,0,2,2,parity) if i+1>j)&1 if j1 else ('drop',d,0,parity) + rewind(nxt) + elif tag=='rewind': + _,nxt=key;move(2,-1);branch(2,{0:key,1:key,6:('rewind-ready',nxt)}) + elif tag=='rewind-ready':_,nxt=key;move(2,1);go(nxt) + elif tag=='residue': + _,rho,power,sn,parity=key + cases={n:('res-digit',(rho+n*power)%o,(2*power)%o,n,parity) for n in (0,1)} + if sn in (0,1): + r=(rho-(0 if mutant=='unsigned-residue' else sn)*power)%o + cases[2]=('res-done',r,parity) + branch(2,cases) + elif tag=='res-digit': + _,rho,power,sn,parity=key;move(2,1);go(('residue',rho,power,sn,parity)) + elif tag=='res-done':_,r,parity=key;rewind(('drop',d,-r,parity)) + elif tag=='drop': + _,left,k,parity=key + if left:branch(2,{n:('drop-digit',left,k,n,parity) for n in (0,1)}) + else:go(('emit',k,2,parity)) + elif tag=='drop-digit': + _,left,k,n,parity=key;z,kk=qdigit(n,k);move(2,1);go(('drop',left-1,kk,parity)) + elif tag=='emit': + _,k,sz,parity=key;cases={x:('emit-y',k,parity) for x in (0,1)} + if sz in (0,1):cases[2]=('emit-end',k,sz,parity) + branch(0,cases) + elif tag=='emit-y': + _,k,parity=key;branch(1,{y:('emit-n',k,parity) for y in (0,1)}) + elif tag=='emit-n': + _,k,parity=key;branch(2,{n:('emit-digit',k,n,parity) for n in (0,1)}) + elif tag=='emit-digit': + _,k,n,parity=key;z,kk=qdigit(n,k);b.emit('write',3,z);move(3,1);move(2,1);publics();go(('emit',kk,z,parity)) + elif tag=='emit-end': + _,k,sz,parity=key;branch(1,{2:('high',K-d,k,sz,parity)}) + elif tag=='high': + _,left,k,sz,parity=key;branch(2,{n:('high-digit',left,k,n,sz,parity) for n in (0,1)}) + elif tag=='high-digit': + _,left,k,n,sz,parity=key;z,kk=qdigit(n,k) + if z!=sz and mutant!='omit-high':go(reject) + else: + move(2,1) + if left>1:go(('high',left-1,kk,sz,parity)) + elif kk==n-o*sz or mutant=='omit-high':go(('quotient-end',parity)) + else:go(reject) + elif tag=='quotient-end': + _,parity=key;branch(2,{2:('next',parity)}) + elif tag=='next': + _,parity=key;b.emit('write',3,2);move(3,1);move(2,1);publics();go(('start',1-parity,True)) + elif tag=='global-back': + move(2,-1);branch(2,{2:('global-delimiter',),5:('install',)}) + elif tag=='global-delimiter': + move(0,-1);move(1,-1);move(3,-1);move(2,-K);go(('global-bits',)) + elif tag=='global-bits': + move(2,-1);branch(2,{0:('global-public',),1:('global-public',),6:('global-back',)}) + elif tag=='global-public': + move(0,-1);move(1,-1);move(3,-1);go(('global-bits',)) + elif tag=='install':branch(3,{s:('install-symbol',s) for s in (0,1,2)}|{4:('install-end',)}) + elif tag=='install-symbol': + _,s=key;b.emit('write',0,s);move(0,1);move(3,1);go(('install',)) + elif tag=='install-end':branch(0,{4:('halt',)}) + elif tag=='halt':b.emit('halt') + else:raise ValueError(('unknown state',key)) + table=b.finish() + receipt=dict(coefficient=str(q),numerator=a,denominator=den,coefficient_bits=L,extra_width=K, + denominator_twos=d,odd_divisor=o,rows=len(table),states=len(b.labels),max_horner_carry=maxcarry, + port_order=['target','source','numerator-work','output-work'],mutant=mutant) + return table,receipt + + +def cost_bound(receipt,extent,records,old_backing=0,contexts=0): + U=1+extent+(receipt['extra_width']+1)*records + return 512*(receipt['coefficient_bits']+8)*U+7*old_backing+16*contexts diff --git a/research/compact-rounded-add/vendor/exact_scalar_tables.py b/research/compact-rounded-add/vendor/exact_scalar_tables.py new file mode 100644 index 0000000000..1cc22f75fb --- /dev/null +++ b/research/compact-rounded-add/vendor/exact_scalar_tables.py @@ -0,0 +1,295 @@ +"""Fixed scalar services compiled to the unchanged lifecycle table ABI. + +All arithmetic here belongs to finite-template construction. The returned +runtime uses only branch/write/unit-move/goto/halt/reject instructions. +Prepared for @CubeJerry with substantial OpenAI assistance. Apache-2.0. +""" +from collections import deque +from fractions import Fraction + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +class Builder: + def __init__(self): + self.rows, self.labels = [], {} + self.pending, self.claimed = deque(), set() + + def request(self, key): + if key not in self.claimed: + self.claimed.add(key) + self.pending.append(key) + return key + + def mark(self, key): + need(key not in self.labels, "unique compiled state") + self.labels[key] = len(self.rows) + + def emit(self, *row): + self.rows.append(row) + + def goto(self, key): + self.emit("goto", self.request(key)) + + def branch(self, port, cases, default): + self.emit("branch", port, + tuple((s, self.request(k)) for s,k in sorted(cases.items())), + self.request(default)) + + def finish(self): + need(not self.pending, "complete finite graph") + out = [] + for row in self.rows: + if row[0] == "goto": + out.append(("goto", self.labels[row[1]])) + elif row[0] == "branch": + out.append(("branch", row[1], tuple((s,self.labels[k]) for s,k in row[2]), + self.labels[row[3]])) + else: + out.append(row) + return tuple(out) + + +def compile_scalar(op, coefficient): + """Build a table for all complete complex records on one common grid. + + SCALE ports: target, output-work, guide-work. + ADD ports: target, source, output-work, guide-work. + Additional supplied work/context ports are untouched. Work is physically + retired by the unchanged Controller.primitive success wrapper. + """ + need(op in ("ADD", "SCALE"), "scalar operation") + q = Fraction(coefficient) + need(q != 0, "nonzero selected scalar") + a, denominator = q.numerator, q.denominator + d, odd = 0, denominator + while odd % 2 == 0: + d += 1 + odd //= 2 + p, r = (denominator,a) if op == "ADD" else (a,0) + count = 2 if op == "ADD" else 1 + output, guide = count, count+1 + bound = abs(p)+abs(r)+odd + b, carry_states = Builder(), set() + b.request(("entry",)) + + def advance_inputs(): + for port in range(count): + b.emit("move", port, 1) + + def guide_one(): + b.emit("write", guide, 1) + b.emit("move", guide, 1) + + def digit(k, carry, last_q, x, y): + need(0 <= k <= d and abs(carry) <= bound, "finite carry invariant") + carry_states.add(carry) + value = p*x+r*y+carry + if k < d: + if value % 2: + return None + return k+1, value//2, last_q + bit = value & 1 + following = (value-odd*bit)//2 + need(abs(following) <= bound, "closed finite carry interval") + b.emit("write", output, bit) + b.emit("move", output, 1) + return d, following, bit + + while b.pending: + key = b.pending.popleft() + b.mark(key) + tag = key[0] + if tag == "entry": + b.branch(output, {4:("guide-entry",)}, ("reject","nonblank output work")) + elif tag == "guide-entry": + b.branch(guide, {4:("begin",)}, ("reject","nonblank guide work")) + elif tag == "begin": + b.emit("write", guide, 5) + b.emit("move", guide, 1) + b.goto(("start",0,False)) + elif tag == "start": + _, parity, seen = key + ending = ("finish-source",) if parity == 0 and seen else ("reject","complete nonempty complex field") + b.branch(0, {0:("read-source",0,0,2,parity,0), + 1:("read-source",0,0,2,parity,1), 4:ending}, + ("reject","positive component width")) + elif tag == "scan": + _, k, carry, sx, sy, sq, parity = key + b.branch(0, {0:("read-source",k,carry,sq,parity,0), + 1:("read-source",k,carry,sq,parity,1), + 2:("component-end",k,carry,sx,sy,sq,parity)}, + ("reject","unterminated signed component")) + elif tag == "read-source": + _, k, carry, sq, parity, x = key + if count == 2: + b.branch(1, {y:("digit",k,carry,sq,parity,x,y) for y in (0,1)}, + ("reject","same complete component shape")) + else: + b.goto(("digit",k,carry,sq,parity,x,0)) + elif tag == "digit": + _, k, carry, sq, parity, x, y = key + following = digit(k,carry,sq,x,y) + if following is None: + b.goto(("reject","inexact low numerator bits")) + else: + k1,c1,q1 = following + guide_one() + advance_inputs() + b.goto(("scan",k1,c1,x,y,q1,parity)) + elif tag == "component-end": + _, k, carry, sx, sy, sq, parity = key + following = ("extend",d,k,carry,sx,sy,sq,parity) + if count == 2: + b.branch(1, {2:following}, ("reject","same complete component shape")) + else: + b.goto(following) + elif tag == "extend": + _, remaining, k, carry, sx, sy, sq, parity = key + if remaining: + following = digit(k,carry,sq,sx,sy) + if following is None: + b.goto(("reject","inexact sign-extension numerator bits")) + else: + k1,c1,q1 = following + b.goto(("extend",remaining-1,k1,c1,sx,sy,q1,parity)) + elif sq not in (0,1) or carry != p*sx+r*sy-odd*sq: + b.goto(("reject","inexact quotient or signed output overflow")) + else: + b.emit("write", output, 2) + b.emit("move", output, 1) + guide_one() + advance_inputs() + b.goto(("start",parity^1,True)) + elif tag == "finish-source": + if count == 2: + b.branch(1, {4:("finish-output",)}, ("reject","same complete field frontier")) + else: + b.goto(("finish-output",)) + elif tag == "finish-output": + b.branch(output, {4:("rewind-step",)}, ("reject","exact staged output frontier")) + elif tag == "rewind-step": + b.emit("move", guide, -1) + b.goto(("rewind-read",)) + elif tag == "rewind-read": + b.branch(guide, {1:("rewind-inputs",),5:("install-start",)}, + ("reject","complete unary rewind guide")) + elif tag == "rewind-inputs": + for port in tuple(range(count))+(output,): + b.emit("move", port, -1) + b.goto(("rewind-step",)) + elif tag == "install-start": + b.emit("move", guide, 1) + b.goto(("install-guide",)) + elif tag == "install-guide": + b.branch(guide, {1:("install-read",),4:("installed-target-end",)}, + ("reject","install guide format")) + elif tag == "install-read": + b.branch(output, {s:("install-symbol",s) for s in (0,1,2)}, + ("reject","complete protected numeric output")) + elif tag == "install-symbol": + b.emit("write", 0, key[1]) + for port in (0,output,guide): + b.emit("move", port, 1) + b.goto(("install-guide",)) + elif tag == "installed-target-end": + b.branch(0, {4:("installed-output-end",)}, ("reject","exact installed target frontier")) + elif tag == "installed-output-end": + b.branch(output, {4:("halt",)}, ("reject","exact consumed protected output")) + elif tag == "halt": + b.emit("halt") + elif tag == "reject": + b.emit("reject", key[1]) + else: + raise ValueError("unknown compiler state") + return b.finish(), dict(operation=op,coefficient=str(q),denominator_twos=d, + odd_denominator=odd,numerator_target=p,numerator_source=r, + carry_bound=bound,carry_states=len(carry_states), + rows=len(b.rows),states=len(b.labels),public_ports=count,work_ports=2) + + +def source_literal(event, word, caller=None): + """Authenticate a source scalar retained by source_ir's nested remappings. + + Fields stay the source lowerer's actual ordered binding. Whole-job native + normalizers and two-output SWAP/SIGNED_SWAP services remain outside scope. + """ + need(event.op == "SERVICE", "only original scalar SERVICE") + token = event.token + 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] # The source remap API's empty context. + continue + if isinstance(token[0],str) and token[0] in wrappers: + need(len(token)==wrappers[token[0]],'source remap wrapper grammar') + # product-right also retains an issuing PAID token as provenance. + # Only the last member is the instruction currently being remapped. + token = token[-1] + continue + break + need(isinstance(token,(tuple,list)) and token and isinstance(token[0],str) + and token[0] in ('local','boundary-right','boundary-left','outer','query-add'), + 'source scalar origin grammar') + tag = token[0] + if tag == 'local': + need(len(token)==3,'local scalar token grammar') + _,pc,raw = token + need(type(pc) is int and 0 <= pc < len(word['program']), "actual current source event") + need(tuple(raw) == tuple(word['program'][pc]), "exact current scalar source bytes") + q, origin = Fraction(raw[-2]), ('local',pc) + else: + need(caller is not None,'outer scalar requires exact caller source') + if tag in ('boundary-right','boundary-left'): + need(len(token)==3,'boundary scalar token grammar') + _,column,raw = token + rows = caller['boundaries'][tag.split('-')[1]+'_program'] + need(tuple(raw) in tuple(tuple(x) for x in rows),'actual boundary scalar instruction') + origin = (tag,column) + elif tag == 'outer': + need(len(token)==4,'outer scalar token grammar') + _,site,column,raw = token + need(type(site) is int and 0 <= site < len(caller['physical_events']), + 'actual outer source site') + need(tuple(raw)==tuple(caller['physical_events'][site]),'exact outer scalar instruction') + origin = (tag,site,column) + else: + need(len(token)==5 and token[1]=='query','query scalar token grammar') + _,_,site,stage,column = token + need(type(site) is int and 0 <= site < len(caller['physical_events']), + 'actual query source site') + original = caller['physical_events'][site] + need(original[0]=='QUERY_SHEAR' and original[1]==stage and original[3] is False, + 'actual forward source query') + raw = ('ADD',None,None,1) + origin = (tag,site,column) + need(type(column) is int and 0 <= column < 104,'actual source scalar column') + need(raw[0] in ('ADD','SCALE'),'original source arithmetic scalar') + q = Fraction(raw[-1]) + op = raw[0] + need(op in ("ADD","SCALE"), "original scalar kind") + arity = 2 if op == "ADD" else 1 + need(len(event.fields) == arity and len(set(event.fields)) == arity, + "distinct actual scalar field ports") + need(q != 0, "nonzero source coefficient") + return op,q,origin + + +def bind_services(events, word, caller=None): + """Bind precisely the supplied source scalar events to finite tables.""" + cache, services, receipt = {}, {}, [] + for event in events: + op,q,origin = source_literal(event,word,caller) + key = (op,q) + if key not in cache: + cache[key] = compile_scalar(op,q) + table,_ = cache[key] + token = event.token + need(token not in services or services[token] == table, "unambiguous scalar service token") + services[token] = table + receipt.append((origin,op,str(q),tuple(event.fields))) + return services, tuple(cache[key][1] for key in sorted(cache)), tuple(receipt) diff --git a/research/compact-rounded-add/vendor/machine.py b/research/compact-rounded-add/vendor/machine.py new file mode 100644 index 0000000000..acf475e4fc --- /dev/null +++ b/research/compact-rounded-add/vendor/machine.py @@ -0,0 +1,406 @@ +"""Literal lifecycle control on fixed sequential tapes. + +Prepared for @CubeJerry with substantial OpenAI assistance. Apache-2.0. +Stack is the authenticated #5356 implementation supplied by the loader. +Algorithms never read tape addresses, extents, hardware arrays or a host stack. +Instruction and primitive tables are fixed before runtime inputs vary. +""" +from dataclasses import dataclass + +ZERO, ONE, LEFT, SEP, END, BASE, BLANK = range(7) +COMPONENT = 2 + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def emit(tape, symbol): + tape.write(symbol) + tape.move(1) + + +def origin(tape, marker=LEFT): + tape.move(-1) + while tape.read() != marker: + tape.move(-1) + tape.move(1) + + +def retire(tape, marker=LEFT): + """Erase all coded bytes, including encoded logical blanks.""" + origin(tape, marker) + while (symbol := tape.read()) != BLANK: + need(symbol in (ZERO, ONE), "contiguous binary body") + emit(tape, BLANK) + origin(tape, marker) + + +def transfer(source, target, source_marker=LEFT, target_marker=LEFT): + """Administrative actual-byte copy; never an arithmetic COPY.""" + origin(source, source_marker) + origin(target, target_marker) + need(target.read() == BLANK, "administrative transfer needs empty target") + while (symbol := source.read()) != BLANK: + need(symbol in (ZERO, ONE), "binary transfer") + emit(target, symbol) + source.move(1) + origin(source, source_marker) + origin(target, target_marker) + + +class CodedPort: + """Seven virtual symbols encoded as three nonblank physical bits. + + The physical LEFT before the current body is never exposed as data. + A left step at its local origin rejects. Two-sided routines first use + the standard translation to two one-sided ports. + """ + __slots__ = ("tape",) + + def __init__(self, tape): + self.tape = tape + + def read(self): + t = self.tape + if t.read() == BLANK: + return 4 + value = 0 + for _ in range(3): + bit = t.read() + need(bit in (ZERO, ONE), "whole virtual codeword") + value = 2 * value + bit + t.move(1) + for _ in range(3): + t.move(-1) + need(value < 7, "unused virtual codeword") + return value + + def write(self, value): + need(type(value) is int and 0 <= value < 7, "virtual alphabet") + for shift in (2, 1, 0): + emit(self.tape, (value >> 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/compact-rounded-add/vendor/physical_fixture.py b/research/compact-rounded-add/vendor/physical_fixture.py new file mode 100644 index 0000000000..027b563887 --- /dev/null +++ b/research/compact-rounded-add/vendor/physical_fixture.py @@ -0,0 +1,147 @@ +"""Metered fixtures execute unchanged Controller.primitive and execute_table. + +Only fixture construction and post-run oracles inspect integer values/storage. +Prepared for @CubeJerry with substantial OpenAI assistance. Apache-2.0. +""" +from types import SimpleNamespace +from fractions import Fraction +from source_binding import need, vendor + +M = vendor("rounded_retained_lifecycle", "vendor/machine.py") + + +class RowCounter: + """Observer-only table lookup counter; returns the unchanged immutable row. + + It never receives a tape, input value or coefficient, and never changes + the instruction stream. Ordinary fixtures use the tuple directly. + """ + def __init__(self, rows): + self.rows, self.steps = rows, 0 + + def __getitem__(self, pc): + self.steps += 1 + return self.rows[pc] + + +class Tape: + def __init__(self, bits=(), origin=17, readonly=False): + self.origin = self.pos = origin + self.cells = {origin-1:M.LEFT, origin-2:91} + self.cells.update({origin+i:s for i,s in enumerate(bits)}) + self.readonly = readonly + self.actions = self.reads = self.writes = self.moves = 0 + self.highwater = origin+len(bits) + + def tick(self): + need(self.pos >= self.origin-1, "no ancestor access") + self.actions += 1; self.highwater = max(self.highwater,self.pos) + + def read(self): + self.tick(); self.reads += 1 + return self.cells.get(self.pos,M.BLANK) + + def write(self,s): + self.tick(); self.writes += 1 + need(not self.readonly and self.pos >= self.origin, "protected source/marker") + need(s in range(7), "physical alphabet") + self.cells[self.pos]=s + + def move(self,step): + self.tick(); self.moves += 1 + need(step in (-1,1), "unit physical movement") + self.pos += step + need(self.pos >= self.origin-1, "no ancestor crossing") + self.highwater=max(self.highwater,self.pos) + + def body(self): + end=self.origin + while self.cells.get(end,M.BLANK)!=M.BLANK: + end+=1 + return tuple(self.cells.get(k,M.BLANK) for k in range(self.origin,end)) + + def blank(self): + return all(v==M.BLANK for k,v in self.cells.items() if k>=self.origin) + + def protected(self): + return self.cells[self.origin-1]==M.LEFT 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(values,width): + need(width>=1,"positive signed width") + out=[] + for n in values: + need(-(1<<(width-1))<=n<(1<<(width-1)),"signed fixture input") + out.extend((n>>k)&1 for k in range(width));out.append(2) + return tuple(out) + + +def decode(bits,width): + need(len(bits)%3==0,"whole physical codes") + syms=[4*bits[i]+2*bits[i+1]+bits[i+2] for i in range(0,len(bits),3)] + need(len(syms)%(width+1)==0,"whole components") + out=[] + for i in range(0,len(syms),width+1): + b=syms[i:i+width] + need(all(z in (0,1) for z in b) and syms[i+width]==2,"numeric result grammar") + out.append(sum(z<