| {-# 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 |
| {-# 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: |
| -- 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. |
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.
Semi-private keys are an expansion of the traditional idea