def base_rel

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/ed25519/pdec.bend:188

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/ed25519/point.bend as PT
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend as WD
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/rel.bend as RL
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/prel.bend as PR
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/pcodec.bend as PC

188def base_rel(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +cs: PT.Cs, +D: Nat, +rd: RL.R(pp, PT.cs_d(cs), D), +rs: RL.R(pp, PT.cs_s(cs), SE.sqm1(1n+pp)), +xs: List<&2, U32>) -> PR.Rp(pp, PT.base(cs, xs), SE.base(1n+pp, D)):
189  +P = {1n+pp : Nat}
190  +m = F.mul(PT.lit(xs, F.small(4)), F.inv(PT.lit(xs, F.small(5))))
191  +FM = FS.fmul(P, 4n, FS.finv(P, 5n))
192  +r5 = PC.r_lit_small(pp, xs, 5, {==})
193  +rm = PR.rmul(one, h1, pp, hP, PT.lit(xs, F.small(4)), F.inv(PT.lit(xs, F.small(5))), 4n, FS.finv(P, 5n), PC.r_lit_small(pp, xs, 4, {==}), RL.r_inv(one, h1, pp, hP, PT.lit(xs, F.small(5)), 5n, RL.r_o(pp, PT.lit(xs, F.small(5)), 5n, r5), RL.r_c(pp, PT.lit(xs, F.small(5)), 5n, r5)))
194  +eb = PC.bytes_rel(one, h1, pp, hP, m, FM, rm, PC.red(pp, Nat.mul(4n, FS.finv(P, 5n))))
195  %Equal.sym(List<&2, U32>, F.to_bytes(m), SX.le_bytes(32n, FM), eb) : PR.Rp(pp, PT.base_of(PT.decode(cs, _)), SE.base(P, D))
196  base_of_rel(pp, PT.decode(cs, SX.le_bytes(32n, FM)), SE.decode(P, D, SX.le_bytes(32n, FM)), decode_rel(one, h1, pp, hP, cs, D, rd, rs, SX.le_bytes(32n, FM), le_bytes_ok(32n, FM)))