Skip to content

deterministic-lua.md

Latest commit

 

History

History
111 lines (76 loc) · 5.04 KB

deterministic-lua.md

File metadata and controls

111 lines (76 loc) · 5.04 KB
title Deterministic Lua (EchoLua Profile)

Deterministic Lua (EchoLua Profile)

EchoLua defines a deterministic execution profile for Lua used in GATOS policies and folds. It locks down semantics so the same inputs yield the same bytes across platforms.

This document is normative where called out by SPEC and TECH-SPEC; elsewhere it is strongly RECOMMENDED.

Goals

  • Pure, total, side-effect-free fold execution.
  • Cross-platform bit-for-bit deterministic results.
  • Portable compiled form for long-term verification.

Compilation Pipeline

Lua source  ──parse/normalize──► AST ──lower──► ELC (Echo Lua IR; deterministic IR)
                                         │
                                         └─► DAG-CBOR bytes  (CBOR-encoded DAG; fold_root = sha256(ELC_bytes))
  • Normalize: remove syntactic sugar, canonical constant folding, resolve upvalues.
  • Lower: emit a small, explicitly typed IR + minimal VM op set.
  • Serialize: ELC encoded as DAG-CBOR; fold_root = sha256(ELC_bytes).
  • Prohibition: Stock Lua bytecode (luac) is NOT portable and MUST NOT be used on disk or for signing.

Deterministic Runtime Profile

Area Default Lua EchoLua profile (deterministic)
Time/OS os.clock, os.time, io.* Removed (forbidden)
Random math.random (MT) rng(seed) intrinsic only; no global state
Numbers Host IEEE-754 Fixed-point Q32.32 with ties-to-even; canonical NaN handling (N/A)
Iteration pairs() unspecified dpairs(t) sorts keys; ipairs allowed
Table hashing Randomized seed Fixed seed; do not rely on hash order
Coroutines yield anywhere Disallowed in folds/policy eval
Metamethods __gc etc. __gc and __pairs forbidden; compile-time error
FFI/dlopen via add-ons Forbidden
Math lib Host-lib variance Deterministic lib; exp/log/sin/cos pinned or disallowed

Additional invariants:

  • Canonical JSON: UTF-8 NFC; lexicographic key sort; fixed number encoding (no -0, no trailing zeros).
  • Resource caps: fuel/step counters (MUST terminate within limits).

Standard Library (Deterministic Subset)

  • table: dkeys, dvalues, dsort, dpairs(t) (sorted iteration).
  • json: encode_canonical, decode_strict.
  • math: +, −, ×, ÷ in Q32.32 (division rounds toward zero). Transcendentals (sin/exp/log/…) are not permitted in v1 folds; perform in jobs (PoE) instead.
  • set, counter: deterministic CRDT (Conflict-free Replicated Data Type)-style helpers for folds.
  • No debug, package, io, os modules.

RNG

  • No ambient RNG. Provide rng(seed_bytes) which expands a user-supplied seed into a deterministic stream.
  • Normative algorithm: pcg32@1. Implementations MUST record RNG id and version via the Fold-Engine string and SHOULD include Fold-RNG trailer when RNG is used.
  • Canonical seed helper: seed64 = trunc64(blake3(inputs_root || policy_root || fold_root)).
  • Use discouraged in folds; if used, caller MUST pass explicit seed material.

Linter / Compiler Rules

Hard-fail on:

  • use of pairs, coroutine, __gc, __pairs, math.random, os.*, io.*, debug.*, package.*.
  • non-canonical numeric literals; non-deterministic table traversal.

Proof / Trailer Integration

  • State checkpoints MUST include Fold-Root: sha256:<hex> trailers.
  • RECOMMENDED trailers: Fold-Math: fixed-q32.32@<libver>, Fold-RNG: <alg>@<ver>.
  • PoF (Proof of Fold) envelopes SHOULD include fold_root and verifiers MUST recompute from ELC bytes when present.

Open Implementation Notes

  • Transcendentals: when required, ship a pinned deterministic math library and record its version in Fold-Engine.
  • Performance: heavy data operators should be implemented as deterministic native intrinsics, invoked from EchoLua.