law wadc.m

lawful-words@0.1.0.0 · proof_u32.bend:39

import Base
import lawful-words@0.1.0.0/proof_nat.bend as N
import lawful-words@0.1.0.0/proof_word.bend as W

39law wadc.m:
40  for +x: Word(32n)
41  for +y: Word(32n)
42  for +c: Bool
43  for +m: Nat
44  for +hm: {Nat.pow(2n, 32n) == m : Nat}
45  {Nat.add(Word.to_nat(32n, Word.adc(32n, x, y, False{}, c)), Nat.mul(N.bn(W.cout(32n, x, y, c)), m))
46    == Nat.add(N.bn(c), Nat.add(Word.to_nat(32n, x), Word.to_nat(32n, y))) : Nat}