Crate mikino_api
source · [−]Expand description
A minimal (1-)induction library.
Mikino has a binary crate and a companion tutorial/introduction to formal verification, Verification for Dummies: SMT and Induction. While it discusses mikino mainly from the (binary-side) end-user point of view, it will be pretty useful to users of the mikino API unfamiliar with (SMT-based) formal verification.
This crate deals with two main objects: hsmt scripts and hsmt (transition)
systems, where hsmt stands for Human SMT-LIB 2.
Mikino has the ability to run scripts, and (dis)prove properties over transition systems using
k
-induction. Both features are realized using SMT solvers, see the solver
module for more.
Mikino only handles relatively simple SMT-LIB 2 expressions where the only types are bool
,
int
and rat
. For details regarding the expression structures see expr
.
Also, note that you will find a bunch of examples in repository/examples
which use the
systems/scripts in repository/rsc
.
Scripts
An hsmt script is a Rust-flavored SMT-LIB 2 script, with a twist. The twist is that check
sat results are meta-values that users can store in meta-variables with let is_sat = check_sat!()
. Users can then branch on check sat results using if-then-else
s. For more,
see
SCRIPT_DEMO
for a description of mikino’s syntax for hsmt scripts;parse::script
for parsing scripts;script
for running scripts;repository/rsc/script_demo.rs
for a documented hsmt script demo.
Transition Systems
An hsmt transition system is a declarative transition system specified with three objects:
- the system’s state variables, which define the notion of state for the system as a valuation of all the state variables.
- the system’s initial predicate or
init
, which is a predicate over the state variables (a function from a state of the system tobool
);init
defines the legal initial states of the system as the states for whichinit(state) = true
. - the system’s transition predicate or
trans
, which is a predicate over two statesstate
andstate'
;trans
defines the states that legally follow any statestate
as all the statesstate'
such thattrans(state, state') = true
.
For more, see
TRANS_DEMO
for a description of mikino’s syntax for hsmt systems;parse::trans
for parsing hsmt systems;trans
for how hsmt systems are structured;check
for hsmt systemk
-induction-based verification;repository/rsc/trans_demo.rs
for a documented hsmt system demo.
Re-exports
pub extern crate rsmt2;
Modules
AST structures for expressions and scripts.
Types and helpers to check a transition system.
Error-handling.
Defines the expression structure used to represent predicates.
Backend parser (SMT-LIB) and frontend parser (requires the parser
feature).
Common imports throughout this project.
HSmt 2 scripts.
Provides parser-equipped rsmt2::Solver
s.
Transition system structures and helpers.
Macros
Builds some declarations.
Convenience macro, provides a DSL for writing expressions.
Builds a transition system.
Builds an expression.
Builds a type.
Imports mikino’s prelude.
Converts a crate::prelude::Res
in a crate::prelude::PRes
.
Constants
String representation of a simple demo script.
String representation of a simple demo system.