~/bend-docscommunity

spec/crypto/kex.bend checks

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

4 imports
import Base
import ./curve25519/field.bend as FS
import ./curve25519/x25519.bend as S
import ../../src/crypto/kex.bend as K

Definitions

def base source · line 15 · raw

List<&2, U32>

def unless_zero source · line 19 · raw

@ss:List<&2, U32> -> @z:Bool -> Maybe<&2, List<&2, U32>>

def Kex.public source · line 26 · raw

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

def Kex.shared source · line 29 · raw

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

def Kex.reject source · line 32 · raw

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