law step_alg

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/poly1305/poly.bend:25

import Base

25# (r (a + n)) X == a (r X) + n (r X)
26law step_alg:
27  for +r: Nat
28  for +a: Nat
29  for +n: Nat
30  for +x: Nat
31  for +p: Nat
32  {Nat.add(Nat.mul(Nat.mul(r, Nat.add(a, n)), x), p) == Nat.add(Nat.mul(a, Nat.mul(r, x)), Nat.add(Nat.mul(n, Nat.mul(r, x)), p)) : Nat}