def AP.u32_wrap

bend-osdev-array@0.1.0.1 · PROOF.bend:1733

import Base
import bend-osdev-array@0.1.0.1/array.bend as A

1733def AP.u32_wrap(a: U32, +d: Nat, +k: Nat, e: {U32.to_nat(a) == Nat.add(A.Arrays.slots(d), k) : Nat}, hk: {Nat.is_lt(k, A.Arrays.slots(d)) == True{} : Bool}, hd: {Nat.is_lt(d, 32n) == True{} : Bool}) -> {U32.to_nat(U32.and(a, U32{AP.lm(32n, d)})) == k : Nat}:
1734  match a:
1735    case U32{w}:
1736      AP.wrap(32n, w, d, k, e, hk, hd)