~/jendhub

proofs/crypto/ed25519/pdec.bend

bend-collections-laws-crypto@1.0.0.0 · 196 lines · 16 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/freeze.bend as FZ
19import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/cong.bend as G
20import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/rel.bend as RL
21import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/xbits.bend as XB
22import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/ladder.bend as LD
23import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/scalar.bend as SC
24import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/prel.bend as PR
25import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/pcodec.bend as PC
26import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend as M3
27
28# Decoding (RFC 8032 5.1.3) of src/crypto/ed25519/point.bend against
29# spec/crypto/ed25519.bend: for every 32-byte string both reject, or both
30# accept with related points; and the base point.
31
32def v(+x: U32) -> Nat:
33  U32.to_nat(x)
34
35# y >= p exactly when the carry of y + 2^256 - p is not 0
36def hv_p(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}) -> {Nat.add(K.valo(one, F.comp_p()), 1n+pp) == SC.T(one) : Nat}:
37  +P = {1n+pp : Nat}
38  +e1 = M3.cong_l(K.valo(one, F.comp_p()), Nat.add(P, 38n), P, FZ.comp_p_val(one, h1, pp, hP))
39  +e2 = Equal.trans(Nat, Nat.add(Nat.add(P, 38n), P), Nat.add(P, Nat.add(38n, P)), Nat.add(Nat.add(P, P), 38n), NA.add_assoc(P, 38n, P), Equal.trans(Nat, Nat.add(P, Nat.add(38n, P)), Nat.add(P, Nat.add(P, 38n)), Nat.add(Nat.add(P, P), 38n), M3.cong_r(P, Nat.add(38n, P), Nat.add(P, 38n), NA.add_comm(38n, P)), Equal.sym(Nat, Nat.add(Nat.add(P, P), 38n), Nat.add(P, Nat.add(P, 38n)), NA.add_assoc(P, P, 38n))))
40  Equal.trans(Nat, Nat.add(K.valo(one, F.comp_p()), P), Nat.add(Nat.add(P, 38n), P), SC.T(one), e1, Equal.trans(Nat, Nat.add(Nat.add(P, 38n), P), Nat.add(Nat.add(P, P), 38n), SC.T(one), e2, Equal.sym(Nat, SC.T(one), Nat.add(Nat.add(P, P), 38n), FZ.t_val(one, h1, pp, hP))))
41
42def ge_p_eq(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +y: List<&2, U32>, +hy: {LM.okb(32n, y, 255n) == True{} : Bool}) -> {PT.ge_p(y) == Bool.not(Nat.is_lt(FS.value(y), 1n+pp)) : Bool}:
43  Equal.cong(Bool, Bool, z => Bool.not(z), U32.is_eq(LM.cc(F.carry(F.addl(y, F.comp_p()), 0)), 0), Nat.is_lt(FS.value(y), 1n+pp), SC.lt_by(one, h1, pp, y, F.comp_p(), hy, {==}, hv_p(one, h1, pp, hP), Nat.is_lt(v(LM.cc(F.carry(F.addl(y, F.comp_p()), 0))), one), {==}))
44
45# ---- the end of decoding: the sign of x ----
46
47def dec_fin_rel_core(+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}, +y: List<&2, U32>, +b: Nat, +ry: RL.R(pp, y, b), +x0: U32, +b0: Nat, +hx0: {v(x0) == b0 : Nat}, +hb0: {Nat.is_le(b0, 1n) == True{} : Bool}, +fs: Bool, +hf: {Bool.and(F.is_zero(x), U32.is_eq(x0, 1)) == fs : Bool}) -> PC.MR(pp, PT.dec_fin(x, y, x0, fs), SE.dec_fin(1n+pp, a, b, b0, fs)):
48  match fs:
49    case True{}:
50      {==}
51    case False{}:
52      +P = {1n+pp : Nat}
53      +s = U32.xor(F.parity(x), x0)
54      +S = SX.bxor(Nat.mod(a, 2n), b0)
55      +hs = XB.xor_bits(F.parity(x), x0, Nat.mod(a, 2n), b0, PC.par_rel(one, h1, pp, hP, x, a, rx, ha), hx0, PC.mod2_le(a), hb0)
56      +hsb = XB.bxor_le(Nat.mod(a, 2n), b0, hb0)
57      +nx = F.neg(x)
58      +NX = FS.fsub(P, 0n, a)
59      +rn = PR.rsub(one, h1, pp, hP, F.zero(), x, 0n, a, PC.r_zero(pp), rx)
60      +ox = RL.r_o(pp, x, a, rx)
61      +on = RL.r_o(pp, nx, NX, rn)
62      +x2 = F.select(s, x, nx)
63      +X2 = SX.cs_fst(S, a, NX)
64      +r2 = RL.mkR(pp, x2, X2, LD.o_sel(one, h1, s, S, hs, hsb, x, nx, ox, on), LD.c_fst(one, h1, pp, s, S, hs, hsb, x, nx, a, NX, ox, RL.r_c(pp, x, a, rx), on, RL.r_c(pp, nx, NX, rn)))
65      PR.mk(pp, x2, y, F.one(), F.mul(x2, y), X2, b, 1n, FS.fmul(P, X2, b), r2, ry, PC.r_one(pp), PR.rmul(one, h1, pp, hP, x2, y, X2, b, r2, ry))
66
67def dec_fin_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}, +y: List<&2, U32>, +b: Nat, +ry: RL.R(pp, y, b), +x0: U32, +b0: Nat, +hx0: {v(x0) == b0 : Nat}, +hb0: {Nat.is_le(b0, 1n) == True{} : Bool}, +fs: Bool, +hf: {Bool.and(F.is_zero(x), U32.is_eq(x0, 1)) == fs : Bool}) -> PC.MR(pp, PT.dec_fin(x, y, x0, Bool.and(F.is_zero(x), U32.is_eq(x0, 1))), SE.dec_fin(1n+pp, a, b, b0, fs)):
68  %Equal.sym(Bool, Bool.and(F.is_zero(x), U32.is_eq(x0, 1)), fs, hf) : PC.MR(pp, PT.dec_fin(x, y, x0, _), SE.dec_fin(1n+pp, a, b, b0, fs))
69  dec_fin_rel_core(one, h1, pp, hP, x, a, rx, ha, y, b, ry, x0, b0, hx0, hb0, fs, hf)
70
71def fail_eq(+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}, +x0: U32, +b0: Nat, +hx0: {v(x0) == b0 : Nat}) -> {Bool.and(F.is_zero(x), U32.is_eq(x0, 1)) == Bool.and(Nat.is_eq(a, 0n), Nat.is_eq(b0, 1n)) : Bool}:
72  +e1 = PC.iz_rel(one, h1, pp, hP, x, a, rx, ha)
73  +e2 = Equal.trans(Bool, U32.is_eq(x0, 1), Nat.is_eq(v(x0), 1n), Nat.is_eq(b0, 1n), PC.u32_eq_nat(x0, 1), Equal.cong(Nat, Bool, z => Nat.is_eq(z, 1n), v(x0), b0, hx0))
74  Equal.trans(Bool, Bool.and(F.is_zero(x), U32.is_eq(x0, 1)), Bool.and(Nat.is_eq(a, 0n), U32.is_eq(x0, 1)), Bool.and(Nat.is_eq(a, 0n), Nat.is_eq(b0, 1n)), Equal.cong(Bool, Bool, z => Bool.and(z, U32.is_eq(x0, 1)), F.is_zero(x), Nat.is_eq(a, 0n), e1), Equal.cong(Bool, Bool, z => Bool.and(Nat.is_eq(a, 0n), z), U32.is_eq(x0, 1), Nat.is_eq(b0, 1n), e2))
75
76# ---- the root choice ----
77
78def dec_root_rel_core(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +cs: PT.Cs, +rs: RL.R(pp, PT.cs_s(cs), SE.sqm1(1n+pp)), +x: List<&2, U32>, +a: Nat, +rx: RL.R(pp, x, a), +ha: {Nat.mod(a, 1n+pp) == a : Nat}, +y: List<&2, U32>, +b: Nat, +ry: RL.R(pp, y, b), +x0: U32, +b0: Nat, +hx0: {v(x0) == b0 : Nat}, +hb0: {Nat.is_le(b0, 1n) == True{} : Bool}, +u: List<&2, U32>, +vxx: List<&2, U32>, +iu: Bool, +inu: Bool, +su: Bool, +snu: Bool, +hu: {iu == su : Bool}, +hnu: {inu == snu : Bool}) -> PC.MR(pp, PT.dec_root(cs, x, y, x0, u, vxx, su, snu), SE.dec_root(1n+pp, a, b, b0, su, snu)):
79  match su snu:
80    case True{} _:
81      dec_fin_rel(one, h1, pp, hP, x, a, rx, ha, y, b, ry, x0, b0, hx0, hb0, Bool.and(Nat.is_eq(a, 0n), Nat.is_eq(b0, 1n)), fail_eq(one, h1, pp, hP, x, a, rx, ha, x0, b0, hx0))
82    case False{} True{}:
83      +P = {1n+pp : Nat}
84      +x1 = F.mul(x, PT.cs_s(cs))
85      +X1 = FS.fmul(P, a, SE.sqm1(P))
86      +r1 = PR.rmul(one, h1, pp, hP, x, PT.cs_s(cs), a, SE.sqm1(P), rx, rs)
87      +h1r = PC.red(pp, Nat.mul(a, SE.sqm1(P)))
88      dec_fin_rel(one, h1, pp, hP, x1, X1, r1, h1r, y, b, ry, x0, b0, hx0, hb0, Bool.and(Nat.is_eq(X1, 0n), Nat.is_eq(b0, 1n)), fail_eq(one, h1, pp, hP, x1, X1, r1, h1r, x0, b0, hx0))
89    case False{} False{}:
90      {==}
91
92# ---- after the y check ----
93
94def dec_root_rel(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +cs: PT.Cs, +rs: RL.R(pp, PT.cs_s(cs), SE.sqm1(1n+pp)), +x: List<&2, U32>, +a: Nat, +rx: RL.R(pp, x, a), +ha: {Nat.mod(a, 1n+pp) == a : Nat}, +y: List<&2, U32>, +b: Nat, +ry: RL.R(pp, y, b), +x0: U32, +b0: Nat, +hx0: {v(x0) == b0 : Nat}, +hb0: {Nat.is_le(b0, 1n) == True{} : Bool}, +u: List<&2, U32>, +vxx: List<&2, U32>, +iu: Bool, +inu: Bool, +su: Bool, +snu: Bool, +hu: {iu == su : Bool}, +hnu: {inu == snu : Bool}) -> PC.MR(pp, PT.dec_root(cs, x, y, x0, u, vxx, iu, inu), SE.dec_root(1n+pp, a, b, b0, su, snu)):
95  %Equal.sym(Bool, iu, su, hu) : PC.MR(pp, PT.dec_root(cs, x, y, x0, u, vxx, _, inu), SE.dec_root(1n+pp, a, b, b0, su, snu))
96  %Equal.sym(Bool, inu, snu, hnu) : PC.MR(pp, PT.dec_root(cs, x, y, x0, u, vxx, su, _), SE.dec_root(1n+pp, a, b, b0, su, snu))
97  dec_root_rel_core(one, h1, pp, hP, cs, rs, x, a, rx, ha, y, b, ry, x0, b0, hx0, hb0, u, vxx, iu, inu, su, snu, hu, hnu)
98
99def nf(+b: Bool, +h: {Bool.not(b) == False{} : Bool}) -> {b == True{} : Bool}:
100  match b:
101    case True{}:
102      {==}
103    case False{}:
104      Empty.absurd({False{} == True{} : Bool}, L.true_false(h))
105
106def dec_y_rel_core(+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)), +y: List<&2, U32>, +Y: Nat, +hyv: {FS.value(y) == Y : Nat}, +hy: {LM.okb(32n, y, 255n) == True{} : Bool}, +x0: U32, +b0: Nat, +hx0: {v(x0) == b0 : Nat}, +hb0: {Nat.is_le(b0, 1n) == True{} : Bool}, +bad: Bool, +hbad: {PT.ge_p(y) == bad : Bool}, +hlt: {Bool.not(Nat.is_lt(Y, 1n+pp)) == bad : Bool}) -> PC.MR(pp, PT.dec_y(cs, y, x0, bad), SE.dec_y(1n+pp, D, Y, b0, bad)):
107  match bad:
108    case True{}:
109      {==}
110    case False{}:
111      +P = {1n+pp : Nat}
112      +lt = nf(Nat.is_lt(Y, P), hlt)
113      +ry = RL.mkR(pp, y, Y, hy, G.c_eq(pp, FS.value(y), Y, hyv))
114      +hYr = NR.mod_of(0n, pp, Y, lt)
115      +yy = F.sq(y)
116      +YY = FS.fmul(P, Y, Y)
117      +ryy = PR.rsq(one, h1, pp, hP, y, Y, ry)
118      +u = F.sub(yy, F.one())
119      +UU = FS.fsub(P, YY, 1n)
120      +ru = PR.rsub(one, h1, pp, hP, yy, F.one(), YY, 1n, ryy, PC.r_one(pp))
121      +vv = F.add(F.mul(PT.cs_d(cs), yy), F.one())
122      +VV = FS.fadd(P, FS.fmul(P, D, YY), 1n)
123      +rv = PR.radd(one, h1, pp, hP, F.mul(PT.cs_d(cs), yy), F.one(), FS.fmul(P, D, YY), 1n, PR.rmul(one, h1, pp, hP, PT.cs_d(cs), yy, D, YY, rd, ryy), PC.r_one(pp))
124      +v3 = F.mul(F.sq(vv), vv)
125      +V3 = FS.fmul(P, FS.fmul(P, VV, VV), VV)
126      +rv3 = PR.rmul(one, h1, pp, hP, F.sq(vv), vv, FS.fmul(P, VV, VV), VV, PR.rsq(one, h1, pp, hP, vv, VV, rv), rv)
127      +v7 = F.mul(F.sq(v3), vv)
128      +V7 = FS.fmul(P, FS.fmul(P, V3, V3), VV)
129      +rv7 = PR.rmul(one, h1, pp, hP, F.sq(v3), vv, FS.fmul(P, V3, V3), VV, PR.rsq(one, h1, pp, hP, v3, V3, rv3), rv)
130      +uv7 = F.mul(u, v7)
131      +UV7 = FS.fmul(P, UU, V7)
132      +ruv7 = PR.rmul(one, h1, pp, hP, u, v7, UU, V7, ru, rv7)
133      +pw = F.pow_p58(uv7)
134      +PWV = FS.fpow(P, UV7, Nat.div(Nat.sub(P, 5n), 8n))
135      +rpw = RL.r_p58(one, h1, pp, hP, uv7, UV7, RL.r_o(pp, uv7, UV7, ruv7), RL.r_c(pp, uv7, UV7, ruv7))
136      +x = F.mul(F.mul(u, v3), pw)
137      +XX = FS.fmul(P, FS.fmul(P, UU, V3), PWV)
138      +rx = PR.rmul(one, h1, pp, hP, F.mul(u, v3), pw, FS.fmul(P, UU, V3), PWV, PR.rmul(one, h1, pp, hP, u, v3, UU, V3, ru, rv3), rpw)
139      +vxx = F.mul(vv, F.sq(x))
140      +VXX = FS.fmul(P, VV, FS.fmul(P, XX, XX))
141      +rvxx = PR.rmul(one, h1, pp, hP, vv, F.sq(x), VV, FS.fmul(P, XX, XX), rv, PR.rsq(one, h1, pp, hP, x, XX, rx))
142      +NU = FS.fsub(P, 0n, UU)
143      +rnu = PR.rsub(one, h1, pp, hP, F.zero(), u, 0n, UU, PC.r_zero(pp), ru)
144      +eu = PC.eq_rel(one, h1, pp, hP, vxx, u, VXX, UU, rvxx, ru, PC.red(pp, Nat.mul(VV, FS.fmul(P, XX, XX))), PC.red(pp, Nat.sub(Nat.add(YY, P), Nat.mod(1n, P))))
145      +enu = PC.eq_rel(one, h1, pp, hP, vxx, F.neg(u), VXX, NU, rvxx, rnu, PC.red(pp, Nat.mul(VV, FS.fmul(P, XX, XX))), PC.red(pp, Nat.sub(Nat.add(0n, P), Nat.mod(UU, P))))
146      dec_root_rel(one, h1, pp, hP, cs, rs, x, XX, rx, PC.red(pp, Nat.mul(FS.fmul(P, UU, V3), PWV)), y, Y, ry, x0, b0, hx0, hb0, u, vxx, F.eq(vxx, u), F.eq(vxx, F.neg(u)), Nat.is_eq(VXX, UU), Nat.is_eq(VXX, NU), eu, enu)
147
148def dec_y_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)), +y: List<&2, U32>, +Y: Nat, +hyv: {FS.value(y) == Y : Nat}, +hy: {LM.okb(32n, y, 255n) == True{} : Bool}, +x0: U32, +b0: Nat, +hx0: {v(x0) == b0 : Nat}, +hb0: {Nat.is_le(b0, 1n) == True{} : Bool}, +bad: Bool, +hbad: {PT.ge_p(y) == bad : Bool}, +hlt: {Bool.not(Nat.is_lt(Y, 1n+pp)) == bad : Bool}) -> PC.MR(pp, PT.dec_y(cs, y, x0, PT.ge_p(y)), SE.dec_y(1n+pp, D, Y, b0, bad)):
149  %Equal.sym(Bool, PT.ge_p(y), bad, hbad) : PC.MR(pp, PT.dec_y(cs, y, x0, _), SE.dec_y(1n+pp, D, Y, b0, bad))
150  dec_y_rel_core(one, h1, pp, hP, cs, D, rd, rs, y, Y, hyv, hy, x0, b0, hx0, hb0, bad, hbad, hlt)
151
152def decode_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)), +bs: List<&2, U32>, +hb: {LM.okb(32n, bs, 255n) == True{} : Bool}) -> PC.MR(pp, PT.decode(cs, bs), SE.decode(1n+pp, D, bs)):
153  +y = F.mask_top(bs)
154  +Y = FS.value(SX.mask_last(bs))
155  +hyv = Equal.cong(List<&2, U32>, Nat, z => FS.value(z), F.mask_top(bs), SX.mask_last(bs), XB.mask_eq(bs))
156  +hy = XB.mask_okb(31n, bs, hb)
157  +hl = LM.okb_lea(32n, bs, 255n, hb)
158  +hbad = Equal.trans(Bool, PT.ge_p(y), Bool.not(Nat.is_lt(FS.value(y), 1n+pp)), Bool.not(Nat.is_lt(Y, 1n+pp)), ge_p_eq(one, h1, pp, hP, y, hy), Equal.cong(Nat, Bool, z => Bool.not(Nat.is_lt(z, 1n+pp)), FS.value(y), Y, hyv))
159  dec_y_rel(one, h1, pp, hP, cs, D, rd, rs, y, Y, hyv, hy, X.kbit(bs, 255n), SX.kbit(FS.value(bs), 255n), XB.kbit_val(bs, 255n, hl), XB.kbit_le(bs, 255n, hl), Bool.not(Nat.is_lt(Y, 1n+pp)), hbad, {==})
160
161# ---- the base point ----
162
163def le_bytes_ok(+n: Nat, +x: Nat) -> {LM.okb(n, SX.le_bytes(n, x), 255n) == True{} : Bool}:
164  match n:
165    case 0n:
166      {==}
167    case 1n+ +m:
168      +r = Nat.mod(x, 256n)
169      +hr = NR.dm_lt(255n, x)
170      +e = U.to_nat_from_nat(r, 8n, {==}, hr)
171      +h = L.subst(Nat, z => {Nat.is_le(z, 255n) == True{} : Bool}, r, v(U32.from_nat(r)), Equal.sym(Nat, v(U32.from_nat(r)), r, e), N.lt_succ_le(r, 255n, hr))
172      L.and_intro(Nat.is_le(v(U32.from_nat(r)), 255n), LM.okb(m, SX.le_bytes(m, Nat.div(x, 256n)), 255n), h, le_bytes_ok(m, Nat.div(x, 256n)))
173
174def identity_rel(+pp: Nat) -> PR.Rp(pp, PT.identity(), SE.identity()):
175  PR.mk(pp, F.zero(), F.one(), F.one(), F.zero(), 0n, 1n, 1n, 0n, PC.r_zero(pp), PC.r_one(pp), PC.r_one(pp), PC.r_zero(pp))
176
177def base_of_rel(+pp: Nat, +m: Maybe<&2, PT.Pt>, +sm: Maybe<&2, SE.EPt>, +h: PC.MR(pp, m, sm)) -> PR.Rp(pp, PT.base_of(m), SE.base_of(sm)):
178  match m sm:
179    case None{} None{}:
180      identity_rel(pp)
181    case Some{+p} Some{+sp}:
182      h
183    case None{} Some{sp}:
184      Empty.absurd(PR.Rp(pp, PT.identity(), sp), L.true_false(h))
185    case Some{p} None{}:
186      Empty.absurd(PR.Rp(pp, p, SE.identity()), L.true_false(h))
187
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)))