law ev_lt

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

import Base

657# limbs of 8 bits: the value is below 2^(8 len)
658law ev_lt:
659  for +xs: List<&2, U32>
660  for +one: Nat
661  for +h1: {one == 1n : Nat}
662  for +h: {fit_all(xs, 8n) == True{} : Bool}
663  {Nat.is_lt(ev(xs), pos(len(xs), one)) == True{} : Bool}