~/jendhub

proofs/crypto/ed25519/scalar2.bend

bend-collections-laws-crypto@1.0.0.0 · 196 lines · 14 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/u32alg.bend as A
14import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
15import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as NR
16import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend as WI
17import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend as M
18import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend as LM
19import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/consts.bend as K
20import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/fieldops.bend as FO
21import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/cong.bend as G
22import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/xbits.bend as XB
23import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/scalar.bend as SC
24
25# The double-and-add loop over the bits of a byte string (mac), reduce and
26# mul_add of src/crypto/ed25519/scalar.bend, for a modulus M = 1 + mm with
27# the constant cp = 2^256 - M as a parameter:
28#   value(mac(n, bs, s, acc)) == (2^n acc + (bs mod 2^n) s) mod M
29
30def v(+x: U32) -> Nat:
31  U32.to_nat(x)
32
33def shift_sc(+k: Nat, +x: Nat) -> {C.shift(k, x) == WD.sc(k, x) : Nat}:
34  match k:
35    case 0n:
36      {==}
37    case 1n+ +p:
38      Equal.cong(Nat, Nat, t => Nat.double(t), C.shift(p, x), WD.sc(p, x), shift_sc(p, x))
39
40# bit t joins the low t bits
41def low_step(+t: Nat, +V: Nat) -> {C.low(1n+t, V) == Nat.add(C.low(t, V), WD.sc(t, C.bit(C.high(t, V)))) : Nat}:
42  match t:
43    case 0n:
44      N.add_zero(C.bit(V))
45    case 1n+ +q:
46      +hV = C.half(V)
47      +lo = C.low(q, hV)
48      +S = WD.sc(q, C.bit(C.high(q, hV)))
49      +ih = low_step(q, hV)
50      +e1 = Equal.cong(Nat, Nat, z => Nat.add(C.bit(V), Nat.double(z)), C.low(1n+q, hV), Nat.add(lo, S), ih)
51      +e2 = M.cong_r(C.bit(V), Nat.double(Nat.add(lo, S)), Nat.add(Nat.double(lo), Nat.double(S)), NA.double_add(lo, S))
52      +e3 = Equal.sym(Nat, Nat.add(Nat.add(C.bit(V), Nat.double(lo)), Nat.double(S)), Nat.add(C.bit(V), Nat.add(Nat.double(lo), Nat.double(S))), NA.add_assoc(C.bit(V), Nat.double(lo), Nat.double(S)))
53      Equal.trans(Nat, Nat.add(C.bit(V), Nat.double(C.low(1n+q, hV))), Nat.add(C.bit(V), Nat.double(Nat.add(lo, S))), Nat.add(Nat.add(C.bit(V), Nat.double(lo)), Nat.double(S)), e1, Equal.trans(Nat, Nat.add(C.bit(V), Nat.double(Nat.add(lo, S))), Nat.add(C.bit(V), Nat.add(Nat.double(lo), Nat.double(S))), Nat.add(Nat.add(C.bit(V), Nat.double(lo)), Nat.double(S)), e2, e3))
54
55# a byte string's value fits its bit count
56def byte_fits(+bs: List<&2, U32>, +hb: {LM.lea(bs, 255n) == True{} : Bool}) -> {C.high(X.bitlen(bs), FS.value(bs)) == 0n : Nat}:
57  match bs:
58    case Nil{}:
59      {==}
60    case Con{+b, +bt}:
61      +V = FS.value(bt)
62      +hbl = N.le_lt_succ(v(b), 255n, LM.lea_head(b, bt, 255n, hb))
63      +e1 = WI.high_comp(X.bitlen(bt), 8n, Nat.add(v(b), C.shift(8n, V)))
64      +e2 = Equal.cong(Nat, Nat, z => C.high(X.bitlen(bt), z), C.high(8n, Nat.add(v(b), C.shift(8n, V))), V, WI.high_uniq(8n, v(b), V, hbl))
65      Equal.trans(Nat, C.high(Nat.add(8n, X.bitlen(bt)), Nat.add(v(b), C.shift(8n, V))), C.high(X.bitlen(bt), V), 0n, Equal.trans(Nat, C.high(Nat.add(8n, X.bitlen(bt)), Nat.add(v(b), C.shift(8n, V))), C.high(X.bitlen(bt), C.high(8n, Nat.add(v(b), C.shift(8n, V)))), C.high(X.bitlen(bt), V), e1, e2), byte_fits(bt, LM.lea_tail(b, bt, 255n, hb)))
66
67def low_all(+bs: List<&2, U32>, +hb: {LM.lea(bs, 255n) == True{} : Bool}) -> {C.low(X.bitlen(bs), FS.value(bs)) == FS.value(bs) : Nat}:
68  WI.low_fit(X.bitlen(bs), FS.value(bs), Equal.cong(Nat, Bool, z => Nat.is_eq(z, 0n), C.high(X.bitlen(bs), FS.value(bs)), 0n, byte_fits(bs, hb)))
69
70# ---- mac with its constant as a parameter ----
71
72def macg(n: Nat, +bs: List<&2, U32>, +s: List<&2, U32>, +acc: List<&2, U32>, +cp: List<&2, U32>) -> List<&2, U32>:
73  match n:
74    case 0n:
75      acc
76    case 1n+ +t:
77      +a2 = SC.addg(acc, acc, cp)
78      macg(t, bs, s, SC.addg(a2, F.select(X.kbit(bs, t), F.zero(), s), cp), cp)
79
80def mac_eq(+n: Nat, +bs: List<&2, U32>, +s: List<&2, U32>, +acc: List<&2, U32>) -> {ESC.mac(n, bs, s, acc) == macg(n, bs, s, acc, ESC.comp_l()) : List<&2, U32>}:
81  match n:
82    case 0n:
83      {==}
84    case 1n+ +t:
85      mac_eq(t, bs, s, ESC.addm(ESC.addm(acc, acc), F.select(X.kbit(bs, t), F.zero(), s)))
86
87# the selected addend: bit * s
88def sel_okb(+one: Nat, +h1: {one == 1n : Nat}, +kb: U32, +b: Nat, +hk: {v(kb) == b : Nat}, +hb: {Nat.is_le(b, 1n) == True{} : Bool}, +s: List<&2, U32>, +hs: {LM.okb(32n, s, 255n) == True{} : Bool}) -> {LM.okb(32n, F.select(kb, F.zero(), s), 255n) == True{} : Bool}:
89  match b:
90    case 0n:
91      %Equal.sym(U32, kb, 0, XB.u0(kb, hk)) : {LM.okb(32n, F.select(_, F.zero(), s), 255n) == True{} : Bool}
92      %Equal.sym(List<&2, U32>, F.select(0, F.zero(), s), F.zero(), FO.select0(one, h1, 32n, F.zero(), s, {==}, hs)) : {LM.okb(32n, _, 255n) == True{} : Bool}
93      {==}
94    case 1n:
95      %Equal.sym(U32, kb, 1, XB.u1(kb, hk)) : {LM.okb(32n, F.select(_, F.zero(), s), 255n) == True{} : Bool}
96      %Equal.sym(List<&2, U32>, F.select(1, F.zero(), s), s, FO.select1(one, h1, 32n, F.zero(), s, {==}, hs)) : {LM.okb(32n, _, 255n) == True{} : Bool}
97      hs
98    case 2n+q:
99      Empty.absurd({LM.okb(32n, F.select(kb, F.zero(), s), 255n) == True{} : Bool}, L.false_true(hb))
100
101def sel_val(+one: Nat, +h1: {one == 1n : Nat}, +kb: U32, +b: Nat, +hk: {v(kb) == b : Nat}, +hb: {Nat.is_le(b, 1n) == True{} : Bool}, +s: List<&2, U32>, +hs: {LM.okb(32n, s, 255n) == True{} : Bool}) -> {FS.value(F.select(kb, F.zero(), s)) == Nat.mul(b, FS.value(s)) : Nat}:
102  match b:
103    case 0n:
104      %Equal.sym(U32, kb, 0, XB.u0(kb, hk)) : {FS.value(F.select(_, F.zero(), s)) == 0n : Nat}
105      %Equal.sym(List<&2, U32>, F.select(0, F.zero(), s), F.zero(), FO.select0(one, h1, 32n, F.zero(), s, {==}, hs)) : {FS.value(_) == 0n : Nat}
106      {==}
107    case 1n:
108      %Equal.sym(U32, kb, 1, XB.u1(kb, hk)) : {FS.value(F.select(_, F.zero(), s)) == Nat.mul(1n, FS.value(s)) : Nat}
109      %Equal.sym(List<&2, U32>, F.select(1, F.zero(), s), s, FO.select1(one, h1, 32n, F.zero(), s, {==}, hs)) : {FS.value(_) == Nat.mul(1n, FS.value(s)) : Nat}
110      Equal.sym(Nat, Nat.mul(1n, FS.value(s)), FS.value(s), AR.one_mul(FS.value(s)))
111    case 2n+q:
112      Empty.absurd({FS.value(F.select(kb, F.zero(), s)) == Nat.mul(2n+q, FS.value(s)) : Nat}, L.false_true(hb))
113
114def sel_lt(+mm: Nat, +b: Nat, +S: Nat, +hb: {Nat.is_le(b, 1n) == True{} : Bool}, +ls: {Nat.is_lt(S, 1n+mm) == True{} : Bool}) -> {Nat.is_lt(Nat.mul(b, S), 1n+mm) == True{} : Bool}:
115  match b:
116    case 0n:
117      {==}
118    case 1n:
119      L.subst(Nat, z => {Nat.is_lt(z, 1n+mm) == True{} : Bool}, S, Nat.mul(1n, S), Equal.sym(Nat, Nat.mul(1n, S), S, AR.one_mul(S)), ls)
120    case 2n+q:
121      Empty.absurd({Nat.is_lt(Nat.mul(2n+q, S), 1n+mm) == True{} : Bool}, L.false_true(hb))
122
123def mac_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) == SC.T(one) : Nat}, +n: Nat, +bs: List<&2, U32>, +s: List<&2, U32>, +acc: List<&2, U32>, +hbs: {LM.lea(bs, 255n) == True{} : Bool}, +hs: {LM.okb(32n, s, 255n) == True{} : Bool}, +ha: {LM.okb(32n, acc, 255n) == True{} : Bool}) -> {LM.okb(32n, macg(n, bs, s, acc, cp), 255n) == True{} : Bool}:
124  match n:
125    case 0n:
126      ha
127    case 1n+ +t:
128      +a2 = SC.addg(acc, acc, cp)
129      +o2 = SC.addg_okb(one, h1, mm, cp, hk, hv, acc, acc, ha, ha)
130      +sel = F.select(X.kbit(bs, t), F.zero(), s)
131      +os = sel_okb(one, h1, X.kbit(bs, t), SX.kbit(FS.value(bs), t), XB.kbit_val(bs, t, hbs), XB.kbit_le(bs, t, hbs), s, hs)
132      mac_okb(one, h1, mm, cp, hk, hv, t, bs, s, SC.addg(a2, sel, cp), hbs, hs, SC.addg_okb(one, h1, mm, cp, hk, hv, a2, sel, o2, os))
133
134def mac_lt(+one: Nat, +h1: {one == 1n : Nat}, +mm: Nat, +h2: {Nat.is_le(Nat.add(1n+mm, 1n+mm), SC.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) == SC.T(one) : Nat}, +n: Nat, +bs: List<&2, U32>, +s: List<&2, U32>, +acc: List<&2, U32>, +hbs: {LM.lea(bs, 255n) == True{} : Bool}, +hs: {LM.okb(32n, s, 255n) == True{} : Bool}, +ls: {Nat.is_lt(FS.value(s), 1n+mm) == True{} : Bool}, +ha: {LM.okb(32n, acc, 255n) == True{} : Bool}, +la: {Nat.is_lt(FS.value(acc), 1n+mm) == True{} : Bool}) -> G.ceq(mm, FS.value(macg(n, bs, s, acc, cp)), Nat.add(WD.sc(n, FS.value(acc)), Nat.mul(C.low(n, FS.value(bs)), FS.value(s)))):
135  match n:
136    case 0n:
137      G.c_eq(mm, FS.value(acc), Nat.add(FS.value(acc), Nat.mul(0n, FS.value(s))), Equal.sym(Nat, Nat.add(FS.value(acc), 0n), FS.value(acc), N.add_zero(FS.value(acc))))
138    case 1n+ +t:
139      +P = {1n+mm : Nat}
140      +V = FS.value(bs)
141      +S = FS.value(s)
142      +AA = FS.value(acc)
143      +bt = SX.kbit(V, t)
144      +a2 = SC.addg(acc, acc, cp)
145      +o2 = SC.addg_okb(one, h1, mm, cp, hk, hv, acc, acc, ha, ha)
146      +v2 = SC.addg_val(one, h1, mm, h2, cp, hk, hv, acc, acc, ha, ha, la, la)
147      +l2 = L.subst(Nat, z => {Nat.is_lt(z, P) == True{} : Bool}, Nat.mod(Nat.add(AA, AA), P), FS.value(a2), Equal.sym(Nat, FS.value(a2), Nat.mod(Nat.add(AA, AA), P), v2), SC.lt_mod(mm, Nat.add(AA, AA)))
148      +sel = F.select(X.kbit(bs, t), F.zero(), s)
149      +hkv = XB.kbit_val(bs, t, hbs)
150      +hkb = XB.kbit_le(bs, t, hbs)
151      +os = sel_okb(one, h1, X.kbit(bs, t), bt, hkv, hkb, s, hs)
152      +vs = sel_val(one, h1, X.kbit(bs, t), bt, hkv, hkb, s, hs)
153      +lsel = L.subst(Nat, z => {Nat.is_lt(z, P) == True{} : Bool}, Nat.mul(bt, S), FS.value(sel), Equal.sym(Nat, FS.value(sel), Nat.mul(bt, S), vs), sel_lt(mm, bt, S, hkb, ls))
154      +acc2 = SC.addg(a2, sel, cp)
155      +o3 = SC.addg_okb(one, h1, mm, cp, hk, hv, a2, sel, o2, os)
156      +v3 = SC.addg_val(one, h1, mm, h2, cp, hk, hv, a2, sel, o2, os, l2, lsel)
157      +l3 = L.subst(Nat, z => {Nat.is_lt(z, P) == True{} : Bool}, Nat.mod(Nat.add(FS.value(a2), FS.value(sel)), P), FS.value(acc2), Equal.sym(Nat, FS.value(acc2), Nat.mod(Nat.add(FS.value(a2), FS.value(sel)), P), v3), SC.lt_mod(mm, Nat.add(FS.value(a2), FS.value(sel))))
158      +W = Nat.add(Nat.add(AA, AA), Nat.mul(bt, S))
159      +c3 = G.c_trans(mm, FS.value(acc2), Nat.add(FS.value(a2), FS.value(sel)), W, G.c_trans(mm, FS.value(acc2), Nat.mod(Nat.add(FS.value(a2), FS.value(sel)), P), Nat.add(FS.value(a2), FS.value(sel)), G.c_eq(mm, FS.value(acc2), Nat.mod(Nat.add(FS.value(a2), FS.value(sel)), P), v3), G.c_mod(mm, Nat.add(FS.value(a2), FS.value(sel)))), G.c_add(mm, FS.value(a2), Nat.add(AA, AA), FS.value(sel), Nat.mul(bt, S), G.c_trans(mm, FS.value(a2), Nat.mod(Nat.add(AA, AA), P), Nat.add(AA, AA), G.c_eq(mm, FS.value(a2), Nat.mod(Nat.add(AA, AA), P), v2), G.c_mod(mm, Nat.add(AA, AA))), G.c_eq(mm, FS.value(sel), Nat.mul(bt, S), vs)))
160      +ih = mac_lt(one, h1, mm, h2, cp, hk, hv, t, bs, s, acc2, hbs, hs, ls, o3, l3)
161      +lo = C.low(t, V)
162      # sc(t, acc2) == sc(t, W) mod M
163      +c4 = G.c_trans(mm, WD.sc(t, FS.value(acc2)), Nat.mul(FS.value(acc2), WD.sc(t, 1n)), WD.sc(t, W), G.c_eq(mm, WD.sc(t, FS.value(acc2)), Nat.mul(FS.value(acc2), WD.sc(t, 1n)), Equal.sym(Nat, Nat.mul(FS.value(acc2), WD.sc(t, 1n)), WD.sc(t, FS.value(acc2)), AR.mul_sc(t, FS.value(acc2)))), G.c_trans(mm, Nat.mul(FS.value(acc2), WD.sc(t, 1n)), Nat.mul(W, WD.sc(t, 1n)), WD.sc(t, W), G.c_mul(mm, FS.value(acc2), W, WD.sc(t, 1n), WD.sc(t, 1n), c3, G.c_refl(mm, WD.sc(t, 1n))), G.c_eq(mm, Nat.mul(W, WD.sc(t, 1n)), WD.sc(t, W), AR.mul_sc(t, W))))
164      +c5 = G.c_add(mm, WD.sc(t, FS.value(acc2)), WD.sc(t, W), Nat.mul(lo, S), Nat.mul(lo, S), c4, G.c_refl(mm, Nat.mul(lo, S)))
165      # sc(t, 2A + b S) + lo S == sc(1+t, A) + low(1+t) S
166      +f1 = Equal.sym(Nat, Nat.add(WD.sc(t, Nat.add(AA, AA)), WD.sc(t, Nat.mul(bt, S))), WD.sc(t, W), M.sc_add(t, Nat.add(AA, AA), Nat.mul(bt, S)))
167      +f2 = M.cong_add(WD.sc(t, Nat.add(AA, AA)), WD.sc(1n+t, AA), WD.sc(t, Nat.mul(bt, S)), Nat.mul(WD.sc(t, bt), S), Equal.trans(Nat, WD.sc(t, Nat.add(AA, AA)), Nat.add(WD.sc(t, AA), WD.sc(t, AA)), WD.sc(1n+t, AA), Equal.sym(Nat, Nat.add(WD.sc(t, AA), WD.sc(t, AA)), WD.sc(t, Nat.add(AA, AA)), M.sc_add(t, AA, AA)), M.sc_dbl(t, AA)), AR.sc_mul(t, bt, S))
168      +f3 = Equal.trans(Nat, Nat.add(Nat.add(WD.sc(1n+t, AA), Nat.mul(WD.sc(t, bt), S)), Nat.mul(lo, S)), Nat.add(WD.sc(1n+t, AA), Nat.add(Nat.mul(WD.sc(t, bt), S), Nat.mul(lo, S))), Nat.add(WD.sc(1n+t, AA), Nat.mul(C.low(1n+t, V), S)), NA.add_assoc(WD.sc(1n+t, AA), Nat.mul(WD.sc(t, bt), S), Nat.mul(lo, S)), M.cong_r(WD.sc(1n+t, AA), Nat.add(Nat.mul(WD.sc(t, bt), S), Nat.mul(lo, S)), Nat.mul(C.low(1n+t, V), S), Equal.trans(Nat, Nat.add(Nat.mul(WD.sc(t, bt), S), Nat.mul(lo, S)), Nat.mul(Nat.add(WD.sc(t, bt), lo), S), Nat.mul(C.low(1n+t, V), S), Equal.sym(Nat, Nat.mul(Nat.add(WD.sc(t, bt), lo), S), Nat.add(Nat.mul(WD.sc(t, bt), S), Nat.mul(lo, S)), NA.mul_add_right(WD.sc(t, bt), lo, S)), Equal.cong(Nat, Nat, z => Nat.mul(z, S), Nat.add(WD.sc(t, bt), lo), C.low(1n+t, V), Equal.trans(Nat, Nat.add(WD.sc(t, bt), lo), Nat.add(lo, WD.sc(t, bt)), C.low(1n+t, V), NA.add_comm(WD.sc(t, bt), lo), Equal.sym(Nat, C.low(1n+t, V), Nat.add(lo, WD.sc(t, bt)), low_step(t, V)))))))
169      +f = Equal.trans(Nat, Nat.add(WD.sc(t, W), Nat.mul(lo, S)), Nat.add(Nat.add(WD.sc(1n+t, AA), Nat.mul(WD.sc(t, bt), S)), Nat.mul(lo, S)), Nat.add(WD.sc(1n+t, AA), Nat.mul(C.low(1n+t, V), S)), M.cong_l(WD.sc(t, W), Nat.add(WD.sc(1n+t, AA), Nat.mul(WD.sc(t, bt), S)), Nat.mul(lo, S), Equal.trans(Nat, WD.sc(t, W), Nat.add(WD.sc(t, Nat.add(AA, AA)), WD.sc(t, Nat.mul(bt, S))), Nat.add(WD.sc(1n+t, AA), Nat.mul(WD.sc(t, bt), S)), f1, f2)), f3)
170      G.c_trans(mm, FS.value(macg(t, bs, s, acc2, cp)), Nat.add(WD.sc(t, FS.value(acc2)), Nat.mul(lo, S)), Nat.add(WD.sc(1n+t, AA), Nat.mul(C.low(1n+t, V), S)), ih, G.c_trans(mm, Nat.add(WD.sc(t, FS.value(acc2)), Nat.mul(lo, S)), Nat.add(WD.sc(t, W), Nat.mul(lo, S)), Nat.add(WD.sc(1n+t, AA), Nat.mul(C.low(1n+t, V), S)), c5, G.c_eq(mm, Nat.add(WD.sc(t, W), Nat.mul(lo, S)), Nat.add(WD.sc(1n+t, AA), Nat.mul(C.low(1n+t, V), S)), f)))
171
172def mac_below(+one: Nat, +h1: {one == 1n : Nat}, +mm: Nat, +h2: {Nat.is_le(Nat.add(1n+mm, 1n+mm), SC.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) == SC.T(one) : Nat}, +n: Nat, +bs: List<&2, U32>, +s: List<&2, U32>, +acc: List<&2, U32>, +hbs: {LM.lea(bs, 255n) == True{} : Bool}, +hs: {LM.okb(32n, s, 255n) == True{} : Bool}, +ls: {Nat.is_lt(FS.value(s), 1n+mm) == True{} : Bool}, +ha: {LM.okb(32n, acc, 255n) == True{} : Bool}, +la: {Nat.is_lt(FS.value(acc), 1n+mm) == True{} : Bool}) -> {Nat.is_lt(FS.value(macg(n, bs, s, acc, cp)), 1n+mm) == True{} : Bool}:
173  match n:
174    case 0n:
175      la
176    case 1n+ +t:
177      +a2 = SC.addg(acc, acc, cp)
178      +o2 = SC.addg_okb(one, h1, mm, cp, hk, hv, acc, acc, ha, ha)
179      +v2 = SC.addg_val(one, h1, mm, h2, cp, hk, hv, acc, acc, ha, ha, la, la)
180      +l2 = L.subst(Nat, z => {Nat.is_lt(z, 1n+mm) == True{} : Bool}, Nat.mod(Nat.add(FS.value(acc), FS.value(acc)), 1n+mm), FS.value(a2), Equal.sym(Nat, FS.value(a2), Nat.mod(Nat.add(FS.value(acc), FS.value(acc)), 1n+mm), v2), SC.lt_mod(mm, Nat.add(FS.value(acc), FS.value(acc))))
181      +bt = SX.kbit(FS.value(bs), t)
182      +sel = F.select(X.kbit(bs, t), F.zero(), s)
183      +hkv = XB.kbit_val(bs, t, hbs)
184      +hkb = XB.kbit_le(bs, t, hbs)
185      +os = sel_okb(one, h1, X.kbit(bs, t), bt, hkv, hkb, s, hs)
186      +vs = sel_val(one, h1, X.kbit(bs, t), bt, hkv, hkb, s, hs)
187      +lsel = L.subst(Nat, z => {Nat.is_lt(z, 1n+mm) == True{} : Bool}, Nat.mul(bt, FS.value(s)), FS.value(sel), Equal.sym(Nat, FS.value(sel), Nat.mul(bt, FS.value(s)), vs), sel_lt(mm, bt, FS.value(s), hkb, ls))
188      +acc2 = SC.addg(a2, sel, cp)
189      +v3 = SC.addg_val(one, h1, mm, h2, cp, hk, hv, a2, sel, o2, os, l2, lsel)
190      +l3 = L.subst(Nat, z => {Nat.is_lt(z, 1n+mm) == True{} : Bool}, Nat.mod(Nat.add(FS.value(a2), FS.value(sel)), 1n+mm), FS.value(acc2), Equal.sym(Nat, FS.value(acc2), Nat.mod(Nat.add(FS.value(a2), FS.value(sel)), 1n+mm), v3), SC.lt_mod(mm, Nat.add(FS.value(a2), FS.value(sel))))
191      mac_below(one, h1, mm, h2, cp, hk, hv, t, bs, s, acc2, hbs, hs, ls, SC.addg_okb(one, h1, mm, cp, hk, hv, a2, sel, o2, os), l3)
192
193# the exact value: the loop result is reduced
194def mac_val(+one: Nat, +h1: {one == 1n : Nat}, +mm: Nat, +h2: {Nat.is_le(Nat.add(1n+mm, 1n+mm), SC.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) == SC.T(one) : Nat}, +n: Nat, +bs: List<&2, U32>, +s: List<&2, U32>, +acc: List<&2, U32>, +hbs: {LM.lea(bs, 255n) == True{} : Bool}, +hs: {LM.okb(32n, s, 255n) == True{} : Bool}, +ls: {Nat.is_lt(FS.value(s), 1n+mm) == True{} : Bool}, +ha: {LM.okb(32n, acc, 255n) == True{} : Bool}, +la: {Nat.is_lt(FS.value(acc), 1n+mm) == True{} : Bool}) -> {FS.value(macg(n, bs, s, acc, cp)) == Nat.mod(Nat.add(WD.sc(n, FS.value(acc)), Nat.mul(C.low(n, FS.value(bs)), FS.value(s))), 1n+mm) : Nat}:
195  +r = FS.value(macg(n, bs, s, acc, cp))
196  Equal.trans(Nat, r, Nat.mod(r, 1n+mm), Nat.mod(Nat.add(WD.sc(n, FS.value(acc)), Nat.mul(C.low(n, FS.value(bs)), FS.value(s))), 1n+mm), Equal.sym(Nat, Nat.mod(r, 1n+mm), r, NR.mod_of(0n, mm, r, mac_below(one, h1, mm, h2, cp, hk, hv, n, bs, s, acc, hbs, hs, ls, ha, la))), mac_lt(one, h1, mm, h2, cp, hk, hv, n, bs, s, acc, hbs, hs, ls, ha, la))