def secret_eq

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

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/curve25519/x25519.bend as SX
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/ed25519.bend as SE
import bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/field.bend as F
import bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/x25519.bend as X
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/xbits.bend as XB
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/bytes.bend as BY

76def secret_eq(+h: List<&2, U32>) -> {FS.value(X.clamp(F.take(32n, h))) == SE.secret(h) : Nat}:
77  +t = F.take(32n, h)
78  +st = SE.first(32n, h)
79  Equal.cong(List<&2, U32>, Nat, z => FS.value(z), X.clamp(t), SX.clamp(st), Equal.trans(List<&2, U32>, X.clamp(t), SX.clamp(t), SX.clamp(st), XB.clamp_eq(t), Equal.cong(List<&2, U32>, List<&2, U32>, z => SX.clamp(z), t, st, BY.take_eq(32n, h))))