Reading a symbolic-length Vec back through a slice loop blows the SAT formula ~14x (heap read-back, not allocation)

[ixmatus]

Versions: kani 0.67.0; bundled CBMC toolchain nightly-2025-11-21 (aarch64-apple-darwin); --object-bits 16, 48 offset bits (Kani defaults). macOS 15, 64 GiB host.

Summary. A #[kani::proof] that builds a Vec of bounded length (at most 3) with a data-dependent (symbolic) length and then iterates it back through a for &e in &v slice loop produces an order-of-magnitude larger propositional formula than the same proof that builds the Vec but does not read it back. The blowup is not the allocator or the push path (those are cheap); it is the read-back of a symbolic-length heap slice. Bounding the element domain to 2 bits and the count to 3 does not help, because the cost is in CBMC's symbolic-offset heap model, not the element values.

Minimal reproducer (cargo kani --harness <name>, no_std + alloc):

#![no_std]
extern crate alloc;
use alloc::vec::Vec;

#[cfg(kani)] #[kani::proof] #[kani::unwind(4)]
fn build_only_no_readback() {
    let mut v: Vec<u64> = Vec::new();
    for _ in 0..3u32 { let x: u64 = kani::any(); kani::assume(x < 4); if x != 0 { v.push(x); } }
    kani::assert(v.len() <= 3, "at most three");
}

#[cfg(kani)] #[kani::proof] #[kani::unwind(4)]
fn build_then_readback() {
    let mut v: Vec<u64> = Vec::new();
    for _ in 0..3u32 { let x: u64 = kani::any(); kani::assume(x < 4); if x != 0 { v.push(x); } }
    let mut ok = true; let mut prev: u64 = 0;
    for &e in &v { if e < prev { ok = false; } prev = e; }
    kani::assert(ok || !ok, "trivial");
}

Measured (identical inputs, one extra read-back loop):

harness	variables	clauses	peak RSS	wall
build_only_no_readback	102,267	216,950	140 MiB	1.6 s
build_then_readback	1,387,736	5,642,263	1.24 GiB	4.4 s

One for &e in &v over a symbolic-length heap Vec multiplies variables 13.6x and RSS about 9x. A third variant replacing the iterator with concrete-index reads under a length guard (for i in 0..3 { if i < v.len() { ... v[i] ... } }) measured 1,635,070 variables, larger than the iterator form (each guarded index adds a bounds check against the symbolic length), showing the cost is the symbolic heap buffer itself, not the traversal pattern.

In a production harness (Vec<(u64, f64)>, three pushes with an ascending/finite accept-check, then an invariant scan of the result) the same construct reaches 15.24M variables / 67.3M clauses, peaking nondeterministically between 14 and 23 GiB, at which point it sits on a CI runner's OOM cliff. Isolating just the read-back assertion in its own harness still yields the full 15.24M formula.

Ask. (1) Is a tighter encoding feasible for iteration over a bounded-but-symbolic-length heap slice (for example, specializing when a small static upper bound on len is provable)? (2) Is there a supported idiom to keep such a read-back tractable without rewriting the property against a fixed-length view? Happy to share the full production harness.

Provenance: the reproducer was derived from the problem directly, not adapted from other code.