From 7f76a3f1259f76b0a74551166919a0fd6975bc9e Mon Sep 17 00:00:00 2001 From: Ryanson Jonathan Date: Wed, 21 Oct 2026 16:34:49 +0700 Subject: [PATCH 1/2] Decide #4100 CRT.md's guard premise under mod-K coloring Window lemma: with position-mod-K coloring, (K-1)-bit guards are disjoint and free of active targets for every descriptor; K-bit guards contain another active target exactly at spacing K. #4100's own gadget fails on good addresses with K-bit guards (3,888 / 2,388 of 2^20) and is exact with the (K-1)-bit guards its code and 8B/2^K term use. On all 104,864 of #4174's production plans (allocator vendored, byte-checked) no two active targets can share a color for any Benes schedule. No new kappa. Co-Authored-By: Claude Opus 5.5 --- research/pr4100-guard-coloring/README.md | 142 +++++++ research/pr4100-guard-coloring/SOURCES.json | 30 ++ research/pr4100-guard-coloring/TASK.json | 80 ++++ research/pr4100-guard-coloring/VERIFY.json | 21 ++ .../pr4100-guard-coloring/vendor/NOTICE.md | 19 + .../vendor/pr4174_allocator.py | 347 ++++++++++++++++++ research/pr4100-guard-coloring/verify.py | 232 ++++++++++++ 7 files changed, 871 insertions(+) create mode 100644 research/pr4100-guard-coloring/README.md create mode 100644 research/pr4100-guard-coloring/SOURCES.json create mode 100644 research/pr4100-guard-coloring/TASK.json create mode 100644 research/pr4100-guard-coloring/VERIFY.json create mode 100644 research/pr4100-guard-coloring/vendor/NOTICE.md create mode 100644 research/pr4100-guard-coloring/vendor/pr4174_allocator.py create mode 100644 research/pr4100-guard-coloring/verify.py diff --git a/research/pr4100-guard-coloring/README.md b/research/pr4100-guard-coloring/README.md new file mode 100644 index 0000000000..e29fe387b1 --- /dev/null +++ b/research/pr4100-guard-coloring/README.md @@ -0,0 +1,142 @@ +# Guard windows under #4100's position-mod-K coloring + +**Claim type: a scoped proof audit with a counterexample to the literal text, +plus a census of #4174's actual production descriptors. No new κ.** This +does not accept #4100 and changes nothing in it. + +## Object + +Cinna Davis's [CRT.md](../unconditional-batched-crt/CRT.md) §4, at #4100 head +`337d04939571a637aeab54a0f58f54fde811663a`, says three things: + +- the good predicate requires "a margin 2B from both ends of each K-bit + guard"; +- the bad density is at most `r[2/B + 8B/2^K]`; +- "Color targets by current position modulo K, so guard intervals are + disjoint." + +Three open audits take this disjoint-guard premise as given: + +- #4321 (unpaidmoon) assumes "the `K`-bit guards are pairwise disjoint" and + notes that no audit decides that hypothesis. +- #4328's exact `r`-target density needs disjoint windows. +- #4174 (kumagi) supplies the actual placement descriptors; this package + checks them. + +## Results + +### 1. Lemma + +Let one macro's active targets all share a color, that is, a residue of their +`y`-significance position mod `K`. + +- With `(K−1)`-bit guards (the `K−1` bits above each target), the guards are + pairwise disjoint and contain no active target, for every descriptor. + Distinct same-color targets differ by a nonzero multiple of `K`, hence by + at least `K`. +- With `K`-bit guards, they are still pairwise disjoint, but a guard contains + another active target exactly when two same-color targets are `K` apart. + +This is checked exhaustively on 3,266 small position sets. + +### 2. The literal `K`-bit reading fails on #4100's own gadget + +In #4100's `check_batched_crt.py`, `good(…, guard=g)` reads `g−1` window bits. +Its two-target fixture places the targets at positions 0 and 6, exactly +`K = 6` apart. Running every one of the `2^20` addresses: + +| Source | Window bits | Good addresses | `S ≠ T` on good addresses | `T` leaves the good set | +| --- | --- | --- | --- | --- | +| #4100's `source_pair` | 5 (`K−1`) | 82,944 | 0 | 0 | +| #4100's `source_pair` | 6 (`K`) | 186,624 | **3,888** | **31,104** | +| second pair | 5 (`K−1`) | 82,944 | 0 | 0 | +| second pair | 6 (`K`) | 186,624 | **2,388** | **15,552** | + +Example: `(u,t,y) = (0,1,1086)` goes to `(0,5,1087)` instead of +`(0,1,1087)`. A carry inside target 0's 6-bit window flips target 1 before +target 1 is read, so the control field is not restored. + +**Consequence.** The premise must read "**`(K−1)`-bit guards**, free of active +targets". The equivalent alternative is `K`-bit guards with coloring mod +`K+1`. This matches the code, and it matches the density term `8B/2^K`, +which counts `4B` bad values in `K−1` bits. A `K`-bit window would give +`4B/2^K`. This is a presentational correction to CRT.md's "K-bit guard" and +to #4321's hypothesis wording. No bound changes. + +### 3. #4174's production descriptors + +The layout is #4174's own production census: `d = 65,536`, `ell = 24`, +widths alternating 24/23, `p = 6L`. That gives: + +| `L` | `G` | `K` | `r_max` | `H` | `y` bits | +| --- | --- | --- | --- | --- | --- | +| 1,540,096 | 3,072 | 196,608 | 5 | 15,360 | 1,494,016 | + +The census covers all 104,864 plans, 524,288 active-axis visits and 524,314 +fragments: + +- **Every active axis lies in `y`** after the three exchanges. +- **No two active axes of any plan can ever share a color, for any Beneš bit + schedule.** For every pair of fragments, the range of position differences + contains no nonzero multiple of `K`. This holds even though pairs reach + 1,463,286 bits apart. The aligned schedule (bit `m` on every axis wider + than `m`) confirms it over 12,304,384 target visits: maximum color + multiplicity 1, and no exact-`K` pair. +- **So at production parameters the disjoint-guard premise holds + vacuously,** and each compact macro handles one target. The multi-target + cancellation, and #4328's `r ≥ 2` density, are not exercised there. The + `O(K)`-colors-per-layer tariff covers this. +- **The last-`K` branch carries a material share.** 16,225 plans (15.5%) have + active axes in the top `K−1` bits of `y`. Under the aligned schedule, + 388,466 plan-layers contain exceptions, up to all 5 targets. At these sizes + `K/|y| ≈ 13%`. #4187 audits that branch at `O(VK)`. + +## Evidence + +`verify.py` uses only the standard library and takes about 18 seconds. It +also checks the source bindings: SHA256 pins of CRT.md and +`check_batched_crt.py`, 3 exact CRT.md phrases, `good()`'s `guard−1` window +expression, and the byte hash of the vendored allocator. + +## Not covered + +- Other production layouts. Only #4174's own pattern is censused here. + Other mixed-width patterns or larger `ell` could, in principle, create + same-color pairs; the lemma still covers them with `(K−1)`-bit guards. +- The elementary last-`K` branch's correctness (#4187). +- The control-function supports (#4169, #4174). +- There is no proof-kernel check. + +## Reproduce + +```sh +python3 scripts/research_package.py --package research/pr4100-guard-coloring --check-only +python3.12 scripts/research_package.py --package research/pr4100-guard-coloring +python3.12 -B research/pr4100-guard-coloring/verify.py +``` + +The verifier prints `PASS_PR4100_GUARD_COLORING_FINITE`. + +## Open next questions + +1. **Price macros per occupied color, not per residue.** + - *Why it matters:* at production every color is a singleton, so a layer + uses at most `r_max` macros per batch rather than `K`. The tariff could + be stated per occupied color. + - *First step:* bound occupied colors per batch by `r_max` in the CRT §4 + cost line. + - *Blocked by:* nothing. +2. **Census other admitted width patterns.** + - *Why it matters:* the vacuity finding is pattern-specific. + - *First step:* run the census on blocked and random `ell`/`ell−1` + patterns at `d = 65,536`. + - *Blocked by:* nothing; about 20 seconds per pattern. + +## Credit + +The construction and audited text are Cinna Davis's #4100 (OpenAI Codex +assistance). The placement descriptors are Hiroki KUMAZAKI's (@kumagi) #4174, +vendored unmodified; see [vendor/NOTICE.md](vendor/NOTICE.md). #4321 +(unpaidmoon) states the guard hypothesis this package decides. Prepared by +Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance. +Apache-2.0. diff --git a/research/pr4100-guard-coloring/SOURCES.json b/research/pr4100-guard-coloring/SOURCES.json new file mode 100644 index 0000000000..6e80240792 --- /dev/null +++ b/research/pr4100-guard-coloring/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65", + "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96" + }, + { + "path": "research/unconditional-batched-crt/CRT.md", + "usage": "input", + "git_blob": "d98dd8e368431cac33d5fc1c8c336696663641d6", + "sha256": "02c3a1e38cbee25aefe2640cc72676da62ba10eb7519fbcb9adb9d48b74eff2b" + }, + { + "path": "research/unconditional-batched-crt/check_batched_crt.py", + "usage": "input", + "git_blob": "1cf78abccd5e06beecc3ed21ba55f7c03b65fdbc", + "sha256": "681e2e3d71fa74c8b9b326f3860104fd9d89590a222e26ae6ee718d1fd40ff2e" + } + ] +} diff --git a/research/pr4100-guard-coloring/TASK.json b/research/pr4100-guard-coloring/TASK.json new file mode 100644 index 0000000000..8183a5f346 --- /dev/null +++ b/research/pr4100-guard-coloring/TASK.json @@ -0,0 +1,80 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/unconditional-batched-crt/README.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 PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": [ + "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller." + ], + "scope_change_triggers": [ + "Replacing a quantified obligation with another finite smoke test.", + "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses." + ], + "overlap_terms": [ + "uniform transfer", + "all-size", + "precision", + "4100", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "refined", + "actual_scope": "Decide the disjoint-guard premise of #4100 CRT.md section 4 under position-mod-K coloring: a window lemma, a counterexample to the literal K-bit guard on #4100's own gadget, and a census of #4174's actual production placement descriptors.", + "scope_change_reason": "The card asks for one quantified implication at its caller; this is the guard hypothesis that #4321 and #4328 assume and no audit decided, checked at the actual caller's descriptors (#4174).", + "bottleneck_link": "The compact switch's correctness and the bad-density term both rest on this premise; a wrong window convention breaks the gadget on good addresses.", + "budget_minutes": 75, + "stop_rule": "Stop once the premise is decided (lemma plus counterexample) and checked on #4174's production descriptors.", + "outcome": "completed", + "evidence": "verify.py: 3,266 exhaustive lemma cases; #4100's gadget on all 2^20 two-target addresses at spacing K: (K-1)-bit guards give S=T on all 82,944 good addresses, K-bit guards fail on 3,888/2,388 good addresses and T leaves the good set on 31,104/15,552; #4174 production census (104,864 plans, 524,288 axis visits): all axes in y, zero possible same-color pairs for any Benes schedule, aligned multiplicity 1, 16,225 plans with last-K exception axes.", + "author": "Ryanson Jonathan, with Claude Code (Claude Opus 5.5) assistance", + "ai_assistance": "Substantial Claude Code (Claude Opus 5.5) assistance in reading, the lemma, census implementation and writing; no independent human or proof-kernel review.", + "open_questions": [ + { + "question": "Price compact macros per occupied color rather than per residue mod K.", + "why_it_matters": "At #4174's production descriptors every color is a singleton, so a layer needs at most r_max macros per batch, not K.", + "first_step": "Bound occupied colors per batch by r_max in the CRT section 4 cost line.", + "blocked_by": "None." + }, + { + "question": "Census other admitted ell/ell-1 width patterns at d=65,536.", + "why_it_matters": "The vacuity of the premise at production is pattern-specific.", + "first_step": "Run the census on blocked and random width patterns.", + "blocked_by": "None; about 20 seconds per pattern." + } + ] +} diff --git a/research/pr4100-guard-coloring/VERIFY.json b/research/pr4100-guard-coloring/VERIFY.json new file mode 100644 index 0000000000..24c22289fb --- /dev/null +++ b/research/pr4100-guard-coloring/VERIFY.json @@ -0,0 +1,21 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/unconditional-batched-crt/CRT.md", + "research/unconditional-batched-crt/check_batched_crt.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Source pins, CRT.md phrases, good()'s guard-1 window and the vendored #4174 allocator hash; exhaustive window lemma; #4100's two-target gadget with (K-1)-bit versus K-bit guards on all 2^20 addresses; census of all 104,864 #4174 production plans." + } + ] +} diff --git a/research/pr4100-guard-coloring/vendor/NOTICE.md b/research/pr4100-guard-coloring/vendor/NOTICE.md new file mode 100644 index 0000000000..b511b6f44e --- /dev/null +++ b/research/pr4100-guard-coloring/vendor/NOTICE.md @@ -0,0 +1,19 @@ +# Vendored file + +`pr4174_allocator.py` is a byte-identical copy of +`research/crt-reservoir-placement/allocator.py` from +[PR #4174](https://github.com/CrocSwap/integer-mult-bounds/pull/4174). + +| Field | Value | +| --- | --- | +| Head | `5fec853f0c048871de3b8098d1e30d4ee19cda23` | +| Git blob | `4b3ad89652a28f7d142248d1b5747272e696493c` | +| SHA256 | `b764195fc6291e3c8fa8297b1f4ceaefc119d5664d8ff348b49eac8a2e79c688` | + +It is copied, not pinned, because that PR head is not reachable from canonical main, and +package pins resolve only against reachable Git objects. `verify.py` checks the SHA256 +before importing the file. + +Author: Hiroki KUMAZAKI (@kumagi), with substantial OpenAI Codex assistance. It implements +the CRT.md §3 placement of Cinna Davis's PR #4100. Apache-2.0, as stated in the file. It is +unmodified. diff --git a/research/pr4100-guard-coloring/vendor/pr4174_allocator.py b/research/pr4100-guard-coloring/vendor/pr4174_allocator.py new file mode 100644 index 0000000000..4b3ad89652 --- /dev/null +++ b/research/pr4100-guard-coloring/vendor/pr4174_allocator.py @@ -0,0 +1,347 @@ +"""Construct the bit-field placements specified by PR4100 CRT.md, section 3. + +Positions increase from the front (most significant end) of the complete +address. Logical axes appear physically in order d-1, ..., 0. Every interval +is half-open. This module manipulates address descriptors, not payload tapes; +it makes no machine-cost claim and performs no I/O. + +API: + layout = Layout(p, ell, widths) # widths indexed by logical axis + for plan in iter_plans(layout, level=None): + plan.active_axes # at most layout.r_max logical axes + plan.dependencies # original own/left-child intervals + plan.source_blocks # three original reservoir intervals + plan.destination_blocks # front u, front t, back b intervals + plan.map_position(position) # involution, also the inverse map + plan.map_interval(lo, hi) # translation fragments, original order + plan.descriptor_fragment_count # all d axes, without enumerating them + +The generator holds only one batch at a time. Layout's prefix index is built +once in O(d) space; no plan allocates the descriptors for all d axes. + +Cinna Davis supplies the audited CRT construction. This constructive +descriptor implementation is by Hiroki KUMAZAKI (@kumagi), with substantial +OpenAI Codex assistance. Apache-2.0. +""" +from __future__ import annotations + +from bisect import bisect_left +from dataclasses import dataclass, field +from itertools import islice +from typing import Iterable, Iterator + + +Interval = tuple[int, int] + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def ceil_log2(value: int) -> int: + """Return ceil(log2(value)) exactly for a positive integer.""" + require(type(value) is int and value >= 1, "positive integer logarithm input") + return (value - 1).bit_length() + + +def intersects(first: Interval, second: Interval) -> bool: + """Whether two half-open intervals have positive-length intersection.""" + return max(first[0], second[0]) < min(first[1], second[1]) + + +@dataclass(frozen=True, init=False) +class Layout: + """One validated actual-family layout, with widths in logical-axis order.""" + + p: int + ell: int + widths: tuple[int, ...] + prefix: tuple[int, ...] + d: int + L: int + G: int + K: int + r_max: int + H: int + + def __init__(self, p: int, ell: int, widths: Iterable[int]) -> None: + require(type(p) is int and p >= 1, "p must be a positive integer") + require(type(ell) is int and ell >= 2, "ell must be an integer at least 2") + logarithm = ceil_log2(p + 2) + require(ell >= logarithm, "ell must be at least ceil(log2(p+2))") + widths = tuple(widths) + d = len(widths) + require(d >= 51200 and d & (d - 1) == 0, + "d must be a power of two at least 51200") + require(all(type(width) is int and width in (ell - 1, ell) for width in widths), + "every axis width must be ell-1 or ell") + prefix = [0] + for width in widths: + prefix.append(prefix[-1] + width) + length = prefix[-1] + guard_digit_bits = 64 * (ell + logarithm) + maximum_batch = length // (100 * guard_digit_bits) + field_bits = maximum_batch * guard_digit_bits + require(maximum_batch >= 1, "the compact reservoir must have an active digit") + require(100 * field_bits <= length, "compact fields exceed their volume bound") + for name, value in ( + ("p", p), ("ell", ell), ("widths", widths), ("prefix", tuple(prefix)), + ("d", d), ("L", length), ("G", guard_digit_bits), + ("K", 64 * guard_digit_bits), ("r_max", maximum_batch), ("H", field_bits), + ): + object.__setattr__(self, name, value) + + @property + def levels(self) -> int: + return self.d.bit_length() - 1 + + def axes_interval(self, lo: int, hi: int) -> Interval: + """Physical span of consecutive logical axes [lo, hi).""" + require(type(lo) is int and type(hi) is int and 0 <= lo <= hi <= self.d, + "logical axis interval out of range") + return self.L - self.prefix[hi], self.L - self.prefix[lo] + + def axis_interval(self, axis: int) -> Interval: + """Original physical interval occupied by one complete logical axis.""" + require(type(axis) is int and 0 <= axis < self.d, "logical axis out of range") + return self.axes_interval(axis, axis + 1) + + def is_axis_boundary(self, position: int) -> bool: + """Test a physical boundary in O(log d), without building all intervals.""" + require(type(position) is int and 0 <= position <= self.L, + "physical boundary out of range") + value = self.L - position + index = bisect_left(self.prefix, value) + return index < len(self.prefix) and self.prefix[index] == value + + +@dataclass(frozen=True) +class Dependency: + """Conservative original support of one axis's Beneš switch function. + + own_interval contains the entire active axis, including its target bit. + The actual function omits that one target; retaining it here gives a + stronger reservoir-disjointness check. left_axes and left_interval are + the complete logical and physical left child of the current tree node. + """ + + axis: int + own_interval: Interval + left_axes: Interval + left_interval: Interval + + +@dataclass(frozen=True) +class Fragment: + """A piece translated without reversal from original to image interval.""" + + original_interval: Interval + image_interval: Interval + + @property + def delta(self) -> int: + return self.image_interval[0] - self.original_interval[0] + + +@dataclass(frozen=True) +class Placement: + """Strict exchange geometry, independently of the large-family cutoff. + + This also permits small exhaustive geometry fixtures without weakening + Layout's parameter checks. The three destinations are always [0,H), + [H,2H), and [length-H,length). Each supplied source has exactly H bits. + """ + + length: int + H: int + source_blocks: tuple[Interval, Interval, Interval] + destination_blocks: tuple[Interval, Interval, Interval] = field(init=False) + + def __post_init__(self) -> None: + require(type(self.length) is int and self.length > 0, "positive address length") + require(type(self.H) is int and self.H > 0, "positive field width") + sources = tuple(tuple(block) for block in self.source_blocks) + require(len(sources) == 3, "exactly three source fields are required") + require(all(len(block) == 2 and all(type(point) is int for point in block) + and 0 <= block[0] < block[1] <= self.length + and block[1] - block[0] == self.H for block in sources), + "each source must be an in-range interval of width H") + destinations = ((0, self.H), (self.H, 2 * self.H), + (self.length - self.H, self.length)) + require(3 * self.H <= self.length, "destination fields do not fit") + all_blocks = sources + destinations + require(all(not intersects(first, second) for i, first in enumerate(all_blocks) + for second in all_blocks[i + 1:]), + "source and destination fields must be pairwise disjoint") + object.__setattr__(self, "source_blocks", sources) + object.__setattr__(self, "destination_blocks", destinations) + + @property + def swaps(self) -> tuple[tuple[Interval, Interval], ...]: + """Three endpoint pairs; all six intervals are mutually disjoint.""" + return tuple(zip(self.source_blocks, self.destination_blocks)) + + @property + def cuts(self) -> tuple[int, ...]: + """At most twelve distinct endpoints of the six exchange intervals.""" + return tuple(sorted({point for block in self.source_blocks + self.destination_blocks + for point in block})) + + def map_position(self, position: int) -> int: + """Map an original bit to its current position; also the inverse map.""" + require(type(position) is int and 0 <= position < self.length, + "bit position out of range") + for source, destination in self.swaps: + if source[0] <= position < source[1]: + return position + destination[0] - source[0] + if destination[0] <= position < destination[1]: + return position + source[0] - destination[0] + return position + + def map_interval(self, lo: int, hi: int) -> tuple[Fragment, ...]: + """Split an original interval only at exchange cuts and translate it. + + Fragments are ordered by original position, so concatenating their + current bit slices reconstructs the original field. Their image + intervals need not occur in physical order. An empty input returns (). + """ + require(type(lo) is int and type(hi) is int and 0 <= lo <= hi <= self.length, + "physical interval out of range") + if lo == hi: + return () + boundaries = [lo] + [cut for cut in self.cuts if lo < cut < hi] + [hi] + fragments = [] + for start, stop in zip(boundaries, boundaries[1:]): + image_start = self.map_position(start) + fragments.append(Fragment((start, stop), (image_start, image_start + stop - start))) + return tuple(fragments) + + +@dataclass(frozen=True) +class Plan: + """A batch plus three disjoint source/destination field exchanges. + + partition is 0 or 1: a global half at non-root levels, and a quarter of + the logical right child at the root. batch_index starts at zero within + each partition. Every support interval is expressed before placement. + The Plan retains its shared Layout reference, not a copy of that index. + """ + + layout: Layout + level: int + partition: int + batch_index: int + active_axes: tuple[int, ...] + reservoir_axes: Interval + reservoir_interval: Interval + placement: Placement + dependencies: tuple[Dependency, ...] + + @property + def source_blocks(self) -> tuple[Interval, Interval, Interval]: + return self.placement.source_blocks + + @property + def destination_blocks(self) -> tuple[Interval, Interval, Interval]: + return self.placement.destination_blocks + + @property + def swaps(self) -> tuple[tuple[Interval, Interval], ...]: + return self.placement.swaps + + @property + def cuts(self) -> tuple[int, ...]: + return self.placement.cuts + + def map_position(self, position: int) -> int: + return self.placement.map_position(position) + + def map_interval(self, lo: int, hi: int) -> tuple[Fragment, ...]: + return self.placement.map_interval(lo, hi) + + @property + def descriptor_fragment_count(self) -> int: + """Exact number from splitting all d axes at the exchange endpoints. + + Every non-axis-boundary cut splits precisely one original axis. + This uses at most twelve binary searches and creates no d-axis list. + """ + return self.layout.d + sum(not self.layout.is_axis_boundary(cut) for cut in self.cuts) + + +def _active_in_region(lo: int, hi: int, width: int) -> Iterator[int]: + """Enumerate logical right-child axes of all nodes wholly in the region.""" + for start in range(lo, hi, width): + yield from range(start + width // 2, start + width) + + +def _regions(layout: Layout, level: int) -> Iterator[tuple[int, Iterator[int], Interval]]: + """Return partition, lazy active-axis stream, and unused logical interval.""" + half = layout.d // 2 + if level == layout.levels: + middle = half + layout.d // 4 + yield 0, iter(range(half, middle)), (middle, layout.d) + yield 1, iter(range(middle, layout.d)), (half, middle) + else: + width = 1 << level + yield 0, _active_in_region(0, half, width), (half, layout.d) + yield 1, _active_in_region(half, layout.d, width), (0, half) + + +def _make_plan(layout: Layout, level: int, partition: int, batch_index: int, + active_axes: tuple[int, ...], reservoir_axes: Interval) -> Plan: + reservoir = layout.axes_interval(*reservoir_axes) + require(8 * (reservoir[1] - reservoir[0]) >= layout.L, + "chosen reservoir is shorter than L/8") + field_bits = layout.H + free_lo = max(reservoir[0], 2 * field_bits) + free_hi = min(reservoir[1], layout.L - field_bits) + first = ((free_lo + field_bits - 1) // field_bits) * field_bits + require(first + 3 * field_bits <= free_hi, + "three aligned source fields do not fit after excluding destinations") + source_blocks = tuple((first + i * field_bits, first + (i + 1) * field_bits) + for i in range(3)) + placement = Placement(layout.L, field_bits, source_blocks) + width = 1 << level + dependencies = [] + for axis in active_axes: + node_start = axis // width * width + left_axes = (node_start, node_start + width // 2) + require(left_axes[1] <= axis < node_start + width, + "active axis is not in the node's right child") + own = layout.axis_interval(axis) + left = layout.axes_interval(*left_axes) + require(not intersects(reservoir, own) and not intersects(reservoir, left), + "reservoir intersects an active switch's original support") + dependencies.append(Dependency(axis, own, left_axes, left)) + return Plan(layout, level, partition, batch_index, active_axes, reservoir_axes, + reservoir, placement, tuple(dependencies)) + + +def iter_plans(layout: Layout, level: int | None = None) -> Iterator[Plan]: + """Yield the construction lazily, in increasing level/partition/batch order. + + level=None covers levels 1 through log2(d), each containing exactly d/2 + active axes. A supplied level selects only that level. Each partition's + right-child stream is cut into consecutive groups of at most r_max axes. + A group may cross a node boundary; its dependencies retain each node's + own left child. No list of all plans is constructed. + """ + require(isinstance(layout, Layout), "a validated Layout is required") + if level is None: + levels = range(1, layout.levels + 1) + else: + require(type(level) is int and 1 <= level <= layout.levels, + "tree level out of range") + levels = (level,) + for current_level in levels: + for partition, axes, reservoir_axes in _regions(layout, current_level): + batch_index = 0 + while True: + active = tuple(islice(axes, layout.r_max)) + if not active: + break + yield _make_plan(layout, current_level, partition, batch_index, + active, reservoir_axes) + batch_index += 1 diff --git a/research/pr4100-guard-coloring/verify.py b/research/pr4100-guard-coloring/verify.py new file mode 100644 index 0000000000..2d8998cd50 --- /dev/null +++ b/research/pr4100-guard-coloring/verify.py @@ -0,0 +1,232 @@ +#!/usr/bin/env python3 +"""Guard windows under #4100 CRT.md's position-mod-K coloring, on #4174's descriptors. + +Standard library only. Three parts: + +1. An exhaustive check of the window lemma on small position sets. +2. The compact gadget from #4100's own check_batched_crt.py on every one of + the 2^20 two-target addresses with targets exactly K apart: (K-1)-bit + guards versus literal K-bit guards. +3. A census of every one of #4174's production placement plans (vendored + allocator, byte-checked): targets in y, same-color pairs for any Beneš + bit schedule, exact-K spacings, and last-K exceptions. + +Finite evidence for the written lemma in README.md. Ryanson Jonathan with +Claude Code (Claude Opus 5.5) assistance. Apache-2.0. +""" +import hashlib +import importlib.util +import itertools +import json +from pathlib import Path +import sys + +ROOT = Path(__file__).resolve().parents[2] +HERE = Path(__file__).resolve().parent +SOURCE = ROOT / "research/unconditional-batched-crt" +ALLOCATOR_SHA256 = "b764195fc6291e3c8fa8297b1f4ceaefc119d5664d8ff348b49eac8a2e79c688" + + +def need(condition, message): + if not condition: + raise AssertionError(message) + + +PHRASES = [ + "from both ends of each K-bit guard. Its bad density is at most", + " r [2/B + 8B/2^K] <= C p 2^-G.", + "Color targets by current position modulo K, so guard intervals are disjoint.", +] +CODE_PHRASE = "2 * radix <= ((y >> (pos + 1)) & ((1 << (guard - 1)) - 1))" + + +def load(name, path): + spec = importlib.util.spec_from_file_location(name, path) + module = importlib.util.module_from_spec(spec) + sys.modules[name] = module # dataclasses resolve string annotations through sys.modules + spec.loader.exec_module(module) + return module + + +def check_sources(): + pins = {row["path"]: row["sha256"] + for row in json.loads((HERE / "SOURCES.json").read_text())["files"]} + for rel in ("research/unconditional-batched-crt/CRT.md", + "research/unconditional-batched-crt/check_batched_crt.py"): + need(hashlib.sha256((ROOT / rel).read_bytes()).hexdigest() == pins[rel], f"pin {rel}") + text = (SOURCE / "CRT.md").read_text() + for phrase in PHRASES: + need(phrase in text, f"CRT.md phrase missing: {phrase}") + need(CODE_PHRASE in (SOURCE / "check_batched_crt.py").read_text(), "good() uses guard-1 window bits") + vendored = HERE / "vendor/pr4174_allocator.py" + need(hashlib.sha256(vendored.read_bytes()).hexdigest() == ALLOCATOR_SHA256, + "vendored #4174 allocator bytes (head 5fec853f, blob 4b3ad896)") + return load("pr4100_crt", SOURCE / "check_batched_crt.py"), load("pr4174_allocator", vendored), len(PHRASES) + 2 + + +# --- 1. The window lemma ------------------------------------------------------------ + +def windows_ok(targets, K, width): + """Same-color (mod K) targets: are their width-bit windows above them free of active targets + and pairwise disjoint?""" + for c in range(K): + same = sorted(j for j in targets if j % K == c) + for a, b in itertools.combinations(same, 2): + if a < b <= a + width: # b inside a's window [a+1, a+width] + return False + if b + 1 <= a + width: # windows overlap (b's window starts at b+1) + return False + return True + + +def check_lemma(): + cases = 0 + for K in (3, 4, 6): + span = range(4 * K) + for size in (2, 3): + for targets in itertools.combinations(span, size): + need(windows_ok(targets, K, K - 1), "(K-1)-bit windows are always disjoint and target-free") + exact_k = any(b - a == K for a, b in itertools.combinations(sorted(targets), 2)) + need(windows_ok(targets, K, K) == (not exact_k), + "K-bit windows fail exactly when two same-color targets are K apart") + cases += 1 + return cases + + +# --- 2. #4100's gadget with K-bit versus (K-1)-bit guards --------------------------------- + +SOURCES_2T = { + "source_pair": lambda y: ((y >> 3) & 1, (y & ~65).bit_count() & 1), # #4100's own two-target source + "mixed_pair": lambda y: (((y >> 1) & 1) ^ ((y >> 11) & 1), ((y >> 5) & 1) & ((y >> 8) & 1)), +} + + +def check_gadget(crt): + """Targets at 0 and 6 (K = 6 apart), B = 4; guard g means g-1 window bits in the code.""" + rows = [] + for name, fn in SOURCES_2T.items(): + for guard in (6, 7): + good_n = disagree = leaves = 0 + example = None + for u in range(16): + for t in range(16): + for y in range(1 << 12): + if not crt.good(u, t, y, bits=2, positions=(0, 6), guard=guard): + continue + good_n += 1 + f0, f1 = fn(y) + ideal = (u, t, y ^ f0 ^ (f1 << 6)) + actual = crt.compact(u, t, y, fn, positions=(0, 6), ybits=12, control_bits=4) + if actual != ideal: + disagree += 1 + example = example or [[u, t, y], list(actual), list(ideal)] + if not crt.good(*ideal, bits=2, positions=(0, 6), guard=guard): + leaves += 1 + rows.append(dict(source=name, window_bits=guard - 1, good=good_n, + S_differs_from_T_on_good=disagree, T_leaves_good_set=leaves, + example=example)) + if guard == 6: + need(disagree == 0 and leaves == 0, "(K-1)-bit guards: the gadget is the ideal switch") + else: + need(disagree > 0 and leaves > 0, "K-bit guards at spacing K: the gadget fails on good addresses") + return rows + + +# --- 3. Census of #4174's production plans ------------------------------------------------- + +def census(alloc, ell, widths): + d = len(widths) + length = sum(widths) + layout = alloc.Layout(6 * length, ell, widths) + L, H, K = layout.L, layout.H, layout.K + y_lo, y_hi = 2 * H, L - H + ylen = y_hi - y_lo + stats = dict(d=d, ell=ell, L=L, G=layout.G, K=K, r_max=layout.r_max, H=H, y_bits=ylen, + plans=0, axis_visits=0, fragments=0, targets_outside_y=0, + possible_same_color_pairs=0, possible_exact_K_pairs=0, + plans_with_possible_exception_axes=0, + aligned_target_visits=0, aligned_max_color_multiplicity=0, + aligned_multi_target_colors=0, aligned_exact_K_pairs=0, + aligned_exception_layers=0, aligned_max_exceptions_per_layer=0, + max_pair_distance=0) + for plan in alloc.iter_plans(layout): + stats["plans"] += 1 + frags = [] + for dep in plan.dependencies: + lo, hi = dep.own_interval + fr = plan.map_interval(lo, hi) + for f in fr: + a, b = f.image_interval + if not (y_lo <= a and b <= y_hi): + stats["targets_outside_y"] += 1 + frags.append((dep.axis, lo, hi, fr)) + stats["axis_visits"] += 1 + stats["fragments"] += len(fr) + # Schedule-independent: can any bit of one active axis share a color with any bit of another? + exception_axes = 0 + for _, lo, hi, fr in frags: + if any(f.image_interval[0] < y_lo + K - 1 for f in fr): + exception_axes += 1 + stats["plans_with_possible_exception_axes"] += exception_axes > 0 + for (_, _, _, fa), (_, _, _, fb) in itertools.combinations(frags, 2): + for f, g in itertools.product(fa, fb): + dmin = g.image_interval[0] - (f.image_interval[1] - 1) + dmax = (g.image_interval[1] - 1) - f.image_interval[0] + stats["max_pair_distance"] = max(stats["max_pair_distance"], abs(dmin), abs(dmax)) + lo_m, hi_m = -(-dmin // K), dmax // K # multiples of K in [dmin, dmax] + if any(m != 0 for m in range(lo_m, hi_m + 1)): + stats["possible_same_color_pairs"] += 1 + if (dmin <= K <= dmax) or (dmin <= -K <= dmax): + stats["possible_exact_K_pairs"] += 1 + # Aligned Beneš schedule: at bit m, every active axis wider than m targets its bit m. + for m in range(ell): + js = [] + for _, lo, hi, fr in frags: + if hi - lo <= m: + continue + orig = hi - 1 - m + for f in fr: + if f.original_interval[0] <= orig < f.original_interval[1]: + cur = orig + f.delta + break + js.append((y_hi - 1) - cur) + stats["aligned_target_visits"] += len(js) + colors = {} + for j in js: + colors.setdefault(j % K, []).append(j) + for same in colors.values(): + stats["aligned_max_color_multiplicity"] = max(stats["aligned_max_color_multiplicity"], len(same)) + if len(same) > 1: + stats["aligned_multi_target_colors"] += 1 + same.sort() + stats["aligned_exact_K_pairs"] += sum(b - a == K for a, b in zip(same, same[1:])) + exceptions = sum(j > ylen - K for j in js) + if exceptions: + stats["aligned_exception_layers"] += 1 + stats["aligned_max_exceptions_per_layer"] = max(stats["aligned_max_exceptions_per_layer"], exceptions) + need(stats["targets_outside_y"] == 0, "every active axis lies in y after placement") + need(stats["aligned_max_color_multiplicity"] <= stats["r_max"], "a color never exceeds the batch") + return stats + + +def main(): + crt, alloc, phrases = check_sources() + lemma_cases = check_lemma() + gadget = check_gadget(crt) + widths = tuple(24 - (i % 2) for i in range(65536)) # #4174's production pattern + production = census(alloc, 24, widths) + need(production["plans"] == 104864 and production["axis_visits"] == 524288, + "same plan count as #4174's production census") + print(json.dumps({ + "status": "PASS_PR4100_GUARD_COLORING_FINITE", + "source_bindings": phrases, + "lemma_cases": lemma_cases, + "gadget": gadget, + "production_census": production, + "all_size_theorem_claimed": False, + "new_kappa_claimed": False, + }, indent=1)) + + +if __name__ == "__main__": + sys.exit(main()) From a3b9095c536c404e11d2ed868699fc4fcd4d4f57 Mon Sep 17 00:00:00 2001 From: Ryanson Jonathan Date: Wed, 21 Oct 2026 16:44:16 +0700 Subject: [PATCH 2/2] Census eight more width patterns and two adversarial ones for #4329 Blocked (both ways), uniform 24, uniform 23, three random and ell=32 patterns all have zero possible same-color pairs. Uniform 24 misses a multiple of K by one bit, and the admitted pattern with ell-1 axes 16384..16407 puts aligned same-color targets exactly K apart at 24 layers, where literal K-bit guards fail and (K-1)-bit windows are checked target-free. Co-Authored-By: Claude Opus 5.5 --- research/pr4100-guard-coloring/README.md | 59 ++++++++++++++++---- research/pr4100-guard-coloring/TASK.json | 12 ++-- research/pr4100-guard-coloring/VERIFY.json | 4 +- research/pr4100-guard-coloring/verify.py | 65 +++++++++++++++++++++- 4 files changed, 118 insertions(+), 22 deletions(-) diff --git a/research/pr4100-guard-coloring/README.md b/research/pr4100-guard-coloring/README.md index e29fe387b1..6948763f4a 100644 --- a/research/pr4100-guard-coloring/README.md +++ b/research/pr4100-guard-coloring/README.md @@ -91,18 +91,51 @@ fragments: 388,466 plan-layers contain exceptions, up to all 5 targets. At these sizes `K/|y| ≈ 13%`. #4187 audits that branch at `O(VK)`. +### 4. Other admitted width patterns + +The same census ran on eight more width patterns at `d = 65,536`, each +accepted by #4174's `Layout`: + +| Pattern | Plans | Possible same-color pairs | Aligned: max multiplicity / exact-`K` pairs | Plans with last-`K` axes | +| --- | --- | --- | --- | --- | +| alternating 24/23 (production) | 104,864 | 0 | 1 / 0 | 16,225 | +| blocked: 24 on axes 0..32767, then 23 | 104,864 | 0 | 1 / 0 | 16,534 | +| blocked: 23 on axes 0..32767, then 24 | 104,864 | 0 | 1 / 0 | 15,925 | +| uniform 24 | 104,864 | 0 | 1 / 0 | 15,899 | +| uniform 23 (all `ell−1`, `r_max = 4`) | 131,072 | 0 | 1 / 0 | 20,654 | +| random, half short, seed 4100 | 104,864 | 0 | 1 / 0 | 16,227 | +| random, half short, seed 4174 | 104,864 | 0 | 1 / 0 | 16,232 | +| random, 1/8 short, seed 4329 | 104,864 | 0 | 1 / 0 | 15,986 | +| alternating 32/31 (`ell = 32`, `K = 229,376`) | 104,864 | 0 | 1 / 0 | 14,078 | +| **uniform 24, one `ell−1` axis at 20000** | 104,864 | **1** (exact `K`) | 1 / 0 | 15,899 | +| **uniform 24, `ell−1` axes 16384..16407** | 104,864 | **1** (exact `K`) | **2 / 24** | 15,899 | + +In every pattern, every active axis lies in `y`, and wherever a color holds +two targets, the `(K−1)`-bit windows are checked directly to be target-free. + +**The vacuity is pattern-specific, and the `K−1` correction is needed on +admitted layouts.** Uniform 24 comes within one bit of a collision. At level +14, batch 1638 pairs axes 16383 and 24576. A batch can straddle a skipped +left half, and here the 8,193 axes between them span `196,632 = K + 24` bits. +Shortening 24 of the axes in between gives an admitted pattern (the last row) +where the aligned Beneš schedule puts two active targets of one color +**exactly `K` apart** at 24 layers. Under literal `K`-bit guards each such +target sits inside the other's window, which is the gadget failure of §2. +With `(K−1)`-bit guards those windows are target-free. Shortening a single +axis instead reaches exact `K` for some bit schedule, but not the aligned one. + ## Evidence -`verify.py` uses only the standard library and takes about 18 seconds. It +`verify.py` uses only the standard library and takes about 2 minutes (11 censuses). It also checks the source bindings: SHA256 pins of CRT.md and `check_batched_crt.py`, 3 exact CRT.md phrases, `good()`'s `guard−1` window expression, and the byte hash of the vendored allocator. ## Not covered -- Other production layouts. Only #4174's own pattern is censused here. - Other mixed-width patterns or larger `ell` could, in principle, create - same-color pairs; the lemma still covers them with `(K−1)`-bit guards. +- Other values of `d` and `ell`. Eleven patterns are censused at + `d = 65,536`, with `ell ∈ {24, 32}`. The lemma covers every descriptor with + `(K−1)`-bit guards. - The elementary last-`K` branch's correctness (#4187). - The control-function supports (#4169, #4174). - There is no proof-kernel check. @@ -120,17 +153,21 @@ The verifier prints `PASS_PR4100_GUARD_COLORING_FINITE`. ## Open next questions 1. **Price macros per occupied color, not per residue.** - - *Why it matters:* at production every color is a singleton, so a layer - uses at most `r_max` macros per batch rather than `K`. The tariff could + - *Why it matters:* in every regular pattern each color is a singleton, so + a layer uses at most `r_max` macros per batch rather than `K`. The tariff could be stated per occupied color. - *First step:* bound occupied colors per batch by `r_max` in the CRT §4 cost line. - *Blocked by:* nothing. -2. **Census other admitted width patterns.** - - *Why it matters:* the vacuity finding is pattern-specific. - - *First step:* run the census on blocked and random `ell`/`ell−1` - patterns at `d = 65,536`. - - *Blocked by:* nothing; about 20 seconds per pattern. +2. **Fix the window convention in the written construction.** (The earlier + question 2, other width patterns, is answered in §4.) + - *Why it matters:* an admitted layout puts same-color targets exactly `K` + apart, so the text's "K-bit guard" must become `(K−1)` bits, or the + coloring must be mod `K+1`. That change also changes #4321's hypothesis + wording. + - *First step:* restate CRT.md §4's predicate with `(K−1)`-bit windows and + re-derive `8B/2^K`. + - *Blocked by:* author or maintainer action on #4100's text. ## Credit diff --git a/research/pr4100-guard-coloring/TASK.json b/research/pr4100-guard-coloring/TASK.json index 8183a5f346..0d26da64ff 100644 --- a/research/pr4100-guard-coloring/TASK.json +++ b/research/pr4100-guard-coloring/TASK.json @@ -54,13 +54,13 @@ ] }, "scope_status": "refined", - "actual_scope": "Decide the disjoint-guard premise of #4100 CRT.md section 4 under position-mod-K coloring: a window lemma, a counterexample to the literal K-bit guard on #4100's own gadget, and a census of #4174's actual production placement descriptors.", + "actual_scope": "Decide the disjoint-guard premise of #4100 CRT.md section 4 under position-mod-K coloring: a window lemma, a counterexample to the literal K-bit guard on #4100's own gadget, and a census of #4174's actual production placement descriptors, plus eight further admitted width patterns and two adversarial ones.", "scope_change_reason": "The card asks for one quantified implication at its caller; this is the guard hypothesis that #4321 and #4328 assume and no audit decided, checked at the actual caller's descriptors (#4174).", "bottleneck_link": "The compact switch's correctness and the bad-density term both rest on this premise; a wrong window convention breaks the gadget on good addresses.", "budget_minutes": 75, "stop_rule": "Stop once the premise is decided (lemma plus counterexample) and checked on #4174's production descriptors.", "outcome": "completed", - "evidence": "verify.py: 3,266 exhaustive lemma cases; #4100's gadget on all 2^20 two-target addresses at spacing K: (K-1)-bit guards give S=T on all 82,944 good addresses, K-bit guards fail on 3,888/2,388 good addresses and T leaves the good set on 31,104/15,552; #4174 production census (104,864 plans, 524,288 axis visits): all axes in y, zero possible same-color pairs for any Benes schedule, aligned multiplicity 1, 16,225 plans with last-K exception axes.", + "evidence": "verify.py: 3,266 exhaustive lemma cases; #4100's gadget on all 2^20 two-target addresses at spacing K: (K-1)-bit guards give S=T on all 82,944 good addresses, K-bit guards fail on 3,888/2,388 good addresses and T leaves the good set on 31,104/15,552; #4174 production census (104,864 plans, 524,288 axis visits): all axes in y, zero possible same-color pairs for any Benes schedule, aligned multiplicity 1, 16,225 plans with last-K exception axes; eight more admitted patterns (blocked both ways, uniform 24, uniform 23, three random, ell=32): zero possible same-color pairs; uniform 24 misses a multiple of K by one bit, and the admitted pattern with ell-1 axes 16384..16407 puts aligned same-color targets exactly K apart at 24 layers, where (K-1)-bit windows are checked target-free.", "author": "Ryanson Jonathan, with Claude Code (Claude Opus 5.5) assistance", "ai_assistance": "Substantial Claude Code (Claude Opus 5.5) assistance in reading, the lemma, census implementation and writing; no independent human or proof-kernel review.", "open_questions": [ @@ -71,10 +71,10 @@ "blocked_by": "None." }, { - "question": "Census other admitted ell/ell-1 width patterns at d=65,536.", - "why_it_matters": "The vacuity of the premise at production is pattern-specific.", - "first_step": "Run the census on blocked and random width patterns.", - "blocked_by": "None; about 20 seconds per pattern." + "question": "Restate CRT.md section 4's guard with (K-1)-bit windows (or coloring mod K+1).", + "why_it_matters": "An admitted layout puts same-color targets exactly K apart, so the literal K-bit guard fails there; #4321's hypothesis wording follows the text.", + "first_step": "Restate the predicate with (K-1)-bit windows and re-derive the 8B/2^K term.", + "blocked_by": "Author or maintainer action on #4100's text." } ] } diff --git a/research/pr4100-guard-coloring/VERIFY.json b/research/pr4100-guard-coloring/VERIFY.json index 24c22289fb..0f96538e2a 100644 --- a/research/pr4100-guard-coloring/VERIFY.json +++ b/research/pr4100-guard-coloring/VERIFY.json @@ -14,8 +14,8 @@ "-B", "{package}/verify.py" ], - "timeout_seconds": 300, - "checks": "Source pins, CRT.md phrases, good()'s guard-1 window and the vendored #4174 allocator hash; exhaustive window lemma; #4100's two-target gadget with (K-1)-bit versus K-bit guards on all 2^20 addresses; census of all 104,864 #4174 production plans." + "timeout_seconds": 600, + "checks": "Source pins, CRT.md phrases, good()'s guard-1 window and the vendored #4174 allocator hash; exhaustive window lemma; #4100's two-target gadget with (K-1)-bit versus K-bit guards on all 2^20 addresses; census of all 104,864 #4174 production plans; eight further admitted width patterns and two adversarial ones with direct (K-1)-window checks." } ] } diff --git a/research/pr4100-guard-coloring/verify.py b/research/pr4100-guard-coloring/verify.py index 2d8998cd50..b0dc136a2a 100644 --- a/research/pr4100-guard-coloring/verify.py +++ b/research/pr4100-guard-coloring/verify.py @@ -199,7 +199,10 @@ def census(alloc, ell, widths): if len(same) > 1: stats["aligned_multi_target_colors"] += 1 same.sort() - stats["aligned_exact_K_pairs"] += sum(b - a == K for a, b in zip(same, same[1:])) + gaps = [b - a for a, b in zip(same, same[1:])] + # (K-1)-bit windows [j+1, j+K-1]: disjoint and free of the other targets iff every gap >= K. + need(all(gap >= K for gap in gaps), "(K-1)-bit windows are target-free on actual descriptors") + stats["aligned_exact_K_pairs"] += sum(gap == K for gap in gaps) exceptions = sum(j > ylen - K for j in js) if exceptions: stats["aligned_exception_layers"] += 1 @@ -209,20 +212,76 @@ def census(alloc, ell, widths): return stats +def random_widths(ell, seed, short_fraction): + """Deterministic pseudo-random ell/ell-1 pattern (64-bit LCG, no external state).""" + state, out = seed, [] + for _ in range(65536): + state = (6364136223846793005 * state + 1442695040888963407) % (1 << 64) + out.append(ell - 1 if (state >> 11) / (1 << 53) < short_fraction else ell) + return tuple(out) + + +HALF = 32768 +PATTERNS = [ + ("alternating 24/23 (#4174 production)", 24, tuple(24 - (i % 2) for i in range(65536))), + ("blocked: 24 on axes 0..32767, then 23", 24, (24,) * HALF + (23,) * HALF), + ("blocked: 23 on axes 0..32767, then 24", 24, (23,) * HALF + (24,) * HALF), + ("uniform 24", 24, (24,) * 65536), + ("uniform 23 (all ell-1)", 24, (23,) * 65536), + ("random, half short, seed 4100", 24, random_widths(24, 4100, 0.5)), + ("random, half short, seed 4174", 24, random_widths(24, 4174, 0.5)), + ("random, 1/8 short, seed 4329", 24, random_widths(24, 4329, 0.125)), + ("alternating 32/31", 32, tuple(32 - (i % 2) for i in range(65536))), +] + + +def with_short(shorts): + widths = [24] * 65536 + for i in shorts: + widths[i] = 23 + return tuple(widths) + + +# Uniform 24 misses a multiple of K by one bit: at level 14, batch 1638 pairs axes 16383 and +# 24576, which are 8,193 axes = 196,632 = K + 24 bits apart. Shortening axes between them +# lands pairs exactly on K. Both patterns are admitted by #4174's Layout. +ADVERSARIAL = [ + ("uniform 24, one ell-1 axis at 20000", 24, with_short([20000]), "possible"), + ("uniform 24, ell-1 axes 16384..16407", 24, with_short(range(16384, 16408)), "aligned"), +] + + def main(): crt, alloc, phrases = check_sources() lemma_cases = check_lemma() gadget = check_gadget(crt) - widths = tuple(24 - (i % 2) for i in range(65536)) # #4174's production pattern - production = census(alloc, 24, widths) + production = census(alloc, 24, PATTERNS[0][2]) need(production["plans"] == 104864 and production["axis_visits"] == 524288, "same plan count as #4174's production census") + patterns = [dict(pattern=PATTERNS[0][0], short_axes=PATTERNS[0][2].count(23), **production)] + for name, ell, widths in PATTERNS[1:]: + patterns.append(dict(pattern=name, short_axes=widths.count(ell - 1), **census(alloc, ell, widths))) + for row in patterns: + need(row["possible_same_color_pairs"] == 0 and row["aligned_max_color_multiplicity"] == 1, + f"no same-color pair on the regular pattern {row['pattern']}") + for name, ell, widths, kind in ADVERSARIAL: + row = dict(pattern=name, short_axes=widths.count(ell - 1), **census(alloc, ell, widths)) + need(row["possible_exact_K_pairs"] > 0, f"exact-K spacing reachable on {name}") + if kind == "aligned": + need(row["aligned_exact_K_pairs"] > 0, f"aligned schedule puts same-color targets exactly K apart on {name}") + patterns.append(row) print(json.dumps({ "status": "PASS_PR4100_GUARD_COLORING_FINITE", "source_bindings": phrases, "lemma_cases": lemma_cases, "gadget": gadget, "production_census": production, + "pattern_census": [{k: row[k] for k in ( + "pattern", "ell", "short_axes", "L", "K", "r_max", "plans", "targets_outside_y", + "possible_same_color_pairs", "possible_exact_K_pairs", "aligned_target_visits", + "aligned_max_color_multiplicity", "aligned_multi_target_colors", "aligned_exact_K_pairs", + "plans_with_possible_exception_axes", "aligned_max_exceptions_per_layer", "max_pair_distance")} + for row in patterns], "all_size_theorem_claimed": False, "new_kappa_claimed": False, }, indent=1))