def mac_val

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

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/proofs/lib/word.bend as WD
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as NR
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/ed25519/scalar.bend as SC

193# the exact value: the loop result is reduced
194def 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))