Use tighter loose bounds

[JasonGross]

We now compute the loose bounds to be as tight as possible given the
tight bounds: they are the tightest bounds that will let us add two
tightly-bounded field elements, and will also let us subtract two
tightly-bounded field elements (with balance), without needing to carry.

This is probably required for having 32-bit p448 work, but even with
this, p448 is still not working; see
#797. Seems worth merging
anyway.

@andres-erbsen @davidben please review either the changes in the bounds in the comments, or the changes in the definition of loose_upperbounds in src/UnsaturatedSolinasHeuristics.v, or both.

@jadephilipoom Please review my changes to your proof of loose_bounds_within_base_access_sizes in src/Bedrock/Tests/Proofs/X25519_64.v (the upper bounds are no longer repeat r n, so I had to use a lemma about relaxing them, and then relaxed them to the repetition of the max element).

[davidben]

I transcribed the new curve25519 bounds into the asserts in our code and the tests still passed. I probably am not able to provide useful review beyond that. :-)

[jadephilipoom]

The changes to Tests/ aren't too important because I've now completely deleted Tests/ in my branch (bedrock2_interface) and replaced it with a new thing. It might be a new form of headache now (but hopefully not, I think it's actually just left as computation of is_tighter_than_bool), but I'll consider that my problem.

[hannesm]

I came here while reading #797 which I'm interested in. I understand this does not bring fiat-crypto to p448-32, but already goes some way. I was wondering (since this has multiple positive reviews) what is missing to get this PR merged (apart from a rebase)?

[JasonGross]

My impression from #797 (comment) was that determining headroom is more complicated than just "how many additions / subtractions do you want to be able to do in a row without carrying?" and hence the one-line change here (changing headroom_add_count from 2 to 1) does not actually make progress conceptually towards handling p448-32. I did in fact merge the earlier underlying changes, i.e., factoring the computation in a way that lets us just declare how many times we want to be able to add in a row and bounds for that.

I think the thing standing in the way of merging a PR like this is having an understanding of what the right interface to present here is. Should we compute the loose bounds by asking people to specify how many additions they'd like to perform in a row (and encode it somehow in the types so that users can in fact perform that many additions in a row)? It's not clear to me what the landscape looks like around choosing bounds.

If it's useful to you, I'm happy to make headroom_add_count an argument to the binary, but again I think this is the wrong strategy in the absence of a vision about what should be tunable parameters of the implementation, and what should be computed automagically and how. Perhaps @bitwiseshiftleft or @kevaundray has thoughts on what a global plan for this should look like.

[hannesm]

Thanks for your explanation @JasonGross. Indeed that sounds like this PR may not be relevant for the p448-32 goal. I'll read up on #797 to figure out the missing bits and pieces when I find enough time and headroom.