Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
24 commits
Select commit Hold shift + click to select a range
21c669f
Add certificate mode status policy for gated PF-Core modes.
fraware Jul 23, 2026
a427a46
Propagate lean-check-result fields through release validation.
fraware Jul 23, 2026
1e47205
Tighten handoff delegated_capabilities and evidence selection.
fraware Jul 23, 2026
3d329e2
Add PFCoreResolvedEvidence for explicit evidence selection.
fraware Jul 23, 2026
50edead
Project contract semantics_layer into semantic evidence.
fraware Jul 23, 2026
54dd7d5
Add PFCoreEffectFrame.v0 and effect-frame certificate evidence.
fraware Jul 23, 2026
f659189
Enforce FramePreserved stepState transition evidence.
fraware Jul 23, 2026
7d84089
Bind theorem manifests to proof obligations for release.
fraware Jul 23, 2026
0eedb22
Close PF-Core release bundles with verify-bundle results.
fraware Jul 23, 2026
01d16c9
Align TraceSafe and TraceSafeR across Python, Rust, and TypeScript.
fraware Jul 23, 2026
76ef778
Require PCS projection binding for Lean release catalogs.
fraware Jul 23, 2026
bb3fffa
Verify ResultArtifact payload digests against on-disk bytes.
fraware Jul 23, 2026
75f95f6
Add asset resolver and verifier wheel/OCI distribution paths.
fraware Jul 23, 2026
02726b8
Make release profiles declarative and engine-driven.
fraware Jul 23, 2026
ce11872
Separate legacy and release canonical JSON hash APIs.
fraware Jul 23, 2026
a7054f3
Add ArtifactIntegrity Ed25519 checks and CertifyEdge pin machinery.
fraware Jul 23, 2026
db43da7
Add release provenance binding and SLSA attestation scripts.
fraware Jul 23, 2026
1615894
Split CI and release workflows into focused job matrices.
fraware Jul 23, 2026
f5e70de
Advance compositional PF-Core Lean proofs and research suites.
fraware Jul 23, 2026
7fa3726
Add operator release gates and runbook checks.
fraware Jul 23, 2026
2c34a34
Wire CLI and validators to new evidence schemas.
fraware Jul 23, 2026
4c52736
Refresh release-chain fixtures for strengthened obligations.
fraware Jul 23, 2026
ad086a7
Update trust docs and gap audit for evidence hardening.
fraware Jul 23, 2026
64f6989
Sync local smoke and materialize scripts with new gates.
fraware Jul 23, 2026
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
505 changes: 451 additions & 54 deletions .github/workflows/ci.yml

Large diffs are not rendered by default.

83 changes: 83 additions & 0 deletions .github/workflows/distribution.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,83 @@
name: Distribution

# Clean-environment validator / verifier wheel + OCI acceptance (PR 11 / A12).
on:
push:
branches: [main, master]
pull_request:
workflow_dispatch:

jobs:
validator-wheel:
name: Validator-wheel clean install
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
- uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065 # v5.6.0
with:
python-version: "3.12"
- name: Validator wheel clean install
run: bash scripts/test-validator-wheel.sh

verifier-wheel:
name: Verifier-wheel clean install
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
- uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065 # v5.6.0
with:
python-version: "3.12"
- name: Install elan (checksum verified)
run: bash scripts/install-elan-verified.sh
- name: Verifier wheel clean install
run: |
export PATH="$HOME/.elan/bin:$PATH"
bash scripts/test-verifier-wheel.sh

verifier-oci-scaffold:
name: Verifier OCI Dockerfile pin
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
- name: Assert Dockerfile base pin + non-root user
run: |
python3 - <<'PY'
from pathlib import Path
import json
import re

pin = json.loads(Path("pins/python-base-image.json").read_text(encoding="utf-8"))
df = Path("docker/verifier/Dockerfile").read_text(encoding="utf-8")
digest = pin["index_digest"]
assert digest.startswith("sha256:")
assert digest in df, "Dockerfile must pin PYTHON_IMAGE by index digest"
assert "USER pcs" in df
assert "uid 10001" in df or "--uid 10001" in df
assert "org.opencontainers.image.base.digest" in df
# Forbid floating tag-only FROM without digest
for line in df.splitlines():
if re.match(r"^FROM\s+", line.strip()) and "@sha256:" not in line and "PYTHON_IMAGE" not in line:
raise SystemExit(f"unpinned FROM: {line}")
print("OK verifier OCI Dockerfile pin + non-root")
PY

verifier-oci:
name: Verifier OCI clean execution
runs-on: ubuntu-latest
timeout-minutes: 120
steps:
- uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
- name: Verifier OCI build + clean run
run: bash scripts/test-verifier-oci.sh

distribution-gate:
name: Distribution matrix gate
runs-on: ubuntu-latest
needs:
- validator-wheel
- verifier-wheel
- verifier-oci-scaffold
- verifier-oci
steps:
- name: All distribution jobs passed
run: echo "OK distribution matrix gate"
118 changes: 94 additions & 24 deletions .github/workflows/pf-core-release-gate.yml
Original file line number Diff line number Diff line change
@@ -1,7 +1,12 @@
name: PF-Core Release Gate

# Live CertifyEdge + pin verification. Tag/release path is fail-closed.
# Preview path may be exercised via workflow_dispatch with release_mode=preview.
# Preview path (workflow_dispatch release_mode=preview): lean-check → bundle-release
# → validate-bundle → absence-notice/attest → upload.
#
# Part of the mandatory CI matrix: preview path also runs on every PR via
# ci.yml `preview-release`; stable live checker is org-gated
# (pins/certifyedge.json + secrets.PF_CORE_CERTIFYEDGE_CLI).

on:
workflow_dispatch:
Expand Down Expand Up @@ -31,6 +36,8 @@ jobs:
run: |
MODE="${{ github.event.inputs.release_mode || 'release' }}"
echo "PCS_RELEASE_MODE=${MODE}" >> "$GITHUB_ENV"
- name: Install elan (checksum verified)
run: bash scripts/install-elan-verified.sh
- name: Verify CertifyEdge pin
run: python3 scripts/verify-certifyedge-pin.py --mode "${PCS_RELEASE_MODE}"
- name: Provision CertifyEdge
Expand All @@ -42,27 +49,49 @@ jobs:
if [ "${PCS_RELEASE_MODE}" = "release" ] && [ $status -ne 0 ]; then
exit 1
fi
if [ -x .tools/certifyedge/certifyedge ]; then
if [ -f .tools/certifyedge/provision.env ]; then
# shellcheck disable=SC1091
set -a
# Source machine-readable provision env (path, digest, version, pin, strategy).
# Do not let an empty repository secret overwrite a provisioned path.
# shellcheck source=/dev/null
. .tools/certifyedge/provision.env
set +a
{
echo "PF_CORE_CERTIFYEDGE_CLI=${PF_CORE_CERTIFYEDGE_CLI}"
echo "PCS_CERTIFYEDGE_PROVISION_ENV=${PWD}/.tools/certifyedge/provision.env"
echo "PCS_CERTIFYEDGE_TRUST_GRADE=${PCS_CERTIFYEDGE_TRUST_GRADE:-}"
} >> "$GITHUB_ENV"
elif [ -x .tools/certifyedge/certifyedge ]; then
echo "PF_CORE_CERTIFYEDGE_CLI=${PWD}/.tools/certifyedge/certifyedge" >> "$GITHUB_ENV"
fi
- name: Install pcs-core
run: |
cd python
pip install -c requirements.lock -e ".[dev,quality]"
pcs capabilities
- name: Org/infra release gates
run: pcs release check-gates --mode "${PCS_RELEASE_MODE}"
- name: CertifyEdge live attestation bound to release bundle (release mode)
if: env.PCS_RELEASE_MODE == 'release'
env:
PF_CORE_CERTIFYEDGE_CLI: ${{ secrets.PF_CORE_CERTIFYEDGE_CLI }}
PF_CORE_CERTIFYEDGE_REQUIRE_LIVE: "1"
# Optional last-resort override — only applied when non-empty.
PF_CORE_CERTIFYEDGE_CLI_SECRET: ${{ secrets.PF_CORE_CERTIFYEDGE_CLI }}
run: |
cd python
if [ -n "${PF_CORE_CERTIFYEDGE_CLI_SECRET:-}" ] && [ -f "${PF_CORE_CERTIFYEDGE_CLI_SECRET}" ]; then
export PF_CORE_CERTIFYEDGE_CLI="${PF_CORE_CERTIFYEDGE_CLI_SECRET}"
echo "Using non-empty PF_CORE_CERTIFYEDGE_CLI secret override"
fi
CLI="${PF_CORE_CERTIFYEDGE_CLI:-}"
if [ -n "${CLI}" ] && [ -f "${CLI}" ]; then
echo "Using PF_CORE_CERTIFYEDGE_CLI=${CLI}"
elif command -v certifyedge >/dev/null 2>&1; then
CLI="$(command -v certifyedge)"
echo "Using certifyedge on PATH: ${CLI}"
echo "WARNING: using unpinned certifyedge on PATH: ${CLI}"
echo "Arbitrary PATH executables are untrusted_development even if exit 0."
export PF_CORE_CERTIFYEDGE_CLI="${CLI}"
else
echo "FAIL: release gate requires live CertifyEdge CLI after pin provision."
echo "Pin digest in pins/certifyedge.json (status=pinned) or set runner secret."
Expand All @@ -71,22 +100,24 @@ jobs:
fi
export PF_CORE_CERTIFYEDGE_CLI="${CLI}"
export PF_CORE_CERTIFYEDGE_MODE=live
# Build a lean certificate when lake available; otherwise fail closed for release.
if command -v lake >/dev/null 2>&1 || [ -x "$HOME/.elan/bin/lake" ]; then
export PATH="$HOME/.elan/bin:$PATH"
pcs pf-core lean-check \
--trace ../examples/pf-core-valid/tool_use_trace_compiled/pfcore_trace.json \
--out /tmp/pfcore-release-cert.json
TRACE=../examples/pf-core-valid/tool_use_trace_compiled/pfcore_trace.json
CERT=/tmp/pfcore-release-cert.json
else
# Bundle still requires a valid certificate artifact; use fixture cert only if lean unavailable
# is unacceptable for release — fail closed.
export PATH="$HOME/.elan/bin:$PATH"
if ! command -v lake >/dev/null 2>&1; then
echo "FAIL: lake required to produce LeanKernelChecked certificate for release bundle"
exit 1
fi
pcs pf-core lean-check \
--trace ../examples/pf-core-valid/tool_use_trace_compiled/pfcore_trace.json \
--out /tmp/pfcore-release-cert.json \
--result-out /tmp/pfcore-release-lean-check.json
TRACE=../examples/pf-core-valid/tool_use_trace_compiled/pfcore_trace.json
CERT=/tmp/pfcore-release-cert.json
LEAN_CHECK_RESULT=/tmp/pfcore-release-lean-check.json
rm -rf /tmp/pfcore-release-bundle
pcs pf-core bundle-release --trace "${TRACE}" --cert "${CERT}" --out /tmp/pfcore-release-bundle
pcs pf-core bundle-release \
--trace "${TRACE}" \
--cert "${CERT}" \
--lean-check-result "${LEAN_CHECK_RESULT}" \
--out /tmp/pfcore-release-bundle
pcs pf-core validate-bundle /tmp/pfcore-release-bundle
pcs pf-core attest-bundle \
--bundle /tmp/pfcore-release-bundle \
Expand All @@ -99,6 +130,7 @@ jobs:
pcs validate /tmp/pfcore-release-bundle/external_attestation.json
python3 - <<'PY'
import json, sys
from pathlib import Path
att = json.load(open("/tmp/pfcore-release-bundle/external_attestation.json", encoding="utf-8"))
assert att["attestation_class"] == "live", att
assert att["result"] == "CertificateChecked", att
Expand All @@ -108,28 +140,66 @@ jobs:
"attestation_signature", "issuer_identity",
):
assert att.get(key), f"missing {key}"
print("OK live ExternalAttestation.v0 bound to release bundle")
manifest = json.loads(
Path("/tmp/pfcore-release-bundle/manifest.json").read_text(
encoding="utf-8"
)
)
lean_rel = manifest.get("lean_check_result_path")
assert lean_rel, "missing lean_check_result_path"
assert (Path("/tmp/pfcore-release-bundle") / lean_rel).is_file(), lean_rel
print("OK live ExternalAttestation.v0 bound to release bundle with lean-check-result")
PY
- name: Preview mode absence-or-attestation gate
- name: Preview lean-check → bundle → validate → absence/attest → upload prep
if: env.PCS_RELEASE_MODE == 'preview'
run: |
cd python
PF_CORE_CERTIFYEDGE_MODE=mock pcs pf-core certifyedge-check \
--trace ../examples/pf-core-valid/labtrust_replay/trace.json \
--property qc_release.temporal.safety \
--out /tmp/pfcore-preview-cert.json
export PATH="$HOME/.elan/bin:$PATH"
if ! command -v lake >/dev/null 2>&1; then
echo "FAIL: preview path requires lake for lean-check → bundle with lean-check-result"
exit 1
fi
pcs pf-core lean-check \
--trace ../examples/pf-core-valid/tool_use_trace_compiled/pfcore_trace.json \
--out /tmp/pfcore-preview-cert.json \
--result-out /tmp/pfcore-preview-lean-check.json
rm -rf /tmp/pfcore-preview-bundle
mkdir -p /tmp/pfcore-preview-bundle
pcs pf-core bundle-release \
--trace ../examples/pf-core-valid/labtrust_replay/trace.json \
--trace ../examples/pf-core-valid/tool_use_trace_compiled/pfcore_trace.json \
--cert /tmp/pfcore-preview-cert.json \
--lean-check-result /tmp/pfcore-preview-lean-check.json \
--out /tmp/pfcore-preview-bundle
pcs pf-core validate-bundle /tmp/pfcore-preview-bundle
python3 - <<'PY'
import json
from pathlib import Path
root = Path("/tmp/pfcore-preview-bundle")
manifest = json.loads((root / "manifest.json").read_text(encoding="utf-8"))
lean_rel = manifest.get("lean_check_result_path")
if not lean_rel:
raise SystemExit("FAIL: preview bundle missing lean_check_result_path")
if not (root / lean_rel).is_file():
raise SystemExit(f"FAIL: lean-check result missing at {lean_rel}")
print(f"OK preview lean-check-result in bundle: {lean_rel}")
PY
pcs pf-core attest-bundle \
--bundle /tmp/pfcore-preview-bundle \
--property qc_release.temporal.safety \
--allow-absence
--allow-absence || true
pcs pf-core validate-external-attestation \
--bundle /tmp/pfcore-preview-bundle \
--allow-absence
pcs pf-core validate-bundle /tmp/pfcore-preview-bundle
mkdir -p ../dist/pf-core-preview-bundle
cp -a /tmp/pfcore-preview-bundle/. ../dist/pf-core-preview-bundle/
- name: Upload preview release bundle
if: env.PCS_RELEASE_MODE == 'preview'
uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2
with:
name: pcs-core-pf-core-preview-bundle
path: dist/pf-core-preview-bundle/
retention-days: 14
- name: Reject mock-only CertifyEdge as release attestation
run: |
cd python
Expand Down
Loading
Loading