Repository navigation
Conversation
Contributor
|
Independent scoped audit of the uniform Beneš charged arena-scan package at Code-disjoint reimplementation; does not import package Defect (P1):
What passes (16 of 16 with P1 asserting the defect):
Not covered: live arena re-execution; full CRT evaluator; production placement; new κ. This is a finite replay of committed receipts, not a formal proof. Suggested fix: refresh COLD/COST README seals (or record a metadata-only addendum). check_4192.py#!/usr/bin/env python3
"""Independent finite controls for PR4192 (uniform Beneš charged arena scans).
Recomputes COST-REVIEW exact arena formulas on RESULT cases and seals.
Does not import package verify.py / cross_check.py / independent_benes_oracle.py.
Package head 519d811cc48693ad9969d6d7994bef3940167005 via GitHub API.
James Reed (@rcfc-jreed), with substantial AI assistance (Claude, in Cursor).
Apache-2.0.
"""
from __future__ import annotations
import argparse, hashlib, json, sys
from pathlib import Path
HEAD = "519d811cc48693ad9969d6d7994bef3940167005"
BASE = "12fa8c5c844be21bfefb38a19503fbd867a11244"
results = []
def check(name, ok, detail=""):
results.append((name, bool(ok), detail))
print(("PASS " if ok else "FAIL ") + name + ((": " + str(detail)) if detail else ""), flush=True)
return bool(ok)
def load(pkg, name):
return json.loads((pkg / name).read_text(encoding="utf-8"))
def sha(path: Path):
return hashlib.sha256(path.read_bytes()).hexdigest()
def auth_sources(sources, deps: Path):
bad, count = [], 0
for row in sources["files"]:
if row["usage"] != "input":
continue
data = (deps / row["path"]).read_bytes()
if hashlib.sha256(data).hexdigest() != row["sha256"]:
bad.append(row["path"]); continue
blob = b"blob " + str(len(data)).encode() + b"\0" + data
if hashlib.sha1(blob).hexdigest() != row["git_blob"]:
bad.append(row["path"] + ":blob"); continue
count += 1
return count, bad
def case_formulas(c):
"""Exact formulas from COST-REVIEW.primary_bound_checked."""
h, N = c["h"], c["wires"]
w = c["record_width_bits"]
expect_N = 1 << h
arena_records = N * (h * h + 3 * h + 1)
logical = N * N + 2 * N * h * h + (37 * N * h - 35 * N) // 2
init = 6 * c["arena_cells"]
return {
"wires": N == expect_N,
"arena_records": c["arena_records"] == arena_records,
"arena_cells": c["arena_cells"] == arena_records * w,
"logical": c["logical_accesses"] == logical,
"input_tape": c["input_tape_actions"] == 3 * c["input_bits"],
"output_tape": c["owned_output_tape_actions"] == 3 * c["owned_output_bits"],
"init": c["arena_initialization_cleanup_actions"] == init,
"total": c["arena_and_key_tape_actions"]
== c["arena_and_key_scan_actions"] + c["arena_initialization_cleanup_actions"],
"get_put": c["get_calls"] + c["put_calls"] == c["logical_accesses"],
"dfs": c["dfs_pushes"] == c["dfs_pops"],
"heads": c["private_arena_erased"] and c["private_heads_returned"],
}
def run(pkg: Path, deps: Path):
sources = load(pkg, "SOURCES.json")
verify = load(pkg, "VERIFY.json")
result = load(pkg, "RESULT.json")
cost = load(pkg, "COST-REVIEW.json")
cross = load(pkg, "CROSS-CHECK.json")
cold = load(pkg, "COLD-REPLAY.json")
initial = load(pkg, "INITIAL-REVIEW.json")
check("I1 base_commit pins == 12fa8c5c…",
sources["base_commit"] == BASE == result["base_commit"]
== cost["base_commit"] == cold["base_commit"])
check("I2 RESULT PASS_UNIFORM_BENES_SCAN_COMPONENT; VERIFY ready; reviews PASS",
result["result"] == "PASS_UNIFORM_BENES_SCAN_COMPONENT"
and verify["status"] == "ready"
and cost["status"] == "PASS_INDEPENDENT_COST_ENCODING_OWNERSHIP_REVIEW"
and cross["status"] == "PASS_INDEPENDENT_PRIMARY_CROSSCHECK"
and cold["status"] == "PASS_COLD_REGISTERED_REPLAY"
and initial["status"] == "PASS_PREIMPLEMENTATION_INDEPENDENT_REVIEW")
n_in, bad = auth_sources(sources, deps)
check("S1 SOURCES input files authenticate (sha256 + git blob)",
not bad and n_in == result["source_inputs_checked"] == 3, bad)
cold_bad = [k for k, dig in cold["reviewed_hashes"].items() if sha(pkg / k) != dig]
cost_bad = [Path(row["path"]).name for row in cost["primary_files_reviewed"]
if sha(pkg / Path(row["path"]).name) != row["sha256"]]
# Packaging defect: README.md edited after COLD/COST seals without rebind / addendum.
check("P1 COLD+COST seals: only README.md stale (packaging defect)",
cold_bad == ["README.md"] and cost_bad == ["README.md"],
{"cold_stale": cold_bad, "cost_stale": cost_bad,
"sealed_readme": cold["reviewed_hashes"]["README.md"],
"actual_readme": sha(pkg / "README.md")})
cross_bad = [k for k, dig in cross["files"].items() if sha(pkg / k) != dig]
check("P2 CROSS file seals match package bytes", not cross_bad, cross_bad)
check("P3 non-README COLD seals (PROOF/RESULT/SOURCE-PINS/verify) match",
all(sha(pkg / k) == dig for k, dig in cold["reviewed_hashes"].items() if k != "README.md"))
check("P4 COST review_file + replay_helper seals; CROSS oracle/primary bind",
sha(pkg / "INDEPENDENT-COST-REVIEW.md") == cost["review_file"]["sha256"]
and sha(pkg / "replay_primary.py") == cost["replay_helper"]["sha256"]
and cross["runs"][0]["receipt"]["oracle_sha256"] == sha(pkg / "independent_benes_oracle.py")
and cross["runs"][0]["receipt"]["primary_sha256"] == sha(pkg / "verify.py")
and cost["review_findings"]["material_defects_remaining"] == [])
fin = result["finite"]
cats = fin["categories"]
check("F1 cases=49 = 26+20+2+1 categories; receipt sha present",
fin["cases"] == 49 == sum(cats.values())
and cats == {"all_permutations": 26, "modular_rotation": 20,
"arbitrary": 2, "wider_parameter": 1}
and len(fin["receipt_sha256"]) == 64)
check("F2 aggregate: 284 endpoints, 1260 queries, 15984 logical, max arena 55680",
fin["permutation_endpoints"] == 284
and fin["queried_control_bits"] == 1260
and fin["logical_accesses"] == 15984
and fin["maximum_arena_cells"] == 55680
and fin["maximum_dfs_entries"] == 2
and fin["records_scanned"] == 3583480
and fin["arena_and_key_tape_actions"] == 2102126536)
large, wide = fin["largest_case"], fin["wider_parameter_case"]
bad_l = {k: v for k, v in case_formulas(large).items() if not v}
bad_w = {k: v for k, v in case_formulas(wide).items() if not v}
check("F3 largest_case exact COST formulas (arena_records=N(h²+3h+1), logical, 3·bits, init=6·cells)",
not bad_l, bad_l)
check("F4 wider_parameter_case exact COST formulas",
not bad_w, bad_w)
check("F5 largest: h=4,N=16,w=120 → 464 records / 55680 cells / 1672 logical / 485441472 tape",
large["h"] == 4 and large["wires"] == 16 and large["arena_records"] == 464
and large["arena_cells"] == 55680 and large["logical_accesses"] == 1672
and large["arena_and_key_tape_actions"] == 485441472)
check("C1 CROSS dual runs PASS: 37 cases, 848 queries, 200 endpoint columns",
all(r["exit_code"] == 0
and r["receipt"]["status"] == "PASS_PRIMARY_VS_PREIMPLEMENTATION_ORACLE"
and r["receipt"]["cases"] == 37
and r["receipt"]["control_queries"] == 848
for r in cross["runs"]))
check("C2 COLD/COST replays echo RESULT cases=49, logical_accesses=15984",
all(r["exit_code"] == 0 and r["receipt"]["cases"] == 49
and r["receipt"]["logical_accesses"] == 15984 for r in cold["runs"])
and all(r["exit_code"] == 0 and r["stdout"]["cases"] == 49
and r["stdout"]["logical_accesses"] == 15984 for r in cost["replays"]))
check("N1 seven negative_controls; limitations exclude full CRT / new kappa",
len(result["negative_controls"]) == 7
and any("new kappa" in x.lower() for x in result["limitations"])
and any("Bene" in x for x in result["limitations"]))
failed = [name for name, ok, _ in results if not ok]
print(f"\n{len(results) - len(failed)}/{len(results)} PASS", flush=True)
if failed:
print("FAILED:", ", ".join(failed), flush=True)
return 1
return 0
def main():
ap = argparse.ArgumentParser()
ap.add_argument("--pkg", required=True)
ap.add_argument("--deps", required=True)
ap.add_argument("--expect-head", default=HEAD)
args = ap.parse_args()
check("HEAD pin recorded (API fetch)", args.expect_head == HEAD, args.expect_head)
return run(Path(args.pkg), Path(args.deps))
if __name__ == "__main__":
sys.exit(main())James Reed (@rcfc-jreed), with substantial AI assistance (Claude, in Cursor). |
This was referenced Oct 20, 2026
Contributor
|
Independent scoped audit of #4192 Beneš charged arena scans at Code-disjoint checks; package-local forks of No packaging defect in SOURCES scope. All 5 digests match. What passes: sealed Not covered here: Finite pin/seal/Beneš-scan replay ≠ formal proof. James Reed (@rcfc-jreed), with substantial AI assistance (Claude, in Cursor). |
This was referenced Oct 21, 2026
This was referenced Oct 22, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This isolates the Beneš compiler/query component of Cinna Davis’s PR4100 CRT.md §2. For a canonically encoded permutation on N=2^h wires with1<=h<=p, the written uniform lowering has O(N³(p+2)^7) time and O(N(p+2)^3) visited space. It preserves the source, serializes an owned network, clears private workspace and returns heads on fixed reusable tape roles.
The implementation flattens recursion, stores the DFS stack in a tagged arena, and performs a complete scan and return for every logical get/put. The proof derives exact record count N(h²+3h+1), access count N²+2Nh²+(37Nh−35N)/2, and tape-action invoices. Python scalar/header operations are lowered in the written proof; the executed arena/key model is not a complete finite-state transition-table certificate. The original cycle compiler and full-scan proposal remain credited predecessor work.
All six registered normal/optimized commands passed. Primary49cases reproduce the exact retained tables and1,260queries, with15,984logicalaccesses and3,583,480record scans. Contiguous tape macros are checked against expanded one-cell execution. The separately written preimplementation FIFO oracle checks40,394permutations/324,452endpoint columns/1,630,756controls; a hash-pinned direct cross-check adds37cases/848queries. Semantic/admission/head-return controls detect their intended faults. Exact committed bytes and declared source ancestry pass.
This takes the encoded permutation as input. Full CRT reconstruction/modular inversion, parameter and split-descriptor construction, macro forward/inverse keys, complete E evaluation, production placement, ordinary callee, precision/native/outer theorem remain separate. No new κ or frontier change. README/TASK record a concrete full-evaluator follow-up.
Base/current canonical main12fa8c5c844be21bfefb38a19503fbd867a11244, priority7; task uniform-transfer-audit refined to this component. Live handoffs and focused evaluator Discussions plus309 open/draft PR bodies checked; broader Discussion/closed/code coverage partial. Distinct from PR4174 placement, PR4169 repair, PR4187 tail, and completed PR4186 Gaussian solve. Claim: #4173 (comment)
Credit Cinna Davis’s PR4100 (337d049), Hiroki KUMAZAKI’s PR4174 context, Douglas Colkitt/OpenAI framework and complete retained NOTICE lineage. ToikY with substantial OpenAI Codex assistance; separate-agent review is not independent human or proof-assistant acceptance. New work Apache-2.0. Maintainer edits disabled; no merge requested.
Reproduce: