Phase7/shared hash vector ci

.github/workflows/ci.yml

@@ -17,6 +17,7 @@ jobs:
         run: |
           cd python
           pip install -e ".[dev]"
+          pytest -q tests/test_pf_core_tier1.py tests/test_pf_core_cross_language.py
           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
@@ -81,17 +82,33 @@ jobs:
           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)
+      - name: PF-Core CertifyEdge check (live or mock)
         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
+          pip install -e .
+          if command -v certifyedge >/dev/null 2>&1; then
+            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
+          else
+            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
+          fi
+      - name: PF-Core Tier 1 tests
+        run: |
+          cd python
+          pytest -q tests/test_pf_core_tier1.py tests/test_pf_core_cross_language.py
       - 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: PF-Core adapter parity (provability-fabric-core pin)
+        run: bash scripts/run-pf-core-adapter-ci.sh
       - name: LabTrust release fixtures
         run: |
           cd python
@@ -119,6 +136,17 @@ jobs:
             ../examples/pf-core-valid/contract_checked/trace.json \
             --contracts-dir ../examples/pf-core-valid/contract_checked
 
+  pf-core-adapter:
+    runs-on: ubuntu-latest
+    continue-on-error: true
+    steps:
+      - uses: actions/checkout@v4
+      - uses: actions/setup-python@v5
+        with:
+          python-version: "3.12"
+      - name: PF-Core provability-fabric-core adapter parity
+        run: bash scripts/run-pf-core-adapter-ci.sh
+
   rust:
     runs-on: ubuntu-latest
     steps:

CHANGELOG.md

@@ -0,0 +1,25 @@
+# Changelog
+
+## PF-Core v0.1 production kernel (Tier 1–3)
+
+### Added
+
+- `semantics_layer` on `PFCoreContract.v0` declaring per-field discharge layers (`lean`, `runtime`, `out_of_scope`).
+- `contract_semantics_checked` on `PFCoreCertificate.v0` derived from contract semantics layers and actual checks.
+- Shared negative hash vectors under `python/tests/hash_vectors/pf_core/invalid/` with Rust and Python parity tests.
+- `pcs pcs-envelope check` alias for PCS release-envelope consistency; `pcs lean-check` retained with deprecation notice.
+- `scripts/run-pf-core-adapter-ci.sh` for provability-fabric-core hash-vector pin verification.
+- Tier 1 tests in `python/tests/test_pf_core_tier1.py`.
+- Documentation: `generated-proofs.md`, `windows-lean.md`, updated gap audit and contract semantics.
+
+### Changed
+
+- PCS release path framed as envelope-only (`ProofChecked`); not conflated with PF-Core `LeanKernelChecked`.
+- Cross-language PF-Core parity extended to contract validation and denied-event preservation (Rust `pf_core.rs`, TypeScript `pfCore.ts`).
+- CertifyEdge CI tries live CLI when present, falls back to `PCS_CERTIFYEDGE_MOCK=1`.
+
+### Documented (deferred)
+
+- Full global non-interference remains open research (`non-interference.md`).
+- Role-to-capability split is a permanent trusted-boundary assumption (`assumptions.md`).
+- PKI signing infrastructure out of scope for v0.1.

docs/pf-core-trace-mapping.md

@@ -39,6 +39,21 @@ Both repos agree on:
 
 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.
 
+PF-Core-specific vectors live under `python/tests/hash_vectors/pf_core/` (`PFCoreEvent.v0`, `PFCoreTrace.v0`, `PFCoreContract.v0`) and are verified in Python, Rust, and TypeScript parity tests.
+
+---
+
+## Runtime observation ordering
+
+`PFCoreRuntimeObservation.v0` carries a required non-negative `sequence` field. Deterministic trace compilation orders observations by `(sequence, source_index)` before hash chaining:
+
+1. Sort observations by `sequence` ascending; equal sequences preserve input order.
+2. Compile each observation to `PFCoreEvent.v0` using its `sequence` value.
+3. Recompute `previous_event_hash` / `event_hash` sequentially from genesis.
+4. Reject traces that drop denied observations (`DroppedDeniedEvent`).
+
+Single-observation compile paths (`compile_runtime_observation_to_event`) preserve the observation `sequence` and `policy_ref` as `contract_refs`.
+
 ---
 
 ## LabTrust replay path

docs/pf-core/assumptions.md

@@ -5,7 +5,7 @@ PF-Core proofs and certificates are conditional on explicit assumptions. This do
 ## 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.
+- `signature_or_digest` fields bind artifact bytes; **PKI signing, HSM integration, and X.509 certificate chains are out of scope for PF-Core v0.1** (documented assumption only).
 
 ## Producer assumptions
 
@@ -18,15 +18,15 @@ PF-Core proofs and certificates are conditional on explicit assumptions. This do
 - `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.
+- PCS `pcs pcs-envelope check` (alias `pcs lean-check`) validates release-envelope consistency only; it must not be described as PF-Core 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.
+- This role-to-capability split is a **permanent trusted-boundary assumption** unless a future Lean RoleMap stage expands kernel capability resolution.
 
 ## Registry assumptions
 

docs/pf-core/claim-boundary.md

@@ -29,11 +29,20 @@ The claim-boundary linter (`pcs pf-core audit-claims`) fails on these phrases in
 | fully verified runtime | runtime-checked trace with explicit claim class |
 | formally verified platform | release-envelope consistency theorem family (for PCS Lean scope) |
 
-## LeanCheckResult.v0 (PCS bridge artifact)
+## PCS release-envelope consistency (`pcs pcs-envelope check`)
 
-PF-Core `pcs pf-core lean-check` emits a registered `LeanCheckResult.v0` object alongside optional `PFCoreCertificate.v0` output.
+PCS release-envelope checks validate `ProofObligation.v0` against the PCS theorem catalog in `lean/PCS/Theorems.lean`.
+
+- Preferred command: `pcs pcs-envelope check --obligations … --out …`
+- Legacy alias: `pcs lean-check` (prints deprecation notice; same behavior)
+- Emits `LeanCheckResult.v0` with lifecycle status `ProofChecked` when obligations pass
+- Does **not** prove PF-Core trace safety; does not emit `LeanKernelChecked`
+
+Use `pcs pf-core lean-check --trace …` for PF-Core kernel assurance (`LeanKernelChecked` when concrete proof succeeds).
 
-### Current behavior (Stage 4)
+## PF-Core lean-check (`pcs pf-core lean-check`)
+
+PF-Core `pcs pf-core lean-check` emits a registered `LeanCheckResult.v0` object alongside optional `PFCoreCertificate.v0` output.
 
 - `status: LeanProofChecked` means Python deciders passed, the no-sorry audit passed, `lake build PFCore` succeeded, and a generated concrete proof file checked `traceSafeD tr = true` via the Lean kernel.
 - `status: DecidersPassed` means deciders (and no-sorry audit) passed but Lean proof was skipped (`--skip-build` or `--skip-lean-proof`) or only runtime assurance was requested.
@@ -52,7 +61,7 @@ Do **not** treat PCS lifecycle `ProofChecked` as a PF-Core formal claim. PF-Core
 
 Successful lean-check writes a certificate with matching `claim_class`, `assumption_refs`, `theorems_checked`, `obligations`, `lean_build_status`, `lean_proof_checked`, and `disclaimer`.
 
-- `LeanKernelChecked` requires `proof_term_ref`, `proof_ref`, `lean_proof_checked: true`, and successful concrete Lean proof.
+- `LeanKernelChecked` requires `proof_term_ref`, `proof_ref`, `lean_proof_checked: true`, successful concrete Lean proof, and **contract grounding** (non-empty event `contract_refs` or `default_contract_ref: "trace-safe"` aligned with `PFCore.traceSafeContract`).
 - `--skip-build` or `--skip-lean-proof` yields `RuntimeChecked` only (no `proof_term_ref`).
 
 ### Mapping guidance for PF-Core certificates

docs/pf-core/contract-semantics.md

@@ -17,19 +17,58 @@ This document maps `PFCoreContract.v0` JSON fields to runtime checker predicates
 | `ContractPostSpec` | `post` object |
 | `ContractInvariantSpec` | `invariant` object |
 
+## semantics_layer (PFCoreContract.v0)
+
+Each contract may declare which fields are discharged in Lean, checked only at runtime, or explicitly out of scope:
+
+```json
+"semantics_layer": {
+  "require_capability": "lean",
+  "require_role": "runtime",
+  "require_decision": "lean",
+  "require_trace_safe": "lean"
+}
+```
+
+Field names are bare (unique across pre/post/invariant). When `semantics_layer` is omitted, defaults are derived from the mapping table below.
+
+| Layer | Meaning |
+|-------|---------|
+| `lean` | Discharged by generated Lean `ContractDecide` proofs when lean-check runs |
+| `runtime` | Validated by `pcs pf-core validate-contracts` only |
+| `out_of_scope` | Documented gap; must not appear on active required fields |
+
+Validation rejects orphan semantics entries, active fields marked `out_of_scope`, and inconsistent explicit layers.
+
+## semantics_layer (PFCoreContract.v0)
+
+Contracts may declare per-field discharge layers at the source:
+
+```json
+"semantics_layer": {
+  "require_capability": "lean",
+  "require_role": "runtime",
+  "require_policy_ref": "runtime"
+}
+```
+
+Allowed values: `lean`, `runtime`, `out_of_scope`.
+
+When `semantics_layer` is omitted, defaults are derived from the mapping table below. Explicit entries must match the canonical layer for active fields (validated by `pcs validate`).
+
 ## Formal mapping table (JSON ↔ Lean ↔ runtime)
 
-| JSON field | Runtime (`pf_core_contract.py`) | Lean decider | Generated proof |
-|------------|-----------------------------------|--------------|-----------------|
-| `pre.require_capability` | `_principal_has_capability` | `contractPreD` / `hasCapabilityD` | `concrete_contract_pre_*` |
-| `pre.require_effect` | `_action_has_effect` | `contractPreD` / `actionHasEffectD` | `concrete_contract_pre_*` |
-| `pre.require_tenant_match` | `_tenant_matches` | `contractPreD` / `actionWithinTenantD` | `concrete_contract_pre_*` |
-| `pre.require_role` | role list membership | **Not mapped** | — |
-| `pre.require_policy_ref` | `contract_refs` contains ref | **Not mapped** | — |
-| `pre.require_evidence_ref` | `evidence_refs` contains ref | **Not mapped** | — |
-| `post.require_decision` | decision equality | `contractPostD` | `concrete_contract_post_*` |
-| `post.require_event_safe` | capability + tenant on allow | `contractPostD` / `eventSafeD` | `concrete_contract_post_*` |
-| `invariant.require_trace_safe` | (trace-level) | `contractInvariantD` / `traceSafeD` | `concrete_trace_satisfies_*` |
+| JSON field | Default layer | Runtime (`pf_core_contract.py`) | Lean decider | Generated proof |
+|------------|---------------|-----------------------------------|--------------|-----------------|
+| `pre.require_capability` | `lean` | `_principal_has_capability` | `contractPreD` / `hasCapabilityD` | `concrete_contract_pre_*` |
+| `pre.require_effect` | `lean` | `_action_has_effect` | `contractPreD` / `actionHasEffectD` | `concrete_contract_pre_*` |
+| `pre.require_tenant_match` | `lean` | `_tenant_matches` | `contractPreD` / `actionWithinTenantD` | `concrete_contract_pre_*` |
+| `pre.require_role` | `runtime` | role list membership | **Not mapped** | — |
+| `pre.require_policy_ref` | `runtime` | `contract_refs` contains ref | **Not mapped** | — |
+| `pre.require_evidence_ref` | `runtime` | `evidence_refs` contains ref | **Not mapped** | — |
+| `post.require_decision` | `lean` | decision equality | `contractPostD` | `concrete_contract_post_*` |
+| `post.require_event_safe` | `lean` | capability + tenant on allow | `contractPostD` / `eventSafeD` | `concrete_contract_post_*` |
+| `invariant.require_trace_safe` | `lean` | (trace-level) | `contractInvariantD` / `traceSafeD` | `concrete_trace_satisfies_*` |
 
 Per-event discharge: `satisfiesContractSpecD`. Trace-level: `traceSatisfiesContractSpecsD`.
 
@@ -41,7 +80,23 @@ When `contract_refs` appear on events and contract JSON is found alongside the t
 2. Generated `.lean` file includes `ContractPreSpec` / `PostSpec` / `Inv` defs and `decide` proofs.
 3. `lake env lean` on the generated module discharges concrete obligations.
 
-Fields marked **Not mapped** remain runtime-only; codegen documents the gap in the header when refs exist but contracts are missing.
+Fields marked **Not mapped** remain runtime-only unless `semantics_layer` overrides a mapped field to `runtime`. Codegen skips Lean obligations for non-`lean` fields.
+
+## contract_semantics_checked (PFCoreCertificate.v0)
+
+When `pcs pf-core lean-check` emits a certificate, it includes:
+
+```json
+"contract_semantics_checked": {
+  "lean": ["contract-id.pre.require_capability", "..."],
+  "runtime": ["contract-id.pre.require_role", "..."]
+}
+```
+
+- `lean`: contract fields with `semantics_layer` `lean` (discharged by generated Lean proofs when lean-check succeeds).
+- `runtime`: fields with layer `runtime` (validated by `pcs pf-core validate-contracts`).
+
+Out-of-scope fields are omitted from both lists.
 
 ## Invariant preservation (Lean)