Logical functions aliases, reloaded

[mcoulmance]

This PR continues the work started by @dianegolfouse in #1346. It adds two new features to creusot:

• logic aliases between program functions and logic functions. A logic alias can be specified either by a
  path to a logic function, or by a call to a logic function
• hybrid functions, which is basically a mechanism to simultaneously declare a program function and an identical logic
  function, with a logic alias between them.

Example

// An alias defined with a path to a logic function
#[logic(open)]
fn is_zero_logic(a: i64) -> bool {
    a == 0i64
}

#[logic_alias(is_zero_logic)]
fn is_zero(x: i64) -> bool {
    x == 0
}



// An alias defined with a call to a logic function
#[logic(open)]
fn is_one_logic(a: Int) -> bool {
    pearlite! {
        a == 1
    }
}

#[logic_alias(is_one_logic(x@))]
fn is_one(x: i64) -> i64 {
    x == 1
}


// A hybrid declaration
#[hybrid]
#[requires(x@ < i64::MAX@ - 1)]
fn add_one(x: i64) -> i64 {
    x + 1i64
}


fn foo() {
  let mut i = 0;
  proof_assert!(is_zero(i));
  i = add_one(i);
  proof_assert!(is_one(i));
  proof_assert!(add_one(i) == 2i64);
}

It is still quite experimental, but it is already possible to use aliasing in traits. I would like to open a discussion on this PR about the semantic we want to give to aliasing in traits, since it is a pretty important design decision (see header doc in creusot/src/logic_alias.rs).