# Unlambda ATS runtime specification Supplied design notes. These describe intended behavior and proof obligations; they do not claim that the current starter implements or verifies them. The `ats/heap.sats` and `ats/state.sats` files now contain compiler-validated typed interfaces derived from the supplied sketches. Original shorthand files are preserved in `docs/source-sketches/`. No ATS runtime implementation exists yet. [Validation evidence](../docs/verification/ats-spark-af40c4e.md) defines the checked scope. ## Language semantics — Unlambda 2.0.0 Dialect: 2.0.0 GPL2+ from madore.org (as specified by the supplied notes). Syntax: application, primitives `s k i v c d e r @ | .x ?x`. Evaluation is strict except for `d`: `d x => Delayed(x)` without evaluating `x`; `Delayed(x) y => Eval(x)` applied to `y`. Reductions: - `i x => x` - `k x => K1(x)`; `K1(x) y => x` - `s x => S1`; `s x y => S2`; `s x y z => x z y z` - `v x => v` - `.c x => print c, return x`; `r => newline` - `e x => halt` - `c x => capture K as Cont(K), eval x, apply x to Cont` - `Cont(k) y => K=k, result y` - `@ x => read byte, cur_char set, x i if byte else x v` - `?c x => if cur_char==c then x i else x v` - `| x => if cur_char Some(b) then x .b else x v` Observables: output `O` is ordered; input cursor `I` is monotonic. ## Abstract machine `Sigma=` - `C=Ctrl_Term|Ctrl_Value` - `K=list Frame`: `F_EvalArg(arg_term)`, `F_ApplyFun(fun_ref)` - `H=slot-map NodeRef {slot,gen}` - `I={buf,cursor,cur_char}` - `O=vec OutChar` - `F=fuel` - `Q=Running|Halted|Failed|OutOfFuel|OutOfMemory` Step: at most one transition, consumes one fuel. If `F==0`, set `OutOfFuel`. Apply logic handles `d` specially in `EvalArg`: if `fun==D`, produce `Delayed(arg_term)`; otherwise evaluate strictly. Capture the continuation on `c`; restore it on `Cont` application. ## Memory model Slot-map: slots contain generation plus state `Free|Occupied(Node)`; maintain a free list, capacity, and live count. `NodeRef` contains slot and generation. Allocation pops the free list and checks generation. Lookup checks `gen==slot.gen` and `Occupied`, otherwise returns `StaleRef`. Update performs the same checks. Free increments generation. - H1: stored references valid at store time. - H2: free list exact. - H3: live count equals occupied count. - H4: generation monotonic. - H5: no dereference without lookup. Capacity is fixed initially; `OutOfMemory` is explicit and leaves the heap valid. Future GC roots: `C`, `K`, and continuation nodes. ## Invariants - I1: stack references valid. - I2: control valid. - I3: heap satisfies H1–H5. - I4: fuel decreases monotonically by one per transition. - I5: output extends monotonically. - I6: input cursor monotonic. - I7: no hidden state. - I8: status consistent. - R1: `OutOfFuel != Halted`. - R2: `OutOfMemory != Failed`. - R3: `StaleRef` never dereferenced. Intended ATS enforcement: abstract `term_ref` constructible only via parser, abstract `NodeRef`, typed stack, abstract heap. Runtime assertions: lookup before use, depth limit, spans. Future proofs: `s,k,i` match SKI; `d` delays side effects; `c` captures/restores; I/O preserves order. ## Gates - A: heap safety. - B: core machine `s,k,i,v,d,.,r`. - C: all primitives. - D: differential testing. - E: garbage collection. ## Source materials - [Architecture HTML](../docs/unlambda_x5f_ats_x5f_runtime_x5f_architecture.html) - [Heap interface sketch](../ats/heap.sats) - [State interface sketch](../ats/state.sats) The supplied syntax sentence omits its application symbol, and the newline rule does not specify an argument or return value. These details remain to be resolved against the dialect before implementing the evaluator.