def add_split

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/w64m128.bend:54

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/w64.bend as X
import bend-collections-laws-crypto@1.0.0.0/src/math/u64.bend as WU
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64add.bend as WA
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend as WW

54# the sum of two 64-bit values: low 64 bits + 2^64 * the overflow bit
55def add_split(+p: WU.U64, +q: WU.U64) -> {Nat.add(SW.value(p), SW.value(q)) == Nat.add(SW.value(X.add(p, q)), C.shift(64n, S.bit_value(X.add_over(p, q)))) : Nat}:
56  +s = Nat.add(SW.value(p), SW.value(q))
57  av = WA.add_value(p, q)
58  ov = WA.add_over_value(p, q)
59  +hs = sum_fits(64n, SW.value(p), SW.value(q), fit64(p), fit64(q))
60  +hh = fits_hi(s, hs)
61  +eo = Equal.trans(Nat, S.bit_value(X.add_over(p, q)), S.bit_value(Bool.not(Nat.is_eq(C.high(64n, s), 0n))), C.high(64n, s), Equal.cong(Bool, Nat, z => S.bit_value(z), X.add_over(p, q), Bool.not(Nat.is_eq(C.high(64n, s), 0n)), ov), bit_nz(C.high(64n, s), hh))
62  Equal.trans(Nat, s, Nat.add(C.low(64n, s), C.shift(64n, C.high(64n, s))), Nat.add(SW.value(X.add(p, q)), C.shift(64n, S.bit_value(X.add_over(p, q)))), WW.low_high(64n, s), Equal.trans(Nat, Nat.add(C.low(64n, s), C.shift(64n, C.high(64n, s))), Nat.add(SW.value(X.add(p, q)), C.shift(64n, C.high(64n, s))), Nat.add(SW.value(X.add(p, q)), C.shift(64n, S.bit_value(X.add_over(p, q)))), Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(64n, C.high(64n, s))), C.low(64n, s), SW.value(X.add(p, q)), Equal.sym(Nat, SW.value(X.add(p, q)), C.low(64n, s), av)), Equal.cong(Nat, Nat, z => Nat.add(SW.value(X.add(p, q)), C.shift(64n, z)), C.high(64n, s), S.bit_value(X.add_over(p, q)), Equal.sym(Nat, S.bit_value(X.add_over(p, q)), C.high(64n, s), eo))))