Scalar2.mac_val: 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 193-196 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=193&end_line=196

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

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

Uses (22):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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/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/ed25519/scalar2.bend&name=mac_below
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/scalar2.bend&name=mac_lt
  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/scalar.bend&name=T
  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/proofs/math/natural/arith.bend&name=mod_of
  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/lib/common.bend&name=low