def shl_ts

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

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/word.bend as WD

136def shl_ts(+p: Nat, +q: Word(p), +b: U32, +t: Bool, +s: 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, s), WD.sc(32n, WD.bo(t, one))) == Nat.add(S.bit_value(a0), Nat.double(r)) : Nat}) -> inv(1n+p, WCon{a0, hi}, v(b), U32.divmod.go.fin(p, q, U32{s}, b, Bool.or(t, U32.is_ge(U32{s}, b)))):
137  match t:
138    case True{}:
139      fin_true(p, q, U32{s}, b, a0, hi, r, one, h1, he, hr, L.subst(Nat, z => {Nat.add(z, WD.sc(32n, one)) == Nat.add(S.bit_value(a0), Nat.double(r)) : Nat}, WD.uw(32n, s), v(U32{s}), Equal.sym(Nat, v(U32{s}), WD.uw(32n, s), vw(s)), hts))
140    case False{}:
141      +hs = Equal.trans(Nat, v(U32{s}), WD.uw(32n, s), Nat.add(S.bit_value(a0), Nat.double(r)), vw(s), Equal.trans(Nat, WD.uw(32n, s), Nat.add(WD.uw(32n, s), 0n), Nat.add(S.bit_value(a0), Nat.double(r)), Equal.sym(Nat, Nat.add(WD.uw(32n, s), 0n), WD.uw(32n, s), N.add_zero(WD.uw(32n, s))), hts))
142      fin_false(p, q, U32{s}, b, a0, hi, r, he, hr, hs, U32.is_ge(U32{s}, b), {==})