From a17762e852f9cea10f6712dbfef112d7fb2209f7 Mon Sep 17 00:00:00 2001 From: JoyboyBrian <122925040+JoyboyBrian@users.noreply.github.com> Date: Sat, 24 Oct 2026 20:59:36 -0700 Subject: [PATCH 1/2] Refine the complete CRT caller into literal binary control --- .../crt-complete-binary-refinement/PROOF.md | 193 +++++++++++++ .../crt-complete-binary-refinement/README.md | 76 +++++ .../SOURCES.json | 138 ++++++++++ .../crt-complete-binary-refinement/lower.py | 259 ++++++++++++++++++ 4 files changed, 666 insertions(+) create mode 100644 research/crt-complete-binary-refinement/PROOF.md create mode 100644 research/crt-complete-binary-refinement/README.md create mode 100644 research/crt-complete-binary-refinement/SOURCES.json create mode 100644 research/crt-complete-binary-refinement/lower.py diff --git a/research/crt-complete-binary-refinement/PROOF.md b/research/crt-complete-binary-refinement/PROOF.md new file mode 100644 index 0000000000..40b6fe1fa4 --- /dev/null +++ b/research/crt-complete-binary-refinement/PROOF.md @@ -0,0 +1,193 @@ +# Complete binary refinement of the fixed CRT repair program + +Prepared by JoyboyBrian with substantial OpenAI Codex assistance. Apache-2.0. + +## Statement and inherited hypotheses + +Let P be the exact 8,242-instruction program assembled by the pinned PR5105 +`machine.py` and `compiler.py`, with its 31 distinct tape roles. Assume the +successful input contract in its pinned PROOF.md: unary geometry +(G,H,K,Y,J,B)=(2,2,6,8,2,0); a framed, target-independent 32-bit ROM; +4,096 opaque 12-bit record labels in the supplied raw post-S order; zero +heads; and private blank tapes. We inherit its source-algorithm correctness, +allocation and successful-domain theorem. We do not infer those from one run. + +The program emitted by `lower.py` operates through the unchanged PR4982 +`Machine` and `BitTape`: one-bit reads/writes, unit bit-head movement, +one-bit Boolean gates, one-bit assignments, branches, jumps and halts. +Neither a runtime decoded symbol nor a runtime host tape-role selection is +an instruction. The instruction's tape name is always a literal fixed role. +Program counters and emulated head coordinates are configuration machinery. + +The emitted program refines every source step on the stated successful +domain and therefore returns the same ideal-T payload order. It preserves +borrowed geometry/ROM, erases the same private roles, returns every physical +head, and clears all 14,839 finite-control bits. It has 557,123 static +instructions. If the source executes T instructions, including its halt, +then the complete binary invocation costs at most + + 101391 T + 29679 + +charged bit/control actions. This includes initialization and final control +erasure. The source theorem's symbolic bound for T can be substituted +without running the full binary layer. This is a fixed-program refinement, +not a variable-geometry E(p,ell), a complete physical multiplier, or a +claim that the full binary layer was executed. + +## Finite closure and encoding + +`closure` starts each source register at {None}; every tape contains blank, +the six headers also contain `<`, `>`, `1`, ROM contains its markers/bits, +and data contains `<`, `>` and all 4,096 records. It propagates possible +values monotonically through **every** source instruction, including loop +back edges implicitly by repeated saturation. Reads take the union of the +possible named tapes; writes enlarge those tapes; copies and finite tuple +expressions propagate their values; field projection propagates each +defined tuple component; comparisons/record/not yield Boolean values; +bit-string gates yield `0` or `1`. Branches and jumps produce no values. +All constants and nested operand expressions are included in the codebook. +Unsupported operations, large Cartesian products or exhausted code space +fail compilation; they do not silently truncate the domain. + +The saturation terminates after four rounds for this exact P. By induction +on executed steps, registers and tapes remain in the saturated domains. +This is an overapproximation, including transient None alternatives that +are not reachable at many instruction sites. In the successful source +execution all tape operands are actual roles and all field operands are +tuples of the appropriate length. The latter follows specifically from +the producer's returned role products and the scanner's producer-owned +stencil: after the END test, each token is an admitted five-field atom. +We do not claim string indexing or malformed arbitrary source states are +refined by the tuple-field blocks. Undefined/unadmitted dispatch and field +values reject. This preserves the original successful-domain restriction. + +Python equality identifies False with 0 and True with 1, recursively in +tuples. `canon` makes precisely that identification. The source uses no +Boolean identity/type test; its only type-sensitive operation is `record`. +Every reachable record is `('R', n)` with integer 0<=n<4096; canonicalization +preserves this predicate, truthiness, equality, tuple construction and +projection. Thus the canonical state is a sufficient source-state quotient. + +There are 4,932 canonical values. Blank `_` has code zero. Records have +code 4096+n; all other values have distinct codes below 4096. Codes use +13 little-endian bits. In particular record recognition is exactly the +high code bit, and all 4,096 payload labels remain distinct. There is no +record-pair lookup table. Unused bit patterns are outside the entry +contract. Source cell j occupies positions 13j through 13j+12. At source +instruction boundaries each physical head is at 13 times its source head. + +## Instruction simulation + +Each source register is a 13-bit finite-control word. Temporary control +bits are reused between source instructions: names beginning `$` are +disjoint from the actual source register namespace. No temporary is read +before its block assigns it. At entry, explicit set instructions initialize +source words to code(None) and scratch to zero. Both successful and +rejecting exits share explicit all-zero control tails; rejecting exits +have no data rollback promise. + +* **Constants, copies and products.** A constant writes its 13 code bits. + Copies preserve every bit, including when source and destination alias. + A finite product evaluates all component words before its decision chain. + For each statically enumerated tuple, conjunction of component equalities + selects its unique code; injectivity proves exactly one match for an + admitted operand. This includes nested role products and five-field + stencil atoms. Static enumeration is compilation, not execution. +* **Equality, inequality, membership and truth.** XOR each pair of code + bits, OR the differences, then negate: this is equality of canonical + values. Inequality reverses the result. Membership ORs the finitely many + element comparisons. Truth excludes exactly the finitely encoded falsy + values (None and zero here). Boolean results are encoded as canonical + integer zero/one. Inputs are evaluated before an aliased destination is + overwritten. +* **Field and record.** The field block compares the whole input code + against every admitted tuple alternative and emits the chosen component + code. Its defined branches therefore implement tuple projection. Record + uses the high bit, whose exactness follows from the entire code inventory. + This does not decode a payload integer into a runtime address. +* **String-bit gates.** Compare each operand against the code of string + `1`; apply XOR/AND/OR to those Boolean flags; emit the code of string + `0` or `1`. This is the precise source semantics, including its treatment + of operands other than string `1`. It does not confuse integer one with + string `1`. +* **Tape role dispatch.** A literal role chooses its fixed tape directly. + A role register is compared against its statically possible fixed roles; + each matching arm names a literal tape in every emitted instruction. + For this P each role register's valid role set is a singleton (None may + also occur in the overapproximation); the validation chain remains + explicit. No host lookup uses the runtime role word. Role selection + finishes before a read can overwrite an aliased operand register. +* **Read/write/move.** A read or write visits the 13 consecutive bits and + then rewinds twelve positions to the cell start. It realizes exactly one + source symbol access without altering other cells. A source unit move + emits thirteen unit bit moves. Thus the head invariant is preserved, + including append/blank regions and arbitrary existing payload contents. +* **Control.** Internal decision chains have forward edges only and leave + at the designated block end. Source branch/jump targets are relocated + to exact source-block starts, including backward loop edges. A source + halt goes to its shared erase tail and corresponding final halt. + +These cases cover all sixteen opcodes actually emitted by P. They also +explain operand aliasing: every value needed for a result or role arm is +read before a destructive result write. The verifier executes alias +controls, but the cases above establish the quantified step relation. +Induction through arbitrary repeated source loops composes the relation; +finite tests are corroboration, not the induction argument. + +## Cost, storage and composition + +The exact generated source-block intervals have maximum length 101,391. +Every internal edge goes forward; the only source back edges terminate a +block at another source boundary. Therefore every simulated source step +uses at most this many binary actions, regardless of the runtime branch. +Initialization writes 14,839 control bits; the terminal tail writes them +again and executes one halt. Consequently the bound is +101391*T + 2*14839 + 1. The block maximum is deliberately conservative, +dominated by overapproximated aggregate alternatives, not an optimization +or observed maximum for a production input. Shared exit tails avoid +replicating all control erasure at every rejecting source site. + +If the source's visited retained tape backing is B cells, its bit encoding +uses 13B cells, plus 14,839 finite-control bits and the fixed program. +Moving through a source cell's encoding visits only its own 13 bits; +there is no hidden record gather or payload transpose. Private source +blanks become actual zero bits; source marker disposal thus erases the +entire corresponding codeword. All heads zero at source exit implies all +physical heads zero. The ambient/private blank-storage grant is inherited; +we do not establish initialization of arbitrary dirty exterior storage. + +Input serialization, fixed program construction, the ROM producer and raw-S +production remain external prerequisites. Static compilation here takes no +input payload, ROM contents or runtime address. It emits one fixed program +for the specified source, not a program regenerated per payload. + +## Executed evidence and its limits + +`verify.py` authenticates every declared source before assembly. Its +microchecks use the **original PR5105 executor** as the reference, including +aliased destinations, all operator classes, typed equality, stencil fields, +dynamic role selection, bit strides and complete exit-control cleanup. +Three executable faults omit a bit stride, retain control, or route to the +wrong physical tape. The code inventory covers all 4,096 record labels. + +Two longer comparisons run the complete fixed-program blocks on persistent +encoded tape objects, checking each source boundary's changed register, +write and head plus the complete endpoint. One executes the actual producer +through its scanner handoff. The other starts at the key-entry state +obtained from the actual complete source producer/scanner/split and executes +its whole current-inverse key to the real continuation. That cut is encoded +once at entry; it is not evidence of binary scanner execution. No borrowed +or output stream is reconstructed between the bit instructions in a cut. + +We did not execute the full binary mask, all 2,944 keys, all sorting passes +or whole-layer endpoint. Their binary correctness follows conditionally +from the source theorem and the step proof above, not a claimed full replay. +No independent human or formal-kernel acceptance is asserted. + +## Attribution + +PR5105 supplies complete finite control and the source caller proof. PR4982 +supplies the unchanged binary executor and earlier key simulation; PR5015 +supplies the isolated radix refinement. We preserve the CRT/key/scanner/ +repair lineage of Cinna Davis, Hiroki KUMAZAKI, ToikY, Jose Manuel, Ryanson +Jonathan, unpaidmoon, codyw912, Douglas Colkitt and the retained notices. diff --git a/research/crt-complete-binary-refinement/README.md b/research/crt-complete-binary-refinement/README.md new file mode 100644 index 0000000000..9a4b0933fb --- /dev/null +++ b/research/crt-complete-binary-refinement/README.md @@ -0,0 +1,76 @@ +# Complete binary refinement of the fixed CRT repair caller + +This answers PR5105's first Open next question: lower its **complete** +finite-symbol program to a literal bit-operation program, including stencil +products, role registers, split/key, sorting, reinsertion and disposal. +It reuses PR4982's unchanged bit executor. PR4982's key and PR5015's isolated +radix algorithm are not rebuilt or claimed again. + +The written [proof](PROOF.md) establishes source-step simulation for the +actual admitted u2/t2/y8 caller, arbitrary opaque 12-bit payload labels and +its admitted 32-bit ROM. A four-round static closure finds 4,932 canonical +values, all encodable in 13 bits. The complete 8,242-instruction source +compiles to 557,123 bit instructions using 31 tape roles and 14,839 finite +control bits. For T source instructions, its complete invocation bound is + + binary actions <= 101391 T + 29679. + +Every runtime tape operand is a literal role selected by bit tests, and +every data access is one-bit read/write or unit bit-head movement. Stencil +field projection and role products are compiled finite decision chains. +The conservative constant includes the largest overapproximated aggregate +block; this is no speedup or new kappa claim. Input/ROM serialization, +raw-S production and variable geometry remain external. + +The verifier uses the original PR5105 executor as its independent reference +for 63 instruction/alias/dispatch cases, checks all 4,096 payload encodings, +and detects wrong-role, short-stride and retained-control faults. It executes +2,862 actual producer boundaries and 43,130 complete key-cut boundaries on +persistent encoded tape objects. The key cut comes from the actual source +producer/scanner/split state and reaches its real continuation. Its entry +is encoded once; the scanner is not binary-replayed. + +**The full binary layer is not executed.** Its correctness follows +conditionally from the complete source theorem and the written per-step +proof, not from claiming that the bounded cuts cover 2,944 keys or all +sorting passes. Source and proof review are AI-assisted, not independent +human or formal-kernel acceptance. Selected PR5413 and frozen sources stay +unchanged. + +## Reproduce + +Python 3.12, standard library only, a few seconds locally: + +```sh +python3.12 -B scripts/research_package.py --package research/crt-complete-binary-refinement +python3.12 -O -B research/crt-complete-binary-refinement/verify.py +``` + +All declared live sources authenticate before assembly. Normal replay +compares the typed frozen receipt; only `--write-result` authors it. +Direct replay works in the official Git-free export. Compilation is fixed +source preprocessing; no input payload or ROM is an assembler argument. +The private blank backing and valid encoded entry contract are inherited; +this does not provide arbitrary-dirty-storage allocation or malformed-input +rollback. + +## Open next questions + +1. Budget a complete binary-layer replay using the source instruction census + before spending billions of literal steps. This would corroborate the + proof with a whole endpoint; it is not a prerequisite disguised as a + passing partial replay here. +2. Bind encoded ROM/descriptor construction and raw-S production to this + exact representation and ownership contract. Those missing producers, + variable geometry and the full E(p,ell) bill block a uniform CRT claim. + +Exact pins and structured questions are in SOURCES.json and TASK.json. +Canonical claim: [Discussion4709](https://github.com/CrocSwap/integer-mult-bounds/discussions/4709#discussioncomment-19172880). +Fresh entry overlap covered 342 open PRs and 4,736 discussion records. +Unpublished work and arbitrary diffs are outside that coverage. + +Prepared by JoyboyBrian with substantial OpenAI Codex assistance; Apache-2.0. +Retain PR5105/PR4982/PR5015 and the credited Cinna Davis, Hiroki KUMAZAKI, +ToikY, Jose Manuel, Ryanson Jonathan, unpaidmoon, codyw912, Douglas Colkitt +and underlying CRT/repair notices. Source retention is not scientific +acceptance. diff --git a/research/crt-complete-binary-refinement/SOURCES.json b/research/crt-complete-binary-refinement/SOURCES.json new file mode 100644 index 0000000000..5edbe4d323 --- /dev/null +++ b/research/crt-complete-binary-refinement/SOURCES.json @@ -0,0 +1,138 @@ +{ + "schema_version": 1, + "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "fc3d4ba105e1f097d0d7d051a308281e86ab1446", + "sha256": "66974efdced4083c00025f97d95d83909a226cdf801edb9301c195c6641f6903" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/crt-binary-key-port/PROOF.md", + "usage": "input", + "git_blob": "c7bffebbc1cef2420e2ba910b4cbf6e9b3110994", + "sha256": "c1fb60178576f64f170c1c0867c2a109c15a993a7bdc3ad52e1ff70c8a58faa0" + }, + { + "path": "research/crt-binary-key-port/binary.py", + "usage": "input", + "git_blob": "ec574f26d6f64ead00d7c2cf5b808c0498b460cf", + "sha256": "50a3dea7fc087715b4e605e85629566ed31903026540f916df6b8cbaa536182d" + }, + { + "path": "research/crt-binary-radix-consumer/PROOF.md", + "usage": "input", + "git_blob": "600822d5a68687948da0f2ecd08eabbfe626cbf4", + "sha256": "b2f9230f8bd435a3fae006cd8eea760912ec2eb3eab56824411f92b2875aba6f" + }, + { + "path": "research/crt-complete-repair-control/PROOF.md", + "usage": "input", + "git_blob": "d5e56adbe7d9f40d3d7ab0e0401264edf004132c", + "sha256": "151211f34d80c8edd03512dd18af27b9b5b1dfe6f9fda9f904bfd59c4ab1a807" + }, + { + "path": "research/crt-complete-repair-control/compiler.py", + "usage": "input", + "git_blob": "e0004e1c2f2728d7e89d856138cae0dc490ab783", + "sha256": "1186cdefed22890a987c1f289290c6db4c19446a29461c1db46257f318b05156" + }, + { + "path": "research/crt-complete-repair-control/machine.py", + "usage": "input", + "git_blob": "85b7fd529f9478796a3e9368f7e019964788874f", + "sha256": "afa110ed2fdba62e810fd794e5fd62a07ec4caf18e8919066275523713353cc7" + }, + { + "path": "research/crt-dense-guard-scan/PROOF.md", + "usage": "input", + "git_blob": "235d7405ffcf712ad3905c3077719554ade0790c", + "sha256": "c075a3c261bb824884f0da9f99fed227b15f9fac087bbdeb2c2cb861d4091f11" + }, + { + "path": "research/crt-dense-guard-scan/machine.py", + "usage": "input", + "git_blob": "ce763898bd7b4401bbab818c640a0593b65c9a82", + "sha256": "1cb27312932914eb631078bd56e85feb1dc6c4191e9d1962b2cc3a7e1cfb8df7" + }, + { + "path": "research/crt-mask-repair-bridge/PROOF.md", + "usage": "input", + "git_blob": "e6138f3b6c0920f84422a1022064e14e2daea76b", + "sha256": "c74f93a65f7b28e751a9c93aa37fc7f74f7ce42cd96e31fa3d1212c94991769c" + }, + { + "path": "research/crt-mask-repair-bridge/bridge.py", + "usage": "input", + "git_blob": "826d62adbb777ceec20974e600a6ea05e03b7828", + "sha256": "573451d94435b6096a88250ca2a9fb75f39bcfa6f0436ffe2363ee07381d8331" + }, + { + "path": "research/crt-mask-repair-bridge/key_subroutine.py", + "usage": "input", + "git_blob": "5771ae55626dbc2a32a95d8c098bdd03d820833c", + "sha256": "ffdbb610be71ae20bf974946dac66b6c1b4d43739cbc3b1eb81cbbeab8784b44" + }, + { + "path": "research/crt-paid-key-service/PROOF.md", + "usage": "input", + "git_blob": "a0b84e8d3bd80d760a1be9e801fc57939b6f24e9", + "sha256": "1a4ac02653eb6c1b20807033a910f27bf9484cc972bf2629941f589275a87325" + }, + { + "path": "research/crt-paid-key-service/service.py", + "usage": "input", + "git_blob": "726d9523ab7dd4a16697f9201b0224f2da1f2517", + "sha256": "ff06c6305c9f650a694e5c42baa4c7d841decf844a4f44f6776acc10a8400083" + }, + { + "path": "research/crt-unary-stencil-producer/PROOF.md", + "usage": "input", + "git_blob": "d81a6cca7c433bc7fb015a41cc0f72bf9f676a5d", + "sha256": "4076e6041bedce5269c1d4e3d62f0e4213a4b2e790fe270b89b4b4f3363e08aa" + }, + { + "path": "research/crt-unary-stencil-producer/producer.py", + "usage": "input", + "git_blob": "dd357a0679c244e5d95b2b782bd70ea9f2507795", + "sha256": "8586d019a0a35390d36b944a2b764ec96682040b1abc42e29d740faf5a830bd0" + }, + { + "path": "research/crt-uniform-rom-query/PROOF.md", + "usage": "input", + "git_blob": "63b0551a7715b9b67f2b13510183254401eb082f", + "sha256": "736be5e1af590f2195e8b56b958258f0babe5cd6d2cf6f4f5023410112f4d870" + }, + { + "path": "research/crt-uniform-rom-query/machine.py", + "usage": "input", + "git_blob": "88292ce98d31d540c7dba6960bfe4c19f06a8077", + "sha256": "46ee6a635251e498ee9a5d4aff8c0e2a7f1ef2ff951e5b6a2a8953316e9cd02d" + }, + { + "path": "research/unconditional-batched-crt/CRT.md", + "usage": "input", + "git_blob": "d98dd8e368431cac33d5fc1c8c336696663641d6", + "sha256": "02c3a1e38cbee25aefe2640cc72676da62ba10eb7519fbcb9adb9d48b74eff2b" + }, + { + "path": "research/unconditional-batched-crt/NOTICE.md", + "usage": "input", + "git_blob": "886a8fdee275f01b459cbd68ae2815dc9269502f", + "sha256": "924109837e71c52392191710d49c9deb42780878d1094f0b01e8690dbe799461" + }, + { + "path": "research/unconditional-batched-crt/check_batched_crt.py", + "usage": "input", + "git_blob": "1cf78abccd5e06beecc3ed21ba55f7c03b65fdbc", + "sha256": "681e2e3d71fa74c8b9b326f3860104fd9d89590a222e26ae6ee718d1fd40ff2e" + } + ] +} diff --git a/research/crt-complete-binary-refinement/lower.py b/research/crt-complete-binary-refinement/lower.py new file mode 100644 index 0000000000..ac848895f3 --- /dev/null +++ b/research/crt-complete-binary-refinement/lower.py @@ -0,0 +1,259 @@ +"""Closed finite-value refinement of the exact PR5105 program. + +JoyboyBrian, with substantial OpenAI Codex assistance. Apache-2.0. +All enumeration below is static compilation, never an execution primitive. +""" +from itertools import product + +WIDTH = 13 +RECORDS = frozenset(('R', n) for n in range(4096)) + + +def canon(x): + if isinstance(x, bool): + return int(x) # Python source equality identifies bools with 0 and 1. + if isinstance(x, tuple): + return tuple(canon(y) for y in x) + return x + + +def operand(a, domains): + if a[0] == 'c': + return {canon(a[1])} + if a[0] == 'r': + return domains[a[1]] + if a[0] == 'tuple': + sets = [operand(x, domains) for x in a[1]] + size = 1 + for s in sets: + size *= len(s) + if size > 8192: + raise ValueError('static product exceeds explicit compilation budget') + return set(product(*sets)) + raise ValueError('unsupported operand') + + +def closure(source, roles, source_registers): + """Monotone overapproximation; undefined source operations have no successor.""" + regs = {r: {None} for r in source_registers} + tapes = {r: {'_'} for r in roles} + for r in ('G', 'H', 'K', 'Y', 'J', 'B'): + tapes[r].update(('<', '>', '1')) + tapes['rom'].update(('L', 'R', '0', '1')) + tapes['data'].update(RECORDS | {'<', '>'}) + changed = True + rounds = 0 + while changed: + changed = False + rounds += 1 + if rounds > 100: + raise ValueError('finite closure iteration budget') + for op, *a in source: + values = set() + if op == 'read': + for role in operand(a[0], regs): + if role in tapes: + values.update(tapes[role]) + dest = a[1] + elif op == 'write': + for role in operand(a[0], regs): + if role in tapes: + old = len(tapes[role]); tapes[role].update(operand(a[1], regs)) + changed |= len(tapes[role]) != old + continue + elif op == 'copy': + values = operand(a[0], regs); dest = a[1] + elif op == 'field': + values = {x[a[1]] for x in operand(a[0], regs) + if isinstance(x, tuple) and 0 <= a[1] < len(x)} + dest = a[2] + elif op in ('not', 'record', 'eq', 'ne', 'in', 'notin'): + values = {0, 1}; dest = a[-1] + elif op in ('xorbit', 'andbit', 'orbit'): + values = {'0', '1'}; dest = a[-1] + elif op in ('move', 'branch', 'jump', 'halt'): + continue + else: + raise ValueError('unsupported source opcode ' + op) + old = len(regs[dest]); regs[dest].update(values) + changed |= len(regs[dest]) != old + return regs, tapes, rounds + + +class Lower: + def __init__(self, source, roles, regs, tapes, fault=None): + self.source, self.roles, self.domains = source, tuple(sorted(roles)), regs + self.fault = fault + values = {'_', None, 0, 1, '0', '1'} + for domain in (*regs.values(), *tapes.values()): + values.update(domain) + def collect(a): + values.update(operand(a,regs)) + if a[0]=='tuple': + for x in a[1]:collect(x) + for row in source: + for a in row[1:]: + if isinstance(a, tuple) and a and a[0] in ('c', 'r', 'tuple'): + collect(a) + other = sorted(values - RECORDS - {'_'}, key=repr) + if len(other) >= 4096: + raise ValueError('nonrecord code space exhausted') + self.codes = {'_': 0, **{x: i+1 for i, x in enumerate(other)}} + self.codes.update({x: 4096+x[1] for x in RECORDS}) + self.reverse = {v: k for k, v in self.codes.items()} + self.out, self.starts, self.registers = [], [], {} + self.serial = 0 + + def emit(self, *x): + self.out.append(x) + return len(self.out)-1 + + def temp(self): + self.serial += 1 + return '$' + str(self.serial) + + def bit(self, name, j): + key = (name, j) + if key not in self.registers: + self.registers[key] = len(self.registers) + return self.registers[key] + + def setword(self, name, value): + n = self.codes[canon(value)] + for j in range(WIDTH): + self.emit('set', self.bit(name, j), (n >> j) & 1) + + def copyword(self, src, dst): + for j in range(WIDTH): + self.emit('copy', self.bit(src, j), self.bit(dst, j)) + + def equal(self, src, value=None, other=None): + flag, scratch = self.temp(), self.temp() + self.emit('set', self.bit(flag, 0), 0) + for j in range(WIDTH): + if other is None: + self.emit('xor_const', self.bit(src,j), (self.codes[value] >> j)&1, self.bit(scratch,0)) + else: + self.emit('xor', self.bit(src,j), self.bit(other,j), self.bit(scratch,0)) + self.emit('or', self.bit(flag,0), self.bit(scratch,0), self.bit(flag,0)) + self.emit('not', self.bit(flag,0), self.bit(flag,0)) + return self.bit(flag,0) + + def choose(self, tests, success, failure='reject'): + """Ordered finite decision chain. All targets resolve to literal PCs.""" + ends = [] + for test, result in tests: + flag = test() + branch = self.emit('branch', flag, None, None) + yes = len(self.out); success(result); ends.append(self.emit('jump', None)) + self.out[branch] = ('branch', flag, yes, len(self.out)) + self.emit('halt', failure) + for i in ends: + self.out[i] = ('jump', len(self.out)) + + def value(self, a): + if a[0] == 'r': + return a[1] + name = self.temp() + values = operand(a, self.domains) + if len(values) == 1: + self.setword(name, next(iter(values))) + return name + if a[0] != 'tuple': + raise ValueError('unsupported compound value') + parts = [self.value(x) for x in a[1]] + def test(v): + flag = self.bit(self.temp(), 0); self.emit('set', flag, 1) + for p, x in zip(parts, v): + eq = self.equal(p, x); self.emit('and', flag, eq, flag) + return flag + self.choose([(lambda v=v:test(v), v) for v in sorted(values,key=repr)], + lambda v:self.setword(name,v)) + return name + + def boolean(self, flag, dst, negate=False): + branch = self.emit('branch', flag, None, None) + yes = len(self.out); self.setword(dst, int(not negate)); end = self.emit('jump',None) + no = len(self.out); self.setword(dst, int(negate)) + self.out[branch] = ('branch', flag, yes, no) + self.out[end] = ('jump',len(self.out)) + + def truth(self, name): + flag = self.bit(self.temp(),0); self.emit('set',flag,1) + for v in self.codes: + if not v: + eq = self.equal(name,v); self.emit('not',eq,eq); self.emit('and',flag,eq,flag) + return flag + + def tapeop(self, op, role, payload): + def action(r): + if op == 'move': + for _ in range(WIDTH-(self.fault == 'short_stride')): + self.emit('move',r,payload) + else: + for j in range(WIDTH): + self.emit('read' if op == 'read' else 'write_reg',r,self.bit(payload,j)) + if j+1 < WIDTH:self.emit('move',r,1) + for _ in range(WIDTH-1):self.emit('move',r,-1) + values = operand(role,self.domains) + valid = sorted(values & set(self.roles)) + if len(values) == 1 and valid: + action(valid[0]); return + value = self.value(role) + targets=[self.roles[(self.roles.index(r)+1)%len(self.roles)] for r in valid] if self.fault == 'wrong_role' else valid + self.choose([(lambda r=r:self.equal(value,r),dest) for r,dest in zip(valid,targets)],action) + + def compile(self): + for op,*a in self.source: + self.serial=0 # Scratch is dead at every source instruction boundary. + self.starts.append(len(self.out)) + if op == 'copy':self.copyword(self.value(a[0]),a[1]) + elif op == 'read':self.tapeop(op,a[0],a[1]) + elif op == 'write':self.tapeop(op,a[0],self.value(a[1])) + elif op == 'move': + if a[1][0]!='c' or a[1][1] not in (-1,1):raise ValueError('nonunit move') + self.tapeop(op,a[0],a[1][1]) + elif op in ('eq','ne'): + left,right=self.value(a[0]),self.value(a[1]) + self.boolean(self.equal(left,other=right),a[2],op=='ne') + elif op in ('in','notin'): + if a[1][0]!='tuple':raise ValueError('nonliteral membership') + left=self.value(a[0]);flag=self.bit(self.temp(),0);self.emit('set',flag,0) + for x in a[1][1]: + eq=self.equal(left,other=self.value(x));self.emit('or',flag,eq,flag) + self.boolean(flag,a[2],op=='notin') + elif op == 'not':self.boolean(self.truth(self.value(a[0])),a[1],True) + elif op == 'record':self.boolean(self.bit(self.value(a[0]),12),a[1]) + elif op == 'field': + src=self.value(a[0]);valid=[x for x in operand(a[0],self.domains) if isinstance(x,tuple) and a[1]> j)&1 if name in self.domains else 0) + statuses=sorted({a[0] for op,*a in self.out if op=='halt'}) + tail={status:count+len(self.out)+i*(count+1) for i,status in enumerate(statuses)} + for op,*a in self.out: + if op=='halt': + program.append(('jump',tail[a[0]]));continue + elif op=='jump':a[0]=target(a[0]) + elif op=='branch':a[1]=target(a[1]);a[2]=target(a[2]) + program.append((op,*a)) + for status in statuses: + program.extend(('set',i,0) if self.fault!='keep_control' else ('copy',i,i) for i in range(count)) + program.append(('halt',status)) + return program,starts From 3d2bf3599eade3ac12db657ab53ddb8a63d84777 Mon Sep 17 00:00:00 2001 From: JoyboyBrian <122925040+JoyboyBrian@users.noreply.github.com> Date: Sat, 24 Oct 2026 21:01:10 -0700 Subject: [PATCH 2/2] Verify binary source boundaries with independent caller and fault controls --- .../RESULT.json | 87 +++++ .../crt-complete-binary-refinement/TASK.json | 86 +++++ .../VERIFY.json | 39 +++ .../crt-complete-binary-refinement/verify.py | 317 ++++++++++++++++++ 4 files changed, 529 insertions(+) create mode 100644 research/crt-complete-binary-refinement/RESULT.json create mode 100644 research/crt-complete-binary-refinement/TASK.json create mode 100644 research/crt-complete-binary-refinement/VERIFY.json create mode 100644 research/crt-complete-binary-refinement/verify.py diff --git a/research/crt-complete-binary-refinement/RESULT.json b/research/crt-complete-binary-refinement/RESULT.json new file mode 100644 index 0000000000..e85386210b --- /dev/null +++ b/research/crt-complete-binary-refinement/RESULT.json @@ -0,0 +1,87 @@ +{ + "status": "PASS_COMPLETE_BINARY_REFINEMENT", + "sources": { + "research/crt-binary-key-port/PROOF.md": "c1fb60178576f64f170c1c0867c2a109c15a993a7bdc3ad52e1ff70c8a58faa0", + "research/crt-binary-key-port/binary.py": "50a3dea7fc087715b4e605e85629566ed31903026540f916df6b8cbaa536182d", + "research/crt-binary-radix-consumer/PROOF.md": "b2f9230f8bd435a3fae006cd8eea760912ec2eb3eab56824411f92b2875aba6f", + "research/crt-complete-repair-control/PROOF.md": "151211f34d80c8edd03512dd18af27b9b5b1dfe6f9fda9f904bfd59c4ab1a807", + "research/crt-complete-repair-control/compiler.py": "1186cdefed22890a987c1f289290c6db4c19446a29461c1db46257f318b05156", + "research/crt-complete-repair-control/machine.py": "afa110ed2fdba62e810fd794e5fd62a07ec4caf18e8919066275523713353cc7", + "research/crt-dense-guard-scan/PROOF.md": "c075a3c261bb824884f0da9f99fed227b15f9fac087bbdeb2c2cb861d4091f11", + "research/crt-dense-guard-scan/machine.py": "1cb27312932914eb631078bd56e85feb1dc6c4191e9d1962b2cc3a7e1cfb8df7", + "research/crt-mask-repair-bridge/PROOF.md": "c74f93a65f7b28e751a9c93aa37fc7f74f7ce42cd96e31fa3d1212c94991769c", + "research/crt-mask-repair-bridge/bridge.py": "573451d94435b6096a88250ca2a9fb75f39bcfa6f0436ffe2363ee07381d8331", + "research/crt-mask-repair-bridge/key_subroutine.py": "ffdbb610be71ae20bf974946dac66b6c1b4d43739cbc3b1eb81cbbeab8784b44", + "research/crt-paid-key-service/PROOF.md": "1a4ac02653eb6c1b20807033a910f27bf9484cc972bf2629941f589275a87325", + "research/crt-paid-key-service/service.py": "ff06c6305c9f650a694e5c42baa4c7d841decf844a4f44f6776acc10a8400083", + "research/crt-unary-stencil-producer/PROOF.md": "4076e6041bedce5269c1d4e3d62f0e4213a4b2e790fe270b89b4b4f3363e08aa", + "research/crt-unary-stencil-producer/producer.py": "8586d019a0a35390d36b944a2b764ec96682040b1abc42e29d740faf5a830bd0", + "research/crt-uniform-rom-query/PROOF.md": "736be5e1af590f2195e8b56b958258f0babe5cd6d2cf6f4f5023410112f4d870", + "research/crt-uniform-rom-query/machine.py": "46ee6a635251e498ee9a5d4aff8c0e2a7f1ef2ff951e5b6a2a8953316e9cd02d", + "research/unconditional-batched-crt/CRT.md": "02c3a1e38cbee25aefe2640cc72676da62ba10eb7519fbcb9adb9d48b74eff2b", + "research/unconditional-batched-crt/NOTICE.md": "924109837e71c52392191710d49c9deb42780878d1094f0b01e8690dbe799461", + "research/unconditional-batched-crt/check_batched_crt.py": "681e2e3d71fa74c8b9b326f3860104fd9d89590a222e26ae6ee718d1fd40ff2e" + }, + "closure_rounds": 4, + "source_instructions": 8242, + "source_opcodes": { + "andbit": 200, + "branch": 1060, + "copy": 1717, + "eq": 863, + "field": 13, + "halt": 47, + "jump": 867, + "move": 1613, + "ne": 142, + "not": 9, + "notin": 1, + "orbit": 92, + "read": 887, + "record": 5, + "write": 539, + "xorbit": 187 + }, + "tape_roles": 31, + "codes": 4932, + "binary_instructions": 557123, + "control_bits": 14839, + "max_block": 101391, + "source_program_sha256": "192f2e099d8c82cfc2c4d531e615ca52ee15218e620f44df776fcee782511599", + "binary_program_sha256": "ba95a86c5e119438144119a33211d58122d638085804a0454c0e325fe6bdd2e7", + "micro": { + "cases": 63, + "binary_actions": 6457, + "mutants": [ + "short_stride", + "keep_control", + "wrong_role" + ], + "dynamic_role_pc": 899 + }, + "structural": { + "control_edges": 518607, + "dirty_initialization_bits": 14839, + "rejected": [ + "receipt_boolean", + "receipt_float", + "unknown_source_opcode", + "wrong_source_relocation" + ] + }, + "cuts": { + "producer": { + "source_boundaries": 2862, + "binary_actions": 132662, + "tape_actions": 22452, + "encoded_tapes": "4818bd8ec2b09102a7e3d66e675a3b11c199525d989d3395de0b61abb473dfaa" + }, + "actual_scanner_split_key": { + "source_boundaries": 43130, + "binary_actions": 1728409, + "tape_actions": 343742, + "encoded_tapes": "75a29b41535e58d987a34345aad8794fd2be9379ef85e9d11cebbe00f2815839" + }, + "boundary": "Key entry is source-generated and encoded once; scanner itself is not binary-replayed." + } +} diff --git a/research/crt-complete-binary-refinement/TASK.json b/research/crt-complete-binary-refinement/TASK.json new file mode 100644 index 0000000000..b5c7d75e7e --- /dev/null +++ b/research/crt-complete-binary-refinement/TASK.json @@ -0,0 +1,86 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "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": "Complete literal binary refinement of exact PR5105 program, with finite-value closure, every opcode and role dispatch, per-step simulation, cost and control lifecycle. Bounded actual cuts; no full binary layer execution.", + "scope_change_reason": "The original fixed key port and finite-symbol caller are complete; their explicit remaining binary representation obligation is now isolated.", + "bottleneck_link": "Closes a complete actual caller instruction and ownership boundary; raw compact macro and full evaluator remain external.", + "budget_minutes": 60, + "stop_rule": "Stop at this fixed real caller or a precise missing control/ownership contract.", + "outcome": "completed", + "evidence": "PROOF.md gives complete source-step refinement; RESULT.json and verify.py execute opcode controls and bounded actual producer/key cuts, not the full binary layer.", + "author": "JoyboyBrian", + "ai_assistance": "Substantial OpenAI Codex assistance", + "open_questions": [ + { + "question": "Can the complete binary layer be replayed within a deliberately allocated runtime budget?", + "why_it_matters": "This would corroborate the universal source-step proof with an end-to-end binary execution.", + "first_step": "Estimate executed bit steps using committed block bounds and source instruction census before allocating the single heavy slot.", + "blocked_by": "Billion-step full replay is outside this session budget." + }, + { + "question": "Can encoded ROM, variable geometry and raw-S production satisfy the same complete lifecycle?", + "why_it_matters": "Fixed-geometry source refinement does not discharge the uniform CRT evaluator.", + "first_step": "Pin one encoded upstream producer and its actual input contract.", + "blocked_by": "Uniform source/ROM and raw macro premises remain external." + } + ], + "coordination": { + "canonical_discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/4709#discussioncomment-19172880", + "overlap_open_prs": 342, + "overlap_discussion_records": 4736, + "overlap_utc": "2026-10-25T03:48:26.071023+00:00" + } +} diff --git a/research/crt-complete-binary-refinement/VERIFY.json b/research/crt-complete-binary-refinement/VERIFY.json new file mode 100644 index 0000000000..fc3ec55938 --- /dev/null +++ b/research/crt-complete-binary-refinement/VERIFY.json @@ -0,0 +1,39 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/crt-binary-key-port/PROOF.md", + "research/crt-binary-key-port/binary.py", + "research/crt-binary-radix-consumer/PROOF.md", + "research/crt-complete-repair-control/PROOF.md", + "research/crt-complete-repair-control/compiler.py", + "research/crt-complete-repair-control/machine.py", + "research/crt-dense-guard-scan/PROOF.md", + "research/crt-dense-guard-scan/machine.py", + "research/crt-mask-repair-bridge/PROOF.md", + "research/crt-mask-repair-bridge/bridge.py", + "research/crt-mask-repair-bridge/key_subroutine.py", + "research/crt-paid-key-service/PROOF.md", + "research/crt-paid-key-service/service.py", + "research/crt-unary-stencil-producer/PROOF.md", + "research/crt-unary-stencil-producer/producer.py", + "research/crt-uniform-rom-query/PROOF.md", + "research/crt-uniform-rom-query/machine.py", + "research/unconditional-batched-crt/CRT.md", + "research/unconditional-batched-crt/NOTICE.md", + "research/unconditional-batched-crt/check_batched_crt.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Complete static alphabet/CFG compilation, independent instruction simulation, bounded actual caller cuts, lifecycle/fault controls and frozen receipt." + } + ] +} diff --git a/research/crt-complete-binary-refinement/verify.py b/research/crt-complete-binary-refinement/verify.py new file mode 100644 index 0000000000..7e38e9fb67 --- /dev/null +++ b/research/crt-complete-binary-refinement/verify.py @@ -0,0 +1,317 @@ +"""Bounded independent source/bit simulation; never a full binary layer replay.""" +import argparse +from collections import Counter +from hashlib import sha256 +import json +from pathlib import Path +import types + +HERE=Path(__file__).resolve().parent +ROOT=HERE.parents[1] + + +def need(ok,why): + if not ok:raise ValueError(why) + + +def load(path): + module=types.ModuleType(path.stem);module.__file__=str(path) + exec(compile(path.read_bytes(),str(path),'exec'),module.__dict__) + return module + + +def authenticate(): + manifest=json.loads((HERE/'SOURCES.json').read_text()) + result={} + for row in manifest['files']: + if row['usage']=='input': + raw=(ROOT/row['path']).read_bytes() + need(sha256(raw).hexdigest()==row['sha256'],'source corruption: '+row['path']) + result[row['path']]=row['sha256'] + return result + + +def digest(value): + return sha256(repr(value).encode()).hexdigest() + + +def typed_equal(a,b): + return json.dumps(a,sort_keys=True)==json.dumps(b,sort_keys=True) + + +class Harness: + def __init__(self): + self.low=load(HERE/'lower.py') + self.source=load(ROOT/'research/crt-complete-repair-control/machine.py') + self.bits=load(ROOT/'research/crt-binary-key-port/binary.py') + self.code,self.owned,self.stages=self.source.assemble(ROOT) + self.roles=tuple(self.source.prepare(self.owned,{x:[] for x in ('G','H','K','Y','J','B','data','rom')})) + self.regs,self.tapes,self.rounds=self.low.closure(self.code,self.roles,self.source.registers(self.code)) + self.lower=self.low.Lower(self.code,self.roles,self.regs,self.tapes) + self.program,self.starts=self.lower.compile() + + def encoded(self,tapes,heads=None,lower=None): + lower=lower or self.lower + out={} + for role,cells in tapes.items(): + tape=self.bits.BitTape([b for x in cells for b in self.word(lower,x)],13*(heads or {}).get(role,0)) + out[role]=tape + return out + + @staticmethod + def word(lower,value): + n=lower.codes[lower_value(value)] + return [(n>>j)&1 for j in range(13)] + + @staticmethod + def put(machine,lower,name,value): + n=lower.codes[lower_value(value)] + for j in range(13): + if (name,j) in lower.registers:machine.registers[lower.registers[name,j]]=(n>>j)&1 + + @staticmethod + def value(machine,lower,name): + n=sum(machine.registers[lower.registers[name,j]]<pc) or target in expected or target in tails, + 'unpriced internal loop/cross-block target') + edges+=1 + if op in ('read','write_reg','move'):need(a[0] in h.roles,'literal tape role') + if op=='move':need(a[1] in (-1,1),'unit bit move') + if op=='set':need(a[1] in (0,1),'bit constant') + return edges + + +def structural(h): + edges=control_graph(h,h.program) + bad=list(h.program);pc=next(i for i in range(h.starts[0],h.starts[-1]) if bad[i][0]=='branch') + bad[pc]=('branch',bad[pc][1],h.starts[-2],h.starts[-2]) + try:control_graph(h,bad) + except ValueError:pass + else:raise ValueError('wrong source relocation accepted') + machine=h.bits.Machine(h.program,len(h.lower.registers),{}) + machine.registers[:]=[1]*len(machine.registers) + while machine.pc!=h.starts[0]:machine.step() + for (name,j),index in h.lower.registers.items(): + expected=(h.lower.codes[None]>>j)&1 if name in h.regs else 0 + need(machine.registers[index]==expected,'dirty finite control initialization') + need(not typed_equal({'count':1},{'count':True}),'typed receipt Boolean control') + need(not typed_equal({'count':1},{'count':1.0}),'typed receipt floating control') + # Entry domains must include the actual ROM markers, independently of codes. + need({'L','R','0','1','_'}<=h.tapes['rom'],'actual ROM closure alphabet') + bad=list(h.code);bad[0]=('unknown_source_op',) + try:h.low.closure(bad,h.roles,h.source.registers(h.code)) + except ValueError:pass + else:raise ValueError('unknown source opcode accepted') + return dict(control_edges=edges,dirty_initialization_bits=len(machine.registers), + rejected=['receipt_boolean','receipt_float','unknown_source_opcode','wrong_source_relocation']) + + +def actualcuts(h): + borrowed={x:['<',*('1'*v),'>','_'] for x,v in zip(('G','H','K','Y','J','B'),(2,2,6,8,2,0))} + borrowed.update(data=['<',('R',123),'>'],rom=['L',*('1'*32),'R']) + tapes=h.source.prepare(h.owned,borrowed) + producer=h.cut(1,h.stages['scanner'],tapes) + # Obtain the genuine complete scanner/split entry using the exact source. + entry,end=h.stages['key_sites'][0];snapshot={} + class Capture(Exception):pass + def capture(pc,t,heads,regs,*_): + snapshot.update(tapes={r:list(v) for r,v in t.items()},heads=dict(heads),regs=dict(regs));raise Capture + try:h.source.execute(h.code,tapes,observe={entry:capture},max_steps=4000000) + except Capture:pass + need(snapshot,'actual source key-entry capture') + key=h.cut(entry,end,snapshot['tapes'],snapshot['regs'],snapshot['heads'],budget=100000) + return dict(producer=producer,actual_scanner_split_key=key, + boundary='Key entry is source-generated and encoded once; scanner itself is not binary-replayed.') + + +def main(): + ap=argparse.ArgumentParser();ap.add_argument('--write-result',action='store_true');ap.add_argument('--light',action='store_true');args=ap.parse_args() + pins=authenticate();h=Harness() + need(len(h.lower.reverse)==len(h.lower.codes),'injective codebook') + need(all(h.lower.codes[x]==4096+x[1] for x in h.low.RECORDS),'all record encodings') + need(all((code>=4096)==(value in h.low.RECORDS) for value,code in h.lower.codes.items()),'record classifier exactness') + controls=microchecks(h) + result=dict(status='PASS_COMPLETE_BINARY_REFINEMENT',sources=pins,closure_rounds=h.rounds, + source_instructions=len(h.code),source_opcodes=dict(sorted(Counter(r[0] for r in h.code).items())), + tape_roles=len(h.roles),codes=len(h.lower.codes),binary_instructions=len(h.program), + control_bits=len(h.lower.registers),max_block=max(b-a for a,b in zip(h.starts,h.starts[1:])), + source_program_sha256=digest(h.code),binary_program_sha256=digest(h.program),micro=controls, + structural=structural(h)) + if args.light:print(json.dumps(result,indent=2));return + result['cuts']=actualcuts(h) + if args.write_result:(HERE/'RESULT.json').write_text(json.dumps(result,indent=2)+'\n') + else:need(typed_equal(json.loads((HERE/'RESULT.json').read_text()),result),'frozen typed receipt mismatch') + print(result['status'],json.dumps(result['cuts'])) + + +if __name__=='__main__':main()