spec/crypto/sign.bend source

spec/crypto/sign.bend on the hub · documented module

import Baseimport ./curve25519/field.bend as FSimport ./ed25519.bend as SEimport ../../src/crypto/sign.bend as SG# The contract of src/crypto/sign.bend (Ed25519 signatures, RFC 8032).# `one` is the symbolic 1 of spec/crypto/curve25519/field.bend.##   clause          statement#   Sign.keypair    generate_keypair(seed) is the seed with the public key#                   public_key(seed) of spec/crypto/ed25519.bend#   Sign.sign       sign(sk, msg) is the RFC 8032 signature sign(sk, msg)#   Sign.verify     verify(pk, msg, sig) is the RFC 8032 verdict#   Sign.reject     a malformed seed, key or signature gives None / Falsedef Sign.keypair(+one: Nat, +h1: {one == 1n : Nat}, +seed: List<&2, U32>, +hs: {FS.tight(seed) == True{} : Bool}) -> Type:  {SG.generate_keypair(seed) == Some{SG.Keypair{seed, SE.public_key(one, seed)}} : Maybe<&2, SG.Keypair>}def Sign.sign(+one: Nat, +h1: {one == 1n : Nat}, +sk: List<&2, U32>, +msg: List<&2, U32>, +hs: {FS.tight(sk) == True{} : Bool}) -> Type:  {SG.sign(sk, msg) == Some{SE.sign(one, sk, msg)} : Maybe<&2, List<&2, U32>>}def Sign.verify(+one: Nat, +h1: {one == 1n : Nat}, +pk: List<&2, U32>, +msg: List<&2, U32>, +sig: List<&2, U32>, +hp: {FS.tight(pk) == True{} : Bool}, +hg: {FS.bytes_ok(64n, sig) == True{} : Bool}) -> Type:  {SG.verify(pk, msg, sig) == SE.verify(one, pk, msg, sig) : Bool}def Sign.reject_seed(+seed: List<&2, U32>, +h: {FS.tight(seed) == False{} : Bool}) -> Type:  {SG.generate_keypair(seed) == None{} : Maybe<&2, SG.Keypair>}def Sign.reject_key(+sk: List<&2, U32>, +msg: List<&2, U32>, +h: {FS.tight(sk) == False{} : Bool}) -> Type:  {SG.sign(sk, msg) == None{} : Maybe<&2, List<&2, U32>>}def Sign.reject(+pk: List<&2, U32>, +msg: List<&2, U32>, +sig: List<&2, U32>, +h: {Bool.and(FS.tight(pk), FS.bytes_ok(64n, sig)) == False{} : Bool}) -> Type:  {SG.verify(pk, msg, sig) == False{} : Bool}