def next_mod

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

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as NR

69def next_mod(+bp: Nat, +r: Nat, +x: Nat, +n: Nat) -> {Nat.mod(Nat.mul(r, Nat.add(Nat.mod(x, 1n+bp), n)), 1n+bp) == Nat.mod(Nat.mul(r, Nat.add(x, n)), 1n+bp) : Nat}:
70  +m = {1n+bp : Nat}
71  Equal.trans(Nat, Nat.mod(Nat.mul(r, Nat.add(Nat.mod(x, m), n)), m), Nat.mod(Nat.mul(r, Nat.mod(Nat.add(Nat.mod(x, m), n), m)), m), Nat.mod(Nat.mul(r, Nat.add(x, n)), m),
72    Equal.sym(Nat, Nat.mod(Nat.mul(r, Nat.mod(Nat.add(Nat.mod(x, m), n), m)), m), Nat.mod(Nat.mul(r, Nat.add(Nat.mod(x, m), n)), m), NR.mod_mul_r(bp, r, Nat.add(Nat.mod(x, m), n))),
73    Equal.trans(Nat, Nat.mod(Nat.mul(r, Nat.mod(Nat.add(Nat.mod(x, m), n), m)), m), Nat.mod(Nat.mul(r, Nat.mod(Nat.add(x, n), m)), m), Nat.mod(Nat.mul(r, Nat.add(x, n)), m),
74      Equal.cong(Nat, Nat, z => Nat.mod(Nat.mul(r, z), m), Nat.mod(Nat.add(Nat.mod(x, m), n), m), Nat.mod(Nat.add(x, n), m), NR.mod_add_l(bp, x, n)),
75      NR.mod_mul_r(bp, r, Nat.add(x, n))))