feat: full Verus pipeline — verify + strip with hermetic sysroot (#77)

rules_verus 8a2bbf6: hermetic Rust sysroot, no rustup needed.

Both targets pass:
- verus_library: SMT verification (6 proofs verified)
- verus_strip: strips annotations → plain Rust for coq-of-rust

Pipeline: Verus specs → Z3 verify → strip → plain Rust → coq-of-rust → Rocq

Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Author: avrabe

MODULE.bazel

@@ -112,7 +112,7 @@ bazel_dep(name = "rules_verus", version = "0.1.0")
 
 git_override(
     module_name = "rules_verus",
-    commit = "e2c1600",
+    commit = "8a2bbf6",
     remote = "https://github.com/pulseengine/rules_verus.git",
 )
 

src/lib/src/verus_proofs/BUILD.bazel

@@ -1,6 +1,8 @@
-load("@rules_verus//verus:defs.bzl", "verus_library", "verus_test")
+load("@rules_verus//verus:defs.bzl", "verus_library", "verus_strip", "verus_test")
+
+# ── Track 1: Verus SMT verification (CV-20, CV-21, CV-22) ──────────
+# Fully hermetic — bundled Rust sysroot, no rustup needed.
 
-# Merkle tree inclusion proof soundness (CV-20) and anti-rollback (CV-21)
 verus_library(
     name = "wsc_merkle_proofs",
     srcs = [
@@ -23,3 +25,15 @@ verus_test(
     crate_root = "mod.rs",
     crate_name = "wsc_verus_proofs",
 )
+
+# ── Track 2: Strip Verus → plain Rust for coq-of-rust pipeline ─────
+
+verus_strip(
+    name = "wsc_proofs_stripped",
+    srcs = [
+        "mod.rs",
+        "merkle_proofs.rs",
+        "dsse_proofs.rs",
+    ],
+    visibility = ["//visibility:public"],
+)