Performance: symbolic array index plus carry chain does not close (34-limb fixed-point accumulator)

[KyleClouthier]

Opening this at @feliperodri's suggestion on model-checking/kani-verifier-blog#59, where three of my harnesses came up as ones I had to gate out of CI because they would not close.

The harness

From bitrep, src/kani_proofs.rs. The property is that adding two finite f64 values in either order leaves byte-identical accumulator state.

fn any_finite() -> f64 {
    let x: f64 = kani::any();
    kani::assume(x.is_finite());
    x
}

#[kani::proof]
fn add_commutes() {
    let x = any_finite();
    let y = any_finite();
    let mut a = SumF64::new();
    a.add(x);
    a.add(y);
    let mut b = SumF64::new();
    b.add(y);
    b.add(x);
    assert_eq!(a, b);
}

SumF64 is a fixed-point accumulator: limbs: [u64; 34], a 3-bit specials flag, and a u64 count. No heap, no Vec, no recursion.

Result: did not close in roughly three hours on CI runners (ubuntu-latest). Currently gated behind cfg(kani_slow) and run locally only.

Two sibling harnesses have the same shape and the same outcome: cancellation_is_exact and add_placement_is_irrelevant.

For contrast, the merge and codec harnesses over the same 34-limb type close in seconds to minutes and run on every push. They differ in exactly one respect, described below.

Why I think it is expensive

add decomposes a symbolic f64 into a mantissa and a bit position, then writes into the limb array at an index derived from that position:

let (m, e) = /* mantissa and exponent from the symbolic f64 */;
let pos  = (e + BIAS) as usize;   // symbolic, 0..=2045
let limb = pos >> 6;              // SYMBOLIC INDEX into [u64; 34]
let off  = pos & 63;              // symbolic shift amount
let wide = (m as u128) << off;    // symbolic 128-bit shift
self.add_wide(limb, wide as u64, (wide >> 64) as u64);

and add_wide propagates a carry from that symbolic index to the end of the array:

fn add_wide(&mut self, limb: usize, lo: u64, hi: u64) {
    // ... add lo at `limb`, hi at `limb + 1` ...
    while carry && i < LIMBS {
        let (v, c) = self.limbs[i].overflowing_add(1);
        self.limbs[i] = v;
        carry = c;
        i += 1;
    }
}

So the combination is a symbolic index into a fixed array, followed by a carry chain whose length depends on that index, and the harness does this four times over two independent symbolic f64 values.

The merge and codec harnesses avoid this entirely: they start from kani::any() bytes, so every limb access is at a concrete index and the carry structure is fixed-shape. That is the one difference between the harnesses that close in seconds and the ones that do not.

What I am asking

Mostly whether this shape is known and whether anything can be done about it, since I suspect it is not specific to my crate. Symbolic-index-plus-carry-chain is a common pattern in fixed-point, bignum and checksum code.

Concretely:

1. Is there a recommended way to state this so CBMC does not have to consider all 34 limb positions independently? Some form of case split on limb, or restructuring add so the index is concrete per branch?
2. Would loop contracts on the carry loop help here, or is the cost dominated by the symbolic index instead of the loop?
3. Is there instrumentation that would tell me which part is dominating? I have the "did not close" data point and not much resolution beneath it.

I want to be straight that I gated these rather than tuning them exhaustively, because the properties are covered elsewhere: order invariance is proved at the model level in Lean, and the same code paths are exercised by the fast merge and codec harnesses, a BigInt-oracle differential fuzzer, and cross-architecture golden vectors. So this is not blocking me. It is a case where I would rather understand the wall than route around it, and it seemed worth reporting since you asked.

Happy to run any experiment you suggest and report back, and happy to reduce this to a smaller standalone repro if that is more useful than pointing at the crate.

Reproducing

git clone https://github.com/KyleClouthier/bitrep
cd bitrep
RUSTFLAGS="--cfg kani_slow" cargo kani --no-default-features --harness add_commutes

Kani 0.67.0, CBMC 6.8.0 locally; CI used the pinned toolchain in ci.yml.