Skip to content

Qualifiers for definitions and declarations

Jump to bottom Edit New page
Jay Bosamiya edited this page Apr 8, 2020 · 24 revisions

Qualifiers in F*

List of qualifiers

See also Custom-attributes for a list of custom attributes (e.g. [@ "c_inline"], [@ "inline_let"]).

assume

The assume qualifier declares the existence of an element of a particular type. This can be useful for modeling or when declaring the existence of fragments of an incomplete program.

The general form is

assume val x: t

which assumes the existence of an element x of the type t. Aside from assuming that the type t is non-empty, this introduces no further assumptions about x.

As a shorthand, one can also write

assume type t

instead of

assume val t : Type

In both cases, the binding shall not be followed by a definition (i.e. no = … after assume type t or assume val x).

Note that a different use of assume is to introduce an axiom for the SMT :

assume MyAxiom : forall x y. x == y ==> y == x

In that case the name MyAxiom cannot be used in the rest of the program but the axiom is provided to the SMT solver.

private

The private qualifier states that the name will not be bound outside of the current module.

module Foo
private type t = int
assume val f: t → Tot int
module Bar
open Foo
let g = f 0

The user, outside of module Foo, cannot refer to the type t; the type-checker will still refer to it, though, when manipulating the type of f. As such, a client module can apply f 0 and the program will type check, since the type-checker knows that t = int.

Note, a common misunderstanding is to use the private qualifier to enforce abstraction---use the abstract qualifier for that, described next. The private qualifier is solely a mechanism to control namespaces. For example, consider:

module A
let t = 0
module B
private let t = true
module C
open A
open B
let f (x:int) = x + t //the t is resolved to A.t, despite B being opened

abstract

WARNING: DEPRECATED

The abstract qualifier: The qualified name is bound outside the scope of the module, but its definition is hidden.

As such, given:

module Foo
abstract type t = int
assume val f: t → Tot int

Another module Bar can refer to Foo.t but cannot rely on its definition as an int.

module Bar
open Foo
let g = f 0 //fails to type-check
let h (x:t) = f x //Bar can refer to Foo.t

In the case of inductively defined types (datatypes),

module Foo
abstract type t =
  | A of int

When outside of module Foo, the definition above is equivalent to:

module Foo

assume type t
private val A: int → t
private abstract val is_A: t → bool
private abstract val A._0: x:t{is_A x} → Tot int

As such, in another module Bar, the constructors, projectors and discriminators are not accessible.

Note: If a specific type is modeled in F* one way (e.g. type array a = ref (Seq.seq a)) but realized at extraction-time in another way (e.g. type nonrec 'a array = 'a array), then the recommended practice is to mark array a abstract so that the program does not rely on the definition used for modeling purposes only. Adding the abstract qualifier will also ensure that the type annotations in extracted code only refer to array a not to its definition.

irreducible

The irreducible qualifier indicates that a definition may never be reduced by F*'s normalizer nor by the SMT solver. In effect, irreducible makes a definition abstract immediately, even for the current module.

This is useful when the type of a variable carries all the information one wishes to reveal about it. Hiding the definition of that variable can improve the performance of the verification.

See, examples/metatheory/LambdaOmega.fst for many examples.

unfoldable

The unfoldable qualifier is the default qualifier on a definition. It states that both F*'s normalizer and the SMT solver may unfold the definition as needed for type-checking.

While it is hard to specify precisely when a definition may be unfolded, a useful rule of thumb is the following.

A unfoldable definition will be unfolded only if needed for checking that two terms unify or if one is a subtype of another. For example, consider

type nat = x:int{x >= 0}
let f (x:nat) : int = x

To check the body of f we need to prove that x:nat is a subtype of int, the annotated result type of f.

In this case, F* will unfold the definition of nat and check that x:int{x >= 0} is a subtype of int, which succeeds by refinement subtyping.

Note, in the annotation x:nat on the argument of f, the definition of nat is not unfolded, since it is not necessary for type-checking f. As such, in the context for the rest of the program, the type of f will appear as x:nat -> Tot int, rather than x:int{x >= 0} -> Tot int (although these two latter types are definitionally equal, since they are related by an unfolding).

unfold

The unfold qualifier indicates that a type definition must always be reduced by F*'s normalizer. This is designed for power users that need specific improvements in verification performance.

A generally useful pattern is to use the unfold qualifier when defining a higher-order predicate. This will ensure that F* normalizes any applications of that predicate before passing it to the SMT solver, making the program 'more first-order' for the SMT solver.

For example, to augment a post-condition in a stateful specification with an invariant, one can write:

unfold let with_inv (#a:Type) (inv:heap -> Type0) (post: (h0:heap -> a -> h1:heap -> Type0)) = 
  fun h0 res h1 -> inv h0 /\ inv h1 /\ post h0 res h1

And then use

x:ref int -> ST unit (requires some_invariant) (ensures (with_inv some_invariant (fun h0 () h1 -> h0[x] = h1[x]))

new

The new qualifier should rarely be used in a typical user program. The form assume new type t introduces a fresh element t : Type, distinct from all other types already in scope. In particular, the following assert succeeds if both t1 and t2 are marked as new:

assume new type t1
assume new type t2

let distinct () : Lemma (~(t1 == t2)) = ()

F*'s standard libraries use the new qualifier to configure F* with new type constants, e.g., the standard prelude of F*, prims.fst, contains assume new type int and assume new type string to introduce new type constants. If used carelessly in a user program, the new qualifier can easily make your context inconsistent.

noeq && unopteq

The noeq and unopteq qualifiers are related to decidable equality and is described in Deriving-hasEq-predicate-for-inductive-types,-and-types-of-equalities-in-F*

logic

The logic qualifier is deprecated.

reifiable && reflectable

The reifiable and reflectable qualifiers indicates if a new_effect_for_free obtained through the Djiksta monads for free elaboration should be able to reify and reflect computations.

inline_for_extraction

Affects both OCaml and KreMLin extraction. Its effect is to substitute occurrences of a definition by its body. When applied to stateful functions, F* will take care of introducing intermediate variables to hoist effectful expressions appropriately, and KreMLin will do its best to eliminate unnecessary intermediate variables in the generated C code.

When applied to a function that produces a type, has a similar effect of having KreMLin unfold the type-level function before extraction. This can have the effect of erasing spec-only arguments or revealing a function type, enabling extraction of some types that otherwise appear to be impossible to represent. (See FStarLang/kremlin#51 for an example that can be fixed with inline_for_extraction with no impact on verification).

This attribute is automatically added to inductive type projectors (eg, Some?.v).

noextract

Affects only KreMLin extraction, preventing it from extracting the body of a definition. (See https://github.com/FStarLang/FStar/issues/1221 for a tracking issue for expanding this behavior.) Beware that misusing noextract can break extraction. If you mark a definition as noextract and occurrences remain after partial evaluation, the extracted code will have a reference to an undeclared function.

Add a custom footer
Add a custom sidebar
Clone this wiki locally