Skip to content

Instantly share code, notes, and snippets.

View s-zanella's full-sized avatar

Santiago Zanella-Beguelin s-zanella

View GitHub Profile
s-zanella / Opacus bug report (>= 1.0)
Created October 4, 2022 11:01
Opacus bug report: Length of `BatchSplittingSampler` with Poisson sampling
"nbformat": 4,
"nbformat_minor": 0,
"metadata": {
"colab": {
"provenance": [],
"collapsed_sections": []
"kernelspec": {
"name": "python3",
s-zanella / M.fst
Last active July 17, 2018 10:00
Test vector extraction
module M
open FStar.HyperStack.ST
module HS = FStar.HyperStack
module LB = LowStar.Buffer
type vector =
| MkVec:
s-zanella /
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

s-zanella / PalindromicPrimes.fst
Last active October 27, 2017 22:28
Palindromic prime pyramids (aka truncatable palindromic primes)
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 April 29, 2017 23:10
Attempt at modeling opportunistic Diffie-Hellman in Tamarin
theory Sean
builtins: diffie-hellman
section{* DH *}
/* Opportunistic Diffie-Hellman */
// Using ephemeral keys as thread identifiers