Provably Safe Inline Assembly

We have a reflex about inline assembly, and the reflex is that it is automatically unsafe. Drop to the metal and you drop every guarantee at the door. In C you are already in the wild, so it hardly registers. In Rust you wrap it in unsafe and the borrow checker, the bounds checks, the initialization tracking, all of the machinery that made you choose Rust in the first place, politely stops applying inside the block. The instruction runs, the compiler shrugs, and whatever you claimed about alignment or ownership or register width is now a promise between you and the hardware that nobody checks.

This is a reasonable choice for C and Rust. Given what they can express about the machine, refusing to reason about assembly is the only honest move available to them. But the reflex is a failure of imagination dressed up as a law of nature. Nothing about being close to the metal forces you to abandon proof. The metal has rules, the rules are written down, and we just decided not to teach them to the compiler.

Why C and Rust are right to give up

An x86 or ARM instruction has a contract. A vector load reads a span of memory of a particular width, expects a particular alignment, and lands the result in a register of a particular size. That contract is real and precise, and neither C nor Rust has any way to say it. Their type systems can describe a pointer and maybe a length. They cannot express “this address is sixteen-byte aligned and these sixteen bytes are initialized and I uniquely own them right now.” The vocabulary does not exist.

So when one of these languages meets an assembly block, it can pretend to reason about a contract it cannot represent, which is worse than useless, or it can mark the region unsafe, suspend its guarantees, and hand the obligation to the human. Given the tools they have, suspending judgment is the responsible answer. You cannot check what you cannot describe. Marking it unsafe is the language admitting the limit out loud, which is more than C ever did.

The fix is to give the language the vocabulary, rather than to be braver inside the block.

Instructions have contracts, so let them carry contracts

Omega, the language Cathedral is built in, already treats every ordinary operation as a contract. Values carry facts. Operations carry requirements and guarantees, which create obligations the compiler discharges using the facts it has. An assignment, an array index, an arithmetic op: each one is checked against what is known, and code that cannot satisfy its obligations does not compile.

Inline assembly is the same model at a lower altitude. An assembly block is parsed, not treated as an opaque blob of text, and each instruction in the accepted subset has a contract the compiler knows. A memory load emits obligations about initialization, bounds, alignment, provenance, and aliasing. A store emits obligations about mutability, ownership, bounds, alignment, and preserving invariants. A direct jump emits a control-flow obligation. A register clobber tells the compiler which values it just destroyed. Assembly’s contracts are only lower-level and more numerous, not different in kind.

A vector load. To issue it, you have to discharge real obligations:

asm where
    requires src.initialized
    requires src.aligned<16>
    requires src.len >= 16
    requires dst.unique_mut
    requires target_feature<sse2>
    ensures dst[0..16].initialized
{
    // target-specific SIMD load
}

That is a checklist the compiler enforces. You must prove the source bytes are initialized, the source is sixteen-byte aligned, and there are at least sixteen bytes to read so the load fits the register. You must prove you uniquely own the destination so the write aliases nothing, and that the target CPU feature is actually present. If every one of those facts is available from the surrounding code, you may write the instruction and the load is checked, rather than assumed. If even one cannot be proven, the program does not compile. You get the same SIMD load, except its preconditions are now a verified property of the program instead of a hope in a comment.

Control flow gets the same treatment instead of an escape hatch. A jump out of an assembly block cannot invent a hidden branch or loop. It has to land on something the compiler already understands.

asm {
    jmp my_state()
}

That is accepted only when my_state resolves to a real state transition and every obligation that transition normally carries is satisfied: the target is valid, it accepts the current machine invariants, clobbers are declared. The jump is a low-level spelling of a transition the compiler still reasons about. Arbitrary labels and back-edges that map to nothing are rejected, because they would create control flow the proof model cannot see.

When a fact genuinely cannot be proven from Omega code, the answer is an explicit boundary rather than a silent suspension of the rules: a human or a host contract asserts the fact, and that assertion shows up loudly in the build artifact.

unchecked assembly obligations:
  physics.omg:42 requires src.aligned<16>
  crypto.omg:91 boundary target_feature<aes>

Unproven assumptions do not get to be invisible. If you assert something the compiler could not verify, the build names the file, the line, and the obligation. The block is still useful. The trust it rests on is just on the record.

I am not going to pretend this is free

The cost is large. Every instruction the compiler reasons about has to have its contract taught to the compiler, one instruction at a time, per target architecture. There is no trick that does this in bulk. It is a long, grinding catalog of machine semantics, exactly as big as the instruction set you want to support, and it is real engineering work measured in years.

It is also an attack surface. A contract is a model of the hardware, and a wrong model is worse than no model: it lets the compiler bless an instruction that does not actually behave the way the contract claims. Get an alignment rule or a clobber list subtly wrong and you produce confidently-checked code that is nonetheless broken. The contracts have to be right, and being right about every corner of an instruction set is hard.

So I expect this to be gated for a long time. Most libraries will not be allowed to use inline assembly at all until a given instruction’s contract is deemed solid enough to trust, and assembly should be unavailable in a safe build unless every obligation is either discharged or explicitly marked as a boundary. The default should be closed, and instructions should earn their way into the accepted subset slowly.

But the slog and the gating are implementation problems, not a reason to keep believing the reflex. Assembly being unsafe was never a property of the metal. It was a property of languages that had no way to talk about the metal.

The mental model is this: assembly does not get to change reality without telling the compiler what reality changed.