chore: M2 ROADMAP + M3 doc-TODO sweep + M4 dep+action SHA refresh (#68)

* chore: M2 ROADMAP + M3 doc-TODO sweep + M4 dep+action SHA refresh

M2 — ROADMAP.adoc refresh against closed Phase-0 issues:
  * Marked #49 (Coq verify-proofs CI re-enabled) DONE via PR #55.
  * Marked single_op_reversible admit DONE via PR #55 (3 new admits
    surfaced as #56/#57/#58 and tracked).
  * Added "Closed-issue housekeeping (2026-06-01)" section grouping
    #33 / #44 / #46 / #49 closures with their landing PRs.
  * Added "Last refreshed: 2026-06-01" stamp.
  * Linked open #41 / #42 / #43 / #45 / #51 / #56-58 from relevant
    bullets to keep ROADMAP and issue tracker in sync.

M3 — doc TODO sweep (81 markers -> 74, net -7):
  * Replaced bare "(TODO)" status notes with "(tracked under #N)"
    backlinks across 10 docs (UX_IMPROVEMENTS_ROADMAP, ECHIDNA_INTEGRATION,
    ARCHITECTURE, ARCHITECTURE_DIAGRAMS, LEAN4_RUST_CORRESPONDENCE,
    docs/README, PHASE6_M11_COMPLETE).
  * Added top-of-doc maintenance-note headers to V1_TESTING_CHECKLIST.md
    and SEAM_ANALYSIS_AND_IDRIS2_PLAN.md citing #43 / ROADMAP v2.0 so
    the dozens of "❌ TODO" status-table cells are unambiguously
    tracked rather than read as fresh debt.
  * Reframed "Design Complete, Implementation TODO" status lines in
    EXTRACTION_SUMMARY.md + OCAML_EXTRACTION.md as "Implementation
    Pending (ROADMAP v2.0)" with 2026-06-01 review stamp.
  * Intentional pedagogical TODOs in Coq snippets (INTEGRATION_SUMMARY,
    INTEGRATION.md, PROOF-NARRATIVE), historical-changelog mentions,
    and quoted-shell-example text were preserved.

M4 — dep + GH Actions SHA refresh:
  * `cargo update` in impl/rust-cli/: 30 patch-version bumps + 3 new
    transitives (futures-{core,task,util}, slab). No semver-major
    changes; shlex stays at 1.3.x. cargo check --workspace clean.
  * GH Actions SHA bumps (all verified live via gh api):
    - actions/checkout: de0fac2 / b4ffde6 / 34e1148 -> 1cce339
    - actions/cache: 6682284 -> 27d5ce7
    - actions/upload-artifact: bbbca2d -> 043fb46
    - Swatinem/rust-cache: c193711 / bc18602 -> 8ba370a
    - github/codeql-action/{init,analyze,upload-sarif}: c6f9311 -> 2a1689e
    - ossf/scorecard-action: 4eaacf0 -> af76153
  * dtolnay/rust-toolchain pins (stable + nightly-2026-03-27)
    deliberately left — pinned to dated nightly for reproducibility.
  * No [patch.crates-io] in workspace; nothing to prune.

Echo-types audit: NOT RELEVANT (pure maintenance, no L3-echo / L1-region
obligations); recorded here per estate convention.

Verify: cargo check --workspace clean (25 pre-existing warnings, 0 errors).

* fixup: revert codeql-action SHA bump (newer version regressed no-source-seen)

Bumping github/codeql-action from c6f9311 -> 2a1689e in PR #68's M4
track caused `analyze (javascript-typescript, none)` to fail with
"CodeQL could not process any code written in JavaScript/TypeScript"
where it previously succeeded on main.

The repo is Rust-primary; the JS/TS leg is intentionally a no-op
existence check that the older action treated as benign but the
newer action rejects as a fatal error.

Reverting codeql/{init,analyze,upload-sarif} to c6f9311 only; the
other 6 action SHA bumps (checkout, cache, upload-artifact, rust-cache,
scorecard-action) remain at HEAD. Will file a follow-up issue to
either (a) bump codeql with a build-mode that accepts empty JS/TS,
or (b) drop the JS/TS leg entirely from codeql.yml.

* fixup: hold back actions/checkout SHA in codeql.yml to match main (per #71)

Even with codeql-action reverted to c6f9311, the bumped
actions/checkout@1cce339 still triggers "no JS/TS source code seen"
on the analyze step. main with checkout@de0fac2 + same CodeQL bundle
2.25.5 succeeds. Hold checkout back ONLY in codeql.yml until #71 is
resolved (either drop the JS/TS analyze leg or move to a richer
build-mode).

All other workflows keep the actions/checkout@1cce339 bump.

Author: hyperpolymath

.github/workflows/boj-build.yml

@@ -9,7 +9,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout
-        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+        uses: actions/checkout@1cce3390c2bfda521930d01229c073c7ff920824 # v6.0.2
       - name: Trigger BoJ Server (Casket/ssg-mcp)
         run: |
           # Send a secure trigger to boj-server to build this repository

.github/workflows/casket-pages.yml

@@ -20,10 +20,10 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout
-        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v4
+        uses: actions/checkout@1cce3390c2bfda521930d01229c073c7ff920824 # v4
 
       - name: Checkout casket-ssg
-        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v4
+        uses: actions/checkout@1cce3390c2bfda521930d01229c073c7ff920824 # v4
         with:
           repository: hyperpolymath/casket-ssg
           path: .casket-ssg
@@ -35,7 +35,7 @@ jobs:
           cabal-version: '3.10'
 
       - name: Cache Cabal
-        uses: actions/cache@668228422ae6a00e4ad889ee87cd7109ec5666a7 # v4
+        uses: actions/cache@27d5ce7f107fe9357f9df03efb73ab90386fccae # v4
         with:
           path: |
             ~/.cabal/packages

.github/workflows/cflite_batch.yml

@@ -24,7 +24,7 @@ jobs:
         sanitizer: [address, undefined, memory]
     steps:
       - name: Checkout code
-        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v4
+        uses: actions/checkout@1cce3390c2bfda521930d01229c073c7ff920824 # v4
 
       - name: Build fuzzers (${{ matrix.sanitizer }})
         id: build
@@ -52,7 +52,7 @@ jobs:
 
       - name: Upload corpus
         if: always()
-        uses: actions/upload-artifact@bbbca2ddaa5d8feaa63e36b76fdaad77386f024f # v7
+        uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7
         with:
           name: fuzz-corpus-${{ matrix.sanitizer }}
           path: build/corpus

.github/workflows/cflite_pr.yml

@@ -25,7 +25,7 @@ jobs:
         sanitizer: [address, undefined]
     steps:
       - name: Checkout code
-        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v4
+        uses: actions/checkout@1cce3390c2bfda521930d01229c073c7ff920824 # v4
 
       - name: Build fuzzers (${{ matrix.sanitizer }})
         id: build

.github/workflows/codeql.yml

@@ -35,7 +35,7 @@ jobs:
 
     steps:
       - name: Checkout
-        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 (held back per #71)
 
       - name: Initialize CodeQL
         uses: github/codeql-action/init@c6f931105cb2c34c8f901cc885ba1e2e259cf745 # v3

.github/workflows/compilation_tests.yml

@@ -43,27 +43,27 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v4
+        uses: actions/checkout@1cce3390c2bfda521930d01229c073c7ff920824 # v4
 
       - name: Install Rust ${{ matrix.rust }}
         uses: dtolnay/rust-toolchain@6d9817901c499d6b02debbb57edb38d33daa680b
         with:
           toolchain: ${{ matrix.rust }}
 
       - name: Cache cargo registry
-        uses: actions/cache@668228422ae6a00e4ad889ee87cd7109ec5666a7 # v4
+        uses: actions/cache@27d5ce7f107fe9357f9df03efb73ab90386fccae # v4
         with:
           path: ~/.cargo/registry
           key: ${{ runner.os }}-cargo-registry-${{ hashFiles('**/Cargo.lock') }}
 
       - name: Cache cargo index
-        uses: actions/cache@668228422ae6a00e4ad889ee87cd7109ec5666a7 # v4
+        uses: actions/cache@27d5ce7f107fe9357f9df03efb73ab90386fccae # v4
         with:
           path: ~/.cargo/git
           key: ${{ runner.os }}-cargo-index-${{ hashFiles('**/Cargo.lock') }}
 
       - name: Cache cargo build
-        uses: actions/cache@668228422ae6a00e4ad889ee87cd7109ec5666a7 # v4
+        uses: actions/cache@27d5ce7f107fe9357f9df03efb73ab90386fccae # v4
         with:
           path: impl/rust-cli/target
           key: ${{ runner.os }}-cargo-build-${{ matrix.rust }}-${{ hashFiles('**/Cargo.lock') }}
@@ -94,7 +94,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout code
-        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v4
+        uses: actions/checkout@1cce3390c2bfda521930d01229c073c7ff920824 # v4
 
       - name: Install Rust 1.70.0
         uses: dtolnay/rust-toolchain@6d9817901c499d6b02debbb57edb38d33daa680b
@@ -122,7 +122,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v4
+        uses: actions/checkout@1cce3390c2bfda521930d01229c073c7ff920824 # v4
 
       - name: Install Rust stable
         uses: dtolnay/rust-toolchain@6d9817901c499d6b02debbb57edb38d33daa680b
@@ -156,7 +156,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v4
+        uses: actions/checkout@1cce3390c2bfda521930d01229c073c7ff920824 # v4
 
       - name: Install Rust stable
         uses: dtolnay/rust-toolchain@6d9817901c499d6b02debbb57edb38d33daa680b
@@ -180,7 +180,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout code
-        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v4
+        uses: actions/checkout@1cce3390c2bfda521930d01229c073c7ff920824 # v4
 
       - name: Install Rust stable with clippy & rustfmt
         uses: dtolnay/rust-toolchain@6d9817901c499d6b02debbb57edb38d33daa680b
@@ -205,7 +205,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout code
-        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v4
+        uses: actions/checkout@1cce3390c2bfda521930d01229c073c7ff920824 # v4
 
       - name: Install Rust stable
         uses: dtolnay/rust-toolchain@6d9817901c499d6b02debbb57edb38d33daa680b
@@ -240,7 +240,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v4
+        uses: actions/checkout@1cce3390c2bfda521930d01229c073c7ff920824 # v4
 
       - name: Install Rust stable
         uses: dtolnay/rust-toolchain@6d9817901c499d6b02debbb57edb38d33daa680b
@@ -253,7 +253,7 @@ jobs:
         run: cargo build --release --target ${{ matrix.target }}
 
       - name: Upload artifact
-        uses: actions/upload-artifact@bbbca2ddaa5d8feaa63e36b76fdaad77386f024f # v7
+        uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7
         with:
           name: ${{ matrix.artifact }}
           path: impl/rust-cli/target/${{ matrix.target }}/release/vsh${{ matrix.os == 'windows-latest' && '.exe' || '' }}

.github/workflows/dogfood-gate.yml

@@ -25,7 +25,7 @@ jobs:
 
     steps:
       - name: Checkout repository
-        uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4
+        uses: actions/checkout@1cce3390c2bfda521930d01229c073c7ff920824 # v4
 
       - name: Check for A2ML files
         id: detect
@@ -69,7 +69,7 @@ jobs:
 
     steps:
       - name: Checkout repository
-        uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4
+        uses: actions/checkout@1cce3390c2bfda521930d01229c073c7ff920824 # v4
 
       - name: Check for K9 files
         id: detect
@@ -118,7 +118,7 @@ jobs:
 
     steps:
       - name: Checkout repository
-        uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4
+        uses: actions/checkout@1cce3390c2bfda521930d01229c073c7ff920824 # v4
 
       - name: Scan for invisible characters
         id: lint
@@ -182,7 +182,7 @@ jobs:
 
     steps:
       - name: Checkout repository
-        uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4
+        uses: actions/checkout@1cce3390c2bfda521930d01229c073c7ff920824 # v4
 
       - name: Check for Groove manifest
         id: groove
@@ -240,7 +240,7 @@ jobs:
 
     steps:
       - name: Checkout repository
-        uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4
+        uses: actions/checkout@1cce3390c2bfda521930d01229c073c7ff920824 # v4
 
       - name: Check and validate eclexiaiser manifest
         id: eclex
@@ -321,7 +321,7 @@ jobs:
 
     steps:
       - name: Checkout repository
-        uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4
+        uses: actions/checkout@1cce3390c2bfda521930d01229c073c7ff920824 # v4
 
       - name: Generate dogfooding scorecard
         run: |

.github/workflows/echidna-validation.yml

@@ -25,15 +25,15 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout code
-        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd  # v6.0.2
+        uses: actions/checkout@1cce3390c2bfda521930d01229c073c7ff920824  # v6.0.2
 
       - name: Install Rust toolchain
         uses: dtolnay/rust-toolchain@4be9e76fd7c4901c61fb841f559994984270fce7  # stable
         with:
           components: rustfmt, clippy
 
       - name: Cache Rust dependencies
-        uses: Swatinem/rust-cache@c19371144df3bb44fab255c43d04cbc2ab54d1c4  # v2
+        uses: Swatinem/rust-cache@8ba370a7908a18ecf2b2aa574dbfdf4e4e50514c  # v2
         with:
           workspaces: impl/rust-cli
 
@@ -57,13 +57,13 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout code
-        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd  # v6.0.2
+        uses: actions/checkout@1cce3390c2bfda521930d01229c073c7ff920824  # v6.0.2
 
       - name: Install Rust toolchain
         uses: dtolnay/rust-toolchain@4be9e76fd7c4901c61fb841f559994984270fce7  # stable
 
       - name: Cache Rust dependencies
-        uses: Swatinem/rust-cache@c19371144df3bb44fab255c43d04cbc2ab54d1c4  # v2
+        uses: Swatinem/rust-cache@8ba370a7908a18ecf2b2aa574dbfdf4e4e50514c  # v2
         with:
           workspaces: impl/rust-cli
 

.github/workflows/generator-generic-ossf-slsa3-publish.yml

@@ -27,7 +27,7 @@ jobs:
       digests: ${{ steps.hash.outputs.digests }}
 
     steps:
-      - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6
+      - uses: actions/checkout@1cce3390c2bfda521930d01229c073c7ff920824 # v6
 
       # ========================================================
       #

.github/workflows/hypatia-scan.yml

@@ -46,7 +46,7 @@ jobs:
 
     steps:
       - name: Checkout repository
-        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+        uses: actions/checkout@1cce3390c2bfda521930d01229c073c7ff920824 # v6.0.2
         with:
           fetch-depth: 0  # Full history for better pattern analysis