def neg_sum

bend-collections-laws-crypto@1.0.0.0 · proofs/math/random/uint64n.bend:63

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/spec/math/w64.bend as SW
import bend-collections-laws-crypto@1.0.0.0/src/math/u64.bend as WU
import bend-collections-laws-crypto@1.0.0.0/src/math/w64.bend as X
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend as WI
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64m128.bend as M128

63# a nonzero word and its negation add up to 2^64
64def neg_sum(+one: Nat, +h1: {one == 1n : Nat}, +n: WU.U64, +hn: {Nat.is_eq(SW.value(n), 0n) == False{} : Bool}) -> {Nat.add(SW.value(X.sub(Z(), n)), SW.value(n)) == C.shift(64n, one) : Nat}:
65  +s = SW.value(X.sub(Z(), n))
66  +vn = SW.value(n)
67  +q = M128.QSUB(one, Z(), n)
68  +e = M128.sub_eq(one, h1, Z(), n)
69  +hs = Equal.trans(Bool, C.fits(65n, C.shift(64n, q)), C.fits(65n, Nat.add(s, vn)), True{}, Equal.cong(Nat, Bool, z => C.fits(65n, z), C.shift(64n, q), Nat.add(s, vn), Equal.sym(Nat, Nat.add(s, vn), C.shift(64n, q), e)), M128.sum_fits(64n, s, vn, M128.fit64(X.sub(Z(), n)), M128.fit64(n)))
70  +hq1 = Equal.trans(Bool, C.fits(1n, q), C.fits(1n, C.high(64n, C.shift(64n, q))), True{}, Equal.cong(Nat, Bool, z => C.fits(1n, z), q, C.high(64n, C.shift(64n, q)), Equal.sym(Nat, C.high(64n, C.shift(64n, q)), q, WI.high_u(64n, 0n, q, {==}))), M128.fits_hi(C.shift(64n, q), hs))
71  +hq = q_nz(q, s, vn, hn, e)
72  %q_one(q, one, h1, Nat.is_eq(q, 0n), {==}, hq, hq1) : {Nat.add(s, vn) == C.shift(64n, _) : Nat}
73  e