lean/proofs/README.md

Lean 4 Formal Proofs

Two policy kernels formalized in Lean 4.

policy-kernel/

Sovereign Policy Kernel — verdict algebra and policy DSL.

Key types:

• Verdict — canonical verdict algebra (approve | reject | defer | escalate | human_required)
• Context — policy evaluation context (actor DID, task type, evidence, nonce)
• Evidence — hash URIs, signatures, byte arrays
• Policy π — typeclass: any policy ID → Context → Verdict
• Verdict.combine — priority-based combination (escalate > human_required > reject > defer > approve)

Build:

cd policy-kernel && lake build

bifrost-policy/

Bifrost event validity — formal propositions + Boolean decision procedure.

Key definitions:

• validJitCompile — SoulIR sealed ∧ WASM fresh
• validCapTransfer — policyCid sealed ∨ zero, capHash in map ∨ zero
• validAttestation — epoch root matches state
• decide — computable Bool (single source of truth for bifrost-policy/src/lib.rs::policy_decide)
• decide_sound — soundness theorem: decide e s = true → validEvent e s (sorry — Week 3 P0)

Note: bifrost-policy/ imports Bifrost.State which lives in the snap-os workspace. Full build requires snap-os/bifrost-policy/lean/. This directory contains the policy proofs only.