Skip to content

Instantly share code, notes, and snippets.

Santiago Zanella-Beguelin s-zanella

View GitHub Profile
s-zanella / M.fst
Last active Jul 17, 2018
Test vector extraction
View M.fst
module M
open FStar.HyperStack.ST
module HS = FStar.HyperStack
module LB = LowStar.Buffer
type vector =
| MkVec:
s-zanella /
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

s-zanella / PalindromicPrimes.fst
Last active Oct 27, 2017
Palindromic prime pyramids (aka truncatable palindromic primes)
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.
s-zanella / opportunistic_DH.spthy
Created Apr 29, 2017
Attempt at modeling opportunistic Diffie-Hellman in Tamarin
View opportunistic_DH.spthy
theory Sean
builtins: diffie-hellman
section{* DH *}
/* Opportunistic Diffie-Hellman */
// Using ephemeral keys as thread identifiers
You can’t perform that action at this time.