goto-instrument --ensure-one-backedge-per-target needs >20 GB on sha2 0.11's Sha256 #4965

Any harness that reaches sha2 0.11's Sha256::digest exhausts memory in the goto-instrument --ensure-one-backedge-per-target pass that Kani runs before verification. The earlier passes on the same model peak at about 100 MB.

[dependencies]
sha2 = "0.11"   # 0.11.0

use sha2::{Digest, Sha256};

#[cfg(kani)]
#[kani::proof]
fn sha256_of_four_bytes() {
    let input: [u8; 4] = kani::any();
    let digest = Sha256::digest(input);
    assert_eq!(digest.len(), 32);
}

Peak resident memory of each goto-instrument call cargo kani makes (measured with /usr/bin/time; address space capped at 20 GB):

Uncapped, the same pass took about 22 GB on a 30 GB machine before succeeding. The model going into the pass is small: 2,981 effective lines of code (goto-instrument --count-eloc), and goto-instrument --ensure-one-backedge-per-target on that file alone reproduces the blow-up (> 8 GB within 23 s). I have the goto file and can share it.

Kani main at 1640445, CBMC 6.11.0, x86_64 Linux. Found by kani autoharness over https://github.com/krakenfx/kraken-cli, where kraken-lab's hash::sha256_hex reaches this.

This is most likely a CBMC issue in ensure_one_backedge_per_target, triggered by something in sha2 0.11's code (0.10 is fine), so it probably wants a report to diffblue/cbmc with the goto file. On Kani's side, #4966's behaviour makes it worse: when the pass fails, the whole run is lost.