diff --git a/CHANGELOG.md b/CHANGELOG.md
index e813c44..2c0bbf9 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -8,6 +8,9 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 ## [Unreleased]
 
 ### Added
+- **A rewriting toolkit for stored source** (`Superscript\Axiom\Rewrite`, documented in `docs/rewriting.md`). `Rewriter::rewrite(Expression): RewriteRun` applies a set of `RewriteRule`s bottom-up over an immutable source tree and returns the new tree plus a report of every site a rule fired, every site a rule was refused, and every shape the walk could not see inside; report-only is the same run with the tree ignored. A rule owns matching and replacement for the exact `Source` classes it visits and writes no traversal — descent is the toolkit's, dispatch is one array lookup per node, and untouched subtrees come back as the same instance, so `RewriteRun::$changed` is answered by identity. Core node descent is exhaustive by law (a test reflects over `src/Sources` and fails on a class without an arm); host shapes register through `Extension::sourceDescenders()` with the exact, unranked ownership `sourceCompilers()` already uses. **A class no extension claims is an opaque leaf** — never descended, never rewritten, and named in the report rather than silently skipped, so a forgotten arm cannot read as a clean tree.
+  - **Nothing is applied that was not proved.** Every replacement is compiled against the expression's own dialect, definitions and declarations, and must certify the same type as what it replaces — or refuse identically, so a rewrite is never what changes the diagnostic an author reads. A rule may claim more: `Preservation::Verdict` runs both programs over a host `BindingsCorpus` and compares answers case by case, with disagreements naming the case. A broken obligation refuses that one site and reports it; a claim the run has no oracle for is reported *unchecked*, which neither blocks a rewrite nor counts as evidence for one. Subtrees compile standalone in the whole expression's scope exactly because the language has no binding form.
+  - `Rules\RemoveDoubleNegation` is the reference rule: `!!x` becomes `x` for either spelling of core negation. It is neutral because core's `!` is the only row for its symbol — Boolean in, Boolean out — so a `!!x` that compiles has an operand of `Boolean` or, lifted, `Boolean?`, and on both the operation is total and involutive. `!!count` over a Number is refused rather than simplified: the original never compiled, and the replacement would be a certified Number program nobody wrote. `Rules\\RemoveRedundantDefault` is the other shape a rule takes — one whose applicability matching cannot settle: `x ?? 0` is the identity exactly when `x` can never be absent, which is a fact about types, so the rule proposes the removal everywhere and type preservation decides site by site (`Number` against `Number?` refuses the ones absence can reach).
 - **Declarations and records now use one required-by-default property model.** `Expression::$declarations` is a `RecordType` (array input remains shorthand), and every bare property must exist. `new Optional(new NumberType())` permits a property to be omitted without turning `Optional` into a `Type`; `OptionType` independently permits an explicitly supplied absent value. This makes all four useful states representable: required `T`, required `Option<T>`, optional `T`, and optional `Option<T>`. Missing optional properties remain missing during record coercion rather than being canonicalized to `null`.
 - **Input paths are structural.** `SymbolSource` names only root symbols and `MemberAccessSource` traverses one record property per node; empty and dotted member names are rejected. Declarations and bindings are nested records; flat dotted namespaces and the namespace argument on `SymbolSource` are removed. Compiler-resolved reads remain `ReferencePath` values through programs and diagnostics, serialize as `{"root":"customer","properties":["turnover"]}`, and render as `customer.turnover` only when `describe()` is requested. Compilation projects the declaration record to only the paths the program reads while preserving required/optional qualifiers at every level.
 - **Compilation that reports everything wrong, not just the first thing.** `Expression::diagnose(): Diagnosis` compiles for the sake of what compilation learns: every refusal in the expression, the access paths it read even through the parts that refuse, the root type, and — when nothing refused — the certified `Program`, through `Diagnosis::program(): Result<Program, non-empty-list<TypeMismatch>>`. `mystery > 1000 && postcode == 'SW1'` with `mystery` undeclared reports one diagnostic (the unbound symbol), still type-checks the right-hand comparison, and still reports the `mystery` and `postcode` references — where `compile()` reports the unbound symbol and stops. `compile()` is one attempt of the same walk and behaves exactly as before: its refusal is the diagnosis' first diagnostic, same message, same path.
diff --git a/CONTEXT.md b/CONTEXT.md
index f3d83bc..08cd02b 100644
--- a/CONTEXT.md
+++ b/CONTEXT.md
@@ -9,6 +9,7 @@
 - **SourceCompilation** is the straight-line capability passed to a source compiler. It compiles child sources in the current type environment, resolves symbols, binds typed infix and prefix operations from the composed dialect, types embedded PHP values literal-first, and constructs `CompiledSource` values. Nested refusals automatically return through `Expression::compile()`; source compiler callbacks do not compose compilation `Result` values themselves.
 - A **CompilationAnalysis** is the data-only explanation emitted by the same successful compilation that builds a `Program`. Its source graph carries certified return types and source-compiler ownership; its operator selections carry operand and return types plus the stable identity, implementation, and extension of the rule that won. It contains no evaluations or captured collaborators and is not a persistence format for sources. Serializable exports redact literal values by default.
 - A **Program** is the ephemeral compiled artifact. Its evaluation closures may capture live services from extensions, so programs are executed and sources are persisted.
+- A **rewrite rule** owns matching and replacement for exact `Source` classes; **descent** — reaching a node's children and rebuilding it around new ones — belongs to the rewriter, registered per exact class the way source compilers are (`Extension::sourceDescenders()`), so structural knowledge lives in rules and arms and never as a method on `Source`. A class with no arm is an **opaque leaf**: never descended, never rewritten, always reported. A replacement is applied only once it discharges its **preservation obligations** — certified type always, runtime verdicts when the host supplies a bindings corpus — and a broken one refuses that site rather than the run. Rewriting is a tool over stored sources: it runs before compilation and no compiled artifact knows about it.
 - An **execution observer** belongs to one `Program` invocation. Core emits an ordered lifecycle for every compiled source node; tracing and telemetry packages interpret those events. Observers are never stored on sources, expressions, or programs.
 
 Use “source compiler” for this seam. Do not call it a resolver: runtime source resolution and its delegating registry were removed by the compilation pivot.
diff --git a/README.md b/README.md
index a391f0d..50dca9f 100644
--- a/README.md
+++ b/README.md
@@ -18,6 +18,7 @@ The design principle is **compile, then trust**: `Expression::compile()` type-ch
     - [Operators](#operators)
     - [Execution Observation](#execution-observation)
 - [Extending Axiom](#extending-axiom)
+- [Rewriting Stored Source](#rewriting-stored-source)
 - [Development](#development)
 - [License](#license)
 
@@ -538,6 +539,23 @@ Use **[the extension guide](docs/extending-axiom.md)** for a progressive tutoria
 | Add a data source | `Extension::sourceCompilers()` plus composable `CompiledSource` values; sources stay data-only | Host sources |
 | Add match pattern kinds | (reserved: an `Extension::matchers()` hook can be added without breaking implementors) | — |
 | Prove your rules honest | the totality harness + admission-honesty law patterns | Testing your extension |
+| Rewrite a stored corpus | `Extension::sourceDescenders()` plus `RewriteRule` implementations | [Rewriting Stored Source](docs/rewriting.md) |
+
+## Rewriting Stored Source
+
+A host that stores expressions eventually has to change them in bulk. `Rewrite\Rewriter` applies a set of `RewriteRule`s bottom-up over an immutable source tree and returns the new tree with a report of what it did:
+
+```php
+$run = (new Rewriter([new RemoveDoubleNegation()]))->rewrite($expression);
+
+$run->report->describe(); // dry run: read this, take nothing
+$run->changed;            // false when every subtree came back identical
+$run->source;             // the tree to store
+```
+
+Nothing is applied that was not proved. Every replacement is compiled against the expression's own declarations and must certify the same type as what it replaces — or refuse identically; a rule may also claim verdict preservation, which the run checks against a host `BindingsCorpus`. A broken obligation refuses that one site and reports it, because a fold that type-checks can still invert the meaning of a condition. A node class with no descent arm is an opaque leaf: never descended, never rewritten, and always named in the report.
+
+See **[Rewriting Stored Source](docs/rewriting.md)** for rules, descent, obligations, and the report.
 
 ## Development
 
diff --git a/docs/rewriting.md b/docs/rewriting.md
new file mode 100644
index 0000000..cebbe38
--- /dev/null
+++ b/docs/rewriting.md
@@ -0,0 +1,240 @@
+# Rewriting Stored Source
+
+- [Why](#why)
+- [A Worked Example](#a-worked-example)
+- [Rules](#rules)
+- [Descent, and the Opaque-Leaf Policy](#descent-and-the-opaque-leaf-policy)
+- [Obligations](#obligations)
+- [The Report](#the-report)
+- [Writing a Rule](#writing-a-rule)
+- [When the Rule Cannot Decide](#when-the-rule-cannot-decide)
+- [What Is Not a Source Rewrite](#what-is-not-a-source-rewrite)
+
+## Why
+
+A host that stores expressions accumulates a corpus it did not write all at once: thousands of conditions authored over years, against a language that has since grown a better spelling for something. Editing them by hand is a migration nobody finishes; editing them with a script is a migration nobody can prove.
+
+This is the toolkit for the middle path: a rule set applied to stored source, bottom-up over an immutable tree, where every replacement must discharge an obligation before it is applied, and everything the run did — and everything it could not see — is reported.
+
+## A Worked Example
+
+An author wrote a double negation, and the corpus has 400 more like it:
+
+```php
+use Superscript\Axiom\Expression;
+use Superscript\Axiom\Rewrite\{ArrayBindingsCorpus, Rewriter, VerdictPreservation};
+use Superscript\Axiom\Rewrite\Rules\RemoveDoubleNegation;
+use Superscript\Axiom\Sources\{InfixExpression, StaticSource, SymbolSource, UnaryExpression};
+use Superscript\Axiom\Types\{BooleanType, NumberType, OptionType, Optional};
+
+$not = fn ($source) => new UnaryExpression('!', $source);
+
+$expression = new Expression(
+    source: new InfixExpression(
+        $not($not(new InfixExpression(new SymbolSource('roof'), '>', new StaticSource(0.25)))),
+        '&&',
+        $not($not(new SymbolSource('flag'))),
+    ),
+    declarations: [
+        'roof' => new Optional(new OptionType(new NumberType())),
+        'flag' => new BooleanType(),
+    ],
+);
+
+$rewriter = new Rewriter(
+    [new RemoveDoubleNegation()],
+    obligations: [new VerdictPreservation(new ArrayBindingsCorpus([
+        'answered' => ['roof' => 0.3, 'flag' => true],
+        'unanswered' => ['flag' => false],
+    ]))],
+);
+
+$run = $rewriter->rewrite($expression);
+```
+
+Read the report first and take nothing — that is the dry run:
+
+```
+applied axiom.rewrite.remove-double-negation at $.left: !!(roof > 0.25) => roof > 0.25
+  type preservation upheld: both compile to Boolean?
+  verdict preservation upheld: 2 corpus case(s) agree
+applied axiom.rewrite.remove-double-negation at $.right: !!flag => flag
+  type preservation upheld: both compile to Boolean
+  verdict preservation upheld: 2 corpus case(s) agree
+```
+
+Then take the tree:
+
+```php
+$run->changed;             // true
+$run->source->describe();  // (roof > 0.25) && flag
+$run->expression();        // the same dialect, definitions, declarations and boundary over the new tree
+```
+
+There is no mode flag: report-only is this same run with the tree ignored.
+
+Now the same rule against a stored expression that never compiled — `!!count` where `count` is a Number:
+
+```
+refused axiom.rewrite.remove-double-negation at $: !!count => count
+  type preservation broken: the original refuses and the replacement compiles: [!] expects Boolean; got Number.
+  Number is not assignable to Boolean.
+  verdict preservation unchecked: the run was given no oracle for this claim
+```
+
+`$run->changed` is `false` and `$run->source` is the very tree that went in. Simplifying here would have handed back a certified Number program in place of a refusal — a program the author never wrote and the checker never blessed. One site is refused; the rest of the run proceeds.
+
+## Rules
+
+A rule owns matching and replacement for exact source classes:
+
+```php
+interface RewriteRule
+{
+    public function identifier(): string;
+
+    /** @return non-empty-list<class-string<Source>> */
+    public function visits(): array;
+
+    public function rewrite(Source $source): ?Source;   // null = nothing to do here
+
+    /** @return list<Preservation> */
+    public function preserves(): array;
+}
+```
+
+Structural knowledge lives here rather than on `Source`, and descent lives in the toolkit. A `Source` is data a host persists; every method the language puts on it is a method every host node must implement forever. A rule that only rewrites `!!x` needs to know about exactly two node shapes, and writes no traversal at all.
+
+Dispatch is by exact class, the same ownership model source compilers use: rules are indexed by the classes they visit, so a node costs one array lookup however many rules the run carries. A rule listing a parent class is never offered a subclass.
+
+At each node, rules registered for its class are offered in registration order until one takes it. A rule that returns `null` is passed over; a rule whose replacement breaks an obligation is recorded refused and the next rule is asked; the first sound replacement wins and ends the visit.
+
+## Descent, and the Opaque-Leaf Policy
+
+The walk is bottom-up: a node's children are rewritten, the node is rebuilt around whatever came back, and only then are rules offered the rebuilt node. A rule therefore always sees the shape that will actually be stored, and one pass collapses a nest — `!!!!x` reduces at every level on the way out.
+
+**Structural sharing.** A node whose children all came back identical is returned as-is, so an untouched subtree is the same instance in the new tree. `$run->changed` is answered by identity, not comparison.
+
+**Core shapes** are the toolkit's own: `CoreSourceDescenders` has an arm per node class, and an exhaustiveness law reflects over `src/Sources` and fails if a class exists without one.
+
+**Host shapes** register through the extension a package already ships:
+
+```php
+final class BoxExtension extends Extension
+{
+    public function sourceDescenders(): array
+    {
+        return [BoxSource::class => $this->descend(...)];
+    }
+
+    private function descend(BoxSource $source, Descent $descent): Source
+    {
+        $inner = $descent->child($source->inner, 'inner');
+
+        return $inner === $source->inner ? $source : new BoxSource($inner);
+    }
+}
+
+$rewriter = new Rewriter($rules, SourceDescenders::core()->with(new BoxExtension()));
+```
+
+An arm asks for each child by the property holding it — that name is the path segment the report prints — and returns the same instance when no child moved. Ownership is exact and unranked: two extensions claiming one class is a configuration error.
+
+**A class no extension claims is an opaque leaf.** It is never descended, never rewritten — not even by a rule naming its own class, because a rule cannot be trusted to rebuild a shape the toolkit cannot take apart — and it is *reported*:
+
+```
+opaque Acme\Sources\LookupSource at $.right: LookupSource
+```
+
+Silence would be the dangerous answer. A host that adds a source class and forgets its descent arm would read "no rewrites needed" as "nothing to do" for as long as the omission lasted.
+
+## Obligations
+
+A rule declares what it preserves; the run checks what it can.
+
+| Preservation | Oracle | When |
+| --- | --- | --- |
+| `CertifiedType` | compile both subtrees in the expression's declaration scope | always, whether or not the rule claims it |
+| `Verdict` | run both programs over a `BindingsCorpus` and compare answers | when the run is given a `VerdictPreservation` |
+
+Both subtrees are compiled standalone *in the whole expression's scope*, which is exact rather than approximate because the language has no binding form: no node introduces a name for its children, so a subtree reads the same environment wherever it sits.
+
+Type preservation demands the same certified type — or the same refusal, since neither tree can then run and a rewrite must not be what changes the diagnostic an author reads.
+
+Verdict preservation is evidence, not proof: only the host knows what its programs are fed, and a corpus that never exercises a branch says nothing about it. Its cases are labelled, because a disagreement has to be reproducible:
+
+```
+verdict preservation broken: case [zero]: the original answers error(Division by zero) and the replacement value(5)
+```
+
+A verdict comes in three states, and the report keeps them apart: **upheld** (checked, and it holds), **broken** (checked, and it does not — the site is refused), and **unchecked** (no oracle was supplied, so nothing is known either way). Unchecked never blocks a rewrite and never counts as evidence for one.
+
+## The Report
+
+```php
+$run->report->applied();  // list<RewriteRecord>: rule, path, before, after, verdicts
+$run->report->refused();  // the same, for replacements an obligation broke
+$run->report->opaque;     // list<OpaqueSource>: path, class, describe
+$run->report->describe(); // all of it, as text
+```
+
+Paths are property-named: `$.left.operand`, `$.arms[1].expression`. That is deliberately not the `$.children[0].node` language compilation failures and analyses speak — those number the children a *compiler* recorded, and a compiler records what it needs (a wildcard arm records no pattern child at all), so the same arm sits at a different index depending on which patterns precede it. A coordinate into stored source has to name the same node before anything is compiled.
+
+## Writing a Rule
+
+`RemoveDoubleNegation` is the reference. What makes it sound is worth copying, more than the code is:
+
+```php
+public function rewrite(Source $source): ?Source
+{
+    if (! $source instanceof UnaryExpression || ! $this->negates($source->operator)) {
+        return null;
+    }
+
+    $operand = $source->operand;
+
+    if (! $operand instanceof UnaryExpression || ! $this->negates($operand->operator)) {
+        return null;
+    }
+
+    return $operand->operand;
+}
+```
+
+The neutrality argument is about the *dialect*, not the shape. Core's `!` is the only row for that symbol: it takes Boolean and returns Boolean. So a `!!x` that compiles at all has an `x` of `Boolean` or, through the resolver's lift, `Boolean?`. On `Boolean`, `!` is total and involutive. On `Boolean?` the resolver lifts that same row, and lifting is functorial — absence propagates through each negation untouched, so `!!` is the lift of `!∘!`, the identity. Every operand type the rewrite can meet is one it is neutral on.
+
+Note what the argument rests on, and say so in the rule: a host is free to register `!` over its own type and make it something other than an involution, so the spellings are a constructor argument (`new RemoveDoubleNegation(['!'])`) rather than a constant. The obligations then check what the argument assumed rather than trusting it — which is the point. A fold that type-checks can still invert the meaning of a condition, and a rewrite nobody proved is a rewrite nobody should store.
+
+## When the Rule Cannot Decide
+
+`RemoveRedundantDefault` is the other shape a rule takes: one whose applicability is not decided by matching at all.
+
+A `DefaultValue` over a source that can never be absent is already the identity — the compiler returns the inner compiled source untouched, default and all — so the node is noise in stored source, and it reads as if absence were possible where it is not. But whether the inner source can be absent is a fact about *types*, and no amount of looking at the tree settles it.
+
+So the rule proposes the removal everywhere and lets the obligation settle it:
+
+```php
+public function rewrite(Source $source): ?Source
+{
+    return $source instanceof DefaultValue ? $source->source : null;
+}
+```
+
+Over an optional inner, `x ?? 0` certifies `Number` while `x` certifies `Number?`; the types differ and the site is refused. Over a definite inner, both certify the same type — necessarily, since they compile to the same node — and the rewrite is taken. In `amount ?? 1 ?? 0` with `amount` optional, the inner default — the one absence can actually reach — is refused, and the outer one, which never fires, is removed:
+
+```
+refused axiom.rewrite.remove-redundant-default at $.source: amount ?? 1 => amount
+  type preservation broken: the original compiles to Number and the replacement to Number?
+  verdict preservation unchecked: the run was given no oracle for this claim
+applied axiom.rewrite.remove-redundant-default at $: amount ?? 1 ?? 0 => amount ?? 1
+  type preservation upheld: both compile to Number
+  verdict preservation unchecked: the run was given no oracle for this claim
+```
+
+Removing the node does change what an execution observer sees — the `default` label and its annotations go with it. That is a change to the program's trace, not to what it answers.
+
+## What Is Not a Source Rewrite
+
+A migration only becomes a rewrite rule once both the old and new shapes are representable as `Source` trees. Where a language change removed the old shape from the node set, there is nothing for a rule to match: the old form cannot be hydrated into any `Source` at all, and the migration belongs in the host's deserializer, before a tree exists.
+
+The namespaced-symbol migration is exactly that case. `SymbolSource` no longer carries a namespace, and its constructor rejects a dotted name outright, so stored `{"name": "turnover", "namespace": "customer"}` has no `Source` to become except the one the host's hydration chooses — `MemberAccessSource(SymbolSource('customer'), 'turnover')`. Reach for this toolkit for changes *within* the node set; reach for the wire format for changes *to* it.
diff --git a/src/Extension.php b/src/Extension.php
index 2343ebf..1b4dbd1 100644
--- a/src/Extension.php
+++ b/src/Extension.php
@@ -100,4 +100,24 @@ public function sourceCompilers(): array
     {
         return [];
     }
+
+    /**
+     * Exact host Source class → how to descend into it and rebuild it, for
+     * {@see \Superscript\Axiom\Rewrite\Rewriter}. Registration mirrors
+     * {@see sourceCompilers()} — exact ownership, no precedence — so one
+     * package declares both how its node compiles and how a rewrite reaches
+     * through it, and the two cannot end up in different places. A class no
+     * extension claims is an opaque leaf: never descended, never rewritten,
+     * and named in the run's report.
+     *
+     * An arm receives its source and a {@see \Superscript\Axiom\Rewrite\Descent},
+     * asks for each child by the property holding it, and returns the same
+     * instance when no child moved.
+     *
+     * @return array<class-string<Source>, callable(Source, \Superscript\Axiom\Rewrite\Descent): Source>
+     */
+    public function sourceDescenders(): array
+    {
+        return [];
+    }
 }
diff --git a/src/Rewrite/ArrayBindingsCorpus.php b/src/Rewrite/ArrayBindingsCorpus.php
new file mode 100644
index 0000000..5694539
--- /dev/null
+++ b/src/Rewrite/ArrayBindingsCorpus.php
@@ -0,0 +1,21 @@
+<?php
+
+declare(strict_types=1);
+
+namespace Superscript\Axiom\Rewrite;
+
+/**
+ * A corpus written out by hand: the shape a test or a small fixture set
+ * takes. A host with a real corpus streams it from storage instead.
+ */
+final readonly class ArrayBindingsCorpus implements BindingsCorpus
+{
+    /** @param array<string, array<string, mixed>> $cases */
+    public function __construct(private array $cases) {}
+
+    /** @return iterable<string, array<string, mixed>> */
+    public function cases(): iterable
+    {
+        return $this->cases;
+    }
+}
diff --git a/src/Rewrite/BindingsCorpus.php b/src/Rewrite/BindingsCorpus.php
new file mode 100644
index 0000000..a5ffd0d
--- /dev/null
+++ b/src/Rewrite/BindingsCorpus.php
@@ -0,0 +1,20 @@
+<?php
+
+declare(strict_types=1);
+
+namespace Superscript\Axiom\Rewrite;
+
+/**
+ * The host's evidence that two programs answer alike: bindings sets drawn
+ * from data the host believes representative — stored applications, recorded
+ * requests, a generated sweep. Only the host knows what its programs are fed,
+ * so the toolkit asks for the cases rather than inventing them.
+ *
+ * A case is labelled because a disagreement has to be reproducible: the
+ * report names the case that disagreed, not the ordinal of an anonymous row.
+ */
+interface BindingsCorpus
+{
+    /** @return iterable<string, array<string, mixed>> label => bindings */
+    public function cases(): iterable;
+}
diff --git a/src/Rewrite/CoreSourceDescenders.php b/src/Rewrite/CoreSourceDescenders.php
new file mode 100644
index 0000000..90de9d9
--- /dev/null
+++ b/src/Rewrite/CoreSourceDescenders.php
@@ -0,0 +1,153 @@
+<?php
+
+declare(strict_types=1);
+
+namespace Superscript\Axiom\Rewrite;
+
+use Superscript\Axiom\Source;
+use Superscript\Axiom\Sources\Ascription;
+use Superscript\Axiom\Sources\Coerce;
+use Superscript\Axiom\Sources\DefaultValue;
+use Superscript\Axiom\Sources\ExpressionPattern;
+use Superscript\Axiom\Sources\InfixExpression;
+use Superscript\Axiom\Sources\LiteralPattern;
+use Superscript\Axiom\Sources\MatchExpression;
+use Superscript\Axiom\Sources\MatchPattern;
+use Superscript\Axiom\Sources\MemberAccessSource;
+use Superscript\Axiom\Sources\StaticSource;
+use Superscript\Axiom\Sources\SymbolSource;
+use Superscript\Axiom\Sources\UnaryExpression;
+use Superscript\Axiom\Sources\WildcardPattern;
+
+/**
+ * The language's descent registry: for each core node, how to reach its
+ * children and how to put the node back together around rewritten ones.
+ *
+ * The core node set is closed, so this map is exhaustive by law rather than
+ * by habit — `CoreDescentExhaustivenessTest` reflects over `src/Sources` and
+ * fails the moment a node class exists without an arm. Without that law a new
+ * node would quietly become an opaque leaf and every rewrite beneath it would
+ * silently stop happening.
+ *
+ * Every arm shares structure: a node whose children all came back identical
+ * is returned as-is rather than reconstructed, so an untouched subtree is the
+ * same instance in the new tree and `===` answers "did anything change?" for
+ * the whole run.
+ *
+ * Patterns get their own map because they are not sources: they cannot be
+ * rewritten by a rule and cannot be extended by a host — the match compiler
+ * refuses a pattern it does not know — but an expression pattern holds a
+ * source, and a rewrite inside one is an ordinary rewrite.
+ */
+final readonly class CoreSourceDescenders
+{
+    /**
+     * @return array<class-string<Source>, callable(Source, Descent): Source>
+     */
+    public static function sources(): array
+    {
+        /** @var array<class-string<Source>, callable(Source, Descent): Source> */
+        return [
+            StaticSource::class => self::leaf(...),
+            SymbolSource::class => self::leaf(...),
+            Coerce::class => self::coerce(...),
+            Ascription::class => self::ascription(...),
+            DefaultValue::class => self::defaultValue(...),
+            MemberAccessSource::class => self::memberAccess(...),
+            UnaryExpression::class => self::unary(...),
+            InfixExpression::class => self::infix(...),
+            MatchExpression::class => self::matchExpression(...),
+        ];
+    }
+
+    /**
+     * @return array<class-string<MatchPattern>, callable(MatchPattern, Descent): MatchPattern>
+     */
+    public static function patterns(): array
+    {
+        /** @var array<class-string<MatchPattern>, callable(MatchPattern, Descent): MatchPattern> */
+        return [
+            WildcardPattern::class => self::leafPattern(...),
+            LiteralPattern::class => self::leafPattern(...),
+            ExpressionPattern::class => self::expressionPattern(...),
+        ];
+    }
+
+    /** A node with no source children: there is nothing under it to rewrite. */
+    private static function leaf(Source $source, Descent $descent): Source
+    {
+        return $source;
+    }
+
+    private static function leafPattern(MatchPattern $pattern, Descent $descent): MatchPattern
+    {
+        return $pattern;
+    }
+
+    private static function coerce(Coerce $source, Descent $descent): Source
+    {
+        $inner = $descent->child($source->source, 'source');
+
+        return $inner === $source->source ? $source : new Coerce($source->type, $inner);
+    }
+
+    private static function ascription(Ascription $source, Descent $descent): Source
+    {
+        $inner = $descent->child($source->source, 'source');
+
+        return $inner === $source->source ? $source : new Ascription($source->type, $inner);
+    }
+
+    private static function defaultValue(DefaultValue $source, Descent $descent): Source
+    {
+        $inner = $descent->child($source->source, 'source');
+
+        return $inner === $source->source ? $source : new DefaultValue($inner, $source->default);
+    }
+
+    private static function memberAccess(MemberAccessSource $source, Descent $descent): Source
+    {
+        $object = $descent->child($source->object, 'object');
+
+        return $object === $source->object ? $source : new MemberAccessSource($object, $source->property);
+    }
+
+    private static function unary(UnaryExpression $source, Descent $descent): Source
+    {
+        $operand = $descent->child($source->operand, 'operand');
+
+        return $operand === $source->operand ? $source : new UnaryExpression($source->operator, $operand);
+    }
+
+    private static function infix(InfixExpression $source, Descent $descent): Source
+    {
+        $left = $descent->child($source->left, 'left');
+        $right = $descent->child($source->right, 'right');
+
+        return $left === $source->left && $right === $source->right
+            ? $source
+            : new InfixExpression($left, $source->operator, $right);
+    }
+
+    private static function matchExpression(MatchExpression $source, Descent $descent): Source
+    {
+        $subject = $descent->child($source->subject, 'subject');
+        $arms = [];
+        $moved = $subject !== $source->subject;
+
+        foreach ($source->arms as $index => $arm) {
+            $rewritten = $descent->arm($arm, sprintf('arms[%d]', $index));
+            $moved = $moved || $rewritten !== $arm;
+            $arms[] = $rewritten;
+        }
+
+        return $moved ? new MatchExpression($subject, $arms) : $source;
+    }
+
+    private static function expressionPattern(ExpressionPattern $pattern, Descent $descent): MatchPattern
+    {
+        $inner = $descent->child($pattern->source, 'source');
+
+        return $inner === $pattern->source ? $pattern : new ExpressionPattern($inner);
+    }
+}
diff --git a/src/Rewrite/Descent.php b/src/Rewrite/Descent.php
new file mode 100644
index 0000000..5bbf05c
--- /dev/null
+++ b/src/Rewrite/Descent.php
@@ -0,0 +1,43 @@
+<?php
+
+declare(strict_types=1);
+
+namespace Superscript\Axiom\Rewrite;
+
+use Superscript\Axiom\Source;
+use Superscript\Axiom\Sources\MatchArm;
+use Superscript\Axiom\Sources\MatchPattern;
+
+/**
+ * The straight-line capability a descent arm is handed: rewrite this child,
+ * and tell me where it sits. It is bound to the node being descended, so an
+ * arm names the property holding each child — `'left'`, `'arms[1]'` — and
+ * never assembles a path.
+ *
+ * The rewritten child comes back; an arm compares it against the one it had
+ * to decide whether to rebuild. That comparison is the arm's, because only
+ * the arm knows how to put its node back together.
+ */
+final readonly class Descent
+{
+    /** @internal Built by the walk, one per node. */
+    public function __construct(
+        private RewriteWalk $walk,
+        private SourcePath $path,
+    ) {}
+
+    public function child(Source $source, string $segment): Source
+    {
+        return $this->walk->source($source, $this->path->child($segment));
+    }
+
+    public function pattern(MatchPattern $pattern, string $segment): MatchPattern
+    {
+        return $this->walk->pattern($pattern, $this->path->child($segment));
+    }
+
+    public function arm(MatchArm $arm, string $segment): MatchArm
+    {
+        return $this->walk->arm($arm, $this->path->child($segment));
+    }
+}
diff --git a/src/Rewrite/Describes.php b/src/Rewrite/Describes.php
new file mode 100644
index 0000000..6a3df81
--- /dev/null
+++ b/src/Rewrite/Describes.php
@@ -0,0 +1,26 @@
+<?php
+
+declare(strict_types=1);
+
+namespace Superscript\Axiom\Rewrite;
+
+use ReflectionClass;
+use Superscript\Axiom\Describable;
+
+/**
+ * How a report renders one node. A rewrite report is read by a human
+ * deciding whether to take the new tree, so it shows the node the way the
+ * language spells it whenever the node can spell itself, and falls back to
+ * its class name when a host node cannot.
+ *
+ * @internal
+ */
+final readonly class Describes
+{
+    public static function node(object $node): string
+    {
+        return $node instanceof Describable
+            ? $node->describe()
+            : (new ReflectionClass($node))->getShortName();
+    }
+}
diff --git a/src/Rewrite/Obligation.php b/src/Rewrite/Obligation.php
new file mode 100644
index 0000000..e3aeda5
--- /dev/null
+++ b/src/Rewrite/Obligation.php
@@ -0,0 +1,18 @@
+<?php
+
+declare(strict_types=1);
+
+namespace Superscript\Axiom\Rewrite;
+
+/**
+ * The oracle for one {@see Preservation}. A run holds at most one obligation
+ * per preservation — supplying a second for the same one replaces it, the way
+ * a host swaps an oracle rather than ranking two.
+ */
+interface Obligation
+{
+    /** Which claim this obligation discharges. */
+    public function preservation(): Preservation;
+
+    public function check(RewriteSite $site): ObligationVerdict;
+}
diff --git a/src/Rewrite/ObligationVerdict.php b/src/Rewrite/ObligationVerdict.php
new file mode 100644
index 0000000..68f6e00
--- /dev/null
+++ b/src/Rewrite/ObligationVerdict.php
@@ -0,0 +1,49 @@
+<?php
+
+declare(strict_types=1);
+
+namespace Superscript\Axiom\Rewrite;
+
+/**
+ * The answer one {@see Obligation} gives about one site, in three states
+ * that a report must keep apart: upheld (checked, and it holds), broken
+ * (checked, and it does not — the rewrite is refused), and unchecked (no
+ * oracle was available, so nothing is known either way). Unchecked never
+ * blocks a rewrite and never counts as evidence for one; it is the run
+ * saying out loud what it did not prove.
+ */
+final readonly class ObligationVerdict
+{
+    private function __construct(
+        public Preservation $preservation,
+        public bool $checked,
+        public bool $broken,
+        public string $explanation,
+    ) {}
+
+    public static function upheld(Preservation $preservation, string $explanation): self
+    {
+        return new self($preservation, checked: true, broken: false, explanation: $explanation);
+    }
+
+    public static function broken(Preservation $preservation, string $explanation): self
+    {
+        return new self($preservation, checked: true, broken: true, explanation: $explanation);
+    }
+
+    public static function unchecked(Preservation $preservation, string $explanation): self
+    {
+        return new self($preservation, checked: false, broken: false, explanation: $explanation);
+    }
+
+    public function describe(): string
+    {
+        $status = match (true) {
+            ! $this->checked => 'unchecked',
+            $this->broken => 'broken',
+            default => 'upheld',
+        };
+
+        return sprintf('%s %s: %s', $this->preservation->describe(), $status, $this->explanation);
+    }
+}
diff --git a/src/Rewrite/OpaqueSource.php b/src/Rewrite/OpaqueSource.php
new file mode 100644
index 0000000..c07d630
--- /dev/null
+++ b/src/Rewrite/OpaqueSource.php
@@ -0,0 +1,35 @@
+<?php
+
+declare(strict_types=1);
+
+namespace Superscript\Axiom\Rewrite;
+
+/**
+ * A node the run could not see inside: its class has no descent arm, so the
+ * walk stopped there. Nothing beneath it was visited and no rule was offered
+ * it — including rules that name its own class, because a rule cannot be
+ * trusted to rebuild a shape the toolkit cannot take apart.
+ *
+ * Reporting one is the whole point. A silent skip would let a host add a
+ * source class, forget its descent arm, and read "no rewrites needed" as
+ * "nothing to do" for as long as the omission lasted.
+ */
+final readonly class OpaqueSource
+{
+    /** @param class-string $class */
+    private function __construct(
+        public string $path,
+        public string $class,
+        public string $describe,
+    ) {}
+
+    public static function at(SourcePath $path, object $node): self
+    {
+        return new self($path->describe(), $node::class, Describes::node($node));
+    }
+
+    public function describe(): string
+    {
+        return sprintf('opaque %s at %s: %s', $this->class, $this->path, $this->describe);
+    }
+}
diff --git a/src/Rewrite/Preservation.php b/src/Rewrite/Preservation.php
new file mode 100644
index 0000000..5fd5672
--- /dev/null
+++ b/src/Rewrite/Preservation.php
@@ -0,0 +1,38 @@
+<?php
+
+declare(strict_types=1);
+
+namespace Superscript\Axiom\Rewrite;
+
+/**
+ * What a {@see RewriteRule} claims its replacement keeps. A claim is not a
+ * proof: each case names an {@see Obligation} the run discharges at every
+ * site the rule touches, and a claim with no checker supplied is reported
+ * unchecked rather than believed.
+ */
+enum Preservation: string
+{
+    /**
+     * The rewritten source compiles to the same certified type in the same
+     * declaration scope — or both refuse with the same verdict. Always
+     * checked, whether or not a rule claims it: the toolkit has the oracle
+     * for it in every run, and a rewrite that changes a program's type is
+     * never one a host asked for.
+     */
+    case CertifiedType = 'certified-type';
+
+    /**
+     * Both programs answer the same thing on every bindings set of a host
+     * corpus. Only the host owns inputs representative of its data, so this
+     * is checked exactly when the run is given a {@see BindingsCorpus}.
+     */
+    case Verdict = 'verdict';
+
+    public function describe(): string
+    {
+        return match ($this) {
+            self::CertifiedType => 'type preservation',
+            self::Verdict => 'verdict preservation',
+        };
+    }
+}
diff --git a/src/Rewrite/RewriteOutcome.php b/src/Rewrite/RewriteOutcome.php
new file mode 100644
index 0000000..8e54cc0
--- /dev/null
+++ b/src/Rewrite/RewriteOutcome.php
@@ -0,0 +1,14 @@
+<?php
+
+declare(strict_types=1);
+
+namespace Superscript\Axiom\Rewrite;
+
+/** What became of a replacement a rule offered. */
+enum RewriteOutcome: string
+{
+    case Applied = 'applied';
+
+    /** An obligation was broken, so the site keeps its original node. */
+    case Refused = 'refused';
+}
diff --git a/src/Rewrite/RewriteRecord.php b/src/Rewrite/RewriteRecord.php
new file mode 100644
index 0000000..3352a2a
--- /dev/null
+++ b/src/Rewrite/RewriteRecord.php
@@ -0,0 +1,46 @@
+<?php
+
+declare(strict_types=1);
+
+namespace Superscript\Axiom\Rewrite;
+
+/**
+ * One rule, at one site, with what it proposed and what became of it. A
+ * refused record is as much a result as an applied one: it is the run saying
+ * a rewrite was available and was not sound here.
+ */
+final readonly class RewriteRecord
+{
+    /** @param list<ObligationVerdict> $verdicts */
+    private function __construct(
+        public RewriteOutcome $outcome,
+        public string $path,
+        public string $rule,
+        public string $before,
+        public string $after,
+        public array $verdicts,
+    ) {}
+
+    /** @param list<ObligationVerdict> $verdicts */
+    public static function applied(SourcePath $path, RewriteRule $rule, object $before, object $after, array $verdicts): self
+    {
+        return new self(RewriteOutcome::Applied, $path->describe(), $rule->identifier(), Describes::node($before), Describes::node($after), $verdicts);
+    }
+
+    /** @param list<ObligationVerdict> $verdicts */
+    public static function refused(SourcePath $path, RewriteRule $rule, object $before, object $after, array $verdicts): self
+    {
+        return new self(RewriteOutcome::Refused, $path->describe(), $rule->identifier(), Describes::node($before), Describes::node($after), $verdicts);
+    }
+
+    public function describe(): string
+    {
+        $lines = sprintf('%s %s at %s: %s => %s', $this->outcome->value, $this->rule, $this->path, $this->before, $this->after);
+
+        foreach ($this->verdicts as $verdict) {
+            $lines .= "\n  " . $verdict->describe();
+        }
+
+        return $lines;
+    }
+}
diff --git a/src/Rewrite/RewriteReport.php b/src/Rewrite/RewriteReport.php
new file mode 100644
index 0000000..c68336e
--- /dev/null
+++ b/src/Rewrite/RewriteReport.php
@@ -0,0 +1,47 @@
+<?php
+
+declare(strict_types=1);
+
+namespace Superscript\Axiom\Rewrite;
+
+/**
+ * Everything one run of a rule set learned: every site a rule fired, every
+ * site a rule was refused, and every shape the walk could not see inside.
+ *
+ * A report is the whole product of a dry run. {@see RewriteRun} hands back a
+ * tree as well, and a caller that never takes the tree has run the rule set
+ * in report-only mode — there is no second entry point and no mode flag to
+ * pass, because the two runs would otherwise have to be kept identical by
+ * hand.
+ */
+final readonly class RewriteReport
+{
+    /**
+     * @param list<RewriteRecord> $records
+     * @param list<OpaqueSource> $opaque
+     */
+    public function __construct(
+        public array $records,
+        public array $opaque,
+    ) {}
+
+    /** @return list<RewriteRecord> */
+    public function applied(): array
+    {
+        return array_values(array_filter($this->records, fn(RewriteRecord $record): bool => $record->outcome === RewriteOutcome::Applied));
+    }
+
+    /** @return list<RewriteRecord> */
+    public function refused(): array
+    {
+        return array_values(array_filter($this->records, fn(RewriteRecord $record): bool => $record->outcome === RewriteOutcome::Refused));
+    }
+
+    public function describe(): string
+    {
+        $lines = array_map(fn(RewriteRecord $record): string => $record->describe(), $this->records);
+        $lines = [...$lines, ...array_map(fn(OpaqueSource $opaque): string => $opaque->describe(), $this->opaque)];
+
+        return $lines === [] ? 'no rewrites, nothing opaque' : implode("\n", $lines);
+    }
+}
diff --git a/src/Rewrite/RewriteRule.php b/src/Rewrite/RewriteRule.php
new file mode 100644
index 0000000..c78f330
--- /dev/null
+++ b/src/Rewrite/RewriteRule.php
@@ -0,0 +1,61 @@
+<?php
+
+declare(strict_types=1);
+
+namespace Superscript\Axiom\Rewrite;
+
+use Superscript\Axiom\Source;
+
+/**
+ * One transformation of stored source: which node shapes it looks at, what it
+ * replaces one with, and what it claims the replacement keeps.
+ *
+ * Structural knowledge lives here rather than on {@see Source}. A source is
+ * data a host persists, and every method the language puts on it is a method
+ * every host node must implement forever; matching and reconstruction are the
+ * rule's business, and a rule that only rewrites `!!x` needs to know about
+ * exactly two nodes. Descent — the walk that reaches every node and rebuilds
+ * the tree around a replacement — is the toolkit's business, and a rule never
+ * writes any of it.
+ *
+ * A rule is dispatched by exact class, the same ownership model source
+ * compilers use: {@see visits()} lists the classes, and the rewriter indexes
+ * rules by them, so visiting a node costs one array lookup however many rules
+ * a run carries. Exact means exact — a rule listing a parent class is never
+ * offered a subclass.
+ */
+interface RewriteRule
+{
+    /**
+     * Stable identity, reported at every site this rule touches. A class name
+     * will do until a rule outlives one.
+     */
+    public function identifier(): string;
+
+    /**
+     * The exact source classes this rule is offered. Only these; a rule is
+     * never called with anything else.
+     *
+     * @return non-empty-list<class-string<Source>>
+     */
+    public function visits(): array;
+
+    /**
+     * The replacement for this node, or null for "nothing to do here" — the
+     * common answer, and the one that keeps the tree's identity intact.
+     *
+     * The node arrives with its children already rewritten. The replacement is
+     * taken as final: the rewriter does not descend into it, so a rule that
+     * synthesises new structure owns the shape of what it returns.
+     */
+    public function rewrite(Source $source): ?Source;
+
+    /**
+     * What the replacement keeps, beyond the type preservation every rewrite
+     * is held to. Each claim is checked at each site the rule fires, and a
+     * claim the run has no oracle for is reported unchecked.
+     *
+     * @return list<Preservation>
+     */
+    public function preserves(): array;
+}
diff --git a/src/Rewrite/RewriteRun.php b/src/Rewrite/RewriteRun.php
new file mode 100644
index 0000000..7d5b221
--- /dev/null
+++ b/src/Rewrite/RewriteRun.php
@@ -0,0 +1,43 @@
+<?php
+
+declare(strict_types=1);
+
+namespace Superscript\Axiom\Rewrite;
+
+use Superscript\Axiom\Expression;
+use Superscript\Axiom\Source;
+
+/**
+ * The result of applying a rule set to one expression: the tree that came
+ * out, and the {@see RewriteReport} explaining it.
+ *
+ * `changed` is answered by identity, not comparison: a run that applied
+ * nothing returns the very source it was given, because every descent arm
+ * returns its own node when no child moved. A host can therefore store the
+ * result unconditionally and let identity decide whether anything is worth
+ * persisting.
+ */
+final readonly class RewriteRun
+{
+    public bool $changed;
+
+    public function __construct(
+        public Expression $original,
+        public Source $source,
+        public RewriteReport $report,
+    ) {
+        $this->changed = $original->source !== $source;
+    }
+
+    /** The rewritten expression: the original's dialect, definitions, declarations and boundary over the new tree. */
+    public function expression(): Expression
+    {
+        return new Expression(
+            source: $this->source,
+            definitions: $this->original->definitions,
+            dialect: $this->original->dialect,
+            declarations: $this->original->declarations,
+            boundary: $this->original->boundary,
+        );
+    }
+}
diff --git a/src/Rewrite/RewriteSite.php b/src/Rewrite/RewriteSite.php
new file mode 100644
index 0000000..326567d
--- /dev/null
+++ b/src/Rewrite/RewriteSite.php
@@ -0,0 +1,69 @@
+<?php
+
+declare(strict_types=1);
+
+namespace Superscript\Axiom\Rewrite;
+
+use Superscript\Axiom\Expression;
+use Superscript\Axiom\Program;
+use Superscript\Axiom\Source;
+use Superscript\Axiom\Types\TypeMismatch;
+use Superscript\Monads\Result\Result;
+
+/**
+ * One place a rule offered a replacement, and everything an {@see Obligation}
+ * needs to judge it: the two subtrees, and the expression they live in —
+ * its dialect, definitions, declarations and boundary.
+ *
+ * Both subtrees are compiled *standalone in the whole expression's scope*,
+ * which is exact rather than approximate because the language has no binding
+ * form: no node introduces a name for its children, so a subtree reads the
+ * same environment wherever it sits, and match arms are ordinary sources
+ * rather than a scope. A subtree therefore compiles here to the very type it
+ * contributes in place.
+ *
+ * The two compilations are memoized because obligations stack: type
+ * preservation and verdict preservation both want the same two programs, and
+ * a corpus run wants one of them once per bindings set. Nothing here is
+ * mutated after construction that a caller can observe — the answers are
+ * derived from readonly inputs.
+ */
+final class RewriteSite
+{
+    /** @var ?Result<Program, TypeMismatch> */
+    private ?Result $compiledBefore = null;
+
+    /** @var ?Result<Program, TypeMismatch> */
+    private ?Result $compiledAfter = null;
+
+    public function __construct(
+        public readonly Expression $context,
+        public readonly SourcePath $path,
+        public readonly Source $before,
+        public readonly Source $after,
+    ) {}
+
+    /** @return Result<Program, TypeMismatch> */
+    public function compileBefore(): Result
+    {
+        return $this->compiledBefore ??= $this->compile($this->before);
+    }
+
+    /** @return Result<Program, TypeMismatch> */
+    public function compileAfter(): Result
+    {
+        return $this->compiledAfter ??= $this->compile($this->after);
+    }
+
+    /** @return Result<Program, TypeMismatch> */
+    private function compile(Source $source): Result
+    {
+        return (new Expression(
+            source: $source,
+            definitions: $this->context->definitions,
+            dialect: $this->context->dialect,
+            declarations: $this->context->declarations,
+            boundary: $this->context->boundary,
+        ))->compile();
+    }
+}
diff --git a/src/Rewrite/RewriteWalk.php b/src/Rewrite/RewriteWalk.php
new file mode 100644
index 0000000..ff12040
--- /dev/null
+++ b/src/Rewrite/RewriteWalk.php
@@ -0,0 +1,151 @@
+<?php
+
+declare(strict_types=1);
+
+namespace Superscript\Axiom\Rewrite;
+
+use Superscript\Axiom\Expression;
+use Superscript\Axiom\Source;
+use Superscript\Axiom\Sources\MatchArm;
+use Superscript\Axiom\Sources\MatchPattern;
+
+/**
+ * One pass of a rule set over one tree, and the notebook it writes as it
+ * goes. A walk is used once: {@see Rewriter} builds it per run, so the
+ * records it accumulates belong to that run and nothing is carried between
+ * two.
+ *
+ * @internal
+ */
+final class RewriteWalk
+{
+    /** @var list<RewriteRecord> */
+    private array $records = [];
+
+    /** @var list<OpaqueSource> */
+    private array $opaque = [];
+
+    /**
+     * @param array<class-string<Source>, list<RewriteRule>> $rules Indexed by the exact class each rule visits.
+     * @param array<string, Obligation> $obligations Keyed by the preservation each discharges.
+     */
+    public function __construct(
+        private readonly Expression $context,
+        private readonly array $rules,
+        private readonly SourceDescenders $descenders,
+        private readonly array $obligations,
+    ) {}
+
+    public function run(): RewriteRun
+    {
+        $source = $this->source($this->context->source, SourcePath::root());
+
+        return new RewriteRun($this->context, $source, new RewriteReport($this->records, $this->opaque));
+    }
+
+    /**
+     * Bottom-up: a node's children are rewritten, the node is rebuilt around
+     * whatever came back, and only then are rules offered the rebuilt node.
+     * That order is what lets one pass collapse a nest — `!!!!x` reduces at
+     * every level on the way out — and it means a rule always sees the shape
+     * that will actually be stored, never one a deeper rewrite is about to
+     * change.
+     */
+    public function source(Source $node, SourcePath $path): Source
+    {
+        $descender = $this->descenders->sources[$node::class] ?? null;
+
+        if ($descender === null) {
+            $this->opaque[] = OpaqueSource::at($path, $node);
+
+            return $node;
+        }
+
+        return $this->apply($descender($node, new Descent($this, $path)), $path);
+    }
+
+    public function pattern(MatchPattern $node, SourcePath $path): MatchPattern
+    {
+        $descender = $this->descenders->patterns[$node::class] ?? null;
+
+        if ($descender === null) {
+            $this->opaque[] = OpaqueSource::at($path, $node);
+
+            return $node;
+        }
+
+        return $descender($node, new Descent($this, $path));
+    }
+
+    public function arm(MatchArm $arm, SourcePath $path): MatchArm
+    {
+        $descent = new Descent($this, $path);
+        $pattern = $descent->pattern($arm->pattern, 'pattern');
+        $expression = $descent->child($arm->expression, 'expression');
+
+        return $pattern === $arm->pattern && $expression === $arm->expression
+            ? $arm
+            : new MatchArm($pattern, $expression);
+    }
+
+    /**
+     * The rules registered for this exact class, in registration order, until
+     * one of them takes the site. A rule that offers nothing is passed over; a
+     * rule whose replacement breaks an obligation is recorded refused and the
+     * next rule is asked. The first sound replacement wins and ends the visit:
+     * two rules that both want a node would otherwise compose in an order
+     * nobody chose, and a rule offered its own output could rewrite forever.
+     * Opportunities a rewrite creates are found by running the rewriter again
+     * — a decision the caller makes, and can see in the report.
+     */
+    private function apply(Source $node, SourcePath $path): Source
+    {
+        foreach ($this->rules[$node::class] ?? [] as $rule) {
+            $replacement = $rule->rewrite($node);
+
+            if ($replacement === null) {
+                continue;
+            }
+
+            $verdicts = $this->judge($rule, new RewriteSite($this->context, $path, $node, $replacement));
+
+            if (array_any($verdicts, static fn(ObligationVerdict $verdict): bool => $verdict->broken)) {
+                $this->records[] = RewriteRecord::refused($path, $rule, $node, $replacement, $verdicts);
+
+                continue;
+            }
+
+            $this->records[] = RewriteRecord::applied($path, $rule, $node, $replacement, $verdicts);
+
+            return $replacement;
+        }
+
+        return $node;
+    }
+
+    /**
+     * Type preservation is checked at every site whether or not the rule
+     * claims it: the toolkit always has that oracle, and a rewrite that
+     * changes a program's type is not one anybody asked for. Everything else
+     * a rule claims is checked when the run was given the oracle for it, and
+     * reported unchecked when it was not. A rule free to name type
+     * preservation among its own claims costs nothing by doing so: a claim
+     * made twice is judged once.
+     *
+     * @return list<ObligationVerdict>
+     */
+    private function judge(RewriteRule $rule, RewriteSite $site): array
+    {
+        $verdicts = [];
+
+        foreach (array_unique([Preservation::CertifiedType, ...$rule->preserves()], SORT_REGULAR) as $preservation) {
+            $obligation = $this->obligations[$preservation->value] ?? null;
+
+            $verdicts[] = $obligation === null
+                ? ObligationVerdict::unchecked($preservation, 'the run was given no oracle for this claim')
+                : $obligation->check($site);
+        }
+
+        return $verdicts;
+    }
+}
diff --git a/src/Rewrite/Rewriter.php b/src/Rewrite/Rewriter.php
new file mode 100644
index 0000000..173214e
--- /dev/null
+++ b/src/Rewrite/Rewriter.php
@@ -0,0 +1,89 @@
+<?php
+
+declare(strict_types=1);
+
+namespace Superscript\Axiom\Rewrite;
+
+use Superscript\Axiom\Expression;
+use Superscript\Axiom\Source;
+
+/**
+ * Rewrites stored source: a rule set, applied deterministically to an
+ * immutable tree, returning a new tree and a report of everything that
+ * happened. Nothing is mutated, and nothing is applied that was not proved.
+ *
+ * ```php
+ * $run = (new Rewriter([new RemoveDoubleNegation()]))->rewrite($expression);
+ *
+ * $run->report->describe(); // dry run: read this, take nothing
+ * $run->changed;            // false when every subtree came back identical
+ * $run->source;             // the tree to store
+ * ```
+ *
+ * Four decisions govern a run:
+ *
+ *  - **Bottom-up, one pass.** Children are rewritten before their parent is
+ *    offered to rules, so a rule sees the shape that will be stored.
+ *  - **Exact-class dispatch.** A rule declares the classes it visits and is
+ *    indexed by them, so a node costs one array lookup no matter how many
+ *    rules the run carries.
+ *  - **Prove, then apply.** Every replacement is compiled against the
+ *    expression's own declarations and must certify the same type as what it
+ *    replaces; a rule may claim more, and the run checks each claim it has an
+ *    oracle for. A broken obligation refuses that one site — the rest of the
+ *    run proceeds — and the refusal is reported. This is the whole point: a
+ *    fold that type-checks can still invert the meaning of a condition, and a
+ *    rewrite nobody proved is a rewrite nobody should store.
+ *  - **Opaque leaves are reported, never skipped.** A node class with no
+ *    descent arm is not descended and not rewritten, and it appears in the
+ *    report; silence about a shape the run could not see would read exactly
+ *    like a clean tree.
+ *
+ * A rewriter is a value: it holds no run state, so one can be shared across
+ * every expression in a corpus.
+ */
+final readonly class Rewriter
+{
+    /** @var array<class-string<Source>, list<RewriteRule>> */
+    private array $rules;
+
+    /** @var array<string, Obligation> */
+    private array $obligations;
+
+    private SourceDescenders $descenders;
+
+    /**
+     * @param list<RewriteRule> $rules Applied in this order at every node they visit.
+     * @param list<Obligation> $obligations Oracles beyond type preservation — a
+     *        {@see VerdictPreservation} over the host's corpus, typically. One
+     *        supplied for a preservation the toolkit already answers replaces it.
+     */
+    public function __construct(
+        array $rules,
+        ?SourceDescenders $descenders = null,
+        array $obligations = [],
+    ) {
+        $indexed = [];
+
+        foreach ($rules as $rule) {
+            foreach ($rule->visits() as $class) {
+                $indexed[$class][] = $rule;
+            }
+        }
+
+        $checkers = [Preservation::CertifiedType->value => new TypePreservation()];
+
+        foreach ($obligations as $obligation) {
+            $checkers[$obligation->preservation()->value] = $obligation;
+        }
+
+        $this->rules = $indexed;
+        $this->obligations = $checkers;
+        $this->descenders = $descenders ?? SourceDescenders::core();
+    }
+
+    public function rewrite(Expression $expression): RewriteRun
+    {
+        return (new RewriteWalk($expression, $this->rules, $this->descenders, $this->obligations))->run();
+    }
+}
diff --git a/src/Rewrite/Rules/RemoveDoubleNegation.php b/src/Rewrite/Rules/RemoveDoubleNegation.php
new file mode 100644
index 0000000..61de219
--- /dev/null
+++ b/src/Rewrite/Rules/RemoveDoubleNegation.php
@@ -0,0 +1,87 @@
+<?php
+
+declare(strict_types=1);
+
+namespace Superscript\Axiom\Rewrite\Rules;
+
+use Superscript\Axiom\Rewrite\Preservation;
+use Superscript\Axiom\Rewrite\RewriteRule;
+use Superscript\Axiom\Source;
+use Superscript\Axiom\Sources\UnaryExpression;
+
+/**
+ * `!!x` becomes `x`, and so does any pairing of the core dialect's two
+ * spellings of negation (`!` and `not`).
+ *
+ * Why this is meaning-preserving under the core dialect, and not merely
+ * plausible: `!` is a row taking Boolean and returning Boolean, and it is the
+ * only row for that symbol — so a `!!x` that compiles at all has an `x` of
+ * Boolean or, through the resolver's lift, `Boolean?`. On Boolean, `!` is
+ * total and involutive: `!!true` is `true`, `!!false` is `false`, and there is
+ * no third value. On `Boolean?` the resolver lifts the same row, and lifting
+ * is functorial — absence propagates through each negation untouched, so
+ * `!!` is the lift of `!∘!`, which is the identity. Every operand type the
+ * rewrite can meet is therefore one it is neutral on.
+ *
+ * What that argument rests on, and what the run checks anyway:
+ *
+ *  - The named operators must denote that involutive negation. A host free to
+ *    register `!` over its own type is free to make it something else, so the
+ *    spellings are a constructor argument rather than a constant, and a
+ *    dialect that rebinds them declares which of its own are involutive.
+ *  - Type preservation catches the operand the argument excludes. `!!count`
+ *    over a Number never compiled — `!` admits no Number — and simplifying it
+ *    to `count` would mint a certified Number program out of a refusal. The
+ *    obligation compares the two compilations and refuses that site.
+ *  - The rule claims verdict preservation as well, so a host with a corpus
+ *    gets the argument checked against its own data rather than trusted.
+ */
+final readonly class RemoveDoubleNegation implements RewriteRule
+{
+    /** @var list<string> */
+    private array $negations;
+
+    /**
+     * @param list<string> $negations The operator spellings that denote an
+     *        involutive negation in the dialect this rule runs against.
+     */
+    public function __construct(array $negations = ['!', 'not'])
+    {
+        $this->negations = $negations;
+    }
+
+    public function identifier(): string
+    {
+        return 'axiom.rewrite.remove-double-negation';
+    }
+
+    public function visits(): array
+    {
+        return [UnaryExpression::class];
+    }
+
+    public function preserves(): array
+    {
+        return [Preservation::Verdict];
+    }
+
+    public function rewrite(Source $source): ?Source
+    {
+        if (! $source instanceof UnaryExpression || ! $this->negates($source->operator)) {
+            return null;
+        }
+
+        $operand = $source->operand;
+
+        if (! $operand instanceof UnaryExpression || ! $this->negates($operand->operator)) {
+            return null;
+        }
+
+        return $operand->operand;
+    }
+
+    private function negates(string $operator): bool
+    {
+        return in_array($operator, $this->negations, strict: true);
+    }
+}
diff --git a/src/Rewrite/Rules/RemoveRedundantDefault.php b/src/Rewrite/Rules/RemoveRedundantDefault.php
new file mode 100644
index 0000000..99cb956
--- /dev/null
+++ b/src/Rewrite/Rules/RemoveRedundantDefault.php
@@ -0,0 +1,55 @@
+<?php
+
+declare(strict_types=1);
+
+namespace Superscript\Axiom\Rewrite\Rules;
+
+use Superscript\Axiom\Rewrite\Preservation;
+use Superscript\Axiom\Rewrite\RewriteRule;
+use Superscript\Axiom\Source;
+use Superscript\Axiom\Sources\DefaultValue;
+
+/**
+ * `x ?? 0` becomes `x` where `x` can never be absent.
+ *
+ * A `DefaultValue` over a source whose type is not an option is already the
+ * identity: the compiler returns the inner compiled source untouched, default
+ * and all. The node is then pure noise in stored source — an author's guess
+ * about a question that turned out to be required — and it reads as if
+ * absence were possible here, which is worse than noise.
+ *
+ * This rule is the shape of one whose applicability is not decided by
+ * matching. Whether the inner source can be absent is a fact about *types*,
+ * which no amount of looking at the tree can settle, so the rule proposes the
+ * removal everywhere and lets type preservation settle it: over an optional
+ * inner the original certifies the present type `T` while the replacement
+ * certifies `Option<T>`, the types differ, and the site is refused. Over a
+ * definite inner both compile to the same type — necessarily, since they
+ * compile to the same node — and the rewrite is taken.
+ *
+ * Removing the node does change what an execution observer sees: the
+ * `default` label and its annotations go with it. That is a change to the
+ * trace of the program, not to what the program answers.
+ */
+final readonly class RemoveRedundantDefault implements RewriteRule
+{
+    public function identifier(): string
+    {
+        return 'axiom.rewrite.remove-redundant-default';
+    }
+
+    public function visits(): array
+    {
+        return [DefaultValue::class];
+    }
+
+    public function preserves(): array
+    {
+        return [Preservation::Verdict];
+    }
+
+    public function rewrite(Source $source): ?Source
+    {
+        return $source instanceof DefaultValue ? $source->source : null;
+    }
+}
diff --git a/src/Rewrite/SourceDescenders.php b/src/Rewrite/SourceDescenders.php
new file mode 100644
index 0000000..cf28e5f
--- /dev/null
+++ b/src/Rewrite/SourceDescenders.php
@@ -0,0 +1,59 @@
+<?php
+
+declare(strict_types=1);
+
+namespace Superscript\Axiom\Rewrite;
+
+use InvalidArgumentException;
+use Superscript\Axiom\Extension;
+use Superscript\Axiom\Source;
+use Superscript\Axiom\Sources\MatchPattern;
+
+/**
+ * Who knows how to take a node apart. The core map is always there; a host
+ * joins its own through the extension it already ships, so one package
+ * declares both how its node compiles ({@see Extension::sourceCompilers()})
+ * and how it is descended ({@see Extension::sourceDescenders()}), and the two
+ * cannot end up in different places.
+ *
+ * Ownership is exact and unranked, exactly as it is for source compilers: two
+ * extensions claiming one class is a configuration error, never a precedence
+ * question, and a class no extension claims is not an error at all — it is an
+ * opaque leaf the run reports.
+ */
+final readonly class SourceDescenders
+{
+    /**
+     * @param array<class-string<Source>, callable(Source, Descent): Source> $sources
+     * @param array<class-string<MatchPattern>, callable(MatchPattern, Descent): MatchPattern> $patterns
+     */
+    private function __construct(
+        public array $sources,
+        public array $patterns,
+    ) {}
+
+    public static function core(): self
+    {
+        return new self(CoreSourceDescenders::sources(), CoreSourceDescenders::patterns());
+    }
+
+    public function with(Extension ...$extensions): self
+    {
+        $sources = $this->sources;
+
+        foreach ($extensions as $extension) {
+            foreach ($extension->sourceDescenders() as $class => $descender) {
+                if (array_key_exists($class, $sources)) {
+                    throw new InvalidArgumentException(sprintf(
+                        'Source class [%s] has two descent arms; descent ownership is exact and extension order carries no precedence.',
+                        $class,
+                    ));
+                }
+
+                $sources[$class] = $descender;
+            }
+        }
+
+        return new self($sources, $this->patterns);
+    }
+}
diff --git a/src/Rewrite/SourcePath.php b/src/Rewrite/SourcePath.php
new file mode 100644
index 0000000..277f47f
--- /dev/null
+++ b/src/Rewrite/SourcePath.php
@@ -0,0 +1,52 @@
+<?php
+
+declare(strict_types=1);
+
+namespace Superscript\Axiom\Rewrite;
+
+use InvalidArgumentException;
+
+/**
+ * Where a node sits in a {@see \Superscript\Axiom\Source} tree, addressed by
+ * the property that holds it: `$.left.operand`, `$.arms[1].expression`.
+ *
+ * This is deliberately not the `$.children[0].node` language compilation
+ * failures and analyses speak. That one numbers the children a *compiler*
+ * recorded, and a compiler records what it needs: a wildcard arm records no
+ * pattern child at all, so the same arm sits at a different index depending
+ * on which patterns precede it. A coordinate into stored source has to name
+ * the same node before anything is compiled, and the property names do —
+ * they are the tree's own structure rather than an artifact of walking it.
+ */
+final readonly class SourcePath
+{
+    /** @param list<string> $segments */
+    private function __construct(private array $segments) {}
+
+    public static function root(): self
+    {
+        return new self([]);
+    }
+
+    /**
+     * @param string $segment The property holding the child, optionally
+     *                        subscripted for a list slot: `arms[1]`.
+     */
+    public function child(string $segment): self
+    {
+        if ($segment === '') {
+            throw new InvalidArgumentException('A source path segment names a property and cannot be empty.');
+        }
+
+        return new self([...$this->segments, $segment]);
+    }
+
+    public function describe(): string
+    {
+        if ($this->segments === []) {
+            return '$';
+        }
+
+        return '$.' . implode('.', $this->segments);
+    }
+}
diff --git a/src/Rewrite/TypePreservation.php b/src/Rewrite/TypePreservation.php
new file mode 100644
index 0000000..dba230c
--- /dev/null
+++ b/src/Rewrite/TypePreservation.php
@@ -0,0 +1,61 @@
+<?php
+
+declare(strict_types=1);
+
+namespace Superscript\Axiom\Rewrite;
+
+use Superscript\Axiom\Types\TypeDescriber;
+use Superscript\Axiom\Types\TypeRelations;
+
+/**
+ * Compile both subtrees in the site's declaration scope and demand the same
+ * answer: the same certified type, or the same refusal.
+ *
+ * The same refusal counts as preservation because neither tree can run — but
+ * the refusals must match, so a rewrite is never the thing that changes what
+ * an author is told is wrong. A rewrite that turns a refusal into a certified
+ * program is the interesting failure: `!!count` over a Number never compiled
+ * (`!` admits Boolean only), and simplifying it to `count` would hand back a
+ * Number program the author never wrote and the checker never blessed.
+ */
+final readonly class TypePreservation implements Obligation
+{
+    public function preservation(): Preservation
+    {
+        return Preservation::CertifiedType;
+    }
+
+    public function check(RewriteSite $site): ObligationVerdict
+    {
+        $before = $site->compileBefore();
+        $after = $site->compileAfter();
+
+        if ($before->isErr() && $after->isErr()) {
+            $original = $before->unwrapErr()->describe();
+            $replacement = $after->unwrapErr()->describe();
+
+            return $original === $replacement
+                ? ObligationVerdict::upheld($this->preservation(), sprintf('both refuse: %s', $original))
+                : ObligationVerdict::broken($this->preservation(), sprintf('both refuse, but differently: [%s] against [%s]', $original, $replacement));
+        }
+
+        if ($before->isErr()) {
+            return ObligationVerdict::broken($this->preservation(), sprintf('the original refuses and the replacement compiles: %s', $before->unwrapErr()->describe()));
+        }
+
+        if ($after->isErr()) {
+            return ObligationVerdict::broken($this->preservation(), sprintf('the original compiles and the replacement refuses: %s', $after->unwrapErr()->describe()));
+        }
+
+        $beforeType = $before->unwrap()->returns;
+        $afterType = $after->unwrap()->returns;
+
+        return TypeRelations::areEquivalent($beforeType, $afterType)->isOk()
+            ? ObligationVerdict::upheld($this->preservation(), sprintf('both compile to %s', TypeDescriber::describe($beforeType)))
+            : ObligationVerdict::broken($this->preservation(), sprintf(
+                'the original compiles to %s and the replacement to %s',
+                TypeDescriber::describe($beforeType),
+                TypeDescriber::describe($afterType),
+            ));
+    }
+}
diff --git a/src/Rewrite/VerdictPreservation.php b/src/Rewrite/VerdictPreservation.php
new file mode 100644
index 0000000..f416cf2
--- /dev/null
+++ b/src/Rewrite/VerdictPreservation.php
@@ -0,0 +1,76 @@
+<?php
+
+declare(strict_types=1);
+
+namespace Superscript\Axiom\Rewrite;
+
+use SebastianBergmann\Exporter\Exporter;
+use Superscript\Monads\Option\Option;
+use Superscript\Monads\Result\Result;
+use Throwable;
+
+/**
+ * Run both programs over every case of a host corpus and demand the same
+ * answer each time. An answer is the whole invocation result — an error, an
+ * absent value, or a present value — because those are three different things
+ * to a host and a rewrite that trades one for another has changed the program.
+ *
+ * The first disagreement stops the sweep and names the case: one counterexample
+ * refuses the rewrite, and the rest of the corpus cannot un-refuse it.
+ *
+ * Evidence, not proof. A corpus that never exercises a branch says nothing
+ * about it, which is why type preservation is checked independently and
+ * always.
+ */
+final readonly class VerdictPreservation implements Obligation
+{
+    public function __construct(private BindingsCorpus $corpus) {}
+
+    public function preservation(): Preservation
+    {
+        return Preservation::Verdict;
+    }
+
+    public function check(RewriteSite $site): ObligationVerdict
+    {
+        $before = $site->compileBefore();
+        $after = $site->compileAfter();
+
+        if ($before->isErr() || $after->isErr()) {
+            return ObligationVerdict::unchecked($this->preservation(), 'a subtree does not compile, so there is no pair of programs to run');
+        }
+
+        $original = $before->unwrap();
+        $replacement = $after->unwrap();
+        $cases = 0;
+
+        foreach ($this->corpus->cases() as $label => $bindings) {
+            $cases++;
+            $answered = self::answer($original($bindings));
+            $answers = self::answer($replacement($bindings));
+
+            if ($answered !== $answers) {
+                return ObligationVerdict::broken($this->preservation(), sprintf(
+                    'case [%s]: the original answers %s and the replacement %s',
+                    $label,
+                    $answered,
+                    $answers,
+                ));
+            }
+        }
+
+        return ObligationVerdict::upheld($this->preservation(), sprintf('%d corpus case(s) agree', $cases));
+    }
+
+    /**
+     * @param Result<Option<mixed>, Throwable> $result
+     */
+    private static function answer(Result $result): string
+    {
+        /** @var string */
+        return $result->mapOrElse(
+            fn(Throwable $error): string => sprintf('error(%s)', $error->getMessage()),
+            fn(Option $value): string => $value->mapOr('absent', fn(mixed $present): string => sprintf('value(%s)', (new Exporter())->shortenedExport($present))),
+        );
+    }
+}
diff --git a/tests/Rewrite/CoreDescentExhaustivenessTest.php b/tests/Rewrite/CoreDescentExhaustivenessTest.php
new file mode 100644
index 0000000..fedfc76
--- /dev/null
+++ b/tests/Rewrite/CoreDescentExhaustivenessTest.php
@@ -0,0 +1,84 @@
+<?php
+
+declare(strict_types=1);
+
+namespace Superscript\Axiom\Tests\Rewrite;
+
+use PHPUnit\Framework\Attributes\CoversClass;
+use PHPUnit\Framework\Attributes\Test;
+use PHPUnit\Framework\Attributes\UsesNamespace;
+use PHPUnit\Framework\TestCase;
+use ReflectionClass;
+use Superscript\Axiom\Rewrite\CoreSourceDescenders;
+use Superscript\Axiom\Source;
+use Superscript\Axiom\Sources\MatchPattern;
+
+/**
+ * The core node set is closed, and descent over it must stay exhaustive. A
+ * node class with no arm is not a loud failure at runtime — it is an opaque
+ * leaf, so every rewrite beneath it silently stops happening and the report
+ * says so in a line nobody reads. This law makes the omission fail here
+ * instead, at the moment the class is added.
+ */
+#[CoversClass(CoreSourceDescenders::class)]
+#[UsesNamespace('Superscript\\Axiom')]
+final class CoreDescentExhaustivenessTest extends TestCase
+{
+    #[Test]
+    public function every_core_source_class_has_a_descent_arm(): void
+    {
+        $arms = CoreSourceDescenders::sources();
+
+        foreach (self::coreClasses(Source::class) as $class) {
+            $this->assertArrayHasKey($class, $arms, sprintf(
+                '[%s] is a core source with no descent arm: the rewriter would treat it as an opaque leaf and never rewrite inside it.',
+                $class,
+            ));
+        }
+
+        $this->assertSame([], array_diff(array_keys($arms), self::coreClasses(Source::class)), 'every arm names a core source class');
+    }
+
+    #[Test]
+    public function every_core_pattern_class_has_a_descent_arm(): void
+    {
+        $arms = CoreSourceDescenders::patterns();
+
+        foreach (self::coreClasses(MatchPattern::class) as $class) {
+            $this->assertArrayHasKey($class, $arms, sprintf('[%s] is a core match pattern with no descent arm.', $class));
+        }
+
+        $this->assertSame([], array_diff(array_keys($arms), self::coreClasses(MatchPattern::class)), 'every arm names a core pattern class');
+    }
+
+    /**
+     * Read off the directory rather than a hand-kept list: a list would have
+     * to be updated by the same person who forgot the arm.
+     *
+     * @param class-string $interface
+     * @return list<class-string>
+     */
+    private static function coreClasses(string $interface): array
+    {
+        $classes = [];
+
+        foreach (glob(__DIR__ . '/../../src/Sources/*.php') ?: [] as $file) {
+            /** @var class-string $class */
+            $class = 'Superscript\\Axiom\\Sources\\' . basename($file, '.php');
+
+            if (! class_exists($class)) {
+                continue;
+            }
+
+            $reflection = new ReflectionClass($class);
+
+            if ($reflection->isAbstract() || ! $reflection->implementsInterface($interface)) {
+                continue;
+            }
+
+            $classes[] = $class;
+        }
+
+        return $classes;
+    }
+}
diff --git a/tests/Rewrite/Fixtures/BoxExtension.php b/tests/Rewrite/Fixtures/BoxExtension.php
new file mode 100644
index 0000000..caeef83
--- /dev/null
+++ b/tests/Rewrite/Fixtures/BoxExtension.php
@@ -0,0 +1,41 @@
+<?php
+
+declare(strict_types=1);
+
+namespace Superscript\Axiom\Tests\Rewrite\Fixtures;
+
+use Superscript\Axiom\CompiledSource;
+use Superscript\Axiom\Extension;
+use Superscript\Axiom\Rewrite\Descent;
+use Superscript\Axiom\Source;
+use Superscript\Axiom\SourceCompilation;
+
+/** One package, both hooks: how a box compiles, and how a rewrite reaches through it. */
+final class BoxExtension extends Extension
+{
+    public function sourceCompilers(): array
+    {
+        return [
+            BoxSource::class => $this->compile(...),
+        ];
+    }
+
+    public function sourceDescenders(): array
+    {
+        return [
+            BoxSource::class => $this->descend(...),
+        ];
+    }
+
+    private function compile(BoxSource $source, SourceCompilation $compilation): CompiledSource
+    {
+        return $compilation->child($source->inner, 'inner');
+    }
+
+    private function descend(BoxSource $source, Descent $descent): Source
+    {
+        $inner = $descent->child($source->inner, 'inner');
+
+        return $inner === $source->inner ? $source : new BoxSource($inner);
+    }
+}
diff --git a/tests/Rewrite/Fixtures/BoxSource.php b/tests/Rewrite/Fixtures/BoxSource.php
new file mode 100644
index 0000000..7a280ca
--- /dev/null
+++ b/tests/Rewrite/Fixtures/BoxSource.php
@@ -0,0 +1,19 @@
+<?php
+
+declare(strict_types=1);
+
+namespace Superscript\Axiom\Tests\Rewrite\Fixtures;
+
+use Superscript\Axiom\Describable;
+use Superscript\Axiom\Source;
+
+/** A host source with a child: transparent at compile time, so only its descent is under test. */
+final readonly class BoxSource implements Source, Describable
+{
+    public function __construct(public Source $inner) {}
+
+    public function describe(): string
+    {
+        return sprintf('box(%s)', $this->inner instanceof Describable ? $this->inner->describe() : $this->inner::class);
+    }
+}
diff --git a/tests/Rewrite/Fixtures/StubRule.php b/tests/Rewrite/Fixtures/StubRule.php
new file mode 100644
index 0000000..e336a66
--- /dev/null
+++ b/tests/Rewrite/Fixtures/StubRule.php
@@ -0,0 +1,46 @@
+<?php
+
+declare(strict_types=1);
+
+namespace Superscript\Axiom\Tests\Rewrite\Fixtures;
+
+use Closure;
+use Superscript\Axiom\Rewrite\Preservation;
+use Superscript\Axiom\Rewrite\RewriteRule;
+use Superscript\Axiom\Source;
+
+/** A rule whose matching, replacement and claims are handed to it. */
+final readonly class StubRule implements RewriteRule
+{
+    /**
+     * @param non-empty-list<class-string<Source>> $visits
+     * @param Closure(Source): ?Source $rewrite
+     * @param list<Preservation> $preserves
+     */
+    public function __construct(
+        private string $identifier,
+        private array $visits,
+        private Closure $rewrite,
+        private array $preserves = [],
+    ) {}
+
+    public function identifier(): string
+    {
+        return $this->identifier;
+    }
+
+    public function visits(): array
+    {
+        return $this->visits;
+    }
+
+    public function rewrite(Source $source): ?Source
+    {
+        return ($this->rewrite)($source);
+    }
+
+    public function preserves(): array
+    {
+        return $this->preserves;
+    }
+}
diff --git a/tests/Rewrite/ObligationTest.php b/tests/Rewrite/ObligationTest.php
new file mode 100644
index 0000000..49dce57
--- /dev/null
+++ b/tests/Rewrite/ObligationTest.php
@@ -0,0 +1,221 @@
+<?php
+
+declare(strict_types=1);
+
+namespace Superscript\Axiom\Tests\Rewrite;
+
+use PHPUnit\Framework\Attributes\CoversClass;
+use PHPUnit\Framework\Attributes\Test;
+use PHPUnit\Framework\Attributes\UsesNamespace;
+use PHPUnit\Framework\TestCase;
+use Superscript\Axiom\Expression;
+use Superscript\Axiom\Rewrite\ArrayBindingsCorpus;
+use Superscript\Axiom\Rewrite\ObligationVerdict;
+use Superscript\Axiom\Rewrite\Preservation;
+use Superscript\Axiom\Rewrite\RewriteSite;
+use Superscript\Axiom\Rewrite\SourcePath;
+use Superscript\Axiom\Rewrite\TypePreservation;
+use Superscript\Axiom\Rewrite\VerdictPreservation;
+use Superscript\Axiom\Source;
+use Superscript\Axiom\Sources\Coerce;
+use Superscript\Axiom\Sources\InfixExpression;
+use Superscript\Axiom\Sources\StaticSource;
+use Superscript\Axiom\Sources\SymbolSource;
+use Superscript\Axiom\Sources\UnaryExpression;
+use Superscript\Axiom\Types\BooleanType;
+use Superscript\Axiom\Types\NumberType;
+use Superscript\Axiom\Types\Optional;
+use Superscript\Axiom\Types\OptionType;
+use Superscript\Axiom\Types\StringType;
+use Superscript\Axiom\Types\Type;
+
+#[CoversClass(TypePreservation::class)]
+#[CoversClass(VerdictPreservation::class)]
+#[CoversClass(ObligationVerdict::class)]
+#[CoversClass(Preservation::class)]
+#[CoversClass(RewriteSite::class)]
+#[CoversClass(ArrayBindingsCorpus::class)]
+#[UsesNamespace('Superscript\\Axiom')]
+final class ObligationTest extends TestCase
+{
+    /** @param array<string, Type|Optional> $declarations */
+    private static function site(Source $before, Source $after, array $declarations = []): RewriteSite
+    {
+        return new RewriteSite(new Expression($before, declarations: $declarations), SourcePath::root(), $before, $after);
+    }
+
+    #[Test]
+    public function a_site_compiles_each_subtree_once(): void
+    {
+        $site = self::site(new StaticSource(1), new StaticSource(2));
+
+        $this->assertSame($site->compileBefore(), $site->compileBefore());
+        $this->assertSame($site->compileAfter(), $site->compileAfter());
+        $this->assertNotSame($site->compileBefore(), $site->compileAfter());
+    }
+
+    #[Test]
+    public function a_subtree_compiles_in_the_whole_expressions_scope(): void
+    {
+        $site = self::site(new SymbolSource('flag'), new SymbolSource('flag'), ['flag' => new BooleanType()]);
+
+        $this->assertTrue($site->compileBefore()->isOk(), 'the declaration the whole expression makes is the one a subtree is compiled against');
+    }
+
+    #[Test]
+    public function equal_certified_types_uphold_type_preservation(): void
+    {
+        $verdict = (new TypePreservation())->check(self::site(
+            new UnaryExpression('!', new UnaryExpression('!', new SymbolSource('flag'))),
+            new SymbolSource('flag'),
+            ['flag' => new BooleanType()],
+        ));
+
+        $this->assertTrue($verdict->checked);
+        $this->assertFalse($verdict->broken);
+        $this->assertSame('type preservation upheld: both compile to Boolean', $verdict->describe());
+    }
+
+    #[Test]
+    public function different_certified_types_break_type_preservation(): void
+    {
+        $verdict = (new TypePreservation())->check(self::site(
+            new Coerce(new BooleanType(), new StaticSource(true)),
+            new Coerce(new StringType(), new StaticSource('true')),
+        ));
+
+        $this->assertTrue($verdict->broken);
+        $this->assertSame('type preservation broken: the original compiles to Boolean and the replacement to String', $verdict->describe());
+    }
+
+    #[Test]
+    public function turning_a_refusal_into_a_program_breaks_type_preservation(): void
+    {
+        $verdict = (new TypePreservation())->check(self::site(
+            new UnaryExpression('!', new UnaryExpression('!', new SymbolSource('count'))),
+            new SymbolSource('count'),
+            ['count' => new NumberType()],
+        ));
+
+        $this->assertTrue($verdict->broken);
+        $this->assertStringStartsWith('type preservation broken: the original refuses and the replacement compiles: [!] expects Boolean; got Number.', $verdict->describe());
+    }
+
+    #[Test]
+    public function turning_a_program_into_a_refusal_breaks_type_preservation(): void
+    {
+        $verdict = (new TypePreservation())->check(self::site(
+            new SymbolSource('count'),
+            new UnaryExpression('!', new SymbolSource('count')),
+            ['count' => new NumberType()],
+        ));
+
+        $this->assertTrue($verdict->broken);
+        $this->assertStringStartsWith('type preservation broken: the original compiles and the replacement refuses: [!] expects Boolean; got Number.', $verdict->describe());
+    }
+
+    #[Test]
+    public function the_same_refusal_on_both_sides_upholds_type_preservation(): void
+    {
+        $verdict = (new TypePreservation())->check(self::site(
+            new Coerce(new NumberType(), new SymbolSource('missing')),
+            new Coerce(new StringType(), new SymbolSource('missing')),
+        ));
+
+        $this->assertFalse($verdict->broken, 'neither tree can run, and the author is told the same thing either way');
+        $this->assertStringStartsWith('type preservation upheld: both refuse:', $verdict->describe());
+    }
+
+    #[Test]
+    public function two_different_refusals_break_type_preservation(): void
+    {
+        $verdict = (new TypePreservation())->check(self::site(
+            new SymbolSource('missing'),
+            new UnaryExpression('!', new SymbolSource('count')),
+            ['count' => new NumberType()],
+        ));
+
+        $this->assertTrue($verdict->broken, 'a rewrite must not be what changes the diagnostic an author reads');
+        $this->assertStringContainsString('both refuse, but differently:', $verdict->describe());
+    }
+
+    #[Test]
+    public function a_corpus_that_agrees_upholds_verdict_preservation(): void
+    {
+        $obligation = new VerdictPreservation(new ArrayBindingsCorpus([
+            'yes' => ['flag' => true],
+            'no' => ['flag' => false],
+        ]));
+
+        $verdict = $obligation->check(self::site(
+            new UnaryExpression('!', new UnaryExpression('!', new SymbolSource('flag'))),
+            new SymbolSource('flag'),
+            ['flag' => new BooleanType()],
+        ));
+
+        $this->assertFalse($verdict->broken);
+        $this->assertSame('verdict preservation upheld: 2 corpus case(s) agree', $verdict->describe());
+    }
+
+    #[Test]
+    public function absence_answers_alike_and_still_counts(): void
+    {
+        $obligation = new VerdictPreservation(new ArrayBindingsCorpus(['unanswered' => []]));
+
+        $verdict = $obligation->check(self::site(
+            new SymbolSource('roof'),
+            new SymbolSource('roof'),
+            ['roof' => new Optional(new OptionType(new NumberType()))],
+        ));
+
+        $this->assertSame('verdict preservation upheld: 1 corpus case(s) agree', $verdict->describe());
+    }
+
+    #[Test]
+    public function one_disagreeing_case_breaks_verdict_preservation_and_names_itself(): void
+    {
+        $obligation = new VerdictPreservation(new ArrayBindingsCorpus([
+            'ordinary' => ['divisor' => 2],
+            'zero' => ['divisor' => 0],
+        ]));
+
+        $verdict = $obligation->check(self::site(
+            new InfixExpression(new StaticSource(10), '/', new SymbolSource('divisor')),
+            new StaticSource(5),
+            ['divisor' => new NumberType()],
+        ));
+
+        $this->assertTrue($verdict->broken);
+        $this->assertStringContainsString('case [zero]: the original answers error(', $verdict->describe());
+        $this->assertStringContainsString('and the replacement value(5)', $verdict->describe());
+    }
+
+    #[Test]
+    public function a_subtree_that_does_not_compile_leaves_verdicts_unchecked(): void
+    {
+        $obligation = new VerdictPreservation(new ArrayBindingsCorpus(['any' => []]));
+
+        $verdict = $obligation->check(self::site(new SymbolSource('missing'), new StaticSource(1)));
+
+        $this->assertFalse($verdict->checked);
+        $this->assertFalse($verdict->broken);
+        $this->assertSame('verdict preservation unchecked: a subtree does not compile, so there is no pair of programs to run', $verdict->describe());
+    }
+
+    #[Test]
+    public function a_replacement_that_does_not_compile_leaves_verdicts_unchecked(): void
+    {
+        $obligation = new VerdictPreservation(new ArrayBindingsCorpus(['any' => []]));
+
+        $verdict = $obligation->check(self::site(new StaticSource(1), new SymbolSource('missing')));
+
+        $this->assertFalse($verdict->checked);
+    }
+
+    #[Test]
+    public function each_obligation_answers_for_one_preservation(): void
+    {
+        $this->assertSame(Preservation::CertifiedType, (new TypePreservation())->preservation());
+        $this->assertSame(Preservation::Verdict, (new VerdictPreservation(new ArrayBindingsCorpus([])))->preservation());
+    }
+}
diff --git a/tests/Rewrite/RewriterTest.php b/tests/Rewrite/RewriterTest.php
new file mode 100644
index 0000000..902c3c7
--- /dev/null
+++ b/tests/Rewrite/RewriterTest.php
@@ -0,0 +1,430 @@
+<?php
+
+declare(strict_types=1);
+
+namespace Superscript\Axiom\Tests\Rewrite;
+
+use PHPUnit\Framework\Attributes\CoversClass;
+use PHPUnit\Framework\Attributes\Test;
+use PHPUnit\Framework\Attributes\UsesNamespace;
+use PHPUnit\Framework\TestCase;
+use Superscript\Axiom\Expression;
+use Superscript\Axiom\Rewrite\ArrayBindingsCorpus;
+use Superscript\Axiom\Rewrite\CoreSourceDescenders;
+use Superscript\Axiom\Rewrite\ObligationVerdict;
+use Superscript\Axiom\Rewrite\VerdictPreservation;
+use Superscript\Axiom\Rewrite\Descent;
+use Superscript\Axiom\Rewrite\Describes;
+use Superscript\Axiom\Rewrite\OpaqueSource;
+use Superscript\Axiom\Rewrite\Preservation;
+use Superscript\Axiom\Rewrite\RewriteOutcome;
+use Superscript\Axiom\Rewrite\RewriteRecord;
+use Superscript\Axiom\Rewrite\RewriteReport;
+use Superscript\Axiom\Rewrite\Rewriter;
+use Superscript\Axiom\Rewrite\RewriteRun;
+use Superscript\Axiom\Rewrite\RewriteWalk;
+use Superscript\Axiom\Rewrite\Rules\RemoveDoubleNegation;
+use Superscript\Axiom\Rewrite\SourceDescenders;
+use Superscript\Axiom\Rewrite\SourcePath;
+use Superscript\Axiom\Source;
+use Superscript\Axiom\Sources\Ascription;
+use Superscript\Axiom\Sources\Coerce;
+use Superscript\Axiom\Sources\DefaultValue;
+use Superscript\Axiom\Sources\ExpressionPattern;
+use Superscript\Axiom\Sources\InfixExpression;
+use Superscript\Axiom\Sources\LiteralPattern;
+use Superscript\Axiom\Sources\MatchArm;
+use Superscript\Axiom\Sources\MatchExpression;
+use Superscript\Axiom\Sources\MemberAccessSource;
+use Superscript\Axiom\Sources\StaticSource;
+use Superscript\Axiom\Sources\SymbolSource;
+use Superscript\Axiom\Sources\UnaryExpression;
+use Superscript\Axiom\Sources\WildcardPattern;
+use Superscript\Axiom\Tests\Fixtures\HostValueSource;
+use Superscript\Axiom\Tests\Rewrite\Fixtures\BoxExtension;
+use Superscript\Axiom\Tests\Rewrite\Fixtures\BoxSource;
+use Superscript\Axiom\Tests\Rewrite\Fixtures\StubRule;
+use Superscript\Axiom\Types\BooleanType;
+use Superscript\Axiom\Types\NumberType;
+use Superscript\Axiom\Types\OptionType;
+use Superscript\Axiom\Types\RecordType;
+use Superscript\Axiom\Types\StringType;
+
+#[CoversClass(Rewriter::class)]
+#[CoversClass(RewriteWalk::class)]
+#[CoversClass(RewriteRun::class)]
+#[CoversClass(RewriteReport::class)]
+#[CoversClass(RewriteRecord::class)]
+#[CoversClass(OpaqueSource::class)]
+#[CoversClass(Describes::class)]
+#[CoversClass(Descent::class)]
+#[CoversClass(CoreSourceDescenders::class)]
+#[CoversClass(SourceDescenders::class)]
+#[CoversClass(SourcePath::class)]
+#[UsesNamespace('Superscript\\Axiom')]
+final class RewriterTest extends TestCase
+{
+    /** @param list<\Superscript\Axiom\Rewrite\RewriteRule> $rules */
+    private static function rewrite(Source $source, array $rules, RecordType|array $declarations = [], ?SourceDescenders $descenders = null): RewriteRun
+    {
+        return (new Rewriter($rules, $descenders))->rewrite(new Expression($source, declarations: $declarations));
+    }
+
+    private static function replaces(string $identifier, string $class, Source $replacement): StubRule
+    {
+        /** @var non-empty-list<class-string<Source>> $visits */
+        $visits = [$class];
+
+        return new StubRule($identifier, $visits, static fn(Source $source): Source => $replacement);
+    }
+
+    #[Test]
+    public function an_untouched_tree_comes_back_as_the_same_instance(): void
+    {
+        $source = new InfixExpression(new SymbolSource('a'), '&&', new SymbolSource('b'));
+
+        $run = self::rewrite($source, [], ['a' => new BooleanType(), 'b' => new BooleanType()]);
+
+        $this->assertSame($source, $run->source, 'nothing fired, so nothing was rebuilt');
+        $this->assertFalse($run->changed);
+        $this->assertSame('no rewrites, nothing opaque', $run->report->describe());
+    }
+
+    #[Test]
+    public function untouched_siblings_keep_their_identity_when_one_child_is_rewritten(): void
+    {
+        $left = new UnaryExpression('!', new UnaryExpression('!', new SymbolSource('a')));
+        $right = new SymbolSource('b');
+        $source = new InfixExpression($left, '&&', $right);
+
+        $run = self::rewrite($source, [new RemoveDoubleNegation()], ['a' => new BooleanType(), 'b' => new BooleanType()]);
+
+        $this->assertInstanceOf(InfixExpression::class, $run->source);
+        $this->assertNotSame($source, $run->source);
+        $this->assertSame($right, $run->source->right, 'the untouched subtree is the very same instance');
+        $this->assertSame('a && b', $run->source->describe());
+        $this->assertTrue($run->changed);
+    }
+
+    #[Test]
+    public function bottom_up_application_collapses_a_nest_in_one_pass(): void
+    {
+        $source = new UnaryExpression('!', new UnaryExpression('!', new UnaryExpression('!', new UnaryExpression('!', new SymbolSource('a')))));
+
+        $run = self::rewrite($source, [new RemoveDoubleNegation()], ['a' => new BooleanType()]);
+
+        $this->assertSame('a', $run->source->describe());
+        $this->assertCount(2, $run->report->applied());
+    }
+
+    #[Test]
+    public function a_rewritten_expression_carries_the_original_scope(): void
+    {
+        $source = new UnaryExpression('!', new UnaryExpression('!', new SymbolSource('a')));
+
+        $run = self::rewrite($source, [new RemoveDoubleNegation()], ['a' => new BooleanType()]);
+        $program = $run->expression()->compile()->unwrap();
+
+        $this->assertTrue($program(['a' => true])->unwrap()->unwrap());
+        $this->assertSame($run->original->declarations, $run->expression()->declarations);
+    }
+
+    #[Test]
+    public function a_site_is_reported_with_its_path_before_and_after(): void
+    {
+        $source = new InfixExpression(new SymbolSource('a'), '&&', new UnaryExpression('!', new UnaryExpression('!', new SymbolSource('b'))));
+
+        $run = self::rewrite($source, [new RemoveDoubleNegation()], ['a' => new BooleanType(), 'b' => new BooleanType()]);
+        $applied = $run->report->applied();
+
+        $this->assertCount(1, $applied);
+        $this->assertSame(RewriteOutcome::Applied, $applied[0]->outcome);
+        $this->assertSame('$.right', $applied[0]->path);
+        $this->assertSame('axiom.rewrite.remove-double-negation', $applied[0]->rule);
+        $this->assertSame('!!b', $applied[0]->before);
+        $this->assertSame('b', $applied[0]->after);
+        $this->assertSame(
+            "applied axiom.rewrite.remove-double-negation at \$.right: !!b => b"
+            . "\n  type preservation upheld: both compile to Boolean"
+            . "\n  verdict preservation unchecked: the run was given no oracle for this claim",
+            $run->report->describe(),
+        );
+    }
+
+    #[Test]
+    public function a_broken_obligation_refuses_that_site_and_reports_it(): void
+    {
+        $source = new UnaryExpression('!', new UnaryExpression('!', new SymbolSource('count')));
+
+        $run = self::rewrite($source, [new RemoveDoubleNegation()], ['count' => new NumberType()]);
+
+        $this->assertSame($source, $run->source, 'a refused rewrite leaves the tree exactly as it was');
+        $this->assertFalse($run->changed);
+        $this->assertSame([], $run->report->applied());
+
+        $refused = $run->report->refused();
+        $this->assertCount(1, $refused);
+        $this->assertSame('$', $refused[0]->path);
+        $this->assertStringContainsString('type preservation broken: the original refuses and the replacement compiles', $refused[0]->describe());
+        $this->assertStringContainsString('verdict preservation unchecked: the run was given no oracle for this claim', $refused[0]->describe());
+    }
+
+    #[Test]
+    public function a_refused_rule_lets_the_next_rule_take_the_site(): void
+    {
+        $source = new SymbolSource('a');
+        $unsound = self::replaces('unsound', SymbolSource::class, new Coerce(new StringType(), new StaticSource('a string where a boolean was')));
+        $sound = self::replaces('sound', SymbolSource::class, new Coerce(new BooleanType(), new StaticSource(true)));
+
+        $run = self::rewrite($source, [$unsound, $sound], ['a' => new BooleanType()]);
+
+        $this->assertSame([RewriteOutcome::Refused, RewriteOutcome::Applied], array_map(fn(RewriteRecord $record): RewriteOutcome => $record->outcome, $run->report->records));
+        $this->assertSame(['unsound'], array_map(fn(RewriteRecord $record): string => $record->rule, $run->report->refused()));
+        $this->assertSame(['sound'], array_map(fn(RewriteRecord $record): string => $record->rule, $run->report->applied()));
+        $this->assertSame('true (as boolean)', Describes::node($run->source));
+    }
+
+    #[Test]
+    public function the_first_sound_rewrite_ends_the_visit(): void
+    {
+        $first = self::replaces('first', SymbolSource::class, new Coerce(new BooleanType(), new StaticSource(true)));
+        $second = self::replaces('second', SymbolSource::class, new Coerce(new BooleanType(), new StaticSource(false)));
+
+        $run = self::rewrite(new SymbolSource('a'), [$first, $second], ['a' => new BooleanType()]);
+
+        $this->assertCount(1, $run->report->records);
+        $this->assertSame('first', $run->report->applied()[0]->rule);
+    }
+
+    #[Test]
+    public function a_rule_that_offers_nothing_is_passed_over(): void
+    {
+        /** @var non-empty-list<class-string<Source>> $visits */
+        $visits = [SymbolSource::class];
+        $silent = new StubRule('silent', $visits, static fn(Source $source): ?Source => null);
+        $source = new SymbolSource('a');
+
+        $run = self::rewrite($source, [$silent], ['a' => new BooleanType()]);
+
+        $this->assertSame($source, $run->source);
+        $this->assertSame([], $run->report->records);
+    }
+
+    #[Test]
+    public function a_rule_is_only_offered_the_exact_classes_it_visits(): void
+    {
+        $seen = [];
+        /** @var non-empty-list<class-string<Source>> $visits */
+        $visits = [SymbolSource::class];
+        $spy = new StubRule('spy', $visits, static function (Source $source) use (&$seen): ?Source {
+            $seen[] = $source::class;
+
+            return null;
+        });
+
+        self::rewrite(new InfixExpression(new SymbolSource('a'), '&&', new StaticSource(true)), [$spy], ['a' => new BooleanType()]);
+
+        $this->assertSame([SymbolSource::class], $seen);
+    }
+
+    #[Test]
+    public function a_claim_the_rule_repeats_is_judged_once_and_the_rest_still_judged(): void
+    {
+        /** @var non-empty-list<class-string<Source>> $visits */
+        $visits = [SymbolSource::class];
+        $rule = new StubRule(
+            'repeats',
+            $visits,
+            static fn(Source $source): Source => new Coerce(new BooleanType(), new StaticSource(true)),
+            [Preservation::CertifiedType, Preservation::Verdict],
+        );
+
+        $run = self::rewrite(new SymbolSource('a'), [$rule], ['a' => new BooleanType()]);
+
+        $this->assertSame(
+            ['type preservation upheld: both compile to Boolean', 'verdict preservation unchecked: the run was given no oracle for this claim'],
+            array_map(fn(ObligationVerdict $verdict): string => $verdict->describe(), $run->report->applied()[0]->verdicts),
+        );
+    }
+
+    #[Test]
+    public function a_rule_that_offers_nothing_lets_the_next_rule_take_the_site(): void
+    {
+        /** @var non-empty-list<class-string<Source>> $visits */
+        $visits = [SymbolSource::class];
+        $silent = new StubRule('silent', $visits, static fn(Source $source): ?Source => null);
+        $sound = self::replaces('sound', SymbolSource::class, new Coerce(new BooleanType(), new StaticSource(true)));
+
+        $run = self::rewrite(new SymbolSource('a'), [$silent, $sound], ['a' => new BooleanType()]);
+
+        $this->assertSame(['sound'], array_map(fn(RewriteRecord $record): string => $record->rule, $run->report->applied()));
+    }
+
+    #[Test]
+    public function an_applied_site_and_a_refused_one_are_reported_side_by_side(): void
+    {
+        $source = new InfixExpression(
+            new UnaryExpression('!', new UnaryExpression('!', new SymbolSource('flag'))),
+            '&&',
+            new UnaryExpression('!', new UnaryExpression('!', new SymbolSource('count'))),
+        );
+
+        $run = self::rewrite($source, [new RemoveDoubleNegation()], ['flag' => new BooleanType(), 'count' => new NumberType()]);
+
+        $this->assertSame(['$.left'], array_map(fn(RewriteRecord $record): string => $record->path, $run->report->applied()));
+        $this->assertSame(['$.right'], array_map(fn(RewriteRecord $record): string => $record->path, $run->report->refused()));
+    }
+
+    #[Test]
+    public function an_unregistered_host_shape_is_an_opaque_leaf_the_run_reports(): void
+    {
+        $hidden = new UnaryExpression('!', new UnaryExpression('!', new SymbolSource('a')));
+        $source = new InfixExpression(new SymbolSource('a'), '&&', new HostValueSource(new BooleanType(), $hidden));
+
+        $run = self::rewrite($source, [new RemoveDoubleNegation()], ['a' => new BooleanType()]);
+
+        $this->assertSame($source, $run->source, 'an opaque node is never descended and never rewritten');
+        $this->assertSame([], $run->report->applied());
+        $this->assertCount(1, $run->report->opaque);
+        $this->assertSame('$.right', $run->report->opaque[0]->path);
+        $this->assertSame(HostValueSource::class, $run->report->opaque[0]->class);
+        $this->assertSame('HostValueSource', $run->report->opaque[0]->describe, 'a host node that cannot spell itself is named by its class');
+        $this->assertStringContainsString('opaque ' . HostValueSource::class . ' at $.right: HostValueSource', $run->report->describe());
+    }
+
+    #[Test]
+    public function a_registered_host_shape_is_descended_and_rebuilt(): void
+    {
+        $descenders = SourceDescenders::core()->with(new BoxExtension());
+        $source = new BoxSource(new UnaryExpression('!', new UnaryExpression('!', new SymbolSource('a'))));
+
+        $run = self::rewrite($source, [new RemoveDoubleNegation()], ['a' => new BooleanType()], $descenders);
+
+        $this->assertInstanceOf(BoxSource::class, $run->source);
+        $this->assertSame('box(a)', $run->source->describe());
+        $this->assertSame('$.inner', $run->report->applied()[0]->path);
+        $this->assertSame([], $run->report->opaque);
+    }
+
+    #[Test]
+    public function a_registered_host_shape_shares_structure_when_nothing_moved(): void
+    {
+        $descenders = SourceDescenders::core()->with(new BoxExtension());
+        $source = new BoxSource(new SymbolSource('a'));
+
+        $run = self::rewrite($source, [new RemoveDoubleNegation()], ['a' => new BooleanType()], $descenders);
+
+        $this->assertSame($source, $run->source);
+    }
+
+    #[Test]
+    public function every_core_shape_is_descended_through(): void
+    {
+        $doubled = new UnaryExpression('!', new UnaryExpression('!', new SymbolSource('flag')));
+        $source = new MatchExpression(
+            subject: new Coerce(new StringType(), new MemberAccessSource(new SymbolSource('customer'), 'name')),
+            arms: [
+                new MatchArm(new LiteralPattern('ada'), new Ascription(new BooleanType(), $doubled)),
+                new MatchArm(new ExpressionPattern(new DefaultValue(new StaticSource('bob'), 'bob')), new StaticSource(false)),
+                new MatchArm(new WildcardPattern(), new InfixExpression($doubled, '||', new StaticSource(false))),
+            ],
+        );
+
+        $run = self::rewrite($source, [new RemoveDoubleNegation()], [
+            'flag' => new BooleanType(),
+            'customer' => new RecordType(['name' => new StringType()]),
+        ]);
+
+        $this->assertSame([
+            '$.arms[0].expression.source',
+            '$.arms[2].expression.left',
+        ], array_map(fn(RewriteRecord $record): string => $record->path, $run->report->applied()));
+        $this->assertSame('match customer.name (as string) { \'ada\' => flag (is boolean), \'bob\' ?? \'bob\' => false, _ => flag || false }', $run->source->describe());
+    }
+
+    /**
+     * A rewrite under a node that only wraps its child — a coercion, an
+     * authored default, a member access — must rebuild the wrapper around the
+     * new child and keep everything else about it.
+     */
+    #[Test]
+    public function a_wrapping_shape_rebuilds_around_a_rewritten_child(): void
+    {
+        $alias = self::replaces('alias', SymbolSource::class, new SymbolSource('b'));
+        $record = new RecordType(['name' => new StringType()]);
+
+        $coerce = self::rewrite(new Coerce(new StringType(), new SymbolSource('a')), [$alias], ['a' => new StringType(), 'b' => new StringType()]);
+        $default = self::rewrite(new DefaultValue(new SymbolSource('a'), 0), [$alias], ['a' => new OptionType(new NumberType()), 'b' => new OptionType(new NumberType())]);
+        $member = self::rewrite(new MemberAccessSource(new SymbolSource('a'), 'name'), [$alias], ['a' => $record, 'b' => $record]);
+
+        $this->assertSame('b (as string)', Describes::node($coerce->source));
+        $this->assertSame('b ?? 0', Describes::node($default->source));
+        $this->assertSame('b.name', Describes::node($member->source));
+    }
+
+    #[Test]
+    public function a_match_arm_and_its_pattern_keep_their_identity_when_nothing_moved(): void
+    {
+        $arm = new MatchArm(new ExpressionPattern(new StaticSource('ada')), new StaticSource(1));
+        $source = new MatchExpression(new SymbolSource('name'), [$arm, new MatchArm(new WildcardPattern(), new StaticSource(0))]);
+
+        $run = self::rewrite($source, [new RemoveDoubleNegation()], ['name' => new StringType()]);
+
+        $this->assertSame($source, $run->source);
+    }
+
+    #[Test]
+    public function a_rewrite_inside_an_expression_pattern_rebuilds_the_arm(): void
+    {
+        $source = new MatchExpression(
+            subject: new SymbolSource('flag'),
+            arms: [
+                new MatchArm(new ExpressionPattern(new UnaryExpression('!', new UnaryExpression('!', new SymbolSource('flag')))), new StaticSource(1)),
+                new MatchArm(new WildcardPattern(), new StaticSource(0)),
+            ],
+        );
+
+        $run = self::rewrite($source, [new RemoveDoubleNegation()], ['flag' => new BooleanType()]);
+
+        $this->assertSame('match flag { flag => 1, _ => 0 }', $run->source->describe());
+        $this->assertSame('$.arms[0].pattern.source', $run->report->applied()[0]->path);
+    }
+
+    #[Test]
+    public function an_unknown_pattern_shape_is_opaque_too(): void
+    {
+        $pattern = new class implements \Superscript\Axiom\Sources\MatchPattern {};
+        $source = new MatchExpression(new SymbolSource('flag'), [new MatchArm($pattern, new StaticSource(1))]);
+
+        $run = self::rewrite($source, [new RemoveDoubleNegation()], ['flag' => new BooleanType()]);
+
+        $this->assertSame($source, $run->source);
+        $this->assertCount(1, $run->report->opaque);
+        $this->assertSame('$.arms[0].pattern', $run->report->opaque[0]->path);
+    }
+
+    #[Test]
+    public function a_path_segment_names_a_property(): void
+    {
+        $this->assertSame('$.left.operand', SourcePath::root()->child('left')->child('operand')->describe());
+    }
+
+    #[Test]
+    public function an_oracle_the_run_is_given_answers_the_claim_it_discharges(): void
+    {
+        $rewriter = new Rewriter(
+            [new RemoveDoubleNegation()],
+            obligations: [new VerdictPreservation(new ArrayBindingsCorpus(['yes' => ['a' => true]]))],
+        );
+
+        $run = $rewriter->rewrite(new Expression(
+            new UnaryExpression('!', new UnaryExpression('!', new SymbolSource('a'))),
+            declarations: ['a' => new BooleanType()],
+        ));
+
+        $this->assertSame(
+            ['type preservation upheld: both compile to Boolean', 'verdict preservation upheld: 1 corpus case(s) agree'],
+            array_map(fn(ObligationVerdict $verdict): string => $verdict->describe(), $run->report->applied()[0]->verdicts),
+        );
+    }
+}
diff --git a/tests/Rewrite/Rules/RemoveDoubleNegationTest.php b/tests/Rewrite/Rules/RemoveDoubleNegationTest.php
new file mode 100644
index 0000000..f7c80ed
--- /dev/null
+++ b/tests/Rewrite/Rules/RemoveDoubleNegationTest.php
@@ -0,0 +1,155 @@
+<?php
+
+declare(strict_types=1);
+
+namespace Superscript\Axiom\Tests\Rewrite\Rules;
+
+use PHPUnit\Framework\Attributes\CoversClass;
+use PHPUnit\Framework\Attributes\Test;
+use PHPUnit\Framework\Attributes\UsesNamespace;
+use PHPUnit\Framework\TestCase;
+use Superscript\Axiom\Expression;
+use Superscript\Axiom\Rewrite\ArrayBindingsCorpus;
+use Superscript\Axiom\Rewrite\Preservation;
+use Superscript\Axiom\Rewrite\Rewriter;
+use Superscript\Axiom\Rewrite\Rules\RemoveDoubleNegation;
+use Superscript\Axiom\Rewrite\VerdictPreservation;
+use Superscript\Axiom\Sources\InfixExpression;
+use Superscript\Axiom\Sources\StaticSource;
+use Superscript\Axiom\Sources\SymbolSource;
+use Superscript\Axiom\Sources\UnaryExpression;
+use Superscript\Axiom\Types\BooleanType;
+use Superscript\Axiom\Types\NumberType;
+use Superscript\Axiom\Types\Optional;
+use Superscript\Axiom\Types\OptionType;
+
+#[CoversClass(RemoveDoubleNegation::class)]
+#[UsesNamespace('Superscript\\Axiom')]
+final class RemoveDoubleNegationTest extends TestCase
+{
+    #[Test]
+    public function a_pair_of_negations_leaves_only_the_operand(): void
+    {
+        $operand = new SymbolSource('flag');
+
+        $rewritten = (new RemoveDoubleNegation())->rewrite(new UnaryExpression('!', new UnaryExpression('!', $operand)));
+
+        $this->assertSame($operand, $rewritten);
+    }
+
+    #[Test]
+    public function the_two_spellings_of_negation_cancel_each_other(): void
+    {
+        $operand = new SymbolSource('flag');
+
+        $this->assertSame($operand, (new RemoveDoubleNegation())->rewrite(new UnaryExpression('not', new UnaryExpression('!', $operand))));
+        $this->assertSame($operand, (new RemoveDoubleNegation())->rewrite(new UnaryExpression('!', new UnaryExpression('not', $operand))));
+    }
+
+    #[Test]
+    public function a_single_negation_is_left_alone(): void
+    {
+        $this->assertNull((new RemoveDoubleNegation())->rewrite(new UnaryExpression('!', new SymbolSource('flag'))));
+    }
+
+    #[Test]
+    public function another_operator_is_left_alone(): void
+    {
+        $this->assertNull((new RemoveDoubleNegation())->rewrite(new UnaryExpression('-', new UnaryExpression('-', new SymbolSource('count')))));
+        $this->assertNull((new RemoveDoubleNegation())->rewrite(new UnaryExpression('!', new UnaryExpression('-', new SymbolSource('count')))));
+        $this->assertNull((new RemoveDoubleNegation())->rewrite(new UnaryExpression('-', new UnaryExpression('!', new SymbolSource('flag')))));
+    }
+
+    #[Test]
+    public function another_node_shape_is_left_alone(): void
+    {
+        $this->assertNull((new RemoveDoubleNegation())->rewrite(new StaticSource(true)));
+    }
+
+    #[Test]
+    public function a_dialect_declares_which_of_its_spellings_are_involutive(): void
+    {
+        $rule = new RemoveDoubleNegation(['!']);
+
+        $this->assertNull($rule->rewrite(new UnaryExpression('not', new UnaryExpression('not', new SymbolSource('flag')))));
+        $this->assertNotNull($rule->rewrite(new UnaryExpression('!', new UnaryExpression('!', new SymbolSource('flag')))));
+    }
+
+    #[Test]
+    public function it_visits_unary_expressions_and_claims_verdict_preservation(): void
+    {
+        $rule = new RemoveDoubleNegation();
+
+        $this->assertSame([UnaryExpression::class], $rule->visits());
+        $this->assertSame([Preservation::Verdict], $rule->preserves());
+        $this->assertSame('axiom.rewrite.remove-double-negation', $rule->identifier());
+    }
+
+    /**
+     * Absence is where a "harmless" simplification usually stops being one:
+     * the lifted `!` propagates it, so `!!` is the lift of the identity and
+     * an unanswered question stays unanswered on both sides of the rewrite.
+     */
+    #[Test]
+    public function it_is_neutral_over_absence(): void
+    {
+        $comparison = new InfixExpression(new SymbolSource('roof'), '>', new StaticSource(0.25));
+        $expression = new Expression(
+            source: new UnaryExpression('!', new UnaryExpression('!', $comparison)),
+            declarations: ['roof' => new Optional(new OptionType(new NumberType()))],
+        );
+
+        $run = (new Rewriter(
+            [new RemoveDoubleNegation()],
+            obligations: [new VerdictPreservation(new ArrayBindingsCorpus([
+                'above' => ['roof' => 0.3],
+                'below' => ['roof' => 0.1],
+                'unanswered' => [],
+            ]))],
+        ))->rewrite($expression);
+
+        $this->assertSame('roof > 0.25', $run->source->describe());
+        $this->assertSame('verdict preservation upheld: 3 corpus case(s) agree', $run->report->applied()[0]->verdicts[1]->describe());
+
+        $program = $run->expression()->compile()->unwrap();
+        $this->assertTrue($program([])->unwrap()->isNone(), 'not-knowing, negated twice or not at all, is still not-knowing');
+    }
+
+    #[Test]
+    public function a_negation_over_something_that_is_not_boolean_is_refused_rather_than_simplified(): void
+    {
+        $expression = new Expression(
+            source: new UnaryExpression('!', new UnaryExpression('!', new SymbolSource('count'))),
+            declarations: ['count' => new NumberType()],
+        );
+
+        $run = (new Rewriter([new RemoveDoubleNegation()]))->rewrite($expression);
+
+        $this->assertFalse($run->changed, 'the original never compiled; handing back a certified Number program would invent one');
+        $this->assertCount(1, $run->report->refused());
+    }
+
+    #[Test]
+    public function a_boolean_expression_keeps_its_answers(): void
+    {
+        $expression = new Expression(
+            source: new InfixExpression(
+                new UnaryExpression('!', new UnaryExpression('!', new SymbolSource('flag'))),
+                '&&',
+                new UnaryExpression('!', new SymbolSource('other')),
+            ),
+            declarations: ['flag' => new BooleanType(), 'other' => new BooleanType()],
+        );
+
+        $run = (new Rewriter([new RemoveDoubleNegation()]))->rewrite($expression);
+        $before = $expression->compile()->unwrap();
+        $after = $run->expression()->compile()->unwrap();
+
+        foreach ([[true, true], [true, false], [false, true], [false, false]] as [$flag, $other]) {
+            $bindings = ['flag' => $flag, 'other' => $other];
+            $this->assertSame($before($bindings)->unwrap()->unwrap(), $after($bindings)->unwrap()->unwrap());
+        }
+
+        $this->assertSame('flag && !other', $run->source->describe());
+    }
+}
diff --git a/tests/Rewrite/Rules/RemoveRedundantDefaultTest.php b/tests/Rewrite/Rules/RemoveRedundantDefaultTest.php
new file mode 100644
index 0000000..e7ccafe
--- /dev/null
+++ b/tests/Rewrite/Rules/RemoveRedundantDefaultTest.php
@@ -0,0 +1,105 @@
+<?php
+
+declare(strict_types=1);
+
+namespace Superscript\Axiom\Tests\Rewrite\Rules;
+
+use PHPUnit\Framework\Attributes\CoversClass;
+use PHPUnit\Framework\Attributes\Test;
+use PHPUnit\Framework\Attributes\UsesNamespace;
+use PHPUnit\Framework\TestCase;
+use Superscript\Axiom\Expression;
+use Superscript\Axiom\Rewrite\Preservation;
+use Superscript\Axiom\Rewrite\Rewriter;
+use Superscript\Axiom\Rewrite\Rules\RemoveRedundantDefault;
+use Superscript\Axiom\Sources\DefaultValue;
+use Superscript\Axiom\Sources\SymbolSource;
+use Superscript\Axiom\Types\NumberType;
+use Superscript\Axiom\Types\OptionType;
+
+#[CoversClass(RemoveRedundantDefault::class)]
+#[UsesNamespace('Superscript\\Axiom')]
+final class RemoveRedundantDefaultTest extends TestCase
+{
+    #[Test]
+    public function it_proposes_the_inner_source_of_any_default(): void
+    {
+        $inner = new SymbolSource('amount');
+
+        $this->assertSame($inner, (new RemoveRedundantDefault())->rewrite(new DefaultValue($inner, 0)));
+        $this->assertNull((new RemoveRedundantDefault())->rewrite($inner));
+    }
+
+    #[Test]
+    public function it_visits_defaults_and_claims_verdict_preservation(): void
+    {
+        $rule = new RemoveRedundantDefault();
+
+        $this->assertSame([DefaultValue::class], $rule->visits());
+        $this->assertSame([Preservation::Verdict], $rule->preserves());
+        $this->assertSame('axiom.rewrite.remove-redundant-default', $rule->identifier());
+    }
+
+    #[Test]
+    public function a_default_over_a_definite_source_is_removed(): void
+    {
+        $expression = new Expression(
+            source: new DefaultValue(new SymbolSource('amount'), 0),
+            declarations: ['amount' => new NumberType()],
+        );
+
+        $run = (new Rewriter([new RemoveRedundantDefault()]))->rewrite($expression);
+
+        $this->assertSame('amount', $run->source->describe());
+        $this->assertSame('type preservation upheld: both compile to Number', $run->report->applied()[0]->verdicts[0]->describe());
+    }
+
+    #[Test]
+    public function a_default_that_can_actually_fire_is_refused(): void
+    {
+        $expression = new Expression(
+            source: new DefaultValue(new SymbolSource('amount'), 0),
+            declarations: ['amount' => new OptionType(new NumberType())],
+        );
+
+        $run = (new Rewriter([new RemoveRedundantDefault()]))->rewrite($expression);
+
+        $this->assertFalse($run->changed);
+        $this->assertSame(
+            'type preservation broken: the original compiles to Number and the replacement to Number?',
+            $run->report->refused()[0]->verdicts[0]->describe(),
+        );
+    }
+
+    #[Test]
+    public function a_nested_redundant_default_is_removed_without_touching_the_useful_one(): void
+    {
+        $expression = new Expression(
+            source: new DefaultValue(new DefaultValue(new SymbolSource('amount'), 1), 0),
+            declarations: ['amount' => new OptionType(new NumberType())],
+        );
+
+        $run = (new Rewriter([new RemoveRedundantDefault()]))->rewrite($expression);
+
+        $this->assertSame('amount ?? 1', $run->source->describe(), 'the inner default is the one absence can reach');
+        $this->assertSame(['$'], array_map(fn($record): string => $record->path, $run->report->applied()));
+        $this->assertSame(['$.source'], array_map(fn($record): string => $record->path, $run->report->refused()));
+    }
+
+    #[Test]
+    public function the_program_answers_the_same_thing_either_way(): void
+    {
+        $expression = new Expression(
+            source: new DefaultValue(new SymbolSource('amount'), 0),
+            declarations: ['amount' => new NumberType()],
+        );
+
+        $run = (new Rewriter([new RemoveRedundantDefault()]))->rewrite($expression);
+
+        $before = $expression->compile()->unwrap();
+        $after = $run->expression()->compile()->unwrap();
+
+        $this->assertSame(7, $before(['amount' => 7])->unwrap()->unwrap());
+        $this->assertSame(7, $after(['amount' => 7])->unwrap()->unwrap());
+    }
+}
diff --git a/tests/Rewrite/SourceDescendersTest.php b/tests/Rewrite/SourceDescendersTest.php
new file mode 100644
index 0000000..81a70a3
--- /dev/null
+++ b/tests/Rewrite/SourceDescendersTest.php
@@ -0,0 +1,67 @@
+<?php
+
+declare(strict_types=1);
+
+namespace Superscript\Axiom\Tests\Rewrite;
+
+use InvalidArgumentException;
+use PHPUnit\Framework\Attributes\CoversClass;
+use PHPUnit\Framework\Attributes\Test;
+use PHPUnit\Framework\Attributes\UsesNamespace;
+use PHPUnit\Framework\TestCase;
+use Superscript\Axiom\Extension;
+use Superscript\Axiom\Rewrite\SourceDescenders;
+use Superscript\Axiom\Rewrite\SourcePath;
+use Superscript\Axiom\Sources\StaticSource;
+use Superscript\Axiom\Tests\Rewrite\Fixtures\BoxExtension;
+use Superscript\Axiom\Tests\Rewrite\Fixtures\BoxSource;
+
+#[CoversClass(SourceDescenders::class)]
+#[CoversClass(SourcePath::class)]
+#[CoversClass(Extension::class)]
+#[UsesNamespace('Superscript\\Axiom')]
+final class SourceDescendersTest extends TestCase
+{
+    #[Test]
+    public function an_extension_joins_its_arms_to_the_core_ones(): void
+    {
+        $descenders = SourceDescenders::core()->with(new BoxExtension());
+
+        $this->assertArrayHasKey(BoxSource::class, $descenders->sources);
+        $this->assertArrayHasKey(StaticSource::class, $descenders->sources, 'the core arms are always there');
+        $this->assertArrayNotHasKey(BoxSource::class, SourceDescenders::core()->sources, 'joining derives a new registry');
+    }
+
+    #[Test]
+    public function an_extension_contributes_no_descent_arms_by_default(): void
+    {
+        $extension = new class extends Extension {};
+
+        $this->assertSame([], $extension->sourceDescenders());
+        $this->assertSame(array_keys(SourceDescenders::core()->sources), array_keys(SourceDescenders::core()->with($extension)->sources));
+    }
+
+    #[Test]
+    public function two_extensions_claiming_one_class_is_a_configuration_error(): void
+    {
+        $this->expectException(InvalidArgumentException::class);
+        $this->expectExceptionMessage('Source class [' . BoxSource::class . '] has two descent arms; descent ownership is exact and extension order carries no precedence.');
+
+        SourceDescenders::core()->with(new BoxExtension(), new BoxExtension());
+    }
+
+    #[Test]
+    public function the_root_of_a_path_is_the_tree_itself(): void
+    {
+        $this->assertSame('$', SourcePath::root()->describe());
+    }
+
+    #[Test]
+    public function a_path_segment_cannot_be_empty(): void
+    {
+        $this->expectException(InvalidArgumentException::class);
+        $this->expectExceptionMessage('A source path segment names a property and cannot be empty.');
+
+        SourcePath::root()->child('');
+    }
+}