diff --git a/crates/my-lang/src/checker.rs b/crates/my-lang/src/checker.rs
index 3140b93..52d9a74 100644
--- a/crates/my-lang/src/checker.rs
+++ b/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);
+    }
 }
diff --git a/crates/my-qtt/src/bin/conformance_gen.rs b/crates/my-qtt/src/bin/conformance_gen.rs
index 971ebb2..a782130 100644
--- a/crates/my-qtt/src/bin/conformance_gen.rs
+++ b/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();
     }
 }
diff --git a/crates/my-qtt/src/session.rs b/crates/my-qtt/src/session.rs
index 6aeefdd..93df4a3 100644
--- a/crates/my-qtt/src/session.rs
+++ b/crates/my-qtt/src/session.rs
@@ -110,6 +110,122 @@ pub fn cstep1(c: &Config) -> Option<Config> {
     }
 }
 
+// ===== global-type stepper (Coq `SessionEval.gstep1`) =====
+
+/// Payload value types (Coq `vty`).
+#[derive(Clone, PartialEq, Eq, Debug)]
+pub enum Vty {
+    Unit,
+    Bool,
+    Nat,
+}
+
+/// Global session types (Coq `gty`); `Bra` is the labelled-branch list
+/// (Coq `gbranch`).
+#[derive(Clone, PartialEq, Eq, Debug)]
+pub enum Gty {
+    End,
+    Msg(usize, usize, Vty, Box<Gty>),
+    Bra(usize, usize, Vec<(usize, Gty)>),
+    Mu(Box<Gty>),
+    Var(usize),
+}
+
+/// One global-type reduction step (Coq `gstep1`; sound + progress vs the
+/// `gstep` relation). Commits to the head branch of a `Bra` — adequacy is
+/// soundness + progress, not functional determinism (any branch may be chosen).
+pub fn gstep1(g: &Gty) -> Option<Gty> {
+    match g {
+        Gty::Msg(_, _, _, cont) => Some((**cont).clone()),
+        Gty::Bra(_, _, bs) => bs.first().map(|(_, g)| g.clone()),
+        _ => None,
+    }
+}
+
+// ===== n-ary located stepper (Coq `SessionEval.nstep1`) =====
+
+/// A located role → endpoint assignment (Coq `role_assignment`).
+pub type RoleAssignment = Vec<(usize, Party)>;
+
+/// First binding for `r` (Coq `ra_get`).
+fn ra_get(ra: &[(usize, Party)], r: usize) -> Option<&Party> {
+    ra.iter().find(|(r2, _)| *r2 == r).map(|(_, p)| p)
+}
+
+/// Replace the FIRST binding for `r` (Coq `ra_set` — only the first occurrence).
+fn ra_set(ra: &[(usize, Party)], r: usize, p: &Party) -> RoleAssignment {
+    match ra.split_first() {
+        None => vec![],
+        Some(((r2, q), rest)) => {
+            if *r2 == r {
+                let mut v = vec![(*r2, p.clone())];
+                v.extend_from_slice(rest);
+                v
+            } else {
+                let mut v = vec![(*r2, q.clone())];
+                v.extend(ra_set(rest, r, p));
+                v
+            }
+        }
+    }
+}
+
+/// First `q != r` whose canonical party is `Recv`; yields `(q, open_party v Qc)`.
+fn find_recv(ra: &[(usize, Party)], r: usize, v: &Val) -> Option<(usize, Party)> {
+    for (q, _) in ra {
+        if *q == r {
+            continue;
+        }
+        if let Some(Party::Recv(qc)) = ra_get(ra, *q) {
+            return Some((*q, open_party(v, qc)));
+        }
+    }
+    None
+}
+
+/// First `q != r` whose canonical party is `Bra` offering label `l`; yields `(q, Q)`.
+fn find_bra(ra: &[(usize, Party)], r: usize, l: usize) -> Option<(usize, Party)> {
+    for (q, _) in ra {
+        if *q == r {
+            continue;
+        }
+        if let Some(Party::Bra(bs)) = ra_get(ra, *q) {
+            if let Some(qq) = bs.iter().find(|(k, _)| *k == l).map(|(_, p)| p.clone()) {
+                return Some((*q, qq));
+            }
+        }
+    }
+    None
+}
+
+/// Try to fire role `r` (canonical party `p`) against a partner (Coq `try_role`).
+fn try_role(ra: &[(usize, Party)], r: usize, p: &Party) -> Option<RoleAssignment> {
+    match p {
+        Party::Send(v, cont) => {
+            find_recv(ra, r, v).map(|(q, qres)| ra_set(&ra_set(ra, r, cont), q, &qres))
+        }
+        Party::Sel(l, cont) => {
+            find_bra(ra, r, *l).map(|(q, qres)| ra_set(&ra_set(ra, r, cont), q, &qres))
+        }
+        _ => None,
+    }
+}
+
+/// One synchronous n-ary step: the first sender/selector role (left-to-right)
+/// paired with its first dual partner (Coq `nstep1`; sound + progress vs the
+/// `nstep` relation).
+pub fn nstep1(ra: &[(usize, Party)]) -> Option<RoleAssignment> {
+    for (r, _) in ra {
+        if let Some(p) = ra_get(ra, *r) {
+            let p = p.clone();
+            if let Some(ra2) = try_role(ra, *r, &p) {
+                return Some(ra2);
+            }
+        }
+    }
+    None
+}
+
 #[cfg(test)]
 mod tests {
     use super::*;
@@ -163,4 +279,40 @@ mod tests {
     fn ended_is_normal() {
         assert_eq!(cstep1(&Config(b(Party::End), b(Party::End))), None);
     }
+
+    /// gstep1: a message prefix steps to its continuation; a branch to its head;
+    /// `End` and an empty offer are normal.
+    #[test]
+    fn global_steps() {
+        assert_eq!(gstep1(&Gty::Msg(0, 1, Vty::Nat, b(Gty::End))), Some(Gty::End));
+        let br = Gty::Bra(0, 1, vec![(0, Gty::End), (1, Gty::Var(0))]);
+        assert_eq!(gstep1(&br), Some(Gty::End)); // head branch
+        assert_eq!(gstep1(&Gty::End), None);
+        assert_eq!(gstep1(&Gty::Bra(0, 1, vec![])), None);
+    }
+
+    /// nstep1: among n parties, the sender meets the dual receiver and both
+    /// advance; the idle third party is untouched.
+    #[test]
+    fn nary_comm_step() {
+        let ra: RoleAssignment = vec![
+            (0, Party::Send(Val::Nat(7), b(Party::End))),
+            (1, Party::Recv(b(Party::End))),
+            (2, Party::End),
+        ];
+        let stepped = nstep1(&ra).expect("should step");
+        assert_eq!(ra_get(&stepped, 0), Some(&Party::End));
+        assert_eq!(ra_get(&stepped, 1), Some(&Party::End));
+        assert_eq!(ra_get(&stepped, 2), Some(&Party::End));
+    }
+
+    /// nstep1: two senders and no receiver → no communicating pair → stuck.
+    #[test]
+    fn nary_stuck() {
+        let ra: RoleAssignment = vec![
+            (0, Party::Send(Val::Unit, b(Party::End))),
+            (1, Party::Send(Val::Unit, b(Party::End))),
+        ];
+        assert_eq!(nstep1(&ra), None);
+    }
 }
diff --git a/docs/STATUS.adoc b/docs/STATUS.adoc
index 85e5b71..dc76c5c 100644
--- a/docs/STATUS.adoc
+++ b/docs/STATUS.adoc
@@ -45,7 +45,7 @@ the Idris twin's `preservation` (#108) is now DISCHARGED (total, hole-free;
 [cols="4,1,3",options="header"]
 |===
 | Item | Status | Note
-| Make the resource axis the *default* in `crates/my-lang/src/checker.rs` | `[ ]` | the QTT bridge is opt-in (`qtt_bridge::check_expr`) today
+| Make the resource axis the *default* in `crates/my-lang/src/checker.rs` | `[x]` | DONE — the verified QTT core runs by default (no flag) on every `#[safe]` function: `Checker::check_qtt_safe_fn` lowers it via `qtt_bridge` and a dropped/duplicated binder in the resource fragment is a `CheckError::ResourceViolation`; out-of-fragment bodies skip (unverifiable ≠ unsafe). Gated on `#[safe]` so non-linear code is unaffected.
 | Surface *quantity syntax* so the bridge enforces real per-binder linearity | `[ ]` | `Param` has no quantity field; bridge defaults to `One`
 | `wasm32` via the existing LLVM backend (`TargetSpec::wasm32` + `wasm-ld`) | `[ ]` | fastest target leg; backend already emits objects
 | `RISC-V` (`riscv64gc-unknown-linux-gnu`) via LLVM | `[ ]` | near-free once `wasm32` target wiring exists
diff --git a/proofs/STATUS.md b/proofs/STATUS.md
index 2e722c9..9c7bb20 100644
--- a/proofs/STATUS.md
+++ b/proofs/STATUS.md
@@ -66,6 +66,8 @@ Last verified: 2026-06-14.
 | Small-step `step` | Coq `solo-core/SoloCore` | **definitions-only** | CBV left-to-right relation, all redex + congruence constructors. Committed in F1.1. |
 | Functional evaluator `step1` (sound+complete vs `step`) | Coq `solo-core/Eval` | **machine-checked** | **2026-06-21.** `Eval.v`: `step1 : tm -> option tm` with `step1_sound`/`step1_complete` (`step1 t = Some t' ↔ step t t'`), real `Qed`, **axiom-free**, in `_CoqProject` (CI-gated). The executable mirror of the `step` relation; extracted (Extract.v) to couple the Rust evaluator `my_qtt::step1` (interpreter coupling #2). |
 | Functional session stepper `cstep1` (sound+complete vs `cstep`) | Coq `solo-core/SessionEval` | **machine-checked** | **2026-06-21.** `SessionEval.v`: `cstep1 : config -> option config` (binary fused config) with `cstep1_sound`/`cstep1_complete` (`cstep1 c = Some c' ↔ cstep c c'`), real `Qed`, **axiom-free**, in `_CoqProject` (CI-gated). The executable mirror of the `cstep` relation; extracted to couple the Rust session runtime `my_qtt::session::cstep1` (session coupling #4). |
+| Functional global stepper `gstep1` (sound+progress vs `gstep`) | Coq `solo-core/SessionEval` | **machine-checked** | **2026-06-21.** `gstep1 : gty -> option gty` with `gstep1_sound` + `gstep1_complete` (progress: `gstep G G' -> ∃ G'', gstep1 G = Some G''`), real `Qed`, **axiom-free**. Progress not determinism — `gstep` is nondeterministic at `GBra`. Extracted to couple `my_qtt::session::gstep1`. |
+| Functional n-ary stepper `nstep1` (sound+progress vs `nstep`) | Coq `solo-core/SessionEval` | **machine-checked** | **2026-06-21.** `nstep1 : role_assignment -> option role_assignment` (first communicating pair) with `nstep1_sound` + `nstep1_complete` (progress), real `Qed`, **axiom-free**. The pairing search (`find_recv`/`find_bra`) re-fetches parties through `ra_get`, so duplicate role entries never act on a stale party; soundness via per-search inversion lemmas, progress via the dual membership lemmas. Extracted to couple `my_qtt::session::nstep1`. |
 | Small-step `Step` | Idris2 `solo-core/Soundness` | **definitions-only** | CBV left-to-right relation, both products: additive `SFst`/`SSnd` fire on `With` values, multiplicative `SLetPair` fires on a `Tensor` value via `subst2`; plus the echo residue rules (`SWeaken`). Consumed by the verified `progress`. Migrated 2026-06-15. |
 | General core typing + substitution | Coq `coq/Typing.v` | **locally-checked** | Pre-existing: 9 `Qed`, 0 `Admitted`. Non-quantitative; substitution lemma proved. |
 | Echo **residue-measure SEAM** (`RESIDUE_MEASURE`, `EchoTraceTropical`, `echo_measure_not_injective`) | Coq `solo-core/ResourceAlgebra.v` + `EchoMeasure.v` | **machine-checked (Coq)** | **E4 SEAM — Coq mirror (axis-3 ECHO, 2026-06-14).** The my-lang half of the joint seam capstone ("interaction, not identification, is a theorem"), all real `Qed`, **axiom-free** (`Print Assumptions` closed, dedicated `proofs.yml` E4 gate). The former PENDING prose sketch in `ResourceAlgebra.v` is now the real **`Module Type RESIDUE_MEASURE (S : SEMIRING)`** — `measure : Residue → S.Q` with `measure_empty`/`measure_combine` (a monoid homomorphism `(Residue,combine,empty) → (S.Q,qmul,one)`, needing only the DONE R2 SEMIRING) — a faithful mirror of the upstream `tropical-resource-typing` `Resource/EchoBridge.lean` `structure ResidueMeasure`. `EchoMeasure.v` **inhabits** it at the DONE R4 Tropical cost carrier (`EchoTraceTropical`: a residue is an echo reindexing trace, `measure` = accumulated `Affine`-collapse cost = tropical `Fin`), and witnesses measure-**independence** on the Coq side via **`echo_measure_not_injective`** (`[Affine]` and `[Linear;Affine]` both cost `Fin 1` → the measure cannot reconstruct the residue). **Echo-types audit: RELEVANT (axis-3 ECHO)** — the audit confirmed the seam is already mechanised upstream on both foundations (echo-types `Echo/Measure/Interface.agda` `ResidueMeasure` + `Separation/NotResourceInstance.agda` `equal-measure-does-not-imply-equal-echo`, `--safe --without-K`); per the audit directive the Coq side **reuses** rather than re-derives. **Honest fences:** (1) the Coq mirror carries the measure HOMOMORPHISM + residue-level non-injectivity; the full measure-independence over the degrade-compose modality (the `ECHO_MODALITY` `act` transport, sketch (b)) is upstream-**CITED**, not re-derived — hence the ladder marks E4 `◑` (Coq mirror ✓, full seam upstream); (2) **hard IS-NOT invariant kept** — Echo is NOT a resource/SEMIRING instance, `measure` is a one-directional `E→R` lossy decoration, and `EchoMode.v`/`EchoResidue.v` stay `Quantity`-independent; (3) the trace carrier is the **free** residue monoid (the minimal composition skeleton), not a claim to BE the full echo residue object. |
@@ -122,10 +124,10 @@ verified against the crate sources + the conformance harness.)
 
 | Obligation | Status | Note |
 |------------|--------|------|
-| Rust affine checker refines Coq `check` / `aff_type_dec` (R5/R5b) | **conformance-checked** | **CLOSED by differential conformance 2026-06-21.** The verified Coq `check` (R5) is extracted to OCaml (`proofs/verification/coq/solo-core/Extract.v`, `Separate Extraction check`) and used as an independent ORACLE; the Rust port `crates/my-qtt` is the implementation under test. `conformance/run.sh` generates a random corpus of `(ctx, tm)` queries (`crates/my-qtt/src/bin/conformance_gen.rs`), runs BOTH the extracted verified `check` (`conformance/oracle.ml`) and `my_qtt::check`, and asserts byte-identical results — same accept/reject, same synthesized type, same usage vector — including echo (`MkEcho`/`Weaken`/`TEcho`) terms. **25 000 random terms across 5 seeds agree** (≈13% accept / 87% reject, so both branches are exercised). `my_qtt::aff_check` mirrors the Coq `aff_type_iff` (`check … = Some(a,D0) ∧ ule D0 budget`) and carries the R5/R5b reflexivity oracle tests. SCOPE/honesty: this is differential refinement-by-conformance against the *extracted verified algorithm*, NOT a full Rust-in-Coq refinement proof; and the *main* `crates/my-lang/src/checker.rs` (1830 LOC, Hindley) still does not yet CALL the verified core (`my_qtt` is wired via `qtt_bridge` but opt-in) — making it the default checker is the separate `docs/STATUS.adoc` intend "make the resource axis the default in `checker.rs`". |
+| Rust affine checker refines Coq `check` / `aff_type_dec` (R5/R5b) | **conformance-checked** | **CLOSED by differential conformance 2026-06-21.** The verified Coq `check` (R5) is extracted to OCaml (`proofs/verification/coq/solo-core/Extract.v`, `Separate Extraction check`) and used as an independent ORACLE; the Rust port `crates/my-qtt` is the implementation under test. `conformance/run.sh` generates a random corpus of `(ctx, tm)` queries (`crates/my-qtt/src/bin/conformance_gen.rs`), runs BOTH the extracted verified `check` (`conformance/oracle.ml`) and `my_qtt::check`, and asserts byte-identical results — same accept/reject, same synthesized type, same usage vector — including echo (`MkEcho`/`Weaken`/`TEcho`) terms. **25 000 random terms across 5 seeds agree** (≈13% accept / 87% reject, so both branches are exercised). `my_qtt::aff_check` mirrors the Coq `aff_type_iff` (`check … = Some(a,D0) ∧ ule D0 budget`) and carries the R5/R5b reflexivity oracle tests. SCOPE/honesty: this is differential refinement-by-conformance against the *extracted verified algorithm*, NOT a full Rust-in-Coq refinement proof; and the *main* `crates/my-lang/src/checker.rs` (Hindley) now CALLS the verified core by default for `#[safe]` functions (`Checker::check_qtt_safe_fn` → `qtt_bridge` → `my_qtt::check`; a dropped/duplicated binder in the resource fragment is a `CheckError::ResourceViolation`, out-of-fragment bodies skip). So the resource axis is enforced-by-default where opted in via `#[safe]` (the `docs/STATUS.adoc` "make the resource axis the default" item — DONE); whole-program linear-by-default is intentionally NOT the design (my-lang is not a linear language). |
 | Evaluator refines Coq `step` (solo core) | **conformance-checked** | **CLOSED 2026-06-21.** The reference semantics is the `step` RELATION (not extractable), so `Eval.v` adds a FUNCTIONAL `step1 : tm -> option tm` and proves it both ways vs the relation — `step1_sound : step1 t = Some t' -> step t t'` and `step1_complete : step t t' -> step1 t = Some t'` — real `Qed`, **axiom-free** (`Print Assumptions` closed), machine-checked in CI (`Eval.v` is in `_CoqProject`). `step1` is extracted alongside `check` (Extract.v) and the Rust port `my_qtt::step1` (faithful `shift`/`subst_at`/`subst0`/`subst2`/`is_value`/`step1`) is differentially conformance-tested against it: `conformance/run.sh` compares **one-step** results AND **iterated normal forms** (cap 64) over a random + closed-redex corpus. **45 000 results across 5 seeds agree** (3000 terms × {check, one-step, normal-form}); the normal-form pass cross-checks the Rust substitution against Coq's extracted `subst`. SCOPE/honesty: this couples an evaluator over the SHARED solo `tm` (the same approach as the checker), exactly mirroring `step`; the separate AI-surface `interpreter.rs` (richer term language, runtime no-ops for `Restrict`/`Ref`/`RefMut`) is NOT what is coupled here and remains an independent, unverified frontend. |
 | Echo modality wired into surface + checker | **conformance-checked** (verified-core surface) | **2026-06-21.** Echo is wired end-to-end through the VERIFIED core: the `my_qtt::surface` fragment has echo intro (`SExpr::Echo` / `STy::Echo`) and the `weaken` elimination (`SExpr::Weaken`), `elaborate` lowers them to `Tm::MkEcho`/`Tm::Weaken`, and the machine-checked `check` consumes them — so the `linear ⊑ affine` discipline (`EchoLinear`) is enforced from a surface term by the proof. Pinned by `surface.rs` tests: intro types correctly, a LINEAR echo `weaken`s to AFFINE, weakening an AFFINE echo is REJECTED (the one-way *no-section* fact), and witness linearity is threaded (an echo whose witness drops a linear binder is rejected). Echo terms are also in the random differential-conformance corpus (#1/#2), so `my_qtt`'s echo handling matches the extracted Coq `check`/`step1`. SCOPE/honesty: this closes echo on the verified-core-facing surface; the *conventional compiler* (`crates/my-lang` `ast::Expr`/parser) still has no echo SYNTAX (so `qtt_bridge` cannot yet lower a compiler-AST echo — that needs a type-annotated echo grammar, a frontend follow-on like the `Param` quantity syntax). `types.rs` `EchoMode` is no longer inert at the verified boundary; it is in the conventional frontend. |
-| Session runtime refining `cstep` (binary fused config) | **conformance-checked** (binary fragment) | **2026-06-21.** `SessionEval.v` adds a functional `cstep1 : config -> option config` for the binary fused `(νc)(P∣Q)` form and proves it SOUND + COMPLETE vs the `cstep` RELATION (`cstep1_sound`/`cstep1_complete`), real `Qed`, **axiom-free**, in `_CoqProject` (CI-gated). `cstep1` is extracted (Extract.v) and the Rust session runtime `my_qtt::session` (faithful `val`/`party`/`pbranch`/`config` + `vlift`/`vsubst`/`psubst_party`/`open_party`/`pget`/`cstep1`) is differentially conformance-tested against it (`conformance/run.sh`, `(cstep CONFIG)` queries) — **15 000 session steps across 5 seeds agree** (the comm + select redexes and the stuck/None cases). SCOPE/honesty: this couples the BINARY fused config (S1.1b/S1.2 fragment); the n-ary located `nstep` and global `gstep` are NOT yet given executable runtimes (a larger follow-on), and the AI-surface `interpreter.rs` (`Go`/`Await` collapse to sequential) is a separate unverified frontend. |
+| Session runtime refining `cstep` / `nstep` / `gstep` (all three layers) | **conformance-checked** | **2026-06-21.** `SessionEval.v` adds a functional stepper for each layer of the session metatheory and proves it adequate vs the reference RELATION, all real `Qed`, **axiom-free**, in `_CoqProject` (CI-gated): (1) **binary** `cstep1 : config -> option config` — SOUND + COMPLETE vs `cstep`; (2) **global** `gstep1 : gty -> option gty` — SOUND + PROGRESS vs `gstep` (`gstep1_sound` + `gstep1_complete`, the progress form because `gstep` is nondeterministic at `GBra`); (3) **n-ary located** `nstep1 : role_assignment -> option role_assignment` — SOUND + PROGRESS vs `nstep` (`nstep1_sound` + `nstep1_complete`; `nstep1` scans for the first communicating pair via `find_recv`/`find_bra`, parties always re-fetched through `ra_get`). All three are extracted (Extract.v) and the Rust runtime `my_qtt::session` (faithful `val`/`party`/`config`/`gty`/`role_assignment` + the substitution/lookup chain + `cstep1`/`gstep1`/`nstep1`) is differentially conformance-tested against them (`conformance/run.sh`, `(cstep …)`/`(gstep …)`/`(nstep …)` queries) — **90 000 results across 5 seeds agree** (6 query classes × 3000 cases × 5 seeds). SCOPE/honesty: for the two NONDETERMINISTIC relations the functional stepper commits to a deterministic strategy (first branch / first pair), so adequacy is soundness + progress (`step1 = None` iff the relation is stuck), NOT functional determinism — the honest statement for a nondeterministic reduction. The AI-surface `interpreter.rs` (`Go`/`Await` collapse to sequential) is a separate unverified frontend. |
 | Concrete `me` surface exercising the M1 elaboration | **by-design — not a gap** | **Affirmed 2026-06-21.** This is a deliberate architectural decision, NOT an omission: `Me` is an on-the-fly agent-generated *runtime projection* over the `Solo ⊂ Duet ⊂ Ensemble` dialect hierarchy, **not** a static fourth dialect — two attempts to build it as a static compiler were retired (`hyperpolymath/me-dialect` archived; in-tree `dialects/me/` sidelined to `_exploratory/me-scaffolding/SIDELINED.adoc`). The elaboration coupling that DOES matter is already machine-checked: M1 (`me_wt_sound`) proves `me -> solo` adequacy over the abstract Coq `me_tm`, axiom-free. Building a concrete static `me` grammar to "close" this row would CONTRADICT the architecture, so it is intentionally not built. No further action. |
 
 > These do not diminish the mechanised results — they fence the boundary
diff --git a/proofs/verification/coq/solo-core/Extract.v b/proofs/verification/coq/solo-core/Extract.v
index 416259c..e0155a6 100644
--- a/proofs/verification/coq/solo-core/Extract.v
+++ b/proofs/verification/coq/solo-core/Extract.v
@@ -31,6 +31,8 @@ Require Import Coq.extraction.ExtrOcamlNatInt.
 
 (* The verified functions the conformance harnesses test the Rust port against:
    `check` (R5, checker coupling #1), `step1` (Eval.v, interpreter coupling #2 —
-   sound+complete vs the `step` relation), and `cstep1` (SessionEval.v, session
-   coupling #4 — sound+complete vs the `cstep` relation). *)
-Separate Extraction check step1 cstep1.
+   sound+complete vs the `step` relation), and the session steppers (SessionEval.v,
+   coupling #4): `cstep1` (binary, sound+complete vs `cstep`), `gstep1` (global,
+   sound+progress vs `gstep`), and `nstep1` (n-ary located, sound+progress vs
+   `nstep`). *)
+Separate Extraction check step1 cstep1 gstep1 nstep1.
diff --git a/proofs/verification/coq/solo-core/SessionEval.v b/proofs/verification/coq/solo-core/SessionEval.v
index 91a5c31..197c168 100644
--- a/proofs/verification/coq/solo-core/SessionEval.v
+++ b/proofs/verification/coq/solo-core/SessionEval.v
@@ -46,3 +46,258 @@ Proof.
   induction 1; simpl; try reflexivity;
     match goal with [ H : pget _ _ = _ |- _ ] => rewrite H end; reflexivity.
 Qed.
+
+Require Import Coq.Arith.PeanoNat.
+
+(* ===== global-type stepper (coupling #4, global layer) =====
+
+   `gstep` (S3c.3) is NONDETERMINISTIC at `GBra` (any offered label may be
+   chosen), so the honest adequacy is SOUNDNESS + PROGRESS rather than a strong
+   functional-determinism completeness: `gstep1` commits to the FIRST branch and
+   finds a step exactly when the relation can step. *)
+
+Definition gstep1 (G : gty) : option gty :=
+  match G with
+  | GMsg _ _ _ G'            => Some G'
+  | GBra _ _ (GBcons _ G' _) => Some G'   (* commit to the head branch *)
+  | _                        => None
+  end.
+
+#[local] Hint Constructors gstep : sess.
+
+Theorem gstep1_sound : forall G G', gstep1 G = Some G' -> gstep G G'.
+Proof.
+  intros [| p q t G0 | p q bs | G0 | n] G' H; simpl in H; try discriminate.
+  - injection H as <-; apply GStep_Msg.
+  - destruct bs as [| l G0 rest]; simpl in H; try discriminate.
+    injection H as <-. apply GStep_Bra with (l := l). simpl. rewrite Nat.eqb_refl. reflexivity.
+Qed.
+
+(* PROGRESS: whenever the relation can step, `gstep1` returns some reduct.
+   (The strong form `gstep G G' -> gstep1 G = Some G'` is FALSE for `GBra` with
+   more than one branch — the relation may pick a non-head label.) *)
+Theorem gstep1_complete : forall G G', gstep G G' -> exists G'', gstep1 G = Some G''.
+Proof.
+  intros G G' H; destruct H as [p q t G0 | p q bs l G0 Hget].
+  - exists G0; reflexivity.
+  - destruct bs as [| k Gk rest]; simpl in Hget; try discriminate.
+    exists Gk; reflexivity.
+Qed.
+
+Require Import Coq.Lists.List.
+Import ListNotations.
+
+(* ===== n-ary located stepper (coupling #4, multiparty layer) =====
+
+   `nstep` (S2/S3) is NONDETERMINISTIC: any communicating (p,q) pair may fire.
+   `nstep1` commits to the FIRST sender/selector role (left-to-right in the
+   assignment) paired with its FIRST dual partner; adequacy is SOUNDNESS +
+   PROGRESS. Parties are always re-fetched through `ra_get` (the sanctioned
+   lookup), so duplicate role entries never make the stepper act on a stale
+   party. *)
+
+(* first q (with q <> r) whose canonical party is QRecv; yields (q, open_party v Qc) *)
+Fixpoint find_recv (ra cands : role_assignment) (r : role) (v : val)
+  : option (role * party) :=
+  match cands with
+  | [] => None
+  | (q, _) :: rest =>
+      if Nat.eqb q r then find_recv ra rest r v
+      else match ra_get ra q with
+           | Some (QRecv Qc) => Some (q, open_party v Qc)
+           | _ => find_recv ra rest r v
+           end
+  end.
+
+(* first q (with q <> r) whose canonical party is QBra offering label l; yields (q, Q) *)
+Fixpoint find_bra (ra cands : role_assignment) (r : role) (l : nat)
+  : option (role * party) :=
+  match cands with
+  | [] => None
+  | (q, _) :: rest =>
+      if Nat.eqb q r then find_bra ra rest r l
+      else match ra_get ra q with
+           | Some (QBra bs) =>
+               match pget l bs with
+               | Some Q => Some (q, Q)
+               | None => find_bra ra rest r l
+               end
+           | _ => find_bra ra rest r l
+           end
+  end.
+
+Definition try_role (ra : role_assignment) (r : role) (P : party)
+  : option role_assignment :=
+  match P with
+  | QSend v cont =>
+      match find_recv ra ra r v with
+      | Some (q, qres) => Some (ra_set (ra_set ra r cont) q qres)
+      | None => None
+      end
+  | QSel l cont =>
+      match find_bra ra ra r l with
+      | Some (q, qres) => Some (ra_set (ra_set ra r cont) q qres)
+      | None => None
+      end
+  | _ => None
+  end.
+
+Fixpoint nstep1_go (ra cands : role_assignment) : option role_assignment :=
+  match cands with
+  | [] => None
+  | (r, _) :: rest =>
+      match ra_get ra r with
+      | Some P => match try_role ra r P with
+                  | Some ra' => Some ra'
+                  | None => nstep1_go ra rest
+                  end
+      | None => nstep1_go ra rest
+      end
+  end.
+
+Definition nstep1 (ra : role_assignment) : option role_assignment := nstep1_go ra ra.
+
+#[local] Hint Constructors nstep : sess.
+
+(* ----- soundness ----- *)
+
+Lemma find_recv_sound : forall ra cands r v q qres,
+  find_recv ra cands r v = Some (q, qres) ->
+  r <> q /\ exists Qc, ra_get ra q = Some (QRecv Qc) /\ qres = open_party v Qc.
+Proof.
+  induction cands as [| [q0 P0] rest IH]; intros r v q qres H; simpl in H.
+  - discriminate.
+  - destruct (Nat.eqb q0 r) eqn:E.
+    + apply IH in H; exact H.
+    + destruct (ra_get ra q0) as [P|] eqn:Eg; [| apply IH in H; exact H].
+      destruct P; try (apply IH in H; exact H).
+      injection H as <- <-. split.
+      * apply Nat.eqb_neq in E. congruence.
+      * eexists; split; [ exact Eg | reflexivity ].
+Qed.
+
+Lemma find_bra_sound : forall ra cands r l q qres,
+  find_bra ra cands r l = Some (q, qres) ->
+  r <> q /\ exists bs, ra_get ra q = Some (QBra bs) /\ pget l bs = Some qres.
+Proof.
+  induction cands as [| [q0 P0] rest IH]; intros r l q qres H; simpl in H.
+  - discriminate.
+  - destruct (Nat.eqb q0 r) eqn:E.
+    + apply IH in H; exact H.
+    + destruct (ra_get ra q0) as [P|] eqn:Eg; [| apply IH in H; exact H].
+      destruct P as [| ? ? | ? | ? ? | bs0]; try (apply IH in H; exact H).
+      destruct (pget l bs0) as [Q|] eqn:Ep; [| apply IH in H; exact H].
+      injection H as <- <-. split.
+      * apply Nat.eqb_neq in E. congruence.
+      * eexists; split; [ exact Eg | exact Ep ].
+Qed.
+
+Lemma try_role_sound : forall ra r P ra',
+  ra_get ra r = Some P -> try_role ra r P = Some ra' -> nstep ra ra'.
+Proof.
+  intros ra r P ra' Hr H. destruct P as [| v cont | Qc | l cont | bs]; simpl in H; try discriminate.
+  - destruct (find_recv ra ra r v) as [[q qres]|] eqn:Ef; try discriminate.
+    injection H as <-. apply find_recv_sound in Ef.
+    destruct Ef as (Hrq & Qc & Hq & ->). eapply NStep_Comm; eauto.
+  - destruct (find_bra ra ra r l) as [[q qres]|] eqn:Ef; try discriminate.
+    injection H as <-. apply find_bra_sound in Ef.
+    destruct Ef as (Hrq & bs & Hq & Hpg). eapply NStep_Sel; eauto.
+Qed.
+
+Lemma nstep1_go_sound : forall ra cands ra',
+  nstep1_go ra cands = Some ra' -> nstep ra ra'.
+Proof.
+  induction cands as [| [r P0] rest IH]; intros ra' H; simpl in H.
+  - discriminate.
+  - destruct (ra_get ra r) as [P|] eqn:Hr; [| apply IH; exact H].
+    destruct (try_role ra r P) as [ra''|] eqn:Et; [| apply IH; exact H].
+    injection H as <-. eapply try_role_sound; eauto.
+Qed.
+
+Theorem nstep1_sound : forall ra ra', nstep1 ra = Some ra' -> nstep ra ra'.
+Proof. intros ra ra'. apply nstep1_go_sound. Qed.
+
+(* ----- progress: nstep1 finds a step whenever the relation can step ----- *)
+
+Lemma find_recv_steps : forall ra cands r v q Qc P,
+  In (q, P) cands -> r <> q -> ra_get ra q = Some (QRecv Qc) ->
+  find_recv ra cands r v <> None.
+Proof.
+  induction cands as [| [q0 P0] rest IH]; intros r v q Qc P Hin Hrq Hq; simpl.
+  - inversion Hin.
+  - destruct Hin as [Heq | Hin].
+    + inversion Heq; subst q0 P0.
+      destruct (Nat.eqb q r) eqn:E.
+      * apply Nat.eqb_eq in E; subst; contradiction.
+      * rewrite Hq; discriminate.
+    + destruct (Nat.eqb q0 r) eqn:E; [ eapply IH; eauto |].
+      destruct (ra_get ra q0) as [P1|] eqn:Eg; [| eapply IH; eauto].
+      destruct P1; try (eapply IH; eauto); discriminate.
+Qed.
+
+Lemma find_bra_steps : forall ra cands r l q bs Q P,
+  In (q, P) cands -> r <> q -> ra_get ra q = Some (QBra bs) -> pget l bs = Some Q ->
+  find_bra ra cands r l <> None.
+Proof.
+  induction cands as [| [q0 P0] rest IH]; intros r l q bs Q P Hin Hrq Hq Hpg; simpl.
+  - inversion Hin.
+  - destruct Hin as [Heq | Hin].
+    + inversion Heq; subst q0 P0.
+      destruct (Nat.eqb q r) eqn:E.
+      * apply Nat.eqb_eq in E; subst; contradiction.
+      * rewrite Hq, Hpg; discriminate.
+    + destruct (Nat.eqb q0 r) eqn:E; [ eapply IH; eauto |].
+      destruct (ra_get ra q0) as [P1|] eqn:Eg; [| eapply IH; eauto].
+      destruct P1 as [| ? ? | ? | ? ? | bs0]; try (eapply IH; eauto).
+      destruct (pget l bs0) eqn:Ep; [ discriminate | eapply IH; eauto ].
+Qed.
+
+Lemma try_role_send_steps : forall ra p v P q Q,
+  p <> q -> ra_get ra q = Some (QRecv Q) -> try_role ra p (QSend v P) <> None.
+Proof.
+  intros ra p v P q Q Hpq Hq. simpl.
+  destruct (find_recv ra ra p v) as [[q' r']|] eqn:E; [ discriminate |].
+  exfalso. revert E. eapply find_recv_steps with (q := q) (Qc := Q) (P := QRecv Q); eauto.
+  apply ra_get_in; exact Hq.
+Qed.
+
+Lemma try_role_sel_steps : forall ra p l P q bs Q,
+  p <> q -> ra_get ra q = Some (QBra bs) -> pget l bs = Some Q ->
+  try_role ra p (QSel l P) <> None.
+Proof.
+  intros ra p l P q bs Q Hpq Hq Hpg. simpl.
+  destruct (find_bra ra ra p l) as [[q' r']|] eqn:E; [ discriminate |].
+  exfalso. revert E. eapply find_bra_steps with (q := q) (bs := bs) (Q := Q) (P := QBra bs); eauto.
+  apply ra_get_in; exact Hq.
+Qed.
+
+Lemma nstep1_go_steps : forall ra cands r P,
+  In r (map fst cands) -> ra_get ra r = Some P -> try_role ra r P <> None ->
+  nstep1_go ra cands <> None.
+Proof.
+  induction cands as [| [r0 Q0] rest IH]; intros r P Hin Hr Hstep; simpl in Hin |- *.
+  - contradiction.
+  - destruct (ra_get ra r0) as [P0|] eqn:Hr0.
+    + destruct (try_role ra r0 P0) eqn:Et0; [ discriminate |].
+      destruct Hin as [Heq | Hin].
+      * subst r0. rewrite Hr0 in Hr. injection Hr as Hpp. congruence.
+      * eapply IH; eauto.
+    + destruct Hin as [Heq | Hin].
+      * subst r0. rewrite Hr0 in Hr. discriminate.
+      * eapply IH; eauto.
+Qed.
+
+Theorem nstep1_complete : forall ra ra', nstep ra ra' -> exists ra'', nstep1 ra = Some ra''.
+Proof.
+  intros ra ra' H.
+  assert (Hne : nstep1 ra <> None).
+  { unfold nstep1.
+    destruct H as [ra p q v P Q Hpq Hp Hq | ra p q l P bs Q Hpq Hp Hq Hpg].
+    - eapply nstep1_go_steps with (r := p) (P := QSend v P); [| exact Hp |].
+      + apply in_map_iff. exists (p, QSend v P); split; [reflexivity| apply ra_get_in; exact Hp].
+      + eapply try_role_send_steps; eauto.
+    - eapply nstep1_go_steps with (r := p) (P := QSel l P); [| exact Hp |].
+      + apply in_map_iff. exists (p, QSel l P); split; [reflexivity| apply ra_get_in; exact Hp].
+      + eapply try_role_sel_steps; eauto. }
+  destruct (nstep1 ra) as [ra''|]; [ exists ra''; reflexivity | congruence ].
+Qed.
diff --git a/proofs/verification/coq/solo-core/conformance/README.adoc b/proofs/verification/coq/solo-core/conformance/README.adoc
index 60a208b..81e06b1 100644
--- a/proofs/verification/coq/solo-core/conformance/README.adoc
+++ b/proofs/verification/coq/solo-core/conformance/README.adoc
@@ -2,16 +2,21 @@
 // SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 = QTT conformance harness
 
-Differential-conformance evidence for impl ⇄ spec couplings #1 and #2
+Differential-conformance evidence for impl ⇄ spec couplings #1, #2 and #4
 (`proofs/STATUS.md`):
 
 * #1 — *the Rust affine checker refines the Coq `check` (R5)*;
 * #2 — *the Rust evaluator `my_qtt::step1` refines the Coq `step` semantics*,
   via the functional `step1` of `Eval.v` (proved sound+complete vs the `step`
   relation), extracted and compared one-step AND iterated to normal form;
-* #4 — *the Rust session runtime `my_qtt::session::cstep1` refines the Coq
-  `cstep` semantics* (binary fused config), via the functional `cstep1` of
-  `SessionEval.v` (proved sound+complete vs `cstep`), extracted and compared.
+* #4 — *the Rust session runtime `my_qtt::session` refines the Coq session
+  semantics at all three layers*, via the functional steppers of `SessionEval.v`,
+  extracted and compared:
+  ** `cstep1` (binary fused config) — sound+complete vs `cstep`;
+  ** `gstep1` (global type) — sound+progress vs `gstep`;
+  ** `nstep1` (n-ary located role assignment) — sound+progress vs `nstep`.
+  (For the two nondeterministic relations the stepper commits to a deterministic
+  strategy, so adequacy is soundness + progress, not functional determinism.)
 
 (Coupling #3, the echo modality, rides on #1/#2: echo terms are in the corpus
 and `my_qtt::surface` elaborates echo to the verified `check`.)
diff --git a/proofs/verification/coq/solo-core/conformance/oracle.ml b/proofs/verification/coq/solo-core/conformance/oracle.ml
index 153e42d..18be806 100644
--- a/proofs/verification/coq/solo-core/conformance/oracle.ml
+++ b/proofs/verification/coq/solo-core/conformance/oracle.ml
@@ -195,6 +195,62 @@ let show_config (Conf (p1, p2)) = "(conf " ^ show_party p1 ^ " " ^ show_party p2
 
 let show_cstep = function None -> "none" | Some c -> "(some " ^ show_config c ^ ")"
 
+(* ---------- global types (coupling #4, global layer) ---------- *)
+
+let vty_of = function
+  | Atom "vtunit" -> VTUnit
+  | Atom "vtbool" -> VTBool
+  | Atom "vtnat" -> VTNat
+  | _ -> failwith "bad vty"
+
+let rec gty_of = function
+  | Atom "gend" -> GEnd
+  | List [Atom "gmsg"; Atom p; Atom q; t; g] ->
+      GMsg (int_of_string p, int_of_string q, vty_of t, gty_of g)
+  | List (Atom "gbra" :: Atom p :: Atom q :: brs) ->
+      GBra (int_of_string p, int_of_string q, gbranch_of brs)
+  | List [Atom "gmu"; g] -> GMu (gty_of g)
+  | List [Atom "gvar"; Atom n] -> GVar (int_of_string n)
+  | _ -> failwith "bad gty"
+and gbranch_of = function
+  | [] -> GBnil
+  | List [Atom "gbr"; Atom l; g] :: rest -> GBcons (int_of_string l, gty_of g, gbranch_of rest)
+  | _ -> failwith "bad gbranch"
+
+let show_vty = function VTUnit -> "vtunit" | VTBool -> "vtbool" | VTNat -> "vtnat"
+
+let rec show_gty = function
+  | GEnd -> "gend"
+  | GMsg (p, q, t, g) ->
+      "(gmsg " ^ string_of_int p ^ " " ^ string_of_int q ^ " " ^ show_vty t ^ " " ^ show_gty g ^ ")"
+  | GBra (p, q, bs) ->
+      "(gbra " ^ string_of_int p ^ " " ^ string_of_int q ^ show_gbranch bs ^ ")"
+  | GMu g -> "(gmu " ^ show_gty g ^ ")"
+  | GVar n -> "(gvar " ^ string_of_int n ^ ")"
+and show_gbranch = function
+  | GBnil -> ""
+  | GBcons (l, g, rest) -> " (gbr " ^ string_of_int l ^ " " ^ show_gty g ^ ")" ^ show_gbranch rest
+
+let show_gstep = function None -> "none" | Some g -> "(some " ^ show_gty g ^ ")"
+
+(* ---------- role assignments (coupling #4, n-ary located layer) ---------- *)
+
+let rec ra_of = function
+  | [] -> []
+  | List [Atom "rp"; Atom r; p] :: rest -> (int_of_string r, party_of p) :: ra_of rest
+  | _ -> failwith "bad role_assignment"
+
+let ra_of_sexp = function
+  | List (Atom "ra" :: rps) -> ra_of rps
+  | _ -> failwith "bad ra"
+
+let show_ra ra =
+  "(ra"
+  ^ List.fold_left (fun acc (r, p) -> acc ^ " (rp " ^ string_of_int r ^ " " ^ show_party p ^ ")") "" ra
+  ^ ")"
+
+let show_nstep = function None -> "none" | Some ra -> "(some " ^ show_ra ra ^ ")"
+
 (* ---------- driver ---------- *)
 
 let () =
@@ -210,8 +266,12 @@ let () =
           print_endline (show_step (step1 (tm_of tm)))
         | List [Atom "nf"; tm] ->                (* iterate to normal form (cap = NF_FUEL) *)
           print_endline (show_tm (eval_nf 64 (tm_of tm)))
-        | List [Atom "cstep"; cfg] ->            (* one session-config step (coupling #4) *)
+        | List [Atom "cstep"; cfg] ->            (* one binary session-config step (#4) *)
           print_endline (show_cstep (cstep1 (config_of cfg)))
+        | List [Atom "gstep"; g] ->             (* one global-type step (#4, global) *)
+          print_endline (show_gstep (gstep1 (gty_of g)))
+        | List [Atom "nstep"; ra] ->            (* one n-ary located step (#4, multiparty) *)
+          print_endline (show_nstep (nstep1 (ra_of_sexp ra)))
         | _ -> failwith "bad query"
       end
     done
diff --git a/proofs/verification/coq/solo-core/conformance/run.sh b/proofs/verification/coq/solo-core/conformance/run.sh
index 5831c5b..53690ac 100755
--- a/proofs/verification/coq/solo-core/conformance/run.sh
+++ b/proofs/verification/coq/solo-core/conformance/run.sh
@@ -59,11 +59,13 @@ RN=$(wc -l < "$BUILD/rust_results.txt")
 CN=$(wc -l < "$BUILD/coq_results.txt")
 echo "   rust lines=$RN  coq lines=$CN"
 if diff -u "$BUILD/rust_results.txt" "$BUILD/coq_results.txt" > "$BUILD/diff.txt"; then
-  TOT=$((COUNT * 4))
-  echo "PASS: $TOT/$TOT results agree over $COUNT cases x {check, one-step, normal-form, session-step}:"
-  echo "      Rust my_qtt::check  == extracted Coq check    (coupling #1)"
-  echo "      Rust my_qtt::step1  == extracted Coq step1    (coupling #2; sound+complete vs the step relation)"
-  echo "      Rust session::cstep1 == extracted Coq cstep1  (coupling #4; sound+complete vs the cstep relation)"
+  TOT=$((COUNT * 6))
+  echo "PASS: $TOT/$TOT results agree over $COUNT cases x {check, one-step, normal-form, cstep, gstep, nstep}:"
+  echo "      Rust my_qtt::check   == extracted Coq check    (coupling #1)"
+  echo "      Rust my_qtt::step1   == extracted Coq step1    (coupling #2; sound+complete vs the step relation)"
+  echo "      Rust session::cstep1 == extracted Coq cstep1   (coupling #4 binary;  sound+complete vs cstep)"
+  echo "      Rust session::gstep1 == extracted Coq gstep1   (coupling #4 global;  sound+progress vs gstep)"
+  echo "      Rust session::nstep1 == extracted Coq nstep1   (coupling #4 n-ary;   sound+progress vs nstep)"
   exit 0
 else
   echo "FAIL: Rust and verified-Coq results differ:"