proofs/crypto/ed25519/scalar.bend

bend-collections-laws-crypto@1.0.0.0 · 185 lines · 19 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/src/crypto/curve25519/field.bend as F
6import bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/x25519.bend as X
7import bend-collections-laws-crypto@1.0.0.0/src/crypto/ed25519/scalar.bend as ESC
8import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
9import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
10import bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend as WD
11import bend-collections-laws-crypto@1.0.0.0/proofs/lib/arith.bend as AR
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/math/typed/width.bend as WI
16import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend as M
17import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend as LM
18import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/poly.bend as PL
19import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/fold.bend as FD
20import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/reduce.bend as RD
21import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/consts.bend as K
22import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/fieldops.bend as FO
23import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/freeze.bend as FZ
24import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/cong.bend as G
25import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/xbits.bend as XB
26
27# Scalars mod a modulus M = 1 + mm below 2^255 (L for Ed25519) as tight
28# 32-limb values: the conditional subtraction (adding 2^256 - M carries out
29# exactly when x >= M), addm, the double-and-add loop mac, reduce and
30# mul_add of src/crypto/ed25519/scalar.bend. The constant cp = 2^256 - M is
31# a parameter, related to M through the symbolic one.
32
33def v(+x: U32) -> Nat:
34  U32.to_nat(x)
35
36def T(+one: Nat) -> Nat:
37  LM.shn(32n, one)
38
39# ---- x + cp, carried ----
40
41def ad_okb(+one: Nat, +h1: {one == 1n : Nat}, +x: List<&2, U32>, +cp: List<&2, U32>, +hx: {LM.okb(32n, x, 255n) == True{} : Bool}, +hk: {LM.okb(32n, cp, 255n) == True{} : Bool}) -> {LM.okb(32n, F.addl(x, cp), WD.sc(28n, one)) == True{} : Bool}:
42  FO.addl_okb(one, h1, x, cp, hx, hk)
43
44def cvx(+one: Nat, +h1: {one == 1n : Nat}, +mm: Nat, +x: List<&2, U32>, +cp: List<&2, U32>, +hx: {LM.okb(32n, x, 255n) == True{} : Bool}, +hk: {LM.okb(32n, cp, 255n) == True{} : Bool}) -> {Nat.add(FS.value(LM.cl(F.carry(F.addl(x, cp), 0))), LM.shn(32n, v(LM.cc(F.carry(F.addl(x, cp), 0))))) == Nat.add(FS.value(x), FS.value(cp)) : Nat}:
45  +ys = F.addl(x, cp)
46  Equal.trans(Nat, Nat.add(FS.value(LM.cl(F.carry(ys, 0))), LM.shn(32n, v(LM.cc(F.carry(ys, 0))))), FS.value(ys), Nat.add(FS.value(x), FS.value(cp)), FD.cr_val(one, h1, ys, ad_okb(one, h1, x, cp, hx, hk)), PL.addl_val(one, h1, x, cp, 255n, 255n, LM.okb_lea(32n, x, 255n, hx), LM.okb_lea(32n, cp, 255n, hk), FO.lt32_small(one, h1, Nat.add(255n, 255n), {==})))
47
48def cp_val(+one: Nat, +h1: {one == 1n : Nat}, +mm: Nat, +cp: List<&2, U32>, +hv: {Nat.add(K.valo(one, cp), 1n+mm) == T(one) : Nat}) -> {Nat.add(FS.value(cp), 1n+mm) == T(one) : Nat}:
49  Equal.trans(Nat, Nat.add(FS.value(cp), 1n+mm), Nat.add(K.valo(one, cp), 1n+mm), T(one), M.cong_l(FS.value(cp), K.valo(one, cp), 1n+mm, Equal.sym(Nat, K.valo(one, cp), FS.value(cp), K.valo_value(one, h1, cp))), hv)
50
51# case c < 1: x < M
52def mz(+one: Nat, +h1: {one == 1n : Nat}, +mm: Nat, +x: List<&2, U32>, +cp: List<&2, U32>, +hx: {LM.okb(32n, x, 255n) == True{} : Bool}, +hk: {LM.okb(32n, cp, 255n) == True{} : Bool}, +hv: {Nat.add(K.valo(one, cp), 1n+mm) == T(one) : Nat}, +hc: {Nat.is_lt(v(LM.cc(F.carry(F.addl(x, cp), 0))), one) == True{} : Bool}) -> {Nat.is_lt(FS.value(x), 1n+mm) == True{} : Bool}:
53  +r = F.carry(F.addl(x, cp), 0)
54  +c = v(LM.cc(r))
55  +vs = FS.value(LM.cl(r))
56  +VC = FS.value(cp)
57  +c0 = U.lt_one_zero(c, L.subst(Nat, o => {Nat.is_lt(c, o) == True{} : Bool}, one, 1n, h1, hc))
58  +ev = L.subst(Nat, z => {Nat.add(vs, LM.shn(32n, z)) == Nat.add(FS.value(x), VC) : Nat}, c, 0n, c0, cvx(one, h1, mm, x, cp, hx, hk))
59  +ev1 = Equal.trans(Nat, vs, Nat.add(vs, 0n), Nat.add(FS.value(x), VC), Equal.sym(Nat, Nat.add(vs, 0n), vs, N.add_zero(vs)), ev)
60  +lt = RD.val_lt(one, h1, 32n, LM.cl(r), FD.cr_okb(one, h1, F.addl(x, cp), ad_okb(one, h1, x, cp, hx, hk)))
61  +lt2 = L.subst(Nat, z => {Nat.is_lt(vs, z) == True{} : Bool}, T(one), Nat.add(VC, 1n+mm), Equal.sym(Nat, Nat.add(VC, 1n+mm), T(one), cp_val(one, h1, mm, cp, hv)), lt)
62  +lt3 = L.subst(Nat, z => {Nat.is_lt(z, Nat.add(VC, 1n+mm)) == True{} : Bool}, vs, Nat.add(FS.value(x), VC), ev1, lt2)
63  +lt4 = L.subst(Nat, z => {Nat.is_lt(Nat.add(FS.value(x), VC), z) == True{} : Bool}, Nat.add(VC, 1n+mm), Nat.add(1n+mm, VC), NA.add_comm(VC, 1n+mm), lt3)
64  RD.lt_cancel_r(FS.value(x), 1n+mm, VC, lt4)
65
66# case c >= 1 (x < 2^256): c == 1
67def mo_c(+one: Nat, +h1: {one == 1n : Nat}, +mm: Nat, +x: List<&2, U32>, +cp: List<&2, U32>, +hx: {LM.okb(32n, x, 255n) == True{} : Bool}, +hk: {LM.okb(32n, cp, 255n) == True{} : Bool}, +hv: {Nat.add(K.valo(one, cp), 1n+mm) == T(one) : Nat}, +hc: {Nat.is_lt(v(LM.cc(F.carry(F.addl(x, cp), 0))), one) == False{} : Bool}) -> {v(LM.cc(F.carry(F.addl(x, cp), 0))) == one : Nat}:
68  +r = F.carry(F.addl(x, cp), 0)
69  +c = v(LM.cc(r))
70  +vs = FS.value(LM.cl(r))
71  +VC = FS.value(cp)
72  +TT = T(one)
73  +ev = cvx(one, h1, mm, x, cp, hx, hk)
74  +a = N.le_trans(LM.shn(32n, c), Nat.add(vs, LM.shn(32n, c)), Nat.add(FS.value(x), VC), PL.le_add_l(vs, LM.shn(32n, c)), N.eq_le(Nat.add(vs, LM.shn(32n, c)), Nat.add(FS.value(x), VC), ev))
75  +vct = L.subst(Nat, z => {Nat.is_le(VC, z) == True{} : Bool}, Nat.add(VC, 1n+mm), TT, cp_val(one, h1, mm, cp, hv), N.le_add_right(VC, 1n+mm))
76  +b = N.lt_le_trans(Nat.add(FS.value(x), VC), Nat.add(TT, VC), Nat.add(TT, TT), N.lt_add_r2(FS.value(x), TT, VC, RD.val_lt(one, h1, 32n, x, hx)), N.le_add_left(VC, TT, TT, vct))
77  +d = N.le_lt_trans(LM.shn(32n, c), Nat.add(FS.value(x), VC), Nat.add(TT, TT), a, b)
78  +d2 = L.subst(Nat, z => {Nat.is_lt(LM.shn(32n, c), z) == True{} : Bool}, Nat.add(TT, TT), LM.shn(32n, Nat.add(one, one)), M.sc_add(256n, one, one), d)
79  +c2 = RD.shn_lt_cancel(c, Nat.add(one, one), d2)
80  +c2b = L.subst(Nat, o => {Nat.is_lt(c, Nat.add(o, o)) == True{} : Bool}, one, 1n, h1, c2)
81  +cle = L.subst(Nat, o => {Nat.is_le(c, o) == True{} : Bool}, 1n, one, Equal.sym(Nat, one, 1n, h1), N.lt_succ_le(c, 1n, c2b))
82  N.le_antisym(c, one, cle, N.not_lt_le(c, one, hc))
83
84# case c >= 1: value(s) + M == value(x)
85def mo(+one: Nat, +h1: {one == 1n : Nat}, +mm: Nat, +x: List<&2, U32>, +cp: List<&2, U32>, +hx: {LM.okb(32n, x, 255n) == True{} : Bool}, +hk: {LM.okb(32n, cp, 255n) == True{} : Bool}, +hv: {Nat.add(K.valo(one, cp), 1n+mm) == T(one) : Nat}, +hc: {Nat.is_lt(v(LM.cc(F.carry(F.addl(x, cp), 0))), one) == False{} : Bool}) -> {Nat.add(FS.value(LM.cl(F.carry(F.addl(x, cp), 0))), 1n+mm) == FS.value(x) : Nat}:
86  +r = F.carry(F.addl(x, cp), 0)
87  +c = v(LM.cc(r))
88  +vs = FS.value(LM.cl(r))
89  +VC = FS.value(cp)
90  +ev = L.subst(Nat, z => {Nat.add(vs, LM.shn(32n, z)) == Nat.add(FS.value(x), VC) : Nat}, c, one, mo_c(one, h1, mm, x, cp, hx, hk, hv, hc), cvx(one, h1, mm, x, cp, hx, hk))
91  +ev2 = L.subst(Nat, z => {Nat.add(vs, z) == Nat.add(FS.value(x), VC) : Nat}, T(one), Nat.add(VC, 1n+mm), Equal.sym(Nat, Nat.add(VC, 1n+mm), T(one), cp_val(one, h1, mm, cp, hv)), ev)
92  +ev3 = Equal.trans(Nat, Nat.add(Nat.add(vs, 1n+mm), VC), Nat.add(vs, Nat.add(VC, 1n+mm)), Nat.add(FS.value(x), VC), Equal.trans(Nat, Nat.add(Nat.add(vs, 1n+mm), VC), Nat.add(vs, Nat.add(1n+mm, VC)), Nat.add(vs, Nat.add(VC, 1n+mm)), NA.add_assoc(vs, 1n+mm, VC), M.cong_r(vs, Nat.add(1n+mm, VC), Nat.add(VC, 1n+mm), NA.add_comm(1n+mm, VC))), ev2)
93  G.cancel_r(Nat.add(vs, 1n+mm), FS.value(x), VC, ev3)
94
95def cs_mz(+one: Nat, +h1: {one == 1n : Nat}, +x: List<&2, U32>, +cp: List<&2, U32>, +hx: {LM.okb(32n, x, 255n) == True{} : Bool}, +hk: {LM.okb(32n, cp, 255n) == True{} : Bool}, +hc: {Nat.is_lt(v(LM.cc(F.carry(F.addl(x, cp), 0))), one) == True{} : Bool}) -> {FZ.csg(x, cp) == x : List<&2, U32>}:
96  +r = F.carry(F.addl(x, cp), 0)
97  +c0 = U.lt_one_zero(v(LM.cc(r)), L.subst(Nat, o => {Nat.is_lt(v(LM.cc(r)), o) == True{} : Bool}, one, 1n, h1, hc))
98  +cz = U.injective(LM.cc(r), 0, c0)
99  %Equal.sym(List<&2, U32>, F.csub_fin(r, x), F.select(LM.cc(r), x, LM.cl(r)), FZ.cs_eta(r, x)) : {_ == x : List<&2, U32>}
100  %Equal.cong(U32, List<&2, U32>, z => F.select(z, x, LM.cl(r)), 0, LM.cc(r), Equal.sym(U32, LM.cc(r), 0, cz)) : {_ == x : List<&2, U32>}
101  FO.select0(one, h1, 32n, x, LM.cl(r), hx, FD.cr_okb(one, h1, F.addl(x, cp), ad_okb(one, h1, x, cp, hx, hk)))
102
103def cs_mo(+one: Nat, +h1: {one == 1n : Nat}, +mm: Nat, +x: List<&2, U32>, +cp: List<&2, U32>, +hx: {LM.okb(32n, x, 255n) == True{} : Bool}, +hk: {LM.okb(32n, cp, 255n) == True{} : Bool}, +hv: {Nat.add(K.valo(one, cp), 1n+mm) == T(one) : Nat}, +hc: {Nat.is_lt(v(LM.cc(F.carry(F.addl(x, cp), 0))), one) == False{} : Bool}) -> {FZ.csg(x, cp) == LM.cl(F.carry(F.addl(x, cp), 0)) : List<&2, U32>}:
104  +r = F.carry(F.addl(x, cp), 0)
105  +co = U.injective(LM.cc(r), 1, Equal.trans(Nat, v(LM.cc(r)), one, 1n, mo_c(one, h1, mm, x, cp, hx, hk, hv, hc), h1))
106  %Equal.sym(List<&2, U32>, F.csub_fin(r, x), F.select(LM.cc(r), x, LM.cl(r)), FZ.cs_eta(r, x)) : {_ == LM.cl(r) : List<&2, U32>}
107  %Equal.cong(U32, List<&2, U32>, z => F.select(z, x, LM.cl(r)), 1, LM.cc(r), Equal.sym(U32, LM.cc(r), 1, co)) : {_ == LM.cl(r) : List<&2, U32>}
108  FO.select1(one, h1, 32n, x, LM.cl(r), hx, FD.cr_okb(one, h1, F.addl(x, cp), ad_okb(one, h1, x, cp, hx, hk)))
109
110# ---- csub: tight, and value(x) mod M for x < 2 M ----
111
112def cs_okb_by(+one: Nat, +h1: {one == 1n : Nat}, +mm: Nat, +x: List<&2, U32>, +cp: List<&2, U32>, +hx: {LM.okb(32n, x, 255n) == True{} : Bool}, +hk: {LM.okb(32n, cp, 255n) == True{} : Bool}, +hv: {Nat.add(K.valo(one, cp), 1n+mm) == T(one) : Nat}, +b: Bool, +hb: {Nat.is_lt(v(LM.cc(F.carry(F.addl(x, cp), 0))), one) == b : Bool}) -> {LM.okb(32n, FZ.csg(x, cp), 255n) == True{} : Bool}:
113  match b:
114    case True{}:
115      %Equal.sym(List<&2, U32>, FZ.csg(x, cp), x, cs_mz(one, h1, x, cp, hx, hk, hb)) : {LM.okb(32n, _, 255n) == True{} : Bool}
116      hx
117    case False{}:
118      %Equal.sym(List<&2, U32>, FZ.csg(x, cp), LM.cl(F.carry(F.addl(x, cp), 0)), cs_mo(one, h1, mm, x, cp, hx, hk, hv, hb)) : {LM.okb(32n, _, 255n) == True{} : Bool}
119      FD.cr_okb(one, h1, F.addl(x, cp), ad_okb(one, h1, x, cp, hx, hk))
120
121def cs_val_by(+one: Nat, +h1: {one == 1n : Nat}, +mm: Nat, +x: List<&2, U32>, +cp: List<&2, U32>, +hx: {LM.okb(32n, x, 255n) == True{} : Bool}, +hk: {LM.okb(32n, cp, 255n) == True{} : Bool}, +hv: {Nat.add(K.valo(one, cp), 1n+mm) == T(one) : Nat}, +h2m: {Nat.is_lt(FS.value(x), Nat.add(1n+mm, 1n+mm)) == True{} : Bool}, +b: Bool, +hb: {Nat.is_lt(v(LM.cc(F.carry(F.addl(x, cp), 0))), one) == b : Bool}) -> {FS.value(FZ.csg(x, cp)) == Nat.mod(FS.value(x), 1n+mm) : Nat}:
122  match b:
123    case True{}:
124      %Equal.sym(List<&2, U32>, FZ.csg(x, cp), x, cs_mz(one, h1, x, cp, hx, hk, hb)) : {FS.value(_) == Nat.mod(FS.value(x), 1n+mm) : Nat}
125      Equal.sym(Nat, Nat.mod(FS.value(x), 1n+mm), FS.value(x), NR.mod_of(0n, mm, FS.value(x), mz(one, h1, mm, x, cp, hx, hk, hv, hb)))
126    case False{}:
127      +s = LM.cl(F.carry(F.addl(x, cp), 0))
128      %Equal.sym(List<&2, U32>, FZ.csg(x, cp), s, cs_mo(one, h1, mm, x, cp, hx, hk, hv, hb)) : {FS.value(_) == Nat.mod(FS.value(x), 1n+mm) : Nat}
129      +e1 = mo(one, h1, mm, x, cp, hx, hk, hv, hb)
130      +l1 = L.subst(Nat, z => {Nat.is_lt(z, Nat.add(1n+mm, 1n+mm)) == True{} : Bool}, FS.value(x), Nat.add(FS.value(s), 1n+mm), Equal.sym(Nat, Nat.add(FS.value(s), 1n+mm), FS.value(x), e1), h2m)
131      +sl = RD.lt_cancel_r(FS.value(s), 1n+mm, 1n+mm, l1)
132      +e2 = Equal.trans(Nat, FS.value(x), Nat.add(FS.value(s), 1n+mm), Nat.add(Nat.mul(1n, 1n+mm), FS.value(s)), Equal.sym(Nat, Nat.add(FS.value(s), 1n+mm), FS.value(x), e1), Equal.trans(Nat, Nat.add(FS.value(s), 1n+mm), Nat.add(1n+mm, FS.value(s)), Nat.add(Nat.mul(1n, 1n+mm), FS.value(s)), NA.add_comm(FS.value(s), 1n+mm), M.cong_l(1n+mm, Nat.mul(1n, 1n+mm), FS.value(s), Equal.sym(Nat, Nat.mul(1n, 1n+mm), 1n+mm, AR.one_mul(1n+mm)))))
133      Equal.sym(Nat, Nat.mod(FS.value(x), 1n+mm), FS.value(s), Equal.trans(Nat, Nat.mod(FS.value(x), 1n+mm), Nat.mod(Nat.add(Nat.mul(1n, 1n+mm), FS.value(s)), 1n+mm), FS.value(s), M.cong_mod(1n+mm, FS.value(x), Nat.add(Nat.mul(1n, 1n+mm), FS.value(s)), e2), NR.mod_of(1n, mm, FS.value(s), sl)))
134
135# x < M exactly when the carry is 0
136def lt_by(+one: Nat, +h1: {one == 1n : Nat}, +mm: Nat, +x: List<&2, U32>, +cp: List<&2, U32>, +hx: {LM.okb(32n, x, 255n) == True{} : Bool}, +hk: {LM.okb(32n, cp, 255n) == True{} : Bool}, +hv: {Nat.add(K.valo(one, cp), 1n+mm) == T(one) : Nat}, +b: Bool, +hb: {Nat.is_lt(v(LM.cc(F.carry(F.addl(x, cp), 0))), one) == b : Bool}) -> {U32.is_eq(LM.cc(F.carry(F.addl(x, cp), 0)), 0) == Nat.is_lt(FS.value(x), 1n+mm) : Bool}:
137  match b:
138    case True{}:
139      +r = F.carry(F.addl(x, cp), 0)
140      +c0 = U.lt_one_zero(v(LM.cc(r)), L.subst(Nat, o => {Nat.is_lt(v(LM.cc(r)), o) == True{} : Bool}, one, 1n, h1, hb))
141      +cz = U.injective(LM.cc(r), 0, c0)
142      %Equal.sym(U32, LM.cc(r), 0, cz) : {U32.is_eq(_, 0) == Nat.is_lt(FS.value(x), 1n+mm) : Bool}
143      Equal.sym(Bool, Nat.is_lt(FS.value(x), 1n+mm), True{}, mz(one, h1, mm, x, cp, hx, hk, hv, hb))
144    case False{}:
145      +r = F.carry(F.addl(x, cp), 0)
146      +co = U.injective(LM.cc(r), 1, Equal.trans(Nat, v(LM.cc(r)), one, 1n, mo_c(one, h1, mm, x, cp, hx, hk, hv, hb), h1))
147      %Equal.sym(U32, LM.cc(r), 1, co) : {U32.is_eq(_, 0) == Nat.is_lt(FS.value(x), 1n+mm) : Bool}
148      +e1 = mo(one, h1, mm, x, cp, hx, hk, hv, hb)
149      +ge = L.subst(Nat, z => {Nat.is_le(1n+mm, z) == True{} : Bool}, Nat.add(FS.value(LM.cl(r)), 1n+mm), FS.value(x), e1, PL.le_add_l(FS.value(LM.cl(r)), 1n+mm))
150      Equal.sym(Bool, Nat.is_lt(FS.value(x), 1n+mm), False{}, N.le_not_lt(FS.value(x), 1n+mm, ge))
151
152# ---- addm ----
153
154def sum_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.cr_limbs(F.carry(F.addl(a, b), 0)), 255n) == True{} : Bool}:
155  FD.cr_okb(one, h1, F.addl(a, b), FO.addl_okb(one, h1, a, b, ha, hb))
156
157# a + b < 2 M <= 2^256: no carry out, the limbs hold a + b
158def sum_val(+one: Nat, +h1: {one == 1n : Nat}, +mm: Nat, +h2: {Nat.is_le(Nat.add(1n+mm, 1n+mm), T(one)) == True{} : Bool}, +a: List<&2, U32>, +b: List<&2, U32>, +ha: {LM.okb(32n, a, 255n) == True{} : Bool}, +hb: {LM.okb(32n, b, 255n) == True{} : Bool}, +la: {Nat.is_lt(FS.value(a), 1n+mm) == True{} : Bool}, +lb: {Nat.is_lt(FS.value(b), 1n+mm) == True{} : Bool}) -> {FS.value(F.cr_limbs(F.carry(F.addl(a, b), 0))) == Nat.add(FS.value(a), FS.value(b)) : Nat}:
159  +ys = F.addl(a, b)
160  +r = F.carry(ys, 0)
161  +V = Nat.add(FS.value(a), FS.value(b))
162  +hyo = FO.addl_okb(one, h1, a, b, ha, hb)
163  +ev = Equal.trans(Nat, Nat.add(FS.value(LM.cl(r)), LM.shn(32n, v(LM.cc(r)))), FS.value(ys), V, FD.cr_val(one, h1, ys, hyo), PL.addl_val(one, h1, a, b, 255n, 255n, LM.okb_lea(32n, a, 255n, ha), LM.okb_lea(32n, b, 255n, hb), FO.lt32_small(one, h1, Nat.add(255n, 255n), {==})))
164  +l2 = N.lt_le_trans(V, Nat.add(1n+mm, 1n+mm), T(one), N.lt_le_trans(V, Nat.add(1n+mm, FS.value(b)), Nat.add(1n+mm, 1n+mm), N.lt_add_r2(FS.value(a), 1n+mm, FS.value(b), la), N.lt_le(Nat.add(1n+mm, FS.value(b)), Nat.add(1n+mm, 1n+mm), N.lt_add_left(FS.value(b), 1n+mm, 1n+mm, lb))), h2)
165  +z = RD.last_zero(one, h1, FS.value(LM.cl(r)), v(LM.cc(r)), V, ev, l2, Nat.is_lt(v(LM.cc(r)), one), {==})
166  +ev0 = L.subst(Nat, w => {Nat.add(FS.value(LM.cl(r)), LM.shn(32n, w)) == V : Nat}, v(LM.cc(r)), 0n, z, ev)
167  Equal.trans(Nat, FS.value(LM.cl(r)), Nat.add(FS.value(LM.cl(r)), 0n), V, Equal.sym(Nat, Nat.add(FS.value(LM.cl(r)), 0n), FS.value(LM.cl(r)), N.add_zero(FS.value(LM.cl(r)))), ev0)
168
169# addm with its constant as a parameter
170def addg(+a: List<&2, U32>, +b: List<&2, U32>, +cp: List<&2, U32>) -> List<&2, U32>:
171  FZ.csg(F.cr_limbs(F.carry(F.addl(a, b), 0)), cp)
172
173def addg_okb(+one: Nat, +h1: {one == 1n : Nat}, +mm: Nat, +cp: List<&2, U32>, +hk: {LM.okb(32n, cp, 255n) == True{} : Bool}, +hv: {Nat.add(K.valo(one, cp), 1n+mm) == T(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}) -> {LM.okb(32n, addg(a, b, cp), 255n) == True{} : Bool}:
174  +s = F.cr_limbs(F.carry(F.addl(a, b), 0))
175  cs_okb_by(one, h1, mm, s, cp, sum_okb(one, h1, a, b, ha, hb), hk, hv, Nat.is_lt(v(LM.cc(F.carry(F.addl(s, cp), 0))), one), {==})
176
177def addg_val(+one: Nat, +h1: {one == 1n : Nat}, +mm: Nat, +h2: {Nat.is_le(Nat.add(1n+mm, 1n+mm), T(one)) == True{} : Bool}, +cp: List<&2, U32>, +hk: {LM.okb(32n, cp, 255n) == True{} : Bool}, +hv: {Nat.add(K.valo(one, cp), 1n+mm) == T(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}, +la: {Nat.is_lt(FS.value(a), 1n+mm) == True{} : Bool}, +lb: {Nat.is_lt(FS.value(b), 1n+mm) == True{} : Bool}) -> {FS.value(addg(a, b, cp)) == Nat.mod(Nat.add(FS.value(a), FS.value(b)), 1n+mm) : Nat}:
178  +s = F.cr_limbs(F.carry(F.addl(a, b), 0))
179  +es = sum_val(one, h1, mm, h2, a, b, ha, hb, la, lb)
180  +h2m = L.subst(Nat, z => {Nat.is_lt(z, Nat.add(1n+mm, 1n+mm)) == True{} : Bool}, Nat.add(FS.value(a), FS.value(b)), FS.value(s), Equal.sym(Nat, FS.value(s), Nat.add(FS.value(a), FS.value(b)), es), N.lt_le_trans(Nat.add(FS.value(a), FS.value(b)), Nat.add(1n+mm, FS.value(b)), Nat.add(1n+mm, 1n+mm), N.lt_add_r2(FS.value(a), 1n+mm, FS.value(b), la), N.lt_le(Nat.add(1n+mm, FS.value(b)), Nat.add(1n+mm, 1n+mm), N.lt_add_left(FS.value(b), 1n+mm, 1n+mm, lb))))
181  +e1 = cs_val_by(one, h1, mm, s, cp, sum_okb(one, h1, a, b, ha, hb), hk, hv, h2m, Nat.is_lt(v(LM.cc(F.carry(F.addl(s, cp), 0))), one), {==})
182  Equal.trans(Nat, FS.value(addg(a, b, cp)), Nat.mod(FS.value(s), 1n+mm), Nat.mod(Nat.add(FS.value(a), FS.value(b)), 1n+mm), e1, M.cong_mod(1n+mm, FS.value(s), Nat.add(FS.value(a), FS.value(b)), es))
183
184def lt_mod(+mm: Nat, +x: Nat) -> {Nat.is_lt(Nat.mod(x, 1n+mm), 1n+mm) == True{} : Bool}:
185  NR.dm_lt(mm, x)