law ts_ev

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/poly1305/value.bend:253

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/poly1305/limbs.bend as Li

253# ev(xs) = ev(take n xs) + 2^(8n) ev(skip n xs)
254law ts_ev:
255  for +n: Nat
256  for +xs: List<&2, U32>
257  {ev(xs) == Nat.add(ev(Li.take(n, xs)), pos(n, ev(Li.skip(n, xs)))) : Nat}