Add EndianNat for reasoning about representations in different bases and endianness

[zero-to-nat]

EndianNat provides utilities for reasoning about the per-digit representation of a non-negative number in a given base:

• to_nat and from_nat for converting to/from a natural number
• to_big and from_big for converting to/from a different base

These changes are part of the Rust standard library verification effort.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[elanortang]

Thanks for cleaning this up and proving the sanity-checks!

[parno]

Thanks for putting this together. I added various minor comments and suggestions.

[parno]

In theory we ought to be able to do these proofs in an endian-agnostic way, so that we don't have to duplicate the code like this. Might be more trouble than it's worth, unless an LLM can do it.

[elanortang]

What are times when we might care about whether we are calculating to_nat left-to-right or right-to-left? I remember that to_nat_right and to_nat_left were defined before defining the simpler to_nat, which uses least and drop_least to avoid messy definitions.

[parno]

Good question. An important use case I can imagine for this library is verifying a big-integer library, e.g., for computing RSA values. There you'll have functions that take in two BigIntegers x and y, and returns z, where you want to prove something like z.to_nat() == x.to_nat() + y.to_nat(). Your implementation is likely to be a loop over the elements of the BigInteger digits, so you'll want a loop invariant about the partial construction of the nat value. If we can do that from the cleaner least and drop_least, then we can omit the left-to-right and right-to-left definitions.

[zero-to-nat]

@elanortang @parno For to_nat_left and to_nat_right, these are not currently used anywhere in the rustlib project, so it would be fine for us to remove them. I kept the specs and proofs since they are related to to_nat and seemed like they could be useful.

To the question of whether least/drop_least is cleaner than first/drop_first: FWIW, I did rewrite the original to_big and from_big specs to use take_least/skip_least instead of take/skip because I found that it made the proofs simpler -- the arithmetic was the same for both little endian and big endian.

However, I could see how the first/drop_first approach would be more helpful if that aligned with how the implementation processed the data. With that in mind, I would be fine to either keep the spec or remove it.

[parno]

I think it's the case that to_nat is identical to to_nat_right for little endian, and to_nat_left for big endian, right? If so, then I think an implementation that wanted to use to_nat_right on a little endian machine, for example, would be able to just use to_nat. If that's the case, then perhaps we want to replace to_nat_right and to_nat_left with to_nat_msb, which would be the dual of to_nat. Then we'd only have two definitions for how to convert an EndianNat to a nat, and we should be able to eliminate the duplication of nat_left_eq_nat_right_little with nat_left_eq_nat_right_big