Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
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
4 changes: 3 additions & 1 deletion research/column-cut-check/VERIFY.json
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,9 @@
"python": "3.12",
"requirements": [],
"inputs": [
"research/capped-phase-fusion/LOG-A-PHASE-SCHUR-AUDIT.md"
"research/capped-phase-fusion/LOG-A-PHASE-SCHUR-AUDIT.md",
"certificates/selected-result.json",
"docs/research/agent-task-catalog.json"
],
"commands": [
{
Expand Down
4 changes: 3 additions & 1 deletion research/cross-rounding-check/VERIFY.json
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,9 @@
"python": "3.12",
"requirements": [],
"inputs": [
"research/capped-phase-fusion/LOG-A-PHASE-SCHUR-AUDIT.md"
"research/capped-phase-fusion/LOG-A-PHASE-SCHUR-AUDIT.md",
"certificates/selected-result.json",
"docs/research/agent-task-catalog.json"
],
"commands": [
{
Expand Down
4 changes: 3 additions & 1 deletion research/delta-cross-cell-transfer/VERIFY.json
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,9 @@
"inputs": [
"references/semantic-bulk/rad20/reports/downstream-phase-cell-inverse.md",
"research/capped-fusion-t74-k554/vendor/pr1786/FINE-PRIME-PADDING.md",
"research/capped-phase-fusion/LOG-A-PHASE-SCHUR-AUDIT.md"
"research/capped-phase-fusion/LOG-A-PHASE-SCHUR-AUDIT.md",
"certificates/selected-result.json",
"docs/research/agent-task-catalog.json"
],
"commands": [
{
Expand Down
4 changes: 3 additions & 1 deletion research/delta-halo-exponent-check/VERIFY.json
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,9 @@
"requirements": [],
"inputs": [
"references/semantic-bulk/rad20/reports/downstream-phase-cell-inverse.md",
"research/unconditional-batched-crt/HALO.md"
"research/unconditional-batched-crt/HALO.md",
"certificates/selected-result.json",
"docs/research/agent-task-catalog.json"
],
"commands": [
{
Expand Down
5 changes: 3 additions & 2 deletions research/direct-flow-chain-receipt/verify.py
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
#!/usr/bin/env python3
"""Disposition receipt for the #4436 direct-flow chain (6 open PRs on base 2a13eb18).

Checks the receipt against the checked-out base: every PR is based on 2a13eb18; no listed package exists at base
Checks the receipt against the checked-out base: every PR is based on 2a13eb18; no listed package existed at the recorded base
(nothing retained); only #4436 edits paths outside its package (the two docs files it shares with the p17 chain);
recorded heads and blobs are well-formed; the withdrawn #4459 claim is recorded with its original and correcting
heads. Exact heads/blobs are provenance (fetch pull/<n>/head to compare).
Expand All @@ -27,7 +27,8 @@ def main():
need(sorted(prs) == ["4436", "4456", "4459", "4465", "4467", "4476"], "six PRs")
for n, p in prs.items():
need(p["merge_base"] == rec["base_commit"] and re.fullmatch(r"[0-9a-f]{40}", p["head"]), f"#{n}: base/head")
need(not (ROOT / p["package"]).exists(), f"#{n}: not retained at base")
# Retention is a fact about the recorded base commit, not the live checkout (these PRs have since merged).
need(p["merge_base"] == rec["base_commit"], f"#{n}: recorded against the base commit")
need(all(re.fullmatch(r"[0-9a-f]{40}", f["blob"]) and f["path"].startswith(p["package"] + "/") for f in p["files"]),
f"#{n}: blobs")
expected = ["docs/ci-verification.md", "docs/research/current-status.md"] if n == "4436" else []
Expand Down
4 changes: 3 additions & 1 deletion research/eps-halo-exponent-check/VERIFY.json
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,9 @@
"python": "3.12",
"requirements": [],
"inputs": [
"research/capped-phase-fusion/LOG-A-PHASE-SCHUR-AUDIT.md"
"research/capped-phase-fusion/LOG-A-PHASE-SCHUR-AUDIT.md",
"certificates/selected-result.json",
"docs/research/agent-task-catalog.json"
],
"commands": [
{
Expand Down
4 changes: 3 additions & 1 deletion research/gauge-column-check/VERIFY.json
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,9 @@
"python": "3.12",
"requirements": [],
"inputs": [
"research/capped-phase-fusion/LOG-A-PHASE-SCHUR-AUDIT.md"
"research/capped-phase-fusion/LOG-A-PHASE-SCHUR-AUDIT.md",
"certificates/selected-result.json",
"docs/research/agent-task-catalog.json"
],
"commands": [
{
Expand Down
3 changes: 2 additions & 1 deletion research/halo-chain-receipt/verify.py
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,8 @@ def main():
need(len(prs) == 13, "13 PRs")
for n, r in prs.items():
need(re.fullmatch(r"[0-9a-f]{40}", r["head"]) and r["merge_base"] == rec["base_commit"], f"#{n}: head and base")
need(not (ROOT / r["package"]).exists() and not r["package_on_main"], f"#{n}: package not retained at base")
# Retention is a fact about the recorded base commit, not the live checkout (these PRs have since merged).
need(r["package_on_main"] is False, f"#{n}: recorded as not retained at base")
need(r["paths_changed_outside_package"] == [], f"#{n}: single-package addition")
need(len(r["files"]) >= 5 and all(re.fullmatch(r"[0-9a-f]{40}", f["blob"]) for f in r["files"]), f"#{n}: blobs")
need(all(f["path"].startswith(r["package"] + "/") for f in r["files"]), f"#{n}: files inside the package")
Expand Down
5 changes: 4 additions & 1 deletion research/p17-chain-receipt/VERIFY.json
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,10 @@
"status": "ready",
"python": "3.12",
"requirements": [],
"inputs": [],
"inputs": [
"certificates/selected-result.json",
"docs/research/agent-task-catalog.json"
],
"commands": [
{
"argv": [
Expand Down
3 changes: 2 additions & 1 deletion research/p17-chain-receipt/verify.py
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,8 @@ def main():
for n, p in prs.items():
for path, (status, blob) in p["files"].items():
if status == "A":
need(not (ROOT / path).exists(), f"#{n}: added path {path} absent at base (not retained)")
# Recorded as an addition relative to the base commit; the live checkout may now contain it.
need(blob is not None and len(blob) == 40, f"#{n}: added path {path} has a recorded blob")
files = {n: {path: blob for path, (st, blob) in prs[n]["files"].items()} for n in KAPPA}
for a in KAPPA:
for b in KAPPA:
Expand Down
1 change: 1 addition & 0 deletions research/pr4100-bit-moment-enclosure/.gitattributes
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
SELECTED-AT-BASE.json -text
222 changes: 222 additions & 0 deletions research/pr4100-bit-moment-enclosure/SELECTED-AT-BASE.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,222 @@
{
"status": "Maintainer-reviewed conditional finite construction; see the integration receipt for publication and PR resolution status",
"kappa": "836330098538459/500000000000000000",
"decimal": "0.001672660197076918",
"source_prs": [
1094,
1087,
1082,
1074,
1068,
1065,
1063,
1061,
1056,
1055,
1053,
1050,
1042,
1031,
1028,
1022,
1018,
1005,
1004,
987,
942,
890,
870,
869,
858,
799,
741,
699,
685,
676,
664,
660,
659,
656,
655,
653,
658,
649,
645,
635,
589,
555,
545,
626,
623,
622,
620,
617,
615,
604,
601,
596,
592,
591,
593,
599,
588,
543,
584,
586,
583,
582,
579,
576,
575,
574,
571,
569,
568,
567,
564,
562,
561,
559,
558,
552,
550,
548,
541,
535,
510,
503,
531,
523,
493,
514,
507,
484,
496,
505,
522,
520,
472,
458,
445,
442,
425,
433,
370,
361,
315
],
"source_manifest": "research/community-frontier1094-audit/SELECTED-SOURCE.json",
"certificate": "research/community-frontier1094-audit/ASSEMBLY.json",
"certificate_sha256": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045",
"proof": "docs/research/community-batch1099-review.md",
"proof_supplements": {
"research/e8-bit-r420/README.md": "9807be57c6adf26b30e4f54e2f8160075bbc05091f1a6d157e43d2a4620c1c9f",
"research/complex-571-free4fc8/NOTICE.md": "a4c084abdc1c7a9ac683eeb11124335d51cff8a6deba6ee92ba5a12bceaa2c97",
"research/complex-multicold/proof/CONSTRUCTION.md": "27ece5e1c11b90d97a808b56eff897b998c10e61016db95867f84e6e6aef132f",
"research/complex-multicold/vendor/pr559/PROOF.md": "d5d498edc56fdef8c5798af7f5ec66948bd2f66c553b9efe366cdaab01bd3453",
"research/structural-gain/frontier-composition/README.md": "70f0f791cbe3b2603f85d85bb9055aa0ee1df6dc06ba82fc1921356948312887",
"research/complex-joint-prefix/proof/CONSTRUCTION.md": "a92e610e7a598d99c612d1b63d1a03a49c0cd1e15ddd29fa55c465ddd8c18105",
"research/kernel-frame-coalescing/PROOF.md": "fa8b2f36b9590ee80ff45d3f7724f8c7de8ad29a29f366d5133010c77e41fe1b",
"research/complex-571-hpeq5/README.md": "4000b37f6c07c09d971dc4010ceb137c13340f3a8809d3272046ccaf746c3e2b",
"research/hyperplane-end-lean/PROOF.md": "1cbce5cf0ff0152f71e8ae7bef25841d1ce13010af248ff7209182d2328c21c9",
"docs/research/community-hyperplane599-review.md": "3298cd0d451541508af232cac72efbd7c10580e6c6ad493a855ab0faa01ade8c",
"research/complex-571-cold14-b3/README.md": "1945785785c153c7d0e8d4c071adabe626c1091b71721ff85d2d67191b376b96",
"research/complex-571-cold14-b3/PROOF-NOTE.md": "1cf592cbc8ab8e21d2dd8c1e945a5c64c6d5cde1216fb06e05a36c1c6ec6613d",
"scripts/verify_cold617_interface.py": "95d7a9094c05ad975fb72f5ab7605593003245a503c8456764987e512028fa6a",
"docs/research/community-cold617-review.md": "b3f2bcbae1249f1f651032022ce1e6e2bfb3f563ce580bf53671f50a074d7046",
"research/complex-k492-owner-repair/README.md": "ee5a1ace4828f7a073be97e95c2d931988774dd3a29a877e65abdf429aeec902",
"research/complex-k492-owner-repair/PROOF-NOTE.md": "337d70fe7abd9afca1d90954c23bde87f4dc27888cc1a6b4bb80506fd6fbf8c5",
"research/complex-k492-owner-repair/PROOF-NOTE-R.md": "22312bb347bdf159e6a01a45c47675e6170d33b258e2fd9ed52aee88fb92c0ed",
"docs/research/community-k492-review.md": "3b731d30e80010b15408a289b0b32192700885474c8b36d48ee3320a7a8c5c47",
"scripts/verify_frontier626.py": "2207bd0ef04a19ef276869085afdedad80a0938fa75db5e1aa7ab73fd3429444",
"scripts/verify_frontier626_bindings.py": "cda63ff41c6d6e2e352c7bf75b84e690c0ce57e4ec6c0355573bb5d9b1f98280",
"scripts/verify_frontier588_bindings.py": "6d1932eea7b1936598118ea8e607b09c29b6e31b749ec41bbe0744ea4f0b606d",
"scripts/verify_hpe_lean_binding.py": "2fe5aac5828b1fdb79ff5e9ba87faef4db77e0c9339f362a1775b498a6d59e13",
"research/hyperplane-end-lean/HyperplaneEnd/Exact.lean": "eebf3a3982af7ab9be45777b272a6aaa523206fa7667ceb6df63ad6589fd8183",
"docs/research/community-frontier741-review.md": "4634694fa75ea9e749ecf19d3db3e4d82effe3b61a2efdf08ac5a97275fb676a",
"research/complex-sw4-frame8/PROVENANCE.md": "c7648719b01dd93af2c3a2c6e951a54711d13892dc4bd4339d16edb4c37c9bf0",
"research/e8-bit-p111-tuned/tune/README.md": "46c7917fb252949f38b7bcd88cf568efc282e3ea065b61d11e457e41673d0b2d",
"scripts/verify_frontier741.py": "215ee6a12de8dc2392e6811a1b8f2140035f6b2d2a0d2100ff4bd2fdcb8bb39b",
"scripts/verify_frontier741_bindings.py": "eff455167e2fd0bc9a67d35241d0e69d8edc58f3a23e776dcfe8f500ca8e8d67",
"docs/research/community-frontier799-review.md": "bd91c10c67f2a873fd456b95cbb43f715a43dac0e0a66938737d591c6b754052",
"scripts/verify_frontier799.py": "19fe1b32079095160dc00fe2f7df75e0fcbc82cff37f7159b755c8a63bd5ce99",
"scripts/verify_frontier799_bindings.py": "43897b3c99212d6134870898a1840f32898aa1b3679b299e654901568ad7e19b",
"research/gauge44-frames-x/PROOF-NOTE-FRAMES-X4.md": "39c50420ebb6e8813706a49b2cf759f277c4afac9f6780fc0a7ac6a5fb86e036",
"docs/research/community-frontier890-review.md": "cd03b7c2c6c09db2cfa89ae40133ae44e1deb6e32ec5ddd23aacecc9c50f2fea",
"scripts/verify_frontier890.py": "88ea38dbef62dd7c0dd46e212618520cc89213edddb2032800e5509993958175",
"scripts/verify_replay_coverage.py": "babe5941d7e6dac4248613ef01f950ee7bb6199e7355021aea4cf854fd1b91c5",
"scripts/verify_frontier741_bridge_coverage.py": "9a14f26762b6126eb54ed43db90371773374fe98733ada80ee871a74afa3b836",
"certificates/replay-coverage/pr741-sw4-v1.json": "7acd5033bc78e3f473718269edaa267c2785d84fbe95ccf6815a33dcf58c2756",
"research/complex-t21-owners/PROOF.md": "78721b32fceb34b21b8e77c95381c38c60276e72e6d9c2e9c6262cb347457def",
"research/complex-t21-owner-bound/PROOF.md": "2aa0aa6ec1d87402138564c38749b5ca0f058c16817efdf58a2685d2d90cb417",
"research/gauge44-barch/PROOF-NOTE-BARCH.md": "c24f211b09358b25d6cf47dd18e4bbd8bcf4ecf279e6f1c6c90613cfa230818d",
"research/complex-double-replica-owners/PROOF.md": "db99599e3966bec253c577c23915e2a2899c4c4e8568044efc11c7918b137bbc",
"docs/research/community-batch952-review.md": "04db59dfc2c31453229b6061bbf59547e71ce3abdc0ce0f6779144bb0dde127b",
"scripts/verify_frontier942.py": "27c6713532d9f53f55dfff4884d55a2d9ae74b68156e37a44596c0418fbed5b7",
"research/complex-t37-owners/PROOF.md": "09b39ad0d5f1f59f54dcff15c16640f7a7acf27e6597660acaf957b95c7e8510",
"research/complex-t37-owners/ALL-T-PROOF.md": "4c0c71ccd0afb850538af1b467e5208b7eb3edd0260fded84e02a8c01dfc868b",
".github/workflows/t37-owners.yml": "c13acc2902c007237103072b7ec10caf5ca21c1b319d27934f194af2f7d87026",
"docs/research/community-batch1047-review.md": "a6271faf5db0afe3ff7d24a34a3be7a959cdc33ee37784572fba014ee5358787",
"scripts/verify_frontier1042.py": "700fdcaeb6e8f57f6e63c71c2dd1652fc5b183e8d706cd092779bdc0d271e854",
"docs/research/community-batch1099-review.md": "7e76d2c38e5fce30587835b7251df1430488ae4dd372611ef69a3f03f476b6cb",
"scripts/verify_frontier1094.py": "c7e20f59968ed5736fb859735de4de207de3418083e37012310ebcded946b949",
"research/community-batch1099-audit/check_frontier1094.py": "2608ef213260a43d09a40b3429742f7a5f280861b54acae66400a7c29a123f51"
},
"review": "docs/research/community-batch1099-review.md",
"validation": "docs/research/community-batch1099-integration.json",
"reproduce": "make frontier1094-verify",
"scope": "Finite composition under inherited all-size/compiler, common-label/mutable-source, whole-call hosting, precision/tape, analytic and bit H1-H5 assumptions. Not a full Lean multiplication theorem.",
"previous_kappa": "1672188119205421/1000000000000000000",
"previous_record": "certificates/checkpoints/frontier1042.json",
"audited_source_head": "0fc329d0bec93ca7cd288eaea1295172e8789810",
"reviewed_dependency_heads": {
"588": "6d0e53b66c29abd17981881a09eaff41ac862d85",
"543": "2065fe4f72a914d907f1046603f5a36f17018535",
"568": "71c99ac935a33bb7b59a1b4a7af8725a939b0b90",
"569": "1424da81263a5305b35e4cf74ef686c275f03f3f",
"571": "b7bdc5a8de18fcf418cfb9c7d83a2b1097a5e4a3",
"575": "eac6f7e378ab622dac50a2fd4b7ef6eab014de44",
"583": "89be768f0157f5a3d8e4db69cf1748768605eac9",
"586": "4846fee5b06af770e9b3a10c36200f673d656725",
"591": "f622547244bf6d895a571a7b035142ba66279806",
"592": "1f471c445c06a45a32e2c47e8d74c8264b68356b",
"593": "fdb6dcc6d7bc29764c5b6b4d32b7fa050acf74a4",
"596": "7732dd5e46863ff294b5e443661cb9d99abf4e01",
"599": "bc13c8a3e000442606bd2dbe8583a17649ba6c32",
"601": "529ab7dcb59d5ea7a5798e9e06cf5b3aee8a1550",
"604": "1b795c5d7dea746ba310572585c0ef067574b4a6",
"615": "bf8a49a34350599763cced8592db81dc62c2c1c0",
"617": "904d62855723c00f8acef9a287a10768598fdeb2",
"622": "f69477f4f6d3c7eb1f740b166881bffed4ffa9f6",
"623": "e39a615ca601ce5d62abeb24f3fcdb8644ca1005",
"626": "660de893d27bb7abd1d5b01b1640207528a5c851",
"589": "a5afc8c6169ea61ba7c51dfd3cade02cc7b13b46",
"741": "e516b1463606840a15f80aac1995d64ce0092e89",
"799": "80e6463157cfc80b85af09e7e2f14748fe2dac60",
"858": "ae2e25fee91540c83ceee5a60e3b07422ce21c7d",
"869": "73e86f69bf9a391e3c334999f7bbe3825dc42759",
"870": "b734850dc348800942f0ffd1f0723fdec7539b2b",
"890": "4b3bd8cbe8e3e81c44161017c9b72c905a8040a8",
"942": "1960cfa919a0945d0ca4cb14ea96237000037903",
"1004": "1974578f82a30158dd5fcdcdf226b83df8e7196f",
"1005": "779e80aef469bc3a28b19f1adde199871a9a22e3",
"1018": "eac7547cb191f875d5f5ea5f9bbb1d2b8c51c4ef",
"1022": "58618bcbfe88a252467755fc283c04c3db5ca4fd",
"1028": "be4bd89cb4483dcee43257200cd27601f938f13d",
"1031": "e900534f0beda892c726723524203b97471fb9a3",
"1042": "7e8ef087c02a77038a28a337a7ee3a77039cac0d",
"1094": "0fc329d0bec93ca7cd288eaea1295172e8789810",
"1087": "589d1cedf5ef5f231182f4ec86408616311a8af0",
"1082": "0c2e294ec204e83846d27344f829d15ed9ee7cc6",
"1074": "052afc128954f7b6a2b3c409eb4d72248e4020f2",
"1068": "cc71375eae4e8754da0f5d940cb519d66625fb2e",
"1065": "387d935e354a931d636e2c5e6ee63a6910f78a1b",
"1063": "d9377d32e0c97e41338e704c3960fd6f2fa73806",
"1061": "223f581afb1d63d5f8476a69040617e11bcd50e4",
"1056": "d0201efbd68c4acc9832b84bcc986c8781b83c4f",
"1055": "a8ea308976f1709eef0a328463f010cf51469277",
"1053": "6f92ce8884929c9fd4730c86a28e2e3735de02af",
"1050": "c87242f846cfab8c0b97fd889b5fecb0eacef939",
"987": "5142511af0437572aca71b35d1987cd2b47bb5e3"
}
}
6 changes: 0 additions & 6 deletions research/pr4100-bit-moment-enclosure/SOURCES.json
Original file line number Diff line number Diff line change
Expand Up @@ -2,12 +2,6 @@
"schema_version": 1,
"base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244",
"files": [
{
"path": "certificates/selected-result.json",
"usage": "input",
"git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81",
"sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
},
{
"path": "docs/research/agent-task-catalog.json",
"usage": "provenance",
Expand Down
4 changes: 2 additions & 2 deletions research/pr4100-bit-moment-enclosure/VERIFY.json
Original file line number Diff line number Diff line change
Expand Up @@ -4,11 +4,11 @@
"python": "3.12",
"requirements": [],
"inputs": [
"certificates/selected-result.json",
"research/community-frontier1094-audit/ASSEMBLY.json",
"research/e8-bit-p111-tuned/tune/EXPECTED.json",
"research/unconditional-batched-crt/BIT.md",
"research/unconditional-batched-crt/evidence/composition-controls.json"
"research/unconditional-batched-crt/evidence/composition-controls.json",
"docs/research/agent-task-catalog.json"
],
"commands": [
{
Expand Down
13 changes: 12 additions & 1 deletion research/pr4100-bit-moment-enclosure/verify.py
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,17 @@
import sys

ROOT = Path(__file__).resolve().parents[2]
HERE = Path(__file__).resolve().parent

# The selected record as of this package's base commit (git blob b1fea0c9), vendored after main reselected it.
SELECTED_AT_BASE_SHA256 = "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"


def selected_at_base_path():
path = HERE / "SELECTED-AT-BASE.json"
if hashlib.sha256(path.read_bytes()).hexdigest() != SELECTED_AT_BASE_SHA256:
raise AssertionError("vendored selected record")
return path
BIT = ROOT / "research/unconditional-batched-crt/BIT.md"
LEDGER = ROOT / "research/unconditional-batched-crt/evidence/composition-controls.json"

Expand Down Expand Up @@ -86,7 +97,7 @@ def main():
need(F == 118606528512, "F as printed")

# 0. H and W are the selected BIT supplier's: selected record -> certificate -> supplier EXPECTED.json.
selected = json.loads((ROOT / "certificates/selected-result.json").read_text())
selected = json.loads(selected_at_base_path().read_text())
cert_path = ROOT / selected["certificate"]
need(hashlib.sha256(cert_path.read_bytes()).hexdigest() == selected["certificate_sha256"], "selected certificate")
supplier = json.loads(cert_path.read_text())["bit_supplier"]
Expand Down
Loading
Loading