arXiv:1803.06547v1 [] 17 Mar 2018

Meta-F⋆: Metaprogramming and Tactics
in an Effectful Program Verifier
GUIDO MARTÍNEZ, CIFASIS-CONICET Rosario
DANEL AHMAN, Inria Paris
VICTOR DUMITRESCU, MSR-Inria Joint Centre
NICK GIANNARAKIS, Princeton University
CHRIS HAWBLITZEL, Microsoft Research
CĂTĂLIN HRIŢCU, Inria Paris
MONAL NARASIMHAMURTHY, University of Colorado Boulder
ZOE PARASKEVOPOULOU, Princeton University
CLÉMENT PIT-CLAUDEL, MIT CSAIL
JONATHAN PROTZENKO, Microsoft Research
TAHINA RAMANANANDRO, Microsoft Research
ASEEM RASTOGI, Microsoft Research
NIKHIL SWAMY, Microsoft Research
Verification tools for effectful programming languages often rely on automated theorem provers such as SMT
solvers to discharge their proof obligations, usually with very limited facilities for user interaction. When the
need arises for logics (e.g., higher order or separation logic) or theories (e.g., non-linear arithmetic) that are
hard for SMT solvers to efficiently automate, this style of program verification becomes problematic.
Building on ideas from the interactive theorem proving community we introduce Meta-F⋆ , a metaprogramming framework for the F⋆ effectful language and SMT-based program verification tool. Meta-F⋆ allows
developers to write effectful metaprograms suitable for proof scripting, user-defined proof automation, and
verified program construction and transformation. Metaprograms are effectful programs in F⋆ itself, making good use of F⋆ ’s libraries, IDE support, and extraction to efficient native code. Meta-F⋆ , moreover, is
well-integrated with F⋆ ’s weakest precondition calculus and can solve or pre-process parts of the verification
condition while leaving the rest for the SMT solver.
We evaluate Meta-F⋆ on a variety of examples, demonstrating that tactics, and metaprogramming in general,
improve proof stability and automation in F⋆ . Using metaprogrammed decision procedures for richer logics
in combination with SMT solving makes it practical to apply F⋆ in settings that were previously out of reach,
such as separation logic, or that suffered from poor automation, such as the non-linear arithmetic proofs
needed for verifying cryptographic primitives.
CCS Concepts: • Software and its engineering → General programming languages; • Social and professional topics → History of programming languages;

1

INTRODUCTION

Scripting proofs using tactics and metaprogramming has a long tradition in interactive theorem
provers, starting from Milner’s Edinburgh LCF (Gordon et al. 1979). In this lineage, properties about
pure programs are expressed and proven in expressive higher-order (and often also dependently
typed) logics, and proofs are conducted using various imperative programming languages, starting
originally with ML.
Along a different axis, program verification tools like Dafny (Leino 2010), Why3 (Filliâtre and
Paskevich 2013), Liquid Haskell (Vazou et al. 2014), etc., target pure and effectful programs, with
This work is licensed under a Creative Commons Attribution 4.0 International License
© 2018 Copyright held by the owner/author(s).

2

Martínez et al.

side-effects ranging from divergence to concurrency, but provide relatively weak logics in which to
specify properties (e.g., first-order logic with a few selected theories like linear arithmetic). The
verification conditions computed by these tools are encoded to automated theorem provers such as
SMT solvers, with few facilities for user interaction, beyond querying the SMT solver for facts it can
prove. The lack of fine-grained control over proofs and automation, especially when (inherently
incomplete) SMT solving times out, is an often cited shortcoming of this second approach.
This paper proposes a way to bridge the gap between these worlds in the context of F⋆ , a
programming language and verification tool combining user-defined effects and a full-spectrum,
dependent type system (Ahman et al. 2017; Swamy et al. 2016). Verification in F⋆ has, to date, only
relied on generating verification conditions that are discharged by SMT solving. In this work, we
describe Meta-F⋆ , a metaprogramming framework for F⋆ that unleashes the full power of F⋆ ’s
logic, while still retaining its strong support for SMT-based proof automation. This combination
enables new techniques for program verification:
Separation logic + SMT for stateful programs. Despite being expressible in its logic, proofs using
separation logic (Reynolds 2002) have been impractical in F⋆ . A key difficulty is in solving for
existentially bound heap frames at nearly every step of the proof, which is intractable with an SMT
solver. With Meta-F⋆ , we programmed a tactic sl_auto to verify stateful programs in a fragment of
separation logic. The tactic only solves for heap frames, leaving the rest of the proof to the SMT
solver, allowing for the mixture of separation logic with F⋆ ’s regular specifications and theories
well-supported in SMT. Here is a small program automatically verified using this approach:
let swap (r1 r2:ref int) : STATE unit (λ post m0 → ∃x y. m0 == r1 7→ x • r2 7→ y ∧ post () (r1 7→ y • r2 7→ x))
by sl_auto = let x = !r1 in r1 := !r2; r2 := x

Non-linear arithmetic in proofs of cryptography. Non-linear arithmetic poses a serious challenge
for predictable and scalable SMT proofs, yet it is crucially needed for the verification of cryptographic
primitives (Bond et al. 2017; Zinzindohoué et al. 2017). We program a tactic for canonicalizing terms
in commutative semirings, and apply it to prove the main lemmas in the correctness proof of an
optimized implementation of the Poly1305 MAC algorithm (Bernstein 2005). Where previous proofs
in tools like F⋆ and Dafny were painfully detailed and brittle (e.g., requiring dozens of explicit steps
of rewriting of large polynomials to nudge the SMT solver towards a proof), in Meta-F⋆ the proof
is reduced to a single call to our canon_semiring tactic, leaving the rest of the proof to the efficient,
linear arithmetic theory in Z3 (de Moura and Bjørner 2008).
Metaprogramming the construction of verified effectful programs. Tactics in Meta-F⋆ are a special case of general metaprogramming that supports the inspection and construction of arbitrary
program syntax. Our third case study uses Meta-F⋆ to implement a correct-by-construction transformation of F⋆ terms within F⋆ itself. Specifically, we generate a low-level formatter for network
messages from a high-level, pure specification of the network format, with a proof of their equivalence. The generated low-level code is compatible with the rest of the F⋆ toolchain, allowing it to
be extracted to efficient C code by F⋆ ’s C backend (Protzenko et al. 2017).
Meta-F⋆ is just F⋆ with a custom effect. Rather than defining a separate language for metaprogramming and tactics, a central design principle of our work is that the language of Meta-F⋆ is
simply F⋆ itself. As such, metaprograms are typed, call-by-value, direct-style, higher-order functional programs, as intended by Milner. Metaprograms are executed during type-checking and are
isolated using F⋆ ’s user-extensible effect system from programs that execute at run-time. While, by
default, metaprograms are interpreted using F⋆ ’s normalizer, they can also be extracted to OCaml

Meta-F⋆ : Metaprogramming and Tactics in an Effectful Program Verifier

3

and dynamically linked with the F⋆ type-checker for faster execution. Finally, like any other F⋆
program, Meta-F⋆ programs can, in principle, themselves be verified and metaprogrammed.
1.1

Summary of contributions

The main contributions of this work are the design and formalization of a new metaprogramming
framework suitable for aiding the SMT-based verification of effectful programs, together with the
implementation and evaluation of this framework in F⋆ . The main highlights are described below:
(1) The design of the Meta-F⋆ effect-based metaprogramming framework and its implementation in the F⋆ toolchain, providing a new verification tool that encourages the judicious
combination of tactic- and SMT-based automation.
(2) A trust argument for the Meta-F⋆ design in the style of LCF, accounting for metaprogramming
in both proof-relevant and proof-irrelevant contexts. (§3)
(3) A way to integrate metaprogramming with verification condition generation in a program
verifier for effectful programs (§3.2)
(4) The experimental evaluation of Meta-F⋆ on 3 significant case studies: non-linear arithmetic
(§4), separation logic (§5), and correct-by-construction effectful program generation (§6).
2 META-F⋆ , BY EXAMPLE
We start this section with a very brief introduction to F⋆ and then describe how we model tactics as
a user-defined effect. In the rest of the section we illustrate Meta-F⋆ using increasingly sophisticated
metaprogramming examples, from a “Hello Metaprogramming World” to an expressive patternmatching engine used for proof automation, written fully as a user-level F⋆ metaprogram.
2.1

A short introduction to F⋆

At the core of F⋆ is a dependently typed language of pure total functions (Swamy et al. 2016).
This language also forms the logic for F⋆ ’s program specifications and their proofs. In addition,
F⋆ also provides primitive support for divergent computations. Layered on top of this core is
an extensible system of monadic effects, which allows users to program other effects on top of
purity and divergence simply by providing monadic definitions. A type-and-effect system keeps
effectful computations separate from pure ones, ensuring that they do not pollute F⋆ ’s logic, which,
unsurprisingly, demands purity for consistency. F⋆ includes a weakest precondition (WP) calculus
that is generic in the effect and based on an adaptation of Dijkstra’s predicate transformers to
higher-order programs (Ahman et al. 2017; Swamy et al. 2013). Programmers can specify precise preand postconditions for their programs using a notation similar to Hoare Type Theory (Nanevski
et al. 2008b) and F⋆ checks that the specifications inferred for these programs are subsumed by the
programmer-given ones. This subsumption check is reduced to a logical validity problem that was
until now discharged using the Z3 SMT solver, and, as of this work, also metaprogrammed tactics.
Syntax and notational conventions. F⋆ syntax is roughly modeled on OCaml (val, let, match etc.)
although there are differences to account for additional features. Binding occurrences b of variables
take the form x:t, declaring a variable x at type t; or #x:t indicating a binding for an implicit argument.
λ(b1 ) ... (bn ) → t introduces a lambda abstraction, whereas b1 → ... → bn → c is the shape of a curried
function type. Function codomains are computation types of the shape M t wp where M is an
effect label, t a return type, and wp a specification term. Refinement types are written b{t}, e.g.,
x:int{x≥ 0} is the type of non-negative integers (nat). As usual, a bound variable is in scope to the
right of its binding; we omit the type in a binding when it can be inferred; and for non-dependent
function types, we omit the variable name. For example, the type of the pure append function
on vectors is written #a:Type → #m:nat → #n:nat → vec a m → vec a n → vec a (m + n), with the two

4

Martínez et al.

unnamed explicit arguments and the return type depending on the first three implicit arguments.
When no effect is specified for an F⋆ function, the default primitive effect Tot is used implicitly.
2.2

An effect for metaprogramming and some first examples

To add an effect to F⋆ , a programmer must simply define a monad. For instance, by defining the state
monad st a = s → a ∗ s, the programmer can request F⋆ to derive the corresponding ST effect. This
introduces the computation types ST a wp, whose semantics is specified by the predicate transformer
wp of type (a ∗ s → prop) → s → prop. Setting aside predicate transformers for the moment (we’ll
return to them in §2.4), the starting point for Meta-F⋆ is the tac monad below—an exception monad
layered on top of a state monad, with Div denoting the primitive effect for possible divergence.
type result a = Success of (a ∗ proofstate)
| Failed of (string ∗ proofstate)
let tac a = proofstate → Div (result a)

The type proofstate is an abstract type corresponding to the (purely functional, persistent) internal
state of the F⋆ type-checker and our new tactics engine. It contains the information needed to
effectively write metaprograms, such as the current set of goals, each with their environment and
type, the state of all unification variables created during metaprogram execution, configuration
options, and some local state available to tactics (including a freshness counter).
The bind, return, and basic actions get and fail for this monad are standard. Notably, the monad
lacks the put action since a metaprogram is forbidden from arbitrarily replacing its proof state with
another; instead to preserve soundness the proofstate can only be modified via a carefully crafted
API (§3). We also provide a handler for failures, or_else t1 t2 , which runs t1 in proof state p; if t1 fails
returning Failed (msg, q), after optionally logging some information about the failure, or_else runs t2
in p, i.e., the proof state (including the state of unification variables) is reset on failure, allowing for
easy backtracking. Backtracking using this reset operation is guaranteed to be O(1).
Given the definition of the tac monad, F⋆ derives an effect Tac a wp with underlying representation
tac a. Programs that use actions like get, fail, or_else, etc. are inferred to have Tac effect, and F⋆
infers the placement of bind and returns. Moreover, where Tac computations interface with pure or
divergent computations, F⋆ automatically places monad morphisms to compose those computations
with Tac computations. The result is that metaprograms can be written in a natural, ML-like style.
A first metaprogram. The metaprogram below generates a pure function zero : bool → int. The
synth primitive takes as argument a metaprogram of type Tac unit, which runs in an initial proof
state consisting of a program context with a single variable x:bool (for the argument), and whose
body is an int-typed “hole” (as indicated by the result type of zero). This goal is easily dispatched by
running the action exact `(0), which solves the goal with the term 0.
let zero (x:bool) : int = synth (dump "proof␣state␣is:␣"; exact (`0))

Even this very simplest of programs can be used to illustrate several key features of Meta-F⋆ :
(1) Proof states consist of several goals, each of which is a triple Γ ⊢ w : t, where the task is to find
a solution for the witness w (most often a meta-variable ?u) that has type t in context Γ. In this
case, the proof state contains a single goal x : bool ⊢ ?u : int, requiring an int-typed term in a
context x:bool. The goals and their components can be inspected both by the metaprograms,
through a set of primitive actions, and by users in a text console or the emacs IDE for F⋆ .
(2) Metaprograms manipulate the abstract syntax of terms. The notation `t is a static quotation
for t: it represents the abstract syntax of its argument, in this case the int-typed constant 0.
Besides simply manipulating the abstract syntax, metaprograms can also translate between
abstract syntax and concrete values, in different ways which we detail below.

Meta-F⋆ : Metaprogramming and Tactics in an Effectful Program Verifier

5

(3) Metaprograms manipulate the proof state using built-in monadic actions; e.g., dump prints
out the current proof state and exact attempts to solve the goal by unifying the goal’s witness
with 0 and checking that it has the proper type.
(4) F⋆ evaluates metaprograms during type-checking. As they are ordinary F⋆ programs, this
evaluation, by default, happens by just interpreting the term using F⋆ ’s normalizer. The
metaprogram terminates successfully when every goal in the proof state has been solved.
Then, F⋆ replaces the hole with the generated witness; in this case, 0, producing, in a very
roundabout way, the definition let zero (x:bool) : int = 0.
Fibonacci. Next, let us build a slightly more interesting metaprogram: a staged computation of
the nth Fibonacci number. Here is a first attempt:
let rec fib n : Tac unit = if n < 2 then exact (`1) else (apply (`(+)); fib (n − 1); fib (n − 2))
let f3 : int = synth (fib 3)

We define a new metaprogram fib, which uses built-in general recursion available for all computations whose effect may include divergence. The apply action solves the current goal by unifying its
type with the result type of the argument to apply, producing sub-goals for each of the arguments.
In this case, the two generated sub-goals are solved by recursive calls to fib.
This metaprogram almost gets the job done, but not quite: when invoked to define f3, fib builds
the program (1 + 1) + 1, which is close, but not quite the fully staged computation that we were
aiming for. The reason is that metaprograms solve the goal by constructing the witness in exactly
the syntactic shape described—all manipulations of the object programs being built, including
reduction, must be requested explicitly. Here’s one way:
let f8 : int = synth (solve_then (λ () → fib 8) compute)

Here, we use the derived action solve_then t1 t2 , which solves the goal using the thunked tactic t1
and then further process its solution with the thunked tactic t2 —the thunks are necessary because
F⋆ uses call-by-value reduction for effectful terms and, otherwise, the evaluation of fib 8 would
occur prior to calling solve_then. In this case, we post-process the solution with the compute tactic,
which is a hook into F⋆ ’s normalizer. As a result, f8 is metaprogrammed to a fully reduced value,
i.e., to 34, and is from here on indistinguishable from having appeared as such in the program’s text.
Deriving boilerplate. More often than programming fibonacci numbers, programmers are tasked
with writing tedious boilerplate code, such as printers. Metaprograms can help. In the example
below, mk_printer is a metaprogram that from a type t derives a corresponding top-level definition.
The %splice construct evaluates the metaprogram and inserts the definition in the environment.
If the metaprogram generates a definition named print_ty, then print_ty is in scope after the %splice.
type ty = | A : int → string → ty | B : ty → int → ty | ... | ZZ : ... → ty
%splice (λ () → mk_printer (`ty))

On encountering the %splice, the type-checker runs the metaprogram within it presenting a goal of
type def, a datatype providing a view over top-level F⋆ definitions. When the metaprogram finishes,
the type-checker takes such definition and treats it as if it was written by the user, type-checking
it and making it available to other code. In this case, we generate a new top-level function that
converts its argument to a textual representation. This function is in the Tot effect of pure total
functions, which involves a proof about its termination, in this case discharged by F⋆ using SMT.
2.3

Proof irrelevant assertions

Aside from constructive, dependently typed programming, at the heart of F⋆ is a proof-irrelevant
logic of refinement types (and predicate transformers, cf. §2.4). For instance, F⋆ defines the type

6

Martínez et al.

nat to be x:int{x ≥ 0}, i.e., a subtype of int restricted to its non-negative values. In F⋆ nats and ints
share the same representation, i.e., no constructive proof for the refinement formula x ≥ 0 is ever

materialized; instead, typically, an (inherently classical) SMT solver is used to check that the
refinement formula is valid in the current program context.
The notion of proof irrelevance in F⋆ is built from these refinement types, based also on the
ideas of Nogin (2002). In particular, F⋆ defines the type of squashed propositions squash p = _:unit{p},
i.e., the refinement of unit in which p is valid. The type squash p is a sub-singleton whose inhabitants include, at most, the unit value, (). The squash type is a monad: a proof of p can always be
squashed and squash (squash p) is equivalent to squash p. Using squash, F⋆ defines the following
proof-irrelevant connectives on which most of its SMT-based proofs rely:
let ⊥ = squash empty
let ⊤ = squash unit
let ( ∧ ) p q = squash (p ∗ q)
let ( ∨ ) p q = squash (either p q)

let ( =⇒ ) p q = squash (p → q)
let ¬p = p =⇒ ⊥
let (∀) #a p = squash (x:a → p x) (∗ written ∀x. p x ∗)
let (∃) #a p = squash (x:a & p x) (∗ written ∃x. p x ∗)

A typical usage of these connectives is in conjunction with F⋆ ’s statically checked assertions.
When one writes assert p, F⋆ attempts to prove squash p, using an SMT solver. Meta-F⋆ extends this
form of assertion to assert p by t, where t:unit → Tac unit is a metaprogram proving squash p.
Two styles of proofs. Consider the following standard definition of unary natural numbers (unat),
a conversion from nat to unat, and an inductive predicate defining the evenness of unats.
type unat = | Z : unat | S : unat → unat
let rec nat2unary (n: nat) : unat = if n = 0 then Z else S (nat2unary (n − 1))
type even : unat → Type = | Even_Z : even Z | Even_SS : #n: unat → even n → even (S (S n))

Building a proof of evenness for a unat is tedious and can be easily automated with a metaprogram.
For example, prove_even below builds the proof term Even_SS (Even_SS ... Even_Z): this is constructive,
but it comes with the cost of having to build and check proof term, which can often be quite large.
let prove_even () = compute(); ignore (repeat (λ () → apply (`Even_SS))); apply (`Even_Z)
let even10 : even (nat2unary 10) = synth prove_even

An alternative, more efficient way is to work with a squashed variant of even, as implemented by
even_Z and even_SSn below, functions that use the squash monad (written using its do-notation).
let even_Z : squash (even Z) = return Even_Z
let even_SSn #n (s:squash (even n)) : squash (even (S (S n))) = en <- s ; return (Even_SS en)

Now, to prove squash (even (nat2unary 1024)), we assert it and prove it using prove_even_sq. This
time we use mapply, a variant of apply, which when successfully applied to a squashed goal solves
the witness simply using (). Avoiding building the proof term can provide a significant speedup.
let prove_even_sq () : Tac unit = compute(); ignore (repeat (λ () → mapply (`even_SS))); mapply (`even_Z)
let even_sq = assert (even (nat2unary 1024)) by prove_even_sq

2.4

Integrating the proofstate with VC generation

So far, our metaprograms have worked with relatively simple proof states. However, as we build
larger verified programs, we have to contend with proof states that are built using F⋆ ’s verification
condition generator (Ahman et al. 2017).

Meta-F⋆ : Metaprogramming and Tactics in an Effectful Program Verifier

7

VC generation using Dijkstra monads. Every computation e in F⋆ is given a computation type
M a wp, where M (e.g, PURE, ST, or TAC) is a label that is an upper bound on the effects of e; a is its
result type; and wp is a weakest precondition predicate transformer that specifies the semantics of
e by a pure predicate in F⋆ ’s logic.. Just as the underlying representation of the effect M is a monad
m (e.g, tac), the WPs also form a monad derived from m, known as the Dijkstra monad for m. This
Dijkstra monad is, roughly, a composition of m with the continuation monad (a → prop) → prop.
Even pure computations in F⋆ are given such computation types. Specifically, the typing judgment Γ ⊢ e : PURE a wp states that e is pure computation that evaluates, for any postcondition
post : a → Type for which squash (wp post) is valid, to a value of type x:a{post x}. In other words,
wp : (a → Type) → Type is a predicate transformer that computes a proof-irrelevant, sufficient precondition of e with respect to any post. Whereas the system computes WPs for computations,
programmers annotate their programs using Hoare triple types, which are easily desugared into
predicate transformers: a couple of common abbreviations are shown below.
effect Pure a (requires pre) (ensures post) = PURE a (λ k → pre ∧ ∀x. post x =⇒ k x)
effect Lemma (requires pre) (ensures post) = Pure unit (requires pre) (ensures λ() → post)

For example, here is a verified implementation of Quicksort, annotated with a postcondition and
additionally, a termination measure, decreases (length l).1
let rec quicksort #a (f:total_order a) (l:list a) : Pure (list a) (ensures λm → sorted f m ∧ perm l m)
(decreases (length l)) = match l with
| [] → []
| pivot::tl → let hi, lo = partition (f pivot) tl in
let m = quicksort f lo @ pivot :: quicksort f hi in
(assert (perm l m) by (λ () → qs_tac l); m)

This verified implementation uses an “intrinsic proof”. The proof is structured by the control
flow of the program itself, asserting properties at specific program points, avoiding duplication and
making the overall proof more compact. For instance, one step in the proof involves showing that
the returned list m is a permutation of the original list l. Informally, from the pattern matching we
know that l = pivot :: tl and from the specification of partition we know that hi @ lo is a permutation of
tl, so recursively sorting hi and lo and placing the pivot in the middle should produce a permutation
of l. Completing this part of the proof requires the auxiliary lemma below, whose proof, by contrast,
is “extrinsic”, establishing a property of the append function on lists separately from its definition.
val perm_app #a (hd:a) (tl l1 l2:list a) : Lemma (requires perm tl (l1 @ l2)) (ensures perm (hd::tl) (l1 @ hd::l2))

Prior to our work, there were two ways of making use of a lemma like perm_app in the proof of
quicksort, both with their own pros and cons:

• One could decorate the lemma with the expression in its post-condition as an E-matching
trigger (Moura and Bjørner 2007) and rely on the SMT solver to automatically invoke this
lemma when it tries to prove the postcondition of quicksort. While proofs based on E-matching
can be concise and automated, it requires an F⋆ and SMT expert to find a good trigger, when
good choices are at all available. Poorly chosen triggers can cause verification performance
to degrade and can make automation unpredictable: for example, relying on this style even
for this tiny example required doubling the default timeout of the Z3 SMT solver used with
F⋆ from 5 to 10 seconds.
decreases annotation is the termination measure for this function and is not, strictly speaking, part of the type. We
also drop the precondition when it is just requires ⊤.

1 The

8

Martínez et al.
a: eqtype
f: total_order a
l: list a
h0: squash (¬(Nil? l))
h1: squash (Cons? l)
pivot: a
tl: list a
h2: squash (l == pivot :: tl)
hi, lo: list a
h3: squash (partition (f pivot) tl == hi,lo)
----------------------------------------------------------------------?u : squash (perm l (quicksort f lo @ pivot :: quicksort f hi))
Fig. 1. Proof state for qs_tac (simplified)

• Instead of relying on SMT to find an instantiation of the lemma, one can insert an explicit call
to the lemma in the code of quicksort; in this case perm_app pivot (quicksort f lo) (quicksort f hi)
works, but in general, finding the precise instantiation to use requires some careful thought
from the user. This can be especially hard when the user has no way to directly inspect the
current proof state.
In Meta-F⋆ , by associating a tactic to a specific assertion, the user can get a view of the proof
state at that program point, i.e., we retain the intrinsic proof style but extend it with tactics. For
qs_tac above, the proof state is displayed in Figure 1, with only a subset of the hypotheses shown.
As expected, the context includes binders for the variables in the lexical scope. But, more
interestingly, it also includes hypotheses h0, h1, representing the result of case analyzing l with the
patterns taken in order; the hypothesis h2 for the destruction of l into its components; and h3, an
equation for the pattern matching on the tuple hi, lo. In other words, the proof state summarizes
the control and data flow assumptions at that program point. Building this proof state during VC
generation in a form that allows us to focus a tactic’s attention on just a specific part of VC is one
of our main contributions—we present it in detail in §3.2.
Here is our small script that tackles this proof state:
let qs_tac l = with_pat (λ y (h:hyp (squash (l == y))) → rewrite h); mapply (`perm_app)

The with_pat command finds an equality hypothesis h of the form squash (l == y), in this case h2,
and then rewrites l in the goal producing a new goal
squash (perm (pivot::tl) (quicksort f lo @ pivot :: quicksort f hi))

We can solve this by using mapply to unify the postcondition of perm_app with it. What’s left is the
precondition of the perm_app, but rather than solve it the tactic, we leave it for F⋆ to dispatch to the
SMT solver, which handles it automatically (from the specification of partition and hypothesis h3).
This example illustrates proof scripting “in the small”: we used a tactic to do just a couple of
small steps in a proof that are difficult for an SMT solver, and we did so by interacting closely with
the proof state and executing specific commands to transform it. While this kind of exploratory
interaction of the proof state is an important addition to F⋆ , the main use of Meta-F⋆ is more geared
towards building user-defined automation for proof programming “in the large”, i.e., we aim to
build reusable libraries for structuring proofs, as well as partial decision procedures for dispatching
goals mostly automatically. A case in point is the with_pat tactic, a library programmed in Meta-F⋆

Meta-F⋆ : Metaprogramming and Tactics in an Effectful Program Verifier

9

that provides a simple yet powerful way to analyze the current proof state using non-linear pattern
matching: we describe our use of syntax inspection and quotation that supports the construction
of such libraries, next.
2.5

Syntax inspection, generation and quotation

Suppose we have a goal of the form squash(a == b), and we want our metaprogram to take different
paths according to the shape of a and b. How do we capture these subterms of the goal? Once
captured, how do we use those term representations to build deeper syntax? While one can find
ways to do both things via tactic primitives such as apply, it quickly becomes tedious and inefficient
to do so. Therefore, an explicit way of inspecting terms is crucial in order for metaprograms to
implement their own goal-specific logic. Like any metaprogramming system, Meta-F⋆ offers a way
to inspect and construct the syntax of F⋆ terms. Our design, especially the quotation mechanism, is
inspired by Lean’s (Ebner et al. 2017).
Inspecting syntax. Internally, F⋆ uses a locally nameless representation with explicit, delayed
substitutions. Rather than exposing this complex representation directly we keep it hidden from
metaprograms and allow access through a view (Wadler 1987), which shields metaprograms from
some of the internal administration of terms. Here are a few constructors from the term_view type
in FStar.Reflection.Data.
assume new type term
val inspect : term → Tac term_view
val pack : term_view → term

type term_view =
| Tv_BVar : v:dbvar → term_view
| Tv_Var : v:name → term_view
| Tv_FVar : v:qname → term_view
| Tv_Abs : bv:binder → body:term → term_view
| Tv_App : hd:term → a:(term ∗ aqual) → term_view
| Tv_Arrow : bv:binder → c:comp → term_view
...

Views are not recursive: the arguments to the constructors of a term_view are of type term, an
opaque type representing the internal terms. Metaprograms can peel back the view one constructor
at a time to deeply inspect a term. The view exposes three kinds of variables: bound variables,
Tv_BVar; named local variables Tv_Var; and top-level fully qualified names, Tv_FVar. Bound variables
and local variables are distinguished since the internal abstract syntax is locally nameless. For
metaprogramming, it is usually simpler to use a fully-named representation, so inspect and pack
will also open and close binders appropriately to maintain this invariant. Since opening binders
requires freshness, inspect cannot be marked pure if we hope to keep F⋆ ’s logic consistent.2
Generating syntax via repeated applications of pack is too tedious for users, and so we provide
some ways of quoting terms in Meta-F⋆ .
Static quotations. Static quotations (which we have already used since §2.2) make some syntax
handling trivial: `e is just a shorthand to parse e into the abstract syntax of F⋆ terms, thus allowing
to reuse the F⋆ parser for building metaprogram-level abstract syntax. For instance, `(x + 1) is just
sugar for the following abstract syntax:
pack (Tv_App(pack (Tv_FVar "Prims.op_Addition"), [pack (Tv_Var "x"), ...]))

2

We also provide functions inspect_ln, pack_ln which stay in a locally-nameless representation and can be made total.

10

Martínez et al.

The only “smarts” here are that F⋆ tries to resolve names in the current scope before building the
abstract syntax, which allows it to distinguish qualified names (e.g., resolving + to Prims.op_addition)
from local constants.
Dynamic quotations. A second form of quotation is dynamic_quote: #a:Type → a → Tac term, an
effectful operation that is interpreted by F⋆ ’s normalizer during metaprogram evaluation. Intuitively, it returns the syntax of its argument at the time dynamic_quote e is evaluated. Evaluating
dynamic_quote e substitutes all the free variables in e with their current values in the execution
environment, suspends further evaluation, and returns the abstract syntax of the resulting term.
For instance, evaluating (λx → dynamic_quote (x + 1)) 16 produces the abstract syntax of 16 + 1. We
abbreviate dynamic_quote e as `@ e.
Quasi-quotations and Anti-quotations. Static quotations are useful to build big chunks of syntax
concisely, but they are of limited use if we cannot combine them with some other bits of syntax.
Quasi-quotations, noted by ``t, allow such combinations by anti-quotations within them which
escape a purely syntactic meaning, and represent holes in the syntax. For example, the term
``(y + `@x) creates syntax for an application of (+) where one operand is a free variable y and the other
is taken from the lexical scope of the quasi-quotation. Then the term let z = 25 in (λx → ``(y + `@x)) z
produces a representation of y + _, where the underscore is spliced in with a dynamic quotation of
x, and will reduce to a representation of y + 25, where y remains unsubstituted.
Unquotation. Finally, we have an effectful operation, unquote: #a:Type → ast:term → Tac a, which
takes a term representation ast and an expected type for it a (usually inferred to be the expected
type from the context), and calls the F⋆ type-checker to check and elaborate the term representation
into a well-typed term. Note that, morally, unquote #a t is equivalent to synth (λ() → exact t), except
that it runs completely dynamically instead of being removed by type-checking.
Syntax inspection and quotation at work. Let’s return to the question posed at the start of this
subsection: suppose we have a goal of the form squash(a == b); how do we easily capture a and b for
further inspection? One way would be to write a nest of matches inspecting terms in the goal, but
this is very cumbersome:
let eq_lhs_rhs () = match inspect (cur_goal ()) with | Tv_App hd (g, _) → (match inspect hd with ...)

However, using quotation, we can provide a convenient syntax for programmers to write patterns
to match components of the hypotheses and goal, compiling those quoted terms into an libraryspecific language of patterns, and searching through the proof state for matches. The library,
FStar.Tactics.PatternMatching does just this, making it much easier to implement user-tactics that do
fine-grained inspection of the goal, like the propositional tautology prover shown below.
let rec tauto () : Tac unit =
repeat #unit (λ () → first_match
with_pat (λ (g: goal (squash ⊤)) → trivial ());
with_pat (λ a (h: hyp a) (g: goal a) → exact (as_term h));
with_pat (λ a b (g: goal (squash (a ∧ b))) → split ());
with_pat (λ a b (g: goal (squash (a =⇒ b))) → mintro ());
with_pat (λ a b (g: goal (squash (a ∨ b))) → (λ () → left (); tauto ()) `or_else` (λ () → right (); tauto ()))]);
qed()

The metaprogram with_pat demonstrated here is a fairly complete implementation of the type of
backtracking pattern-matching primitive in Coq’s Ltac (Delahaye 2000) or in Lean (Ebner et al. 2017),
built instead as a library in F⋆ . The with_pat metaprogram, of type #a:Type → a → Tac unit is has two

Meta-F⋆ : Metaprogramming and Tactics in an Effectful Program Verifier

11

main components: a DSL to concisely express a pattern-matching problems, and an interpreter to produce an assignment matching it. Take with_pat (λa b (h: hyp (a =⇒ b)) (_: goal (squash b)) → mapply h)
as a concrete example. Using dynamic quoting to inspect its argument, with_pat obtains an F⋆ AST
(Tv_Abs ...), and inspects its binders in search of the tags goal and hyp which indicate what each
pattern applies to. From this AST, it then builds a pattern-matching problem, composed of existential
variables to instantiate (here a and b), hypothesis patterns (here, PApp (PQn "=⇒ ") [PVar a; PVar b]),
goal patterns (here, PApp (PQn "squash") [PVar b]), and a continuation tactic to run with a and b instantiated (here, λa b h _ => mapply h). A recursive backtracking unification procedure matches the
pattern against the current goal and hypotheses, producing a lazy stream of satisfying assignments
and running the continuation with each of them, until the continuation succeeds.
In effect, with_pat hijacks the syntax and type-inference of F⋆ to allow the programmer to build
concise pattern-matching clauses, and then interprets the syntax according to the DSL that it
provides—a testament to the flexibility of the quotation and syntax inspection mechanisms that
Meta-F⋆ provides.
3

THE DESIGN OF META-F⋆

Metaprograms in F⋆ have two main use cases: preprocessing VCs in order to simplify, break down,
or completely solve them; and automatically generating executable code. In this section, we present
both these usage modes as instances of a same concept, which is that in principle metaprograms
generate derivations in F⋆ ’s typing judgment by following its rules. To enable this, following the
long tradition of LCF-based proof assistants (Gordon et al. 1979), we expose each rule in the type
system as a primitive metaprogram action. Additionally, with respect to tackling VCs, we describe
how users specify the tactics (i.e., metaprograms to break down VCs) without having direct access
to the entire VC, which is only created after receiving all user input. We see this capability as a
significant advance over the prior state of F⋆ , which provided no way for a user to explicitly inspect
or manipulate a VC aside from sending them wholesale to an SMT solver—and most SMT-based
program verifiers for effectful programs are similar (§7).
3.1

Execution model and trust assumptions

Metaprograms are evaluated at type-checking time, and have no run-time presence. This phase
separation is enforced by F⋆ ’s effect system, i.e., computations that are meant to be executed at
runtime cannot also have the Tac effect. By default, during type-checking, metaprograms are reduced
using F⋆ ’s normalizer, an abstract machine for computing normal forms of pure terms. However,
metaprograms are, a priori, effectful programs which cannot be normalized. We avoid this restriction
by defining our metaprogramming effect monadically as proof-state-passing computations, with
divergence and exceptions, and then have the type-checker automatically convert it into a new
computational effect, as described by Ahman et al. (2017). Such effectful metaprograms can then be
reified into their state-passing representations, which are suitable for reduction on F⋆ ’s abstract
machine. To run a tactic, we apply the reified metaprogram to the initial proof state and start the
abstract machine. The metaprogram will then either diverge, or produce a value in the result type
described in §2.2.
In the course of this evaluation, the abstract machine encounters various metaprogramming
primitive actions. Most of these are either implemented by (1) safely transforming the proof state,
such as building a term by application; or (2) calling into type-checker internals, such as the type
inference engine, normalizer and unifier. For kind (1), we have a correctness criterion for primitives
that are based on typing rules (described below) to ensure that these transformations faithfully
follow F⋆ ’s static semantics, and thus never build ill-typed terms or incorrect proofs. For kind
(2), there is no additional safety requirement, since their usage is trusted in standard F⋆ anyway.

12

Martínez et al.

Nevertheless, proper implementation measures are taken to ensure that the APIs provided maintain
internal type-checker invariants and are safe to execute in any sequence. Indeed, providing access
to internal compiler components to user scripts is a great way to be forced to harden their APIs.
The proof-state and an interpretation of its primitive actions. The main component of the proof
state is a list of open goals, of shape Γ ⊢ _ : t each of which is an obligation to provide a term that is
well-typed in the environment Γ at type t. For example, the goal ∅ ⊢ _ : int requires a term typeable
at type int in the empty environment. As previously described, there are also proof-irrelevant goals
involved, for which deep witnesses are not needed nor built. In practice, these goals are typing
goals at a squashed goal type, matching the formal model of F⋆ ’s logic.
One way a metaprogram could discharge the goal ∅ ⊢ _ : int is by calling apply `f, for some
f of type bool → int, and then solving the new goal. The apply primitive will, after checking that
the return type of f unifies with the goal, forget the original goal and provide a new one for each
argument of f—in this case, one of type bool. Concretely, apply `f changes the proof state as follows:
[∅ ⊢ _ : int] { [∅ ⊢ _ : bool]
Here, a solution to the original goal has not yet been built, since it depends on the solution to the
remaining goal. When it is solved with, say, true, we can solve our original goal with f true. To
formalize these dependencies, we say that a proof state ϕ correctly evolves (via f ) to ψ , denoted
ϕ ⪯f ψ , when there is a generic mapping f , called a solution mapping, from solutions to all of ψ ’s
goals into correct solutions for ϕ’s goals. When ϕ has n goals and ψ has m goals, the mapping f is
a function from solm into soln , where sol represents our meta-level representation of solutions to
goals. These mappings may be composed, providing the transitivity of correct evolution, and if a
proof state ϕ correctly evolves into a state with no more goals, then we have fully defined solutions
to all of ϕ’s goals. We emphasize that these solution mappings are not constructed explicitly during
the execution of metaprograms, and instead using unification metavariables to instantiate the
mappings automatically.
Every primitive metaprogramming action respects the ⪯ preorder. Some of them, such as the flip
action to reorder goals, do so trivially by means of a permutation function. Primitives for the scoping
of goals, such as divide : int → (unit → Tac α) → (unit → Tac β) → Tac (α∗ β), which divides the current
set of goals in two and applies a different metaprogram to each side, are correct since solution
mappings are also horizontally composable, i.e., if ϕ 1 ⪯f1 ψ 1 and ϕ 2 ⪯f2 ψ 2 , where f 1 : soln1 → solm1 ,
then their concatenations also correctly evolve to each other, that is: ϕ 1 @ϕ 2 ⪯(f1 @f2 ) ψ 1 @ψ 2 , where
(f 1 @f 2 )(ē) = f 1 (take n 1 ē)@f 2 (drop n 1 ē).
The correctness of more interesting primitives relies on modeling F⋆ ’s typing rules. For example,
consider the following rule for typing abstractions:
T-Fun

Γ, x : t ⊢ e : t ′
Γ ⊢ λ(x : t).e : (x : t) → t ′
This typing rule immediately induces a metaprogramming primitive we call intro, given by
[Γ ⊢ _ : (x:t) → t'] ⪯f [Γ, x : t ⊢ _ : t']
with f defined as the (mathematical) function taking a term of type t ′ and building syntax for its
abstraction over x. Further, this derived primitive respects the correct-evolution preorder, by the
very typing rule for which it is defined. In this manner, every syntax-directed typing rule produces
a syntax-building metaprogramming step that is correct by construction. Our primitives come from
this dual interpretation of typing rules in order to ensure that logical consistency is preserved.

Meta-F⋆ : Metaprogramming and Tactics in an Effectful Program Verifier

13

Since the ⪯ relation is a preorder, and every metaprogramming primitive we provide the user
evolves the proof state according ⪯, it is trivially the case that the final proof state returned by
a (successful) computation is a correct evolution of the initial one. That means that when the
metaprogram terminates, we have a (hopefully) simpler set of obligations to fulfill.
Proof-irrelevant goals. The following rule for introducing refinement types is key in F⋆ ’s type
system—it forms the basis of proof irrelevance and squashed types, as described in §2.3.
T-Refine

Γ ⊢e : t

Γ |= ϕ

Γ ⊢ e : x :t {ϕ}
Applying a metaprogramming primitive corresponding to (T-Refine) produces two sub-goals:
the solution to the first premise requires building a witness, but the second premise is from a
judgment in F⋆ ’s proof-irrelevant refinement logic. Traditionally, F⋆ would simply check for the
existence of a derivation of the second premise by calling an SMT solver. Similarly, in Meta-F⋆ ,
the second premise produces a proof-irrelevant goal for which we do not build a witness, but only
need to check that that a valid derivation exists, i.e., the proof of this goal is squashed. As such, our
system uses a classic LCF-style architecture for the proof-irrelevant goals, just ensuring that only
valid derivations are accepted, but never constructing or storing proof terms. Furthermore, we stay
close to F⋆ ’s original behavior by feeding any remaining proof-irrelevant goals that are not fully
discharged by tactics to the SMT solver.
Interactions between proof relevance and irrelevance occur in both directions: proof-relevant
rules (e.g., T-Refine) may have proof-irrelevant premises, and vice versa. So, when trying to typecheck a solution to a proof-relevant goal, F⋆ may generate additional proof-irrelevant goals. As a
matter of organization, for proving these additional goals, we provide users with three options: (1)
fail if additional non-trivial goals are produced; (2) add them as new goals for further processing;
(3) attempt to discharge them automatically using SMT. Of course, when transforming a proofirrelevant goal, a proof-relevant goal can easily arise (e.g., from an argument to a lemma); in contrast
with the additional proof-irrelevant goals, proof-relevant goals are always added to the proof-state
for further processing.
Initial state. There are several ways for metaprograms to come to life. We have already seen
examples of synth, which calls the tactic to produce a term during type-checking; %splice, which
is used to generate top-level definitions; and assert φ by tau for proving assertions. The initial goal
for synth and %splice are clear: a term of the expected type in the current typing environment,
and a term of type def for %splice. However, the environment for assert φ by tau must also contain
assumptions for the control flow of the program, otherwise assertions such as:
let abs (i : int) : nat = if i < 0 then (assert (-i > 0) by tau; -i) else i

are simply unprovable. In the next subsection, we describe how we ensure a proper initial environment is provided for tactics that are used for solving assertions with tactics.
3.2

Integrating tactics in a VC

Statically verified assertions are routine in F⋆ and are easily accommodated in its VC generation. In
fact, the assert keyword is just sugar for a pure function of type p:prop → Lemma (requires p) (ensures p),
which introduces a cut in the generated VC. For Meta-F⋆ , we aim to reuse this while allowing
asserted formulae to be decorated with user-provided tactics that are tasked with proving or
pre-processing them. We do this in three steps.
First, we define the simple predicate shown below:

14

Martínez et al.

let with_tac (p:prop) (t:unit → Tac unit) = p

The term p `with_tac`t simply associates the tactic t with p, and is logically equivalent to p.
Next, we implement the lemma assert_by_tactic p t, and desugar assert p by t into it. This lemma
is easily provable in F⋆ since unfolding with_tactic provides the postcondition p immediately.
let assert_by_tactic p t : Lemma (requires p `with_tactic` t) (ensures p) = ()

With this, assert p by t; e produces the VC p `with_tactic`t ∧ (p =⇒ VC'), where the left sub-goal is
tagged with the user-provided tactic, and the right sub-goal has the cut formula p in its hypothesis.
This VC is then incorporated as usual in the the VC of the surrounding program context.
Once we obtain a full VC, we want to split out each of the sub-goals from within this large
formula into separate formulae. For example, if the VC is the following:
with_tac P τ0 =⇒ (with_tac R τ1 ∧ (∀ (x:t). (Q x =⇒ with_tac (H x) τ2 )))

The F⋆ type-checker will descend through this formula and extract all tactic-annotated nodes in
strictly positive positions. For those in negative positions, the tactic is erased, as they are hypotheses
and not obligations. These extracted nodes are turned into a set of new, simpler goals. The original
sub-goal is replaced with ⊤, trivializing it within the larger one. The resulting set for the previous
VC is:
P =⇒ R
P =⇒ ∀(x:t). Q x =⇒ H x
P =⇒ ⊤∧ (∀ (x:t). Q x =⇒ ⊤)

Then the first two goals are preprocessed by running the tactics τ1 , τ2 on them, while the last one
will be solved simply by an internal simplification, as it is now trivial.
The soundness of this approach is given by the following metatheorem of F⋆ :
Theorem 3.1. Let E be a context of type (Γ1 , prop) → (Γ2 , prop) and Γ1 ⊢ φ : prop then
Γ2 ⊨ E[⊤] Γ2 , γ (E) ⊨ φ
Γ2 ⊨ E[φ]
where γ (E) is the of binders of E.
3.3 Compiled tactics
Meta-F⋆ programs are by default evaluated using the F⋆ interpreter, which can be slow for computationally intensive tactics. We introduce a mechanism for compiling and dynamically loading
F⋆ code, subject to some restrictions discussed below—a full description of this feature and its
underlying theory is beyond the scope of this paper.
The F⋆ compiler is implemented in F⋆ . Relying on F⋆ ’s extraction mechanism to OCaml, the
compiler is bootstrapped and runs as an OCaml program. Since Meta-F⋆ programs are just F⋆
programs, we reuse the extraction mechanism to extract metaprograms also to OCaml, compile
and dynamically load them into the running F⋆ process.
Top-level functions marked with the plugin attribute are compiled and registered with the
interpreter, which allows the interpreter to call into native code when the plugin is applied.
Not every Meta-F⋆ program can be loaded as a plugin. F⋆ ’s extraction to OCaml erases types and
other computationally irrelevant parts of the program, meaning that we cannot read back arbitrary
F⋆ terms from a result computed by compiled code. However, we can embed and un-embed terms
of certain types, including pairs, sums, trees over these types, as well as some polymorphic types.
Furthermore, this restriction only applies at the interface between F⋆ and OCaml code, i.e., only
in the type signatures of these functions. In practice, the main entry point of a tactic often has a

Meta-F⋆ : Metaprogramming and Tactics in an Effectful Program Verifier

15

simple type and can be natively evaluated (e.g., it may have type unit → Tac unit, just working on
the initial proof state).
Additionally, code that uses dynamic quotation cannot be evaluated natively, since it relies on
dynamically embedding a value into its syntax as a term, which is not possible in a compiled OCaml
program, e.g., for closures. Likewise, unquotation is not supported, since it amounts to reflective
code evaluation.
Running compiled tactics does not increase our trust assumptions—we trust OCaml anyway, to
run the F⋆ compiler correctly. Furthermore, the execution of tactic code need not be trusted: any
type-correct interaction with the metaprogramming primitives provided by F⋆ is guaranteed to
maintain the consistency of the proof state.
Plugins can also be used to optimize non-tactic computations, e.g., a call to List.sort can be optimized via a plugin, instead of being interpreted. In such cases, we trust F⋆ ’s extraction mechanism
to correctly extract the function in manner that preserves F⋆ definitional equality on applications of
List.sort. Then again, since the F⋆ compiler is itself an F⋆ program extracted to OCaml, the extractor
is already part of F⋆ ’s TCB.
4

CASE STUDY: PROOFS BY REFLECTION FOR VERIFIED CRYPTOGRAPHY

Non-linear arithmetic poses a serious challenge for predictable and scalable SMT proofs, yet it is
crucially needed for the verification of cryptographic primitives (Bond et al. 2017; Zinzindohoué
et al. 2017), an important use case for F⋆ (Bhargavan et al. 2017). In this section we illustrate how a
reflective tactic for commutative semi-rings can be used in the verification of the Poly1305 Message
Authentication Code (MAC) (Bernstein 2005). Our tactics reduce several dozen intricate, manual
steps of reasoning to the application of a single tactic for proving non-linear identities by reducing
the problem to linear arithmetic, which can then be efficiently decided by an SMT solver. As such,
this case study emphasizes one of the main intended usages of Meta-F⋆ : we use metaprogramming
to build special-purpose automation in proofs, especially for steps that are poorly handled by SMT,
while still feeding to SMT problems for which it is a good fit.
4.1

Reflective tactic for commutative monoids

We start by building a simpler tactic for commutative monoids. This tactic will be extended to
commutative semirings (which put together two commutative monoids; §4.2 describes this extended
tactic and its application to solving non-linear arithmetic goals from crypto verification). The tactic
for commutative monoids will also be used on its own as the core for a separation logic solver (§5).
Our tactic uses computational reflection (Gonthier 2008; Grégoire and Mahboubi 2005). In a
proof by reflection the validity of a statement is reduced to a verified symbolic computation
that is executed with the reduction mechanism(s) of the proof assistant. Given a term from our
commutative monoid, we aim to rewrite it into a canonical form. This can simplify many proofs,
e.g., canonicalizing both sides of an equality goal allows its proofs to be discharged trivially with
reflexivity. We accomplish this rewriting as illustrated by the diagram below.
rewrite using a
certified equality proof

Mult (Mult a c) b

a ∗ (b ∗ c)
denote2

reify

denote1

(a ∗ c) ∗ b

canonicalize

[a;b;c]

First, we use Meta-F⋆ ’s syntax inspection facilities to reify the term (e.g., m = (a ∗ c) ∗ b) into a
simple symbolic expression e = Mult (Mult a c) b. Then, we prove that the denotation back to the

16

Martínez et al.

monoid of e is the inverse of its reification—although the reification step is unverified, the proof
that the denotation of e is equivalent to the original m is typically a simple proof by reduction
and reflexivity. Next, we transform e into an internal, canonical representation (e.g., the sorted
list l = [a;b;c]) and prove once and for all that the denotation in the commutative monoid of the
symbolic expression and their sorted lists (i.e, denote1 and denote2 ) coincide.
Our tactic thus consists of reifying the goal to a symbolic representation, applying our correctness
of canonicalization lemma to the goal, followed by normalization. Programming the denotations, the
canonicalizer, and doing their proofs of correctness benefits from F⋆ ’s libraries and usual support
for functional programming and SMT-based proofs, e.g., we reuse the verified implementation of
quicksort for the canonicalization and its proof.
In F⋆ a commutative monoid is represented as a dependent record indexed by a carrier type a:
type cm (a:Type) = | CM : unit:a → mult:(a → a → a) →
unitality : (x:a → Lemma (unit `mult` x == x)) →
associativity : (x:a → y:a → z:a → Lemma (x `mult` y `mult` z == x `mult` (y `mult` z))) →
commutativity:(x:a → y:a → Lemma (x `mult` y == y `mult` x)) → cm a

This record includes a unit constant and a mult binary operation, together with proofs that unit is an
identity element for mult, and that mult is associative and commutative. For instance, integers with
1 and multiplication form a commutative monoid, which F⋆ can prove automatically, using SMT:
let int_multiply_cm : cm int = CM 1 ( ∗ ) (λ x → ()) (λ x y z → ()) (λ x y → ())

We reify terms of monoid type to simple symbolic expressions with the following syntax:
let atom : eqtype = nat
type exp = | Unit : exp | Mult : exp → exp → exp | Atom : atom → exp

A reification tactic takes a term t of type a equipped with a monoid m, inspects its syntax to recognize
occurrences of the unit and mult for m, and constructs a corresponding exp value.
val reification : #a:Type → m:cm a → ts:list term → vm:vmap a → t:term → Tac (exp ∗ list term ∗ vmap a)

Sub-terms that are neither unit nor mult are atoms (Atom nodes) in the produced expression, each
represented as a natural number index into a map vm that stores its denotation back to the carrier
type a. Multiple occurrences of the same sub-term are identified and associated to the same atom.
For instance, the F⋆ integer term (incr b ∗ 1) ∗ 2 ∗ a ∗ (c ∗ a) ∗ 1 is reified to the symbolic expression
e = (Atom 0 `Mult` Unit) `Mult` Atom 1 `Mult` Atom 2 `Mult` (Atom 3 `Mult` Atom 2) `Mult` Unit

to be interpreted with respect to the variable map vm=[0 7→ incr b; 1 7→ 2; 2 7→ a; 3 7→ c]. Our canonicalization procedure takes e and produces a sorted list of variables: [0,1,2,2,3], that can be easily
compared to another expression that was canonicalized with respect to the same map vm. For
instance the expression a ∗ incr b ∗ c ∗ a ∗ 2 has the same canonical form.
We prove once and for all that this canonicalization procedure is correct. For this we define the
straightforward semantics of expressions and of lists of variables in terms of monoid operations:
val mdenote : #a:Type → cm a → vmap a → exp → a
val xsdenote : #a:Type → cm a → vmap a → list var → a

Using the monoid laws we prove that the semantics of an expression’s canonical form is the same
as the semantics of the original expression:
let canon (e:exp) = sort (flatten e)
val canon_correct #a (m:cm a) (vm:vmap a) (e:exp) : Lemma (mdenote m vm e == xsdenote m vm (canon e))

Meta-F⋆ : Metaprogramming and Tactics in an Effectful Program Verifier

17

We can now use canon_correct to efficiently rewrite monoid terms to canonical form, e.g., in
equality goals such as the one below:
assert (∀ (a b c d : int). (b ∗ 1) ∗ 2 ∗ a ∗ (c ∗ a) ∗ 1 == a ∗ b ∗ c ∗ a ∗ 2)
by (λ _ → ∀_intros(); canon_monoid_eq int_multiply_cm; trefl())

The tactic canon_monoid_eq reifies both sides of the equality, then changes the goal to an equality
between the denotations of these expressions (which requires proving it equal to the original goal;
this is automatic via computation), then rewrites all occurrence of mdenote m vm e in the goal to
xsdenote m vm (canon e), using canon_correct; and finally calls the F⋆ normalizer to reduce the goal:
let canon_monoid_eq (#a:Type) (m:cm a) : Tac unit = norm [];
match term_as_formula (cur_goal ()) with
| Comp _ t1 t2 → let (r1, ts, vm) = reification m [] (const (CM?.unit m)) t1 in
let (r2, _, vm) = reification m ts vm t2 in
change_sq (`@ (mdenote m vm r1 == mdenote m vm r2));
rewrite (`canon_correct);
canon_norm ()
| _ → fail "Goal␣should␣be␣an␣equality"

4.2

Solving non-linear arithmetic in Poly1305 using commutative semirings tactic

Poly1305 (Bernstein 2005) is a widely-used cryptographic message authentication code (MAC)
that computes a series of integer multiplications and additions modulo a large prime number
p = 2130 − 5. Implementations of the Poly1305 multiplication and mod operations are carefully
hand-optimized to represent 130-bit numbers in terms of smaller 32-bit or 64-bit registers, using
clever tricks to express mod p operations with addition, multiplication, and bitwise operations
rather than division. Proving the correctness of such implementations requires reasoning about
long sequences of additions and multiplies. For example, a proof of OpenSSL’s x64 implementation
of Poly1305 requires two main lemmas, poly_multiply and poly_reduce (Bond et al. 2017), the first of
which looks as follows:
val poly_multiply (n p r h r0 r1 h0 h1 h2 s1 d0 h1 h2 hh : int) : Lemma
(requires p > 0 ∧ r1 ≥ 0 ∧ n > 0 ∧ 4 ∗ (n ∗ n) == p + 5 ∧ r == r1 ∗ n + r0 ∧
h == h2 ∗ (n ∗ n) + h1 ∗ n + h0 ∧ s1 == r1 + (r1 / 4) ∧ r1 % 4 == 0 ∧
d0 == h0 ∗ r0 + h1 ∗ s1 ∧ d1 == h0 ∗ r1 + h1 ∗ r0 + h2 ∗ s1 ∧
d2 == h2 ∗ r0 ∧ hh == d2 ∗ (n ∗ n) + d1 ∗ n + d0)
(ensures (h ∗ r) % p == hh % p)

Proving poly_multiply requires 41 steps of rewriting for associativity and commutativity (AC)
of multiplication, and distributivity of addition and multiplication; plus many more steps of ACrewriting for addition.
Prior proofs of correctness of Poly1305 and other cryptographic primitives using SMT-based
proof assistants, including in F⋆ (Zinzindohoué et al. 2017) and Dafny (Bond et al. 2017; Hawblitzel
et al. 2014, 2017) use a combination of SMT automation and manual rewrites. On the plus side, SMT
solvers are excellent at linear arithmetic, so these proofs delegate all AC reasoning of addition to
SMT. Non-linear arithmetic, even just AC-rewriting and distributivity are inefficient and unreliable—
so much so that prior efforts generally just turn off support for non-linear arithmetic theories in
the SMT solver, so as not to degrade the verification performance across the board, due to poor
interaction of theories. In this setting, completing a proof of a lemma like poly_multiply either
requires manually invoking 41 lemmas to do the rewriting, or treating multiplication and addition
as uninterpreted functions and crafting E-matching triggers to have the SMT solver find the needed

18

Martínez et al.

instantiations. Both of these approaches have significant downsides: manual lemma invocation,
especially at this scale, requires great determination, while good E-matching triggers can be hard
to discover and poor choices send the SMT solver off the rails (as also discussed in §2.4).
In this subsection, we briefly describe our reflective, rewriting tactic for commutative semirings,
building on the commutative monoid tactic of the previous section. Using this tactic, we reduce the
proof of Poly1305’s poly_multiply lemma to a single lemma about modular addition followed by a
call to our commutative semiring tactic, which, by canonicalizing the term into a sum-of-products
form, leaves all the remaining work to the SMT solver, which can easily discharge the goal using
linear arithmetic only:
let poly_multiply (n p r h r0 r1 h0 h1 h2 s1 d0 h1 h2 hh : int) =
let r14 = r1 / 4 in
let h_r_expand = (h2 ∗ (n ∗ n) + h1 ∗ n + h0) ∗ ((r14 ∗ 4) ∗ n + r0) in
let hh_expand = (h2 ∗ r0) ∗ (n ∗ n) + (h0 ∗ (r14 ∗ 4) + h1 ∗ r0 + h2 ∗ (5 ∗ r14)) ∗ n
+ (h0 ∗ r0 + h1 ∗ (5 ∗ r14)) in
let b = (h2 ∗ n + h1) ∗ r14 in
modulo_addition_lemma hh_expand p b; //(hh_expand + b ∗ p) % p = hh_expand % p
assert (h_r_expand == hh_expand + b ∗ (n ∗ n ∗ 4 + (−5))) by (λ _ → canon_semiring int_csr)

The proof of Poly1305’s poly_reduce lemma is similarly well automated.
Canonicalizer for commutative semirings. A commutative semiring is a pair of commutative
monoids, one for addition and one for multiplication, together with a proof of distributivity of the
multiplication over addition:
type csr (a:Type) =
| CSR : cm_add:cm a → cm_mult:cm a →
distribute:distribute_lemma a cm_add cm_mult → //x ∗ (y + z) == x ∗ y + x ∗ z

We reuse the proof-by-reflection structure described in the previous section, but instead of
representing a canonicalized term as a single sorted list, we apply distributivity to transform the
term into a canonical sum-of-products form (e.g., x ∗ y + y ∗ z), where each product is a sorted list
of atoms. Our sorting puts constants on the outside of each product (e.g., (x ∗ y) ∗ 3, not (x ∗ 3) ∗ y),
since the SMT solver’s linear arithmetic engine expects a sum of values multiplied by constants.
This enables the SMT solver’s linear reasoning to simplify ((x ∗y) ∗ 3) ∗ 2 + (x ∗y) ∗ (−1) to (x ∗y) ∗ 5,
for example. Finally, the correctness lemma relates the computed sum-of-sorted-products form to
the denotation of the original term:
val canon_correct #a #b (p:permute b) (pc:permute_correct p) (r:csr a) (vm:vmap a b) (e:exp) :
Lemma (denote1 r vm e == denote2 p r vm (exp_to_sum e))

While similar reflective tactics have been built before for other proof assistants (Barras et al.),
the main novelty here is using our commutative semi-ring tactic only to deal with non-linear
arithmetic, while still making good use of the SMT solver’s support for linear arithmetic.
5

CASE STUDY: SEPARATION LOGIC

Separation logic provides another challenging case study for metaprogramming in F⋆ ; the main
obstacle for SMT-only proofs being the inference of heap frames. To this end, we present an
encoding of separating conjunction and the frame rule in F⋆ , using metaprogramming to automate
those parts of the proofs that would be challenging for the SMT solver, i.e. inference of the heap
frames, while leaving rest of the proof obligations (involving classical logical connectives and even
inductive predicates) for SMT.

Meta-F⋆ : Metaprogramming and Tactics in an Effectful Program Verifier
5.1

19

Setting up the heap model and STATE effect

We first set up the STATE effect in F⋆ , such that the WP calculus of the effect encodes separation
logic style framing of heaps. We implement a heap model with the following interface:
type heap
type memory
type ref (a:Type) :Type
val def: memory → prop
val (emp): memory
val (7→): #a:Type → r:ref a → x:a → memory
val (•): memory → memory → memory

The above interface is largely standard: emp is the empty memory, r 7→ x is the singleton memory
mapping the reference r to a value x, and m1 • m2 is the union of two memories that is defined only
for non-overlapping memories (we use the def predicate to distinguish defined memories from
undefined ones). The interface also provides a set of standard algebraic laws (e.g., that (emp,•) form
a partial commutative monoid), and lemmas about the def predicate. Under the hood, our model
implements heap as a pair of a freshness counter and a function from addresses of references to
values; and memory as an optional function from addresses of references to values. We make this
distinction between heaps and (potentially undefined) memories, so as to directly build on this
heap model when extending the work presented here to support allocation and deallocation.
Next, we define a STATE effect in F⋆ . The basic setup is similar to the default state effect of F⋆
(Ahman et al. 2018): the precondition is a predicate on the memory of the input heap, and the
postcondition is a predicate on the return value and the memory of the output heap:
type st_pre = memory → prop
type st_post (a:Type) = a → memory → prop
type st_wp (a:Type) = st_post a → st_pre

The main departure from F⋆ ’s default state effect is in the specification of command footprints,
i.e., in their WPs. In F⋆ ’s default state effect, the footprints of commands are specified using the
custom modifies predicate on the entire input and output heaps. In contrast, in this heap model
each command is specified only in terms of its small footprint, removing the need for the modifies
predicate. For example, the read and write actions have the following specifications in our model:
let read_wp (#a:Type) (r:ref a) = λpost m0 → ∃x. m0 == r 7→ x ∧ post x m0
let write_wp (#a:Type) (r:ref a) (y:a) = λpost m0 → ∃x. m0 == r 7→ x ∧ post () (r 7→ y)

To accommodate tactic-based automation, we prescribe a style for user-defined procedures where
the annotated type explicitly provides the given procedure’s footprint, e.g.,
let swap_wp (r1 r2 :ref nat) = λpost m0 → ∃x y. m0 == r1 7→ x • r2 7→ y ∧ post () (r1 7→ y • r2 7→ x)

Given these small footprint style specifications, our separation logic library then inserts wrappers
around them to perform the framing of the memory of the input heap using the following functions:
(∗ p is the postcondition on the whole memory, m1 is the frame, m is the output memory of a command ∗)
(∗ it frames the postcondition on the whole memory to a postcondition on the command's output memory ∗)
let frame_post (#a:Type) (p:post a) (m1 :memory) :post a = λx m → def (m • m1 ) ∧ p x (m • m1 )
(∗ wp is the small footprint style WP, post is the framed postcondition ∗)
(∗ it partitions the memory, applies wp to (post m1 ) and m0 , where m1 is the frame and m0 is the footprint ∗)
let frame_wp (#a:Type) (wp:st_wp a) (post:memory → prop) (m:memory) =
∃m0 m1 . def (m0 • m1 ) ∧ m == (m0 • m1 ) ∧ wp (post m1 ) m0

20

Martínez et al.

(∗ the wrapper, it frames the postcondition and the small footprint style WP ∗)
let wrap_wp (#a:Type) (wp:st_wp a) = λpost m → frame_wp wp (frame_post post) m

As a result, the (wrapped) specification for assignment is:
val (:=): #a:Type → r:ref a → x:a → STATE unit (wrap_wp (write_wp r v))

In the expanded form, the specification of assignment looks as follows:
∃m1 x. def (r 7→ x • m1 ) ∧ m0 == r 7→ x • m1 ∧ def (r 7→ y • m1 ) ∧ post () (r 7→ y • m1 )

It requires the caller to prove (1) that there exists a frame m1 such that the input memory m0 == r 7→
x • m1 , where r is the footprint of the assignment command, and (2) that the postcondition is true of
the output memory r 7→ y • m1 . This is analogous to the frame rule in separation logic: m1 is joined
with r 7→ y as is. As such, the WPs of the basic commands (!, :=, and procedure calls) mimic the
small-footprint style common in separation logic, while explicitly framing out rest of the memory.
These commands are combined using bind which simply performs sequencing.
We also prove the presented STATE effect specification sound, by implementing the basic commands, bind, and return using the following natural underlying heap-passing representation:
let st (a:Type) (wp:st_wp a) =
post:post a → h0:heap{wp post h0.mem} → squash (x_h:(a ∗ heap){post (fst x_h) (snd x).mem})

5.2

Simple proof automation for straight-line code

We implement a proof-of-concept sl_auto tactic that combines syntax inspection of the proof goals
with the commutative monoid tactic from Section 4.1 to infer the required heap frames. Combined
with SMT-based automation for the rest, sl_auto makes proofs of straight-line code blocks automatic.
Generalizing it to handle branching and (annotated) recursive calls is future work. Indeed, the space
of heuristics for efficient automation of separation logic is large and we have only just scratched
the surface of it. Still the generality of Meta-F⋆ should allow us to grow the sophistication of the
sl_auto tactic with time and experience.
We explain the main idea of sl_auto with the help of an example. Consider the following program:
let read_one (r1 r2 :int) :STATE int (λ p h → ∃x y. h == r1 7→ x • r2 7→ y ∧ p y h) by sl_auto = !r2

Meta-F⋆ computes the WP of the body as wrap_wp (read_wp r2 ). The proof obligation is then to
show that the annotated WP subsumes this computed WP. After performing a sufficient number of
intros(), we are left with the goal wrap_wp (read_wp r2 ) p (r1 7→ x • r2 7→ y).
Recall from the previous section that framing of the memory of the input heap is done at the
basic commands using frame_wp. Relying on this structure of WPs, sl_auto unfolds the goal, one
step at a time, until it reaches a frame_wp. In our example, one unfolding of wrap_wp gives us:
frame_wp (read_wp r2 ) (frame_post p) (r1 7→ x • r2 7→ y)

At this point sl_auto has to partition the input memory r1 7→ x • r2 7→ y into the read command’s
footprint and the remaining frame. To do so, (∗1∗) sl_auto syntactically inspects the first argument
of frame_wp to compute the set of references that the current command requires—for read_wp and
write_wp this is simply the given reference. Then, (∗2∗) sl_auto builds a memory expression joining
the singleton memory expressions mapped to to unification variables, and one unification variable
for the rest of the memory. In our example, this results in r2 7→ ?u1 • ?u2 .
Next, (∗3∗) sl_auto builds a goal that equates r2 7→ ?u1 • ?u2 with the third argument of frame_wp,
i.e., the initial memory (r1 7→ x • r2 7→ y in this case). After doing a cut with this new goal (∗4∗), the
proof state now has this additional goal, and the equality in the context of the original goal.

Meta-F⋆ : Metaprogramming and Tactics in an Effectful Program Verifier

21

Next, (∗5∗) sl_auto instantiates the commutative monoid tactic with (emp,•), and uses it to solve the
equality goal. Once this goal is solved, the unification variables are properly instantiated, and the
context of the original goal contains the solution to the framing problem. The tactic then proceeds
to the next frame. We illustrate the above discussion with the sl_auto code snipped below:
let fp_refs = footprint_of arg1 in (∗1∗)
let fp = build_fp_from_refs fp_refs in
let frame = uvar_env (cur_env ()) None in
let hp = join fp frame in (∗2∗)
let new_goal = equate arg3 hp in (∗3∗)
let heq = tcut new_goal in (∗4∗)
flip();
canon_monoid_sl fp_refs; (∗5∗)
trefl();
...

5.3

Inductive proofs for linked lists

Using tactics we have also written more advanced, but for now manual inductive proofs for programs
operating on mutable singly linked lists. To this end, we first define the slist type as follows:
type listcell = | Cell: hd:nat → tl:slist → listcell a
and slist = option (ref listcell)
let null :slist = None

In addition to slist, we also define an inductive predicate valid, such that valid l fl m holds when
the memory m contains exactly the linked list l representing the (standard inductive) functional list
fl. With these definitions in place, we then verify several operations on linked lists. For example,
we verify that the length function returns the correct length and does not change the heap:
let rec length (l:slist) :STATE int (λ p m0 → ∃fl. valid l fl m0 ∧ p (List.length fl) m0 ) =
match l with
| None → 0
| Some r → let Cell _ tl = !r in 1 + length tl

As another example, we prove a tail-recursive implementation of rev to be correct and that it
does not perform any allocation (rev_append is an auxiliary function whose specification we elide):
let rev (l:slist) :STATE slist (λ p m0 → ∃fl. valid l fl m0 ∧
(∀ m1 r. (m0 .dom = m1 .dom ∧ valid r (List.rev fl) m1 ) =⇒ p r m1 ))
= rev_append l null

We also prove the correctness of slist append. All the proofs use tactics to apply the induction principle for lists, work through the VC instantiating heap frames, and send all other goals to the SMT.
In addition to definedness proofs, the reasoning about folding/unfolding of List.rev, List.length, valid
etc. is also left to the SMT, demonstrating the power of combining metaprogramming and SMT.
5.4

Ongoing and related work

We are working on extending the separation logic support in Meta-F⋆ along several dimensions.
We have already implemented a richer heap model and a corresponding st a wp representation with
support for both allocation and deallocation; we are working on extending sl_auto to support these
operations. Here the basic idea is to thread through a source of freshness in the specifications, while
providing library support to prove the definedness of the final memories. We are also working on

22

Martínez et al.

extending the sl_auto automation to inductive types and predicates. Finally, we also plan to extend
the supported logical connectives with −∗ (though automation is unlikely), and more generally,
extend our work from sequential computations and concrete memories to concurrency and general
partial commutative monoids (Jensen and Birkedal 2012; Krebbers et al. 2017).
Regarding other works on automating separation logic proofs, Botinčan et al. (2009) show how to
extend the jStar separation logic tool with SMT-based automation for discharging proof obligations
involving classical logical connectives. Compared to their work, we do not start with a separation
logic specific prover but instead with a general-purpose program verification tool, demonstrating
that the added power of metaprogramming allows it to be naturally turned into a separation logic
prover. As another example of work in this general area, Piskac et al. (2013, 2014) demonstrate that
certain specific quantifier-free fragments of separation logic, specifically of linked lists and mutable
trees, can in fact be fully automated using SMT solvers via translations of these fragments to logics
of graph reachability for which SMT decision procedures exist.
6

CASE STUDY: METAPROGRAMMING VERIFIED EFFECTFUL PROGRAMS

Besides proving or generating pure terms, the programmer may also use Meta-F⋆ to generate F⋆
terms with arbitrary effects. In this section, we show how Meta-F⋆ can be used to implement F⋆
program transformations from within F⋆ itself, in a correct-by-construction way. Specifically, using
a combination of dependent types, combinators and tactics, we produce low-level formatters of
network messages that are provably correct with respect to a high-level message format specification.
The metaprogrammed formatters are verified in Low⋆ , a fragment of F⋆ that extracts to efficient C
code (Protzenko et al. 2017).
6.1

Network message formats: A high-level spec

The correctness, interoperability, and security of networking protocols such as TLS (Dierks and
Rescorla 2008) depend on correctly formatting high-level messages into low-level network messages
in a format prescribed by the RFC. For instance, in TLS communication between a client and a
server starts by the client telling the server which cipher suites it supports for encryption and
decryption, asking the server to choose one among them. A high-level data type for cipher suites is
just a simple enumeration (partially listed below), and the standard specifies the low-level format
of these values.
type cipher_suite =
| TLS_ECDHE_ECDSA_WITH_AES_256_GCM_SHA384
| TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384
| TLS_DH_anon_WITH_RC4_128_MD5
| TLS_DH_anon_WITH_3DES_EDE_CBC_SHA

The formatting of these values is easy to write as a pure function in the output monad m
producing a byte sequence.
let print_cipher_suite_spec (c:cipher_suite) : m unit =
if c = TLS_ECDHE_ECDSA_WITH_AES_256_GCM_SHA384 then (print_char 0xc0z;; print_char 0x2cz)
else if c = TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384 then (print_char 0xc0z;; print_char 0x30z)
else begin
print_char 0x00z ;;
if c = TLS_DH_anon_WITH_RC4_128_MD5 then print_char 0x18z
else print_char 0x1Bz
end
let rec print_list_cipher_suite_spec (l: list cipher_suite) : m unit =

Meta-F⋆ : Metaprogramming and Tactics in an Effectful Program Verifier

23

if l = [] then ret () else (print_cipher_suite_spec (hd l);; print_list_cipher_suite_spec (tl l))

While the formatter implementation using the m monad is simple, easy to program, and easy to
audit for conformance to the standards document, it is also very inefficient—it dynamically allocates
sequences of bytes and performs a copy at each bind operation. One can manually program more
efficient formatters in a low-level language like C, but doing so sacrifices the ease of programming,
auditability, and safety guarantees provided by the functional implementation above. If only we
could metaprogram a low-level, efficient formatter that is provably equivalent to this specification.
6.2

Correct-by-construction transformations on monadic code

We now show how Meta-F⋆ can automatically derive such an efficient, low-level implementation
from a high-level specification, automatically proving safety without any help from the user. We
proceed in two steps: first, we generate a sz function that determines how many bytes the formatted
output will occupy; second, we generate a low-level printer that, when given a buffer of sufficient
size, proceeds to format the input into it.
To begin with, we write a tactic for transforming the high-level printer (given by a term in the
monad m) into a sz function in a monad for computing the length of formatted message. Since
our goal is to extract a C program, we compute this length as a 32-bit integer, aborting in case
of arithmetic overflow. In particular, we define a “replacement” monad m_sz parameterized over
the original printer f, capturing the correctness criterion that we have f':m_sz f only if f' correctly
computes the size of the output of f, so long as its length fits in a 32-bit integer.3
type m_sz (τ : Type) (f: m τ ) = r:option (τ ∗ U32.t) { let res, log = f () in
match r with None → length log > 231 − 1 | Some (res', len) → res == res' ∧ length log == U32.v len }

We then define a metaprogram mk_sz that transforms code from m to m_sz, recursively traversing
the original term, using inspect and pack. It replaces each original combinator in the m monad
(print_char, bind, etc.) by its counterpart in m_sz. The print_char combinator in the length monad
accumulates 1ul. In the case that two computations f1 and f2 are successful, the bind combinator
returns if U32.max_int -len1 < len2 then None else Some (res2, len1 + len2). Thus, the generated program
reasons about overflow by construction, meaning that the user need not be concerned with proofs
about arithmetic overflow. In particular, if the length overflows a 32-bit integer, the size computation
fails and returns None.
We actually implemented the mk_sz tactic in a modular way as a set of transformations to be
used in a trial-and-error fashion:
let rec compile (e: env) (ty: term) (t: term) : Tac term = first [
(λ () → compile_ret t);
(λ () → compile_bind e ty t compile);
(λ () → compile_print_char t);
(λ () → compile_fvar e ty t (compile e));
(λ () → compile_ifthenelse ty t (compile e));
]
let mk_sz τ (t: m τ ) : Tac unit = exact_guard (compile (cur_env ()) (quote τ ) (quote t))

Each transformation leverages inspect and pack: basically, for a given transformation, its corresponding tactic extracts the head symbol t0 of t, and inspects it. If t0 is a free variable corresponding to a m
combinator, then it is replaced with its m_sz counterpart (thus do compile_ret and compile_print_char
our implementation, we actually choose to implement m_sz in continuation-passing style, to avoid proliferation of
option values when managing overflow in the extracted code.
3 In

24

Martínez et al.

work), and any m-monadic argument is recursively compiled (as does compile_bind). If t0 is an
if-then-else expression, then compile_ifthenelse replaces it with the ifthenelse_sz combinator.
The following mk_sz invocation produces a term that computes the length needed to format its
input; the generated term is type-checked by F⋆ , ensuring its correctness and memory safety.
let print_cipher_suite_sz (c: cipher_suite) : m_sz (print_cipher_suite_spec c) =
synth (mk_sz (print_cipher_suite_spec c))

The generated term could be at the risk of containing several applications of higher-order
combinators. However, F⋆ is capable of performing enough inlining to ensure that the generated
print_cipher_suite_sz is entirely first-order. This means that the function is eligible for an optimized
compilation scheme to C using the KreMLin compiler (Protzenko et al. 2017).
Transforming into the formatter monad. To generate a stateful formatter in the m_st monad from
a high-level specification given in the m monad, we use the same technique as above.
Specifically, we say that an implementation f' : m_st f is correct with respect to a specification
f: m τ if f' is a stateful function, which when given as argument a buffer b large enough to hold the
output of f, writes the expected output of f in b, then returns a pointer to the first un-written byte
of b (which allows chaining combinators). We formalize this specification using F⋆ ’s ST monad,
which models the C memory model, ensuring that buffers can be compiled using C arrays.
type m_st τ (f: m τ ) = (b: buffer U8.t) → ST (τ ∗ buffer U8.t)
(requires (λ h → live h b ∧ Buffer.length b ≥ Seq.length (snd (f ()))))
(ensures (λ h (r', b') h' →
live h' b ∧ modifies1 b h h' ∧ (∗ memory safety and frame ∗)
let (r, log) = f () in
let len32 = U32.uint_to_t (Seq.length log) in
r' == r ∧ as_seq h' (sub b 0ul len32) == log ∧ (∗ λctional correctness ∗)
b' == sub b len32 (U32.uint_to_t (Buffer.length b − Seq.length log ))))

The code generation pattern is very similar to mk_sz and we use in fact the same tactic with a
different set of replacement combinators. The generated formatter is shown to be memory safe
(both temporal and spatial memory safety) and correct by construction; and the user does not write
a single proof for it.
Rewriting the generated code for efficiency. By default, the generated formatter is a tail-recursive
function. This can be inefficient, and thus we may wish to compile it to a proper C loop.
To this end, we enrich the original monad m with a recursive do_while combinator, and provide implementations of it in the m_sz and m_st monads using C loops, as exposed by the KreMLin compiler;
these implementations are shown correct with regards to the original recursive specification.
We then define another Meta-F⋆ tactic and use it to transform tail-recursive specification functions in the original monad m into calls to the newly added do_while combinator. Once again,
F⋆ verifies that the generated code is correct. As a result, we then get optimized versions of
print_cipher_suite_sz and print_cipher_suite_st “for free”, without the user ever having to worry about
proving that the transformation from a tail-recursive function to a do-while combinator is correct.
7

RELATED WORK

Metaprogramming has a long and rich history, starting from LISP (McCarthy 1962). We focus
primarily on the use of metaprogramming in program verification tools and proof assistants.
Program verifiers for imperative languages (Barnett et al. 2005a,b; Burdy et al. 2005; Flanagan
et al. 2013; Leino and Nelson 1998) traditionally provide little support for interactive proofs. They

Meta-F⋆ : Metaprogramming and Tactics in an Effectful Program Verifier

25

instead rely on SMT solvers and other first-order logic theorem provers for discharging VCs
automatically. When SMT automation fails, however, the user has to step in and narrow down
the problem by adding extra assertions that can then also guide the SMT solver towards finding a
proof. Dafny (Amin 2013; Amin et al. 2014; Leino 2010) and F⋆ (Swamy et al. 2016) additionally
allow users to prove inductive lemmas by writing pure recursive functions that return a trivial
result (unit), but that can be called for the logical side-effect of their post-condition. Similar
ideas have recently been used in Liquid Haskell (Vazou et al. 2017, 2018). While this can be
very useful for overcoming the SMT solver’s limitations, it can be very difficult to figure out
what lemmas to prove without a way to inspect the current proof goal. Also, this proof style
can be very tedious in practice without metaprogramming support: for instance the non-linear
arithmetic proofs we do automatically in §4.2 used to take several dozens of manual invocations
to lemmas such as associativity, commutativity, and distributivity. Recognizing this, tools such as
Why3 (Filliâtre and Paskevich 2013) allow verification conditions to be discharged not just using
automatic theorem provers, but also using tactic proofs in Coq, but this involves stepping out
of the Why3 language. Grov and Tumas (2016) present Tacny, a tactic framework for Dafny, a
scripting layer on top of Dafny and separate from it that can be used to generate fragments of
Dafny code to be verified by Dafny’s existing SMT-based tool chain. While Tacny can be used
to automate some verification tasks in Dafny, it is still heavily reliant on SMT solving as its only
engine for proofs. Other program verification frameworks (Krebbers et al. 2017; Nanevski et al.
2008a,b) value metaprogramming and tactics so much that they build directly on top of Coq, even if
this means giving up on SMT automation altogether. In contrast, Meta-F⋆ aims at combining both
the benefits of SMT automation and those of tactic proofs as an embedded DSL within a general
purpose programming and verification-oriented host language, F⋆ .
Tactics and metaprogramming are the workhorse of interactive theorem provers, starting with
Milner’s Edinburgh LCF (Gordon et al. 1979) that introduced ML as its metaprogramming language.
HOL, Isabelle, and Coq still use ML even today to various extents for some of their metaprogramming
tasks. Most Isabelle proofs are, however, written in Isar, a specialized language for structured
proofs (Wenzel 2017). Analogously, most Coq proofs are written in Ltac (Delahaye 2000; Pédrot
2016), a small untyped functional language with primitive support for pattern-matching and backtracking.
Meta-F⋆ builds instead on a recent idea in the space of dependently typed proof assistants
(Christiansen and Brady 2016; Ebner et al. 2017; Ziliani et al. 2015, 2016): rather than defining a
separate language for metaprogramming and tactics, one can reuse the purely-functional programming language of the proof assistant. This idea first appeared in the Mtac tactic framework that
proposes to program tactics in Coq using an abstract monad with primitive actions such as pattern
matching (Ziliani et al. 2015, 2016). This has many generic benefits including reusing the standard
library, IDE support, and type checker of the proof assistant. Taking this idea to its extreme, Mtac
proposes to prove the partial correctness of tactics using dependent types by a shallow embedding
into Coq. While proving tactics correct can be sometimes appealing (as proofs by reflection show),
requiring that all tactics are statically verified to either solve the goal or fail restricts the kind
of metaprogramming tasks one can solve with Mtac. Also proving tactics correct can be very
challenging (if at all possible), which means that key tactics in Mtac are still only typed with a very
uninformative type (basically an existential package).
Meta-F⋆ ’s design is instead more closely inspired by the metaprogramming frameworks of
Idris (Christiansen and Brady 2016) and Lean (Ebner et al. 2017), which provide a deep embedding
of terms that can be inspected and constructed at will without dependent types getting in the way.
F⋆ ’s support for effects allows tactics to be written in ML-style, familiar since Milner’s Edinburgh
LCF (Gordon et al. 1979) and that we believe still provides a good trade-off between expressiveness

26

Martínez et al.

and static guarantees for metaprograms. Beyond benefiting from F⋆ ’s good support for effects,
Meta-F⋆ tactics are also well-integrated with F⋆ ’s weakest precondition calculus and SMT solver,
which poses unique challenges and opportunities that we addressed in this paper.
Our approach of generating verified low-level formatters (§6) is related to Amin and Rompf’s
2017 work on LMS-Verify. They use metaprogramming facilities in Scala to generate efficient C code
together with code annotations and safety specifications in a form that can be checked by FramaC (Cuoq et al. 2012), an SMT-based C verifier. In contrast, we generate correct-by-construction
imperative Low⋆ code, which is verified by F⋆ before being translated to C by the (trusted) KreMLin
compiler. LMS-Verify has also been used to generate efficient and safe HTTP parsers, a larger-scale
effort than the network message formatters than we have currently done.
8

CONCLUSIONS

Research in program verification seeks to balance tradeoffs among automation and expressiveness.
Whereas tactic-based interactive proofs can handle highly expressive logics, all automation is in
the hands of the tactic author. On the other hand, SMT-based program verifiers can provide good
automation for comparatively weak logics, but offer little recourse when verification fails. A design
that allows picking the right tool, at granularity down to each verification sub-task, is a worthy
area of exploration, one that we feel has been underexplored. Meta-F⋆ aims to fill this gap.
Our experience with Meta-F⋆ so far has been encouraging. We have used it effectively to
significantly simplify proofs that were hard to author and had become unmaintainable, e.g., those
involving non-linear arithmetic in cryptography. We have explored proofs in logics, including
separation logic, that were previously impractical in F⋆ . And, although not always applicable,
perhaps most appealing is our avoidance of manual proof altogether by metaprogramming correctby-construction low-level code. In all cases, we use metaprogramming and tactics in concert with
SMT solving, playing to the strengths of each and steering clear of their weaknesses.
ACKNOWLEDGMENTS
We thank the Project Everest team for many useful discussions. Guido Martínez’, Nick Giannarakis’,
Monal Narasimhamurthy’s, and Zoe Paraskevopoulou’s work was done, in part, while interning at
Microsoft Research. Clément Pit-Claudel’s work was in part done during an internship at Inria Paris.
The work of Danel Ahman, Victor Dumitrescu, and Cătălin Hriţcu is supported by the MSR-Inria
Joint Centre and the European Research Council under ERC Starting Grant SECOMP (715753).
REFERENCES
D. Ahman, C. Hriţcu, K. Maillard, G. Martínez, G. Plotkin, J. Protzenko, A. Rastogi, and N. Swamy. Dijkstra monads for free.
POPL. 2017.
D. Ahman, C. Fournet, C. Hriţcu, K. Maillard, A. Rastogi, and N. Swamy. Recalling a witness: Foundations and applications
of monotonic state. PACMPL, 2(POPL), 2018.
N. Amin. How to write your next POPL paper in Dafny. Microsoft Research talk, 2013.
N. Amin and T. Rompf. LMS-Verify: Abstraction without regret for verified systems programming. POPL. 2017.
N. Amin, K. R. M. Leino, and T. Rompf. Computing with an SMT solver. TAP, 2014.
M. Barnett, B. E. Chang, R. DeLine, B. Jacobs, and K. R. M. Leino. Boogie: A modular reusable verifier for object-oriented
programs. FMCO. 2005a.
M. Barnett, R. DeLine, M. Fähndrich, B. Jacobs, K. R. M. Leino, W. Schulte, and H. Venter. The spec# programming system:
Challenges and directions. VSTTE. 2005b.
B. Barras, B. Grégoire, A. Mahboubi, and L. Théry. Coq reference manual; chapter 25: The ring and field tactic families.
Available at https://coq.inria.fr/refman/ring.html.
D. J. Bernstein. The Poly1305-AES message-authentication code. In Proceedings of Fast Software Encryption, 2005.
K. Bhargavan, B. Bond, A. Delignat-Lavaud, C. Fournet, C. Hawblitzel, C. Hriţcu, S. Ishtiaq, M. Kohlweiss, R. Leino, J. Lorch,
K. Maillard, J. Pang, B. Parno, J. Protzenko, T. Ramananandro, A. Rane, A. Rastogi, N. Swamy, L. Thompson, P. Wang,

Meta-F⋆ : Metaprogramming and Tactics in an Effectful Program Verifier

27

S. Zanella-Béguelin, and J.-K. Zinzindohoué. Everest: Towards a verified, drop-in replacement of HTTPS. SNAPL, 2017.
B. Bond, C. Hawblitzel, M. Kapritsos, K. R. M. Leino, J. R. Lorch, B. Parno, A. Rane, S. Setty, and L. Thompson. Vale: Verifying
high-performance cryptographic assembly code. In Proceedings of the USENIX Security Symposium, 2017.
M. Botinčan, M. Parkinson, and W. Schulte. Separation logic verification of c programs with an smt solver. Electron. Notes
Theor. Comput. Sci., 254:5–23, 2009.
L. Burdy, Y. Cheon, D. R. Cok, M. D. Ernst, J. R. Kiniry, G. T. Leavens, K. R. M. Leino, and E. Poll. An overview of JML tools
and applications. STTT, 7(3):212–232, 2005.
D. R. Christiansen and E. Brady. Elaborator reflection: extending idris in idris. In J. Garrigue, G. Keller, and E. Sumii,
editors, Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara,
Japan, September 18-22, 2016. 2016.
P. Cuoq, F. Kirchner, N. Kosmatov, V. Prevosto, J. Signoles, and B. Yakobowski. Frama-c: A software analysis perspective. In
Proceedings of the 10th International Conference on Software Engineering and Formal Methods. 2012.
L. M. de Moura and N. Bjørner. Z3: an efficient SMT solver. TACAS. 2008.
D. Delahaye. A tactic language for the system Coq. In M. Parigot and A. Voronkov, editors, Logic for Programming and
Automated Reasoning, 7th International Conference, LPAR 2000, Reunion Island, France, November 11-12, 2000, Proceedings.
2000.
T. Dierks and E. Rescorla. The Transport Layer Security (TLS) Protocol Version 1.2. IETF RFC 5246, 2008.
G. Ebner, S. Ullrich, J. Roesch, J. Avigad, and L. de Moura. A metaprogramming framework for formal verification. PACMPL,
1(ICFP):34:1–34:29, 2017.
J.-C. Filliâtre and A. Paskevich. Why3 — where programs meet provers. ESOP. 2013.
C. Flanagan, K. R. M. Leino, M. Lillibridge, G. Nelson, J. B. Saxe, and R. Stata. PLDI 2002: Extended static checking for java.
SIGPLAN Notices, 48(4S):22–33, 2013.
G. Gonthier. Formal proof–the four-color theorem. Notices of the AMS, 55(11):1382–1393, 2008.
M. J. C. Gordon, R. Milner, and C. Wadsworth. Edinburgh LCF: A Mechanized Logic of Computation. Springer-Verlag, 1979.
B. Grégoire and A. Mahboubi. Proving equalities in a commutative ring done right in Coq. In J. Hurd and T. F. Melham,
editors, Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25,
2005, Proceedings. 2005.
G. Grov and V. Tumas. Tactics for the dafny program verifier. In M. Chechik and J.-F. Raskin, editors, Tools and Algorithms
for the Construction and Analysis of Systems. 2016.
C. Hawblitzel, J. Howell, J. R. Lorch, A. Narayan, B. Parno, D. Zhang, and B. Zill. Ironclad apps: End-to-end security via
automated full-system verification. In J. Flinn and H. Levy, editors, 11th USENIX Symposium on Operating Systems Design
and Implementation, OSDI ’14, Broomfield, CO, USA, October 6-8, 2014. 2014.
C. Hawblitzel, J. Howell, M. Kapritsos, J. R. Lorch, B. Parno, M. L. Roberts, S. T. V. Setty, and B. Zill. Ironfleet: proving safety
and liveness of practical distributed systems. Commun. ACM, 60(7):83–92, 2017.
J. B. Jensen and L. Birkedal. Fictional separation logic. ESOP. 2012.
R. Krebbers, R. Jung, A. Bizjak, J. Jourdan, D. Dreyer, and L. Birkedal. The essence of higher-order concurrent separation
logic. ESOP. 2017.
K. R. M. Leino. Dafny: An automatic program verifier for functional correctness. LPAR. 2010.
K. R. M. Leino and G. Nelson. An extended static checker for modular-3. In K. Koskimies, editor, Compiler Construction, 7th
International Conference, CC’98, Held as Part of the European Joint Conferences on the Theory and Practice of Software,
ETAPS’98, Lisbon, Portugal, March 28 - April 4, 1998, Proceedings. 1998.
J. McCarthy. LISP 1.5 Programmer’s Manual. The MIT Press, 1962.
L. Moura and N. Bjørner. Efficient e-matching for SMT solvers. In Proceedings of the 21st International Conference on
Automated Deduction: Automated Deduction. 2007.
A. Nanevski, G. Morrisett, A. Shinnar, P. Govereau, and L. Birkedal. Ynot: dependent types for imperative programs. ICFP.
2008a.
A. Nanevski, J. G. Morrisett, and L. Birkedal. Hoare type theory, polymorphism and separation. JFP, 18(5-6):865–911, 2008b.
A. Nogin. Quotient types: A modular approach. TPHOLs. 2002.
P.-M. Pédrot. Ticking like a clockwork: the new Coq tactics. CoqHoTT-minute blog, 2016.
R. Piskac, T. Wies, and D. Zufferey. Automating separation logic using smt. In Proceedings of the 25th International Conference
on Computer Aided Verification. 2013.
R. Piskac, T. Wies, and D. Zufferey. Automating separation logic with trees and data. In Proceedings of the 16th International
Conference on Computer Aided Verification - Volume 8559. 2014.
J. Protzenko, J.-K. Zinzindohoué, A. Rastogi, T. Ramananandro, P. Wang, S. Zanella-Béguelin, A. Delignat-Lavaud, C. Hriţcu,
K. Bhargavan, C. Fournet, and N. Swamy. Verified low-level programming embedded in F*. PACMPL, 1(ICFP):17:1–17:29,
2017.

28

Martínez et al.

J. C. Reynolds. Separation logic: A logic for shared mutable data structures. In Proceedings of the 17th Annual IEEE Symposium
on Logic in Computer Science. 2002.
N. Swamy, J. Weinberger, C. Schlesinger, J. Chen, and B. Livshits. Verifying higher-order programs with the Dijkstra monad.
PLDI , 2013.
N. Swamy, C. Hriţcu, C. Keller, A. Rastogi, A. Delignat-Lavaud, S. Forest, K. Bhargavan, C. Fournet, P.-Y. Strub, M. Kohlweiss,
J.-K. Zinzindohoué, and S. Zanella-Béguelin. Dependent types and multi-monadic effects in F*. POPL. 2016.
N. Vazou, E. L. Seidel, R. Jhala, D. Vytiniotis, and S. L. P. Jones. Refinement types for Haskell. ICFP, 2014.
N. Vazou, L. Lampropoulos, and J. Polakow. A tale of two provers: verifying monoidal string matching in Liquid Haskell
and Coq. In I. S. Diatchki, editor, Proceedings of the 10th ACM SIGPLAN International Symposium on Haskell, Oxford,
United Kingdom, September 7-8, 2017. 2017.
N. Vazou, A. Tondwalkar, V. Choudhury, R. G. Scott, R. R. Newton, P. Wadler, and R. Jhala. Refinement reflection: complete
verification with SMT. PACMPL, 2(POPL):53:1–53:31, 2018.
P. Wadler. Views: A way for pattern matching to cohabit with data abstraction. In Proceedings of the 14th ACM SIGACTSIGPLAN Symposium on Principles of Programming Languages. 1987.
M. Wenzel. The Isabelle/Isar reference manual. Available at http://isabelle.in.tum.de/doc/isar-ref.pdf, 2017.
B. Ziliani, D. Dreyer, N. R. Krishnaswami, A. Nanevski, and V. Vafeiadis. Mtac: A monad for typed tactic programming in
Coq. J. Funct. Program., 25, 2015.
B. Ziliani, Y. Régis-Gianas, and J.-O. Kaiser. The next 700 safe tactic languages. Work in progress, 2016.
J.-K. Zinzindohoué, K. Bhargavan, J. Protzenko, and B. Beurdouche. HACL*: A verified modern cryptographic library.
Cryptology ePrint Archive, Report 2017/536, 2017. http://eprint.iacr.org/2017/536.

