mirror of
https://github.com/brazilofmux/tinymux
synced 2026-08-13 00:23:11 -04:00
caaf252cff
Beef residual coverage at the softcode JIT / Lua JIT boundary: production nest shapes, host setq/attr survival, multi-entry lua(), mux.eval effects, and float/nil/bool marshal consumers. Expand tests/luajit NESTED under brackets-on and add STATE e4 so mux.eval cannot re-run silently.
162 lines
8.6 KiB
Markdown
162 lines
8.6 KiB
Markdown
# Transition plan: Lua post-entry decline/rerun → softcode contract
|
||
|
||
**Status:** campaign complete (2026-07-29); residual quality work continues
|
||
**Stake issue:** [#1751](https://github.com/brazilofmux/tinymux/issues/1751) (closed)
|
||
**Related product enablement:** [`plan-lua-jit-product.md`](plan-lua-jit-product.md)
|
||
|
||
**One-line summary:** Post-entry re-run is gone; remaining work is typed fidelity, corpus growth, and pre-entry eligibility — not “one more soft decline.”
|
||
|
||
This document was the multi-agent source of truth for the campaign. It now records **what shipped**, the **standing contract**, and **residual design goals** so later work does not re-open the poison mechanism.
|
||
|
||
---
|
||
|
||
## 0. Where we are vs where we wanted to go
|
||
|
||
### Shipped (Phases 0–4 + follow-ups)
|
||
|
||
| Layer | State |
|
||
|--------|--------|
|
||
| Default `lua_jit` | **On** (#1745 / #1325) |
|
||
| Nested softcode → Lua | Executes (#1326) |
|
||
| Instruction budget | Live at run time (#1749); LIMITED = interpreter text (Phase 3) |
|
||
| Post-entry re-run | **Deleted** (Phase 4) — fail loud or complete; never silent re-run |
|
||
| GET/SET/LEN family | Total ECALLs or plain-proven typed paths (Phase 1) |
|
||
| CALL boundary | Claims at lowering; marshal at softcode boundary; ineligible for type-erased Lua consumers (#1763 / #1764) |
|
||
| Effectors (`notify`/`pemit`/`set`/`eval`) | **Same bridge on both routes** — effect-free corridor retired after Phase 4 (exactly-once without re-run) |
|
||
| Lua truthiness | VALUE / BOOL / NIL tags; only nil/false falsy |
|
||
| Known-absent plain GETI | Closed key set → nil at lowering (no GETI_INT post-entry miss) |
|
||
| Harness ratchets | `POST_ENTRY_LOUD_BUDGET=0`, `AGREE_DECLINE_BUDGET` may only fall |
|
||
|
||
### Target (unchanged contract)
|
||
|
||
Same product knobs (`lua_jit` on, brackets on), with:
|
||
|
||
1. **All soft refusal at lowering** (cache miss / “ineligible” only).
|
||
2. **After entry:** finish, raise what the interpreter would raise, or budget/alarm as the **interpreter’s** limit — **never** whole-chunk re-run.
|
||
3. **No live values baked** into the program at lower time.
|
||
4. Dynamism handled by **total ECALLs** to real VM ops, or compile-time proof — not “maybe decline later.”
|
||
|
||
Exhibits 1–2 (double mutation; lost effect under re-run) **cannot recur by construction**: re-run is gone.
|
||
|
||
---
|
||
|
||
## 1. Non-negotiable contract (standing)
|
||
|
||
```text
|
||
PRE-ENTRY (nothing user-visible has run yet)
|
||
✓ refuse lower / miss cache → interpreter OK
|
||
|
||
POST-ENTRY (guest code or user-visible Lua work may have run)
|
||
✓ complete successfully
|
||
✓ same error the interpreter would raise
|
||
✓ budget/alarm as interpreter-identical limit error
|
||
✗ silent re-run of the whole chunk
|
||
✗ “decline because type/metatable surprised us” after entry
|
||
```
|
||
|
||
**Failure is allowed; retry is the poison.**
|
||
|
||
`ECALL_DECLINE` remains only as a residual safety net that commits a loud error (no re-run). New handlers must not rely on it for policy — prefer total ops or lowering ineligibility.
|
||
|
||
---
|
||
|
||
## 2. What the phases meant (historical map)
|
||
|
||
| Phase | Goal | Outcome |
|
||
|-------|------|---------|
|
||
| 0 | Post-entry decline → loud, no re-run | Shipped; `POST_ENTRY_LOUD` ratchet |
|
||
| 0.5 | STATE purity oracle | Green; exhibits 1–2 covered |
|
||
| 1 | Total GET/SET/LEN | Shipped; plain_proven for typed reads |
|
||
| 2 | CALL claims / marshal / ineligible | Shipped; #1763 marshal + #1764 consumer refuse |
|
||
| 3 | LIMITED = interpreter limit | Shipped |
|
||
| 4 | Delete re-run | Shipped |
|
||
| Follow-up | Truth tags; closed-key nil; effectors on path | Shipped / in flight as residual PRs |
|
||
|
||
Do **not** reintroduce silent re-run as a “fix.” Do **not** revive effect-free corridor as the end state — it was medicine under re-run.
|
||
|
||
---
|
||
|
||
## 3. Residual design goals (quality, not campaign reboot)
|
||
|
||
These are the open quality / clarity targets after #1751 close:
|
||
|
||
| Goal | Shape | Notes |
|
||
|------|--------|------|
|
||
| **Typed CALL results** | CALL_VAL leaves results on the VM stack; RET marshals; TOBOOL for if/not | Landed for default STRING claims; remaining: VM `==`/arith on handles, CALL_INT nil |
|
||
| **Runtime absent key** | GETI with non-constant key still may hit residual NONINT loud | Closed-set covers constant keys only; dynamic miss needs nil in a typed or handle slot |
|
||
| **Anytime items 3–5** | Nested `mux.args`/executor stomp; `lua_checkstack`; int-returning bridge claims | Independent small work; does not wait on typed results |
|
||
| **Seam corpus** | Softcode ↔ Lua smoke TC061–090; NESTED+STATE e4 in `tests/luajit` | Answer + host setq/attr + multi-entry + mux.eval under brackets |
|
||
| **ECALL_DECLINE ABI** | Optional: assert/unreachable in Lua handlers | Phase 4 left a loud safety net; tightening is polish |
|
||
| **Softcode CALL_FUNC sibling** | Same post-entry audit | **Done** — [#1791](https://github.com/brazilofmux/tinymux/issues/1791) / [`plan-softcode-post-entry-contract.md`](plan-softcode-post-entry-contract.md) |
|
||
|
||
### Design principles for residuals
|
||
|
||
1. **String lies are non-goals** for in-Lua semantics. Marshal only at the softcode boundary (`fun_lua` / chunk return).
|
||
2. **Provenance over coercion.** When HIR erases a Lua type, refuse consumers or keep a handle — do not invent softcode truthiness.
|
||
3. **Proof enables typed fast paths** (`plain_proven`, `keys_closed`, call claims). Loss of proof → ineligible or total ECALL, not silent 0.
|
||
4. **Effects are allowed** on the compiled path under the same permissions as the interpreter, because re-run cannot double them.
|
||
5. **Equality compares TYPES, not representations.** Lua's `==` is false across types, and HIR erases exactly the distinctions that decide it: `false` and `0` are one ICONST, `nil` and `""` one empty SCONST, and the numeric path coerces `"5"` to `5`. Every equality opcode must classify both sides (`lua_type_class_of_value` / `_of_const`) before comparing. Order comparisons are *not* the same rule — Lua raises on mismatched types there, so they decline.
|
||
|
||
6. **New value class ⇒ consumer audit.** Producers are easy; consumers are easy to miss. Emptying a loud bin has repeatedly introduced silent wrongs (#1755, #1756, #1763, #1766 first cut) when a new HIR representation (type-erased string, nil-as-empty-SCONST, …) was not checked at every Lua-semantic use site — including opcodes that look like twins of ones already fixed (EQ vs EQK).
|
||
|
||
|
||
### Standing assumption: the softcode route has no post-entry decline
|
||
|
||
Compiled Lua effects are exactly-once (#1767) **because** nothing can re-run
|
||
a chunk after entry. That holds on the Lua side by construction (Phase 4).
|
||
It holds on the *softcode* side — which sits above `[lua(...)]` and was
|
||
explicitly out of scope for this campaign — only as a **derived** property
|
||
of two unrelated designs:
|
||
|
||
* the softcode depth / invocation / slot bails are checked **before**
|
||
`dbt_run` (the #1002 watermark design), so they are pre-entry; and
|
||
* after Phase 4 exactly one `return ECALL_DECLINE` remains in
|
||
`jit_compiler.cpp`, the defensive arm in `run_cached_program` that nothing
|
||
emits into.
|
||
|
||
If a softcode ECALL ever gains a post-entry decline, a compiled Lua effect
|
||
beneath it would be delivered again by the AST re-run, and **#1767's premise
|
||
expires silently**. The sibling softcode audit ([#1791](https://github.com/brazilofmux/tinymux/issues/1791),
|
||
[`plan-softcode-post-entry-contract.md`](plan-softcode-post-entry-contract.md))
|
||
confirmed CALL_FUNC is total (guest error strings, no soft decline) and
|
||
blocked mid-run DBT failure → AST re-run after any host ECALL via
|
||
`eval_ctx::host_ecalls`. Keep that invariant when adding softcode ECALL
|
||
cases.
|
||
|
||
|
||
---
|
||
|
||
## 4. Harness discipline
|
||
|
||
| Ratchet | Rule |
|
||
|---------|------|
|
||
| `POST_ENTRY_LOUD_BUDGET` | May fall, never rise; target **0** |
|
||
| `AGREE_DECLINE_BUDGET` | May fall, never rise; decline is correct but not coverage |
|
||
| EXEC | Must match **and** `lua_run_ok` advances |
|
||
| STATE | Persistent state + effect markers match across legs |
|
||
|
||
AGREE alone is green when the interpreter answers; EXEC and STATE are what make progress visible.
|
||
|
||
---
|
||
|
||
## 5. Success metrics (campaign close — met)
|
||
|
||
- [x] Phase 0 counter zero under suite (or only pre-entry remains)
|
||
- [x] Phase 0.5 oracle green
|
||
- [x] Phases 1–3 emptied the bins they own
|
||
- [x] Phase 4: no post-entry re-run path
|
||
- [x] Exhibits 1–2 cannot recur by construction
|
||
- [ ] Items 3–5 fixed or filed (optional residual)
|
||
|
||
---
|
||
|
||
## 6. Related
|
||
|
||
| Item | Role |
|
||
|------|------|
|
||
| #1751 | Stake issue (closed); exhibits and amendment history |
|
||
| #1750 / #1748 | Wrong compiled `mux.*`; effect-free medicine (retired after Phase 4) |
|
||
| #1749 | Runtime instruction budget (live-value template) |
|
||
| #1745 / #1325 | Default-on |
|
||
| #1763 / #1764 | CALL_STR marshal + consumer refuse |
|
||
| Softcode JIT | Existence proof for “compile decides; run commits” |
|