ReviewOS

home-lang/home-os

A2 complete: typecheck gate green at 39/39 — and what it found

#40
Open chris opened this 9 days ago ·
9 days ago

Milestone A2 (MASTER_PLAN §6) asked for "the full type system checks the MVK file-set with zero escape-hatch holes", with a diagnostics bar of file:line:col, expected/found types, and a suggested fix.

Done: scripts/typecheck.sh reports 39/39 Appendix A files with zero type errors, gated on every commit.

The headline finding

The Home compiler already shipped a checker meeting that bar — home check, with proper locations and carets. Nothing in this repository had ever run it. First measurement: 35/39.

That is the third time in Phase 0 the gap turned out to be measurement rather than capability, after build.sh's silent fallbacks (#24) and the stub register that no CI job enforced (#25). Worth stating as a pattern: this project's recurring failure mode is not missing work, it is unmeasured work.

The last four files needed compiler fixes, not kernel fixes

Each had been silently mis-shaping programs rather than merely failing to check them.

FixUpstreamEffect
Arbitrary-width integers (u4, u6, u40)home-lang/home@4dc1ec935 → 37
if-expression branches may hold statementshome-lang/home@f39fc6b37 → 39
Bindings survive a failed inference″″
Pointer slicing ptr[0..len]″″

The worst was the parser. An if-expression branch in brace form was parsed with expression() — exactly one expression. A branch containing a statement left the parser mid-block, and the following expect(RightBrace) consumed the brace closing the enclosing function. No error was reported. The AST for a minimal repro had 4 top-level statements instead of 2: the let binding vanished and every statement after it was hoisted to module scope.

So in vmm.home the checker was right — the function genuinely never declared pdpt. Fifteen "Undefined variable" errors, none of them at the cause.

Real kernel bugs the gate found

  • mvk_poc.home declared puts(s: int) and called it with a string literal — in the file that is our boot proof.
  • shell_syscall.home passed bare *u8 pointers to parameters typed []const u8, so the callee would have read a length from whatever followed in memory (#a5dac98).
  • var pipe_fds: [2]u32 was uninitialized, and on the cmd_count == 1 path the SYS_PIPE call never runs while the code below still reads pipe_fds[0] — a file descriptor made of stack garbage.
  • socket.home called tcp.tcp_accept() and declared a tcp.TCPConnectionInfo; neither existed anywhere in the tree (fixed in #21f5fdc).
  • scheduler.home defined scheduler_wake twice.

Follow-on work for the type system is tracked in #39.

Sign in to comment on this issue.