This may seem like a large PR, but it's actually implementing something fairly focused.

The problem: Top-level nullary constants lead to SMT context pollution

Given a top-level nullary constant, say,

let n : u32 = 0ul

F* would encode this to SMT as (roughly)

(declare-fun n () Term)
(assert (HasType n u32))
(assert (n = U32.uint_to_to 0))

i.e., ground facts about the n's typing and definition would be introduced into the top-level SMT context.

Now, for a subsequent proof that has nothing to do with n, these facts are still available in the context leading to clutter. E.g., in this case, the HasType n u32 leads to Z3 deriving facts like about 0 <= n < pow2 32, then potentially unfolding the pow2 32 recursive functions ... etc. all for potentially no good reason.

The fix: Protect assumptions about nullary constants under a dummy quantifier

The change in this PR is to avoid introducing these ground facts into the SMT context by default. Instead, we now thunk these nullary constants, adding a dummy argument, like so:

(declare-fun n (Dummy_sort) Term)
(assert (forall ((x Dummy_sort) (! (HasType (n x) u32) :pattern ((n x)))))
(assert (forall ((x Dummy_sort) (! (= (n x) (U32.uint_to_t 0)) :pattern ((n x)))))

Now, instead of ground facts, we have quantified formulae that are triggered on occurrences of n x.

Every occurrence of n in the rest of the proof is forced to (n Dummy_value): so, only when such an occurrence is present, do facts about n become available, not polluting the context otherwise.

For some proofs in large contexts, this leads to massive SMT performance gains: e.g., in miTLS with LowParse in context, some queries in HSL.Common are sped up by 20x; Negotiation.fst has an end-to-end speed up (full verification time) by 8-9x. etc. So, this can be a big win.

An implementation detail

Note, this thunking happens at a very low-level in the SMT encoding. Basically, the thunks are forced at the very last minute just before terms are printed to SMT. This is important since it ensures that things like sharing of SMT terms are not destroyed by discrepancies in thunking behavior (and earlier attempt did thunking at a higher level in the encoding, but this led to many regressions).

Some downsides: Interaction with triggering behavior

OTOH, the missing ground facts about n can also cause some proofs to break. A typical situation (see LowStar.Monotonic.Buffer.fst; SL.Heap.fst etc.) has to do with the use in SMT patterns. Continuing the example above, say we have the following program in scope

let n : u32 = 0ul
val pred : u32 -> int -> prop
val lem: x:int -> Lemma (pred n x) [SMTPat (pred n x)]
let test (x:int) = assert (pred 0ul x)

Previously, this program would verify as written, because the assert (pred 0ul x) would occur in a context of the ground equality n = 0ul which would then allow pred 0ul x to trigger lem and the proof is done.

Now, however, the ground equality n=0ul is not present and lem is not triggered by pred 0ul x.

There are many ways out of this situation. E.g, assert (pred n x), or assert (n = 0ul); assert (pred 0ul x) etc.

I also introduced a triggering construct, FStar.Pervasives.intro_ambient, which can be used to explicitly trigger quantified formulae about nullary constants and bring them into scope ambiently. So, a third way out of this situation is

let n : u32 = 0ul
let _ = intro_ambient n //makes ground facts about n available ambiently to SMT
val pred : u32 -> int -> prop
val lem: x:int -> Lemma (pred n x) [SMTPat (pred n x)]
let test (x:int) = assert (pred 0ul x)

You can see this pattern used in LowStar.Monotonic.Buffer.fst, SL.Heap.fst, ... etc.

Some other proofs broke because they were just flaky (e.g., proofs in FStar.UInt128, Math.Lemmas, etc.) and I had to adjust them.

A transition path to this new behavior

There is a new boolean command line flag --protect_top_level_axioms [true|false], whose default value is currently false.

The flag is temporary, and will be removed shortly ... yes, I really mean this!

When the flag is set to true you get the new behavior described above.

When the flag is set to false, in addition to the SMT encoding described above, for every nullary constant that is introduce, the SMT encoding implicitly also adds an intro_ambient axiom, to bring facts about the nullary constant into scope.

There are a handful of programs in the Everest tree that currently require this flag to be set to false:

hacl-star/code/old/poly1305/Hacl.Spec.Bignum.Modulo.fst
hacl-star/code/old/bignum/Hacl.Spec.Bignum.Fmul.fst
hacl-star/code/old/poly1305/Hacl.Spec.Bignum.AddAndMultiply.fst
hacl-star/code/old/poly1305/Hacl.Spec.Poly1305_64.fst
hacl-star/providers/evercrypt/fst/EverCrypt.HMAC.fst
hacl-star/providers/evercrypt/fst/EverCrypt.Hash.Incremental.fst
TLSInfo.fst

So far, since the flag is still set to default false, except for the F* build where this is enabled explicitly in fstar.mk, I have an Everest green.

I plan to explicitly turn the flag to true by default, and explicitly set the flag to false for these 7 programs above.

Then, I hope, we can just restore these 7 files and do away with the flag altogether.

Miscellany

To get a full picture of the Everest build, this PR also allows turning errors 9, 16, 19 (SMT verification errors) into warnings (using --warn_error)