Skip to main content

Cmp

Comparison is expressed in Rust through the traits PartialEq and Eq. ECLAIR has analogues of these that explicitly mention the compiler COM to specify the computational environment where comparison occurs. As in Rust, Eq is simply a sub-trait of PartialEq used to indicate that a partial equivalence relation is actually a true equivalence relation.

The ECLAIR equivalent of PartialEq is

/// Partial Equivalence Relations
pub trait PartialEq<Rhs, COM = ()>
where
COM: Has<bool>,
{
/// Returns `true` if `self` and `rhs` are equal.
fn eq(&self, rhs: &Rhs, compiler: &mut COM) -> Bool<COM>;

/// Returns `true` if `self` and `rhs` are not equal.
fn ne(&self, other: &Rhs, compiler: &mut COM) -> Bool<COM>
where
Bool<COM>: Not<COM, Output = Bool<COM>>,
{
self.eq(other, compiler).not(compiler)
}

/// Asserts that `self` and `rhs` are equal.
///
/// # Implementation Note
///
/// This method is an optimization path for the case when
/// comparing for equality and then asserting is more expensive
/// than a custom assertion.
fn assert_equal(&self, rhs: &Rhs, compiler: &mut COM)
where
COM: Assert,
{
let are_equal = self.eq(rhs, compiler);
compiler.assert(&are_equal);
}
}

As with most traits in the ECLAIR Standard Library, PartialEq differs from its pure Rust equivalent mainly by the addition of the COM type and an argument compiler: &mut COM in the function signatures. This allows ECLAIR to generate appropriate constraints whenever COM specifies a ZK proving system.

For example, when an ECLAIR circuit contains the line

output = lhs.eq(rhs, &mut compiler);

this means that compiler will allocate a variable output of COM's boolean type and constraint output to carry the truth value of lhs == rhs.

Besides the compiler argument, the main difference from Rust's PartialEq trait is the added method fn assert_equal. The reason for including this method is that in some ZK proving systems it may be possible to assert equality using fewer constraints than separate calls to PartialEq::eq and Assert::assert. In such situations, the implementation of PartialEq<COM> should replace the blanket implementation here with the more optimized version. This is an example of the sort low-level, COM-specific optimizations that ECLAIR allows.