More fixes to CI

Author: thirtytwobits

.devcontainer/devcontainer.json

@@ -1,6 +1,6 @@
 {
-  "name": "llvm-dsdl (toolshed ts26.4.1)",
-  "image": "ghcr.io/opencyphal/toolshed:ts26.4.1",
+  "name": "llvm-dsdl (toolshed ts26.4.2)",
+  "image": "ghcr.io/opencyphal/toolshed:ts26.4.2",
   "containerEnv": {
     "LLVM_DIR": "/usr/lib/llvm-22/lib/cmake/llvm",
     "MLIR_DIR": "/usr/lib/llvm-22/lib/cmake/mlir",

.devcontainer/post-create.sh

@@ -22,7 +22,7 @@ if [[ -z "${llvm_version}" ]]; then
 fi
 
 missing=()
-for tool in cmake ninja python3 git lit gzip go cargo tsc node "clang-${llvm_version}"; do
+for tool in cmake ninja python3 git lit gzip go cargo tsc node dafny z3 "clang-${llvm_version}"; do
   command -v "${tool}" >/dev/null 2>&1 || missing+=("${tool}")
 done
 for f in "/usr/lib/llvm-${llvm_version}/lib/cmake/mlir/MLIRConfig.cmake" \

.github/actions/setup-language-toolchains/action.yml

@@ -53,6 +53,12 @@ runs:
         require_command tsc          "TypeScript backend integration lane"
         require_command node         "TypeScript backend integration lane"
 
+        # Dafny needs a solver as well as itself. Its NuGet package ships no
+        # native binaries, so a `dafny` that launches proves nothing about
+        # whether it can discharge an obligation -- check for z3 separately.
+        require_command dafny        "formal model check (spec/dafny)"
+        require_command z3           "SMT solver Dafny drives"
+
         require_command "clang-${llvm_version}" "sanitizer and fuzz lanes"
         require_file "/usr/lib/llvm-${llvm_version}/lib/cmake/mlir/MLIRConfig.cmake" \
                      "MLIR dev libraries (libmlir-${llvm_version}-dev)"

.github/workflows/ci.yml

@@ -3,16 +3,15 @@ name: CI
 # Full, unabridged test + report run for the core tools (dsdlc, dsdl-opt, dsdld)
 # across every supported host platform and every generated-output language.
 #
-# The Linux job runs INSIDE the project's own toolshed image
-# (ghcr.io/opencyphal/toolshed:ts26.4.1 — the same image .devcontainer uses), so
-# LLVM/MLIR 22, clang, cmake and ninja are already present: no per-run toolchain
-# install of LLVM. The setup action only adds what the image lacks (MLIR dev libs,
-# Go, Rust, tsc, lit). This job runs identically under `act` locally and on
-# GitHub-hosted runners.
-#
-# The integration suite registers a language's tests only when its toolchain is
-# found at configure time, so installing the full toolchain set is what makes the
-# run actually unabridged.
+# The container jobs run INSIDE the project's own toolshed image
+# (ghcr.io/opencyphal/toolshed:ts26.4.2 — the same image .devcontainer uses). That
+# image is the single source of truth for the build environment: LLVM/MLIR 22,
+# clang, cmake, ninja, the generated-output language toolchains, and Dafny with
+# its solver all come from it. Nothing is installed per run; the setup action
+# asserts the toolchains are present and fails loudly if one is missing, because
+# the integration suite registers a language's tests only when its toolchain is
+# found at configure time — so a silently incomplete image sheds whole lanes
+# while still reporting green.
 
 on:
   push:
@@ -36,7 +35,7 @@ jobs:
     name: Full suite (linux / toolshed)
     runs-on: ubuntu-26.04
     container:
-      image: ghcr.io/opencyphal/toolshed:ts26.4.1
+      image: ghcr.io/opencyphal/toolshed:ts26.4.2
     timeout-minutes: 120
     env:
       LLVM_DIR: /usr/lib/llvm-22/lib/cmake/llvm
@@ -167,7 +166,7 @@ jobs:
     # bounded on PRs (short -runs) and runs deep on the weekly schedule cron.
     runs-on: ubuntu-26.04
     container:
-      image: ghcr.io/opencyphal/toolshed:ts26.4.1
+      image: ghcr.io/opencyphal/toolshed:ts26.4.2
     timeout-minutes: 120
     env:
       LLVM_DIR: /usr/lib/llvm-22/lib/cmake/llvm
@@ -252,15 +251,32 @@ jobs:
     # LLVM/MLIR build matrix, so it is fast and cannot be skipped by a toolchain gap in
     # the heavy lanes.
     runs-on: ubuntu-26.04
+    # Dafny and its solver come from the toolshed image rather than being fetched
+    # per run.
+    container:
+      image: ghcr.io/opencyphal/toolshed:ts26.4.2
     timeout-minutes: 15
     steps:
       - name: Checkout
         uses: actions/checkout@v4
 
-      - name: Set up Dafny
-        uses: dafny-lang/setup-dafny-action@v1.7.0
-        with:
-          dafny-version: "4.11.0"
+      - name: Assert the Dafny toolchain
+        # Deliberately not the shared toolchain action: this lane is independent of
+        # the LLVM/MLIR build matrix and must not be taken down by a Go or
+        # TypeScript gap. It needs exactly two things, and Dafny's NuGet package
+        # ships no solver, so a `dafny` that launches proves nothing on its own.
+        run: |
+          set -uo pipefail
+          missing=()
+          for tool in dafny z3; do
+            command -v "${tool}" >/dev/null 2>&1 || missing+=("${tool}")
+          done
+          if [ "${#missing[@]}" -gt 0 ]; then
+            echo "::error::toolshed image is missing: ${missing[*]} — these belong in the image"
+            exit 1
+          fi
+          dafny --version
+          z3 --version
 
       - name: Verify CyphalSerdes
         # `dafny verify` exits non-zero on any failed proof obligation, so a broken model
@@ -284,7 +300,7 @@ jobs:
           submodules: recursive
 
       - name: Install LLVM/MLIR + ninja (Homebrew; links libc++)
-        # Pin to the toolshed image's LLVM major (ts26.4.1 -> 22) so the C backend
+        # Pin to the toolshed image's LLVM major (ts26.4.2 -> 22) so the C backend
         # (routed through MLIR/EmitC, whose text may vary across MLIR majors) stays
         # comparable. Prefer the versioned formula; fall back to `llvm` (which IS 22
         # while 22 is current). The assertion below is the real pin: a Homebrew

.github/workflows/coverage.yml

@@ -23,7 +23,7 @@ jobs:
     name: LLVM source coverage
     runs-on: ubuntu-26.04
     container:
-      image: ghcr.io/opencyphal/toolshed:ts26.4.1
+      image: ghcr.io/opencyphal/toolshed:ts26.4.2
     timeout-minutes: 120
     env:
       LLVM_DIR: /usr/lib/llvm-22/lib/cmake/llvm

CMakePresets.json

@@ -181,7 +181,23 @@
       "name": "test-ci-full",
       "displayName": "Test (ci full)",
       "inherits": "test-base",
-      "configurePreset": "ci"
+      "configurePreset": "ci",
+      "filter": {
+        "exclude": {
+          "label": "bench"
+        }
+      }
+    },
+    {
+      "name": "test-ci-bench",
+      "displayName": "Test (ci benchmarks)",
+      "inherits": "test-base",
+      "configurePreset": "ci",
+      "filter": {
+        "include": {
+          "label": "bench"
+        }
+      }
     },
     {
       "name": "test-ci-release-blocking",

spec/dafny/CyphalSerdes.dfy

@@ -884,6 +884,9 @@ module CyphalSerdes {
     assert [TokScal(8, 1), TokScal(8, 9)][..2] == [TokScal(8, 1), TokScal(8, 9)];
     assert DeCompat(TScal(8), [TokScal(8, 1), TokScal(8, 9)])
         == Some((Scal(8, 1), [TokScal(8, 9)]));
+    // The skipped-leftover case returns body[take..], not the inner reader's
+    // remainder. Without this the outer cursor's final position is opaque.
+    assert [TokScal(8, 1), TokScal(8, 9)][2..] == [];
     assert DeCompat(TScal(8), []) == Some((Scal(8, 0), []));
     var e: seq<Token> := [];
     assert [TScal(8)][1..] == [];

test/integration/RunPrimitiveEquivalence.cmake

@@ -67,10 +67,17 @@ file(WRITE "${go_dir}/go.mod"
   "replace github.com/thirtytwobits/llvm-dsdl/runtime/go => ${runtime_go}\n")
 file(COPY_FILE "${driver_dir}/PrimitiveEquivalenceDriver.go" "${go_dir}/main.go")
 set(go_bin "${go_dir}/go_primitive_driver")
+# -buildvcs=false because this module is written into the build tree, which sits
+# inside the repository: left to itself `go build` walks up, finds .git, and
+# stamps the driver with commit metadata. That consults git, and git refuses a
+# checkout owned by another user -- the ordinary situation in a CI container,
+# where it exits 128 and takes the build with it. The stamp is unwanted here
+# regardless: this is a throwaway test driver, and baking a commit hash into it
+# would make the binary differ between builds of identical source.
 execute_process(
   COMMAND "${CMAKE_COMMAND}" -E env
     "GOFLAGS=-mod=mod" "GOCACHE=${go_dir}/.gocache" "GOMODCACHE=${go_dir}/.gomodcache"
-    "${GO_EXECUTABLE}" build -o "${go_bin}" .
+    "${GO_EXECUTABLE}" build -buildvcs=false -o "${go_bin}" .
   WORKING_DIRECTORY "${go_dir}"
   RESULT_VARIABLE go_build_rc OUTPUT_VARIABLE go_build_out ERROR_VARIABLE go_build_err)
 if(NOT go_build_rc EQUAL 0)