Skip to content

Lower admitted-stencil CRT guard scan to a literal three-tape program #4201

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
Mister-Meeseeks merged 1 commit into from
Oct 21, 2026
Merged

Lower admitted-stencil CRT guard scan to a literal three-tape program #4201

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
181 changes: 181 additions & 0 deletions research/crt-dense-guard-scan/COST-CHECK-RESULT.json
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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"
}
}
135 changes: 135 additions & 0 deletions research/crt-dense-guard-scan/CROSS-REPLAY.json
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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"
}
46 changes: 46 additions & 0 deletions research/crt-dense-guard-scan/EVIDENCE.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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.
Loading