feat: support quantifiers `forall` and `exists`

[mkovaxx]

The main goal here is to support quantifiers in specs for static analysis, because it's unclear how they'd be runtime checked.

Quantifiers are necessary to express e.g. algebraic properties.

For example, to specify the concept of a group, we should be able to write the following:

#[spec(
    maintains: [
        // The group has an identity element.
        forall(|x: Self| x.op(&Self::IDENTITY) == x && Self::IDENTITY.op(&x) == x),
        // The binary operation is associative.
        forall(|x: Self, y: Self, z: Self| x.op(&y).op(&z) == x.op(&y.op(&z))),
    ],
)]
trait Group: Eq + PartialEq + Sized {
    const IDENTITY: Self;

    fn op(&self, other: &Self) -> Self;

    #[spec(
        ensures: [
            self.op(output) == Self::IDENTITY,
            output.op(self) == Self::IDENTITY,
        ],
    )]
    fn inverse(&self) -> Self;
}

Note that associativity involves 3 variables, even though op only has two inputs.

[mkovaxx]

Implementation Sketch

Anodized would provide a crate (e.g. anodized-logic) to include the following definitions:

pub fn forall<T, P: Predicate<T>>(predicate: P) -> bool {
    unimplemented!("Runtime checks are not supported for quantifiers.")
}

pub fn exists<T, P: Predicate<T>>(predicate: P) -> bool {
    unimplemented!("Runtime checks are not supported for quantifiers.")
}

trait Predicate<T> {}

impl<P> Predicate<()> for P where P: Fn() -> bool {}
impl<P, T1> Predicate<(T1,)> for P where P: Fn(T1) -> bool {}
impl<P, T1, T2> Predicate<(T1, T2)> for P where P: Fn(T1, T2) -> bool {}
impl<P, T1, T2, T3> Predicate<(T1, T2, T3)> for P where P: Fn(T1, T2, T3) -> bool {}
impl<P, T1, T2, T3, T4> Predicate<(T1, T2, T3, T4)> for P where P: Fn(T1, T2, T3, T4) -> bool {}
// ... and so on, up to some number of arguments, say 10.