The Strata Core Language

The Strata Core Language Definition

Table of Contents

  1. 1. Introduction
  2. 2. Lambda
  3. 3. Imperative
  4. 4. Strata Core
  5. 5. Semantics

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.

Strata hourglass diagram

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:

  1. Sections 2 and 3 describe Lambda and Imperative as generic, reusable building blocks.

  2. Section 4 describes how Strata Core assembles these blocks into a concrete verification language with procedures, type declarations, functions, axioms, and programs.

  3. Section 5 describes 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.

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.LExpr (T : LExprParamsT) : Type
Lambda.LExpr (T : LExprParamsT) : 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

const {T : LExprParamsT} (m : T.base.Metadata)
  (c : LConst) : LExpr T

A constant (in the sense of literals).

op {T : LExprParamsT} (m : T.base.Metadata)
  (o : Identifier T.base.IDMeta) (ty : Option T.TypeType) :
  LExpr T

A built-in operation, referred to by name.

bvar {T : LExprParamsT} (m : T.base.Metadata)
  (deBruijnIndex : Nat) : LExpr T

A bound variable, in de Bruijn form.

fvar {T : LExprParamsT} (m : T.base.Metadata)
  (name : Identifier T.base.IDMeta)
  (ty : Option T.TypeType) : LExpr T

A free variable, with an optional type annotation.

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).

app {T : LExprParamsT} (m : T.base.Metadata)
  (fn e : LExpr T) : LExpr T

A function application.

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.

🔗structure
Lambda.Identifier (IDMeta : Type) : Type
Lambda.Identifier (IDMeta : Type) : Type

Identifiers with a name and additional metadata

Constructor

Lambda.Identifier.mk

Fields

name : String

A unique name.

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 type
Lambda.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.

boolConst (b : Bool) : LConst

A Boolean constant.

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
Lambda.LExprParams : Type 1
Lambda.LExprParams : Type 1

Expected interface for pure expressions that can be used to specialize the Imperative dialect.

Constructor

Lambda.LExprParams.mk

Fields

Metadata : Type

The type of metadata allowed on expressions.

IDMeta : Type

The type of metadata allowed on identifiers.

🔗structure
Lambda.LExprParamsT : Type 1
Lambda.LExprParamsT : Type 1

Extended LExprParams that includes TypeType parameter.

Constructor

Lambda.LExprParamsT.mk

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
Lambda.LMonoTy : Type
Lambda.LMonoTy : Type

Monomorphic types in Lambda. Note that all free type variables (.ftvar) are implicitly universally quantified.

Constructors

ftvar (name : TyIdentifier) : LMonoTy

A type variable.

tcons (name : String) (args : List LMonoTy) : LMonoTy

A type constructor.

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.

🔗def
Lambda.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 type
Lambda.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:

  1. 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.

  2. 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
Lambda.LContext (T : LExprParams) : Type
Lambda.LContext (T : LExprParams) : Type

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

Lambda.LContext.mk

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.

🔗structure
Lambda.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

Lambda.TContext.mk

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
Lambda.LExpr.HasType {T : LExprParams} [DecidableEq T.IDMeta]
  [Hashable T.IDMeta] (C : LContext T) :
  TContext T.IDMeta → LExpr T.mono → LTy → Prop
Lambda.LExpr.HasType {T : LExprParams}
  [DecidableEq T.IDMeta]
  [Hashable T.IDMeta] (C : LContext T) :
  TContext T.IDMeta →
    LExpr T.mono → LTy → Prop

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

tbool_const {T : LExprParams} [DecidableEq T.IDMeta]
  [Hashable T.IDMeta] {C : LContext T}
  (Γ : TContext T.IDMeta) (m : T.mono.base.Metadata)
  (b : Bool) :
  C.knownTypes.containsName "bool" = true →
    LExpr.HasType C Γ (LExpr.boolConst m b)
      (LTy.forAll [] LMonoTy.bool)

A boolean constant has type .bool if bool is a known type in this context.

tint_const {T : LExprParams} [DecidableEq T.IDMeta]
  [Hashable T.IDMeta] {C : LContext T}
  (Γ : TContext T.IDMeta) (m : T.mono.base.Metadata)
  (n : Int) :
  C.knownTypes.containsName "int" = true →
    LExpr.HasType C Γ (LExpr.intConst m n)
      (LTy.forAll [] LMonoTy.int)

An integer constant has type .int if int is a known type in this context.

treal_const {T : LExprParams} [DecidableEq T.IDMeta]
  [Hashable T.IDMeta] {C : LContext T}
  (Γ : TContext T.IDMeta) (m : T.mono.base.Metadata)
  (r : Rat) :
  C.knownTypes.containsName "real" = true →
    LExpr.HasType C Γ (LExpr.realConst m r)
      (LTy.forAll [] LMonoTy.real)

A real constant has type .real if real is a known type in this context.

tstr_const {T : LExprParams} [DecidableEq T.IDMeta]
  [Hashable T.IDMeta] {C : LContext T}
  (Γ : TContext T.IDMeta) (m : T.mono.base.Metadata)
  (s : String) :
  C.knownTypes.containsName "string" = true →
    LExpr.HasType C Γ (LExpr.strConst m s)
      (LTy.forAll [] LMonoTy.string)

A string constant has type .string if string is a known type in this context.

tbitvec_const {T : LExprParams} [DecidableEq T.IDMeta]
  [Hashable T.IDMeta] {C : LContext T}
  (Γ : TContext T.IDMeta) (m : T.mono.base.Metadata)
  (n : Nat) (b : BitVec n) :
  C.knownTypes.containsName "bitvec" = true →
    LExpr.HasType C Γ (LExpr.bitvecConst m n b)
      (LTy.forAll [] (LMonoTy.bitvec n))

A bit vector constant of size n has type .bitvec n if bitvec is a known type in this context.

tvar {T : LExprParams} [DecidableEq T.IDMeta]
  [Hashable T.IDMeta] {C : LContext T}
  (Γ : TContext T.IDMeta) (m : T.mono.base.Metadata)
  (x : Identifier T.mono.base.IDMeta) (ty : LTy) :
  Γ.types.find? x = some ty →
    LExpr.HasType C Γ (LExpr.fvar m x none) ty

An un-annotated variable has the type recorded for it in Γ, if any.

tvar_annotated {T : LExprParams} [DecidableEq T.IDMeta]
  [Hashable T.IDMeta] {C : LContext T}
  (Γ : TContext T.IDMeta) (m : T.mono.base.Metadata)
  (x : Identifier T.mono.base.IDMeta) (ty_o : LTy)
  (ty_s : LMonoTy) (tys : List LMonoTy) (ann : LMonoTy) :
  Γ.types.find? x = some ty_o →
    tys.length = ty_o.boundVars.length →
      ty_o.openFull tys = ty_s →
        LExpr.AnnotCompat Γ.aliases ann ty_s →
          LExpr.HasType C Γ (LExpr.fvar m x (some ann))
            (LTy.forAll [] ty_s)

An annotated free variable has its claimed type ty_s if ty_s is an instantiation of the type ty_o recorded for it in Γ, and the annotation ann is compatible with ty_s (via substitution + alias equivalence).

tabs {T : LExprParams} [DecidableEq T.IDMeta]
  [Hashable T.IDMeta] {C : LContext T}
  (Γ : TContext T.IDMeta) (m : T.mono.base.Metadata)
  (name : String) (x : IdentT LMonoTy T.IDMeta) (x_ty : LTy)
  (e : LExpr { base := T, TypeType := LMonoTy })
  (e_ty : LTy) (o : Option LMonoTy) :
  LExpr.fresh x e →
    ∀ (hx : x_ty.isMonoType = true)
      (he : e_ty.isMonoType = true),
      LExpr.HasType C
          { types := Γ.types.insert x.fst x_ty,
            aliases := Γ.aliases }
          (LExpr.varOpen 0 x e) e_ty →
        (o = none ∨
            ∃ t,
              o = some t ∧
                LExpr.AnnotCompat Γ.aliases t
                  (x_ty.toMonoType hx)) →
          LExpr.HasType C Γ (LExpr.abs m name o e)
            (LTy.forAll []
              (LMonoTy.tcons "arrow"
                [x_ty.toMonoType hx, e_ty.toMonoType he]))

An abstraction λ x.e has type x_ty → e_ty if the claimed type of x is x_ty or None and if e has type e_ty when Γ is extended with the binding (x → x_ty).

tapp {T : LExprParams} [DecidableEq T.IDMeta]
  [Hashable T.IDMeta] {C : LContext T}
  (Γ : TContext T.IDMeta) (m : T.mono.base.Metadata)
  (e1 e2 : LExpr T.mono) (t1 t2 : LTy)
  (h1 : t1.isMonoType = true) (h2 : t2.isMonoType = true) :
  LExpr.HasType C Γ e1
      (LTy.forAll []
        (LMonoTy.tcons "arrow"
          [t2.toMonoType h2, t1.toMonoType h1])) →
    LExpr.HasType C Γ e2 t2 →
      LExpr.HasType C Γ (LExpr.app m e1 e2) t1

An application e₁e₂ has type t1 if e₁ has type t2 → t1 and e₂ has type t2.

tinst {T : LExprParams} [DecidableEq T.IDMeta]
  [Hashable T.IDMeta] {C : LContext T}
  (Γ : TContext T.IDMeta) (e : LExpr T.mono) (ty e_ty : LTy)
  (x : TyIdentifier) (x_ty : LMonoTy) :
  LExpr.HasType C Γ e ty →
    e_ty = LTy.open x x_ty ty → LExpr.HasType C Γ e e_ty

If expression e has type ty and ty is more general than e_ty, then e has type e_ty (i.e. we can instantiate ty with e_ty).

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.

tif {T : LExprParams} [DecidableEq T.IDMeta]
  [Hashable T.IDMeta] {C : LContext T}
  (Γ : TContext T.IDMeta) (m : T.mono.base.Metadata)
  (c e1 e2 : LExpr T.mono) (ty : LTy) :
  LExpr.HasType C Γ c (LTy.forAll [] LMonoTy.bool) →
    LExpr.HasType C Γ e1 ty →
      LExpr.HasType C Γ e2 ty →
        LExpr.HasType C Γ (LExpr.ite m c e1 e2) ty

If e1 and e2 have the same type ty, and c has type .bool, then .ite c e1 e2 has type ty.

teq {T : LExprParams} [DecidableEq T.IDMeta]
  [Hashable T.IDMeta] {C : LContext T}
  (Γ : TContext T.IDMeta) (m : T.mono.base.Metadata)
  (e1 e2 : LExpr T.mono) (ty : LTy) :
  LExpr.HasType C Γ e1 ty →
    LExpr.HasType C Γ e2 ty →
      LExpr.HasType C Γ (LExpr.eq m e1 e2)
        (LTy.forAll [] LMonoTy.bool)

If e1 and e2 have the same type ty, then .eq e1 e2 has type .bool.

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)) →
            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.

top {T : LExprParams} [DecidableEq T.IDMeta]
  [Hashable T.IDMeta] {C : LContext T}
  (Γ : TContext T.IDMeta) (m : T.mono.base.Metadata)
  (f : LFunc T) (op : Identifier T.mono.base.IDMeta)
  (ty : LTy) :
  C.functions[op.name]? = some f →
    f.type = Except.ok ty →
      LExpr.HasType C Γ (LExpr.op m op none) ty

An un-annotated operator has the type recorded for it in C.functions, if any.

top_annotated {T : LExprParams} [DecidableEq T.IDMeta]
  [Hashable T.IDMeta] {C : LContext T}
  (Γ : TContext T.IDMeta) (m : T.mono.base.Metadata)
  (f : LFunc T) (op : Identifier T.mono.base.IDMeta)
  (ty_o : LTy) (ty_s : LMonoTy) (tys : List LMonoTy)
  (ann : LMonoTy) :
  C.functions[op.name]? = some f →
    f.type = Except.ok ty_o →
      tys.length = ty_o.boundVars.length →
        ty_o.openFull tys = ty_s →
          LExpr.AnnotCompat Γ.aliases ann ty_s →
            LExpr.HasType C Γ (LExpr.op m op (some ann))
              (LTy.forAll [] ty_s)

Similarly to free variables, an annotated operator has its claimed type ty_s if ty_s is an instantiation of the type ty_o recorded for it in C.functions, and the annotation ann is compatible with ty_s.

talias {T : LExprParams} [DecidableEq T.IDMeta]
  [Hashable T.IDMeta] {C : LContext T}
  (Γ : TContext T.IDMeta) (e : LExpr T.mono)
  (mty mty' : LMonoTy) :
  AliasEquiv Γ.aliases mty mty' →
    LExpr.HasType C Γ e (LTy.forAll [] mty) →
      LExpr.HasType C Γ e (LTy.forAll [] mty')

Alias equivalence preserves typing: if e has type mty and mty is alias-equivalent to mty' (under the aliases in Γ), then e also has type mty'. This covers single-step expansion, subtree resolution, and their transitive composition.

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
Imperative.Cmd (P : PureExpr) : Type
Imperative.Cmd (P : PureExpr) : 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 type
Imperative.ExprOrNondet (P : PureExpr) : Type
Imperative.ExprOrNondet (P : PureExpr) :
  Type

A value that is either a deterministic expression or a non-deterministic choice.

Constructors

det {P : PureExpr} (e : P.Expr) : ExprOrNondet P

A deterministic expression.

nondet {P : PureExpr} : ExprOrNondet P

A non-deterministic (arbitrary) value.

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 type
Imperative.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

cmd {P : PureExpr} {Cmd : Type} (cmd : Cmd) : Stmt P Cmd

An atomic command.

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.

🔗def
Imperative.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 type
Imperative.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.

seq {P : PureExpr} {Cmd : Type} (s1 s2 : KleeneStmt P Cmd) :
  KleeneStmt P Cmd

Execute s1 followed by s2.

choice {P : PureExpr} {Cmd : Type}
  (s1 s2 : KleeneStmt P Cmd) : KleeneStmt P Cmd

Execute either s1 or s2, arbitrarily.

loop {P : PureExpr} {Cmd : Type} (s : KleeneStmt P Cmd) :
  KleeneStmt P Cmd

Execute s an arbitrary number of times (possibly zero).

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. Metadata🔗

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.

🔗inductive type
Imperative.MetaDataElem.Field (P : PureExpr) : Type
Imperative.MetaDataElem.Field
  (P : PureExpr) : Type

A metadata field, which can be either a variable or an arbitrary string label.

For now, we only track the variables modified by a construct, but we will expand this in the future.

Constructors

var {P : PureExpr} (v : P.Ident) : MetaDataElem.Field P

Metadata indexed by a Strata variable.

label {P : PureExpr} (l : String) : MetaDataElem.Field P

Metadata indexed by an arbitrary label.

A value can take the form of an expression, an arbitrary string, a source file range, or a boolean switch.

🔗inductive type
Imperative.MetaDataElem.Value (P : PureExpr) : Type
Imperative.MetaDataElem.Value
  (P : PureExpr) : Type

A metadata value, which can be either an expression, a message, a switch, or a provenance.

Constructors

expr {P : PureExpr} (e : P.Expr) : MetaDataElem.Value P

Metadata value in the form of a structured expression.

msg {P : PureExpr} (s : String) : MetaDataElem.Value P

Metadata value in the form of an arbitrary string.

switch {P : PureExpr} (b : Bool) : MetaDataElem.Value P

Metadata value in the form of a boolean switch.

provenance {P : PureExpr} (p : Strata.Provenance) :
  MetaDataElem.Value P

Metadata value in the form of a provenance (source location or synthesized origin).

A metadata element pairs a field with a value.

🔗structure
Imperative.MetaDataElem (P : PureExpr) : Type
Imperative.MetaDataElem (P : PureExpr) :
  Type

A metadata element

Constructor

Imperative.MetaDataElem.mk

Fields

fld : MetaDataElem.Field P

The field or key used to identify the metadata.

value : MetaDataElem.Value P

The value of the metadata.

And, finally, the metadata attached to an AST node consists of an array of metadata elements.

🔗def
Imperative.MetaData (P : PureExpr) : Type
Imperative.MetaData (P : PureExpr) : Type

Metadata is an array of tagged elements.

3.5. Instantiating Imperative🔗

Using the Imperative dialect for a concrete language requires filling in three pieces:

  1. 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
    Imperative.PureExpr : Type 1
    Imperative.PureExpr : Type 1

    Expected interface for pure expressions that can be used to specialize the Imperative dialect.

    Constructor

    Imperative.PureExpr.mk

    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.

    Expr : Type

    Expressions

    Ty : Type

    Types

    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.

  2. 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., HasVarsPure), 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.

  3. Well-formedness of the evaluator, defined in Strata/DL/Imperative/CmdSemantics.lean. The rules assume the evaluator supplied via PureExpr.eval respects a few sanity conditions on values, variable lookups, and Boolean negation. A concrete instantiation must supply witnesses for each of these predicates (or the bundle WellFormedSemanticEval) against its factory of choice. See Strata/Languages/Core/InstWellFormedSemanticsEval.lean for Strata Core's discharge of these predicates.

    🔗def
    Imperative.WellFormedSemanticEvalBool {P : PureExpr} [HasBool P]
  [HasBoolOps P] (f : P.Factory) : Prop
    Imperative.WellFormedSemanticEvalBool
  {P : PureExpr} [HasBool P]
  [HasBoolOps P] (f : P.Factory) : Prop

    The evaluator respects Boolean negation: for any store σ and expression e, P.eval f σ e = some tt iff P.eval f σ (not e) = some ff, and dually.

    🔗structure
    Imperative.WellFormedSemanticEvalVal {P : PureExpr} [HasVal P]
  (f : P.Factory) : Prop
    Imperative.WellFormedSemanticEvalVal
  {P : PureExpr} [HasVal P]
  (f : P.Factory) : Prop

    Well-formedness of a SemanticEval's value behavior, split into named clauses.

    Constructor

    Imperative.WellFormedSemanticEvalVal.mk

    Fields

    outputsAreValues : ∀ (v v' : P.Expr) (σ : SemanticStore P), WellFormedStore σ f → P.eval f σ v = some v' → HasVal.value f v'

    The evaluator produces only values (on well-formed stores).

    identityOnValues : ∀ (v' : P.Expr) (σ : P.Ident → Option P.Expr), HasVal.value f v' → P.eval f σ v' = some v'

    The evaluator is the identity on values.

    🔗def
    Imperative.WellFormedSemanticEvalVar {P : PureExpr} [HasVal P]
  [HasFvar P] (f : P.Factory) : Prop
    Imperative.WellFormedSemanticEvalVar
  {P : PureExpr} [HasVal P] [HasFvar P]
  (f : P.Factory) : Prop

    The evaluator resolves free variables via the store: on a well-formed store, evaluating a free-variable expression yields its store binding.

    🔗def
    Imperative.WellFormedSemanticEvalExprCongr {P : PureExpr} [HasVal P]
  [HasFvars P] (f : P.Factory) : Prop
    Imperative.WellFormedSemanticEvalExprCongr
  {P : PureExpr} [HasVal P] [HasFvars P]
  (f : P.Factory) : Prop

    The evaluator agrees on well-formed stores that agree on the free variables of the expression under evaluation.

    🔗structure
    Imperative.WellFormedSemanticEval {P : PureExpr} [HasBool P]
  [HasBoolOps P] [HasFvar P] [HasFvars P] [HasInt P] [HasIntOps P]
  [HasSubstFvar P] (f : P.Factory) : Prop
    Imperative.WellFormedSemanticEval
  {P : PureExpr} [HasBool P]
  [HasBoolOps P] [HasFvar P] [HasFvars P]
  [HasInt P] [HasIntOps P]
  [HasSubstFvar P] (f : P.Factory) : Prop

    Bundle of well-formedness conditions on P.eval against a factory f.

    Constructor

    Imperative.WellFormedSemanticEval.mk

    Fields

    bool : WellFormedSemanticEvalBool f

    The evaluator respects boolean negation: eval e = some tt iff eval (not e) = some ff, and dually.

    val : WellFormedSemanticEvalVal f

    The evaluator only outputs values and is the identity on values.

    var : WellFormedSemanticEvalVar f

    The evaluator resolves free variables via the store.

    exprCongr : WellFormedSemanticEvalExprCongr f

    The evaluator agrees on stores that agree on free variables.

    int : WellFormedSemanticEvalInt f

    The evaluator reduces integer comparisons to booleans.

    mono : WellFormedSemanticEvalMono f

    The evaluator is monotone under store extension.

    rename : WellFormedSemanticEvalRename f

    The evaluator commutes with variable renaming (targets defined).

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:

  1. Abstract types (type Name _ ...;): Opaque type constructors with a given arity.

  2. Type synonyms (type Name x y = ...;): Named aliases for existing types, which may be parameterized by type variables.

  3. 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:

  1. Constructors: functions that create values of the datatype (e.g., None() : Option<T>, Cons(head: T, tail: List<T>) : List<T>).

  2. 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).

  3. 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:

  • The measure at the call site is non-negative (0 <= call_measure).

  • The measure strictly decreases (call_measure < caller_measure).

A function that fails its termination check will produce a verification failure on its _terminates_ obligations.

4.3.1.5. Current Limitations🔗

  • Polymorphic recursive functions are not yet supported.

  • 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🔗

Strata Core extends the generic Imperative 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.

🔗inductive type
Core.CmdExt (P : PureExpr) : Type
Core.CmdExt (P : PureExpr) : Type

Extend Imperative's commands by adding a procedure call.

Constructors

cmd {P : PureExpr} (c : Cmd P) : CmdExt P

A standard imperative command.

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 type
Core.CallArg (P : PureExpr) : Type
Core.CallArg (P : PureExpr) : Type

A call argument is either an input expression, an in-out variable, or an output variable.

Constructors

inArg {P : PureExpr} (e : P.Expr) : CallArg P

An input argument: a by-value expression.

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.

🔗structure
Core.Procedure.Header : Type
Core.Procedure.Header : Type

The header of a procedure: its name, type parameters, and input/output signatures.

Constructor

Core.Procedure.Header.mk

Fields

name : CoreIdent

The procedure's name.

typeArgs : List TyIdentifier

Type parameters for polymorphic procedures.

inputs : LMonoTySignature

Input parameters: passed by value from caller to callee (immutable in body).

outputs : LMonoTySignature

Output parameters: passed by value from callee to caller (mutable in body).

noFilter : Bool

If true, FilterProcedures will never remove this procedure.

4.6.1. Parameters🔗

Each procedure has three groups of parameters:

  1. Input parameters (name : T): Passed by value from the caller to the callee. They are immutable within the procedure body.

  2. 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.

  3. 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.

🔗structure
Core.Procedure.Spec : Type
Core.Procedure.Spec : Type

The specification (contract) of a procedure.

  • preconditions: Labeled boolean expressions that must hold before the procedure executes. Checked (asserted) at call sites unless marked Free.

  • postconditions: Labeled boolean expressions that must hold when the procedure returns. May reference old v for pre-state values. Assumed at call sites unless the implementation is being verified.

Constructor

Core.Procedure.Spec.mk

Fields

preconditions : ListMap CoreLabel Procedure.Check

Labeled preconditions (requires clauses).

postconditions : ListMap CoreLabel Procedure.Check

Labeled postconditions (ensures clauses).

Each specification clause is represented by Procedure.Check, pairing a boolean expression with an optional Free attribute and metadata.

🔗structure
Core.Procedure.Check : Type
Core.Procedure.Check : Type

A single specification clause: a boolean expression with an optional Free attribute and optional metadata.

Constructor

Core.Procedure.Check.mk

Fields

expr : Expression.Expr

The boolean expression of this specification clause.

attr : Procedure.CheckAttr

Whether this clause is checked (Default) or free (Free).

md : MetaData Expression

Optional metadata (e.g., source location).

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.

🔗inductive type
Core.Procedure.CheckAttr : Type
Core.Procedure.CheckAttr : Type

Attribute controlling whether a specification clause is checked or free.

  • Default: The clause is checked (asserted at call sites for preconditions, checked on exit for postconditions).

  • Free: The clause is assumed but not checked. 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.

See Section 8.1 of "This is Boogie 2" for motivation.

Constructors

Free : Procedure.CheckAttr

The clause is free: assumed but not checked.

Default : Procedure.CheckAttr

The clause is checked (default behavior).

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.

The semantics of a call are:

  1. Evaluate the argument expressions e₁, ..., eₙ.

  2. Assert each (non-free) precondition, substituting actuals for formals.

  3. Havoc the output variables y₁, ..., yₘ.

  4. Assume each postcondition, substituting actuals for formals and binding old v to the value of v immediately before the call.

  5. Update the caller's state with the new values of the output variables.

This enables modular verification: each procedure is verified against its contract independently, and callers reason only about the contract.

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🔗

🔗structure
Core.Procedure : Type
Core.Procedure : Type

A Strata Core procedure: the main verification unit.

A procedure consists of a header (name, type parameters, input/output signatures), a specification (contract), and an optional body (list of statements or a CFG). If the body is empty, the procedure is abstract and can only be reasoned about via its contract. If the body is present, it is verified against the specification.

Constructor

Core.Procedure.mk

Fields

header : Procedure.Header

The procedure header: name, type parameters, and parameter signatures.

spec : Procedure.Spec

The procedure's contract: preconditions and postconditions. There is no modifies clause: a body may write only its outputs and locals, enforced by the modification-rights check (checkModificationRights) during type checking.

body : Procedure.Body

The procedure body.

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 type
Core.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).

ax (a : Axiom) (md : MetaData Expression) : Decl

An axiom declaration.

distinct (name : Expression.Ident)
  (es : List Expression.Expr) (md : MetaData Expression) :
  Decl

A distinct assertion: the given expressions are pairwise distinct.

proc (d : Procedure) (md : MetaData Expression) : Decl

A procedure declaration.

func (f : Function) (md : MetaData Expression) : Decl

A function declaration.

recFuncBlock (fs : List Function)
  (md : MetaData Expression) : Decl

A mutually recursive function block.

🔗structure
Core.Program : Type
Core.Program : Type

A Core.Program is an ordered list of declarations.

Constructor

Core.Program.mk

Fields

decls : Decls

The declarations that make up this program.

5. Semantics🔗

This section describes the formal semantics of the Strata Core building blocks. The layers compose: Lambda expressions are reduced via small-step reduction or interpreted via a denotational semantics. Commands use an expression evaluator over a variable store. Statements thread configurations through commands, managing control flow.

5.1. Lambda Operational Semantics🔗

The operational semantics of the LExpr type are specified using the small-step inductive relation Lambda.Step. This relation is parameterized by a Factory, which describes built-in functions via an optional body and/or evaluation function.

🔗inductive predicate
Lambda.Step {Tbase : LExprParams} [DecidableEq Tbase.IDMeta]
  [Inhabited Tbase.IDMeta] (F : Lambda.Factory Tbase)
  (rf : Lambda.Env Tbase) : LExpr Tbase.mono → LExpr Tbase.mono → Prop
Lambda.Step {Tbase : LExprParams}
  [DecidableEq Tbase.IDMeta]
  [Inhabited Tbase.IDMeta]
  (F : Lambda.Factory Tbase)
  (rf : Lambda.Env Tbase) :
  LExpr Tbase.mono →
    LExpr Tbase.mono → Prop

A small-step semantics for LExpr.

Currently only defined for expressions paremeterized by LMonoTy, but it will be expanded to an arbitrary type in the future.

The order of constructors matter because the constructor tactic will rely on it.

This small-step definitions faithfully follows the behavior of LExpr.eval, except that:

  1. This inductive definition may get stuck early when there is no assignment to a free variable available.

  2. This semantics does not describe how metadata must change, because metadata must not affect evaluation semantics. Different concrete evaluators like LExpr.eval can have different strategy for updating metadata.

Constructors

expand_fvar {Tbase : LExprParams} [DecidableEq Tbase.IDMeta]
  [Inhabited Tbase.IDMeta] {F : Lambda.Factory Tbase}
  {rf : Lambda.Env Tbase} {m : Tbase.mono.base.Metadata}
  {ty : Option Tbase.mono.TypeType} (x : Tbase.Identifier)
  (e : LExpr Tbase.mono) :
  rf x = some e → Step F rf (LExpr.fvar m x ty) e

A free variable. Stuck if fvar does not exist in FreeVarMap.

beta {Tbase : LExprParams} [DecidableEq Tbase.IDMeta]
  [Inhabited Tbase.IDMeta] {F : Lambda.Factory Tbase}
  {rf : Lambda.Env Tbase} {m1 m2 : Tbase.mono.base.Metadata}
  {name : String} {ty : Option Tbase.mono.TypeType}
  (e1 e2 eres : LExpr Tbase.mono) :
  eres = LExpr.subst (fun x => e2) e1 →
    Step F rf (LExpr.app m1 (LExpr.abs m2 name ty e1) e2)
      eres

Beta reduction. The argument e2 need not be a canonical value; this relaxation (compared to strict call-by-value) is necessary because LExpr.eval evaluates both sub-expressions before performing substitution and we want the semantics to be flexible enough to handle partial evaluation.

reduce_2 {Tbase : LExprParams} [DecidableEq Tbase.IDMeta]
  [Inhabited Tbase.IDMeta] {F : Lambda.Factory Tbase}
  {rf : Lambda.Env Tbase} {m m' : Tbase.mono.base.Metadata}
  (e1 e2 e2' : LExpr Tbase.mono) :
  Step F rf e2 e2' →
    Step F rf (LExpr.app m e1 e2) (LExpr.app m' e1 e2')

Argument evaluation: reduce the argument of an application. Note: this rule does NOT require the function part to be a canonical value. Unlike the call-by-value strategy, this allows stepping any argument of an application, which is needed for factory calls where LExpr.eval evaluates all arguments independently (not left-to-right) with possibly limited fuels.

reduce_1 {Tbase : LExprParams} [DecidableEq Tbase.IDMeta]
  [Inhabited Tbase.IDMeta] {F : Lambda.Factory Tbase}
  {rf : Lambda.Env Tbase} {m m' : Tbase.mono.base.Metadata}
  (e1 e1' e2 : LExpr Tbase.mono) :
  Step F rf e1 e1' →
    Step F rf (LExpr.app m e1 e2) (LExpr.app m' e1' e2)

Function application.

ite_reduce_then {Tbase : LExprParams}
  [DecidableEq Tbase.IDMeta] [Inhabited Tbase.IDMeta]
  {F : Lambda.Factory Tbase} {rf : Lambda.Env Tbase}
  {m mc : Tbase.mono.base.Metadata}
  (ethen eelse : LExpr Tbase.mono) :
  Step F rf
    (LExpr.ite m (LExpr.const mc (LConst.boolConst true))
      ethen eelse)
    ethen

Evaluation of ite: condition is true, select "then" branch.

ite_reduce_else {Tbase : LExprParams}
  [DecidableEq Tbase.IDMeta] [Inhabited Tbase.IDMeta]
  {F : Lambda.Factory Tbase} {rf : Lambda.Env Tbase}
  {m mc : Tbase.mono.base.Metadata}
  (ethen eelse : LExpr Tbase.mono) :
  Step F rf
    (LExpr.ite m (LExpr.const mc (LConst.boolConst false))
      ethen eelse)
    eelse

Evaluation of ite: condition is false, select "else" branch.

ite_reduce_cond {Tbase : LExprParams}
  [DecidableEq Tbase.IDMeta] [Inhabited Tbase.IDMeta]
  {F : Lambda.Factory Tbase} {rf : Lambda.Env Tbase}
  {m m' : Tbase.mono.base.Metadata}
  (econd econd' ethen eelse : LExpr Tbase.mono) :
  Step F rf econd econd' →
    Step F rf (LExpr.ite m econd ethen eelse)
      (LExpr.ite m' econd' ethen eelse)

Evaluation of ite condition.

ite_reduce_then_branch {Tbase : LExprParams}
  [DecidableEq Tbase.IDMeta] [Inhabited Tbase.IDMeta]
  {F : Lambda.Factory Tbase} {rf : Lambda.Env Tbase}
  {m m' : Tbase.mono.base.Metadata}
  (econd ethen ethen' eelse : LExpr Tbase.mono) :
  Step F rf ethen ethen' →
    Step F rf (LExpr.ite m econd ethen eelse)
      (LExpr.ite m' econd ethen' eelse)

Evaluation of ite "then" branch (when condition is not yet resolved).

ite_reduce_else_branch {Tbase : LExprParams}
  [DecidableEq Tbase.IDMeta] [Inhabited Tbase.IDMeta]
  {F : Lambda.Factory Tbase} {rf : Lambda.Env Tbase}
  {m m' : Tbase.mono.base.Metadata}
  (econd ethen eelse eelse' : LExpr Tbase.mono) :
  Step F rf eelse eelse' →
    Step F rf (LExpr.ite m econd ethen eelse)
      (LExpr.ite m' econd ethen eelse')

Evaluation of ite "else" branch (when condition is not yet resolved).

eq_reduce_true {Tbase : LExprParams}
  [DecidableEq Tbase.IDMeta] [Inhabited Tbase.IDMeta]
  {F : Lambda.Factory Tbase} {rf : Lambda.Env Tbase}
  {m mc : Tbase.mono.base.Metadata}
  (e1 e2 : LExpr Tbase.mono) :
  LExpr.eql F e1 e2 = some true →
    Step F rf (LExpr.eq m e1 e2)
      (LExpr.const mc (LConst.boolConst true))

Evaluation of equality to true. Always allowed.

eq_reduce_false {Tbase : LExprParams}
  [DecidableEq Tbase.IDMeta] [Inhabited Tbase.IDMeta]
  {F : Lambda.Factory Tbase} {rf : Lambda.Env Tbase}
  {m mc : Tbase.mono.base.Metadata}
  (e1 e2 : LExpr Tbase.mono) :
  LExpr.eql F e1 e2 = some false →
    Step F rf (LExpr.eq m e1 e2)
      (LExpr.const mc (LConst.boolConst false))

Evaluation of equality to false. Only when neither side contains a binder, because syntactic inequality under binders does not imply semantic inequality (e.g., λx. x+1 vs λx. 1+x).

eq_reduce_lhs {Tbase : LExprParams}
  [DecidableEq Tbase.IDMeta] [Inhabited Tbase.IDMeta]
  {F : Lambda.Factory Tbase} {rf : Lambda.Env Tbase}
  {m m' : Tbase.mono.base.Metadata}
  (e1 e1' e2 : LExpr Tbase.mono) :
  Step F rf e1 e1' →
    Step F rf (LExpr.eq m e1 e2) (LExpr.eq m' e1' e2)

Evaluation of the left-hand side of an equality.

eq_reduce_rhs {Tbase : LExprParams}
  [DecidableEq Tbase.IDMeta] [Inhabited Tbase.IDMeta]
  {F : Lambda.Factory Tbase} {rf : Lambda.Env Tbase}
  {m m' : Tbase.mono.base.Metadata}
  (e1 e2 e2' : LExpr Tbase.mono) :
  Step F rf e2 e2' →
    Step F rf (LExpr.eq m e1 e2) (LExpr.eq m' e1 e2')

Evaluation of the right-hand side of an equality. Note: this rule does NOT require the LHS to be a canonical value.

expand_fn {Tbase : LExprParams} [DecidableEq Tbase.IDMeta]
  [Inhabited Tbase.IDMeta] {F : Lambda.Factory Tbase}
  {rf : Lambda.Env Tbase}
  (e callee fnbody new_body : LExpr Tbase.mono)
  (args :
    List (LExpr { base := Tbase, TypeType := LMonoTy }))
  (fn : LFunc Tbase) (tySubst : Subst) :
  F.callOfLFunc e = some (callee, args, fn) →
    fn.body = some fnbody →
      fn.computeTypeSubst callee args = some tySubst →
        new_body =
            (fnbody.applySubst tySubst).substFvarsLifting
              (fn.inputs.keys.zip args) →
          Step F rf e new_body

Evaluate a built-in function when a body expression is available in the Factory argument F. This is consistent with what LExpr.eval does (modulo the inline flag). Note that it might also be possible to evaluate with eval_fn. A key correctness property is that doing so will yield the same result. Note that this rule does not enforce an evaluation order.

eval_fn {Tbase : LExprParams} [DecidableEq Tbase.IDMeta]
  [Inhabited Tbase.IDMeta] {F : Lambda.Factory Tbase}
  {rf : Lambda.Env Tbase} {m : Tbase.Metadata}
  (e callee e' : LExpr Tbase.mono)
  (args :
    List (LExpr { base := Tbase, TypeType := LMonoTy }))
  (fn : LFunc Tbase)
  (denotefn :
    Tbase.Metadata →
      List (LExpr Tbase.mono) → Option (LExpr Tbase.mono)) :
  F.callOfLFunc e = some (callee, args, fn) →
    fn.concreteEval = some denotefn →
      some e' = denotefn m args → Step F rf e e'

Evaluate a built-in function when a concrete evaluation function is available in the Factory argument F. Note that it might also be possible to evaluate with expand_fn. A key correctness property is that doing so will yield the same result. Note that this rule does not enforce an evaluation order.

abs_subst_fvars {Tbase : LExprParams}
  [DecidableEq Tbase.IDMeta] [Inhabited Tbase.IDMeta]
  {F : Lambda.Factory Tbase} {rf : Lambda.Env Tbase}
  {m : Tbase.mono.base.Metadata} {name : String}
  {ty : Option Tbase.mono.TypeType}
  {m' : Tbase.mono.base.Metadata} (body : LExpr Tbase.mono)
  (x : Tbase.Identifier) :
  x ∈ List.map Prod.fst body.freeVars →
    Step F rf (LExpr.abs m name ty body)
      (LExpr.abs m' name ty
        (LExpr.substFvarsFromEnv rf body))

Substitute free variables under an abstraction binder using the full state. This is analogous to the closure rule in lambda calculi with explicit substitutions: it substitutes all occurrences of a free variable in the body of an abstraction, even though the substitution is not represented as an explicit syntactic term.

The x ∈ freeVars body witness ensures the step only fires when the body actually has free variables. This preserves canonical_value_not_step: isCanonicalValue returns true for an abs only when it is closed (freeVars e = []), so a canonical abs has no free variables for this rule to fire on.

quant_subst_fvars_body {Tbase : LExprParams}
  [DecidableEq Tbase.IDMeta] [Inhabited Tbase.IDMeta]
  {F : Lambda.Factory Tbase} {rf : Lambda.Env Tbase}
  {m : Tbase.mono.base.Metadata} {qk : QuantifierKind}
  {name : String} {ty : Option Tbase.mono.TypeType}
  {m' : Tbase.mono.base.Metadata}
  (tr body : LExpr Tbase.mono) (x : Tbase.Identifier) :
  x ∈ List.map Prod.fst body.freeVars →
    Step F rf (LExpr.quant m qk name ty tr body)
      (LExpr.quant m' qk name ty tr
        (LExpr.substFvarsFromEnv rf body))

Substitute free variables under a quantifier binder (body). Same motivation as abs_subst_fvars.

quant_subst_fvars_trigger {Tbase : LExprParams}
  [DecidableEq Tbase.IDMeta] [Inhabited Tbase.IDMeta]
  {F : Lambda.Factory Tbase} {rf : Lambda.Env Tbase}
  {m : Tbase.mono.base.Metadata} {qk : QuantifierKind}
  {name : String} {ty : Option Tbase.mono.TypeType}
  {m' : Tbase.mono.base.Metadata}
  (tr body : LExpr Tbase.mono) (x : Tbase.Identifier) :
  x ∈ List.map Prod.fst tr.freeVars →
    Step F rf (LExpr.quant m qk name ty tr body)
      (LExpr.quant m' qk name ty
        (LExpr.substFvarsFromEnv rf tr) body)

Substitute free variables in the trigger of a quantifier. Same motivation as abs_subst_fvars.

Typically we will want to talk about arbitrarily long sequences of steps, such as from an initial expression to a value. The Lambda.StepStar relation describes the reflexive, transitive closure of the Lambda.Step relation.

🔗def
Lambda.StepStar {Tbase : LExprParams} [DecidableEq Tbase.IDMeta]
  [Inhabited Tbase.IDMeta] (F : Lambda.Factory Tbase)
  (rf : Lambda.Env Tbase) : LExpr Tbase.mono → LExpr Tbase.mono → Prop
Lambda.StepStar {Tbase : LExprParams}
  [DecidableEq Tbase.IDMeta]
  [Inhabited Tbase.IDMeta]
  (F : Lambda.Factory Tbase)
  (rf : Lambda.Env Tbase) :
  LExpr Tbase.mono →
    LExpr Tbase.mono → Prop

Multi-step execution: reflexive transitive closure of single steps.

5.2. Lambda Denotational Semantics🔗

In addition to the operational semantics, Strata provides a denotational semantics for Lambda that interprets well-typed expressions as Lean values. This enables reasoning about program meaning without stepping through individual reductions.

The denotation maps monomorphic types to Lean types via sorts. A LSort is a ground monomorphic type — an LMonoTy with no free type variables. The SortDenote function interprets sorts into Lean types: built-in sorts (bool, int, real, string, bitvec, arrow) are mapped to their Lean counterparts, and all others are delegated to a user-provided type constructor interpretation (TyConstrInterp).

🔗inductive type
Lambda.LSort : Type
Lambda.LSort : Type

A sort is a ground monomorphic type — an LMonoTy with no free type variables. We use a separate type rather than LMonoTy to avoid carrying around proofs that a type has no type variables.

Constructors

tcons (name : String) (args : List LSort) : LSort

A named type constructor applied to sort arguments.

bitvec (size : Nat) : LSort

A bit vector sort of the given size.

🔗def
Lambda.SortDenote (tcInterp : TyConstrInterp) : LSort → Type
Lambda.SortDenote
  (tcInterp : TyConstrInterp) :
  LSort → Type

Interpret a sort into a Lean Type. Built-in sorts (bool, int, real, string, bitvec, arrow) are mapped to their Lean counterparts; all others are delegated to tcInterp.

The denotation function LExpr.denote interprets a well-typed annotated expression into a Lean value of the appropriate type. It is parameterized by interpretations for type constructors, operators, and free variables. Each Lambda construct is denoted into the corresponding Lean one; for example, an if-then-else becomes a Lean if-then-else, a forall quantifier becomes a Lean forall, and so on. Since Lambda allows unbounded quantification and equality over arbitrary types, this denotation can be used only for reasoning, not for computation. Validity of a Lambda expression means that LExpr.denote evaluates to true under all possible interpretations.

5.2.1. Well-Annotated Output of Type Resolution🔗

The theorem resolve_HasTypeA establishes that when type inference (LExpr.resolve) succeeds, the resulting expression satisfies HasTypeA — i.e., the type annotations placed by resolution are internally consistent. This allows us to give well-defined denotations for all terms that pass the typechecker.

5.2.2. Consistency with Operational Semantics🔗

A key metatheoretic result is that the operational and denotational semantics agree. The theorem Step.denote_preserved states that a single evaluation step preserves the denotation of an expression. StepStar.denote_preserved lifts this to StepStar, showing that denotation is preserved across arbitrary reduction sequences.

5.3. Command Semantics🔗

The semantics of commands are specified in terms of how they interact with a program state. An execution environment (Env) bundles three components:

  1. A store mapping variables to their current values.

  2. An expression evaluator.

  3. A cumulative failure flag that is the disjunction of per-command assertion failures.

🔗structure
Imperative.Env (P : PureExpr) : Type
Imperative.Env (P : PureExpr) : Type

Execution environment: store and cumulative failure flag.

Constructor

Imperative.Env.mk

Fields

store : SemanticStore P

The current variable store.

factory : P.Factory

The expression factory used by the evaluator.

hasFailure : Bool

Cumulative failure flag — true once any command has signalled failure.

Given a state, the InitState relation describes how a variable obtains its initial value, and the UpdateState relation describes how a variable's value can change.

🔗inductive predicate
Imperative.InitState (P : PureExpr) :
  SemanticStore P → P.Ident → P.Expr → SemanticStore P → Prop
Imperative.InitState (P : PureExpr) :
  SemanticStore P →
    P.Ident →
      P.Expr → SemanticStore P → Prop

Abtract variable initialization.

This does not specify how σ is represented, only what it maps each variable to.

Constructors

init {P : PureExpr} {σ σ' : SemanticStore P} {x : P.Ident}
  {v : P.Expr} :
  σ x = none →
    σ' x = some v →
      (∀ (y : P.Ident), x ≠ y → σ' y = σ y) →
        InitState P σ x v σ'

The state σ' is be equivalent to σ except at x, where it maps to v. Requires that x mapped to nothing beforehand.

🔗inductive predicate
Imperative.UpdateState (P : PureExpr) :
  SemanticStore P → P.Ident → P.Expr → SemanticStore P → Prop
Imperative.UpdateState (P : PureExpr) :
  SemanticStore P →
    P.Ident →
      P.Expr → SemanticStore P → Prop

Abstract variable update.

This does not specify how σ is represented, only what it maps each variable to.

Constructors

update {P : PureExpr} {σ σ' : SemanticStore P} {x : P.Ident}
  {v v' : P.Expr} :
  σ x = some v' →
    σ' x = some v →
      (∀ (y : P.Ident), x ≠ y → σ' y = σ y) →
        UpdateState P σ x v σ'

The state σ' is be equivalent to σ except at x, where it maps to v. Requires that x mapped to something beforehand.

Given these state relations, the semantics of each command is specified in a standard way.

🔗inductive predicate
Imperative.EvalCmd (P : PureExpr) [HasFvar P] [HasBool P]
  [HasBoolOps P] :
  P.Factory → SemanticStore P → Cmd P → SemanticStore P → Bool → Prop
Imperative.EvalCmd (P : PureExpr)
  [HasFvar P] [HasBool P] [HasBoolOps P] :
  P.Factory →
    SemanticStore P →
      Cmd P →
        SemanticStore P → Bool → Prop

An inductively-defined operational semantics for Cmd that depends on variable lookup (σ) and expression evaluation (P.eval) functions. Commands do not modify the evaluator - only funcDecl statements do.

The Bool output parameter is a failure flag: true when the command signals an assertion failure, false otherwise. Only eval_assert_fail sets it to true; all other constructors report false.

The failure flag is accumulated in Env.hasFailure by the statement semantics (EvalStmt).

Constructors

eval_init {P : PureExpr} [HasFvar P] [HasBool P]
  [HasBoolOps P] {x✝ : P.Ty} {x✝¹ : MetaData P}
  {f : P.Factory} {σ : P.Ident → Option P.Expr}
  {e v : P.Expr} {x : P.Ident} {σ' : SemanticStore P} :
  P.eval f σ e = some v →
    InitState P σ x v σ' →
      WellFormedSemanticEvalVar f →
        EvalCmd P f σ
          (Cmd.init x x✝ (ExprOrNondet.det e) x✝¹) σ' false

If e evaluates to a value v, initialize x according to InitState.

eval_init_unconstrained {P : PureExpr} [HasFvar P]
  [HasBool P] [HasBoolOps P] {x✝ : P.Ty} {x✝¹ : MetaData P}
  {σ : SemanticStore P} {x : P.Ident} {v : P.Expr}
  {σ' : SemanticStore P} {f : P.Factory} :
  InitState P σ x v σ' →
    HasVal.value f v →
      WellFormedSemanticEvalVar f →
        EvalCmd P f σ
          (Cmd.init x x✝ ExprOrNondet.nondet x✝¹) σ' false

Initialize x with an unconstrained value (havoc semantics). The havoc'd value v is still required to be a value, so a nondet write preserves store well-formedness.

eval_set {P : PureExpr} [HasFvar P] [HasBool P]
  [HasBoolOps P] {x✝ : MetaData P} {f : P.Factory}
  {σ : P.Ident → Option P.Expr} {e v : P.Expr} {x : P.Ident}
  {σ' : SemanticStore P} :
  P.eval f σ e = some v →
    UpdateState P σ x v σ' →
      WellFormedSemanticEvalVar f →
        EvalCmd P f σ (Cmd.set x (ExprOrNondet.det e) x✝) σ'
          false

If e evaluates to a value v, assign x according to UpdateState.

eval_set_nondet {P : PureExpr} [HasFvar P] [HasBool P]
  [HasBoolOps P] {x✝ : MetaData P} {σ : SemanticStore P}
  {x : P.Ident} {v : P.Expr} {σ' : SemanticStore P}
  {f : P.Factory} :
  UpdateState P σ x v σ' →
    HasVal.value f v →
      WellFormedSemanticEvalVar f →
        EvalCmd P f σ (Cmd.set x ExprOrNondet.nondet x✝) σ'
          false

Assign x an arbitrary value v according to UpdateState. The havoc'd value v is still required to be a value, so a nondet write preserves store well-formedness.

eval_assert_pass {P : PureExpr} [HasFvar P] [HasBool P]
  [HasBoolOps P] {x✝ : String} {x✝¹ : MetaData P}
  {f : P.Factory} {σ : P.Ident → Option P.Expr}
  {e : P.Expr} :
  P.eval f σ e = some HasBool.tt →
    WellFormedSemanticEvalBool f →
      EvalCmd P f σ (Cmd.assert x✝ e x✝¹) σ false

Assert passes: e evaluates to true, no failure. The store is unchanged.

eval_assert_fail {P : PureExpr} [HasFvar P] [HasBool P]
  [HasBoolOps P] {x✝ : String} {x✝¹ : MetaData P}
  {f : P.Factory} {σ : P.Ident → Option P.Expr}
  {e : P.Expr} :
  P.eval f σ e = some HasBool.ff →
    WellFormedSemanticEvalBool f →
      EvalCmd P f σ (Cmd.assert x✝ e x✝¹) σ true

Assert fails: e does not evaluate to true, failure flag is set. The store is unchanged — the command is an unconditional skip on the store, but the failure flag records the violation.

eval_assume {P : PureExpr} [HasFvar P] [HasBool P]
  [HasBoolOps P] {x✝ : String} {x✝¹ : MetaData P}
  {f : P.Factory} {σ : P.Ident → Option P.Expr}
  {e : P.Expr} :
  P.eval f σ e = some HasBool.tt →
    WellFormedSemanticEvalBool f →
      EvalCmd P f σ (Cmd.assume x✝ e x✝¹) σ false

If e evaluates to true in σ, evaluate to the same σ.

eval_cover {P : PureExpr} [HasFvar P] [HasBool P]
  [HasBoolOps P] {x✝ : String} {x✝¹ : MetaData P}
  {f : P.Factory} {σ : SemanticStore P} {e : P.Expr} :
  WellFormedSemanticEvalBool f →
    EvalCmd P f σ (Cmd.cover x✝ e x✝¹) σ false

A cover, when encountered, is essentially a skip.

5.4. Structured Statement Semantics🔗

The semantics of the Stmt type is defined in terms of configurations, represented by the Config type.

🔗inductive type
Imperative.Config (P : PureExpr) (CmdT : Type) : Type
Imperative.Config (P : PureExpr)
  (CmdT : Type) : Type

Configuration for small-step semantics, representing the current execution state. A configuration consists of:

  • The current statement (or list of statements) being executed

  • An execution environment (Env) bundling store, evaluator, and failure flag

Constructors

stmt {P : PureExpr} {CmdT : Type} :
  Stmt P CmdT → Imperative.Env P → Imperative.Config P CmdT

A single statement to execute next.

stmts {P : PureExpr} {CmdT : Type} :
  List (Stmt P CmdT) →
    Imperative.Env P → Imperative.Config P CmdT

A list of statements to execute next, in order.

terminal {P : PureExpr} {CmdT : Type} :
  Imperative.Env P → Imperative.Config P CmdT

A terminal configuration, indicating that execution has finished.

exiting {P : PureExpr} {CmdT : Type} :
  String → Imperative.Env P → Imperative.Config P CmdT

An exiting configuration, indicating that an exit statement was encountered. The label identifies which block to exit to.

block {P : PureExpr} {CmdT : Type} :
  Option String →
    SemanticStore P →
      P.Factory →
        Imperative.Config P CmdT → Imperative.Config P CmdT

A block context: execute the inner config, then consume matching exits.

  • The block label is Option String — none denotes an unnamed block, and is only used for scoping of variables; no explicit exit statement can reach this block.

  • The SemanticStore P is the parent store at block entry; on exit, the result is projected through it so that variables initialized inside the block are not visible outside.

  • The P.Factory is the parent factory at block entry; on exit, the factory is restored so that any internal function declarations introduced inside the block are not visible outside.

seq {P : PureExpr} {CmdT : Type} :
  Imperative.Config P CmdT →
    List (Stmt P CmdT) → Imperative.Config P CmdT

A sequence context: execute the first statement (as a sub-config), then continue with the remaining statements.

The StepStmt relation describes how each type of statement transforms configurations. It is parameterized by a command evaluator and an extendFactory function (used by funcDecl to add new function definitions to the expression evaluator within a scope).

🔗inductive predicate
Imperative.StepStmt {CmdT : Type} (P : PureExpr) [HasBool P]
  [HasBoolOps P] (EvalCmd : EvalCmdParam P CmdT)
  (extendFactory : ExtendFactory P) :
  Imperative.Config P CmdT → Imperative.Config P CmdT → Prop
Imperative.StepStmt {CmdT : Type}
  (P : PureExpr) [HasBool P]
  [HasBoolOps P]
  (EvalCmd : EvalCmdParam P CmdT)
  (extendFactory : ExtendFactory P) :
  Imperative.Config P CmdT →
    Imperative.Config P CmdT → Prop

StepStmt defines a single execution step from one configuration to another. The expression evaluator is P.eval (part of the PureExpr bundle). The cumulative failure flag in Env.hasFailure is OR-ed with the per-command failure flag at each step_cmd.

Constructors

step_cmd {CmdT : Type} {P : PureExpr} [HasBool P]
  [HasBoolOps P] {EvalCmd : EvalCmdParam P CmdT}
  {extendFactory : ExtendFactory P} {c : CmdT}
  {σ' : SemanticStore P} {hasAssertFailure : Bool}
  {ρ : Imperative.Env P} :
  EvalCmd ρ.factory ρ.store c σ' hasAssertFailure →
    StepStmt P EvalCmd extendFactory
      (Config.stmt (Stmt.cmd c) ρ)
      (Config.terminal
        { store := σ', factory := ρ.factory,
          hasFailure := ρ.hasFailure || hasAssertFailure })

A command steps to terminal configuration if it evaluates successfully. The per-command failure flag hasAssertFailure is OR-ed into ρ.hasFailure to produce the new environment's flag.

step_block {CmdT : Type} {P : PureExpr} [HasBool P]
  [HasBoolOps P] {EvalCmd : EvalCmdParam P CmdT}
  {extendFactory : ExtendFactory P} {x✝ : MetaData P}
  {label : String} {ss : List (Stmt P CmdT)}
  {ρ : Imperative.Env P} :
  StepStmt P EvalCmd extendFactory
    (Config.stmt (Stmt.block label ss x✝) ρ)
    (Config.block (some label) ρ.store ρ.factory
      (Config.stmts ss ρ))

A labeled block steps to a block context that wraps its body as .stmts. The AST label label : String is lifted into .some label for the Config.block wrapper (whose label is Option String). The parent store ρ.store and parent factory are saved so that block-local variables and function declarations can be popped on exit.

step_ite_true {CmdT : Type} {P : PureExpr} [HasBool P]
  [HasBoolOps P] {EvalCmd : EvalCmdParam P CmdT}
  {extendFactory : ExtendFactory P} {x✝ : MetaData P}
  {c : P.Expr} {tss ess : List (Stmt P CmdT)}
  {ρ : Imperative.Env P} :
  P.eval ρ.factory ρ.store c = some HasBool.tt →
    WellFormedSemanticEvalBool ρ.factory →
      StepStmt P EvalCmd extendFactory
        (Config.stmt
          (Stmt.ite (ExprOrNondet.det c) tss ess x✝) ρ)
        (Config.block none ρ.store ρ.factory
          (Config.stmts tss ρ))

If the condition of an ite statement evaluates to true, step to the then branch. The branch is wrapped in a block so that variables init'd inside are projected away on exit (matching definedVars with excludeScoped = true).

step_ite_false {CmdT : Type} {P : PureExpr} [HasBool P]
  [HasBoolOps P] {EvalCmd : EvalCmdParam P CmdT}
  {extendFactory : ExtendFactory P} {x✝ : MetaData P}
  {c : P.Expr} {tss ess : List (Stmt P CmdT)}
  {ρ : Imperative.Env P} :
  P.eval ρ.factory ρ.store c = some HasBool.ff →
    WellFormedSemanticEvalBool ρ.factory →
      StepStmt P EvalCmd extendFactory
        (Config.stmt
          (Stmt.ite (ExprOrNondet.det c) tss ess x✝) ρ)
        (Config.block none ρ.store ρ.factory
          (Config.stmts ess ρ))

If the condition of an ite statement evaluates to false, step to the else branch (scoped via block wrapper).

step_ite_nondet_true {CmdT : Type} {P : PureExpr}
  [HasBool P] [HasBoolOps P] {EvalCmd : EvalCmdParam P CmdT}
  {extendFactory : ExtendFactory P} {x✝ : MetaData P}
  {tss ess : List (Stmt P CmdT)} {ρ : Imperative.Env P} :
  StepStmt P EvalCmd extendFactory
    (Config.stmt (Stmt.ite ExprOrNondet.nondet tss ess x✝)
      ρ)
    (Config.block none ρ.store ρ.factory
      (Config.stmts tss ρ))

Non-deterministic ite: step to the then branch (scoped).

step_ite_nondet_false {CmdT : Type} {P : PureExpr}
  [HasBool P] [HasBoolOps P] {EvalCmd : EvalCmdParam P CmdT}
  {extendFactory : ExtendFactory P} {x✝ : MetaData P}
  {tss ess : List (Stmt P CmdT)} {ρ : Imperative.Env P} :
  StepStmt P EvalCmd extendFactory
    (Config.stmt (Stmt.ite ExprOrNondet.nondet tss ess x✝)
      ρ)
    (Config.block none ρ.store ρ.factory
      (Config.stmts ess ρ))

Non-deterministic ite: step to the else branch (scoped).

step_loop_enter {CmdT : Type} {P : PureExpr} [HasBool P]
  [HasBoolOps P] {EvalCmd : EvalCmdParam P CmdT}
  {extendFactory : ExtendFactory P} {g : P.Expr}
  {m : Option P.Expr} {inv : List (String × P.Expr)}
  {body : List (Stmt P CmdT)} {md : MetaData P}
  {ρ : Imperative.Env P} :
  P.eval ρ.factory ρ.store g = some HasBool.tt →
    WellFormedSemanticEvalBool ρ.factory →
      StepStmt P EvalCmd extendFactory
        (Config.stmt
          (Stmt.loop (ExprOrNondet.det g) m inv body md) ρ)
        ((Config.block none ρ.store ρ.factory
              (Config.stmts body ρ)).seq
          [Stmt.loop (ExprOrNondet.det g) m inv body md])

If a loop guard is true, execute the body (followed by the loop again). Loop invariants are not evaluated during execution: they are treated purely as verification-condition annotations elsewhere, not as runtime assertions. The invariants are labeled pairs (String × P.Expr).

The body alone is wrapped in an unnamed .block, sequenced with the recursive loop. This means each iteration runs the body in its own block scope: variables init'd inside body are projected away at the end of each iteration, allowing the next iteration's body to re-init the same names.

step_loop_exit {CmdT : Type} {P : PureExpr} [HasBool P]
  [HasBoolOps P] {EvalCmd : EvalCmdParam P CmdT}
  {extendFactory : ExtendFactory P} {x✝ : MetaData P}
  {g : P.Expr} {m : Option P.Expr}
  {inv : List (String × P.Expr)} {body : List (Stmt P CmdT)}
  {ρ : Imperative.Env P} :
  P.eval ρ.factory ρ.store g = some HasBool.ff →
    WellFormedSemanticEvalBool ρ.factory →
      StepStmt P EvalCmd extendFactory
        (Config.stmt
          (Stmt.loop (ExprOrNondet.det g) m inv body x✝) ρ)
        (Config.terminal ρ)

If a loop guard is false, terminate the loop. As with step_loop_enter, loop invariants are not evaluated during execution.

step_loop_nondet_enter {CmdT : Type} {P : PureExpr}
  [HasBool P] [HasBoolOps P] {EvalCmd : EvalCmdParam P CmdT}
  {extendFactory : ExtendFactory P} {m : Option P.Expr}
  {inv : List (String × P.Expr)} {body : List (Stmt P CmdT)}
  {md : MetaData P} {ρ : Imperative.Env P} :
  StepStmt P EvalCmd extendFactory
    (Config.stmt
      (Stmt.loop ExprOrNondet.nondet m inv body md) ρ)
    ((Config.block none ρ.store ρ.factory
          (Config.stmts body ρ)).seq
      [Stmt.loop ExprOrNondet.nondet m inv body md])

Non-deterministic loop: enter the body. As with the det variant, loop invariants are not evaluated during execution; the body alone is wrapped in an unnamed .block and sequenced with the recursive loop, giving each iteration its own block scope.

step_loop_nondet_exit {CmdT : Type} {P : PureExpr}
  [HasBool P] [HasBoolOps P] {EvalCmd : EvalCmdParam P CmdT}
  {extendFactory : ExtendFactory P} {x✝ : MetaData P}
  {m : Option P.Expr} {inv : List (String × P.Expr)}
  {body : List (Stmt P CmdT)} {ρ : Imperative.Env P} :
  StepStmt P EvalCmd extendFactory
    (Config.stmt
      (Stmt.loop ExprOrNondet.nondet m inv body x✝) ρ)
    (Config.terminal ρ)

Non-deterministic loop: exit the loop.

step_exit {CmdT : Type} {P : PureExpr} [HasBool P]
  [HasBoolOps P] {EvalCmd : EvalCmdParam P CmdT}
  {extendFactory : ExtendFactory P} {x✝ : MetaData P}
  {label : String} {ρ : Imperative.Env P} :
  StepStmt P EvalCmd extendFactory
    (Config.stmt (Stmt.exit label x✝) ρ)
    (Config.exiting label ρ)

An exit statement produces an exiting configuration.

step_funcDecl {CmdT : Type} {P : PureExpr} [HasBool P]
  [HasBoolOps P] {EvalCmd : EvalCmdParam P CmdT}
  {extendFactory : ExtendFactory P} {decl : PureFunc P}
  {md : MetaData P} {ρ : Imperative.Env P} :
  StepStmt P EvalCmd extendFactory
    (Config.stmt (Stmt.funcDecl decl md) ρ)
    (Config.terminal
      { store := ρ.store,
        factory := extendFactory ρ.factory ρ.store decl,
        hasFailure := ρ.hasFailure })

A function declaration extends the factory with the new function.

step_typeDecl {CmdT : Type} {P : PureExpr} [HasBool P]
  [HasBoolOps P] {EvalCmd : EvalCmdParam P CmdT}
  {extendFactory : ExtendFactory P} {_tc : TypeConstructor}
  {_md : MetaData P} {ρ : Imperative.Env P} :
  StepStmt P EvalCmd extendFactory
    (Config.stmt (Stmt.typeDecl _tc _md) ρ)
    (Config.terminal ρ)

A type declaration is a no-op at runtime.

step_stmts_nil {CmdT : Type} {P : PureExpr} [HasBool P]
  [HasBoolOps P] {EvalCmd : EvalCmdParam P CmdT}
  {extendFactory : ExtendFactory P} {ρ : Imperative.Env P} :
  StepStmt P EvalCmd extendFactory (Config.stmts [] ρ)
    (Config.terminal ρ)

An empty list of statements steps to .terminal with no state changes.

step_stmts_cons {CmdT : Type} {P : PureExpr} [HasBool P]
  [HasBoolOps P] {EvalCmd : EvalCmdParam P CmdT}
  {extendFactory : ExtendFactory P} {s : Stmt P CmdT}
  {ss : List (Stmt P CmdT)} {ρ : Imperative.Env P} :
  StepStmt P EvalCmd extendFactory
    (Config.stmts (s :: ss) ρ) ((Config.stmt s ρ).seq ss)

To evaluate a non-empty sequence, enter a seq context that processes the first statement while remembering the remaining statements.

step_seq_inner {CmdT : Type} {P : PureExpr} [HasBool P]
  [HasBoolOps P] {EvalCmd : EvalCmdParam P CmdT}
  {extendFactory : ExtendFactory P}
  {inner inner' : Imperative.Config P CmdT}
  {ss : List (Stmt P CmdT)} :
  StepStmt P EvalCmd extendFactory inner inner' →
    StepStmt P EvalCmd extendFactory (inner.seq ss)
      (inner'.seq ss)

A seq context steps its inner config forward.

step_seq_done {CmdT : Type} {P : PureExpr} [HasBool P]
  [HasBoolOps P] {EvalCmd : EvalCmdParam P CmdT}
  {extendFactory : ExtendFactory P} {ρ' : Imperative.Env P}
  {ss : List (Stmt P CmdT)} :
  StepStmt P EvalCmd extendFactory
    ((Config.terminal ρ').seq ss) (Config.stmts ss ρ')

When the inner config of a seq reaches terminal, continue with the remaining statements.

step_seq_exit {CmdT : Type} {P : PureExpr} [HasBool P]
  [HasBoolOps P] {EvalCmd : EvalCmdParam P CmdT}
  {extendFactory : ExtendFactory P} {label : String}
  {ρ' : Imperative.Env P} {ss : List (Stmt P CmdT)} :
  StepStmt P EvalCmd extendFactory
    ((Config.exiting label ρ').seq ss)
    (Config.exiting label ρ')

When the inner config of a seq exits, propagate the exit (skip remaining statements).

step_block_body {CmdT : Type} {P : PureExpr} [HasBool P]
  [HasBoolOps P] {EvalCmd : EvalCmdParam P CmdT}
  {extendFactory : ExtendFactory P}
  {inner inner' : Imperative.Config P CmdT}
  {label : Option String} {σ_parent : SemanticStore P}
  {f_parent : P.Factory} :
  StepStmt P EvalCmd extendFactory inner inner' →
    StepStmt P EvalCmd extendFactory
      (Config.block label σ_parent f_parent inner)
      (Config.block label σ_parent f_parent inner')

A block context steps its inner body one step forward. The inner body can be any config (stmts, seq, etc.).

step_block_done {CmdT : Type} {P : PureExpr} [HasBool P]
  [HasBoolOps P] {EvalCmd : EvalCmdParam P CmdT}
  {extendFactory : ExtendFactory P} {label : Option String}
  {σ_parent : SemanticStore P} {f_parent : P.Factory}
  {ρ' : Imperative.Env P} :
  StepStmt P EvalCmd extendFactory
    (Config.block label σ_parent f_parent
      (Config.terminal ρ'))
    (Config.terminal
      { store := projectStore σ_parent ρ'.store,
        factory := f_parent, hasFailure := ρ'.hasFailure })

When a block's inner body reaches terminal, the block terminates. The resulting store is projected through the parent store: only variables that existed before the block keep their (possibly updated) values; variables initialized inside the block are discarded. The evaluator is restored to the parent's: function declarations introduced inside the block are not visible outside.

step_block_exit_match {CmdT : Type} {P : PureExpr}
  [HasBool P] [HasBoolOps P] {EvalCmd : EvalCmdParam P CmdT}
  {extendFactory : ExtendFactory P} {label : Option String}
  {σ_parent : SemanticStore P} {f_parent : P.Factory}
  {l : String} {ρ' : Imperative.Env P} :
  label = some l →
    StepStmt P EvalCmd extendFactory
      (Config.block label σ_parent f_parent
        (Config.exiting l ρ'))
      (Config.terminal
        { store := projectStore σ_parent ρ'.store,
          factory := f_parent,
          hasFailure := ρ'.hasFailure })

When a block's inner body exits with a matching label, the block consumes it. Store and factory are projected/restored.

step_block_exit_mismatch {CmdT : Type} {P : PureExpr}
  [HasBool P] [HasBoolOps P] {EvalCmd : EvalCmdParam P CmdT}
  {extendFactory : ExtendFactory P} {label : Option String}
  {σ_parent : SemanticStore P} {f_parent : P.Factory}
  {l : String} {ρ' : Imperative.Env P} :
  label ≠ some l →
    StepStmt P EvalCmd extendFactory
      (Config.block label σ_parent f_parent
        (Config.exiting l ρ'))
      (Config.exiting l
        { store := projectStore σ_parent ρ'.store,
          factory := f_parent,
          hasFailure := ρ'.hasFailure })

When a block's inner body exits with a non-matching label, the exit propagates. Includes the case where the block's own label is .none (anonymous loop/ite wrapper, which never matches a labeled exit) as well as any other mismatched .some label. Store and factory are projected/restored since we're leaving this block.

The Imperative.StepStmtStar relation describes the reflexive, transitive closure of the Imperative.StepStmt relation.

🔗def
Imperative.StepStmtStar {CmdT : Type} (P : PureExpr) [HasBool P]
  [HasBoolOps P] (EvalCmd : EvalCmdParam P CmdT)
  (extendFactory : ExtendFactory P) :
  Imperative.Config P CmdT → Imperative.Config P CmdT → Prop
Imperative.StepStmtStar {CmdT : Type}
  (P : PureExpr) [HasBool P]
  [HasBoolOps P]
  (EvalCmd : EvalCmdParam P CmdT)
  (extendFactory : ExtendFactory P) :
  Imperative.Config P CmdT →
    Imperative.Config P CmdT → Prop

A multi-step execution of Imperative.

5.5. Non-deterministic Statement Semantics🔗

The semantics of KleeneStmt follow the same small-step pattern, with configurations (KleeneConfig) that can be: executing a single statement, in a sequence context, or terminal.

🔗inductive type
Imperative.KleeneConfig (P : PureExpr) (CmdT : Type) : Type
Imperative.KleeneConfig (P : PureExpr)
  (CmdT : Type) : Type

Configurations for small-step execution of KleeneStmt.

Constructors

stmt {P : PureExpr} {CmdT : Type} :
  KleeneStmt P CmdT → Imperative.Env P → KleeneConfig P CmdT

Executing a single nondeterministic statement.

seq {P : PureExpr} {CmdT : Type} :
  KleeneConfig P CmdT →
    KleeneStmt P CmdT → KleeneConfig P CmdT

Sequencing: execute the left config, then continue with the right stmt.

terminal {P : PureExpr} {CmdT : Type} :
  Imperative.Env P → KleeneConfig P CmdT

Execution has finished.

block {P : PureExpr} {CmdT : Type} :
  SemanticStore P →
    KleeneConfig P CmdT → KleeneConfig P CmdT

A block context for scoping. The SemanticStore P is the parent store; on exit, variables init'd inside are projected away.

The StepKleene relation describes a single execution step for non-deterministic statements.

🔗inductive predicate
Imperative.StepKleene {CmdT : Type} (P : PureExpr)
  (EvalCmd : EvalCmdParam P CmdT) :
  KleeneConfig P CmdT → KleeneConfig P CmdT → Prop
Imperative.StepKleene {CmdT : Type}
  (P : PureExpr)
  (EvalCmd : EvalCmdParam P CmdT) :
  KleeneConfig P CmdT →
    KleeneConfig P CmdT → Prop

A single execution step for non-deterministic (Kleene) statements.

Constructors

step_cmd {CmdT : Type} {P : PureExpr}
  {EvalCmd : EvalCmdParam P CmdT} {c : CmdT}
  {σ' : SemanticStore P} {hasAssertFailure : Bool}
  {ρ : Imperative.Env P} :
  EvalCmd ρ.factory ρ.store c σ' hasAssertFailure →
    StepKleene P EvalCmd
      (KleeneConfig.stmt (KleeneStmt.cmd c) ρ)
      (KleeneConfig.terminal
        { store := σ', factory := ρ.factory,
          hasFailure := ρ.hasFailure || hasAssertFailure })

A command steps to terminal.

step_seq {CmdT : Type} {P : PureExpr}
  {EvalCmd : EvalCmdParam P CmdT}
  {s1 s2 : KleeneStmt P CmdT} {ρ : Imperative.Env P} :
  StepKleene P EvalCmd (KleeneConfig.stmt (s1.seq s2) ρ)
    ((KleeneConfig.stmt s1 ρ).seq s2)

A seq statement enters a seq context.

step_choice_left {CmdT : Type} {P : PureExpr}
  {EvalCmd : EvalCmdParam P CmdT}
  {s1 s2 : KleeneStmt P CmdT} {ρ : Imperative.Env P} :
  StepKleene P EvalCmd (KleeneConfig.stmt (s1.choice s2) ρ)
    (KleeneConfig.stmt s1 ρ)

A choice nondeterministically picks the left branch.

step_choice_right {CmdT : Type} {P : PureExpr}
  {EvalCmd : EvalCmdParam P CmdT}
  {s1 s2 : KleeneStmt P CmdT} {ρ : Imperative.Env P} :
  StepKleene P EvalCmd (KleeneConfig.stmt (s1.choice s2) ρ)
    (KleeneConfig.stmt s2 ρ)

A choice nondeterministically picks the right branch.

step_loop_zero {CmdT : Type} {P : PureExpr}
  {EvalCmd : EvalCmdParam P CmdT} {s : KleeneStmt P CmdT}
  {ρ : Imperative.Env P} :
  StepKleene P EvalCmd (KleeneConfig.stmt s.loop ρ)
    (KleeneConfig.terminal ρ)

A loop can exit immediately (zero iterations).

step_loop_step {CmdT : Type} {P : PureExpr}
  {EvalCmd : EvalCmdParam P CmdT} {s : KleeneStmt P CmdT}
  {ρ : Imperative.Env P} :
  StepKleene P EvalCmd (KleeneConfig.stmt s.loop ρ)
    ((KleeneConfig.block ρ.store
          (KleeneConfig.stmt s ρ)).seq
      s.loop)

A loop can execute one iteration then continue looping. Each iteration's body runs in its own block scope, sequenced with the recursive loop step. When the body's block terminates, projection drops any variables initialized inside the body, so the next iteration starts with the same isSome-domain as the loop entry.

step_block {CmdT : Type} {P : PureExpr}
  {EvalCmd : EvalCmdParam P CmdT} {s : KleeneStmt P CmdT}
  {ρ : Imperative.Env P} :
  StepKleene P EvalCmd (KleeneConfig.stmt s.block ρ)
    (KleeneConfig.block ρ.store (KleeneConfig.stmt s ρ))

A block statement enters a block context, saving the parent store.

step_seq_inner {CmdT : Type} {P : PureExpr}
  {EvalCmd : EvalCmdParam P CmdT}
  {inner inner' : KleeneConfig P CmdT}
  {s2 : KleeneStmt P CmdT} :
  StepKleene P EvalCmd inner inner' →
    StepKleene P EvalCmd (inner.seq s2) (inner'.seq s2)

A seq context steps its inner config forward.

step_seq_done {CmdT : Type} {P : PureExpr}
  {EvalCmd : EvalCmdParam P CmdT} {ρ' : Imperative.Env P}
  {s2 : KleeneStmt P CmdT} :
  StepKleene P EvalCmd ((KleeneConfig.terminal ρ').seq s2)
    (KleeneConfig.stmt s2 ρ')

When the inner config of a seq reaches terminal, continue with the right statement.

step_block_body {CmdT : Type} {P : PureExpr}
  {EvalCmd : EvalCmdParam P CmdT}
  {inner inner' : KleeneConfig P CmdT}
  {σ_parent : SemanticStore P} :
  StepKleene P EvalCmd inner inner' →
    StepKleene P EvalCmd (KleeneConfig.block σ_parent inner)
      (KleeneConfig.block σ_parent inner')

A block context steps its inner config forward.

step_block_done {CmdT : Type} {P : PureExpr}
  {EvalCmd : EvalCmdParam P CmdT}
  {σ_parent : SemanticStore P} {ρ' : Imperative.Env P} :
  StepKleene P EvalCmd
    (KleeneConfig.block σ_parent (KleeneConfig.terminal ρ'))
    (KleeneConfig.terminal
      { store := projectStore σ_parent ρ'.store,
        factory := ρ'.factory,
        hasFailure := ρ'.hasFailure })

When a block's inner config reaches terminal, project the store.

The StepKleeneStar relation is the reflexive, transitive closure.

🔗def
Imperative.StepKleeneStar {CmdT : Type} (P : PureExpr) [HasBool P]
  [HasBoolOps P] (EvalCmd : EvalCmdParam P CmdT) :
  KleeneConfig P CmdT → KleeneConfig P CmdT → Prop
Imperative.StepKleeneStar {CmdT : Type}
  (P : PureExpr) [HasBool P]
  [HasBoolOps P]
  (EvalCmd : EvalCmdParam P CmdT) :
  KleeneConfig P CmdT →
    KleeneConfig P CmdT → Prop

Multi-step execution for non-deterministic statements: the reflexive, transitive closure of StepKleene.

5.6. Program-wide Semantics🔗

The per-component semantics above are linked to program-wide specifications via two key definitions in Specification.lean:

  • Hoare.Triple: a partial-correctness triple {Pre} s {Post} stating that if Pre holds on entry and the statement terminates, the postcondition holds and no assertion has failed.

  • AllAssertsValid: universally quantifies over all assertion sites in a statement, requiring each to hold on every reachable path.

The two are shown equivalent by hoareTriple_implies_assertValid and allAssertsValid_implies_hoareTriple.