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.
 
@@ -534,11 +534,215 @@ 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 Self-Cancellation
+
+**Theorem:** If constraint $C: a \land \mathbb{1} \oplus (a \oplus r) = 0$, then $r = 0$.
+
+**Proof:**
+$$\begin{align}
+a \land \mathbb{1} \oplus (a \oplus r) &= 0 && \text{(Given)} \\
+a \oplus a \oplus r &= 0 && \text{(B1: } a \land \mathbb{1} = a\text{)} \\
+0 \oplus r &= 0 && \text{(F2: } a \oplus a = 0\text{)} \\
+r &= 0 && \text{(F1: } 0 \oplus r = r\text{)} \quad \square
+\end{align}$$
+
+### Derivation 2: Double Negation Elimination
+
+**Theorem:** Given constraints:
+- $C_1: a \land \mathbb{1} \oplus (\mathbb{1} \oplus \bar{a}) = 0$  
+- $C_2: \bar{a} \land \mathbb{1} \oplus (\mathbb{1} \oplus r) = 0$
+
+Then $r = a$.
+
+**Proof:**
+$$\begin{align}
+\text{From } C_1: \quad a \oplus \mathbb{1} \oplus \bar{a} &= 0 && \text{(B1, E1)} \\
+\Rightarrow \bar{a} &= a \oplus \mathbb{1} && \text{(Rearranging via F2, F3)} \\
+\\
+\text{From } C_2: \quad \bar{a} \oplus \mathbb{1} \oplus r &= 0 && \text{(B1, E1)} \\
+\text{Substituting: } \quad (a \oplus \mathbb{1}) \oplus \mathbb{1} \oplus r &= 0 && \text{(E2)} \\
+a \oplus (\mathbb{1} \oplus \mathbb{1}) \oplus r &= 0 && \text{(F3)} \\
+a \oplus 0 \oplus r &= 0 && \text{(F2)} \\
+a \oplus r &= 0 && \text{(F1)} \\
+r &= a && \text{(E1)} \quad \square
+\end{align}$$
+
+### Derivation 3: 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{align}
+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{align}$$
+
+*Inductive step:* Assume $t_k = \bigoplus_{i=0}^k x_i$. From $C_{k+1}$:
+$$\begin{align}
+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{align}$$
+
+### Derivation 4: Keccak Chi 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{align}
+\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{align}$$
+
+### Derivation 5: SHA Ch Function
+
+**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{align}
+\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{align}$$
+
+### Derivation 6: SHA Maj Function  
+
+**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{align}
+\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{align}$$
+
+### Derivation 7: Conditional Selection
+
+**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{align}
+\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{align}$$
+
+### Derivation 8: Boolean Simplification (AND with Zero)
+
+**Theorem:** If constraint $C: a \land 0 \oplus r = 0$, then $r = 0$.
+
+**Proof:**
+$$\begin{align}
+a \land 0 \oplus r &= 0 && \text{(Given)} \\
+0 \oplus r &= 0 && \text{(B2: } a \land 0 = 0\text{)} \\
+r &= 0 && \text{(F1: } 0 \oplus r = r\text{)} \quad \square
+\end{align}$$
+
+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,