Primes — primality test, prime list, factorization
Trial division up to √n decides primality. primes_up_to collects them into a list. factorize peels off prime factors smallest-first. Everything stays in plain Int arithmetic with while loops.
A Soma program from the math part of the verified corpus: 76 lines, cells Primes, PrimeTests. It passes soma check with soma 3.2.4.
How it is built
The cell Primes declares 4 signals in its face: is_prime(n: Int) -> Bool, primes_up_to(n: Int) -> List, factorize(n: Int) -> List and run() -> Map. Handlers: is_prime (line 20), primes_up_to (line 32), factorize (line 40) and run (line 55).
The file also holds 1 test cell (PrimeTests) with 7 assertions, run by soma test.
The source
primes.cell
// ============================================================================
// Primes — primality test, prime list, factorization
// ============================================================================
//
// Trial division up to √n decides primality. primes_up_to collects them into
// a list. factorize peels off prime factors smallest-first. Everything stays
// in plain Int arithmetic with while loops.
//
// soma run primes.cell run
// ============================================================================
cell Primes {
face {
signal is_prime(n: Int) -> Bool
signal primes_up_to(n: Int) -> List
signal factorize(n: Int) -> List
signal run() -> Map
}
on is_prime(n: Int) {
if n < 2 { return false }
if n < 4 { return true }
if n % 2 == 0 { return false }
let i = 3
while i * i <= n {
if n % i == 0 { return false }
i = i + 2
}
return true
}
on primes_up_to(n: Int) {
let ps = []
for i in range(2, n + 1) {
if is_prime(i) { ps = push(ps, i) }
}
return ps
}
on factorize(n: Int) {
let m = n
let factors = []
let d = 2
while d * d <= m {
while m % d == 0 {
factors = push(factors, d)
m = idiv(m, d)
}
d = d + 1
}
if m > 1 { factors = push(factors, m) }
return factors
}
on run() {
return map(
"is_97_prime", is_prime(97),
"primes_30", primes_up_to(30),
"factors_360", factorize(360)
)
}
}
cell test PrimeTests {
rules {
assert is_prime(2)
assert is_prime(97)
assert is_prime(91) == false // 7 * 13
assert len(primes_up_to(30)) == 10 // 2,3,5,7,11,13,17,19,23,29
// 360 = 2^3 * 3^2 * 5
assert len(factorize(360)) == 6
assert product(factorize(360)) == 360
assert product(factorize(97)) == 97
}
}What the toolchain says
$ soma check primes.cell
✓ All checks passed.$ soma test primes.cell
test PrimeTests ...
✓ assert is_prime(2)
✓ assert is_prime(97)
✓ assert is_prime(91) == false
✓ assert len(primes_up_to(30)) == 10
✓ assert len(factorize(360)) == 6
✓ assert product(factorize(360)) == 360
✓ assert product(factorize(97)) == 97
7 tests: 7 passed, 0 failed$ soma verify primes.cell
Verifying primes.cell...
Primes/termination:
⚠ handler `is_prime`: while-loop without provable termination bound (write `while [loop_bound(N)] cond { … }`, or a for-loop over a bounded range)
⚠ `primes_up_to` calls `Primes.is_prime`, which may not terminate
⚠ handler `factorize`: while-loop without provable termination bound (write `while [loop_bound(N)] cond { … }`, or a for-loop over a bounded range)
⚠ `run` calls `Primes.factorize`, which may not terminate
0 passed, 4 warnings, 0 failures
Temporal: 0 passed, 0 failed
VERIFY OK$ soma run primes.cell run
{"is_97_prime": true, "primes_30": [2, 3, 5, 7, 11, 13, 17, 19, 23, 29], "factors_360": [2, 2, 2, 3, 3, 5]}