~/jendhub

def mac_lt

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/ed25519/scalar2.bend:134

import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/scalar2.bend as Scalar2
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

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)))

Uses (53)

Used by (1)