File size: 1,357 Bytes
224e773 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 | # 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:**
```bash
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.
|