law sq_ev
bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/poly1305/value.bend:456
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/value.bend as Value
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/src/crypto/poly1305/limbs.bend as Li
456law sq_ev:
457 for +n: Nat
458 for +xs: List<&2, U32>
459 {Nat.add(Nat.add(ev(Li.split(n, xs)), pos(n, C.shift(2n, v(Li.quot(n, xs))))), pos(1n+n, ev(Li.skip(1n+n, xs)))) == ev(xs) : Nat}