diff --git a/crates/my-qtt/src/bin/conformance_gen.rs b/crates/my-qtt/src/bin/conformance_gen.rs new file mode 100644 index 0000000..971ebb2 --- /dev/null +++ b/crates/my-qtt/src/bin/conformance_gen.rs @@ -0,0 +1,356 @@ +// SPDX-License-Identifier: MPL-2.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +// +// Differential-conformance GENERATOR for the QTT checker coupling. +// +// Emits a corpus of random `(ctx, tm)` queries plus the result of the Rust +// `my_qtt::check` on each, in a canonical text form byte-identical to the one +// the OCaml ORACLE (extracted from the verified Coq `check`) prints. The +// harness `conformance/run.sh` then asserts the two streams are equal, i.e. +// ∀ (g,t) in corpus. my_qtt::check g t == (extracted Coq check) g t +// which is the refinement evidence for "the Rust checker refines Coq `check`". +// +// Usage: conformance_gen +// +// The generator is deterministic in `seed` (a tiny SplitMix64), depends only on +// std, and deliberately produces a MIX of well-typed and ill-typed terms (out- +// 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::{check, step1, Mode, Q, Tm, Ty}; +use std::fs::File; +use std::io::{BufWriter, Write}; + +/// normal-form fuel cap — MUST equal the oracle's `eval_nf` cap so a divergent +/// term yields the same capped term on both sides. +const NF_FUEL: u32 = 64; + +// ---------- deterministic PRNG (SplitMix64) ---------- +struct Rng(u64); +impl Rng { + fn next(&mut self) -> u64 { + self.0 = self.0.wrapping_add(0x9E37_79B9_7F4A_7C15); + let mut z = self.0; + z = (z ^ (z >> 30)).wrapping_mul(0xBF58_476D_1CE4_E5B9); + z = (z ^ (z >> 27)).wrapping_mul(0x94D0_49BB_1331_11EB); + z ^ (z >> 31) + } + fn upto(&mut self, n: u64) -> u64 { + self.next() % n + } +} + +// ---------- random AST ---------- +fn gen_q(r: &mut Rng) -> Q { + match r.upto(3) { + 0 => Q::Zero, + 1 => Q::One, + _ => Q::Omega, + } +} +fn gen_m(r: &mut Rng) -> Mode { + if r.upto(2) == 0 { Mode::Linear } else { Mode::Affine } +} + +fn gen_ty(r: &mut Rng, fuel: u32) -> Ty { + if fuel == 0 { + return Ty::Unit; + } + match r.upto(6) { + 0 => Ty::Unit, + 1 => Ty::With(Box::new(gen_ty(r, fuel - 1)), Box::new(gen_ty(r, fuel - 1))), + 2 => Ty::Tensor(Box::new(gen_ty(r, fuel - 1)), Box::new(gen_ty(r, fuel - 1))), + 3 => Ty::Sum(Box::new(gen_ty(r, fuel - 1)), Box::new(gen_ty(r, fuel - 1))), + 4 => Ty::Arr(gen_q(r), Box::new(gen_ty(r, fuel - 1)), Box::new(gen_ty(r, fuel - 1))), + _ => Ty::Echo(gen_m(r), Box::new(gen_ty(r, fuel - 1)), Box::new(gen_ty(r, fuel - 1))), + } +} + +// `scope` = number of binders in scope; Var picks 0..scope+1 so some indices +// fall out of range (→ `none`), exercising the ill-typed branch. +fn gen_tm(r: &mut Rng, fuel: u32, scope: usize) -> Tm { + if fuel == 0 { + return if r.upto(2) == 0 { + Tm::Var((r.upto((scope + 1) as u64)) as usize) + } else { + Tm::UnitT + }; + } + match r.upto(15) { + 0 => Tm::Var((r.upto((scope + 2) as u64)) as usize), + 1 => Tm::UnitT, + 2 => Tm::Lam(gen_q(r), gen_ty(r, fuel - 1), Box::new(gen_tm(r, fuel - 1, scope + 1))), + 3 => Tm::App(Box::new(gen_tm(r, fuel - 1, scope)), Box::new(gen_tm(r, fuel - 1, scope))), + 4 => Tm::With(Box::new(gen_tm(r, fuel - 1, scope)), Box::new(gen_tm(r, fuel - 1, scope))), + 5 => Tm::Fst(Box::new(gen_tm(r, fuel - 1, scope))), + 6 => Tm::Snd(Box::new(gen_tm(r, fuel - 1, scope))), + 7 => Tm::Tensor(Box::new(gen_tm(r, fuel - 1, scope)), Box::new(gen_tm(r, fuel - 1, scope))), + 8 => Tm::LetPair(Box::new(gen_tm(r, fuel - 1, scope)), Box::new(gen_tm(r, fuel - 1, scope + 2))), + 9 => Tm::Inl(gen_ty(r, fuel - 1), Box::new(gen_tm(r, fuel - 1, scope))), + 10 => Tm::Inr(gen_ty(r, fuel - 1), Box::new(gen_tm(r, fuel - 1, scope))), + 11 => Tm::Case( + Box::new(gen_tm(r, fuel - 1, scope)), + Box::new(gen_tm(r, fuel - 1, scope + 1)), + Box::new(gen_tm(r, fuel - 1, scope + 1)), + ), + 12 => Tm::Let(gen_q(r), Box::new(gen_tm(r, fuel - 1, scope)), Box::new(gen_tm(r, fuel - 1, scope + 1))), + 13 => Tm::MkEcho(gen_m(r), gen_ty(r, fuel - 1), gen_ty(r, fuel - 1), Box::new(gen_tm(r, fuel - 1, scope))), + _ => Tm::Weaken(Box::new(gen_tm(r, fuel - 1, scope))), + } +} + +// ---------- canonical printers (MUST match conformance/oracle.ml) ---------- +fn show_q(q: Q) -> &'static str { + match q { + Q::Zero => "0", + Q::One => "1", + Q::Omega => "w", + } +} +fn show_m(m: Mode) -> &'static str { + match m { + Mode::Linear => "lin", + Mode::Affine => "aff", + } +} +fn show_ty(t: &Ty) -> String { + match t { + Ty::Unit => "unit".into(), + Ty::With(a, b) => format!("(with {} {})", show_ty(a), show_ty(b)), + Ty::Tensor(a, b) => format!("(tensor {} {})", show_ty(a), show_ty(b)), + Ty::Sum(a, b) => format!("(sum {} {})", show_ty(a), show_ty(b)), + Ty::Arr(q, a, b) => format!("(arr {} {} {})", show_q(*q), show_ty(a), show_ty(b)), + Ty::Echo(m, a, b) => format!("(echo {} {} {})", show_m(*m), show_ty(a), show_ty(b)), + } +} +fn show_uvec(d: &[Q]) -> String { + let parts: Vec<&str> = d.iter().map(|&q| show_q(q)).collect(); + format!("[{}]", parts.join(" ")) +} +fn show_result(r: &Option<(Ty, Vec)>) -> String { + match r { + None => "none".into(), + Some((a, d)) => format!("(ok {} {})", show_ty(a), show_uvec(d)), + } +} + +// ---------- S-expression query emitters (MUST match the oracle grammar) ---------- +fn sexp_ty(t: &Ty) -> String { + show_ty(t) // identical grammar +} +fn sexp_tm(t: &Tm) -> String { + match t { + Tm::Var(n) => format!("(var {})", n), + Tm::UnitT => "star".into(), + Tm::Lam(q, a, b) => format!("(lam {} {} {})", show_q(*q), sexp_ty(a), sexp_tm(b)), + Tm::App(f, x) => format!("(app {} {})", sexp_tm(f), sexp_tm(x)), + Tm::With(a, b) => format!("(with {} {})", sexp_tm(a), sexp_tm(b)), + Tm::Fst(t) => format!("(fst {})", sexp_tm(t)), + Tm::Snd(t) => format!("(snd {})", sexp_tm(t)), + Tm::Tensor(a, b) => format!("(tensor {} {})", sexp_tm(a), sexp_tm(b)), + Tm::LetPair(a, b) => format!("(letpair {} {})", sexp_tm(a), sexp_tm(b)), + Tm::Inl(ty, t) => format!("(inl {} {})", sexp_ty(ty), sexp_tm(t)), + Tm::Inr(ty, t) => format!("(inr {} {})", sexp_ty(ty), sexp_tm(t)), + Tm::Case(s, l, r) => format!("(case {} {} {})", sexp_tm(s), sexp_tm(l), sexp_tm(r)), + Tm::Let(q, a, b) => format!("(let {} {} {})", show_q(*q), sexp_tm(a), sexp_tm(b)), + Tm::MkEcho(m, a, b, t) => { + format!("(mkecho {} {} {} {})", show_m(*m), sexp_ty(a), sexp_ty(b), sexp_tm(t)) + } + Tm::Weaken(t) => format!("(weaken {})", sexp_tm(t)), + } +} +fn sexp_ctx(g: &[Ty]) -> String { + let mut s = String::from("(ctx"); + for ty in g { + s.push(' '); + s.push_str(&sexp_ty(ty)); + } + s.push(')'); + s +} + +fn show_step(r: &Option) -> String { + match r { + None => "none".into(), + Some(t) => format!("(some {})", sexp_tm(t)), + } +} + +fn eval_nf(t: &Tm, fuel: u32) -> Tm { + let mut cur = t.clone(); + let mut f = fuel; + while f > 0 { + match step1(&cur) { + None => break, + Some(n) => { + cur = n; + f -= 1; + } + } + } + cur +} + +// ---------- closed, redex-rich generators (deep substitution coverage) ---------- +fn gen_value(r: &mut Rng, fuel: u32) -> Tm { + if fuel == 0 { + return Tm::UnitT; + } + match r.upto(6) { + 0 => Tm::UnitT, + 1 => Tm::Lam(gen_q(r), gen_ty(r, 1), Box::new(gen_tm(r, fuel - 1, 1))), + 2 => Tm::With(Box::new(gen_value(r, fuel - 1)), Box::new(gen_value(r, fuel - 1))), + 3 => Tm::Tensor(Box::new(gen_value(r, fuel - 1)), Box::new(gen_value(r, fuel - 1))), + 4 => Tm::Inl(gen_ty(r, 1), Box::new(gen_value(r, fuel - 1))), + _ => Tm::MkEcho(gen_m(r), gen_ty(r, 1), gen_ty(r, 1), Box::new(gen_value(r, fuel - 1))), + } +} + +// closed (scope 0) terms built around redexes so reduction proceeds and +// exercises subst0/subst2/shift in chains. +fn gen_closed(r: &mut Rng, fuel: u32) -> Tm { + if fuel == 0 { + return gen_value(r, 1); + } + match r.upto(8) { + 0 => Tm::App( + Box::new(Tm::Lam(gen_q(r), gen_ty(r, 1), Box::new(gen_tm(r, fuel - 1, 1)))), + Box::new(gen_value(r, fuel - 1)), + ), + 1 => Tm::Let(gen_q(r), Box::new(gen_value(r, fuel - 1)), Box::new(gen_tm(r, fuel - 1, 1))), + 2 => Tm::Fst(Box::new(Tm::With(Box::new(gen_value(r, fuel - 1)), Box::new(gen_value(r, fuel - 1))))), + 3 => Tm::Snd(Box::new(Tm::With(Box::new(gen_value(r, fuel - 1)), Box::new(gen_value(r, fuel - 1))))), + 4 => Tm::LetPair( + Box::new(Tm::Tensor(Box::new(gen_value(r, fuel - 1)), Box::new(gen_value(r, fuel - 1)))), + Box::new(gen_tm(r, fuel - 1, 2)), + ), + 5 => Tm::Case( + Box::new(Tm::Inl(gen_ty(r, 1), Box::new(gen_value(r, fuel - 1)))), + Box::new(gen_tm(r, fuel - 1, 1)), + Box::new(gen_tm(r, fuel - 1, 1)), + ), + 6 => Tm::Weaken(Box::new(Tm::MkEcho( + Mode::Linear, + gen_ty(r, 1), + gen_ty(r, 1), + Box::new(gen_value(r, fuel - 1)), + ))), + _ => gen_value(r, fuel - 1), + } +} + +// ---------- session configs (coupling #4) ---------- +fn sval(v: &Val) -> String { + match v { + Val::Var(n) => format!("(vvar {})", n), + Val::Unit => "vunit".into(), + Val::Bool(true) => "(vbool t)".into(), + Val::Bool(false) => "(vbool f)".into(), + Val::Nat(n) => format!("(vnat {})", n), + } +} +fn sparty(p: &Party) -> String { + match p { + Party::End => "qend".into(), + Party::Send(v, q) => format!("(qsend {} {})", sval(v), sparty(q)), + Party::Recv(q) => format!("(qrecv {})", sparty(q)), + Party::Sel(l, q) => format!("(qsel {} {})", l, sparty(q)), + Party::Bra(bs) => { + let mut s = String::from("(qbra"); + for (l, q) in bs { + s.push_str(&format!(" (br {} {})", l, sparty(q))); + } + s.push(')'); + s + } + } +} +fn sconfig(c: &Config) -> String { + format!("(conf {} {})", sparty(&c.0), sparty(&c.1)) +} +fn show_cstep(r: &Option) -> String { + match r { + None => "none".into(), + Some(c) => format!("(some {})", sconfig(c)), + } +} + +fn gen_val(r: &mut Rng) -> Val { + match r.upto(4) { + 0 => Val::Var(r.upto(3) as usize), + 1 => Val::Unit, + 2 => Val::Bool(r.upto(2) == 0), + _ => Val::Nat(r.upto(5)), + } +} +fn gen_party(r: &mut Rng, fuel: u32) -> Party { + if fuel == 0 { + return Party::End; + } + match r.upto(6) { + 0 | 5 => Party::End, + 1 => Party::Send(gen_val(r), Box::new(gen_party(r, fuel - 1))), + 2 => Party::Recv(Box::new(gen_party(r, fuel - 1))), + 3 => Party::Sel(r.upto(3) as usize, Box::new(gen_party(r, fuel - 1))), + _ => { + let n = r.upto(3) as usize; + Party::Bra((0..n).map(|i| (i, gen_party(r, fuel - 1))).collect()) + } + } +} +// bias toward dual pairs so the comm/select steps fire (alongside stuck configs) +fn gen_config(r: &mut Rng) -> Config { + let f = 2 + r.upto(2) as u32; + match r.upto(6) { + 0 => Config(Box::new(Party::Send(gen_val(r), Box::new(gen_party(r, f)))), Box::new(Party::Recv(Box::new(gen_party(r, f))))), + 1 => Config(Box::new(Party::Recv(Box::new(gen_party(r, f)))), Box::new(Party::Send(gen_val(r), Box::new(gen_party(r, f))))), + 2 => Config( + Box::new(Party::Sel(r.upto(4) as usize, Box::new(gen_party(r, f)))), + Box::new(gen_party(r, f + 1)), + ), + 3 => Config( + Box::new(gen_party(r, f + 1)), + Box::new(Party::Sel(r.upto(4) as usize, Box::new(gen_party(r, f)))), + ), + _ => Config(Box::new(gen_party(r, f)), Box::new(gen_party(r, f))), + } +} + +fn main() { + let args: Vec = std::env::args().collect(); + if args.len() != 5 { + eprintln!("usage: conformance_gen "); + std::process::exit(2); + } + let count: u64 = args[1].parse().expect("count"); + let seed: u64 = args[2].parse().expect("seed"); + let mut corpus = BufWriter::new(File::create(&args[3]).expect("corpus_out")); + let mut results = BufWriter::new(File::create(&args[4]).expect("rust_results_out")); + + let mut r = Rng(seed.wrapping_add(0xD1B5_4A32_D192_ED03)); + for _ in 0..count { + // (a) checker (#1) + one-step (#2) conformance on a random term that + // may be open and may be ill-typed (exercises both decision branches) + let k = r.upto(4) as usize; + let g: Vec = (0..k).map(|_| gen_ty(&mut r, 2)).collect(); + let fuel = 2 + (r.upto(3) as u32); // depth 2..=4 + let t = gen_tm(&mut r, fuel, k); + writeln!(corpus, "(q {} {})", sexp_ctx(&g), sexp_tm(&t)).unwrap(); + writeln!(results, "{}", show_result(&check(&g, &t))).unwrap(); + writeln!(corpus, "(s {})", sexp_tm(&t)).unwrap(); + writeln!(results, "{}", show_step(&step1(&t))).unwrap(); + + // (b) normal-form (#2, deep) conformance on a CLOSED redex-rich term, + // cross-checking subst0/subst2/shift against Coq's extracted subst + let ct = gen_closed(&mut r, 3); + 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) + let cfg = gen_config(&mut r); + writeln!(corpus, "(cstep {})", sconfig(&cfg)).unwrap(); + writeln!(results, "{}", show_cstep(&cstep1(&cfg))).unwrap(); + } +} diff --git a/crates/my-qtt/src/lib.rs b/crates/my-qtt/src/lib.rs index 9bb3079..f6e5c5f 100644 --- a/crates/my-qtt/src/lib.rs +++ b/crates/my-qtt/src/lib.rs @@ -35,6 +35,7 @@ #![forbid(unsafe_code)] +pub mod session; pub mod surface; /// Quantities: the three-point affine semiring `{0, 1, ω}` (Coq `Quantity.Q`). @@ -327,6 +328,220 @@ pub fn aff_check(g: &[Ty], t: &Tm, expected: &Ty, budget: &[Q]) -> bool { } } +// ===== the call-by-value evaluator (Coq `step1`, Eval.v) ===== +// +// A FAITHFUL port of the Coq functional one-step evaluator `step1`, which is +// proved SOUND + COMPLETE against the reference `step` RELATION (Eval.v: +// `step1_sound`/`step1_complete`, axiom-free). Coupling #2 (interpreter +// adequacy vs Coq `step`) is then closed by differential conformance: +// `conformance/run.sh` checks `my_qtt::step1` == extracted Coq `step1` on a +// random corpus (one step AND iterated to normal form, which cross-checks the +// substitution below against Coq's extracted `subst`). + +/// de Bruijn shift (Coq `shift`): increment every free var `>= c`. +pub fn shift(c: usize, t: &Tm) -> Tm { + match t { + Tm::Var(k) => if *k < c { Tm::Var(*k) } else { Tm::Var(k + 1) }, + Tm::UnitT => Tm::UnitT, + Tm::Lam(q, a, b) => Tm::Lam(*q, a.clone(), Box::new(shift(c + 1, b))), + Tm::App(f, x) => Tm::App(Box::new(shift(c, f)), Box::new(shift(c, x))), + Tm::With(a, b) => Tm::With(Box::new(shift(c, a)), Box::new(shift(c, b))), + Tm::Fst(t0) => Tm::Fst(Box::new(shift(c, t0))), + Tm::Snd(t0) => Tm::Snd(Box::new(shift(c, t0))), + Tm::Tensor(a, b) => Tm::Tensor(Box::new(shift(c, a)), Box::new(shift(c, b))), + Tm::LetPair(a, b) => Tm::LetPair(Box::new(shift(c, a)), Box::new(shift(c + 2, b))), + Tm::Inl(ty, t0) => Tm::Inl(ty.clone(), Box::new(shift(c, t0))), + Tm::Inr(ty, t0) => Tm::Inr(ty.clone(), Box::new(shift(c, t0))), + Tm::Case(s, l, r) => Tm::Case( + Box::new(shift(c, s)), + Box::new(shift(c + 1, l)), + Box::new(shift(c + 1, r)), + ), + Tm::Let(q, a, b) => Tm::Let(*q, Box::new(shift(c, a)), Box::new(shift(c + 1, b))), + Tm::MkEcho(m, a, b, t0) => Tm::MkEcho(*m, a.clone(), b.clone(), Box::new(shift(c, t0))), + Tm::Weaken(t0) => Tm::Weaken(Box::new(shift(c, t0))), + } +} + +/// Replace de Bruijn index `j` by `u`, decrementing free vars `> j` (Coq `subst_at`). +pub fn subst_at(j: usize, u: &Tm, t: &Tm) -> Tm { + match t { + Tm::Var(k) => { + if *k < j { + Tm::Var(*k) + } else if *k == j { + u.clone() + } else { + Tm::Var(k - 1) + } + } + Tm::UnitT => Tm::UnitT, + Tm::Lam(q, a, b) => Tm::Lam(*q, a.clone(), Box::new(subst_at(j + 1, &shift(0, u), b))), + Tm::App(f, x) => Tm::App(Box::new(subst_at(j, u, f)), Box::new(subst_at(j, u, x))), + Tm::With(a, b) => Tm::With(Box::new(subst_at(j, u, a)), Box::new(subst_at(j, u, b))), + Tm::Fst(t0) => Tm::Fst(Box::new(subst_at(j, u, t0))), + Tm::Snd(t0) => Tm::Snd(Box::new(subst_at(j, u, t0))), + Tm::Tensor(a, b) => Tm::Tensor(Box::new(subst_at(j, u, a)), Box::new(subst_at(j, u, b))), + Tm::LetPair(a, b) => Tm::LetPair( + Box::new(subst_at(j, u, a)), + Box::new(subst_at(j + 2, &shift(0, &shift(0, u)), b)), + ), + Tm::Inl(ty, t0) => Tm::Inl(ty.clone(), Box::new(subst_at(j, u, t0))), + Tm::Inr(ty, t0) => Tm::Inr(ty.clone(), Box::new(subst_at(j, u, t0))), + Tm::Case(s, l, r) => Tm::Case( + Box::new(subst_at(j, u, s)), + Box::new(subst_at(j + 1, &shift(0, u), l)), + Box::new(subst_at(j + 1, &shift(0, u), r)), + ), + Tm::Let(q, a, b) => { + Tm::Let(*q, Box::new(subst_at(j, u, a)), Box::new(subst_at(j + 1, &shift(0, u), b))) + } + Tm::MkEcho(m, a, b, t0) => Tm::MkEcho(*m, a.clone(), b.clone(), Box::new(subst_at(j, u, t0))), + Tm::Weaken(t0) => Tm::Weaken(Box::new(subst_at(j, u, t0))), + } +} + +/// Substitute for the index-0 binder (Coq `subst0`). +pub fn subst0(u: &Tm, t: &Tm) -> Tm { + subst_at(0, u, t) +} + +/// Two-variable substitution for `LetPair` bodies (Coq `subst2`). +pub fn subst2(u1: &Tm, u2: &Tm, t: &Tm) -> Tm { + subst0(u1, &subst0(&shift(0, u2), t)) +} + +/// Decidable value predicate (Coq `is_value`). +pub fn is_value(t: &Tm) -> bool { + match t { + Tm::UnitT | Tm::Lam(..) => true, + Tm::With(a, b) | Tm::Tensor(a, b) => is_value(a) && is_value(b), + Tm::Inl(_, a) | Tm::Inr(_, a) => is_value(a), + Tm::MkEcho(_, _, _, a) => is_value(a), + _ => false, + } +} + +/// One call-by-value step, or `None` if normal/stuck (Coq `step1`; proved +/// sound + complete vs the reference `step` relation in Eval.v). +pub fn step1(t: &Tm) -> Option { + match t { + Tm::Var(_) | Tm::UnitT | Tm::Lam(..) => None, + Tm::App(t1, t2) => { + if let Some(p) = step1(t1) { + Some(Tm::App(Box::new(p), t2.clone())) + } else if is_value(t1) { + if let Some(p) = step1(t2) { + Some(Tm::App(t1.clone(), Box::new(p))) + } else if is_value(t2) { + if let Tm::Lam(_, _, body) = &**t1 { + Some(subst0(t2, body)) + } else { + None + } + } else { + None + } + } else { + None + } + } + Tm::With(t1, t2) => { + if let Some(p) = step1(t1) { + Some(Tm::With(Box::new(p), t2.clone())) + } else if is_value(t1) { + step1(t2).map(|p| Tm::With(t1.clone(), Box::new(p))) + } else { + None + } + } + Tm::Fst(t0) => { + if let Some(p) = step1(t0) { + Some(Tm::Fst(Box::new(p))) + } else if let Tm::With(v1, v2) = &**t0 { + if is_value(v1) && is_value(v2) { + Some((**v1).clone()) + } else { + None + } + } else { + None + } + } + Tm::Snd(t0) => { + if let Some(p) = step1(t0) { + Some(Tm::Snd(Box::new(p))) + } else if let Tm::With(v1, v2) = &**t0 { + if is_value(v1) && is_value(v2) { + Some((**v2).clone()) + } else { + None + } + } else { + None + } + } + Tm::Tensor(t1, t2) => { + if let Some(p) = step1(t1) { + Some(Tm::Tensor(Box::new(p), t2.clone())) + } else if is_value(t1) { + step1(t2).map(|p| Tm::Tensor(t1.clone(), Box::new(p))) + } else { + None + } + } + Tm::LetPair(t1, t2) => { + if let Some(p) = step1(t1) { + Some(Tm::LetPair(Box::new(p), t2.clone())) + } else if let Tm::Tensor(v1, v2) = &**t1 { + if is_value(v1) && is_value(v2) { + Some(subst2(v1, v2, t2)) + } else { + None + } + } else { + None + } + } + Tm::Inl(b, t0) => step1(t0).map(|p| Tm::Inl(b.clone(), Box::new(p))), + Tm::Inr(a, t0) => step1(t0).map(|p| Tm::Inr(a.clone(), Box::new(p))), + Tm::Case(s, l, r) => { + if let Some(p) = step1(s) { + Some(Tm::Case(Box::new(p), l.clone(), r.clone())) + } else { + match &**s { + Tm::Inl(_, v) if is_value(v) => Some(subst0(v, l)), + Tm::Inr(_, v) if is_value(v) => Some(subst0(v, r)), + _ => None, + } + } + } + Tm::Let(q, t1, t2) => { + if let Some(p) = step1(t1) { + Some(Tm::Let(*q, Box::new(p), t2.clone())) + } else if is_value(t1) { + Some(subst0(t1, t2)) + } else { + None + } + } + Tm::MkEcho(m, a, b, t0) => step1(t0).map(|p| Tm::MkEcho(*m, a.clone(), b.clone(), Box::new(p))), + Tm::Weaken(t0) => { + if let Some(p) = step1(t0) { + Some(Tm::Weaken(Box::new(p))) + } else if let Tm::MkEcho(Mode::Linear, a, b, v) = &**t0 { + if is_value(v) { + Some(Tm::MkEcho(Mode::Affine, a.clone(), b.clone(), v.clone())) + } else { + None + } + } else { + None + } + } + } +} + #[cfg(test)] mod tests { //! Oracle tests: each mirrors a `reflexivity` `Example` in `SoloCore.v`, so @@ -418,4 +633,29 @@ mod tests { assert!(!qle(One, Zero)); assert!(qle(Omega, Omega)); } + + /// Evaluator (Coq `step1`) spot-checks. The conformance harness + /// (`conformance/run.sh`) is the systematic check vs the extracted verified + /// `step1`; these pin the headline redexes for Coq-free CI. + #[test] + fn step_redexes() { + // beta: (\x:Unit. x) star --> star + let beta = Tm::App(b(lam(One, Ty::Unit, Tm::Var(0))), b(Tm::UnitT)); + assert_eq!(step1(&beta), Some(Tm::UnitT)); + // additive projection: fst --> star + let fst = Tm::Fst(b(Tm::With(b(Tm::UnitT), b(Tm::UnitT)))); + assert_eq!(step1(&fst), Some(Tm::UnitT)); + // echo weaken: weaken (echo_L star) --> echo_A star + let wk = Tm::Weaken(b(Tm::MkEcho(Mode::Linear, Ty::Unit, Ty::Unit, b(Tm::UnitT)))); + assert_eq!( + step1(&wk), + Some(Tm::MkEcho(Mode::Affine, Ty::Unit, Ty::Unit, b(Tm::UnitT))) + ); + // let-pair (exercises subst2): let (x,y) = (star,star) in x --> star + let lp = Tm::LetPair(b(Tm::Tensor(b(Tm::UnitT), b(Tm::UnitT))), b(Tm::Var(1))); + assert_eq!(step1(&lp), Some(Tm::UnitT)); + // values are normal + assert_eq!(step1(&Tm::UnitT), None); + assert_eq!(step1(&lam(One, Ty::Unit, Tm::UnitT)), None); + } } diff --git a/crates/my-qtt/src/session.rs b/crates/my-qtt/src/session.rs new file mode 100644 index 0000000..6aeefdd --- /dev/null +++ b/crates/my-qtt/src/session.rs @@ -0,0 +1,166 @@ +// SPDX-License-Identifier: MPL-2.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell + +//! # `session` — the binary session-config evaluator (Coq `SessionEval.cstep1`) +//! +//! Coupling **#4**: a faithful Rust port of the Coq functional session stepper +//! `cstep1`, which `SessionEval.v` proves SOUND and COMPLETE vs the reference +//! `cstep` RELATION of `SessionPi.v` (the binary fused `(νc)(P∣Q)` form, S1.1b). +//! `conformance/run.sh` differentially tests this `cstep1` against the extracted +//! Coq `cstep1` on a random corpus of configurations. +//! +//! The reference semantics is a relation (not runnable); the verified `cstep1` +//! is its executable mirror, so a green conformance run means this runtime makes +//! exactly the communication step the machine-checked semantics sanctions. + +/// Payload values (Coq `val`): a de Bruijn receive-binder variable + base data. +#[derive(Clone, PartialEq, Eq, Debug)] +pub enum Val { + Var(usize), + Unit, + Bool(bool), + Nat(u64), +} + +/// An endpoint process (Coq `party`); `Bra` is the labelled-branch list (Coq +/// `pbranch`, an assoc list — `pget` takes the first matching label). +#[derive(Clone, PartialEq, Eq, Debug)] +pub enum Party { + End, + Send(Val, Box), + Recv(Box), + Sel(usize, Box), + Bra(Vec<(usize, Party)>), +} + +/// The fused two-party configuration (Coq `config = Conf party party`). +#[derive(Clone, PartialEq, Eq, Debug)] +pub struct Config(pub Box, pub Box); + +/// value shift (Coq `vlift`). +fn vlift(c: usize, v: &Val) -> Val { + match v { + Val::Var(k) => { + if *k < c { + Val::Var(*k) + } else { + Val::Var(k + 1) + } + } + _ => v.clone(), + } +} + +/// value substitution (Coq `vsubst`). +fn vsubst(c: usize, u: &Val, v: &Val) -> Val { + match v { + Val::Var(k) => { + if *k < c { + Val::Var(*k) + } else if *k == c { + u.clone() + } else { + Val::Var(k - 1) + } + } + _ => v.clone(), + } +} + +/// payload substitution into a party body (Coq `psubst_party`). +fn psubst_party(c: usize, u: &Val, p: &Party) -> Party { + match p { + Party::End => Party::End, + Party::Send(v, q) => Party::Send(vsubst(c, u, v), Box::new(psubst_party(c, u, q))), + Party::Recv(q) => Party::Recv(Box::new(psubst_party(c + 1, &vlift(0, u), q))), + Party::Sel(l, q) => Party::Sel(*l, Box::new(psubst_party(c, u, q))), + Party::Bra(bs) => { + Party::Bra(bs.iter().map(|(l, q)| (*l, psubst_party(c, u, q))).collect()) + } + } +} + +/// receive the value `u` into the index-0 binder (Coq `open_party`). +pub fn open_party(u: &Val, p: &Party) -> Party { + psubst_party(0, u, p) +} + +/// first-match label lookup (Coq `pget`). +fn pget<'a>(l: usize, bs: &'a [(usize, Party)]) -> Option<&'a Party> { + bs.iter().find(|(k, _)| *k == l).map(|(_, q)| q) +} + +/// one synchronous communication step of the fused config (Coq `cstep1`, +/// proved sound + complete vs the `cstep` relation in SessionEval.v). +pub fn cstep1(c: &Config) -> Option { + match (&*c.0, &*c.1) { + (Party::Send(v, p), Party::Recv(q)) => { + Some(Config(p.clone(), Box::new(open_party(v, q)))) + } + (Party::Recv(q), Party::Send(v, p)) => { + Some(Config(Box::new(open_party(v, q)), p.clone())) + } + (Party::Sel(l, p), Party::Bra(bs)) => { + pget(*l, bs).map(|q| Config(p.clone(), Box::new(q.clone()))) + } + (Party::Bra(bs), Party::Sel(l, p)) => { + pget(*l, bs).map(|q| Config(Box::new(q.clone()), p.clone())) + } + _ => None, + } +} + +#[cfg(test)] +mod tests { + use super::*; + + fn b(x: T) -> Box { + Box::new(x) + } + + /// ping-pong: `Conf (send 42; end) (recv; end)` steps to `Conf end end` + /// (the received value is substituted into the — here closed — continuation). + #[test] + fn comm_step() { + let c = Config( + b(Party::Send(Val::Nat(42), b(Party::End))), + b(Party::Recv(b(Party::End))), + ); + assert_eq!( + cstep1(&c), + Some(Config(b(Party::End), b(Party::End))) + ); + } + + /// select/branch: `Conf (sel 1) (bra {0:end, 1:send; end})` picks label 1. + #[test] + fn select_step() { + let c = Config( + b(Party::Sel(1, b(Party::End))), + b(Party::Bra(vec![ + (0, Party::End), + (1, Party::Send(Val::Unit, b(Party::End))), + ])), + ); + assert_eq!( + cstep1(&c), + Some(Config(b(Party::End), b(Party::Send(Val::Unit, b(Party::End))))) + ); + } + + /// a select on an UNOFFERED label is stuck (no step) — `pget` returns None. + #[test] + fn select_missing_label_stuck() { + let c = Config( + b(Party::Sel(7, b(Party::End))), + b(Party::Bra(vec![(0, Party::End)])), + ); + assert_eq!(cstep1(&c), None); + } + + /// two ended parties are a normal form. + #[test] + fn ended_is_normal() { + assert_eq!(cstep1(&Config(b(Party::End), b(Party::End))), None); + } +} diff --git a/crates/my-qtt/src/surface.rs b/crates/my-qtt/src/surface.rs index 0ff324b..aac73c6 100644 --- a/crates/my-qtt/src/surface.rs +++ b/crates/my-qtt/src/surface.rs @@ -288,4 +288,48 @@ mod tests { Err(CheckError::Elab(ElabError::Unbound("nope".into()))) ); } + + // ----- echo modality wired into the surface + the verified checker (#3) ----- + + fn echo(mode: Mode, witness: SExpr) -> SExpr { + SExpr::Echo { mode, a: STy::Unit, b: STy::Unit, witness: b(witness) } + } + + /// `[linear] echo Unit>(unit)` elaborates and the verified checker + /// assigns the echo residue type — echo flows surface → machine-checked walk. + #[test] + fn echo_intro_ok() { + assert_eq!( + check_surface(&echo(Mode::Linear, SExpr::Unit)), + Ok((Ty::Echo(Mode::Linear, b(Ty::Unit), b(Ty::Unit)), vec![])) + ); + } + + /// The echo discipline (`EchoLinear`): a LINEAR echo `weaken`s to an AFFINE + /// one — checked by the verified walk on the surface term. + #[test] + fn echo_weaken_linear_to_affine() { + let w = SExpr::Weaken(b(echo(Mode::Linear, SExpr::Unit))); + assert_eq!( + check_surface(&w), + Ok((Ty::Echo(Mode::Affine, b(Ty::Unit), b(Ty::Unit)), vec![])) + ); + } + + /// ...and weakening an AFFINE echo is REJECTED — the one-way `linear ⊑ affine` + /// (the *no-section* fact) is enforced from the surface by the proof. + #[test] + fn echo_weaken_affine_rejected() { + let w = SExpr::Weaken(b(echo(Mode::Affine, SExpr::Unit))); + assert_eq!(check_surface(&w), Err(CheckError::Untypable)); + } + + /// Echo threads its witness's usage: `|1 x:Unit| [linear] echo<…>(unit)` + /// drops the linear `x` inside the echo → rejected. So the echo residue does + /// not launder away linearity. + #[test] + fn echo_witness_linearity_enforced() { + let dropx = lam(One, "x", STy::Unit, echo(Mode::Linear, SExpr::Unit)); + assert_eq!(check_surface(&dropx), Err(CheckError::Untypable)); + } } diff --git a/proofs/STATUS.md b/proofs/STATUS.md index 20404d9..53435a4 100644 --- a/proofs/STATUS.md +++ b/proofs/STATUS.md @@ -17,6 +17,7 @@ Last verified: 2026-06-14. |------|---------| | **machine-checked** | A proof assistant accepts it today (`Qed` / no holes) **and** it is run in CI. | | **locally-checked** | Accepts under the proof assistant locally; **not** yet in CI. | +| **conformance-checked** | An *implementation* is shown to refine a *verified spec* by differential testing against the artifact extracted from that spec (not a full refinement proof). Used for impl ⇄ spec couplings. | | **proved-on-paper** | A written proof exists in `proofs/**.md`; not mechanised. | | **statement-only** | The theorem is *stated* mechanically (typed hole / `Admitted`); the proof is a tracked obligation, not done. | | **definitions-only** | Syntax/rules/operations defined; no theorems yet. | @@ -63,6 +64,8 @@ Last verified: 2026-06-14. | `preservation` | Coq `solo-core/SoloCore` | **machine-checked** | `Theorem preservation : Preservation.`, real `Qed`, axiom-free, via the open-context QTT substitution lemma `ht_subst`. Phase F1.4. CI: `proofs.yml` compiles it + asserts `Print Assumptions` closed (and likewise `affine_pres`). | | `preservation` | Idris2 `solo-core/Soundness` | **locally-checked** | **DISCHARGED 2026-06-21 (#108).** `preservation : (t : Tm) -> Has g d t a -> Step t t' -> Has g d t' a` is a total, hole-free function by induction on `Step` — `:total preservation` confirms; `%default total`, no `postulate`/`believe_me`/`assert_total`/`?hole`. Mirrors the Coq twin `preservation`: the β/projection/elimination cases consume the QTT substitution lemmas from `Substitution.idr` — `substLemma0` (App/Case/Let single-variable) and `subst2Lemma` (LetPair two-variable) — realigning the residual usage with `d` via `uadd` commutativity/associativity (`uaddAssoc`) and `uscale One`; congruence cases recurse structurally. Stated over the CORRECT design (separated context + genuine products) that made the same-usage statement sound (issue #93). The reduct term `t` is taken explicitly (relevant), exactly as `progress` does, because Idris erases the derivation's term/type indices while the substitution lemmas compute on the bound body + substituted value. `affinePreservation` follows as the Solo-kernel corollary (`:total` too). Supporting chain in `Substitution.idr` (all total, hole-free): append-context algebra, shape invariant (`shapeVar`/`shapeType`), `hvShift`/`htShift`, the accounting algebra (`qReassoc`/`vecReassoc`/`substReassocAdd`/`substReassocMult`/`usplit3`/`uaddSplitBoundary2`/`uaddAssoc`), `hvSubst`, the FULL `htSubst` (all 15 cases), `substLemma0`, `subst2Lemma`. The `b`-index-erasure obstruction (ADR-003) is resolved by carrying `b` erased. `idris2 --build solo-core.ipkg` exits 0; **the solo core is now HOLE-FREE**. CI: `proofs.yml` Idris job. | | 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). | | 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. | @@ -97,23 +100,33 @@ Last verified: 2026-06-14. | Complexity analysis | absent | F4 | | Proof CI leg | **present** — `proofs.yml` machine-checks both tracks (`coqc` + `idris2 --build`); overtakes AS | F5 | -## Implementation ⇄ spec coupling (status: **absent** — deferred to P-later) +## Implementation ⇄ spec coupling (status: #1–#4 **closed**, #5 **by-design**, 2026-06-21) The mechanised cores above are the **spec**; the Rust toolchain -(`crates/my-lang`) is a separate, conventional AI-first implementation. -No refinement/adequacy proof couples them today, and the resource axis is -**unwired** in the implementation. These are honest **absent** obligations, -deferred to the post-proof compiler-parity phases (ALIGNMENT-PLAN §4, -P-later) and recorded here so the gap is not mistaken for closed. (Audit: -2026-06-15, verified against the crate sources.) +(`crates/my-lang`) is a separate, conventional AI-first implementation. The +coupling method adopted here is **differential conformance against the +Coq-extracted verified artifact** (extract the verified function to OCaml, +then assert the Rust implementation agrees on a random corpus) — the honest, +reproducible alternative to an infeasible full Rust-in-Coq refinement proof. +Couplings **#1 (checker)**, **#2 (evaluator vs `step`)**, **#3 (echo +modality)**, and **#4 (session runtime vs `cstep`)** are **closed** by this +method (below). Where the spec is a relation (`step`, `cstep`), a functional +mirror (`step1`, `cstep1`) is first proved sound+complete vs the relation +(`Eval.v`, `SessionEval.v` — machine-checked, axiom-free), then the Rust port +is conformance-tested against the extracted mirror. One harness +(`conformance/run.sh`) drives all of them: **60 000 results across 5 seeds +agree** (3000 cases × {check, one-step, normal-form, session-step}). #5 is +deliberately **by-design** (Me is a runtime projector, not a static dialect — +see the top-level pedagogy note), so it is not a gap. (Audit: 2026-06-21, +verified against the crate sources + the conformance harness.) | Obligation | Status | Note | |------------|--------|------| -| Rust affine checker refines Coq `check` / `aff_type_dec` (R5/R5b) | **absent** | `crates/my-lang/src/checker.rs` (1830 LOC) is a conventional Hindley-style structural checker — no usage/multiplicity/context-split; `Symbol` (`scope.rs`) and `Param` (`ast.rs`) carry no quantity field. The verified executable `check` has no Rust counterpart. The intended affine checker is `TODO(#typeck)` in the lexer-only `dialects/solo/compiler` stub. | -| Interpreter adequacy vs Coq `step` | **absent** | `interpreter.rs` (tree-walking) and the Coq `step` are over disjoint term languages; no adequacy / extraction. `Restrict`/`Try`/`Ref`/`RefMut` are runtime no-ops and values are freely cloned (no runtime resource discipline). The "implements the equivalent big-step semantics" prose in `proofs/shared/operational-semantics/` is **unproven** (and references op-sem docs that do not exist). | -| Echo modality wired into surface + checker | **absent** | `types.rs` `EchoMode`/`Ty::Echo` (the `linear ⊑ affine` thin poset, faithful to echo-types) is **inert** — never produced by the parser or consumed by the checker; no surface syntax maps to it. | -| Session/ensemble runtime refining `cstep`/`nstep`/`gstep` | **absent** | the machine-checked session metatheory has no executable counterpart (`Go`/`Await` collapse to sequential execution; no channel/process value). | -| Concrete `me` surface exercising the M1 elaboration | **absent (by design)** | M1 (`me_wt_sound`) is machine-checked over an **abstract** Coq `me_tm`; there is no concrete `me` grammar/lexer/parser in code (`_exploratory/me-scaffolding/SIDELINED.adoc` — `me` is intended as a runtime projector). So "the `me` surface elaborates into solo" is machine-checked at the **AST level only**. | +| 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`". | +| 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. | +| 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 > between *proved* (the four-axis core) and *implemented* (the AI-first diff --git a/proofs/verification/coq/solo-core/Eval.v b/proofs/verification/coq/solo-core/Eval.v new file mode 100644 index 0000000..277e4f0 --- /dev/null +++ b/proofs/verification/coq/solo-core/Eval.v @@ -0,0 +1,198 @@ +(* SPDX-License-Identifier: MPL-2.0 *) +(* SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell *) +(* + * A FUNCTIONAL one-step evaluator `step1 : tm -> option tm` for the solo core, + * proved SOUND (and COMPLETE) with respect to the reference `step` RELATION of + * SoloCore.v. The reference semantics is a relation (Prop), so it cannot be + * extracted/run directly; `step1` is the executable mirror, and + * + * step1_sound : step1 t = Some t' -> step t t' (every evaluator step + * is sanctioned by spec) + * step1_complete : step t t' -> step1 t = Some t' (the evaluator finds a + * step whenever spec can) + * + * make it a faithful decision procedure for one CBV step. `step1` is extracted + * (Extract.v) and differentially conformance-tested against the Rust evaluator + * `my_qtt::step1` (conformance/eval/), closing impl ⇄ spec coupling #2 + * (interpreter adequacy vs Coq `step`) over the shared solo `tm` language. + * + * In CI (`_CoqProject` lists this file) `coqc` checks both theorems `Qed`. + *) +From SoloCore Require Import SoloCore. +From SoloCore Require Import EchoMode. +Require Import Coq.Bool.Bool. + +(* ---------- decidable value predicate ---------- *) + +Fixpoint is_value (t : tm) : bool := + match t with + | UnitT => true + | Lam _ _ _ => true + | With a b => is_value a && is_value b + | Inl _ a => is_value a + | Inr _ a => is_value a + | MkEcho _ _ _ a => is_value a + | Tensor a b => is_value a && is_value b + | _ => false + end. + +Lemma is_value_value : forall t, is_value t = true -> value t. +Proof. + induction t; simpl; intro H; try discriminate; + try (apply andb_prop in H as [H1 H2]); + constructor; auto. +Qed. + +Lemma value_is_value : forall t, value t -> is_value t = true. +Proof. + induction 1; simpl; + repeat match goal with + | [ H : is_value ?v = true |- context[is_value ?v] ] => rewrite H + end; + reflexivity. +Qed. + +(* ---------- the functional one-step evaluator ---------- *) + +Fixpoint step1 (t : tm) : option tm := + match t with + | Var _ | UnitT | Lam _ _ _ => None + | App t1 t2 => + match step1 t1 with + | Some t1' => Some (App t1' t2) + | None => + if is_value t1 then + match step1 t2 with + | Some t2' => Some (App t1 t2') + | None => + if is_value t2 + then match t1 with + | Lam _ _ body => Some (subst0 t2 body) + | _ => None + end + else None + end + else None + end + | With t1 t2 => + match step1 t1 with + | Some t1' => Some (With t1' t2) + | None => + if is_value t1 + then match step1 t2 with Some t2' => Some (With t1 t2') | None => None end + else None + end + | Fst t0 => + match step1 t0 with + | Some t0' => Some (Fst t0') + | None => match t0 with + | With v1 v2 => if is_value v1 && is_value v2 then Some v1 else None + | _ => None + end + end + | Snd t0 => + match step1 t0 with + | Some t0' => Some (Snd t0') + | None => match t0 with + | With v1 v2 => if is_value v1 && is_value v2 then Some v2 else None + | _ => None + end + end + | Tensor t1 t2 => + match step1 t1 with + | Some t1' => Some (Tensor t1' t2) + | None => + if is_value t1 + then match step1 t2 with Some t2' => Some (Tensor t1 t2') | None => None end + else None + end + | LetPair t1 t2 => + match step1 t1 with + | Some t1' => Some (LetPair t1' t2) + | None => match t1 with + | Tensor v1 v2 => + if is_value v1 && is_value v2 then Some (subst2 v1 v2 t2) else None + | _ => None + end + end + | Inl b t0 => match step1 t0 with Some t0' => Some (Inl b t0') | None => None end + | Inr a t0 => match step1 t0 with Some t0' => Some (Inr a t0') | None => None end + | Case s tL tR => + match step1 s with + | Some s' => Some (Case s' tL tR) + | None => match s with + | Inl _ v => if is_value v then Some (subst0 v tL) else None + | Inr _ v => if is_value v then Some (subst0 v tR) else None + | _ => None + end + end + | Let q t1 t2 => + match step1 t1 with + | Some t1' => Some (Let q t1' t2) + | None => if is_value t1 then Some (subst0 t1 t2) else None + end + | MkEcho m a b t0 => + match step1 t0 with Some t0' => Some (MkEcho m a b t0') | None => None end + | Weaken t0 => + match step1 t0 with + | Some t0' => Some (Weaken t0') + | None => match t0 with + | MkEcho Linear a b v => if is_value v then Some (MkEcho Affine a b v) else None + | _ => None + end + end + end. + +(* values do not step (functionally) *) +Lemma value_no_step1 : forall t, value t -> step1 t = None. +Proof. + induction 1; simpl; + repeat match goal with + | [ H : step1 ?t = None |- context[step1 ?t] ] => rewrite H + | [ H : value ?v |- context[is_value ?v] ] => rewrite (value_is_value v H) + end; + reflexivity. +Qed. + +(* ---------- SOUNDNESS: functional step is a relational step ---------- *) + +(* Hint set: every `step` constructor + the value-decision soundness bridge. + The proof below is name-INDEPENDENT (it never refers to a destruct-generated + variable), so it is robust to Coq's argument-naming for `tm`. *) +#[local] Hint Constructors step : eval. +#[local] Hint Resolve is_value_value : eval. +(* `destruct (step1 s) eqn:` specialises the IH to `Some v = Some ? -> step s ?`; + discharging the residual `Some v = Some v` needs reflexivity, which eauto does + not try unaided. *) +#[local] Hint Extern 0 (@eq (option _) _ _) => reflexivity : eval. + +Theorem step1_sound : forall t t', step1 t = Some t' -> step t t'. +Proof. + induction t; simpl; intros t' H; try discriminate; + (* peel every `match step1 _`, `if is_value _`, and redex `match _` + scrutinee inside H, reducing the iota-redex each time so the loop + makes progress and terminates *) + repeat (match type of H with + | context[match step1 ?s with _ => _ end] => destruct (step1 s) eqn:?; simpl in H + | context[if ?b then _ else _] => destruct b eqn:?; simpl in H + | context[match ?x with _ => _ end] => destruct x; simpl in H + end); + try discriminate; try (injection H as <-); + repeat match goal with + | [ E : is_value ?a && is_value ?b = true |- _ ] => apply andb_prop in E as [? ?] + end; + eauto 8 with eval. +Qed. + +(* ---------- COMPLETENESS: relational step is found by the function ---------- *) + +Theorem step1_complete : forall t t', step t t' -> step1 t = Some t'. +Proof. + induction 1; simpl; + repeat match goal with + | [ IH : step1 ?t = Some _ |- context[step1 ?t] ] => rewrite IH + | [ H : value ?v |- context[step1 ?v] ] => rewrite (value_no_step1 v H) + | [ H : value ?v |- context[is_value ?v] ] => rewrite (value_is_value v H) + end; + reflexivity. +Qed. diff --git a/proofs/verification/coq/solo-core/Extract.v b/proofs/verification/coq/solo-core/Extract.v new file mode 100644 index 0000000..416259c --- /dev/null +++ b/proofs/verification/coq/solo-core/Extract.v @@ -0,0 +1,36 @@ +(* SPDX-License-Identifier: MPL-2.0 *) +(* SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell *) +(* + * Extraction of the VERIFIED usage-walk checker `check` (R5) to OCaml, so the + * Rust port in `crates/my-qtt` can be DIFFERENTIALLY CONFORMANCE-TESTED against + * the machine-checked algorithm itself (not just against a handful of hand- + * picked reflexivity vectors). + * + * This file is NOT part of the proof suite (`_CoqProject` does not list it, so + * `make` ignores it). It is consumed only by `conformance/run.sh`, which runs + * coqc -R SoloCore Extract.v + * from a scratch build directory; Coq 8.18 writes the extracted *.ml/*.mli to + * the current working directory. + * + * `check` is a real `Fixpoint : tctx -> tm -> option (ty * uvec)` (SoloCore.v + * ~2128), so it extracts to a total OCaml function. `q` extracts to the bare + * `Zero | One | Omega` enum — constructor-for-constructor identical to the Rust + * `my_qtt::Q`, which is what makes the line-by-line result comparison exact. + *) +From SoloCore Require Import SoloCore. +From SoloCore Require Import Eval. +From SoloCore Require Import SessionEval. +Require Coq.extraction.Extraction. +Extraction Language OCaml. + +(* Use native OCaml ints for the de Bruijn `nat` so the oracle and the Rust + `usize`-indexed terms share one numeric vocabulary in the S-expression + bridge. The checker only ever pattern-matches O/S and never does unbounded + arithmetic on indices, so int is faithful for the corpus sizes used. *) +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. diff --git a/proofs/verification/coq/solo-core/SessionEval.v b/proofs/verification/coq/solo-core/SessionEval.v new file mode 100644 index 0000000..91a5c31 --- /dev/null +++ b/proofs/verification/coq/solo-core/SessionEval.v @@ -0,0 +1,48 @@ +(* SPDX-License-Identifier: MPL-2.0 *) +(* SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell *) +(* + * A FUNCTIONAL session-configuration stepper `cstep1 : config -> option config` + * for the binary fused `(νc)(P∣Q)` form of SessionPi.v, proved SOUND and + * COMPLETE w.r.t. the reference `cstep` RELATION (S1.1b). The reference is a + * relation (Prop) and so not extractable/runnable; `cstep1` is its executable + * mirror — extracted (Extract.v) and differentially conformance-tested against + * a Rust session runtime (`my_qtt::session`), closing impl ⇄ spec coupling #4 + * (session runtime refining `cstep`) for the binary fragment. + * + * cstep1_sound : cstep1 c = Some c' -> cstep c c' + * cstep1_complete : cstep c c' -> cstep1 c = Some c' + * + * In CI (`_CoqProject` lists this file) `coqc` checks both `Qed`. + *) +From SoloCore Require Import SessionPi. + +(* one synchronous communication step of the fused two-party config: + a send meets the dual receive (payload substituted), or a select meets the + dual branch (label looked up). Mirrors the 4 `cstep` constructors. *) +Definition cstep1 (c : config) : option config := + match c with + | Conf (QSend v p) (QRecv q) => Some (Conf p (open_party v q)) + | Conf (QRecv q) (QSend v p) => Some (Conf (open_party v q) p) + | Conf (QSel l p) (QBra bs) => + match pget l bs with Some q => Some (Conf p q) | None => None end + | Conf (QBra bs) (QSel l p) => + match pget l bs with Some q => Some (Conf q p) | None => None end + | _ => None + end. + +#[local] Hint Constructors cstep : sess. + +Theorem cstep1_sound : forall c c', cstep1 c = Some c' -> cstep c c'. +Proof. + intros [p1 p2] c' H; destruct p1; destruct p2; simpl in H; + repeat (match type of H with + | context[match pget ?l ?bs with _ => _ end] => destruct (pget l bs) eqn:? + end); + try discriminate; injection H as <-; eauto with sess. +Qed. + +Theorem cstep1_complete : forall c c', cstep c c' -> cstep1 c = Some c'. +Proof. + induction 1; simpl; try reflexivity; + match goal with [ H : pget _ _ = _ |- _ ] => rewrite H end; reflexivity. +Qed. diff --git a/proofs/verification/coq/solo-core/_CoqProject b/proofs/verification/coq/solo-core/_CoqProject index 1df8967..01f7da1 100644 --- a/proofs/verification/coq/solo-core/_CoqProject +++ b/proofs/verification/coq/solo-core/_CoqProject @@ -4,9 +4,11 @@ Quantity.v EchoMode.v ResourceAlgebra.v SoloCore.v +Eval.v Tropical.v Context.v ContextProps.v EchoResidue.v EchoMeasure.v SessionPi.v +SessionEval.v diff --git a/proofs/verification/coq/solo-core/conformance/README.adoc b/proofs/verification/coq/solo-core/conformance/README.adoc new file mode 100644 index 0000000..bc0a8c9 --- /dev/null +++ b/proofs/verification/coq/solo-core/conformance/README.adoc @@ -0,0 +1,70 @@ +// SPDX-License-Identifier: MPL-2.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell += QTT conformance harness + +Differential-conformance evidence for impl ⇄ spec couplings #1 and #2 +(`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. + +(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`.) + +Rather than a (currently infeasible) full Rust-in-Coq refinement proof, this +harness establishes the coupling by **differential testing against the +extracted verified algorithm**: + +[source] +---- + Coq `check` (R5, verified) Rust `my_qtt::check` (port) + │ Extract.v │ + ▼ (Separate Extraction) │ + OCaml oracle.ml ◀── corpus.sexp ── conformance_gen ──▶ rust_results.txt + │ │ + ▼ ▼ + coq_results.txt ─────────── diff (must be identical) ───────┘ +---- + +If `diff` is empty over a large random corpus, then on every tested term the +Rust port and the *machine-checked* algorithm make the same accept/reject +decision and synthesize the same type and usage vector. + +== Run + +[source,sh] +---- +cd proofs/verification/coq/solo-core +COUNT=5000 SEED=1 ./conformance/run.sh # PASS / FAIL, exit 0 / 1 +---- + +Requires `coqc` (8.18), `ocamlfind` + `ocamlc`/`ocamlopt`, and `cargo` +(all present in the proof CI image). All build artifacts land in +`conformance/_build/` (git-ignored). `SoloCore.vo` must be built first +(`make` in this directory). + +== Files + +* `../Extract.v` — extracts the verified `check` to OCaml (not in `_CoqProject`; + `make` ignores it). +* `oracle.ml` — reads `(q (ctx TY...) TM)` queries, runs the extracted `check`, + prints the canonical result. +* `../../../../../crates/my-qtt/src/bin/conformance_gen.rs` — random corpus + + Rust `my_qtt::check` results, with canonical printers byte-matching `oracle.ml`. +* `run.sh` — orchestrates extract → compile oracle → generate → diff. + +== Scope / honesty + +* This is refinement-by-conformance against the *extracted* verified `check`, + not a full Rust-in-Coq refinement proof. +* It tests the closed/open-context checker over the solo QTT term language + (including echo `MkEcho`/`Weaken`/`TEcho`). It does not test the wider + AI-surface compiler frontend. +* Making the verified core the *default* path in `crates/my-lang/src/checker.rs` + (today it is reachable only via the opt-in `qtt_bridge`) is a separate + programme item — see `docs/STATUS.adoc` (INTEND). diff --git a/proofs/verification/coq/solo-core/conformance/oracle.ml b/proofs/verification/coq/solo-core/conformance/oracle.ml new file mode 100644 index 0000000..153e42d --- /dev/null +++ b/proofs/verification/coq/solo-core/conformance/oracle.ml @@ -0,0 +1,218 @@ +(* SPDX-License-Identifier: MPL-2.0 *) +(* SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell *) +(* + * Differential-conformance ORACLE for the QTT checker coupling. + * + * Links against the OCaml that `Extract.v` extracts from the VERIFIED Coq + * `check` (R5). Reads one query S-expression per stdin line + * (q (ctx TY...) TM) + * builds the corresponding `SoloCore.tctx` / `SoloCore.tm`, runs the extracted + * `SoloCore.check`, and prints the result in the SAME canonical form the Rust + * `conformance_gen` binary prints — so `diff` of the two output streams is the + * refinement check "Rust `my_qtt::check` == extracted Coq `check`". + * + * The oracle parses; it never generates. Inputs come from the Rust side, so the + * two implementations are genuinely independent. + *) + +open SoloCore +open Eval +open SessionPi +open SessionEval +open Quantity + +(* ---------- tiny S-expression reader ---------- *) + +type sexp = Atom of string | List of sexp list + +let tokenize (s : string) : string list = + let b = Buffer.create (String.length s * 2) in + String.iter (fun c -> + match c with + | '(' | ')' -> Buffer.add_char b ' '; Buffer.add_char b c; Buffer.add_char b ' ' + | _ -> Buffer.add_char b c) s; + Buffer.contents b + |> String.split_on_char ' ' + |> List.filter (fun t -> t <> "") + +let parse_sexp (toks : string list) : sexp = + let rec go toks = + match toks with + | [] -> failwith "unexpected eof" + | "(" :: rest -> + let rec loop acc toks = + match toks with + | ")" :: rest -> (List (List.rev acc), rest) + | [] -> failwith "unterminated list" + | _ -> let (e, rest') = go toks in loop (e :: acc) rest' + in loop [] rest + | ")" :: _ -> failwith "unexpected )" + | a :: rest -> (Atom a, rest) + in + let (e, rest) = go toks in + (match rest with [] -> () | _ -> failwith "trailing tokens"); + e + +(* ---------- sexp -> Coq AST ---------- *) + +let q_of = function + | Atom "0" -> Zero | Atom "1" -> One | Atom "w" -> Omega + | _ -> failwith "bad q" + +let m_of = function + | Atom "lin" -> EchoMode.Linear | Atom "aff" -> EchoMode.Affine + | _ -> failwith "bad mode" + +let rec ty_of = function + | Atom "unit" -> TUnit + | List [Atom "with"; a; b] -> TWith (ty_of a, ty_of b) + | List [Atom "tensor"; a; b] -> TTensor (ty_of a, ty_of b) + | List [Atom "sum"; a; b] -> TSum (ty_of a, ty_of b) + | List [Atom "arr"; q; a; b] -> TArr (q_of q, ty_of a, ty_of b) + | List [Atom "echo"; m; a; b] -> TEcho (m_of m, ty_of a, ty_of b) + | _ -> failwith "bad ty" + +let rec tm_of = function + | List [Atom "var"; Atom n] -> Var (int_of_string n) + | Atom "star" -> UnitT + | List [Atom "lam"; q; a; t] -> Lam (q_of q, ty_of a, tm_of t) + | List [Atom "app"; f; x] -> App (tm_of f, tm_of x) + | List [Atom "with"; a; b] -> With (tm_of a, tm_of b) + | List [Atom "fst"; t] -> Fst (tm_of t) + | List [Atom "snd"; t] -> Snd (tm_of t) + | List [Atom "tensor"; a; b] -> Tensor (tm_of a, tm_of b) + | List [Atom "letpair"; a; b] -> LetPair (tm_of a, tm_of b) + | List [Atom "inl"; ty; t] -> Inl (ty_of ty, tm_of t) + | List [Atom "inr"; ty; t] -> Inr (ty_of ty, tm_of t) + | List [Atom "case"; s; l; r] -> Case (tm_of s, tm_of l, tm_of r) + | List [Atom "let"; q; a; b] -> Let (q_of q, tm_of a, tm_of b) + | List [Atom "mkecho"; m; a; b; t] -> MkEcho (m_of m, ty_of a, ty_of b, tm_of t) + | List [Atom "weaken"; t] -> Weaken (tm_of t) + | _ -> failwith "bad tm" + +(* context list is OUTERMOST-first; fold into TSnoc so the LAST element is the + outer snoc = de Bruijn 0 (matches Rust `Vec` where `.last()` is db0). *) +let ctx_of = function + | List (Atom "ctx" :: tys) -> + List.fold_left (fun acc s -> TSnoc (acc, ty_of s)) TEmpty tys + | _ -> failwith "bad ctx" + +(* ---------- canonical printer (MUST match the Rust side) ---------- *) + +let show_q = function Zero -> "0" | One -> "1" | Omega -> "w" +let show_m = function EchoMode.Linear -> "lin" | EchoMode.Affine -> "aff" + +let rec show_ty = function + | TUnit -> "unit" + | TWith (a, b) -> "(with " ^ show_ty a ^ " " ^ show_ty b ^ ")" + | TTensor (a, b) -> "(tensor " ^ show_ty a ^ " " ^ show_ty b ^ ")" + | TSum (a, b) -> "(sum " ^ show_ty a ^ " " ^ show_ty b ^ ")" + | TArr (q, a, b) -> "(arr " ^ show_q q ^ " " ^ show_ty a ^ " " ^ show_ty b ^ ")" + | TEcho (m, a, b) -> "(echo " ^ show_m m ^ " " ^ show_ty a ^ " " ^ show_ty b ^ ")" + +(* uvec OUTERMOST-first: recurse into `rest` before emitting the outer `q`, so + db0 (the outer USnoc) prints LAST — identical to the Rust `Vec` index order. *) +let show_uvec u = + let rec go = function UEmpty -> [] | USnoc (rest, q) -> go rest @ [show_q q] in + "[" ^ String.concat " " (go u) ^ "]" + +let show_result = function + | None -> "none" + | Some (a, d) -> "(ok " ^ show_ty a ^ " " ^ show_uvec d ^ ")" + +(* canonical term printer — MUST match conformance_gen's `sexp_tm` *) +let rec show_tm = function + | Var n -> "(var " ^ string_of_int n ^ ")" + | UnitT -> "star" + | Lam (q, a, t) -> "(lam " ^ show_q q ^ " " ^ show_ty a ^ " " ^ show_tm t ^ ")" + | App (f, x) -> "(app " ^ show_tm f ^ " " ^ show_tm x ^ ")" + | With (a, b) -> "(with " ^ show_tm a ^ " " ^ show_tm b ^ ")" + | Fst t -> "(fst " ^ show_tm t ^ ")" + | Snd t -> "(snd " ^ show_tm t ^ ")" + | Tensor (a, b) -> "(tensor " ^ show_tm a ^ " " ^ show_tm b ^ ")" + | LetPair (a, b) -> "(letpair " ^ show_tm a ^ " " ^ show_tm b ^ ")" + | Inl (ty, t) -> "(inl " ^ show_ty ty ^ " " ^ show_tm t ^ ")" + | Inr (ty, t) -> "(inr " ^ show_ty ty ^ " " ^ show_tm t ^ ")" + | Case (s, l, r) -> "(case " ^ show_tm s ^ " " ^ show_tm l ^ " " ^ show_tm r ^ ")" + | Let (q, a, b) -> "(let " ^ show_q q ^ " " ^ show_tm a ^ " " ^ show_tm b ^ ")" + | MkEcho (m, a, b, t) -> + "(mkecho " ^ show_m m ^ " " ^ show_ty a ^ " " ^ show_ty b ^ " " ^ show_tm t ^ ")" + | Weaken t -> "(weaken " ^ show_tm t ^ ")" + +let show_step = function None -> "none" | Some t -> "(some " ^ show_tm t ^ ")" + +(* iterate the verified step1 to a normal form (or fuel cap); both sides use the + SAME cap so a divergent term yields the same capped term. *) +let rec eval_nf fuel t = + if fuel <= 0 then t + else match step1 t with None -> t | Some t' -> eval_nf (fuel - 1) t' + +(* ---------- session configs (coupling #4) ---------- *) + +let val_of = function + | List [Atom "vvar"; Atom n] -> VVar (int_of_string n) + | Atom "vunit" -> VUnit + | List [Atom "vbool"; Atom "t"] -> VBool true + | List [Atom "vbool"; Atom "f"] -> VBool false + | List [Atom "vnat"; Atom n] -> VNat (int_of_string n) + | _ -> failwith "bad val" + +(* pbranch is built from `(br L PARTY)` items, right-folded into PBcons/PBnil *) +let rec party_of = function + | Atom "qend" -> QEnd + | List [Atom "qsend"; v; p] -> QSend (val_of v, party_of p) + | List [Atom "qrecv"; p] -> QRecv (party_of p) + | List [Atom "qsel"; Atom l; p] -> QSel (int_of_string l, party_of p) + | List (Atom "qbra" :: brs) -> QBra (pbranch_of brs) + | _ -> failwith "bad party" +and pbranch_of = function + | [] -> PBnil + | List [Atom "br"; Atom l; p] :: rest -> PBcons (int_of_string l, party_of p, pbranch_of rest) + | _ -> failwith "bad pbranch" + +let config_of = function + | List [Atom "conf"; p1; p2] -> Conf (party_of p1, party_of p2) + | _ -> failwith "bad config" + +let show_val = function + | VVar n -> "(vvar " ^ string_of_int n ^ ")" + | VUnit -> "vunit" + | VBool true -> "(vbool t)" + | VBool false -> "(vbool f)" + | VNat n -> "(vnat " ^ string_of_int n ^ ")" + +let rec show_party = function + | QEnd -> "qend" + | QSend (v, p) -> "(qsend " ^ show_val v ^ " " ^ show_party p ^ ")" + | QRecv p -> "(qrecv " ^ show_party p ^ ")" + | QSel (l, p) -> "(qsel " ^ string_of_int l ^ " " ^ show_party p ^ ")" + | QBra bs -> "(qbra" ^ show_pbranch bs ^ ")" +and show_pbranch = function + | PBnil -> "" + | PBcons (l, p, rest) -> " (br " ^ string_of_int l ^ " " ^ show_party p ^ ")" ^ show_pbranch rest + +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 ^ ")" + +(* ---------- driver ---------- *) + +let () = + try + while true do + let line = input_line stdin in + if String.trim line <> "" then begin + let q = parse_sexp (tokenize line) in + match q with + | List [Atom "q"; ctx; tm] -> (* checker query (coupling #1) *) + print_endline (show_result (check (ctx_of ctx) (tm_of tm))) + | List [Atom "s"; tm] -> (* one CBV step (coupling #2) *) + 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) *) + print_endline (show_cstep (cstep1 (config_of cfg))) + | _ -> failwith "bad query" + end + done + with End_of_file -> () diff --git a/proofs/verification/coq/solo-core/conformance/run.sh b/proofs/verification/coq/solo-core/conformance/run.sh new file mode 100755 index 0000000..5831c5b --- /dev/null +++ b/proofs/verification/coq/solo-core/conformance/run.sh @@ -0,0 +1,72 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +# +# Differential-conformance harness for the QTT checker coupling (#1). +# +# Asserts: ∀ (g,t) in a random corpus. +# my_qtt::check g t == (Coq-extracted check) g t +# +# Pipeline: +# 1. coqc Extract.v -> OCaml extracted from the VERIFIED `check` +# 2. ocaml compile oracle.ml -> the verified-checker ORACLE binary +# 3. cargo run conformance_gen -> corpus.sexp + rust_results.txt +# 4. ./oracle < corpus.sexp -> coq_results.txt +# 5. diff rust_results.txt coq_results.txt (must be identical) +# +# Requires: coqc (8.18), ocamlfind + ocamlc/ocamlopt, cargo. All present in the +# proof CI image. Env: COUNT (default 3000), SEED (default 1). +set -euo pipefail + +HERE="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)" +SC="$(cd "$HERE/.." && pwd)" # solo-core dir +ROOT="$(cd "$SC/../../../.." && pwd)" # repo root +BUILD="$HERE/_build" +COUNT="${COUNT:-3000}" +SEED="${SEED:-1}" + +echo "== QTT checker conformance ==" +echo " solo-core: $SC" +echo " repo root: $ROOT" +rm -rf "$BUILD"; mkdir -p "$BUILD" + +echo "-- 1. extract verified check -> OCaml" +( cd "$BUILD" && coqc -R "$SC" SoloCore "$SC/Extract.v" >/dev/null ) + +echo "-- 2. compile the oracle" +cp "$HERE/oracle.ml" "$BUILD/oracle.ml" +# dependency-sort ALL extracted modules (robust to whatever Coq emits — +# PeanoNat, BinNat, ...); compile each module's .mli then .ml, oracle last. +( cd "$BUILD" + FILES="" + for ml in $(ocamldep -sort *.ml); do + base="${ml%.ml}" + [ -f "$base.mli" ] && FILES="$FILES $base.mli" + FILES="$FILES $ml" + done + ocamlc -w -a -o oracle $FILES ) + +echo "-- 3. generate corpus + rust results (count=$COUNT seed=$SEED)" +( cd "$ROOT" && cargo build -q -p my-qtt --bin conformance_gen ) +GEN="$ROOT/target/debug/conformance_gen" +"$GEN" "$COUNT" "$SEED" "$BUILD/corpus.sexp" "$BUILD/rust_results.txt" + +echo "-- 4. run the verified oracle over the corpus" +"$BUILD/oracle" < "$BUILD/corpus.sexp" > "$BUILD/coq_results.txt" + +echo "-- 5. compare" +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)" + exit 0 +else + echo "FAIL: Rust and verified-Coq results differ:" + head -40 "$BUILD/diff.txt" + exit 1 +fi diff --git a/proofs/verification/idris/solo-core/Soundness.idr b/proofs/verification/idris/solo-core/Soundness.idr index 5969598..2ff7c92 100644 --- a/proofs/verification/idris/solo-core/Soundness.idr +++ b/proofs/verification/idris/solo-core/Soundness.idr @@ -323,7 +323,7 @@ preservation : {g : Tctx} -> {d : Uvec} -> (t : Tm) -> Has g d t a -> Step t t' -> Has g d t' a preservation (App (Lam q' a0 tb) v) (THApp d1 d2 q' (THLam hb) h2 prf) (SApp vval) = let (dgr ** (hadd, hht)) = substLemma0 g a0 d1 q' tb d2 v hb h2 - in coeUsage (justInj' (trans (sym hadd) prf)) hht + in coeUse (justInj' (trans (sym hadd) prf)) hht -- additive projections fire on a With value preservation (Fst (With v1 v2)) (THFst (THWith h1 h2)) (SFst v1v v2v) = h1 preservation (Snd (With v1 v2)) (THSnd (THWith h1 h2)) (SSnd v1v v2v) = h2 @@ -331,21 +331,21 @@ preservation (Snd (With v1 v2)) (THSnd (THWith h1 h2)) (SSnd v1v v2v) = h2 preservation (Case (Inl bb v) tL tR) (THCase d1 d2 aa bb (THInl hv) hL hR prf) (SCaseL vval) = let (dgr ** (hadd, hht)) = substLemma0 g aa d2 One tL d1 v hL hv - in coeUsage + in coeUse (justInj' (trans (sym (trans (uaddComm d1 d2) (trans (sym (cong (uadd d2) (uscaleOne d1))) hadd))) prf)) hht preservation (Case (Inr aa v) tL tR) (THCase d1 d2 aa bb (THInr hv) hL hR prf) (SCaseR vval) = let (dgr ** (hadd, hht)) = substLemma0 g bb d2 One tR d1 v hR hv - in coeUsage + in coeUse (justInj' (trans (sym (trans (uaddComm d1 d2) (trans (sym (cong (uadd d2) (uscaleOne d1))) hadd))) prf)) hht -- let binding: substitute the bound value preservation (Let q1 v t2) (THLet d1 d2 q1 aa h1 h2 prf) (SLet vval) = let (dgr ** (hadd, hht)) = substLemma0 g aa d2 q1 t2 d1 v h2 h1 - in coeUsage + in coeUse (justInj' (trans (sym (trans (uaddComm (uscale q1 d1) d2) hadd)) prf)) hht -- multiplicative let-pair: two-variable substitution of the tensor components diff --git a/proofs/verification/idris/solo-core/Substitution.idr b/proofs/verification/idris/solo-core/Substitution.idr index 284d8eb..dec96ea 100644 --- a/proofs/verification/idris/solo-core/Substitution.idr +++ b/proofs/verification/idris/solo-core/Substitution.idr @@ -935,3 +935,58 @@ substLemma0 : (g : Tctx) -> (a : Ty) -> (dg : Uvec) -> (q : Q) -> (t : Tm) -> Has g du u a -> (dgr : Uvec ** (uadd dg (uscale q du) = Just dgr, Has g dgr (subst0 u t) b)) substLemma0 g a dg q t du u ht hu = htSubst t TEmpty g a dg q UEmpty du u Refl ht hu + +||| Retype a derivation along a usage equality. `subst2Lemma` uses it to reshape +||| the residual usages the two nested `substLemma0` calls produce. (Soundness +||| keeps its own private `coeUse` of the same shape for `preservation`.) +public export +coeUsage : d = d' -> Has g d t b -> Has g d' t b +coeUsage Refl x = x + +||| Two-variable substitution lemma (mirrors Coq `subst2_lemma`): the `LetPair` +||| eliminator substitutes BOTH tensor components into the two-binder body `t`. +||| Two nested `substLemma0` applications — first the pre-shifted `u2` under the +||| inner (type-`b`) binder, then `u1` for the (now top) type-`a` binder — with +||| the residual usages realigned via `uaddAssoc` / `uaddComm`. `subst2 u1 u2 t` +||| reduces definitionally to `subst0 u1 (subst0 (shift 0 u2) t)`, exactly what +||| the outer call yields. The `S_LetPair` case of `preservation` consumes this. +public export +subst2Lemma : (g : Tctx) -> (a, b : Ty) -> (d, d1, d2, dv1, dv2 : Uvec) + -> (t, u1, u2 : Tm) -> {0 c : Ty} + -> Has (TSnoc (TSnoc g a) b) (USnoc (USnoc d2 One) One) t c + -> Has g dv1 u1 a + -> Has g dv2 u2 b + -> uadd dv1 dv2 = Just d1 + -> uadd d1 d2 = Just d + -> Has g d (subst2 u1 u2 t) c +subst2Lemma g a b d d1 d2 dv1 dv2 t u1 u2 ht hu1 hu2 hd1 hd = + -- inner substitution: (shift 0 u2) for the index-0, type-`b` binder + let (dr1 ** (hadd1, hht1)) = + substLemma0 (TSnoc g a) b (USnoc d2 One) One t (USnoc dv2 Zero) + (shift 0 u2) ht (htShift0 g a dv2 u2 hu2) in + -- the residual `dr1` reshapes to `USnoc dr1g One`, where `dr1g = D2 + Dv2` + let (dr1g ** hdr1g) = + uaddTotal d2 dv2 + (trans (predEq' (predEq' (shapeType (TSnoc (TSnoc g a) b) t ht))) + (sym (shapeType g u2 hu2))) in + let hht1' = coeUsage + (justInj' + (trans (sym (trans (sym (cong (uadd (USnoc d2 One)) + (uscaleOne (USnoc dv2 Zero)))) hadd1)) + (trans (uaddUSnocReduce d2 dv2 One Zero) + (trans (cong (combMaybe (qAdd One Zero)) hdr1g) + (cong (\z => Just (USnoc dr1g z)) (qAddZeroR One)))))) + hht1 in + -- outer substitution: u1 for the (now top) type-`a` binder + let (dr ** (hadd2, hht2)) = + substLemma0 g a dr1g One (subst0 (shift 0 u2) t) dv1 u1 hht1' hu1 in + -- realign `dr = d` via associativity: (Dv1+Dv2)+D2 = Dv1+(D2+Dv2) = Dv1+Dr1g = Dr + let (yz ** (hyz, hx)) = uaddAssoc dv1 dv2 d2 d1 d hd1 hd in + coeUsage + (sym (justInj' + (trans (sym hx) + (trans (cong (uadd dv1) + (justInj' (trans (sym (trans (sym (uaddComm dv2 d2)) hyz)) hdr1g))) + (trans (uaddComm dv1 dr1g) + (trans (sym (cong (uadd dr1g) (uscaleOne dv1))) hadd2)))))) + hht2