Repository navigation
Bind mixed-provider precision to the rounded Gaussian tensor caller - #4178
jmbarrancoml wants to merge 2 commits into
Conversation
|
Independent scoped audit of the Gaussian height-contract / rounded caller package at Code-disjoint reimplementation; does not import package What passes (14 of 14):
Not covered: live verify/check_caller re-execution; full SOURCES gz archive auth; physical mixed-provider; new κ. This is a finite replay of committed receipts, not a formal proof. check_4178.py#!/usr/bin/env python3
"""Independent finite controls for PR4178 (Gaussian height contract + caller).
Recomputes program kind/event totals, caller error bound, and a core SOURCES
subset. Does not import package verify.py / check_caller.py.
Package head 3e69c9360f609bdbf3617d35ea44f497f5506f93 via GitHub API.
Full remote auth of all 35 SOURCES inputs (incl. large gz archives) is out of
scope; ten core text inputs are authenticated.
James Reed (@rcfc-jreed), with substantial AI assistance (Claude, in Cursor).
Apache-2.0.
"""
from __future__ import annotations
import argparse, hashlib, json, sys
from fractions import Fraction
from pathlib import Path
HEAD = "3e69c9360f609bdbf3617d35ea44f497f5506f93"
BASE = "12fa8c5c844be21bfefb38a19503fbd867a11244"
CORE = {
"research/capped-phase-fusion/evidence/inplace_algebra_ultra/check_tensor_compiler.py",
"research/capped-phase-fusion/README.md",
"research/simultaneous-gate-rounding/README.md",
"research/complex-grid-prefix-audit/PROOF.md",
"research/unconditional-batched-crt/COMPLEX.md",
"research/unconditional-batched-crt/GAUSSIAN.md",
"research/unconditional-batched-crt/PROOF.md",
"research/unconditional-batched-crt/vendor/TENSOR-COMPILER.md",
}
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 auth_core(sources, deps: Path):
bad, count = [], 0
for row in sources["files"]:
if row["path"] not in CORE:
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 run(pkg: Path, deps: Path):
sources = load(pkg, "SOURCES.json")
verify = load(pkg, "VERIFY.json")
result = load(pkg, "RESULT.json")
caller = load(pkg, "CALLER-RESULT.json")
check("I1 SOURCES base_commit == 12fa8c5c…; VERIFY ready",
sources["base_commit"] == BASE and verify["status"] == "ready")
check("I2 RESULT PASS_GAUSSIAN_HEIGHT_CONTRACT; CALLER PASS_ROUNDED_GAUSSIAN_CALLER",
result["status"] == "PASS_GAUSSIAN_HEIGHT_CONTRACT"
and caller["status"] == "PASS_ROUNDED_GAUSSIAN_CALLER")
check("I3 scopes exclude native/full Gaussian/multiplication theorem / physical mixed-provider",
"multiplication-theorem" in result["scope"]
and "no physical mixed-provider" in caller["scope"])
n_in = sum(1 for f in sources["files"] if f["usage"] == "input")
check("S0 SOURCES declares 35 input files (+2 provenance)",
n_in == 35 and len(sources["files"]) == 37)
n_core, bad = auth_core(sources, deps)
check("S1 core SOURCES subset authenticates (8 text inputs)",
not bad and n_core == 8, bad)
# Programs
check("P1 eight programs: THREE/FOUR × base/extra × forward/backward",
set(result["programs"]) == {
"FOUR-base/backward", "FOUR-base/forward",
"FOUR-extra/backward", "FOUR-extra/forward",
"THREE-base/backward", "THREE-base/forward",
"THREE-extra/backward", "THREE-extra/forward",
})
bad_k = []
for name, prog in result["programs"].items():
if sum(prog["kinds"].values()) != prog["events"]:
bad_k.append(name)
if len(prog["sha256"]) != 64 or len(prog["canonical_construction_sha256"]) != 64:
bad_k.append(("sha", name))
if sum(prog["child_profile"].values()) != sum(prog["kinds"].values()) - prog["kinds"].get("scalar", 0):
# child_profile may not equal non-scalar; skip strict
pass
check("P2 each program: sum(kinds)=events; sha256 present",
not bad_k, bad_k)
# forward/backward share construction sha within base/extra
check("P3 forward/backward share canonical_construction_sha256 within each base/extra pair",
all(result["programs"][f"{tag}/forward"]["canonical_construction_sha256"]
== result["programs"][f"{tag}/backward"]["canonical_construction_sha256"]
for tag in ("FOUR-base", "FOUR-extra", "THREE-base", "THREE-extra")))
prim = result["primitives"]
check("R1 primitives: 338 C_cases; 4394 scalar_cases; 26 distinct scalars",
prim["C_cases"] == 338 and prim["scalar_cases"] == 4394
and len(prim["distinct_scalars"]) == 26)
check("R2 contract: C dims 1..6; 54 incoming height cases; 9 controls",
result["contract"]["C_dimensions"] == [1, 2, 3, 4, 5, 6]
and result["contract"]["incoming_height_cases"] == 54
and len(result["controls"]) == 9)
check("R3 reserve C_bits=2650; bridges_per_replica_port=9",
result["reserve"]["C_bits"] == 2650
and result["reserve"]["bridges_per_replica_port"] == 9)
check("A1 CALLER: maximum_error < proved_error_bound; 34 trajectories/output shas",
Fraction(caller["maximum_error"]) < Fraction(caller["proved_error_bound"])
and caller["trajectories"] == 34 == len(caller["output_sha256"])
and all(len(h) == 64 for h in caller["output_sha256"]))
check("A2 CALLER geometry: K=6,M0=2,R=64,axes=2; fractional_bits=256; 4 controls",
caller["K"] == 6 and caller["M0"] == 2 and caller["R"] == 64
and caller["axes"] == 2 and caller["fractional_bits"] == 256
and len(caller["controls"]) == 4
and caller["observed_height"] == caller["observed_raw_H_entrance_height"] == 8)
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). |
|
Independent scoped audit of #4178 Gaussian height / mixed-provider precision at Code-disjoint nested fork of No packaging defect in SOURCES scope. All 37 digests match. What passes: sealed Not covered here: Finite pin/seal/height-contract replay ≠ formal proof. James Reed (@rcfc-jreed), with substantial AI assistance (Claude, in Cursor). |
I identify an omitted incoming-height term in PR4100's literal common-grid allocation and give an exact constant-vector witness. The author allows inputs on
2^-(P+t0) Z[i]with magnitude at most2^t0, then allocates a grid withoutt0. Fort0=Bh+1, a constant input lies half a unit below the stated fractional grid and C preserves it. I propose one root allocation ofP+t0+Bhfractional bits andt0+Bh+2integer/sign bits.I derive an explicit conditional reserve from all eight emitted THREE/FOUR base/extra programs. I reconstruct their canonical construction fields from the original words, regenerate the complete programs through the authenticated emitter and match the retained digests. The census includes initial corrections, backward center flushes, restoration and cleanup. Maximum scalar-height charge: 30,349; maximum division shift: 3. I count all 725,760 bridge ADDs per cover and retain the full native rank mass, giving
S=23431680*Gamma,E=99056520*Gamma+73,B=max(2,ceil((S+E)/25)).I prove the recurrence by strong induction, including the growing leaf cutoff, without assuming monotonicity. I retain a separate shift-extent condition and add the Gaussian caller's raw-H conversion/restoration reserve. I do not exhibit a failing Gaussian execution or reject the proposed exponent.
I also bind an explicit rounding protocol to the actual six-H/Beneš compiler: rounded tables and cached suffix products, rounded diagonal outputs, and exact raw-H returns after H0 scale restoration. I prove a forward-error bound independent of scan length, account for temporary product widths and the complete cache/rounding scans, and derive O(p)-bit records even with O(p) incoming height. I retain the author's coefficient-generation and boundary-prefix norm hypotheses.
CALLER.mdgives the quantified protocol and its outer error-budget substitution.I replay 34 trajectories through two distinct coarse-label programs, with eighteen raw-H calls and nineteen diagonals per trajectory, against separate original-gate endpoints. I observe nonzero rounding error, raw-H entrance height eight and temporary fractional width 511. Controls detect stale carries, incompatible global H signatures, omitted product rounding and omitted H0 restoration. The retained provider controls cover 4,394 scalar cases, 338 C/inverse-C cases and 54 incoming-height witnesses.
At
3e69c9360f609bdbf3617d35ea44f497f5506f93, all four ordinary/optimized registered checks pass. I passed the 45-file committed-byte/source-history preflight, official export integrity and all four Git-free export commands in 1.521, 1.569, 1.621 and 1.415 seconds, with all 46 files including the receipt unchanged. Export SHA256:1e1bb43646fab5f790d861ed8288ec00970ecede8f1df8f98e866f97adda9aa0; receipt SHA256:dce18db1b3a1bad362f53060c1cc1d0a9d3c4cce228388a7a8be948258c47eb6. I retain the first revision's successful hosted/export receipt in the canonical Discussion.I matched all four successful hosted records to the committed export and verified the successful unchanged-input step. Test merge
a7ea76d10c99400669d116bcdb39870a598e1660has the published tree5d1a6bfaec5d97485342cc4c2bcc97f45649b5cb. Provider receipt:6a5a920762c63f1b53cb46f9dc7139294372ff99006072207a9898f0b5479b3f; caller receipt:60f8a60f8268bbc8717a4b505aca1cd39dc4e1e10d4fbdc0d6dd53af4b60f142.I start from main
12fa8c5c844be21bfefb38a19503fbd867a11244, priority revision 7, and pin PR4100 at337d04939571a637aeab54a0f58f54fde811663aand PR4088 at72d7efc181edb21806a878f174847c96dd410ab0. I refreshed main and checked both source heads, current feedback, the canonical claim and 100 recent PR records before submission. I record the broader bounded overlap search and scope in Discussion4175.I leave the analytic coefficient/conditioning and rounded boundary-prefix estimates, native/free-algebra endpoints, physical execution and complete theorem acceptance open. I use an exact C/H0 interface model in the caller replay; I do not execute the physical mixed-provider cover. Yssite's PR4180 supplies separate finite-admission evidence. The conservative reserve constant has 2,650 bits; I claim an asymptotic existence bound, not a practical precision improvement. I keep the selected frontier unchanged.
Jose Manuel (
jmbarrancoml), with substantial OpenAI Codex assistance. I credit Vlado Vojdanovski's compiler, ywz65's earlier simultaneous-rounding theorem, Cinna Davis's construction, AAAmirinu's prefix/divisibility/shift audit, Gareth Davidson's Horner analysis and the retained native lineage and source notices. My source-analysis agents belong to the author process; I claim no independent human or formal-kernel acceptance.