law mul_le

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

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

158law mul_le:
159  for +x: List<&2, U32>
160  for +r: List<&2, U32>
161  for +bx: Nat
162  for +br: Nat
163  for +hx: {le_all(x, bx) == True{} : Bool}
164  for +hr: {le_all(r, br) == True{} : Bool}
165  for +hf: {C.fits(32n, Nat.mul(List.length(&2, U32, r), Nat.mul(bx, br))) == True{} : Bool}
166  {le_all(Li.mul(x, r), Nat.mul(List.length(&2, U32, r), Nat.mul(bx, br))) == True{} : Bool}