diff --git a/research/unique-write-xor-batching/README.md b/research/unique-write-xor-batching/README.md new file mode 100644 index 0000000000..c5806fcd3a --- /dev/null +++ b/research/unique-write-xor-batching/README.md @@ -0,0 +1,223 @@ +# Exact batching of unique-destination dirty XOR sweeps + +This contribution was produced by Nick Petalas. Apache-2.0. + +**Scoped proof with exact finite corroboration; no new κ.** For a finite +ordered list of in-place XORs with distinct destinations, serial execution +equals entry-snapshot execution on every dirty input exactly when no event +reads a cell written by an earlier event. Every failed guard has a concrete +single-basis-input discrepancy. A safe reordering exists exactly when the +directed source-to-destination graph is acyclic. + +The contribution is the exact batching contract, necessity proof and executable +witness guard. Read-before-write dependency scheduling and topological sorting +are standard background; no historical-priority claim is made for those ideas. +Rohan Arun's [PR409](https://github.com/CrocSwap/integer-mult-bounds/pull/409) +already uses read-before-write as a sufficient premise for a particular +rational entrance-shear word; [PR413](https://github.com/CrocSwap/integer-mult-bounds/pull/413) +retains it. The additional step here is necessity with a final-state witness +and an exact safe-ordering criterion under the Boolean unique-write contract. +Neither predecessor's word or reported bound is replayed here. + +## Contract and theorem + +Let `V` be any finite set of cells and let each payload be an element of any +nonzero vector space `W` over `F2`. In particular, payloads may be arbitrary +dirty bit strings or Boolean functions on a common address set. They may be +correlated. For an ordered word of `m` events, write + +```text +event j: x[t_j] <- x[t_j] XOR x[s_j] +``` + +Require `t_j != s_j` and require every `t_j` to be distinct. No other +operations, hidden writes or changes of coordinate encoding occur inside +the word. Extra cells are allowed and remain untouched unless named. + +The snapshot endpoint is the linear map `S` defined by +`S(x)[t_j] = x[t_j] XOR x[s_j]`, with every right-hand value taken from the +entry state; unselected cells retain their entry values. Let `P` be the +literal serial in-place map. + +**Theorem 1.** The following are equivalent: + +1. `P(x)=S(x)` for every input `x in W^V`. +2. There are no indices `i t_j` is acyclic. + +If a safe order exists, Theorem 1 requires every edge leaving a cell to +precede the edge entering that cell, whenever both exist. A directed cycle +would impose a strict cyclic order on its edges, which is impossible. +Conversely, in a DAG process vertices in reverse topological order and +execute the event entering each vertex, if present. Every edge leaving a +cell then precedes its unique incoming edge, so no source has been written +before it is read. Theorem 1 applies. Distinct destinations make `S` +independent of the event permutation. ∎ + +## Smallest examples and scope boundaries + +For `a,b,c` initially arbitrary, the word + +```text +b ^= a; c ^= b +``` + +returns `c XOR b XOR a` in the last cell; the snapshot contract requires +`c XOR b`. Reversing those two events implements the snapshot exactly. +The two-cycle `a ^= b; b ^= a` has no safe reordering. + +Repeated destinations are outside both theorems. In three cells the word +`(b ^= a; c ^= b)` repeated four times is the identity, as is its snapshot +sum. It has chronological conflicts whose discrepancies later cancel. +The verifier checks this boundary and the public guard rejects such a word. +Self-XOR is also rejected. Its erasure semantics is outside the invertible +update contract. + +The algorithms in [batching.py](batching.py) are: + +- `first_conflict`: validate the contract and scan once, returning the two + event indices, entry basis cell and final discrepancy cell, or `None`. +- `safe_order`: remove sinks with a heap and emit their incoming events; + return a permutation or `None` for a directed cycle. +- `execute`: literal serial or snapshot execution on dirty bit strings. + +The guard uses `O(|V|+m)` storage and time bounded by the input validation +and scan. The ordering routine uses `O(|V|+m)` storage and +`O(|V|+m log(|V|+1))` time. The implementation admits at most 4,096 cells, +at most one event per cell, and payload entries of at most 256 bits. +The written theorems cover every finite cell set and every such `W`. + +## Evidence and reproduction + +The standard-library verifier enumerates every ordered admitted word on one +through five cells and directly constructs both full Boolean operators. +It uses a separate transitive-closure oracle for cycles, then checks the +returned ordering against the full operators. It executes every unsafe +basis witness on literal bits, rather than accepting only a conflict flag. + +Observed exhaustive totals are 160,579 words, 4,833 safe orders and 155,746 +unsafe orders with 155,746 executed witnesses. Of these words, 141,736 +have a directed cycle. Each word is counted with its order; these are not +counts of unlabelled graphs. The replay also checks 512 dirty two-bit +payload executions, 16 invalid-input rejections and six boundary controls. +The latter include a 4,096-cell chain and cycle, the largest payload bit, +and the repeated-write cancellation example. The all-size result rests on +the written proof, not extrapolation from these counts. + +From the repository root: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/unique-write-xor-batching/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/unique-write-xor-batching/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/unique-write-xor-batching +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/unique-write-xor-batching --check-source-history +``` + +Use the host's CPython 3.12 path elsewhere. The first two commands print +`PASS_UNIQUE_WRITE_XOR_BATCHING`, the complete derived totals and SHA256 +of every regular package file. They write no files and work without Git. +No receipt is handwritten or used as a substitute for recomputation. +Registered replay runs both modes with 120-second command limits. + +## Connection to the current bottleneck and predecessor credit + +The selected `owned_erasure` and `compiler` assumptions require legal +chronological physical operations. Jose Manuel's +[PR2195](https://github.com/CrocSwap/integer-mult-bounds/pull/2195), +`selected-bit-local-ring-sweeps`, distinguishes pointwise owner injection +from separation of complete high packets and supplies an alias countermodel. +Adam Gall's [PR2088](https://github.com/CrocSwap/integer-mult-bounds/pull/2088) +constructs physical private snapshots with separately charged storage and +transports. Their results, counts and native guards are cited premises or +motivation and are not audited or replayed here. + +This package supplies a different, conditional admission test: **after** a +caller has emitted its actual cells and proved global destination uniqueness, +the guard decides whether its serial reads may be replaced by entry reads. +Disjoint read and write sets suffice, but are unnecessary. For example, +`c ^= b; b ^= a` is safe despite overlap. A directed cycle obstructs every +in-place ordering in this class before routing costs are considered. + +This does not prove uniqueness, packet separation, selected source provenance, +COPY/ERASE restoration, paid routing, recursive workspace or child closure for +any actual GL64 sweep. It changes no selected source, supplier or frontier. +No complete multiplication theorem, selected assumption discharge or native +cost saving is claimed. The exact scopes of #2195 and #2088 remain theirs. +Credit their alephnan, eumemic, DreamingOfClouds, source/compiler/owner and +retained native lineage without transferring those results to this package. + +Scientific base is canonical main +`a5bff3bf133e482541c09eba4e773884bdb2b1b7`, priority revision 8. The selected +κ there is `781451/250000000`. [TASK.json](TASK.json) retains the original +`uniform-transfer-audit` card and marks this reusable side result as changed +scope. [SOURCES.json](SOURCES.json) pins the catalogue, selected record and +the two contextual predecessor texts as historical provenance. The new proof +is self-contained and imports no predecessor executable. + +Live overlap covered 310 open PR bodies and 5,906 Discussion records with +complete remote pagination. Sparse local search covered 91 of 8,623 tracked +notes, so omitted notes were not treated as searched. Separate main-wide +README and merged-PR searches checked the distinctive unique-write, dirty +XOR, snapshot and read-before-write terms. This is bounded overlap evidence, +not proof of novelty or scientific acceptance. + +## Implementation limits + +No recursion, generated code, dynamic evaluation or asynchronous work is +used. The fixed package-local import makes isolated `-I` execution explicit. +All public contracts use exceptions that remain active under `-O`; the +verifier's mathematical invariants use explicit checks. Every enumeration +has fixed finite bounds. Functions are below 60 physical lines. + +Python allocates collections during execution, a Power of Ten rule-3 +deviation. Public words have at most 4,096 events, public values at most +256 bits each, and each exhaustive oracle case has at most five cells. +Cases are processed one at a time. No allocation-free or hard real-time +claim is made. Warning-strict normal and optimized runs are the available +diagnostics; no third-party static analyzer or Lean build is required. +Independent human and formal proof-kernel review are unclaimed. + +## Open next questions + +1. Emit one named physical packet sweep, prove its global destination + uniqueness and apply the guard. This could settle one actual batching + decision. Begin with its exact physical coordinate encoding; that emitter + and a complete routing invoice are missing here. +2. Classify a bounded repeated-write family. This could admit schedules + excluded by this contract. Begin with full operators and the eight-event + cancellation example; the first-conflict proof no longer freezes its + output when later writes are permitted. + +The structured questions are in [TASK.json](TASK.json). Research stops at +this first verified criterion. diff --git a/research/unique-write-xor-batching/SOURCES.json b/research/unique-write-xor-batching/SOURCES.json new file mode 100644 index 0000000000..1f6ec15cd0 --- /dev/null +++ b/research/unique-write-xor-batching/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "a5bff3bf133e482541c09eba4e773884bdb2b1b7", + "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/selected-bit-local-ring-sweeps/PROOF.md", + "usage": "provenance", + "git_blob": "4330de85dd9862ed15d84ab917887d249753df99", + "sha256": "846c59440cc99e28bae93ad2af99525bc769de29368080071b8427141215b4f7" + }, + { + "path": "research/bit-two-copy-physical/README.md", + "usage": "provenance", + "git_blob": "dd6271806fe3b5f15c03a733cd1e91908d63df13", + "sha256": "8fb8fe7a164f86beecaf4e8524e06389988f4bcc5ebeccc3efcd2a10a2c89480" + } + ] +} diff --git a/research/unique-write-xor-batching/TASK.json b/research/unique-write-xor-batching/TASK.json new file mode 100644 index 0000000000..0243a829cb --- /dev/null +++ b/research/unique-write-xor-batching/TASK.json @@ -0,0 +1,89 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 8, + "base_commit": "a5bff3bf133e482541c09eba4e773884bdb2b1b7", + "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 exact snapshot-equivalence criterion, constructive failure witness and safe-ordering theorem for arbitrary finite dirty Boolean XOR sweeps whose destinations are distinct.", + "scope_change_reason": "The suggested card concerns a complete selected caller assumption. This original side result isolates a finite-coordinate safety condition relevant to owned_erasure and compiler batching; it does not discharge either selected assumption or recheck a predecessor.", + "bottleneck_link": "Owner injection alone does not justify replacing serial mutable reads by entry-snapshot reads. The result supplies a necessary and sufficient batching guard under a precise unique-destination contract, before any physical routing or child-volume claim.", + "budget_minutes": 60, + "stop_rule": "Ship the first verified batching criterion and its witness-producing guard; do not expand into repeated-write words, new owner charts or supplier admission.", + "outcome": "completed", + "evidence": "Written first-conflict proof and reverse-topological construction. The executable independently compares full Boolean operators for all 160579 ordered admitted words on 1..5 cells: 4833 safe, 155746 unsafe, each unsafe case has a literal basis witness. Independent reachability checks safe-order existence, with 141736 cyclic words. It also runs 512 dirty multi-bit executions, 16 invalid-input rejections and six boundary controls including 4096-cell chain/cycle limits and repeated-write cancellation.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a named physical packet sweep be emitted with globally unique destinations, and does its serial order pass this guard?", + "why_it_matters": "This would connect the finite-coordinate theorem to a concrete owned-erasure or compiler batching decision.", + "first_step": "Freeze one packet enumerator and its physical coordinate encoding; prove global destination uniqueness before applying the guard.", + "blocked_by": "No physical selected GL64 coordinate enumerator or complete routing invoice is supplied here." + }, + { + "question": "What exact criterion replaces this one when destinations may repeat?", + "why_it_matters": "Later writes can cancel the first discrepancy, as the eight-event boundary control demonstrates.", + "first_step": "Classify one bounded repeated-write family using full operators rather than treating a local conflict as a proof of final inequality.", + "blocked_by": "The unique-write proof no longer freezes the witness output; a general dependency-only rule need not be necessary." + } + ] +} diff --git a/research/unique-write-xor-batching/VERIFY.json b/research/unique-write-xor-batching/VERIFY.json new file mode 100644 index 0000000000..e874bee821 --- /dev/null +++ b/research/unique-write-xor-batching/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact complete Boolean-operator census, unsafe basis witnesses, independent graph-cycle oracle, dirty payloads, invalid inputs and capacity/cancellation controls." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact complete Boolean-operator census, unsafe basis witnesses, independent graph-cycle oracle, dirty payloads, invalid inputs and capacity/cancellation controls." + } + ] +} diff --git a/research/unique-write-xor-batching/batching.py b/research/unique-write-xor-batching/batching.py new file mode 100644 index 0000000000..cf54abf545 --- /dev/null +++ b/research/unique-write-xor-batching/batching.py @@ -0,0 +1,98 @@ +"""Exact snapshot guard for XOR sweeps with distinct destinations. + +An event is (destination, source). Payload entries are arbitrary bit strings. +Copyright 2026 Nick Petalas. Apache-2.0. +""" + +from dataclasses import dataclass +from heapq import heappop, heappush + +MAX_CELLS = 4096 +MAX_PAYLOAD_BITS = 256 +Event = tuple[int, int] +Word = tuple[Event, ...] + + +@dataclass(frozen=True) +class Conflict: + first: int + second: int + basis: int + output: int + + +def checked_word(cells: int, events: object) -> Word: + """Validate the unique-write contract before applying the theorem.""" + if type(cells) is not int or not 1 <= cells <= MAX_CELLS: + raise ValueError("cell count must be an integer in 1..4096") + if not isinstance(events, (tuple, list)) or len(events) > cells: + raise ValueError("events must be a sequence with at most cells entries") + result = [] + destinations = set() + for event in events: + if not isinstance(event, (tuple, list)) or len(event) != 2: + raise ValueError("an event must contain destination and source") + target, source = event + if any(type(x) is not int or not 0 <= x < cells for x in event): + raise ValueError("event endpoints must be integer cell indices") + if target == source or target in destinations: + raise ValueError("self-updates and repeated destinations are excluded") + destinations.add(target) + result.append((target, source)) + return tuple(result) + + +def first_conflict(cells: int, events: object) -> Conflict | None: + """Return a basis-input discrepancy, or certify snapshot equality.""" + word = checked_word(cells, events) + written: dict[int, int] = {} + for second, (target, source) in enumerate(word): + if source in written: + first = written[source] + return Conflict(first, second, word[first][1], target) + written[target] = second + return None + + +def safe_order(cells: int, events: object) -> tuple[int, ...] | None: + """Return safe event indices, or None exactly for a directed cycle.""" + word = checked_word(cells, events) + incoming = {target: i for i, (target, _) in enumerate(word)} + outgoing = [0] * cells + for _, source in word: + outgoing[source] += 1 + ready = [] + for target in incoming: + if outgoing[target] == 0: + heappush(ready, target) + order = [] + for _ in range(len(word)): + if not ready: + return None + target = heappop(ready) + index = incoming[target] + order.append(index) + source = word[index][1] + outgoing[source] -= 1 + if outgoing[source] == 0 and source in incoming: + heappush(ready, source) + return tuple(order) + + +def checked_payload(cells: int, values: object) -> tuple[int, ...]: + if not isinstance(values, (tuple, list)) or len(values) != cells: + raise ValueError("payload must have one entry per cell") + if any(type(x) is not int or not 0 <= x < 1 << MAX_PAYLOAD_BITS for x in values): + raise ValueError("payload entries must be unsigned bit strings of at most 256 bits") + return tuple(values) + + +def execute(cells: int, events: object, values: object, *, snapshot: bool) -> tuple[int, ...]: + word = checked_word(cells, events) + entry = checked_payload(cells, values) + if type(snapshot) is not bool: + raise ValueError("snapshot must be a Boolean") + current = list(entry) + for target, source in word: + current[target] ^= entry[source] if snapshot else current[source] + return tuple(current) diff --git a/research/unique-write-xor-batching/verify.py b/research/unique-write-xor-batching/verify.py new file mode 100644 index 0000000000..04c7860c86 --- /dev/null +++ b/research/unique-write-xor-batching/verify.py @@ -0,0 +1,171 @@ +#!/usr/bin/env python3 +"""Bounded exact corroboration of the written unique-write batching proof. + +No predecessor executable is imported. No output files are written. +Copyright 2026 Nick Petalas. Apache-2.0. +""" + +import hashlib +import itertools +import json +from pathlib import Path +import sys + +PACKAGE = Path(__file__).resolve().parent +sys.path.insert(0, str(PACKAGE)) +from batching import ( + MAX_CELLS, checked_word, execute, first_conflict, safe_order, +) + + +def require(condition: bool, description: str) -> None: + if not condition: + raise ValueError(description) + + +def operators(cells: int, word: tuple) -> tuple[tuple[int, ...], tuple[int, ...]]: + """Independent formal-column replay; row bits encode arbitrary input data.""" + entry = tuple(1 << i for i in range(cells)) + serial = list(entry) + snapshot = list(entry) + for target, source in word: + serial[target] = serial[target] ^ serial[source] + snapshot[target] = snapshot[target] ^ entry[source] + return tuple(serial), tuple(snapshot) + + +def has_cycle(cells: int, word: tuple) -> bool: + """Independent Boolean reachability closure, without using the planner.""" + rows = [0] * cells + for target, source in word: + rows[source] |= 1 << target + for middle in range(cells): + for source in range(cells): + if rows[source] >> middle & 1: + rows[source] |= rows[middle] + return any(row >> i & 1 for i, row in enumerate(rows)) + + +def check_word(cells: int, word: tuple, totals: dict) -> None: + serial, snapshot = operators(cells, word) + conflict = first_conflict(cells, word) + require((conflict is None) == (serial == snapshot), "snapshot criterion") + totals["words"] += 1 + totals["safe" if conflict is None else "unsafe"] += 1 + if conflict is not None: + require(word[conflict.first][0] == word[conflict.second][1], "conflict edge") + require(conflict.first < conflict.second, "chronological conflict") + require((serial[conflict.output] ^ snapshot[conflict.output]) >> conflict.basis & 1, + "formal basis discrepancy") + witness = tuple(int(i == conflict.basis) for i in range(cells)) + left = execute(cells, word, witness, snapshot=False) + right = execute(cells, word, witness, snapshot=True) + require(left[conflict.output] != right[conflict.output], "literal witness") + totals["literal_witnesses"] += 1 + order = safe_order(cells, word) + cycle = has_cycle(cells, word) + require((order is None) == cycle, "safe ordering iff acyclic") + if order is not None: + require(sorted(order) == list(range(len(word))), "event permutation") + changed = tuple(word[i] for i in order) + require(first_conflict(cells, changed) is None, "planner contract") + left, right = operators(cells, changed) + require(left == right == snapshot, "planner preserves snapshot endpoint") + else: + totals["cyclic_words"] += 1 + + +def exhaustive(totals: dict) -> None: + """All ordered unique-destination words on 1..5 cells.""" + for cells in range(1, 6): + for length in range(cells + 1): + for targets in itertools.permutations(range(cells), length): + choices = tuple(tuple(s for s in range(cells) if s != t) for t in targets) + for sources in itertools.product(*choices): + word = tuple(zip(targets, sources)) + check_word(cells, word, totals) + + +def payload_fixtures() -> int: + count = 0 + words = (((1, 0), (2, 1)), ((2, 1), (1, 0)), ((0, 1), (1, 0)), ()) + for word in words: + for values in itertools.product(range(4), repeat=3): + rows, snap = operators(3, word) + for snapshot, matrix in ((False, rows), (True, snap)): + expected = [] + for row in matrix: + value = 0 + for column in range(3): + if row >> column & 1: + value ^= values[column] + expected.append(value) + require(execute(3, word, values, snapshot=snapshot) == tuple(expected), + "dirty multi-bit execution") + count += 1 + return count + + +def rejection_controls() -> int: + cases = ((True, ()), (0, ()), (MAX_CELLS + 1, ()), (2, None), + (2, ((0,),)), (2, ((0, 2),)), (2, ((0, True),)), + (2, ((0, 0),)), (2, ((0, 1), (0, 1))), (2, ((-1, 1),))) + for cells, word in cases: + try: + checked_word(cells, word) + except ValueError: + continue + raise ValueError("invalid word accepted") + invalid = ((0,), (0, -1), (0, True), (0, 1 << 256), None) + for values in invalid: + try: + execute(2, ((1, 0),), values, snapshot=False) + except ValueError: + continue + raise ValueError("invalid payload accepted") + try: + execute(2, (), (0, 0), snapshot=1) + except ValueError: + return len(cases) + len(invalid) + 1 + raise ValueError("non-Boolean execution mode accepted") + + +def boundary_controls() -> dict: + chain = tuple((i, i - 1) for i in range(1, MAX_CELLS)) + conflict = first_conflict(MAX_CELLS, chain) + require(conflict is not None and conflict.second == 1, "long-chain witness") + order = safe_order(MAX_CELLS, chain) + require(order == tuple(reversed(range(len(chain)))), "long-chain schedule") + reversed_chain = tuple(chain[i] for i in order) + require(first_conflict(MAX_CELLS, reversed_chain) is None, "long-chain safety") + cycle = chain + ((0, MAX_CELLS - 1),) + require(safe_order(MAX_CELLS, cycle) is None, "long-cycle obstruction") + require(execute(2, ((1, 0),), (1 << 255, 7), snapshot=False) + == (1 << 255, (1 << 255) ^ 7), "max payload bit") + # Without unique destinations, the first discrepancy can cancel later. + repeated = ((1, 0), (2, 1)) * 4 + serial, snapshot = operators(3, repeated) + require(serial == snapshot == (1, 2, 4), "repeated-write cancellation boundary") + return {"long_chain_cells": MAX_CELLS, "long_cycle_cells": MAX_CELLS, + "repeated_write_cancellation_events": len(repeated), "controls": 6} + + +def file_hashes() -> dict: + paths = sorted(p for p in PACKAGE.iterdir() if p.is_file()) + require(len(paths) <= 16, "bounded package inventory") + return {p.name: hashlib.sha256(p.read_bytes()).hexdigest() for p in paths} + + +def main() -> None: + totals = {"words": 0, "safe": 0, "unsafe": 0, + "literal_witnesses": 0, "cyclic_words": 0} + exhaustive(totals) + result = {"status": "PASS_UNIQUE_WRITE_XOR_BATCHING", "claim_type": "scoped proof", + "exact_operator_census": totals, "dirty_payload_executions": payload_fixtures(), + "invalid_input_rejections": rejection_controls(), "boundaries": boundary_controls(), + "package_sha256": file_hashes()} + print(json.dumps(result, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()