def neg

bend-collections-laws-math@1.0.0.0 · proofs/math/u64/u64.bend:242

import Base
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as U
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/src/wide.bend as W
import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD

242# THEOREM: neg is two's-complement negation.
243def neg(+a: U.U64) -> {bits(U.neg(a)) == Word.inc(64n, Word.not(64n, bits(a))) : Word(64n)}:
244  match a:
245    case U.U64{+lo, +hi}:
246      match lo hi:
247        case U32{+x} U32{+y}:
248          +nx = Word.not(32n, x)
249          +ny = Word.not(32n, y)
250          +j = W.join(32n, 32n, Word.inc(32n, nx), WD.incif(32n, WD.ones(32n, nx), ny))
251          +p1 = Equal.cong(U32, Word(64n), z => W.pack(U32{Word.inc(32n, nx)}, z), U32.add(U32{ny}, U.carry(U32.is_zero(U32{Word.inc(32n, nx)}))), U32{WD.incif(32n, WD.ones(32n, nx), ny)},
252            Equal.trans(U32, U32.add(U32{ny}, U.carry(U32.is_zero(U32{Word.inc(32n, nx)}))), U32.add(U32{ny}, U.carry(WD.ones(32n, nx))), U32{WD.incif(32n, WD.ones(32n, nx), ny)},
253              Equal.cong(Bool, U32, c => U32.add(U32{ny}, U.carry(c)), U32.is_zero(U32{Word.inc(32n, nx)}), WD.ones(32n, nx), inc_zero32(nx)),
254              add_carry(ny, WD.ones(32n, nx))))
255          +p2 = Equal.trans(Word(64n), Word.inc(64n, Word.not(64n, W.join(32n, 32n, x, y))), Word.inc(64n, W.join(32n, 32n, nx, ny)), j,
256            Equal.cong(Word(64n), Word(64n), w => Word.inc(64n, w), Word.not(64n, W.join(32n, 32n, x, y)), W.join(32n, 32n, nx, ny), WD.not_join(32n, 32n, x, y)),
257            WD.inc_join(32n, 32n, nx, ny))
258          Equal.trans(Word(64n), bits(U.neg(U.U64{U32{x}, U32{y}})), j, Word.inc(64n, Word.not(64n, W.join(32n, 32n, x, y))), p1, Equal.sym(Word(64n), Word.inc(64n, Word.not(64n, W.join(32n, 32n, x, y))), j, p2))