iter env-unify.audit: tidy stale Env docs, pin-test docstring; queue types/ctor_index shape

crates/ailang-check/src/lib.rs

@@ -2503,15 +2503,18 @@ pub struct Env {
     /// (qualified cross-module reference).
     pub imports: BTreeMap<String, String>,
     /// Top-level symbol table per module of the workspace.
-    /// `check_in_workspace` populates this from `build_module_globals`.
+    /// Populated by [`crate::build_check_env`] from
+    /// [`build_module_globals`].
     pub module_globals: BTreeMap<String, IndexMap<String, Type>>,
     /// Per-module import map: module-name → (alias-or-module-name →
     /// actual-module-name). Sibling-shape to [`Self::module_globals`];
-    /// populated only by [`crate::mono::build_workspace_env`] so the
+    /// populated workspace-flat by [`crate::build_check_env`] so the
     /// mono pass's per-fn entry points can re-seed the local
-    /// [`Self::imports`] before re-running [`synth`] on a body.
-    /// `check_in_workspace` does not populate this — it has the module
-    /// in hand and seeds [`Self::imports`] directly.
+    /// [`Self::imports`] before re-running [`synth`] on a body. Both
+    /// `check_in_workspace` and `mono::build_workspace_env` consume
+    /// the same env shape; `check_in_workspace` then overwrites
+    /// [`Self::imports`] with the current module's map at the call
+    /// site.
     pub module_imports: BTreeMap<String, BTreeMap<String, String>>,
     /// Iter 15a: ADT type definitions per module of the workspace. Used
     /// to resolve qualified type references (`module.Type` in

crates/ailang-check/tests/env_construction_pin.rs

@@ -23,11 +23,14 @@ fn examples_dir() -> std::path::PathBuf {
         .join("examples")
 }
 
-/// In-test reproduction of the pre-refactor `check_in_workspace`
-/// workspace-flat seeding (the inline seeding that lived in
-/// `check_in_workspace` before this milestone). Kept as a frozen
-/// reference: any future divergence between this body and
-/// `build_check_env` makes the assertion below fail.
+/// Independent reproduction of every workspace-flat env seeding
+/// step. Pre-refactor, workspace-flat seeding was split between
+/// `check_in_workspace` (per-module `types`/`ctor_index`) and
+/// `mono::build_workspace_env` (workspace-flat `types`/`ctor_index`
+/// plus everything else); this reproduction captures the *union*
+/// — exactly the surface `build_check_env` is responsible for.
+/// Kept as a frozen reference: any future divergence between this
+/// body and `build_check_env` makes the assertion below fail.
 fn build_env_inline_pre_refactor(ws: &ailang_core::workspace::Workspace) -> Env {
     let mut env = Env::default();
     ailang_check::builtins::install(&mut env);

docs/JOURNAL.md

@@ -12117,3 +12117,42 @@ Known debt: none introduced. Out-of-scope items from the spec
 (pipeline-topology changes, per-module overlay refactor,
 primitive-name-set consolidation, new env fields) remain queued
 for separate milestones.
+
+## 2026-05-10 — Audit close: env-construction unify
+
+Architect drift review of diff `08abfdf..e414144` found three
+low-medium items. Bench gates 0/0/0; rustdoc 16→15 warnings (one
+removed by the milestone, none added); E2E coverage map produced
+by tester confirmed existing 345-test suite + pin tripwire pin
+every named invariant.
+
+Resolution:
+
+- `[medium]` Stale doc comment on `Env::module_imports`
+  (`crates/ailang-check/src/lib.rs:2508-2516`) said "populated only
+  by `mono::build_workspace_env`" and "`check_in_workspace` does
+  not populate this." Both clauses contradicted the post-unify
+  shape. Fixed inline as part of audit close (one-line
+  doc tidy). Same drift on `Env::module_globals` (line 2506)
+  fixed for consistency.
+- `[low]` Pin test docstring
+  (`crates/ailang-check/tests/env_construction_pin.rs:26-30`)
+  claimed it reproduced "the pre-refactor `check_in_workspace`
+  workspace-flat seeding," but pre-refactor `check_in_workspace`
+  seeded `types`/`ctor_index` per-module, not workspace-flat. The
+  test still pins `build_check_env` against an independent
+  reproduction (its real value); the comment misnamed what was
+  pinned. Fixed inline.
+- `[medium, queued]` `env.types.clear()` / `env.ctor_index.clear()`
+  immediately after `build_check_env` populates them
+  (`lib.rs:1187-1188`) is the visible scar of a deeper shape
+  mismatch: `types`/`ctor_index` are *per-module overlay* for
+  typecheck (`Pattern::Ctor`'s local-first / imports-fallback
+  resolution at lib.rs:2314-2316) but *workspace-flat* for the
+  mono pass. One field, two shapes. Not a fire (the wasteful
+  copy is small and bench gates are clean), but worth queuing
+  as a follow-up shape question for whichever iteration next
+  feels env-field pressure. Marker: "types/ctor_index overlay
+  shape" in the JOURNAL queue.
+
+Milestone closed: drift items 1 and 3 tidied; item 2 queued.