Strata Core Semantics

The Strata Core Language Semantics

Table of Contents

  1. 1. Formal Semantics of Lambda
  2. 2. Formal Semantics of Imperative
  3. 3. Formal Semantics of Core
  4. 4. Formally Reasoning about Imperative and Strata Core

1.Β Formal Semantics of LambdaπŸ”—

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.

1.1.Β 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.

The predicate isCanonicalValue returns true for LExpr that is a value: constants, closed abstractions and quantifiers, etc.

πŸ”—def
Lambda.LExpr.isCanonicalValue {T : LExprParamsT}
  (F : Lambda.Factory T.base) (e : LExpr T) : Bool
Lambda.LExpr.isCanonicalValue
  {T : LExprParamsT}
  (F : Lambda.Factory T.base)
  (e : LExpr T) : Bool

Canonical values of LExprs.

If e:LExpr is .app, say e1 e2 .. en, e is a canonical value if (1) e1 is a constructor and e2 .. en are all canonical values, or (2) e1 is a named function f (not abstraction) and n is less than the number of arguments required to run the function f.

The theorem canonical_value_not_step confirms the intended relationship between the two notions: canonical values are precisely the normal forms of Step, so no reduction rule can fire on them.

1.1.1.Β Soundness of Partial Evaluator of LambdaπŸ”—

Alongside the relational semantics, Lambda provides an executable partial evaluator, LExpr.eval. It takes a fuel bound n and reduces an expression as far as that fuel allows, returning the resulting expression together with an EvalResult that classifies the outcome as outOfFuel, a canonical value, or a nonvalue.

The theorem eval_StepStar states the soundness of evaluator with respect to the operational semantics. For every fuel bound n, the expression LExpr.eval n F env e is reachable from e by zero or more Steps (up to metadata β€” see below).

1.1.2.Β Invariance under MetadataπŸ”—

The theorem eval_eraseMetadata_invariant srates that expressions that agree up to metadata evaluate under LExpr.eval to results that again agree up to metadata. This guarantees that the concrete metadata a front end chooses to record can never change the computed value.

1.2.Β Denotational SemanticsπŸ”—

In addition to the operational semantics, Strata provides a denotational semantics for Lambda (LExpr.denote) 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).

The denotational style has three practical advantages over the small-step relation. First, the substitution algorithm is not in the trusted base. Second, LExpr.denote produces ordinary Lean terms, so proofs can work over native Lean values instead of LExpr syntax, which can be quite verbose to manipulate (the operational semantics always operates on LExpr). Third, it gives a natural account of the forall/exists quantifiers: a quantified Lambda expression is denoted directly by the corresponding Lean quantifier (currently the rules in operational semantics are confined to computable expressions only). The small-step semantics, in turn, doesn't require the expression to be type-annotated, and remains the better tool for describing traditional programming-language concepts - such as type safety and what counts as a value - which are naturally phrased in terms of reduction and normal forms.

πŸ”—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.

1.2.1.Β Consistency with Operational SemanticsπŸ”—

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.

1.3.Β Type SystemπŸ”—

The syntax document introduces Lambda's polymorphic, Hindley-Milner typing relation HasType, which assigns type schemes (LTy) under an LContext and a TContext. For the semantics, the relevant relation is its annotated counterpart, HasTypeA.

In an annotated expression, every operator, free variable, and abstraction/quantifier binder carries an explicit LMonoTy, and HasTypeA Ξ” e Ο„ checks that those annotations are mutually consistent β€” with Ξ” the de Bruijn context giving the types of the enclosing bound variables. Because the annotations already pin down every choice, the relation is deterministic: a well-annotated expression has a unique - hence principal - type. Equivalently, HasTypeA is the declarative counterpart of the decidable checker LExpr.typeCheck, and the two are proved equivalent.

Type inference is implemented by LExpr.resolve, which elaborates a raw expression β€” inferring types and filling in the annotations that HasTypeA reads. The implementation is verified against both typing relations:

  • resolve_HasType (in LExprTypeSpec.lean) shows that a successful type inference (LExpr.resolve) implies the input expression has the inferenced type under the HasType relation.

  • resolve_HasTypeA (in LExprResolveAnnotated.lean) shows that the output expression has the inferenced type under HasTypeA.

The HasTypeA guarantee is the one that feeds the denotational semantics: it is exactly the hypothesis LExpr.denote requires, so every expression that passes the checker can be given a well-defined denotation. Also, Step.type_preserved proves the type preservation of Step with respect to HasTypeA.

2.Β Formal Semantics of ImperativeπŸ”—

2.1.Β Command SemanticsπŸ”—

The semantics of commands are specified in terms of how they interact with a program state.

πŸ”—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.

2.1.1.Β Event-Producing Command SemanticsπŸ”—

The legacy command relation reports one cumulative failure bit. The alternative EvalCmdE relation instead emits a chronological list of observations. Each assertion, assumption, or cover captures its condition and the semantic snapshot where the command was encountered.

πŸ”—structure
Imperative.EventArg (P : PureExpr) : Type
Imperative.EventArg (P : PureExpr) : Type

An argument captured by an event together with the semantic state in which it was observed. Labels and metadata are retained for assertion identity and diagnostics; condition interpretation depends only on factory, store, and expr.

Constructor

Imperative.EventArg.mk

Fields

factory : P.Factory

Expression factory active when the event was emitted.

store : SemanticStore P

Variable store observed when the event was emitted.

label : String

Source-level label identifying the observed command.

expr : P.Expr

Unevaluated condition captured by the event.

metadata : MetaData P

Source and analysis metadata attached to the command.

πŸ”—inductive type
Imperative.Event (P : PureExpr) : Type
Imperative.Event (P : PureExpr) : Type

Observable events emitted by Imperative commands.

Constructors

assert {P : PureExpr} : EventArg P β†’ Event P

An assertion condition that must hold under preceding assumptions.

assume {P : PureExpr} : EventArg P β†’ Event P

An assumption condition that constrains later observations.

cover {P : PureExpr} : EventArg P β†’ Event P

A coverage condition whose matching occurrence may be checked for satisfiability.

πŸ”—def
Imperative.Trace (P : PureExpr) : Type
Imperative.Trace (P : PureExpr) : Type

An Imperative event trace is a chronological list of assertion and assumption observations.

The event payload type is a parameter of the command-evaluator interface, so a custom command language may use its own observation type. The base Imperative commands instantiate it with Event P.

πŸ”—def
Imperative.EvalCmdParamE (P : PureExpr) (Cmd EventT : Type) : Type
Imperative.EvalCmdParamE (P : PureExpr)
  (Cmd EventT : Type) : Type

Command evaluation relation that reports an ordered event trace instead of an assertion-failure flag. The event payload type EventT is a parameter so that generic operational metatheory can be stated over an arbitrary payload; the base command semantics EvalCmdE instantiates it at Trace P.

For the base commands, the emitted trace is a deterministic function of the command, factory, and input store.

πŸ”—def
Imperative.Cmd.emittedEvents (P : PureExpr) :
  Cmd P β†’ P.Factory β†’ SemanticStore P β†’ Trace P
Imperative.Cmd.emittedEvents
  (P : PureExpr) :
  Cmd P β†’
    P.Factory β†’ SemanticStore P β†’ Trace P

The event trace emitted by a base command at its input snapshot. Assertions, assumptions, and covers emit their captured condition; all other commands are silent.

πŸ”—inductive predicate
Imperative.EvalCmdE (P : PureExpr) [HasFvar P] [HasBool P] :
  P.Factory β†’ SemanticStore P β†’ Cmd P β†’ SemanticStore P β†’ Trace P β†’ Prop
Imperative.EvalCmdE (P : PureExpr)
  [HasFvar P] [HasBool P] :
  P.Factory β†’
    SemanticStore P β†’
      Cmd P β†’
        SemanticStore P β†’ Trace P β†’ Prop

Event-producing command semantics.

Assertions, assumptions, and covers are unconditional skips on the store that emit their unevaluated condition at the input snapshot. They do not ask the partial evaluator to reduce the condition to a Boolean.

Constructors

eval_init {P : PureExpr} [HasFvar P] [HasBool P]
  {f : P.Factory} {Οƒ : P.Ident β†’ Option P.Expr}
  {e v : P.Expr} {x : P.Ident} {Οƒ' : SemanticStore P}
  {ty : P.Ty} {md : MetaData P} :
  P.eval f Οƒ e = some v β†’
    InitState P Οƒ x v Οƒ' β†’
      WellFormedSemanticEvalVar f β†’
        EvalCmdE P f Οƒ
          (Cmd.init x ty (ExprOrNondet.det e) md) Οƒ' []

Evaluate a deterministic initializer, update the store, and emit no observation.

eval_init_unconstrained {P : PureExpr} [HasFvar P]
  [HasBool P] {Οƒ : SemanticStore P} {x : P.Ident}
  {v : P.Expr} {Οƒ' : SemanticStore P} {f : P.Factory}
  {ty : P.Ty} {md : MetaData P} :
  InitState P Οƒ x v Οƒ' β†’
    HasVal.value f v β†’
      WellFormedSemanticEvalVar f β†’
        EvalCmdE P f Οƒ
          (Cmd.init x ty ExprOrNondet.nondet md) Οƒ' []

Initialize a variable with an arbitrary value and emit no observation.

eval_set {P : PureExpr} [HasFvar P] [HasBool P]
  {f : P.Factory} {Οƒ : P.Ident β†’ Option P.Expr}
  {e v : P.Expr} {x : P.Ident} {Οƒ' : SemanticStore P}
  {md : MetaData P} :
  P.eval f Οƒ e = some v β†’
    UpdateState P Οƒ x v Οƒ' β†’
      WellFormedSemanticEvalVar f β†’
        EvalCmdE P f Οƒ (Cmd.set x (ExprOrNondet.det e) md)
          Οƒ' []

Evaluate a deterministic assignment, update the store, and emit no observation.

eval_set_nondet {P : PureExpr} [HasFvar P] [HasBool P]
  {Οƒ : SemanticStore P} {x : P.Ident} {v : P.Expr}
  {Οƒ' : SemanticStore P} {f : P.Factory} {md : MetaData P} :
  UpdateState P Οƒ x v Οƒ' β†’
    HasVal.value f v β†’
      WellFormedSemanticEvalVar f β†’
        EvalCmdE P f Οƒ (Cmd.set x ExprOrNondet.nondet md) Οƒ'
          []

Assign an arbitrary value and emit no observation.

eval_assert {P : PureExpr} [HasFvar P] [HasBool P]
  {f : P.Factory} {Οƒ : SemanticStore P} {label : String}
  {e : P.Expr} {md : MetaData P} :
  EvalCmdE P f Οƒ (Cmd.assert label e md) Οƒ
    [Event.assert
        { factory := f, store := Οƒ, label := label,
          expr := e, metadata := md }]

Preserve the store and emit the captured assertion condition.

eval_assume {P : PureExpr} [HasFvar P] [HasBool P]
  {f : P.Factory} {Οƒ : SemanticStore P} {label : String}
  {e : P.Expr} {md : MetaData P} :
  EvalCmdE P f Οƒ (Cmd.assume label e md) Οƒ
    [Event.assume
        { factory := f, store := Οƒ, label := label,
          expr := e, metadata := md }]

Preserve the store and emit the captured assumption condition.

eval_cover {P : PureExpr} [HasFvar P] [HasBool P]
  {f : P.Factory} {Οƒ : SemanticStore P} {label : String}
  {e : P.Expr} {md : MetaData P} :
  EvalCmdE P f Οƒ (Cmd.cover label e md) Οƒ
    [Event.cover
        { factory := f, store := Οƒ, label := label,
          expr := e, metadata := md }]

Preserve the store and emit the captured coverage condition.

The event-producing relation agrees with that deterministic trace, and every legacy command execution has a corresponding event execution with the same resulting store.

πŸ”—theorem
Imperative.EvalCmdE.emitted_eq {P : PureExpr} [HasFvar P] [HasBool P]
  {f : P.Factory} {Οƒ Οƒ' : SemanticStore P} {c : Cmd P}
  {emitted : Trace P} (h : EvalCmdE P f Οƒ c Οƒ' emitted) :
  emitted = Cmd.emittedEvents P c f Οƒ
Imperative.EvalCmdE.emitted_eq
  {P : PureExpr} [HasFvar P] [HasBool P]
  {f : P.Factory} {Οƒ Οƒ' : SemanticStore P}
  {c : Cmd P} {emitted : Trace P}
  (h : EvalCmdE P f Οƒ c Οƒ' emitted) :
  emitted = Cmd.emittedEvents P c f Οƒ

Event-producing command evaluation emits exactly the trace selected by the command and its input snapshot.

πŸ”—theorem
Imperative.EvalCmd.toEvalCmdE {P : PureExpr} [HasFvar P] [HasBool P]
  [HasBoolOps P] {f : P.Factory} {Οƒ Οƒ' : SemanticStore P} {c : Cmd P}
  {failed : Bool} (h : EvalCmd P f Οƒ c Οƒ' failed) :
  EvalCmdE P f Οƒ c Οƒ' (Cmd.emittedEvents P c f Οƒ)
Imperative.EvalCmd.toEvalCmdE
  {P : PureExpr} [HasFvar P] [HasBool P]
  [HasBoolOps P] {f : P.Factory}
  {Οƒ Οƒ' : SemanticStore P} {c : Cmd P}
  {failed : Bool}
  (h : EvalCmd P f Οƒ c Οƒ' failed) :
  EvalCmdE P f Οƒ c Οƒ'
    (Cmd.emittedEvents P c f Οƒ)

Forgetting the failure result of an existing command execution yields an event-producing execution with the same resulting store and exactly the trace selected by Cmd.emittedEvents from the command and its input snapshot.

The converse does not hold in general because EvalCmdE treats assertions and assumptions as unconditional observations, while EvalCmd requires the partial evaluator to reduce them to a Boolean.

2.2.Β 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 (because statements are parameteric to the list of defined commands) 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.

2.2.1.Β Event-Producing Statement SemanticsπŸ”—

StepStmtE labels each statement transition with the events emitted by its active command. Administrative control-flow transitions are reused from StepStmt with a command evaluator that cannot step; they emit the empty event list. Sequence and block frames propagate the active inner step's events unchanged.

πŸ”—def
Imperative.noCommandEvalE (P : PureExpr) (CmdT : Type) :
  EvalCmdParam P CmdT
Imperative.noCommandEvalE (P : PureExpr)
  (CmdT : Type) : EvalCmdParam P CmdT

Command relation with no possible command step, used to reuse the existing administrative control-flow rules without inheriting failure-flag command behavior.

πŸ”—inductive predicate
Imperative.StepStmtE {CmdT : Type} (P : PureExpr) [HasBool P]
  [HasBoolOps P] {EventT : Type} (EvalCmd : EvalCmdParamE P CmdT EventT)
  (extendFactory : ExtendFactory P) :
  Imperative.Config P CmdT β†’
    List EventT β†’ Imperative.Config P CmdT β†’ Prop
Imperative.StepStmtE {CmdT : Type}
  (P : PureExpr) [HasBool P]
  [HasBoolOps P] {EventT : Type}
  (EvalCmd : EvalCmdParamE P CmdT EventT)
  (extendFactory : ExtendFactory P) :
  Imperative.Config P CmdT β†’
    List EventT β†’
      Imperative.Config P CmdT β†’ Prop

Event-labeled statement step. Command steps use EvalCmdParamE; existing administrative control-flow steps are reused through noCommandEvalE.

A StepStmtE derivation describes one operational step and carries one event list; it never concatenates traces. Sequence and block rules propagate the inner step's events unchanged. Administrative wrapper steps can have duplicate derivationsβ€”either lifted as a whole by step_admin or through step_seq_inner/step_block_bodyβ€”but those derivations have the same empty trace and target, so they add no observable nondeterminism. Intended choices, such as nondeterministic conditionals and loops, remain nondeterministic.

Constructors

step_cmd {CmdT : Type} {P : PureExpr} [HasBool P]
  [HasBoolOps P] {EventT : Type}
  {EvalCmd : EvalCmdParamE P CmdT EventT}
  {extendFactory : ExtendFactory P} {cmd : CmdT}
  {Οƒ' : SemanticStore P} {emitted : List EventT}
  {ρ : Imperative.Env P} :
  EvalCmd ρ.factory ρ.store cmd Οƒ' emitted β†’
    StepStmtE P EvalCmd extendFactory
      (Config.stmt (Stmt.cmd cmd) ρ) emitted
      (Config.terminal
        { store := Οƒ', factory := ρ.factory,
          hasFailure := ρ.hasFailure })

Execute one command and expose exactly the event list produced by its command semantics.

step_admin {CmdT : Type} {P : PureExpr} [HasBool P]
  [HasBoolOps P] {EventT : Type}
  {EvalCmd : EvalCmdParamE P CmdT EventT}
  {extendFactory : ExtendFactory P}
  {c c' : Imperative.Config P CmdT} :
  StepStmt P (noCommandEvalE P CmdT) extendFactory c c' β†’
    StepStmtE P EvalCmd extendFactory c [] c'

Reuse a command-free administrative StepStmt; administrative steps emit no events. This may overlap with the explicit wrapper constructors, but only as an alternative derivation of the same transition.

step_seq_inner {CmdT : Type} {P : PureExpr} [HasBool P]
  [HasBoolOps P] {EventT : Type}
  {EvalCmd : EvalCmdParamE P CmdT EventT}
  {extendFactory : ExtendFactory P}
  {inner : Imperative.Config P CmdT} {emitted : List EventT}
  {inner' : Imperative.Config P CmdT}
  {ss : List (Stmt P CmdT)} :
  StepStmtE P EvalCmd extendFactory inner emitted inner' β†’
    StepStmtE P EvalCmd extendFactory (inner.seq ss) emitted
      (inner'.seq ss)

Lift one inner sequence step.

step_block_body {CmdT : Type} {P : PureExpr} [HasBool P]
  [HasBoolOps P] {EventT : Type}
  {EvalCmd : EvalCmdParamE P CmdT EventT}
  {extendFactory : ExtendFactory P}
  {inner : Imperative.Config P CmdT} {emitted : List EventT}
  {inner' : Imperative.Config P CmdT}
  {label : Option String} {Οƒ_parent : SemanticStore P}
  {f_parent : P.Factory} :
  StepStmtE P EvalCmd extendFactory inner emitted inner' β†’
    StepStmtE P EvalCmd extendFactory
      (Config.block label Οƒ_parent f_parent inner) emitted
      (Config.block label Οƒ_parent f_parent inner')

Lift one inner block step.

The traced reflexive-transitive closure concatenates each step's event list in execution order.

πŸ”—inductive predicate
ReflTransTrace {A E : Type} (r : A β†’ List E β†’ A β†’ Prop) :
  A β†’ List E β†’ A β†’ Prop
ReflTransTrace {A E : Type}
  (r : A β†’ List E β†’ A β†’ Prop) :
  A β†’ List E β†’ A β†’ Prop

IsReflexive-transitive closure of a relation whose steps emit a list of observations. The accumulated trace is chronological: a step's output precedes the trace emitted by the remaining execution.

Constructors

refl {A E : Type} {r : A β†’ List E β†’ A β†’ Prop} (x : A) :
  ReflTransTrace r x [] x

IsReflexive execution emits the empty trace.

step {A E : Type} {r : A β†’ List E β†’ A β†’ Prop} (x : A)
  (emitted : List E) (y : A) (rest : List E) (z : A) :
  r x emitted y β†’
    ReflTransTrace r y rest z β†’
      ReflTransTrace r x (emitted ++ rest) z

Prepend one labeled step to a traced execution, concatenating its events before the remaining trace.

πŸ”—def
Imperative.StepStmtStarE {CmdT : Type} (P : PureExpr) [HasBool P]
  [HasBoolOps P] {EventT : Type} (EvalCmd : EvalCmdParamE P CmdT EventT)
  (extendFactory : ExtendFactory P) :
  Imperative.Config P CmdT β†’
    List EventT β†’ Imperative.Config P CmdT β†’ Prop
Imperative.StepStmtStarE {CmdT : Type}
  (P : PureExpr) [HasBool P]
  [HasBoolOps P] {EventT : Type}
  (EvalCmd : EvalCmdParamE P CmdT EventT)
  (extendFactory : ExtendFactory P) :
  Imperative.Config P CmdT β†’
    List EventT β†’
      Imperative.Config P CmdT β†’ Prop

Structured multi-step execution with a chronological event trace. ReflTransTrace concatenates the event list from each successive step as emitted ++ rest; this closure, not StepStmtE, performs trace concatenation.

For base Imperative commands, the active configuration also determines its next event list. The compatibility theorem normalizes only the legacy target's cumulative failure flag because event semantics records assertion observations in the trace instead of updating that bit.

πŸ”—def
Imperative.Config.emittedEvents {P : PureExpr} :
  Imperative.Config P (Cmd P) β†’ Trace P
Imperative.Config.emittedEvents
  {P : PureExpr} :
  Imperative.Config P (Cmd P) β†’ Trace P

Events emitted by the active base command in the next statement step. Administrative configurations and non-command statements are silent.

πŸ”—def
Imperative.Config.withFailure {P : PureExpr} {CmdT : Type}
  (hasFailure : Bool) :
  Imperative.Config P CmdT β†’ Imperative.Config P CmdT
Imperative.Config.withFailure
  {P : PureExpr} {CmdT : Type}
  (hasFailure : Bool) :
  Imperative.Config P CmdT β†’
    Imperative.Config P CmdT

Replace the active environment's cumulative failure flag, preserving the configuration's control shape, stores, and factories.

πŸ”—theorem
Imperative.StepStmt.toStepStmtE {P : PureExpr} [HasFvar P] [HasBool P]
  [HasBoolOps P] (extendFactory : ExtendFactory P)
  {c c' : Imperative.Config P (Cmd P)}
  (h : StepStmt P (EvalCmd P) extendFactory c c') :
  StepStmtE P (EvalCmdE P) extendFactory c c.emittedEvents
    (Config.withFailure c.getEnv.hasFailure c')
Imperative.StepStmt.toStepStmtE
  {P : PureExpr} [HasFvar P] [HasBool P]
  [HasBoolOps P]
  (extendFactory : ExtendFactory P)
  {c c' : Imperative.Config P (Cmd P)}
  (h :
    StepStmt P (EvalCmd P) extendFactory c
      c') :
  StepStmtE P (EvalCmdE P) extendFactory c
    c.emittedEvents
    (Config.withFailure
      c.getEnv.hasFailure c')

A legacy statement step is reproduced by the event semantics with the source configuration's deterministic active-command trace. The event target is the legacy target with its cumulative failure flag normalized back to the source flag, because event semantics records assertion observations in the trace instead of mutating hasFailure.

2.3.Β Control-Flow Graph SemanticsπŸ”—

The unstructured control-flow graphs introduced in "The Strata Core Language Syntax" are given a small-step, per-command operational semantics. Execution state is tracked by a CFGConfig.

πŸ”—inductive type
Imperative.CFGConfig (l CmdT : Type) (P : PureExpr) : Type
Imperative.CFGConfig (l CmdT : Type)
  (P : PureExpr) : Type

Configuration for small-step semantics. A configuration is one of:

  • .atBlock t Οƒ f β€” about to fetch the block at label t.

  • .inBlock t cs tr Οƒ f β€” partway through a block: cs are the residual commands that still need to execute, tr is the block's transfer.

  • .terminal Οƒ f β€” execution has finished normally.

  • .exiting l Οƒ f β€” execution escaped via an uncaught exit to label l.

The configuration is parameterised by the command type CmdT so that the mid-block residual command list and the block's transfer have the right type at the level of the configuration.

Constructors

atBlock {l CmdT : Type} {P : PureExpr} :
  l β†’ SemanticStore P β†’ Bool β†’ CFGConfig l CmdT P

Fetch-and-start: about to look up label l in the CFG.

inBlock {l CmdT : Type} {P : PureExpr} :
  l β†’
    List CmdT β†’
      DetTransferCmd l P β†’
        SemanticStore P β†’ Bool β†’ CFGConfig l CmdT P

Mid-block: residual commands cs and the block's transfer tr survive, with the running store and failure flag.

terminal {l CmdT : Type} {P : PureExpr} :
  SemanticStore P β†’ Bool β†’ CFGConfig l CmdT P

Halt.

exiting {l CmdT : Type} {P : PureExpr} :
  l β†’ SemanticStore P β†’ Bool β†’ CFGConfig l CmdT P

Escape via an uncaught structured exit to label l. A top-level outcome, like terminal, but tagged with the escaping label so that the outcome kind (normal halt vs. escaping exit) is observable.

The StepCFG relation takes one execution step over a deterministic CFG.

πŸ”—inductive predicate
Imperative.StepCFG {l CmdT : Type} [BEq l] (P : PureExpr)
  (EvalCmd : EvalCmdParam P CmdT) (extendFactory : ExtendFactory P)
  (fac : P.Factory) [HasBool P] [HasBoolOps P] [HasVal P] [HasFvars P] :
  CFG l (DetBlock l CmdT P) β†’
    CFGConfig l CmdT P β†’ CFGConfig l CmdT P β†’ Prop
Imperative.StepCFG {l CmdT : Type} [BEq l]
  (P : PureExpr)
  (EvalCmd : EvalCmdParam P CmdT)
  (extendFactory : ExtendFactory P)
  (fac : P.Factory) [HasBool P]
  [HasBoolOps P] [HasVal P] [HasFvars P] :
  CFG l (DetBlock l CmdT P) β†’
    CFGConfig l CmdT P β†’
      CFGConfig l CmdT P β†’ Prop

Per-command small-step operational semantics for a deterministic CFG.

There are five constructors:

  • fetch: from .atBlock t, look up the block at label t and unfold to .inBlock t b.cmds b.transfer.

  • step_cmd: from .inBlock t (c :: cs) tr, evaluate the head command via EvalCmd and step to .inBlock t cs tr.

  • goto_true / goto_false: from .inBlock t [] (.condGoto c tlbl elbl _), evaluate the condition and jump to .atBlock tlbl or .atBlock elbl.

  • finish: from .inBlock t [] (.finish _), halt at .terminal.

Note: the unconditional .goto k transfer is the special case condGoto HasBool.tt k k _ (definitionally equal); we therefore do not need a separate goto constructor here β€” proofs rewrite .goto k as .condGoto HasBool.tt k k _ and use goto_true.

The expression evaluator is P.eval (part of the PureExpr bundle), applied against a single factory fac : P.Factory that indexes the whole relation. Fixing one factory across the relation makes the conditional transfer rules deterministic: for a given condGoto, fac pins the condition's value, so at most one of goto_true / goto_false applies.

Constructors

fetch {l CmdT : Type} [BEq l] {P : PureExpr}
  {EvalCmd : EvalCmdParam P CmdT}
  {extendFactory : ExtendFactory P} {fac : P.Factory}
  [HasBool P] [HasBoolOps P] [HasVal P] [HasFvars P] {t : l}
  {b : DetBlock l CmdT P} {cfg : CFG l (DetBlock l CmdT P)}
  {Οƒ : SemanticStore P} {f : Bool} :
  List.lookup t cfg.blocks = some b β†’
    StepCFG P EvalCmd extendFactory fac cfg
      (CFGConfig.atBlock t Οƒ f)
      (CFGConfig.inBlock t b.cmds b.transfer Οƒ f)

Fetch: turn .atBlock t into .inBlock t b.cmds b.transfer.

step_cmd {l CmdT : Type} [BEq l] {P : PureExpr}
  {EvalCmd : EvalCmdParam P CmdT}
  {extendFactory : ExtendFactory P} {fac : P.Factory}
  [HasBool P] [HasBoolOps P] [HasVal P] [HasFvars P]
  {Οƒ : SemanticStore P} {c : CmdT} {Οƒ' : SemanticStore P}
  {f' : Bool} {cfg : CFG l (DetBlock l CmdT P)} {t : l}
  {cs : List CmdT} {tr : DetTransferCmd l P} {f : Bool} :
  EvalCmd fac Οƒ c Οƒ' f' β†’
    StepCFG P EvalCmd extendFactory fac cfg
      (CFGConfig.inBlock t (c :: cs) tr Οƒ f)
      (CFGConfig.inBlock t cs tr Οƒ' (f || f'))

Run one command from the residual list.

goto_true {l CmdT : Type} [BEq l] {P : PureExpr}
  {EvalCmd : EvalCmdParam P CmdT}
  {extendFactory : ExtendFactory P} {fac : P.Factory}
  [HasBool P] [HasBoolOps P] [HasVal P] [HasFvars P]
  {Οƒ : P.Ident β†’ Option P.Expr} {c : P.Expr}
  {cfg : CFG l (DetBlock l CmdT P)} {t tlbl elbl : l}
  {md : MetaData P} {f : Bool} :
  P.eval fac Οƒ c = some HasBool.tt β†’
    WellFormedSemanticEvalBool fac β†’
      WellFormedSemanticEvalExprCongr fac β†’
        StepCFG P EvalCmd extendFactory fac cfg
          (CFGConfig.inBlock t []
            (DetTransferCmd.condGoto c tlbl elbl md) Οƒ f)
          (CFGConfig.atBlock tlbl Οƒ f)

Empty residual + true branch: jump to .atBlock of the true label.

goto_false {l CmdT : Type} [BEq l] {P : PureExpr}
  {EvalCmd : EvalCmdParam P CmdT}
  {extendFactory : ExtendFactory P} {fac : P.Factory}
  [HasBool P] [HasBoolOps P] [HasVal P] [HasFvars P]
  {Οƒ : P.Ident β†’ Option P.Expr} {c : P.Expr}
  {cfg : CFG l (DetBlock l CmdT P)} {t tlbl elbl : l}
  {md : MetaData P} {f : Bool} :
  P.eval fac Οƒ c = some HasBool.ff β†’
    WellFormedSemanticEvalBool fac β†’
      WellFormedSemanticEvalExprCongr fac β†’
        StepCFG P EvalCmd extendFactory fac cfg
          (CFGConfig.inBlock t []
            (DetTransferCmd.condGoto c tlbl elbl md) Οƒ f)
          (CFGConfig.atBlock elbl Οƒ f)

Empty residual + false branch: jump to .atBlock of the false label.

finish {l CmdT : Type} [BEq l] {P : PureExpr}
  {EvalCmd : EvalCmdParam P CmdT}
  {extendFactory : ExtendFactory P} {fac : P.Factory}
  [HasBool P] [HasBoolOps P] [HasVal P] [HasFvars P]
  {cfg : CFG l (DetBlock l CmdT P)} {t : l}
  {md : MetaData P} {Οƒ : SemanticStore P} {f : Bool} :
  StepCFG P EvalCmd extendFactory fac cfg
    (CFGConfig.inBlock t [] (DetTransferCmd.finish md) Οƒ f)
    (CFGConfig.terminal Οƒ f)

Empty residual + finish: halt at .terminal.

πŸ”—def
Imperative.StepCFGStar {l CmdT : Type} [BEq l] (P : PureExpr)
  (EvalCmd : EvalCmdParam P CmdT) (extendFactory : ExtendFactory P)
  (fac : P.Factory) [HasBool P] [HasBoolOps P] [HasVal P] [HasFvars P]
  (cfg : CFG l (DetBlock l CmdT P)) :
  CFGConfig l CmdT P β†’ CFGConfig l CmdT P β†’ Prop
Imperative.StepCFGStar {l CmdT : Type}
  [BEq l] (P : PureExpr)
  (EvalCmd : EvalCmdParam P CmdT)
  (extendFactory : ExtendFactory P)
  (fac : P.Factory) [HasBool P]
  [HasBoolOps P] [HasVal P] [HasFvars P]
  (cfg : CFG l (DetBlock l CmdT P)) :
  CFGConfig l CmdT P β†’
    CFGConfig l CmdT P β†’ Prop

Operational semantics to evaluate an arbitrary number of CFG steps in sequence β€” the reflexive, transitive closure of StepCFG.

2.4.Β Well-Formedness of the PureExpr EvaluatorπŸ”—

As described in "The Strata Core Language Syntax", instantiating Imperative needs to provide the expression language PureExpr. On top of it, the well-formedness conditions of the evaluator PureExpr.eval must be provided (bundled as 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.WellFormedSemanticEvalInt {P : PureExpr} [HasBool P]
  [HasFvars P] [HasInt P] [HasIntOps P] (f : P.Factory) : Prop
Imperative.WellFormedSemanticEvalInt
  {P : PureExpr} [HasBool P] [HasFvars P]
  [HasInt P] [HasIntOps P]
  (f : P.Factory) : Prop

Well-formedness for the integer fragment of a factory-based evaluator.

Constructor

Imperative.WellFormedSemanticEvalInt.mk

Fields

ltReduces : βˆ€ (Οƒ : P.Ident β†’ Option P.Expr) (x y nx ny : P.Expr),
  P.eval f Οƒ x = some nx β†’
    HasInt.isNumeral nx = true β†’
      P.eval f Οƒ y = some ny β†’
        HasInt.isNumeral ny = true β†’
          P.eval f Οƒ (HasIntOps.lt x y) = some HasBool.tt ∨ P.eval f Οƒ (HasIntOps.lt x y) = some HasBool.ff

Comparing two evaluated integer numerals with < reduces to a Boolean value: the result is either tt or ff, never a stuck or non-Boolean expression.

πŸ”—def
Imperative.WellFormedSemanticEvalMono {P : PureExpr} (f : P.Factory) :
  Prop
Imperative.WellFormedSemanticEvalMono
  {P : PureExpr} (f : P.Factory) : Prop

The evaluator is monotone under store extension: if Οƒ' retains every binding of Οƒ, a successful evaluation at Οƒ succeeds identically at Οƒ'. A successful result depends only on the bindings the evaluation reads, so growing the store preserves it.

πŸ”—def
Imperative.WellFormedSemanticEvalRename {P : PureExpr} [HasVal P]
  [HasFvar P] [HasSubstFvar P] (f : P.Factory) : Prop
Imperative.WellFormedSemanticEvalRename
  {P : PureExpr} [HasVal P] [HasFvar P]
  [HasSubstFvar P] (f : P.Factory) : Prop

The evaluator commutes with variable renaming, under definedness of the rename targets. For a variable-only sm whose targets are all defined in the well-formed store Οƒ', evaluating the renamed expression in Οƒ' equals evaluating the original in the pulled-back store. The WellFormedStore Οƒ' guard rules out the non-canonical store bindings under which a step-indexed evaluator could otherwise diverge.

πŸ”—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).

3.Β Formal Semantics of CoreπŸ”—

Strata Core's expressions are Lambda expressions and its statements are Imperative statements, so a Core program is evaluated by the Lambda and Imperative semantics above, instantiated at Core's expression and command types.

3.1.Β Type SystemπŸ”—

Core's well-typedness is specified declaratively, with one judgment per syntactic category. Every judgment is parameterized by the ExprTypingSpec typeclass, so each instantiates to both the polymorphic HasType and the annotated HasTypeA expression relations of the Lambda type system above. The judgments layer up from commands to the whole program.

3.1.1.Β CommandsπŸ”—

Core's commands are the imperative commands plus a procedure call, typed by CmdExtHasType'.

πŸ”—inductive predicate
Core.TypeSpec.CmdExtHasType' {Ο„ : Type} (C : LContext CoreLParams)
  (P : Program) [S : TypeSpec.ExprTypingSpec Ο„] :
  TContext Unit β†’ Command β†’ TContext Unit β†’ Prop
Core.TypeSpec.CmdExtHasType' {Ο„ : Type}
  (C : LContext CoreLParams) (P : Program)
  [S : TypeSpec.ExprTypingSpec Ο„] :
  TContext Unit β†’
    Command β†’ TContext Unit β†’ Prop

Declarative typing for extended commands (imperative commands + procedure calls).

Constructors

cmd {Ο„ : Type} {C : LContext CoreLParams} {P : Program}
  [S : TypeSpec.ExprTypingSpec Ο„] (Ξ“ Ξ“' : TContext Unit)
  (c : Cmd Expression) :
  TypeSpec.CmdHasType' C Ξ“ c Ξ“' β†’
    TypeSpec.CmdExtHasType' C P Ξ“ (CmdExt.cmd c) Ξ“'

A standard imperative command delegates to CmdHasType'.

call {Ο„ : Type} {C : LContext CoreLParams} {P : Program}
  [S : TypeSpec.ExprTypingSpec Ο„] (Ξ“ : TContext Unit)
  (pname : String) (callArgs : List (CallArg Expression))
  (proc : Core.Procedure) (md : MetaData Expression)
  (Οƒ : List (TyIdentifier Γ— LMonoTy))
  (Ξ” : TContext CoreLParams.IDMeta) :
  Program.Procedure.find? P
        (have s := pname;
        { name := s, metadata := () }) =
      some proc β†’
    (CallArg.getInputExprs callArgs).length =
        List.length proc.header.inputs β†’
      (CallArg.getLhs callArgs).length =
          List.length proc.header.outputs β†’
        (βˆ€ (v : Expression.Ident),
            v ∈ CallArg.getLhs callArgs β†’
              (Ξ“.types.find? v).isSome = true) β†’
          (βˆ€ (i : Nat)
              (hi :
                i < (CallArg.getInputExprs callArgs).length)
              (hj :
                i <
                  (ListMap.values
                      proc.header.inputs).length),
              βˆƒ mty,
                AliasEquiv Ξ“.aliases mty
                    (LMonoTy.subst
                      (Strata.Util.HMaps.ofScopes [Οƒ])
                      (ListMap.values
                          proc.header.inputs)[i]) ∧
                  match
                    (CallArg.getInputExprs callArgs)[i] with
                  | LExpr.fvar m x none =>
                    Ξ“.types.find? x =
                      some (LTy.forAll [] mty)
                  | e =>
                    TypeSpec.ExprTypingSpec.exprTyped C Ξ“ e
                      (TypeSpec.ExprTypingSpec.embed mty)) β†’
            (βˆ€ (i : Nat)
                (hi : i < (CallArg.getLhs callArgs).length)
                (hj :
                  i <
                    (ListMap.values
                        proc.header.outputs).length),
                βˆƒ mty,
                  AliasEquiv Ξ“.aliases mty
                      (LMonoTy.subst
                        (Strata.Util.HMaps.ofScopes [Οƒ])
                        (ListMap.values
                            proc.header.outputs)[i]) ∧
                    Ξ“.types.find?
                        (CallArg.getLhs callArgs)[i] =
                      some (LTy.forAll [] mty)) β†’
              (βˆ€ (i : Nat)
                  (hi :
                    i <
                      (ListMap.keys
                          proc.header.inputs).length),
                  (ListMap.keys
                            proc.header.outputs).contains
                        (ListMap.keys
                            proc.header.inputs)[i] =
                      true β†’
                    βˆƒ m ty,
                      (CallArg.getInputExprs callArgs)[i]? =
                        some
                          (LExpr.fvar m
                            (ListMap.keys
                                proc.header.inputs)[i]
                            ty)) β†’
                Ξ”.Equiv Ξ“ β†’
                  TypeSpec.CmdExtHasType' C P Ξ“
                    (CmdExt.call pname callArgs md) Ξ”

A procedure call.

There exists a type instantiation Οƒ (mapping the procedure's type parameters to concrete monotypes) such that:

  • The procedure exists in the program.

  • Arities match (inputs and outputs).

  • All LHS (output) variables exist in the context.

  • Each input expression has the instantiated formal input type.

  • Each LHS variable's context type equals the instantiated formal output type.

  • In-out arguments are simple variable references with matching names.

A call leaves the context unchanged; the output Ξ” is up to TContext.Equiv (see CmdHasType').

3.1.2.Β DatatypesπŸ”—

A mutual datatype block must satisfy MutualADTWF.

πŸ”—structure
Core.TypeSpec.MutualADTWF (C : LContext CoreLParams)
  (block : MutualDatatype Unit) : Prop
Core.TypeSpec.MutualADTWF
  (C : LContext CoreLParams)
  (block : MutualDatatype Unit) : Prop

Declarative well-formedness of a mutual datatype block block in ambient context C.

Inhabitance is required against C.datatypes.push block, the factory extended with the new block, so that mutual and forward references between the block's datatypes resolve.

Constructor

Core.TypeSpec.MutualADTWF.mk

Fields

nonempty : block β‰  []

The block is non-empty.

namesNodup : (List.map (fun x => x.name) block).Nodup

Datatype names in the block are distinct.

namesFresh : βˆ€ (d : LDatatype Unit), d ∈ block β†’ Β¬C.knownTypes.containsName d.name = true

The block's names do not clash with existing known types.

namesNew : βˆ€ (d : LDatatype Unit), d ∈ block β†’ C.datatypes.getType d.name = none

The block's names do not redefine existing datatypes.

argVarsScoped : βˆ€ (d : LDatatype Unit),
  d ∈ block β†’
    βˆ€ (c : LConstr Unit),
      c ∈ d.constrs β†’
        βˆ€ (arg : Identifier Unit Γ— LMonoTy), arg ∈ c.args β†’ βˆ€ (v : TyIdentifier), v ∈ arg.snd.freeVars β†’ v ∈ d.typeArgs

Every free type variable of a constructor argument is one of the enclosing datatype's own typeArgs (constructor arguments introduce no fresh type variables).

argsWF : βˆ€ (d : LDatatype Unit),
  d ∈ block β†’
    βˆ€ (c : LConstr Unit), c ∈ d.constrs β†’ βˆ€ (arg : Identifier Unit Γ— LMonoTy), arg ∈ c.args β†’ ConstrArgWF block arg.snd

Every constructor argument type is not-nested and strictly-positive/uniform.

refsKnown : βˆ€ (d : LDatatype Unit),
  d ∈ block β†’
    βˆ€ (c : LConstr Unit),
      c ∈ d.constrs β†’
        βˆ€ (arg : Identifier Unit Γ— LMonoTy),
          arg ∈ c.args β†’
            βˆ€ (ref : String),
              ref ∈ getTypeRefs arg.snd β†’
                ref ∈ C.knownTypes.keywords ∨ ref ∈ C.datatypes.allTypeNames ∨ ref ∈ List.map (fun x => x.name) block

Every type name referenced in a constructor argument is a known type of C, an existing datatype of C, or a name declared in the block.

argsWellKinded : βˆ€ (d : LDatatype Unit),
  d ∈ block β†’
    βˆ€ (c : LConstr Unit),
      c ∈ d.constrs β†’
        βˆ€ (arg : Identifier Unit Γ— LMonoTy),
          arg ∈ c.args β†’
            βˆ€ (ref : String) (n : Nat),
              (ref, n) ∈ getTypeConsArities arg.snd β†’
                C.knownTypes[ref]? = some n ∨
                  (βˆƒ d', d' ∈ C.datatypes.allDatatypes ∧ d'.name = ref ∧ d'.typeArgs.length = n) ∨
                    βˆƒ d', d' ∈ block ∧ d'.name = ref ∧ d'.typeArgs.length = n

Every type-constructor reference in a constructor argument is applied at the right arity: its argument count equals the referenced type's arity β€” a known type's registered arity, or a datatype's number of typeArgs (an existing datatype of C or one declared in the block).

inhabited : βˆ€ (d : LDatatype Unit), d ∈ block β†’ TySymInhab (Array.push C.datatypes block) d.name

Every datatype in the block is inhabited.

3.1.3.Β FunctionsπŸ”—

Function declarations (recursive or not) are governed by FuncHasType'.

πŸ”—structure
Core.TypeSpec.FuncHasType' (Ο„ : Type) [S : TypeSpec.ExprTypingSpec Ο„]
  (C : LContext CoreLParams) (Ξ“ : TContext Unit) (func : Function) :
  Prop
Core.TypeSpec.FuncHasType' (Ο„ : Type)
  [S : TypeSpec.ExprTypingSpec Ο„]
  (C : LContext CoreLParams)
  (Ξ“ : TContext Unit) (func : Function) :
  Prop

Declarative typing for functions, parameterized over ExprTypingSpec. The Ξ“ is the ambient context the function was type-checked in.

Constructor

Core.TypeSpec.FuncHasType'.mk

Fields

inputsNodup : func.inputs.keys.Nodup

The function's formal parameter names are distinct.

typeArgsNodup : func.typeArgs.Nodup

The function's type argument names are distinct.

noUndeclaredVars : βˆ€ (v : TyIdentifier), v ∈ (func.output.mkArrow' func.inputs.values).freeVars β†’ v ∈ func.typeArgs

All free type variables in the signature are declared in typeArgs.

signatureWellKinded : βˆ€ (ty : LMonoTy),
  ty ∈ func.output :: func.inputs.values β†’
    βˆƒ ty', TypeSpec.ExprTypingSpec.tyCompat Ο„ Ξ“.aliases ty ty' ∧ C.WellKindedTy ty'

Each input and output type is tyCompat to a type well-kinded in C (type constructors applied at their arity).

bodyTyped : βˆ€ (body : LExpr CoreLParams.mono),
  func.body = some body β†’
    TypeSpec.ExprTypingSpec.exprTyped C (TypeSpec.funcContext Ξ“ func) body (TypeSpec.ExprTypingSpec.embed func.output)

If a body exists, it has the declared return type in the ambient context extended with a scope binding each formal to its monomorphic type (up to consistent renaming of type variables).

measureTyped : βˆ€ (m : LExpr CoreLParams.mono),
  func.measure = some m β†’
    (βˆ€ (mid : CoreLParams.mono.base.Metadata) (x : Identifier CoreLParams.mono.base.IDMeta)
        (ann : Option CoreLParams.mono.TypeType), m β‰  LExpr.fvar mid x ann) β†’
      TypeSpec.ExprTypingSpec.exprTyped C (TypeSpec.funcContext Ξ“ func) m (TypeSpec.ExprTypingSpec.embed LMonoTy.int)

If a measure exists and is not a simple variable, it has type int in the same context.

3.1.4.Β ProceduresπŸ”—

Procedure declarations are governed by ProcHasType'; its bodyTyped field defers to ProcBodyHasType', which accepts only structured bodies (CFG bodies carry no typing obligation).

πŸ”—structure
Core.TypeSpec.ProcHasType' (Ο„ : Type) (P : Program)
  [S : TypeSpec.ExprTypingSpec Ο„] (C : LContext CoreLParams)
  (Ξ“ : TContext Unit) (proc : Core.Procedure) : Prop
Core.TypeSpec.ProcHasType' (Ο„ : Type)
  (P : Program)
  [S : TypeSpec.ExprTypingSpec Ο„]
  (C : LContext CoreLParams)
  (Ξ“ : TContext Unit)
  (proc : Core.Procedure) : Prop

Declarative typing for procedures, parameterized over ExprTypingSpec. P is the enclosing program (threaded to the body's StatementsHasType' for funcDecl); C and Ξ“ are the ambient context and type-scope the procedure declaration is checked in.

Constructor

Core.TypeSpec.ProcHasType'.mk

Fields

inputsNodup : (ListMap.keys proc.header.inputs).Nodup

The procedure's input parameter names are distinct.

outputsNodup : (ListMap.keys proc.header.outputs).Nodup

The procedure's output (return) variable names are distinct.

typeArgsNodup : proc.header.typeArgs.Nodup

The procedure's type argument names are distinct.

noUndeclaredVars : βˆ€ (v : TyIdentifier),
  v ∈ LMonoTys.freeVars (ListMap.values proc.header.inputs) ++ LMonoTys.freeVars (ListMap.values proc.header.outputs) β†’
    v ∈ proc.header.typeArgs

Every free type variable in the input/output signature is declared in typeArgs.

signatureWellKinded : βˆ€ (ty : LMonoTy),
  ty ∈ ListMap.values proc.header.inputs ++ ListMap.values proc.header.outputs β†’
    βˆƒ ty', TypeSpec.ExprTypingSpec.tyCompat Ο„ Ξ“.aliases ty ty' ∧ C.WellKindedTy ty'

Each input and output parameter type is tyCompat to a type well-kinded in C (type constructors applied at their arity).

modRights : βˆ€ (v : Expression.Ident),
  v ∈ HasVarsImp.modifiedVars proc.body β†’ v ∈ ListMap.keys proc.header.outputs ++ HasVarsImp.definedVars proc.body false

Every variable the body modifies is an output parameter or is defined in the body (the modification-rights check).

preconditionsTyped : βˆ€ (c : Check Expression),
  c ∈ proc.spec.preconditions.values β†’
    TypeSpec.ExprTypingSpec.exprTyped C (TypeSpec.procInputContext Ξ“ proc) c.expr
      (TypeSpec.ExprTypingSpec.embed LMonoTy.bool)

Each precondition is a bool expression in the input context.

postconditionsTyped : βˆ€ (c : Check Expression),
  c ∈ proc.spec.postconditions.values β†’
    TypeSpec.ExprTypingSpec.exprTyped C (TypeSpec.procBodyContext Ξ“ proc) c.expr
      (TypeSpec.ExprTypingSpec.embed LMonoTy.bool)

Each postcondition is a bool expression in the body context (which includes outputs and old bindings for in-out parameters).

bodyTyped : TypeSpec.ProcBodyHasType' Ο„ P C (TypeSpec.procBodyContext Ξ“ proc) proc.body

The body is well-typed in the body context (see ProcBodyHasType').

3.1.5.Β ProgramsπŸ”—

Program typing is layered: a single declaration (DeclHasType'), the declaration list (DeclsHasType', which threads the context so each declaration is checked against those before it), and the whole program (ProgramHasType').

πŸ”—inductive predicate
Core.TypeSpec.DeclHasType' (Ο„ : Type) (P : Program)
  [S : TypeSpec.ExprTypingSpec Ο„] :
  LContext CoreLParams β†’
    TContext Unit β†’ Decl β†’ LContext CoreLParams β†’ TContext Unit β†’ Prop
Core.TypeSpec.DeclHasType' (Ο„ : Type)
  (P : Program)
  [S : TypeSpec.ExprTypingSpec Ο„] :
  LContext CoreLParams β†’
    TContext Unit β†’
      Decl β†’
        LContext CoreLParams β†’
          TContext Unit β†’ Prop

Declarative typing for a single declaration, parameterized over ExprTypingSpec.

DeclHasType' Ο„ P C Ξ“ decl C' Ξ“' reads: "under program P, in ambient context C and type-scope Ξ“, declaration decl is well-typed and yields output context C' and type-scope Ξ“'." P is threaded to ProcHasType' (so procedure bodies can resolve calls and local funcDecls).

Only type synonyms extend Ξ“ (with a new alias); type constructors/datatypes and function/procedure declarations extend C (with a known type, datatype factory entries, or factory functions).

Constructors

type_con {Ο„ : Type} {P : Program}
  [S : TypeSpec.ExprTypingSpec Ο„]
  (C C' : LContext CoreLParams) (Ξ“ : TContext Unit)
  (tc : TypeConstructor) (md : MetaData Expression) :
  C.addKnownTypeWithError
        { name := tc.name, metadata := tc.numargs }
        default =
      Except.ok C' β†’
    TypeSpec.DeclHasType' Ο„ P C Ξ“
      (Decl.type (TypeDecl.con tc) md) C' Ξ“

A type-constructor declaration: the new type is added to C's known types (must not clash with an existing one); Ξ“ is unchanged.

type_syn {Ο„ : Type} {P : Program}
  [S : TypeSpec.ExprTypingSpec Ο„] (C : LContext CoreLParams)
  (Ξ“ : TContext Unit) (ts : TypeSynonym)
  (md : MetaData Expression) (storedTy : LMonoTy) :
  ts.typeArgs.Nodup β†’
    (βˆ€ (v : TyIdentifier),
        v ∈ ts.type.freeVars β†’ v ∈ ts.typeArgs) β†’
      (βˆ€ (v : TyIdentifier),
          v ∈ ts.typeArgs β†’ v ∈ ts.type.freeVars) β†’
        Β¬C.knownTypes.containsName ts.name = true β†’
          LMonoTy.aliasFree Ξ“.aliases storedTy β†’
            AliasEquiv Ξ“.aliases storedTy ts.type β†’
              TypeSpec.DeclHasType' Ο„ P C Ξ“
                (Decl.type (TypeDecl.syn ts) md) C
                { types := Ξ“.types,
                  aliases :=
                    { name := ts.name,
                        typeArgs := ts.typeArgs,
                        type := storedTy } ::
                      Ξ“.aliases }

A type-synonym declaration: the alias is well-formed (distinct type args, body closed over the args, no phantom args, name not reserved), and Ξ“ gains it. The stored body is fully de-aliased β€” alias-free w.r.t. the existing aliases and alias-equivalent to the written body. C is unchanged.

type_data {Ο„ : Type} {P : Program}
  [S : TypeSpec.ExprTypingSpec Ο„]
  (C C' : LContext CoreLParams) (Ξ“ : TContext Unit)
  (block : MutualDatatype Unit) (md : MetaData Expression) :
  TypeSpec.MutualADTWF C block β†’
    C.addMutualBlock block = Except.ok C' β†’
      TypeSpec.DeclHasType' Ο„ P C Ξ“
        (Decl.type (TypeDecl.data block) md) C' Ξ“

A (mutual) datatype declaration: the block is well-formed (MutualADTWF); the datatypes and their generated functions extend C. Ξ“ is unchanged.

ax {Ο„ : Type} {P : Program} [S : TypeSpec.ExprTypingSpec Ο„]
  (C : LContext CoreLParams) (Ξ“ : TContext Unit) (a : Axiom)
  (md : MetaData Expression) :
  TypeSpec.ExprTypingSpec.exprTyped C Ξ“ a.e
      (TypeSpec.ExprTypingSpec.embed LMonoTy.bool) β†’
    TypeSpec.DeclHasType' Ο„ P C Ξ“ (Decl.ax a md) C Ξ“

An axiom declaration: its expression is a bool in the current context. Contexts are unchanged.

distinct {Ο„ : Type} {P : Program}
  [S : TypeSpec.ExprTypingSpec Ο„] (C : LContext CoreLParams)
  (Ξ“ : TContext Unit) (l : Expression.Ident)
  (es : List Expression.Expr) (md : MetaData Expression) :
  (βˆ€ (e : Expression.Expr),
      e ∈ es β†’
        βˆƒ mty,
          TypeSpec.ExprTypingSpec.exprTyped C Ξ“ e
            (TypeSpec.ExprTypingSpec.embed mty)) β†’
    TypeSpec.DeclHasType' Ο„ P C Ξ“ (Decl.distinct l es md) C
      Ξ“

A distinct declaration: each listed expression is well-typed at some monotype. Contexts are unchanged.

proc {Ο„ : Type} {P : Program}
  [S : TypeSpec.ExprTypingSpec Ο„] (C : LContext CoreLParams)
  (Ξ“ : TContext Unit) (proc : Core.Procedure)
  (md : MetaData Expression) :
  TypeSpec.ProcHasType' Ο„ P C Ξ“ proc β†’
    TypeSpec.DeclHasType' Ο„ P C Ξ“ (Decl.proc proc md) C Ξ“

A procedure declaration: it is well-typed per ProcHasType' (evaluated in the enclosing program P). Contexts are unchanged.

func {Ο„ : Type} {P : Program}
  [S : TypeSpec.ExprTypingSpec Ο„]
  (C C' : LContext CoreLParams) (Ξ“ : TContext Unit)
  (func : Function) (md : MetaData Expression) :
  Β¬func.isRecursive = true β†’
    TypeSpec.FuncHasType' Ο„ C Ξ“ func β†’
      TypeSpec.FactoryExtendedBy C C'
          [LFuncDefined.toLFunc func] β†’
        TypeSpec.DeclHasType' Ο„ P C Ξ“ (Decl.func func md) C'
          Ξ“

A function declaration: non-recursive and well-typed per FuncHasType'; the output C' is C extended with the function (via FactoryExtendedBy). Ξ“ is unchanged.

recFuncBlock {Ο„ : Type} {P : Program}
  [S : TypeSpec.ExprTypingSpec Ο„]
  (C Cstub C' : LContext CoreLParams) (Ξ“ : TContext Unit)
  (funcs : List Function) (md : MetaData Expression)
  (stubs fullFuncs : List (LFunc CoreLParams)) :
  funcs β‰  [] β†’
    (βˆ€ (f : Function),
        f ∈ funcs β†’
          βˆ€ (a : Strata.DL.Util.FuncAttr),
            a ∈ f.attr β†’
              a β‰  Strata.DL.Util.FuncAttr.inline) β†’
      stubs =
          List.map
            (fun f =>
              { name := f.name, typeArgs := f.typeArgs,
                inputs := f.inputs, output := f.output })
            funcs β†’
        fullFuncs =
            List.map (fun x => LFuncDefined.toLFunc x)
              funcs β†’
          TypeSpec.FactoryExtendedBy C Cstub stubs β†’
            TypeSpec.FactoryExtendedBy C C' fullFuncs β†’
              (βˆ€ (f : Function),
                  f ∈ funcs β†’
                    TypeSpec.FuncHasType' Ο„ Cstub Ξ“ f) β†’
                TypeSpec.DeclHasType' Ο„ P C Ξ“
                  (Decl.recFuncBlock funcs md) C' Ξ“

A mutually recursive function block. Two-phase:

  • Cstub is C extended with a signature stub for every block function (so mutual calls resolve during body checking);

  • every block function is well-typed against Cstub;

  • the output C' is C extended with each function's full toLFunc.

The block is non-empty and contains no inline functions; Ξ“ is unchanged.

πŸ”—inductive predicate
Core.TypeSpec.DeclsHasType' (Ο„ : Type) (P : Program)
  [S : TypeSpec.ExprTypingSpec Ο„] :
  LContext CoreLParams β†’
    TContext Unit β†’
      List Decl β†’ LContext CoreLParams β†’ TContext Unit β†’ Prop
Core.TypeSpec.DeclsHasType' (Ο„ : Type)
  (P : Program)
  [S : TypeSpec.ExprTypingSpec Ο„] :
  LContext CoreLParams β†’
    TContext Unit β†’
      List Decl β†’
        LContext CoreLParams β†’
          TContext Unit β†’ Prop

Declarative typing for a list of declarations, threading C and Ξ“ (analogue of StatementsHasType'). P is fixed across the list (it is the enclosing program).

Constructors

nil {Ο„ : Type} {P : Program} [S : TypeSpec.ExprTypingSpec Ο„]
  (C : LContext CoreLParams) (Ξ“ : TContext Unit) :
  TypeSpec.DeclsHasType' Ο„ P C Ξ“ [] C Ξ“

The empty declaration list leaves the context unchanged.

cons {Ο„ : Type} {P : Program}
  [S : TypeSpec.ExprTypingSpec Ο„]
  (C C' C'' : LContext CoreLParams)
  (Ξ“ Ξ“' Ξ“'' : TContext Unit) (d : Decl) (ds : List Decl) :
  TypeSpec.DeclHasType' Ο„ P C Ξ“ d C' Ξ“' β†’
    TypeSpec.DeclsHasType' Ο„ P C' Ξ“' ds C'' Ξ“'' β†’
      TypeSpec.DeclsHasType' Ο„ P C Ξ“ (d :: ds) C'' Ξ“''

The first declaration is typed, then the rest in the updated context.

πŸ”—def
Core.TypeSpec.ProgramHasType' (Ο„ : Type) [S : TypeSpec.ExprTypingSpec Ο„]
  (C : LContext CoreLParams) (Ξ“ : TContext Unit) (P : Program) : Prop
Core.TypeSpec.ProgramHasType' (Ο„ : Type)
  [S : TypeSpec.ExprTypingSpec Ο„]
  (C : LContext CoreLParams)
  (Ξ“ : TContext Unit) (P : Program) : Prop

Declarative typing for a whole program P from ambient context C and type-scope Ξ“: every declared name is globally distinct (P.getNames.Nodup, a single flat namespace across all declaration kinds), and the declarations are well-typed. P is passed as its own enclosing program so procedure bodies can resolve calls.

3.2.Β Procedure CallsπŸ”—

Core extends the Imperative commands with a procedure call. A call is executed by descending into the callee's body (EvalCommand.call_sem).

  1. Evaluate the input and inout argument expressions, and read the current values of caller-side out actuals.

  2. Initialize a fresh callee frame: bind input and inout formals to the evaluated argument values, copy the out values into output-only formals, and snapshot each inout formal as old g.

  3. Assert each non-free precondition unchanged in the initialized callee frame.

  4. Run the callee body in that frame. The old g snapshots continue to hold the values that the inout formals had immediately before the call.

  5. Assert each non-free postcondition unchanged in the final callee frame.

  6. Update the caller's state with the final values of the callee output formals.

Concrete execution of the body of procedure is necessary to make the procedure inlining transform exactly semantics-preserving. A contract version of call semantics is also defined at EvalCommandContract.call_sem. It does not execute the body: after checking preconditions, it havocs all initialized callee output formals, including inouts, and assumes the postconditions. In this semantics, procedure inlining becomes an underapproximating transform because it replaces the values of havoc'ed output variables with concrete values.

3.3.Β ProceduresπŸ”—

A procedure body is verified against its contract by assuming the preconditions on entry and asserting the postconditions on exit. This is a partial correctness reading: a procedure is correct when, if its body terminates, the postconditions hold. Termination is not part of the obligation and is not checked for procedures.

3.4.Β Programs and Declaration OrderπŸ”—

A Core program is a list of declarations, and the order is significant. When the i-th declaration is elaborated it can refer only to the declarations that precede it (the 1st through (iβˆ’1)-th). A declaration therefore cannot mention a name introduced later in the program, unless the referred declaration is in the same rec block.

4.Β Formally Reasoning about Imperative and Strata CoreπŸ”—

4.1.Β The Language Bundle (Strata.Logic.Lang P)πŸ”—

Strata provides formal definitions for reasoning about Imperative and Strata Core. The framework is built on a small, language-agnostic abstraction Strata.Logic.Lang P bundle (P is a parameter for the pure-expression type PureExpr). It packages exactly what a program logic or a transform specification needs from a language:

πŸ”—structure
Strata.Logic.Lang (P : PureExpr) : Type 1
Strata.Logic.Lang (P : PureExpr) : Type 1

Bundles the abstract ingredients for small-step statement semantics, parameterized by a shared pure-expression system P.

Constructor

Strata.Logic.Lang.mk

Fields

StmtT : Type

Statement type.

CfgT : Type

Configuration type.

star : self.CfgT β†’ self.CfgT β†’ Prop

Multi-step relation.

stmtCfg : self.StmtT β†’ Imperative.Env P β†’ self.CfgT

Embed a single statement and env into a config.

terminalCfg : Imperative.Env P β†’ self.CfgT

Terminal configuration.

exitingCfg : String β†’ Imperative.Env P β†’ self.CfgT

Exiting configuration.

isAtAssert : self.CfgT β†’ AssertId P β†’ Prop

Assert detection in configurations.

getEnv : self.CfgT β†’ Imperative.Env P

Extract env from a configuration.

InitEnvWFParamsTy : Type

The type of parameters threaded into initEnvWF. The Core language uses a record bundling reserved "fresh-prefixes" and a declaredFuncs predicate (see Core.Logic.InitEnvWFParams).

initEnvWF : self.InitEnvWFParamsTy β†’ self.StmtT β†’ Imperative.Env P β†’ Prop

Initial environment well-formedness: The language-specific well-formedness parameters are passed via InitEnvWFParamsTy.

The Lang structure itself belongs to no dialect, and the definitions in this chapter quantify over an arbitrary Lang P. For the Imperative dialect there are three instances, in the Imperative.Logic namespace: Lang.imperative (structured statements), Lang.imperativeBlock (block bodies), and Lang.cfg (unstructured control-flow graphs).

4.1.1.Β The Event Language BundleπŸ”—

Event-trace reasoning uses EventLang P EventT. It replaces unlabeled reachability and syntactic assertion-head detection with a trace-producing closure whose event alphabet is explicit in the type.

πŸ”—structure
Strata.Logic.EventLang (P : PureExpr) (EventT : Type) : Type 1
Strata.Logic.EventLang (P : PureExpr)
  (EventT : Type) : Type 1

Language interface for event-trace semantics. It exposes one-step transitions so clients can reason about progress and must-termination; EventLang.traceStar derives chronological traced reachability. Terminal and exiting configurations have no outgoing steps. Unlike Lang, assertion observations are carried by EventT rather than detected from configurations.

Constructor

Strata.Logic.EventLang.mk

Fields

StmtT : Type

Statement type.

CfgT : Type

Configuration type.

step : self.CfgT β†’ List EventT β†’ self.CfgT β†’ Prop

One operational step and the events it emits.

stmtCfg : self.StmtT β†’ Imperative.Env P β†’ self.CfgT

Embed a statement and initial environment into a configuration.

terminalCfg : Imperative.Env P β†’ self.CfgT

Terminal configuration.

exitingCfg : String β†’ Imperative.Env P β†’ self.CfgT

Exiting configuration.

terminal_no_step : βˆ€ (ρ : Imperative.Env P) (emitted : List EventT) (cfg' : self.CfgT), Β¬self.step (self.terminalCfg ρ) emitted cfg'

Terminal configurations have no outgoing operational steps.

exiting_no_step : βˆ€ (label : String) (ρ : Imperative.Env P) (emitted : List EventT) (cfg' : self.CfgT),
  ¬self.step (self.exitingCfg label ρ) emitted cfg'

Exiting configurations have no outgoing operational steps.

getEnv : self.CfgT β†’ Imperative.Env P

Extract an environment from a configuration.

InitEnvWFParamsTy : Type

Parameters threaded into initEnvWF.

initEnvWF : self.InitEnvWFParamsTy β†’ self.StmtT β†’ Imperative.Env P β†’ Prop

Language-specific initial-environment well-formedness.

The structured Imperative constructors package StepStmtE for individual statements and statement lists; EventLang.traceStar derives its traced closure. Their command evaluator determines EventT.

πŸ”—def
Strata.Logic.EventLang.TerminatesAt {P : PureExpr} {EventT : Type}
  (EL : Strata.Logic.EventLang P EventT) (s : EL.StmtT)
  (ρ₀ : Imperative.Env P) (trace : List EventT)
  (ρ' : Imperative.Env P) : Prop
Strata.Logic.EventLang.TerminatesAt
  {P : PureExpr} {EventT : Type}
  (EL : Strata.Logic.EventLang P EventT)
  (s : EL.StmtT) (ρ₀ : Imperative.Env P)
  (trace : List EventT)
  (ρ' : Imperative.Env P) : Prop

s terminates from ρ₀ at ρ' along trace either normally or by exiting with a label. Hoare triples constrain both outcomes because an enclosing block may catch an exiting outcome and continue execution.

πŸ”—def
Strata.Logic.EventLang.Terminates {P : PureExpr} {EventT : Type}
  (EL : Strata.Logic.EventLang P EventT) (s : EL.StmtT)
  (ρ₀ : Imperative.Env P) : Prop
Strata.Logic.EventLang.Terminates
  {P : PureExpr} {EventT : Type}
  (EL : Strata.Logic.EventLang P EventT)
  (s : EL.StmtT) (ρ₀ : Imperative.Env P) :
  Prop

Every execution of s from ρ₀ eventually reaches a terminal or exiting configuration. In particular, no execution gets stuck or diverges. The final environment and emitted trace may differ across nondeterministic executions.

πŸ”—def
Imperative.Logic.EventLang.imperativeE (P : PureExpr) [HasBool P]
  [HasBoolOps P] [HasFvar P] [HasFvars P] [HasInt P] [HasIntOps P]
  [HasSubstFvar P] (CmdT : Type) {EventT : Type}
  (evalCmd : EvalCmdParamE P CmdT EventT)
  (extendFactory : ExtendFactory P) (ParamsTy : Type)
  (initEnvWF : ParamsTy β†’ Stmt P CmdT β†’ Imperative.Env P β†’ Prop) :
  Strata.Logic.EventLang P EventT
Imperative.Logic.EventLang.imperativeE
  (P : PureExpr) [HasBool P]
  [HasBoolOps P] [HasFvar P] [HasFvars P]
  [HasInt P] [HasIntOps P]
  [HasSubstFvar P] (CmdT : Type)
  {EventT : Type}
  (evalCmd : EvalCmdParamE P CmdT EventT)
  (extendFactory : ExtendFactory P)
  (ParamsTy : Type)
  (initEnvWF :
    ParamsTy β†’
      Stmt P CmdT β†’
        Imperative.Env P β†’ Prop) :
  Strata.Logic.EventLang P EventT

Build an event-trace language from Imperative.Stmt/Config with a given command event evaluator. The resulting bundle exposes StepStmtE as its one-step relation.

πŸ”—def
Imperative.Logic.EventLang.imperativeBlockE (P : PureExpr) [HasBool P]
  [HasBoolOps P] [HasFvar P] [HasFvars P] [HasInt P] [HasIntOps P]
  [HasSubstFvar P] (CmdT : Type) {EventT : Type}
  (evalCmd : EvalCmdParamE P CmdT EventT)
  (extendFactory : ExtendFactory P)
  (wfPkg :
    (ParamsTy : Type) Γ—
      (ParamsTy β†’ List (Stmt P CmdT) β†’ Imperative.Env P β†’ Prop)) :
  Strata.Logic.EventLang P EventT
Imperative.Logic.EventLang.imperativeBlockE
  (P : PureExpr) [HasBool P]
  [HasBoolOps P] [HasFvar P] [HasFvars P]
  [HasInt P] [HasIntOps P]
  [HasSubstFvar P] (CmdT : Type)
  {EventT : Type}
  (evalCmd : EvalCmdParamE P CmdT EventT)
  (extendFactory : ExtendFactory P)
  (wfPkg :
    (ParamsTy : Type) Γ—
      (ParamsTy β†’
        List (Stmt P CmdT) β†’
          Imperative.Env P β†’ Prop)) :
  Strata.Logic.EventLang P EventT

Event-trace language for block-level (statement-list) reachability. StmtT is List (Stmt P CmdT) and stmtCfg embeds via .stmts. The EventLang counterpart of Lang.imperativeBlock; wfPkg carries the initial-environment well-formedness with no default (a real language supplies it), so no isAtAssert field is needed.

Strata Core instantiates Lang.imperative as well as Lang.imperativeBlock, and defines Lang.core / Lang.coreBlock. The Core's language bundle uses its own initial-environment well-formedness predicate InitEnvWF and BlockInitEnvWF. Core's logic and analysis judgements are mostly all over Lang.coreBlock because it is more convenient than Lang.core which is about a single statement (but still can have nested sub-statements).

4.2.Β Interpreting Event TracesπŸ”—

Operational semantics records snapshots but does not itself decide whether the captured conditions hold. A ConditionInterp provides a semantic world shared by the conditions in a trace and a predicate for interpreting each captured EventArg in that world.

πŸ”—structure
Imperative.ConditionInterp (P : PureExpr) : Type 1
Imperative.ConditionInterp
  (P : PureExpr) : Type 1

Interprets captured conditions in a semantic world shared by every condition in a trace.

Constructor

Imperative.ConditionInterp.mk

Fields

World : Type

Shared semantic worlds in which captured conditions are interpreted.

holds : self.World β†’ EventArg P β†’ Prop

Whether a captured event condition holds in a semantic world.

The initial implementation delegates condition interpretation to the partial PureExpr.eval evaluator. A denotational interpretation can replace it without changing the operational transition relation or trace representation.

πŸ”—def
Imperative.EvaluatorBasedInterp (P : PureExpr) [HasBool P] :
  ConditionInterp P
Imperative.EvaluatorBasedInterp
  (P : PureExpr) [HasBool P] :
  ConditionInterp P

Interpretation of event conditions using the partial evaluator.

πŸ”—def
Imperative.Event.neutral (P : PureExpr) (I : ConditionInterp P) :
  Event P β†’ Prop
Imperative.Event.neutral (P : PureExpr)
  (I : ConditionInterp P) : Event P β†’ Prop

An event is semantically neutral when its condition holds in every world.

Only assumption events constrain the worlds considered later in a trace.

πŸ”—def
Imperative.Trace.AssumptionsHold (P : PureExpr) (I : ConditionInterp P)
  (world : I.World) (trace : Trace P) : Prop
Imperative.Trace.AssumptionsHold
  (P : PureExpr) (I : ConditionInterp P)
  (world : I.World) (trace : Trace P) :
  Prop

Every assumption in trace holds in world.

A trace is reachable when one shared world satisfies all of its assumptions.

πŸ”—def
Imperative.Trace.Reachable (P : PureExpr) (I : ConditionInterp P)
  (trace : Trace P) : Prop
Imperative.Trace.Reachable (P : PureExpr)
  (I : ConditionInterp P)
  (trace : Trace P) : Prop

Given a trace, the program state after execution of the trace is reachable when its assumptions are jointly satisfiable in one shared semantic world.

Assertion validity is a partial-correctness property. Each assertion occurrence must hold in every world satisfying the assumptions that precede that occurrence; later assumptions cannot discharge an earlier assertion. The per-identifier version restricts this check to matching assertion occurrences.

πŸ”—def
Imperative.Trace.AssertionsValidFromP (P : PureExpr)
  (I : ConditionInterp P) (keep : EventArg P β†’ Prop) :
  Trace P β†’ Trace P β†’ Prop
Imperative.Trace.AssertionsValidFromP
  (P : PureExpr) (I : ConditionInterp P)
  (keep : EventArg P β†’ Prop) :
  Trace P β†’ Trace P β†’ Prop

Worker for assertion validity parameterized by the assertion conditions to keep. The first trace contains assumptions accumulated before the remaining trace.

πŸ”—def
Imperative.Trace.AssertionsValidFrom (P : PureExpr)
  (I : ConditionInterp P) : Trace P β†’ Trace P β†’ Prop
Imperative.Trace.AssertionsValidFrom
  (P : PureExpr) (I : ConditionInterp P) :
  Trace P β†’ Trace P β†’ Prop

Worker for validity of every assertion, with assumptions accumulated before the remaining trace.

πŸ”—def
Imperative.Trace.AssertionsValid (P : PureExpr) (I : ConditionInterp P)
  (trace : Trace P) : Prop
Imperative.Trace.AssertionsValid
  (P : PureExpr) (I : ConditionInterp P)
  (trace : Trace P) : Prop

Every assertion in the trace holds whenever all assumptions preceding that particular assertion hold. Later assumptions cannot discharge an earlier assertion.

πŸ”—def
Imperative.Trace.AssertionValidFrom (P : PureExpr)
  (I : ConditionInterp P) (aid : AssertId P) : Trace P β†’ Trace P β†’ Prop
Imperative.Trace.AssertionValidFrom
  (P : PureExpr) (I : ConditionInterp P)
  (aid : AssertId P) :
  Trace P β†’ Trace P β†’ Prop

Worker for validity of occurrences matching one assertion identifier.

πŸ”—def
Imperative.Trace.AssertionValid (P : PureExpr) (I : ConditionInterp P)
  (aid : AssertId P) (trace : Trace P) : Prop
Imperative.Trace.AssertionValid
  (P : PureExpr) (I : ConditionInterp P)
  (aid : AssertId P) (trace : Trace P) :
  Prop

Validity of all occurrences of one assertion identifier in a trace.

Assertion satisfiability existentially selects one matching occurrence and one world satisfying both its captured condition and all assumptions preceding that occurrence.

πŸ”—def
Imperative.Trace.AssertionSatisfiableFrom (P : PureExpr)
  (I : ConditionInterp P) (aid : AssertId P) : Trace P β†’ Trace P β†’ Prop
Imperative.Trace.AssertionSatisfiableFrom
  (P : PureExpr) (I : ConditionInterp P)
  (aid : AssertId P) :
  Trace P β†’ Trace P β†’ Prop

Worker for satisfiability of one assertion identifier with assumptions accumulated before the remaining trace. It succeeds when some matching assertion occurrence has a world satisfying both its preceding assumptions and captured condition.

πŸ”—def
Imperative.Trace.AssertionSatisfiable (P : PureExpr)
  (I : ConditionInterp P) (aid : AssertId P) (trace : Trace P) : Prop
Imperative.Trace.AssertionSatisfiable
  (P : PureExpr) (I : ConditionInterp P)
  (aid : AssertId P) (trace : Trace P) :
  Prop

An assertion identifier is satisfiable in a trace when at least one matching occurrence and all assumptions preceding it hold in one shared world. The predicate is false when the identifier does not occur in the trace.

Cover satisfiability is existential rather than universal. For one CoverId, a single trace satisfies the property only if it contains a matching cover occurrence whose condition is satisfiable with the assumptions preceding that occurrence. A language-level analysis can account for nondeterministic execution by existentially selecting a reachable trace and then applying this predicate.

πŸ”—def
Imperative.Trace.CoverSatisfiableFrom (P : PureExpr)
  (I : ConditionInterp P) (cid : CoverId P) : Trace P β†’ Trace P β†’ Prop
Imperative.Trace.CoverSatisfiableFrom
  (P : PureExpr) (I : ConditionInterp P)
  (cid : CoverId P) :
  Trace P β†’ Trace P β†’ Prop

Worker for satisfiability of one cover identifier with assumptions accumulated before the remaining trace. It succeeds when some matching cover occurrence has a world satisfying both its preceding assumptions and captured condition.

πŸ”—def
Imperative.Trace.CoverSatisfiable (P : PureExpr) (I : ConditionInterp P)
  (cid : CoverId P) (trace : Trace P) : Prop
Imperative.Trace.CoverSatisfiable
  (P : PureExpr) (I : ConditionInterp P)
  (cid : CoverId P) (trace : Trace P) :
  Prop

A cover identifier is satisfiable in a trace when at least one matching occurrence is satisfiable with all assumptions preceding that occurrence. The predicate is false when the identifier does not occur in the trace.

The metatheory includes monotonicity results for changing accumulated assumptions.

πŸ”—theorem
Imperative.Trace.AssertionValidFrom.mono_assumptions {P : PureExpr}
  (I : ConditionInterp P) (aid : AssertId P)
  {weaker stronger trace : Trace P}
  (himp :
    βˆ€ (world : I.World),
      Trace.AssumptionsHold P I world weaker β†’
        Trace.AssumptionsHold P I world stronger)
  (hvalid : Trace.AssertionValidFrom P I aid stronger trace) :
  Trace.AssertionValidFrom P I aid weaker trace
Imperative.Trace.AssertionValidFrom.mono_assumptions
  {P : PureExpr} (I : ConditionInterp P)
  (aid : AssertId P)
  {weaker stronger trace : Trace P}
  (himp :
    βˆ€ (world : I.World),
      Trace.AssumptionsHold P I world
          weaker β†’
        Trace.AssumptionsHold P I world
          stronger)
  (hvalid :
    Trace.AssertionValidFrom P I aid
      stronger trace) :
  Trace.AssertionValidFrom P I aid weaker
    trace

Per-identifier assertion validity is contravariant in accumulated assumptions.

πŸ”—theorem
Imperative.Trace.CoverSatisfiableFrom.mono_assumptions {P : PureExpr}
  (I : ConditionInterp P) (cid : CoverId P)
  {weaker stronger trace : Trace P}
  (himp :
    βˆ€ (world : I.World),
      Trace.AssumptionsHold P I world stronger β†’
        Trace.AssumptionsHold P I world weaker)
  (hcover : Trace.CoverSatisfiableFrom P I cid stronger trace) :
  Trace.CoverSatisfiableFrom P I cid weaker trace
Imperative.Trace.CoverSatisfiableFrom.mono_assumptions
  {P : PureExpr} (I : ConditionInterp P)
  (cid : CoverId P)
  {weaker stronger trace : Trace P}
  (himp :
    βˆ€ (world : I.World),
      Trace.AssumptionsHold P I world
          stronger β†’
        Trace.AssumptionsHold P I world
          weaker)
  (hcover :
    Trace.CoverSatisfiableFrom P I cid
      stronger trace) :
  Trace.CoverSatisfiableFrom P I cid
    weaker trace

Cover satisfiability is preserved when accumulated assumptions are weakened.

4.3.Β Hoare LogicπŸ”—

A partial-correctness Hoare triple Strata.Logic.Hoare.Triple (Logic/HoareTemplate.lean), states that any run of s from an initial environment satisfying Pre that reaches a terminal or exiting (like break in C/Java) configuration emits an assertion-valid trace under EvaluatorBasedInterp. If that trace is Trace.Reachable, the final environment also satisfies Post.

For Imperative's structured statements, since Imperative doesn't fix command type and wellformedness of the statement, the structural rules (consequence, seq_append, block, ite, while_rule, ...) in Imperative.Logic.Hoare carry its well-formedness side conditions as additional assumptions.

The Hoare rules of Strata Core (Core/Logic/Hoare.lean) instantiates the Imperative template over its block language EventLang.coreBlock with its own wellformedness conditions Core.Logic.BlockInitEnvWF and discharges the side conditions. Also, a Core procedure can be translated into a Hoare triple. Core/Logic/ContractToHoareTriple.lean, Procedure.contractTriple reads a spec { requires ...; ensures ...; } as a triple over the body β€” the requires clauses (including free ones, which the caller guarantees) as precondition, and the checked, non-free ensures clauses as postcondition (free postconditions are assumed at call sites, not proved by the body) β€” so that "this procedure meets its contract" is a single Hoare judgement. StrataTest/Languages/Core/Tests/Logic/Hoare.lean has examples of Hoare triples derived from procedure contracts and their proofs.

4.4.Β Satisfiability and Validity of AssertionsπŸ”—

To reason about assertion commands, Strata has two different notions of properties: validity and satisfiability. An assertion is valid (AssertValid, or AssertValidWhen relative to a precondition) when it holds in every reachable configuration where it is about to execute. AllAssertsValid lifts this to all assertions of a statement. Dually, an assertion is satisfiable (AssertSatisfiable) when some reachable run makes it hold.

The event-trace formulation quantifies directly over traces produced by an EventLang. Assertion validity remains universal over all reachable finite traces. Assertion satisfiability existentially selects a reachable trace and a matching occurrence satisfiable under its preceding assumptions; cover satisfiability follows the same existential trace pattern.

πŸ”—def
Imperative.Specification.AssertValidOnTracesWhen {P : PureExpr}
  (EL : Strata.Logic.EventLang P (Event P)) (I : ConditionInterp P)
  (Pre : Imperative.Env P β†’ Prop) (s : EL.StmtT) (a : AssertId P) : Prop
Imperative.Specification.AssertValidOnTracesWhen
  {P : PureExpr}
  (EL :
    Strata.Logic.EventLang P (Event P))
  (I : ConditionInterp P)
  (Pre : Imperative.Env P β†’ Prop)
  (s : EL.StmtT) (a : AssertId P) : Prop

Every occurrence of assertion a in every reachable finite event trace is valid under the assumptions preceding that occurrence.

πŸ”—def
Imperative.Specification.AllAssertsValidOnTracesWhen {P : PureExpr}
  (EL : Strata.Logic.EventLang P (Event P)) (I : ConditionInterp P)
  (Pre : Imperative.Env P β†’ Prop) (s : EL.StmtT) : Prop
Imperative.Specification.AllAssertsValidOnTracesWhen
  {P : PureExpr}
  (EL :
    Strata.Logic.EventLang P (Event P))
  (I : ConditionInterp P)
  (Pre : Imperative.Env P β†’ Prop)
  (s : EL.StmtT) : Prop

Every assertion event in every reachable finite trace is valid.

πŸ”—def
Imperative.Specification.AssertSatisfiableOnTracesWhen {P : PureExpr}
  (EL : Strata.Logic.EventLang P (Event P)) (I : ConditionInterp P)
  (Pre : Imperative.Env P β†’ Prop) (s : EL.StmtT) (a : AssertId P) : Prop
Imperative.Specification.AssertSatisfiableOnTracesWhen
  {P : PureExpr}
  (EL :
    Strata.Logic.EventLang P (Event P))
  (I : ConditionInterp P)
  (Pre : Imperative.Env P β†’ Prop)
  (s : EL.StmtT) (a : AssertId P) : Prop

Assertion a is satisfiable on traces under Pre when some permitted initial environment produces a finite trace containing a matching assertion occurrence satisfiable with its preceding assumptions.

πŸ”—def
Imperative.Specification.AssertSatisfiableOnTraces {P : PureExpr}
  (EL : Strata.Logic.EventLang P (Event P)) (I : ConditionInterp P)
  (s : EL.StmtT) (a : AssertId P) : Prop
Imperative.Specification.AssertSatisfiableOnTraces
  {P : PureExpr}
  (EL :
    Strata.Logic.EventLang P (Event P))
  (I : ConditionInterp P) (s : EL.StmtT)
  (a : AssertId P) : Prop

Trace-native assertion satisfiability with no initial-state restriction.

The event Hoare triple validates every completed trace and gates its postcondition on joint satisfiability of that trace's assumptions. Trace validity above quantifies over every finite prefix, so the two notions are separate unless an additional progress or trace-extension result relates them.

4.4.1.Β Soundness and Completeness of AnalysisπŸ”—

To formally describe analyses that answer validity and satisfiability, an abstract notion of analysis is defined over an arbitrary Lang:

πŸ”—structure
Imperative.Specification.Analysis (β„™ D : Type) : Type
Imperative.Specification.Analysis
  (β„™ D : Type) : Type

An Analysis over programs β„™ producing diagnostics D. β„™ is written double-struck (\bbP) to avoid clashing with the pure-expression parameter P used elsewhere in this file.

Constructor

Imperative.Specification.Analysis.mk

Fields

desirableProperty : β„™ β†’ Prop

The property we want every program to satisfy.

analyze : β„™ β†’ D

The analysis function: produce a diagnostic from a program.

pass : D β†’ Prop

Whether a diagnostic is considered passing.

πŸ”—def
Imperative.Specification.Analysis.Sound {β„™ D : Type}
  (a : Specification.Analysis β„™ D) : Prop
Imperative.Specification.Analysis.Sound
  {β„™ D : Type}
  (a : Specification.Analysis β„™ D) : Prop

An analysis is sound when a passing diagnostic implies the desirable property holds of the analyzed program.

πŸ”—def
Imperative.Specification.Analysis.Complete {β„™ D : Type}
  (a : Specification.Analysis β„™ D) : Prop
Imperative.Specification.Analysis.Complete
  {β„™ D : Type}
  (a : Specification.Analysis β„™ D) : Prop

An analysis is complete when every program with the desirable property yields a passing diagnostic.

The connection of the definition of analysis to Core's verifier is packaged as CoreVerifierModel:

πŸ”—def
Core.Specification.Analysis.CoreVerifierModel
  (Ο† : Expression.Factory β†’ PureFunc Expression β†’ Expression.Factory)
  (mode : VerificationMode)
  (analyze :
    VerificationMode β†’
      Specification.Analysis.CoreVerifierInput β†’ Core.VCResults) :
  Specification.Analysis Specification.Analysis.CoreVerifierInput
    Core.VCResults
Core.Specification.Analysis.CoreVerifierModel
  (Ο† :
    Expression.Factory β†’
      PureFunc Expression β†’
        Expression.Factory)
  (mode : VerificationMode)
  (analyze :
    VerificationMode β†’
      Specification.Analysis.CoreVerifierInput β†’
        Core.VCResults) :
  Specification.Analysis
    Specification.Analysis.CoreVerifierInput
    Core.VCResults

An analysis whose desirable property under each VerificationMode is:

  • .deductive β€” ProcedureAssertsValid (universal: every assert valid and every terminating run satisfies the postconditions);

  • .bugFinding β€” ProcedureAssertsSatisfiable (existential dual: some run reaches each assert and some terminating run satisfies the postconditions);

  • .bugFindingAssumingCompleteSpec β€” False (not yet specified).

The diagnostic is a VCResults array; the analyze function additionally receives the VerificationMode so it can shape the obligations it produces, and pass reports success on every VCResult under the given mode.

Its desirable property is selected by the VerificationMode β€” deductive mode requires every entry procedure's assertions to be valid, and bug-finding mode requires them to be satisfiable.

Fully proving the soundness of Core's verifier is an ongoing work.

4.5.Β Correctness of Program TransformationπŸ”—

Transformations must not change what the verifier concludes. The definitions in Strata/Transform/Specification.lean can relate different source and target languages.

The analysis-specific Sound predicate relates two EventLang values under one condition interpretation. It states that validity of each target assertion on reachable traces implies the corresponding source validity, so a verified output certifies the input.

The operational definitions are more general across analyses and support horizontal and vertical composition. They are the primary specifications for program transformations.

  • The Overapproximates family states this operationally. Plain Overapproximates requires that every terminal or exiting state reachable in the source is reachable in the target, and that any source assertion failure is reproduced in the target. The variants generalize it: OverapproximatesWhen adds a precondition; OverapproximatesUpto(When) relates source and target states up to input/output relations (needed when a transform renames or generates variables); and the ...Aggressively... variants permit the target to fail spuriously (needed when a transform prunes paths).

  • Underapproximates is the dual β€” every terminal/exiting state reachable in the target is reachable in the source, and target failures are reflected back β€” which is what bug-finding soundness needs.

  • SemanticallyEquivalent is their conjunction: source and target reach exactly the same terminal/exiting states and fail on exactly the same initial states.

For EventLang, the OverapproximatesTraces family additionally relates the chronological event lists produced by source and target executions. The most general member carries separate input/output environment relations and simulates all finite prefixes as well as terminal and exiting runs.

πŸ”—def
Imperative.Specification.Transform.OverapproximatesTracesUptoWhen
  {P : PureExpr} {EventT : Type} (Rtrace : Relation (List EventT))
  (Rin Rout : Relation (Imperative.Env P))
  (L₁ Lβ‚‚ : Strata.Logic.EventLang P EventT)
  (T : L₁.StmtT β†’ Option Lβ‚‚.StmtT) (pre : L₁.StmtT β†’ Prop)
  (params₁ : L₁.InitEnvWFParamsTy) (paramsβ‚‚ : Lβ‚‚.InitEnvWFParamsTy) :
  Prop
Imperative.Specification.Transform.OverapproximatesTracesUptoWhen
  {P : PureExpr} {EventT : Type}
  (Rtrace : Relation (List EventT))
  (Rin Rout : Relation (Imperative.Env P))
  (L₁ Lβ‚‚ :
    Strata.Logic.EventLang P EventT)
  (T : L₁.StmtT β†’ Option Lβ‚‚.StmtT)
  (pre : L₁.StmtT β†’ Prop)
  (params₁ : L₁.InitEnvWFParamsTy)
  (paramsβ‚‚ : Lβ‚‚.InitEnvWFParamsTy) : Prop

Trace-based overapproximation up to explicit trace and state relations. It simulates every finite prefix (for safety properties) and terminal/exiting runs (for partial-correctness postconditions). The definition is independent of any particular trace property or condition interpretation.

πŸ”—def
Imperative.Specification.Transform.OverapproximatesTracesWhen
  {P : PureExpr} {EventT : Type} (Rtrace : Relation (List EventT))
  (L₁ Lβ‚‚ : Strata.Logic.EventLang P EventT)
  (T : L₁.StmtT β†’ Option Lβ‚‚.StmtT) (pre : L₁.StmtT β†’ Prop)
  (params₁ : L₁.InitEnvWFParamsTy) (paramsβ‚‚ : Lβ‚‚.InitEnvWFParamsTy) :
  Prop
Imperative.Specification.Transform.OverapproximatesTracesWhen
  {P : PureExpr} {EventT : Type}
  (Rtrace : Relation (List EventT))
  (L₁ Lβ‚‚ :
    Strata.Logic.EventLang P EventT)
  (T : L₁.StmtT β†’ Option Lβ‚‚.StmtT)
  (pre : L₁.StmtT β†’ Prop)
  (params₁ : L₁.InitEnvWFParamsTy)
  (paramsβ‚‚ : Lβ‚‚.InitEnvWFParamsTy) : Prop

Equality-state trace overapproximation under a statement precondition.

πŸ”—def
Imperative.Specification.Transform.OverapproximatesTraces {P : PureExpr}
  {EventT : Type} (Rtrace : Relation (List EventT))
  (L₁ Lβ‚‚ : Strata.Logic.EventLang P EventT)
  (T : L₁.StmtT β†’ Option Lβ‚‚.StmtT) (params₁ : L₁.InitEnvWFParamsTy)
  (paramsβ‚‚ : Lβ‚‚.InitEnvWFParamsTy) : Prop
Imperative.Specification.Transform.OverapproximatesTraces
  {P : PureExpr} {EventT : Type}
  (Rtrace : Relation (List EventT))
  (L₁ Lβ‚‚ :
    Strata.Logic.EventLang P EventT)
  (T : L₁.StmtT β†’ Option Lβ‚‚.StmtT)
  (params₁ : L₁.InitEnvWFParamsTy)
  (paramsβ‚‚ : Lβ‚‚.InitEnvWFParamsTy) : Prop

Trace overapproximation with equality states and no statement restriction.

Trace overapproximation connects back to the event logic through overapproximatesTraces_triple (in SpecHoareConnection.lean): with equality as the trace relation, if a Hoare triple holds on the target T(st), the same triple holds on the source st. The terminal or exiting simulation supplies the identical event trace and final environment required by the target triple.

Strata proves that sequentially chaining multiple transformations is correct through (vertical composition), overapproximates_comp which turns overapproximations L₁ β†’ Lβ‚‚ and Lβ‚‚ β†’ L₃ into one L₁ β†’ L₃. overapproximatesUpto_comp does the same for the up-to-relation form, composing the two state relations with relation composition (RComp); and overapproximatesAggressively_comp composes the assertion-failure-relaxed variant.

Trace overapproximations compose their trace relations explicitly. The general composition theorem produces relational composition, while the shared-start up-to theorem accepts stage-specific trace relations and a transitive output state relation.

πŸ”—theorem
Imperative.Specification.Transform.OverapproximatesTraces.rel_comp
  {P : PureExpr} {EventT : Type} (R₁ Rβ‚‚ : Relation (List EventT))
  (L₁ Lβ‚‚ L₃ : Strata.Logic.EventLang P EventT)
  (T₁ : L₁.StmtT β†’ Option Lβ‚‚.StmtT) (Tβ‚‚ : Lβ‚‚.StmtT β†’ Option L₃.StmtT)
  (params₁ : L₁.InitEnvWFParamsTy) (paramsβ‚‚ : Lβ‚‚.InitEnvWFParamsTy)
  (params₃ : L₃.InitEnvWFParamsTy)
  (h₁ :
    Specification.Transform.OverapproximatesTraces R₁ L₁ Lβ‚‚ T₁ params₁
      paramsβ‚‚)
  (hβ‚‚ :
    Specification.Transform.OverapproximatesTraces Rβ‚‚ Lβ‚‚ L₃ Tβ‚‚ paramsβ‚‚
      params₃) :
  Specification.Transform.OverapproximatesTraces (RComp R₁ Rβ‚‚) L₁ L₃
    (fun s => T₁ s >>= Tβ‚‚) params₁ params₃
Imperative.Specification.Transform.OverapproximatesTraces.rel_comp
  {P : PureExpr} {EventT : Type}
  (R₁ Rβ‚‚ : Relation (List EventT))
  (L₁ Lβ‚‚ L₃ :
    Strata.Logic.EventLang P EventT)
  (T₁ : L₁.StmtT β†’ Option Lβ‚‚.StmtT)
  (Tβ‚‚ : Lβ‚‚.StmtT β†’ Option L₃.StmtT)
  (params₁ : L₁.InitEnvWFParamsTy)
  (paramsβ‚‚ : Lβ‚‚.InitEnvWFParamsTy)
  (params₃ : L₃.InitEnvWFParamsTy)
  (h₁ :
    Specification.Transform.OverapproximatesTraces
      R₁ L₁ Lβ‚‚ T₁ params₁ paramsβ‚‚)
  (hβ‚‚ :
    Specification.Transform.OverapproximatesTraces
      Rβ‚‚ Lβ‚‚ L₃ Tβ‚‚ paramsβ‚‚ params₃) :
  Specification.Transform.OverapproximatesTraces
    (RComp R₁ Rβ‚‚) L₁ L₃
    (fun s => T₁ s >>= Tβ‚‚) params₁ params₃

Explicit trace-relation overapproximations compose by relational composition of their trace relations.

πŸ”—theorem
Imperative.Specification.Transform.OverapproximatesTracesUptoWhen.comp_trans_eq
  {P : PureExpr} {EventT : Type}
  (Rtrace₁ Rtraceβ‚‚ : Relation (List EventT))
  (Rout : Relation (Imperative.Env P)) (houtTrans : IsTransitive Rout)
  (L₁ Lβ‚‚ L₃ : Strata.Logic.EventLang P EventT)
  (T₁ : L₁.StmtT β†’ Option Lβ‚‚.StmtT) (Tβ‚‚ : Lβ‚‚.StmtT β†’ Option L₃.StmtT)
  {pre₁ : L₁.StmtT β†’ Prop} {preβ‚‚ : Lβ‚‚.StmtT β†’ Prop}
  (params₁ : L₁.InitEnvWFParamsTy) (paramsβ‚‚ : Lβ‚‚.InitEnvWFParamsTy)
  (params₃ : L₃.InitEnvWFParamsTy)
  (hpre :
    βˆ€ (st : L₁.StmtT) (st' : Lβ‚‚.StmtT),
      T₁ st = some st' β†’ pre₁ st β†’ preβ‚‚ st')
  (h₁ :
    Specification.Transform.OverapproximatesTracesUptoWhen Rtrace₁
      (fun x1 x2 => x1 = x2) Rout L₁ Lβ‚‚ T₁ pre₁ params₁ paramsβ‚‚)
  (hβ‚‚ :
    Specification.Transform.OverapproximatesTracesUptoWhen Rtraceβ‚‚
      (fun x1 x2 => x1 = x2) Rout Lβ‚‚ L₃ Tβ‚‚ preβ‚‚ paramsβ‚‚ params₃) :
  Specification.Transform.OverapproximatesTracesUptoWhen
    (RComp Rtrace₁ Rtraceβ‚‚) (fun x1 x2 => x1 = x2) Rout L₁ L₃
    (fun s => T₁ s >>= Tβ‚‚) pre₁ params₁ params₃
Imperative.Specification.Transform.OverapproximatesTracesUptoWhen.comp_trans_eq
  {P : PureExpr} {EventT : Type}
  (Rtrace₁ Rtraceβ‚‚ :
    Relation (List EventT))
  (Rout : Relation (Imperative.Env P))
  (houtTrans : IsTransitive Rout)
  (L₁ Lβ‚‚ L₃ :
    Strata.Logic.EventLang P EventT)
  (T₁ : L₁.StmtT β†’ Option Lβ‚‚.StmtT)
  (Tβ‚‚ : Lβ‚‚.StmtT β†’ Option L₃.StmtT)
  {pre₁ : L₁.StmtT β†’ Prop}
  {preβ‚‚ : Lβ‚‚.StmtT β†’ Prop}
  (params₁ : L₁.InitEnvWFParamsTy)
  (paramsβ‚‚ : Lβ‚‚.InitEnvWFParamsTy)
  (params₃ : L₃.InitEnvWFParamsTy)
  (hpre :
    βˆ€ (st : L₁.StmtT) (st' : Lβ‚‚.StmtT),
      T₁ st = some st' β†’
        pre₁ st β†’ preβ‚‚ st')
  (h₁ :
    Specification.Transform.OverapproximatesTracesUptoWhen
      Rtrace₁ (fun x1 x2 => x1 = x2) Rout
      L₁ Lβ‚‚ T₁ pre₁ params₁ paramsβ‚‚)
  (hβ‚‚ :
    Specification.Transform.OverapproximatesTracesUptoWhen
      Rtraceβ‚‚ (fun x1 x2 => x1 = x2) Rout
      Lβ‚‚ L₃ Tβ‚‚ preβ‚‚ paramsβ‚‚ params₃) :
  Specification.Transform.OverapproximatesTracesUptoWhen
    (RComp Rtrace₁ Rtraceβ‚‚)
    (fun x1 x2 => x1 = x2) Rout L₁ L₃
    (fun s => T₁ s >>= Tβ‚‚) pre₁ params₁
    params₃

Shared-start composition for trace overapproximations with potentially different trace relations and a transitive outcome relation.

Composition across a statement list (horizontal composition): overapproximates_stmts and overapproximatesUpto_stmts lift a per-statement overapproximation to the whole block (fun ss => ss.mapM T). Like the Hoare rules above, these carry well-formedness side conditions: the lift needs an environment invariant that holds at block entry, is preserved as each statement runs, and implies the per-statement source well-formedness. When no such statement-independent invariant exists, the block-level result has to be proved directly instead.

The trace-aware counterpart, overapproximatesTraces_stmts, additionally requires the trace relation to relate empty traces and respect chronological append. It simulates arbitrary finite prefixes as well as terminal and exiting runs.

πŸ”—theorem
Imperative.Specification.Transform.overapproximatesTraces_stmts
  {P : PureExpr} [HasFvar P] [HasFvars P] [HasBool P] [HasBoolOps P]
  [HasSubstFvar P] [HasInt P] [HasIntOps P] {CmdT EventT : Type}
  (evalCmdE : EvalCmdParamE P CmdT EventT)
  (extendFactory : ExtendFactory P) (Rtrace : Relation (List EventT))
  (hnil : Rtrace [] [])
  (happend :
    βˆ€ (a a' b b' : List EventT),
      Rtrace a a' β†’ Rtrace b b' β†’ Rtrace (a ++ b) (a' ++ b'))
  {Params : Type}
  (wf : Params β†’ List (Stmt P CmdT) β†’ Imperative.Env P β†’ Prop)
  (p₁ pβ‚‚ : Params) {SParams : Type}
  (swf : SParams β†’ Stmt P CmdT β†’ Imperative.Env P β†’ Prop)
  (sp₁ spβ‚‚ : SParams) (T : Stmt P CmdT β†’ Option (Stmt P CmdT))
  (Inv : Imperative.Env P β†’ Prop)
  (hGround :
    βˆ€ (ss : List (Stmt P CmdT)) (ρ : Imperative.Env P),
      wf p₁ ss ρ β†’ Inv ρ)
  (hPres :
    βˆ€ {s : Stmt P CmdT} {ρ ρ' : Imperative.Env P} {tr : List EventT},
      Inv ρ β†’
        StepStmtStarE P evalCmdE extendFactory (Config.stmt s ρ) tr
            (Config.terminal ρ') β†’
          Inv ρ')
  (hGate :
    βˆ€ {s : Stmt P CmdT} {ρ : Imperative.Env P}, Inv ρ β†’ swf sp₁ s ρ)
  (hWF :
    βˆ€ (ss ss' : List (Stmt P CmdT)) (ρ : Imperative.Env P),
      List.mapM T ss = some ss' β†’ wf p₁ ss ρ β†’ wf pβ‚‚ ss' ρ)
  (hsem :
    Specification.Transform.OverapproximatesTraces Rtrace
      (Logic.EventLang.imperativeE P CmdT evalCmdE extendFactory SParams
        swf)
      (Logic.EventLang.imperativeE P CmdT evalCmdE extendFactory SParams
        swf)
      T sp₁ spβ‚‚) :
  Specification.Transform.OverapproximatesTraces Rtrace
    (Logic.EventLang.imperativeBlockE P CmdT evalCmdE extendFactory
      ⟨Params, wf⟩)
    (Logic.EventLang.imperativeBlockE P CmdT evalCmdE extendFactory
      ⟨Params, wf⟩)
    (fun ss => List.mapM T ss) p₁ pβ‚‚
Imperative.Specification.Transform.overapproximatesTraces_stmts
  {P : PureExpr} [HasFvar P] [HasFvars P]
  [HasBool P] [HasBoolOps P]
  [HasSubstFvar P] [HasInt P]
  [HasIntOps P] {CmdT EventT : Type}
  (evalCmdE : EvalCmdParamE P CmdT EventT)
  (extendFactory : ExtendFactory P)
  (Rtrace : Relation (List EventT))
  (hnil : Rtrace [] [])
  (happend :
    βˆ€ (a a' b b' : List EventT),
      Rtrace a a' β†’
        Rtrace b b' β†’
          Rtrace (a ++ b) (a' ++ b'))
  {Params : Type}
  (wf :
    Params β†’
      List (Stmt P CmdT) β†’
        Imperative.Env P β†’ Prop)
  (p₁ pβ‚‚ : Params) {SParams : Type}
  (swf :
    SParams β†’
      Stmt P CmdT β†’
        Imperative.Env P β†’ Prop)
  (sp₁ spβ‚‚ : SParams)
  (T : Stmt P CmdT β†’ Option (Stmt P CmdT))
  (Inv : Imperative.Env P β†’ Prop)
  (hGround :
    βˆ€ (ss : List (Stmt P CmdT))
      (ρ : Imperative.Env P),
      wf p₁ ss ρ β†’ Inv ρ)
  (hPres :
    βˆ€ {s : Stmt P CmdT}
      {ρ ρ' : Imperative.Env P}
      {tr : List EventT},
      Inv ρ β†’
        StepStmtStarE P evalCmdE
            extendFactory
            (Config.stmt s ρ) tr
            (Config.terminal ρ') β†’
          Inv ρ')
  (hGate :
    βˆ€ {s : Stmt P CmdT}
      {ρ : Imperative.Env P},
      Inv ρ β†’ swf sp₁ s ρ)
  (hWF :
    βˆ€ (ss ss' : List (Stmt P CmdT))
      (ρ : Imperative.Env P),
      List.mapM T ss = some ss' β†’
        wf p₁ ss ρ β†’ wf pβ‚‚ ss' ρ)
  (hsem :
    Specification.Transform.OverapproximatesTraces
      Rtrace
      (Logic.EventLang.imperativeE P CmdT
        evalCmdE extendFactory SParams
        swf)
      (Logic.EventLang.imperativeE P CmdT
        evalCmdE extendFactory SParams
        swf)
      T sp₁ spβ‚‚) :
  Specification.Transform.OverapproximatesTraces
    Rtrace
    (Logic.EventLang.imperativeBlockE P
      CmdT evalCmdE extendFactory
      ⟨Params, wf⟩)
    (Logic.EventLang.imperativeBlockE P
      CmdT evalCmdE extendFactory
      ⟨Params, wf⟩)
    (fun ss => List.mapM T ss) p₁ pβ‚‚

Event-trace analogue of overapproximates_stmts: lift a per-statement trace overapproximation to whole statement lists. It simulates every finite source prefix and every terminal/exiting run. As with overapproximates_stmts, the lift is mediated by an environment invariant Inv established at block entry (hGround), preserved across each statement's terminal run (hPres), and implying the per-statement source gate (hGate). Rtrace need only satisfy the empty-trace law hnil and the append-compatibility law happend.