law scale_le

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

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

137law scale_le:
138  for +c: U32
139  for +a: List<&2, U32>
140  for +b: Nat
141  for +bc: Nat
142  for +ha: {le_all(a, b) == True{} : Bool}
143  for +hc: {Nat.is_le(v(c), bc) == True{} : Bool}
144  for +hf: {C.fits(32n, Nat.mul(b, bc)) == True{} : Bool}
145  {le_all(Li.scale(c, a), Nat.mul(b, bc)) == True{} : Bool}