The replay window

int main(void)
{
	struct noise_replay_counter c;
	struct acc *set = NULL, *a, **l;
	u64 top = 0, n;
	size_t steps, i;
	int in, ok;
	bool r;

	c.counter = 0;
	for (i = 0; i < COUNTER_BITS_TOTAL / BITS_PER_LONG; i++)
		c.backtrack[i] = 0;
	steps = draw_steps();
	for (i = 0; i < steps; i++) {
		switch (nondet_u8() % 5) {
		case 0: n = top + (u64)(nondet_u32() % 200) - 100; break;           // around the top
		case 1: n = top - (u64)(nondet_u32() % 9000); break;                // inside and just outside the window
		case 4: n = top - M_W - 1 + (u64)(nondet_u32() % 5) - 2; break;     // the window's edge
		case 2: n = M_R + (u64)(nondet_u32() % 8) - 4; break;               // around the limit
		default: n = draw_u64(); break;
		}
		r = wg_counter_validate(&c, n);
		in = 0;
		for (a = set; a; a = a->next)
			if (a->n == n)
				in = 1;
		ok = top < M_R + 1 && n < M_R && n + 1 + M_W >= top && !in;
		CHECK(r == ok);
		if (ok) {
			a = malloc(sizeof(*a));
			if (a == NULL)
				break;
			a->n = n;
			a->next = set;
			set = a;
			if (n + 1 > top)
				top = n + 1;
		}
		CHECK(c.counter == top);
		// forget the nonces the window has left behind (the model accepts none of them again anyway)
		for (l = &set; *l;) {
			if ((*l)->n + 1 + M_W < top) {
				a = *l;
				*l = a->next;
				free(a);
			} else {
				l = &(*l)->next;
			}
		}
	}
	while (set) {
		a = set->next;
		free(set);
		set = a;
	}
	return 0;
}

static bool counter_validate(struct noise_replay_counter *counter, u64 their_counter)
{
	unsigned long index, index_current, top, i;
	bool ret = false;

	spin_lock_bh(&counter->lock);

	/* QUICKPROOF P10: `goto out` is `break` out of this block (VST has no goto); same statements in the same order */
	do {
	if (unlikely(counter->counter >= REJECT_AFTER_MESSAGES + 1 ||
		     their_counter >= REJECT_AFTER_MESSAGES))
		break;

	++their_counter;

	if (unlikely((COUNTER_WINDOW_SIZE + their_counter) <
		     counter->counter))
		break;

	index = their_counter >> ilog2(BITS_PER_LONG);

	if (likely(their_counter > counter->counter)) {
		index_current = counter->counter >> ilog2(BITS_PER_LONG);
		top = min_t(unsigned long, index - index_current,
			    COUNTER_BITS_TOTAL / BITS_PER_LONG);
		for (i = 1; i <= top; ++i)
			counter->backtrack[(i + index_current) &
				((COUNTER_BITS_TOTAL / BITS_PER_LONG) - 1)] = 0;
		WRITE_ONCE(counter->counter, their_counter);
	}

	index &= (COUNTER_BITS_TOTAL / BITS_PER_LONG) - 1;
	ret = !test_and_set_bit(their_counter & (BITS_PER_LONG - 1),
				&counter->backtrack[index]);

	} while (0); /* QUICKPROOF P10: was the label `out:` */
	spin_unlock_bh(&counter->lock);
	return ret;
}

Theorem x_counter : harness_safe whole_prog.

Theorem x_counter : harness_safe WgNoise.contracts.x_counter.whole_prog.
Proof. exact (proj1 (proj2 (proj2 (proj2 (proj2 (proj2 WgNoise.contracts.suite.suite_x)))))). Qed.