From 625fe849befe66ef5c62efdb4d87f1b68862ec3f Mon Sep 17 00:00:00 2001 From: Brummel Date: Tue, 2 Jun 2026 11:14:01 +0200 Subject: [PATCH] docs(contracts): reconcile contracts + honesty-pin with shipped reality MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit First tranche of a contracts-against-code audit (the inverse of the usual direction: testing the ledger's claims against the code). Each fix here is a verified factual divergence between a contract and the code; the direction of the fix follows which side actually drifted. Code drifted from the stated goal -> fix the code: - 0014's claim 6 ("`cargo doc --no-deps` runs warning-free") was the design goal; reality had 6 warnings. Demote the offending intra-doc links to plain code spans so the docs match the goal: - ailang-core: `[`load_workspace`]` cannot resolve from core (the fn lives in ailang-surface, which core may not depend on) — three sites in workspace.rs. - ailang-check: three public-item docs linked the `pub(crate)` helpers `qualify_local_types` / `qualify_workspace_types`. `cargo doc --no-deps --workspace` is now warning-free. Contract stale, code legitimately advanced -> fix the contract: - 0011 stated `float_to_str` "codegen is reserved and not yet shipped". It is shipped: lowers to `@ailang_float_to_str(double)`, green under the codegen `float_to_str_no_longer_errors_internal` unit test and the e2e `float_to_str_smoke`. The docs_honesty_pin anchor that protected the stale "reserved" wording moved in lockstep to assert the present-tense lowering instead — the pin had been guarding a claim the code already falsified. - 0013 named the diagnostic `ConstraintReferencesUnboundTypeVar`; the variant is `UnboundConstraintTypeVar` (workspace.rs), and its scope is a class-method signature whose constraint mentions a tyvar bound neither by the method's `forall` nor by the class `param`. - 0017 called the primitive Eq/Ord bodies "placeholder lambdas"; they carry the `(intrinsic)` marker — the lockstep partner to the INTERCEPTS registry, not a placeholder. - 0009 said "seven" `.ail.json` carve-outs and described the inventory test as pinning seven; the test pins twelve (7 subject-matter + 4 recur + 1 loop-binder, per carve_out_inventory.rs). Verified separately: 0001's "pretty-printer code in pretty.rs was deleted, leaving only diagnostic helpers" is factually correct (an audit agent misread it as "pretty.rs was deleted"); its only issue is history phrasing, deferred to the honesty-prose tranche. Deferred to later tranches: honesty-rule prose (history/rationale that is not a protected honest-reserved/tiebreaker anchor), stale/mislinked ratifying-tests (0014's `architect_sweeps.sh`, 0015's uniqueness in-source tests), 0014's never-existent `tests/expected/`, 0012's non-exhaustive tail-context list, and the 0016<->0013 redundancy. --- crates/ailang-check/src/lib.rs | 6 +++--- crates/ailang-core/src/workspace.rs | 6 +++--- crates/ailang-core/tests/docs_honesty_pin.rs | 4 ++-- design/contracts/0009-roundtrip-invariant.md | 8 ++++---- design/contracts/0011-str-abi.md | 5 +++-- design/contracts/0013-typeclasses.md | 5 +++-- design/contracts/0017-prelude-classes.md | 7 ++++--- 7 files changed, 22 insertions(+), 19 deletions(-) diff --git a/crates/ailang-check/src/lib.rs b/crates/ailang-check/src/lib.rs index fe3a1dd..fa9be8e 100644 --- a/crates/ailang-check/src/lib.rs +++ b/crates/ailang-check/src/lib.rs @@ -1131,7 +1131,7 @@ pub fn check_module(m: &Module) -> Vec { /// 2. Normalize every consumer module's bare cross-module `Type::Con` /// references to qualified `.` form (so consumer-side /// declared types unify with imported-fn signatures, which the -/// existing [`qualify_local_types`] step already qualifies at the +/// existing `qualify_local_types` step already qualifies at the /// owner's side). /// /// Both [`check_workspace`] and [`monomorphise_workspace`] call this @@ -4844,11 +4844,11 @@ pub(crate) fn qualify_workspace_types( /// prep.1: walk a [`Module`] and rewrite every `Type` annotation /// (function signatures, const types, `Term::Lam.param_tys`/`ret_ty`, -/// `Term::LetRec.ty`) by applying [`qualify_workspace_types`]. Bare +/// `Term::LetRec.ty`) by applying `qualify_workspace_types`. Bare /// cross-module `Type::Con` names are upgraded to qualified /// `.` form so that consumer-side declared types unify /// against imported-fn signatures (which the existing -/// [`qualify_local_types`] step already qualifies on the owner side). +/// `qualify_local_types` step already qualifies on the owner side). pub fn qualify_workspace_module( mut m: Module, own_local_types: &IndexMap, diff --git a/crates/ailang-core/src/workspace.rs b/crates/ailang-core/src/workspace.rs index 603aac4..b121ad9 100644 --- a/crates/ailang-core/src/workspace.rs +++ b/crates/ailang-core/src/workspace.rs @@ -41,12 +41,12 @@ use std::path::{Path, PathBuf}; /// in; all imports are resolved relative to it. /// /// `registry` is the workspace-global -/// instance registry, built at the end of [`load_workspace`] after the +/// instance registry, built at the end of `load_workspace` after the /// DFS over imports completes. It is empty for any workspace whose /// modules contain no [`crate::ast::Def::Instance`] defs. #[derive(Debug, Clone)] pub struct Workspace { - /// Name of the entry module (the one passed to [`load_workspace`]). + /// Name of the entry module (the one passed to `load_workspace`). pub entry: String, /// Every module reachable from `entry`, indexed by module name. /// `BTreeMap` is used so iteration order is deterministic, which @@ -61,7 +61,7 @@ pub struct Workspace { /// workspace-global instance registry (the typeclass design). /// -/// Built at the end of [`load_workspace`] after all modules are +/// Built at the end of `load_workspace` after all modules are /// loaded. Keyed by `(class-name, canonical-type-hash)`; values are /// the matching [`crate::ast::InstanceDef`] plus the name of the /// module it was declared in. The hash key uses diff --git a/crates/ailang-core/tests/docs_honesty_pin.rs b/crates/ailang-core/tests/docs_honesty_pin.rs index e735079..02aa49a 100644 --- a/crates/ailang-core/tests/docs_honesty_pin.rs +++ b/crates/ailang-core/tests/docs_honesty_pin.rs @@ -120,8 +120,8 @@ fn design_md_present_tense_anchors_present() { assert!(memory.contains("a tiebreaker, not a rationale"), "the self-labelled tiebreaker is honest and stays in memory-model.md (do not over-strip)"); // corrected present-tense anchors - assert!(str_abi.contains("type-installed; codegen is reserved and not yet shipped"), - "float_to_str must be present-tense honest-reserved in str-abi.md"); + assert!(str_abi.contains("Lowers to `call ptr @ailang_float_to_str(double)`"), + "float_to_str is shipped — str-abi.md must state its lowering present-tense, not as reserved"); assert!(prelude_classes.contains("`io/print_str` is the only built-in direct-output effect-op"), "the print-op set must be stated present-tense in prelude-classes.md (post-split home), not as a retirement narrative"); } diff --git a/design/contracts/0009-roundtrip-invariant.md b/design/contracts/0009-roundtrip-invariant.md index 45db3bc..d20b0ab 100644 --- a/design/contracts/0009-roundtrip-invariant.md +++ b/design/contracts/0009-roundtrip-invariant.md @@ -28,9 +28,9 @@ Concretely: byte-identical to direct `ail parse` of the source `.ail`. Pins drift that crate-internal tests cannot see. -4. **Carve-out anchor.** Seven `.ail.json`-only fixtures - (subject-matter rejection tests) survive in the corpus by - structural necessity. They participate in their own dedicated +4. **Carve-out anchor.** Twelve `.ail.json`-only fixtures + (canonical-form / negative-typecheck rejection tests) survive in + the corpus by structural necessity. They participate in their own dedicated rejection-shape tests, not in the round-trip gate. (The prelude is embedded as `examples/prelude.ail` in `ailang-surface` and parsed at compile time via `ailang_surface::parse_prelude`.) @@ -74,7 +74,7 @@ inherit the gate automatically): variants fail compile until the visitor and corpus are extended in lockstep. - `crates/ailang-core/tests/carve_out_inventory.rs::examples_ail_json_inventory_matches_carve_outs` - — exactly the seven named carve-out files exist under + — exactly the twelve named carve-out files exist under `examples/*.ail.json` at any commit. A new `.ail.json` or a missing carve-out fails the test. diff --git a/design/contracts/0011-str-abi.md b/design/contracts/0011-str-abi.md index 37e96e6..72dcc7c 100644 --- a/design/contracts/0011-str-abi.md +++ b/design/contracts/0011-str-abi.md @@ -16,8 +16,9 @@ and backed by a `runtime/str.c` C helper. [prelude](0017-prelude-classes.md). - `bool_to_str : (borrow Bool) -> Str` — `"true"`/`"false"`. Backs `Show Bool` in the [prelude](0017-prelude-classes.md). -- `float_to_str : (borrow Float) -> Str` — - type-installed; codegen is reserved and not yet shipped. +- `float_to_str : (borrow Float) -> Str` — renders a `Float` to its + decimal string via libc `%g`. Lowers to + `call ptr @ailang_float_to_str(double)`. - `str_clone : (borrow Str) -> Str` — allocates a fresh heap-Str copy of the input's bytes. Backs `Show Str` in the [prelude](0017-prelude-classes.md). diff --git a/design/contracts/0013-typeclasses.md b/design/contracts/0013-typeclasses.md index ae90eb5..cbb8450 100644 --- a/design/contracts/0013-typeclasses.md +++ b/design/contracts/0013-typeclasses.md @@ -229,8 +229,9 @@ name overlap, via the `class-method-shadowed-by-fn` warning. See - `InvalidSuperclassParam` — superclass `type` differs from the class's own `param`. -- `ConstraintReferencesUnboundTypeVar` — a constraint mentions a - type variable not bound by the surrounding `forall`. +- `UnboundConstraintTypeVar` — a class method's signature carries a + constraint mentioning a type variable bound neither by the method's + `forall` nor by the class `param`. A class param appearing in applied position (e.g., `f a` where `f` is the class param) is rejected earlier by the canonical-form diff --git a/design/contracts/0017-prelude-classes.md b/design/contracts/0017-prelude-classes.md index 51d30bf..2182c00 100644 --- a/design/contracts/0017-prelude-classes.md +++ b/design/contracts/0017-prelude-classes.md @@ -6,9 +6,10 @@ The prelude ships the `Ordering` ADT, the `Eq` and `Ord` [classes](0013-typeclasses.md), primitive `Eq Int/Bool/Str/Unit` and `Ord Int/Bool/Str` instances, and the five polymorphic free-fn helpers `ne`/`lt`/`le`/`gt`/`ge`. The primitive `Eq` / `Ord` -instance bodies are placeholder lambdas in `examples/prelude.ail`; -the codegen intercept `try_emit_primitive_instance_body` overrides -them with single-instruction bodies (`icmp eq i64` for `eq__Int`, +instance bodies carry the `(intrinsic)` marker in `examples/prelude.ail` +(the marker is the lockstep partner to the `INTERCEPTS` registry); +the codegen intercept `try_emit_primitive_instance_body` supplies +their single-instruction bodies (`icmp eq i64` for `eq__Int`, `icmp eq i1` for `eq__Bool`, `@ail_str_eq` for `eq__Str`, `ret i1 1` for `eq__Unit`; a three-way `icmp` ladder constructing `LT`/`EQ`/`GT` for `compare__T`) and attaches `alwaysinline` so