Function fifo_bound_certified 

pub fn fifo_bound_certified(depth: usize, width: usize) -> bool

0 ≤ cnt ≤ depth for EVERY push/pop stream, by k-induction over the FIFO’s count register exactly as the RTL computes it (popped = pop ∧ cnt≠0, pushed = push ∧ cnt≠depth).