Composability — the building-block contract

Status: Design record. The principles (one-way DAG, the stud vocabulary, the TK_CONFIG_* selectors) are settled and in use throughout the root tree; the machine enforcement (the minimal-build matrix, §6) is designed but not yet migrated — the tooling lives at _legacy/tools/ and the sovereign/feature probe examples it drives do not exist at root (§7). Known glue is catalogued honestly (§7–8). Scope: the rules that keep k2’s layers (HAL · kernel · application) and the components within each layer independently usable — “bricks connected by studs, not fused by glue.” Companions: kernel-tiers.md (the header/symbol split), board-contract.md (the board↔kernel boundary), hal-architecture.md (HAL internals), ADR 0002 (§7 tracks the one live leak).

1. Thesis

k2 is a set of bricks: independently selectable components you assemble into exactly the system you need — as much HAL, as much kernel, as much application as the job calls for, and no more. Bricks are not independent (a blocking mutex genuinely needs a scheduler); they are decoupled — they connect only through narrow, declared, one-way interfaces (studs), never through hidden, bidirectional fusion (glue).

In an embedded, safety-minded system this is the opposite of a luxury:

  • Pay only for what you use. Flash/RAM budgets make à-la-carte composition a requirement. A brick you didn’t select costs zero bytes.

  • Composability is a safety asset. A small, named set of bricks with freedom-from-interference is easier to certify than a monolith: smaller TCB, explicit interfaces, and an argument that an unused brick cannot affect a used one — because it isn’t linked.

  • Confidence is machine-checked, not hoped. “This brick is decoupled” is provable: it links alone (§6).

2. The layer model and the one-way dependency rule

Three layers, and a single invariant that governs all coupling:

Dependencies flow one way only. hardware ← HAL ← kernel, HAL ← application, kernel ← application (optional). No brick names a brick above it. The graph is a DAG.

            application            (sovereign, privileged, or confined — see below)
             /         \
        (optional)      \
            v            v
          kernel ----> HAL ----> hardware
                        ^
                        |
                  (kernel and application are PEERS on the HAL)

Consequences that follow directly:

  • The HAL is a capability layer, never a policy layer. It abstracts hardware so the code above is portable; it has no power to restrict. “Running on the HAL” can never mean “limited.”

  • The kernel is the only layer that can restrict, and only via its hardware-management machinery (context switch, MPU, the unprivileged-thread confinement). Restriction is a kernel service, not a HAL property.

  • An application is a peer of the kernel on the HAL. Both sit directly on it; the kernel is a component that also offers management. Hence three application modes:

    mode

    how it runs

    hardware access

    gets kernel services

    sovereign (bare)

    no kernel below it

    full — identical to the kernel’s

    no

    privileged

    under the kernel

    full; drives hardware in parallel with the kernel

    yes

    confined (TK_CONFIG_UNPRIV_THREADS)

    under the kernel

    mediated via the syscall trap; kernel RAM/peripherals locked

    yes

    “HAL-only” would be a misleading name for the first mode: it is the maximal-freedom mode. The “only” describes what is below the app (nothing but the HAL), not what it may do (everything). Prefer sovereign / bare. It gives up services, not rights. The confined mode’s syscall/handle stud is specified in kernel-tiers.md (Tier A [rt] ops + the confinement seam).

The corollary the whole document turns on: the HAL must never depend on the kernel for behaviour. The HAL knows nothing of the kernel’s code; a HAL file that names a kernel function or object is a dependency inversion — glue — and §7/§8 show the places the root tree currently does this.

One narrow, deliberate exception (ADR 0002 review 0001, D1): shared pure-TYPE vocabulary. tk_status_t (like tk_stack_cell_t) is a compile-time TYPE both layers agree on. The kernel’s public API now returns tk_status_t, so an app that includes tk_kernel.h and a HAL header must see ONE definition or the enum constants collide — and the kernel may depend only on the arch layer, so the shared type cannot live in the HAL. It therefore lives in kernel/tk_status.h (a sibling of kernel/tk_types.h) and the HAL borrows it via #include. This is a pure type borrow — zero code, zero link symbols: a sovereign HAL build still references no kernel symbol (I2 holds; types don’t link), it only needs kernel/ on its include path. The forbidden thing stays forbidden — a HAL brick naming a kernel function/object. Graph: arch <- kernel <- hal (types only).

3. The brick map (what the build actually sees)

The build’s source groups are the brick boundaries. In the reshaped root (make/tk.mk + make/board/<board>.mk) there are three:

group

defined in

contents

TK_KERNEL_SRCS

make/tk.mk

kernel/tk_kernel.c · tk_sync.c · tk_trace_ring.c — constant across every board/arch

TK_ARCH_SRCS

make/arch/<arch>.mk

the CPU port (arch/<cpu>/kernel_arch.c, switch .S, …)

TK_BOARD_SRCS

make/board/<board>.mk

the board’s HAL-port .c and hal/tk_console.c

Note — there is no TK_HAL_SRCS at root. The portable HAL is header-only (hal/*.h) plus the one shared hal/tk_console.c; every concrete peripheral driver is a per-board .c swept into TK_BOARD_SRCS. So the HAL↔kernel seam is a property of symbols, not of a separate source group — which is exactly why the I2 pull-test (§6) needs a dedicated sovereign example rather than “link the HAL group alone.”

HAL bricks (hal/ contracts + a board’s HAL-port in boards/<board>/):

  • Peripheral / mechanism bricks — each its own header, its own tk_*_init(): tk_uart · tk_dio/tk_port · tk_dio_irq (edge→IRQ) · tk_mcu.

  • The portable text console tk_console (tk_print; one .c serves every board).

  • Leaf brick — the uniform return contract tk_status_t. It lives in kernel/tk_status.h (the shared type-vocabulary home, beside tk_types.h) so the kernel’s public API can return it without a kernel→HAL edge; the HAL borrows it as a pure-type include (§2’s exception). Depended on by everything, depends on nothing.

    *(The wider _legacy HAL — tk_spi/tk_i2c/tk_adc/tk_pwm/tk_gpt/crypto/tk_wdg

    • the tk_error/DET module — is not in the minimal root. It is _legacy-only; see hal-architecture.md for what the minimal HAL keeps and drops.)*

Kernel bricks (kernel/), in dependency order — each studs onto the one before:

scheduler  ←  sync (mutex/sem/cond)  ←  higher services  ←  system features

Scheduler-without-sync is valid; sync-without-features is valid; never the reverse. Feature bricks (STACK_CHECK, MPU_GUARD, UNPRIV, ISOLATION, AFFINITY, EDF, PROFILING, INTROSPECT, TRACE, SYSVIEW) each gate on a TK_CONFIG_* flag (§4c) and compile to nothing when off. The header/symbol placement of the kernel bricks is kernel-tiers.md; this doc owns only the linkage/selection law.

Arch bricks (arch/<cpu>/): the kernel’s port to one CPU, reached only through the arch_* contract (§4f). The board↔arch division of that contract (who owns the tick, the vectors, the MPU map) is board-contract.md.

A board = a HAL-port (always) + kernel-facing glue (only on kernel boards). That split is the heart of §7: today the two are not cleanly separated in the source grouping for the Cortex-M kernel boards.

4. The stud catalog — the approved connectors

The only sanctioned ways one brick connects to another. Every one shares a property: the lower/used brick never names the higher/using brick.

(a) Callback / hook registration (inversion-of-control). The used brick exposes “register a handler”; the using brick plugs in. The canonical stud — it turns would-be glue around.

tk_dio_irq_enable_channel(cb, ctx) (edge→callback) · tk_kernel_set_idle_hook.

(b) Weak default + strong override (link-time stud). A brick ships a weak default; a higher brick optionally overrides it. Absent the override, the default stands — so the brick links alone.

tk_console_lock/tk_console_unlock (weak no-ops single-core; an SMP board overrides with a hardware spinlock) · the ALIAS_DEFAULT vector handlers in each boards/<board>/startup_*.c · the weak arch_timer_init a tick-owning board overrides.

(c) Compile-time selectors (TK_CONFIG_*). The à-la-carte switch: which bricks compile in. Each must be independently toggleable (the §6/I1 invariant).

TK_CONFIG_ENABLE_{PROFILING,EDF,AFFINITY,INTROSPECT,STACK_CHECK,MPU_GUARD,MPU_ISOLATION,TRACE,SYSVIEW} · TK_CONFIG_UNPRIV_THREADS · TK_CONFIG_FAULT_CONTAIN · TK_CONFIG_PREEMPT_MODE · TK_CONFIG_SCHED_POLICY · TK_SMP_CORES. (How a selector is paired with an arch capability into a single TK_FEAT_* gate is kernel-tiers.md §6 — stated once there.)

(d) Instance / config tables. Data-driven parameterisation — a brick configured without code coupling. The board supplies a table; the brick reads it.

boards/<board>/tk_*_cfg.h (g_port_config, the tk_dio_cfg.h channel manifest).

(e) Opaque handle + syscall (the confinement stud). The narrow, kernel-mediated interface between a confined app and the kernel — closes the confused-deputy hole. Specified in kernel-tiers.md ([rt] syscall path + kernel-owned sync handles).

(f) The arch_* contract. The kernel’s one-way stud to the CPU.

arch_context_{init,switch,start} · arch_irq_{save,restore,enable,disable} · arch_core_id · arch_ipi · arch_kernel_tick · arch_timer_init · arch_mpu_init. Its board-vs-arch ownership split is board-contract.md §4.

(g) The status contract. One uniform return type across every brick: tk_status_t (kernel/tk_status.h — shared vocabulary, borrowed by the HAL per §2’s pure-type exception). (The fuller DET/error-detail module is _legacy-only; the minimal root keeps the coarse status enum + a kernel-side kernel/tk_det.h DET hook, off by default via TK_CONFIG_ENABLE_DET.)

5. The glue anti-patterns — forbidden

Glue is anything that makes two bricks inseparable. The tells:

  1. A lower brick names a higher brick. The dependency-inversion smell. Live examples in §8. Fix: invert it into a stud (§4a).

  2. Shared mutable god-state. A global struct many bricks read/write couples them. Keep per-brick state private; connect via studs, not a shared object.

  3. Mega-init. One init() that initialises everything forces pulling every brick. Keep per-brick init; the app calls only what it uses.

  4. Mega-header. A header that includes everything makes the include graph the dependency graph. Each brick exposes a narrow header.

  5. Lumped source groups. Globbing separable bricks into one build group fuses them for the linker even if the code is clean — e.g. a board’s kernel-facing tick .c swept into the same board group as its pure HAL-port.

6. Invariants and their enforcement

The contract is only real if the build proves it. Three invariants, one mechanism:

  • I1 — Independent selection. Every TK_CONFIG_* toggles on/off without breaking another brick. If turning B off breaks A, A had glue on B.

  • I2 — Links alone. Each brick (and each layer subset) links with only its declared transitive dependencies present — nothing else. The HAL↔kernel seam: a sovereign build must reference zero kernel link symbols. (Borrowing kernel/tk_status.h is a compile-time TYPE include — it emits no link symbol — so a sovereign HAL build still satisfies this; it only needs kernel/ on the include path. See §2.)

  • I3 — One-way DAG. No brick references a symbol from a brick above it.

The intended enforcement is a minimal-build matrix — small builds, each selecting one brick / feature / layer subset, that must compile and link, so coupling becomes a build error, not a review opinion. The design (_legacy/tools/composability_matrix.sh) runs four checks: I3 static (a per-board scan that no HAL-port names a kernel symbol), I2 dynamic (a sovereign app links HAL-only, per board), I1 dynamic (each TK_CONFIG_* feature builds alone on host), and I4 (board pin/clock config validates + its generated file is fresh). The static half is _legacy/tools/composability_check.sh.

Migration status (honest). Neither tool is at root — tools/ currently holds only SEGGER/ + bin2uf2.py, and the probe examples the matrix drives (hal_probe, feature_probe) are not in the root examples/ set. So at root the matrix is a specified mechanism, not a running gate. Standing it back up (port the two scripts + add a sovereign probe + a feature probe) is the open work that turns §7 from a hand-audit into a build invariant.

7. Current state — an honest scorecard

Clean / proven:

  • The layer model and the connector vocabulary of §4 — all in use at root.

  • The TK_CONFIG_* selectors of §4c (verified in kernel/tk_config.h).

  • The confinement stud — unprivileged-thread isolation (kernel-RAM .privileged_bss, per-thread stacks); see board-contract.md §3.2 for the boards it is proven on.

  • Sovereign-capable boards exist by construction. A board with no kernel-facing .c (e.g. boards/host, boards/qemu_riscv32_virt — pure HAL-port + tk_console) references no kernel symbol.

Known glue — present at root (the retrofit was not carried into the reshape). The kernel-facing board files were, in the legacy tree, split into boards/<board>/kernel/ to keep the HAL group kernel-free. The reshaped root flattened the board directories, so that glue is live again inside TK_BOARD_SRCS:

  • boards/nrf52832_pca10040/tk_tick_nrf52.c calls arch_kernel_tick() from RTC1_IRQHandler — the §8 worked example, verbatim.

  • boards/rp2040_pico/tk_smp_rp2040.c #includes tk_kernel.h + tk_kernel_port.h and calls tk_kernel_start_this_core().

An I3 scan would flag both today. The planned resolution is not another boards/<board>/kernel/ move but a per-arch multicore tier (arch/<cpu>/<mp>/<soc>/), scoped in ADR 0002 §7 — which calls the rp2040 case out as “the invariant’s one leak, self-documented in the file.” The trap-frame boards (RISC-V) and the host are clean by construction (the arch owns the tick; no board→kernel call).

Enforcement status: I3 is designed (the static scan) but not running at root; I1/I2 likewise. Composability at root is enforced by convention + code review, with the build-invariant machinery a migration away (§6).

8. Worked example — nRF52 tick: glue → stud

Now (glue), verbatim at root: the board’s tick ISR reaches up into the kernel.

/* boards/nrf52832_pca10040/tk_tick_nrf52.c — a board HAL-port file */
void RTC1_IRQHandler(void) { ...; arch_kernel_tick((uint8_t)RTC1_IRQn); }  /* names a kernel/arch symbol */

The file cannot stand alone in a sovereign build, because it has fused itself to the kernel’s tick entry.

Target (stud, §4a): invert the direction. The HAL timer exposes a callback; the kernel — when present — registers arch_kernel_tick as that callback. The HAL-port names nothing above it.

/* HAL timer brick: exposes a stud */
void tk_timer_set_tick_handler(void (*fn)(uint32_t));
void RTC1_IRQHandler(void) { ...; if (s_tick) s_tick(RTC1_IRQn); }   /* names nothing above */

/* kernel start (only when a kernel is present): plugs in */
tk_timer_set_tick_handler(arch_kernel_tick);

Same behaviour; opposite dependency direction. No handler registered ⇒ no kernel ⇒ the timer brick still links and runs. This is the pattern k2 already uses for the DIO edge IRQ and the idle hook — the tick simply never adopted it. On the trap-frame archs the question is moot: the arch owns the timer vector, so there is no board→kernel call to invert (see board-contract.md §4 ★).

9. Open work (the path to “build without fear”)

  1. ~~Write this contract.~~ (this document)

  2. Migrate the enforcement to root: port composability_check.sh (I3 static) + composability_matrix.sh (I1/I2/I4) from _legacy/tools/, and add the sovereign hal_probe + feature_probe examples they drive.

  3. Resolve the known glue per ADR 0002 §7: move the Cortex-M kernel-facing board files (nRF52 tick, rp2040 SMP) into a per-arch multicore tier so a sovereign Cortex-M link references zero kernel symbols.

  4. Optional polish: the tick callback-inversion (§8) to give a sovereign Cortex-M app a HAL timebase.

After (2)+(3), the foundation’s state stops being a matter of belief: the build reports it, every time.