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

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 Why3. 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

  1. Install Rust using rustup to manage toolchains
  2. Clone the repository
  3. Install the Rust compiler libraries: rustup component add rustc-dev
  4. (Optional, Recommended) Install the Rust compiler sources: rustup component add rustc-src
  5. 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

    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

    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

    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

    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

    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'

    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

    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

    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

    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

    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

    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)

    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

    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

    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

    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

    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)
Owner
Xavier Denis
phd on rust verification @ LMF. coq / haskell / rust / ruby provably incorrect
Xavier Denis
Fastmurmur3 - Fast non-cryptographic hash, with the benchmarks to prove it.

Fastmurmur3 Murmur3 is a fast, non-cryptographic hash function. fastmurmur3 is, in my testing, the fastest implementation of Murmur3. Usage let bytes:

Kurt Wolf 13 Dec 2, 2022
🛠️ Uses zkevm-circuits and anvil mainnetfork to prove that a tx solves an EVM challenge

zk-proof-of-evm-execution This is a PoC developed at hackathon that enables a user to prove that they know some calldata that can solve a challenge on

soham 9 Mar 29, 2023
A "Type 0" zkEVM. Prove validity of Ethereum blocks using RISC Zero's zkVM

zeth NEW: Zeth now supports Optimism blocks! Just pass in --network=optimism! Zeth is an open-source ZK block prover for Ethereum built on the RISC Ze

RISC Zero 222 Oct 26, 2023
Fast and efficient ed25519 signing and verification in Rust.

ed25519-dalek Fast and efficient Rust implementation of ed25519 key generation, signing, and verification in Rust. Documentation Documentation is avai

dalek cryptography 563 Dec 26, 2022
An implementation of NZ COVID Pass verification written in Rust

NZCP Rust   An implementation of NZ COVID Pass verification, New Zealand's proof of COVID-19 vaccination solution, written in Rust ?? We also have a J

Vaxx.nz 7 Nov 24, 2022
RSA dependency for rust, with cert verification

About Project End to End encryption (RSA) for multiple languages (cross-platform) with double encryption and double decryption methods Icon Item ?? Up

Zot Cryptography 2 Nov 27, 2022
A certificate verification library for rustls that uses the operating system's verifier

rustls-platform-verifier A Rust library to verify the validity of TLS certificates based on the operating system's certificate facilities. On operatin

null 17 Dec 26, 2022
A certificate verification library for rustls that uses the operating system's verifier

rustls-platform-verifier A Rust library to verify the validity of TLS certificates based on the operating system's certificate facilities. On operatin

null 13 Nov 6, 2022
Simple, reliable, open-source contract verification built for an L2 centric Ethereum ecosystem

Cove This repo contains the backend verification1 code for Cove, a simple, reliable, open-source contract verification built for an L2 centric Ethereu

ScopeLift 12 Apr 1, 2023
specs & benchmarks for the ZPrize 3 - High Throughput Signature Verification

Zprize: High Throughput Signature Verification How fast do you think you can verify our ECDSA signatures on Aleo? This year's Zprize is winner-take-al

null 6 Oct 21, 2023
Kubernetes controller written in Rust for automatically generating and updating secrets

Kubernetes controller written in Rust for automatically generating and updating secrets

Loc Mai 6 Nov 8, 2022
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.

shavee is a simple program to decrypt and mount encrypted ZFS user home directories at login using Yubikey HMAC or a Simple USB drive as 2FA written in rust.

Ashutosh Verma 38 Dec 24, 2022
Automatically assess and score software repositories for supply chain risk.

Hipcheck Hipcheck scores risks for software projects; yours and your dependencies. It analyzes repositories to assess risks, review development practi

The MITRE Corporation 6 Jan 26, 2023
Release complex cargo-workspaces automatically with changelog generation, used by `gitoxide`

cargo smart-release Fearlessly release workspace crates and with beautiful semi-handcrafted changelogs. Key Features zero-configuration cargo smart-re

Sebastian Thiel 24 Oct 11, 2023
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

Bitcoin Push Notification Service (BPNS) Description Bitcoin Push Notification Service (BPNS) allows you to receive notifications of Bitcoin transacti

BPNS 1 May 2, 2022
A PackageJson struct for your rust code.

??️ package_json_schema Load a package.json file as a PackageJson struct. Why? You want to load a package.json file and interact with it as a struct.

Ifiok Jr. 3 Oct 13, 2022
Employ your built-in wetware pattern recognition and signal processing facilities to understand your network traffic

Nethoscope Employ your built-in wetware pattern recognition and signal processing facilities to understand your network traffic. Check video on how it

Vesa Vilhonen 86 Dec 5, 2022
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.

Koofr Vault https://vault.koofr.net Koofr Vault is an open-source, client-side encrypted folder for your Koofr cloud storage offering an extra layer o

Koofr 12 Dec 30, 2022
A cryptographically verifiable code review system for the cargo (Rust) package manager.

A cryptographically verifiable code review system for the cargo (Rust) package manager.

crev - Code REView system 1.8k Jan 2, 2023