Build and check Lean 4 proofs. Triggers: "lean build", "check proofs", "run lean", "verify proofs", "lean".
Build and type-check the formal verification proofs in lean/.
~/.elan/bin/lean/ in pz root, initialized with lake init pz-proofs mathcd lean && ~/.elan/bin/lake build
First build downloads mathlib (~10 min). Subsequent builds are incremental (~seconds).
If .lake/ is corrupt: rm -rf .lake && lake update && lake build.
After adding a dependency to lakefile.toml: lake update before lake build.
lean/
lakefile.toml # project config, mathlib dependency
lean-toolchain # pinned lean version
PzProofs.lean # root module (imports all proof files)
PzProofs/
Basic.lean # auto-generated stub
Mask.lean # Proof 1: tool mask sanitization
Approval.lean # Proof 4: approval flow (future)
Policy.lean # Proof 2: signed policy (future)
Ownership.lean # Proof 3: file ownership (future)
Crypto.lean # abstract signature scheme (future)
lean/PzProofs/Name.leanimport PzProofs.Name to lean/PzProofs.leancd lean && ~/.elan/bin/lake buildbv_decide: automatic bitvector reasoning via SAT. Handles all mask proofs.omega: linear arithmetic over naturals/integerssimp: simplification with lemma databaseintro/exact/have: manual proof stepsby decide: decidable propositions (finite enums, bool)Zig u16 maps to Lean BitVec 16. Operations:
&&& = bitwise AND, ||| = bitwise OR, ~~~ = complement<<< = shift left, ≤ = unsigned less-or-equal.getLsbD i = get bit at position ibv_decide solves all fixed-width bitvector properties exhaustively.
See docs/LEAN-PROOF.md for the full verification plan with 4 proofs, acceptance criteria, and dependencies.