From 9e59c7a6d017ac569b7d8479ce60a1e27cd74add Mon Sep 17 00:00:00 2001
From: Apocky <apocky13@gmail.com>
Date: Fri, 15 May 2026 10:36:30 -0700
Subject: [PATCH] =?UTF-8?q?=C2=A7=20pr-gamma/iccombs-toy-harness=20?=
 =?UTF-8?q?=E2=97=90=20TOY=20=E2=8A=90=20U-K-prelude=20(=C2=AC=20PD-bindin?=
 =?UTF-8?q?g)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Lands the iccombs experimental demo-harness per IMPL_06_CORRIGENDUM § U-K-prelude :

  cssl-iccombs-toy-elab : surface λ-calculus → cssl-hgraph + grade-context + toy effect-row

  cssl-lower-iccombs    : LINEAR fragment → cssl-iccombs interaction net (Lafont/Mackie SIC)

  cssl-iccombs-toy-cli  : S-exp frontend + bin cssl-iccombs-toy

INVARIANTS (per corrigendum) :

  ✗ NOT a production elaborator (production = cssl-hir per Wave U-B revised)

  ✗ NOT a production driver    (production = csslc)

  ✗ NOT a PD-discipline gate   (PD = cssl-caps + cssl-effects + cssl-ifc per Wave U-G revised)

  ✓ doc-headers + Cargo descriptions + bin-name carry TOY warning + corrigendum link

GATES : cargo check ✓ · cargo test ✓ · cargo clippy --all-targets ✓ (3 toy crates + their deps)

Stacks on : pr-beta/foundation-baseline (depends on cssl-cas + cssl-hgraph + cssl-grades + cssl-iccombs)
---
 compiler-rs/Cargo.lock                        |  29 +
 .../crates/cssl-iccombs-toy-cli/Cargo.toml    |  22 +
 .../crates/cssl-iccombs-toy-cli/src/lib.rs    | 255 +++++++++
 .../crates/cssl-iccombs-toy-cli/src/main.rs   | 101 ++++
 .../crates/cssl-iccombs-toy-elab/Cargo.toml   |  18 +
 .../crates/cssl-iccombs-toy-elab/src/lib.rs   | 498 ++++++++++++++++++
 .../crates/cssl-lower-iccombs/Cargo.toml      |  17 +
 .../crates/cssl-lower-iccombs/src/lib.rs      | 228 ++++++++
 8 files changed, 1168 insertions(+)
 create mode 100644 compiler-rs/crates/cssl-iccombs-toy-cli/Cargo.toml
 create mode 100644 compiler-rs/crates/cssl-iccombs-toy-cli/src/lib.rs
 create mode 100644 compiler-rs/crates/cssl-iccombs-toy-cli/src/main.rs
 create mode 100644 compiler-rs/crates/cssl-iccombs-toy-elab/Cargo.toml
 create mode 100644 compiler-rs/crates/cssl-iccombs-toy-elab/src/lib.rs
 create mode 100644 compiler-rs/crates/cssl-lower-iccombs/Cargo.toml
 create mode 100644 compiler-rs/crates/cssl-lower-iccombs/src/lib.rs

diff --git a/compiler-rs/Cargo.lock b/compiler-rs/Cargo.lock
index f7ae3be..790397c 100644
--- a/compiler-rs/Cargo.lock
+++ b/compiler-rs/Cargo.lock
@@ -2055,6 +2055,26 @@ dependencies = [
 name = "cssl-iccombs"
 version = "0.1.0"
 
+[[package]]
+name = "cssl-iccombs-toy-cli"
+version = "0.1.0"
+dependencies = [
+ "cssl-cas",
+ "cssl-iccombs",
+ "cssl-iccombs-toy-elab",
+ "cssl-lower-iccombs",
+]
+
+[[package]]
+name = "cssl-iccombs-toy-elab"
+version = "0.1.0"
+dependencies = [
+ "cssl-cas",
+ "cssl-grades",
+ "cssl-hgraph",
+ "thiserror 1.0.69",
+]
+
 [[package]]
 name = "cssl-ifc"
 version = "0.1.0"
@@ -2117,6 +2137,15 @@ dependencies = [
  "thiserror 1.0.69",
 ]
 
+[[package]]
+name = "cssl-lower-iccombs"
+version = "0.1.0"
+dependencies = [
+ "cssl-iccombs",
+ "cssl-iccombs-toy-elab",
+ "thiserror 1.0.69",
+]
+
 [[package]]
 name = "cssl-macros"
 version = "0.1.0"
diff --git a/compiler-rs/crates/cssl-iccombs-toy-cli/Cargo.toml b/compiler-rs/crates/cssl-iccombs-toy-cli/Cargo.toml
new file mode 100644
index 0000000..c1a1c36
--- /dev/null
+++ b/compiler-rs/crates/cssl-iccombs-toy-cli/Cargo.toml
@@ -0,0 +1,22 @@
+[package]
+name         = "cssl-iccombs-toy-cli"
+version.workspace      = true
+edition.workspace      = true
+rust-version.workspace = true
+license.workspace      = true
+authors.workspace      = true
+description  = "TOY S-exp frontend + driver for the iccombs demo-harness (Wave U-D + IMPL_06_CORRIGENDUM). NOT the production driver — production driver = csslc."
+repository.workspace   = true
+
+[[bin]]
+name = "cssl-iccombs-toy"
+path = "src/main.rs"
+
+[dependencies]
+cssl-iccombs-toy-elab = { path = "../cssl-iccombs-toy-elab" }
+cssl-cas              = { path = "../cssl-cas" }
+cssl-iccombs          = { path = "../cssl-iccombs" }
+cssl-lower-iccombs    = { path = "../cssl-lower-iccombs" }
+
+[lints]
+workspace = true
diff --git a/compiler-rs/crates/cssl-iccombs-toy-cli/src/lib.rs b/compiler-rs/crates/cssl-iccombs-toy-cli/src/lib.rs
new file mode 100644
index 0000000..781eab5
--- /dev/null
+++ b/compiler-rs/crates/cssl-iccombs-toy-cli/src/lib.rs
@@ -0,0 +1,255 @@
+#![forbid(unsafe_code)]
+#![doc = "cssl-iccombs-toy-cli — TOY S-expression frontend for the iccombs demo.\n\n\
+⚠ TOY per `specs/Upgrade/impl/IMPL_06_CORRIGENDUM.csl`. NOT the production parser\n\
+(real parser = cssl-parse, real driver = csslc). This crate exists ONLY to feed\n\
+the iccombs harness (cssl-iccombs-toy-elab + cssl-lower-iccombs + cssl-iccombs-toy bin).\n\n\
+Grammar (recursive S-exp) :\n\
+  term     := atom | list\n\
+  atom     := identifier | `()`\n\
+  list     := `(` head args `)`\n\
+  head     := `lam` <ident> <grade> body\n\
+            | `let` <ident> <grade> value body\n\
+            | `app` fn arg\n\
+            | `op` <label>\n\
+  grade    := `L` | `A` | `W`     (linear / affine / unrestricted-ω)\n\
+  identifier = `[A-Za-z_][A-Za-z0-9_-]*`\n"]
+
+use cssl_iccombs_toy_elab::{Grade, Term};
+
+/// Parse error.
+#[derive(Debug, PartialEq, Eq)]
+pub struct ParseError {
+    pub msg: String,
+    pub at: usize,
+}
+
+impl std::fmt::Display for ParseError {
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        write!(f, "parse error at offset {} : {}", self.at, self.msg)
+    }
+}
+
+impl std::error::Error for ParseError {}
+
+/// Parse a complete S-expression source into a `Term`.
+pub fn parse(src: &str) -> Result<Term, ParseError> {
+    let tokens = tokenize(src)?;
+    let mut p = Parser { tokens, pos: 0 };
+    let t = p.parse_term()?;
+    if p.pos != p.tokens.len() {
+        return Err(ParseError {
+            msg: "trailing tokens after term".into(),
+            at: p.tokens[p.pos].at,
+        });
+    }
+    Ok(t)
+}
+
+#[derive(Clone, Debug, PartialEq, Eq)]
+enum Tok {
+    LParen,
+    RParen,
+    Ident(String),
+}
+
+#[derive(Clone, Debug)]
+struct Token {
+    tok: Tok,
+    at: usize,
+}
+
+fn tokenize(src: &str) -> Result<Vec<Token>, ParseError> {
+    let mut out = Vec::new();
+    let bytes = src.as_bytes();
+    let mut i = 0;
+    while i < bytes.len() {
+        let c = bytes[i];
+        match c {
+            b' ' | b'\t' | b'\n' | b'\r' => { i += 1; }
+            b'(' => { out.push(Token { tok: Tok::LParen, at: i }); i += 1; }
+            b')' => { out.push(Token { tok: Tok::RParen, at: i }); i += 1; }
+            b';' => { while i < bytes.len() && bytes[i] != b'\n' { i += 1; } }
+            _ if is_ident_start(c) => {
+                let start = i;
+                while i < bytes.len() && is_ident_cont(bytes[i]) { i += 1; }
+                let s = std::str::from_utf8(&bytes[start..i])
+                    .map_err(|_| ParseError { msg: "non-utf8 ident".into(), at: start })?;
+                out.push(Token { tok: Tok::Ident(s.into()), at: start });
+            }
+            _ => return Err(ParseError { msg: format!("unexpected byte 0x{c:02x}"), at: i }),
+        }
+    }
+    Ok(out)
+}
+
+fn is_ident_start(c: u8) -> bool { c.is_ascii_alphabetic() || c == b'_' }
+fn is_ident_cont(c: u8) -> bool {
+    c.is_ascii_alphanumeric() || c == b'_' || c == b'-'
+}
+
+struct Parser {
+    tokens: Vec<Token>,
+    pos: usize,
+}
+
+impl Parser {
+    fn peek(&self) -> Option<&Token> { self.tokens.get(self.pos) }
+
+    fn bump(&mut self) -> Result<Token, ParseError> {
+        let t = self.tokens
+            .get(self.pos)
+            .ok_or_else(|| ParseError { msg: "unexpected end of input".into(), at: usize::MAX })?
+            .clone();
+        self.pos += 1;
+        Ok(t)
+    }
+
+    fn expect_ident(&mut self) -> Result<(String, usize), ParseError> {
+        let t = self.bump()?;
+        match t.tok {
+            Tok::Ident(s) => Ok((s, t.at)),
+            other => Err(ParseError { msg: format!("expected ident, got {other:?}"), at: t.at }),
+        }
+    }
+
+    fn expect(&mut self, want: Tok) -> Result<(), ParseError> {
+        let t = self.bump()?;
+        if t.tok == want { Ok(()) } else {
+            Err(ParseError { msg: format!("expected {want:?}, got {:?}", t.tok), at: t.at })
+        }
+    }
+
+    fn parse_grade(&mut self) -> Result<Grade, ParseError> {
+        let (s, at) = self.expect_ident()?;
+        match s.as_str() {
+            "L" => Ok(Grade::Linear),
+            "A" => Ok(Grade::Affine),
+            "W" | "ω" => Ok(Grade::Unrestricted),
+            _ => Err(ParseError { msg: format!("unknown grade `{s}` (use L | A | W)"), at }),
+        }
+    }
+
+    fn parse_term(&mut self) -> Result<Term, ParseError> {
+        let t = self.peek()
+            .ok_or_else(|| ParseError { msg: "expected term".into(), at: usize::MAX })?
+            .clone();
+        match &t.tok {
+            Tok::LParen => self.parse_list(),
+            Tok::Ident(_) => {
+                let (name, _) = self.expect_ident()?;
+                Ok(Term::Var(name))
+            }
+            Tok::RParen => Err(ParseError { msg: "unexpected `)`".into(), at: t.at }),
+        }
+    }
+
+    fn parse_list(&mut self) -> Result<Term, ParseError> {
+        self.expect(Tok::LParen)?;
+        // `()` is unit.
+        if let Some(t) = self.peek() {
+            if matches!(t.tok, Tok::RParen) {
+                self.expect(Tok::RParen)?;
+                return Ok(Term::Unit);
+            }
+        }
+        let (head, head_at) = self.expect_ident()?;
+        let term = match head.as_str() {
+            "lam" => {
+                let (param, _) = self.expect_ident()?;
+                let grade = self.parse_grade()?;
+                let body = self.parse_term()?;
+                Term::Lam { param, grade, body: Box::new(body) }
+            }
+            "let" => {
+                let (name, _) = self.expect_ident()?;
+                let grade = self.parse_grade()?;
+                let value = self.parse_term()?;
+                let body = self.parse_term()?;
+                Term::Let { name, grade, value: Box::new(value), body: Box::new(body) }
+            }
+            "app" => {
+                let f = self.parse_term()?;
+                let x = self.parse_term()?;
+                Term::App(Box::new(f), Box::new(x))
+            }
+            "op" => {
+                let (label, _) = self.expect_ident()?;
+                Term::Op(label)
+            }
+            other => return Err(ParseError {
+                msg: format!("unknown head `{other}` (expect lam | let | app | op)"),
+                at: head_at,
+            }),
+        };
+        self.expect(Tok::RParen)?;
+        Ok(term)
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use cssl_iccombs_toy_elab::elaborate;
+
+    #[test]
+    fn parse_unit() {
+        assert_eq!(parse("()").unwrap(), Term::Unit);
+    }
+
+    #[test]
+    fn parse_var() {
+        assert_eq!(parse("x").unwrap(), Term::Var("x".into()));
+    }
+
+    #[test]
+    fn parse_linear_identity() {
+        let t = parse("(lam x L x)").unwrap();
+        assert!(matches!(t, Term::Lam { grade: Grade::Linear, .. }));
+        elaborate(&t).expect("parsed identity must elaborate");
+    }
+
+    #[test]
+    fn parse_application_of_op() {
+        let t = parse("(app (lam x W x) (op io))").unwrap();
+        let e = elaborate(&t).unwrap();
+        assert!(e.effects.contains("io"));
+    }
+
+    #[test]
+    fn parse_let_unrestricted() {
+        let t = parse("(let x W (op io) (op state))").unwrap();
+        let e = elaborate(&t).unwrap();
+        assert!(e.effects.contains("io"));
+        assert!(e.effects.contains("state"));
+    }
+
+    #[test]
+    fn parse_rejects_unknown_head() {
+        let err = parse("(foo x)").unwrap_err();
+        assert!(err.msg.contains("unknown head"));
+    }
+
+    #[test]
+    fn parse_rejects_unknown_grade() {
+        let err = parse("(lam x Z x)").unwrap_err();
+        assert!(err.msg.contains("unknown grade"));
+    }
+
+    #[test]
+    fn parse_rejects_trailing_tokens() {
+        let err = parse("() x").unwrap_err();
+        assert!(err.msg.contains("trailing"));
+    }
+
+    #[test]
+    fn parse_strips_line_comments() {
+        let t = parse("; this is a comment\n(lam x W x) ; trailing\n").unwrap();
+        assert!(matches!(t, Term::Lam { .. }));
+    }
+
+    #[test]
+    fn parse_rejects_unmatched_close_paren() {
+        let err = parse(")").unwrap_err();
+        assert!(err.msg.contains("unexpected `)`"));
+    }
+}
diff --git a/compiler-rs/crates/cssl-iccombs-toy-cli/src/main.rs b/compiler-rs/crates/cssl-iccombs-toy-cli/src/main.rs
new file mode 100644
index 0000000..bad06a7
--- /dev/null
+++ b/compiler-rs/crates/cssl-iccombs-toy-cli/src/main.rs
@@ -0,0 +1,101 @@
+#![forbid(unsafe_code)]
+//! `cssl-iccombs-toy` — TOY interaction-combinator demo binary.
+//!
+//! ⚠ TOY per `specs/Upgrade/impl/IMPL_06_CORRIGENDUM.csl`. NOT a PD-binding driver.
+//! Real driver = `csslc`. Real PD = composition of cssl-caps + cssl-effects + cssl-ifc.
+//!
+//! Usage :
+//!   cssl-iccombs-toy [--lower-iccombs] [--reduce <N>] -- <S-exp>
+//!   cssl-iccombs-toy --stdin                          (read source from stdin)
+
+use cssl_iccombs_toy_cli::parse;
+use std::io::Read;
+use std::process::ExitCode;
+
+fn main() -> ExitCode {
+    let args: Vec<String> = std::env::args().skip(1).collect();
+    match run(&args) {
+        Ok(()) => ExitCode::SUCCESS,
+        Err(e) => {
+            eprintln!("error: {e}");
+            ExitCode::FAILURE
+        }
+    }
+}
+
+fn run(args: &[String]) -> Result<(), String> {
+    let mut source: Option<String> = None;
+    let mut from_stdin = false;
+    let mut lower_ic = false;
+    let mut reduce_steps: Option<usize> = None;
+    let mut i = 0;
+    while i < args.len() {
+        match args[i].as_str() {
+            "--help" | "-h" => { print_help(); return Ok(()); }
+            "--stdin" => { from_stdin = true; i += 1; }
+            "--lower-iccombs" => { lower_ic = true; i += 1; }
+            "--reduce" => {
+                i += 1;
+                let n = args.get(i).ok_or("`--reduce` requires a step-count")?;
+                reduce_steps = Some(n.parse::<usize>().map_err(|e| format!("`--reduce` : {e}"))?);
+                lower_ic = true;
+                i += 1;
+            }
+            "--" => { i += 1; source = Some(args[i..].join(" ")); break; }
+            other => return Err(format!("unknown arg `{other}` (try --help)")),
+        }
+    }
+
+    let src = if from_stdin {
+        let mut s = String::new();
+        std::io::stdin().read_to_string(&mut s).map_err(|e| e.to_string())?;
+        s
+    } else {
+        source.ok_or("no source : pass `-- <S-exp>` or `--stdin`")?
+    };
+
+    let term = parse(&src).map_err(|e| e.to_string())?;
+    let elab = cssl_iccombs_toy_elab::elaborate(&term).map_err(|e| format!("elab : {e}"))?;
+
+    println!("=== cssl-iccombs-toy report ===");
+    println!("hgraph nodes : {}", elab.hgraph.node_count());
+    println!("hgraph edges : {}", elab.hgraph.edge_count());
+    println!("hgraph cid   : {}", cssl_cas::cid_hex(&elab.cid()));
+    println!("effects pure : {}", elab.effects.is_pure());
+    println!("effects      : [{}]",
+        elab.effects.labels.iter().cloned().collect::<Vec<_>>().join(", "));
+
+    if lower_ic {
+        match cssl_lower_iccombs::lower(&term) {
+            Ok(mut lowered) => {
+                println!("iccombs net  : {} agent(s) initial", lowered.net.agent_count());
+                if let Some(max) = reduce_steps {
+                    let r = lowered.net.reduce_to_normal_form(max);
+                    println!("iccombs reduce: {r:?} ; {} agent(s) post-reduce", lowered.net.agent_count());
+                }
+            }
+            Err(e) => println!("iccombs lower: SKIPPED : {e}"),
+        }
+    }
+
+    Ok(())
+}
+
+fn print_help() {
+    println!("cssl-iccombs-toy : CSSLv3 interaction-combinator demo (TOY ; not PD-binding)");
+    println!();
+    println!("USAGE :");
+    println!("  cssl-iccombs-toy [OPTIONS] -- <S-EXP>");
+    println!("  cssl-iccombs-toy [OPTIONS] --stdin");
+    println!();
+    println!("OPTIONS :");
+    println!("  --stdin               read source from stdin instead of args");
+    println!("  --lower-iccombs       additionally lower term to a cssl-iccombs interaction net (linear fragment only)");
+    println!("  --reduce <N>          implies --lower-iccombs ; reduce up to <N> active-pair steps");
+    println!("  -h, --help            print this help");
+    println!();
+    println!("EXAMPLES :");
+    println!("  cssl-iccombs-toy -- '(lam x L x)'");
+    println!("  cssl-iccombs-toy --lower-iccombs -- '(lam x L x)'");
+    println!("  cssl-iccombs-toy --reduce 64 -- '(app (lam x L x) ())'");
+}
diff --git a/compiler-rs/crates/cssl-iccombs-toy-elab/Cargo.toml b/compiler-rs/crates/cssl-iccombs-toy-elab/Cargo.toml
new file mode 100644
index 0000000..430a19a
--- /dev/null
+++ b/compiler-rs/crates/cssl-iccombs-toy-elab/Cargo.toml
@@ -0,0 +1,18 @@
+[package]
+name         = "cssl-iccombs-toy-elab"
+version.workspace      = true
+edition.workspace      = true
+rust-version.workspace = true
+license.workspace      = true
+authors.workspace      = true
+description  = "TOY graded-modal elaborator for the iccombs demo-harness (Wave U-D + IMPL_06_CORRIGENDUM). NOT a production elaborator — production elab lives in cssl-hir. Surface λ-calculus → hgraph + grade-context + toy effect-row."
+repository.workspace   = true
+
+[dependencies]
+cssl-cas    = { path = "../cssl-cas" }
+cssl-hgraph = { path = "../cssl-hgraph" }
+cssl-grades = { path = "../cssl-grades" }
+thiserror.workspace = true
+
+[lints]
+workspace = true
diff --git a/compiler-rs/crates/cssl-iccombs-toy-elab/src/lib.rs b/compiler-rs/crates/cssl-iccombs-toy-elab/src/lib.rs
new file mode 100644
index 0000000..cb9b0df
--- /dev/null
+++ b/compiler-rs/crates/cssl-iccombs-toy-elab/src/lib.rs
@@ -0,0 +1,498 @@
+#![forbid(unsafe_code)]
+#![doc = "cssl-iccombs-toy-elab — TOY graded-modal elaborator (iccombs harness).\n\n\
+⚠ TOY per `specs/Upgrade/impl/IMPL_06_CORRIGENDUM.csl`. NOT a production elaborator.\n\
+The production elaborator is `cssl-hir` (CST→typed-resolved-inferred HIR + integrates\n\
+cssl-caps + cssl-effects + cssl-ifc). Wave U-B revised : extend cssl-hir with grades,\n\
+do NOT keep this crate as the elab path. This crate exists only as the L1 input to\n\
+the iccombs demo-harness (cssl-lower-iccombs + cssl-iccombs-toy-cli)."]
+
+use cssl_cas::{cid_of_bytes, Cid};
+use cssl_hgraph::{EdgeKind, HGraph, NodeId, NodeLabel, Port, TypeCid};
+use std::collections::HashMap;
+use thiserror::Error;
+
+/// Toy effect-row : ordered set of effect labels accumulated during elaboration.
+///
+/// ⚠ TOY per IMPL_06_CORRIGENDUM. Real effect-rows live in `cssl-effects`
+/// (28 built-in effects + Ω-substrate-rows + sub_effect_check + banned_composition).
+#[derive(Clone, Debug, Default, PartialEq, Eq)]
+pub struct EffectRow {
+    pub labels: std::collections::BTreeSet<String>,
+}
+
+impl EffectRow {
+    #[must_use]
+    pub fn empty() -> Self { Self::default() }
+    #[must_use]
+    pub fn singleton(label: String) -> Self {
+        let mut s = std::collections::BTreeSet::new();
+        s.insert(label);
+        Self { labels: s }
+    }
+    #[must_use]
+    pub fn union(mut self, other: Self) -> Self {
+        self.labels.extend(other.labels);
+        self
+    }
+    #[must_use]
+    pub fn is_pure(&self) -> bool { self.labels.is_empty() }
+    #[must_use]
+    pub fn contains(&self, label: &str) -> bool { self.labels.contains(label) }
+}
+
+/// Grade annotation on a binder.
+///
+/// Maps onto `cssl-grades::Linear` / `Affine` / `Unrestricted` semirings ; this
+/// enum is the surface-syntax form. Mapping happens during elaboration when
+/// usage counts are checked.
+#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
+pub enum Grade {
+    Linear,
+    Affine,
+    Unrestricted,
+}
+
+/// Surface-syntax term.
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub enum Term {
+    /// Variable reference.
+    Var(String),
+    /// λ-abstraction with a graded parameter.
+    Lam {
+        param: String,
+        grade: Grade,
+        body: Box<Term>,
+    },
+    /// Function application.
+    App(Box<Term>, Box<Term>),
+    /// Graded let-binding.
+    Let {
+        name: String,
+        grade: Grade,
+        value: Box<Term>,
+        body: Box<Term>,
+    },
+    /// Perform an effect operation labelled `label`.
+    Op(String),
+    /// Pure unit (no effects, no captures).
+    Unit,
+}
+
+/// Errors raised during elaboration.
+#[derive(Debug, Error, PartialEq, Eq)]
+pub enum ElabError {
+    /// Variable referenced but not in scope.
+    #[error("unbound variable `{0}`")]
+    UnboundVar(String),
+    /// Linearity discipline violated (e.g. linear var used twice or zero times).
+    #[error("linearity violation : `{var}` graded {grade:?} but used {used} time(s)")]
+    LinearityViolation {
+        var: String,
+        grade: Grade,
+        used: u32,
+    },
+}
+
+/// Result of elaborating a `Term`.
+#[derive(Clone, Debug)]
+pub struct Elaborated {
+    /// Hypergraph encoding of the elaborated term.
+    pub hgraph: HGraph,
+    /// `NodeId` of the root expression node within `hgraph`.
+    pub root: NodeId,
+    /// Effect-row accumulated over the term's effect operations.
+    pub effects: EffectRow,
+}
+
+impl Elaborated {
+    /// Content-Cid of the elaborated hypergraph.
+    #[must_use]
+    pub fn cid(&self) -> Cid {
+        self.hgraph.cid()
+    }
+}
+
+/// Elaborate a closed surface term.
+pub fn elaborate(term: &Term) -> Result<Elaborated, ElabError> {
+    let mut g = HGraph::new();
+    let mut env = Env::default();
+    let (root, effects) = elab_inner(term, &mut g, &mut env)?;
+    Ok(Elaborated { hgraph: g, root, effects })
+}
+
+#[derive(Default)]
+struct Env {
+    /// Stack of scopes ; innermost last.
+    scopes: Vec<Scope>,
+}
+
+struct Scope {
+    name: String,
+    grade: Grade,
+    binder_node: NodeId,
+    uses: u32,
+}
+
+impl Env {
+    fn push(&mut self, name: String, grade: Grade, binder_node: NodeId) {
+        self.scopes.push(Scope { name, grade, binder_node, uses: 0 });
+    }
+
+    fn pop_and_check(&mut self) -> Result<(), ElabError> {
+        let s = self.scopes.pop().expect("scope-stack underflow : elaborator bug");
+        check_grade(&s.name, s.grade, s.uses)
+    }
+
+    /// Look up a variable, incrementing its use count. Returns the binder's hgraph node.
+    fn lookup(&mut self, name: &str) -> Option<NodeId> {
+        for scope in self.scopes.iter_mut().rev() {
+            if scope.name == name {
+                scope.uses = scope.uses.saturating_add(1);
+                return Some(scope.binder_node);
+            }
+        }
+        None
+    }
+}
+
+fn check_grade(name: &str, grade: Grade, uses: u32) -> Result<(), ElabError> {
+    let ok = match grade {
+        Grade::Linear => uses == 1,
+        Grade::Affine => uses <= 1,
+        Grade::Unrestricted => true,
+    };
+    if ok {
+        Ok(())
+    } else {
+        Err(ElabError::LinearityViolation { var: name.into(), grade, used: uses })
+    }
+}
+
+/// Single placeholder type-cid until Wave U-B (type elaboration) lands.
+fn placeholder_type() -> TypeCid {
+    TypeCid(cid_of_bytes(b"cssl-elab::U-A::placeholder-type"))
+}
+
+fn elab_inner(
+    term: &Term,
+    g: &mut HGraph,
+    env: &mut Env,
+) -> Result<(NodeId, EffectRow), ElabError> {
+    let ty = placeholder_type();
+    match term {
+        Term::Unit => {
+            let n = g.add_node(ty, NodeLabel::Leaf("()".into()));
+            Ok((n, EffectRow::empty()))
+        }
+        Term::Var(name) => {
+            let binder = env
+                .lookup(name)
+                .ok_or_else(|| ElabError::UnboundVar(name.clone()))?;
+            let n = g.add_node(ty, NodeLabel::Leaf(name.clone()));
+            // Edge from var-occurrence to its binder.
+            g.add_edge(
+                EdgeKind::DataFlow,
+                &[
+                    Port { node: n, idx: 0, type_cid: ty },
+                    Port { node: binder, idx: 0, type_cid: ty },
+                ],
+            )
+            .expect("ports refer to just-added nodes");
+            Ok((n, EffectRow::empty()))
+        }
+        Term::Lam { param, grade, body } => {
+            let lam_node = g.add_node(ty, NodeLabel::Lam);
+            // Binder pseudo-node : a leaf labeled with the bound name + its grade.
+            let binder_label = format!("bind:{param}:{}", grade_tag(*grade));
+            let binder = g.add_node(ty, NodeLabel::Leaf(binder_label));
+            g.add_edge(
+                EdgeKind::Subterm,
+                &[
+                    Port { node: lam_node, idx: 0, type_cid: ty },
+                    Port { node: binder, idx: 0, type_cid: ty },
+                ],
+            )
+            .expect("ports valid");
+            env.push(param.clone(), *grade, binder);
+            let (body_node, body_effects) = elab_inner(body, g, env)?;
+            env.pop_and_check()?;
+            g.add_edge(
+                EdgeKind::Subterm,
+                &[
+                    Port { node: lam_node, idx: 0, type_cid: ty },
+                    Port { node: body_node, idx: 0, type_cid: ty },
+                ],
+            )
+            .expect("ports valid");
+            // λ suspends effects : the row of the lambda itself is empty ;
+            // the latent effects live on the body and surface when applied.
+            // For Wave U-A we conservatively keep the body-effects on the lambda
+            // node so callers see them ; refinement (effect-suspension) is U-B.
+            Ok((lam_node, body_effects))
+        }
+        Term::App(f, x) => {
+            let (fn_node, fn_eff) = elab_inner(f, g, env)?;
+            let (arg_node, arg_eff) = elab_inner(x, g, env)?;
+            let app_node = g.add_node(ty, NodeLabel::App);
+            g.add_edge(
+                EdgeKind::Subterm,
+                &[
+                    Port { node: app_node, idx: 0, type_cid: ty },
+                    Port { node: fn_node, idx: 0, type_cid: ty },
+                    Port { node: arg_node, idx: 0, type_cid: ty },
+                ],
+            )
+            .expect("ports valid");
+            Ok((app_node, fn_eff.union(arg_eff)))
+        }
+        Term::Let { name, grade, value, body } => {
+            let (val_node, val_eff) = elab_inner(value, g, env)?;
+            let binder_label = format!("let:{name}:{}", grade_tag(*grade));
+            let binder = g.add_node(ty, NodeLabel::Leaf(binder_label));
+            g.add_edge(
+                EdgeKind::DataFlow,
+                &[
+                    Port { node: binder, idx: 0, type_cid: ty },
+                    Port { node: val_node, idx: 0, type_cid: ty },
+                ],
+            )
+            .expect("ports valid");
+            env.push(name.clone(), *grade, binder);
+            let (body_node, body_eff) = elab_inner(body, g, env)?;
+            env.pop_and_check()?;
+            Ok((body_node, val_eff.union(body_eff)))
+        }
+        Term::Op(label) => {
+            let n = g.add_node(ty, NodeLabel::Custom(format!("op:{label}")));
+            let row = EffectRow::singleton(label.clone());
+            // Annotate the op-node with its effect label as a hyperedge so the
+            // hgraph itself is self-describing for downstream passes.
+            g.add_edge(
+                EdgeKind::EffectScope,
+                &[Port { node: n, idx: 0, type_cid: ty }],
+            )
+            .expect("ports valid");
+            Ok((n, row))
+        }
+    }
+}
+
+fn grade_tag(g: Grade) -> &'static str {
+    match g {
+        Grade::Linear => "L",
+        Grade::Affine => "A",
+        Grade::Unrestricted => "ω",
+    }
+}
+
+/// Convenience : count distinct effect-labels collected during elaboration of `t`.
+///
+/// For tooling / quick spot-checks. Production code should pattern-match
+/// `Elaborated::effects` directly.
+#[must_use]
+pub fn effect_label_count(t: &Term) -> usize {
+    elaborate(t)
+        .map(|e| e.effects.labels.len())
+        .unwrap_or(0)
+}
+
+/// Helper : count occurrences of a free variable inside a term (approximate ;
+/// does not respect shadowing — used for testing only).
+#[doc(hidden)]
+pub fn approx_free_uses(name: &str, t: &Term) -> u32 {
+    fn go(name: &str, t: &Term, shadowed: bool) -> u32 {
+        if shadowed {
+            return 0;
+        }
+        match t {
+            Term::Var(n) if n == name => 1,
+            Term::Var(_) | Term::Op(_) | Term::Unit => 0,
+            Term::Lam { param, body, .. } => go(name, body, param == name),
+            Term::App(f, x) => go(name, f, false) + go(name, x, false),
+            Term::Let { name: n, value, body, .. } => {
+                go(name, value, false) + go(name, body, n == name)
+            }
+        }
+    }
+    go(name, t, false)
+}
+
+/// Sanity helper : check whether `name` is in the elaborator's view of free vars
+/// (returns the binders-stack key set as a snapshot).
+#[doc(hidden)]
+#[must_use]
+pub fn free_var_names(t: &Term) -> Vec<String> {
+    let mut out = Vec::new();
+    let mut bound = HashMap::<String, u32>::new();
+    fn go(t: &Term, bound: &mut HashMap<String, u32>, out: &mut Vec<String>) {
+        match t {
+            Term::Var(n) => {
+                if !bound.contains_key(n) && !out.contains(n) {
+                    out.push(n.clone());
+                }
+            }
+            Term::Lam { param, body, .. } => {
+                *bound.entry(param.clone()).or_insert(0) += 1;
+                go(body, bound, out);
+                let e = bound.get_mut(param).expect("present");
+                *e -= 1;
+                if *e == 0 { bound.remove(param); }
+            }
+            Term::App(f, x) => { go(f, bound, out); go(x, bound, out); }
+            Term::Let { name, value, body, .. } => {
+                go(value, bound, out);
+                *bound.entry(name.clone()).or_insert(0) += 1;
+                go(body, bound, out);
+                let e = bound.get_mut(name).expect("present");
+                *e -= 1;
+                if *e == 0 { bound.remove(name); }
+            }
+            Term::Op(_) | Term::Unit => {}
+        }
+    }
+    go(t, &mut bound, &mut out);
+    out
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    fn var(s: &str) -> Term { Term::Var(s.into()) }
+    fn lam(p: &str, g: Grade, b: Term) -> Term {
+        Term::Lam { param: p.into(), grade: g, body: Box::new(b) }
+    }
+    fn app(f: Term, x: Term) -> Term { Term::App(Box::new(f), Box::new(x)) }
+    fn let_(n: &str, g: Grade, v: Term, b: Term) -> Term {
+        Term::Let { name: n.into(), grade: g, value: Box::new(v), body: Box::new(b) }
+    }
+    fn op(l: &str) -> Term { Term::Op(l.into()) }
+
+    #[test]
+    fn pure_unit_elaborates_to_empty_effect_row() {
+        let e = elaborate(&Term::Unit).unwrap();
+        assert!(e.effects.is_pure());
+        assert_eq!(e.hgraph.node_count(), 1);
+    }
+
+    #[test]
+    fn linear_var_used_exactly_once_succeeds() {
+        // λx:L. x
+        let t = lam("x", Grade::Linear, var("x"));
+        elaborate(&t).expect("linear-once must elaborate");
+    }
+
+    #[test]
+    fn linear_var_used_twice_fails() {
+        // λx:L. (x x)
+        let t = lam("x", Grade::Linear, app(var("x"), var("x")));
+        let err = elaborate(&t).unwrap_err();
+        assert!(matches!(err, ElabError::LinearityViolation { used: 2, .. }));
+    }
+
+    #[test]
+    fn linear_var_unused_fails() {
+        // λx:L. ()
+        let t = lam("x", Grade::Linear, Term::Unit);
+        let err = elaborate(&t).unwrap_err();
+        assert!(matches!(err, ElabError::LinearityViolation { used: 0, .. }));
+    }
+
+    #[test]
+    fn affine_var_unused_succeeds() {
+        // λx:A. ()
+        let t = lam("x", Grade::Affine, Term::Unit);
+        elaborate(&t).expect("affine-zero must elaborate");
+    }
+
+    #[test]
+    fn affine_var_used_twice_fails() {
+        // λx:A. (x x)
+        let t = lam("x", Grade::Affine, app(var("x"), var("x")));
+        let err = elaborate(&t).unwrap_err();
+        assert!(matches!(err, ElabError::LinearityViolation { used: 2, .. }));
+    }
+
+    #[test]
+    fn unrestricted_var_used_any_number_of_times() {
+        // λx:ω. (x x)
+        let t = lam("x", Grade::Unrestricted, app(var("x"), var("x")));
+        elaborate(&t).expect("unrestricted permits any count");
+    }
+
+    #[test]
+    fn unbound_var_fails() {
+        let err = elaborate(&var("x")).unwrap_err();
+        assert_eq!(err, ElabError::UnboundVar("x".into()));
+    }
+
+    #[test]
+    fn op_emits_effect_label_in_row() {
+        let t = op("io");
+        let e = elaborate(&t).unwrap();
+        assert!(e.effects.contains("io"));
+        assert!(!e.effects.is_pure());
+    }
+
+    #[test]
+    fn app_unions_effects_of_subterms() {
+        // (op io) (op state) — applies one effect-op to another.
+        let t = app(op("io"), op("state"));
+        let e = elaborate(&t).unwrap();
+        assert!(e.effects.contains("io"));
+        assert!(e.effects.contains("state"));
+    }
+
+    #[test]
+    fn let_unions_value_and_body_effects() {
+        // let x:ω = op io in op state
+        let t = let_("x", Grade::Unrestricted, op("io"), op("state"));
+        let e = elaborate(&t).unwrap();
+        assert!(e.effects.contains("io"));
+        assert!(e.effects.contains("state"));
+    }
+
+    #[test]
+    fn elaborated_cid_is_deterministic_across_runs() {
+        let t = lam("x", Grade::Linear, var("x"));
+        let e1 = elaborate(&t).unwrap();
+        let e2 = elaborate(&t).unwrap();
+        assert_eq!(e1.cid(), e2.cid());
+    }
+
+    #[test]
+    fn shadowing_does_not_leak_uses_to_outer_binder() {
+        // λx:L. (λx:L. x) x
+        let inner = lam("x", Grade::Linear, var("x"));
+        let t = lam("x", Grade::Linear, app(inner, var("x")));
+        // Outer x is used once (in `x` after the inner lam) ;
+        // inner x is used once (in its body). Both linear-once = OK.
+        elaborate(&t).expect("nested same-named linear binders elaborate");
+    }
+
+    #[test]
+    fn nested_unbound_inside_lambda_is_reported() {
+        // λx:ω. y
+        let t = lam("x", Grade::Unrestricted, var("y"));
+        let err = elaborate(&t).unwrap_err();
+        assert_eq!(err, ElabError::UnboundVar("y".into()));
+    }
+
+    #[test]
+    fn approx_free_uses_helper_counts_correctly() {
+        // (x x) — x free, used twice
+        let t = app(var("x"), var("x"));
+        assert_eq!(approx_free_uses("x", &t), 2);
+        // λx. x — x bound, zero free uses
+        let t = lam("x", Grade::Unrestricted, var("x"));
+        assert_eq!(approx_free_uses("x", &t), 0);
+    }
+
+    #[test]
+    fn free_var_names_excludes_bound() {
+        // λx. (x y)
+        let t = lam("x", Grade::Unrestricted, app(var("x"), var("y")));
+        let frees = free_var_names(&t);
+        assert_eq!(frees, vec!["y".to_string()]);
+    }
+}
diff --git a/compiler-rs/crates/cssl-lower-iccombs/Cargo.toml b/compiler-rs/crates/cssl-lower-iccombs/Cargo.toml
new file mode 100644
index 0000000..f022bba
--- /dev/null
+++ b/compiler-rs/crates/cssl-lower-iccombs/Cargo.toml
@@ -0,0 +1,17 @@
+[package]
+name         = "cssl-lower-iccombs"
+version.workspace      = true
+edition.workspace      = true
+rust-version.workspace = true
+license.workspace      = true
+authors.workspace      = true
+description  = "Lower cssl-iccombs-toy-elab λ-terms to cssl-iccombs interaction nets — Lafont/Mackie SIC encoding for the LINEAR fragment (Wave U-D per IMPL_01_PLAN.csl + IMPL_06_CORRIGENDUM ; iccombs demo-harness L1→L3)."
+repository.workspace   = true
+
+[dependencies]
+cssl-iccombs-toy-elab = { path = "../cssl-iccombs-toy-elab" }
+cssl-iccombs          = { path = "../cssl-iccombs" }
+thiserror.workspace = true
+
+[lints]
+workspace = true
diff --git a/compiler-rs/crates/cssl-lower-iccombs/src/lib.rs b/compiler-rs/crates/cssl-lower-iccombs/src/lib.rs
new file mode 100644
index 0000000..6968e13
--- /dev/null
+++ b/compiler-rs/crates/cssl-lower-iccombs/src/lib.rs
@@ -0,0 +1,228 @@
+#![forbid(unsafe_code)]
+#![doc = "cssl-lower-iccombs — Lafont/Mackie symmetric-interaction-combinator encoding\n\
+of the LINEAR fragment of cssl-iccombs-toy-elab's surface λ-calculus.\n\n\
+Encoding (λ_lin → SIC) :\n\
+  • Lam(x, body)   ↦ Con node ; principal=output ; aux1=variable-port (env[x]) ;\n\
+                       aux2 ← linked to body's output\n\
+  • App(f, arg)    ↦ Con node ; principal ← linked to f's output ;\n\
+                       aux1 ← linked to arg's output ; aux2=result port (returned)\n\
+  • Var(x)         ↦ env[x] (the binder's aux1 port) — exactly-once linear use\n\
+  • Unit           ↦ Era node ; return its principal port\n\
+  • Let(x,v,b)     ↦ desugars to App(Lam(x, b), v)\n\n\
+Out of scope (returns `LowerError::UnsupportedGrade` / `UnsupportedTerm`) :\n\
+  • Affine / Unrestricted binders → would require Era for unused, Dup-tree for\n\
+    multi-use ; deferred to a follow-up pass that performs erasure-Era / share-Dup\n\
+    insertion based on use-counts.\n\
+  • `Op(_)` effectful primitives → no SIC encoding ; effects must be discharged\n\
+    via cssl-effects::banned_composition + cssl-ifc::validate_egress at HIR-level\n\
+    before lowering (per IMPL_06_CORRIGENDUM Wave U-G revision), or thunked into a runtime-call\n\
+    combinator (deferred).\n\n\
+Spec : `specs/Upgrade/impl/IMPL_01_PLAN.csl` § Wave U-D ; `IMPL_02_FOUNDATION.csl`\n\
+§ cssl-iccombs."]
+
+use cssl_iccombs_toy_elab::{Grade, Term};
+use cssl_iccombs::{AgentKind, Net, PortRef};
+use std::collections::HashMap;
+
+/// Lowering error.
+#[derive(Debug, thiserror::Error)]
+pub enum LowerError {
+    /// Variable referenced but not in scope (would be caught by elab too).
+    #[error("unbound variable `{0}`")]
+    UnboundVar(String),
+    /// Linear fragment only ; affine / unrestricted require Dup/Era insertion.
+    #[error("unsupported grade {0:?} (linear fragment only ; Affine/Unrestricted deferred)")]
+    UnsupportedGrade(Grade),
+    /// Effectful primitive ; must be discharged before lowering or wrapped in a runtime combinator.
+    #[error("unsupported term : `Op({0})` is effectful and has no pure-SIC encoding")]
+    UnsupportedTerm(String),
+}
+
+/// Result of lowering : the net + the principal output port of the term.
+#[derive(Debug)]
+pub struct Lowered {
+    pub net: Net,
+    pub root: PortRef,
+}
+
+/// Lower a `Term` to an interaction net (linear fragment only).
+///
+/// The returned `root` port is the term's "output" — typically the lambda's
+/// principal port or the application's result-port.
+///
+/// # Errors
+///
+/// Returns `LowerError::UnsupportedGrade` for non-Linear binders, or
+/// `LowerError::UnsupportedTerm` for `Op(_)` primitives.
+pub fn lower(term: &Term) -> Result<Lowered, LowerError> {
+    let mut net = Net::new();
+    let mut env: HashMap<String, PortRef> = HashMap::new();
+    let root = lower_inner(&mut net, &mut env, term)?;
+    Ok(Lowered { net, root })
+}
+
+fn lower_inner(
+    net: &mut Net,
+    env: &mut HashMap<String, PortRef>,
+    term: &Term,
+) -> Result<PortRef, LowerError> {
+    match term {
+        Term::Unit => {
+            let era = net.add_agent(AgentKind::Era);
+            Ok(PortRef::Port(era, 0))
+        }
+        Term::Var(name) => env
+            .get(name)
+            .copied()
+            .ok_or_else(|| LowerError::UnboundVar(name.clone())),
+        Term::Lam { param, grade, body } => {
+            if *grade != Grade::Linear {
+                return Err(LowerError::UnsupportedGrade(*grade));
+            }
+            let con = net.add_agent(AgentKind::Con);
+            let var_port = PortRef::Port(con, 1);
+            let principal = PortRef::Port(con, 0);
+            let body_port_2 = PortRef::Port(con, 2);
+            let prev = env.insert(param.clone(), var_port);
+            let body_out = lower_inner(net, env, body)?;
+            // Restore shadowed binding (or remove ours).
+            match prev {
+                Some(p) => { env.insert(param.clone(), p); }
+                None    => { env.remove(param); }
+            }
+            net.link(body_out, body_port_2);
+            Ok(principal)
+        }
+        Term::App(f, x) => {
+            let con = net.add_agent(AgentKind::Con);
+            let principal = PortRef::Port(con, 0);
+            let arg_port = PortRef::Port(con, 1);
+            let result   = PortRef::Port(con, 2);
+            let f_out = lower_inner(net, env, f)?;
+            net.link(f_out, principal);
+            let x_out = lower_inner(net, env, x)?;
+            net.link(x_out, arg_port);
+            Ok(result)
+        }
+        Term::Let { name, grade, value, body } => {
+            // Desugar : (let x g v b) ≡ (app (lam x g b) v)
+            let lam = Term::Lam {
+                param: name.clone(),
+                grade: *grade,
+                body: body.clone(),
+            };
+            let desugared = Term::App(Box::new(lam), value.clone());
+            lower_inner(net, env, &desugared)
+        }
+        Term::Op(label) => Err(LowerError::UnsupportedTerm(label.clone())),
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use cssl_iccombs::ReduceResult;
+
+    fn lin_lam(param: &str, body: Term) -> Term {
+        Term::Lam { param: param.into(), grade: Grade::Linear, body: Box::new(body) }
+    }
+
+    #[test]
+    fn lower_unit_yields_one_era() {
+        let l = lower(&Term::Unit).unwrap();
+        assert_eq!(l.net.agent_count(), 1);
+        assert!(matches!(l.root, PortRef::Port(_, 0)));
+    }
+
+    #[test]
+    fn lower_linear_identity() {
+        // λx.x : a single Con whose aux1 = body output (= var-port itself) linked to aux2.
+        let id = lin_lam("x", Term::Var("x".into()));
+        let l = lower(&id).unwrap();
+        assert_eq!(l.net.agent_count(), 1);
+        assert!(matches!(l.root, PortRef::Port(_, 0)));
+    }
+
+    #[test]
+    fn lower_application_creates_two_cons() {
+        // ((λx.x) ()) : 1 Con (lambda) + 1 Con (app) + 1 Era (unit) = 3 agents
+        let id = lin_lam("x", Term::Var("x".into()));
+        let app = Term::App(Box::new(id), Box::new(Term::Unit));
+        let l = lower(&app).unwrap();
+        assert_eq!(l.net.agent_count(), 3);
+    }
+
+    #[test]
+    fn lower_identity_applied_to_unit_reduces_to_normal_form() {
+        // ((λx.x) ()) : the Con-Con annihilation between λ and app fires ; then Con-Era erasure ;
+        // any further reductions until normal form. The exact final form depends on how we
+        // expose the result — here we just verify it terminates.
+        let id = lin_lam("x", Term::Var("x".into()));
+        let app = Term::App(Box::new(id), Box::new(Term::Unit));
+        let mut l = lower(&app).unwrap();
+        let r = l.net.reduce_to_normal_form(64);
+        assert_eq!(r, ReduceResult::NormalForm);
+    }
+
+    #[test]
+    fn lower_let_desugars_to_application() {
+        // (let x L () x)  ≡  ((λx.x) ())  → 3 agents
+        let t = Term::Let {
+            name: "x".into(),
+            grade: Grade::Linear,
+            value: Box::new(Term::Unit),
+            body: Box::new(Term::Var("x".into())),
+        };
+        let l = lower(&t).unwrap();
+        assert_eq!(l.net.agent_count(), 3);
+    }
+
+    #[test]
+    fn lower_rejects_affine_binder() {
+        let t = Term::Lam {
+            param: "x".into(),
+            grade: Grade::Affine,
+            body: Box::new(Term::Unit),
+        };
+        let err = lower(&t).unwrap_err();
+        assert!(matches!(err, LowerError::UnsupportedGrade(Grade::Affine)));
+    }
+
+    #[test]
+    fn lower_rejects_unrestricted_binder() {
+        let t = Term::Lam {
+            param: "x".into(),
+            grade: Grade::Unrestricted,
+            body: Box::new(Term::Unit),
+        };
+        let err = lower(&t).unwrap_err();
+        assert!(matches!(err, LowerError::UnsupportedGrade(Grade::Unrestricted)));
+    }
+
+    #[test]
+    fn lower_rejects_op_primitive() {
+        let err = lower(&Term::Op("io".into())).unwrap_err();
+        assert!(matches!(err, LowerError::UnsupportedTerm(_)));
+    }
+
+    #[test]
+    fn lower_rejects_unbound_var() {
+        let err = lower(&Term::Var("oops".into())).unwrap_err();
+        assert!(matches!(err, LowerError::UnboundVar(_)));
+    }
+
+    #[test]
+    fn lower_nested_linear_lambdas() {
+        // λx.λy.x  is NOT linear (y is unused) — but for THIS test we want a use of both,
+        // so : λx.λy.(y x)  ≈  swap. Both vars used exactly once.
+        let inner = Term::App(
+            Box::new(Term::Var("y".into())),
+            Box::new(Term::Var("x".into())),
+        );
+        let lam_y = lin_lam("y", inner);
+        let lam_x = lin_lam("x", lam_y);
+        let l = lower(&lam_x).unwrap();
+        // 2 lambdas + 1 application = 3 Con agents, no Eras
+        assert_eq!(l.net.agent_count(), 3);
+    }
+}