A rewrite must carry its justification
A binary can decode, pass MLIR verification, and still compute the wrong answer or wait forever. sass2mlir’s contracts connect each representation to the obligations it cannot express alone. They grew out of concrete failures: predicated values losing their old destination, instruction edits emitting old raw words, legal scheduling codes producing incorrect results, and address bounds admitting cells that were never written.
The working rule is admit a modeled input → prepare a candidate → check its obligations → commit atomically. Missing evidence is a refusal. A successful check belongs to the exact input and IR epoch it examined; an edit can invalidate that evidence.
This chapter collects obligations across the compiler. The reusable checkers in
contracts/ implement particular subsets. Their presence does not make the
whole compiler formally verified.
Preserve the value on every path
For a guarded instruction, the result is guard ? new_value : old_value.
The old destination is a real input, tied to the physical destination. Replacing
the instruction with an unconditional operation, dropping the old-value source,
or treating a possible write as a definite kill changes the false-predicate path.
The contract: structured register occurrences must agree with actual SSA sources and results, including guard and retained old values. Physical effects must retain implicit reads, possible writes, definite kills, and register spans. Opaque effects cannot be interpreted as empty effects.
Follow the selected definition through control flow. A physical register name alone does not identify an SSA value, and ordinary SSA last-use does not establish physical safety. The FMA pass consequently refuses guarded contraction and checks whether the product survives after its apparent consumer.
Numerical meaning is also a premise. FMUL/FADD → FFMA changes rounding. Retiling attention changes accumulation order and rounding boundaries. State the permitted policy before transforming; neither mathematical equality nor a successful random run grants exact floating-point equivalence.
One host deletion check omitted the high half of a wide address: R4 was still read even though the visible operand projection missed it. The lesson is to query complete physical effects rather than infer them from the printed base register.
Landmarks: SassOps.cpp, SassInstAnalysis.h,
docs/development/instruction-register-bindings.md, and passes/fma.cpp.
The emitted word must describe the edited instruction
Retained raw words are authoritative: the emitter returns them verbatim.
Changing a structured operand while keeping the old word can therefore emit the
original instruction. Conversely, blindly rebuilding an opaque instruction can
destroy fields whose meaning the compiler does not own.
The contract: preserve untouched words; regenerate semantic edits through
the shared emitter after sass::mark_edited removes stale raw authority. A
specialized checked-raw path must install newly encoded, independently decoded
words. Respect encoder-owned fields and refuse UNREGENERABLE output.
Scheduling overlays make ownership especially subtle. On the inspected forms,
yield, group/batch state, and operand reuse participate in joint issue codes;
operand extensions can overlap the nominal control window. PM is another
control field to transport, separate from the ordinary instruction predicate.
An edited-emission path once changed PM3 to PMN; another delay edit advanced W11
to an absent W12 code. Neither is a harmless scheduling hint. The same raw code can
mean different things on different operand forms. set_sched is a low-level
mutation helper, not a complete form-specific legality checker.
Landmarks: lib/pepesilvia/emit.cpp, SassLower.cpp, and the
scheduling chapter.
Keep ownership until the machine is finished
A value can be dead in SSA while an asynchronous instruction still reads its registers. A memory destination can have been issued without being visible to its consumer. Releasing either resource early can corrupt a later operation.
The contract: allocation and scheduling must preserve physical RAW, WAR, and WAW dependencies, tuple constraints, outstanding register holds, and operation-specific completion. Fixed-latency readiness, scoreboard posts/waits, and HGMMA/TMA protocols are distinct obligations.
The attention work also exposed separate register-budget and ABI obligations.
A retained-source candidate disassembled and fit its role limit, yet faulted at
scalar FSEL R158. Missing N192 matrix-footprint seeding and an intermediate
allocation mode had bypassed its immutable source budget. Encodable register
numbers and role limits could not authorize that larger physical footprint.
Complete matrix spans, source budgets where retained, and role limits must all
be checked.
R1 must remain reserved and initialized for all 512 threads, including a program with a zero-sized stack frame; a zero frame does not remove the machine ABI. These are required checks, not a claim that R1 caused earlier unresolved instrumentation failures.
The scheduling investigation found numerical failures after model acceptance: an empty scoreboard and accumulated low-delay codes were insufficient evidence of readiness. The experimental Hopper scalar model therefore admits a bounded subset. Unknown contexts retain their controls or refuse the edit. A recognized commit mnemonic does not prove asynchronous visibility or freedom from deadlock.
Landmarks: the shared PSIR physical model, SassPhysicalLiveness.h,
allocation, and
scheduling.
Prove membership, not just proximity
A read can lie inside a generous bounding range while naming a cell that no producer wrote. A complete write footprint can also be paired with an incomplete or escaping read set. These are reasons to reject a rewrite even when address expressions look similar.
The contract: TMA-related replacement requires a successful layout audit, nonempty complete candidate sets, and strictly covered reads. Truncated searches are refused. Frame identity, signed shifts, alignment, injectivity, density, and loop-stride assumptions must survive address projection.
STRICT, SLACK, and CLAMP are separate grades. Slack or clamp acceptance in
an address diagnostic does not establish strict coverage. A successful write-only
check does not authorize the full rewrite. Sibling footprints must be explicit
inputs to a later coverage check.
The reusable checker enumerates a fixed 128-thread domain. That domain and the symbolic resolver’s supported semantics are applicability assumptions. The result cannot be generalized to a different launch without establishing them.
Descriptor fields, shared-memory frames, swizzle/address formulas, barrier generations, and GMMA drain must also agree with the finished emitted program. Footprint coverage alone cannot establish that physical protocol.
Landmarks: contracts/footprint.cpp, contracts/tma.cpp,
contracts/tma_address.cpp, and docs/contracts/tma.md.
Publish one consistent program image
Deleting or inserting a word changes coordinates used by branches, schedules, symbols, relocations, and NVIDIA metadata. Chained passes also need to distinguish an instruction’s current location from its original provenance.
The contract: each stage finishes its current layout before the next stage. An earlier resize path skipped
EIATTR_ANNOTATIONS, leaving stale instruction offsets.
Origin maps identify retained, deleted, cloned, and inserted instructions; pinned
or relocated words obey stricter rules. Fixups apply exactly once. Final resolved
direct branch targets come from MLIR control-flow edges, rather than stale
immediates. Text and metadata publish together.
Prepare a full replacement before mutating the accepted program. A failed candidate must leave the original input intact; an invalid partial image must never become the successful output. Reusing stale liveness, symbolic projections, or schedule evidence after mutation violates that same boundary.
Landmarks: sass_code_edit, SassPasses.cpp, SassLower.h, and
docs/development/instruction-layout.md.
Bind recovered computation to its host contract
Source recovery must account for the selected computation through actual instruction witnesses. A changed or unexplained source operation is a refusal, not permission to substitute a familiar-looking kernel.
The contract: the rebuilt device program and host adapter must agree on parameter layout, grid, block size, shared memory, descriptors, and any scheduler state or reset protocol. Publication binds the sidecar to the exact image and source bytes; changing either invalidates that binding. A cubin is only one part of that artifact. For persistent causal launches, the scheduler semaphore reset belongs on the same stream before each launch, including graph capture.
The attention reconstruction uses a typed launch sidecar and a supported adapter for its fresh 512-thread program. Its numerical policy is scoped to two admitted FP16 source programs and the tested inputs. Finite extreme-input counterexamples prevent extending the observed acceptance to all finite inputs. Causal retile also needs a fresh mask argument: moving from M128 to M192 can expose rows that the old tile never visited. One counterexample produced 63.5 where the expected value was zero when those newly exposed rows were left unmasked.
Fusion has a related boundary: matching symbolic address geometry cannot prove that runtime pointers are equal or that launch domains correspond. Removing a kernel boundary also requires a replacement for its visibility and ordering. The recompute geometry diagnostic explicitly does not authorize executable fusion.
Landmarks: FlashAttention reconstruction,
Fusion & CUDA Graphs, and docs/contracts/recompute.md.
Say exactly what a proof establishes
The Isabelle SassContracts session proves properties of executable models for
footprint ownership and coverage, swizzle formulas, and recompute geometry. For
example, its footprint model separates strict membership from slack bounds, and
its swizzle model proves involution and bijection for the modeled XOR formulas.
Execution is an independent obligation too. Attention candidates have produced thousands of wrong outputs while memcheck and synccheck reported no errors. Clean sanitizers establish their checked properties, not numerical correctness; static schedule completion does not establish hardware completion.
The C++ implementations remain a trusted transcription. The proofs do not establish correctness of lifting, symbolic resolution, hardware correspondence, asynchronous visibility, barrier progress, numerical equivalence, or the complete compiler. A separate manual allocation/ABI model proves bounds, injectivity, and R1 exclusion; it does not prove the CUDA ABI or refine GPU execution. Recompute geometry is a structural diagnostic, with separate runtime binding and arithmetic assumptions.
Reusable checkers take explicit data and return evidence or a refusal. They do not edit IR, publish cubins, or launch GPU work. The pass discovers a candidate; the checker evaluates a stated predicate; the pass decides whether that evidence satisfies its complete rewrite contract.
Continue with the FMA walkthrough.
Source details live in docs/contracts/README.md and docs/contracts/proofs.md.