PF-Core production kernel: claim classes, Lean research, CI fixes

.gitattributes

@@ -0,0 +1,5 @@
+# Normalize line endings for fixtures hashed on Linux CI.
+examples/** text eol=lf
+benchmarks/** text eol=lf
+test_vectors/** text eol=lf
+lean/** text eol=lf

.github/workflows/ci.yml

@@ -87,15 +87,20 @@ jobs:
           cd python
           pip install -e .
           if command -v certifyedge >/dev/null 2>&1; then
+            echo "CertifyEdge CLI found: $(command -v certifyedge)"
+            certifyedge --version || true
             pcs pf-core certifyedge-check \
               --trace ../examples/pf-core-valid/labtrust_replay/trace.json \
               --property qc_release.temporal.safety \
-              --out /tmp/PFCoreCertificate.certifyedge.json || \
-            PCS_CERTIFYEDGE_MOCK=1 pcs pf-core certifyedge-check \
-              --trace ../examples/pf-core-valid/labtrust_replay/trace.json \
-              --property qc_release.temporal.safety \
-              --out /tmp/PFCoreCertificate.certifyedge.json
+              --out /tmp/PFCoreCertificate.certifyedge.json || {
+              echo "WARNING: live CertifyEdge check failed; falling back to mock"
+              PCS_CERTIFYEDGE_MOCK=1 pcs pf-core certifyedge-check \
+                --trace ../examples/pf-core-valid/labtrust_replay/trace.json \
+                --property qc_release.temporal.safety \
+                --out /tmp/PFCoreCertificate.certifyedge.json
+            }
           else
+            echo "WARNING: certifyedge not on PATH; using PCS_CERTIFYEDGE_MOCK=1"
             PCS_CERTIFYEDGE_MOCK=1 pcs pf-core certifyedge-check \
               --trace ../examples/pf-core-valid/labtrust_replay/trace.json \
               --property qc_release.temporal.safety \
@@ -125,13 +130,17 @@ jobs:
         run: curl -sSfL https://github.com/leanprover/elan/releases/download/v4.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz && ./elan-init -y --default-toolchain none
       - name: Build Lean libraries and PF-Core lean-check
         run: |
+          export PATH="$HOME/.elan/bin:$PATH"
           cd lean
           elan default leanprover/lean4:v4.14.0
           lake build PCS
           lake build PFCore
           cd ../python
           pip install -e .
-          pcs pf-core lean-check --trace ../examples/pf-core-valid/tool_use_trace_compiled/pfcore_trace.json
+          pcs pf-core lean-check --trace ../examples/pf-core-valid/tool_use_trace_compiled/pfcore_trace.json --out /tmp/pfcore-ci-cert.json
+          pcs pf-core verify-proof-binding \
+            --certificate /tmp/pfcore-ci-cert.json \
+            --trace ../examples/pf-core-valid/tool_use_trace_compiled/pfcore_trace.json
           pcs pf-core validate-contracts \
             ../examples/pf-core-valid/contract_checked/trace.json \
             --contracts-dir ../examples/pf-core-valid/contract_checked

benchmarks/computation-reproducibility/expected_reports/benchmark_report.computation-reproducibility-v0.v0.json

@@ -46,11 +46,11 @@
       "denominator": 2.0,
       "coverage_ratio": 0.7,
       "details": {
-        "registry_entry_count": 38
+        "registry_entry_count": 49
       },
       "source_repo": "https://github.com/SentinelOps-CI/pcs-core",
       "source_commit": "d444444444444444444444444444444444444444",
-      "signature_or_digest": "sha256:f7a35b8bfa1db2f23acc34db7698cbf8537905015aaee5982e9b7c9457f9ec11"
+      "signature_or_digest": "sha256:68b662bc594764cb4ba4c1596a61e4f6b82c18c3382e240e9861f27f7b7292a9"
     },
     "formal_checks": {
       "schema_version": "v0",
@@ -194,11 +194,11 @@
   "failures": [],
   "source_repo": "https://github.com/SentinelOps-CI/pcs-core",
   "source_commit": "d444444444444444444444444444444444444444",
-  "signature_or_digest": "sha256:9e4f85897ca54facb2d79a53ad3eb6ef84402dbdd23b6166d78831080eccabed",
+  "signature_or_digest": "sha256:d8a650e16939d91fe4e05de9ecb8beda0b77b07fca3e652bbf8ad76b6f40abe9",
   "conformance_refs": [
     {
       "suite": "computation",
-      "run_id": "conf-run-computation-20260521T112227Z",
+      "run_id": "conf-run-computation-20260628T004834Z",
       "status": "passed"
     }
   ]

benchmarks/computation-reproducibility/expected_reports/benchmark_report.v0.json

@@ -46,11 +46,11 @@
       "denominator": 2.0,
       "coverage_ratio": 0.7,
       "details": {
-        "registry_entry_count": 38
+        "registry_entry_count": 49
       },
       "source_repo": "https://github.com/SentinelOps-CI/pcs-core",
       "source_commit": "d444444444444444444444444444444444444444",
-      "signature_or_digest": "sha256:f7a35b8bfa1db2f23acc34db7698cbf8537905015aaee5982e9b7c9457f9ec11"
+      "signature_or_digest": "sha256:68b662bc594764cb4ba4c1596a61e4f6b82c18c3382e240e9861f27f7b7292a9"
     },
     "formal_checks": {
       "schema_version": "v0",
@@ -194,11 +194,11 @@
   "failures": [],
   "source_repo": "https://github.com/SentinelOps-CI/pcs-core",
   "source_commit": "d444444444444444444444444444444444444444",
-  "signature_or_digest": "sha256:9e4f85897ca54facb2d79a53ad3eb6ef84402dbdd23b6166d78831080eccabed",
+  "signature_or_digest": "sha256:d8a650e16939d91fe4e05de9ecb8beda0b77b07fca3e652bbf8ad76b6f40abe9",
   "conformance_refs": [
     {
       "suite": "computation",
-      "run_id": "conf-run-computation-20260521T112227Z",
+      "run_id": "conf-run-computation-20260628T004834Z",
       "status": "passed"
     }
   ]

benchmarks/computation-reproducibility/input_releases/invalid-witness-hash/README.md

@@ -1,19 +1,36 @@
-# Scientific computation reproducibility release train
+# Computation reproducibility release fixtures
 
-Conformance fixture for workflow `scientific_computation.reproducibility_v0`.
+Release fixtures for workflow `scientific_computation.reproducibility_v0` document computation witnesses and release-chain validation for the reproducibility profile.
+
+The workflow profile appears in `examples/workflow_profiles/scientific_computation_reproducibility.valid.json`, and the guide is [docs/workflow-profiles.md](../../docs/workflow-profiles.md).
 
 ## Artifacts
 
-- Runtime: `dataset_receipt.json`, `environment_receipt.json`, `computation_run_receipt.json`, `result_artifact.json`
-- Certificate: `computation_witness.json`
-- PCS chain: `science_claim_bundle.certified.json`, `verification_result.json`, `signed_science_claim_bundle.json`, `release_manifest.v0.json`, `release_chain_validation_result.v0.json`
+| File | Type |
+|------|------|
+| `dataset_receipt.json` | `DatasetReceipt.v0` |
+| `environment_receipt.json` | `EnvironmentReceipt.v0` |
+| `computation_run_receipt.json` | `ComputationRunReceipt.v0` |
+| `result_artifact.json` | `ResultArtifact.v0` |
+| `computation_witness.json` | `ComputationWitness.v0` |
+| `science_claim_bundle.certified.json` | `ScienceClaimBundle.v0` |
+| `verification_result.json` | `VerificationResult.v0` |
+| `signed_science_claim_bundle.json` | `SignedScienceClaimBundle.v0` |
+| `release_manifest.v0.json` | `ReleaseManifest.v0` |
+| `release_chain_validation_result.v0.json` | `ReleaseChainValidationResult.v0` |
+
+## Validate
+
+```bash
+pcs validate-release-chain examples/computation-release/
+pcs conformance run --suite computation
+```
 
-Regenerate:
+Regenerate through the Python materialize script.
 
 ```bash
 cd python
 python scripts/materialize_computation_fixtures.py
-pcs validate-release-chain ../examples/computation-release/
 ```
 
-Invalid negative cases: `examples/computation-release-invalid/` (one failure class per directory).
+Invalid cases live under `examples/computation-release-invalid/` with one failure class per directory.

benchmarks/computation-reproducibility/input_releases/invalid-witness-hash/RELEASE_FIXTURE_MANIFEST.json

@@ -9,14 +9,14 @@
   "provability_fabric_commit": "c333333333333333333333333333333333333333",
   "scientific_memory_commit": "d444444444444444444444444444444444444444",
   "artifacts": {
-    "dataset_receipt.json": "sha256:d54994e19c32caeb7508edbb73a14efc94341ffd93013873af527e180385dfec",
-    "environment_receipt.json": "sha256:6335e612b739e925d74ca94a39690380f8be7c9db836fcad4c8ff0ba8b6c98ae",
-    "computation_run_receipt.json": "sha256:c14b4fed421343459ad081e74f7b613b39b6bca803eca27ffde0fdda1a8dd12a",
-    "result_artifact.json": "sha256:a38eeaab2b0cd104ac461b6a061bfa09e4f797253c27173107452a5acd9c42ed",
-    "computation_witness.json": "sha256:a86081703ca5bc521445cc5a38826adfc1ca55f87f52f35b3c429a2bbdaf13f9",
-    "science_claim_bundle.certified.json": "sha256:c47168f2de32da5f25407f34ab66cba9e853390e22108bf56ea24712343fd60d",
-    "verification_result.json": "sha256:59c45c6e24cbca96489cfdefc0b156c39bec252b53b09e8f1d8b7b48fa88676f",
-    "signed_science_claim_bundle.json": "sha256:6995cdbdcb788d7e570093db3fd204072d69bd07c03390dce2f5a3a1490bf2ea",
-    "scientific_memory_import_report.json": "sha256:21fa9d915b7f313a3e9d1b1fdf4bdd2815bbd06404ae9699518bd5e367bca41e"
+    "dataset_receipt.json": "sha256:f94a4a839cea893cd0abeea758326e0e28f01a293b6ac87f8436ca5cca753e79",
+    "environment_receipt.json": "sha256:c01a8f055da8965e01c1172eb7ff9f58e702619261a6d6159e24ee861e134598",
+    "computation_run_receipt.json": "sha256:567e0adeec5bc61786efa529dcb777f5ac2ddda1f8cb1160d67e5638405cbd4a",
+    "result_artifact.json": "sha256:a2b8d26f9d0e056e7fd963156021a88b43c764c84357e2ff8ae70cd2c2d99acc",
+    "computation_witness.json": "sha256:b89def93118f055abb45b8b0187e2aaeb452ec6eae502c9ba9bbf7ded83377cb",
+    "science_claim_bundle.certified.json": "sha256:5a6a675d23354d219e85daec27a89443d8648d158249e86c48b99528b4412643",
+    "verification_result.json": "sha256:f78c35d74928bb139e2d507424a022f2dfa78fcc2e1a67ccd4adeb0f51e0b43c",
+    "signed_science_claim_bundle.json": "sha256:e6419afb62cf88f2ae12f5f8bf58fc7ebde8cf7f2f28b61c9aea1a2aba889c4a",
+    "scientific_memory_import_report.json": "sha256:ba324c85c2aee78e1893c7b667e8580cbeede842b7027d42b9474b8c9dafbe70"
   }
 }

benchmarks/computation-reproducibility/input_releases/invalid-witness-hash/handoff_manifest.bundle_to_verifier.v0.json

@@ -10,7 +10,7 @@
   "input_artifacts": {
     "science_claim_bundle.certified.json": {
       "artifact_type": "ScienceClaimBundle.v0",
-      "sha256": "sha256:c47168f2de32da5f25407f34ab66cba9e853390e22108bf56ea24712343fd60d"
+      "sha256": "sha256:5a6a675d23354d219e85daec27a89443d8648d158249e86c48b99528b4412643"
     }
   },
   "expected_outputs": {
@@ -24,8 +24,8 @@
   "invariants": {
     "witness_id": "witness-sci-comp-repro-001",
     "run_receipt_hash": "sha256:9c74749d2ad46c6a60394db676e5527929f9b7bef9a012439d6d14b26d960828",
-    "certified_bundle_hash": "sha256:c47168f2de32da5f25407f34ab66cba9e853390e22108bf56ea24712343fd60d"
+    "certified_bundle_hash": "sha256:5a6a675d23354d219e85daec27a89443d8648d158249e86c48b99528b4412643"
   },
   "status": "Validated",
-  "signature_or_digest": "sha256:3db04a8c9656ed55c3efbc7bb08ebd2a606d9b26f21f492d201e0071c8b7e968"
+  "signature_or_digest": "sha256:91f0cdb6ab949b0ab706bcbf64281bac53f48083476944d1ef3a09a29d4e5a0e"
 }

benchmarks/computation-reproducibility/input_releases/invalid-witness-hash/handoff_manifest.certificate_to_bundle.v0.json

@@ -10,7 +10,7 @@
   "input_artifacts": {
     "computation_witness.json": {
       "artifact_type": "ComputationWitness.v0",
-      "sha256": "sha256:a86081703ca5bc521445cc5a38826adfc1ca55f87f52f35b3c429a2bbdaf13f9"
+      "sha256": "sha256:b89def93118f055abb45b8b0187e2aaeb452ec6eae502c9ba9bbf7ded83377cb"
     }
   },
   "expected_outputs": {
@@ -23,5 +23,5 @@
     "run_receipt_hash": "sha256:9c74749d2ad46c6a60394db676e5527929f9b7bef9a012439d6d14b26d960828"
   },
   "status": "Validated",
-  "signature_or_digest": "sha256:e2170d91b655ae0d9ae9b8f6a18fa78f9801d76213bd8e5bfba577ac7599f501"
+  "signature_or_digest": "sha256:170b7a0dfa9132870f4a7f96de1b4e9cb483c7ea6a354d8162e452a6b151543c"
 }

benchmarks/computation-reproducibility/input_releases/invalid-witness-hash/handoff_manifest.runtime_to_certificate.v0.json

@@ -10,19 +10,19 @@
   "input_artifacts": {
     "dataset_receipt.json": {
       "artifact_type": "DatasetReceipt.v0",
-      "sha256": "sha256:d54994e19c32caeb7508edbb73a14efc94341ffd93013873af527e180385dfec"
+      "sha256": "sha256:f94a4a839cea893cd0abeea758326e0e28f01a293b6ac87f8436ca5cca753e79"
     },
     "environment_receipt.json": {
       "artifact_type": "EnvironmentReceipt.v0",
-      "sha256": "sha256:6335e612b739e925d74ca94a39690380f8be7c9db836fcad4c8ff0ba8b6c98ae"
+      "sha256": "sha256:c01a8f055da8965e01c1172eb7ff9f58e702619261a6d6159e24ee861e134598"
     },
     "computation_run_receipt.json": {
       "artifact_type": "ComputationRunReceipt.v0",
-      "sha256": "sha256:c14b4fed421343459ad081e74f7b613b39b6bca803eca27ffde0fdda1a8dd12a"
+      "sha256": "sha256:567e0adeec5bc61786efa529dcb777f5ac2ddda1f8cb1160d67e5638405cbd4a"
     },
     "result_artifact.json": {
       "artifact_type": "ResultArtifact.v0",
-      "sha256": "sha256:a38eeaab2b0cd104ac461b6a061bfa09e4f797253c27173107452a5acd9c42ed"
+      "sha256": "sha256:a2b8d26f9d0e056e7fd963156021a88b43c764c84357e2ff8ae70cd2c2d99acc"
     }
   },
   "expected_outputs": {
@@ -35,5 +35,5 @@
     "dataset_hash": "sha256:84c9037231eef6a1742c1d6d0a043878b4de8395397c168026450d8ca9e647e3"
   },
   "status": "Validated",
-  "signature_or_digest": "sha256:bafff8665c39e3662b34563a34671f518639fbb46853d889925a537a964c1b41"
+  "signature_or_digest": "sha256:00a3731d61029e4ae124bd4503e3eae35eb7b1c271cf3f5f3930cfe2a89e137f"
 }

benchmarks/computation-reproducibility/input_releases/invalid-witness-hash/handoff_manifest.signed_bundle_to_memory.v0.json

@@ -10,7 +10,7 @@
   "input_artifacts": {
     "signed_science_claim_bundle.json": {
       "artifact_type": "SignedScienceClaimBundle.v0",
-      "sha256": "sha256:6995cdbdcb788d7e570093db3fd204072d69bd07c03390dce2f5a3a1490bf2ea"
+      "sha256": "sha256:e6419afb62cf88f2ae12f5f8bf58fc7ebde8cf7f2f28b61c9aea1a2aba889c4a"
     }
   },
   "expected_outputs": {
@@ -23,5 +23,5 @@
     "claim_id": "claim-qc-release-v0.1"
   },
   "status": "Validated",
-  "signature_or_digest": "sha256:68159cf6671e21245b197912e054410bf50e39b068e25c0eb66ecc73fca10250"
+  "signature_or_digest": "sha256:d7040e584b65b50f2b17d467f6ca7dd1e098f818dc72e7158e0bcd009b400f71"
 }

benchmarks/computation-reproducibility/input_releases/invalid-witness-hash/handoff_to_certifyedge.json

@@ -10,19 +10,19 @@
   "input_artifacts": {
     "dataset_receipt.json": {
       "artifact_type": "DatasetReceipt.v0",
-      "sha256": "sha256:d54994e19c32caeb7508edbb73a14efc94341ffd93013873af527e180385dfec"
+      "sha256": "sha256:f94a4a839cea893cd0abeea758326e0e28f01a293b6ac87f8436ca5cca753e79"
     },
     "environment_receipt.json": {
       "artifact_type": "EnvironmentReceipt.v0",
-      "sha256": "sha256:6335e612b739e925d74ca94a39690380f8be7c9db836fcad4c8ff0ba8b6c98ae"
+      "sha256": "sha256:c01a8f055da8965e01c1172eb7ff9f58e702619261a6d6159e24ee861e134598"
     },
     "computation_run_receipt.json": {
       "artifact_type": "ComputationRunReceipt.v0",
-      "sha256": "sha256:c14b4fed421343459ad081e74f7b613b39b6bca803eca27ffde0fdda1a8dd12a"
+      "sha256": "sha256:567e0adeec5bc61786efa529dcb777f5ac2ddda1f8cb1160d67e5638405cbd4a"
     },
     "result_artifact.json": {
       "artifact_type": "ResultArtifact.v0",
-      "sha256": "sha256:a38eeaab2b0cd104ac461b6a061bfa09e4f797253c27173107452a5acd9c42ed"
+      "sha256": "sha256:a2b8d26f9d0e056e7fd963156021a88b43c764c84357e2ff8ae70cd2c2d99acc"
     }
   },
   "expected_outputs": {
@@ -35,5 +35,5 @@
     "dataset_hash": "sha256:84c9037231eef6a1742c1d6d0a043878b4de8395397c168026450d8ca9e647e3"
   },
   "status": "Validated",
-  "signature_or_digest": "sha256:bafff8665c39e3662b34563a34671f518639fbb46853d889925a537a964c1b41"
+  "signature_or_digest": "sha256:00a3731d61029e4ae124bd4503e3eae35eb7b1c271cf3f5f3930cfe2a89e137f"
 }

benchmarks/computation-reproducibility/input_releases/invalid-witness-hash/handoff_to_pf.json

@@ -10,7 +10,7 @@
   "input_artifacts": {
     "science_claim_bundle.certified.json": {
       "artifact_type": "ScienceClaimBundle.v0",
-      "sha256": "sha256:c47168f2de32da5f25407f34ab66cba9e853390e22108bf56ea24712343fd60d"
+      "sha256": "sha256:5a6a675d23354d219e85daec27a89443d8648d158249e86c48b99528b4412643"
     }
   },
   "expected_outputs": {
@@ -24,8 +24,8 @@
   "invariants": {
     "witness_id": "witness-sci-comp-repro-001",
     "run_receipt_hash": "sha256:9c74749d2ad46c6a60394db676e5527929f9b7bef9a012439d6d14b26d960828",
-    "certified_bundle_hash": "sha256:c47168f2de32da5f25407f34ab66cba9e853390e22108bf56ea24712343fd60d"
+    "certified_bundle_hash": "sha256:5a6a675d23354d219e85daec27a89443d8648d158249e86c48b99528b4412643"
   },
   "status": "Validated",
-  "signature_or_digest": "sha256:3db04a8c9656ed55c3efbc7bb08ebd2a606d9b26f21f492d201e0071c8b7e968"
+  "signature_or_digest": "sha256:91f0cdb6ab949b0ab706bcbf64281bac53f48083476944d1ef3a09a29d4e5a0e"
 }

benchmarks/computation-reproducibility/input_releases/invalid-witness-hash/lean_check_result.v0.json

@@ -5,7 +5,7 @@
   "lean_module": "PCS.Theorems",
   "lean_theorem": "ReleaseChainAdmissible",
   "status": "ProofChecked",
-  "checked_at": "2026-05-19T13:37:27Z",
+  "checked_at": "2026-06-28T00:48:30Z",
   "lean_version": "leanprover/lean4:stable",
   "source_repo": "https://github.com/SentinelOps-CI/pcs-core",
   "source_commit": "d444444444444444444444444444444444444444",
@@ -33,5 +33,5 @@
       "failure_reason": ""
     }
   ],
-  "signature_or_digest": "sha256:fd47f305ab323dffeee4f60ebd3ac164563ca784b0199842f23b7fec315df397"
+  "signature_or_digest": "sha256:46006f2dbeb6b1ed7d4840e085dbbdd7e1c3c977b24d0ea8e0af50878206365d"
 }

benchmarks/computation-reproducibility/input_releases/invalid-witness-hash/proof_obligation.v0.json

@@ -22,17 +22,17 @@
       "kind": "VerificationAdmitsBundle",
       "inputs": {
         "verification_status": "ProofChecked",
-        "verified_input_bundle_hash": "sha256:c47168f2de32da5f25407f34ab66cba9e853390e22108bf56ea24712343fd60d",
-        "certified_bundle_hash": "sha256:c47168f2de32da5f25407f34ab66cba9e853390e22108bf56ea24712343fd60d",
+        "verified_input_bundle_hash": "sha256:5a6a675d23354d219e85daec27a89443d8648d158249e86c48b99528b4412643",
+        "certified_bundle_hash": "sha256:5a6a675d23354d219e85daec27a89443d8648d158249e86c48b99528b4412643",
         "release_blocking_checks_passed": true
       }
     },
     {
       "obligation_id": "signed_bundle_admissible",
       "kind": "SignedBundleAdmissible",
       "inputs": {
-        "signed_input_bundle_hash": "sha256:c47168f2de32da5f25407f34ab66cba9e853390e22108bf56ea24712343fd60d",
-        "verified_input_bundle_hash": "sha256:c47168f2de32da5f25407f34ab66cba9e853390e22108bf56ea24712343fd60d"
+        "signed_input_bundle_hash": "sha256:5a6a675d23354d219e85daec27a89443d8648d158249e86c48b99528b4412643",
+        "verified_input_bundle_hash": "sha256:5a6a675d23354d219e85daec27a89443d8648d158249e86c48b99528b4412643"
       }
     }
   ],
@@ -61,5 +61,5 @@
   "lean_module": "PCS.Theorems",
   "source_repo": "https://github.com/SentinelOps-CI/pcs-core",
   "source_commit": "d444444444444444444444444444444444444444",
-  "signature_or_digest": "sha256:8b5791def92cff90bb899cf228e7a26d3305e8e141fae361d698c23bb2dd14b6"
+  "signature_or_digest": "sha256:8f3640d982b551859055d5fb1f351b8f099bc3b3f5b6c9feda56bee69aaa6c83"
 }