def c3_eq

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

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD
import bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64.bend as P64
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64mul.bend as W64M
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sqrt.bend as W64S
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend as LW

115# the carry of s + b32(c) is c and s all ones
116def c3_eq(+one: Nat, +h1: {one == 1n : Nat}, +s: U32, +c: Bool, +m: U32, +pm: {m == U32{WD.mask(32n, 32n)} : U32}) -> {P64.carry32(s, X.b32(c)) == Bool.and(c, U32.is_eq(s, m)) : Bool}:
117  match c:
118    case False{}:
119      +ht = L.subst(Nat, z => {C.fits(32n, z) == True{} : Bool}, v(s), Nat.add(v(s), 0n), Equal.sym(Nat, Nat.add(v(s), 0n), v(s), N.add_zero(v(s))), vb(s))
120      no_carry(one, h1, v(U32.add(s, 0)), P64.carry32(s, 0), Nat.add(v(s), 0n), acons_o(one, h1, s, 0), ht)
121    case True{}:
122      +em = Equal.trans(Nat, 1n+v(m), WD.sc(32n, one), C.shift(32n, one), W64S.mask_v(32n, {==}, one, h1, m, pm), Equal.sym(Nat, C.shift(32n, one), WD.sc(32n, one), W64M.shift_sc(32n, one)))
123      +c1 = c_one(one, h1, v(U32.add(s, 1)), v(s), v(m), P64.carry32(s, 1), acons_o(one, h1, s, 1), em, vb(U32.add(s, 1)), vb(s))
124      Equal.trans(Bool, P64.carry32(s, 1), Nat.is_eq(v(s), v(m)), U32.is_eq(s, m), c1, Equal.sym(Bool, U32.is_eq(s, m), Nat.is_eq(v(s), v(m)), LW.eq_nat(s, m)))