def mac_below

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

import Base
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/logic.bend as L
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/xbits.bend as XB
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/scalar.bend as SC

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)