-
Notifications
You must be signed in to change notification settings - Fork 243
Qualifiers for definitions and declarations
- assume
- private
- abstract
- irreducible
- unfoldable
- inline
- new
- noeq
- unopteq
- logic
- reifiable
- reflectable
- opaque (deprecated ?)
- default (F# extraction only)
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).
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
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.
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 verified.
See, examples/metatheory/LambdaOmega.fst for many examples.
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.
The inline 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 inline 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:
inline 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]))
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. 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.
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*
The logic qualifier serves as a way to trigger an optimization in the SMT encoding by translating a term shallowly to SMT, rather than the default deep embedding. F* usually infers when to add this qualifier. (according to #638)
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.