circuit-cas

A computer algebra system in Rust for algebraic circuit verification over polynomial rings with integer coefficients.

Overview

circuit-cas provides two main layers:

• poly — multivariate polynomials over ℤ, Gröbner bases, and ideals
• circuit — arithmetic circuits (DAGs of add/mul nodes) quotiented by an ideal

The intended use case is verifying arithmetic circuits modulo an ideal: two circuits computing the same polynomial in the quotient ring are equivalent.

Modules

poly

Variables — poly::var

Variables are any type implementing the Var trait. The built-in StaticVar carries a static string name and optional integer indices, with a var! macro for construction:

use circuit_cas::var;

let x   = var!("x");          // x
let x0  = var!("x", 0);       // x₀
let x01 = var!("x", 0, 1);    // x₀,₁

Polynomials — poly::flat

Poly<V> is a multivariate polynomial over ℤ backed by a HashMap<Mono<V>, i32>. Arithmetic operators (+, -, *) and scalar multiplication are provided. Monomial ordering uses pure lexicographic order (lex) with variable names sorted alphabetically.

// x² - 2xy  (using array-of-pairs syntax)
let f: Poly<StaticVar> = [
    (1i32,  Mono::from([("x", 2u32)])),
    (-2i32, Mono::from([("x", 1u32), ("y", 1u32)])),
].into_iter().collect();

Key operations:

Method	Description
Poly::is_zero	whether the polynomial is the zero polynomial
Poly::leading_term_lex	leading (monomial, coefficient) under lex
Poly::s_poly(&other)	S-polynomial of two polynomials
Poly::div_rem(divisor)	pseudo-division: returns (d, q, r) with lc(g)^d·f = q·g + r

Ideals — poly::ideal

Ideal<V, S> uses the typestate pattern to track at the type level whether its generators form a Gröbner basis:

use circuit_cas::poly::ideal::{Ideal, Generators, GroebnerBasis};

// Arbitrary generators
let ideal: Ideal<StaticVar, Generators> = Ideal::new(vec![f1, f2]);

// Compute the reduced Gröbner basis — consumes the original ideal
let gb: Ideal<StaticVar, GroebnerBasis> = ideal.groebner_basis();

// Ideal membership test (only available on GroebnerBasis state)
assert!(gb.contains(&some_poly));

Ideal implements Display as <g1, g2, ...> and FromIterator<Poly<V>> for construction from an iterator.

Buchberger's algorithm — poly::buchberger

use circuit_cas::poly::buchberger::{groebner_basis, is_groebner_basis};

let basis = groebner_basis(vec![f1, f2]);
assert!(is_groebner_basis(&basis));

groebner_basis returns the reduced Gröbner basis: after running Buchberger's algorithm it minimizes (removes redundant generators) and interreduces (fully reduces each generator modulo the others).

circuit

DAG — circuit::dag

Circuit<V> is a DAG of Node<V> values, with structural sharing via interning. Nodes are Leaf(V), Scale(id, i32), Sum(id, id), or Prod(id, id).

Quotient ring — circuit::quotient

Quotient<V> pairs an arithmetic circuit with a Ideal<V, GroebnerBasis>, representing a circuit in the quotient ring ℤ[vars] / I.

use circuit_cas::circuit::quotient::Quotient;

// Build from a list of generators — Gröbner basis is computed automatically
let quotient: Quotient<StaticVar> = vec![f1, f2, f3].into_iter().collect();

// Or from a pre-computed Gröbner basis
let quotient = Quotient::from(gb);

println!("{quotient}"); // C/<g1, g2>

Example

use circuit_cas::{var, circuit::quotient::Quotient, poly::var::StaticVar};

fn main() {
    let x  = var!("x");
    let xb = var!("x\u{0304}");  // x̄

    // Idempotency relations: x² = x, x̄² = x̄, x·x̄ = x
    let idem = vec![
        1 * (&x  ^ 2) - 1 * (&x  ^ 1),
        1 * (&xb ^ 2) - 1 * (&xb ^ 1),
        1 * ((&x ^ 1) * (&xb ^ 1)) - 1 * (&x ^ 1),
    ];

    let quotient: Quotient<StaticVar> = idem.into_iter().collect();
    println!("{quotient}");
}

Run with:

cargo run --example quotient

Development

cargo test     # run all tests