From d720645e80cce85975f549deb3aa0937c3201e55 Mon Sep 17 00:00:00 2001 From: JoyboyBrian <122925040+JoyboyBrian@users.noreply.github.com> Date: Thu, 22 Oct 2026 23:16:01 -0700 Subject: [PATCH 1/3] Implement literal runtime-coefficient affine shear and independent replay --- research/fixed-tape-affine-shear/RESULT.json | 44 ++++ research/fixed-tape-affine-shear/SOURCES.json | 68 +++++++ .../fixed-tape-affine-shear/TABLE.json.gz | Bin 0 -> 3078 bytes .../fixed-tape-affine-shear/independent.py | 155 +++++++++++++++ research/fixed-tape-affine-shear/kernel.py | 143 +++++++++++++ research/fixed-tape-affine-shear/loader.py | 48 +++++ research/fixed-tape-affine-shear/verify.py | 188 ++++++++++++++++++ 7 files changed, 646 insertions(+) create mode 100644 research/fixed-tape-affine-shear/RESULT.json create mode 100644 research/fixed-tape-affine-shear/SOURCES.json create mode 100644 research/fixed-tape-affine-shear/TABLE.json.gz create mode 100644 research/fixed-tape-affine-shear/independent.py create mode 100644 research/fixed-tape-affine-shear/kernel.py create mode 100644 research/fixed-tape-affine-shear/loader.py create mode 100644 research/fixed-tape-affine-shear/verify.py diff --git a/research/fixed-tape-affine-shear/RESULT.json b/research/fixed-tape-affine-shear/RESULT.json new file mode 100644 index 0000000000..36ebcd4673 --- /dev/null +++ b/research/fixed-tape-affine-shear/RESULT.json @@ -0,0 +1,44 @@ +{ + "binding": { + "actual_half_0_to_3": 1, + "descriptor_preparation": "charged separate binary half/increment scan", + "serialized_half_leaves": 96, + "serialized_later_target_leaves": 160, + "source_f": 1, + "source_q": 5, + "source_w": 4, + "whole_route_admitted": false + }, + "controls": [ + "input_4", + "input_5", + "input_6", + "input_7", + "input_14", + "input_16", + "noncanonical", + "occupied_scratch", + "nonlocal_move", + "wrong_orientation", + "retained_scratch_2", + "retained_scratch_17", + "source_hash", + "unbilled_extra_steps" + ], + "physical": { + "alphabet_symbols": 7, + "cases": 610, + "instructions": { + "False": 877, + "True": 877 + }, + "maximum_fixture_span": 3028, + "maximum_fixture_steps": 52940, + "payload_bits": 38850, + "tapes": 19, + "transcript_sha256": "163d6510128fe6cd585011b5a5062b5b750d1115625a902b0fbe036f1e363f74", + "transitions_bound_per_bit": 1024, + "visited_cells_bound_per_bit": 64 + }, + "schema_version": 1 +} diff --git a/research/fixed-tape-affine-shear/SOURCES.json b/research/fixed-tape-affine-shear/SOURCES.json new file mode 100644 index 0000000000..2064c10cd0 --- /dev/null +++ b/research/fixed-tape-affine-shear/SOURCES.json @@ -0,0 +1,68 @@ +{ + "schema_version": 1, + "files": [ + { + "path": "research/fixed-tape-ordered-shear/machine.py", + "usage": "input", + "commit": "bee95ce88f9f19802f0613f92838895cd0e14a1f", + "sha256": "04b7b76b9f06653d94d2158196cdd1bed7883dd1f59fcbc81a486e3ffb248681", + "git_blob": "6ed03865cdb646d40573c132f841afbe335daba0" + }, + { + "path": "research/fixed-tape-ordered-shear/counters.py", + "usage": "input", + "commit": "bee95ce88f9f19802f0613f92838895cd0e14a1f", + "sha256": "2b51181a3efd403be14111ed2d556ba10e63a8939756e69d488d12344d5a7ad1", + "git_blob": "c4878a7a7e3f390d193df496a579e4a788f25e32" + }, + { + "path": "research/fixed-tape-ordered-shear/shear.py", + "usage": "input", + "commit": "bee95ce88f9f19802f0613f92838895cd0e14a1f", + "sha256": "84d60e552bb35657b3c5e63b4ab21846a90d71dfd22c8a46cd01acba76475818", + "git_blob": "b814b6f77b03f12577464df91be6c4f103d1722c" + }, + { + "path": "research/fixed-tape-ordered-shear/PROOF.md", + "usage": "input", + "commit": "bee95ce88f9f19802f0613f92838895cd0e14a1f", + "sha256": "2b5df8f57a9d36a8281e8267f1a9fefbccb4c5e5e044bdd73e911aa55acbfe24", + "git_blob": "967eaeb4a17263194a6932b409a2637e133ad238" + }, + { + "path": "research/fixed-tape-unit-carry/carry.py", + "usage": "input", + "commit": "bee95ce88f9f19802f0613f92838895cd0e14a1f", + "sha256": "553b16d27f5126d2fc734b42c4bce0e80f5e0622fb6650756c3cdd16ca34b01f", + "git_blob": "f5cea000160309e0a529b8eaae8eac7e18d45e1d" + }, + { + "path": "research/fixed-tape-unit-carry/README.md", + "usage": "input", + "commit": "bee95ce88f9f19802f0613f92838895cd0e14a1f", + "sha256": "9e0e4e80763785191a5a8077e2c9ee37590084e2dd57b08f2000cd6aece6500c", + "git_blob": "fb5454aff35c6ffa0bdb1cdb7537bd45cd2038a8" + }, + { + "path": "research/bit-row-route-generator/generator.py", + "usage": "input", + "commit": "bee95ce88f9f19802f0613f92838895cd0e14a1f", + "sha256": "c3721d4f52bf431b2f1d4464e08088fcf2b453215308dd4a8bef221e61122885", + "git_blob": "30015c270b483fae9889246aa7a66768012bbed7" + }, + { + "path": "research/bit-row-route-generator/PROGRAM.json.gz", + "usage": "input", + "commit": "bee95ce88f9f19802f0613f92838895cd0e14a1f", + "sha256": "83448ca22ef773847b748d62f19ea80b2a51c53913ce22624003b6170be7044c", + "git_blob": "2df37028f46614301118980ad14d2b3f80e43c31" + }, + { + "path": "research/bit-row-route-generator/PROOF.md", + "usage": "input", + "commit": "bee95ce88f9f19802f0613f92838895cd0e14a1f", + "sha256": "b620b2fbca0261972f96585f5adfd170fc0aa9591a9952d8cc6d7aac327737c3", + "git_blob": "358ba70e944e8bbef3504da5d59089255b4ded9f" + } + ] +} diff --git a/research/fixed-tape-affine-shear/TABLE.json.gz b/research/fixed-tape-affine-shear/TABLE.json.gz new file mode 100644 index 0000000000000000000000000000000000000000..2299b468a71c2065c3d72f5e657e28fc591a4498 GIT binary patch literal 3078 zcmchX`8yPh7RSAn5E-cq*&5kigR;yJV+yGl`b^j4jWtSCg69})ey3K9 z8hdv0><(~w!dVEW??k5*s#Rt=7D%21m%hXTnN0^$B!E#8J+jj_%9;E@$HBW5jW_!u zX^~UDk@TJ+R3iY{8mJ6!g&hT*Y^?bOeGlH-L+|b{uKJy{djbyPg(*Vt;Bi%Q&W^Be zD_pHfKtCjM2z5v8*lV8wV`&$VotqBgob#6K9dO{J%p1Zxw7%=gbx|bhgA(KM@6%@I z@j-Al-OOhQwKUyJNV%KDzSK=GW?4m6Biw67lWx?9evx~S{G?5Jtu_t(b#yj(UK?t_ zv#Hoy5FP9cH2`kTj2gMzc)LQ|uRVda!1O07HX(jiVLP*g*7a-yu>a!$=KZfXfo6up z=so_vMY-meLI|AD?!YD@pbn^TRQ{^$E>4=tMr-r(8SClF#q~T%0Of@ZS%5qd?XQ~E z(4ZFiTQUpdP+q;ZL1WI^)VU{|jxH#V{ReDaIB8tnhiOIuRJD}gS8BF z%sr*Fh+QIc(&^pTMrfWNXY}l8MqL3Ns}0ja?j~FkKf`7p^EfoGLaDw7HMbJ9Uz;SY z8FR)|!+>+#cS701vpG-HCR>+x8Y|-a05<`x0-meC;^I3Z4;pVOl^ne$MB_1p#oZmQ7j_~Xl1c2m^z#XNqAR%Bh(zUuEE{X> zLJ#v5)y7+_KU@<-$s+1~gq|++tF#)}veNA0y5kVxDe_Eh(Yo$r_**v1-tf!}X=jZu zu?!SrzySkOa4TpgD6@mMK&~qo>*k=JYtB&ogCDV`$*!jL_!3#7K8rZ>0eq?DzTo_p zCwmtm3sa2Yw0UMf)0+%K@z%1FXf6|VSssBgrUL$wv+Ld=b3a#mi}8zOZw2lL*(4t) zXZJBd#erAZFIp09zH+7G2M6p;G@WxPCH_vn5nKv^=iWbLQe)4A-PTZTy_b8@KVb4* z4uTGB+UwL|Emj5;!{^U^yp_KR+>M3tIhf13+%nTm0BZ8ydn}W$X_nFA<0ns<1^I)` z%8eNC5)MSkkfnBBYmACXtO|9J#-m8cnm1{QbniK}xNzFPoh0@_q`$^Z4jk83sQ)_Y z%sXi%1v96JL~0R^dZesSWTC1M3xQkdi|%W9X=+0kXfX~zXRT46%| zHf!{8D#XY~Gn+Ko>o}7prX-HOJQKj9t4Gy4O>do5sc>xl6nAHak7k*g9-@h{PSGa5f2AIgNlb`GBYT*=4S$gB(JuRqq z4Xt|;6{HoGtp|{?p20R~bMS9q{Hx2*=Xu~M z$m1rg1TFwy2`zX%6(uNpu`)tc=9;NRKiRmTrx_Eh?yCa%8?caHVOS8)_Zi3bDdi3h ztN83_q3NfArDj9vF9X>JYHUC_~=1e z$u1-0kA)^u!}VY%0;%POJwHFQG&G_5kH?kjn}ei@N7a<2z^O|gzO;pwn~N@d+v;C= z=HZm*e)J!?3g{Hd)z`GEoCC>K3+c5M$}uEMgV(f!sY{L|U-?W!P|ue4&T8QjQgHqS z&3%8{#R%mZZyX?^A?bTNh8XjD8cp};5w&?AXb|KKvLQLQ`kgq`V6i$L9HVwr%vgAM zgZUdp4-JmgGEyoFceLGKL(%|8yKNpEQjvwttVdL!H+$DHNq;JxU<_6hZN{ba#I z91jb(mtxhk=28SV4Ub&SPjj>gWA}MdBs=v;(dIlm8KDTOs$>~(#pRD&&<+H2)<`!r zuz(_fF&~K1#!BA|FR(wIaO5LFEq9(6d6dR@{5{Bk2=b&>;&(J8(A@eTxMUkcufF80 z7fXv8tC_4!VJ#HA2%&z$L&zQB$e$(qig;HAxv!B)73{!ntJeOM=aGT=b4r-`y2CA< zy_z7v?Q+5B2p12A!%CQii6siuwe&O=7r{LgEk;R)rDsG<1q_RVdZWC{o%G~UnvENa z0;}bS7hhA&Csfq(M3c)zZQoMbic70S4Z`s*0kxtwt&-KCWy_~lK%9I?=3I~JQWW8y z$%hCq(wwZzzhvg-zDdME+~TqMs1Lk&LG~iL+vJTgE>;=)O`(6ajo)y#9wko@*R>d&SR(o2> zb{TSSxEb=JVI;A-Ho`B^ZA`4Kr5+;iQ@Q7nKOH`GZEpE8Fh|N-6Kt(XVtkY)lj!An zE1BI9zxyvJc}sz-6CWeIgycr8(5N?Vqis1{U&~_olF1E1U(4Fv=;=OP&##{3*C9s~ z%RfCS&92I)xDU9|`AD-j0fTH_ka(Q;ytlQzuK4HuY0Kc#7u}!AxxDTCLUcGFhvw5b z#Jc4w25u9Op2>>AI!xzE{t4PidRO$CGjdho()y0AxMs)ocP(Cl zu`;WR$D1$eQ%&_{?-gZb65S=7T!)BBI$jaz2~lw;EAVusN4vYyhSQI4H6!Ooy~xQP zc;pOWng82MMY)- zU+UEb_J{1};d5M99!Wb}{8cr?&Fg2Cgd`-7D=RYofrX$!qPMGyN-Lfza25%qN!*gv zfU?PVrnnR-#OdC?)yHj9_D(W#2C8~Cu27)v`J$}iHNl%g!RdrZUw0`@;Dbq=egT~m zh_N#}ts*CIYxF`oZ;m>aAdiU}X76*z#MqQ&StNJ&;}E_-)T66D1V`b`$*0``A)k*% z&Z?dU)KZ;i3nKGAL@m~Re&P-#!o-B{cRMXL)fO9qt%o)q93Mo|LADuczfkZy$3cgy zYc$Fc{mE~yljpzP>hul{8LNAA3caFZk-jXlGW25CYj=CC>451t{%Cc|;10m>n2GU! zODBSN_hlB`n3LkcxrgUB4umgs7egg;e&5|6X7BERO19$sNTC}~n3JaVLfB3W4dFHF z`(rHK9d?Frj{gZg*;L<`@pETR0{nqA9H7{`JHV%Nrv!0H;i+@ok$*t2QxN(O=<$UR ogdyCPt-JV?0#V=J5;uf%{tx!w({tFmPv|EM#=Umw5GJO715IuYHvj+t literal 0 HcmV?d00001 diff --git a/research/fixed-tape-affine-shear/independent.py b/research/fixed-tape-affine-shear/independent.py new file mode 100644 index 0000000000..0d93b49039 --- /dev/null +++ b/research/fixed-tape-affine-shear/independent.py @@ -0,0 +1,155 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Separate table interpreter and coordinate gather oracle; no producer imports. + +Dense tape mechanics follow David Arias's PR2776 independent checker. +The runtime affine contract, fixtures and validation are new. +""" +import itertools + +BLANK, LEFT, RIGHT, ZERO, ONE, UNIT, MARK = range(7) +TAPES = 19 +INPUTS = (0, 4, 5, 6, 7, 14, 16) +WORK = (2, 3, 8, 9, 10, 11, 12, 13, 15, 17, 18) + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def validate(program): + need(set(program) == {'tapes', 'entry', 'instructions'} and program['tapes'] == TAPES, + 'fixed nineteen-tape program schema') + code = program['instructions'] + target = lambda x: type(x) is int and 0 <= x < len(code) + tape = lambda x: type(x) is int and 0 <= x < TAPES + need(target(program['entry']), 'finite entry') + for pc, row in enumerate(code): + op = row[0] + if op == 'branch': + need(len(row) == 4 and tape(row[1]) and target(row[3]), 'local branch') + need(len(set(x[0] for x in row[2])) == len(row[2]), 'unique branches') + need(all(type(s) is int and 0 <= s < 7 and target(p) for s, p in row[2]), 'finite branches') + elif op == 'move': + need(len(row) == 3 and tape(row[1]) and type(row[2]) is int and row[2] in (-1, 1), + 'literal unit motion') + elif op == 'write': + need(len(row) == 3 and tape(row[1]) and type(row[2]) is int and 0 <= row[2] < 7, + 'local alphabet write') + elif op == 'goto': + need(len(row) == 2 and target(row[1]), 'finite jump') + elif op in ('halt', 'reject'): + need(len(row) == (1 if op == 'halt' else 2), 'terminal schema') + else: + raise ValueError('unsupported instruction') + if op in ('move', 'write'): + need(target(pc + 1), 'finite successor') + + +class DenseTape: + def __init__(self, cells, head): + self.base = min(cells, default=head) + end = max(cells, default=head) + self.cells = [BLANK] * (end - self.base + 1) + for k, v in cells.items(): + self.cells[k - self.base] = v + self.head = self.low = self.high = head + + def read(self): + k = self.head - self.base + return self.cells[k] if 0 <= k < len(self.cells) else BLANK + + def write(self, value): + k = self.head - self.base + if k < 0: + self.cells[:0] = [BLANK] * -k + self.base = self.head + k = 0 + if k >= len(self.cells): + self.cells.extend([BLANK] * (k - len(self.cells) + 1)) + self.cells[k] = value + + def move(self, delta): + self.head += delta + self.low = min(self.low, self.head) + self.high = max(self.high, self.head) + + def snapshot(self): + return {self.base + k: v for k, v in enumerate(self.cells) if v != BLANK} + + +def execute(program, bank, cap): + validate(program) + tapes = [DenseTape(*row) for row in bank] + code, pc, steps = program['instructions'], program['entry'], 0 + while True: + need(steps < cap, 'experimental execution cap') + steps += 1 + row = code[pc] + op = row[0] + if op == 'halt': + return tapes, steps + if op == 'reject': + raise ValueError('machine rejected: ' + row[1]) + if op == 'goto': + pc = row[1] + elif op == 'branch': + symbol = tapes[row[1]].read() + pc = next((p for s, p in row[2] if s == symbol), row[3]) + else: + if op == 'move': + tapes[row[1]].move(row[2]) + else: + tapes[row[1]].write(row[2]) + pc += 1 + + +def marked(bits, origin): + return ({origin: LEFT, **{origin + k + 1: v for k, v in enumerate(bits)}, + origin + len(bits) + 1: RIGHT}, origin + 1) + + +def binary(n, origin): + return marked([ONE if n >> j & 1 else ZERO for j in range(n.bit_length())], origin) + + +def fixtures(shape, coefficient, offset, payload, translated=False): + p, q, g, s = shape + need(all(type(n) is int and n > 0 for n in shape), 'positive extents') + need(len(payload) == p * q * q * g * s and all(type(b) is int and b in (0, 1) for b in payload), + 'complete Boolean stream') + origins = [i * 3 - 23 if translated else 0 for i in range(TAPES)] + bank = [({}, k) for k in origins] + bank[0] = marked([ONE if b else ZERO for b in payload], origins[0]) + for t, value in zip((4, 5, 6, 7, 14, 16), (*shape, coefficient + 1, offset + 1)): + bank[t] = binary(value, origins[t]) + return bank + + +def oracle(shape, coefficient, offset, payload, inverse=False): + p, q, g, s = shape + sign = -1 if inverse else 1 + out = [] + # Gather by output coordinate, with a direct flat-address formula. + for a, x, b, y, z in itertools.product(range(p), range(q), range(g), range(q), range(s)): + original_y = (y - sign * (coefficient * x + offset)) % q + index = ((((a * q + x) * g + b) * q + original_y) * s + z) + out.append(payload[index]) + return out + + +def check_result(tapes, steps, bank, shape, coefficient, offset, payload, inverse=False): + expected = oracle(shape, coefficient, offset, payload, inverse) + for t in INPUTS: + need(tapes[t].snapshot() == bank[t][0], 'input preservation ' + str(t)) + need(tapes[t].head == bank[t][1], 'input head return ' + str(t)) + for t in WORK: + need(not tapes[t].snapshot(), 'whole scratch erasure ' + str(t)) + need(tapes[t].head == bank[t][1], 'scratch head return ' + str(t)) + cells, head = marked([ONE if b else ZERO for b in expected], bank[1][1]) + need(tapes[1].snapshot() == cells and tapes[1].head == head, 'affine output and head') + volume = len(payload) + need(steps <= 1024 * volume, 'proved conservative physical transition bill') + span = sum(t.high - t.low + 1 for t in tapes) + need(span <= 64 * volume, 'proved visited-cell bill') + return span diff --git a/research/fixed-tape-affine-shear/kernel.py b/research/fixed-tape-affine-shear/kernel.py new file mode 100644 index 0000000000..694e03ee3d --- /dev/null +++ b/research/fixed-tape-affine-shear/kernel.py @@ -0,0 +1,143 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Literal runtime-coefficient affine shear, using PR2776's paid macros.""" + +C_INPUT, C_COUNT, OFFSET_INPUT, OFFSET_COUNT, X_COUNT = range(14, 19) +TAPES = 19 +EXTRA_WORK = (C_COUNT, OFFSET_COUNT, X_COUNT) + + +def build_program(modules, inverse=False): + if type(inverse) is not bool: + raise ValueError('fixed Boolean direction') + b, m, c = (modules[k] for k in ('shear', 'machine', 'counters')) + a = m.Assembler(TAPES) + fail = a.fresh('invalid_affine_interface') + work = b.SCRATCH_TAPES + EXTRA_WORK + + def trim_one(tape, prefix): + b._seek_right(a, tape, fail, prefix + '_end') + a.write(tape, m.BLANK) + a.move(tape, -1) + good = a.fresh(prefix + '_positive') + a.branch(tape, {m.UNIT: good}, fail) + a.label(good) + a.write(tape, m.RIGHT) + c.emit_rewind(a, tape, prefix + '_return') + + def strict_below_q(tape, prefix): + c.emit_rewind(a, X_COUNT, prefix + '_Q') + loop, unit, advance, end, good = (a.fresh(prefix + s) for s in + ('_loop', '_unit', '_advance', '_end', '_good')) + a.label(loop) + a.branch(tape, {m.UNIT: unit, m.RIGHT: end}, fail) + a.label(unit) + a.branch(X_COUNT, {m.UNIT: advance}, fail) + a.label(advance) + a.move(tape, 1) + a.move(X_COUNT, 1) + a.goto(loop) + a.label(end) + a.branch(X_COUNT, {m.UNIT: good}, fail) + a.label(good) + c.emit_rewind(a, tape, prefix + '_coefficient') + c.emit_rewind(a, X_COUNT, prefix + '_Q_return') + + def transfer_one(prefix): + b._decrease_left_increase_right(a, fail, prefix + '_transfer') + a.move(b.LEFT_LENGTH, -1) + nonzero, zero, done = (a.fresh(prefix + s) for s in ('_positive', '_zero', '_done')) + a.branch(b.LEFT_LENGTH, {m.UNIT: nonzero, m.LEFT: zero}, fail) + a.label(nonzero) + a.move(b.LEFT_LENGTH, 1) + a.goto(done) + a.label(zero) + a.move(b.LEFT_LENGTH, 1) + b._reset_lengths(a, fail, prefix + '_wrap') + a.label(done) + + def advance_by(tape, prefix): + c.emit_rewind(a, tape, prefix + '_counter') + loop, unit, done = (a.fresh(prefix + s) for s in ('_loop', '_unit', '_done')) + a.label(loop) + a.branch(tape, {m.UNIT: unit, m.RIGHT: done}, fail) + a.label(unit) + transfer_one(prefix + '_one') + a.move(tape, 1) + a.goto(loop) + a.label(done) + + def phase(operations, prefix): + c.emit_rewind(a, b.P_COUNT, prefix + '_P_return') + p_loop, p_body, x_loop, x_body, g_loop, body, next_x, next_p, done = ( + a.fresh(prefix + s) for s in + ('_P', '_P_body', '_x', '_x_body', '_G', '_body', '_next_x', '_next_P', '_done')) + a.label(p_loop) + a.branch(b.P_COUNT, {m.UNIT: p_body, m.RIGHT: done}, fail) + a.label(p_body) + c.emit_rewind(a, X_COUNT, prefix + '_x_return') + a.label(x_loop) + a.branch(X_COUNT, {m.UNIT: x_body, m.RIGHT: next_p}, fail) + a.label(x_body) + c.emit_rewind(a, b.G_COUNT, prefix + '_G_return') + a.label(g_loop) + a.branch(b.G_COUNT, {m.UNIT: body, m.RIGHT: next_x}, fail) + a.label(body) + for i, (length, source, destination, consume) in enumerate(operations): + b._segment(a, length, source, destination, consume, fail, prefix + '_segment_' + str(i)) + a.move(b.G_COUNT, 1) + a.goto(g_loop) + a.label(next_x) + advance_by(C_COUNT, prefix + '_coefficient') + a.move(X_COUNT, 1) + a.goto(x_loop) + a.label(next_p) + a.move(b.P_COUNT, 1) + a.goto(p_loop) + a.label(done) + + for tape in (b.OUTPUT,) + work: + empty = a.fresh('initialize') + a.branch(tape, {m.BLANK: empty}, fail) + a.label(empty) + a.write(tape, m.LEFT) + a.move(tape, 1) + for src, dst, name in ((b.P_INPUT, b.P_COUNT, 'P'), (b.Q_INPUT, b.LEFT_LENGTH, 'Q'), + (b.G_INPUT, b.G_COUNT, 'G'), (b.S_INPUT, b.S_COUNT, 'S'), + (b.Q_INPUT, X_COUNT, 'x_extent'), + (C_INPUT, C_COUNT, 'coefficient_plus_one'), + (OFFSET_INPUT, OFFSET_COUNT, 'offset_plus_one')): + c.emit_binary_to_unary(a, src, b.BINARY_WORK, dst, 'prepare_' + name) + trim_one(C_COUNT, 'decode_coefficient') + trim_one(OFFSET_COUNT, 'decode_offset') + strict_below_q(C_COUNT, 'bound_coefficient') + strict_below_q(OFFSET_COUNT, 'bound_offset') + a.write(b.RIGHT_LENGTH, m.RIGHT) + b._seek_right(a, b.LEFT_LENGTH, fail, 'initial_left_end') + advance_by(OFFSET_COUNT, 'initial_offset') + gather = ((b.LEFT_LENGTH, b.SOURCE, b.SPLIT_A, False), + (b.RIGHT_LENGTH, b.SOURCE, b.SPLIT_B, False)) + emit = ((b.RIGHT_LENGTH, b.SPLIT_B, b.OUTPUT, True), + (b.LEFT_LENGTH, b.SPLIT_A, b.OUTPUT, True)) + if inverse: + gather, emit = tuple(reversed(gather)), tuple(reversed(emit)) + phase(gather, 'gather') + complete = a.fresh('source_complete') + a.branch(b.SOURCE, {m.RIGHT: complete}, fail) + a.label(complete) + for tape in (b.SPLIT_A, b.SPLIT_B): + a.write(tape, m.RIGHT) + c.emit_rewind(a, tape, 'bucket_return_' + str(tape)) + phase(emit, 'emit') + for tape in (b.SPLIT_A, b.SPLIT_B): + complete = a.fresh('bucket_complete') + a.branch(tape, {m.RIGHT: complete}, fail) + a.label(complete) + a.write(b.OUTPUT, m.RIGHT) + c.emit_rewind(a, b.SOURCE, 'source_return') + c.emit_rewind(a, b.OUTPUT, 'output_return') + for tape in work: + b._erase_back_to_origin(a, tape, 'clear_' + str(tape)) + a.halt() + a.label(fail) + a.reject('canonical affine extents, bounded coefficients and blank owned workspace') + return a.finish() diff --git a/research/fixed-tape-affine-shear/loader.py b/research/fixed-tape-affine-shear/loader.py new file mode 100644 index 0000000000..02aed787cc --- /dev/null +++ b/research/fixed-tape-affine-shear/loader.py @@ -0,0 +1,48 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Authenticate the actual source bytes before loading the retained macros.""" +import hashlib +import json +from pathlib import Path +import sys +import types + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def authenticate(overrides=None): + overrides = overrides or {} + manifest = json.loads((HERE / 'SOURCES.json').read_text()) + contents = {} + for row in manifest['files']: + if row['usage'] != 'input': + continue + raw = overrides.get(row['path'], (ROOT / row['path']).read_bytes()) + need(hashlib.sha256(raw).hexdigest() == 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: ' + row['path']) + contents[row['path']] = raw + return contents + + +def load_macros(contents): + modules = {} + names = ('machine', 'counters', 'shear') + need(all(name not in sys.modules for name in names), 'no preloaded predecessor modules') + try: + for name in names: + path = 'research/fixed-tape-ordered-shear/' + name + '.py' + module = types.ModuleType(name) + module.__file__ = str(ROOT / path) + sys.modules[name] = module + exec(compile(contents[path], module.__file__, 'exec'), module.__dict__) + modules[name] = module + finally: + for name in names: + sys.modules.pop(name, None) + return modules diff --git a/research/fixed-tape-affine-shear/verify.py b/research/fixed-tape-affine-shear/verify.py new file mode 100644 index 0000000000..2d8aca7d66 --- /dev/null +++ b/research/fixed-tape-affine-shear/verify.py @@ -0,0 +1,188 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Read-only source-bound finite-machine replay and controls.""" +import argparse +import gzip +import hashlib +import json +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +from loader import authenticate, load_macros, need +from kernel import build_program +import independent as i + + +def canonical(x): + return json.dumps(x, sort_keys=True, separators=(',', ':')).encode() + + +def export(program): + return json.loads(json.dumps(dict(tapes=program.tapes, entry=program.entry, + instructions=program.instructions))) + + +def pattern(n, seed): + return [((j * j + 3 * j + seed) ^ (j >> (seed % 3))) & 1 for j in range(n)] + + +def cases(): + for q in range(1, 9): + for c in range(q): + for h in range(q): + yield (1, q, 1, 1), c, h, pattern(q*q, c*7+h), False + for c in range(3): + for h in range(3): + for k in range(9): + yield (1, 3, 1, 1), c, h, [int(j == k) for j in range(9)], True + for shape in ((2, 5, 2, 2), (2, 6, 3, 2), (3, 7, 2, 2), (2, 9, 2, 3), (1, 17, 1, 1)): + p, q, g, s = shape + for c, h in ((0, q-1), (q-1, q-1), ((q+1)//2, 0), (2, 3 % q)): + yield shape, c, h, pattern(p*q*q*g*s, c+h), True + + +def source_binding(contents): + program = json.loads(gzip.decompress(contents['research/bit-row-route-generator/PROGRAM.json.gz'])) + selected = [s for s in program['steps'] if s['op'] == 'ordered_shift' + and s['addresses'] == [3, 0] and s['coefficient'] == [1, 2]] + need(bool(selected), 'actual source half leaf at ordered addresses 0 -> 3') + leaves = [s for s in program['steps'] if s['op'] == 'ordered_shift' + and s['addresses'][0] > s['addresses'][1]] + need(set(tuple(s['coefficient']) for s in leaves) == {(1, 1), (-1, 1), (1, 2), (-1, 2)}, + 'exact admitted later-target coefficient inventory') + half = [s for s in leaves if s['coefficient'][1] == 2] + for q in (3, 5, 7, 11): + for e in range(1, 9): + Q = q**e + need((2*((Q+1)//2)) % Q == 1 and (2*((Q-1)//2)) % Q == Q-1, + 'source half descriptor identity') + return dict(actual_half_0_to_3=len(selected), serialized_later_target_leaves=len(leaves), + serialized_half_leaves=len(half), source_f=program['f'], source_q=program['q'], + source_w=program['w'], descriptor_preparation='charged separate binary half/increment scan', + whole_route_admitted=False) + + +def physical(modules, mode, saved): + programs = {str(inv): build_program(modules, inv) for inv in (False, True)} + counts = {k: len(p.instructions) for k, p in programs.items()} + need(saved == {k: export(p) for k, p in programs.items()}, 'literal exported tables match assembler') + total = 0 + volume = 0 + max_steps = max_span = 0 + digest = hashlib.sha256() + for case_number, (shape, c, h, payload, translated) in enumerate(cases()): + for inverse in (False, True): + bank = i.fixtures(shape, c, h, payload, translated) + key = str(inverse) + if mode == 'primary': + m = modules['machine'] + run = m.Machine(programs[key], [m.Tape(cells, head) for cells, head in bank]).run(1024*len(payload)+1) + # Adapt only the observation interface, not the execution. + class View: + def __init__(self, tape, visits): + self.head = tape.head + self.cells = tape.cells + self.low = min(visits or {tape.head}) + self.high = max(visits or {tape.head}) + def snapshot(self): + return dict(self.cells) + tapes = [View(t, v) for t, v in zip(run.tapes, run.visits)] + steps = run.steps + else: + tapes, steps = i.execute(saved[key], bank, 1024*len(payload)+1) + span = i.check_result(tapes, steps, bank, shape, c, h, payload, inverse) + total += 1 + volume += len(payload) + max_steps = max(max_steps, steps) + max_span = max(max_span, span) + digest.update(canonical([shape, c, h, inverse, steps, span, i.oracle(shape, c, h, payload, inverse)])) + return dict(cases=total, payload_bits=volume, instructions=counts, tapes=19, alphabet_symbols=7, + transitions_bound_per_bit=1024, visited_cells_bound_per_bit=64, + maximum_fixture_steps=max_steps, maximum_fixture_span=max_span, + transcript_sha256=digest.hexdigest()) + + +def expect_reject(fn, text): + try: + fn() + except (ValueError, RuntimeError): + return + raise ValueError('control accepted: ' + text) + + +def controls(modules, saved, contents): + base = saved['False'] + shape, c, h = (2, 5, 2, 2), 3, 2 + payload = [int(j == 0) for j in range(200)] + checks = [] + for field, value in ((4, 0), (5, 0), (6, 0), (7, 0), (14, 6), (16, 6)): + bank = i.fixtures(shape, c, h, payload) + bank[field] = i.binary(value, 0) + expect_reject(lambda: i.execute(base, bank, 100000), 'bad extent/coefficient') + checks.append('input_' + str(field)) + bank = i.fixtures(shape, c, h, payload) + bank[14] = i.marked([i.ONE, i.ZERO], 0) + expect_reject(lambda: i.execute(base, bank, 100000), 'noncanonical coefficient') + checks.append('noncanonical') + bank = i.fixtures(shape, c, h, payload) + bank[2] = ({0:i.ONE}, 0) + expect_reject(lambda: i.execute(base, bank, 100000), 'occupied scratch') + checks.append('occupied_scratch') + bad = json.loads(json.dumps(base)) + pos = next(k for k, r in enumerate(bad['instructions']) if r == ['move', 0, 1]) + bad['instructions'][pos][2] = 2 + expect_reject(lambda: i.validate(bad), 'nonlocal move') + checks.append('nonlocal_move') + bank = i.fixtures(shape, c, h, payload) + tapes, steps = i.execute(saved['True'], bank, 100000) + expect_reject(lambda: i.check_result(tapes, steps, bank, shape, c, h, payload), 'wrong orientation') + checks.append('wrong_orientation') + for t, symbol in ((2, i.ONE), (17, i.LEFT)): + tapes, steps = i.execute(base, bank, 100000) + tapes[t].write(symbol) + expect_reject(lambda: i.check_result(tapes, steps, bank, shape, c, h, payload), 'retained scratch') + checks.append('retained_scratch_' + str(t)) + path = next(iter(contents)) + expect_reject(lambda: authenticate({path: contents[path] + b'\n'}), 'source mutation') + checks.append('source_hash') + # Endpoint-preserving unbilled work must change the physical observation. + bad = json.loads(json.dumps(base)) + halt = next(k for k, r in enumerate(bad['instructions']) if r[0] == 'halt') + bad['instructions'][halt] = ['goto', len(bad['instructions'])] + bad['instructions'].extend([['move', 1, 1], ['move', 1, -1], ['halt']]) + good_tapes, good_steps = i.execute(base, bank, 100000) + bad_tapes, bad_steps = i.execute(bad, bank, 100000) + need(all(t.snapshot() == u.snapshot() and t.head == u.head for t,u in zip(good_tapes,bad_tapes)), + 'cost-only mutation preserves endpoint') + need(bad_steps == good_steps + 3, 'cost-only mutation observation includes jump and moves') + checks.append('unbilled_extra_steps') + return checks + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument('--write', action='store_true') + parser.add_argument('--mode', choices=('primary', 'independent', 'controls'), default='independent') + args = parser.parse_args() + contents = authenticate() + modules = load_macros(contents) + tables = {str(inv): export(build_program(modules, inv)) for inv in (False, True)} + table_path = HERE / 'TABLE.json.gz' + if args.write: + table_path.write_bytes(gzip.compress(canonical(tables), mtime=0)) + saved = json.loads(gzip.decompress(table_path.read_bytes())) + need(saved == tables, 'complete table export') + result = dict(schema_version=1, binding=source_binding(contents), + physical=physical(modules, 'independent' if args.mode == 'controls' else args.mode, saved), + controls=controls(modules, saved, contents)) + receipt = HERE / 'RESULT.json' + if args.write: + receipt.write_text(json.dumps(result, indent=2, sort_keys=True)+'\n') + need(canonical(result) == canonical(json.loads(receipt.read_text())), 'typed exact receipt comparison') + print('PASS_FIXED_TAPE_AFFINE_SHEAR', args.mode, json.dumps(result['physical'], sort_keys=True)) + + +if __name__ == '__main__': + main() From 9027b471aff9f6bcad64def5aa038ed98259750c Mon Sep 17 00:00:00 2001 From: JoyboyBrian <122925040+JoyboyBrian@users.noreply.github.com> Date: Thu, 22 Oct 2026 23:20:27 -0700 Subject: [PATCH 2/3] Bind the actual half-coefficient leaf with literal preparation and full resource proof --- research/fixed-tape-affine-shear/PROOF.md | 199 ++++++++++++++++++ research/fixed-tape-affine-shear/RESULT.json | 9 +- research/fixed-tape-affine-shear/SOURCES.json | 7 + .../fixed-tape-affine-shear/TABLE.json.gz | Bin 3078 -> 5786 bytes research/fixed-tape-affine-shear/kernel.py | 92 ++++++++ research/fixed-tape-affine-shear/verify.py | 73 ++++++- 6 files changed, 375 insertions(+), 5 deletions(-) create mode 100644 research/fixed-tape-affine-shear/PROOF.md diff --git a/research/fixed-tape-affine-shear/PROOF.md b/research/fixed-tape-affine-shear/PROOF.md new file mode 100644 index 0000000000..3b2e34e6ee --- /dev/null +++ b/research/fixed-tape-affine-shear/PROOF.md @@ -0,0 +1,199 @@ +# Literal runtime affine shear and its source half-coefficient leaf + +This is an algorithmic proof for the supplied finite programs. It is not a +proof-kernel result, a native operator proof or a complete supplier admission. +The split/merge idea and the local machine/counter/copy macros are David Arias's +PR2776. Charles Bethin's unit-carry kernel is the closest fixed-carry successor. +The new feature is an arbitrary **runtime** coefficient and offset, with their +complete conversion, wrap, reset and cleanup costs. + +## Contract and fixed machine + +For every positive integer `P,Q,G,S` and `0<=c,C (p,x,g, y +/- (c*x+C) mod Q, z). +``` + +The total cost, including descriptor conversion, all carries, rewinds and +cleanup, is at most `1024V` transitions and `64V` visited tape cells. The space +bill includes visited cells subsequently cleared; it is not a final live-space +count. Invalid inputs need not be cleaned up on rejection. This is a valid-input +contract; inspecting one initial cell does not certify an otherwise unbounded +scratch tape is empty. + +## Split invariant and termination + +PR2776's retained binary-to-unary macro preserves its canonical input and +returns its work tape blank. Convert seven values: `P,Q,G,S,Q,c+1,C+1`. +The second Q copy is a genuine independent x-traversal counter. Remove one +unary mark from each last counter, and compare each with the Q counter to +reject `c>=Q` or `C>=Q`. These comparisons are literal finite loops. + +At a boundary the two split tapes have lengths `(L,R)=(Q-r,r)` with `0<=r r+1 mod Q`. The transient `(0,Q)` is reset before any payload. +Initialization advances by C. At the start of the x-th group, therefore, + +``` +r = C + c*x mod Q, (L,R) = (Q-r,r). +``` + +For every gap g, gather the first L source records into A and the remaining R +into B; a record has S opaque bits. Advance the split by exactly c mark transfers +and advance the **separate** Q counter once. This works for zero and nonunit c: +traversal does not depend on the order or period of the offsets. After Q groups, +`C+cQ = C mod Q`, so no prefix reset or reconstructed coefficient is needed. +The same invariant applies to each next prefix and to the emission pass. + +Forward emission consumes B's next R records, then A's next L. This moves each +source y to y+r modulo Q. Inverse compilation reverses the two gather segments +and the two emission segments: it gathers R then L and emits L then R, giving +`y-r`. Both are permutations for **every** c; c need not be a unit because x is +preserved. Every copied bucket cell is consumed exactly once. Rewinds preserve +source and descriptors. The retained eraser clears each private region back +through its temporary LEFT origin marker and returns that head to its origin. + +All loops use finite positive unary counters or finite segments. Each x iteration +finishes c transfers; each wrap finishes Q transfers; P,Q,G,S are finite. This +proves termination and all endpoints for every permitted shape and payload. +Finite coefficient grids corroborate this argument; they do not replace it. + +## Complete uniform transition ledger + +The retained positive conversion takes +`24n - 7 popcount(n) + 15 bit_length(n) + 12 <= 44n` transitions. +A rewind from a right marker after h symbols costs `3h+3`; scanning/deleting one +unary suffix marker uses the actual local instructions in the retained source. +The following conservative blocks are upper bounds obtained by summing those +instructions. Every extent monomial displayed is at most V. + +| Executed block | Transition bound | +|---|---:| +| Initialize output and eleven private marked tapes | `36 <= 36V` | +| Seven conversions | `44(P+G+S+2Q+c+C+2) <= 308V` | +| Decode c+1,C+1 by one-mark removal | `6c+6C+22 <= 22Q <= 22V` | +| Two strict coefficient/Q comparisons, including rewinds | `11c+11C+22 <= 22Q <= 22V` | +| Initialize the split and advance C (no wrap) | `14C+3Q+6 <= 17Q <= 17V` | +| Two payload/traversal phases, excluding coefficient advancement | `23V+20PQ^2G+28PQG+20PQ+20P+8 <= 119V` | +| All coefficient advancements and cyclic resets in both phases | `2P[Q(17c+4)+c(10Q+3)] <= 54PQ^2 <= 54V` | +| Finish gather and rewind both buckets | `3V+9 <= 12V` | +| Finish output, source/output rewinds and all eleven complete erasures | `<=111V` | +| Final halt | `1 <= V` | + +Their sum is at most `802V`, below the stated `1024V` allowance. + +For the phase row, one record copy costs at most `(11+consume)S+4`, and a segment +of length l costs at most `(11+consume)Sl+10l+4`, including its length rewind. +The two segment lengths sum to Q regardless of gcd(c,Q). Summing the actual +P/x/G loop branches and unit moves gives the displayed two-phase polynomial. +No uniform distribution of offsets is used in this bound. + +For the advancement row, a coefficient rewind costs at most `3c+3`; c ordinary +transfers plus loop tests cost at most `14c+1`. Each cyclic reset adds at most +`10Q+3`. Across all Q x-groups at one prefix there are exactly c resets, since +the total advance is cQ starting at C=1`, the complete high fields have common extent `Q=q^e`, and + +``` +2 * ((Q+1)/2) = Q+1 = 1 mod Q. +``` + +Thus the runtime multiplier is c=(Q+1)/2. The negative half leaf is the inverse +program. This grows with e; treating the rational factor as a fixed number of +unit shears would be an invalid uniform-time argument. + +The complete linked half program includes a **literal** preparer on the same +nineteen-tape bank. It checks that Q's low bit is one and at least one further +bit exists, copies the remaining bits into an owned blank coefficient tape, +then performs a ripple increment beginning at its second bit. The copied +integer is floor(Q/2); the result is `floor(Q/2)+2=(Q+3)/2=c+1`. The final +high-bit check enforces canonical encoding. It returns Q and both input heads. +After the generic kernel, a literal scan erases every coefficient bit and its +markers, returning its tape to its original blank origin. These tables are +retained in TABLE.json.gz together with the generic programs; linking adjusts +only finite state destinations, not runtime addresses. + +Preparation costs at most `40 bit_length(Q)+80 <= 67Q` for Q>=3. Complete owned +descriptor erasure costs at most `8 bit_length(Q)+8 <= 11Q`. Their tape cells +already lie within the generic space ledger. The linked half call therefore +costs less than `880V`, still within `1024V` and `64V`, including preparation and +cleanup. General c,C are supplied descriptors; preparing arbitrary rational +coefficients from a caller is not made free by this half-specific construction. +The offset descriptor is C+1=1 for this actual source leaf and is preserved. + +For an actual complete source packet, group every coordinate before source0 as +P, those between source0 and target3 as G, and those after target3 as S. Their +extents may be enormous; the proof quantifies over them. No sorting, random +access, hidden high-coordinate lookup or ordinary interchange is used. This +binds the later-target half leaf on the complete-high-fiber interface. The +finite executed fixtures compress these spectator dimensions and do not +materialize the full source high matrix or prove the whole native invocation. +Other later-target +/-1 and +/-1/2 slots have the same interface; no claim about +reversed-field slots or unit_scale is implied. + +## Remaining obligations and decision + +This closes one physically priced ordered-affine primitive with a source-bound +half descriptor. It does not construct PR4989's complete low-type cache, native +canonical call, raw-body call, completed ordinary swap, ROW padding or the full +compiled matcher. Installation in the whole recursive owner bank, matched +physical tape allocation, reserve/precision/threshold constants and the P3 +recurrence remain open. Output/source separation is explicit; replacing the +source owner by the output or erasing that original source needs the caller's +paid ownership protocol. No selected frontier or multiplication exponent is +changed. Continue only after one of those separate contracts is selected and +its complete allowance is stated; another small coefficient fixture is not a +new contribution. diff --git a/research/fixed-tape-affine-shear/RESULT.json b/research/fixed-tape-affine-shear/RESULT.json index 36ebcd4673..7af71ddbce 100644 --- a/research/fixed-tape-affine-shear/RESULT.json +++ b/research/fixed-tape-affine-shear/RESULT.json @@ -1,7 +1,7 @@ { "binding": { "actual_half_0_to_3": 1, - "descriptor_preparation": "charged separate binary half/increment scan", + "descriptor_preparation": "literal linked binary half/increment preparation and owned erasure", "serialized_half_leaves": 96, "serialized_later_target_leaves": 160, "source_f": 1, @@ -25,6 +25,13 @@ "source_hash", "unbilled_extra_steps" ], + "half": { + "complete_half_calls": 10, + "descriptor_cases": 107, + "preparation_instructions": 47, + "program_instructions": 934, + "transcript_sha256": "6b7b6dec6ea20a8caab4d8ecc57087d5cd1e94791d600ed8b90f91cd1e260119" + }, "physical": { "alphabet_symbols": 7, "cases": 610, diff --git a/research/fixed-tape-affine-shear/SOURCES.json b/research/fixed-tape-affine-shear/SOURCES.json index 2064c10cd0..51f0898f47 100644 --- a/research/fixed-tape-affine-shear/SOURCES.json +++ b/research/fixed-tape-affine-shear/SOURCES.json @@ -63,6 +63,13 @@ "commit": "bee95ce88f9f19802f0613f92838895cd0e14a1f", "sha256": "b620b2fbca0261972f96585f5adfd170fc0aa9591a9952d8cc6d7aac327737c3", "git_blob": "358ba70e944e8bbef3504da5d59089255b4ded9f" + }, + { + "path": "research/bit-row-route-generator/interpreter.py", + "usage": "input", + "commit": "bee95ce88f9f19802f0613f92838895cd0e14a1f", + "sha256": "10b68232a7b642e7746393b505326fbf6832e7d64c1e0ddc3858835ae74283f9", + "git_blob": "90f79f9d7e7bf57d392ca51232596809d51fc0a8" } ] } diff --git a/research/fixed-tape-affine-shear/TABLE.json.gz b/research/fixed-tape-affine-shear/TABLE.json.gz index 2299b468a71c2065c3d72f5e657e28fc591a4498..5dd4d81c7e4aa49908380c84b8f1b3d7ef55ec7c 100644 GIT binary patch literal 5786 zcmchZWmJ^kx5w#Dk%pm>l5QBJOBw+gIwXamh8U1WkPemZmQHEmhcI-FfHaB-L&pqA z-|=_6q=9EgmnY6!RI`m>5GA zd+Yb-^!joqcJXFwA>{h-?pdW|zlS9p@3%*hXVmK397$<#6eKt6#wkbLd!1(? z$;dNWw^SVbeouYjmuYc6zOin!c`H9WbJ-t-Bj_~qn-|Ar#U#Upw#DUKJQBQOLgh*; z=K98ycE!KXZHM+SZl$>KS(Tecf`1UAagC!L)D3^Q-$9^UL7_QegSv(N*ux0$(PpxZ zwpJFg4p@J^5^JS;Iz(?=2 zNtk%fKopJQky5Vv8Oks%?n*tP;$^j}ZkK3qTumK>i~b1uwSAwthS3~|17V$QATJAT zrdwEX8w_a!=R6f9{prG$4z?L@PIqsA9%@TU4DEZkxm(*u{kR^7j}Pt-f-lViKBwrX zkOzD&YzPev?0Iv)wRaz8^8_9Ux%q?GyDzk{e(2~5hTb0DU%hHhHv94n_^`D-ez0)n;O&lH+|OM6HbdAZdMTskxFjV^8#`<8QSecI1(^X7$!DleSQ?xuV8ax(uu z^US%*BjIEs?QLs%bNWrp?YgJ0_$i|{ah0blabpQhJOtkj-*E?2BXVr+VLkzyW%sX# zRU5lD>@|~}VcGGp4|b0vY5B+>)1kDK=eijLYyT0*t#QRkj;2HkbUowq+)q*fWJ(Uh zOGhizV%>;WTXUWFNON^8mUJvGD@1eJ_jJ8j%4eG)@({^icc6pXS8#mAIRqKEZAb1s%fz|T=-_$!to|BoZugn3FJSgXXMzduxq)z572Dc% z6JI+Bo@DTaZJjXI%6UX7H-61crmeSwJaA87QX_-rjaDcBYdt$pJ>xa1a3`w#g0JLr zju<8#sy!yfFRg9G2((B_WIjEemKCQr*-{Ftf016+rBFR3Sgz+>o^>yXAmc&^X9mDW zvP{>R?|@##e}&#a207RSAH{#Z?z?bOGt5dSJUtB8+0Lam%#IM+5&b@el7__l^NWp% zDBzf>b_Jv{W;_mDj{;;Uoj}dj%0HM-96d{=Ri6#TH3)SK5hKhTu3zhCNy+_G*{mTYV&sI-0i}!iFPcmq+KlwPC>ZP;&8hp1Y zw^-^&bYPwIHVckP&=i+=%r3=E7_@GfGDY!im&Dg+Gm?SS%Kw2fLpZWPZRh<{*|jxQ zXQ^R$`Ru2!*;Y>4de}vRJeIL4Ap?>7&7SA%nRanc(!uKxWX{z!42*RcIY!QWNcGw$8$_ zA2=uWpy_>nO(-MOOZUFvMQ)~vg+Qfv#gqweeth>ahVXU|Mn#D(RZqfdR@qmvLZl`s z)t*%^(ki?~2H=GkL+K~bwZ+*W)^(0Z+@RCXbUUB-`gpN?Ez0!MF7U_vT<%zxsps3M zlr9D@g8<2$R?DWLWYW?Eqk>h;zGwS}9>oC4{HIb{K30{MU)2S5!Y0X-GDDE*Ayu5~ ztu3-1m{Tvh`HZcee6##eeKb}j(>DXr`@-Snd6>+)kt#Q3Duk!@!HvVPO~yvA8a8Dj z197`#jv$sX+zk28sUwmZeOnG35e)QEr~ZxFW^X`CUdtHcFK)%Z0> zxa3adLT7$W)aUabHto9<r@aHW;mpA3zpV1=KF zCzL_sK0F7^yA}&eYZeP!_dE#rwz6E=rJJma;H%1|EuEj@(&UqypNL-`d%!w?U@8`* z_l<-`Q7sQl+PE+>EuL_4!Q{M&OZ#bY0r`e0tsuAio$|^#^N}HFIjehjSpysiUWSe! zR+z+fHnDPRmR&jL`&X0}KH3nX}S9ClUuz8H0G6QsnB{S0raHC)i;3zVPA7?At zgZpTr|I|%b>1i8*Q=Q9`{kIrPON8wvA!9&gTNOHis!M`_dTPpC_V2U<#U=>uMI|5H z_qq4F%BK=j`=_r_BN8b-W{Cz(Pp$lM_S+l)d?`vY-y@De*qRLmUDRe{1;q!18O{Vv z!LEP0B#IU@@zyTpI$q*Dfw)>GZ$)Ak55MUXpE60YJlA~5U}?^fm@`aNWd*~JT2V0B z{39G#dHrHwD?aQn;cTQ`@=sue74bkQZa0ncMU`?9q??BQpv|4_W76}JCrfRL>T6t- zt$~7pM!iF-+Vu4e{N!VV@#({nooAh{!rbt$Tnn{YflWx^Hll+=mw{W1HF2-U!K{5R zNqF0Z3KaCm*xuL4XP3(9ox@FXEkqmbwo6AZVo6Y-pr6a^plHvw?;WoHx&$uFgMKCo zm^YXQUb#W zq=>}1)jN18mZBo&Z{L2mgj|`4qAn(2M-na9cu6k3vPlF*hX+dAQb|=WU~0re&iTcA z@hi`r#9PCd)Wv+Uvz00O7$3gg%{(P*$-;cGbgT}yr6N#Lmp~6l5}`I~W??SbAnW-n z{U@^l<$fn;yg$S0p1vl6jh?D*gOf%q@%h2rhjX3jv|z0~AwsoaU@0L+G5c9a@CEdjs)JubiGHcupWVchy`OO!Q{w82#gTe8 zsDEk_2AP*`RX4m7^;zXOdb(8iyv=ox%(U*64bUI+G1@7XsgI)8`o8kokg5kl(f~;^ zhIF!?`v3k)TqyPNadDk{88SCXQ#}v`{#E5zp6B-oQBeduw6kAhR82aYc z?*XxQgb0QDTzcK|Z&cjfUR|8BnCX9crbq5f>-vnj-Uj?-^^4_$E&L1lV%VE|Ncb5( zPuTyLd9c9PcAqiBd{53_6oPwommhg%h`;T?!ow1*bX62}Ch@feW9&0J79;dS4tG0> zY%Es6Kmi$fc8IY}ZgBsvxg;N3+-$<)*{BacqxQR$A{>j&FACX3e@!$N+oE`7iofkX z;_%-oVxIrV#o6A{Gf=odXTsgyGA|0DE4sxTWBK2vfq1M?_3msVtn==6j&w2r{QVYc zEL(l%V!gggm-p2fB0{K>#EXRyve*R{U zYpF`gmH3PeS=Fnn9+y%C!;lDg!Dyb{n9?qnlkJ zBNv2_k*Ni9WGQE021Y5yNzy!z@WE~Rry81e+YPfZ_PQ4|ovdv?R?4CB%&K(sdCws5 zw^I;lr5!t|lDw#x(vcUc6#;1$jll(ejr@(lrT+6}&pF0U9j}tmOhdh+nm0tvfEk^1 zY8l5k*o@gm)*3eFA+rt!GMTe}^)SL| z7JvShEENpKgnLI$te5bpj-8;CP+adXb0$6FI2pRx4#J^wXxP%Pg~5rU6p0wOI+=iY zjUq80Sd1`A=f;$$e!RiKX-Nk8dIKMC5liBO^&)M3c0mP)<*;zsz%@4NM9#Jp0Cs;H zlFpzutPshnwNVD+!MF`F)OqSwaFj+&Dm zDl?v|$>G;%utt?@vwhr~N)- zdJ0)ZQIVrkLS6J`rh8AQZuSw)<{Jw2nU>wWxuFhaCWoNM~O<-ylS2vOfWRqBuWi0yr4n0ZOHDtj;(z&w_VF?449j z&`U#eaVc!%R?0Pom#qS=RXFQ=S?=Ev zErxGQOY|!>T=H9DE4+p~;MicCwLB`~s!=xh98b_rtbVIWp}>9|^IAvc+of{R8j@}) zo^lVa)`;%EP!w?JL&}^aaG06jREzzNPa}CZKGQbFxxlKR8 zg3SqTua9~b@T+p$7(mpdb(ZgPS%H^V!_?5YRtxA*L8cf?MJwMA9Dav26HcSk#xVZ{@4MAp9-U}zJ=if@oWT4 zJ8p-B7^gIrR8j^)+<%$KyT)i`B1DKFj6sX;+wa^HM)t)+CA6)JVLZ_<9_ti-crrC& zgz*8u@tu^PB|%I}xvVmuD;Zf8kE97^pOKta<^#PeT6}MCPp>mqgX>n05#!88BXG+U z(6VV>l&4zGqZnZtNaH4WLR}EEJH2VnY88=sXwZO$PpyC{9yENOmX#TQ_NBR6l;c56 z(U*Jd2rP&2l~U%lOt?ML^`9zv+>fZ`ZW1J3G}kSWxIr63W+`o@QW!z#id@{)=X^U{ zc@H@HcCnKm|Ax5}h)=nTCeNm?)|B38@)Sgqr~Rm+dSY05fWZi{DwKp);+Pfd6OvBB z6-fucg_0beu+BOlE=f5A_K5DNV?a>Kbaz%S)W&hju@B0HVb>=5@vKN zVFc*WtCU@fD~AvvkVJ^sSGc@GUl^)rrLzsV?a>n&B}PdERR5j!t|=G5VT6|4nZe;7 zPiP_zdXT@H)Ytjzo<*1YvpLJL5j_{^zgNICEmPBV4$5JgZ`%-7wNX##Xa@_h|+SCa13{V+k^Om3+Z3*U* z{s|iPQ|K+~YEfxl#07{~2P;C+wF06R9A=;-pp^eFC%MNZK`Wq9dB508Bc!qwPz8tD zvee;U%t6ET_KSH*BNhhhXP`WZ{2RP=_`9uu8I66+-d2GB{}kC51|mPqBSQOP7E~m; zHn{8X56V#C)*x~NSKy`qh`a_4b>TB8LWNU<$d_bpBwc}CPyWqNq`e>EJPYmrzZS0X wtPWOrli9r!E7YJr9kuF^8cgDo;^~tTQg**F0hrIey?nr=zLS;%6JcWf7sEb^j4jWtSCg69})ey3K9 z8hdv0><(~w!dVEW??k5*s#Rt=7D%21m%hXTnN0^$B!E#8J+jj_%9;E@$HBW5jW_!u zX^~UDk@TJ+R3iY{8mJ6!g&hT*Y^?bOeGlH-L+|b{uKJy{djbyPg(*Vt;Bi%Q&W^Be zD_pHfKtCjM2z5v8*lV8wV`&$VotqBgob#6K9dO{J%p1Zxw7%=gbx|bhgA(KM@6%@I z@j-Al-OOhQwKUyJNV%KDzSK=GW?4m6Biw67lWx?9evx~S{G?5Jtu_t(b#yj(UK?t_ zv#Hoy5FP9cH2`kTj2gMzc)LQ|uRVda!1O07HX(jiVLP*g*7a-yu>a!$=KZfXfo6up z=so_vMY-meLI|AD?!YD@pbn^TRQ{^$E>4=tMr-r(8SClF#q~T%0Of@ZS%5qd?XQ~E z(4ZFiTQUpdP+q;ZL1WI^)VU{|jxH#V{ReDaIB8tnhiOIuRJD}gS8BF z%sr*Fh+QIc(&^pTMrfWNXY}l8MqL3Ns}0ja?j~FkKf`7p^EfoGLaDw7HMbJ9Uz;SY z8FR)|!+>+#cS701vpG-HCR>+x8Y|-a05<`x0-meC;^I3Z4;pVOl^ne$MB_1p#oZmQ7j_~Xl1c2m^z#XNqAR%Bh(zUuEE{X> zLJ#v5)y7+_KU@<-$s+1~gq|++tF#)}veNA0y5kVxDe_Eh(Yo$r_**v1-tf!}X=jZu zu?!SrzySkOa4TpgD6@mMK&~qo>*k=JYtB&ogCDV`$*!jL_!3#7K8rZ>0eq?DzTo_p zCwmtm3sa2Yw0UMf)0+%K@z%1FXf6|VSssBgrUL$wv+Ld=b3a#mi}8zOZw2lL*(4t) zXZJBd#erAZFIp09zH+7G2M6p;G@WxPCH_vn5nKv^=iWbLQe)4A-PTZTy_b8@KVb4* z4uTGB+UwL|Emj5;!{^U^yp_KR+>M3tIhf13+%nTm0BZ8ydn}W$X_nFA<0ns<1^I)` z%8eNC5)MSkkfnBBYmACXtO|9J#-m8cnm1{QbniK}xNzFPoh0@_q`$^Z4jk83sQ)_Y z%sXi%1v96JL~0R^dZesSWTC1M3xQkdi|%W9X=+0kXfX~zXRT46%| zHf!{8D#XY~Gn+Ko>o}7prX-HOJQKj9t4Gy4O>do5sc>xl6nAHak7k*g9-@h{PSGa5f2AIgNlb`GBYT*=4S$gB(JuRqq z4Xt|;6{HoGtp|{?p20R~bMS9q{Hx2*=Xu~M z$m1rg1TFwy2`zX%6(uNpu`)tc=9;NRKiRmTrx_Eh?yCa%8?caHVOS8)_Zi3bDdi3h ztN83_q3NfArDj9vF9X>JYHUC_~=1e z$u1-0kA)^u!}VY%0;%POJwHFQG&G_5kH?kjn}ei@N7a<2z^O|gzO;pwn~N@d+v;C= z=HZm*e)J!?3g{Hd)z`GEoCC>K3+c5M$}uEMgV(f!sY{L|U-?W!P|ue4&T8QjQgHqS z&3%8{#R%mZZyX?^A?bTNh8XjD8cp};5w&?AXb|KKvLQLQ`kgq`V6i$L9HVwr%vgAM zgZUdp4-JmgGEyoFceLGKL(%|8yKNpEQjvwttVdL!H+$DHNq;JxU<_6hZN{ba#I z91jb(mtxhk=28SV4Ub&SPjj>gWA}MdBs=v;(dIlm8KDTOs$>~(#pRD&&<+H2)<`!r zuz(_fF&~K1#!BA|FR(wIaO5LFEq9(6d6dR@{5{Bk2=b&>;&(J8(A@eTxMUkcufF80 z7fXv8tC_4!VJ#HA2%&z$L&zQB$e$(qig;HAxv!B)73{!ntJeOM=aGT=b4r-`y2CA< zy_z7v?Q+5B2p12A!%CQii6siuwe&O=7r{LgEk;R)rDsG<1q_RVdZWC{o%G~UnvENa z0;}bS7hhA&Csfq(M3c)zZQoMbic70S4Z`s*0kxtwt&-KCWy_~lK%9I?=3I~JQWW8y z$%hCq(wwZzzhvg-zDdME+~TqMs1Lk&LG~iL+vJTgE>;=)O`(6ajo)y#9wko@*R>d&SR(o2> zb{TSSxEb=JVI;A-Ho`B^ZA`4Kr5+;iQ@Q7nKOH`GZEpE8Fh|N-6Kt(XVtkY)lj!An zE1BI9zxyvJc}sz-6CWeIgycr8(5N?Vqis1{U&~_olF1E1U(4Fv=;=OP&##{3*C9s~ z%RfCS&92I)xDU9|`AD-j0fTH_ka(Q;ytlQzuK4HuY0Kc#7u}!AxxDTCLUcGFhvw5b z#Jc4w25u9Op2>>AI!xzE{t4PidRO$CGjdho()y0AxMs)ocP(Cl zu`;WR$D1$eQ%&_{?-gZb65S=7T!)BBI$jaz2~lw;EAVusN4vYyhSQI4H6!Ooy~xQP zc;pOWng82MMY)- zU+UEb_J{1};d5M99!Wb}{8cr?&Fg2Cgd`-7D=RYofrX$!qPMGyN-Lfza25%qN!*gv zfU?PVrnnR-#OdC?)yHj9_D(W#2C8~Cu27)v`J$}iHNl%g!RdrZUw0`@;Dbq=egT~m zh_N#}ts*CIYxF`oZ;m>aAdiU}X76*z#MqQ&StNJ&;}E_-)T66D1V`b`$*0``A)k*% z&Z?dU)KZ;i3nKGAL@m~Re&P-#!o-B{cRMXL)fO9qt%o)q93Mo|LADuczfkZy$3cgy zYc$Fc{mE~yljpzP>hul{8LNAA3caFZk-jXlGW25CYj=CC>451t{%Cc|;10m>n2GU! zODBSN_hlB`n3LkcxrgUB4umgs7egg;e&5|6X7BERO19$sNTC}~n3JaVLfB3W4dFHF z`(rHK9d?Frj{gZg*;L<`@pETR0{nqA9H7{`JHV%Nrv!0H;i+@ok$*t2QxN(O=<$UR ogdyCPt-JV?0#V=J5;uf%{tx!w({tFmPv|EM#=Umw5GJO715IuYHvj+t diff --git a/research/fixed-tape-affine-shear/kernel.py b/research/fixed-tape-affine-shear/kernel.py index 694e03ee3d..e9e4d4da79 100644 --- a/research/fixed-tape-affine-shear/kernel.py +++ b/research/fixed-tape-affine-shear/kernel.py @@ -141,3 +141,95 @@ def phase(operations, prefix): a.label(fail) a.reject('canonical affine extents, bounded coefficients and blank owned workspace') return a.finish() + + +def half_descriptor(modules): + """Finite preparation: odd Q>=3 on tape5 -> owned (Q+3)/2 on tape14.""" + b, m, c = (modules[k] for k in ('shear', 'machine', 'counters')) + a = m.Assembler(TAPES) + fail = a.fresh('invalid_half_descriptor') + empty, odd, first = (a.fresh(s) for s in ('owned_empty', 'odd_Q', 'copy_first')) + a.branch(C_INPUT, {m.BLANK: empty}, fail) + a.label(empty) + a.write(C_INPUT, m.LEFT) + a.move(C_INPUT, 1) + a.branch(b.Q_INPUT, {m.ONE: odd}, fail) + a.label(odd) + a.move(b.Q_INPUT, 1) + a.goto(first) + after_zero, after_one, copy_zero, copy_one, copied = (a.fresh(s) for s in + ('after_zero', 'after_one', 'copy_zero', 'copy_one', 'copied')) + a.label(first) + a.branch(b.Q_INPUT, {m.ZERO: copy_zero, m.ONE: copy_one}, fail) + for symbol, label, after in ((m.ZERO, copy_zero, after_zero), (m.ONE, copy_one, after_one)): + a.label(label) + good = a.fresh('blank_output') + a.branch(C_INPUT, {m.BLANK: good}, fail) + a.label(good) + a.write(C_INPUT, symbol) + a.move(C_INPUT, 1) + a.move(b.Q_INPUT, 1) + a.goto(after) + a.label(after) + targets = {m.ZERO: copy_zero, m.ONE: copy_one} + if symbol == m.ONE: + targets[m.RIGHT] = copied + a.branch(b.Q_INPUT, targets, fail) + a.label(copied) + a.write(C_INPUT, m.RIGHT) + c.emit_rewind(a, b.Q_INPUT, 'half_Q_return') + c.emit_rewind(a, C_INPUT, 'half_low_bit') + a.move(C_INPUT, 1) + loop, zero, one, grow, done = (a.fresh(s) for s in ('increment', 'zero', 'one', 'grow', 'done')) + a.label(loop) + a.branch(C_INPUT, {m.ZERO: zero, m.ONE: one, m.RIGHT: grow}, fail) + a.label(zero) + a.write(C_INPUT, m.ONE) + a.goto(done) + a.label(one) + a.write(C_INPUT, m.ZERO) + a.move(C_INPUT, 1) + a.goto(loop) + a.label(grow) + a.write(C_INPUT, m.ONE) + a.move(C_INPUT, 1) + a.write(C_INPUT, m.RIGHT) + a.label(done) + c.emit_rewind(a, C_INPUT, 'half_descriptor_return') + a.halt() + a.label(fail) + a.reject('odd canonical Q>=3 and blank owned coefficient tape') + return a.finish() + + +def half_program(modules, inverse=False): + """Link preparation, actual +1/2 leaf and complete coefficient erasure.""" + m = modules['machine'] + before, body = half_descriptor(modules), build_program(modules, inverse) + a = m.Assembler(TAPES) + # Descriptor is at its first bit after the completed runtime kernel. + end, bit, marker = (a.fresh(s) for s in ('erase_loop', 'erase_bit', 'erase_end')) + a.label(end) + a.branch(C_INPUT, {m.ZERO: bit, m.ONE: bit, m.RIGHT: marker}, marker) + a.label(bit) + a.write(C_INPUT, m.BLANK) + a.move(C_INPUT, 1) + a.goto(end) + a.label(marker) + modules['shear']._erase_back_to_origin(a, C_INPUT, 'erase_owned_coefficient') + a.halt() + after = a.finish() + starts = (0, len(before.instructions), len(before.instructions)+len(body.instructions)) + programs = (before, body, after) + rows = [] + for which, (program, start) in enumerate(zip(programs, starts)): + for row in program.instructions: + if row[0] == 'branch': + rows.append(('branch', row[1], tuple((s, p+start) for s,p in row[2]), row[3]+start)) + elif row[0] == 'goto': + rows.append(('goto', row[1]+start)) + elif row[0] == 'halt' and which < 2: + rows.append(('goto', starts[which+1])) + else: + rows.append(row) + return m.Program(tuple(rows), TAPES) diff --git a/research/fixed-tape-affine-shear/verify.py b/research/fixed-tape-affine-shear/verify.py index 2d8aca7d66..c18760c82a 100644 --- a/research/fixed-tape-affine-shear/verify.py +++ b/research/fixed-tape-affine-shear/verify.py @@ -2,6 +2,7 @@ # SPDX-License-Identifier: Apache-2.0 """Read-only source-bound finite-machine replay and controls.""" import argparse +import ast import gzip import hashlib import json @@ -11,7 +12,7 @@ HERE = Path(__file__).resolve().parent sys.path.insert(0, str(HERE)) from loader import authenticate, load_macros, need -from kernel import build_program +from kernel import build_program, half_program, half_descriptor import independent as i @@ -45,6 +46,10 @@ def cases(): def source_binding(contents): program = json.loads(gzip.decompress(contents['research/bit-row-route-generator/PROGRAM.json.gz'])) + semantics = ast.parse(contents['research/bit-row-route-generator/interpreter.py']) + expected = ast.parse("data['high'][a]=(data['high'][a]+z*data['high'][addresses[1]])%R").body[0] + need(sum(ast.dump(n) == ast.dump(expected) for n in ast.walk(semantics)) == 1, + 'actual source ordered-shift assignment and argument direction') selected = [s for s in program['steps'] if s['op'] == 'ordered_shift' and s['addresses'] == [3, 0] and s['coefficient'] == [1, 2]] need(bool(selected), 'actual source half leaf at ordered addresses 0 -> 3') @@ -60,14 +65,14 @@ def source_binding(contents): 'source half descriptor identity') return dict(actual_half_0_to_3=len(selected), serialized_later_target_leaves=len(leaves), serialized_half_leaves=len(half), source_f=program['f'], source_q=program['q'], - source_w=program['w'], descriptor_preparation='charged separate binary half/increment scan', + source_w=program['w'], descriptor_preparation='literal linked binary half/increment preparation and owned erasure', whole_route_admitted=False) def physical(modules, mode, saved): programs = {str(inv): build_program(modules, inv) for inv in (False, True)} counts = {k: len(p.instructions) for k, p in programs.items()} - need(saved == {k: export(p) for k, p in programs.items()}, 'literal exported tables match assembler') + need(all(saved[k] == export(p) for k, p in programs.items()), 'literal exported tables match assembler') total = 0 volume = 0 max_steps = max_span = 0 @@ -104,6 +109,51 @@ def snapshot(self): transcript_sha256=digest.hexdigest()) +def half_checks(modules): + total = 0 + digest = hashlib.sha256() + for q in (3, 5, 7, 9, 17): + shape = (2, q, 2, 2) + payload = pattern(8*q*q, q) + for inverse in (False, True): + c = (q+1)//2 + bank = i.fixtures(shape, c, 0, payload, True) + origin = bank[14][1]-1 + bank[14] = ({}, origin) + program = export(half_program(modules, inverse)) + tapes, steps = i.execute(program, bank, 1024*len(payload)+1) + expected = i.oracle(shape, c, 0, payload, inverse) + cells, head = i.marked([i.ONE if b else i.ZERO for b in expected], bank[1][1]) + need(tapes[1].snapshot() == cells and tapes[1].head == head, 'prepared half endpoint') + for t in i.INPUTS: + if t != 14: + need(tapes[t].snapshot() == bank[t][0] and tapes[t].head == bank[t][1], + 'half source/descriptor return') + for t in (*i.WORK, 14): + need(not tapes[t].snapshot() and tapes[t].head == bank[t][1], 'half owned return') + span = sum(t.high-t.low+1 for t in tapes) + need(steps <= 1024*len(payload) and span <= 64*len(payload), 'composed half physical bill') + digest.update(canonical([q,inverse,steps,span,expected])) + total += 1 + # Exact coefficient preparation, without payload execution, across carry chains. + preparation = export(half_descriptor(modules)) + for Q in [*range(3, 200, 2), 255, 257, 511, 513, 1023, 1025, 2**40-1, 2**40+1]: + bank = [({},0) for _ in range(19)] + bank[5] = i.binary(Q,0) + tapes, steps = i.execute(preparation,bank,1000*(Q.bit_length()+1)) + cells, head = i.binary((Q+3)//2,0) + need(tapes[14].snapshot() == cells and tapes[14].head == head, 'all-bit half descriptor') + need(tapes[5].snapshot() == bank[5][0] and tapes[5].head == bank[5][1], 'half Q preservation') + need(steps <= 40*Q.bit_length()+80, 'binary preparation linear bit bill') + for Q in (1,2,4,6): + bank = [({},0) for _ in range(19)] + bank[5] = i.binary(Q,0) + expect_reject(lambda: i.execute(preparation,bank,10000), 'invalid half modulus') + return dict(complete_half_calls=total, descriptor_cases=107, transcript_sha256=digest.hexdigest(), + program_instructions=len(half_program(modules).instructions), + preparation_instructions=len(half_descriptor(modules).instructions)) + + def expect_reject(fn, text): try: fn() @@ -139,6 +189,19 @@ def controls(modules, saved, contents): tapes, steps = i.execute(saved['True'], bank, 100000) expect_reject(lambda: i.check_result(tapes, steps, bank, shape, c, h, payload), 'wrong orientation') checks.append('wrong_orientation') + for wrong_c, wrong_h, name in ((0, h, 'lost_coefficient'), (c, 0, 'lost_offset')): + wrong_bank = i.fixtures(shape, wrong_c, wrong_h, payload) + wrong_tapes, wrong_steps = i.execute(base, wrong_bank, 100000) + expect_reject(lambda: i.check_result(wrong_tapes, wrong_steps, wrong_bank, + shape, c, h, payload), name) + checks.append(name) + bad = json.loads(json.dumps(base)) + write = next(k for k, row in enumerate(bad['instructions']) if row == ['write', 1, i.ONE]) + bad['instructions'][write][2] = i.ZERO + bad_tapes, bad_steps = i.execute(bad, bank, 100000) + expect_reject(lambda: i.check_result(bad_tapes, bad_steps, bank, shape, c, h, payload), + 'corrupted emitted payload') + checks.append('payload_flip') for t, symbol in ((2, i.ONE), (17, i.LEFT)): tapes, steps = i.execute(base, bank, 100000) tapes[t].write(symbol) @@ -169,6 +232,8 @@ def main(): contents = authenticate() modules = load_macros(contents) tables = {str(inv): export(build_program(modules, inv)) for inv in (False, True)} + tables.update({'half_' + str(inv): export(half_program(modules, inv)) for inv in (False, True)}) + tables['half_descriptor'] = export(half_descriptor(modules)) table_path = HERE / 'TABLE.json.gz' if args.write: table_path.write_bytes(gzip.compress(canonical(tables), mtime=0)) @@ -176,7 +241,7 @@ def main(): need(saved == tables, 'complete table export') result = dict(schema_version=1, binding=source_binding(contents), physical=physical(modules, 'independent' if args.mode == 'controls' else args.mode, saved), - controls=controls(modules, saved, contents)) + controls=controls(modules, saved, contents), half=half_checks(modules)) receipt = HERE / 'RESULT.json' if args.write: receipt.write_text(json.dumps(result, indent=2, sort_keys=True)+'\n') From 39f3cf9fb4f2e495a716c7b501ea3bceb6b2a748 Mon Sep 17 00:00:00 2001 From: JoyboyBrian <122925040+JoyboyBrian@users.noreply.github.com> Date: Thu, 22 Oct 2026 23:23:42 -0700 Subject: [PATCH 3/3] Strengthen discriminating controls and register reproducible affine kernel package --- research/fixed-tape-affine-shear/README.md | 134 ++++++++++++++++++ research/fixed-tape-affine-shear/RESULT.json | 3 + research/fixed-tape-affine-shear/SOURCES.json | 15 +- research/fixed-tape-affine-shear/TASK.json | 108 ++++++++++++++ research/fixed-tape-affine-shear/VERIFY.json | 70 +++++++++ research/fixed-tape-affine-shear/verify.py | 8 +- 6 files changed, 334 insertions(+), 4 deletions(-) create mode 100644 research/fixed-tape-affine-shear/README.md create mode 100644 research/fixed-tape-affine-shear/TASK.json create mode 100644 research/fixed-tape-affine-shear/VERIFY.json diff --git a/research/fixed-tape-affine-shear/README.md b/research/fixed-tape-affine-shear/README.md new file mode 100644 index 0000000000..7859c3a3ca --- /dev/null +++ b/research/fixed-tape-affine-shear/README.md @@ -0,0 +1,134 @@ +# Runtime affine shear on nineteen literal tapes + +One fixed finite program realizes + +``` +(p,x,g,y,z) -> (p,x,g,y+c*x+C mod Q,z) +``` + +and its inverse for **all** positive binary-encoded `P,Q,G,S`, `0<=c,C true`; every original exported byte is restored. A +separate read-only AI peer independently recounted the transfer/comparison, +phase, cleanup, space and half-preparation ledgers and found no blocker. +This is not independent human or scientific acceptance. + +## Open next questions + +1. Bind one complete actual route's source/output banks and source retirement, + including shared scratch lifetimes. This is needed to install the kernel; + full physical ownership and native/ROW protocols remain the blocker. +2. Physically lower one actual unit_scale or reversed-field primitive, with its + full all-width tape bill. The current program does not cover those positive + costs. Begin with the source coefficient and explicit owner/tape contract, + rather than extending this same coefficient grid. + +[TASK.json](TASK.json) records the refined card and structured questions. +Canonical [claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/4945#discussioncomment-19139354). +Base: canonical main `bee95ce88f9f19802f0613f92838895cd0e14a1f`, priority7. +Entry overlap covered310open PRs (06:05:59UTC),4096Discussion records +(06:06:48UTC) and all6690tracked local notes on October23,2026. These cached +metadata searches do not cover arbitrary diffs or unpublished work and are not +a novelty certificate. + +## Credit + +David Arias / PR2776 supplied the finite machine, counters and copy/erase macros; +Charles Bethin supplied the unit-carry successor and explicit open carry +question. Jose Manuel and the retained upstream authors supplied the selected +stream reduction and ordered-affine method. ai-nanachi #4760/#4814/#4326, +Chris R / Clear1nsight #4957, JoyboyBrian #4989 and the retained native, +ROW/ordinary/stock/routing/precision/tape lineage supply the source boundary. +All predecessor files remain unchanged. New runtime controller, literal half +preparation, linked owned cleanup, proof and checks prepared by JoyboyBrian +with substantial OpenAI Codex assistance. Apache-2.0. No independent human or +proof-kernel acceptance is claimed. diff --git a/research/fixed-tape-affine-shear/RESULT.json b/research/fixed-tape-affine-shear/RESULT.json index 7af71ddbce..2b0c2cb235 100644 --- a/research/fixed-tape-affine-shear/RESULT.json +++ b/research/fixed-tape-affine-shear/RESULT.json @@ -20,6 +20,9 @@ "occupied_scratch", "nonlocal_move", "wrong_orientation", + "lost_coefficient", + "lost_offset", + "payload_flip", "retained_scratch_2", "retained_scratch_17", "source_hash", diff --git a/research/fixed-tape-affine-shear/SOURCES.json b/research/fixed-tape-affine-shear/SOURCES.json index 51f0898f47..6433257ad8 100644 --- a/research/fixed-tape-affine-shear/SOURCES.json +++ b/research/fixed-tape-affine-shear/SOURCES.json @@ -70,6 +70,19 @@ "commit": "bee95ce88f9f19802f0613f92838895cd0e14a1f", "sha256": "10b68232a7b642e7746393b505326fbf6832e7d64c1e0ddc3858835ae74283f9", "git_blob": "90f79f9d7e7bf57d392ca51232596809d51fc0a8" + }, + { + "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" } - ] + ], + "base_commit": "bee95ce88f9f19802f0613f92838895cd0e14a1f" } diff --git a/research/fixed-tape-affine-shear/TASK.json b/research/fixed-tape-affine-shear/TASK.json new file mode 100644 index 0000000000..35047275e4 --- /dev/null +++ b/research/fixed-tape-affine-shear/TASK.json @@ -0,0 +1,108 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "bee95ce88f9f19802f0613f92838895cd0e14a1f", + "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 all-size fixed-tape affine shear with runtime coefficients and offsets, with complete preparation/erasure of the actual PR4989 coefficient-1/2 later-target leaf", + "scope_change_reason": "PR4989 supplies source-bound addressed scheduling but leaves physical ordered-shift leaves conditional. PR2776 and unit-carry predecessors cover fixed coefficients, not the growing (Q+1)/2 runtime multiplier of the actual source leaf.", + "bottleneck_link": "Pays one actual later-target source primitive in uniform linear complete-payload time, replacing host scalar control by a fixed finite program. No full route or supplier admission follows.", + "budget_minutes": 60, + "stop_rule": "Stop at this named physical leaf and quantified full resource proof. No full native/ROW matcher expansion or extra coefficient census.", + "outcome": "completed", + "evidence": "877 microinstructions per generic direction,19tapes,7symbols;610 exact direction fixtures/38850bits agree in separate sparse/dense interpreters; literal half preparation, owned erasure and rejection controls pass. Written induction proves 1024V/64V bounds.", + "author": "JoyboyBrian", + "ai_assistance": "Substantial OpenAI Codex assistance, including a separate read-only AI peer review of the finite control, all-size transition/space ledgers, half-descriptor preparation/cleanup and actual source binding. No independent human or proof-kernel acceptance.", + "open_questions": [ + { + "question": "Can one complete source route install the separately owned output without a bank-lifetime conflict?", + "why_it_matters": "A physical leaf does not implement the whole recursive ownership protocol.", + "first_step": "Bind one actual parent source/output pair and include source retirement and shared scratch lifetimes.", + "blocked_by": "The whole native/ROW/owner bank has not been physically installed." + }, + { + "question": "Can the remaining source unit_scale and reversed-field leaves be physically completed?", + "why_it_matters": "The current primitive only addresses a later target; the whole matcher needs the other positive-count leaves.", + "first_step": "Choose one actual source coefficient and state its complete all-width tape contract and budget.", + "blocked_by": "Those physical programs, native calls and full P3 recurrence/precision/stock remain unimplemented here." + } + ], + "canonical_claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/4945#discussioncomment-19139354", + "scientific_claim": "One physical kernel and source-half leaf, not complete P3 admission or a new kappa", + "overlap": { + "local": { + "head": "bee95ce88f9f19802f0613f92838895cd0e14a1f", + "records": 6690, + "head_records": 6690, + "complete_head_inventory": true, + "unsearched_head_paths": [] + }, + "open_prs": { + "fetched_at": "2026-10-23T06:05:59.324278+00:00", + "complete_pagination": true, + "records": 310 + }, + "discussions": { + "fetched_at": "2026-10-23T06:06:48.270801+00:00", + "complete_pagination": true, + "records": 4096 + } + }, + "validation": { + "environment": "CPython3.12.2 / macOS27.0 arm64", + "registered_modes": "normal and optimized sparse/dense: all four pass", + "committed_source_history": "21files, basebee95 ancestral: pass", + "export": "Official committed export integrity and all four Git-free direct modes pass; actual exported source/table/typed-receipt mutations reject and all bytes restored", + "peer_review": "Separate AI peer independently recounted transfer/compare/trim/phase/cleanup and visited-space bounds; no blocker; code and PROOF reviewed at d4c93b352" + } +} diff --git a/research/fixed-tape-affine-shear/VERIFY.json b/research/fixed-tape-affine-shear/VERIFY.json new file mode 100644 index 0000000000..d352f61145 --- /dev/null +++ b/research/fixed-tape-affine-shear/VERIFY.json @@ -0,0 +1,70 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/fixed-tape-ordered-shear/machine.py", + "research/fixed-tape-ordered-shear/counters.py", + "research/fixed-tape-ordered-shear/shear.py", + "research/fixed-tape-ordered-shear/PROOF.md", + "research/fixed-tape-unit-carry/carry.py", + "research/fixed-tape-unit-carry/README.md", + "research/bit-row-route-generator/generator.py", + "research/bit-row-route-generator/PROGRAM.json.gz", + "research/bit-row-route-generator/PROOF.md", + "research/bit-row-route-generator/interpreter.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py", + "--mode", + "primary" + ], + "timeout_seconds": 120, + "checks": "Complete source/table/typed-receipt binding, all610direction fixtures, actual linked half preparation/erasure and semantic/physical controls in primary interpreter." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py", + "--mode", + "independent" + ], + "timeout_seconds": 120, + "checks": "Complete source/table/typed-receipt binding, all610direction fixtures, actual linked half preparation/erasure and semantic/physical controls in independent interpreter." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "-O", + "{package}/verify.py", + "--mode", + "primary" + ], + "timeout_seconds": 120, + "checks": "Complete source/table/typed-receipt binding, all610direction fixtures, actual linked half preparation/erasure and semantic/physical controls in primary interpreter." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "-O", + "{package}/verify.py", + "--mode", + "independent" + ], + "timeout_seconds": 120, + "checks": "Complete source/table/typed-receipt binding, all610direction fixtures, actual linked half preparation/erasure and semantic/physical controls in independent interpreter." + } + ] +} diff --git a/research/fixed-tape-affine-shear/verify.py b/research/fixed-tape-affine-shear/verify.py index c18760c82a..67ba50ae64 100644 --- a/research/fixed-tape-affine-shear/verify.py +++ b/research/fixed-tape-affine-shear/verify.py @@ -165,7 +165,7 @@ def expect_reject(fn, text): def controls(modules, saved, contents): base = saved['False'] shape, c, h = (2, 5, 2, 2), 3, 2 - payload = [int(j == 0) for j in range(200)] + payload = [int(j == 40) for j in range(200)] checks = [] for field, value in ((4, 0), (5, 0), (6, 0), (7, 0), (14, 6), (16, 6)): bank = i.fixtures(shape, c, h, payload) @@ -196,8 +196,10 @@ def controls(modules, saved, contents): shape, c, h, payload), name) checks.append(name) bad = json.loads(json.dumps(base)) - write = next(k for k, row in enumerate(bad['instructions']) if row == ['write', 1, i.ONE]) - bad['instructions'][write][2] = i.ZERO + writes = [k for k, row in enumerate(bad['instructions']) if row == ['write', 1, i.ONE]] + need(len(writes) == 2, 'both emitted bucket branches present') + for write in writes: + bad['instructions'][write][2] = i.ZERO bad_tapes, bad_steps = i.execute(bad, bank, 100000) expect_reject(lambda: i.check_result(bad_tapes, bad_steps, bank, shape, c, h, payload), 'corrupted emitted payload')