Hermetic Rust decision cores, gates, duals

.cargo/config.toml

@@ -0,0 +1,5 @@
+# Prefer system linker so cargo isn't broken by hermetic_cc/zig from Bazel env.
+[target.aarch64-apple-darwin]
+linker = "cc"
+[target.x86_64-apple-darwin]
+linker = "cc"

.gitignore

@@ -6,3 +6,4 @@ bazel-*
 /sample-eval
 /ote
 gen/
+/target

AGENTS.md

@@ -54,8 +54,9 @@ CI: `tla-specs` job runs `scripts/check-specs.sh`.
 
 ```bash
 scripts/decision-check.sh              # lean: wires + decision-tagged tests
-bazel run  //tools/decision:update     # Decision.tla → committed *spec
-bazel test //tools/decision:up_to_date # codegen freshness
+bazel run  //tools/decision:update     # Decision.tla → Go *spec + Rust modules
+bazel test //tools/decision:up_to_date # Go + Rust codegen freshness
+cargo test -p decision_cores           # Rust gates + duals
 ```
 
 Rules (short):

Cargo.toml

@@ -0,0 +1,3 @@
+[workspace]
+members = ["crates/decision_cores"]
+resolver = "2"

crates/decision_cores/BUILD.bazel

@@ -0,0 +1,15 @@
+# gazelle:ignore
+# Committed Rust decision modules (generated). Up-to-date via //tools/decision:*_rs_up_to_date.
+exports_files([
+    "src/tui_reload.rs",
+    "src/rate_limit.rs",
+    "src/timing_clamp.rs",
+    "src/sync_bounds.rs",
+    "src/gha_lifecycle.rs",
+    "src/log_groups.rs",
+    "src/span_tree.rs",
+    "src/lib.rs",
+    "src/gates.rs",
+    "tests/log_groups_dual.rs",
+    "Cargo.toml",
+])

crates/decision_cores/Cargo.toml

@@ -0,0 +1,10 @@
+[package]
+name = "decision_cores"
+version = "0.1.0"
+edition = "2021"
+description = "TLA+ decision cores (Rust) — generated from specs/*/decision/Decision.tla"
+license = "MIT"
+publish = false
+
+[lib]
+path = "src/lib.rs"

crates/decision_cores/src/gates.rs

@@ -0,0 +1,96 @@
+//! Thin production-style gates over generated decision modules.
+//! Call generated pure/actions — do not re-inline formulas.
+
+use crate::log_groups;
+use crate::rate_limit;
+use crate::span_tree;
+use crate::sync_bounds;
+use crate::timing_clamp;
+use crate::tui_reload;
+
+/// log-groups: may close stack (→ `log_groups::State::can_close`).
+pub fn can_close_group(depth: i64) -> bool {
+    log_groups::State { depth }.can_close()
+}
+
+/// log-groups: may open when depth is within decision MaxDepth=3.
+pub fn can_open_group(depth: i64, max_depth: i64) -> bool {
+    if depth < 0 {
+        return false;
+    }
+    if max_depth <= 0 {
+        return true; // unbounded (matches Go splitGroups)
+    }
+    if max_depth == 3 {
+        return log_groups::State { depth }.can_open();
+    }
+    depth < max_depth
+}
+
+/// rate-limit: wait needed (scalar encoding of duration, like Go).
+pub fn rate_limit_wait_needed(remaining: i64, reset_known: bool, until_reset_positive: bool) -> bool {
+    let reset_at = if reset_known { 1 } else { 0 };
+    let clock = if until_reset_positive { 0 } else { reset_at };
+    rate_limit::State {
+        remaining,
+        sleeping: false,
+        clock,
+        reset_at,
+        sent_while_exhausted: false,
+    }
+    .wait_needed()
+}
+
+/// sync-bounds: accept jobs attempt.
+pub fn accept_jobs_attempt(stored: i64, incoming: i64) -> bool {
+    sync_bounds::State {
+        phase: String::from("stored"),
+        stored_attempt: stored,
+        incoming_attempt: incoming,
+        accepted: false,
+    }
+    .accept_allowed()
+}
+
+/// tui-reload: fresh log-fetch (job match + CanFetchAccept).
+pub fn log_fetch_result_fresh(msg_job: i64, fetching_job: i64, msg_gen: i64, reload_gen: i64) -> bool {
+    if msg_job == 0 || msg_job != fetching_job {
+        return false;
+    }
+    tui_reload::State {
+        is_loading: false,
+        reload_gen,
+        fetch_job: fetching_job,
+        fetch_gen: msg_gen,
+        stale_accepted: false,
+    }
+    .can_fetch_accept()
+}
+
+/// span-tree: drop API side of 1+1 twin.
+pub fn drop_api_for_runner_twin(api_count: i64, runner_count: i64, this_is_runner: bool) -> bool {
+    if api_count != 1 || runner_count != 1 {
+        return false;
+    }
+    let kept = span_tree::State::init()
+        .see_api()
+        .see_runner()
+        .dedup_choose()
+        .kept;
+    kept == "runner" && !this_is_runner
+}
+
+/// timing-clamp: DoClamp on hostile child.
+pub fn clamp_span_to_parent(start: i64, end: i64, parent_start: i64, parent_end: i64) -> (i64, i64) {
+    let s = timing_clamp::State {
+        phase: String::from("init"),
+        start,
+        end,
+        parent_start,
+        parent_end,
+        out_start: 0,
+        out_end: 0,
+    }
+    .do_clamp();
+    (s.out_start, s.out_end)
+}

crates/decision_cores/src/gha_lifecycle.rs

@@ -0,0 +1,195 @@
+// Code generated by specgen from specs/gha-lifecycle/decision/Decision.tla — DO NOT EDIT.
+//
+// Source:     specs/gha-lifecycle/decision/Decision.tla
+// Regenerate: bazel run //tools/decision:update
+//
+// Edit the .tla, not this file. Language: Rust (PATH A decision core).
+// Package/module hint: ghalifecyclespec
+
+#[derive(Clone, Debug, Default, PartialEq, Eq)]
+pub struct State {
+	pub has_completed_at: bool,
+	pub conclusion: String,
+	pub counted_pending: bool,
+	pub counted_failed: bool,
+	pub queue_counted: bool,
+}
+
+impl State {
+	/// Initial state from the TLA+ Init predicate.
+	pub fn init() -> Self {
+		Self {
+			has_completed_at: false,
+			conclusion: String::from("failure"),
+			counted_pending: false,
+			counted_failed: false,
+			queue_counted: false,
+		}
+	}
+
+	/// Guard for action ClassifyPending.
+	pub fn can_classify_pending(&self) -> bool {
+		!(self.has_completed_at) && !(self.counted_pending)
+	}
+
+	/// Apply action ClassifyPending (consuming self — pure transition).
+	pub fn classify_pending(self) -> Self {
+		let pre = self;
+		Self {
+			counted_pending: true,
+			has_completed_at: pre.has_completed_at,
+			conclusion: pre.conclusion,
+			counted_failed: pre.counted_failed,
+			queue_counted: pre.queue_counted,
+		}
+	}
+
+	/// Guard for action ClassifyFailed.
+	pub fn can_classify_failed(&self) -> bool {
+		((false || self.has_completed_at) && ((self.conclusion == "failure") || (self.conclusion == "timed_out"))) && !(self.counted_failed)
+	}
+
+	/// Apply action ClassifyFailed (consuming self — pure transition).
+	pub fn classify_failed(self) -> Self {
+		let pre = self;
+		Self {
+			counted_failed: true,
+			has_completed_at: pre.has_completed_at,
+			conclusion: pre.conclusion,
+			counted_pending: pre.counted_pending,
+			queue_counted: pre.queue_counted,
+		}
+	}
+
+	/// Guard for action ClassifyQueue.
+	pub fn can_classify_queue(&self) -> bool {
+		(false || self.has_completed_at) && !(self.queue_counted)
+	}
+
+	/// Apply action ClassifyQueue (consuming self — pure transition).
+	pub fn classify_queue(self) -> Self {
+		let pre = self;
+		Self {
+			queue_counted: true,
+			has_completed_at: pre.has_completed_at,
+			conclusion: pre.conclusion,
+			counted_pending: pre.counted_pending,
+			counted_failed: pre.counted_failed,
+		}
+	}
+
+	/// Guard for action Reset.
+	pub fn can_reset(&self) -> bool {
+		true
+	}
+
+	/// Apply action Reset (consuming self — pure transition).
+	pub fn reset(self) -> Self {
+		let pre = self;
+		Self {
+			counted_pending: false,
+			counted_failed: false,
+			queue_counted: false,
+			has_completed_at: true,
+			conclusion: (if pre.conclusion == "failure" { String::from("timed_out") } else { if pre.conclusion == "timed_out" { String::from("success") } else { String::from("failure") } }),
+		}
+	}
+
+	/// Names of actions whose guards hold.
+	pub fn enabled_actions(&self) -> Vec<&'static str> {
+		let mut out = Vec::new();
+		if self.can_classify_pending() {
+			out.push("ClassifyPending");
+		}
+		if self.can_classify_failed() {
+			out.push("ClassifyFailed");
+		}
+		if self.can_classify_queue() {
+			out.push("ClassifyQueue");
+		}
+		if self.can_reset() {
+			out.push("Reset");
+		}
+		out
+	}
+
+	/// Apply a named action if its guard holds.
+	pub fn apply_action(self, name: &str) -> Option<Self> {
+		match name {
+			"ClassifyPending" => {
+				if self.can_classify_pending() {
+					Some(self.classify_pending())
+				} else {
+					None
+				}
+			}
+			"ClassifyFailed" => {
+				if self.can_classify_failed() {
+					Some(self.classify_failed())
+				} else {
+					None
+				}
+			}
+			"ClassifyQueue" => {
+				if self.can_classify_queue() {
+					Some(self.classify_queue())
+				} else {
+					None
+				}
+			}
+			"Reset" => {
+				if self.can_reset() {
+					Some(self.reset())
+				} else {
+					None
+				}
+			}
+			_ => None,
+		}
+	}
+}
+
+impl State {
+	/// Pure TLA+ operator PendingNeverFailed.
+	pub fn pending_never_failed(&self) -> bool {
+		!((self.counted_pending && self.counted_failed))
+	}
+
+	/// Pure TLA+ operator QueueOnlyNotPending.
+	pub fn queue_only_not_pending(&self) -> bool {
+		!(self.queue_counted) || (self.has_completed_at)
+	}
+
+}
+
+/// Named pure predicates for dual/CI enumeration.
+pub struct PurePredicate {
+	pub name: &'static str,
+	pub check: fn(&State) -> bool,
+}
+
+/// Every pure operator emitted for this module.
+pub const PURE_PREDICATES: &[PurePredicate] = &[
+	PurePredicate { name: "PendingNeverFailed", check: State::pending_never_failed },
+	PurePredicate { name: "QueueOnlyNotPending", check: State::queue_only_not_pending },
+];
+
+#[cfg(test)]
+mod tests {
+	use super::*;
+
+	#[test]
+	fn init_ok() {
+		let s = State::init();
+		let _ = s.enabled_actions();
+	}
+
+	#[test]
+	fn pure_predicates_no_panic() {
+		let s = State::init();
+		assert_eq!(PURE_PREDICATES.len(), 2);
+		for p in PURE_PREDICATES {
+			let _ = (p.check)(&s);
+		}
+	}
+}

crates/decision_cores/src/lib.rs

@@ -0,0 +1,20 @@
+//! Decision cores for otel-explorer (Rust peer of Go `*spec` packages).
+//!
+//! **SSOT:** `specs/<core>/decision/Decision.tla`  
+//! **Regen:** `bazel run //tools/decision:update`  
+//! **Check:** `cargo test -p decision_cores` and `bazel test //tools/decision:up_to_date`
+//!
+//! Generated modules are pure state machines. Production-style gates live in
+//! [`gates`] — thin wrappers (same idea as Go `canCloseGroup` → `CanClose`).
+
+#![allow(dead_code)]
+
+pub mod gha_lifecycle;
+pub mod log_groups;
+pub mod rate_limit;
+pub mod span_tree;
+pub mod sync_bounds;
+pub mod timing_clamp;
+pub mod tui_reload;
+
+pub mod gates;