Bugs about ghost code.

[jhjourdan]

Consider this piece of code:

extern crate creusot_contracts;

use creusot_contracts::*;

struct S {
    g: Ghost<i32>
}

#[logic]
fn prophecy(x: &mut S) -> i32 {
    pearlite!{ *(^x).g }
}

pub fn f() {
    let b = &mut S{ g:ghost! { 1 } };
    b.g = ghost!{ (prophecy(b) + 1) };
    proof_assert! { false }
}

There are three issues here: 1- I need to put parentheses in ghost!{ (prophecy(b) + 1) };, otherwise I get weird type errors. This sounds like an easy to fix bug in the ghost macro.

2- The Ghost in struct S is not translated into a ghost field. Similarly, a borrow of a ghost is not translated into anything Ghost, which is blocking since then we cannot make use of it.

In my view, the way we should solve this issue is by not using the ghost keyword in WhyML, and make sure that Ghost is indeed a monad that cannot be escaped, and make this check in Creusot.

3- Once this code compile correctly, it exhibits a causality loop. Using logic functions such as prophecy should be forbidden in ghost code.

[dewert99]

Now that #488 has been merged this seems to have become a soundness issue. However, I'm not sure it would be okay to make logic functions forbidden in ghost code (eg. The desugaring of a for loop currently includes produced = ghost!(produced.push(e)) which calls Ghost::deref and Seq::push both of which are logic functions). Currently, there doesn't seem to be much difference between predicates and logic functions (that return bool), so I wonder if it would work to forbid calling predicates in logic functions and ghost code, and restrict ^/creusot_contracts::stubs::fin to being used in predicates.

[xldenis]

Now that https://github.com/xldenis/creusot/pull/488 has been merged this seems to have become a soundness issue.

Yea, the example given above demonstrates that. Allowing access to prophetic information in ghost code is problematic.

I'm leaving on vacation next week, but when I get back I think the most crucial concern will be overhauling ghost code and placing it on a firm theoretical foundation. There are several other questions that I want to answer simultaneously:

1. Should ghost code have ownership typing?
2. Should ghost code have access to logical types and values?
3. Related to the previous questions: should there be a 'logic ghost code' and a 'linear ghost code'?
4. How do we state the non-interference / erasure theorems of ghost code in the context of Rust / RustHornBelt?
5. How can we develop a better ghost! macro and Ghost type (currently you have to annotate all bindings with type information).

If you would like to help with this redesign, your input is welcome!

-- Re: predicates vs functions

Currently, there doesn't seem to be much difference between predicates and logic functions (that return bool)

The reason for the existence of predicate is to target why3's predicate construct, but I've never gotten a clear answer from Why3 devs about the reason for the need to distinguish the two.

[xldenis]

Currently, there doesn't seem to be much difference between predicates and logic functions (that return bool), so I wonder if it would work to forbid calling predicates in logic functions and ghost code, and restrict ^/creusot_contracts::stubs::fin to being used in predicates.

I rather like this solution, I don't think i've ever needed prophetic information in a logical function, though more generally, I think there's a real need to sit down and understand ghost code, it's rules and impact on soundness, even if we ban this specific hole.

[xldenis]

From @dewert99

enum Bad<'a> {
    None,
    Some(Ghost<&'a mut Bad<'a>>)
}

fn test_bad() {
    let mut x = Bad::None;
    let m = &mut x;
    let g = ghost!(m);
    *m = Bad::Some(ghost!(*g));
    proof_assert!(*m == Bad::Some(g));
    proof_assert!(^(*g) == ^m);
    let _ = m;
    proof_assert!(^(*g) == Bad::Some(g));
}

[xldenis]

This should be fixed now, right?

[jhjourdan]

Indeed.