def fin_lt

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/u32div.bend:119

import Base
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/lib/lemmas/proofs/division_bounds.bend as DB

119def fin_lt(+p: Nat, +q: Word(p), +s: U32, +b: U32, +a0: Bool, +hi: Word(p), +r: Nat, +he: {Nat.add(Nat.mul(S.unsigned(p, q), v(b)), r) == S.unsigned(p, hi) : Nat}, +hs: {v(s) == Nat.add(S.bit_value(a0), Nat.double(r)) : Nat}, +hge: {Nat.is_ge(v(s), v(b)) == False{} : Bool}) -> inv(1n+p, WCon{a0, hi}, v(b), U32.divmod.go.fin(p, q, s, b, False{})):
120  +bn = v(b)
121  +t = Nat.add(S.bit_value(a0), Nat.double(r))
122  +lt = DB.not_ge(v(s), bn, hge)
123  +eq = Equal.trans(Nat, Nat.add(Nat.mul(Nat.double(S.unsigned(p, q)), bn), v(s)), Nat.add(Nat.mul(Nat.double(S.unsigned(p, q)), bn), t), Nat.add(S.bit_value(a0), Nat.double(S.unsigned(p, hi))),
124    Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(Nat.double(S.unsigned(p, q)), bn), z), v(s), t, hs),
125    %he : {Nat.add(Nat.mul(Nat.double(S.unsigned(p, q)), bn), t) == Nat.add(S.bit_value(a0), Nat.double(_)) : Nat}
126    digit_zero(S.unsigned(p, q), bn, r, S.bit_value(a0)))
127  (eq, lt)