diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index 03ad9cd..d2c5d68 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -9,6 +9,27 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning]. === [Unreleased] +==== L15-C at the front-end: a caller's caps contain its callee's (2026-10-27) + +* The canonical Rust front-end (`typed-wasm-codegen`, ADR-0006) now parses + `capability NAME;`, the `caps: { … }` sub-clause of `effects` and the + calls in each function body, and refuses a module that breaks L15-A (a + capability declared twice), L15-B (a function requires an undeclared + capability) or L15-C (a function calls one in the same module whose caps + it does not hold). L15-C is checked per call site, as `WellFormedCall` + states it; `callCompose` covers chains of calls. A function with no + `caps` clause holds no capabilities. New module `src/caps.rs`. +* Until now the front-end skipped capabilities, and its AffineScript + counterpart `Checker.checkCapabilities` (L15-A + L15-B) is not compiled + or run in CI. The emitted-wasm verifier checks L15-A and L15-B from the + `typedwasm.capabilities` carrier (behind `unstable-l15`); it has no + L15-C pass. +* `tests/capabilities.rs`: one accepted program and a refused program for + each rule (10 tests). With the L15-C rule disabled, its four refusal + tests fail. +* Not covered: `module isolated` bodies (the front-end skips them) and + calls to imported functions (proposal 0004). + ==== Certificates whose level is their witnesses (2026-10-26) * `Proofs.idr`: `ProgressiveW n`, a chain holding a witness for every diff --git a/LEVEL-STATUS.adoc b/LEVEL-STATUS.adoc index 65e4552..ff6aa36 100644 --- a/LEVEL-STATUS.adoc +++ b/LEVEL-STATUS.adoc @@ -39,10 +39,11 @@ declarations; v1.1 `+caps: { ... }+` sub-clause becomes load-bearing. Idris2 proof: ResourceCapabilities.idr (DistinctCaps L15-A, ContainedIn + containedTrans L15-B, CallCompatible + callCompose L15-C, FullEffectBudget orthogonality with L8). Surface enforcement: -Checker.checkCapabilities + scope-threaded checkDeclaration. L15-A -(distinct) + L15-B (well-scoped) live at v1.4; L15-C (call-graph -monotone) deferred to v1.4.x (proof already carries the theorem). 76/76 -parser tests pass.* +the canonical Rust front-end (`+typed-wasm-codegen+` `+caps.rs+`, +ADR-0006) checks L15-A, L15-B and L15-C (per call site, top-level +module) and refuses violations; `+tests/capabilities.rs+` runs in CI. +The AffineScript `+Checker.checkCapabilities+` (L15-A + L15-B) is not +compiled or run in CI.* |*v1.5* |*L1-10, L13, L14, L15, L16* |*v0.6 sugar* |*+L16 Agent choreography: @@ -203,10 +204,11 @@ that frees peak − drift (`+BoundaryCut+`, `+boundaryOccupancy+`, future) |13 parser/Checker tests |*v1.3 — Idris2 proof + surface checker live; 007 send/receive lowering DONE (task #7)* -|15 |Resource capabilities |ResourceCapabilities.idr |(future) |13 -parser/Checker tests |*v1.4 — Idris2 proof + surface checker (L15-A + -L15-B) live; L15-C call-graph check deferred to v1.4.x; 007 lowering -DONE (task #9)* +|15 |Resource capabilities |ResourceCapabilities.idr |(future) |10 +front-end tests (`+tests/capabilities.rs+`) |*v1.4 — Idris2 proof + +front-end checks L15-A, L15-B and L15-C (per call site, top-level +module); 007 lowering DONE (task #9). Isolated-module bodies and +cross-module calls are not checked (proposal 0004).* |16 |Agent choreography |Choreography.idr + KCut.idr |(future) |12 parser/Checker tests |*v1.5 — composition proof over L13+L14+L15 live; surface checker diff --git a/crates/typed-wasm-codegen/src/caps.rs b/crates/typed-wasm-codegen/src/caps.rs new file mode 100644 index 0000000..8f0ec7e --- /dev/null +++ b/crates/typed-wasm-codegen/src/caps.rs @@ -0,0 +1,218 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) 2026 Jonathan D.A. Jewell +// +//! L15 resource capabilities: the surface checks for one module. +//! +//! The front-end ([`crate::parser`]) records the module's `capability NAME;` +//! declarations, each function's `caps: { … }` sub-clause and the names each +//! function body calls; [`check`] then enforces +//! +//! * **L15-A** (distinct): no capability is declared twice in the module; +//! * **L15-B** (well-scoped): every name in a function's `caps` set is a +//! declared capability; +//! * **L15-C** (monotone): when F calls G in the same module, G's `caps` set +//! is contained in F's. +//! +//! L15-C is checked per call site, as `ResourceCapabilities.idr` states it +//! (`WellFormedCall` carries `CallCompatible caller.required callee.required`). +//! Transitive calls need no separate check: `callCompose` proves that +//! well-formed edges compose. A function without a `caps` clause requires no +//! capabilities, so it may only call functions that require none. +//! +//! Scope: the top-level module. The front-end skips `module isolated … { … }` +//! bodies, so their declarations and functions are not checked here, and a +//! call to an imported function is not checked either (cross-module grants are +//! proposal 0004). + +/// One function's L15 facts, as the front-end recorded them. +#[derive(Debug, Clone, Default)] +pub struct FnCaps { + pub name: String, + /// The `caps: { … }` names, in source order; empty when absent. + pub caps: Vec, + /// Names the body calls (`name(…)`), in source order. Only names that are + /// functions of this module take part in L15-C. + pub calls: Vec, +} + +/// A lexical token: an identifier, or any other single non-space character. +#[derive(Debug, Clone, PartialEq, Eq)] +enum Tok { + Ident(String), + Punct(char), +} + +/// Split source text into identifiers and punctuation, dropping whitespace, +/// `//` and `/* */` comments and the contents of string literals, so a name +/// that only appears in a comment or a string is never taken for a call. +fn tokens(src: &str) -> Vec { + let b = src.as_bytes(); + let mut out = Vec::new(); + let mut i = 0; + while i < b.len() { + let c = b[i]; + if c.is_ascii_whitespace() { + i += 1; + } else if c == b'/' && b.get(i + 1) == Some(&b'/') { + while i < b.len() && b[i] != b'\n' { + i += 1; + } + } else if c == b'/' && b.get(i + 1) == Some(&b'*') { + i += 2; + while i < b.len() && !(b[i] == b'*' && b.get(i + 1) == Some(&b'/')) { + i += 1; + } + i = (i + 2).min(b.len()); + } else if c == b'"' { + i += 1; + while i < b.len() && b[i] != b'"' { + i += if b[i] == b'\\' { 2 } else { 1 }; + } + i = (i + 1).min(b.len()); + out.push(Tok::Punct('"')); + } else if c.is_ascii_alphabetic() || c == b'_' { + let start = i; + while i < b.len() && (b[i].is_ascii_alphanumeric() || b[i] == b'_') { + i += 1; + } + out.push(Tok::Ident(src[start..i].to_string())); + } else { + // Step over a whole UTF-8 character so slicing stays on a boundary. + let ch = src[i..].chars().next().unwrap_or('\u{FFFD}'); + out.push(Tok::Punct(ch)); + i += ch.len_utf8(); + } + } + out +} + +/// Collect call candidates in source order, retaining repeated names. +/// A candidate is an identifier followed by `(`, +/// unless it follows `.`, `$` or `@` (a field, region variable or region +/// reference). Comments and string contents are ignored. Keywords and +/// unresolved names are included; [`check`] resolves candidates against +/// the module's functions. +pub fn called_names(body: &str) -> Vec { + let toks = tokens(body); + let mut out = Vec::new(); + for (i, t) in toks.iter().enumerate() { + if let Tok::Ident(name) = t { + let prev_ok = i == 0 + || !matches!( + toks[i - 1], + Tok::Punct('.') | Tok::Punct('$') | Tok::Punct('@') + ); + if prev_ok && toks.get(i + 1) == Some(&Tok::Punct('(')) { + out.push(name.clone()); + } + } + } + out +} + +/// The `caps: { a, b }` sub-clause inside the text of an `effects { … }` +/// block (without its outer braces). `None` when the block has no `caps` +/// sub-clause (the flat `effects { Read, Write }` form). +/// Only the first `caps: {` is used; names are collected in source order, +/// retaining duplicates, until a token other than an identifier or comma. +/// An empty clause returns `Some` with an empty vector; closing braces and +/// separators are not validated. +pub fn caps_clause(effects_body: &str) -> Option> { + let toks = tokens(effects_body); + let start = toks.windows(3).position(|w| { + w[0] == Tok::Ident("caps".into()) && w[1] == Tok::Punct(':') && w[2] == Tok::Punct('{') + })?; + let mut caps = Vec::new(); + for t in &toks[start + 3..] { + match t { + Tok::Ident(name) => caps.push(name.clone()), + Tok::Punct(',') => {} + _ => break, // `}` closes the list + } + } + Some(caps) +} + +/// Run L15-A, L15-B and L15-C over one module. `declared` lists the +/// `capability` declarations in source order (duplicates included, so L15-A +/// can see them). Returns diagnostic strings grouped by L15-A, L15-B, +/// then L15-C, preserving input order within each rule; empty on success. +/// Calls absent from `funcs` are ignored. Each offending call produces one +/// L15-C diagnostic listing the callee's capabilities missing from the caller. +pub fn check(declared: &[String], funcs: &[FnCaps]) -> Vec { + let mut errors = Vec::new(); + let mut seen: Vec<&str> = Vec::new(); + for cap in declared { + if seen.contains(&cap.as_str()) { + errors.push(format!( + "L15-A: capability '{cap}' is declared more than once in the module \ + (capability declarations must be distinct)" + )); + } else { + seen.push(cap); + } + } + for f in funcs { + for cap in &f.caps { + if !seen.contains(&cap.as_str()) { + errors.push(format!( + "L15-B: function '{}' requires capability '{cap}', which the module does \ + not declare (add `capability {cap};`)", + f.name + )); + } + } + } + for f in funcs { + for callee in &f.calls { + let Some(g) = funcs.iter().find(|g| &g.name == callee) else { + continue; // not a function of this module + }; + let missing: Vec<&str> = g + .caps + .iter() + .filter(|c| !f.caps.contains(c)) + .map(String::as_str) + .collect(); + if !missing.is_empty() { + errors.push(format!( + "L15-C: function '{}' calls '{}', which requires capabilities {{ {} }} that \ + '{}' does not hold (a caller's caps must contain its callee's)", + f.name, + g.name, + missing.join(", "), + f.name + )); + } + } + } + errors +} + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn calls_skip_comments_strings_and_fields() { + let body = r#" + // net_send(x) in a comment + let s = "log(1)"; + let a = $p.helper(1); + if (ready()) { return send(a, compute (2)); } + "#; + // `if (` is a candidate too; `check` drops it, since only the + // module's own functions take part in L15-C. + assert_eq!(called_names(body), ["if", "ready", "send", "compute"]); + } + + #[test] + fn caps_clause_forms() { + assert_eq!( + caps_clause(" memory: { Read }, caps: { net, fs } "), + Some(vec!["net".to_string(), "fs".to_string()]) + ); + assert_eq!(caps_clause(" caps: { } "), Some(Vec::new())); + assert_eq!(caps_clause(" Read, Write "), None); + } +} diff --git a/crates/typed-wasm-codegen/src/lib.rs b/crates/typed-wasm-codegen/src/lib.rs index 315365b..06aeddc 100644 --- a/crates/typed-wasm-codegen/src/lib.rs +++ b/crates/typed-wasm-codegen/src/lib.rs @@ -56,6 +56,7 @@ use wasm_encoder::{ NameMap, NameSection, TypeSection, ValType, }; +pub mod caps; pub mod parser; // ---------------------------------------------------------------------- diff --git a/crates/typed-wasm-codegen/src/parser.rs b/crates/typed-wasm-codegen/src/parser.rs index e14037a..65d88cd 100644 --- a/crates/typed-wasm-codegen/src/parser.rs +++ b/crates/typed-wasm-codegen/src/parser.rs @@ -9,7 +9,9 @@ //! recording region schemas, ownership qualifiers (`own`/`&mut`/`&` → //! the `typedwasm.ownership` carrier) and cross-module region imports //! (`import region … from "…" { … }` → the `typedwasm.region-imports` -//! carrier, ADR-0007). +//! carrier, ADR-0007). It also records `capability NAME;` declarations, +//! each function's `caps:` set and the calls in its body, and refuses a +//! module that breaks L15-A, L15-B or L15-C ([`crate::caps`]). //! //! Known gaps against `spec/grammar.ebnf` are tracked debt (ADR-0006 //! §Consequences): non-lowerable statement bodies fall back to @@ -161,9 +163,14 @@ struct Parser<'a> { /// True when the source declared `memory { … }` — a synthesised /// memory must never override it. memory_declared: bool, + /// L15: `capability NAME;` declarations in source order, duplicates kept. + capabilities: Vec, + /// L15: each function's `caps` set and the names its body calls. + fn_caps: Vec, } impl<'a> Parser<'a> { + /// Create a parser at the start of `src` with no declarations recorded. fn new(src: &'a str) -> Self { Self { src, @@ -177,6 +184,8 @@ impl<'a> Parser<'a> { region_imports: Vec::new(), region_instances: Vec::new(), memory_declared: false, + capabilities: Vec::new(), + fn_caps: Vec::new(), } } @@ -188,6 +197,12 @@ impl<'a> Parser<'a> { /// declared instance counts (needed to seed importers in /// [`parse_modules`] so their scans iterate the producer's real /// instance array). + /// + /// # Errors + /// + /// Propagates declaration parsing errors. If parsing completes but + /// [`crate::caps::check`] finds L15 violations, returns all its diagnostics + /// joined by newlines. fn parse_with_instances(mut self) -> Result<(Module, Vec), String> { while self.pos < self.src.len() { self.skip_whitespace(); @@ -207,12 +222,19 @@ impl<'a> Parser<'a> { self.parse_function()?; } else if self.peek_word("import") { self.parse_import()?; + } else if self.peek_word("capability") { + self.parse_capability()?; } else { // Skip comments and unknown declarations self.skip_declaration(); } } + let cap_errors = crate::caps::check(&self.capabilities, &self.fn_caps); + if !cap_errors.is_empty() { + return Err(cap_errors.join("\n")); + } + Ok(( Module { regions: self.regions, @@ -728,6 +750,13 @@ impl<'a> Parser<'a> { Ok(()) } + /// Parse and append an exported function, recording ownership and L15 facts. + /// Bodies that cannot be lowered become stubs that drop all parameters and + /// return a typed zero result, if any; their call candidates are still recorded. + /// + /// # Errors + /// + /// Propagates errors parsing parameter and return types or required syntax. fn parse_function(&mut self) -> Result<(), String> { self.expect("fn")?; let name = self.parse_ident(); @@ -807,7 +836,9 @@ impl<'a> Parser<'a> { // Skip any annotation clauses before the body: `effects { ... }`, // `cost_bound { ... }`, `requires { ... }`, etc. The body is the - // first `{` not preceded by an annotation keyword. + // first `{` not preceded by an annotation keyword. The `caps:` + // sub-clause of `effects` is kept for the L15 checks. + let mut caps = Vec::new(); loop { self.skip_whitespace(); if self.peek_char('{') { @@ -815,11 +846,22 @@ impl<'a> Parser<'a> { } let at = self.pos; if at < self.src.len() && (self.src.as_bytes()[at] as char).is_ascii_alphabetic() { - let _annotation = self.parse_ident(); + let annotation = self.parse_ident(); self.skip_whitespace(); if self.peek_char('{') { self.expect("{")?; + let clause_start = self.pos; self.skip_to_brace_close(); + if annotation == "effects" { + let clause_end = self.pos.saturating_sub(1).max(clause_start); + if let Some(found) = self + .src + .get(clause_start..clause_end) + .and_then(crate::caps::caps_clause) + { + caps = found; + } + } continue; } } @@ -874,6 +916,20 @@ impl<'a> Parser<'a> { } }; + // L15: every path above has consumed the body through its closing + // `}`, so the body text is `body_start..pos`. Its calls are resolved + // against this module's functions once the whole module is parsed. + let calls = self + .src + .get(body_start..self.pos) + .map(crate::caps::called_names) + .unwrap_or_default(); + self.fn_caps.push(crate::caps::FnCaps { + name: name.clone(), + caps, + calls, + }); + // Record the function's ownership signature when the source asked // for L7/L10 discipline anywhere in it. All-Unrestricted functions // stay out of the carrier (empty = no constraint, matching the @@ -1414,6 +1470,29 @@ impl<'a> Parser<'a> { } } + /// Record a `capability NAME;` declaration for L15 checks, keeping duplicates. + /// Declarations whose first identifier is not exactly `capability` (such as + /// `capability_x`) are skipped without recording a capability. + /// + /// # Errors + /// + /// Returns an error if the name is missing or the required `;` cannot be parsed. + fn parse_capability(&mut self) -> Result<(), String> { + let save = self.pos; + if self.parse_ident() != "capability" { + self.pos = save; + self.skip_declaration(); + return Ok(()); + } + let name = self.parse_ident(); + if name.is_empty() { + return Err(format!("Expected a capability name at position {}", self.pos)); + } + self.expect(";")?; + self.capabilities.push(name); + Ok(()) + } + fn parse_import(&mut self) -> Result<(), String> { self.expect("import")?; self.skip_whitespace(); diff --git a/crates/typed-wasm-codegen/tests/capabilities.rs b/crates/typed-wasm-codegen/tests/capabilities.rs new file mode 100644 index 0000000..88da2de --- /dev/null +++ b/crates/typed-wasm-codegen/tests/capabilities.rs @@ -0,0 +1,150 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) 2026 Jonathan D.A. Jewell +// +// L15 resource capabilities at the `.twasm` front-end: L15-A (distinct +// declarations), L15-B (caps are declared) and L15-C (a caller's caps contain +// its callee's), the surface form of `ResourceCapabilities.idr`'s +// `DistinctCaps`, `ContainedIn` and `CallCompatible`. Each rule has a program +// it accepts and one it must refuse. + +use typed_wasm_codegen::parser::parse_module; + +fn refused(src: &str) -> String { + match parse_module(src) { + Ok(_) => panic!("program must be refused:\n{src}"), + Err(e) => e, + } +} + +const ACCEPTED: &str = r#" +capability net; +capability fs; + +fn send(x: i32) -> i32 + effects { memory: { Read }, caps: { net } } +{ + return x; +} + +fn sync(x: i32) -> i32 + effects { memory: { Read }, caps: { net, fs } } +{ + let a: i32 = send(x); + if a > 0 { + return send(a); + } + return a; +} + +fn pure_helper(x: i32) -> i32 { + return x; +} + +fn plain(x: i32) -> i32 { + // send(x) here is only a comment + return pure_helper(x); +} +"#; + +#[test] +fn accepts_well_formed_capabilities_and_calls() { + parse_module(ACCEPTED).expect("well-formed L15 program must parse"); +} + +#[test] +fn l15a_refuses_a_duplicate_declaration() { + let e = refused("capability net;\ncapability net;\nfn f() -> i32 { return 0; }\n"); + assert!(e.contains("L15-A") && e.contains("'net'"), "{e}"); +} + +#[test] +fn l15b_refuses_an_undeclared_capability() { + let e = refused( + "capability net;\n\ + fn f() -> i32 effects { memory: { Read }, caps: { net, fs } } { return 0; }\n", + ); + assert!( + e.contains("L15-B") && e.contains("'fs'") && !e.contains("'net'"), + "{e}" + ); +} + +#[test] +fn l15c_refuses_a_caller_missing_a_callee_capability() { + let e = refused( + "capability net;\ncapability fs;\n\ + fn write_file() -> i32 effects { caps: { fs } } { return 0; }\n\ + fn upload() -> i32 effects { caps: { net } } { return write_file(); }\n", + ); + assert!( + e.contains("L15-C") && e.contains("'upload' calls 'write_file'") && e.contains("{ fs }"), + "{e}" + ); +} + +#[test] +fn l15c_refuses_a_caller_without_caps_calling_a_capped_function() { + // No caps clause means no capabilities: calling `send` would launder `net`. + let e = refused( + "capability net;\n\ + fn send() -> i32 effects { caps: { net } } { return 0; }\n\ + fn quiet() -> i32 { if 1 > 0 { return send(); } return 0; }\n", + ); + assert!( + e.contains("L15-C") && e.contains("'quiet' calls 'send'"), + "{e}" + ); +} + +#[test] +fn l15c_checks_calls_to_functions_declared_later() { + let e = refused( + "capability net;\n\ + fn early() -> i32 { return late(); }\n\ + fn late() -> i32 effects { caps: { net } } { return 0; }\n", + ); + assert!(e.contains("'early' calls 'late'"), "{e}"); +} + +#[test] +fn l15c_is_per_call_site_not_transitive_only() { + // f -> g -> h. g holds h's `net`, so g -> h is fine; f holds nothing and + // g requires `net`, so the f -> g edge alone is refused. + let e = refused( + "capability net;\n\ + fn h() -> i32 effects { caps: { net } } { return 0; }\n\ + fn g() -> i32 effects { caps: { net } } { return h(); }\n\ + fn f() -> i32 { return g(); }\n", + ); + assert!( + e.contains("'f' calls 'g'") && !e.contains("'g' calls 'h'"), + "{e}" + ); +} + +#[test] +fn calls_in_comments_and_strings_do_not_count() { + parse_module( + "capability net;\n\ + fn send() -> i32 effects { caps: { net } } { return 0; }\n\ + fn f() -> i32 {\n // send()\n /* send() */\n return 0;\n}\n", + ) + .expect("a call that only appears in a comment is not a call"); +} + +#[test] +fn a_non_capability_identifier_is_not_a_declaration() { + // `capability_count` starts with the keyword but is not one. + parse_module("capability_count stuff;\nfn f() -> i32 { return 0; }\n") + .expect("an identifier that merely starts with `capability` is skipped"); +} + +#[test] +fn examples_without_capabilities_still_parse() { + for ex in [ + include_str!("../../../examples/01-single-module.twasm"), + include_str!("../../../examples/03-ownership-linearity.twasm"), + ] { + parse_module(ex).expect("examples declare no capabilities and must still parse"); + } +} diff --git a/spec/grammar.ebnf b/spec/grammar.ebnf index 9a52690..192cb8c 100644 --- a/spec/grammar.ebnf +++ b/spec/grammar.ebnf @@ -26,8 +26,9 @@ * `capability` declaration in the enclosing module's scope. * - Checker enforcements: L15-A distinct capability names per module * (top-level or isolated-module body), L15-B function caps ⊆ enclosing - * module's declared capability set. Call-graph monotonicity (L15-C) is - * proven in the Idris2 core and deferred at the surface checker for v1.4. + * module's declared capability set, L15-C a caller's caps contain the + * caps of every function it calls (per call site; checked by the Rust + * front-end, crates/typed-wasm-codegen/src/caps.rs). * - Idris2 proof artefact: src/abi/TypedWasm/ABI/ResourceCapabilities.idr — * DistinctCaps (L15-A), ContainedIn + containedRefl/containedTrans * (L15-B subset), CallCompatible + callCompose (L15-C monotonicity), diff --git a/src/parser/Ast.affine b/src/parser/Ast.affine index 2b41142..d6032bc 100644 --- a/src/parser/Ast.affine +++ b/src/parser/Ast.affine @@ -219,10 +219,10 @@ and sessionTransitionDecl = { // // L15-C (call-graph monotonicity) is proven in the Idris2 core // (`ResourceCapabilities.idr`: `CallCompatible`, `callCompose`, -// `callReachesModule`) but surface-level call-graph analysis is -// deferred — v1.4 ships without it because the current checker doesn't -// track inter-function calls. When the call-graph check lands, it will -// piggy-back on this same capability-declaration set. +// `callReachesModule`). This AffineScript checker does not track +// inter-function calls; the canonical Rust front-end checks L15-C per call +// site over the same capability-declaration set +// (crates/typed-wasm-codegen/src/caps.rs). // // Reserved-keyword policy: `capability` is NOT globally lexed; the parser // recognises it contextually from `Ident("capability")`. The reserved diff --git a/src/parser/Checker.affine b/src/parser/Checker.affine index 687d3d6..6c4b983 100644 --- a/src/parser/Checker.affine +++ b/src/parser/Checker.affine @@ -732,8 +732,10 @@ let checkSession = (s: sessionDecl, m: module_, loc: Lexer.loc): array