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-elses. 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 to bool); init defines the legal initial states of the system as the states for which init(state) = true.
  • the system’s transition predicate or trans, which is a predicate over two states state and state'; trans defines the states that legally follow any state state as all the states state' such that trans(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 system k-induction-based verification;
  • repository/rsc/trans_demo.rs for a documented hsmt system demo.

Re-exports§

pub extern crate rsmt2;

Modules§

ast
AST structures for expressions and scripts.
check
Types and helpers to check a transition system.
err
Error-handling.
expr
Defines the expression structure used to represent predicates.
parse
Backend parser (SMT-LIB) and frontend parser (requires the parser feature).
prelude
Common imports throughout this project.
script
HSmt 2 scripts.
solver
Provides parser-equipped rsmt2::Solvers.
trans
Transition system structures and helpers.

Macros§

build_decls
Builds some declarations.
build_expr
Convenience macro, provides a DSL for writing expressions.
build_trans
Builds a transition system.
build_trans_expr
Builds an expression.
build_typ
Builds a type.
prelude
Imports mikino’s prelude.
try_to_pres
Converts a crate::prelude::Res in a crate::prelude::PRes.

Constants§

SCRIPT_DEMO
String representation of a simple demo script.
TRANS_DEMO
String representation of a simple demo system.