Causality loop with ghosts and equality

[jhjourdan]

This is unsound:

extern crate creusot_contracts;

use creusot_contracts::*;

#[ensures(false)]
pub fn bad() {
    let mut x = gh! { true };
    let b = &mut x;
    let bg = gh! { b };
    proof_assert! { ***bg == true && *^*bg == true };
    let evil = &mut x;
    proof_assert! { (evil == *bg) == (*^evil == true) }; // Since **evil == true
    *evil = gh! { if evil == *bg { false } else { true } };
    proof_assert! { **evil == !*^evil };
    // Resolve evil
    proof_assert! { **evil == !**evil }; //BOOM !
}

[xldenis]

The real solution is something we should have done a long time ago. Ghost could should be Rust code.

[xldenis]

In that world, none of these issues could occur and ghost code would have much clearer and safer semantics. Additional notions of specifications-in-your-code could be added separately from ghost code

[jhjourdan]

Additional notions of specifications-in-your-code could be added separately from ghost code

Well but then how do you call that? Won't you have the same soundness problems?

[xldenis]

Well but then how do you call that?

I don't know

Won't you have the same soundness problems?

Maybe, but we can worry about that when we can clearly define this not-quite-ghost-specification-code

[dewert99]

The real solution is something we should have done a long time ago. Ghost could should be Rust code.

I'm not exactly sure what you mean by this.

Do you mean handling ghosts with trusted specifications? somewhat like:

impl<T> Ghost<T> {
  #[ensures(*result = t)]
  fn new(t: T) -> Self;

  #[requires(f.precondition((*self,)))]
  #[ensures(f.postcondition_once((*self,), *result))]
  fn map<U>(self, f: impl FnOnce(T) -> U) -> Ghost<U>;
}

This seems like it would be somewhat limiting since values must be consumed to create ghosts and this version is also unsound:

fn unsound() {
  let g = Ghost::new(());
  let mut x = false;
  let g2 = g.map(|()| *x = true);
  assert!(x); //This would be verified, but panic when actually run
}

Or do you mean limiting ghost functions to only all rust expressions inside them? This would involve not allowing equality, quantifiers, and potentially the "logical reborrow/unnesting" (#606) as I'm not totally sure how that works.

This seems like a good idea and is in line with what I was able to prove to be allowable in ghost functions:

• constructors of structs and enums
• basic pattern matching on structs and enums
• operations only involving primitives (ints and bools)
• if expressions
• box dereference
• shared reference dereference
• mutable reference current operator

[dewert99]

It would also be important to not allow blocked variables to be used in gh!: eg.

fn bad() {
    let mut a = gh!(true);
    let mut c = &mut a;
    *c = gh!(!*a);
}

This would also help with #873

[xldenis]

Or do you mean limiting ghost functions to only all rust expressions inside them? This would involve not allowing equality, quantifiers, and potentially the "logical reborrow/unnesting" (https://github.com/xldenis/creusot/pull/606) as I'm not totally sure how that works.

Yea, my point is that "ghost code" as used in other languages like Why3/Dafny/Frama-C etc.. is just the program language but erased at compile time, nothing more. If we also want to allow a notion of "Iris-style" ghost code that's a different subject imo.

It would also be important to not allow blocked variables to be used in gh!: eg.

This is definitely on the list.

[dewert99]

Would converting something into a Ghost consume it?

[xldenis]

Hmm interesting question naively I would say no otherwise it greatly limits what you can do and breaks non-interference, but not consuming also seems precarious in it's own ways.

What are your thoughts on it?

[dewert99]

I would think no, ideally, ghosts would work roughly the same as they do now but with more restrictions on what is allowed inside of a ghost function like I mentioned above (and with the restriction about mentioning blocked variables which you will be doing anyway).

Eventually, if it is useful I could try and prove the "logical reborrow/unnesting" operations. I'm now guessing that equality could be sound if mutable references weren't injective but I would have to try and prove that as well.

Sorry that I forgot about equality when I was trying to prove soundness for ghosts.

[voidc]

The unsound example above would be impossible without extensionality for mutable references, right? Since *^evil == true would no longer imply evil == *bg.

[jhjourdan]

The unsound example above would be impossible without extensionality for mutable references, right? Since ^evil == true would no longer imply evil == bg.

Indeed, that's right in this specific example. Are we sure that removing extensionality is enough to prevent polymorphic equality from leaking information about the prophecy to ghost code? That seems a bit magical to me, but why not.

[voidc]

I think it is. For soundness we have to prevent prophecies from ending up in the current value of mutable references. Prophecies are accessible through the final value operator, as the value of blocked variables, or through extensionality on the reference.

[dewert99]

While I haven't tried to prove it yet, I think @voidc is correct. I think at the RustHornBelt level, this would work by representing mutable references as a triple of their current value, final value, and the integer index of the prophecy variable ξi. This way the two mutable references would equal iff they have the same prophecy variable and current value. Comparing the prophecy variable indices would be independent of the prophecy assignment π, but if they were equal it would imply the final values are equal as well. If we inductively assume that the current value comparison also didn't depend on π, comparing two mutable references for equality could be done non-prophetically.

[xldenis]

As @dewert99 has noticed, we could also encode this by making borrows a triplet and adding a non-deterministic "id" tag to each one.

However, another question I have is what do we gain from removing extensionality? Are there any meaningful increases in expressivity if we relax this constraint?

[jhjourdan]

FTR, I have a variant of the counter example which is incompatible with an "addr" field representing the pointer physical address, and with an "id" field which would be systematically inherited when reborrowing:

#[ensures(false)]
pub fn bad() {
    let mut x = gh! { true };
    let b = &mut x;
    let bg = gh! { b };
    let b2 = &mut *b;
    let b2g = gh! { b2 };
    // Resolve b2
    proof_assert! { ***b2g == true && *^*b2g == true };
    *b = gh! { if *bg == *b2g /* Same current value (true), same addr, same id */ { false } else { true } };
    proof_assert! { **b == !*^b };
    // Resolve b
    proof_assert! { **b == !**b }; //BOOM !
}

[jhjourdan]

This should be fixed by #912.