SentinelOps-CI · fraware · Jun 27, 2026 · Jun 19, 2026 · Jun 19, 2026 · Jun 19, 2026
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -17,9 +17,15 @@ jobs:
         run: |
           cd python
           pip install -e ".[dev]"
+          pytest -q tests/test_pf_core_stage1.py tests/test_pf_core_stage2.py tests/test_pf_core_stage3.py
+          pytest -q tests/test_pf_core_phase_f.py
           pytest -q
           pytest -q tests/test_protocol_conformance.py
           pcs schema check
+          pcs pf-core audit-claims
+          pcs pf-core audit-boundary
+          pcs pf-core audit-lean-catalog
+          pcs pf-core audit-lean-no-sorry
           pcs examples check
           pcs validate-release-chain ../examples/labtrust-release/
           pcs validate-release-chain ../examples/labtrust-release/ --json > /dev/null
@@ -69,13 +75,50 @@ jobs:
           pytest -q tests/test_multidomain_workflows.py
           ruff check pcs_core tests
           ruff format --check pcs_core tests
+      - name: PF-Core fixture validation
+        run: |
+          cd python
+          pip install -e .
+          pcs validate ../examples/pf-core-valid/tool_use_trace_compiled/pfcore_trace.json
+          pcs pf-core validate-trace ../examples/pf-core-valid/tool_use_trace_compiled/pfcore_trace.json
+      - name: PF-Core CertifyEdge mock check (Phase F3)
+        run: |
+          cd python
+          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
       - name: Schema drift check (reference)
         run: bash scripts/pcs-schema-diff.sh schemas
+      - name: PF-Core hash vector parity (Phase 7)
+        run: bash scripts/verify-pf-core-hash-vectors.sh python/tests/hash_vectors
       - name: LabTrust release fixtures
         run: |
           cd python
           pcs validate-release-chain ../examples/labtrust-release/
 
+  lean:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - uses: actions/setup-python@v5
+        with:
+          python-version: "3.12"
+      - name: Install elan
+        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: |
+          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 validate-contracts \
+            ../examples/pf-core-valid/contract_checked/trace.json \
+            --contracts-dir ../examples/pf-core-valid/contract_checked
+
   rust:
     runs-on: ubuntu-latest
     steps:
@@ -106,17 +149,6 @@ jobs:
           npm run test:hash-vectors -w @pcs/core
           npm run lint
 
-  lean:
-    runs-on: ubuntu-latest
-    steps:
-      - uses: actions/checkout@v4
-      - name: Install Lean
-        run: |
-          curl -sSfL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh -s -- -y --default-toolchain stable
-          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
-      - name: Build Lean trust-boundary skeleton
-        run: cd lean && lake build
-
   validate-cli-contract:
     runs-on: ubuntu-latest
     needs: python

diff --git a/.gitignore b/.gitignore
@@ -16,6 +16,8 @@ typescript/packages/core/dist/
 lake-packages/
 lean/lakefile.olean.trace
 lean/build/
+lean/PFCore/Generated/*.lean
+!lean/PFCore/Generated/.gitkeep
 
 .DS_Store
 *.swp

diff --git a/docs/pf-core-trace-mapping.md b/docs/pf-core-trace-mapping.md
@@ -0,0 +1,83 @@
+# PF-Core trace ↔ PCS trace_certificate mapping
+
+Phase 7 documents how PCS release artifacts relate to PF-Core traces and certificates. PCS and PF-Core use **different certificate schemas**; this document records field correspondence and shared hash rules. It does not unify schemas.
+
+**Reference implementation:** [provability-fabric-core](https://github.com/SentinelOps-CI/provability-fabric-core) tag `pf-core-v0.6.0`, adapter `adapters/pcs/normalize_release.py`.
+
+**PF-Core hash and certificate semantics:** [certificate-semantics.md](https://github.com/SentinelOps-CI/provability-fabric-core/blob/pf-core-v0.6.0/pf-core/docs/certificate-semantics.md) (hash chain section).
+
+---
+
+## PCS `trace_certificate` (v0) vs PF-Core artifacts
+
+| PCS `trace_certificate` field | PF-Core equivalent | Notes |
+|------------------------------|-------------------|-------|
+| `certificate_id` | `certificate.certificate_id` | PCS uses `cert-*` naming; PF-Core generates `cert-{uuid}` |
+| `schema_version` | `certificate.schema_version` | PCS `v0` vs PF-Core `pf-core.certificate.v0` |
+| `trace_hash` | `trace.trace_hash`, `certificate.trace_hash` | PCS uses `sha256:` prefix; PF-Core stores hex64 — normalize at boundary |
+| `spec_hash` | `certificate.contract_hash` | PCS spec hash binds to PF-Core contract hash |
+| `property_id` | (none) | PCS property identifier; map to `policy_ref` or contract id when bridging |
+| `checker` | `certificate.checker` | PCS `certifyedge` vs PF-Core `lean4` |
+| `checker_version` | `certificate.checker_version` | Version strings differ by design |
+| `status` | `certificate.safe` | `CertificateChecked` + `safe: true` documented equivalence |
+| `counterexample_ref` | (none) | PCS-only; out of PF-Core scope |
+| `created_at` | (none) | Organizational metadata |
+| `producer` / `producer_version` | `certificate.created_by` | Optional PF-Core field |
+| `source_repo` / `source_commit` | `certificate.proof_ref` | Different semantics; cross-reference only |
+| `signature_or_digest` | (none) | PCS bundle integrity; post-incident-proofs layer |
+
+---
+
+## Event / trace hash rules (shared)
+
+Both repos agree on:
+
+1. **Genesis** `previous_event_hash`: 64 ASCII `0` characters.
+2. **Canonical JSON:** sorted keys, minimal separators (`separators=(",", ":")`).
+3. **`event_hash`:** `sha256(payload)` as lowercase hex; accept `sha256:` prefix at validation.
+4. **`trace_hash`:** `sha256(canonical_json(trace \ {trace_hash}))`.
+
+PCS hash vectors under `python/tests/hash_vectors/` must match provability-fabric-core `adapters/pcs/tests/fixtures/hash_vectors/` at the pinned PF-Core tag.
+
+---
+
+## LabTrust replay path
+
+Pinned LabTrust release fixtures (e.g. `examples/labtrust/trace_certificate.valid.json`) feed PF-Core traces via the untrusted adapter:
+
+```
+labtrust-release/trace_certificate.valid.json
+  → normalize_release.normalize_labtrust_release()
+  → pf-core/examples/valid/pcs_replay_trace.json
+```
+
+### Release directory fields
+
+| LabTrust / PCS artifact | Role in PF-Core trace |
+|-------------------------|----------------------|
+| `trace_certificate.valid.json` | Source `trace_hash` / `spec_hash` for mapping docs; adapter reads when present |
+| Release observation (when emitted) | Compiles to `pf-core.event.v1` via `compile-observation` |
+| PCS `trace_hash` (with `sha256:` prefix) | Normalizes to hex64 for `trace.trace_hash` binding |
+| PCS `spec_hash` | Maps to `certificate.contract_hash` when emitting PF-Core certificate |
+
+The reference adapter builds a single-event trace with `lab.release` effect, principal `lab-operator-1`, and genesis hash chain. See `pcs_replay_trace.json` in provability-fabric-core.
+
+### Verification command
+
+```bash
+PYTHONPATH=pf-core/validator python -m pf_core.cli core check-trace \
+  --schemas pf-core/schemas \
+  --file pf-core/examples/valid/pcs_replay_trace.json
+```
+
+---
+
+## Assurance boundary
+
+| Layer | Claim |
+|-------|-------|
+| PF-Core `safe: true` | T1 (Lean-proved) + T4 (runtime deciders) |
+| PCS `CertificateChecked` | PCS checker semantics |
+| This mapping doc | Organizational cross-reference only |
+
+PCS does not expand PF-Core TCB. Policy alignment remains vector-tested in provability-fabric-core.
diff --git a/docs/pf-core/assumptions.md b/docs/pf-core/assumptions.md
@@ -0,0 +1,50 @@
+# PF-Core assumptions
+
+PF-Core proofs and certificates are conditional on explicit assumptions. This document lists assumptions baked into the current implementation (Stages 1–7) and assumptions deferred to later research.
+
+## Cryptographic assumptions
+
+- SHA-256 collision resistance for canonical artifact hashes and event hash chains.
+- `signature_or_digest` fields bind artifact bytes; full PKI signing infrastructure is out of scope for v0.1.
+
+## Producer assumptions
+
+- Runtime producers (`AgentRuntime`, LabTrust-Gym, adapters) emit faithful observations unless contradicted by hash-chain validation.
+- Adapters that compile PCS artifacts into PF-Core traces are **untrusted**; their output must pass schema and semantic validation.
+
+## Lean bridge (Stages 3–4)
+
+- Default `pcs pf-core lean-check` runs Python deciders aligned with `lean/PFCore/` predicates, then generates a concrete proof file under `lean/PFCore/Generated/` and checks it with `lake env lean`.
+- `LeanKernelChecked` is emitted **only** when that concrete proof succeeds (`traceSafeD … = true` via `decide`). `--skip-build` or `--skip-lean-proof` yields `RuntimeChecked` only.
+- `lake build PFCore` means the PF-Core library compiles; individual traces still require generated proof files for kernel claims.
+- Theorem names in `PF_CORE_THEOREM_CATALOG` exist as Lean symbols (enforced by `pcs pf-core audit-lean-catalog`).
+- PCS `pcs lean-check` (without `--trace`) is **not** Lean-backed per trace. It prints the assurance boundary and exits; it must not be described as kernel-verified trace safety.
+
+## Role and capability alignment (permanent boundary)
+
+- Lean `HasCapability` inspects `principal.capabilities` only; **roles are not expanded in the kernel**.
+- The PF-Core runtime compiler expands known roles into explicit capability ids on compiled principals.
+- Traces submitted to `pcs pf-core lean-check` must list those expanded capabilities explicitly; lean-check rejects principals where `capabilities` does not match role expansion.
+- Runtime authorization may still consult roles during compilation; lean-check and Lean proofs rely on the explicit capability list only.
+- This role-to-capability split is a **permanent trusted-boundary assumption**, not a temporary Stage 1 gap.
+
+## Registry assumptions
+
+- Registry semantic checks marked `allowed_to_skip: true` are not treated as proved.
+- Deferred checks must surface as `AssumptionDeclared` or `OutOfScope` claim classes, never `LeanKernelChecked` or unjustified `ProofChecked`.
+- PF-Core certificates with skipped deferrable checks require non-empty `assumption_refs` pointing at `AssumptionSet.v0` ids or documented paths under `docs/pf-core/`.
+
+## Out of scope (not assumed by PF-Core)
+
+- Model correctness or alignment.
+- Clinical or production safety of real-world systems.
+- Natural-language policy interpretation.
+- Global non-interference across tenants before event-level trace safety is proved.
+
+## Assumption artifacts
+
+Domain assumptions must be recorded in `AssumptionSet.v0` (PCS) or referenced from PF-Core certificates. Simulation scope disclaimers from the LabTrust profile remain mandatory for QC-release demonstrations. Prefer citing `assumption_set_id` values (for example `as-labtrust-qc-v0.1`) over documentation paths alone when issuing `AssumptionDeclared` certificates.
+
+## Contract and invariant simplification
+
+See [contract-semantics.md](contract-semantics.md) for the mapping between `PFCoreContract.v0` JSON fields and runtime/Lean predicates.
diff --git a/docs/pf-core/bridge-artifact.md b/docs/pf-core/bridge-artifact.md
@@ -0,0 +1,70 @@
+# PCS TraceCertificate to PFCoreCertificate bridge artifact
+
+This document specifies the organizational bridge between PCS release-layer
+`TraceCertificate.v0` artifacts and PF-Core `PFCoreCertificate.v0` claim objects.
+It is a cross-reference spec for demos and adapters; it does not unify schemas.
+
+## Purpose
+
+PCS science bundles attach `TraceCertificate.v0` objects checked by external
+tools (e.g. CertifyEdge). PF-Core certificates carry explicit `claim_class`
+values that state what assurance was obtained. The bridge maps PCS checker output
+into PF-Core certificate fields without expanding the PF-Core TCB.
+
+## Field mapping
+
+| PCS `TraceCertificate.v0` | PF-Core `PFCoreCertificate.v0` | Bridge rule |
+|---------------------------|-------------------------------|-------------|
+| `certificate_id` | `certificate_id` | Prefix optional; preserve id for cross-reference |
+| `trace_hash` | `trace_hash` | Normalize `sha256:` prefix at boundary |
+| `spec_hash` | `contract_hash` | Direct bind |
+| `checker` | `checker` | Copy verbatim |
+| `checker_version` | `checker_version` | Copy verbatim |
+| `status: CertificateChecked` | `claim_class: CertificateChecked` | Required when external checker attests |
+| `source_repo` | `source_repo` | Copy verbatim |
+| `source_commit` | `source_commit` | Copy verbatim |
+| `property_id` | (none) | Record in trace event `contract_refs` when compiling |
+| `counterexample_ref` | (none) | PCS-only; PF-Core `OutOfScope` if replay needed |
+| `signature_or_digest` | (none) | PCS bundle integrity; recompute PF-Core digest |
+
+## Claim class selection
+
+| Bridge operation | Required `claim_class` |
+|------------------|------------------------|
+| External checker attestation only | `CertificateChecked` |
+| PF-Core runtime compiler + hash chain | `RuntimeChecked` |
+| Deterministic hash replay | `ReplayValidated` |
+| Lean kernel concrete proof | `LeanKernelChecked` |
+| Deferred registry checks documented | `AssumptionDeclared` |
+
+Do not emit `LeanKernelChecked` from the bridge when only PCS
+`CertificateChecked` status is available.
+
+## Bridge workflow (demo)
+
+```
+examples/labtrust/trace_certificate.valid.json
+  → pf_core_labtrust_adapter.normalize_labtrust_release()
+  → examples/pf-core-valid/labtrust_replay/trace.json
+  → pcs pf-core replay-trace trace.json
+  → pcs pf-core attach-certificate-check --trace trace.json ...
+  → PFCoreCertificate.v0 (claim_class: CertificateChecked)
+```
+
+## Assurance boundary
+
+| Layer | What the bridge claims |
+|-------|------------------------|
+| PCS `CertificateChecked` | External checker semantics for the declared property |
+| PF-Core `CertificateChecked` | Same attestation recorded in PF-Core schema |
+| PF-Core `ReplayValidated` | Hash chain reproducibility only |
+| PF-Core `LeanKernelChecked` | Not implied by this bridge |
+
+Adapters that perform the bridge are **untrusted**. All bridged artifacts must
+pass PCS schema and PF-Core semantic validation before release.
+
+## Related documents
+
+- [claim-boundary.md](claim-boundary.md) — claim class definitions
+- [pf-core-trace-mapping.md](../pf-core-trace-mapping.md) — trace field mapping
+- [assumptions.md](assumptions.md) — deferred registry obligations