law carry_ev

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

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

352# A carry pass over n limbs keeps the value: carry(n, ds, u) + 2^(8(n+1)) ds[n+1..] == u + ds.
353law carry_ev:
354  for +n: Nat
355  for +ds: List<&2, U32>
356  for +u: U32
357  for +j: Nat
358  for +hj: {Nat.is_le(Nat.add(9n, j), 32n) == True{} : Bool}
359  for +hd: {fit_all(ds, Nat.add(8n, j)) == True{} : Bool}
360  for +hu: {C.fits(Nat.add(8n, j), v(u)) == True{} : Bool}
361  {Nat.add(ev(Li.carry(n, ds, u)), pos(1n+n, ev(Li.skip(1n+n, ds)))) == Nat.add(v(u), ev(ds)) : Nat}