Resources

memory resources: cells and places

A cell: a piece of memory made of a size: Nat of octets of Bits (assumption: octets of bits).

# Addr is an abstract identity of a Cell:
const Addr
func (addr: Addr).space: AddrSpace
func (a1: Addr).is(a2: Addr): Bool

const Cell
# TODO: it is a Resource on Memory
func (p: Cell).addr: Addr
func (p: Cell).size: Nat
func (p: Cell).parent: Resource        # parent Cell?
func (p: Cell).manager: Maybe(Allocator)

Addr is a member of a set of type AddrSpace. It can be many things: a bare bin.Num as a C-style pointer, a pair of (AddrSpace, bin.Num), a 16-bit x86 pair of (Segment, U16), a CHERI memory handle (TODO), a hash for a content-addressable store (?), etc.

Process memory segments are Cells without values (but e.g. unused .bss can have a witness that all its bits are zero). They are narrowed down to smaller and smaller non-overlapping Cells used as Places for values of specific types. Cells are linear resources.

A place is a combination of a cell + a value type + a binary encoding of values into sequences of bits.

with (
    size: Int,
    ty: Type,
    encoder: ty -> Seq(size, U8)
    decoder: Seq(size, U8) -> ty,
) {
    const Place(ty)
    with (p: Place(ty)) {
        p.cell(): Cell
        p.get(): ty
        p.ref(): Ref(ty)
        do p.set(value: ty)     # linear action, consumes and produces
    }
}

Q: should a Place <-> Type relation be 1:1? Or: a Cell can be a part of many Places?

arrays

Arrays are fixed-size resources, laid out in contiguous memory (possibly with stride != item.size?).

No access by bare Nat indexes. Indexes should be opaque and be/have witnesses that they are valid and more static metainformation.

test {
    let a = do mem.Array(Int, 5)

    # if statically known size, compiler can verify this (implicit witness?):
    do a.at(1) = 43

    #
    do a.at(5) = -1 or error("out of bounds")
}

func (a: Array) Reverse() {
    var i0 = a.first()    # witness: i0 < a.len
    var i1 = a.last()     # witness: i1 < a.len
    while i0 < i1 {       # witness: i0 < i1
        a.swap(i0, i1)    # since i0 < i1, these are different places
        do i0.next()      # since i0 < a.len, no need to handle OOB
        do i1.prev()      # since i0 < i1, no need to handle OOB
    }
}

TODO: Accomodate Structs of Arrays naturally.

structs

Struct are less important and more obfuscated than in many other low-level languages. The notion of a composite value (a typed record) and memory resource holding it (Cell) is explicitly separated.

Structs do not necessarily live in contiguous blobs of memory (e.g. SOA). Abstract references that do not necessarily correspond to a pointer. Access happens via accessors that are efficiently inlined.

traits and objects

Can add complexity, but very useful to keep dot-namespaces flexible and extensible. Not sure how to fit them into the language yet.

memory management

Run-time behavior depends on given capabilities. Modules can be allocating or non-allocating. A package can request proc.alloc, then it is considered alloc-dependent. A sum of dependent package capabilities must be computed to ensure that a package is non-alloc (or e.g. non-panic). proc.alloc can be a heap memory allocator or a garbage-collecting allocator. Each package (module?) instance can use its own allocator.

Linear types + defer for resources that must be freed, including heap allocations?

Low-level, static memory management (i.e. ~ Rust core) in const-eval?