def mac_eq

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

import Base
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/src/crypto/ed25519/scalar.bend as ESC

80def mac_eq(+n: Nat, +bs: List<&2, U32>, +s: List<&2, U32>, +acc: List<&2, U32>) -> {ESC.mac(n, bs, s, acc) == macg(n, bs, s, acc, ESC.comp_l()) : List<&2, U32>}:
81  match n:
82    case 0n:
83      {==}
84    case 1n+ +t:
85      mac_eq(t, bs, s, ESC.addm(ESC.addm(acc, acc), F.select(X.kbit(bs, t), F.zero(), s)))