Repository navigation

feat(formal): Clean/Lean model of BITWISE, LT, EQ and SHIFT with proo… - #1027

Draft

ColoCarletti wants to merge 17 commits into

mainfrom

formal/clean-model

Draft

feat(formal): Clean/Lean model of BITWISE, LT, EQ and SHIFT with proo…#1027
ColoCarletti wants to merge 17 commits into
mainfrom
formal/clean-model

Commits on Oct 22, 2026
- feat(formal): Clean/Lean model of BITWISE, LT, EQ and SHIFT with proofs and a differential check against the prover
  ColoCarletti
  committed
  b9bcccc
Commits on Oct 26, 2026
- refactor(formal): single lemma for the bit constraint and chips call isBit
  ColoCarletti
  committed
  2b2d9e2
Commits on Oct 28, 2026
Commits on Nov 2, 2026
- Bump Clean to f3abad7c (current main, Lean v4.35.0) and adapt the model to its channel API.
  jotabulacios
  committed
  3b04970
- Rename the if/dif lemmas that Lean v4.35.0 deprecates, and drop a skip fallback the linter flags.
  jotabulacios
  committed
  48fd9e7
Commits on Nov 3, 2026