feat(verify): human-readable error messages + grouped tw-verify output (refs #126 — source-line resolution defers to #129) (#159)

## Summary

Closes the prose-readability slice of #126: reword all `#[error(...)]`
templates and replace `tw-verify`'s `{:?}` debug-dump with a grouped,
location-anchored bulleted list.

## Changes

**lib.rs — error message rewording (Display-only; no API breaks)**

Pattern: `L<n> (<aspect>): <subject is X but should be Y>`.

| Variant | Old (excerpt) | New (excerpt) |
|---|---|---|
| `LinearUsedMultiple` | "Level 10 violation: function 0, param 0 —
Linear (own) param loaded 5 times on some path" | "L10 (linearity):
function #0 parameter #0 is a Linear (own) resource but is used 5 times
on some control-flow path; Linear resources must be consumed exactly
once (possible duplication)" |
| `ExclBorrowAliased` | "Level 7 violation: function 0, param 0 —
ExclBorrow (mut) param aliased (2 simultaneous references)" | "L7
(aliasing): function #0 parameter #0 is an ExclBorrow (&mut) reference
but 2 simultaneous borrows occur on some control-flow path; at most one
is permitted" |
| `ModuleNotIsolated` | "Level 13 violation: {reason}" | "L13 (module
isolation): {reason}" |
| `LinearImportCalledMultiple` | "Level 10 boundary violation: caller fn
7 calls import 'consume' 2 time(s)…" | "L10 (linearity, cross-module):
caller function #7 calls Linear import 'consume' 2 times on some
control-flow path; Linear imports must be called at most once on every
path" |
| `MissingDependentRegions` | "Level 2 violation: typedwasm.access-sites
section emitted without companion typedwasm.regions section
(MissingDependentCarrier)" | "L2 (region binding):
typedwasm.access-sites section is present but the companion
typedwasm.regions section is missing — access-site (region, field) keys
have nothing to resolve against" |

Same treatment for `LinearNotUsed`, `LinearDroppedOnSomePath`,
`LinearImportDroppedOnSomePath`, `CapabilitiesError::*`,
`AccessSiteError::*`.

**VerifyError Vec-wrappers**: replaced raw `{:?}` debug with a
`display_first_then_ellipsis` helper that renders as `"3 L7/L10/L13
ownership violation(s) — <first error's full Display>; … and 2 more"`.

**bin/tw-verify.rs — grouped output**

Replaces the previous flat `{:?}` / `{e}` printouts with grouping:

- `OwnershipError`s are bucketed by `func_idx` (with `(module-scope)`
bucket for L13). Per bucket, errors are sorted by `param_idx` and
printed as ` - <message>`.
- `CrossError`s are bucketed by `caller_func_idx`.
- L2 / L15 errors get an explicit `FAIL <pass> ({n} violation(s))`
header + bulleted list.

Sample output (before / after) — see commit message for details.

## Out of scope

Source-line resolution ("at `.twasm` line N") **defers to #129** (source
maps). The verifier still has only wasm-level indices today; the `#0`
parameter / `#N` function notation makes that boundary explicit in the
prose.

## Test plan

- [x] `cargo test -p typed-wasm-verify` — 65 lib tests pass (62 baseline
+ 3 new Display tests)
- [x] `cargo test -p typed-wasm-verify --all-features` — 80 lib + 10
cross-compat + 5 cross-compat-real all green
- [x] `cargo clippy -p typed-wasm-verify --all-features --tests` — no
new warnings (the pre-existing `collapsible-match` at `verify.rs:323`
remains; not mine)
- [x] No test compared raw error strings (all use `matches!` on
variants), so rewording is backwards-compatible for the test suite

Refs #126. Source-line resolution defers to #129.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

crates/typed-wasm-verify/src/bin/tw-verify.rs

@@ -1,4 +1,5 @@
 // SPDX-License-Identifier: MPL-2.0
+// Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 //
 // `tw-verify` — command-line front-end for the typed-wasm verifier.
 //
@@ -10,16 +11,14 @@
 //
 // Exit codes: 0 = verified, 1 = a check failed, 2 = usage / I/O error.
 //
-// This is the executable that makes "verifiable end-to-end by
-// `typed-wasm-verify`" a single command rather than a library call.
-// The in-tree producer `crates/typed-wasm-codegen` (`tw build`) already
-// self-verifies via `verify_from_module`; `tw-verify` is the standalone
-// front-end for checking a `.wasm` from any producer (incl. external /
-// third-party modules).
+// Diagnostic format (#126): violations are printed as a level-prefixed
+// bulleted list grouped by function-index, so a regression points at a
+// named function rather than a `[…]` debug-dump. Source-line resolution
+// ("at .twasm line N") defers to #129 (source maps).
 
 use std::process::ExitCode;
 
-use typed_wasm_verify::verify_from_module;
+use typed_wasm_verify::{verify_from_module, OwnershipError, VerifyError};
 
 fn main() -> ExitCode {
     let args: Vec<String> = std::env::args().collect();
@@ -54,8 +53,16 @@ fn main() -> ExitCode {
     // 2. L7 (aliasing) + L10 (linearity) + L13 (module isolation).
     match verify_from_module(&bytes) {
         Ok(()) => println!("ok  L7/L10/L13 ownership verification"),
+        Err(VerifyError::Ownership(errs)) => {
+            print_ownership_violations(&errs);
+            return ExitCode::FAILURE;
+        }
+        Err(VerifyError::Cross(errs)) => {
+            print_cross_violations(&errs);
+            return ExitCode::FAILURE;
+        }
         Err(e) => {
-            eprintln!("tw-verify: ownership verification FAILED: {e}");
+            eprintln!("tw-verify: verification error: {e}");
             return ExitCode::FAILURE;
         }
     }
@@ -65,7 +72,13 @@ fn main() -> ExitCode {
     match typed_wasm_verify::verify_access_sites_from_module(&bytes) {
         Ok(errs) if errs.is_empty() => println!("ok  L2 access-site verification"),
         Ok(errs) => {
-            eprintln!("tw-verify: access-site violations: {errs:?}");
+            eprintln!(
+                "FAIL L2 access-site verification ({} violation(s)):",
+                errs.len()
+            );
+            for e in &errs {
+                eprintln!("  - {e}");
+            }
             return ExitCode::FAILURE;
         }
         Err(e) => {
@@ -79,7 +92,13 @@ fn main() -> ExitCode {
     match typed_wasm_verify::verify_capabilities_from_module(&bytes) {
         Ok(errs) if errs.is_empty() => println!("ok  L15 capability verification"),
         Ok(errs) => {
-            eprintln!("tw-verify: capability violations: {errs:?}");
+            eprintln!(
+                "FAIL L15 capability verification ({} violation(s)):",
+                errs.len()
+            );
+            for e in &errs {
+                eprintln!("  - {e}");
+            }
             return ExitCode::FAILURE;
         }
         Err(e) => {
@@ -91,3 +110,74 @@ fn main() -> ExitCode {
     println!("VERIFIED {path}");
     ExitCode::SUCCESS
 }
+
+/// Group OwnershipErrors by their func_idx (or by "(module-scope)" for
+/// the L13 `ModuleNotIsolated` variant which has no func_idx), and print
+/// a bulleted list under each header. Within a function, errors are
+/// sorted by param_idx then by Display.
+fn print_ownership_violations(errs: &[OwnershipError]) {
+    use std::collections::BTreeMap;
+
+    let mut by_func: BTreeMap<String, Vec<&OwnershipError>> = BTreeMap::new();
+    for e in errs {
+        let key = match e {
+            OwnershipError::LinearNotUsed { func_idx, .. }
+            | OwnershipError::LinearDroppedOnSomePath { func_idx, .. }
+            | OwnershipError::LinearUsedMultiple { func_idx, .. }
+            | OwnershipError::ExclBorrowAliased { func_idx, .. } => format!("function #{func_idx}"),
+            OwnershipError::ModuleNotIsolated { .. } => "(module-scope)".to_string(),
+        };
+        by_func.entry(key).or_default().push(e);
+    }
+
+    eprintln!(
+        "FAIL L7/L10/L13 ownership verification ({} violation(s) in {} location(s)):",
+        errs.len(),
+        by_func.len()
+    );
+    for (loc, group) in &by_func {
+        eprintln!("  in {loc}:");
+        let mut sorted: Vec<&&OwnershipError> = group.iter().collect();
+        sorted.sort_by_key(|e| match e {
+            OwnershipError::LinearNotUsed { param_idx, .. }
+            | OwnershipError::LinearDroppedOnSomePath { param_idx, .. }
+            | OwnershipError::LinearUsedMultiple { param_idx, .. }
+            | OwnershipError::ExclBorrowAliased { param_idx, .. } => *param_idx,
+            OwnershipError::ModuleNotIsolated { .. } => 0,
+        });
+        for e in sorted {
+            eprintln!("    - {e}");
+        }
+    }
+}
+
+/// Group CrossErrors by caller_func_idx. Print bulleted list per caller.
+fn print_cross_violations(errs: &[typed_wasm_verify::CrossError]) {
+    use std::collections::BTreeMap;
+    use typed_wasm_verify::CrossError;
+
+    let mut by_caller: BTreeMap<u32, Vec<&CrossError>> = BTreeMap::new();
+    for e in errs {
+        let caller = match e {
+            CrossError::LinearImportCalledMultiple {
+                caller_func_idx, ..
+            }
+            | CrossError::LinearImportDroppedOnSomePath {
+                caller_func_idx, ..
+            } => *caller_func_idx,
+        };
+        by_caller.entry(caller).or_default().push(e);
+    }
+
+    eprintln!(
+        "FAIL L10 cross-module boundary verification ({} violation(s) in {} caller(s)):",
+        errs.len(),
+        by_caller.len()
+    );
+    for (caller, group) in &by_caller {
+        eprintln!("  in caller function #{caller}:");
+        for e in group {
+            eprintln!("    - {e}");
+        }
+    }
+}

crates/typed-wasm-verify/src/lib.rs

@@ -71,20 +71,20 @@ impl OwnershipKind {
 /// Mirrors OCaml `Tw_verify.ownership_error`.
 #[derive(Debug, Clone, PartialEq, Eq, Error)]
 pub enum OwnershipError {
-    #[error("Level 10 violation: function {func_idx}, param {param_idx} — Linear (own) param dropped on all paths (must be consumed exactly once)")]
+    #[error("L10 (linearity): function #{func_idx} parameter #{param_idx} is a Linear (own) resource but is never used; Linear resources must be consumed exactly once on every path")]
     LinearNotUsed { func_idx: u32, param_idx: u32 },
 
-    #[error("Level 10 violation: function {func_idx}, param {param_idx} — Linear (own) param dropped on some paths (per-path min uses = 0; must be consumed on every path)")]
+    #[error("L10 (linearity): function #{func_idx} parameter #{param_idx} is a Linear (own) resource that is consumed on some control-flow paths but dropped on others; Linear resources must be consumed exactly once on every path")]
     LinearDroppedOnSomePath { func_idx: u32, param_idx: u32 },
 
-    #[error("Level 10 violation: function {func_idx}, param {param_idx} — Linear (own) param loaded {count} times on some path (exactly 1 required; possible duplication)")]
+    #[error("L10 (linearity): function #{func_idx} parameter #{param_idx} is a Linear (own) resource but is used {count} times on some control-flow path; Linear resources must be consumed exactly once (possible duplication)")]
     LinearUsedMultiple {
         func_idx: u32,
         param_idx: u32,
         count: u32,
     },
 
-    #[error("Level 7 violation: function {func_idx}, param {param_idx} — ExclBorrow (mut) param aliased ({count} simultaneous references; at most 1 permitted)")]
+    #[error("L7 (aliasing): function #{func_idx} parameter #{param_idx} is an ExclBorrow (&mut) reference but {count} simultaneous borrows occur on some control-flow path; at most one is permitted")]
     ExclBorrowAliased {
         func_idx: u32,
         param_idx: u32,
@@ -97,23 +97,23 @@ pub enum OwnershipError {
     /// or table — a cross-module shared-state channel outside the
     /// declared function-import boundary. Carrier-free (standard
     /// import/memory sections only; no ownership-section ABI change).
-    #[error("Level 13 violation: {reason}")]
+    #[error("L13 (module isolation): {reason}")]
     ModuleNotIsolated { reason: String },
 }
 
 /// A cross-module ownership violation found in a caller's function body.
 /// Mirrors OCaml `Tw_interface.cross_error`.
 #[derive(Debug, Clone, PartialEq, Eq, Error)]
 pub enum CrossError {
-    #[error("Level 10 boundary violation: caller fn {caller_func_idx} calls import '{import_name}' {count} time(s) on some path (Linear param; must be called at most once)")]
+    #[error("L10 (linearity, cross-module): caller function #{caller_func_idx} calls Linear import '{import_name}' {count} times on some control-flow path; Linear imports must be called at most once on every path")]
     LinearImportCalledMultiple {
         caller_func_idx: u32,
         import_func_idx: u32,
         import_name: String,
         count: u32,
     },
 
-    #[error("Level 10 boundary violation: caller fn {caller_func_idx} calls import '{import_name}' on some paths but not others (Linear param dropped on zero-call path)")]
+    #[error("L10 (linearity, cross-module): caller function #{caller_func_idx} calls Linear import '{import_name}' on some control-flow paths but not on others; calls must be balanced across all paths")]
     LinearImportDroppedOnSomePath {
         caller_func_idx: u32,
         import_func_idx: u32,
@@ -122,18 +122,35 @@ pub enum CrossError {
 }
 
 /// Top-level verification failures (parse + verify).
+///
+/// The `Ownership` and `Cross` variants carry vectors of inner errors
+/// whose Display impls each emit a full natural-language explanation; the
+/// vector wrappers below render as "N L7/L10 violation(s): <first>; …"
+/// so a single-line log line is still informative and the full per-error
+/// detail is one `Vec::iter()` away for richer surfaces like `tw-verify`.
 #[derive(Debug, Error)]
 pub enum VerifyError {
     #[error("wasm parse error: {0}")]
     Parse(#[from] wasmparser::BinaryReaderError),
 
-    #[error("ownership violations: {0:?}")]
+    #[error("{} L7/L10/L13 ownership violation(s) — {}", .0.len(), display_first_then_ellipsis(.0))]
     Ownership(Vec<OwnershipError>),
 
-    #[error("cross-module boundary violations: {0:?}")]
+    #[error("{} L10 cross-module boundary violation(s) — {}", .0.len(), display_first_then_ellipsis(.0))]
     Cross(Vec<CrossError>),
 }
 
+/// Helper for the vector-variant Display impls: format the first inner
+/// error fully, then append "… and N more" if there are more, otherwise
+/// just the first. Empty vectors render as "(empty)".
+fn display_first_then_ellipsis<E: std::fmt::Display>(errs: &[E]) -> String {
+    match errs.split_first() {
+        None => "(empty)".to_string(),
+        Some((first, [])) => first.to_string(),
+        Some((first, rest)) => format!("{first}; … and {} more", rest.len()),
+    }
+}
+
 /// Custom-section name carrying ownership annotations. Producer-neutral as
 /// of the 2026-05-26 rename; both AffineScript (`Codegen.build_ownership_section`)
 /// and Ephapax (`ephapax-wasm`) emit and read this name.
@@ -167,14 +184,14 @@ pub const REGION_IMPORTS_SECTION_NAME: &str = "typedwasm.region-imports";
 #[cfg(feature = "unstable-l15")]
 #[derive(Debug, Clone, PartialEq, Eq, Error)]
 pub enum CapabilitiesError {
-    #[error("Level 15 violation: function index {func_idx} (entry {entry_idx}) is out of bounds for wasm function section (function_count = {function_count})")]
+    #[error("L15 (capabilities): typedwasm.capabilities entry #{entry_idx} declares function #{func_idx} but the module only has {function_count} function(s)")]
     FuncIdxOutOfRange {
         entry_idx: u32,
         func_idx: u32,
         function_count: u32,
     },
 
-    #[error("Level 15 violation: capability index {cap_idx} in function entry {entry_idx} (func_idx = {func_idx}) is out of bounds for capability table (capability_count = {capability_count})")]
+    #[error("L15 (capabilities): typedwasm.capabilities entry #{entry_idx} (for function #{func_idx}) requires capability #{cap_idx} but the capability table only has {capability_count} entries")]
     CapabilityIdxOutOfRange {
         entry_idx: u32,
         func_idx: u32,
@@ -192,24 +209,24 @@ pub enum AccessSiteError {
     /// `typedwasm.regions` section — the access-site entries reference
     /// `region_id` + `field_id` keys with nothing to resolve them
     /// against otherwise.
-    #[error("Level 2 violation: typedwasm.access-sites section emitted without companion typedwasm.regions section (MissingDependentCarrier)")]
+    #[error("L2 (region binding): typedwasm.access-sites section is present but the companion typedwasm.regions section is missing — access-site (region, field) keys have nothing to resolve against")]
     MissingDependentRegions,
 
-    #[error("Level 2 violation: access-site entry {entry_idx}: func_idx {func_idx} is out of bounds for wasm function section (function_count = {function_count})")]
+    #[error("L2 (region binding): typedwasm.access-sites entry #{entry_idx} declares function #{func_idx} but the module only has {function_count} function(s)")]
     FuncIdxOutOfRange {
         entry_idx: u32,
         func_idx: u32,
         function_count: u32,
     },
 
-    #[error("Level 2 violation: access-site entry {entry_idx}: region_id {region_id} is out of bounds for typedwasm.regions table (region_count = {region_count})")]
+    #[error("L2 (region binding): typedwasm.access-sites entry #{entry_idx} references region #{region_id} but typedwasm.regions only declares {region_count} region(s)")]
     RegionIdOutOfRange {
         entry_idx: u32,
         region_id: u32,
         region_count: u32,
     },
 
-    #[error("Level 2 violation: access-site entry {entry_idx}: field_id {field_id} is out of bounds for region {region_id}'s field table (field_count = {field_count})")]
+    #[error("L2 (region binding): typedwasm.access-sites entry #{entry_idx} references field #{field_id} of region #{region_id}, but that region only has {field_count} field(s)")]
     FieldIdOutOfRange {
         entry_idx: u32,
         region_id: u32,
@@ -387,4 +404,63 @@ mod tests {
         }
         assert_eq!(OwnershipKind::from_byte(99), OwnershipKind::Unrestricted);
     }
+
+    #[test]
+    fn ownership_error_display_is_natural_language() {
+        let e = OwnershipError::LinearUsedMultiple {
+            func_idx: 3,
+            param_idx: 1,
+            count: 5,
+        };
+        let s = e.to_string();
+        assert!(s.starts_with("L10 (linearity):"), "got: {s}");
+        assert!(s.contains("function #3 parameter #1"), "got: {s}");
+        assert!(s.contains("used 5 times"), "got: {s}");
+        assert!(s.contains("exactly once"), "got: {s}");
+    }
+
+    #[test]
+    fn verify_error_ownership_summary_renders_count_and_first() {
+        let e = VerifyError::Ownership(vec![
+            OwnershipError::LinearNotUsed {
+                func_idx: 0,
+                param_idx: 0,
+            },
+            OwnershipError::ExclBorrowAliased {
+                func_idx: 1,
+                param_idx: 0,
+                count: 2,
+            },
+            OwnershipError::ModuleNotIsolated {
+                reason: "module owns linear memory yet imports memory 'Host.memory'".to_string(),
+            },
+        ]);
+        let s = e.to_string();
+        // Header: total count + level mix
+        assert!(
+            s.starts_with("3 L7/L10/L13 ownership violation(s)"),
+            "got: {s}"
+        );
+        // First inner error's full Display is included
+        assert!(
+            s.contains("L10 (linearity): function #0 parameter #0"),
+            "got: {s}"
+        );
+        // Tail summarises remainder
+        assert!(s.contains("… and 2 more"), "got: {s}");
+    }
+
+    #[test]
+    fn cross_error_display_includes_import_name() {
+        let e = CrossError::LinearImportCalledMultiple {
+            caller_func_idx: 7,
+            import_func_idx: 0,
+            import_name: "consume".to_string(),
+            count: 2,
+        };
+        let s = e.to_string();
+        assert!(s.starts_with("L10 (linearity, cross-module):"), "got: {s}");
+        assert!(s.contains("caller function #7"), "got: {s}");
+        assert!(s.contains("'consume'"), "got: {s}");
+    }
 }