law scale_ev

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

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

114law scale_ev:
115  for +c: U32
116  for +a: List<&2, U32>
117  for +b: Nat
118  for +bc: Nat
119  for +ha: {le_all(a, b) == True{} : Bool}
120  for +hc: {Nat.is_le(v(c), bc) == True{} : Bool}
121  for +hf: {C.fits(32n, Nat.mul(b, bc)) == True{} : Bool}
122  {ev(Li.scale(c, a)) == Nat.mul(ev(a), v(c)) : Nat}