From 25bce9aef7e6e3c719792e4491b2b30aaa2115fc Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 21 Oct 2026 19:47:39 +0000 Subject: [PATCH 1/4] gkat-probe: D-GKAT-0 bounded GKAT fixture for structured Rubicon flows Lab crate, zero dependencies, excluded from the workspace. Guarded Thompson automata, normalization and union-find bisimulation decide equivalence over a declared atom set of at most 8 tests; a separate check requires WHERE(rev) and WHERE(mul) immediately before every RequestCommit. Unguarded choice, GoTo, GoBack, undeclared projections and more than 8 tests are refused. Every verdict is cross-checked against an independent bounded interpreter. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01VncKoyG6JkpsoqhqTGTv3f --- .github/workflows/gkat-probe.yml | 35 ++ Cargo.toml | 3 + crates/gkat-probe/Cargo.toml | 14 + crates/gkat-probe/src/automaton.rs | 343 +++++++++++++++++++ crates/gkat-probe/src/expr.rs | 252 ++++++++++++++ crates/gkat-probe/src/flow.rs | 267 +++++++++++++++ crates/gkat-probe/src/lib.rs | 49 +++ crates/gkat-probe/src/oracle.rs | 175 ++++++++++ crates/gkat-probe/src/rubicon.rs | 233 +++++++++++++ crates/gkat-probe/tests/differential.rs | 138 ++++++++ crates/gkat-probe/tests/g1_factoring.rs | 58 ++++ crates/gkat-probe/tests/g2_nondeterminism.rs | 51 +++ crates/gkat-probe/tests/g5_atoms.rs | 93 +++++ crates/gkat-probe/tests/rubicon.rs | 149 ++++++++ 14 files changed, 1860 insertions(+) create mode 100644 .github/workflows/gkat-probe.yml create mode 100644 crates/gkat-probe/Cargo.toml create mode 100644 crates/gkat-probe/src/automaton.rs create mode 100644 crates/gkat-probe/src/expr.rs create mode 100644 crates/gkat-probe/src/flow.rs create mode 100644 crates/gkat-probe/src/lib.rs create mode 100644 crates/gkat-probe/src/oracle.rs create mode 100644 crates/gkat-probe/src/rubicon.rs create mode 100644 crates/gkat-probe/tests/differential.rs create mode 100644 crates/gkat-probe/tests/g1_factoring.rs create mode 100644 crates/gkat-probe/tests/g2_nondeterminism.rs create mode 100644 crates/gkat-probe/tests/g5_atoms.rs create mode 100644 crates/gkat-probe/tests/rubicon.rs diff --git a/.github/workflows/gkat-probe.yml b/.github/workflows/gkat-probe.yml new file mode 100644 index 000000000..52173ea3c --- /dev/null +++ b/.github/workflows/gkat-probe.yml @@ -0,0 +1,35 @@ +name: GKAT probe +# `crates/gkat-probe` (D-GKAT-0) is excluded from the workspace (own +# [workspace], zero dependencies), so no workspace job builds it. +on: + pull_request: + paths: + - 'crates/gkat-probe/**' + - '.github/workflows/gkat-probe.yml' + - 'rust-toolchain.toml' + push: + branches: [main] + paths: + - 'crates/gkat-probe/**' + - '.github/workflows/gkat-probe.yml' + - 'rust-toolchain.toml' + workflow_dispatch: +permissions: + contents: read +jobs: + probe: + runs-on: ubuntu-latest + timeout-minutes: 20 + defaults: + run: + working-directory: crates/gkat-probe + env: + CARGO_PROFILE_DEV_DEBUG: "0" + CARGO_INCREMENTAL: "0" + steps: + - uses: actions/checkout@v4 + - name: Setup rust toolchain (pinned by rust-toolchain.toml) + run: rustup show + - run: cargo fmt --check + - run: cargo clippy --all-targets -- -D warnings + - run: cargo test diff --git a/Cargo.toml b/Cargo.toml index bbe702b9e..049d569b9 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -174,6 +174,9 @@ exclude = [ # -> MORK query_multi -> relalg over the D-MPS-8 table. Own workspace; run # from its directory so `.cargo/config.toml` applies. "crates/crepe-plan-probe", + # D-GKAT-0 PROBE: bounded GKAT equivalence/safety fixture, zero deps, own + # [workspace]. `cargo test --manifest-path crates/gkat-probe/Cargo.toml`. + "crates/gkat-probe", # D-RU-1 (U1) JC statistical batch: one battery of means/variances/ANOVA/ # covariance/Pearson/regression answered from shared power-sum passes vs # request by request. Lab probe, own workspace: `cd crates/jc-batch-probe && cargo test --release`. diff --git a/crates/gkat-probe/Cargo.toml b/crates/gkat-probe/Cargo.toml new file mode 100644 index 000000000..7ff2fabaf --- /dev/null +++ b/crates/gkat-probe/Cargo.toml @@ -0,0 +1,14 @@ +[package] +name = "gkat-probe" +version = "0.0.0" +edition = "2024" +publish = false +description = "D-GKAT-0 PROBE: a bounded research fixture for Guarded Kleene Algebra with Tests (Smolka et al., POPL 2020). Decides equivalence of structured guarded flows over a declared atom set of at most 256 atoms, checks a separate RequestCommit safety property, and refuses constructs outside the admitted fragment. Not a production verifier, runtime or executor." + +# Its own workspace root, excluded from the lance-graph workspace. Zero +# dependencies on purpose: the probe must not become a runtime dependency of +# anything. Run from this directory: +# cd crates/gkat-probe && cargo test +[workspace] + +[dependencies] diff --git a/crates/gkat-probe/src/automaton.rs b/crates/gkat-probe/src/automaton.rs new file mode 100644 index 000000000..b058484f0 --- /dev/null +++ b/crates/gkat-probe/src/automaton.rs @@ -0,0 +1,343 @@ +//! Guarded automata, the Thompson construction, normalization, the +//! bisimulation equivalence check and the separate commit-safety check. +//! +//! Follows Smolka et al. (arXiv:1907.05920): guarded automata (§4.1), the +//! Thompson construction with uniform continuations (§4.2, Proposition 4.2), +//! normalization by removing transitions into states that can never accept +//! (§5.2), and equivalence of normal automata by bisimulation with a +//! union-find, after Hopcroft and Karp (§5.3, Algorithm 1). +//! +//! **Scope.** For expressions in the admitted fragment over a fixed, declared +//! atom set, the paper proves that bisimilarity of the normalized Thompson +//! automata coincides with equivalence of the guarded-string semantics. This +//! module is an implementation of that procedure; its correctness is tested +//! against the independent oracle in [`crate::oracle`], not proven. + +use std::collections::{BTreeSet, VecDeque}; + +use crate::expr::{Action, Atom, Atoms, BExp, Exp, Refusal}; + +/// What a state does on one atom. +#[derive(Clone, Copy, PartialEq, Eq, Debug)] +pub enum Out { + Accept, + Reject, + /// Perform the action, then continue in the state. + Step(Action, usize), +} + +/// A guarded automaton over a declared atom set. `start[a]` and +/// `states[s][a]` are indexed by the atom's position in [`Atoms`]. +#[derive(Clone, Debug)] +pub struct Automaton { + pub start: Vec, + pub states: Vec>, +} + +/// Builds the guarded Thompson automaton of `e` over `atoms`. +pub fn thompson(e: &Exp, atoms: &Atoms) -> Result { + atoms.admit(e)?; + let mut states = Vec::new(); + let start = build(e, atoms, &mut states); + Ok(Automaton { start, states }) +} + +fn uniform(atoms: &Atoms, out: Out) -> Vec { + vec![out; atoms.len()] +} + +fn sat(b: &BExp, atoms: &Atoms, a: usize) -> bool { + b.eval(atoms.get(a)) +} + +/// Returns the initial pseudostate of `e`; appends its states to `states`. +fn build(e: &Exp, atoms: &Atoms, states: &mut Vec>) -> Vec { + match e { + Exp::Fail => uniform(atoms, Out::Reject), + Exp::Skip => uniform(atoms, Out::Accept), + Exp::Assert(b) => (0..atoms.len()) + .map(|a| { + if sat(b, atoms, a) { + Out::Accept + } else { + Out::Reject + } + }) + .collect(), + Exp::Do(p) => { + let s = states.len(); + states.push(uniform(atoms, Out::Accept)); + uniform(atoms, Out::Step(*p, s)) + } + Exp::If(b, e1, e2) => { + let i1 = build(e1, atoms, states); + let i2 = build(e2, atoms, states); + (0..atoms.len()) + .map(|a| if sat(b, atoms, a) { i1[a] } else { i2[a] }) + .collect() + } + Exp::Seq(e1, e2) => { + let lo = states.len(); + let i1 = build(e1, atoms, states); + let hi = states.len(); + let i2 = build(e2, atoms, states); + // Uniform continuation: wherever e1 would accept, continue as e2. + for s in &mut states[lo..hi] { + for (a, out) in s.iter_mut().enumerate() { + if *out == Out::Accept { + *out = i2[a]; + } + } + } + (0..atoms.len()) + .map(|a| if i1[a] == Out::Accept { i2[a] } else { i1[a] }) + .collect() + } + Exp::While(b, body) => { + let lo = states.len(); + let ib = build(body, atoms, states); + let hi = states.len(); + // On ¬b the loop exits. On b it enters the body; a body that + // would accept without acting would repeat on the same atom + // forever, so it rejects (the paper's `e^(b)` construction). + let head: Vec = (0..atoms.len()) + .map(|a| { + if !sat(b, atoms, a) { + Out::Accept + } else { + match ib[a] { + Out::Step(p, s) => Out::Step(p, s), + Out::Accept | Out::Reject => Out::Reject, + } + } + }) + .collect(); + for s in &mut states[lo..hi] { + for (a, out) in s.iter_mut().enumerate() { + if *out == Out::Accept { + *out = head[a]; + } + } + } + head + } + } +} + +impl Automaton { + /// States from which some run accepts. + pub fn live(&self) -> Vec { + let mut live: Vec = self + .states + .iter() + .map(|s| s.contains(&Out::Accept)) + .collect(); + loop { + let mut changed = false; + for (i, s) in self.states.iter().enumerate() { + if !live[i] && s.iter().any(|o| matches!(o, Out::Step(_, t) if live[*t])) { + live[i] = true; + changed = true; + } + } + if !changed { + return live; + } + } + } + + /// Normalization: a step into a state that can never accept is a reject. + pub fn normalize(&self) -> Automaton { + let live = self.live(); + let fix = |row: &Vec| -> Vec { + row.iter() + .map(|o| match o { + Out::Step(_, t) if !live[*t] => Out::Reject, + other => *other, + }) + .collect() + }; + Automaton { + start: fix(&self.start), + states: self.states.iter().map(fix).collect(), + } + } + + /// Indices of the states reachable from the start pseudostate. + pub fn reachable(&self) -> BTreeSet { + let mut seen = BTreeSet::new(); + let mut work: Vec = Vec::new(); + let push = |row: &Vec, seen: &mut BTreeSet, work: &mut Vec| { + for o in row { + if let Out::Step(_, t) = o + && seen.insert(*t) + { + work.push(*t); + } + } + }; + push(&self.start, &mut seen, &mut work); + while let Some(s) = work.pop() { + push(&self.states[s], &mut seen, &mut work); + } + seen + } +} + +/// A guarded-string prefix: the atom observed before each action, and the +/// action taken. +pub type Witness = Vec<(Atom, Action)>; + +/// The result of an equivalence check. +#[derive(Clone, Debug, PartialEq, Eq)] +pub enum Equivalence { + Equivalent { + /// Pairs merged by the union-find (the proof's size). + pairs: usize, + }, + /// The two flows differ on this prefix followed by `atom`. + Different { + prefix: Witness, + atom: Atom, + left: Out, + right: Out, + }, +} + +impl Equivalence { + pub fn holds(&self) -> bool { + matches!(self, Equivalence::Equivalent { .. }) + } +} + +struct UnionFind(Vec); + +impl UnionFind { + fn find(&mut self, x: usize) -> usize { + let mut r = x; + while self.0[r] != r { + r = self.0[r]; + } + let mut y = x; + while self.0[y] != r { + let next = self.0[y]; + self.0[y] = r; + y = next; + } + r + } +} + +/// Decides GKAT equivalence of `e` and `f` over `atoms`. +pub fn equivalent(e: &Exp, f: &Exp, atoms: &Atoms) -> Result { + let x = thompson(e, atoms)?.normalize(); + let y = thompson(f, atoms)?.normalize(); + // Node ids: 0 = x.start, 1..=nx = x.states, nx+1 = y.start, then y.states. + let nx = x.states.len(); + let y0 = nx + 1; + let row = |n: usize| -> &Vec { + if n == 0 { + &x.start + } else if n <= nx { + &x.states[n - 1] + } else if n == y0 { + &y.start + } else { + &y.states[n - y0 - 1] + } + }; + let node_x = |s: usize| s + 1; + let node_y = |s: usize| s + y0 + 1; + let mut uf = UnionFind((0..y0 + 1 + y.states.len()).collect()); + let mut queue: VecDeque<(usize, usize, Witness)> = VecDeque::new(); + queue.push_back((0, y0, Vec::new())); + let mut pairs = 0; + while let Some((p, q, prefix)) = queue.pop_front() { + let (rp, rq) = (uf.find(p), uf.find(q)); + if rp == rq { + continue; + } + uf.0[rp] = rq; + pairs += 1; + let (rowp, rowq) = (row(p), row(q)); + for a in 0..atoms.len() { + match (rowp[a], rowq[a]) { + (Out::Accept, Out::Accept) | (Out::Reject, Out::Reject) => {} + (Out::Step(pa, s), Out::Step(qa, t)) if pa == qa => { + let mut next = prefix.clone(); + next.push((atoms.get(a), pa)); + queue.push_back((node_x(s), node_y(t), next)); + } + (l, r) => { + return Ok(Equivalence::Different { + prefix, + atom: atoms.get(a), + left: l, + right: r, + }); + } + } + } + } + Ok(Equivalence::Equivalent { pairs }) +} + +/// The result of the commit-safety check. +#[derive(Clone, Debug, PartialEq, Eq)] +pub enum Safety { + Safe, + /// A reachable step performs the guarded action on an atom that does not + /// satisfy the authorization. + Unsafe { + prefix: Witness, + atom: Atom, + }, +} + +impl Safety { + pub fn holds(&self) -> bool { + self == &Safety::Safe + } +} + +/// Checks that every reachable step performing `action` happens on an atom +/// satisfying `authorized`. +/// +/// The check runs on the unnormalized automaton: an action that is emitted on +/// a run which later rejects was still emitted, so a run's eventual rejection +/// does not excuse an unauthorized intent. The atom checked is the one +/// observed **immediately** before the action: after any intervening action +/// the environment may have changed every test, so an authorization observed +/// earlier does not carry over. +pub fn commit_safe( + e: &Exp, + atoms: &Atoms, + action: Action, + authorized: &BExp, +) -> Result { + let m = thompson(e, atoms)?; + // Breadth-first over (row, prefix) so the counterexample is shortest. + let mut seen = BTreeSet::new(); + let mut queue: VecDeque<(Option, Witness)> = VecDeque::new(); + queue.push_back((None, Vec::new())); + while let Some((node, prefix)) = queue.pop_front() { + let row = match node { + None => &m.start, + Some(s) => &m.states[s], + }; + for (a, out) in row.iter().enumerate() { + if let Out::Step(p, t) = out { + let atom = atoms.get(a); + if *p == action && !authorized.eval(atom) { + return Ok(Safety::Unsafe { prefix, atom }); + } + if seen.insert(*t) { + let mut next = prefix.clone(); + next.push((atom, *p)); + queue.push_back((Some(*t), next)); + } + } + } + } + Ok(Safety::Safe) +} diff --git a/crates/gkat-probe/src/expr.rs b/crates/gkat-probe/src/expr.rs new file mode 100644 index 000000000..83a89e8dd --- /dev/null +++ b/crates/gkat-probe/src/expr.rs @@ -0,0 +1,252 @@ +//! The admitted GKAT fragment: Boolean tests, atoms and guarded expressions. +//! +//! Syntax follows Smolka et al., *Guarded Kleene Algebra with Tests* +//! (POPL 2020, arXiv:1907.05920), §2.1: +//! +//! ```text +//! b ::= 0 | 1 | t | ¬b | b ∧ b | b ∨ b (t a primitive test) +//! e ::= 0 | 1 | b | p | e · e | e +_b e | e^(b) (p an uninterpreted action) +//! ``` +//! +//! `e +_b f` is `if b then e else f` and `e^(b)` is `while b do e`. There is +//! no unguarded union and no Kleene star: they are what this fragment leaves +//! out, and constructs that need them are refused one layer up in +//! [`crate::flow`], never encoded here. + +use std::collections::BTreeSet; +use std::fmt; + +/// The largest number of primitive tests a probe may declare. +/// +/// Atoms are explicit truth assignments, so `k` tests give up to `2^k` +/// atoms. Eight tests bound the atom set at 256. The paper's +/// `O(n α(n))` bound (Theorem 5.10) assumes a fixed atom set; equivalence +/// with an unbounded number of tests is co-NP-hard (Proposition 5.11), so +/// the probe refuses rather than enumerate past this bound. +pub const MAX_TESTS: u8 = 8; + +/// An uninterpreted action, identified only by its label. +#[derive(Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)] +pub struct Action(pub &'static str); + +impl fmt::Debug for Action { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + f.write_str(self.0) + } +} + +/// One truth assignment to the declared primitive tests: bit `t` is test `t`. +#[derive(Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Debug)] +pub struct Atom(pub u16); + +impl Atom { + pub fn holds(self, test: u8) -> bool { + self.0 >> test & 1 == 1 + } +} + +/// A Boolean test expression over primitive tests. +#[derive(Clone, PartialEq, Eq, Debug)] +pub enum BExp { + False, + True, + Test(u8), + Not(Box), + And(Box, Box), + Or(Box, Box), +} + +impl BExp { + pub fn eval(&self, atom: Atom) -> bool { + match self { + BExp::False => false, + BExp::True => true, + BExp::Test(t) => atom.holds(*t), + BExp::Not(b) => !b.eval(atom), + BExp::And(a, b) => a.eval(atom) && b.eval(atom), + BExp::Or(a, b) => a.eval(atom) || b.eval(atom), + } + } + + pub fn negated(self) -> BExp { + BExp::Not(Box::new(self)) + } + + pub fn and(self, other: BExp) -> BExp { + BExp::And(Box::new(self), Box::new(other)) + } + + pub fn or(self, other: BExp) -> BExp { + BExp::Or(Box::new(self), Box::new(other)) + } + + fn max_test(&self) -> Option { + match self { + BExp::False | BExp::True => None, + BExp::Test(t) => Some(*t), + BExp::Not(b) => b.max_test(), + BExp::And(a, b) | BExp::Or(a, b) => a.max_test().max(b.max_test()), + } + } +} + +/// A GKAT expression in the admitted fragment. +#[derive(Clone, PartialEq, Eq, Debug)] +pub enum Exp { + /// `0`: reject. + Fail, + /// `1`: accept without acting. + Skip, + /// `b`: accept if the current atom satisfies `b`, else reject. + Assert(BExp), + /// `p`: perform an action. The next atom is chosen by the environment. + Do(Action), + /// `e · f`. + Seq(Box, Box), + /// `e +_b f`, i.e. `if b then e else f`. + If(BExp, Box, Box), + /// `e^(b)`, i.e. `while b do e`. + While(BExp, Box), +} + +impl Exp { + pub fn seq(self, other: Exp) -> Exp { + Exp::Seq(Box::new(self), Box::new(other)) + } + + pub fn if_(b: BExp, then: Exp, otherwise: Exp) -> Exp { + Exp::If(b, Box::new(then), Box::new(otherwise)) + } + + pub fn while_(b: BExp, body: Exp) -> Exp { + Exp::While(b, Box::new(body)) + } + + /// The actions the expression can name. + pub fn actions(&self) -> BTreeSet { + let mut out = BTreeSet::new(); + self.collect_actions(&mut out); + out + } + + fn collect_actions(&self, out: &mut BTreeSet) { + match self { + Exp::Fail | Exp::Skip | Exp::Assert(_) => {} + Exp::Do(p) => { + out.insert(*p); + } + Exp::Seq(a, b) | Exp::If(_, a, b) => { + a.collect_actions(out); + b.collect_actions(out); + } + Exp::While(_, e) => e.collect_actions(out), + } + } + + fn max_test(&self) -> Option { + match self { + Exp::Fail | Exp::Skip | Exp::Do(_) => None, + Exp::Assert(b) => b.max_test(), + Exp::Seq(a, b) => a.max_test().max(b.max_test()), + Exp::If(c, a, b) => c.max_test().max(a.max_test()).max(b.max_test()), + Exp::While(c, e) => c.max_test().max(e.max_test()), + } + } +} + +/// Why the probe refuses an input instead of answering. +#[derive(Clone, PartialEq, Eq, Debug)] +pub enum Refusal { + /// More primitive tests were declared than [`MAX_TESTS`]. + AtomBound { tests: usize, max: u8 }, + /// The declared constraint leaves no atom. + NoAtoms, + /// An expression names a test the atom set does not declare. + UndeclaredTest { test: u8, declared: u8 }, + /// An expression names an action outside the declared alphabet. + UndeclaredAction(Action), + /// Two flows were compared under different declarations. + DeclarationMismatch(&'static str), + /// Unguarded choice between branches: outside GKAT (no `+` in the fragment). + UnguardedChoice, + /// `GoTo` / `GoBack`: unstructured control flow, outside GKAT. + UnstructuredJump(&'static str), + /// A guard used a projection its observable does not declare. + UndeclaredProjection { + observable: &'static str, + projection: &'static str, + }, + /// An observable name that was not declared. + UnknownObservable(&'static str), +} + +/// The declared atom set: every truth assignment to `tests` primitive tests +/// that satisfies `constraint`. +#[derive(Clone, Debug)] +pub struct Atoms { + tests: u8, + list: Vec, +} + +impl Atoms { + /// Enumerates the atoms of `tests` primitive tests under `constraint`. + /// Refuses more than [`MAX_TESTS`] tests and an empty atom set. + pub fn new(tests: usize, constraint: &BExp) -> Result { + if tests > MAX_TESTS as usize { + return Err(Refusal::AtomBound { + tests, + max: MAX_TESTS, + }); + } + if let Some(t) = constraint.max_test() + && t as usize >= tests + { + return Err(Refusal::UndeclaredTest { + test: t, + declared: tests as u8, + }); + } + let list: Vec = (0..1u32 << tests) + .map(|a| Atom(a as u16)) + .filter(|a| constraint.eval(*a)) + .collect(); + if list.is_empty() { + return Err(Refusal::NoAtoms); + } + Ok(Atoms { + tests: tests as u8, + list, + }) + } + + pub fn tests(&self) -> u8 { + self.tests + } + + pub fn len(&self) -> usize { + self.list.len() + } + + pub fn is_empty(&self) -> bool { + self.list.is_empty() + } + + pub fn iter(&self) -> impl Iterator + '_ { + self.list.iter().copied() + } + + pub fn get(&self, index: usize) -> Atom { + self.list[index] + } + + /// Refuses an expression that names a test outside this atom set. + pub fn admit(&self, e: &Exp) -> Result<(), Refusal> { + match e.max_test() { + Some(t) if t >= self.tests => Err(Refusal::UndeclaredTest { + test: t, + declared: self.tests, + }), + _ => Ok(()), + } + } +} diff --git a/crates/gkat-probe/src/flow.rs b/crates/gkat-probe/src/flow.rs new file mode 100644 index 000000000..dbea8f77a --- /dev/null +++ b/crates/gkat-probe/src/flow.rs @@ -0,0 +1,267 @@ +//! A small graph-flow-shaped source language and its lowering to GKAT. +//! +//! The source language is deliberately larger than GKAT: it has the +//! constructs a workflow author can write, including the ones GKAT cannot +//! express. Lowering admits the structured fragment and **refuses** the rest +//! with a typed [`Refusal`]; it never invents a predicate to make an +//! unguarded choice look guarded, and never translates a jump. +//! +//! Correspondence with `graph_flow::NextAction` (rs-graph-llm +//! `graph-flow/src/task.rs`): +//! +//! | `NextAction` | here | +//! |---|---| +//! | `Continue`, `ContinueAndExecute` | sequence (the two differ in scheduling, not in the control-flow language) | +//! | `End` | end of the flow: accept | +//! | `WaitForInput` | [`Step::WaitForInput`]: a guarded loop whose test is observed at resume | +//! | `GoTo(id)` | [`Step::GoTo`]: refused | +//! | `GoBack` | [`Step::GoBack`]: refused | +//! +//! Conditional edges correspond to [`Step::If`]. graph-flow has no edge type +//! that picks a branch without a condition; [`Step::Choice`] models one so the +//! refusal can be tested. +//! +//! ## Guards and projections +//! +//! An observable is declared as Boolean or as three-valued (K3: T, F, U). A +//! K3 observable occupies two primitive tests, `is_t` and `is_u`, and the +//! atom set excludes the assignment where both hold, so it has exactly three +//! values. A K3 observable reaches a Boolean guard only through a declared +//! projection: +//! +//! * [`Cond::Where`]: designated `{T}`, i.e. `is_t`; +//! * [`Cond::Check`]: designated `{T, U}`, i.e. `is_t ∨ is_u`. +//! +//! A Boolean observable is read with [`Cond::Is`]. Using a K3 projection on a +//! Boolean observable, or `Is` on a K3 one, is refused. + +use crate::expr::{Action, Atoms, BExp, Exp, Refusal}; + +/// The kind of an observable. +#[derive(Clone, Copy, PartialEq, Eq, Debug)] +pub enum Kind { + Bool, + K3, +} + +/// A guard condition in the source language. +#[derive(Clone, PartialEq, Eq, Debug)] +pub enum Cond { + /// A Boolean observable is true. + Is(&'static str), + /// WHERE projection of a K3 observable: only `T` passes. + Where(&'static str), + /// CHECK projection of a K3 observable: `T` and `U` pass. + Check(&'static str), + Not(Box), + And(Box, Box), + Or(Box, Box), +} + +impl Cond { + pub fn negated(self) -> Cond { + Cond::Not(Box::new(self)) + } + pub fn and(self, other: Cond) -> Cond { + Cond::And(Box::new(self), Box::new(other)) + } + pub fn or(self, other: Cond) -> Cond { + Cond::Or(Box::new(self), Box::new(other)) + } +} + +/// A step of a source flow. +#[derive(Clone, PartialEq, Eq, Debug)] +pub enum Step { + Skip, + /// Abort the flow: reject. + Abort, + Act(Action), + Seq(Vec), + If(Cond, Box, Box), + While(Cond, Box), + /// Suspend until `ready` holds. Lowers to `while ¬ready do suspend`: the + /// flow performs `suspend`, and `ready` is a test of the external state + /// observed at resume. Snapshot and codebook staleness are not modelled; + /// they are a separate runtime check. + WaitForInput { + ready: Cond, + suspend: Action, + }, + /// Pick a branch without a condition. Outside GKAT: refused. + Choice(Vec), + /// Jump to a named task. Outside GKAT: refused. + GoTo(&'static str), + /// Return to the previous task. Outside GKAT: refused. + GoBack, +} + +impl Step { + pub fn if_(c: Cond, then: Step, otherwise: Step) -> Step { + Step::If(c, Box::new(then), Box::new(otherwise)) + } + pub fn while_(c: Cond, body: Step) -> Step { + Step::While(c, Box::new(body)) + } +} + +/// The declarations a flow is checked under: its observables (which fix the +/// atom set) and its action alphabet. +#[derive(Clone, PartialEq, Eq, Debug)] +pub struct Signature { + pub observables: Vec<(&'static str, Kind)>, + pub actions: Vec, +} + +impl Signature { + /// The primitive test of an observable: `is_t` for K3 (and the only test + /// of a Boolean), plus `is_u` for K3. + fn tests_of(&self, name: &'static str) -> Result<(Kind, u8), Refusal> { + let mut next = 0u8; + for (n, k) in &self.observables { + if *n == name { + return Ok((*k, next)); + } + next += match k { + Kind::Bool => 1, + Kind::K3 => 2, + }; + } + Err(Refusal::UnknownObservable(name)) + } + + /// The number of primitive tests the observables occupy. + pub fn test_count(&self) -> usize { + self.observables + .iter() + .map(|(_, k)| match k { + Kind::Bool => 1, + Kind::K3 => 2, + }) + .sum() + } + + /// The declared atom set. Refuses more than [`crate::expr::MAX_TESTS`] + /// primitive tests. + pub fn atoms(&self) -> Result { + let tests = self.test_count(); + if tests > crate::expr::MAX_TESTS as usize { + return Err(Refusal::AtomBound { + tests, + max: crate::expr::MAX_TESTS, + }); + } + // Each K3 observable excludes the assignment is_t ∧ is_u. + let mut constraint = BExp::True; + let mut next = 0u8; + for (_, k) in &self.observables { + match k { + Kind::Bool => next += 1, + Kind::K3 => { + constraint = + constraint.and(BExp::Test(next).and(BExp::Test(next + 1)).negated()); + next += 2; + } + } + } + Atoms::new(tests, &constraint) + } + + /// Lowers a condition to a Boolean test. + pub fn guard(&self, c: &Cond) -> Result { + Ok(match c { + Cond::Is(n) => match self.tests_of(n)? { + (Kind::Bool, t) => BExp::Test(t), + (Kind::K3, _) => { + return Err(Refusal::UndeclaredProjection { + observable: n, + projection: "Is", + }); + } + }, + Cond::Where(n) => match self.tests_of(n)? { + (Kind::K3, t) => BExp::Test(t), + (Kind::Bool, _) => { + return Err(Refusal::UndeclaredProjection { + observable: n, + projection: "Where", + }); + } + }, + Cond::Check(n) => match self.tests_of(n)? { + (Kind::K3, t) => BExp::Test(t).or(BExp::Test(t + 1)), + (Kind::Bool, _) => { + return Err(Refusal::UndeclaredProjection { + observable: n, + projection: "Check", + }); + } + }, + Cond::Not(a) => self.guard(a)?.negated(), + Cond::And(a, b) => self.guard(a)?.and(self.guard(b)?), + Cond::Or(a, b) => self.guard(a)?.or(self.guard(b)?), + }) + } + + /// Lowers a flow to GKAT, or refuses it. + pub fn lower(&self, s: &Step) -> Result { + Ok(match s { + Step::Skip => Exp::Skip, + Step::Abort => Exp::Fail, + Step::Act(p) => { + if !self.actions.contains(p) { + return Err(Refusal::UndeclaredAction(*p)); + } + Exp::Do(*p) + } + Step::Seq(steps) => { + let mut out = Exp::Skip; + for (i, st) in steps.iter().enumerate() { + let e = self.lower(st)?; + out = if i == 0 { e } else { out.seq(e) }; + } + out + } + Step::If(c, a, b) => Exp::if_(self.guard(c)?, self.lower(a)?, self.lower(b)?), + Step::While(c, body) => Exp::while_(self.guard(c)?, self.lower(body)?), + Step::WaitForInput { ready, suspend } => { + if !self.actions.contains(suspend) { + return Err(Refusal::UndeclaredAction(*suspend)); + } + Exp::while_(self.guard(ready)?.negated(), Exp::Do(*suspend)) + } + Step::Choice(_) => return Err(Refusal::UnguardedChoice), + Step::GoTo(_) => return Err(Refusal::UnstructuredJump("GoTo")), + Step::GoBack => return Err(Refusal::UnstructuredJump("GoBack")), + }) + } +} + +/// A flow under its signature. +#[derive(Clone, Debug)] +pub struct Flow { + pub signature: Signature, + pub body: Step, +} + +impl Flow { + /// Lowers the flow and builds its atom set. + pub fn lower(&self) -> Result<(Exp, Atoms), Refusal> { + let atoms = self.signature.atoms()?; + let e = self.signature.lower(&self.body)?; + atoms.admit(&e)?; + Ok((e, atoms)) + } +} + +/// Decides equivalence of two flows. Refuses flows declared under different +/// signatures: equivalence is only meaningful over the same action alphabet, +/// the same observables and the same projections. +pub fn flows_equivalent(a: &Flow, b: &Flow) -> Result { + if a.signature != b.signature { + return Err(Refusal::DeclarationMismatch("signature")); + } + let (ea, atoms) = a.lower()?; + let (eb, _) = b.lower()?; + crate::automaton::equivalent(&ea, &eb, &atoms) +} diff --git a/crates/gkat-probe/src/lib.rs b/crates/gkat-probe/src/lib.rs new file mode 100644 index 000000000..2a9ceecc7 --- /dev/null +++ b/crates/gkat-probe/src/lib.rs @@ -0,0 +1,49 @@ +//! # D-GKAT-0 — PROBE: bounded GKAT checking of structured Rubicon flows +//! +//! **This is a research fixture, not a verifier.** It is not used by any +//! runtime, has no dependencies, and executes nothing. It answers three +//! questions about small structured flows: +//! +//! 1. **Equivalence** ([`automaton::equivalent`]): do two flows have the same +//! guarded traces? Decided by bisimulation of normalized guarded Thompson +//! automata (Smolka et al., *Guarded Kleene Algebra with Tests*, POPL 2020, +//! arXiv:1907.05920, §§4–5). +//! 2. **Safety** ([`automaton::commit_safe`]): is every `RequestCommit` +//! immediately preceded by an atom with a valid revision and MUL +//! authorization? This is a separate check: a flow equivalent to an unsafe +//! flow is unsafe. +//! 3. **Refusal** ([`flow`]): constructs outside the admitted fragment +//! (unguarded choice, `GoTo`, `GoBack`, more than [`expr::MAX_TESTS`] +//! primitive tests, undeclared projections) are refused with a typed +//! [`expr::Refusal`], never translated. +//! +//! ## Proof boundary +//! +//! * **What the paper proves.** For GKAT expressions over a fixed finite set +//! of atoms, two expressions denote the same guarded strings iff their +//! normalized Thompson automata are bisimilar (§5), and the check runs in +//! `O(n α(n))` for a fixed atom set (Theorem 5.10). With an unbounded +//! number of tests the problem is co-NP-hard (Proposition 5.11). +//! * **What this crate does.** It implements that procedure over an +//! explicitly enumerated atom set of at most 256 atoms. The implementation +//! is **tested, not proven**: every verdict in the test suite is +//! cross-checked against [`oracle`], an independent interpreter that +//! exhaustively explores all runs up to a **stated bound** on the number of +//! actions. That bound makes the oracle a one-directional check (see its +//! module documentation); it is not a completeness argument. +//! * **What is outside.** The paper's relational model interprets actions as +//! uninterpreted state relations. Versions, snapshot and codebook staleness, +//! SQL three-valued logic beyond a declared projection, bag counts, side +//! effects and the Lance write are not modelled. `RequestCommit` is an +//! intent; the write belongs to the supervisor / `cycle_driver`. +//! * **No timings.** Under the workspace rule against millisecond results, +//! the probe reports counts (atoms, states, merged pairs), never times. + +pub mod automaton; +pub mod expr; +pub mod flow; +pub mod oracle; +pub mod rubicon; + +pub use automaton::{Equivalence, Safety, commit_safe, equivalent}; +pub use expr::{Action, Atom, Atoms, BExp, Exp, MAX_TESTS, Refusal}; diff --git a/crates/gkat-probe/src/oracle.rs b/crates/gkat-probe/src/oracle.rs new file mode 100644 index 000000000..6e93be559 --- /dev/null +++ b/crates/gkat-probe/src/oracle.rs @@ -0,0 +1,175 @@ +//! The independent oracle: a direct operational interpreter of [`Exp`], +//! sharing no code with [`crate::automaton`]. +//! +//! It explores every run of an expression in which the environment picks an +//! arbitrary declared atom at the start and after every action, up to a +//! **stated bound** on the number of actions. Within that bound the +//! exploration is exhaustive: every run with at most `max_actions` actions is +//! visited. Runs that would perform more actions are cut and recorded as cut, +//! not as accepted or rejected. +//! +//! **What this oracle can and cannot show.** Equal accepted sets up to `n` +//! actions is necessary for equivalence, not sufficient: two flows may first +//! differ after `n` actions. A difference it finds, though, is a real +//! difference. So the tests use it in one direction only: whenever the +//! automaton says "equivalent", the oracle must agree at every bound tried; +//! whenever the oracle finds a difference, the automaton must say +//! "different". + +use std::collections::{BTreeMap, BTreeSet}; + +use crate::expr::{Action, Atom, Atoms, BExp, Exp}; + +/// Internal steps allowed between two actions before a run counts as +/// diverging. Between actions the atom cannot change, so a run that takes +/// more steps than the expression has nodes without acting is in a loop that +/// never acts; the bound only needs to exceed any terminating stretch. +const FUEL: usize = 1 << 14; + +/// One accepted run: the atoms observed (one more than the actions) and the +/// actions performed. +pub type GuardedString = (Vec, Vec); + +/// Everything the bounded exploration saw. +#[derive(Debug, Default)] +pub struct Exploration { + /// Accepted runs with at most `max_actions` actions. + pub accepted: BTreeSet, + /// Every emitted action with the atom observed immediately before it. + pub emitted: Vec<(Vec, Vec, Atom, Action)>, + /// Runs cut at the action bound. + pub cut: usize, + /// Runs that loop forever without acting. + pub diverged: usize, + /// Runs that reject. + pub rejected: usize, +} + +/// Explores `e` over `atoms` up to `max_actions` actions. +pub fn explore(e: &Exp, atoms: &Atoms, max_actions: usize) -> Exploration { + let mut out = Exploration::default(); + for a in atoms.iter() { + run( + vec![e], + a, + &mut vec![a], + &mut Vec::new(), + atoms, + max_actions, + &mut out, + ); + } + out +} + +fn run( + mut stack: Vec<&Exp>, + atom: Atom, + seen_atoms: &mut Vec, + actions: &mut Vec, + atoms: &Atoms, + max_actions: usize, + out: &mut Exploration, +) { + let mut fuel = FUEL; + loop { + let Some(e) = stack.pop() else { + out.accepted.insert((seen_atoms.clone(), actions.clone())); + return; + }; + if fuel == 0 { + out.diverged += 1; + return; + } + fuel -= 1; + match e { + Exp::Fail => { + out.rejected += 1; + return; + } + Exp::Skip => {} + Exp::Assert(b) => { + if !b.eval(atom) { + out.rejected += 1; + return; + } + } + Exp::Seq(f, g) => { + stack.push(g); + stack.push(f); + } + Exp::If(b, f, g) => stack.push(if b.eval(atom) { f } else { g }), + Exp::While(b, body) => { + if b.eval(atom) { + stack.push(e); + stack.push(body); + } + } + Exp::Do(p) => { + if actions.len() == max_actions { + out.cut += 1; + return; + } + out.emitted + .push((seen_atoms.clone(), actions.clone(), atom, *p)); + actions.push(*p); + for next in atoms.iter() { + seen_atoms.push(next); + run( + stack.clone(), + next, + seen_atoms, + actions, + atoms, + max_actions, + out, + ); + seen_atoms.pop(); + } + actions.pop(); + return; + } + } + } +} + +/// Whether the oracle sees the same accepted runs for both expressions. +pub fn same_up_to(e: &Exp, f: &Exp, atoms: &Atoms, max_actions: usize) -> bool { + explore(e, atoms, max_actions).accepted == explore(f, atoms, max_actions).accepted +} + +/// Whether some emitted `action` within the bound follows an atom that does +/// not satisfy `authorized`. +pub fn unsafe_within( + e: &Exp, + atoms: &Atoms, + max_actions: usize, + action: Action, + authorized: &BExp, +) -> bool { + explore(e, atoms, max_actions) + .emitted + .iter() + .any(|(_, _, atom, p)| *p == action && !authorized.eval(*atom)) +} + +/// The GKAT determinacy property (paper §2.2) of a set of guarded strings: +/// two strings that observe the same atoms up to a position must have taken +/// the same actions up to that position. +pub fn deterministic(strings: &BTreeSet) -> bool { + // Map each observed atom prefix to the action taken after it. + let mut next: BTreeMap, Action> = BTreeMap::new(); + for (atoms, actions) in strings { + for (i, action) in actions.iter().enumerate() { + let key = atoms[..=i].to_vec(); + match next.get(&key) { + Some(seen) if seen != action => return false, + Some(_) => {} + None => { + next.insert(key, *action); + } + } + } + } + true +} diff --git a/crates/gkat-probe/src/rubicon.rs b/crates/gkat-probe/src/rubicon.rs new file mode 100644 index 000000000..63df8d974 --- /dev/null +++ b/crates/gkat-probe/src/rubicon.rs @@ -0,0 +1,233 @@ +//! The Rubicon reference flow, an optimized variant, and the mutants the +//! disable runs use. +//! +//! The flow, in words: +//! +//! 1. If deliberation is needed, deliberate. +//! 2. Wait for external input (suspend until it is ready). +//! 3. Decide, on the atom observed at that moment: +//! * revision valid **and** MUL authorization granted (both WHERE, `{T}`) +//! → `RequestCommit`; +//! * revision invalid (`F`) → `Prune`; +//! * revision valid, authorization refused (`F`) → `Plan`; +//! * otherwise (an `U` on either side) → `Hold`. +//! +//! `RequestCommit` is an intent. The probe never writes anything; the actual +//! Lance write belongs to the supervisor / `cycle_driver`, which this crate +//! does not touch. The Kanban terminals `Commit | Plan | Prune` of +//! `kanban.rs` `next_phases(Evaluation)` correspond to `RequestCommit`, +//! `Plan` and `Prune`; `Hold` corresponds to a phase stay +//! (`GateDecision::Hold` → `advance_on_gate` returns `None`). This crate +//! does not depend on `kanban.rs` and owns no progression. + +use crate::expr::{Action, BExp, Refusal}; +use crate::flow::{Cond, Flow, Kind, Signature, Step}; + +pub const DELIBERATE: Action = Action("Deliberate"); +pub const SUSPEND: Action = Action("Suspend"); +pub const REQUEST_COMMIT: Action = Action("RequestCommit"); +pub const HOLD: Action = Action("Hold"); +pub const PLAN: Action = Action("Plan"); +pub const PRUNE: Action = Action("Prune"); + +/// Revision validity, three-valued. +pub const REV: &str = "rev"; +/// MUL authorization, three-valued. +pub const MUL: &str = "mul"; +/// Whether deliberation is needed. +pub const DELIBERATE_NEEDED: &str = "deliberate"; +/// Whether external input is ready at resume. +pub const INPUT_READY: &str = "input"; + +/// 6 primitive tests: rev (2), mul (2), deliberate (1), input (1); 36 atoms. +pub fn signature() -> Signature { + Signature { + observables: vec![ + (REV, Kind::K3), + (MUL, Kind::K3), + (DELIBERATE_NEEDED, Kind::Bool), + (INPUT_READY, Kind::Bool), + ], + actions: vec![DELIBERATE, SUSPEND, REQUEST_COMMIT, HOLD, PLAN, PRUNE], + } +} + +/// The authorization the safety check requires immediately before +/// `RequestCommit`: WHERE(rev) ∧ WHERE(mul). It is fixed by the checker, not +/// taken from the flow, so a flow that authorizes with CHECK fails. +pub fn authorized() -> Result { + signature().guard(&Cond::Where(REV).and(Cond::Where(MUL))) +} + +fn act(p: Action) -> Step { + Step::Act(p) +} + +fn wait() -> Step { + Step::WaitForInput { + ready: Cond::Is(INPUT_READY), + suspend: SUSPEND, + } +} + +/// The reference decision. +pub fn decide_reference() -> Step { + Step::if_( + Cond::Where(REV).and(Cond::Where(MUL)), + act(REQUEST_COMMIT), + Step::if_( + Cond::Check(REV).negated(), + act(PRUNE), + Step::if_( + Cond::Where(REV).and(Cond::Check(MUL).negated()), + act(PLAN), + act(HOLD), + ), + ), + ) +} + +/// The reference flow: the decision tail is written out in both branches of +/// the deliberation choice. +pub fn reference() -> Flow { + Flow { + signature: signature(), + body: Step::if_( + Cond::Is(DELIBERATE_NEEDED), + Step::Seq(vec![act(DELIBERATE), wait(), decide_reference()]), + Step::Seq(vec![wait(), decide_reference()]), + ), + } +} + +/// The optimized decision: tests the revision first and nests the +/// authorization inside it. +pub fn decide_optimized(mul_branch: Step) -> Step { + Step::if_( + Cond::Check(REV).negated(), + act(PRUNE), + Step::if_(Cond::Where(REV), mul_branch, act(HOLD)), + ) +} + +/// The optimized decision's authorization branch. +pub fn mul_branch() -> Step { + Step::if_( + Cond::Where(MUL), + act(REQUEST_COMMIT), + Step::if_(Cond::Check(MUL), act(HOLD), act(PLAN)), + ) +} + +/// The optimized flow: the shared tail is factored out of the deliberation +/// choice (G1) and the decision is reordered. +pub fn optimized() -> Flow { + optimized_with(decide_optimized(mul_branch())) +} + +fn optimized_with(decide: Step) -> Flow { + Flow { + signature: signature(), + body: Step::Seq(vec![ + Step::if_(Cond::Is(DELIBERATE_NEEDED), act(DELIBERATE), Step::Skip), + wait(), + decide, + ]), + } +} + +/// Disable 1: the authorization guard's polarity is reversed. +pub fn mutant_reversed_polarity() -> Flow { + optimized_with(decide_optimized(Step::if_( + Cond::Where(MUL).negated(), + act(REQUEST_COMMIT), + Step::if_(Cond::Check(MUL), act(HOLD), act(PLAN)), + ))) +} + +/// Disable 2: `RequestCommit` is moved ahead of its authorization guard. +pub fn mutant_commit_before_guard() -> Flow { + optimized_with(decide_optimized(Step::Seq(vec![ + act(REQUEST_COMMIT), + Step::if_( + Cond::Where(MUL), + Step::Skip, + Step::if_(Cond::Check(MUL), act(HOLD), act(PLAN)), + ), + ]))) +} + +/// Disable 2b: authorization is observed, then `Deliberate` runs, then +/// `RequestCommit`. The authorization was observed before an action and is +/// stale when the intent is emitted. +pub fn mutant_stale_authorization() -> Flow { + Flow { + signature: signature(), + body: Step::Seq(vec![ + wait(), + Step::if_( + Cond::Where(REV).and(Cond::Where(MUL)), + Step::Seq(vec![act(DELIBERATE), act(REQUEST_COMMIT)]), + Step::if_(Cond::Check(REV).negated(), act(PRUNE), act(HOLD)), + ), + ]), + } +} + +/// Disable 3: unguarded nondeterminism between committing and holding. +pub fn mutant_unguarded_choice() -> Flow { + optimized_with(decide_optimized(Step::Choice(vec![ + act(REQUEST_COMMIT), + act(HOLD), + ]))) +} + +/// Commit authorization with CHECK projections instead of WHERE: an `U` +/// revision or authorization would authorize. +pub fn reference_with_check_auth() -> Flow { + Flow { + signature: signature(), + body: Step::Seq(vec![ + wait(), + Step::if_( + Cond::Check(REV).and(Cond::Check(MUL)), + act(REQUEST_COMMIT), + Step::if_(Cond::Check(REV).negated(), act(PRUNE), act(PLAN)), + ), + ]), + } +} + +/// An optimized form of [`reference_with_check_auth`]: equivalent to it, and +/// just as unsafe. +pub fn optimized_with_check_auth() -> Flow { + Flow { + signature: signature(), + body: Step::Seq(vec![ + wait(), + Step::if_( + Cond::Check(REV).negated(), + act(PRUNE), + Step::if_(Cond::Check(MUL), act(REQUEST_COMMIT), act(PLAN)), + ), + ]), + } +} + +/// The flow with a `GoTo` retry instead of a structured loop. +pub fn mutant_goto() -> Flow { + optimized_with(Step::if_( + Cond::Check(REV).negated(), + Step::GoTo("planning"), + decide_optimized(mul_branch()), + )) +} + +/// The flow with a `GoBack` instead of a structured loop. +pub fn mutant_goback() -> Flow { + optimized_with(Step::if_( + Cond::Is(INPUT_READY).negated(), + Step::GoBack, + decide_optimized(mul_branch()), + )) +} diff --git a/crates/gkat-probe/tests/differential.rs b/crates/gkat-probe/tests/differential.rs new file mode 100644 index 000000000..b67fad15d --- /dev/null +++ b/crates/gkat-probe/tests/differential.rs @@ -0,0 +1,138 @@ +//! Differential check of the automaton against the independent oracle over +//! random expressions and single-point mutations of them. +//! +//! The direction of each assertion follows what a bounded oracle can show: +//! automaton-equivalent ⇒ oracle-equal at every bound; oracle-different ⇒ +//! automaton-different. The count of automaton-different pairs the oracle +//! also separates is asserted non-trivial so the check cannot pass vacuously. + +use gkat_probe::oracle::same_up_to; +use gkat_probe::{Action, Atoms, BExp, Exp, equivalent}; + +struct Rng(u64); + +impl Rng { + fn next(&mut self) -> u64 { + self.0 ^= self.0 << 13; + self.0 ^= self.0 >> 7; + self.0 ^= self.0 << 17; + self.0 + } + fn below(&mut self, n: u64) -> u64 { + self.next() % n + } +} + +const ACTIONS: [Action; 2] = [Action("p"), Action("q")]; + +fn bexp(r: &mut Rng, depth: u32) -> BExp { + match if depth == 0 { r.below(3) } else { r.below(6) } { + 0 => BExp::Test(0), + 1 => BExp::Test(1), + 2 => [BExp::True, BExp::False][r.below(2) as usize].clone(), + 3 => bexp(r, depth - 1).negated(), + 4 => bexp(r, depth - 1).and(bexp(r, depth - 1)), + _ => bexp(r, depth - 1).or(bexp(r, depth - 1)), + } +} + +fn exp(r: &mut Rng, depth: u32) -> Exp { + match if depth == 0 { r.below(4) } else { r.below(7) } { + 0 => Exp::Skip, + 1 => Exp::Fail, + 2 => Exp::Assert(bexp(r, 1)), + 3 => Exp::Do(ACTIONS[r.below(2) as usize]), + 4 => exp(r, depth - 1).seq(exp(r, depth - 1)), + 5 => Exp::if_(bexp(r, 1), exp(r, depth - 1), exp(r, depth - 1)), + _ => Exp::while_(bexp(r, 1), exp(r, depth - 1)), + } +} + +/// One random local change: flip an action label, negate a guard, or swap +/// the branches of a conditional. +fn mutate(e: &Exp, r: &mut Rng) -> Exp { + match e { + Exp::Do(p) if r.below(2) == 0 => Exp::Do(if *p == ACTIONS[0] { + ACTIONS[1] + } else { + ACTIONS[0] + }), + Exp::If(b, x, y) => match r.below(3) { + 0 => Exp::If(b.clone().negated(), x.clone(), y.clone()), + 1 => Exp::If(b.clone(), Box::new(mutate(x, r)), y.clone()), + _ => Exp::If(b.clone(), x.clone(), Box::new(mutate(y, r))), + }, + Exp::Seq(x, y) => { + if r.below(2) == 0 { + Exp::Seq(Box::new(mutate(x, r)), y.clone()) + } else { + Exp::Seq(x.clone(), Box::new(mutate(y, r))) + } + } + Exp::While(b, x) => { + if r.below(2) == 0 { + Exp::While(b.clone().negated(), x.clone()) + } else { + Exp::While(b.clone(), Box::new(mutate(x, r))) + } + } + other => other.clone(), + } +} + +#[test] +fn automaton_and_oracle_agree_on_random_pairs() { + let atoms = Atoms::new(2, &BExp::True).unwrap(); + let mut r = Rng(0x9E37_79B9_7F4A_7C15); + let (mut equal, mut separated, mut different) = (0, 0, 0); + for _ in 0..600 { + let e = exp(&mut r, 3); + let f = if r.below(2) == 0 { + mutate(&e, &mut r) + } else { + exp(&mut r, 3) + }; + let v = equivalent(&e, &f, &atoms).unwrap().holds(); + let oracle = same_up_to(&e, &f, &atoms, 3); + if v { + equal += 1; + assert!( + oracle, + "automaton equivalent, oracle differs:\n{e:?}\n{f:?}" + ); + for n in 0..=4 { + assert!(same_up_to(&e, &f, &atoms, n), "bound {n}:\n{e:?}\n{f:?}"); + } + } else { + different += 1; + if !oracle { + separated += 1; + } + } + // Reflexivity: every expression is equivalent to itself. + assert!(equivalent(&e, &e, &atoms).unwrap().holds()); + } + eprintln!("equivalent {equal}, different {different}, oracle-separated {separated}"); + // Anti-vacuity: both verdicts occur, and the oracle confirms most + // differences within its bound. + assert!(equal > 50, "{equal}"); + assert!(different > 50, "{different}"); + assert!(separated * 10 >= different * 8, "{separated}/{different}"); +} + +/// Oracle-different ⇒ automaton-different, checked from the oracle's side. +#[test] +fn every_oracle_difference_is_an_automaton_difference() { + let atoms = Atoms::new(2, &BExp::True).unwrap(); + let mut r = Rng(0xD1B5_4A32_D192_ED03); + for _ in 0..600 { + let e = exp(&mut r, 3); + let f = mutate(&e, &mut r); + if !same_up_to(&e, &f, &atoms, 3) { + assert!( + !equivalent(&e, &f, &atoms).unwrap().holds(), + "\n{e:?}\n{f:?}" + ); + } + } +} diff --git a/crates/gkat-probe/tests/g1_factoring.rs b/crates/gkat-probe/tests/g1_factoring.rs new file mode 100644 index 000000000..db042dd26 --- /dev/null +++ b/crates/gkat-probe/tests/g1_factoring.rs @@ -0,0 +1,58 @@ +//! G1: guarded factoring (paper §2.3, Example 2.5). +//! +//! `if b then {p; q} else {q} ≡ (if b then {p} else {skip}); q` + +use gkat_probe::oracle::same_up_to; +use gkat_probe::{Action, Atoms, BExp, Exp, equivalent}; + +const P: Action = Action("p"); +const Q: Action = Action("q"); +const R: Action = Action("r"); + +fn b() -> BExp { + BExp::Test(0) +} + +fn atoms() -> Atoms { + Atoms::new(1, &BExp::True).unwrap() +} + +fn lhs() -> Exp { + Exp::if_(b(), Exp::Do(P).seq(Exp::Do(Q)), Exp::Do(Q)) +} + +fn rhs(trailing: Action, guard: BExp) -> Exp { + Exp::if_(guard, Exp::Do(P), Exp::Skip).seq(Exp::Do(trailing)) +} + +#[test] +fn factoring_is_equivalent_and_the_oracle_agrees() { + let v = equivalent(&lhs(), &rhs(Q, b()), &atoms()).unwrap(); + assert!(v.holds(), "{v:?}"); + for n in 0..=4 { + assert!(same_up_to(&lhs(), &rhs(Q, b()), &atoms(), n), "bound {n}"); + } +} + +#[test] +fn a_changed_action_label_is_rejected() { + let v = equivalent(&lhs(), &rhs(R, b()), &atoms()).unwrap(); + assert!(!v.holds()); + assert!(!same_up_to(&lhs(), &rhs(R, b()), &atoms(), 2)); +} + +#[test] +fn a_reversed_guard_is_rejected() { + let v = equivalent(&lhs(), &rhs(Q, b().negated()), &atoms()).unwrap(); + assert!(!v.holds()); + assert!(!same_up_to(&lhs(), &rhs(Q, b().negated()), &atoms(), 2)); +} + +/// The factoring needs the same trailing action in both branches; with +/// different trailing actions the two sides are not equivalent. +#[test] +fn factoring_different_tails_is_rejected() { + let lhs = Exp::if_(b(), Exp::Do(P).seq(Exp::Do(Q)), Exp::Do(R)); + let v = equivalent(&lhs, &rhs(Q, b()), &atoms()).unwrap(); + assert!(!v.holds()); +} diff --git a/crates/gkat-probe/tests/g2_nondeterminism.rs b/crates/gkat-probe/tests/g2_nondeterminism.rs new file mode 100644 index 000000000..b176beb47 --- /dev/null +++ b/crates/gkat-probe/tests/g2_nondeterminism.rs @@ -0,0 +1,51 @@ +//! G2: genuine nondeterminism is refused, never encoded as a guarded choice. + +use std::collections::BTreeSet; + +use gkat_probe::oracle::{deterministic, explore}; +use gkat_probe::rubicon; +use gkat_probe::{Action, Atoms, BExp, Exp, Refusal}; + +#[test] +fn unguarded_choice_is_refused() { + assert_eq!( + rubicon::mutant_unguarded_choice().lower().unwrap_err(), + Refusal::UnguardedChoice + ); +} + +#[test] +fn goto_and_goback_are_refused() { + assert_eq!( + rubicon::mutant_goto().lower().unwrap_err(), + Refusal::UnstructuredJump("GoTo") + ); + assert_eq!( + rubicon::mutant_goback().lower().unwrap_err(), + Refusal::UnstructuredJump("GoBack") + ); +} + +/// The union "do p or do q, whatever the atom" violates the determinacy +/// property, so no GKAT expression denotes it. Encoding it as `if c then p +/// else q` under an invented test `c` changes the language: it adds a test +/// the flow never declared. +#[test] +fn a_union_of_two_actions_is_not_deterministic() { + let atoms = Atoms::new(1, &BExp::True).unwrap(); + let p = explore(&Exp::Do(Action("p")), &atoms, 1).accepted; + let q = explore(&Exp::Do(Action("q")), &atoms, 1).accepted; + let union: BTreeSet<_> = p.union(&q).cloned().collect(); + assert!(deterministic(&p) && deterministic(&q)); + assert!(!deterministic(&union)); +} + +/// Every lowered Rubicon fixture is deterministic (can-stay-silent half of the +/// check above). +#[test] +fn admitted_flows_are_deterministic() { + for flow in [rubicon::reference(), rubicon::optimized()] { + let (e, atoms) = flow.lower().unwrap(); + assert!(deterministic(&explore(&e, &atoms, 2).accepted)); + } +} diff --git a/crates/gkat-probe/tests/g5_atoms.rs b/crates/gkat-probe/tests/g5_atoms.rs new file mode 100644 index 000000000..cf84d49e5 --- /dev/null +++ b/crates/gkat-probe/tests/g5_atoms.rs @@ -0,0 +1,93 @@ +//! G5: the atom set is explicitly bounded and declared. + +use gkat_probe::automaton::thompson; +use gkat_probe::flow::{Kind, Signature}; +use gkat_probe::{Action, Atoms, BExp, Exp, MAX_TESTS, Refusal, equivalent}; + +#[test] +fn atom_counts_are_exact() { + for k in 0..=MAX_TESTS as usize { + assert_eq!(Atoms::new(k, &BExp::True).unwrap().len(), 1 << k); + } + // A K3 observable occupies two tests and has three values. + let sig = |n: usize| Signature { + observables: (0..n).map(|_| ("x", Kind::K3)).collect(), + actions: vec![], + }; + for n in 0..=4 { + assert_eq!(sig(n).atoms().unwrap().len(), 3usize.pow(n as u32)); + } +} + +#[test] +fn more_tests_than_the_bound_are_refused() { + let k = MAX_TESTS as usize + 1; + assert_eq!( + Atoms::new(k, &BExp::True).unwrap_err(), + Refusal::AtomBound { + tests: k, + max: MAX_TESTS + } + ); + // A DR64 register is not 64 GKAT tests: declaring 64 Boolean + // observables is refused, not enumerated. + let dr64 = Signature { + observables: (0..64).map(|_| ("lane", Kind::Bool)).collect(), + actions: vec![], + }; + assert_eq!( + dr64.atoms().unwrap_err(), + Refusal::AtomBound { + tests: 64, + max: MAX_TESTS + } + ); + // Five K3 observables need ten tests. + let k3 = Signature { + observables: (0..5).map(|_| ("x", Kind::K3)).collect(), + actions: vec![], + }; + assert_eq!( + k3.atoms().unwrap_err(), + Refusal::AtomBound { + tests: 10, + max: MAX_TESTS + } + ); +} + +#[test] +fn an_undeclared_test_is_refused() { + let atoms = Atoms::new(2, &BExp::True).unwrap(); + let e = Exp::Assert(BExp::Test(5)); + assert_eq!( + equivalent(&e, &e, &atoms).unwrap_err(), + Refusal::UndeclaredTest { + test: 5, + declared: 2 + } + ); +} + +/// A chain of `k` independent guards: automaton states grow with the +/// expression (one state per action), the atom set grows as `2^k`. The +/// counts are what G5 measures; no timing is reported. +#[test] +fn states_grow_with_the_expression_atoms_with_the_tests() { + let mut rows = Vec::new(); + for k in 1..=MAX_TESTS { + let atoms = Atoms::new(k as usize, &BExp::True).unwrap(); + let chain = (0..k) + .map(|t| Exp::if_(BExp::Test(t), Exp::Do(Action("p")), Exp::Do(Action("q")))) + .reduce(Exp::seq) + .unwrap(); + let states = thompson(&chain, &atoms).unwrap().states.len(); + let pairs = match equivalent(&chain, &chain.clone(), &atoms).unwrap() { + gkat_probe::Equivalence::Equivalent { pairs } => pairs, + other => panic!("{other:?}"), + }; + rows.push((k, atoms.len(), states, pairs)); + assert_eq!(states, 2 * k as usize); + } + eprintln!("tests atoms states merged-pairs: {rows:?}"); +} diff --git a/crates/gkat-probe/tests/rubicon.rs b/crates/gkat-probe/tests/rubicon.rs new file mode 100644 index 000000000..7b0999456 --- /dev/null +++ b/crates/gkat-probe/tests/rubicon.rs @@ -0,0 +1,149 @@ +//! The Rubicon fixture: equivalence and safety are separate checks, and each +//! disable run fails the check it names. + +use gkat_probe::flow::flows_equivalent; +use gkat_probe::oracle::{same_up_to, unsafe_within}; +use gkat_probe::rubicon::{self, REQUEST_COMMIT}; +use gkat_probe::{Refusal, commit_safe}; + +/// Oracle bound: two actions covers Deliberate or one Suspend, followed by +/// the decision. With 36 atoms that is 36^3 runs per flow. +const BOUND: usize = 2; + +fn safe(flow: &gkat_probe::flow::Flow) -> bool { + let (e, atoms) = flow.lower().unwrap(); + let auth = rubicon::authorized().unwrap(); + let automaton = commit_safe(&e, &atoms, REQUEST_COMMIT, &auth) + .unwrap() + .holds(); + let oracle_unsafe = unsafe_within(&e, &atoms, BOUND, REQUEST_COMMIT, &auth); + // The oracle only sees runs up to the bound: an oracle violation must be + // a real one, so it can never coexist with an automaton "safe". + assert!( + !(automaton && oracle_unsafe), + "oracle found a violation the automaton missed" + ); + automaton +} + +fn equivalent(a: &gkat_probe::flow::Flow, b: &gkat_probe::flow::Flow) -> bool { + let verdict = flows_equivalent(a, b).unwrap().holds(); + let (ea, atoms) = a.lower().unwrap(); + let (eb, _) = b.lower().unwrap(); + let oracle_same = same_up_to(&ea, &eb, &atoms, BOUND); + // Equivalent ⇒ equal up to every bound; a bounded difference ⇒ different. + if verdict { + assert!( + oracle_same, + "automaton equivalent, oracle found a difference" + ); + } + verdict +} + +#[test] +fn the_signature_declares_36_atoms() { + assert_eq!(rubicon::signature().atoms().unwrap().len(), 36); +} + +#[test] +fn reference_and_optimized_are_equivalent_and_both_safe() { + assert!(equivalent(&rubicon::reference(), &rubicon::optimized())); + assert!(safe(&rubicon::reference())); + assert!(safe(&rubicon::optimized())); +} + +#[test] +fn disable_1_reversed_polarity_fails_equivalence() { + assert!(!equivalent( + &rubicon::reference(), + &rubicon::mutant_reversed_polarity() + )); +} + +#[test] +fn disable_2_commit_before_guard_fails_equivalence_and_safety() { + let m = rubicon::mutant_commit_before_guard(); + assert!(!equivalent(&rubicon::reference(), &m)); + assert!(!safe(&m)); +} + +#[test] +fn disable_2b_stale_authorization_fails_safety() { + assert!(!safe(&rubicon::mutant_stale_authorization())); +} + +#[test] +fn disable_3_unguarded_choice_is_refused() { + let m = rubicon::mutant_unguarded_choice(); + assert_eq!(m.lower().unwrap_err(), Refusal::UnguardedChoice); + assert_eq!( + flows_equivalent(&rubicon::reference(), &m).unwrap_err(), + Refusal::UnguardedChoice + ); +} + +/// Commit authorization must never inherit CHECK semantics. +#[test] +fn check_projection_for_commit_is_unsafe() { + assert!(!safe(&rubicon::reference_with_check_auth())); +} + +/// Equivalence does not establish safety: a flow equivalent to an unsafe +/// reference is unsafe. +#[test] +fn equivalent_to_an_unsafe_reference_is_still_unsafe() { + let r = rubicon::reference_with_check_auth(); + let o = rubicon::optimized_with_check_auth(); + assert!(equivalent(&r, &o)); + assert!(!safe(&o)); +} + +/// The safety counterexample is a concrete atom on which an `U` revision or +/// authorization reaches `RequestCommit`. +#[test] +fn the_check_counterexample_has_an_unknown() { + let (e, atoms) = rubicon::reference_with_check_auth().lower().unwrap(); + let auth = rubicon::authorized().unwrap(); + match commit_safe(&e, &atoms, REQUEST_COMMIT, &auth).unwrap() { + gkat_probe::Safety::Unsafe { atom, .. } => { + // rev is tests 0 (is_t) and 1 (is_u); mul is tests 2 and 3. + assert!(atom.holds(1) || atom.holds(3), "{atom:?}"); + } + gkat_probe::Safety::Safe => panic!("expected unsafe"), + } +} + +#[test] +fn flows_under_different_signatures_are_refused() { + let mut other = rubicon::optimized(); + other.signature.actions.pop(); + assert_eq!( + flows_equivalent(&rubicon::reference(), &other).unwrap_err(), + Refusal::DeclarationMismatch("signature") + ); +} + +#[test] +fn undeclared_projections_are_refused() { + use gkat_probe::flow::Cond; + let sig = rubicon::signature(); + assert!(matches!( + sig.guard(&Cond::Is(rubicon::REV)), + Err(Refusal::UndeclaredProjection { + projection: "Is", + .. + }) + )); + assert!(matches!( + sig.guard(&Cond::Where(rubicon::INPUT_READY)), + Err(Refusal::UndeclaredProjection { + projection: "Where", + .. + }) + )); + assert!(matches!( + sig.guard(&Cond::Is("nope")), + Err(Refusal::UnknownObservable("nope")) + )); +} From dd60f14aa79e55cbeff140b0592155cad4dfcdbd Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 21 Oct 2026 19:48:29 +0000 Subject: [PATCH 2/4] gkat-probe: pin dead-state normalization MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The first disable run of normalization stayed green: no test compared an action into a dead state with a rejection. p·0 ≡ 0 now does. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01VncKoyG6JkpsoqhqTGTv3f --- crates/gkat-probe/tests/g1_factoring.rs | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/crates/gkat-probe/tests/g1_factoring.rs b/crates/gkat-probe/tests/g1_factoring.rs index db042dd26..8c3e96712 100644 --- a/crates/gkat-probe/tests/g1_factoring.rs +++ b/crates/gkat-probe/tests/g1_factoring.rs @@ -56,3 +56,16 @@ fn factoring_different_tails_is_rejected() { let v = equivalent(&lhs, &rhs(Q, b()), &atoms()).unwrap(); assert!(!v.holds()); } + +/// Normalization (paper §5.2): an action into a state that can never accept +/// is a rejection. `p · 0` and `0` both have no guarded strings, and so do +/// `if b then (p · 0) else q` and `if b then 0 else q`'s `b` branch. +#[test] +fn a_step_into_a_dead_state_is_a_rejection() { + let dead = Exp::Do(P).seq(Exp::Fail); + assert!(equivalent(&dead, &Exp::Fail, &atoms()).unwrap().holds()); + let l = Exp::if_(b(), dead, Exp::Do(Q)); + let r = Exp::if_(b(), Exp::Fail, Exp::Do(Q)); + assert!(equivalent(&l, &r, &atoms()).unwrap().holds()); + assert!(same_up_to(&l, &r, &atoms(), 3)); +} From 650e129d91a6fc227ef061b2a91329dfe4509ea2 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 21 Oct 2026 19:50:08 +0000 Subject: [PATCH 3/4] board: D-GKAT-0 probe entry, STATUS_BOARD row, regenerated indexes Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01VncKoyG6JkpsoqhqTGTv3f --- .claude/board/STATUS_BOARD.md | 2 +- .claude/board/SUPERSESSION-INDEX.md | 2 +- .../entries/2026-10-21-d-gkat-0-probe.md | 105 ++++++++++++++++++ .claude/board/entries/README.md | 3 +- 4 files changed, 109 insertions(+), 3 deletions(-) create mode 100644 .claude/board/entries/2026-10-21-d-gkat-0-probe.md diff --git a/.claude/board/STATUS_BOARD.md b/.claude/board/STATUS_BOARD.md index 2030b77e1..e42fb63c5 100644 --- a/.claude/board/STATUS_BOARD.md +++ b/.claude/board/STATUS_BOARD.md @@ -8,7 +8,7 @@ Plans in #1667 (`d-rft-relalg-thought-git-frontier-v1.md`, `d-qsp-classview-quac | **D-QSP-0 remainder, slice 1** | scalar aggregates under SQL NULL: empty / all-NULL `SUM` is NULL, `COUNT(x)` vs `COUNT(*)`, MIN/MAX/AVG | In PR (EXO-50 claim `session_013z2e1YXkm6o6HNrDn5BPWA/026`; `entries/2026-10-21-d-qsp-0-scalar-aggregates-null.md`): Quack `lower_sum` + `sum_finish` over existing terminals. MEASURED: PostgreSQL 16.15 = Quack = Kleene oracle on 3600/3600 queries | `tests/sql_aggregate_null.rs` (4 disables red); `examples/qsp_agg_pg_parity.rs` (SKIP without a server) | | **D-RFT-1..5, D-LFA-0** | composition, substitution, recursion, frontier, replay; flow census | PROPOSAL (`entries/2026-10-21-d-rft-d-lfa-0-assessment.md`) | per-row falsifiers in the entry; unclaimed | | **D-LFA-1 / D-LFA-2** (amended 2026-10-21) | guarded-control verification of a Rubicon flow; integration with the existing drivers | PROPOSAL (plan amendment, `d-lfa-…-v1.md` § Amendment 2026-10-21; map `entries/2026-10-21-coresearch-plans-mapping-foresight.md`) | GKAT equivalence + separate no-commit-without-revision-and-MUL trace check; 3 disables; `GoTo`/`GoBack` refused; unclaimed | -| **D-GKAT-0** | GKAT fixture probe: G1 factoring, G2 nondeterminism refusal, G5 declared atom bound | Queued, unclaimed (research only; no runtime, dependency or executor) | the three fixtures in the D-LFA plan amendment | +| **D-GKAT-0** | GKAT fixture probe: G1 factoring, G2 nondeterminism refusal, G5 declared atom bound | In PR, PROBE (EXO-50 claim `session_01VncKoyG6JkpsoqhqTGTv3f/026`; `crates/gkat-probe`; `entries/2026-10-21-d-gkat-0-probe.md`). TEST-PINNED: Rubicon reference ≡ optimized, both safe; CHECK-authorized flows equivalent and unsafe; ≤ 8 tests (256 atoms) else refused | 3 flow disables + 11 checker disables red; independent bounded oracle; not a production verifier | ## D-RU — D-RELALG-UNIFIED: JC/R statistics and Datalog sharing work through the contract set IR (2026-10-20) diff --git a/.claude/board/SUPERSESSION-INDEX.md b/.claude/board/SUPERSESSION-INDEX.md index b21e9fbba..718aef7e7 100644 --- a/.claude/board/SUPERSESSION-INDEX.md +++ b/.claude/board/SUPERSESSION-INDEX.md @@ -56,7 +56,7 @@ coverage instead. | `persist_cycle` | BLOCKED | — | 12 | 8 | 5 | | `CognitiveMarkers` | REPURPOSE | `Commit` | 1 | 0 | 0 | | `DominoCascade` | REPURPOSE | `Commit` | 7 | 1 | 0 | -| `GateDecision` | REPURPOSE | — | 26 | 30 | 26 | +| `GateDecision` | REPURPOSE | — | 27 | 30 | 26 | | `GateState` | REPURPOSE | — | 14 | 1 | 1 | | `MergeMode` | REPURPOSE | — | 8 | 14 | 13 | | `ResonanceDto` | REPURPOSE | `PerturbationDto` | 2 | 12 | 7 | diff --git a/.claude/board/entries/2026-10-21-d-gkat-0-probe.md b/.claude/board/entries/2026-10-21-d-gkat-0-probe.md new file mode 100644 index 000000000..87edc3a0b --- /dev/null +++ b/.claude/board/entries/2026-10-21-d-gkat-0-probe.md @@ -0,0 +1,105 @@ +# 2026-10-21 — D-GKAT-0: PROBE, bounded GKAT checking of structured Rubicon flows + +**Status:** PROBE (lab, `crates/gkat-probe`). This is a research fixture, not a production verifier. Everything here is TEST-PINNED; nothing is proven beyond what the cited paper proves. +**Claim:** EXO-50 `session_01VncKoyG6JkpsoqhqTGTv3f/026`, ACKed in `session_01G22yT6htkcdyXsihxxXdrg/036`. +**Plan:** `.claude/plans/d-lfa-lance-graph-flow-rubicon-assimilation-v1.md` § Amendment 2026-10-21 (#1673). +**Source:** `.arxiv/1907.05920_guarded_kleene_algebra_verified_control_flow_excerpt.md` (#1670); Smolka et al., POPL 2020, arXiv:1907.05920 §§2–5. + +## What landed + +`crates/gkat-probe`: zero dependencies, its own `[workspace]`, excluded from the workspace, with its own CI workflow (`.github/workflows/gkat-probe.yml`). + +**The admitted fragment.** +- Constructs: `0`, `1`, assert `b`, action `p`, `e·f`, `if b then e else f`, `while b do e`. +- Boolean tests: `0`, `1`, `t`, `¬`, `∧`, `∨`, over at most **8 primitive tests (at most 256 atoms)**. +- Excluded: unguarded union and Kleene star. + +**The source flow language** (`flow.rs`) is a graph-flow-shaped superset. Lowering admits the structured part and refuses the rest with a typed `Refusal`, never by translation. + +| construct | lowered as | +|---|---| +| `NextAction::Continue` / `ContinueAndExecute` | sequence | +| `End` | accept | +| `WaitForInput` | `while ¬ready do Suspend`, where `ready` is observed at resume | +| conditional edge | `if` | +| `GoTo` / `GoBack` | `Refusal::UnstructuredJump` | +| choice without a condition | `Refusal::UnguardedChoice` | + +**K3 guards.** +- A K3 observable occupies two primitive tests, `is_t` and `is_u`. The atom set excludes `is_t ∧ is_u`, which leaves exactly three values. +- A K3 guard reaches a Boolean test only through a declared projection: + - `Where` = `{T}` + - `Check` = `{T,U}` + - `Is` applies to Boolean observables only. +- Any other pairing of projection and observable is refused. + +**Checks.** +- **Equivalence** (`automaton::equivalent`): the steps follow the paper: + 1. guarded Thompson automata with uniform continuations (§4.2); + 2. normalization of steps into dead states (§5.2); + 3. bisimulation with a union-find (§5.3, Algorithm 1). + + It returns a counterexample prefix. Flows under different signatures are refused (`DeclarationMismatch`); the signature covers observables, projections and action alphabet. +- **Safety** (`automaton::commit_safe`): a separate check, over every reachable step of the **unnormalized** automaton. + - Every `RequestCommit` must come immediately after an atom satisfying WHERE(rev) ∧ WHERE(mul). + - That authorization is fixed by the checker, never taken from the flow. + - An authorization observed before an intervening action is stale. +- **Oracle** (`oracle.rs`): an independent operational interpreter of the expression AST that shares no code with the automaton. It explores every run exhaustively up to a stated action bound. + +## Measured (`cargo test`, 26 tests) + +- **G1.** `if b then {p;q} else {q}` ≡ `(if b then {p} else {skip}); q`. The oracle agrees at bounds 0–4. A changed action label is rejected, a reversed guard is rejected, and a different tail is rejected. `p·0 ≡ 0` (normalization). +- **G2.** Rejections: + - unguarded choice → `UnguardedChoice`; + - `GoTo` / `GoBack` → `UnstructuredJump`; + - the union "do `p` or `q` whatever the atom" fails the determinacy property (§2.2), so no GKAT expression denotes it. + + The admitted Rubicon flows are deterministic. +- **G5.** + - For `k ≤ 8` tests: `2^k` atoms exactly. For `n ≤ 4` K3 observables: `3^n` atoms exactly. + - `k = 9` is refused (`AtomBound`). A DR64-shaped signature (64 Boolean lanes) is refused, as is one with 5 K3 observables (10 tests). + - On a chain of `k` guards, the automaton has `2k` states while the atom count is `2^k`. Measured (k, atoms, states, merged pairs): (1,2,2,3) … (8,256,16,17). + - Counts only, no timings (the workspace's no-ms rule). +- **Rubicon** (11 tests, 36 atoms). + - The reference flow has the decision tail written out twice; the optimized flow factors it out (G1) and reorders the decision. The two are **equivalent**, and both are **safe**. + - Disable runs on the flows: + - reversed authorization polarity → equivalence fails; + - `RequestCommit` moved ahead of its guard → both checks fail; + - authorization observed before `Deliberate`, then `RequestCommit` → safety fails; + - unguarded `Choice{RequestCommit, Hold}` → refused; + - commit authorized with CHECK → safety fails, and the counterexample atom carries a `U`. + - CHECK-authorized reference ≡ CHECK-authorized optimized, and both are **unsafe**: equivalence does not establish safety. +- **Differential.** 600 random expression pairs over 2 tests, half of them single-point mutations: + - 252 equivalent, 348 different, and the oracle separates all 348 within 3 actions; + - every automaton-equivalent pair agrees with the oracle at bounds 0–4; + - every oracle difference is an automaton difference. +- **Checker disable runs: 11, each red then restored green.** + - bisimulation ignoring action labels; + - safety ignoring authorization; + - a loop body that accepts without acting accepting the loop; + - no normalization; + - CHECK lowered as WHERE; + - choice encoded as `if`; + - `GoTo` translated to skip; + - atom bound raised to 64; + - uniform sequence continuation not patched; + - signature mismatch not refused; + - K3 exclusion dropped. + + The first normalization disable stayed green because no test compared a step into a dead state with a rejection. `a_step_into_a_dead_state_is_a_rejection` was added to close that gap. + +## Proof boundary + +- **The paper proves it, for the admitted fragment over a fixed atom set:** bisimilarity of normalized Thompson automata coincides with guarded-string equivalence. +- **This crate's own correctness is tested, not proven.** The oracle is bounded, so its use is one-directional: a difference it finds is real; an agreement up to `n` actions is not a proof. +- **Not modelled:** + - versions, and snapshot or codebook staleness (a separate runtime gate); + - SQL three-valued logic beyond a declared projection, and bag counts; + - side effects, and the Lance write. `RequestCommit` is an intent; the write belongs to the supervisor / `cycle_driver`, which this crate does not touch. +- No near-linear complexity is claimed outside the paper's fixed-atom assumption. + +## Open + +- **D-LFA-1 runtime flow:** unclaimed. The probe models it but does not run graph-flow. +- **Symbolic guards:** BDDs or a SAT-backed bisimulation, to go past 8 tests. Not built, not measured. +- **G3/G4/G6/G7** of the excerpt: not attempted (NULL/bag negatives, loop productivity against a derivative form, physical parity, amortization). diff --git a/.claude/board/entries/README.md b/.claude/board/entries/README.md index be6256020..a0d0036e9 100644 --- a/.claude/board/entries/README.md +++ b/.claude/board/entries/README.md @@ -25,7 +25,7 @@ index row, (3) no duplicate entry id. Checks 1 and 2 are deliberately opposite directions; the stranding this convention prevents shows up in exactly one of them, never both. -421 entries, 2026-08-06 .. 2026-10-21. +423 entries, 2026-08-06 .. 2026-10-21. | date | entry id | finding | file | |---|---|---|---| @@ -46,6 +46,7 @@ exactly one of them, never both. | 2026-10-21 | `D-RA-2` | | [2026-10-21-d-ra-2-relalg-symbolic-repoint.md](2026-10-21-d-ra-2-relalg-symbolic-repoint.md) | | 2026-10-21 | `D-QSP` | | [2026-10-21-d-qsp-d-rft-d-lfa-classview-quack-plan.md](2026-10-21-d-qsp-d-rft-d-lfa-classview-quack-plan.md) | | 2026-10-21 | `D-QSP-0` | | [2026-10-21-d-qsp-0-scalar-aggregates-null.md](2026-10-21-d-qsp-0-scalar-aggregates-null.md) | +| 2026-10-21 | `D-GKAT-0` | | [2026-10-21-d-gkat-0-probe.md](2026-10-21-d-gkat-0-probe.md) | | 2026-10-21 | `D-CMR-6` | | [2026-10-21-d-cmr-6-rule-catalogue.md](2026-10-21-d-cmr-6-rule-catalogue.md) | | 2026-10-21 | `D-CMR-5` | | [2026-10-21-d-cmr-5-rescope.md](2026-10-21-d-cmr-5-rescope.md) | | 2026-10-21 | `D-CMR-2b` | | [2026-10-21-d-cmr-2b-scratch-probe.md](2026-10-21-d-cmr-2b-scratch-probe.md) | From bccff823d4308d5449128ad4a00243a232e4e186 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 21 Oct 2026 19:54:50 +0000 Subject: [PATCH 4/4] gkat-probe: exact divergence detection; determinacy covers acceptance MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Codex review on #1676, two P2 findings, each reproduced by a test that failed before the fix: - the oracle's fixed silent-step budget classified a terminating run of 2^14 skips as divergent; divergence is now a repeated loop-head stack; - the determinacy check ignored acceptance, so skip ∪ p passed; a prefix that both accepts and continues is now nondeterministic. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01VncKoyG6JkpsoqhqTGTv3f --- .../entries/2026-10-21-d-gkat-0-probe.md | 5 +- crates/gkat-probe/src/oracle.rs | 49 ++++++++++++------- crates/gkat-probe/tests/differential.rs | 23 +++++++++ crates/gkat-probe/tests/g2_nondeterminism.rs | 12 +++++ 4 files changed, 68 insertions(+), 21 deletions(-) diff --git a/.claude/board/entries/2026-10-21-d-gkat-0-probe.md b/.claude/board/entries/2026-10-21-d-gkat-0-probe.md index 87edc3a0b..07e7e76cb 100644 --- a/.claude/board/entries/2026-10-21-d-gkat-0-probe.md +++ b/.claude/board/entries/2026-10-21-d-gkat-0-probe.md @@ -45,8 +45,9 @@ - That authorization is fixed by the checker, never taken from the flow. - An authorization observed before an intervening action is stale. - **Oracle** (`oracle.rs`): an independent operational interpreter of the expression AST that shares no code with the automaton. It explores every run exhaustively up to a stated action bound. + Divergence is detected exactly, by a repeated continuation stack at a loop head, not by a step budget. The first version used a fixed budget, which Codex showed misclassifies a terminating run of 2^14 silent steps. -## Measured (`cargo test`, 26 tests) +## Measured (`cargo test`, 28 tests) - **G1.** `if b then {p;q} else {q}` ≡ `(if b then {p} else {skip}); q`. The oracle agrees at bounds 0–4. A changed action label is rejected, a reversed guard is rejected, and a different tail is rejected. `p·0 ≡ 0` (normalization). - **G2.** Rejections: @@ -54,7 +55,7 @@ - `GoTo` / `GoBack` → `UnstructuredJump`; - the union "do `p` or `q` whatever the atom" fails the determinacy property (§2.2), so no GKAT expression denotes it. - The admitted Rubicon flows are deterministic. + So does the union of `skip` and `p`: on one atom it may either accept or act. The admitted Rubicon flows are deterministic. - **G5.** - For `k ≤ 8` tests: `2^k` atoms exactly. For `n ≤ 4` K3 observables: `3^n` atoms exactly. - `k = 9` is refused (`AtomBound`). A DR64-shaped signature (64 Boolean lanes) is refused, as is one with 5 K3 observables (10 tests). diff --git a/crates/gkat-probe/src/oracle.rs b/crates/gkat-probe/src/oracle.rs index 6e93be559..21d8faab6 100644 --- a/crates/gkat-probe/src/oracle.rs +++ b/crates/gkat-probe/src/oracle.rs @@ -16,15 +16,18 @@ //! whenever the oracle finds a difference, the automaton must say //! "different". -use std::collections::{BTreeMap, BTreeSet}; +use std::collections::{BTreeMap, BTreeSet, HashSet}; use crate::expr::{Action, Atom, Atoms, BExp, Exp}; -/// Internal steps allowed between two actions before a run counts as -/// diverging. Between actions the atom cannot change, so a run that takes -/// more steps than the expression has nodes without acting is in a loop that -/// never acts; the bound only needs to exceed any terminating stretch. -const FUEL: usize = 1 << 14; +// Divergence is detected exactly, not by a step budget. Between two actions +// the atom cannot change, so a silent run is determined by its continuation +// stack. Any silent run that never ends re-enters some loop head with a +// stack it has had before, and the set of stacks at loop heads is finite +// (each is a path through the expression). A repeated loop-head stack is +// therefore divergence, and a stretch with no repeat terminates, however +// long it is. (A fixed budget misclassified long terminating stretches; +// Codex review on #1676.) /// One accepted run: the atoms observed (one more than the actions) and the /// actions performed. @@ -71,17 +74,12 @@ fn run( max_actions: usize, out: &mut Exploration, ) { - let mut fuel = FUEL; + let mut loop_heads: HashSet> = HashSet::new(); loop { let Some(e) = stack.pop() else { out.accepted.insert((seen_atoms.clone(), actions.clone())); return; }; - if fuel == 0 { - out.diverged += 1; - return; - } - fuel -= 1; match e { Exp::Fail => { out.rejected += 1; @@ -101,6 +99,12 @@ fn run( Exp::If(b, f, g) => stack.push(if b.eval(atom) { f } else { g }), Exp::While(b, body) => { if b.eval(atom) { + let mut key: Vec<*const Exp> = stack.iter().map(|x| *x as *const Exp).collect(); + key.push(e as *const Exp); + if !loop_heads.insert(key) { + out.diverged += 1; + return; + } stack.push(e); stack.push(body); } @@ -154,19 +158,26 @@ pub fn unsafe_within( } /// The GKAT determinacy property (paper §2.2) of a set of guarded strings: -/// two strings that observe the same atoms up to a position must have taken -/// the same actions up to that position. +/// two strings that observe the same atoms up to a position must take the +/// same step there: the same action, or both accept. pub fn deterministic(strings: &BTreeSet) -> bool { - // Map each observed atom prefix to the action taken after it. - let mut next: BTreeMap, Action> = BTreeMap::new(); + // Map each observed atom prefix to what follows it: an action, or `None` + // for acceptance. A prefix that both accepts and continues is as + // nondeterministic as one followed by two different actions (Codex + // review on #1676). + let mut next: BTreeMap, Option> = BTreeMap::new(); for (atoms, actions) in strings { - for (i, action) in actions.iter().enumerate() { + let steps = actions + .iter() + .map(|a| Some(*a)) + .chain(std::iter::once(None)); + for (i, step) in steps.enumerate() { let key = atoms[..=i].to_vec(); match next.get(&key) { - Some(seen) if seen != action => return false, + Some(seen) if *seen != step => return false, Some(_) => {} None => { - next.insert(key, *action); + next.insert(key, step); } } } diff --git a/crates/gkat-probe/tests/differential.rs b/crates/gkat-probe/tests/differential.rs index b67fad15d..6b496baf7 100644 --- a/crates/gkat-probe/tests/differential.rs +++ b/crates/gkat-probe/tests/differential.rs @@ -136,3 +136,26 @@ fn every_oracle_difference_is_an_automaton_difference() { } } } + +/// A terminating stretch of more silent steps than any fixed budget is not a +/// divergence (Codex review, #1676): a balanced sequence of 2^14 `skip`s is +/// equivalent to `skip`, and the oracle must agree at bound 0. +#[test] +fn long_silent_stretches_are_not_divergence() { + fn skips(depth: u32) -> Exp { + if depth == 0 { + Exp::Skip + } else { + skips(depth - 1).seq(skips(depth - 1)) + } + } + let atoms = Atoms::new(1, &BExp::True).unwrap(); + let e = skips(14); + assert!(equivalent(&e, &Exp::Skip, &atoms).unwrap().holds()); + let x = gkat_probe::oracle::explore(&e, &atoms, 0); + assert_eq!(x.diverged, 0); + assert!(same_up_to(&e, &Exp::Skip, &atoms, 0)); + // A genuinely silent loop still diverges. + let spin = gkat_probe::oracle::explore(&Exp::while_(BExp::True, Exp::Skip), &atoms, 0); + assert_eq!(spin.diverged, atoms.len()); +} diff --git a/crates/gkat-probe/tests/g2_nondeterminism.rs b/crates/gkat-probe/tests/g2_nondeterminism.rs index b176beb47..bb0758b7f 100644 --- a/crates/gkat-probe/tests/g2_nondeterminism.rs +++ b/crates/gkat-probe/tests/g2_nondeterminism.rs @@ -49,3 +49,15 @@ fn admitted_flows_are_deterministic() { assert!(deterministic(&explore(&e, &atoms, 2).accepted)); } } + +/// Termination versus action is nondeterminism too: on the same atom the +/// union of `skip` and `p` may either accept or act (Codex review, #1676). +#[test] +fn a_union_of_accepting_and_acting_is_not_deterministic() { + let atoms = Atoms::new(1, &BExp::True).unwrap(); + let skip = explore(&Exp::Skip, &atoms, 1).accepted; + let p = explore(&Exp::Do(Action("p")), &atoms, 1).accepted; + let union: BTreeSet<_> = skip.union(&p).cloned().collect(); + assert!(deterministic(&skip) && deterministic(&p)); + assert!(!deterministic(&union)); +}