Euler's Sieve

This is a variant of Eratosthenes's sieve with complexity O(N)

Authors: Josué Moreau

Topics: Mathematics / Algorithms

Tools: Why3

see also the index (by topic, by tool, by reference, by year)

Euler's Sieve

This is a variant of Eratosthenes's sieve with complexity O(N), where N is the upper limit of the sieve. Cf https://en.wikipedia.org/wiki/Sieve_of_Eratosthenes#Euler's_sieve

Euler's Sieve makes use of a linked list of all integers, and marks composite numbers as in Eratosthenes's sieve.

In the program below, the linked list is implemented with an array (where each integer is mapped to the next one) and negative values are used to represent marked integers. In addition, the list only contains the odd integers (to save half of space).

Author: Josué Moreau (Université Paris-Saclay)

```module ArithmeticResults

use int.Int
use number.Divisibility
use number.Prime
use int.EuclideanDivision

let lemma mult_croissance_locale (n a: int)
requires { n > 0 /\ 0 <= a }
ensures  { n * a < n * (a + 1) } = ()

let rec lemma mult_croissance (n a b: int)
requires { n > 0 /\ 0 <= a < b }
ensures  { n * a < n * b }
variant  { b - a }
= if a + 1 = b then ()
else mult_croissance n (a + 1) b

let lemma comp_mult_2 (n k: int)
requires { n > 0 /\ k >= 2 }
ensures  { n * k >= n * 2 } = ()

let lemma div_croissance_locale1 (i n: int)
requires { 0 <= i /\ n > 0 }
ensures  { div i n <= div (i + 1) n } = ()

let rec lemma div_croissance1 (i j n: int)
requires { 0 <= i <= j /\ n > 0 }
ensures  { div i n <= div j n }
variant  { j - i }
= if i < j then
div_croissance1 i (j - 1) n

let rec lemma div_croissance_locale2 (m i: int)
requires { i > 0 /\ m >= 0 }
ensures  { div m (i + 1) <= div m i }
variant  { m }
= if m > 0 then div_croissance_locale2 (m - 1) i

let rec lemma div_croissance2 (m i j: int)
requires { 0 < i <= j /\ m >= 0 }
ensures  { div m i >= div m j }
variant  { j - i }
= if i < j then div_croissance2 m i (j - 1)

let lemma div_mult_1 (n k max: int)
requires { n > 0 /\ max >= n /\ n * k <= max }
ensures  { k = div (n * k) n <= div max n } = ()

let lemma mult_borne_sous_exp (n a b: int)
requires { a >= 1 /\ b >= 1 /\ n >= 1 /\ a * b < n }
ensures  { a < n /\ b < n } = ()

let rec lemma sq_ineq (a b: int)
requires { a >= 0 /\ b >= 0 }
requires { a * a < b * b }
ensures  { a < b }
variant  { b * b - a * a }
= if (b - 1) * (b - 1) > a * a then
sq_ineq a (b - 1)

end

module DivisibilityResults

use int.Int
use int.EuclideanDivision
use number.Divisibility
use number.Prime

let lemma divides_div (n m k: int)
requires { 2 <= n /\ 2 <= m /\ 2 <= k < n /\ divides n m /\ not divides k m }
ensures  { not divides k (div m n) } = ()

let lemma divides_inf (n m: int)
requires { 2 <= n /\ 2 <= m /\ divides n m /\
forall k. 2 <= k < n -> not divides k m }
ensures  { forall k. 2 <= k < n -> not divides k (div m n) } = ()

let lemma not_prime_divider_limits (n: int)
requires { not prime n /\ 2 <= n }
ensures  { exists i. 2 <= i /\ i * i <= n /\ divides i n } = ()

let lemma no_prod_impl_no_divider (n: int)
requires { n >= 0 }
ensures  { forall i.
2 <= i < n * n ->
not (exists k l. 2 <= k < n /\ 2 <= l < i /\ k * l = i ) ->
not (exists k. 2 <= k < n /\ k <> i /\ divides k i) } = ()

use ArithmeticResults

let lemma not_prime_impl_divisor_under_sqrt (n: int)
requires { n >= 2 }
ensures  { forall i.
2 <= i < n * n ->
not prime i ->
exists j. 2 <= j < i /\ ((j < n)
by j * j < n * n /\ j >= 0) /\ divides j i } = ()

end

module EulerSieveSpec

use int.Int
use number.Divisibility
use number.Prime
use seq.Seq
use int.EuclideanDivision

use ArithmeticResults
use DivisibilityResults

(*                                                                             *)
(*         INVARIANTS SUR LES RELATIONS ENTRE STRUCTURES DE DONNEES            *)
(*                                                                             *)

(* Borne sur le suivant de chaque élément de la liste chaînée *)
predicate inv_nexts (nexts: seq int) (n: int) =
forall i. 0 <= i < n ->
i < nexts[i] <= n

(* Tous les éléments éliminés de la liste chaînée sont marqués *)
predicate all_eliminated_marked (marked: seq bool)
(nexts: seq int) =
marked.length = nexts.length /\
forall i. 0 <= i < marked.length ->
forall j. i < j < nexts[i] ->
marked[j]

(* Tous les éléments éliminés, à partir d'un certain indice, sont marqués *)
predicate all_eliminated_marked_partial (marked: seq bool)
(nexts: seq int)
(min: int) =
marked.length = nexts.length /\
forall i. min <= i < marked.length ->
forall j. i < j < nexts[i] ->
marked[j]

(* L'élément suivant d'un élément non marqué inférieur à max / n est
non marqué lorsqu'il est lui-même inférieur à max / n *)
predicate not_marked_impl_next_not_marked (marked_old: seq bool)
(nexts: seq int)
(n: int) =
marked_old.length = nexts.length /\
marked_old.length >= 2 /\
n >= 2 /\
forall i. 2 <= i <= div (marked_old.length - 1) n ->
nexts[i] <= div (marked_old.length - 1) n ->
not marked_old[i] ->
not marked_old[nexts[i]]

(* Les deux tableaux marked sont identiques *)
predicate is_copy (marked: seq bool)
(marked_old: seq bool) =
marked.length = marked_old.length /\
forall i. 0 <= i < marked.length ->
not marked[i] ->
not marked_old[i]

(* L'élément suivant d'un élément non marqué inférieur à p <= max / n est
non marqué lorsqu'il est inférieur à max / n *)
predicate not_marked_impl_next_not_marked_partial (marked: seq bool)
(nexts: seq int)
(n: int)
(p: int) =
marked.length = nexts.length /\
marked.length >= 2 /\
n >= 2 /\
p <= div (marked.length - 1) n /\
forall i. 2 <= i < p ->
nexts[i] <= div (marked.length - 1) n ->
not marked[i] ->
not marked[nexts[i]]

(*                                                                             *)
(*                   PROPRIETES LIEES AUX NOMBRES PREMIERS                     *)
(*                                                                             *)

(* Tous les nombres jusqu'à n sont non marqués si et seulement si ils sont
premiers *)
predicate all_primes (marked: seq bool) (n: int) =
forall i. 0 <= i < n -> not marked[i] <-> prime i

(* Tous les multiples de i sont marqués *)
predicate all_multiples_marked (marked: seq bool) (i max: int) =
2 <= i < marked.length /\
forall k. 2 <= k < max ->
i * k < marked.length ->
marked[i * k]

(* Tous les multiples des 2 <= i < n sont marqués *)
predicate previously_marked_multiples (marked: seq bool) (n: int) =
forall i. 2 <= i < n ->
all_multiples_marked marked i marked.length

(* Les multiples des 2 <= i < n sont les uniques nombres marqués *)
predicate only_multiples_marked (marked: seq bool) (n: int) =
forall k. 2 <= k < marked.length ->
marked[k] ->
exists i j. 2 <= i < n /\ 2 <= j < marked.length /\ i * j = k

(* Les multiples de n avec les éléments non marqués précédement sont
marqués *)
predicate prime_multiples_marked (marked_old: seq bool)
(marked: seq bool)
(n max: int) =
marked_old.length = marked.length /\
n < max <= marked.length /\
forall i. n <= i < max ->
not marked_old[i] ->
n * i < marked_old.length ->
marked[n * i]

(* Invariants de base de remove_products *)
predicate inv_remove_products (nexts: seq int)
(marked: seq bool)
(n: int) =
nexts.length = marked.length /\
not marked[2] /\
all_primes marked n /\
prime n /\
not marked[n] /\
inv_nexts nexts nexts.length

(*                                                                             *)
(*             QUELQUES LEMMES DE CONSERVATION DES STRUCTURES                  *)
(*                                                                             *)

let lemma conservation_all_eliminated_marked_on_marked_change
(marked: seq bool)
(nexts: seq int)
(i: int)
requires { marked.length = nexts.length }
requires { inv_nexts nexts nexts.length }
requires { all_eliminated_marked marked nexts }
requires { 0 <= i < marked.length }
ensures  { all_eliminated_marked marked[i <- true] nexts } = ()

let lemma conservation_all_eliminated_marked_on_nexts_change
(marked: seq bool)
(nexts: seq int)
(i v: int)
requires { marked.length = nexts.length }
requires { all_eliminated_marked marked nexts }
requires { inv_nexts nexts marked.length }
requires { 0 <= i < marked.length }
requires { i < v <= marked.length }
requires { forall j. i < j < v -> marked[j] }
ensures  { all_eliminated_marked marked nexts[i <- v] } = ()

(*                                                                             *)
(*                         QUELQUES PREDICATS UTILES                           *)
(*                                                                             *)

predicate ordered (a: seq int) (n: int) =
forall i j. 0 <= i < j < n -> a[i] < a[j]

predicate all_inf_or_eq (a: seq int) (n k: int) =
forall i. 0 <= i < n -> a[i] <= k

end

module EulerSieve

use int.Int
use number.Divisibility
use number.Prime
use seq.Seq
use int.EuclideanDivision

use ArithmeticResults
use DivisibilityResults

use EulerSieveSpec

(*                                                                             *)
(*                   PROPRIETES LIEES AUX NOMBRES PREMIERS                     *)
(*                                                                             *)

(* Si tous les multiples des nombres i < n sont marqués,
alors les mutliples de ces multiples sont marqués *)
let lemma multiples_of_marked_are_marked (marked: seq bool) (n: int)
requires { 2 <= n <= marked.length }
requires { previously_marked_multiples marked n }
ensures  { forall k i.
2 <= k < n ->
2 <= i < marked.length ->
k * i < marked.length ->
forall j.
1 <= j < marked.length ->
k * i * j < marked.length ->
(marked[k * i * j]
by 1 <= i * j < marked.length
by k >= 2 /\ i >= 2 /\ j >= 1 /\ k * (i * j) < marked.length) }
= ()

(* Lemme essentiel : si tous les multiples des nombres i < n sont marqués
et qu'on a marqué tous les produits de n avec les nombres
non marqués
alors tous les multiples de n sont marqués *)
let lemma prev_and_new_impl_all_multiples_marked
(marked_old marked: seq bool)
(n max: int)
requires { 2 <= n < marked.length /\ 2 <= max < marked.length /\
marked_old.length = marked.length }
requires { is_copy marked marked_old }
requires { previously_marked_multiples marked_old n }
requires { previously_marked_multiples marked n }
requires { only_multiples_marked marked_old n }
requires { prime_multiples_marked marked_old marked n marked.length }
ensures  { all_multiples_marked marked n marked.length } =
assert { forall i. 2 <= i < n /\ 2 <= i < marked.length ->
not marked_old[i] ->
i * n < marked.length ->
marked[i * n] };
assert { forall k. 2 <= k < marked_old.length ->
marked_old[k] ->
n * k < marked_old.length ->
exists i j. 2 <= i < n /\ 2 <= j < marked_old.length /\
i * j = k /\ marked_old[i * j] };
multiples_of_marked_are_marked marked_old n;
multiples_of_marked_are_marked marked n;
assert { marked.length = marked_old.length };
assert { forall k. 2 <= k < marked_old.length ->
marked_old[k] ->
n * k < marked_old.length ->
marked[k * n]
by forall k. 2 <= k < marked_old.length ->
marked_old[k] ->
n * k < marked_old.length ->
marked_old[k * n] };
assert { prime_multiples_marked marked_old marked n marked.length };
assert { (forall k. 2 <= k < marked.length ->
not marked_old[k] -> n * k < marked.length ->
marked[n * k]) }

(*                                                                             *)
(*             LEMMES DE CONSERVATION LIES AUX NOMBRES PREMIERS                *)
(*                                                                             *)

let lemma conservation_only_multiples_marked (marked: seq bool) (n i j: int)
requires { 2 <= i < n /\ 2 <= j < marked.length /\ i * j < marked.length }
requires { only_multiples_marked marked n }
ensures  { only_multiples_marked marked[(i * j) <- true] n } =
assert { forall k. 0 <= k < marked.length ->
k <> i * j ->
marked[(i * j) <- true][k] = marked[k] };
assert { forall k.
2 <= k < marked.length ->
k <> i * j ->
marked[(i * j) <- true][k] ->
exists x y. 2 <= x < n /\ 2 <= y < marked.length /\ k = x * y };
assert { marked[i * j] -> 2 <= i < n -> 2 <= j < marked.length ->
exists x y. 2 <= x < n /\ 2 <= y < marked.length /\ x * y = i * j }

let lemma conservation_previously_marked_multiples (marked: seq bool)
(nexts: seq int)
(n: int)
requires { 2 <= n < marked.length /\ marked.length = nexts.length /\
nexts[n] <= marked.length }
requires { previously_marked_multiples marked n }
requires { only_multiples_marked marked (n + 1) }
requires { all_eliminated_marked marked nexts }
requires { not_marked_impl_next_not_marked marked nexts nexts[n] }
requires { all_multiples_marked marked n marked.length }
ensures  { previously_marked_multiples marked nexts[n] } =
assert { previously_marked_multiples marked (n + 1) };
assert { forall i. n < i < nexts[n] -> marked[i] };
assert { forall i. n < i < nexts[n] ->
((exists k l. 2 <= k <= n /\ 2 <= l < marked.length /\ k * l = i)
by marked[i]) };
multiples_of_marked_are_marked marked (n + 1);
assert { forall i j.
n < i < nexts[n] ->
2 <= j < marked.length ->
i * j < marked.length ->
(marked[i * j]
by (exists k l. 2 <= k <= n /\ 2 <= l < marked.length /\ k * l = i)) };
assert { forall i.
n < i < nexts[n] ->
all_multiples_marked marked i marked.length }

lemma conservation_previously_marked_multiples_on_marked_change:
forall marked n.
previously_marked_multiples marked n ->
forall i. 0 <= i < marked.length ->
previously_marked_multiples marked[i <- true] n

(*                                                                             *)
(*                      INVARIANTS SIMPLES DE FONCTIONS                        *)
(*                                                                             *)

let lemma conservation_not_marked_impl_next_not_marked
(marked: seq bool)
(nexts: seq int)
(max n p: int)
requires { not_marked_impl_next_not_marked marked nexts n /\
nexts[n] > n > 0 /\
div max nexts[n] <= div max n
by forall i. p < i < nexts[p] -> marked[i] /\
not_marked_impl_next_not_marked_partial marked nexts n p }
ensures  { not_marked_impl_next_not_marked marked nexts nexts[n] } = ()

let lemma unchanged_other_elements (s1: seq 'a) (s2: seq 'a) (i: int) (v: 'a)
requires { 0 <= i < length s1 /\ length s1 = length s2 }
requires { s1 = s2[i <- v] }
ensures  { forall j. 0 <= j < length s1 -> i <> j -> s1[j] = s2[j] } = ()

(*                                                                             *)
(*              DEFINITION DE LA STRUCTURE DE DONNEE ABSTRAITE                 *)
(*                                                                             *)

use mach.int.Int63

type t = private {
mutable ghost nexts: seq int;
mutable ghost marked: seq bool;
max: int63;
}
invariant { max_int > max >= 3 }
invariant { nexts.length = marked.length = max + 1 }
invariant { inv_nexts nexts nexts.length }
invariant { all_eliminated_marked marked nexts }
invariant { forall i. 3 <= i <= max -> mod i 2 = 0 -> marked[i] }
invariant { forall i. 3 <= i < max - 1 ->
mod i 2 = 1 ->
mod (Seq.get nexts i) 2 = 1 \/ Seq.get nexts i = max + 1 }
invariant { Seq.get nexts max = max + 1 /\
(mod (max - 1) 2 = 0 -> Seq.get nexts (max - 1) = max) /\
(mod (max - 1) 2 = 1 -> Seq.get nexts (max - 1) = max + 1) }

by { nexts = Seq.create 4 (fun i -> i + 1);
marked = Seq.create 4 (fun i -> i < 2);
max = 3 }

val create (max: int63) : t
requires { max_int > max >= 3 }
ensures  { result.max = max }
ensures  { Seq.get result.marked 0 = Seq.get result.marked 1 = true /\
not Seq.get result.marked 2 }
ensures  { forall i. 3 <= i <= max ->
mod i 2 = 0 <-> Seq.get result.marked i }
ensures  { forall i. 3 <= i < max - 1 ->
mod i 2 = 0 -> Seq.get result.nexts i = i + 1 }
ensures  { forall i. 3 <= i < max - 1 ->
mod i 2 = 1 -> Seq.get result.nexts i = i + 2 }
ensures  { forall i. 0 <= i <= max ->
Seq.get result.marked i -> i < 2 \/ divides 2 i }

val set_next (t: t) (i v: int63) : unit
requires { 0 <= i <= t.max /\ i < v <= t.max + 1 }
requires { mod i 2 = 1 }
requires { forall j. i < j < v -> Seq.get t.marked j }
requires { not Seq.get t.marked i }
requires { mod v 2 = 1 \/ v = t.max + 1 }
writes   { t.nexts }
ensures  { t.nexts = (old t.nexts)[i <- v] }

val get_next (t: t) (i: int63) : int63
requires { 3 <= i <= t.max }
requires { mod i 2 = 1 }
ensures  { 3 <= result <= t.max + 1 }
ensures  { result = t.nexts[i] }
ensures  { mod result 2 = 1 \/ result = t.max + 1 }

val set_mark (t: t) (i: int63) : unit
requires { 0 <= i <= t.max }
requires { mod i 2 = 1 }
writes   { t.marked }
ensures  { t.marked = (old t.marked)[i <- true] }

val get_mark (t: t) (i: int63) : bool
requires { 0 <= i <= t.max }
requires { mod i 2 = 1 }
ensures { result = t.marked[i] }

val get_max (t: t) : int63
ensures { result = t.max /\ result >= 2 }

(*                                                                             *)
(*     PREUVE DE REMOVE_PRODUCTS DANS LA STRUCTURE DE DONNEE ABSTRAITE         *)
(*                                                                             *)

let remove_products (t: t) (n: int63) : unit
requires { 3 <= n <= t.max /\ n * n <= t.max }
requires { inv_remove_products t.nexts t.marked n }
requires { previously_marked_multiples t.marked n }
requires { only_multiples_marked t.marked n }
requires { not_marked_impl_next_not_marked t.marked t.nexts n }
ensures  { inv_remove_products t.nexts t.marked n }
ensures  { not_marked_impl_next_not_marked t.marked t.nexts t.nexts[n] }
ensures  { previously_marked_multiples t.marked t.nexts[n] }
ensures  { only_multiples_marked t.marked t.nexts[n] }
= let d = get_max t / n in
let ghost max = t.max in
let ghost marked_old = t.marked in
let rec loop (p: int63) (ghost x: int) =
requires { n <= p <= max /\ 3 <= n <= max /\ mod p 2 = 1 /\
p <= x < t.nexts[p] /\ t.nexts[x] = t.nexts[p] /\
t.marked[n * n] }
requires { inv_remove_products t.nexts t.marked n }
requires { previously_marked_multiples t.marked n }
requires { not t.marked[p] }
requires { is_copy t.marked marked_old }
requires { all_eliminated_marked_partial marked_old t.nexts x }
requires { not_marked_impl_next_not_marked marked_old t.nexts n }
requires { prime_multiples_marked marked_old t.marked n t.nexts[x] }
requires { not_marked_impl_next_not_marked_partial t.marked t.nexts n p }
requires { only_multiples_marked t.marked (n + 1) }
ensures  { inv_remove_products t.nexts t.marked n }
ensures  { not_marked_impl_next_not_marked t.marked t.nexts t.nexts[n] }
ensures  { is_copy t.marked marked_old }
ensures  { previously_marked_multiples t.marked n }
ensures  { prime_multiples_marked marked_old t.marked n t.marked.length }
ensures  { only_multiples_marked t.marked (n + 1) }
variant  { max - t.nexts[p] }
let next = get_next t p in
if 0 <= next <= get_max t then
if next <= d then begin
assert { n * next <= max by n * next <= n * d by next <= d };
ghost (conservation_only_multiples_marked t.marked (to_int n + 1)
(to_int n) t.nexts[to_int p]);
let ghost marked_copy = t.marked in
set_mark t (n * next);
unchanged_other_elements t.marked marked_copy
(to_int n * to_int next) true;
assert { p < 2 * p < 2 * t.nexts[p] <= n * t.nexts[p] = n * next };
assert { not t.marked[p] by n * next > p /\ p <= length t.marked };
assert { not marked_old[t.nexts[p]] by 2 <= p < next <= div max n };
assert { prime_multiples_marked marked_old t.marked n t.nexts[next]
by prime_multiples_marked marked_old t.marked n t.nexts[x] };
assert { forall i. 0 <= i < p -> t.nexts[i] <= p
by forall i. 0 <= i < p ->
forall j. i < j < t.nexts[i] -> t.marked[j] };
if get_mark t next then begin
assert { t.nexts[p] <> t.marked.length };
let ghost nexts_copy = t.nexts in
set_next t p (get_next t next);
unchanged_other_elements t.nexts nexts_copy (to_int p)
nexts_copy[to_int next];
assert { all_eliminated_marked_partial marked_old t.nexts next
by p <= x < next /\
forall j. next <= j < length t.nexts ->
t.nexts[j] = nexts_copy[j] };
loop p (to_int next)
end else begin
assert { forall i. p < i < t.nexts[p] -> t.marked[i] };
loop next (to_int next)
end
end else begin
assert { n * next > max
by n * (div max n + 1) > max >= n * div max n /\
n * next >= n * (d + 1) by next >= d + 1 };
ghost (conservation_not_marked_impl_next_not_marked t.marked t.nexts
(to_int max) (to_int n) (to_int p))
end else
ghost (conservation_not_marked_impl_next_not_marked t.marked t.nexts
(to_int max) (to_int n) (to_int p)) in
ghost (conservation_only_multiples_marked t.marked (to_int n + 1)
(to_int n) (to_int n));
let ghost marked_copy = t.marked in
set_mark t (n * n);
unchanged_other_elements t.marked marked_copy (to_int n * to_int n) true;
assert { forall i. 0 <= i < n -> t.nexts[i] <> n * n
by forall i. 0 <= i < n -> t.nexts[i] <= n < n * n
by not t.marked[n] /\
forall i. 0 <= i < n ->
forall j. i < j < t.nexts[i] -> t.marked[j] };
loop n (to_int n);
ghost (prev_and_new_impl_all_multiples_marked marked_old t.marked
(to_int n) (to_int max));
ghost (conservation_previously_marked_multiples t.marked t.nexts
(to_int n))

(*                                                                             *)
(*           QUELQUES LEMMES NECESSAIRES A LA SUITE DE LA PREUVE               *)
(*                                                                             *)

let lemma previously_marked_multiples_impl_prime (marked: seq bool) (n: int)
requires { 2 <= n < marked.length /\ not marked[n] }
requires { previously_marked_multiples marked n }
ensures  { prime n } =
assert { forall k.
2 <= k < n -> not divides k n
by forall k.
2 <= k < n ->
not (exists i. 2 <= i < marked.length /\ n = k * i) }

let lemma only_multiples_marked_impl_not_marked (marked: seq bool)
(nexts: seq int)
(n: int)
requires { 2 <= n < marked.length }
requires { only_multiples_marked marked nexts[n] }
requires { prime n }
ensures  { not marked[n] } =
assert { forall i j. 2 <= i < n -> 2 <= j < marked.length -> i * j <> n }

end

module EulerSieveImpl

use int.Int
use seq.Seq
use mach.int.Int63
use mach.array.ArrayInt63

use int.Abs
use int.EuclideanDivision
use number.Divisibility
use number.Prime

use DivisibilityResults
use EulerSieveSpec

(*                                                                             *)
(*              LEMMES DE CONSERVATION LIES A L'IMPLEMENTATION                 *)
(*                                                                             *)

let lemma conservation_inv_arr_on_mark (arr: seq int) (i: int)
requires { forall j k. 0 <= j < length arr ->
j < k < div (abs arr[j]) 2 -> arr[k] < 0 }
requires { forall i. 0 <= i < length arr ->
i < div (abs arr[i]) 2 <= length arr }
requires { 0 <= i < length arr }
requires { arr[i] >= 0 }
ensures  { forall j k. 0 <= j < length arr ->
j < k < div (abs arr[i <- - arr[i]][j]) 2 ->
arr[i <- - arr[i]][k] < 0 } =
assert { forall j. 0 <= j < length arr ->
arr[j] < i -> arr[j] = arr[i <- - arr[i]][j] };
assert { forall j. 0 <= j < length arr ->
arr[i] < j -> arr[j] = arr[i <- - arr[i]][j] }

let lemma conservation_inv_arr_on_jump (arr: seq int) (min i: int)
requires { min >= 0 }
requires { forall j k. min <= j < length arr ->
j < k < div (abs arr[j]) 2 -> arr[k] < 0 }
requires { forall i. min <= i < length arr ->
i < div (abs arr[i]) 2 <= length arr }
requires { min <= i < length arr }
requires { 0 <= div arr[i] 2 < length arr }
requires { arr[div arr[i] 2] < 0 }
ensures  { forall j k. min <= j < length arr ->
j < k < div (abs arr[i <- - arr[div arr[i] 2]][j]) 2 ->
arr[i <- - arr[div arr[i] 2]][k] < 0 } =
let ghost next = div (Seq.get arr i) 2 in
let ghost arr1 = arr[i <- - Seq.get arr next] in
assert { forall j. min <= j < i -> arr[j] = arr1[j] };
assert { forall j. i < j < length arr -> arr[j] = arr1[j] }

(*                                                                             *)
(*         DEFINITION DE L'IMPLEMENTATION DE LA STRUCTURE DE DONNEE            *)
(*                                                                             *)

type t = {
mutable ghost nexts: seq int;
mutable ghost marked: seq bool;
arr: array63;
max: int63;
max_arr: int63
}
invariant { max_int > max >= 3 }
invariant { Seq.length nexts = Seq.length marked = max + 1 }
invariant { div (max - 1) 2 = max_arr }
invariant { length arr = max_arr + 1 }
invariant { inv_nexts nexts (Seq.length nexts) }
invariant { all_eliminated_marked marked nexts }
invariant { forall i. 3 <= i <= max -> mod i 2 = 0 -> Seq.get marked i }
invariant { forall i. 3 <= i < max - 1 ->
mod i 2 = 1 ->
mod (Seq.get nexts i) 2 = 1 \/ Seq.get nexts i = max + 1 }
invariant { Seq.get nexts max = max + 1 /\
(mod (max - 1) 2 = 0 -> Seq.get nexts (max - 1) = max) /\
(mod (max - 1) 2 = 1 -> Seq.get nexts (max - 1) = max + 1) }
(* glueing invariant *)
invariant { forall i. 0 <= i <= max_arr -> -(max + 1) <= arr[i] <= max + 1 }
invariant { forall i. 0 <= i <= max_arr ->
Seq.get marked (2 * i + 1) <-> arr[i] < 0 }
invariant { forall i. 0 <= i <= max_arr ->
not Seq.get marked (2 * i + 1) ->
arr[i] = Seq.get nexts (2 * i + 1) }
invariant { forall i. 0 <= i <= max_arr ->
Seq.get marked (2 * i + 1) ->
arr[i] = - Seq.get nexts (2 * i + 1) }
invariant { forall i. 0 <= i <= max_arr ->
i < div (abs arr[i]) 2 <= max_arr + 1 /\
abs arr[i] <= max + 1 }
invariant { forall i j. 0 <= i <= max_arr ->
i < j < div (abs arr[i]) 2 -> arr[j] < 0 }
by { nexts = Seq.create 4 (fun i -> i + 1);
marked = Seq.create 4 (fun i -> i < 2);
arr = ArrayInt63.set (ArrayInt63.make 2 (-2)) 1 4;
max = 3; max_arr = 1 }

let create (max: int63) : t
requires { max_int > max >= 3 }
ensures  { result.max = max }
ensures  { Seq.get result.marked 0 = Seq.get result.marked 1 = true /\
not Seq.get result.marked 2 }
ensures  { forall i. 1 <= i <= div (max - 1) 2 ->
not Seq.get result.marked (2 * i + 1) }
ensures  { forall i. 2 <= i <= div (max + 1) 2 ->
2 * i <= max ->
Seq.get result.marked (2 * i) }
ensures  { forall i. 1 <= i <= div (max - 1) 2 ->
2 * i + 1 < max - 1 ->
Seq.get result.nexts (2 * i + 1) = 2 * i + 3 }
ensures  { forall i. 2 <= i <= div (max - 1) 2 ->
2 * i < max - 1 ->
Seq.get result.nexts (2 * i) = 2 * i + 1 }
ensures  { forall i. 0 <= i <= max ->
Seq.get result.marked i -> i < 2 \/ divides 2 i }
= let ghost len = pure { max + 1 } in
let len_arr = (max - 1) / 2 + 1 in
let ghost nexts = Seq.create len (pure { fun (i: int) ->
if i = max then max + 1
else if i = max - 1 then if mod i 2 = 0 then max else max + 1
else if i < 3 || mod i 2 = 0 then i + 1
else i + 2}) in
let ghost marked = Seq.create len (fun i ->
i = 0 || i = 1 || (i > 2 && mod i 2 = 0)) in
let ghost f = pure { fun i -> if i = len_arr - 1 then max + 1
else if i = 0 then -2
else 2 * i + 3 } in
let arr = ArrayInt63.make len_arr (-2) in
for i = 1 to len_arr - 1 do
invariant { forall j. 0 <= j < i -> arr[j] = f j }
arr[i] <- if i = len_arr - 1 then max + 1 else 2 * i + 3
done;
{ nexts = nexts;
marked = marked;
arr = arr;
max = max;
max_arr = (max - 1) / 2 }

let set_next (t: t) (i v: int63) : unit
requires { 0 <= i <= t.max /\ i < v <= t.max + 1 }
requires { mod i 2 = 1 }
requires { forall j. i < j < v -> Seq.get t.marked j }
requires { not Seq.get t.marked i }
requires { mod v 2 = 1 \/ v = t.max + 1 }
writes   { t.nexts, t.arr }
ensures  { t.nexts = Seq.set (old t.nexts) i v }
= ghost ( conservation_all_eliminated_marked_on_nexts_change
t.marked t.nexts (to_int i) (to_int v) );
t.arr[i / 2] <- v;
ghost (t.nexts <- Seq.set t.nexts (to_int i) (to_int v))

let get_next (t: t) (i: int63) : int63
requires { 3 <= i <= t.max }
requires { mod i 2 = 1 }
ensures  { 3 <= result <= t.max + 1 }
ensures  { result = Seq.get t.nexts i }
ensures  { mod result 2 = 1 \/ result = t.max + 1 }
= let x = i / 2 in
if t.arr[x] < 0 then - t.arr[x] else t.arr[x]

let set_mark (t: t) (i: int63) : unit
requires { 0 <= i <= t.max }
requires { mod i 2 = 1 }
writes   { t.marked, t.arr }
ensures  { t.marked = Seq.set (old t.marked) i true }
= let x = i / 2 in
ghost ( conservation_all_eliminated_marked_on_marked_change
t.marked t.nexts (to_int i));
if t.arr[x] >= 0 then begin
ghost ( conservation_inv_arr_on_mark t.arr.elts (to_int x) );
t.arr[x] <- - t.arr[x]
end;
ghost (t.marked <- Seq.set t.marked (to_int i) true)

let get_mark (t: t) (i: int63) : bool
requires { 0 <= i <= t.max }
requires { mod i 2 = 1 }
ensures  { result = Seq.get t.marked i }
= t.arr[i / 2] < 0

let get_max (t: t) : int63
ensures { result = t.max /\ result >= 2 }
= t.max

clone EulerSieve with type t = t,
val create = create,
val set_next = set_next, val get_next = get_next,
val set_mark = set_mark, val get_mark = get_mark,
val get_max = get_max

predicate inv_count (arr: seq int) (min: int) =
forall i. min <= i < arr.length ->
(i < div (abs arr[i]) 2 <= arr.length /\
- max_int <= arr[i] <= max_int /\
(forall j. i < j < div (abs arr[i]) 2 -> arr[j] < 0) /\
(forall j. 2 * i + 1 < j < abs arr[i] -> not prime j))

(*                                                                             *)
(*                         PREUVE DU CRIBLE D'EULER                            *)
(*                                                                             *)

let euler_sieve (max: int63) : array63
requires { max_int > max >= 3 }
ensures  { forall i j. 0 <= i < j < result.length -> result[i] < result[j] }
ensures  { forall i. 0 <= i < result.length -> 2 <= result[i] <= max }
ensures  { forall i. 0 <= i < result.length -> prime result[i] }
ensures  { forall i. 2 <= i <= max -> prime i ->
exists j. 0 <= j < result.length /\ result[j] = i }
= [@vc:do_not_keep_trace] (* traceability info breaks the proof with Vampire on sub goal 13.2 *)
let t = create max in
let rec loop (n: int63) =
requires { 3 <= n <= max }
requires { n * n <= max }
requires { previously_marked_multiples t.marked n }
requires { only_multiples_marked t.marked n }
requires { not_marked_impl_next_not_marked t.marked t.nexts n }
requires { inv_remove_products t.nexts t.marked n }
ensures { forall i. 0 <= i < Seq.length t.marked ->
not Seq.get t.marked i <-> prime i }
variant { max + 1 - n }
remove_products t n;
let nn = get_next t n in
if nn <= max / nn then begin
assert { nn * nn <= max };
ghost (previously_marked_multiples_impl_prime t.marked (to_int nn));
assert { (forall i. n < i < nn -> not prime i)
by (forall i.
n < i < nn ->
(exists j k.
2 <= j < nn /\
2 <= k < Seq.length t.marked /\
j * k = i)
by Seq.get t.marked i) };
loop (nn)
end else begin
ghost (not_prime_impl_divisor_under_sqrt (to_int nn));
assert { forall i.
2 <= i < Seq.length t.marked ->
not Seq.get t.marked i ->
not (exists k l. 2 <= k < nn /\ 2 <= l < i /\
k * l = i) };
ghost (no_prod_impl_no_divider (to_int nn));
assert { Seq.length t.marked <= nn * nn
by nn * nn > max
by nn * (div max nn + 1) > max >= nn * div max nn
/\ nn * nn >= nn * (div max nn + 1)
by nn >= div max nn + 1 };
assert { forall i. 2 <= i < Seq.length t.marked ->
not Seq.get t.marked i ->
prime i
by forall i.
2 <= i < Seq.length t.marked ->
not Seq.get t.marked i ->
(not (exists k. 2 <= k < nn /\ k <> i /\
divides k i)
by forall k.
2 <= k ->
k <> i ->
(divides k i <-> exists l. 2 <= l < i /\ k * l = i)
by divides k i -> 2 <= div i k < i) }
end in
if max >= 9 then loop 3;
assert { forall i. 1 <= i <= t.max_arr -> t.arr[i] >= 0 <-> prime (2 * i + 1) };
assert { forall p i. 1 <= p <= t.max_arr ->
2 * p + 1 < i < abs t.arr[p] -> not prime i
by mod i 2 = 0 -> (Seq.get t.marked i
by Seq.get t.nexts (2 * i + 1) = t.arr[i]) };
assert { forall j. 1 <= j <= t.max_arr -> t.arr[0 <- 2][j] = t.arr[j] };
let ref cnt = 1:int63 in
let ref p = 1 in
t.arr[0] <- 2;
while 2 * p + 1 <= max do
invariant { 1 <= p <= t.max_arr + 1 }
invariant { 1 <= cnt <= p }
invariant { 2 * p + 1 <= max -> t.arr[p] >= 0 }
invariant { 2 * p + 1 <= max -> prime (2 * p + 1) }
invariant { inv_count t.arr cnt }
invariant { ordered t.arr cnt }
invariant { all_inf_or_eq t.arr cnt (2 * p) }
invariant { forall i. cnt <= i <= t.max_arr ->
t.arr[i] >= 0 <-> prime (2 * i + 1) }
invariant { forall i. 0 <= i < cnt -> prime t.arr[i] }
invariant { forall i. 2 <= i < 2 * p + 1 -> prime i ->
exists j. 0 <= j < cnt /\ t.arr[j] = i }
variant { t.max_arr + 1 - p , max + 1 - t.arr[p] }
let next = t.arr[p] / 2 in
if next <= t.max_arr then begin
assert { 1 <= p <= t.max_arr /\ t.arr[p] >= 0 /\ prime (2 * p + 1) };
if t.arr[next] < 0 then begin
t.arr[p] <- - t.arr[next];
unchanged_other_elements t.arr.elts (pure { t.arr.elts at BeforeAssign })
(to_int p) (- to_int t.arr[next]);
assert { forall i. p < i < div t.arr[p] 2 -> t.arr[i] < 0 };
assert { t.arr[p] = abs (t.arr at BeforeAssign)[next]
> (t.arr at BeforeAssign)[p] > p };
conservation_inv_arr_on_jump (pure { t.arr.elts at BeforeAssign })
(to_int cnt) (to_int p);
assert { cnt <= next < length t.arr };
assert { (forall j. 2 * p + 1 < j < (t.arr at BeforeAssign)[p] ->
not prime j) /\
(forall j. 2 * next + 1 < j < abs (t.arr at BeforeAssign)[next] ->
not prime j) }
end else begin
t.arr[cnt] <- 2 * p + 1;
unchanged_other_elements t.arr.elts (pure { t.arr.elts at BeforeAssign })
(to_int cnt) (2 * to_int p + 1);
cnt <- cnt + 1;
p <- next;
assert { forall k. cnt <= k < length (t.arr at BeforeAssign) ->
t.arr[k] = (t.arr at BeforeAssign)[k] }
end
end else begin
t.arr[cnt] <- 2 * p + 1;
unchanged_other_elements t.arr.elts (pure { t.arr.elts at BeforeAssign })
(to_int cnt) (2 * to_int p + 1);
cnt <- cnt + 1;
p <- t.max_arr + 1;
assert { forall k. cnt <= k < length (t.arr at BeforeAssign) ->
t.arr[k] = (t.arr at BeforeAssign)[k] }
end
done;
sub t.arr 0 cnt

end
```

Why3 Proof Results for Project "euler_sieve"

Theory "euler_sieve.ArithmeticResults": fully verified

 Obligations Alt-Ergo 2.3.3 CVC4 1.8 VC for mult_croissance_locale 0.00 --- VC for mult_croissance 0.01 --- VC for comp_mult_2 0.01 --- VC for div_croissance_locale1 --- 0.27 VC for div_croissance1 0.02 --- VC for div_croissance_locale2 --- 0.24 VC for div_croissance2 0.02 --- VC for div_mult_1 --- 0.28 VC for mult_borne_sous_exp 0.30 --- VC for sq_ineq --- 0.18

Theory "euler_sieve.DivisibilityResults": fully verified

 Obligations Alt-Ergo 2.3.3 Vampire 4.2.2 VC for divides_div 0.05 --- VC for divides_inf 0.04 --- VC for not_prime_divider_limits 0.01 --- VC for no_prod_impl_no_divider --- --- split_vc postcondition --- --- case (exists k:int. (2 <= k /\ k < n) /\ not k = i /\ divides k i) true case (postcondition) --- --- destruct H true case (postcondition) --- --- destruct H destruct premise --- --- introduce_exists destruct premise --- --- assert (exists l:int. l * k = i) asserted formula 0.02 --- destruct premise --- --- introduce_exists destruct premise --- --- exists k no_prod_impl_no_divider'vc.0.0.0.0.0.1.0.0 --- --- exists l no_prod_impl_no_divider'vc.0.0.0.0.0.1.0.0.0 --- --- case (l = i) true case --- --- assert (k = 1) asserted formula --- 0.08 true case 0.01 --- false case 2.92 --- true case (postcondition) 0.01 --- false case (postcondition) 0.01 --- VC for not_prime_impl_divisor_under_sqrt 0.03 ---

Theory "euler_sieve.EulerSieveSpec": fully verified

 Obligations Alt-Ergo 2.3.3 VC for conservation_all_eliminated_marked_on_marked_change 0.06 VC for conservation_all_eliminated_marked_on_nexts_change --- inline_goal VC for conservation_all_eliminated_marked_on_nexts_change --- split_vc postcondition --- split_vc postcondition 0.02 postcondition 0.55

Theory "euler_sieve.EulerSieve": fully verified

 Obligations Alt-Ergo 2.0.0 Alt-Ergo 2.3.3 Alt-Ergo 2.4.1 Alt-Ergo 2.4.2 CVC3 2.4.1 CVC4 1.7 CVC4 1.8 CVC5 1.0.5 Eprover 2.0 Vampire 4.2.2 Z3 3.2 Z3 4.7.1 Z3 4.8.10 VC for multiples_of_marked_are_marked --- --- --- --- --- --- --- --- --- --- --- --- --- split_vc postcondition --- --- --- --- --- --- --- --- --- --- --- --- --- split_vc postcondition --- 0.02 --- --- --- --- --- --- --- --- --- --- --- postcondition --- 0.01 --- --- --- --- --- --- --- --- --- --- --- postcondition --- 0.01 --- --- --- --- --- --- --- --- --- --- --- postcondition --- 0.01 --- --- --- --- --- --- --- --- --- --- --- VC for multiples_of_marked_are_marked --- --- --- --- --- --- --- --- --- --- --- --- --- inline_all VC for multiples_of_marked_are_marked --- --- --- --- 0.04 --- --- --- --- --- --- --- --- remove Assoc1,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm1,Assoc,Mul_distr_l,Mul_distr_r,Comm,Unitary,NonTrivialRing,Refl,ZeroLessOne,CompatOrderAdd,CompatOrderMult,Abs_le,Abs_pos,Mod_bound,Div_unique,Div_bound,Mod_1,Div_1,Div_inf,Div_inf_neg,Mod_0,Div_1_left,Div_minus1_left,Mod_minus1_left,Div_mult,Mod_mult,Div_mod1,Div_bound1,Mod_bound1,Div_sign_pos,Div_sign_neg,Mod_sign_pos,Mod_sign_neg,Rounds_toward_zero,Div_11,Mod_11,Div_inf1,Mod_inf,Div_mult1,Mod_mult1,even_or_odd,even_not_odd,even_odd,odd_even,even_even,odd_odd,even_2k,odd_2k1,even_mod2,divides'spec,divides_refl,divides_1_n,divides_0,divides_left,divides_right,divides_oppr,divides_oppl,divides_oppr_rev,divides_oppl_rev,divides_plusr,divides_minusr,divides_multl,divides_multr,divides_factorl,divides_factorr,divides_n_1,divides_antisym,divides_trans,divides_bounds,mod_divides_euclidean,mod_divides_computer,divides_mod_computer,odd_divides,prime_2,prime_3,prime_divisors,small_divisors,even_prime,odd_prime,mult_croissance_locale,mult_croissance,comp_mult_2,div_croissance_locale1,div_croissance1,div_croissance_locale2,div_croissance2,div_mult_1,sq_ineq,divides_div,divides_inf,not_prime_divider_limits,no_prod_impl_no_divider,not_prime_impl_divisor_under_sqrt,length_nonnegative,(==)'spec,create'spec,empty'def,set'spec,set'def,([<-])'def,singleton'spec,cons'spec,snoc'spec,([..])'spec,([..])'def,([_..])'def,([.._])'def,(++)'spec,conservation_all_eliminated_marked_on_marked_change,conservation_all_eliminated_marked_on_nexts_change,H13,H12,Requires,H11,H10,H9,H8,H7,H6,H5,H4,H3,H VC for multiples_of_marked_are_marked --- --- --- --- 0.01 --- 0.03 --- --- --- --- --- 0.01 VC for multiples_of_marked_are_marked --- --- --- --- --- --- --- --- --- --- --- --- --- assert (k * (i * j) = i*j + (k-1)*(i*j)) asserted formula --- 0.02 --- --- --- --- --- --- --- --- --- --- --- VC for multiples_of_marked_are_marked --- --- --- --- --- --- --- --- --- --- --- --- --- assert ((k-1)*(i*j) >= 0) asserted formula --- 0.02 --- --- --- --- --- --- --- --- --- --- --- VC for multiples_of_marked_are_marked --- 0.02 --- --- --- --- --- --- --- --- --- --- --- VC for multiples_of_marked_are_marked --- --- --- --- --- --- --- --- --- --- --- --- --- unfold previously_marked_multiples in Requires VC for multiples_of_marked_are_marked --- --- --- --- --- --- --- --- --- --- --- --- --- unfold all_multiples_marked in Requires VC for multiples_of_marked_are_marked --- --- --- --- --- --- --- --- --- --- 0.04 --- --- remove zero,one,(-),even,([]),inv_nexts,all_eliminated_marked,all_eliminated_marked_partial,is_copy,not_marked_impl_next_not_marked_partial,all_primes,all_multiples_marked,previously_marked_multiples,only_multiples_marked,prime_multiples_marked,inv_remove_products,Assoc1,Unit_def_r,Mul_distr_l,Refl,Trans,Div_unique,Div_bound,Div_minus1_left,Div_sign_pos,even_not_odd,odd_not_even,even_odd,odd_2k1,divides_left,divides_oppr_rev,divides_multl,divides_multr,divides_mod_euclidean,mod_divides_computer,prime_divisors,odd_prime,mult_croissance_locale,comp_mult_2,sq_ineq,divides_div,no_prod_impl_no_divider,create'spec,empty'def,set'spec,set'def,singleton'spec,cons'spec,snoc'spec,([..])'spec,([..])'def,(++)'spec,conservation_all_eliminated_marked_on_marked_change,conservation_all_eliminated_marked_on_nexts_change VC for multiples_of_marked_are_marked --- --- --- --- --- --- --- --- --- 0.11 0.03 --- --- VC for prev_and_new_impl_all_multiples_marked --- --- --- --- --- --- --- --- --- --- --- --- --- split_vc assertion --- --- --- --- --- --- --- --- --- --- --- --- --- split_vc assertion --- --- --- --- --- --- --- --- --- --- --- --- --- unfold previously_marked_multiples in Requires2 assertion --- --- --- --- --- --- --- --- --- --- --- --- --- unfold all_multiples_marked in Requires2 assertion --- 0.03 --- --- --- --- --- --- --- --- --- --- --- assertion --- 0.09 --- --- --- --- --- --- --- --- --- --- --- precondition --- 0.01 --- --- --- --- --- --- --- --- --- --- --- precondition --- 0.01 --- --- --- --- --- --- --- --- --- --- --- precondition --- 0.01 --- --- --- --- --- --- --- --- --- --- --- precondition --- 0.02 --- --- --- --- --- --- --- --- --- --- --- assertion --- 0.01 --- --- --- --- --- --- --- --- --- --- --- assertion --- 0.25 --- --- --- --- --- --- --- --- --- --- --- assertion --- 0.01 --- --- --- --- --- --- --- --- --- --- --- assertion --- 0.03 --- --- --- --- --- --- --- --- --- --- --- postcondition --- 0.05 --- --- --- --- --- --- --- --- --- --- --- VC for conservation_only_multiples_marked --- --- --- --- --- --- --- --- --- --- --- --- --- split_vc assertion --- 0.12 --- --- --- --- --- --- --- --- --- --- --- assertion --- 0.10 --- --- --- --- --- --- --- --- --- --- --- assertion --- 0.02 --- --- --- --- --- --- --- --- --- --- --- postcondition --- --- --- --- --- --- --- --- --- --- --- --- --- inline_goal postcondition --- --- --- --- --- --- --- --- --- --- --- --- --- split_vc postcondition --- --- --- --- --- --- --- --- --- --- --- --- --- case (k = i * j) true case (postcondition) --- 0.03 --- --- --- --- --- --- --- --- --- --- --- false case (postcondition) --- 0.10 --- --- --- --- --- --- --- --- --- --- --- VC for conservation_previously_marked_multiples --- --- --- --- --- --- --- --- --- --- --- --- --- split_vc assertion --- 0.02 --- --- --- --- --- --- --- --- --- --- --- assertion --- 0.03 --- --- --- --- --- --- --- --- --- --- --- assertion --- --- --- --- --- --- --- --- --- --- --- --- --- split_vc assertion --- 0.02 --- --- --- --- --- --- --- --- --- --- --- VC for conservation_previously_marked_multiples --- 0.08 --- --- --- --- --- --- --- --- --- --- --- precondition --- 0.02 --- --- --- --- --- --- --- --- --- --- --- precondition --- 0.02 --- --- --- --- --- --- --- --- --- --- --- assertion --- --- --- --- --- --- --- --- --- --- --- --- --- split_vc assertion --- --- --- --- --- --- --- --- --- 0.59 --- --- --- VC for conservation_previously_marked_multiples --- 0.04 --- --- --- --- --- --- --- --- --- --- --- assertion --- --- --- --- --- --- --- --- --- --- --- --- --- split_vc assertion --- --- --- --- --- --- --- --- --- --- --- --- --- inline_goal assertion --- --- --- --- --- --- --- --- --- --- --- --- --- split_vc assertion --- 0.02 --- --- --- --- --- --- --- --- --- --- --- assertion --- 0.02 --- --- --- --- --- --- --- --- --- --- --- assertion --- 0.02 --- --- --- --- --- --- --- --- --- --- --- postcondition --- 0.02 --- --- --- --- --- --- --- --- --- --- --- conservation_previously_marked_multiples_on_marked_change --- --- --- --- --- --- --- --- --- --- --- --- --- inline_goal conservation_previously_marked_multiples_on_marked_change.0 --- --- --- --- --- --- --- --- --- --- --- --- --- split_vc conservation_previously_marked_multiples_on_marked_change.0.0 --- --- --- --- --- --- --- --- --- --- --- --- --- inline_goal conservation_previously_marked_multiples_on_marked_change.0.0.0 --- --- --- --- --- --- --- --- --- --- --- --- --- split_vc conservation_previously_marked_multiples_on_marked_change.0.0.0.0 --- 0.01 --- --- --- --- --- --- --- --- --- --- --- conservation_previously_marked_multiples_on_marked_change.0.0.0.1 --- --- --- --- --- --- --- --- 0.13 --- --- --- --- remove zero,one,(-),(>),(<=),(>=),abs,even,odd,divides,prime,([]),singleton,cons,snoc,(++),inv_nexts,all_eliminated_marked,all_eliminated_marked_partial,not_marked_impl_next_not_marked,is_copy,not_marked_impl_next_not_marked_partial,all_primes,previously_marked_multiples,only_multiples_marked,prime_multiples_marked,inv_remove_products,ordered,all_inf_or_eq,Assoc1,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm1,Assoc,Mul_distr_l,Mul_distr_r,Unitary,NonTrivialRing,ZeroLessOne,CompatOrderAdd,CompatOrderMult,Abs_le,Abs_pos,Div_mod,Mod_bound,Div_unique,Div_bound,Mod_1,Div_inf,Mod_0,Div_1_left,Div_minus1_left,Mod_1_left,Mod_minus1_left,Div_mult,Mod_mult,Div_mod1,Div_bound1,Mod_bound1,Div_sign_pos,Div_sign_neg,Mod_sign_pos,Mod_sign_neg,Rounds_toward_zero,Div_11,Mod_11,Div_inf1,Mod_inf,Div_mult1,Mod_mult1,even_or_odd,even_not_odd,odd_not_even,even_odd,odd_even,even_even,odd_odd,even_2k,odd_2k1,even_mod2,divides'spec,divides_1_n,divides_0,divides_left,divides_right,divides_oppr,divides_oppl,divides_plusr,divides_minusr,divides_multl,divides_multr,divides_factorl,divides_factorr,divides_trans,divides_bounds,mod_divides_euclidean,divides_mod_euclidean,mod_divides_computer,divides_mod_computer,even_divides,odd_divides,not_prime_1,prime_2,prime_3,prime_divisors,small_divisors,even_prime,odd_prime,mult_croissance_locale,mult_croissance,comp_mult_2,div_croissance_locale1,div_croissance1,div_croissance_locale2,div_croissance2,div_mult_1,mult_borne_sous_exp,sq_ineq,divides_div,divides_inf,not_prime_divider_limits,no_prod_impl_no_divider,not_prime_impl_divisor_under_sqrt,(==)'spec,create'spec,empty'def,set'def,cons'spec,snoc'spec,([..])'spec,([..])'def,([_..])'def,([.._])'def,(++)'spec,conservation_all_eliminated_marked_on_marked_change,conservation_all_eliminated_marked_on_nexts_change,multiples_of_marked_are_marked,prev_and_new_impl_all_multiples_marked,conservation_only_multiples_marked,conservation_previously_marked_multiples conservation_previously_marked_multiples_on_marked_change.0.0.0.1.0 --- 0.10 --- --- --- --- --- --- 0.19 0.04 --- --- --- conservation_previously_marked_multiples_on_marked_change.0.0.0.2 --- --- --- --- --- --- --- --- --- --- --- --- --- inline_all conservation_previously_marked_multiples_on_marked_change.0.0.0.2.0 --- --- --- --- --- --- --- --- --- --- --- --- 0.16 VC for conservation_not_marked_impl_next_not_marked --- 0.33 --- --- --- --- --- --- --- --- --- --- --- VC for unchanged_other_elements --- 0.03 --- --- --- --- --- --- --- --- --- --- --- VC for t --- --- --- --- --- --- --- --- --- --- --- --- --- split_vc precondition --- 0.01 --- --- --- --- --- --- --- --- --- --- --- precondition --- 0.01 --- --- --- --- --- --- --- --- --- --- --- type invariant --- 0.02 --- --- --- --- --- --- --- --- --- --- --- type invariant --- 0.02 --- --- --- --- --- --- --- --- --- --- --- type invariant --- 0.03 --- --- --- --- --- --- --- --- --- --- --- type invariant --- 0.04 --- --- --- --- --- --- --- --- --- --- --- type invariant --- 0.02 --- --- --- --- --- --- --- --- --- --- --- type invariant --- 0.01 --- --- --- --- --- --- --- --- --- --- --- type invariant --- 0.03 --- --- --- --- --- --- --- --- --- --- --- VC for remove_products --- --- --- --- --- --- --- --- --- --- --- --- --- split_vc division by zero --- 0.02 --- --- --- --- --- --- --- --- --- --- --- integer overflow --- 0.04 --- --- --- --- --- --- --- --- --- --- --- precondition --- 0.02 --- --- --- --- --- --- --- --- --- --- --- precondition --- 0.02 --- --- --- --- --- --- --- --- --- --- --- assertion --- --- --- --- --- --- --- --- --- --- --- --- --- split_vc assertion --- 0.03 --- --- --- --- --- --- --- --- --- --- --- VC for remove_products --- 0.08 --- --- --- --- --- --- --- --- --- --- --- VC for remove_products --- 0.31 --- --- --- --- --- --- --- --- --- --- --- precondition --- 0.08 --- --- --- --- --- --- --- --- --- --- --- precondition --- 0.03 --- --- --- --- --- --- --- --- --- --- --- integer overflow --- 0.08 --- --- --- --- --- --- --- --- --- --- --- precondition --- --- --- --- --- 0.21 --- --- --- --- --- --- --- precondition --- --- --- --- --- --- --- --- --- --- --- --- --- assert (mod (int63'int n) 2 = 1) asserted formula --- 0.34 --- --- --- --- --- --- --- --- --- --- --- precondition --- 0.04 --- --- --- --- --- --- --- --- --- --- --- precondition --- --- --- --- --- --- --- --- --- --- --- --- --- split_vc precondition --- 0.03 --- --- --- --- --- --- --- --- --- --- --- precondition --- 0.11 --- --- --- --- --- --- --- --- --- --- --- precondition --- 0.11 --- --- --- --- --- --- --- --- --- --- --- precondition --- 0.03 --- --- --- --- --- --- --- --- --- --- --- assertion --- --- --- --- --- --- --- --- --- --- --- --- --- inline_goal assertion --- --- --- --- --- --- --- --- --- --- --- --- --- split_vc assertion --- 0.03 --- --- --- --- --- --- --- --- --- --- --- assertion --- 0.03 --- --- --- --- --- --- --- --- --- --- --- assertion --- 0.12 --- --- --- --- --- --- --- --- --- --- --- assertion --- 0.03 --- --- --- --- --- --- --- --- --- --- --- assertion --- --- --- --- --- --- --- --- --- --- --- --- --- split_vc assertion --- 0.03 --- --- --- --- --- --- --- --- --- --- --- assertion --- 0.13 --- --- --- --- --- --- --- --- --- --- --- VC for remove_products --- 0.24 --- --- --- --- --- --- --- --- --- --- --- assertion --- --- --- --- --- --- --- --- --- --- --- --- --- split_vc assertion --- 0.03 --- --- --- --- --- --- --- --- --- --- --- assertion --- 0.03 --- --- --- --- --- --- --- --- --- --- --- assertion --- 0.14 --- --- --- --- --- --- --- --- --- --- --- VC for remove_products --- 1.55 --- --- --- --- --- --- --- --- --- --- --- assertion --- --- --- --- --- --- --- --- --- --- --- --- --- split_vc assertion --- --- --- --- --- --- --- --- --- --- --- --- --- inline_goal assertion --- --- --- --- --- --- --- --- --- --- --- --- --- split_vc assertion --- 0.12 --- --- --- --- --- --- --- --- --- --- --- assertion --- 0.03 --- --- --- --- --- --- --- --- --- --- --- assertion --- 0.13 --- --- --- --- --- --- --- --- --- --- --- assertion --- 0.86 --- --- --- --- --- --- --- --- --- --- --- VC for remove_products 1.36 --- --- --- --- --- --- --- --- --- --- --- --- assertion --- --- --- --- --- --- --- --- --- --- --- --- --- split_vc assertion --- --- --- --- --- --- 9.50 --- --- --- --- --- --- VC for remove_products --- 0.64 --- --- --- --- 0.34 --- --- --- --- --- --- precondition --- 0.03 --- --- --- --- --- --- --- --- --- --- --- precondition --- 0.04 --- --- --- --- --- --- --- --- --- --- --- assertion --- 0.12 --- --- --- --- --- --- --- --- --- --- --- precondition --- 0.03 --- --- --- --- --- --- --- --- --- --- --- precondition --- 0.04 --- --- --- --- --- --- --- --- --- --- --- precondition --- --- --- --- --- --- --- --- --- --- --- --- --- split_vc precondition --- 0.04 --- --- --- --- --- --- --- --- --- --- --- precondition --- --- --- --- --- --- 0.18 --- --- --- --- --- --- precondition --- --- --- --- --- --- 0.45 --- --- --- --- --- --- precondition --- 0.04 --- --- --- --- --- --- --- --- --- --- --- precondition --- 0.04 --- --- --- --- --- --- --- --- --- --- --- precondition --- --- --- --- 1.01 --- --- --- --- --- --- --- --- precondition --- 0.04 --- --- --- --- --- --- --- --- --- --- --- precondition --- 0.04 --- --- --- --- --- --- --- --- --- --- --- precondition --- 0.17 --- --- --- --- --- --- --- --- --- --- --- precondition --- 0.04 --- --- --- --- --- --- --- --- --- --- --- assertion --- --- --- --- --- --- --- --- --- --- --- --- --- inline_goal assertion --- --- --- --- --- --- --- --- --- --- --- --- --- split_vc assertion --- 0.04 --- --- --- --- --- --- --- --- --- --- --- assertion --- 0.04 --- --- --- --- --- --- --- --- --- --- --- assertion --- 0.70 --- --- --- --- --- --- --- --- --- --- --- VC for remove_products --- 0.15 --- --- --- --- --- --- --- --- --- --- --- VC for remove_products --- --- --- --- --- --- --- --- --- --- --- --- --- case (j < x) true case --- 0.04 --- --- --- --- --- --- --- --- --- --- --- false case --- --- --- --- --- --- --- --- --- --- --- --- --- unfold all_eliminated_marked_partial in Requires4 false case --- --- --- --- --- --- 8.08 --- --- --- --- --- --- variant decrease --- --- --- --- --- --- 0.46 --- --- --- --- --- 0.11 precondition --- --- --- --- --- --- --- --- --- --- --- --- --- split_vc precondition --- 0.04 --- --- --- --- --- --- --- --- --- --- --- precondition --- 0.04 --- --- --- --- --- --- --- --- --- --- --- precondition --- 0.04 --- --- --- --- --- --- --- --- --- --- --- precondition --- 0.04 --- --- --- --- --- --- --- --- --- --- --- precondition --- 0.04 --- --- --- --- --- --- --- --- --- --- --- precondition --- 0.04 --- --- --- --- --- --- --- --- --- --- --- precondition --- --- --- --- --- --- 0.53 --- --- --- --- --- 0.12 precondition --- --- --- --- --- --- 0.28 --- --- --- --- --- 0.12 precondition --- --- --- --- --- --- 0.27 0.55 --- --- --- --- --- precondition --- --- --- --- --- --- --- --- --- --- --- --- --- split_vc precondition --- --- --- --- --- --- --- --- --- --- --- --- --- inline_goal precondition --- --- --- --- --- --- --- --- --- --- --- --- --- split_all_full VC for remove_products --- 0.16 --- --- --- --- --- --- --- --- --- --- --- VC for remove_products --- 0.42 --- --- --- --- --- --- --- --- --- --- --- VC for remove_products --- --- --- --- --- --- --- --- --- --- --- --- --- unfold inv_remove_products in Requires8 VC for remove_products --- --- --- --- --- --- --- --- --- --- --- --- --- split_premise_right VC for remove_products --- --- --- --- --- --- --- --- --- --- --- --- --- inline_goal VC for remove_products --- --- --- --- --- --- --- --- --- --- --- --- --- unfold all_primes in Requires11 VC for remove_products --- --- --- --- --- --- --- --- --- --- --- --- --- split_vc VC for remove_products --- --- --- --- --- --- --- --- --- --- --- --- --- instantiate Requires11 i VC for remove_products --- 0.56 --- --- --- --- --- --- --- --- --- --- --- VC for remove_products --- --- --- --- --- --- --- --- --- --- --- --- --- instantiate Requires11 i VC for remove_products --- 0.56 --- --- --- --- --- --- --- --- --- --- --- VC for remove_products --- 0.16 --- --- --- --- --- --- --- --- --- --- --- VC for remove_products --- 0.40 --- --- --- --- --- --- --- --- --- --- --- VC for remove_products --- 0.16 --- --- --- --- --- --- --- --- --- --- --- precondition --- --- --- --- --- 0.10 --- --- --- --- --- --- --- precondition --- 0.92 --- --- --- --- --- --- --- --- --- --- --- precondition --- 0.05 --- --- --- --- --- --- --- --- --- --- --- precondition --- --- --- --- --- --- 0.29 --- --- --- --- --- --- precondition --- 0.05 --- --- --- --- --- --- --- --- --- --- --- precondition --- --- --- --- --- --- --- --- --- --- --- --- --- inline_goal precondition --- --- --- --- --- --- --- --- --- --- --- --- --- split_vc precondition --- 0.16 --- --- --- --- --- --- --- --- --- --- --- precondition --- 0.16 --- --- --- --- --- --- --- --- --- --- --- precondition --- 0.04 --- --- --- --- --- --- --- --- --- --- --- precondition --- --- --- --- --- --- --- --- --- --- --- --- --- case (i = p) true case (precondition) --- --- --- --- --- --- --- --- --- --- --- --- --- remove H24,H23,H22 true case (precondition) --- 2.71 --- --- --- --- --- --- --- --- --- --- --- false case (precondition) --- --- --- --- --- --- --- --- --- --- --- --- --- assert (forall i. 0 <= i < div (length marked_old - 1) n -> i <> p -> (nexts t)[i] = (nexts t1)[i]) asserted formula --- 0.20 --- --- --- --- --- --- --- --- --- --- --- false case (precondition) --- --- --- --- --- --- --- --- --- --- --- --- --- inline_all false case (precondition) --- --- --- --- --- --- --- --- --- --- --- 0.11 --- precondition --- 0.39 --- --- --- --- --- --- --- --- --- --- --- precondition --- --- --- --- --- --- --- --- --- --- --- --- --- inline_goal precondition --- --- --- --- --- --- --- --- --- --- --- --- --- split_vc precondition --- 0.16 --- --- --- --- --- --- --- --- --- --- --- precondition --- 0.17 --- --- --- --- --- --- --- --- --- --- --- precondition --- 0.04 --- --- --- --- --- --- --- --- --- --- --- precondition --- 0.19 --- --- --- --- --- --- --- --- --- --- --- precondition --- --- --- --- --- --- --- --- --- --- --- --- --- unfold not_marked_impl_next_not_marked_partial in Requires8 precondition --- --- --- --- --- --- --- --- --- --- --- --- --- split_premise_right precondition --- --- --- --- --- --- --- --- --- --- --- --- --- instantiate Requires8 i precondition --- --- --- --- --- --- 0.64 --- --- --- --- --- --- precondition --- 0.05 --- --- --- --- --- --- --- --- --- --- --- postcondition --- 0.04 --- --- --- --- --- --- --- --- --- --- --- postcondition --- 0.04 --- --- --- --- --- --- --- --- --- --- --- postcondition --- 0.04 --- --- --- --- --- --- --- --- --- --- --- postcondition --- 0.04 --- --- --- --- --- --- --- --- --- --- --- postcondition --- 0.04 --- --- --- --- --- --- --- --- --- --- --- postcondition --- 0.04 --- --- --- --- --- --- --- --- --- --- --- assertion --- --- --- --- --- --- 0.86 --- --- --- --- --- 0.09 variant decrease --- --- --- --- --- --- --- --- --- --- --- --- --- split_vc variant decrease --- 0.03 --- --- --- --- --- --- --- --- --- --- --- variant decrease --- --- --- --- --- --- 0.43 --- --- --- --- --- 0.10 precondition --- --- --- --- --- --- --- --- --- --- --- --- --- split_vc precondition --- 0.03 --- --- --- --- --- --- --- --- --- --- --- precondition --- 0.03 --- --- --- --- --- --- --- --- --- --- --- precondition --- 0.04 --- --- --- --- --- --- --- --- --- --- --- precondition --- 0.04 --- --- --- --- --- --- --- --- --- --- --- precondition --- 0.03 --- --- --- --- --- --- --- --- --- --- --- precondition --- 0.03 --- --- --- --- --- --- --- --- --- --- --- precondition --- --- --- --- --- --- 0.41 --- --- --- --- --- 0.08 precondition --- 0.03 --- --- --- --- --- --- --- --- --- --- --- precondition --- --- --- --- --- --- 0.38 0.46 --- --- --- --- --- precondition --- --- --- --- --- --- --- --- --- --- --- --- --- split_vc precondition --- --- --- --- --- --- --- --- --- --- --- --- --- inline_goal precondition --- --- --- --- --- --- --- --- --- --- --- --- --- split_all_full VC for remove_products --- 0.13 --- --- --- --- --- --- --- --- --- --- --- VC for remove_products --- 0.29 --- --- --- --- --- --- --- --- --- --- --- VC for remove_products --- --- --- --- --- --- --- --- --- --- --- --- --- unfold inv_remove_products in Requires8 VC for remove_products --- --- --- --- --- --- --- --- --- --- --- --- --- split_premise_right VC for remove_products --- --- --- --- --- --- --- --- --- --- --- --- --- inline_goal VC for remove_products --- --- --- --- --- --- --- --- --- --- --- --- --- unfold all_primes in Requires11 VC for remove_products --- --- --- --- --- --- --- --- --- --- --- --- --- split_vc VC for remove_products --- --- --- --- --- --- --- --- --- --- --- --- --- instantiate Requires11 i VC for remove_products --- 0.36 --- --- --- --- --- --- --- --- --- --- --- VC for remove_products --- --- --- --- --- --- --- --- --- --- --- --- --- instantiate Requires11 i VC for remove_products --- 0.34 --- --- --- --- --- --- --- --- --- --- --- VC for remove_products --- 0.14 --- --- --- --- --- --- --- --- --- --- --- VC for remove_products --- 0.27 --- --- --- --- --- --- --- --- --- --- --- VC for remove_products --- 0.13 --- --- --- --- --- --- --- --- --- --- --- precondition --- --- --- --- --- 0.08 --- --- --- --- --- --- --- precondition --- 0.64 --- --- --- --- --- --- --- --- --- --- --- precondition --- 0.04 --- --- --- --- --- --- --- --- --- --- --- precondition --- 0.78 --- --- --- --- --- --- --- --- --- --- --- precondition --- --- --- --- --- --- --- --- --- --- --- --- 0.10 precondition --- 0.04 --- --- --- --- --- --- --- --- --- --- --- precondition --- 0.04 --- --- --- --- --- --- --- --- --- --- --- precondition --- --- --- --- --- --- --- --- --- --- --- --- --- inline_goal precondition --- --- --- --- --- --- --- --- --- --- --- --- --- split_vc precondition --- 0.14 --- --- --- --- --- --- --- --- --- --- --- precondition --- 0.14 --- --- --- --- --- --- --- --- --- --- --- precondition --- 0.04 --- --- --- --- --- --- --- --- --- --- --- precondition --- 0.17 --- --- --- --- --- --- --- --- --- --- --- precondition --- --- --- --- --- --- --- --- --- --- --- --- --- unfold not_marked_impl_next_not_marked_partial in Requires8 precondition --- --- --- --- --- --- --- --- --- --- --- --- --- split_premise_right precondition --- --- --- --- --- --- --- --- --- --- --- --- --- instantiate Requires8 i precondition --- --- --- --- --- --- 0.52 --- --- --- --- --- --- precondition --- 0.04 --- --- --- --- --- --- --- --- --- --- --- postcondition --- 0.04 --- --- --- --- --- --- --- --- --- --- --- postcondition --- 0.04 --- --- --- --- --- --- --- --- --- --- --- postcondition --- 0.03 --- --- --- --- --- --- --- --- --- --- --- postcondition --- 0.04 --- --- --- --- --- --- --- --- --- --- --- postcondition --- 0.03 --- --- --- --- --- --- --- --- --- --- --- postcondition --- 0.03 --- --- --- --- --- --- --- --- --- --- --- assertion --- --- --- --- --- --- --- --- --- --- --- --- --- split_vc assertion --- 0.03 --- --- --- --- --- --- --- --- --- --- --- VC for remove_products --- --- --- --- --- --- --- --- --- --- --- --- 0.08 VC for remove_products --- 0.61 --- --- --- --- --- --- --- --- --- --- --- VC for remove_products --- 0.12 --- --- --- --- --- --- --- --- --- --- --- VC for remove_products --- 0.10 --- --- --- --- --- --- --- --- --- --- --- precondition --- --- --- --- --- --- --- --- --- --- --- --- --- split_vc precondition --- --- --- --- --- --- 0.24 0.62 --- --- --- --- --- precondition --- 0.03 --- --- --- --- --- --- --- --- --- --- --- VC for remove_products --- --- --- --- --- --- --- --- --- --- --- --- --- split_vc VC for remove_products --- --- --- --- --- --- --- --- --- --- --- --- --- split_vc VC for remove_products --- --- --- 0.51 --- --- --- --- --- --- --- --- --- VC for remove_products --- --- --- --- --- --- 0.15 --- --- --- --- --- --- VC for remove_products --- --- --- --- --- --- 0.31 --- --- --- --- --- 0.07 VC for remove_products --- 0.03 --- --- --- --- --- --- --- --- --- --- --- VC for remove_products --- --- --- --- --- --- --- --- --- --- --- --- 0.09 postcondition --- 0.03 --- --- --- --- --- --- --- --- --- --- --- postcondition --- 0.02 --- --- --- --- --- --- --- --- --- --- --- postcondition --- 0.03 --- --- --- --- --- --- --- --- --- --- --- postcondition --- 0.02 --- --- --- --- --- --- --- --- --- --- --- postcondition --- --- --- --- --- --- --- --- --- --- --- --- --- inline_goal postcondition --- --- --- --- --- --- --- --- --- --- --- --- --- split_vc postcondition --- 0.06 --- --- --- --- --- --- --- --- --- --- --- postcondition --- 0.07 --- --- --- --- --- --- --- --- --- --- --- postcondition --- 0.03 --- --- --- --- --- --- --- --- --- --- --- postcondition --- --- --- --- --- --- --- --- --- --- --- --- --- unfold prime_multiples_marked in Requires2 postcondition --- --- --- --- --- --- --- --- --- --- --- --- --- split_all_right postcondition --- --- --- --- --- --- --- --- --- --- --- --- --- case (i < (nexts t)[x]) true case (postcondition) --- 0.08 --- --- --- --- --- --- --- --- --- --- --- false case (postcondition) --- 0.16 --- --- --- --- --- --- --- --- --- --- --- postcondition --- 0.03 --- --- --- --- --- --- --- --- --- --- --- precondition --- --- --- --- --- --- --- --- --- --- --- --- --- split_vc precondition --- --- --- --- --- --- 0.41 0.52 --- --- --- --- --- precondition --- 0.03 --- --- --- --- --- --- --- --- --- --- --- VC for remove_products --- --- 2.00 --- --- --- --- --- --- --- --- --- --- VC for remove_products --- --- --- --- --- --- 0.43 --- --- --- --- --- 0.08 VC for remove_products --- 0.02 --- --- --- --- --- --- --- --- --- --- --- VC for remove_products --- --- --- --- --- --- --- --- --- --- --- --- 0.09 postcondition --- 0.02 --- --- --- --- --- --- --- --- --- --- --- postcondition --- 0.02 --- --- --- --- --- --- --- --- --- --- --- postcondition --- 0.03 --- --- --- --- --- --- --- --- --- --- --- postcondition --- 0.03 --- --- --- --- --- --- --- --- --- --- --- postcondition --- 0.06 --- --- --- --- --- --- --- --- --- --- --- postcondition --- 0.03 --- --- --- --- --- --- --- --- --- --- --- precondition --- 0.03 --- --- --- --- --- --- --- --- --- --- --- precondition 0.04 --- --- --- --- --- --- --- --- --- --- --- --- remove zero1,one1,(-),(>),(<=),(>=),abs,int63'maxInt,int63'minInt,min_int63,max_int63,to_int,in_bounds,zero,one,even,odd,divides,prime,([]),singleton,cons,snoc,(++),inv_nexts,all_eliminated_marked,all_eliminated_marked_partial,not_marked_impl_next_not_marked,is_copy,not_marked_impl_next_not_marked_partial,all_primes,all_multiples_marked,previously_marked_multiples,prime_multiples_marked,inv_remove_products,ordered,all_inf_or_eq,max,marked_old,Assoc1,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm1,Assoc,Mul_distr_l,Mul_distr_r,Comm,Unitary,NonTrivialRing,Refl,Trans,Antisymm,Total,ZeroLessOne,CompatOrderAdd,CompatOrderMult,Abs_le,Abs_pos,Div_mod,Mod_bound,Div_unique,Div_bound,Mod_1,Div_1,Div_inf,Div_inf_neg,Mod_0,Div_1_left,Div_minus1_left,Mod_1_left,Mod_minus1_left,Div_mult,Mod_mult,Div_mod1,Div_bound1,Mod_bound1,Div_sign_pos,Div_sign_neg,Mod_sign_pos,Mod_sign_neg,Rounds_toward_zero,Div_11,Mod_11,Div_inf1,Mod_inf,Div_mult1,Mod_mult1,to_int_in_bounds,extensionality,max_int'def,min_int'def,even_or_odd,even_not_odd,odd_not_even,even_odd,odd_even,even_even,odd_odd,even_2k,odd_2k1,even_mod2,divides'spec,divides_refl,divides_1_n,divides_0,divides_left,divides_right,divides_oppr,divides_oppl,divides_oppr_rev,divides_oppl_rev,divides_plusr,divides_minusr,divides_multl,divides_multr,divides_factorl,divides_factorr,divides_n_1,divides_antisym,divides_trans,divides_bounds,mod_divides_euclidean,divides_mod_euclidean,mod_divides_computer,divides_mod_computer,even_divides,odd_divides,not_prime_1,prime_2,prime_3,prime_divisors,small_divisors,even_prime,odd_prime,mult_croissance_locale,mult_croissance,comp_mult_2,div_croissance_locale1,div_croissance1,div_croissance_locale2,div_croissance2,div_mult_1,mult_borne_sous_exp,sq_ineq,divides_div,divides_inf,not_prime_divider_limits,no_prod_impl_no_divider,not_prime_impl_divisor_under_sqrt,length_nonnegative,(==)'spec,create'spec,empty'def,set'spec,set'def,([<-])'def,singleton'spec,cons'spec,snoc'spec,([..])'spec,([..])'def,([_..])'def,([.._])'def,(++)'spec,conservation_all_eliminated_marked_on_marked_change,conservation_all_eliminated_marked_on_nexts_change,multiples_of_marked_are_marked,prev_and_new_impl_all_multiples_marked,conservation_only_multiples_marked,conservation_previously_marked_multiples,conservation_previously_marked_multiples_on_marked_change,conservation_not_marked_impl_next_not_marked,unchanged_other_elements,t'invariant,H2,H1,H,Requires4,Requires3,Requires1,Ensures1,Ensures,Requires precondition 0.00 0.00 --- --- --- --- --- --- --- --- --- --- 0.02 integer overflow --- 0.03 --- --- --- --- --- --- --- --- --- --- --- precondition --- 0.02 --- --- --- --- --- --- --- --- --- --- --- precondition --- --- --- --- --- --- --- --- --- --- --- --- --- assert (mod (int63'int n) 2 = 1) asserted formula --- --- --- --- --- --- 0.17 --- --- --- --- --- 0.06 precondition --- 0.08 --- --- --- --- --- --- --- --- --- --- --- precondition --- 0.04 --- --- --- --- --- --- --- --- --- --- --- precondition --- 0.02 --- --- --- --- --- --- --- --- --- --- --- assertion --- --- --- --- --- --- --- --- --- --- --- --- --- split_vc assertion --- 0.06 --- --- --- --- --- --- --- --- --- --- --- assertion --- --- --- --- --- --- 0.37 --- --- --- --- --- --- VC for remove_products --- --- --- --- --- --- 0.17 --- --- --- --- --- 0.07 VC for remove_products --- 0.04 --- --- --- --- --- --- --- --- --- --- --- VC for remove_products --- 0.04 --- --- --- --- --- --- --- --- --- --- --- precondition --- --- --- --- --- --- --- --- --- --- --- --- --- split_vc precondition --- 0.02 --- --- --- --- --- --- --- --- --- --- --- precondition --- 0.02 --- --- --- --- --- --- --- --- --- --- --- precondition --- 0.02 --- --- --- --- --- --- --- --- --- --- --- precondition --- 0.02 --- --- --- --- --- --- --- --- --- --- --- precondition --- --- --- --- --- --- 0.20 --- --- --- --- --- 0.06 precondition --- 0.02 --- --- --- --- --- --- --- --- --- --- --- precondition --- --- --- --- --- --- 0.24 --- --- --- --- --- 0.07 precondition --- 0.02 --- --- --- --- --- --- --- --- --- --- --- precondition --- --- --- --- --- --- --- --- --- --- --- --- 0.08 precondition --- --- --- --- --- --- --- --- --- --- --- --- --- inline_goal precondition --- --- --- --- --- --- --- --- --- --- --- --- --- split_vc precondition --- --- --- --- --- --- 0.18 --- --- --- --- --- 0.07 precondition --- --- --- --- --- --- --- --- --- --- --- --- 0.06 precondition --- --- --- --- --- --- --- --- --- --- --- --- --- assert (n * n > n) asserted formula --- --- --- --- --- --- --- --- --- --- --- --- 0.07 precondition --- --- --- --- --- --- 0.35 --- --- --- --- --- --- precondition --- --- --- --- --- --- 0.15 --- --- --- --- --- 0.06 precondition --- --- --- --- --- --- --- --- --- --- --- --- 0.07 precondition --- --- --- --- --- --- 0.16 --- --- --- --- --- 0.06 precondition --- --- --- --- --- --- --- --- --- --- --- --- 0.08 precondition --- --- --- --- --- --- 0.14 --- --- --- --- --- 0.07 precondition --- --- --- --- --- --- 0.22 --- --- --- --- --- --- precondition --- --- --- --- 1.41 --- --- --- --- --- --- --- --- remove zero1,one1,(-),(>),(<=),(>=),abs,int63'maxInt,int63'minInt,min_int63,max_int63,to_int,in_bounds,zero,one,even,odd,divides,prime,([]),singleton,cons,snoc,(++),inv_nexts,not_marked_impl_next_not_marked,is_copy,not_marked_impl_next_not_marked_partial,all_primes,all_multiples_marked,previously_marked_multiples,only_multiples_marked,prime_multiples_marked,inv_remove_products,ordered,all_inf_or_eq,max,marked_copy,Assoc1,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm1,Assoc,Mul_distr_l,Mul_distr_r,Comm,Unitary,NonTrivialRing,Refl,Trans,Antisymm,Total,ZeroLessOne,CompatOrderAdd,CompatOrderMult,Abs_le,Abs_pos,Div_mod,Mod_bound,Div_unique,Div_bound,Mod_1,Div_1,Div_inf,Div_inf_neg,Mod_0,Div_1_left,Div_minus1_left,Mod_1_left,Mod_minus1_left,Div_mult,Mod_mult,Div_mod1,Div_bound1,Mod_bound1,Div_sign_pos,Div_sign_neg,Mod_sign_pos,Mod_sign_neg,Rounds_toward_zero,Div_11,Mod_11,Div_inf1,Mod_inf,Div_mult1,Mod_mult1,to_int_in_bounds,extensionality,max_int'def,min_int'def,even_or_odd,even_not_odd,odd_not_even,even_odd,odd_even,even_even,odd_odd,even_2k,odd_2k1,even_mod2,divides'spec,divides_refl,divides_1_n,divides_0,divides_left,divides_right,divides_oppr,divides_oppl,divides_oppr_rev,divides_oppl_rev,divides_plusr,divides_minusr,divides_multl,divides_multr,divides_factorl,divides_factorr,divides_n_1,divides_antisym,divides_trans,divides_bounds,mod_divides_euclidean,divides_mod_euclidean,mod_divides_computer,divides_mod_computer,even_divides,odd_divides,not_prime_1,prime_2,prime_3,prime_divisors,small_divisors,even_prime,odd_prime,mult_croissance_locale,mult_croissance,comp_mult_2,div_croissance_locale1,div_croissance1,div_croissance_locale2,div_croissance2,div_mult_1,mult_borne_sous_exp,sq_ineq,divides_div,divides_inf,not_prime_divider_limits,no_prod_impl_no_divider,not_prime_impl_divisor_under_sqrt,length_nonnegative,(==)'spec,create'spec,empty'def,set'spec,set'def,([<-])'def,singleton'spec,cons'spec,snoc'spec,([..])'spec,([..])'def,([_..])'def,([.._])'def,(++)'spec,conservation_all_eliminated_marked_on_marked_change,conservation_all_eliminated_marked_on_nexts_change,multiples_of_marked_are_marked,prev_and_new_impl_all_multiples_marked,conservation_only_multiples_marked,conservation_previously_marked_multiples,conservation_previously_marked_multiples_on_marked_change,conservation_not_marked_impl_next_not_marked,unchanged_other_elements,H4,H3,H2,Requires8,Requires7,Requires6,Requires5,Ensures5,Ensures4,Ensures3,Ensures2,H,Ensures1,Ensures,Assert,Requires3,Requires2,Requires1,Requires precondition --- 0.10 --- --- 0.02 --- 0.06 --- --- --- --- --- --- precondition --- --- --- --- --- --- --- --- --- --- --- --- --- inline_goal precondition --- --- --- --- --- --- --- --- --- --- --- --- --- split_vc precondition --- --- --- --- --- --- 0.15 --- --- --- --- --- 0.06 precondition --- --- --- --- --- --- 0.18 --- --- --- --- --- 0.06 precondition --- 0.02 --- --- --- --- 0.15 --- --- --- --- --- --- precondition --- --- --- --- --- --- --- --- --- --- --- --- 0.07 precondition --- --- --- --- --- --- --- --- --- --- --- --- --- split_vc precondition --- --- --- --- --- --- --- --- --- --- --- --- --- inline_goal precondition --- --- --- --- --- --- --- --- --- --- --- --- --- split_all_full VC for remove_products --- --- --- --- --- --- 0.20 --- --- --- --- --- 0.08 VC for remove_products --- 0.02 --- --- --- --- 0.11 --- --- --- --- --- --- VC for remove_products --- --- --- --- --- --- 0.28 --- --- --- --- --- 0.08 VC for remove_products --- --- --- --- --- --- 0.26 --- --- --- --- --- --- precondition --- --- --- --- --- --- --- --- --- --- --- --- --- inline_goal precondition --- --- --- --- --- --- --- --- --- --- --- --- --- split_vc precondition --- --- --- --- --- --- 0.15 --- --- --- --- --- 0.08 precondition --- --- --- --- --- --- 0.18 --- --- --- --- --- 0.06 precondition --- 0.02 --- --- --- --- 0.15 --- --- --- --- --- 0.06 precondition --- --- --- --- --- --- --- --- --- --- --- --- 0.06 precondition --- --- --- --- --- --- --- --- --- --- --- --- --- inline_all precondition --- --- --- --- --- --- --- --- --- --- --- --- 0.61 precondition --- 0.02 --- --- --- --- 0.15 --- --- --- --- --- 0.07 precondition --- 0.05 --- --- --- --- 0.18 --- --- --- --- --- 0.06 precondition --- 0.02 --- --- --- --- 0.11 --- --- --- --- --- 0.02 precondition --- 0.02 --- --- --- --- 0.11 --- --- --- --- --- 0.02 precondition --- 0.02 --- --- --- --- 0.11 --- --- --- --- --- 0.02 precondition --- 0.02 --- --- --- --- 0.10 --- --- --- --- --- 0.02 precondition --- 0.02 --- --- --- --- 0.12 --- --- --- --- --- 0.02 precondition --- --- --- --- --- --- 0.28 --- --- --- --- --- 0.07 precondition --- 0.02 --- --- --- --- 0.12 --- --- --- --- --- 0.02 precondition --- 0.02 --- --- --- --- 0.12 --- --- --- --- --- 0.02 precondition --- 0.05 --- --- --- --- 0.20 --- --- --- --- --- 0.07 precondition --- 0.02 --- --- --- --- 0.12 --- --- --- --- --- 0.02 precondition --- 0.02 --- --- --- --- 0.11 --- --- --- --- --- 0.02 postcondition --- 0.02 --- --- --- --- 0.12 --- --- --- --- --- 0.01 postcondition --- 0.02 --- --- --- --- 0.11 --- --- --- --- --- 0.02 postcondition --- 0.02 --- --- --- --- 0.11 --- --- --- --- --- 0.02 postcondition --- --- --- --- --- --- --- --- --- --- --- --- --- inline_goal postcondition --- --- --- --- --- --- --- --- --- --- --- --- --- split_vc postcondition --- --- --- --- --- --- --- --- --- --- --- --- --- unfold only_multiples_marked in Ensures5 postcondition --- --- --- --- --- --- --- --- --- --- --- --- --- instantiate Ensures5 k postcondition 0.82 --- --- --- --- --- --- --- --- --- --- --- --- remove zero1,one1,(-),(>),(<=),(>=),abs,int63'maxInt,int63'minInt,min_int63,max_int63,to_int,in_bounds,zero,one,even,odd,divides,prime,([]),singleton,cons,snoc,(++),all_eliminated_marked,all_eliminated_marked_partial,not_marked_impl_next_not_marked,is_copy,not_marked_impl_next_not_marked_partial,all_primes,all_multiples_marked,previously_marked_multiples,only_multiples_marked,prime_multiples_marked,inv_remove_products,ordered,all_inf_or_eq,max,marked_old,marked_copy,Assoc1,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm1,Assoc,Mul_distr_l,Mul_distr_r,Comm,Unitary,NonTrivialRing,Refl,Trans,Antisymm,Total,ZeroLessOne,CompatOrderAdd,CompatOrderMult,Abs_le,Abs_pos,Div_mod,Mod_bound,Div_unique,Div_bound,Mod_1,Div_1,Div_inf,Div_inf_neg,Mod_0,Div_1_left,Div_minus1_left,Mod_1_left,Mod_minus1_left,Div_mult,Mod_mult,Div_mod1,Div_bound1,Mod_bound1,Div_sign_pos,Div_sign_neg,Mod_sign_pos,Mod_sign_neg,Rounds_toward_zero,Div_11,Mod_11,Div_inf1,Mod_inf,Div_mult1,Mod_mult1,to_int_in_bounds,extensionality,max_int'def,min_int'def,even_or_odd,even_not_odd,odd_not_even,even_odd,odd_even,even_even,odd_odd,even_2k,odd_2k1,even_mod2,divides'spec,divides_refl,divides_1_n,divides_0,divides_left,divides_right,divides_oppr,divides_oppl,divides_oppr_rev,divides_oppl_rev,divides_plusr,divides_minusr,divides_multl,divides_multr,divides_factorl,divides_factorr,divides_n_1,divides_antisym,divides_trans,divides_bounds,mod_divides_euclidean,divides_mod_euclidean,mod_divides_computer,divides_mod_computer,even_divides,odd_divides,not_prime_1,prime_2,prime_3,prime_divisors,small_divisors,even_prime,odd_prime,mult_croissance_locale,mult_croissance,comp_mult_2,div_croissance_locale1,div_croissance1,div_croissance_locale2,div_croissance2,div_mult_1,mult_borne_sous_exp,sq_ineq,divides_div,divides_inf,not_prime_divider_limits,no_prod_impl_no_divider,not_prime_impl_divisor_under_sqrt,length_nonnegative,(==)'spec,create'spec,empty'def,set'spec,set'def,([<-])'def,singleton'spec,cons'spec,snoc'spec,([..])'spec,([..])'def,([_..])'def,([.._])'def,(++)'spec,conservation_all_eliminated_marked_on_marked_change,conservation_all_eliminated_marked_on_nexts_change,multiples_of_marked_are_marked,prev_and_new_impl_all_multiples_marked,conservation_only_multiples_marked,conservation_previously_marked_multiples,conservation_previously_marked_multiples_on_marked_change,conservation_not_marked_impl_next_not_marked,unchanged_other_elements,H8,H6,Requires3,Requires2,Requires1,Requires,Ensures16,Ensures15,Ensures14,Ensures13,H5,Ensures12,Ensures11,Assert,Ensures10,Ensures9,Ensures8,Ensures7,Ensures6,Ensures5,Ensures4,Ensures3,Ensures2,Ensures1,Ensures postcondition 0.06 0.05 --- --- --- --- --- --- --- --- --- --- 0.02 VC for previously_marked_multiples_impl_prime --- --- --- --- --- --- --- --- --- --- --- --- --- split_vc assertion --- --- --- --- --- --- --- --- --- --- --- --- --- split_vc assertion --- --- --- --- --- --- --- --- --- --- --- --- --- inline_all assertion --- --- --- --- --- --- --- --- --- --- --- --- 0.10 VC for previously_marked_multiples_impl_prime --- 0.45 --- --- --- --- --- --- --- --- --- --- --- postcondition --- 0.03 --- --- --- --- 0.16 --- --- --- --- --- 0.06 VC for only_multiples_marked_impl_not_marked --- --- --- --- --- --- --- --- --- --- --- --- --- split_vc assertion --- 0.03 --- --- --- --- --- --- --- --- --- --- --- postcondition --- 0.53 --- --- --- --- --- --- --- --- --- --- ---