Grind Simplification Sets: Design Summary

# Grind Homomorphisms as Simplification Sets: Design Summary ## Motivation: domain-specific injection into integers At a meeting with Google engineers working on software verification, Andres Erbsen described a mechanism used across the Bedrock2 ecosystem in Rocq: **intblasting**. The strategy is to inject bitvector/word operations into integer arithmetic using rewrite rules, then solve with standard techniques. For example, given a word equality `x + y = y + x`, the injection produces: ``` (word.unsigned x + word.unsigned y) % 2^w = (word.unsigned y + word.unsigned x) % 2^w ``` This is then solvable by integer arithmetic. The injection is defined by a collection of rewrite rules: | Original | Injected | |----------|----------| | `word.unsigned (word.add x y)` | `(word.unsigned x + word.unsigned y) % 2^w` | | `word.unsigned (word.mul x y)` | `(word.unsigned x * word.unsigned y) % 2^w` | | `word.unsigned (word.slu x n)` | `(word.unsigned x * 2^n) % 2^w` | | `word.signed (word.srs w n)` | `word.signed w / 2^n` | | `w1 = w2` | `word.unsigned w1 = word.unsigned w2` | | `word.ltu w1 w2` | `word.unsigned w1 < word.unsigned w2` | The rules are applied recursively: injecting `word.unsigned` at the top triggers further injection through subterms, bottoming out at variables. Cleanup rules like `(a % m + b) % m = (a + b) % m` remove redundant modular wrappers from the output. The request from the meeting was distilled as: **a mechanism for attaching new solver strategies to `grind`**, specifically a way for users to provide rewriting rules that translate terms from one domain into another where a dedicated solver can handle them. `grind` already has `ToInt` type classes that inject types into integers, but these only cover generic algebraic operations (addition, multiplication, etc.). Type-specific operations like bitwise `&&&`, `|||`, shifts, and unsigned/signed interpretations are not covered. The intblasting strategy requires injecting these operations too, which the `ToInt` mechanism cannot express. The simplification set approach is strictly more general: the user defines arbitrary rewrite rules for any operation, not just those anticipated by a type class interface. ## Simplification sets as algebra homomorphisms A simplification set defines an **algebra homomorphism** h : A → B from a source algebra to a target algebra: - **Source algebra A**: the type and operations the user's problem talks about (e.g., `BitVec w` with `+`, `*`, `&&&`, etc.). - **Target algebra B**: a type with a **dedicated solver** in `grind` (e.g., `Int` with linear arithmetic). - **Homomorphism h**: a function from A to B (e.g., `word.unsigned`), with rules specifying how h commutes with operations. The rules encode the homomorphism equations: ``` h(f(x, y)) = g(h(x), h(y)) ``` For example: `word.unsigned (word.add x y) = (word.unsigned x + word.unsigned y) % 2^w`. Confluence ensures h is well-defined (unique image for each source term). Termination guarantees computation finishes. The `=` injection rule translates equality itself: ``` (a = b) ↔ (h(a) = h(b)) -- injective case (a = b) → (h(a) = h(b)) -- non-injective case ``` ### Why a target solver is essential The homomorphism is the *bridge*; the solver is the *reason for crossing*. Without a solver in the target domain, the translation just creates more terms that nobody knows how to reason about. Every useful set follows this pattern: - **Intblasting**: `BitVec → Int`, target solver is linear integer arithmetic. - **Bit-level decomposition**: `BitVec w → (Fin w → Bool)`, target solver is SAT (`bv_decide`). - **Type coercions**: `Nat → Int → Rat`, target solver is arithmetic at each level. - **Representation changes**: `Complex → Real × Real` via projections, target solver is real arithmetic. - **Modular arithmetic**: `ZMod n → Int` with constraints, target solver is integer arithmetic. ### Injective vs. non-injective homomorphisms **Injective (biconditional `=` rule, embedding):** ``` (w1 = w2) ↔ (word.unsigned w1 = word.unsigned w2) ``` - Forward direction (→): free from homomorphism property. - Backward direction (←): requires injectivity of h. - **Power:** the target solver can fully determine source equalities. If the integer solver proves `word.unsigned w1 = word.unsigned w2`, that flows back as `w1 = w2`. - **Example:** intblasting — `word.unsigned` is injective. **Non-injective (forward-only `=` rule):** ``` (a = b) → (h(a) = h(b)) ``` - Only the forward implication holds. - The target can derive **disequalities** back via contrapositive: `h(a) ≠ h(b) → a ≠ b`. - The target cannot conclude source equalities. - **Weaker but still useful:** can find contradictions in the target domain. ### Why injecting `=` matters `grind` reasons modulo equalities: if it knows `x = a + b`, it treats `x` and `a + b` as interchangeable. A simplification set fires syntactically — it rewrites terms based on their structure, not modulo the E-graph's equalities. Injecting `=` bridges this gap. When the E-graph contains `x = a + b` (words), the `=` injection rule fires on this equality, producing: ``` word.unsigned x = (word.unsigned a + word.unsigned b) % 2^w ``` The connection between `x` and `a + b` is now explicit in the target domain. Both `word.unsigned x` and the injection of `a + b` are explicitly created. The E-graph connects them. Without this rule, the simplification set would translate `word.unsigned x` and `word.unsigned (a + b)` independently, and the connection would be lost. This is the abstract safety criterion: **a simplification set must inject `=` over the source type.** This ensures every equality in the source domain is explicitly translated to the target domain. ## Proposal: two-component architecture ### Two components **Normalizer (`@[grind norm]`).** Reserved for internal `grind` invariants. Runs before internalization (existing behavior, unchanged). Ensures terms meet assumptions of internal procedures (e.g., canonical comparison operators, canonical Int representation). Not intended for user extension. **Homomorphisms.** Each runs to fixpoint *outside the E-graph*. Only the final normal form is internalized — no intermediate terms enter the E-graph. The result is a final domain-specific form. Intblasting is one instance: the `intblast` simplification set injects word operations into integer arithmetic. But the mechanism is general — any domain translation where a dedicated solver handles the target domain. ### Execution model For a new term `e`: 1. Normalize `e` → `e_norm` (internal invariants). 2. For each active simplification set T, apply T to `e_norm` via `simp` to fixpoint → `e_T`. 3. Normalize each `e_T` → `e_T_norm`. 4. Internalize `e_norm` and each `e_T_norm` (if distinct). Merge all into same equivalence class. 5. Subterms of internalized results go through the full pipeline (steps 1–4) as they are internalized bottom-up. ### Rules are unconditional only Simplification sets contain only unconditional equalities. Conditional reasoning is handled by E-matching, which already reacts to evolving E-graph equalities. This separation is both a design choice and a correctness requirement — it enables the performance optimizations described below. ## Simplification set definitions and scoping ### Simplification sets as standalone artifacts A simplification set is defined independently, with its own identity and execution semantics: ```lean -- Define simplification sets grind_simp_set intblast -- Add theorems @[intblast] theorem unsigned_add ... @[intblast] theorem unsigned_mul ... @[intblast] theorem mod_add_mod : (a % m + b) % m = (a + b) % m -- cleanup ``` ### Grind attributes as namespaces Grind attributes bundle E-matching theorems and attached simplification sets. They enable project-level isolation: Aeneas avoids interactions with Mathlib theorems; Velvet uses only cheap E-matching theorems for fast eager discharge. ```lean -- Define grind attributes grind_attr Aeneas grind_attr Velvet -- E-matching theorems scoped to attributes @[Aeneas =] theorem foo ... @[Velvet =] theorem bar ... -- Attach simplification sets to attributes grind_attach intblast [Aeneas] grind_attach intblast [grind] -- default attribute ``` ### Call site syntax ```lean grind -- default attribute with attached sets grind [Aeneas] -- default + Aeneas (additive) grind only [Aeneas] -- Aeneas only (exclusive) grind [Aeneas, +intblast] -- Aeneas attribute + intblast set ad-hoc grind only [+intblast] -- no attributes, just intblast ``` - `grind only` controls attributes and simplification sets, not the normalizer. The normalizer always runs. - Combining multiple attributes is supported but no properties are guaranteed about the combination. - Programmatic API (used by Aeneas, Velvet internally) gives full control over selection. ## Performance: simp traversal ### The problem When a simplificaton set's `simp` call processes a term, it must avoid re-traversing subterms that have already been processed. Without this, cost is proportional to the full term tree rather than the new terms produced by rewriting. ### Bottom-up internalization and the stop condition `grind` internalizes terms bottom-up. By the time a simplification set runs on a term `e`, all subterms of `e` are already in the E-graph and have been processed by the pipeline. **Stop condition.** When `simp` encounters a term `t` during traversal: - If a rule matches `t`: apply it, continue (result is a new term). - If no rule matches `t` AND `t`'s E-graph node has been marked as processed by the current set: **stop, don't descend**. - Otherwise: descend normally. Both pre-rules and post-rules are supported. Users are not required to classify rules. The stop condition is sound because: - Already-internalized and already-processed terms will not be rewritten at any depth. Descending would find nothing to do. - New terms produced by the rewriting (the "bubble" above the already-internalized "floor") get full treatment: rules fire on descent, cleanup rules fire on ascent. **Cost model.** Proportional to new terms produced by the rewriting, not the input term's subterm tree. ### Worked example Consider the term `word.unsigned (word.add (word.add a b) c)` with `w_u` as shorthand for `word.unsigned`: ``` w_u (a + b + c) → (w_u (a + b) + w_u c) % 2^w -- injection rule fires → ((w_u a + w_u b) % 2^w + w_u c) % 2^w -- injection rule fires on subterm → (w_u a + w_u b + w_u c) % 2^w -- cleanup: (a % m + b) % m = (a + b) % m ``` During the `simp` traversal: - `w_u (a + b + c)`: rule matches → apply injection, producing new terms. - `w_u (a + b)`: rule matches → apply injection. - `w_u a`: in E-graph, processed, no rule matches → **stop**. - `w_u b`, `w_u c`: same → **stop**. - On ascent through *new* terms: cleanup rule `(a % m + b) % m = (a + b) % m` fires, eliminating the nested `% 2^w`. The `simp` call never descends into `a`, `b`, or `c`. The traversal cost is proportional to the injection output. The final result `(w_u a + w_u b + w_u c) % 2^w` is clean — no intermediate `%` wrappers reach the E-graph. ### Why intermediate terms must not enter the E-graph Simplification sets run to fixpoint *outside* the E-graph. Only the final normal form is internalized. This is critical because intermediate terms are expensive for satellite solvers. For example, the linear arithmetic module processes every `a % b` term by: - Treating `a % b` as a variable. - Adding the constraint `a = b * [a/b] + [a%b]`. - Adding the bound `0 <= [a%b] < b`. An intermediate term like `((w_u a + w_u b) % 2^w + w_u c) % 2^w` would create unnecessary variables and constraints that become immediately redundant after cleanup. ### E-graph pipeline invariant The stop condition relies on a critical invariant: **every term in the E-graph has been through the full pipeline.** This means "in E-graph AND no rule matches → stop" is sound — we know the term and all its descendants have already been processed by all active simplification sets. Currently, some satellite solvers insert auxiliary terms into the E-graph bypassing the standard internalization pipeline. These solvers must be audited and modified to route their terms through the pipeline. This is safe because the pipeline does not destroy terms — the normalizer enforces internal invariants (which satellite solvers already expect), and the simplification sets produce *additional* equivalent terms merged into the same equivalence class. The original auxiliary term survives unchanged in its equivalence class. The number of satellite solver code paths that bypass the pipeline is believed to be small. ### Proof terms and type class instances During rewriting, `simp` may construct `f proof1 x` where the E-graph contains `f proof2 x` (same proposition, different proof term). Pointer equality fails, causing `simp` to treat the term as new. Fix: canonicalize proof and type class instance arguments at the E-graph membership check point. When `simp` checks "is this term in the E-graph?", first canonicalize these arguments against the E-graph's canonical representatives, then do pointer comparison. This is targeted — only at the decision point, not at every rewrite step. ### Implementation: `Sym.simp` The simp set's `simp` call uses `Sym.simp`, which ensures all produced terms are maximally shared. This enables pointer equality for E-graph membership checks — no structural comparison needed. ### Head symbol index A `HashMap HeadSymbol (Array SimpSetId)` pre-filters before disc tree lookups. On internalization of a term `e`, look up `e`'s head symbol to find the relevant simp sets (typically zero or one), then do disc tree lookups only against those sets. Most head symbols are relevant to a single simp set (e.g., `word.unsigned` → `intblast` only). Shared head symbols like `=` may map to multiple sets, but these are also where entry-point rules are most likely to fire, so the additional lookups are not wasted. The index is built once when the `grind` call selects its active simp sets. ## User-facing documentation ### When to use a simplification set A simplification set is appropriate when: 1. **You have a source type and a target type.** For example, `BitVec w` (source) and `Int` (target). 2. **You have an injection function** from source to target. For example, `word.unsigned : BitVec w → Int`. 3. **You have rules that push the injection through source-domain operations.** For example, `word.unsigned (a + b) = (word.unsigned a + word.unsigned b) % 2^w`. 4. **You inject `=` and other relations over the source type.** For example, `(w1 = w2) ↔ (word.unsigned w1 = word.unsigned w2)`. This ensures equalities in the source domain are explicitly captured in the target domain. 5. **The target domain has a solver** that can handle the translated terms. Without a solver, the translation just creates more terms nobody can reason about. ### Example: intblasting ```lean -- Define the simplification set grind_simp_set intblast -- Inject relations (entry points) @[intblast] theorem eq_unsigned : (w1 = w2) ↔ (word.unsigned w1 = word.unsigned w2) := ... @[intblast] theorem ltu_unsigned : (word.ltu w1 w2) ↔ (word.unsigned w1 < word.unsigned w2) := ... -- Push injection through operations @[intblast] theorem unsigned_add : word.unsigned (word.add x y) = (word.unsigned x + word.unsigned y) % 2^w := ... @[intblast] theorem unsigned_mul : word.unsigned (word.mul x y) = (word.unsigned x * word.unsigned y) % 2^w := ... -- Cleanup rules (remove redundant modular wrappers) @[intblast] theorem mod_add_mod : (a % m + b) % m = (a + b) % m := ... ``` ### Checklist for authors Before creating a simplification set, verify: - [ ] **Injection of `=`**: the set includes a rule translating equality over the source type. Biconditional if h is injective, forward-only if not. Without this, reasoning modulo equalities is lost. - [ ] **Coverage of operations**: every source-domain operation that may appear in user terms has a corresponding injection rule. Missing operations leave untranslated subterms. - [ ] **Cleanup rules**: the injection may produce redundant structure in the target domain (e.g., nested `% 2^w`). Include cleanup rules to keep the translated terms simple. This matters for performance — every term internalized in the E-graph is processed by satellite solvers. - [ ] **Confluence**: the rule set should be confluent. Non-confluent rules may produce different results depending on application order, leading to unpredictable behavior. - [ ] **Termination**: the rule set should terminate. Typically, injection rules decrease a natural measure (e.g., nesting depth of source-domain constructors under the injection function). - [ ] **Target solver exists**: the target domain must have a dedicated solver in `grind`. Without one, the translation creates terms nobody can reason about. ### What simplification sets are NOT for Grind simplification sets are not a general-purpose rewriting mechanism. They are designed for **translating between domains where a dedicated solver handles the target**. Do not use them for: - **Rewriting within a single domain.** A rule like `?a ^ (?n + ?m) → ?a ^ ?n * ?a ^ ?m` does not translate between types — it restructures `Nat` into `Nat`. There's no injection function, no `=` injection, and no dedicated solver on the other side. Use E-matching instead. - **Non-confluent rule sets.** If your rules can produce different results depending on application order, use E-matching, which adds all matching instances and lets the E-graph resolve the connections. ## Relationship to other mechanisms | Mechanism | When it fires | Modulo E-graph? | Rule type | |-----------|--------------|-----------------|-----------| | Normalizer (`@[grind norm]`) | Before internalization | No | Internal invariants | | simplification sets | After normalization | No (syntactic) | Domain translations | | E-matching | On E-graph merge | Yes | Conditional, quantified | These are complementary: - Simplification sets handle syntactic translation of new terms to target domains with dedicated solvers. - E-matching handles reasoning that depends on equalities learned later. - The normalizer enforces internal invariants. ## Open items 1. **Migration of existing `@[grind norm]` rules.** Many current norm rules may belong elsewhere. Inventory needed to identify which must remain as normalization (internal invariant) vs. which are "useful rewrites" better suited as E-matching theorems. 2. **Diagnostics.** Extend existing `grind` tracing to cover the full pipeline: which set fired, what it produced, what was internalized.

Syntax	Example	Reference
# Header	Header	基本排版
- Unordered List	Unordered List
1. Ordered List	Ordered List
- [ ] Todo List	Todo List
> Blockquote	Blockquote
Bold font	Bold font
Italics font	Italics font
~~Strikethrough~~	~~Strikethrough~~
19^th^	19^th
H~2~O	H₂O
++Inserted text++	Inserted text
==Marked text==	Marked text
[link text](https:// "title")	Link
![image alt](https:// "title")	Image
`Code`	`Code`	在筆記中貼入程式碼
```javascript var i = 0; ```	`var i = 0;`
:smile:		Emoji list
{%youtube youtube_id %}	Externals
$L^aT_eX$	L^aT_eX
:::info This is a alert area. :::	This is a alert area.