From 0d8af3eeb311e11c967cfaabfdd51af6112dd335 Mon Sep 17 00:00:00 2001 From: JoyboyBrian <122925040+JoyboyBrian@users.noreply.github.com> Date: Sat, 24 Oct 2026 21:30:33 -0700 Subject: [PATCH 1/2] Prove actual CRT offset to physical current-row query composition --- research/crt-current-row-query/PROOF.md | 226 ++++++++++++++++++++ research/crt-current-row-query/SOURCES.json | 180 ++++++++++++++++ research/crt-current-row-query/join.py | 224 +++++++++++++++++++ 3 files changed, 630 insertions(+) create mode 100644 research/crt-current-row-query/PROOF.md create mode 100644 research/crt-current-row-query/SOURCES.json create mode 100644 research/crt-current-row-query/join.py 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< Date: Sat, 24 Oct 2026 21:31:06 -0700 Subject: [PATCH 2/2] Validate physical row semantics, ownership controls, and bounded replay closure --- research/crt-current-row-query/ATTEMPT.json | 16 ++ research/crt-current-row-query/README.md | 68 ++++++++ research/crt-current-row-query/RESULT.json | 183 ++++++++++++++++++++ research/crt-current-row-query/TASK.json | 80 +++++++++ research/crt-current-row-query/VERIFY.json | 62 +++++++ research/crt-current-row-query/verify.py | 129 ++++++++++++++ 6 files changed, 538 insertions(+) create mode 100644 research/crt-current-row-query/ATTEMPT.json create mode 100644 research/crt-current-row-query/README.md create mode 100644 research/crt-current-row-query/RESULT.json create mode 100644 research/crt-current-row-query/TASK.json create mode 100644 research/crt-current-row-query/VERIFY.json create mode 100644 research/crt-current-row-query/verify.py 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/README.md b/research/crt-current-row-query/README.md new file mode 100644 index 0000000000..f5c66d745a --- /dev/null +++ b/research/crt-current-row-query/README.md @@ -0,0 +1,68 @@ +# Actual CRT offsets to a physical current-row query + +The sequential numerical result of Ali Romman's PR5353 now feeds the +unchanged PR5092 encoded Beneš ROM producer. The join reads the produced +ROM on its original backing, selects the current padded coordinate with +an encoded countdown, and returns the actual micro-row coordinate stream. +It pays for serialization, queries, rewinds and disposal of both the +selected ROM and the unused complete-layer output. + +[PROOF.md](PROOF.md) gives the source-relative quantified interface theorem, +admission W=P, current-coordinate convention, complete local time bound +and retained-backing bound. [RESULT.json](RESULT.json) records the small +actual producer/query cases and four falsifying controls. The h=2 checks +exercise the complete encoded producer, not a verifier-supplied row table. + +```sh +python3.12 -B scripts/research_package.py --package research/crt-current-row-query +``` + +The registered normal and optimized runs authenticate every source input +and compare typed deterministic receipts. The separate, expensive h=4 +four-axis test is explicitly opt-in: + +```sh +python3.12 -B research/crt-current-row-query/verify.py --four-axis +``` + +This optional whole-ROM test is distinct from the small executed h=2 ABI +checks. The author attempt exceeded180seconds without completion; no +ACTUAL4 receipt exists and no h=4 joined result is claimed. See +[ATTEMPT.json](ATTEMPT.json) for exact attempted bytes and the subsequent +all-size repairs. A future completed optional run checks the caller and +invoices even without a frozen receipt; `--write-result` records one. + +The small mixed-width case reaches padded coordinate3 before its last +query. Suppressing that query gives the wrong endpoint. Mutating the +offset, selected row or unused-layer disposal also fails. All source and +protected words are restored; all63 numerical ports and every joined +owned backing are retired. Separate row invocations use test-harness +input serialization; no uninterrupted physical level execution is claimed. + +## Open next questions + +- Physically update the canonical axis input with the returned row stream, + so successive rows need no host serialization. +- Compose the current query into the complete three-epoch exceptional key, + paying for all original/current coordinate conversions and restorations. +- Resolve cross-session bank ownership and a complete binary numerical + lowering before claiming a global machine or outer multiplication bound. + +No new kappa, selected frontier, human acceptance or formal-kernel proof is +claimed. Source models and initial blank owned backing remain explicit +premises. This is one actual caller boundary, not full total repair. + +## Provenance and credit + +Base32890bc5de034ab8fc93ac88ead7279a6a416d04, priority7. The scope takes +PR5353's explicit physical-query handoff, Discussion4709 comment19152738; +the new claim is comment19173182. Fresh overlap covered352 open PRs and +4747 fully paginated Discussion records through2026-10-25T04:14:44Z, +plus exact local source packages. Unpublished work was not searched. +[SOURCES.json](SOURCES.json) freezes the complete input closure. + +JoyboyBrian, with substantial OpenAI Codex assistance. Apache-2.0. +Retain Ali Romman's actual RowEntry, Hiroki KUMAZAKI's mixed-width caller, +JoyboyBrian's numerical entry and ROM producer, Cinna Davis's CRT/Beneš +construction, ToikY's arena/DFS proof and all predecessor notices and +credits listed in PROOF.md. No predecessor file is modified. diff --git a/research/crt-current-row-query/RESULT.json b/research/crt-current-row-query/RESULT.json new file mode 100644 index 0000000000..35be57bdde --- /dev/null +++ b/research/crt-current-row-query/RESULT.json @@ -0,0 +1,183 @@ +{ + "status": "PASS_CURRENT_ROW_QUERY", + "sources": { + "research/crt-dense-guard-scan/machine.py": "1cb27312932914eb631078bd56e85feb1dc6c4191e9d1962b2cc3a7e1cfb8df7", + "research/crt-encoded-benes-rom-producer/PROOF.md": "93bd340ac9b77f8f781926aeb7327325789b331863b3088fed1809eefb789bd2", + "research/crt-encoded-benes-rom-producer/SOURCES.json": "527b3a3a2996c24462b7f81f0e37c86fb315f8401026f2e19e46bb5bc55bffce", + "research/crt-encoded-benes-rom-producer/microcode.py": "d4af5350854a87b67484840800b94e1e53cff82c78ec0f2a91753fed9ea70af7", + "research/crt-encoded-benes-rom-producer/vendor/pr4192-NOTICE.md": "b886589be7c8b87bcf12b14ce4db6827299b7cec93836ed22cff81aed37623dc", + "research/crt-encoded-benes-rom-producer/vendor/pr4192-PROOF.md": "c3eb4e14dc5ee0102cbf77c4a0e61db9989c2b8a0eaf7f0659a6e39373197474", + "research/crt-encoded-benes-rom-producer/vendor/pr4192-verify.py": "e8ff7800ffa267d2825009656b78ab1613544b55301982744ec0d99f38800913", + "research/crt-mask-repair-bridge/key_subroutine.py": "ffdbb610be71ae20bf974946dac66b6c1b4d43739cbc3b1eb81cbbeab8784b44", + "research/crt-mixed-row-entry/PROOF.md": "8a529ece497c62d5225261cdacebfd88979322b3a8886d1a31eb6295f1989e4b", + "research/crt-mixed-row-entry/SOURCES.json": "aac37dac580b1c3b3b4b53220b76292519d3188da0384a728270b02119ea7d80", + "research/crt-mixed-row-entry/bridge.py": "89c38638c0d66da731566c903c32e7fa1ad31088d29cfd2634fce823dd07c1f9", + "research/crt-mixed-row-entry/verify.py": "b8695e19bbd597b61dd97379f3970b62f375719a10512dea77784e2ce3b71f2d", + "research/crt-mixed-width-caller/README.md": "c5126d2e1f381fe5a34b8e3350799ac4c3a58fe2def590b12ad4354da7b01ebf", + "research/crt-mixed-width-caller/verify.py": "5e62787f3c4a8f1175ca7dea6c6b8ceff7863a3f879abd6245faf6aeb272fd45", + "research/crt-paid-key-service/PROOF.md": "1a4ac02653eb6c1b20807033a910f27bf9484cc972bf2629941f589275a87325", + "research/crt-paid-key-service/service.py": "ff06c6305c9f650a694e5c42baa4c7d841decf844a4f44f6776acc10a8400083", + "research/crt-paid-key-service/verify.py": "fb02e2792cb07c52367c0a8c7087d54958bdf55214e51bc02f4e68dbf95547b1", + "research/crt-uniform-rom-query/PROOF.md": "736be5e1af590f2195e8b56b958258f0babe5cd6d2cf6f4f5023410112f4d870", + "research/crt-uniform-rom-query/machine.py": "46ee6a635251e498ee9a5d4aff8c0e2a7f1ef2ff951e5b6a2a8953316e9cd02d", + "research/encoded-crt-entry-lifecycle/PROOF.md": "a619be48c8c85749ea5411929aa6ff3986443b467133d32d19d543250b0054b0", + "research/encoded-crt-entry-lifecycle/entry.py": "0537ec98f306270c8ff6a424841886cf53f675d9947029347090c7dc779616d7", + "research/encoded-current-crt/PROOF.md": "7da614e737414a373c8716158f2c02a52666620ea1f114fac7ca09b3b38489bc", + "research/encoded-current-crt/producer.py": "88dab4ca02a92164a67826db361214fa1405e4b4a588f8c4279a21bcee95ab76", + "research/r437-preparation-composition/predecessor4025/source/records.py": "0c9c4b23e998597fb877bb1a29da69ac869b68262abe635b162b4dba9c69b372", + "research/r437-preparation-composition/predecessor4025/source/words.py": "5c37f57708ba3131bdcb03139f9dbc29886bee44569c09cbba51b68f75acd7f9", + "research/unconditional-batched-crt/NOTICE.md": "924109837e71c52392191710d49c9deb42780878d1094f0b01e8690dbe799461", + "research/unconditional-batched-crt/check_batched_crt.py": "681e2e3d71fa74c8b9b326f3860104fd9d89590a222e26ae6ee718d1fd40ff2e" + }, + "cases": [ + { + "idle": false, + "moduli": [ + 7, + 3 + ], + "widths": [ + 3, + 2 + ], + "state": [ + 1, + 1 + ], + "level": 1, + "start": 0, + "row": 0, + "precision": 6, + "output": [ + 1 + ], + "producer_calls": 1, + "producer_instructions": 2776926, + "adapter_tape_actions": 579, + "entry_and_numeric_tape_actions": 44309, + "producer_retained_cells": 1744, + "new_retained_cells": 46, + "entry_retained_cells": 536, + "distinct_owned_cells": 2293, + "time_bound": 733299510016, + "storage_bound": 2911 + }, + { + "idle": false, + "moduli": [ + 7, + 3 + ], + "widths": [ + 3, + 2 + ], + "state": [ + 1, + 1 + ], + "level": 1, + "start": 0, + "row": 1, + "precision": 6, + "output": [ + 3 + ], + "producer_calls": 1, + "producer_instructions": 2776927, + "adapter_tape_actions": 582, + "entry_and_numeric_tape_actions": 44309, + "producer_retained_cells": 1744, + "new_retained_cells": 46, + "entry_retained_cells": 536, + "distinct_owned_cells": 2293, + "time_bound": 733299510016, + "storage_bound": 2911 + }, + { + "idle": true, + "row": 2, + "producer_instructions": 0 + }, + { + "idle": true, + "row": 3, + "producer_instructions": 0 + }, + { + "idle": false, + "moduli": [ + 7, + 3 + ], + "widths": [ + 3, + 2 + ], + "state": [ + 1, + 3 + ], + "level": 1, + "start": 0, + "row": 4, + "precision": 6, + "output": [ + 2 + ], + "producer_calls": 1, + "producer_instructions": 2776927, + "adapter_tape_actions": 627, + "entry_and_numeric_tape_actions": 42297, + "producer_retained_cells": 1744, + "new_retained_cells": 46, + "entry_retained_cells": 537, + "distinct_owned_cells": 2294, + "time_bound": 733299510016, + "storage_bound": 2911 + }, + { + "idle": false, + "moduli": [ + 7, + 3 + ], + "widths": [ + 3, + 2 + ], + "state": [ + 7, + 1 + ], + "level": 1, + "start": 0, + "row": 1, + "precision": 6, + "output": [ + 1 + ], + "producer_calls": 1, + "producer_instructions": 2776287, + "adapter_tape_actions": 582, + "entry_and_numeric_tape_actions": 44429, + "producer_retained_cells": 1744, + "new_retained_cells": 46, + "entry_retained_cells": 538, + "distinct_owned_cells": 2295, + "time_bound": 733299510016, + "storage_bound": 2911 + } + ], + "controls": [ + "zero_offset", + "wrong_local_row", + "suppress_query", + "omit_layers_disposal" + ], + "join_sha256": "11c9ac1175a45edae80869b22c041e31a1b5cc75f4389ec2e073de37e547bf35", + "level_endpoint": [ + 1, + 2 + ] +} diff --git a/research/crt-current-row-query/TASK.json b/research/crt-current-row-query/TASK.json new file mode 100644 index 0000000000..d7cc335aae --- /dev/null +++ b/research/crt-current-row-query/TASK.json @@ -0,0 +1,80 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Prove one missing implication with explicit quantified hypotheses.", + "Find an exact counterexample at the claimed interface boundary." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": [ + "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller." + ], + "scope_change_triggers": [ + "Replacing a quantified obligation with another finite smoke test.", + "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses." + ], + "overlap_terms": [ + "uniform transfer", + "all-size", + "precision", + "4100", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "refined", + "actual_scope": "Connect the actual current numerical offset stream to the unchanged encoded Bene\u0161 ROM producer and a physical current-coordinate micro-row query, with complete local retirement and invoice.", + "scope_change_reason": "PR5353 explicitly leaves physical row-key querying open after producing numerical offset records; PR5092 already supplies the encoded ROM engine.", + "bottleneck_link": "Logical caller agreement does not supply the physical encoded-output to ROM/query boundary.", + "budget_minutes": 60, + "stop_rule": "One source-relative quantified interface theorem and bounded actual callers; no full three-epoch key or outer theorem.", + "outcome": "completed", + "evidence": "PROOF.md, join.py, verify.py, RESULT.json and optional ACTUAL4.json", + "author": "JoyboyBrian", + "ai_assistance": "Substantial OpenAI Codex assistance in proof, implementation, review and verification. No independent human or proof-kernel acceptance claimed.", + "open_questions": [ + { + "question": "Can the returned row stream become the next row input without host serialization?", + "why_it_matters": "The current finite level sequence uses separately supplied canonical input tapes.", + "first_step": "Implement paid in-place axis stream update and preserve the protected numeric bank.", + "blocked_by": "Sequential full-level stream ownership remains external." + }, + { + "question": "Can this query be composed into the full three-epoch exceptional key?", + "why_it_matters": "One current row does not implement inverse/row/forward key transport.", + "first_step": "Bind original/current epochs and all restoration to the existing key caller.", + "blocked_by": "Multi-epoch physical context and complete total repair remain separate." + } + ] +} diff --git a/research/crt-current-row-query/VERIFY.json b/research/crt-current-row-query/VERIFY.json new file mode 100644 index 0000000000..77e4c4d41d --- /dev/null +++ b/research/crt-current-row-query/VERIFY.json @@ -0,0 +1,62 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/crt-dense-guard-scan/machine.py", + "research/crt-encoded-benes-rom-producer/PROOF.md", + "research/crt-encoded-benes-rom-producer/SOURCES.json", + "research/crt-encoded-benes-rom-producer/microcode.py", + "research/crt-encoded-benes-rom-producer/vendor/pr4192-NOTICE.md", + "research/crt-encoded-benes-rom-producer/vendor/pr4192-PROOF.md", + "research/crt-encoded-benes-rom-producer/vendor/pr4192-verify.py", + "research/crt-mask-repair-bridge/key_subroutine.py", + "research/crt-mixed-row-entry/PROOF.md", + "research/crt-mixed-row-entry/SOURCES.json", + "research/crt-mixed-row-entry/bridge.py", + "research/crt-mixed-row-entry/verify.py", + "research/crt-mixed-width-caller/README.md", + "research/crt-mixed-width-caller/verify.py", + "research/crt-paid-key-service/PROOF.md", + "research/crt-paid-key-service/service.py", + "research/crt-paid-key-service/verify.py", + "research/crt-uniform-rom-query/PROOF.md", + "research/crt-uniform-rom-query/machine.py", + "research/encoded-crt-entry-lifecycle/PROOF.md", + "research/encoded-crt-entry-lifecycle/entry.py", + "research/encoded-current-crt/PROOF.md", + "research/encoded-current-crt/producer.py", + "research/r437-preparation-composition/predecessor4025/source/records.py", + "research/r437-preparation-composition/predecessor4025/source/words.py", + "research/unconditional-batched-crt/NOTICE.md", + "research/unconditional-batched-crt/check_batched_crt.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Small actual numerical-output to encoded ROM/query cases, padded-coordinate semantics, complete retirement, four falsifying controls, exact source and typed receipt checks. The optional h4 four-axis replay is separately budgeted." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Small actual numerical-output to encoded ROM/query cases, padded-coordinate semantics, complete retirement, four falsifying controls, exact source and typed receipt checks. The optional h4 four-axis replay is separately budgeted." + } + ] +} diff --git a/research/crt-current-row-query/verify.py b/research/crt-current-row-query/verify.py new file mode 100644 index 0000000000..0d286b9a24 --- /dev/null +++ b/research/crt-current-row-query/verify.py @@ -0,0 +1,129 @@ +"""Actual current-row comparison and paid ownership controls; source-bound.""" +from hashlib import sha256 +import argparse +import json +from pathlib import Path +import sys +import types + +P=Path(__file__).resolve().parent +ROOT=P.parents[1] + + +def need(ok,why): + if not ok:raise ValueError(why) + + +def load(name,path): + module=types.ModuleType(name);module.__file__=str(path);sys.modules[name]=module + exec(compile(path.read_bytes(),str(path),'exec'),module.__dict__) + return module + + +def authenticate(): + sources={} + for row in json.loads((P/'SOURCES.json').read_text())['files']: + if row['usage']=='input': + digest=sha256((ROOT/row['path']).read_bytes()).hexdigest() + need(digest==row['sha256'],'source SHA256 '+row['path']);sources[row['path']]=digest + return sources + + +def modules(): + original=load('row_fixture',ROOT/'research/crt-mixed-row-entry/verify.py') + rom=load('rom_producer',ROOT/'research/crt-encoded-benes-rom-producer/microcode.py') + return original,original.modules(),rom,load('row_join',P/'join.py'),rom.producer_program() + + +def case(mod,moduli,widths,ell,state,level,start,row,fault=None): + helper,old,rom,join,program=mod;w,r,e,numeric,caller_module,crt,row_module=old + precision=1+sum(widths[start:start+(1<