Distinction between spec and impl types

[txiang61]

Currently there are no distinction between a specification enum and a implementation enum in Verus and the well-formedness check is applied to both types.

pub enum ListSpec {
    Nil,
    Con {v: Seq<char>, rest: Box<ListSpec>}
}

pub enum List {
    Nil,
    Con {
        v: std::string::String,
        rest: Box<List>
    }
}

impl View for List {
    type V = ListSpec;

    open spec fn view(&self) -> Self::V {
        self.view_impl()
    }
}

impl List {
    pub open spec fn view_impl(&self) -> ListSpec
        decreases self,
    {
        match self {
            Self::Nil => ListSpec::Nil,
            Self::Con { v, rest } => ListSpec::Con {
                v: v.view(),
                rest: Box::new(rest.view_impl())
            },
        }
    }
}

Things like Box are implementation detail and would be great if we can strip it out from the implementation for reasoning.

Suggestion:

pub spec enum ListSpec {
    Nil,
    Con {v: Seq<char>, rest: ListSpec}
}

[y1ca1]

Agree that things like Box is unnecessary for structural, ghost types, just like technically you don't need to use &self in ghost spec fns.

Interestingly, Verus does already support the ghost keyword and one can define ghost types like

ghost enum MyEnum {
    ...
}

So maybe currently the well-formedness checks for ghost types is being conservative.

[parno]

FWIW, @tjhance has done some exploratory work on this topic here:
https://github.com/verus-lang/verus/blob/slightly-less-crazy-refactor/source/rust_verify/src/spec_typeck/README.md
but it's still quite early.