s-zanella

{
  "nbformat": 4,
  "nbformat_minor": 0,
  "metadata": {
    "colab": {
      "provenance": [],
      "collapsed_sections": []
    },
    "kernelspec": {
      "name": "python3",

s-zanella

module M

open FStar.HyperStack.ST

module HS = FStar.HyperStack
module LB = LowStar.Buffer

noeq
type vector = 
| MkVec:

s-zanella

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

(**
  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

s-zanella

theory Sean
begin

builtins: diffie-hellman

section{* DH *}

/* Opportunistic Diffie-Hellman */

// Using ephemeral keys as thread identifiers