def est_eq_c

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/w64est.bend:189

import Base
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/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64sqrt.bend as W64S

189def est_eq_c(+y: WU.U64, +d: U32, +hd: {U32.is_zero(d) == False{} : Bool}, +bp: Nat, +hn: {v(d) == 1n+bp : Nat}, +c: Bool, +hc: {U32.is_le(d, X.hi(y)) == c : Bool}) -> {X.est_pick(y, d, c) == X.q_clamp(X.fst_q(X.div32(y, d))) : U32}:
190  match c:
191    case True{}:
192      +h0 = Equal.trans(Bool, Nat.is_le(v(d), v(X.hi(y))), U32.is_le(d, X.hi(y)), True{}, Equal.sym(Bool, U32.is_le(d, X.hi(y)), Nat.is_le(v(d), v(X.hi(y))), W64S.is_le_nat(d, X.hi(y))), hc)
193      +hle = L.subst(Nat, z => {Nat.is_le(z, v(X.hi(y))) == True{} : Bool}, v(d), 1n+bp, hn, h0)
194      %Equal.sym(Bool, U32.is_zero(U32.div(X.hi(y), d)), False{}, dpos(X.hi(y), d, hd, bp, hn, hle)) : {4294967295 == X.q_clamp_z(X.lo(X.fst_q(X.div32(y, d))), _) : U32}
195      {==}
196    case False{}:
197      +h0 = Equal.trans(Bool, Nat.is_le(v(d), v(X.hi(y))), U32.is_le(d, X.hi(y)), False{}, Equal.sym(Bool, U32.is_le(d, X.hi(y)), Nat.is_le(v(d), v(X.hi(y))), W64S.is_le_nat(d, X.hi(y))), hc)
198      +hl = L.subst(Nat, z => {Nat.is_lt(v(X.hi(y)), z) == True{} : Bool}, v(d), 1n+bp, hn, N.not_le_lt(v(d), v(X.hi(y)), h0))
199      %Equal.sym(U32, U32.mod(X.hi(y), d), X.hi(y), msmall(X.hi(y), d, hd, bp, hn, hl)) : {X.est_pick(y, d, False{}) == X.q_clamp(X.fst_q(X.div32_t1(U32.div(X.hi(y), d), X.lo(y), X.dig_t(U32.to_nat(_), 65536n, X.dig1(X.lo(y))), U32.to_nat(d)))) : U32}
200      %Equal.sym(U32, U32.div(X.hi(y), d), 0, dsmall(X.hi(y), d, hd, bp, hn, hl)) : {X.est_pick(y, d, False{}) == X.q_clamp(X.fst_q(X.div32_t1(_, X.lo(y), X.dig_t(U32.to_nat(X.hi(y)), 65536n, X.dig1(X.lo(y))), U32.to_nat(d)))) : U32}
201      {==}