Rewrite Trace Log¶
Provenance log / artifact — instantiates Equivalence-Preserving Rewrite Optimization
An append-only record of every rewrite applied — the rule, the before/after forms, the evidence of equivalence, the cost delta, and the accept decision — so any change can be explained, reproduced, and undone.
When a chain of equivalence-preserving rewrites turns form A into form Z, the individual steps usually vanish — you are left with Z and a claim that it means the same as A. The Rewrite Trace Log refuses to let them vanish. It is the append-only record that captures, for each rewrite, the rule or transform applied, the before-and-after forms, the evidence that licensed it, the measured or estimated cost change, and the decision to accept it. It neither rewrites nor checks anything itself; its entire job is provenance — turning an opaque A→Z leap into a replayable, inspectable chain. That is what lets someone months later ask "which rewrite changed this, and why was it allowed?" and get an exact answer instead of a shrug.
Example¶
A logic-synthesis tool compiles a register-transfer-level hardware design into a gate netlist, applying thousands of equivalence-preserving rewrites — Boolean simplifications, restructurings of the and-inverter graph, technology remappings — to shrink area and delay. Weeks later, formal equivalence checking on a later revision flags a mismatch, and a timing path has quietly regressed.
The Rewrite Trace Log is what makes that tractable. Because every rewrite was logged with its rule, the sub-circuit it touched, its area/delay delta, and a reference to the equivalence check that licensed it, the engineers bisect the log — halving the rewrite sequence until the offending step is isolated.[n1] They find a single restructuring applied under an assumption about a don't-care condition that a later constraint had invalidated. The log shows the rule, the exact node, and the now-false precondition — one entry localised out of thousands — and the accompanying side-effect record confirms which downstream signals it perturbed.
How it works¶
For each applied rewrite the log appends a structured entry: an identifier for the rule or transform, the source and result forms (or a diff of them), the evidence of equivalence (a cited identity, a passed check, a discharged precondition), the cost criterion and its before/after value, and the accept decision. It also records what the rewrite touched beyond its main result — the exceptions and side effects it preserved or perturbed — because those are exactly what a value-level view misses. The log is deliberately passive and append-only: it asserts nothing about correctness and changes nothing, which is what makes it trustworthy as evidence. Its value is realised later, by reading it — to explain a change, reproduce a pipeline, or bisect a regression to the single step that caused it.
Tuning parameters¶
- Capture granularity — every micro-rewrite versus only milestone transforms. Fine granularity makes bisection exact but produces huge logs; coarse logging is compact but can only localise to a batch.
- Payload depth — full before/after forms versus a compact diff or hash. Full forms are self-contained and replayable; diffs and hashes save space but need the original to reconstruct.
- Evidence linkage — how tightly each entry ties to the check or identity that licensed it. Strong linkage makes the log auditable; weak linkage records what changed but not why it was allowed.
- Side-effect scope — how much exception, ordering, and side-effect detail each entry carries. More scope catches non-value drift; less keeps entries lean.
- Retention / immutability — how long entries are kept and how strictly append-only is enforced. Strong immutability makes the log admissible as an audit trail; aggressive pruning trades reproducibility for storage.
When it helps, and when it misleads¶
Its strength is the difference between an optimizer you can audit and one you must trust. A good trace log makes a rewrite chain reproducible, explains any single change on demand, and — its highest-value use — lets a downstream regression be bisected to the exact rewrite that introduced it, out of thousands.
Its limits come from being purely descriptive. A log is only as good as it is complete and honest: if capture is partial, the one rewrite that mattered may be the one not logged; if entries record what changed but not the evidence that licensed it, the log documents drift without explaining it. And a green, detailed log is not a correctness check — it will faithfully record rewrites that were wrong. The classic misuse is writing the log for compliance and never reading it, treating its mere existence as verification. The discipline: log every accepted rewrite with its licensing evidence, keep it append-only, and actually use it — to reproduce and to bisect — rather than to reassure.
How it implements the components¶
Rewrite Trace Log fills the recording components a provenance artifact owns:
rewrite_trace_and_provenance— it is the record: rule, before/after forms, licensing evidence, cost delta, and accept decision, appended per rewrite so the whole A→Z chain is replayable and auditable.exception_and_side_effect_register— each entry also logs the exceptions and side effects a rewrite preserved or perturbed, capturing the non-value behaviour a form-only record would lose.
It does not produce the rewrites it records (Compiler Optimization Pass, Peephole Optimization), does not decide whether a rewrite is equivalence-preserving (the oracle siblings — Golden-Output Regression Test, Metamorphic Test Suite), and does not measure the cost it logs (Benchmark Harness); it records what those mechanisms did and found.
Related¶
- Instantiates: Equivalence-Preserving Rewrite Optimization — it is the provenance layer that makes a rewrite chain auditable and reproducible.
- Consumes: the output of the rewriters and checkers it records — a Compiler Optimization Pass's transforms, a Benchmark Harness's cost figures, an oracle's verdicts.
- Sibling mechanisms: Compiler Optimization Pass · Benchmark Harness · Metamorphic Test Suite · Golden-Output Regression Test · Algebraic Simplification Rulebook
Editorial Notes¶
Form Classification¶
Form family: Record, Log & Register
Rationale: Rewrite Trace Log operates as a persistent ledger, log, register, or case record that preserves history and traceability because it an append-only record of every rewrite applied — the rule, the before/after forms, the evidence of equivalence, the cost delta, and the accept decision — so any change can be explained, reproduced, and undone.
Independent corroboration: The frozen evidence defines Rewrite Trace Log as 'An append-only record of every rewrite applied — the rule, the before/after forms, the evidence of equivalence, the cost delta, and the accept decision — so any change can be explained, reproduced, and undone', so its operative form is Record, Log & Register.
Review outcome: Independent reviewer agreement; high confidence.
Origin Attribution¶
Primary origin: Computer Science & Software Engineering
Origin pattern: Cross-disciplinary synthesis
Present-day reach: Multi-domain
Rationale: Append-only before-and-after transformation traces arise from software versioning and provenance systems.
Related originating lineages:
- Accounting & Auditing — Audit trails independently require authorized, explainable, reversible changes.
- Engineering & Design — Engineering design, reliability, and systems-safety practice supplies a parallel or contributing lineage for the mechanism's defining operation: an append-only record of every rewrite applied — the rule, the before/after forms, the evidence of equivalence, the cost delta, and the accept decision — so any change can be….
- Library & Information Science — Provenance and version history materially shape reproducible change records.
Review resolution: Both blind reviewers agree that computer_science is the primary historical origin. Explicit reconciliation of alternate origin disagreement, origin mode disagreement, domain reach disagreement, encyclopedia synthesis disagreement starts from reviewer_a’s mechanism-specific evidence: Append-only before-and-after transformation traces arise from software versioning and provenance systems. Reviewer A proposed alternates=accounting_auditing, library_information_science, origin_mode=cross_disciplinary_synthesis, domain_reach=multi_domain, and encyclopedia_synthesis=true; reviewer B proposed alternates=engineering_design, origin_mode=single_lineage, domain_reach=specialized, and encyclopedia_synthesis=false. The final record retains every independently supported alternate from either review (accounting_auditing, library_information_science, engineering_design) without an arbitrary cap, selects origin_mode=cross_disciplinary_synthesis to represent the combined lineage evidence, and keeps domain_reach=multi_domain and encyclopedia_synthesis=true from the more mechanism-specific assessment. Present-day transfer is recorded as reach and is not treated as proof of historical origin.
Encyclopedia synthesis: The exact catalogued form synthesizes established practice rather than reproducing a single standard historical label.
Review outcome: Reconciled after independent review; high confidence.
Notes¶
The trace log is the one mechanism here that produces nothing the optimization needs in order to run — it is pure overhead until something goes wrong, at which point it is often the only thing that helps. That insurance character (paid continuously, redeemed only on failure) is the real design tension, and it is why capture granularity is the load-bearing dial: log too little to save effort now, and the step you most need to find later is the one you did not record.
[n1] Bisection — repeatedly halving a sequence of changes to isolate the one responsible for a regression — is the standard way to localise a fault in a long chain (the technique behind tools such as git bisect). A rewrite trace log is what makes an optimizer's transform sequence bisectable at all. ↩