diff --git a/docs/journals/2026-05-16-audit-iteration-discipline-revert.md b/docs/journals/2026-05-16-audit-iteration-discipline-revert.md new file mode 100644 index 0000000..1855794 --- /dev/null +++ b/docs/journals/2026-05-16-audit-iteration-discipline-revert.md @@ -0,0 +1,107 @@ +# audit — iteration-discipline-revert milestone close + +**Date:** 2026-05-16 +**Milestone:** iteration-discipline-revert (HEAD `37ac704`) +**Verdict:** Milestone-iteration-discipline-revert tidy — **clean** + +## Step 1 — Architect drift review + +The revert is byte-pristine: all 18 reverted production source files ++ 5 reverted test files byte-identical to `git show 1ff7e81:` +(`crates/ailang-check/src/lib.rs` fully so); zero residual it.1/it.2 +production surface (`Term::Loop`/`Recur`/`LoopBinder`/ +`verify_structural_recursion`/`term_contains_loop`/`module_fns`/ +`"Diverge"`-injection / the five `Recur*`+`NonStructuralRecursion` +variants all absent from `crates/*/src/`). DESIGN.md coherent: +Decision 3 & 8 byte-identical to oracle, no loop/recur in §"Data +model", clause 3 retained (hunk-edited, not wholesale-restored — the +`1ff7e81` DESIGN.md had zero clause-3 text) with its worked example +de-claimed to explicit hypothetical, `skills/brainstorm/SKILL.md` +de-claimed in lockstep, F1/F4 idiom note present and guarded by a +passing `design_schema_drift.rs` test. Roadmap: Iteration-discipline +block + blocking-fork section gone, single deferred P2 entry with +correct `depends on:`/`context:`, F3 todo + Stateful-islands intact, +old spec carries the superseded header. + +One `[medium]` drift item: + +- `docs/roadmap.md` Stateful-islands `[~]` scope bullet still + asserted *"the 'Iteration discipline' P1 milestone supersedes the + earlier 'while-loops legal' scope … repetition is structural + recursion or named `loop`/`recur`"* — a dangling cross-reference + into the now-reverted milestone from a **live planning doc** that + would mislead the next brainstorm into treating `loop`/`recur` as + the committed repetition story. **Resolved inline** (Boss + doc-hygiene, full context already loaded): reworded to keep the + real, still-true scope guard (AILang has no `while`/`for`; this + milestone introduces none; repetition stays recursion exactly as + the language has it today; a `mut` block is a sealed expression, + never a loop) and drop the reverted-milestone reference. + +## Step 2 — Bench-regression check + +- `bench/compile_check.py` — exit 0 (24/24 stable). +- `bench/cross_lang.py` — exit 0 (25/25 stable; notably + `bench_list_sum.ail_bump_s` only +2.44% vs baseline). +- `bench/check.py` — exit 1: single metric + `throughput.bench_list_sum.bump_s` baseline 0.046s → 0.052s, + +12.71% (tol 10%); the 4 "improvements" are `gc_over_bump` ratio + shifts downstream of that one number. + +**Localisation (bencher, hypothesis-driven).** Built release `ail` +at HEAD `37ac704` and at the byte-oracle `1ff7e81` (read-only +`git worktree`, removed after). The compiled `bench_list_sum` +bump binaries are **`cmp`-identical** (byte-for-byte same machine +code, identical stdout). Interleaved 3 trials × 60 runs/arm: head +median 0.051233s vs oracle median 0.051206s; head−oracle delta +oscillates around zero (+0.05% / +0.61% / −0.20%, within ~1.5% +stdev); **both** arms read ~+11% over the 0.046 baseline on this +machine *now*. Verdict: **environmental/hardware drift relative to +the 2026-05-09 baseline-capture machine state, NOT a revert +regression** — confirmed independently of the architect byte-diff +and the implement Task-11 behavioural-equivalence sweep (third +independent proof the revert's codegen == `1ff7e81`'s codegen). + +## Step 3 — Classification & resolution + +- Architect `[medium]` roadmap dangling xref → **fix**, done inline + (Boss doc-hygiene; no separate tidy iteration warranted for a + one-bullet prose correction with a single correct outcome). +- `check.py` exit 1 → **carry-on**, baseline **NOT ratified**. + Ratify is categorically wrong here: nothing *intentionally* moved + the metric (the revert returned codegen to byte-identical + `1ff7e81`), and the audit Iron Law forbids a baseline bump without + an iter that intentionally moved it. Bumping 0.052 in would bake a + noise/environment value into `bench/baseline.json`. The spec's + "bench PRISTINE, not ratified" mandate is **satisfied**: pristine + means the revert introduced no regression, and it provably did not + (byte-identical binaries vs the clean `1ff7e81` oracle). +- The pre-existing `*.bump_s` baseline-vs-hardware staleness (the + `1ff7e81` oracle itself trips the same +11% on current hardware — + predates this milestone, revert-foreign) recorded as a separate + **P2 roadmap `[todo]`** (bench-harness recalibration; no language + change), so it is tracked without being mis-attributed to the + revert or laundered through a ratify. + +## Fieldtest + +**Skipped** (Boss judgement; fieldtest is non-mandatory). A revert +restores the already-field-tested pre-`9973546` user-visible surface +(structural / tail recursion; `tail-app` intact) — the surface that +the mut-local fieldtest already exercised and that started this +corrective arc. A fieldtest here would re-test a known, well-trodden +state and add no signal; the implement Task-11 byte-equivalence +sweep over 164 fixtures is the stronger correctness proof for a +revert. + +## Close + +Milestone **iteration-discipline-revert** closed clean: +byte-pristine vs `1ff7e81` across all production surface; behaviour +byte-identical over 164 surviving fixtures; `cargo test --workspace` +600/0; one roadmap drift fixed inline; the single `check.py` metric +localised to environmental variance (baseline untouched) with the +pre-existing staleness filed forward. AILang's iteration story is +exactly the pre-`9973546` state; the genuine total-recursion +ambition is preserved on the roadmap, sequenced behind a future +`Nat`/refinement-types milestone. diff --git a/docs/journals/INDEX.md b/docs/journals/INDEX.md index c5f2a02..4d80ea0 100644 --- a/docs/journals/INDEX.md +++ b/docs/journals/INDEX.md @@ -79,3 +79,4 @@ - 2026-05-15 — iter it.2: iteration-discipline milestone (2 of 3) — structural-recursion guardedness checker + first real `Diverge` effect, strictly additive (nothing `tail`-related removed; that is it.3). New whole-body pass `verify_structural_recursion` runs as a sibling of `verify_tail_positions` in `check_fn`'s post-synth region (DD-1): the `smaller`-set algorithm with implicit candidate-position inference + unconstrained accumulator positions (DD-2 — foldl-shape accumulator classifies as structural recursion, pure+total), self/mutual identification with an inline ADT-family connected-components union-find (DD-3), and the it.2-only `tail==false` grandfather. `CheckError::NonStructuralRecursion {callee,arg}` (bracket-`[code]`-free Display per F2). `term_contains_loop` (stops at `Term::Lam` boundaries, DD-4) injects `"Diverge"` into the raised effect set so the existing `UndeclaredEffect` machinery enforces it with no new diagnostic variant; lam-arrow + `Term::LetRec` sub-effect sites wired (loop behind a lam edge carries `!Diverge` on the lam's arrow, propagating via the free callee-effect path, not leaking to the enclosing fn — exactly as `!IO` scopes). DESIGN.md Decision 3 + §Data-model hook synced present-tense. Four it.1 loop fixtures gained `!Diverge`. Two spec-premise boundary defects surfaced and resolved inside the task's invariants (corpus clean, check not weakened): (§1) the spec's "21 tail-app fixtures" grandfather premise under-counts the corpus — no-ADT-candidate counter recursions (~18, e.g. `build_tree(depth:Int)`) have no structural position to verify and are deferred to it.3 migration; (§2) two RC-regression fixtures (`rc_pin_recurse_implicit`, `rc_let_alias_implicit_param`) hold an ADT param constant while decrementing an Int — genuinely non-structural, joined the spec's transitional `tail-app` grandfather exactly as the other 20 corpus fixtures do (their RC==GC regression guards verified still green; the regression lives in the unchanged `pin`/`pin_aliased` bodies). Both recorded as corrected it.3 corpus-migration scope. `cargo test --workspace` 622 green / 0 red; all 9 acceptance pins non-vacuous (negatives `.contains(code)`); struct_rec_sum→15, loop_needs_diverge→55, the it.1 55/49 e2e still green → 2026-05-15-iter-it.2.md - 2026-05-15 — iter it.3 (BLOCKED, bounce-back): destructive terminal iteration of iteration-discipline. Task 1 (non-destructive: pre-migration oracle + the spec-delegated class-(b) live sweep) ran complete — 40 recursive corpus fixtures classified + oracled under `bench/it3-oracle/`; zero production code changed; HEAD clean at c992eb9. The mandated Task-1.3 sweep surfaced a **fundamental milestone-design flaw**, not a migration nuisance: 6 fixtures contain `build(d: Int) = if d==0 then Leaf else Node(1, build(d-1), build(d-1))` — a terminating, maximally-LLM-natural, **non-structural (Int param, no ADT-candidate) non-tail BRANCHING (double) recursion** that the milestone's totality dichotomy ("structural-over-ADT OR loop/recur, else error") makes **inexpressible**: not ADT-structural, and not `recur`-able (branching ≠ single tail back-edge). Post-it.3 it is a hard `NonStructuralRecursion` with no expressible alternative — the milestone as-specified would fail its own feature-acceptance criterion (clause 1: the LLM reaches for `build(d-1),build(d-1)`; clause 2: the milestone would *remove* expressivity). The orchestrator correctly refused a 4th plan-patch and bounced (`feedback_spec_over_plan_patches`). Boss verdict: the totality story overlooked a second canonical total-by-construction scheme — well-founded recursion on a strictly-decreasing non-negative Int measure. Resolution requires a new additive iteration **it.2b** (widen the it.2 guardedness checker to accept Int-bounded recursion incl. branching) BEFORE it.3 re-dispatches; the purity sub-fork (Int≠Nat: total only for non-negative entry) touches the user-co-designed purity pillar → user design decision, recommended option A1 (accept with a documented non-negative-entry obligation, analogous to array-bounds). Notify sent; loop stopped. The RC-RSS/18g.1 load-bearing risk (it.3 Task 5.5/5b) was NOT reached and must NOT be treated as resolved by the milestone-close audit → 2026-05-15-iter-it.3.md - 2026-05-16 — iter revert: Iteration-discipline milestone (it.1 `96db54d` + it.2 `a4be1e5`) fully backed out by one **forward** iteration (`main` sacrosanct — never rewound; `1ff7e81`, the pre-`9973546` commit, is the per-region byte oracle). Root cause: the milestone was an over-escalation of fieldtest finding F1 (a `[friction]` item whose own minimal recommendation was a DESIGN.md note); its totality dichotomy made the maximally-LLM-natural `build(d:Int)=Node(1,build(d-1),build(d-1))` inexpressible (it.3 BLOCKED), and the only in-thesis escape (A1/it.2b) conceded the language's first documented-unenforced totality precondition — a purity-pillar dilution the user rejected. `Term::Loop`/`Term::Recur`/`LoopBinder`, the `verify_structural_recursion` guardedness pass + `term_contains_loop` + `Diverge`-injection + the transitively-it.2 `module_fns` plumbing, the five `Recur*`/`NonStructuralRecursion` `CheckError` variants (+ `code()` + 3 dedicated `ctx()` arms), the it.1 codegen loop-header/phi/back-edge + parallel `block_terminated` setter, and all walker arms are removed — `crates/ailang-check/src/lib.rs` and every reverted source/test file byte-identical to `1ff7e81`. Surgical keeps: feature-acceptance **clause 3** (DESIGN.md + brainstorm SKILL.md, worked example de-claimed "shipped"→hypothetical) and the F3 P2 todo. Sole net addition: an honest F1/F4 documented-idiom note (tail-recursive accumulator fallback; `examples/mut_counter.ail`) guarded by a doc-presence test. 16 it.1/it.2 fixtures + 2 pin files + `bench/it3-oracle/` deleted; 2 RC fixtures restored to `1ff7e81`; `bench/orchestrator-stats/2026-05-15-iter-it.{1,2,3}.json` kept (historical record). Roadmap: Iteration-discipline block + blocking-fork section removed; the genuine total-Int-recursion ambition preserved as a deferred P2 milestone sequenced behind a future `Nat`/refinement-types milestone (not abandoned — correctly sequenced). Correctness gate PRISTINE: 164 surviving `1ff7e81`-era fixtures `ail check`/`ail run` byte-identical to pre-milestone behaviour (1ff7e81 worktree reference compiler, zero drift); `cargo test --workspace` 600/0; zero residual it.1/it.2 production surface. The old it.* journals/plans + the superseded-headered `2026-05-15-iteration-discipline.md` stay as historical record → 2026-05-16-iter-revert.md +- 2026-05-16 — audit iteration-discipline-revert (milestone close, clean): architect confirmed the revert byte-pristine (18 src + 5 test files byte-identical to `1ff7e81`, zero residual it.1/it.2 production surface, DESIGN.md coherent, roadmap/spec hygiene correct); one `[medium]` drift — a dangling `loop`/`recur` cross-reference into the reverted milestone inside the *live* Stateful-islands roadmap scope bullet — fixed inline (Boss doc-hygiene; reworded to keep the real "no `while`; repetition stays recursion" scope guard, drop the reverted-milestone reference). Bench: `compile_check.py`/`cross_lang.py` exit 0; `check.py` exit 1 on the single metric `bench_list_sum.bump_s` +12.71%. Bencher localisation: HEAD and `1ff7e81` bump binaries `cmp`-identical, interleaved 3×60-run measurement shows head−oracle delta ~0 (±1.5% stdev) with *both* ~+11% over the 2026-05-09 baseline → environmental/hardware drift, NOT a revert regression (third independent proof codegen == `1ff7e81`). Resolution: carry-on, baseline NOT ratified (Iron Law — nothing intentionally moved the metric; byte-identical codegen must not move the baseline; the spec's PRISTINE mandate is satisfied because pristine = "no regression introduced", proven). Pre-existing `*.bump_s` baseline-vs-hardware staleness (the `1ff7e81` oracle trips the same +11%) filed forward as a separate P2 `[todo]` (bench-harness recalibration, no language change), not mis-attributed to the revert. Fieldtest skipped (revert restores the already-field-tested pre-`9973546` surface; Task-11 164-fixture byte-equivalence is the stronger proof). Milestone closed clean → 2026-05-16-audit-iteration-discipline-revert.md diff --git a/docs/roadmap.md b/docs/roadmap.md index 0c18a4c..6ae8a15 100644 --- a/docs/roadmap.md +++ b/docs/roadmap.md @@ -270,6 +270,22 @@ clean. Pick the next milestone from P2.)_ - context: fieldtest 2026-05-11 — fieldtest fixtures could not be placed under `examples/fieldtest/` because of this; predates the canonical-type-names milestone but surfaces every time. +- [ ] **\[todo\]** `*.bump_s` throughput baseline is stale vs current + hardware — `bench/check.py`'s `throughput.*.bump_s` family (the + fastest, most jitter-prone metrics) reads ~+5–13% over + `bench/baseline.json` on the current machine. Localised at the + iteration-discipline-revert audit (2026-05-16): an interleaved + 3×60-run measurement of `bench_list_sum` bump_s built from the + byte-oracle commit `1ff7e81` shows the *same* ~+11% elevation as + HEAD, and the two bump binaries are `cmp`-identical — so this is + environmental drift relative to the 2026-05-09 baseline-capture + machine state, **not** a codegen regression. Re-capture the full + `*.bump_s` set on current hardware from a known-clean commit and + recalibrate the `bump_s` baseline+tolerance pair (or widen the + tolerance) so the noise floor stops tripping `check.py` exit 1. + Pure bench-harness recalibration; no language change. + - context: `docs/journals/2026-05-16-audit-iteration-discipline-revert.md` + (the bencher localisation evidence). - [x] **\[todo\]** `check_in_workspace` per-module overlay narrowing — `crates/ailang-check/src/lib.rs:1234` still clears+rebuilds `env.ctor_index` per-module; ct.3.2 narrowed the analogous mono @@ -345,10 +361,11 @@ clean. Pick the next milestone from P2.)_ the effect-handler infrastructure forward. - `mut` block as the syntactic boundary in Form A — outside, AILang's pure self; inside, `var` / `assign` / mutable arrays - legal. (Iteration is *not* part of this boundary: the "Iteration - discipline" P1 milestone supersedes the earlier "while-loops - legal" scope here — repetition is structural recursion or named - `loop`/`recur`, never a `while` over mutable state.) + legal. (Iteration is *not* part of this boundary: AILang has no + `while`/`for` and this milestone does not introduce one — + repetition stays recursion, exactly as the language has it today + (structural / tail recursion); a `mut` block is a sealed + expression, never a loop over mutable state.) - `var x = expr` + `assign x expr` AST nodes, legal only inside `mut`. - Mutable array primitive (`MutArray a`, O(1) index/update under