ark-r1cs-std

The Boolean<F> type represents a boolean value in a constraint system, ensuring it is either zero or one. It can represent either a variable (Boolean::Var(AllocatedBool<F>)) or a constant (Boolean::Constant(bool)). This abstraction allows you to perform boolean logic and conversions within a R1CS constraint system.

Key capabilities include:

• Creating constant booleans (TRUE, FALSE).
• Converting bitwise representations (little-endian) of field elements into FpVar<F> variables.
• Converting boolean vectors from raw bytes.
• Extracting underlying Variable or LinearCombination representations for use in arithmetic constraints.

use ark_r1cs_std::prelude::*;n
use ark_test_curves::bls12_381::Fr;

// Example: Creating and enforcing constant booleans
let cs = ConstraintSystem::<Fr>::new_ref();
let t = Boolean::<Fr>::TRUE;
let f = Boolean::<Fr>::FALSE;

t.enforce_equal(&Boolean::TRUE)?;
f.enforce_equal(&Boolean::constant(false))?;

The EqGadget<F> trait provides a standardized way to compare two R1CS variables (or collections of variables) for equality or inequality within a circuit. It can be implemented for individual variables, slices [T], Vec<T>, and fixed-size arrays [T; N], provided the underlying type T implements EqGadget<F> and GR1CSVar<F>.

Key methods include:

• is_eq(&self, other: &Self): Returns a Boolean<F> representing whether the values are equal.
• is_neq(&self, other: &Self): Returns a Boolean<F> representing whether the values are not equal.
• enforce_equal(&self, other: &Self): Immediately enforces that the two variables are equal by adding constraints to the circuit.
• enforce_not_equal(&self, other: &Self): Immediately enforces that the two variables are not equal.
• conditional_enforce_equal(&self, other: &Self, should_enforce: &Boolean<F>): Enforces equality only if the should_enforce boolean variable is true.

use crate::prelude::*;

// Assuming `var_a` and `var_b` are types implementing EqGadget
// such as Boolean or other R1CS variables.

// 1. Get a boolean variable representing equality
let is_equal: Boolean<F> = var_a.is_eq(&var_b)?;

// 2. Enforce equality directly
var_a.enforce_equal(&var_b)?;

// 3. Enforce equality conditionally based on another boolean variable
var_a.conditional_enforce_equal(&var_b, &condition_var)?;

When working with elliptic curve points on Short Weierstrass curves in R1CS, ProjectiveVar is the recommended gadget. It uses projective coordinates $(x, y, z)$ and implements complete addition formulae, making it safer and more robust than affine representations which can lead to unsatisfiable or underconstrained systems if a point is equal to zero.

Key features include:

• Complete Addition: Supports adding any two points, including the identity (point at infinity).
• Scalar Multiplication: Supports multiplying a point by a scalar (represented as a little-endian Boolean bit vector).
• Coordinate Conversion: Can be converted to an AffineVar representation.

// Example of creating a ProjectiveVar (conceptual)
let point = ProjectiveVar::new(x_var, y_var, z_var);

// Converting to affine form
let affine_point = point.to_affine()?;

// Scalar multiplication
let scalar_bits = vec![bit1, bit2, ...];
let result = point.scalar_mul_le(scalar_bits.iter())?;

To avoid boilerplate when creating non-deterministic advice (hints), use new_variable_with_inferred_mode. This method infers the mode from the ConstraintSystem associated with the provided Namespace. If the Namespace is empty (no ConstraintSystem), it allocates a Constant; if it contains a ConstraintSystem, it allocates a Witness.

Example of computing division using inferred mode for a hint variable:

use ark_ff::PrimeField;
use ark_r1cs_std::{alloc::AllocVar, fields::{fp::FpVar, FieldVar}, GR1CSVar};
use ark_relations::gr1cs::SynthesisError;

fn div<F: PrimeField>(x_var: &FpVar<F>, y_var: &FpVar<F>) -> Result<FpVar<F>, SynthesisError> {
  // Get the constraint system from existing variables if available
  let cs = x_var.cs().or(y_var.cs());
  
  // z_var will be a Witness if x_var or y_var are witnesses, otherwise a Constant
  let z_var = FpVar::new_variable_with_inferred_mode(cs, || Ok(x_var.value()? / y_var.value()?))?;
  
  // Verify the relationship: z * y = x
  z_var.mul_equals(y_var, x_var)?;
  
  Ok(z_var)
}