Logical functions aliases

[dianegolfouse]

Example

// In `creusot_contracts`

impl<K, V> FMap<K, V> {
    #[trusted]
    #[logic]
    #[ensures(result >= 0)]
    pub fn len_logic(self) -> Int {
        dead
    }

    #[trusted]
    #[pure]
    #[has_logical_alias(Self::len_logic)]
    pub fn len(self) -> Int {
        panic!()
    }
}

// User code

pub fn foo() {
    let mut m = FMap::new();
    proof_assert!(m.len() == 0); // logic call
    ghost! {
        m.insert_ghost(1int, 1int);
        let l = m.len(); // program (ghost) call
        proof_assert!(l == 1);
        m.insert_ghost(2int, 2int);
        proof_assert!(m.len() == 2);
    };
}

[jhjourdan]

This is a very interesting feature, howeer, there are a few important parts missing:

• Support for aliases in traits. A simple constraint could be to force the alias to belong to the same trait. Then, we sould add a refinement check for implementations (i.e., implementors declare compatible aliases).

• Uses in creusot_contracts, to get rid of all the _ghost and _logic functions.

• Use this for Ghost::Deref, Rc::Deref, Snapshot::Deref, etc... and get rid of the special cases for this in Creusot's code.

[jhjourdan]

This means that you force the method to have a body, which forbids logical aliases for trait methods. This seems restrictive. Is this intended? A simple fix may be to use FnOrMethod here instead.

[jhjourdan]

This assumes that the pattern is also a term, which is not always the case.

This is probably fine in this case, but it would be better to detect this in the macro, and emit an error.

[jhjourdan]

Cannot we simply reject them?

[jhjourdan]

Why don't we check the equality of constant param names, too? It seems weird to do that for types and lifetimes, but not for constants.

[jhjourdan]

Doing that directly in the loop would be clearer and shorter.

[jhjourdan]

From itertools:

for (prog_arg, logic_arg) in program_subst.zip_longest(logic_subst) { ... }

[jhjourdan]

Perhaps we could ask Maël Coulmance to work on this?

[xldenis]

What is the current thinking on this? I think this would be really nice and would really contribute to making proofs & specs easier to follow by getting rid of ubioquitous "_logic" suffixes, especially if there's a macro to help you automatically generate these aliases.