~/bend-docscommunity

proofs/crypto/ed25519/scalar2.bend source

proofs/crypto/ed25519/scalar2.bend on the hub · documented module

import Baseimport ../../../spec/lib/common.bend as Cimport ../../../spec/crypto/curve25519/field.bend as FSimport ../../../spec/crypto/curve25519/x25519.bend as SXimport ../../../src/crypto/curve25519/field.bend as Fimport ../../../src/crypto/curve25519/x25519.bend as Ximport ../../../src/crypto/ed25519/scalar.bend as ESCimport ../../lib/nat.bend as Nimport ../../lib/logic.bend as Limport ../../lib/word.bend as WDimport ../../lib/arith.bend as ARimport ../../lib/u32.bend as Uimport ../../lib/u32alg.bend as Aimport ../../lib/lemmas/proofs/nat_algebra.bend as NAimport ../../math/natural/arith.bend as NRimport ../../math/typed/width.bend as WIimport ../curve25519/num.bend as Mimport ../curve25519/limbs.bend as LMimport ../curve25519/consts.bend as Kimport ../curve25519/fieldops.bend as FOimport ../curve25519/cong.bend as Gimport ../curve25519/xbits.bend as XBimport ./scalar.bend as SC# The double-and-add loop over the bits of a byte string (mac), reduce and# mul_add of src/crypto/ed25519/scalar.bend, for a modulus M = 1 + mm with# the constant cp = 2^256 - M as a parameter:#   value(mac(n, bs, s, acc)) == (2^n acc + (bs mod 2^n) s) mod Mdef v(+x: U32) -> Nat:  U32.to_nat(x)def shift_sc(+k: Nat, +x: Nat) -> {C.shift(k, x) == WD.sc(k, x) : Nat}:  match k:    case 0n:      {==}    case 1n+ +p:      Equal.cong(Nat, Nat, t => Nat.double(t), C.shift(p, x), WD.sc(p, x), shift_sc(p, x))# bit t joins the low t bitsdef 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}:  match t:    case 0n:      N.add_zero(C.bit(V))    case 1n+ +q:      +hV = C.half(V)      +lo = C.low(q, hV)      +S = WD.sc(q, C.bit(C.high(q, hV)))      +ih = low_step(q, hV)      +e1 = Equal.cong(Nat, Nat, z => Nat.add(C.bit(V), Nat.double(z)), C.low(1n+q, hV), Nat.add(lo, S), ih)      +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))      +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)))      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))# a byte string's value fits its bit countdef byte_fits(+bs: List<&2, U32>, +hb: {LM.lea(bs, 255n) == True{} : Bool}) -> {C.high(X.bitlen(bs), FS.value(bs)) == 0n : Nat}:  match bs:    case Nil{}:      {==}    case Con{+b, +bt}:      +V = FS.value(bt)      +hbl = N.le_lt_succ(v(b), 255n, LM.lea_head(b, bt, 255n, hb))      +e1 = WI.high_comp(X.bitlen(bt), 8n, Nat.add(v(b), C.shift(8n, V)))      +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))      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)))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}:  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)))# ---- mac with its constant as a parameter ----def macg(n: Nat, +bs: List<&2, U32>, +s: List<&2, U32>, +acc: List<&2, U32>, +cp: List<&2, U32>) -> List<&2, U32>:  match n:    case 0n:      acc    case 1n+ +t:      +a2 = SC.addg(acc, acc, cp)      macg(t, bs, s, SC.addg(a2, F.select(X.kbit(bs, t), F.zero(), s), cp), cp)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>}:  match n:    case 0n:      {==}    case 1n+ +t:      mac_eq(t, bs, s, ESC.addm(ESC.addm(acc, acc), F.select(X.kbit(bs, t), F.zero(), s)))# the selected addend: bit * sdef 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}:  match b:    case 0n:      %Equal.sym(U32, kb, 0, XB.u0(kb, hk)) : {LM.okb(32n, F.select(_, F.zero(), s), 255n) == True{} : Bool}      %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}      {==}    case 1n:      %Equal.sym(U32, kb, 1, XB.u1(kb, hk)) : {LM.okb(32n, F.select(_, F.zero(), s), 255n) == True{} : Bool}      %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}      hs    case 2n+q:      Empty.absurd({LM.okb(32n, F.select(kb, F.zero(), s), 255n) == True{} : Bool}, L.false_true(hb))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}:  match b:    case 0n:      %Equal.sym(U32, kb, 0, XB.u0(kb, hk)) : {FS.value(F.select(_, F.zero(), s)) == 0n : Nat}      %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}      {==}    case 1n:      %Equal.sym(U32, kb, 1, XB.u1(kb, hk)) : {FS.value(F.select(_, F.zero(), s)) == Nat.mul(1n, FS.value(s)) : Nat}      %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}      Equal.sym(Nat, Nat.mul(1n, FS.value(s)), FS.value(s), AR.one_mul(FS.value(s)))    case 2n+q:      Empty.absurd({FS.value(F.select(kb, F.zero(), s)) == Nat.mul(2n+q, FS.value(s)) : Nat}, L.false_true(hb))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}:  match b:    case 0n:      {==}    case 1n:      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)    case 2n+q:      Empty.absurd({Nat.is_lt(Nat.mul(2n+q, S), 1n+mm) == True{} : Bool}, L.false_true(hb))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}:  match n:    case 0n:      ha    case 1n+ +t:      +a2 = SC.addg(acc, acc, cp)      +o2 = SC.addg_okb(one, h1, mm, cp, hk, hv, acc, acc, ha, ha)      +sel = F.select(X.kbit(bs, t), F.zero(), s)      +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)      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))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)))):  match n:    case 0n:      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))))    case 1n+ +t:      +P = {1n+mm : Nat}      +V = FS.value(bs)      +S = FS.value(s)      +AA = FS.value(acc)      +bt = SX.kbit(V, t)      +a2 = SC.addg(acc, acc, cp)      +o2 = SC.addg_okb(one, h1, mm, cp, hk, hv, acc, acc, ha, ha)      +v2 = SC.addg_val(one, h1, mm, h2, cp, hk, hv, acc, acc, ha, ha, la, la)      +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)))      +sel = F.select(X.kbit(bs, t), F.zero(), s)      +hkv = XB.kbit_val(bs, t, hbs)      +hkb = XB.kbit_le(bs, t, hbs)      +os = sel_okb(one, h1, X.kbit(bs, t), bt, hkv, hkb, s, hs)      +vs = sel_val(one, h1, X.kbit(bs, t), bt, hkv, hkb, s, hs)      +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))      +acc2 = SC.addg(a2, sel, cp)      +o3 = SC.addg_okb(one, h1, mm, cp, hk, hv, a2, sel, o2, os)      +v3 = SC.addg_val(one, h1, mm, h2, cp, hk, hv, a2, sel, o2, os, l2, lsel)      +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))))      +W = Nat.add(Nat.add(AA, AA), Nat.mul(bt, S))      +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)))      +ih = mac_lt(one, h1, mm, h2, cp, hk, hv, t, bs, s, acc2, hbs, hs, ls, o3, l3)      +lo = C.low(t, V)      # sc(t, acc2) == sc(t, W) mod M      +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))))      +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)))      # sc(t, 2A + b S) + lo S == sc(1+t, A) + low(1+t) S      +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)))      +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))      +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)))))))      +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)      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)))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}:  match n:    case 0n:      la    case 1n+ +t:      +a2 = SC.addg(acc, acc, cp)      +o2 = SC.addg_okb(one, h1, mm, cp, hk, hv, acc, acc, ha, ha)      +v2 = SC.addg_val(one, h1, mm, h2, cp, hk, hv, acc, acc, ha, ha, la, la)      +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))))      +bt = SX.kbit(FS.value(bs), t)      +sel = F.select(X.kbit(bs, t), F.zero(), s)      +hkv = XB.kbit_val(bs, t, hbs)      +hkb = XB.kbit_le(bs, t, hbs)      +os = sel_okb(one, h1, X.kbit(bs, t), bt, hkv, hkb, s, hs)      +vs = sel_val(one, h1, X.kbit(bs, t), bt, hkv, hkb, s, hs)      +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))      +acc2 = SC.addg(a2, sel, cp)      +v3 = SC.addg_val(one, h1, mm, h2, cp, hk, hv, a2, sel, o2, os, l2, lsel)      +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))))      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)# the exact value: the loop result is reduceddef 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}:  +r = FS.value(macg(n, bs, s, acc, cp))  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))