Rewrite stored source under proved obligations

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.

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.

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