From 8d778d29b9e1cf3344d21122817f0f37580a419b Mon Sep 17 00:00:00 2001 From: JoyboyBrian <122925040+JoyboyBrian@users.noreply.github.com> Date: Fri, 23 Oct 2026 01:32:06 -0700 Subject: [PATCH 1/3] =?UTF-8?q?Execute=20encoded=20Bene=C5=A1=20arena=20an?= =?UTF-8?q?d=20scalar=20control=20from=20rotation=20descriptors?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .../crt-encoded-benes-rom-producer/PROOF.md | 176 +++++++ .../microcode.py | 358 ++++++++++++++ .../vendor/pr4192-NOTICE.md | 7 + .../vendor/pr4192-PROOF.md | 258 ++++++++++ .../vendor/pr4192-verify.py | 450 ++++++++++++++++++ 5 files changed, 1249 insertions(+) create mode 100644 research/crt-encoded-benes-rom-producer/PROOF.md create mode 100644 research/crt-encoded-benes-rom-producer/microcode.py create mode 100644 research/crt-encoded-benes-rom-producer/vendor/pr4192-NOTICE.md create mode 100644 research/crt-encoded-benes-rom-producer/vendor/pr4192-PROOF.md create mode 100644 research/crt-encoded-benes-rom-producer/vendor/pr4192-verify.py diff --git a/research/crt-encoded-benes-rom-producer/PROOF.md b/research/crt-encoded-benes-rom-producer/PROOF.md new file mode 100644 index 0000000000..f3172053f0 --- /dev/null +++ b/research/crt-encoded-benes-rom-producer/PROOF.md @@ -0,0 +1,176 @@ +# Executed control for a source-bound Beneš ROM producer + +## Statement and assumptions + +Fix integers h>=1, W>=h+3, N=2^h, 1<=s<=N and a nonempty ordered +list of m offsets, m>=1, each 0<=a_i=h+3 bounds all node/index/sentinel values, and kind<=4. +No cell-tariff equality with the predecessor is asserted for this different +literal instruction encoding. + +The rotation permutation is generated directly into root P. For x=s, +keep x. Thus all padded wires are fixed. This uses encoded loops, not a +host-generated permutation or stored truth table. + +## Primitive simulation invariant + +Each scalar role is a fixed-width bit record. At the entrance and return of +`copy`, `clear`, `constant`, `inc`, `dec`, `double`, `half`, `equal`, `less` +and `zero`, all involved heads are zero. The definitions imply: + +* `inc` and `dec` propagate one carry/borrow from low to high bits; overflow + or underflow takes a rejecting halt. Valid control invariants exclude it. +* `double` shifts left with a one-bit carry; `half` shifts right and writes + zero at the highest bit. +* Equality scans every bit. `less` replaces its flag at each differing bit, + so the highest differing bit decides unsigned order. +* `copy` moves one bit at a time and returns both heads. All call sites use + distinct source and destination roles. +* `repeat` and the two while macros re-evaluate their conditions on tapes. + They are assembler macros only: their Python bodies run once to emit + fixed instructions. Runtime bounds are never host loop counts. + +All runtime register values are symbols from a fixed finite set. The only +machine instructions are one-cell read/write/move, finite-symbol assignment, +finite equality/not, a finite branch, a static jump and halt. PC/head/list +positions belong to the emulator configuration. They do not feed into a +machine operand. The interpreter watchdog is a verifier timeout, not an +accepting branch or a complexity proof. + +`access` compares each of four key words against every record, reads or +writes the value on the unique match, scans to the end even after the match, +and returns all heads. Its found flag rejects missing/duplicate matches. +There is no decoded address or host-indexed record access. Arena storage is +built by the same encoded depth/node/kind/layer/index counters. The number of +records is J=N(h^2+3h+1); each contains five W-bit words. + +## Complete source refinement + +The padded rotation is a permutation. At a node with permutation P, the +source's two matchings are x xor 1 and INV[P[x] xor 1]. The program retains +that order. A newly reached vertex receives its color **before** being pushed +onto the shared stack. The stack top is a bit record; pop decrements it, +reads the slot, and restores its sentinel N before visiting neighbours. +Every vertex is pushed once and the top never exceeds the node size or N. +The pop/colour/ordered-push transition therefore agrees with the retained +source, including coincident neighbours and parallel matching edges. + +First/last rows are color[x] xor parity(x) and color[INV[x]] xor parity(x). +The two child permutations use exactly node 2v+color[x], index floor(x/2), +value floor(P[x]/2). The source's perfect-matching argument makes each child +a permutation. Consequently the omitted redundant quadratic distinctness +scan is unnecessary for these **generated rotations** and their children; +this is not a compiler for arbitrary unvalidated supplied permutations. + +The leaf case size2 writes P[0] twice. By induction, the top-down loop +constructs the same child data and endpoint rows as PR4192. The bottom-up +loop chooses child parity x and child index floor(x/2), copies its layer, +and adds one to the parent layer index. Thus every root table equals the +canonical source table, rather than merely realizing an equivalent network. + +Each offset is compiled in a reused arena. Its full root network is appended +to an owned spool before the arena is erased. A final repeated sequential +scan transposes offset-major networks into layer-major output, iterating the original offset stream until its end marker, with no +numeric offset-count register or list-length capacity. This preserves +both list multiplicity and within-layer wire order. The selected row is +written simultaneously; it is never reconstructed from an oracle. The spool +and all scalar roles are then erased. Offsets, modulus, selector and h are +read-only throughout. This proves the stated success endpoint and ownership. + +Malformed inputs may reject with dirty owned work or nonreturned heads; +there is no arbitrary-error rollback claim. Unbounded/nonterminated records, +aliased tape roles and initially dirty owned backing are outside the domain. + +## A conservative complete instruction and storage bound + +This proof prices the new primitive program, not host execution time. +Let A=N^2+2Nh^2+(37Nh-35N)/2 be PR4192's complete logical-access bound. +The new valid-rotation path has no more accesses: it replaces root input +copies with the same N puts and omits the redundant validation gets. Each +access takes fewer than 1000 W(J+1) primitive instructions. This follows by +expanding the four key-bit loops, value loop, marker rewinds and found test; +each loop iteration has fewer than 50 instructions and each return traverses +at most W or 5WJ cells. Each other scalar macro takes fewer than 100W +instructions, except initial repeated doubling (at most 100hW). + +Arena creation/disposal uses O(WJ) instructions per offset. There are +O(A+J+N^2+Nh^2) scalar macro invocations per offset: the rotation loop has +at most N(s-1)<=N^2 iterations; source traversal loops are bounded by the +same tree/stack counts as the inherited access census. Transposition scans +mN(2h-1)^2 bits, with O(W) counter work per bit. Header, scalar-bank and +successful disposal costs are included. The deliberately loose explicit +upper bound + + T <= 10^6 W^2 (m+1) (N+1)^3 (h+1)^4 + +therefore dominates initialization, all scalar/control operations, every +arena scan, both serializations and all successful cleanup. It does not +charge borrowed payload initialization as free production; descriptor +construction is outside this interface. No comparison to E(p,ell) follows. + +Peak represented cells are at most + + 100(W+2) + 5WJ + mN(4h-1) + 10(h+1) + input_cells. + +The 100 scalar-role allowance exceeds the fixed bank. Terms include the full +arena, spool mN(2h-1), complete layer output of the same size, selected ROM +mN, markers and separators. Spool/arena ownership is not productive credit. +The retained caller may reuse the ROM, but this bound does not amortize an +unproved number of future queries. Final output disposal is a separate +literal erase scan with its own observed instruction count. + +## Actual consumer and remaining boundary + +For h=3,s=5, offsets[0,2,4,0], the output is five 32-bit layers. Selected +layer2 has target bit2 and is handed directly, as the same owned cell list, +to the unchanged #4795 Service. Its query ABI uses h_query=4,s_query=2 and +addresses the same flat 32-bit table as two rows of16; the producer used four +rows of8. The equality is of flat ordered cells, not an identification of +these different header parameters. The existing service observes the actual +current y at each of its three epochs. No query answer is supplied by the +verification oracle. The service returns the ROM unchanged; the new erase +program subsequently disposes of it and of the full layer output. + +This joins one generated actual row to the existing fixed key port. A +variable-geometry key adapter, full descriptor production from current CRT +coordinates, all five repair layers, binary lowering of the whole new +symbol machine, full E allocation and outer/native/precision contracts are +not established. The retained supplied-ROM key proof remains its own premise. diff --git a/research/crt-encoded-benes-rom-producer/microcode.py b/research/crt-encoded-benes-rom-producer/microcode.py new file mode 100644 index 0000000000..052b01a83b --- /dev/null +++ b/research/crt-encoded-benes-rom-producer/microcode.py @@ -0,0 +1,358 @@ +"""Fixed bit-symbol microcode for the missing PR4192 scalar/arena boundary. + +JoyboyBrian, substantial OpenAI assistance. Apache-2.0. +""" + +class Builder: + def __init__(self): + self.code=[]; self.labels={}; self.serial=0 + def label(self, tag='l'): + self.serial+=1; return f'{tag}_{self.serial}' + def mark(self, label): self.labels[label]=len(self.code) + def e(self, op, *args): self.code.append((op,*args)) + def branch(self, reg, value, yes, no): self.e('branch',reg,value,yes,no) + def finish(self): + out=[] + for op,*a in self.code: + if op=='jump': a[0]=self.labels[a[0]] + if op=='branch': a[2]=self.labels[a[2]];a[3]=self.labels[a[3]] + out.append((op,*a)) + return tuple(out) + def rewind(self, role): + loop,back,done=[self.label() for _ in range(3)] + self.mark(loop);self.e('read',role,'s');self.branch('s','L',done,back) + self.mark(back);self.e('move',role,-1);self.e('jump',loop);self.mark(done) + def each(self, role, body): + loop,more,done=[self.label() for _ in range(3)] + self.e('move',role,1);self.mark(loop);self.e('read',role,'s');self.branch('s','R',done,more) + self.mark(more);body();self.e('move',role,1);self.e('jump',loop) + self.mark(done);self.rewind(role) + def clear(self, role): self.each(role,lambda:self.e('write',role,'0')) + def copy(self, src, dst): + self.e('move',dst,1) + def body():self.e('read',src,'bit');self.e('write_reg',dst,'bit');self.e('move',dst,1) + self.each(src,body);self.rewind(dst) + def xor1(self, role): + self.e('move',role,1);self.e('read',role,'bit');self.e('not','bit','bit');self.e('write_reg',role,'bit');self.e('move',role,-1) + def inc(self, role): + loop,zero,one,overflow,done=[self.label() for _ in range(5)] + self.e('move',role,1);self.mark(loop);self.e('read',role,'bit');self.branch('bit','R',overflow,zero+'_test') + self.mark(zero+'_test');self.branch('bit','0',zero,one) + self.mark(zero);self.e('write',role,'1');self.e('jump',done) + self.mark(one);self.e('write',role,'0');self.e('move',role,1);self.e('jump',loop) + self.mark(overflow);self.e('halt','overflow');self.mark(done);self.rewind(role) + def dec(self, role): + loop,zero,one,underflow,done=[self.label() for _ in range(5)] + self.e('move',role,1);self.mark(loop);self.e('read',role,'bit');self.branch('bit','R',underflow,zero+'_test') + self.mark(zero+'_test');self.branch('bit','0',zero,one) + self.mark(one);self.e('write',role,'0');self.e('jump',done) + self.mark(zero);self.e('write',role,'1');self.e('move',role,1);self.e('jump',loop) + self.mark(underflow);self.e('halt','underflow');self.mark(done);self.rewind(role) + def equal(self, left, right, flag): + self.e('set',flag,'1');self.e('move',right,1) + def body(): + same,diff,after=[self.label() for _ in range(3)] + self.e('read',left,'a');self.e('read',right,'b');self.e('eq','a','b','test');self.branch('test','1',same,diff) + self.mark(diff);self.e('set',flag,'0');self.e('jump',after);self.mark(same);self.mark(after);self.e('move',right,1) + self.each(left,body);self.rewind(right) + def zero(self, role, flag): + self.e('set',flag,'1') + def body(): + no,yes=[self.label() for _ in range(2)] + self.e('read',role,'bit');self.branch('bit','0',yes,no);self.mark(no);self.e('set',flag,'0');self.mark(yes) + self.each(role,body) + def constant(self, role, value): + self.clear(role) + self.e('move',role,1) + for bit in bin(value)[:1:-1]:self.e('write',role,bit);self.e('move',role,1) + self.rewind(role) + def access(self, keys, put=False): + """Scan original PR4192 four-key/one-value records, all heads returned.""" + loop,record,end,missing=[self.label() for _ in range(4)] + self.e('set','found','0');self.e('move','arena',1);self.mark(loop);self.e('read','arena','s');self.branch('s','R',end,record) + self.mark(record);self.e('set','match','1') + for key in keys: + def body(key=key): + same,diff,after=[self.label() for _ in range(3)] + self.e('read',key,'a');self.e('read','arena','b');self.e('eq','a','b','test');self.branch('test','1',same,diff) + self.mark(diff);self.e('set','match','0');self.e('jump',after);self.mark(same);self.mark(after);self.e('move','arena',1) + self.each(key,body) + selected,skip,after=[self.label() for _ in range(3)] + self.branch('match','1',selected,skip);self.mark(selected) + unique=self.label();self.branch('found','0',unique,missing);self.mark(unique);self.e('set','found','1') + def valuebody(): + if put:self.e('read','value','bit');self.e('write_reg','arena','bit') + else:self.e('read','arena','bit');self.e('write_reg','value','bit') + self.e('move','arena',1) + self.each('value',valuebody);self.e('jump',after);self.mark(skip) + self.each('value',lambda:self.e('move','arena',1));self.mark(after);self.e('jump',loop) + self.mark(end);self.rewind('arena');ok=self.label();self.branch('found','1',ok,missing) + self.mark(missing);self.e('halt','missing_or_duplicate_record');self.mark(ok) + + +def cycle_program(): + """One exact PR4192 pop and its ordered two-neighbour visits; no host scalars.""" + b=Builder();keys=('node','kind','layer','index') + def get(kind,index,dst,node='root'): + b.copy(node,'node');b.constant('kind',kind);b.clear('layer');b.copy(index,'index');b.access(keys);b.copy('value',dst) + def put(kind,index,src,node='root'): + b.copy(node,'node');b.constant('kind',kind);b.clear('layer');b.copy(index,'index');b.copy(src,'value');b.access(keys,True) + b.dec('top');get(4,'top','x','zero');put(4,'top','n','zero') + for edge in (0,1): + if edge==0:b.copy('x','other');b.xor1('other') + else:get(0,'x','other');b.xor1('other');get(1,'other','other') + get(2,'x','opposite');b.xor1('opposite');get(2,'other','color') + b.equal('color','n','uncolored');fresh,old,done=[b.label() for _ in range(3)] + b.branch('uncolored','1',fresh,old);b.mark(fresh) + put(2,'other','opposite');put(4,'top','other','zero');b.inc('top');b.e('jump',done) + b.mark(old);b.equal('color','opposite','consistent');good=b.label();b.branch('consistent','1',good,'inconsistent');b.mark(good);b.mark(done) + b.e('halt','accept');b.mark('inconsistent');b.e('halt','inconsistent_color') + return b.finish() + + +def execute(program, tapes, max_steps=20000000): + """Only fixed-symbol instructions; host objects are emulator configurations.""" + heads={r:0 for r in tapes};regs={};pc=steps=0 + while steps floor(P[x]/2)` is therefore a +permutation on m/2 wires. This proves child validation and permits +induction. Distinct child calls share no state: replacing source DFS +recursion by top-down construction and bottom-up assembly preserves +the returned tables byte for byte. The first/last tables and child +selector use precisely the source formulas. + +Induction gives the desired permutation endpoint. First and last +tables are equal on the two wires of their target pair because +matching colors differ. An interior table inherits target independence +from its child: flipping its higher target bit preserves the selected +child parity. Thus each returned queried bit is independent of its +own active target bit. This is a theorem about the component; it +does not establish the full CRT caller's simultaneous target omission. + +## 4. Traffic, scalar lowering and quantified bound + +There are three separate statements: the **executed arena/key cell +invoice**, the **written bounded-scalar lowering**, and the resulting +**uniform asymptotic bit bound**. The Python simulator is not a +complete finite-state transition-table certificate. + +For a logical arena access, the arena/key tapes execute exactly + +``` +26wJ + 25w read/write/one-cell-head actions. (2) +``` + +Arena key reads cost `8wJ`; unmatched value skips plus the matching +read/write cost `wJ+w`; arena return costs `5wJ`. Key comparisons +read/return `12wJ`, and constructing/clearing/returning its key costs +24w. Sum these terms to obtain (2). Initialization and final arena +erasure/returns add `6B`. The modeled protected input read/return costs `3Nh`; +this excludes the host pre-admission length/bit-format checks. Their sequential +implementation is separately charged in the written scalar lowering below. +Owned network writing/return costs `3(2h-1)N`. Each complete query scan, +return and one-bit owned output costs exactly `3(2h-1)N+3` tape actions. +These exact numbers exclude scalar instruction work, not its cost. + +The finite simulator batches a contiguous block read/write/move by +charging the corresponding number of repeated one-cell operations. +Such methods advance from the current head only. An expanded one-cell +execution is checked against the batched version on the same case. +They have identical tape contents, heads and traffic. Byte slices used +to batch those moves are not indexed logical-array access instructions. + +To lower the remaining control, use a fixed bank of O(1) w-bit +registers with binary counters. Every integer comparison, copy, +increment, halving, parity/XOR, add, or schoolbook product used here +has a fixed sequential implementation in O(w²) time and O(w²) scratch, +including local head returns. Key equality is a streaming equality +flag, not an uncharged comparison of host strings. Input bit-format +checks, record construction, all loop/index/key generation and query +selection counters are charged by the same conservative envelope. +The Python integer mirrors are observations of this bounded control; +they are not treated as unit-cost machine arithmetic. +The bank explicitly includes candidate and supplied four-word key +buffers, the decoded value, parameters, node/depth/layer/index/top +counters and a fixed number of temporary arithmetic words. These +are O(1) fixed-width roles, not host lists growing with N. Reading +encoded parameters and clearing/returning every such private role +are included in the envelope. + +The width also covers full arena offsets, rather than only wire IDs: + +``` +B <= 20 * 2^p * (p+2)^3 + <= 160 * 2^(4p) < 2^(4p+8) = 2^w. (3) +``` + +Here `p+2<=2^(p+1)` for p>=1. All node IDs, values, sentinels, +depth/layer indices, DFS tops and record/cell loop counters fit in w +bits. Observer-only accumulated receipt counters need not be runtime +registers. A product may use two w-bit registers while being reduced +to a known in-range result. No growing collection of scalar registers +is hidden in the bound. + +Let A be the number of logical arena accesses. Across depths, total +node-size is Nh. Pairwise validation uses `N²-N-Nh/2` comparisons; +initial reads add Nh. At a nonleaf node with m wires and c components, +coloring uses m initial tests, 2c component-start accesses, 2m stack +pop/clear accesses, 6m edge accesses and `2(m-c)` discovery writes: +exactly 11m. Inverse and first/last/child construction add 2m and 7m, +giving exactly 20m nonleaf accesses. Bottom-up assembly uses +`2N(h-1)²` accesses. Root loading/serialization add `N+(2h-1)N`; +leaves add `3N/2`. Thus the exact valid-input census and a convenient +conservative bound are + +``` +A = N² + 2Nh² + (37Nh-35N)/2, +A <= N² + 2Nh² + 24Nh + 3N = O(N²(p+2)²). (4) +``` + +The displayed bound is conservative; it is derived from the loops, +not fitted to finite receipts. Loop control outside scans has +O(A+J) iterations. Scan/key comparison control has O(B) elementary +cell/word iterations per access. Charging each bounded scalar +instruction by O(w²), including its register access, gives + +``` +T_compile = O((A+J+1) B (p+2)²) + = O(N³ (p+2)^7), (5) +visited space = O(B+(p+2)²+Nh) = O(N(p+2)^3). (6) +``` + +Owned output and protected input are included in visited space. +The fixed inventory is the arena, reused key tape, input, owned +output, and a fixed scalar-work bank. The queried-bit interface uses +the protected output, one new owned bit, and that same fixed bank; +its time O(N(p+2)^3) is absorbed by (5). Register-work erasure/returns +are included in the scalar envelope. All parameters have one uniform +encoded implementation, independent of input size. + +For the source family `1<=h<=ell<=p`, (5) is bounded by +`O(2^(3ell)(p+2)^7)`, hence by the stated `O(2^(4ell)(p+2)^16)` E +allowance after a fixed constant. Even O(p) such component invocations +fit that allowance. This comparison does **not** certify all the +other work charged to E: CRT reconstruction/modular inversion, +transported descriptors, macro inverse keys, parameter generation +and the complete evaluator remain separate obligations. + +## 5. Corroboration and remaining boundary + +`verify.py` checks exact retained source bytes before calling its +reference compiler. Its executed arena traffic covers every get/put, +all DFS data, table serialization, erasure and head returns. Scalar +microcode is justified by the written construction above; its complete +literal transition table is not emitted or executed. No native or +full outer replay is represented by these tests. + +Finite cases include all permutations on two/four wires, modular +rotations and other eight/sixteen-wire permutations. Every output +table is compared exactly to the retained source, every query and +its target independence is checked, and every wire endpoint is +checked. Mutation/admission controls cover malformed encodings, +duplicate permutations, an incorrect matching edge, and missing +arena/query head returns. All checks remain active under Python -O. + +The result is a scoped constructive component proof plus independently +replayable corroboration. It is not a complete CRT evaluator, physical +ordinary interchange, native/precision closure, multiplication theorem +or selected-frontier change. diff --git a/research/crt-encoded-benes-rom-producer/vendor/pr4192-verify.py b/research/crt-encoded-benes-rom-producer/vendor/pr4192-verify.py new file mode 100644 index 0000000000..e79a9ce3f3 --- /dev/null +++ b/research/crt-encoded-benes-rom-producer/vendor/pr4192-verify.py @@ -0,0 +1,450 @@ +"""Uniform sequential-arena Beneš component: cell/head model and scoped proof. + +Block tape methods batch repeated ONE-CELL operations, charging each cell. +They never perform an indexed arena lookup. Bounded scalar control is mirrored +by Python integers; its bit lowering is proved separately in PROOF.md. +""" + +import argparse +import hashlib +import itertools +import json +from pathlib import Path +import sys +import types + + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +P, INV, COLOR, OUT, STACK = range(5) + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def word(value, width): + need(isinstance(value, int) and 0 <= value < (1 << width), "encoded word range") + return format(value, "0%db" % width).encode() + + +class Tape: + """Alphabet {0,1,blank}, implicit left marker, one sequential head.""" + + def __init__(self, data=b"", expanded=False): + self.data = bytearray(data) + self.head = self.actions = 0 + self.expanded = expanded + + def read(self, count): + need(0 <= count and self.head + count <= len(self.data), "tape read bounds") + if self.expanded: + result = bytearray() + for _ in range(count): + result.append(self.data[self.head]) + self.head += 1 + self.actions += 2 + return bytes(result) + result = bytes(self.data[self.head:self.head + count]) + self.head += count + self.actions += 2 * count # count repetitions of READ; RIGHT. + return result + + def write(self, data): + if self.expanded: + for cell in data: + if self.head == len(self.data): + self.data.append(cell) + else: + self.data[self.head] = cell + self.head += 1 + self.actions += 2 + return + stop = self.head + len(data) + self.data[self.head:stop] = data + self.head = stop + self.actions += 2 * len(data) + + def skip(self, count): + need(0 <= count and self.head + count <= len(self.data), "tape move bounds") + if self.expanded: + for _ in range(count): + self.head += 1 + self.actions += 1 + else: + self.head += count + self.actions += count # count one-cell RIGHT operations. + + def rewind(self): + if self.expanded: + while self.head: + self.head -= 1 + self.actions += 1 + else: + self.actions += self.head + self.head = 0 + + def clear(self): + need(self.head == 0, "clear starts at left marker") + self.write(bytes(len(self.data))) # NUL encodes blank, distinct from ASCII 0/1. + self.rewind() + + +def descriptors(h): + n = 1 << h + for depth in range(h): + size = n >> depth + height = h - depth + for node in range(1 << depth, 1 << (depth + 1)): + for kind in (P, INV, COLOR): + for index in range(size): + yield (node, kind, 0, index), n if kind == COLOR else 0 + for layer in range(2 * height - 1): + for index in range(size): + yield (node, OUT, layer, index), 0 + for index in range(n): + yield (0, STACK, 0, index), n + + +class Arena: + """Fixed-width tagged records; EVERY get/put scans all records and returns.""" + + def __init__(self, h, p, expanded=False): + self.h, self.p, self.width = h, p, 4 * p + 8 + self.tape = Tape(expanded=expanded) + self.key_tape = Tape(expanded=expanded) + self.calls = self.records_scanned = self.scan_actions = 0 + self.key_actions = 0 + self.kinds = {"get": 0, "put": 0} + self.count = 0 + for key, initial in descriptors(h): + self.tape.write(b"".join(word(v, self.width) for v in key) + word(initial, self.width)) + self.count += 1 + self.tape.rewind() + n = 1 << h + need(self.count == n * (h * h + 3 * h + 1), "exact flattened arena census") + self.length = len(self.tape.data) + need(self.length == 5 * self.width * self.count, "fixed-width arena size") + + def access(self, key, value=None, omit_return=False): + need(self.tape.head == 0, "arena operation must start at left marker") + encoded = b"".join(word(v, self.width) for v in key) + key_tape = self.key_tape # One reused physical scratch tape, never a tape per call. + key_start = key_tape.actions + key_tape.write(encoded) + key_tape.rewind() + start = self.tape.actions + answer = None + found = 0 + for _ in range(self.count): + candidate = self.tape.read(4 * self.width) + supplied = key_tape.read(4 * self.width) + key_tape.rewind() + if candidate == supplied: + found += 1 + if value is None: + answer = int(self.tape.read(self.width), 2) + else: + self.tape.write(word(value, self.width)) + else: + self.tape.skip(self.width) + self.records_scanned += 1 + if not omit_return: + self.tape.rewind() + key_tape.clear() + need(found == 1, "tagged record must exist exactly once") + self.calls += 1 + self.kinds["get" if value is None else "put"] += 1 + self.scan_actions += self.tape.actions - start + self.key_actions += key_tape.actions - key_start + need(all(cell == 0 for cell in key_tape.data) and key_tape.head == 0, + "key scratch must be cleared/returned") + return answer + + def get(self, node, kind, index, layer=0): + return self.access((node, kind, layer, index)) + + def put(self, node, kind, index, value, layer=0): + self.access((node, kind, layer, index), value) + + def finish(self): + need(self.tape.head == 0, "arena final head return") + self.tape.clear() + need(all(cell == 0 for cell in self.tape.data), "private arena must be erased") + need(self.records_scanned == self.calls * self.count, "every logical access is a full scan") + # One matching value read/write adds w beyond the unmatched skip. + # The key tape is written, returned, reread/returned N times, erased/returned. + expected = self.calls * (26 * self.width * self.count + 25 * self.width) + need(self.scan_actions + self.key_actions == expected, "complete scan/key/head-return invoice") + return {"record_width_bits": 5 * self.width, + "word_width_bits": self.width, "arena_records": self.count, + "arena_cells": self.length, "logical_accesses": self.calls, + "get_calls": self.kinds["get"], "put_calls": self.kinds["put"], + "records_scanned": self.records_scanned, + "arena_and_key_scan_actions": self.scan_actions + self.key_actions, + "arena_initialization_cleanup_actions": 6 * self.length, + "arena_and_key_tape_actions": self.tape.actions + self.key_actions, + "private_arena_erased": True, "private_heads_returned": True} + + +def compile_stream(input_bits, h, p, expanded=False, wrong_neighbor=False): + """Uniform valid-input compiler; no host recursion, no indexed arena accesses. + + Input is the protected h-bit encoding of N permutation entries. Output is + the owned concatenation of the 2h-1 root switch tables, N bits per layer. + """ + need(isinstance(h, int) and isinstance(p, int) and 1 <= h <= p, "1<=h<=p") + n = 1 << h + need(len(input_bits) == n * h and all(cell in (48, 49) for cell in input_bits), + "complete binary permutation encoding") + incoming = Tape(input_bits, expanded=expanded) + arena = Arena(h, p, expanded) + for index in range(n): + arena.put(1, P, index, int(incoming.read(h), 2)) + incoming.rewind() + pushes = pops = max_stack = validation_pairs = 0 + + # Top-down recursion-tree schedule, not Python recursive calls. + for depth in range(h): + size = n >> depth + height = h - depth + for node in range(1 << depth, 1 << (depth + 1)): + # Explicit quadratic validation replaces the source's sorted call. + for x in range(size): + px = arena.get(node, P, x) + need(px < size, "permutation range") + for y in range(x): + need(arena.get(node, P, y) != px, "permutation distinctness") + validation_pairs += 1 + if size == 2: + bit = arena.get(node, P, 0) + arena.put(node, OUT, 0, bit) + arena.put(node, OUT, 1, bit) + continue + for x in range(size): + arena.put(node, INV, arena.get(node, P, x), x) + for initial in range(size): + if arena.get(node, COLOR, initial) != n: + continue + arena.put(node, COLOR, initial, 0) + top = 0 + arena.put(0, STACK, top, initial) + top += 1 + pushes += 1 + while top: + max_stack = max(max_stack, top) + top -= 1 + x = arena.get(0, STACK, top) + arena.put(0, STACK, top, n) + pops += 1 + for edge in (0, 1): + other = (x ^ 1 if edge == 0 else + arena.get(node, INV, arena.get(node, P, x) ^ (0 if wrong_neighbor else 1))) + opposite = arena.get(node, COLOR, x) ^ 1 + color = arena.get(node, COLOR, other) + if color == n: + arena.put(node, COLOR, other, opposite) + need(top < n, "encoded DFS capacity") + arena.put(0, STACK, top, other) + top += 1 + pushes += 1 + else: + need(color == opposite, "two perfect matching color constraints") + for x in range(size): + color = arena.get(node, COLOR, x) + arena.put(node, OUT, x, color ^ (x & 1), layer=0) + inverse = arena.get(node, INV, x) + last = arena.get(node, COLOR, inverse) ^ (x & 1) + arena.put(node, OUT, x, last, layer=2 * height - 2) + # Each input pair has exactly one representative of each color. + arena.put(2 * node + color, P, x // 2, arena.get(node, P, x) // 2) + + # Bottom-up assembly of complete child tables. + for depth in reversed(range(h - 1)): + size = n >> depth + height = h - depth + for node in range(1 << depth, 1 << (depth + 1)): + for layer in range(2 * height - 3): + for x in range(size): + value = arena.get(2 * node + (x & 1), OUT, x // 2, layer=layer) + arena.put(node, OUT, x, value, layer=layer + 1) + need(pushes == pops and max_stack <= n, "encoded DFS stack balanced") + # Serialize the OWNED root output before erasing every private arena cell. + output = Tape(expanded=expanded) + for layer in range(2 * h - 1): + for x in range(n): + output.write(word(arena.get(1, OUT, x, layer), 1)) + output.rewind() + # Observer gate: independently derived from validation/tree/DFS/merge sums. + expected_accesses = n * n + 2 * n * h * h + (37 * n * h - 35 * n) // 2 + need(arena.calls == expected_accesses, "derived exact logical-access census") + invoice = arena.finish() + invoice.update({"h": h, "p": p, "wires": n, + "input_bits": len(input_bits), "input_tape_actions": incoming.actions, + "owned_output_bits": len(output.data), "owned_output_tape_actions": output.actions, + "validation_pairs": validation_pairs, + "dfs_pushes": pushes, "dfs_pops": pops, "maximum_dfs_entries": max_stack}) + need(incoming.head == output.head == 0 and bytes(incoming.data) == input_bits, + "protected source/owned output return contract") + return output, invoice + + +def query_stream(network, h, layer, address, omit_return=False): + """Read one queried bit by a complete sequential scan, protecting network.""" + n = 1 << h + need(0 <= layer < 2 * h - 1 and 0 <= address < n, "query domain") + need(network.head == 0 and len(network.data) == n * (2 * h - 1), "complete network input") + selected = layer * n + address # bounded scalar multiplication; proof charges it. + before = network.actions + answer = Tape(expanded=network.expanded) + for index in range(len(network.data)): + value = network.read(1) + need(value in (b"0", b"1"), "binary network entry") + if index == selected: + answer.write(value) + if not omit_return: + network.rewind() + answer.rewind() + need(len(answer.data) == 1 and answer.data[0] in (48, 49), "owned query bit exists") + return answer, network.actions - before + answer.actions + + +def unpack(network, h): + """Observer only: compare owned encoded output to the retained source API.""" + n = 1 << h + schedule = list(range(h)) + list(reversed(range(h - 1))) + return [(bit, tuple(int(chr(v)) for v in network.data[layer * n:(layer + 1) * n])) + for layer, bit in enumerate(schedule)] + + +def run_case(permutation, p, source, expanded=False): + n = len(permutation) + h = n.bit_length() - 1 + incoming = b"".join(word(x, h) for x in permutation) + output, invoice = compile_stream(incoming, h, p, expanded) + expected = source.benes(permutation) + need(unpack(output, h) == expected, "byte-exact retained compiler output") + before = bytes(output.data) + queries = steps = 0 + for layer, (bit, table) in enumerate(expected): + for address in range(n): + encoded_value, actions = query_stream(output, h, layer, address) + value = int(bytes(encoded_value.data), 2) # Observer of the owned one-bit output. + need(value == table[address] == table[address ^ (1 << bit)], "exact queried target-independent bit") + need(actions == 3 * len(output.data) + 3, "complete query scan, owned bit and return") + queries += 1 + steps += actions + need(bytes(output.data) == before and output.head == 0, "query protects encoded network") + for address in range(n): + need(source.run_network(unpack(output, h), address) == permutation[address], "permutation endpoint") + invoice.update({"queries": queries, "query_tape_actions": steps, + "owned_output_sha256": hashlib.sha256(before).hexdigest()}) + return invoice + + +def rejected(call, label): + try: + call() + except ValueError: + return label + raise ValueError("negative control accepted: " + label) + + +def finite(source): + cases = [] + for n in (2, 4): + cases.extend(("all_permutations", tuple(p), n.bit_length() - 1) + for p in itertools.permutations(range(n))) + for n, moduli in ((4, (2, 3)), (8, (5, 7)), (16, (11,))): + for modulus in moduli: + offsets = range(modulus) if n <= 8 else (0, 1, 10) + cases.extend(("modular_rotation", source.rotation(n, modulus, c), n.bit_length() - 1) + for c in offsets) + cases.extend(("arbitrary", p, 3) for p in + ((7, 0, 6, 1, 5, 2, 4, 3), (1, 4, 7, 2, 5, 0, 3, 6))) + cases.append(("wider_parameter", (3, 2, 0, 1), 7)) + receipts = [] + digest = hashlib.sha256() + categories = {} + for category, permutation, p in cases: + invoice = run_case(permutation, p, source) + categories[category] = categories.get(category, 0) + 1 + digest.update(json.dumps([list(permutation), invoice], sort_keys=True).encode() + b"\n") + receipts.append(invoice) + # Compare expanded one-cell execution with batched sequential macros. + example = (2, 0, 3, 1) + fast = run_case(example, 2, source) + expanded = run_case(example, 2, source, expanded=True) + need(fast == expanded, "expanded cell execution matches batched macro trace") + return {"cases": len(cases), "categories": categories, + "permutation_endpoints": sum(r["wires"] for r in receipts), + "queried_control_bits": sum(r["queries"] for r in receipts), + "logical_accesses": sum(r["logical_accesses"] for r in receipts), + "records_scanned": sum(r["records_scanned"] for r in receipts), + "arena_and_key_tape_actions": sum(r["arena_and_key_tape_actions"] for r in receipts), + "maximum_arena_cells": max(r["arena_cells"] for r in receipts), + "maximum_dfs_entries": max(r["maximum_dfs_entries"] for r in receipts), + "expanded_one_cell_case": list(example), "receipt_sha256": digest.hexdigest(), + "largest_case": max(receipts, key=lambda row: row["wires"]), + "wider_parameter_case": receipts[-1]} + + +def mutations(source): + failures = [] + failures.append(rejected(lambda: compile_stream(word(0, 2) * 4, 2, 2), "duplicate input permutation")) + failures.append(rejected(lambda: compile_stream(b"001", 2, 2), "incomplete input encoding")) + failures.append(rejected(lambda: compile_stream(b"0110", 2, 1), "h exceeds p")) + failures.append(rejected(lambda: compile_stream(b"00100111", 2, 2, wrong_neighbor=True), + "wrong inverse-permutation matching edge")) + arena = Arena(1, 1) + arena.access((1, P, 0, 0), omit_return=True) + need(arena.tape.head != 0, "missing arena return mutant detected") + failures.append("missing arena head return") + network, _ = compile_stream(b"01", 1, 1) + _, actions = query_stream(network, 1, 0, 0, omit_return=True) + need(network.head != 0 and actions != 3 * len(network.data) + 3, "missing query return tariff detected") + failures.append("missing query return and tariff") + network, _ = compile_stream(b"01", 1, 1) + network.data[1] = 50 # A nonselected entry is not a binary bit. + failures.append(rejected(lambda: query_stream(network, 1, 0, 0), "nonselected nonbinary network entry")) + return failures + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write-result", action="store_true") + args = parser.parse_args() + pins = json.loads((PACKAGE / "SOURCE-PINS.json").read_text()) + authenticated = {} + for row in pins: + data = (ROOT / row["path"]).read_bytes() + need(hashlib.sha256(data).hexdigest() == row["sha256"], "source SHA256: " + row["path"]) + need(hashlib.sha1(f"blob {len(data)}\0".encode() + data).hexdigest() == row["git_blob"], + "source Git blob: " + row["path"]) + authenticated[row["path"]] = data + path = "research/unconditional-batched-crt/check_batched_crt.py" + module = types.ModuleType("_pinned_benes_scan_reference") + module.__file__ = str(ROOT / path) + sys.modules[module.__name__] = module + exec(compile(authenticated[path], module.__file__, "exec"), module.__dict__) + result = {"schema_version": 1, "result": "PASS_UNIFORM_BENES_SCAN_COMPONENT", + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "source_inputs_checked": len(authenticated), "finite": finite(module), + "negative_controls": mutations(module), + "limitations": ["Executed model charges sequential tape cells/heads; bounded scalar lowering is the written proof.", + "Canonical header decoding and pre-admission format checks are written lowerings, not executed microcode.", + "No literal complete finite-state transition table or proof-assistant formalization.", + "Beneš component only; no full CRT arithmetic/control evaluator or production placement.", + "No ordinary interchange, precision/native/outer multiplication theorem or new kappa."]} + output = PACKAGE / "RESULT.json" + if args.write_result: + output.write_text(json.dumps(result, indent=2) + "\n") + else: + need(json.loads(output.read_text()) == result, "stored receipt differs from replay") + print(json.dumps({"result": result["result"], "cases": result["finite"]["cases"], + "logical_accesses": result["finite"]["logical_accesses"]}, sort_keys=True)) + + +if __name__ == "__main__": + main() From 16608add33a20853fb08709b529dcaa7b8a300d7 Mon Sep 17 00:00:00 2001 From: JoyboyBrian <122925040+JoyboyBrian@users.noreply.github.com> Date: Fri, 23 Oct 2026 01:39:19 -0700 Subject: [PATCH 2/3] Join generated ROM to actual key and record source-bound replay controls --- .../crt-encoded-benes-rom-producer/PROOF.md | 4 +- .../crt-encoded-benes-rom-producer/README.md | 91 ++++++++ .../RESULT.json | 219 ++++++++++++++++++ .../SOURCES.json | 96 ++++++++ .../crt-encoded-benes-rom-producer/TASK.json | 87 +++++++ .../VALIDATION.md | 11 + .../VERIFY.json | 41 ++++ .../crt-encoded-benes-rom-producer/verify.py | 146 ++++++++++++ 8 files changed, 693 insertions(+), 2 deletions(-) create mode 100644 research/crt-encoded-benes-rom-producer/README.md create mode 100644 research/crt-encoded-benes-rom-producer/RESULT.json create mode 100644 research/crt-encoded-benes-rom-producer/SOURCES.json create mode 100644 research/crt-encoded-benes-rom-producer/TASK.json create mode 100644 research/crt-encoded-benes-rom-producer/VALIDATION.md create mode 100644 research/crt-encoded-benes-rom-producer/VERIFY.json create mode 100644 research/crt-encoded-benes-rom-producer/verify.py diff --git a/research/crt-encoded-benes-rom-producer/PROOF.md b/research/crt-encoded-benes-rom-producer/PROOF.md index f3172053f0..cdd530c668 100644 --- a/research/crt-encoded-benes-rom-producer/PROOF.md +++ b/research/crt-encoded-benes-rom-producer/PROOF.md @@ -160,8 +160,8 @@ literal erase scan with its own observed instruction count. ## Actual consumer and remaining boundary For h=3,s=5, offsets[0,2,4,0], the output is five 32-bit layers. Selected -layer2 has target bit2 and is handed directly, as the same owned cell list, -to the unchanged #4795 Service. Its query ABI uses h_query=4,s_query=2 and +layer index 2 is handed directly, as the same owned cell list, to the +unchanged #4795 Service with target bit position 2. ROM values remain 0 or 1. Its query ABI uses h_query=4,s_query=2 and addresses the same flat 32-bit table as two rows of16; the producer used four rows of8. The equality is of flat ordered cells, not an identification of these different header parameters. The existing service observes the actual diff --git a/research/crt-encoded-benes-rom-producer/README.md b/research/crt-encoded-benes-rom-producer/README.md new file mode 100644 index 0000000000..b6f478f868 --- /dev/null +++ b/research/crt-encoded-benes-rom-producer/README.md @@ -0,0 +1,91 @@ +# Executed finite-control CRT Beneš ROM producer + +This closes a supplied-ROM boundary left by #4795/#4982/#5015. A single fixed +finite-symbol program reads encoded rotation descriptors, executes the retained +Beneš construction with encoded scalar registers and an explicit stack, writes +all canonical switch layers and one selected ROM row, and returns every head +with private backing erased. The actual selected row is handed directly to the +unchanged #4795 key service; its three current-state queries read those generated +cells. Output disposal is also executed. No new kappa is claimed. + +The source fixture is h=3,N=8,s=5,offsets[0,2,4,0]: five 32-bit layers, including +the duplicate offset and padded wires. An independent retained source compiler +checks every bit. The same static program also covers variable h/modulus/list +length; the proof is for every finite nonempty offset list in the declared ABI, +not an inference from the fixtures. In particular a 17-element list works with +W=4: list traversal is marker-driven and has no W-bit count limit. + +ToikY's #4192 already supplies the encoded arena schedule, explicit DFS stack, +canonical source equivalence and cell invoice. We retain that work and its +notice. Its simulator mirrors scalar control in host integers. This package +executes those missing decisions as literal single-cell instructions; no decoded +h, index, color, stack top, address or variable loop bound enters the runtime. +The Python assembler has no instance parameters. Interpreter positions and +verification oracles are observer machinery only. + +## Contract and full local bill + +Inputs use padded W-bit little-endian records with W>=h+3, 1<=s<=2^h and +offsets in [0,s). Four borrowed roles are distinct. The caller supplies a fixed +bank of blank owned tapes; the adapter creates those distinct roles and rejects +borrowed-role aliasing. It does not claim initialization of arbitrary dirty +borrowed storage. Successful output and cleanup are proved; malformed-input +rejection has no blanket rollback guarantee. The per-word bit reversal from +#4192's big-endian representation is explicit in [PROOF.md](PROOF.md). + +The complete conservative instruction bound is +`10^6 W^2 (m+1) (N+1)^3 (h+1)^4`, including scalar/control operations, +full arena scans, both serializations and successful private cleanup. The full +arena, spool, selected ROM and complete layer output are retained in the storage +bound. This is not the old arena cell tariff and is not a comparison to E(p,ell). +A separate final erase scan disposes of both output roles after consumption. + +The actual key ABI interprets the same 32 flat cells as 2 rows of 16, whereas the +producer writes 4 rows of 8. The adapter identifies the same tape, without a +host-decoded table rewrite. Five key cases preserve borrowed descriptors, +opaque stream prefix and ROM, with exact returned keys, all three query epochs +and private cleanup corroborated by the retained independent instruction audit. + +## Reproduce + +``` +python3.12 -B scripts/research_package.py --package research/crt-encoded-benes-rom-producer +``` + +The verifier authenticates exact input bytes, checks the full generated output +against the canonical source, compares a frozen receipt, and rejects changed +neighbor routing, selected-row omission, output-disposal omission, malformed +headers/offsets and role aliasing. `--write-result` is the explicit authoring +mode; `--light` runs the bounded small cases without claiming the actual h3 +fixture. Normal/optimized/source-history/export evidence is in VALIDATION.md. + +## Open next questions + +1. Bind the encoded current-child CRT descriptor producer to this input ABI, + charging serialization and the actual requested row list. +2. Supply the variable-geometry key adapter and complete evaluator lifecycle + bill before any E(p,ell) or global ROM-reuse claim. +3. Execute a fixed binary encoding of the complete marker alphabet if a literal + binary transition-table certificate is required. + +TASK.json gives first steps and blockers. This package does not run the full +2,944-hole repair, five-layer caller, global CRT/native/precision/outer transfer, +Lean, Docker or the selected scientific cold suite. It supplies one local +producer and an actual fixed consumer calibration, not full multiplication. + +## Provenance and credit + +Scientific base 4c0a359d88f22f05189d51f48387750b801a45d4, priority 7. Canonical +[claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/4709#discussioncomment-19141162). +The final scout read 320 open PRs at 07:41:25UTC, 4168 Discussion records at 07:42:18UTC +and 6760 local notes with complete reported pagination/inventory; text overlap +is advisory. #5039's already completed thin-query task was excluded, as were +#5043's native fan rewrite and the fresh coded-p19/FOUR-base/compiler-width claims. +This does not repackage #5053's current-coordinate arithmetic. + +Credit ToikY/#4192 for the arena/DFS construction and original notice; +Cinna Davis/#4100 for the Beneš and CRT source; Hiroki KUMAZAKI, unpaidmoon, +Ryanson Jonathan, Jose Manuel, John-Michael Smith, Douglas Colkitt and retained +physical-repair lineage. JoyboyBrian, with substantial OpenAI Codex assistance. +Apache-2.0. Separate agent review is not independent human or proof-kernel +acceptance. Frozen predecessor and selected-frontier files are unchanged. diff --git a/research/crt-encoded-benes-rom-producer/RESULT.json b/research/crt-encoded-benes-rom-producer/RESULT.json new file mode 100644 index 0000000000..21c1b85db2 --- /dev/null +++ b/research/crt-encoded-benes-rom-producer/RESULT.json @@ -0,0 +1,219 @@ +{ + "status": "PASS_CRT_ENCODED_BENES_ROM_PRODUCER", + "scope": "Uniform valid typed descriptor producer plus fixed actual key calibration; no full evaluator tariff or all-size supplier admission", + "program_instructions": 10648, + "code_sha256": "d4af5350854a87b67484840800b94e1e53cff82c78ec0f2a91753fed9ea70af7", + "program_sha256": "4aabd24ff17c5161b16d4c518defe07b36c89c71ed683a5b5691dc61a2fc4bc0", + "source_hashes": { + "research/crt-uniform-rom-query/machine.py": "46ee6a635251e498ee9a5d4aff8c0e2a7f1ef2ff951e5b6a2a8953316e9cd02d", + "research/crt-uniform-rom-query/PROOF.md": "736be5e1af590f2195e8b56b958258f0babe5cd6d2cf6f4f5023410112f4d870", + "research/crt-paid-key-service/service.py": "ff06c6305c9f650a694e5c42baa4c7d841decf844a4f44f6776acc10a8400083", + "research/crt-paid-key-service/verify.py": "fb02e2792cb07c52367c0a8c7087d54958bdf55214e51bc02f4e68dbf95547b1", + "research/crt-paid-key-service/PROOF.md": "1a4ac02653eb6c1b20807033a910f27bf9484cc972bf2629941f589275a87325", + "research/crt-dense-guard-scan/machine.py": "1cb27312932914eb631078bd56e85feb1dc6c4191e9d1962b2cc3a7e1cfb8df7", + "research/crt-mask-repair-bridge/key_subroutine.py": "ffdbb610be71ae20bf974946dac66b6c1b4d43739cbc3b1eb81cbbeab8784b44", + "research/unconditional-batched-crt/check_batched_crt.py": "681e2e3d71fa74c8b9b326f3860104fd9d89590a222e26ae6ee718d1fd40ff2e", + "research/unconditional-batched-crt/NOTICE.md": "924109837e71c52392191710d49c9deb42780878d1094f0b01e8690dbe799461", + "research/crt-encoded-benes-rom-producer/vendor/pr4192-verify.py": "e8ff7800ffa267d2825009656b78ab1613544b55301982744ec0d99f38800913", + "research/crt-encoded-benes-rom-producer/vendor/pr4192-PROOF.md": "c3eb4e14dc5ee0102cbf77c4a0e61db9989c2b8a0eaf7f0659a6e39373197474", + "research/crt-encoded-benes-rom-producer/vendor/pr4192-NOTICE.md": "b886589be7c8b87bcf12b14ce4db6827299b7cec93836ed22cff81aed37623dc" + }, + "cases": [ + { + "h": 1, + "W": 4, + "modulus": 2, + "offsets": [ + 0, + 1 + ], + "selected_layer": 0, + "instructions": 92369, + "layers_sha256": "40a769b8f91b4c81e3463de23d9901a3e5b1c195a52f1e4e329642dd13a8741a", + "rom": "0011", + "instruction_bound": 20736000000, + "represented_cells": 515, + "storage_bound": 862, + "disposal_instructions": 104 + }, + { + "h": 2, + "W": 16, + "modulus": 3, + "offsets": [ + 0, + 1 + ], + "selected_layer": 1, + "instructions": 13784532, + "layers_sha256": "62362c34a43df3d140219671bbe152b32d476a0f04d3901b66507033ba0bccbd", + "rom": "00000101", + "instruction_bound": 7776000000000, + "represented_cells": 4469, + "storage_bound": 5496, + "disposal_instructions": 338 + }, + { + "h": 1, + "W": 4, + "modulus": 1, + "offsets": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "selected_layer": 0, + "instructions": 726491, + "layers_sha256": "9627d016ae34dcbd690eda869a60292fac4ad879f3e45e3fc168501d4be7ad98", + "rom": "0000000000000000000000000000000000", + "instruction_bound": 124416000000, + "represented_cells": 680, + "storage_bound": 1027, + "disposal_instructions": 644 + }, + { + "h": 3, + "W": 20, + "modulus": 5, + "offsets": [ + 0, + 2, + 4, + 0 + ], + "selected_layer": 2, + "instructions": 459156907, + "layers_sha256": "3fc72814b9bbb80be9952f390f539016123ac97c23c2c3e243bda1d73262a2f2", + "rom": "00000000001000101000100000000000", + "instruction_bound": 373248000000000, + "represented_cells": 16685, + "storage_bound": 17944, + "key_consumer": [ + { + "address": 0, + "key": "000000000000", + "oracle_epochs": [ + [ + 0, + 0 + ], + [ + 0, + 0 + ], + [ + 0, + 0 + ] + ], + "instructions": 41539 + }, + { + "address": 10, + "key": "000000001010", + "oracle_epochs": [ + [ + 10, + 1 + ], + [ + 14, + 1 + ], + [ + 14, + 1 + ] + ], + "instructions": 44208 + }, + { + "address": 17, + "key": "000000010001", + "oracle_epochs": [ + [ + 17, + 0 + ], + [ + 17, + 0 + ], + [ + 17, + 0 + ] + ], + "instructions": 41657 + }, + { + "address": 1699, + "key": "011010100011", + "oracle_epochs": [ + [ + 163, + 0 + ], + [ + 167, + 0 + ], + [ + 163, + 0 + ] + ], + "instructions": 43548 + }, + { + "address": 4095, + "key": "111111011111", + "oracle_epochs": [ + [ + 255, + 0 + ], + [ + 251, + 0 + ], + [ + 223, + 0 + ] + ], + "instructions": 44928 + } + ], + "disposal_instructions": 1796 + } + ], + "controls": [ + "h_nonbit", + "offset_origin", + "modulus_zero", + "modulus_above_N", + "offset_outside_modulus", + "selector_outside_layers", + "empty_offsets", + "truncated_offset", + "borrowed_role_alias", + "wrong_neighbor", + "missing_output_disposal", + "wrong_selected_row" + ] +} diff --git a/research/crt-encoded-benes-rom-producer/SOURCES.json b/research/crt-encoded-benes-rom-producer/SOURCES.json new file mode 100644 index 0000000000..ea930342bb --- /dev/null +++ b/research/crt-encoded-benes-rom-producer/SOURCES.json @@ -0,0 +1,96 @@ +{ + "schema_version": 1, + "base_commit": "4c0a359d88f22f05189d51f48387750b801a45d4", + "files": [ + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "research/crt-uniform-rom-query/machine.py", + "usage": "input", + "git_blob": "88292ce98d31d540c7dba6960bfe4c19f06a8077", + "sha256": "46ee6a635251e498ee9a5d4aff8c0e2a7f1ef2ff951e5b6a2a8953316e9cd02d" + }, + { + "path": "research/crt-uniform-rom-query/PROOF.md", + "usage": "input", + "git_blob": "63b0551a7715b9b67f2b13510183254401eb082f", + "sha256": "736be5e1af590f2195e8b56b958258f0babe5cd6d2cf6f4f5023410112f4d870" + }, + { + "path": "research/crt-paid-key-service/service.py", + "usage": "input", + "git_blob": "726d9523ab7dd4a16697f9201b0224f2da1f2517", + "sha256": "ff06c6305c9f650a694e5c42baa4c7d841decf844a4f44f6776acc10a8400083" + }, + { + "path": "research/crt-paid-key-service/verify.py", + "usage": "input", + "git_blob": "9cd6b46a1ae52223ffe8de73c8e223e74f11ba4a", + "sha256": "fb02e2792cb07c52367c0a8c7087d54958bdf55214e51bc02f4e68dbf95547b1" + }, + { + "path": "research/crt-paid-key-service/PROOF.md", + "usage": "input", + "git_blob": "a0b84e8d3bd80d760a1be9e801fc57939b6f24e9", + "sha256": "1a4ac02653eb6c1b20807033a910f27bf9484cc972bf2629941f589275a87325" + }, + { + "path": "research/crt-dense-guard-scan/machine.py", + "usage": "input", + "git_blob": "ce763898bd7b4401bbab818c640a0593b65c9a82", + "sha256": "1cb27312932914eb631078bd56e85feb1dc6c4191e9d1962b2cc3a7e1cfb8df7" + }, + { + "path": "research/crt-mask-repair-bridge/key_subroutine.py", + "usage": "input", + "git_blob": "5771ae55626dbc2a32a95d8c098bdd03d820833c", + "sha256": "ffdbb610be71ae20bf974946dac66b6c1b4d43739cbc3b1eb81cbbeab8784b44" + }, + { + "path": "research/unconditional-batched-crt/check_batched_crt.py", + "usage": "input", + "git_blob": "1cf78abccd5e06beecc3ed21ba55f7c03b65fdbc", + "sha256": "681e2e3d71fa74c8b9b326f3860104fd9d89590a222e26ae6ee718d1fd40ff2e" + }, + { + "path": "research/unconditional-batched-crt/NOTICE.md", + "usage": "input", + "git_blob": "886a8fdee275f01b459cbd68ae2815dc9269502f", + "sha256": "924109837e71c52392191710d49c9deb42780878d1094f0b01e8690dbe799461" + }, + { + "path": "research/crt-encoded-benes-rom-producer/vendor/pr4192-verify.py", + "usage": "input", + "pin": "head:8d778d29b9e1cf3344d21122817f0f37580a419b:research/crt-encoded-benes-rom-producer/vendor/pr4192-verify.py", + "origin_pin": "head:519d811cc48693ad9969d6d7994bef3940167005:research/crt-benes-scan/verify.py", + "git_blob": "e79a9ce3f38f78031310acd9e384fd4010ce8ca8", + "sha256": "e8ff7800ffa267d2825009656b78ab1613544b55301982744ec0d99f38800913" + }, + { + "path": "research/crt-encoded-benes-rom-producer/vendor/pr4192-PROOF.md", + "usage": "input", + "pin": "head:8d778d29b9e1cf3344d21122817f0f37580a419b:research/crt-encoded-benes-rom-producer/vendor/pr4192-PROOF.md", + "origin_pin": "head:519d811cc48693ad9969d6d7994bef3940167005:research/crt-benes-scan/PROOF.md", + "git_blob": "af1ea10b9d2b117d150ec7bddfb81e681172cdb4", + "sha256": "c3eb4e14dc5ee0102cbf77c4a0e61db9989c2b8a0eaf7f0659a6e39373197474" + }, + { + "path": "research/crt-encoded-benes-rom-producer/vendor/pr4192-NOTICE.md", + "usage": "input", + "pin": "head:8d778d29b9e1cf3344d21122817f0f37580a419b:research/crt-encoded-benes-rom-producer/vendor/pr4192-NOTICE.md", + "origin_pin": "head:519d811cc48693ad9969d6d7994bef3940167005:research/crt-benes-scan/NOTICE.md", + "git_blob": "6ca47019de7e58edf93c4278a6a8251625d37477", + "sha256": "b886589be7c8b87bcf12b14ce4db6827299b7cec93836ed22cff81aed37623dc" + } + ] +} diff --git a/research/crt-encoded-benes-rom-producer/TASK.json b/research/crt-encoded-benes-rom-producer/TASK.json new file mode 100644 index 0000000000..4e5e731276 --- /dev/null +++ b/research/crt-encoded-benes-rom-producer/TASK.json @@ -0,0 +1,87 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "4c0a359d88f22f05189d51f48387750b801a45d4", + "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": "Literal finite-control lowering of the retained Bene\u0161 arena schedule from encoded rotation descriptors, owned layer/ROM output, and direct actual fixed key consumption.", + "scope_change_reason": "Public handoff #4795/#5015 requests the missing source ROM producer; #4192 already supplied its mathematical arena schedule and cost proof, not executed scalar/header control.", + "bottleneck_link": "Closes one actual supplied-ROM assumption without treating descriptor preparation or full evaluator costs as zero.", + "budget_minutes": 60, + "stop_rule": "Stop at this complete local producer and actual fixed key join; no full CRT repair or selected supplier replay.", + "outcome": "completed", + "evidence": "PROOF.md; verify.py; RESULT.json; normal/optimized registered replay and source/export checks recorded in VALIDATION.md.", + "author": "JoyboyBrian", + "ai_assistance": "Substantial OpenAI Codex assistance; separate agent code/proof review, not human or proof-kernel acceptance.", + "open_questions": [ + { + "question": "Connect encoded current-child CRT descriptor production to this rotation-list ABI.", + "why_it_matters": "The producer consumes encoded modulus/offset descriptors; their CRT preparation is not free.", + "first_step": "Pin one #5053 right-node offset output and charge serialization into the W-bit offset records before any ROM reuse.", + "blocked_by": "Variable source descriptor traversal and layout contracts are not integrated here." + }, + { + "question": "Supply a variable-geometry key adapter and a complete evaluator lifecycle bill.", + "why_it_matters": "Only the real fixed #4795 port is joined; the local instruction bound does not establish E(p,ell).", + "first_step": "Write one parameterized current-state query header adapter with the full generated layer ownership and disposal schedule.", + "blocked_by": "Raw macro, repair/scanner Boolean control and full caller reuse remain separate." + }, + { + "question": "Lower the complete producer symbol alphabet to an actual binary machine.", + "why_it_matters": "Literal bit payload and finite-symbol control are executed; marker encoding overhead is not a binary transition-table certificate.", + "first_step": "Apply a source-bound fixed symbol encoding to the unchanged producer and preserve every branch/head invariant.", + "blocked_by": "Not needed for the scoped finite-alphabet construction; no such execution claimed." + } + ], + "coordination": "https://github.com/CrocSwap/integer-mult-bounds/discussions/4709#discussioncomment-19141162" +} diff --git a/research/crt-encoded-benes-rom-producer/VALIDATION.md b/research/crt-encoded-benes-rom-producer/VALIDATION.md new file mode 100644 index 0000000000..2596c04a12 --- /dev/null +++ b/research/crt-encoded-benes-rom-producer/VALIDATION.md @@ -0,0 +1,11 @@ +# Validation and scope + +Python 3.12.2 on macOS; no dependencies, Lean, Docker or selected-result replay. + +* Full normal `python3.12 -B research/crt-encoded-benes-rom-producer/verify.py --write-result` passed all four producer fixtures and twelve controls. Authoring mode executes the same checks as registered verification; only its final receipt write replaces receipt equality. +* The actual h3, W20, modulus5, offsets[0,2,4,0] producer executed459,156,907 primitive instructions, used16,685 represented cells, and emitted all five canonical layers. It directly joined the same selected ROM list to the unchanged key service. Final disposal took1,796 instructions. +* After that run, the verifier's receipt epochs were normalized from tuples to JSON lists, and address10 was added to the four original consumer cases. A consumer-only calibration passed its positive epochs (10,1),(14,1),(14,1). The final exported optimized replay below executes all five cases on the newly generated actual list; no normal producer rerun is implied. +* Independent agent review checked the literal control, word representation transport, marker-driven unbounded finite list traversal, ownership/rejection boundaries, source recurrence, consumer identity and independent epoch audit. The small W4,17-offset case was independently replayed. This is agent review, not human or proof-kernel acceptance. +* Metadata and exact source pins passed. Vendored PR4192 bytes were compared with original commit519d811cc48693ad9969d6d7994bef3940167005. The manifest records that original pin separately; its transport pin identifies the identical vendored path in this branch's first implementation commit. + +Final committed source-history check passed at ae564e3c13bde53f292a608a38793aa7710ded84 (21 files; both source commits in ancestry). The official export/check passed. In an extracted tree with no .git metadata, `/opt/local/bin/python3.12 -O -B research/crt-encoded-benes-rom-producer/verify.py` passed all four complete producer fixtures, all five direct consumer cases and twelve controls, including frozen exact receipt equality. Export SHA256: ed2e8b2601df11e825fa281423e57d7d3bbfd4bf42a5f16989986f69c5b8ee00. A separately corrupted retained machine source was rejected by source authentication before producer execution. Subsequent edits record this validation and clarify that the service target is bit position 2, not Boolean value 2; every executable/input-source/receipt hash remains unchanged. Frozen receipt comparisons authenticate source content and exact primitive counts; these finite replays calibrate the separately stated scoped proof. No complete CRT evaluator or selected frontier change is claimed. diff --git a/research/crt-encoded-benes-rom-producer/VERIFY.json b/research/crt-encoded-benes-rom-producer/VERIFY.json new file mode 100644 index 0000000000..bd018024b8 --- /dev/null +++ b/research/crt-encoded-benes-rom-producer/VERIFY.json @@ -0,0 +1,41 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/crt-uniform-rom-query/machine.py", + "research/crt-uniform-rom-query/PROOF.md", + "research/crt-paid-key-service/service.py", + "research/crt-paid-key-service/verify.py", + "research/crt-paid-key-service/PROOF.md", + "research/crt-dense-guard-scan/machine.py", + "research/crt-mask-repair-bridge/key_subroutine.py", + "research/unconditional-batched-crt/check_batched_crt.py", + "research/unconditional-batched-crt/NOTICE.md", + "research/crt-encoded-benes-rom-producer/vendor/pr4192-verify.py", + "research/crt-encoded-benes-rom-producer/vendor/pr4192-PROOF.md", + "research/crt-encoded-benes-rom-producer/vendor/pr4192-NOTICE.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Source hashes, static finite-control instruction audit, actual complete five-layer rotation ROM producer and direct three-epoch key join, complete small fixtures including17 offsets with W4, ownership/disposal and semantic mutations." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Same full source-bound receipt and semantic controls with assertions disabled." + } + ] +} diff --git a/research/crt-encoded-benes-rom-producer/verify.py b/research/crt-encoded-benes-rom-producer/verify.py new file mode 100644 index 0000000000..78c5e8103b --- /dev/null +++ b/research/crt-encoded-benes-rom-producer/verify.py @@ -0,0 +1,146 @@ +"""Source-bound endpoint, caller and semantic controls; no hidden producer oracle.""" +import argparse +import hashlib +import json +from pathlib import Path +import sys +import types + +P=Path(__file__).resolve().parent +ROOT=P.parents[1] + +def need(ok,label): + if not ok:raise ValueError(label) + +def load(name,path,source=None): + mod=types.ModuleType(name);mod.__file__=str(path) + exec(compile(path.read_bytes() if source is None else source,str(path),'exec'),mod.__dict__) + return mod + +def authenticate(): + hashes={} + for row in json.loads((P/'SOURCES.json').read_text())['files']: + if row['usage']!='input':continue + raw=(ROOT/row['path']).read_bytes();digest=hashlib.sha256(raw).hexdigest() + need(digest==row['sha256'],'source SHA256 '+row['path']) + need(hashlib.sha1(b'blob '+str(len(raw)).encode()+b'\0'+raw).hexdigest()==row['git_blob'],'source Git blob') + hashes[row['path']]=digest + return hashes + +def headers(h,s,offsets,selected,w=None): + w=w or 4*h+8 + def word(x):return ['L',*f'{x:0{w}b}'[::-1],'R'] + return dict(h=word(h),modulus=word(s),selected_layer=word(selected), + offsets=['L',*[b for v in offsets for b in list(f'{v:0{w}b}'[::-1])+['|']],'R']) + +def check_static(code): + allowed={'read','write','write_reg','move','set','not','copybit','eq','branch','jump','halt'} + for op,*a in code: + need(op in allowed,'literal finite-symbol opcode') + if op=='move':need(type(a[1]) is int and a[1] in (-1,1),'unit move') + if op in ('set','write'):need(a[1] in ('0','1','L','R','|','_'),'fixed symbol') + if op=='branch':need(all(type(x)is int and 0<=x']);stream=native.Tape(['<',('R',819),('R',17),'_']);stream.head=3 + engine=service.Service(query,target,rom) + roles=dict(engine.private,counter=counter,stream=stream,rom=rom) + initial={r:audit.snapshot(t) for r,t in roles.items()};heads={r:t.head for r,t in roles.items()} + engine.evaluate_key(counter,stream,trace=True) + reference=oracle.ReverseWordKey(target,tuple(map(int,oracle_bits)));epochs=[];original=reference.source + def observed(y): + bit=original(y);epochs.append((y,bit));return bit + reference.source=observed;want=reference.key_of(raw) + need(''.join(stream.cells[3:15])==want,'actual key equals independent reverse word') + need(rom.cells is cells and cells==saved and rom.head==0,'same generated ROM preserved') + need(counter.cells==['<',*raw,'>'] and counter.head==0,'borrowed counter preserved') + need(stream.cells[:3]==['<',('R',819),('R',17)] and stream.head==15,'opaque prefix and append') + need(all(t.head==0 and all(v=='_' for v in t.cells.values()) for t in engine.private.values()),'consumer private cleanup') + actual_epochs,_=audit.audit(engine,initial,heads) + need(actual_epochs==[dict(y=y,bit=bit) for y,bit in epochs],'three actual current-state epochs') + result.append(dict(address=address,key=want,oracle_epochs=[list(e) for e in epochs],instructions=sum(engine.last['census'].values()))) + return result + +def controls(m,crt): + rejected=[] + for name,mutate in [ + ('h_nonbit',lambda d:d['h'].__setitem__(1,'x')), + ('offset_origin',lambda d:d['offsets'].__setitem__(0,'_')), + ('modulus_zero',lambda d:d.update(modulus=headers(1,0,[0],0)['modulus'])), + ('modulus_above_N',lambda d:d.update(modulus=headers(1,3,[0],0)['modulus'])), + ('offset_outside_modulus',lambda d:d.update(offsets=headers(1,2,[2],0)['offsets'])), + ('selector_outside_layers',lambda d:d.update(selected_layer=headers(1,2,[0],1)['selected_layer'])), + ('empty_offsets',lambda d:d.update(offsets=['L','R'])), + ('truncated_offset',lambda d:d['offsets'].pop(1)), + ]: + d=headers(1,2,[0],0);mutate(d);out,_=m.run_producer(d,max_steps=200000) + need(out['status']!='accept','reject '+name);rejected.append(name) + d=headers(1,2,[0],0);d['modulus']=d['h'] + try:m.run_producer(d) + except ValueError:rejected.append('borrowed_role_alias') + else:raise ValueError('aliased role admitted') + # Changed source program, not a changed expected digest: semantic controls. + source=(P/'microcode.py').read_text() + mutants=[('wrong_neighbor',"b.xor1('other');b.get(1,'other','other')","b.get(1,'other','other')"), + ('missing_output_disposal',"for role in ('layers','rom'):b.erase(role)","for role in ('layers',):b.erase(role)"), + ('wrong_selected_row',"b.equal('outlayer','selected_layer','selected_bit')","b.e('set','selected_bit','0')")] + for name,old,new in mutants: + need(old in source,'mutation applied '+name);bad=load('mutant',P/'microcode.py',source.replace(old,new).encode()) + try:fixture(bad,crt,2,3,[0,1],1) + except ValueError:rejected.append(name) + else:raise ValueError('semantic mutant accepted '+name) + return rejected + +def main(): + parser=argparse.ArgumentParser();parser.add_argument('--write-result',action='store_true');parser.add_argument('--light',action='store_true');args=parser.parse_args() + hashes=authenticate();m=load('micro',P/'microcode.py');crt=load('crt',ROOT/'research/unconditional-batched-crt/check_batched_crt.py') + code=m.producer_program();check_static(code) + cases=[fixture(m,crt,1,2,[0,1],0,w=4),fixture(m,crt,2,3,[0,1],1),fixture(m,crt,1,1,[0]*17,0,w=4)] + faults=controls(m,crt) + if args.light:print('PASS_CRT_ROM_LIGHT',json.dumps({'cases':cases,'controls':faults}));return + cases.append(fixture(m,crt,3,5,[0,2,4,0],2,consume=True)) + result={'status':'PASS_CRT_ENCODED_BENES_ROM_PRODUCER','scope':'Uniform valid typed descriptor producer plus fixed actual key calibration; no full evaluator tariff or all-size supplier admission', + 'program_instructions':len(code),'code_sha256':hashlib.sha256((P/'microcode.py').read_bytes()).hexdigest(), + 'program_sha256':hashlib.sha256(json.dumps(code,separators=(',',':')).encode()).hexdigest(),'source_hashes':hashes,'cases':cases,'controls':faults} + path=P/'RESULT.json' + if args.write_result:path.write_text(json.dumps(result,indent=2)+'\n') + else:need(json.loads(path.read_text())==result,'frozen exact receipt') + print(result['status'],f"cases={len(cases)} controls={len(faults)} instructions={cases[-1]['instructions']}") + +if __name__=='__main__':main() From af3030a82d22cb1d897d891eb872e927dc322db3 Mon Sep 17 00:00:00 2001 From: JoyboyBrian <122925040+JoyboyBrian@users.noreply.github.com> Date: Fri, 23 Oct 2026 02:23:23 -0700 Subject: [PATCH 3/3] Allow bounded Linux runtime for complete ROM producer replay --- .../crt-encoded-benes-rom-producer/VALIDATION.md | 13 +++++++++++++ research/crt-encoded-benes-rom-producer/VERIFY.json | 4 ++-- 2 files changed, 15 insertions(+), 2 deletions(-) diff --git a/research/crt-encoded-benes-rom-producer/VALIDATION.md b/research/crt-encoded-benes-rom-producer/VALIDATION.md index 2596c04a12..fb995fcd01 100644 --- a/research/crt-encoded-benes-rom-producer/VALIDATION.md +++ b/research/crt-encoded-benes-rom-producer/VALIDATION.md @@ -9,3 +9,16 @@ Python 3.12.2 on macOS; no dependencies, Lean, Docker or selected-result replay. * Metadata and exact source pins passed. Vendored PR4192 bytes were compared with original commit519d811cc48693ad9969d6d7994bef3940167005. The manifest records that original pin separately; its transport pin identifies the identical vendored path in this branch's first implementation commit. Final committed source-history check passed at ae564e3c13bde53f292a608a38793aa7710ded84 (21 files; both source commits in ancestry). The official export/check passed. In an extracted tree with no .git metadata, `/opt/local/bin/python3.12 -O -B research/crt-encoded-benes-rom-producer/verify.py` passed all four complete producer fixtures, all five direct consumer cases and twelve controls, including frozen exact receipt equality. Export SHA256: ed2e8b2601df11e825fa281423e57d7d3bbfd4bf42a5f16989986f69c5b8ee00. A separately corrupted retained machine source was rejected by source authentication before producer execution. Subsequent edits record this validation and clarify that the service target is bit position 2, not Boolean value 2; every executable/input-source/receipt hash remains unchanged. Frozen receipt comparisons authenticate source content and exact primitive counts; these finite replays calibrate the separately stated scoped proof. No complete CRT evaluator or selected frontier change is claimed. + +## Hosted replay budget correction + +GitHub Actions on Linux with CPython 3.12.15 reached the original 180-second +per-command limit on the complete normal producer replay (run 39927492849, +job 120328791828, 2026-10-23 08:55:01–08:58:01 UTC). The reported failure was +`verification timed out`; it did not report a mathematical or receipt mismatch. +Both registered commands now have a bounded 600-second budget to accommodate +that platform. This change preserves every executable, retained input, source +pin and frozen receipt byte. The existing complete local normal and exported +optimized evidence above is reused; no additional scientific replay is implied. +Metadata/source-history and committed export checks were repeated for the budget +change. Hosted completion must be reported separately from the local evidence. diff --git a/research/crt-encoded-benes-rom-producer/VERIFY.json b/research/crt-encoded-benes-rom-producer/VERIFY.json index bd018024b8..e410f470d2 100644 --- a/research/crt-encoded-benes-rom-producer/VERIFY.json +++ b/research/crt-encoded-benes-rom-producer/VERIFY.json @@ -24,7 +24,7 @@ "-B", "{package}/verify.py" ], - "timeout_seconds": 180, + "timeout_seconds": 600, "checks": "Source hashes, static finite-control instruction audit, actual complete five-layer rotation ROM producer and direct three-epoch key join, complete small fixtures including17 offsets with W4, ownership/disposal and semantic mutations." }, { @@ -34,7 +34,7 @@ "-B", "{package}/verify.py" ], - "timeout_seconds": 180, + "timeout_seconds": 600, "checks": "Same full source-bound receipt and semantic controls with assertions disabled." } ]