def low_exact

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/w64dm.bend:178

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
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/math/typed/width.bend as WW

178# a 96-bit value below 2^64 has top word 0: its low 64 bits are the value
179def low_exact(+r: Nat, +t: Nat, +x: Nat, +e: {Nat.add(r, C.shift(64n, t)) == x : Nat}, +hr: {C.fits(64n, r) == True{} : Bool}, +hx: {C.fits(64n, x) == True{} : Bool}) -> {r == x : Nat}:
180  +et = Equal.trans(Nat, t, C.high(64n, Nat.add(r, C.shift(64n, t))), 0n, Equal.sym(Nat, C.high(64n, Nat.add(r, C.shift(64n, t))), t, WW.high_u(64n, r, t, hr)), Equal.trans(Nat, C.high(64n, Nat.add(r, C.shift(64n, t))), C.high(64n, x), 0n, Equal.cong(Nat, Nat, z => C.high(64n, z), Nat.add(r, C.shift(64n, t)), x, e), N.eq_from_is_eq(C.high(64n, x), 0n, hx)))
181  Equal.trans(Nat, r, Nat.add(r, C.shift(64n, 0n)), x, Equal.sym(Nat, Nat.add(r, C.shift(64n, 0n)), r, Equal.trans(Nat, Nat.add(r, C.shift(64n, 0n)), Nat.add(r, 0n), r, Equal.cong(Nat, Nat, z => Nat.add(r, z), C.shift(64n, 0n), 0n, WW.shift_zero(64n)), N.add_zero(r))), Equal.trans(Nat, Nat.add(r, C.shift(64n, 0n)), Nat.add(r, C.shift(64n, t)), x, Equal.cong(Nat, Nat, z => Nat.add(r, C.shift(64n, z)), 0n, t, Equal.sym(Nat, t, 0n, et)), e))