def slot

lawful-arrays@0.1.0.0 · defs.bend:31

import Base

31# The leaf an access at index i reaches in a perfect tree of depth d < 32:
32# i modulo 2^d. (From depth 32 up, Base's Array.size wraps to 0 and every
33# access reaches the last leaf; the laws exclude that.)
34def slot(i: U32, d: Nat) -> Nat:
35  Nat.mod(U32.to_nat(i), Nat.pow(2n, d))