1 import Base 2 import ../../../spec/lib/common.bend as C 3 import ../../../spec/crypto/curve25519/field.bend as FS 4 import ../../../spec/crypto/curve25519/x25519.bend as SX 5 import ../../../src/crypto/curve25519/field.bend as F 6 import ../../../src/crypto/curve25519/x25519.bend as X 7 import ../../../src/crypto/ed25519/scalar.bend as ESC 8 import ../../lib/nat.bend as N 9 import ../../lib/logic.bend as L 10 import ../../lib/word.bend as WD 11 import ../../lib/arith.bend as AR 12 import ../../lib/u32.bend as U 13 import ../../lib/u32alg.bend as A 14 import ../../lib/lemmas/proofs/nat_algebra.bend as NA 15 import ../../math/natural/arith.bend as NR 16 import ../../math/typed/width.bend as WI 17 import ../curve25519/num.bend as M 18 import ../curve25519/limbs.bend as LM 19 import ../curve25519/consts.bend as K 20 import ../curve25519/fieldops.bend as FO 21 import ../curve25519/cong.bend as G 22 import ../curve25519/xbits.bend as XB 23 import ./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 30 def v(+x: U32) -> Nat: 31 U32.to_nat(x) 32 33 def 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 41 def 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 56 def 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 67 def 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 72 def 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 80 def 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 88 def 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 101 def 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 114 def 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 123 def 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 134 def 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 172 def 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 194 def 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))