Transition systems and bounded model checking, sort-erased

A Sys is a transition system over a symbol structure: an initial predicate, a transition relation and named candidate invariants, each a function of the symbols at one step or two.

Sys.Bmc checks the candidates by bounded model checking. Bmc.mk starts at step 0; check answers the candidates some run reaching the current step falsifies, and is called again until it answers none; unroll then moves to the next step. isDone holds once no candidate is left.

@[reducible, inline]

abbrev Cvc.Untyped.Symbols.Sig.Candidates [Ω] {SVars : Sig} [Symbols SVars] : Type

An array of named predicates over SVars.

Equations

• Cvc.Untyped.Symbols.Sig.Candidates = Array (String × SVars.FunAt')

inductive Cvc.Untyped.Sys.Trace (α : Nat → Type) (k : Nat) : Type

One value per step from 0 to k, the latest first.

• zero {α : Nat → Type} : α 0 → Trace α 0
• cons {α : Nat → Type} {k : Nat} : α (k + 1) → Trace α k → Trace α (k + 1)

def Cvc.Untyped.Sys.Trace.iterM {m : Type → Type u_1} {α : Nat → Type} {k : Nat} [Monad m] (f : {k : Nat} → α k → m Unit) : Trace α k → m Unit

Runs f on each step's value, from step 0 up.

Equations

• Cvc.Untyped.Sys.Trace.iterM f (Cvc.Untyped.Sys.Trace.zero val) = f val
• Cvc.Untyped.Sys.Trace.iterM f (Cvc.Untyped.Sys.Trace.cons val tl) = do Cvc.Untyped.Sys.Trace.iterM (fun {k : Nat} => f) tl f val

def Cvc.Untyped.Sys.Trace.getCurrent {α : Nat → Type} {k : Nat} : Trace α k → α k

The value at the latest step, k.

Equations

• (Cvc.Untyped.Sys.Trace.zero val).getCurrent = val
• (Cvc.Untyped.Sys.Trace.cons val tl).getCurrent = val

def Cvc.Untyped.Sys.Trace.getZero {α : Nat → Type} {k : Nat} : Trace α k → α 0

The value at step 0.

Equations

• (Cvc.Untyped.Sys.Trace.zero val).getZero = val
• (Cvc.Untyped.Sys.Trace.cons val tl).getZero = tl.getZero

@[reducible, inline]

abbrev Cvc.Untyped.Symbols.Sig.TermTrace {SVars : Sig} [Ω] (k : Nat) : Type

The symbols of each step, as terms.

Equations

• Cvc.Untyped.Symbols.TermTrace = Cvc.Untyped.Sys.Trace SVars.TermsAt

@[reducible, inline]

abbrev Cvc.Untyped.Symbols.Sig.ValueTrace {SVars : Sig} (k : Nat) : Type

The values of each step's symbols, as Lean values.

Equations

• Cvc.Untyped.Symbols.ValueTrace = Cvc.Untyped.Sys.Trace SVars.ValuesAt

@[reducible, inline]

abbrev Cvc.Untyped.Symbols.Sig.ValueTermTrace {SVars : Sig} [Ω] (k : Nat) : Type

The values of each step's symbols, as terms.

Equations

• Cvc.Untyped.Symbols.ValueTermTrace = Cvc.Untyped.Sys.Trace SVars.ValueTermsAt

def Cvc.Untyped.Symbols.Sig.ValueTrace.extract {SVars : Sig} [Ω] [Symbols SVars] {k : Nat} {s : Solver} : TermTrace k → s.EnvSat (ValueTrace k)

The values the model gives a TermTrace, as Lean values.

Equations

• One or more equations did not get rendered due to their size.
• Cvc.Untyped.Symbols.Sig.ValueTrace.extract (Cvc.Untyped.Sys.Trace.zero terms) = Cvc.Untyped.Sys.Trace.zero <$> terms.getValues s

def Cvc.Untyped.Symbols.Sig.TermTrace.getValues {SVars : Sig} [Ω] [Symbols SVars] {k : Nat} {s : Solver} : TermTrace k → s.EnvSat (ValueTrace k)

The values the model gives a TermTrace, as Lean values.

Equations

• @Cvc.Untyped.Symbols.Sig.TermTrace.getValues = @Cvc.Untyped.Symbols.Sig.ValueTrace.extract

def Cvc.Untyped.Symbols.Sig.TermTrace.getCex {SVars : Sig} [Ω] [Symbols SVars] {k : Nat} {s : Solver} : TermTrace k → s.EnvSat (ValueTrace k)

The values the model gives a TermTrace, as Lean values.

Equations

• @Cvc.Untyped.Symbols.Sig.TermTrace.getCex = @Cvc.Untyped.Symbols.Sig.TermTrace.getValues

def Cvc.Untyped.Symbols.Sig.ValueTermTrace.extract {SVars : Sig} [Ω] [Symbols SVars] {k : Nat} {s : Solver} : TermTrace k → s.EnvSat (ValueTermTrace k)

The values the model gives a TermTrace, as terms.

Equations

• One or more equations did not get rendered due to their size.
• Cvc.Untyped.Symbols.Sig.ValueTermTrace.extract (Cvc.Untyped.Sys.Trace.zero terms) = Cvc.Untyped.Sys.Trace.zero <$> terms.getValueTerms s

def Cvc.Untyped.Symbols.Sig.TermTrace.getValueTerms {SVars : Sig} [Ω] [Symbols SVars] {k : Nat} {s : Solver} : TermTrace k → s.EnvSat (ValueTermTrace k)

The values the model gives a TermTrace, as terms.

Equations

• @Cvc.Untyped.Symbols.Sig.TermTrace.getValueTerms = @Cvc.Untyped.Symbols.Sig.ValueTermTrace.extract

def Cvc.Untyped.Symbols.Sig.TermTrace.getTermCex {SVars : Sig} [Ω] [Symbols SVars] {k : Nat} {s : Solver} : TermTrace k → s.EnvSat (ValueTermTrace k)

The values the model gives a TermTrace, as terms.

Equations

• @Cvc.Untyped.Symbols.Sig.TermTrace.getTermCex = @Cvc.Untyped.Symbols.Sig.TermTrace.getValueTerms

structure Cvc.Untyped.Sys [Ω] (SVars : Symbols.Sig) [Symbols SVars] : Type

A transition system over the symbol structure SVars.

• idents : SVars.Idents

  The state variables' identifiers.

• init : SVars.FunAt'

  The initial predicate.

• next : SVars.Fun2At'

  The transition relation, from one step to the next.

• candidates : Symbols.Sig.Candidates

  The candidate invariants, by name.

@[reducible, inline]

abbrev Cvc.Untyped.Symbols.Sys [Ω] (SVars : Sig) [Symbols SVars] : Type

A transition system over the symbol structure SVars.

Equations

• @Cvc.Untyped.Symbols.Sys = @Cvc.Untyped.Sys

@[reducible, inline]

abbrev Cvc.Untyped.Symbols.Sig.Sys [Ω] (SVars : Sig) [Symbols SVars] : Type

A transition system over the symbol structure SVars.

Equations

• @Cvc.Untyped.Symbols.Sig.Sys = @Cvc.Untyped.Sys

def Cvc.Untyped.Sys.initAt {SVars : Symbols.Sig} [Ω] [Symbols SVars] (sys : SVars.Sys) (solver : Solver) (k : Nat) : Env Term

Declares the symbols of step k in solver, and builds the initial predicate over them.

Equations

• Cvc.Untyped.Sys.initAt sys solver k = Cvc.Untyped.Solver.declareSymbolsAt k solver sys.idents >>= sys.init

def Cvc.Untyped.Sys.nextAt {SVars : Symbols.Sig} [Ω] [Symbols SVars] (sys : SVars.Sys) {k k' : Nat} (curr : SVars.TermsAt k) (next : SVars.TermsAt k') : Env Term

The transition predicate from step k to step k', over symbols already declared.

Equations

• Cvc.Untyped.Sys.nextAt sys curr next = sys.next curr next

structure Cvc.Untyped.Sys.Bmc [Ω] (SV : Symbols.Sig) [Symbols SV] (k : Nat) : Type

Bounded model checking of a system, unrolled to step k.

• mk' :: (
• idents : SV.Idents

  The system's state variables.

• next {k k' : Nat} : SV.TermsAt k → SV.TermsAt k' → Env Term

  The transition relation.

• candidates : Array (String × ({k : Nat} → SV.TermsAt k → Env Term))

  The candidate invariants not falsified yet.

• solver : Solver

  The solver the unrolling is asserted in.

• sVars : Symbols.TermTrace k

  The state variables of every step so far.

• falsified : List ((k : Nat) × Symbols.ValueTrace k × Array String)

  The counterexamples found, the latest first.

  Each holds its step, its trace, and the candidates it falsified.

• )

@[reducible, inline]

abbrev Cvc.Untyped.Symbols.Bmc [Ω] (SV : Sig) [Symbols SV] (k : Nat) : Type

Bounded model checking of a system, unrolled to step k.

Equations

• @Cvc.Untyped.Symbols.Bmc = @Cvc.Untyped.Sys.Bmc

@[reducible, inline]

abbrev Cvc.Untyped.Symbols.Sig.Bmc [Ω] (SV : Sig) [Symbols SV] (k : Nat) : Type

Bounded model checking of a system, unrolled to step k.

Equations

• @Cvc.Untyped.Symbols.Sig.Bmc = @Cvc.Untyped.Sys.Bmc

def Cvc.Untyped.Sys.Bmc.mk {SVars : Symbols.Sig} [Ω] [Symbols SVars] (sys : SVars.Sys) : Env (SVars.Bmc 0)

Starts checking sys at step 0, in a solver of its own.

Equations

• One or more equations did not get rendered due to their size.

def Cvc.Untyped.Sys.Bmc.isDone {SVars : Symbols.Sig} [Ω] [Symbols SVars] {k : Nat} (bmc : SVars.Bmc k) : Bool

Whether every candidate has been falsified.

Equations

• Cvc.Untyped.Sys.Bmc.isDone bmc = bmc.candidates.isEmpty

def Cvc.Untyped.Sys.Bmc.check {SVars : Symbols.Sig} [Ω] [Symbols SVars] {k : Nat} (bmc : SVars.Bmc k) : Env (Option (Array String × SVars.Bmc k))

The candidates some run reaching step k falsifies, and the checker without them.

The counterexample is recorded in falsified. Answers none when no candidate left is falsified at this step, and fails if the solver gives up.

Equations

• One or more equations did not get rendered due to their size.

def Cvc.Untyped.Sys.Bmc.unroll {SVars : Symbols.Sig} [Ω] [Symbols SVars] {k : Nat} (bmc : SVars.Bmc k) : Env (SVars.Bmc k.succ)

Moves to step k + 1, asserting the transition to it.

Equations

• One or more equations did not get rendered due to their size.