law wmul.m

lawful-words@0.1.0.0 · proof_u32.bend:86

import Base

86law wmul.m:
87  for +x: Word(32n)
88  for +y: Word(32n)
89  for +m: Nat
90  for +hm: {Nat.pow(2n, 32n) == m : Nat}
91  {Word.to_nat(32n, Word.mul.go(32n, 32n, x, y, Word.zero(32n)))
92    == Nat.mod(Nat.add(Word.to_nat(32n, Word.zero(32n)), Nat.mul(Word.to_nat(32n, x), Word.to_nat(32n, y))), m) : Nat}