def w_assoc

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

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

116def w_assoc(+n: Nat, +a: Word(n), +b: Word(n), +c: Word(n)) -> {Word.add(n, Word.add(n, a, b), c) == Word.add(n, a, Word.add(n, b, c)) : Word(n)}:
117  -s = Word.add(n, a, b)
118  -t = Word.add(n, b, c)
119  +ua = uw(n, a)
120  +ub = uw(n, b)
121  +uc = uw(n, c)
122  +us = uw(n, Word.add(n, a, b))
123  +ut = uw(n, Word.add(n, b, c))
124  +uL = uw(n, Word.add(n, Word.add(n, a, b), c))
125  +uR = uw(n, Word.add(n, a, Word.add(n, b, c)))
126  +c1 = cy(n, a, b, False{})
127  +c2 = cy(n, b, c, False{})
128  +c3 = cy(n, Word.add(n, a, b), c, False{})
129  +c4 = cy(n, a, Word.add(n, b, c), False{})
130  +e1 = cons(n, Word.add(n, a, b), c)
131  +e2 = cons(n, a, b)
132  +e3 = cons(n, a, Word.add(n, b, c))
133  +e4 = cons(n, b, c)
134  # uL + sc(c3 + c1) == (ua + ub) + uc
135  +left = Equal.trans(Nat, Nat.add(uL, sc(n, Nat.add(c3, c1))), Nat.add(Nat.add(uL, sc(n, c3)), sc(n, c1)), Nat.add(Nat.add(ua, ub), uc),
136    %sc_add(n, c3, c1) : {Nat.add(uL, _) == Nat.add(Nat.add(uL, sc(n, c3)), sc(n, c1)) : Nat}
137    Equal.sym(Nat, Nat.add(Nat.add(uL, sc(n, c3)), sc(n, c1)), Nat.add(uL, Nat.add(sc(n, c3), sc(n, c1))), N.add_assoc(uL, sc(n, c3), sc(n, c1))),
138    %Equal.sym(Nat, Nat.add(uL, sc(n, c3)), Nat.add(us, uc), e1) : {Nat.add(_, sc(n, c1)) == Nat.add(Nat.add(ua, ub), uc) : Nat}
139    %Equal.sym(Nat, Nat.add(Nat.add(us, uc), sc(n, c1)), Nat.add(Nat.add(us, sc(n, c1)), uc), add_rot(us, uc, sc(n, c1))) : {_ == Nat.add(Nat.add(ua, ub), uc) : Nat}
140    %Equal.sym(Nat, Nat.add(us, sc(n, c1)), Nat.add(ua, ub), e2) : {Nat.add(_, uc) == Nat.add(Nat.add(ua, ub), uc) : Nat}
141    {==})
142  # uR + sc(c4 + c2) == (ua + ub) + uc
143  +right = Equal.trans(Nat, Nat.add(uR, sc(n, Nat.add(c4, c2))), Nat.add(Nat.add(uR, sc(n, c4)), sc(n, c2)), Nat.add(Nat.add(ua, ub), uc),
144    %sc_add(n, c4, c2) : {Nat.add(uR, _) == Nat.add(Nat.add(uR, sc(n, c4)), sc(n, c2)) : Nat}
145    Equal.sym(Nat, Nat.add(Nat.add(uR, sc(n, c4)), sc(n, c2)), Nat.add(uR, Nat.add(sc(n, c4), sc(n, c2))), N.add_assoc(uR, sc(n, c4), sc(n, c2))),
146    %Equal.sym(Nat, Nat.add(uR, sc(n, c4)), Nat.add(ua, ut), e3) : {Nat.add(_, sc(n, c2)) == Nat.add(Nat.add(ua, ub), uc) : Nat}
147    %Equal.sym(Nat, Nat.add(Nat.add(ua, ut), sc(n, c2)), Nat.add(ua, Nat.add(ut, sc(n, c2))), N.add_assoc(ua, ut, sc(n, c2))) : {_ == Nat.add(Nat.add(ua, ub), uc) : Nat}
148    %Equal.sym(Nat, Nat.add(ut, sc(n, c2)), Nat.add(ub, uc), e4) : {Nat.add(ua, _) == Nat.add(Nat.add(ua, ub), uc) : Nat}
149    Equal.sym(Nat, Nat.add(Nat.add(ua, ub), uc), Nat.add(ua, Nat.add(ub, uc)), N.add_assoc(ua, ub, uc)))
150  w_inj(n, Word.add(n, Word.add(n, a, b), c), Word.add(n, a, Word.add(n, b, c)), uniq(n, uL, uR, Nat.add(c3, c1), Nat.add(c4, c2), Equal.trans(Nat, Nat.add(uL, sc(n, Nat.add(c3, c1))), Nat.add(Nat.add(ua, ub), uc), Nat.add(uR, sc(n, Nat.add(c4, c2))), left, Equal.sym(Nat, Nat.add(uR, sc(n, Nat.add(c4, c2))), Nat.add(Nat.add(ua, ub), uc), right)), U.WB_unsigned(n, Word.add(n, Word.add(n, a, b), c)), U.WB_unsigned(n, Word.add(n, a, Word.add(n, b, c)))))