def shl_ok

bend-collections-laws-math@1.0.0.0 · proofs/lib/u32div.bend:144

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S
import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD

144def shl_ok(+p: Nat, +q: Word(p), +b: U32, ts: Bool & Word(32n), +a0: Bool, +hi: Word(p), +r: Nat, +one: Nat, +h1: {one == 1n : 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}, hts: {Nat.add(WD.uw(32n, WD.ow(32n, ts)), WD.sc(32n, WD.bo(WD.ob(32n, ts), one))) == Nat.add(S.bit_value(a0), Nat.double(r)) : Nat}) -> inv(1n+p, WCon{a0, hi}, v(b), U32.divmod.go.shl(p, q, b, ts)):
145  match ts:
146    case (+t, +s):
147      shl_ts(p, q, b, t, s, a0, hi, r, one, h1, he, hr, hts)