Oro Computer logooro
Inside
Silk
Language / Unsafe Boundaries

Unsafe Boundaries

Silk uses unsafe to mark operations whose validity depends on an invariant the compiler cannot prove. An unsafe boundary does not disable the type checker, ownership rules, borrow checking, purity checking, target checks, or ABI validation. It authorizes only the operations listed in this document.

unsafe is a last resort, not a label inferred from an operation merely looking low-level. The language applies this decision order:

  1. If the compiler can validate the invariant statically, the operation is safe.
  2. If a runtime check can trap before an invalid access or call, the checked operation is safe.
  3. Only an operation that must trust an invariant supplied by the programmer requires an unsafe context.

Adding a new primitive, cast, or ABI form does not make it unsafe by default. Its specification must identify the concrete invariant that cannot be checked and why a trapping checked form cannot provide the required semantics before the operation may be added to the gated list below.

Syntax#

An unsafe statement block contains ordinary statements:

unsafe {
  asm "pause";
}

An unsafe expression contains exactly one expression and yields its value:

let callback = unsafe {
  address as raw c_fn (i64, i64) -> i64
};

When the boundary contains one unary or postfix expression, braces are optional:

unsafe operation();
let callback = unsafe address as raw c_fn (i64, i64) -> i64;

The first line is exactly equivalent to unsafe { operation() };. The prefix form owns one complete unary/postfix expression, including its calls, field or index accesses, and cast suffixes. It does not absorb a following binary operator: unsafe operation() + other() authorizes only operation(). Use unsafe (operation() + other()) or unsafe { operation() + other() } when the whole compound expression must share the boundary.

At statement position, punctuation disambiguates the two forms: unsafe { operation(); } is a statement block, while unsafe { operation() }; is an unsafe expression used as an expression statement. An unbraced unsafe operation(); always uses the single-expression form. In value position, such as after =, the expression forms are unambiguous.

Functions may declare an unsafe calling contract:

unsafe fn read_device_register (address: u64) -> u64 {
  return std::runtime::mem::load_u64(address, 0);
}

The body of an unsafe fn is an unsafe context. Calling it from safe code requires an enclosing unsafe expression/block. unsafe is orthogonal to const, pure, task, and async; all existing discipline rules continue to apply.

Callable types retain the effect:

type RawReader = unsafe fn (u64) -> u64;
type ForeignRawReader = unsafe c_fn (u64) -> u64;

A safe callable may be stored where an unsafe callable is expected. An unsafe callable may not be stored in a safe callable type, because doing so would erase the call-site obligation.

Interface methods may use the same effect:

interface RawReadable {
  unsafe fn read_at (address: u64) -> u64;
}

A safe implementation may satisfy an unsafe interface method. An unsafe implementation cannot satisfy a safe interface method, because that would erase the caller's obligation from the interface contract.

Operations That Require an Unsafe Context#

The compiler requires unsafe for:

  • constructing an array/slice or string view from a raw u64/usize address, including ptr as T[], ptr as T[](/silk/docs/len), and ptr as string(len);
  • constructing a c_fn/unsafe c_fn from a raw u64/usize address with as raw;
  • indexing or assigning through a slice whose runtime length is the unknown-length sentinel; safe indexing traps instead of performing an unchecked access, while the same index expression inside unsafe may use that sentinel;
  • the raw memory load/store and pointer-to-string primitives declared as unsafe fn by std::runtime::mem;
  • inline assembly;
  • calling an unsafe fn or unsafe c_fn, directly, through a method, or through a stored callable value.

Each gate corresponds to a concrete unchecked obligation: a raw view needs a valid, suitably aligned allocation with the claimed extent; a raw callback needs an executable address with the claimed ABI and signature; a raw memory primitive needs valid accessible storage; inline assembly may violate machine state invariants; and an unsafe callable documents an obligation its body cannot establish for the caller. The checker must not extend this list by analogy alone.

Raw address-to-reference construction is not implemented. If it is added, it must require an unsafe context under the same rule as other pointer-backed views.

Operations That Remain Safe#

The following do not require unsafe:

  • checked fn (...) -> R to c_fn (...) -> R conversion, which rejects or traps on a nonzero closure environment;
  • storing, returning, passing, or calling a verified function/callback value;
  • scalar as raw bit reinterpretation;
  • extracting a string/reference/slice/array/c_fn address as an inert u64/usize value;
  • layout-proven struct and reference shape casts;
  • calling a safe c_fn, including one produced from a verified non-capturing Silk function.

Worked Example: Checked Silk Callback Conversion#

No unsafe boundary is needed when Silk can validate the conversion. The compiler checks that the signatures match, rejects a directly visible capture, and emits a runtime environment check for an indirect function value:

let add = fn (x: int, y: int) -> x + y;
let callback = add as c_fn (int, int) -> int;
let answer = callback(20, 22);

The conversion either produces a valid environment-free callback or traps before producing one. Adding unsafe here would communicate no caller-owned invariant and is unnecessary.

Worked Example: Dynamic Symbol Lookup#

A dynamic loader returns an untyped address. Only the program and the foreign library's documentation can establish that the address is executable, has the declared signature and calling convention, and remains live while it is used. That assertion belongs at the address-to-callback cast:

import { Library, Symbol, is_supported, open_self } from "std/dylib";

type StrLen = c_fn (u64) -> u64;

fn main () -> int {
  if !is_supported() {
    return 0;
  }

  let library_opt: Library? = open_self().unwrap();
  if library_opt == None {
    return 1;
  }
  let library = library_opt ?? Library.invalid();

  let symbol_opt: Symbol? = library.symbol("strlen").unwrap();
  if symbol_opt == None {
    return 1;
  }
  let symbol = symbol_opt ?? Symbol.invalid();

  let strlen: StrLen = unsafe { symbol.address() as raw StrLen };
  let length = strlen("dynamic" as raw u64);
  if length != 7 {
    return 1;
  }
  return 0;
}

The strlen(...) call is safe after the cast because the narrow unsafe boundary established a safe c_fn value. The Library must remain open until after the call. Closing it earlier, selecting a data symbol, or declaring the wrong parameter/result types would violate the asserted invariant; Silk cannot discover any of those facts from the integer address.

The runnable source is examples/std_dylib_strlen.slk.

Worked Example: Raw Memory Owned by an Allocation#

Raw memory access needs a live allocation, a non-overflowing in-bounds offset, the required alignment, and suitable read/write permission. A helper that cannot establish those facts from its u64 and length arguments exposes an unsafe calling contract:

import { alloc, free, load_u8, store_u8 } from "std/runtime/mem";

unsafe fn checksum_bytes (ptr: u64, len: i64) -> u64 {
  var index: i64 = 0;
  var sum: u64 = 0;
  while index < len {
    sum += load_u8(ptr, index) as u64;
    index += 1;
  }

  return sum;
}

fn main () -> int {
  let ptr = alloc(4);
  if ptr == 0 {
    return 1;
  }

  unsafe {
    store_u8(ptr, 0, 10);
    store_u8(ptr, 1, 20);
    store_u8(ptr, 2, 5);
    store_u8(ptr, 3, 7);
  }

  let sum = unsafe { checksum_bytes(ptr, 4) };
  free(ptr);

  if sum != 42 {
    return 1;
  }
  return 0;
}

Here main owns the allocation, checks allocation failure, uses only offsets 0..3, calls the helper before free, and never publishes the pointer. Those facts justify both narrow boundaries. Moving free(ptr) before the checksum or passing a length greater than four would violate the contract. The runnable source is examples/unsafe_raw_memory_checksum.slk.

Formal Silk Integration#

Unsafe permission and formal proof are independent:

  • the ordinary checker runs first, so a missing boundary reports E2129 before formal verification;
  • unsafe expression and statement wrappers are transparent to the Formal Silk translator and add no path condition, assumption, or axiom;
  • #require, #assure, #assert, loop obligations, and contracted-call preconditions are checked inside unsafe wrappers exactly as outside them;
  • contracts can prove modeled facts such as address != 0 or len > 0, but the current model cannot prove that an integer denotes live readable memory or executable code with a particular C ABI.

For example, a declaration-only platform primitive can expose both a formal condition and a broader unsafe machine contract:

#require address != 0;
#assure result == address;
unsafe fn preserve_registered_address (address: u64) -> u64;

#require address != 0;
#assure result == address;
fn checked_forwarder (address: u64) -> u64 {
  return unsafe preserve_registered_address(address);
}

The verifier proves that checked_forwarder supplies the declared nonzero precondition and may use the callee's postcondition. The unsafe boundary does not prove that the address is registered, mapped, executable, or associated with a particular device. Those machine facts remain part of the documented unsafe contract. Calling the primitive with literal 0 inside an unsafe block passes the unsafe-context check but fails formal call-precondition verification with E3007.

See formal verification for the complete modeled subset.

Encapsulation#

Safe functions may contain a narrow unsafe block after validating the invariants needed by the operation. Callers then rely on the safe function's documented contract rather than repeating unsafe.

For example, a collection implementation may bounds-check an index and use an unsafe raw-memory operation internally. The collection's public checked method can remain safe. A function that cannot establish the necessary invariant must instead be declared unsafe fn and document the caller's obligation.

Diagnostics#

Using a gated operation outside an unsafe context reports E2129. The diagnostic identifies the operation and suggests a narrow unsafe prefix, an unsafe { ... } boundary, or a safe wrapper.

For example:

fn main () -> int {
  let address: u64 = 1;
  let callback = address as raw c_fn (int) -> int;
  return 0;
}

reports:

error[E2129]: unsafe operation requires an unsafe context
  |
  |   let callback = address as raw c_fn (int) -> int;
  |                             ^^^ raw address-to-callback cast
  = help: prefix the operation with `unsafe` or wrap it in `unsafe { ... }` after validating its safety invariants
  = help: or declare the containing function `unsafe fn` when callers must uphold those invariants

The compiler anchors the diagnostic at the gated operation rather than the containing function. CLI, C ABI diagnostic adapters, and LSP diagnostics use the same stable E2129 code and operation-specific detail.

E2128 is distinct: it reports a known capturing fn converted to c_fn. That conversion is invalid rather than an operation an unsafe boundary may authorize, so adding unsafe does not suppress E2128.

Source repository · Edit this page · View Markdown

PreviousComplexity Analysis API

Quick links

Type to search across the site. Use the up and down arrow keys to choose a result, Enter to open it, and Escape to close.