def bitw.last_le

bend-osdev-algo@0.1.0.0 · PROOF.bend:498

import Base
import bend-osdev-algo@0.1.0.0/algo.bend as A

498# with the highest set bit at k, k <= m in a word of width 1 + m
499def bitw.last_le(+m: Nat, +w: Word(1n+m), +k: Nat, e: {A.bitw.index(A.bitw.fls(1n+m, w)) == Some{k} : Maybe<&2, Nat>}) -> {Nat.is_le(k, m) == True{} : Bool}:
500  %bitw.index_some(A.bitw.fls(1n+m, w), k, e) : {Nat.is_le(_, 1n+m) == True{} : Bool}
501  bitw.fls_le(1n+m, w)