pyvm: split op handlers into ops_core/ops_box/ops_ctrl; add ops_flow + intrinsic; delegate vm.py without behavior change
net-plugin: modularize constants (consts.rs) and sockets (sockets.rs); remove legacy commented socket code; fix unused imports mir: move instruction unit tests to tests/mir_instruction_unit.rs (file lean-up); no semantic changes runner/pyvm: ensure using pre-strip; misc docs updates Build: cargo build ok; legacy cfg warnings remain as before
This commit is contained in:
27
docs/reference/invariants.md
Normal file
27
docs/reference/invariants.md
Normal file
@ -0,0 +1,27 @@
|
||||
# Nyash Invariants (Spec)
|
||||
|
||||
This document lists non‑negotiable invariants the implementation preserves across backends. They’re 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 immediately‑preceding expression.
|
||||
- LoopForm
|
||||
- Loop bodies may be normalized where safe to a stable order: non‑assign statements then assign statements. No semantic reorder is performed when a non‑assign 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 loop‑aware lowering).
|
||||
- Scope
|
||||
- Enter/Leave scope events are observable through MIR hints; they do not affect program semantics.
|
||||
|
||||
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.
|
||||
Reference in New Issue
Block a user