Proposed refactor of Bitvec

Stream: mathlib4

[Alex Keizer]

There's been some discussion on what is the appropriate representation of bitvectors.

Currently, we have Bitvec n defined as Vector bool n. @Harun Khan and @Abdalrhman M Mohamed are proposing to change this to Fin (2^n), the definition they've been using in lean-smt, which is more efficient computationally, and allows us to reuse existing theorems on Fin or Nat more easily.

However, this definition does put us farther away from the perspective of Bitvec as, well, a vector of bits, and the Fin-based definition might make it harder to prove theorems that mix bitwise operations and arithmetic.

Thus, we propose to have both definitions, say Bitvec n := Fin (2^n) and another type abbrev Bitvec.BitVector n := Vector bool n (exact name T.B.D.). We'd suggest the Fin-based definition as the one to primarily use in definitions and to state theorems, to reduce duplication. But we do keep the Vector-definition, after proving that the isomorphism translates, say, Bitvec.and to Bitvec.BitVector.and, as an internal detail of the proofs of these theorems when appropriate. We are working on a draft PR that moves the current Bitvec theory to Bitvec.BitVector.

Does this plan make sense as a way to go forward?

[James Gallicchio]

If you're only using it as a theoretic model, I'm wondering if Fin n -> Bool isn't more appropriate than Vector Bool n?

[James Gallicchio]

or is the intention to preserve the current vector based interface as a deprecated api?

[Alex Keizer]

Some part of wanting to stick with Vector comes from it's current API and particularly it's recursion principles (Vector.inductionOn/Vector.revInductionOn). I don't think Fin n -> Bool has as nice of an API currently, but it could of course always be developped

[Kyle Miller]

Are you familiar with docs#Matrix.vecEmpty, docs#Matrix.vecCons, and the ![x0, x1, ..., xn] : Fin (n + 1) -> X vector notation?

[Kyle Miller]

Vector seems fine too, and it might be easier in some ways to develop API for it just because there's a Vector namespace and you can use dot notation.

[Alex Keizer]

I am, but Matrix is two-dimensional, right? There is also Vector3, which is more akin to Fin n -> Bool (Although it uses Fin2 instead), but Vector3 has much less than Vector. In particular, currently a lot of bitvector operations are defined in terms of Vector.mapAccumr, and I'm working on a PR that adds a lot of simplification lemmas for this. Ideally, I'd like mapAccumr to be defined in terms of some generic Foldable typeclass, and define these simplificaiton lemmas also generically (w.r.t. to some laws that should hold for the Foldable)

[Alex Keizer]

But, maybe let's first get consensus for the approach of having two bitvector definitions, a computationally efficient one with Fin, and a more semantically "Vector"-like definition (in terms of Vector, Fin n -> Bool, Vector3, or some other T.B.D. option)?

[Alex Keizer]

@Harun Khan, you did a +1 on the original post one, I guess that means you are on board?

[Alex Keizer]

@Mario Carneiro could you maybe weigh in, does this plan make sense?

[Kyle Miller]

It's in the Matrix namespace, but take a look at the types, they're Fin n -> X. (Matrices that are m x n are modeled as nested Fin m -> Fin n -> X vectors-of-vectors.)

[Harun Khan]

Alex Keizer said:

Harun Khan, you did a +1 on the original post one, I guess that means you are on board?

Yes. This plan sounds good!

[Wojciech Nawrocki]

Alex Keizer said:

But, maybe let's first get consensus for the approach of having two bitvector definitions, a computationally efficient one with Fin, and a more semantically "Vector"-like definition (in terms of Vector, Fin n -> Bool, Vector3, or some other T.B.D. option)?

Chiming in as I am responsible for the comment promoting the Fin (2^w) version. I believe that having two versions connected by extensionality lemmas is basically necessary if you want to switch between the bitwise and more arithmetic viewpoints, and to prove lemmas about both.

[Wojciech Nawrocki]

Btw, I have now come to believe that (although it is good to have), in the Fin (2^w) variant having a nice computational representation is less important than the fact that it gives you the entire docs#ZMod theory for free.

[Alex Keizer]

I suspect we're not really getting ZMod for free. We still have to prove the equivalence between Vector Bool n and Fin (2^n), which would also give us the ZMod theory for the Vector definition, right?

[Alex Keizer]

In any case, I'll continue with the proposed PR. I think keeping the Bitvec.BitVector definition based on Vector is the easiest way to go forward with this change. If we do want to change that to, say, Fin n -> Bool, I propose we do so in a subsequent PR

[Chris Hughes]

My perspective is that we should have Bitvector as Fin (2^n) because it is the fastest one, and maybe Bitvector is something people actually want to compute with from time to time.

As Alex said, it doesn't really save any work or create any work in terms of proof. We still want to know the Bitvector definitions of addition and so on in terms of folding over a vector, and we want to know that these are isomorphic to the definition on ZMod. I personally would advocate for defining Bitvec to be Fin, and proving an isomorphism with Vector n Bool (I personally wouldn't make any abbreviations as Alex suggested). I would also define a bunch of recursion principles directly on Bitvec that allowed you to think and reason about Bitvec as though it were a Vector, without invoking the isomorphism with Vector.

[Mario Carneiro]

My impression from mathlib experience is that we have tried every representation under the sun and have now mostly settled on Fin n -> A or a type wrapper around it for fixed length vectors. So I am dubious about putting more work into Vector n A. I agree with Chris regarding Fin (2^n) as the "official" representation, since that's pretty close to what you want from a real bitvector type.

[Mario Carneiro]

I would like to see more regarding why we need bitvector anything, what is the actual use case?

[Mario Carneiro]

For implementing most fixed width integer operations Nat.bitAnd et al seem to be sufficient

[Alex Keizer]

Thanks for your input! Then I guess we want to end up with (a wrapper around) Fin n -> Bool as the semantic Vector-like definition eventually. But, would you agree it makes sense to split this in two: first rename the existing Vector definitions and introduce a more efficient Fin (2^n) as the main representation. Then, in a second PR, reimplement the Vector definitions in terms of Fin n -> Bool?

[Alex Keizer]

Also, I got the impressions Vector was preferred over Vector3 (i.e., Fin n -> A), since it has the shorter, more obvious name. If you suggest Fin n -> A should be the preferred encoding of fixed length vectors, would it make sense to name that one Vector, and call the other one, say, VectorList (to indicate it's based on List)? Possibly with documentation to indicate Vector (i.e., Fin n -> A, post-rename) is generally preferred?

[Mario Carneiro]

Also, I got the impressions Vector was preferred over Vector3 (i.e., Fin n -> A), since it has the shorter, more obvious name.

That's not a correct inference. A shorter name can also mean that it is the older version which got the good name and is preserved for compatibility purposes

[Mario Carneiro]

this is especially true for types that were in core for a long time, since this largely prevented iterating on the design or making any naming changes

[Mario Carneiro]

As Kyle linked earlier, the modern mathlib spelling uses Fin n -> A directly, and the ![...] literal syntax is for constructing such functions

[Alex Keizer]

Sorry, I should have clarified. I am not disagreeing with you, I'm saying that as someone who isn't as familiar with mathlib, it is difficult to see which definition to use. The naive strategy of "just pick the one with the most obvious/nice name, since that is probably the preferred version" apparently doesn't work. I'm asking if it would make sense to change the names (at some point in the future) so that the actually preferred version does have the nicer name.

[Alex Keizer]

Mario Carneiro said:

As Kyle linked earlier, the modern mathlib spelling uses Fin n -> A directly, and the ![...] literal syntax is for constructing such functions

Isn't it benificial to have a namespace for such vectors? For example, a lot of the bitvec definitions currently use Vector.mapAccumr (which is essentially a specialized version of a monadic foldr), how would I call the Fin n -> A version of that operation, if we just use Fin n -> A directly everywhere?
I could always define Bitvec.mapAccumr directly, but that seems like a missed oppurtunity for code reuse.

[Alex Keizer]

That's also what bothers me a bit about, say Typevec n (which is defined as Fin2 n -> Type u). All of the vector operations are re-implemented in the Typevec namespace. We could do the same for BitVector n, but then we have a lot of duplication.

[Alex Keizer]

(deleted)

[James Gallicchio]

definitely worth having a namespace. not really sure why mathlib just uses Fin n -> A directly, is there a thread about why that became standard practice?

[Wojciech Nawrocki]

Alex Keizer said:

I suspect we're not really getting ZMod for free. We still have to prove the equivalence between Vector Bool n and Fin (2^n), which would also give us the ZMod theory for the Vector definition, right?

Yes, exactly. But once you prove the core Vector Bool n ≃ Fin (2^n) equivalence, a lot of the theory should hopefully transfer.

[Eric Wieser]

The equivalence essentially amounts to a docs#FinEnum instance I think

[James Gallicchio]

(which could be automatically inferred if bitvec is taken as Fin n -> Bool :wink:)

[Eric Wieser]

The current instance is awful computationally though

[Eric Wieser]

And you'd want a proof the order is lexicographic

[Alex Keizer]

I PRed the proposed refactor at https://github.com/leanprover-community/mathlib4/pull/5687. For now, I've kept the alternative definition as Vector Bool n. I suggest we make the move to Fin n -> Bool, if desired, in a subsequent PR.

[Eric Wieser]

This is hard to review on github because you're moving A -> B then replacing A with something else

[Eric Wieser]

I think it would be best to leave the names as is for now, and introduce the new version in terms of Fin as BitVec; it's much easier to review a PR that moves around the names when it's separate to one that adds a load of content

[Alex Keizer]

This one doesn't add any new content, besides the bare-bones for the new Bitvec := Fin (2^n) definition. All of the content in Bitvec.BitVector.Defs and Bitvec.BitVector.Lemmas are directly taken from the previous Bitvec.Defs and Bitvec.Lemmas files (modulo namespace renaming)

[Alex Keizer]

Or do you mean that I should first change the namespaces in one PR (without moving the files), and then in a second PR do the moving of the files (without touching the contents)?

[Alex Keizer]

OK, I completely removed the Bitvec definition, which has made GitHub realize that the BitVector files are just renames of existing files. I'll re-add the new definitions in another PR, after this gets merged

[Eric Wieser]

Note that the PR title is now misleading

[Tobias Grosser]

Thank you @Alex Keizer. The diff now really shows that the actual theorems remain unchanged. That should simplify reviewing given that we already agreed on the rename. Thank you @Eric Wieser for pointing this out.

[Eric Wieser]

Did we agree on the rename? I didn't see the message above. It would be great to link to the zulip message from the PR!

[Tobias Grosser]

My understanding was that there was agreement to move Bitvec to Fin (2^n), but maybe I missed something. Here the positive messages that I found, I guess you did not vote for Bitvec as Fin (2^n), so maybe I was too fast. Sorry for this. As I am not very active her, let me take a step back and wait for more established people to advice on how to advance.

Below some of the positive messages that i found:

---

Harun Khan said:

Alex Keizer said:

Harun Khan, you did a +1 on the original post one, I guess that means you are on board?

Yes. This plan sounds good!

---

Wojciech Nawrocki said:

Alex Keizer said:

But, maybe let's first get consensus for the approach of having two bitvector definitions, a computationally efficient one with Fin, and a more semantically "Vector"-like definition (in terms of Vector, Fin n -> Bool, Vector3, or some other T.B.D. option)?

Chiming in as I am responsible for the comment promoting the Fin (2^w) version. I believe that having two versions connected by extensionality lemmas is basically necessary if you want to switch between the bitwise and more arithmetic viewpoints, and to prove lemmas about both.

---

Chris Hughes said:

My perspective is that we should have Bitvector as Fin (2^n) because it is the fastest one, and maybe Bitvector is something people actually want to compute with from time to time.

---

Mario Carneiro said:

I agree with Chris regarding Fin (2^n) as the "official" representation, since that's pretty close to what you want from a real bitvector type.

[Eric Wieser]

None of those messages seem to suggest that we should be keeping the Vector Bool n implementation under a longer name though, right? sorry, that's the original post!

[Eric Wieser]

@Chris Hughes said:

I personally wouldn't make any abbreviations as Alex suggested).

Chris, just to check I understand correctly; you are advocating that all the bit API for Vector Bool n should just be dropped, and inlined into lemma statement about the replacement API on NewBitvector = Fin (2^n) and NewBitvector.toBoolVector? If so, I think I agree with this

[Alex Keizer]

Indeed, that is what Chris suggested. I personally like the idea of having a separate namespace to organize the Vector-like definitions, but am not opposed to implementing the inlined-lemmas approach, if that is the consensus of the community.

[Alex Keizer]

/poll How should we refactor Bitvec

1. Keep it as-is (only the Vector bool definition)
2. Change it to Fin (2^n); move the existing Vector Bool n API to a new type Bitvec.BitVector
3. Change it to Fin (2^n); drop the existing API and inline it in lemmas that relate, say Fin.add to Vector.mapAccumr (the current implementation of bitwise addition on Vector Bool)
4. Something else

[Alex Keizer]

@Eric Wieser @Wojciech Nawrocki @Chris Hughes @Mario Carneiro @Harun Khan @James Gallicchio You've all expressed opinions in this thread, if you could cast your vote in the poll above, or explain why none of these options seem appropriate for you, then I know which one to implement

[Harun Khan]

I chose 3 because now I'm not completely convinced that one needs the type Bitvec.BitVector anyway. Inlining it with the equivalence lemmas sounds like a good option :).

[Chris Hughes]

Eric Wieser said:

Chris Hughes said:

I personally wouldn't make any abbreviations as Alex suggested).

Chris, just to check I understand correctly; you are advocating that all the bit API for Vector Bool n should just be dropped, and inlined into lemma statement about the replacement API on NewBitvector = Fin (2^n) and NewBitvector.toBoolVector? If so, I think I agree with this

I voted for 3. I wouldn't rename Vector Bool n because the name is completely clear already, and nobody will know at first what Bitvec.BitVector

I think there should not be add and things defined on Vector Bool n, anything that's not about generic Vectors should be on Bitvec.

[Eric Wieser]

Some of the shift primitives on BitVector might make sense to generalize to Vector T n

[Eric Wieser]

Maybe that should be the first phase of the refactor; turn as many definitions as possible into result about Vector T instead of Vector Bool, and implement the BitVector ones in terms of the general ones

[Alex Keizer]

I think only the shift primitives, and a congruence definition w.r.t. the length of the vector, can be generalized, the other definitions seem pretty specific to the interpretation of a Bitvec as a number.

/-- Create a vector from another with a provably equal length. -/
protected def congr {n m : ℕ} (h : n = m) : Vector α n → Vector α m

/-- `shiftLeftFill v i` is the vector obtained by left-shifting `v` `i` times and padding with the
    `fill` argument. If `v.length < i` then this will return `replicate n fill`. -/
def shiftLeftFill (v : Vector α n) (i : ℕ) (fill : α) : Vector α n

/-- `shiftRightFill v i` is the vector obtained by right-shifting `v` `i` times and padding with the
    `fill` argument. If `v.length < i` then this will return `replicate n fill`. -/
def shiftRightFill (v : Vector α n) (i : ℕ) (fill : α) : Vector α n

I PRed this at https://github.com/leanprover-community/mathlib4/pull/5896 (currently awaiting CI)

[Alex Keizer]

There seems to be a preference for dropping and inlining the current API. So then I guess the next step is to introduce the new Fin-based definition? @Harun Khan you seem to have this already, can you get a PR started?

[Eric Wieser]

Are there any lemmas about BitVector.shl that generalize too?

[Alex Keizer]

There's no theorems about shifts at all yet

[Wrenna Robson]

Just want to chime in to say that I have just encountered the utility of being able to move between Fin(2^n) and Fin n -> Bool, and having an API for that would be very useful.

[Wrenna Robson]

Specifically actually I had a context where I was considering Fin((2*n + 1)*2^n) -> Bool, and it is useful to think of this as Fin (2*n + 1) → (Fin n → Bool) → Bool

[Wrenna Robson]

(Not sure if we have a good way of going Fin(a*b) -> (Fin a -> Fin b) in the natural way - obviously there's some wrinkles there.)

[Alex Keizer]

Do you mean you'd just like an API to translate between these contexts (i.e., option 3 from the poll above), or that you'd want to have an API to, say, add Fin n -> Bools together (i.e., option 2 from the poll)?

[Wrenna Robson]

Hmm - I thought both option 2 and option 3 were about Vector rather than Vector3? Vector (which I think is the subtype definition?) is basically of no interest to me.

[Wrenna Robson]

It would be quite nice to have an API to add Fin n -> Bool together, but I would accept some nice way of translating it forward and backwards. In a sense, you want to move to Fin n -> Bool when you're doing operations like, say, "add in an extra bit at the 4th place", which is natural there. So it doesn't need arithmetic - it makes sense to do arithmetic at Fin(2^n) for sure.

[Alex Keizer]

Yeah, the move from Vector to Fin n -> Bool was suggested already, but it's in a sense orthogonal. First we wanted to reach consensus about what Bitvec's definition should be, and whether we'd have an alternative, more vector-like definition, and later we might move this vector-like definition to Fin n -> Bool

[Alex Keizer]

Do note that Vector3 is different from both of these still, that one is defined as Fin2 n -> A, instead of Fin n -> A!

[Wrenna Robson]

Oh yes, doy. Well, I see what you're saying.

[Wrenna Robson]

I think I'm going to vote for 3 because in a sense I don't think Fin n -> Bool should have a special name!

[Wrenna Robson]

Oh - you'd want a good way to work with endianness.

[Wrenna Robson]

i.e. for f : Fin n -> Bool, is f 0 the MSB or LSB? It can be either!

[Wrenna Robson]

Also pretty printing of bitvectors has some utility... I don't know if that's a thing we can do for such types easily currently.

[Alex Keizer]

If you don't have an API to do arithmetic on Fin n -> Bool, then endianness doesn't really matter, right? We'd only care about that at the border, i.e,. when defining the equivalence between Bitvec n and Fin n -> Bool. We currently use the convention that v[0] is the MSB, so I'll assume we continue to do so

[Mario Carneiro]

I highly recommend using v[0] as the LSB (aka little endian)

[Mario Carneiro]

IMO that was the biggest issue with the lean 3 bitvec

[Alex Keizer]

I wonder if it matters that much, if we have a reverse induction principle on vectors. You are right in that the bitwise arithmetic operations generally operate from the LSB to the MSB, so little endian would make it a bit more natural

[Wrenna Robson]

I am certainly currently considering a context where it does matter. Suppose as I said above I am considering Fin((2*n + 1)*2^n) -> Bool (which I suppose in turn could be interpreted as Fin(2^((2n + 1)2^n)) but I don't wish to do this), and I want to re-interpret this as Fin (2*n + 1) → (Fin n → Bool) → Bool. Indeed, in that context, I am then also going to want to, like, considering the Fin n -> Bool part, going to also want to think about Fin (n + 1) -> Bool, and then think about "deleting" a bit. I just want to be clear as to which bit, like, is represented by v[0] in that.

I think I agree with Mario that little-endian is better. It makes more sense to me that the 0th bit represents 2^0, the 1st bit represents 2^1, and so on.

If you had a good "bit reverse" operation and API around that, of course, it wouldn't matter too much - but I think little-endian is the way to go.

[Eric Wieser]

docs#finReverse

[Harun Khan]

Alex Keizer said:

There seems to be a preference for dropping and inlining the current API. So then I guess the next step is to introduce the new Fin-based definition? Harun Khan you seem to have this already, can you get a PR started?

Sure!

[Harun Khan]

Mario Carneiro said:

I highly recommend using v[0] as the LSB (aka little endian)

Yes! This is alot better because Nat.testBit 0 is also the lsb and Data.Nat.Bitwise (the file that uses testBit) is really clean.

[Alex Keizer]

Allright, there seems to be clear consensus that little endian is the way to go (if anyone disagrees, please speak up).

[Wrenna Robson]

Further thoughts: there are issues with Bool. https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Algebraic.20structure.20on.20Bool

[Wrenna Robson]

Specifically: I see computer scientists happily and interchangably use logical operations (and/or/xor) on bitvectors, and also sometimes addition, where addition means addition as bitvectors (that is to say, bitwise-xor).

[Wrenna Robson]

Bool doesn't provide +/*/0/1, so you will not, for free, get "0" as a zero vector.

[Wrenna Robson]

Instead it will be ⊥. I would say that that will seem perverse notation to most people who might use this part of the library.

[Wrenna Robson]

@Harun Khan in particular, if you're starting a PR, I would be interested in your thoughts.

[Eric Wieser]

An argument against using Fin 2 instead of Bool is now you have two ways to spell everything not one

[Wrenna Robson]

Yeah I mean I think Bool is better for this.

[Wrenna Robson]

I just also think that Bool should have +/*/0/1

[Eric Wieser]

Having two ways to spell the same thing is bad because now every lemma that mentions one thing has to be duplicated, every lemma that mentions two has to be quadrupled, ...

[Wrenna Robson]

i.e. Field Bool does not to me feel unreasonable.

[Eric Wieser]

Or you make simp lemmas that turns one spelling into the other, and essentially say "0 : Bool exists, but the only lemma we will write about it is 0 = false"

[Wrenna Robson]

Eric Wieser said:

Having two ways to spell the same thing is bad because now every lemma that mentions one thing has to be duplicated, every lemma that mentions two has to be quadrupled, ...

I don't disagree but because you can't get rid of Fin 2 and I assume you couldn't just define Bool as a synonym of Fin 2 to a degree this tension is there.

[Wrenna Robson]

Sure - how do you think the zero bitvector should be spelled?

[Eric Wieser]

Sorry, I should have been clear that I meant two ways to spell the same "function". I don't hold that opinion as strongly for types.

[Kyle Miller]

A point in favor for defining bit vectors as Fin n -> Fin 2 is that you can use coercions go from each Fin 2 element to Nat or Int. Then the bitwise-or is ⊔, right?

[Wrenna Robson]

I feel like you're getting into the weeds here when ultimately I don't disagree with you. It's bad to have two ways of spelling the same thing. I just ran into the pitfall that I was expected 0 : Fin n -> Bool to exist and it doesn't.

[James Gallicchio]

I am also guessing any context where you want to handle bools as elements of Z/2 it would be fine to insert an explicit coercion Bool.toFin : Bool -> Fin 2, so I don't really know that this needs to be hashed out right now.

[Wrenna Robson]

I think nearly every context in which you would want to use bitvectors, you would want 0 to mean the zero bitvector.

[James Gallicchio]

Yes, but that would be covered by having an OfNat Bitvector 0 instance.

[Wrenna Robson]

Fair.

[Eric Wieser]

I think this is the same argument as "if I want to use a single bit, I want to talk about 0/1 not true/false"

[Wrenna Robson]

It is certainly related.

[James Gallicchio]

I do think it would be reasonable to add OfNat Bool 0/1 to mathlib, even if we don't add Add Bool

[Eric Wieser]

If you do that none of the lemmas about true and false work when you're using it

[Alex Keizer]

You could have a simp lemma that rewrites 0 : Bool to false

[James Gallicchio]

simp lemma to true/false seems fine with me. I just sometimes want to write 0/1 in source cuz it's more readable to have 1-wide characters there.

[James Gallicchio]

although now that I think more on it, using 0/1 outside the context of bitvectors is a bit cursed... I take it back!

[Wrenna Robson]

James Gallicchio said:

I do think it would be reasonable to add OfNat Bool 0/1 to mathlib, even if we don't add Add Bool

It is mildly odd to me, at least that while presumably when moved inline, you would have the instance of Xor (Bitvec n) still, but that Xor operation isn't much related to other things.

[Eric Wieser]

James Gallicchio said:

I just sometimes want to write 0/1 in source cuz it's more readable to have 1-wide characters there.

But as soon as you start writing lemma statements you'll be forced to use true and false again, otherwise the simpNF linter will complain at you

[Kyle Miller]

Eric Wieser said:

I think this is the same argument as "if I want to use a single bit, I want to talk about 0/1 not true/false"

This is basically what I was trying to say. Plus, Fin 2 gives you zero/false as 0, one/true as 1, + as xor, * as mul/and, and ⊔ as or, so there's no need for new operations to handle all the basics.

[Eric Wieser]

I don't think you need new operators whatever you do, right?

[Wrenna Robson]

Well, you need ^^^ for xor-ing bitvectors.

[Eric Wieser]

That's docs#symmDiff

[Eric Wieser]

Which works for both spellings

[Eric Wieser]

All the bitwise operations you need exist on bool. Fin gives you duplicate spellings for some of them.

[Kyle Miller]

Eric Wieser said:

I don't think you need new operators whatever you do, right?

There's this talk about using 0 and 1, which are 0-ary operators, and adding + and * to Bool

[Wrenna Robson]

That is true, ∆ does exist.

[Wrenna Robson]

I suppose - from my point of view, this is a library.

[Eric Wieser]

I think my point is that the only argument is here is notation. The operations themselves are already defined on both types, just with spellings that have the "wrong" notation.

[Wrenna Robson]

It is designed to be used by people.

[Wrenna Robson]

Yes, I think it is just a notation issue - if you can seamlessly handle the notation issue then it's all gucci.

[Eric Wieser]

We've already forced mathematicians to use \bot for the 0 submodule

[Wrenna Robson]

I think a) that's more natural, b) they whine less.

[Eric Wieser]

(though admittedly we do have a 0 : Submodule R M instance too, but that's because we actually want the semiring structure)

[Wrenna Robson]

I didn't say that and you can't quote it against me professionally.

[Kyle Miller]

Eric Wieser said:

I think my point is that the only argument is here is notation

Right, I don't mean to say the operations don't exist, just that basically the correct notation already exists for Fin 2. I'm only talking about notation.

[Kyle Miller]

(unless people want && and || notation extended to these vectors)

[Wrenna Robson]

But "⊥ ∆ k is the correct notation for xor-ing a bitvector k with 0" is like. It reminds me of this meme.
image.png

[James Gallicchio]

We can have whatever notation we want for bit vectors. The thing that is (somewhat) constrained is notation on elements of the bitvector, be they Fin 2 or Bool, since the types have somewhat different notations

[Eric Wieser]

I think that is mathlib's stance, because it gives you the lemma docs#bot_symmDiff

[Alex Keizer]

Kyle Miller said:

(unless people want && and || notation extended to these vectors)

That is exactly what I planned, with the non-short-circuiting versions &&& and |||, at least

[Wrenna Robson]

yes, and I feel very affectionate about mathlib

[Wrenna Robson]

But I'm sort of merrily and with no judgement noting that it is, well. Eccentric.

[James Gallicchio]

mathlib is in the weird position of being forced to regularize/unify notation that historically has never been aligned :rofl: the computer scientist in me is not used to it.

[Wrenna Robson]

I am happy with the idea that that is how you spell it for proofs, to stop the lemma multiplication issue, and that the simp-normal form of (0 + k) should be (⊥ ∆ k) when k is a bitvector. It is weird but that is the nature of proofs. It feels Odd to me that that former wouldn't work.

[Alex Keizer]

To me, it seems more natural to have + refer to addition in the regular, numeric sense. I feel that having + refer to xor would be very surprising, given that we have an explicit xor operator typeclass and notation ^^^.

[Kyle Miller]

James Gallicchio said:

We can have whatever notation we want for bit vectors.

There are limits though -- for this to be mathlib-friendly you want the notation to all be compatible in the sense of being within the theory of some sort of structure. Mixing */+ and ⊓/∆ is already going to lead to the pain. (A mild but persistent pain.)

[Eric Wieser]

A type synonym that converts one notation to the other is probably a good idea

[Wrenna Robson]

Alex Keizer said:

To me, it seems more natural to have + refer to addition in the regular, numeric sense. I feel that having + refer to xor would be very surprising, given that we have an explicit xor operator typeclass and notation ^^^.

This is interesting. But I note that a bitvector does not unambiguously represent a natural.

[James Gallicchio]

Alex Keizer said:

/poll How should we refactor Bitvec

1. Keep it as-is (only the Vector bool definition)
2. Change it to Fin (2^n); move the existing Vector Bool n API to a new type Bitvec.BitVector
3. Change it to Fin (2^n); drop the existing API and inline it in lemmas that relate, say Fin.add to Vector.mapAccumr (the current implementation of bitwise addition on Vector Bool)
4. Something else

perhaps people want to reconsider their votes here...

[Wrenna Robson]

And I actually think that, while we should (as discussed above) provide the machinery to dip over to the Fin(2^n) form and back again when doing arithmetric, you should be neutral about what a Bitvector represents.

[Wrenna Robson]

Indeed, there are various horrible, terrible tricks (that real humans regrettably do) that come from taking a vector of bits that was a natural, and reinterpreting it as, say, a floating-point number.

[Eric Wieser]

Eric Wieser said:

A type synonym that converts one notation to the other is probably a good idea

The data already exists, it's docs3#boolean_algebra.to_boolean_ring. This already exists, it's docs#AsBoolRing !

[Reid Barton]

The neutral option would be to not have anything called "a bitvector" at all and just let people write Fin n -> Bool, Fin n -> Fin 2, Fin (2^n), whatever they mean

[Reid Barton]

Heck you could use a list if you're into that sort of thing.

[Wrenna Robson]

I think there are substantial advantages to having clearly indicated spellings for various purposes and interpretations.

[Alex Keizer]

There is a tension here between wanting neutral/general representations, and not wanting multiple, redundant, representations.

[Wrenna Robson]

Otherwise people will definitely use one when they really should have used another.

[Reid Barton]

right, but this seems incompatible with

you should be neutral about what a Bitvector represents.

[James Gallicchio]

Two (named) types: BitVector n (represented as Fin n -> Bool, implemented as Fin (2^n)) and FixedWidth n (represented as Fin (2^n)). APIs for both, conversions between them.

I posit nobody actually wants Fin n -> Fin 2.

[Wrenna Robson]

A Bitvector should almost certainly (to me) be a vector of bits. That is to say, it's of type Fin n -> Bit where Bit is the type that represents the singular unit of information.

[Eric Wieser]

FWIW, the isomorphism between the last two of Reid's suggestions already exists as docs#finFunctionFinEquiv (and the one between the first two is boring)

[Wrenna Robson]

Bit is nearly certainly Bool I think.

[Wrenna Robson]

James Gallicchio said:

Two (named) types: BitVector n (represented as Fin n -> Bool, implemented as Fin (2^n)) and FixedWidth n (represented as Fin (2^n)). APIs for both, conversions between them.

I posit nobody actually wants Fin n -> Fin 2.

Yes I think I agree with this - my original post was that people would want to use +/0 on -> Bool, but I actually think they wouldn't want to use Fin 2 for that!

[Alex Keizer]

There's also a risk of premature generalization. I am interested in developing a theory of bitvectors that involves doing arithmetic on them as if they are (signless) integers. It would be nice to have a type for this were I can just use +.

[Reid Barton]

James Gallicchio said:

I posit nobody actually wants Fin n -> Fin 2.

I'm very sure there are people who do want Fin n -> Fin 2, but they might be disjoint from the set of people who would use the word "bitvector".

[Eric Wieser]

I would guess that anyone wanting to prove things about bitwise operations alone would prefer Fin n -> Fin 2

[Wrenna Robson]

To quote Wikipedia (dangerously): "These values are most commonly represented as either "1" or "0", but other representations such as true/false, yes/no, on/off, or +/− are also widely used. "

In a sense this is the issue. While I think in practice Bit should probably be Bool, actually Bit is NOT Bool. To get slightly philosophical: Bool represents decided truthiness - it is the type of decide p for decidable statements p. Wheras Bit is the type that fundamentally represents the basic unit of information - which is conceptually distinct from the basic unit of truth.

[James Gallicchio]

also worth having a FixedWidth type so that we can get all the UIntXs into a consistent proving API...

[Wrenna Robson]

James Gallicchio said:

also worth having a FixedWidth type so that we can get all the UIntXs into a consistent proving API...

Yes, definitely.

[Eric Wieser]

I think there are technical reasons why the Uint types are distinct, related to native compilation

[James Gallicchio]

Wrenna Robson said:

Wheras Bit is the type that fundamentally represents the basic unit of information - which is conceptually distinct from the basic unit of truth.

Still not sure that means we should have a separate type for it. You have to have some asymmetry in Bit by choosing an order, which makes it equivalent to Bool again...

[Wrenna Robson]

I actually agree.

[Wrenna Robson]

I think Bool is the way. It's also what other languages tend to do (e.g. I was just reminding myself what Rust does).

[James Gallicchio]

Eric Wieser said:

I think there are technical reasons why the Uint types are distinct, related to native compilation

Yep. But there's a whole swath of lemmas to talk about UInt operations when they could instead all be simp'd to a single FixedWidth type in proofs.

[Wrenna Robson]

(There's also the wrinkle that in practice bits don't exist - bytes do - but I think we can all agree that is overcomplicated for this issue.)

[James Gallicchio]

In fact I'd be very open to PR'ing a fixedwidth type to core so that the proof representation of the UIntX's can be FixedWidth X instead of Fin (2^X), but I don't think core would be open to it atm.

[Wrenna Robson]

James Gallicchio said:

Wrenna Robson said:

Wheras Bit is the type that fundamentally represents the basic unit of information - which is conceptually distinct from the basic unit of truth.

Still not sure that means we should have a separate type for it. You have to have some asymmetry in Bit by choosing an order, which makes it equivalent to Bool again...

In other words - I think there's a conceptual difference but not everything that has a conceptual difference needs a separate type - you have to be practical.

[James Gallicchio]

but anyways. it sounds like alex wants to make an API for going between bitwise representation Fin n -> Bool and the Fin (2^n) ring. so does it make sense to have a type for each and build the API on that?

[James Gallicchio]

(The reason to have a def for Fin n -> Bool is to get a namespace for operations, and the reason to have a def for Fin (2^n) is so that the 2^n doesn't get unfolded)

[Alex Keizer]

Although that was indeed my original proposal, now I think it would be OK to have just the name for Fin (2^n), and have all the arithmetic operations live only on that representation. However, I do think we should give a name to Fin n -> \a, so that we have a namespace for the structural operations on vectors.

[Wrenna Robson]

Is \a a generic type there?

[Alex Keizer]

Yes

[Wrenna Robson]

Could do with a name though I assume Pi types cover most of it. https://leanprover-community.github.io/mathlib4_docs/Mathlib/InformationTheory/Hamming.html is defined for Π i : ι, β i, for instance, and just uses Fintype ι (and decidable equality on the β i).

[Eric Wieser]

I think you might do better to write things about [IsPowTwo n] (x : Fin n) instead of (x : Fin (2 ^ n))

[Wrenna Robson]

I disagree with that - it is often pretty handy to have what the power is explict.

[Wrenna Robson]

So more widely, what does Fin n -> \a need to cover? I think the main one is, like, properties that come from the specific ordering on Fin n that means that we think of it as have a 0th element, next a 1st, next a 2nd, and so on.

[Eric Wieser]

Because you're in trouble when you concatenate the latter with with docs#finProdFinEquiv

[Alex Keizer]

For example, cons : \a -> (Fin n -> \a) -> (Fin (n+1) -> \a), which currently exists as Matrix.vecCons, but also things like appending two vectors, and an analogue of Vector.mapAccumr (map-accumulate)

[Wrenna Robson]

Yes, on that subject, I think I mentioned either in this thread or another that Fin 6 -> Bool, Fin 2 -> Fin 3 -> Bool, Fin 3 -> Fin 2 -> Bool are like - they naturally correspond to certain operations you perform on... well, it doesn't have to just be Bool, but you do do it on that.

[Wrenna Robson]

I don't know if people are familiar with Cryptol (https://github.com/GaloisInc/cryptol), but that does some very nice stuff with size-dependent typing and type inference (for instance, if you have a function with type signature f : [6] -> [4], where [n] is Bitvec n, you can define f = take, where take is a library function with generic type signature [n + m] -> [n], and it will work out for you that n = 6, m = 2 and f is a special case of take. You can do wackier stuff - though actually it doesn't work very well when you have bitvectors whose length are exponents - beyond the tooling).

[Reid Barton]

Alex Keizer said:

Although that was indeed my original proposal, now I think it would be OK to have just the name for Fin (2^n), and have all the arithmetic operations live only on that representation. However, I do think we should give a name to Fin n -> \a, so that we have a namespace for the structural operations on vectors.

I would be more than happy if someone wanted to take over and port mathlib#4406.

[Wrenna Robson]

Wrenna Robson said:

I don't know if people are familiar with Cryptol (https://github.com/GaloisInc/cryptol), but that does some very nice stuff with size-dependent typing and type inference (for instance, if you have a function with type signature f : [6] -> [4], where [n] is Bitvec n, you can define f = take, where take is a library function with generic type signature [n + m] -> [n], and it will work out for you that n = 6, m = 2 and f is a special case of take. You can do wackier stuff - though actually it doesn't work very well when you have bitvectors whose length are exponents - beyond the tooling).

More relevantly to my previous paragraph: defining a function as split : [6] -> [2][3] or split : [6] -> [3][2]does exactly what you expect.

[Alex Keizer]

That's cool, but adopting that would require changes to core, right?

[Wrenna Robson]

Yeah that's a good point - it's certainly not likely to be a simple refactor.

[Eric Wieser]

I would be more than happy if someone wanted to take over and port mathlib#4406.

Note that various things have grown in Mathlib.Data.Fin.Tuple since that PR was first made; so taking over should probably involve unifying it with the now-existing aPI

[Wrenna Robson]

Reid Barton said:

Alex Keizer said:

Although that was indeed my original proposal, now I think it would be OK to have just the name for Fin (2^n), and have all the arithmetic operations live only on that representation. However, I do think we should give a name to Fin n -> \a, so that we have a namespace for the structural operations on vectors.

I would be more than happy if someone wanted to take over and port mathlib#4406.

Is there a particular reason you did them as homogenous tuples?

[Reid Barton]

Yes, because dealing with possibly heterogeneous tuples is a nightmare when you actually want homogenous ones (which I did in my application).

[Wrenna Robson]

Yeah that is fair enough.

[Reid Barton]

In fact there is already something like fin.snoc and it was trying to use it and giving up which led me to write finvec.

[Wrenna Robson]

Yeah I can imagine it might be tricky.

[Wrenna Robson]

snoc or cons feel like they just won't be natural there - though as I allude to above, you somewhat do want to be able to go join (Fin n -> \a) (Fin m -> \a) and end up with a (Fin (n + m) -> \a).

[Wrenna Robson]

But cons and snoc are different because you're appending an element rather than doing arithmetic on the index.

[Alex Keizer]

Are you saying that snoc won't be natural in the homogeneous or the heterogeneous case?

[Reid Barton]

Wrenna Robson said:

snoc or cons feel like they just won't be natural there - though as I allude to above, you somewhat do want to be able to go join (Fin n -> \a) (Fin m -> \a) and end up with a (Fin (n + m) -> \a).

https://github.com/leanprover-community/mathlib/pull/4406/files#diff-23c1469dd6b09926b8ad8dff0cb586a154b0e24dec44e0d3358f98a63fa2959aR85-R92

[Eric Wieser]

@Wrenna Robson, your join already exists it's docs#Fin.append

[Wrenna Robson]

Oh I assumed it did.

[Wrenna Robson]

That wasn't "I am big brain smarter than you all because I have remembered you can add numbers".

[Wrenna Robson]

I was just trying to think through what the difference was.

[Eric Wieser]

Wrenna Robson said:

More relevantly to my previous paragraph: defining a function as split : [6] -> [2][3] or split : [6] -> [3][2]does exactly what you expect.

There is a trick with Decidable to achieve this:

import Mathlib.Data.Fin.Tuple.Basic

class When (p : Prop) [Decidable p] : Prop where
  isTrue : p

instance : @When p (.isTrue h) := @When.mk p (.isTrue h) h

def split {α : Type _} {m n mn : ℕ} [When (m + n = mn)] : (Fin mn → α) ≃ (Fin m → α) × (Fin n → α) :=
  sorry  -- Reid's code + `Fin.cast`

variable {α : Type _}

#check (split : (Fin 6 → α) ≃ (Fin 4 → α) × (Fin 2 → α))  -- ok!

Edit: oops, you wanted multiplication not addition

[Reid Barton]

FWIW in my application there were a lot of inductions on the dimension, so snoc was a frequent operation.

[Wrenna Robson]

Oh yeah I mean I can very much see why you'd do it!

[Alex Keizer]

The reason for having an alternative, more vector-like, representations of bitvectors is exactly to do inductions on the dimension, so that seems similar enough

[Wrenna Robson]

But "induction on the dimension" is, again, arithmetic on the indexing set. As opposed to List where cons/snoc doesn't have that sense.

[Alex Keizer]

Are you argueing that arithmetic on the index is bad? That is also what happens with Vector currently, IIUC

[Eric Wieser]

docs#Fin.consInduction gives you list-like induction on tuples

[Alex Keizer]

(that link 404's)

[Wrenna Robson]

Alex Keizer said:

Are you argueing that arithmetic on the index is bad? That is also what happens with Vector currently, IIUC

No, sorry!

[Wrenna Robson]

I think arithmetic on the index is extremely good and I want to do as much of it as possible.

[Wrenna Robson]

For example I also want to do things like "consider vectors of length 2^k, and induct on k".

[Wrenna Robson]

(To remove ambiguity: I mean like, Fin 2^k -> Bool, and so if you interpreted these as naturals they would be Fin (2^(2^k)), that is to say quite quickly very large.)

[Wrenna Robson]

But, as it was pointed out to me the other day... one could also interpret this as (Fin k -> Bool) -> Bool... and so we imagine vectors indexed by vectors...

[Wrenna Robson]

(deleted)

[Wrenna Robson]

A further thought (going way back to what I first brought up): how do I spell "the bit vector that is True at index i and False everywhere else"?

[Wrenna Robson]

I can't use Pi.single if there isn't a Zero instance.

[Eric Wieser]

docs#Function.update \bot i true

[James Gallicchio]

fin tuples always annoyed me for not having a namespace. might be a minority view there.

[Yaël Dillies]

Wrenna Robson said:

Bool doesn't provide +/*/0/1, so you will not, for free, get "0" as a zero vector.

It does: See docs#Bool.BooleanRing

[James Gallicchio]

( docs4#BooleanRing , docs4#BooleanAlgebra )

[Kyle Miller]

I think Yaël meant docs#instBooleanRingBool ? I didn't know about this instance, and I missed when searching inst.*Bool

[James Gallicchio]

there's also docs#instBooleanAlgebraBool

[Yaël Dillies]

Yeah sorry for not joining the discussion earlier. It seems you fluffed a lot around the absence of notation that is actually there.

[Yaël Dillies]

Kyle Miller said:

I think Yaël meant docs#instBooleanRingBool ? I didn't know about this instance, and I missed when searching inst.*Bool

... which is why I keep on sending links to the mathlib docs :laughing:

[Kyle Miller]

You mean the "mathlib3 docs" by this point, right? :wink:

[Mario Carneiro]

you sent a wrong link then, docs# links to mathlib4 now

[Mario Carneiro]

But also, I disagree with this instance, instBooleanRingBool should be a scoped instance

[Eric Wieser]

I think if we remove it it shouldn't even be scoped, we already have a type alias to apply it

[Wrenna Robson]

Yaël Dillies said:

Yeah sorry for not joining the discussion earlier. It seems you fluffed a lot around the absence of notation that is actually there.

Hmm. Sorry about that - but I am getting that it doesn't exist (though maybe I just didn't import the right file?)

[Wrenna Robson]

#check 0 : Bool doesn't work for me - what am I doing wrong/how do I get that notation?

[Wrenna Robson]

It does seem as I get the other stuff I wanted if I do import Mathlib.Algebra.Ring.BooleanRing. Arguably that is... a bit of an odd import simply to get that Bool is a ring. It feels like a weird instance!

[Eric Wieser]

I don't see why you find it weird to have to import a file with "boolean" and "ring" in the name to get a ring on booleans

[Wrenna Robson]

But thanks Yael - it would have been a lot quicker to just be told I was wrong about the lack of +/-/0/1 etc. in the first place!

[Wrenna Robson]

Eric Wieser said:

I don't see why you find it weird to have to import a file with "boolean" and "ring" in the name to get a ring on booleans

Well, because I don't want the BooleanRing stuff really! It is, clearly, a little hard to find... I don't have to import anything to get the BooleanAlgebra structure on Bool.

[Wrenna Robson]

Or, well, maybe I do but it seems if so it's a very basic import. (I was also importing Mathlib.Data.Fin.Basic so maybe that did it.)

[Alex Keizer]

To go back on topic, with how much we want to change the vector-like representation (moving from Vector Bool n to Fin n -> Bool, without giving it a special name, and changing the endianness). I don't expect it makes a lot of sense to preserve the current API. Instead, should we go ahead with #5920, and try to introduce the inlined vector-like lemmas (as discussed in the poll) afterwards?

[Andrés Goens]

Alex Keizer said:

To go back on topic, with how much we want to change the vector-like representation (moving from Vector Bool n to Fin n -> Bool, without giving it a special name, and changing the endianness). I don't expect it makes a lot of sense to preserve the current API. Instead, should we go ahead with #5920, and try to introduce the inlined vector-like lemmas (as discussed in the poll) afterwards?

Is there anything that would speak against that? (or is this PR just needing review)

[Yaël Dillies]

@Wrenna Robson, @Alex Keizer, @Tobias Grosser, would you mind discussing further the implications of a PR like #5920 ? Reviewing here has stalled because I believe no maintainer is competent enough to tell whether this is a step in the right direction.

[Yaël Dillies]

Given that he already approved related PRs to Std, maybe @Mario Carneiro has opinions too?

[Wrenna Robson]

Let me take a look. I haven't been paying close attention to this work; I seem to recall I walked back from my initial thoughts on it after the rationale for it was discussed.

[Tobias Grosser]

This PR has meanwhile in large portions been upstreamed to std4

[Tobias Grosser]

https://github.com/leanprover/std4/pull/286

[Tobias Grosser]

So we are now just adding mathlib specific features to mathlib.

[Tobias Grosser]

In fact, most of these are minor extensions.

[Tobias Grosser]

Such as https://github.com/leanprover-community/mathlib4/pull/8301.

[Tobias Grosser]

Advice on #8301 would unblock us.

[Wrenna Robson]

Tobias, could you possibly give a brief executive summary of what's ended up going into std4/what's still to go in?

[Eric Wieser]

Is there a reason that Nat.ofBits and related fallout is part of #5920? Is it replacing part of the old bitvector API, or is this a new feature being introduced at the same time as the cleanup?

[Wrenna Robson]

Wrenna Robson said:

Tobias, could you possibly give a brief executive summary of what's ended up going into std4/what's still to go in?

Actually, ignore that, everything you have in std4 now seems very comprehensible.

[Tobias Grosser]

Nice.

[Wrenna Robson]

One thing you don't seem to have - please correct me if I'm wrong: you have special functions for adding a bit to either end.

[Wrenna Robson]

What about functions for adding a bit to arbitrary places in a bitvector?

[Wrenna Robson]

Specifically "inserting" a bit, so that for a bitvector of length m, there are m + 1 possible places you could add it?

[Tobias Grosser]

I am curious, why are you asking for these functions?

[Tobias Grosser]

These seem to go beyond the featureset of the current bitvector implementation in mathlib, no?

[Wrenna Robson]

They're very relevant to some work I've been doing, enough that I have a whole parallel API I developed to use them.

[Eric Wieser]

As @Tobias Grosser alludes to, I definitely don't think #5920 should be growing new features not already in mathlib. The scope of "deduplicate what we already have" is already big enough

[Tobias Grosser]

Sure, we would like to get these to. The honest answer: we do not have more features because we are already struggeling to get the existing featureset into mathlib.

[Wrenna Robson]

for sure, I'm not saying "please add these special functions right now". Just wondering how hard it would be.

[Tobias Grosser]

Probably not that hard, given that we agreed on the representation in std4 already.

[Wrenna Robson]

What I'm not clear on is: if much of #5920 is now part of std4, and mathlib4 incorporates std4 anyway, what actually is being added/changed? And what functionality is desired to be preserved?

[Wrenna Robson]

Frankly I don't remember the current bitvector representation in mathlib being very good - I don't use it - so I'm curious what features are at stake.

[Eric Wieser]

#5920 has already absorbed the std upstreaming. Its aim is to move all the existing lemmas to be about the new bitvector instead of the old one

[Wrenna Robson]

(deleted)

[Wrenna Robson]

@Tobias Grosser what advice do you want on 8301? My only thought is that the type signature of Subtype.extendFun is slightly odd and it might be better to maintain symmetry by having the two inputs be f : Subtype p -> alpha and g : Subtype not p -> alpha? But I can't actually remember offhand if you can "not" predicates like that. Your definition is equivalent but unpacked I think.

That's minor though. What is the blocker there?

[Wrenna Robson]

Eric Wieser said:

#5920 has already absorbed the std upstreaming. Its aim is to move all the existing lemmas to be about the new bitvector instead of the old one

Well that seems pretty straightforward. The idea is to delete the old definition entirely, right?

[Tobias Grosser]

Wrenna Robson said:

Tobias Grosser what advice do you want on 8301? My only thought is that the type signature of Subtype.extendFun is slightly odd and it might be better to maintain symmetry by having the two inputs be f : Subtype p -> alpha and g : Subtype not p -> alpha? But I can't actually remember offhand if you can "not" predicates like that. Your definition is equivalent but unpacked I think.

That's minor though. What is the blocker there?

I would just like to get this one reviewed. This is a independent PR that will unblock further work on the bitvector stuff. @Eric Wieser already offered some advice which we implemented. @Yaël Dillies had some concerns, but is now unavailable for reviews due to exams. I think we would benefit from a second mathlib reviewer to make sure this PR is indeed ready to go. From my understanding it is relatively streightforward. So if you can give it a thumbs up (or point out minor issues), we could move this along.

[Tobias Grosser]

Wrenna Robson said:

Eric Wieser said:

#5920 has already absorbed the std upstreaming. Its aim is to move all the existing lemmas to be about the new bitvector instead of the old one

Well that seems pretty straightforward. The idea is to delete the old definition entirely, right?

Right. There is really very little left. We have corresponding proofs for everything that was in the old bitvector implementation and added #align to the old mathlib implementation.

[Tobias Grosser]

The last missing piece is the review of Nat.ofBits.

[Wrenna Robson]

I don't think I'm senior enough to give 8301 a a true thumbs up, but it does look fairly good! As I say I think I would make small definition changes but that's a personal preference and I don't know that it's helpful to stick my oar in there.

[Eric Wieser]

Can Nat.ofBits move to it's own PR? I think that would help with review

[Eric Wieser]

(I assume it's a prerequisite for adapting some of the old proofs?)

[Tobias Grosser]

Eric Wieser said:

Can Nat.ofBits move to it's own PR? I think that would help with review

I went into the history of Nat.ofBits. It was added in:

commit b211ed21dd53e8932bcfbcb8d1aedcdad59c7b7d
Author: Harun Khan <harun19@stanford.edu>
Date:   Sun Jun 18 01:18:59 2023 -0700

    merged recent work into bitwise.lean

as:

+def toNat (f : Nat → Bool) (z : Nat) : Nat → Nat
+  | 0 => z.bit (f 0)
+  | i + 1 => toNat f (z.bit (f (i + 1))) i

This commit never hit mathlib (as it ist still part of #5920). So, we can probably just drop Nat.ofBits and continue with life.

[Tobias Grosser]

(meaning, we add and review it later if needed)

[Tobias Grosser]

@Eric Wieser, would that simplify reviewing?

[Eric Wieser]

Tobias Grosser said:

(meaning, we add and review it later if needed)

Or add and review it in parallel; it's a reasonable function to want, but anything that makes #5920 smaller is good

[Eric Wieser]

Presumably that also saves #5920 from depending on #8301?

[Tobias Grosser]

Eric Wieser said:

Presumably that also saves #5920 from depending on #8301?

Indeed. I think your comment unlocked #5920. Great observation.

[Tobias Grosser]

I will implement it and push the changes.

[Wrenna Robson]

Having just been reading #5920... I'm not actually sure what that leaves.

[Wrenna Robson]

Apart from a few useful lemmas about 2^n here and there.

[Tobias Grosser]

Not a lot. That's the point. Mostly the #align directives for the old Bitvec proofs, which are important to be able to remove the old bitvector implementation.

[Tobias Grosser]

This hopefully gives us then a clean foundation for further work.

[Wrenna Robson]

If I'm entirely honest you might then be better to split those off in a new PR and simply abandon 5920. The main issue with it seems to be that it was this titanic PR that has got smaller thanks to all your hard work... but the history probably remains an albatross around it.

[Wrenna Robson]

But I'm a big advocate of "PRs are cheap". If the patch isn't working... make a new patch. Might not actually be the best choice here though.

[Eric Wieser]

I don't think restarting the PR is useful, the size of the diff is a much bigger factor than the length of the history

[Wrenna Robson]

Yes, I suppose. Making that smaller can't hurt.

[Wrenna Robson]

@Tobias Grosser incidentally, as I think I've said before, I would love to help out with any of this work in the future, or talk with you about what I've been doing and my whys and wherefores for that.

[Tobias Grosser]

Wrenna Robson said:

Tobias Grosser incidentally, as I think I've said before, I would love to help out with any of this work in the future, or talk with you about what I've been doing and my whys and wherefores for that.

Sure. That would be great. Just drop me an email and we can get this arranged.

[Tobias Grosser]

OK. I dropped the ofBits from #5920. Let's hope that the build goes through.

[Alex Keizer]

Sorry I wasn't around earlier today. For some context: @Harun Khan and @Abdalrhman M Mohamed were the original authors of #5920. Tobias and I have just been helping out with pushing the PR forward since we also have an interest in a stable bitvector representation.
Like Tobias mentioned, large parts of the new bitvector representation are already upstreamed, #5920 is now mostly about getting rid of the old bitvector representation in Mathlib, and adding equivalent API to the Std.BitVec type. This of course has a risk of code churn for users of the old API, but, like @Wrenna Robson mentions, the old API is not really used. At least, in the 6+ months since discussing this refactor, nobody has mentioned using the old API. (Well, we did for a while, but are now instead blocked on the refactor since we bought in and decided to go with the new representation).

[Wrenna Robson]

Am I right in saying your interest comes from an SMT solver perspective? I know we've chatted about this before but I can't recall the details.

[Alex Keizer]

Not directly, we are doing a project on formalizing the semantics of MLIR (a framework for compiler IRs evolved from LLVM), and as part of that we are formalizing an IR that does fixed-bit arithmetic. Our interest in standardizing the representation, though, is definitely in hopefully being able to use some of the SMT-solver work done by the community for proving the goals that come up in our project.

[Alex Keizer]

Wrenna Robson said:

If I'm entirely honest you might then be better to split those off in a new PR and simply abandon 5920. The main issue with it seems to be that it was this titanic PR that has got smaller thanks to all your hard work... but the history probably remains an albatross around it.

It might be worth mentioning #8345 and #8353. Those PRs together contain most of the additions made in #5920, without removing the existing API.

These definitions are factored out from #5920. That PR is blocked (and has been for quite a long time) on not wanting to lose any API for bitvectors, and has become very large.

[Alex Keizer]

However, Eric and Yael seem to not be a fan of restarting the PR, for good reasons, so it might be best to focus on getting #5920 in a state where we can do the refactor in one go

[Tobias Grosser]

Indeed. We seem to get pretty close. :smile:

[Wrenna Robson]

What I would say about #8345, from my perspective, is that I tend to live by the maxim "every definition is a debt". If you create definitions, that is not useful unless you fulfil the promise implied by their existence and add lemmas that demonstrate all the distinguishing properties they have.

[Wrenna Robson]

Unfortunately, this applies even if you're re-implementing old functions that didn't have API - it's just old debt!

[Wrenna Robson]

To give a concrete example: adc x y false = x + y, adc x y true = x + y + 1 (with appropriate extensions), adc x y b = adc y x b, and so forth.

[Wrenna Robson]

In addition, I am afraid I have had another thought. Namely: I could imagine it could be useful to have a type synonym for "Signed Bitvector", rather than, as you do currently, sort of interpreting a BitVec as both but favoring the unsigned interpretation.

[Wrenna Robson]

Probably this would be better as future work after #5920 is in though :). I can definitely see reasons why having a clear type distinguishment between SgnBitVec and BitVec would be good though!

[Eric Wieser]

Note that #5920 currently has merge conflicts

[Alex Keizer]

I've just merged master, so the conflicts should be gone

[Alex Keizer]

Wrenna Robson said:

Probably this would be better as future work after #5920 is in though :). [...]

Don't worry, I have plenty of things to add to make the API better, but let's first get the basis merged!

[Harun Khan]

Eric Wieser said:

(I assume it's a prerequisite for adapting some of the old proofs?)

It's a prerequsite for new proofs we intended to add in subsequent PRs. Specifically, now that bit-vector operations are defined as arithemtic over Fin 2^w we want to show that this is equivalent to corresponding bit-blasting operations (or corresponding operations over Fin n -> Bool). Here's an example for addition.

[Harun Khan]

Eric Wieser said:

Can Nat.ofBits move to it's own PR? I think that would help with review

Good idea. That will also reduce the size of #5920.

[Eric Wieser]

Harun Khan said:

Eric Wieser said:

(I assume it's a prerequisite for adapting some of the old proofs?)

Here's an example for addition.

I would argue that you shouldn't define bitAdd, but should instead have a lemma that says (a + b).bits j = (x.testBit j ^^ y.testBit j) ^^ carry x y j

[Wrenna Robson]

Congratulations on the successful merge.

[Wrenna Robson]

Do we have, yet, the Equiv between Fin n -> Bool and Std.BitVec? It looks like there's a bunch more stuff that would probably be useful to do, certainly...

[Wrenna Robson]

(The equiv shouldn't be particularly hard to do, given the definitions: though it is probably wise to define it in a way compatible with the rest of the API, and that might be a little harder. In particular you want it to be compatible with getLsb and getMsb in the obvious way!)

[Eric Wieser]

The reverse direction is docs#Std.BitVec.getLsb'

[Alex Keizer]

It's on the roadmap, but we don't have the full equivalence yet

[Eric Wieser]

docs#finPiFinEquiv is pretty much exactly the equivalence

[Eric Wieser]

Which leads to an obvious API gap; the equivalence between Fin and Bitvec

[Alex Keizer]

I assume you meant docs#finFunctionFinEquiv ?

[Alex Keizer]

#8775 is a simple draft that shows the equivalence with Fin n -> Bool by composing existing equivalences (like the one Eric linked), although we probably want to define the equivalence in terms of getLsb' and a (yet to-be-defined) ofFn def.

[Wrenna Robson]

Yeah, getting the equivalence is easy, the trick is then making sure that's compatible with the rest of your API.

[Wrenna Robson]

finFunctionFinEquiv is something I am intimately familiar with nowadays and it's great, but proving things about its actual values can sometimes be a little fiddly.

[Yaël Dillies]

Oh interesting. It's one of those things I added not because I needed it but because it was neat.

[Wrenna Robson]

Yeah it's been really really useful for my project I've been doing.

[Wrenna Robson]

Because I needed to do a lot of inserting and removing bits from a given place and the best way to do that is converting to tuples and using the appropriate equivs for that

[Alex Keizer]

I've been playing around with #8775, it now has a theorem that getaLsb' is an isomorpism

[Wrenna Robson]

Like, specifically defining the family of equivs Fin (m + 1) -> (Fin(2^(m+1)) \equiv Bool -> Fin(2^m)) is really nice when you have it.

[Wrenna Robson]

Which is the "isolate a particular bit" transformation.

[Wrenna Robson]

Alex Keizer said:

I've been playing around with #8775, it now has a theorem that getaLsb' is an isomorpism

This is very nice.

[Alex Keizer]

The strategy I took is to define the easy equivalence, and then proof a theorem that coercing this equiv to a function is equal to getLsb, is that a sensible proof strategy?

[Wrenna Robson]

I think that is how I would have gone about it. Though I suspect you probably want to show that the equivs are equal, not just their coercion - i.e. I would define another equiv, your "via getLsb" equiv, that has getLsb' and ofLEFn as components, and assert that these are equal as equivs. Obviously your coercion lemmas are necessary for this.

[Wrenna Robson]

You should also think about getMsb, and how it interacts with Fin.revPerm (I think this is the right thing to consider but opinions might differ).

[Wrenna Robson]

(Reasons to have an actual equiv - I am somewhat assuming your getLSB' and ofLEFn may well be faster than the implementation that comes from finFunctionFinEquiv, which isn't written for performance. It would be useful to have a performant equiv!)

[Alex Keizer]

I would also assume they're faster. I guess my question is does having a fast equiv matter, or would people use getLsb, etc. directly anyways?

[Wrenna Robson]

I would use the equivs!

[Alex Keizer]

Then again, it's easy to define the actual equiv, so I might as well

[Eric Wieser]

I think you should make the equiv fast; but more importantly, defeq to the underlying operations

[Eric Wieser]

It's very convenient to be able to use the fact that an equiv is defeq to some raw function in the goal state

[Wrenna Robson]

Just to make explicit my example of how I am currently using finFunctionFinEquiv.

def getBitRes (i : Fin (m + 1)) : Fin (2^(m + 1)) ≃ Bool × Fin (2^m) :=
calc
  _ ≃ (Fin (m + 1) → Fin 2)   := finFunctionFinEquiv.symm
  _ ≃ Fin 2 × (Fin m → Fin 2) := Equiv.piFinSuccAboveEquiv _ i
  _ ≃ _                       := finTwoEquiv.prodCongr finFunctionFinEquiv

[Wrenna Robson]

You can see how that would translate to your context. But having the actual equiv is useful.

[Wrenna Robson]

def Bitvec.getBitRes (i : Fin (m + 1)) : Bitvec (m + 1) ≃ Bool × Bitvec m :=
calc
  _ ≃ (Fin (m + 1) → Bool)   := finFunctionEquiv.symm
  _ ≃ Bool × (Fin m → Bool) := Equiv.piFinSuccAboveEquiv _ i
  _ ≃ _                       := (Equiv.refl _).prodCongr finFunctionEquiv

Specifically it would look something like this.

[Eric Wieser]

I would argue that should be called consEquiv (or do I mean concatEquiv / snocEquiv?)

[Eric Wieser]

And it should probably not be implemented that way, because we want the reverse direction to be defeq to docs#BitVec.cons

[Wrenna Robson]

I don't disagree, but currently this only exists in my project file and I intend to name everything according to convention when I port stuff.

[Wrenna Robson]

I am not re-implementing it though :P

[Wrenna Robson]

For quite a lot of reasons that I am not going to get into (mainly because Zulip is REALLY SLOW right now) I think this is the right choice, it's very convenient to work with.

[Wrenna Robson]

Anyway, it can't use cons because it isn't only for the bit on the end.

[Wrenna Robson]

Note the (i : Fin (m + 1))

[Wrenna Robson]

if we had an extension to cons that did the calculation of the residuum/its inverse in some other way... yeah fine OK. I'd still want that as an equiv though!

[Wrenna Robson]

It has been my experience that defining stuff using the standard equivalences makes things so, so much easier.

[Wrenna Robson]

(Also, huh, I would have expected what we call Bitvec.concat to be called Bitvec.snoc. ++ to me is what you would use to join two vectors together (which I would called concatenation), rather than what you would use to add an element to the end (which I would call appending).)

[Alex Keizer]

This discussion has been had, but we're kind of stuck with the naming of List.concat, and wanting to be consistent with that

[Wrenna Robson]

Yeah I get you. I think Lean is Just Wrong on this but I agree and there's no sense bikeshedding about fixing that here.

[Alex Keizer]

Sure, I like the snoc name, too (although concat has grown on me), but if you're serious about that, petition core to change List.concat first. ( don't think the name change there is worth the code churn, though

[Wrenna Robson]

I think being correct is always worth it, but this isn't the time or place I agree.

[Wrenna Robson]

For your interest by the way, I also had this equivalence.

def getBitResZero : Fin (2^(m + 1)) ≃ Bool × Fin (2^m) :=
 calc
  Fin (2^(m + 1)) ≃ Fin (2^m * 2) := finCongr (Nat.pow_succ 2 m)
  Fin (2^m * 2) ≃ Fin (2^m) × Fin 2 := finProdFinEquiv.symm
  Fin (2^m) × Fin 2 ≃ Fin 2 × Fin (2^m) := Equiv.prodComm ..
  _ ≃ _ := finTwoEquiv.prodCongr (Equiv.refl _)

This is equal to the above (not defeq) for i = 0, i.e. this actually probably is a thing you have in terms of actual bit operations etc.

[Alex Keizer]

Is i indexed least-significant-first, or most-significant?

[Wrenna Robson]

least significant (i = 0 is the odd/even bit)

[Wrenna Robson]

Simply because that is what made much more sense in my context. Clearly you could do it the other way.

[Alex Keizer]

Then we have it as (x.msb, x.truncate n), where x : BitVec (n+1) (EDIT: this is for the other endiannes)

[Wrenna Robson]

Hurrah!

[Eric Wieser]

Which end does truncate truncate? Shouldn't that be msb?

[Wrenna Robson]

Wait, truncate?

[Wrenna Robson]

Ah right yes, just for the i = 0 case.

[Alex Keizer]

Wait, no, we have it for msb with truncate

[Wrenna Robson]

I assume you have the i = Fin.last _ case also? Or - that is that I guess.

[Alex Keizer]

There might be some shifting in there too

[Eric Wieser]

As an aside, I find it very surprising that anyone wants to index bits by their msb

[Wrenna Robson]

Endianness is the cause of all the sins of the world, Eric.

[Eric Wieser]

Sure, but anyone writing C, verilog, or VHDL is indexing from the LSB (even if they view it as on the left instead of the right), so this msb API just feels like a trap to lead curious people astray.

[Wrenna Robson]

"This msb API" = is that what Bitvec currently does?

[Eric Wieser]

Bitvec builds everything in duplicate, once for msb and once for lsb

[Wrenna Robson]

Does it not define one in terms of the other?

[Wrenna Robson]

I think you want an msb API purely for people who are perverse I fear. But technically of course this isn't even an endianess thing - endianess is for bytestrings.

[Wrenna Robson]

Rather it's a bit order thing - and I do agree that for most contexts -- all I can think of - it's LSB-first.

[Wrenna Robson]

(As I say - if you are thinking about them as Fin n -> Bool, then this just represents a suitable conjugation through Fin.revPerm)

[Alex Keizer]

The definitions are usually not that bad to duplicate, it becomes annoying for theorems

[Alex Keizer]

(As I'm currently experiencing, trying to duplicate the equivalence for getMsb/ofBEFn)

[Wrenna Robson]

So I essentially think maybe you should just have the getLsb interface, and anywhere you have a theorem about getMsb i x, you replace it with a theorem about getLsb (Fin.rev i) x. But I am Fin-API-pilled.

[Alex Keizer]

Well, we already have a theorem that getMsb' i x = getLsb i.rev x, so that's essentially what we're doing

[Wrenna Robson]

(Indeed, I think you should probably define getMsb i x as getLsb (Fin.rev i) x. I think you currently do it by manually subtracting? I think this is probably a Bad Plan.)

[Wrenna Robson]

Fin is so much easier to work with as an index set if you avoid doing arithmetic in it as much as possible...

[Alex Keizer]

Currently there is getLsb/getMsb in Std which index with naturals, then there are getLsb'/getMsb' in mathlib which index with Fin's, but just by wrapping the Nat-indexing functions and Fin.val

[Wrenna Robson]

Cursed. I mean I see why you've presumably done that but D:

[Wrenna Robson]

That means in fact getMsb is defined with tsub. Abandon hope, all, ye are doomed.

[Wrenna Robson]

Not that I mean to be overdramatic. But I can feel the spectre of Lemma Hell here.

[Alex Keizer]

There is https://github.com/leanprover/std4/pull/400, but the reaction there was luke-warm. Maybe you can try to convince Joe Hendrix to re-consider

[Wrenna Robson]

I would be enthusiastic about it I think.

[Alex Keizer]

Wrenna Robson said:

Not that I mean to be overdramatic. But I can feel the spectre of Lemma Hell here.

To be fair, in proofs I just don't unfold getMsb' and instead use the aforementioned getMsb' i x = getLsb i.rev x equality, so it's not that bad, so far

[Wrenna Robson]

Incidentally, as an example of the kind of nonsense (but useful nonsense) you can prove with my getBitRes, I have this theorem as essentially a straightforward consequence of the definitions.

getBit (j.succAbove i) q = getBit i (getRes j q)

getBit and getRes are the two components of getBitRes. So this says that "If you take all bits except the jth bit of q, and then take the ith bit, that is the same as taking the j.succAbove ith bit of q, which essentially like saying "the ith bit of q, once you have j back in, but ignored".

[Wrenna Robson]

But with the wrong definitions, proving this sort of thing becomes extremely tiresome.

[Wrenna Robson]

Alex Keizer said:

Wrenna Robson said:

Not that I mean to be overdramatic. But I can feel the spectre of Lemma Hell here.

To be fair, in proofs I just don't unfold getMsb' and instead use the aforementioned getMsb' i x = getLsb i.rev x equality, so it's not that bad, so far

Indeed, but this might be an indication that this is a better definition.

[Wrenna Robson]

Oh, another definition that was handier to define using the equivalence:

abbrev bitInvar (i : Fin (m + 1)) (f : Fin (2^(m + 1)) → Fin (2^(m + 1))) : Prop :=
∀ b bp, bp.fst = b → ((getBitRes i).conj f bp).fst = b

[Wrenna Robson]

(For reference, after looking it up and finding my third comment of the form "this is the function append, which concatenates, I broke and decided to raise the conversation: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/List.2Econcat.20and.20List.2Eappend)

[Alex Keizer]

@Wrenna Robson what is the idiomatic way to reverse a tuple? Currently I'm using f ∘ Fin.rev, but I'm missing a result that says that reversing Fin.cons gives Fin.snoc, i.e., Fin.cons a f ∘ Fin.rev = Fin.snoc (f ∘ Fin.rev) a

[Alex Keizer]

It's not too hard to prove, I PR'ed it at #8814, just checking if I'm missing an easier way to do this

[Eric Wieser]

It might be shorter to prove that via List.ofFn

[Wrenna Robson]

Alex Keizer said:

Wrenna Robson what is the idiomatic way to reverse a tuple? Currently I'm using f ∘ Fin.rev, but I'm missing a result that says that reversing Fin.cons gives Fin.snoc, i.e., Fin.cons a f ∘ Fin.rev = Fin.snoc (f ∘ Fin.rev) a

Good question. The API here is a little weird.

Another option would be, for a f : Fin n -> a, ((Fin.revPerm).prodCongr (Equiv.refl _)) f.

Arguably, (Fin n)ᵒᵈ -> a would be a better type for "tuples indexed from the end".

[Wrenna Robson]

In this logic, you're then using Fin.revOrderIso to transport between the two...

[Wrenna Robson]

I'm sure our "order heads" could say that in a more sophisticated way.

[Eric Wieser]

Alex Keizer said:

Wrenna Robson what is the idiomatic way to reverse a tuple? Currently I'm using f ∘ Fin.rev

I think composition with rev is sensible

[Wrenna Robson]

Yes, I think so too, despite my digression. The above do boil down to that also - it's just a question of the best way of doing it.

[Alex Keizer]

The context is this definition, for which I think keeping it simple (i.e., sticking with rev) seems the best way:

/-- Create a bitvector from a function that maps index `i` to the `i`-th most significant bit -/
def ofBEFn {w} (f : Fin w → Bool) : BitVec w :=
  ofLEFn (f ∘ Fin.rev)

[Wrenna Robson]

Yep. Also it will not be hard to change if later you find a different definition would be more convenient.

[Wrenna Robson]

I generally find that if you are doing your homework as you go and splitting stuff neatly into logical lemmas, refactoring is straightforward. It's when you've got some titanic proof that uses about 8 different facts and the details of the implementation that things go wrong.

[Wrenna Robson]

@Alex Keizer for your reference:

getBitRes j q = (getLsb j q, (q % 2^j) + ((q >> (j + 1)) << j)
(getBitRes j).symm (b, p) = (p % 2^j) + ((q >> j) << (j + 1)) + bif b then 2^j else 0

I don't know if there's a simpler way to write this in the Bitvec form - the modulo operation is presumably some kind of truncation, for instance. This isn't how it is defined under the hood for me, but I think this is probably how you'd want to define it in the "closer to bit operation" form.

[Wrenna Robson]

So if you tell me "oh yeah we can definitely prove that these are inverse already" I'll be very excited

[Alex Keizer]

The modulus is indeed docs#Std.BitVec.truncate

[Wrenna Robson]

Though presumably you then need to zero-extend it back to length.

[Wrenna Robson]

Oho, but zeroextend and truncate are just the same thing in a hat ;)

[Alex Keizer]

We also have the shift notation on bitvectors (although that one truncates bits that are shifted out of the static width, so you might have to zero-extend first)

[Wrenna Robson]

The "+" here could equally be "^^", incidentally - I don't know which is more efficient.

[Wrenna Robson]

(Because as it happens you're only ever adding stuff to 0, you don't need to keep track of carries.)

[Alex Keizer]

And the bif b then 2^j else 0 can be stated in terms of docs#Std.BitVec.ofBool and docs#Std.BitVec.shiftLeftZeroExtend

[Alex Keizer]

Not sure about efficiency, but ^^^ might make proofs easier

[Alex Keizer]

Now as to whether we can prove these are isomorphisms, I'm not confident enough to say "definitely", but I'd encourage you to try

[Alex Keizer]

You might want to wait until some of my outstanding PRs are merged, though

[Wrenna Robson]

Would that I could, but that might have to be an after-thesis jobbie.

[Wrenna Robson]

In practice, when you are building a context time implementation, what you do is mask by ~(b - 1), because when b is 0 that is all-zeroes and when b is 1 that is all -ones).

[Wrenna Robson]

Because you want to avoid the branch.

[Wrenna Robson]

I don't know if that's really meaningfully modelable in Lean yet.

[Wrenna Robson]

Also morally it is somewhat evil to just casually treat (-1) as the all-ones vector, even though it is true (because you are using overflow properties which depending on your type and target language might be ambiguously defined/IMPDEF). Nevertheless it is the standard way I've seen.

[Wrenna Robson]

And I think it's true for you here!

[Alex Keizer]

Wrenna Robson said:

In practice, when you are building a context time implementation, what you do is mask by ~(b - 1), because when b is 0 that is all-zeroes and when b is 1 that is all -ones).

That would work if you're talking about 2^j - 1, but your previous code bit had 2^j in the true branch, so that is different, no? Hence my suggestion to model it as b.toNat <<< j, that would be 0 <<< j = 0 if b = false and 1 <<< j = 2^j if b = true.

[Wrenna Robson]

Well, hmm. Yes, it used 2^j*b, and for that I think you're quite correct. HOWEVER in practice what you have is two elements of an arbitrary array of a type (but we can cast it to a bitvector, like, it's morally a number of some size). The index for these two things are given by that calculation - but you don't need to hide this because you always load those two things. The secret information is whether you swap them or not.

So what you do is you XOR them together, and then XOR that by an all-1s or all-0s number (that you've made from b). Then you XOR each entry by your result and set it. This achieves conditional exchange without branching, do you see?

So you're absolutely right - but in context the things you want to mask are not the bitvecs but things you've loaded from an array using the bitvecs as indices.

[Wrenna Robson]

Does that make sense?