law carry_top

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

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

423# the top limb fits 9 + j bits
424law carry_top:
425  for +n: Nat
426  for +ds: List<&2, U32>
427  for +u: U32
428  for +j: Nat
429  for +hj: {Nat.is_le(Nat.add(9n, j), 32n) == True{} : Bool}
430  for +hd: {fit_all(ds, Nat.add(8n, j)) == True{} : Bool}
431  for +hu: {C.fits(Nat.add(8n, j), v(u)) == True{} : Bool}
432  {C.fits(Nat.add(9n, j), v(Li.hd0(Li.skip(n, Li.carry(n, ds, u))))) == True{} : Bool}