Instantly share code, notes, and snippets.

# s-zanella/ProofWalkthrough.md Last active Jan 16, 2018

A walk through a proof in F* that 733929337 is the largest truncatable palindromic prime. # Walking through an F* proof

Let's see what it takes to trust an F* proof by walking through this proof that 733929337 is the largest truncatable palindromic prime.

Like in any other proof assistant, it requires trusting that the meta-theory of F* is sound. Unlike more mature systems like Coq that have small trusted kernels and independent proof checkers, in the case of F* this entails trusting a larger code base. Mistakes can be made (it has happened in LCF, Coq and F*), but if the author of a proof is well-intended, it's unlikely that they have exploited any unsound corner case to complete a proof. I'm well-intended :)

## Main statement

Starting from the main statement, we'll walk backwards identifying all definitions involved.

In this case, the statement reads:

`val largest_prime_pyramid: n:prime_pyramid -> Lemma (n <= 733929337)`

This says that 733929337 is the largest value of type `prime_pyramid`. Assuming the author hasn't tampered with the pre-defined meaning of `Lemma` and `<=` (easy to check, but for another time), this statement only depends on the definition of `prime_pyramid` below.

``````val is_prime_pyramid: nat -> bool
let rec is_prime_pyramid n =
if n <= 9 then is_prime n
else is_prime n && is_palindrome n && no_zero n && is_prime_pyramid (truncate n)

type prime_pyramid = n:nat{is_prime_pyramid n}
``````

The type `prime_pyramid` refines the pre-defined `nat` type (itself a refinement of the built-in `int` type). It is the type of natural numbers that satisfy the `is_prime_pyramid` predicate. `is_prime_pyramid` is recusively defined. For an integer `n`, it holds when either:

• `n` is a single prime digit, or
• `n` is a palindromic prime without zeros and `is_prime_pyramid (truncate n)` holds.

This matches closely the definition one would expect. Everything checks out so far, but we still need to validate the definitions of `is_prime`, `is_palindrome`, `no_zero` and `truncate`.

## Primality by trial division

Let's start with `is_prime`:

``````val is_prime: nat -> bool
let is_prime a = 1 < a && greatest_divisor a 2 1 = 1
``````

It depends on `greatest_divisor a b d`, a recursive function that finds the largest divisor greater than or equal to `b` of a positive integer `a` , returning `d` if there is none. It does so by dumbly trying every number between `b` and the square root of `a`. This is schoolbook trial division.

``````val divides: pos -> nat -> bool
let divides b a = a % b = 0

val greatest_divisor: a:pos -> b:pos -> d:pos{d < b} -> Tot pos (decreases (a - b))
let rec greatest_divisor a b d =
if a < b * b then d
else greatest_divisor a (b + 1) (if b `divides` a then b else d)
``````

When `sqrt(a) < b`, the function returns `d`. Otherwise, it continues from `b + 1`, updating the largest divisor `d` when `b` divides `a`. It is not hard to see that `greatest_divisor a 2 1` computes the greatest divisor of `a`, and hence `is_prime` is correct.

In F*, by default all defintions are proven terminating. The `decreases (a - b)` clause says that the quantity `a - b` decreases in every recursive call (and is non-negative), so `greatest_divisor` terminates.

## Palindromic numbers

Let's have a look at `is_palindrome` now:

``````val is_palindrome: nat -> bool
let is_palindrome n = (n = reverse n)

type palindrome = n:nat{is_palindrome n}
``````

A number is a palindrome if it equals its reverse. Fair enough.

The definition of `reverse` is short but slightly convoluted:

``````val reverse_acc: nat -> nat -> nat
let rec reverse_acc n m =
if n <= 9 then m + n else reverse_acc (n / 10) (10 * (m + n % 10))

val reverse: nat -> nat
let reverse n = reverse_acc n 0
``````

To reverse a decimal number `n`, we successively divide it by `10` to remove the last digit (`n % 10`), computing its reverse in an accumulator. So,

``````reverse (10^n * dn + ... + 10 * d1 + d0) = 10^n * d0 + ... + dn
``````

## No zero

No complications here. A number `n` has no zeros if it is a single non-zero digit, or it has more than one digit, its last digit is not `0` and `n / 10` has no zeros.

``````val no_zero: nat -> bool
let rec no_zero n =
if n <= 9 then 0 < n % 10
else 0 < n % 10 && no_zero (n / 10)
``````

## Truncating a number

Lastly, to truncate a palindromic number we

• remove its last digit by dividing it by 10;
• reverse the result;
• remove the last digit of this reverse (which is the first digit of the original number).

Note that if the number wasn't palindromic, we would need to reverse the result once more.

``````val truncate: palindrome -> nat
let truncate n = reverse (n / 10) / 10
``````

## Concluding remarks

That was it. To convince ourselves that the proof is correct we did not have to look at definitions used in proofs, or at intermediate lemmas. Surely, these are essential to complete the proof, but looking at them is unnecessary because F* checked the proof.

One last thing though; I'm well-intended, but I'm also lazy, so I left one lemma unproved. Such assumptions are easy to identify by the `assume` keyword:

``````val add: n:nat{n <= 9} -> nat -> nat
let add d n = 10 * reverse (10 * n + d) + d

assume val add_truncate: n:prime_pyramid{9 < n} ->
Lemma (n = add (n % 10) (truncate n))
``````

This is more or less obvious: adding the truncated digits back to a prime pyramid with more than one digit gives the original number. This crucially relies on the number having no zeros. For instance, 10001 is a palindrome, but truncating it yields 0, and adding the last digit back results in 11, not 10001. I have tested this property in F* for all integers up to 6 digits long, but I think that proving it is not easy without a roundtrip converting numbers to strings (list of digits) and back. I may get back to this when I have more time to spare.

F* checks the proof in about 2 minutes on a modest laptop. The expensive part is to construct the list of all prime pyramids of length 9, and check that none can be extended. As expected, the bottleneck is the primality test. It can be improved by not checking even divisors, or only prime divisors with a full sieve.

## Recap

Let's recap to see the parts of the proof we had to inspect, stripping everything else.

``````val divides: pos -> nat -> bool
let divides b a = a % b = 0

val greatest_divisor: a:pos -> b:pos -> d:pos{d < b} -> Tot pos (decreases (a - b))
let rec greatest_divisor a b d =
if a < b * b then d
else greatest_divisor a (b + 1) (if b `divides` a then b else d)

val is_prime: nat -> bool
let is_prime a = 1 < a && greatest_divisor a 2 1 = 1

val reverse_acc: nat -> nat -> nat
let rec reverse_acc n m =
if n <= 9 then m + n else reverse_acc (n / 10) (10 * (m + n % 10))

val reverse: nat -> nat
let reverse n = reverse_acc n 0

val is_palindrome: nat -> bool
let is_palindrome n = (n = reverse n)

type palindrome = n:nat{is_palindrome n}

val truncate: palindrome -> nat
let truncate n = reverse (n / 10) / 10

val no_zero: nat -> bool
let rec no_zero n =
if n <= 9 then 0 < n % 10
else 0 < n % 10 && no_zero (n / 10)

val is_prime_pyramid: nat -> bool
let rec is_prime_pyramid n =
if n <= 9 then is_prime n
else is_prime n && is_palindrome n && no_zero n && is_prime_pyramid (truncate n)

type prime_pyramid = n:nat{is_prime_pyramid n}

val add: n:nat{n <= 9} -> nat -> nat
let add d n = 10 * reverse (10 * n + d) + d

assume val add_truncate: n:prime_pyramid{9 < n} ->
Lemma (n = add (n % 10) (truncate n))

val largest_prime_pyramid: n:prime_pyramid -> Lemma (n <= 733929337)
``````

For the sake of readability, I haven't attempted to minimize this. Type definitions could be inlined, `val` declarations could be omitted, etc. Had there been good library support for reasoning about prime numbers in F* (there is such thing in Coq), I would also have saved a couple of definitions.

Assuming a trusted definition of `is_prime`, proving `add_truncate`, and inlining type definitions and `val` annotations, would result in a core proof of just 15 lines, 5 of which are empty. Now that's not bad at all: auditing these 10 lines of code is all it would take:

``````let rec reverse_acc (n:nat) (m:nat) : nat =
if n <= 9 then m + n else reverse_acc (n / 10) (10 * (m + n % 10))

let reverse (n:nat) = reverse_acc n 0

let truncate (n:nat{n = reverse n}) : nat = reverse (n / 10) / 10

let rec no_zero (n:nat) =
if n <= 9 then 0 < n % 10 else 0 < n % 10 && no_zero (n / 10)

let rec is_prime_pyramid (n:nat) =
if n <= 9 then is_prime n
else is_prime n && n = reverse n && no_zero n && is_prime_pyramid (truncate n)

val largest_prime_pyramid: (n:nat{is_prime_pyramid n}) -> Lemma (n <= 733929337)
``````