Memory Safety & PAL

Toka achieves rigorous, compile-time memory safety without the heavy runtime overhead of a Garbage Collector, and without requiring complex, verbose lifetime annotations.

This is accomplished by the compiler's Pointer Analysis Layer (PAL) Checker, which acts as a static verification engine inspecting the usage of Hat pointer typologies and access permission modifiers.

How the PAL Checker Works

The PAL Checker performs static compile-time flow analysis to track the Permission View and Active Scope (Region) of every resource in your codebase.

By requiring explicit pointer specifiers (Hats like ^, ~, &) and mutation intent markers (like # on declarations and receiver method call sites), the compiler gains enough semantic information to perform rigorous safety checking automatically.

It guarantees four core pillars of memory safety at compile time:

1. No Use After Move (Unique Pointers ^)

A unique pointer ^ represents exclusive heap ownership. When it is assigned to another handle, the original handle is marked as "moved-from." The PAL Checker statically blocks any subsequent read or write to the original variable:

fn no_use_after_move_example() {
    auto ^p = new i32(42)
    auto ^q = ^p
    println("q: {}", q)
}

2. No Dangling References (Borrow Pointers &)

A borrow pointer & must never outlive its referent. The PAL Checker tracks the lifetime bounds of the underlying Soul and rejects compilation if a borrow is returned or held beyond the soul's deallocation scope.

3. No Double Free

For owned resources (^ unique pointers or the last ~ shared pointer), the compiler injects a single, deterministic destruction call when the handle exits its scope. Handlers that have been moved or ceded are bypassed, preventing double frees statically.

4. No Data Races / Aliasing Violations

To prevent data races and modification conflicts, Toka enforces the fundamental aliasing rule: you may have either one active mutable borrow OR multiple read-only borrows, but never both simultaneously.

Because Toka requires mutating method calls to explicitly tag their receiver (e.g. obj#.mutate()), the PAL Checker can trivially and securely verify exclusive mutable access at every method call boundary.

Zero-Copy Argument Safety

Toka's function argument passing utilizes the zero-copy implicit reference capture mechanism. When passing arguments to a function, the PAL Checker automatically captures variables by reference under the hood with zero copying.

Because parameters are immutable inside the function by default, the caller's argument remains perfectly safe from modification:

fn show(x: i32) {
    println("x: {}", x)
}

fn borrowing_safe_example() {
    auto val = 10
    show(val)
    println("val: {}", val)
}

To allow a function to modify a parameter, the parameter must be declared mutable (#) in the function signature, and the PAL Checker will then enforce exclusive borrowing at the call site.

PAL Static Assurances at a Glance

The PAL Checker statically analyzes and verifies memory safety during compilation:

By shifting the verification of memory safety to the Pointer Analysis Layer (PAL), Toka allows developers to write safe, high-performance code without the need for manual lifetime annotations.