Performance difference between `==` and `=`?

Stream: lean4

[Geoffrey Irving]

Here is a very simple structure, and a BEq instance:

/-- 64-bit two's complement integers -/
structure Int64 where
  n : UInt64
  deriving DecidableEq

/-- Boolean equality -/
instance : BEq Int64 where
  beq x y := x.n == y.n

In working with Int64s, will there be a performance difference between == and =, resp. bif and if, or will the decidable equality checks get inlined away? I started with bif and ==, but I'm finding it annoying to prove stuff about the bif, == version, though possibly this will go away once I build up a few extra ergonomic lemmas. I suppose a first difference is that bif and Bool give me short-circuiting && and ||.

Aside: I didn't do deriving BEq since I didn't know how to get a LawfulBEq instance in this case, but I am likely missing something obvious. Automating deriving for LawfulBEq seems not to exist. Here's an MWE for the issue: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/How.20to.20prove.20.60LawfulBEq.60.20for.20automatically.20generated.20.60BEq.60/near/396675319

To add more detail, here's the kind of thing I'll be doing with this structure (not a fully closed example, but it illustrates the kind of bif code I'm dealing with):

/-- The sign bit of an `Int64` -/
@[pp_dot] def Int64.isNeg (x : Int64) : Bool := 1 <<< 63 ≤ x.n

/-- A 64-bit fixed point number, corresponding to either
    1. `n * 2^s`, if `n ≠ nan`
    2. Arbitrary, if `n = nan` -/
structure Fixed (s : ℤ) where
  n : Int64
  deriving DecidableEq

/-- Sentinel value, indicating we don't know what the number is -/
def nan : Fixed s := ⟨⟨1 <<< 63⟩⟩

/-- `Fixed` addition saturates to `nan` -/
def Fixed.add (x y : Fixed s) :=
  let z : Fixed s := ⟨x.n + y.n⟩
  bif x == nan || y == nan || (x.n.isNeg == y.n.isNeg && x.n.isNeg != z.n.isNeg) then nan else z

instance : Add (Fixed s) where add x y := x.add y

[Henrik Böving]

You can find this out quite easily on your own. If you write an example function you can see the resulting IR that gets thrown into codegen like this:

set_option trace.compiler.ir.result true in
def test (x y : Int64) : Bool :=
  x = y && x == y

in your case:

def test (x_1 : u64) (x_2 : u64) : u8 :=
  let x_3 : u8 := UInt64.decEq x_1 x_2;
  case x_3 : u8 of
  Bool.false →
    let x_4 : u8 := 0;
    ret x_4
  Bool.true →
    let x_5 : u8 := UInt64.decEq x_1 x_2;
    ret x_5
def test._boxed (x_1 : obj) (x_2 : obj) : obj :=
  let x_3 : u64 := unbox x_1;
  dec x_1;
  let x_4 : u64 := unbox x_2;
  dec x_2;
  let x_5 : u8 := test x_3 x_4;
  let x_6 : obj := box x_5;
  ret x_6

we are interested in the test version which as you can see ends up using decidable equality on UInt64 in both cases.

[Geoffrey Irving]

Thank you! I will be using set_option trace.compiler.ir.result true a lot (and I also didn't know about the in syntax).