def expand

bend-collections-laws-crypto@1.0.0.0 · proofs/math/u64/u64div.bend:109

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/u32alg.bend as A
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend as WD

109# 2^8 (2^12 (2^12 h + a) + b) + c == ((2^20 a + 2^8 b) + c) + 2^32 h
110def expand(+h: Nat, +a: Nat, +b: Nat, +c: Nat) -> {Nat.add(WD.sc(8n, Nat.add(WD.sc(12n, Nat.add(WD.sc(12n, h), a)), b)), c) == Nat.add(Nat.add(Nat.add(WD.sc(20n, a), WD.sc(8n, b)), c), WD.sc(32n, h)) : Nat}:
111  +rhs = Nat.add(Nat.add(Nat.add(WD.sc(20n, a), WD.sc(8n, b)), c), WD.sc(32n, h))
112  +x = WD.sc(32n, h)
113  +y = WD.sc(20n, a)
114  +z = WD.sc(8n, b)
115  %A.sc_add(12n, WD.sc(12n, h), a) : {Nat.add(WD.sc(8n, Nat.add(_, b)), c) == rhs : Nat}
116  %A.sc_add(8n, Nat.add(WD.sc(12n, WD.sc(12n, h)), WD.sc(12n, a)), b) : {Nat.add(_, c) == rhs : Nat}
117  %A.sc_add(8n, WD.sc(12n, WD.sc(12n, h)), WD.sc(12n, a)) : {Nat.add(Nat.add(_, z), c) == rhs : Nat}
118  Equal.trans(Nat, Nat.add(Nat.add(Nat.add(x, y), z), c), Nat.add(Nat.add(x, Nat.add(y, z)), c), rhs,
119    Equal.cong(Nat, Nat, w => Nat.add(w, c), Nat.add(Nat.add(x, y), z), Nat.add(x, Nat.add(y, z)), N.add_assoc(x, y, z)),
120    Equal.trans(Nat, Nat.add(Nat.add(x, Nat.add(y, z)), c), Nat.add(x, Nat.add(Nat.add(y, z), c)), rhs, N.add_assoc(x, Nat.add(y, z), c), N.add_comm(x, Nat.add(Nat.add(y, z), c))))