A Ghost<T> struct field cannot be used as its contents in ensures/ghost! (E0599 no method push/len, E0369 for ==), while a Ghost<T> parameter can #300

Summary

std.rs documents Ghost<T> as "in the logic it is its content, so a specification refers to a Ghost<T> as if it were a T". That holds for a Ghost<T> parameter: a lifted formula function lowers each parameter type to <T as Model>::Ty, and Ghost<T>'s Model impl resolves to the content's model. It does not hold for a Ghost<T> struct field. When the struct's Model::Ty is the struct itself, a formula that projects the field sees Ghost<Seq<Int>>. Ghost<T> only implements Clone, Copy and Model, so push, len and == on the field fail to type-check (E0599, E0369), in ensures and in ghost! bodies alike.

As a result, a ghost history cannot live in the struct it describes and be named by field. It has to be passed through a free function taking a Ghost<T> parameter, or the struct's Model::Ty has to be rewritten as a tuple and the field reached by position (as tests/ui/pass/ghost_field.rs does).

Minimal reproduction

len_only.rs:

use thrust_models::model::{Int, Seq};
use thrust_models::{Ghost, Model};

struct Hist {
    produced: Ghost<Seq<Int>>,
}
impl Model for Hist {
    type Ty = Hist;
}

#[thrust_macros::ensures((*h).produced.len() >= 0)]
fn bump(h: &mut Hist, x: i64) {
    let _ = x;
}

fn main() {
    let mut h = Hist {
        produced: thrust_macros::ghost!(|| -> Seq<Int> { Seq::empty() }),
    };
    bump(&mut h, 1);
}

On main e112206:

$ export LD_LIBRARY_PATH=$(rustc --print sysroot)/lib
$ THRUST_SOLVER=true target/debug/thrust-rustc -Adead_code -Aunused -C debug-assertions=false --edition 2021 len_only.rs
error[E0599]: no method named `len` found for struct `thrust_models::Ghost<T>` in the current scope
   --> len_only.rs:11:40
    |
 11 | #[thrust_macros::ensures((*h).produced.len() >= 0)]
    |                                        ^^^ method not found in `thrust_models::Ghost<thrust_models::model::Seq<thrust_models::model::Int>>`

Replacing the ensures with #[thrust_macros::ensures((!h).produced == (*h).produced)]:

error[E0369]: binary operation `==` cannot be applied to type `thrust_models::Ghost<thrust_models::model::Seq<thrust_models::model::Int>>`
   --> eq_only.rs:11:40
    |
 11 | #[thrust_macros::ensures((!h).produced == (*h).produced)]
    |                          ------------- ^^ ------------- thrust_models::Ghost<thrust_models::model::Seq<thrust_models::model::Int>>

The same happens inside a ghost! body that reads the field, e.g. ghost!(|h: &mut Hist, x: i64| -> Seq<Int> { (*h).produced.push(x) }) (E0599, no method push).

The control passes the frontend. It is the same history passed as a Ghost<T> parameter of a free function, and THRUST_SOLVER=true gets past rustc's type check and analysis to the solver stage:

#[thrust_macros::ensures(result == produced.push(x))]
fn push_produced(produced: Ghost<Seq<Int>>, x: i64) -> Ghost<Seq<Int>> {
    thrust_macros::ghost!(|produced: Ghost<Seq<Int>>, x: i64| -> Seq<Int> { produced.push(x) })
}

fn bump(h: &mut Hist, x: i64) {
    h.produced = push_produced(h.produced, x);
}

Seven variants (field in ensures, field in ghost!, a local rebound from the field, the parameter control) with their transcripts: https://github.com/coeff-aij/thrust/tree/71e759d41c1dd90daa8d712a976487d5e0beefc4/repro/ghost-field-contents. On e112206 every field variant fails with E0599/E0369 as above. The two controls, ctrl_param.rs and ctrl_local.rs (which rebinds the field to a local first), pass the frontend.

Expected

A Ghost<T> field used in a specification is typed as its content, as a Ghost<T> parameter is.

Notes

The refinement side already builds a Ghost<T> field at the content's sort. Only the surface typing of the formula is missing. A fork has one possible fix in coeff-aij@4fc9b1a. It gives Ghost<T> a Deref to <T as Model>::Ty and a PartialEq against any type with the same model, both #[thrust::ignored] stand-ins in std.rs, plus the matching arm in the annotation lowering. It panics if executable code (not a specification) calls something that relies on them.

I checked the tracker for "Ghost"/"ghost" and found no existing issue.