From 4f49743a9df0cf7501cdc62bd5707a122fa071e9 Mon Sep 17 00:00:00 2001 From: ToikY <27568617+ToikY@users.noreply.github.com> Date: Tue, 20 Oct 2026 06:45:03 -0700 Subject: [PATCH] Lower admitted-stencil CRT guard scan to a literal three-tape program --- .../COST-CHECK-RESULT.json | 181 ++++++++ .../crt-dense-guard-scan/CROSS-REPLAY.json | 135 ++++++ research/crt-dense-guard-scan/EVIDENCE.md | 46 ++ .../INDEPENDENT-COST-REVIEW.md | 158 +++++++ .../crt-dense-guard-scan/INITIAL-REVIEW.json | 408 ++++++++++++++++++ .../crt-dense-guard-scan/INITIAL-REVIEW.md | 89 ++++ .../crt-dense-guard-scan/PRIMARY-REVIEW.json | 61 +++ .../crt-dense-guard-scan/PRIMARY-REVIEW.md | 77 ++++ research/crt-dense-guard-scan/PROOF.md | 181 ++++++++ research/crt-dense-guard-scan/README.md | 70 +++ research/crt-dense-guard-scan/REPORT.json | 133 ++++++ research/crt-dense-guard-scan/RESULT.json | 179 ++++++++ .../crt-dense-guard-scan/SOURCE-PINS.json | 20 + research/crt-dense-guard-scan/SOURCES.json | 36 ++ research/crt-dense-guard-scan/TASK.json | 122 ++++++ research/crt-dense-guard-scan/VERIFY.json | 111 +++++ research/crt-dense-guard-scan/cost_check.py | 119 +++++ research/crt-dense-guard-scan/cross_check.py | 161 +++++++ .../independent_guard_oracle.py | 179 ++++++++ research/crt-dense-guard-scan/machine.py | 169 ++++++++ research/crt-dense-guard-scan/verify.py | 226 ++++++++++ 21 files changed, 2861 insertions(+) create mode 100644 research/crt-dense-guard-scan/COST-CHECK-RESULT.json create mode 100644 research/crt-dense-guard-scan/CROSS-REPLAY.json create mode 100644 research/crt-dense-guard-scan/EVIDENCE.md create mode 100644 research/crt-dense-guard-scan/INDEPENDENT-COST-REVIEW.md create mode 100644 research/crt-dense-guard-scan/INITIAL-REVIEW.json create mode 100644 research/crt-dense-guard-scan/INITIAL-REVIEW.md create mode 100644 research/crt-dense-guard-scan/PRIMARY-REVIEW.json create mode 100644 research/crt-dense-guard-scan/PRIMARY-REVIEW.md create mode 100644 research/crt-dense-guard-scan/PROOF.md create mode 100644 research/crt-dense-guard-scan/README.md create mode 100644 research/crt-dense-guard-scan/REPORT.json create mode 100644 research/crt-dense-guard-scan/RESULT.json create mode 100644 research/crt-dense-guard-scan/SOURCE-PINS.json create mode 100644 research/crt-dense-guard-scan/SOURCES.json create mode 100644 research/crt-dense-guard-scan/TASK.json create mode 100644 research/crt-dense-guard-scan/VERIFY.json create mode 100644 research/crt-dense-guard-scan/cost_check.py create mode 100644 research/crt-dense-guard-scan/cross_check.py create mode 100644 research/crt-dense-guard-scan/independent_guard_oracle.py create mode 100644 research/crt-dense-guard-scan/machine.py create mode 100644 research/crt-dense-guard-scan/verify.py diff --git a/research/crt-dense-guard-scan/COST-CHECK-RESULT.json b/research/crt-dense-guard-scan/COST-CHECK-RESULT.json new file mode 100644 index 0000000000..b8d1d73c1a --- /dev/null +++ b/research/crt-dense-guard-scan/COST-CHECK-RESULT.json @@ -0,0 +1,181 @@ +{ + "cases": 14, + "complete_addresses": 2058, + "cost_fault_controls": [ + { + "detected_by": "independently derived read/write/move invoice", + "name": "one READ omitted from observer tariff; mask and ownership preserved" + } + ], + "kernel_sha256": "1cb27312932914eb631078bd56e85feb1dc6c4191e9d1962b2cc3a7e1cfb8df7", + "result": "PASS_INDEPENDENT_LITERAL_GUARD_COST", + "rows": [ + { + "L": 1, + "M": 2, + "actions": 77, + "mask_sha256": "f1534392279bddbf9d43dde8701cb5be14b82f76ec6607bf8d6ad557f60f304e", + "moves": 34, + "name": "all_skip", + "reads": 34, + "visited_cells": 10, + "writes": 9 + }, + { + "L": 2, + "M": 4, + "actions": 168, + "mask_sha256": "9af15b336e6a9619928537df30b2e6a2376569fcf9d7e773eccede65606529a0", + "moves": 76, + "name": "all_skip", + "reads": 75, + "visited_cells": 14, + "writes": 17 + }, + { + "L": 3, + "M": 8, + "actions": 369, + "mask_sha256": "7e071fd9b023ed8f18458a73613a0834f6220bd5cc50357ba3493c6040a9ea8c", + "moves": 170, + "name": "all_skip", + "reads": 168, + "visited_cells": 20, + "writes": 31 + }, + { + "L": 4, + "M": 16, + "actions": 822, + "mask_sha256": "fcdb4b423f4e5283afa249d762ef6aef150e91fccd810d43e5e719d14512dec7", + "moves": 384, + "name": "all_skip", + "reads": 381, + "visited_cells": 30, + "writes": 57 + }, + { + "L": 5, + "M": 32, + "actions": 1843, + "mask_sha256": "84e0c0eafaa95a34c293f278ac52e45ce537bab5e752a00e6959a13ae103b65a", + "moves": 870, + "name": "all_skip", + "reads": 866, + "visited_cells": 48, + "writes": 107 + }, + { + "L": 6, + "M": 64, + "actions": 4128, + "mask_sha256": "60e05bd1b195af2f94112fa7197a5c88289058840ce7c6df9693756bc6250f55", + "moves": 1964, + "name": "all_skip", + "reads": 1959, + "visited_cells": 82, + "writes": 205 + }, + { + "L": 7, + "M": 128, + "actions": 9197, + "mask_sha256": "45725791c47b32618cc57b88343e2bceec3b0a01b83bc97d144a2cbc11a20c3d", + "moves": 4402, + "name": "all_skip", + "reads": 4396, + "visited_cells": 148, + "writes": 399 + }, + { + "L": 8, + "M": 256, + "actions": 20346, + "mask_sha256": "67f022195ee405142968ca1b53ae2513a8bab0404d70577785316fa95218e8ba", + "moves": 9784, + "name": "all_skip", + "reads": 9777, + "visited_cells": 278, + "writes": 785 + }, + { + "L": 9, + "M": 512, + "actions": 44679, + "mask_sha256": "17ded6e69bc62c7196b1e93a4b3713243767de04ab0367fe35e18d358206c55f", + "moves": 21566, + "name": "all_skip", + "reads": 21558, + "visited_cells": 536, + "writes": 1555 + }, + { + "L": 10, + "M": 1024, + "actions": 97428, + "mask_sha256": "35ae5091b37e8f0f306833ef57a635f9dc06738d7f4e563a610eec2adb26fe28", + "moves": 47172, + "name": "all_skip", + "reads": 47163, + "visited_cells": 1050, + "writes": 3093 + }, + { + "L": 1, + "M": 2, + "actions": 77, + "mask_sha256": "938db8c9f82c8cb58d3f3ef4fd250036a48d26a712753d2fde5abd03a85cabf4", + "moves": 34, + "name": "single_cell_digit", + "reads": 34, + "visited_cells": 10, + "writes": 9 + }, + { + "L": 1, + "M": 2, + "actions": 77, + "mask_sha256": "938db8c9f82c8cb58d3f3ef4fd250036a48d26a712753d2fde5abd03a85cabf4", + "moves": 34, + "name": "single_cell_guard", + "reads": 34, + "visited_cells": 10, + "writes": 9 + }, + { + "L": 2, + "M": 4, + "actions": 168, + "mask_sha256": "5bedd317328c9ed79ecd3aecee74d37f97813cb4ce61ef3402eb388fb369fa86", + "moves": 76, + "name": "two_adjacent_single_cell_digits", + "reads": 75, + "visited_cells": 14, + "writes": 17 + }, + { + "L": 2, + "M": 4, + "actions": 168, + "mask_sha256": "fe675fe7aaee830b6fed09b64e034f84dcbdaeb429d9cccd4ebb90e15af8dd71", + "moves": 76, + "name": "two_cell_MSB_guard", + "reads": 75, + "visited_cells": 14, + "writes": 17 + } + ], + "scope": "Admitted fixed-alphabet stencil only; no construction/admission/E/payload tariff", + "structural_guardrail": { + "functions_inspected": [ + "rewind", + "compare_flag", + "predicate", + "increment_and_return", + "erase_counter", + "transduce" + ], + "observer_accesses": 0, + "scope": "AST guardrail plus manual finite-control review, not a complete program proof" + } +} diff --git a/research/crt-dense-guard-scan/CROSS-REPLAY.json b/research/crt-dense-guard-scan/CROSS-REPLAY.json new file mode 100644 index 0000000000..3cc9955d54 --- /dev/null +++ b/research/crt-dense-guard-scan/CROSS-REPLAY.json @@ -0,0 +1,135 @@ +{ + "helpers": { + "cross_check.py": "a1fb766eeaa062b7677ff33d4430c96563b97de0a5129455d4710a0b947f69ed", + "independent_guard_oracle.py": "5863cd978de7f81c0627ba6ade29912ea2de99fbd149db8575302f3f10e97a3e" + }, + "python": "3.12.14 (main, Aug 25 2026, 13:50:33) [Clang 22.1.3 ]", + "runs": [ + { + "argv_template": [ + "{python}", + "-I", + "-B", + "{review}/cross_check.py", + "{package}", + "{repository}" + ], + "exit_code": 0, + "receipt": { + "generic_stencils": { + "addresses": 1300, + "cases": 181, + "combined_mask_ascii_sha256": "b41657849cd1c7a0b05473a1ef687b627d13f970c2dc55942bb8c5e084d4a363", + "coverage": "L=1..3 all-SKIP; every single D placement; every single G placement/all threshold pairs; adjacent D/G orders", + "observed_actions": 59409 + }, + "preimplementation_oracle_sha256": "5863cd978de7f81c0627ba6ade29912ea2de99fbd149db8575302f3f10e97a3e", + "primary_hashes": { + "SOURCE-PINS.json": "e8e5c7320fb0bd1494e063eaa5aaf5f2f08562b80b72750081ea5a409eea5b1e", + "machine.py": "1cb27312932914eb631078bd56e85feb1dc6c4191e9d1962b2cc3a7e1cfb8df7", + "verify.py": "40794cd2e2936f0f5e42fac1bb51b65c951a2ab56b7e88824e8c2d09a3dbf40e" + }, + "scope": "Complete Boolean output/ownership cross-check; source predicate projections, not production placement; geometry/admission and oracle are unpriced host work.", + "source_files_checked": 3, + "source_fixture_addresses": 49408, + "source_fixtures": [ + { + "addresses": 16384, + "back_skip_bits": 0, + "bad": 16128, + "good": 256, + "mask_ascii_sha256": "5d1906a782234a5664d5b1478baaaea2becd207fe111676581c6fc64c40fca29", + "name": "two_active_digits", + "observed_actions": 2080968 + }, + { + "addresses": 32768, + "back_skip_bits": 0, + "bad": 18944, + "good": 13824, + "mask_ascii_sha256": "92e2c33f11c21d88a022ab8fedd137181ee026557f2b84dce81d7a1bd40d1354", + "name": "single_with_dirty_spectators", + "observed_actions": 4423893 + }, + { + "addresses": 256, + "back_skip_bits": 1, + "bad": 224, + "good": 32, + "mask_ascii_sha256": "30852858b0e592a63a14bf785536c81b448d1d6fb4fc3f79979876aad58bd278", + "name": "one_target_with_back_spectator", + "observed_actions": 20346 + } + ], + "status": "PASS_INDEPENDENT_LITERAL_GUARD_CROSS_CHECK" + }, + "stderr": "" + }, + { + "argv_template": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{review}/cross_check.py", + "{package}", + "{repository}" + ], + "exit_code": 0, + "receipt": { + "generic_stencils": { + "addresses": 1300, + "cases": 181, + "combined_mask_ascii_sha256": "b41657849cd1c7a0b05473a1ef687b627d13f970c2dc55942bb8c5e084d4a363", + "coverage": "L=1..3 all-SKIP; every single D placement; every single G placement/all threshold pairs; adjacent D/G orders", + "observed_actions": 59409 + }, + "preimplementation_oracle_sha256": "5863cd978de7f81c0627ba6ade29912ea2de99fbd149db8575302f3f10e97a3e", + "primary_hashes": { + "SOURCE-PINS.json": "e8e5c7320fb0bd1494e063eaa5aaf5f2f08562b80b72750081ea5a409eea5b1e", + "machine.py": "1cb27312932914eb631078bd56e85feb1dc6c4191e9d1962b2cc3a7e1cfb8df7", + "verify.py": "40794cd2e2936f0f5e42fac1bb51b65c951a2ab56b7e88824e8c2d09a3dbf40e" + }, + "scope": "Complete Boolean output/ownership cross-check; source predicate projections, not production placement; geometry/admission and oracle are unpriced host work.", + "source_files_checked": 3, + "source_fixture_addresses": 49408, + "source_fixtures": [ + { + "addresses": 16384, + "back_skip_bits": 0, + "bad": 16128, + "good": 256, + "mask_ascii_sha256": "5d1906a782234a5664d5b1478baaaea2becd207fe111676581c6fc64c40fca29", + "name": "two_active_digits", + "observed_actions": 2080968 + }, + { + "addresses": 32768, + "back_skip_bits": 0, + "bad": 18944, + "good": 13824, + "mask_ascii_sha256": "92e2c33f11c21d88a022ab8fedd137181ee026557f2b84dce81d7a1bd40d1354", + "name": "single_with_dirty_spectators", + "observed_actions": 4423893 + }, + { + "addresses": 256, + "back_skip_bits": 1, + "bad": 224, + "good": 32, + "mask_ascii_sha256": "30852858b0e592a63a14bf785536c81b448d1d6fb4fc3f79979876aad58bd278", + "name": "one_target_with_back_spectator", + "observed_actions": 20346 + } + ], + "status": "PASS_INDEPENDENT_LITERAL_GUARD_CROSS_CHECK" + }, + "stderr": "" + } + ], + "schema_version": 1, + "status": "PASS_INDEPENDENT_CROSS_NORMAL_OPTIMIZED", + "timestamp_utc": "2026-10-20T13:38:31.105404+00:00" +} diff --git a/research/crt-dense-guard-scan/EVIDENCE.md b/research/crt-dense-guard-scan/EVIDENCE.md new file mode 100644 index 0000000000..c389a3df9b --- /dev/null +++ b/research/crt-dense-guard-scan/EVIDENCE.md @@ -0,0 +1,46 @@ +# Evidence and review boundary + +The mathematical result is the uniform supplied-stencil program and census +in PROOF.md. Finite complete masks corroborate that written construction; +they do not implement the geometry producer or a full CRT/callee theorem. + +VERIFY.json registers eight normal/optimized commands: primary source-bound +literal replay, independent preimplementation predicate oracle, pinned +complete-mask crosscheck, and independent generic cost checker. Every helper +referenced by the retained receipts is included. The required Open next +questions README heading was added after review; both reviewers independently +confirmed that exact heading-only change, updated the submitted README pin, +and retained their original reviewed hash in explicit metadata addenda. Default replay never +regenerates the stored scientific RESULT.json. + +INITIAL-REVIEW.md/json and independent_guard_oracle.py preserve the semantic +oracle fixed before primary inspection. It covers49,152 complete addresses, +196,608 parity/spectator toggles and12 boundary cases. The primary adds the +complete256-address back-spectator fixture. cross_check.py pins the final +machine, host adapter, source pins and unchanged oracle; it checks49,408 source +addresses and181 generic stencils/1,300 addresses. PRIMARY-REVIEW.md/json +records that later source-bound comparison and read-only review. + +INDEPENDENT-COST-REVIEW.md and REPORT.json retain a separate implementation/ +proof inspection. cost_check.py independently checks READ/WRITE/MOVE and +visited-cell formulas over14 cases/2,058 addresses, including single-cell +begin/end cases. Its omitted-READ accounting fault preserves output and +ownership but fails the invoice. AST guardrails support inspection; they +are explicitly not a formal finite-state certificate. + +The normal program actually executes one-cell/head actions; its exact census +is8ML+15M+13L+18. Converting fixed alphabet/control to bit-machine steps adds +a parameter-independent constant factor. The claim is not Python wall-time +or an exact bit-machine coefficient. Host admission, source comparisons, +geometry building, hashing and observer integers are outside that program. + +The input stencil is admitted and protected; private counter data plus its +right marker return to blank, and permanent left boundaries are initial +infrastructure. The owned BAD mask is retained with its head returned. Physical +roles are reused only after the prior owned result is consumed and cleared. + +Cinna Davis already supplied the ordered-scan proposal and predicate; Hiroki +KUMAZAKI's PR4169/4174 supply repair and descriptor/placement context. Their +mechanisms, Douglas Colkitt/OpenAI framework and full source NOTICE lineage +remain credited. All work has substantial OpenAI Codex assistance; separate +agents are not independent human or formal-kernel acceptance. diff --git a/research/crt-dense-guard-scan/INDEPENDENT-COST-REVIEW.md b/research/crt-dense-guard-scan/INDEPENDENT-COST-REVIEW.md new file mode 100644 index 0000000000..cfb0717837 --- /dev/null +++ b/research/crt-dense-guard-scan/INDEPENDENT-COST-REVIEW.md @@ -0,0 +1,158 @@ +# Independent literal dense-guard machine review + +Reviewer: independent OpenAI Codex agent, not human or formal-kernel review. +Scope: the admitted ordered-stencil transducer, its complete address counter, +owned mask and physical head/cleanup tariff. The semantic guard predicate, +good-set theorem, compact inverse/repair and reservoir descriptors are +predecessor work. This review adds no E evaluator, physical compact switch, +payload movement, precision or multiplication theorem. + +## Quantified interface and constructive cost argument + +Let a protected stencil have L>=1 data cells and explicit boundary markers. +Each data symbol comes from one fixed finite product alphabet. It describes +an untested bit, a bit of an active all-ones digit test, or a guard-comparison +bit with its two threshold bits; interval begin/end flags determine when the +finite comparison state resets or contributes to the final conjunction. +Assume this stencil is well formed, ordered and complete. Geometry parsing, +sorting, source-descriptor transport, threshold/stencil construction and +admission are dependencies unless the submitted machine literally executes +and charges them. Their host adapters cannot be silently included in this +transducer's invoice. + +A private L-bit counter starts at zero. On each pass, scan its bits and the +stencil from most significant to least significant. One all-ones flag, two +three-state less/equal/greater flags, a running conjunction and a fixed +control mode suffice. They are finite state, independent of the number of +intervals and of L. This scan needs neither an interval-ID array nor a +numeric address register. The lower threshold accepts equality; the upper +threshold rejects equality. The target parity bit, inactive high compact +digits and dirty spectator bits remain untested by the source-bound stencil. + +Append exactly one classification bit to one owned mask tape. Increment the +counter using a literal binary-carry walk, with tape-marker tests and all +head motions charged. Stop only on left-marker overflow after processing the +all-ones counter. Do not use a host loop through range(2^L), an uncharged +numeric address/position variable, or a test-fixture fuel counter as the +machine's termination criterion. The loop invariant is that its counter is +the next address and every previous address has been classified exactly once. +Therefore the owned mask has M=2^L bits in increasing address order. + +One aligned scan and returns, one binary-carry increment and returns, and a +constant amount of finite state work per visited cell cost O(L) transitions +per emitted bit. Initialization and final erasure/returns cost O(L), and +returning the owned mask head costs O(M). Thus time is O(ML) and total visited +space, including protected input and owned mask, is O(M+L). The tape-role +inventory is fixed. No source-function or E-evaluator call is needed to +classify any address. + +For the retained source family, L=Theta(p) and R=Theta(p), hence L=O(R) and +O(ML)=O(MR)=O(V). The final equality cannot be asserted for arbitrary positive +record width R. Mask classification also does not include payload reading, +exception extraction, key computation, sorting or reinsertion. + +## Exact counter check independent of the implementation + +Across x=0,...,M-1, the sum of trailing-one counts is + +``` +sum_(k=1)^L count{x: x has at least k trailing ones} += sum_(k=1)^L M/2^k = M-1. +``` + +Every nonoverflow increment also reads/writes one terminating zero, and +there are M-1 such increments. Consequently a straightforward binary carry +routine changes exactly `2M-2` counter-bit cells across the entire run: +`M-1` one-to-zero changes and `M-1` zero-to-one changes. Marker reads, head +movement and final blank erasure are additional paid work. This is an exact +all-size identity, not an extrapolation from finite receipts. + +Overflow restores all counter bits to zero. Zero is distinct from blank, +so this is not by itself private-work erasure. A claimed blank-return +contract must execute a final erase pass (including any owned boundary +marker) and return that private head. A weaker reusable-zero counter +contract must be named explicitly instead. + +All successful-call protected inputs must be unchanged and their heads +returned. The final owned mask remains the output, with its head returned; +it must not be erased as private work. Repeated invocations reuse these +fixed physical tape roles only after their previous owned outputs have been +consumed/transferred and the relevant role has been prepared for reuse. + +The exact submitted transition invoice and frozen file hashes are recorded +in the final section and accompanying receipt after stable-code review. + +## Final stable kernel and written-proof review + +I read the complete submitted `machine.py`, `verify.py`, `PROOF.md`, +`README.md`, `RESULT.json` and `SOURCE-PINS.json`. The program below the +emulator never reads `Tape.head`, allocated-cell arrays, action counts, +`len`, `L`, `M` or a host position counter. Its marker-driven helper calls +have fixed depth and can be inlined. Each stencil atom is one symbol of a +fixed finite product alphabet; tuple decoding and comparison-state updates +therefore have fixed finite-control implementations. Exact READ/WRITE/MOVE +totals are cell/head action counts. The extra finite-control transitions +introduce a uniform constant factor, not free unbounded arithmetic. + +The normal program has these independently derived phase counts: + +| Phase | Cell/head actions | +|---|---:| +| Initialize counter from stencil; position owned mask | `8L+11` | +| All predicate scans, mask appends and stencil returns | `(6L+8)M` | +| All carries, overflow detection and counter returns | `(2L+5)M-3` | +| Blank private counter data and allocated right marker; return | `5L+6` | +| Owned mask right marker and complete return | `2M+4` | + +A successful carry reads exactly `L+2` symbols and makes `L+1` moves, +including its return: if there are t trailing ones, its carry examines t+1 +bits and its rewind starts L-t cells from the permanent left sentinel. +The final overflowing carry reads and moves `L+1` times. Together with the +`2M-2` bit changes derived above, these give the third row. Counting each +kind of operation separately gives + +``` +READ = (4L+6)M + 5L + 9 +WRITE = 3M + 2L + 1 +MOVE = (4L+6)M + 6L + 8 +SUM = 8ML + 15M + 13L + 18. +``` + +The two length-L roles visit `L+2` cells each. The owned mask role visits +`M+2` cells. Thus complete visited space is exactly `M+2L+6` cells, +including every marker, protected input and owned output. The permanent +left sentinel is initial tape infrastructure; all counter data and its +allocated right marker are restored to blank, and all heads return. +The mask's bits/right marker remain owned output. Reuse obligations are +stated explicitly; no new tape is allocated per record or retained answer. + +`cost_check.py` independently imports only this frozen machine, not the +primary verifier. It checks the separately derived per-operation and space +formulas on 14 admitted stencils covering 2,058 complete addresses: all-skip +lengths 1 through 10, single-cell digit and guard begin=end boundaries, +adjacent single-cell digits, and a two-cell MSB-first threshold case. Its +observer-tariff fault omits one READ charge without changing output or +ownership, and the independent invoice rejects it. Its AST checks are +structural guardrails against accessing observer coordinates/counters or +host loop/index helpers; they are not presented as a complete formal proof. +Normal and optimized Python results are recorded in the accompanying report. + +The primary's omitted-low-counter-bit mutation is an actual terminating +incorrect enumeration and is rejected by complete output cardinality. +Its omitted-mask-return mutation violates the owned-head contract. Its +threshold/significance/parity mutants and host admission rejections are +accurately separated. There is no claimed private-erasure mutation test; +normal successful blank erasure is inspected and checked directly. + +The source-binding geometry uses exactly the low active compact digits and +K-1 higher guard bits, with lower-inclusive/upper-strict comparison. Target +parity, inactive high compact digits, Y spectators and optional dirty back +bits are untested. Complete source fixtures are predicate projections, not +full production reservoir invocations. Geometry/stencil construction and +admission remain explicitly unpriced dependencies; so do exceptional keys, +extraction/sorting/reinsertion, payload movement and the complete evaluator. + +No material kernel, exact-invoice, finite-inventory, cleanup, source-interface +or written-cost-proof defect remains in the reviewed stable candidate. +Independent AI review is not human review, formal-kernel acceptance or a +literal emitted finite-state transition-table certificate. diff --git a/research/crt-dense-guard-scan/INITIAL-REVIEW.json b/research/crt-dense-guard-scan/INITIAL-REVIEW.json new file mode 100644 index 0000000000..fefa288e94 --- /dev/null +++ b/research/crt-dense-guard-scan/INITIAL-REVIEW.json @@ -0,0 +1,408 @@ +{ + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "before_primary_read": true, + "files": { + "INITIAL-REVIEW.md": "de8213183f4b02378dcbc43f50afde6adb4dfb4ee1bed5665edae04519359519", + "independent_guard_oracle.py": "5863cd978de7f81c0627ba6ade29912ea2de99fbd149db8575302f3f10e97a3e" + }, + "python": "3.12.14 (main, Aug 25 2026, 13:50:33) [Clang 22.1.3 ]", + "runs": [ + { + "argv_template": [ + "{python}", + "-I", + "-B", + "{package}/independent_guard_oracle.py", + "research/unconditional-batched-crt/check_batched_crt.py" + ], + "cwd_template": "{repository}", + "exit_code": 0, + "receipt": { + "fixtures": [ + { + "G": 1, + "H": 2, + "K": 5, + "L": 14, + "Y": 10, + "addresses": 16384, + "bad": 16128, + "bad_mask_ascii_sha256": "5d1906a782234a5664d5b1478baaaea2becd207fe111676581c6fc64c40fca29", + "boundaries": [ + { + "good": false, + "guard_value": 3, + "position": 0 + }, + { + "good": true, + "guard_value": 4, + "position": 0 + }, + { + "good": true, + "guard_value": 11, + "position": 0 + }, + { + "good": false, + "guard_value": 12, + "position": 0 + }, + { + "good": false, + "guard_value": 3, + "position": 5 + }, + { + "good": true, + "guard_value": 4, + "position": 5 + }, + { + "good": true, + "guard_value": 11, + "position": 5 + }, + { + "good": false, + "guard_value": 12, + "position": 5 + } + ], + "domain": "complete U|T|Y source predicate projection; no back reservoir/payload permutation", + "good": 256, + "good_mask_ascii_sha256": "5b6d6634c9368e794e397e552107cf134cf7ec053ca313912b6ceb417f38d043", + "good_mask_binary_sha256": "fde614ca102c04865118150c86a5e580bf10d95a6e4b5f2849ad5512d12e4428", + "ignored_bit_invariance_toggles": 32768, + "ignored_bits": [ + { + "numeric_address_bit": 0, + "role": "target_parity" + }, + { + "numeric_address_bit": 5, + "role": "target_parity" + } + ], + "name": "two_active_digits", + "positions": [ + 0, + 5 + ] + }, + { + "G": 2, + "H": 3, + "K": 7, + "L": 15, + "Y": 9, + "addresses": 32768, + "bad": 18944, + "bad_mask_ascii_sha256": "92e2c33f11c21d88a022ab8fedd137181ee026557f2b84dce81d7a1bd40d1354", + "boundaries": [ + { + "good": false, + "guard_value": 7, + "position": 1 + }, + { + "good": true, + "guard_value": 8, + "position": 1 + }, + { + "good": true, + "guard_value": 55, + "position": 1 + }, + { + "good": false, + "guard_value": 56, + "position": 1 + } + ], + "domain": "complete U|T|Y source predicate projection; no back reservoir/payload permutation", + "good": 13824, + "good_mask_ascii_sha256": "533b638b6dd44db05b278659a5901a5ffd76593aadb5d01cab972f3054ee4f4b", + "good_mask_binary_sha256": "be65805e70b31dd2d373bf13a9deebbae8ca236424bb420f5d7b59dac5f64bd3", + "ignored_bit_invariance_toggles": 163840, + "ignored_bits": [ + { + "numeric_address_bit": 1, + "role": "target_parity" + }, + { + "numeric_address_bit": 14, + "role": "inactive_u" + }, + { + "numeric_address_bit": 11, + "role": "inactive_t" + }, + { + "numeric_address_bit": 0, + "role": "Y_spectator" + }, + { + "numeric_address_bit": 8, + "role": "Y_spectator" + } + ], + "name": "single_with_dirty_spectators", + "positions": [ + 1 + ] + } + ], + "negative_controls": { + "dirty_inactive_upper_control": { + "expected_good": true, + "t": 0, + "u": 4, + "y": 32, + "zero_initialization_assumption_wrong": false + }, + "ignore_upper_active_digit": { + "address": 2312, + "expected_good": false, + "t": 2, + "u": 0, + "wrong_good": true, + "y": 264 + }, + "inclusive_upper": { + "address": 280, + "expected_good": false, + "t": 0, + "u": 0, + "wrong_good": true, + "y": 280 + }, + "strict_lower": { + "address": 264, + "expected_good": true, + "t": 0, + "u": 0, + "wrong_good": false, + "y": 264 + }, + "target_parity_in_guard": { + "address": 231, + "expected_good": false, + "t": 0, + "u": 0, + "wrong_good": true, + "y": 231 + } + }, + "scope": "complete Boolean masks and boundary/dirty-coordinate controls; no sequential/tape tariff", + "source_sha256": "681e2e3d71fa74c8b9b326f3860104fd9d89590a222e26ae6ee718d1fd40ff2e", + "status": "PASS_PREIMPLEMENTATION_DENSE_GUARD_ORACLE" + }, + "stderr": "" + }, + { + "argv_template": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/independent_guard_oracle.py", + "research/unconditional-batched-crt/check_batched_crt.py" + ], + "cwd_template": "{repository}", + "exit_code": 0, + "receipt": { + "fixtures": [ + { + "G": 1, + "H": 2, + "K": 5, + "L": 14, + "Y": 10, + "addresses": 16384, + "bad": 16128, + "bad_mask_ascii_sha256": "5d1906a782234a5664d5b1478baaaea2becd207fe111676581c6fc64c40fca29", + "boundaries": [ + { + "good": false, + "guard_value": 3, + "position": 0 + }, + { + "good": true, + "guard_value": 4, + "position": 0 + }, + { + "good": true, + "guard_value": 11, + "position": 0 + }, + { + "good": false, + "guard_value": 12, + "position": 0 + }, + { + "good": false, + "guard_value": 3, + "position": 5 + }, + { + "good": true, + "guard_value": 4, + "position": 5 + }, + { + "good": true, + "guard_value": 11, + "position": 5 + }, + { + "good": false, + "guard_value": 12, + "position": 5 + } + ], + "domain": "complete U|T|Y source predicate projection; no back reservoir/payload permutation", + "good": 256, + "good_mask_ascii_sha256": "5b6d6634c9368e794e397e552107cf134cf7ec053ca313912b6ceb417f38d043", + "good_mask_binary_sha256": "fde614ca102c04865118150c86a5e580bf10d95a6e4b5f2849ad5512d12e4428", + "ignored_bit_invariance_toggles": 32768, + "ignored_bits": [ + { + "numeric_address_bit": 0, + "role": "target_parity" + }, + { + "numeric_address_bit": 5, + "role": "target_parity" + } + ], + "name": "two_active_digits", + "positions": [ + 0, + 5 + ] + }, + { + "G": 2, + "H": 3, + "K": 7, + "L": 15, + "Y": 9, + "addresses": 32768, + "bad": 18944, + "bad_mask_ascii_sha256": "92e2c33f11c21d88a022ab8fedd137181ee026557f2b84dce81d7a1bd40d1354", + "boundaries": [ + { + "good": false, + "guard_value": 7, + "position": 1 + }, + { + "good": true, + "guard_value": 8, + "position": 1 + }, + { + "good": true, + "guard_value": 55, + "position": 1 + }, + { + "good": false, + "guard_value": 56, + "position": 1 + } + ], + "domain": "complete U|T|Y source predicate projection; no back reservoir/payload permutation", + "good": 13824, + "good_mask_ascii_sha256": "533b638b6dd44db05b278659a5901a5ffd76593aadb5d01cab972f3054ee4f4b", + "good_mask_binary_sha256": "be65805e70b31dd2d373bf13a9deebbae8ca236424bb420f5d7b59dac5f64bd3", + "ignored_bit_invariance_toggles": 163840, + "ignored_bits": [ + { + "numeric_address_bit": 1, + "role": "target_parity" + }, + { + "numeric_address_bit": 14, + "role": "inactive_u" + }, + { + "numeric_address_bit": 11, + "role": "inactive_t" + }, + { + "numeric_address_bit": 0, + "role": "Y_spectator" + }, + { + "numeric_address_bit": 8, + "role": "Y_spectator" + } + ], + "name": "single_with_dirty_spectators", + "positions": [ + 1 + ] + } + ], + "negative_controls": { + "dirty_inactive_upper_control": { + "expected_good": true, + "t": 0, + "u": 4, + "y": 32, + "zero_initialization_assumption_wrong": false + }, + "ignore_upper_active_digit": { + "address": 2312, + "expected_good": false, + "t": 2, + "u": 0, + "wrong_good": true, + "y": 264 + }, + "inclusive_upper": { + "address": 280, + "expected_good": false, + "t": 0, + "u": 0, + "wrong_good": true, + "y": 280 + }, + "strict_lower": { + "address": 264, + "expected_good": true, + "t": 0, + "u": 0, + "wrong_good": false, + "y": 264 + }, + "target_parity_in_guard": { + "address": 231, + "expected_good": false, + "t": 0, + "u": 0, + "wrong_good": true, + "y": 231 + } + }, + "scope": "complete Boolean masks and boundary/dirty-coordinate controls; no sequential/tape tariff", + "source_sha256": "681e2e3d71fa74c8b9b326f3860104fd9d89590a222e26ae6ee718d1fd40ff2e", + "status": "PASS_PREIMPLEMENTATION_DENSE_GUARD_ORACLE" + }, + "stderr": "" + } + ], + "schema_version": 1, + "scope": "complete independent source-bound Boolean masks and boundary/dirty-coordinate controls; no tape tariff", + "status": "PASS_PREIMPLEMENTATION_GUARD_REVIEW", + "time_utc": "2026-10-20T13:26:25.011591+00:00" +} diff --git a/research/crt-dense-guard-scan/INITIAL-REVIEW.md b/research/crt-dense-guard-scan/INITIAL-REVIEW.md new file mode 100644 index 0000000000..5f5f38d0bc --- /dev/null +++ b/research/crt-dense-guard-scan/INITIAL-REVIEW.md @@ -0,0 +1,89 @@ +# Independent dense-guard review before primary implementation inspection + +Context: canonical main `12fa8c5c844be21bfefb38a19503fbd867a11244`, +priority7; retained Cinna Davis PR4100 `CRT.md` dense-guard paragraph and +`check_batched_crt.py::good/linear_guard`. No primary scanner code was read +before this oracle was fixed. Source SHA256 is pinned in the oracle. + +## Predicate and bit order + +Let B=2^G and let r active digits occupy the low rG bits of complete H-bit +control fields U,T, with H>=rG. For each target position p_i in Y define + + v_i = floor(Y/2^(p_i+1)) modulo 2^(K-1). + +The guard is good exactly when every active U/T digit differs from B-1 +and every `v_i` satisfies + + 2B <= v_i < 2^(K-1)-2B. + +The lower boundary is inclusive and the upper boundary strict. Target +parity at p_i is omitted. The complete K-bit guard intervals are disjoint +and fit within Y. On a physical MSB-first scan the comparison bits for a +guard run from p_i+K-1 down to p_i+1; the target bit itself is skipped. +Comparison flags retain the first unequal bit. An all-ones flag is reset +at each active digit boundary. Upper unused control bits and all other +Y spectators must be ignored even when dirty. + +This factorized predicate does not require a permutation, source switch +evaluation, modular arithmetic, sparse-hole extraction or record sorting. +The literals are numerical address bits and comparison thresholds. A mask +must declare whether one means good or bad, and must follow the complete +address-counter order exactly once, including zero and the all-ones address. + +## Complete independent oracle + +`independent_guard_oracle.py` uses integer quotient/remainder expressions, +rather than a stencil scanner, and compares every address against both +authenticated source predicates. Address order is numeric MSB U|T|Y, +`address=(u*2^H+t)*2^Y+y`. + +The first fixture has G1,K5,H2,Y10, positions(0,5): L14 and all16,384 +addresses. Both U/T fields must be zero. Each 4-bit comparison field has +eight accepted values4,...,11, while both target parities are free. There +are exactly256 good and16,128 bad addresses. + +The second has G2,K7,H3,Y9, position1: L15 and all32,768 addresses. Each +control has six accepted values (the low two-bit digit must differ from3, +while its high bit is arbitrary). The six-bit comparison has48 accepted +values8,...,55. Target parity, lower Y bit0 and upper Y bit8 are free. +There are exactly13,824 good and18,944 bad addresses. + +The oracle records good-mask hashes in both binary-byte and ASCII-bit +representations, plus an ASCII bad-mask hash. It checks196,608 target-parity +and dirty-spectator invariance toggles, twelve explicit interval boundaries, +and witnesses for strict-lower, inclusive-upper, parity-in-comparison and +omitted-higher-active-digit mutations. A separate dirty-upper-control +witness is accepted, whereas an actual all-ones low active digit is rejected. + +These are complete U|T|Y **predicate projections**, not complete three-H-field +reservoir placement or payload-permutation executions. Appending an omitted +back field adds independent spectator bits; no production placement claim +is inferred from the reduced fixtures. + +## Scanner review obligations + +For an admitted ordered finite-alphabet stencil, its cell count must be O(L) +with fixed alphabet/role types. All comparisons and counters need an explicit +sequential implementation, without a free numerical L, M or random-access +position register. The binary counter must emit exactly2^L masks and terminate +on final overflow, without repeating zero. Every read/write/head return, +descriptor pass, mask write and final rewind must be paid. + +Final overflow makes a binary counter zero; it does **not** blank its tape. +If the contract promises erased private work, a literal final erase/return +pass is required. Output-mask preservation and original-stencil preservation +are separate from private cleanup. A host stencil builder is not a uniform +paid builder unless its own lowering is supplied. The scanner theorem may +instead take an admitted stencil as input, with that boundary explicit. + +An O(ML) scan bound becomes O(V) only with the source relation L=O(R), +V=MR, such as L,R=Theta(p). It does not pay exceptional key evaluation, +extraction, sorting, reinsertion, full E preparation or multiplication. + +## Credit and scope + +Cinna Davis supplies the dense-guard comparison and linear-pass proposal. +The source NOTICE retains the guard/compact-control lineage. This is separate +OpenAI Codex semantic review, not independent human review or formal-kernel +verification. The selected frontier and kappa are unchanged. diff --git a/research/crt-dense-guard-scan/PRIMARY-REVIEW.json b/research/crt-dense-guard-scan/PRIMARY-REVIEW.json new file mode 100644 index 0000000000..dc474a3a41 --- /dev/null +++ b/research/crt-dense-guard-scan/PRIMARY-REVIEW.json @@ -0,0 +1,61 @@ +{ + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "generic_addresses_per_cross_run": 1300, + "generic_stencil_cases_per_cross_run": 181, + "material_blockers": [], + "metadata_addendum": { + "change": "README only inserts heading ## Open next questions and one blank line before the existing next-obligation paragraph.", + "integrated_readme_sha256": "912595166aded8591819c1f4fccdd7bfa44361906a1466057f838a656e85f329", + "mathematical_replay_repeated": false, + "original_readme_sha256": "feb63f8391b49ee55332568bb8392b38c2c993fb31124902fd22c90987511b6b", + "other_five_primary_hashes_unchanged": true, + "reason_no_new_replay": "No algorithm, proof, fixture, receipt, source-pin or claim text changed.", + "status": "PASS_EXACT_METADATA_ONLY_INTEGRATION_DIFF", + "timestamp_utc": "2026-10-20T13:43:01.057177+00:00" + }, + "original_reviewed_primary_sha256": { + "PROOF.md": "c075a3c261bb824884f0da9f99fed227b15f9fac087bbdeb2c2cb861d4091f11", + "README.md": "feb63f8391b49ee55332568bb8392b38c2c993fb31124902fd22c90987511b6b", + "RESULT.json": "afb527f5f654d7888ca654ea4504258cdc0def8e952d7db67f66aeb3b292ae1a", + "SOURCE-PINS.json": "e8e5c7320fb0bd1494e063eaa5aaf5f2f08562b80b72750081ea5a409eea5b1e", + "machine.py": "1cb27312932914eb631078bd56e85feb1dc6c4191e9d1962b2cc3a7e1cfb8df7", + "verify.py": "40794cd2e2936f0f5e42fac1bb51b65c951a2ab56b7e88824e8c2d09a3dbf40e" + }, + "predecessor_credit": [ + "Cinna Davis pinned CRT.md ordered counter/comparison scan proposal.", + "Hiroki KUMAZAKI PR4169 arbitrary-source repair audit and PR4174 reservoir/ordered descriptors.", + "Douglas Colkitt/OpenAI retained source framework and notices." + ], + "preimplementation_oracle_unchanged": true, + "remaining_obligations": [ + "Coordinating agent registered package warm/cold replay and final integration integrity.", + "Uniform charged geometry/threshold producer and admission at actual transported caller.", + "Extraction/sort/repair/full E/callee/native/outer composition remain outside result." + ], + "replay_modes": [ + "normal isolated", + "optimized isolated warnings-as-errors" + ], + "retained_review_files_sha256": { + "CROSS-REPLAY.json": "19f82ceaf9aee4652087ef5a9e15ff76f1e749f837890cc7c2d8184d9cae2789", + "INITIAL-REVIEW.json": "ce8db24bbbff18656c2ab2df9834371d9604bb7f472e59d1ca04310633fd850d", + "INITIAL-REVIEW.md": "de8213183f4b02378dcbc43f50afde6adb4dfb4ee1bed5665edae04519359519", + "PRIMARY-REVIEW.md": "08d97e455c94c37c8f46b30095875aa2e89e5c9d7145366050bff160572b832a", + "cross_check.py": "a1fb766eeaa062b7677ff33d4430c96563b97de0a5129455d4710a0b947f69ed", + "independent_guard_oracle.py": "5863cd978de7f81c0627ba6ade29912ea2de99fbd149db8575302f3f10e97a3e" + }, + "review_kind": "Independent OpenAI Codex semantic review; not independent human or formal-kernel certification.", + "reviewed_primary_sha256": { + "PROOF.md": "c075a3c261bb824884f0da9f99fed227b15f9fac087bbdeb2c2cb861d4091f11", + "README.md": "912595166aded8591819c1f4fccdd7bfa44361906a1466057f838a656e85f329", + "RESULT.json": "afb527f5f654d7888ca654ea4504258cdc0def8e952d7db67f66aeb3b292ae1a", + "SOURCE-PINS.json": "e8e5c7320fb0bd1494e063eaa5aaf5f2f08562b80b72750081ea5a409eea5b1e", + "machine.py": "1cb27312932914eb631078bd56e85feb1dc6c4191e9d1962b2cc3a7e1cfb8df7", + "verify.py": "40794cd2e2936f0f5e42fac1bb51b65c951a2ab56b7e88824e8c2d09a3dbf40e" + }, + "schema_version": 1, + "scope": "Admitted finite stencil literal BAD mask, complete Boolean/source binding, ownership and census observer checks; source fixtures are predicate projections. Geometry/admission production and full caller remain open.", + "source_fixture_addresses_per_cross_run": 49408, + "status": "PASS_SCOPED_INDEPENDENT_SEMANTIC_REVIEW", + "timestamp_utc": "2026-10-20T13:39:31.074528+00:00" +} diff --git a/research/crt-dense-guard-scan/PRIMARY-REVIEW.md b/research/crt-dense-guard-scan/PRIMARY-REVIEW.md new file mode 100644 index 0000000000..22d28c1358 --- /dev/null +++ b/research/crt-dense-guard-scan/PRIMARY-REVIEW.md @@ -0,0 +1,77 @@ +# Independent review: literal dense guard-mask scan + +Verdict: **no material blocker found in the stated admitted-stencil result**. +This is an independent OpenAI Codex review and executed semantic oracle, not +independent human review or formal-kernel certification. + +## Scope and distinct evidence + +The frozen preimplementation quotient/remainder oracle (`INITIAL-REVIEW.json`, +`independent_guard_oracle.py`) was completed before reading the candidate. +It directly defines active compact digits and each parity-excluding guard +interval. Both retained source predicates agree on all 49,152 original fixture +addresses, with boundary, active-high-digit, dirty-spectator and parity controls. + +`cross_check.py` authenticates the primary machine/adapter/source pins and the +unchanged preimplementation oracle, then executes the literal transducer. +Normal and strict optimized Python each match the complete ordered BAD masks on +49,408 source-projection addresses. The third fixture independently lifts a +128-address oracle by repeating every decision over the omitted back bit. +Good counts are 256, 13,824 and 32; complete ASCII BAD hashes, including address +order, are retained in `CROSS-REPLAY.json`. Counts alone are not the comparison. + +The cross-check also exercises 181 admitted generic stencils / 1,300 addresses: +all-SKIP lengths 1..3; every single D placement; every single G placement and +every representable lower/upper threshold pair at those lengths; and both +adjacent D/G orders. This includes singleton begin=end, equal/reversed bounds, +and conjunction latching. Its oracle directly extracts numeric intervals and +does not reproduce the streaming comparison-state implementation. + +Every execution checks protected stencil preservation, returned heads, blank +private data including the right marker, owned output boundaries/cardinality, +and the exact cell-action and visited-cell formulas. The observer formulas +agree on all tested admitted stencils. Their all-size justification is the +written census, reviewed separately by the cost reviewer; finite matches do +not establish an asymptotic theorem by themselves. + +## Code and mathematical review + +The normal kernel never reads emulator coordinates, lengths, address integers, +or action totals. All non-tape values have fixed finite range and fixed-depth +helpers can be inlined. Lexicographic comparison retains the first differing +MSB, accepts lower equality and rejects upper equality. Source geometry maps +low active digits correctly, excludes arithmetic target parity, and leaves +inactive control/Y/back bits SKIP. This matches the independently defined +interval predicate over arbitrary dirty padded addresses. + +The zero counter is processed first; carry occurs after each emitted bit, +including the all-ones value. Overflow is distinct from cleanup: a subsequent +literal pass blanks every counter cell and its END marker, then returns. +Input and output ownership contracts are explicit, including retained LEFT +infrastructure and the caller's obligation to clear a prior owned output +before physical-role reuse. No source/E callback is hidden in the kernel. + +## Claim boundary and ancestry + +The proof and README consistently start from an **admitted ordered finite- +alphabet stencil**. Geometry/threshold production and admission remain +unpriced host adapters. The source's L=Theta(p), R=Theta(p), V=MR supports the +stated conditional O(V) detector tariff; R>=1 alone would not. The fixture +labels correctly say predicate projections, rather than production reservoir +placement. No extraction, sorting, repair, payload routing, full E evaluator, +ordinary callee, precision, native/outer theorem, or new kappa is certified. + +The scan mechanism is already proposed by Cinna Davis in pinned CRT.md +238–253. This result contributes its literal lowering, ownership/cleanup +contract and exact quantitative audit. The proof credits Hiroki KUMAZAKI's +PR4169 arbitrary-source repair audit and PR4174 reservoir/ordered-descriptor +work, plus retained Douglas Colkitt/OpenAI ancestry. Their open PRs are not +imported as discharged dependencies. + +## Replay and integrity + +`PRIMARY-REVIEW.json` records all six reviewed primary hashes and the complete +helper closure. `CROSS-REPLAY.json` contains normal and strict optimized argv +templates and exact outputs. No primary/shared file was edited. This review +performs the independent warm cross-check; the coordinating agent owns the +registered package warm/cold replay, final integration and publication. diff --git a/research/crt-dense-guard-scan/PROOF.md b/research/crt-dense-guard-scan/PROOF.md new file mode 100644 index 0000000000..235d7405ff --- /dev/null +++ b/research/crt-dense-guard-scan/PROOF.md @@ -0,0 +1,181 @@ +# Literal dense guard-mask scan from an admitted stencil + +## Scope and interface + +The input is an **admitted** nonempty length-`L` stencil, `L>=1`, over the +fixed finite alphabet below. The output is the complete `M=2^L`-bit BAD mask, +in increasing numerical order of the MSB-first binary address. BAD is the +complement of the conjunction of the stencil's digit and guard tests. +Geometry parsing, interval ordering, threshold generation and admission are +outside this interface. `verify.py` supplies host adapters for those tasks; +their rejection tests do not certify a tape implementation of admission. + +There are three reusable physical tape roles: protected stencil, private +counter, and caller-owned mask. Each has a permanent left marker `<` in its +initial configuration and otherwise initially blank cells `_`. The supplied +stencil has its `L` atoms followed by `>`. All heads start at `<`. On success +the stencil is unchanged, the counter's data and allocated right marker are +blank again, and the mask has `M` output bits followed by `>`. +Every head returns to `<`. The permanent left infrastructure is retained. +The caller must consume/transfer and clear a previous owned mask before this +same output role is reused; the theorem does not allocate a new physical +tape for each invocation. Source/payload streams are not among these roles. + +An atom is `(kind,begin,end,lower_bit,upper_bit)`, with kind in `{S,D,G}`, +two Boolean boundary flags and two bits. The canonical S atom is +`(S,false,false,0,0)`. D atoms carry zero threshold bits. Non-S intervals +are ordered, disjoint and complete: exactly one begin and end, of the same +kind, with no intervening S atom. A one-cell interval may begin and end in +the same atom. G atoms contain equal-width MSB-first lower/upper strings. +There may be no intervals at all. This is a fixed product alphabet; an atom +does not contain an integer interval number or a parameter-sized descriptor. + +For each D interval, reject exactly its all-ones string. For each G interval +with strings `lo,hi`, accept exactly `lo<=value`, and +writes an equally long all-zero binary counter and its own `>`. Literal +rewinds read symbols until `<`, paying for the boundary test. For each +counter value the two tapes are scanned together from left to right. A D +begin resets `all_ones=true`; every cell conjoins its bit, and the D end +conjoins `not all_ones` into the overall predicate. A G begin resets both +comparison flags to E. The first unequal pair sets L or G and later pairs +leave that flag unchanged. Induction over an interval proves that this is +the lexicographic comparison of its complete MSB-first strings. At its end +the lower flag must be E or G and the upper flag must be L. Thus equality +with the lower bound is accepted and equality with the upper bound rejected. +Each interval's result is conjoined, and S bits are ignored. + +Write one BAD bit at the mask head and move that head one cell right. Rewind +the stencil. The counter head is at `>`: move left, replace trailing ones +by zero, replace the first zero by one, and rewind to `<`. If carrying reaches +`<`, return the overflow flag. Standard binary induction proves that the +successive scanned counters are exactly `0,1,...,M-1`, with no repetition or +omission, and that the last carry leaves all counter bits zero. This proves +both the output length and its ordering, without a host loop of `M` steps. + +Overflow is not erasure: zero is distinct from blank. A final literal pass +therefore writes blank on every counter data cell **and its right marker**, +then reads/moves back to `<`. Append `>` to the mask and rewind that head. +This restores the exact initial private infinite-tape configuration while +preserving both protected input and owned output. A final fixed control state +discards the transient finite flags. The program has no variable-depth +recursion, indexed geometry lookup or parameter-dependent tape inventory. + +## Exact action census and asymptotic tariff + +Count each read, write and one-cell move as one action. Finite-control +transitions compile into a constant factor more machine steps, independent +of all parameters. Let `M=2^L`. The following counts are for the normal +program on every admitted stencil; they do not depend on which tests pass. + +| Phase | Cell/head actions | +|---|---:| +| Initialization, including first mask move | `8L+11` | +| Predicate scan, BAD append, stencil rewind for all addresses | `(6L+8)M` | +| All counter increments, including final overflow and rewinds | `(2L+5)M-3` | +| Counter data/right-marker blank erasure and return | `5L+6` | +| Mask right marker and return | `2M+4` | + +For the carry line, the `M-1` successful increments each read `L+2` cells +and move `L+1` times, including the rewind. Final overflow reads and moves +`L+1` times. The number of carried one bits over the complete enumeration is +`M-1`; there are also `M-1` successful zero-to-one writes. Thus carry writes +are `2M-2`, and its total is `(2L+5)M-3`. This charges every marker read, +counter update and return; there is no free numerical head-zero test. + +The resulting exact totals are + +``` +reads = (4L+6)M + 5L + 9 +writes = 3M + 2L + 1 +moves = (4L+6)M + 6L + 8 +total = 8ML + 15M + 13L + 18. +``` + +Visited cells, including protected input, output and all markers, are exactly +`(L+2)+(L+2)+(M+2)=M+2L+6`. The finite alphabet has constant encoding size. +Consequently this is one uniform fixed-tape procedure with time `O(ML)` and +visited space `O(M+L)`, from the admitted-stencil interface. The stored +receipt checks the exact census, not a fitted timing bound. Emulator counters, +hashing, source comparisons and host admission are not machine registers or +included action evidence. + +For the source's `V=MR` caller, its stated `L=Theta(p)` and `R=Theta(p)` give +`O(ML)=O(V)`. The condition `R>=1` alone would not suffice. This conclusion +prices the detector from its supplied stencil, not a complete source caller. +Its uniform geometry/threshold producer and admission tariff remain an +explicit obligation before composing an end-to-end O(V) implementation. + +## Binding the source predicate, without a hidden parity test + +The three pinned current-main files are authenticated by SHA-256 and Git +blob hash before loading the source. `check_batched_crt.py:142-175` defines +the same predicate in `good` and `linear_guard`. For `B=2^G`, active digits +are the low `rG` bits of each H-bit u/t field, split into G-bit digits; each +must differ from `B-1`. For target arithmetic position j, the guard is + +``` +g = (y >> (j+1)) mod 2^(K-1), 2B <= g < 2^(K-1)-2B. +``` + +The parity bit at j is excluded. Under the explicit physical address order +`u_H | t_H | y_Y | w_W`, with each field MSB-first, digit i of either control +field occupies `[field_start+H-(i+1)G, field_start+H-iG)`. The guard occupies +`[2H+Y-j-K, 2H+Y-j-1)`, width `K-1`. Encode its two thresholds in that width. +All other cells, including inactive high control bits, target parity bits, +unused Y cells and the complete optional w field, are S. The host adapter +requires complete disjoint `[j,j+K)` target segments and `H>=rG`. +These formulas prove equality with the source for every padded address of +any admitted geometry, independently of the finite tests. + +The finite fixtures are predicate projections, not full production +three-reservoir invocations: `(G,H,Y,K,targets,W)` is `(1,2,10,5,[0,5],0)`, +`(2,3,9,7,[1],0)` and `(1,1,5,5,[0],1)`. They exhaust all 49,408 addresses, +including dirty compact digits, guard boundaries, parity and spectator bits. +The two source functions agree with every literal output bit. All-S stencils +at `L=1,2,3` separately cover the no-test and smallest-overflow boundaries. +Negative controls alter lower/upper strictness, MSB significance, unadjusted +whole-K thresholds, output return and the counter's least significant bit. +The whole-K mutant keeps the K-1-bit numeric thresholds unchanged; properly +rescaled full-segment thresholds can represent the same guard and are not +claimed wrong. Host malformed-input rejection controls are admission-adapter +evidence only. Optimized Python retains every verifier check via explicit +exceptions rather than `assert`. + +## Predecessors and remaining obligations + +Cinna Davis already proposes this counter/ordered-descriptor scan and its +three-state comparisons in current-main `CRT.md:238-253`. This package +contributes the literal finite-control lowering, complete ownership/cell +census and source-bound executed checks; it claims no new guard mechanism. +Hiroki KUMAZAKI (@kumagi), PR4169 head +`835c3563ee7ede8ceaf329ede7372e50f7823136`, gives the arbitrary-source repair +predicate/proof and leaves guard-scan/function/sort costs open. PR4174 head +`5fec853f0c048871de3b8098d1e30d4ee19cda23` gives reservoir placement and +ordered descriptors while leaving their fixed-tape tariff open. Their +mechanisms and other source ancestry retain credit; neither open PR is +imported here. Douglas Colkitt/OpenAI's stream and compact-control framework +and all retained source notices remain unchanged. This work has substantial +OpenAI Codex assistance, Apache-2.0; no new formal-kernel or independent human +review is claimed. + +Still outside certification: uniform geometry/stencil production/admission, +transported caller descriptors, extraction/reinsertion and sorting, E work on +exceptional keys, switch-table/arithmetic evaluation, payload routing, repair, +ordinary callees, numerical precision, native/outer composition and a new +kappa or multiplication theorem. No selected-frontier change follows. diff --git a/research/crt-dense-guard-scan/README.md b/research/crt-dense-guard-scan/README.md new file mode 100644 index 0000000000..fd0dd321ba --- /dev/null +++ b/research/crt-dense-guard-scan/README.md @@ -0,0 +1,70 @@ +# Literal CRT dense guard-mask scan + +This package lowers the ordered scan already proposed in +[`CRT.md:238-253`](../unconditional-batched-crt/CRT.md) to a marker-driven +three-tape program. From an **admitted ordered stencil** of L fixed-alphabet +cells it writes the complete `M=2^L`-bit bad-address mask, preserves the +stencil, blanks all private work and returns every head. All padded address +bits are enumerated; inactive control bits, target parity and spectators +remain unconstrained when marked SKIP. + +The exact normal-program census is `8ML+15M+13L+18` cell/head actions and +`M+2L+6` visited cells, including input, output and markers. This gives +`O(ML)` time and `O(M+L)` space with three fixed tape roles and finite control. +Under the source's `L=Theta(p), R=Theta(p), V=MR`, the detector is `O(V)`. +Geometry-to-stencil production and admission remain explicit **unpriced** +dependencies. No complete caller or new kappa result is claimed. + +`machine.py` is the literal cell/head program. It neither reads a host +length/address/head coordinate nor calls a predicate/E callback. Its emulator +uses numerical coordinates and action totals solely as observers. The stencil +alphabet packs kind, interval boundaries and two threshold bits in one fixed +product alphabet. `PROOF.md` proves enumeration, MSB comparison, cleanup and +the exact census, and separates this supplied-stencil interface from the +unimplemented geometry producer. The permanent left sentinels belong to the +initial tape infrastructure; cleanup restores blank data and erases the +private right marker while retaining those sentinels. + +Run from the repository root with Python 3.12 and the pinned sources present: + +``` +python3 -I -B research/crt-dense-guard-scan/verify.py +python3 -I -O -W error -B research/crt-dense-guard-scan/verify.py +``` + +Both commands authenticate the three source files against `SOURCE-PINS.json` +and compare a fresh replay with `RESULT.json`; they do not rewrite it. +`--write-result` explicitly regenerates the receipt. The package uses only the +Python standard library and explicit checks that remain active under `-O`. + +Executed source binding exhausts 49,408 addresses in three predicate-projection +fixtures, rather than claiming a full production reservoir invocation: + +| G | H | Y | K | target positions | back SKIP bits | addresses | good | +|---:|---:|---:|---:|---|---:|---:|---:| +| 1 | 2 | 10 | 5 | 0,5 | 0 | 16,384 | 256 | +| 2 | 3 | 9 | 7 | 1 | 0 | 32,768 | 13,824 | +| 1 | 1 | 5 | 5 | 0 | 1 | 256 | 32 | + +Every output bit is compared with both retained `good` and `linear_guard`. +All-SKIP L=1..3 fixtures exercise the smallest complete counters. Mutations +detect wrong lower/upper strictness, wrong MSB significance, a whole-K guard +with unadjusted K-1-bit thresholds, omitted counter low bit and omitted owned +output return. Malformed geometry/stencil rejection tests belong to the +unpriced host admission adapter. Semantic/source comparisons, observer totals +and hashes are verification work, not hidden runtime registers or steps. + +Cinna Davis already supplied the predicate and ordered-scan proposal. +Hiroki KUMAZAKI (@kumagi), PR4169 and PR4174, supplied arbitrary-source repair +and reservoir/descriptor audits; those open PRs are credited, not imported. +Douglas Colkitt/OpenAI's stream and compact-control framework and the pinned +source NOTICE retain their ancestry. This contribution is the literal +lowering and quantitative audit, with substantial OpenAI Codex assistance, +Apache-2.0. No independent human or new formal-kernel review is claimed. + +## Open next questions + +The next obligation is a uniformly encoded, charged geometry/threshold +producer and admission path at the transported caller. Extraction, sorting, +repair, payload routing, full E evaluation, ordinary callees, precision, +native/outer composition and the selected frontier are outside this result. diff --git a/research/crt-dense-guard-scan/REPORT.json b/research/crt-dense-guard-scan/REPORT.json new file mode 100644 index 0000000000..d118ab0d31 --- /dev/null +++ b/research/crt-dense-guard-scan/REPORT.json @@ -0,0 +1,133 @@ +{ + "schema_version": 1, + "status": "PASS_INDEPENDENT_LITERAL_DENSE_GUARD_COST_INTERFACE_REVIEW", + "reviewer": "Independent OpenAI Codex agent; not human or formal-kernel review", + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "scope": "Admitted ordered finite-alphabet stencil to complete ordered BAD mask, literal counter and all head/ownership tariffs", + "primary_package": "research/crt-dense-guard-scan", + "primary_files_reviewed": [ + { + "path": "research/crt-dense-guard-scan/machine.py", + "sha256": "1cb27312932914eb631078bd56e85feb1dc6c4191e9d1962b2cc3a7e1cfb8df7" + }, + { + "path": "research/crt-dense-guard-scan/verify.py", + "sha256": "40794cd2e2936f0f5e42fac1bb51b65c951a2ab56b7e88824e8c2d09a3dbf40e" + }, + { + "path": "research/crt-dense-guard-scan/PROOF.md", + "sha256": "c075a3c261bb824884f0da9f99fed227b15f9fac087bbdeb2c2cb861d4091f11" + }, + { + "path": "research/crt-dense-guard-scan/README.md", + "sha256": "912595166aded8591819c1f4fccdd7bfa44361906a1466057f838a656e85f329" + }, + { + "path": "research/crt-dense-guard-scan/RESULT.json", + "sha256": "afb527f5f654d7888ca654ea4504258cdc0def8e952d7db67f66aeb3b292ae1a" + }, + { + "path": "research/crt-dense-guard-scan/SOURCE-PINS.json", + "sha256": "e8e5c7320fb0bd1494e063eaa5aaf5f2f08562b80b72750081ea5a409eea5b1e" + } + ], + "review_files": [ + { + "path": "INDEPENDENT-COST-REVIEW.md", + "sha256": "33a5f11a119ee40fcc9c5439e61ecefc96ab178a8e084a678b70f29f36b7122f" + }, + { + "path": "cost_check.py", + "sha256": "f78e0cc3faaad793241c1b11690033dc3ffa34f15b37217fa650c79e36a168bc" + }, + { + "path": "COST-CHECK-RESULT.json", + "sha256": "17d746168ae62b15efd66490d60b1f83546a030a47c0ccdcc6ceb2dac8da2ab6" + } + ], + "exact_quantified_counts": { + "read_actions": "(4L+6)M+5L+9", + "write_actions": "3M+2L+1", + "move_actions": "(4L+6)M+6L+8", + "total_cell_head_actions": "8ML+15M+13L+18", + "visited_cells_including_all_markers": "M+2L+6", + "carry_bit_changes": "2M-2", + "M": "2^L", + "L": "any positive admitted stencil length" + }, + "bounds": { + "time": "O(ML), including a fixed finite-control compilation factor", + "visited_space": "O(M+L), including protected stencil and owned mask", + "source_linear_payload_bound": "O(V) only under L=Theta(p), R=Theta(p), V=MR" + }, + "ownership": "Protected stencil unchanged; private data/right-marker blank; permanent left infrastructure retained; all three heads returned; mask owned", + "independent_checks": { + "cases": 14, + "complete_addresses": 2058, + "observer_tariff_faults": [ + { + "detected_by": "independently derived read/write/move invoice", + "name": "one READ omitted from observer tariff; mask and ownership preserved" + } + ], + "structural_guardrail": { + "functions_inspected": [ + "rewind", + "compare_flag", + "predicate", + "increment_and_return", + "erase_counter", + "transduce" + ], + "observer_accesses": 0, + "scope": "AST guardrail plus manual finite-control review, not a complete program proof" + } + }, + "replays": [ + { + "command": "python3 -B cost_check.py --machine PACKAGE/machine.py", + "exit_code": 0, + "elapsed_seconds": 0.043, + "result": "PASS_INDEPENDENT_LITERAL_GUARD_COST", + "cases": 14, + "complete_addresses": 2058, + "stderr": "" + }, + { + "command": "python3 -B -O cost_check.py --machine PACKAGE/machine.py", + "exit_code": 0, + "elapsed_seconds": 0.098, + "result": "PASS_INDEPENDENT_LITERAL_GUARD_COST", + "cases": 14, + "complete_addresses": 2058, + "stderr": "" + } + ], + "primary_unchanged_during_review": true, + "material_defects_remaining": [], + "remaining_obligations": [ + "Uniform encoded geometry/stencil generation and admission", + "Transported full caller descriptors", + "Exceptional E evaluation and keyed repair", + "Extraction/sorting/reinsertion and payload routing", + "Ordinary callees, precision/native/outer composition", + "Human or formal-kernel acceptance" + ], + "credit": [ + "Cinna Davis: predicate and proposed ordered counter/three-state scan", + "Hiroki KUMAZAKI PR4169/4174: arbitrary-source repair and reservoir descriptors", + "Douglas Colkitt/OpenAI and retained source notices: compact/stream framework" + ], + "metadata_addenda": [ + { + "kind": "Required research-package README heading", + "path": "research/crt-dense-guard-scan/README.md", + "original_reviewed_sha256": "feb63f8391b49ee55332568bb8392b38c2c993fb31124902fd22c90987511b6b", + "retained_integrated_sha256": "912595166aded8591819c1f4fccdd7bfa44361906a1466057f838a656e85f329", + "exact_change": "Insert literal ## Open next questions followed by a blank line immediately before the existing The next obligation paragraph.", + "independent_confirmation": "Byte-for-byte equality after exactly one heading insertion; every other retained primary file matches its original reviewed pin.", + "mathematical_or_executable_change": false, + "new_mathematical_replay": "Not needed for this heading-only metadata insertion." + } + ] +} diff --git a/research/crt-dense-guard-scan/RESULT.json b/research/crt-dense-guard-scan/RESULT.json new file mode 100644 index 0000000000..226a6a7d53 --- /dev/null +++ b/research/crt-dense-guard-scan/RESULT.json @@ -0,0 +1,179 @@ +{ + "schema_version": 1, + "result": "PASS_LITERAL_DENSE_GUARD_MASK", + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "source_inputs_checked": 3, + "fixtures": [ + { + "address_bits": 14, + "addresses": 16384, + "good_addresses": 256, + "bad_addresses": 16128, + "read_actions": 1015887, + "write_actions": 49181, + "move_actions": 1015900, + "total_cell_head_actions": 2080968, + "visited_cells_including_owned_mask": 16418, + "heads_returned": true, + "private_data_blank": true, + "mask_semantics": "1=bad, 0=good; increasing MSB-first binary address", + "mask_ascii_sha256": "5d1906a782234a5664d5b1478baaaea2becd207fe111676581c6fc64c40fca29", + "name": "two_target_complete", + "G": 1, + "H": 2, + "Y_bits": 10, + "targets": [ + 0, + 5 + ], + "K": 5, + "back_skip_bits": 0, + "domain": "predicate projection/stencil fixture, not a full production reservoir invocation" + }, + { + "address_bits": 15, + "addresses": 32768, + "good_addresses": 13824, + "bad_addresses": 18944, + "read_actions": 2162772, + "write_actions": 98335, + "move_actions": 2162786, + "total_cell_head_actions": 4423893, + "visited_cells_including_owned_mask": 32804, + "heads_returned": true, + "private_data_blank": true, + "mask_semantics": "1=bad, 0=good; increasing MSB-first binary address", + "mask_ascii_sha256": "92e2c33f11c21d88a022ab8fedd137181ee026557f2b84dce81d7a1bd40d1354", + "name": "inactive_digits_and_Y_spectators", + "G": 2, + "H": 3, + "Y_bits": 9, + "targets": [ + 1 + ], + "K": 7, + "back_skip_bits": 0, + "domain": "predicate projection/stencil fixture, not a full production reservoir invocation" + }, + { + "address_bits": 8, + "addresses": 256, + "good_addresses": 32, + "bad_addresses": 224, + "read_actions": 9777, + "write_actions": 785, + "move_actions": 9784, + "total_cell_head_actions": 20346, + "visited_cells_including_owned_mask": 278, + "heads_returned": true, + "private_data_blank": true, + "mask_semantics": "1=bad, 0=good; increasing MSB-first binary address", + "mask_ascii_sha256": "30852858b0e592a63a14bf785536c81b448d1d6fb4fc3f79979876aad58bd278", + "name": "one_target_with_back_spectator", + "G": 1, + "H": 1, + "Y_bits": 5, + "targets": [ + 0 + ], + "K": 5, + "back_skip_bits": 1, + "domain": "predicate projection/stencil fixture, not a full production reservoir invocation" + } + ], + "all_skip_boundaries": [ + { + "address_bits": 1, + "addresses": 2, + "good_addresses": 2, + "bad_addresses": 0, + "read_actions": 34, + "write_actions": 9, + "move_actions": 34, + "total_cell_head_actions": 77, + "visited_cells_including_owned_mask": 10, + "heads_returned": true, + "private_data_blank": true, + "mask_semantics": "1=bad, 0=good; increasing MSB-first binary address", + "mask_ascii_sha256": "f1534392279bddbf9d43dde8701cb5be14b82f76ec6607bf8d6ad557f60f304e" + }, + { + "address_bits": 2, + "addresses": 4, + "good_addresses": 4, + "bad_addresses": 0, + "read_actions": 75, + "write_actions": 17, + "move_actions": 76, + "total_cell_head_actions": 168, + "visited_cells_including_owned_mask": 14, + "heads_returned": true, + "private_data_blank": true, + "mask_semantics": "1=bad, 0=good; increasing MSB-first binary address", + "mask_ascii_sha256": "9af15b336e6a9619928537df30b2e6a2376569fcf9d7e773eccede65606529a0" + }, + { + "address_bits": 3, + "addresses": 8, + "good_addresses": 8, + "bad_addresses": 0, + "read_actions": 168, + "write_actions": 31, + "move_actions": 170, + "total_cell_head_actions": 369, + "visited_cells_including_owned_mask": 20, + "heads_returned": true, + "private_data_blank": true, + "mask_semantics": "1=bad, 0=good; increasing MSB-first binary address", + "mask_ascii_sha256": "7e071fd9b023ed8f18458a73613a0834f6220bd5cc50357ba3493c6040a9ea8c" + } + ], + "negative_controls": { + "semantic_mutants": [ + { + "name": "lower threshold incorrectly strict", + "address": 8, + "correct_bad_bit": "0", + "wrong_bad_bit": "1" + }, + { + "name": "upper threshold incorrectly inclusive", + "address": 24, + "correct_bad_bit": "1", + "wrong_bad_bit": "0" + }, + { + "name": "last differing bit overrides MSB significance", + "address": 10, + "correct_bad_bit": "0", + "wrong_bad_bit": "1" + }, + { + "name": "whole K-bit segment compared to unadjusted K-1-bit thresholds", + "address": 4, + "correct_bad_bit": "1", + "wrong_bad_bit": "0" + } + ], + "ownership_mutants": [ + "owned mask head return omitted" + ], + "counter_mutants": [ + "least significant counter bit omitted" + ], + "unpriced_adapter_rejections": [ + "empty stencil", + "missing interval start", + "missing interval end", + "overlapping source guards", + "incomplete source guard" + ] + }, + "limitations": [ + "Literal transducer starts from admitted ordered finite-alphabet stencil.", + "Geometry/stencil generation and admission are unpriced host adapters, not discharged tape obligations.", + "Observer integers, hashes and source comparisons are outside runtime finite control.", + "No source/E callback exists in the detector interface; keyed work is outside it.", + "No extraction/sort/repair/payload movement, full CRT evaluator or new kappa." + ] +} diff --git a/research/crt-dense-guard-scan/SOURCE-PINS.json b/research/crt-dense-guard-scan/SOURCE-PINS.json new file mode 100644 index 0000000000..f4c01fc0ec --- /dev/null +++ b/research/crt-dense-guard-scan/SOURCE-PINS.json @@ -0,0 +1,20 @@ +[ + { + "path": "research/unconditional-batched-crt/CRT.md", + "size": 15699, + "sha256": "02c3a1e38cbee25aefe2640cc72676da62ba10eb7519fbcb9adb9d48b74eff2b", + "git_blob": "d98dd8e368431cac33d5fc1c8c336696663641d6" + }, + { + "path": "research/unconditional-batched-crt/check_batched_crt.py", + "size": 11520, + "sha256": "681e2e3d71fa74c8b9b326f3860104fd9d89590a222e26ae6ee718d1fd40ff2e", + "git_blob": "1cf78abccd5e06beecc3ed21ba55f7c03b65fdbc" + }, + { + "path": "research/unconditional-batched-crt/NOTICE.md", + "size": 2380, + "sha256": "924109837e71c52392191710d49c9deb42780878d1094f0b01e8690dbe799461", + "git_blob": "886a8fdee275f01b459cbd68ae2815dc9269502f" + } +] diff --git a/research/crt-dense-guard-scan/SOURCES.json b/research/crt-dense-guard-scan/SOURCES.json new file mode 100644 index 0000000000..3cd7684219 --- /dev/null +++ b/research/crt-dense-guard-scan/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65", + "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96" + }, + { + "path": "research/unconditional-batched-crt/CRT.md", + "usage": "input", + "git_blob": "d98dd8e368431cac33d5fc1c8c336696663641d6", + "sha256": "02c3a1e38cbee25aefe2640cc72676da62ba10eb7519fbcb9adb9d48b74eff2b" + }, + { + "path": "research/unconditional-batched-crt/NOTICE.md", + "usage": "input", + "git_blob": "886a8fdee275f01b459cbd68ae2815dc9269502f", + "sha256": "924109837e71c52392191710d49c9deb42780878d1094f0b01e8690dbe799461" + }, + { + "path": "research/unconditional-batched-crt/check_batched_crt.py", + "usage": "input", + "git_blob": "1cf78abccd5e06beecc3ed21ba55f7c03b65fdbc", + "sha256": "681e2e3d71fa74c8b9b326f3860104fd9d89590a222e26ae6ee718d1fd40ff2e" + } + ] +} diff --git a/research/crt-dense-guard-scan/TASK.json b/research/crt-dense-guard-scan/TASK.json new file mode 100644 index 0000000000..d105d91f24 --- /dev/null +++ b/research/crt-dense-guard-scan/TASK.json @@ -0,0 +1,122 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "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": "Lower the retained dense guard classification scan to a literal marker-driven finite-alphabet fixed-inventory transducer on an admitted ordered stencil, including all padded addresses, counter/comparison work, owned mask, cleanup and head returns.", + "scope_change_reason": "The source already proposes a linear scan; actual PR4169/4174 code/proofs leave its tape tariff open. This isolates the executable scanner/cost implication, distinct from predicate/repair algebra, placement, Bene\u0161 compilation and the shared-row caller.", + "bottleneck_link": "Dense detection is a separate O(ML) obligation when record length is only Theta(p); it cannot import a superpolynomial-record tariff or evaluate E on every address. A literal scanner tests that charged component while retaining descriptor and other total-evaluator obligations.", + "budget_minutes": 60, + "stop_rule": "Stop science by2026-10-20T14:02:22Z; reserve final15minutes until14:17:22Z for committed-byte/source-history, cold/hosted verification, refreshed main/overlap and concise handoff. Stop at scanner implication; descriptor construction remains a premise unless separately lowered and charged.", + "outcome": "completed", + "evidence": "PROOF.md gives a uniform admitted-stencil finite-control construction, exact 8ML+15M+13L+18 cell/head actions and M+2L+6 visited cells. RESULT.json executes49408 source addresses/6525207 actions. Separate pre-code oracle, complete pinned mask crosscheck and independent cost review are retained; eight normal/optimized registered checks.", + "author": "ToikY, with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance from primary implementation, separate preimplementation semantic oracle, independent machine-cost reviewer and coordinating agent. No human or formal-kernel acceptance.", + "open_questions": [ + { + "question": "Can the complete CRT caller construct and admit the ordered stencil and classify/extract/repair/reinsert with all remaining numerical and physical work uniformly paid?", + "why_it_matters": "The admitted-stencil mask scanner is one component; it cannot certify geometry generation, E, sparse keys, sorting, movement or callee costs.", + "first_step": "Bind one actual placed-source descriptor plan to a literal encoded stencil builder and mask consumer; account for every construction, transfer, erasure and head return.", + "blocked_by": "Outside this bounded scanner component; unpriced adapter and missing modules remain explicit." + } + ], + "scope_key": "0593fcf1b94f3cd8f1be", + "boundary": { + "inputs": "Admitted ordered fixed-alphabet stencil specifying disjoint active digit and parity-excluded guard comparisons for L address bits; input preserved.", + "output": "Owned one-bit-per-address mask in increasing full binary address order, all M=2^L padded states including arbitrary spectators.", + "private": "Literal finite-inventory counter and bounded control flags; all work and head returns charged and cleanup verified.", + "physical_execution": "Scanner tape actions only; no payload macro, placement or callee." + }, + "obligation_ledger": { + "literal_scanner": "Constructively proved from admitted stencil and executed source-bound finite fixtures; O(ML) time/O(M+L) space. Exact tape actions differ from finite-control bit-machine steps by a parameter-independent factor.", + "geometry_to_stencil_and_admission": "Explicit dependency; host source-binding adapter is unpriced unless actually lowered.", + "full_E_arithmetic_descriptors": "Unknown/outside scope.", + "exception_extract_sort_keys_reinsert_payload_callee": "Outside scope, not zero.", + "precision_native_outer": "Open/outside scope." + }, + "decision": "Narrow to one dense scan implication already requested by complete-tariff handoff; no mechanism expansion or supplier admission.", + "freshness": { + "canonical_main": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "priority_revision": 7, + "checked_at": "2026-10-20T13:40:00Z", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129", + "guidance": "Current-main AGENTS/autoresearch/CONTRIBUTING reread; unchanged from prior round.", + "overlap": { + "open_and_draft_pr_bodies": 315, + "pagination": [ + 100, + 100, + 100, + 15 + ], + "discussion": "Current hub/4173 and focused dense-guard search read live before submission; broader coverage partial.", + "novelty": "No matching body found is not novelty certification.", + "actual_predecessor_heads": { + "4169": "835c3563ee7ede8ceaf329ede7372e50f7823136", + "4174": "5fec853f0c048871de3b8098d1e30d4ee19cda23" + }, + "distinct_new_results": [ + "PR4197 restored compensation forests on older staged3605 words; separate.", + "PR4198 rational Stein/Gaussian coefficient producer; separate." + ] + }, + "canonical_fetch_head_observed_at": "2026-10-20T13:38:19.817803Z", + "decision": "Continue frozen inputs and admitted-stencil scanner; guidance/main/priority/selected unchanged." + }, + "orientation": { + "card_first_example": "scripts/research_baseline.py source-binding orientation", + "same_base_predecessor_round": "Attempted on identical canonical main in round1; stopped because sparse checkout omits historical community-frontier1094-audit/ASSEMBLY.json.", + "scope": "Orientation was not a selected/full native/outer replay and is not claimed successful. Exact unchanged canonical CRT inputs are authenticated by this package. No unrelated historical suite was relaunched." + } +} diff --git a/research/crt-dense-guard-scan/VERIFY.json b/research/crt-dense-guard-scan/VERIFY.json new file mode 100644 index 0000000000..0612a6812d --- /dev/null +++ b/research/crt-dense-guard-scan/VERIFY.json @@ -0,0 +1,111 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/unconditional-batched-crt/CRT.md", + "research/unconditional-batched-crt/NOTICE.md", + "research/unconditional-batched-crt/check_batched_crt.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Source-pinned literal three-tape scan: complete mask, exact action/space invoice, all head returns/private cleanup and actual semantic/counter/ownership mutants." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Source-pinned literal three-tape scan: complete mask, exact action/space invoice, all head returns/private cleanup and actual semantic/counter/ownership mutants." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/independent_guard_oracle.py", + "research/unconditional-batched-crt/check_batched_crt.py" + ], + "timeout_seconds": 120, + "checks": "Preimplementation mathematical interval/source-good/linear_guard oracle, full padded domains, parity/spectator and threshold controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/independent_guard_oracle.py", + "research/unconditional-batched-crt/check_batched_crt.py" + ], + "timeout_seconds": 120, + "checks": "Preimplementation mathematical interval/source-good/linear_guard oracle, full padded domains, parity/spectator and threshold controls." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/cross_check.py", + "{package}", + "." + ], + "timeout_seconds": 120, + "checks": "Pinned actual machine/source adapter against complete independent masks plus generic admitted interval boundary cases." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/cross_check.py", + "{package}", + "." + ], + "timeout_seconds": 120, + "checks": "Pinned actual machine/source adapter against complete independent masks plus generic admitted interval boundary cases." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/cost_check.py" + ], + "timeout_seconds": 120, + "checks": "Separate generic finite-tape opcode/space invoice, finite-control guardrails and an underbilled READ cost fault with unchanged mask/ownership." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/cost_check.py" + ], + "timeout_seconds": 120, + "checks": "Separate generic finite-tape opcode/space invoice, finite-control guardrails and an underbilled READ cost fault with unchanged mask/ownership." + } + ] +} diff --git a/research/crt-dense-guard-scan/cost_check.py b/research/crt-dense-guard-scan/cost_check.py new file mode 100644 index 0000000000..6a6f4eca26 --- /dev/null +++ b/research/crt-dense-guard-scan/cost_check.py @@ -0,0 +1,119 @@ +"""Independent cost/ownership checker; imports the literal kernel, not its verifier. + +Written with substantial OpenAI Codex assistance. Apache-2.0. +Finite checks corroborate the separately written quantified cost derivation. +""" +import argparse +import ast +import hashlib +import json +from pathlib import Path +import sys +import types + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def load_kernel(path): + data = path.read_bytes() + module = types.ModuleType("_independent_literal_guard_cost") + module.__file__ = str(path) + sys.modules[module.__name__] = module + exec(compile(data, str(path), "exec"), module.__dict__) + return module, data + + +def inspect_program(data): + """A structural guardrail, not a complete finite-state formalization.""" + tree = ast.parse(data) + functions = {node.name: node for node in tree.body if isinstance(node, ast.FunctionDef)} + names = ("rewind", "compare_flag", "predicate", "increment_and_return", "erase_counter", "transduce") + forbidden_attributes = {"head", "cells", "actions", "reads", "writes", "moves"} + forbidden_calls = {"len", "range", "enumerate", "int", "sum", "any", "all", "zip"} + for name in names: + need(name in functions, "missing literal program function: " + name) + for node in ast.walk(functions[name]): + if isinstance(node, ast.Attribute): + need(node.attr not in forbidden_attributes, "literal program reads simulator observer: " + node.attr) + if isinstance(node, ast.Call) and isinstance(node.func, ast.Name): + need(node.func.id not in forbidden_calls, "literal program uses host iteration/index helper: " + node.func.id) + return {"functions_inspected": list(names), "observer_accesses": 0, + "scope": "AST guardrail plus manual finite-control review, not a complete program proof"} + + +def run(machine, cells, expected): + stencil = machine.Tape([machine.LEFT] + list(cells) + [machine.END]) + original = list(stencil.cells) + counter, mask = machine.transduce(stencil) + length = len(cells) + records = 1 << length + need(stencil.cells == original, "protected stencil changed") + need(stencil.head == counter.head == mask.head == 0, "head return contract") + need(counter.cells == [machine.LEFT] + [machine.BLANK] * (length + 1), "private blank erasure including end marker") + need(mask.cells == [machine.LEFT] + list(expected) + [machine.END], "complete owned mask/markers") + actual = {"reads": sum(t.reads for t in (stencil, counter, mask)), + "writes": sum(t.writes for t in (stencil, counter, mask)), + "moves": sum(t.moves for t in (stencil, counter, mask))} + wanted = {"reads": (4 * length + 6) * records + 5 * length + 9, + "writes": 3 * records + 2 * length + 1, + "moves": (4 * length + 6) * records + 6 * length + 8} + need(actual == wanted, "independently derived read/write/move invoice") + visited = sum(len(t.cells) for t in (stencil, counter, mask)) + need(visited == records + 2 * length + 6, "exact complete visited space") + return {"L": length, "M": records, **actual, + "actions": sum(actual.values()), "visited_cells": visited, + "mask_sha256": hashlib.sha256(expected.encode()).hexdigest()} + + +def undercharged_read_control(machine): + """Observer-ledger fault: omit one charged READ while preserving semantics.""" + base = machine.Tape + changed = [False] + + class UnderchargedTape(base): + def read(self): + value = super().read() + if not changed[0]: + self.reads -= 1 + changed[0] = True + return value + + machine.Tape = UnderchargedTape + try: + try: + run(machine, [machine.SKIP], "00") + except ValueError as error: + need(str(error) == "independently derived read/write/move invoice", "tariff mutant failed for another reason") + return {"name": "one READ omitted from observer tariff; mask and ownership preserved", "detected_by": str(error)} + raise ValueError("undercharged read accepted") + finally: + machine.Tape = base + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--machine", type=Path, default=Path(__file__).resolve().with_name("machine.py")) + args = parser.parse_args() + machine, data = load_kernel(args.machine) + structural = inspect_program(data) + rows = [] + for length in range(1, 11): + rows.append({"name": "all_skip", **run(machine, [machine.SKIP] * length, "0" * (1 << length))}) + rows.append({"name": "single_cell_digit", **run(machine, [("D", True, True, "0", "0")], "01")}) + rows.append({"name": "single_cell_guard", **run(machine, [("G", True, True, "0", "1")], "01")}) + rows.append({"name": "two_adjacent_single_cell_digits", **run(machine, [("D", True, True, "0", "0")] * 2, "0111")}) + rows.append({"name": "two_cell_MSB_guard", **run(machine, [("G", True, False, "0", "1"), ("G", False, True, "1", "1")], "1001")}) + report = {"result": "PASS_INDEPENDENT_LITERAL_GUARD_COST", + "kernel_sha256": hashlib.sha256(data).hexdigest(), + "cases": len(rows), "complete_addresses": sum(r["M"] for r in rows), + "rows": rows, "structural_guardrail": structural, + "cost_fault_controls": [undercharged_read_control(machine)], + "scope": "Admitted fixed-alphabet stencil only; no construction/admission/E/payload tariff"} + print(json.dumps(report, sort_keys=True, indent=2)) + + +if __name__ == "__main__": + main() diff --git a/research/crt-dense-guard-scan/cross_check.py b/research/crt-dense-guard-scan/cross_check.py new file mode 100644 index 0000000000..31ccfa0dab --- /dev/null +++ b/research/crt-dense-guard-scan/cross_check.py @@ -0,0 +1,161 @@ +"""Independent pinned machine/source cross-check; host oracle has no tariff claim. + +Usage: python3 -I -B cross_check.py PACKAGE REPOSITORY +All publishable output uses logical role names, never local input paths. +""" +import hashlib +import json +from pathlib import Path +import sys +import types + +PINS = { + "machine.py": "1cb27312932914eb631078bd56e85feb1dc6c4191e9d1962b2cc3a7e1cfb8df7", + "verify.py": "40794cd2e2936f0f5e42fac1bb51b65c951a2ab56b7e88824e8c2d09a3dbf40e", + "SOURCE-PINS.json": "e8e5c7320fb0bd1494e063eaa5aaf5f2f08562b80b72750081ea5a409eea5b1e", +} +ORACLE_SHA = "5863cd978de7f81c0627ba6ade29912ea2de99fbd149db8575302f3f10e97a3e" +SOURCE_PINS = { + "research/unconditional-batched-crt/CRT.md": ("02c3a1e38cbee25aefe2640cc72676da62ba10eb7519fbcb9adb9d48b74eff2b", "d98dd8e368431cac33d5fc1c8c336696663641d6"), + "research/unconditional-batched-crt/check_batched_crt.py": ("681e2e3d71fa74c8b9b326f3860104fd9d89590a222e26ae6ee718d1fd40ff2e", "1cf78abccd5e06beecc3ed21ba55f7c03b65fdbc"), + "research/unconditional-batched-crt/NOTICE.md": ("924109837e71c52392191710d49c9deb42780878d1094f0b01e8690dbe799461", "886a8fdee275f01b459cbd68ae2815dc9269502f"), +} + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def digest(data): + return hashlib.sha256(data).hexdigest() + + +def load(name, path, expected): + data = path.read_bytes() + need(digest(data) == expected, "changed input: " + path.name) + module = types.ModuleType(name) + module.__file__ = str(path) + sys.modules[name] = module + exec(compile(data, str(path), "exec"), module.__dict__) + return module + + +def literal(cells, machine, adapter): + adapter.admit_stencil(cells, machine) # Host admission is explicitly unpriced. + original = [machine.LEFT] + list(cells) + [machine.END] + stencil = machine.Tape(original) + counter, output = machine.transduce(stencil) + need(stencil.cells == original, "protected input changed") + need(stencil.head == counter.head == output.head == 0, "head return") + need(counter.cells[0] == machine.LEFT and all(x == machine.BLANK for x in counter.cells[1:]), + "private cells/right marker not blank") + need(output.cells[0] == machine.LEFT and output.cells[-1] == machine.END, "owned output marker") + mask = "".join(output.cells[1:-1]).encode("ascii") + length, records = len(cells), 2 ** len(cells) + need(len(mask) == records and set(mask) <= {48, 49}, "complete binary output length") + roles = (stencil, counter, output) + actions = sum(t.reads + t.writes + t.moves for t in roles) + need(actions == 8 * records * length + 15 * records + 13 * length + 18, "action formula observer") + need(sum(len(t.cells) for t in roles) == records + 2 * length + 6, "visited cell formula") + return mask, actions + + +def source_cases(machine, adapter, oracle, source): + rows = [] + cases = [(shape, 0) for shape in oracle.SHAPES] + cases.append((oracle.Shape("one_target_with_back_spectator", 1, 5, 1, 5, (0,)), 1)) + for shape, back in cases: + # This frozen quotient/remainder oracle predates reading the machine. + # Repeat each base-address decision for every omitted back-bit suffix. + base = oracle.good_mask(shape, source) + expected = bytes(49 - bit for bit in base for _ in range(2 ** back)) + cells = adapter.geometry_stencil(shape.G, shape.H, shape.Y, shape.positions, + shape.K, back, machine) + actual, actions = literal(cells, machine, adapter) + need(actual == expected, "literal output differs from preimplementation interval oracle") + rows.append({"name": shape.name, "addresses": len(expected), "good": expected.count(b"0"), + "bad": expected.count(b"1"), "mask_ascii_sha256": digest(actual), + "observed_actions": actions, "back_skip_bits": back}) + return rows + + +def stencil(length, groups, machine): + cells = [machine.SKIP] * length + for start, width, kind, low, high in groups: + lower = format(low, "0%db" % width) + upper = format(high, "0%db" % width) + for offset in range(width): + need(cells[start + offset] == machine.SKIP, "test descriptor overlap") + cells[start + offset] = (kind, offset == 0, offset == width - 1, + lower[offset], upper[offset]) + return cells + + +def interval_mask(length, groups): + result = bytearray() + for address in range(2 ** length): + accepted = True + for start, width, kind, low, high in groups: + # Independent direct numeric interval extraction, not streaming flags. + value = (address // (2 ** (length - start - width))) % (2 ** width) + accepted = accepted and (value != 2 ** width - 1 if kind == "D" else low <= value < high) + result.append(48 if accepted else 49) + return bytes(result) + + +def generic_cases(machine, adapter): + cases = [] + for length in (1, 2, 3): + cases.append((length, ())) + for width in range(1, length + 1): + for start in range(length - width + 1): + cases.append((length, ((start, width, "D", 0, 0),))) + for low in range(2 ** width): + for high in range(2 ** width): + cases.append((length, ((start, width, "G", low, high),))) + # Adjacent intervals test conjunctive latching, including singleton intervals. + for kind1, kind2 in (("D", "G"), ("G", "D")): + for low in range(4): + for high in range(4): + groups = ((0, 1, "D", 0, 0), (1, 2, "G", low, high)) if kind1 == "D" else ( + (0, 2, "G", low, high), (2, 1, "D", 0, 0)) + cases.append((3, groups)) + combined = hashlib.sha256() + addresses = actions = 0 + for length, groups in cases: + actual, count = literal(stencil(length, groups, machine), machine, adapter) + expected = interval_mask(length, groups) + need(actual == expected, "admitted generic interval semantics mismatch") + combined.update(actual) + addresses += len(actual) + actions += count + return {"cases": len(cases), "addresses": addresses, "combined_mask_ascii_sha256": combined.hexdigest(), + "observed_actions": actions, + "coverage": "L=1..3 all-SKIP; every single D placement; every single G placement/all threshold pairs; adjacent D/G orders"} + + +def main(): + need(len(sys.argv) == 3, "usage: cross_check.py PACKAGE REPOSITORY") + package, repository = map(Path, sys.argv[1:]) + for name, sha in PINS.items(): + need(digest((package / name).read_bytes()) == sha, "changed primary input: " + name) + for path, (sha, blob) in SOURCE_PINS.items(): + data = (repository / path).read_bytes() + need(digest(data) == sha, "changed retained source: " + path) + need(hashlib.sha1(f"blob {len(data)}\0".encode() + data).hexdigest() == blob, "source Git blob mismatch") + oracle = load("_independent_before_machine_guard_oracle", Path(__file__).with_name("independent_guard_oracle.py"), ORACLE_SHA) + source = oracle.load_source(repository / "research/unconditional-batched-crt/check_batched_crt.py") + machine = load("_cross_literal_guard_machine", package / "machine.py", PINS["machine.py"]) + adapter = load("_cross_literal_guard_adapter", package / "verify.py", PINS["verify.py"]) + rows = source_cases(machine, adapter, oracle, source) + generic = generic_cases(machine, adapter) + print(json.dumps({"status": "PASS_INDEPENDENT_LITERAL_GUARD_CROSS_CHECK", "primary_hashes": PINS, + "preimplementation_oracle_sha256": ORACLE_SHA, "source_files_checked": len(SOURCE_PINS), + "source_fixture_addresses": sum(r["addresses"] for r in rows), "source_fixtures": rows, + "generic_stencils": generic, + "scope": "Complete Boolean output/ownership cross-check; source predicate projections, not production placement; geometry/admission and oracle are unpriced host work."}, sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/crt-dense-guard-scan/independent_guard_oracle.py b/research/crt-dense-guard-scan/independent_guard_oracle.py new file mode 100644 index 0000000000..caf8fc874e --- /dev/null +++ b/research/crt-dense-guard-scan/independent_guard_oracle.py @@ -0,0 +1,179 @@ +"""Separate interval oracle for the source dense guard, before primary read. + +Complete numeric U|T|Y address order; host arithmetic is semantic only. +The fixtures are source-predicate projections, not three-reservoir callers. +""" +from dataclasses import dataclass +import hashlib +import json +from pathlib import Path +import sys +import types + + +SOURCE_SHA256 = "681e2e3d71fa74c8b9b326f3860104fd9d89590a222e26ae6ee718d1fd40ff2e" + + +@dataclass(frozen=True) +class Shape: + name: str + G: int + K: int + H: int + Y: int + positions: tuple[int, ...] + + @property + def L(self): + return 2 * self.H + self.Y + + +SHAPES = (Shape("two_active_digits", 1, 5, 2, 10, (0, 5)), + Shape("single_with_dirty_spectators", 2, 7, 3, 9, (1,))) + + +def split(address, shape): + controls, y = divmod(address, 2 ** shape.Y) + u, t = divmod(controls, 2 ** shape.H) + return u, t, y + + +def pack(u, t, y, shape): + return (u * (2 ** shape.H) + t) * (2 ** shape.Y) + y + + +def interval_good(u, t, y, shape, *, lower_strict=False, upper_inclusive=False, + mix_target_parity=False, ignore_upper_active=False): + base = 2 ** shape.G + count = len(shape.positions) + active_digits = range(1 if ignore_upper_active else count) + for i in active_digits: + if (u // (base ** i)) % base == base - 1: + return False + if (t // (base ** i)) % base == base - 1: + return False + lower = 2 * base + upper = 2 ** (shape.K - 1) - lower + for position in shape.positions: + value = (y // (2 ** (position + 1))) % (2 ** (shape.K - 1)) + if mix_target_parity: + value += (y // (2 ** position)) % 2 + if not (value > lower if lower_strict else value >= lower): + return False + if not (value <= upper if upper_inclusive else value < upper): + return False + return True + + +def load_source(path): + path = Path(path) + data = path.read_bytes() + if hashlib.sha256(data).hexdigest() != SOURCE_SHA256: + raise ValueError("retained guard source changed") + module = types.ModuleType("_guard_retained_source") + module.__file__ = str(path) + sys.modules[module.__name__] = module + exec(compile(data, str(path), "exec"), module.__dict__) + return module + + +def good_mask(shape, source=None): + accepted = bytearray() + for address in range(1 << shape.L): + u, t, y = split(address, shape) + expected = interval_good(u, t, y, shape) + if source is not None: + actual = source.good(u, t, y, bits=shape.G, positions=shape.positions, guard=shape.K) + linear = source.linear_guard(u, t, y, bits=shape.G, positions=shape.positions, + guard=shape.K, control_bits=shape.H, ybits=shape.Y) + if actual != expected or linear != expected: + raise ValueError("source predicate or source bit scan differs from interval oracle") + accepted.append(int(expected)) + return bytes(accepted) + + +def boundary_checks(shape): + base = 2 ** shape.G + low = 2 * base + high = 2 ** (shape.K - 1) - low + initial_y = sum(low * (2 ** (p + 1)) for p in shape.positions) + checks = [] + for position in shape.positions: + for value, expected in ((low - 1, False), (low, True), + (high - 1, True), (high, False)): + y = initial_y + (value - low) * (2 ** (position + 1)) + if interval_good(0, 0, y, shape) != expected: + raise ValueError("interval boundary error") + checks.append({"position": position, "guard_value": value, "good": expected}) + return checks + + +def inspect(shape, source): + mask = good_mask(shape, source) + ignored = [("target_parity", p) for p in shape.positions] + for bit in range(len(shape.positions) * shape.G, shape.H): + ignored.append(("inactive_u", shape.Y + shape.H + bit)) + ignored.append(("inactive_t", shape.Y + bit)) + occupied = {q for p in shape.positions for q in range(p, p + shape.K)} + ignored.extend(("Y_spectator", q) for q in range(shape.Y) if q not in occupied) + toggles = 0 + for address, accepted in enumerate(mask): + for _, bit in ignored: + if mask[address ^ (1 << bit)] != accepted: + raise ValueError("dirty spectator or target parity affected guard") + toggles += 1 + ascii_good = bytes(48 + bit for bit in mask) + ascii_bad = bytes(49 - bit for bit in mask) + return {"name": shape.name, "G": shape.G, "K": shape.K, "H": shape.H, + "Y": shape.Y, "positions": list(shape.positions), "L": shape.L, + "addresses": len(mask), "good": sum(mask), "bad": len(mask) - sum(mask), + "good_mask_binary_sha256": hashlib.sha256(mask).hexdigest(), + "good_mask_ascii_sha256": hashlib.sha256(ascii_good).hexdigest(), + "bad_mask_ascii_sha256": hashlib.sha256(ascii_bad).hexdigest(), + "ignored_bit_invariance_toggles": toggles, + "ignored_bits": [{"role": role, "numeric_address_bit": bit} for role, bit in ignored], + "boundaries": boundary_checks(shape), + "domain": "complete U|T|Y source predicate projection; no back reservoir/payload permutation"} + + +def mutations(): + shape = SHAPES[0] + witnesses = {} + for label, options in (("strict_lower", {"lower_strict": True}), + ("inclusive_upper", {"upper_inclusive": True}), + ("target_parity_in_guard", {"mix_target_parity": True}), + ("ignore_upper_active_digit", {"ignore_upper_active": True})): + for address in range(1 << shape.L): + u, t, y = split(address, shape) + expected = interval_good(u, t, y, shape) + wrong = interval_good(u, t, y, shape, **options) + if expected != wrong: + witnesses[label] = {"address": address, "u": u, "t": t, "y": y, + "expected_good": expected, "wrong_good": wrong} + break + else: + raise ValueError("semantic mutation did not fail: " + label) + dirty = SHAPES[1] + y = 2 * (2 ** dirty.G) * (2 ** (dirty.positions[0] + 1)) + if not interval_good(4, 0, y, dirty) or interval_good(3, 0, y, dirty): + raise ValueError("inactive/active upper-control distinction failed") + witnesses["dirty_inactive_upper_control"] = {"u": 4, "t": 0, "y": y, + "expected_good": True, + "zero_initialization_assumption_wrong": False} + return witnesses + + +def main(): + source = load_source(sys.argv[1]) + rows = [inspect(shape, source) for shape in SHAPES] + if [row["good"] for row in rows] != [256, 13824]: + raise ValueError("independently counted accepted cardinality mismatch") + print(json.dumps({"status": "PASS_PREIMPLEMENTATION_DENSE_GUARD_ORACLE", + "source_sha256": SOURCE_SHA256, "fixtures": rows, + "negative_controls": mutations(), + "scope": "complete Boolean masks and boundary/dirty-coordinate controls; no sequential/tape tariff"}, + sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/crt-dense-guard-scan/machine.py b/research/crt-dense-guard-scan/machine.py new file mode 100644 index 0000000000..ce763898bd --- /dev/null +++ b/research/crt-dense-guard-scan/machine.py @@ -0,0 +1,169 @@ +"""Three fixed tape roles and a marker-driven, finite-control guard program. + +Tape.head and read/write/move totals are SIMULATOR OBSERVERS. The program +below never reads them, a tape length, or a host L/M/position counter. +Stencil atoms form a fixed finite product alphabet, independent of geometry. +""" + +LEFT, END, BLANK = "<", ">", "_" +SKIP = ("S", False, False, "0", "0") + + +class Tape: + """One cell/head operation per method; permanently marked left boundary.""" + + def __init__(self, cells=None): + self.cells = [LEFT] if cells is None else list(cells) + self.head = 0 + self.reads = self.writes = self.moves = 0 + + def read(self): + self.reads += 1 + return self.cells[self.head] + + def write(self, symbol): + self.writes += 1 + self.cells[self.head] = symbol + + def move(self, direction): + # Only the emulator uses a numerical head coordinate. The program + # emits one LEFT/RIGHT action and branches only on the read symbol. + if direction not in (-1, 1): + raise ValueError("one-cell direction") + self.moves += 1 + self.head += direction + if self.head < 0: + raise ValueError("crossing permanent left boundary") + if self.head == len(self.cells): + self.cells.append(BLANK) # Initially blank infinite tape cell. + + @property + def actions(self): + return self.reads + self.writes + self.moves + + +def rewind(tape): + while tape.read() != LEFT: + tape.move(-1) + + +def compare_flag(flag, bit, threshold, last_difference_wins): + """L/E/G are three finite control states; all arguments have finite range.""" + if bit == threshold: + return flag + if flag == "E" or last_difference_wins: + return "L" if bit == "0" else "G" + return flag + + +def predicate(stencil, counter, lower_strict, upper_inclusive, last_difference_wins): + good = True + all_ones = False + lower = upper = "E" + active = "S" + stencil.move(1) + counter.move(1) + while True: + token = stencil.read() + if token == END: + if active != "S": + raise ValueError("unterminated admitted interval") + return good + bit = counter.read() + if bit not in ("0", "1"): + raise ValueError("counter/stencil alignment") + # Tuple fields decode one atom of a FIXED finite alphabet. They do + # not index a parameter-sized geometry table or interval collection. + kind, begin, end, lower_bit, upper_bit = token + if kind == "D": + if begin: + active = "D" + all_ones = True + all_ones = all_ones and bit == "1" + if end: + good = good and not all_ones + active = "S" + all_ones = False + elif kind == "G": + if begin: + active = "G" + lower = upper = "E" + lower = compare_flag(lower, bit, lower_bit, last_difference_wins) + upper = compare_flag(upper, bit, upper_bit, last_difference_wins) + if end: + lower_ok = lower == "G" if lower_strict else lower != "L" + upper_ok = upper != "G" if upper_inclusive else upper == "L" + good = good and lower_ok and upper_ok + lower = upper = "E" + active = "S" + stencil.move(1) + counter.move(1) + + +def increment_and_return(counter, skip_low_counter_bit): + """Counter starts at END; overflow returns False at permanent LEFT.""" + counter.move(-1) + if skip_low_counter_bit: + counter.move(-1) + while True: + bit = counter.read() + if bit == "1": + counter.write("0") + counter.move(-1) + elif bit == "0": + counter.write("1") + rewind(counter) + return True + elif bit == LEFT: + return False + else: + raise ValueError("binary carry alphabet") + + +def erase_counter(counter): + """Restore private data to BLANK, including its allocated END marker.""" + counter.move(1) + while True: + symbol = counter.read() + counter.write(BLANK) + if symbol == END: + break + counter.move(1) + rewind(counter) + + +def transduce(stencil, lower_strict=False, upper_inclusive=False, + last_difference_wins=False, omit_output_return=False, + skip_low_counter_bit=False): + """Admitted stencil -> protected stencil, blank private work, owned BAD mask. + + The booleans select fixed mutation programs for verification. The normal + transducer has all False. There is no function/E-evaluator callback. + """ + counter, mask = Tape(), Tape() # Two fixed roles, reused throughout. + stencil.move(1) + counter.move(1) + while True: + symbol = stencil.read() + if symbol == END: + counter.write(END) + break + counter.write("0") + stencil.move(1) + counter.move(1) + rewind(stencil) + rewind(counter) + mask.move(1) + while True: + good = predicate(stencil, counter, lower_strict, upper_inclusive, last_difference_wins) + mask.write("0" if good else "1") + mask.move(1) + rewind(stencil) + if not increment_and_return(counter, skip_low_counter_bit): + break + erase_counter(counter) + mask.write(END) + if not omit_output_return: + rewind(mask) + # A fixed final control state replaces all transient finite flags. + return counter, mask diff --git a/research/crt-dense-guard-scan/verify.py b/research/crt-dense-guard-scan/verify.py new file mode 100644 index 0000000000..2f221b5678 --- /dev/null +++ b/research/crt-dense-guard-scan/verify.py @@ -0,0 +1,226 @@ +"""Source binding and observer audit of the literal dense guard-mask program. + +Geometry-to-stencil construction/admission and source-oracle computations below +are host adapters, explicitly OUTSIDE the transducer's machine tariff. +""" + +import argparse +import hashlib +import json +from pathlib import Path +import sys +import types + + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def load_bytes(name, data, path): + module = types.ModuleType(name) + module.__file__ = str(path) + sys.modules[name] = module + exec(compile(data, str(path), "exec"), module.__dict__) + return module + + +def admit_stencil(cells, machine): + """Host admission only, not a claimed tape implementation or charged step.""" + need(len(cells) >= 1, "nonempty stencil") + active = None + for atom in cells: + need(type(atom) is tuple and len(atom) == 5, "fixed product alphabet") + kind, begin, end, lo, hi = atom + need(kind in ("S", "D", "G") and type(begin) is bool and type(end) is bool + and lo in ("0", "1") and hi in ("0", "1"), "finite alphabet atom") + if kind == "S": + need(atom == machine.SKIP and active is None, "skip outside intervals") + continue + if begin: + need(active is None, "nonoverlapping ordered interval start") + active = kind + else: + need(active == kind, "interval continuation") + if kind == "D": + need(lo == hi == "0", "digit has no threshold data") + if end: + active = None + need(active is None, "complete intervals") + return cells + + +def geometry_stencil(g, h, ybits, targets, k, back_bits, machine, include_parity=False): + """Unpriced source-binding adapter; preserves all unspecified bits as SKIP.""" + targets = tuple(targets) + need(all(type(v) is int for v in (g, h, ybits, k, back_bits)), "integer geometry") + need(g >= 1 and targets and h >= len(targets) * g and k >= g + 4 and back_bits >= 0, + "admissible compact/guard widths") + need(all(type(j) is int and 0 <= j and j + k <= ybits for j in targets), "complete target intervals") + intervals = sorted((j, j + k) for j in targets) + need(all(a[1] <= b[0] for a, b in zip(intervals, intervals[1:])), "disjoint target intervals") + length = 2 * h + ybits + back_bits + cells = [machine.SKIP] * length + + def place(lo, hi, kind, low=0, high=0): + width = hi - lo + low_bits = format(low, "0%db" % width) + high_bits = format(high, "0%db" % width) + need(width >= 1 and len(low_bits) == len(high_bits) == width, "fixed threshold widths") + for offset, position in enumerate(range(lo, hi)): + need(cells[position] == machine.SKIP, "no overlapping stencil cells") + cells[position] = (kind, offset == 0, offset == width - 1, + low_bits[offset], high_bits[offset]) + + for field_start in (0, h): + for digit in range(len(targets)): + place(field_start + h - (digit + 1) * g, field_start + h - digit * g, "D") + for j in targets: + # The source compares K-1 HIGHER guard bits, excluding parity bit j. + start = 2 * h + ybits - j - k + stop = 2 * h + ybits - j - (0 if include_parity else 1) + place(start, stop, "G", 1 << (g + 1), (1 << (k - 1)) - (1 << (g + 1))) + return admit_stencil(cells, machine) + + +def audit(cells, machine, **mutant): + """Observer integers are not read by the literal transducer.""" + admit_stencil(cells, machine) + stencil = machine.Tape([machine.LEFT] + cells + [machine.END]) + original = list(stencil.cells) + counter, mask = machine.transduce(stencil, **mutant) + length, records = len(cells), 1 << len(cells) + need(stencil.cells == original, "protected stencil unchanged") + need(counter.head == stencil.head == 0, "private/input heads returned") + need(counter.cells[0] == machine.LEFT and all(c == machine.BLANK for c in counter.cells[1:]), + "private counter restored to blank data, including right marker") + need(mask.cells[0] == machine.LEFT and mask.cells[-1] == machine.END, + "owned output markers") + bits = "".join(mask.cells[1:-1]) + need(len(bits) == records and all(bit in "01" for bit in bits), "one BAD bit per complete address") + actions = sum(t.actions for t in (stencil, counter, mask)) + if not mutant: + need(mask.head == 0, "owned output head returned") + need(actions == 8 * records * length + 15 * records + 13 * length + 18, + "derived exact marker/counter/cleanup action census") + need(sum(len(t.cells) for t in (stencil, counter, mask)) == records + 2 * length + 6, + "derived exact three-role visited space") + return bits, {"address_bits": length, "addresses": records, + "good_addresses": bits.count("0"), "bad_addresses": bits.count("1"), + "read_actions": sum(t.reads for t in (stencil, counter, mask)), + "write_actions": sum(t.writes for t in (stencil, counter, mask)), + "move_actions": sum(t.moves for t in (stencil, counter, mask)), + "total_cell_head_actions": actions, + "visited_cells_including_owned_mask": sum(len(t.cells) for t in (stencil, counter, mask)), + "heads_returned": mask.head == counter.head == stencil.head == 0, + "private_data_blank": True, + "mask_semantics": "1=bad, 0=good; increasing MSB-first binary address", + "mask_ascii_sha256": hashlib.sha256(bits.encode()).hexdigest()} + + +def fixture(name, g, h, ybits, targets, k, back_bits, source, machine): + cells = geometry_stencil(g, h, ybits, targets, k, back_bits, machine) + mask, receipt = audit(cells, machine) + for address, bit in enumerate(mask): + y = (address >> back_bits) & ((1 << ybits) - 1) + t = (address >> (ybits + back_bits)) & ((1 << h) - 1) + u = address >> (h + ybits + back_bits) + expected = source.good(u, t, y, bits=g, positions=targets, guard=k) + linear = source.linear_guard(u, t, y, bits=g, positions=targets, guard=k, + control_bits=h, ybits=ybits) + need(expected == linear == (bit == "0"), "literal mask equals exact source predicates on every address") + receipt.update({"name": name, "G": g, "H": h, "Y_bits": ybits, + "targets": list(targets), "K": k, "back_skip_bits": back_bits, + "domain": "predicate projection/stencil fixture, not a full production reservoir invocation"}) + return receipt, cells, mask + + +def must_reject(call, label): + try: + call() + except ValueError: + return label + raise ValueError("admission control accepted: " + label) + + +def controls(machine): + cells = geometry_stencil(1, 1, 5, (0,), 5, 0, machine) + right, _ = audit(cells, machine) + mutants = [] + for name, kwargs in (("lower threshold incorrectly strict", {"lower_strict": True}), + ("upper threshold incorrectly inclusive", {"upper_inclusive": True}), + ("last differing bit overrides MSB significance", {"last_difference_wins": True})): + wrong, _ = audit(cells, machine, **kwargs) + different = next((i for i, (a, b) in enumerate(zip(right, wrong)) if a != b), None) + need(different is not None, "semantic mutant differs: " + name) + mutants.append({"name": name, "address": different, + "correct_bad_bit": right[different], "wrong_bad_bit": wrong[different]}) + wrong_cells = geometry_stencil(1, 1, 5, (0,), 5, 0, machine, include_parity=True) + wrong, _ = audit(wrong_cells, machine) + different = next(i for i, (a, b) in enumerate(zip(right, wrong)) if a != b) + mutants.append({"name": "whole K-bit segment compared to unadjusted K-1-bit thresholds", + "address": different, "correct_bad_bit": right[different], "wrong_bad_bit": wrong[different]}) + _, missing_return = audit(cells, machine, omit_output_return=True) + need(not missing_return["heads_returned"], "missing owned-mask return detected") + return {"semantic_mutants": mutants, "ownership_mutants": ["owned mask head return omitted"], + "counter_mutants": [must_reject(lambda: audit(cells, machine, skip_low_counter_bit=True), + "least significant counter bit omitted")], + "unpriced_adapter_rejections": [ + must_reject(lambda: admit_stencil([], machine), "empty stencil"), + must_reject(lambda: admit_stencil([("D", False, True, "0", "0")], machine), "missing interval start"), + must_reject(lambda: admit_stencil([("G", True, False, "0", "1")], machine), "missing interval end"), + must_reject(lambda: geometry_stencil(1, 2, 10, (0, 4), 5, 0, machine), "overlapping source guards"), + must_reject(lambda: geometry_stencil(1, 1, 4, (0,), 5, 0, machine), "incomplete source guard"), + ]} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write-result", action="store_true") + args = parser.parse_args() + pins = json.loads((PACKAGE / "SOURCE-PINS.json").read_text()) + authenticated = {} + for row in pins: + data = (ROOT / row["path"]).read_bytes() + need(hashlib.sha256(data).hexdigest() == row["sha256"], "source SHA256: " + row["path"]) + need(hashlib.sha1(f"blob {len(data)}\0".encode() + data).hexdigest() == row["git_blob"], + "source Git blob: " + row["path"]) + authenticated[row["path"]] = data + path = "research/unconditional-batched-crt/check_batched_crt.py" + source = load_bytes("_guard_source", authenticated[path], ROOT / path) + machine = load_bytes("_literal_guard_machine", (PACKAGE / "machine.py").read_bytes(), PACKAGE / "machine.py") + rows = [] + for name, g, h, y, targets, k, w in ( + ("two_target_complete", 1, 2, 10, (0, 5), 5, 0), + ("inactive_digits_and_Y_spectators", 2, 3, 9, (1,), 7, 0), + ("one_target_with_back_spectator", 1, 1, 5, (0,), 5, 1)): + receipt, _, _ = fixture(name, g, h, y, targets, k, w, source, machine) + rows.append(receipt) + all_skip = [] + for length in (1, 2, 3): + mask, receipt = audit([machine.SKIP] * length, machine) + need(set(mask) == {"0"}, "all-skip stencil accepts every address") + all_skip.append(receipt) + result = {"schema_version": 1, "result": "PASS_LITERAL_DENSE_GUARD_MASK", + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", "source_inputs_checked": len(authenticated), + "fixtures": rows, "all_skip_boundaries": all_skip, "negative_controls": controls(machine), + "limitations": ["Literal transducer starts from admitted ordered finite-alphabet stencil.", + "Geometry/stencil generation and admission are unpriced host adapters, not discharged tape obligations.", + "Observer integers, hashes and source comparisons are outside runtime finite control.", + "No source/E callback exists in the detector interface; keyed work is outside it.", + "No extraction/sort/repair/payload movement, full CRT evaluator or new kappa."]} + output = PACKAGE / "RESULT.json" + if args.write_result: + output.write_text(json.dumps(result, indent=2) + "\n") + else: + need(json.loads(output.read_text()) == result, "stored receipt differs from replay") + print(json.dumps({"result": result["result"], "source_addresses": sum(r["addresses"] for r in rows), + "tape_actions": sum(r["total_cell_head_actions"] for r in rows)}, sort_keys=True)) + + +if __name__ == "__main__": + main()