Figure 27 — Upload-Driven Lifecycle
The complete lifecycle from source code to running abstraction: the CLOOMC++ compiler produces a compiled abstraction, which Navana validates, allocates a power-of-2 lump, writes code and c-list, creates a sealed NS entry, forges an Inform E-GT, and returns it to the creator.
1
Source Code
JavaScript or Haskell — problem-oriented language
abstraction MyRobot {
capabilities { Memory, Scheduler }
method Forward(steps) { ... }
}
2
CLOOMC++ Compiler
Parse → Resident Object Model → Code Generator
Maps capabilities to c-list offsets, emits 32-bit instruction words
Correctness Domain (outside TCB)
• Compiler bugs → wrong answers, never security breaches
• Cannot forge GTs, escape bounds, or access other c-lists
produces
3
Compiled Abstraction
{ "abstraction": "MyRobot",
"type": "abstraction", "grants": ["E"],
"capabilities": [{ "target":7, "grants":["E"] }, ...],
"methods": [{ "name":"Forward", "code":[0x1E8...] }] }
Upload Format Fields
abstraction : problem-oriented namecapabilities : c-list wiring (target index + grants)methods : name + compiled code word arrayssubmitted to
4
Navana.Abstraction.Add (Validation)
✓ codeSize + clistCount ≤ allocSize (no overlap)
✓ Each capability: creator holds GT with sufficient perms
✓ clistCount ≤ 511 (fits 9-bit field)
✓ allocSize is valid power-of-2 ≥ 256
Security Checks (R007)
✗ Integer underflow in clistStart → REJECT
✗ Capability escalation (no delegation) → REJECT
✗ Code overlaps c-list region → REJECT
Navana is sole NS writer — all creation goes through here
validated → proceed
5
Memory.Allocate (Power-of-2 Lump)
Round up: codeSize + clistCount → next power-of-2 (min 32)
Returns: base address + allocated size
Power-of-2 Sizing
10 code + 3 c-list = 13 words → alloc 256 (next power-of-2)
Freespace = 256 - 13 = 243 words (growth room)
6
Write Code + Populate C-List
Code region (offset 0):
method_table[N] + compiled code words → DWRITE to lump
C-list region (offset clistStart):
Forge E-GTs for each capability → SAVE to c-list slots
Lump Layout After Write
Code (method_table + instructions) — Turing X
FREESPACE (inaccessible)
C-List (GT slots) — Church L
clistStart = allocSize - clistCount
7
NS Entry Creation (Navana.Add)
W0: location = base address
W1: B|F|G|C|type=01|clistCount|limit
W2: seal = CRC-16(location, limit)
Navana is Sole NS Writer
Finds free NS slot, writes sealed 3-word entry
clistCount encoded in word1 bits[25:17]
Seal protects against tampering (R002)
8
Forge Inform E-GT → Return to Creator
E-GT: Version(7) | Index(17) | Perms=E(6) | Type=01(2)
Creator receives sole E-GT — can CALL the new abstraction
Lifecycle Complete
Creator can now CALL the abstraction via the E-GT
CALL reads clistCount, splits lump → CR14 (X) + CR6 (L)
E-GT returned to creator — lifecycle restarts on next CALL