Transition systems and bounded model checking, typed

A Sys is a transition system over a symbol structure of state variables (see structure.symbols): an initial predicate, a transition relation between a state and the next, and named candidate invariants. Sys.Bmc checks the candidates on runs of increasing length.

Sys.Bmc.mk sys starts at step 0. check looks for a run whose state at the current step falsifies some remaining candidates: it answers their names and the checker without them, the counterexample recorded in falsified, or none once no remaining candidate can be falsified at this step. unroll then moves to the next step.

@[reducible, inline]

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

Named candidate invariants: predicates over the state variables, at any step.

Equations

• Cvc.Typed.Symbols.Sig.Candidates = Array (String × SVars.PredAt')

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

One value per step, from step k down to step 0: an α i at step i.

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

def Cvc.Typed.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 to step k.

Equations

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

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

The value at step k, the last one.

Equations

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

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

The value at step 0.

Equations

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

@[reducible, inline]

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

A trace of unrolled Term-symbols.

Equations

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

@[reducible, inline]

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

A trace of Lean-values for some unrolled symbols.

Equations

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

@[reducible, inline]

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

A trace of Term-values for some unrolled symbols.

Equations

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

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

Extracts the Lean-values of a TermTrace.

Equations

• Cvc.Typed.Symbols.Sig.ValueTrace.extract (Cvc.Typed.Sys.Trace.zero terms) = Cvc.Typed.Sys.Trace.zero <$> terms.getValues s
• Cvc.Typed.Symbols.Sig.ValueTrace.extract (Cvc.Typed.Sys.Trace.cons terms tl) = do let values ← terms.getValues s Cvc.Typed.Sys.Trace.cons values <$> Cvc.Typed.Symbols.Sig.ValueTrace.extract tl

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

Extracts the Lean-values of a TermTrace.

Equations

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

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

Extracts the Lean-values of a TermTrace.

Equations

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

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

Extracts the Term-values of a TermTrace.

Equations

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

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

Extracts the Term-values of a TermTrace.

Equations

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

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

Extracts the Term-values of a TermTrace.

Equations

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

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

A transition system over the state variables SVars, with candidate invariants to check.

• idents : SVars.Idents

  State variable identifiers.

• init : SVars.PredAt'

  Initial predicate over SVars.

• next : SVars.RelAt'

  Transition relation over SVars.

• candidates : Symbols.Sig.Candidates

  Candidate properties over the system.

@[reducible, inline]

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

Sys SVars, written SVars.Sys.

Equations

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

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

Declares step k's state variables in solver, and answers the initial predicate on them.

Equations

• Cvc.Typed.Sys.initAt sys solver k = do let svs_k ← Cvc.Typed.Solver.declareSymbolsAt k solver sys.idents sys.init svs_k

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

The transition relation from the state curr to the state next.

Equations

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

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

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

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

  The system's state variables.

• next {k k' : Nat} : SVars.TermsAt k → SVars.TermsAt k' → Env (Term Bool)

  The transition relation, at this scope.

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

  The candidate invariants not falsified yet, at this scope.

• solver : Solver

  The solver the steps are 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, latest first: each one's step, trace and falsified candidates.

• )

@[reducible, inline]

abbrev Cvc.Typed.Symbols.Sig.Bmc [Ω] (SVars : Sig) [Symbols SVars] (k : Nat) : Type

Sys.Bmc SVars k, written SVars.Bmc k.

Equations

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

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

A checker for sys at step 0, on a new solver asserting the initial predicate.

Equations

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

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

Whether every candidate has been falsified.

Equations

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

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

Looks for a run whose state at the current step falsifies some remaining candidates.

Answers their names and the checker without them, the counterexample added to falsified, or none if no remaining candidate can be falsified at this step. Call it until it answers none.

Equations

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

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

Moves to the next step: declares its state variables and asserts the transition into it.

Equations

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