Secrecy

A program can give away a password it never prints. Writing ^ in front of a type marks a value as secret, and the compiler then refuses to build code that would leak it - and keeps refusing all the way through optimization.

What this is for

Say you check a password by comparing it one character at a time, and stop at the first character that does not match. That is the obvious way to write it, and it is correct - it never prints the password, never logs it, and returns nothing but yes or no.

It still gives the password away. An attacker who can time the check learns something from every attempt: a guess starting with the right character takes a hair longer to reject than one starting with the wrong character, because the comparison got one step further before giving up. Guess the first character - only one of them is measurably slower. Keep it, and guess the second. A password that would take longer than the universe to brute-force all at once falls in a few thousand tries, one character at a time.

Timing is not the only such channel. Three things about a running program are observable without reading its memory:

• Which way it branched. Taking one path rather than another takes a different amount of time, and leaves different traces in the processor.
• Which memory it touched. Reading table[secret] pulls exactly that entry into the cache. An attacker sharing the machine can often work out which one.
• How long an instruction took. Some instructions - division especially - finish faster or slower depending on the values fed to them.

The standard defence is to write the code so none of those depend on the secret: compare every character whether or not an earlier one already failed, and combine the results arithmetically instead of branching. This is called constant-time code, and it is notoriously easy to get wrong.

Why the compiler has to be involved

Even when you get it right by hand, the compiler can undo it. An optimizer's whole job is to notice that work is unnecessary and remove it - and branch-free code that carefully does the same work every time looks exactly like work worth eliminating. A shortcut you deliberately avoided writing gets helpfully added back, and nothing warns you. The source is still constant-time; the binary is not.

So the guarantee cannot live in a coding convention or a library. It has to be something the compiler itself knows about and is obliged to preserve. That is what ^ is.

# `^u64` is a secret. the compiler tracks where it flows.
#[oblivious]
fun ct_diff(a: ^u64, b: ^u64) ^u64 {
    ret a ^ b;                 # one xor, always the same work
}

fun verify(given: ^u64, secret: ^u64) bool {
    if (given == secret) { ret true; }   # refused - see below
    ret (ct_diff(given, secret):^) == 0;
}

That branch does not compile:

error: secret value used as a branch condition
  --> ./src/main.mach:16:5
   |
16 |     if (given == secret) { ret true; }
   |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   |
   = note: a secret may not steer control flow; branching on it leaks
     through timing. compute branch-free, or `:^` to a public value when
     disclosure is intended

Three things are worth drawing out of that. The mistake is caught when you compile, not by an audit or a timing measurement after the fact. Secrecy is part of the type, so it travels with the value through every function it is passed to - you cannot lose track of which variable holds the sensitive one. And disclosure is possible but never accidental: :^ is the one way to turn a secret back into an ordinary value, so every deliberate release is a visible mark in the source that a reviewer can search for.

The rest of this page is the precise version of all that.

The secrecy lattice

There are two secrecy levels in a two-point lattice: public is the bottom, secret the top. ^ lifts a type to secret and binds to the type immediately to its right, so it nests with * and [N] in any order: ^u32, *^u8, ^*u8, [N]^u8, ^MyRec. Doubling collapses: ^^T is ^T.

A public value coerces up to secret wherever a secret is expected, with no syntax. The reverse never happens implicitly.

fun up(p: u32) ^u32 { ret p; }      # public u32 flows into a secret slot

A literal is public by construction and stays public through that coercion: its value sits in the instruction stream, so classifying it as secret would protect nothing. That does not weaken the join below - a value computed with a secret is secret however its other operand is spelled - so v << 3 on a secret v still yields a secret, while the constant 3 is not mistaken for a secret shift count.

Join

Any operation with a secret operand yields a secret result. Taint joins across arithmetic, bitwise, shift, and comparison operators, and through a value read out of a secret container.

fun mix(a: ^u32, b: u32) ^u32 { ret a + b; }    # ^u32 + u32 -> ^u32

rec Key { d: ^[32]u8; }
fun first(k: Key) ^u8 { ret k.d[0]; }            # element of a secret array is ^u8

Taking the address of a ^T value with ? gives the public pointer *^T - the address is public, the pointee secret - and dereferencing it with @ recovers the secret ^T.

Gates

A secret may not reach a position the leakage model observes. Each is a compile error decided by operand type:

• a secret branch or loop condition (if, for)
• a secret left operand of a short-circuiting && / || - it is the branch the operator keys on; a secret right operand only taints the result
• a secret memory index (table[i] with i secret)
• a secret memory address - an access through a secret pointer, whether by @p, p[i], or the auto-deref in p.x
• a secret operand of the always-variable-latency / or %

fun leak(a: ^u32, t: *u8, p: ^*u8) u8 {
    if (a) { ret 1; }       # error: secret value used as a branch condition
    ret t[a];               # error: secret value used as a memory index
    ret @p;                 # error: secret value used as a memory address
}

The index and the address are the two halves of one effective address, so both are gated. Only a secret pointer is an address: a ^[N]T or ^Rec is a secret value living at a public address, and a *^T is a public address to secret storage.

Three more gates decide against the target's constant-time capabilities rather than the source alone, so they are reported at lowering: a secret operand of a floating-point operation (always variable-latency, gated on every target); a secret operand of an integer multiply on a target without a trusted data-independent-timing mode, conservatively every ISA today; and a secret variable shift count on a target without a barrel shifter. A secret passed to a variadic pack is also rejected, including one wrapped inside an aggregate.

Asking about secrecy at comptime

$is_secret(T) folds true when T is ^-qualified at the outermost level. It is a type predicate like $is_record / $is_union / $is_pointer: comptime-only, valid as a $if / $or gate condition, and answered per instantiation inside a generic. The full reference is in Intrinsics.

It exists because secrecy was otherwise invisible to a library. Every other predicate asks about the shape under the ^ and so answers false for every secret, which makes $is_record(^u64) and $is_record(u64) the same answer - a reflection walk could only ever meet a secret field as a fallthrough it had to refuse. $is_secret is the positive question, and it is what lets a derive decide rather than refuse: a formatter redacts a secret field, a hash refuses one (a data-dependent fold is a leak in the shape of a digest), and an equality picks the constant-time comparison instead of the early-out whose timing is the secret.

rec Session { id: u64; key: ^[32]u8; }

$each f in $fields(Session) {
    $if ($is_secret(f.type)) { }            # redact: no read of `key` is emitted
    $or { render(s.[f]); }
}

Outermost only, the same line the rest of the family draws. ^*u8 is secret - the pointer is the secret, which is the shape the welded-storage rules exist for. *^u8 is not: it is a public address to secret storage, and $is_secret($pointee_of(f.type)) asks about the pointee. [N]^u8 is not, and neither is a record with a secret field - the field is, and that is where a walk meets the question.

There is deliberately no transitive "contains a secret anywhere" query: the per-field question is the one a walk actually has, and answering the transitive one in its place would make the common case wrong.

Downgrade with :^

:^ is the only way to remove ^. It produces a new public value and never reinterprets storage in place.

fun publish(a: ^u32) u32 { ret a:^; }       # bare strip
fun publish2(a: ^u32) u32 { ret a:^u32; }   # explicit target names the public type

:^ peels exactly the outer qualifier, so it can never launder a welded pointee - *^T stays *^T. :: and :~ may neither add nor drop ^.

Welded-storage pointers

Secrecy is fixed at declaration and is non-launderable, which makes the public/secret aliasing leak unconstructable with no alias analysis at all:

• a ^T is stored only through a *^T, never a *T
• a secret-welded pointer cannot be erased to the untyped ptr
• a uni's overlapping variants must agree on secrecy

fun erase(p: *^u8) ptr { ret p; }     # error: cannot erase a secret pointer to ptr
uni Bad { a: ^u32; b: u32; }          # error: variants disagree on secrecy

The union rule is a property of the union type, not of the syntax that declared it, so it holds for an inline uni { ... } and at every instance of a generic union. At the declaration a variant typed by a generic parameter says nothing about secrecy, so the check happens where each instance is formed.

uni U[T] { a: T; b: u32; }
rec Box[T] { u: U[T]; }

var s: U[^u32];                       # error: this instantiation makes the variants disagree
var b: Box[^u32];                     # same error: the instance need not be spelled
var p: U[u32];                        # fine, and so is an all-secret instantiation

The check is deep and fails closed: a secret nested anywhere inside an aggregate counts as secret at these boundaries, and a placement the checker cannot prove severs no weld is rejected rather than allowed. Two aggregates are compared by byte extent, not by field ordinal - matching ^ placement in the type graph does not put two fields on the same bytes, so each paired field must also agree in size and alignment.

#[oblivious] - the codegen contract

The flow typing constrains the source; #[oblivious] carries the obligation through codegen. Inside a function carrying it, the backend must not introduce a secret-dependent branch or select a variable-latency instruction on a secret operand.

#[oblivious]
fun ct_select(mask: ^u32, a: ^u32, b: ^u32) ^u32 { ret (a & mask) | (b & ~mask); }

A function instance that computes on a secret must carry it; one that only moves, stores, or declassifies secrets is transparent and stays annotation-free. The check runs per monomorphized instance.

A secret-taint bit is threaded from sema's flow typing through IR and MIR to the emitted instruction stream, preserved across every value replacement, inline clone, instruction selection, and register-allocator copy. The one place taint stops is the declassify barrier a :^ cast lowers to. Secret-free code carries no taint and compiles byte-identically. A translation validator then re-derives the taint over the lowered MIR as a monotone dataflow fixpoint and independently re-checks the leakage conditions - a backstop behind the compile-time gates, not a replacement for them.

Inline assembly inside an oblivious function

Inline asm inside such a function is validated, not rejected. The block is parsed into instructions and walked for the same three leaks the compiler checks everywhere else. Taint enters through the block's {name} bindings, whose secrecy is stamped from the local's declared type. What the walk cannot model, it refuses:

That last row is a per-target asymmetry worth stating precisely. A branch whose condition is a register operand is visible to the walk and is checked: aarch64's cbz / cbnz, and every riscv64 branch, which compares two registers - RISC-V has no flags register at all. A branch whose condition rides the flags register cannot be checked, because a cmp of a secret before it would be invisible, so those are refused.

#[oblivious] remains a per-function contract. A call out to a non-oblivious function is not validated - that is the boundary the decorator draws, not a hole in it.

The zeroizing-write guarantee

Wiping a secret is only useful if the wipe survives to run. That guarantee exists, but it is not provided by #[oblivious], and it is scoped more broadly than the decorator is. A store into secret storage is tainted at lowering, keyed on the storage rather than on any decorator:

# no decorator: the wipe is protected anyway
fun clear(p: *^u8, n: usize) {
    var i: usize = 0;
    for (i < n) { p[i] = 0; i = i + 1; }
}

What it covers. Memory reached through a pointer that escapes the function - the shape a zeroize helper has. Such a store cannot be promoted out of memory, and the taint is present for any future pass to read.

What it does not cover. A value the compiler keeps in a register. Writing to a promoted local is not a memory write, so wiping one is not preserved:

var x: ^u8 = k;
x = 0;          # NOT guaranteed: `x` may never have been in memory

Adding #[oblivious] does not change this. To wipe reliably, write through a pointer whose target is memory the compiler cannot promote away.

Trusted base

The only secret-to-public crossings are the explicit :^ cast and inline asm blocks. Everything else is enforced. A proof is always relative to a leakage model, and its fidelity to real silicon is empirical.

The contract is only offered where mach emits the instructions that execute. A target whose back half hands a module to a downstream compiler instead - the SPIR-V backend - rejects #[oblivious]: neither that translation nor the device's timing behaviour is covered by the leakage model. Compile constant-time code for a machine target, and pass such a target only public data.

Assurance

What holds today: the type system checks that the source respects the leakage model, #[oblivious] carries the obligation through codegen, and the translation validator independently re-checks the lowered MIR. A dudect-style timing harness measures a branchless constant-time reference against a deliberately-leaky control and flags the leak with Welch's t-test.

The leakage model has three channels, and the harness does not cover them uniformly:

The two harness modes need opposite sampling and neither substitutes for the other. Latency mode times a large batch of calls per sample, which is what lifts a running-time difference above clock resolution - and that same batching hides an address-trace leak, since every call in a batch is handed the same input and the single cache miss carrying the signal is averaged away. Two consequences worth stating plainly:

• A clean latency-mode number for a table lookup is not evidence of address-trace safety. It is the wrong instrument for that channel.
• An address-trace leak is only measurable when the table exceeds the last-level cache. A cache-resident table leaks its index just as truly and no timing harness will see it. For small tables the property rests entirely on the secret-index gate and on reading the emitted code.

The known open holes:

• $fields reflection projection inside a generic erases a secret field's secrecy, which discloses the secret. Proven, security-blocking.
• The validator over-taints a wide secret on a narrow-ALU target, rejecting a public-count shift as a secret memory address. A false positive; it fails safe.
• A member or index access through a ^Rec or ^[N]T - which this page documents as legal - fails at lowering, which does not strip the ^ before resolving the field. A spurious error, not a disclosure.

The validator's scope is the lowered MIR; it trusts instruction selection, width legalization, register allocation, and encoding to be timing-preserving. Validation of the emitted machine code is future work.