def fin_ge

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

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/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/lib/u32.bend as U
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/division_bounds.bend as DB

102def fin_ge(+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}, +hr: {Nat.is_lt(r, v(b)) == True{} : Bool}, +hs: {v(s) == Nat.add(S.bit_value(a0), Nat.double(r)) : Nat}, +hge: {Nat.is_ge(v(s), v(b)) == True{} : Bool}) -> inv(1n+p, WCon{a0, hi}, v(b), U32.divmod.go.fin(p, q, s, b, True{})):
103  +bn = v(b)
104  +t = Nat.add(S.bit_value(a0), Nat.double(r))
105  +htb = L.subst(Nat, z => {Nat.is_lt(t, z) == True{} : Bool}, Nat.double(bn), Nat.add(bn, bn), NA.double_self(bn), N.double_lt_bit(a0, r, bn, hr))
106  +hle = Equal.trans(Bool, Nat.is_le(bn, v(s)), Nat.is_ge(v(s), bn), True{}, Equal.sym(Bool, Nat.is_ge(v(s), bn), Nat.is_le(bn, v(s)), DB.ge_reverse(v(s), bn)), hge)
107  +d = Nat.sub(v(s), bn)
108  +hsub = U.sub_nat(s, b, hle)
109  +hsum = Equal.trans(Nat, Nat.add(bn, d), v(s), t, N.sub_add(v(s), bn, hle), hs)
110  +hsb = L.subst(Nat, z => {Nat.is_lt(z, Nat.add(bn, bn)) == True{} : Bool}, t, v(s), Equal.sym(Nat, v(s), t, hs), htb)
111  +hdb = N.sub_lt(v(s), bn, bn, hle, hsb)
112  +eq = Equal.trans(Nat, Nat.add(Nat.mul(1n+Nat.double(S.unsigned(p, q)), bn), v(U32.sub(s, b))), Nat.add(Nat.mul(1n+Nat.double(S.unsigned(p, q)), bn), d), Nat.add(S.bit_value(a0), Nat.double(S.unsigned(p, hi))),
113    Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(1n+Nat.double(S.unsigned(p, q)), bn), z), v(U32.sub(s, b)), d, hsub),
114    %he : {Nat.add(Nat.mul(1n+Nat.double(S.unsigned(p, q)), bn), d) == Nat.add(S.bit_value(a0), Nat.double(_)) : Nat}
115    digit_one(S.unsigned(p, q), bn, r, S.bit_value(a0), d, hsum))
116  +lt = L.subst(Nat, z => {Nat.is_lt(z, bn) == True{} : Bool}, d, v(U32.sub(s, b)), Equal.sym(Nat, v(U32.sub(s, b)), d, hsub), hdb)
117  (eq, lt)