Some arithmetic:
For any j > 0, there is a unique pair (n, k) such that j = (2k+1)2^{n}.

Every access to memory is via a memory cap and an integer offset. We write A(c, j) to denote the byte or cap sized memory location accessed by cap c and offset j.

For every memory cap c there is a positive integer n such that for all integers j and k:

If 0 ≤ j < k < 2^{n} then A(c, j) and A(c, k) are both valid and denote different memory locations.

There is just one such n and we write n = S(c).

If j ≥ 2^{S(c)} then A(c, j) is invalid, yields nothing and results in some sort of safe fault.

There are the following machine ops:

- S takes a cap c and returns S(c).
- Sub takes a cap and integer, and yields a cap.

If n < S(c) then S(Sub(c, (2k+1)2^{n})) = n+1

If j < 2^{n+1}then A(Sub(c, (2k+1)2^{n}), j) = A(c, 2^{n+1}k+j). - Loc takes two caps and yields an int:

If j < S(c) then Loc(c, Sub(c, j)) = j.

Loc yields 0 if the respective blocks are disjoint. - Load takes a cap c, an int j and if j < S(c) returns the current contents of A(c, j).
- Store takes a cap c, an int j and a byte b, and if j < S(c) changes A(c, j) to hold b.

- S returns the log of the size of the memory block referred to by the cap.
- Sub derives a sub-cap to a specified sub-block from a cap to the super-block.
- Loc determines whether one cap is to a sub-block of the other, and if so says which sub-block.
- Load fetches the content of the byte of the sub-block of the cap, indexed by an int.
- Store changes the content of the byte of the sub-block of the cap, indexed by an int.

To be integrated:

There exists a null cap d such that S(d) = −1 and for all c Sub(c, 0) = d.

There is a cap c such that S(c) = 56, or thereabouts.