Pin CI sibling checkouts; add rules_rocq_rust (e4660cc)

.github/workflows/ci.yml

@@ -12,6 +12,12 @@ concurrency:
 env:
   CARGO_TERM_COLOR: always
   RUST_BACKTRACE: 1
+  # Pinned sibling-repo commits — bumped explicitly via PR. Without these
+  # pins, unpinned `main` of relay/rivet can change tool behavior on this
+  # workflow with zero wohl code change (see #8 for the concrete
+  # incident that motivated pinning).
+  RELAY_REF: 4d42acf4a23c56980091f943c966ae5e0223a79f
+  RIVET_REF: 335bb84be0bb1be3768438ecec109c945c6b6530
 
 jobs:
   lint:
@@ -25,6 +31,7 @@ jobs:
         with:
           repository: pulseengine/relay
           path: relay
+          ref: ${{ env.RELAY_REF }}
       - uses: dtolnay/rust-toolchain@master
         with:
           toolchain: "1.85.0"
@@ -58,6 +65,7 @@ jobs:
         with:
           repository: pulseengine/relay
           path: relay
+          ref: ${{ env.RELAY_REF }}
       - uses: dtolnay/rust-toolchain@master
         with:
           toolchain: "1.85.0"
@@ -79,6 +87,7 @@ jobs:
         with:
           repository: pulseengine/relay
           path: relay
+          ref: ${{ env.RELAY_REF }}
       # Kani-verifier (the installer) needs newer Rust than our MSRV.
       # Kani itself uses an internal nightly for the proofs.
       - uses: dtolnay/rust-toolchain@stable
@@ -120,6 +129,7 @@ jobs:
         with:
           repository: pulseengine/relay
           path: relay
+          ref: ${{ env.RELAY_REF }}
       - uses: dtolnay/rust-toolchain@master
         with:
           toolchain: nightly
@@ -150,6 +160,7 @@ jobs:
         with:
           repository: pulseengine/rivet
           path: rivet
+          ref: ${{ env.RIVET_REF }}
       # rivet-cli's deps need Rust 1.89+; we don't care about MSRV for tooling.
       - uses: dtolnay/rust-toolchain@stable
       - uses: Swatinem/rust-cache@v2

MODULE.bazel

@@ -25,6 +25,20 @@ use_repo(verus, "verus_toolchains")
 
 register_toolchains("@verus_toolchains//:all")
 
+# ── rules_rocq_rust (Rocq theorem-proving rules) ────────────────────────
+# Pinned for reproducibility. wohl has no proofs/rocq/ yet, so the Rocq
+# toolchain extension is intentionally deferred — when rocq proofs land,
+# follow the rivet integration pattern (toolchain + nixpkgs + register).
+
+bazel_dep(name = "rules_rocq_rust", version = "0.1.0")
+
+git_override(
+    module_name = "rules_rocq_rust",
+    remote = "https://github.com/pulseengine/rules_rocq_rust.git",
+    # e4660cc: build: migrate rocq-of-rust to a hermetic rules_rust toolchain (#34).
+    commit = "e4660cc1b06fc4c0aefb49401fa2e2184cf804e3",
+)
+
 local_path_override(
     module_name = "rules_wasm_component",
     path = "../rules_wasm_component",