feat: @safe-gated verified resource checking + n-ary/global session runtimes

crates/my-lang/src/checker.rs

@@ -109,6 +109,13 @@ pub enum CheckError {
         line: usize,
         column: usize,
     },
+
+    #[error("`@safe` function `{name}` violates the verified linear resource discipline (a parameter is dropped or used more than once) at line {line}, column {column}")]
+    ResourceViolation {
+        name: String,
+        line: usize,
+        column: usize,
+    },
 }
 
 /// Maximum AST nesting depth the type checker will recurse through before
@@ -614,10 +621,56 @@ impl Checker {
         // Check function body
         self.check_block(&f.body);
 
+        // `@safe`: enforce the machine-checked QTT resource discipline (runs by
+        // default — no flag — for every `@safe`-annotated function).
+        if f.modifiers.contains(&FnModifier::Safe) {
+            self.check_qtt_safe_fn(f);
+        }
+
         self.current_return_type = None;
         self.symbols.exit_scope();
     }
 
+    /// Resource-check a `@safe` function with the verified QTT core
+    /// (`my_qtt::check`, the faithful R5 port reached via [`crate::qtt_bridge`]).
+    ///
+    /// The function is modelled as a lambda over its parameters — each treated
+    /// **linearly** (`DEFAULT_Q = One`, the strictest reading) — and the
+    /// machine-checked usage-walk runs on it. A parameter dropped or used more
+    /// than once *within the resource-relevant fragment* is reported as a
+    /// [`CheckError::ResourceViolation`]. A body that uses constructs OUTSIDE
+    /// that fragment (arithmetic, records, AI expressions, calls to globals, …)
+    /// cannot be lowered and is **skipped** — unverifiable is not unsafe, and
+    /// name/type resolution of those parts is the main checker's job. So
+    /// `@safe` means "the proof core has checked this function's resource
+    /// discipline wherever it is expressible", enforced by default.
+    fn check_qtt_safe_fn(&mut self, f: &FnDecl) {
+        use crate::qtt_bridge::{check_expr, BridgeCheckError};
+        use my_qtt::surface::CheckError as QttError;
+
+        // model the @safe function as `|params| body`
+        let lam = Expr::Lambda {
+            params: f.params.clone(),
+            body: LambdaBody::Block(f.body.clone()),
+            span: f.span,
+        };
+        match check_expr(&lam) {
+            // resource-safe, or outside the verifiable fragment (skip), or a
+            // free name the main resolver already diagnoses (skip).
+            Ok(_)
+            | Err(BridgeCheckError::Bridge(_))
+            | Err(BridgeCheckError::Check(QttError::Elab(_))) => {}
+            // lowered fully, but the verified walk rejected the usage discipline.
+            Err(BridgeCheckError::Check(QttError::Untypable)) => {
+                self.errors.push(CheckError::ResourceViolation {
+                    name: f.name.name.clone(),
+                    line: f.span.line,
+                    column: f.span.column,
+                });
+            }
+        }
+    }
+
     fn check_struct(&mut self, s: &StructDecl) {
         // Check that field types are valid
         for field in &s.fields {
@@ -1827,4 +1880,45 @@ mod tests {
         let errors = result.unwrap_err();
         assert!(errors.iter().any(|e| matches!(e, CheckError::NonBoolCondition { .. })));
     }
+
+    // ---- `@safe` functions are resource-checked by the verified QTT core ----
+
+    /// A `#[safe]` function whose parameter is used exactly once passes the
+    /// machine-checked linear discipline.
+    #[test]
+    fn qtt_safe_linear_param_ok() {
+        let result = check_source("#[safe]\nfn id(x: Int) { x; }");
+        assert!(result.is_ok(), "expected ok, got {:?}", result);
+    }
+
+    /// A `#[safe]` function that DROPS its linear parameter is rejected by the
+    /// verified usage-walk — the resource axis is now enforced in the compiler.
+    #[test]
+    fn qtt_safe_dropped_param_rejected() {
+        let result = check_source("#[safe]\nfn drp(x: Int) { 0; }");
+        assert!(result.is_err(), "expected ResourceViolation, got Ok");
+        let errors = result.unwrap_err();
+        assert!(
+            errors.iter().any(|e| matches!(e, CheckError::ResourceViolation { .. })),
+            "expected ResourceViolation, got {:?}",
+            errors
+        );
+    }
+
+    /// The SAME body without `#[safe]` is accepted — the discipline is opt-in
+    /// per function (gated on the modifier), so nothing else changes.
+    #[test]
+    fn non_safe_dropped_param_ok() {
+        let result = check_source("fn drp(x: Int) { 0; }");
+        assert!(result.is_ok(), "non-@safe fn must not be resource-checked, got {:?}", result);
+    }
+
+    /// A `#[safe]` body that uses constructs OUTSIDE the resource fragment
+    /// (here, arithmetic) cannot be lowered and is skipped — unverifiable is
+    /// not unsafe, so no false rejection.
+    #[test]
+    fn qtt_safe_out_of_fragment_skipped() {
+        let result = check_source("#[safe]\nfn add1(x: Int) { x + 1; }");
+        assert!(result.is_ok(), "out-of-fragment @safe body should be skipped, got {:?}", result);
+    }
 }

crates/my-qtt/src/bin/conformance_gen.rs

@@ -17,7 +17,7 @@
 // of-range vars, quantity/type mismatches) so both the `ok` and `none` branches
 // of `check` are exercised on both sides.
 
-use my_qtt::session::{cstep1, Config, Party, Val};
+use my_qtt::session::{cstep1, gstep1, nstep1, Config, Gty, Party, RoleAssignment, Val, Vty};
 use my_qtt::{check, step1, Mode, Q, Tm, Ty};
 use std::fs::File;
 use std::io::{BufWriter, Write};
@@ -317,6 +317,96 @@ fn gen_config(r: &mut Rng) -> Config {
     }
 }
 
+// ---------- global types ----------
+fn svty(t: &Vty) -> &'static str {
+    match t {
+        Vty::Unit => "vtunit",
+        Vty::Bool => "vtbool",
+        Vty::Nat => "vtnat",
+    }
+}
+fn sgty(g: &Gty) -> String {
+    match g {
+        Gty::End => "gend".into(),
+        Gty::Msg(p, q, t, c) => format!("(gmsg {} {} {} {})", p, q, svty(t), sgty(c)),
+        Gty::Bra(p, q, bs) => {
+            let mut s = format!("(gbra {} {}", p, q);
+            for (l, g) in bs {
+                s.push_str(&format!(" (gbr {} {})", l, sgty(g)));
+            }
+            s.push(')');
+            s
+        }
+        Gty::Mu(c) => format!("(gmu {})", sgty(c)),
+        Gty::Var(n) => format!("(gvar {})", n),
+    }
+}
+fn show_gstep(r: &Option<Gty>) -> String {
+    match r {
+        None => "none".into(),
+        Some(g) => format!("(some {})", sgty(g)),
+    }
+}
+fn gen_vty(r: &mut Rng) -> Vty {
+    match r.upto(3) {
+        0 => Vty::Unit,
+        1 => Vty::Bool,
+        _ => Vty::Nat,
+    }
+}
+fn gen_gty(r: &mut Rng, fuel: u32) -> Gty {
+    if fuel == 0 {
+        return Gty::End;
+    }
+    match r.upto(6) {
+        0 | 5 => Gty::End,
+        1 => Gty::Msg(r.upto(3) as usize, r.upto(3) as usize, gen_vty(r), Box::new(gen_gty(r, fuel - 1))),
+        2 => {
+            let nb = r.upto(3) as usize;
+            Gty::Bra(r.upto(3) as usize, r.upto(3) as usize, (0..nb).map(|i| (i, gen_gty(r, fuel - 1))).collect())
+        }
+        3 => Gty::Mu(Box::new(gen_gty(r, fuel - 1))),
+        _ => Gty::Var(r.upto(3) as usize),
+    }
+}
+
+// ---------- role assignments (n-ary located) ----------
+fn sra(ra: &[(usize, Party)]) -> String {
+    let mut s = String::from("(ra");
+    for (r, p) in ra {
+        s.push_str(&format!(" (rp {} {})", r, sparty(p)));
+    }
+    s.push(')');
+    s
+}
+fn show_nstep(r: &Option<RoleAssignment>) -> String {
+    match r {
+        None => "none".into(),
+        Some(ra) => format!("(some {})", sra(ra)),
+    }
+}
+// bias toward a fireable send/recv (or select/branch) pair among n roles
+fn gen_ra(r: &mut Rng) -> RoleAssignment {
+    let n = 2 + r.upto(3) as usize; // 2..=4 roles
+    let mut ra: RoleAssignment = Vec::new();
+    match r.upto(4) {
+        0 => {
+            ra.push((0, Party::Send(gen_val(r), Box::new(gen_party(r, 2)))));
+            ra.push((1, Party::Recv(Box::new(gen_party(r, 2)))));
+        }
+        1 => {
+            ra.push((0, Party::Sel(r.upto(3) as usize, Box::new(gen_party(r, 2)))));
+            ra.push((1, gen_party(r, 2)));
+        }
+        _ => {}
+    }
+    while ra.len() < n {
+        let i = ra.len();
+        ra.push((i, gen_party(r, 2)));
+    }
+    ra
+}
+
 fn main() {
     let args: Vec<String> = std::env::args().collect();
     if args.len() != 5 {
@@ -347,10 +437,18 @@ fn main() {
         writeln!(corpus, "(nf {})", sexp_tm(&ct)).unwrap();
         writeln!(results, "{}", sexp_tm(&eval_nf(&ct, NF_FUEL))).unwrap();
 
-        // (c) session-config step (#4): Rust my_qtt::session::cstep1 vs the
-        //     extracted Coq cstep1 (proved sound+complete vs the cstep relation)
+        // (c) session steppers (#4): Rust my_qtt::session vs the extracted Coq
+        //     cstep1 / gstep1 / nstep1 (binary / global / n-ary located layers)
         let cfg = gen_config(&mut r);
         writeln!(corpus, "(cstep {})", sconfig(&cfg)).unwrap();
         writeln!(results, "{}", show_cstep(&cstep1(&cfg))).unwrap();
+
+        let g = gen_gty(&mut r, 3);
+        writeln!(corpus, "(gstep {})", sgty(&g)).unwrap();
+        writeln!(results, "{}", show_gstep(&gstep1(&g))).unwrap();
+
+        let ra = gen_ra(&mut r);
+        writeln!(corpus, "(nstep {})", sra(&ra)).unwrap();
+        writeln!(results, "{}", show_nstep(&nstep1(&ra))).unwrap();
     }
 }