From c747cdf932bdeaf7289dac1263fcf55af08622ae Mon Sep 17 00:00:00 2001 From: Brummel Date: Tue, 2 Jun 2026 11:57:51 +0200 Subject: [PATCH] docs(ledger): fix two coherence gaps surfaced by the project skim MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit A read-only coherence skim across the project (the contract edits themselves verified code-true, INDEX bijection exact, all pins green) surfaced two pre-existing drifts — both predating this audit, neither from the contract pass. Fixed in the same conservative style. 1. Model 0008 (ownership-totality) §1+§2 narrated the `Implicit` leak in the PRESENT tense, contradicting the file's own STATUS header (Implicit deleted via #55, 76b21c0), contract 0008 ("There is no `Implicit`"), and the live fixture. §1 claimed "This is documented intentional behaviour today ... the fixture asserts `live = 1`"; the `rc_let_implicit_returning_app.ail` fixture now asserts `live = 0` (its own comment marks the `live = 1` lane as "Pre-0062"). §2 claimed "the typechecker already treats `Implicit ≡ Own` (`ParamMode::mode_eq`)"; that variant and fn no longer exist. Rewrote both to past tense (the leak the cutover fixed). The STATUS header had been updated at cutover; these two bodies had not. The design argument (§2-§8) is untouched — the header frames it as the whitepaper's reasoning and points readers to the contract for current state. 2. Contract 0010 (scope-boundaries) referenced 18 example fixtures as `examples/*.ail.json` — files that exist only as `.ail` since the form-A-default migration (JSON is derived in-process; only the twelve carve-outs remain `.ail.json` on disk). All 18 → `.ail` (every target verified present). Same single stale file-path ref in model 0001 §3 (`list_map_poly`) corrected; model 0001's other two `.ail.json` mentions are intentional references to the canonical JSON *form* (the whitepaper's subject) and were left. Honesty sweep clean; design_index_pin / docs_honesty_pin / effect_doc_honesty_pin green; no dangling example path remains. --- design/contracts/0010-scope-boundaries.md | 36 +++++++++++------------ design/models/0001-authoring-surface.md | 2 +- design/models/0008-ownership-totality.md | 35 +++++++++++----------- 3 files changed, 36 insertions(+), 37 deletions(-) diff --git a/design/contracts/0010-scope-boundaries.md b/design/contracts/0010-scope-boundaries.md index 6a112c1..8531e6c 100644 --- a/design/contracts/0010-scope-boundaries.md +++ b/design/contracts/0010-scope-boundaries.md @@ -101,12 +101,12 @@ What **is** supported (and used as the smoke test for the pipeline): cover `Int` / `Bool` / `Str` / `Unit`; `Float` lit-patterns are hard-rejected at typecheck (`CheckError::FloatPatternNotAllowed`, see [float-semantics](0005-float-semantics.md)). `(pat-lit "hi")` over - a `Str` scrutinee is exercised by `examples/eq_demo.ail.json`. + a `Str` scrutinee is exercised by `examples/eq_demo.ail`. - **Imports + qualified cross-module references** via dotted names. Extends to **types and constructors**: a foreign module's ADT is referenced as `(con std_pair.Pair a b)`, its ctors as `(term-ctor std_pair.Pair MkPair x y)` and `(pat-ctor MkPair x y)` - inside that scrutinee. Std-library demos (`examples/std_*_demo.ail.json`) + inside that scrutinee. Std-library demos (`examples/std_*_demo.ail`) exercise this end-to-end. - **AI-authoring text surface, form (A)** (see [authoring surface](0001-authoring-surface.md)). The `ailang-surface` @@ -127,7 +127,7 @@ What **is** supported (and used as the smoke test for the pipeline): "Per-fn arena via stack `alloca`" subsection of [RC + uniqueness](../models/0004-rc-uniqueness.md). The per-fn-arena path is exercised end-to-end by - `examples/escape_local_demo.ail.json`. + `examples/escape_local_demo.ail`. - **First-class function references.** A top-level fn name (or qualified `prefix.def`) used as a `Term::Var` is a fn-value. - **Anonymous lambdas with capture.** `Term::Lam` constructs a @@ -156,36 +156,36 @@ What **is** supported (and used as the smoke test for the pipeline): rather than a silent fallback to `ptr`. Pipeline regression smoke tests: -- `examples/sum.ail.json` → prints 55 (recursion, arithmetic). -- `examples/list.ail.json` → prints 42 (ADTs + match). -- `examples/hof.ail.json` → prints 42 (first-class fn-refs, indirect call). -- `examples/closure.ail.json` → prints 42 (lambda capturing a let-bound var). -- `examples/list_map.ail.json` → prints 2/4/6 (ADTs + closure + recursive +- `examples/sum.ail` → prints 55 (recursion, arithmetic). +- `examples/list.ail` → prints 42 (ADTs + match). +- `examples/hof.ail` → prints 42 (first-class fn-refs, indirect call). +- `examples/closure.ail` → prints 42 (lambda capturing a let-bound var). +- `examples/list_map.ail` → prints 2/4/6 (ADTs + closure + recursive HOF + IO; the dogfood smoke test). -- `examples/sort.ail.json` → prints sorted [3,1,4,1,5,9,2,6,5,3,5] +- `examples/sort.ail` → prints sorted [3,1,4,1,5,9,2,6,5,3,5] one-per-line (insertion sort over an 11-element list). -- `examples/poly_id.ail.json` → prints 42 then "true" (polymorphic +- `examples/poly_id.ail` → prints 42 then "true" (polymorphic identity at `Int` and `Bool`; two specialised fns emitted). -- `examples/poly_apply.ail.json` → prints 42 (polymorphic `apply` +- `examples/poly_apply.ail` → prints 42 (polymorphic `apply` with a fn-typed parameter; `apply(succ, 41)`). -- `examples/box.ail.json` → prints 42 (parameterised ADT round- +- `examples/box.ail` → prints 42 (parameterised ADT round- trip: `MkBox(42)` constructed, then projected by a polymorphic `unbox : forall a. (Box) -> a` and printed). -- `examples/maybe_int.ail.json` → prints 7 then 99 (pattern match +- `examples/maybe_int.ail` → prints 7 then 99 (pattern match over `Maybe`: `or_else(Some(7), 99)` then `or_else(None, 99)`). -- `examples/std_list_demo.ail.json` → exercises +- `examples/std_list_demo.ail` → exercises `std_list`'s combinators (length, sum, reverse, take/drop-style uses) end-to-end against `std_list`'s `List`. -- `examples/std_maybe_demo.ail.json` → exercises `std_maybe` +- `examples/std_maybe_demo.ail` → exercises `std_maybe` combinators over `Maybe`, including `from_maybe` and `map`. -- `examples/std_either_demo.ail.json` → first program with +- `examples/std_either_demo.ail` → first program with three distinct type variables in a single fn (the `either` eliminator), monomorphised six different ways in the IR. -- `examples/std_pair_demo.ail.json` → drives every +- `examples/std_pair_demo.ail` → drives every `std_pair` combinator (fst, snd, swap, map_first, map_second); expected output 7, 9, 9, 7, 8, 18. -- `examples/nested_pat.ail.json` → first program to use a +- `examples/nested_pat.ail` → first program to use a nested `(pat-ctor Cons a (pat-ctor Cons b _))`; the desugar pass flattens it into a chain that the existing flat-match codegen consumes. Prints 30 for a 3-element input list. diff --git a/design/models/0001-authoring-surface.md b/design/models/0001-authoring-surface.md index 29fd3bb..51337e5 100644 --- a/design/models/0001-authoring-surface.md +++ b/design/models/0001-authoring-surface.md @@ -2,7 +2,7 @@ ## Candidate notations (same `map` encoded in each) -The reference target — the polymorphic `map` from `examples/list_map_poly.ail.json`: +The reference target — the polymorphic `map` from `examples/list_map_poly.ail`: ``` data List a where Nil | Cons a (List a) diff --git a/design/models/0008-ownership-totality.md b/design/models/0008-ownership-totality.md index 29a41ba..02f7a0a 100644 --- a/design/models/0008-ownership-totality.md +++ b/design/models/0008-ownership-totality.md @@ -33,21 +33,21 @@ the sharpened §7 questions, and §8 (relation to Rust).* --- -## 1. The leak that motivates it +## 1. The leak that motivated it -A user function whose return **type** is an RC-heap value (`Str`, or a -boxed ADT) but whose signature omits the ownership mode carries +A user function whose return **type** was an RC-heap value (`Str`, or a +boxed ADT) but whose signature omitted the ownership mode carried `ret_mode == ParamMode::Implicit` — the parser's silent default, which -nothing infers post-parse. Codegen reads `Implicit` faithfully: the -caller does **not** `dec` the returned slab, so the owned allocation -leaks (`live = 1` under `AILANG_RC_STATS`). This is documented -intentional behaviour today: `../contracts/0008-memory-model.md` states -`ret_mode` is author-required and never inferred, and the -`examples/rc_let_implicit_returning_app.ail` fixture asserts `live = 1` -as correct under the Implicit back-compat lane. +nothing inferred post-parse. Codegen read `Implicit` faithfully: the +caller did **not** `dec` the returned slab, so the owned allocation +leaked (`live = 1` under `AILANG_RC_STATS`). The #55 cutover removed +this lane: `../contracts/0008-memory-model.md` now requires an explicit +author-supplied `ret_mode`, and the +`examples/rc_let_implicit_returning_app.ail` fixture asserts `live = 0` +(the returned cell frees at the call site). -The leak is the symptom. The cause is that an ownership default exists -at all. +The leak was the symptom. The cause was that an ownership default +existed at all. ## 2. The principle: ownership is authored, never defaulted @@ -60,12 +60,11 @@ annotations are kept*; *machine readability over human readability*. the owner of a value crossing a signature boundary — and must free it — is **not recoverable from the type alone**: a `Str`-returning `own` and a `Str`-returning `borrow` are indistinguishable by type; only the -mode says who frees. The code makes this concrete: the typechecker -already treats `Implicit ≡ Own` (`ParamMode::mode_eq`, -`crates/ailang-core/src/ast.rs`), yet codegen reads `Implicit` -separately and omits the caller `dec`. The *same* fn-type is read two -ways depending on whether one knows codegen's special-casing — exactly -the trust break local reasoning exists to forbid. +mode says who frees. The code made this concrete: the typechecker +treated `Implicit ≡ Own`, yet codegen read `Implicit` separately and omitted the +caller `dec`. The *same* fn-type was read two ways depending on +whether one knew codegen's special-casing — exactly the trust break +local reasoning exists to forbid. So the principle is: **ownership is authored, never defaulted.**