spec/crypto/sign.bend checks

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

4 imports

import Base
import ./curve25519/field.bend as FS
import ./ed25519.bend as SE
import ../../src/crypto/sign.bend as SG

Definitions

def Sign.keypair source · line 16 · raw

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

def Sign.sign source · line 19 · 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} -> Type

def Sign.verify source · line 22 · 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

def Sign.reject_seed source · line 25 · raw

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

def Sign.reject_key source · line 28 · raw

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

def Sign.reject source · line 31 · 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} -> Type