deductive verification of Rust code. (semi) automatically prove your code satisfies your specifications!

Xavier Denis

Last update: Dec 28, 2022

Related tags

Cryptography proof verification rust-lang formal-verification deductive-reasoning why3

Overview

Le marteau-pilon, forges et aciéries de Saint-Chamond, Joseph-Fortuné LAYRAUD, 1889

About

Creusot is a tool for deductive verification of Rust code. It allows you to annotate your code with specifications, invariants and assertions and then check them formally, returning a proof your code satisfies its specification.

Creusot works by translating Rust code to WhyML the verification and specification language of . Users can then leverage the full power of Why3 to (semi)-automatically discharge the verification conditions!

Note: ⚠️ I am developping this in the context of my PhD thesis, the software quality is commensurate. ⚠️

Example programs that have been proven:

Installing

Install Rust using rustup to manage toolchains
Clone the repository
Install the Rust compiler libraries: rustup component add rustc-dev
(Optional, Recommended) Install the Rust compiler sources: rustup component add rustc-src
Run cargo build

Generating MLCFG outputs

cargo run -- path/to/file.rs

Creusot will translate the code in this file and its dependencies, producing a file in a language called MLCFG. By default it prints this to standard out but an output file can be specified with -o.

Proving programs with Why3

To actually prove programs using Why3, you will need to use a branch I am currently developing that includes the relevant support. You can find this branch here: https://gitlab.inria.fr/why3/why3/-/tree/stackify. I hope to have this branch integrated and released by 1.5.0 (though ideally earlier).

With this version of Why3, you can load your generated MLCFG in the IDE by running

why3 ide path/to/file.mlcfg

From there standard proof strategies should work. I would like to improve this part of the user experience, but that will have to wait until Creusot is more stable and complete.

Writing specifications

Currently, writing specifications with Creusot requires a little bit of tedium. You will need to include the creusot-contracts crate in your project. However, since this crate is not published you will need to either load it as an extern crate or include a local copy in your Cargo.toml.

Loading as an extern crate

To include creusot-contracts as an extern crate, add the appropriate declaration to your Rust file,

extern crate creusot_contracts;
use creusot_contracts::*;

Then compile your code and add creusot-contracts to the loadpath using the -L flag like so: cargo build -L path/to/directory/with/creusot-contracts.

⚠️ Currently creusot-contracts is very unfinished, using the macros included in this crate may prevent your Rust code from compiling normally, I still need to implement a pass-through mode for normal compilation. ⚠️

Kinds of contract expressions

Currently Creusot uses 4 different kinds of contract expressions. The most basic are requires and ensures which can be attached to a Rust function declaration like so:

#[requires(R)]
#[ensures(E)]
fn my_function(b: u32) -> bool { .. }

You can attach as many ensures and requires clauses as you would like, in any order.

Inside a function, you can attach invariant clauses to loops, these are attached on top of the loop rather than inside, that is:

#[invariant(name, E)]
while true {}

Invariants must have names (for now).

Finally, there is a variant expression which may be useful when defining logical functions where it is required to prove termination. You can give it an expression as argument, that expression must form a well-founded order which strictly decreases at each recursive call.

Pearlite

Contracts and logic functions are written in Pearlite, a specification language for Rust I am developing. Pearlite can be seen as a pure, immutable fragment of Rust which has access to a few additional logical operations and connectors. In practice you have:

Base Rust expressions: matching, function calls, let bindings, binary and unary operators, tuples, structs and enums, projections, primitive casts, and dereferencing.
Logical Expressions: quantifiers (forall and exists), logical implication ->, logical equality ≡ /===, labels
Rust specific logical expressions: Access to the final value of a mutable borrow! ^ /@fin

You also have two new kinds of declarations: logic and hybrid

When a function is annotated with logic, its body will be treated as a pearlite expression, this means that you can use quantifiers, have access to final values of borrows and all the goodies. However, you cannot call this function in normal Rust code, currently this is enforced by replacing the body with a panic!.

The second kind of declaration hybrid (not yet implemented), allows you to mark a Rust function as both a logic function and a program function. This means your code must lie in the intersection of these languages. In particular this means no mutation of any kind (even recursively) and no quantifiers or logic specific constructs.

Comments

Introduce the `Model` trait and add the `@` notation

Introduce the Model trait and add the @ notation, as mentioned in the recent comments of #63. I think this provides a really good interface for handling models.

opened by shiatsumat 36
Add `Model` instances for references and integers

This PR adds and uses Model instances for &T and integer types, which closes #128. I decided not to add an instance for &mut T, to keep symmetry between @*x and @^x.

opened by shiatsumat 30

internal compiler error

+  0 ┊ error: internal compiler error: compiler/rustc_middle/src/ty/subst.rs:634:17: type parameter `A/#2` (A/2) out of range when substituting, substs=[<K as creusot_contracts::Model>::ModelTy, std::option::Option<V>]
+  1 ┊ 
+  2 ┊ thread 'rustc' panicked at 'Box<dyn Any>', /rustc/34a6c9f26e2ce32cad0d71f5e342365b09f4d12c/compiler/rustc_errors/src/lib.rs:1289:9
+  3 ┊ note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
+  4 ┊ 
+  5 ┊ note: Creusot has panic-ed!
+  6 ┊   |
+  7 ┊   = note: Oops, that shouldn't have happened, sorry about that.
+  8 ┊   = note: Please report this bug over here: https://github.com/xldenis/creusot/issues/new
+  9 ┊ 
+ 10 ┊ error: aborting due to previous error
+ 11 ┊ 
thread 'main' panicked at '1 failures out of 140 tests', creusot/tests/ui.rs:149:9
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

When trying to use Creusot on the following :+1:

#![feature(box_patterns)]
extern crate creusot_contracts;

use creusot_contracts::std::*;
use creusot_contracts::*;
use std::cmp::Ord;
use std::cmp::Ordering::*;

extern_spec! {
    #[ensures(result === (@self_).cmp_log(@*o))]
    fn std::cmp::Ord::cmp<Self_>(self_: &Self_, o: &Self_) -> Ordering
        where Self_: Ord + Model,
              Self_::ModelTy: OrdLogic
}

#[derive(Clone, Copy)]
enum Color {
    Red,
    Black,
}
use Color::*;

struct Node<K, V> {
    left: Tree<K, V>,
    color: Color,
    key: K,
    val: V,
    right: Tree<K, V>,
}

struct Tree<K, V> {
    node: Option<Box<Node<K, V>>>,
}

/*************  The model of a tree, and the set of its mappings  *************/

impl<K: Model, V> Tree<K, V> {
    #[predicate]
    fn has_mapping(self, k: K::ModelTy, v: V) -> bool {
        pearlite! {
            match self {
                Tree { node: None } => false,
                Tree { node: Some(box Node { left, color, key, val, right }) } =>
                    left.has_mapping(k, v) || right.has_mapping(k, v) || k === @key && v === val
            }
        }
    }

    #[predicate]
    fn same_mappings(self, o: Self) -> bool {
        pearlite! {
            forall<k: K::ModelTy, v: V> self.has_mapping(k, v) === o.has_mapping(k, v)
        }
    }

    #[logic]
    fn model_acc(self, accu: <Self as Model>::ModelTy) -> <Self as Model>::ModelTy {
        pearlite! {
            match self {
                Tree { node: None } => accu,
                Tree { node: Some(box Node { left, color, key, val, right }) } => {
                    let accu1 = left.model_acc(accu);
                    let accu2 = accu1.set(@key, Some(val));
                    right.model_acc(accu2)
                }
            }
        }
    }

    #[logic]
    #[ensures(self.model_acc(accu).get(k) === accu.get(k) ||
              exists<v: V> self.model_acc(accu).get(k) === Some(v) && self.has_mapping(k, v))]
    fn model_acc_has_binding(self, accu: <Self as Model>::ModelTy, k: K::ModelTy) {
        pearlite! {
            match self {
                Tree { node: None } => (),
                Tree { node: Some(box Node { left, color, key, val, right }) } => {
                    left.model_acc_has_binding(accu, k);
                    let accu1 = left.model_acc(accu);
                    let accu2 = accu1.set(@key, Some(val));
                    right.model_acc_has_binding(accu2, k)
                }
            }
        }
    }

    #[logic]
    #[requires(self.bst_invariant())]
    #[ensures(forall<v: V> self.has_mapping(k, v) ==> self.model_acc(accu).get(k) === Some(v))]
    fn has_binding_model_acc(self, accu: <Self as Model>::ModelTy, k: K::ModelTy)
    where
        K::ModelTy: OrdLogic,
    {
        pearlite! {
            match self {
                Tree { node: None } => (),
                Tree { node: Some(box Node { left, color, key, val, right }) } => {
                    left.has_binding_model_acc(accu, k);
                    let accu1 = left.model_acc(accu);
                    let accu2 = accu1.set(@key, Some(val));
                    right.has_binding_model_acc(accu2, k);
                    right.model_acc_has_binding(accu2, k)
                }
            }
        }
    }

    #[logic]
    #[requires(self.bst_invariant())]
    #[ensures(self.has_mapping(k, v) === ((@self).get(k) === Some(v)))]
    fn has_binding_model(self, k: K::ModelTy, v: V)
    where
        K::ModelTy: OrdLogic,
    {
        pearlite! { {
            self.model_acc_has_binding(Mapping::cst(None), k);
            self.has_binding_model_acc(Mapping::cst(None), k)
        } }
    }
}

impl<K: Model, V> Node<K, V> {
    #[predicate]
    fn same_mappings(self, o: Self) -> bool {
        pearlite! {
            forall<st: Tree<K, V>, ot: Tree<K, V>>
                (match st { Tree { node: Some(x) } => self === *x, _ => false }) &&
                (match ot { Tree { node: Some(x) } => o === *x, _ => false }) ==>
                st.same_mappings(ot)
        }
    }
}

impl<K: Model, V> Model for Node<K, V> {
    type ModelTy = Mapping<K::ModelTy, Option<V>>;

    #[logic]
    fn model(self) -> Self::ModelTy {
        pearlite! {
            self.right.model_acc(self.left.model().set(@self.key, Some(self.val)))
        }
    }
}

impl<K: Model, V> Model for Tree<K, V> {
    type ModelTy = Mapping<K::ModelTy, Option<V>>;

    #[logic]
    fn model(self) -> Self::ModelTy {
        pearlite! { self.model_acc(Mapping::cst(None)) }
    }
}

/*******************************  The BST invariant ***************************/

impl<K: Model, V> Node<K, V>
where
    K::ModelTy: OrdLogic,
{
    #[predicate]
    fn bst_invariant_here(self) -> bool {
        pearlite! {
            (forall<k: K::ModelTy, v: V> self.left.has_mapping(k, v) ==> k < @self.key) &&
            (forall<k: K::ModelTy, v: V> self.right.has_mapping(k, v) ==> @self.key < k)
        }
    }

    #[predicate]
    fn bst_invariant(self) -> bool {
        pearlite! {
            self.bst_invariant_here() && self.left.bst_invariant() && self.right.bst_invariant()
        }
    }
}

impl<K: Model, V> Tree<K, V>
where
    K::ModelTy: OrdLogic,
{
    #[predicate]
    fn bst_invariant(self) -> bool {
        pearlite! {
            match self {
                Tree { node: None } => true,
                Tree { node: Some(box node) } => {
                    let Node { left, color, key, val, right } = node;
                    node.bst_invariant_here() && left.bst_invariant() && right.bst_invariant()
                }
            }
        }
    }
}

/******************************  The color invariant **************************/

impl<K, V> Tree<K, V> {
    #[predicate]
    fn is_red_log(self) -> bool {
        match self.node {
            Some(box Node { left, color: Red, key, val, right }) => true,
            _ => false,
        }
    }

    #[predicate]
    fn color_invariant(self) -> bool {
        pearlite! {
            match self {
                Tree { node: None } => true,
                Tree { node: Some(box node) } => {
                    let Node { left, color, key, val, right } = node;
                    node.color_invariant_here() && left.color_invariant() && right.color_invariant()
                }
            }
        }
    }
}

impl<K, V> Node<K, V> {
    #[predicate]
    fn color_invariant_here(self) -> bool {
        pearlite! { !self.right.is_red_log() && (self.color === Red ==> !self.left.is_red_log()) }
    }

    #[predicate]
    fn color_invariant(self) -> bool {
        self.color_invariant_here() && self.left.color_invariant() && self.right.color_invariant()
    }
}

/*****************************  The height invariant  *************************/

impl<K, V> Node<K, V> {
    #[predicate]
    fn has_height(self, h: Int) -> bool {
        match self {
            Node { left, color: Red, key, val, right } => left.has_height(h) && right.has_height(h),
            Node { left, color: Black, key, val, right } => {
                left.has_height(h - 1) && right.has_height(h - 1)
            }
        }
    }
}

impl<K, V> Tree<K, V> {
    #[predicate]
    fn has_height(self, h: Int) -> bool {
        pearlite! {
            match self {
                Tree { node: None } => h === 0,
                Tree { node: Some(box Node { left, color: Red, key, val, right }) } =>
                    left.has_height(h) && right.has_height(h),
                Tree { node: Some(box Node { left, color: Black, key, val, right }) } =>
                    left.has_height(h-1) && right.has_height(h-1)
            }
        }
    }
}

/*************************  Conjunction of invariants  ************************/

impl<K: Model, V> Tree<K, V>
where
    K::ModelTy: OrdLogic,
{
    #[predicate]
    pub fn invariant(self) -> bool {
        pearlite! {
            self.bst_invariant() && self.color_invariant() &&
            exists<h: Int> self.has_height(h)
        }
    }
}

/*************************  Code of the data structure  ***********************/

impl<K: Model, V> Node<K, V> {
    #[ensures(result == self.is_red_log())]
    fn is_red(&self) -> bool {
        match self.node {
            Some(box Node { color: Red, .. }) => true,
            _ => false,
        }
    }
}

impl<K: Model, V> Node<K, V>
where
    K::ModelTy: OrdLogic,
{
    #[requires((*self).bst_invariant())]
    #[requires((*self).left.is_red_log())]
    #[ensures((*self).same_mappings(^self))]
    #[ensures((^self).bst_invariant())]
    #[ensures((^self).right.is_red_log())]
    #[ensures((^self).color === (*self).color)]
    #[ensures(exists<l: Box<Self>, r: Box<Self>>
              (*self).left.node === Some(l) && (^self).right.node === Some(r) &&
              ((^self).left, r.left, r.right) === (l.left, l.right, (*self).right))]
    #[ensures(forall<h: Int> (*self).has_height(h) ==> (^self).has_height(h))]
    fn rotate_right(&mut self) {
        let old_self = Ghost::record(&*self);

        //     self
        //    /    \
        //   x      c
        //  / \
        // a   b
        // Rip out the left subtree
        let mut x: Box<_> = match std::mem::replace(&mut self.left.node, None) {
            Some(x) => x,
            None => panic!(),
        };

        //     self
        //         \
        //   x      c
        //  / \
        // a   b
        std::mem::swap(&mut self.left, &mut x.right);
        //        self
        //       /    \
        //   x  b      c
        //  /
        // a
        std::mem::swap(self, &mut x);
        self.color = x.color;
        x.color = Red;
        //   self
        //  /
        // a      x
        //       / \
        //      b   c
        proof_assert! { (@old_self).left.has_mapping(@(*self).key, (*self).val) }
        proof_assert! { forall<k: K::ModelTy, v: V> x.left.has_mapping(k, v) ==> (@old_self).left.has_mapping(k, v) }
        self.right = Tree { node: Some(x) };
        //   self
        //  /    \
        // a      x
        //       / \
        //      b   c
    }

    #[requires((*self).bst_invariant())]
    #[requires((*self).right.is_red_log())]
    #[ensures((*self).same_mappings(^self))]
    #[ensures((^self).bst_invariant())]
    #[ensures((^self).left.is_red_log())]
    #[ensures((^self).color === (*self).color)]
    #[ensures(exists<l: Box<Self>, r: Box<Self>>
              (*self).right.node === Some(r) && (^self).left.node === Some(l) &&
              (l.left, l.right, (^self).right) === ((*self).left, r.left, r.right))]
    #[ensures(forall<h: Int> (*self).has_height(h) ==> (^self).has_height(h))]
    fn rotate_left(&mut self) {
        let old_self = Ghost::record(&*self);

        let mut x: Box<_> = match std::mem::replace(&mut self.right.node, None) {
            Some(x) => x,
            None => panic!(),
        };
        std::mem::swap(&mut self.right, &mut x.left);
        std::mem::swap(self, &mut x);
        self.color = x.color;
        x.color = Red;
        proof_assert! { (@old_self).right.has_mapping(@(*self).key, (*self).val) }
        proof_assert! { forall<k: K::ModelTy, v: V> x.right.has_mapping(k, v) ==> (@old_self).right.has_mapping(k, v) }
        self.left = Tree { node: Some(x) };
    }

    #[requires((*self).bst_invariant())]
    #[requires((*self).color === Red && (*self).left.is_red_log() ==>
               (*self).left.color_invariant())]
    #[requires((*self).color === Red && (*self).right.is_red_log() ==>
               (*self).right.color_invariant())]
    #[requires((*self).color === Red && (*self).right.is_red_log() && (*self).left.is_red_log() ==> false)]
    #[ensures((*self).same_mappings(^self))]
    #[ensures((^self).bst_invariant())]
    #[ensures((*self).left.color_invariant() && !(*self).right.is_red_log() ==>
              (*self) === (^self))]
    #[ensures(forall<l: Box<Self>> (*self).left.node === Some(l) &&
              (*self).color === Black && l.color === Red &&
              l.left.is_red_log() && l.left.color_invariant() &&
              !l.right.is_red_log() && l.right.color_invariant() &&
              !(*self).right.is_red_log() && (*self).right.color_invariant() ==>
              (^self).color === Red && (^self).color_invariant())]
    #[ensures(!(*self).left.is_red_log() && (*self).left.color_invariant() &&
              (*self).right.is_red_log() && (*self).right.color_invariant() ==>
              (^self).left.is_red_log() && (^self).left.color_invariant() &&
              !(^self).right.is_red_log() && (^self).right.color_invariant() &&
              (^self).color === (*self).color)]
    #[ensures((*self).color === Black &&
              (*self).left.is_red_log() && (*self).left.color_invariant() &&
              (*self).right.is_red_log() && (*self).right.color_invariant() ==>
              (^self).color === Red && (^self).color_invariant())]
    #[ensures(forall<h: Int> (*self).has_height(h) ==> (^self).has_height(h))]
    fn insert_rebalance(&mut self) {
        if self.right.is_red() && !self.left.is_red() {
            self.rotate_left();
        }

        if self.left.is_red() && self.left.node.as_ref().unwrap().left.is_red() {
            self.rotate_right();
        }

        if self.left.is_red() && self.right.is_red() {
            self.color = Red;
            match self {
                Node { left: Tree { node: Some(l) }, right: Tree { node: Some(r) }, .. } => {
                    l.color = Black;
                    r.color = Black;
                    proof_assert!((*l).bst_invariant());
                    proof_assert!((*r).bst_invariant());
                }
                _ => panic!(),
            }
            proof_assert!((*self).bst_invariant_here());
        }
    }
}

impl<K: Model + Ord, V> Tree<K, V>
where
    K::ModelTy: OrdLogic
{
    #[ensures(@result === Mapping::cst(None))]
    #[ensures(result.invariant())]
    pub fn new() -> Tree<K, V> {
        Tree { node: None }
    }

    #[requires((*self).bst_invariant())]
    #[requires((*self).color_invariant())]
    #[requires(forall<k:K::ModelTy> @key == k ==> @key === k)] // FIXME: get rid of log_eq
    #[ensures((^self).bst_invariant())]
    #[ensures(exists<node: Box<Node<K, V>>> (^self).node === Some(node) &&
              !node.right.is_red_log() &&
              node.left.color_invariant() && node.right.color_invariant())]
    #[ensures(!(*self).is_red_log() ==> (^self).color_invariant())]
    #[ensures((^self).has_mapping(@key, val))]
    #[ensures(forall<k: K::ModelTy, v: V> k === @key || (*self).has_mapping(k, v) === (^self).has_mapping(k, v))]
    #[ensures(forall<h: Int> (*self).has_height(h) ==> (^self).has_height(h))]
    fn insert_rec(&mut self, key: K, val: V) {
        let old_self = Ghost::record(&*self);
        match &mut self.node {
            None => {
                self.node = Some(Box::new(Node {
                    left: Tree { node: None },
                    color: Red,
                    key,
                    val,
                    right: Tree { node: None },
                }));
                return;
            }
            Some(node) => {
                match key.cmp(&node.key) {
                    Less => node.left.insert_rec(key, val),
                    Equal => {
                        node.val = val;
                        return;
                    }
                    Greater => node.right.insert_rec(key, val),
                }
                proof_assert!(forall<h: Int> (@old_self).has_height(h) ==> node.has_height(h));

                node.insert_rebalance();
            }
        }
    }

    #[requires((*self).invariant())]
    #[requires(forall<k:K::ModelTy> @key == k ==> @key === k)] // FIXME: get rid of log_eq
    #[ensures((^self).invariant())]
    #[ensures(@^self === (@*self).set(@key, Some(val)))]
    pub fn insert(&mut self, key: K, val: V) {
        let old_self = Ghost::record(&*self);
        self.insert_rec(key, val);
        self.node.as_mut().unwrap().color = Black;
        proof_assert! { forall<h: Int> (@old_self).has_height(h) ==>
        (*self).has_height(h) || (*self).has_height(h+1) }
        proof_assert! { (*self).has_binding_model(@key /* dummy */, val /* dummy */); true }
    }

    #[requires((*self).bst_invariant())]
    #[requires(forall<k:K::ModelTy> @key == k ==> @key === k)] // FIXME: get rid of log_eq
    #[ensures(forall<r: &V> result === Some(r) ==> (*self).has_mapping(@*key, *r))]
    #[ensures(result === None ==> forall<v: V> !(*self).has_mapping(@*key, v))]
    fn get_rec(&self, key: &K) -> Option<&V> {
        match &self.node {
            None => None,
            Some(node) => match key.cmp(&node.key) {
                Less => node.left.get_rec(key),
                Equal => Some(&node.val),
                Greater => node.right.get_rec(key),
            },
        }
    }

    #[requires((*self).invariant())]
    #[requires(forall<k:K::ModelTy> @key == k ==> @key === k)] // FIXME: get rid of log_eq
    #[ensures(forall<v: &V> (result === Some(v)) === ((@*self).get(@*key) === Some(*v)))]
    #[ensures((result === None) === (@*self).get(@*key) === None)]
    pub fn get(&self, key: &K) -> Option<&V> {
        proof_assert! { forall<v:V> { self.has_binding_model(@*key, v); true } }
        self.get_rec(key)
    }

    #[requires((*self).invariant())]
    #[requires(forall<k:K::ModelTy> @key == k ==> @key === k)] // FIXME: get rid of log_eq
    #[ensures((^self).invariant())]
    #[ensures((^self).is_red_log() === (*self).is_red_log())]
    #[ensures(forall<r: &mut V> result === Some(r) ==> (*self).has_mapping(@*key, *r) && (^self).has_mapping(@*key, ^r))]
    #[ensures(result === None ==> forall<v: V> !(*self).has_mapping(@*key, v) && !(^self).has_mapping(@*key, v))]
    #[ensures(forall<k: K::ModelTy, v: V> k === @key || (*self).has_mapping(k, v) === (^self).has_mapping(k, v))]
    #[ensures(forall<h: Int> (*self).has_height(h) ==> (^self).has_height(h))]
    fn get_mut_rec(&mut self, key: &K) -> Option<&mut V> {
        match &mut self.node {
            None => None,
            Some(node) => match key.cmp(&node.key) {
                Less => node.left.get_mut_rec(key),
                Equal => Some(&mut node.val),
                Greater => node.right.get_mut_rec(key),
            },
        }
    }

    #[requires((*self).invariant())]
    #[requires(forall<k:K::ModelTy> @key == k ==> @key === k)] // FIXME: get rid of log_eq
    #[ensures((^self).invariant())]
    #[ensures(forall<v: &mut V> result === Some(v) ==>
              (@*self).get(@*key) === Some(*v) && @^self === (@*self).set(@key, Some(^v)))]
    #[ensures(result === None ==> (@*self).get(@*key) === None && (@^self).get(@*key) === None)]
    pub fn get_mut(&mut self, key: &K) -> Option<&mut V> {
        proof_assert! { forall<v:V> { self.has_binding_model(@*key, v); true } }
        self.get_mut_rec(key)
    }
}

opened by jhjourdan 29

Add `#[logic_rust]` and `#[predicate_rust]` attributes

This PR adds #[logic] attribute and renames logic! to logic_fn!. You can use #[logic] when the function body does not use pearlite syntax. In this way, we can get better IDE support. When we want to use pearlite syntax, we use logic_fn! macro (old logic! macro).

I also updated README.md to give better explanation on logic and pure.

opened by shiatsumat 16

Timeouts

I was trying to see if I could get why3 prove -P z3 to give more Unknown responses as opposed to Timeout. I modified my .why3.conf to include:

[prover]
alternative = "no_mbqi"
command = "/usr/bin/z3 -smt2 -T:%t smt.AUTO_CONFIG=false smt.PHASE_SELECTION=0 smt.RESTART_STRATEGY=0 smt.RESTART_FACTOR=1.5 smt.ARITH.RANDOM_INITIAL_VALUE=true smt.CASE_SPLIT=3 smt.DELAY_UNITS=true NNF.SK_HACK=true smt.MBQI=false smt.BV.REFLECT=true smt.qi.max_multi_patterns=1000 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 -st %f"
command_steps = "/usr/bin/z3 -smt2 smt.AUTO_CONFIG=false smt.PHASE_SELECTION=0 smt.RESTART_STRATEGY=0 smt.RESTART_FACTOR=1.5 smt.ARITH.RANDOM_INITIAL_VALUE=true smt.CASE_SPLIT=3 smt.DELAY_UNITS=true NNF.SK_HACK=true smt.MBQI=false smt.BV.REFLECT=true smt.qi.max_multi_patterns=1000 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 -st rlimit=%S %f"
driver = "z3_471"
editor = ""
in_place = false
interactive = false
name = "Z3"
shortcut = "z3_no_mbqi"
version = "4.8.12"

and switched -P z3_no_mbqi which fixed:

fn test(x: Int, y: Int) {
    proof_assert!(x == y);
}

and also seemed to improve performance somewhat. The example:

fn test(x: Option<Int>) {
    proof_assert!(x == None);
}

still timed out. I was able to fix this by removing use seq.Seq and use prelude.Prelude (which uses seq.Seq) from the Type module, and figured out that anything using seq.Seq will cause Z3 to timeout instead of returning unknown. A potential mitigation might be to split the Type module into individual modules (one per rust type) and prelude.Prelude into

module Prelude
  type opaque_ptr

  type borrowed 'a = { current : 'a ; final : 'a; }
  let function ( *_ ) x = x.current
  let function ( ^_ ) x = x.final
  val borrow_mut (a : 'a) : borrowed 'a
  ensures { *result = a }

  let function id (x: 'a) : 'a = x

  let eqb (a : bool) (b : bool) : bool =
    ensures { result <-> a = b  }
    match a, b with
    | True, True -> True
    | False, False -> True
    | _ -> False
    end
end
module RustArray
    use seq.Seq
    type rust_array 'a = seq 'a
end
module IntSize
    use mach.int.Int64
    type isize = int64
end
module UIntSize
    use mach.int.UInt64
    type isize = uint64
end

This also seems to be good for performance in general.

opened by dewert99 15

unbound type symbol 'Item0.item'

I'm getting that error on the reproducer below:

extern crate creusot_contracts;
use creusot_contracts::*;

fn search() -> usize {
   #[invariant(dummy,true)]
   for i in 0..1 {
      if true {
         return i
      }
   }
   return 0
}

Do you have a suggestion to work around that issue? thanks

opened by yannickmoy 13

Lacking logic in generated mlcfg

When generating the mlcfg file, the logic part seems to be missing. For example, for the inc-max.rs file, i get the file attached. Is there an option to generate the logic?

Best inc_max.txt .

opened by DabrowskiFr 12
Interpreting dereference in postconditions
This is a question to understand how dereference is interpreted in postconditions. If I take your code for Zeroing out a list, I can turn it into a function bad_all_zero which drops the list as follows:

#[ensures(len(*l) === 0)] fn bad_all_zero(l: &mut List) { *l = Nil; proof_assert!(len(*l) === 0); }

The proof assertion is proved, but not the postcondition, where *l is interpreted in the memory before the call to bad_all_zero. What's the model to keep in mind to understand this?
opened by yannickmoy 12

Panicked at 'could not find instance', creusot/src/translation/function/terminator.rs:143:22

I get the following error message, when running cargo creusot in the concordium-contracts-common crate located Concordium/concordium-contracts-common.

warning: load the `creusot_contract` crate to enable resolution of mutable borrows.

module 
  use Ref
  use mach.int.Int
  use mach.int.Int32
  use mach.int.Int64
  use mach.int.UInt32
  use mach.int.UInt64
  use string.Char
  use floating_point.Single
  use floating_point.Double
  use prelude.Prelude
  type core_marker_phantomdata 't = 
    | Core_Marker_PhantomData
    
  type creusotcontracts_logic_ghost 't = 
    | CreusotContracts_Logic_Ghost (core_marker_phantomdata 't)
    
end
module 
  type t   
  use prelude.Prelude
  use Type
  val record (_1 : t) : Type.creusotcontracts_logic_ghost t
end
module 
  type t   
  use prelude.Prelude
  use Type
  let rec cfg record (_1 : t) : Type.creusotcontracts_logic_ghost t = 
  {
    goto BB0
  }
  
end
thread 'rustc' panicked at 'could not find instance', creusot/src/translation/function/terminator.rs:143:22
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

note: Creusot has panic-ed!
  |
  = note: Oops, that shouldn't have happened, sorry about that.
  = note: Please report this bug over here: https://github.com/xldenis/creusot/issues/new

error: could not compile `concordium-contracts-common`; 1 warning emitted

opened by cmester0 12

Add `#[modeled_by=X]` attribute
When using 'unsafe types' we want to give them a model, or representation value in the formalization which will be used during proofs.

The way I'm proposing to do this at the moment is to add an attribute which can be attached to type declarations which specifies which type models a given type. This does not create new verification conditions, and is meant to be used only in cases where we have separately proved the model in RustHornBelt or some other mechanism. Additionally, it should be subsumed by a proper ghost field & type invariant system (once we figure out how that works).

What does this attribute do? Well,...

#[model=List<T>] struct Vec<T> { spooky_pointers: *mut T }

Simply generates an opaque predicate model on Vec:

struct Vec<T> { ... } impl Vec<T> { predicate! { fn model(self) -> List<T>; } }

This allows us to refer to the model of a vector in contracts like so:

impl Vec<T> { #[ensures(^self.model() = *.self.model().snoc(e))] fn push(&mut self, e: T) -> { ... } ... }
opened by xldenis 12

PartialEq on Vec fails with a Why3 type error

I haven't really thought about why this is happening yet, I'll look at this in more detail tomorrow but thought I should document it now.

This code

use creusot_contracts::*;

#[ensures(result == true)]
fn veq() -> bool {
    let v1: Vec<i32> = Vec::new();
    let v2: Vec<i32> = Vec::new();
    v1 == v2
}

fn main() {}

Fails with this error

File "./target/debug/testbin-bin.mlcfg", line 165, characters 44-62:
This term has type seq.Seq.seq Alloc_Vec_PartialEq_Impl0_Eq_Interface.u,
but is expected to have type seq.Seq.seq
Alloc_Vec_PartialEq_Impl0_Eq_Interface.t

And this seems to be the relevant whyml snippet (line 165 is the ensures line at the end of the module).

module Alloc_Vec_PartialEq_Impl0_Eq_Interface
  type t
  type u
  type a1
  type a2
  use prelude.Borrow
  clone CreusotContracts_Std1_Vec_Impl0_ModelTy_Type as ModelTy1 with type t = u, type a = a2
  clone CreusotContracts_Std1_Vec_Impl0_ModelTy_Type as ModelTy0 with type t = t, type a = a1
  use Alloc_Vec_Vec_Type as Alloc_Vec_Vec_Type
  clone CreusotContracts_Logic_Model_Impl0_Model_Stub as Model1 with type t = Alloc_Vec_Vec_Type.t_vec u a2,
    type ModelTy0.modelTy = ModelTy1.modelTy
  clone CreusotContracts_Logic_Model_Impl0_Model_Stub as Model0 with type t = Alloc_Vec_Vec_Type.t_vec t a1,
    type ModelTy0.modelTy = ModelTy0.modelTy
  val eq [@cfg:stackify] (self : Alloc_Vec_Vec_Type.t_vec t a1) (other : Alloc_Vec_Vec_Type.t_vec u a2) : bool
    ensures { result = (Model0.model self = Model1.model other) }
    
end

I haven't bisected yet, but this error is new from a few weeks ago (the code validates correctly on ea4a283193a00ec0583d37e13f04e279a68bb736)

opened by gmorenz 11

Refactorings (WIP)
Lower why3 lowering to backend

Cleanup promoted translation

Move dependency calculation to new system

Better, semantic interface to cloning

Make to_clones consume map

wip: refactor ty

start moving logic to new system

Get a basic logic function working

Translate basic program function

Add support for types

Add trait impls

Get traits working

Enable most of creusot_contracts

Fix dependency calculation to handle nested deps

renable baubles

Add constants and accessors

Fix imports for constructors and accessors

Remove clonemap from logic

Cleanup some warnings

🐛🐞 hunting

Continue working on getting a fully working version of 206

Ever closer

Fix some missing deps

Fully renable creusot-contracts logic

Fix most of std

Enable even more stuff

Uncomment all impls

Everything except map

Rewrite closure contracts in terms of pearlite

baby steps towards closureS

Fix calls of program functions

Sketch working closure

fixeS

Get a closure compiling

support unnest predicate in closures

Get all bug modules to generate mlcfg

initial mlcfg for all bug modules

wip

closer

wip

Wip

Properly handle mutual rec

Dead code cleanup

Fix some more bugs

More dead code

more dead code elimination

Bug hunting

Fix closures

No tests panic

Introduce a custom id type to handle multiple closure definitions

Continue

wip
opened by xldenis 0

Crash reported

@jhaye reports that the following code creates ill typed why3 code.


use creusot_contracts::*;

/// A sparse map representation over a totally ordered key type.
///
/// Used in [crate::ExecutableReactions]
///
pub struct VecMap<K, V>
where
    K: Eq + Ord,
{
    v: Vec<(K, V)>,
}

impl<K, V> VecMap<K, V>
where
    K: Eq + Ord + DeepModel,
    K::DeepModelTy: OrdLogic,
{
    #[logic]
    #[trusted]
    #[ensures(result.len() == (@self.v).len() &&
              forall<i: Int> i >= 0 && i < (@self.v).len() ==>
              result[i] == (@self.v)[i].0.deep_model())]
    fn key_seq(self) -> Seq<K::DeepModelTy> {
        pearlite! { absurd }
    }

    #[predicate]
    fn is_sorted(self) -> bool {
        pearlite! {
            forall<m: Int, n: Int> m >= 0 && n >= 0 && m < (@self.v).len() && n < (@self.v).len() && m < n ==>
                self.key_seq()[m] < self.key_seq()[n]
        }
    }
}

impl<K, V> VecMap<K, V>
where
    K: Eq + Ord + DeepModel,
    K::DeepModelTy: OrdLogic,
{
    /// Directly insert into the underlying `Vec`. This does not maintain the sorting of elements
    /// by itself.
    #[requires(@idx <= (@self.v).len())]
    #[ensures((@(^self).v).len() == (@self.v).len() + 1)]
    #[ensures(forall<i: Int> 0 <= i && i < @idx ==> (@(^self).v)[i] == (@self.v)[i])]
    #[ensures((@(^self).v)[@idx] == (key, value))]
    #[ensures(forall<i: Int> @idx < i && i < (@(^self).v).len() ==> (@(^self).v)[i] == (@self.v)[i - 1])]
    #[ensures(self.is_sorted() && (@self.v).len() == 0 ==> (^self).is_sorted())]
    #[ensures(self.is_sorted() && (@self.v).len() > 0 && @idx > 0 && @idx < (@self.v).len() &&
              (@self.v)[@idx].0.deep_model() > key.deep_model() &&
              (@self.v)[@idx - 1].0.deep_model() < key.deep_model() ==>
              (^self).is_sorted()
    )]
    #[ensures(self.is_sorted() && (@self.v).len() > 0 && @idx == 0 &&
              (@self.v)[@idx].0.deep_model() > key.deep_model() ==>
              (^self).is_sorted()
    )]
    #[ensures(self.is_sorted() && (@self.v).len() > 0 && @idx == (@self.v).len() &&
              (@self.v)[@idx - 1].0.deep_model() < key.deep_model() ==>
              (^self).is_sorted()
    )]
    fn insert_internal(&mut self, idx: usize, key: K, value: V) {
        self.v.insert(idx, (key, value))
    }
}

/// A vacant Entry.
pub struct VacantEntry<'a, K, V>
where
    K: Ord + Eq,
{
    map: &'a mut VecMap<K, V>,
    key: K,
    index: usize,
}

impl<K, V> VacantEntry<'_, K, V>
where
    K: Ord + Eq + Clone + DeepModel,
    K::DeepModelTy: OrdLogic,
{
    /// Sets the value of the entry with the VacantEntry's key.
    #[requires(self.map.is_sorted())]
    #[requires(@self.index <= (@self.map.v).len())]
    #[requires(forall<i: Int> i >= 0 && i < @self.index ==>
               self.map.key_seq()[i] < self.key.deep_model())]
    #[requires(forall<i: Int> i >= @self.index && i < (@self.map.v).len() ==>
               self.map.key_seq()[i] > self.key.deep_model())]
    #[ensures((^self).map.is_sorted())]
    pub fn insert(&mut self, value: V) {
        self.map
            .insert_internal(self.index, self.key.clone(), value)
    }
}

opened by xldenis 0

Support for bit-level operations
Hi,

I wanted to try proving the correctness of data-encoding but I hit the following error:

error[creusot]: unsupported binary operation: Shl

Is support for bit-level operations planned? I could not find an existing issue about it. Would be happy to subscribe to such issue and give it another try once there's support.

Thanks!
opened by ia0 1
Remove CloneMap
12030th time is the charm.

Removes CloneMap in favor of pre-calculating all the dependencies in the crate. This also makes it simpler to not produce clones but instead monomorphize all the definitions.

The code is incomplete and not cleaned up, at the moment it can translate basic logic functions and basic program functions. I'll keep progressively upping the complexity (promoteds, closures, etc) until it covers everything before doing a major clean up pass.

Major TODOs:

[x] Closures

[x] Constants

[ ] External Dependencies

[ ] Debug

[ ] Add caching for dependency calculation

[ ] Remove CloneMap
opened by xldenis 1

Please tell users to use z3 4.8.8 and older

Consider this code:

#[cfg(my_prover)]
extern crate creusot_contracts;

#[cfg(my_prover)]
use creusot_contracts::*;

#[trusted]
#[ensures(result == forall<k: usize> (@a).len() - @i - 1 <= @k && @k < (@a).len() - 1 ==> (@a)[@k] <= (@a)[@k + 1])]
fn f(a: &[i32], i: usize) -> bool {
    return true;
}

fn sort(a: &mut [i32]) {
    let len = a.len();
    if a.len() == 0 {
        return;
    }
    let mut i = 0;
    #[cfg_attr(my_prover, invariant(a, (@a).len() == @len))]
    #[cfg_attr(my_prover, invariant(a, @i > 0 ==> forall<k: usize> @k < @len - @i ==> (@a)[@k] <= (@a)[@len - @i]))]
    while i < a.len() - 1 {
        if !f(a, i) {
            return;
        }
        proof_assert!(forall<k: usize> (@a).len() - @i - 1 <= @k && @k < (@a).len() - 1 ==> (@a)[@k] <= (@a)[@k + 1]);
        proof_assert!(forall<k: usize> (@a).len() - @i <= @k && @k < (@a).len() - 1 ==> (@a)[@k] <= (@a)[@k + 1]);
        proof_assert!(@i > 0 ==> forall<k: usize> @k < @len - @i ==> (@a)[@k] <= (@a)[@len - @i]);
        {
            let mut j = 0;
            let x = if i == 0 { 0 } else { a[len - i] };
            #[cfg_attr(my_prover, invariant(a, (@a).len() == @len))]
            #[cfg_attr(my_prover, invariant(a, forall<k: usize> @k < @j ==> (@a)[@k] <= (@a)[@j]))]
            #[cfg_attr(my_prover, invariant(a, @j <= @len - @i - 1))]
            #[cfg_attr(my_prover, invariant(a, forall<k: usize> (@a).len() - @i <= @k && @k < (@a).len() - 1 ==> (@a)[@k] <= (@a)[@k + 1]))]
            while j < a.len() - i - 1 {
                if a[j] > a[j + 1] {
                    let sw = a[j];
                    a[j] = a[j + 1];
                    a[j + 1] = sw;
                }
                j += 1;
            }
        }
        proof_assert!(forall<k: usize> (@a).len() - @i <= @k && @k < (@a).len() - 1 ==> (@a)[@k] <= (@a)[@k + 1]);
        proof_assert!(forall<k: usize> @k < @len - @i - 1 ==> (@a)[@k] <= (@a)[@len - @i - 1]);
        i += 1;
    }
}

fn main(){ }

This is my (incomplete) attempt to prove bubble sort in Creusot. I'm sorry for my_prover noise, I added it to make sure the source can be built in the same time by Creusot and normal rust compiler.

I check this code using Creusot (obviously, I add --cfg my_prover to creusot-rustc invocation). And checking takes 8.13s (I have to pass -t option to why3 to make sure I will not get timeout).

My z3 version is 4.8.10. This reminds me z3 regression I recently discovered when working with Prusti ( https://github.com/viperproject/prusti-dev/issues/1245 , https://github.com/viperproject/silicon/issues/664#issuecomment-1324811845 ). So I tried to use older z3 version, namely this: https://github.com/Z3Prover/z3/commit/3c9ada54b64e5516e0cf869c5de7881686df8fd0 . (This is "last good" commit I discovered when I did gitbisecting when working with Prusti).

And now that Creusot source checks for 0.42s!

So it seems that z3 regression applies to Creusot, too. Please, update installation instructions, tell your users to always use z3 no later than 4.8.8 version. See also https://twitter.com/RanjitJhala/status/1391486845435871233 .

P. S. In this code I used function f as "assume". Is there proper way to do "assume"?

opened by safinaskar 10

Releases(v0.2)

v0.2(Nov 9, 2022)

Source code(tar.gz)
Source code(zip)

deductive verification of Rust code. (semi) automatically prove your code satisfies your specifications!

Related tags

Overview

About

Example programs that have been proven:

Installing

Generating MLCFG outputs

Proving programs with Why3

Writing specifications

Loading as an extern crate

Kinds of contract expressions

Pearlite

Comments

Releases(v0.2)

v0.2(Nov 9, 2022)

Owner

Xavier Denis

Fastmurmur3 - Fast non-cryptographic hash, with the benchmarks to prove it.

🛠️ Uses zkevm-circuits and anvil mainnetfork to prove that a tx solves an EVM challenge

A "Type 0" zkEVM. Prove validity of Ethereum blocks using RISC Zero's zkVM

Fast and efficient ed25519 signing and verification in Rust.

An implementation of NZ COVID Pass verification written in Rust

RSA dependency for rust, with cert verification

A certificate verification library for rustls that uses the operating system's verifier

A certificate verification library for rustls that uses the operating system's verifier

Simple, reliable, open-source contract verification built for an L2 centric Ethereum ecosystem

specs & benchmarks for the ZPrize 3 - High Throughput Signature Verification

Kubernetes controller written in Rust for automatically generating and updating secrets

shavee is a Program to automatically decrypt and mount ZFS datasets using Yubikey HMAC as 2FA or any USB drive with support for PAM to auto mount home directories.

Automatically assess and score software repositories for supply chain risk.

Release complex cargo-workspaces automatically with changelog generation, used by `gitoxide`

Bitcoin Push Notification Service (BPNS) allows you to receive notifications of Bitcoin transactions of your non-custodial wallets on a provider of your choice, all while respecting your privacy

A PackageJson struct for your rust code.

A collection of lints to catch common mistakes and improve your Cairo code.

Employ your built-in wetware pattern recognition and signal processing facilities to understand your network traffic

Koofr Vault is an open-source, client-side encrypted folder for your Koofr cloud storage offering an extra layer of security for your most sensitive files.