Skip to content

Instantly share code, notes, and snippets.

# Santiago Zanella-Beguelin s-zanella

Created April 29, 2017 23:10
Attempt at modeling opportunistic Diffie-Hellman in Tamarin
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 theory Sean begin builtins: diffie-hellman section{* DH *} /* Opportunistic Diffie-Hellman */ // Using ephemeral keys as thread identifiers
Last active October 27, 2017 22:28
Palindromic prime pyramids (aka truncatable palindromic primes)
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 (** 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
Last active January 16, 2018 14:38
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

Last active July 17, 2018 10:00
Test vector extraction
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 module M open FStar.HyperStack.ST module HS = FStar.HyperStack module LB = LowStar.Buffer noeq type vector = | MkVec:
Created October 4, 2022 11:01
Opacus bug report: Length of `BatchSplittingSampler` with Poisson sampling
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 { "nbformat": 4, "nbformat_minor": 0, "metadata": { "colab": { "provenance": [], "collapsed_sections": [] }, "kernelspec": { "name": "python3",