diff --git a/crates/my-lang/Cargo.toml b/crates/my-lang/Cargo.toml index 71897ae..836f1ed 100644 --- a/crates/my-lang/Cargo.toml +++ b/crates/my-lang/Cargo.toml @@ -16,6 +16,7 @@ name = "my" path = "src/main.rs" [dependencies] +my-qtt.workspace = true thiserror.workspace = true anyhow.workspace = true serde = { workspace = true, optional = true } diff --git a/crates/my-lang/src/lib.rs b/crates/my-lang/src/lib.rs index bc0f9bb..49103dc 100644 --- a/crates/my-lang/src/lib.rs +++ b/crates/my-lang/src/lib.rs @@ -23,6 +23,7 @@ pub mod scope; pub mod stdlib; pub mod token; pub mod types; +pub mod qtt_bridge; // Library modules (common utilities and language-specific features) #[path = "../lib/mod.rs"] diff --git a/crates/my-lang/src/qtt_bridge.rs b/crates/my-lang/src/qtt_bridge.rs new file mode 100644 index 0000000..fde5146 --- /dev/null +++ b/crates/my-lang/src/qtt_bridge.rs @@ -0,0 +1,261 @@ +// SPDX-License-Identifier: MPL-2.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell + +//! # `qtt_bridge` — lower the my-lang surface AST onto the verified QTT core +//! +//! Coupling **step 2b**: the actual lowering of the running compiler's +//! [`crate::ast::Expr`]/[`crate::ast::Type`] onto [`my_qtt::surface::SExpr`], so +//! that the machine-checked QTT usage-walk (`my-qtt`, the faithful port of the +//! Coq `check`) can be run on real my-lang programs. With `my-qtt` now in +//! my-lang's dependency graph, the proofs' own algorithm is *in the compiler*. +//! +//! ## Scope (honest) +//! Only the **resource-relevant fragment** lowers: variables, λ, application, +//! `let`/block bindings, and literals (as opaque values). Everything else +//! (binary/unary ops, `match`, records, AI expressions, `try`, `restrict`, …) +//! returns [`BridgeError::Unsupported`] — these are follow-on work, not silent +//! passes. Base/opaque types (`Int`/`String`/…/records/effects) carry no +//! resource content and map to `Unit`; function and tuple types map +//! structurally (`->` to the affine arrow, tuples to `⊗`). +//! +//! ## The quantity default +//! The Coq `check` is **exact-usage**: a binder's declared quantity must equal +//! its realised usage. The my-lang `Param` has no quantity syntax yet, so this +//! bridge applies the **linear** reading ([`DEFAULT_Q`]` = One`): every binder +//! must be used *exactly once*. That is the strictest QTT discipline — it makes +//! [`check_expr`] genuinely *enforce* linearity on the real AST (a dropped or +//! duplicated binder is rejected by the verified walk), and it is the most +//! faithful demonstration of the coupling. Real per-binder quantities await +//! `Param` gaining quantity annotations (a small parser+AST follow-on); the +//! engine already threads whatever quantity it is given, so that change +//! activates here with no rewrite. + +use crate::ast::{Block, Expr, LambdaBody, Stmt, Type}; +use my_qtt::surface::{check_surface, CheckError, SExpr, STy}; +use my_qtt::{Q, Ty, Uvec}; + +/// The quantity assigned to every surface binder pending quantity syntax — the +/// linear reading (`One` = used exactly once). See the module docs. +pub const DEFAULT_Q: Q = Q::One; + +/// A surface construct outside the resource-relevant fragment. +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum BridgeError { + Unsupported(&'static str), +} + +/// Lower a surface type to a core resource type. Opaque base types map to +/// `Unit` (no resource content); `->` and tuples map structurally. +pub fn lower_ty(t: &Type) -> STy { + match t { + Type::Function { param, result, .. } => { + STy::Arr(DEFAULT_Q, Box::new(lower_ty(param)), Box::new(lower_ty(result))) + } + Type::Tuple { elements, .. } => lower_tuple(elements), + Type::Reference { inner, .. } => lower_ty(inner), + // Primitive / Named / Effect / Ai / Array / Record / Constrained: opaque. + _ => STy::Unit, + } +} + +fn lower_tuple(elems: &[Type]) -> STy { + match elems { + [] => STy::Unit, + [t] => lower_ty(t), + [t, rest @ ..] => STy::Tensor(Box::new(lower_ty(t)), Box::new(lower_tuple(rest))), + } +} + +/// Lower a surface expression to the named-variable core fragment. +pub fn lower_expr(e: &Expr) -> Result { + Ok(match e { + Expr::Ident(id) => SExpr::Var(id.name.clone()), + // a literal is a value with no resource content. + Expr::Literal(_) => SExpr::Unit, + Expr::Lambda { params, body, .. } => { + let inner = match body { + LambdaBody::Expr(e) => lower_expr(e)?, + LambdaBody::Block(b) => lower_block(b)?, + }; + // right-fold params: `|x, y| body` -> `Lam x (Lam y body)` + let mut acc = inner; + for p in params.iter().rev() { + acc = SExpr::Lam { + q: DEFAULT_Q, + param: p.name.name.clone(), + ty: lower_ty(&p.ty), + body: Box::new(acc), + }; + } + acc + } + Expr::Call { callee, args, .. } => { + // `f(a, b)` -> `App (App f a) b` + let mut acc = lower_expr(callee)?; + for a in args { + acc = SExpr::App(Box::new(acc), Box::new(lower_expr(a)?)); + } + acc + } + Expr::Block(b) => lower_block(b)?, + Expr::Binary { .. } => return Err(BridgeError::Unsupported("binary op")), + Expr::Unary { .. } => return Err(BridgeError::Unsupported("unary op")), + Expr::Field { .. } => return Err(BridgeError::Unsupported("field access")), + Expr::Try { .. } => return Err(BridgeError::Unsupported("try")), + Expr::Restrict { .. } => return Err(BridgeError::Unsupported("restrict")), + Expr::Ai(_) => return Err(BridgeError::Unsupported("AI expression")), + Expr::Match { .. } => return Err(BridgeError::Unsupported("match (use a 2-arm sum case)")), + Expr::Array { .. } => return Err(BridgeError::Unsupported("array literal")), + Expr::Record { .. } => return Err(BridgeError::Unsupported("record literal")), + }) +} + +/// Lower a block: `let` statements become nested core `let`s; a trailing +/// expression statement is the block's value (an empty block is `unit`). Other +/// statement forms (control flow, non-final non-`let` statements) are out of +/// the resource fragment. +pub fn lower_block(b: &Block) -> Result { + lower_stmts(&b.stmts) +} + +fn lower_stmts(stmts: &[Stmt]) -> Result { + match stmts { + [] => Ok(SExpr::Unit), + [Stmt::Expr(e)] => lower_expr(e), + [Stmt::Let { name, value, .. }, rest @ ..] => Ok(SExpr::Let { + q: DEFAULT_Q, + name: name.name.clone(), + value: Box::new(lower_expr(value)?), + body: Box::new(lower_stmts(rest)?), + }), + _ => Err(BridgeError::Unsupported("block statement form")), + } +} + +/// Lowering or checking failure. +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum BridgeCheckError { + /// The surface construct is outside the resource fragment. + Bridge(BridgeError), + /// Lowered, but the verified usage-walk rejected it (ill-typed, or — under + /// the linear default — a binder dropped or duplicated). + Check(CheckError), +} + +/// Lower a surface expression and run the **machine-checked** QTT usage-walk on +/// it. The running compiler's hook into the proofs' own resource discipline. +pub fn check_expr(e: &Expr) -> Result<(Ty, Uvec), BridgeCheckError> { + let s = lower_expr(e).map_err(BridgeCheckError::Bridge)?; + check_surface(&s).map_err(BridgeCheckError::Check) +} + +#[cfg(test)] +mod tests { + use super::*; + use crate::ast::{Expr, Ident, Literal, Param, PrimitiveType}; + use crate::token::Span; + use my_qtt::surface::ElabError; + + fn sp() -> Span { + Span { start: 0, end: 0, line: 0, column: 0 } + } + fn id(n: &str) -> Ident { + Ident::new(n, sp()) + } + fn param(n: &str, ty: Type) -> Param { + Param { name: id(n), ty, span: sp() } + } + + /// A real `ast::Expr::Lambda` `|x: Int| x` lowers and is accepted: the + /// linear binder is used exactly once. The verified engine now runs on the + /// compiler's actual AST. + #[test] + fn real_linear_lambda_accepted() { + let lam = Expr::Lambda { + params: vec![param("x", Type::Primitive(PrimitiveType::Int))], + body: LambdaBody::Expr(Box::new(Expr::Ident(id("x")))), + span: sp(), + }; + let r = check_expr(&lam); + assert!(r.is_ok(), "expected ok, got {:?}", r); + // Int is opaque (Unit); the arrow carries the linear quantity. + assert!(matches!(r.unwrap().0, Ty::Arr(Q::One, _, _))); + } + + /// `|x: Int| { 0 }` drops the linear binder `x` → rejected by the verified + /// walk. Linearity is enforced on the real AST. + #[test] + fn real_dropping_lambda_rejected() { + let lam = Expr::Lambda { + params: vec![param("x", Type::Primitive(PrimitiveType::Int))], + body: LambdaBody::Block(Block { + stmts: vec![Stmt::Expr(Expr::Literal(Literal::Int(0, sp())))], + span: sp(), + }), + span: sp(), + }; + assert_eq!( + check_expr(&lam), + Err(BridgeCheckError::Check(CheckError::Untypable)) + ); + } + + /// A block `{ let z = 0; z }` lowers to a core `let` and checks (z used once). + #[test] + fn real_block_let_accepted() { + let blk = Expr::Block(Block { + stmts: vec![ + Stmt::Let { + mutable: false, + name: id("z"), + ty: None, + value: Expr::Literal(Literal::Int(0, sp())), + span: sp(), + }, + Stmt::Expr(Expr::Ident(id("z"))), + ], + span: sp(), + }); + assert!(check_expr(&blk).is_ok()); + } + + /// A free identifier is an elaboration error, surfaced through the bridge. + #[test] + fn real_unbound_ident() { + assert_eq!( + check_expr(&Expr::Ident(id("free"))), + Err(BridgeCheckError::Check(CheckError::Elab(ElabError::Unbound( + "free".into() + )))) + ); + } + + /// Out-of-fragment constructs are reported, not silently accepted. + #[test] + fn unsupported_is_reported() { + let field = Expr::Field { + object: Box::new(Expr::Ident(id("r"))), + field: id("f"), + span: sp(), + }; + assert_eq!( + check_expr(&field), + Err(BridgeCheckError::Bridge(BridgeError::Unsupported("field access"))) + ); + } + + /// Function and tuple types lower structurally; base types are opaque `Unit`. + #[test] + fn type_lowering() { + assert_eq!(lower_ty(&Type::Primitive(PrimitiveType::Int)), STy::Unit); + let f = Type::Function { + param: Box::new(Type::Primitive(PrimitiveType::Int)), + result: Box::new(Type::Primitive(PrimitiveType::Bool)), + span: sp(), + }; + assert_eq!( + lower_ty(&f), + STy::Arr(Q::One, Box::new(STy::Unit), Box::new(STy::Unit)) + ); + } +} diff --git a/crates/my-qtt/src/lib.rs b/crates/my-qtt/src/lib.rs index 90d680a..9bb3079 100644 --- a/crates/my-qtt/src/lib.rs +++ b/crates/my-qtt/src/lib.rs @@ -35,6 +35,8 @@ #![forbid(unsafe_code)] +pub mod surface; + /// Quantities: the three-point affine semiring `{0, 1, ω}` (Coq `Quantity.Q`). #[derive(Debug, Clone, Copy, PartialEq, Eq)] pub enum Q { diff --git a/crates/my-qtt/src/surface.rs b/crates/my-qtt/src/surface.rs new file mode 100644 index 0000000..0ff324b --- /dev/null +++ b/crates/my-qtt/src/surface.rs @@ -0,0 +1,291 @@ +// SPDX-License-Identifier: MPL-2.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell + +//! # `surface` — named-variable elaboration onto the QTT core +//! +//! Coupling **step 2**: the bridge from a *named* surface to the de Bruijn +//! [`crate::Tm`] that the verified [`crate::check`] consumes, so the running +//! compiler can enforce the QTT resource axis on real programs (today its +//! `checker.rs` has none — `proofs/STATUS.md`). +//! +//! [`SExpr`]/[`STy`] are the **resource-relevant fragment** of the my-lang +//! surface `ast::Expr`/`ast::Type` (variables, λ with a quantity, application, +//! the two products, sums, `let`, the echo residue) — the schema the my-lang +//! frontend lowers onto (see the `ast::Expr → SExpr` lowering, the thin +//! mechanical follow-on). The non-resource surface (AI models, prompts, +//! records, …) carries no usage content and is out of this fragment. +//! +//! Elaboration is a scope-resolution pass: names become de Bruijn indices +//! against a [`Scope`] (innermost binder last, matching [`crate::Tctx`]). Types +//! have no binders, so [`elaborate_ty`] is purely structural. After elaboration +//! [`check_surface`] runs the verified usage-walk — so a linear binder dropped +//! at the *surface* is rejected by the *machine-checked* algorithm. +//! +//! Quantities are explicit on [`SExpr`] binders. Because the current my-lang +//! `Param` has no quantity syntax, the `ast` lowering will default binders +//! (documented at the lowering site); this engine already threads whatever +//! quantity the surface supplies, so adding the syntax later needs no change +//! here. + +use crate::{check, Mode, Q, Ty, Tm, Uvec}; + +/// Resource-relevant surface types (named-free; mirror of the QTT core types). +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum STy { + Unit, + With(Box, Box), + Tensor(Box, Box), + Sum(Box, Box), + /// `(q x : a) -> b` + Arr(Q, Box, Box), + Echo(Mode, Box, Box), +} + +/// Resource-relevant surface terms with **named** binders. +#[derive(Debug, Clone, PartialEq)] +pub enum SExpr { + Var(String), + Unit, + /// `|q x : ty| body` + Lam { + q: Q, + param: String, + ty: STy, + body: Box, + }, + App(Box, Box), + /// additive pair `` (shared usage) + With(Box, Box), + Fst(Box), + Snd(Box), + /// multiplicative pair `(e1, e2)` (split usage) + Tensor(Box, Box), + /// `let (x, y) = pair in body` + LetPair { + x: String, + y: String, + pair: Box, + body: Box, + }, + /// `inl[other] e` — `other` is the RIGHT summand annotation + Inl(STy, Box), + /// `inr[other] e` — `other` is the LEFT summand annotation + Inr(STy, Box), + /// `case scrut of inl xl => arm_l | inr xr => arm_r` + Case { + scrut: Box, + xl: String, + arm_l: Box, + xr: String, + arm_r: Box, + }, + /// `let (q name) = value in body` + Let { + q: Q, + name: String, + value: Box, + body: Box, + }, + /// echo residue `[mode] echo b>(witness)` + Echo { + mode: Mode, + a: STy, + b: STy, + witness: Box, + }, + Weaken(Box), +} + +/// A lexical scope: binder names, **innermost last** (so the de Bruijn index of +/// a name is its distance from the end). Aligns with [`crate::Tctx`]. +pub type Scope = Vec; + +/// Elaboration failures (the surface fragment is otherwise total). +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum ElabError { + /// A name with no binder in scope. + Unbound(String), +} + +/// Translate a surface type to the core (purely structural — no binders). +pub fn elaborate_ty(t: &STy) -> Ty { + match t { + STy::Unit => Ty::Unit, + STy::With(a, b) => Ty::With(Box::new(elaborate_ty(a)), Box::new(elaborate_ty(b))), + STy::Tensor(a, b) => Ty::Tensor(Box::new(elaborate_ty(a)), Box::new(elaborate_ty(b))), + STy::Sum(a, b) => Ty::Sum(Box::new(elaborate_ty(a)), Box::new(elaborate_ty(b))), + STy::Arr(q, a, b) => Ty::Arr(*q, Box::new(elaborate_ty(a)), Box::new(elaborate_ty(b))), + STy::Echo(m, a, b) => Ty::Echo(*m, Box::new(elaborate_ty(a)), Box::new(elaborate_ty(b))), + } +} + +fn lookup(scope: &Scope, name: &str) -> Option { + // de Bruijn index = distance from the innermost (last) binder. + scope.iter().rev().position(|n| n == name) +} + +/// Resolve names to de Bruijn indices, producing a core [`Tm`]. `scope` holds +/// the enclosing binders (innermost last); it is restored on return. +pub fn elaborate(e: &SExpr, scope: &mut Scope) -> Result { + Ok(match e { + SExpr::Var(name) => { + Tm::Var(lookup(scope, name).ok_or_else(|| ElabError::Unbound(name.clone()))?) + } + SExpr::Unit => Tm::UnitT, + SExpr::Lam { q, param, ty, body } => { + scope.push(param.clone()); + let body = elaborate(body, scope); + scope.pop(); + Tm::Lam(*q, elaborate_ty(ty), Box::new(body?)) + } + SExpr::App(f, a) => Tm::App( + Box::new(elaborate(f, scope)?), + Box::new(elaborate(a, scope)?), + ), + SExpr::With(x, y) => Tm::With( + Box::new(elaborate(x, scope)?), + Box::new(elaborate(y, scope)?), + ), + SExpr::Fst(p) => Tm::Fst(Box::new(elaborate(p, scope)?)), + SExpr::Snd(p) => Tm::Snd(Box::new(elaborate(p, scope)?)), + SExpr::Tensor(x, y) => Tm::Tensor( + Box::new(elaborate(x, scope)?), + Box::new(elaborate(y, scope)?), + ), + SExpr::LetPair { x, y, pair, body } => { + let pair = elaborate(pair, scope)?; + scope.push(x.clone()); // index 1 in body + scope.push(y.clone()); // index 0 in body (innermost) + let body = elaborate(body, scope); + scope.pop(); + scope.pop(); + Tm::LetPair(Box::new(pair), Box::new(body?)) + } + SExpr::Inl(other, e) => Tm::Inl(elaborate_ty(other), Box::new(elaborate(e, scope)?)), + SExpr::Inr(other, e) => Tm::Inr(elaborate_ty(other), Box::new(elaborate(e, scope)?)), + SExpr::Case { scrut, xl, arm_l, xr, arm_r } => { + let scrut = elaborate(scrut, scope)?; + scope.push(xl.clone()); + let arm_l = elaborate(arm_l, scope); + scope.pop(); + scope.push(xr.clone()); + let arm_r = elaborate(arm_r, scope); + scope.pop(); + Tm::Case(Box::new(scrut), Box::new(arm_l?), Box::new(arm_r?)) + } + SExpr::Let { q, name, value, body } => { + let value = elaborate(value, scope)?; + scope.push(name.clone()); + let body = elaborate(body, scope); + scope.pop(); + Tm::Let(*q, Box::new(value), Box::new(body?)) + } + SExpr::Echo { mode, a, b, witness } => Tm::MkEcho( + *mode, + elaborate_ty(a), + elaborate_ty(b), + Box::new(elaborate(witness, scope)?), + ), + SExpr::Weaken(e) => Tm::Weaken(Box::new(elaborate(e, scope)?)), + }) +} + +/// Outcome of resource-checking a closed surface term. +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum CheckError { + /// Elaboration failed (e.g. an unbound name). + Elab(ElabError), + /// Elaborated, but the verified usage-walk rejected it (ill-typed or a + /// linear binder dropped/duplicated). + Untypable, +} + +/// Elaborate a **closed** surface term and run the verified usage-walk. On +/// success returns its type and exact realised usage (empty for a closed term). +/// This is the running compiler's hook into the machine-checked QTT discipline. +pub fn check_surface(e: &SExpr) -> Result<(Ty, Uvec), CheckError> { + let mut scope = Scope::new(); + let tm = elaborate(e, &mut scope).map_err(CheckError::Elab)?; + check(&[], &tm).ok_or(CheckError::Untypable) +} + +#[cfg(test)] +mod tests { + use super::*; + use Q::*; + + fn b(x: T) -> Box { + Box::new(x) + } + fn lam(q: Q, p: &str, ty: STy, body: SExpr) -> SExpr { + SExpr::Lam { q, param: p.into(), ty, body: b(body) } + } + fn var(n: &str) -> SExpr { + SExpr::Var(n.into()) + } + + /// `|1 x : Unit| x` — the linear identity elaborates and checks; the usage + /// axis is now enforced on a NAMED surface term by the verified walk. + #[test] + fn linear_identity_ok() { + let id = lam(One, "x", STy::Unit, var("x")); + assert_eq!( + check_surface(&id), + Ok((Ty::Arr(One, b(Ty::Unit), b(Ty::Unit)), vec![])) + ); + } + + /// `|1 x : Unit| unit` — a linear binder dropped at the surface is REJECTED + /// (the coupling's whole point: the surface inherits the proof's discipline). + #[test] + fn linear_drop_rejected() { + let drop = lam(One, "x", STy::Unit, SExpr::Unit); + assert_eq!(check_surface(&drop), Err(CheckError::Untypable)); + } + + /// `|ω x : Unit| (x, x)` — the same body under an `ω` binder is accepted, so + /// the rejection above is exactly the linearity check, not a parse error. + #[test] + fn omega_dup_ok() { + let dup = lam(Omega, "x", STy::Unit, SExpr::Tensor(b(var("x")), b(var("x")))); + assert!(matches!(check_surface(&dup), Ok((Ty::Arr(Omega, _, _), _)))); + } + + /// Nested binders resolve to the right de Bruijn indices. `|1 x| |1 y| (x, y)` + /// uses BOTH exactly once → accepted; `|1 x| |1 y| y` drops the outer `x` → + /// linear-rejected. (Each non-trivial term uses each linear binder exactly + /// once, so resolution and the usage walk are both exercised.) + #[test] + fn scope_resolution() { + let both = lam( + One, + "x", + STy::Unit, + lam(One, "y", STy::Unit, SExpr::Tensor(b(var("x")), b(var("y")))), + ); + assert!(check_surface(&both).is_ok()); + let drop_outer = lam(One, "x", STy::Unit, lam(One, "y", STy::Unit, var("y"))); + assert_eq!(check_surface(&drop_outer), Err(CheckError::Untypable)); + } + + /// `let (1 z) = unit in z` — a linear `let` used once is accepted. + #[test] + fn linear_let_ok() { + let e = SExpr::Let { + q: One, + name: "z".into(), + value: b(SExpr::Unit), + body: b(var("z")), + }; + assert_eq!(check_surface(&e), Ok((Ty::Unit, vec![]))); + } + + /// An unbound name is an elaboration error, distinct from ill-typed. + #[test] + fn unbound_is_elab_error() { + assert_eq!( + check_surface(&var("nope")), + Err(CheckError::Elab(ElabError::Unbound("nope".into()))) + ); + } +}