Abstract
Reordering operations in a declared finite, straight-line MLIR Transform IR core must preserve request availability, handle phases, effects, and completed outcomes. We present a model-relative certificate framework for this core, restricted to operation handles and matcher-generated carriers. Polynomial interfaces describe request menus, completed coalgebras represent success and failure, and exact branch descriptors compile to ordinary fixed-unit Petri nets. For total-success paths, our reordering theorem constructs the swapped path from residual guards and derives Petri interchange from disjoint compiled supports. With exact atomic source summaries, concrete-to-rich refinement, and an exact target quotient as premises, the two paths have equivalent concrete outcomes. Two worked instances cover unit annotations and guarded handle generation. An independent finite-model audit validates 29 complete-marking transitions and 12 local exchange squares, and rejects seven targeted semantic mutations. Checks of 39 archived MLIR cases in each of two runs confirm the expected payload outputs and diagnostics. A repeated evaluation across 522 files in a fixed corpus available during development constructs 617 V3 kernel records, compared with 292 for V2, and records five native successes among six candidates. A mirror benchmark over 39 conditions confirms the structural count formulas. These results validate the finite model-to-Petri construction and show that the frozen pipeline operates reproducibly on the declared corpus.