diff --git a/research/binary-elementary-interchange/README.md b/research/binary-elementary-interchange/README.md new file mode 100644 index 0000000000..3f842f16ca --- /dev/null +++ b/research/binary-elementary-interchange/README.md @@ -0,0 +1,131 @@ +# Binary elementary interchange + +This package closes the first open question in the literal elementary +interchange package: a fixed block encoding and an actual binary alignment +program. It lowers all 4,589 source instructions and all five entries to +58,608 binary instructions on the same 20 tapes. The program does not depend +on the input width. Runtime instructions contain no source executor, +numeric loop bound, allocator callback, or decoded geometry. + +The proof below gives exact state, cost, and retained-storage refinement. +RESULT.json records 68 full entry comparisons over 16 sessions, including +eight independent payload columns, caller install, and a growing then +shrinking call history. The verifier also checks 153 local instruction cases, +three unused codewords, and seven failure controls. Finite checks support the +written proof; they do not replace it. + +Run from the repository root with Python 3.12 and the standard library: + +```sh +python3 -I -W error -B research/binary-elementary-interchange/verify.py +python3 -I -O -W error -B research/binary-elementary-interchange/verify.py +python3 -B scripts/research_package.py --package research/binary-elementary-interchange +``` + +The direct result is `PASS_BINARY_ELEMENTARY_INTERCHANGE`. +SOURCES.json pins every consumed source at +`ff3cc58e370d0f678e529246f8c73e8094e18fcf`. The verifier checks these bytes +before and after execution. A fresh test-only directory runs the unmodified +source machine; the binary runtime does not call it. The complete receipt +is compared with typed canonical JSON, including under optimized Python. + +## Refinement theorem + +Encode the five source symbols ZERO, ONE, LEFT, RIGHT, BLANK as 001, 010, +011, 100, 000, respectively. Each allocated source cell becomes three +allocated binary cells. A source head at h becomes a binary head at 3h. +Unallocated source cells are BLANK; unallocated binary cells are zero. +Thus both views have the same blank extension. Tape roles remain disjoint. + +At a source instruction boundary, let the source and binary states obey +this relation. The lowered program has the following behavior. + +1. A test reads all three bits through a fixed depth-three decision tree. + Two unit moves advance the head. At each leaf, two unit moves restore + it. Each of the five valid leaves jumps to the matching source successor. + Each unused codeword halts with `rejected` after head restoration. A valid + test uses three reads, four moves and one jump. It changes no tape cell. +2. A write stores all three bits. Two forward and two backward unit moves + restore the head. A jump reaches the next source instruction. This uses + three writes, four moves and one jump. If a write extends the source + array to h+1 cells, the last binary write extends its array to 3(h+1). + Every gap is zero. This also holds when the new symbol is BLANK. +3. A legal source unit move becomes three binary unit moves and one jump. + It allocates no cells. Legal left moves cannot cross the binary origin. +4. A source jump becomes one binary jump. A source halt keeps its status. + +These cases prove the state relation by induction at every source +instruction boundary. All tests have a bounded depth. Every inserted path +reaches a source successor or a halt. Compilation checks the complete +finite instruction alphabet and rejects control-only cycles. The actual +binary program has at most three consecutive jump instructions; its +control factor is four. No extra head or tape is required. + +Suppose a terminating source entry has R reads, W writes, M moves, J jumps +and one halt. The binary entry has exactly + +```text +reads = 3R +writes = 3W +moves = 4R + 4W + 3M +jumps = R + W + M + J +steps = 8R + 8W + 4M + J + 1 <= 8(R + W + M + J + 1). +``` + +Allocated length is exactly three times source allocated length at each +source boundary. During a microprogram it does not exceed the length at +the next source boundary. Reads and moves do not allocate. All three bit +writes are charged even for zero. Therefore erased backing remains in the +account. For every valid sequence of calls, the binary retained-storage +history is three times the corresponding source history. This is a +relative theorem; it does not supply a new absolute source-space bound. + +Apply the theorem to the source program's valid domain: H >= 0, +A,G,S >= 1, V = A*4^H*G*S, canonical encoded descriptors and disjoint roles. +The source proof supplies the interchange permutation and five-entry +lifecycle. The binary program inherits those properties on encoded states. +If L = H + bit_length(H) + bit_length(A) + bit_length(G) + bit_length(S) + 8, +with bit_length(0) taken as one, its complete init/run/consume/close session +cost is at most 2^23*(H+1)*(V+1)*(L+1)^2. This follows from the source bound +2^20*(H+1)*(V+1)*(L+1)^2 and the instruction factor eight. Caller install +has the exact per-entry factor above; the quoted session excludes install. + +## Scope and limits + +This is a finite program plus a written uniform representation proof. +It uses the source program's all-width correctness proof as a premise. +The finite replay here has maximum H=3 and V=64. It does not repeat the +predecessor's 196,608-cell source fixture or claim a new all-size acceptance. +The proof applies to all valid widths because its induction is per opcode. + +Encoded descriptors and payloads are supplied at the boundary. The Python +fixture encoder is not a free runtime adapter. A caller must provide encoded +data directly or pay for a separate codec, its heads, storage and disposal. +Unused codewords are rejected only when a test reads them; this is not a +global input validator or an error rollback guarantee. State refinement +does not cover a source move that crosses the origin. + +No selected file, supplier, physical stock, native operator, precision claim, +ROM producer, whole raw/repair caller, outer recovery proof or complete +kappa calculation changes. Selected kappa remains 60403/20000000. There is +no independent human or proof-kernel acceptance claim. + +## Open next questions + +- Integrate the encoded callee with the complete raw/repair caller. Identify + the representation of every port and pay every codec and lifecycle cost. +- Apply a source retained-backing theorem to obtain an absolute binary + storage grant. Include all old erased arrays and varying call histories. +- Independently check the source all-width proof and this instruction + refinement. A finite execution receipt alone cannot discharge either. + +## Attribution + +JoyboyBrian supplied the literal five-symbol program, lifecycle, source +proof and binary-lowering handoff in PR #5188. Its source notices retain +Jose Manuel's ordinary wrapper, the PR #2809 and PR #2753 stream/cardinality +authors, Cinna Davis, Hiroki KUMAZAKI and Douglas Colkitt. This package does +not modify those sources. PR #5286 is related retained-backing work; it is +not a consumed proof premise here. Ali Romman prepared this refinement +with substantial OpenAI Codex assistance in proof, code and verification. +Apache-2.0. diff --git a/research/binary-elementary-interchange/RESULT.json b/research/binary-elementary-interchange/RESULT.json new file mode 100644 index 0000000000..2c090e4ca4 --- /dev/null +++ b/research/binary-elementary-interchange/RESULT.json @@ -0,0 +1,43 @@ +{ + "status": "PASS_BINARY_ELEMENTARY_INTERCHANGE", + "source_program_length": 4589, + "binary_program_length": 58608, + "binary_program_sha256": "38ade5f7598b0f4aa9ec23a37ce0ebb80ec917c286dacd2d9c2e36e23a4ab931", + "entries": { + "init": 0, + "run": 736, + "consume": 56493, + "install": 56644, + "close": 57256 + }, + "binary_control_factor": 4, + "tape_roles": 20, + "sessions": 16, + "entry_comparisons": 68, + "source_steps": 122805, + "binary_actions": { + "steps": 654512, + "reads": 133569, + "writes": 38706, + "moves": 359432, + "jumps": 122737 + }, + "source_states_sha256": "6f34cb280908c6ceaba0666302745d36b6136e57b38b2e0e7fa12fdad4d52580", + "controls": { + "positive": 153, + "invalid_codewords": 3, + "rejected": [ + "left_origin_crossing", + "missing_alignment_move", + "wrong_bit", + "missing_tail_write", + "host_callback", + "control_only_cycle", + "nonbinary_write" + ] + }, + "code_sha256": { + "binary_machine.py": "3fe87e8919d99ea2767db0a468e11668e337e71b7074216de756d0a4a967c977", + "reference.py": "2d99f27d841a57a4f0a839bf7b31ab6d9f8f7cc0306079571ecde100396367c7" + } +} diff --git a/research/binary-elementary-interchange/SOURCES.json b/research/binary-elementary-interchange/SOURCES.json new file mode 100644 index 0000000000..f7eea0a6e6 --- /dev/null +++ b/research/binary-elementary-interchange/SOURCES.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/literal-elementary-interchange/PROOF.md", + "usage": "input", + "git_blob": "d4e14bba3fe10e0f269b0891b0e196b723b651cf", + "sha256": "507684173bde7865161d641bbffc6862c1e825407c42efa70747c763dadd03af" + }, + { + "path": "research/literal-elementary-interchange/RESULT.json", + "usage": "input", + "git_blob": "d2f4588b53837d22be39636c6661772196b594e9", + "sha256": "a8d4746eb333ea0fcb1d6f613f09b122f7d7a029390dab0df07a4cefb7164c73" + }, + { + "path": "research/literal-elementary-interchange/machine.py", + "usage": "input", + "git_blob": "78dc14bf1c995b5ea348d2e753cf9f56dbdb480b", + "sha256": "66b5c371ff4aebd4391d71b95c59769a067e0a04910521b4881f074f986327bf" + }, + { + "path": "research/literal-elementary-interchange/program.py", + "usage": "input", + "git_blob": "c606ed51a06409a648d3fd385b0dfdaa5e096720", + "sha256": "3b83fbe3451000b00030ff3156222def23ce15d17d00c7d09a324aea5fd92e72" + } + ] +} diff --git a/research/binary-elementary-interchange/TASK.json b/research/binary-elementary-interchange/TASK.json new file mode 100644 index 0000000000..ef2ae8d133 --- /dev/null +++ b/research/binary-elementary-interchange/TASK.json @@ -0,0 +1,81 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "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": "Fixed binary instruction lowering of all five entries in the literal elementary interchange program.", + "scope_change_reason": "The selected bit-mechanisms seed 73182b1ebd6c4262508b6370f43eb467 led to the explicit binary-alphabet handoff in PR #5188. This is a uniform-transfer representation obligation.", + "bottleneck_link": "Remove the finite five-symbol alphabet obligation at the actual interchange callee. Whole-caller integration remains open.", + "budget_minutes": 60, + "stop_rule": "Stop on an uncharged runtime codec, extra tape, failed state refinement, or source-sized replay claim without execution.", + "outcome": "completed", + "evidence": "README.md, RESULT.json, verify.py", + "author": "Ali Romman", + "ai_assistance": "Substantial OpenAI Codex assistance; no independent human or kernel review.", + "open_questions": [ + { + "question": "Integrate all encoded caller ports.", + "why_it_matters": "A representation theorem does not pay codecs.", + "first_step": "List port representations and explicit codec programs.", + "blocked_by": "Whole caller construction." + }, + { + "question": "Give an absolute binary retained-storage grant.", + "why_it_matters": "The current bound is relative to source storage.", + "first_step": "Compose a verified source history bound with factor three.", + "blocked_by": "Source storage theorem intake." + } + ], + "coordination": "https://github.com/CrocSwap/integer-mult-bounds/discussions/4709#discussioncomment-19150847" +} diff --git a/research/binary-elementary-interchange/VERIFY.json b/research/binary-elementary-interchange/VERIFY.json new file mode 100644 index 0000000000..bee1d3aecc --- /dev/null +++ b/research/binary-elementary-interchange/VERIFY.json @@ -0,0 +1,39 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/literal-elementary-interchange/PROOF.md", + "research/literal-elementary-interchange/RESULT.json", + "research/literal-elementary-interchange/machine.py", + "research/literal-elementary-interchange/program.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Fixed-program state, exact cost, backing extent, source bytes, and failure controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same complete checks with assertions disabled." + } + ] +} diff --git a/research/binary-elementary-interchange/binary_machine.py b/research/binary-elementary-interchange/binary_machine.py new file mode 100644 index 0000000000..91a9cb6921 --- /dev/null +++ b/research/binary-elementary-interchange/binary_machine.py @@ -0,0 +1,148 @@ +"""Lower a literal five-symbol program to aligned three-bit blocks. + +Ali Romman, with substantial OpenAI Codex assistance. Apache-2.0. +""" + +ENCODING = ((0, 0, 1), (0, 1, 0), (0, 1, 1), (1, 0, 0), (0, 0, 0)) +STATUSES = ('initialized', 'returned', 'consumed', 'installed', 'closed', 'rejected') + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def admit(code, entries, roles, alphabet): + """Check the finite instruction alphabet and exclude control-only cycles.""" + for pc, row in enumerate(code): + op, *args = row + targets = [] + if op == 'test': + need(len(args) == 4 and args[0] in roles and type(args[1]) is int + and args[1] in alphabet, 'test domain') + targets = args[2:] + elif op == 'write': + need(len(args) == 2 and args[0] in roles and type(args[1]) is int + and args[1] in alphabet, 'write domain') + elif op == 'move': + need(len(args) == 2 and args[0] in roles and type(args[1]) is int + and args[1] in (-1, 1), 'move domain') + elif op == 'jump': + need(len(args) == 1, 'jump arity') + targets = args + else: + need(op == 'halt' and len(args) == 1 and args[0] in STATUSES, 'halt domain') + if op in ('write', 'move'): + need(pc+1 < len(code), 'fallthrough boundary') + need(all(type(t) is int and 0 <= t < len(code) for t in targets), 'target domain') + need(code and all(type(v) is int and 0 <= v < len(code) for v in entries.values()), 'entry') + longest = 0 + for start, row in enumerate(code): + if row[0] != 'jump': + continue + seen, pc = set(), start + while code[pc][0] == 'jump': + need(pc not in seen, 'control-only cycle') + seen.add(pc) + pc = code[pc][1] + longest = max(longest, len(seen)) + return longest+1 + + +def lower(code, entries, roles): + """Compile once; the output has no source executor or runtime callback.""" + admit(code, entries, roles, range(5)) + output, labels = [], {} + def emit(*row): + output.append(row) + def mark(label): + labels[label] = len(output) + for pc, row in enumerate(code): + mark(('source', pc)) + op = row[0] + if op == 'test': + _, role, symbol, yes, no = row + def decode(prefix): + if len(prefix) == 3: + emit('move', role, -1) + emit('move', role, -1) + if prefix not in ENCODING: + emit('halt', 'rejected') + else: + emit('jump', ('source', yes if prefix == ENCODING[symbol] else no)) + return + zero, one = ('bit', pc, prefix, 0), ('bit', pc, prefix, 1) + emit('test', role, 1, one, zero) + for bit, label in ((0, zero), (1, one)): + mark(label) + if len(prefix) < 2: + emit('move', role, 1) + decode(prefix+(bit,)) + decode(()) + elif op == 'write': + _, role, symbol = row + for offset, bit in enumerate(ENCODING[symbol]): + emit('write', role, bit) + if offset < 2: + emit('move', role, 1) + emit('move', role, -1) + emit('move', role, -1) + emit('jump', ('source', pc+1)) + elif op == 'move': + for _ in range(3): + emit(*row) + emit('jump', ('source', pc+1)) + elif op == 'jump': + emit('jump', ('source', row[1])) + else: + emit(*row) + resolved = [] + for row in output: + if row[0] == 'test': + row = (*row[:3], labels[row[3]], labels[row[4]]) + elif row[0] == 'jump': + row = ('jump', labels[row[1]]) + resolved.append(row) + lowered_entries = {name: labels[('source', pc)] for name, pc in entries.items()} + result = tuple(resolved) + admit(result, lowered_entries, roles, (0, 1)) + return result, lowered_entries + + +def execute(code, tapes, heads, entry, max_steps=10000000): + """Interpret only binary local-cell instructions; count every instruction.""" + pc = entry + counts = dict(steps=0, reads=0, writes=0, moves=0, jumps=0) + while counts['steps'] < max_steps: + row = code[pc] + op = row[0] + counts['steps'] += 1 + if op == 'test': + _, role, bit, yes, no = row + head, cells = heads[role], tapes[role] + value = cells[head] if head < len(cells) else 0 + need(value in (0, 1), 'nonbinary cell') + counts['reads'] += 1 + pc = yes if value == bit else no + elif op == 'write': + _, role, bit = row + head, cells = heads[role], tapes[role] + if head >= len(cells): + cells.extend([0]*(head+1-len(cells))) + cells[head] = bit + counts['writes'] += 1 + pc += 1 + elif op == 'move': + _, role, step = row + need(heads[role]+step >= 0, 'left boundary') + heads[role] += step + counts['moves'] += 1 + pc += 1 + elif op == 'jump': + counts['jumps'] += 1 + pc = row[1] + elif op == 'halt': + return dict(counts, status=row[1]) + else: + raise ValueError('invalid opcode') + raise ValueError('observer watchdog') diff --git a/research/binary-elementary-interchange/reference.py b/research/binary-elementary-interchange/reference.py new file mode 100644 index 0000000000..ac5c5850d6 --- /dev/null +++ b/research/binary-elementary-interchange/reference.py @@ -0,0 +1,32 @@ +"""Run the pinned source machine in a fresh test-only import directory.""" +import json +from pathlib import Path +import sys + +sys.path.insert(0, str(Path(__file__).resolve().parent)) +from program import assemble, ROLES, BORROWED, BLANK, LEFT, RIGHT +from machine import execute + +code, entries = assemble() +result = [] +for session in json.load(sys.stdin): + tapes = {r: bytearray([BLANK]) for r in ROLES} + heads = {r: 0 for r in ROLES} + events = [] + def call(name): + receipt = execute(code, tapes, heads, entries[name], max_steps=10000000) + events.append(dict(entry=name, receipt=receipt, heads=dict(heads), + tapes={r: list(v) for r, v in tapes.items()})) + call('init') + for case in session: + h, a, g, s = case['geometry'] + tapes['SOURCE'] = bytearray([LEFT] + case['bits']) + for r, v in zip(('H', 'A', 'G', 'S'), (h, a, g, s)): + tapes[r] = bytearray([LEFT] + [int(x) for x in reversed(bin(v)[2:])] + [RIGHT]) + for r in BORROWED: + heads[r] = 1 + call('run') + call('install' if case.get('install') else 'consume') + call('close') + result.append(events) +json.dump(result, sys.stdout, sort_keys=True) diff --git a/research/binary-elementary-interchange/verify.py b/research/binary-elementary-interchange/verify.py new file mode 100644 index 0000000000..3e8263bf41 --- /dev/null +++ b/research/binary-elementary-interchange/verify.py @@ -0,0 +1,195 @@ +"""Check the binary lowering, full states, meters, and retained tape storage.""" +import argparse +from hashlib import sha256 +import json +from pathlib import Path +import runpy +import subprocess +import sys +import tempfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +bm = runpy.run_path(str(HERE / 'binary_machine.py')) +need, lower, execute, admit, ENCODING = (bm[k] for k in ('need', 'lower', 'execute', 'admit', 'ENCODING')) + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(',', ':'), allow_nan=False) + +def authenticate(): + rows = json.loads((HERE / 'SOURCES.json').read_text())['files'] + result = {} + for row in rows: + if row['usage'] == 'input': + data = (ROOT / row['path']).read_bytes() + need(sha256(data).hexdigest() == row['sha256'], 'source bytes: ' + row['path']) + result[Path(row['path']).name] = data + return result + +def encode(cells): + return bytearray(bit for cell in cells for bit in ENCODING[cell]) + +def reject(action): + try: + action() + except ValueError: + return + raise ValueError('negative control accepted') + +def micro_checks(): + checked = 0 + for head in (0, 1, 4): + for value in range(5): + cells = [2, value, 3] + if head == 0: + cells[0] = value + if head == 4: + cells += [1, value] + for symbol in range(5): + source = (('test', 't', symbol, 1, 2), ('halt', 'returned'), ('halt', 'rejected')) + code, entries = lower(source, {'run': 0}, ('t',)) + tapes, heads = {'t': encode(cells)}, {'t': 3*head} + receipt = execute(code, tapes, heads, entries['run']) + need(receipt == dict(status='returned' if value == symbol else 'rejected', + steps=9, reads=3, writes=0, moves=4, jumps=1), 'test meter or branch') + need(tapes['t'] == encode(cells) and heads['t'] == 3*head, 'test frame') + checked += 1 + for symbol in range(5): + source = (('write', 't', symbol), ('halt', 'returned')) + code, entries = lower(source, {'run': 0}, ('t',)) + tapes, heads = {'t': encode(cells[:2])}, {'t': 3*head} + receipt = execute(code, tapes, heads, entries['run']) + expected = cells[:2] + [4]*max(0, head+1-2) + expected[head] = symbol + need(tapes['t'] == encode(expected) and heads['t'] == 3*head, 'write frame or extent') + need(receipt == dict(status='returned', steps=9, reads=0, writes=3, moves=4, jumps=1), 'write meter') + checked += 1 + for step in (-1, 1): + code, entries = lower((('move', 't', step), ('halt', 'returned')), {'run': 0}, ('t',)) + tapes, heads = {'t': encode([2])}, {'t': 6} + receipt = execute(code, tapes, heads, entries['run']) + need(heads['t'] == 6+3*step and tapes['t'] == encode([2]), 'move frame') + need(receipt['steps'] == 5 and receipt['moves'] == 3, 'move meter') + checked += 1 + negative_move, _ = lower((('move', 't', -1), ('halt', 'returned')), {'run': 0}, ('t',)) + reject(lambda: execute(negative_move, {'t': encode([2])}, {'t': 0}, 0)) + code, entries = lower((('test', 't', 4, 1, 2), ('halt', 'returned'), ('halt', 'closed')), {'run': 0}, ('t',)) + tapes, heads = {'t': bytearray()}, {'t': 21} + need(execute(code, tapes, heads, 0)['status'] == 'returned' and not tapes['t'] and heads['t'] == 21, 'unallocated blank') + for value in ((1, 0, 1), (1, 1, 0), (1, 1, 1)): + tapes, heads = {'t': bytearray(value)}, {'t': 0} + need(execute(code, tapes, heads, 0)['status'] == 'rejected' and heads['t'] == 0, 'invalid codeword') + # Change real lowered instructions and require observable failures. + bad = list(code) + pos = next(i for i, row in enumerate(bad) if row == ('move', 't', -1)) + bad[pos] = ('jump', pos+1) + tapes, heads = {'t': encode([4])}, {'t': 0} + execute(bad, tapes, heads, 0) + reject(lambda: need(heads['t'] == 0, 'missing alignment move')) + write, _ = lower((('write', 't', 3), ('halt', 'returned')), {'run': 0}, ('t',)) + for index, label in ((0, 'wrong bit'), (4, 'missing tail write')): + bad = list(write) + bad[index] = ('write', 't', 0) if index == 0 else ('jump', index+1) + tapes, heads = {'t': bytearray()}, {'t': 0} + execute(bad, tapes, heads, 0) + reject(lambda: need(tapes['t'] == encode([3]), label)) + reject(lambda: admit((('call', 'host'),), {'run': 0}, ('t',), (0, 1))) + reject(lambda: admit((('jump', 0),), {'run': 0}, ('t',), (0, 1))) + reject(lambda: admit((('write', 't', 2), ('halt', 'closed')), {'run': 0}, ('t',), (0, 1))) + return dict(positive=checked+1, invalid_codewords=3, + rejected=['left_origin_crossing', 'missing_alignment_move', 'wrong_bit', 'missing_tail_write', + 'host_callback', 'control_only_cycle', 'nonbinary_write']) + +def fixture(h, a=1, g=1, s=1, bits=None, install=False): + n = a*4**h*g*s + if bits is None: + bits = [((i*13) ^ (i//3)) & 1 for i in range(n)] + return dict(geometry=[h, a, g, s], bits=bits, install=install) + +def permutation(case): + h, a, g, s = case['geometry'] + return [case['bits'][((((p*2**h+x)*g+m)*2**h+y)*s)+b] + for p in range(a) for y in range(2**h) for m in range(g) + for x in range(2**h) for b in range(s)] + +def run(): + source = authenticate() + namespace = {} + exec(compile(source['program.py'], 'pinned-program.py', 'exec'), namespace) + original, original_entries = namespace['assemble']() + need(sha256(canonical((original, original_entries)).encode()).hexdigest() == + json.loads(source['RESULT.json'])['program_sha256'], 'source program digest') + roles, borrowed = namespace['ROLES'], namespace['BORROWED'] + code, entries = lower(original, original_entries, roles) + sessions = [[fixture(h)] for h in range(4)] + sessions += [[fixture(0, 2, 3, 2)], [fixture(1, 2, 2, 2)], [fixture(2, 1, 2, 1, install=True)]] + sessions += [[fixture(1, g=2, bits=[int(i == j) for i in range(8)])] for j in range(8)] + sessions += [[fixture(0), fixture(2, g=2), fixture(1)]] + with tempfile.TemporaryDirectory() as tmp: + directory = Path(tmp) + for name in ('program.py', 'machine.py'): + (directory/name).write_bytes(source[name]) + driver = directory/'reference.py' + driver.write_bytes((HERE/'reference.py').read_bytes()) + response = subprocess.run([sys.executable, '-I', '-B', str(driver)], input=canonical(sessions), + capture_output=True, text=True, timeout=60) + need(response.returncode == 0, 'source process: ' + response.stderr) + reference = json.loads(response.stdout) + totals = dict(steps=0, reads=0, writes=0, moves=0, jumps=0) + original_steps = 0 + events = 0 + state_digest = sha256() + for session, source_events in zip(sessions, reference, strict=True): + tapes = {r: encode([4]) for r in roles} + heads = {r: 0 for r in roles} + case_index = -1 + for event in source_events: + entry = event['entry'] + if entry == 'run': + case_index += 1 + case = session[case_index] + h, a, g, s = case['geometry'] + tapes['SOURCE'] = encode([2] + case['bits']) + for r, v in zip(('H', 'A', 'G', 'S'), (h, a, g, s)): + tapes[r] = encode([2] + [int(x) for x in reversed(bin(v)[2:])] + [3]) + for r in borrowed: + heads[r] = 3 + receipt = execute(code, tapes, heads, entries[entry]) + expected_tapes = {r: encode(v) for r, v in event['tapes'].items()} + need(tapes == expected_tapes and heads == {r: 3*v for r, v in event['heads'].items()}, 'complete state') + old = event['receipt'] + reads, writes, moves = (old[k] for k in ('reads', 'writes', 'moves')) + jumps = old['steps'] - reads - writes - moves - 1 + expected = dict(status=old['status'], reads=3*reads, writes=3*writes, + moves=4*(reads+writes)+3*moves, jumps=reads+writes+moves+jumps, + steps=8*(reads+writes)+4*moves+jumps+1) + need(receipt == expected and receipt['steps'] <= 8*old['steps'], 'exact meter') + if entry == 'run': + oracle = encode(permutation(case)) + need(tapes['OUTPUT'][3:3+len(oracle)] == oracle, 'independent permutation') + for k in totals: + totals[k] += receipt[k] + original_steps += old['steps'] + state_digest.update(canonical(event).encode()) + events += 1 + controls = micro_checks() + need(authenticate() == source, 'source changed during replay') + return dict(status='PASS_BINARY_ELEMENTARY_INTERCHANGE', source_program_length=len(original), + binary_program_length=len(code), binary_program_sha256=sha256(canonical((code, entries)).encode()).hexdigest(), + entries=entries, binary_control_factor=admit(code, entries, roles, (0, 1)), + tape_roles=len(roles), sessions=len(sessions), entry_comparisons=events, + source_steps=original_steps, binary_actions=totals, source_states_sha256=state_digest.hexdigest(), + controls=controls, code_sha256={n: sha256((HERE/n).read_bytes()).hexdigest() + for n in ('binary_machine.py', 'reference.py')}) + +if __name__ == '__main__': + parser = argparse.ArgumentParser() + parser.add_argument('--emit', action='store_true') + args = parser.parse_args() + expected = None if args.emit else json.loads((HERE/'RESULT.json').read_text()) + result = run() + if args.emit: + print(json.dumps(result, indent=2)) + else: + need(canonical(result) == canonical(expected), 'complete typed receipt') + print(result['status'])