Skip to content

STATUS.md

Latest commit

 

History

History
51 lines (37 loc) · 10.6 KB

STATUS.md

File metadata and controls

51 lines (37 loc) · 10.6 KB
Raw

Component: interp

Status: tested Last updated: 2026-07-25 · S29 TimeMs eval arm (the time builtin — IoToken → (IoToken, f64) against one process-lifetime Instant epoch; the interpreter is the oracle for the clock's shape, never for a duration). S21: Widen eval arm (Rust as conversions — round-ties-even, exactly LLVM sitofp/fpext and C-cast semantics; the oracle-normative denotation). S20: Iota/Fill arms + contracts. S13: ADR-0021 Update eval arm + loop-driven matmul4 / fanout value-semantics contracts; LoopPlan derivation migrated to mapal_ir::loop_plan (BL7) Spec references: interp/DESIGN.md (increment 1, M1) · ADR-0002 (E1 fueled/Elgot loop semantics) · ADR-0016 (guard-first loop branch evaluation) · ADR-0013 (traps: int div/mod-zero, OOB Index; float IEEE) · ADR-0015 (print/println) · ir/DESIGN §5.1/§7/§8/§13 · category-ir.md §2.6–2.8/§11.4. Depends on: ir (only — borrowed &CategoryIr, never mutated; + slotmap for the env/buffer SecondaryMaps). Tests also use lower + syntax (dev-deps) for the parse→lower→run pipeline. Depended on by: rewrite, backend-llvm, backend-cuda, backend-verilog, cli (the differential-test oracle).

What works

The fueled reference interpreter (THE ORACLE) — parse → lower → run for all nine examples/*.mapal produces the exact pinned output: abs "7\n" · sum_to_n "55\n" · pipeline "f(10) = 25\n" · fanout "36\n12\n" · fir "5.375\n" · sepia "4080\n" · zip_demo "c[0] = 100\nc[15] = 115\ne[0] = 0\ne[15] = 30\n" (ADR-0018 zip + enumerate) · vector_add "c[0] = 100\nc[15] = 115\nsum = 1720\n" · seq_demo "36\n12\n" (ADR-0019 — no interp code change, pin d: seq has no IR footprint, ordering is the token thread). Plus the committed countdown fixture → "5\n4\n3\n2\n1\n0\n".

  • Value domain (§1): RValue = Scalar(mapal_ir::Value) | Tuple | Struct | Array | Token(String) | Unit; Outcome = Done | Diverged | Trapped(TrapKind); internal Result<RValue, Abort> with ?, lifted to Outcome at the boundary.
  • Evaluator (§2/§3): env (SecondaryMap<ObjectId, RValue>) + topo walk; per-slot Pair product assembly into Tuple/Struct/Array; all Core ops (arith at operand width, Div/Mod int-trap & float-IEEE, Neg fneg, comparisons with IEEE NaN ordering, And/Or/Not, Phi, Proj, Call, Map, Fold, Index, Zip, Enumerate, Iota, Fill, Update, Print{newline}, TimeMs, Output).
  • Iota / Fill (ADR-0029, stage 1): Iota materializes [0,…,n-1] as [i32; n] (count = the Constant source); Fill materializes [x; n] (count = the internal 2-tuple's slot-1 Constant, read like Zip's pair). Both total/pure/trap-free — the oracle-normative denotations every backend must reproduce (tests/iota_fill.rs: the contracts, incl. iota → map — the benchmark generators' target shape).
  • Update (§3 / ADR-0021): Update(arr, i, v) returns a fresh array with slot i replaced (eval.rs:update); OOB (i<0 ∨ i≥n) ⇒ Trapped(IndexOob), same class as Index; pure — no token, one budget spend. Value semantics: two branches updating the same source array produce independent results (the pipeline fixture pins it). Loop-driven mut c[i] <- … builds a 4×4 matmul result one slot per iteration.
  • Zip / Enumerate (§3 / ADR-0018): Zip pairs two equal-size arrays elementwise ([(a[i],b[i])]); Enumerate pairs each element with its i32 index ([(0,a[0]),…], n ≤ i32::MAX ir-guaranteed so the cast is exact). Both total/pure — no trap, no token, one budget spend per morphism — and legal under parallel fanout. These are the oracle-normative denotations for every future backend.
  • Guard-first loop driver (§4 / ADR-0016): the decide/exit cone is evaluated first, the guard is read, and the continue-branch (next-state) is evaluated only when the guard continues — so fir's coeffs[k] is never indexed at k=4 (no spurious IndexOob) and countdown prints 0 on its exit step. The 55-contract holds by execution.
  • Effects (§5): world token = RValue::Token(String); print raw, println appends \n; effect order = dataflow order (E2 structural, no scheduler). Floats render via Rust shortest round-trip (4080.0→"4080", 5.375→"5.375").
  • Clock (§5 / plan-time-builtin, S29): TimeMs consumes the token and writes Tuple[token, F64(ms)] (eval.rs), reading elapsed against one process-lifetime Instant epoch (eval.rs:time_epoch — the same clock kind as mapal-rt's mapal_time_ms). Effectful by token, so no rewrite or reorder touches it. The denotation is monotone + finite only: tests/acceptance.rs::time_brackets_are_monotone_and_finite pins t1 >= t0 >= 0 and that the bracketed iota → map still computed (3969); a duration is a machine fact, never a golden.
  • Fuel / divergence / traps (§6): global u64 budget decremented per morphism; 0 ⇒ Diverged (returns, never hangs). Trapped(DivZero)/Trapped(IndexOob); float 1.0/0.0 ⇒ Done(inf).
  • Entry & API (§7/§8): run(&ir, budget) -> RunResult{outcome, output} (seeds Token("") for an IoToken entry, Unit otherwise); eval_call(&ir, f, arg, budget) -> Outcome. No Display (C3).

What does not / known issues

  • Out-of-M1 loop shapes (multi-merge SCC, >1 LoopBack, ≠1 attributed LoopExit per merge's own SCC) make mapal_ir::loop_plan return None, which run_loop unwraps as unreachable! (S13: the predicate moved to mapal-ir, BL7 — was an assert! in the interp-local derive_plan), not a returned error variant (Outcome has no error case; DESIGN §9 classes these as unreachable!-class; the multi-merge nested shape IS lower-reachable — rewrite RW8/F3 — but never produced by the examples/testgen). S12: attribution is per-merge-SCC, never the per-fn union — the union falsely tripped this on two sequential canonical loops (legal Core, now supported + pinned); and multi-hop computed loop-invariants (x*2, a[i*4+k]) previously read-before-write-panicked the driver — fixed by ir §13's LoopEnter deferral (both pinned in tests/loop_invariants.rs).
  • mapal_ir::loop_plan recomputes the per-merge layout (topo/SCC/decide-cone fixpoint) on every run_loop invocation rather than caching once per merge — a minor perf cost only for a looping fn called repeatedly (none in the six examples). Deferred (YAGNI; profile-driven).
  • Per-iteration reset clears staging buffers, relying on each product's slot feeders living in a single phase (true at M1 — no straddling product across decide/advance). Not asserted in code; revisit if a future loop shape splits a product's slots across the guard.
  • Integer overflow uses wrapping_* (IN7, out of M1 scope; no example overflows) — pinning UB-vs-wrap-vs-trap is a later mapal-check/backend ADR.

Invariants enforced (and where in code)

  • Totality (C-interp-1/E1): every run halts with Done/Diverged/Trapped; budget decrement per eval_morphism (eval.rs); divergence threaded as Abort::Diverged via ?, lifted in eval_call/run (lib.rs).
  • Guard-first (ADR-0016): loops.rs run_loop evaluates decide_order → reads cond from exit_route@1 → evaluates advance_order only on continue.
  • Determinism (C-interp-3/E2): SecondaryMap + Vec only, no HashMap; Map/Fold iterate array order (eval.rs). Tested by running each example twice.
  • No IR mutation: the IR is borrowed & throughout; the library depends on mapal-ir (+ slotmap) only.

Test coverage (golden / property / differential / skipped+why)

63 tests, all green (the inventory below is the S13 base; appended since: S18 captures.rs/loop_exit_payload.rs, S20 iota_fill.rs — 3 contracts + 2 e2e — S29 acceptance.rs::time_brackets_are_monotone_and_finite (the one time test the oracle owes: monotone, finite, work-still-ran — no duration assertion), and S21 widen.rs: the four-edge value contract at the boundary values i32::MIN sign-extension, 16777217 f32 round-to-even, −2000000001 exact f64, 0.1f32 fpext). tests/loop_invariants.rs (3, S12): computed-invariant loop body (x*2 → 30), full 4×4 matmul with dynamic indexing over computed invariants (a[i*4+k], user-found repro → 8\n136\n), two sequential loops in one fn (→ 20\n). tests/acceptance.rs (15): nine example goldens (incl. zip_demo + vector_add ADR-0018, seq_demo ADR-0019) + countdown + eval_call(sum_to_n,10)==Done(I32(55)) + fir4(...)==Done(F32(5.375)) + sepia-input-ty sanity + sum_to_n_seq_wrapped_reassign_value_contract (ADR-0019 pin b: a loop-carried mut reassigned inside a seq still threads the loop merge — oracle-pinned to 55; the S11 fix for lower's carried-set walker). tests/traps.rs (8): int div/mod-0, Index i=n/i=-1, float 1.0/0.0=Done, nan_ordering_is_ieee (Lt/Gt/Le/Ge/Eq false, Neq true on NaN), in-bounds/nonzero sanity. tests/divergence.rs (3): budget boundary on sum_to_n + constant-true-guard loop ⇒ Diverged (returns). tests/determinism.rs (6): each example byte-identical across two runs. tests/zip_enumerate.rs (3, ADR-0018): zip'd add value contract (c[0]=100, c[15]=115), enumerate i32 index pairing, enumerate-under-fanout — IR built directly via the mapal-ir builder (lower's builtin routing is WP2, landing concurrently). tests/update.rs (4, ADR-0021): update_in_bounds_replaces_one_slot, update_at_n_traps / update_negative_traps (OOB ⇒ Trapped(IndexOob)), update_u8_index_ge_128_in_bounds (u8 index ≥128 is in-bounds, not sign-confused). tests/update_pipeline.rs (3, ADR-0021, parse→lower→run): matmul4_loop_driven_builds_result_via_mut_array (loop-driven mut c[i] <- … → matmul), fanout_two_branches_update_same_source_independently (value semantics), runtime_oob_update_traps_through_pipeline. Differential (backend-vs-oracle) lands with the backends (P5+).

Performance notes (numbers + bench name + date; regressions flagged)

benches/interp_scale.rs (criterion) — baseline Session 08 (2026-06-15): deep_loop/1000 323 µs, deep_loop/10000 3.20 ms; large_map/1000 862 µs, large_map/10000 8.56 ms (≈ linear in step count). First baseline; no regressions tracked yet.

Open questions (→ ADR candidates)

  • IN6 float ÷0 amendment — closed S13: ADR-0013 amended + ratified (integer-trap / float-IEEE is normative).
  • Multi-merge / multi-back-or-exit loop SCCs are out of M1 (§4 scope); lifting waits on lower OQ7.
  • mapal-check owes the §9 assumptions (Return exclusivity IN3, seq effect legality E2, full typing/E3) — discharged: T0101 + T0201 delivered S10; E2 walk rebased node-kind (ADR-0019, S11); typing at the validate boundary; E3 vacuous-by-proof.