ReviewOS

home-lang/home-os

A10: Systems types in the TypeScript-derived checker

#39
Open chris opened this 8 days ago ·
8 days ago

Home's type system descends from a full TypeScript implementation — roughly 445k lines of Zig across ts_parser, ts_checker, ts_resolver, ts_lsp, and a tsc-compatible driver. That inheritance is an asset: the checker is mature, the diagnostics are good, and Home's surface syntax is already TypeScript-flavored.

It is also the constraint. A JavaScript type system has no vocabulary for what a kernel is made of. Closing that gap is tracked here, separately from codegen (#38), as milestone A10 in MASTER_PLAN §6.

Done

  • Arbitrary-width integers — u4, u6, u40, u63 (home-lang/home@4dc1ec9). A page table entry is a u40 address beside a u3 of available bits; an interrupt gate is a u128 whose fields are not byte-aligned. The failure mode was badly misleading: let nibble: u4 resolved to no type, so the binding never entered scope, and every later use reported "Undefined variable" — pointing at the use rather than the declaration. vga.home and serial.home were failing entirely on this.
  • Pointer slicing — ptr[0..len] (home-lang/home@f39fc6b). How a kernel turns a syscall's raw address into something carrying a length. Without it the only way to pass such data on was a bare pointer to a parameter that would read .len off it — which is exactly the bug it then found in shell_syscall.home.

Open

  • Layout as a type property. packed, backing types, and field bit ranges are known to the codegen but invisible to the checker, so nothing verifies that a bitfield's declared widths actually fit its backing integer. A packed struct: u64 whose fields sum to 65 bits is currently accepted.
  • Pointer provenance and volatility. *T, [*]T, []T, and volatile are matched as type-name text rather than modelled, so nothing catches indexing a pointer that carries no length.
  • Address-space and alignment constraints. align(N) is a placement note today; a checker that understood it could reject a misaligned MMIO access at compile time.
  • Integer overflow and truncation at assignment and cast sites — where a kernel silently corrupts state.

Why this is worth doing here

Every one of these was found by pointing the checker at a real kernel and reading what it said. The corpus is the specification.

Sign in to comment on this issue.