Am I doing this right? (Generic function on signed ints)

[ethanbb]

First of all, this is an awesome tool. It's been a bit tricky to get started, especially since I'm also new to Rust as a whole, but I'm interested in the space and you've shown this has a lot of potential with the verified SAT solver, so I'm determined to muddle through it.

I wanted to try to implement the abs function generically over signed integers as an exercise. I'm now realizing this was maybe not the most approachable exercise, since to do generics in Rust you have to deal with traits, and to use them with Creusot they all have to have an extern_spec. But I eventually came up with something that works below. I have some lingering questions though:

• When exactly does one have to use DeepModel/deep_model() and when is View/@ enough? Midway through, I saw Cannot prove 02_linear_search.rs #993 and started using DeepModel for everything, which helped a lot, but it is more verbose.
• I added this NegCheckable trait because I kept getting an error when trying to use functions from existing traits in the precondition. I realized I needed a logic function or predicate (btw it seems like predicate has been removed?), so I made a sub-trait of Neg to provide that. Is this the best way to do it or am I missing something? Can existing functions be turned into logic functions by an extern_spec or similar?

use creusot_contracts::*;
use creusot_contracts::std::ops::Neg;
use num_traits::{identities::Zero, sign::Signed, int::PrimInt};


pub trait NegCheckable: Neg<Output = Self> {
    #[logic]
    pub fn is_negatable(&self) -> bool;
}

macro_rules! impl_negcheckable_signed {
    ($($t:ty),*) => {
        $(
            impl NegCheckable for $t {
                #[logic]
                fn is_negatable(&self) -> bool { *self > <$t>::MIN }
            }
        )*
    };
}

impl_negcheckable_signed!(i8, i16, i32, i64, i128, isize);


extern_spec! {
    mod std {
        mod ops {
            trait Neg
            where
                Self: DeepModel<DeepModelTy = Int> + Signed + NegCheckable,
                <Self as Neg>::Output: DeepModel<DeepModelTy = Int>
            {
                #[requires(self.is_negatable())]
                #[ensures(result.deep_model() == -self.deep_model())]
                fn neg(self) -> <Self as Neg>::Output;
            }
        }
    }

    mod num_traits {
        mod identities {
            trait Zero 
            where
                Self: DeepModel<DeepModelTy = Int>
            {
                #[ensures(result.deep_model() == 0)]
                fn zero() -> Self;
            }
        }
    }
}


#[requires(x.is_negatable())]
#[ensures(result.deep_model() >= 0)]
#[ensures(result.deep_model() == x.deep_model() || result.deep_model() == -x.deep_model())]
fn abs<T>(x: T) -> T
where
    T: NegCheckable + PrimInt + Signed + Zero + DeepModel<DeepModelTy = Int>
{
    if x < T::zero() {
        -x
    } else {
        x
    }
}

[jhjourdan]

Hi @ethanbb !

I'm glad you like our work! Don"t hesitate to ask more questions, we will be happy to answer! Indeed, you did not start with the simplest exercise! But since you tried, I will try to answer your questions.

• When exactly does one have to use DeepModel/deep_model() and when is View/@ enough? Midway through, I saw Cannot prove 02_linear_search.rs #993 and started using DeepModel for everything, which helped a lot, but it is more verbose.

View is just the trait used behind the @ notation. Nothing more, nothing less. It is useful, because we often want to speak about "the logical value of" a program type, and it is convenient to have a short notation for that. But it has no "generic" meaning whatsoever, it is simply a convention. In many cases, the view of a type is needed, because the program type contains more information than its canonical logic representation. For example, a vector has a capacity, but its logical value is just a sequence, and in most of the applications, we let Vec manage capicities by itself. Another example is a BTreeMap or any other map represented using trees: what the user is interested in is the mapping represented by the data structure, but the data structure contains more information (such as the tree structure: one mapping can be represented in several different ways).

On the other hand, DeepModel is the type representing the information used by PartialEq to compare objects. I.e., partial_eq will return true if and only if the deep model of its parameters are equal. This has implications on many other traits, because many other traits are required to be compatible with partial_eq. So, PartialOrd compares deep models, etc... It is indeed rather verbose and should only be used when some kind of comparison is involved (in the large sense: equating, ordering, computing hashes, ...).

In many simple types, these two notions coincide. For example, the deep models and views of any integer type coincide. But it differs for complex types: the view of a Vec is the sequence of the program values it contains, while its deep model is the sequence of the deep models of these values (this recursive nature is the reason why we call it "deep").

Your case is a bit peculiar, because, since you are using integers, deep model and view coincide, but Creusot does not know that, because it only sees a generic type variable, for which they don't necessarily coincide. Since you are using DeepModel in abs, because you are indeed comparing stuff (x < T::zero()), then you are left to either requiring somewhere that view and deep model coincide, or use deep model everywhere. I agree, this is not ideal.

btw it seems like predicate has been removed?

Indeed, we removed it recently (in #1594), because we kept forgetting to use it. Instead, a function returning bool is automatically treated as a predicate. In the vast majority of cases, this is what you want, and in the other cases (where you actually want a function that returns a value in a 2-valued type), it's not clear that we loose expressive power of SMT solvers.

so I made a sub-trait of Neg to provide that. Is this the best way to do it or am I missing something?

That is indeed a valid way of doing this, if you really want to have a generic version of abs (instead of a different abs method for every signed type), and you don't want what I will propose bellow.

Can existing functions be turned into logic functions by an extern_spec or similar?

Yes and no. It is not possible to turn a program function into a logic function (yet). One issue is with termination: you need to make sure that the program function always terminates, for example. Something like this could be possible for #[pure] functions, and const values will soon be usable in logic specifications (see #1539).

That being said, you can always refer to the pre- and post-condition of any function. So, in your case, a possibility is to specify abs thanks to the pre- and post-condition of <, zero and neg, which will be rather verbose, but exactly as expressive. For example, you can refer to the pre-condition of neg with T::neg.precondition((x,)), and to its post-condition as T::neg.postcondition((x,), result).

The advantage of this technique is that you don't need to add a generic extern_spec for the Neg trait, you only need to specify its implementations. This is a good thing, because you don't want to force implementations of Neg to actually perform the negation of an integer type (i.e., it can work on floats, rationals...). You only need to add extern specs for its implementations, which is much more acceptable.

(Note that it will not work out of the box, because, as you noticed, creusot-contracts does not have extern specs for integr operations of primitive types. Feel free to open a pull request for that.)

You may answer that it's not quite satisfactory, because the specification of abs (or any other complicated integer-based function that you will build on top of it) will not say that it returns the absolute value, but rather that it does a sequence of operations (i.e., comparing to zero, and negating if necessary). For abs, it is still tractable, but for more complicated functions, it will be too verbose. Instead, you may want to add a new trait SignedSpec, which says that Self is a type, which implements all the usual integer operations, and add some laws stating that the specifications of these operation are as expected.

[jhjourdan]

Edit: one more question, if I did use the abs_allowed pattern, is it necessary to repeat that precondition Self::abs_allowed() in each implementer, or will it be inherited/dispatched correctly? It seems like it could still be a useful pattern in cases where the precondition might be complicated, although maybe there are more idiomatic solutions to that.

Yes, you need to repeat it. And I agree with you that Creusot should have a mechanism to avoid repeating specs.

[jhjourdan]

Also while I'm asking questions, is there any way to mark an external function as "pure" or "logic" in an extern spec so that it can be used in a logic context? That's a roadblock I keep running into.

You can mark an extern spec as being #[pure], but it does not make sense for #[logic], since, logic functions are a Creusot concept and extern specs are designed for libraries which do not have Creusot specifications.

Edit: alright I can see why this wouldn't be feasible. You would have to find a way to express what you want in terms of the function's precondition and/or postcondition, right?

Sorry, I don't understand your point

[ethanbb]

Sorry I was unclear, I just realized myself that it doesn't make sense for #[logic], and was thinking there may be a way to work around calling the function by referring to its postcondition in some cases.

[ethanbb]

OK sorry to ask so many questions. When you get the chance: what is pure actually? Looking through issues it looks like historically pure functions could be used in both logic and non-logic context, and that seems really useful, but they were almost removed at one point? But now if I try to use them in a spec I get an error.

Edit: I guess it's just about ghost code? Sorry don't know how I missed that in the manual, I think I have my answer.

[jhjourdan]

We once wanted to have a notion of function that could be both logic and program. For various reasons, we know think this is not such a great idea. We have another proposal in #1346, that would allow us to overload the name of a function in logic context and in program context. But this is just a project that we have not implemented yet.

Nowadays, #[pure] annotate program functions that can be used in both program and ghost context. They are guaranteed to always terminate and always have a defined semantics. A good example of non-pure function is Vec::push, which can panic because of OOM, but has no precondition, because Creusot gave up on verifying OOM conditions (this is just not realistic to check this). However, it is unsound to consider Vec::push pure, because it does not have a defined semantics in the case the length of the vector overflows usize::MAX.