Architecture & semantics

This section is the specification side of VeriTile: how the codebase is laid out, which Triton features the DSL admits, and what semantic models the proofs commit to.

In this section

• Code organization — three layers, what lives where, and the typical change shape when you add an operator, a bridge lemma, or a new kernel transcription.

• Triton subset — the Triton-like surface syntax that’s actually embedded, with the language features that are modelled vs. deliberately out-of-scope.

• Erase + dtype — how typed Op terms project through toAlgorithm? to a mathematical (ℝ / ℤ) channel for algorithmic proofs.

• GPU memory model — what the kernel semantics assume about regions, pointers, and reads/writes.

• Concurrency semantics — the serialized projection model, and what’s deliberately not claimed.

• Memory safety — the safety side of tl.load / tl.store, masks, and bounds.

• Semantic caveats — model assumptions to check when interpreting a theorem.