I need to write the code for the sieve of Eratosthenes algorithm so that it is verifiable, that is, to verify that the method really returns only prime numbers.

I tried to add invariants and guarantees to the code, but I can’t prove anything to the verifier. My idea is this: in Eratosthenes Sieve comes an array of bool values of size n+1, from 0 to n. True is a prime number, False is a composite number. I iterate through the numbers from 2 to the root of n and if the number is prime, then I cross out the numbers to the right in the array that are divisible by this prime number, starting with a doubled prime number. This is an algorithm with optimizations, but I would like to verify at least an algorithm without optimizations. It seems to me that it can be proved this way: the index i goes from left to right from 2 to the root of n. If we encounter sieve[i] == true, then we remove all numbers greater than i and multiples of i from the array. Therefore, if we meet sieve[i] == false, then exists k :: k < i==> j % k == 0, because initially all the elements of the array were equal to true. Otherwise, if we met sieve[i] == true, it means forall k :: k < i ==> i % k != 0, so i is a prime.

But simple assertion might not hold. How to fix that? Or how to proof it simpler?

My code:

predicate is_prime(k: nat)    
{
    k > 1 && forall d :: 2 <= d < k ==> k % d != 0
}

method EratosthenesSieve(n: nat) returns (primes: set<nat>)        
    requires n > 2    
    //[1] i want to proof it:
    ensures forall k :: k in primes ==> is_prime(k)
    //[2] i want to proof it:
    ensures forall k :: 2 <= k <= n && is_prime(k) ==> k in primes
{
    var sieve: array<bool> := new bool[n+1];
    forall i:nat | 2 <= i < n { sieve[i] := true; }    

    var i: nat := 2;
    assert forall i:nat :: 2 <= i < n ==> sieve[i] == true;
    while i * i < n
        invariant 2 <= i < n < sieve.Length        
        decreases n - i
    {
        if sieve[i] {            
            forall j:nat | (i * i <= j < n) && (j % i == 0) { sieve[i] := false; }    
            //[3] assertion might not hold        
            assert forall j:nat :: (i * i <= j < n) && (j % i == 0) ==> sieve[j] == false;
        }
        i := i + 1;
    }
    primes := {}; 
    for i := 2 to n {
        if sieve[i] {
            primes := primes + {i};
        }
    }    
}