proofs/crypto/ed25519/pcodec.bend

bend-collections-laws-crypto@1.0.0.0 · 239 lines · 33 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
3import bend-collections-laws-crypto@1.0.0.0/spec/crypto/curve25519/field.bend as FS
4import bend-collections-laws-crypto@1.0.0.0/spec/crypto/curve25519/x25519.bend as SX
5import bend-collections-laws-crypto@1.0.0.0/spec/crypto/ed25519.bend as SE
6import bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/field.bend as F
7import bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/x25519.bend as X
8import bend-collections-laws-crypto@1.0.0.0/src/crypto/ed25519/point.bend as PT
9import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
10import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
11import bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend as WD
12import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32.bend as U
13import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
14import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as NR
15import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend as LM
16import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/consts.bend as K
17import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/fieldops.bend as FO
18import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/mulw.bend as MW
19import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/pow.bend as PW
20import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/canon.bend as CN
21import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/eqf.bend as EQ
22import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/freeze.bend as FZ
23import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/cong.bend as G
24import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/rel.bend as RL
25import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/xbits.bend as XB
26import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/ladder.bend as LD
27import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/scalar.bend as SC
28import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/prel.bend as PR
29import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend as M2
30
31# Constants, encoding (5.1.2), decoding (5.1.3), equality and the base
32# point of src/crypto/ed25519/point.bend against spec/crypto/ed25519.bend.
33
34def v(+x: U32) -> Nat:
35  U32.to_nat(x)
36
37# decoding results: both None, or both Some of related points
38def MR(+pp: Nat, +m: Maybe<&2, PT.Pt>, +sm: Maybe<&2, SE.EPt>) -> Data:
39  match m sm:
40    case None{} None{}:
41      {True{} == True{} : Bool}
42    case Some{p} Some{sp}:
43      PR.Rp(pp, p, sp)
44    case None{} Some{sp}:
45      {True{} == False{} : Bool}
46    case Some{p} None{}:
47      {True{} == False{} : Bool}
48
49# ---- small constants ----
50
51def r_zero(+pp: Nat) -> RL.R(pp, F.zero(), 0n):
52  ({==}, G.c_refl(pp, 0n))
53
54def r_one(+pp: Nat) -> RL.R(pp, F.one(), 1n):
55  ({==}, G.c_refl(pp, 1n))
56
57def r_small(+pp: Nat, +k: U32, +hk: {Nat.is_le(v(k), 255n) == True{} : Bool}) -> RL.R(pp, F.small(k), v(k)):
58  (L.and_intro(Nat.is_le(v(k), 255n), LM.okb(31n, K.rep(31n, 0, Nil{}), 255n), hk, {==}), G.c_eq(pp, FS.value(F.small(k)), v(k), Equal.trans(Nat, FS.value(F.small(k)), Nat.add(v(k), 0n), v(k), {==}, N.add_zero(v(k)))))
59
60def c65_shape() -> {PT.c121665() == Con{65, Con{219, Con{1, K.rep(29n, 0, Nil{})}}} : List<&2, U32>}:
61  {==}
62
63def c66_shape() -> {PT.c121666() == Con{66, Con{219, Con{1, K.rep(29n, 0, Nil{})}}} : List<&2, U32>}:
64  {==}
65
66def c65_valo(+one: Nat) -> {K.valo(one, PT.c121665()) == FS.digits(one, [65n, 219n, 1n]) : Nat}:
67  %Equal.sym(List<&2, U32>, PT.c121665(), Con{65, Con{219, Con{1, K.rep(29n, 0, Nil{})}}}, c65_shape()) : {K.valo(one, _) == FS.digits(one, [65n, 219n, 1n]) : Nat}
68  %Equal.sym(Nat, K.valo(one, K.rep(29n, 0, Nil{})), 0n, K.run0(one, 29n, Nil{})) : {Nat.add(Nat.mul(one, v(65)), C.shift(8n, Nat.add(Nat.mul(one, v(219)), C.shift(8n, Nat.add(Nat.mul(one, v(1)), C.shift(8n, _)))))) == FS.digits(one, [65n, 219n, 1n]) : Nat}
69  {==}
70
71def c66_valo(+one: Nat) -> {K.valo(one, PT.c121666()) == FS.digits(one, [66n, 219n, 1n]) : Nat}:
72  %Equal.sym(List<&2, U32>, PT.c121666(), Con{66, Con{219, Con{1, K.rep(29n, 0, Nil{})}}}, c66_shape()) : {K.valo(one, _) == FS.digits(one, [66n, 219n, 1n]) : Nat}
73  %Equal.sym(Nat, K.valo(one, K.rep(29n, 0, Nil{})), 0n, K.run0(one, 29n, Nil{})) : {Nat.add(Nat.mul(one, v(66)), C.shift(8n, Nat.add(Nat.mul(one, v(219)), C.shift(8n, Nat.add(Nat.mul(one, v(1)), C.shift(8n, _)))))) == FS.digits(one, [66n, 219n, 1n]) : Nat}
74  {==}
75
76# a constant given through its valo, the list kept a variable
77def r_valo(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +ks: List<&2, U32>, +D: Nat, +hv: {K.valo(one, ks) == D : Nat}, +ho: {LM.okb(32n, ks, 255n) == True{} : Bool}) -> RL.R(pp, ks, D):
78  (ho, G.c_eq(pp, FS.value(ks), D, Equal.trans(Nat, FS.value(ks), K.valo(one, ks), D, Equal.sym(Nat, K.valo(one, ks), FS.value(ks), K.valo_value(one, h1, ks)), hv)))
79
80def lit_valo(+one: Nat, +xs: List<&2, U32>, +k: List<&2, U32>, +D: Nat, +hv: {K.valo(one, k) == D : Nat}) -> {K.valo(one, PT.lit(xs, k)) == D : Nat}:
81  match xs:
82    case Nil{}:
83      hv
84    case Con{h, t}:
85      hv
86
87def lit_okb(+xs: List<&2, U32>, +k: List<&2, U32>, +ho: {LM.okb(32n, k, 255n) == True{} : Bool}) -> {LM.okb(32n, PT.lit(xs, k), 255n) == True{} : Bool}:
88  match xs:
89    case Nil{}:
90      ho
91    case Con{h, t}:
92      ho
93
94def r_lit_small(+pp: Nat, +xs: List<&2, U32>, +k: U32, +hk: {Nat.is_le(v(k), 255n) == True{} : Bool}) -> RL.R(pp, PT.lit(xs, F.small(k)), v(k)):
95  match xs:
96    case Nil{}:
97      r_small(pp, k, hk)
98    case Con{h, t}:
99      r_small(pp, k, hk)
100
101def r_c65(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +xs: List<&2, U32>) -> RL.R(pp, PT.lit(xs, PT.c121665()), FS.digits(one, [65n, 219n, 1n])):
102  r_valo(one, h1, pp, PT.lit(xs, PT.c121665()), FS.digits(one, [65n, 219n, 1n]), lit_valo(one, xs, PT.c121665(), FS.digits(one, [65n, 219n, 1n]), c65_valo(one)), lit_okb(xs, PT.c121665(), {==}))
103
104def r_c66(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +xs: List<&2, U32>) -> RL.R(pp, PT.lit(xs, PT.c121666()), FS.digits(one, [66n, 219n, 1n])):
105  r_valo(one, h1, pp, PT.lit(xs, PT.c121666()), FS.digits(one, [66n, 219n, 1n]), lit_valo(one, xs, PT.c121666(), FS.digits(one, [66n, 219n, 1n]), c66_valo(one)), lit_okb(xs, PT.c121666(), {==}))
106
107# ---- d, 2 d, sqrt(-1) ----
108
109def dval(+xs: List<&2, U32>) -> List<&2, U32>:
110  F.mul(F.neg(PT.lit(xs, PT.c121665())), F.inv(PT.lit(xs, PT.c121666())))
111
112def r_d(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +xs: List<&2, U32>) -> RL.R(pp, PT.cs_d(PT.consts(xs)), SE.dconst(one, 1n+pp)):
113  +P = {1n+pp : Nat}
114  +D65 = FS.digits(one, [65n, 219n, 1n])
115  +D66 = FS.digits(one, [66n, 219n, 1n])
116  +r66 = r_c66(one, h1, pp, xs)
117  PR.rmul(one, h1, pp, hP, F.neg(PT.lit(xs, PT.c121665())), F.inv(PT.lit(xs, PT.c121666())), FS.fsub(P, 0n, D65), FS.finv(P, D66), PR.rsub(one, h1, pp, hP, F.zero(), PT.lit(xs, PT.c121665()), 0n, D65, r_zero(pp), r_c65(one, h1, pp, xs)), RL.r_inv(one, h1, pp, hP, PT.lit(xs, PT.c121666()), D66, RL.r_o(pp, PT.lit(xs, PT.c121666()), D66, r66), RL.r_c(pp, PT.lit(xs, PT.c121666()), D66, r66)))
118
119def r_d2(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +xs: List<&2, U32>) -> RL.R(pp, PT.cs_d2(PT.consts(xs)), FS.fadd(1n+pp, SE.dconst(one, 1n+pp), SE.dconst(one, 1n+pp))):
120  PR.radd(one, h1, pp, hP, dval(xs), dval(xs), SE.dconst(one, 1n+pp), SE.dconst(one, 1n+pp), r_d(one, h1, pp, hP, xs), r_d(one, h1, pp, hP, xs))
121
122def p14_bits() -> List<&2, Bool>:
123  [False{}, True{}, True{}]
124
125def eb_p14(+one: Nat, +h1: {one == 1n : Nat}) -> {PW.eb(one, p14_bits()) == 3n : Nat}:
126  L.subst(Nat, o => {PW.eb(o, p14_bits()) == 3n : Nat}, 1n, one, Equal.sym(Nat, one, 1n, h1), {==})
127
128# 8 Fo(250) + 3 == (p - 1) / 4
129def p14_exp(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}) -> {Nat.add(Nat.mul(PW.Fo(one, 250n), WD.sc(PW.blen(p14_bits()), one)), PW.eb(one, p14_bits())) == Nat.div(Nat.sub(1n+pp, 1n), 4n) : Nat}:
130  +F2 = PW.Fo(one, 250n)
131  +P = {1n+pp : Nat}
132  %Equal.sym(Nat, WD.sc(3n, one), 8n, PW.small_one(one, h1, 3n, 8n, {==})) : {Nat.add(Nat.mul(F2, _), PW.eb(one, p14_bits())) == Nat.div(Nat.sub(P, 1n), 4n) : Nat}
133  %Equal.sym(Nat, PW.eb(one, p14_bits()), 3n, eb_p14(one, h1)) : {Nat.add(Nat.mul(F2, 8n), _) == Nat.div(Nat.sub(P, 1n), 4n) : Nat}
134  +e = Nat.add(Nat.mul(F2, 8n), 3n)
135  +m4 = Equal.trans(Nat, Nat.mul(e, 4n), Nat.add(Nat.mul(Nat.mul(F2, 8n), 4n), Nat.mul(3n, 4n)), Nat.add(Nat.mul(F2, 32n), 12n), NA.mul_add_right(Nat.mul(F2, 8n), 3n, 4n), M2.cong_l(Nat.mul(Nat.mul(F2, 8n), 4n), Nat.mul(F2, 32n), Nat.mul(3n, 4n), NA.mul_assoc(F2, 8n, 4n)))
136  +e1 = Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(e, 4n), 1n), 19n), Nat.add(Nat.add(Nat.add(Nat.mul(F2, 32n), 12n), 1n), 19n), Nat.add(P, 19n), M2.cong_l(Nat.add(Nat.mul(e, 4n), 1n), Nat.add(Nat.add(Nat.mul(F2, 32n), 12n), 1n), 19n, M2.cong_l(Nat.mul(e, 4n), Nat.add(Nat.mul(F2, 32n), 12n), 1n, m4)),
137    Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.mul(F2, 32n), 12n), 1n), 19n), Nat.add(Nat.mul(F2, 32n), 32n), Nat.add(P, 19n), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.mul(F2, 32n), 12n), 1n), 19n), Nat.add(Nat.add(Nat.mul(F2, 32n), 12n), Nat.add(1n, 19n)), Nat.add(Nat.mul(F2, 32n), 32n), NA.add_assoc(Nat.add(Nat.mul(F2, 32n), 12n), 1n, 19n), NA.add_assoc(Nat.mul(F2, 32n), 12n, 20n)), PW.f32(one, h1, pp, hP)))
138  +e2 = G.cancel_r(Nat.add(Nat.mul(e, 4n), 1n), P, 19n, e1)
139  +e3 = Equal.trans(Nat, P, Nat.add(Nat.mul(e, 4n), 1n), Nat.add(1n, Nat.mul(e, 4n)), Equal.sym(Nat, Nat.add(Nat.mul(e, 4n), 1n), P, e2), NA.add_comm(Nat.mul(e, 4n), 1n))
140  %Equal.sym(Nat, P, Nat.add(1n, Nat.mul(e, 4n)), e3) : {e == Nat.div(Nat.sub(_, 1n), 4n) : Nat}
141  %Equal.sym(Nat, Nat.sub(Nat.add(1n, Nat.mul(e, 4n)), 1n), Nat.mul(e, 4n), N.add_sub_cancel(1n, Nat.mul(e, 4n))) : {e == Nat.div(_, 4n) : Nat}
142  %N.add_zero(Nat.mul(e, 4n)) : {e == Nat.div(_, 4n) : Nat}
143  Equal.sym(Nat, Nat.div(Nat.add(Nat.mul(e, 4n), 0n), 4n), e, NR.div_of(e, 3n, 0n, {==}))
144
145def r_sqm1(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +xs: List<&2, U32>) -> RL.R(pp, PT.cs_s(PT.consts(xs)), SE.sqm1(1n+pp)):
146  +P = {1n+pp : Nat}
147  +two = PT.lit(xs, F.small(2))
148  +ex = Nat.add(Nat.mul(PW.Fo(one, 250n), WD.sc(PW.blen(p14_bits()), one)), PW.eb(one, p14_bits()))
149  +k = Nat.div(Nat.sub(P, 1n), 4n)
150  +o2 = RL.r_o(pp, two, 2n, r_lit_small(pp, xs, 2, {==}))
151  +r2 = r_lit_small(pp, xs, 2, {==})
152  +c1 = PW.chain_val(one, h1, pp, hP, 249n, p14_bits(), two, o2)
153  +c1b = G.c_trans(pp, FS.value(PT.pow_p14(two)), Nat.pow(FS.value(two), ex), Nat.pow(2n, ex), c1, G.c_pow(pp, FS.value(two), 2n, ex, RL.r_c(pp, two, 2n, r2)))
154  +c2 = G.c_eq(pp, Nat.pow(2n, ex), Nat.pow(2n, k), Equal.cong(Nat, Nat, t => Nat.pow(2n, t), ex, k, p14_exp(one, h1, pp, hP)))
155  +c3 = G.c_sym(pp, FS.fpow(P, 2n, k), Nat.pow(2n, k), G.c_mod(pp, Nat.pow(2n, k)))
156  (PW.pbs_okb(one, h1, p14_bits(), two, F.pow_ones(two, 249n, two), o2, PW.po_okb(one, h1, 249n, two, two, o2, o2)), G.c_trans(pp, FS.value(PT.pow_p14(two)), Nat.pow(2n, ex), FS.fpow(P, 2n, k), c1b, G.c_trans(pp, Nat.pow(2n, ex), Nat.pow(2n, k), FS.fpow(P, 2n, k), c2, c3)))
157
158# ---- equality of reduced values ----
159
160def red(+pp: Nat, +a: Nat) -> {Nat.mod(Nat.mod(a, 1n+pp), 1n+pp) == Nat.mod(a, 1n+pp) : Nat}:
161  NR.mod_mod(pp, a)
162
163def eq_rel(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +x: List<&2, U32>, +y: List<&2, U32>, +a: Nat, +b: Nat, +rx: RL.R(pp, x, a), +ry: RL.R(pp, y, b), +ha: {Nat.mod(a, 1n+pp) == a : Nat}, +hb: {Nat.mod(b, 1n+pp) == b : Nat}) -> {F.eq(x, y) == Nat.is_eq(a, b) : Bool}:
164  +e1 = EQ.eq_val(one, h1, pp, hP, x, y, RL.r_o(pp, x, a, rx), RL.r_o(pp, y, b, ry))
165  +ea = Equal.trans(Nat, Nat.mod(FS.value(x), 1n+pp), Nat.mod(a, 1n+pp), a, RL.r_c(pp, x, a, rx), ha)
166  +eb = Equal.trans(Nat, Nat.mod(FS.value(y), 1n+pp), Nat.mod(b, 1n+pp), b, RL.r_c(pp, y, b, ry), hb)
167  Equal.trans(Bool, F.eq(x, y), Nat.is_eq(Nat.mod(FS.value(x), 1n+pp), Nat.mod(FS.value(y), 1n+pp)), Nat.is_eq(a, b), e1, Equal.trans(Bool, Nat.is_eq(Nat.mod(FS.value(x), 1n+pp), Nat.mod(FS.value(y), 1n+pp)), Nat.is_eq(a, Nat.mod(FS.value(y), 1n+pp)), Nat.is_eq(a, b), Equal.cong(Nat, Bool, z => Nat.is_eq(z, Nat.mod(FS.value(y), 1n+pp)), Nat.mod(FS.value(x), 1n+pp), a, ea), Equal.cong(Nat, Bool, z => Nat.is_eq(a, z), Nat.mod(FS.value(y), 1n+pp), b, eb)))
168
169def iz_rel(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +x: List<&2, U32>, +a: Nat, +rx: RL.R(pp, x, a), +ha: {Nat.mod(a, 1n+pp) == a : Nat}) -> {F.is_zero(x) == Nat.is_eq(a, 0n) : Bool}:
170  +e1 = CN.is_zero_val(one, h1, pp, hP, x, RL.r_o(pp, x, a, rx))
171  Equal.trans(Bool, F.is_zero(x), Nat.is_eq(Nat.mod(FS.value(x), 1n+pp), 0n), Nat.is_eq(a, 0n), e1, Equal.cong(Nat, Bool, z => Nat.is_eq(z, 0n), Nat.mod(FS.value(x), 1n+pp), a, Equal.trans(Nat, Nat.mod(FS.value(x), 1n+pp), Nat.mod(a, 1n+pp), a, RL.r_c(pp, x, a, rx), ha)))
172
173def par_rel(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +x: List<&2, U32>, +a: Nat, +rx: RL.R(pp, x, a), +ha: {Nat.mod(a, 1n+pp) == a : Nat}) -> {v(F.parity(x)) == Nat.mod(a, 2n) : Nat}:
174  Equal.trans(Nat, v(F.parity(x)), Nat.mod(Nat.mod(FS.value(x), 1n+pp), 2n), Nat.mod(a, 2n), CN.parity_val(one, h1, pp, hP, x, RL.r_o(pp, x, a, rx)), Equal.cong(Nat, Nat, z => Nat.mod(z, 2n), Nat.mod(FS.value(x), 1n+pp), a, Equal.trans(Nat, Nat.mod(FS.value(x), 1n+pp), Nat.mod(a, 1n+pp), a, RL.r_c(pp, x, a, rx), ha)))
175
176def u32_eq_nat(+a: U32, +b: U32) -> {U32.is_eq(a, b) == Nat.is_eq(v(a), v(b)) : Bool}:
177  Equal.cong(Cmp, Bool, c => Cmp.is_eq(c), U32.cmp(a, b), Nat.cmp(v(a), v(b)), U.u32_cmp(a, b))
178
179def mod2_le(+a: Nat) -> {Nat.is_le(Nat.mod(a, 2n), 1n) == True{} : Bool}:
180  N.lt_succ_le(Nat.mod(a, 2n), 1n, NR.dm_lt(1n, a))
181
182# ---- the point equality ----
183
184def equal_rel(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +p: PT.Pt, +q: PT.Pt, +sp: SE.EPt, +sq: SE.EPt, +hp: PR.Rp(pp, p, sp), +hq: PR.Rp(pp, q, sq)) -> {PT.equal(p, q) == SE.equal(1n+pp, sp, sq) : Bool}:
185  match p q sp sq:
186    case PT.Pt{+x1, +y1, +z1, +t1} PT.Pt{+x2, +y2, +z2, +t2} SE.EPt{+a1, +b1, +c1, +d1} SE.EPt{+a2, +b2, +c2, +d2}:
187      +P = {1n+pp : Nat}
188      +rx1 = PR.rX(pp, x1, y1, z1, t1, a1, b1, c1, d1, hp)
189      +ry1 = PR.rY(pp, x1, y1, z1, t1, a1, b1, c1, d1, hp)
190      +rz1 = PR.rZ(pp, x1, y1, z1, t1, a1, b1, c1, d1, hp)
191      +rx2 = PR.rX(pp, x2, y2, z2, t2, a2, b2, c2, d2, hq)
192      +ry2 = PR.rY(pp, x2, y2, z2, t2, a2, b2, c2, d2, hq)
193      +rz2 = PR.rZ(pp, x2, y2, z2, t2, a2, b2, c2, d2, hq)
194      +e1 = eq_rel(one, h1, pp, hP, F.mul(x1, z2), F.mul(x2, z1), FS.fmul(P, a1, c2), FS.fmul(P, a2, c1), PR.rmul(one, h1, pp, hP, x1, z2, a1, c2, rx1, rz2), PR.rmul(one, h1, pp, hP, x2, z1, a2, c1, rx2, rz1), red(pp, Nat.mul(a1, c2)), red(pp, Nat.mul(a2, c1)))
195      +e2 = eq_rel(one, h1, pp, hP, F.mul(y1, z2), F.mul(y2, z1), FS.fmul(P, b1, c2), FS.fmul(P, b2, c1), PR.rmul(one, h1, pp, hP, y1, z2, b1, c2, ry1, rz2), PR.rmul(one, h1, pp, hP, y2, z1, b2, c1, ry2, rz1), red(pp, Nat.mul(b1, c2)), red(pp, Nat.mul(b2, c1)))
196      Equal.trans(Bool, Bool.and(F.eq(F.mul(x1, z2), F.mul(x2, z1)), F.eq(F.mul(y1, z2), F.mul(y2, z1))), Bool.and(Nat.is_eq(FS.fmul(P, a1, c2), FS.fmul(P, a2, c1)), F.eq(F.mul(y1, z2), F.mul(y2, z1))), Bool.and(Nat.is_eq(FS.fmul(P, a1, c2), FS.fmul(P, a2, c1)), Nat.is_eq(FS.fmul(P, b1, c2), FS.fmul(P, b2, c1))), Equal.cong(Bool, Bool, z => Bool.and(z, F.eq(F.mul(y1, z2), F.mul(y2, z1))), F.eq(F.mul(x1, z2), F.mul(x2, z1)), Nat.is_eq(FS.fmul(P, a1, c2), FS.fmul(P, a2, c1)), e1), Equal.cong(Bool, Bool, z => Bool.and(Nat.is_eq(FS.fmul(P, a1, c2), FS.fmul(P, a2, c1)), z), F.eq(F.mul(y1, z2), F.mul(y2, z1)), Nat.is_eq(FS.fmul(P, b1, c2), FS.fmul(P, b2, c1)), e2))
197
198# ---- encoding ----
199
200def set_eq(+xs: List<&2, U32>, +b: U32) -> {PT.set_top(xs, b) == SE.set_msb(xs, b) : List<&2, U32>}:
201  match xs:
202    case Nil{}:
203      {==}
204    case Con{+x, +xt}:
205      match xt:
206        case Nil{}:
207          {==}
208        case Con{+y, +yt}:
209          Equal.cong(List<&2, U32>, List<&2, U32>, z => Con{x, z}, PT.set_top(Con{y, yt}, b), SE.set_msb(Con{y, yt}, b), set_eq(Con{y, yt}, b))
210
211# the canonical bytes of an element related to a reduced a
212def bytes_rel(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +x: List<&2, U32>, +a: Nat, +rx: RL.R(pp, x, a), +ha: {Nat.mod(a, 1n+pp) == a : Nat}) -> {F.to_bytes(x) == SX.le_bytes(32n, a) : List<&2, U32>}:
213  +y = F.freeze(x)
214  +oy = CN.freeze_okb(one, h1, pp, hP, x, RL.r_o(pp, x, a, rx))
215  +ey = Equal.trans(Nat, FS.value(y), Nat.mod(FS.value(x), 1n+pp), a, CN.freeze_val(one, h1, pp, hP, x, RL.r_o(pp, x, a, rx)), Equal.trans(Nat, Nat.mod(FS.value(x), 1n+pp), Nat.mod(a, 1n+pp), a, RL.r_c(pp, x, a, rx), ha))
216  Equal.trans(List<&2, U32>, y, SX.le_bytes(32n, FS.value(y)), SX.le_bytes(32n, a), Equal.sym(List<&2, U32>, SX.le_bytes(32n, FS.value(y)), y, XB.bytes_le(32n, y, oy)), Equal.cong(Nat, List<&2, U32>, z => SX.le_bytes(32n, z), FS.value(y), a, ey))
217
218def par_u32(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +x: List<&2, U32>, +a: Nat, +rx: RL.R(pp, x, a), +ha: {Nat.mod(a, 1n+pp) == a : Nat}) -> {F.parity(x) == U32.from_nat(Nat.mod(a, 2n)) : U32}:
219  +e = par_rel(one, h1, pp, hP, x, a, rx, ha)
220  +lt = NR.dm_lt(1n, a)
221  U.injective(F.parity(x), U32.from_nat(Nat.mod(a, 2n)), Equal.trans(Nat, v(F.parity(x)), Nat.mod(a, 2n), v(U32.from_nat(Nat.mod(a, 2n))), e, Equal.sym(Nat, v(U32.from_nat(Nat.mod(a, 2n))), Nat.mod(a, 2n), U.to_nat_from_nat(Nat.mod(a, 2n), 1n, {==}, lt))))
222
223def encode_rel(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +p: PT.Pt, +sp: SE.EPt, +hp: PR.Rp(pp, p, sp)) -> {PT.encode(p) == SE.encode_n(32n, 1n+pp, sp) : List<&2, U32>}:
224  match p sp:
225    case PT.Pt{+x, +y, +z, +t} SE.EPt{+a, +b, +c, +d}:
226      +P = {1n+pp : Nat}
227      +rx = PR.rX(pp, x, y, z, t, a, b, c, d, hp)
228      +ry = PR.rY(pp, x, y, z, t, a, b, c, d, hp)
229      +rz = PR.rZ(pp, x, y, z, t, a, b, c, d, hp)
230      +zi = F.inv(z)
231      +ZI = FS.finv(P, c)
232      +rzi = RL.r_inv(one, h1, pp, hP, z, c, RL.r_o(pp, z, c, rz), RL.r_c(pp, z, c, rz))
233      +my = PR.rmul(one, h1, pp, hP, y, zi, b, ZI, ry, rzi)
234      +mx = PR.rmul(one, h1, pp, hP, x, zi, a, ZI, rx, rzi)
235      +eb = bytes_rel(one, h1, pp, hP, F.mul(y, zi), FS.fmul(P, b, ZI), my, red(pp, Nat.mul(b, ZI)))
236      +ep = par_u32(one, h1, pp, hP, F.mul(x, zi), FS.fmul(P, a, ZI), mx, red(pp, Nat.mul(a, ZI)))
237      +e1 = Equal.cong(List<&2, U32>, List<&2, U32>, w => PT.set_top(w, F.parity(F.mul(x, zi))), F.to_bytes(F.mul(y, zi)), SX.le_bytes(32n, FS.fmul(P, b, ZI)), eb)
238      +e2 = Equal.cong(U32, List<&2, U32>, w => PT.set_top(SX.le_bytes(32n, FS.fmul(P, b, ZI)), w), F.parity(F.mul(x, zi)), U32.from_nat(Nat.mod(FS.fmul(P, a, ZI), 2n)), ep)
239      Equal.trans(List<&2, U32>, PT.set_top(F.to_bytes(F.mul(y, zi)), F.parity(F.mul(x, zi))), PT.set_top(SX.le_bytes(32n, FS.fmul(P, b, ZI)), U32.from_nat(Nat.mod(FS.fmul(P, a, ZI), 2n))), SE.set_msb(SX.le_bytes(32n, FS.fmul(P, b, ZI)), U32.from_nat(Nat.mod(FS.fmul(P, a, ZI), 2n))), Equal.trans(List<&2, U32>, PT.set_top(F.to_bytes(F.mul(y, zi)), F.parity(F.mul(x, zi))), PT.set_top(SX.le_bytes(32n, FS.fmul(P, b, ZI)), F.parity(F.mul(x, zi))), PT.set_top(SX.le_bytes(32n, FS.fmul(P, b, ZI)), U32.from_nat(Nat.mod(FS.fmul(P, a, ZI), 2n))), e1, e2), set_eq(SX.le_bytes(32n, FS.fmul(P, b, ZI)), U32.from_nat(Nat.mod(FS.fmul(P, a, ZI), 2n))))