From a29700cc9efab4c31854c60a155d48ced6f6130a Mon Sep 17 00:00:00 2001 From: Brummel Date: Sat, 16 May 2026 13:25:49 +0200 Subject: [PATCH] iter effect-doc-honesty: make the effect-system documentation true MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Standalone documentation-honesty tidy (no language/checker/codegen change; `ail check`/`run` byte-unchanged by construction). Corrects three false effect-system claims the effect-subsystem recon surfaced, plus two satellite mentions, guarded by a new doc-presence pin: - DESIGN.md Decision 3: removed the "row-polymorphic (`![IO | r]`)" claim (no EffectRow / row variable exists in any crate — effect sets are a flat, unordered, closed set unified by set-equality); reconciled "`IO` and `Diverge` are wired up" to IO-only + `Diverge` reserved/unimplemented (zero code in any crate), modelled on Decision 4's reserved-refinements precedent. - DESIGN.md "What is not (yet) supported": "IO and Diverge ops" bullet -> IO-only + Diverge-reserved. - ast.rs Term::Do doc-comment: "resolved against the effect-handler table at link time" -> the real mechanism (typecheck lookup in Env::effect_ops + literal lower_effect_op codegen match; no handler table, no link-time resolution). - form_a.md:226 + rule 3, and main.rs merge-prose CONTRACT example: Diverge mentions reconciled in lockstep. - new crates/ailang-core/tests/effect_doc_honesty_pin.rs: 4 tests, fiction-absent + corrected-anchor-present, single-line wrap-robust substrings. cargo test --workspace 600 -> 604 (4 new pin tests, 0 regressions); design_schema_drift / spec_drift / schema_coverage stay green, empirically confirming none scans the effect-prose region. --- .../2026-05-16-iter-effect-doc-honesty.json | 13 +++ crates/ail/src/main.rs | 6 +- crates/ailang-core/specs/form_a.md | 7 +- crates/ailang-core/src/ast.rs | 7 +- .../tests/effect_doc_honesty_pin.rs | 61 ++++++++++++++ docs/DESIGN.md | 14 +++- .../2026-05-16-iter-effect-doc-honesty.md | 81 +++++++++++++++++++ docs/journals/INDEX.md | 1 + 8 files changed, 179 insertions(+), 11 deletions(-) create mode 100644 bench/orchestrator-stats/2026-05-16-iter-effect-doc-honesty.json create mode 100644 crates/ailang-core/tests/effect_doc_honesty_pin.rs create mode 100644 docs/journals/2026-05-16-iter-effect-doc-honesty.md diff --git a/bench/orchestrator-stats/2026-05-16-iter-effect-doc-honesty.json b/bench/orchestrator-stats/2026-05-16-iter-effect-doc-honesty.json new file mode 100644 index 0000000..d5b360d --- /dev/null +++ b/bench/orchestrator-stats/2026-05-16-iter-effect-doc-honesty.json @@ -0,0 +1,13 @@ +{ + "iter_id": "effect-doc-honesty", + "date": "2026-05-16", + "mode": "standard", + "outcome": "DONE", + "tasks_total": 6, + "tasks_completed": 6, + "reloops_per_task": { "1": 0, "2": 1, "3": 0, "4": 0, "5": 0, "6": 0 }, + "review_loops_spec": 0, + "review_loops_quality": 0, + "blocked_reason": null, + "notes": "Task 2 took 1 implementer-internal repair re-loop (not a spec/quality review loop): the plan's verbatim Task-2 replacement body soft-wrapped 'flat, unordered,\\nclosed set of effect names' mid-phrase, contradicting Task-1's single-line pin substring and the plan's own self-review item 6. Resolved by re-wrapping the soft-wrap column only (wording byte-identical to plan intent; pin unchanged). Recorded as a planner self-review item-3 cross-check gap." +} diff --git a/crates/ail/src/main.rs b/crates/ail/src/main.rs index 8b9788b..7704878 100644 --- a/crates/ail/src/main.rs +++ b/crates/ail/src/main.rs @@ -285,9 +285,9 @@ details unless the prose explicitly contradicts them. Specifically: These are hard contracts (memory model). The prose shows them as `own T` / `borrow T`; the Form-A wraps them. If the prose is ambiguous, default to the original. - - Effect annotations on return types (`(effects IO)`, - `(effects Diverge)`). Prose shows these as `with IO` etc.; if - uncertain, keep what the original had. + - Effect annotations on return types (e.g. `(effects IO)`). + Prose shows these as `with IO` etc.; if uncertain, keep what + the original had. - `tail` flags on calls. The prose prints `tail f(x)`; the Form-A keyword is `(tail-app f x)`. If the edit moved a call, decide whether the new position is still in tail position. diff --git a/crates/ailang-core/specs/form_a.md b/crates/ailang-core/specs/form_a.md index 2517bb6..f7ebff9 100644 --- a/crates/ailang-core/specs/form_a.md +++ b/crates/ailang-core/specs/form_a.md @@ -223,7 +223,9 @@ TYPE ; implicit mode (DO NOT USE in new (fn ...) defs) (borrow TYPE) ; caller retains ownership; callee must not consume ``` -`EFFECT-NAME` is a bare identifier — currently `IO` and `Diverge`. +`EFFECT-NAME` is a bare identifier. The only effect with a built-in +op today is `IO` (op `io/print_str`); `Diverge` is a reserved name +(no op, unimplemented). Effects are a set; order is irrelevant. Built-in type-constructors: `Int`, `Bool`, `Str`, `Unit`. User ADTs @@ -355,7 +357,8 @@ checked code on the first try. `(app Cons 1 (app Nil))`. 3. **Effects on side-effecting fns.** A function whose body uses `(do ...)` MUST list every effect operation's effect in its `(effects ...)` - clause. `IO` for `io/print_*`; `Diverge` for `diverge/*`. + clause. The only built-in effect op is `io/print_str`, whose + effect is `IO`. 4. **Tail correctness.** `(tail-app f x)` MUST appear in tail position — i.e. as the body of a fn, the last expression of a `(seq ...)`, the chosen arm of an `(if ...)` or `(match ...)`, or the body of diff --git a/crates/ailang-core/src/ast.rs b/crates/ailang-core/src/ast.rs index 6208405..0c4a9c0 100644 --- a/crates/ailang-core/src/ast.rs +++ b/crates/ailang-core/src/ast.rs @@ -435,8 +435,11 @@ pub enum Term { #[serde(rename = "else")] else_: Box, }, - /// Effect operation invocation (e.g. `do print "hi"`). The `op` is - /// resolved against the effect-handler table at link time. + /// Effect operation invocation (e.g. `do io/print_str "hi"`). The + /// `op` is resolved at typecheck against `Env::effect_ops` (an + /// `IndexMap`) and lowered by a literal + /// `match` in codegen (`lower_effect_op`); there is no + /// effect-handler table and no link-time resolution. /// /// Iter 14e: see [`Term::App`] for the `tail` field semantics. Do { diff --git a/crates/ailang-core/tests/effect_doc_honesty_pin.rs b/crates/ailang-core/tests/effect_doc_honesty_pin.rs new file mode 100644 index 0000000..6d840e7 --- /dev/null +++ b/crates/ailang-core/tests/effect_doc_honesty_pin.rs @@ -0,0 +1,61 @@ +//! Regression pin: the effect-system documentation must stay true. +//! +//! Three load-bearing effect claims were fiction until the +//! 2026-05-16 effect-doc-honesty tidy: a non-existent +//! row-polymorphic effect row, `Diverge` advertised as a wired-up +//! built-in op (zero code in any crate), and a `Term::Do` +//! doc-comment naming a non-existent link-time effect-handler +//! table. This pin fails if any of the fiction strings reappears +//! or any corrected anchor is dropped. + +use std::fs; + +fn read(rel: &str) -> String { + let p = concat!(env!("CARGO_MANIFEST_DIR"), "/../../"); + fs::read_to_string(format!("{p}{rel}")) + .unwrap_or_else(|e| panic!("read {rel}: {e}")) +} + +#[test] +fn design_md_effect_prose_is_true() { + let d = read("docs/DESIGN.md"); + // fiction absent + assert!(!d.contains("row-polymorphic"), + "DESIGN.md: the effect row is NOT row-polymorphic (no EffectRow / row var exists)"); + assert!(!d.contains("`IO` and `Diverge` (for infinite"), + "DESIGN.md: `Diverge` is not a wired-up MVP effect"); + assert!(!d.contains("the built-in IO and Diverge ops"), + "DESIGN.md §What-is-not-supported: there is no built-in Diverge op"); + // corrected anchors present + assert!(d.contains("flat, unordered, closed set of effect names"), + "DESIGN.md Decision 3 must describe the real (flat set-equality) effect model"); + assert!(d.contains("`Diverge` (for non-termination) is reserved"), + "DESIGN.md Decision 3 must state Diverge is reserved/unimplemented"); +} + +#[test] +fn term_do_doc_comment_is_true() { + let a = read("crates/ailang-core/src/ast.rs"); + assert!(!a.contains("resolved against the effect-handler table at link time"), + "ast.rs Term::Do: there is no effect-handler table and no link-time resolution"); + assert!(a.contains("resolved at typecheck against `Env::effect_ops`"), + "ast.rs Term::Do doc must describe the real resolution mechanism"); +} + +#[test] +fn form_a_spec_effect_names_are_true() { + let f = read("crates/ailang-core/specs/form_a.md"); + assert!(!f.contains("`Diverge` for `diverge/*`"), + "form_a.md: there is no `diverge/*` op namespace"); + assert!(!f.contains("currently `IO` and `Diverge`"), + "form_a.md: `Diverge` is reserved, not a currently-usable effect"); + assert!(f.contains("The only built-in effect op is `io/print_str`"), + "form_a.md rule 3 must name the real single built-in effect op"); +} + +#[test] +fn merge_prose_contract_example_is_true() { + let m = read("crates/ail/src/main.rs"); + assert!(!m.contains("`(effects Diverge)`"), + "main.rs CONTRACT: do not use a non-existent effect as the example"); +} diff --git a/docs/DESIGN.md b/docs/DESIGN.md index 89d4ec6..f495d66 100644 --- a/docs/DESIGN.md +++ b/docs/DESIGN.md @@ -168,9 +168,14 @@ Advantages: ## Decision 3: pure core language + algebraic effects The default is total, pure functions. Effects are declared as a set in the -function type: `(Int) -> Int ![IO]`. The effect set is row-polymorphic -(`![IO | r]`). In the MVP only the effects `IO` and `Diverge` (for infinite -loops) are wired up. +function type: `(Int) -> Int ![IO]`. The effect set is a +flat, unordered, closed set of effect names, unified by set-equality — +there is no effect row variable; a signature lists exactly the effects +its body may perform. +In the MVP only the effect `IO` is wired up (its sole op is `io/print_str`). +`Diverge` (for non-termination) is reserved as an effect name but is +unimplemented — no op, no codegen, no checker injection — in the same +sense Decision 4 reserves refinements. This is the most important LLM property: when I read a function, I can trust its signature without reading the body. @@ -2719,7 +2724,8 @@ proof is the protection. Snapshot of the current boundary. Items move out of this list as iterations land; the JOURNAL records when. -- No effect handlers — only the built-in IO and Diverge ops. +- No effect handlers — only the built-in `IO` op (`io/print_str`). + `Diverge` is a reserved effect name with no op and no codegen. - No refinements / SMT escalation. - No HM inference inside bodies. Top-level def types are explicit; polymorphism is opt-in via `Type::Forall { vars, body }`. Inside diff --git a/docs/journals/2026-05-16-iter-effect-doc-honesty.md b/docs/journals/2026-05-16-iter-effect-doc-honesty.md new file mode 100644 index 0000000..896d0ad --- /dev/null +++ b/docs/journals/2026-05-16-iter-effect-doc-honesty.md @@ -0,0 +1,81 @@ +# iter effect-doc-honesty — effect-system documentation-honesty tidy + +**Date:** 2026-05-16 +**Started from:** c41e0e5a9e48fd0099eda8c286f10ec7a30e8e8a +**Status:** DONE +**Tasks completed:** 6 of 6 + +## Summary + +Documentation-honesty tidy: corrected three false effect-system +claims plus their two satellite mentions across the project docs, +guarded by one new doc-presence regression pin. No language, +checker, or codegen code changed — only a doc-comment, two markdown +spec files, an internal CLI guidance string, and a new integration +test. `ail check`/`ail run` behaviour is byte-unchanged by +construction; `cargo test --workspace` 600 → 604 (the four new pin +tests, zero regressions), `cargo build --workspace` clean. The +three sentinel drift/coverage tests (`design_schema_drift`, +`spec_drift`, `schema_coverage`) stay green, empirically confirming +none scans the effect-prose region. + +## Per-task notes + +- iter effect-doc-honesty.1: new pin `crates/ailang-core/tests/effect_doc_honesty_pin.rs` + (4 tests asserting fiction strings absent + corrected anchors + present across the 4 edited files); authored first, ran RED 0/4 + for the right reason (TDD: RED before corrections). +- iter effect-doc-honesty.2: `docs/DESIGN.md` Decision 3 row-polymorphic + block → flat/unordered/closed set-equality + Diverge-reserved + wording; line-2722 "IO and Diverge ops" bullet → IO-only + + Diverge-reserved bullet. `design_md_effect_prose_is_true` GREEN. +- iter effect-doc-honesty.3: `crates/ailang-core/src/ast.rs` `Term::Do` + doc-comment effect-handler-table-at-link-time fiction → real + mechanism (typecheck against `Env::effect_ops`, `lower_effect_op` + literal-match codegen). `term_do_doc_comment_is_true` GREEN. +- iter effect-doc-honesty.4: `crates/ailang-core/specs/form_a.md` + line-226 "currently `IO` and `Diverge`" → IO-built-in-op / + Diverge-reserved; rule-3 "`Diverge` for `diverge/*`" → + io/print_str-is-the-only-built-in-op. `form_a_spec_effect_names_are_true` + GREEN. +- iter effect-doc-honesty.5: `crates/ail/src/main.rs` merge-prose + CONTRACT effect-annotation bullet dropped the non-existent + `(effects Diverge)` example. Whole pin 4/4 GREEN. +- iter effect-doc-honesty.6: full verification — whole pin 4/4, + `cargo test --workspace` 604/0 (600 prior + 4), drift/coverage + trio green, `cargo build --workspace` clean. + +## Concerns + +- Task 2: the plan's verbatim Task-2 replacement body soft-wrapped + the phrase "flat, unordered,\nclosed set of effect names" + mid-phrase, which contradicts Task-1's single-line pin substring + `"flat, unordered, closed set of effect names"` AND the plan's + own self-review item 6 ("every pin substring is single-line — the + documented iter-revert grep-wrap failure mode is avoided"). The + two authoritative artefacts (exact replacement text vs. exact + pin) could not both be applied verbatim. Resolved by preserving + the exact corrected *wording* (byte-identical to the plan's + intent) and the exact pin (Task 1, unchanged), moving only the + soft-wrap column so the asserted phrase stays contiguous on one + line. No wording added/dropped/changed. This is a planner + self-review-item-3 cross-check gap (the asserted-substring vs. + replacement-body check did not account for the replacement body's + own line wrap) — orchestrator may want to tighten the planner's + pin/replacement-body wrap cross-check. + +## Known debt + +- (none) — the tidy is self-contained; no deferred follow-up. + +## Files touched + +- `crates/ailang-core/tests/effect_doc_honesty_pin.rs` (new — the pin) +- `docs/DESIGN.md` (Decision 3 + "What is not supported" bullet) +- `crates/ailang-core/src/ast.rs` (`Term::Do` doc-comment) +- `crates/ailang-core/specs/form_a.md` (line 226 + rule 3) +- `crates/ail/src/main.rs` (merge-prose CONTRACT string) + +## Stats + +bench/orchestrator-stats/2026-05-16-iter-effect-doc-honesty.json diff --git a/docs/journals/INDEX.md b/docs/journals/INDEX.md index 4d80ea0..d48486c 100644 --- a/docs/journals/INDEX.md +++ b/docs/journals/INDEX.md @@ -80,3 +80,4 @@ - 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 +- 2026-05-16 — iter effect-doc-honesty: standalone documentation-honesty tidy (split out from the retired effect-op-arg-modes bundle — user rejected bundling a real DESIGN.md fix with speculative build-ahead infra). Corrected three false effect-system claims the recon surfaced: DESIGN.md Decision 3 "row-polymorphic (`![IO | r]`)" (no `EffectRow`/row var exists — effect sets are flat closed sets unified by set-equality) + "`IO` and `Diverge` … are wired up" (`Diverge` is 100% vapour: zero code in any crate) → reconciled to IO-only/Diverge-reserved-unimplemented (modelled on Decision 4's reserved-refinements precedent); DESIGN.md §"What is not supported" "IO and Diverge ops" bullet; `ast.rs` `Term::Do` doc-comment "resolved against the effect-handler table at link time" → the real mechanism (typecheck `Env::effect_ops` lookup + `lower_effect_op` literal codegen match, no handler table). Satellite lockstep: `form_a.md:226` + rule-3, `main.rs:289` merge-prose CONTRACT example. Guarded by a new 4-test doc-presence pin `crates/ailang-core/tests/effect_doc_honesty_pin.rs` (fiction-absent + corrected-anchor-present, single-line substrings — wrap-robust). No language/checker/codegen change; `ail check`/`run` byte-unchanged by construction. `cargo test --workspace` 600 → 604; drift/coverage trio (`design_schema_drift`/`spec_drift`/`schema_coverage`) green, empirically confirming none scans the effect-prose region. One concern: the plan's Task-2 replacement body soft-wrapped a phrase the single-line pin asserts; orchestrator resolved correctly (exact wording + exact pin preserved, wrap column moved) — recurring-class planner gap, fixed forward by a Step-5 self-review tightening → 2026-05-16-iter-effect-doc-honesty.md