@@ -45,16 +45,17 @@
   - 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:
   - 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.
+  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).
 
@@ -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<Vec<*const Exp>> = 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<GuardedString>) -> bool {
-    // Map each observed atom prefix to the action taken after it.
-    let mut next: BTreeMap<Vec<Atom>, 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<Vec<Atom>, Option<Action>> = 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);
                 }
             }
         }
 
@@ -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());
+}
@@ -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));
+}