feat(runtimes): add first-class TLA+/TLC runtime support

[Copilot]

Adds runtimes: tla: — a first-class TLA+/TLC runtime mirroring the existing lean, python, node, and dotnet runtimes. Closes the gap for agentic workflows that want to run formal model checking (TLC is the counterpart to Lean: it discovers liveness/safety violations exhaustively rather than proving a fixed design).

What runtimes: tla: does

runtimes:
  tla: true          # latest tla2tools.jar, JDK 21

  # or pin versions:
  tla:
    version: "1.8.0" # tla2tools.jar GitHub release tag
    jdk: "21"        # JDK major version for JavaToolInstaller@0 (default: 21)

• Installs JDK via JavaToolInstaller@0 (pre-installed mode) — selects the JDK matching runtimes.tla.jdk and sets JAVA_HOME
• Installs tla2tools.jar from TLA+ GitHub releases → $HOME/.tla/
• Creates shims tlc (tlc2.TLC), pluscal (pcal.trans), sany (tla2sany.SANY) in $HOME/.tla/bin/ — shims delegate to java from PATH
• Network: GitHub is already in the built-in allowlist; the JDK is pre-installed so no additional network entries needed
• AWF mounts: $HOME/.tla and $(JAVA_HOME) read-only into the AWF sandbox
• AWF PATH: prepends $HOME/.tla/bin and $(JAVA_HOME)/bin inside the AWF chroot
• Bash allow-list: auto-adds java, tlc, pluscal, sany
• Env vars: sets TLA_JAR pipeline variable; JAVA_HOME is set by JavaToolInstaller@0
• Prompt supplement: informs the agent of available commands and invocation patterns

Changes

• src/runtimes/tla/ — new module: TlaRuntimeConfig/TlaOptions config types, generate_tla_tools_install() bash script builder (tla2tools.jar + shims only), TlaExtension implementing CompilerExtension with two prepare steps: Step::Task(JavaToolInstaller@0) + Step::Bash
• src/runtimes/mod.rs — pub mod tla
• src/compile/types.rs — tla field in RuntimesConfig
• src/compile/extensions/mod.rs — Tla(TlaExtension) variant, re-export, collect_extensions wiring
• src/compile/common.rs + standalone.rs — tla: None in existing test RuntimesConfig struct literals
• docs/runtimes.md — full TLA+ section: field reference, shim table, env vars, example model-checking workflow
• prompts/create-ado-agentic-workflow.md — tla: snippet; updated runtime notes

Test plan

cargo test — all 2292 tests pass. TLA+ unit tests cover: default JDK task step (JavaToolInstaller@0 versionSpec "21"), pinned versions, latest jar URL, injection rejection for version: and jdk:, and the bash-disabled warning.

[jamesadevine]

@copilot we should be using JavaToolInstall from the compiler IR. Hook it up to the TLA frontmatter.

[Copilot]

@copilot we should be using JavaToolInstall from the compiler IR. Hook it up to the TLA frontmatter.

Done in the latest commit. TlaExtension.declarations() now emits two steps in order:

1. Step::Task(JavaToolInstaller@0, PreInstalled) — selects the pre-installed JDK matching runtimes.tla.jdk (default "21") and sets JAVA_HOME
2. Step::Bash — downloads tla2tools.jar and creates the tlc/pluscal/sany shims that delegate to java from PATH

The manual Adoptium curl/tar download is removed. Since JavaToolInstaller@0 uses the pre-installed JDK, the java network host entry is no longer needed. The $(JAVA_HOME) ADO macro is added to both the AWF mounts and path prepends so java is accessible inside the AWF chroot.

[jamesadevine]

/rust-review

[jamesadevine]

/rust-review

[github-actions]

✅ Rust PR Reviewer completed successfully!

[github-actions]

🔍 Rust PR Review

Summary: Looks good overall — the structure mirrors existing runtimes faithfully. Two real issues found (one security, one functional bug), plus a stale doc comment.

Findings

🐛 Bugs / Logic Issues

• src/runtimes/tla/mod.rs:164 — version embedded in a double-quoted curl argument without a character allowlist

  generate_tla_tools_install formats the URL directly into a double-quoted bash string:

  curl -sSfL "{jar_url}" -o "$TLA_HOME/tla2tools.jar"

  reject_pipeline_injection blocks ADO expressions ($(, $[), ##vso[ commands, and newlines — but not shell metacharacters like ". A version string such as 1.8.0" -o ~/.ssh/authorized_keys # would break out of the quoted argument and inject curl flags, redirecting the download to an attacker-chosen path.

  This is uniquely worse here than in node/python runtimes: those pass version to an ADO task input (a YAML string value, shell-inert). Here the version ends up inside an executed bash curl command.

  Fix: Add a strict character allowlist before the URL is constructed — only allow [a-zA-Z0-9._-]:

  if let Some(version) = self.config.version() {
      validate::reject_pipeline_injection(version, "runtimes.tla.version")?;
      // NEW: character-allowlist check — version is embedded in a bash curl URL
      if !version.chars().all(|c| c.is_ascii_alphanumeric() || matches!(c, '.' | '-' | '_')) {
          anyhow::bail!(
              "runtimes.tla.version '{}' contains characters not permitted in a version string \
               (only ASCII alphanumeric, '.', '-', '_' are allowed).",
              version
          );
      }
  }

• src/runtimes/tla/extension.rs:134 — JdkArchitecture::X64 is hardcoded

  JavaToolInstaller::pre_installed(jdk_version, JdkArchitecture::X64).into_step()

  Azure Pipelines supports arm64 agent pools (scale sets, self-hosted). In PreInstalled mode JavaToolInstaller@0 uses the architecture to filter available JDKs; asking for x64 on an arm64 agent will fail to find a match (or find the wrong one). JdkArchitecture::Arm64 already exists in the enum. The simplest fix is to omit the architecture or expose it as an optional front-matter field alongside jdk:; the task defaults to the host architecture when no arch is specified.

⚠️ Suggestions

• src/runtimes/tla/mod.rs:109 — stale doc comment on TlaOptions.jdk

  /// JRE/JDK major version to download from Eclipse Temurin (Adoptium).
  

  The implementation uses JavaToolInstaller@0 in PreInstalled mode — nothing is downloaded from Adoptium; the JDK must already be on the build agent. Should read something like: "JDK major version for JavaToolInstaller@0 (pre-installed on the build agent). Examples: \"21\", \"17\". Defaults to \"21\" (current LTS)."

• No integration fixture — every other runtime has at least one fixture in tests/fixtures/ checked by tests/compiler_tests.rs. A minimal fixture (tla-true.md / tla-pinned.md → expected YAML) would lock the JavaToolInstaller task step and curl URL against accidental regression.

✅ What Looks Good

• Validation order is correct: reject_pipeline_injection fires before Ok(Declarations {...}), so errors short-circuit before any script is generated.
• SanitizeConfig derive on TlaOptions follows the existing convention.
• Unit tests cover default JDK, pinned versions, injection rejection on both fields, and the bash-disabled warning.
• set -eo pipefail in the install script.
• is_enabled() / TlaRuntimeConfig::Enabled(bool) / WithOptions mirrors every other runtime exactly — no surprises.

Generated by Rust PR Reviewer for issue #1223 · 479.1 AIC · ⌖ 12.6 AIC · ⊞ 35.2K · ◷
_{Comment /rust-review to run again}