From 198ffb11a8bb82c71d7dafb6a5cb137728b01362 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 3 Nov 2026 14:03:23 +0000 Subject: [PATCH] feat(research): construct minimum exact union state headers --- research/union-state-header/PROOF.md | 113 ++++++++++++++++ research/union-state-header/README.md | 126 ++++++++++++++++++ research/union-state-header/SOURCES.json | 30 +++++ research/union-state-header/TASK.json | 90 +++++++++++++ research/union-state-header/VERIFY.json | 37 ++++++ research/union-state-header/codec.py | 119 +++++++++++++++++ research/union-state-header/verify.py | 160 +++++++++++++++++++++++ 7 files changed, 675 insertions(+) create mode 100644 research/union-state-header/PROOF.md create mode 100644 research/union-state-header/README.md create mode 100644 research/union-state-header/SOURCES.json create mode 100644 research/union-state-header/TASK.json create mode 100644 research/union-state-header/VERIFY.json create mode 100644 research/union-state-header/codec.py create mode 100644 research/union-state-header/verify.py diff --git a/research/union-state-header/PROOF.md b/research/union-state-header/PROOF.md new file mode 100644 index 0000000000..ffd181157e --- /dev/null +++ b/research/union-state-header/PROOF.md @@ -0,0 +1,113 @@ +# Exact minimum header width + +This contribution was produced by Nick Petalas. Apache-2.0. + +## Contract + +Fix integers L>=2 and g>=1 and shared sorted sets E_i contained in +{0,...,L-1}, with a_i=|E_i|. A coordinate vector x has g entries in that +range. The legal tag is either the sentinel g or an axis i with x_i in E_i. +The flags, canonical boundary ordinals and flag count are determined by x +and the shared sets. An unflagged ordinal is zero. This is the full legal +header domain of Mihir Srivastava's PR4583, including sentinel records +outside the sparse union. There is no restriction on the payload. + +A record has a fixed two-bit marker 01 followed by a fixed number of data +bits. The decoder knows L, g and every E_i, but receives no record-dependent +side information or previous record state. Records must decode individually +and exactly. We optimize width within this contract, without a locality, +time or fixed-tape requirement. Context storage is outside that width. + +## Theorem + +The number of legal headers is exactly + + N = L^(g-1) (L + sum_i a_i). + +Their minimum fixed width, including the marker, is + + H* = 2 + ceil(log2 N). + +Writing h=ceil(log2 L) and b=ceil(log2(g+1)), it satisfies + + H* <= 2 + gh + b. + +Compared with PR4583's separate-field width + + H_old = 2 + 2gh + g + 2b, + +this saves at least gh+g+b bits at every allowed context. All flags, +ordinals, count, tag, active-round choice, prefix keys and keep decisions +remain exactly recoverable. This is a representation theorem, with no +claim about physical time, tape travel or the full multiplication theorem. + +## Counting and lower bound + +Partition legal headers by tag. The sentinel block has all L^g coordinate +vectors. The block tagged i has a_i choices for coordinate i and L choices +for every other coordinate, hence a_i L^(g-1) states. Blocks are disjoint +because their tags differ, even when the same coordinate occurs in several +blocks. Summing proves the formula. Flags, ordinals and count add no states, +since they are determined by the coordinate and shared context. + +A width-H record with marker 01 has at most 2^(H-2) distinct bit strings. +Exact decoding requires distinct legal headers to have distinct strings, +including headers sharing coordinates but having different legal tags. +Therefore 2^(H-2)>=N, giving the stated lower bound for every encoder, +including nonlinear encoders. The conclusion does not apply to variable +lengths, joint compression across records or an additional side channel. + +## Attaining construction + +Order the blocks as sentinel, axis 0, ..., axis g-1. The sentinel block +starts at zero. Axis i starts at + + L^g + L^(g-1) sum_{j=N are rejected. + +Given the recovered coordinate, sorted-set membership and rank recover every +flag and ordinal, hence the count. The round-r active axis is the r-th set +flag, for zero-based rr+1. +Retagging re-encodes the same coordinate with that active axis. These are +semantic operations; they make no assertion about in-place reversibility +or preservation of an arbitrary previous tag. + +Finally a_i<=L implies N<=(g+1)L^g<=2^(b+gh). Thus ceil(log2 N)<=b+gh. +Subtracting this upper bound from H_old gives the uniform saving. For +L=16, g=4 and each E_i={0,15}, N=98,304, so H*=19 while H_old=44. + +## Scope and implementation + +Enumerative coding, mixed-radix conversion and the pigeonhole principle are +classical. The contribution is their exact application to this full legal +union-header domain and the new bounded reference codec. The prior field +codec and its scientific checks are not replayed or audited here. + +The written construction holds for arbitrary finite contexts. codec.py +implements it within explicit capacities of 32 axes, L<=2^4096 and 128 +entries per boundary set. It never enumerates the coordinate box. Boundary +queries use the supplied sorted lists. The bit-width theorem does not charge +those lists, arithmetic temporaries, rank/select access or decoding travel. +In particular, the old tag-only update is replaced by a possible whole-index +rewrite. Identical contexts may share code words; context boundaries remain +required. Some bit changes produce another legal state, so this format is +not an error-detecting code. + +The universal claim rests on this written proof. Finite execution corroborates +only its declared domains. No physical caller, selected-frontier change, +new kappa or discharge of the five inherited assumptions follows. diff --git a/research/union-state-header/README.md b/research/union-state-header/README.md new file mode 100644 index 0000000000..a10425ae1d --- /dev/null +++ b/research/union-state-header/README.md @@ -0,0 +1,126 @@ +# Minimum exact state headers for sparse-union records + +This contribution was produced by Nick Petalas. Apache-2.0. + +Claim type: scoped written construction and sharp information bound, with +exact finite corroboration. No new kappa is claimed. + +For a shared context of g axes, side L>=2 and boundary sets E_i of sizes a_i, +the full legal coordinate/tag header domain of Mihir Srivastava's +[PR4583](https://github.com/CrocSwap/integer-mult-bounds/pull/4583) has exactly + + N = L^(g-1) (L + sum_i a_i) + +states. The new mixed-radix codec uses the minimum possible fixed width + + H* = 2 + ceil(log2 N) + +including the retained two-bit marker. It recovers every coordinate, flag, +canonical ordinal, count and tag. The minimum covers arbitrary encoders with +individual exact decoding under the same fixed shared context. + +For h=ceil(log2 L), b=ceil(log2(g+1)), this saves at least gh+g+b bits against +the predecessor's separate-field format. At L=16, g=4 and E_i={0,15}, all +98,304 legal states fit in 19 bits including framing; that format uses 44. +[PROOF.md](PROOF.md) gives the disjoint-tag count, matching lower bound and +attaining rank/unrank construction. [codec.py](codec.py) implements it. + +The source metadata contract is a cited premise. Its codec, schedule and +scientific results are not replayed or audited. The new finite enumeration +checks the new representation directly against the legal-state definition. + +## Evidence and reproduction + +From the repository root, using CPython 3.12 and its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/union-state-header/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/union-state-header/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/union-state-header +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/union-state-header --check-source-history --check-modes +``` + +Substitute another CPython 3.12 executable on other machines. Direct replay +prints PASS_UNION_STATE_HEADER and a generated JSON receipt bound to every +package file and both declared source inputs. It writes nothing. + +The finite domain includes every boundary subset and every legal state for +L=2 with g=1..4, L=3 with g=1..3 and L=4 with g=1..2. It enumerates 1,196 +contexts and 57,744 legal states, checks 105,120 retags and their line keys, +and rejects all 22,022 unused codes within those record widths. Sixty larger +rank/serialization round trips reach L=2^4096 and g=32. Twenty-seven explicit +controls reject malformed contexts, coordinates, tags, indices, framing, +rounds and mismatched line keys. A collision control retains the distinction +between active and sentinel tags on the same coordinates. A legal substitution +control makes explicit that this is not an error-detecting code. + +Normal and optimized commands execute the same always-enabled contracts. +Registered replays are bounded individually by 120 seconds. The universal +conclusion rests on the written proof, not on a finite census. + +## Scope, credit and overlap + +The shared boundary sets are decoder context. Rank/select access, arbitrary +precision arithmetic, context storage and temporary space are not free in a +physical implementation. Retagging may rewrite the entire index. The old +format's tag-local update and direct metadata fields are not preserved as +locality guarantees. No faster reader, fixed-tape saving or complete emitter +is supplied. Context boundaries remain necessary, and payloads are untouched. +The result does not implement an arbitrary-dirty reversible retagging map. + +Credit Mihir Srivastava / mihir-s-05, PR4583, for the precise metadata contract +and separate-field header. Retain Cinna Davis / PR4100, Jeremy Kothe / PR1731, +Vlado Vojdanovski / PR1673, Ryanson Jonathan / PR4327 and PR4590, unpaidmoon / +PR4376, rtyu193-rgb and LeverRank's schedule, layout and review lineage. +Enumerative coding, mixed-radix indexing and the pigeonhole principle are +classical. This contribution applies them to that interface and supplies the +smaller exact codec; no general literature-priority claim is made. + +Canonical base is 7c49fe32c55de02c2c873655c804b16e4c3fef0a, priority revision 8, +selected PR6030. SOURCES.json binds the unmodified contract and field-codec +bytes. The card changes from a selected-assumption audit to this representation +side result for precision_tape. The source-binding orientation passed. +The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19375380) +records the target and stop rule. The cached overlap snapshot covers 572 open +PRs and 6,641 Discussion records with complete reported remote pagination. +Only 141 of 8,917 local note paths were materialized. Separate main-wide +README searches and live merged/general-form searches supplement that sparse +coverage. Historical diffs and unpublished work remain limits. + +No selected cold replay, Lean or Docker run is needed for this side result. +All five selected framework assumptions remain. Independent human and formal +proof-kernel review are unclaimed. This is not a physical supplier, selected +frontier change or complete multiplication theorem. + +## Open next questions + +Can an actual union invocation use this representation with a favorable full +reader, emitter and retagging bill? Start with one carving description, bind +rank/select access, and charge every header rewrite and temporary through one +round. Missing bit-level decoding, context delivery and complete caller costs +block an operational saving. TASK.json records this handoff explicitly. + +## Code bounds and diagnostics + +The codec has at most 32 axes, 128 entries per boundary and L<=2^4096, giving +at most 131,078 index bits and 131,080 serialized bits. No coordinate box is +materialized by rank/unrank. Each codec loop has at most 32 iterations, and +boundary validation operates on at most 128 entries. The exhaustive verifier +retains at most 108 ranks per context. Its context and fixture domains are +fixed as listed above. Source reads are capped at one MiB and the manifest +at sixteen rows; the package receipt covers seven fixed filenames. Functions +stay below sixty physical lines. Warning-strict normal and optimized replay +provide the available runtime diagnostics; no unavailable static analyzer is +claimed as run. + +Power-of-Ten rule 3 has a managed-runtime deviation in codec.py and verify.py. +Python allocates integers, strings, tuples, sets and JSON values during the +run. The enforced dimensions, integer and header lengths, bounded live rank +set, capped input reads and streamed contexts bound their sizes. This is not +a static-pool or byte-exact heap bound. Reassess these bounds before enlarging +the capacities; a fixed-pool backend would be a separate implementation. +Rule 9's verifier callback deviation is confined to explicit negative-test +calls to Layout and its encode, decode, unrank, retag and line_key methods. +No dynamic code or unbounded dispatch is accepted. Normal and optimized +negative controls exercise every listed target. Production codec calls are +direct, and decoded Header values and boundary tuples are immutable. diff --git a/research/union-state-header/SOURCES.json b/research/union-state-header/SOURCES.json new file mode 100644 index 0000000000..ab386545f4 --- /dev/null +++ b/research/union-state-header/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/union-header-encoding/README.md", + "usage": "input", + "git_blob": "790660a0a0f0c8cbb7945ce766ce8600d8c1dde1", + "sha256": "320345a6ed2b7ca82057c4b2a9551c664cd96b5c387e43e6c3a98b422bd77d9a" + }, + { + "path": "research/union-header-encoding/header.py", + "usage": "input", + "git_blob": "424699d49c57e762ca5f04091bfab8f8d145d14c", + "sha256": "9e24704bf2b73e5c812827ed03aa9f2fcb8a1999c079ba1d260f7658020e69aa" + } + ] +} diff --git a/research/union-state-header/TASK.json b/research/union-state-header/TASK.json new file mode 100644 index 0000000000..0433c869fc --- /dev/null +++ b/research/union-state-header/TASK.json @@ -0,0 +1,90 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Choose one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "native_all_columns", + "owned_erasure", + "compiler", + "precision_tape", + "analytic_recovery" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "An information-optimal fixed-width encoding of the full legal PR4583 coordinate/tag header domain, with an attaining mixed-radix codec.", + "scope_change_reason": "Replace a supplier-assumption audit by a new smaller representation at the existing per-microbox metadata contract. This is a side result for precision_tape; physical reader and emitter costs are not discharged.", + "bottleneck_link": "The sparse-union tape invoice depends on record width. The new representation removes redundant metadata at the information level; physical adoption needs a separately charged decoder and retagging implementation.", + "budget_minutes": 60, + "stop_rule": "Stop at the first strict width improvement, exact fixed-width lower bound and bounded corroboration. Do not expand into a physical caller or replay predecessor mathematics.", + "outcome": "completed", + "evidence": "PROOF.md establishes the all-size count, optimality and rank/unrank construction. verify.py independently enumerates the declared small legal state domains and checks metadata queries, unused code rejection, large indices and invalid inputs.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can an actual union invocation use this representation with a favorable complete reader, emitter and retagging bill?", + "why_it_matters": "Smaller records do not by themselves reduce tape cost; retagging here may rewrite every index bit.", + "first_step": "Bind one carving description to rank/select access and measure all header reads, rewrites and temporary storage through one round.", + "blocked_by": "No bit-level fixed-tape decoder, carving producer, context delivery or complete caller budget is supplied." + } + ], + "coordination": { + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19375380", + "source_pr": 4583, + "source_author": "mihir-s-05", + "freshness_utc": "2026-11-03T13:57:00Z", + "overlap_limits": "Capped live PR searches, sparse historical notes, arbitrary diffs and unpublished work do not establish novelty." + } +} diff --git a/research/union-state-header/VERIFY.json b/research/union-state-header/VERIFY.json new file mode 100644 index 0000000000..0ca03a2036 --- /dev/null +++ b/research/union-state-header/VERIFY.json @@ -0,0 +1,37 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/union-header-encoding/README.md", + "research/union-header-encoding/header.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Independent complete legal-state enumeration, exact index bijection and minimum width, all metadata/retag queries, unused codes and invalid-domain controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same exact coverage with Python assertions disabled; all contracts remain enabled." + } + ] +} diff --git a/research/union-state-header/codec.py b/research/union-state-header/codec.py new file mode 100644 index 0000000000..ef35976f9a --- /dev/null +++ b/research/union-state-header/codec.py @@ -0,0 +1,119 @@ +"""Exact joint headers, produced by Nick Petalas. Apache-2.0. + +This is an information codec, not a fixed-tape implementation. +""" + +from bisect import bisect_left +from dataclasses import dataclass + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +@dataclass(frozen=True) +class Header: + coordinates: tuple + flags: tuple + ordinals: tuple + count: int + tag: int + + +class Layout: + """At most 32 axes, 4096 side bits and 128 boundary entries per axis.""" + + def __init__(self, side, boundaries): + require(type(side) is int and 2 <= side <= 1 << 4096, "side domain") + require(type(boundaries) in (tuple, list), "boundary container") + require(1 <= len(boundaries) <= 32, "axis capacity") + for boundary in boundaries: + require(type(boundary) in (tuple, list), "boundary container") + require(len(boundary) <= 128, "boundary capacity") + require(all(type(v) is int and 0 <= v < side for v in boundary), + "boundary coordinate") + require(tuple(boundary) == tuple(sorted(set(boundary))), + "boundary ordering") + self.side = side + self.boundaries = tuple(tuple(e) for e in boundaries) + self.g = len(self.boundaries) + self.plane = side ** (self.g - 1) + self.sentinel_size = side * self.plane + self.states = self.plane * (side + sum(map(len, self.boundaries))) + self.index_bits = (self.states - 1).bit_length() + self.width = self.index_bits + 2 + + def describe(self, coordinates, tag=None): + require(type(coordinates) in (tuple, list), "coordinate container") + require(len(coordinates) == self.g, "coordinate count") + require(all(type(v) is int and 0 <= v < self.side for v in coordinates), + "coordinate domain") + tag = self.g if tag is None else tag + require(type(tag) is int and 0 <= tag <= self.g, "tag domain") + flags, ordinals = [], [] + for value, boundary in zip(coordinates, self.boundaries): + rank = bisect_left(boundary, value) + member = rank < len(boundary) and boundary[rank] == value + flags.append(int(member)) + ordinals.append(rank if member else 0) + require(tag == self.g or flags[tag] == 1, "unflagged tag") + return Header(tuple(coordinates), tuple(flags), tuple(ordinals), + sum(flags), tag) + + def rank(self, coordinates, tag=None): + record = self.describe(coordinates, tag) + value = 0 + for axis, coordinate in enumerate(record.coordinates): + radix = self.side + if axis == record.tag: + radix = len(self.boundaries[axis]) + coordinate = record.ordinals[axis] + value = value * radix + coordinate + if record.tag < self.g: + before = sum(len(e) for e in self.boundaries[:record.tag]) + value += self.sentinel_size + before * self.plane + require(0 <= value < self.states, "internal rank range") + return value + + def unrank(self, value): + require(type(value) is int and 0 <= value < self.states, "index domain") + tag = self.g + if value >= self.sentinel_size: + value -= self.sentinel_size + for axis, boundary in enumerate(self.boundaries): + size = len(boundary) * self.plane + if value < size: + tag = axis + break + value -= size + require(tag < self.g, "internal block selection") + coordinates = [0] * self.g + for axis in range(self.g - 1, -1, -1): + radix = len(self.boundaries[axis]) if axis == tag else self.side + value, digit = divmod(value, radix) + coordinates[axis] = self.boundaries[axis][digit] if axis == tag else digit + require(value == 0, "internal mixed-radix remainder") + return self.describe(coordinates, tag) + + def encode(self, coordinates, tag=None): + value = self.rank(coordinates, tag) + return "01" + format(value, f"0{self.index_bits}b") + + def decode(self, encoded): + require(type(encoded) is str and len(encoded) == self.width, "header length") + require(set(encoded) <= {"0", "1"} and encoded[:2] == "01", "header marker") + return self.unrank(int(encoded[2:], 2)) + + def retag(self, encoded, round_index): + record = self.decode(encoded) + require(type(round_index) is int and 0 <= round_index < record.count, + "inactive round") + axes = tuple(axis for axis, flag in enumerate(record.flags) if flag) + return self.encode(record.coordinates, axes[round_index]) + + def line_key(self, encoded, round_index): + updated = self.retag(encoded, round_index) + record = self.decode(updated) + require(record.tag == self.decode(encoded).tag, "wrong round tag") + return record.coordinates[:record.tag], record.ordinals[record.tag] diff --git a/research/union-state-header/verify.py b/research/union-state-header/verify.py new file mode 100644 index 0000000000..390effabd0 --- /dev/null +++ b/research/union-state-header/verify.py @@ -0,0 +1,160 @@ +"""Bounded exact corroboration, produced by Nick Petalas. Apache-2.0.""" + +import hashlib +import itertools +import json +from pathlib import Path +import sys + +# -I removes the script directory. Resolve just this package's sibling module. +sys.path.insert(0, str(Path(__file__).resolve().parent)) +from codec import Header, Layout + + +def check(condition, message): + if not condition: + raise AssertionError(message) + + +def read_small(path): + check(path.stat().st_size <= 1 << 20, "source file exceeds one MiB") + return path.read_bytes() + + +def expect_rejection(operation, *arguments): + try: + operation(*arguments) + except ValueError: + return 1 + raise AssertionError("invalid input accepted") + + +def literal_states(side, boundaries): + """Independent semantic enumeration, without index arithmetic.""" + g = len(boundaries) + for x in itertools.product(range(side), repeat=g): + flags = tuple(int(value in e) for value, e in zip(x, boundaries)) + ordinals = tuple(e.index(value) if flag else 0 + for value, e, flag in zip(x, boundaries, flags)) + for tag in (g,) + tuple(i for i, flag in enumerate(flags) if flag): + yield Header(x, flags, ordinals, sum(flags), tag) + + +def check_context(side, boundaries): + layout = Layout(side, boundaries) + ranks = set() + states = retags = unused = 0 + for expected in literal_states(side, boundaries): + rank = layout.rank(expected.coordinates, expected.tag) + check(rank not in ranks, "two legal states collide") + ranks.add(rank) + encoded = layout.encode(expected.coordinates, expected.tag) + check(len(encoded) == layout.width, "nonconstant record width") + check(layout.decode(encoded) == expected, "semantic round trip") + check(layout.unrank(rank) == expected, "index round trip") + for round_index in range(expected.count): + updated = layout.retag(encoded, round_index) + axis = tuple(i for i, flag in enumerate(expected.flags) if flag)[round_index] + actual = layout.decode(updated) + check(actual == Header(expected.coordinates, expected.flags, + expected.ordinals, expected.count, axis), + "retag metadata") + check(layout.line_key(updated, round_index) == + (expected.coordinates[:axis], expected.ordinals[axis]), "line key") + retags += 1 + states += 1 + check(ranks == set(range(layout.states)), "rank map is not onto") + check(states == layout.states, "closed state count") + check(1 << (layout.index_bits - 1) < states <= 1 << layout.index_bits, + "fixed-width information minimum") + old = 2 + 2 * layout.g * (side - 1).bit_length() + layout.g + 2 * layout.g.bit_length() + gain = layout.g * (side - 1).bit_length() + layout.g + layout.g.bit_length() + check(old - layout.width >= gain, "uniform width improvement") + for index in range(layout.states, 1 << layout.index_bits): + unused += expect_rejection(layout.decode, "01" + format(index, f"0{layout.index_bits}b")) + return states, retags, unused + + +def exhaustive(): + totals = {"contexts": 0, "states": 0, "retags": 0, "unused_codes_rejected": 0} + for side, maximum_axes in ((2, 4), (3, 3), (4, 2)): + subsets = tuple(tuple(i for i in range(side) if mask >> i & 1) + for mask in range(1 << side)) + for g in range(1, maximum_axes + 1): + for boundaries in itertools.product(subsets, repeat=g): + values = check_context(side, boundaries) + totals["contexts"] += 1 + for key, value in zip(("states", "retags", "unused_codes_rejected"), values): + totals[key] += value + return totals + + +def large_and_controls(): + count = 0 + for exponent in (8, 31, 127, 1024, 4096): + side = 1 << exponent + for g in (1, 2, 7, 32): + boundaries = tuple((0, side - 1) if i % 2 else () for i in range(g)) + layout = Layout(side, boundaries) + for index in (0, layout.sentinel_size - 1, layout.states - 1): + record = layout.unrank(index) + check(layout.rank(record.coordinates, record.tag) == index, "large index") + check(layout.decode(layout.encode(record.coordinates, record.tag)) == record, + "large serialization") + count += 1 + layout = Layout(3, ((1,), ())) + encoded = layout.encode((1, 2), 0) + controls = 0 + for args in ((1, ((0,),)), (3, ()), (3, ((1, 1),)), (3, ((2, 1),)), + (3, ((3,),)), (3, ((True,),)), (3, ((0,),) * 33), + (1 << 4097, ((0,),)), (256, (tuple(range(129)),))): + controls += expect_rejection(Layout, *args) + for x, tag in (((1,), 0), ((1, 3), 0), ((0, 2), 0), ((1, 2), 1), + ((1, 2), 3), ((True, 2), 0), ((1, 2), True)): + controls += expect_rejection(layout.encode, x, tag) + for value in (-1, layout.states, True): + controls += expect_rejection(layout.unrank, value) + for value in (encoded[:-1], encoded + "0", "00" + encoded[2:], "x" + encoded[1:]): + controls += expect_rejection(layout.decode, value) + for round_index in (-1, 1, True): + controls += expect_rejection(layout.retag, encoded, round_index) + controls += expect_rejection(layout.line_key, layout.encode((1, 2)), 0) + check(layout.rank((1, 2), 0) != layout.rank((1, 2)), "tag collision control") + check(layout.decode(layout.encode((0, 0))).coordinates == (0, 0), "legal substitution") + witness = Layout(16, ((0, 15),) * 4) + check((witness.states, witness.width) == (98304, 19), "strict improvement fixture") + return {"large_round_trips": count, "domain_controls": controls, + "witness_states": witness.states, "witness_old_bits": 44, + "witness_new_bits": witness.width} + + +def source_hashes(package): + manifest = json.loads(read_small(package / "SOURCES.json")) + check(len(manifest["files"]) <= 16, "source manifest capacity") + root = package.parents[1] + hashes = {} + for row in manifest["files"]: + if row["usage"] == "input": + path = root / row["path"] + digest = hashlib.sha256(read_small(path)).hexdigest() + check(digest == row["sha256"], "changed source input: " + row["path"]) + hashes[row["path"]] = digest + return hashes + + +def main(): + package = Path(__file__).resolve().parent + inputs = source_hashes(package) + result = exhaustive() + result.update(large_and_controls()) + result["inputs_sha256"] = inputs + names = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", + "codec.py", "verify.py") + result["package_sha256"] = { + name: hashlib.sha256(read_small(package / name)).hexdigest() for name in names} + print("PASS_UNION_STATE_HEADER") + print(json.dumps(result, sort_keys=True)) + + +if __name__ == "__main__": + main()