Hi all,

Some capability resolution, such as for fault handling, winds up calling resolveAddressBits with n_bits = wordBits, and any remaining bits are ignored. In other cases, such as the destination slot for seL4_CNode_Copy, the user provides a resolution depth parameter, and the call to resolveAddressBits is mediated by lookupSlotForCNodeOp, which fails with a depth mismatch if there are any bits remaining.

Individually these seem like reasonable choices, but it leads to code like this: 

    seL4_CNode cspace_root = ...; // freshly allocated 256-slot CNode with no guard
    seL4_CPtr slot_for_copy = 0x23; // arbitrary slot we know is available
    seL4_CPtr slot_for_tcb = slot_for_copy << 24;

    seL4_CNode_Copy(cspace_root , endpoint_for_copy, 8, ...);
    seL4_TCB_Configure(..., endpoint_for_tcb, ...);

I found it surprising that two different CPtrs are needed to describe the same slot! Is there a conceptual-model-explanation that doesn't involve appeal to the underlying implementation?

Also: my current understanding is that the depth parameter is only needed to disambiguate indirections through CNode-containing slots. What goes wrong if the depth mismatch checks are relaxed?