Solnix Examples

These examples demonstrate how Solnix expresses verifier-safe kernel programs using explicit maps, guards, and memory classes. All examples compile to eBPF object files using the Solnix compiler.

Example 1: Hello Verifier

A minimal tracepoint program that increments a counter safely using a guarded map lookup. This example demonstrates pointer safety and verifier-aware control flow.

map counter {
    type: .array;
    key: u32;
    value: u64;
    max: 1;
}

unit hello_verifier {
    section: "tracepoint/syscalls/sys_enter_execve";
    license: "GPL";

    imm k0 = 0;
    heap p = counter.lookup(k0);

    if guard(p != null) {
        *p = *p + 1;
    }

    return 0;
}

Compile

solnixc compile hello_verifier.snx -o hello_verifier.o

Example 2: Conditional Map Write

Demonstrates verifier-proof conditional execution using guard. The compiler guarantees that the condition holds within the guarded block.

map results {
    type: .array;
    key: u32;
    value: u64;
    max: 8;
}

unit conditional_write {
    section: "tracepoint/syscalls/sys_enter_execve";
    license: "GPL";

    reg a = 10;
    reg b = 20;

    if guard(a < b) {
        imm k0 = 0;
        heap p0 = results.lookup(k0);
        *p0 = 1;
    }

    return 0;
}

Compile

solnixc compile conditional_write.snx -o conditional_write.o

Example 3: Safe Map Indexing

Shows how Solnix enforces safe map access by requiring explicit guards before dereferencing heap pointers.

map data {
    type: .array;
    key: u32;
    value: u64;
    max: 4;
}

unit safe_index {
    section: "tracepoint/syscalls/sys_enter_execve";
    license: "GPL";

    imm idx = 2;
    heap p = data.lookup(idx);

    if guard(p != null) {
        *p = 42;
    }

    return 0;
}

Compile

solnixc compile safe_index.snx -o safe_index.o

Example 4: Invalid Program (Rejected)

This example intentionally violates Solnix safety rules. The compiler rejects it because the heap pointer is dereferenced without a guard.

map bad {
    type: .array;
    key: u32;
    value: u64;
    max: 1;
}

unit invalid_example {
    section: "tracepoint/syscalls/sys_enter_execve";
    license: "GPL";

    imm k0 = 0;
    heap p = bad.lookup(k0);

    *p = 1;   // ERROR: unguarded heap dereference

    return 0;
}

Compile (fails)

solnixc compile invalid_example.snx -o invalid_example.o

Compilation fails with a verifier-safety error.