BitVec dependent type problem

Stream: new members

[Per Lindgren]

Hi Folks
I'm new to Lean, so probably a rookie mistake.

Background:
I teach a course on digital design at Luleå University of Technology. Among other things students learn to build an adder (based on FullAdders with carry propagation). There is a neat trick where you can check overflow for signed addition, by just C[N] ^ C[N-1] (^ being exor), where C is carry out from the full addition for bit N. While this just works, it would be neat to show a proof that it actually works. I tried with Why3, got stuck, and I did not dare to approach Coq.

Lean:
Looked around a bit, and found Lean (I've seen it before, but never tried it seriously). So why not, did some tutorials, and found it more approachable (vscode integration feels like home).

Problem:

import Mathlib.Algebra.Ring.Defs
import Mathlib.Data.Real.Basic
import Mathlib.Data.BitVec
import MIL.Common

#check BitVec

def full_adder (a b c: Bool) : Bool × Bool :=
  ( a && b || a && c || b && c, a ^^ b ^^ c)

#eval (full_adder false false false)
#eval (full_adder false false true)
#eval (full_adder false true false)
#eval (full_adder false true true)

#eval (full_adder true false false)
#eval (full_adder true false true)
#eval (full_adder true true false)
#eval (full_adder true true true)

def adder {w: Nat}(a b : BitVec w) : Bool × BitVec w :=
  if w = 0 then
    (false, 0)
  else
    let (c_in, s_in) := adder (a.truncate (w - 1)) (b.truncate (w - 1))
    let (c_out, s) := full_adder false false c_in
    (c_out, BitVec.cons s s_in)

So the idea here is to recursively compute the addition by invoking the full_adder for each bit.

Also as this is my very first Lean program (besides the tutorials), the whole approach might be stupid. There might be better (leaner) ways of defining addition and proving the overflow "rule". (By the way, this is not yet even an attempt of proving anything, its just to get the definition correct in the first place.)

I ran into the problem where Lean reports the type: BitVec (w - 1 + 1) : Type (for BitVec.cons s s_in), which is incompatible to the expected BitVec (w ) : Type.

Any tips, both to the adder definition and if it seems reasonable to the type error problem.

Thanks in advance
Per

[Aaron Liu]

Instead of doing if w = 0 then ... else ..., you should do match w with | 0 => ... | n + 1 => ...

[Aaron Liu]

This gives you better definitional properties. In particular, you won't run into the problem with BitVec (w - 1 + 1) because you won't have subtraction.

[Per Lindgren]

Ahh thanks, that makes sense, will try and check back, guess this is not my last problem :)

[Henrik Böving]

@Per Lindgren FYI, these concepts are already mechanized in Lean as we have a bit blasting decision procedure called bv_decide which makes use of this, the overflow property is docs#BitVec.uaddOverflow and we have a proof of the property you want here docs#BitVec.uaddOverflow_eq

[Per Lindgren]

def adder {w: Nat}(a b : BitVec w) : Bool × BitVec w :=
  match w with
  | 0 =>  (false, 0)
  | n + 1 =>
    let (c_in, s_in) := adder (a.truncate (n)) (b.truncate (n))
    let (c_out, s) := full_adder (a.getMsb' (n+1)) (b.getMsb' (n+1)) c_in
    (c_out, BitVec.cons s s_in)

[Henrik Böving]

And the fact that add corresponds to a full adder is here: docs#BitVec.getLsbD_add

[Per Lindgren]

@Henrik Böving , thanks for the tip.

However, the point here is not the correctness of the bitvector additon in Lean, but rather, the implementation in terms of full adders with carry propagation (and the "neat" overflow checking mechanism).

The equation in Lean is: x.uaddOverflow y = decide (x.toNat + y.toNat ≥ 2 ^ w), so no direct connection to the carry propagation, or am I missing something?

[Per Lindgren]

Ahh you beat me to it...

[Henrik Böving]

The definitions in Lean are built after the SMTLIB standard for quantifier free bitvector theory which defines the semantics of bitvector operations in terms of integer operations. We thus copy these integer operations and then demonstrate that they correspond to certain equations that you would be used to from a bitwise point of view. The great thing about this is, that we do not need to mechanize BitVec as a List Bool and thus actually retain the ability to efficiently execute code that is built using BitVec + we get the entire arithmetic theory from Int modulo 2^n for free.

[Per Lindgren]

This is truly awesome!!!!

[Per Lindgren]

So the trick I mentioned that overflow can be checked by exor of the two most significant carries, can it bee seen/proven directly from the Lean definitions?

[Per Lindgren]

(My thought was to model the adder, and then somehow attack the problem... but if the full-adder connection is already there, there might be easier ways...)

[Henrik Böving]

So you want to essentially prove:

example (x y : BitVec w) : BitVec.saddOverflow x y = (BitVec.carry w x y false) ^^ (BitVec.carry (w - 1) x y false)

?

[Per Lindgren]

Yes

By the way, the homebrew adder did work:

#eval (adder 0#0 0#0) -- (false, 0#0)
#eval (adder 0#1 0#1) -- (false, 0#1)
#eval (adder 0#1 1#1) -- (false, 1#1)
#eval (adder 1#1 0#1) -- (false, 1#1)
#eval (adder 1#1 1#1) -- (true, 0#1)

[Henrik Böving]

I can offer you a very quick proof like this:

import Std.Tactic.BVDecide

example (x y : BitVec w) : BitVec.saddOverflow x y = (BitVec.carry w x y false) ^^ (BitVec.carry (w - 1) x y false) := by
  rw [BitVec.saddOverflow_eq]
  rw [BitVec.msb_add]
  match w with
  | 0 => decide +revert
  | w + 1 =>
    simp [BitVec.carry_succ, Bool.atLeastTwo]
    bv_decide

though there is no need to go as hard as bv_decide here, I'll try to get rid of that in a moment.

[Per Lindgren]

Wow that's crazy!!!!

[Per Lindgren]

Hmm, I was not able to replay your proof, got an error on BitVec.saddOverflow x y

Am I missing some import (I used the BVDecide import), or do I have another BitVec lib perhaps (installed through vscode example quickstart... under macos).

[Henrik Böving]

saddOverflow was added very recently as we focused on getting all other BitVec operations in first, what is your Lean version?

[Henrik Böving]

example (x y : BitVec w) : BitVec.saddOverflow x y = (BitVec.carry w x y false) ^^ (BitVec.carry (w - 1) x y false) := by
  rw [BitVec.saddOverflow_eq, BitVec.msb_add]
  match w with
  | 0 => decide +revert
  | w + 1 =>
    simp [BitVec.carry_succ, Bool.atLeastTwo, BitVec.msb_eq_getLsbD_last]
    cases BitVec.carry w x y false <;> cases x[w] <;> cases y[w] <;> simp

this one is without bv_decide, you could also decide to play out the Bool simplification game that the last line uses yourself but I think it's just easier to do it like this if you are not into that :D

[Per Lindgren]

I assume it installs lean according to toml.

name = "mil"
defaultTargets = ["MIL"]

[leanOptions]
pp.unicode.fun = true # pretty-prints `fun a ↦ b`
autoImplicit = false
relaxedAutoImplicit = false

[[require]]
name = "mathlib"
git = "https://github.com/leanprover-community/mathlib4"
rev = "v4.17.0"

[[lean_lib]]
name = "MIL"

[Henrik Böving]

Ah, so v4.17.0, that's unfortunately exactly one version behind 4.18.0 which was the first version that had this overflow theory already

[Henrik Böving]

Though as all the theory is in lean core and there is no need for mathlib to do this kind of stuff you could create a project that uses 4.18.0 and do things there, alternatively if you just wanna do a quick demo and not get too deep into Lean there is also the option of the Lean web editor: https://live.lean-lang.org/

[Per Lindgren]

I changed the toml to 4.18 and restarted the file (in vscode), but it still does show the same error.

[Henrik Böving]

I assume you got this toml from here: https://github.com/leanprover-community/mathematics_in_lean right?

[Per Lindgren]

exactly that

[Henrik Böving]

Right, that's more of a tutorial repository and it hasn't been made compatible to 4.18 yet as that is the latest stable release. What you can do to get a fresh project quickly is go into the command line and type lake +leanprover/lean4:v4.18.0 new overflow lib to get project set up called overflow (of course names may vary) in a directory of the same name. That project is going to contain nothing but the core installation of 4.18.0 and there the proof should work.

[Per Lindgren]

Would you be interested in giving a talk to our students in digital design? Just to raise some curiosity among the students.

[Henrik Böving]

I'd definitely be interested yes!

[Per Lindgren]

Awesome, we could move the discussion to a private channel.

[Kevin Buzzard]

@Per Lindgren just alerting you to Henrik's recent talk at Lean Together: https://www.youtube.com/watch?v=Q1LDavBJ94A