fn erase_step<M: Memory + Copy, const SIDE: u64>(
m: M,
queue: u64,
node: &mut u64,
parent: &mut u64,
) -> Option<i32>Expand description
One step of erase_fixup with the short side, SIDE, known at compile
time, as the verifier explores far fewer states through two fixed-side
copies than through one that picks the side at run time. Returns the
result once the properties hold, or None to go on one level up.