135 lines
4.1 KiB
Markdown
135 lines
4.1 KiB
Markdown
# 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:
|
||
|
||
```rust
|
||
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.
|
||
|
||
```rust
|
||
// 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:
|
||
|
||
```rust
|
||
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`
|
||
|
||
```rust
|
||
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`.
|
||
|
||
```rust
|
||
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
|
||
|
||
```rust
|
||
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
|
||
```
|