def shl_c

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/w64sh.bend:244

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-crypto@1.0.0.0/spec/math/w64.bend as SW
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/math/typed/width.bend as WW

244def shl_c(+l: U32, +h: U32, +k: Nat, +c: Bool, +hc: {Nat.is_lt(k, 32n) == c : Bool}, +hk: {Nat.is_lt(k, 64n) == True{} : Bool}) -> {SW.value(X.shl_pick(WU.U64{l, h}, k, c)) == C.low(64n, C.shift(k, val(l, h))) : Nat}:
245  match k c:
246    case 0n True{}:
247      Equal.sym(Nat, C.low(64n, val(l, h)), val(l, h), WW.low_fit(64n, val(l, h), fit64(l, h)))
248    case 1n+ +j True{}:
249      shl_small(l, h, j, hc)
250    case _ False{}:
251      shl_big(l, h, k, N.not_lt_le(k, 32n, hc), hk)