Skip to content

tutorial.md

Latest commit

 

History

History
91 lines (68 loc) · 3.41 KB

tutorial.md

File metadata and controls

91 lines (68 loc) · 3.41 KB
Raw

PF-Core Tutorial (Non-Lean Engineers)

This tutorial explains PF-Core without requiring Lean. For formal details see formal-model.md.

Soundness split

Layer What it does
Lean proves If JSON is modeled correctly, deciders match safety predicates
Runtime validates Schema, hash chains, compile determinism
Assumptions Emitters are honest enough to produce valid JSON and tenant labels

Core artifacts

  1. Runtime observation — what an adapter saw (MCP audit line, lab gate, etc.)
  2. Event — normalized record with event_kind (action or handoff), decision, and hash-chain fields
  3. Trace — ordered events with trace_hash
  4. Certificate — summary bit safe over a trace hash

Quick start

pip install -e pf-core/validator
pf core schema-check --schemas pf-core/schemas
pf core compile-observation --file pf-core/examples/valid/mcp_sidecar_observation.json
pf core check-trace --file pf-core/examples/valid/file_read_allowed_trace.json
pf core emit-artifacts --file pf-core/examples/valid/mcp_sidecar_observation.json --out-dir ./artifacts

Windows: powershell -File pf-core/scripts/pf-core-trusted.ps1

End-to-end replay (Phase 6)

Full pipeline gate (sidecar → normalize → compile → check-trace → certificate):

make pf-core-e2e
# or
bash pf-core/scripts/e2e-replay-gate.sh
powershell -File pf-core/scripts/e2e-replay-gate.ps1

Scenarios exercised:

Scenario Expected
File read allow (v1 observation) PASS through certificate
MCP sidecar normalize PASS through certificate
Compile downgrades unsafe allow decision: denied
Handoff subset violation FAIL at check-trace
PCS replay trace PASS at check-trace
Tampered hash chain FAIL at replay validation
Lean replay (3 goldens) PASS with --lean-check
Handoff validate + audit.jsonl PASS (validate-handoff, handoff trace audit line)

Single observation walkthrough:

pf core compile-observation --schemas pf-core/schemas \
  --file pf-core/examples/valid/mcp_sidecar_observation.json --output /tmp/event.json
pf core validate-event --schemas pf-core/schemas --file /tmp/event.json
pf core check-trace --schemas pf-core/schemas \
  --file pf-core/examples/valid/file_read_allowed_trace.json --lean-check
pf core validate-handoff --schemas pf-core/schemas \
  --file pf-core/examples/valid/handoff.json
pf core emit-certificate --schemas pf-core/schemas \
  --trace pf-core/examples/valid/file_read_allowed_trace.json --output /tmp/cert.json

Event kinds (v1)

Kind Meaning Safety check
action Tool call / effect attempt Capability + tenant + effect
handoff Authority transfer between principals Same tenant + bilateral capability

Handoff trace example: pf-core/examples/valid/handoff_trace.json

What PF-Core does not do

  • Does not prove LLM outputs are correct
  • Does not sandbox MCP servers or OS calls
  • Does not guarantee recipients honor handoffs

See claim-boundary.md for allowed wording.

Next steps