feat(verus): verified StaticVec proofs pass via Bazel — 13 verified, 0 errors

Update the Verus proof model to use proof-mode operations throughout,
matching the verified pattern that passes rust_verify. Add Bazel
integration via MODULE.bazel and BUILD.bazel targets.

Key changes:
- All operations (new, push, pop, clear) are proof fn, not exec fn,
  since the model exists purely for verification
- Ghost fields use direct assignment in proof mode (no Ghost wrapper)
- Arithmetic casts with `as usize` for proof-mode int→usize conversion
- MODULE.bazel pins rules_verus with rust_verify direct invocation
- BUILD.bazel defines verus_test target for CI integration
- .gitignore updated for Bazel output directories

Verified properties (all unbounded — proved for ALL inputs):
1. Capacity invariant: len <= N always maintained
2. Push correctness: appends exactly one element
3. Push-full rejection: returns Err without mutation
4. Pop correctness: returns last pushed element (LIFO)
5. Push-pop inverse: push(x); pop() restores original state
6. Get bounds safety: get(i) returns Some iff i < len
7. Clear correctness: empties vector, preserves well-formedness
8. Length bounded by capacity: core ASIL-D invariant

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Author: avrabe

.gitignore

@@ -48,6 +48,13 @@ docs_output/
 .cursorignore
 *.rlib
 
+# Bazel build system
+/bazel-bin
+/bazel-out
+/bazel-testlogs
+/bazel-wrt2
+MODULE.bazel.lock
+
 # Temporary test files
 *.log
 /test_*.wat

BUILD.bazel

@@ -0,0 +1,2 @@
+# Root BUILD file for Kiln
+# Verus verification targets are in kiln-foundation/src/verus_proofs/

MODULE.bazel

@@ -0,0 +1,19 @@
+module(
+    name = "kiln",
+    version = "0.2.0",
+)
+
+# Verus verification toolchain
+bazel_dep(name = "rules_verus", version = "0.1.0")
+
+git_override(
+    module_name = "rules_verus",
+    remote = "https://github.com/pulseengine/rules_verus.git",
+    commit = "e2c1600a8cca4c0deb78c5fcb4a33f1da2273d29",
+)
+
+verus = use_extension("@rules_verus//verus:extensions.bzl", "verus")
+verus.toolchain(version = "0.2026.02.15")
+use_repo(verus, "verus_toolchains")
+
+register_toolchains("@verus_toolchains//:all")

kiln-foundation/src/verus_proofs/BUILD.bazel

@@ -0,0 +1,22 @@
+load("@rules_verus//verus:defs.bzl", "verus_library", "verus_test")
+
+verus_library(
+    name = "static_vec_proofs",
+    srcs = [
+        "mod.rs",
+        "static_vec_proofs.rs",
+    ],
+    crate_root = "static_vec_proofs.rs",
+    crate_name = "static_vec_proofs",
+    visibility = ["//visibility:public"],
+)
+
+verus_test(
+    name = "static_vec_verify",
+    srcs = [
+        "mod.rs",
+        "static_vec_proofs.rs",
+    ],
+    crate_root = "static_vec_proofs.rs",
+    crate_name = "static_vec_proofs",
+)