[NFC] Chore: Canonicalise Bits of BitStream.addAux to match subAux and negAux

[AtticusKuhn]

Before, there was an in-congruity where subAux and negAux would return the result bit on the left and the carry bit on the right. However, addAux was defined in such a way so that the result bit was on the right and the carry bit is on the left.

This PR swaps the bits for addAux so that addAux matches the convention of subAux and negAux.

This is a non-functional refactor. It does not add any new features.

[github-actions[bot]]

Alive Statistics: 64 / 93 (29 failed)

[github-actions[bot]]

Alive Statistics: 64 / 93 (29 failed)

[tobiasgrosser]

Nice. Can we get a quick review from @Equilibris?

[github-actions[bot]]

Alive Statistics: 64 / 93 (29 failed)

[AtticusKuhn]

In general there are two ways we might fix this issue:

option #1:

/--
addAux' is the old version of addAux, which is kept around for backward-compatability reasons.
To use the new version, use addAux
-/
def addAux' (x y : BitStream) : Nat → Bool × Bool
  | 0 => BitVec.adcb (x 0) (y 0) false
  | n+1 =>
    let carry := (addAux' x y n).1
    let a := x (n + 1)
    let b := y (n + 1)
    BitVec.adcb a b carry

/--
The reason that there is a Prod.swap in the definition of addAux is that
BitVec.adcb returns the carry bit on the left and the result bit on the right.

In order to preserve the same design as subAux and negAux, we use Prod.swap
so that the result bit is on the left and the carry bit is on the right.

The un-swapped version is still availiable as addAux'
-/
@[simp]
def addAux (x y : BitStream) : Nat →  Bool × Bool := Prod.swap ∘ (addAux' x y)

or option #2:

def addAux (x y : BitStream) : Nat → Bool × Bool
  | 0 => Prod.swap (BitVec.adcb (x 0) (y 0) false)
  | n+1 =>
    let carry := (addAux' x y n).1
    let a := x (n + 1)
    let b := y (n + 1)
    Prod.swap (BitVec.adcb a b carry)

I have chosen option #1.

[tobiasgrosser]

Why would we want to keep around the old version? Is the new version not strictly better? In case it is, I suggest to just drop the old version.

[tobiasgrosser]

The reason that there is a Prod.swap in the definition of addAux is that BitVec.adcb returns the carry bit on the left and the result bit on the right.

In that case, would it not be better to follow the convention in adbc and always return the carry bit on the left in all our implementation? Or is lean inconsistent within itself?

[AtticusKuhn]

Great, thanks for your feedback.

[github-actions[bot]]

Alive Statistics: 64 / 93 (29 failed)

[github-actions[bot]]

Alive Statistics: 64 / 93 (29 failed)

[github-actions[bot]]

Alive Statistics: 64 / 93 (29 failed)

[github-actions[bot]]

Alive Statistics: 64 / 93 (29 failed)

[github-actions[bot]]

Alive Statistics: 64 / 93 (29 failed)

[AtticusKuhn]

I think this is good to go now. If you could rebase your other patch on this one, I can look at the actual problem.

Got it. I have done that now:

https://github.com/opencompl/lean-mlir/pull/554/files