Mapping creation and indexing

[arnaudgolfouse]

I'm not a fan of the naming of unknown, but I don't really have a better idea.

Also this implies that logic code may create values ex nihilo. I assumed this was what we wanted ; but should we rather have a function

#[logic]
#[trusted]
fn conjure<T>() -> T { dead }

?

[jhjourdan]

Indexing: LGTM.

Creation of an arbitrary mapping: why cannot we use cst in your specific case?

In general, I think a function like your conjure is a good idea. I think there is no reason this should be restricted to Mapping. Actually, I think we should even go further, by having the equivalent of an epsilon function in Creusot, which would essentially let us eliminate existential quantifiers in ghost code.

[arnaudgolfouse]

Creation of an arbitrary mapping: why cannot we use cst in your specific case?

Because the type of values of that mapping is a generic type T, so I cannot create a value of type T (unless of course we add conjure).

In general, I think a function like your conjure is a good idea.

I'll add it then! We can think about an epsilon function later, but yes it is something that I wanted occasionally.

[arnaudgolfouse]

Btw what is our position on uninhabited types?

[jhjourdan]

Btw what is our position on uninhabited types?

Smt solvers and why3 don't support uninhabited types, they assume that all types are inhabited. It is rather heavy to encode uninhabited types in these tools, so I prefer not supporting them either.

This is the main reason why we don't encode type invariants as subset types.

[jhjourdan]

I'll add it then! We can think about an epsilon function later, but yes it is something that I wanted occasionally.

Why waiting for epsilon ? I don't expect it to be much more difficult than conjure, and I'd prefer not having two redundant features in the future.