Support for unsafe operations that Creusot can support

[ia0]

Creusot probably can't support unsafe operations with requirements mentioning the memory or aliasing model, but it should be able to support purely arithmetic safety requirements. For example slice::get_unchecked(), u64::unchecked_add(), or String::from_utf8_unchecked(). A related closed issue is #36 which actually mentions get_unchecked as something that could be soundly supported.

This issue is about whether such unsafe operations would be something Creusot wants to support.

[xldenis]

I see no issue adding support for those! in fact it should really just be a matter of writing down the specifications and adding them to the standard library. Do you have a specific use case / set of methods in mind?

[ia0]

Yes, I need the following methods:

• https://doc.rust-lang.org/nightly/core/primitive.slice.html#method.get_unchecked
• https://doc.rust-lang.org/nightly/core/primitive.slice.html#method.get_unchecked_mut
• https://doc.rust-lang.org/nightly/core/str/fn.from_utf8_unchecked.html
• https://doc.rust-lang.org/nightly/alloc/string/struct.String.html#method.from_utf8_unchecked
• https://doc.rust-lang.org/nightly/alloc/string/struct.String.html#method.as_mut_vec

[xldenis]

For the string methods what specifications do you expect? Those methods have tricky safety obligations relating to the utf-8 validity of the contents.

[xldenis]

Worst case for those methods, I can give you the code to add those specifications locally to your project. get_unchecked_* should definitely be added to creusot though.

[ia0]

For the string methods what specifications do you expect? Those methods have tricky safety obligations relating to the utf-8 validity of the contents.

Good question. I actually need much simpler (and stronger) specifications than the real ones.

For from_utf8_unchecked() (it should be similar for str and String, so just showing str), I need:

// Requires that input is ASCII, which is trivially UTF-8.
#[requires(forall<i: Int> i < v@.len() ==> v@[i]@ < 128)]
// Ensures that it's the identity function.
#[ensures(result@.len() == v@.len())]
#[ensures(forall<i: Int> i < v@.len() ==> result@[i]@ == v@[i]@)]
pub const unsafe fn from_utf8_unchecked(v: &[u8]) -> &str;

A first issue here is that char doesn't implement View. I filed #1380 for that.

For as_mut_vec(), I would expect something like this:

#[ensures(
    // Requires that only ASCII is pushed (in particular the prefix is not modified).
    ((*result)@.len() <= (^result)@.len()
     && forall<i: Int> i < (*result)@.len() ==> (^result)@[i]@ == (*result)@[i]@
     && forall<i: Int> (*result)@.len() <= i && i < (^result)@.len() ==> (^result)@[i]@ < 128)
    ==>
    // Ensures that it's the identity function (trying to avoid talking about UTF-8).
    ((^self)@.len() == (*self)@.len() + (^result)@.len() - (*result)@.len()
     && forall<i: Int> i < (*self)@.len() ==> (^self)@[i]@ == (*self)@[i]@
     && forall<i: Int> (*self)@.len() <= i && i < (^self)@.len() ==>
          (^self)@[i]@ == (^result)@[(*result)@.len() + i - (*self)@.len()]@)
)]
pub unsafe fn as_mut_vec(&mut self) -> &mut Vec<u8>;

A second issue here is that the function is unsafe but doesn't have requirements. As far as I can tell, the requirements can't be expressed in Creusot, since it's about the prophecy of the result, which is not in scope for requires clauses. Is there a way to make sure this function is only called when it's safety precondition holds (without adding a proof_assert!() after each function call for the requirements)? Ideally some post_requires clause would exist (factoring out the requirements into a predicate to use it both in the ensures and post_requires clauses).

Worst case for those methods, I can give you the code to add those specifications locally to your project. get_unchecked_* should definitely be added to creusot though.

Yes, given that those contracts are stronger than the correctness contracts of those functions, I guess it makes sense to have them local to my project.

[xldenis]

Ideally some post_requires clause would exist (factoring out the requirements into a predicate to use it both in the ensures and post_requires clauses).

This is what we refer to as "after_expiry" or a pledge. Tagging @arnaudgolfouse since we talked about this last week.

[xldenis]

#[requires(forall<i: Int> i < [email protected]() ==> v@[i]@ < 128)]

I think that for this to work the View instance needs to be a little more sophisticated than what you suggested, merely because its value needs to be related to literal chars. Not a huge lift but a little bit of work to make sure it works well.

[xldenis]

To axiomatize the string methods you just need to add an extern_spec block with your specs like the following:

extern_spec! {
    mod std {
        mod string {
            impl String {
                #[requires(...)]
                unsafe fn from_utf8_unchecked(vec: Vec<u8>);
            }
        }
    }
}

[ia0]

This is what we refer to as "after_expiry" or a pledge. Tagging @arnaudgolfouse since we talked about this last week.

Thanks! I guess this is work in progress. I don't see any mention of after_expiry in the creusot repository.

#[requires(forall<i: Int> i < [email protected]() ==> v@[i]@ < 128)]

I think that for this to work the View instance needs to be a little more sophisticated than what you suggested, merely because its value needs to be related to literal chars. Not a huge lift but a little bit of work to make sure it works well.

I'm not sure what you mean. This requirement is about ASCII, which is a subset of Unicode where the UTF-8 encoding is the same as the ASCII encoding, and ASCII values are also the same as their Unicode scalar values. So once char gets a model (see #1381), we'll be able to talk about its Unicode scalar value with to_int which will be equal to the model of u8 for ASCII.

To axiomatize the string methods you just need to add an extern_spec block with your specs like the following:

Thanks! I'll try this when I get time.

[xldenis]

I'm not sure what you mean. This requirement is about ASCII, which is a subset of Unicode where the UTF-8 encoding is the same as the ASCII encoding, and ASCII values are also the same as their Unicode scalar values. So once char gets a model (see #1381), we'll be able to talk about its Unicode scalar value with to_int which will be equal to the model of u8 for ASCII.

What I meant, is that if we simply add an uninterpreted View for char, there's nothing showing that 'c'.to_int() < 127

[xldenis]

That may or may not be a problem for you at this juncture, but if we need to ensure that literal chars have accurate View then that'll be a little trickier.

[ia0]

What I meant, is that if we simply add an uninterpreted View for char, there's nothing showing that 'c'.to_int() < 127

Ah ok, I misunderstood "literal". Indeed, it's not a problem for me. The project doesn't use any literal chars. It actually doesn't use any chars at all (they only come from the model of str and String chosen by Creusot). The project only deals with str and String, and it only relies on the fact that 0u8 .. 128u8 bytes between char boundaries are themselves chars and don't break the overall UTF-8 encoding. In particular, the only char boundaries considered by the project are the beginning and end of any string at any program point in the library.