Summary

A comprehensive inventory of documentation holes surfaced during the Game of Life agent run (same run that produced #514, #515, #516, #517, and #518). Twelve items, roughly ordered by how much debugging time the gap cost. Some have been partially addressed in PR #518; the rest are scoped here as follow-up work.

The agent's own framing for why this matters:

The skill file does an excellent job of describing what each language construct and standard library function is, and a less thorough job of describing what each of them costs and what their edge cases are. For a language that is explicitly designed for LLMs to write rather than humans, this emphasis is almost exactly backwards — humans are good at extrapolating from examples but bad at allocating mental budget for unstated edge cases, and LLMs are the opposite.

Status legend

• ✅ Addressed in PR SKILL.md documentation sweep + bug tracking from Game of Life agent run (#513) #518
• 🔶 Partial — short version in SKILL.md documentation sweep + bug tracking from Game of Life agent run (#513) #518, deeper treatment deferred
• ⬜ Not yet addressed; deferred to a follow-up PR

Gaps

1. 🔶 Closure capture rules — what types are capturable, what happens during compilation

   • PR SKILL.md documentation sweep + bug tracking from Game of Life agent run (#513) #518: documented which types are capturable today (Closures capturing heap-allocated values produce invalid WASM (nested-closure case is a narrow instance) #514 primitive-only limitation)
   • Deferred: "how closures are compiled" (internal representation, lifetime rules)

2. ⬜ Allocation behaviour of standard library operations. The skill file documents signatures but is nearly silent on which stdlib functions allocate. Examples: int_to_nat allocates an Option<Nat> per call (agent's 14,400 hidden allocations per generation); abs is a primitive with no heap cost; array_append appears to copy (O(n²) over a full build); string_concat / string_join allocation patterns are undocumented; whether string literals are deduplicated is unknown. Proposed fix: allocation-cost annotation convention across stdlib entries.

3. 🔶 Runtime limits: heap size, GC behaviour, call stack, tail calls

   • PR SKILL.md documentation sweep + bug tracking from Game of Life agent run (#513) #518: Known Bugs table points at GC collect itself faults with out-of-bounds memory access under sustained allocation pressure #515 (GC collect fault), Tail-call optimization missing: deep recursion blows the WASM call stack #517 (no TCO)
   • Deferred: explicit "runtime model" section — current heap cap ~1.5MB, GC runs only on allocation failure, no user knob for memory size, no TCO so recursion depth is limited

4. 🔶 String handling

   • PR SKILL.md documentation sweep + bug tracking from Game of Life agent run (#513) #518: escape-sequence table (\n / \t / \r / \0 / \\ / \" / \u{XXXX}); unsupported escapes listed; UTF-8 literals work
   • Deferred: string_length semantics (byte count vs grapheme count vs code points); string_chars with multi-byte sequences; encoding guarantees across all string ops

5. ⬜ Arithmetic semantics

   • Nat subtraction: verified empirically to silently wrap to negative i64 (let @Nat = 0 - 1; nat_to_int(...) == -1). The Nat type is refinement-only at checker time; no runtime bounds check. This is a real safety observation, not just a doc gap.
   • Nat division by zero: traps with raw wasm trap: integer divide by zero (no Vera diagnostic — see Runtime traps need Vera-native diagnostics, not raw wasmtime stack traces #516).
   • Int overflow: not documented (likely WASM wrap semantics).
   • Int / Nat mixing: implicit or explicit conversion? Not stated.
   • Proposed fix: dedicated "Arithmetic edge cases" section.

6. ⬜ Standard library return-type conventions. array_length returns Int not Nat; array_range(0, n) takes Int parameters even though callers usually hold a Nat. These asymmetries confuse callers. Proposed fix: short "type conventions" note explaining the rationale (indices can go out-of-range; length participates in arithmetic; etc.).

7. 🔶 Let scoping inside branch expressions

   • PR SKILL.md documentation sweep + bug tracking from Game of Life agent run (#513) #518 (implicit via closure docs): block scope explained for closures
   • Deferred: explicit statement that let bindings inside if/else/match arms are scoped to the arm; the slot-shift-on-shadowing rule as a principle, not an inference from examples

8. ⬜ Refinement types: practical conversion patterns. The skill file mentions refinement types like { @Int | @Int.0 >= 0 } but not how to produce a refined value from an ordinary one, or how to exploit refinement evidence to avoid Option allocations. Proposed fix: "patterns for converting between types with refinement evidence" section.

9. ⬜ Tier 3 (runtime) contract check cost. Skill explains the three tiers but not what a Tier-3 runtime check actually compiles to. Agents writing hot loops need to know whether a requires(@Int.0 >= 0) is a single branch or something more expensive. Proposed fix: "Tier 3 implementation" note.

10. ✅ Empty array literals — addressed in PR SKILL.md documentation sweep + bug tracking from Game of Life agent run (#513) #518 with an explicit [] example and type-inference rules.

11. ⬜ Array in-memory representation. For allocation math, agents need to know whether an Array<Bool> of size 40 is ~5 bytes (bit-packed), ~40 bytes (byte-aligned), or ~320 bytes (word-aligned). Currently undocumented. Proposed fix: per-element memory cost per element type, as a stdlib annotation.

12. ✅ "Pure" helpers and capture — addressed in PR SKILL.md documentation sweep + bug tracking from Game of Life agent run (#513) #518 via the closure known-limitation and the heap-capture root-cause doc; the agent's workaround pattern is now explicit.

Scope of follow-up work

Items 2, 5, 6, 8, 9, 11 (and the deferred parts of 1, 3, 4, 7) are a cohesive follow-up PR: every one is a 1–3 paragraph addition or a column in an existing table. Estimated total: ~400 lines of SKILL.md additions.

Items 2 and 11 are the largest (per-stdlib annotations). They might warrant their own PR if we want to preserve PR review velocity.

Not in scope

• Fixing the underlying compiler bugs (those are Closures capturing heap-allocated values produce invalid WASM (nested-closure case is a narrow instance) #514, GC collect itself faults with out-of-bounds memory access under sustained allocation pressure #515, Runtime traps need Vera-native diagnostics, not raw wasmtime stack traces #516, Tail-call optimization missing: deep recursion blows the WASM call stack #517 and the ROADMAP campaign).
• Restructuring SKILL.md sections — pure additions where possible.