law rg

lawful-bytes@0.1.1.0 · proof_fast_w2.bend:190

import Base
import lawful-words@0.1.0.0/defs.bend as W

190# rep(c) == pack4(c, c, c, c), as numbers with 2^32, 2^8, 2^16, 2^24 abstract.
191law rg:
192  for +c: U32
193  for +M: Nat
194  for +A: Nat
195  for +B: Nat
196  for +E: Nat
197  for +h1: {U32.to_nat(U32.mul(c, W.pack4(1, 1, 1, 1))) == Nat.mod(Nat.mul(U32.to_nat(c), U32.to_nat(W.pack4(1, 1, 1, 1))), M) : Nat}
198  for +h2: {U32.to_nat(W.pack4(1, 1, 1, 1)) == Nat.add(U32.to_nat(1), Nat.add(Nat.mul(U32.to_nat(1), A), Nat.add(Nat.mul(U32.to_nat(1), B), Nat.mul(U32.to_nat(1), E)))) : Nat}
199  for +h3: {U32.to_nat(W.pack4(c, c, c, c)) == Nat.add(U32.to_nat(c), Nat.add(Nat.mul(U32.to_nat(c), A), Nat.add(Nat.mul(U32.to_nat(c), B), Nat.mul(U32.to_nat(c), E)))) : Nat}
200  for +h4: {Nat.is_lt(U32.to_nat(W.pack4(c, c, c, c)), M) == True{} : Bool}
201  {U32.to_nat(U32.mul(c, W.pack4(1, 1, 1, 1))) == U32.to_nat(W.pack4(c, c, c, c)) : Nat}