def w_add_sub

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/u32alg.bend:201

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32.bend as U

201# (v - a) + a == v
202def w_add_sub(+n: Nat, +a: Word(n), +b: Word(n)) -> {Word.sub(n, Word.add(n, a, b), a) == b : Word(n)}:
203  +ux = uw(n, Word.add(n, a, b))
204  +ua = uw(n, a)
205  +ub = uw(n, b)
206  +un = uw(n, Word.not(n, a))
207  +r = uw(n, Word.sub(n, Word.add(n, a, b), a))
208  +c1 = cy(n, a, b, False{})
209  +c5 = cy(n, Word.add(n, a, b), Word.not(n, a), True{})
210  +e2 = cons(n, a, b)
211  +e5 = cons_sub(n, Word.add(n, a, b), a)
212  +nv = not_value(n, a)
213  # r + sc(c5 + c1) == ub + sc(1)
214  +chain = Equal.trans(Nat, Nat.add(r, sc(n, Nat.add(c5, c1))), Nat.add(Nat.add(r, sc(n, c5)), sc(n, c1)), Nat.add(ub, sc(n, 1n)),
215    %sc_add(n, c5, c1) : {Nat.add(r, _) == Nat.add(Nat.add(r, sc(n, c5)), sc(n, c1)) : Nat}
216    Equal.sym(Nat, Nat.add(Nat.add(r, sc(n, c5)), sc(n, c1)), Nat.add(r, Nat.add(sc(n, c5), sc(n, c1))), N.add_assoc(r, sc(n, c5), sc(n, c1))),
217    %Equal.sym(Nat, Nat.add(r, sc(n, c5)), Nat.add(1n, Nat.add(ux, un)), e5) : {Nat.add(_, sc(n, c1)) == Nat.add(ub, sc(n, 1n)) : Nat}
218    %nv : {Nat.add(Nat.add(1n, Nat.add(ux, un)), sc(n, c1)) == Nat.add(ub, _) : Nat}
219    arith_sub(ux, un, ua, ub, sc(n, c1), e2))
220  w_inj(n, Word.sub(n, Word.add(n, a, b), a), b, uniq(n, r, ub, Nat.add(c5, c1), 1n, chain, U.WB_unsigned(n, Word.sub(n, Word.add(n, a, b), a)), U.WB_unsigned(n, b)))