Carrying universes through to the SMT encoding

[nikswamy]

Background

In F* PR #2954, I mention work in progress to propagate universes to the SMT encoding.

In #2069, we note that WellFounded.axiom1 is incompatible with universe erasure in the SMT encoding.

In #3647, Gabriel points out that it one can directly exploit the erasure of universes in the SMT encoding to prove a contradiction.

This PR

So, in this PR, Gabriel revived an old incomplete branch where I started to add universes to the SMT encoding. I picked it up from there and propagated universes throughout the SMT encoding, getting things back to a point where the F* repo again verifies. This prevents the unsoundness in #3647.

Impact

The side-effect of this PR is that some proofs needed universe annotations, where previously they didn't. A common case is something like

let some_lemma () : Lemma (forall (a:Type u#a). p)

Previously, one could call some_lemma (), and F* would default the universe argument u#a to u#0, and since universes were erased anyway in the SMT encoding, this would suffice for a proof that required instantiating the quantifier for some type t say in Type u#1.

Now, in such cases, you have to explicit instantiate the universe at which you are invoking the lemma, i.e., some_lemma u#1 ()---since there is no way for F* to infer which universe to instantiate to in the caller's context.

Impact on other repos

I have branches of karamel, EverParse, and Pulse with this branch of F*, and with minimal changes to the code/proofs.
I also have a branch of HACL* mostly working with this branch of F*, but there are ~6 proofs with very large rlimits that no longer go through. I think the failure there is orthogonal to the addition of universes. But, restoring these brittle proofs is tough ... I will probably need some help on it from HACL* folks.

I plan to investigate the impact on other repositories as well, such as those in our check-world build. Though this is likely to take some time.

I think this branch is stable and worth trying out---it has worked already on substantial chunks of code without any unexpected changes.

But, until I have some more complete story for impact on other repos, this PR is a draft.