Experience Report

[xldenis]

Hi, I just discovered your repository, and I was wondering if you could provide feedback on your experience using Creusot? I think we'd love to hear how we can make your life better.

[ruth561]

Hi! Thank you for reaching out. I was planning to report back after implementing a bit more.

I would like to provide some feedback based on my experience implementing DBM.

First, let me report on the features desired but not implemented in DBM. DBM uses a system that extends integers to include infinity. I wanted to implement this numeric system, but I couldn't figure out how to create an original data structure, so I gave up. Instead, I am treating i64::MAX as infinity. I noticed that the Creusot repository has an Option type which seemed similar, but since None is treated as Bottom, I couldn't use it. It seems that the tutorial does not yet cover how to implement custom data types, so if there are any methods or examples on how to achieve this, could you please share them with me?

Another issue I encountered was not knowing how to effectively use lemmas within forall or exists. In Creusot, is it possible to use such lemmas in forall or exists? For example, I would like to call a lemma like fn lem(i: Int, j: Int) {} within forall<i: Int, j: Int> ... to assist with inference within forall.

Finally, I would like to report on the types of inferences that Creusot struggles to prove. DBM can be interpreted as operations on a graph representation using adjacency matrices. Therefore, to prove the properties of DBM, it is necessary to prove the properties of adjacency matrices. However, this often results in deeply nested forall statements, leading to cases where proofs do not pass, and requiring multiple lemmas. Specifically, it seems challenging to derive statements such as forall<i: Int, j: Int, k: Int> i == 0 && 0 <= j && j < n && 0 <= k && k < n ==> property(i, j, k) from forall<i: Int, j: Int, k: Int> 0 <= i && i < n && 0 <= j && j < n && 0 <= k && k < n ==> property(i, j, k). Using lemmas such as forall<j: Int, k: Int> 0 <= j && j < n && 0 <= k && k < n ==> property(0, j, k) to assist with the proof works well. It would be beneficial if such instances of instantiation could be handled effectively.

[xldenis]

First, let me report on the features desired but not implemented in DBM. DBM uses a system that extends integers to include infinity. I wanted to implement this numeric system, but I couldn't figure out how to create an original data structure, so I gave up. Instead, I am treating i64::MAX as infinity. I noticed that the Creusot repository has an Option type which seemed similar, but since None is treated as Bottom, I couldn't use it. It seems that the tutorial does not yet cover how to implement custom data types, so if there are any methods or examples on how to achieve this, could you please share them with me?

You can use ordinary Rust definitions, such as the following

enum ZPlusOmega {
  Z(i128),
  PosInf,
  NegInf,
}

You will then need to define in Rust the various mathematical operations you want and prove their expected specifications. You may also need to define #[logic] versions of these functions to define their behavior in the logical fragment of Creusot. In the upcoming 0.2 version of Creusot you would be able to use the #[pure] keyword to combine both of these in for things like your Z type (cc @arnaudgolfhouse).

In a prior project I was designing an Abstract Interpreter verified with creusot, and I had a BotOrNot<T> type which could be used to extend any domain with a bottom value, that worked in a manner quite similar to what I described above.

Another issue I encountered was not knowing how to effectively use lemmas within forall or exists. In Creusot, is it possible to use such lemmas in forall or exists? For example, I would like to call a lemma like fn lem(i: Int, j: Int) {} within forall<i: Int, j: Int> ... to assist with inference within forall.

Hmm, I assume you mean you would like to use a lemma to prove a forall? We don't provide any syntax to explicitly prove foralls or exists today, I would expect this will become more of a subject when a 0.3 or 0.4 release rolls around.

That being said, you can do this in a slightly different manner using lemma functions.

#[logic]
#[requires(0 <= i && i <= j && j <= k && k <n)]
#[ensures(property(I,j,k)]
fn my_lemma(I, j ,k , n, dbm) {

}

Will provide a lemma of the shape forall i j k n dbm. requires_clauses -> ensures_clauses

You can then explicitly call this lemma in your code with desired values which will introduce that specific instantiation in your proof context, ie: ghost! { my_lemma(0,0,0, 10, DBM) } will force why3 to prove the preconditions and then introduce that postcondition instantiated with teh desired variables in your proof context.

Finally, I would like to report on the types of inferences that Creusot struggles to prove. DBM can be interpreted as operations on a graph representation using adjacency matrices. Therefore, to prove the properties of DBM, it is necessary to prove the properties of adjacency matrices. However, this often results in deeply nested forall statements, leading to cases where proofs do not pass, and requiring multiple lemmas. Specifically, it seems challenging to derive statements such as forall<i: Int, j: Int, k: Int> i == 0 && 0 <= j && j < n && 0 <= k && k < n ==> property(i, j, k) from forall<i: Int, j: Int, k: Int> 0 <= i && i < n && 0 <= j && j < n && 0 <= k && k < n ==> property(i, j, k). Using lemmas such as forall<j: Int, k: Int> 0 <= j && j < n && 0 <= k && k < n ==> property(0, j, k) to assist with the proof works well. It would be beneficial if such instances of instantiation could be handled effectively.

This is fairly subtle, do you think this is something where SMT triggers would help? This could potentially make interesting test cases for performance optimization. I'm not sure I have any immediate advice to give here, though perhaps some concrete examples would help.

[xldenis]

I think you might also be able to improve your ergonomics by defining an appropriate IndexLogic instance which lets you index your matrices in one go rather than through nested indexing, there are other improvements like that that may be possible. You could consider looking at cdsat which includes some various tricks and complex specifications.

[ruth561]

Thank you for your detailed advice. Learning about Creusot's useful features will certainly benefit my future implementations. I'm looking forward to the upcoming versions of Creusot.

Regarding my second question, I realized my previous question was unclear, so I would like to ask again. I apologize for not being clear enough earlier. Is it possible to prove a proposition like forall<i:Int, j:Int, k:Int> 0<=i && i<=j && j<=k && k<n ==> property(i,j,k) using a lemma created as shown above? In the example provided, it seems feasible to use specific values for the lemma, but what I often want to do is to use a lemma with arguments that are quantified by forall. Can a lemma be called within forall to effectively continue the proof in such cases?

To elaborate further, let's assume we have proven a heavy proposition regarding forall using lemmas as follows.

#[logic]
#[requires(0 <= i && i <= j && j <= k && k < n)]
#[ensures(property(i, j, k, n, dbm))]
fn my_lemma(i: Int, j: Int, k: Int, n: Int, dbm: DBM) {
    [...]
}

Once we can prove this lemma, I would like to actually rewrite it using forall. Specifically, I think having the following notation would be convenient.

fn my_theorem() {
    [...]
    proof_assert! {
        forall<i:Int, j:Int, k:Int>
            0 <= i && i <= j && j <= k && k < n ==> {
                my_lemma(i, j, k, n, dbm); // this helps to prove the next property 
                property(i, j, k, n, dbm)
            }
    }
    // and, we get the following proof
    proof_assert! {
        forall<i:Int, j:Int, k:Int>
            0 <= i && i <= j && j <= k && k < n ==> property(i, j, k, n, dbm)
    }
    [...]
}

do you think this is something where SMT triggers would help?

I apologize, but my understanding of SMT solvers is not deep enough to provide an informed answer.

[xldenis]

Once we can prove this lemma, I would like to actually rewrite it using forall. Specifically, I think having the following notation would be convenient. ...

I definitely think this kind of notation would be helpful but we don't offer it at the moment, why3 has a similar notion: assert { x } by { foo } which will cause why3 to attempt to apply foo to prove the goal and move from there.

Dafny on the other hand has all: expressions which you can use to provide ghost steps to prove a lemma (like the body of lemmas in creusot). ie:

all x:
   assert { Q(x) };
   P(x)

Allows you to prove forall x . P(x) but use an intermediate assertion in the proof itself.

If you can point me to an example of this issue in your code, I could take a look to see how I can improve that using Creusot.

[ruth561]

I managed to handle it well in the DBM implementation, so I may not be able to provide code immediately. However, if I encounter cases where I can't handle it well in future implementations, I will ask for your assistance.