def th_v

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/pschn.bend:65

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend as FS
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend as CV
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/schnorr.bend as SS
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/scalar.bend as S
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/bytes.bend as B
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/schnorr.bend as SC
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pscal.bend as SQ

65# int(hash) mod n
66def th_v(+one: Nat, +h1: {one == 1n : Nat}, +tag: List<&2, U32>, +x: List<&2, U32>) -> {FS.value(one, S.reduce(B.of_be(SC.tagged(tag, x)))) == Nat.mod(CV.os2ip(SS.tagged(tag, x)), FS.order(one)) : Nat}:
67  %Equal.sym(List<&2, U32>, SC.tagged(tag, x), SS.tagged(tag, x), tagged_v(tag, x)) : {FS.value(one, S.reduce(B.of_be(_))) == Nat.mod(CV.os2ip(SS.tagged(tag, x)), FS.order(one)) : Nat}
68  SQ.hash_v(one, h1, SS.tagged(tag, x), tagged_len(tag, x))