def no_carry

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/w64add.bend:91

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/word.bend as WD
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend as WW

91# no carry out of a sum that fits
92def no_carry(+one: Nat, +h1: {one == 1n : Nat}, +r: Nat, +c: Bool, +t: Nat, +e: {Nat.add(r, C.shift(32n, WD.bo(c, one))) == t : Nat}, +ht: {C.fits(32n, t) == True{} : Bool}) -> {c == False{} : Bool}:
93  match c:
94    case False{}:
95      {==}
96    case True{}:
97      Empty.absurd({True{} == False{} : Bool}, true_ne_false(Equal.trans(Bool, True{}, C.fits(32n, t), False{}, Equal.sym(Bool, C.fits(32n, t), True{}, ht), Equal.trans(Bool, C.fits(32n, t), C.fits(32n, Nat.add(r, C.shift(32n, one))), False{}, Equal.cong(Nat, Bool, z => C.fits(32n, z), t, Nat.add(r, C.shift(32n, one)), Equal.sym(Nat, Nat.add(r, C.shift(32n, one)), t, e)), WW.unfit_one(32n, one, h1, r)))))