hyperpolymath
diff --git a/‎crates/my-qtt/src/bin/conformance_gen.rs‎
Lines changed: 101 additions & 3 deletions b/‎crates/my-qtt/src/bin/conformance_gen.rs‎
Lines changed: 101 additions & 3 deletions
diff --git a/‎crates/my-qtt/src/session.rs‎
Lines changed: 152 additions & 0 deletions b/‎crates/my-qtt/src/session.rs‎
Lines changed: 152 additions & 0 deletions
@@ -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();
     }
 }
@@ -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);
+    }
 }