Add a new vector / bitvector library for the Rocq exporter

[sauclovian-g]

The existing one has numerous problems.

This one is much larger and more complete, and as an unexpected bonus, despite this it builds much, much faster, I guess because it doesn't use mathcomp.

On the minus side, it's not going to be compatible with old code, let alone old proofs; the internals are completely different and the arguments of the Vec type are now in the opposite order. (This is unfortunately necessary: it has to be Vec a n with the type first and then the length, because the type needs to be a parameter and the length needs to be an index, and therefore they must appear in that order.) The old library made Vec a Definition that reverses the order; we could conceivably bring that back but it's rarely a good idea to have noise like that.

[sauclovian-g]

This is likely to change a good deal still, and it hasn't been integrated at all yet, but the core of it's ready to be looked at.

[RyanGlScott]

Before I leave a more detailed review, I have some general questions:

• The definition of Vec itself, as far as I can tell, is identical to what Rocq offers in Stdlib.Vectors.VectorDef, but with different naming conventions. Is there a compelling reason to redefine all of these Stdlib operations rather than reusing what is already there?

• Relatedly, modern versions of Rocq will now warn if you try to use this particular encoding of length-indexed vectors---see the long warning text here. This warning text explicitly recommends using lists paired with proofs about their lengths, although stops short of actually providing an implementation of this in the standard library. (It points to mathcomp as one place where you can obtain an implementation, but for the reasons you note above, it is unclear whether depending on mathcomp is actually desirable.)

  I think it would be worth considering the use of this vector encoding as opposed to the traditional inductive style currently used in this PR. This is especially going to become relevant if we want to prove the remaining unproven lemmas, as I suspect that many of them will be far easier to prove over lists.

[brianhuffman]

In the discussion thread for #3202, we talked about how it would be better to map the SAWCore Nat type onto N instead of nat. How does this vector library fit in with that plan?

[sauclovian-g]

N is orthogonal (the current vector code uses nat but changing it won't be a big deal)

[sauclovian-g]

On the stdlib vectors... the goal was to create something independent.

Note that the warning specifically says that using the stdlib vectors is difficult. There are quite a few reasons for this that extend beyond the form of the Vec type. (For example, see https://github.com/rocq-prover/stdlib/blob/master/theories/Vectors/Fin.v, which is its own little horror.)

We could conceivably share the base type under the covers, but I don't think it's a great idea; it creates a bunch of complications and doesn't really buy much of anything.

Also, I've been thinking I should change the vectors to be snoc-based instead of cons-based. This doesn't matter much for the vectors themselves, but for bitvectors it's most natural to have the least significant bit be at the near end of the list; with cons-based vectors this puts bitvectors in backwards order left-to-right, which is confusing under the best of circumstances and worse when using vector tools like append on them.

On the broader topic of the choice of formulation: there are more issues involved than that comment acknowledges.

First, as long as we continue to encode the lengths of vectors in their types, as far as the library user is concerned all the accompanying headaches (e.g. the coercions) will still be present. In principle we could move away from this, and treat the lengths as premises to be carried around in proofs about the code instead. But I don't think that's really a good idea; it would require a near-complete rewrite of the exporter. Plus since Cryptol handles the lengths as type material it's probably better for the exported code to do so too. This means that we can't wish away the problem entirely as some of the comments elsewhere in the stdlib vectors seem to think one should.

Second, the best way to deal with large but finite objects is to figure out a way to construct them so that they're finite without that being a huge mess. Then they're just values. You can do this if all you really care about is normal-sized bitvectors (8, 16, 32, 64, etc.) which can all just be separate types, but it doesn't really work if you want the size to be a parameter. Or at least I haven't figured out a way to.

Absent that, there are two choices. You can carry around the size as an index type (as the stdlib vectors and this code do), or you can carry around an unbounded object and bundle a proof of the size with it. That's what the comment in the stdlib vectors code suggests, but the comment makes it sound like it has no downsides. That's not true. One cost is that once you have values containing proofs, you get to choose between not using = on them and jumping into setoid hell, incurring proof irrelevance, or deploying machinery based on decidable equality to avoid proof irrelevance. The other more substantial cost is that the proofs are negative instances and then you can't use these values in inductive types. We might get away with the latter for SAW, maybe, as long as we stick to cryptographic code. But in general, it's really not suitable for a bitvector library to use a type that can't be included in other types. (This is a recurring headache with the stdlib maps, and in general it will arise much more often with bitvectors.) I'd consider it a stopper, and that's why I chose the index type formulation.

[RyanGlScott]

Thanks for the feedback!

I have thoughts on basically every point you raise, so I'll respond to each point below. I do want to emphasize that I'm not trying to be nitpicky here, but rather to make sure that we've carefully thought through the tradeoffs involved in picking a vector representation. We don't get many opportunities to make huge backwards-incompatible changes like this one, so I want to make sure we feel good about the choice we'll make before breaking things!

---

On stdlib vectors:

We could conceivably share the base type under the covers, but I don't think it's a great idea; it creates a bunch of complications and doesn't really buy much of anything.

Can you elaborate more on this? In particular, I want to point out that this does buy us something: namely, that we can reuse a lot of the machinery that the stdlib already defines. For instance, we wouldn't need to redefine caseVec_S, as this PR does---we could instead use caseS from the stdlib.

Also, I've been thinking I should change the vectors to be snoc-based instead of cons-based. This doesn't matter much for the vectors themselves, but for bitvectors it's most natural to have the least significant bit be at the near end of the list

Perhaps I'm misunderstanding you, but isn't it already the case that the least significant bit is near the end of the list? for instance, saw-core-rocq currently translates 0b10 to Vector.cons _ True _ (Vector.cons _ False _ (Vector.nil _)), where False (the least significant bit) is at the end of the list.

---

On the formulation of the vector type:

In principle we could move away from this, and treat the lengths as premises to be carried around in proofs about the code instead. But I don't think that's really a good idea; it would require a near-complete rewrite of the exporter.

Can you elaborate more on this? I'm unclear why using lists paired with proofs about their lengths would be more work than the work you've put into this PR. In principle, it should be possible to give the functions in the saw-core-rocq support libraries the same type signatures as before, which means that the exporter would continue to work as before. (If there is an example of where this isn't the case, I'd be interested in hearing it.)

Plus since Cryptol handles the lengths as type material it's probably better for the exported code to do so too.

I'm not sure what you mean here, mainly because I'm not sure what "type material" means in a Rocq context. Since Rocq is dependently typed, the distinction between types and values isn't as clear as it is in Cryptol.

the best way to deal with large but finite objects is to figure out a way to construct them so that they're finite without that being a huge mess. Then they're just values. You can do this if all you really care about is normal-sized bitvectors (8, 16, 32, 64, etc.) which can all just be separate types, but it doesn't really work if you want the size to be a parameter. Or at least I haven't figured out a way to.

Again, I'm not sure what you mean here. It is certainly possible for the lists-paired-with-proofs approach to be parametric over the list size. I think I need to see an example of what sort of difficulty you'd anticipate.

One cost is that once you have values containing proofs, you get to choose between not using = on them and jumping into setoid hell, incurring proof irrelevance, or deploying machinery based on decidable equality to avoid proof irrelevance.

Of those choices, I would pick "deploying machinery based on decidable equality to avoid proof irrelevance". And having chosen that, I'm not sure I understand why this is counted as a downside. If anything, I would consider this an upside: if you need to prove that two vectors are equal, showing that the vectors' underlying proofs are equivalent becomes very simple due to decidable equality.

The other more substantial cost is that the proofs are negative instances and then you can't use these values in inductive types. We might get away with the latter for SAW, maybe, as long as we stick to cryptographic code. But in general, it's really not suitable for a bitvector library to use a type that can't be included in other types.

This is a subtle point, and I think it's one that helps to illustrate with an example. In particular, I believe you're alluding to the fact that if you have a definition like this:

Inductive value : Type :=
| Value (Vec 2 value)

Then Rocq will accept this definition if Vec is defined as a length-indexed vector, but Rocq will reject this definition if Vec is defined as a list paired with a proof about its length. The sticking point here is that a recursive use of value is also used as a Vec element type.

This is an interesting edge case to be sure, but I'm not sure I would elevate this to the level of "stopper". For starters, you can't write a recursive data type like this in either Cryptol or SAWCore, so this sort of code will never arise as a result of saw-core-rocq translation. Moreover, it's not really fair to say that you can't include Vec in other types---you could certainly include Vec 2 Bool (i.e., bitvector 2) as a field of value, for instance.

[sauclovian-g]

Thanks for the feedback!

I have thoughts on basically every point you raise, so I'll respond to each point below. I do want to emphasize that I'm not trying to be nitpicky here, but rather to make sure that we've carefully thought through the tradeoffs involved in picking a vector representation. We don't get many opportunities to make huge backwards-incompatible changes like this one, so I want to make sure we feel good about the choice we'll make before breaking things!

Right, sure.

That said, at this point redoing everything would be pretty expensive :-(

On stdlib vectors:

We could conceivably share the base type under the covers, but I don't think it's a great idea; it creates a bunch of complications and doesn't really buy much of anything.

Can you elaborate more on this? In particular, I want to point out that this does buy us something: namely, that we can reuse a lot of the machinery that the stdlib already defines. For instance, we wouldn't need to redefine caseVec_S, as this PR does---we could instead use caseS from the stdlib.

Well, at this point we already have it... plus we can only reuse things that don't involve Fin, which isn't that much, plus most of what's in there is undocumented. Plus they might remove the whole thing upstream at any time. I think the benefits of having a standalone implementation exceed the benefits of a small amount of logic sharing, especially under those circumstances and especially since none of it is likely to require much maintenance.

Also, I've been thinking I should change the vectors to be snoc-based instead of cons-based. This doesn't matter much for the vectors themselves, but for bitvectors it's most natural to have the least significant bit be at the near end of the list

Perhaps I'm misunderstanding you, but isn't it already the case that the least significant bit is near the end of the list? for instance, saw-core-rocq currently translates 0b10 to Vector.cons _ True _ (Vector.cons _ False _ (Vector.nil _)), where False (the least significant bit) is at the end of the list.

I thought I had preserved all the same ordering as the original implementation, but maybe I didn't. Anyway, my current implementation puts the LSB at the near end. Some of the pieces (e.g. the multiply and divide code) would be fairly gnarly the other way, and others (increment, add, etc.) would at least be messier. That suggests I may have to rearrange some things in the exporter to accommodate it, which I'll grant is unfortunate.

I suppose ideally we would want a library that's exactly the same as Cryptol's handling of vectors and bitvectors (complete with index 0 of a bitvector being the MSB, even though that's against everyone else's understanding of what "bit 0" means) ... but since Cryptol doesn't define vectors inductively and (AFAIK) doesn't natively have either cons or snoc, the exporter shouldn't care which end is the near end.

Also my first concern is making the Rocq output comprehensible because that's what people doing manual proofs need to look at.

Which I think means I should go ahead and switch to snoc.

On the formulation of the vector type:

In principle we could move away from this, and treat the lengths as premises to be carried around in proofs about the code instead. But I don't think that's really a good idea; it would require a near-complete rewrite of the exporter.

Can you elaborate more on this? I'm unclear why using lists paired with proofs about their lengths would be more work than the work you've put into this PR. In principle, it should be possible to give the functions in the saw-core-rocq support libraries the same type signatures as before, which means that the exporter would continue to work as before. (If there is an example of where this isn't the case, I'd be interested in hearing it.)

I'm talking about making the type Vec a (or just list a) and translating a function like my_add : [8] -> [8] -> [8] to something like

Definition my_add (a b: Vec bool) : Vec bool => add a b.
Lemma my_add_lengths: forall a b,
   length a = 8 -> length b = 8 -> length (my_add a b) = 8.

That is, not encoding the lengths in the types at all.

the best way to deal with large but finite objects is to figure out a way to construct them so that they're finite without that being a huge mess. Then they're just values. You can do this if all you really care about is normal-sized bitvectors (8, 16, 32, 64, etc.) which can all just be separate types, but it doesn't really work if you want the size to be a parameter. Or at least I haven't figured out a way to.

Again, I'm not sure what you mean here. It is certainly possible for the lists-paired-with-proofs approach to be parametric over the list size. I think I need to see an example of what sort of difficulty you'd anticipate.

I'm talking about approaches like the stdlib's char type, which is 8 bools, or the byte type, which is a single inductive with 256 cases. Both of those are annoying to work with; however, you can make a 32-bit bitvector out of four byte values. You can even make odd sizes. But if you want anything shaped like bitvector n, it becomes something like

Definition bitvector (n: nat) : Type :=
   match n with
   | 0 => unit
   | 1 => bool
   | 2 => bits2
   |   :
   | 8 => bits8
   | 9 => bits9
   |   :
   | 384 => bits384
   .

which you can probably imagine becomes impractical pretty quickly. Even if you can come up with a good definition of bits9 on which arithmetic isn't a horror.

One cost is that once you have values containing proofs, you get to choose between not using = on them and jumping into setoid hell, incurring proof irrelevance, or deploying machinery based on decidable equality to avoid proof irrelevance.

Of those choices, I would pick "deploying machinery based on decidable equality to avoid proof irrelevance". And having chosen that, I'm not sure I understand why this is counted as a downside. If anything, I would consider this an upside: if you need to prove that two vectors are equal, showing that the vectors' underlying proofs are equivalent becomes very simple due to decidable equality.

Yes, assuming you're familiar with those tools. It's still a bunch of goop you need that is deep into prover metatheory and confusing to casual users. In an adequately complete library, users shouldn't need to see it, same as with dealing with the related cases in the dependently-typed inductive. Is it actually any simpler, given adequate internal machinery? I'm not convinced.

(To be clear, I expected to have much more trouble with this code than I did. The only thing I couldn't get to go was atWithProof, and that's something I would have left out if it hadn't already existed. That said, there are a bunch of proofs that haven't been done yet, and I have had some annoying problems where certain lengths are convertible enough for the typechecker but not convertible enough for rewrite to match them, and then nothing works.)

Because we're still encoding the length in the type, it doesn't mean that we get to drop the explicit length coercions or the headaches they cause. So I don't think it makes any real difference for users of the library, which is who we need to be most concerned about.

The other more substantial cost is that the proofs are negative instances and then you can't use these values in inductive types. We might get away with the latter for SAW, maybe, as long as we stick to cryptographic code. But in general, it's really not suitable for a bitvector library to use a type that can't be included in other types.

This is a subtle point, and I think it's one that helps to illustrate with an example. In particular, I believe you're alluding to the fact that if you have a definition like this:

Inductive value : Type :=
| Value (Vec 2 value)

Then Rocq will accept this definition if Vec is defined as a length-indexed vector, but Rocq will reject this definition if Vec is defined as a list paired with a proof about its length. The sticking point here is that a recursive use of value is also used as a Vec element type.

Right.

This is an interesting edge case to be sure, but I'm not sure I would elevate this to the level of "stopper". For starters, you can't write a recursive data type like this in either Cryptol or SAWCore, so this sort of code will never arise as a result of saw-core-rocq translation.

You can't in Cryptol. I thought you could in SAWCore, but apparently not. (Nonetheless, there's been some talk about adding inductives to Cryptol and at some point if we want to be able to prove things about non-cryptographic code we'll need either that or some alternative.)

Moreover, it's not really fair to say that you can't include Vec in other types---you could certainly include Vec 2 Bool (i.e., bitvector 2) as a field of value, for instance.

True, that's not a negative usage of Value at all, and I overstated the problem.

[RyanGlScott]

That said, at this point redoing everything would be pretty expensive :-(

All the more reason to tread carefully here! I want to make sure that we won't regret our new design and want to redo it yet again some months (or years) later.

Well, at this point we already have it... plus we can only reuse things that don't involve Fin, which isn't that much, plus most of what's in there is undocumented. Plus they might remove the whole thing upstream at any time.

To be clear, I didn't have any of the Fin-related functions in mind when I wrote my comment. I was thinking of things like case0, caseS, splitat, etc. I will grant you that the Rocq stdlib's documentation is not the best, although that hasn't stopped us from using other parts of the stdlib.

However, you raise a good point about the future of the stdlib's VectorDef being unknown now that that whole module is deprecated. I think that is enough to (just barely) convince me that re-implementing it locally would be a better alternative.

Which I think means I should go ahead and switch to snoc.

If we do pick an length-indexed vector representation, then I don't have a very strong opinion about whether it should be done as a cons list or a snoc list. As you've noted, both choices make certain things easier to define and certain things harder to define. The only real constraint is that we should implement big-endian indexing, as Cryptol does this and being consistent with Cryptol would be the least surprising design. I don't have strong feelings about whether we pick a big-endian cons list or a big-endian snoc list, however.

I'm talking about making the type Vec a (or just list a) and translating a function like my_add : [8] -> [8] -> [8] to something like

Definition my_add (a b: Vec bool) : Vec bool => add a b.
Lemma my_add_lengths: forall a b,
   length a = 8 -> length b = 8 -> length (my_add a b) = 8.

That is, not encoding the lengths in the types at all.

I think I may have given the wrong impression with what I was proposing. I'm not proposing that we translate a SAWCore function argument of type (a : Vec 8 Bool) -> ... to multiple Rocq arguments with the types (a : Vec bool) -> length a = 8 -> .... Rather, I'm proposing that the Vec type be defined roughly as follows:

Record Vec (n : nat) (a : Type) : Type := MkVec
  { vlist : list a; veq : length vlist = n }.

And that we would translate SAWCore's Vec (8 : Nat) (a : sort 0) to Rocq's Vec (8 : nat) (a : Type), exactly as we currently do. This shouldn't require deep changes to the translator, just the saw-core-rocq support libraries.

I'm talking about approaches like the stdlib's char type, which is 8 bools, or the byte type, which is a single inductive with 256 cases. Both of those are annoying to work with; however, you can make a 32-bit bitvector out of four byte values. You can even make odd sizes. But if you want anything shaped like bitvector n, it becomes something like

Definition bitvector (n: nat) : Type :=
   match n with
   | 0 => unit
   | 1 => bool
   | 2 => bits2
   |   :
   | 8 => bits8
   | 9 => bits9
   |   :
   | 384 => bits384
   .

which you can probably imagine becomes impractical pretty quickly. Even if you can come up with a good definition of bits9 on which arithmetic isn't a horror.

I appreciate you providing an example here, but I'm afraid I'm even more confused than I was before. Are you proposing an illustrating a hypothetical encoding of Vec that isn't inductive? I'm not sure what point is being made here.

Yes, assuming you're familiar with those tools. It's still a bunch of goop you need that is deep into prover metatheory and confusing to casual users. In an adequately complete library, users shouldn't need to see it, same as with dealing with the related cases in the dependently-typed inductive. Is it actually any simpler, given adequate internal machinery? I'm not convinced.

I would like to challenge the idea that you need to be an expert in Rocq metatheory in order to use the list-bundled-with-a-proof encoding. We can easily offer combinators for users that hide the lower-level details of decidable equality, just like how we would offer combinators that hide the lower-level details of performing dependent pattern matching on length-indexed vectors. For instance, one of the more useful combinators for working over lists-bundled-with-proofs is:

Theorem Vec_f_equal :
  forall (n : nat) (a : Type) (l1 l2 : list a)
         (eq1 : length l1 = n) (eq2 : length l2 = n),
         l1 = l2 ->
         MkVec l1 eq1 = MkVec l2 eq2.
Proof.
intros.
subst.
f_equal.
apply (UIP_dec Nat.eq_dec).
Qed.

With this, most equality proofs over Vecs become a simple matter of (1) destructing values of type Vec, (2) applying Vec_f_equal, and (3) writing a proof that the underlying lists are the same. That's it! Vec_f_equal hides the low-level details of using decidable equality.

(To be clear, I expected to have much more trouble with this code than I did. The only thing I couldn't get to go was atWithProof, and that's something I would have left out if it hadn't already existed. That said, there are a bunch of proofs that haven't been done yet, and I have had some annoying problems where certain lengths are convertible enough for the typechecker but not convertible enough for rewrite to match them, and then nothing works.)

One advantage of the lists-bundled-with-proofs encoding is that the stdlib already offers a nth_error function that pretty much does what atWithProof does when used in conjunction with the nth_error_Some lemma. That is, a lot of these tricky definitions degrade to writing definitions over simply typed lists, which (I find) is much nicer than doing the same with dependently-typed lists and dependent pattern matching.

Because we're still encoding the length in the type, it doesn't mean that we get to drop the explicit length coercions or the headaches they cause. So I don't think it makes any real difference for users of the library, which is who we need to be most concerned about.

I agree that explicit length coercions are still required, but I would challenge the idea that they're as much of a headache as they are in the dependently-typed vector setting. One of the nice properties of the lists-bundled-with-proofs encoding is that the representation (list) is decoupled from the n type, which makes dealing with length coercions a lot easier. As a case study, let's consider the append_append_l lemma that you prove in this PR:

Lemma append_append_l: forall a n m l
     (xs: Vec a n) (ys: Vec a m) (zs: Vec a l) pf,
   append (append xs ys) zs =
      coerceVec (n + m + l) pf (append xs (append ys zs)).
Proof.
   intros.
   revert pf.
   revert zs ys.
   revert m l.
   induction xs; intros; simpl.
   - rewrite coerceVec_vacuous. auto.
   - assert (n + m + l = n + (m + l)) as HN1 by lia.
     rewrite IHxs with (pf := HN1).
     rewrite ConsVec_coerceVec.
     apply coerceVec_irr.
Qed.

I'd argue (and hopefully you'll agree) that this proof is somewhat tedious, as it requires appealing to three separate helper lemmas (coerceVec_vacuous, ConsVec_coerceVec, and coerceVec_irr) in order to complete the proof. Doable, but tedious.

Let's compare how this proof would work in a lists-bundled-with-proofs setting. We need only establish one lemma about how coerceVec interacts with MkVec:

Theorem pushCoerceVec :
  forall (m n : nat) (a : Type) (pf : m = n) (v : Vec m a),
  coerceVec _ _ _ pf v = MkVec (vlist v) (eq_trans (veq v) pf).
Proof.
intros.
subst.
now destruct v.
Qed.

With this, proving append_append_l becomes very straightforward:

Theorem append_append_l :
  forall (m n p : nat) (a : Type) (vm : Vec m a) (vn : Vec n a) (vp : Vec p a),
  append vm (append vn vp) =
  coerceVec _ _ _ (eq_sym (Nat.add_assoc m n p)) (append (append vm vn) vp).
Proof.
intros.
destruct vm, vn, vp.
rewrite pushCoerceVec.
simpl.
apply Vec_f_equal.
apply List.app_assoc.
Qed.

All of the heavy lifting is done in the final apply List.app_assoc step, which establishes the associativity of list appending (++). This, I argue, is how it should be. The Rocq standard library goes through a lot of effort in defining lemmas over lists, so we might as well reuse them!

To put this another way: Lean also picks the lists-bundled-with-proofs encoding in its own vector definition. I think it would be worth following suit.

[sauclovian-g]

That said, at this point redoing everything would be pretty expensive :-(

All the more reason to tread carefully here! I want to make sure that we won't regret our new design and want to redo it yet again some months (or years) later.

Fair enough.

Well, at this point we already have it... plus we can only reuse things that don't involve Fin, which isn't that much, plus most of what's in there is undocumented. Plus they might remove the whole thing upstream at any time.

To be clear, I didn't have any of the Fin-related functions in mind when I wrote my comment.

Well, right, you're not crazy :-)

However, you raise a good point about the future of the stdlib's VectorDef being unknown now that that whole module is deprecated. I think that is enough to (just barely) convince me that re-implementing it locally would be a better alternative.

ok then.

Which I think means I should go ahead and switch to snoc.

If we do pick an length-indexed vector representation, then I don't have a very strong opinion about whether it should be done as a cons list or a snoc list. As you've noted, both choices make certain things easier to define and certain things harder to define. The only real constraint is that we should implement big-endian indexing, as Cryptol does this and being consistent with Cryptol would be the least surprising design. I don't have strong feelings about whether we pick a big-endian cons list or a big-endian snoc list, however.

Well, it has indexing from both ends and we'll need that one way or another.

The divider is what convinced me it really ought to be LSB on the near end of the list. It could be written inside-out, but it would be a lot uglier. (The multiplier too, except currently it is incorrect and therefore is not an existence proof of anything substantive.)

That is, not encoding the lengths in the types at all.

I think I may have given the wrong impression with what I was proposing.

No, I think I must have been unclear that I was trying to comment on the entire space of design choices.

I'm proposing that the Vec type be defined roughly as follows:

Record Vec (n : nat) (a : Type) : Type := MkVec
  { vlist : list a; veq : length vlist = n }.

You don't want to use the record syntax unless you need to.

Inductive Vec (n: nat) (a: Type) : Type :=
| MkVec (xs: list a) (pf: length xs = n): Vec n a.

On the plus side, because it's not recursive, n can be a parameter, so we can keep the current argument order and we don't have to make that breaking change.

Given that I need a custom proof term (and therefore a lemma to keep it short) just to define ConsVec I worry there's going to be a lot more explicit proof terms in this formulation.

Also, while in the dependently typed case all the proofs contain only nats, here we also have lists floating about. The advantage of proofs that are entirely about nats and not lists is that we have both lia and a large library of preexisting lemmas to retire those proofs and there are often preexisting short (single-application) proof terms to be had.

(Plus anywhere we have equality of lists we lose UIP in the general case...)

I would like to challenge the idea that you need to be an expert in Rocq metatheory in order to use the list-bundled-with-a-proof encoding. We can easily offer combinators for users that hide the lower-level details of decidable equality, just like how we would offer combinators that hide the lower-level details of performing dependent pattern matching on length-indexed vectors.

Well, sure. For an adequately complete library, these concerns aren't user-facing, and users shouldn't be writing proofs about the library internals. I already said that.

For instance, one of the more useful combinators for working over lists-bundled-with-proofs is:

Theorem Vec_f_equal :
  forall (n : nat) (a : Type) (l1 l2 : list a)
         (eq1 : length l1 = n) (eq2 : length l2 = n),
         l1 = l2 ->
         MkVec l1 eq1 = MkVec l2 eq2.
Proof.
intros.
subst.
f_equal.
apply (UIP_dec Nat.eq_dec).
Qed.

With this, most equality proofs over Vecs become a simple matter of (1) destructing values of type Vec, (2) applying Vec_f_equal, and (3) writing a proof that the underlying lists are the same. That's it! Vec_f_equal hides the low-level details of using decidable equality.

Well, apart from when you have e.g. one list of length S n and the other of length n + 1, when you're back to coerceVec.

We need only establish one lemma about how coerceVec interacts with MkVec:

Theorem pushCoerceVec :
  forall (m n : nat) (a : Type) (pf : m = n) (v : Vec m a),
  coerceVec _ _ _ pf v = MkVec (vlist v) (eq_trans (veq v) pf).
Proof.
intros.
subst.
now destruct v.
Qed.

I admit that this part is appealing. I am near to persuaded, but as I noted above, tinkering a bit with this formulation suggests that even if eliminating coercions is easier, it's going to have a much higher length proof overhead. And it's fairly easy to write an ltac that eliminates coercions using all the available tools, so the fact that they do end up being user-facing isn't actually that compelling an argument.

Also we lose the advantage of dropping down to lists if we want snoc, and I think we do. That way bitvectors will display something like comprehensibly and the behavior of append doesn't require lengthy explanation every time.

(I also don't think that proving append_append_l in the absence of length-induced headaches is heavy lifting or complicated enough to spend more than about thirty seconds on...)

One advantage of the lists-bundled-with-proofs encoding is that the stdlib already offers a nth_error function that pretty much does what atWithProof does when used in conjunction with the nth_error_Some lemma. That is, a lot of these tricky definitions degrade to writing definitions over simply typed lists, which (I find) is much nicer than doing the same with dependently-typed lists and dependent pattern matching.

Erm, I think you mean atOption.

To put this another way: Lean also picks the lists-bundled-with-proofs encoding in its own vector definition. I think it would be worth following suit.

Lean's metatheory and dependent typing formulation is all different so I don't think that really means much.

Meanwhile, I had an idea:

Inductive Vec (a: Type): nat -> Type :=
| MkVec (xs: list a) : Vec a (length xs).

It was not a good idea.

[RyanGlScott]

@sauclovian-g and I discussed this synchronously. The short version is that I'm now aligned with the length-indexed vector approach used in this PR. To summarize some of the key points from the longer discussion we had:

• There (sadly) isn't a third-party bitvector library in the wild that is high-equality enough for our needs, and we both agree that creating our own would be wise. (We can include this library locally in saw-core-rocq for now, but in the future, we may want to consider releasing this more widely.)

• @sauclovian-g is pretty firmly in favor of using snoc lists, as it makes defining bitvector division much more straightforward than if one were to use cons lists. I don't have any particular objections to this. (We note that Rocq's standard library does not offer a snoc list type, which is unfortunate.)

  If we use snoc lists, then a lot of my arguments for using lists-bundled-with-proofs are now moot, as we no longer have access to a large catalog of already-proven lemmas about lists. The only real advantage would be that you could prove things about simply typed snoc lists as opposed to dependently typed ones, but my hope is that the saw-core-rocq support libraries would offer most of the proofs where you need to resort to dependent pattern matching.

• Regardless of whether one uses length-indexed vectors or lists-bundled-with-length-proofs, there are certain definitions that will require helper lemmas involving nats. With length-indexed vectors, these lemmas involve "raw" nats (e.g., showing that m + S n equals S (m + n)), but with lists-bundled-with-length-proofs, these lemmas involve applications of the length function (e.g., showing that length (m ++ n) equals length m ++ length n). Rocq's standard library has a lot more of the former type of lemma than the latter type of lemma, which is one slight argument in favor of length-indexed vectors.

  As an aside, if we do use lemmas from the standard library in definitions that are expected to reduce (e.g., take), we should make sure that we use proofs in a computable way. This blog post offers one technique for doing so, taking advantage of the fact that nats have decidable equality.

• An argument in favor of not using lists-bundled-with-length-proofs is that is is easy to accidentally vector terms whose definitions are unreasonably large. For instance, here is one possible way to define Cons in this setting:

  Definition Cons {a : Type} (x : a) {n : nat} (vs : Vec n a) : Vec (S n) a.
  destruct vs as [xs eq].
  apply (MkVec (cons x xs)).
  cbn.
  f_equal.
  exact eq.
  Defined.
  

  When defined using Proof mode as above, this definition doesn't look so bad. If you unfold the definition of Cons, however, the resulting term is surprisingly large:

  Cons =
  fun (a : Type) (x : a) (n : nat) (vs : Vec n a) =>
  match vs with
  | {| vlist := vlist; veq := veq |} =>
      (fun (xs : list a) (eq0 : length xs = n) =>
       {|
         vlist := x :: xs;
         veq :=
           (let H : length xs = n := eq0 in
            (fun H0 : length xs = n =>
             eq_trans
               (f_equal
                  (fun f : nat -> nat => f (length xs))
                  eq_refl)
               (f_equal S H0))
              H)
           :
           length (x :: xs) = S n
       |}) vlist veq
  end
  

  This matters because users who write proofs may need to unfold Cons, and this can result in walls of text in your proof state. It's possible to lessen the impact by encapsulating this large proof term into its own definition, but the fact remains that you will likely have these terms floating around in end users' proof states.

• One sticking point in this PR is that Vec is redefined such that the order of parameters is Vec a n, with the n appearing second rather than first. @sauclovian-g argues that this order is more natural, and I don't disagree. That being said, Vec a n the opposite convention of what SAWCore uses (Vec n a), and unless we either change the SAWCore Vec type or change the saw-core-rocq translator to account for this difference, that is going to pose issues when trying to integrate Vec a n into the overall workflow.

  @sauclovian-g envisions a future in which the saw-core-rocq translator more aggressively normalizes generated terms to look more like idiomatic Rocq code. We already do this to some extent: SAWCore's Bool and Nat are translated to Rocq's bool and nat, for instance, and we could envision translating SAWCore's Vec n a to Vec a n. The latter transformation would be trickier due to the fact that SAWCore can (in theory) allow partial applications of Vec, so we might need to translate something like let { f = Vec n; } in f a in SAWCore to let f := fun a => Vec a n in f a in Rocq. In principle, such transformations could be done on the saw-core-rocq AST, but I doubt that the machinery for doing so exists.

  My personal preference would be to first integrate this new bitvector library in a way that is minimally disruptive to the current saw-core-rocq translator, which may require adding "wrapper" definitions like Definition Vec n a := RealVec a n for now to accommodate what the translator expects. We can then revisit the question of normalizing generated Rocq code afterwards.