A SHA-256 compression circuit over secret-shared bits, built with Weft. Lean proofs establish:
- Correctness against Wychelean’s compression function
- Perfect privacy
- 38,656 AND gates and 456 rounds, with all input bits available at round zero
The main results are in Numbers.lean. The circuit works for arbitrary chaining values and message blocks.
Uses Lean 4.34.0-rc2 and a Weft checkout at ../weft.
Wychelean and Mathlib are pinned in lakefile.toml.
lake exe cache get
lake build --wfail WeftChals Tests
See LEAN_STYLE.md for proof conventions.