Language Reference

A conservative snapshot of the current implemented/reference-backed Aura language surface.

This page is intentionally conservative. When documentation conflicts with the current compiler, use this precedence:

1. current implementation,
2. sdk/docs/reference.md,
3. focused current verifier/protocol docs,
4. historical roadmap/design/completion documents.

Lexical structure

Indentation is significant. The lexer models structural indentation/newline tokens rather than treating whitespace as presentation only.

cell main():
    val x: u32 = 1
    if x == 1:
        log("one")

Modules

import std::io
import aura::tensor

SDK installs may inject default standard modules based on imports.

Bindings

val answer: u32 = 42
val mut index: u32 = 0
index = index + 1

Cells

cell add(a: u32, b: u32) -> u32:
    a + b

Foreign declarations:

extern cell native_read(fd: u32) -> u32
trusted extern cell audited_clock() -> u32

Trust metadata is not proof of the external implementation.

Current built-in type snapshot

The compact reference currently names:

• u32
• bool
• String
• Unit
• Tensor<Elem, [d0, d1, ...]>
• Model
• Style

This is not a frozen pre-1.0 type-system promise.

Refinements

Range refinement syntax is documented for u32:

val percent: u32[0..100] = 75

Contracts and proof statements

cell inc(x: u32) -> u32:
    requires x < 100
    ensures result == x + 1

    val next = x + 1
    assert next <= 100
    next

assume intentionally adds trusted information to proof reasoning and should be used carefully.

Loops

val mut i: u32 = 0
while i < n invariant i <= n decreases n - i:
    i = i + 1

The verifier guide also documents quantifiers. Repository verification examples note that quantifiers are accepted only under the thorough SMT profile in that path.

Control flow

Current reference includes:

• if
• match
• while

Precise pattern grammar should come from current parser behavior, not old design prose.

Flow operators

left -> right
left ~> right

The compact reference distinguishes synchronous (->) and asynchronous (~>) flow.

Resource moves

For resource-like types such as Tensor, Model and Style, the current reference documents move behavior on identifier binding/assignment. Broader ownership/linear/capability infrastructure exists in the compiler, but the stable language guarantee is not yet frozen.

Async capture safety

Current reference states that async lambdas may not capture mutable outer bindings.

Unsafe and FFI

Untrusted external calls require an explicit unsafe boundary in the current model:

unsafe:
    native_read(fd)

UI syntax

Current reference includes layout: and render: statements used by the evolving Lumina layer.

cell main():
    layout:
        VStack(alignment: "center") {
            render: Text(text: "Aura")
        }

Not a stable promise yet

Do not infer today that Aura provides:

• a complete Rust-equivalent borrow checker,
• a frozen generic/trait model,
• a stable ABI,
• frozen UI DSL semantics,
• universal no-segfault guarantees,
• source compatibility across every future pre-1.0 revision.