diff --git a/docs/runtimes.md b/docs/runtimes.md index f0922108..03e399a5 100644 --- a/docs/runtimes.md +++ b/docs/runtimes.md @@ -165,6 +165,99 @@ When enabled, the compiler: - **`config:` is functional, not a deferred warning.** AWF only overlays files in `$HOME` (e.g., `~/.npmrc` → `/dev/null`); workspace files such as `nuget.config` are preserved inside the agent sandbox, so a checked-in `nuget.config` works today. - **`NuGetAuthenticate@1` requires no `workingFile:` input.** It auto-discovers `nuget.config` files anywhere in the workspace, unlike `npmAuthenticate@0` which needs an explicit path. +### TLA+ (`tla:`) + +TLA+ / TLC formal model-checking runtime. Uses `JavaToolInstaller@0` to select a pre-installed JDK and downloads `tla2tools.jar` from the TLA+ GitHub releases page, then creates convenience shims (`tlc`, `pluscal`, `sany`) and extends the bash command allow-list. + +TLA+ is a natural complement to the `lean` runtime: **TLC discovers** liveness/safety gaps by exhaustively searching the state space and emitting counterexample traces, while **Lean proves** a fixed design. Agentic workflows that scan codebases for state-machine bugs — finding stuck states, deadlocks, and missing timeouts — are a primary use case. + +```yaml +# Simple enablement (latest tla2tools.jar, JDK 21 LTS) +runtimes: + tla: true + +# With options (pin tla2tools.jar and JDK versions) +runtimes: + tla: + version: "1.8.0" # tla2tools.jar version (omit for latest) + jdk: "21" # JDK major version (default: 21) +``` + +**Fields:** + +| Field | Type | Description | +|-------|------|-------------| +| `version` | string | `tla2tools.jar` version to download from the TLA+ GitHub releases (e.g., `"1.8.0"`, `"1.7.3"`). When omitted, the latest release is downloaded via GitHub's `releases/latest/download/` redirect. | +| `jdk` | string | JDK major version to pass to `JavaToolInstaller@0` (pre-installed on the build agent), e.g., `"21"`, `"17"`. Defaults to `"21"` (current LTS). | + +When enabled, the compiler: +- Contributes a `JavaToolInstaller@0` task step (pre-installed mode) that selects the JDK matching `jdk:` and sets `JAVA_HOME` +- Contributes a bash step to `Declarations::agent_prepare_steps` that: + 1. Downloads `tla2tools.jar` from [TLA+ GitHub releases](https://github.com/tlaplus/tlaplus/releases) into `$HOME/.tla/` + 2. Creates convenience shims (`tlc`, `pluscal`, `sany`) in `$HOME/.tla/bin/` that delegate to `java` from PATH +- Auto-adds `java`, `tlc`, `pluscal`, `sany` to the bash command allow-list +- GitHub is already in the built-in allowlist so no extra network host entry is needed for `tla2tools.jar`. The JDK is provided by `JavaToolInstaller@0` (pre-installed on the build agent) so no additional network access is needed for the JDK either. +- Mounts `$HOME/.tla` and `$(JAVA_HOME)` into the AWF container via `--mount` (read-only) so the toolchain is accessible inside the agent sandbox +- Prepends `$HOME/.tla/bin` and `$(JAVA_HOME)/bin` to `PATH` inside the AWF sandbox +- Sets `TLA_JAR` as a pipeline variable so downstream steps can reference the jar path +- Appends a prompt supplement informing the agent about TLA+ availability and invocation patterns + +**Shims:** + +| Command | Java main class | Description | +|---------|----------------|-------------| +| `tlc` | `tlc2.TLC` | Run the TLC model checker: `tlc -config M.cfg M.tla` | +| `pluscal` | `pcal.trans` | Translate PlusCal to TLA+: `pluscal -nocfg M.tla` | +| `sany` | `tla2sany.SANY` | Parse and syntax-check a spec: `sany M.tla` | + +You can also invoke the JVM directly: `java -XX:+UseParallelGC -cp "$TLA_JAR" tlc2.TLC -workers auto -config M.cfg M.tla` + +**Environment variables available inside the agent sandbox:** + +| Variable | Value | +|----------|-------| +| `TLA_JAR` | Absolute path to `tla2tools.jar` | +| `JAVA_HOME` | JDK home directory (set by `JavaToolInstaller@0`) | + +**Example: TLA+ model-checking workflow** + +```yaml +--- +name: tla-liveness-checker +description: | + Scans the codebase for event-driven state machines, builds TLA+ models, + runs TLC to find liveness gaps, and proposes findings via safe-outputs. +on: + schedule: "weekly on monday" +runtimes: + tla: true +tools: + bash: + - find + - grep + - tlc + - pluscal + - sany + - java +safe-outputs: + create-pull-request: {} + create-work-item: {} +--- + +Scan the repository for state machine implementations (look for enums with +state names, switch/match blocks on state, or explicit state transition maps). + +For each state machine found: +1. Build a TLA+ model in a temp file capturing the states and transitions. +2. Run `pluscal` to translate PlusCal if used, or write TLA+ directly. +3. Run `tlc -config .tla` to check for deadlocks and liveness. +4. If TLC finds a counterexample trace, record the violation. + +If violations are found, propose: +- A draft PR adding the TLA+ models under `formal/` in the repository. +- A work item per liveness gap with the TLC counterexample trace attached. +``` + ### Combining Runtimes Multiple runtimes can be enabled simultaneously: @@ -178,6 +271,8 @@ runtimes: dotnet: version: "8.0.x" lean: true + tla: + version: "1.8.0" ``` All runtime extensions are sorted into `ExtensionPhase::Runtime` and execute before tool extensions (`ExtensionPhase::Tool`), ensuring language toolchains are available before any tools that depend on them. diff --git a/prompts/create-ado-agentic-workflow.md b/prompts/create-ado-agentic-workflow.md index ddd527c9..0dc4f57a 100644 --- a/prompts/create-ado-agentic-workflow.md +++ b/prompts/create-ado-agentic-workflow.md @@ -495,6 +495,13 @@ runtimes: # lean: # toolchain: "leanprover/lean4:v4.29.1" # pin a specific version +# TLA+ / TLC formal model checker +runtimes: + tla: true + # tla: + # version: "1.8.0" # pin tla2tools.jar version (omit for latest) + # jdk: "21" # JDK major version for JavaToolInstaller@0 (default: 21) + # Python runtimes: python: true @@ -529,7 +536,7 @@ runtimes: version: "8.0.x" ``` -> Each enabled runtime auto-adds its ecosystem's bash commands (e.g., `dotnet`, `python`, `node`, `npm`, `lean`, `lake`) and network domains to the allowlist. See `docs/runtimes.md` for full configuration reference. +> Each enabled runtime auto-adds its ecosystem's bash commands (e.g., `dotnet`, `python`, `node`, `npm`, `lean`, `lake`, `tlc`, `java`) and network domains to the allowlist. The `tla:` runtime uses `JavaToolInstaller@0` (pre-installed JDK) and the built-in GitHub allowlist, so it requires no extra network entries. See `docs/runtimes.md` for full configuration reference. ### Step 15 — Network (standalone target only) @@ -544,7 +551,7 @@ network: - "evil.example.com" ``` -`allowed` accepts raw domain patterns (wildcards supported) or ecosystem identifiers (`python`, `node`, `rust`, `dotnet`, `lean`) that expand to the full set of package registry domains for that ecosystem. The built-in allowlist includes: Azure DevOps, GitHub, Microsoft identity, Azure services, Application Insights, and MCP-specific endpoints for each enabled server. +`allowed` accepts raw domain patterns (wildcards supported) or ecosystem identifiers (`python`, `node`, `rust`, `dotnet`, `lean`, `java`) that expand to the full set of package registry domains for that ecosystem. The built-in allowlist includes: Azure DevOps, GitHub, Microsoft identity, Azure services, Application Insights, and MCP-specific endpoints for each enabled server. ### Step 16 — Parameters (optional) diff --git a/src/compile/common.rs b/src/compile/common.rs index 5ba09b7e..932fe57b 100644 --- a/src/compile/common.rs +++ b/src/compile/common.rs @@ -3224,6 +3224,7 @@ mod tests { python: None, node: None, dotnet: None, + tla: None, }); let params = engine_args_for(&fm).unwrap(); assert!( @@ -3259,6 +3260,7 @@ mod tests { python: None, node: None, dotnet: None, + tla: None, }); let params = engine_args_for(&fm).unwrap(); assert!( diff --git a/src/compile/extensions/mod.rs b/src/compile/extensions/mod.rs index eb84f326..7b8c1e49 100644 --- a/src/compile/extensions/mod.rs +++ b/src/compile/extensions/mod.rs @@ -571,6 +571,7 @@ pub use crate::runtimes::dotnet::DotnetExtension; pub use crate::runtimes::lean::LeanExtension; pub use crate::runtimes::node::NodeExtension; pub use crate::runtimes::python::PythonExtension; +pub use crate::runtimes::tla::TlaExtension; pub use crate::tools::azure_devops::AzureDevOpsExtension; pub use crate::tools::cache_memory::CacheMemoryExtension; pub use ado_aw_marker::AdoAwMarkerExtension; @@ -600,6 +601,7 @@ extension_enum! { Python(PythonExtension), Node(NodeExtension), Dotnet(DotnetExtension), + Tla(TlaExtension), AzureDevOps(AzureDevOpsExtension), CacheMemory(CacheMemoryExtension), AzureCli(AzureCliExtension), @@ -742,6 +744,11 @@ pub fn collect_extensions(front_matter: &FrontMatter) -> Vec { { extensions.push(Extension::Dotnet(DotnetExtension::new(dotnet.clone()))); } + if let Some(tla) = front_matter.runtimes.as_ref().and_then(|r| r.tla.as_ref()) + && tla.is_enabled() + { + extensions.push(Extension::Tla(TlaExtension::new(tla.clone()))); + } // ── First-party tools (ExtensionPhase::Tool) ── if let Some(tools) = front_matter.tools.as_ref() { diff --git a/src/compile/standalone.rs b/src/compile/standalone.rs index 56afdc41..a8da344e 100644 --- a/src/compile/standalone.rs +++ b/src/compile/standalone.rs @@ -176,6 +176,7 @@ mod tests { python: None, node: None, dotnet: None, + tla: None, }); let exts = super::super::extensions::collect_extensions(&fm); let domains = allowed_domains(&fm, &exts).unwrap(); @@ -201,6 +202,7 @@ mod tests { python: None, node: None, dotnet: None, + tla: None, }); let exts = super::super::extensions::collect_extensions(&fm); let domains = allowed_domains(&fm, &exts).unwrap(); diff --git a/src/compile/types.rs b/src/compile/types.rs index 9a832b92..0d7930f2 100644 --- a/src/compile/types.rs +++ b/src/compile/types.rs @@ -569,6 +569,14 @@ pub struct RuntimesConfig { /// equivalent for selecting a package source. #[serde(default)] pub dotnet: Option, + + /// TLA+ / TLC formal model-checking runtime. + /// Downloads a JRE from Eclipse Temurin (Adoptium) and `tla2tools.jar` + /// from the TLA+ GitHub releases page, creates convenience shims + /// (`tlc`, `pluscal`, `sany`), adds Java ecosystem domains to the AWF + /// network allowlist, and extends the bash command allow-list. + #[serde(default)] + pub tla: Option, } impl SanitizeConfigTrait for RuntimesConfig { @@ -585,6 +593,9 @@ impl SanitizeConfigTrait for RuntimesConfig { if let Some(ref mut dotnet) = self.dotnet { dotnet.sanitize_config_fields(); } + if let Some(ref mut tla) = self.tla { + tla.sanitize_config_fields(); + } } } diff --git a/src/runtimes/mod.rs b/src/runtimes/mod.rs index 17b4e582..b0ae7b94 100644 --- a/src/runtimes/mod.rs +++ b/src/runtimes/mod.rs @@ -13,3 +13,4 @@ pub mod dotnet; pub mod lean; pub mod node; pub mod python; +pub mod tla; diff --git a/src/runtimes/tla/extension.rs b/src/runtimes/tla/extension.rs new file mode 100644 index 00000000..1d727b3e --- /dev/null +++ b/src/runtimes/tla/extension.rs @@ -0,0 +1,315 @@ +// ─── TLA+ ──────────────────────────────────────────────────────────── + +use super::{TLA_BASH_COMMANDS, TlaRuntimeConfig, DEFAULT_JDK_VERSION, generate_tla_tools_install}; +use crate::compile::extensions::{ + AwfMount, AwfMountMode, CompileContext, CompilerExtension, Declarations, ExtensionPhase, +}; +use crate::compile::ir::step::{BashStep, Step}; +use crate::compile::ir::tasks::java_tool_installer::{JdkArchitecture, JavaToolInstaller}; +use crate::validate; +use anyhow::Result; + +/// TLA+ / TLC runtime extension. +/// +/// Injects: bash commands (`java`, `tlc`, `pluscal`, `sany`), a +/// [`JavaToolInstaller@0`] task step (selects the pre-installed JDK and +/// sets `JAVA_HOME`), a bash step that downloads `tla2tools.jar` and +/// creates shims, AWF mounts (`$HOME/.tla` and `$(JAVA_HOME)`), +/// PATH prepends (`$HOME/.tla/bin` and `$(JAVA_HOME)/bin`), and a prompt +/// supplement. +/// +/// GitHub is already in the built-in allowlist so no extra network host +/// entry is needed for the `tla2tools.jar` download. +/// +/// [`JavaToolInstaller@0`]: crate::compile::ir::tasks::java_tool_installer::JavaToolInstaller +pub struct TlaExtension { + config: TlaRuntimeConfig, +} + +impl TlaExtension { + pub fn new(config: TlaRuntimeConfig) -> Self { + Self { config } + } +} + +impl CompilerExtension for TlaExtension { + fn name(&self) -> &str { + "TLA+" + } + + fn phase(&self) -> ExtensionPhase { + ExtensionPhase::Runtime + } + + /// Returns two typed prepare steps and all static signals: + /// + /// 1. [`Step::Task`] — `JavaToolInstaller@0` (`PreInstalled` mode): + /// selects the JDK matching `runtimes.tla.jdk` and sets `JAVA_HOME`. + /// 2. [`Step::Bash`] — downloads `tla2tools.jar` and creates shims + /// (`tlc`, `pluscal`, `sany`) that delegate to `java` from PATH. + fn declarations(&self, ctx: &CompileContext) -> Result { + let mut warnings = Vec::new(); + + let is_bash_disabled = ctx + .front_matter + .tools + .as_ref() + .and_then(|t| t.bash.as_ref()) + .is_some_and(|cmds| cmds.is_empty()); + + if is_bash_disabled { + warnings.push(format!( + "Agent '{}' has runtimes.tla enabled but tools.bash is empty. \ + TLA+ requires bash access (java, tlc, pluscal, sany commands).", + ctx.agent_name + )); + } + + // Validate version string (reject pipeline injection) + if let Some(version) = self.config.version() { + validate::reject_pipeline_injection(version, "runtimes.tla.version")?; + } + + // Validate jdk string (reject pipeline injection) + if let Some(jdk) = self.config.jdk() { + validate::reject_pipeline_injection(jdk, "runtimes.tla.jdk")?; + } + + Ok(Declarations { + agent_prepare_steps: vec![ + Step::Task(java_install_task_step(&self.config)), + Step::Bash(tla_tools_bash_step(&self.config)), + ], + // GitHub is already in the built-in allowlist — no extra entry + // is needed for tla2tools.jar. The JDK is provided by + // JavaToolInstaller@0 (pre-installed on the build agent). + network_hosts: vec![], + bash_commands: TLA_BASH_COMMANDS + .iter() + .map(|c| (*c).to_string()) + .collect(), + prompt_supplement: Some( + "\n\ +---\n\ +\n\ +## TLA+ / TLC Formal Model Checking\n\ +\n\ +TLA+ is installed and available. The toolchain includes:\n\ +- `tlc` — run the TLC model checker: `tlc -config M.cfg M.tla`\n\ +- `pluscal` — translate PlusCal to TLA+: `pluscal -nocfg M.tla`\n\ +- `sany` — parse and syntax-check a TLA+ spec: `sany M.tla`\n\ +- `java` — direct JVM access: `java -cp \"$TLA_JAR\" tlc2.TLC ...`\n\ +\n\ +Environment variables available inside the agent sandbox:\n\ +- `TLA_JAR` — absolute path to `tla2tools.jar`\n\ +- `JAVA_HOME` — JDK home directory (set by `JavaToolInstaller@0`)\n\ +\n\ +TLA+ spec files use the `.tla` extension; PlusCal sources are embedded in\n\ +`(*--algorithm ... *)` blocks inside `.tla` files.\n" + .to_string(), + ), + awf_mounts: vec![ + AwfMount::new("$HOME/.tla", "$HOME/.tla", AwfMountMode::ReadOnly), + // Mount the JDK installation (path set at runtime by JavaToolInstaller@0) + // into the AWF sandbox so `java` is accessible inside the chroot. + AwfMount::new("$(JAVA_HOME)", "$(JAVA_HOME)", AwfMountMode::ReadOnly), + ], + awf_path_prepends: vec![ + "$HOME/.tla/bin".to_string(), + // JavaToolInstaller@0 sets $(JAVA_HOME); expose its bin/ inside + // the AWF chroot so shims can call `java` directly. + "$(JAVA_HOME)/bin".to_string(), + ], + warnings, + ..Declarations::default() + }) + } +} + +/// Build the typed [`crate::compile::ir::step::TaskStep`] for installing the JDK via `JavaToolInstaller@0`. +fn java_install_task_step( + config: &TlaRuntimeConfig, +) -> crate::compile::ir::step::TaskStep { + let jdk_version = config.jdk().unwrap_or(DEFAULT_JDK_VERSION); + JavaToolInstaller::pre_installed(jdk_version, JdkArchitecture::X64).into_step() +} + +/// Build the typed [`BashStep`] for downloading `tla2tools.jar` and creating shims. +fn tla_tools_bash_step(config: &TlaRuntimeConfig) -> BashStep { + BashStep::new( + "Install TLA+ toolchain (tla2tools.jar + shims)", + generate_tla_tools_install(config), + ) +} + +#[cfg(test)] +mod tests { + use super::*; + use crate::compile::parse_markdown; + + #[test] + fn test_validate_tla_bash_disabled_emits_warning() { + let (fm, _) = + parse_markdown("---\nname: test\ndescription: test\ntools:\n bash: []\n---\n") + .unwrap(); + let ext = TlaExtension::new(TlaRuntimeConfig::Enabled(true)); + let ctx = CompileContext::for_test(&fm); + let warnings = ext.declarations(&ctx).unwrap().warnings; + assert!(!warnings.is_empty()); + assert!(warnings[0].contains("tools.bash is empty")); + } + + /// Locks `declarations()`: must return a typed `Step::Task` (`JavaToolInstaller@0`) + /// followed by a `Step::Bash` (tla2tools.jar + shims), plus all static signals + /// (bash commands, mounts, PATH prepends, prompt). + #[test] + fn declarations_returns_typed_task_then_bash_step_and_static_signals() { + let (fm, _) = parse_markdown("---\nname: t\ndescription: x\n---\n").unwrap(); + let ext = TlaExtension::new(TlaRuntimeConfig::Enabled(true)); + let ctx = CompileContext::for_test(&fm); + let decl = ext.declarations(&ctx).unwrap(); + assert_eq!(decl.agent_prepare_steps.len(), 2); + // Step 1: JavaToolInstaller@0 + match &decl.agent_prepare_steps[0] { + Step::Task(t) => { + assert_eq!(t.task, "JavaToolInstaller@0"); + assert_eq!( + t.inputs.get("versionSpec").map(String::as_str), + Some("21"), + "default JDK version should be 21" + ); + assert_eq!( + t.inputs.get("jdkSourceOption").map(String::as_str), + Some("PreInstalled") + ); + } + other => panic!("expected Step::Task(JavaToolInstaller@0), got {other:?}"), + } + // Step 2: tla2tools.jar + shims bash step + match &decl.agent_prepare_steps[1] { + Step::Bash(b) => { + assert_eq!( + b.display_name, + "Install TLA+ toolchain (tla2tools.jar + shims)" + ); + assert!( + !b.script.contains("api.adoptium.net"), + "should NOT fetch JRE from Adoptium (JavaToolInstaller handles it)" + ); + assert!(b.script.contains("tla2tools.jar"), "should download tla2tools.jar"); + assert!(b.script.contains("tlc2.TLC"), "should create tlc shim"); + assert!(b.script.contains("pcal.trans"), "should create pluscal shim"); + assert!(b.script.contains("tla2sany.SANY"), "should create sany shim"); + } + other => panic!("expected Step::Bash, got {other:?}"), + } + assert!( + decl.network_hosts.is_empty(), + "no extra network hosts needed: GitHub is built-in, JDK is pre-installed" + ); + assert!(decl.bash_commands.contains(&"tlc".to_string())); + assert!(decl.bash_commands.contains(&"java".to_string())); + assert!(decl.bash_commands.contains(&"pluscal".to_string())); + assert!(decl.bash_commands.contains(&"sany".to_string())); + assert!(decl.prompt_supplement.is_some()); + assert_eq!(decl.awf_mounts.len(), 2); + assert_eq!(decl.awf_mounts[0].host_path, "$HOME/.tla"); + assert_eq!(decl.awf_mounts[1].host_path, "$(JAVA_HOME)"); + assert_eq!( + decl.awf_path_prepends, + vec!["$HOME/.tla/bin".to_string(), "$(JAVA_HOME)/bin".to_string()] + ); + // Slots TLA+ doesn't contribute to must be empty. + assert!(decl.setup_steps.is_empty()); + assert!(decl.mcpg_servers.is_empty()); + assert!(decl.copilot_allow_tools.is_empty()); + } + + #[test] + fn declarations_uses_default_jdk_and_latest_jar_when_unset() { + let (fm, _) = parse_markdown("---\nname: t\ndescription: x\n---\n").unwrap(); + let ext = TlaExtension::new(TlaRuntimeConfig::Enabled(true)); + let ctx = CompileContext::for_test(&fm); + let decl = ext.declarations(&ctx).unwrap(); + // Step 1: JavaToolInstaller with default JDK version + match &decl.agent_prepare_steps[0] { + Step::Task(t) => { + assert_eq!( + t.inputs.get("versionSpec").map(String::as_str), + Some("21"), + "default JDK should be 21" + ); + } + other => panic!("expected Step::Task, got {other:?}"), + } + // Step 2: bash step with latest jar URL + match &decl.agent_prepare_steps[1] { + Step::Bash(b) => { + assert!( + b.script.contains("releases/latest/download/tla2tools.jar"), + "default jar URL should use latest release redirect: {}", + b.script + ); + } + other => panic!("expected Step::Bash, got {other:?}"), + } + } + + #[test] + fn declarations_uses_pinned_versions_when_configured() { + let (fm, _) = parse_markdown( + "---\nname: t\ndescription: x\nruntimes:\n tla:\n version: '1.8.0'\n jdk: '17'\n---\n", + ) + .unwrap(); + let tla = fm.runtimes.as_ref().unwrap().tla.as_ref().unwrap(); + let ext = TlaExtension::new(tla.clone()); + let ctx = CompileContext::for_test(&fm); + let decl = ext.declarations(&ctx).unwrap(); + // Step 1: JavaToolInstaller with pinned JDK version + match &decl.agent_prepare_steps[0] { + Step::Task(t) => { + assert_eq!( + t.inputs.get("versionSpec").map(String::as_str), + Some("17"), + "should use JDK 17" + ); + } + other => panic!("expected Step::Task, got {other:?}"), + } + // Step 2: bash step with pinned jar version + match &decl.agent_prepare_steps[1] { + Step::Bash(b) => { + assert!( + b.script.contains("download/v1.8.0/tla2tools.jar"), + "should use pinned jar version 1.8.0: {}", + b.script + ); + } + other => panic!("expected Step::Bash, got {other:?}"), + } + } + + #[test] + fn declarations_rejects_injection_in_version() { + let (fm, _) = parse_markdown( + "---\nname: t\ndescription: x\nruntimes:\n tla:\n version: '$(SECRET)'\n---\n", + ) + .unwrap(); + let tla = fm.runtimes.as_ref().unwrap().tla.as_ref().unwrap(); + let ext = TlaExtension::new(tla.clone()); + let ctx = CompileContext::for_test(&fm); + assert!(ext.declarations(&ctx).is_err()); + } + + #[test] + fn declarations_rejects_injection_in_jdk() { + let (fm, _) = parse_markdown( + "---\nname: t\ndescription: x\nruntimes:\n tla:\n jdk: '$(SECRET)'\n---\n", + ) + .unwrap(); + let tla = fm.runtimes.as_ref().unwrap().tla.as_ref().unwrap(); + let ext = TlaExtension::new(tla.clone()); + let ctx = CompileContext::for_test(&fm); + assert!(ext.declarations(&ctx).is_err()); + } +} diff --git a/src/runtimes/tla/mod.rs b/src/runtimes/tla/mod.rs new file mode 100644 index 00000000..2383b389 --- /dev/null +++ b/src/runtimes/tla/mod.rs @@ -0,0 +1,192 @@ +//! TLA+ / TLC runtime support for the ado-aw compiler. +//! +//! When enabled via `runtimes: tla:`, the compiler emits a +//! [`JavaToolInstaller@0`] task step (selecting a pre-installed JDK) followed +//! by a bash step that downloads `tla2tools.jar` from the TLA+ GitHub releases +//! page and creates convenience shims (`tlc`, `pluscal`, `sany`). +//! +//! [`JavaToolInstaller@0`]: crate::compile::ir::tasks::java_tool_installer::JavaToolInstaller +//! +//! The `tla2tools.jar` and shims are installed into `$HOME/.tla/`, which is +//! mounted read-only into the AWF chroot via the `required_awf_mounts()` +//! mechanism. The JDK itself is mounted via the `$(JAVA_HOME)` pipeline +//! variable that `JavaToolInstaller@0` sets. +//! +//! ## Network requirements +//! +//! - **JDK**: provided by `JavaToolInstaller@0` (pre-installed on the build +//! agent — no network download required). +//! - **`tla2tools.jar` download**: GitHub releases — covered by the built-in +//! GitHub allowlist that every pipeline includes by default. +//! +//! ## Shims +//! +//! Three shims are created in `$HOME/.tla/bin/`: +//! - `tlc` — runs `tlc2.TLC` (the model checker) +//! - `pluscal` — runs `pcal.trans` (PlusCal → TLA+ translator) +//! - `sany` — runs `tla2sany.SANY` (the SANY parser) + +pub mod extension; + +pub use extension::TlaExtension; + +use ado_aw_derive::SanitizeConfig; +use serde::Deserialize; + +use crate::sanitize::SanitizeConfig as SanitizeConfigTrait; + +/// TLA+ runtime configuration — accepts both `true` and object formats. +/// +/// Examples: +/// ```yaml +/// # Simple enablement (installs latest tla2tools.jar with JDK 21) +/// runtimes: +/// tla: true +/// +/// # With options (pin versions) +/// runtimes: +/// tla: +/// version: "1.8.0" # tla2tools.jar version; omit for latest +/// jdk: "21" # JRE major version (default 21) +/// ``` +#[derive(Debug, Deserialize, Clone)] +#[serde(untagged)] +pub enum TlaRuntimeConfig { + /// Simple boolean enablement + Enabled(bool), + /// Full configuration with options + WithOptions(TlaOptions), +} + +impl TlaRuntimeConfig { + /// Whether TLA+ is enabled. + pub fn is_enabled(&self) -> bool { + match self { + TlaRuntimeConfig::Enabled(enabled) => *enabled, + TlaRuntimeConfig::WithOptions(_) => true, + } + } + + /// Get the `tla2tools.jar` version override (None = use latest from GitHub). + pub fn version(&self) -> Option<&str> { + match self { + TlaRuntimeConfig::Enabled(_) => None, + TlaRuntimeConfig::WithOptions(opts) => opts.version.as_deref(), + } + } + + /// Get the JDK major version (None = use default of `"21"`). + pub fn jdk(&self) -> Option<&str> { + match self { + TlaRuntimeConfig::Enabled(_) => None, + TlaRuntimeConfig::WithOptions(opts) => opts.jdk.as_deref(), + } + } +} + +impl SanitizeConfigTrait for TlaRuntimeConfig { + fn sanitize_config_fields(&mut self) { + match self { + TlaRuntimeConfig::Enabled(_) => {} + TlaRuntimeConfig::WithOptions(opts) => opts.sanitize_config_fields(), + } + } +} + +/// TLA+ runtime options. +#[derive(Debug, Deserialize, Clone, Default, SanitizeConfig)] +pub struct TlaOptions { + /// `tla2tools.jar` version to download from the TLA+ GitHub releases. + /// + /// Examples: `"1.8.0"`, `"1.7.3"`. + /// + /// When omitted the compiler downloads the latest GitHub release using + /// the `releases/latest/download/` redirect — no explicit version pinning + /// is required for most workflows. + #[serde(default)] + pub version: Option, + + /// JRE/JDK major version to download from Eclipse Temurin (Adoptium). + /// + /// Examples: `"21"`, `"17"`. Defaults to `"21"` (current LTS). + /// + /// The JRE (not a full JDK) is downloaded since TLC only needs a runtime. + #[serde(default)] + pub jdk: Option, +} + +/// Default JRE major version used when `jdk:` is not specified. +pub const DEFAULT_JDK_VERSION: &str = "21"; + +/// Bash commands that the TLA+ runtime adds to the allow-list. +/// +/// - `java` — direct JVM invocation (e.g. `java -cp $TLA_JAR tlc2.TLC`) +/// - `tlc` — convenience shim for running the TLC model checker +/// - `pluscal` — shim for the PlusCal → TLA+ translator +/// - `sany` — shim for the SANY parser / syntax checker +pub const TLA_BASH_COMMANDS: &[&str] = &["java", "tlc", "pluscal", "sany"]; + +/// Generate the TLA+ tools installation bash script body. +/// +/// Downloads and stages: +/// 1. `tla2tools.jar` from TLA+ GitHub releases into `$HOME/.tla/` +/// 2. Shim scripts (`tlc`, `pluscal`, `sany`) in `$HOME/.tla/bin/` +/// +/// The JDK is provided by a preceding [`JavaToolInstaller@0`] task step, +/// which sets `JAVA_HOME` and adds it to `PATH`. The shims therefore invoke +/// `java` directly from `PATH`. +/// +/// Sets `TLA_JAR` via `##vso[task.setvariable]` so downstream steps can +/// reference the jar path. Also prepends `$HOME/.tla/bin` to PATH via +/// `##vso[task.prependpath]`. +/// +/// [`JavaToolInstaller@0`]: crate::compile::ir::tasks::java_tool_installer::JavaToolInstaller +pub fn generate_tla_tools_install(config: &TlaRuntimeConfig) -> String { + let jar_url = match config.version() { + Some(v) => format!( + "https://github.com/tlaplus/tlaplus/releases/download/v{v}/tla2tools.jar" + ), + None => { + "https://github.com/tlaplus/tlaplus/releases/latest/download/tla2tools.jar" + .to_string() + } + }; + + format!( + "\ +set -eo pipefail +TLA_HOME=\"$HOME/.tla\" +BIN_DIR=\"$TLA_HOME/bin\" +mkdir -p \"$TLA_HOME\" \"$BIN_DIR\" + +# Download tla2tools.jar +echo \"Downloading tla2tools.jar...\" +curl -sSfL \"{jar_url}\" -o \"$TLA_HOME/tla2tools.jar\" + +# Create shim: tlc (TLC model checker) +cat > \"$BIN_DIR/tlc\" << 'TLA_SHIM_EOF' +#!/usr/bin/env bash +exec java -XX:+UseParallelGC -cp \"$HOME/.tla/tla2tools.jar\" tlc2.TLC \"$@\" +TLA_SHIM_EOF + +# Create shim: pluscal (PlusCal -> TLA+ translator) +cat > \"$BIN_DIR/pluscal\" << 'TLA_SHIM_EOF' +#!/usr/bin/env bash +exec java -cp \"$HOME/.tla/tla2tools.jar\" pcal.trans \"$@\" +TLA_SHIM_EOF + +# Create shim: sany (SANY parser / syntax checker) +cat > \"$BIN_DIR/sany\" << 'TLA_SHIM_EOF' +#!/usr/bin/env bash +exec java -cp \"$HOME/.tla/tla2tools.jar\" tla2sany.SANY \"$@\" +TLA_SHIM_EOF + +chmod +x \"$BIN_DIR/tlc\" \"$BIN_DIR/pluscal\" \"$BIN_DIR/sany\" + +# Expose environment +echo \"##vso[task.prependpath]$HOME/.tla/bin\" +echo \"##vso[task.setvariable variable=TLA_JAR]$HOME/.tla/tla2tools.jar\" +echo \"TLA+ toolchain ready: $TLA_HOME\"\ +" + ) +}