This is an axiomatic description of how buddy caps appear to the user. While it is precise and concise, it is, alas, hard to understand. Below j, k and n are all non-negative integers. “c” and “d” always denote a cap.

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

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 < 2n 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 ≥ 2S(c) then A(c, j) is invalid, yields nothing and results in some sort of safe fault.

There are the following machine ops:

In plain words: Of course the Load and Store ops must be designed to preserve the distinction between byte and cap. Slight adjustments are required above for unsegregated cap designs.
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.