Instantly share code, notes, and snippets.

View M.fst
module M
open FStar.HyperStack.ST
module HS = FStar.HyperStack
module LB = LowStar.Buffer
noeq
type vector =
| MkVec:
View ProofWalkthrough.md

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

View PalindromicPrimes.fst
(**
A truncatable palindromic prime is either a prime digit, or a palindromic
prime number that contains no 0 and such that removing its leading and
trailing digits yields a truncatable palindromic prime.
Here we prove that there are no truncatable palindromic primes with more
than 9 digits, and that the largest is 733929337.
See http://www.utm.edu/staff/caldwell/preprints/JRM_prime_pyramids.pdf
View opportunistic_DH.spthy
theory Sean
begin
builtins: diffie-hellman
section{* DH *}
/* Opportunistic Diffie-Hellman */
// Using ephemeral keys as thread identifiers