module Savi::Compiler::XTypes::Cap

Defined in:

savi/compiler/xtypes/cap.cr

Constant Summary

BIT_ADDR = 1_u8 << 0

Each cap is represented as a bitset of five fundamental elements, with each element having an associated semantic meaning.

BIT_HELD = 1_u8 << 3

BIT_READ = 1_u8 << 1

BIT_ROOT = 1_u8 << 4

BIT_WRITE = 1_u8 << 2

BITS_ALL_UNION = (((BIT_ROOT | BIT_HELD) | BIT_WRITE) | BIT_READ) | BIT_ADDR

BOX = BOX_P + BIT_HELD

BOX_P = TAG + BIT_READ

ISO = REF + BIT_ROOT

NON = 0_u8

From these five bits we form a lattice of the useful combinations of them, forming the caps that users can refer to in type expression syntax.

In our constants, we use BOX_P and REF_P to refer to box' and ref', respectively. The "prime" character '` cannot be used, so we use _P here.

The most powerful cap iso contains all permission bits, so in type theory it is considered to be the "bottom cap", as it is a subtype of all caps. That is, it is the most specific type and has the most features, so no other cap can be used where an iso is expected.

Similarly, the weakest cap non is considered the "top cap", because it has no bits/features in it that are not also in the other caps, making all other caps subtypes of it (and making it the top supertype).

The lattice looks like this, portrayed as a graph with subtypes being below, with non as the "top cap" and iso as the "bottom cap" in the lattice.

non             (top cap: widest, fewest features, weakest)
 |
 |
tag
 |
 |
box'

/ \ (lines show subtyping relationships, with the / \ subtype shown below its immediate supertype) ref' box \ /
\ /
ref val \ / \ / iso (bottom cap: narrowest, most features, strongest)

REF = REF_P + BIT_HELD

REF_P = BOX_P + BIT_WRITE

TAG = NON + BIT_ADDR

VAL = BOX + BIT_ROOT