Code pattern for hiding definitions from Z3 and selectively revealing them

Quick version: Selectively revealing definitions to the SMT solver

Sometimes, you don't want the SMT solver to see a definition globally. You might prefer to expose the definition only within a certain scope. The way to do this is like so:

[@"opaque_to_smt"]
let incr (x:nat) = x + 1

(* This fails because the SMT solver cannot see the definition of `incr` *)
[@@(expect_failure [19])]
let test = assert (incr 0 == 1)

(* But, if you call `FStar.Pervasives.reveal_opaque` like shown below, 
   the definition of `incr` is available in the rest of the scope and 
   the proof goes through. *)
let test2 =
   reveal_opaque (`%incr) incr;
   assert (incr 0 = 1)

Main target audience: HACL* and Vale specs

HACL* and Vale specs are written as Tot functions that operate on pure data structures e.g. FStar.Seq. The implementation of these specs are stateful functions that operate on LowStar.Buffer and provide a postcondition that the buffer contents are consistent with the corresponding Tot spec functions.

Currently the implementation file simply opens the spec file and then all the spec definitions are in the Z3 context for the complete implementation module (sometimes the spec files are friended, but that's irrelevant here).

This situation is much less than ideal:

• Most of the times, there is one-to-one correspondence between the spec functions and the implementation functions, and once implementation of a spec functions is there, the spec function is not needed for the rest of the module. But currently these spec functions remain in the Z3 context.

• We have noticed in some Z3 profiles for Hacl.Impl.Core.MD5 that these spec functions fire a lot in Z3.

• As a result, the implementations currently play various tricks (--using_facts_from, higher z3rlimit, split code into smaller functions, etc.) to get the proofs going.

This page lists some code patterns that can be used to optimize this situation. The goal is to keep the spec functions hidden from Z3 by-default, and reveal them selectively only when needed, e.g. in the corresponding implementations.

The patterns below have been tested on MD5 specs and implementation in HACL*. It simplified the proofs a lot by not needing --using_facts_from, higher z3rlimits, or smaller unnecessary functions.

Design pattern

There are two things we need to do: (a) we need to hide the definitions from Z3, and (b) we need to selectively reveal them to Z3.

For hiding definitions, we can use the [@"opaque_to_smt"] attribute. For example, say module A is the spec module that defines a function incr:

let incr (x:nat) :nat = x + 1

To hide this definition from Z3, we can slap the [@"opaque_to_smt"] attribute on it:

[@"opaque_to_smt"]
let incr (x:nat) :nat = x + 1

Now suppose a module B wants to prove some fact about A.incr; by default, the following fails:

open A

let test () = assert (incr 1 == 2)

since Z3 does not know the definition of A.incr.

To reveal the definition, we can use a library function reveal as follows, and then the assert in B succeeds:

let test () =
  reveal [delta_only [`%A.incr]] A.incr;
  assert (incr 1 == 2)

The reveal function essentially normalizes the definition of A.incr (by unfolding it) and passes it to Z3.

There are a few drawbacks of this pattern to hide the definitions:

• This pattern could be brittle if the implementation needs to reveal a single spec multiple times and prove all those instances to be equal. Essentially, this pattern reveals the incr function as a lambda abstraction to Z3 and so, when revealed multiple times, F* will encode the (same) lambda abstraction multiple times. If lucky, the hash consing in F* will figure that these lambdas are the same, and encode them once. Otherwise it will encode different lambda abstraction every time and then we will be out of luck trying to prove them equal.

• If the spec function is a let rec then also this pattern may not work well (since F*'s smt encoding of inner let rec is not precise).

Hiding via an indirection

To get around the drawbacks of the previous approach, we can introduce an indirection for each spec function:

let incr_defn (x:nat) :nat = x + 1

[@"opaque_to_smt"]
let incr = incr_defn

The key idea is that the main spec function incr is opaque to Z3, however it is defined in terms of an auxiliary incr_defn which is encoded as usual to Z3. Z3 does not have any opportunity, by default, to fire the incr_defn, since none of the functions in the implementation or rest of the spec refer to it directly -- they only refer to incr, and incr is hidden from Z3.

And then when we reveal the incr function in the client as before:

let test () =
  reveal [delta_only [`%A.incr]] A.incr;
  assert (incr 1 == 2)

Z3 gets to know incr == incr_defn, and it can then use the definition of incr_defn but only locally in the test function.

This pattern gets around the drawbacks of the previous approach at the cost of an indirection.

Using meta-programming to reveal

If you are troubled by the verbosity or duplication in

reveal [delta_only [`%A.incr]] A.incr

We can avoid it using meta-programming. But that means you end up bringing the whole meta-programming framework (along with sequences etc.) in your context.

For example, we can provide a reveal tactic which can be used as:

assert (incr == incr_defn) by (reveal incr)

Using meta-programming even for specs

Santiago suggests that we can use meta-programming even for specs. For example, we can write a tactic hide_defn that elaborates the following spec code:

let incr_defn (x:nat) : nat = x + 1
%splice[] (hide_defn "incr_defn")

to

[@"opaque_to_smt"]
let incr = incr_defn

let reveal_incr: unit -> Lemma (incr == incr_defn) = 
  reveal [delta_only [`%A.incr]] A.incr

So that the clients can now simply call reveal_incr ():

let test () =
  reveal_incr ();
  assert (incr 1 == 2)

It makes it easier for the clients (less verbose) at the cost of even the specs depending on the tactics.