diff --git a/research/crt-current-row-query/ATTEMPT.json b/research/crt-current-row-query/ATTEMPT.json new file mode 100644 index 0000000000..386fcf1b37 --- /dev/null +++ b/research/crt-current-row-query/ATTEMPT.json @@ -0,0 +1,16 @@ +{ + "status": "INCOMPLETE_RESOURCE_TIMEOUT", + "command": "/opt/local/bin/python3.12 -B research/crt-current-row-query/verify.py --four-axis --write-result", + "elapsed_limit_seconds": 180, + "exit_code": 1, + "completed_receipt": false, + "join_sha256": "bcae8074a67fe74ee9979a4608452de6e2decbe7023671624573f362f3caefe5", + "verify_sha256": "e0ba8c478eb5054e7f83be1840c42f99472e012e67cc2edf527c84589f80e9bf", + "case": "moduli5,7,11,13 widths3,3,4,4 current1,5,0,9 level2 row0 P15; two h4 complete producers", + "observation": "No completed producer/query result was emitted before the subprocess timeout killed the child. No progress count or passing h4 result is claimed.", + "subsequent_repairs": [ + "Replace linear active tuple membership with the equivalent constant-time compiled width/node/row predicate.", + "Replace fixed2e9 watchdog with the proved T_rom bound computed from compiled P and h." + ], + "evidence_scope": "The final implementation is tested on the complete h2 actual pipeline. This timeout is not acceptance evidence for either version." +} diff --git a/research/crt-current-row-query/PROOF.md b/research/crt-current-row-query/PROOF.md new file mode 100644 index 0000000000..0449d47c50 --- /dev/null +++ b/research/crt-current-row-query/PROOF.md @@ -0,0 +1,226 @@ +# Current numerical offsets to a physical CRT micro-row + +JoyboyBrian, with substantial OpenAI Codex assistance. Apache-2.0. + +## The exact boundary + +Use the admitted `RowEntry` domain of Ali Romman's PR5353: a power-of-two +axis count d, declared h_i in {ell-1,ell}, ell>=2, pairwise coprime moduli +2<=s_i<2^h_i, arbitrary padded current coordinates 0<=x_i<2^h_i, one +compiled tree node [a,a+n) and one global row. The source is its literal +sequential padded-axis tape, not a host list of numeric values. Eight +distinct protected numerical words are supplied with the retained legal +heads. Fixed topology, input ownership and the source numerical-operation +model remain predecessor premises. + +Let b=a+n/2, P=1+sum_{i=a}^{a+n-1}h_i, and A be the non-idle right axes +of this global row. The result is an owned stream containing, in axis +order, the h_i bits of the **micro-row output** for every right axis +b<=i=h_i+3. A node has at least two +axes, and every modulus is at least two, hence every admitted h_j>=2. +Consequently P>=h_i+2+1=h_i+3. Taking W=P meets its width contract; its +modulus and singleton-offset guards follow from the numerical theorem. +The local row is g for a long axis, and g or g-2 on the two active pieces +of a short axis, with global rows ell-1 and ell idle. This is exactly the +pinned `local_row` function, and lies in [0,2h_i-2]. + +Thus the unchanged encoded producer emits the exact canonical Beneš +network for the rotation x->x+c_i mod s_i on x existing ROM -> physical row query. +JoyboyBrian, with substantial OpenAI Codex assistance. Apache-2.0. +Topology is compiled data; runtime numeric values are never decoded. +""" + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +class Tape: + def __init__(self, cells=None): + self.cells = ['_'] if cells is None else cells + self.head = 0 + self.actions = 0 + + def read(self): + self.actions += 1 + return self.cells[self.head] + + def write(self, value): + need(value in ('_', 'L', 'R', '|', '0', '1'), 'fixed symbol') + self.actions += 1 + self.cells[self.head] = value + + def step(self, direction): + need(direction in (-1, 1) and self.head+direction >= 0, 'unit move') + self.actions += 1 + self.head += direction + if self.head == len(self.cells): + self.cells.append('_') + + def emit(self, value): + self.write(value) + self.step(1) + + def rewind(self): + while self.read() != 'L': + self.step(-1) + + def erase(self): + self.rewind() + self.step(1) + while self.read() != 'R': + self.write('_'); self.step(1) + self.write('_'); self.rewind(); self.write('_') + + +def padded_constant(target, bits, guide, w): + target.emit('L') + for bit in bits: # A compile-time constant, never an encoded input integer. + need(guide.read() == w.ONE, 'constant fits encoded width') + target.emit('1' if bit else '0'); guide.step(1) + while guide.read() == w.ONE: + target.emit('0'); guide.step(1) + need(guide.read() == w.BLANK, 'guide terminator') + target.write('R'); target.rewind(); guide.rewind() + + +def copy_numeric_field(source, target, guide, w, delimiter, suffix='R'): + target.emit('L') + while guide.read() == w.ONE: + bit = source.read() + need(bit in (w.ZERO, w.ONE), 'numeric field bit') + target.emit('1' if bit == w.ONE else '0') + source.step(1); guide.step(1) + need(source.read() == delimiter and guide.read() == w.BLANK, 'exact P-bit field') + source.step(1); guide.rewind() + if suffix == '|': + target.emit('|') + target.write('R'); target.rewind() + + +def skip_numeric_field(source, guide, w, delimiter): + while guide.read() == w.ONE: + need(source.read() in (w.ZERO, w.ONE), 'skipped numeric bit') + source.step(1); guide.step(1) + need(source.read() == delimiter and guide.read() == w.BLANK, 'skipped exact width') + source.step(1); guide.rewind() + + +def select_row_bit(rom, countdown, fault=None): + """Scan the produced row; index is an encoded countdown, not a host cursor.""" + enabled, answer, seen = True, '0', False + rom.step(1) + while rom.read() != 'R': + value = rom.read(); need(value in ('0', '1'), 'ROM row bit') + if enabled: + zero = True + countdown.step(1) + while countdown.read() != 'R': + zero = zero and countdown.read() == '0' + countdown.step(1) + countdown.rewind() + if zero: + answer, seen, enabled = value, True, False + else: + countdown.step(1) + while countdown.read() == '0': + countdown.write('1'); countdown.step(1) + need(countdown.read() == '1', 'countdown underflow') + countdown.write('0'); countdown.rewind() + rom.step(1) + need(seen, 'current coordinate outside complete row') + rom.rewind(); countdown.erase() + return '0' if fault == 'suppress_query' else answer + + +class RowQuery: + def __init__(self, w, records, entry_module, numeric, row_module, rom_module, + program, source, dirty, widths, ell, level, start, row, fault=None): + self.w, self.records, self.source = w, records, source + self.fault = fault + self.entry = row_module.RowEntry(w, records, entry_module, numeric, + source, dirty, widths, ell, level, start, row) + self.output = None + self.ports = [] + self.service = None + self.producer_steps = 0 + self.invocations = 0 + self.closed = False + if not self.entry.active: + return + # All variable-width initialization is driven by the existing unary guide. + guide = self.entry.guide + names = ('h', 'modulus', 'selected_layer', 'offsets') + headers = {name: Tape() for name in names} + coordinate, countdown, output = Tape(), Tape(), Tape() + self.ports = [*headers.values(), coordinate, countdown, output] + self.output = output + output.emit('L') + self.program = program + self.service = {name: ['_'] for name in rom_module.REGS+('arena','spool','layers','rom')} + self.service.update({name: headers[name].cells for name in names}) + self.produced_rom = Tape(self.service['rom']) + self.produced_layers = Tape(self.service['layers']) + self.ports.extend((self.produced_rom, self.produced_layers)) + result = self.entry.result['stream'] + size = 1 << level + middle, stop = start+size//2, start+size + precision = 1 + sum(widths[start:stop]) # Compiled topology only. + for axis, h in enumerate(widths): + chosen = middle <= axis < stop + active = chosen and (h == ell or row not in (ell-1, ell)) + need(source.read() == records.ROOT, 'axis tag'); source.step(1) + for _ in range(h): + need(source.read() == w.ONE, 'compiled axis width'); source.step(1) + need(source.read() == records.WORD_END, 'width delimiter'); source.step(1) + if active: + headers['modulus'].emit('L') + for _ in range(h): + bit=source.read(); need(bit in (w.ZERO,w.ONE), 'modulus bit') + if active: + need(guide.read()==w.ONE,'modulus fits guide') + headers['modulus'].emit('1' if bit==w.ONE else '0');guide.step(1) + source.step(1) + if active: + while guide.read()==w.ONE: + headers['modulus'].emit('0');guide.step(1) + need(guide.read()==w.BLANK,'guide end');guide.rewind() + headers['modulus'].write('R');headers['modulus'].rewind() + need(source.read()==records.WORD_END,'modulus delimiter');source.step(1) + if chosen: + coordinate.emit('L') + if active:countdown.emit('L') + for _ in range(h): + bit=source.read();need(bit in (w.ZERO,w.ONE),'coordinate bit') + if chosen: + symbol='1' if bit==w.ONE else '0';coordinate.emit(symbol) + if active:countdown.emit(symbol) + source.step(1) + need(source.read()==records.RECORD_END,'axis end');source.step(1) + if not chosen: + continue + coordinate.write('R');coordinate.rewind() + need(result.read()==records.ROOT,'offset record');result.step(1) + if active: + countdown.write('R');countdown.rewind() + local=row if h==ell or row>j)&1 for j in range(h.bit_length())) + rowbits=tuple((selected>>j)&1 for j in range(max(1,selected.bit_length()))) + padded_constant(headers['h'],hbits,guide,w) + padded_constant(headers['selected_layer'],rowbits,guide,w) + copy_numeric_field(result,headers['offsets'],guide,w,records.WORD_END,'|') + if fault=='zero_offset': + tape=headers['offsets'];tape.step(1) + while tape.read()!='|':tape.write('0');tape.step(1) + tape.rewind() + # Proven producer bound, compiled from topology, not input values. + budget=2*10**6*precision**2*((1<