A library for writing MPC programs against ideal functionalities and proving, in Lean 4 on Mathlib, that:
- They are correct
- What they cost in rounds and communication
- That they are private
With easy composition of subcircuits / subprograms based on ideas from the universal composability framework.
Start with Universal Composability, then read Functionalities, Hybrids, Programs, Privacy, Rounds, and Communication.
lake exe cache get # Mathlib's cache, once
lake build --wfail # library and examples; warnings fail the build, as in CI
CI uses axiom-audit to check
that library and example declarations depend only on the standard
axioms propext, Classical.choice, and Quot.sound:
lake --wfail exe axiom-audit --root Weft
lake --wfail exe axiom-audit --root Examples