Scalar2.mac_lt: def of bend-collections-laws-crypto@1.0.0.0 Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/scalar2.bend as Scalar2 Lines 134-170 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/scalar2.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/scalar2.bend&start_line=134&end_line=170 import Base import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C import bend-collections-laws-crypto@1.0.0.0/spec/crypto/curve25519/field.bend as FS import bend-collections-laws-crypto@1.0.0.0/spec/crypto/curve25519/x25519.bend as SX import bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/field.bend as F import bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/x25519.bend as X import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L import bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend as WD import bend-collections-laws-crypto@1.0.0.0/proofs/lib/arith.bend as AR import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend as M import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend as LM import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/consts.bend as K import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/cong.bend as G import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/xbits.bend as XB import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/scalar.bend as SC 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))) Uses (53): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mod https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/cong.bend&name=c_add https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/cong.bend&name=c_eq https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/cong.bend&name=c_mod https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/cong.bend&name=c_mul https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/cong.bend&name=c_refl https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/cong.bend&name=c_trans https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/cong.bend&name=ceq https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/consts.bend&name=valo https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend&name=lea https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend&name=okb https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend&name=cong_add https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend&name=cong_l https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend&name=cong_r https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend&name=sc_add https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend&name=sc_dbl https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/xbits.bend&name=kbit_le https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/xbits.bend&name=kbit_val https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/scalar2.bend&name=low_step https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/scalar2.bend&name=macg https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/scalar2.bend&name=sel_lt https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/scalar2.bend&name=sel_okb https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/scalar2.bend&name=sel_val https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/scalar.bend&name=T https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/scalar.bend&name=addg https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/scalar.bend&name=addg_okb https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/scalar.bend&name=addg_val https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/scalar.bend&name=lt_mod https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/arith.bend&name=mul_sc https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/arith.bend&name=sc_mul https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=add_assoc https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=add_comm https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=mul_add_right https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend&name=subst https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=add_zero https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend&name=sc https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/curve25519/field.bend&name=value https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/curve25519/x25519.bend&name=kbit https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=low https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/field.bend&name=select https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/field.bend&name=zero https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/x25519.bend&name=kbit