def spec_tight

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/curve25519/proof.bend:169

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 S

169def spec_tight(+one: Nat, +k: List<&2, U32>, +u: List<&2, U32>) -> {FS.tight(S.x25519(one, k, u)) == True{} : Bool}:
170  +p = FS.prime(one)
171  +x1 = Nat.mod(S.decode_u(u), p)
172  finish_tight(p, S.ladder(one, p, S.bits(k), S.decode_scalar(k), x1, S.LSt{1n, 0n, x1, 1n, 0n}))