def hram_s

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/ed25519/top.bend:58

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/curve25519/field.bend as FS
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/ed25519.bend as SE
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/sha512.bend as SHA

58def hram_s(+one: Nat, +rb: List<&2, U32>, +a: List<&2, U32>, +msg: List<&2, U32>) -> {SE.hram(one, rb, a, msg) == Nat.mod(FS.value(SHA.sha512_bytes(SE.cat(rb, SE.cat(a, msg)))), SE.ell(one)) : Nat}:
59  match rb:
60    case Nil{}:
61      {==}
62    case Con{x, xt}:
63      {==}