1. Introduction🔗
Strata aims to provide a foundation for representing the semantics of programs,
specifications, protocols, architectures, and other aspects of large-scale
distributed systems and their components. It achieves this through languages of
two types. The first type, consisting of the single Strata Core language,
provides a central hub that can serve as a connection point between multiple
types of input artifact and multiple types of analysis, reducing the cost of
implementing N analyses for M languages from N*M to N+M.
The second type consists of numerous Strata dialects. The Dialect Definition
Mechanism, described
here,
provides a way to define the syntax and a simple type system for a dialect. At
the moment, dialects do not directly have semantics (though we may add a
mechanism for defining their semantics in the future) but instead are defined by
translation to or from Strata Core. Said another way, each of these dialects is
a different concrete way to write Strata programs, but all of these dialects are
ultimately represented internally using the same Core language.
Dialects are used to describe both the initial artifacts being analyzed by
Strata and more low-level representations of those artifacts used to communicate
with external reasoning tools such as model checkers or SMT solvers. In both
situations, Strata uses dialects as a mechanism for communicating with external
tools (either language front ends or generic automated reasoning tools like SMT
solvers).
The following "hourglass" diagram illustrates how various existing (blue) or
potential (gray) input dialects could be translated into Strata Core and then
into the input language for various back end tools. Solid lines indicate
translation paths that exist (though experimentally in the connection between
Strata Core and CBMC), and dotted lines indicate translations that illustrate
the sorts of use cases we expect Strata to support but that haven't yet been
implemented.
The Strata Core language is constructed using a few building blocks that can be
combined in different ways. This allows concrete dialects to systematically use
different combinations that still share the majority of their implementation. In
Lean (and in principle in most other source languages that could be used to
process Strata programs), the type system can enforce various structural
constraints, ensuring that only expected language constructs show up. The Strata
Core language itself consists of an imperative statement type parameterized by
an expression type, with various more fine-grained adjustments of other
parameters.
The two fundamental building blocks of Strata Core are a representation of
functional programs (Lambda), and a representation of imperative programs
(Imperative). The Lambda language is parameterized by a type system and a
set of built-in types and functions. The Imperative language is then
parameterized by the type of expressions it allows in conditions, assignments,
and so on. Currently, those expressions will almost always be some
instantiation of Lambda. Both Core building blocks are parameterized by a
metadata type, which by default is instantiated with a map from keys to
structured values that can contain expressions (typically from Lambda).
The remainder of this document is structured as follows:
-
Sections 2 and 3 describe Lambda and Imperative as generic, reusable
building blocks.
-
Section 4 describes how Strata Core assembles these blocks into a concrete
verification language with procedures, type declarations, functions, axioms,
lemmas, and programs.
The semantics of each layer — operational and denotational for Lambda, and
operational for Imperative — and how they compose to give meaning to Strata
Core programs, are described in a companion document,
The Strata Core Language Semantics.
We do not consider the Core language set in stone. It may evolve over time,
particularly to add new fundamental constructs, and this document will be
updated as it does.
2. Lambda🔗
The Lambda language is a standard but generic implementation of the lambda
calculus. It is parameterized by a type for metadata and the type of types
(which may be Unit, to describe the untyped lambda calculus). It includes the
standard constructs for constants, free and bound variables, abstractions, and
applications. In addition, it includes a special type of constant, an operator,
to represent built-in functions. It extends the standard lambda calculus by
allowing quantifiers (since a key use of the language is to write logical
predicates) and includes dedicated constructors for if-then-else and equality,
both of which occur frequently enough to warrant their own nodes rather than
being built-in operations.
Although Lambda can be parameterized by an arbitrary type system, the Strata
code base includes a
formalization
of a polymorphic Hindley-Milner type system and an
implementation
of an inference algorithm over the type LTy (described below). This allows
prenex (Hindley-Milner) polymorphism and the use of arbitrary named type
constructors (as well as special support for bit vector types, to allow them to
be parameterized by size).
2.1. Syntax🔗
The syntax of lambda expressions is provided by the LExpr type.
🔗inductive type
Lambda expressions with quantifiers.
Like Lean's own expressions, we use the locally nameless
representation for this abstract syntax.
See this paper
for details.
We leave placeholders for type annotations only for constants
(.const), operations (.op), binders (.abs, .quant), and free
variables (.fvar).
LExpr is parameterized by LExprParamsT, which includes arbitrary metadata,
user-allowed type annotations (optional), and special metadata to attach to
Identifiers. Type inference adds any missing type annotations.
Constructors
Lambda.LExpr.quant {T : LExprParamsT} (m : T.base.Metadata)
(k : QuantifierKind) (prettyName : String)
(ty : Option T.TypeType) (trigger e : LExpr T) : LExpr T
A quantified expression, where k indicates whether it is universally or
existentially quantified, prettyName is a display name (empty string if none provided) and ty is the type of bound variable; trigger is
a trigger pattern (primarily for use with SMT).
Identifiers in lambda expressions, using the Identifier type,
can be annotated with metadata.
🔗structure
Identifiers with a name and additional metadata
Fields
metadata : IDMeta
Any additional metadata that it would be useful to attach to an
identifier.
Specific constructors exist for constants of various scalar types, including
booleans, bit vectors, integers, reals, and strings, and for literals of the
collection types Map k v and Sequence a.
🔗inductive type
Lambda constants.
Constants are integers, strings, reals, bitvectors of a fixed length,
booleans, and literals of the collection types Map k v and Sequence a
built from constants.
A collection literal names the sorts of its elements, so its type is known even
when it has no elements. Its elements are not checked against those sorts by
construction; LConst.wt checks them, and LConst.ty gives a collection
literal that fails the check the type bool (see LConst.ty).
Constructors
Lambda.LConst.strConst (s : String) : LConst
A string constant, using Lean's String type for a sequence of Unicode
code points encoded with UTF-8.
Lambda.LConst.rationalConst (r : Rat) : LConst
A literal of type real. Literals are exact rationals because every real
written in Strata's finite literal notation (a decimal or frac{n, d}) is
rational. Rat normalizes each value to a canonical representation, so two
literals are equal exactly when their stored values are equal.
Lambda.LConst.mapConst (keySort valSort : LSort)
(dflt : LConst) (entries : Array (LConst × LConst)) :
LConst
A literal of type Map keySort valSort: the total map sending each key of
entries to its value and every other key to dflt. When two entries have
the same key, the first one counts. The literals the evaluator builds have
distinct keys and no entry whose value is dflt (see LConst.mapUpdate).
The LExpr type can be parameterized by the type used to represent
normal metadata and the type used to represent identifier metadata, as well as
the type of types.
🔗structure
Expected interface for pure expressions that can be used to specialize the
Imperative dialect.
Fields
Metadata : Type
The type of metadata allowed on expressions.
IDMeta : Type
The type of metadata allowed on identifiers.
🔗structure
Extended LExprParams that includes TypeType parameter.
Fields
base : LExprParams
The base parameters, with the types for expression and identifier metadata.
TypeType : Type
The type of types used to annotate expressions.
2.2. Type System🔗
Although LExpr can be parameterized by an arbitrary type system,
Strata currently implements one, based on the types LMonoTy and
LTy.
The first, LMonoTy, represents monomorphic types. A monomorphic
type may contain free type variables (via ftvar); these are implicitly
universally quantified. LMonoTy is a separate type because some contexts
(e.g., variable declarations, function parameter types) allow only monomorphic
types.
🔗inductive type
Monomorphic types in Lambda. Note that all free type variables (.ftvar)
are implicitly universally quantified.
Type variables in LMonoTy use the TyIdentifier type.
🔗def
Type identifiers. For now, these are just strings.
The LTy type makes the universal quantification explicit by wrapping
a monomorphic type in prenex universal quantifiers that bind its free type
variables, creating polymorphic type schemes.
🔗inductive type
Polymorphic type schemes in Lambda.
An expression LExpr parameterized by LTy is
well-typed according to the HasType relation.
This relation depends on two contexts:
-
LContext: information that is typically constant during
expression type checking, but may be extended during statement type checking.
For example, a typeDecl statement adds a new type. This context also
includes information about built-in functions, using the
Factory type, and built-in types, using the
TypeFactory type. Built-in functions optionally include
concrete evaluation functions, which can be used in the semantics described
below.
-
TContext: data that changes throughout the type
checking process — a map from free variables in expressions to types, and a
list of type aliases including the name and definition of each alias.
🔗structure
Context data for type checking: a factory of user-specified functions and
data structures for ensuring unique names of types and functions.
This context is typically constant during expression type checking, but may
be extended during statement type checking (for example, a typeDecl statement
adds a new type).
Invariant: all functions defined in TypeFactory.genFactory
for datatypes should be in functions.
Fields
functions : Lambda.Factory T
Descriptions of all built-in functions.
datatypes : TypeFactory
Descriptions of all built-in datatypes.
knownTypes : Lambda.KnownTypes
A list of known built-in types.
idents : Identifiers T.IDMeta
The set of identifiers that have been seen or generated so far.
rigidTypeVars : List TyIdentifier
Type variables that are rigid (skolemized) in the current scope.
🔗structureLambda.TContext (IDMeta : Type) [DecidableEq IDMeta] [Hashable IDMeta] :
Type Lambda.TContext (IDMeta : Type)
[DecidableEq IDMeta] [Hashable IDMeta] :
Type
A type context describing the types of free variables and the mappings of type
aliases.
Fields
types : Strata.Util.HMaps (Identifier IDMeta) LTy
A map from free variables in expressions (i.e., LExpr.fvars) to their
type schemes. This is essentially a stack to account for variable scopes.
aliases : List TypeAlias
A map from type synonym names to their corresponding type definitions. We
expect these type definitions to not be aliases themselves, to avoid any
cycles in the map (see TEnv.addTypeAlias).
Given these two contexts, the HasType relation describes
the valid type of each expression form.
🔗inductive predicate
Typing relation for LExprs with respect to LTy.
The typing relation is parameterized by two contexts. An LContext contains
known types and functions while a TContext associates free variables with
their types.
Constructors
Lambda.LExpr.HasType.tquant {T : LExprParams}
[DecidableEq T.IDMeta] [Hashable T.IDMeta]
{C : LContext T} (Γ : TContext T.IDMeta)
(m : T.mono.base.Metadata) (k : QuantifierKind)
(name : String)
(tr : LExpr { base := T, TypeType := LMonoTy })
(tr_ty : LTy) (x : IdentT LMonoTy T.IDMeta) (x_ty : LTy)
(e : LExpr { base := T, TypeType := LMonoTy })
(o : Option LMonoTy) :
LExpr.fresh x e →
∀ (hx : x_ty.isMonoType = true),
LExpr.HasType C
{ types := Γ.types.insert x.fst x_ty,
aliases := Γ.aliases }
(LExpr.varOpen 0 x e)
(LTy.forAll [] LMonoTy.bool) →
LExpr.HasType C
{ types := Γ.types.insert x.fst x_ty,
aliases := Γ.aliases }
(LExpr.varOpen 0 x tr) tr_ty →
(o = none ∨
∃ t,
o = some t ∧
LExpr.AnnotCompat Γ.aliases t
(x_ty.toMonoType hx)) →
(∀ (t : LMonoTy),
o = some t →
∃ r,
SourceTyWF C TyVarAdmissibility.all
Γ.aliases t r) →
LExpr.HasType C Γ
(LExpr.quant m k name o tr e)
(LTy.forAll [] LMonoTy.bool)
A quantifier ∀/∃ {x: tr}.e has type bool if the claimed type of x is
x_ty or None, and if, when Γ is extended with the binding (x → x_ty),
e has type bool and tr is well-typed. A written binder annotation must
be a valid source type, which may mention any type variable.
After Lambda's type inference (LExpr.resolve), the type-annotated
expressions follow tighter typing rules which are defined by
LExpr.HasTypeA. The rule doesn't require typing
contexts.
3. Imperative🔗
The Imperative language is a standard core imperative calculus, parameterized
by a type of expressions (PureExpr) and divided into two pieces: commands and statements.
Commands represent atomic operations that do not induce control flow.
Statements are parameterized by a command type and describe the control flow
surrounding those commands. This parameterization allows clients of Imperative
to extend the command type with domain-specific operations (e.g., Strata Core
adds procedure calls). Currently, Imperative offers two families of
statements: structured deterministic statements and non-deterministic (Kleene)
statements.
3.1. Commands🔗
The core built-in set of commands includes variable initializations,
deterministic assignments, non-deterministic assignments ("havoc"), assertions,
assumptions, and coverage checks. A coverage check (cover) is the dual of
an assertion: it checks whether there exists a reachable path on which the
given condition holds.
🔗inductive type
A an atomic command in the Imperative dialect.
Commands don't create local control flow, and are typically used as a parameter
to Imperative.Stmt or other similar types.
Command values can be either deterministic expressions or non-deterministic
(arbitrary) choices, represented by the ExprOrNondet type.
🔗inductive type
A value that is either a deterministic expression or a non-deterministic choice.
3.2. Structured Deterministic Statements🔗
Statements allow commands to be organized into standard control flow
arrangements, including sequencing, alternation, and iteration. Sequencing
statements occurs by grouping them into blocks. Loops can be annotated with
optional invariants and decreasing measures, which can be used for deductive
verification. An exit statement transfers control out of the nearest
enclosing block with a matching label. Statements also include typeDecl for
local type declarations. Core concrete syntax may use an internal function
declaration; translation lowers that syntax to an ordinary local variable
initialization whose value is a Lambda abstraction. Internal declarations with
type parameters or preconditions are not supported by this lowering, because
Lambda abstractions do not represent those features.
🔗inductive type
Imperative statements focused on control flow.
The P parameter specifies the type of expressions that appear in conditional
and loop guards. The Cmd parameter specifies the type of atomic command
contained within the .cmd constructor.
Constructors
Imperative.Stmt.loop.{u_1} {P : PureExpr} {Cmd : Type}
(guard : ExprOrNondet P) (measure : Option P.Expr)
(invariants : List (String × P.Expr))
(body : List (Stmt P Cmd)) (md : MetaData P) : Stmt P Cmd
An iterated execution statement. Includes an optional measure (for
termination) and labeled invariants. When guard is .nondet, the loop iterates
a non-deterministic number of times. Each invariant carries a label string
(expected to be distinct, like assert labels do).
TODO: invariants and measure will be moved to metadata md, since they don't
contribute to the small-step semantics (StepStmtE).
🔗def
A block is simply an abbreviation for a list of commands.
3.3. Non-deterministic Statements🔗
Non-deterministic statements, inspired by
Kleene Algebra with Tests
and
Guarded Commands,
encode control flow using only non-deterministic choices. A KleeneStmt
can be: an atomic command, a sequential composition, a non-deterministic choice
between two sub-statements, or a loop that executes its body an arbitrary number
of times (possibly zero). Conditions can be encoded when the command type
includes assumptions.
🔗inductive type
A Kleene statement, parameterized by a type of pure expressions (P)
and a type of commands (Cmd).
This encodes the same types of control flow as Stmt, but using only
non-deterministic choices: arbitrarily choosing one of two sub-statements to
execute or executing a sub-statement an arbitrary number of times. Conditions
can be encoded if the command type includes assumptions.
Constructors
Imperative.KleeneStmt.block.{u_1} {P : PureExpr}
{Cmd : Type} (s : KleeneStmt P Cmd) : KleeneStmt P Cmd
Execute s in a scoped block: variables initialized inside are
projected away on exit (matching the deterministic .block semantics).
There is no label unlike Imperative.Stmt.block because KleeneStmt doesn't
have .exit.
3.4. Control-Flow Graphs🔗
Imperative offers a control-flow graph (CFG) as well.
A CFG is a flat collection of labeled basic blocks wired together by terminators
(explicit jumps). This is the natural representation for
lowering unstructured source languages and for interacting with backends that
already think in terms of basic blocks and jumps.
A BasicBlock is a straight-line list of body
commands.
🔗structure
A basic block consists of a list of body commands, and a transfer
command that indicates where to go next. It can be deterministic or
non-deterministic depending on the type of transfer command.
Fields
cmds : List Cmd
The straight-line body commands, executed in order.
transfer : TransferCmd
The transfer command run after the body, selecting the successor block(s)
(or halting).
🔗inductive type
A DetTransfer command terminates a deterministic basic block, indicating
where execution should proceed next, if anywhere.
🔗inductive type
A NondetTransfer command terminates a non-deterministic basic block,
indicating the list of possible blocks where execution could proceed next, if
anywhere.
Specializing the transfer type gives the two block flavors,
DetBlock and NondetBlock.
A CFG then bundles an entry label with the graph's labeled
blocks.
🔗structure
A control flow graph is a list of blocks paired with a label indicating
where execution should start.
Fields
entry : Label
The label of the block where execution begins.
blocks : List (Label × Block)
The labeled blocks of the graph, as an association list from label to
block.
Metadata allows additional information to be attached to nodes in the Strata
AST. This may include information such as the provenance of specific AST nodes
(e.g., the locations in source code that gave rise to them), facts inferred by
specific analyses, or indications of the goal of a specific analysis, among many
other possibilities.
Each metadata element maps a field to a value. A field can be named with a
variable or an arbitrary string.
A value can take the form of an expression, an arbitrary string, a source file
range, or a boolean switch.
A metadata element pairs a field with a value.
And, finally, the metadata attached to an AST node consists of an array of
metadata elements.
3.6. Instantiating Imperative🔗
Using the Imperative dialect for a concrete language requires filling in three
pieces:
-
The expression parameter PureExpr, defined in
Strata/DL/Imperative/PureExpr.lean.
A PureExpr bundles the types the dialect will use for identifiers,
expressions, types, metadata, typing environments, factories, and the
expression evaluator (eval). Instantiating Imperative starts by
constructing a PureExpr for the target language (Strata Core does this
with Core.Expression).
🔗structure
Expected interface for pure expressions that can be used to specialize the
Imperative dialect.
Fields
Ident : Type
Kinds of identifiers allowed in expressions. We expect identifiers to have
decidable equality; see EqIdent.
EqIdent : DecidableEq self.Ident
Decidable equality on identifiers.
ExprMetadata : Type
Expression metadata type (for use in function declarations, etc.)
TyEnv : Type
Typing environment, expected to contain a map of variables to their types,
type substitution, etc.
TyContext : Type
Typing context, expected to contain information that does not change
during type checking/inference (e.g., known types and known functions.)
Factory : Type u
Factory for function/operator resolution. A factory may also carry a
semantic model (as Core's runtime factory does), which is why it lives in
an arbitrary universe.
Val : Type u
Runtime values held by variable stores and produced by eval. A value
may record the model it was produced in; HasVal.value says which
values belong to a given factory.
eval : self.Factory → (self.Ident → Option self.Val) → self.Expr → Option self.Val
The expression evaluator. Takes a factory, a variable store, and an
expression, and returns an optional value.
-
Structural typeclasses on PureExpr. Imperative's commands and
statements need to inspect and manipulate expressions in generic ways —
extracting free variables, constructing Boolean/integer literals, negating
conditions, and so on. These operations are provided via typeclasses whose
names start with Has (e.g., HasVarsImp),
defined in Strata/DL/Imperative/PureExpr.lean and
Strata/DL/Imperative/HasVars.lean. See
Strata/Languages/Core/InstWellFormedSemanticsEval.lean for Strata Core's
instantiations of these typeclasses.
-
Well-formedness of the evaluator. The semantics rules assume the evaluator
supplied via PureExpr.eval respects a few sanity conditions on values,
variable lookups, and Boolean negation. These predicates, and the bundle
WellFormedSemanticEval that packages
them, are described in the companion document, "The Strata Core Language
Semantics" (see its "Well-Formedness of the Evaluator" section).
The Strata Core language, described next, is a worked example of an
Imperative instantiation: it picks Lambda expressions for PureExpr,
supplies the required Has-typeclass instances, and discharges the
well-formedness conditions against LExpr.denoteEval, Lambda's denotational evaluator.
4. Strata Core🔗
Strata Core is the concrete verification language built by instantiating the
generic Lambda and Imperative building blocks with specific types. This
section describes the top-level constructs that make up a Strata Core program.
4.1. Expressions🔗
Strata Core expressions are Lambda expressions instantiated with a specific
identifier type (CoreIdent) and a monomorphic type system (LMonoTy). A
CoreIdent identifies either a local variable or an old expression (denoting
a pre-state value).
4.1.1. Built-in Types🔗
Strata Core provides the following built-in types:
-
bool — booleans
-
int — unbounded integers
-
real — rationals (used to model reals)
-
string — UTF-8 strings
-
regex — regular expressions over strings
-
bv<n> — bit vectors of size n (e.g., bv32, bv64)
-
Map<K, V> — maps from keys of type K to values of type V
-
Sequence<T> — finite sequences of elements of type T
In addition, function types (a → b) are supported as first-class types.
Users can define additional types via type declarations (abstract types, type
synonyms, and algebraic datatypes).
4.1.2. Built-in Operators🔗
Strata Core provides built-in operators organized by the types they operate on.
The following summarizes each category; the definitive list of operators is
registered in
Core.Factory
(see also the
API reference).
-
Boolean: conjunction, disjunction, negation, implication, equivalence.
-
Numeric (int and real): addition, subtraction, multiplication, negation,
division, modulus (Euclidean and truncating variants), comparisons
(<, ≤, >, ≥). Safe variants of division and modulus generate
precondition checks for division by zero.
-
Bit vector: arithmetic (add, sub, mul, div, mod — both signed and
unsigned), bitwise (and, or, xor, not, shifts), comparisons (signed and
unsigned), concatenation, and extraction of sub-ranges. Safe arithmetic
variants generate overflow precondition checks.
-
String: length, concatenation, substring extraction, prefix and suffix
checks, conversion to regular expression, and regular expression membership.
-
Regular expression: constructors (all, allChar, range, none), composition
(concatenation, union, intersection, complement, star, plus, loop).
-
Map: constant map, select (lookup), and update (store).
-
Sequence: length, empty, append, select (index), build, update, contains,
take, and drop.
Equality (==) and if-then-else are provided as built-in Lambda expression
constructors rather than operators.
4.2. Type Declarations🔗
Strata Core supports three forms of type declaration:
-
Abstract types (type Name _ ...;): Opaque type constructors with a
given arity.
-
Type synonyms (type Name x y = ...;): Named aliases for existing types,
which may be parameterized by type variables.
-
Algebraic datatypes (datatype Name(...) { ... };): Datatypes with
multiple constructors, each of which can have zero or more typed fields.
Mutual datatypes are supported. See below for details.
4.2.1. Algebraic Datatypes🔗
Datatypes are declared using the datatype keyword:
datatype <Name>(<TypeParams>) {
<Constructor1>(<field1>: <type1>, ...),
<Constructor2>(<field2>: <type2>, ...),
...
};
Strata Core datatypes must satisfy several well-formedness properties: they must
be inhabited (subject to a syntactic check that tries to determine a provably
inhabited constructor), uniform (the type parameters cannot change through
recursion), strictly positive (all recursive occurrences of a type in a
constructor do not appear to the left of any arrow), and non-nested (disallowing
e.g. datatype Foo() { A(x: List<Foo>) }).
Datatypes may be polymorphic and recursive:
datatype Color () { Red(), Green(), Blue() };
datatype Option<T> () { None(), Some(val: T) };
datatype List<T> () { Nil(), Cons(head: T, tail: List<T>) };
When a datatype is declared, Strata automatically generates three kinds of
auxiliary functions:
-
Constructors: functions that create values of the datatype (e.g.,
None() : Option<T>, Cons(head: T, tail: List<T>) : List<T>).
-
Tester functions: for each constructor, a function that returns true if
a value was created with that constructor. The naming convention is
<Datatype>..is<Constructor> (e.g., Option..isNone, List..isCons).
-
Field accessors: for each field, Strata generates safe and unsafe variants.
The default (safe) versions (e.g., List..head) add a precondition check
requiring that the argument is an instance of the given constructor. The
unsafe versions (e.g., List..head!) do not check this — the result is
unspecified (an arbitrary value of the return type) if called on the wrong
constructor.
4.3. Functions🔗
Strata Core functions are pure, named operations with typed input parameters
and a return type. A function may have an optional body (an expression over the
declared parameters); if absent, it is uninterpreted. Functions may also have
preconditions that restrict their domain.
The concrete syntax for a function declaration without a body is:
function Name<TypeArgs>(x₁ : T₁, ..., xₙ : Tₙ) : ReturnType;
A function with a body:
function Name<TypeArgs>(x₁ : T₁, ..., xₙ : Tₙ) : ReturnType
{
body_expression
};
A function may be prefixed with inline to allow its calls to be replaced by its
body. Inlining is a request, not a guarantee. The simplify phase expands a call to an
inline function only where the copy cannot compound: when every parameter the body
uses more than once receives a closed value (a literal or a constructor applied to
closed values) or a single variable or constant, or, for an argument that is a
constructor application, when the expanded call folds to something smaller. Symbolic
evaluation then expands a call only when all its arguments are closed values. So
dup(3) still folds to 6, while dup(dup(y)) keeps its outer call. A call to a
function with a precondition is never expanded. Calls to a function that takes,
returns or builds a function value are always expanded, because expanding them is what
removes the lambdas the SMT encoder cannot represent.
4.3.1. Recursive Functions🔗
Strata supports two kinds of recursive functions: structural recursion over
algebraic datatypes, and int-valued recursion with integer termination
measures. Both single and mutually recursive functions are supported.
Recursive functions cannot be marked inline.
4.3.1.1. Structural Recursion (ADT)🔗
Structural recursive functions are declared with the rec keyword, and exactly
one parameter must be annotated with @[cases] to indicate the algebraic
datatype argument for per-constructor axiom generation: one unfolding axiom is
generated for each constructor of the datatype, case-splitting on the @[cases]
parameter.
rec function listLen (@[cases] xs : IntList) : int
{
if IntList..isNil(xs) then 0 else 1 + listLen(IntList..tl(xs))
};
An optional decreases clause specifies which parameter is used as the
termination measure. It appears after the preconditions and before the body.
If omitted, the @[cases] parameter is used. If provided, it overrides only the
termination check — @[cases] still controls axiom generation.
rec function zipLen (@[cases] xs : IntList, ys : IntList) : int
decreases ys
{
if IntList..isNil(xs) then 0
else if IntList..isNil(ys) then 0
else 1 + zipLen(IntList..tl(xs), IntList..tl(ys))
};
4.3.1.2. Int-Valued Recursion🔗
When the decreases clause specifies an expression of type int (rather than
a datatype-typed parameter), the function uses int-valued termination checking.
These functions do NOT require @[cases].
rec function fib (n : int) : int
decreases n
{
if n <= 1 then n else fib(n - 1) + fib(n - 2)
};
The decreases expression may be an arbitrary integer expression over the
function's parameters:
rec function diagonal (m : int, n : int) : int
requires m >= 0;
requires n >= 0;
decreases m + n
{
if m <= 0 then (if n <= 0 then 0 else diagonal(m, n - 1))
else diagonal(m - 1, n)
};
4.3.1.3. General Rules🔗
Every recursive function must have at least a @[cases] annotation or a
decreases clause; Strata rejects recursive functions without a termination hint.
If a function has both @[cases] and an int-valued decreases clause,
@[cases] enables per-constructor axiom generation and partial evaluation,
while decreases is used for termination checking.
Mutually recursive functions are declared as multiple functions within a single
rec block:
rec function treeSize (@[cases] t : RoseTree) : int
{
if RoseTree..isLeaf(t) then 1 else listSize(RoseTree..children(t))
}
function listSize (@[cases] xs : RoseList) : int
{
if RoseList..isRNil(xs) then 0
else treeSize(RoseList..hd(xs)) + listSize(RoseList..tl(xs))
};
4.3.1.4. Termination Checking🔗
Termination checking is always on for all rec functions.
For structural recursion, Strata checks that recursive calls pass a
structurally smaller argument at the termination measure position. A rank
function is generated for the datatype, and each recursive call must have
strictly smaller rank than the caller's parameter.
For int-valued recursion, two obligations are checked at each recursive
call site:
A function that fails its termination check will produce a verification failure
on its _terminates_ obligations.
4.3.1.5. Current Limitations🔗
-
Recursive functions must be declared at the top level (not as local
declarations inside procedures).
-
Only single-expression termination measures are supported; lexicographic
measures are not yet supported.
-
There is no way currently to give additional information for the
proofs of non-negativity for int-valued measures. For example,
using the measure listLen(l1) + listLen(l2) will produce currently
unprovable obligations about the nonnegativity of listLen over
arbitrary lists.
4.4. Axioms🔗
Axioms are propositions assumed to be true throughout a Strata Core program.
It is the responsibility of the user to ensure that axioms are consistent.
The concrete syntax is:
axiom [label]: expression;
An axiom may also list parameters, with optional triggers after them. This
form is sugar for a universal quantifier over the parameters:
axiom [label] (x : int, y : int) { f(x, y) }: expression;
// stands for
axiom [label]: forall x : int, y : int :: { f(x, y) } expression;
4.5. Lemmas🔗
A lemma is a proposition that must be proved. It is written like an axiom,
with the keyword lemma, and accepts the same parameter list and triggers:
lemma [label]: expression;
lemma [label] (x : int) { f(x) }: expression;
lemma is a keyword, like axiom; an identifier of that name is written
|lemma|.
Each lemma yields one proof obligation, checked under the axioms and
distinct facts declared before it, like an assertion in a procedure. A lemma
is never assumed when checking other declarations, so proving it does not make
it available to later proofs. Its outermost universal quantifiers are checked
over fresh free variables, so a failing lemma reports a counterexample for
them.
A lemma may take type parameters, written after its label as for a procedure:
lemma [label] <a> (x : a, xs : List a): expression;
lemma [label] <a>: expression;
Such a lemma must hold at every type. It is checked with each type parameter
replaced by a fresh opaque type, so its formula cannot constrain a type
parameter to a particular type.
Functions and procedures list the lemmas they depend on. The
well-formedness checks of a function's or procedure's contract are generated
as such lemmas, one per check: each states that the preconditions of a partial
function call hold under the conditions written before it. Procedure filtering
keeps a procedure's lemmas exactly when it keeps the procedure.
Preconditions describe the state on entry, so in these lemmas an in-out
parameter g named in a precondition stands for its entry value old g. A
postcondition that reads g reads its final value, which the preconditions do
not constrain: with requires !(g == 0), the check for int.safeDiv(y, g) in a
postcondition fails, while the check for int.safeDiv(y, old g) succeeds.
A lemma written in the program gets the same checks for the partial calls in
its own formula, as an assertion does. Generated lemmas are named after their
checks, with a _k suffix when that name is already declared in the program.
4.6. Commands and Statements🔗
Imperative extends its own commands with a procedure call command. A
CmdExt is either a standard Imperative.Cmd or a call to a
named procedure with a list of arguments. Strata Core's Command is CmdExt
instantiated at Core's expression type.
🔗inductive type
Extend Imperative's commands by adding a procedure call.
Each call argument specifies whether the corresponding parameter is passed by
value (input), by mutable reference (input-output), or as an output-only
variable.
🔗inductive type
A call argument is either an input expression, an in-out variable, or an
output variable.
A Strata Core Statement is an Imperative.Stmt parameterized by Core's
expression type and extended command type. Strata provides convenience
abbreviations: Statement.init, Statement.set, Statement.havoc,
Statement.assert, Statement.assume, Statement.call, and
Statement.cover.
4.7. Procedures🔗
A procedure is the main verification unit in Strata Core. It is a named
signature with typed input and output parameters, a specification (contract),
and an optional implementation body.
The concrete syntax of a procedure declaration is ([] denotes optional):
procedure Name<TypeArgs>([out/inout] x₁ : T₁, ..., [out/inout] xₙ : Tₙ)
spec {
[free] requires [label]: P;
[free] ensures [label]: Q;
}
{ body };
The Procedure.Header structure captures the procedure's
name, type parameters, and input/output signatures.
4.7.1. Parameters🔗
Each procedure has three groups of parameters:
-
Input parameters (name : T): Passed by value from the caller to the
callee. They are immutable within the procedure body.
-
Output parameters (out name : T): Passed by value from the callee back
to the caller. They are mutable within the procedure body and their final
values are returned to the caller.
-
Input-output parameters (inout name : T): Appear in both input and
output roles. The input value is the pre-state and the output value is the
post-state.
Parameter names must be disjoint from each other.
4.7.2. Specification🔗
A procedure's specification (Procedure.Spec) consists of
two parts: preconditions (requires) that must hold before invocation, and
postconditions (ensures) that must hold on return. Postconditions may reference
old v for pre-state values of inout variables.
🔗def
A procedure's specification (contract) over Core expressions.
Postconditions may reference old v for pre-state values.
Each specification clause is represented by Procedure.Check,
pairing a boolean expression with an optional Free attribute and metadata.
🔗def
A single specification clause over Core expressions.
The Procedure.CheckAttr type controls whether a
clause is checked or free. A free precondition is assumed by the implementation
but not asserted at call sites; a free postcondition is assumed upon return from
calls but not checked on exit from implementations.
🔗def
The check/free attribute of a specification clause.
4.7.3. The old expression🔗
Postconditions and procedure bodies are two-state contexts: they can refer to
both the pre-state (on entry) and the post-state (on exit) of a procedure
invocation. The pre-state value of an inout parameter v is denoted by old v.
old is not allowed in preconditions.
4.7.4. Procedure calls🔗
A procedure is invoked via the call statement:
call ProcName([out/inout] e₁, ..., [out/inout] eₙ);
Note that out and inout keywords can only be attached when eᵢ is a variable.
A call's arguments must match the procedure's parameters, in order: an argument
without a keyword for each input parameter, inout x for each inout parameter
and out x for each out parameter. An inout parameter is passed as one
variable, as in call P(inout x), not as a value and a separate result, as in
call P(x, out x). The variables passed for a call's out and inout parameters
must be distinct: a variable may not be passed for two results of the same call,
as in call P(out x, out x) or call P(inout x, out x). Strata rejects any other
call.
4.7.5. Body and verification🔗
If a procedure has a non-empty body, the preconditions are assumed to hold on
entry, the body is executed, and the postconditions must hold on exit. If the
body is empty, the procedure is abstract and can only be reasoned about via its
contract.
4.7.6. The Procedure type🔗
🔗def
A Strata Core procedure: the main verification unit. A procedure is a header
(name, type parameters, input/output signatures), a specification (contract),
and an optional body. An empty body makes the procedure abstract, reasoned
about only via its contract.
4.8. Programs🔗
A Strata Core program is an ordered list of declarations. Each declaration is
one of:
-
a type declaration (abstract type, type synonym, or algebraic datatype),
-
an axiom,
-
a lemma,
-
a distinct declaration (asserting that a list of expressions are pairwise distinct),
-
a procedure,
-
a (non-recursive) function, or
-
a mutually recursive function block.
🔗inductive type
A Strata Core declaration.
Note: constants are 0-ary functions.
Constructors
Core.Decl.type (t : TypeDecl) (md : MetaData Expression) :
Decl
A type declaration (abstract type, type synonym, or algebraic datatype).
🔗structure
A Core.Program is an ordered list of declarations.
Fields
decls : Decls
The declarations that make up this program.