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,
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
abs {T : LExprParamsT} (m : T.base.Metadata)
(prettyName : String) (ty : Option T.TypeType)
(e : LExpr T) : LExpr T
An abstraction, where prettyName is a display name (empty string if none provided) and ty is the (optional) type of bound variable.
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).
ite {T : LExprParamsT} (m : T.base.Metadata)
(c t e : LExpr T) : LExpr T
A conditional expression. This is a constructor rather than a built-in
operation because it occurs so frequently.
eq {T : LExprParamsT} (m : T.base.Metadata)
(e1 e2 : LExpr T) : LExpr T
An equality expression. This is a constructor rather than a built-in
operation because it occurs so frequently.
Identifiers in lambda expressions, using the Identifier type,
can be annotated with metadata.
🔗structureLambda.Identifier (IDMeta : Type) : Type
Lambda.Identifier (IDMeta : Type) : Type
Identifiers with a name and additional metadata
Constructor
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.
🔗inductive typeLambda.LConst : Type
Lambda.LConst : Type
Lambda constants.
Constants are integers, strings, reals, bitvectors of a fixed length, or
booleans.
Constructors
intConst (i : Int) : LConst
An unbounded integer constant.
strConst (s : String) : LConst
A string constant, using Lean's String type for a sequence of Unicode
code points encoded with UTF-8.
realConst (r : Rat) : LConst
A real constant, represented as a rational number.
bitvecConst (n : Nat) (b : BitVec n) : LConst
A bit vector constant, represented using Lean's BitVec type.
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.
🔗structureLambda.LExprParams : Type 1
Lambda.LExprParams : Type 1
Expected interface for pure expressions that can be used to specialize the
Imperative dialect.
Constructor
Fields
Metadata : Type
The type of metadata allowed on expressions.
IDMeta : Type
The type of metadata allowed on identifiers.
🔗structureLambda.LExprParamsT : Type 1
Lambda.LExprParamsT : Type 1
Extended LExprParams that includes TypeType parameter.
Constructor
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 typeLambda.LMonoTy : Type
Lambda.LMonoTy : Type
Monomorphic types in Lambda. Note that all free type variables (.ftvar)
are implicitly universally quantified.
Constructors
bitvec (size : Nat) : LMonoTy
A bit vector type. This is a special case so that it can be parameterized
by a size.
Type variables in LMonoTy use the TyIdentifier type.
🔗defLambda.TyIdentifier : Type
Lambda.TyIdentifier : Type
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 typeLambda.LTy : Type
Lambda.LTy : Type
Polymorphic type schemes in Lambda.
Constructors
forAll (vars : List TyIdentifier) (ty : LMonoTy) : LTy
A type containing universally quantified type variables.
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
(e.g., when a funcDecl statement adds a new function to the factory).
This 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 when local function declarations
(funcDecl) add new functions to the factory.
Invariant: all functions defined in TypeFactory.genFactory
for datatypes should be in functions.
Constructor
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.
Constructor
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
tgen {T : LExprParams} [DecidableEq T.IDMeta]
[Hashable T.IDMeta] {C : LContext T}
(Γ : TContext T.IDMeta) (e : LExpr T.mono)
(a : TyIdentifier) (ty : LTy) :
LExpr.HasType C Γ e ty →
TContext.isFresh a Γ →
LExpr.HasType C Γ e (LTy.close a ty)
If e has type ty, it also has type ∀ a. ty as long as a is fresh.
For instance, (·ftvar "a") → (.ftvar "a") (or a → a)
can be generalized to (.btvar 0) → (.btvar 0) (or ∀a. a → a), assuming
a is not in the context.
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.
Constructors
init {P : PureExpr} (name : P.Ident) (ty : P.Ty)
(e : ExprOrNondet P) (md : MetaData P) : Cmd P
Define a variable called name with type ty and value e.
When e is .nondet, the variable is initialized with an arbitrary value.
set {P : PureExpr} (name : P.Ident) (e : ExprOrNondet P)
(md : MetaData P) : Cmd P
Assign e to a pre-existing variable name.
When e is .nondet, assigns an arbitrary value (havoc semantics).
assert {P : PureExpr} (label : String) (b : P.Expr)
(md : MetaData P) : Cmd P
Checks if condition b is true on all paths on which this command is
encountered. Reports an error if b does not hold on any of these paths.
assume {P : PureExpr} (label : String) (b : P.Expr)
(md : MetaData P) : Cmd P
Ignore any execution state in which b is not true.
cover {P : PureExpr} (label : String) (b : P.Expr)
(md : MetaData P) : Cmd P
Checks if there exists a path that reaches this command and condition b is
true. Reports an error otherwise. This is the dual of assert, and can be
used for coverage analysis.
Command values can be either deterministic expressions or non-deterministic
(arbitrary) choices, represented by the ExprOrNondet type.
🔗inductive typeImperative.ExprOrNondet (P : PureExpr) : Type Imperative.ExprOrNondet (P : PureExpr) :
Type
A value that is either a deterministic expression or a non-deterministic choice.
Constructors
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. In addition, statements include
funcDecl for local function declarations (which extend the expression
evaluator within a scope) and typeDecl for local type declarations.
🔗inductive typeImperative.Stmt (P : PureExpr) (Cmd : Type) : Type Imperative.Stmt (P : PureExpr)
(Cmd : Type) : 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
block {P : PureExpr} {Cmd : Type} (label : String)
(b : List (Stmt P Cmd)) (md : MetaData P) : Stmt P Cmd
An block containing a List of Stmt.
ite {P : PureExpr} {Cmd : Type} (cond : ExprOrNondet P)
(thenb elseb : List (Stmt P Cmd)) (md : MetaData P) :
Stmt P Cmd
A conditional execution statement. When cond is .nondet, the branch
is chosen non-deterministically.
loop {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 (StepStmt).
exit {P : PureExpr} {Cmd : Type} (label : String)
(md : MetaData P) : Stmt P Cmd
An exit statement that transfers control out of the enclosing block
with the given label.
funcDecl {P : PureExpr} {Cmd : Type} (decl : PureFunc P)
(md : MetaData P) : Stmt P Cmd
A function declaration within a statement block.
typeDecl {P : PureExpr} {Cmd : Type} (tc : TypeConstructor)
(md : MetaData P) : Stmt P Cmd
A type declaration within a statement block.
🔗defImperative.Block (P : PureExpr) (Cmd : Type) : Type Imperative.Block (P : PureExpr)
(Cmd : Type) : Type
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 typeImperative.KleeneStmt (P : PureExpr) (Cmd : Type) : Type Imperative.KleeneStmt (P : PureExpr)
(Cmd : Type) : 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
cmd {P : PureExpr} {Cmd : Type} (cmd : Cmd) :
KleeneStmt P Cmd
An atomic command, of an arbitrary type.
block {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.
🔗structureImperative.BasicBlock (TransferCmd Cmd : Type) : Type
Imperative.BasicBlock
(TransferCmd Cmd : Type) : Type
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.
Constructor
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 typeImperative.DetTransferCmd (Label : Type) (P : PureExpr) : Type Imperative.DetTransferCmd (Label : Type)
(P : PureExpr) : Type
A DetTransfer command terminates a deterministic basic block, indicating
where execution should proceed next, if anywhere.
Constructors
finish {Label : Type} {P : PureExpr} (md : MetaData P) :
DetTransferCmd Label P
Stop execution of the current unstructured program. If in a procedure
body, this can be interpreted as returning to the caller.
🔗inductive typeImperative.NondetTransferCmd (Label : Type) (P : PureExpr) : Type Imperative.NondetTransferCmd
(Label : Type) (P : PureExpr) : Type
A NondetTransfer command terminates a non-deterministic basic block,
indicating the list of possible blocks where execution could proceed next, if
anywhere.
Constructors
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.
🔗structureImperative.CFG (Label Block : Type) : Type
Imperative.CFG (Label Block : Type) : Type
A control flow graph is a list of blocks paired with a label indicating
where execution should start.
Constructor
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).
🔗structureImperative.PureExpr : Type 1
Imperative.PureExpr : Type 1
Expected interface for pure expressions that can be used to specialize the
Imperative dialect.
Constructor
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
Factory for function/operator resolution
eval : self.Factory → (self.Ident → Option self.Expr) → self.Expr → Option self.Expr
The expression evaluator. Takes a factory, a variable store, and an
expression, and returns an optional evaluated expression.
-
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.evalFully.
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 request inlining during the partial
evaluation transform, when applied.
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;
4.5. 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.
Constructors
call {P : PureExpr} (procName : String)
(args : List (CallArg P)) (md : MetaData P) : CmdExt P
A procedure call with the given name and arguments.
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 typeImperative.CallArg (P : PureExpr) : Type Imperative.CallArg (P : PureExpr) : Type
A call argument is either an input expression, an in-out variable, or an
output variable.
Constructors
inoutArg {P : PureExpr} (id : P.Ident) : CallArg P
An input-output argument: a mutable variable passed by reference.
outArg {P : PureExpr} (id : P.Ident) : CallArg P
An output-only argument: a variable whose final value is returned to the caller.
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.6. 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.6.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.6.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.
🔗defCore.Procedure.Spec : Type
Core.Procedure.Spec : Type
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.
🔗defCore.Procedure.Check : Type
Core.Procedure.Check : Type
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.
🔗defCore.Procedure.CheckAttr : Type
Core.Procedure.CheckAttr : Type
The check/free attribute of a specification clause.
4.6.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.6.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.
4.6.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.6.6. The Procedure type🔗
🔗defCore.Procedure : Type
Core.Procedure : Type
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.7. 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 distinct declaration (asserting that a list of expressions are pairwise distinct),
-
a procedure,
-
a (non-recursive) function, or
-
a mutually recursive function block.
🔗inductive typeCore.Decl : Type
Core.Decl : Type
A Strata Core declaration.
Note: constants are 0-ary functions.
Constructors
type (t : TypeDecl) (md : MetaData Expression) : Decl
A type declaration (abstract type, type synonym, or algebraic datatype).
distinct (name : Expression.Ident)
(es : List Expression.Expr) (md : MetaData Expression) :
Decl
A distinct assertion: the given expressions are pairwise distinct.
recFuncBlock (fs : List Function)
(md : MetaData Expression) : Decl
A mutually recursive function block.
🔗structureCore.Program : Type
Core.Program : Type
A Core.Program is an ordered list of declarations.
Constructor
Fields
decls : Decls
The declarations that make up this program.