Rewrite stored source under proved obligations

[robertvansteen]

Hosts that store expressions eventually have to change them in bulk, and today the only options are editing a corpus by hand (a migration nobody finishes) or a script (a migration nobody can prove). This adds Superscript\Axiom\Rewrite: a rule set applied bottom-up over an immutable Source 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.

Stacks on #93 (demanded-inputs); it targets that branch and should merge after it. Review only the last commit.

One expression, end to end

$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()],
);

$run = (new Rewriter(
    [new RemoveDoubleNegation()],
    obligations: [new VerdictPreservation(new ArrayBindingsCorpus([
        'answered' => ['roof' => 0.3, 'flag' => true],
        'unanswered' => ['flag' => false],
    ]))],
))->rewrite($expression);

Read the report 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: $run->changed is true, $run->source->describe() is (roof > 0.25) && flag, and $run->expression() puts it back under the original dialect, definitions, declarations and boundary. There is no mode flag — report-only is this same run with the tree ignored.

Now the same rule against a stored !!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 would have handed back a certified Number program in place of a refusal — one the author never wrote and the checker never blessed. One site is refused; the rest of the run proceeds.

What is in the box

• A rule owns matching and replacement for the exact Source classes it visits — identifier(), visits(), rewrite(Source): ?Source, preserves() — and writes no traversal. Structural knowledge stays in rules rather than becoming a method every host node must implement forever. Dispatch is exact-class indexed, so a node costs one array lookup however many rules a run carries.
• Descent belongs to the toolkit. CoreSourceDescenders has a descend-and-rebuild arm per core node (and per match pattern), and CoreDescentExhaustivenessTest reflects over src/Sources and fails if a class exists without one. Untouched subtrees come back as the same instance, so $run->changed is answered by identity.
• Opaque-leaf policy: a class no extension claims through Extension::sourceDescenders() is never descended, never rewritten — not even by a rule naming its own class, since a rule cannot be trusted to rebuild a shape the toolkit cannot take apart — and it is named in the report (opaque Acme\Sources\LookupSource at $.right: LookupSource). A silent skip would let a host add a node class, forget its arm, and read "no rewrites needed" as "nothing to do".
• Obligations: type preservation is checked at every site whether or not a rule claims it; verdict preservation runs both programs over a host BindingsCorpus and compares answers, naming the case that disagrees. A claim with no oracle is reported unchecked — which neither blocks a rewrite nor counts as evidence for one.
• Two reference rules. RemoveDoubleNegation 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. RemoveRedundantDefault is the other shape — 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 it proposes the removal everywhere and lets type preservation decide (Number against Number? refuses the ones absence can reach).

The namespaced-symbol migration is wire-level, not a Source rule

A natural question is whether the namespaced-symbol migration (the wire format this branch retires) is expressible here. It is not, and the reason is structural rather than a gap in the toolkit: SymbolSource no longer carries a namespace and its constructor rejects a dotted name outright, so stored {"name": "turnover", "namespace": "customer"} cannot be hydrated into any Source. There is no input tree for a rule to match. The migration belongs in the host's deserializer, which chooses MemberAccessSource(SymbolSource('customer'), 'turnover') before a tree exists. A migration is a rewrite rule only once both shapes are representable; this one changes the node set rather than moving within it. docs/rewriting.md states the distinction so the next such change is triaged in the right place.

Notes for the reviewer

• Paths are property-named ($.left.operand, $.arms[1].expression), deliberately not the $.children[0].node language compilation speaks. Those indices number the children a compiler recorded, and a compiler records what it needs — a wildcard arm records no pattern child — so the same arm sits at a different index depending on which patterns precede it. A coordinate into stored source must name the same node before anything is compiled.
• Both subtrees of a site compile standalone in the whole expression's scope. That is exact, not an approximation, 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.
• Extension gains one hook (sourceDescenders()) with the same exact, unranked ownership as sourceCompilers(), so one package declares both how its node compiles and how a rewrite reaches through it.
• CONTEXT.md gains one bullet: the file already names every seam a host implements, and rewrite rules, descent arms and the opaque leaf are one.

Validation

composer test green: PHPStan max clean, 1290 tests / 4911 assertions at 100% line coverage, Infection at MSI 100%. vendor/bin/pint --test clean on touched files, git diff --check clean.

[robertvansteen]

Kept as a design reference: this will be proven inside a host application first — module-local, against the current released model — and extracted here once the API has real migration rules behind it.

🤖 Generated with Claude Code