spec/crypto/ed25519.bend checks

raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/spec/crypto/ed25519.bend as Ed25519

7 imports

import Base
import ../lib/common.bend as C
import ./curve25519/field.bend as FS
import ./curve25519/x25519.bend as SX
import ./sha512.bend as SHA
import ../../src/crypto/ed25519/ed25519.bend as E
import ../../src/crypto/ed25519/scalar.bend as ESC

Types

type EPt source · line 40 · raw

Data

EPt

@x:Nat -> @y:Nat -> @z:Nat -> @t:Nat -> EPt

Definitions

def ell_bytes source · line 31 · raw

List<&2, U32>

L = 2^252 + 27742317777372353535851937790883648493, little-endian bytes

def ell source · line 35 · raw

@+one:Nat -> Nat

def dconst source · line 44 · raw

@+one:Nat -> @+p:Nat -> Nat

d = -121665 / 121666

def sqm1 source · line 48 · raw

@+p:Nat -> Nat

2^((p - 1) / 4), a square root of -1

def identity source · line 51 · raw

EPt

def add source · line 56 · raw

@+p:Nat -> @+d:Nat -> @a:EPt -> @b:EPt -> EPt

5.1.4: A = (Y1-X1)(Y2-X2), B = (Y1+X1)(Y2+X2), C = T1 2d T2, D = Z1 2 Z2, E = B-A, F = D-C, G = D+C, H = B+A, X3 = EF, Y3 = GH, T3 = EH, Z3 = FG

def double source · line 71 · raw

@+p:Nat -> @a:EPt -> EPt

5.1.4: A = X1^2, B = Y1^2, C = 2 Z1^2, H = A+B, E = H-(X1+Y1)^2, G = A-B, F = C+G, X3 = EF, Y3 = GH, T3 = EH, Z3 = FG

def pick source · line 85 · raw

@b:Nat -> @q:EPt -> @r:EPt -> EPt

def smul source · line 93 · raw

@+p:Nat -> @+d:Nat -> @n:Nat -> @+k:Nat -> @+a:EPt -> @q:EPt -> EPt

bits t = n - 1 .. 0 of k: q = 2 q, plus a on a one bit

def mul source · line 103 · raw

@+one:Nat -> @+p:Nat -> @+d:Nat -> @+k:Nat -> @+a:EPt -> EPt

[k] a for a scalar below 2^256: 256 bits, written 2^8 one (one == 1), so the proof checker never unrolls the loop

def set_msb source · line 109 · raw

@xs:List<&2, U32> -> @+b:U32 -> List<&2, U32>

the most significant bit of the final octet set to b

def encode_n source · line 121 · raw

@n:Nat -> @+p:Nat -> @a:EPt -> List<&2, U32>

n = 32 bytes

def encode source · line 129 · raw

@+one:Nat -> @+p:Nat -> @a:EPt -> List<&2, U32>

32 bytes, written 2^5 one (one == 1): the byte count stays symbolic, so the checker never expands an encoding (and the SHA-512 over it) into bytes

def dec_fin source · line 134 · raw

@+p:Nat -> @+x:Nat -> @+y:Nat -> @+x0:Nat -> @fail:Bool -> Maybe<&2, EPt>

def dec_root source · line 142 · raw

@+p:Nat -> @+x:Nat -> @+y:Nat -> @+x0:Nat -> @is_u:Bool -> @is_nu:Bool -> Maybe<&2, EPt>

def dec_y source · line 157 · raw

@+p:Nat -> @+d:Nat -> @+y:Nat -> @+x0:Nat -> @bad:Bool -> Maybe<&2, EPt>

u = y^2 - 1, v = d y^2 + 1, x = u v^3 (u v^7)^((p-5)/8); x or x sqrt(-1) when v x^2 is u or -u; fail when x = 0 and x_0 = 1; x = p - x (here as -x mod p) when x mod 2 != x_0

def decode source · line 172 · raw

@+p:Nat -> @+d:Nat -> @+bs:List<&2, U32> -> Maybe<&2, EPt>

bit 255 is x_0; the rest is y, rejected when y >= p

def base_of source · line 178 · raw

@m:Maybe<&2, EPt> -> EPt

def base source · line 185 · raw

@+p:Nat -> @+d:Nat -> EPt

def equal source · line 189 · raw

@+p:Nat -> @a:EPt -> @b:EPt -> Bool

the same point: X1 Z2 == X2 Z1 and Y1 Z2 == Y2 Z1

def first source · line 196 · raw

@n:Nat -> @xs:List<&2, U32> -> List<&2, U32>

def rest source · line 207 · raw

@n:Nat -> @xs:List<&2, U32> -> List<&2, U32>

def cat source · line 218 · raw

@xs:List<&2, U32> -> @ys:List<&2, U32> -> List<&2, U32>

def hram source · line 227 · raw

@+one:Nat -> @rb:List<&2, U32> -> @+a:List<&2, U32> -> @+msg:List<&2, U32> -> Nat

k = SHA-512(R || A || M) mod L; a function of R first, so a comparison of two such terms compares R, A and M once instead of walking the digest

def secret source · line 236 · raw

@+h:List<&2, U32> -> Nat

def public_body source · line 239 · raw

@+one:Nat -> @+p:Nat -> @+d:Nat -> @+h:List<&2, U32> -> List<&2, U32>

def public_of source · line 244 · raw

@+one:Nat -> @+p:Nat -> @d:Nat -> @+h:List<&2, U32> -> List<&2, U32>

the same, a function of d first (d = dconst(one, p) is symbolic, so the checker keeps it a call instead of expanding it on every comparison)

def public_key_at source · line 253 · raw

@+one:Nat -> @p:Nat -> @+seed:List<&2, U32> -> List<&2, U32>

at p = prime(one); a function of p first, so the checker keeps it a call (p is symbolic) instead of expanding it whenever it compares two of them

def public_key source · line 260 · raw

@+one:Nat -> @+seed:List<&2, U32> -> List<&2, U32>

def sign_body source · line 265 · raw

@+one:Nat -> @+p:Nat -> @+d:Nat -> @+h:List<&2, U32> -> @+msg:List<&2, U32> -> List<&2, U32>

def sign_with source · line 273 · raw

@+one:Nat -> @+p:Nat -> @d:Nat -> @+h:List<&2, U32> -> @+msg:List<&2, U32> -> List<&2, U32>

def sign_at source · line 280 · raw

@+one:Nat -> @p:Nat -> @+seed:List<&2, U32> -> @+msg:List<&2, U32> -> List<&2, U32>

def sign source · line 287 · raw

@+one:Nat -> @+seed:List<&2, U32> -> @+msg:List<&2, U32> -> List<&2, U32>

def check source · line 292 · raw

@+one:Nat -> @+p:Nat -> @+d:Nat -> @+s:Nat -> @+rb:List<&2, U32> -> @+pk:List<&2, U32> -> @+msg:List<&2, U32> -> @ra:Maybe<&2, EPt> -> @aa:Maybe<&2, EPt> -> Bool

def verify_with source · line 300 · raw

@+one:Nat -> @+p:Nat -> @+d:Nat -> @+pk:List<&2, U32> -> @+msg:List<&2, U32> -> @+rb:List<&2, U32> -> @+s:Nat -> @s_ok:Bool -> Bool

def verify source · line 307 · raw

@+one:Nat -> @+pk:List<&2, U32> -> @+msg:List<&2, U32> -> @+sig:List<&2, U32> -> Bool

def Scalar.reduce source · line 314 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+bs:List<&2, U32> -> @+hb:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.bytes_ok(64n, bs) == True{} : Bool} -> Type

def Scalar.mul_add source · line 317 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+k:List<&2, U32> -> @+s:List<&2, U32> -> @+r:List<&2, U32> -> @+hk:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.tight(k) == True{} : Bool} -> @+hs:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.tight(s) == True{} : Bool} -> @+hr:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.tight(r) == True{} : Bool} -> @+hsl:{Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(s), ell(one)) == True{} : Bool} -> @+hrl:{Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(r), ell(one)) == True{} : Bool} -> Type

def Ed25519.public source · line 320 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+seed:List<&2, U32> -> @+hs:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.tight(seed) == True{} : Bool} -> Type

def Ed25519.sign source · line 323 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+seed:List<&2, U32> -> @+msg:List<&2, U32> -> @+hs:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.tight(seed) == True{} : Bool} -> Type

def Ed25519.verify source · line 326 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+pk:List<&2, U32> -> @+msg:List<&2, U32> -> @+sig:List<&2, U32> -> @+hp:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.tight(pk) == True{} : Bool} -> @+hg:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.bytes_ok(64n, sig) == True{} : Bool} -> Type