From 5a41fea466cbeb7839bde864e563e191de47a0f7 Mon Sep 17 00:00:00 2001 From: ToikY <27568617+ToikY@users.noreply.github.com> Date: Tue, 20 Oct 2026 08:11:24 -0700 Subject: [PATCH 1/2] Retain minimal unchanged PR4201 guard-scan sources and attribution --- .../SOURCE-PINS.json | 38 +++ .../source/PREDECESSOR-PROOF.md.txt | 181 ++++++++++++++ .../source/PREDECESSOR-README.md.txt | 70 ++++++ .../source/predecessor_adapter.py | 226 ++++++++++++++++++ .../source/predecessor_machine.py | 169 +++++++++++++ 5 files changed, 684 insertions(+) create mode 100644 research/crt-unary-stencil-producer/SOURCE-PINS.json create mode 100644 research/crt-unary-stencil-producer/source/PREDECESSOR-PROOF.md.txt create mode 100644 research/crt-unary-stencil-producer/source/PREDECESSOR-README.md.txt create mode 100644 research/crt-unary-stencil-producer/source/predecessor_adapter.py create mode 100644 research/crt-unary-stencil-producer/source/predecessor_machine.py diff --git a/research/crt-unary-stencil-producer/SOURCE-PINS.json b/research/crt-unary-stencil-producer/SOURCE-PINS.json new file mode 100644 index 0000000000..22613fdd6e --- /dev/null +++ b/research/crt-unary-stencil-producer/SOURCE-PINS.json @@ -0,0 +1,38 @@ +[ + { + "origin_pr": 4201, + "origin_commit": "4f49743a9df0cf7501cdc62bd5707a122fa071e9", + "origin_path": "research/crt-dense-guard-scan/machine.py", + "path": "research/crt-unary-stencil-producer/source/predecessor_machine.py", + "size": 5545, + "sha256": "1cb27312932914eb631078bd56e85feb1dc6c4191e9d1962b2cc3a7e1cfb8df7", + "git_blob": "ce763898bd7b4401bbab818c640a0593b65c9a82" + }, + { + "origin_pr": 4201, + "origin_commit": "4f49743a9df0cf7501cdc62bd5707a122fa071e9", + "origin_path": "research/crt-dense-guard-scan/verify.py", + "path": "research/crt-unary-stencil-producer/source/predecessor_adapter.py", + "size": 11970, + "sha256": "40794cd2e2936f0f5e42fac1bb51b65c951a2ab56b7e88824e8c2d09a3dbf40e", + "git_blob": "2f221b5678bbb80c3c694c843b2eb84c5f5e9ee4" + }, + { + "origin_pr": 4201, + "origin_commit": "4f49743a9df0cf7501cdc62bd5707a122fa071e9", + "origin_path": "research/crt-dense-guard-scan/PROOF.md", + "path": "research/crt-unary-stencil-producer/source/PREDECESSOR-PROOF.md.txt", + "size": 10476, + "sha256": "c075a3c261bb824884f0da9f99fed227b15f9fac087bbdeb2c2cb861d4091f11", + "git_blob": "235d7405ffcf712ad3905c3077719554ade0790c" + }, + { + "origin_pr": 4201, + "origin_commit": "4f49743a9df0cf7501cdc62bd5707a122fa071e9", + "origin_path": "research/crt-dense-guard-scan/README.md", + "path": "research/crt-unary-stencil-producer/source/PREDECESSOR-README.md.txt", + "size": 3880, + "sha256": "912595166aded8591819c1f4fccdd7bfa44361906a1466057f838a656e85f329", + "git_blob": "fd0dd321baa1592999677f212ffa77cbb1bb513c" + } +] diff --git a/research/crt-unary-stencil-producer/source/PREDECESSOR-PROOF.md.txt b/research/crt-unary-stencil-producer/source/PREDECESSOR-PROOF.md.txt new file mode 100644 index 0000000000..235d7405ff --- /dev/null +++ b/research/crt-unary-stencil-producer/source/PREDECESSOR-PROOF.md.txt @@ -0,0 +1,181 @@ +# Literal dense guard-mask scan from an admitted stencil + +## Scope and interface + +The input is an **admitted** nonempty length-`L` stencil, `L>=1`, over the +fixed finite alphabet below. The output is the complete `M=2^L`-bit BAD mask, +in increasing numerical order of the MSB-first binary address. BAD is the +complement of the conjunction of the stencil's digit and guard tests. +Geometry parsing, interval ordering, threshold generation and admission are +outside this interface. `verify.py` supplies host adapters for those tasks; +their rejection tests do not certify a tape implementation of admission. + +There are three reusable physical tape roles: protected stencil, private +counter, and caller-owned mask. Each has a permanent left marker `<` in its +initial configuration and otherwise initially blank cells `_`. The supplied +stencil has its `L` atoms followed by `>`. All heads start at `<`. On success +the stencil is unchanged, the counter's data and allocated right marker are +blank again, and the mask has `M` output bits followed by `>`. +Every head returns to `<`. The permanent left infrastructure is retained. +The caller must consume/transfer and clear a previous owned mask before this +same output role is reused; the theorem does not allocate a new physical +tape for each invocation. Source/payload streams are not among these roles. + +An atom is `(kind,begin,end,lower_bit,upper_bit)`, with kind in `{S,D,G}`, +two Boolean boundary flags and two bits. The canonical S atom is +`(S,false,false,0,0)`. D atoms carry zero threshold bits. Non-S intervals +are ordered, disjoint and complete: exactly one begin and end, of the same +kind, with no intervening S atom. A one-cell interval may begin and end in +the same atom. G atoms contain equal-width MSB-first lower/upper strings. +There may be no intervals at all. This is a fixed product alphabet; an atom +does not contain an integer interval number or a parameter-sized descriptor. + +For each D interval, reject exactly its all-ones string. For each G interval +with strings `lo,hi`, accept exactly `lo<=value`, and +writes an equally long all-zero binary counter and its own `>`. Literal +rewinds read symbols until `<`, paying for the boundary test. For each +counter value the two tapes are scanned together from left to right. A D +begin resets `all_ones=true`; every cell conjoins its bit, and the D end +conjoins `not all_ones` into the overall predicate. A G begin resets both +comparison flags to E. The first unequal pair sets L or G and later pairs +leave that flag unchanged. Induction over an interval proves that this is +the lexicographic comparison of its complete MSB-first strings. At its end +the lower flag must be E or G and the upper flag must be L. Thus equality +with the lower bound is accepted and equality with the upper bound rejected. +Each interval's result is conjoined, and S bits are ignored. + +Write one BAD bit at the mask head and move that head one cell right. Rewind +the stencil. The counter head is at `>`: move left, replace trailing ones +by zero, replace the first zero by one, and rewind to `<`. If carrying reaches +`<`, return the overflow flag. Standard binary induction proves that the +successive scanned counters are exactly `0,1,...,M-1`, with no repetition or +omission, and that the last carry leaves all counter bits zero. This proves +both the output length and its ordering, without a host loop of `M` steps. + +Overflow is not erasure: zero is distinct from blank. A final literal pass +therefore writes blank on every counter data cell **and its right marker**, +then reads/moves back to `<`. Append `>` to the mask and rewind that head. +This restores the exact initial private infinite-tape configuration while +preserving both protected input and owned output. A final fixed control state +discards the transient finite flags. The program has no variable-depth +recursion, indexed geometry lookup or parameter-dependent tape inventory. + +## Exact action census and asymptotic tariff + +Count each read, write and one-cell move as one action. Finite-control +transitions compile into a constant factor more machine steps, independent +of all parameters. Let `M=2^L`. The following counts are for the normal +program on every admitted stencil; they do not depend on which tests pass. + +| Phase | Cell/head actions | +|---|---:| +| Initialization, including first mask move | `8L+11` | +| Predicate scan, BAD append, stencil rewind for all addresses | `(6L+8)M` | +| All counter increments, including final overflow and rewinds | `(2L+5)M-3` | +| Counter data/right-marker blank erasure and return | `5L+6` | +| Mask right marker and return | `2M+4` | + +For the carry line, the `M-1` successful increments each read `L+2` cells +and move `L+1` times, including the rewind. Final overflow reads and moves +`L+1` times. The number of carried one bits over the complete enumeration is +`M-1`; there are also `M-1` successful zero-to-one writes. Thus carry writes +are `2M-2`, and its total is `(2L+5)M-3`. This charges every marker read, +counter update and return; there is no free numerical head-zero test. + +The resulting exact totals are + +``` +reads = (4L+6)M + 5L + 9 +writes = 3M + 2L + 1 +moves = (4L+6)M + 6L + 8 +total = 8ML + 15M + 13L + 18. +``` + +Visited cells, including protected input, output and all markers, are exactly +`(L+2)+(L+2)+(M+2)=M+2L+6`. The finite alphabet has constant encoding size. +Consequently this is one uniform fixed-tape procedure with time `O(ML)` and +visited space `O(M+L)`, from the admitted-stencil interface. The stored +receipt checks the exact census, not a fitted timing bound. Emulator counters, +hashing, source comparisons and host admission are not machine registers or +included action evidence. + +For the source's `V=MR` caller, its stated `L=Theta(p)` and `R=Theta(p)` give +`O(ML)=O(V)`. The condition `R>=1` alone would not suffice. This conclusion +prices the detector from its supplied stencil, not a complete source caller. +Its uniform geometry/threshold producer and admission tariff remain an +explicit obligation before composing an end-to-end O(V) implementation. + +## Binding the source predicate, without a hidden parity test + +The three pinned current-main files are authenticated by SHA-256 and Git +blob hash before loading the source. `check_batched_crt.py:142-175` defines +the same predicate in `good` and `linear_guard`. For `B=2^G`, active digits +are the low `rG` bits of each H-bit u/t field, split into G-bit digits; each +must differ from `B-1`. For target arithmetic position j, the guard is + +``` +g = (y >> (j+1)) mod 2^(K-1), 2B <= g < 2^(K-1)-2B. +``` + +The parity bit at j is excluded. Under the explicit physical address order +`u_H | t_H | y_Y | w_W`, with each field MSB-first, digit i of either control +field occupies `[field_start+H-(i+1)G, field_start+H-iG)`. The guard occupies +`[2H+Y-j-K, 2H+Y-j-1)`, width `K-1`. Encode its two thresholds in that width. +All other cells, including inactive high control bits, target parity bits, +unused Y cells and the complete optional w field, are S. The host adapter +requires complete disjoint `[j,j+K)` target segments and `H>=rG`. +These formulas prove equality with the source for every padded address of +any admitted geometry, independently of the finite tests. + +The finite fixtures are predicate projections, not full production +three-reservoir invocations: `(G,H,Y,K,targets,W)` is `(1,2,10,5,[0,5],0)`, +`(2,3,9,7,[1],0)` and `(1,1,5,5,[0],1)`. They exhaust all 49,408 addresses, +including dirty compact digits, guard boundaries, parity and spectator bits. +The two source functions agree with every literal output bit. All-S stencils +at `L=1,2,3` separately cover the no-test and smallest-overflow boundaries. +Negative controls alter lower/upper strictness, MSB significance, unadjusted +whole-K thresholds, output return and the counter's least significant bit. +The whole-K mutant keeps the K-1-bit numeric thresholds unchanged; properly +rescaled full-segment thresholds can represent the same guard and are not +claimed wrong. Host malformed-input rejection controls are admission-adapter +evidence only. Optimized Python retains every verifier check via explicit +exceptions rather than `assert`. + +## Predecessors and remaining obligations + +Cinna Davis already proposes this counter/ordered-descriptor scan and its +three-state comparisons in current-main `CRT.md:238-253`. This package +contributes the literal finite-control lowering, complete ownership/cell +census and source-bound executed checks; it claims no new guard mechanism. +Hiroki KUMAZAKI (@kumagi), PR4169 head +`835c3563ee7ede8ceaf329ede7372e50f7823136`, gives the arbitrary-source repair +predicate/proof and leaves guard-scan/function/sort costs open. PR4174 head +`5fec853f0c048871de3b8098d1e30d4ee19cda23` gives reservoir placement and +ordered descriptors while leaving their fixed-tape tariff open. Their +mechanisms and other source ancestry retain credit; neither open PR is +imported here. Douglas Colkitt/OpenAI's stream and compact-control framework +and all retained source notices remain unchanged. This work has substantial +OpenAI Codex assistance, Apache-2.0; no new formal-kernel or independent human +review is claimed. + +Still outside certification: uniform geometry/stencil production/admission, +transported caller descriptors, extraction/reinsertion and sorting, E work on +exceptional keys, switch-table/arithmetic evaluation, payload routing, repair, +ordinary callees, numerical precision, native/outer composition and a new +kappa or multiplication theorem. No selected-frontier change follows. diff --git a/research/crt-unary-stencil-producer/source/PREDECESSOR-README.md.txt b/research/crt-unary-stencil-producer/source/PREDECESSOR-README.md.txt new file mode 100644 index 0000000000..fd0dd321ba --- /dev/null +++ b/research/crt-unary-stencil-producer/source/PREDECESSOR-README.md.txt @@ -0,0 +1,70 @@ +# Literal CRT dense guard-mask scan + +This package lowers the ordered scan already proposed in +[`CRT.md:238-253`](../unconditional-batched-crt/CRT.md) to a marker-driven +three-tape program. From an **admitted ordered stencil** of L fixed-alphabet +cells it writes the complete `M=2^L`-bit bad-address mask, preserves the +stencil, blanks all private work and returns every head. All padded address +bits are enumerated; inactive control bits, target parity and spectators +remain unconstrained when marked SKIP. + +The exact normal-program census is `8ML+15M+13L+18` cell/head actions and +`M+2L+6` visited cells, including input, output and markers. This gives +`O(ML)` time and `O(M+L)` space with three fixed tape roles and finite control. +Under the source's `L=Theta(p), R=Theta(p), V=MR`, the detector is `O(V)`. +Geometry-to-stencil production and admission remain explicit **unpriced** +dependencies. No complete caller or new kappa result is claimed. + +`machine.py` is the literal cell/head program. It neither reads a host +length/address/head coordinate nor calls a predicate/E callback. Its emulator +uses numerical coordinates and action totals solely as observers. The stencil +alphabet packs kind, interval boundaries and two threshold bits in one fixed +product alphabet. `PROOF.md` proves enumeration, MSB comparison, cleanup and +the exact census, and separates this supplied-stencil interface from the +unimplemented geometry producer. The permanent left sentinels belong to the +initial tape infrastructure; cleanup restores blank data and erases the +private right marker while retaining those sentinels. + +Run from the repository root with Python 3.12 and the pinned sources present: + +``` +python3 -I -B research/crt-dense-guard-scan/verify.py +python3 -I -O -W error -B research/crt-dense-guard-scan/verify.py +``` + +Both commands authenticate the three source files against `SOURCE-PINS.json` +and compare a fresh replay with `RESULT.json`; they do not rewrite it. +`--write-result` explicitly regenerates the receipt. The package uses only the +Python standard library and explicit checks that remain active under `-O`. + +Executed source binding exhausts 49,408 addresses in three predicate-projection +fixtures, rather than claiming a full production reservoir invocation: + +| G | H | Y | K | target positions | back SKIP bits | addresses | good | +|---:|---:|---:|---:|---|---:|---:|---:| +| 1 | 2 | 10 | 5 | 0,5 | 0 | 16,384 | 256 | +| 2 | 3 | 9 | 7 | 1 | 0 | 32,768 | 13,824 | +| 1 | 1 | 5 | 5 | 0 | 1 | 256 | 32 | + +Every output bit is compared with both retained `good` and `linear_guard`. +All-SKIP L=1..3 fixtures exercise the smallest complete counters. Mutations +detect wrong lower/upper strictness, wrong MSB significance, a whole-K guard +with unadjusted K-1-bit thresholds, omitted counter low bit and omitted owned +output return. Malformed geometry/stencil rejection tests belong to the +unpriced host admission adapter. Semantic/source comparisons, observer totals +and hashes are verification work, not hidden runtime registers or steps. + +Cinna Davis already supplied the predicate and ordered-scan proposal. +Hiroki KUMAZAKI (@kumagi), PR4169 and PR4174, supplied arbitrary-source repair +and reservoir/descriptor audits; those open PRs are credited, not imported. +Douglas Colkitt/OpenAI's stream and compact-control framework and the pinned +source NOTICE retain their ancestry. This contribution is the literal +lowering and quantitative audit, with substantial OpenAI Codex assistance, +Apache-2.0. No independent human or new formal-kernel review is claimed. + +## Open next questions + +The next obligation is a uniformly encoded, charged geometry/threshold +producer and admission path at the transported caller. Extraction, sorting, +repair, payload routing, full E evaluation, ordinary callees, precision, +native/outer composition and the selected frontier are outside this result. diff --git a/research/crt-unary-stencil-producer/source/predecessor_adapter.py b/research/crt-unary-stencil-producer/source/predecessor_adapter.py new file mode 100644 index 0000000000..2f221b5678 --- /dev/null +++ b/research/crt-unary-stencil-producer/source/predecessor_adapter.py @@ -0,0 +1,226 @@ +"""Source binding and observer audit of the literal dense guard-mask program. + +Geometry-to-stencil construction/admission and source-oracle computations below +are host adapters, explicitly OUTSIDE the transducer's machine tariff. +""" + +import argparse +import hashlib +import json +from pathlib import Path +import sys +import types + + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def load_bytes(name, data, path): + module = types.ModuleType(name) + module.__file__ = str(path) + sys.modules[name] = module + exec(compile(data, str(path), "exec"), module.__dict__) + return module + + +def admit_stencil(cells, machine): + """Host admission only, not a claimed tape implementation or charged step.""" + need(len(cells) >= 1, "nonempty stencil") + active = None + for atom in cells: + need(type(atom) is tuple and len(atom) == 5, "fixed product alphabet") + kind, begin, end, lo, hi = atom + need(kind in ("S", "D", "G") and type(begin) is bool and type(end) is bool + and lo in ("0", "1") and hi in ("0", "1"), "finite alphabet atom") + if kind == "S": + need(atom == machine.SKIP and active is None, "skip outside intervals") + continue + if begin: + need(active is None, "nonoverlapping ordered interval start") + active = kind + else: + need(active == kind, "interval continuation") + if kind == "D": + need(lo == hi == "0", "digit has no threshold data") + if end: + active = None + need(active is None, "complete intervals") + return cells + + +def geometry_stencil(g, h, ybits, targets, k, back_bits, machine, include_parity=False): + """Unpriced source-binding adapter; preserves all unspecified bits as SKIP.""" + targets = tuple(targets) + need(all(type(v) is int for v in (g, h, ybits, k, back_bits)), "integer geometry") + need(g >= 1 and targets and h >= len(targets) * g and k >= g + 4 and back_bits >= 0, + "admissible compact/guard widths") + need(all(type(j) is int and 0 <= j and j + k <= ybits for j in targets), "complete target intervals") + intervals = sorted((j, j + k) for j in targets) + need(all(a[1] <= b[0] for a, b in zip(intervals, intervals[1:])), "disjoint target intervals") + length = 2 * h + ybits + back_bits + cells = [machine.SKIP] * length + + def place(lo, hi, kind, low=0, high=0): + width = hi - lo + low_bits = format(low, "0%db" % width) + high_bits = format(high, "0%db" % width) + need(width >= 1 and len(low_bits) == len(high_bits) == width, "fixed threshold widths") + for offset, position in enumerate(range(lo, hi)): + need(cells[position] == machine.SKIP, "no overlapping stencil cells") + cells[position] = (kind, offset == 0, offset == width - 1, + low_bits[offset], high_bits[offset]) + + for field_start in (0, h): + for digit in range(len(targets)): + place(field_start + h - (digit + 1) * g, field_start + h - digit * g, "D") + for j in targets: + # The source compares K-1 HIGHER guard bits, excluding parity bit j. + start = 2 * h + ybits - j - k + stop = 2 * h + ybits - j - (0 if include_parity else 1) + place(start, stop, "G", 1 << (g + 1), (1 << (k - 1)) - (1 << (g + 1))) + return admit_stencil(cells, machine) + + +def audit(cells, machine, **mutant): + """Observer integers are not read by the literal transducer.""" + admit_stencil(cells, machine) + stencil = machine.Tape([machine.LEFT] + cells + [machine.END]) + original = list(stencil.cells) + counter, mask = machine.transduce(stencil, **mutant) + length, records = len(cells), 1 << len(cells) + need(stencil.cells == original, "protected stencil unchanged") + need(counter.head == stencil.head == 0, "private/input heads returned") + need(counter.cells[0] == machine.LEFT and all(c == machine.BLANK for c in counter.cells[1:]), + "private counter restored to blank data, including right marker") + need(mask.cells[0] == machine.LEFT and mask.cells[-1] == machine.END, + "owned output markers") + bits = "".join(mask.cells[1:-1]) + need(len(bits) == records and all(bit in "01" for bit in bits), "one BAD bit per complete address") + actions = sum(t.actions for t in (stencil, counter, mask)) + if not mutant: + need(mask.head == 0, "owned output head returned") + need(actions == 8 * records * length + 15 * records + 13 * length + 18, + "derived exact marker/counter/cleanup action census") + need(sum(len(t.cells) for t in (stencil, counter, mask)) == records + 2 * length + 6, + "derived exact three-role visited space") + return bits, {"address_bits": length, "addresses": records, + "good_addresses": bits.count("0"), "bad_addresses": bits.count("1"), + "read_actions": sum(t.reads for t in (stencil, counter, mask)), + "write_actions": sum(t.writes for t in (stencil, counter, mask)), + "move_actions": sum(t.moves for t in (stencil, counter, mask)), + "total_cell_head_actions": actions, + "visited_cells_including_owned_mask": sum(len(t.cells) for t in (stencil, counter, mask)), + "heads_returned": mask.head == counter.head == stencil.head == 0, + "private_data_blank": True, + "mask_semantics": "1=bad, 0=good; increasing MSB-first binary address", + "mask_ascii_sha256": hashlib.sha256(bits.encode()).hexdigest()} + + +def fixture(name, g, h, ybits, targets, k, back_bits, source, machine): + cells = geometry_stencil(g, h, ybits, targets, k, back_bits, machine) + mask, receipt = audit(cells, machine) + for address, bit in enumerate(mask): + y = (address >> back_bits) & ((1 << ybits) - 1) + t = (address >> (ybits + back_bits)) & ((1 << h) - 1) + u = address >> (h + ybits + back_bits) + expected = source.good(u, t, y, bits=g, positions=targets, guard=k) + linear = source.linear_guard(u, t, y, bits=g, positions=targets, guard=k, + control_bits=h, ybits=ybits) + need(expected == linear == (bit == "0"), "literal mask equals exact source predicates on every address") + receipt.update({"name": name, "G": g, "H": h, "Y_bits": ybits, + "targets": list(targets), "K": k, "back_skip_bits": back_bits, + "domain": "predicate projection/stencil fixture, not a full production reservoir invocation"}) + return receipt, cells, mask + + +def must_reject(call, label): + try: + call() + except ValueError: + return label + raise ValueError("admission control accepted: " + label) + + +def controls(machine): + cells = geometry_stencil(1, 1, 5, (0,), 5, 0, machine) + right, _ = audit(cells, machine) + mutants = [] + for name, kwargs in (("lower threshold incorrectly strict", {"lower_strict": True}), + ("upper threshold incorrectly inclusive", {"upper_inclusive": True}), + ("last differing bit overrides MSB significance", {"last_difference_wins": True})): + wrong, _ = audit(cells, machine, **kwargs) + different = next((i for i, (a, b) in enumerate(zip(right, wrong)) if a != b), None) + need(different is not None, "semantic mutant differs: " + name) + mutants.append({"name": name, "address": different, + "correct_bad_bit": right[different], "wrong_bad_bit": wrong[different]}) + wrong_cells = geometry_stencil(1, 1, 5, (0,), 5, 0, machine, include_parity=True) + wrong, _ = audit(wrong_cells, machine) + different = next(i for i, (a, b) in enumerate(zip(right, wrong)) if a != b) + mutants.append({"name": "whole K-bit segment compared to unadjusted K-1-bit thresholds", + "address": different, "correct_bad_bit": right[different], "wrong_bad_bit": wrong[different]}) + _, missing_return = audit(cells, machine, omit_output_return=True) + need(not missing_return["heads_returned"], "missing owned-mask return detected") + return {"semantic_mutants": mutants, "ownership_mutants": ["owned mask head return omitted"], + "counter_mutants": [must_reject(lambda: audit(cells, machine, skip_low_counter_bit=True), + "least significant counter bit omitted")], + "unpriced_adapter_rejections": [ + must_reject(lambda: admit_stencil([], machine), "empty stencil"), + must_reject(lambda: admit_stencil([("D", False, True, "0", "0")], machine), "missing interval start"), + must_reject(lambda: admit_stencil([("G", True, False, "0", "1")], machine), "missing interval end"), + must_reject(lambda: geometry_stencil(1, 2, 10, (0, 4), 5, 0, machine), "overlapping source guards"), + must_reject(lambda: geometry_stencil(1, 1, 4, (0,), 5, 0, machine), "incomplete source guard"), + ]} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write-result", action="store_true") + args = parser.parse_args() + pins = json.loads((PACKAGE / "SOURCE-PINS.json").read_text()) + authenticated = {} + for row in pins: + data = (ROOT / row["path"]).read_bytes() + need(hashlib.sha256(data).hexdigest() == row["sha256"], "source SHA256: " + row["path"]) + need(hashlib.sha1(f"blob {len(data)}\0".encode() + data).hexdigest() == row["git_blob"], + "source Git blob: " + row["path"]) + authenticated[row["path"]] = data + path = "research/unconditional-batched-crt/check_batched_crt.py" + source = load_bytes("_guard_source", authenticated[path], ROOT / path) + machine = load_bytes("_literal_guard_machine", (PACKAGE / "machine.py").read_bytes(), PACKAGE / "machine.py") + rows = [] + for name, g, h, y, targets, k, w in ( + ("two_target_complete", 1, 2, 10, (0, 5), 5, 0), + ("inactive_digits_and_Y_spectators", 2, 3, 9, (1,), 7, 0), + ("one_target_with_back_spectator", 1, 1, 5, (0,), 5, 1)): + receipt, _, _ = fixture(name, g, h, y, targets, k, w, source, machine) + rows.append(receipt) + all_skip = [] + for length in (1, 2, 3): + mask, receipt = audit([machine.SKIP] * length, machine) + need(set(mask) == {"0"}, "all-skip stencil accepts every address") + all_skip.append(receipt) + result = {"schema_version": 1, "result": "PASS_LITERAL_DENSE_GUARD_MASK", + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", "source_inputs_checked": len(authenticated), + "fixtures": rows, "all_skip_boundaries": all_skip, "negative_controls": controls(machine), + "limitations": ["Literal transducer starts from admitted ordered finite-alphabet stencil.", + "Geometry/stencil generation and admission are unpriced host adapters, not discharged tape obligations.", + "Observer integers, hashes and source comparisons are outside runtime finite control.", + "No source/E callback exists in the detector interface; keyed work is outside it.", + "No extraction/sort/repair/payload movement, full CRT evaluator or new kappa."]} + output = PACKAGE / "RESULT.json" + if args.write_result: + output.write_text(json.dumps(result, indent=2) + "\n") + else: + need(json.loads(output.read_text()) == result, "stored receipt differs from replay") + print(json.dumps({"result": result["result"], "source_addresses": sum(r["addresses"] for r in rows), + "tape_actions": sum(r["total_cell_head_actions"] for r in rows)}, sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/crt-unary-stencil-producer/source/predecessor_machine.py b/research/crt-unary-stencil-producer/source/predecessor_machine.py new file mode 100644 index 0000000000..ce763898bd --- /dev/null +++ b/research/crt-unary-stencil-producer/source/predecessor_machine.py @@ -0,0 +1,169 @@ +"""Three fixed tape roles and a marker-driven, finite-control guard program. + +Tape.head and read/write/move totals are SIMULATOR OBSERVERS. The program +below never reads them, a tape length, or a host L/M/position counter. +Stencil atoms form a fixed finite product alphabet, independent of geometry. +""" + +LEFT, END, BLANK = "<", ">", "_" +SKIP = ("S", False, False, "0", "0") + + +class Tape: + """One cell/head operation per method; permanently marked left boundary.""" + + def __init__(self, cells=None): + self.cells = [LEFT] if cells is None else list(cells) + self.head = 0 + self.reads = self.writes = self.moves = 0 + + def read(self): + self.reads += 1 + return self.cells[self.head] + + def write(self, symbol): + self.writes += 1 + self.cells[self.head] = symbol + + def move(self, direction): + # Only the emulator uses a numerical head coordinate. The program + # emits one LEFT/RIGHT action and branches only on the read symbol. + if direction not in (-1, 1): + raise ValueError("one-cell direction") + self.moves += 1 + self.head += direction + if self.head < 0: + raise ValueError("crossing permanent left boundary") + if self.head == len(self.cells): + self.cells.append(BLANK) # Initially blank infinite tape cell. + + @property + def actions(self): + return self.reads + self.writes + self.moves + + +def rewind(tape): + while tape.read() != LEFT: + tape.move(-1) + + +def compare_flag(flag, bit, threshold, last_difference_wins): + """L/E/G are three finite control states; all arguments have finite range.""" + if bit == threshold: + return flag + if flag == "E" or last_difference_wins: + return "L" if bit == "0" else "G" + return flag + + +def predicate(stencil, counter, lower_strict, upper_inclusive, last_difference_wins): + good = True + all_ones = False + lower = upper = "E" + active = "S" + stencil.move(1) + counter.move(1) + while True: + token = stencil.read() + if token == END: + if active != "S": + raise ValueError("unterminated admitted interval") + return good + bit = counter.read() + if bit not in ("0", "1"): + raise ValueError("counter/stencil alignment") + # Tuple fields decode one atom of a FIXED finite alphabet. They do + # not index a parameter-sized geometry table or interval collection. + kind, begin, end, lower_bit, upper_bit = token + if kind == "D": + if begin: + active = "D" + all_ones = True + all_ones = all_ones and bit == "1" + if end: + good = good and not all_ones + active = "S" + all_ones = False + elif kind == "G": + if begin: + active = "G" + lower = upper = "E" + lower = compare_flag(lower, bit, lower_bit, last_difference_wins) + upper = compare_flag(upper, bit, upper_bit, last_difference_wins) + if end: + lower_ok = lower == "G" if lower_strict else lower != "L" + upper_ok = upper != "G" if upper_inclusive else upper == "L" + good = good and lower_ok and upper_ok + lower = upper = "E" + active = "S" + stencil.move(1) + counter.move(1) + + +def increment_and_return(counter, skip_low_counter_bit): + """Counter starts at END; overflow returns False at permanent LEFT.""" + counter.move(-1) + if skip_low_counter_bit: + counter.move(-1) + while True: + bit = counter.read() + if bit == "1": + counter.write("0") + counter.move(-1) + elif bit == "0": + counter.write("1") + rewind(counter) + return True + elif bit == LEFT: + return False + else: + raise ValueError("binary carry alphabet") + + +def erase_counter(counter): + """Restore private data to BLANK, including its allocated END marker.""" + counter.move(1) + while True: + symbol = counter.read() + counter.write(BLANK) + if symbol == END: + break + counter.move(1) + rewind(counter) + + +def transduce(stencil, lower_strict=False, upper_inclusive=False, + last_difference_wins=False, omit_output_return=False, + skip_low_counter_bit=False): + """Admitted stencil -> protected stencil, blank private work, owned BAD mask. + + The booleans select fixed mutation programs for verification. The normal + transducer has all False. There is no function/E-evaluator callback. + """ + counter, mask = Tape(), Tape() # Two fixed roles, reused throughout. + stencil.move(1) + counter.move(1) + while True: + symbol = stencil.read() + if symbol == END: + counter.write(END) + break + counter.write("0") + stencil.move(1) + counter.move(1) + rewind(stencil) + rewind(counter) + mask.move(1) + while True: + good = predicate(stencil, counter, lower_strict, upper_inclusive, last_difference_wins) + mask.write("0" if good else "1") + mask.move(1) + rewind(stencil) + if not increment_and_return(counter, skip_low_counter_bit): + break + erase_counter(counter) + mask.write(END) + if not omit_output_return: + rewind(mask) + # A fixed final control state replaces all transient finite flags. + return counter, mask From fb1f3c84535f3e5138bd07e7ed2f211f08fc296d Mon Sep 17 00:00:00 2001 From: ToikY <27568617+ToikY@users.noreply.github.com> Date: Tue, 20 Oct 2026 08:22:04 -0700 Subject: [PATCH 2/2] Add paid unary one-target CRT stencil producer and independent audits --- .../COST-RESULT.json | 270 ++ .../CROSS-REPLAY.json | 1110 ++++++ .../ORACLE-NOTES.txt | 37 + .../ORACLE-PROVENANCE.json | 23 + .../ORACLE-RESULT.json | 1278 +++++++ .../PRIMARY-REVIEW.json | 198 ++ .../PRIMARY-REVIEW.md | 24 + research/crt-unary-stencil-producer/PROOF.md | 285 ++ research/crt-unary-stencil-producer/README.md | 97 + .../crt-unary-stencil-producer/RESULT.json | 3113 +++++++++++++++++ .../crt-unary-stencil-producer/SOURCES.json | 64 + research/crt-unary-stencil-producer/TASK.json | 100 + .../crt-unary-stencil-producer/VERIFY.json | 109 + .../crt-unary-stencil-producer/cost_check.py | 138 + .../crt-unary-stencil-producer/cross_check.py | 148 + .../independent_oracle.py | 223 ++ .../primary_verify.py | 247 ++ .../crt-unary-stencil-producer/producer.py | 223 ++ 18 files changed, 7687 insertions(+) create mode 100644 research/crt-unary-stencil-producer/COST-RESULT.json create mode 100644 research/crt-unary-stencil-producer/CROSS-REPLAY.json create mode 100644 research/crt-unary-stencil-producer/ORACLE-NOTES.txt create mode 100644 research/crt-unary-stencil-producer/ORACLE-PROVENANCE.json create mode 100644 research/crt-unary-stencil-producer/ORACLE-RESULT.json create mode 100644 research/crt-unary-stencil-producer/PRIMARY-REVIEW.json create mode 100644 research/crt-unary-stencil-producer/PRIMARY-REVIEW.md create mode 100644 research/crt-unary-stencil-producer/PROOF.md create mode 100644 research/crt-unary-stencil-producer/README.md create mode 100644 research/crt-unary-stencil-producer/RESULT.json create mode 100644 research/crt-unary-stencil-producer/SOURCES.json create mode 100644 research/crt-unary-stencil-producer/TASK.json create mode 100644 research/crt-unary-stencil-producer/VERIFY.json create mode 100644 research/crt-unary-stencil-producer/cost_check.py create mode 100644 research/crt-unary-stencil-producer/cross_check.py create mode 100644 research/crt-unary-stencil-producer/independent_oracle.py create mode 100644 research/crt-unary-stencil-producer/primary_verify.py create mode 100644 research/crt-unary-stencil-producer/producer.py diff --git a/research/crt-unary-stencil-producer/COST-RESULT.json b/research/crt-unary-stencil-producer/COST-RESULT.json new file mode 100644 index 0000000000..171d56e20e --- /dev/null +++ b/research/crt-unary-stencil-producer/COST-RESULT.json @@ -0,0 +1,270 @@ +{ + "action_formula": "33H+25K+38Y-6G-J+12B+335", + "cases": [ + { + "geometry_G_H_K_Y_J_B": [ + 1, + 1, + 5, + 5, + 0, + 0 + ], + "moves": 298, + "primitive_actions": 677, + "reads": 314, + "reported_actions": 677, + "roles": 15, + "visited_cells": 71, + "writes": 65 + }, + { + "geometry_G_H_K_Y_J_B": [ + 1, + 3, + 5, + 9, + 2, + 2 + ], + "moves": 414, + "primitive_actions": 917, + "reads": 412, + "reported_actions": 917, + "roles": 15, + "visited_cells": 99, + "writes": 91 + }, + { + "geometry_G_H_K_Y_J_B": [ + 1, + 1, + 7, + 8, + 1, + 0 + ], + "moves": 376, + "primitive_actions": 840, + "reads": 382, + "reported_actions": 840, + "roles": 15, + "visited_cells": 87, + "writes": 82 + }, + { + "geometry_G_H_K_Y_J_B": [ + 2, + 2, + 6, + 6, + 0, + 0 + ], + "moves": 342, + "primitive_actions": 767, + "reads": 353, + "reported_actions": 767, + "roles": 15, + "visited_cells": 80, + "writes": 72 + }, + { + "geometry_G_H_K_Y_J_B": [ + 2, + 5, + 9, + 15, + 3, + 4 + ], + "moves": 612, + "primitive_actions": 1328, + "reads": 583, + "reported_actions": 1328, + "roles": 15, + "visited_cells": 142, + "writes": 133 + }, + { + "geometry_G_H_K_Y_J_B": [ + 3, + 3, + 7, + 7, + 0, + 1 + ], + "moves": 392, + "primitive_actions": 869, + "reads": 397, + "reported_actions": 869, + "roles": 15, + "visited_cells": 91, + "writes": 80 + }, + { + "geometry_G_H_K_Y_J_B": [ + 3, + 4, + 10, + 16, + 6, + 0 + ], + "moves": 600, + "primitive_actions": 1301, + "reads": 579, + "reported_actions": 1301, + "roles": 15, + "visited_cells": 135, + "writes": 122 + }, + { + "geometry_G_H_K_Y_J_B": [ + 4, + 8, + 8, + 15, + 7, + 3 + ], + "moves": 638, + "primitive_actions": 1374, + "reads": 610, + "reported_actions": 1374, + "roles": 15, + "visited_cells": 148, + "writes": 126 + }, + { + "geometry_G_H_K_Y_J_B": [ + 8, + 10, + 12, + 20, + 8, + 4 + ], + "moves": 806, + "primitive_actions": 1717, + "reads": 761, + "reported_actions": 1717, + "roles": 15, + "visited_cells": 182, + "writes": 150 + }, + { + "geometry_G_H_K_Y_J_B": [ + 15, + 17, + 21, + 30, + 9, + 2 + ], + "moves": 1180, + "primitive_actions": 2486, + "reads": 1092, + "reported_actions": 2486, + "roles": 15, + "visited_cells": 257, + "writes": 214 + }, + { + "geometry_G_H_K_Y_J_B": [ + 31, + 32, + 35, + 40, + 5, + 0 + ], + "moves": 1724, + "primitive_actions": 3595, + "reads": 1577, + "reported_actions": 3595, + "roles": 15, + "visited_cells": 365, + "writes": 294 + }, + { + "geometry_G_H_K_Y_J_B": [ + 1, + 80, + 5, + 9, + 4, + 90 + ], + "moves": 2174, + "primitive_actions": 4512, + "reads": 1855, + "reported_actions": 4512, + "roles": 15, + "visited_cells": 583, + "writes": 483 + }, + { + "geometry_G_H_K_Y_J_B": [ + 1, + 1, + 100, + 120, + 20, + 3 + ], + "moves": 3526, + "primitive_actions": 7438, + "reads": 3119, + "reported_actions": 7438, + "roles": 15, + "visited_cells": 727, + "writes": 793 + }, + { + "geometry_G_H_K_Y_J_B": [ + 100, + 120, + 104, + 140, + 36, + 20 + ], + "moves": 5742, + "primitive_actions": 11819, + "reads": 5111, + "reported_actions": 11819, + "roles": 15, + "visited_cells": 1226, + "writes": 966 + } + ], + "code_sha256": "b99e59c5a964308a2bde87f390729474b18b3ea50a4a45c1d861008487cf96bd", + "consumer_sha256": "1cb27312932914eb631078bd56e85feb1dc6c4191e9d1962b2cc3a7e1cfb8df7", + "control_guardrail": { + "primitive_attributes": [ + "move", + "read", + "write" + ], + "syntactic_guardrail_only_not_formal_compilation": true + }, + "limits": [ + "finite-control AST check is a guardrail, not a formal compiler certificate", + "canonical distinct protected unary role inputs with blank tails are an interface premise", + "no full many-target/transformed-descriptor/caller E evaluation or outer theorem" + ], + "producer_sha256": "8586d019a0a35390d36b944a2b764ec96682040b1abc42e29d740faf5a830bd0", + "scope": "Exact affine formulas justified by separate macro proof; finite actual-program primitive-call instrumentation corroborates them. No duplicate semantic oracle or complete caller theorem.", + "status": "PASS_INDEPENDENT_PRODUCER_ACTION_AND_OWNERSHIP_CENSUS", + "underbilled_READ_control": { + "invoice_rejected": true, + "omitted_READ_actions": 1, + "primitive_actions": 677, + "reported_actions": 676, + "same_actual_program": true, + "same_final_cells_and_ownership": true + }, + "visited_cell_formula": "4H+2K+4Y-G+2B+38" +} diff --git a/research/crt-unary-stencil-producer/CROSS-REPLAY.json b/research/crt-unary-stencil-producer/CROSS-REPLAY.json new file mode 100644 index 0000000000..f40cea69e5 --- /dev/null +++ b/research/crt-unary-stencil-producer/CROSS-REPLAY.json @@ -0,0 +1,1110 @@ +{ + "addresses": 433280, + "declared_source_bindings": 7, + "geometries": 83, + "rows": [ + { + "addresses": 128, + "geometry": [ + 1, + 1, + 5, + 5, + 0, + 0 + ], + "scanner_actions": 9197, + "setup_actions": 677 + }, + { + "addresses": 256, + "geometry": [ + 1, + 1, + 5, + 5, + 0, + 1 + ], + "scanner_actions": 20346, + "setup_actions": 689 + }, + { + "addresses": 256, + "geometry": [ + 1, + 1, + 5, + 6, + 0, + 0 + ], + "scanner_actions": 20346, + "setup_actions": 715 + }, + { + "addresses": 512, + "geometry": [ + 1, + 1, + 5, + 6, + 0, + 1 + ], + "scanner_actions": 44679, + "setup_actions": 727 + }, + { + "addresses": 256, + "geometry": [ + 1, + 1, + 5, + 6, + 1, + 0 + ], + "scanner_actions": 20346, + "setup_actions": 714 + }, + { + "addresses": 512, + "geometry": [ + 1, + 1, + 5, + 6, + 1, + 1 + ], + "scanner_actions": 44679, + "setup_actions": 726 + }, + { + "addresses": 512, + "geometry": [ + 1, + 1, + 5, + 7, + 1, + 0 + ], + "scanner_actions": 44679, + "setup_actions": 752 + }, + { + "addresses": 1024, + "geometry": [ + 1, + 1, + 5, + 7, + 1, + 1 + ], + "scanner_actions": 97428, + "setup_actions": 764 + }, + { + "addresses": 512, + "geometry": [ + 1, + 1, + 5, + 7, + 2, + 0 + ], + "scanner_actions": 44679, + "setup_actions": 751 + }, + { + "addresses": 1024, + "geometry": [ + 1, + 1, + 5, + 7, + 2, + 1 + ], + "scanner_actions": 97428, + "setup_actions": 763 + }, + { + "addresses": 1024, + "geometry": [ + 1, + 1, + 5, + 8, + 2, + 0 + ], + "scanner_actions": 97428, + "setup_actions": 789 + }, + { + "addresses": 2048, + "geometry": [ + 1, + 1, + 5, + 8, + 2, + 1 + ], + "scanner_actions": 211105, + "setup_actions": 801 + }, + { + "addresses": 256, + "geometry": [ + 1, + 1, + 6, + 6, + 0, + 0 + ], + "scanner_actions": 20346, + "setup_actions": 740 + }, + { + "addresses": 512, + "geometry": [ + 1, + 1, + 6, + 6, + 0, + 1 + ], + "scanner_actions": 44679, + "setup_actions": 752 + }, + { + "addresses": 512, + "geometry": [ + 1, + 1, + 6, + 7, + 0, + 0 + ], + "scanner_actions": 44679, + "setup_actions": 778 + }, + { + "addresses": 1024, + "geometry": [ + 1, + 1, + 6, + 7, + 0, + 1 + ], + "scanner_actions": 97428, + "setup_actions": 790 + }, + { + "addresses": 512, + "geometry": [ + 1, + 1, + 6, + 7, + 1, + 0 + ], + "scanner_actions": 44679, + "setup_actions": 777 + }, + { + "addresses": 1024, + "geometry": [ + 1, + 1, + 6, + 7, + 1, + 1 + ], + "scanner_actions": 97428, + "setup_actions": 789 + }, + { + "addresses": 1024, + "geometry": [ + 1, + 1, + 6, + 8, + 1, + 0 + ], + "scanner_actions": 97428, + "setup_actions": 815 + }, + { + "addresses": 2048, + "geometry": [ + 1, + 1, + 6, + 8, + 1, + 1 + ], + "scanner_actions": 211105, + "setup_actions": 827 + }, + { + "addresses": 1024, + "geometry": [ + 1, + 1, + 6, + 8, + 2, + 0 + ], + "scanner_actions": 97428, + "setup_actions": 814 + }, + { + "addresses": 2048, + "geometry": [ + 1, + 1, + 6, + 8, + 2, + 1 + ], + "scanner_actions": 211105, + "setup_actions": 826 + }, + { + "addresses": 2048, + "geometry": [ + 1, + 1, + 6, + 9, + 2, + 0 + ], + "scanner_actions": 211105, + "setup_actions": 852 + }, + { + "addresses": 4096, + "geometry": [ + 1, + 1, + 6, + 9, + 2, + 1 + ], + "scanner_actions": 454830, + "setup_actions": 864 + }, + { + "addresses": 512, + "geometry": [ + 1, + 2, + 5, + 5, + 0, + 0 + ], + "scanner_actions": 44679, + "setup_actions": 710 + }, + { + "addresses": 1024, + "geometry": [ + 1, + 2, + 5, + 5, + 0, + 1 + ], + "scanner_actions": 97428, + "setup_actions": 722 + }, + { + "addresses": 1024, + "geometry": [ + 1, + 2, + 5, + 6, + 0, + 0 + ], + "scanner_actions": 97428, + "setup_actions": 748 + }, + { + "addresses": 2048, + "geometry": [ + 1, + 2, + 5, + 6, + 0, + 1 + ], + "scanner_actions": 211105, + "setup_actions": 760 + }, + { + "addresses": 1024, + "geometry": [ + 1, + 2, + 5, + 6, + 1, + 0 + ], + "scanner_actions": 97428, + "setup_actions": 747 + }, + { + "addresses": 2048, + "geometry": [ + 1, + 2, + 5, + 6, + 1, + 1 + ], + "scanner_actions": 211105, + "setup_actions": 759 + }, + { + "addresses": 2048, + "geometry": [ + 1, + 2, + 5, + 7, + 1, + 0 + ], + "scanner_actions": 211105, + "setup_actions": 785 + }, + { + "addresses": 4096, + "geometry": [ + 1, + 2, + 5, + 7, + 1, + 1 + ], + "scanner_actions": 454830, + "setup_actions": 797 + }, + { + "addresses": 2048, + "geometry": [ + 1, + 2, + 5, + 7, + 2, + 0 + ], + "scanner_actions": 211105, + "setup_actions": 784 + }, + { + "addresses": 4096, + "geometry": [ + 1, + 2, + 5, + 7, + 2, + 1 + ], + "scanner_actions": 454830, + "setup_actions": 796 + }, + { + "addresses": 4096, + "geometry": [ + 1, + 2, + 5, + 8, + 2, + 0 + ], + "scanner_actions": 454830, + "setup_actions": 822 + }, + { + "addresses": 8192, + "geometry": [ + 1, + 2, + 5, + 8, + 2, + 1 + ], + "scanner_actions": 975035, + "setup_actions": 834 + }, + { + "addresses": 1024, + "geometry": [ + 1, + 2, + 6, + 6, + 0, + 0 + ], + "scanner_actions": 97428, + "setup_actions": 773 + }, + { + "addresses": 2048, + "geometry": [ + 1, + 2, + 6, + 6, + 0, + 1 + ], + "scanner_actions": 211105, + "setup_actions": 785 + }, + { + "addresses": 2048, + "geometry": [ + 1, + 2, + 6, + 7, + 0, + 0 + ], + "scanner_actions": 211105, + "setup_actions": 811 + }, + { + "addresses": 4096, + "geometry": [ + 1, + 2, + 6, + 7, + 0, + 1 + ], + "scanner_actions": 454830, + "setup_actions": 823 + }, + { + "addresses": 2048, + "geometry": [ + 1, + 2, + 6, + 7, + 1, + 0 + ], + "scanner_actions": 211105, + "setup_actions": 810 + }, + { + "addresses": 4096, + "geometry": [ + 1, + 2, + 6, + 7, + 1, + 1 + ], + "scanner_actions": 454830, + "setup_actions": 822 + }, + { + "addresses": 4096, + "geometry": [ + 1, + 2, + 6, + 8, + 1, + 0 + ], + "scanner_actions": 454830, + "setup_actions": 848 + }, + { + "addresses": 8192, + "geometry": [ + 1, + 2, + 6, + 8, + 1, + 1 + ], + "scanner_actions": 975035, + "setup_actions": 860 + }, + { + "addresses": 4096, + "geometry": [ + 1, + 2, + 6, + 8, + 2, + 0 + ], + "scanner_actions": 454830, + "setup_actions": 847 + }, + { + "addresses": 8192, + "geometry": [ + 1, + 2, + 6, + 8, + 2, + 1 + ], + "scanner_actions": 975035, + "setup_actions": 859 + }, + { + "addresses": 8192, + "geometry": [ + 1, + 2, + 6, + 9, + 2, + 0 + ], + "scanner_actions": 975035, + "setup_actions": 885 + }, + { + "addresses": 16384, + "geometry": [ + 1, + 2, + 6, + 9, + 2, + 1 + ], + "scanner_actions": 2080968, + "setup_actions": 897 + }, + { + "addresses": 1024, + "geometry": [ + 2, + 2, + 6, + 6, + 0, + 0 + ], + "scanner_actions": 97428, + "setup_actions": 767 + }, + { + "addresses": 2048, + "geometry": [ + 2, + 2, + 6, + 6, + 0, + 1 + ], + "scanner_actions": 211105, + "setup_actions": 779 + }, + { + "addresses": 2048, + "geometry": [ + 2, + 2, + 6, + 7, + 0, + 0 + ], + "scanner_actions": 211105, + "setup_actions": 805 + }, + { + "addresses": 4096, + "geometry": [ + 2, + 2, + 6, + 7, + 0, + 1 + ], + "scanner_actions": 454830, + "setup_actions": 817 + }, + { + "addresses": 2048, + "geometry": [ + 2, + 2, + 6, + 7, + 1, + 0 + ], + "scanner_actions": 211105, + "setup_actions": 804 + }, + { + "addresses": 4096, + "geometry": [ + 2, + 2, + 6, + 7, + 1, + 1 + ], + "scanner_actions": 454830, + "setup_actions": 816 + }, + { + "addresses": 4096, + "geometry": [ + 2, + 2, + 6, + 8, + 1, + 0 + ], + "scanner_actions": 454830, + "setup_actions": 842 + }, + { + "addresses": 8192, + "geometry": [ + 2, + 2, + 6, + 8, + 1, + 1 + ], + "scanner_actions": 975035, + "setup_actions": 854 + }, + { + "addresses": 4096, + "geometry": [ + 2, + 2, + 6, + 8, + 2, + 0 + ], + "scanner_actions": 454830, + "setup_actions": 841 + }, + { + "addresses": 8192, + "geometry": [ + 2, + 2, + 6, + 8, + 2, + 1 + ], + "scanner_actions": 975035, + "setup_actions": 853 + }, + { + "addresses": 8192, + "geometry": [ + 2, + 2, + 6, + 9, + 2, + 0 + ], + "scanner_actions": 975035, + "setup_actions": 879 + }, + { + "addresses": 16384, + "geometry": [ + 2, + 2, + 6, + 9, + 2, + 1 + ], + "scanner_actions": 2080968, + "setup_actions": 891 + }, + { + "addresses": 2048, + "geometry": [ + 2, + 2, + 7, + 7, + 0, + 0 + ], + "scanner_actions": 211105, + "setup_actions": 830 + }, + { + "addresses": 4096, + "geometry": [ + 2, + 2, + 7, + 7, + 0, + 1 + ], + "scanner_actions": 454830, + "setup_actions": 842 + }, + { + "addresses": 4096, + "geometry": [ + 2, + 2, + 7, + 8, + 0, + 0 + ], + "scanner_actions": 454830, + "setup_actions": 868 + }, + { + "addresses": 8192, + "geometry": [ + 2, + 2, + 7, + 8, + 0, + 1 + ], + "scanner_actions": 975035, + "setup_actions": 880 + }, + { + "addresses": 4096, + "geometry": [ + 2, + 2, + 7, + 8, + 1, + 0 + ], + "scanner_actions": 454830, + "setup_actions": 867 + }, + { + "addresses": 8192, + "geometry": [ + 2, + 2, + 7, + 8, + 1, + 1 + ], + "scanner_actions": 975035, + "setup_actions": 879 + }, + { + "addresses": 8192, + "geometry": [ + 2, + 2, + 7, + 9, + 1, + 0 + ], + "scanner_actions": 975035, + "setup_actions": 905 + }, + { + "addresses": 16384, + "geometry": [ + 2, + 2, + 7, + 9, + 1, + 1 + ], + "scanner_actions": 2080968, + "setup_actions": 917 + }, + { + "addresses": 8192, + "geometry": [ + 2, + 2, + 7, + 9, + 2, + 0 + ], + "scanner_actions": 975035, + "setup_actions": 904 + }, + { + "addresses": 16384, + "geometry": [ + 2, + 2, + 7, + 9, + 2, + 1 + ], + "scanner_actions": 2080968, + "setup_actions": 916 + }, + { + "addresses": 16384, + "geometry": [ + 2, + 2, + 7, + 10, + 2, + 0 + ], + "scanner_actions": 2080968, + "setup_actions": 942 + }, + { + "addresses": 4096, + "geometry": [ + 2, + 3, + 6, + 6, + 0, + 0 + ], + "scanner_actions": 454830, + "setup_actions": 800 + }, + { + "addresses": 8192, + "geometry": [ + 2, + 3, + 6, + 6, + 0, + 1 + ], + "scanner_actions": 975035, + "setup_actions": 812 + }, + { + "addresses": 8192, + "geometry": [ + 2, + 3, + 6, + 7, + 0, + 0 + ], + "scanner_actions": 975035, + "setup_actions": 838 + }, + { + "addresses": 16384, + "geometry": [ + 2, + 3, + 6, + 7, + 0, + 1 + ], + "scanner_actions": 2080968, + "setup_actions": 850 + }, + { + "addresses": 8192, + "geometry": [ + 2, + 3, + 6, + 7, + 1, + 0 + ], + "scanner_actions": 975035, + "setup_actions": 837 + }, + { + "addresses": 16384, + "geometry": [ + 2, + 3, + 6, + 7, + 1, + 1 + ], + "scanner_actions": 2080968, + "setup_actions": 849 + }, + { + "addresses": 16384, + "geometry": [ + 2, + 3, + 6, + 8, + 1, + 0 + ], + "scanner_actions": 2080968, + "setup_actions": 875 + }, + { + "addresses": 16384, + "geometry": [ + 2, + 3, + 6, + 8, + 2, + 0 + ], + "scanner_actions": 2080968, + "setup_actions": 874 + }, + { + "addresses": 8192, + "geometry": [ + 2, + 3, + 7, + 7, + 0, + 0 + ], + "scanner_actions": 975035, + "setup_actions": 863 + }, + { + "addresses": 16384, + "geometry": [ + 2, + 3, + 7, + 7, + 0, + 1 + ], + "scanner_actions": 2080968, + "setup_actions": 875 + }, + { + "addresses": 16384, + "geometry": [ + 2, + 3, + 7, + 8, + 0, + 0 + ], + "scanner_actions": 2080968, + "setup_actions": 901 + }, + { + "addresses": 16384, + "geometry": [ + 2, + 3, + 7, + 8, + 1, + 0 + ], + "scanner_actions": 2080968, + "setup_actions": 900 + } + ], + "scanner_actions": 51658145, + "scope": "One-target unary geometry producer composed with unchanged scanner. Finite execution corroborates the separate all-admitted-input proof; no binary/global descriptor, many-target, payload or full CRT theorem.", + "semantic_producer_consumer_controls": [ + { + "correct_bad": "1", + "first_different_address": 16, + "mutant": "include_parity", + "mutant_bad": "0" + }, + { + "correct_bad": "1", + "first_different_address": 0, + "mutant": "wrong_lower_pivot", + "mutant_bad": "0" + }, + { + "correct_bad": "0", + "first_different_address": 64, + "mutant": "wrong_upper_pivot", + "mutant_bad": "1" + } + ], + "setup_actions": 67748, + "status": "PASS_UNARY_STENCIL_CALLER_CROSSCHECK" +} diff --git a/research/crt-unary-stencil-producer/ORACLE-NOTES.txt b/research/crt-unary-stencil-producer/ORACLE-NOTES.txt new file mode 100644 index 0000000000..812177cda4 --- /dev/null +++ b/research/crt-unary-stencil-producer/ORACLE-NOTES.txt @@ -0,0 +1,37 @@ +Independent one-target CRT guard geometry oracle + +This module was written before viewing the new encoded producer. No primary +producer or consumer code is imported. The old PR4201 machine/verify code and +the canonical check_batched_crt.py predicates were read as interface/source +specification only. The consumer remains unchanged in the parent's integration. + +API: expected_stencil(G,H,K,Y,J,B) returns the exact finite-alphabet token list. +source_good(address,G,H,K,Y,J,B) independently decodes u/t/y/B and applies the +source's numeric predicate. Geometry requires exact integers, G>=1, H>=G, +K>=G+4, J>=0, B>=0, Y>=J+K. Intervals are MSB-indexed half-open ranges. + +The two G-bit active digits occupy [H-G,H) and [2H-G,2H). The guard occupies +[2H+Y-J-K,2H+Y-J-1), so parity bit J is excluded. Its lower bound is inclusive +2^(G+1) and upper bound is strict 2^(K-1)-2^(G+1). All other bits are SKIP. + +Finite coverage: every address for all 83 geometries in the recorded cap, +433280 addresses total. A separate interval-integer interpreter (not the +consumer's comparison-flag algorithm) matches the direct source formula. +Boundary coverage includes G=1,2,3,8,31; J=0,1,3; lower-1/lower/lower+1 and +upper-1/upper/upper+1; parity and all ignored-field classes independently +toggled in two patterns. Nine malformed numeric geometries are rejected. +Five semantic boundary witnesses expose relaxed comparisons, parity inclusion, +and accidentally testing complete H fields rather than active G-bit digits. +These are specification witnesses, not executed mutants of the new producer. + +This is an unpriced direct numeric oracle. It does not establish that a fixed +tape machine constructs/admit/erases the stencil with the claimed invoice. +That needs the new producer, exact machine accounting, and written proof. +Neither finite enumeration nor a green replay certifies the full CRT supplier, +multi-target production reservoir, evaluator, physical repair/callee/precision, +outer multiplication theorem or any new kappa. + +Credit: the PR4201 guard-consumer package, Cinna Davis PR4100's original scan +proposal, Hiroki KUMAZAKI's PR4169/PR4174 repair/placement context, and the +canonical CRT source/NOTICE lineage remain predecessor work. Substantial +OpenAI Codex assistance; Apache-2.0 repository contribution. diff --git a/research/crt-unary-stencil-producer/ORACLE-PROVENANCE.json b/research/crt-unary-stencil-producer/ORACLE-PROVENANCE.json new file mode 100644 index 0000000000..186b7582aa --- /dev/null +++ b/research/crt-unary-stencil-producer/ORACLE-PROVENANCE.json @@ -0,0 +1,23 @@ +{ + "commands": [ + "python3 -I -B oracle.py --output ORACLE.json", + "python3 -I -O -W error -B oracle.py --output ORACLE-O.json" + ], + "files": { + "NOTES.txt": "8e6a0fb65cb40203ce83df4d487302434c39b774e99ef0865bfea6b7ae6d8eee", + "ORACLE-O.json": "766aa0c148bb027ef317011648d623f4610c1e6fe7a499aab25b4ab2138e4363", + "ORACLE.json": "766aa0c148bb027ef317011648d623f4610c1e6fe7a499aab25b4ab2138e4363", + "oracle.py": "78ba91c921ddcb37cefe674e10f34e9f896c6243af859bdb63f50b6e7086cd34" + }, + "python": "3.12.14", + "result_normal_O_identical": true, + "sources_read": { + "AGENTS.md": "eb25d8ec495b80190a4b1a634710819bb74f0fae88d5203285c2b75b6f147347", + "CONTRIBUTING.md": "8a49fe97e2ad088a2b2e0c5b222aaab08752783b1f9c1260790d7dd13011d215", + "PR4201/machine.py": "1cb27312932914eb631078bd56e85feb1dc6c4191e9d1962b2cc3a7e1cfb8df7", + "PR4201/verify.py": "40794cd2e2936f0f5e42fac1bb51b65c951a2ab56b7e88824e8c2d09a3dbf40e", + "autoresearch.md": "8c98d179208c34a8c6768931e13f3bbeaa1cb63d59c660799ffde05c40935d9b", + "research/unconditional-batched-crt/check_batched_crt.py": "681e2e3d71fa74c8b9b326f3860104fd9d89590a222e26ae6ee718d1fd40ff2e" + }, + "status": "FROZEN_BEFORE_PRIMARY_PRODUCER_VIEW" +} diff --git a/research/crt-unary-stencil-producer/ORACLE-RESULT.json b/research/crt-unary-stencil-producer/ORACLE-RESULT.json new file mode 100644 index 0000000000..3180443106 --- /dev/null +++ b/research/crt-unary-stencil-producer/ORACLE-RESULT.json @@ -0,0 +1,1278 @@ +{ + "address_count": 433280, + "admission_controls": { + "classes": [ + "zero G", + "H=1,H>=G,K>=G+4,Y>=J+K,J>=0,B_back>=0; distinct roles, unique permanent LEFT and initially blank tails", + "no_new_kappa": true, + "oracle_original_to_package": { + "NOTES.txt": "ORACLE-NOTES.txt", + "ORACLE-O.json": "ORACLE-RESULT.json", + "ORACLE.json": "ORACLE-RESULT.json", + "oracle.py": "independent_oracle.py" + }, + "package_file_snapshot": { + "COST-RESULT.json": { + "bytes": 5430, + "sha256": "640fa1b1f16fd1ed8a52126942aa2cfb9587ea929c525d166d74cd02fd0a366b" + }, + "CROSS-REPLAY.json": { + "bytes": 16802, + "sha256": "f2f0e60af593ccfae0fd9531d906ad1911be4071e7fb3cef3d0d3a16ee8e0a0d" + }, + "ORACLE-NOTES.txt": { + "bytes": 2299, + "sha256": "8e6a0fb65cb40203ce83df4d487302434c39b774e99ef0865bfea6b7ae6d8eee" + }, + "ORACLE-PROVENANCE.json": { + "bytes": 1222, + "sha256": "1c96880736652b5729f70decec6dc3b205e2622f6443b1324ee8485e9d64337d" + }, + "ORACLE-RESULT.json": { + "bytes": 33302, + "sha256": "766aa0c148bb027ef317011648d623f4610c1e6fe7a499aab25b4ab2138e4363" + }, + "PROOF.md": { + "bytes": 13192, + "sha256": "4076e6041bedce5269c1d4e3d62f0e4213a4b2e790fe270b89b4b4f3363e08aa" + }, + "README.md": { + "bytes": 5512, + "sha256": "747255e3c7b58c9f7ba77ccaa82799628e66851091f35c408db1950a6c91bf47" + }, + "RESULT.json": { + "bytes": 69491, + "sha256": "131bebf8f8b1a628789c5c959959f07fd4d2f77ad3e367f2381136d72b0289d5" + }, + "SOURCE-PINS.json": { + "bytes": 1606, + "sha256": "0f196c956560409319ac51d153341c012f448d38c9c9e4d46d898d021a5c4b80" + }, + "SOURCES.json": { + "bytes": 2906, + "sha256": "28d47c5c1b34b20b1c2ce1c2962b06a23f4892e0bec8bed6a7ef42ff1a5c5094" + }, + "TASK.json": { + "bytes": 6412, + "sha256": "ef9934bb20185430fae29c07cf46de1906bcdd48a890d3c94414dbb5ac5106c5" + }, + "VERIFY.json": { + "bytes": 3042, + "sha256": "17cf82f7c39e5a1dfac9fe5714b1aca7f0d2e7ac3c27f675d3c990fd9eb26680" + }, + "cost_check.py": { + "bytes": 7487, + "sha256": "b99e59c5a964308a2bde87f390729474b18b3ea50a4a45c1d861008487cf96bd" + }, + "cross_check.py": { + "bytes": 7438, + "sha256": "c73b50621ce31be84f617a34f0dc9a421fff89622615771e129dcba17e9608c3" + }, + "independent_oracle.py": { + "bytes": 10252, + "sha256": "78ba91c921ddcb37cefe674e10f34e9f896c6243af859bdb63f50b6e7086cd34" + }, + "primary_verify.py": { + "bytes": 12067, + "sha256": "0754df084eb32403c865d36b71837a4f85e805460779380add3dcbce8e9ce997" + }, + "producer.py": { + "bytes": 6012, + "sha256": "8586d019a0a35390d36b944a2b764ec96682040b1abc42e29d740faf5a830bd0" + }, + "source/PREDECESSOR-PROOF.md.txt": { + "bytes": 10476, + "sha256": "c075a3c261bb824884f0da9f99fed227b15f9fac087bbdeb2c2cb861d4091f11" + }, + "source/PREDECESSOR-README.md.txt": { + "bytes": 3880, + "sha256": "912595166aded8591819c1f4fccdd7bfa44361906a1466057f838a656e85f329" + }, + "source/predecessor_adapter.py": { + "bytes": 11970, + "sha256": "40794cd2e2936f0f5e42fac1bb51b65c951a2ab56b7e88824e8c2d09a3dbf40e" + }, + "source/predecessor_machine.py": { + "bytes": 5545, + "sha256": "1cb27312932914eb631078bd56e85feb1dc6c4191e9d1962b2cc3a7e1cfb8df7" + } + }, + "package_metadata_review": { + "README_TASK_VERIFY_scope_credit_cost_boundary_consistent": true, + "TASK_unary_setup_updated_from_under_construction_to_scoped_proved_and_agent_checked": true, + "actual_committed_git_free_remote_and_hosted_replays": "later coordinator verification; not yet claimed by this review", + "all_argv_portable_no_fixed_output_path": true, + "declared_input_bindings_verified": 7, + "declared_sources_bindings_verified": 9, + "four_unchanged_predecessor_exports_verified": true, + "no_private_local_paths_in_public_text": true, + "registered_commands": 8, + "retained_source_ancestor": "5a41fea466cbeb7839bde864e563e191de47a0f7" + }, + "package_snapshot_excludes": "This review JSON/MD themselves, which are added only after the snapshot; future coordinator records source-history/cold/publication/CI separately.", + "proof_method": "Independent macro-composition derivation; finite instrumentation corroborates, not proves universal formula.", + "remaining": [ + "unary input production from actual binary/source/transformed descriptors", + "many-target/color descriptor integration", + "complete E evaluator and sparse repair/caller tariff", + "ordinary callees, precision, native placement and outer multiplication theorem", + "human or formal-kernel acceptance" + ], + "reviewer": "separate OpenAI Codex agent; not human or formal-kernel acceptance", + "scope": "Canonical six protected unary roles, one target J, all admitted lengths; actual source/binary descriptor production and many-target integration remain open.", + "source_head": "4f49743a9df0cf7501cdc62bd5707a122fa071e9", + "status": "PASS_ENCODED_ONE_TARGET_PRODUCER_CONTRACT_AND_EXACT_INVOICE_REVIEW", + "substantial_ai_assistance": true, + "verification": { + "independent_cost_geometries": 14, + "normal_exit": 0, + "primary_and_cross_review_method": "code inspection; no redundant scientific replay", + "receipts_byte_identical": true, + "strict_optimized_exit": 0, + "underbilled_READ_invoice_rejected": true, + "underbilled_READ_primitive_actions": 677, + "underbilled_READ_reported_actions": 676, + "underbilled_READ_same_final_cells_and_ownership": true + } +} diff --git a/research/crt-unary-stencil-producer/PRIMARY-REVIEW.md b/research/crt-unary-stencil-producer/PRIMARY-REVIEW.md new file mode 100644 index 0000000000..5b6bd7fe53 --- /dev/null +++ b/research/crt-unary-stencil-producer/PRIMARY-REVIEW.md @@ -0,0 +1,24 @@ +# Independent unary-producer contract and invoice review + +Status: PASS for the explicitly encoded one-target interface. This is a separate OpenAI Codex agent review, not human acceptance or formal-kernel verification. + +The new paid program takes six distinct protected unary roles G,H,K,Y,J,B_back, with unique permanent LEFT infrastructure and initially blank tails, and admits exactly G>=1, H>=G, K>=G+4, Y>=J+K, J/B_back>=0. Admission reads the encoding and executes unary comparisons/subtractions. It is not a host-side inequality predicate. The arbitrary-infinite-tail property and physical role separation are representation/infrastructure premises, not a decidable admission claim. Input construction from binary or actual transported descriptors remains unpriced. + +Code inspection confirms that producer.py accesses only read/write/move methods. Every mutable control flag ranges over a fixed finite set; all variable-length traversal is marker driven. The nine created roles are eight private words plus one owned stencil. All arithmetic rejects before stencil construction. Subtraction underflow happens before output writes, so each private word remains END-terminated and rejection cleanup can erase it. On success or the stated grammar/arithmetic rejection paths, private data and END markers are blank, input data remains protected, and heads return to LEFT. Successful owned stencil data remains available. After consuming it, the caller still owns that stencil and the BAD mask; clearing/consuming owned outputs before role reuse is a caller obligation. + +The stencil pattern is exactly S^(H-G) D^G S^(H-G) D^G S^(Y-J-K) GUARD^(K-1) S^(J+1) S^B_back. It tests the two active low G-bit digits and the K-1 guard bits above the excluded target parity bit J. With a=K-G-3>=1, the MSB-first lower threshold is 0^a 1 0^(G+1), and the upper threshold is 1^a 1 0^(G+1). The supplied-stencil consumer is byte-identical to PR4201. This is a meaningful executable refinement for positions=(J,), r=1; it does not establish the many-target/color or complete transported-caller boundary. + +I independently derived the successful affine invoice from the literal macros, before comparing finite counters. For a unary word n and a subtraction a-b with 0<=b<=a: rewind from head n costs 2n+1; validate costs 4n+10; difference costs 8a+15; plus_one costs 8a+14; the fixed three costs17; skip/digit/leading_guard/trailing_guard cost6n+5; erase from LEFT costs5n+7. All marker reads and returns are included. With N=G+H+K+Y+J+B_back, L=2H+Y+B_back and W=H+K-2G+2Y-J+2, the phase sum is + + 27 + (4N+60) + (8H+16K+16Y+130) + (8L+46) + (5W+56) + 6 + = 33H+25K+38Y-6G-J+12B_back+335 <= 63L+335. + +The protected input roles visit N+18 cells, the eight private roles W+16, and the stencil L+2. Thus setup visited cells are exactly4H+2K+4Y-G+2B_back+38 <=6L+38. Adding the unchanged counter and owned mask, while sharing the stencil, yields seventeen fixed roles, time T_prod+8ML+15M+13L+18 and visited cells M+6H+2K+5Y-G+3B_back+42 <= M+7L+42. These all-size formulas are written macro arguments, not fitted finite data. Fixed finite-alphabet/control encoding changes physical machine steps only by a parameter-independent factor; the exact counts concern the stated cell/head model. + +The independent cost_check.py imports neither the primary verifier nor semantic oracle. It instruments primitive calls separately from the retained Tape's reported bill, checks the two exact formulas on14 producer-only geometries (including long and skewed inputs), and checks ownership and fifteen-role setup inventory. Normal and strict optimized runs produce identical receipts. A deliberately underbilled READ executes the actual unchanged producer with identical final cells/ownership: the primitive trace has677 actions but the faulty bill reports676. The invoice check detects that discrepancy. Its AST restriction is expressly a review guardrail, not a formal compiler certificate. + +Primary verification and the root cross-check were inspected rather than redundantly rerun here. The primary covers145 geometries, four complete consumer compositions, seven rejection cleanup cases, three executed semantic producer mutants, two ownership mutants and two pre-exec source-authentication controls. The root cross-check authenticates declared source bytes before execution, binds the pre-code direct oracle, compares every emitted token and source good/linear_guard predicate, and subtracts prior stencil action counts when computing scanner actions. Its three semantic mutants execute the actual consumer. Canonical source dependencies and the four unchanged predecessor exports are explicit in SOURCES/SOURCE-PINS. + +Remaining obligations are not discharged: producing unary inputs from actual source/binary/transformed descriptors, multiple target intervals and color ordering, complete E evaluation, extraction/keys/sort/reinsertion, payload repair, ordinary callees, precision, native placement and the outer multiplication theorem. Cinna Davis/PR4100 retains predicate/scan-proposal credit; Hiroki KUMAZAKI/PR4169/PR4174 retain repair/placement credit; PR4201 retains scanner/atom/adapter/census credit; Douglas Colkitt/OpenAI and NOTICE ancestry remain retained. No new kappa, selected-frontier result, human acceptance or full supplier is claimed. + +Final package metadata review: README/TASK/VERIFY preserve the narrow unary one-target boundary, exact invoice and credit. The corrected TASK ledger now marks unary setup as scoped written proof with separate agent checks. All9 declared source/provenance bindings (7 input bindings) match their SHA256 and Git blobs; four predecessor exports match unchanged pins. Eight portable registered commands cover normal/strict optimized primary, oracle, root cross and cost checks. The review JSON records a21-file pre-review snapshot, excluding this review pair, plus explicit original-to-package oracle receipt/name mappings. Later committed-byte/source-history, cold, remote and hosted receipts are coordinator obligations, not claimed completed by this review. diff --git a/research/crt-unary-stencil-producer/PROOF.md b/research/crt-unary-stencil-producer/PROOF.md new file mode 100644 index 0000000000..d81a6cca7c --- /dev/null +++ b/research/crt-unary-stencil-producer/PROOF.md @@ -0,0 +1,285 @@ +# A paid unary producer for one source guard stencil + +## Claim and scope + +`producer.py` gives a uniform, marker-driven tape program for the **one-target** +geometry family + + G >= 1, H >= G, K >= G+4, Y >= J+K, J >= 0, B >= 0. + +Here B denotes the spectator/back-bit count, not the radix 2^G. Input is +six protected canonical unary tapes for G,H,K,Y,J,B. On successful admission +the program outputs exactly the stencil returned by the frozen predecessor +`geometry_stencil(G,H,Y,(J,),K,B)` in PR4201 at head +`4f49743a9df0cf7501cdc62bd5707a122fa071e9`. + +Unlike the predecessor's host geometry adapter, the new producer pays every +read, write and one-cell head movement used to validate the unary inputs, +perform the required arithmetic, construct the stencil, clear private +workspace and return heads. The predecessor's scanner is then used without +modification. This closes only its supplied-stencil obligation for this +specific unary-encoded, one-target family. It does not produce arbitrary +binary-encoded CRT descriptors, many-target stencils, the full E evaluator, +complete physical placement, or a multiplication supplier. + +## Input, machine and ownership contract + +There are six fixed protected input roles. A tape of unary value n initially +has permanent LEFT, then n copies of symbol `1`, then END, with an initially +blank infinite tail. Every head enters at its unique permanent LEFT. +LEFT is reserved tape infrastructure and does not occur in input data. The +initially blank tail is part of this representation contract, rather than +a claim that a finite program decides whether an arbitrary infinite tape +is eventually blank. `validate` literally reads LEFT, every unary symbol, +END and the immediately following blank. A wrong data symbol, missing END, +or immediately nonblank END successor is rejected by paid actions. + +The producer has eight fixed private unary roles and one fresh owned +stencil role: fifteen tape roles including the six inputs. It creates no +parameter-dependent array, tape family, integer register or transition +alphabet. The private roles are HG, KG, THREE, A, TAIL, JP, YJ and YJK. +They all have permanent LEFT infrastructure like the predecessor's tapes. +Each is initialized by paid actions with an empty END-terminated unary word. + +The executable program reads and writes tape symbols and moves one cell at +a time. It never reads a host length, head coordinate, cell container, +action counter, G/H/K/Y/J/B integer, or source geometry table. Its tuples +are fixed role lists or fixed product-alphabet symbols. Every loop branches +on a read symbol or fixed finite control state; the five optional booleans +select named faulty programs used only by the verifier. + +On success all six inputs are protected, their heads are at LEFT, every +private data cell and allocated private END marker is BLANK, every private +head is at LEFT, and the owned stencil has LEFT, L atoms, END, head LEFT. +The permanently reserved LEFT markers are not erased. Visiting the blank +cell just after an input END may extend the emulator's finite cell list; +the represented infinite protected tape is unchanged. + +Grammar or arithmetic rejection happens before output generation. On these +rejections the program erases all eight private words and the empty output +word and returns every head to LEFT; input data is protected. The guarantee +assumes the input representation's unique permanent LEFT and initially +blank tail. It does not cover a broken tape primitive, an interrupted run, +or arbitrary symbols imitating the reserved boundary infrastructure. + +## Paid arithmetic and admission + +All successful arithmetic is performed by literal scans: + +- `difference(left,right,out)` scans matching unary prefixes. It rejects + if right is longer. Otherwise it copies the remaining suffix of left + into out and returns all three heads. Both operands are protected. +- `plus_one` scans/copies its operand and appends one unary symbol. +- `three` writes exactly three unary symbols and END by a fixed sequence + of actions. +- `positive` reads the first unary cell and rejects an empty word. + +The resulting private words are + + HG = H-G, + KG = K-G, + THREE= 3, + A = K-G-3, + TAIL = G+1, + JP = J+1, + YJ = Y-J, + YJK = Y-J-K. + +Every subtraction is executed and its underflow test is charged. Reading +G's first cell enforces G>=1. The H-G subtraction enforces H>=G. The +K-G and then KG-3 subtractions followed by `positive(A)` enforce exactly +K>=G+4. The two Y subtractions enforce Y>=J+K. J and B are nonnegative +by their unary representation. Thus admission is implemented inside the +paid program rather than delegated to a host inequality test. + +Importantly, subtraction underflow occurs before writing its output. +Therefore every allocated private word still has a complete END marker +when rejection cleanup begins. Arithmetic rejection cannot leave a +partially written unterminated scratch word for the eraser to search. + +## Stencil identity for all admitted geometry + +Let L=2H+Y+B. Indexing positions is used only in this written proof and in +the observer verifier, not by the executable producer. In the predecessor's +MSB-first address layout, the two H-bit digit fields precede the Y-bit +target region and B spectator bits. Its one-target stencil has the form + + S^(H-G) D^G S^(H-G) D^G + S^(Y-J-K) GUARD^(K-1) S^(J+1) S^B. + +Each D block has exactly its first/last atom marked as begin/end. The two +G-bit D intervals therefore occupy precisely the low G bits of each +H-bit digit field. Their threshold bits are both zero, as required by the +predecessor's not-all-ones digit test. + +The guard begins at position 2H+Y-J-K and ends just before +2H+Y-J-1, giving exactly K-1 higher bits of the K-bit source window. The +omitted bit J is its parity bit and is part of the following J+1 SKIP +cells. The program emits these lengths from the computed unary words, +without converting an endpoint or length to a host coordinate. + +For width K-1 the required thresholds are + + low = 2^(G+1), + high = 2^(K-1)-2^(G+1). + +Put a=K-G-3. Admission gives a>=1. Their exact MSB-first bit patterns are + + low = 0^a 1 0^(G+1), + high = 1^a 1 0^(G+1). + +The guard has a leading segment of a atoms `(low0,high1)`, one pivot +`(low1,high1)`, and a trailing segment of G+1 atoms `(low0,high0)`. +Its length is a+1+(G+1)=K-1. Begin is set only on its first leading atom; +end is set only on its last trailing atom. All other cells are the exact +predecessor SKIP atom. This proves atom-for-atom identity with the frozen +adapter for every admitted input, including G=1, H=G, K=G+4, J=0 or B=0. + +The output is owned and remains available to the unchanged consumer. +Its finite product alphabet is independent of geometry; the program does +not place an unbounded integer into a tape cell or a finite control flag. + +## Exact successful producer action invoice + +One action is one Tape.read, Tape.write or one-cell Tape.move. Host simulator +administration and observation are outside that unit-cost model, exactly as +in the predecessor. These are literal invoked actions, not a host-computed +macro tariff substituted for unexecuted scans. For an END-terminated unary +word of value n, each macro's successful action count is: + +| Macro | Entry and action count | +|---|---| +| rewind from coordinate n | 2n+1; n appears only in this proof | +| validate(n) | 4n+10 | +| difference(a,b), 0<=b<=a | 8a+15 | +| plus_one(a) | 8a+14 | +| three | 17 | +| skip/digit/leading_guard/trailing_guard(n) | 6n+5 | +| erase(n), entering at LEFT | 5n+7 | + +For example, difference(a,b) performs 3a+b+8 reads, a-b+1 +writes and 4a+6 moves, totaling 8a+15. The counts include operand +returns and output END. Rewind reads its final LEFT cell as well as +every visited cell on the way back. + +Let N=G+H+K+Y+J+B be total unary input symbols and + + W=H+K-2G+2Y-J+2 + +be total private unary symbols across the eight derived words. Summing +the fixed sequence of macros gives: + +| Stage | Actions | +|---|---| +| initialize nine empty words | 27 | +| validate six inputs | 4N+60 | +| all positivity/arithmetic operations | 8H+16K+16Y+130 | +| output atoms, END and output return | 8L+46 | +| erase eight private words | 5W+56 | +| final input-head checks/returns | 6 | + +Thus the exact normal successful setup invoice is + + T_prod = 33H+25K+38Y-6G-J+12B+335. + +Under admission K<=Y and L=2H+Y+B, so + + T_prod <= 63L+335 = O(L). + +The equation is a written all-size action derivation. Primary verification +also compares observed literal counts against it on each finite case; +finite equality alone is not the proof of the equation for unbounded input. + +## Exact visited-cell space and composition + +This space measure counts every visited tape cell, including cells erased +at the end and owned input/output. It is stronger than merely counting +nonblank cells at the endpoint. The protected roles visit N+18 cells, +including each immediate blank after END. Private roles visit W+16 and +the stencil L+2. Therefore + + S_prod = N+W+L+36 + = 4H+2K+4Y-G+2B+38 + <= 6L+38. + +The unchanged predecessor scanner adds one private counter role and one +owned BAD-mask role, reusing the produced stencil. This is seventeen +fixed roles for the composed program; no private-role reuse is claimed. +For M=2^L its separate established scanner invoice is + + T_scan = 8ML+15M+13L+18. + +All producer actions precede it, including producer cleanup, so the complete +one-target producer/consumer time is exactly T_prod+T_scan, at most + + 8ML+15M+76L+353 = O(ML). + +Its visited cells are exactly + + S_comb = S_prod+(L+2)+(M+2) + = M+6H+2K+5Y-G+3B+42 + <= M+7L+42. + +These are counts in the explicit logical finite-alphabet cell/head model. +Encoding fixed alphabet symbols/control as bits changes them only by +parameter-independent constants. They are not Python runtime predictions +or an exact coefficient for an unspecified physical transition table. + +## Evidence and controls + +`primary_verify.py` imports the literal producer and authenticated frozen +predecessor machine/adapter bytes, never a `.pyc` cache. Its host integers, +list inspection and direct formulas are observer/oracle work, not paid +producer steps. It checks 145 admitted producer geometries, including a +500-bit output and zero J/B and tight admission boundaries. It compares +every emitted stencil atom with the frozen adapter, exact observed action +and space invoices, protected input, blank private data/markers and every +head return. Four compositions execute 5,760 complete addresses through the +unchanged scanner and compare every output bit with its frozen adapter +baseline and the exact unchanged scanner action invoice. + +Four arithmetic failures and three malformed unary encodings must reject, +with allocated private/output data blank and all heads returned. Five +faulty programs must fail their named observations: included parity, +wrong lower pivot bit, wrong upper pivot bit, omitted private erasure and +omitted owned-stencil head return. The three semantic mutants are also +executed through the unchanged scanner and must change its actual mask. +An AST guardrail rejects producer host arithmetic, indexing, host-length +primitives and simulator observer fields; this is a review aid, not a +formal machine certificate. + +Both retained consumer/adapter modules are SHA256-authenticated before +compile/exec, including an overridden consumer path. Corrupted temporary +copies containing an execution-failure marker must reject at that hash +check, before their appended marker can execute. + +Independent source-predicate, cost and source-code review are separate +evidence. In particular, atom identity with a predecessor adapter and +agreement with the unchanged scanner do not alone certify the original +CRT source predicate or every inherited caller assumption. + +## Attribution and remaining obligations + +The source guard predicate, scan proposal and arithmetic context come from +Cinna Davis/PR4100. Hiroki KUMAZAKI/kumagi's PR4169/PR4174 supply retained +repair/placement context. PR4201 supplies the literal dense-guard consumer, +finite atom format, host adapter and scanner cost derivation; this package +adds a paid unary one-target producer, not that earlier scanner result. +Retain Douglas Colkitt/OpenAI and the inherited NOTICE lineage. Substantial +OpenAI Codex assistance was used for implementation, proof and separate +agent review. No human review or formal-kernel verification is claimed. +Apache-2.0. + +## Open next questions + +- Produce these unary descriptors from the actual source representation, + with paid parsing/conversion and a legal caller contract. Unary input + construction and binary/uniform descriptor production are not priced here. +- Extend to multiple target intervals with paid ordering, disjointness and + correct digit ownership; this one-target program does not establish that + wider mechanism. +- Compose the classifier with paid extraction, repair, keys, sorting, + reinsertion, ordinary callees and full E arithmetic. Precision, native + physical placement and the outer multiplication theorem remain open. +- No selected frontier, kappa value or full CRT supplier is changed by this + bounded lowering result. diff --git a/research/crt-unary-stencil-producer/README.md b/research/crt-unary-stencil-producer/README.md new file mode 100644 index 0000000000..1abff6e101 --- /dev/null +++ b/research/crt-unary-stencil-producer/README.md @@ -0,0 +1,97 @@ +# Paid unary geometry to one-target CRT guard mask + +PR4201’s literal scanner accepted an already admitted stencil and left its +geometry/threshold producer unpriced. This package supplies one actual +marker-driven producer for six protected unary geometry words +`G,H,K,Y,J,B_back`, with `G>=1, H>=G, K>=G+4, Y>=J+K` and nonnegative +`J,B_back`. It emits the exact retained stencil for target `J` and composes +with the unchanged scanner. `B_back` is a spectator-bit count; the radix is +`2^G`. + +The program pays unary syntax checks, comparisons/subtractions, threshold +construction, all transfers/head returns and erasure of eight private words, +including their right markers. It reads no simulator coordinate, host +length, integer geometry or action counter. All roles and alphabet/control +sizes are fixed. [PROOF.md](PROOF.md) proves the identity and invoice for +**every admitted unary input**. The result starts at this representation; +production/binary/transported geometry conversion and many-target ordering +remain open. + +For `L=2H+Y+B_back`, `M=2^L`, one read/write/one-cell move is one action: + +- Producer: exactly `33H+25K+38Y-6G-J+12B_back+335 <= 63L+335` actions. +- Unchanged scanner: exactly `8ML+15M+13L+18` actions. +- Composition: exactly the sum, at most `8ML+15M+76L+353`, on seventeen fixed + roles. Exact visited space is `M+6H+2K+5Y-G+3B_back+42 <= M+7L+42`. + +Input values remain protected; all private data and allocated markers are +blank and all heads return. The stencil and complete BAD mask are owned +outputs. A caller must consume and clear previous owned outputs before +reusing these fixed roles. The coefficient counts are for the explicit +finite-alphabet cell/head model; fixed bit encoding gives a constant factor, +not an emitted physical transition table or measured Python cost. The +source’s `O(ML)=O(V)` interpretation additionally needs `L=Theta(p)`, +`R=Theta(p)`, `V=MR` at the actual caller. + +## Evidence and reproduction + +Primary verification checks 145 produced stencils and exact setup bills, +including tight boundaries, zero inactive fields and a 500-bit stencil; +four unchanged-consumer compositions cover 5,760 addresses. Seven malformed +arithmetic/encoding cases reject with private/output cleanup. Actual producer +faults change parity/threshold semantics, omit cleanup or omit output return; +corrupt source bytes reject before execution. + +A code-disjoint oracle was frozen before inspecting the producer. It checks +83 geometries / 433,280 addresses and 360 larger boundary/parity/spectator +cases. `cross_check.py` feeds the paid producer’s output through the +unchanged scanner on every one of those 433,280 addresses, compares the +frozen mask hashes and both original CRT predicates, and executes three +semantic producer faults through the actual consumer. The separate cost +checker instruments primitive calls independently of the simulator bill; +its one-READ undercharge preserves final values/ownership but fails the +invoice. Receipts and exact review coverage accompany the code. + +```sh +python3.12 -B scripts/research_package.py --package research/crt-unary-stencil-producer --check-only +python3.12 -B scripts/research_package.py --package research/crt-unary-stencil-producer +python3.12 -B scripts/check_research_commit.py --package research/crt-unary-stencil-producer --check-source-history +``` + +The registered replay uses Python 3.12’s standard library, in ordinary and +strict optimized modes. Source pins include canonical CRT bytes and four +minimal unchanged PR4201 exports. Pending source exports are retained in +this PR’s own ancestor `5a41fea466cbeb7839bde864e563e191de47a0f7`; the original +source head remains `4f49743a9df0cf7501cdc62bd5707a122fa071e9`. + +## Scope, overlap and credit + +Handoff-first `uniform-transfer-audit`, refined to one encoded input +boundary; canonical base `12fa8c5c844be21bfefb38a19503fbd867a11244`, priority7. +[Canonical claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/4173#discussioncomment-19075225). +Initial live check covered 322 open/draft PR bodies and current #1166/#4173; +closed/code and broader Discussion coverage is partial. This replaces an +explicitly unpriced local input adapter, not the entire caller. The +family decision is **narrow**, with all other costs retained as unknown in +[TASK.json](TASK.json). + +Cinna Davis’s PR4100 supplies the original predicate and ordered-scan +proposal. Hiroki KUMAZAKI (`kumagi`), PR4169/4174, supplies repair/placement +context. PR4201 supplies the scanner, atom format and its proof; those are +predecessor work. Douglas Colkitt/OpenAI and the full retained CRT NOTICE +lineage keep credit. Prepared for ToikY with substantial OpenAI Codex +assistance, including separate producer/proof, pre-code oracle and cost +review contexts. Those checks are not independent human or formal-kernel +acceptance. Apache-2.0. No new κ, supplier admission, merge or selected-frontier +change is claimed. + +## Open next questions + +Structured questions, relevance, first steps and blockers are in +[TASK.json](TASK.json). The next missing input is a paid producer at the +actual binary/transported source boundary; before expanding, pin that caller +and its complete ownership/cost ledger. Many-target ordering/admission, +exception extraction, inverse keys, sorting, repair/reinsertion, ordinary +callees, full E arithmetic, precision, physical/native and outer composition +remain open. This predicate projection is not a full production reservoir +execution or multiplication theorem. diff --git a/research/crt-unary-stencil-producer/RESULT.json b/research/crt-unary-stencil-producer/RESULT.json new file mode 100644 index 0000000000..156a8ebb2b --- /dev/null +++ b/research/crt-unary-stencil-producer/RESULT.json @@ -0,0 +1,3113 @@ +{ + "authentication_controls": [ + { + "damaged_bytes_rejected_before_exec": true, + "source": "machine" + }, + { + "damaged_bytes_rejected_before_exec": true, + "source": "adapter" + } + ], + "cases": [ + { + "actions": 677, + "geometry_G_H_K_Y_J_B": [ + 1, + 1, + 5, + 5, + 0, + 0 + ], + "heads_returned": true, + "moves": 298, + "private_blank": true, + "protected_input": true, + "reads": 314, + "stencil_bits": 7, + "stencil_canonical_sha256": "969d4f6bd491483d33d2dce752bf3d931f53117a8a4ef8ed24b3fef11917d95c", + "visited_cells": 71, + "writes": 65 + }, + { + "actions": 689, + "geometry_G_H_K_Y_J_B": [ + 1, + 1, + 5, + 5, + 0, + 1 + ], + "heads_returned": true, + "moves": 304, + "private_blank": true, + "protected_input": true, + "reads": 319, + "stencil_bits": 8, + "stencil_canonical_sha256": "da6177bafbf7c08ea556360da356abfe9892de4625e4a8f492b71a6c0e448a2a", + "visited_cells": 73, + "writes": 66 + }, + { + "actions": 715, + "geometry_G_H_K_Y_J_B": [ + 1, + 1, + 5, + 6, + 0, + 0 + ], + "heads_returned": true, + "moves": 316, + "private_blank": true, + "protected_input": true, + "reads": 329, + "stencil_bits": 8, + "stencil_canonical_sha256": "6f80dd9571243b49ce9382c1f9fd633ce1c60a3e7d6217717df40e9b17fb24bf", + "visited_cells": 75, + "writes": 70 + }, + { + "actions": 727, + "geometry_G_H_K_Y_J_B": [ + 1, + 1, + 5, + 6, + 0, + 1 + ], + "heads_returned": true, + "moves": 322, + "private_blank": true, + "protected_input": true, + "reads": 334, + "stencil_bits": 9, + "stencil_canonical_sha256": "deb629d19877f8d5ca8d75168f1aaa6a80ee599119a6889824b2fb8b00b7412d", + "visited_cells": 77, + "writes": 71 + }, + { + "actions": 714, + "geometry_G_H_K_Y_J_B": [ + 1, + 1, + 5, + 6, + 1, + 0 + ], + "heads_returned": true, + "moves": 316, + "private_blank": true, + "protected_input": true, + "reads": 330, + "stencil_bits": 8, + "stencil_canonical_sha256": "da6177bafbf7c08ea556360da356abfe9892de4625e4a8f492b71a6c0e448a2a", + "visited_cells": 75, + "writes": 68 + }, + { + "actions": 726, + "geometry_G_H_K_Y_J_B": [ + 1, + 1, + 5, + 6, + 1, + 1 + ], + "heads_returned": true, + "moves": 322, + "private_blank": true, + "protected_input": true, + "reads": 335, + "stencil_bits": 9, + "stencil_canonical_sha256": "ecfe6056cc5ce80d597a254a5b58717e843fc05005e38dcb8fd8d70a9c6833c9", + "visited_cells": 77, + "writes": 69 + }, + { + "actions": 752, + "geometry_G_H_K_Y_J_B": [ + 1, + 1, + 5, + 7, + 1, + 0 + ], + "heads_returned": true, + "moves": 334, + "private_blank": true, + "protected_input": true, + "reads": 345, + "stencil_bits": 9, + "stencil_canonical_sha256": "deb629d19877f8d5ca8d75168f1aaa6a80ee599119a6889824b2fb8b00b7412d", + "visited_cells": 79, + "writes": 73 + }, + { + "actions": 764, + "geometry_G_H_K_Y_J_B": [ + 1, + 1, + 5, + 7, + 1, + 1 + ], + "heads_returned": true, + "moves": 340, + "private_blank": true, + "protected_input": true, + "reads": 350, + "stencil_bits": 10, + "stencil_canonical_sha256": "a628f51e02a91d721cac0627f50eea8eb9ed540d7be77fcb94f73ad6e191b361", + "visited_cells": 81, + "writes": 74 + }, + { + "actions": 751, + "geometry_G_H_K_Y_J_B": [ + 1, + 1, + 5, + 7, + 2, + 0 + ], + "heads_returned": true, + "moves": 334, + "private_blank": true, + "protected_input": true, + "reads": 346, + "stencil_bits": 9, + "stencil_canonical_sha256": "ecfe6056cc5ce80d597a254a5b58717e843fc05005e38dcb8fd8d70a9c6833c9", + "visited_cells": 79, + "writes": 71 + }, + { + "actions": 763, + "geometry_G_H_K_Y_J_B": [ + 1, + 1, + 5, + 7, + 2, + 1 + ], + "heads_returned": true, + "moves": 340, + "private_blank": true, + "protected_input": true, + "reads": 351, + "stencil_bits": 10, + "stencil_canonical_sha256": "c7e63ddd8132022f19c67e9d99fab37ba53ab19d95eacbcf22eb909e92870507", + "visited_cells": 81, + "writes": 72 + }, + { + "actions": 789, + "geometry_G_H_K_Y_J_B": [ + 1, + 1, + 5, + 8, + 2, + 0 + ], + "heads_returned": true, + "moves": 352, + "private_blank": true, + "protected_input": true, + "reads": 361, + "stencil_bits": 10, + "stencil_canonical_sha256": "a628f51e02a91d721cac0627f50eea8eb9ed540d7be77fcb94f73ad6e191b361", + "visited_cells": 83, + "writes": 76 + }, + { + "actions": 801, + "geometry_G_H_K_Y_J_B": [ + 1, + 1, + 5, + 8, + 2, + 1 + ], + "heads_returned": true, + "moves": 358, + "private_blank": true, + "protected_input": true, + "reads": 366, + "stencil_bits": 11, + "stencil_canonical_sha256": "ccd6ec8342ff9d4a4b716d3ad05965f28583254b3ddfe2748ccad3047a9f2902", + "visited_cells": 85, + "writes": 77 + }, + { + "actions": 740, + "geometry_G_H_K_Y_J_B": [ + 1, + 1, + 6, + 6, + 0, + 0 + ], + "heads_returned": true, + "moves": 328, + "private_blank": true, + "protected_input": true, + "reads": 340, + "stencil_bits": 8, + "stencil_canonical_sha256": "9466e27de84336306a1e34b4ed7d6926dfbe1d9a5cae3bc2426b6b55c8bc6e5d", + "visited_cells": 77, + "writes": 72 + }, + { + "actions": 752, + "geometry_G_H_K_Y_J_B": [ + 1, + 1, + 6, + 6, + 0, + 1 + ], + "heads_returned": true, + "moves": 334, + "private_blank": true, + "protected_input": true, + "reads": 345, + "stencil_bits": 9, + "stencil_canonical_sha256": "18ec557e0513477c9a2e5d8d3f570ff12487767534aa222011d98f81e132415f", + "visited_cells": 79, + "writes": 73 + }, + { + "actions": 778, + "geometry_G_H_K_Y_J_B": [ + 1, + 1, + 6, + 7, + 0, + 0 + ], + "heads_returned": true, + "moves": 346, + "private_blank": true, + "protected_input": true, + "reads": 355, + "stencil_bits": 9, + "stencil_canonical_sha256": "3f457c52018b62f8c8ebaf3cf321e94c0822f18ba31717d8ff9e9a27da2bf98c", + "visited_cells": 81, + "writes": 77 + }, + { + "actions": 790, + "geometry_G_H_K_Y_J_B": [ + 1, + 1, + 6, + 7, + 0, + 1 + ], + "heads_returned": true, + "moves": 352, + "private_blank": true, + "protected_input": true, + "reads": 360, + "stencil_bits": 10, + "stencil_canonical_sha256": "98b62f727f10705868b31c257a364fa72296e02b02910a674dbbb3f5fbe7ea08", + "visited_cells": 83, + "writes": 78 + }, + { + "actions": 777, + "geometry_G_H_K_Y_J_B": [ + 1, + 1, + 6, + 7, + 1, + 0 + ], + "heads_returned": true, + "moves": 346, + "private_blank": true, + "protected_input": true, + "reads": 356, + "stencil_bits": 9, + "stencil_canonical_sha256": "18ec557e0513477c9a2e5d8d3f570ff12487767534aa222011d98f81e132415f", + "visited_cells": 81, + "writes": 75 + }, + { + "actions": 789, + "geometry_G_H_K_Y_J_B": [ + 1, + 1, + 6, + 7, + 1, + 1 + ], + "heads_returned": true, + "moves": 352, + "private_blank": true, + "protected_input": true, + "reads": 361, + "stencil_bits": 10, + "stencil_canonical_sha256": "20a0eb3b18aaea88346d664c6ac60769f162f5e8b04c1e19595f56f3514d3d70", + "visited_cells": 83, + "writes": 76 + }, + { + "actions": 815, + "geometry_G_H_K_Y_J_B": [ + 1, + 1, + 6, + 8, + 1, + 0 + ], + "heads_returned": true, + "moves": 364, + "private_blank": true, + "protected_input": true, + "reads": 371, + "stencil_bits": 10, + "stencil_canonical_sha256": "98b62f727f10705868b31c257a364fa72296e02b02910a674dbbb3f5fbe7ea08", + "visited_cells": 85, + "writes": 80 + }, + { + "actions": 827, + "geometry_G_H_K_Y_J_B": [ + 1, + 1, + 6, + 8, + 1, + 1 + ], + "heads_returned": true, + "moves": 370, + "private_blank": true, + "protected_input": true, + "reads": 376, + "stencil_bits": 11, + "stencil_canonical_sha256": "cce70f8cc3c88835abebdeb2452cd0193627e4178ea830833ec723b12f0d94d2", + "visited_cells": 87, + "writes": 81 + }, + { + "actions": 814, + "geometry_G_H_K_Y_J_B": [ + 1, + 1, + 6, + 8, + 2, + 0 + ], + "heads_returned": true, + "moves": 364, + "private_blank": true, + "protected_input": true, + "reads": 372, + "stencil_bits": 10, + "stencil_canonical_sha256": "20a0eb3b18aaea88346d664c6ac60769f162f5e8b04c1e19595f56f3514d3d70", + "visited_cells": 85, + "writes": 78 + }, + { + "actions": 826, + "geometry_G_H_K_Y_J_B": [ + 1, + 1, + 6, + 8, + 2, + 1 + ], + "heads_returned": true, + "moves": 370, + "private_blank": true, + "protected_input": true, + "reads": 377, + "stencil_bits": 11, + "stencil_canonical_sha256": "5838caa723ba3617ee100bcb2e6468d859259791a4080203eeb7e27e5883cd39", + "visited_cells": 87, + "writes": 79 + }, + { + "actions": 852, + "geometry_G_H_K_Y_J_B": [ + 1, + 1, + 6, + 9, + 2, + 0 + ], + "heads_returned": true, + "moves": 382, + "private_blank": true, + "protected_input": true, + "reads": 387, + "stencil_bits": 11, + "stencil_canonical_sha256": "cce70f8cc3c88835abebdeb2452cd0193627e4178ea830833ec723b12f0d94d2", + "visited_cells": 89, + "writes": 83 + }, + { + "actions": 864, + "geometry_G_H_K_Y_J_B": [ + 1, + 1, + 6, + 9, + 2, + 1 + ], + "heads_returned": true, + "moves": 388, + "private_blank": true, + "protected_input": true, + "reads": 392, + "stencil_bits": 12, + "stencil_canonical_sha256": "bbd46485d4ea7f29f797f103a9b970cbb70b0661fae0a4c655012d4b512de590", + "visited_cells": 91, + "writes": 84 + }, + { + "actions": 710, + "geometry_G_H_K_Y_J_B": [ + 1, + 2, + 5, + 5, + 0, + 0 + ], + "heads_returned": true, + "moves": 314, + "private_blank": true, + "protected_input": true, + "reads": 327, + "stencil_bits": 9, + "stencil_canonical_sha256": "143b7541171bc48318d5633f29815c4dc3064fc19e1ec1b8e9e150df780764d8", + "visited_cells": 75, + "writes": 69 + }, + { + "actions": 722, + "geometry_G_H_K_Y_J_B": [ + 1, + 2, + 5, + 5, + 0, + 1 + ], + "heads_returned": true, + "moves": 320, + "private_blank": true, + "protected_input": true, + "reads": 332, + "stencil_bits": 10, + "stencil_canonical_sha256": "c74fc22a37add28ab9ea8cb6f5f8458b63ace97fff4671aa09ac6e333db3bfce", + "visited_cells": 77, + "writes": 70 + }, + { + "actions": 748, + "geometry_G_H_K_Y_J_B": [ + 1, + 2, + 5, + 6, + 0, + 0 + ], + "heads_returned": true, + "moves": 332, + "private_blank": true, + "protected_input": true, + "reads": 342, + "stencil_bits": 10, + "stencil_canonical_sha256": "f7fdacfd02a774bb86c7ad3857d484fa1fdcd7bf38c0010c055cadc0c765ee07", + "visited_cells": 79, + "writes": 74 + }, + { + "actions": 760, + "geometry_G_H_K_Y_J_B": [ + 1, + 2, + 5, + 6, + 0, + 1 + ], + "heads_returned": true, + "moves": 338, + "private_blank": true, + "protected_input": true, + "reads": 347, + "stencil_bits": 11, + "stencil_canonical_sha256": "af719f9ba451aa3bbcf486ce5a62c6b3289be9b947edc2aadce1f13732f46f8e", + "visited_cells": 81, + "writes": 75 + }, + { + "actions": 747, + "geometry_G_H_K_Y_J_B": [ + 1, + 2, + 5, + 6, + 1, + 0 + ], + "heads_returned": true, + "moves": 332, + "private_blank": true, + "protected_input": true, + "reads": 343, + "stencil_bits": 10, + "stencil_canonical_sha256": "c74fc22a37add28ab9ea8cb6f5f8458b63ace97fff4671aa09ac6e333db3bfce", + "visited_cells": 79, + "writes": 72 + }, + { + "actions": 759, + "geometry_G_H_K_Y_J_B": [ + 1, + 2, + 5, + 6, + 1, + 1 + ], + "heads_returned": true, + "moves": 338, + "private_blank": true, + "protected_input": true, + "reads": 348, + "stencil_bits": 11, + "stencil_canonical_sha256": "017ebcb7dc5993950a76f28a705c51851f75a65bd0bf8cd52dbc16f3e1be1d8d", + "visited_cells": 81, + "writes": 73 + }, + { + "actions": 785, + "geometry_G_H_K_Y_J_B": [ + 1, + 2, + 5, + 7, + 1, + 0 + ], + "heads_returned": true, + "moves": 350, + "private_blank": true, + "protected_input": true, + "reads": 358, + "stencil_bits": 11, + "stencil_canonical_sha256": "af719f9ba451aa3bbcf486ce5a62c6b3289be9b947edc2aadce1f13732f46f8e", + "visited_cells": 83, + "writes": 77 + }, + { + "actions": 797, + "geometry_G_H_K_Y_J_B": [ + 1, + 2, + 5, + 7, + 1, + 1 + ], + "heads_returned": true, + "moves": 356, + "private_blank": true, + "protected_input": true, + "reads": 363, + "stencil_bits": 12, + "stencil_canonical_sha256": "bbe6b155152ee6249cdd709358d324325870fb6444f0d78a76faf5b04781354b", + "visited_cells": 85, + "writes": 78 + }, + { + "actions": 784, + "geometry_G_H_K_Y_J_B": [ + 1, + 2, + 5, + 7, + 2, + 0 + ], + "heads_returned": true, + "moves": 350, + "private_blank": true, + "protected_input": true, + "reads": 359, + "stencil_bits": 11, + "stencil_canonical_sha256": "017ebcb7dc5993950a76f28a705c51851f75a65bd0bf8cd52dbc16f3e1be1d8d", + "visited_cells": 83, + "writes": 75 + }, + { + "actions": 796, + "geometry_G_H_K_Y_J_B": [ + 1, + 2, + 5, + 7, + 2, + 1 + ], + "heads_returned": true, + "moves": 356, + "private_blank": true, + "protected_input": true, + "reads": 364, + "stencil_bits": 12, + "stencil_canonical_sha256": "136800919c65ba8990c172d00fa9d36ea13727e0414ccf06448abe41f7ef5443", + "visited_cells": 85, + "writes": 76 + }, + { + "actions": 822, + "geometry_G_H_K_Y_J_B": [ + 1, + 2, + 5, + 8, + 2, + 0 + ], + "heads_returned": true, + "moves": 368, + "private_blank": true, + "protected_input": true, + "reads": 374, + "stencil_bits": 12, + "stencil_canonical_sha256": "bbe6b155152ee6249cdd709358d324325870fb6444f0d78a76faf5b04781354b", + "visited_cells": 87, + "writes": 80 + }, + { + "actions": 834, + "geometry_G_H_K_Y_J_B": [ + 1, + 2, + 5, + 8, + 2, + 1 + ], + "heads_returned": true, + "moves": 374, + "private_blank": true, + "protected_input": true, + "reads": 379, + "stencil_bits": 13, + "stencil_canonical_sha256": "a0d1b563d75c937c6836b6b3d5c32743cc6d06704c84621bd399dfd6b8524ca3", + "visited_cells": 89, + "writes": 81 + }, + { + "actions": 773, + "geometry_G_H_K_Y_J_B": [ + 1, + 2, + 6, + 6, + 0, + 0 + ], + "heads_returned": true, + "moves": 344, + "private_blank": true, + "protected_input": true, + "reads": 353, + "stencil_bits": 10, + "stencil_canonical_sha256": "dfba89ebf291f1d38e0f24fb0d8e79525f4f67604421ee87922da3dd5fc24ddc", + "visited_cells": 81, + "writes": 76 + }, + { + "actions": 785, + "geometry_G_H_K_Y_J_B": [ + 1, + 2, + 6, + 6, + 0, + 1 + ], + "heads_returned": true, + "moves": 350, + "private_blank": true, + "protected_input": true, + "reads": 358, + "stencil_bits": 11, + "stencil_canonical_sha256": "c2689b74612923c638f1a7ca1f5fbe48f29fddce678e3241d344099d1bc93e46", + "visited_cells": 83, + "writes": 77 + }, + { + "actions": 811, + "geometry_G_H_K_Y_J_B": [ + 1, + 2, + 6, + 7, + 0, + 0 + ], + "heads_returned": true, + "moves": 362, + "private_blank": true, + "protected_input": true, + "reads": 368, + "stencil_bits": 11, + "stencil_canonical_sha256": "e14bc444cadce0022eddb6f327ce29d19ba6f3a6c9072f5a307c8fe2c70f3284", + "visited_cells": 85, + "writes": 81 + }, + { + "actions": 823, + "geometry_G_H_K_Y_J_B": [ + 1, + 2, + 6, + 7, + 0, + 1 + ], + "heads_returned": true, + "moves": 368, + "private_blank": true, + "protected_input": true, + "reads": 373, + "stencil_bits": 12, + "stencil_canonical_sha256": "5ebe4484a92e88a8c6fab7372c210557b7455b0979d276be219e4552f49082c1", + "visited_cells": 87, + "writes": 82 + }, + { + "actions": 810, + "geometry_G_H_K_Y_J_B": [ + 1, + 2, + 6, + 7, + 1, + 0 + ], + "heads_returned": true, + "moves": 362, + "private_blank": true, + "protected_input": true, + "reads": 369, + "stencil_bits": 11, + "stencil_canonical_sha256": "c2689b74612923c638f1a7ca1f5fbe48f29fddce678e3241d344099d1bc93e46", + "visited_cells": 85, + "writes": 79 + }, + { + "actions": 822, + "geometry_G_H_K_Y_J_B": [ + 1, + 2, + 6, + 7, + 1, + 1 + ], + "heads_returned": true, + "moves": 368, + "private_blank": true, + "protected_input": true, + "reads": 374, + "stencil_bits": 12, + "stencil_canonical_sha256": "3f07b3e5aba566732bac3bed268f66fa335bd49ebc90b98135f91397efa03f31", + "visited_cells": 87, + "writes": 80 + }, + { + "actions": 848, + "geometry_G_H_K_Y_J_B": [ + 1, + 2, + 6, + 8, + 1, + 0 + ], + "heads_returned": true, + "moves": 380, + "private_blank": true, + "protected_input": true, + "reads": 384, + "stencil_bits": 12, + "stencil_canonical_sha256": "5ebe4484a92e88a8c6fab7372c210557b7455b0979d276be219e4552f49082c1", + "visited_cells": 89, + "writes": 84 + }, + { + "actions": 860, + "geometry_G_H_K_Y_J_B": [ + 1, + 2, + 6, + 8, + 1, + 1 + ], + "heads_returned": true, + "moves": 386, + "private_blank": true, + "protected_input": true, + "reads": 389, + "stencil_bits": 13, + "stencil_canonical_sha256": "8f1219131d174c1c704bc9cc0b0d68a3b39cd08a2d36461200280f14570d3a57", + "visited_cells": 91, + "writes": 85 + }, + { + "actions": 847, + "geometry_G_H_K_Y_J_B": [ + 1, + 2, + 6, + 8, + 2, + 0 + ], + "heads_returned": true, + "moves": 380, + "private_blank": true, + "protected_input": true, + "reads": 385, + "stencil_bits": 12, + "stencil_canonical_sha256": "3f07b3e5aba566732bac3bed268f66fa335bd49ebc90b98135f91397efa03f31", + "visited_cells": 89, + "writes": 82 + }, + { + "actions": 859, + "geometry_G_H_K_Y_J_B": [ + 1, + 2, + 6, + 8, + 2, + 1 + ], + "heads_returned": true, + "moves": 386, + "private_blank": true, + "protected_input": true, + "reads": 390, + "stencil_bits": 13, + "stencil_canonical_sha256": "86c7de106927c73f7e8686cab55dfa455450b51a165651c94074f8c4e0b94e78", + "visited_cells": 91, + "writes": 83 + }, + { + "actions": 885, + "geometry_G_H_K_Y_J_B": [ + 1, + 2, + 6, + 9, + 2, + 0 + ], + "heads_returned": true, + "moves": 398, + "private_blank": true, + "protected_input": true, + "reads": 400, + "stencil_bits": 13, + "stencil_canonical_sha256": "8f1219131d174c1c704bc9cc0b0d68a3b39cd08a2d36461200280f14570d3a57", + "visited_cells": 93, + "writes": 87 + }, + { + "actions": 897, + "geometry_G_H_K_Y_J_B": [ + 1, + 2, + 6, + 9, + 2, + 1 + ], + "heads_returned": true, + "moves": 404, + "private_blank": true, + "protected_input": true, + "reads": 405, + "stencil_bits": 14, + "stencil_canonical_sha256": "749ba73cc114799164de8f572c41f98497ba1ff9c3754c84ffd7b2c8cafa06e7", + "visited_cells": 95, + "writes": 88 + }, + { + "actions": 767, + "geometry_G_H_K_Y_J_B": [ + 2, + 2, + 6, + 6, + 0, + 0 + ], + "heads_returned": true, + "moves": 342, + "private_blank": true, + "protected_input": true, + "reads": 353, + "stencil_bits": 10, + "stencil_canonical_sha256": "b05d6a624df6a08d4bd9c4961180a8b5570329b9255b8c01f2fe3aedd187d0eb", + "visited_cells": 80, + "writes": 72 + }, + { + "actions": 779, + "geometry_G_H_K_Y_J_B": [ + 2, + 2, + 6, + 6, + 0, + 1 + ], + "heads_returned": true, + "moves": 348, + "private_blank": true, + "protected_input": true, + "reads": 358, + "stencil_bits": 11, + "stencil_canonical_sha256": "5d1ff1aa1c0795e962f936cd2406250b8bfe4cb969e25cbd9ac98a61cfe5133a", + "visited_cells": 82, + "writes": 73 + }, + { + "actions": 805, + "geometry_G_H_K_Y_J_B": [ + 2, + 2, + 6, + 7, + 0, + 0 + ], + "heads_returned": true, + "moves": 360, + "private_blank": true, + "protected_input": true, + "reads": 368, + "stencil_bits": 11, + "stencil_canonical_sha256": "9eff808d64cfe1a78242d033bbff14de7201a6025f34652c70f058ca741a33bb", + "visited_cells": 84, + "writes": 77 + }, + { + "actions": 817, + "geometry_G_H_K_Y_J_B": [ + 2, + 2, + 6, + 7, + 0, + 1 + ], + "heads_returned": true, + "moves": 366, + "private_blank": true, + "protected_input": true, + "reads": 373, + "stencil_bits": 12, + "stencil_canonical_sha256": "0691294289c26cd2a13815ef9445bdd970c6935e3a43fdd830cde47cb8f80a01", + "visited_cells": 86, + "writes": 78 + }, + { + "actions": 804, + "geometry_G_H_K_Y_J_B": [ + 2, + 2, + 6, + 7, + 1, + 0 + ], + "heads_returned": true, + "moves": 360, + "private_blank": true, + "protected_input": true, + "reads": 369, + "stencil_bits": 11, + "stencil_canonical_sha256": "5d1ff1aa1c0795e962f936cd2406250b8bfe4cb969e25cbd9ac98a61cfe5133a", + "visited_cells": 84, + "writes": 75 + }, + { + "actions": 816, + "geometry_G_H_K_Y_J_B": [ + 2, + 2, + 6, + 7, + 1, + 1 + ], + "heads_returned": true, + "moves": 366, + "private_blank": true, + "protected_input": true, + "reads": 374, + "stencil_bits": 12, + "stencil_canonical_sha256": "c741e63c0500f0f13263a3e064a7233d162adc116c5a22d313c102c67454e868", + "visited_cells": 86, + "writes": 76 + }, + { + "actions": 842, + "geometry_G_H_K_Y_J_B": [ + 2, + 2, + 6, + 8, + 1, + 0 + ], + "heads_returned": true, + "moves": 378, + "private_blank": true, + "protected_input": true, + "reads": 384, + "stencil_bits": 12, + "stencil_canonical_sha256": "0691294289c26cd2a13815ef9445bdd970c6935e3a43fdd830cde47cb8f80a01", + "visited_cells": 88, + "writes": 80 + }, + { + "actions": 854, + "geometry_G_H_K_Y_J_B": [ + 2, + 2, + 6, + 8, + 1, + 1 + ], + "heads_returned": true, + "moves": 384, + "private_blank": true, + "protected_input": true, + "reads": 389, + "stencil_bits": 13, + "stencil_canonical_sha256": "742369b87a553fc0a14e417f0e9056c1eef4cd109d6dee2cbdd51e86dbf8a236", + "visited_cells": 90, + "writes": 81 + }, + { + "actions": 841, + "geometry_G_H_K_Y_J_B": [ + 2, + 2, + 6, + 8, + 2, + 0 + ], + "heads_returned": true, + "moves": 378, + "private_blank": true, + "protected_input": true, + "reads": 385, + "stencil_bits": 12, + "stencil_canonical_sha256": "c741e63c0500f0f13263a3e064a7233d162adc116c5a22d313c102c67454e868", + "visited_cells": 88, + "writes": 78 + }, + { + "actions": 853, + "geometry_G_H_K_Y_J_B": [ + 2, + 2, + 6, + 8, + 2, + 1 + ], + "heads_returned": true, + "moves": 384, + "private_blank": true, + "protected_input": true, + "reads": 390, + "stencil_bits": 13, + "stencil_canonical_sha256": "83c5339bb47944373466adc60c3262faa6d5b0a5116ea70898da1ab2c612d12f", + "visited_cells": 90, + "writes": 79 + }, + { + "actions": 879, + "geometry_G_H_K_Y_J_B": [ + 2, + 2, + 6, + 9, + 2, + 0 + ], + "heads_returned": true, + "moves": 396, + "private_blank": true, + "protected_input": true, + "reads": 400, + "stencil_bits": 13, + "stencil_canonical_sha256": "742369b87a553fc0a14e417f0e9056c1eef4cd109d6dee2cbdd51e86dbf8a236", + "visited_cells": 92, + "writes": 83 + }, + { + "actions": 891, + "geometry_G_H_K_Y_J_B": [ + 2, + 2, + 6, + 9, + 2, + 1 + ], + "heads_returned": true, + "moves": 402, + "private_blank": true, + "protected_input": true, + "reads": 405, + "stencil_bits": 14, + "stencil_canonical_sha256": "db5e01921f6c7634bf97860e9031dc619aff6b5c5e97baca3464f6948a0ff54f", + "visited_cells": 94, + "writes": 84 + }, + { + "actions": 830, + "geometry_G_H_K_Y_J_B": [ + 2, + 2, + 7, + 7, + 0, + 0 + ], + "heads_returned": true, + "moves": 372, + "private_blank": true, + "protected_input": true, + "reads": 379, + "stencil_bits": 11, + "stencil_canonical_sha256": "06ae04feb7260784ee79fe2919ea020bb40c0bbea459e37c0da9d3f8011c46c6", + "visited_cells": 86, + "writes": 79 + }, + { + "actions": 842, + "geometry_G_H_K_Y_J_B": [ + 2, + 2, + 7, + 7, + 0, + 1 + ], + "heads_returned": true, + "moves": 378, + "private_blank": true, + "protected_input": true, + "reads": 384, + "stencil_bits": 12, + "stencil_canonical_sha256": "ffc029dc55587e5c54ce8ee5b4ae61ffb867240a363adcf1abd2dbae1a14279e", + "visited_cells": 88, + "writes": 80 + }, + { + "actions": 868, + "geometry_G_H_K_Y_J_B": [ + 2, + 2, + 7, + 8, + 0, + 0 + ], + "heads_returned": true, + "moves": 390, + "private_blank": true, + "protected_input": true, + "reads": 394, + "stencil_bits": 12, + "stencil_canonical_sha256": "082f8bc8f0edc5c2ccb7cdeea2d8e10ffada66090bb4cccee4aa75ce39c0b4f2", + "visited_cells": 90, + "writes": 84 + }, + { + "actions": 880, + "geometry_G_H_K_Y_J_B": [ + 2, + 2, + 7, + 8, + 0, + 1 + ], + "heads_returned": true, + "moves": 396, + "private_blank": true, + "protected_input": true, + "reads": 399, + "stencil_bits": 13, + "stencil_canonical_sha256": "90e9f75fa2b62c4aa455892ae4f8997d8ef242b450da353d8adbef789b9ed8f8", + "visited_cells": 92, + "writes": 85 + }, + { + "actions": 867, + "geometry_G_H_K_Y_J_B": [ + 2, + 2, + 7, + 8, + 1, + 0 + ], + "heads_returned": true, + "moves": 390, + "private_blank": true, + "protected_input": true, + "reads": 395, + "stencil_bits": 12, + "stencil_canonical_sha256": "ffc029dc55587e5c54ce8ee5b4ae61ffb867240a363adcf1abd2dbae1a14279e", + "visited_cells": 90, + "writes": 82 + }, + { + "actions": 879, + "geometry_G_H_K_Y_J_B": [ + 2, + 2, + 7, + 8, + 1, + 1 + ], + "heads_returned": true, + "moves": 396, + "private_blank": true, + "protected_input": true, + "reads": 400, + "stencil_bits": 13, + "stencil_canonical_sha256": "b67fcef74197fb8a5749e7e78960bb2709d284d0ee77ca776b418eb70bc78175", + "visited_cells": 92, + "writes": 83 + }, + { + "actions": 905, + "geometry_G_H_K_Y_J_B": [ + 2, + 2, + 7, + 9, + 1, + 0 + ], + "heads_returned": true, + "moves": 408, + "private_blank": true, + "protected_input": true, + "reads": 410, + "stencil_bits": 13, + "stencil_canonical_sha256": "90e9f75fa2b62c4aa455892ae4f8997d8ef242b450da353d8adbef789b9ed8f8", + "visited_cells": 94, + "writes": 87 + }, + { + "actions": 917, + "geometry_G_H_K_Y_J_B": [ + 2, + 2, + 7, + 9, + 1, + 1 + ], + "heads_returned": true, + "moves": 414, + "private_blank": true, + "protected_input": true, + "reads": 415, + "stencil_bits": 14, + "stencil_canonical_sha256": "b5a7df2c81385ff50ef0cf3db277019e6e57f9414c8a9dd2d5a22484b6caa81e", + "visited_cells": 96, + "writes": 88 + }, + { + "actions": 904, + "geometry_G_H_K_Y_J_B": [ + 2, + 2, + 7, + 9, + 2, + 0 + ], + "heads_returned": true, + "moves": 408, + "private_blank": true, + "protected_input": true, + "reads": 411, + "stencil_bits": 13, + "stencil_canonical_sha256": "b67fcef74197fb8a5749e7e78960bb2709d284d0ee77ca776b418eb70bc78175", + "visited_cells": 94, + "writes": 85 + }, + { + "actions": 916, + "geometry_G_H_K_Y_J_B": [ + 2, + 2, + 7, + 9, + 2, + 1 + ], + "heads_returned": true, + "moves": 414, + "private_blank": true, + "protected_input": true, + "reads": 416, + "stencil_bits": 14, + "stencil_canonical_sha256": "de4ccdb52481cebadb664e15e01b07ea105025207cf65c94c2772d30be290824", + "visited_cells": 96, + "writes": 86 + }, + { + "actions": 942, + "geometry_G_H_K_Y_J_B": [ + 2, + 2, + 7, + 10, + 2, + 0 + ], + "heads_returned": true, + "moves": 426, + "private_blank": true, + "protected_input": true, + "reads": 426, + "stencil_bits": 14, + "stencil_canonical_sha256": "b5a7df2c81385ff50ef0cf3db277019e6e57f9414c8a9dd2d5a22484b6caa81e", + "visited_cells": 98, + "writes": 90 + }, + { + "actions": 954, + "geometry_G_H_K_Y_J_B": [ + 2, + 2, + 7, + 10, + 2, + 1 + ], + "heads_returned": true, + "moves": 432, + "private_blank": true, + "protected_input": true, + "reads": 431, + "stencil_bits": 15, + "stencil_canonical_sha256": "cbe1235a184af03b47072dfc682f41af06528d4d7f8556ffc06d8727fec90200", + "visited_cells": 100, + "writes": 91 + }, + { + "actions": 800, + "geometry_G_H_K_Y_J_B": [ + 2, + 3, + 6, + 6, + 0, + 0 + ], + "heads_returned": true, + "moves": 358, + "private_blank": true, + "protected_input": true, + "reads": 366, + "stencil_bits": 12, + "stencil_canonical_sha256": "d357e81ef7c58c9bab5e5aaaea3c591469a4d1aa5f6a9a6bf52d7f0178c785ca", + "visited_cells": 84, + "writes": 76 + }, + { + "actions": 812, + "geometry_G_H_K_Y_J_B": [ + 2, + 3, + 6, + 6, + 0, + 1 + ], + "heads_returned": true, + "moves": 364, + "private_blank": true, + "protected_input": true, + "reads": 371, + "stencil_bits": 13, + "stencil_canonical_sha256": "12a7f93805fb5ad6565a476e08953215c947c5cb3e1dd71118fb7917fab6c4bd", + "visited_cells": 86, + "writes": 77 + }, + { + "actions": 838, + "geometry_G_H_K_Y_J_B": [ + 2, + 3, + 6, + 7, + 0, + 0 + ], + "heads_returned": true, + "moves": 376, + "private_blank": true, + "protected_input": true, + "reads": 381, + "stencil_bits": 13, + "stencil_canonical_sha256": "34dbb714ea75b77fd724f0425292ccbcb16435abfbc4627e84126f57fc2b2f4b", + "visited_cells": 88, + "writes": 81 + }, + { + "actions": 850, + "geometry_G_H_K_Y_J_B": [ + 2, + 3, + 6, + 7, + 0, + 1 + ], + "heads_returned": true, + "moves": 382, + "private_blank": true, + "protected_input": true, + "reads": 386, + "stencil_bits": 14, + "stencil_canonical_sha256": "0376877011bfb0f87888db5b21057d2add6953f00efc107bb85ddda74647e18a", + "visited_cells": 90, + "writes": 82 + }, + { + "actions": 837, + "geometry_G_H_K_Y_J_B": [ + 2, + 3, + 6, + 7, + 1, + 0 + ], + "heads_returned": true, + "moves": 376, + "private_blank": true, + "protected_input": true, + "reads": 382, + "stencil_bits": 13, + "stencil_canonical_sha256": "12a7f93805fb5ad6565a476e08953215c947c5cb3e1dd71118fb7917fab6c4bd", + "visited_cells": 88, + "writes": 79 + }, + { + "actions": 849, + "geometry_G_H_K_Y_J_B": [ + 2, + 3, + 6, + 7, + 1, + 1 + ], + "heads_returned": true, + "moves": 382, + "private_blank": true, + "protected_input": true, + "reads": 387, + "stencil_bits": 14, + "stencil_canonical_sha256": "d9542a0be883be39f4dac402c69182461fa51584f196b24380de2cb9b05968ee", + "visited_cells": 90, + "writes": 80 + }, + { + "actions": 875, + "geometry_G_H_K_Y_J_B": [ + 2, + 3, + 6, + 8, + 1, + 0 + ], + "heads_returned": true, + "moves": 394, + "private_blank": true, + "protected_input": true, + "reads": 397, + "stencil_bits": 14, + "stencil_canonical_sha256": "0376877011bfb0f87888db5b21057d2add6953f00efc107bb85ddda74647e18a", + "visited_cells": 92, + "writes": 84 + }, + { + "actions": 887, + "geometry_G_H_K_Y_J_B": [ + 2, + 3, + 6, + 8, + 1, + 1 + ], + "heads_returned": true, + "moves": 400, + "private_blank": true, + "protected_input": true, + "reads": 402, + "stencil_bits": 15, + "stencil_canonical_sha256": "ec9ff0c376127a928a7b2ade8cbdec3993b2c3053e734959713b2df15c0f31ce", + "visited_cells": 94, + "writes": 85 + }, + { + "actions": 874, + "geometry_G_H_K_Y_J_B": [ + 2, + 3, + 6, + 8, + 2, + 0 + ], + "heads_returned": true, + "moves": 394, + "private_blank": true, + "protected_input": true, + "reads": 398, + "stencil_bits": 14, + "stencil_canonical_sha256": "d9542a0be883be39f4dac402c69182461fa51584f196b24380de2cb9b05968ee", + "visited_cells": 92, + "writes": 82 + }, + { + "actions": 886, + "geometry_G_H_K_Y_J_B": [ + 2, + 3, + 6, + 8, + 2, + 1 + ], + "heads_returned": true, + "moves": 400, + "private_blank": true, + "protected_input": true, + "reads": 403, + "stencil_bits": 15, + "stencil_canonical_sha256": "e74e425d957a0b24249cc1e21570d97caf57a434451f8fadfb3e4d7776df76b8", + "visited_cells": 94, + "writes": 83 + }, + { + "actions": 912, + "geometry_G_H_K_Y_J_B": [ + 2, + 3, + 6, + 9, + 2, + 0 + ], + "heads_returned": true, + "moves": 412, + "private_blank": true, + "protected_input": true, + "reads": 413, + "stencil_bits": 15, + "stencil_canonical_sha256": "ec9ff0c376127a928a7b2ade8cbdec3993b2c3053e734959713b2df15c0f31ce", + "visited_cells": 96, + "writes": 87 + }, + { + "actions": 924, + "geometry_G_H_K_Y_J_B": [ + 2, + 3, + 6, + 9, + 2, + 1 + ], + "heads_returned": true, + "moves": 418, + "private_blank": true, + "protected_input": true, + "reads": 418, + "stencil_bits": 16, + "stencil_canonical_sha256": "ce607e53f3b476943ea4d929da586fcd30dd10b6ee2599a0da8901cbc76ffd53", + "visited_cells": 98, + "writes": 88 + }, + { + "actions": 863, + "geometry_G_H_K_Y_J_B": [ + 2, + 3, + 7, + 7, + 0, + 0 + ], + "heads_returned": true, + "moves": 388, + "private_blank": true, + "protected_input": true, + "reads": 392, + "stencil_bits": 13, + "stencil_canonical_sha256": "069aae5a5a88757169df7f868c7bb5e33cde81b723b3f7d181296a34bf10c15b", + "visited_cells": 90, + "writes": 83 + }, + { + "actions": 875, + "geometry_G_H_K_Y_J_B": [ + 2, + 3, + 7, + 7, + 0, + 1 + ], + "heads_returned": true, + "moves": 394, + "private_blank": true, + "protected_input": true, + "reads": 397, + "stencil_bits": 14, + "stencil_canonical_sha256": "8dd5f32b5ed88689fc1da421f8c08b7dea32d9f52fdc324c7020f8f5b210c1f6", + "visited_cells": 92, + "writes": 84 + }, + { + "actions": 901, + "geometry_G_H_K_Y_J_B": [ + 2, + 3, + 7, + 8, + 0, + 0 + ], + "heads_returned": true, + "moves": 406, + "private_blank": true, + "protected_input": true, + "reads": 407, + "stencil_bits": 14, + "stencil_canonical_sha256": "aa6846355d908347fdd7868636cb932eaffc6d65d583090183f7b92b4227c224", + "visited_cells": 94, + "writes": 88 + }, + { + "actions": 913, + "geometry_G_H_K_Y_J_B": [ + 2, + 3, + 7, + 8, + 0, + 1 + ], + "heads_returned": true, + "moves": 412, + "private_blank": true, + "protected_input": true, + "reads": 412, + "stencil_bits": 15, + "stencil_canonical_sha256": "58553575dfbe39557fa8da50df03e8e04ecfd39086af14bb95d6413ebb8740e3", + "visited_cells": 96, + "writes": 89 + }, + { + "actions": 900, + "geometry_G_H_K_Y_J_B": [ + 2, + 3, + 7, + 8, + 1, + 0 + ], + "heads_returned": true, + "moves": 406, + "private_blank": true, + "protected_input": true, + "reads": 408, + "stencil_bits": 14, + "stencil_canonical_sha256": "8dd5f32b5ed88689fc1da421f8c08b7dea32d9f52fdc324c7020f8f5b210c1f6", + "visited_cells": 94, + "writes": 86 + }, + { + "actions": 912, + "geometry_G_H_K_Y_J_B": [ + 2, + 3, + 7, + 8, + 1, + 1 + ], + "heads_returned": true, + "moves": 412, + "private_blank": true, + "protected_input": true, + "reads": 413, + "stencil_bits": 15, + "stencil_canonical_sha256": "38de7a44bc1eb8b9fa3a4889788abfc94050f62f42ecaffb4a821024e91d1972", + "visited_cells": 96, + "writes": 87 + }, + { + "actions": 938, + "geometry_G_H_K_Y_J_B": [ + 2, + 3, + 7, + 9, + 1, + 0 + ], + "heads_returned": true, + "moves": 424, + "private_blank": true, + "protected_input": true, + "reads": 423, + "stencil_bits": 15, + "stencil_canonical_sha256": "58553575dfbe39557fa8da50df03e8e04ecfd39086af14bb95d6413ebb8740e3", + "visited_cells": 98, + "writes": 91 + }, + { + "actions": 950, + "geometry_G_H_K_Y_J_B": [ + 2, + 3, + 7, + 9, + 1, + 1 + ], + "heads_returned": true, + "moves": 430, + "private_blank": true, + "protected_input": true, + "reads": 428, + "stencil_bits": 16, + "stencil_canonical_sha256": "06201c7a68ea9fcf93935572763c11fed09431de66e6fb24789990313eeaec54", + "visited_cells": 100, + "writes": 92 + }, + { + "actions": 937, + "geometry_G_H_K_Y_J_B": [ + 2, + 3, + 7, + 9, + 2, + 0 + ], + "heads_returned": true, + "moves": 424, + "private_blank": true, + "protected_input": true, + "reads": 424, + "stencil_bits": 15, + "stencil_canonical_sha256": "38de7a44bc1eb8b9fa3a4889788abfc94050f62f42ecaffb4a821024e91d1972", + "visited_cells": 98, + "writes": 89 + }, + { + "actions": 949, + "geometry_G_H_K_Y_J_B": [ + 2, + 3, + 7, + 9, + 2, + 1 + ], + "heads_returned": true, + "moves": 430, + "private_blank": true, + "protected_input": true, + "reads": 429, + "stencil_bits": 16, + "stencil_canonical_sha256": "421d4e71c75f3049d53eb36e3ba25558c279a4569235929830b4ceb2f4ef064c", + "visited_cells": 100, + "writes": 90 + }, + { + "actions": 975, + "geometry_G_H_K_Y_J_B": [ + 2, + 3, + 7, + 10, + 2, + 0 + ], + "heads_returned": true, + "moves": 442, + "private_blank": true, + "protected_input": true, + "reads": 439, + "stencil_bits": 16, + "stencil_canonical_sha256": "06201c7a68ea9fcf93935572763c11fed09431de66e6fb24789990313eeaec54", + "visited_cells": 102, + "writes": 94 + }, + { + "actions": 987, + "geometry_G_H_K_Y_J_B": [ + 2, + 3, + 7, + 10, + 2, + 1 + ], + "heads_returned": true, + "moves": 448, + "private_blank": true, + "protected_input": true, + "reads": 444, + "stencil_bits": 17, + "stencil_canonical_sha256": "1210a0b6c9c5e9eecccc285e736855ab6af8ce60f9adc727c834dace27f0dcba", + "visited_cells": 104, + "writes": 95 + }, + { + "actions": 857, + "geometry_G_H_K_Y_J_B": [ + 3, + 3, + 7, + 7, + 0, + 0 + ], + "heads_returned": true, + "moves": 386, + "private_blank": true, + "protected_input": true, + "reads": 392, + "stencil_bits": 13, + "stencil_canonical_sha256": "adceff39ffef5bfa4ecb9da365c272c5c2fed739445608a9be4d4d8e0864cb5a", + "visited_cells": 89, + "writes": 79 + }, + { + "actions": 869, + "geometry_G_H_K_Y_J_B": [ + 3, + 3, + 7, + 7, + 0, + 1 + ], + "heads_returned": true, + "moves": 392, + "private_blank": true, + "protected_input": true, + "reads": 397, + "stencil_bits": 14, + "stencil_canonical_sha256": "7abe80e94e8373f5b28ca7026f86e9c20673f5525199cafbcda2cc87b7d91ea6", + "visited_cells": 91, + "writes": 80 + }, + { + "actions": 895, + "geometry_G_H_K_Y_J_B": [ + 3, + 3, + 7, + 8, + 0, + 0 + ], + "heads_returned": true, + "moves": 404, + "private_blank": true, + "protected_input": true, + "reads": 407, + "stencil_bits": 14, + "stencil_canonical_sha256": "4b2c2345c0377dbc52d87d48a80686314f99ea2960be86ae09c4c9c593ebf0ea", + "visited_cells": 93, + "writes": 84 + }, + { + "actions": 907, + "geometry_G_H_K_Y_J_B": [ + 3, + 3, + 7, + 8, + 0, + 1 + ], + "heads_returned": true, + "moves": 410, + "private_blank": true, + "protected_input": true, + "reads": 412, + "stencil_bits": 15, + "stencil_canonical_sha256": "75672ae4f27105610f34e23abbfeda095f29d522d893254df3275a05beae443b", + "visited_cells": 95, + "writes": 85 + }, + { + "actions": 894, + "geometry_G_H_K_Y_J_B": [ + 3, + 3, + 7, + 8, + 1, + 0 + ], + "heads_returned": true, + "moves": 404, + "private_blank": true, + "protected_input": true, + "reads": 408, + "stencil_bits": 14, + "stencil_canonical_sha256": "7abe80e94e8373f5b28ca7026f86e9c20673f5525199cafbcda2cc87b7d91ea6", + "visited_cells": 93, + "writes": 82 + }, + { + "actions": 906, + "geometry_G_H_K_Y_J_B": [ + 3, + 3, + 7, + 8, + 1, + 1 + ], + "heads_returned": true, + "moves": 410, + "private_blank": true, + "protected_input": true, + "reads": 413, + "stencil_bits": 15, + "stencil_canonical_sha256": "f685e2a2fb865c1aa4debf3c5cc8e3deb4ffa43810546ed9547b3a0bf205123e", + "visited_cells": 95, + "writes": 83 + }, + { + "actions": 932, + "geometry_G_H_K_Y_J_B": [ + 3, + 3, + 7, + 9, + 1, + 0 + ], + "heads_returned": true, + "moves": 422, + "private_blank": true, + "protected_input": true, + "reads": 423, + "stencil_bits": 15, + "stencil_canonical_sha256": "75672ae4f27105610f34e23abbfeda095f29d522d893254df3275a05beae443b", + "visited_cells": 97, + "writes": 87 + }, + { + "actions": 944, + "geometry_G_H_K_Y_J_B": [ + 3, + 3, + 7, + 9, + 1, + 1 + ], + "heads_returned": true, + "moves": 428, + "private_blank": true, + "protected_input": true, + "reads": 428, + "stencil_bits": 16, + "stencil_canonical_sha256": "288c25facf24e698644d098c3a99e376cec6407b4bd0c14f2e23214ada69e0c6", + "visited_cells": 99, + "writes": 88 + }, + { + "actions": 931, + "geometry_G_H_K_Y_J_B": [ + 3, + 3, + 7, + 9, + 2, + 0 + ], + "heads_returned": true, + "moves": 422, + "private_blank": true, + "protected_input": true, + "reads": 424, + "stencil_bits": 15, + "stencil_canonical_sha256": "f685e2a2fb865c1aa4debf3c5cc8e3deb4ffa43810546ed9547b3a0bf205123e", + "visited_cells": 97, + "writes": 85 + }, + { + "actions": 943, + "geometry_G_H_K_Y_J_B": [ + 3, + 3, + 7, + 9, + 2, + 1 + ], + "heads_returned": true, + "moves": 428, + "private_blank": true, + "protected_input": true, + "reads": 429, + "stencil_bits": 16, + "stencil_canonical_sha256": "3d40edb28351ee67c5d35f2f15aa3adeee1ca578baf1fb1197ffb1037c7b2de4", + "visited_cells": 99, + "writes": 86 + }, + { + "actions": 969, + "geometry_G_H_K_Y_J_B": [ + 3, + 3, + 7, + 10, + 2, + 0 + ], + "heads_returned": true, + "moves": 440, + "private_blank": true, + "protected_input": true, + "reads": 439, + "stencil_bits": 16, + "stencil_canonical_sha256": "288c25facf24e698644d098c3a99e376cec6407b4bd0c14f2e23214ada69e0c6", + "visited_cells": 101, + "writes": 90 + }, + { + "actions": 981, + "geometry_G_H_K_Y_J_B": [ + 3, + 3, + 7, + 10, + 2, + 1 + ], + "heads_returned": true, + "moves": 446, + "private_blank": true, + "protected_input": true, + "reads": 444, + "stencil_bits": 17, + "stencil_canonical_sha256": "366c6e1b74f271ee2d96861e0af2fef9bca081f4b2cee61f326a91e554898c28", + "visited_cells": 103, + "writes": 91 + }, + { + "actions": 920, + "geometry_G_H_K_Y_J_B": [ + 3, + 3, + 8, + 8, + 0, + 0 + ], + "heads_returned": true, + "moves": 416, + "private_blank": true, + "protected_input": true, + "reads": 418, + "stencil_bits": 14, + "stencil_canonical_sha256": "f502d4bab7cf0f0007c1969407cc3b518cf12c8e59d03ae3f20aeb96c529bff6", + "visited_cells": 95, + "writes": 86 + }, + { + "actions": 932, + "geometry_G_H_K_Y_J_B": [ + 3, + 3, + 8, + 8, + 0, + 1 + ], + "heads_returned": true, + "moves": 422, + "private_blank": true, + "protected_input": true, + "reads": 423, + "stencil_bits": 15, + "stencil_canonical_sha256": "c577b08841f224627b0b2fca29bb7fc17cc78644f7fce9819b009e526340e40c", + "visited_cells": 97, + "writes": 87 + }, + { + "actions": 958, + "geometry_G_H_K_Y_J_B": [ + 3, + 3, + 8, + 9, + 0, + 0 + ], + "heads_returned": true, + "moves": 434, + "private_blank": true, + "protected_input": true, + "reads": 433, + "stencil_bits": 15, + "stencil_canonical_sha256": "dad8bf925aa6fa5280ac3534fb5ea83d31ad1f9166c8f33cd527a425ef943668", + "visited_cells": 99, + "writes": 91 + }, + { + "actions": 970, + "geometry_G_H_K_Y_J_B": [ + 3, + 3, + 8, + 9, + 0, + 1 + ], + "heads_returned": true, + "moves": 440, + "private_blank": true, + "protected_input": true, + "reads": 438, + "stencil_bits": 16, + "stencil_canonical_sha256": "4ac82d0c24db9134ab5b46fa335e77b9f28f935eac206cd65497716e803982c2", + "visited_cells": 101, + "writes": 92 + }, + { + "actions": 957, + "geometry_G_H_K_Y_J_B": [ + 3, + 3, + 8, + 9, + 1, + 0 + ], + "heads_returned": true, + "moves": 434, + "private_blank": true, + "protected_input": true, + "reads": 434, + "stencil_bits": 15, + "stencil_canonical_sha256": "c577b08841f224627b0b2fca29bb7fc17cc78644f7fce9819b009e526340e40c", + "visited_cells": 99, + "writes": 89 + }, + { + "actions": 969, + "geometry_G_H_K_Y_J_B": [ + 3, + 3, + 8, + 9, + 1, + 1 + ], + "heads_returned": true, + "moves": 440, + "private_blank": true, + "protected_input": true, + "reads": 439, + "stencil_bits": 16, + "stencil_canonical_sha256": "c71903dd665bffaf8898ae6c4b7cdbf2ed57bddc5b4c65dab394f36fbc3ec061", + "visited_cells": 101, + "writes": 90 + }, + { + "actions": 995, + "geometry_G_H_K_Y_J_B": [ + 3, + 3, + 8, + 10, + 1, + 0 + ], + "heads_returned": true, + "moves": 452, + "private_blank": true, + "protected_input": true, + "reads": 449, + "stencil_bits": 16, + "stencil_canonical_sha256": "4ac82d0c24db9134ab5b46fa335e77b9f28f935eac206cd65497716e803982c2", + "visited_cells": 103, + "writes": 94 + }, + { + "actions": 1007, + "geometry_G_H_K_Y_J_B": [ + 3, + 3, + 8, + 10, + 1, + 1 + ], + "heads_returned": true, + "moves": 458, + "private_blank": true, + "protected_input": true, + "reads": 454, + "stencil_bits": 17, + "stencil_canonical_sha256": "fe64dce859d7830aea398e38fa4fee38f2992b8a1898935b2625f5270548b6da", + "visited_cells": 105, + "writes": 95 + }, + { + "actions": 994, + "geometry_G_H_K_Y_J_B": [ + 3, + 3, + 8, + 10, + 2, + 0 + ], + "heads_returned": true, + "moves": 452, + "private_blank": true, + "protected_input": true, + "reads": 450, + "stencil_bits": 16, + "stencil_canonical_sha256": "c71903dd665bffaf8898ae6c4b7cdbf2ed57bddc5b4c65dab394f36fbc3ec061", + "visited_cells": 103, + "writes": 92 + }, + { + "actions": 1006, + "geometry_G_H_K_Y_J_B": [ + 3, + 3, + 8, + 10, + 2, + 1 + ], + "heads_returned": true, + "moves": 458, + "private_blank": true, + "protected_input": true, + "reads": 455, + "stencil_bits": 17, + "stencil_canonical_sha256": "b88f8eac9fd1e12c26b4f0f8aace4cc2a431fd220bb1267ec0bccc9271d23edf", + "visited_cells": 105, + "writes": 93 + }, + { + "actions": 1032, + "geometry_G_H_K_Y_J_B": [ + 3, + 3, + 8, + 11, + 2, + 0 + ], + "heads_returned": true, + "moves": 470, + "private_blank": true, + "protected_input": true, + "reads": 465, + "stencil_bits": 17, + "stencil_canonical_sha256": "fe64dce859d7830aea398e38fa4fee38f2992b8a1898935b2625f5270548b6da", + "visited_cells": 107, + "writes": 97 + }, + { + "actions": 1044, + "geometry_G_H_K_Y_J_B": [ + 3, + 3, + 8, + 11, + 2, + 1 + ], + "heads_returned": true, + "moves": 476, + "private_blank": true, + "protected_input": true, + "reads": 470, + "stencil_bits": 18, + "stencil_canonical_sha256": "d1bc93983b648eb490a675444ade664c269659f2ab40e908be5ef3e9782f3e1a", + "visited_cells": 109, + "writes": 98 + }, + { + "actions": 890, + "geometry_G_H_K_Y_J_B": [ + 3, + 4, + 7, + 7, + 0, + 0 + ], + "heads_returned": true, + "moves": 402, + "private_blank": true, + "protected_input": true, + "reads": 405, + "stencil_bits": 15, + "stencil_canonical_sha256": "9bd206e747614c68ff4389f9cbef776f93334e765d5a90765fb3c246f07e307c", + "visited_cells": 93, + "writes": 83 + }, + { + "actions": 902, + "geometry_G_H_K_Y_J_B": [ + 3, + 4, + 7, + 7, + 0, + 1 + ], + "heads_returned": true, + "moves": 408, + "private_blank": true, + "protected_input": true, + "reads": 410, + "stencil_bits": 16, + "stencil_canonical_sha256": "a4f5205b5524c78a60ea2972b7b79fed093e7e21ccb6a308569fc9b3c4f685e5", + "visited_cells": 95, + "writes": 84 + }, + { + "actions": 928, + "geometry_G_H_K_Y_J_B": [ + 3, + 4, + 7, + 8, + 0, + 0 + ], + "heads_returned": true, + "moves": 420, + "private_blank": true, + "protected_input": true, + "reads": 420, + "stencil_bits": 16, + "stencil_canonical_sha256": "1304a45d1cae9bf963af063a0ecc365f8be17d444b7e90792bdbf86d2eab9d3f", + "visited_cells": 97, + "writes": 88 + }, + { + "actions": 940, + "geometry_G_H_K_Y_J_B": [ + 3, + 4, + 7, + 8, + 0, + 1 + ], + "heads_returned": true, + "moves": 426, + "private_blank": true, + "protected_input": true, + "reads": 425, + "stencil_bits": 17, + "stencil_canonical_sha256": "431d3e8528ccf0bd2cdacb4e9319c40a85054d1df740d69b4fd86df44898871b", + "visited_cells": 99, + "writes": 89 + }, + { + "actions": 927, + "geometry_G_H_K_Y_J_B": [ + 3, + 4, + 7, + 8, + 1, + 0 + ], + "heads_returned": true, + "moves": 420, + "private_blank": true, + "protected_input": true, + "reads": 421, + "stencil_bits": 16, + "stencil_canonical_sha256": "a4f5205b5524c78a60ea2972b7b79fed093e7e21ccb6a308569fc9b3c4f685e5", + "visited_cells": 97, + "writes": 86 + }, + { + "actions": 939, + "geometry_G_H_K_Y_J_B": [ + 3, + 4, + 7, + 8, + 1, + 1 + ], + "heads_returned": true, + "moves": 426, + "private_blank": true, + "protected_input": true, + "reads": 426, + "stencil_bits": 17, + "stencil_canonical_sha256": "aa004ffc8910d48eba28183c83a9fecc68991abf5f52007a36c886f09c240ed6", + "visited_cells": 99, + "writes": 87 + }, + { + "actions": 965, + "geometry_G_H_K_Y_J_B": [ + 3, + 4, + 7, + 9, + 1, + 0 + ], + "heads_returned": true, + "moves": 438, + "private_blank": true, + "protected_input": true, + "reads": 436, + "stencil_bits": 17, + "stencil_canonical_sha256": "431d3e8528ccf0bd2cdacb4e9319c40a85054d1df740d69b4fd86df44898871b", + "visited_cells": 101, + "writes": 91 + }, + { + "actions": 977, + "geometry_G_H_K_Y_J_B": [ + 3, + 4, + 7, + 9, + 1, + 1 + ], + "heads_returned": true, + "moves": 444, + "private_blank": true, + "protected_input": true, + "reads": 441, + "stencil_bits": 18, + "stencil_canonical_sha256": "9451250511d6f2a4467e68b98986e85f0190bbf1446ee4c1ed00ef51f2cd8635", + "visited_cells": 103, + "writes": 92 + }, + { + "actions": 964, + "geometry_G_H_K_Y_J_B": [ + 3, + 4, + 7, + 9, + 2, + 0 + ], + "heads_returned": true, + "moves": 438, + "private_blank": true, + "protected_input": true, + "reads": 437, + "stencil_bits": 17, + "stencil_canonical_sha256": "aa004ffc8910d48eba28183c83a9fecc68991abf5f52007a36c886f09c240ed6", + "visited_cells": 101, + "writes": 89 + }, + { + "actions": 976, + "geometry_G_H_K_Y_J_B": [ + 3, + 4, + 7, + 9, + 2, + 1 + ], + "heads_returned": true, + "moves": 444, + "private_blank": true, + "protected_input": true, + "reads": 442, + "stencil_bits": 18, + "stencil_canonical_sha256": "8d24562ec40788944933da46cf8417729752c45f697cab794998c18c53f316ff", + "visited_cells": 103, + "writes": 90 + }, + { + "actions": 1002, + "geometry_G_H_K_Y_J_B": [ + 3, + 4, + 7, + 10, + 2, + 0 + ], + "heads_returned": true, + "moves": 456, + "private_blank": true, + "protected_input": true, + "reads": 452, + "stencil_bits": 18, + "stencil_canonical_sha256": "9451250511d6f2a4467e68b98986e85f0190bbf1446ee4c1ed00ef51f2cd8635", + "visited_cells": 105, + "writes": 94 + }, + { + "actions": 1014, + "geometry_G_H_K_Y_J_B": [ + 3, + 4, + 7, + 10, + 2, + 1 + ], + "heads_returned": true, + "moves": 462, + "private_blank": true, + "protected_input": true, + "reads": 457, + "stencil_bits": 19, + "stencil_canonical_sha256": "6ef926cc4e1dc63023bc3a771885965129c4ff0d4d89b0b6770c0f1e876c452d", + "visited_cells": 107, + "writes": 95 + }, + { + "actions": 953, + "geometry_G_H_K_Y_J_B": [ + 3, + 4, + 8, + 8, + 0, + 0 + ], + "heads_returned": true, + "moves": 432, + "private_blank": true, + "protected_input": true, + "reads": 431, + "stencil_bits": 16, + "stencil_canonical_sha256": "cc79b221446d595d21deb6ae14490afe8b4e7301da65ad0252308a18f3182e16", + "visited_cells": 99, + "writes": 90 + }, + { + "actions": 965, + "geometry_G_H_K_Y_J_B": [ + 3, + 4, + 8, + 8, + 0, + 1 + ], + "heads_returned": true, + "moves": 438, + "private_blank": true, + "protected_input": true, + "reads": 436, + "stencil_bits": 17, + "stencil_canonical_sha256": "f57d461354d665eb279905fe7945cd063ca615ea0db14dc76c521abb82750115", + "visited_cells": 101, + "writes": 91 + }, + { + "actions": 991, + "geometry_G_H_K_Y_J_B": [ + 3, + 4, + 8, + 9, + 0, + 0 + ], + "heads_returned": true, + "moves": 450, + "private_blank": true, + "protected_input": true, + "reads": 446, + "stencil_bits": 17, + "stencil_canonical_sha256": "3b4d1d426dfa3b1063c556c6e6278c624ea9bc4416b3e422837ba0b1abb658c5", + "visited_cells": 103, + "writes": 95 + }, + { + "actions": 1003, + "geometry_G_H_K_Y_J_B": [ + 3, + 4, + 8, + 9, + 0, + 1 + ], + "heads_returned": true, + "moves": 456, + "private_blank": true, + "protected_input": true, + "reads": 451, + "stencil_bits": 18, + "stencil_canonical_sha256": "e8f2222c9a1be16306dacb0325cebe11a5cc1fe03bf6e74c9c08b47aa94841c1", + "visited_cells": 105, + "writes": 96 + }, + { + "actions": 990, + "geometry_G_H_K_Y_J_B": [ + 3, + 4, + 8, + 9, + 1, + 0 + ], + "heads_returned": true, + "moves": 450, + "private_blank": true, + "protected_input": true, + "reads": 447, + "stencil_bits": 17, + "stencil_canonical_sha256": "f57d461354d665eb279905fe7945cd063ca615ea0db14dc76c521abb82750115", + "visited_cells": 103, + "writes": 93 + }, + { + "actions": 1002, + "geometry_G_H_K_Y_J_B": [ + 3, + 4, + 8, + 9, + 1, + 1 + ], + "heads_returned": true, + "moves": 456, + "private_blank": true, + "protected_input": true, + "reads": 452, + "stencil_bits": 18, + "stencil_canonical_sha256": "52a80610ac86380d6c25c91605b30a9632307e832e0f6dc8cf1a1ed7e9715425", + "visited_cells": 105, + "writes": 94 + }, + { + "actions": 1028, + "geometry_G_H_K_Y_J_B": [ + 3, + 4, + 8, + 10, + 1, + 0 + ], + "heads_returned": true, + "moves": 468, + "private_blank": true, + "protected_input": true, + "reads": 462, + "stencil_bits": 18, + "stencil_canonical_sha256": "e8f2222c9a1be16306dacb0325cebe11a5cc1fe03bf6e74c9c08b47aa94841c1", + "visited_cells": 107, + "writes": 98 + }, + { + "actions": 1040, + "geometry_G_H_K_Y_J_B": [ + 3, + 4, + 8, + 10, + 1, + 1 + ], + "heads_returned": true, + "moves": 474, + "private_blank": true, + "protected_input": true, + "reads": 467, + "stencil_bits": 19, + "stencil_canonical_sha256": "1eede644a7aebe8ca2a2ca1726d8d9742af72d14fe8c4d9c6af3eab9af342a75", + "visited_cells": 109, + "writes": 99 + }, + { + "actions": 1027, + "geometry_G_H_K_Y_J_B": [ + 3, + 4, + 8, + 10, + 2, + 0 + ], + "heads_returned": true, + "moves": 468, + "private_blank": true, + "protected_input": true, + "reads": 463, + "stencil_bits": 18, + "stencil_canonical_sha256": "52a80610ac86380d6c25c91605b30a9632307e832e0f6dc8cf1a1ed7e9715425", + "visited_cells": 107, + "writes": 96 + }, + { + "actions": 1039, + "geometry_G_H_K_Y_J_B": [ + 3, + 4, + 8, + 10, + 2, + 1 + ], + "heads_returned": true, + "moves": 474, + "private_blank": true, + "protected_input": true, + "reads": 468, + "stencil_bits": 19, + "stencil_canonical_sha256": "05a00be98b3839537c747979b60178c3537d5917f1a707149e8f07a86ab0995f", + "visited_cells": 109, + "writes": 97 + }, + { + "actions": 1065, + "geometry_G_H_K_Y_J_B": [ + 3, + 4, + 8, + 11, + 2, + 0 + ], + "heads_returned": true, + "moves": 486, + "private_blank": true, + "protected_input": true, + "reads": 478, + "stencil_bits": 19, + "stencil_canonical_sha256": "1eede644a7aebe8ca2a2ca1726d8d9742af72d14fe8c4d9c6af3eab9af342a75", + "visited_cells": 111, + "writes": 101 + }, + { + "actions": 1077, + "geometry_G_H_K_Y_J_B": [ + 3, + 4, + 8, + 11, + 2, + 1 + ], + "heads_returned": true, + "moves": 492, + "private_blank": true, + "protected_input": true, + "reads": 483, + "stencil_bits": 20, + "stencil_canonical_sha256": "2c2f9960269daa7dd6e9116e71d84f6ee698f386a4df84886fa1cc0b0473fd72", + "visited_cells": 113, + "writes": 102 + }, + { + "actions": 12504, + "geometry_G_H_K_Y_J_B": [ + 1, + 100, + 5, + 200, + 50, + 100 + ], + "heads_returned": true, + "moves": 5992, + "private_blank": true, + "protected_input": true, + "reads": 5076, + "stencil_bits": 500, + "stencil_canonical_sha256": "3be4fd43ee2f6ac4b8e5db2a586a4dfdec3cdcce4bbe641a856bcbc8282dfb3f", + "visited_cells": 1447, + "writes": 1436 + } + ], + "consumer_cases": [ + { + "actions": 677, + "consumer": { + "addresses": 128, + "good": 16, + "mask_sha256": "b1666b8f98e384414ae2539b95b7b15324b83057a48b8700904196c5ce383321", + "prior_consumer_action_formula": 9197 + }, + "geometry_G_H_K_Y_J_B": [ + 1, + 1, + 5, + 5, + 0, + 0 + ], + "heads_returned": true, + "moves": 298, + "private_blank": true, + "protected_input": true, + "reads": 314, + "stencil_bits": 7, + "stencil_canonical_sha256": "969d4f6bd491483d33d2dce752bf3d931f53117a8a4ef8ed24b3fef11917d95c", + "visited_cells": 71, + "writes": 65 + }, + { + "actions": 797, + "consumer": { + "addresses": 4096, + "good": 512, + "mask_sha256": "eaab86cecc30fe98665aa51cda59b21aaa85f2d586fcaf5522710b65c2b00758", + "prior_consumer_action_formula": 454830 + }, + "geometry_G_H_K_Y_J_B": [ + 1, + 2, + 5, + 7, + 1, + 1 + ], + "heads_returned": true, + "moves": 356, + "private_blank": true, + "protected_input": true, + "reads": 363, + "stencil_bits": 12, + "stencil_canonical_sha256": "bbe6b155152ee6249cdd709358d324325870fb6444f0d78a76faf5b04781354b", + "visited_cells": 85, + "writes": 78 + }, + { + "actions": 767, + "consumer": { + "addresses": 1024, + "good": 288, + "mask_sha256": "0517c1ef82aa8a40a9b2be2379ef94d13ddddda8b7ed8a3744e58071931eb0a1", + "prior_consumer_action_formula": 97428 + }, + "geometry_G_H_K_Y_J_B": [ + 2, + 2, + 6, + 6, + 0, + 0 + ], + "heads_returned": true, + "moves": 342, + "private_blank": true, + "protected_input": true, + "reads": 353, + "stencil_bits": 10, + "stencil_canonical_sha256": "b05d6a624df6a08d4bd9c4961180a8b5570329b9255b8c01f2fe3aedd187d0eb", + "visited_cells": 80, + "writes": 72 + }, + { + "actions": 777, + "consumer": { + "addresses": 512, + "good": 96, + "mask_sha256": "3d7435c77cb2dbe73f106304644951ade8fce939005865040a614e7b9ec6a6a0", + "prior_consumer_action_formula": 44679 + }, + "geometry_G_H_K_Y_J_B": [ + 1, + 1, + 6, + 7, + 1, + 0 + ], + "heads_returned": true, + "moves": 346, + "private_blank": true, + "protected_input": true, + "reads": 356, + "stencil_bits": 9, + "stencil_canonical_sha256": "18ec557e0513477c9a2e5d8d3f570ff12487767534aa222011d98f81e132415f", + "visited_cells": 81, + "writes": 75 + } + ], + "controls": [ + { + "detected": true, + "mutant": "include_parity" + }, + { + "detected": true, + "mutant": "wrong_lower_pivot" + }, + { + "detected": true, + "mutant": "wrong_upper_pivot" + }, + { + "detected": true, + "mutant": "omit_cleanup" + }, + { + "detected": true, + "mutant": "omit_output_return" + } + ], + "guardrail": "PASS_AST_SCOPE_GUARDRAIL_NOT_A_FORMAL_MACHINE_CERTIFICATE", + "predecessor_head": "4f49743a9df0cf7501cdc62bd5707a122fa071e9", + "predecessor_source_sha256": { + "adapter": "40794cd2e2936f0f5e42fac1bb51b65c951a2ab56b7e88824e8c2d09a3dbf40e", + "machine": "1cb27312932914eb631078bd56e85feb1dc6c4191e9d1962b2cc3a7e1cfb8df7" + }, + "producer_cases": 145, + "producer_sha256": "8586d019a0a35390d36b944a2b764ec96682040b1abc42e29d740faf5a830bd0", + "rejections": [ + { + "actions": 205, + "shape": [ + 0, + 1, + 5, + 5, + 0, + 0 + ] + }, + { + "actions": 237, + "shape": [ + 2, + 1, + 6, + 6, + 0, + 0 + ] + }, + { + "actions": 394, + "shape": [ + 2, + 2, + 5, + 5, + 0, + 0 + ] + }, + { + "actions": 579, + "shape": [ + 1, + 1, + 5, + 5, + 1, + 0 + ] + }, + { + "actions": 101, + "defect": "bad_symbol" + }, + { + "actions": 105, + "defect": "missing_end" + }, + { + "actions": 109, + "defect": "nonblank_after_end" + } + ], + "scope": "Canonical unary six-field one-target family only; input encoding and general descriptor production remain unpriced; no complete E evaluator, CRT supplier, precision or kappa claim", + "setup_action_formula": "33H+25K+38Y-6G-J+12B+335 <= 63L+335; L=2H+Y+B", + "setup_visited_space_formula": "4H+2K+4Y-G+2B+38 <= 6L+38", + "status": "PASS_LITERAL_UNARY_ONE_TARGET_STENCIL_PRODUCER_NO_NEW_KAPPA", + "total_producer_actions": 138792 +} diff --git a/research/crt-unary-stencil-producer/SOURCES.json b/research/crt-unary-stencil-producer/SOURCES.json new file mode 100644 index 0000000000..9670a89349 --- /dev/null +++ b/research/crt-unary-stencil-producer/SOURCES.json @@ -0,0 +1,64 @@ +{ + "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" + }, + { + "path": "research/unconditional-batched-crt/NOTICE.md", + "usage": "input", + "git_blob": "886a8fdee275f01b459cbd68ae2815dc9269502f", + "sha256": "924109837e71c52392191710d49c9deb42780878d1094f0b01e8690dbe799461" + }, + { + "path": "research/crt-unary-stencil-producer/source/PREDECESSOR-PROOF.md.txt", + "usage": "input", + "git_blob": "235d7405ffcf712ad3905c3077719554ade0790c", + "sha256": "c075a3c261bb824884f0da9f99fed227b15f9fac087bbdeb2c2cb861d4091f11", + "pin": "head:5a41fea466cbeb7839bde864e563e191de47a0f7:research/crt-unary-stencil-producer/source/PREDECESSOR-PROOF.md.txt" + }, + { + "path": "research/crt-unary-stencil-producer/source/PREDECESSOR-README.md.txt", + "usage": "input", + "git_blob": "fd0dd321baa1592999677f212ffa77cbb1bb513c", + "sha256": "912595166aded8591819c1f4fccdd7bfa44361906a1466057f838a656e85f329", + "pin": "head:5a41fea466cbeb7839bde864e563e191de47a0f7:research/crt-unary-stencil-producer/source/PREDECESSOR-README.md.txt" + }, + { + "path": "research/crt-unary-stencil-producer/source/predecessor_adapter.py", + "usage": "input", + "git_blob": "2f221b5678bbb80c3c694c843b2eb84c5f5e9ee4", + "sha256": "40794cd2e2936f0f5e42fac1bb51b65c951a2ab56b7e88824e8c2d09a3dbf40e", + "pin": "head:5a41fea466cbeb7839bde864e563e191de47a0f7:research/crt-unary-stencil-producer/source/predecessor_adapter.py" + }, + { + "path": "research/crt-unary-stencil-producer/source/predecessor_machine.py", + "usage": "input", + "git_blob": "ce763898bd7b4401bbab818c640a0593b65c9a82", + "sha256": "1cb27312932914eb631078bd56e85feb1dc6c4191e9d1962b2cc3a7e1cfb8df7", + "pin": "head:5a41fea466cbeb7839bde864e563e191de47a0f7:research/crt-unary-stencil-producer/source/predecessor_machine.py" + } + ] +} diff --git a/research/crt-unary-stencil-producer/TASK.json b/research/crt-unary-stencil-producer/TASK.json new file mode 100644 index 0000000000..7e34600ffb --- /dev/null +++ b/research/crt-unary-stencil-producer/TASK.json @@ -0,0 +1,100 @@ +{ + "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": "One-target unary encoded geometry to literal paid ordered stencil and unchanged retained guard-mask scanner.", + "scope_change_reason": "Take PR4201 explicit open encoded-stencil-producer handoff, replacing one unpriced host geometry adapter with a marker-driven finite-alphabet fixed-role tape program. Unary r=1 boundary is deliberate; global/binary/many-target conversion remains open.", + "bottleneck_link": "The supplied-stencil scanner alone does not charge construction/admission of its thresholds and layout. This contribution closes that one input boundary for six protected unary geometry words.", + "budget_minutes": 60, + "stop_rule": "Freeze one bounded producer/consumer result by15:48:31UTC; reserve final15minutes for independent verification, exact committed Git-free replay, publication and handoff. Stop before full E, many-target or native/outer expansion.", + "outcome": "completed", + "evidence": "Paid producer with written all-admitted-input bound, exact encoded admission, unchanged scanner, independent pre-code oracle and separate cost/ownership review; normal/strict-optimized committed replay.", + "author": "ToikY with substantial OpenAI Codex assistance", + "ai_assistance": "Coordinating integration, primary producer/proof, independently frozen oracle and separate contract/cost-review contexts; not independent human or formal-kernel acceptance.", + "open_questions": [ + { + "question": "Can an actual transported/binary geometry producer supply the same unary descriptor without exceeding the complete caller allowance?", + "why_it_matters": "The current component starts at six unary records for exactly one target. The full E and many-target production boundary remains open.", + "first_step": "Pin a production descriptor at its actual caller, specify owned/borrowed state and charge conversion, all reads, returns, erasure and the retained mask scan.", + "blocked_by": "No full transformed descriptor production or many-target scanner invocation is supplied here." + } + ], + "scope_key": "d88f6c1a1a5a19d7cc66", + "upstream_main": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "predecessor_head": "4f49743a9df0cf7501cdc62bd5707a122fa071e9", + "canonical_claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/4173#discussioncomment-19075225", + "first_working_example": { + "command": "python3.12 -I -B research/crt-unary-stencil-producer/primary_verify.py", + "reason_for_override": "The live explicit producer handoff supplies the concrete first example; no complete PR4100 or historical source replay is warranted." + }, + "freshness": { + "open_prs": 322, + "fetched_at": "2026-10-20T15:09:22+00:00", + "live_discussions": [ + 1166, + 4173 + ], + "broader_coverage": "partial" + }, + "family_decision": "narrow to explicit unpriced producer/consumer interface", + "obligation_ledger": { + "supplied_stencil_scan": "predecessor proof; source pinned", + "unary_setup": "scoped written proof and separate-agent checks for unary r=1 producer; exact paid setup/cleanup; no human/formal acceptance", + "binary_global_descriptor_producer": "unknown", + "many_target_composition": "unknown", + "exception_keys_sort_reinsert": "unknown", + "payload_repair_ordinary_callee_precision_native_outer": "unknown" + } +} diff --git a/research/crt-unary-stencil-producer/VERIFY.json b/research/crt-unary-stencil-producer/VERIFY.json new file mode 100644 index 0000000000..0a1e632eff --- /dev/null +++ b/research/crt-unary-stencil-producer/VERIFY.json @@ -0,0 +1,109 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/unconditional-batched-crt/CRT.md", + "research/unconditional-batched-crt/check_batched_crt.py", + "research/unconditional-batched-crt/NOTICE.md", + "research/crt-unary-stencil-producer/source/PREDECESSOR-PROOF.md.txt", + "research/crt-unary-stencil-producer/source/PREDECESSOR-README.md.txt", + "research/crt-unary-stencil-producer/source/predecessor_adapter.py", + "research/crt-unary-stencil-producer/source/predecessor_machine.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/primary_verify.py" + ], + "timeout_seconds": 120, + "checks": "Actual encoded admission/producer, paid tape actions, ownership and semantic controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/primary_verify.py" + ], + "timeout_seconds": 120, + "checks": "Actual encoded admission/producer, paid tape actions, ownership and semantic controls." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/independent_oracle.py" + ], + "timeout_seconds": 120, + "checks": "Code-disjoint preimplementation direct stencil/predicate oracle; no primary import." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/independent_oracle.py" + ], + "timeout_seconds": 120, + "checks": "Code-disjoint preimplementation direct stencil/predicate oracle; no primary import." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/cross_check.py" + ], + "timeout_seconds": 120, + "checks": "Hash-bound produced stencils consumed by unchanged predecessor machine and compared against independent/source predicates." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/cross_check.py" + ], + "timeout_seconds": 120, + "checks": "Hash-bound produced stencils consumed by unchanged predecessor machine and compared against independent/source predicates." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/cost_check.py" + ], + "timeout_seconds": 120, + "checks": "Separate primitive-call instrumentation corroborates exact producer action/space formulas and detects a one-READ undercharge with unchanged values/ownership." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/cost_check.py" + ], + "timeout_seconds": 120, + "checks": "Separate primitive-call instrumentation corroborates exact producer action/space formulas and detects a one-READ undercharge with unchanged values/ownership." + } + ] +} diff --git a/research/crt-unary-stencil-producer/cost_check.py b/research/crt-unary-stencil-producer/cost_check.py new file mode 100644 index 0000000000..c595921730 --- /dev/null +++ b/research/crt-unary-stencil-producer/cost_check.py @@ -0,0 +1,138 @@ +#!/usr/bin/env python3 +"""Independent primitive-call census for the literal unary stencil producer. + +No primary verifier or semantic oracle is imported. A read-accounting fault +executes the same program and cell semantics but omits exactly one billed READ. +The observer trace must reject that one-action invoice discrepancy. +""" +import argparse +import ast +from hashlib import sha256 +import json +from pathlib import Path + +CONSUMER_SHA = '1cb27312932914eb631078bd56e85feb1dc6c4191e9d1962b2cc3a7e1cfb8df7' + +def need(test, message): + if not test: + raise RuntimeError(message) + +def load_code(path): + raw=path.read_bytes() + scope={'__file__':str(path),'__name__':'cost_review_component'} + exec(compile(raw,str(path),'exec',dont_inherit=True,optimize=0),scope) + return raw,scope + +def inspect_control(raw): + tree=ast.parse(raw) + need(not any(isinstance(n,(ast.Import,ast.ImportFrom,ast.Subscript,ast.BinOp,ast.AugAssign)) for n in ast.walk(tree)), + 'program acquired imports, indexing or host arithmetic; re-review finite control') + attrs={n.attr for n in ast.walk(tree) if isinstance(n,ast.Attribute)} + need(attrs <= {'read','write','move'},'program acquired an observer or nonprimitive attribute') + direct_calls={n.func.id for n in ast.walk(tree) if isinstance(n,ast.Call) and isinstance(n.func,ast.Name)} + need(not direct_calls & {'len','range','enumerate','zip','int','float','sum','min','max','getattr','setattr','eval','exec','compile'}, + 'program acquired host data operations') + return {'primitive_attributes':sorted(attrs),'syntactic_guardrail_only_not_formal_compilation':True} + +class World: + def __init__(self, base_tape, undercharge_one_read=False): + self.roles=[] + self.omissions=1 if undercharge_one_read else 0 + world=self + class ObservedTape(base_tape): + def __init__(self,cells=None): + super().__init__(cells) + self.primitive_reads=self.primitive_writes=self.primitive_moves=0 + self.visited={0} + world.roles.append(self) + def read(self): + self.primitive_reads+=1 + self.visited.add(self.head) + symbol=super().read() + if world.omissions: + self.reads-=1 + world.omissions-=1 + return symbol + def write(self,symbol): + self.primitive_writes+=1 + self.visited.add(self.head) + super().write(symbol) + def move(self,direction): + self.primitive_moves+=1 + super().move(direction) + self.visited.add(self.head) + self.Tape=ObservedTape + + def census(self): + reads=sum(t.primitive_reads for t in self.roles) + writes=sum(t.primitive_writes for t in self.roles) + moves=sum(t.primitive_moves for t in self.roles) + return {'reads':reads,'writes':writes,'moves':moves,'primitive_actions':reads+writes+moves, + 'reported_actions':sum(t.actions for t in self.roles), + 'visited_cells':sum(len(t.visited) for t in self.roles),'roles':len(self.roles)} + +def execute(geometry,producer,base_tape,fault=False): + world=World(base_tape,fault) + inputs=[world.Tape(['<']+['1']*n+['>','_']) for n in geometry] + before=[list(t.cells) for t in inputs] + work,stencil=producer(*inputs,world.Tape) + g,h,k,y,j,b=geometry + length=2*h+y+b + expected_actions=33*h+25*k+38*y-6*g-j+12*b+335 + expected_space=4*h+2*k+4*y-g+2*b+38 + census=world.census() + need(census['roles']==15,'producer role inventory') + need(census['primitive_actions']==expected_actions,'exact macro-composed action invoice') + need(census['visited_cells']==expected_space,'exact visited-cell invoice') + need(all(t.head==0 for t in world.roles),'all producer heads return') + need([t.cells for t in inputs]==before,'protected input changed') + need(all(t.cells[0]=='<' and all(s=='_' for s in t.cells[1:]) for t in work),'private data/END not blank') + need(len(stencil.cells)==length+2 and stencil.cells[0]=='<' and stencil.cells[-1]=='>','owned stencil shape') + if fault: + need(census['reported_actions']==expected_actions-1,'one READ omission failed to change invoice') + else: + need(census['reported_actions']==expected_actions,'nominal observer bill') + return census,[t.cells[:] for t in world.roles] + +def main(): + parser=argparse.ArgumentParser(description=__doc__) + parser.add_argument('--producer',type=Path,default=Path(__file__).resolve().parent/'producer.py') + parser.add_argument('--consumer',type=Path,default=Path(__file__).resolve().parent/'source'/'predecessor_machine.py') + parser.add_argument('--output',type=Path) + args=parser.parse_args() + consumer_raw=args.consumer.read_bytes() + need(sha256(consumer_raw).hexdigest()==CONSUMER_SHA,'retained consumer immutable hash') + producer_raw,program=load_code(args.producer) + _,consumer=load_code(args.consumer) + control=inspect_control(producer_raw) + fixtures=[(1,1,5,5,0,0),(1,3,5,9,2,2),(1,1,7,8,1,0), + (2,2,6,6,0,0),(2,5,9,15,3,4),(3,3,7,7,0,1), + (3,4,10,16,6,0),(4,8,8,15,7,3),(8,10,12,20,8,4), + (15,17,21,30,9,2),(31,32,35,40,5,0),(1,80,5,9,4,90), + (1,1,100,120,20,3),(100,120,104,140,36,20)] + cases=[] + for geom in fixtures: + census,_=execute(geom,program['produce'],consumer['Tape']) + cases.append({'geometry_G_H_K_Y_J_B':list(geom),**census}) + baseline,baseline_cells=execute(fixtures[0],program['produce'],consumer['Tape']) + fault,fault_cells=execute(fixtures[0],program['produce'],consumer['Tape'],True) + need(baseline_cells==fault_cells,'READ billing fault unexpectedly changed semantics/ownership') + need(fault['primitive_actions']==baseline['primitive_actions'] and fault['reported_actions']!=baseline['reported_actions'], + 'READ billing fault not independently rejected') + result={'status':'PASS_INDEPENDENT_PRODUCER_ACTION_AND_OWNERSHIP_CENSUS', + 'scope':'Exact affine formulas justified by separate macro proof; finite actual-program primitive-call instrumentation corroborates them. No duplicate semantic oracle or complete caller theorem.', + 'producer_sha256':sha256(producer_raw).hexdigest(),'consumer_sha256':CONSUMER_SHA, + 'code_sha256':sha256(Path(__file__).read_bytes()).hexdigest(), + 'action_formula':'33H+25K+38Y-6G-J+12B+335', + 'visited_cell_formula':'4H+2K+4Y-G+2B+38','cases':cases,'control_guardrail':control, + 'underbilled_READ_control':{'same_actual_program':True,'same_final_cells_and_ownership':True, + 'primitive_actions':fault['primitive_actions'],'reported_actions':fault['reported_actions'], + 'omitted_READ_actions':1,'invoice_rejected':True}, + 'limits':['finite-control AST check is a guardrail, not a formal compiler certificate', + 'canonical distinct protected unary role inputs with blank tails are an interface premise', + 'no full many-target/transformed-descriptor/caller E evaluation or outer theorem']} + payload=json.dumps(result,sort_keys=True,indent=2)+'\n' + if args.output is not None:args.output.write_text(payload) + print(json.dumps({k:v for k,v in result.items() if k!='cases'},sort_keys=True)) + +if __name__=='__main__':main() diff --git a/research/crt-unary-stencil-producer/cross_check.py b/research/crt-unary-stencil-producer/cross_check.py new file mode 100644 index 0000000000..2a3108565e --- /dev/null +++ b/research/crt-unary-stencil-producer/cross_check.py @@ -0,0 +1,148 @@ +"""Bind paid unary output to the unchanged scanner and pre-code source oracle. + +All indexing, integers and hashes here are observer verification, not producer +instructions. The consumer and source adapter are authenticated before exec. +""" +import argparse +import ast +import hashlib +import json +from pathlib import Path +import sys +import types + +P = Path(__file__).resolve().parent +ROOT = P.parents[1] + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def load(name, path): + module = types.ModuleType(name) + module.__file__ = str(path) + sys.modules[name] = module + exec(compile(path.read_bytes(), str(path), 'exec', dont_inherit=True, optimize=0), module.__dict__) + return module + + +def bind_inputs(): + rows = json.loads((P / 'SOURCES.json').read_text())['files'] + count = 0 + for row in rows: + if row['usage'] != 'input': + continue + raw = (ROOT / row['path']).read_bytes() + need(hashlib.sha256(raw).hexdigest() == row['sha256'], 'declared input SHA256: ' + row['path']) + need(hashlib.sha1(b'blob ' + str(len(raw)).encode() + b'\0' + raw).hexdigest() == row['git_blob'], + 'declared Git blob: ' + row['path']) + count += 1 + pins = json.loads((P / 'SOURCE-PINS.json').read_text()) + for row in pins: + need(row['origin_commit'] == '4f49743a9df0cf7501cdc62bd5707a122fa071e9', 'exact predecessor head') + raw = (ROOT / row['path']).read_bytes() + need(len(raw) == row['size'] and hashlib.sha256(raw).hexdigest() == row['sha256'], + 'unchanged minimal predecessor export') + need(hashlib.sha256((P / 'independent_oracle.py').read_bytes()).hexdigest() + == '78ba91c921ddcb37cefe674e10f34e9f896c6243af859bdb63f50b6e7086cd34', + 'pre-code oracle freeze') + return count + + +def build(producer, machine, shape, **mutant): + inputs = tuple(machine.Tape([machine.LEFT] + ['1'] * n + [machine.END, machine.BLANK]) for n in shape) + before = [list(t.cells) for t in inputs] + work, stencil = producer.produce(*inputs, machine.Tape, **mutant) + need(all(t.cells == old for t, old in zip(inputs, before)), 'protected unary input cells') + if not mutant.get('omit_cleanup'): + need(all(t.cells[0] == machine.LEFT and all(c == machine.BLANK for c in t.cells[1:]) for t in work), + 'eight private records erased with END markers') + if not mutant.get('omit_output_return'): + need(all(t.head == 0 for t in inputs + work + (stencil,)), 'producer heads at permanent LEFT') + invoice = sum(t.actions for t in inputs + work + (stencil,)) + if not mutant: + g, h, k, y, j, b = shape + need(invoice == 33*h + 25*k + 38*y - 6*g - j + 12*b + 335, 'independent exact producer invoice') + need(sum(len(t.cells) for t in inputs + work + (stencil,)) == 4*h + 2*k - g + 4*y + 2*b + 38, + 'independent exact visited-space census') + return stencil, invoice + + +def consume(machine, stencil): + original = list(stencil.cells) + previous = stencil.actions + counter, mask = machine.transduce(stencil) + need(stencil.cells == original and counter.head == mask.head == stencil.head == 0, 'consumer protected/returned boundary') + need(all(c == machine.BLANK for c in counter.cells[1:]), 'consumer counter erased including END') + bits = ''.join(mask.cells[1:-1]) + length = len(stencil.cells) - 2 + need(len(bits) == 1 << length and mask.cells[0] == machine.LEFT and mask.cells[-1] == machine.END, + 'owned complete mask') + actions = sum(t.actions for t in (stencil, counter, mask)) - previous + need(actions == 8 * len(bits) * length + 15 * len(bits) + 13 * length + 18, 'unchanged scanner exact invoice') + return bits, actions + + +def run(): + bindings = bind_inputs() + producer = load('cross_producer', P / 'producer.py') + machine = load('cross_retained_machine', P / 'source/predecessor_machine.py') + oracle = load('cross_frozen_oracle', P / 'independent_oracle.py') + source = load('cross_crt_source', ROOT / 'research/unconditional-batched-crt/check_batched_crt.py') + frozen = json.loads((P / 'ORACLE-RESULT.json').read_text()) + rows, addresses, setups, scans = [], 0, 0, 0 + for entry in frozen['rows']: + shape = tuple(entry[key] for key in ('G', 'H', 'K', 'Y', 'J', 'B')) + g, h, k, y, j, b = shape + stencil, invoice = build(producer, machine, shape) + cells = oracle.expected_stencil(*shape) + need(stencil.cells == [machine.LEFT] + cells + [machine.END], 'paid output versus pre-code direct stencil') + need(hashlib.sha256(json.dumps(cells, separators=(',', ':')).encode()).hexdigest() + == entry['stencil_json_sha256'], 'frozen oracle stencil receipt') + bits, scan = consume(machine, stencil) + need(hashlib.sha256(bits.encode()).hexdigest() == entry['bad_mask_sha256'], 'actual consumer versus pre-code mask') + for address, bit in enumerate(bits): + yy = (address >> b) & ((1 << y) - 1) + tt = (address >> (b + y)) & ((1 << h) - 1) + uu = address >> (b + y + h) + expected = oracle.source_good(address, *shape) + need(source.good(uu, tt, yy, bits=g, positions=(j,), guard=k) == expected == (bit == '0'), + 'actual source good predicate') + need(source.linear_guard(uu, tt, yy, bits=g, positions=(j,), guard=k, control_bits=h, ybits=y) + == expected, 'actual source linear-guard predicate') + rows.append(dict(geometry=list(shape), addresses=len(bits), setup_actions=invoice, scanner_actions=scan)) + addresses += len(bits) + setups += invoice + scans += scan + # These execute changed producer instructions and the unchanged consumer. + # They leave the admitted model deliberately; they are not predecessor bugs. + shape = (1, 2, 5, 7, 1, 1) + stencil, _ = build(producer, machine, shape) + right, _ = consume(machine, stencil) + controls = [] + for name in ('include_parity', 'wrong_lower_pivot', 'wrong_upper_pivot'): + wrong_stencil, _ = build(producer, machine, shape, **{name: True}) + wrong, _ = consume(machine, wrong_stencil) + address = next((i for i, pair in enumerate(zip(right, wrong)) if pair[0] != pair[1]), None) + need(address is not None, 'changed producer has actual predicate impact: ' + name) + controls.append(dict(mutant=name, first_different_address=address, correct_bad=right[address], mutant_bad=wrong[address])) + return dict(status='PASS_UNARY_STENCIL_CALLER_CROSSCHECK', declared_source_bindings=bindings, + geometries=len(rows), addresses=addresses, setup_actions=setups, scanner_actions=scans, + rows=rows, semantic_producer_consumer_controls=controls, + scope='One-target unary geometry producer composed with unchanged scanner. Finite execution corroborates the separate all-admitted-input proof; no binary/global descriptor, many-target, payload or full CRT theorem.') + + +def main(): + ap = argparse.ArgumentParser(description=__doc__) + ap.add_argument('--output', type=Path) + args = ap.parse_args() + result = run() + if args.output: + args.output.write_text(json.dumps(result, indent=2, sort_keys=True) + '\n') + print(json.dumps({k:result[k] for k in ('status','geometries','addresses','setup_actions','scanner_actions')})) + + +if __name__ == '__main__': + main() diff --git a/research/crt-unary-stencil-producer/independent_oracle.py b/research/crt-unary-stencil-producer/independent_oracle.py new file mode 100644 index 0000000000..e8c989cdf7 --- /dev/null +++ b/research/crt-unary-stencil-producer/independent_oracle.py @@ -0,0 +1,223 @@ +#!/usr/bin/env python3 +"""Direct one-target geometry oracle, independent of the encoded producer. + +Only the predecessor's published source predicate/consumer alphabet was read. +This module imports no primary implementation and has no runtime source loader. +""" + +import argparse +import hashlib +from itertools import product +import json +from pathlib import Path + + +SKIP = ("S", False, False, "0", "0") + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def admit_geometry(g, h, k, y, j, b): + need(all(type(v) is int for v in (g, h, k, y, j, b)), "exact integer geometry") + need(g >= 1 and h >= g and k >= g + 4 and j >= 0 and b >= 0 + and y >= j + k, "one-target source geometry") + return 2 * h + y + b + + +def expected_stencil(g, h, k, y, j, b): + """Direct MSB-position specification; numeric offsets are oracle-only.""" + length = admit_geometry(g, h, k, y, j, b) + intervals = ((h - g, h, "D"), (2 * h - g, 2 * h, "D"), + (2 * h + y - j - k, 2 * h + y - j - 1, "G")) + low, high = 1 << (g + 1), (1 << (k - 1)) - (1 << (g + 1)) + result = [] + for position in range(length): + atom = SKIP + for start, stop, kind in intervals: + if start <= position < stop: + need(atom == SKIP, "oracle interval overlap") + shift = stop - 1 - position + atom = (kind, position == start, position == stop - 1, + str((low >> shift) & 1) if kind == "G" else "0", + str((high >> shift) & 1) if kind == "G" else "0") + result.append(atom) + return result + + +def source_good(address, g, h, k, y, j, b): + """Direct predecessor formula with MSB-ordered u/t/y/back fields.""" + length = admit_geometry(g, h, k, y, j, b) + need(type(address) is int and 0 <= address < (1 << length), "fixed-width address") + y_word = (address >> b) % (1 << y) + t_word = (address >> (b + y)) % (1 << h) + u_word = address >> (b + y + h) + radix = 1 << g + higher_guard = (y_word >> (j + 1)) % (1 << (k - 1)) + return (u_word % radix != radix - 1 and t_word % radix != radix - 1 + and 2 * radix <= higher_guard < (1 << (k - 1)) - 2 * radix) + + +def stencil_good(address, cells): + """Independent interval-integer semantics, not the consumer flag machine.""" + word, low, high, kind = 0, 0, 0, None + for index, atom in enumerate(cells): + tag, begin, end, lo, hi = atom + if tag == "S": + need(kind is None and atom == SKIP, "skip while active") + continue + if begin: + need(kind is None, "nested interval") + word, low, high, kind = 0, 0, 0, tag + need(kind == tag, "interval kind mismatch") + bit = (address >> (len(cells) - 1 - index)) & 1 + word = 2 * word + bit + low = 2 * low + int(lo) + high = 2 * high + int(hi) + if end: + if tag == "D": + # All accumulated bits are one iff word+1 is a power of two. + # Track interval width by its begin position, independently of G. + start = index + while not cells[start][1]: + start -= 1 + if word == (1 << (index - start + 1)) - 1: + return False + elif tag == "G": + if not low <= word < high: + return False + else: + raise ValueError("unexpected active alphabet") + kind = None + need(kind is None, "unterminated interval") + return True + + +def expected_boundary_controls(): + count = 0 + examples = [] + for g in (1, 2, 3, 8, 31): + for j in (0, 1, 3): + h, k, y, b = g + 2, g + 4, j + g + 6, 2 + lower, upper = 1 << (g + 1), (1 << (k - 1)) - (1 << (g + 1)) + cells = expected_stencil(g, h, k, y, j, b) + for guard in (lower - 1, lower, lower + 1, upper - 1, upper, upper + 1): + expected = lower <= guard < upper + for parity, spectators in product((0, 1), repeat=2): + # Both H fields have nonzero inactive prefixes in one case; + # active G-bit digits are zero. Every unspecified bit toggles. + u = t = (((1 << (h - g)) - 1) << g) if spectators else 0 + ignored_high = ((1 << (y - j - k)) - 1) << (j + k) if spectators else 0 + ignored_low = (1 << j) - 1 if spectators else 0 + y_word = ignored_high | (guard << (j + 1)) | (parity << j) | ignored_low + back = (1 << b) - 1 if spectators else 0 + address = (((u << h) | t) << (y + b)) | (y_word << b) | back + need(source_good(address, g, h, k, y, j, b) == expected, + "source boundary/parity/spectator discrepancy") + need(stencil_good(address, cells) == expected, + "stencil boundary/parity/spectator discrepancy") + count += 1 + examples.append({"G": g, "J": j, "lower_inclusive": lower, + "upper_exclusive": upper, "length": len(cells)}) + return {"checked_addresses": count, "geometries": examples, + "spectators": ["inactive H prefixes", "Y bits above guard", "Y bits below parity", "B bits"], + "parity_excluded": True} + + +def must_reject(arguments): + try: + expected_stencil(*arguments) + except ValueError: + return True + raise RuntimeError("invalid geometry was admitted: " + repr(arguments)) + + +def admission_controls(): + invalid = [(0, 1, 5, 5, 0, 0), (2, 1, 6, 6, 0, 0), + (1, 1, 4, 5, 0, 0), (1, 1, 5, 4, 0, 0), + (1, 1, 5, 5, -1, 0), (1, 1, 5, 5, 0, -1), + (True, 1, 5, 5, 0, 0), (1, 1.0, 5, 5, 0, 0), + (1, 1, 5, 6, 2, 0)] + return {"rejected_geometry_cases": sum(must_reject(args) for args in invalid), + "classes": ["zero G", "H> (b + j)) % (1 << k) + need(source_good(correct, g, h, k, y, j, b) + and not lower <= wrong_guard_with_parity < upper, + "include-parity counterexample not discriminating") + evidence.append({"control": "include-parity-mutant", "expected_good": True, + "wrong_guard": wrong_guard_with_parity}) + return evidence + + +def run(): + rows, addresses, total_good = [], 0, 0 + for g, extra_h, extra_k, j, extra_y, b in product((1, 2), (0, 1), (0, 1), + (0, 1, 2), (0, 1), (0, 1)): + h, k = g + extra_h, g + 4 + extra_k + y = j + k + extra_y + length = 2 * h + y + b + if length > 14: + continue + cells = expected_stencil(g, h, k, y, j, b) + mask = bytearray() + good_count = 0 + for address in range(1 << length): + expected = source_good(address, g, h, k, y, j, b) + need(stencil_good(address, cells) == expected, "source/stencil finite mismatch") + mask.append(ord("0") if expected else ord("1")) + good_count += expected + addresses += len(mask) + total_good += good_count + rows.append({"G": g, "H": h, "K": k, "Y": y, "J": j, "B": b, + "L": length, "addresses": len(mask), "good_addresses": good_count, + "bad_mask_sha256": hashlib.sha256(mask).hexdigest(), + "stencil_json_sha256": hashlib.sha256(json.dumps(cells, separators=(",", ":")).encode()).hexdigest()}) + return {"status": "PASS", "scope": "direct one-target numeric oracle, not a charged producer", + "finite_cap": {"G": [1, 2], "extra_H": [0, 1], "extra_K": [0, 1], + "J": [0, 1, 2], "extra_Y": [0, 1], "B": [0, 1], "max_L": 14}, + "geometry_count": len(rows), "address_count": addresses, + "good_address_count": total_good, "rows": rows, + "boundary_controls": expected_boundary_controls(), + "admission_controls": admission_controls(), "semantic_controls": semantic_controls(), + "limitations": ["Finite corroboration; arbitrary parameters require the written proof.", + "No primary producer imported or inspected before oracle freeze.", + "No production multi-target reservoir, payload repair, E evaluator, or outer theorem."]} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--output", type=Path) + args = parser.parse_args() + result = run() + payload = json.dumps(result, indent=2, sort_keys=True) + "\n" + if args.output: + args.output.write_text(payload, encoding="utf-8") + print(json.dumps({key: result[key] for key in ("status", "scope", "geometry_count", "address_count", "good_address_count")}, sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/crt-unary-stencil-producer/primary_verify.py b/research/crt-unary-stencil-producer/primary_verify.py new file mode 100644 index 0000000000..cea5903219 --- /dev/null +++ b/research/crt-unary-stencil-producer/primary_verify.py @@ -0,0 +1,247 @@ +"""Observer-only verification of the literal unary producer and consumer.""" +import argparse +import ast +from hashlib import sha256 +import json +from pathlib import Path +import sys +import tempfile +import types + +HERE = Path(__file__).resolve().parent +MACHINE_SHA = "1cb27312932914eb631078bd56e85feb1dc6c4191e9d1962b2cc3a7e1cfb8df7" +ADAPTER_SHA = "40794cd2e2936f0f5e42fac1bb51b65c951a2ab56b7e88824e8c2d09a3dbf40e" + + +def need(ok, why): + if not ok: + raise ValueError(why) + + +def load(name, path, expected=None): + data = path.read_bytes() + if expected is not None: + need(sha256(data).hexdigest() == expected, "authenticated predecessor source: " + name) + module = types.ModuleType(name) + module.__file__ = str(path) + sys.modules[name] = module + exec(compile(data, str(path), "exec", dont_inherit=True, optimize=0), module.__dict__) + return module + + +def public_inputs(machine, shape): + return tuple(machine.Tape([machine.LEFT] + ["1"] * n + [machine.END]) for n in shape) + + +def observed_run(producer, machine, shape, mutant=None): + inputs = public_inputs(machine, shape) + before = [t.cells[:] for t in inputs] + allocated = [] + + def fresh(): + t = machine.Tape() + allocated.append(t) + return t + + work, stencil = producer.produce(*inputs, fresh, **(mutant or {})) + need(len(work) == 8 and len(allocated) == 9, "fixed eight private plus one output role") + protected = all(t.cells[:len(old)] == old and all(x == machine.BLANK for x in t.cells[len(old):]) + for t, old in zip(inputs, before)) + private_blank = all(t.cells[0] == machine.LEFT and all(x == machine.BLANK for x in t.cells[1:]) + for t in work) + heads = all(t.head == 0 for t in inputs + work + (stencil,)) + all_tapes = inputs + work + (stencil,) + counts = {"reads": sum(t.reads for t in all_tapes), + "writes": sum(t.writes for t in all_tapes), + "moves": sum(t.moves for t in all_tapes)} + counts["actions"] = sum(counts.values()) + counts["visited_cells"] = sum(len(t.cells) for t in all_tapes) + return stencil, {"geometry_G_H_K_Y_J_B": list(shape), **counts, + "protected_input": protected, "private_blank": private_blank, + "heads_returned": heads}, inputs, work + + +def case(producer, machine, adapter, shape, consume=False): + g, h, k, y, j, b = shape + stencil, receipt, inputs, work = observed_run(producer, machine, shape) + expected = adapter.geometry_stencil(g, h, y, (j,), k, b, machine) + need(stencil.cells == [machine.LEFT] + expected + [machine.END], "actual predecessor stencil equality") + need(receipt["protected_input"] and receipt["private_blank"] and receipt["heads_returned"], + "producer complete boundary") + length = 2*h+y+b + need(receipt["actions"] == 33*h+25*k+38*y-6*g-j+12*b+335, + "written exact successful setup action census") + need(receipt["actions"] <= 63*length+335, "written linear setup bound") + need(receipt["visited_cells"] == 4*h+2*k+4*y-g+2*b+38, + "written exact visited-space census") + need(receipt["visited_cells"] <= 6*length+38, "written visited-space bound") + receipt["stencil_bits"] = length + receipt["stencil_canonical_sha256"] = sha256(json.dumps(expected, separators=(",", ":")).encode()).hexdigest() + if consume: + original = stencil.cells[:] + prior_stencil_actions = stencil.actions + counter, mask = machine.transduce(stencil) + expected_bits, old_receipt = adapter.audit(expected, machine) + need(stencil.cells == original and stencil.head == 0 and counter.head == mask.head == 0, + "unchanged consumer protects retained stencil and returns heads") + need(all(x == machine.BLANK for x in counter.cells[1:]), "consumer private cleanup") + bits = "".join(mask.cells[1:-1]) + need(bits == expected_bits, "unchanged consumer complete BAD mask equality") + need(sum(t.actions for t in (stencil, counter, mask)) - prior_stencil_actions == old_receipt["total_cell_head_actions"], + "exact unchanged consumer action invoice") + receipt["consumer"] = {"addresses": len(bits), "good": bits.count("0"), + "mask_sha256": sha256(bits.encode()).hexdigest(), + "prior_consumer_action_formula": old_receipt["total_cell_head_actions"]} + return receipt + + +def rejections(producer, machine): + shapes = ((0, 1, 5, 5, 0, 0), (2, 1, 6, 6, 0, 0), + (2, 2, 5, 5, 0, 0), (1, 1, 5, 5, 1, 0)) + rows = [] + for shape in shapes: + inputs = public_inputs(machine, shape) + before = [t.cells[:] for t in inputs] + allocated = [] + + def fresh(): + t = machine.Tape() + allocated.append(t) + return t + + rejected = False + try: + producer.produce(*inputs, fresh) + except ValueError: + rejected = True + need(rejected, "invalid arithmetic geometry rejected") + need(all(t.head == 0 for t in inputs + tuple(allocated)), "rejected geometry heads returned") + need(all(all(x == machine.BLANK for x in t.cells[1:]) for t in allocated), + "rejected geometry private and output data erased") + need(all(t.cells[:len(old)] == old for t, old in zip(inputs, before)), "reject input protected") + rows.append({"shape": list(shape), "actions": sum(t.actions for t in inputs + tuple(allocated))}) + # Unique LEFT and initially blank tail are infrastructure. These defects + # occur inside that contract: bad data symbol, missing END, END followed + # immediately by a nonblank symbol. + for defect in ("bad_symbol", "missing_end", "nonblank_after_end"): + inputs = public_inputs(machine, (1, 1, 5, 5, 0, 0)) + if defect == "bad_symbol": + inputs[0].cells[1] = "0" + elif defect == "missing_end": + inputs[0].cells[-1] = machine.BLANK + else: + inputs[0].cells.append("1") + before = [t.cells[:] for t in inputs] + allocated = [] + + def fresh(): + t = machine.Tape() + allocated.append(t) + return t + + rejected = False + try: + producer.produce(*inputs, fresh) + except ValueError: + rejected = True + need(rejected and all(t.head == 0 for t in inputs + tuple(allocated)), "grammar defect rejected and heads returned") + need(all(all(x == machine.BLANK for x in t.cells[1:]) for t in allocated), "grammar rejection cleanup") + need(all(t.cells[:len(old)] == old for t, old in zip(inputs, before)), "grammar rejection input protected") + rows.append({"defect": defect, "actions": sum(t.actions for t in inputs + tuple(allocated))}) + return rows + + +def authentication_controls(machine_path, adapter_path): + rows = [] + with tempfile.TemporaryDirectory(prefix="unary-stencil-auth-") as directory: + for name, path, expected in (("machine", machine_path, MACHINE_SHA), + ("adapter", adapter_path, ADAPTER_SHA)): + corrupted = Path(directory) / (name + ".py") + corrupted.write_bytes(path.read_bytes() + b"\nraise RuntimeError('UNAUTHENTICATED_BYTES_EXECUTED')\n") + rejected = False + try: + load("damaged_" + name, corrupted, expected) + except ValueError as exc: + rejected = "authenticated predecessor source" in str(exc) + need(rejected, "damaged source must reject before compile/exec") + rows.append({"source": name, "damaged_bytes_rejected_before_exec": True}) + return rows + + +def controls(producer, machine, adapter): + shape = (1, 2, 5, 7, 1, 1) + g, h, k, y, j, b = shape + expected = [machine.LEFT] + adapter.geometry_stencil(g, h, y, (j,), k, b, machine) + [machine.END] + expected_bits, _ = adapter.audit(expected[1:-1], machine) + rows = [] + for name in ("include_parity", "wrong_lower_pivot", "wrong_upper_pivot", "omit_cleanup", "omit_output_return"): + stencil, receipt, inputs, work = observed_run(producer, machine, shape, {name: True}) + if name in ("include_parity", "wrong_lower_pivot", "wrong_upper_pivot"): + detected = stencil.cells != expected + counter, mask = machine.transduce(stencil) + need("".join(mask.cells[1:-1]) != expected_bits, "semantic mutant must alter actual consumer mask") + elif name == "omit_cleanup": + detected = not receipt["private_blank"] + else: + detected = not receipt["heads_returned"] + need(detected, "named faulty producer unexpectedly accepted: " + name) + rows.append({"mutant": name, "detected": True}) + return rows + + +def guardrail(path): + tree = ast.parse(path.read_text()) + forbidden = {"len", "range", "enumerate", "int", "str", "format", "sum", "min", "max", "pow"} + for node in ast.walk(tree): + if isinstance(node, ast.Call) and isinstance(node.func, ast.Name): + need(node.func.id not in forbidden, "host arithmetic/coordinate primitive") + if isinstance(node, ast.Attribute): + need(node.attr not in ("head", "cells", "reads", "writes", "moves", "actions"), + "producer inspects emulator observer") + need(not isinstance(node, (ast.BinOp, ast.Subscript)), "host arithmetic or indexed geometry") + return "PASS_AST_SCOPE_GUARDRAIL_NOT_A_FORMAL_MACHINE_CERTIFICATE" + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument("--source-dir", type=Path, default=HERE / "source") + parser.add_argument("--consumer-path", type=Path) + parser.add_argument("--output", type=Path) + args = parser.parse_args() + producer = load("unary_producer", HERE / "producer.py") + machine_path = args.consumer_path or args.source_dir / "predecessor_machine.py" + adapter_path = args.source_dir / "predecessor_adapter.py" + machine = load("predecessor_machine", machine_path, MACHINE_SHA) + adapter = load("predecessor_adapter", adapter_path, ADAPTER_SHA) + rows = [] + for g in (1, 2, 3): + for h in (g, g+1): + for k in (g+4, g+5): + for j in (0, 1, 2): + for padding in (0, 1): + for b in (0, 1): + rows.append(case(producer, machine, adapter, (g, h, k, j+k+padding, j, b))) + rows.append(case(producer, machine, adapter, (1, 100, 5, 200, 50, 100))) + consumer_rows = [case(producer, machine, adapter, shape, True) for shape in + ((1, 1, 5, 5, 0, 0), (1, 2, 5, 7, 1, 1), (2, 2, 6, 6, 0, 0), (1, 1, 6, 7, 1, 0))] + result = {"status": "PASS_LITERAL_UNARY_ONE_TARGET_STENCIL_PRODUCER_NO_NEW_KAPPA", + "producer_sha256": sha256((HERE / "producer.py").read_bytes()).hexdigest(), + "predecessor_head": "4f49743a9df0cf7501cdc62bd5707a122fa071e9", + "predecessor_source_sha256": {"machine": MACHINE_SHA, "adapter": ADAPTER_SHA}, + "setup_action_formula": "33H+25K+38Y-6G-J+12B+335 <= 63L+335; L=2H+Y+B", + "setup_visited_space_formula": "4H+2K+4Y-G+2B+38 <= 6L+38", + "cases": rows, "producer_cases": len(rows), + "total_producer_actions": sum(x["actions"] for x in rows), + "consumer_cases": consumer_rows, + "rejections": rejections(producer, machine), + "controls": controls(producer, machine, adapter), + "authentication_controls": authentication_controls(machine_path, adapter_path), + "guardrail": guardrail(HERE / "producer.py"), + "scope": "Canonical unary six-field one-target family only; input encoding and general descriptor production remain unpriced; no complete E evaluator, CRT supplier, precision or kappa claim"} + if args.output is not None: + args.output.write_text(json.dumps(result, indent=2, sort_keys=True) + "\n") + print(result["status"]) + + +if __name__ == "__main__": + main() diff --git a/research/crt-unary-stencil-producer/producer.py b/research/crt-unary-stencil-producer/producer.py new file mode 100644 index 0000000000..dd357a0679 --- /dev/null +++ b/research/crt-unary-stencil-producer/producer.py @@ -0,0 +1,223 @@ +"""Literal fixed-role unary geometry -> one-target dense-guard stencil. + +The program touches tapes only through read/write/move. It never inspects +host lengths, heads, counters, cell lists, geometry integers or coordinates. +The Tape class supplied by the simulator has a permanent LEFT cell. +""" + +LEFT, END, BLANK = "<", ">", "_" +SKIP = ("S", False, False, "0", "0") + + +def rewind(tape): + while tape.read() != LEFT: + tape.move(-1) + + +def empty_word(tape): + tape.move(1) + tape.write(END) + tape.move(-1) + + +def validate(tape): + if tape.read() != LEFT: + raise ValueError("input must enter at permanent LEFT") + tape.move(1) + while True: + symbol = tape.read() + if symbol == END: + # The initially blank tail is part of the tape input contract; + # this checks that END is immediately followed by blank. + tape.move(1) + if tape.read() != BLANK: + raise ValueError("nonblank immediately after unary END") + rewind(tape) + return + if symbol != "1": + raise ValueError("unary input alphabet or missing END") + tape.move(1) + + +def positive(tape): + tape.move(1) + ok = tape.read() == "1" + rewind(tape) + if not ok: + raise ValueError("required positive unary field") + + +def difference(left, right, out): + """Protected unary left-right, rejecting underflow before writing out.""" + left.move(1) + right.move(1) + while True: + symbol = right.read() + if symbol == END: + break + if symbol != "1" or left.read() != "1": + raise ValueError("unary subtraction underflow") + left.move(1) + right.move(1) + out.move(1) + while True: + symbol = left.read() + if symbol == END: + out.write(END) + break + if symbol != "1": + raise ValueError("internal unary subtraction alphabet") + out.write("1") + out.move(1) + left.move(1) + rewind(left) + rewind(right) + rewind(out) + + +def plus_one(source, out): + source.move(1) + out.move(1) + while source.read() == "1": + out.write("1") + source.move(1) + out.move(1) + out.write("1") + out.move(1) + out.write(END) + rewind(source) + rewind(out) + + +def three(out): + out.move(1) + out.write("1") + out.move(1) + out.write("1") + out.move(1) + out.write("1") + out.move(1) + out.write(END) + rewind(out) + + +def skip(source, stencil): + source.move(1) + while source.read() == "1": + stencil.write(SKIP) + stencil.move(1) + source.move(1) + rewind(source) + + +def digit(source, stencil): + source.move(1) + symbol = source.read() + first = True + while symbol == "1": + source.move(1) + symbol = source.read() + stencil.write(("D", first, symbol == END, "0", "0")) + stencil.move(1) + first = False + rewind(source) + + +def leading_guard(source, stencil, first): + source.move(1) + while source.read() == "1": + stencil.write(("G", first, False, "0", "1")) + stencil.move(1) + source.move(1) + first = False + rewind(source) + + +def trailing_guard(source, stencil): + source.move(1) + symbol = source.read() + while symbol == "1": + source.move(1) + symbol = source.read() + stencil.write(("G", False, symbol == END, "0", "0")) + stencil.move(1) + rewind(source) + + +def erase(tape): + rewind(tape) + tape.move(1) + while True: + symbol = tape.read() + tape.write(BLANK) + if symbol == END: + break + tape.move(1) + rewind(tape) + + +def produce(G, H, K, Y, J, B, Tape, include_parity=False, + wrong_lower_pivot=False, wrong_upper_pivot=False, + omit_cleanup=False, omit_output_return=False): + """Six protected canonical unary words -> owned one-target stencil. + + Each input is LEFT, 1^n, END followed by initially blank tail, head LEFT. + On successful validation G>=1,H>=G,K>=G+4,Y>=J+K,J/B>=0. + Eight fixed private unary roles are erased, including every END marker. + Fixed booleans select named mutation programs for verification only. + """ + HG, KG, THREE, A, TAIL, JP, YJ, YJK = ( + Tape(), Tape(), Tape(), Tape(), Tape(), Tape(), Tape(), Tape()) + stencil = Tape() + work = (HG, KG, THREE, A, TAIL, JP, YJ, YJK) + for tape in work: + empty_word(tape) + empty_word(stencil) + try: + for tape in (G, H, K, Y, J, B): + validate(tape) + positive(G) + difference(H, G, HG) + difference(K, G, KG) + three(THREE) + difference(KG, THREE, A) + positive(A) # K-G-3 >= 1, exactly K >= G+4. + plus_one(G, TAIL) + plus_one(J, JP) + difference(Y, J, YJ) + difference(YJ, K, YJK) + stencil.move(1) + skip(HG, stencil) + digit(G, stencil) + skip(HG, stencil) + digit(G, stencil) + skip(YJK, stencil) + if include_parity: + stencil.write(("G", True, False, "0", "0")) + stencil.move(1) + leading_guard(A, stencil, not include_parity) + stencil.write(("G", False, False, + "0" if wrong_lower_pivot else "1", + "0" if wrong_upper_pivot else "1")) + stencil.move(1) + trailing_guard(TAIL, stencil) + skip(J if include_parity else JP, stencil) + skip(B, stencil) + stencil.write(END) + if not omit_output_return: + rewind(stencil) + except ValueError: + # All private words remain complete on every grammar/admission + # rejection. Input values are never written in either branch. + for tape in work: + erase(tape) + erase(stencil) + for tape in (G, H, K, Y, J, B): + rewind(tape) + raise + if not omit_cleanup: + for tape in work: + erase(tape) + for tape in (G, H, K, Y, J, B): + rewind(tape) + return work, stencil