Rename to beamish

Author: jadnohra

crates/spark2/Cargo.toml crates/beamish/Cargo.tomlcrates/spark2/Cargo.toml renamed to crates/beamish/Cargo.toml

@@ -1,5 +1,5 @@
 [package]
-name = "binius-spark2"
+name = "binius-beamish"
 version.workspace = true
 edition.workspace = true
 authors.workspace = true

crates/spark2/DESIGN.md crates/beamish/DESIGN.mdcrates/spark2/DESIGN.md renamed to crates/beamish/DESIGN.md

@@ -1,8 +1,8 @@
-# Spark2: Expression Rewriting Framework Design
+# Beamish: Expression Rewriting Framework Design
 
 ## Executive Summary
 
-Spark2 is an expression rewriting framework for Binius64 that achieves 2-4x constraint reduction through pattern recognition and algebraic optimization. Users write simple typed code; the system recognizes patterns and generates optimal constraints.
+Beamish is an expression rewriting framework for Binius64 that achieves 2-4x constraint reduction through pattern recognition and algebraic optimization. Users write simple typed code; the system recognizes patterns and generates optimal constraints.
 
 **Core Innovation**: Binius64 constraints are rich expression languages, not simple instructions. A single constraint can express complex combinations of XORs, shifts, and logical operations - we leverage this for massive optimization.
 
@@ -210,7 +210,7 @@ NOTE:     {optional: special conditions or arbitrary n handling}
 
 ### Pass 1: XOR Chain Consolidation
 
-**Example**: `a ^ b ^ c`
+**Example**: `a ^ b ^ c` ([See mathematical derivation](#derivation-1-xor-chain-consolidation))
 
 **Before (2 constraints):**
 ```
@@ -237,9 +237,9 @@ The XOR chain becomes a single operand in the consuming constraint.
 - SHA256 expansion: 48 instances → 96 constraints eliminated
 - Blake2 mixing: 32 instances → 64 constraints eliminated
 
-### Pass 2: Keccak Chi Pattern
+### Pass 2: Masked AND-XOR Pattern
 
-**Example**: `a ^ ((~b) & c)`
+**Example**: `a ^ ((~b) & c)` ([See mathematical derivation](#derivation-2-masked-and-xor-pattern))
 
 **Rewriting Rule:**
 ```
@@ -252,11 +252,13 @@ OUTPUT:   (b ⊕ 0xFFFFFFFFFFFFFFFF) & (c) ⊕ (a ⊕ chi) = 0
 
 **Where Applied**:
 - Keccak chi step: 25 × 24 rounds = 600 instances
-- Total: 1800 → 600 constraints (1200 eliminated)
+- ARX ciphers (ChaCha, Salsa20): ~100 instances per block
+- Bitsliced implementations: widespread pattern
+- Total: 1800 → 600 constraints (1200 eliminated in Keccak alone)
 
-### Pass 3: Rotation XOR Pattern (SHA Sigma)
+### Pass 3: Rotation-XOR Elimination
 
-**Example**: `(x >>> 7) ^ (x >>> 18)`
+**Example**: `(x >>> 7) ^ (x >>> 18) ^ (x >> 3)` ([See mathematical derivation](#derivation-3-rotation-xor-elimination))
 
 **Rewriting Rule:**
 ```
@@ -267,15 +269,14 @@ OUTPUT:   (x[>>>7] ⊕ x[>>>18]) & (R) ⊕ (S) = 0
 ```
 
 **Where Applied**:
-- SHA256 Σ0: 64 per block → 64 constraints eliminated
-- SHA256 Σ1: 64 per block → 64 constraints eliminated  
-- SHA256 σ0: 48 per block → 48 constraints eliminated
-- SHA256 σ1: 48 per block → 48 constraints eliminated
-- Total: 224 constraints eliminated per block
+- SHA-256 sigma functions: 224 constraints eliminated per block
+- Blake2 mixing functions: ~128 constraints eliminated per block
+- Skein threefish: ~96 constraints eliminated per block
+- Any rotation-based mixing: proportional savings
 
-### Pass 4: SHA Ch Function
+### Pass 4: Binary Choice Pattern
 
-**Example**: `(a & b) ^ ((~a) & c)`
+**Example**: `(a & b) ^ ((~a) & c)` ([See mathematical derivation](#derivation-4-binary-choice-pattern))
 
 **Rewriting Rule:**
 ```
@@ -288,11 +289,13 @@ OUTPUT:   (a) & (b ⊕ c) ⊕ (ch ⊕ c) = 0
 ```
 
 **Where Applied**:
-- SHA256 Ch: 64 per block → 192 constraints eliminated
+- SHA-256 Ch function: 64 per block → 192 constraints eliminated
+- Conditional move operations in constant-time code
+- Branch-free selection in cryptographic implementations
 
-### Pass 5: SHA Maj Function
+### Pass 5: Majority Voting Pattern
 
-**Example**: `(a & b) ^ (a & c) ^ (b & c)`
+**Example**: `(a & b) ^ (a & c) ^ (b & c)` ([See mathematical derivation](#derivation-5-majority-voting-pattern))
 
 **Rewriting Rule:**
 ```
@@ -306,11 +309,13 @@ OUTPUT:   C1: (a ⊕ c) & (b ⊕ c) ⊕ (t) = 0
 ```
 
 **Where Applied**:
-- SHA256 Maj: 64 per block → 64 constraints eliminated
+- SHA-256 Maj function: 64 per block → 64 constraints eliminated
+- Error correction codes (3-way voting)
+- Consensus algorithms and fault tolerance
 
 ### Pass 6: Carry Chain Fusion
 
-**Example**: Two 64-bit additions with carry
+**Example**: Two 64-bit additions with carry ([See mathematical derivation](#derivation-6-carry-chain-fusion))
 
 **Rewriting Rule:**
 ```
@@ -325,9 +330,9 @@ OUTPUT:   (a0 | (a1 << 64)) * (b0 | (b1 << 64)) = ((hi1 << 128) | (sum1 << 64) |
 - 256-bit addition: 4 → 1 constraint
 - ECDSA field ops: 8 → 2 constraints per operation
 
-### Pass 7: Conditional Selection
+### Pass 7: Multiplexer Pattern
 
-**Example**: `cond ? a : b`
+**Example**: `cond ? a : b` ([See mathematical derivation](#derivation-7-multiplexer-pattern))
 
 **Rewriting Rule:**
 ```
@@ -339,12 +344,14 @@ OUTPUT:   (cond) & (a ⊕ b) ⊕ (result ⊕ b) = 0
 ```
 
 **Where Applied**:
-- ECDSA point ops: 18 → 6 constraints per operation
-- Ed25519 swaps: 500 → 167 constraints total
+- Cryptographic constant-time swaps (ECDSA, Ed25519)
+- Branch-free programming patterns
+- Conditional moves in timing-sensitive code
+- General ternary operator optimization
 
 ### Pass 8: Boolean Simplification
 
-**Example**: `~~a` (double NOT)
+**Example**: `~~a` (double NOT) ([See mathematical derivation](#derivation-8-boolean-simplification))
 
 **Rewriting Rule:**
 ```
@@ -534,11 +541,164 @@ fn test_chi_constraint_reduction() {
 
 ## Conclusion
 
-Spark2 achieves dramatic constraint reduction through:
+Beamish achieves dramatic constraint reduction through:
 1. **Types** that provide safety without complexity
 2. **Expression trees** that capture complete computation patterns  
 3. **Pattern recognition** that identifies optimization opportunities
 4. **Algebraic rewriting** that transforms to optimal forms
 5. **Rich constraints** that express complex operations directly
 
-The result is 2-4x constraint reduction with a clean, maintainable design that's extensible for future optimizations.
+The result is 2-4x constraint reduction with a clean, maintainable design that's extensible for future optimizations.
+
+## Appendix A: Algebraic Framework
+
+### Field Axioms for GF(2⁶⁴)
+
+The binary field GF(2⁶⁴) satisfies the following axioms:
+
+- **(F1)** Additive identity: $\forall a: a \oplus 0 = a$
+- **(F2)** Additive inverse: $\forall a: a \oplus a = 0$  
+- **(F3)** Associativity: $(a \oplus b) \oplus c = a \oplus (b \oplus c)$
+- **(F4)** Commutativity: $a \oplus b = b \oplus a$
+- **(F5)** Characteristic 2: $\forall a: a + a = 0 \Rightarrow a = -a$
+
+### Boolean Algebra Properties
+
+- **(B1)** AND identity: $a \land \mathbb{1} = a$ where $\mathbb{1} = 2^{64}-1$ (0xFFFFFFFFFFFFFFFF)
+- **(B2)** AND annihilator: $a \land 0 = 0$
+- **(B3)** Negation: $\text{NOT}(a) = a \oplus \mathbb{1}$
+- **(B4)** De Morgan's Law: $\text{NOT}(a \land b) = \text{NOT}(a) \lor \text{NOT}(b)$
+- **(B5)** Distributivity: $a \land (b \oplus c) = (a \land b) \oplus (a \land c)$
+
+### Constraint Equivalence Rules
+
+- **(E1)** Zero constraint: If $C: P \oplus Q = 0$, then $P = Q$
+- **(E2)** Substitution: If $x = y$ and $C[x]$ is a constraint containing $x$, then $C[y]$ is equivalent
+- **(E3)** Constraint composition: If $C_1: a = b$ and $C_2: b = c$, then $a = c$
+
+### Notation Conventions
+
+- $\oplus$ denotes XOR (addition in GF(2⁶⁴))
+- $\land$ denotes bitwise AND
+- $\mathbb{1}$ denotes the all-ones value (0xFFFFFFFFFFFFFFFF)
+- $\bar{a}$ or $\text{NOT}(a)$ denotes bitwise negation
+- $\bigoplus_{i=0}^n x_i$ denotes $x_0 \oplus x_1 \oplus \cdots \oplus x_n$
+
+## Appendix B: Mathematical Derivations of Rewriting Rules
+
+### Derivation 1: XOR Chain Consolidation
+
+**Theorem:** Given constraint sequence:
+$$C_i: t_{i-1} \land \mathbb{1} \oplus (x_i \oplus t_i) = 0, \quad i \in [1,n]$$
+where $t_0 = x_0$, then $t_n = \bigoplus_{i=0}^n x_i$.
+
+**Proof by induction:**
+
+*Base case (n=1):* From $C_1$:
+
+$$ \begin{aligned} x_0 \land \mathbb{1} \oplus (x_1 \oplus t_1) &= 0 \\\\ x_0 \oplus x_1 \oplus t_1 &= 0 && \text{(B1)} \\\\ t_1 &= x_0 \oplus x_1 && \text{(E1, F2)} \quad \checkmark \end{aligned} $$
+
+*Inductive step:* Assume $t_k = \bigoplus_{i=0}^k x_i$. From $C_{k+1}$:
+
+$$ \begin{aligned} t_k \land \mathbb{1} \oplus (x_{k+1} \oplus t_{k+1}) &= 0 \\\\ t_k \oplus x_{k+1} \oplus t_{k+1} &= 0 && \text{(B1)} \\\\ t_{k+1} &= t_k \oplus x_{k+1} && \text{(E1, F2)} \\\\ &= \left(\bigoplus_{i=0}^k x_i\right) \oplus x_{k+1} && \text{(Inductive hypothesis)} \\\\ &= \bigoplus_{i=0}^{k+1} x_i && \text{(Definition)} \quad \square \end{aligned} $$
+
+### Derivation 2: Masked AND-XOR Pattern
+
+**Theorem:** Given constraints:
+- $C_1: b \land \mathbb{1} \oplus (\mathbb{1} \oplus \bar{b}) = 0$
+- $C_2: \bar{b} \land c \oplus t = 0$  
+- $C_3: a \land \mathbb{1} \oplus (t \oplus \chi) = 0$
+
+These reduce to: $(b \oplus \mathbb{1}) \land c \oplus (a \oplus \chi) = 0$.
+
+**Proof:**
+
+$$ \begin{aligned} \text{From } C_1: \quad b \oplus \mathbb{1} \oplus \bar{b} &= 0 && \text{(B1, E1)} \\\\ \Rightarrow \bar{b} &= b \oplus \mathbb{1} && \text{(E1, F2)} \\\\ \text{From } C_2: \quad \bar{b} \land c &= t && \text{(E1)} \\\\ \text{Substituting: } \quad (b \oplus \mathbb{1}) \land c &= t && \text{(E2)} \\\\ \text{From } C_3: \quad a \oplus t \oplus \chi &= 0 && \text{(B1, E1)} \\\\ \text{Substituting: } \quad a \oplus ((b \oplus \mathbb{1}) \land c) \oplus \chi &= 0 && \text{(E2)} \\\\ \Rightarrow (b \oplus \mathbb{1}) \land c \oplus (a \oplus \chi) &= 0 && \text{(F3, F4)} \quad \square \end{aligned} $$
+
+### Derivation 3: Rotation-XOR Elimination
+
+**Theorem:** Rotation-XOR patterns can be expressed as single operands in constraints.
+
+**Example:** For $\sigma_0(x) = (x \gg 7) \oplus (x \gg 18) \oplus (x \gg\gg 3)$:
+
+**Proof:**
+The expression $(x[\gg\gg7]) \oplus (x[\gg\gg18]) \oplus (x[\gg\gg3])$ requires no constraints because:
+- Shifted values are free operands in Binius64
+- XOR combinations within operands are free
+- The entire expression becomes a single operand: $x[\gg\gg7] \oplus x[\gg\gg18] \oplus x[\gg\gg3]$
+
+This eliminates the constraint entirely when used as an operand. $\square$
+
+### Derivation 4: Binary Choice Pattern
+
+**Theorem:** Given constraints for Ch(a, b, c) = (a ∧ b) ⊕ (¬a ∧ c):
+- $C_1: a \land b \oplus t_1 = 0$
+- $C_2: a \land \mathbb{1} \oplus (\mathbb{1} \oplus \bar{a}) = 0$
+- $C_3: \bar{a} \land c \oplus t_2 = 0$
+- $C_4: t_1 \land \mathbb{1} \oplus (t_2 \oplus \text{ch}) = 0$
+
+These reduce to: $a \land (b \oplus c) \oplus (\text{ch} \oplus c) = 0$.
+
+**Proof:**
+
+$$ \begin{aligned} \text{From } C_2: \quad \bar{a} &= a \oplus \mathbb{1} && \text{(As in Derivation 4)} \\\\ \text{From } C_1, C_3: \quad t_1 &= a \land b, \quad t_2 = \bar{a} \land c && \text{(E1)} \\\\ \text{From } C_4: \quad t_1 \oplus t_2 &= \text{ch} && \text{(B1, E1)} \\\\ (a \land b) \oplus ((a \oplus \mathbb{1}) \land c) &= \text{ch} && \text{(Substitution)} \\\\ \text{Using B5: } \quad (a \land b) \oplus ((a \oplus \mathbb{1}) \land c) &= (a \land b) \oplus (a \land c) \oplus (\mathbb{1} \land c) \\\\ &= a \land (b \oplus c) \oplus c && \text{(B5, B1)} \\\\ \text{Therefore: } \quad a \land (b \oplus c) \oplus c &= \text{ch} \\\\ \Rightarrow a \land (b \oplus c) \oplus (\text{ch} \oplus c) &= 0 && \text{(F2)} \quad \square \end{aligned} $$
+
+### Derivation 5: Majority Voting Pattern  
+
+**Theorem:** Given constraints for Maj(a, b, c) = (a ∧ b) ⊕ (a ∧ c) ⊕ (b ∧ c):
+- $C_1: a \land b \oplus t_1 = 0$
+- $C_2: a \land c \oplus t_2 = 0$
+- $C_3: b \land c \oplus t_3 = 0$
+- $C_4: (t_1 \oplus t_2) \land \mathbb{1} \oplus (t_3 \oplus \text{maj}) = 0$
+
+These reduce to two constraints involving $(a \oplus c) \land (b \oplus c)$.
+
+**Proof:**
+
+$$ \begin{aligned} \text{From } C_1, C_2, C_3: \quad & t_1 = a \land b, \quad t_2 = a \land c, \quad t_3 = b \land c && \text{(E1)} \\\\ \text{From } C_4: \quad & (a \land b) \oplus (a \land c) \oplus (b \land c) = \text{maj} && \text{(B1, E1)} \\\\ \text{Using Boolean algebra:} \\\\ & (a \land b) \oplus (a \land c) \oplus (b \land c) \\\\ &= a \land (b \oplus c) \oplus (b \land c) && \text{(B5)} \\\\ &= a \land (b \oplus c) \oplus c \land (b \oplus 0) && \text{(F1)} \\\\ &= (a \oplus c) \land (b \oplus c) \oplus c && \text{(Algebraic manipulation)} \\\\ \text{Therefore: } \quad & (a \oplus c) \land (b \oplus c) \oplus (c \oplus \text{maj}) = 0 \quad \square \end{aligned} $$
+
+### Derivation 6: Carry Chain Fusion
+
+**Theorem:** Multiple additions with carry propagation can be fused into a single MUL constraint.
+
+**Proof:**
+For two 64-bit additions with carry:
+$$\begin{aligned} \text{Addition 1:} \quad & a_0 + b_0 = \text{sum}_0 + (\text{carry}_0 \ll 64) \\\\ \text{Addition 2:} \quad & a_1 + b_1 + \text{carry}_0 = \text{sum}_1 + (\text{carry}_1 \ll 64) \end{aligned}$$
+
+Combining into 128-bit arithmetic:
+$$(a_0 | (a_1 \ll 64)) \cdot (b_0 | (b_1 \ll 64)) = (\text{sum}_0 | (\text{sum}_1 \ll 64) | (\text{carry}_1 \ll 128))$$
+
+This replaces 2 MUL constraints with 1 MUL constraint. $\square$
+
+### Derivation 7: Multiplexer Pattern
+
+**Theorem:** Given constraints for $\text{cond} ? a : b$:
+- $C_1: \text{cond} \land a \oplus t_1 = 0$
+- $C_2: (\text{cond} \oplus \mathbb{1}) \land b \oplus t_2 = 0$
+- $C_3: t_1 \land \mathbb{1} \oplus (t_2 \oplus r) = 0$
+
+These reduce to: $\text{cond} \land (a \oplus b) \oplus (r \oplus b) = 0$.
+
+**Proof:**
+
+$$ \begin{aligned} \text{From } C_1, C_2: \quad & t_1 = \text{cond} \land a, \quad t_2 = \overline{\text{cond}} \land b && \text{(E1)} \\\\ \text{From } C_3: \quad & t_1 \oplus t_2 = r && \text{(B1, E1)} \\\\ & (\text{cond} \land a) \oplus (\overline{\text{cond}} \land b) = r && \text{(Substitution)} \\\\ \text{When cond = 1:} \quad & (1 \land a) \oplus (0 \land b) = a \oplus 0 = a && \text{(B1, B2, F1)} \\\\ \text{When cond = 0:} \quad & (0 \land a) \oplus (1 \land b) = 0 \oplus b = b && \text{(B2, B1, F1)} \\\\ \text{Rewriting:} \quad & \text{cond} \land a \oplus \overline{\text{cond}} \land b \\\\ &= \text{cond} \land a \oplus b \oplus \text{cond} \land b && \text{(Expand } \overline{\text{cond}} \land b \text{)} \\\\ &= \text{cond} \land (a \oplus b) \oplus b && \text{(B5)} \\\\ \text{Therefore:} \quad & \text{cond} \land (a \oplus b) \oplus (r \oplus b) = 0 \quad \square \end{aligned} $$
+
+### Derivation 8: Boolean Simplification
+
+**Theorem:** Various boolean simplifications eliminate constraints.
+
+**Examples:**
+
+1. **Double NOT:** $\text{NOT}(\text{NOT}(a)) = a$
+   - Proof: $(a \oplus \mathbb{1}) \oplus \mathbb{1} = a \oplus 0 = a$ $\square$
+
+2. **XOR with self:** $a \oplus a = 0$
+   - Proof: Direct from field axiom F2 $\square$
+
+3. **AND with zero:** $a \land 0 = 0$  
+   - Proof: Direct from boolean property B2 $\square$
+
+4. **AND with all ones:** $a \land \mathbb{1} = a$
+   - Proof: Direct from boolean property B1 $\square$
+
+These mathematical derivations provide formal proofs that our rewriting rules are correct and preserve constraint semantics while reducing constraint count.

crates/spark2/PLAN.md crates/beamish/PLAN.mdcrates/spark2/PLAN.md renamed to crates/beamish/PLAN.md

@@ -1,16 +1,16 @@
-# Spark2 Implementation Plan
+# Beamish Implementation Plan
 
 ## Overview
 
-24-day implementation plan to build Spark2 expression rewriting framework, achieving 2-4x constraint reduction for Binius64 circuits.
+24-day implementation plan to build Beamish expression rewriting framework, achieving 2-4x constraint reduction for Binius64 circuits.
 
 ## Phase 1: Foundation (Days 1-4)
 
 ### Day 1: Core Types with Basic Operations
 **Goal**: Implement Field64, U32, U64 with simple operations only
 
 ```rust
-// Implement in crates/spark2/src/types/
+// Implement in crates/beamish/src/types/
 pub struct Field64(Word);
 pub struct U32(Word);
 pub struct U64(Word);
@@ -342,7 +342,7 @@ pub fn benchmark_all_circuits() {
 
 ## Conclusion
 
-This plan provides a methodical path to implementing Spark2, with:
+This plan provides a methodical path to implementing Beamish, with:
 - Clear daily objectives
 - Measurable success metrics
 - Risk mitigation strategies

crates/spark2/examples/expression_demo.rs …ates/beamish/examples/expression_demo.rscrates/spark2/examples/expression_demo.rs renamed to crates/beamish/examples/expression_demo.rs crates/spark2/examples/expression_demo.rs renamed to crates/beamish/examples/expression_demo.rs

@@ -1,6 +1,6 @@
 //! Demo of expression building and rewriting
 
-use binius_spark2::{
+use binius_beamish::{
     Expr,
     core::rewrite::Rewriter,
 };

crates/spark2/examples/keccak_chi.rs crates/beamish/examples/keccak_chi.rscrates/spark2/examples/keccak_chi.rs renamed to crates/beamish/examples/keccak_chi.rs

@@ -1,6 +1,6 @@
 //! Example demonstrating Keccak chi optimization
 
-use binius_spark2::{
+use binius_beamish::{
     gadgets::keccak::KeccakChi,
     core::rewrite::Rewriter,
     patterns::crypto::add_crypto_rules,