[vxfemboy]

Summary

Implements Phase 2 of the verification and optimization architecture as specified in docs/superpowers/plans/2026-11-13-phase2-zero-copy-and-formal-verification.md:

1. Ingress Zero-Copy AEAD Decryption (perf(crypto): in-place zero-copy AEAD decryption via open_into for dataplane ingress #209):

   • Migrated dataplane packet ingress to use yip_wire::FrameRef and Codec::deframe_borrowed.
   • Reused pre-allocated scratch buffers (inner_scratch and control_scratch) with Session::open_into for zero heap allocations on ingress hotpaths.
   • Verified under assert_no_alloc! in bin/yipd/tests/ingress_zero_alloc_test.rs.

2. Zero-Allocation Transmit Scratch Arena for FecEncoder (perf(transport): zero-allocation scratch arena for FecEncoder on packet transmit path #208):

   • Introduced FecScratchArena with pre-allocated shard buffers and reusable Symbol records.
   • Slices systematic symbols directly from input ciphertext and computes Reed-Solomon repair rows in-place via repair_row_into and encode_repair_into in crates/yip-transport/src/rs.rs.
   • Verified under assert_no_alloc! in crates/yip-transport/tests/fec_zero_alloc_test.rs.

3. Bounded Circular ObjectTable & Zero-Copy Repair Buffering (perf(transport): zero-copy repair shard buffering and circular ring-buffer ObjectTable for FEC reassembler #213):

   • Replaced backward-shift open addressing in ObjectTable with candidate-associative bounded buckets (4 ways, max 2 candidate buckets), ensuring O(1) worst-case lookup, insert, and eviction without cascades or memory leaks.
   • Replaced per-shard cloning in ObjState with reusable buffer pooling and stack-allocated repair reference slices in FecReassembler.
   • Verified zero heap allocations under steady-state churn (10,000 objects) in crates/yip-transport/tests/object_table_test.rs.

4. O(1) Tail-Eviction MacTable Sweep & Monotonic SentLog Accounting (perf(dataplane): O(1) tail-eviction MAC table sweep and monotonic binary search for SentLog accounting #214):

   • Replaced allocating hash scan in MacTable::sweep with O(k) tail eviction using pre-allocated slab free capacity.
   • Optimized SentLog::count_classes_in_range with partition_point binary search across VecDeque ring slices.
   • Verified in bin/yipd/tests/mac_table_sweep_test.rs.

5. Loom Weak-Memory SPSC Concurrency Verification:

   • Instrumented crates/yip-io/src/spsc.rs under #[cfg(loom)] with conditional atomic and UnsafeCell abstractions.
   • Added exhaustive permutation tests in crates/yip-io/tests/loom_spsc.rs and added a dedicated Loom verification step in CI workflows.

6. Miri Strict-Provenance & Kani Symbolic Verification:

   • Created crates/yip-transport/src/rs_simd_kani.rs with Kani symbolic proofs and 65,536 exhaustive test cases verifying SIMD Galois Field equivalence against scalar gf256::mul.
   • Guarded FFI syscalls in crates/yip-verify/src/syscall.rs under not(miri).
   • Added Miri strict-provenance CI gate (-Zmiri-strict-provenance -Zmiri-symbolic-alignment-check -Zmiri-disable-isolation) in CI workflows.

Verification

• cargo fmt -- --check: PASSED
• cargo clippy --workspace --all-targets -- -D warnings: PASSED (0 warnings)
• cargo test --workspace: PASSED (all unit, integration, netns, and doc tests)
• cargo deny check: PASSED
• cargo shear: PASSED
• RUSTFLAGS="--cfg loom" cargo test -p yip-io --test loom_spsc: PASSED (3/3 permutations)
• cargo +nightly miri test -p yip-verify: PASSED (12/12 tests)
• All pre-commit hooks passed cleanly.
• Closes perf(transport): zero-allocation scratch arena for FecEncoder on packet transmit path #208, closes perf(crypto): in-place zero-copy AEAD decryption via open_into for dataplane ingress #209, closes perf(transport): zero-copy repair shard buffering and circular ring-buffer ObjectTable for FEC reassembler #213, closes perf(dataplane): O(1) tail-eviction MAC table sweep and monotonic binary search for SentLog accounting #214.