convention: counter-prefix file naming across docs/specs/, docs/plans/, design/contracts/, design/models/

All 176 files in the four accumulating directories now use a
zero-padded 4-digit counter prefix that reflects creation order
(`NNNN-slug.md`). The counter is assigned per directory in strict
git-log creation order; ties broken alphabetically by original name.
The old `YYYY-MM-DD-` prefix on docs/specs/ and docs/plans/ files is
dropped — the date is recoverable from git log and the counter
carries the ordering.

A file's counter is stable for the life of the file: never reassigned,
never reused, never compacted. Deleted files retire their counter;
subsequent files do not fill the gap. This is the property that lets
cross-references stay literal — refs use the full filename including
the counter (`design/contracts/0007-honesty-rule.md`) so they grep
cleanly and resolve directly without a glob step.

313 cross-references updated across .md/.rs/.toml/.c/.json files
(test pins, include_str! paths, design-INDEX entries, baseline notes,
runtime C comments, inter-contract markdown links incl. bare basename
and `../models/foo.md` forms).

CLAUDE.md gets a new "File-naming convention" section spelling out
the rule and rationale. skills/brainstorm/SKILL.md and
skills/planner/SKILL.md updated so new spec/plan creation produces
counter-prefixed names from the start.

The full test suite (cargo test --workspace) passes.

design/contracts/0010-scope-boundaries.md

@@ -0,0 +1,193 @@
+# What is not (yet) supported
+
+## What is not (yet) supported
+
+Snapshot of the current boundary.
+
+- No effect handlers — only the built-in `IO` op (`io/print_str`);
+  the effect system is described in [effects](../models/0002-effects.md).
+  `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 }` (see
+  [Data model](0002-data-model.md)). Inside a body, lambdas check
+  monomorphically against their declared type.
+- Polymorphic fns must be **directly called** at the use site.
+  Passing a polymorphic fn as a value (`let f = id in f(42)`) is
+  not yet supported.
+- No higher-rank polymorphism. Passing a polymorphic fn to another
+  polymorphic fn (`apply(id, 42)`) is not supported.
+- No recursive `let` for non-fn values. Plain `let x = … in …` only
+  sees `x` inside the body, not inside its own RHS — recursive value
+  bindings would break the
+  [acyclicity invariant](0015-language-constraints.md). Recursive
+  *fn* bindings are supported via `Term::LetRec` (`{ "t": "letrec",
+  ... }`); the desugar pass lifts most occurrences to a synthetic
+  top-level fn, with `lift_letrecs` finishing the residue after
+  typecheck (see [pipeline](../models/0003-pipeline.md)).
+- No visibility rules in imports. Every top-level def of an imported module
+  is reachable; there is no `pub` / `priv`.
+
+What **is** supported (and used as the smoke test for the pipeline):
+
+- Int, Bool, Unit, **Str**, **Float** as primitive types.
+- `if`, `let`, function calls, recursion.
+- Effects on function signatures, with `do op(args)` for direct effect
+  ops (`io/print_str`). The polymorphic `print` (see
+  [prelude classes](0017-prelude-classes.md)) is the canonical output
+  path for non-Str values.
+- **Builtins.** Arithmetic operators (`+`, `-`, `*`, `/`) of type
+  `forall a. (a, a) -> a` (codegen-restricted to `{Int, Float}`);
+  `%` of type `(Int, Int) -> Int` (Int-only — `fmod` semantics for
+  Float deferred); polymorphic `neg : forall a. (a) -> a`
+  (codegen-restricted to `{Int, Float}`; Float arm uses LLVM
+  `fneg double` for correct `-0.0` handling); logical
+  `not : (Bool) -> Bool`; conversions
+  `int_to_float : (Int) -> Float`,
+  `float_to_int_truncate : (Float) -> Int` (saturating, NaN → 0),
+  `float_to_str : (Float) -> Str`,
+  `int_to_str : (Int) -> Str` (both allocate a heap-Str slab at
+  call time and return it with `ret_mode: Own`; see [Str ABI](0011-str-abi.md) for
+  the dual heap-/static-Str realisation); inspection
+  `is_nan : (Float) -> Bool` (LLVM
+  `fcmp uno`); Float bit-pattern constants `nan : Float`,
+  `inf : Float`, `neg_inf : Float` (resolved as bare values, lower
+  to direct hex-float `double` SSA constants at use site); the IO
+  effect op `io/print_str`; and **`__unreachable__ : forall a. a`**.
+  - **Equality + ordering** are not builtins. The class method
+    `eq` (`prelude.Eq`) dispatches via the per-type Eq instance;
+    the class method `compare` (`prelude.Ord`) dispatches via the
+    per-type Ord instance, returning a three-ctor `Ordering` ADT
+    (`LT` / `EQ` / `GT`). The five free helpers `ne` / `lt` /
+    `le` / `gt` / `ge` are defined in the prelude in terms of
+    `eq` / `compare`. The primitive Eq/Ord instance bodies are
+    emitted by the codegen intercept
+    `try_emit_primitive_instance_body`: Eq Int → `icmp eq i64`,
+    Eq Bool → `icmp eq i1`, Eq Str → `call @ail_str_eq(...)`,
+    Eq Unit → `ret i1 1`, Ord Int / Bool / Str → three-way
+    `icmp slt` / `icmp eq` ladder constructing the `Ordering`
+    ctor; every primitive instance body carries the
+    `alwaysinline` attribute so the call folds at every use site.
+    Float has no Eq / Ord instance (see
+    [Float semantics](0005-float-semantics.md)); explicit comparison
+    is via the named fns `float_eq` / `float_ne` / `float_lt` /
+    `float_le` / `float_gt` / `float_ge`, each lowering to a
+    single `fcmp` with the matching predicate. `float_ne` uses
+    `fcmp une double` (NOT `one`) so `nan != nan` returns `true`
+    per IEEE.
+  - **`__unreachable__`** is a polymorphic bottom value: a use of
+    `__unreachable__` typechecks against any expected type at
+    the use site and codegens to the LLVM `unreachable`
+    instruction (UB if ever executed). It is the chain
+    machinery's deepest fall-through for matches that the
+    typechecker proved exhaustive, and it is available to user
+    code as an explicit panic primitive
+    (`(if cond __unreachable__ ...)` for assertions or
+    impossible branches). Reference site is
+    `Term::Var { name = "__unreachable__" }` / form-A bare
+    `__unreachable__`.
+- **ADTs + pattern matching.** Sub-patterns of a Ctor pattern may be `Var`, `Wild`,
+  another `Ctor`, or a literal. The desugar pass flattens
+  nested Ctor patterns into a chain of let + match and rewrites every
+  `Pattern::Lit` (top-level or sub-) to a `Term::If` on `eq` (the
+  class method `prelude.Eq.eq`) before typecheck/codegen — see
+  [desugar](../../crates/ailang-core/src/desugar.rs) and
+  [Pipeline](../models/0003-pipeline.md).
+- Literal patterns at top level and inside Ctor sub-patterns (via desugar).
+  `(pat-lit 0)` and `(pat-ctor Cons (pat-lit 0) _)` both
+  parse and lower; the rewrite is to `Term::If { cond = (eq sv lit) }`,
+  so any literal kind whose `eq` dispatch resolves to a known
+  primitive Eq instance is authorable. The primitive instances
+  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`.
+- **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`)
+  exercise this end-to-end.
+- **AI-authoring text surface, form (A)** (see
+  [authoring surface](0001-authoring-surface.md)). The `ailang-surface`
+  crate parses `.ail` form-A text into a canonical
+  `ailang-core::ast::Module` and prints any module back as form-A
+  text. `ail render` and `ail describe` use it as the
+  sole text projection; `ail parse` is the inverse direction. Round-trip
+  identity (text → AST → JSON → AST → text) is gated by
+  `ailang-surface/tests/round_trip.rs` over every shipped fixture.
+- **Memory management via reference counting + uniqueness inference**
+  (see [RC + uniqueness](../models/0004-rc-uniqueness.md)), with
+  **per-fn arena via stack `alloca` for non-escaping allocations**
+  layered on top. Every ADT box, lambda env, and closure pair
+  allocates either via `@ailang_rc_alloc` (escaping; RC-managed
+  with inc/dec instrumentation per the memory model) or via LLVM
+  `alloca` (non-escaping; freed at fn return). The decision is
+  made by an escape-analysis pre-pass over the fn body — see the
+  "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`.
+- **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
+  closure that captures any free variables of its body from the
+  enclosing scope. All fn-values share a single ABI: a `ptr` to a
+  closure pair `{ thunk_ptr, env_ptr }`. Top-level fns get an auto-
+  generated adapter and a static closure pair (env = null) so they
+  remain passable as values without heap overhead.
+- **Polymorphism via `Type::Forall`** at top-level def types.
+  Use sites instantiate fresh metavars; unification pins them against
+  the concrete types of the call args. Codegen monomorphises on
+  demand: each unique instantiation emits a specialised LLVM fn
+  mangled `@ail_<m>_<def>__<descriptor>` (e.g. `id__I` for `id` at
+  `Int`, `apply__I_I` for `apply` at `(Int, Int)`).
+- **Parameterised ADTs.** `TypeDef.vars: Vec<String>`
+  declares type parameters; `Type::Con.args: Vec<Type>` carries the
+  type arguments at use sites. Both fields default to empty and are
+  skipped during serialization, so canonical-JSON hashes of every
+  existing definition stay bit-identical (regression test in
+  `crates/ailang-core/src/hash.rs`). Ctor and match codegen stay
+  inline at every use site — there is no specialised ADT symbol —
+  but LLVM field types are derived per use site by substituting
+  through `cdef.ail_fields`. The substitution is read off the call's
+  arg types (ctor) or the scrutinee's `Type::Con.args` (match). An
+  unresolved `Type::Var` reaching `llvm_type` is a hard error
+  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
+  HOF + IO; the dogfood smoke test).
+- `examples/sort.ail.json` → 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
+  identity at `Int` and `Bool`; two specialised fns emitted).
+- `examples/poly_apply.ail.json` → prints 42 (polymorphic `apply`
+  with a fn-typed parameter; `apply(succ, 41)`).
+- `examples/box.ail.json` → prints 42 (parameterised ADT round-
+  trip: `MkBox(42)` constructed, then projected by a polymorphic
+  `unbox : forall a. (Box<a>) -> a` and printed).
+- `examples/maybe_int.ail.json` → prints 7 then 99 (pattern match
+  over `Maybe<Int>`: `or_else(Some(7), 99)` then
+  `or_else(None, 99)`).
+- `examples/std_list_demo.ail.json` → exercises
+  `std_list`'s combinators (length, sum, reverse, take/drop-style
+  uses) end-to-end against `std_list`'s `List<a>`.
+- `examples/std_maybe_demo.ail.json` → exercises `std_maybe`
+  combinators over `Maybe<Int>`, including `from_maybe` and `map`.
+- `examples/std_either_demo.ail.json` → 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
+  `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
+  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.
+
+Ratified by: `crates/ailang-core/tests/effect_doc_honesty_pin.rs`.