Qualifiers for definitions and declarations

The qualifiers that one can use in front of a definition have been overhauled in the universes rewrite; as of 02/11/2016, the behavior described below is the one that corresponds to the --universes flag of F★.

Type qualifiers in the new universes-F★

The assume keyword binds an existentially-quantified, abstract variable. No further assumptions are made about it. The binding shall not be followed by a definition (i.e. no = … after assume type t or assume val x).

assume type t
assume val x: t

The new keyword, can only be used in conjunction with assume; it further states that the variable is distinct from all other variables. One can observe the difference by passing --log-smt-queries to F★.

assume new type t
assume new val x: t

The private keyword (on a type or let definition) states that the name will not be bound outside of the current module. This means that the user cannot refer to the type.

module Foo

private type t
val f: t → ...

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.

The abstract keyword is mutually exclusive with private; it hides a definition outside of the current module.

module Foo

abstract type t =
  | A of u

val f: x:t{is_A x} → ...

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

module Foo

assume type t
private val A: u → t
private val is_A: t → bool

Here, the type of f may refer not only to the type t, but also to its projectors/discriminators/constructors. Therefore, the user may not refer to is_A, but F★ still will, when manipulating the type of f.

The irreducible keyword indicates that a definition may never be reduced by F★'s type-normalization mechanism before being handed out to the SMT solver.

This is useful for the classic "trigger pattern":

irreducible type trigger (i: int) = true

type lemma = forall (arg: int).{:pattern (trigger arg)} trigger arg ==> ...

let my_proof =
  cut (trigger 3);
  ...

The unfoldable keyword correspond to the default case.

The inline keyword indicates that a type definition must always be reduced by F★. This is designed for power users that need specific improvements in verification performance.

Note:

If a specific type is modelized in F* one way (e.g. type array a = Seq.seq a) but realized at extraction-time in another way (e.g. type nonrec 'a array = 'a array), then the only way to make sure Seq.seq a does not appear in type annotations in extracted code is to make that type abstract.

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

Universes vs no universes

As of 02/11/2016, here's the correspondence between the new syntax explained above and the current syntax you get (without the --universes flag).

New syntax	Old (current) syntax
?	opaque logic type
?	opaque type
?	{val,type} t
?	assume {type,val} t
?	abstract {type,val} t

---