nela-tools

name	nela-tools
description	Tool specifications and interfaces for the NELA language toolchain. Covers surface language (NELA-S) interpreter, type checking, compiler (NELA-S → NELA-C interaction nets), serialization, legacy code migration, and LLM context optimization. Load when implementing any NELA toolchain component.
applyTo	**/*.nela,**/*.nela.json,**/nela/**

NELA Toolchain — Tool Specifications

Architecture note (v0.10): LLMs read and write NELA-S in ML/Haskell-like syntax (.nela files). The interaction net layer (NELA-C) is generated by the compiler. Tools are organised by layer. LLMs directly use Tool 1 and Tool 7. The rest are compiler/runtime internals.

v0.10 addition: nela_compiler.py (Tool 1c) compiles NELA-S to NELA-C — a serialised interaction net graph in .nelac binary format. This is NOT a Von Neumann VM; there is no stack, no registers, no program counter. The bytecode IS the interaction net graph (nodes + ports + root pointer). The current compiler reduces eagerly to normal form before serialising; v0.11 will emit unreduced nets with active pairs and run the SIC reducer on-net.

Mission constraint: The Python harness (examples/wolf/src/wolf_player.py) is I/O-only. All game logic (raycasting, frame assembly, shading, movement, collision, trig) lives in NELA-S. Python provides only: raw keyboard input and print. Zero precomputed data (no trig tables, no constants).

---

Tool 1: nela.surface — NELA-S Interpreter (LLM-facing)

Purpose: Evaluate NELA-S programs (ML/Haskell-like .nela files). Parse with nela_parser.parse_file(path) or nela_parser.parse_program(text), then run with run_program. This is the primary tool an LLM uses to run and verify programs it has written.

Interface

def run_program(prog: dict, fn_name: str, *arg_values) -> Any:
    """
    Execute a NELA-S program.
    prog:       program dict from parse_program() or parse_file()
    fn_name:    name of the entry-point function in prog["defs"]
    arg_values: one value per param in fn_def["params"]
    Returns the Python value computed by the surface interpreter.
    """

def eval_expr(expr: dict, env: dict, defs: dict) -> Any:
    """
    Core expression evaluator (recursive tree-walk).
    expr: Expr dict  {"op": ..., ...fields}
    env:  variable bindings  {name: value}
    defs: all function definitions in scope  {name: def_dict}
    """

Supported Ops (runtime v0.9)

Op	Fields	Semantics
var	n	look up name in env
int	v	integer literal
float	v	float literal (3.14, 0.017453)
char	v	char literal ('A', '0'; Python str of len 1)
bool	v	boolean literal
nil	—	empty list []
cons	head, tail	prepend element to list
match	e, cases	exhaustive pattern match on list
call	fn, a	call named function with arg list
let	x, e, in	local binding
if	cond, then, else_	conditional branch
pair	l, r	construct tuple (a, b)
fst	e	first element of pair
snd	e	second element of pair
head	e	first element of list (unsafe)
tail	e	rest of list (unsafe)
take	n, e	first n elements
drop	n, e	skip first n elements
add/sub/mul/div/mod	l, r	arithmetic (div = integer division, mod = remainder)
neg	e	unary negation (use (-5) paren syntax in source)
eq/lt/le/gt/ge	l, r	comparison
and/or	l, r	boolean logic
not	e	boolean negation
sin/cos/sqrt	e	float math (uses math.sin, math.cos, math.sqrt; argument in radians)
floor/ceil	e	round toward −∞ / +∞; returns Python int
round/abs	e	round to nearest int / absolute value
ord	e	char → int: ord 'A' = 65
chr	e	int → char: chr 65 = 'A'
get	e, n	O(1) list index: get lst n → lst[n] (replaces head (drop n lst))
len	e	list length: len [1,2,3] → 3
array	n, v	create list of length n filled with v: array 3 0 → [0,0,0]
aset	e, n, v	functional update: copy of e with index n set to v
filter	pred, pivot, list	predicate filter with literal comparator
append	l, r	list concatenation
io_key	e	consume token e; call token.read_key(); return (char, token')
io_print	l, r	consume token r; call token.print_frame(l); return token'

Error Conditions

• KeyError: variable not in scope (unbound name in env)
• ValueError("Unknown op: ..."): op string not in the table above
• ValueError("Non-exhaustive match"): no case pattern matched the scrutinee

---

Tool 1b: nela.graph — Net Construction (NELA-C, compiler internal)

Interface

class Net:
    signature: dict[str, int]          # agent_name -> arity
    nodes:     dict[str, Agent]        # node_id -> Agent
    edges:     list[tuple[Port, Port]] # undirected port connections
    types:     dict[Port, str]         # port -> linear type string

class Agent:
    id:        str
    name:      str                     # must be in signature
    ports:     dict[str, Port]         # "principal", "aux0", "aux1", ...

class Port:
    node_id:   str
    port_name: str                     # "principal" | "auxN"

Key Operations

Operation	Signature	Effect
add_agent	(net, name, type_ann?) -> node_id	Add agent node
connect	(net, port_a, port_b) -> net	Connect two ports (raises if either already connected)
find_redexes	(net) -> list[tuple[node_id, node_id]]	Find all active pairs
is_linear	(net) -> bool	Check every port has exactly one connection
interface	(net) -> list[Port]	Return all free (unconnected) ports
tensor	(net_a, net_b) -> net	Disjoint union of two nets
compose	(net_a, out_port, net_b, in_port) -> net	Connect interface ports

Error Conditions

• NonLinearError: Port connected more than once → structural type violation
• UnknownAgentError: Agent name not in signature
• TypeMismatchError: Port types incompatible under linear type system

---

Tool 2: nela.rewrite — Reduction Engine

Purpose: Apply interaction rules to active pairs; drive computation to normal form.

Reduction Strategies

Strategy	Description	Use case
leftmost	Reduce leftmost-outermost redex	Deterministic sequential execution
parallel	Reduce all redexes simultaneously	Maximum parallelism (safe by Thm 1.2)
lazy	Reduce only redexes on spine	Avoid computing unused branches

Interface

def step(net: Net, strategy: str = "parallel") -> Net:
    """Apply one round of reductions. Returns new net."""

def normalize(net: Net, max_steps: int = 10_000) -> Net:
    """Reduce to normal form. Raises if max_steps exceeded."""

def trace(net: Net, n: int) -> list[Net]:
    """Return list of n successive reduction steps."""

def count_redexes(net: Net) -> int:
    """Number of active pairs currently in net."""

Rule Registration

# Define a custom interaction rule
@rule(left="Lam", right="App")
def beta(lam: Agent, app: Agent) -> list[tuple[Port, Port]]:
    # returns list of port-to-port connections replacing the active pair
    return [
        (lam.ports["aux0"], app.ports["aux1"]),  # body <- arg
        (lam.ports["aux1"], app.ports["aux0"]),  # var  <- func residue
    ]

When a rule is applied, the two agents (Lam, App) and the edge between their principal ports are deleted. The returned port connections replace them.

---

Tool 1c: nela.compiler — NELA-S → NELA-C Bytecode Compiler (v0.10)

File: src/nela_compiler.py

Purpose: Compile a parsed NELA-S program to a .nelac binary file — a serialised interaction net graph. This is the primary bridge between the human-readable surface language and the low-level NELA-C network layer.

Public API

def compile_and_run(prog: dict, fn_name: str, *args) -> tuple[Any, bytes]:
    """
    Compile fn_name(*args) from prog, run it eagerly, and return:
      (python_result, nelac_bytes)
    nelac_bytes is the serialised normal-form net for the result value.
    Uses stable-id format (v3) so node record order is irrelevant.
    """

def net_to_bytes(net: Net, root_nid: int, fn_table=None, stable_ids: bool=False) -> bytes:
    """Serialise Net to .nelac binary (supports legacy v1/v2 and stable v3/v4)."""

def bytes_to_net(data: bytes) -> tuple[Net, int]:
    """Deserialise .nelac binary back to (Net, root_nid)."""

def bytes_to_py(data: bytes) -> Any:
    """Deserialise .nelac binary directly to Python value."""

def disassemble(data: bytes) -> str:
    """Human-readable node listing for a .nelac binary."""

.nelac Binary Format

b"NELAC"          magic (5 bytes)
version: u8       format version
node_count: u32   number of nodes (big-endian)
nodes[]:          node table
    v1/v2 records:
        tag: u8         agent type
        arity: u8       number of ports
        meta: i64       payload (int/float bits/string length/bool; big-endian)
        ports[arity+1]: u32  port node IDs (0xFFFFFFFF = unconnected)
    v3/v4 records:
        nid: u32        explicit node ID (order-independent decoding)
        tag: u8
        arity: u8
        meta: i64
        ports[arity+1]: u32
root: u32         node ID of root output

Version guide:

• v1: legacy, implicit node IDs by stream order
• v2: legacy + function table, implicit node IDs by stream order
• v3: stable IDs, order-independent node record decoding
• v4: stable IDs + function table

Compatibility behavior:

• compile_program(...) keeps emitting legacy versions for C runtime compatibility.
• compile_and_run(...) emits stable-id version for Python-side robustness.

Agent Tag Table

Tag	Hex	Arity	Description
CON	0x01	2	List cons cell h:t (head aux0, tail aux1)
DUP	0x02	2	Duplicator δ (copying)
ERA	0x03	0	Eraser ε (discard)
APP	0x04	2	Application
LAM	0x05	2	Lambda abstraction
INT	0x10	0	Integer leaf; value in meta as i64
FLT	0x11	0	Float leaf; value in meta as IEEE 754 bits (struct.pack "d")
STR	0x12	1	String leaf; length in meta, chars in aux0 CON chain
BOO	0x13	0	Boolean leaf; meta = 1 (True) or 0 (False)
PAR	0x14	2	Pair/tensor (a, b); aux0 = left, aux1 = right (distinct from CON)
ADD	0x20	0	Arithmetic op addition result leaf
SUB	0x21	0	Subtraction
MUL	0x22	0	Multiplication
DIV	0x23	0	Integer division
MOD	0x24	0	Modulo
NEG	0x25	0	Unary negation
EQL	0x30	0	Equality comparison result
LTH	0x31	0	Less-than
LEQ	0x32	0	Less-or-equal
GTH	0x33	0	Greater-than
GEQ	0x34	0	Greater-or-equal
AND	0x40	0	Boolean AND
ORR	0x41	0	Boolean OR
NOT	0x42	0	Boolean NOT
IFT	0x50	2	If-then-else result; aux0 = then-branch, aux1 = else-branch
NIL	0x60	0	Empty list []
HED	0x61	0	head op result
TAL	0x62	0	tail op result
GET	0x63	0	list index result
LEN	0x64	0	list length result
ARR	0x65	0	array constructor result
AST	0x66	0	aset (array set) result

Critical distinction: CON (0x01) is list-only. PAR (0x14) is pair/tuple-only. _node_to_py uses the tag to determine [h] + t (CON) vs (l, r) (PAR). Mixing them causes incorrect decoding for pairs of lists (e.g., the output of split in mergesort).

Compilation Strategy (v0.10: Eager / Call-by-Value)

The compiler traverses the NELA-S AST and immediately evaluates every expression to a Python value, then converts the result to a leaf/CON/PAR/NIL chain in the Net. Functions are called via Python recursion with the NELA-S interpreter semantics. The resulting net is the normal-form of the computation — no active pairs remain.

v0.11 plan: Emit unreduced nets with active pairs; run the SIC (Symmetric Interaction Combinators) reducer on-net before serialisation. This enables lazy evaluation and first-class functions in .nelac files.

Known Bugs Fixed in v0.10

1. CON/PAR ambiguity — _py_to_node originally used CON for both lists and tuples. Fixed by adding PAR = 0x14 for tuples exclusively.
2. Dict literal eager evaluation — {"div": lv//rv, ...}[op] evaluates ALL entries before indexing, causing ZeroDivisionError for rv=0 even on non-div ops. Fixed with if/elif chain.

---

Tool 3: nela.types — Type Checker

Purpose: Verify linear typing and dependent type correctness of NELA nets.

Type Language

Type ::=
  | Atom(name)                     -- base type: Nat, Bool, String, ...
  | Linear(A, B)         A -o B    -- linear function
  | Tensor(A, B)         A ⊗ B     -- multiplicative pair (both consumed)
  | With(A, B)           A & B     -- additive pair: offer both; consumer picks one (Mat_T branches)
  | Plus(A, B)           A ⊕ B     -- additive sum: exactly one provided (Con_i / ADT constructors)
  | Bang(A)              !A        -- exponential: copyable and discardable resource
  | IO(A)                IO(A)     -- linear world token threading side effects
  | Pi(x : A, B(x))               -- dependent product
  | Sigma(x : A, B(x))            -- dependent sum
  | Id(A, a, b)                    -- identity / equality type
  | Unit                 1         -- tensor unit
  | Zero                 0         -- empty / eraser type

Correction: With and Plus were absent in the original spec. With is required to type Mat_T branches (each branch is offered, only one is selected by annihilation). Plus is required to type ADT values (tagged injection via Con_i). Without these, Mat_T had no well-formed type.

Interface

def check(net: Net) -> TypeResult:
    """
    Returns TypeResult with:
      - ok: bool
      - errors: list[TypeError]  (port, expected, actual)
      - proof_net: bool          -- passes Girard correctness criterion
    """

def infer_ports(net: Net) -> dict[Port, str]:
    """Bidirectional type inference on all free ports."""

def girard_criterion(net: Net) -> bool:
    """
    Check proof net correctness (long trip condition).
    A net passes iff it corresponds to a valid LL proof.
    """

def linearity_check(net: Net) -> list[Port]:
    """Return list of ports violating linearity (used ≠ 1 time)."""

Typing Rules (selected)

Lam: $$\frac{\Gamma, x : A \vdash \text{body} : B}{\Gamma \vdash \text{Lam}(\text{body}, x) : A \multimap B}$$

App: $$\frac{\Gamma_1 \vdash f : A \multimap B \quad \Gamma_2 \vdash a : A \quad \Gamma_1 \cap \Gamma_2 = \emptyset}{\Gamma_1, \Gamma_2 \vdash \text{App}(f, a) : B}$$

Dup: (requires !A) $$\frac{\Gamma \vdash e : {!A}}{\Gamma \vdash \text{Dup}(e) : A \otimes A}$$

Era: (requires !A) $$\frac{\Gamma \vdash e : {!A}}{\Gamma \vdash \text{Era}(e) : \mathbf{1}}$$

Inl: (additive left injection) $$\frac{\Gamma \vdash a : A}{\Gamma \vdash \text{Inl}(a) : A \oplus B}$$

Inr: (additive right injection) $$\frac{\Gamma \vdash b : B}{\Gamma \vdash \text{Inr}(b) : A \oplus B}$$

Case: (additive elimination; exactly one branch fires) $$\frac{\Gamma_1 \vdash s : A \oplus B \quad \Gamma_2 \vdash f : A \multimap C \quad \Gamma_2 \vdash g : B \multimap C \quad \Gamma_1 \cap \Gamma_2 = \emptyset}{\Gamma_1, \Gamma_2 \vdash \text{Case}(f, g, s) : C}$$

Fix: (corrected; function receives copyable recursive handle) $$\frac{\Gamma \vdash F : !(A \multimap B) \multimap A \multimap B}{\Gamma \vdash \text{Fix}(F) : A \multimap B}$$

IOToken threading: $$\frac{\Gamma_1 \vdash a : A \quad \Gamma_2 \vdash \mathit{io} : \mathbf{IO} \quad \Gamma_1 \cap \Gamma_2 = \emptyset \quad \text{handler} : A \otimes \mathbf{IO} \multimap B \otimes \mathbf{IO}}{\Gamma_1, \Gamma_2 \vdash \text{handler}(a, \mathit{io}) : B \otimes \mathbf{IO}}$$

---

Tool 4: nela.serialize — Serialization / Deserialization

Purpose: Convert NELA nets to/from compact representations optimized for LLM context windows.

Formats

Format	Description	Use case
json	Full JSON graph (human-readable)	Debugging, storage
compact	Adjacency list (integer node IDs, no field names)	Context-window compression
binary	Msgpack binary encoding	High-throughput pipeline
dot	Graphviz DOT language	Visualization
latex	Proof net diagram (TikZ)	Documentation

Interface

def to_json(net: Net) -> dict:
    """Full serialization with agent names, types, port labels."""

def from_json(data: dict) -> Net:
    """Deserialize; validates signature and linearity."""

def to_compact(net: Net) -> str:
    """
    Compact adjacency format:
      <n_nodes> <n_edges>
      <agent_idx> <agent_idx> ...   (one per node)
      <node_i> <port_i> <node_j> <port_j> ...  (one per edge)

    Port encoding: 0 = principal, 1..n = aux0..auxN-1
    Token cost: ~3 tokens per node, ~4 tokens per edge.
    """

def from_compact(s: str, signature: dict) -> Net:
    """Parse compact format back to Net."""

def token_cost(net: Net) -> int:
    """Estimate LLM token cost for compact format."""

Context Budget Planning

For an LLM with context window $W$ tokens and overhead $O$ tokens reserved for reasoning:

$$\text{max edges} = \lfloor (W - O) / 4 \rfloor$$

$$\text{max nodes} = \lfloor (W - O) / 3 \rfloor$$

A complex program with $N$ functions: estimate $\approx 12N$ tokens for compact format vs. $\approx 80N$ tokens for equivalent Python.

---

Tool 5: nela.migrate — Legacy Code Migration

Purpose: Extract semantic intent from existing source code and reconstruct it as a NELA net.

Pipeline

Source code (Python/Rust/JS/...)
         │
         ▼
  [Step 1] AST Extraction
         │  language-specific parser
         ▼
  [Step 2] Semantic Intent Extraction
         │  LLM (Architect model): "what does this function DO?"
         │  Output: TypedSpec JSON (not code)
         ▼
  [Step 3] NELA Construction
         │  LLM (Constructor model): TypedSpec → NELA net
         ▼
  [Step 4] Equivalence Verification
         │  Property-based testing: source_fn(x) == nela.eval(net, x) for random x
         ▼
  NELA net (semantically equivalent)

Interface

def extract_intent(source: str, language: str) -> TypedSpec:
    """
    Returns TypedSpec:
    {
      "name": str,
      "inputs": [
        {
          "name": str,
          "type": str,
          "banged": bool   -- True if this value will be Dup-ed (e.g., pivot in quicksort)
        }
      ],
      "outputs": [{"type": str}],
      "behavior": str,             -- NL description of intent
      "invariants": [str],         -- formal properties to preserve
      "side_effects": [str],       -- explicit list; non-empty ⇒ IOToken must appear in type
      "mutual_with": [str]         -- names of mutually recursive co-functions (if any)
    }
    """

def build_from_spec(spec: TypedSpec) -> Net:
    """Constructor model: produces NELA net from TypedSpec."""

def verify_equivalence(source_fn, net: Net, n_samples: int = 1000) -> VerifyResult:
    """
    Property-based equivalence testing.
    Returns { ok: bool, counterexample: any | None }
    """

Migration Strategy for Large Codebases

1. Topological sort the dependency graph of the codebase
2. Migrate leaf functions first (no dependencies)
3. Verify each migration before proceeding to callers
4. Build NELA standard library from migrated primitives
5. Replace callers bottom-up; discard original source after verification

---

Tool 7: nela.llm — LLM Interface

Purpose: Bridge between natural language and NELA graph construction/interpretation.

Architect Model Interface

def nl_to_spec(natural_language: str, context: list[Net] = None) -> TypedSpec:
    """
    Architect model: translate NL requirement to formal TypedSpec.
    context: existing NELA nets available for reference (type signatures only).
    Raises AmbiguityError if intent cannot be resolved without clarification.
    """

def clarify(spec: TypedSpec, question: str) -> TypedSpec:
    """Refine a TypedSpec based on follow-up clarification."""

Constructor Model Interface

def spec_to_net(spec: TypedSpec, sig: dict) -> Net:
    """
    Constructor model: builds NELA net from TypedSpec.
    Operates ONLY on graph structure — no natural language output.
    The model receives the compact adjacency format in its prompt.
    Returns validated, type-checked Net.
    """

def patch_net(net: Net, delta_spec: TypedSpec) -> Net:
    """
    Modify an existing net based on a change specification.
    Only touches the subgraph relevant to delta_spec (locality property).
    """

Context Window Budget

CONTEXT_OVERHEAD = 2048    # tokens reserved for instructions + reasoning

def fits_in_context(net: Net, window_size: int = 128_000) -> bool:
    cost = token_cost(net) + CONTEXT_OVERHEAD
    return cost <= window_size

---

Tool 8: nela.verify — Formal Verification

Purpose: Verify NELA nets against formal specifications using type-theoretic proof checking.

Interface

def is_confluent(rules: list[Rule]) -> bool:
    """Check that the rule set satisfies strong confluence (Theorem 2.1)."""

def terminates(net: Net, sig: dict) -> bool:
    """
    Check termination via interaction complexity measure:
    Assign weight w(α) to each agent; prove sum strictly decreases.
    Raises UndecidableError for nets containing Fix agents (recursion).
    """

def prove_property(net: Net, prop: str) -> ProofResult:
    """
    Attempt to automatically prove a property expressed as a type.
    prop: a type expression; net must inhabit the type.
    Uses the Curry-Howard correspondence: types = propositions.
    """

def ripple_effect_free(net: Net, change: PortChange) -> bool:
    """
    Check that modifying the subgraph at `change` has no effect outside
    the transitive closure of directly connected agents.
    Guaranteed True for well-formed NELA nets (locality property).
    """

Formal Properties Guaranteed by NELA Structure

Property	Guarantee	Formal basis
No ripple effects	Modifying a subgraph only affects reachable ports	Locality of interaction net rules
No aliasing	No two agents share the same resource	Linearity (each port connected once)
Confluence	All evaluation orders reach same result	Theorem 1.2 (Lafont 1990)
Type safety	No type errors at runtime	Well-typed net (Section 5.3)
Structural impossibility of invalid states	Invalid configurations have no representation	Linear type system + proof net criterion
IO ordering	Side-effecting operations are sequentially ordered	IOToken linearity (cannot be Dup-ed)
ADT exhaustiveness	Pattern match covers all constructors	&-type branch offer; Con_i ⊳ Mat_T annihilation

---

Dependency Diagram

nl_to_spec (Tool 7)
      │ TypedSpec
      ▼
spec_to_net (Tool 7) ─── nela.graph (Tool 1b)
      │ Net               │
      ▼                   ▼
nela.types (Tool 3)   nela.rewrite (Tool 2)
      │ TypeResult        │ Net (normal form)
      ▼                   ▼
nela.verify (Tool 8)  nela.serialize (Tool 4)
                          │
                          ▼
                    nela.migrate (Tool 5)
                    (legacy bridge)