From 02920a630738c5b89f615cf859b40020f02c498f Mon Sep 17 00:00:00 2001 From: pinterbanget Date: Thu, 22 Oct 2026 12:29:58 +0700 Subject: [PATCH] Portable-replay repair of pinterbanget packages: VERIFY inputs, at-base receipts, vendored historical selected record, timeout Co-Authored-By: Claude Opus 5.5 --- research/column-cut-check/VERIFY.json | 4 +- research/cross-rounding-check/VERIFY.json | 4 +- .../delta-cross-cell-transfer/VERIFY.json | 4 +- .../delta-halo-exponent-check/VERIFY.json | 4 +- research/direct-flow-chain-receipt/verify.py | 5 +- research/eps-halo-exponent-check/VERIFY.json | 4 +- research/gauge-column-check/VERIFY.json | 4 +- research/halo-chain-receipt/verify.py | 3 +- research/p17-chain-receipt/VERIFY.json | 5 +- research/p17-chain-receipt/verify.py | 3 +- .../.gitattributes | 1 + .../SELECTED-AT-BASE.json | 222 ++++++++++++++++++ .../pr4100-bit-moment-enclosure/SOURCES.json | 6 - .../pr4100-bit-moment-enclosure/VERIFY.json | 4 +- .../pr4100-bit-moment-enclosure/verify.py | 13 +- .../pr4100-chirp-odometer-tariff/VERIFY.json | 4 +- research/pr4100-crt-repair-tariff/VERIFY.json | 4 +- research/pr4100-guard-coloring/VERIFY.json | 4 +- .../VERIFY.json | 4 +- research/pr4100-union-head-travel/VERIFY.json | 4 +- .../.gitattributes | 1 + .../SELECTED-AT-BASE.json | 222 ++++++++++++++++++ .../pr4270-outer-exponent-check/SOURCES.json | 6 - .../pr4270-outer-exponent-check/VERIFY.json | 2 +- .../pr4270-outer-exponent-check/verify.py | 13 +- research/pr4326-bit-root-check/SOURCES.json | 6 - research/pr4326-bit-root-check/VERIFY.json | 4 +- research/pr4338-b2-chain-check/.gitattributes | 1 + .../SELECTED-AT-BASE.json | 222 ++++++++++++++++++ research/pr4338-b2-chain-check/SOURCES.json | 6 - research/pr4338-b2-chain-check/VERIFY.json | 4 +- research/pr4338-b2-chain-check/verify.py | 12 + research/pr4470-arithmetic-check/VERIFY.json | 2 +- .../stage-zero-forced-translation/VERIFY.json | 4 +- .../three-base-census-recount/VERIFY.json | 4 +- 35 files changed, 762 insertions(+), 53 deletions(-) create mode 100644 research/pr4100-bit-moment-enclosure/.gitattributes create mode 100644 research/pr4100-bit-moment-enclosure/SELECTED-AT-BASE.json create mode 100644 research/pr4270-outer-exponent-check/.gitattributes create mode 100644 research/pr4270-outer-exponent-check/SELECTED-AT-BASE.json create mode 100644 research/pr4338-b2-chain-check/.gitattributes create mode 100644 research/pr4338-b2-chain-check/SELECTED-AT-BASE.json diff --git a/research/column-cut-check/VERIFY.json b/research/column-cut-check/VERIFY.json index 9784f01335..6d5a0f3e81 100644 --- a/research/column-cut-check/VERIFY.json +++ b/research/column-cut-check/VERIFY.json @@ -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": [ { diff --git a/research/cross-rounding-check/VERIFY.json b/research/cross-rounding-check/VERIFY.json index 67010526d1..7da4bbeab1 100644 --- a/research/cross-rounding-check/VERIFY.json +++ b/research/cross-rounding-check/VERIFY.json @@ -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": [ { diff --git a/research/delta-cross-cell-transfer/VERIFY.json b/research/delta-cross-cell-transfer/VERIFY.json index e50eb45b2c..033267a096 100644 --- a/research/delta-cross-cell-transfer/VERIFY.json +++ b/research/delta-cross-cell-transfer/VERIFY.json @@ -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": [ { diff --git a/research/delta-halo-exponent-check/VERIFY.json b/research/delta-halo-exponent-check/VERIFY.json index 7c7fed46e5..c9c032d876 100644 --- a/research/delta-halo-exponent-check/VERIFY.json +++ b/research/delta-halo-exponent-check/VERIFY.json @@ -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": [ { diff --git a/research/direct-flow-chain-receipt/verify.py b/research/direct-flow-chain-receipt/verify.py index e0e4336b9e..19bc71e897 100644 --- a/research/direct-flow-chain-receipt/verify.py +++ b/research/direct-flow-chain-receipt/verify.py @@ -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//head to compare). @@ -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 [] diff --git a/research/eps-halo-exponent-check/VERIFY.json b/research/eps-halo-exponent-check/VERIFY.json index 88ed7e9c48..a355bc57ab 100644 --- a/research/eps-halo-exponent-check/VERIFY.json +++ b/research/eps-halo-exponent-check/VERIFY.json @@ -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": [ { diff --git a/research/gauge-column-check/VERIFY.json b/research/gauge-column-check/VERIFY.json index 12ed85caef..71daa37f10 100644 --- a/research/gauge-column-check/VERIFY.json +++ b/research/gauge-column-check/VERIFY.json @@ -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": [ { diff --git a/research/halo-chain-receipt/verify.py b/research/halo-chain-receipt/verify.py index e862ee2072..96b0711a17 100644 --- a/research/halo-chain-receipt/verify.py +++ b/research/halo-chain-receipt/verify.py @@ -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") diff --git a/research/p17-chain-receipt/VERIFY.json b/research/p17-chain-receipt/VERIFY.json index ba8ad08441..50b6ed542c 100644 --- a/research/p17-chain-receipt/VERIFY.json +++ b/research/p17-chain-receipt/VERIFY.json @@ -3,7 +3,10 @@ "status": "ready", "python": "3.12", "requirements": [], - "inputs": [], + "inputs": [ + "certificates/selected-result.json", + "docs/research/agent-task-catalog.json" + ], "commands": [ { "argv": [ diff --git a/research/p17-chain-receipt/verify.py b/research/p17-chain-receipt/verify.py index e71e5a3f41..bec3c47751 100644 --- a/research/p17-chain-receipt/verify.py +++ b/research/p17-chain-receipt/verify.py @@ -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: diff --git a/research/pr4100-bit-moment-enclosure/.gitattributes b/research/pr4100-bit-moment-enclosure/.gitattributes new file mode 100644 index 0000000000..b99f18e429 --- /dev/null +++ b/research/pr4100-bit-moment-enclosure/.gitattributes @@ -0,0 +1 @@ +SELECTED-AT-BASE.json -text diff --git a/research/pr4100-bit-moment-enclosure/SELECTED-AT-BASE.json b/research/pr4100-bit-moment-enclosure/SELECTED-AT-BASE.json new file mode 100644 index 0000000000..b1fea0c944 --- /dev/null +++ b/research/pr4100-bit-moment-enclosure/SELECTED-AT-BASE.json @@ -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" + } +} diff --git a/research/pr4100-bit-moment-enclosure/SOURCES.json b/research/pr4100-bit-moment-enclosure/SOURCES.json index a3c5f78af6..b1250a0e09 100644 --- a/research/pr4100-bit-moment-enclosure/SOURCES.json +++ b/research/pr4100-bit-moment-enclosure/SOURCES.json @@ -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", diff --git a/research/pr4100-bit-moment-enclosure/VERIFY.json b/research/pr4100-bit-moment-enclosure/VERIFY.json index 98cf61a1de..e864afde82 100644 --- a/research/pr4100-bit-moment-enclosure/VERIFY.json +++ b/research/pr4100-bit-moment-enclosure/VERIFY.json @@ -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": [ { diff --git a/research/pr4100-bit-moment-enclosure/verify.py b/research/pr4100-bit-moment-enclosure/verify.py index a1c44117e2..67ef187a07 100644 --- a/research/pr4100-bit-moment-enclosure/verify.py +++ b/research/pr4100-bit-moment-enclosure/verify.py @@ -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" @@ -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"] diff --git a/research/pr4100-chirp-odometer-tariff/VERIFY.json b/research/pr4100-chirp-odometer-tariff/VERIFY.json index 7cd09e3b48..a925e3fee2 100644 --- a/research/pr4100-chirp-odometer-tariff/VERIFY.json +++ b/research/pr4100-chirp-odometer-tariff/VERIFY.json @@ -5,7 +5,9 @@ "requirements": [], "inputs": [ "research/unconditional-batched-crt/PROOF.md", - "research/unconditional-batched-crt/evidence/composition-controls.json" + "research/unconditional-batched-crt/evidence/composition-controls.json", + "certificates/selected-result.json", + "docs/research/agent-task-catalog.json" ], "commands": [ { diff --git a/research/pr4100-crt-repair-tariff/VERIFY.json b/research/pr4100-crt-repair-tariff/VERIFY.json index 4e6e639937..2acf9c3f8a 100644 --- a/research/pr4100-crt-repair-tariff/VERIFY.json +++ b/research/pr4100-crt-repair-tariff/VERIFY.json @@ -6,7 +6,9 @@ "inputs": [ "research/selected-complex-compact-adapters/PROOF.md", "research/unconditional-batched-crt/CRT.md", - "research/unconditional-batched-crt/check_batched_crt.py" + "research/unconditional-batched-crt/check_batched_crt.py", + "certificates/selected-result.json", + "docs/research/agent-task-catalog.json" ], "commands": [ { diff --git a/research/pr4100-guard-coloring/VERIFY.json b/research/pr4100-guard-coloring/VERIFY.json index 0f96538e2a..db6dacb1d4 100644 --- a/research/pr4100-guard-coloring/VERIFY.json +++ b/research/pr4100-guard-coloring/VERIFY.json @@ -5,7 +5,9 @@ "requirements": [], "inputs": [ "research/unconditional-batched-crt/CRT.md", - "research/unconditional-batched-crt/check_batched_crt.py" + "research/unconditional-batched-crt/check_batched_crt.py", + "certificates/selected-result.json", + "docs/research/agent-task-catalog.json" ], "commands": [ { diff --git a/research/pr4100-proof-composition-audit/VERIFY.json b/research/pr4100-proof-composition-audit/VERIFY.json index f356fab452..35898afc9f 100644 --- a/research/pr4100-proof-composition-audit/VERIFY.json +++ b/research/pr4100-proof-composition-audit/VERIFY.json @@ -6,7 +6,9 @@ "inputs": [ "research/unconditional-batched-crt/CRT.md", "research/unconditional-batched-crt/PROOF.md", - "research/unconditional-batched-crt/check_batched_crt.py" + "research/unconditional-batched-crt/check_batched_crt.py", + "certificates/selected-result.json", + "docs/research/agent-task-catalog.json" ], "commands": [ { diff --git a/research/pr4100-union-head-travel/VERIFY.json b/research/pr4100-union-head-travel/VERIFY.json index af7e09519a..fce98b92a3 100644 --- a/research/pr4100-union-head-travel/VERIFY.json +++ b/research/pr4100-union-head-travel/VERIFY.json @@ -5,7 +5,9 @@ "requirements": [], "inputs": [ "research/unconditional-batched-crt/evidence/composition-controls.json", - "research/unconditional-batched-crt/vendor/UNION-SCHEDULE.md" + "research/unconditional-batched-crt/vendor/UNION-SCHEDULE.md", + "certificates/selected-result.json", + "docs/research/agent-task-catalog.json" ], "commands": [ { diff --git a/research/pr4270-outer-exponent-check/.gitattributes b/research/pr4270-outer-exponent-check/.gitattributes new file mode 100644 index 0000000000..b99f18e429 --- /dev/null +++ b/research/pr4270-outer-exponent-check/.gitattributes @@ -0,0 +1 @@ +SELECTED-AT-BASE.json -text diff --git a/research/pr4270-outer-exponent-check/SELECTED-AT-BASE.json b/research/pr4270-outer-exponent-check/SELECTED-AT-BASE.json new file mode 100644 index 0000000000..b1fea0c944 --- /dev/null +++ b/research/pr4270-outer-exponent-check/SELECTED-AT-BASE.json @@ -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" + } +} diff --git a/research/pr4270-outer-exponent-check/SOURCES.json b/research/pr4270-outer-exponent-check/SOURCES.json index 4ad162d174..ac2a480952 100644 --- a/research/pr4270-outer-exponent-check/SOURCES.json +++ b/research/pr4270-outer-exponent-check/SOURCES.json @@ -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", diff --git a/research/pr4270-outer-exponent-check/VERIFY.json b/research/pr4270-outer-exponent-check/VERIFY.json index 01524d4955..b7b62cd6dc 100644 --- a/research/pr4270-outer-exponent-check/VERIFY.json +++ b/research/pr4270-outer-exponent-check/VERIFY.json @@ -4,7 +4,7 @@ "python": "3.12", "requirements": [], "inputs": [ - "certificates/selected-result.json" + "docs/research/agent-task-catalog.json" ], "commands": [ { diff --git a/research/pr4270-outer-exponent-check/verify.py b/research/pr4270-outer-exponent-check/verify.py index fa2b2908b8..9726ed7634 100644 --- a/research/pr4270-outer-exponent-check/verify.py +++ b/research/pr4270-outer-exponent-check/verify.py @@ -15,6 +15,16 @@ HERE = Path(__file__).resolve().parent ROOT = HERE.parents[1] + +# 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 VENDORED = { "vendor/OUTER-JOIN.md": "bfb4677ee82ffc070be880eca87af05fd096686b464dfd5268cee1b27afa453e", "vendor/pr4181-RESULT.json": "d823509ea38e545db6c287a85c00bc4257825fb2710728dfc776c8801d2becd9", @@ -72,8 +82,7 @@ def main(): text = (HERE / "vendor/OUTER-JOIN.md").read_text() need(all(p in text for p in PHRASES), "OUTER-JOIN.md phrases") pins = {row["path"]: row["sha256"] for row in json.loads((HERE / "SOURCES.json").read_text())["files"]} - sel_path = ROOT / "certificates/selected-result.json" - need(hashlib.sha256(sel_path.read_bytes()).hexdigest() == pins["certificates/selected-result.json"], "selected pin") + sel_path = selected_at_base_path() selected_kappa = Q(json.loads(sel_path.read_text())["kappa"]) fill = json.loads((HERE / "vendor/pr4181-RESULT.json").read_text()) diff --git a/research/pr4326-bit-root-check/SOURCES.json b/research/pr4326-bit-root-check/SOURCES.json index 0cbf76d6e0..c8d770bfbb 100644 --- a/research/pr4326-bit-root-check/SOURCES.json +++ b/research/pr4326-bit-root-check/SOURCES.json @@ -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", diff --git a/research/pr4326-bit-root-check/VERIFY.json b/research/pr4326-bit-root-check/VERIFY.json index 6f4e246bd9..ec7b6c8a0f 100644 --- a/research/pr4326-bit-root-check/VERIFY.json +++ b/research/pr4326-bit-root-check/VERIFY.json @@ -4,8 +4,8 @@ "python": "3.12", "requirements": [], "inputs": [ - "certificates/selected-result.json", - "research/e8-bit-p111-tuned/tune/EXPECTED.json" + "research/e8-bit-p111-tuned/tune/EXPECTED.json", + "docs/research/agent-task-catalog.json" ], "commands": [ { diff --git a/research/pr4338-b2-chain-check/.gitattributes b/research/pr4338-b2-chain-check/.gitattributes new file mode 100644 index 0000000000..b99f18e429 --- /dev/null +++ b/research/pr4338-b2-chain-check/.gitattributes @@ -0,0 +1 @@ +SELECTED-AT-BASE.json -text diff --git a/research/pr4338-b2-chain-check/SELECTED-AT-BASE.json b/research/pr4338-b2-chain-check/SELECTED-AT-BASE.json new file mode 100644 index 0000000000..b1fea0c944 --- /dev/null +++ b/research/pr4338-b2-chain-check/SELECTED-AT-BASE.json @@ -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" + } +} diff --git a/research/pr4338-b2-chain-check/SOURCES.json b/research/pr4338-b2-chain-check/SOURCES.json index 80b73b2606..e9983b93c0 100644 --- a/research/pr4338-b2-chain-check/SOURCES.json +++ b/research/pr4338-b2-chain-check/SOURCES.json @@ -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", diff --git a/research/pr4338-b2-chain-check/VERIFY.json b/research/pr4338-b2-chain-check/VERIFY.json index 3a6d8899d8..0592cdf36a 100644 --- a/research/pr4338-b2-chain-check/VERIFY.json +++ b/research/pr4338-b2-chain-check/VERIFY.json @@ -4,10 +4,10 @@ "python": "3.12", "requirements": [], "inputs": [ - "certificates/selected-result.json", "research/e8-bit-p111-tuned/tune/EXPECTED.json", "research/selected-bit-recursive-closure/RESULT.json", - "research/staged-fourth-mixture-ceiling/RESULT.json" + "research/staged-fourth-mixture-ceiling/RESULT.json", + "docs/research/agent-task-catalog.json" ], "commands": [ { diff --git a/research/pr4338-b2-chain-check/verify.py b/research/pr4338-b2-chain-check/verify.py index 10363301ff..f9e421a42c 100644 --- a/research/pr4338-b2-chain-check/verify.py +++ b/research/pr4338-b2-chain-check/verify.py @@ -15,6 +15,16 @@ HERE = Path(__file__).resolve().parent ROOT = HERE.parents[1] + +# 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 PROOF_SHA256 = "c2ca95cc85439768ebfae81057b845b9e26cc8f153ef787c15f74127456dba8b" PHRASES = [ "a2 = 57697923247/33292900000000", @@ -95,6 +105,8 @@ def main(): pins = {row["path"]: row["sha256"] for row in json.loads((HERE / "SOURCES.json").read_text())["files"]} def pinned(rel): + if rel == "certificates/selected-result.json": + return json.loads(selected_at_base_path().read_text()) path = ROOT / rel need(hashlib.sha256(path.read_bytes()).hexdigest() == pins[rel], f"pin {rel}") return json.loads(path.read_text()) diff --git a/research/pr4470-arithmetic-check/VERIFY.json b/research/pr4470-arithmetic-check/VERIFY.json index 1c75462df0..874e480d28 100644 --- a/research/pr4470-arithmetic-check/VERIFY.json +++ b/research/pr4470-arithmetic-check/VERIFY.json @@ -11,7 +11,7 @@ "-B", "{package}/verify.py" ], - "timeout_seconds": 120, + "timeout_seconds": 300, "checks": "#4470: p16 invoice totals and surplus 752, local change vs #4447 (53 fewer jobs, masses +37), surplus-gain polynomial (derivative certified negative on [0,1]), certified raw root bracket (0.0030201659770, 0.0030201659771), tails alpha/gamma/delta within limits and matching printed values. Logarithmic compiler conditions at ambient 145^1024 and sufficiency of H = 64,215,200,000,000. All nine outer rows from the printed parameters (FINE-PRIME formulas), binding row main_transform above kappa." } ] diff --git a/research/stage-zero-forced-translation/VERIFY.json b/research/stage-zero-forced-translation/VERIFY.json index c61ffecacf..14caecdd63 100644 --- a/research/stage-zero-forced-translation/VERIFY.json +++ b/research/stage-zero-forced-translation/VERIFY.json @@ -4,7 +4,9 @@ "python": "3.12", "requirements": [], "inputs": [ - "research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/direct-decoder/sources/DATA-PHASES.json" + "research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/direct-decoder/sources/DATA-PHASES.json", + "certificates/selected-result.json", + "docs/research/agent-task-catalog.json" ], "commands": [ { diff --git a/research/three-base-census-recount/VERIFY.json b/research/three-base-census-recount/VERIFY.json index 960cd5c092..50d723d8ae 100644 --- a/research/three-base-census-recount/VERIFY.json +++ b/research/three-base-census-recount/VERIFY.json @@ -5,7 +5,9 @@ "requirements": [], "inputs": [ "research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-CANONICAL.json.gz", - "research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-NATIVE.json.gz" + "research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-NATIVE.json.gz", + "certificates/selected-result.json", + "docs/research/agent-task-catalog.json" ], "commands": [ {