Fix derived-namespace propagation and computed enum reverse maps

.github/workflows/ci.yml

@@ -49,11 +49,34 @@ jobs:
       - name: Clippy
         run: cargo clippy --workspace --all-targets --locked -- -D warnings
 
+      # The workspace guard shells out to `cargo metadata --offline`,
+      # which resolves the graph for every target and so needs crates
+      # this host build never downloads. `cargo fetch` without `--target`
+      # gets all of them, matching the Formal job's G0 ledger step.
+      - name: Fetch dependencies for all targets
+        run: cargo fetch --locked
+
       - name: Fetch pinned TypeScript test fixtures
         run: >-
           cargo run --locked -p bamts-verification -- source fetch
           typescript-primary-tests --dest target/authority/typescript-7.0.2-tests
 
+      # `cargo test --workspace` covers authority, oracle-pin, and formal
+      # bridge tests that read `node_modules/typescript/package.json` and
+      # drive a local Quint. Without these the step fails on a missing
+      # toolchain rather than on a real defect.
+      - name: Setup Node
+        uses: actions/setup-node@49933ea5288caeca8642d1e84afbd3f7d6820020 # v4
+        with:
+          node-version: 24.18.0
+          package-manager-cache: false
+
+      - name: Install npm dependencies
+        run: npm ci
+
+      - name: Install Quint
+        run: npm ci --prefix formal/quint
+
       - name: Test workspace
         run: cargo test --workspace --locked
 
@@ -189,6 +212,12 @@ jobs:
           rustup toolchain install "$TOOLCHAIN" --profile minimal --component rustfmt,clippy,rust-src
           rustup default "$TOOLCHAIN"
 
+      # `ledger verify` shells out to `cargo metadata --offline`, which
+      # resolves the graph for every target and so needs crates the host
+      # build never downloads. `cargo fetch` without `--target` gets all.
+      - name: Fetch dependencies for all targets
+        run: cargo fetch --locked
+
       - name: G0 ledger
         run: cargo run --locked -p bamts-verification --bin bamts-verification -- ledger verify --gate G0
 
@@ -228,6 +257,18 @@ jobs:
         run: cargo run --locked -p bamts-verification --bin ts_conformance -- sync --verify-pin --write-snapshot
       - name: Build compiler lane worker
         run: cargo build --locked --release -p bamts-verification --bin ts_lane_worker
+      # `suite run` hashes the locked authority markers under
+      # target/authority. The typescript-7.0.2 catalog reads both the
+      # compiler tree and the test tree, so both must be materialized
+      # or the receipt step fails with E_TOOL_MISSING.
+      - name: Fetch pinned TypeScript compiler authority
+        run: >-
+          cargo run --locked -p bamts-verification -- source fetch
+          typescript-7-compiler --dest target/authority/typescript-7.0.2
+      - name: Fetch pinned TypeScript test authority
+        run: >-
+          cargo run --locked -p bamts-verification -- source fetch
+          typescript-primary-tests --dest target/authority/typescript-7.0.2-tests
       - name: Write strict conformance receipt
         env:
           BAMTS_SUITE_COMPILER_ADAPTER: target/release/ts_lane_worker
@@ -285,6 +326,17 @@ jobs:
           merge-multiple: true
       - name: Build compiler lane worker
         run: cargo build --locked --release -p bamts-verification --bin ts_lane_worker
+      # `suite merge` recomputes the run binding, whose authority digest
+      # reads both markers under target/authority. The receipts artifact
+      # carries only JSONL, so this clean runner must materialize them too.
+      - name: Fetch pinned TypeScript compiler authority
+        run: >-
+          cargo run --locked -p bamts-verification -- source fetch
+          typescript-7-compiler --dest target/authority/typescript-7.0.2
+      - name: Fetch pinned TypeScript test authority
+        run: >-
+          cargo run --locked -p bamts-verification -- source fetch
+          typescript-primary-tests --dest target/authority/typescript-7.0.2-tests
       - name: Merge complete compatible matrix
         env:
           BAMTS_SUITE_COMPILER_ADAPTER: target/release/ts_lane_worker

.github/workflows/nightly.yml

@@ -95,6 +95,18 @@ jobs:
         run: cargo run --locked -p bamts-verification --bin ts_conformance -- sync --verify-pin --write-snapshot
       - name: Build compiler lane worker
         run: cargo build --locked --release -p bamts-verification --bin ts_lane_worker
+      # `suite run` hashes the locked authority markers under
+      # target/authority. The typescript-7.0.2 catalog reads both the
+      # compiler tree and the test tree, so both must be materialized
+      # or the receipt step fails with E_TOOL_MISSING.
+      - name: Fetch pinned TypeScript compiler authority
+        run: >-
+          cargo run --locked -p bamts-verification -- source fetch
+          typescript-7-compiler --dest target/authority/typescript-7.0.2
+      - name: Fetch pinned TypeScript test authority
+        run: >-
+          cargo run --locked -p bamts-verification -- source fetch
+          typescript-primary-tests --dest target/authority/typescript-7.0.2-tests
       - name: Write strict nightly receipt
         env:
           BAMTS_SUITE_COMPILER_ADAPTER: target/release/ts_lane_worker
@@ -148,6 +160,17 @@ jobs:
           merge-multiple: true
       - name: Build compiler lane worker
         run: cargo build --locked --release -p bamts-verification --bin ts_lane_worker
+      # `suite merge` recomputes the run binding, whose authority digest
+      # reads both markers under target/authority. The receipts artifact
+      # carries only JSONL, so this clean runner must materialize them too.
+      - name: Fetch pinned TypeScript compiler authority
+        run: >-
+          cargo run --locked -p bamts-verification -- source fetch
+          typescript-7-compiler --dest target/authority/typescript-7.0.2
+      - name: Fetch pinned TypeScript test authority
+        run: >-
+          cargo run --locked -p bamts-verification -- source fetch
+          typescript-primary-tests --dest target/authority/typescript-7.0.2-tests
       - name: Merge complete compatible matrix
         env:
           BAMTS_SUITE_COMPILER_ADAPTER: target/release/ts_lane_worker
@@ -359,6 +382,12 @@ jobs:
           rustup toolchain install "$TOOLCHAIN" --profile minimal --component rustfmt,clippy,rust-src
           rustup default "$TOOLCHAIN"
 
+      # `ledger verify` shells out to `cargo metadata --offline`, which
+      # resolves the graph for every target and so needs crates the host
+      # build never downloads. `cargo fetch` without `--target` gets all.
+      - name: Fetch dependencies for all targets
+        run: cargo fetch --locked
+
       - name: G0 ledger
         run: cargo run --locked -p bamts-verification --bin bamts-verification -- ledger verify --gate G0
 

crates/bamts-cli/src/api_server/mod.rs

@@ -11,6 +11,7 @@ use std::io::{self, Write};
 use std::os::fd::AsFd;
 use std::sync::Arc;
 use std::thread;
+use std::time::Duration;
 
 use control::{Control, ControlKind, Inbound, Next, REAP_DEADLINE, ReaderExit};
 use reader::reader_main;
@@ -145,6 +146,15 @@ where
 
     control.stop();
     let _ = waker.wake();
+    // `shutdown` ends the loop by design, and the drain owes a terminal
+    // response to work the transport already carried. Reaping the reader
+    // first is what makes that set well defined: without it the loop can
+    // break while the next frame is still being parsed, and that request
+    // leaves unanswered depending only on thread scheduling. One wait
+    // serves both the drain and the join below, so a reader that never
+    // exits costs the deadline once. A reader that cannot be woken keeps
+    // the existing orphan path rather than stalling shutdown at all.
+    let reader_reaped = I::Waker::REAPABLE && control.wait_reaped(REAP_DEADLINE);
     for inbound in control.drain() {
         match inbound {
             Inbound::Work {
@@ -168,7 +178,14 @@ where
         }
     }
 
-    let reaped = if I::Waker::REAPABLE && control.wait_reaped(REAP_DEADLINE) {
+    // A reader that exits while the drain is writing its responses still
+    // owes its terminal error, so re-read the state once the drain is
+    // done. A zero deadline reads without waiting again, which keeps the
+    // single bounded wait above.
+    let reader_reaped =
+        reader_reaped || (I::Waker::REAPABLE && control.wait_reaped(Duration::ZERO));
+
+    let reaped = if reader_reaped {
         Reaped::Joined(
             reader
                 .join()

crates/bamts-cli/src/driver.rs

@@ -2879,27 +2879,30 @@ printf started > link-started
         let cancel = CancellationToken::new();
         let trigger = cancel.clone();
         let marker = directory.join("link-started");
+        // Wait for the linker to actually start rather than for a fixed
+        // slice of wall clock: a loaded runner can take longer to spawn
+        // the process than a short deadline allows. The cap only breaks a
+        // genuine hang, and the returned instant dates the cancel so the
+        // bound below measures cancellation, not process startup.
         let canceller = thread::spawn(move || {
-            let deadline = Instant::now() + Duration::from_secs(2);
+            let deadline = Instant::now() + Duration::from_secs(60);
             while !marker.is_file() && Instant::now() < deadline {
                 thread::sleep(Duration::from_millis(5));
             }
             let started = marker.is_file();
             trigger.cancel();
-            started
+            started.then(Instant::now)
         });
 
-        let started = Instant::now();
         let error = link_executable(&[], &directory.join("output"), &context, &cancel)
             .expect_err("cancelled linker must fail as cancellation");
         assert!(matches!(error, DriverError::Cancelled));
+        let cancelled_at = canceller
+            .join()
+            .expect("link cancellation thread completes")
+            .expect("the linker must start before it is cancelled");
         assert!(
-            canceller
-                .join()
-                .expect("link cancellation thread completes")
-        );
-        assert!(
-            started.elapsed() < Duration::from_secs(3),
+            cancelled_at.elapsed() < Duration::from_secs(3),
             "managed link cancellation must be bounded"
         );
         fs::remove_dir_all(directory)?;