def finish_tight

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

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

164def finish_tight(+p: Nat, +st: S.LSt) -> {FS.tight(S.finish(p, st)) == True{} : Bool}:
165  match st:
166    case S.LSt{+x2, +z2, +x3, +z3, +sw}:
167      le_bytes_ok(32n, Nat.mod(FS.fmul(p, S.cs_fst(sw, x2, x3), FS.finv(p, S.cs_fst(sw, z2, z3))), p))