diff --git a/Makefile b/Makefile index 4035aaa7cb..0f0b0c1100 100644 --- a/Makefile +++ b/Makefile @@ -619,6 +619,14 @@ frontier1042-verify: selected-record-check @work=$$(mktemp -d "$${TMPDIR:-/tmp}/integer-mult-frontier1042.XXXXXX"); \ python3 -B scripts/verify_frontier1042.py --work "$$work/replay" +# Historical publication evidence; the live pointer has its own selected-record-check target. +.PHONY: frontier1042-capsule-closure-verify +frontier1042-capsule-closure-verify: + python3 -B research/frontier1042-capsule-closure-seed75/verify.py --check + python3 -O -B research/frontier1042-capsule-closure-seed75/verify.py --check + python3 -B research/frontier1042-capsule-closure-seed75/test_package.py + python3 -O -B research/frontier1042-capsule-closure-seed75/test_package.py + # Independent verification: code-disjoint T37 moment endpoints and kappa reduction (no new kappa). .PHONY: t37-endpoints-independent-verify t37-endpoints-independent-verify: diff --git a/research/frontier1042-capsule-closure-seed75/CLAIM.md b/research/frontier1042-capsule-closure-seed75/CLAIM.md new file mode 100644 index 0000000000..1f94dcde81 --- /dev/null +++ b/research/frontier1042-capsule-closure-seed75/CLAIM.md @@ -0,0 +1,10 @@ +# Sprint claim + +- Track 75–84, independent verification; OS-random seed **75**. +- Exact base: `ba82555c64e1879e4b7decce28186f208fcb8262`. +- Chosen object: closed, path-safe audit of the selected PR1042 replay capsule. +- Method: standard-library tar/SHA-256 checker; no extraction or construction imports. +- Deliverable: verifier, deterministic receipt, six integrity controls and three historical-record regression controls, exact pins and scope note; no new kappa. +- Stopping rule: all members and declared edges checked, all integrity controls reject, optimized run agrees, historical selected-record pins pass. Live selected-pointer validation remains separate. + +Candidates considered were invoice/outer arithmetic (overlapped PR1112), T16 owner/profile checking (overlapped prior audits), and capsule closure (chosen as distinct publication-evidence coverage). No pinned sprint coordination issue was found. diff --git a/research/frontier1042-capsule-closure-seed75/NOTICE.md b/research/frontier1042-capsule-closure-seed75/NOTICE.md new file mode 100644 index 0000000000..77cf8befd4 --- /dev/null +++ b/research/frontier1042-capsule-closure-seed75/NOTICE.md @@ -0,0 +1,3 @@ +New material: Copyright 2026 Martin Rv. Apache-2.0. +Prepared with substantial Perplexity AI assistance. PR1042/batch1047 construction, review and predecessor attribution remain with their original contributors and notices. +The historical-record portability fix, reproduction target, and regression controls were prepared with OpenAI Codex assistance. diff --git a/research/frontier1042-capsule-closure-seed75/PINS.json b/research/frontier1042-capsule-closure-seed75/PINS.json new file mode 100644 index 0000000000..1642ed9645 --- /dev/null +++ b/research/frontier1042-capsule-closure-seed75/PINS.json @@ -0,0 +1,13 @@ +{ + "schema": "integer-mult-frontier1042-capsule-closure-v1", + "assignment_seed": 75, + "base_commit": "ba82555c64e1879e4b7decce28186f208fcb8262", + "audited_source_head": "7e8ef087c02a77038a28a337a7ee3a77039cac0d", + "kappa": "1672188119205421/1000000000000000000", + "decimal": "0.001672188119205421", + "archive": {"path": "research/community-frontier1042-audit/selected-replay.tar.gz", "sha256": "22c3f4dce4b897a1d423d1388801933e288b6a6b1906cb15e1b16a5eb68db754", "members": 458, "declared_artifacts": 457, "expanded_bytes": 45647427}, + "selected_record": {"path": "SELECTED-RESULT.json", "sha256": "207d1f49f113c585024b9d3c17eadbb8b1be17c1321e3d190aabe2f18ce1c5b7", "source_path": "certificates/selected-result.json", "source_commit": "ba82555c64e1879e4b7decce28186f208fcb8262"}, + "integration_record": {"path": "docs/research/community-batch1047-integration.json", "sha256": "b04623d39df453804f327a203f07882554b138e6b322b9d1f674d84d94a14a8c"}, + "promoted_receipts": {"ASSEMBLY.json": "t16/ASSEMBLY.json", "BASELINE-BINDING.json": "BASELINE-BINDING.json", "INDEPENDENT-T16.json": "t16/INDEPENDENT-T16.json", "RESULT.json": "RESULT.json", "STAGES.json": "STAGES.json", "T16-REPLAY.json": "t16/REPLAY.json"}, + "stages": ["leaver-manifest", "slots-manifest", "t16-manifest", "base", "cells", "chain", "independent-leaver", "leaver-global", "slots", "t16"] +} diff --git a/research/frontier1042-capsule-closure-seed75/PROOF.md b/research/frontier1042-capsule-closure-seed75/PROOF.md new file mode 100644 index 0000000000..b4642fa493 --- /dev/null +++ b/research/frontier1042-capsule-closure-seed75/PROOF.md @@ -0,0 +1,11 @@ +# Closure argument + +Let `A` be the byte-pinned selected replay archive and `R` its archived `RESULT.json`. + +1. Every entry is a unique relative POSIX path, a bounded regular non-executable file; no extraction occurs. +2. `R.artifacts` equals `members(A) - {RESULT.json}` and every declared SHA-256 equals bytes read from `A`. The separately pinned archive digest binds the self-excluded result too. +3. `STAGES.json` equals `R.stages`; the ten fixed names, zero exit codes and log digests are checked. +4. Six promoted public receipts equal their archived bytes. +5. Exact frozen historical selected and integration record pins bind the value, source head, certificate, source manifest, archive and promoted receipts. The selected record is package-local data copied byte-for-byte from the pinned base; the live selected pointer is outside this historical audit. + +Therefore all 458 capsule bytes and stated publication edges are authenticated relative to `PINS.json`. This says nothing about execution history or the inherited multiplication theorem assumptions. diff --git a/research/frontier1042-capsule-closure-seed75/README.md b/research/frontier1042-capsule-closure-seed75/README.md new file mode 100644 index 0000000000..f58f2ee652 --- /dev/null +++ b/research/frontier1042-capsule-closure-seed75/README.md @@ -0,0 +1,46 @@ +# Independent PR1042 replay-capsule closure + +**Status:** independent verification; no new construction and no new kappa. + +This package independently checks the frozen publication capsule behind selected PR1042, conditional kappa `1672188119205421 / 10^18`. It was selected by OS-random seed **75** at base `ba82555c64e1879e4b7decce28186f208fcb8262`. + +## Result + +`verify.py` treats `research/community-frontier1042-audit/selected-replay.tar.gz` as untrusted data, uses only the Python standard library, never extracts a member, and imports no construction code. It authenticates 458 safe regular members (45,647,427 expanded bytes), all 457 declared artifact digests, exact inventory closure, ten successful stage/log bindings, six promoted receipts, and the selected/integration publication pins. + +`SELECTED-RESULT.json` is the byte-for-byte historical `certificates/selected-result.json` from base `ba82555c64e1879e4b7decce28186f208fcb8262`, also retained at `certificates/checkpoints/frontier1042.json`. Its original SHA-256, `207d1f49f113c585024b9d3c17eadbb8b1be17c1321e3d190aabe2f18ce1c5b7`, remains pinned in `PINS.json`. The checker reads this package-local snapshot. It does not read the live `certificates/selected-result.json`, so later selected frontiers do not invalidate this historical audit. + +## Reproduce + +```sh +make frontier1042-capsule-closure-verify +``` + +Expected final markers: `PASS_FRONTIER1042_CAPSULE_CLOSURE`, nine tests, `OK`. The target compares both normal and optimized verifier receipts byte-for-byte with the committed `RESULT.json`, then runs the suite in both modes so checks cannot depend on removable assertions. + +The same checks can be run directly with Python 3.9+: + +```sh +python3 -B research/frontier1042-capsule-closure-seed75/verify.py --check +python3 -O -B research/frontier1042-capsule-closure-seed75/verify.py --check +python3 -B research/frontier1042-capsule-closure-seed75/test_package.py +python3 -O -B research/frontier1042-capsule-closure-seed75/test_package.py +``` + +Current selected-pointer validation remains the separate `make selected-record-check` target. It is not a prerequisite of the historical capsule target. + +## Controls + +The suite rejects path traversal, duplicate members, undeclared members, mutated artifact bytes, a nonzero stage, and a promoted-receipt mismatch. + +Regression controls run the complete checker in an isolated fixture: it must pass with the live selected pointer absent or advanced to a later frontier, and reject mutated bytes in the frozen selected record. The original `RESULT.json` is unchanged. + +## Scope + +This is finite integrity and binding evidence about the committed capsule. It does not establish that recorded commands ran, independently recompute T16 mathematics, verify named source packages, discharge inherited interfaces, prove analytic transfer, benchmark multiplication, or formalize the full theorem. + +## Attribution + +Martin Rv (@martinxxx9), with substantial Perplexity AI assistance in research, implementation, verification and writing. It preserves all PR1042 and batch1047 predecessor attribution. Apache-2.0. + +The historical-record portability fix, reproduction target, and regression controls were prepared with OpenAI Codex assistance in response to the maintainer review. diff --git a/research/frontier1042-capsule-closure-seed75/RESULT.json b/research/frontier1042-capsule-closure-seed75/RESULT.json new file mode 100644 index 0000000000..95c1d7e617 --- /dev/null +++ b/research/frontier1042-capsule-closure-seed75/RESULT.json @@ -0,0 +1,22 @@ +{ + "status": "PASS_FRONTIER1042_CAPSULE_CLOSURE", + "assignment_seed": 75, + "base_commit": "ba82555c64e1879e4b7decce28186f208fcb8262", + "audited_source_head": "7e8ef087c02a77038a28a337a7ee3a77039cac0d", + "kappa": "1672188119205421/1000000000000000000", + "archive_sha256": "22c3f4dce4b897a1d423d1388801933e288b6a6b1906cb15e1b16a5eb68db754", + "members": 458, + "declared_artifacts": 457, + "expanded_bytes": 45647427, + "stages": 10, + "promoted_receipts": 6, + "controls": [ + "C1_path_traversal", + "C2_duplicate_member", + "C3_nondeclared_member", + "C4_mutated_artifact_digest", + "C5_nonzero_stage", + "C6_promoted_receipt_mismatch" + ], + "scope": "Independent standard-library, data-only finite closure audit of the frozen PR1042 selected replay capsule. Authenticates paths, complete bytes, receipt edges and publication pins; does not authenticate execution, replay construction code, all-size interfaces, analytic transfer or the multiplication theorem." +} diff --git a/research/frontier1042-capsule-closure-seed75/SELECTED-RESULT.json b/research/frontier1042-capsule-closure-seed75/SELECTED-RESULT.json new file mode 100644 index 0000000000..f451ced662 --- /dev/null +++ b/research/frontier1042-capsule-closure-seed75/SELECTED-RESULT.json @@ -0,0 +1,194 @@ +{ + "status": "Maintainer-reviewed conditional finite construction; see the integration receipt for publication and PR resolution status", + "kappa": "1672188119205421/1000000000000000000", + "decimal": "0.001672188119205421", + "source_prs": [ + 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-frontier1042-audit/SELECTED-SOURCE.json", + "certificate": "research/community-frontier1042-audit/ASSEMBLY.json", + "certificate_sha256": "093f35445812ea96fe1bfe6a3af7d769cb7f274e08f4fb30f71a17ed1161e54e", + "proof": "docs/research/community-batch1047-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": "52aa1d23641e4c716b43c98f6b883ad042087dd03a9d01369e8e6a735b07aa03", + "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" + }, + "review": "docs/research/community-batch1047-review.md", + "validation": "docs/research/community-batch1047-integration.json", + "reproduce": "make frontier1042-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": "1661960547713947/1000000000000000000", + "previous_record": "certificates/checkpoints/frontier942.json", + "audited_source_head": "7e8ef087c02a77038a28a337a7ee3a77039cac0d", + "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" + } +} diff --git a/research/frontier1042-capsule-closure-seed75/test_package.py b/research/frontier1042-capsule-closure-seed75/test_package.py new file mode 100644 index 0000000000..6ece284177 --- /dev/null +++ b/research/frontier1042-capsule-closure-seed75/test_package.py @@ -0,0 +1,100 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +import copy +from pathlib import Path +import shutil +import sys +import tarfile +import tempfile +import unittest +from unittest.mock import patch +sys.path.insert(0, str(Path(__file__).resolve().parent)) +import verify + +class FakeMember: + def __init__(self, name, size=0, mode=0o644, regular=True): + self.name, self.size, self.mode, self._regular = name, size, mode, regular + def isfile(self): return self._regular + +class NamespaceControls(unittest.TestCase): + def test_C1_path_traversal(self): + with self.assertRaisesRegex(ValueError, "unsafe archive"): + verify.validate_namespace([FakeMember("../escape")]) + def test_C2_duplicate_member(self): + with self.assertRaisesRegex(ValueError, "duplicate archive"): + verify.validate_namespace([FakeMember("a"), FakeMember("a")]) + +class ClosureControls(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.pins = verify.strict_json((verify.HERE / "PINS.json").read_bytes(), "PINS.json") + a = verify.ROOT / cls.pins["archive"]["path"] + cls.names, _, cls.digests, cls.roots = verify.read_capsule(a) + cls.result = verify.strict_json(cls.roots["RESULT.json"], "RESULT.json") + cls.stages = verify.strict_json(cls.roots["STAGES.json"], "STAGES.json") + def validate(self, result=None, stages=None, names=None, digests=None): + return verify.validate_result(result or self.result, stages or self.stages, + names or self.names, digests or self.digests, + self.pins["stages"]) + def test_C3_nondeclared_member(self): + result = copy.deepcopy(self.result); result["artifacts"].pop(next(iter(result["artifacts"]))) + with self.assertRaisesRegex(ValueError, "not exact archive closure"): self.validate(result=result) + def test_C4_mutated_artifact_digest(self): + digests = dict(self.digests); name = next(iter(self.result["artifacts"])); digests[name] = "0" * 64 + with self.assertRaisesRegex(ValueError, "artifact digest differs"): self.validate(digests=digests) + def test_C5_nonzero_stage(self): + stages = copy.deepcopy(self.stages); stages[0]["exit_code"] = 1 + result = copy.deepcopy(self.result); result["stages"] = stages + with self.assertRaisesRegex(ValueError, "recorded stage failed"): self.validate(result=result, stages=stages) + def test_C6_promoted_receipt_mismatch(self): + original = verify.repository_file + def mismatched_receipt(relative, expected=None): + data = original(relative, expected) + return data + b"x" if relative == "research/community-frontier1042-audit/ASSEMBLY.json" else data + with patch.object(verify, "repository_file", side_effect=mismatched_receipt): + with self.assertRaisesRegex(ValueError, "promoted receipt differs from capsule"): + verify.check(self.pins) + +class HistoricalSelectedControls(unittest.TestCase): + def setUp(self): + self.pins = verify.strict_json((verify.HERE / "PINS.json").read_bytes(), "PINS.json") + self.expected = verify.strict_json((verify.HERE / "RESULT.json").read_bytes(), "RESULT.json") + self.temporary = tempfile.TemporaryDirectory() + self.addCleanup(self.temporary.cleanup) + self.root = Path(self.temporary.name) + self.package = self.root / "research" / verify.HERE.name + self.package.mkdir(parents=True) + shutil.copyfile(verify.HERE / self.pins["selected_record"]["path"], + self.package / self.pins["selected_record"]["path"]) + paths = [self.pins["archive"]["path"], self.pins["integration_record"]["path"]] + paths.extend("research/community-frontier1042-audit/" + name + for name in self.pins["promoted_receipts"]) + selected = verify.strict_json(verify.package_file(self.pins["selected_record"]["path"], + self.pins["selected_record"]["sha256"]), "selected") + paths.append(selected["source_manifest"]) + for relative in paths: + target = self.root / relative + target.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(verify.ROOT / relative, target) + for name, value in (("ROOT", self.root), ("HERE", self.package)): + patcher = patch.object(verify, name, value) + patcher.start() + self.addCleanup(patcher.stop) + + def test_missing_live_selected_pointer_does_not_affect_history(self): + self.assertFalse((self.root / "certificates/selected-result.json").exists()) + self.assertEqual(verify.check(self.pins), self.expected) + + def test_advanced_live_selected_pointer_does_not_affect_history(self): + live = self.root / "certificates/selected-result.json" + live.parent.mkdir(parents=True) + live.write_text('{"kappa": "1672660197076918/1000000000000000000"}\n', encoding="utf-8") + self.assertEqual(verify.check(self.pins), self.expected) + + def test_mutated_frozen_selected_record_is_rejected(self): + frozen = self.package / self.pins["selected_record"]["path"] + frozen.write_bytes(frozen.read_bytes() + b"x") + with self.assertRaisesRegex(ValueError, "package pin differs: SELECTED-RESULT.json"): + verify.check(self.pins) + +if __name__ == "__main__": unittest.main(verbosity=2) diff --git a/research/frontier1042-capsule-closure-seed75/verify.py b/research/frontier1042-capsule-closure-seed75/verify.py new file mode 100644 index 0000000000..3ab556e1b3 --- /dev/null +++ b/research/frontier1042-capsule-closure-seed75/verify.py @@ -0,0 +1,204 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Independent data-only closure audit of the selected PR1042 replay capsule.""" +import argparse +from hashlib import sha256 +import json +from pathlib import Path, PurePosixPath +import re +import tarfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +HEX64 = re.compile(r"[0-9a-f]{64}") +MAX_MEMBERS = 1000 +MAX_MEMBER_BYTES = 8 * 1024 * 1024 +MAX_TOTAL_BYTES = 64 * 1024 * 1024 +ROOT_MEMBERS = { + "RESULT.json", "STAGES.json", "BASELINE-BINDING.json", + "t16/ASSEMBLY.json", "t16/INDEPENDENT-T16.json", "t16/REPLAY.json", +} + +def require(ok, message): + if not ok: + raise ValueError(message) + +def digest(data): + return sha256(data).hexdigest() + +def strict_json(data, label): + def no_duplicates(pairs): + out = {} + for key, value in pairs: + require(key not in out, f"duplicate JSON key in {label}: {key}") + out[key] = value + return out + try: + return json.loads(data, object_pairs_hook=no_duplicates) + except (UnicodeDecodeError, json.JSONDecodeError) as exc: + raise ValueError(f"invalid JSON in {label}: {exc}") from exc + +def safe_name(name): + require(type(name) is str and name and "\\" not in name and ":" not in name, + "invalid archive member path") + p = PurePosixPath(name) + require(not p.is_absolute() and p.as_posix() == name and + all(part not in ("", ".", "..") for part in p.parts), + "unsafe archive member path: " + name) + return name + +def validate_namespace(members): + require(type(members) is list and len(members) <= MAX_MEMBERS, + "archive member limit exceeded") + names, total = [], 0 + for member in members: + name = safe_name(member.name) + require(member.isfile(), "archive member is not a regular file: " + name) + require(type(member.size) is int and 0 <= member.size <= MAX_MEMBER_BYTES, + "archive member size limit exceeded: " + name) + require(member.mode & 0o111 == 0, "archive member is executable: " + name) + names.append(name) + total += member.size + require(len(names) == len(set(names)), "duplicate archive member name") + require(total <= MAX_TOTAL_BYTES, "expanded archive size limit exceeded") + return names, total + +def read_capsule(path): + raw_roots, member_digests = {}, {} + with tarfile.open(path, "r:gz") as archive: + members = archive.getmembers() + names, total = validate_namespace(members) + for member in members: + stream = archive.extractfile(member) + require(stream is not None, "archive regular file is unreadable: " + member.name) + payload = stream.read(MAX_MEMBER_BYTES + 1) + require(len(payload) == member.size, "archive member length differs: " + member.name) + member_digests[member.name] = digest(payload) + if member.name in ROOT_MEMBERS: + raw_roots[member.name] = payload + require(ROOT_MEMBERS <= set(raw_roots), "required root receipt missing") + return names, total, member_digests, raw_roots + +def validate_result(result, stages, names, member_digests, expected_stages): + require(type(result) is dict and result.get("status") == "PASS_COMPLETE_PR1042_COMPOSITION", + "unexpected capsule result status") + artifacts = result.get("artifacts") + require(type(artifacts) is dict, "artifact inventory is not an object") + require(set(artifacts) == set(names) - {"RESULT.json"}, + "RESULT artifact inventory is not exact archive closure") + for name, expected in artifacts.items(): + require(type(expected) is str and HEX64.fullmatch(expected) is not None, + "invalid artifact digest: " + name) + require(member_digests[name] == expected, "artifact digest differs: " + name) + recorded_stages = result.get("stages") + require(type(recorded_stages) is list and recorded_stages == stages, + "STAGES.json differs from RESULT stages") + require([item.get("name") for item in stages] == expected_stages, + "stage sequence differs") + for item in stages: + name = item.get("name") + require(type(item.get("exit_code")) is int and item["exit_code"] == 0, + "recorded stage failed: " + str(name)) + expected = item.get("log_sha256") + require(type(expected) is str and HEX64.fullmatch(expected) is not None, + "invalid stage log digest: " + str(name)) + log_name = name + ".log" + require(log_name in member_digests and member_digests[log_name] == expected, + "stage log binding differs: " + str(name)) + return len(artifacts) + +def repository_file(relative, expected=None): + require(type(relative) is str, "invalid repository path") + path = (ROOT / relative).resolve() + require(path.is_relative_to(ROOT.resolve()) and path.is_file(), + "missing repository file: " + relative) + data = path.read_bytes() + if expected is not None: + require(digest(data) == expected, "repository pin differs: " + relative) + return data + +def package_file(relative, expected): + require(type(relative) is str, "invalid package path") + path = (HERE / relative).resolve() + require(path.is_relative_to(HERE.resolve()) and path.is_file(), + "missing package file: " + relative) + data = path.read_bytes() + require(digest(data) == expected, "package pin differs: " + relative) + return data + +def check(pins): + require(pins.get("schema") == "integer-mult-frontier1042-capsule-closure-v1", + "unsupported pins schema") + archive_pin = pins["archive"] + archive_raw = repository_file(archive_pin["path"], archive_pin["sha256"]) + names, expanded, member_digests, roots = read_capsule(ROOT / archive_pin["path"]) + require(len(names) == archive_pin["members"] and expanded == archive_pin["expanded_bytes"], + "archive count or expanded size differs") + result = strict_json(roots["RESULT.json"], "RESULT.json") + stages = strict_json(roots["STAGES.json"], "STAGES.json") + artifact_count = validate_result(result, stages, names, member_digests, pins["stages"]) + require(artifact_count == archive_pin["declared_artifacts"], "artifact count differs") + require(result.get("kappa") == pins["kappa"] and result.get("decimal") == pins["decimal"], + "capsule selected value differs") + promoted_hashes = {} + for outer, inner in pins["promoted_receipts"].items(): + outer_data = repository_file("research/community-frontier1042-audit/" + outer) + require(outer_data == roots[inner], "promoted receipt differs from capsule: " + outer) + promoted_hashes[outer] = digest(outer_data) + selected_pin = pins["selected_record"] + selected = strict_json(package_file(selected_pin["path"], selected_pin["sha256"]), selected_pin["path"]) + require(selected.get("audited_source_head") == pins["audited_source_head"], "audited source head differs") + require(selected.get("kappa") == pins["kappa"] and selected.get("decimal") == pins["decimal"], + "published selected value differs") + require(selected.get("certificate") == "research/community-frontier1042-audit/ASSEMBLY.json", + "selected certificate path differs") + require(selected.get("certificate_sha256") == promoted_hashes["ASSEMBLY.json"], + "selected certificate digest differs") + integration_pin = pins["integration_record"] + integration = strict_json(repository_file(integration_pin["path"], integration_pin["sha256"]), integration_pin["path"]) + receipts = integration.get("receipts") + require(type(receipts) is dict, "integration receipt map missing") + require(receipts.get(archive_pin["path"]) == digest(archive_raw), "integration archive digest differs") + for outer, expected in promoted_hashes.items(): + relative = "research/community-frontier1042-audit/" + outer + require(receipts.get(relative) == expected, "integration promoted digest differs: " + outer) + source_path = selected.get("source_manifest") + source_data = repository_file(source_path) + require(receipts.get(source_path) == digest(source_data), "integration source manifest digest differs") + require(result.get("baseline_binding_sha256") == promoted_hashes["BASELINE-BINDING.json"], + "capsule baseline binding differs") + require(result.get("selected_assembly_sha256") == promoted_hashes["ASSEMBLY.json"], + "capsule selected assembly binding differs") + return { + "status": "PASS_FRONTIER1042_CAPSULE_CLOSURE", + "assignment_seed": pins["assignment_seed"], "base_commit": pins["base_commit"], + "audited_source_head": pins["audited_source_head"], "kappa": pins["kappa"], + "archive_sha256": digest(archive_raw), "members": len(names), + "declared_artifacts": artifact_count, "expanded_bytes": expanded, + "stages": len(stages), "promoted_receipts": len(promoted_hashes), + "controls": ["C1_path_traversal", "C2_duplicate_member", "C3_nondeclared_member", + "C4_mutated_artifact_digest", "C5_nonzero_stage", "C6_promoted_receipt_mismatch"], + "scope": "Independent standard-library, data-only finite closure audit of the frozen PR1042 selected replay capsule. Authenticates paths, complete bytes, receipt edges and publication pins; does not authenticate execution, replay construction code, all-size interfaces, analytic transfer or the multiplication theorem." + } + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument("--out", type=Path) + ap.add_argument("--check", action="store_true", + help="require byte equality with the committed RESULT.json") + args = ap.parse_args() + pins = strict_json((HERE / "PINS.json").read_bytes(), "PINS.json") + receipt = check(pins) + raw = (json.dumps(receipt, indent=2) + "\n").encode() + if args.check: + require(raw == (HERE / "RESULT.json").read_bytes(), "committed receipt differs") + if args.out: + args.out.write_bytes(raw) + print(raw.decode(), end="") + print(receipt["status"]) + +if __name__ == "__main__": + try: + main() + except (KeyError, OSError, ValueError, tarfile.TarError) as exc: + raise SystemExit("FAIL: " + str(exc)) from exc