From e8bdf35809eecfb0b8db7b5e141cb1ba0f4f6a1c Mon Sep 17 00:00:00 2001 From: JoyboyBrian Date: Thu, 22 Oct 2026 12:08:00 -0700 Subject: [PATCH] Execute a uniform ROM query from encoded binary parameters --- research/crt-uniform-rom-query/FIXTURE.json | 61 ++++++ research/crt-uniform-rom-query/PROOF.md | 204 +++++++++++++++++++ research/crt-uniform-rom-query/README.md | 123 +++++++++++ research/crt-uniform-rom-query/RESULT.json | 84 ++++++++ research/crt-uniform-rom-query/SOURCES.json | 18 ++ research/crt-uniform-rom-query/TASK.json | 94 +++++++++ research/crt-uniform-rom-query/VERIFY.json | 18 ++ research/crt-uniform-rom-query/machine.py | 215 ++++++++++++++++++++ research/crt-uniform-rom-query/verify.py | 196 ++++++++++++++++++ 9 files changed, 1013 insertions(+) create mode 100644 research/crt-uniform-rom-query/FIXTURE.json create mode 100644 research/crt-uniform-rom-query/PROOF.md create mode 100644 research/crt-uniform-rom-query/README.md create mode 100644 research/crt-uniform-rom-query/RESULT.json create mode 100644 research/crt-uniform-rom-query/SOURCES.json create mode 100644 research/crt-uniform-rom-query/TASK.json create mode 100644 research/crt-uniform-rom-query/VERIFY.json create mode 100644 research/crt-uniform-rom-query/machine.py create mode 100644 research/crt-uniform-rom-query/verify.py diff --git a/research/crt-uniform-rom-query/FIXTURE.json b/research/crt-uniform-rom-query/FIXTURE.json new file mode 100644 index 0000000000..dd73396152 --- /dev/null +++ b/research/crt-uniform-rom-query/FIXTURE.json @@ -0,0 +1,61 @@ +{ + "source_pr": 4739, + "source_commit": "26ccde014218f7d906d1251dc295fbc1437ede8a", + "source_result_path": "research/crt-transported-key-tape/RESULT.json", + "source_result_sha256": "d05f73929b4f3b396a37736b98bd27d7c7a4018fbe878cc6929c1d175972ada1", + "rom_bit_bytes_sha256": "bc0ab563e6d8fdfa24ee89b50dbe3f9a3a6f23681f491e883c6b5aeef07d4104", + "h": 5, + "s": 17, + "rom": "0000000000000000000000000000000000010001000100010001000100000000001100110011001100100010000000000111011101110111010001000000000011111111111111111000100000000000111111111110111000000000000000001110111011001100000000000000000011001100100010000000000000000000100010000000000000000000000000000000000000010001000100010000000000010001001100110010001000000000001100110111011101000100000000000111011111111111100010000000000011111111111111110000000000000000111011101110111000000000000000001100110011001100000000000000000010001000100010000000000000000000", + "witnesses": [ + { + "input": [ + 0, + 1, + 4 + ], + "queries": [ + { + "offset": 5, + "target": 0, + "bit": 1 + }, + { + "offset": 4, + "target": 20, + "bit": 1 + }, + { + "offset": 4, + "target": 20, + "bit": 1 + } + ] + }, + { + "input": [ + 1, + 1, + 4 + ], + "queries": [ + { + "offset": 5, + "target": 0, + "bit": 1 + }, + { + "offset": 5, + "target": 0, + "bit": 1 + }, + { + "offset": 4, + "target": 20, + "bit": 1 + } + ] + } + ], + "boundary": "Derived fixed ROM/input fixture; ROM compiler and source-key adapter are external, not invoked by this query machine." +} diff --git a/research/crt-uniform-rom-query/PROOF.md b/research/crt-uniform-rom-query/PROOF.md new file mode 100644 index 0000000000..63b0551a77 --- /dev/null +++ b/research/crt-uniform-rom-query/PROOF.md @@ -0,0 +1,204 @@ +# Uniform encoded row-ROM query + +JoyboyBrian, with substantial OpenAI Codex assistance. Apache-2.0. +This is a scoped proof for `machine.py`, not a proof of the CRT compiler or its +complete `E(p,ell)` allowance. The finite replay is a check on this proof's +implementation, not the reason its quantified statements hold. + +## Interface and quantified proposition + +There are ten semi-infinite tapes, all heads initially at cell zero. Borrowed +roles are `h,s,offset,target,rom`; owned roles are `out,count,col,row,limit`. +Owned tapes are initially blank. A borrowed record has exactly one left marker +`L` at zero, a finite payload of `0,1` symbols, then `R` and blank cells. This +framing is the input contract, not an admission check for arbitrary unframed +infinite tapes. Malformed finite parameter payloads are also checked in the +replay, provided they contain no additional `L` or `R` markers. + +Integers use little-endian binary with no most-significant zero, except that +zero is the single digit `0`. Let + +- `h >= 1`, `2 <= s <= 2^h`, `0 <= offset < s`, `0 <= target < 2^h`; +- `M = s*2^h`, and let the ROM payload be any word of exactly `M` bits; +- `b = bit_length(s)` and `w = h+b+2` (so `w >= 5`). + +The *same* assembled program accepts, returns the bit at zero-based ROM index +`offset*2^h+target` in the owned record `L bit R`, preserves all borrowed cells, +erases all four scratch tapes including their markers, and returns all ten heads +to zero. Its complete instruction count is at most + +`T <= 512*(M+1)*w^2`. + +A fixed three-bit encoding of the five tape symbols gives the binary-action +upper bound + +`T_binary <= 65536*(M+1)*(h+log2(s)+1)^2`. + +The executed object is the marker-alphabet program. The binary bound is the +explicit local lowering proved below, not a measured binary emulator result. + +Incorrect finite parameter records, out-of-range parameters, non-bit ROM +payloads, and short/long ROMs are rejected with owned tapes blank and all heads +returned. The displayed bound is for legal parameters and a correctly sized ROM; +there is deliberately no bound independent of the length of malformed headers. +For example, an arbitrarily long noncanonical header cannot be validated for a +cost depending only on its small decoded value. + +## Fixed program and finite control + +`assemble()` takes no arguments. Its only Python loops range over a fixed list +of role names. It always emits the same 752 instructions and fixed jump targets. +The 16 registers hold a current symbol, a comparison result, or a Boolean. None +holds an unbounded integer. The instruction set has reads, writes, unit moves, +finite-alphabet equality, Boolean branch, finite-register set/copy, jump and +halt. Every one of these instructions contributes one to the reported census; +equality and its subsequent branch are separate instructions. + +The host interpreter's `pc`, tape-head coordinates, dictionary keys and census +are simulation metadata. The program has no instruction to inspect those +integers, array lengths, the trace, or a host-decoded input value. A head is used +only for its current cell. Branches use only a Boolean equality result. The +observer watchdog can abort a test; it cannot select an answer or certify a +partly executed query. Thus the program and the proof are independent of the +watchdog, interpreter memory allocation, Python timing and test-oracle decoding. + +## Functional invariants and termination + +`canonical` scans to `R`, requires at least one binary digit, and remembers +whether there was more than one digit. The final digit must be `1` unless there +was just one digit. These are finite flags. `is_zero(h)` rejects zero, and +canonical `s` has value at least two exactly when it has at least two digits. +All these scans return their head. + +`copy_word` copies the complete encoded `h` to `count`, including its fixed +width. In `width_loop`, `count` is tested for zero and decremented bitwise once +per iteration. Leading zeroes created in this *private* countdown are retained. +The decrement routine is called only on a positive value: change low zeroes to +ones, change the first one to zero, and rewind. Hence it terminates without +crossing `R`, and there are **exactly h iterations**, despite h arriving in +binary. Each iteration appends one zero to `col` and `limit`. On termination, +`col` is an h-bit zero and `limit` is h zeroes followed by one, the encoding of +`2^h`. No host-sized h controls allocation or this loop. + +`compare` scans both words from their least-significant digits, pads a word by +zero after its `R`, and replaces its comparison flag whenever the current digits +differ. The highest differing bit determines unsigned order. It stops when both +heads are at `R`, then rewinds both. Thus the three comparisons establish +`s <= 2^h`, `offset < s`, and `target < 2^h` without decoding a parameter. The +row counter is initialized to exactly b zeroes by traversing `s`. + +Before ROM position j, the invariant is + +`row = floor(j/2^h)`, `col = j mod 2^h`. + +The h-bit column increment returns a carry exactly on wraparound. On carry, +the b-bit row increment runs. Until j=M, row <= s < 2^b, so row never overflows. +The endpoint **s=2^h** is included: then **b=h+1**, leaving room for the terminal +row value s. This extra bit is not discarded. + +Before consuming a ROM bit, the program rejects if row=s. At each legal +position it compares row with offset and col with target; their simultaneous +match occurs exactly once, at j=offset*2^h+target. Only that bit is written to +`out`; `found` rejects an unexpected second match. At `R`, col must be zero, +row must equal s and `found` must be set. Thus short and long ROMs are rejected, +and the accepted output is the claimed bit. Every ROM symbol is read, with no +random lookup or multiplication of decoded indices. + +All rejection paths enter the same cleanup after the scratch/output records +have been initialized. Scratch records always have a finite right marker; +clear scans to it, overwrites every visited cell and the right marker with +blank, rewinds to the left marker, then erases it. Borrowed roles are never +written. Their unique left marker makes rewind terminate. On rejection the +output record is erased in the same way; on acceptance its head already is zero. +No early return bypasses cleanup. + +On legal inputs the four private tapes occupy exactly +`bit_length(h)+2h+b+9` cells including their eight markers; the owned output +uses three more cells. This is O(h+log s) private space, with ten tape roles +and sixteen finite-control registers independent of every parameter. There +is no copy of the ROM. All occupied private cells return to blank. + +## Static instruction charging + +The following bounds come from the emitted instruction paths, not from sampled +maxima. Let d be a payload length, or the maximum of the two lengths for compare. +A head may start at its right marker for rewind. Each table entry includes all +branch tests, branches, jumps and final rewind operations. + +| Routine | Repeated path and its number of iterations | Upper bound | +| --- | --- | ---: | +| rewind | each non-L cell: read, eq, branch, move, jump; <=d+1 iterations; final read/eq/branch | 5d+8 | +| canonical | <=11 instructions per digit; finite last-digit checks; one rewind | 32(d+1) | +| copy_word | <=7 per digit, terminal branch/write, two rewinds | 32(d+1) | +| is_zero | <=8 per digit, terminal branch, one rewind | 16(d+1) | +| decrement | <=6 per borrowed zero, one terminating bit update, one rewind | 16(d+1) | +| increment | <=8 per propagated one, terminal zero/overflow path, one rewind | 16(d+1) | +| compare | <=32 per paired/padded digit, <=6 terminal instructions, two rewinds | 64(d+1) | +| clear (starting at L) | <=6 per digit, terminal marker erasure, rewind, erase L | 16(d+1) | + +All admitted parameter/counter words have length <=w-1: +`bit_length(h)<=h`, `b<=h+1`, `bit_length(offset)<=b`, +`bit_length(target)<=h`, and `limit` has h+1 digits. In each width-loop +iteration, the zero test and decrement use at most 32w instructions together; +append/branch/jump uses at most nine more, hence at most 40w. Its h iterations +cost at most 40w^2; its final zero test is separate. + +For clarity, deliberately rounded phase bounds are: + +- **Startup <=256w^2.** The four canonical scans cost <=128w, the first h zero + test <=16w, h copy <=32w, final countdown test <=16w, three range comparisons + <=192w, row initialization <=32w, and terminal column/limit rewinds <=10w. + The s-length head return costs <=5w. All remaining initialization, branch, + append termination and finite s-length tests cost <=96. Together with 40w^2 + this is <=40w^2+431w+96, which is <256w^2 for + w>=5. The `h` countdown cost is explicitly present. +- **One ROM-bit iteration <=256w.** There are three comparisons (row/s, + row/offset, col/target) costing <=192w; column and optional row increment + cost <=32w; remaining tests, saved finite flags, selected-bit output, movement + and jumps cost <=40. Since w>=5, the sum is <=256w. +- **Finishing <=256w+8M.** The column zero test and row/s comparison cost <=80w. + Four scratch rewinds/clears cost <=128w, four parameter rewinds <=20w, the + ROM rewind costs 5M+8, and the remaining branch/status/halt steps fit in + 28w+3M-8. On an accepted execution no output erase is needed. + +Thus `T <=256w^2+256Mw+256w+8M`. For w>=5 this is smaller than +`512(M+1)w^2`. The constant is intentionally loose; no measured case is used in +this inequality. Rejection cleanup is verified and terminates, but rejection +cost is not silently included in the legal-input bound. + +## Fixed binary lowering + +Encode `_`, `L`, `R`, `0`, `1` respectively as `000`, `001`, `010`, `100`, `101` +on each of the ten binary tapes, whose blank background is zero. A logical +head at cell j is represented by a physical head at 3j. The finite registers +and the 752 instruction addresses are part of the fixed finite control; their +number does not grow with h, s or M. + +A symbol read reads three bits, uses four unit moves to visit them and return, +and retains the three bits in finite control. A symbol write writes three bits +with the same four moves. One logical move is three physical unit moves. +An equality of three-bit symbol codes needs at most three XORs, two ORs and one +NOT; a register assignment copies/sets at most three bits. A Boolean branch, +jump or halt is a fixed control transition. Charging the associated local +sequencing and bit decisions as well, **32 binary read/write/move/Boolean/control +actions per marker-alphabet instruction** is a common upper bound (the largest +listed data-access path uses fewer than 16). No decoded multi-bit integer, +unbounded arithmetic, address multiplication or variable lookup is introduced. +This is a constant-state local compilation, so concatenating it over the entire +executed program gives `T_binary<=32T`. Initial encoded packets/ROM are supplied; +converting an external representation to those packets is outside this theorem. + +Write q=h+log2(s)+1. Since b<=log2(s)+1 and q>=3, w<=q+2<=2q. Consequently +`32*512*(M+1)*w^2 <=65536*(M+1)*q^2`. + +## Caller and remaining costs + +For PR4739 the row-query parameters are h=5,s=17, with the 544-bit ROM retained +in `FIXTURE.json`. Its two transported witnesses use query sequences +`(offset,target)=(5,0),(4,20),(4,20)` and `(5,0),(5,0),(4,20)` respectively. +The component returns the same six source bits. The caller must still serialize +its computed descriptor/offset into this canonical interface, pay for ROM +construction and CRT reconstruction, and account for three invocations plus +its remaining key/repair work. This package does not execute that adapter or +replace the entire predecessor key. Its different instruction model must not +be subtracted from PR4739's read/write/move-only census as a speedup claim. diff --git a/research/crt-uniform-rom-query/README.md b/research/crt-uniform-rom-query/README.md new file mode 100644 index 0000000000..286b4fa03c --- /dev/null +++ b/research/crt-uniform-rom-query/README.md @@ -0,0 +1,123 @@ +# Uniform ROM query from encoded parameters + +One fixed 752-instruction, ten-tape program now reads binary `h,s,offset,target`, +validates their relations, scans an externally supplied row ROM, returns its +selected bit, erases private scratch and returns every head. Neither a decoded +parameter nor a host loop index is available to its finite control. + +For **every** h>=1, 2<=s<=2^h, offset=1, 2<=s<=2^h, offset') + self.mark(equal); self.branch('a', 'R', advance, moveleft) + self.mark(moveleft); self.emit('move', left, 1) + self.mark(advance); self.branch('b', 'R', loop, moveright) + self.mark(moveright); self.emit('move', right, 1); self.emit('jump', loop) + self.mark(end); self.rewind(left); self.rewind(right) + def finish(self): + resolved = [] + for op, *args in self.code: + if op == 'jump': args[0] = self.labels[args[0]] + if op == 'branch': args[1], args[2] = self.labels[args[1]], self.labels[args[2]] + resolved.append((op, *args)) + return tuple(resolved) + +def assemble(): + b = Builder(); e = b.emit + reject, cleanup, accept = 'reject', 'cleanup', 'accept' + for tape in PRIVATE: b.init(tape) + b.init('out'); e('move', 'out', 1); e('write', 'out', '0') + e('move', 'out', 1); e('write', 'out', 'R'); b.rewind('out') + for tape in ('h', 's', 'offset', 'target'): b.canonical(tape, reject) + b.is_zero('h'); b.branch('zero', '1', reject, 'h_positive'); b.mark('h_positive') + # Canonical s has at least two digits iff s >= 2. + e('move', 's', 1); e('move', 's', 1); e('read', 's', 'scan') + b.branch('scan', 'R', reject, 's_at_least_two'); b.mark('s_at_least_two'); b.rewind('s') + b.copy_word('h', 'count'); e('move', 'col', 1); e('move', 'limit', 1) + b.mark('width_loop'); b.is_zero('count'); b.branch('zero', '1', 'width_done', 'width_more') + b.mark('width_more') + for tape in ('col', 'limit'): + e('write', tape, '0'); e('move', tape, 1); e('write', tape, 'R') + b.decrement('count'); e('jump', 'width_loop') + b.mark('width_done'); e('write', 'limit', '1'); e('move', 'limit', 1); e('write', 'limit', 'R') + b.rewind('limit'); b.rewind('col') + b.compare('s', 'limit'); b.branch('cmp', '>', reject, 's_fits'); b.mark('s_fits') + b.compare('offset', 's'); b.branch('cmp', '<', 'offset_fits', reject); b.mark('offset_fits') + b.compare('target', 'limit'); b.branch('cmp', '<', 'target_fits', reject); b.mark('target_fits') + b.copy_word('s', 'row', zeros=True) + e('set', 'found', '0'); e('move', 'rom', 1) + b.mark('scan_loop'); e('read', 'rom', 'rombit') + b.branch('rombit', 'R', 'scan_done', 'rom_not_end') + b.mark('rom_not_end'); b.branch('rombit', '0', 'rom_bit', 'rom_maybe_one') + b.mark('rom_maybe_one'); b.branch('rombit', '1', 'rom_bit', reject) + b.mark('rom_bit'); b.compare('row', 's'); b.branch('cmp', '=', reject, 'row_room'); b.mark('row_room') + b.compare('row', 'offset'); e('copy', 'cmp', 'rowmatch'); b.compare('col', 'target') + b.branch('rowmatch', '=', 'maybe_hit', 'after_hit'); b.mark('maybe_hit') + b.branch('cmp', '=', 'hit', 'after_hit'); b.mark('hit') + b.branch('found', '1', reject, 'first_hit'); b.mark('first_hit') + e('set', 'found', '1'); e('move', 'out', 1); e('write_reg', 'out', 'rombit'); e('move', 'out', -1) + b.mark('after_hit'); b.increment('col'); b.branch('carry', '1', 'next_row', 'next_bit') + b.mark('next_row'); b.increment('row'); b.branch('carry', '1', reject, 'next_bit') + b.mark('next_bit'); e('move', 'rom', 1); e('jump', 'scan_loop') + b.mark('scan_done'); b.is_zero('col'); b.branch('zero', '1', 'col_done', reject); b.mark('col_done') + b.compare('row', 's'); b.branch('cmp', '=', 'row_done', reject); b.mark('row_done') + b.branch('found', '1', accept, reject) + b.mark(accept); e('set', 'status', '1'); e('jump', cleanup) + b.mark(reject); e('set', 'status', '0') + b.mark(cleanup) + for tape in PRIVATE: + b.rewind(tape); b.clear(tape) + for tape in BORROWED: b.rewind(tape) + b.branch('status', '1', 'halt_accept', 'clean_reject_output') + b.mark('clean_reject_output'); b.rewind('out'); b.clear('out'); e('halt', 'reject') + b.mark('halt_accept'); e('halt', 'accept') + return b.finish() + +PROGRAM = assemble() + +class Machine: + """Host interpreter: position/PC/census integers are machine metadata only. + + The fixed program can access only alphabet registers and current cells. + Python dictionary addressing implements a tape head, never a data lookup. + """ + def __init__(self, records, trace=False, program=PROGRAM): + self.tapes = {role: {} for role in ROLES} + for role, payload in records.items(): + self.tapes[role] = dict(enumerate('L' + payload + 'R')) + self.heads = dict.fromkeys(ROLES, 0) + self.registers = {}; self.pc = 0; self.census = Counter() + self.trace = [] if trace else None + self.program = program + def run(self, limit=20_000_000): + # limit is an observer watchdog; an overrun fails, never returns a bit. + for _ in range(limit): + pc = self.pc; instruction = self.program[pc]; op, *a = instruction + self.pc += 1; self.census[op] += 1 + observed = None + if op == 'read': + observed = self.tapes[a[0]].get(self.heads[a[0]], '_') + self.registers[a[1]] = observed + elif op in ('write', 'write_reg'): + observed = a[1] if op == 'write' else self.registers[a[1]] + self.tapes[a[0]][self.heads[a[0]]] = observed + elif op == 'move': self.heads[a[0]] += a[1] + elif op == 'set': self.registers[a[0]] = a[1] + elif op == 'copy': self.registers[a[1]] = self.registers[a[0]] + elif op == 'eq': self.registers[a[2]] = self.registers[a[0]] == a[1] + elif op == 'eq_reg': self.registers[a[2]] = self.registers[a[0]] == self.registers[a[1]] + elif op == 'branch': self.pc = a[1] if self.registers[a[0]] else a[2] + elif op == 'jump': self.pc = a[0] + elif op != 'halt': raise ValueError(op) + if self.trace is not None: self.trace.append((pc, observed)) + if op == 'halt': return a[0] + raise RuntimeError('observer watchdog exceeded: not an accepted execution') diff --git a/research/crt-uniform-rom-query/verify.py b/research/crt-uniform-rom-query/verify.py new file mode 100644 index 0000000000..bc28b77e2b --- /dev/null +++ b/research/crt-uniform-rom-query/verify.py @@ -0,0 +1,196 @@ +"""Independent event replay, bounded query checks, and frozen receipt. + +JoyboyBrian with substantial OpenAI Codex assistance. Apache-2.0. +Host integers below belong to the external test oracle, never machine control. +""" +import argparse +from collections import Counter +import hashlib +import importlib.util +import itertools +import json +from pathlib import Path + +P = Path(__file__).resolve().parent + +def need(value, message): + if not value: raise ValueError(message) + +def load_machine(): + spec = importlib.util.spec_from_file_location('rom_query_machine', P / 'machine.py') + module = importlib.util.module_from_spec(spec); spec.loader.exec_module(module) + return module + +def validate_program(m, program): + registers = set() + for inst in program: + op, *a = inst + if op in ('read', 'write', 'write_reg', 'move'): + need(a[0] in m.ROLES, 'static role') + if op in ('write', 'write_reg'): + need(a[0] not in m.BORROWED, 'borrowed write in program') + if op == 'move': need(a[1] in (-1, 1), 'unit move in program') + elif op == 'read': registers.add(a[1]) + elif op == 'write': need(a[1] in 'LR01_', 'tape alphabet') + elif op == 'write_reg': registers.add(a[1]) + elif op == 'set': + registers.add(a[0]); need(a[1] in ('0', '1', '=', '<', '>'), 'finite register constant') + elif op == 'copy': registers.update(a) + elif op in ('eq', 'eq_reg'): + registers.add(a[0]); registers.add(a[2]) + if op == 'eq_reg': registers.add(a[1]) + else: need(a[1] in 'LR01_=<>', 'finite equality constant') + elif op == 'jump': need(type(a[0]) is int and 0 <= a[0] < len(program), 'static jump') + elif op == 'branch': + registers.add(a[0]); need(all(type(x) is int and 0 <= x < len(program) for x in a[1:]), 'static branch') + elif op == 'halt': need(a[0] in ('accept', 'reject'), 'halt state') + else: need(op == 'move', 'known instruction') + return sorted(registers) + +def audit(m, machine, records, expected_status): + # Deliberately uses growable cell lists rather than the runner's dictionaries. + cells = {role: list('L' + records[role] + 'R') if role in records else [] for role in m.ROLES} + heads = dict.fromkeys(m.ROLES, 0); regs = {}; pc = 0; census = Counter(); halted = False + for listed_pc, observed in machine.trace: + need(not halted and listed_pc == pc, 'event PC/control continuity') + op, *a = machine.program[pc]; pc += 1; census[op] += 1 + if op in ('read', 'write', 'write_reg', 'move'): + role = a[0]; head = heads[role]; need(head >= 0, 'left boundary') + if op == 'read': + actual = cells[role][head] if head < len(cells[role]) else '_' + need(observed == actual, 'event read content'); regs[a[1]] = actual + elif op in ('write', 'write_reg'): + need(role not in m.BORROWED, 'event ownership') + value = a[1] if op == 'write' else regs[a[1]] + need(value in 'LR01_' and observed == value, 'event write content') + while len(cells[role]) <= head: cells[role].append('_') + cells[role][head] = value + else: + need(observed is None, 'noncell event has no readback') + if op == 'move': + need(a[1] in (-1, 1), 'unit event move'); heads[role] += a[1] + need(heads[role] >= 0, 'left boundary after move') + elif op == 'set': regs[a[0]] = a[1] + elif op == 'copy': regs[a[1]] = regs[a[0]] + elif op == 'eq': regs[a[2]] = regs[a[0]] == a[1] + elif op == 'eq_reg': regs[a[2]] = regs[a[0]] == regs[a[1]] + elif op == 'branch': + need(type(regs[a[0]]) is bool, 'Boolean branch register'); pc = a[1] if regs[a[0]] else a[2] + elif op == 'jump': pc = a[0] + elif op == 'halt': + need(a[0] == expected_status, 'expected halt'); halted = True + need(halted, 'complete halt event') + need(census == machine.census and pc == machine.pc, 'complete instruction census') + need(heads == machine.heads and all(h == 0 for h in heads.values()), 'all heads restored') + need(regs == machine.registers, 'finite-control registers replay') + for role in m.ROLES: + expected = {i: x for i, x in enumerate(cells[role]) if x != '_'} + actual = {i: x for i, x in machine.tapes[role].items() if x != '_'} + need(actual == expected, 'independent final tape') + for role in m.BORROWED: need(cells[role] == list('L' + records[role] + 'R'), 'borrowed restoration') + for role in m.PRIVATE: need(all(x == '_' for x in cells[role]), 'private erasure') + if expected_status == 'reject': need(all(x == '_' for x in cells['out']), 'rejection output erasure') + else: need(cells['out'] == ['L', cells['out'][1], 'R'] and cells['out'][1] in '01', 'one-bit output record') + return dict(sorted(census.items())) + +def enc(n): return bin(n)[2:][::-1] + +def records(h, s, offset, target, rom): + return dict(h=enc(h), s=enc(s), offset=enc(offset), target=enc(target), rom=rom) + +def execute(m, data, expected, program=None): + machine = m.Machine(data, trace=True, program=m.PROGRAM if program is None else program) + status = machine.run() + need(status == ('reject' if expected is None else 'accept'), 'machine admission') + counts = audit(m, machine, data, status) + if expected is not None: need(machine.tapes['out'][1] == expected, 'oracle selected bit') + return machine, counts + +def must_fail(call, message): + try: call() + except (ValueError, RuntimeError): return + raise ValueError('fault control accepted: ' + message) + +def verify(): + m = load_machine(); registers = validate_program(m, m.PROGRAM) + need(m.PROGRAM == m.assemble(), 'same static program') + cases = []; total_steps = 0; largest_steps = 0; shape_counts = Counter() + def check(h, s, a, t, rom, family): + nonlocal total_steps, largest_steps + x, counts = execute(m, records(h, s, a, t, rom), rom[a * (1 << h) + t]) + steps = sum(counts.values()); w = h + s.bit_length() + 2; M = s * (1 << h) + need(steps <= 512 * (M + 1) * w * w, 'proved instruction majorant') + total_steps += steps; largest_steps = max(largest_steps, steps); shape_counts[family] += 1 + cases.append((h, s, a, t, hashlib.sha256(rom.encode()).hexdigest(), steps, counts)) + return x + # Complete ROM truth tables and addresses for the smallest admissible shape. + for row in itertools.product('01', repeat=4): + rom = ''.join(row) + for a in range(2): + for t in range(2): check(1, 2, a, t, rom, 'h1_all_roms_all_addresses') + # Every valid parameter tuple at h=2, under two different ROM patterns. + for s in range(2, 5): + for phase in (0, 1): + rom = ''.join(str(((i * 7) ^ (i // 3) ^ phase) & 1) for i in range(s * 4)) + for a in range(s): + for t in range(4): check(2, s, a, t, rom, 'h2_all_parameters_two_roms') + for h in (3, 4, 5): + for s in (2, (1 << h) - 1, 1 << h): + rom = ''.join(str(((i * 11) ^ (i // 5)) & 1) for i in range(s * (1 << h))) + for a, t in ((0, 0), (s - 1, (1 << h) - 1), (s - 1, 1)): + check(h, s, a, t, rom, 'larger_boundary_parameters') + fixture = json.loads((P / 'FIXTURE.json').read_text()) + need(fixture['source_commit'] == '26ccde014218f7d906d1251dc295fbc1437ede8a', 'fixture source pin') + need(hashlib.sha256(bytes(map(int, fixture['rom']))).hexdigest() == + 'bc0ab563e6d8fdfa24ee89b50dbe3f9a3a6f23681f491e883c6b5aeef07d4104', 'source ROM bytes') + source_queries = [] + for witness in fixture['witnesses']: + for q in witness['queries']: + x = check(5, 17, q['offset'], q['target'], fixture['rom'], 'source_query_epochs') + need(int(x.tapes['out'][1]) == q['bit'], 'retained source query answer') + source_queries.append(dict(offset=q['offset'], target=q['target'], bit=q['bit'], instructions=sum(x.census.values()))) + base = records(2, 3, 1, 2, '010101100101') + rejected = [dict(base, h='0'), dict(base, h=''), dict(base, h='010'), dict(base, s='1'), + dict(base, s=enc(5)), dict(base, offset=enc(3)), dict(base, target=enc(4)), + dict(base, offset='00'), dict(base, target='_'), dict(base, rom=base['rom'][:-1]), + dict(base, rom=base['rom']+'0'), dict(base, rom='01_101100101'), dict(base, rom=''), + records(65, 2, 0, 0, ''), records(127, (1 << 127) + 1, 0, 0, ''), + dict(base, h='0' * 129)] + for data in rejected: execute(m, data, None) + # Independent ledger checks reject omitted control, changed reads and missing halt. + x, _ = execute(m, base, base['rom'][6]); original = list(x.trace) + index = next(i for i, event in enumerate(original) if m.PROGRAM[event[0]][0] == 'eq') + x.trace = original[:index] + original[index+1:] + must_fail(lambda: audit(m, x, base, 'accept'), 'omitted equality event') + x.trace = list(original); index = next(i for i, event in enumerate(original) if m.PROGRAM[event[0]][0] == 'read') + x.trace[index] = (original[index][0], '1' if original[index][1] != '1' else '0') + must_fail(lambda: audit(m, x, base, 'accept'), 'wrong read event') + x.trace = original[:-1]; must_fail(lambda: audit(m, x, base, 'accept'), 'missing halt event') + bad = list(m.PROGRAM); index = next(i for i, inst in enumerate(bad) if inst[0] == 'move'); bad[index] = ('move', bad[index][1], 0) + must_fail(lambda: validate_program(m, bad), 'nonunit movement') + bad = list(m.PROGRAM); index = next(i for i, inst in enumerate(bad) if inst[0] == 'write'); bad[index] = ('write', 'rom', '0') + must_fail(lambda: validate_program(m, bad), 'borrowed mutation') + bad = list(m.PROGRAM); index = next(i for i, inst in enumerate(bad) if inst == ('write', 'count', '_')); bad[index] = ('write', 'count', '0') + must_fail(lambda: execute(m, base, base['rom'][6], bad), 'dirty private cells') + bad = list(m.PROGRAM); index = next(i for i, inst in enumerate(bad) if inst[0] == 'write_reg' and inst[1] == 'out'); bad[index] = ('write', 'out', '1') + zero = dict(base, rom='0'*12) + must_fail(lambda: execute(m, zero, '0', bad), 'wrong selected answer') + return dict(status='PASS_UNIFORM_ROM_QUERY_COMPONENT', program_instructions=len(m.PROGRAM), + registers=registers, tapes=len(m.ROLES), accepted_cases=len(cases), + case_families=dict(sorted(shape_counts.items())), rejected_records=len(rejected), + fault_controls=7, measured_total_instructions=total_steps, measured_max_instructions=largest_steps, + source_queries=source_queries, case_digest=hashlib.sha256(json.dumps(cases, sort_keys=True).encode()).hexdigest(), + machine_sha256=hashlib.sha256((P/'machine.py').read_bytes()).hexdigest(), + fixture_sha256=hashlib.sha256((P/'FIXTURE.json').read_bytes()).hexdigest(), + instruction_bound='512*(s*2^h+1)*(h+bit_length(s)+2)^2', + binary_action_bound='65536*(s*2^h+1)*(h+log2(s)+1)^2', + excluded=['ROM and header preparation', 'source descriptor serialization adapter', 'CRT reconstruction', 'complete repair/compiler/E tariff', 'host observer overhead']) + +def main(): + parser = argparse.ArgumentParser(); parser.add_argument('--write-result', action='store_true'); args = parser.parse_args() + result = verify() + if args.write_result: (P/'RESULT.json').write_text(json.dumps(result, indent=2, sort_keys=True)+'\n') + else: need(result == json.loads((P/'RESULT.json').read_text()), 'frozen result receipt') + print(json.dumps(result, sort_keys=True)) + +if __name__ == '__main__': main()