Skip to content

Instantly share code, notes, and snippets.

@tarcieri
tarcieri / semiprivate.md
Last active January 18, 2023 01:08
Ed25519-based semi-private keys

Semiprivate Keys

🚨 DANGER: INSECURE! 🚨

This may have seemed like a great idea in 2013, but the repeated "set/clear bits", a.k.a. clamping phases at each level of the hierarchy slowly subtract key strength.

Don't use this as described. Check out Ristretto.

Original text

Semi-private keys are an expansion of the traditional idea

@rntz
rntz / MinimalNBE.hs
Last active May 13, 2024 09:17
Normalisation by evaluation for the simply-typed lambda calculus, in Agda
-- A simply-typed lambda calculus, and a definition of normalisation by
-- evaluation for it.
--
-- The NBE implementation is based on a presentation by Sam Lindley from 2016:
-- http://homepages.inf.ed.ac.uk/slindley/nbe/nbe-cambridge2016.pdf
--
-- Adapted to handle terms with explicitly typed contexts (Sam's slides only
-- consider open terms with the environments left implicit/untyped). This was a
-- pain in the ass to figure out.
@AndrasKovacs
AndrasKovacs / Ordinals.agda
Last active July 27, 2024 06:34
Large countable ordinals and numbers in Agda
{-# OPTIONS --postfix-projections --without-K --safe #-}
{-
Large countable ordinals in Agda. For examples, see the bottom of this file.
Checked with Agda 2.6.0.1.
Countable ordinals are useful in "big number" contests, because they
can be directly converted into fast-growing ℕ → ℕ functions via the
fast-growing hierarchy:
@bobatkey
bobatkey / cont-cwf.agda
Last active June 16, 2023 21:23
Construction of the Containers / Polynomials CwF in Agda, showing that function extensionality is refuted
{-# OPTIONS --rewriting #-}
module cont-cwf where
open import Agda.Builtin.Sigma
open import Agda.Builtin.Unit
open import Agda.Builtin.Bool
open import Agda.Builtin.Nat
open import Data.Empty
import Relation.Binary.PropositionalEquality as Eq