~/bend-docscommunity

proofs/crypto/ed25519/proof.bend checks

raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/proof.bend as Proof

21 imports
import Base
import ../../../spec/crypto/curve25519/field.bend as FS
import ../../../spec/crypto/curve25519/x25519.bend as SX
import ../../../spec/crypto/ed25519.bend as SE
import ../../../spec/crypto/sha512.bend as SHA
import ../../../src/crypto/hash.bend as H
import ../../../src/crypto/curve25519/field.bend as F
import ../../../src/crypto/ed25519/point.bend as PT
import ../../../src/crypto/ed25519/scalar.bend as ESC
import ../../../src/crypto/ed25519/ed25519.bend as E
import ../../../src/crypto/curve25519/x25519.bend as X
import ../../../src/crypto/sign.bend as SG
import ../../../spec/crypto/sign.bend as SS
import ../../lib/u32.bend as U
import ../../lib/logic.bend as L
import ../curve25519/limbs.bend as LM
import ../curve25519/prime.bend as PRM
import ./scalar3.bend as S3
import ./bytes.bend as BY
import ./top.bend as TP
import ./pcodec.bend as PC

Definitions

def v source · line 28 · raw

@+x:U32 -> Nat

def pp1 source · line 31 · raw

@+one:Nat -> Nat

def ok source · line 34 · raw

@+n:Nat -> @+a:List<&2, U32> -> @+h:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.bytes_ok(n, a) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(n, a, 255n) == True{} : Bool}

def ell_m source · line 37 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {1n+0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/ed25519/scalar3.mmL(one) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.ell(one) : Nat}

def scalar_reduce source · line 42 · raw

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

def below source · line 46 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:Nat -> @+h:{Nat.is_lt(x, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.ell(one)) == True{} : Bool} -> {Nat.is_lt(x, 1n+0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/ed25519/scalar3.mmL(one)) == True{} : Bool}

def scalar_mul_add source · line 49 · 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), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.ell(one)) == True{} : Bool} -> @+hrl:{Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(r), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.ell(one)) == True{} : Bool} -> 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.Scalar.mul_add(one, h1, k, s, r, hk, hs, hr, hsl, hrl)

def ed_public source · line 57 · raw

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

def ed_sign source · line 68 · 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} -> 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.Ed25519.sign(one, h1, seed, msg, hs)

def ed_verify source · line 79 · 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} -> 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.Ed25519.verify(one, h1, pk, msg, sig, hp, hg)

def valid_eq source · line 110 · raw

@+n:Nat -> @+xs:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/x25519.valid_bytes(n, xs) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.bytes_ok(n, xs) : Bool}

def keypair_if_eq source · line 123 · raw

@+seed:List<&2, U32> -> @+ok:Bool -> @+pk:List<&2, U32> -> @+hok:{ok == True{} : Bool} -> @+e:{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/ed25519.public_key(seed) == pk : List<&2, U32>} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sign.keypair_if(seed, ok) == Some{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sign.Keypair{seed, pk}} : Maybe<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sign.Keypair>}

def sign_if_eq source · line 130 · raw

@+sk:List<&2, U32> -> @+msg:List<&2, U32> -> @+ok:Bool -> @+S:List<&2, U32> -> @+hok:{ok == True{} : Bool} -> @+e:{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/ed25519.sign_raw(sk, msg) == S : List<&2, U32>} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sign.sign_if(sk, msg, ok) == Some{S} : Maybe<&2, List<&2, U32>>}

def verify_if_eq source · line 137 · raw

@+pk:List<&2, U32> -> @+msg:List<&2, U32> -> @+sig:List<&2, U32> -> @+ok:Bool -> @+V:Bool -> @+hok:{ok == True{} : Bool} -> @+e:{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/ed25519.verify_raw(pk, msg, sig) == V : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sign.verify_if(pk, msg, sig, ok) == V : Bool}

def valid_ok source · line 144 · raw

@+n:Nat -> @+xs:List<&2, U32> -> @+h:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.bytes_ok(n, xs) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/x25519.valid_bytes(n, xs) == True{} : Bool}

def sign_keypair source · line 147 · raw

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

def sign_sign source · line 150 · raw

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

def sign_verify source · line 153 · 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} -> 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/sign.Sign.verify(one, h1, pk, msg, sig, hp, hg)

def sign_reject_seed source · line 156 · raw

@+seed:List<&2, U32> -> @+h:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.tight(seed) == False{} : Bool} -> 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/sign.Sign.reject_seed(seed, h)

def sign_reject_key source · line 161 · raw

@+sk:List<&2, U32> -> @+msg:List<&2, U32> -> @+h:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.tight(sk) == False{} : Bool} -> 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/sign.Sign.reject_key(sk, msg, h)

def sign_reject source · line 166 · raw

@+pk:List<&2, U32> -> @+msg:List<&2, U32> -> @+sig:List<&2, U32> -> @+h:{Bool.and(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.tight(pk), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.bytes_ok(64n, sig)) == False{} : Bool} -> 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/sign.Sign.reject(pk, msg, sig, h)