def hram_i

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

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/hash.bend as H
import bend-collections-laws-crypto@1.0.0.0/src/crypto/ed25519/scalar.bend as ESC
import bend-collections-laws-crypto@1.0.0.0/src/crypto/ed25519/ed25519.bend as E

65def hram_i(+rb: List<&2, U32>, +a: List<&2, U32>, +msg: List<&2, U32>) -> {E.hram(rb, a, msg) == ESC.reduce(H.sha512(E.cat(rb, E.cat(a, msg)))) : List<&2, U32>}:
66  match rb:
67    case Nil{}:
68      {==}
69    case Con{x, xt}:
70      {==}