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.