Protect top-level nullary axioms

[nikswamy]

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)

[nikswamy]

I realize that this PR is probably very hard to review.

I will highlight some specific bits that could be interesting

[nikswamy]

This flag is flipped on to true for the F* build

[nikswamy]

Note, I am setting a 10 minute hard timeout on individual Z3 queries. WIthout it, I find that Z3 can run forever on the CI machine and we get no feedback about a build. But, we could revert this ...

[nikswamy]

Removed a double inclusion of fstar.mk z3.mk (also included in Makefile.verify etc.)

Should probably just delete these lines

[nikswamy]

This whole region of code is the main part of the new functionality. Probably worth a review here @aseemr or @mtzguido

[mtzguido]

Looks good to me! Nitpicking: I would thunk should_thunk :).

Also the explanation on this PR is really useful. Maybe we could put it within the file too as a "note", in the style of GHC (https://ghc.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Commentsinthesourcecode). But this is good to merge as-is IMO.

[nikswamy]

@aseemr @tahina-pro ... FYI

[nikswamy]

FYI @aseemr @mtzguido

[msprotz]

This is an excellent improvement, and thanks for running regressions at the Everest level!

The files in HACL*'s code/old directory do not need to be preserved and are slated to be replaced in the near future by new algorithms from Karthik. So, no need to spend any precious cycles there, assume or admit smt queries is fine.

Seeing the benefits of this patch, I would actually advocate for the flag to be turned on by default directly, leaving only three files to set the flag to false right now.

EverCrypt.Hash.Incremental and EverCrypt.HMAC are files that a lot of us (@fournet, @aseemr, @tahina-pro, myself) have spent significant time on, to keep them under verification. In particular, EverCrypt.Hash.Incremental is the file that Aseem and I looked at, and for which I could never understand proof fragility (the infamous 15s-on-Linux, 80 minutes-on-OSX proof). As we later try to restore these files to no longer rely on the flag, perhaps this would be a good motivation to screen-share and try to diagnose what's going at the SMT level rather than try to power through the proof and call modifies lemmas by hand (as was the case before)?

Thanks,

Jonathan