Last updated: v0.31.3.10
Note: The canonical KNOWN_ISSUES.md is in the
nitpickrepo. This is a working copy for internal tracking.
Closed in Phase 3 of the v0.31.x cycle but explicitly carried forward:
-
is unknown/== unknownoperator surface (D-18) — intentionally deferred during Phase 3; v0.31.2.4 wired the taint-tracking infrastructure (Symbol::mayBeUnknown+exprCarriesUnknownTaint), v0.31.2.10 pulled the taint intopickexhaustiveness, but no first-classx is unknown/x == unknownboolean form is wired into sema. Today the parser acceptsx == unknownand the type checker folds it to a structural equality on the literal's underlying zero, which is not the documented semantic. Revisit alongside user-facingunknownergonomics. -
unknownruntime failsafe layer for D-17 — only the compile-time taint path landed in v0.31.2.4; the runtime-only failsafe arm ("only runtime-detectable unknowns trigger the existingfailsafe(...)plumbing") is deferred until a real program exercises the path.
Closed in Phase 2 of the v0.31.x cycle but explicitly carried forward:
- Re-borrow from a
$$m dyn Tparameter — passingbonward as$$mto another call is treated conservatively: the callee binds the fat ptr to a struct alloca without setting the__borrow_param_mutmarker forb. No current fixture exercises this path; revisit if a real program demands it. - Field-level borrows of a
dyn Tstruct field — not supported; borrow the whole containing struct. - Trait inheritance / super-traits — out of scope for Phase 2.
- Associated types / associated constants — out of scope for Phase 2.
- Generic trait bounds (
func:f = T($$i T:x) where T: Trait) — out of scope for Phase 2. derivefor arbitrary traits — onlyderive(Display)is supported (v0.21.1).obj(owned trait object) — distinguishing semantics fromdynwas deferred at v0.31.1.0 (D-9 follow-on).
The items below are explicitly out of scope for the v0.25.x cycle and carried forward to v0.26.x triage:
- Closure capture for non-primitive types — defaults to BY_VALUE; capture-by-reference is currently supported only for primitive scalars.
- IR-gen path-arg lowering for
$$mparameters — the borrow checker enforces the rules but codegen still uses the existing pointer-passing convention. - Cross-module return-borrow inference — summary-based, not global; novel cross-module shapes may require explicit scoping.
- K model field-path depth — capped at 3 levels (
a.b.c); deeper paths exist in the parser but are not yet expressible in the K model.
--comptime-budgetflag — CTFE step cap is documented as configurable but the CLI flag is not exposed; the cap is a fixed compile-time constant.--trace-comptime=<funcname>flag — documented innitpick-docs/guide/comptime/debug.mdas planned; not implemented.- Comptime arrays of struct values evaluate correctly inside comptime
but cannot yet be embedded directly into IR globals; large lookup tables
should be built inside a
comptime { ... }returning the final scalar or small array.
Macros that generate code requiring a C-shim bridge (heavy FFI body generation) are deferred. Current macros support all pure-Nitpick body patterns. C-bridging code generation macros require additional codegen work planned for v0.25.x+.
| Slice | Bugs | Theme |
|---|---|---|
| v0.31.3.0 | (audit only) | Phase 4 baseline audit & decisions D-24..D-44 |
| v0.31.3.1 | bug423 – bug426 | DEF-CHAIN-RESULT chained .is_error / .value / .error off Result<T>-returning call expressions — codegen fallback for Result LLVM shape at the call-result site (D-24) |
| v0.31.3.2 | bug427 – bug430 | ARIA-029 (gc → wild) and ARIA-031 (stack → gc field) now fire on field-access shapes (@o.inner, @s.value), not just bare identifiers (D-25). Reserved codes ARIA-047/048 remain free. |
| v0.31.3.3 | bug431 – bug434 | User-defined drop method auto-dispatch — runtime-observable verification of the v0.29.2 wiring (D-26): drop body executes (bug431), self carries the binding's final field values (bug432), same-scope LIFO ordering is observable (bug433), and inner-scope drops fire before outer-scope drops (bug434). Implementation was already complete; v0.31.3.3 ratifies it with runtime tests. Minor IR-gen polish noted: passing self.<field> as a call argument directly (e.g. _exit(self.n)) fails with Unknown Nitpick type: <T>; two-step int32:v = self.n; _exit(v); is the workaround. Filed for a future surface-polish slice. |
| v0.31.3.4 | bug435 – bug437 | Pointer-typed wild RAII — wild T->:p = alloc(N); is auto-freed at scope end via emitted npk_free when use "drop.npk".*; is in scope (D-27 — the v0.29.3b split). Single-binding (bug435), reverse-order LIFO with two bindings (bug436), and opt-in-required ARIA-014 (bug437). Implemented as new DropEntry::Kind::WildPtrRaw (recognizer mirrors WildxRaw shape, dispatch loads the inner pointer from the heap slot then calls npk_free). The heap-allocated slot itself is intentionally leaked — same convention as the WildxRaw arm; per-binding slot reclamation is part of D-43/D-36 (Phase 5). |
| v0.31.3.5 | bug438 – bug440 | #[destroys_arena] surface polish (D-28). (a) Parser now accepts #[...] attributes immediately before func:name = ... inside an impl block — bug438 proves the attribute parses on an impl method AND survives into the borrow checker's per-method summary (the new ARIA-049 warning fires for an unknown param name in the impl method's attribute). (b) Multi-parameter form #[destroys_arena(a, b)] marks every named arg as destroyed at the call site — bug439 emits exactly 2 [ARIA-032] errors. (c) New ARIA-049 WARNING fires when a name in #[destroys_arena(...)] does not match any of the function's parameters — bug440 verifies one warning, no errors. Implementation: small parser hoist of #[...] parsing into the impl method loop (mirrors the top-level path) plus a matched flag on the borrow-checker's attribute-resolution loop that emits the warning when no parameter name matches. Pre-existing fixture bug324 (top-level unknown-name on a #[destroys_arena]) was reconfirmed against the new diagnostic: compile still succeeds with 0 [ARIA-032], now also emits 1 [ARIA-049]. |
| v0.31.3.6 | bug441 – bug443 | Cross-module / transitive ARIA-032 variants promoted from WARNING to ERROR (D-29). FP-rate measurement against the in-tree corpus (104 packages + the existing bug fixtures, excluding the synthetic transitive-handle ones) showed 0/484 = 0% false-positive rate, well under the 5% gate per IPC-DEC-004. Three borrow-checker emission sites were flipped from addWarning → addError in src/frontend/sema/borrow_checker.cpp: (i) escape Case A — checkHandleArenaEscape transitive_handles_ branch (returning a handle inferred from a transitively-escaping callee); (ii) escape Case B — same function, the inline pass raw wrap(a) form keyed off summary.escapes_param_arena_indices ∩ local_arenas_; (iii) destroy variant — the CallExpr handler's transitively_destroyed_arenas_ branch. The trailer "This will become an error in a future release." was removed from all three sites (verified by grep). Fixture migration: bug311/312/314/315/316/317/318/323 now reject at compile time instead of producing soft warnings — runners run_bug_tests_0301.sh, run_bug_tests_0302.sh, run_bug_tests_0304.sh switched to a new expect_compile_error helper. D-43 depth-3+ transitive verified via existing bug312 (depth 3) and the new bug441 (depth 4: tier4 → tier3 → tier2 → destroyer → HandleArena.destroy(a)). D-44 imported-extern Handle<T> visibility verified via bug442 (cross-module fail: handle allocated by an imported helper, arena destroyed, then deref triggers exactly 1 [ARIA-032]) plus bug443 (cross-module pass control: proper free-then-destroy ordering, clean compile). New: bug441_handle_transitive_destroy_depth4_fail.npk, bug442_xmod_extern_handle_visibility_fail.npk, bug443_xmod_extern_handle_visibility_pass.npk, bug442_helper.npk, run_bug_tests_03136.sh, and the FP-measurement harness measure_nitpick032_fp_v03136.sh (writes measure_nitpick032_fp_v03136.report). |
| v0.31.3.7 | bug444 – bug446 | ARIA-050 static double-free detection for manual npk_free(p) on a binding that is already tracked for scope-end auto-drop (D-30). New per-function auto_drop_bindings_ set in BorrowChecker, populated by checkVarDecl whenever a binding's region/shape matches an existing DropEntry recognizer (WildxRaw for wildx <T>:x = ..., WildPtrRaw for wild T->:p = alloc(...)) AND the current function has use "drop.npk".*; in scope (same opt-in gate the dispatch path already uses). On every npk_free(p) lowering, recordWildFree checks whether p resolves to a name in the set and, if so, emits ARIA-050: manual npk_free of binding 'p' would double-free at scope-end auto-drop. The set is saved/restored around nested function bodies and cleared at each per-function boundary so callee state never bleeds. Opt-out: simply omit use "drop.npk".*; — bug446 verifies the legacy manual-management flow compiles clean with no ARIA-050. Fixtures: bug444 (wild T->:p = alloc(...) + manual npk_free(p) → 1 ARIA-050), bug445 (wildx <T>:x = ... + manual free of the inner arena ptr → 1 ARIA-050), bug446 (no use "drop.npk" import, manual npk_free is the user's responsibility → clean). Runner: run_bug_tests_03137.sh (3/3). |
| v0.31.3.8 | bug447 – bug450 | Borrow-checker polish verification (D-31): flow-sensitive release across if/else arms + implicit two-phase borrows within a single call. Empirical characterisation of the existing borrow checker (LifetimeContext::merge union semantics at src/frontend/sema/borrow_checker.cpp L67-200; checkPathConflict honouring LoanPhase::RESERVED at L5121-5167) showed BOTH deferred items are already satisfied by the current implementation: (a) when each arm declares a $$m borrow in its own scope, the union-merge of empty post-arm active_loans/path_loans sets correctly leaves the host writable; (b) b.write(raw b.read()) style nested calls compose $$i then $$m on the same receiver without ARIA-020/023 because the inner shared borrow is fully released (off-the-stack) before the outer mutable borrow is established. Outer-scope live loans (bug199 / bug450) are still rejected — two-phase is in-call only. No source changes; v0.31.3.8 ratifies the working behaviour with regression fixtures. Fixtures: bug447 (symmetric in-arm $$m borrows, post-if write to host PASSES), bug448 (outer-scope $$m held across if/else, post-if write FAILS with ARIA-026), bug449 (b.write(raw b.read()) PASSES — implicit two-phase compose), bug450 (outer $$i then c.bump(...) FAILS — two-phase doesn't extend across statements, mirrors bug199). Runner: run_bug_tests_03138.sh (4/4). |
| v0.31.3.9 | bug451 – bug454 | Runtime array out-of-bounds check at every dynamic-index GEP site (D-32, the v0.19.0 deferred gap). New shared helper npk::emitArrayBoundsCheckImpl (include/backend/ir/array_bounds_check.h + body in src/backend/ir/ir_generator.cpp) emits 0 <= idx < size → bc.fail → failsafe(99) + exit(99) / bc.ok continue. Wired into FIVE codegen sites that previously emitted CreateInBoundsGEP with a non-constant index: (1) getBorrowAliasPointer IndexExpr branch in ir_generator.cpp (the v0.19.0 $$m arr[i] borrow path); (2) IRGenerator's struct-field array READ at the index-expr fallback (obj.field[i]); (3) IRGenerator's struct-field array WRITE at the assignment LHS (obj.field[i] = X); (4) IRGenerator's nested struct-field-array WRITE on a member (obj.field[i].member = X); (5) IRGenerator's multi-dim read (m[i][j] → one check per dimension). ExprCodegen mirrors are wired in codegen_expr_compound.cpp for the single-dim identifier read, multi-dim read, and struct-field read paths. Existing inline read-path check at ir_generator.cpp ~L13216 is now gated by npk::g_bounds_checks_enabled && bounds_check_safe.count(expr) == 0 so the Z3-proven-safe set still elides the check. New CLI flag --no-bounds-checks (default OFF, i.e. checks ON) clears the global toggle for release builds; emitted IR contains zero bc.fail/bc.ok blocks under the flag (verified by the runner's IR-grep step). Constant in-range indices are elided cheaply in the helper itself. Fixtures: bug451 (dynamic OOB $$m arr[i] write → exit 99), bug452 (struct-field array OOB read b.nums[i] → exit 99), bug453 (multi-dim OOB outer index m[i][j] → exit 99), bug454 (--no-bounds-checks smoke: in-bounds program still exits 0 and emitted IR has no bc.fail block). Runner: run_bug_tests_03139.sh (6/6 including the two flag-mode passes). |
| v0.31.3.10 | n/a | pin_address_stable.k formal K proof landed (D-33, two-and-a-half cycles overdue from v0.27.4). The proof file already existed (3 base claims authored in v0.27.4) and was already wired into k_semantics_proofs via the *.k glob in k-semantics/run_k_proofs.sh, but had never been explicitly ratified in a release. This slice extends the proof with a depth-4 gc_cycle chain claim (mirrors v0.31.3.6 D-44's depth-4 transitive cross-fn stress at the K-proof level) and formally lands the file. Total claims now 4: (1) gc_cycle ; => .K preserves <env>/<store>/<pinned-hosts>; (2) deref-after-1-cycle reads same V from same L; (3) deref-after-2-cycles same; (4) deref-after-4-cycles same — generalises to any finite chain. No source changes; no fixtures (proof-only slice). K proofs runner now reports 11/11 PASS including the extended ARIA-PIN-ADDRESS-STABLE-PROOFS module. |
| Slice | Bugs | Theme |
|---|---|---|
| v0.31.2.0 | (audit only) | Phase 3 baseline survey & decisions D-13..D-23 |
| v0.31.2.1 | bug379 – bug382 | const outside extern rejected (ARIA-044); fixed opportunistic comptime fold; 36-file stdlib const → fixed sweep |
| v0.31.2.2 | bug383 – bug386 | NIL/NULL safety guard mirrored into checkAssignment (statement-level =) — D-15 gap close |
| v0.31.2.3 | bug387 – bug393 | tbb ERR sticky verified across compare / bitwise ops (D-16 / D-16a) |
| v0.31.2.4 | bug394 – bug399 | Symbol::mayBeUnknown taint + exprCarriesUnknownTaint walker; unknown-without-ok() rejected (ARIA-045) — D-17 / D-17a |
| v0.31.2.5 | (collapsed) | D-18 is unknown / == unknown operator surface deferred per slice-plan ratification |
| v0.31.2.6 | bug400 – bug402 | fixed T:x × generic monomorphisation regression — D-19 verified, no source changes |
| v0.31.2.7 | bug406 – bug409 | func:f = NIL(...) { ... }; wraps to Result<NIL> — D-21 verified, no source changes; DEF-CHAIN-RESULT logged in-flight |
| v0.31.2.8 | bug410 – bug413 | fail(code) ⇒ .value == NIL for Result<NIL> / Result<Optional<T>>; sema gate relaxed (ARIA-046); var-init Optional double-wrap fix |
| v0.31.2.9 | bug414 – bug417 | fixed × Drop verification — Drop still fires at scope exit; no source changes |
| v0.31.2.10 | bug418 – bug422 | pick exhaustiveness for special values: Optional NIL, Pointer NULL, tbb ERR (regression), unknown-tainted selector — D-23 |
| v0.31.2.11 | (no new bugs) | Phase 3 close — guide/special-values/ cookbook, KNOWN_ISSUES refresh, cycle audit |
| Slice | Bugs | Theme |
|---|---|---|
| v0.31.1.0 – v0.31.1.6 | bug363 – bug370 | dyn T surface scaffolding (local var, struct field, fn arg, heterogeneous branch, no-impl diagnostic ARIA-043, two-method dispatch) |
| v0.31.1.7 | bug371 | Probe C $$i dyn T local borrow + dispatch |
| v0.31.1.8 | bug372, bug373 | impl-method $$m self lowering; $$m dyn T local borrow mutation |
| v0.31.1.9 | bug374 | $$m dyn T parameter coercion (call-site + callee-side ABI) |
| v0.31.1.10 | bug375 – bug378 | Probe D regression slice: dyn-borrow source-side conflict rules (ARIA-019/023/026 fire uniformly for dyn T borrows) |
| Slice | Bugs | Theme |
|---|---|---|
| v0.25.0 | bug173 – bug174 | TILL body borrow checking, FAIL dispatch |
| v0.25.1 | bug175 – bug178 | defer body borrow tracking; early-exit leak audit |
| v0.25.2 | bug179 – bug183 | Multi-dim and nested array borrow paths |
| v0.25.3 | bug184 – bug189 | Deep struct field paths and ptr->field |
| v0.25.4 | bug190 – bug194 | Inter-procedural parameter intent and return-borrow lifetime |
| v0.25.5 | bug195 – bug199 | Two-phase borrows; $$m self in trait impls |
| v0.25.6 | bug200 – bug204 | Closure capture borrows; multi-await polish; ARIA-023/026 secondary spans |
| v0.25.7 | (no new bugs) | K core tests 143/144/145; guide/borrow/ cookbook; cycle audit |
| ID | Description | Resolution | Version |
|---|---|---|---|
| (unnamed) | string:x = comptime("...") segfaulted at runtime — COMPTIME_EXPR codegen emitted raw i8* instead of NitpickString struct |
Construct struct.NpkString {data, length} global mirroring string-literal codegen |
v0.24.7 |
| (unnamed) | inferComptimeExpr() failed on intrinsic chains like @typeInfo(T).fields.x.type_name |
Refactored to evaluate-first; only fall back to inferType() when evaluation fails |
v0.24.7 |
| ID | Description | Resolution | Version |
|---|---|---|---|
| MACRO-003 | Macro variable hygiene | gensym/cloneAST per call site | v0.23.2 |
| (unnamed) | case RETURN: dropped from checkStatement() in v0.23.5 |
Restored in ba66d8a |
v0.23.6 |
| ID | Description | Resolution | Version |
|---|---|---|---|
| POLISH-001 | eprint/eprintln not wired in type checker/codegen |
Implemented; stdlib builtins | v0.22.2 |
| POLISH-002 | .npk extension rejected by module resolver |
isValidSourceFile() accepts both .npk and .npk |
v0.22.2 |
| POLISH-003 | npk_arg(i) broken ABI |
Replaced with get_argc/get_argv builtins |
v0.22.3 |
| POLISH-004 | File extension conventions undocumented | use_import.md File Extension Conventions section |
v0.22.6 |
| POLISH-006 | pick on integer values untested |
Regression tests added; already worked | v0.22.4 |
| POLISH-007 | Bitwise ops on int32 variables untested | Regression tests added; already worked | v0.22.4 |
| POLISH-008 | Reserved keyword as var name → cryptic error | Parser emits friendly message with suggestions | v0.22.6 |
| POLISH-009 | \xNN / \u{NNNN} escape sequences unsupported |
Added to all three string scanners in lexer | v0.22.5 |
| POLISH-010 | "type X but expects X" multi-module import clash | checkFuncDecl() in-place symbol update |
v0.22.2 |
| POLISH-011 | break/continue not in loop bodies |
Already implemented end-to-end; tests added | v0.22.3 |
| POLISH-012 | pass n; not counted as variable use |
collectIdentifiers() PASS case added |
v0.22.1 |
| POLISH-013 | print() vs C stdio buffering interop |
ffi_advanced.md Stdio Buffering section |
v0.22.1 |
| POLISH-014 | while body not scanned by unused-var checker |
collectIdentifiers() WHILE+6 cases added |
v0.22.1 |
| — | isValidNitpickFile() pre-rebrand name |
Renamed to isValidSourceFile() |
v0.22.7 |
| ID | Description | Resolution | Version |
|---|---|---|---|
| — | vec9 dynamic indexing throws std::runtime_error at runtime |
ICmpEQ type mismatch fixed in ir_generator.cpp; read and write paths now cast loop index to i32 before select loop |
v0.20.5 |
| — | UNUSED_FUNCTION and EMPTY_BLOCK warnings not emitted |
Warning pass implemented | v0.20.0 |
| — | %error/%warning directives not implemented |
Preprocessor directives implemented | v0.20.1 |
| — | Struct interpolation in template literals not supported | Display trait and struct interpolation implemented |
v0.20.2 |
| — | comptime evaluator Step 7 (struct comparison) stub |
Const evaluator Step 7 complete | v0.20.3 |
| — | Closure validateLifetimes stub (no escape detection) |
Closure lifetime validation implemented | v0.20.4 |
| — | optional<T> not in type system |
optional<T> with safe navigation (?.) and null coalescing (`? |
`) implemented |
| ID | Description | Resolution | Version |
|---|---|---|---|
| bug072 | Non-pub helper called from pub func: crashes codegen |
Intra-module calls work regardless of visibility | v0.19.3 |
| bug073 | ahget on missing key segfaults |
Returns zero; always check ahtype(h,k) >= 0 |
v0.19.3 |
| bug074 | @func_name as call argument: type-checker mismatch |
Assign to lambda variable first, then pass | v0.19.3 |
| bug075 | Variables declared before loop() inaccessible after exit |
Pre-loop variables remain in scope after loop | v0.19.3 |
| bug076 | Result<T> in arithmetic emitted misleading error |
Error message improved | v0.19.3 |
| bug077 | Large pick (30+ arms) triggers codegen segfault | Chunked codegen for large pick statements | v0.19.3 |
| ID | Description | Resolution | Version |
|---|---|---|---|
| — | pass(extern_returning_struct()) required temp variable |
Direct pass of extern-returned struct now works | v0.19.1 |
| ID | Description | Resolution | Version |
|---|---|---|---|
| BUG-06 | _test filename segfault |
Fixed module name generation | v0.13.0 |
| BUG-09 | Computed fixed constants zeroed on import |
Fixed constant folding codegen | v0.13.0 |
| STUBS | 12 stub implementations across compiler/runtime | All replaced with real implementations | v0.13.1 |
| FEAT-06 | Multi-file linking not supported | Implemented | v0.13.2 |
| FEAT-10 | Extern block ≤7 limit | Removed limit | v0.13.2 |
| — | @func_name function pointer syntax broken |
Trampoline wrapper generation | v0.13.6 |
| — | ahash missing ahdelete, ahhas, ahclear, ahkeys |
Full implementation with tombstone support | v0.13.5 |
| — | Variadic/rest/spread not implemented | ..? (variadic/rest) and ..^ (spread) operators |
v0.13.5 |
| ID | Description | Fixed In |
|---|---|---|
| BUG-14 | Float != returned false when comparing NaN |
v0.4.6 |
| BUG-17 | LLVM module verifier was commented out | v0.4.6 |
| #16–#27 | Various float/integer/ABI crashes | v0.1.0–v0.2.x |
| BUG-008–011 | ?! literals, .error type, tbb32 compare, field borrow |
v0.4.x |
(none — all high-severity issues resolved as of v0.20.3)
-
Nested module function calls (A→B, both pub) (Medium): May trigger GC OOM in pathological cases. Avoid deep pub-pub chains across modules in tight memory environments. v0.21.5 investigation: 4-level chains and 16-leaf hub graphs compile and run cleanly under 70 MB; the failure mode appears only on much larger or cyclic graphs and could not be reproduced on small/medium fixtures. Floor regression test:
tests/bugs/bug104_pub_pub_chain_pass.npk(4-level chain). -
pickexhaustiveness foruint64(Medium):uint64is treated as an infinite domain (its max value exceedsint64_t). A(*)wildcard is always required.
-
flt32 ABI (Low):
flt32passes asdoubleat the C ABI boundary. C shims must acceptdoubleparams and cast internally. -
String ABI is asymmetric (Low):
stringparams →const char*in C.stringreturns →NitpickString {char*, int64_t}by value (not pointer). -
Extern pointer returns (Low):
{ i1, ptr }optional wrapper can corrupt struct fields. Useint64for handle types in extern blocks. -
Negative constants imported via— Resolved in v0.60.8. Module-leveluseare zeroedconstis now NITPICK-044 (reserved forexternblocks only). The correct keywordfixedcorrectly imports negative, binary-expression, and string constants across module boundaries. Workaround no longer needed. Regression suite:tests/modules/const_import/.
ifrequires parentheses:if (cond) { }- Control flow blocks have no trailing semicolons:
loop(...){},pick(...){},if(...){}etc. - Bitwise operators (
&,|,^) require unsigned types pick()requires a(*)wildcard case for types with infinite domains (e.g.string,uint64); forint32,uint32,int64,int8,int16, and alltbb*types, range arms are tracked and(*)is only needed if the range arms do not cover all valuesNILfor non-extern void returns;voidonly in extern blocksloop/tilliteration variable is$(reserved — cannot be reused in loop body)fixednotconstfor immutable bindings;constonly in extern blocks- Reserved names (cannot use as variable/parameter):
max,end,raw,ok,is,stream,limit,binary,pipe,process,debug,write
- No threading, process spawning, signals, mmap, or native FFI
- File I/O requires WASI-compatible runtime
- 24/24 CTest suites passing (all CTest registered tests pass)
- K core: 139/139 (k_semantics_core test) — up from 127 (v0.21.5: 127, v0.21.6 adds tbb8/16/64 + async/await tests)
- K proofs: 10/10 (k_semantics_proofs test)
- bug_tests_v0216: 2/2 (bug105 tbb variants, bug106 async/await)
- 0 genuine failures
K now formalizes all four TBB types (tbb8, tbb16, tbb32, tbb64) with arithmetic
and ERR sentinels. Remaining type lattice gaps (int128, flt arithmetic, etc.) are
documented in k-semantics/SEMANTIC_GAPS.md.
K now models async func: declarations and await (synchronous model). True
coroutine frame semantics (suspension/resume) remain unformalized. See
k-semantics/SEMANTIC_GAPS.md.
103+ ecosystem packages in nitpick-packages. Standard library: 57 modules (13 pure, 20 nitpick-libc, 24 FFI).
Nitpick's integer arithmetic uses llvm.sadd.with.overflow intrinsics. Overflow is replaced with an Unknown sentinel (INT32_MAX for int32). This is intentional Layer 1 Safety — overflow is detected, not undefined behavior.
Use TBB types for arithmetic where overflow detection with error propagation is needed — TBB types propagate to ERR state via sticky error semantics.
IEEE 754 compliance, energy conservation (Störmer-Verlet), determinism, TBB sticky errors, field identities, type casting precision, catastrophic cancellation, large integers (int1024), overflow/underflow boundaries.
Native Nitpick functions consistently wrap their return types in Result<T>, forcing the developer (or agent) to unpack them safely with raw or handle the error. However, extern functions from C-FFI do not undergo this conversion; they return their raw scalar types (e.g., int32) directly.
Because FFI functions and native functions look syntactically identical at the call-site, this inconsistency completely violates the "things don't change based on context" philosophy. Developers and agents are forced to manually track the origin module of every function to know whether the raw keyword is forbidden (FFI) or mandatory (Native).
The original design specifications mandated that the FFI layer perform an automatic conversion to Result<T> to unify the behavior across the board. This conversion is currently missing and must be implemented in a future roadmap cycle to restore call-site consistency.
The v0.60.x release series introduced strict visibility (pub) and scoped imports (use "file".*, use "file" as X).
As a result of this architectural hardening, a significant portion of the legacy integration tests (bug_tests_v02xx through bug_tests_v03xx) in the CTest suite now fail to compile. The common failures are:
Type 'X' is not public and cannot be used outside its defining module. Add 'pub' to its declaration.Undefined identifier: 'Y'(arising from the transition away from implicit wildcard imports). These failures are expected and represent the legacy test corpus violating the new compiler rules. A future slice will need to mass-migrate thetests/bugs/corpus to comply with the v0.60 module system.
The formal K semantics tests currently emit parse errors (unexpected token ')]' following token ':CfgPred') due to syntactic drift between the formal K model and the current Nitpick parser. This remains a known issue to be resolved in a future formal verification sprint.
During v0.60 integration, it was discovered that npkc was silently ignoring trailing && arguments because it only compiled the first input file. With multi-file support in v0.60, npkc began interpreting && as a source file and crashing. The tests/CMakeLists.txt file has been updated to wrap these commands in sh -c "...", fixing 65 false-negative tests that were silently passing without running.
Nitpick strictly enforces that all non-NIL expressions must be explicitly used, assigned to a discard variable (_), or explicitly dropped. This ensures that operations with side effects (like returning a Result<T> that must be checked, or values that are allocated) are not silently ignored.
When resolving unused value errors, it is important to distinguish between drop and discard, as they serve different purposes:
drop(_?is shorthand): Used for expressions or function return values. When you call a function and want to explicitly ignore its return value (e.g.,_? println("hello");), you usedrop(_?).discard(_~is shorthand): Used for parameters or variables that are declared but unused. If you have a variablexthat you don't read from, you can mark it as discarded (e.g.,_~ x;) to suppress unused variable warnings.
Using discard on an expression or drop on a variable is syntactically invalid and will be rejected by the compiler.