From 2a3768e0878389851921ab05598b5d685c859701 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Thu, 29 Oct 2026 13:22:35 +0000 Subject: [PATCH 1/2] feat(research): add a paid arbitrary-bit Sandwich boundary --- research/arbitrary-bit-sandwich/PROOF.md | 148 ++++++ research/arbitrary-bit-sandwich/README.md | 137 ++++++ research/arbitrary-bit-sandwich/SOURCES.json | 467 +++++++++++++++++++ research/arbitrary-bit-sandwich/TASK.json | 91 ++++ research/arbitrary-bit-sandwich/VERIFY.json | 108 +++++ research/arbitrary-bit-sandwich/boundary.py | 178 +++++++ research/arbitrary-bit-sandwich/verify.py | 346 ++++++++++++++ 7 files changed, 1475 insertions(+) create mode 100644 research/arbitrary-bit-sandwich/PROOF.md create mode 100644 research/arbitrary-bit-sandwich/README.md create mode 100644 research/arbitrary-bit-sandwich/SOURCES.json create mode 100644 research/arbitrary-bit-sandwich/TASK.json create mode 100644 research/arbitrary-bit-sandwich/VERIFY.json create mode 100644 research/arbitrary-bit-sandwich/boundary.py create mode 100644 research/arbitrary-bit-sandwich/verify.py diff --git a/research/arbitrary-bit-sandwich/PROOF.md b/research/arbitrary-bit-sandwich/PROOF.md new file mode 100644 index 0000000000..0d8f6844f5 --- /dev/null +++ b/research/arbitrary-bit-sandwich/PROOF.md @@ -0,0 +1,148 @@ +# Conditional arbitrary-bit boundary construction + +This is the correctness and payment argument for the new wrapper in +`boundary.py`. It uses the completed Sandwich interface of JoyboyBrian's +PR5095 and implements the released handoff in Discussion3664. The handoff's +representation calculation is predecessor work. No production recovery or +multiplication theorem is established here. + +## Preconditions and promised return + +Let n,b be positive integers represented by canonical independent Count +tapes. First, second and catalogue are three further distinct borrowed Tape +ports, disjoint from every boundary and child resident tape. Both operands +contain exactly n binary cells followed by BLANK, after a LEFT marker. +Their values x,y lie in [0,2^n); leading zeroes are allowed. Input heads are +at their canonical first-cell positions. Arbitrary incoming head positions +are outside this contract. The catalogue remains a child-admission input. + +The child is idle with no pending return. For positive q,b and two complete +qb-bit packed operands, its successful production call returns exactly 2qb +MSB-first bits for their exact integer product. Its returned Tape is borrowed +until `consume`, which clears the body and owned marker. It preserves its +borrowed ports, returns their heads canonically, and closes its own work. +A failed child call must also close its work and preserve the borrowed ports. +The child retains every analytic/catalogue/native precondition for recovery. +These are interface premises, not claims proved by wrapper tests. + +The wrapper's successful return is exactly 2n MSB-first bits representing xy. +It preserves the five borrowed ports and their canonical heads. Its two packed +banks and metadata leases are erased. Its own return stays protected until +the caller invokes `consume`, after which its body and marker are erased. + +## Encoded parameter and representation argument + +The retained exact `divide(n,b)` returns quotient a and remainder r with +n=ab+r and 0<=r0]. Its exact product and +subtraction operations compute d=qb-n, so 0<=d=1. No input Count +is converted into a host integer. + +Validation reads exactly n symbols and then requires BLANK. Reversing those +n MSB-first bits puts bit i of x at packed position i for 0<=i> i) & 1 for i in reversed(range(width))) + + +def meters(tapes): + return tuple(sum(getattr(t.meter, field) for t in tapes) + for field in ("reads", "writes", "moves")) + + +def difference(after, before): + return tuple(a - b for a, b in zip(after, before)) + + +class FixtureChild: + """An exact child oracle whose run is excluded and consume is charged. + + Host integers and direct tape inspection here are test-oracle work only. + The real boundary never receives these integers or the oracle object state. + """ + + def __init__(self, api, n, b, x, y): + self.api = api + q = (n + b - 1) // b + self.expected = tuple(bits(v, n)[::-1] + bytes(q*b-n) for v in (x, y)) + self.product = bits(x*y, 2*q*b) + self.b, self.q = api.Count.literal(b), api.Count.literal(q) + self.output = api.Tape() + api.erase_marker(self.output) + self.private = (self.output, self.b.tape, self.q.tape) + self.closed, self.pending = True, False + self.calls = self.consumed = 0 + self.work = (0, 0, 0) + self.observed = () + self.mode = "ok" + + def run(self, first, second, catalogue, b, q): + before = meters(self.observed) + self.calls += 1 + try: + need(self.closed and not self.pending, "fixture child idle") + need(self.api.compare(b, self.b) == self.api.compare(q, self.q) == 0, + "actual encoded child shape") + need(tuple(self.api.packet_bytes(t) for t in (first, second)) == self.expected, + "actual packed operand direction and padding") + if self.mode == "raise": + raise ValueError("injected completed child failure") + self.api.initialize_marker(self.output) + raw = self.product + if self.mode == "prefix": + raw = bytes([1]) + raw[1:] + elif self.mode == "short": + raw = raw[:-1] + elif self.mode == "extra": + raw += bytes([0]) + elif self.mode == "symbol": + raw = raw[:-1] + bytes([self.api.RIGHT]) + for bit in raw: # At most 129 fixed fixture cells. + self.output.append(bit) + self.output.rewind() + self.pending = True + return self.output + finally: + delta = difference(meters(self.observed), before) + self.work = tuple(a+b for a, b in zip(self.work, delta)) + + def consume(self): + need(self.pending, "fixture pending return") + self.output.clear() + self.api.erase_marker(self.output) + self.pending = False + self.consumed += 1 + + +def prepare(api, n, b, x, y): + child = FixtureChild(api, n, b, x, y) + wrapper = api.ArbitraryBits(child) + ports = [api.tape(bits(x, n)), api.tape(bits(y, n)), api.tape(bytes([1]))] + counts = api.Count.literal(n), api.Count.literal(b) + tapes = (*wrapper.private, *ports, *(c.tape for c in counts)) + need(len({id(t) for t in tapes}) == len(tapes), "independent fixture inventory") + child.observed = tapes + return SimpleNamespace(child=child, wrapper=wrapper, ports=ports, counts=counts, + tapes=tapes, n=n, b=b, x=x, y=y) + + +def idle(case): + w, child = case.wrapper, case.child + need(w.closed and not w.pending and not w.pool.live, "idle complete boundary") + need(child.closed and not child.pending, "child return released") + for tape in (*w.resident, child.output): + need(tape.head == 1 and all(v == case.child.api.BLANK for v in tape.cells), + "erased resident body, marker and canonical head") + + +def successful(api, case): + w, child = case.wrapper, case.child + snapshots = [(bytes(t.cells), t.head) for t in (*case.ports, *(c.tape for c in case.counts))] + before, prior_work = meters(case.tapes), child.work + with api.no_decode(): + result = w.run(*case.ports, *case.counts) + run_delta = difference(meters(case.tapes), before) + child_delta = difference(child.work, prior_work) + own_delta = difference(run_delta, child_delta) + need(all(x >= 0 for x in own_delta), "nonnegative complete boundary tariff") + need(api.packet_bytes(result) == bits(case.x*case.y, 2*case.n), + "exact 2n-bit integer product with leading zeroes") + need([(bytes(t.cells), t.head) for t in (*case.ports, *(c.tape for c in case.counts))] + == snapshots, "all five borrowed ports preserved") + before_consume = meters(case.tapes) + w.consume() + consumption = difference(meters(case.tapes), before_consume) + idle(case) + return tuple(a+b for a, b in zip(own_delta, consumption)) + + +def reject_case(api, case, message, preflight=False): + before = [(bytes(t.cells), t.head) for t in case.tapes] + try: + with api.no_decode(): + case.wrapper.run(*case.ports, *case.counts) + except ValueError as error: + need(message in str(error), "expected rejection: " + str(error)) + else: + raise ValueError("missing rejection: " + message) + if preflight: + need([(bytes(t.cells), t.head) for t in case.tapes] == before, + "preflight rejection preserves physical state") + else: + idle(case) + + +def return_controls(api): + checks = [] + messages = {"prefix": "zero discarded", "short": "binary product extent", + "extra": "extra product", "symbol": "binary product extent", + "raise": "injected completed"} + for mode, message in messages.items(): + case = prepare(api, 5, 3, 29, 23) + case.child.mode = mode + reject_case(api, case, message) + need(case.child.calls == 1 and case.child.consumed == int(mode != "raise"), + "failed output validation consumes every completed child return") + case.child.mode = "ok" + successful(api, case) + checks.append(mode) + return checks + + +def input_controls(api): + checks = [] + for raw, message in [(bytes([1, 0]), "binary input extent"), + (bytes([1, 0, 1, 0, 1, 0]), "extra input"), + (bytes([1, api.RIGHT, 0, 1, 0]), "binary input extent")]: + for port in (0, 1): + case = prepare(api, 5, 3, 29, 23) + original = case.ports[port] + case.ports[port] = api.tape(raw) + reject_case(api, case, message) + need(case.child.calls == 0, "validate both operands before child entry") + case.ports[port] = original + successful(api, case) + checks.append((list(raw), port)) + for zero in (0, 1): + case = prepare(api, 5, 3, 29, 23) + values = list(case.counts) + values[zero] = api.Count.literal(0) + case.counts = tuple(values) + reject_case(api, case, "positive cardinality") + need(case.child.calls == 0, "zero parameter never reaches the child") + checks.append(("zero", zero)) + return checks + + +def ownership_controls(api): + checks = [] + for destination in (1, 2): + case = prepare(api, 5, 3, 29, 23) + case.ports[destination] = case.ports[0] + reject_case(api, case, "five distinct", True) + checks.append(("payload_alias", destination)) + for port in (0, 1, 2): + for count in (0, 1): + case = prepare(api, 5, 3, 29, 23) + case.counts[count].tape = case.ports[port] + reject_case(api, case, "five distinct", True) + checks.append(("metadata_alias", port, count)) + for slot in (0, 32, 34, 35): + case = prepare(api, 5, 3, 29, 23) + case.ports[0] = case.wrapper.private[slot] + reject_case(api, case, "external boundary", True) + checks.append(("private_alias", slot)) + case = prepare(api, 5, 3, 29, 23) + case.wrapper.run(*case.ports, *case.counts) + for _ in range(2*case.n): + case.wrapper.output.step(1) + reject_case(api, case, "consume prior boundary", True) + case.wrapper.consume() + successful(api, case) + checks.append(("pending_return_at_end",)) + try: + case.wrapper.consume() + except ValueError as error: + need("pending boundary" in str(error), "double consume rejected") + else: + raise ValueError("double consume accepted") + checks.append(("double_consume",)) + return checks + + +def positive_cases(api): + transcript = sha256() + count = partial = 0 + max_peak = 0 + demonstration = None + shapes = [(n, b, x, y) for n in range(1, 5) for b in range(1, 6) + for x in range(1 << n) for y in range(1 << n)] + for n in (5, 9, 17, 31, 32, 33): + for b in (1, 2, 3, 7, 8, 16): + top = (1 << n)-1 + for x, y in ((0, top), (1, top), (top, top), (top//3, top//5)): + shapes.append((n, b, x, y)) + shapes.append((5, 3, 29, 23)) + need(len(shapes) <= 2048, "bounded complete positive fixture list") + for n, b, x, y in shapes: + case = prepare(api, n, b, x, y) + tariff = successful(api, case) + transcript.update(json.dumps([n, b, x, y, tariff]).encode()+b"\n") + count += 1 + partial += int(n % b != 0) + max_peak = max(max_peak, case.wrapper.pool.peak) + if (n, b, x, y) == (5, 3, 29, 23): + demonstration = dict(n=n, b=b, q=2, padding=1, x=x, y=y, product=x*y, + packed=[list(s) for s in case.child.expected], + output=list(bits(x*y, 2*n)), + tariff=dict(zip(("reads", "writes", "moves"), tariff)), + scratch_peak=case.wrapper.pool.peak) + return dict(cases=count, nonmultiple_shapes=partial, scratch_peak=max_peak, + transcript_sha256=transcript.hexdigest(), demonstration=demonstration) + + +def actual_child_policy(api): + from crt_converter import Converter + from sandwich import Sandwich + from tensor_engine import Tensor + from tensor_fixture import finite_chirp, literal_native + from tensor_router import FullRouter + child = Sandwich(Tensor(finite_chirp(), FullRouter(literal_native())), + Converter(FullRouter(literal_native()))) + wrapper = api.ArbitraryBits(child) + raw = (ROOT / "research/physical-tensor-crt-sandwich-recovery/inputs/p48-5x7.bin").read_bytes() + ports = [api.tape(bits(29, 17)), api.tape(bits(23, 17)), api.tape(raw)] + case = SimpleNamespace(child=child, wrapper=wrapper, ports=ports, + counts=(api.Count.literal(17), api.Count.literal(8))) + try: + with api.no_decode(): + wrapper.run(*case.ports, *case.counts) + except ValueError as error: + need("production coefficient/locality contract required" in str(error), + "the actual child's production guard remains mandatory") + else: + raise ValueError("reduced catalogue admitted production recovery") + need(wrapper.closed and not wrapper.pending and not wrapper.pool.live, + "actual-child policy rejection cleans boundary") + need(child.closed and not child.pending and not child.pool.live, + "actual child cleans its own failed entry") + for tape in wrapper.resident: + need(tape.head == 1 and all(v == api.BLANK for v in tape.cells), + "actual-child failure erases every boundary role") + return dict(recovery_policy="mandatory production admission", payload_executed=False) + + +def run(): + inputs = authenticate() + sys.path[:0] = [str(HERE), str(ROOT / "research/physical-tensor-crt-sandwich-recovery")] + from sandwich_sources import opened + with opened(): + from boundary import ArbitraryBits + from cardinal_counts import Count + from check_support import no_decode + from encoded import compare + from expansion_check_block import packet_bytes + from records import Tape + from ring_check_words import tape + from session import erase_marker, initialize_marker + from words import BLANK, RIGHT + api = SimpleNamespace(ArbitraryBits=ArbitraryBits, Count=Count, + no_decode=no_decode, compare=compare, + packet_bytes=packet_bytes, Tape=Tape, tape=tape, + erase_marker=erase_marker, + initialize_marker=initialize_marker, + BLANK=BLANK, RIGHT=RIGHT) + result = positive_cases(api) + result["return_controls"] = return_controls(api) + result["input_controls"] = input_controls(api) + result["ownership_controls"] = ownership_controls(api) + result["actual_child"] = actual_child_policy(api) + result["inputs_authenticated"] = inputs + result["claim_type"] = "scoped caller construction under a completed-child contract" + result["tariff_scope"] = "All wrapper work and both return consumptions; only child.run is excluded. Host oracle/output inspection is excluded." + result["package_sha256"] = {p.name: sha256(p.read_bytes()).hexdigest() + for p in sorted(HERE.iterdir()) if p.is_file()} + print(json.dumps(result, sort_keys=True)) + print("PASS_ARBITRARY_BIT_SANDWICH") + + +if __name__ == "__main__": + run() From 9ef83f675cb193d9f7a3fddb4cd452b12398c08b Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Thu, 29 Oct 2026 13:25:36 +0000 Subject: [PATCH 2/2] fix(research): declare the Sandwich catalogue replay input --- research/arbitrary-bit-sandwich/README.md | 2 +- research/arbitrary-bit-sandwich/SOURCES.json | 6 ++++++ research/arbitrary-bit-sandwich/VERIFY.json | 1 + 3 files changed, 8 insertions(+), 1 deletion(-) diff --git a/research/arbitrary-bit-sandwich/README.md b/research/arbitrary-bit-sandwich/README.md index 97177fe942..5005807688 100644 --- a/research/arbitrary-bit-sandwich/README.md +++ b/research/arbitrary-bit-sandwich/README.md @@ -78,7 +78,7 @@ is executed. Positive child fixtures are explicitly supplied exact oracles; their host arithmetic is outside the charged wrapper. [SOURCES.json](SOURCES.json) binds canonical main -`3f0152a32eeebac0df11946dbd50cabe5a7f7839`, the original task card and all 73 +`3f0152a32eeebac0df11946dbd50cabe5a7f7839`, the original task card and all 74 runtime/source inputs. The predecessor's scientific verifier is not run. The selected baseline control reports `PASS_RESEARCH_BASELINE_BINDINGS_ONLY` with selected kappa `781451/250000000`; that control authenticates metadata. diff --git a/research/arbitrary-bit-sandwich/SOURCES.json b/research/arbitrary-bit-sandwich/SOURCES.json index 46452b0d00..351388ae88 100644 --- a/research/arbitrary-bit-sandwich/SOURCES.json +++ b/research/arbitrary-bit-sandwich/SOURCES.json @@ -428,6 +428,12 @@ "git_blob": "f66fe12d581eb5410e097331d8a4f2b18c8f901c", "sha256": "a27cf9d637009403d3ab1e766590ef1bc6db8fdc364dfab3bfe0b76e5c8f8354" }, + { + "path": "research/physical-tensor-crt-sandwich-recovery/inputs/p48-5x7.bin", + "usage": "input", + "git_blob": "5c420cc4aecc15c74cc37011866ab5719c441e85", + "sha256": "7dd7adbe9e8f6d5ffbecd425a72827b31d7222ee51bcd67a4148ebfd03420381" + }, { "path": "research/physical-tensor-crt-sandwich-recovery/sandwich.py", "usage": "input", diff --git a/research/arbitrary-bit-sandwich/VERIFY.json b/research/arbitrary-bit-sandwich/VERIFY.json index 42acc68f9e..40c579f486 100644 --- a/research/arbitrary-bit-sandwich/VERIFY.json +++ b/research/arbitrary-bit-sandwich/VERIFY.json @@ -73,6 +73,7 @@ "research/physical-gaussian-tensor/tensor_word.py", "research/physical-gaussian-tensor/verify.py", "research/physical-tensor-crt-sandwich-recovery/SOURCES.json", + "research/physical-tensor-crt-sandwich-recovery/inputs/p48-5x7.bin", "research/physical-tensor-crt-sandwich-recovery/sandwich.py", "research/physical-tensor-crt-sandwich-recovery/sandwich_sources.py", "upstream/build/sections/07-resampling.tex",