Checking low-depth circuits / polynomials

Stream: lean4

[Geoffrey Irving]

I have a bunch of theorems which are identities of boolean circuits over a reasonably small number of bits. For example,

import Mathlib.Data.Nat.Basic

structure UInt128 where
  lo : UInt64
  hi : UInt64

def UInt128.toNat (x : UInt128) : ℕ :=
  (x.hi.toNat * 2^64) + x.lo.toNat

/-- Add with carry, producing the `{0,1}` value as an `UInt64` -/
def addc (x y : UInt64) : UInt64 × UInt64 :=
  let z := x + y
  (z, if z < x then 1 else 0)

/-- Split a `UInt64` into low and high 32-bit values, both represented as `UInt64` -/
def split (x : UInt64) : UInt64 × UInt64 :=
  (x.toUInt32.toUInt64, x >>> 32)

/-- All the bits of two `UInt64`s multiplied together -/
def mul128 (x y : UInt64) : UInt128 :=
  let (x0,x1) := split x
  let (y0,y1) := split y
  let (a1,a3) := addc (x1 * y0) (x0 * y1)
  let (b1,b2) := split a1
  let (c0,c2) := addc (x0 * y0) b1
  ⟨c0, (a3 <<< 32) + x1 * y1 + b2 + c2⟩

lemma toNat_mul128 {x y : UInt64} : (mul128 x y).toNat = x.toNat * y.toNat :=
  sorry

Do we have tactic machinery that can prove this kind of theorem automatically, with the only work being converting the theorem into the underlying Boolean circuit identity? If I were doing normal programming, I'd write a randomized unit test and "prove" it with the Schwartz-Zippel lemma. If it was available, presumably Z3 could do it (after some mechanical translation work), proving a trace that Lean could then check. Is that Z3 setup available yet?

(Caveat: Quite possibly that mul128 implementation is buggy, since I haven't filled in the sorry yet.)

[Eric Wieser]

Maybe the way to handle this is to go back and forth with docs#Std.BitVec, and show that the analogous result is true for some arbitrary number of bits

[Eric Wieser]

Though you'll likely have a bad time until we finish merging it with docs#Bitvec

[Geoffrey Irving]

I've already proven a variety of other theorems that way, but it would be nice if I could get them for free from SAT/SMT solvers given that they really are fundamentally fixed size (I'm working up towards some numerical computations). https://github.com/ufmg-smite/lean-smt seems to be one attempt in this direction, but it says "This project is in its early design/development phase and is not recommended for use."

[Scott Morrison]

@Geoffrey Irving, this sort of application is considered very high priority by the FRO, but ... there's nothing production ready for you. :-)