Files
hakorune/docs/reference/invariants.md

29 lines
1.8 KiB
Markdown
Raw Permalink Normal View History

# Nyash Invariants (Spec)
This document lists nonnegotiable invariants the implementation preserves across backends. Theyre used as a contract for testing and design.
Core
- PHI hygiene
- No empty PHI nodes are emitted in LLVM IR (temporary safety valve exists behind `NYASH_LLVM_SANITIZE_EMPTY_PHI=1`).
- All PHIs appear at the beginning of a basic block.
- Match/Peek
- A match scrutinee is evaluated exactly once, bound to an internal gensym.
- Guard conditions are logically conjoined with the arm predicate; fallthrough reaches the next arm.
- Exceptions
- Exceptions follow “scope first” semantics. Postfix `catch/cleanup` normalize to a single `TryCatch` block around the immediatelypreceding expression.
- LoopForm
- Loop bodies may be normalized where safe to a stable order: nonassign statements then assign statements. No semantic reorder is performed when a nonassign appears after any assign.
- Carrier analysis emits observation hints only (zero runtime cost).
- Break/continue lowering is unified via LoopBuilder; nested bare blocks inside loops are handled consistently (Program nodes recurse into loopaware lowering).
- Scope
- Enter/Leave scope events are observable through MIR hints; they do not affect program semantics.
- Blockscoped locals: `local x = ...` declares a binding limited to the lexical block. Assignment without `local` updates the nearest enclosing binding; redeclaration with `local` shadows the outer variable. This is Lualike and differs from Python's block (no) scope.
Observability
- MIR hints can be traced via `NYASH_MIR_HINTS` (pipe style): `trace|scope|join|loop|phi` or `jsonl=path|loop`.
- Golden/Smoke tests cover representative invariants.
Backends
- PyVM and LLVM share semantics; PyVM prioritizes clarity over performance.
- Cranelift/WASM routes inherit the same invariants when enabled.