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

Lambda.Step.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)
      (LExpr.replaceMetadata1 m e)

A free variable. Stuck if rf does not assign an expression to x.

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

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

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

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

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

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

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

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

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

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

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

Lambda.Step.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 value.

Lambda.Step.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.applyTypeSubst
                  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.

Lambda.Step.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 : ConcreteEval Tbase) :
  F.callOfLFunc e = some (callee, args, fn) β†’
    fn.concreteEval = some denotefn β†’
      some e' = denotefn m callee.opTy? 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.

Lambda.Step.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 value_not_step: isValue returns true for an abs only when it is closed (freeVars e = []), so an abstraction that is a value has no free variables for this rule to fire on.

Lambda.Step.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, except for value_not_step, which does not concern quantifiers: a quantifier is never a value.

Lambda.Step.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, except for value_not_step, which does not concern quantifiers: a quantifier is never a value.

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 isValue returns true for LExpr that is a value: constants, closed abstractions, constructor applications of values, etc. A quantifier is never a value.

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

Values of LExprs.

If e:LExpr is .app, say e1 e2 .. en, e is a value if (1) e1 is a constructor and e2 .. en are all 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.

A constant is a value, and so is a closed abstraction. A quantifier is never a value, closed or not: evaluation does not decide it, and a closed quantifier of type bool taken as a value would be a value of type bool that is neither true nor false (LExpr.isValue_bool_eq_boolConst: on a factory with no constructor producing a Boolean, every value that typeCheckWith types bool is a Boolean constant).

The theorem value_not_step confirms the intended relationship between the two notions: no reduction rule of Step fires on a value. The converse fails: some normal forms are not values, e.g. closed quantifiers.

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

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

A named type constructor applied to sort arguments.

Lambda.LSort.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, a Map k v to the functions from k to v and a Sequence a to the lists of a; all others are delegated to tcInterp.

Map and Sequence are built in because they have literals (LConst.mapConst, LConst.sequenceConst), which must denote values whatever tcInterp is. Maps are total and extensional, and sequences finite, as in the SMT-LIB theories of arrays and sequences. So Map with two arguments and Sequence with one are reserved type-constructor names for every Lambda language: a client type constructor registered under one of them has the built-in meaning, whatever tcInterp says.

The real sort denotes Strata.Util.Real, the real numbers, a complete ordered field. A rational literal r denotes Real.ofRat r.

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.{u_1} (P : PureExpr) : Type u_1
Imperative.Env.{u_1} (P : PureExpr) :
  Type u_1

Execution environment: store and expression factory.

Constructor

Imperative.Env.mk.{u_1}

Fields

store : SemanticStore P

The current variable store.

factory : P.Factory

The read-only expression factory used to evaluate expressions. Commands, guards, and events read it from the active configuration as ρ.factory; every statement step preserves it, and leaving a block projects only the store.

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.{u_1} (P : PureExpr) :
  SemanticStore P β†’ P.Ident β†’ P.Val β†’ SemanticStore P β†’ Prop
Imperative.InitState.{u_1}
  (P : PureExpr) :
  SemanticStore P β†’
    P.Ident β†’
      P.Val β†’ SemanticStore P β†’ Prop

Abtract variable initialization.

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

Constructors

Imperative.InitState.init.{u_1} {P : PureExpr}
  {Οƒ Οƒ' : SemanticStore P} {x : P.Ident} {v : P.Val} :
  Οƒ 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.{u_1} (P : PureExpr) :
  SemanticStore P β†’ P.Ident β†’ P.Val β†’ SemanticStore P β†’ Prop
Imperative.UpdateState.{u_1}
  (P : PureExpr) :
  SemanticStore P β†’
    P.Ident β†’
      P.Val β†’ SemanticStore P β†’ Prop

Abstract variable update.

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

Constructors

Imperative.UpdateState.update.{u_1} {P : PureExpr}
  {Οƒ Οƒ' : SemanticStore P} {x : P.Ident} {v v' : P.Val} :
  Οƒ 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 by the EvalCmdE relation, which updates the store and 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.{u_1} (P : PureExpr) : Type u_1
Imperative.EventArg.{u_1} (P : PureExpr) :
  Type u_1

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.{u_1}

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.{u_1} (P : PureExpr) : Type u_1
Imperative.Event.{u_1} (P : PureExpr) :
  Type u_1

Observable events emitted by Imperative commands.

Constructors

Imperative.Event.assert.{u_1} {P : PureExpr} :
  EventArg P β†’ Event P

An assertion condition that must hold under preceding assumptions.

Imperative.Event.assume.{u_1} {P : PureExpr} :
  EventArg P β†’ Event P

An assumption condition that constrains later observations.

Imperative.Event.cover.{u_1} {P : PureExpr} :
  EventArg P β†’ Event P

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

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

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.{u_1, u_2} (P : PureExpr) (Cmd : Type)
  (EventT : Type u_2) : Type (max u_1 u_2)
Imperative.EvalCmdParamE.{u_1, u_2}
  (P : PureExpr) (Cmd : Type)
  (EventT : Type u_2) : Type (max u_1 u_2)

Command evaluation relation that reports an ordered event trace. Commands do not modify the evaluator. 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.{u_1} (P : PureExpr) :
  Cmd P β†’ P.Factory β†’ SemanticStore P β†’ Trace P
Imperative.Cmd.emittedEvents.{u_1}
  (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.{u_1} (P : PureExpr) [HasFvar P] [HasBool P] :
  P.Factory β†’ SemanticStore P β†’ Cmd P β†’ SemanticStore P β†’ Trace P β†’ Prop
Imperative.EvalCmdE.{u_1} (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.

This relation covers the monomorphic runtime semantics: every type carried by an .init, and every type witnessed for a .set, is assumed to have already been monomorphized by type checking. Polymorphic instantiation is outside EvalCmdE.

Constructors

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

Evaluate a deterministic initializer, update the store, and emit no observation. The typed-value premise mirrors nondeterministic init, which makes deterministic-to-nondeterministic refinement direct.

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

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

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

Evaluate a deterministic assignment and emit no observation. The stored-type premise mirrors nondeterministic set for refinement proofs.

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

Assign an arbitrary value and emit no observation.

Imperative.EvalCmdE.eval_assert.{u_1} {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.

Imperative.EvalCmdE.eval_assume.{u_1} {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.

Imperative.EvalCmdE.eval_cover.{u_1} {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 relation agrees with that deterministic trace.

πŸ”—theorem
Imperative.EvalCmdE.emitted_eq.{u_1} {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.{u_1}
  {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.

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.{u} (P : PureExpr) (CmdT : Type) : Type u
Imperative.Config.{u} (P : PureExpr)
  (CmdT : Type) : Type u

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 and evaluator

Constructors

Imperative.Config.stmt.{u} {P : PureExpr} {CmdT : Type} :
  Stmt P CmdT β†’ Imperative.Env P β†’ Imperative.Config P CmdT

A single statement to execute next.

Imperative.Config.stmts.{u} {P : PureExpr} {CmdT : Type} :
  List (Stmt P CmdT) β†’
    Imperative.Env P β†’ Imperative.Config P CmdT

A list of statements to execute next, in order.

Imperative.Config.terminal.{u} {P : PureExpr}
  {CmdT : Type} :
  Imperative.Env P β†’ Imperative.Config P CmdT

A terminal configuration, indicating that execution has finished.

Imperative.Config.exiting.{u} {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.

Imperative.Config.block.{u} {P : PureExpr} {CmdT : Type} :
  Option String β†’
    SemanticStore P β†’
      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.

Imperative.Config.seq.{u} {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 StepStmtE relation describes how each type of statement transforms configurations, labeling each transition with the events emitted by its active command. It is parameterized by a command evaluator (because statements are parameteric to the list of defined commands). Administrative control-flow transitions emit the empty event list, and sequence and block frames propagate the active inner step's events unchanged. The expression factory is immutable during execution: it is carried in the environment to evaluate expressions, and no statement step mutates it.

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

Event-labeled single statement step. The expression evaluator is P.eval (part of the PureExpr bundle); command steps use the command relation EvalCmd : EvalCmdParamE.

A StepStmtE derivation describes one operational step and carries one event list; it never concatenates traces. A command step exposes exactly the events its command semantics produces. Every other rule is administrative and emits no events; the sequence and block context rules propagate the inner step's events unchanged. Intended choices, such as nondeterministic conditionals and loops, remain nondeterministic.

Constructors

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

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

Imperative.StepStmtE.step_block.{u_1, u_2} {CmdT : Type}
  {P : PureExpr} [HasBool P] {EventT : Type u_2}
  {EvalCmd : EvalCmdParamE P CmdT EventT} {x✝ : MetaData P}
  {label : String} {ss : List (Stmt P CmdT)}
  {ρ : Imperative.Env P} :
  StepStmtE P EvalCmd
    (Config.stmt (Stmt.block label ss x✝) ρ) []
    (Config.block (some label) ρ.store (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 is saved so that block-local variables can be popped on exit.

Imperative.StepStmtE.step_ite_true.{u_1, u_2} {CmdT : Type}
  {P : PureExpr} [HasBool P] {EventT : Type u_2}
  {EvalCmd : EvalCmdParamE P CmdT EventT} {x✝ : MetaData P}
  {c : P.Expr} {tss ess : List (Stmt P CmdT)}
  {ρ : Imperative.Env P} :
  P.eval ρ.factory ρ.store c =
      some (HasBool.ttVal ρ.factory) β†’
    StepStmtE P EvalCmd
      (Config.stmt
        (Stmt.ite (ExprOrNondet.det c) tss ess x✝) ρ)
      [] (Config.block none ρ.store (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).

Imperative.StepStmtE.step_ite_false.{u_1, u_2} {CmdT : Type}
  {P : PureExpr} [HasBool P] {EventT : Type u_2}
  {EvalCmd : EvalCmdParamE P CmdT EventT} {x✝ : MetaData P}
  {c : P.Expr} {tss ess : List (Stmt P CmdT)}
  {ρ : Imperative.Env P} :
  P.eval ρ.factory ρ.store c =
      some (HasBool.ffVal ρ.factory) β†’
    StepStmtE P EvalCmd
      (Config.stmt
        (Stmt.ite (ExprOrNondet.det c) tss ess x✝) ρ)
      [] (Config.block none ρ.store (Config.stmts ess ρ))

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

Imperative.StepStmtE.step_ite_nondet_true.{u_1, u_2}
  {CmdT : Type} {P : PureExpr} [HasBool P]
  {EventT : Type u_2}
  {EvalCmd : EvalCmdParamE P CmdT EventT} {x✝ : MetaData P}
  {tss ess : List (Stmt P CmdT)} {ρ : Imperative.Env P} :
  StepStmtE P EvalCmd
    (Config.stmt (Stmt.ite ExprOrNondet.nondet tss ess x✝)
      ρ)
    [] (Config.block none ρ.store (Config.stmts tss ρ))

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

Imperative.StepStmtE.step_ite_nondet_false.{u_1, u_2}
  {CmdT : Type} {P : PureExpr} [HasBool P]
  {EventT : Type u_2}
  {EvalCmd : EvalCmdParamE P CmdT EventT} {x✝ : MetaData P}
  {tss ess : List (Stmt P CmdT)} {ρ : Imperative.Env P} :
  StepStmtE P EvalCmd
    (Config.stmt (Stmt.ite ExprOrNondet.nondet tss ess x✝)
      ρ)
    [] (Config.block none ρ.store (Config.stmts ess ρ))

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

Imperative.StepStmtE.step_loop_enter.{u_1, u_2}
  {CmdT : Type} {P : PureExpr} [HasBool P]
  {EventT : Type u_2}
  {EvalCmd : EvalCmdParamE P CmdT EventT} {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.ttVal ρ.factory) β†’
    StepStmtE P EvalCmd
      (Config.stmt
        (Stmt.loop (ExprOrNondet.det g) m inv body md) ρ)
      []
      ((Config.block none ρ.store (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.

Imperative.StepStmtE.step_loop_exit.{u_1, u_2} {CmdT : Type}
  {P : PureExpr} [HasBool P] {EventT : Type u_2}
  {EvalCmd : EvalCmdParamE P CmdT EventT} {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.ffVal ρ.factory) β†’
    StepStmtE P EvalCmd
      (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.

Imperative.StepStmtE.step_loop_nondet_enter.{u_1, u_2}
  {CmdT : Type} {P : PureExpr} [HasBool P]
  {EventT : Type u_2}
  {EvalCmd : EvalCmdParamE P CmdT EventT}
  {m : Option P.Expr} {inv : List (String Γ— P.Expr)}
  {body : List (Stmt P CmdT)} {md : MetaData P}
  {ρ : Imperative.Env P} :
  StepStmtE P EvalCmd
    (Config.stmt
      (Stmt.loop ExprOrNondet.nondet m inv body md) ρ)
    []
    ((Config.block none ρ.store (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.

Imperative.StepStmtE.step_loop_nondet_exit.{u_1, u_2}
  {CmdT : Type} {P : PureExpr} [HasBool P]
  {EventT : Type u_2}
  {EvalCmd : EvalCmdParamE P CmdT EventT} {x✝ : MetaData P}
  {m : Option P.Expr} {inv : List (String Γ— P.Expr)}
  {body : List (Stmt P CmdT)} {ρ : Imperative.Env P} :
  StepStmtE P EvalCmd
    (Config.stmt
      (Stmt.loop ExprOrNondet.nondet m inv body x✝) ρ)
    [] (Config.terminal ρ)

Non-deterministic loop: exit the loop.

Imperative.StepStmtE.step_exit.{u_1, u_2} {CmdT : Type}
  {P : PureExpr} [HasBool P] {EventT : Type u_2}
  {EvalCmd : EvalCmdParamE P CmdT EventT} {x✝ : MetaData P}
  {label : String} {ρ : Imperative.Env P} :
  StepStmtE P EvalCmd (Config.stmt (Stmt.exit label x✝) ρ)
    [] (Config.exiting label ρ)

An exit statement produces an exiting configuration.

Imperative.StepStmtE.step_typeDecl.{u_1, u_2} {CmdT : Type}
  {P : PureExpr} [HasBool P] {EventT : Type u_2}
  {EvalCmd : EvalCmdParamE P CmdT EventT}
  {_tc : TypeConstructor} {_md : MetaData P}
  {ρ : Imperative.Env P} :
  StepStmtE P EvalCmd
    (Config.stmt (Stmt.typeDecl _tc _md) ρ) []
    (Config.terminal ρ)

A type declaration is a no-op at runtime.

Imperative.StepStmtE.step_stmts_nil.{u_1, u_2} {CmdT : Type}
  {P : PureExpr} [HasBool P] {EventT : Type u_2}
  {EvalCmd : EvalCmdParamE P CmdT EventT}
  {ρ : Imperative.Env P} :
  StepStmtE P EvalCmd (Config.stmts [] ρ) []
    (Config.terminal ρ)

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

Imperative.StepStmtE.step_stmts_cons.{u_1, u_2}
  {CmdT : Type} {P : PureExpr} [HasBool P]
  {EventT : Type u_2}
  {EvalCmd : EvalCmdParamE P CmdT EventT} {s : Stmt P CmdT}
  {ss : List (Stmt P CmdT)} {ρ : Imperative.Env P} :
  StepStmtE P EvalCmd (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.

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

A seq context steps its inner config forward, propagating its events.

Imperative.StepStmtE.step_seq_done.{u_1, u_2} {CmdT : Type}
  {P : PureExpr} [HasBool P] {EventT : Type u_2}
  {EvalCmd : EvalCmdParamE P CmdT EventT}
  {ρ' : Imperative.Env P} {ss : List (Stmt P CmdT)} :
  StepStmtE P EvalCmd ((Config.terminal ρ').seq ss) []
    (Config.stmts ss ρ')

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

Imperative.StepStmtE.step_seq_exit.{u_1, u_2} {CmdT : Type}
  {P : PureExpr} [HasBool P] {EventT : Type u_2}
  {EvalCmd : EvalCmdParamE P CmdT EventT} {label : String}
  {ρ' : Imperative.Env P} {ss : List (Stmt P CmdT)} :
  StepStmtE P EvalCmd ((Config.exiting label ρ').seq ss) []
    (Config.exiting label ρ')

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

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

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

Imperative.StepStmtE.step_block_done.{u_1, u_2}
  {CmdT : Type} {P : PureExpr} [HasBool P]
  {EventT : Type u_2}
  {EvalCmd : EvalCmdParamE P CmdT EventT}
  {label : Option String} {Οƒ_parent : SemanticStore P}
  {ρ' : Imperative.Env P} :
  StepStmtE P EvalCmd
    (Config.block label Οƒ_parent (Config.terminal ρ')) []
    (Config.terminal
      { store := projectStore Οƒ_parent ρ'.store,
        factory := ρ'.factory })

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 factory is preserved.

Imperative.StepStmtE.step_block_exit_match.{u_1, u_2}
  {CmdT : Type} {P : PureExpr} [HasBool P]
  {EventT : Type u_2}
  {EvalCmd : EvalCmdParamE P CmdT EventT}
  {label : Option String} {Οƒ_parent : SemanticStore P}
  {l : String} {ρ' : Imperative.Env P} :
  label = some l β†’
    StepStmtE P EvalCmd
      (Config.block label Οƒ_parent (Config.exiting l ρ')) []
      (Config.terminal
        { store := projectStore Οƒ_parent ρ'.store,
          factory := ρ'.factory })

When a block's inner body exits with a matching label, the block consumes it. The store is projected; the factory is preserved.

Imperative.StepStmtE.step_block_exit_mismatch.{u_1, u_2}
  {CmdT : Type} {P : PureExpr} [HasBool P]
  {EventT : Type u_2}
  {EvalCmd : EvalCmdParamE P CmdT EventT}
  {label : Option String} {Οƒ_parent : SemanticStore P}
  {l : String} {ρ' : Imperative.Env P} :
  label β‰  some l β†’
    StepStmtE P EvalCmd
      (Config.block label Οƒ_parent (Config.exiting l ρ')) []
      (Config.exiting l
        { store := projectStore Οƒ_parent ρ'.store,
          factory := ρ'.factory })

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. The store is projected since we're leaving this block.

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

πŸ”—inductive predicate
ReflTransTrace.{u, v} {A : Type u} {E : Type v}
  (r : A β†’ List E β†’ A β†’ Prop) : A β†’ List E β†’ A β†’ Prop
ReflTransTrace.{u, v} {A : Type u}
  {E : Type v}
  (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

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

IsReflexive execution emits the empty trace.

ReflTransTrace.step.{u, v} {A : Type u} {E : Type v}
  {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.{u_1, u_2} {CmdT : Type} (P : PureExpr)
  [HasBool P] {EventT : Type u_2}
  (EvalCmd : EvalCmdParamE P CmdT EventT) :
  Imperative.Config P CmdT β†’
    List EventT β†’ Imperative.Config P CmdT β†’ Prop
Imperative.StepStmtStarE.{u_1, u_2}
  {CmdT : Type} (P : PureExpr) [HasBool P]
  {EventT : Type u_2}
  (EvalCmd :
    EvalCmdParamE P CmdT EventT) :
  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.

πŸ”—def
Imperative.Config.emittedEvents.{u_1} {P : PureExpr} :
  Imperative.Config P (Cmd P) β†’ Trace P
Imperative.Config.emittedEvents.{u_1}
  {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.

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.{u} (l CmdT : Type) (P : PureExpr) : Type u
Imperative.CFGConfig.{u} (l CmdT : Type)
  (P : PureExpr) : Type u

Configuration for small-step CFG semantics. Every configuration carries:

  • the CFG program cfg, so the step relation need not capture a constructor-local program as a parameter; and

  • the execution environment ρ, so the store and expression factory travel together exactly as in structured statement configurations.

Active configurations carry cfg because it is needed for future fetches. Terminal configurations cannot step, so retaining a program there would be unobservable and would prevent the generic EventLang.terminalCfg operation from constructing exact outcomes.

Constructors

Imperative.CFGConfig.atBlock.{u} {l CmdT : Type}
  {P : PureExpr} :
  CFG l (DetBlock l CmdT P) β†’
    l β†’ Imperative.Env P β†’ CFGConfig l CmdT P

Configuration immediately before the block at the given label is fetched.

Imperative.CFGConfig.inBlock.{u} {l CmdT : Type}
  {P : PureExpr} :
  CFG l (DetBlock l CmdT P) β†’
    l β†’
      List CmdT β†’
        DetTransferCmd l P β†’
          Imperative.Env P β†’ CFGConfig l CmdT P

Configuration within a block, retaining its label, residual commands, and transfer.

Imperative.CFGConfig.terminal.{u} {l CmdT : Type}
  {P : PureExpr} : Imperative.Env P β†’ CFGConfig l CmdT P

Configuration after CFG execution has completed.

The StepCFGE relation takes one execution step over a deterministic CFG, emitting the events of the command it runs.

πŸ”—inductive predicate
Imperative.StepCFGE.{u_1, u_2} {l CmdT : Type} {EventT : Type u_1}
  [BEq l] (P : PureExpr) (EvalCmd : EvalCmdParamE P CmdT EventT)
  [HasBool P] [HasBoolOps P] [HasVal P] [HasFvars P] :
  CFGConfig l CmdT P β†’ List EventT β†’ CFGConfig l CmdT P β†’ Prop
Imperative.StepCFGE.{u_1, u_2}
  {l CmdT : Type} {EventT : Type u_1}
  [BEq l] (P : PureExpr)
  (EvalCmd : EvalCmdParamE P CmdT EventT)
  [HasBool P] [HasBoolOps P] [HasVal P]
  [HasFvars P] :
  CFGConfig l CmdT P β†’
    List EventT β†’
      CFGConfig l CmdT P β†’ Prop

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

The source configuration supplies both the CFG program and execution environment. Every constructor preserves the program and factory; command steps update only the store and emit the command's events, while control-flow steps update only control and emit no events. Consequently StepCFGE itself captures neither a factory nor a CFG program. An unconditional .goto k remains the definitional special case .condGoto HasBool.tt k k _ and is handled by goto_true.

Constructors

Imperative.StepCFGE.fetch.{u_1, u_2} {l CmdT : Type}
  {EventT : Type u_1} [BEq l] {P : PureExpr}
  {EvalCmd : EvalCmdParamE P CmdT EventT} [HasBool P]
  [HasBoolOps P] [HasVal P] [HasFvars P] {t : l}
  {b : DetBlock l CmdT P} {cfg : CFG l (DetBlock l CmdT P)}
  {ρ : Imperative.Env P} :
  List.lookup t cfg.blocks = some b β†’
    StepCFGE P EvalCmd (CFGConfig.atBlock cfg t ρ) []
      (CFGConfig.inBlock cfg t b.cmds b.transfer ρ)

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

Imperative.StepCFGE.step_cmd.{u_1, u_2} {l CmdT : Type}
  {EventT : Type u_1} [BEq l] {P : PureExpr}
  {EvalCmd : EvalCmdParamE P CmdT EventT} [HasBool P]
  [HasBoolOps P] [HasVal P] [HasFvars P] {c : CmdT}
  {Οƒ' : SemanticStore P} {emitted : List EventT}
  {cfg : CFG l (DetBlock l CmdT P)} {t : l} {cs : List CmdT}
  {tr : DetTransferCmd l P} {ρ : Imperative.Env P} :
  EvalCmd ρ.factory ρ.store c Οƒ' emitted β†’
    StepCFGE P EvalCmd
      (CFGConfig.inBlock cfg t (c :: cs) tr ρ) emitted
      (CFGConfig.inBlock cfg t cs tr
        { store := Οƒ', factory := ρ.factory })

Run one command from the residual list.

Imperative.StepCFGE.goto_true.{u_1, u_2} {l CmdT : Type}
  {EventT : Type u_1} [BEq l] {P : PureExpr}
  {EvalCmd : EvalCmdParamE P CmdT EventT} [HasBool P]
  [HasBoolOps P] [HasVal P] [HasFvars P] {c : P.Expr}
  {cfg : CFG l (DetBlock l CmdT P)} {t tlbl elbl : l}
  {md : MetaData P} {ρ : Imperative.Env P} :
  P.eval ρ.factory ρ.store c =
      some (HasBool.ttVal ρ.factory) β†’
    StepCFGE P EvalCmd
      (CFGConfig.inBlock cfg t []
        (DetTransferCmd.condGoto c tlbl elbl md) ρ)
      [] (CFGConfig.atBlock cfg tlbl ρ)

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

Imperative.StepCFGE.goto_false.{u_1, u_2} {l CmdT : Type}
  {EventT : Type u_1} [BEq l] {P : PureExpr}
  {EvalCmd : EvalCmdParamE P CmdT EventT} [HasBool P]
  [HasBoolOps P] [HasVal P] [HasFvars P] {c : P.Expr}
  {cfg : CFG l (DetBlock l CmdT P)} {t tlbl elbl : l}
  {md : MetaData P} {ρ : Imperative.Env P} :
  P.eval ρ.factory ρ.store c =
      some (HasBool.ffVal ρ.factory) β†’
    StepCFGE P EvalCmd
      (CFGConfig.inBlock cfg t []
        (DetTransferCmd.condGoto c tlbl elbl md) ρ)
      [] (CFGConfig.atBlock cfg elbl ρ)

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

Imperative.StepCFGE.finish.{u_1, u_2} {l CmdT : Type}
  {EventT : Type u_1} [BEq l] {P : PureExpr}
  {EvalCmd : EvalCmdParamE P CmdT EventT} [HasBool P]
  [HasBoolOps P] [HasVal P] [HasFvars P]
  {cfg : CFG l (DetBlock l CmdT P)} {t : l}
  {md : MetaData P} {ρ : Imperative.Env P} :
  StepCFGE P EvalCmd
    (CFGConfig.inBlock cfg t [] (DetTransferCmd.finish md)
      ρ)
    [] (CFGConfig.terminal ρ)

Empty residual + finish: halt at .terminal.

πŸ”—def
Imperative.StepCFGStarE.{u_1, u_2} {l CmdT : Type} {EventT : Type u_1}
  [BEq l] (P : PureExpr) (EvalCmd : EvalCmdParamE P CmdT EventT)
  [HasBool P] [HasBoolOps P] [HasVal P] [HasFvars P] :
  CFGConfig l CmdT P β†’ List EventT β†’ CFGConfig l CmdT P β†’ Prop
Imperative.StepCFGStarE.{u_1, u_2}
  {l CmdT : Type} {EventT : Type u_1}
  [BEq l] (P : PureExpr)
  (EvalCmd : EvalCmdParamE P CmdT EventT)
  [HasBool P] [HasBoolOps P] [HasVal P]
  [HasFvars P] :
  CFGConfig l CmdT P β†’
    List EventT β†’
      CFGConfig l CmdT P β†’ Prop

Reflexive-transitive event-trace execution of StepCFGE.

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.{u_1} {P : PureExpr} [HasBool P]
  [HasBoolOps P] (f : P.Factory) : Prop
Imperative.WellFormedSemanticEvalBool.{u_1}
  {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 (ttVal f) iff P.eval f Οƒ (not e) = some (ffVal f), and dually.

πŸ”—structure
Imperative.WellFormedSemanticEvalVal.{u_1} {P : PureExpr} [HasBool P]
  (f : P.Factory) : Prop
Imperative.WellFormedSemanticEvalVal.{u_1}
  {P : PureExpr} [HasBool P]
  (f : P.Factory) : Prop

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

Constructor

Imperative.WellFormedSemanticEvalVal.mk.{u_1}

Fields

outputsAreValues : βˆ€ (e : P.Expr) (v : P.Val) (Οƒ : SemanticStore P), WellFormedStore Οƒ f β†’ P.eval f Οƒ e = some v β†’ HasVal.value f v

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

eval_tt : βˆ€ (Οƒ : P.Ident β†’ Option P.Val), P.eval f Οƒ HasBool.tt = some (HasBool.ttVal f)

The Boolean constant tt evaluates to the value ttVal f.

eval_ff : βˆ€ (Οƒ : P.Ident β†’ Option P.Val), P.eval f Οƒ HasBool.ff = some (HasBool.ffVal f)

The Boolean constant ff evaluates to the value ffVal f.

πŸ”—def
Imperative.WellFormedSemanticEvalVar.{u_1} {P : PureExpr} [HasVal P]
  [HasFvar P] (f : P.Factory) : Prop
Imperative.WellFormedSemanticEvalVar.{u_1}
  {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.{u_1} {P : PureExpr}
  [HasVal P] [HasFvars P] (f : P.Factory) : Prop
Imperative.WellFormedSemanticEvalExprCongr.{u_1}
  {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.{u_1} {P : PureExpr} [HasBool P]
  [HasFvars P] [HasInt P] [HasIntOps P] (f : P.Factory) : Prop
Imperative.WellFormedSemanticEvalInt.{u_1}
  {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.{u_1}

Fields

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

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.{u_1} {P : PureExpr}
  (f : P.Factory) : Prop
Imperative.WellFormedSemanticEvalMono.{u_1}
  {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.{u_1} {P : PureExpr} [HasVal P]
  [HasFvar P] [HasSubstFvar P] (f : P.Factory) : Prop
Imperative.WellFormedSemanticEvalRename.{u_1}
  {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 store bindings that are not values under which a step-indexed evaluator could otherwise diverge.

πŸ”—structure
Imperative.WellFormedSemanticEval.{u_1} {P : PureExpr} [HasBool P]
  [HasBoolOps P] [HasFvar P] [HasFvars P] [HasInt P] [HasIntOps P]
  [HasSubstFvar P] (f : P.Factory) : Prop
Imperative.WellFormedSemanticEval.{u_1}
  {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.{u_1}

Extends

Fields

var : WellFormedSemanticEvalVar f
Inherited from
  1. WellFormedSemanticEvalBase f
val : WellFormedSemanticEvalVal f
Inherited from
  1. WellFormedSemanticEvalBase f
exprCongr : WellFormedSemanticEvalExprCongr f
Inherited from
  1. WellFormedSemanticEvalBase f
rename : WellFormedSemanticEvalRename f
Inherited from
  1. WellFormedSemanticEvalBase f
bool : WellFormedSemanticEvalBool f

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

int : WellFormedSemanticEvalInt f

The evaluator reduces integer comparisons to booleans.

mono : WellFormedSemanticEvalMono f

The evaluator is monotone under store extension.

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

Core.TypeSpec.CmdExtHasType'.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'.

Core.TypeSpec.CmdExtHasType'.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 β†’
    WF.WFcallProp P pname callArgs β†’
      (βˆ€ (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)) β†’
            Ξ”.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, and the call is well-formed (WF.WFcallProp): its arguments match the procedure's parameters in number and mode, and its result variables are distinct.

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

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

3.1.2.Β DatatypesπŸ”—

A mutual datatype declaration is well-typed when registering its block with LContext.addMutualBlock succeeds (DeclHasType'.type_data).

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

Every block that LContext.addMutualBlock accepts satisfies MutualADTWF (Datatype.addMutualBlock_sound).

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.

typeArgsAgree : βˆ€ (d : LDatatype Unit),
  d ∈ block β†’ βˆ€ (d' : LDatatype Unit), d' ∈ block β†’ βˆ€ (v : TyIdentifier), v ∈ d.typeArgs ↔ v ∈ d'.typeArgs

All datatypes in the block declare the same type parameters, ignoring order.

typeArgsNodup : βˆ€ (d : LDatatype Unit), d ∈ block β†’ d.typeArgs.Nodup

No datatype declares a type parameter twice.

typeArgsNotReserved : βˆ€ (d : LDatatype Unit), d ∈ block β†’ βˆ€ (v : TyIdentifier), v ∈ d.typeArgs β†’ isAllowedName v = true

No declared type parameter starts with a reserved prefix.

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.

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 command typing); 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).

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

Core.TypeSpec.DeclHasType'.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.

Core.TypeSpec.DeclHasType'.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.

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

A (mutual) datatype declaration: LContext.addMutualBlock accepts the block and extends C with its datatypes and their generated functions. The block then satisfies MutualADTWF (Datatype.addMutualBlock_sound). Ξ“ is unchanged.

Core.TypeSpec.DeclHasType'.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.

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

A lemma declaration: its expression is a bool in the current context. Contexts are unchanged.

Core.TypeSpec.DeclHasType'.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.

Core.TypeSpec.DeclHasType'.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.

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

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

Core.TypeSpec.DeclHasType'.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 β†’ Β¬f.name.name ∈ C.functions) β†’
      (βˆ€ (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 (fun f g => g = f) C
                Cstub stubs β†’
              TypeSpec.FactoryExtendedBy (fun f g => g = f)
                  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, contains no inline functions, and no block function is named like a function of C; Ξ“ 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

Core.TypeSpec.DeclsHasType'.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.

Core.TypeSpec.DeclsHasType'.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 (EvalCmdExtE.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 EvalCmdExtContractE.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.EventLang P EventT)πŸ”—

Strata provides formal definitions for reasoning about Imperative and Strata Core. The framework is built on a small, language-agnostic abstraction, the EventLang P EventT bundle (P is a parameter for the pure-expression type PureExpr, and EventT is the event alphabet). It packages exactly what a program logic or a transform specification needs from a language: a one-step relation that emits events, together with a trace-producing closure, EventLang.traceStar.

πŸ”—structure
Strata.Logic.EventLang.{u, v} (P : PureExpr) (EventT : Type v) :
  Type (max (u + 1) v)
Strata.Logic.EventLang.{u, v}
  (P : PureExpr) (EventT : Type v) :
  Type (max (u + 1) v)

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. Assertion observations are carried by EventT rather than detected from configurations.

Constructor

Strata.Logic.EventLang.mk.{u, v}

Fields

StmtT : Type

Statement type.

CfgT : Type u

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. The Core languages use a record bundling reserved fresh prefixes and a declaredFuncs predicate (see Core.Logic.InitEnvWFParams).

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

Language-specific initial-environment well-formedness.

The EventLang structure itself belongs to no dialect, and the definitions in this chapter quantify over an arbitrary EventLang. For the Imperative dialect the instances live in the Imperative.Logic namespace: structured statements, block bodies, deterministic control-flow graphs (EventLang.cfgE), and Kleene statements (EventLang.kleeneE). The structured constructors package StepStmtE for individual statements and statement lists. Their command evaluator determines EventT.

πŸ”—def
Strata.Logic.EventLang.TerminatesAt.{u_1, u_2} {P : PureExpr}
  {EventT : Type u_2} (EL : Strata.Logic.EventLang P EventT)
  (s : EL.StmtT) (ρ₀ : Imperative.Env P) (trace : List EventT)
  (ρ' : Imperative.Env P) : Prop
Strata.Logic.EventLang.TerminatesAt.{u_1,
    u_2}
  {P : PureExpr} {EventT : Type u_2}
  (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.{u_1, u_2} {P : PureExpr}
  {EventT : Type u_2} (EL : Strata.Logic.EventLang P EventT)
  (s : EL.StmtT) (ρ₀ : Imperative.Env P) : Prop
Strata.Logic.EventLang.Terminates.{u_1,
    u_2}
  {P : PureExpr} {EventT : Type u_2}
  (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.{u_1, u_2} (P : PureExpr)
  [HasBool P] [HasBoolOps P] [HasFvar P] [HasFvars P] [HasInt P]
  [HasIntOps P] [HasSubstFvar P] (CmdT : Type) {EventT : Type u_2}
  (evalCmd : EvalCmdParamE P CmdT EventT) (ParamsTy : Type)
  (initEnvWF : ParamsTy β†’ Stmt P CmdT β†’ Imperative.Env P β†’ Prop) :
  Strata.Logic.EventLang P EventT
Imperative.Logic.EventLang.imperativeE.{u_1,
    u_2}
  (P : PureExpr) [HasBool P]
  [HasBoolOps P] [HasFvar P] [HasFvars P]
  [HasInt P] [HasIntOps P]
  [HasSubstFvar P] (CmdT : Type)
  {EventT : Type u_2}
  (evalCmd : EvalCmdParamE P CmdT EventT)
  (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.{u_1, u_2} (P : PureExpr)
  [HasBool P] [HasBoolOps P] [HasFvar P] [HasFvars P] [HasInt P]
  [HasIntOps P] [HasSubstFvar P] (CmdT : Type) {EventT : Type u_2}
  (evalCmd : EvalCmdParamE P CmdT EventT)
  (wfPkg :
    (ParamsTy : Type) Γ—
      (ParamsTy β†’ List (Stmt P CmdT) β†’ Imperative.Env P β†’ Prop)) :
  Strata.Logic.EventLang P EventT
Imperative.Logic.EventLang.imperativeBlockE.{u_1,
    u_2}
  (P : PureExpr) [HasBool P]
  [HasBoolOps P] [HasFvar P] [HasFvars P]
  [HasInt P] [HasIntOps P]
  [HasSubstFvar P] (CmdT : Type)
  {EventT : Type u_2}
  (evalCmd : EvalCmdParamE P CmdT EventT)
  (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. wfPkg carries the initial-environment well-formedness parameters and predicate, for example ⟨InitEnvWFParams P, BlockInitEnvWF⟩.

Strata Core instantiates these as EventLang.core, EventLang.coreBlock, and EventLang.coreCFG. The Core language bundles use their own initial-environment well-formedness predicates InitEnvWF, BlockInitEnvWF, and CFGInitEnvWF. Core's logic and analysis judgements are mostly all over EventLang.coreBlock because it is more convenient than EventLang.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.{u, w} (P : PureExpr) : Type (max u (w + 1))
Imperative.ConditionInterp.{u, w}
  (P : PureExpr) : Type (max u (w + 1))

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

Constructor

Imperative.ConditionInterp.mk.{u, w}

Fields

World : Type w

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.

πŸ”—def
Imperative.Event.neutral.{u_1, u_2} (P : PureExpr)
  (I : ConditionInterp P) : Event P β†’ Prop
Imperative.Event.neutral.{u_1, u_2}
  (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.{u_1, u_2} (P : PureExpr)
  (I : ConditionInterp P) (world : I.World) (trace : Trace P) : Prop
Imperative.Trace.AssumptionsHold.{u_1,
    u_2}
  (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.{u_1, u_2} (P : PureExpr)
  (I : ConditionInterp P) (trace : Trace P) : Prop
Imperative.Trace.Reachable.{u_1, u_2}
  (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.{u_1, u_2} (P : PureExpr)
  (I : ConditionInterp P) (keep : EventArg P β†’ Prop) :
  Trace P β†’ Trace P β†’ Prop
Imperative.Trace.AssertionsValidFromP.{u_1,
    u_2}
  (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.{u_1, u_2} (P : PureExpr)
  (I : ConditionInterp P) : Trace P β†’ Trace P β†’ Prop
Imperative.Trace.AssertionsValidFrom.{u_1,
    u_2}
  (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.{u_1, u_2} (P : PureExpr)
  (I : ConditionInterp P) (trace : Trace P) : Prop
Imperative.Trace.AssertionsValid.{u_1,
    u_2}
  (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.{u_1, u_2} (P : PureExpr)
  (I : ConditionInterp P) (aid : AssertId P) : Trace P β†’ Trace P β†’ Prop
Imperative.Trace.AssertionValidFrom.{u_1,
    u_2}
  (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.{u_1, u_2} (P : PureExpr)
  (I : ConditionInterp P) (aid : AssertId P) (trace : Trace P) : Prop
Imperative.Trace.AssertionValid.{u_1, u_2}
  (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.{u_1, u_2} (P : PureExpr)
  (I : ConditionInterp P) (aid : AssertId P) : Trace P β†’ Trace P β†’ Prop
Imperative.Trace.AssertionSatisfiableFrom.{u_1,
    u_2}
  (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.{u_1, u_2} (P : PureExpr)
  (I : ConditionInterp P) (aid : AssertId P) (trace : Trace P) : Prop
Imperative.Trace.AssertionSatisfiable.{u_1,
    u_2}
  (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.{u_1, u_2} (P : PureExpr)
  (I : ConditionInterp P) (cid : CoverId P) : Trace P β†’ Trace P β†’ Prop
Imperative.Trace.CoverSatisfiableFrom.{u_1,
    u_2}
  (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.{u_1, u_2} (P : PureExpr)
  (I : ConditionInterp P) (cid : CoverId P) (trace : Trace P) : Prop
Imperative.Trace.CoverSatisfiable.{u_1,
    u_2}
  (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.{u_1, u_2}
  {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.{u_1,
    u_2}
  {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.{u_1, u_2}
  {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.{u_1,
    u_2}
  {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.TripleWith (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 its supplied condition interpreter. 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) instantiate the Imperative template over its block language EventLang.coreBlock with its own wellformedness conditions Core.Logic.BlockInitEnvWF and discharge the side conditions. Core's expression evaluator is denotational: Core.Expression.eval is Lambda.LExpr.denoteEval, which annotates each free variable with the sort of its stored value, type checks the expression, and interprets it with Lambda.LExpr.denote in the model that the runtime factory carries (Lambda.ModeledFactory). Stores hold semantic values (Lambda.SemValue), so a condition captured by an event is interpreted without substitution: Core.Logic.DenoteBasedInterp F reads a condition captured under a runtime factory over F as true when it evaluates to true. A Core triple quantifies over its entry environments, and so over every model of F. In this current denotation, Core real has Lean domain Rat; these correctness statements are therefore about rational semantics and do not claim adequacy with mathematical or SMT Real. 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. Both quantify over traces produced by an EventLang. Assertion validity is 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.{u_1, u_2}
  {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.{u_1,
    u_2}
  {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.{u_1, u_2}
  {P : PureExpr} (EL : Strata.Logic.EventLang P (Event P))
  (I : ConditionInterp P) (Pre : Imperative.Env P β†’ Prop)
  (s : EL.StmtT) : Prop
Imperative.Specification.AllAssertsValidOnTracesWhen.{u_1,
    u_2}
  {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.{u_1, u_2}
  {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.{u_1,
    u_2}
  {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.{u_1, u_2}
  {P : PureExpr} (EL : Strata.Logic.EventLang P (Event P))
  (I : ConditionInterp P) (s : EL.StmtT) (a : AssertId P) : Prop
Imperative.Specification.AssertSatisfiableOnTraces.{u_1,
    u_2}
  {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πŸ”—

An analysis is defined by a relation between a program and an output, saying which outputs are correct answers about the program. An analyzer is any function producing outputs, and it implements the analysis when every output it produces is correct:

πŸ”—def
Imperative.Analysis.MatchesAnalysis {β„™ D : Type} (analyzer : β„™ β†’ D)
  (analysisDefinition : β„™ β†’ D β†’ Prop) : Prop
Imperative.Analysis.MatchesAnalysis
  {β„™ D : Type} (analyzer : β„™ β†’ D)
  (analysisDefinition : β„™ β†’ D β†’ Prop) :
  Prop

analyzer implements analysisDefinition: on every program, the output it produces is one the definition accepts as correct.

Soundness and completeness of a pass/fail analyzer are two such definitions:

πŸ”—def
Imperative.Analysis.Sound {β„™ D : Type} (property : β„™ β†’ Prop)
  (pass : D β†’ Prop) : β„™ β†’ D β†’ Prop
Imperative.Analysis.Sound {β„™ D : Type}
  (property : β„™ β†’ Prop)
  (pass : D β†’ Prop) : β„™ β†’ D β†’ Prop

Soundness as an analysis definition: an output is correct when passing implies property, so a passing output claims property, and any other claims nothing. An analyzer matches it exactly when it passes only programs with the property.

πŸ”—def
Imperative.Analysis.Complete {β„™ D : Type} (property : β„™ β†’ Prop)
  (pass : D β†’ Prop) : β„™ β†’ D β†’ Prop
Imperative.Analysis.Complete {β„™ D : Type}
  (property : β„™ β†’ Prop)
  (pass : D β†’ Prop) : β„™ β†’ D β†’ Prop

Completeness as an analysis definition: an output is correct when property implies passing. An analyzer matches it exactly when it passes every program with the property.

Core's verifier is specified by CoreVerifierModel:

πŸ”—def
Core.Specification.Analysis.CoreVerifierModel (mode : VerificationMode)
  (params : Core.Logic.InitEnvWFParams) :
  Specification.Analysis.CoreVerifierInput β†’ Core.VCResults β†’ Prop
Core.Specification.Analysis.CoreVerifierModel
  (mode : VerificationMode)
  (params : Core.Logic.InitEnvWFParams) :
  Specification.Analysis.CoreVerifierInput β†’
    Core.VCResults β†’ Prop

The definition of Core verification under each VerificationMode. A VCResults array passing under the mode claims:

  • .deductive: ProcedureAssertsValidOnTraces.denote (universal: from every entry environment, so in every model, every assertion a run reaches is valid and every terminating run satisfies the postconditions);

  • .bugFinding: ProcedureAssertsSatisfiableOnTraces.denote (existential dual: from some entry environment, some run reaches each assert and some terminating run satisfies the postconditions);

  • .bugFindingAssumingCompleteSpec: not yet specified. Every result passes and claims False, so no analyzer implements this mode yet.

  • .deductiveAssumingSatisfiablePaths: as .deductive. The mode's premise only adds failures, never passes, so a pass claims the same as in .deductive; failures reported under the premise are not specified.

A result that does not pass claims nothing. An analyzer analyze implements the mode when MatchesAnalysis (analyze mode) (CoreVerifierModel mode params). params fixes the entry well-formedness of procedure bodies (see ProcEnvWF). It must admit the program's entry environments: when it admits none, the property holds vacuously, so a soundness statement should fix params to the one the verifier assumes rather than leave it free.

What a pass claims is selected by the VerificationMode: in deductive mode, that every entry procedure's assertions are valid; in bug-finding mode, that they are 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 OverapproximatesTraces family relates the chronological event lists produced by source and target executions. The most general member carries separate input/output environment relations, and may relate finite prefixes and terminal or exiting runs by different trace relations; the others relate both by one trace relation.

πŸ”—def
Imperative.Specification.Transform.OverapproximatesTraces2UptoWhen.{u_1,
    u_2}
  {P : PureExpr} {EventT : Type u_2}
  (Rtrace Rtrace_full : 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.OverapproximatesTraces2UptoWhen.{u_1,
    u_2}
  {P : PureExpr} {EventT : Type u_2}
  (Rtrace Rtrace_full :
    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, with one trace relation for finite prefixes and another for completed runs. Every finite source prefix has a target prefix related by Rtrace; every terminal or exiting source run has a target run ending the same way, in an Rout-related environment, with its trace related by Rtrace_full. The prefix clause carries safety properties such as assertion validity; the run clauses carry what completed runs establish, such as postconditions and the context of the statements that follow. A transformation covering one source run by several target runs, each faithful to a part of it, can promise more about prefixes than about runs, and so relate them by different relations. The definition is independent of any particular trace property or condition interpretation.

πŸ”—def
Imperative.Specification.Transform.OverapproximatesTracesUptoWhen.{u_1,
    u_2}
  {P : PureExpr} {EventT : Type u_2} (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.{u_1,
    u_2}
  {P : PureExpr} {EventT : Type u_2}
  (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: finite prefixes and completed runs are related by the same trace relation Rtrace (OverapproximatesTraces2UptoWhen with Rtrace_full := Rtrace). It simulates every finite prefix (for safety properties) and terminal/exiting runs (for partial-correctness postconditions).

πŸ”—def
Imperative.Specification.Transform.OverapproximatesTracesWhen.{u_1, u_2}
  {P : PureExpr} {EventT : Type u_2} (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.{u_1,
    u_2}
  {P : PureExpr} {EventT : Type u_2}
  (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.{u_1, u_2}
  {P : PureExpr} {EventT : Type u_2} (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.{u_1,
    u_2}
  {P : PureExpr} {EventT : Type u_2}
  (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.

Every law about the family is proved for the two-relation member and then instantiated for the others, which relate prefixes and runs by one trace relation. Weakening a relation preserves an overapproximation: the trace relations may be coarsened (OverapproximatesTraces2UptoWhen.mono_trace, with its instance OverapproximatesTracesUptoWhen.mono_trace), and so may the output environment relation while the input environment relation is refined (OverapproximatesTraces2UptoWhen.mono_env).

πŸ”—theorem
Imperative.Specification.Transform.OverapproximatesTraces2UptoWhen.mono_trace.{u_1,
    u_2}
  {P : PureExpr} {EventT : Type u_1}
  {Rtrace Rtrace' Rtrace_full Rtrace_full' : 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}
  (hsub : βˆ€ (t t' : List EventT), Rtrace t t' β†’ Rtrace' t t')
  (hsub_full :
    βˆ€ (t t' : List EventT), Rtrace_full t t' β†’ Rtrace_full' t t')
  (h :
    Specification.Transform.OverapproximatesTraces2UptoWhen Rtrace
      Rtrace_full Rin Rout L₁ Lβ‚‚ T pre params₁ paramsβ‚‚) :
  Specification.Transform.OverapproximatesTraces2UptoWhen Rtrace'
    Rtrace_full' Rin Rout L₁ Lβ‚‚ T pre params₁ paramsβ‚‚
Imperative.Specification.Transform.OverapproximatesTraces2UptoWhen.mono_trace.{u_1,
    u_2}
  {P : PureExpr} {EventT : Type u_1}
  {Rtrace Rtrace' Rtrace_full
    Rtrace_full' : 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}
  (hsub :
    βˆ€ (t t' : List EventT),
      Rtrace t t' β†’ Rtrace' t t')
  (hsub_full :
    βˆ€ (t t' : List EventT),
      Rtrace_full t t' β†’
        Rtrace_full' t t')
  (h :
    Specification.Transform.OverapproximatesTraces2UptoWhen
      Rtrace Rtrace_full Rin Rout L₁ Lβ‚‚ T
      pre params₁ paramsβ‚‚) :
  Specification.Transform.OverapproximatesTraces2UptoWhen
    Rtrace' Rtrace_full' Rin Rout L₁ Lβ‚‚ T
    pre params₁ paramsβ‚‚

Trace-relation weakening. Both trace relations occur only covariantly in OverapproximatesTraces2UptoWhen, so replacing them by coarser relations preserves the overapproximation.

πŸ”—theorem
Imperative.Specification.Transform.OverapproximatesTraces2UptoWhen.mono_env.{u_1,
    u_2}
  {P : PureExpr} {EventT : Type u_1}
  {Rtrace Rtrace_full : Relation (List EventT)}
  {Rin Rin' Rout 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}
  (hin : βˆ€ (ρ ρ' : Imperative.Env P), Rin' ρ ρ' β†’ Rin ρ ρ')
  (hout : βˆ€ (ρ ρ' : Imperative.Env P), Rout ρ ρ' β†’ Rout' ρ ρ')
  (h :
    Specification.Transform.OverapproximatesTraces2UptoWhen Rtrace
      Rtrace_full Rin Rout L₁ Lβ‚‚ T pre params₁ paramsβ‚‚) :
  Specification.Transform.OverapproximatesTraces2UptoWhen Rtrace
    Rtrace_full Rin' Rout' L₁ Lβ‚‚ T pre params₁ paramsβ‚‚
Imperative.Specification.Transform.OverapproximatesTraces2UptoWhen.mono_env.{u_1,
    u_2}
  {P : PureExpr} {EventT : Type u_1}
  {Rtrace Rtrace_full :
    Relation (List EventT)}
  {Rin Rin' Rout 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}
  (hin :
    βˆ€ (ρ ρ' : Imperative.Env P),
      Rin' ρ ρ' β†’ Rin ρ ρ')
  (hout :
    βˆ€ (ρ ρ' : Imperative.Env P),
      Rout ρ ρ' β†’ Rout' ρ ρ')
  (h :
    Specification.Transform.OverapproximatesTraces2UptoWhen
      Rtrace Rtrace_full Rin Rout L₁ Lβ‚‚ T
      pre params₁ paramsβ‚‚) :
  Specification.Transform.OverapproximatesTraces2UptoWhen
    Rtrace Rtrace_full Rin' Rout' L₁ Lβ‚‚ T
    pre params₁ paramsβ‚‚

Environment-relation weakening. The input relation occurs contravariantly (it restricts the entry environments) and the output relation covariantly, so a finer input relation and a coarser output relation preserve the overapproximation.

Validity of an assertion transports back from the target to the source through the prefix trace relation, when it reflects that validity: overapproximatesTraces2UptoWhen_assertValid for one assertion identifier and overapproximatesTraces2UptoWhen_allAsserts for all assertions, with the one-relation instances overapproximatesTracesUptoWhen_assertValid, overapproximatesTraces_assertValid and overapproximatesTraces_allAsserts. A transformation whose target traces drop source events, such as loop elimination, cannot keep every assertion of a source trace in one target trace; its prefix relation can still keep the last assertion of a prefix (Trace.ReflectsLastAssertion), which suffices through overapproximatesTraces2UptoWhen_assertValid_of_reflectsLastAssertion, and, for a verifier run after the transformation, through ValidOnTracesVerifier.of_overapproximatesTraces2UptoWhen_of_reflectsLastAssertion.

πŸ”—theorem
Imperative.Specification.Transform.overapproximatesTraces2UptoWhen_assertValid.{u_1,
    u_2}
  {P : PureExpr} (I : ConditionInterp P)
  {Rtrace Rtrace_full : Relation (Trace P)}
  {Rout : Relation (Imperative.Env P)}
  {L₁ Lβ‚‚ : Strata.Logic.EventLang P (Event P)}
  {T : L₁.StmtT β†’ Option Lβ‚‚.StmtT} {pre : L₁.StmtT β†’ Prop}
  {params₁ : L₁.InitEnvWFParamsTy} {paramsβ‚‚ : Lβ‚‚.InitEnvWFParamsTy}
  (hreflect :
    βˆ€ (trace trace' : Trace P),
      Rtrace trace trace' β†’
        βˆ€ (aid : AssertId P),
          Trace.AssertionValid P I aid trace' β†’
            Trace.AssertionValid P I aid trace)
  (hover :
    Specification.Transform.OverapproximatesTraces2UptoWhen Rtrace
      Rtrace_full (fun x1 x2 => x1 = x2) Rout L₁ Lβ‚‚ T pre params₁
      paramsβ‚‚)
  {st : L₁.StmtT} {st' : Lβ‚‚.StmtT} {aid : AssertId P}
  (ht : T st = some st') (hpre : pre st)
  (hvalid :
    Specification.AssertValidOnTracesWhen Lβ‚‚ I
      (Lβ‚‚.initEnvWF paramsβ‚‚ st') st' aid) :
  Specification.AssertValidOnTracesWhen L₁ I (L₁.initEnvWF params₁ st)
    st aid
Imperative.Specification.Transform.overapproximatesTraces2UptoWhen_assertValid.{u_1,
    u_2}
  {P : PureExpr} (I : ConditionInterp P)
  {Rtrace Rtrace_full :
    Relation (Trace P)}
  {Rout : Relation (Imperative.Env P)}
  {L₁ Lβ‚‚ :
    Strata.Logic.EventLang P (Event P)}
  {T : L₁.StmtT β†’ Option Lβ‚‚.StmtT}
  {pre : L₁.StmtT β†’ Prop}
  {params₁ : L₁.InitEnvWFParamsTy}
  {paramsβ‚‚ : Lβ‚‚.InitEnvWFParamsTy}
  (hreflect :
    βˆ€ (trace trace' : Trace P),
      Rtrace trace trace' β†’
        βˆ€ (aid : AssertId P),
          Trace.AssertionValid P I aid
              trace' β†’
            Trace.AssertionValid P I aid
              trace)
  (hover :
    Specification.Transform.OverapproximatesTraces2UptoWhen
      Rtrace Rtrace_full
      (fun x1 x2 => x1 = x2) Rout L₁ Lβ‚‚ T
      pre params₁ paramsβ‚‚)
  {st : L₁.StmtT} {st' : Lβ‚‚.StmtT}
  {aid : AssertId P}
  (ht : T st = some st') (hpre : pre st)
  (hvalid :
    Specification.AssertValidOnTracesWhen
      Lβ‚‚ I (Lβ‚‚.initEnvWF paramsβ‚‚ st') st'
      aid) :
  Specification.AssertValidOnTracesWhen L₁
    I (L₁.initEnvWF params₁ st) st aid

A trace overapproximation with two trace relations, equal initial environments and any relation Rout between final environments transports validity of one assertion identifier when its prefix relation reflects that validity. The run relation is not used.

πŸ”—theorem
Imperative.Specification.Transform.overapproximatesTraces2UptoWhen_assertValid_of_reflectsLastAssertion.{u_1,
    u_2}
  {P : PureExpr} (I : ConditionInterp P)
  {Rprefix Rtrace_full : Relation (Trace P)}
  (hR : Trace.ReflectsLastAssertion I Rprefix)
  (Rout : Relation (Imperative.Env P))
  (L₁ Lβ‚‚ : Strata.Logic.EventLang P (Event P))
  (T : L₁.StmtT β†’ Option Lβ‚‚.StmtT) (pre : L₁.StmtT β†’ Prop)
  (params₁ : L₁.InitEnvWFParamsTy) (paramsβ‚‚ : Lβ‚‚.InitEnvWFParamsTy)
  (hover :
    Specification.Transform.OverapproximatesTraces2UptoWhen Rprefix
      Rtrace_full (fun x1 x2 => x1 = x2) Rout L₁ Lβ‚‚ T pre params₁
      paramsβ‚‚)
  {st : L₁.StmtT} {st' : Lβ‚‚.StmtT} {aid : AssertId P}
  (ht : T st = some st') (hpre : pre st)
  (hprefix :
    βˆ€ (ρ₀ : Imperative.Env P) (cfg : L₁.CfgT) (tr : List (Event P))
      (e : Event P) (post : List (Event P)),
      L₁.traceStar (L₁.stmtCfg st ρ₀) (tr ++ e :: post) cfg β†’
        βˆƒ cfg', L₁.traceStar (L₁.stmtCfg st ρ₀) (tr ++ [e]) cfg')
  (hvalid :
    Specification.AssertValidOnTracesWhen Lβ‚‚ I
      (Lβ‚‚.initEnvWF paramsβ‚‚ st') st' aid) :
  Specification.AssertValidOnTracesWhen L₁ I (L₁.initEnvWF params₁ st)
    st aid
Imperative.Specification.Transform.overapproximatesTraces2UptoWhen_assertValid_of_reflectsLastAssertion.{u_1,
    u_2}
  {P : PureExpr} (I : ConditionInterp P)
  {Rprefix Rtrace_full :
    Relation (Trace P)}
  (hR :
    Trace.ReflectsLastAssertion I Rprefix)
  (Rout : Relation (Imperative.Env P))
  (L₁ Lβ‚‚ :
    Strata.Logic.EventLang P (Event P))
  (T : L₁.StmtT β†’ Option Lβ‚‚.StmtT)
  (pre : L₁.StmtT β†’ Prop)
  (params₁ : L₁.InitEnvWFParamsTy)
  (paramsβ‚‚ : Lβ‚‚.InitEnvWFParamsTy)
  (hover :
    Specification.Transform.OverapproximatesTraces2UptoWhen
      Rprefix Rtrace_full
      (fun x1 x2 => x1 = x2) Rout L₁ Lβ‚‚ T
      pre params₁ paramsβ‚‚)
  {st : L₁.StmtT} {st' : Lβ‚‚.StmtT}
  {aid : AssertId P}
  (ht : T st = some st') (hpre : pre st)
  (hprefix :
    βˆ€ (ρ₀ : Imperative.Env P)
      (cfg : L₁.CfgT)
      (tr : List (Event P)) (e : Event P)
      (post : List (Event P)),
      L₁.traceStar (L₁.stmtCfg st ρ₀)
          (tr ++ e :: post) cfg β†’
        βˆƒ cfg',
          L₁.traceStar (L₁.stmtCfg st ρ₀)
            (tr ++ [e]) cfg')
  (hvalid :
    Specification.AssertValidOnTracesWhen
      Lβ‚‚ I (Lβ‚‚.initEnvWF paramsβ‚‚ st') st'
      aid) :
  Specification.AssertValidOnTracesWhen L₁
    I (L₁.initEnvWF params₁ st) st aid

Assertion validity transported through a trace overapproximation whose prefixes reflect last assertions. A trace overapproximation with equal initial environments whose prefix relation Rprefix reflects last assertions under I (Trace.ReflectsLastAssertion) transports validity of an assertion identifier, when the source traces are closed under prefixes ending at an event. Each source occurrence of aid is reflected through the prefix ending at it, whose related target trace has that occurrence after assumptions implied by those before it in the source. The run relation Rtrace_full is not used.

πŸ”—theorem
Imperative.Specification.Analysis.ValidOnTracesVerifier.of_overapproximatesTraces2UptoWhen_of_reflectsLastAssertion.{u_1,
    u_2}
  {P : PureExpr} {I : ConditionInterp P}
  {Rprefix Rtrace_full : Relation (Trace P)}
  {Rout : Relation (Imperative.Env P)}
  {L₁ Lβ‚‚ : Strata.Logic.EventLang P (Event P)}
  {T : L₁.StmtT β†’ Option Lβ‚‚.StmtT} {pre : L₁.StmtT β†’ Prop}
  {params₁ : L₁.InitEnvWFParamsTy} {paramsβ‚‚ : Lβ‚‚.InitEnvWFParamsTy}
  {analyze : Lβ‚‚.StmtT β†’ Bool}
  (hR : Trace.ReflectsLastAssertion I Rprefix)
  (hover :
    Specification.Transform.OverapproximatesTraces2UptoWhen Rprefix
      Rtrace_full (fun x1 x2 => x1 = x2) Rout L₁ Lβ‚‚ T pre params₁
      paramsβ‚‚)
  (hprefix :
    βˆ€ (st : L₁.StmtT),
      pre st β†’
        βˆ€ (ρ₀ : Imperative.Env P) (cfg : L₁.CfgT) (tr : List (Event P))
          (e : Event P) (post : List (Event P)),
          L₁.traceStar (L₁.stmtCfg st ρ₀) (tr ++ e :: post) cfg β†’
            βˆƒ cfg', L₁.traceStar (L₁.stmtCfg st ρ₀) (tr ++ [e]) cfg')
  (hsound :
    Specification.Analysis.ValidOnTracesVerifier Lβ‚‚ I
      (Lβ‚‚.initEnvWF paramsβ‚‚) analyze) :
  Specification.Analysis.ValidOnTracesVerifier L₁ I
    (fun s ρ₀ => pre s ∧ L₁.initEnvWF params₁ s ρ₀)
    (Analysis.thenVerify T analyze)
Imperative.Specification.Analysis.ValidOnTracesVerifier.of_overapproximatesTraces2UptoWhen_of_reflectsLastAssertion.{u_1,
    u_2}
  {P : PureExpr} {I : ConditionInterp P}
  {Rprefix Rtrace_full :
    Relation (Trace P)}
  {Rout : Relation (Imperative.Env P)}
  {L₁ Lβ‚‚ :
    Strata.Logic.EventLang P (Event P)}
  {T : L₁.StmtT β†’ Option Lβ‚‚.StmtT}
  {pre : L₁.StmtT β†’ Prop}
  {params₁ : L₁.InitEnvWFParamsTy}
  {paramsβ‚‚ : Lβ‚‚.InitEnvWFParamsTy}
  {analyze : Lβ‚‚.StmtT β†’ Bool}
  (hR :
    Trace.ReflectsLastAssertion I Rprefix)
  (hover :
    Specification.Transform.OverapproximatesTraces2UptoWhen
      Rprefix Rtrace_full
      (fun x1 x2 => x1 = x2) Rout L₁ Lβ‚‚ T
      pre params₁ paramsβ‚‚)
  (hprefix :
    βˆ€ (st : L₁.StmtT),
      pre st β†’
        βˆ€ (ρ₀ : Imperative.Env P)
          (cfg : L₁.CfgT)
          (tr : List (Event P))
          (e : Event P)
          (post : List (Event P)),
          L₁.traceStar (L₁.stmtCfg st ρ₀)
              (tr ++ e :: post) cfg β†’
            βˆƒ cfg',
              L₁.traceStar
                (L₁.stmtCfg st ρ₀)
                (tr ++ [e]) cfg')
  (hsound :
    Specification.Analysis.ValidOnTracesVerifier
      Lβ‚‚ I (Lβ‚‚.initEnvWF paramsβ‚‚)
      analyze) :
  Specification.Analysis.ValidOnTracesVerifier
    L₁ I
    (fun s ρ₀ =>
      pre s ∧ L₁.initEnvWF params₁ s ρ₀)
    (Analysis.thenVerify T analyze)

A verifier after a transformation whose prefixes reflect last assertions is sound on the source, from every well-formed entry environment that satisfies the precondition, when the traces of such sources are closed under prefixes ending at an event. The prefix relation need not reflect the validity of whole traces: each source assertion is reflected through the prefix ending at it (Trace.ReflectsLastAssertion). The run relation is not used.

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. It is an instance of overapproximatesTraces2UptoWhen_triple_general, which reads only the run clauses: the run trace relation must reflect the validity of every assertion of a run and carry its reachability forward to a target run whose assertions are valid, and the output environment relation must carry the postcondition back. Its one-relation instance is overapproximatesTracesUptoWhen_triple_general. Inserting the checks of loop invariants needs reachability only on such target runs: an inserted assumption of an invariant holds only where the inserted assertion before it does (Core.InsertLoopInvAsserts.triple_of_blockRel).

πŸ”—theorem
Imperative.Specification.Transform.overapproximatesTraces2UptoWhen_triple_general.{u_1,
    u_2}
  {P : PureExpr} (L₁ Lβ‚‚ : Strata.Logic.EventLang P (Event P))
  (I : ConditionInterp P) {Rtrace : Relation (Trace P)}
  (Rtrace_full : Relation (Trace P))
  (Rin Rout : Relation (Imperative.Env P))
  (T : L₁.StmtT β†’ Option Lβ‚‚.StmtT) (pre : L₁.StmtT β†’ Prop)
  (params₁ : L₁.InitEnvWFParamsTy) (paramsβ‚‚ : Lβ‚‚.InitEnvWFParamsTy)
  (st : L₁.StmtT) (s' : Lβ‚‚.StmtT) (ht : T st = some s')
  (hsem :
    Specification.Transform.OverapproximatesTraces2UptoWhen Rtrace
      Rtrace_full Rin Rout L₁ Lβ‚‚ T pre params₁ paramsβ‚‚)
  {Pre Post : Imperative.Env P β†’ Prop}
  (htriple : Strata.Logic.Hoare.TripleWith Lβ‚‚ I paramsβ‚‚ Pre s' Post)
  (hsource_pre : pre st)
  (hin : βˆ€ (ρ₀ : Imperative.Env P), Pre ρ₀ β†’ Rin ρ₀ ρ₀)
  (hvalid_reflect :
    βˆ€ (sourceTr targetTr : Trace P),
      Rtrace_full sourceTr targetTr β†’
        Trace.AssertionsValid P I targetTr β†’
          Trace.AssertionsValid P I sourceTr)
  (hreach_transfer :
    βˆ€ (sourceTr targetTr : Trace P),
      Rtrace_full sourceTr targetTr β†’
        Trace.AssertionsValid P I targetTr β†’
          Trace.Reachable P I sourceTr β†’ Trace.Reachable P I targetTr)
  (hpost_transport :
    βˆ€ (ρ' ρ'' : Imperative.Env P), Rout ρ' ρ'' β†’ Post ρ'' β†’ Post ρ') :
  Strata.Logic.Hoare.TripleWith L₁ I params₁ Pre st Post
Imperative.Specification.Transform.overapproximatesTraces2UptoWhen_triple_general.{u_1,
    u_2}
  {P : PureExpr}
  (L₁ Lβ‚‚ :
    Strata.Logic.EventLang P (Event P))
  (I : ConditionInterp P)
  {Rtrace : Relation (Trace P)}
  (Rtrace_full : Relation (Trace P))
  (Rin Rout : Relation (Imperative.Env P))
  (T : L₁.StmtT β†’ Option Lβ‚‚.StmtT)
  (pre : L₁.StmtT β†’ Prop)
  (params₁ : L₁.InitEnvWFParamsTy)
  (paramsβ‚‚ : Lβ‚‚.InitEnvWFParamsTy)
  (st : L₁.StmtT) (s' : Lβ‚‚.StmtT)
  (ht : T st = some s')
  (hsem :
    Specification.Transform.OverapproximatesTraces2UptoWhen
      Rtrace Rtrace_full Rin Rout L₁ Lβ‚‚ T
      pre params₁ paramsβ‚‚)
  {Pre Post : Imperative.Env P β†’ Prop}
  (htriple :
    Strata.Logic.Hoare.TripleWith Lβ‚‚ I
      paramsβ‚‚ Pre s' Post)
  (hsource_pre : pre st)
  (hin :
    βˆ€ (ρ₀ : Imperative.Env P),
      Pre ρ₀ β†’ Rin ρ₀ ρ₀)
  (hvalid_reflect :
    βˆ€ (sourceTr targetTr : Trace P),
      Rtrace_full sourceTr targetTr β†’
        Trace.AssertionsValid P I
            targetTr β†’
          Trace.AssertionsValid P I
            sourceTr)
  (hreach_transfer :
    βˆ€ (sourceTr targetTr : Trace P),
      Rtrace_full sourceTr targetTr β†’
        Trace.AssertionsValid P I
            targetTr β†’
          Trace.Reachable P I sourceTr β†’
            Trace.Reachable P I targetTr)
  (hpost_transport :
    βˆ€ (ρ' ρ'' : Imperative.Env P),
      Rout ρ' ρ'' β†’ Post ρ'' β†’ Post ρ') :
  Strata.Logic.Hoare.TripleWith L₁ I
    params₁ Pre st Post

General trace-overapproximation transport for TripleWith. Transports an event-trace Hoare triple from the target Lβ‚‚ back to the source L₁ across an OverapproximatesTraces2UptoWhen with an arbitrary trace relation Rtrace_full for completed runs, input-state relation Rin and output-state relation Rout; its prefix relation Rtrace is not used. The target runs from the source's initial environment, so Rin must relate every environment satisfying the precondition to itself.

The terminal and exiting simulations may return a related target trace and final environment. The compatibility premises connect those witnesses to assertion validity, reachability, and the postcondition; reachability need only transfer to a target trace whose assertions are valid, as the target triple provides.

Strata proves that sequentially chaining multiple transformations is correct (vertical composition). Trace overapproximations compose their trace relations explicitly. OverapproximatesTraces2UptoWhen.rel_comp produces the relational composition of every relation of the stages: the prefix and run trace relations and the input and output environment relations. Its instance OverapproximatesTraces.rel_comp composes the trace relations of stages relating equal environments, while OverapproximatesTraces2UptoWhen.comp_trans_eq and its instance OverapproximatesTracesUptoWhen.comp_trans_eq handle a shared start, accepting stage-specific trace relations and a transitive output state relation.

πŸ”—theorem
Imperative.Specification.Transform.OverapproximatesTraces2UptoWhen.rel_comp.{u_1,
    u_2}
  {P : PureExpr} {EventT : Type u_1}
  {Rtrace₁ Rtraceβ‚‚ Rtrace_full₁ Rtrace_fullβ‚‚ : Relation (List EventT)}
  {Rin₁ Rinβ‚‚ Rout₁ Routβ‚‚ : Relation (Imperative.Env P)}
  {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.OverapproximatesTraces2UptoWhen Rtrace₁
      Rtrace_full₁ Rin₁ Rout₁ L₁ Lβ‚‚ T₁ pre₁ params₁ paramsβ‚‚)
  (hβ‚‚ :
    Specification.Transform.OverapproximatesTraces2UptoWhen Rtraceβ‚‚
      Rtrace_fullβ‚‚ Rinβ‚‚ Routβ‚‚ Lβ‚‚ L₃ Tβ‚‚ preβ‚‚ paramsβ‚‚ params₃) :
  Specification.Transform.OverapproximatesTraces2UptoWhen
    (RComp Rtrace₁ Rtraceβ‚‚) (RComp Rtrace_full₁ Rtrace_fullβ‚‚)
    (RComp Rin₁ Rinβ‚‚) (RComp Rout₁ Routβ‚‚) L₁ L₃ (fun s => T₁ s >>= Tβ‚‚)
    pre₁ params₁ params₃
Imperative.Specification.Transform.OverapproximatesTraces2UptoWhen.rel_comp.{u_1,
    u_2}
  {P : PureExpr} {EventT : Type u_1}
  {Rtrace₁ Rtraceβ‚‚ Rtrace_full₁
    Rtrace_fullβ‚‚ : Relation (List EventT)}
  {Rin₁ Rinβ‚‚ Rout₁ Routβ‚‚ :
    Relation (Imperative.Env P)}
  {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.OverapproximatesTraces2UptoWhen
      Rtrace₁ Rtrace_full₁ Rin₁ Rout₁ L₁
      Lβ‚‚ T₁ pre₁ params₁ paramsβ‚‚)
  (hβ‚‚ :
    Specification.Transform.OverapproximatesTraces2UptoWhen
      Rtraceβ‚‚ Rtrace_fullβ‚‚ Rinβ‚‚ Routβ‚‚ Lβ‚‚
      L₃ Tβ‚‚ preβ‚‚ paramsβ‚‚ params₃) :
  Specification.Transform.OverapproximatesTraces2UptoWhen
    (RComp Rtrace₁ Rtraceβ‚‚)
    (RComp Rtrace_full₁ Rtrace_fullβ‚‚)
    (RComp Rin₁ Rinβ‚‚) (RComp Rout₁ Routβ‚‚)
    L₁ L₃ (fun s => T₁ s >>= Tβ‚‚) pre₁
    params₁ params₃

Trace overapproximations with two trace relations compose by relational composition of every relation: prefix and run trace relations, and input and output environment relations. The first stage's target gate is the second stage's source gate, and the first stage's output meets the second stage's precondition.

πŸ”—theorem
Imperative.Specification.Transform.OverapproximatesTraces.rel_comp.{u_1,
    u_2}
  {P : PureExpr} {EventT : Type u_1} (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.{u_1,
    u_2}
  {P : PureExpr} {EventT : Type u_1}
  (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.OverapproximatesTraces2UptoWhen.comp_trans_eq.{u_1,
    u_2}
  {P : PureExpr} {EventT : Type u_1}
  {Rtrace₁ Rtraceβ‚‚ Rtrace_full₁ Rtrace_fullβ‚‚ : 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.OverapproximatesTraces2UptoWhen Rtrace₁
      Rtrace_full₁ (fun x1 x2 => x1 = x2) Rout L₁ Lβ‚‚ T₁ pre₁ params₁
      paramsβ‚‚)
  (hβ‚‚ :
    Specification.Transform.OverapproximatesTraces2UptoWhen Rtraceβ‚‚
      Rtrace_fullβ‚‚ (fun x1 x2 => x1 = x2) Rout Lβ‚‚ L₃ Tβ‚‚ preβ‚‚ paramsβ‚‚
      params₃) :
  Specification.Transform.OverapproximatesTraces2UptoWhen
    (RComp Rtrace₁ Rtraceβ‚‚) (RComp Rtrace_full₁ Rtrace_fullβ‚‚)
    (fun x1 x2 => x1 = x2) Rout L₁ L₃ (fun s => T₁ s >>= Tβ‚‚) pre₁
    params₁ params₃
Imperative.Specification.Transform.OverapproximatesTraces2UptoWhen.comp_trans_eq.{u_1,
    u_2}
  {P : PureExpr} {EventT : Type u_1}
  {Rtrace₁ Rtraceβ‚‚ Rtrace_full₁
    Rtrace_fullβ‚‚ : 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.OverapproximatesTraces2UptoWhen
      Rtrace₁ Rtrace_full₁
      (fun x1 x2 => x1 = x2) Rout L₁ Lβ‚‚ T₁
      pre₁ params₁ paramsβ‚‚)
  (hβ‚‚ :
    Specification.Transform.OverapproximatesTraces2UptoWhen
      Rtraceβ‚‚ Rtrace_fullβ‚‚
      (fun x1 x2 => x1 = x2) Rout Lβ‚‚ L₃ Tβ‚‚
      preβ‚‚ paramsβ‚‚ params₃) :
  Specification.Transform.OverapproximatesTraces2UptoWhen
    (RComp Rtrace₁ Rtraceβ‚‚)
    (RComp Rtrace_full₁ Rtrace_fullβ‚‚)
    (fun x1 x2 => x1 = x2) Rout L₁ L₃
    (fun s => T₁ s >>= Tβ‚‚) pre₁ params₁
    params₃

Shared-start composition for trace overapproximations with two trace relations, stage- specific trace relations and a transitive output relation: rel_comp with the composed equalities and output relations collapsed.

πŸ”—theorem
Imperative.Specification.Transform.OverapproximatesTracesUptoWhen.comp_trans_eq.{u_1,
    u_2}
  {P : PureExpr} {EventT : Type u_1}
  (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.{u_1,
    u_2}
  {P : PureExpr} {EventT : Type u_1}
  (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): overapproximatesTraces2UptoWhen_stmts lifts a per-statement trace overapproximation to the whole block (fun ss => ss.mapM T). It requires the trace relations to relate empty traces and respect chronological append; since a prefix of a list is a completed run of its first statements followed by a prefix of the next one, the prefix relation must extend on the left by traces related by the run relation. Its instance overapproximatesTraces_stmts needs one trace relation relating empty traces and respecting append. Like the Hoare rules above, it carries 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.

πŸ”—theorem
Imperative.Specification.Transform.overapproximatesTraces2UptoWhen_stmts.{u_1,
    u_2}
  {P : PureExpr} [HasFvar P] [HasFvars P] [HasBool P] [HasBoolOps P]
  [HasSubstFvar P] [HasInt P] [HasIntOps P] {CmdT : Type}
  {EventT : Type u_1} (evalCmdE : EvalCmdParamE P CmdT EventT)
  (Rtrace Rtrace_full : Relation (List EventT)) (hnil : Rtrace [] [])
  (hnil_full : Rtrace_full [] [])
  (happend :
    βˆ€ (a a' b b' : List EventT),
      Rtrace_full a a' β†’ Rtrace b b' β†’ Rtrace (a ++ b) (a' ++ b'))
  (happend_full :
    βˆ€ (a a' b b' : List EventT),
      Rtrace_full a a' β†’
        Rtrace_full b b' β†’ Rtrace_full (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 (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.OverapproximatesTraces2UptoWhen Rtrace
      Rtrace_full (fun x1 x2 => x1 = x2) (fun x1 x2 => x1 = x2)
      (Logic.EventLang.imperativeE P CmdT evalCmdE SParams swf)
      (Logic.EventLang.imperativeE P CmdT evalCmdE SParams swf) T
      (fun x => True) sp₁ spβ‚‚) :
  Specification.Transform.OverapproximatesTraces2UptoWhen Rtrace
    Rtrace_full (fun x1 x2 => x1 = x2) (fun x1 x2 => x1 = x2)
    (Logic.EventLang.imperativeBlockE P CmdT evalCmdE ⟨Params, wf⟩)
    (Logic.EventLang.imperativeBlockE P CmdT evalCmdE ⟨Params, wf⟩)
    (fun ss => List.mapM T ss) (fun x => True) p₁ pβ‚‚
Imperative.Specification.Transform.overapproximatesTraces2UptoWhen_stmts.{u_1,
    u_2}
  {P : PureExpr} [HasFvar P] [HasFvars P]
  [HasBool P] [HasBoolOps P]
  [HasSubstFvar P] [HasInt P]
  [HasIntOps P] {CmdT : Type}
  {EventT : Type u_1}
  (evalCmdE : EvalCmdParamE P CmdT EventT)
  (Rtrace Rtrace_full :
    Relation (List EventT))
  (hnil : Rtrace [] [])
  (hnil_full : Rtrace_full [] [])
  (happend :
    βˆ€ (a a' b b' : List EventT),
      Rtrace_full a a' β†’
        Rtrace b b' β†’
          Rtrace (a ++ b) (a' ++ b'))
  (happend_full :
    βˆ€ (a a' b b' : List EventT),
      Rtrace_full a a' β†’
        Rtrace_full b b' β†’
          Rtrace_full (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
            (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.OverapproximatesTraces2UptoWhen
      Rtrace Rtrace_full
      (fun x1 x2 => x1 = x2)
      (fun x1 x2 => x1 = x2)
      (Logic.EventLang.imperativeE P CmdT
        evalCmdE SParams swf)
      (Logic.EventLang.imperativeE P CmdT
        evalCmdE SParams swf)
      T (fun x => True) sp₁ spβ‚‚) :
  Specification.Transform.OverapproximatesTraces2UptoWhen
    Rtrace Rtrace_full
    (fun x1 x2 => x1 = x2)
    (fun x1 x2 => x1 = x2)
    (Logic.EventLang.imperativeBlockE P
      CmdT evalCmdE ⟨Params, wf⟩)
    (Logic.EventLang.imperativeBlockE P
      CmdT evalCmdE ⟨Params, wf⟩)
    (fun ss => List.mapM T ss)
    (fun x => True) p₁ pβ‚‚

Lift a per-statement trace overapproximation with two trace relations to whole statement lists. It simulates every finite source prefix and every terminal/exiting run. 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). Both trace relations relate empty traces (hnil, hnil_full); the run relation Rtrace_full is closed under concatenation (happend_full), and the prefix relation Rtrace extends on the left by traces of completed runs related by Rtrace_full (happend): a prefix of a list is a completed run of its first statements followed by a prefix of the next one.

πŸ”—theorem
Imperative.Specification.Transform.overapproximatesTraces_stmts.{u_1,
    u_2}
  {P : PureExpr} [HasFvar P] [HasFvars P] [HasBool P] [HasBoolOps P]
  [HasSubstFvar P] [HasInt P] [HasIntOps P] {CmdT : Type}
  {EventT : Type u_1} (evalCmdE : EvalCmdParamE P CmdT EventT)
  (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 (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 SParams swf)
      (Logic.EventLang.imperativeE P CmdT evalCmdE SParams swf) T sp₁
      spβ‚‚) :
  Specification.Transform.OverapproximatesTraces Rtrace
    (Logic.EventLang.imperativeBlockE P CmdT evalCmdE ⟨Params, wf⟩)
    (Logic.EventLang.imperativeBlockE P CmdT evalCmdE ⟨Params, wf⟩)
    (fun ss => List.mapM T ss) p₁ pβ‚‚
Imperative.Specification.Transform.overapproximatesTraces_stmts.{u_1,
    u_2}
  {P : PureExpr} [HasFvar P] [HasFvars P]
  [HasBool P] [HasBoolOps P]
  [HasSubstFvar P] [HasInt P]
  [HasIntOps P] {CmdT : Type}
  {EventT : Type u_1}
  (evalCmdE : EvalCmdParamE P CmdT EventT)
  (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
            (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 SParams swf)
      (Logic.EventLang.imperativeE P CmdT
        evalCmdE SParams swf)
      T sp₁ spβ‚‚) :
  Specification.Transform.OverapproximatesTraces
    Rtrace
    (Logic.EventLang.imperativeBlockE P
      CmdT evalCmdE ⟨Params, wf⟩)
    (Logic.EventLang.imperativeBlockE P
      CmdT evalCmdE ⟨Params, wf⟩)
    (fun ss => List.mapM T ss) p₁ pβ‚‚

Lift a per-statement trace overapproximation to whole statement lists. It simulates every finite source prefix and every terminal/exiting run. 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 (overapproximatesTraces2UptoWhen_stmts with one trace relation).