Formal Memory & Execution Subsystems

Deterministic Memory,
Formal Typing & Dual-Engine AVM

The mathematical design behind Aether's ability to unify bare-metal microcontrollers, cooperative fiber concurrency, and GPU tensor compute without garbage collection pauses.

Deterministic Memory

1. Perceus Reference Counting & Destructive Reuse

Traditional languages force an unacceptable trade-off: non-deterministic stop-the-world GC pauses (Go, Java, Python), or tedious lifetime and borrow-checker annotations that complicate systems modeling (Rust, C++). Aether implements Perceus Reference Counting: an exact static analysis that transforms functional updates into in-place destructive mutation whenever a reference count is uniquely 1 (\(rc = 1\)).

matrix_transform.ae (Source)

Functional Invariant

# Pure functional transform of a 4096x4096 matrix buffer
fn normalize_weights(w: Tensor) -> Tensor:
    # Syntactically creates a transformed tensor
    return w.map(fn(x): (x - 0.5) * 2.0)

fn main():
    mut weights := Tensor::randn([4096, 4096])
    for epoch in 0 .. 1000:
        # Local's last use moves memory; rc stays 1
        weights = normalize_weights(weights)

aether_perceus_lowered.c

Zero Malloc Reuse

// Zero heap malloc! Buffer reused in-place if rc == 1
if (ae_is_unique(w)) {
    // In-place destructive reuse: overwrites in CPU cache
    float* raw = (float*)w->data;
    for (size_t i = 0; i < 16777216; ++i) {
        raw[i] = (raw[i] - 0.5f) * 2.0f;
    }
    return w; // Reuses same pointer
} else {
    return ae_tensor_clone_map(w);
}

Mathematical Guarantee: Strictly \(O(1)\) deterministic deallocation with 0 cycle leaks (`-DAE_TRACK_LIVE` tested).

Type Theory

2. Formal Typing Inference Rules

Aether's typing judgments incorporate hardware capability effects directly into the inference relation \(\Gamma \vdash e : \tau \ \& \ \Phi\), where \(\Phi\) denotes the hardware constraint effect.

Rule [T-Kernel]: Bare-Metal Allocation Invariant Z3 SMT Proved

\(\Gamma \vdash e : \tau \ \& \ \Phi \quad \quad \text{Alloc}(\Phi) = \emptyset \quad \quad \forall i \in \text{Indices}(e), \ \text{Z3\_Prove}(\Gamma \models 0 \le i < \text{len}(arr))\)

\(\Gamma \vdash \text{@kernel}(e) : \tau \ \& \ \text{Deterministic}(\Phi)\)

Statically proves that no heap allocations (\(\text{Alloc} = \emptyset\)) occur within the marked block. The integrated Z3 solver statically verifies index safety, allowing the compiler to safely omit runtime bounds-checking branches.

Rule [T-MatMul]: Fused Tensor Dimension Contraction GPU Warp Invariant

\(\Gamma \vdash A : \text{Tensor}\langle [M, K], T \rangle \quad \quad \Gamma \vdash B : \text{Tensor}\langle [K, N], T \rangle \quad \quad T \in \{ \text{f16}, \text{bf16}, \text{f32}, \text{dec128} \}\)

\(\Gamma \vdash A \ @ \ B : \text{Tensor}\langle [M, N], T \rangle \ \& \ \text{FusedKernel}(\text{WarpSize}=32)\)

Proves static shape dimension alignment (\(K = K\)) at compile time. When chained with activations (e.g. \((A @ B).\text{relu}()\)), operations are fused into a single GPU register pass without writing intermediate results to VRAM.

Rule [T-Try]: Zero-Cost Algebraic Error Propagation Zero Stack Unwind

\(\Gamma \vdash e : \text{Result}\langle \tau, \epsilon \rangle \quad \quad \Gamma(\text{ret}) = \text{Result}\langle \tau', \epsilon' \rangle \quad \quad \epsilon \subseteq \epsilon'\)

\(\Gamma \vdash e? : \tau \ \& \ \text{Branch}(\epsilon \to \text{EarlyReturn})\)

Lowers early returns to single register test-and-branch instructions. No C++ exception tables (Dwarf CFI) or stack unwinding machinery required.

Execution Engines

3. Dual-Engine Architecture: Native AOT C vs 3-Tier AVM

ENGINE A (DEFAULT) ae run / ae build --native

Deterministic Native AOT C Backend

Lowers Aether AST directly to standard C99/C11 and compiles via bundled Zig CC, Clang, or GCC.

✓ Unboxed Int/Float/Bool/dec128 values
✓ M:N fibers on Chase-Lev work-stealing scheduler
✓ OS-thread `parallel for` with work chunking
✓ Incremental: one cached object per function

ENGINE B (DEV LOOP) ae run --engine vm / ae repl

3-Tier AVM (Aether Virtual Machine)

Tier 0: Register Interpreter — Instant 0ms launch.

Tier 1: Copy-and-Patch JIT — Template machine code.

Tier 2: Machine-Code JIT — Inlines loops into vector pipelines.

Cryptographic Reproducibility

4. 3-Stage Self-Hosting Deterministic Bootstrap

The reference compiler achieves bit-for-bit reproducible self-hosting across 3 stages, eliminating trusting-trust security vectors.

Stage 0

aetherc-boot.py

Pure Python 3.10+ reference lexer, parser, SMT checker, and C generator with zero required external dependencies.

Stage 1

aetherc-stage1

Aether compiler written in pure *.ae, compiled natively via Stage 0. Implements Perceus and SMT solvers.

Stage 2

aetherc-release

Recompiled by Stage 1. Output binary is bit-identical to Stage 3 recompilations (verified via BLAKE3 hash).

Deterministic Memory,Formal Typing & Dual-Engine AVM