diff --git a/research/typed-actual-width-h/PROOF.md b/research/typed-actual-width-h/PROOF.md new file mode 100644 index 0000000000..94c4a1ea1e --- /dev/null +++ b/research/typed-actual-width-h/PROOF.md @@ -0,0 +1,136 @@ +# Typed actual-width H and one rounded return + +This is a finite, exact interface lemma for the first open question in +[discussion 1166, comment 19016699](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19016699). +It does not prove the multi-round stock bound, execute a production-size cube, +or change the selected exponent. + +## Statement + +Let `p >= 1` and `g >= 1`. A Gaussian numerator is a pair of integers `(re, im)` +in the closed unit disk, meaning `re^2 + im^2 <= 2^{2p}`. The represented value +is that pair divided by `2^p`. On a block of `N = 2^m` such gaussians, `m >= g`, +fix `g` distinct address bits. Write `H0 = [[1, 1], [1, -1]] / 2`, and let +`H` be `H0` tensored on those bits and the identity on every other coordinate. + +Evaluate `H` exactly, then apply one truncation `Q_p` toward zero onto the +`p`-grid. Store the input and the returned words as two's-complement integers +of width `w = p + 2`, least-significant bit first. Bridge each returned +component to a most-significant-bit-first scan of the same width. + +Then: + +1. The exact numerator, in units of `2^{-(p+g)}`, is an integer of absolute + value at most `2^{p+g}`. Signed width `p + g + 2` holds every such + numerator, and width `p + g + 1` does not: the constant input `2^p` attains + `2^{p+g}` on the aligned character. +2. `Q_p` returns integers in `[-2^p, 2^p]`, still on the disk, in width `w`. + Each real or imaginary component is wrong by strictly less than `2^{-p}`, + so the Euclidean error is strictly less than `sqrt(2) 2^{-p}`. +3. `Q_p` commutes with a signed permutation of the coefficients. Truncation by + floor division does not, because `(-1) // 2 = -1` while toward-zero sends + `-1` at denominator `2` to `0`. +4. The bit bridge preserves each integer. Reading the least-significant-bit-first + encoding as if it were most-significant-bit-first changes any + non-palindromic word. +5. One call, with no layout permutation, performs `2 g N` real additions or + subtractions, `2 N` truncations, and `6 N (p + 2)` bit reads together with + the same number of bit writes. Two word tapes are rewound to their first + bit. A record permutation, when used, adds four word transfers per Gaussian + (read and write of both components). + +The old outer constructor admits a root only when +`plan.dimension_exponent == (1, 40)`. The frozen active-width planner computes +`K = floor(selected^{1/500})` and does not assign `dimension_exponent`. The +typed plan check uses the matched floor and the cardinality + +```text +gaussians = outer_rows * 2^{left + selected * K + right} * coefficients +``` + +instead of that guard. + +## Why the width and the error are exact + +The unnormalized Walsh sum on `g` bits is `sum_x chi(x, y) A_x`. Each `|A_x|` +is at most `2^p`, and there are `2^g` characters, so the sum is at most +`2^{p+g}`. Equality holds for the constant input `A_x = 2^p` at the trivial +character. A signed word of width `t` represents `[-2^{t-1}, 2^{t-1} - 1]`. +Width `p + g + 1` stops at `2^{p+g} - 1`. Width `p + g + 2` reaches +`2^{p+g+1} - 1`, which contains both `2^{p+g}` and `-2^{p+g}`. + +Dividing by `2^g` toward zero leaves a remainder of absolute value at most +`2^g - 1` in units of `2^{-(p+g)}`. That is strictly less than one `p`-grid +step. The same bound on both components gives Euclidean error strictly less +than `sqrt(2) 2^{-p}`. Toward-zero moves each component toward the origin, and +`H0` has `L1` row norm one, so a disk input returns a disk output. This is the +same endpoint shape as Jose Manuel's normalized `H0` statement; the new content +is the typed width, the single truncation, and the bit-scan invoice. + +## Matched bits, not another arithmetic oracle + +Nick Petalas's frozen `OuterLayer.__init__` requires +`dimension_exponent == (1, 40)`. Jose Manuel's frozen `ActiveWidthPlan.compute` +sets `d` from the selected count and `K` from `floor_power(d, 1, 500)`. Those +two source texts do not join: the planner never writes the exponent the +constructor demands. + +On every common round of the ten small layouts below, the matched root bits + +```text +right + rho + t K, 0 <= t < g, +rho = (h - b) mod K, b = (ell - 1) mod K +``` + +are exactly the bits of height `h` in the `K`-layout. For three short axes, +`ell = 3` and `K = 1`, height `0` occupies bits `{0, 1, 2}`. The same names in +the pre-layout order occupy `{0, 2, 4}`. + +The degree-`2` calibration `d = 4`, `g = 3` has `floor(d^{1/2}) = 2` and +`floor((d - 1)^{1/2}) = 1`. It is a stand-in for the production identity +`floor(k^{500}^{1/500}) = k` and `floor((k^{500} - 1)^{1/500}) = k - 1`, not a +legal outer cube. On 32 addresses with the single nonzero numerator `(8, 0)` at +address `0` and `p = 3`: + +- bits `{0, 1, 2}` return `(1, 0)` at address `2`; +- bits `{0, 2, 4}` return `(0, 0)` there. + +The matched layout of the 64-address three-short cube fixes this origin +impulse, and the height-`0` root bits are `{0, 1, 2}`, so the same return +survives that permutation. The layout is nevertheless nontrivial: a +nonconstant disk pattern is moved, at `256` word transfers. + +For `k = 2` and `k = 3` the production floors and both `p`-thresholds are +checked as exact integers, including the caller's multiples of six. At `k = 2` +those admitted precisions are `2^{20000} + 2` and `(2^{500} + 1)^{40} + 5`. +The address-extent ratio between `K = k` and `K = k - 1` is `2^{k^{500} - 1}`. +No tape of that size is allocated. A feasible plan with selected width `3`, +`K = 1`, left `2`, right `1` and four coefficients has `256` gaussians. The +typed check admits it. The `(1, 40)` guard rejects it, and `K = 2` fails the +matched floor. + +## Invoice boundary + +The counts above are one typed round. They do not include descriptor updates, +previous-output reset, borrowed restoration, private erasure, or a fixed +cube buffer carried across rounds. Clear1nsight's sufficient multi-round +allowance `Q <= C M R (r w + A + p^3) + poly(p)` is still a criterion, not a +supplied contract. This package stops at that point. + +The ten layouts are the geometries already used by the matched-layer checker: +`(ell, long flags, K)` equal to `(2, (F,), 1)`, `(2, (T,), 1)`, +`(3, (F, F), 1)`, `(3, (T, F), 1)`, `(3, (T, T), 1)`, `(3, (F, F, F), 1)`, +`(3, (T, F, T), 1)`, `(3, (F, F, F, F), 2)`, `(3, (T, F, F, F), 2)`, and +`(4, (T, F), 2)`. Eighteen common-round bit identities are checked there. + +The `g = 1`, `p = 3` disk is exhaustive: `197` numerators and `38,809` ordered +pairs, each compared with the explicit two-point matrix. The constant and +negative-constant inputs check the sharp numerator. A separate `g = 3`, `p = 4` +constant block checks the same bound one tensor higher. + +## What was not run + +No production T74 root, no PR3617 diagonal, no all-round lifecycle, no selected +cold replay, and no execution at `ell >= 45,812,984,491`. The frozen planner +and outer constructor are hashed and read as text. They are not imported: +their modules are not on this branch. diff --git a/research/typed-actual-width-h/README.md b/research/typed-actual-width-h/README.md new file mode 100644 index 0000000000..904b2b8f2e --- /dev/null +++ b/research/typed-actual-width-h/README.md @@ -0,0 +1,96 @@ +# Typed actual-width H and one rounded return + +**Partial result, no new κ.** One typed round of the normalized transform +`H0 = [[1, 1], [1, -1]] / 2` on the matched actual-width bits, followed by one +toward-zero return `Q_p` and an MSB-first component bridge. The selected +frontier is unchanged. + +This takes the first open question of the handoff in +[discussion 1166, comment 19016699](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19016699), +left by [PR #3623](https://github.com/CrocSwap/integer-mult-bounds/pull/3623). +The multi-round tape allowance in that handoff is still unspecified, so this +package does not start that construction. + +## Result + +For `p >= 1` and `g` selected bits, an exact `H0` tensor sends a `p`-grid unit +disk to integer numerators in units of `2^{-(p+g)}`. Those numerators fit in +signed width `p + g + 2` and do not fit in width `p + g + 1`. One truncation +toward zero returns the `p`-grid disk in width `p + 2`, with Euclidean error +strictly below `sqrt(2) 2^{-p}`. The truncation commutes with signed +permutations; floor division does not. The bit bridge preserves values and is +exactly the conversion from the LSB-first root word to an MSB-first scan. + +On the matched layout, common-round root bits are the physical slots of that +height. The degree-2 witness (`d = 4`, so `K_d = 2` and `K_g = 1`) puts a +numerator `(8, 0)` at address 0 and `p = 3`: + +| Selected bits | Address 2 after `Q_p` | +|---|---| +| matched `{0, 1, 2}` | `(1, 0)` | +| old stride `{0, 2, 4}` | `(0, 0)` | + +The 32-address witness invoice is 192 real add/sub operations, 64 +truncations, and 960 bit reads plus 960 bit writes. Those bit counts include +the input load, the MSB-first bridge, and the read of the returned tape. +Temporary width is 8 and final width is 5. The `g = 1`, `p = 3` disk is exhaustive (197 points, 38,809 +pairs). Production floors at `k = 2, 3` are exact integers, including the +six-multiple offsets `+2` and `+5` at `k = 2`. The extent ratio between the two +chunk widths has base-2 logarithm `k^{500} - 1`; that cube is not allocated. + +The argument, the finite domain, and the claims that are not made are in +[PROOF.md](PROOF.md). + +## Evidence + +Canonical main for this package is `bb4bccbf42844d2801487450727c2f63e10d1d0f`, +priority revision 6. The predecessor proof was written against +`20ecf2891d80b5acf18d980b2164fb44ea7faa90`. The two frozen sources have the same +git blobs at PR #3623 heads `328c40966b650f60b1d62cfb0b1d67b2b755eb62` and +`c5ab698bba8b35323e40ae3b132e78f26179d393`. + +```sh +python3.12 -I -B research/typed-actual-width-h/verify.py +python3.12 -B scripts/research_package.py --package research/typed-actual-width-h +``` + +Both the normal command and the same command under `-O` print +`PASS_TYPED_ACTUAL_WIDTH_H` and the same receipt. The local run below used +CPython 3.12.3 and finished in about two seconds. It does not import the frozen +modules. + +## Credit + +The `(1, 40)` outer guard is Nick Petalas's PR #3493, as vendored by +Clear1nsight in PR #3623. The selected-width `K` law and the normalized `H0` +endpoint are Jose Manuel's PR #3599 (`jmbarrancoml`), retaining Hiroki +Kumazaki's factory work. The matched layout, the address-2 witness, and the +decision to stop when the multi-round allowance is unspecified are +Clear1nsight's PR #3623, incorporating Sagar Thakrar's PR #3617 diagonal as an +unexecuted predecessor. The transform lineage retained there includes Douglas +Colkitt, Philipp, and the authors named in that proof. + +New work is the typed width, the single toward-zero return, the MSB/LSB bit +invoice, and the independent checker. unpaidmoon, with substantial AI +assistance. No independent human review or formal-kernel proof is claimed. +Apache-2.0. The frozen files keep their original notices. + +## Open next questions + +1. **Can one fixed cube and packet inventory carry every round?** The + sufficient bound `Q <= C M R (r w + A + p^3) + poly(p)` still does not name + descriptor updates, previous-output reset, borrowed restoration, or the + constant number of cube buffers. First step: write those operations for one + common round and one prefix round on the 64-address three-short cube, with + an explicit simultaneous tape count. Blocked by: that contract is not in + PR #3623 or in this package, and the handoff says to stop while it is + unspecified. +2. **Does this one-round invoice plug into PR #3617 without a second producer + charge?** PR #3617 already pays a fixed-h diagonal. First step: add this + bridge's `6 N (p + 2)` bit scans once per record and show which of its 38 + roles, if any, already move those bits. Blocked by: PR #3617 is unmerged, + and its full-array pass was not replayed here. +3. **Is the `k = 2` extent gap visible to any executable outer instance?** The + ratio is `2^{2^{500} - 1}` and the source band forces + `ell >= 45,812,984,491`. First step: none that allocates the cube. A + symbolic tape-count identity would still not be a physical execution. diff --git a/research/typed-actual-width-h/SOURCES.json b/research/typed-actual-width-h/SOURCES.json new file mode 100644 index 0000000000..a2cb687fd8 --- /dev/null +++ b/research/typed-actual-width-h/SOURCES.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "base_commit": "bb4bccbf42844d2801487450727c2f63e10d1d0f", + "files": [ + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ], + "related_work": [ + { + "pr": 3623, + "heads": [ + "328c40966b650f60b1d62cfb0b1d67b2b755eb62", + "c5ab698bba8b35323e40ae3b132e78f26179d393" + ], + "usage": "Frozen outer guard and active-width planner copied into this package. Not ancestors of this branch, so they are hashed by verify.py rather than pinned with head:.", + "blobs": { + "research/twiddle-matched-layer/pr3493-outer_layer.py": "2fc3370ea7e1b32be27faa4ec726ad7732af6769", + "research/twiddle-matched-layer/pr3599-active_plan.py": "c3a01cd8c4f52cab478aefacad60f64f60f1453a" + } + } + ] +} diff --git a/research/typed-actual-width-h/TASK.json b/research/typed-actual-width-h/TASK.json new file mode 100644 index 0000000000..11e92aee06 --- /dev/null +++ b/research/typed-actual-width-h/TASK.json @@ -0,0 +1,80 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 6, + "base_commit": "bb4bccbf42844d2801487450727c2f63e10d1d0f", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Can one exact all-size/compiler, precision, hosting or restoration implication be proved or falsified?", + "starting_points": [ + "certificates/selected-result.json", + "docs/audit.md" + ], + "methods": [ + "Prove one missing implication with explicit quantified hypotheses.", + "Find an exact counterexample at the claimed interface boundary." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the selected review scope and choose one exact all-size or precision implication.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write its quantified inputs and conclusion; find a missing hypothesis or construct a minimal exact adversarial instance.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": [ + "Choose one tape, precision, hosting or restoration lemma." + ], + "scope_change_triggers": [ + "Replacing a quantified obligation with another finite smoke test." + ], + "overlap_terms": [ + "uniform transfer", + "all-size", + "precision" + ] + }, + "scope_status": "changed", + "actual_scope": "Typed actual-width H0 tensor, one toward-zero Q_p return, and an MSB-first bit bridge on the matched twiddle array, with an exact one-round invoice.", + "scope_change_reason": "Handoff 1166#19016699 asks for a typed actual-width physical H and rounded return on the matched array from PR3623. The catalogue card is a general all-size or precision implication. This session takes only that one-round construction. The multi-round allowance is unspecified, so the lifecycle is not started.", + "bottleneck_link": "The matched K repair does not move the retained outer movement bottleneck. Pricing this previously unpriced one-round H and Q_p removes an oracle from that interface without a new exponent.", + "budget_minutes": 60, + "stop_rule": "Stop after the typed one-round width, return, bridge and invoice. Do not build multi-round stock or a production-size cube while the caller allowance remains an uninstantiated criterion.", + "outcome": "partial", + "evidence": "PROOF.md and verify.py. Exhaustive g=1, p=3 disk (197 points, 38809 pairs); degree-2 address-2 witness (1,0) versus (0,0); 18 common-round bit identities; exact k=2,3 floors including six-multiple offsets +2 and +5 at k=2. Normal and -O runs both print PASS_TYPED_ACTUAL_WIDTH_H.", + "author": "unpaidmoon, with substantial AI assistance", + "ai_assistance": "Substantial AI assistance in the proof, the checker, and the write-up. No independent human review or formal-kernel proof is claimed.", + "open_questions": [ + { + "question": "Can one fixed cube and packet inventory carry every round under an explicit simultaneous tape count?", + "why_it_matters": "The one-round invoice does not discharge the handoff's all-round reuse obligation, and an unknown multi-round charge is not zero.", + "first_step": "Write descriptor update, previous-output reset, borrowed restoration and the cube-buffer count for one common round and one prefix round on the 64-address three-short cube.", + "blocked_by": "PR3623 states Q<=C M R(rw+A+p^3)+poly(p) only as a sufficient criterion. The operations themselves are not specified." + }, + { + "question": "Does this one-round bit invoice plug into PR3617 without charging the producer a second time?", + "why_it_matters": "The diagonal pass already has a 38-role tariff. Adding 6N(p+2) bit scans blindly could double-count work the pass already pays.", + "first_step": "Identify which PR3617 roles already move component bits, then add only the missing bridge scans once per record.", + "blocked_by": "PR3617 is unmerged and its full-array pass was not replayed here." + }, + { + "question": "Is the k=2 extent gap visible to any executable outer instance?", + "why_it_matters": "The address-extent ratio is 2^(2^500-1), so every feasible cube has K_g=K_d=1 and cannot exhibit the production mismatch.", + "first_step": "Keep the exact integer thresholds already checked. Do not allocate the cube.", + "blocked_by": "The retained outer band forces ell>=45812984491, above the predecessor executable cap of 32." + } + ], + "handoff": { + "discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19016699", + "predecessor_pr": 3623, + "predecessor_heads": [ + "328c40966b650f60b1d62cfb0b1d67b2b755eb62", + "c5ab698bba8b35323e40ae3b132e78f26179d393" + ] + } +} diff --git a/research/typed-actual-width-h/VERIFY.json b/research/typed-actual-width-h/VERIFY.json new file mode 100644 index 0000000000..4fcfe826cc --- /dev/null +++ b/research/typed-actual-width-h/VERIFY.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Typed width, exhaustive g=1 disk, matched-bit witness, production floors, bridge, and one-round invoice." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "-O", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "The same checks with asserts disabled. Failures are raised explicitly, so the receipt must match the unoptimized run." + } + ] +} diff --git a/research/typed-actual-width-h/frozen/NOTICE.md b/research/typed-actual-width-h/frozen/NOTICE.md new file mode 100644 index 0000000000..bbdb907809 --- /dev/null +++ b/research/typed-actual-width-h/frozen/NOTICE.md @@ -0,0 +1,18 @@ +# Frozen predecessor sources + +These two Python files are unmodified copies. `verify.py` hashes them and reads +two source lines. It does not import them. + +| File | Vendored path in PR #3623 | Git blob | SHA-256 | +|---|---|---|---| +| `pr3493-outer_layer.py` | `research/twiddle-matched-layer/pr3493-outer_layer.py` | `2fc3370ea7e1b32be27faa4ec726ad7732af6769` | `3e6bae42f4e6239d0a467fb0498da3906fc139672fae96211c835be3b5fef307` | +| `pr3599-active_plan.py` | `research/twiddle-matched-layer/pr3599-active_plan.py` | `c3a01cd8c4f52cab478aefacad60f64f60f1453a` | `e1092fdbb70df43f1d4fdb50f39a07a543d71c4ea9f9e8a50b790b81fd50223e` | + +Both blobs are identical at PR #3623 heads +`328c40966b650f60b1d62cfb0b1d67b2b755eb62` and +`c5ab698bba8b35323e40ae3b132e78f26179d393`. + +`pr3493-outer_layer.py` is Nick Petalas's outer join from PR #3493. +`pr3599-active_plan.py` is Jose Manuel's actual-width planner from PR #3599. +Clear1nsight vendored both into PR #3623. Apache-2.0, with the notices already +in those files. They are not a new derivation. diff --git a/research/typed-actual-width-h/frozen/pr3493-outer_layer.py b/research/typed-actual-width-h/frozen/pr3493-outer_layer.py new file mode 100644 index 0000000000..2fc3370ea7 --- /dev/null +++ b/research/typed-actual-width-h/frozen/pr3493-outer_layer.py @@ -0,0 +1,70 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Join an explicitly planned physical root to MSB-first outer packets.""" + +import cohort + +cohort.activate() +from cardinal_counts import Count +from scratch_pool import ScratchPool +from session import OuterScope, erase_marker, sealed_constructors +from word_order import WordOrderBridge +from words import BLANK, need + + +class OuterLayer: + """The supplied root retains responsibility for its native construction.""" + + def __init__(self, root): + need(root.plan.dimension_exponent == (1, 40), "explicit outer root plan") + self.root = root + self.entrance, self.exit = WordOrderBridge(), WordOrderBridge() + self.pool = ScratchPool(8) + self.scope = OuterScope(self.pool) + self.closed = True + + def run( + self, + payload, + precision, + selected, + left, + right, + coefficients, + outer_rows, + residue, + ): + need( + self.closed and self.root.closed and self.exit.output.read() == BLANK, + "consumed complete outer layer", + ) + parameters = ( + precision, + selected, + left, + right, + coefficients, + outer_rows, + residue, + ) + width = gaussians = entry = result = None + self.closed = False + try: + self.root.plan.compute(*parameters) + with sealed_constructors(), self.scope.installed(): + width = Count(self.root.plan.count("input_bits")) + gaussians = Count(self.root.plan.count("gaussians")) + self.root.plan.clear() + entry = self.entrance.run(payload, width, gaussians) + result = self.root.run(entry, *parameters) + return self.exit.run(result, width, gaussians) + finally: + for tape in (result, entry): + if tape is not None: + tape.clear() + erase_marker(tape) + for value in (width, gaussians): + if value is not None: + value.close() + self.root.plan.clear() + self.pool.empty() + self.closed = True diff --git a/research/typed-actual-width-h/frozen/pr3599-active_plan.py b/research/typed-actual-width-h/frozen/pr3599-active_plan.py new file mode 100644 index 0000000000..c3a01cd8c4 --- /dev/null +++ b/research/typed-actual-width-h/frozen/pr3599-active_plan.py @@ -0,0 +1,109 @@ +"""Keep the retained encoded reservations, using the actual selected width.""" + +from active_sources import active +active() +from root_plan import (Count, Counter, RootPlan, ceil_divide, ceil_log2, coarse_depth, + compare, copy_symbols, floor_power, need, positive, + power_two, sealed_constructors, subtract) + + +class ActiveWidthPlan(RootPlan): + def compute(self, precision, selected, left, right, coefficients, outer_rows, residue): + need(self.closed and not self.pool.live, "closed root planning entry") + self.clear() + self.closed = False + inputs = dict(precision=precision, selected=selected, left=left, right=right, + coefficients=coefficients, outer_rows=outer_rows, residue=residue) + need(all(isinstance(v, Count) for v in inputs.values()), "encoded root inputs") + for name, value in inputs.items(): + copy_symbols(value.tape, self.roles[name]) + owned = [] + + def keep(value): + owned.append(value) + return value + + def literal(value): + return keep(Count.literal(value)) + + def plus(*values, constant=0): + result = literal(constant) + for value in values: + result.add(value) + return result + + def times(a, b): + return keep(Count.product(a, b)) + + def scaled(value, constant): + if constant == 0: + return literal(0) + result = keep(Count(value)) + if constant > 1: + result.multiply_small(constant) + return result + + def save(name, value): + copy_symbols(value.tape, self.roles[name]) + return value + + try: + with sealed_constructors(), self.scope.installed(): + save("zero", literal(0)) + two = literal(2) + need(compare(precision, two) >= 0, "root precision at least two") + positive(coefficients) + positive(outer_rows) + limit = keep(floor_power(precision, 997, 1000)) + need(compare(selected, limit) <= 0, "selected width within root domain") + d = save("d", literal(1) if selected.zero() else keep(Count(selected))) + K = save("K", keep(floor_power(d, 1, 500))) + need(compare(residue, K) < 0, "selected root residue") + logarithm = keep(ceil_log2(precision)) + G = save("G", plus(scaled(logarithm, 4), constant=6)) + H = save("H", times(d, G)) + depth = save("depth", keep(coarse_depth(d, self.dimension, self.maximum_rank))) + q0 = save("q0", scaled(depth, (self.level_divisor - 1).bit_length())) + qF = save("qF", keep(ceil_divide(scaled(H, 2), K))) + qB = save("qB", keep(ceil_divide(H, K))) + Q0 = save("Q0", plus(q0, qF, qB)) + delta = save("delta", scaled(d, 1 << self.guard_exponent)) + save("input_bits", plus(precision, constant=2)) + work_bits = save("work_bits", plus(precision, scaled(delta, 2), constant=3)) + active_bits = times(selected, K) + addresses = keep(power_two(plus(left, active_bits, right))) + save("gaussians", times(times(addresses, coefficients), outer_rows)) + self.fast = compare(selected, Q0) > 0 + if self.fast: + save("core_width", keep(subtract(selected, Q0))) + save("core_front", keep(subtract(times(qF, K), scaled(H, 2)))) + save("core_back", plus(keep(subtract(times(qB, K), H)), right)) + row_axes = times(q0, K) + original_rows = save("original_rows", keep(power_two(row_axes))) + prefix_count = save("prefixes", times(outer_rows, keep(power_two(left)))) + stock = literal(1) + repetitions = keep(Counter(depth)) + while not repetitions.finished: + stock.multiply_small(self.level_divisor) + repetitions.decrement() + save("stock", stock) + multiples = keep(ceil_divide(original_rows, stock)) + save("padded_rows", times(multiples, stock)) + rectangle = plus(keep(subtract(active_bits, row_axes)), right) + row_gaussians = times(keep(power_two(rectangle)), coefficients) + save("row_bits", scaled(times(row_gaussians, work_bits), 2)) + else: + for name in ("core_width", "core_front", "core_back", "row_bits"): + save(name, literal(0)) + for name in ("prefixes", "original_rows", "padded_rows", "stock"): + save(name, literal(1)) + except BaseException: + for tape in self.roles.values(): + tape.clear() + raise + finally: + for value in reversed(owned): + value.close() + self.pool.empty() + self.closed = True + return self diff --git a/research/typed-actual-width-h/verify.py b/research/typed-actual-width-h/verify.py new file mode 100644 index 0000000000..1c8184eabe --- /dev/null +++ b/research/typed-actual-width-h/verify.py @@ -0,0 +1,547 @@ +#!/usr/bin/env python3 +"""Typed actual-width H0 and one toward-zero return on the matched array. + +The multi-round stock allowance from discussion 1166 comment 19016699 is not +claimed. unpaidmoon, with substantial AI assistance. Apache-2.0. +""" + +from hashlib import sha256 +import json +from pathlib import Path +import sys + +ROOT = Path(__file__).resolve().parent +FROZEN = { + "frozen/pr3493-outer_layer.py": + "3e6bae42f4e6239d0a467fb0498da3906fc139672fae96211c835be3b5fef307", + "frozen/pr3599-active_plan.py": + "e1092fdbb70df43f1d4fdb50f39a07a543d71c4ea9f9e8a50b790b81fd50223e", +} + + +def need(condition, reason): + if not condition: + raise ValueError(reason) + + +def root_int(n, degree): + need(type(n) is int and n >= 0 and type(degree) is int and degree >= 1, "root domain") + if n < 2: + return n + x = 1 << ((n.bit_length() + degree - 1) // degree) + while True: + y = ((degree - 1) * x + n // pow(x, degree - 1)) // degree + if y >= x: + break + x = y + need(pow(x, degree) <= n < pow(x + 1, degree), "exact integer root") + return x + + +def fits(value, width): + need(type(value) is int and type(width) is int and width >= 1, "word domain") + return -(1 << (width - 1)) <= value <= (1 << (width - 1)) - 1 + + +def on_disk(re, im, p): + limit = 1 << p + return re * re + im * im <= limit * limit + + +def toward_zero(value, denominator): + need(type(value) is int and type(denominator) is int and denominator > 0, "truncation domain") + return (1 if value >= 0 else -1) * (abs(value) // denominator) + + +def twos(value, width): + need(fits(value, width), "word does not fit") + return value % (1 << width) + + +def from_lsb(bits): + width = len(bits) + raw = 0 + for i, bit in enumerate(bits): + raw |= bit << i + if raw >= (1 << (width - 1)): + raw -= 1 << width + return raw + + +def from_msb(bits): + width = len(bits) + raw = 0 + for bit in bits: + raw = (raw << 1) | bit + if raw >= (1 << (width - 1)): + raw -= 1 << width + return raw + + +class Meter: + def __init__(self): + self.bit_reads = 0 + self.bit_writes = 0 + self.real_add_sub = 0 + self.truncations = 0 + self.rewinds = 0 + self.layout_word_transfers = 0 + + +class WordTape: + """Concatenated two's-complement words, least-significant bit first.""" + + def __init__(self, width, meter): + self.width = width + self.meter = meter + self.bits = [] + self.head = 0 + + def write_word(self, value): + raw = twos(value, self.width) + for i in range(self.width): + self.bits.append((raw >> i) & 1) + self.meter.bit_writes += 1 + + def read_word(self): + raw = 0 + for i in range(self.width): + raw |= self.bits[self.head] << i + self.head += 1 + self.meter.bit_reads += 1 + if raw >= (1 << (self.width - 1)): + raw -= 1 << self.width + return raw + + def rewind(self): + self.head = 0 + self.meter.rewinds += 1 + + +def write_msb_word(bits, value, width, meter): + raw = twos(value, width) + for i in range(width): + bits.append((raw >> (width - 1 - i)) & 1) + meter.bit_writes += 1 + + +def butterfly(rows, bits, temp_width, meter): + result = [pair for pair in rows] + for bit in bits: + for x in range(len(result)): + if (x >> bit) & 1: + continue + y = x | (1 << bit) + left, right = result[x], result[y] + summed = (left[0] + right[0], left[1] + right[1]) + diffed = (left[0] - right[0], left[1] - right[1]) + for pair in (summed, diffed): + need(fits(pair[0], temp_width) and fits(pair[1], temp_width), "temporary width") + result[x] = summed + result[y] = diffed + meter.real_add_sub += 4 + return result + + +def direct_tensor(rows, bits): + mask = sum(1 << bit for bit in bits) + result = [] + for x in range(len(rows)): + acc = (0, 0) + for choice in range(1 << len(bits)): + y = x & ~mask + for j, bit in enumerate(bits): + y |= ((choice >> j) & 1) << bit + sign = -1 if (x & y & mask).bit_count() % 2 else 1 + acc = (acc[0] + sign * rows[y][0], acc[1] + sign * rows[y][1]) + result.append(acc) + return result + + +def truncate_rows(rows, denominator, meter): + output = [] + for re, im in rows: + output.append((toward_zero(re, denominator), toward_zero(im, denominator))) + meter.truncations += 2 + return output + + +def slots_for(ell, flags, k): + need(ell >= 2 and flags and 1 <= k < ell, "layout domain") + original = tuple((i, h) for i, long in enumerate(flags) + for h in range(ell - (not long) - 1, -1, -1)) + b, q = (ell - 1) % k, (ell - 1) // k + prefix = [(i, ell - 1) for i, long in enumerate(flags) if long] + prefix += [(i, h) for h in range(b - 1, -1, -1) for i in range(len(flags))] + chunks = [(i, h) for j in range(q) for i in range(len(flags)) + for h in range(ell - 2 - j * k, ell - 2 - (j + 1) * k, -1)] + changed = tuple(prefix + chunks) + need(len(set(changed)) == len(original) and set(changed) == set(original), "layout bijection") + return original, changed + + +def selected_bits(slots, h): + return tuple(len(slots) - 1 - j for j, item in enumerate(slots) if item[1] == h) + + +def root_bits(flags, ell, k, h): + g, a = len(flags), sum(flags) + b, q = (ell - 1) % k, (ell - 1) // k + need(b <= h < ell - 1, "common-round domain") + j, rho = (ell - 2 - h) // k, (h - b) % k + left = a + g * b + j * g * k + right = (q - j - 1) * g * k + bits = tuple(right + rho + t * k for t in range(g)) + return left, right, bits + + +def layout_address_width(flags, ell): + return sum(ell - (not long) for long in flags) + + +def check_layout_family(): + cases = ((2, (False,), 1), (2, (True,), 1), + (3, (False, False), 1), (3, (True, False), 1), + (3, (True, True), 1), (3, (False, False, False), 1), + (3, (True, False, True), 1), + (3, (False, False, False, False), 2), + (3, (True, False, False, False), 2), + (4, (True, False), 2)) + checked = 0 + for ell, flags, k in cases: + _original, physical = slots_for(ell, flags, k) + need(len(_original) == layout_address_width(flags, ell), "named-slot count") + b = (ell - 1) % k + for h in range(b, ell - 1): + left, right, bits = root_bits(flags, ell, k, h) + need(left + len(flags) * k + right == len(physical), "complete root extent") + need(set(bits) == set(selected_bits(physical, h)), "matched selected bits") + checked += 1 + original, physical = slots_for(3, (False, False, False), 1) + need(set(selected_bits(original, 0)) == {0, 2, 4}, "original height-0 bits are the old stride") + need(set(selected_bits(physical, 0)) == {0, 1, 2}, "matched height-0 bits are contiguous") + # The scaled K=2 versus K=1 layouts are different permutations. + short = (False, False, False) + _, old = slots_for(3, short, 2) + _, new = slots_for(3, short, 1) + need(old != new, "old and matched layouts differ") + need(len(old) == 6 and 3 * 1 != len(old), "concealed-extent bit count disagrees") + return checked + + +def apply_layout(rows, coefficients, before, after, meter): + """Permute whole records. `rows` is address-major with `coefficients` gaussians each.""" + addresses = len(rows) // coefficients + need(len(before) == addresses.bit_length() - 1 or (1 << len(before)) == addresses, "layout shape") + need(len(rows) % coefficients == 0, "record shape") + + def bit_at(x, slots, named): + return (x >> (len(slots) - 1 - slots.index(named))) & 1 + + output = [None] * len(rows) + for x in range(addresses): + y = 0 + for name in after: + y = 2 * y + bit_at(x, before, name) + for j in range(coefficients): + output[y * coefficients + j] = rows[x * coefficients + j] + meter.layout_word_transfers += 4 + need(all(row is not None for row in output), "layout image") + return output + + +def physical_round(rows, bits, p, meter, final_width=None): + """Read LSB-first words, apply H0 tensor g, one Q_p, then an MSB-first bridge.""" + g = len(bits) + need(g >= 1 and p >= 1, "round domain") + n = len(rows) + need(n > 0 and (n & (n - 1)) == 0, "power-of-two address block") + width = p + 2 + temp_width = p + g + 2 + denominator = 1 << g + source = WordTape(width, meter) + for re, im in rows: + need(on_disk(re, im, p), "input disk") + source.write_word(re) + source.write_word(im) + source.rewind() + loaded = [(source.read_word(), source.read_word()) for _ in range(n)] + need(loaded == [tuple(pair) for pair in rows], "LSB-first reload") + raw = butterfly(loaded, bits, temp_width, meter) + need(raw == direct_tensor(loaded, bits), "butterfly matches explicit tensor") + for re, im in raw: + need(fits(re, temp_width) and fits(im, temp_width), "sharp temporary admission") + need(not (fits(1 << (p + g), temp_width - 1)), "narrow width is not a standing fact") + coarse = truncate_rows(raw, denominator, meter) + for (ure, uim), (cre, cim) in zip(raw, coarse): + need(abs(ure - cre * denominator) <= denominator - 1, "real remainder") + need(abs(uim - cim * denominator) <= denominator - 1, "imag remainder") + need(on_disk(cre, cim, p), "returned disk") + need(fits(cre, width) and fits(cim, width), "returned width") + if final_width is None: + final_width = width + need(final_width == width, "one final p-grid width") + output = WordTape(width, meter) + bridge_bits = [] + for re, im in coarse: + output.write_word(re) + output.write_word(im) + for part in (re, im): + before = len(bridge_bits) + write_msb_word(bridge_bits, part, width, meter) + stored = bridge_bits[before:before + width] + meter.bit_reads += width + need(from_msb(stored) == part, "MSB-first bridge preserves the value") + lsb = [(twos(part, width) >> i) & 1 for i in range(width)] + need(from_lsb(lsb) == part, "LSB-first encoding preserves the value") + if lsb != list(reversed(lsb)): + need(from_msb(lsb) != part, "reading LSB order as MSB changes a non-palindromic word") + output.rewind() + returned = [(output.read_word(), output.read_word()) for _ in range(n)] + need(returned == coarse, "coarse reload") + return returned, raw + + +def closed_form(n, g, p, layout=False): + width = p + 2 + # Input write, input read, output write, output read: 4 word passes, 2 components. + # Four LSB word passes (write, read, write, read) plus one MSB bridge + # write and read, two components each. + bit_passes = 6 * n * width + return { + "gaussians": n, + "temporary_width": p + g + 2, + "final_width": width, + "real_add_sub": 2 * g * n, + "truncations": 2 * n, + "bit_reads": bit_passes, + "bit_writes": bit_passes, + "layout_word_transfers": 4 * n if layout else 0, + "rewinds": 2, + } + + +def check_invoice(rows, bits, p): + meter = Meter() + returned, raw = physical_round(rows, bits, p, meter) + form = closed_form(len(rows), len(bits), p, layout=False) + need(meter.real_add_sub == form["real_add_sub"], "addition invoice") + need(meter.truncations == form["truncations"], "truncation invoice") + need(meter.bit_reads == form["bit_reads"], "bit-read invoice") + need(meter.bit_writes == form["bit_writes"], "bit-write invoice") + need(meter.rewinds == form["rewinds"], "rewind invoice") + need(meter.layout_word_transfers == 0, "no layout in this call") + return returned, raw, form + + +def disk_points(p): + limit = 1 << p + return [(a, b) for a in range(-limit, limit + 1) for b in range(-limit, limit + 1) + if a * a + b * b <= limit * limit] + + +def exhaustive_one_bit(): + p, bit = 3, (0,) + points = disk_points(p) + checked = 0 + for left in points: + for right in points: + returned, raw, _ = check_invoice([left, right], bit, p) + # Explicit two-point H0 before the single truncation. + need(raw[0] == (left[0] + right[0], left[1] + right[1]), "sum branch") + need(raw[1] == (left[0] - right[0], left[1] - right[1]), "difference branch") + need(returned[0] == tuple(toward_zero(v, 2) for v in raw[0]), "sum return") + checked += 1 + # Sharp temporary numerator on the constant boundary input. + limit = 1 << p + constant = [(limit, 0), (limit, 0)] + returned, raw, form = check_invoice(constant, bit, p) + need(raw[0] == (2 * limit, 0) and raw[1] == (0, 0), "sharp unnormalized sum") + need(returned[0] == (limit, 0) and returned[1] == (0, 0), "sharp rounded return") + need(not fits(2 * limit, form["temporary_width"] - 1), "width p+g+1 rejects the sharp sum") + need(fits(2 * limit, form["temporary_width"]), "width p+g+2 admits the sharp sum") + negative = [(-limit, 0), (-limit, 0)] + returned, raw, _ = check_invoice(negative, bit, p) + need(raw[0] == (-2 * limit, 0) and returned[0] == (-limit, 0), "odd rounded return") + return {"disk_points": len(points), "pairs": checked, "temporary_width": form["temporary_width"]} + + +def scaled_witness(): + """Degree-2 stand-in of the K_d/K_g selected-bit mismatch. Not a 500th-power cube.""" + need(root_int(4, 2) == 2 and root_int(3, 2) == 1, "scaled floors") + rows = [(0, 0) for _ in range(1 << 5)] + rows[0] = (8, 0) + p = 3 + matched, raw_m, invoice = check_invoice(rows, (0, 1, 2), p) + old, raw_o, _ = check_invoice(rows, (0, 2, 4), p) + need(matched[2] == (1, 0) and raw_m[2] == (8, 0), "matched address-two return") + need(old[2] == (0, 0) and raw_o[2] == (0, 0), "old selected bits miss address two") + need(matched != old, "the two tensors disagree") + flags = (False, False, False) + original, physical = slots_for(3, flags, 1) + meter = Meter() + impulse = [(0, 0) for _ in range(1 << len(original))] + impulse[0] = (8, 0) + moved_impulse = apply_layout(impulse, 1, original, physical, meter) + need(moved_impulse == impulse, "origin impulse is fixed by the matched layout") + need(meter.layout_word_transfers == 4 * len(impulse), "impulse layout transfer count") + _, _, height0 = root_bits(flags, 3, 1, 0) + need(set(height0) == {0, 1, 2}, "common height 0 uses the matched bits") + laid, _, _ = check_invoice(moved_impulse, height0, p) + need(laid[2] == (1, 0), "layout-fixed impulse still returns address two") + meter = Meter() + base = [((i % 5) - 2, 0) for i in range(1 << len(original))] + moved = apply_layout(base, 1, original, physical, meter) + need(meter.layout_word_transfers == 4 * len(base), "layout transfer count") + need(sorted(moved) == sorted(base) and moved != base, "layout is a nontrivial permutation") + h = 1 + _, _, bits = root_bits(flags, 3, 1, h) + need(set(bits) == set(selected_bits(physical, h)), "physical common-round bits") + returned, _, _ = check_invoice(moved, bits, p) + need(all(on_disk(re, im, p) for re, im in returned), "layout image returns to the disk") + return {"matched_address_2": list(matched[2]), "old_address_2": list(old[2]), + "witness_invoice": invoice, "layout_word_transfers": meter.layout_word_transfers} + + +def production_binding(): + records = [] + for k in (2, 3): + d0 = pow(k, 500) + old = pow(d0, 40) + changed = pow(d0 + 1, 40) + need(root_int(d0, 500) == k, "old floor at a perfect power") + need(root_int(d0 - 1, 500) == k - 1, "matched floor just below the power") + need(root_int(old, 40) == d0 and root_int(old - 1, 40) == d0 - 1, "old threshold") + need(root_int(changed, 40) == d0 + 1 and root_int(changed - 1, 40) == d0, "matched threshold") + g = d0 - 1 + need(g * (k - (k - 1)) == d0 - 1, "log2 extent ratio equals g") + # The actual caller admits precisions divisible by six. + admitted = [] + for p, expected in ((6 * ((old + 5) // 6), k - 1), + (6 * ((changed + 5) // 6), k)): + need(p % 6 == 0, "multiple of six") + d = root_int(p, 40) + need(root_int(d - 1, 500) == expected, "six-multiple matched floor") + need(admit_k(d - 1, 500, expected) and not admit_k(d - 1, 500, expected + 1), + "typed K predicate") + admitted.append(p - (old if expected == k - 1 else changed)) + if k == 2: + need(admitted == [2, 5], "stated k=2 six-multiple offsets") + records.append({"k": k, "extent_ratio_log2": "k^500-1", + "old_threshold_bits": old.bit_length(), + "new_threshold_bits": changed.bit_length(), + "six_multiple_offsets": admitted}) + # A feasible active-width plan uses K=1. The old outer guard does not admit it. + g, degree = 3, 500 + k_matched = root_int(g, degree) + need(k_matched == 1, "feasible production K") + plan = {"selected": g, "degree": degree, "K": k_matched, "residue": 0, + "left": 2, "right": 1, "coefficients": 4, "outer_rows": 1, + "precision": 6, "dimension_exponent": None} + plan["gaussians"] = plan["outer_rows"] * (1 << (plan["left"] + g * k_matched + plan["right"])) * plan["coefficients"] + need(plan["gaussians"] == 256, "small matched extent") + need(typed_plan_admits(plan), "typed wrapper admits the active-width plan") + need(not old_outer_admits(plan["dimension_exponent"]), "old wrapper rejects this plan") + plan["K"] = 2 + try: + typed_plan_admits(plan) + except ValueError: + rejected = True + else: + rejected = False + need(rejected, "typed wrapper rejects the old chunk width") + return {"powers": records, "small_plan_gaussians": 256} + + +def admit_k(selected, degree, k): + return k == root_int(selected, degree) and k >= 1 + + +def old_outer_admits(dimension_exponent): + return dimension_exponent == (1, 40) + + +def typed_plan_admits(plan): + g, k = plan["selected"], plan["K"] + need(admit_k(g, plan["degree"], k), "K is the matched floor") + need(0 <= plan["residue"] < k, "residue") + need(plan["precision"] >= 2, "precision") + width_bits = plan["left"] + g * k + plan["right"] + need(0 <= width_bits <= 20, "this checker allocates only a small extent") + extent = plan["outer_rows"] * (1 << width_bits) * plan["coefficients"] + need(plan["gaussians"] == extent and plan["outer_rows"] > 0 and plan["coefficients"] > 0, + "matched cardinality") + need(not old_outer_admits(plan.get("dimension_exponent")), + "typed wrapper does not reuse the (1, 40) guard") + return True + + +def frozen_sources(): + for name, digest in FROZEN.items(): + data = (ROOT / name).read_bytes() + need(sha256(data).hexdigest() == digest, "frozen sha256 " + name) + outer = (ROOT / "frozen/pr3493-outer_layer.py").read_text(encoding="utf-8") + plan = (ROOT / "frozen/pr3599-active_plan.py").read_text(encoding="utf-8") + need('root.plan.dimension_exponent == (1, 40)' in outer, "old guard text") + need("dimension_exponent" not in plan, "active planner does not set that guard") + need('floor_power(d, 1, 500)' in plan, "active K law") + need('literal(1) if selected.zero() else keep(Count(selected))' in plan, "d copies selected") + return {"outer_bytes": len(outer.encode()), "plan_bytes": len(plan.encode())} + + +def commutation_controls(): + need((-1) // 2 != toward_zero(-1, 2), "floor division is not toward zero") + need(toward_zero(-5, 2) == -toward_zero(5, 2) == -2, "toward zero is odd") + p, g = 3, 2 + rows = [((i % 3) - 1, (1 if i == 2 else 0)) for i in range(4)] + meter = Meter() + returned, raw = physical_round(rows, (0, 1), p, meter) + signed = [(-re, -im) for re, im in returned] + raw_signed = [(-re, -im) for re, im in raw] + need(truncate_rows(raw_signed, 1 << g, Meter()) == signed, "Q commutes with a global sign") + flipped = list(reversed(returned)) + need(list(reversed(truncate_rows(raw, 1 << g, Meter()))) == flipped, "Q commutes with a reversal") + # The same sign applied before truncation disagrees with floor-division. + floor_signed = [((-re) // (1 << g), (-im) // (1 << g)) for re, im in raw] + odd_floor = [(-(re // (1 << g)), -(im // (1 << g))) for re, im in raw] + need(floor_signed != odd_floor, "floor truncation does not commute with the sign") + + +def run(): + frozen = frozen_sources() + layouts = check_layout_family() + one_bit = exhaustive_one_bit() + witness = scaled_witness() + powers = production_binding() + commutation_controls() + # A g=3 constant input attains the sharp numerator 2^{p+g}. + p, g = 4, 3 + limit = 1 << p + rows = [(limit, 0) for _ in range(1 << g)] + returned, raw, invoice = check_invoice(rows, tuple(range(g)), p) + need(raw[0] == (limit << g, 0) and returned[0] == (limit, 0), "g=3 sharp return") + need(invoice["temporary_width"] == p + g + 2, "stated temporary width") + return { + "frozen": frozen, + "common_round_bit_checks": layouts, + "exhaustive_g1": one_bit, + "scaled_witness": witness, + "production": powers, + "sharp_g3_invoice": invoice, + } + + +def main(): + receipt = run() + text = json.dumps(receipt, sort_keys=True) + need("TODO" not in text, "receipt placeholder") + print("PASS_TYPED_ACTUAL_WIDTH_H") + print(text) + + +if __name__ == "__main__": + try: + main() + except ValueError as error: + print("FAIL_TYPED_ACTUAL_WIDTH_H: " + str(error), file=sys.stderr) + raise SystemExit(1)