~/jendhub

proofs/crypto/curve25519/mulw.bend

bend-collections-laws-crypto@1.0.0.0 · 183 lines · 27 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/src/crypto/curve25519/field.bend as F
5import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
6import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
7import bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend as WD
8import bend-collections-laws-crypto@1.0.0.0/proofs/lib/arith.bend as AR
9import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
10import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as NR
11import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend as M
12import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend as LM
13import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/poly.bend as PL
14import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/fold.bend as FD
15import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/reduce.bend as RD
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
18
19# mul, sq and mul_small of src/crypto/curve25519/field.bend: the schoolbook
20# product of two tight elements has 63 limbs below 32 * 2^16 = 2^21; `wide`
21# folds limbs 32.. down by 38 (2^256 == 2 p + 38) into 32 limbs below 2^28;
22# `reduce` makes them tight. The value is the product mod p.
23
24def v(+x: U32) -> Nat:
25  U32.to_nat(x)
26
27# ---- the product's limb bound: 32 * 2^8 * 2^8 ----
28
29def cbn_add(+a: Nat, +b: Nat, +k: Nat) -> {PL.cbn(Nat.add(a, b), k) == Nat.add(PL.cbn(a, k), PL.cbn(b, k)) : Nat}:
30  match a:
31    case 0n:
32      {==}
33    case 1n+ +q:
34      Equal.trans(Nat, Nat.add(k, PL.cbn(Nat.add(q, b), k)), Nat.add(k, Nat.add(PL.cbn(q, k), PL.cbn(b, k))), Nat.add(Nat.add(k, PL.cbn(q, k)), PL.cbn(b, k)), M.cong_r(k, PL.cbn(Nat.add(q, b), k), Nat.add(PL.cbn(q, k), PL.cbn(b, k)), cbn_add(q, b, k)), Equal.sym(Nat, Nat.add(Nat.add(k, PL.cbn(q, k)), PL.cbn(b, k)), Nat.add(k, Nat.add(PL.cbn(q, k), PL.cbn(b, k))), NA.add_assoc(k, PL.cbn(q, k), PL.cbn(b, k))))
35
36def cbn_pow(+j: Nat, +k: Nat) -> {PL.cbn(WD.sc(j, 1n), k) == WD.sc(j, k) : Nat}:
37  match j:
38    case 0n:
39      N.add_zero(k)
40    case 1n+ +q:
41      +n = WD.sc(q, 1n)
42      +e1 = Equal.cong(Nat, Nat, t => PL.cbn(t, k), Nat.double(n), Nat.add(n, n), NA.double_self(n))
43      +e2 = cbn_add(n, n, k)
44      +e3 = M.cong_add(PL.cbn(n, k), WD.sc(q, k), PL.cbn(n, k), WD.sc(q, k), cbn_pow(q, k), cbn_pow(q, k))
45      Equal.trans(Nat, PL.cbn(Nat.double(n), k), Nat.add(PL.cbn(n, k), PL.cbn(n, k)), WD.sc(1n+q, k), Equal.trans(Nat, PL.cbn(Nat.double(n), k), PL.cbn(Nat.add(n, n), k), Nat.add(PL.cbn(n, k), PL.cbn(n, k)), e1, e2), Equal.trans(Nat, Nat.add(PL.cbn(n, k), PL.cbn(n, k)), Nat.add(WD.sc(q, k), WD.sc(q, k)), WD.sc(1n+q, k), e3, M.sc_dbl(q, k)))
46
47def cb_okb(+n: Nat, +xs: List<&2, U32>, +b: Nat, +k: Nat, +e: {LM.okb(n, xs, b) == True{} : Bool}) -> {PL.cb(xs, k) == PL.cbn(n, k) : Nat}:
48  match n xs:
49    case 0n Nil{}:
50      {==}
51    case 0n Con{y, yt}:
52      Empty.absurd({PL.cb(Con{y, yt}, k) == 0n : Nat}, L.false_true(e))
53    case 1n+m Nil{}:
54      Empty.absurd({0n == PL.cbn(1n+m, k) : Nat}, L.false_true(e))
55    case 1n+ +m Con{+y, +yt}:
56      M.cong_r(k, PL.cb(yt, k), PL.cbn(m, k), cb_okb(m, yt, b, k, LM.okb_tail(m, y, yt, b, e)))
57
58def mm8(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.mul(WD.sc(8n, one), WD.sc(8n, one)) == WD.sc(16n, one) : Nat}:
59  Equal.trans(Nat, Nat.mul(WD.sc(8n, one), WD.sc(8n, one)), WD.sc(16n, Nat.mul(one, one)), WD.sc(16n, one), M.mul_sc2(8n, 8n, one, one), M.cong_sc(16n, Nat.mul(one, one), one, K.one_k(one, h1, one)))
60
61def cb32(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +b: Nat, +ha: {LM.okb(32n, a, b) == True{} : Bool}) -> {PL.cb(a, Nat.mul(WD.sc(8n, one), WD.sc(8n, one))) == WD.sc(21n, one) : Nat}:
62  +mm = Nat.mul(WD.sc(8n, one), WD.sc(8n, one))
63  +e1 = cb_okb(32n, a, b, mm, ha)
64  +e2 = cbn_pow(5n, mm)
65  +e3 = M.cong_sc(5n, mm, WD.sc(16n, one), mm8(one, h1))
66  Equal.trans(Nat, PL.cb(a, mm), PL.cbn(32n, mm), WD.sc(21n, one), e1, Equal.trans(Nat, PL.cbn(32n, mm), WD.sc(5n, mm), WD.sc(21n, one), e2, e3))
67
68def lea8(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +ha: {LM.okb(32n, a, 255n) == True{} : Bool}) -> {LM.lea(a, WD.sc(8n, one)) == True{} : Bool}:
69  LM.lea_mono(a, 255n, WD.sc(8n, one), FD.le255(one, h1, 0n), LM.okb_lea(32n, a, 255n, ha))
70
71def conv_ge(+m: Nat, +xs: List<&2, U32>, +ys: List<&2, U32>, +n: Nat, +b: Nat, +hx: {LM.okb(1n+m, xs, b) == True{} : Bool}, +hy: {PL.len_ge(n, ys) == True{} : Bool}) -> {PL.len_ge(n, F.conv(xs, ys)) == True{} : Bool}:
72  match xs:
73    case Nil{}:
74      Empty.absurd({PL.len_ge(n, Nil{}) == True{} : Bool}, L.false_true(hx))
75    case Con{+x, +xt}:
76      PL.conv_len_ge(n, x, xt, ys, hy)
77
78def conv_hc(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +ha: {LM.okb(32n, a, 255n) == True{} : Bool}) -> {Nat.is_lt(PL.cb(a, Nat.mul(WD.sc(8n, one), WD.sc(8n, one))), WD.sc(32n, one)) == True{} : Bool}:
79  L.subst(Nat, z => {Nat.is_lt(z, WD.sc(32n, one)) == True{} : Bool}, WD.sc(21n, one), PL.cb(a, Nat.mul(WD.sc(8n, one), WD.sc(8n, one))), Equal.sym(Nat, PL.cb(a, Nat.mul(WD.sc(8n, one), WD.sc(8n, one))), WD.sc(21n, one), cb32(one, h1, a, 255n, ha)), LM.sc_lt(10n, 21n, one, h1))
80
81def conv_lea21(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +b: List<&2, U32>, +ha: {LM.okb(32n, a, 255n) == True{} : Bool}, +hb: {LM.okb(32n, b, 255n) == True{} : Bool}) -> {LM.lea(F.conv(a, b), WD.sc(21n, one)) == True{} : Bool}:
82  +s8 = WD.sc(8n, one)
83  +e = PL.conv_lea(one, h1, a, b, s8, s8, lea8(one, h1, a, ha), lea8(one, h1, b, hb), conv_hc(one, h1, a, ha))
84  L.subst(Nat, z => {LM.lea(F.conv(a, b), z) == True{} : Bool}, PL.cb(a, Nat.mul(s8, s8)), WD.sc(21n, one), cb32(one, h1, a, 255n, ha), e)
85
86def conv_val(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +b: List<&2, U32>, +ha: {LM.okb(32n, a, 255n) == True{} : Bool}, +hb: {LM.okb(32n, b, 255n) == True{} : Bool}) -> {FS.value(F.conv(a, b)) == Nat.mul(FS.value(a), FS.value(b)) : Nat}:
87  +s8 = WD.sc(8n, one)
88  PL.conv_val(one, h1, a, b, s8, s8, lea8(one, h1, a, ha), lea8(one, h1, b, hb), conv_hc(one, h1, a, ha))
89
90# ---- wide ----
91
92def m38_27(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_le(Nat.mul(38n, WD.sc(21n, one)), WD.sc(27n, one)) == True{} : Bool}:
93  FD.m38(WD.sc(21n, one))
94
95def wsum_le(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_le(Nat.add(WD.sc(21n, one), Nat.mul(38n, WD.sc(21n, one))), WD.sc(28n, one)) == True{} : Bool}:
96  +a = M.le_add2(WD.sc(21n, one), Nat.mul(38n, WD.sc(21n, one)), WD.sc(27n, one), WD.sc(27n, one), M.sc_mono(6n, 21n, one), m38_27(one, h1))
97  L.subst(Nat, z => {Nat.is_le(Nat.add(WD.sc(21n, one), Nat.mul(38n, WD.sc(21n, one))), z) == True{} : Bool}, Nat.add(WD.sc(27n, one), WD.sc(27n, one)), WD.sc(28n, one), M.sc_dbl(27n, one), a)
98
99def wsum_lt(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_lt(Nat.add(WD.sc(21n, one), Nat.mul(38n, WD.sc(21n, one))), WD.sc(32n, one)) == True{} : Bool}:
100  N.le_lt_trans(Nat.add(WD.sc(21n, one), Nat.mul(38n, WD.sc(21n, one))), WD.sc(28n, one), WD.sc(32n, one), wsum_le(one, h1), LM.sc_lt(3n, 28n, one, h1))
101
102def m38_lt(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_lt(Nat.mul(38n, WD.sc(21n, one)), WD.sc(32n, one)) == True{} : Bool}:
103  N.le_lt_trans(Nat.mul(38n, WD.sc(21n, one)), WD.sc(27n, one), WD.sc(32n, one), m38_27(one, h1), LM.sc_lt(4n, 27n, one, h1))
104
105def wide_okb(+one: Nat, +h1: {one == 1n : Nat}, +zs: List<&2, U32>, +hl: {LM.lea(zs, WD.sc(21n, one)) == True{} : Bool}, +hge: {PL.len_ge(32n, zs) == True{} : Bool}, +hle: {PL.len_le(64n, zs) == True{} : Bool}) -> {LM.okb(32n, F.wide(zs), WD.sc(28n, one)) == True{} : Bool}:
106  +k21 = WD.sc(21n, one)
107  +T = F.take(32n, zs)
108  +D = F.drop(32n, zs)
109  +okT = PL.take_okb(32n, zs, k21, hge, hl)
110  +leD = PL.drop_lea(32n, zs, k21, hl)
111  +lnD = PL.drop_len_le(32n, 32n, zs, hle)
112  +leS = PL.scal_lea(one, h1, 38, D, 38n, k21, N.le_refl(38n), leD, m38_lt(one, h1))
113  +lnS = PL.scal_len_le(32n, 38, D, lnD)
114  +e = PL.addl_okb(one, h1, 32n, T, F.scal(38, D), k21, Nat.mul(38n, k21), okT, leS, lnS, wsum_lt(one, h1))
115  PL.okb_mono(32n, F.addl(T, F.scal(38, D)), Nat.add(k21, Nat.mul(38n, k21)), WD.sc(28n, one), wsum_le(one, h1), e)
116
117def wide_mod(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +zs: List<&2, U32>, +hl: {LM.lea(zs, WD.sc(21n, one)) == True{} : Bool}, +hge: {PL.len_ge(32n, zs) == True{} : Bool}) -> {Nat.mod(FS.value(F.wide(zs)), 1n+pp) == Nat.mod(FS.value(zs), 1n+pp) : Nat}:
118  +k21 = WD.sc(21n, one)
119  +T = F.take(32n, zs)
120  +D = F.drop(32n, zs)
121  +okT = PL.take_okb(32n, zs, k21, hge, hl)
122  +leD = PL.drop_lea(32n, zs, k21, hl)
123  +leS = PL.scal_lea(one, h1, 38, D, 38n, k21, N.le_refl(38n), leD, m38_lt(one, h1))
124  +VT = FS.value(T)
125  +VD = FS.value(D)
126  +ew = PL.addl_val(one, h1, T, F.scal(38, D), k21, Nat.mul(38n, k21), LM.okb_lea(32n, T, k21, okT), leS, wsum_lt(one, h1))
127  +es = PL.scal_val(one, h1, 38, D, 38n, k21, N.le_refl(38n), leD, m38_lt(one, h1))
128  +ew2 = Equal.trans(Nat, FS.value(F.wide(zs)), Nat.add(VT, FS.value(F.scal(38, D))), Nat.add(VT, Nat.mul(38n, VD)), ew, M.cong_r(VT, FS.value(F.scal(38, D)), Nat.mul(38n, VD), es))
129  +ez = Equal.trans(Nat, FS.value(zs), Nat.add(VT, LM.sh(T, VD)), Nat.add(VT, LM.shn(32n, VD)), PL.take_drop_val(32n, zs), M.cong_r(VT, LM.sh(T, VD), LM.shn(32n, VD), LM.sh_okb(32n, T, k21, VD, okT)))
130  +ef = FD.fold_id(one, h1, pp, hP, VT, VD)
131  +q = Nat.add(VD, VD)
132  +ez2 = Equal.trans(Nat, FS.value(zs), Nat.add(VT, LM.shn(32n, VD)), Nat.add(Nat.mul(q, 1n+pp), FS.value(F.wide(zs))), ez, Equal.trans(Nat, Nat.add(VT, LM.shn(32n, VD)), Nat.add(Nat.mul(q, 1n+pp), Nat.add(VT, Nat.mul(38n, VD))), Nat.add(Nat.mul(q, 1n+pp), FS.value(F.wide(zs))), ef, M.cong_r(Nat.mul(q, 1n+pp), Nat.add(VT, Nat.mul(38n, VD)), FS.value(F.wide(zs)), Equal.sym(Nat, FS.value(F.wide(zs)), Nat.add(VT, Nat.mul(38n, VD)), ew2))))
133  Equal.trans(Nat, Nat.mod(FS.value(F.wide(zs)), 1n+pp), Nat.mod(Nat.add(Nat.mul(q, 1n+pp), FS.value(F.wide(zs))), 1n+pp), Nat.mod(FS.value(zs), 1n+pp), Equal.sym(Nat, Nat.mod(Nat.add(Nat.mul(q, 1n+pp), FS.value(F.wide(zs))), 1n+pp), Nat.mod(FS.value(F.wide(zs)), 1n+pp), NR.absorb(pp, q, FS.value(F.wide(zs)))), M.cong_mod(1n+pp, Nat.add(Nat.mul(q, 1n+pp), FS.value(F.wide(zs))), FS.value(zs), Equal.sym(Nat, FS.value(zs), Nat.add(Nat.mul(q, 1n+pp), FS.value(F.wide(zs))), ez2)))
134
135# ---- mul, sq ----
136
137def wide_in(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +b: List<&2, U32>, +ha: {LM.okb(32n, a, 255n) == True{} : Bool}, +hb: {LM.okb(32n, b, 255n) == True{} : Bool}) -> {LM.okb(32n, F.wide(F.conv(a, b)), WD.sc(28n, one)) == True{} : Bool}:
138  +zs = F.conv(a, b)
139  +hge = conv_ge(31n, a, b, 32n, 255n, ha, PL.okb_len_ge(32n, b, 255n, hb))
140  +hle = PL.conv_len_le(32n, 32n, a, b, PL.okb_len_le(32n, a, 255n, ha), PL.okb_len_le(32n, b, 255n, hb))
141  wide_okb(one, h1, zs, conv_lea21(one, h1, a, b, ha, hb), hge, hle)
142
143def mul_okb(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +b: List<&2, U32>, +ha: {LM.okb(32n, a, 255n) == True{} : Bool}, +hb: {LM.okb(32n, b, 255n) == True{} : Bool}) -> {LM.okb(32n, F.mul(a, b), 255n) == True{} : Bool}:
144  RD.reduce_okb(one, h1, F.wide(F.conv(a, b)), wide_in(one, h1, a, b, ha, hb))
145
146def mul_mod(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +a: List<&2, U32>, +b: List<&2, U32>, +ha: {LM.okb(32n, a, 255n) == True{} : Bool}, +hb: {LM.okb(32n, b, 255n) == True{} : Bool}) -> {Nat.mod(FS.value(F.mul(a, b)), 1n+pp) == Nat.mod(Nat.mul(FS.value(a), FS.value(b)), 1n+pp) : Nat}:
147  +zs = F.conv(a, b)
148  +hge = conv_ge(31n, a, b, 32n, 255n, ha, PL.okb_len_ge(32n, b, 255n, hb))
149  +e1 = RD.reduce_mod(one, h1, pp, hP, F.wide(zs), wide_in(one, h1, a, b, ha, hb))
150  +e2 = wide_mod(one, h1, pp, hP, zs, conv_lea21(one, h1, a, b, ha, hb), hge)
151  +e3 = M.cong_mod(1n+pp, FS.value(zs), Nat.mul(FS.value(a), FS.value(b)), conv_val(one, h1, a, b, ha, hb))
152  Equal.trans(Nat, Nat.mod(FS.value(F.mul(a, b)), 1n+pp), Nat.mod(FS.value(F.wide(zs)), 1n+pp), Nat.mod(Nat.mul(FS.value(a), FS.value(b)), 1n+pp), e1, Equal.trans(Nat, Nat.mod(FS.value(F.wide(zs)), 1n+pp), Nat.mod(FS.value(zs), 1n+pp), Nat.mod(Nat.mul(FS.value(a), FS.value(b)), 1n+pp), e2, e3))
153
154def sq_okb(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +ha: {LM.okb(32n, a, 255n) == True{} : Bool}) -> {LM.okb(32n, F.sq(a), 255n) == True{} : Bool}:
155  mul_okb(one, h1, a, a, ha, ha)
156
157def sq_mod(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +a: List<&2, U32>, +ha: {LM.okb(32n, a, 255n) == True{} : Bool}) -> {Nat.mod(FS.value(F.sq(a)), 1n+pp) == Nat.mod(Nat.mul(FS.value(a), FS.value(a)), 1n+pp) : Nat}:
158  mul_mod(one, h1, pp, hP, a, a, ha, ha)
159
160# ---- mul_small (k at most 2^17) ----
161
162def ms_lt(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_lt(Nat.mul(WD.sc(17n, one), 255n), WD.sc(32n, one)) == True{} : Bool}:
163  +a = M.le_mul2(WD.sc(17n, one), 255n, WD.sc(17n, one), WD.sc(8n, one), N.le_refl(WD.sc(17n, one)), FD.le255(one, h1, 0n))
164  +b = L.subst(Nat, z => {Nat.is_le(Nat.mul(WD.sc(17n, one), 255n), z) == True{} : Bool}, Nat.mul(WD.sc(17n, one), WD.sc(8n, one)), WD.sc(25n, one), Equal.trans(Nat, Nat.mul(WD.sc(17n, one), WD.sc(8n, one)), WD.sc(25n, Nat.mul(one, one)), WD.sc(25n, one), M.mul_sc2(17n, 8n, one, one), M.cong_sc(25n, Nat.mul(one, one), one, K.one_k(one, h1, one))), a)
165  N.le_lt_trans(Nat.mul(WD.sc(17n, one), 255n), WD.sc(25n, one), WD.sc(32n, one), b, LM.sc_lt(6n, 25n, one, h1))
166
167def ms_le(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_le(Nat.mul(WD.sc(17n, one), 255n), WD.sc(28n, one)) == True{} : Bool}:
168  +a = M.le_mul2(WD.sc(17n, one), 255n, WD.sc(17n, one), WD.sc(8n, one), N.le_refl(WD.sc(17n, one)), FD.le255(one, h1, 0n))
169  +b = L.subst(Nat, z => {Nat.is_le(Nat.mul(WD.sc(17n, one), 255n), z) == True{} : Bool}, Nat.mul(WD.sc(17n, one), WD.sc(8n, one)), WD.sc(25n, one), Equal.trans(Nat, Nat.mul(WD.sc(17n, one), WD.sc(8n, one)), WD.sc(25n, Nat.mul(one, one)), WD.sc(25n, one), M.mul_sc2(17n, 8n, one, one), M.cong_sc(25n, Nat.mul(one, one), one, K.one_k(one, h1, one))), a)
170  N.le_trans(Nat.mul(WD.sc(17n, one), 255n), WD.sc(25n, one), WD.sc(28n, one), b, M.sc_mono(3n, 25n, one))
171
172def scal_in(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +k: U32, +ha: {LM.okb(32n, a, 255n) == True{} : Bool}, +hk: {Nat.is_le(v(k), WD.sc(17n, one)) == True{} : Bool}) -> {LM.okb(32n, F.scal(k, a), WD.sc(28n, one)) == True{} : Bool}:
173  +e = PL.scal_okb(one, h1, 32n, k, a, WD.sc(17n, one), 255n, hk, ha, ms_lt(one, h1))
174  PL.okb_mono(32n, F.scal(k, a), Nat.mul(WD.sc(17n, one), 255n), WD.sc(28n, one), ms_le(one, h1), e)
175
176def mul_small_okb(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +k: U32, +ha: {LM.okb(32n, a, 255n) == True{} : Bool}, +hk: {Nat.is_le(v(k), WD.sc(17n, one)) == True{} : Bool}) -> {LM.okb(32n, F.mul_small(a, k), 255n) == True{} : Bool}:
177  RD.reduce_okb(one, h1, F.scal(k, a), scal_in(one, h1, a, k, ha, hk))
178
179def mul_small_mod(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +a: List<&2, U32>, +k: U32, +ha: {LM.okb(32n, a, 255n) == True{} : Bool}, +hk: {Nat.is_le(v(k), WD.sc(17n, one)) == True{} : Bool}) -> {Nat.mod(FS.value(F.mul_small(a, k)), 1n+pp) == Nat.mod(Nat.mul(FS.value(a), v(k)), 1n+pp) : Nat}:
180  +e1 = RD.reduce_mod(one, h1, pp, hP, F.scal(k, a), scal_in(one, h1, a, k, ha, hk))
181  +e2 = PL.scal_val(one, h1, k, a, WD.sc(17n, one), 255n, hk, LM.okb_lea(32n, a, 255n, ha), ms_lt(one, h1))
182  +e3 = Equal.trans(Nat, FS.value(F.scal(k, a)), Nat.mul(v(k), FS.value(a)), Nat.mul(FS.value(a), v(k)), e2, NA.mul_comm(v(k), FS.value(a)))
183  Equal.trans(Nat, Nat.mod(FS.value(F.mul_small(a, k)), 1n+pp), Nat.mod(FS.value(F.scal(k, a)), 1n+pp), Nat.mod(Nat.mul(FS.value(a), v(k)), 1n+pp), e1, M.cong_mod(1n+pp, FS.value(F.scal(k, a)), Nat.mul(FS.value(a), v(k)), e3))