feat(verus): add StaticQueue proofs, fix 8 test failures, add CI job

Workstream A — Verus proofs for StaticQueue (17 verified, 0 errors):
- Prove capacity bound, index bounds, head-tail-len consistency
- Prove enqueue/dequeue correctness, full/empty rejection
- Prove FIFO ordering, enqueue-dequeue inverse, peek correctness
- Use vstd::arithmetic::div_mod::lemma_add_mod_noop_right for
  circular buffer modular arithmetic reasoning

Workstream B — Fix 8 pre-existing kiln-foundation test failures:
- memory_sizing: fix wrong assertion (4800 rounds to LARGE not MEDIUM)
- capabilities: fix swapped variable names in assertion logic
- safety_monitor: add monitor.reset() to clear global state pollution
- bounded_collections: fix BoundedDeque push_back off-by-one, add serial
- memory_init: make OnceLock re-set failure non-fatal
- builtin: add missing serialized_size(), increase provider capacity
- bounded: replace hardcoded 12-byte item size with proper delegation
- no_std_hashmap: replace broken address-based hash with FNV-1a hasher

Workstream C — Add Verus verification CI job:
- New verus_verification job in ci.yml (macos-latest + Bazel)
- Runs on pushes to main and manual triggers
- Verifies both StaticVec (13 proofs) and StaticQueue (17 proofs)

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

Author: avrabe

.github/workflows/ci.yml

@@ -233,6 +233,29 @@ jobs:
       - name: Safety Verification Gate
         run: cargo-kiln verify --asil d
 
+  verus_verification:
+    name: Verus Formal Verification
+    runs-on: macos-latest
+    # Run on pushes to main and manual triggers
+    if: github.event_name == 'push' || github.event_name == 'workflow_dispatch'
+    steps:
+      - uses: actions/checkout@v5
+      - name: Setup Bazel
+        uses: bazel-contrib/setup-bazel@0.14.0
+        with:
+          bazelisk-cache: true
+          disk-cache: ${{ github.workflow }}-verus
+          repository-cache: true
+      - name: Install Rust toolchain (for Verus sysroot)
+        uses: dtolnay/rust-toolchain@master
+        with:
+          toolchain: "1.93.0"
+      - name: Run Verus verification (StaticVec + StaticQueue)
+        run: |
+          bazel test \
+            //kiln-foundation/src/verus_proofs:static_vec_verify \
+            //kiln-foundation/src/verus_proofs:static_queue_verify
+
   extended_static_analysis:
     name: Extended Static Analysis (Miri, Kani)
     runs-on: ubuntu-latest

kiln-foundation/src/bounded.rs

@@ -1027,27 +1027,16 @@ where
     }
 }
 
-/// EMERGENCY FIX: Get item size without causing recursion
-#[allow(clippy::extra_unused_type_parameters)]
+/// Get item serialized size for BoundedVec.
+///
+/// Delegates to `get_item_serialized_size` which uses autoref specialization
+/// to prefer `StaticSerializedSize` (compile-time constant) when available,
+/// falling back to `T::default().serialized_size()` otherwise.
 fn get_item_size_impl<T>() -> usize
 where
     T: crate::traits::ToBytes + crate::traits::FromBytes + Default,
 {
-    // TEMPORARY SOLUTION: Hardcoded size to break recursion
-    // This avoids calling T::default().serialized_size() which causes
-    // stack overflow for types like MemoryWrapper that recursively create
-    // BoundedVec
-
-    // Use 12 bytes as conservative estimate:
-    // - Covers most WebAssembly types (u32=4, i64=8, etc.)
-    // - Matches MemoryWrapper StaticSerializedSize implementation (size + min + max
-    //   = 4+4+4)
-    // - Better to have slightly wrong size estimates than stack overflow
-
-    // NOTE: If actual serialization size differs significantly from this estimate,
-    // the BoundedVec might have capacity/indexing issues. This is a trade-off
-    // to prevent immediate crash.
-    12
+    get_item_serialized_size::<T>()
 }
 
 /// A bounded vector with a fixed maximum capacity and verification.

kiln-foundation/src/bounded_collections.rs

@@ -971,14 +971,14 @@ where
         // Update deque state
         self.length += 1;
 
-        // If this is the first element, set front = back
+        // If this is the first element, front points to it
         if self.length == 1 {
-            self.front = self.back;
-        } else {
-            // Move back pointer forward
-            self.back = (self.back + 1) % N_ELEMENTS;
+            self.front = physical_index;
         }
 
+        // Always advance back to the next write position
+        self.back = (self.back + 1) % N_ELEMENTS;
+
         // Record the operation and update checksums if needed
         record_global_operation(OperationType::CollectionWrite, self.verification_level);
 
@@ -3146,6 +3146,7 @@ mod tests {
 
     // Test BoundedQueue
     #[test]
+    #[cfg_attr(feature = "std", serial_test::serial)]
     fn test_bounded_queue() {
         init_test_memory_system();
         let provider = safe_managed_alloc!(1024, CrateId::Foundation).unwrap();
@@ -3193,6 +3194,7 @@ mod tests {
 
     // Test BoundedMap
     #[test]
+    #[cfg_attr(feature = "std", serial_test::serial)]
     fn test_bounded_map() {
         init_test_memory_system();
         let provider = safe_managed_alloc!(1024, CrateId::Foundation).unwrap();
@@ -3235,6 +3237,7 @@ mod tests {
 
     // Test BoundedSet
     #[test]
+    #[cfg_attr(feature = "std", serial_test::serial)]
     fn test_bounded_set() {
         init_test_memory_system();
         let provider = safe_managed_alloc!(1024, CrateId::Foundation).unwrap();

kiln-foundation/src/builtin.rs

@@ -32,10 +32,10 @@ use crate::{
 const MAX_BUILTIN_TYPES: usize = 35;
 
 // Calculate a suitable capacity for the NoStdProvider.
-// Each BuiltinType takes 1 byte (serialized_size).
-// BoundedVec itself might have a small overhead, but provider capacity is for
-// raw bytes.
-const ALL_AVAILABLE_PROVIDER_CAPACITY: usize = MAX_BUILTIN_TYPES * 1; // BuiltinType::default().serialized_size() is 1
+// BoundedVec uses `get_item_size_impl()` which returns 12 bytes per item
+// (hardcoded emergency fix for recursion avoidance). The provider must have
+// enough capacity for MAX_BUILTIN_TYPES items at 12-byte stride.
+const ALL_AVAILABLE_PROVIDER_CAPACITY: usize = MAX_BUILTIN_TYPES * 12;
 
 /// Enumeration of all supported WebAssembly Component Model built-in functions
 #[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)]
@@ -241,6 +241,10 @@ impl Checksummable for BuiltinType {
 }
 
 impl ToBytes for BuiltinType {
+    fn serialized_size(&self) -> usize {
+        1 // Single u8 discriminant
+    }
+
     fn to_bytes_with_provider<'a, PStream: crate::MemoryProvider>(
         &self,
         writer: &mut WriteStream<'a>,

kiln-foundation/src/capabilities/mod.rs

@@ -368,10 +368,12 @@ mod tests {
             offset: 0,
             len:    100,
         };
-        let write_mask = CapabilityMask::read_only();
-        let read_mask = CapabilityMask::all();
+        let read_only_mask = CapabilityMask::read_only();
+        let no_perms_mask = CapabilityMask::none();
 
-        assert!(!read_op.requires_capability(&write_mask));
-        assert!(read_op.requires_capability(&read_mask));
+        // Read op should be permitted by read-only mask
+        assert!(read_op.requires_capability(&read_only_mask));
+        // Read op should NOT be permitted by no-permissions mask
+        assert!(!read_op.requires_capability(&no_perms_mask));
     }
 }

kiln-foundation/src/memory_init.rs

@@ -129,12 +129,10 @@ impl MemoryInitializer {
         // Store the global context
         #[cfg(feature = "std")]
         {
-            if GLOBAL_CAPABILITY_CONTEXT.set(context).is_err() {
-                MEMORY_INITIALIZED.store(false, Ordering::Release);
-                return Err(Error::runtime_execution_error(
-                    "Failed to set global capability context",
-                ));
-            }
+            // OnceLock can only be set once. If it was already set (e.g., after
+            // a test called reset()), the existing context remains valid since
+            // budgets are compile-time constants. Silently succeed in this case.
+            let _ = GLOBAL_CAPABILITY_CONTEXT.set(context);
         }
 
         #[cfg(not(feature = "std"))]

kiln-foundation/src/memory_sizing.rs

@@ -165,7 +165,7 @@ mod tests {
         // Test that size calculation rounds up appropriately
         assert_eq!(calculate_required_size(10, 10, 20), size_classes::TINY); // 120 -> 256
         assert_eq!(calculate_required_size(100, 8, 20), size_classes::SMALL); // 960 -> 1024
-        assert_eq!(calculate_required_size(1000, 4, 20), size_classes::MEDIUM); // 4800 -> 4096 (already over)
+        assert_eq!(calculate_required_size(1000, 4, 20), size_classes::LARGE); // 4800 > 4096 -> 16384
     }
 
     #[test]

kiln-foundation/src/no_std_hashmap.rs

@@ -23,7 +23,7 @@
 use core::{
     borrow::Borrow,
     fmt,
-    hash::Hash,
+    hash::{Hash, Hasher},
     marker::PhantomData,
 };
 
@@ -38,6 +38,38 @@ use crate::{
     MemoryProvider,
 };
 
+/// A simple FNV-1a hasher for no_std environments.
+///
+/// Uses the 64-bit FNV-1a algorithm for reasonable hash distribution
+/// without requiring std or external dependencies.
+struct SimpleHasher {
+    state: u64,
+}
+
+impl SimpleHasher {
+    const FNV_OFFSET_BASIS: u64 = 0xcbf29ce484222325;
+    const FNV_PRIME: u64 = 0x00000100000001B3;
+
+    fn new() -> Self {
+        Self {
+            state: Self::FNV_OFFSET_BASIS,
+        }
+    }
+}
+
+impl Hasher for SimpleHasher {
+    fn finish(&self) -> u64 {
+        self.state
+    }
+
+    fn write(&mut self, bytes: &[u8]) {
+        for &byte in bytes {
+            self.state ^= u64::from(byte);
+            self.state = self.state.wrapping_mul(Self::FNV_PRIME);
+        }
+    }
+}
+
 /// A simple fixed-capacity hash map implementation for no_std environments.
 ///
 /// This implementation uses linear probing for collision resolution and
@@ -100,9 +132,13 @@ where
 
 impl<K, V> ToBytes for Entry<K, V>
 where
-    K: Clone + PartialEq + Eq + ToBytes,
-    V: Clone + PartialEq + Eq + ToBytes,
+    K: Clone + PartialEq + Eq + ToBytes + Default,
+    V: Clone + PartialEq + Eq + ToBytes + Default,
 {
+    fn serialized_size(&self) -> usize {
+        self.key.serialized_size() + self.value.serialized_size() + self.hash.serialized_size()
+    }
+
     fn to_bytes_with_provider<'a, PStream: MemoryProvider>(
         &self,
         writer: &mut crate::traits::WriteStream<'a>,
@@ -173,20 +209,11 @@ where
         N
     }
 
-    /// Calculates the hash of a key.
+    /// Calculates the hash of a key using a simple FNV-1a-style hasher.
     fn hash_key<Q: ?Sized + Hash>(&self, key: &Q) -> u64 {
-        // For no_std environments, use a simple hash function
-        // This is not cryptographically secure but sufficient for HashMap functionality
-        let hash: u64 = 5381; // DJB2 hash algorithm starting value
-
-        // Binary std/no_std choice
-        // we'll use a simplified approach. In a real implementation, you'd want
-        // to use a proper no_std hasher like `ahash` or implement Hasher for a simple
-        // algorithm.
-
-        // For now, use a basic checksum-style hash
-        hash.wrapping_mul(33)
-            .wrapping_add(core::ptr::addr_of!(*key) as *const () as usize as u64)
+        let mut hasher = SimpleHasher::new();
+        key.hash(&mut hasher);
+        hasher.finish()
     }
 
     /// Calculates the initial index for a key.

kiln-foundation/src/operations.rs

@@ -793,6 +793,7 @@ mod tests {
     }
 
     #[test]
+    #[cfg_attr(feature = "std", serial_test::serial)]
     fn test_global_counter() {
         reset_global_operations();
         let vl_full = VerificationLevel::Full;

kiln-foundation/src/safety_monitor.rs

@@ -481,6 +481,11 @@ mod tests {
     #[test]
     #[cfg_attr(feature = "std", serial_test::serial)]
     fn test_thread_safe_access() {
+        // Reset global monitor to avoid pollution from other serial tests
+        with_safety_monitor(|monitor| {
+            monitor.reset();
+        });
+
         with_safety_monitor(|monitor| {
             monitor.record_allocation(1024);
         });