def Hex.Nat.primeTableBound : Nat

Exclusive upper bound of the committed prime table. The accepted 100000 policy is the largest measured candidate inside the fresh-replay build budget; primeTable lists every prime below it.

Equations

• Hex.Nat.primeTableBound = 100000

def Hex.Nat.primeTable : Array Nat

Every prime below primeTableBound, ascending. A committed literal; mem_primeTable_prime and mem_primeTable_of_prime are the two membership directions, so the generator that produced the literal is untrusted.

Equations

• One or more equations did not get rendered due to their size.

def Hex.Nat.ascAdj : List Nat → Bool

Adjacent strict ascent of a list, structurally: true iff consecutive entries strictly increase.

Equations

• Hex.Nat.ascAdj [] = true
• Hex.Nat.ascAdj [head] = true
• Hex.Nat.ascAdj (a :: b :: rest) = (decide (a < b) && Hex.Nat.ascAdj (b :: rest))

theorem Hex.Nat.primeTable_sorted : List.Pairwise (fun (x1 x2 : Nat) => x1 < x2) primeTable.toList

The committed table is strictly ascending.

def Hex.Nat.binSearchGo (a : Array Nat) (n : Nat) : Nat → Nat → Nat → Bool

Fuel-bounded binary search for n in the sorted array a over the half-open index range [lo, hi).

Equations

• One or more equations did not get rendered due to their size.
• Hex.Nat.binSearchGo a n 0 x✝¹ x✝ = false

def Hex.Nat.tableSearch (n : Nat) : Bool

Membership in the committed prime table, by binary search.

Equations

• Hex.Nat.tableSearch n = Hex.Nat.binSearchGo Hex.Nat.primeTable n (Hex.Nat.primeTable.size + 1) 0 Hex.Nat.primeTable.size

def Hex.Nat.primeBits : Nat

The final verified sieve state underlying the committed prime table.

Equations

• One or more equations did not get rendered due to their size.

def Hex.Nat.isTablePrime (n : Nat) : Bool

Membership in the committed prime table. Kernel reduction reads a bit from the already verified final sieve state; compiled code uses binary search through isTablePrime_eq_tableSearch.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.Nat.isTablePrime_iff {n : Nat} : isTablePrime n = true ↔ n ∈ primeTable

A lookup succeeds exactly on members of the committed table.

@[csimp]

theorem Hex.Nat.isTablePrime_eq_tableSearch : isTablePrime = tableSearch

Compiled lookup retains binary search; the equality protects both successful and unsuccessful lookups at every input.

theorem Hex.Nat.mem_primeTable_prime {n : Nat} (h : n ∈ primeTable) : Prime n

Every table entry is prime: the committed literal read back through the verified sieve run.

theorem Hex.Nat.mem_primeTable_of_prime {n : Nat} (hp : Prime n) (hlt : n < primeTableBound) : n ∈ primeTable

Every prime below the bound is a table entry: completeness through the sieve's completeness direction, which is what lets a caller conclude anything from a failed lookup.

def Hex.Nat.primesIn (lo hi : Nat) : Array Nat

The primes in [lo, hi), ascending. Runtime decision through the isPrimeTrial-backed Decidable instance; the committed table plays no role, so the range is unrestricted.

Equations

• Hex.Nat.primesIn lo hi = (List.filter (fun (n : Nat) => decide (Hex.Nat.Prime n)) (List.range' lo (hi - lo))).toArray

theorem Hex.Nat.mem_primesIn {lo hi n : Nat} : n ∈ primesIn lo hi ↔ lo ≤ n ∧ n < hi ∧ Prime n

Membership in primesIn lo hi is exactly primality in the half-open interval [lo, hi).