diff --git a/lib/ww/ast.ww b/lib/ww/ast.ww
index 163b7b36..0d771241 100644
--- a/lib/ww/ast.ww
+++ b/lib/ww/ast.ww
@@ -149,7 +149,7 @@ export fn newnode(k: nkind, file: str, line: i32, col: i32) *node = {
 
 // ---- printer ----------------------------------------------------------
 
-fn nkname(k: nkind) str = {
+export fn nkname(k: nkind) str = {
 	if (k == nkind.N_NONE)      { return "none"; };
 	if (k == nkind.N_INTLIT)    { return "int"; };
 	if (k == nkind.N_FLOATLIT)  { return "float"; };
diff --git a/selfhost/cmd/w6c/main.combined.ww b/selfhost/cmd/w6c/main.combined.ww
index d80022b2..23574d86 100644
--- a/selfhost/cmd/w6c/main.combined.ww
+++ b/selfhost/cmd/w6c/main.combined.ww
@@ -4569,7 +4569,7 @@ export fn newnode(k: nkind, file: str, line: i32, col: i32) *node = {
 
 // ---- printer ----------------------------------------------------------
 
-fn nkname(k: nkind) str = {
+export fn nkname(k: nkind) str = {
 	if (k == nkind.N_NONE)      { return "none"; };
 	if (k == nkind.N_INTLIT)    { return "int"; };
 	if (k == nkind.N_FLOATLIT)  { return "float"; };
@@ -6985,6 +6985,7 @@ package wcc;
 
 import os;
 import tok;
+import strconv;
 
 type checker = struct {
 	tc:       *tctx,
@@ -8310,10 +8311,17 @@ fn tinfofornode(c: *checker, n: *node) *tinfo = {
 };
 
 // unifyarith — usual-arithmetic-conversion analogue at the AST-tnode
-// layer. Mirrors cstage cmd/wcc/check.c:580-596 `unify_arith`. The
-// trailing typeeq fallback covers same-typed operands; mismatched typed
-// pairs silently return ltn (cstage flags the same shape — wwstage's
-// checker stays silent here per existing discipline).
+// layer. Mirrors cstage cmd/wcc/check.c:580-596 `unify_arith` and harec
+// ref/harec/src/types.c type_promote. Trailing `return ltn` covers
+// mismatched typed pairs; cstage flags the same shape — wwstage's
+// checker stays silent here per existing discipline.
+//
+// Nil-on-valid classification (5-lite-b #34, A.6.2.1c #24): both ltn
+// and rtn can be nil when an operand was an inherent-IDENT bail
+// (exprtype N_IDENT arm L1596-1599 — SK_USE module ref or pseudo-
+// builtin callee with sym.decl == nil; #19 retires these as
+// dedicated AST kinds). Propagation, not silent gap — asserttyped
+// gates those idents at the consumer layer.
 fn unifyarith(c: *checker, ltn: *node, rtn: *node) *node = {
 	let lu: bool = isuntypedint(ltn) || isuntypedfloat(ltn);
 	let ru: bool = isuntypedint(rtn) || isuntypedfloat(rtn);
@@ -8331,6 +8339,9 @@ fn unifyarith(c: *checker, ltn: *node, rtn: *node) *node = {
 		if (isassignable(c, ltn, rtn, &conf)) { return ltn; };
 	};
 	if (typeeqast(ltn, rtn)) { return ltn; };
+	// Mismatched typed pair — return ltn so the binop stamps something;
+	// 5-lite-b: the trailing nil-on-mismatch shape was eliminated when
+	// the helper was split out of binoptype.
 	return ltn;
 };
 
@@ -8372,13 +8383,18 @@ fn binoptype(c: *checker, e: *node) *node = {
 	    op == tkind.TK_AND || op == tkind.TK_OR) {
 		return mktname(c, "bool");
 	};
+	// Unreachable for valid input: op is one of TK_PLUS/MINUS/STAR/
+	// SLASH/PERCENT/AMP/PIPE/CARET/LSHIFT/RSHIFT/EQ/NEQ/LT/LE/GT/GE/
+	// AND/OR per parser invariant (lib/ww/parse/expr.ww binary-op
+	// table); all are handled above. 5-lite-b #34.
 	return nil;
 };
 
 // unoptype — derive the result tnode of an N_UN unary expression. Mirrors
-// cstage cmd/wcc/check.c:642-687 `cunop`. The slice/str .len/.cap
-// pseudo-field address-of widening to *i64 mirrors check.c:672-682
-// directly — its purpose is documented at the cstage site.
+// cstage cmd/wcc/check.c:642-687 `cunop` and harec ref/harec/src/types.c
+// type_promote. The slice/str .len/.cap pseudo-field address-of widening
+// to *i64 mirrors check.c:672-682 directly — its purpose is documented
+// at the cstage site.
 fn unoptype(c: *checker, e: *node) *node = {
 	let op: tkind = e.op;
 	let opt: *node = exprtype(c, e.lhs, nil);
@@ -8386,9 +8402,18 @@ fn unoptype(c: *checker, e: *node) *node = {
 	if (op == tkind.TK_NOT)   { return mktname(c, "bool"); };
 	if (op == tkind.TK_TILDE) { return opt; };
 	if (op == tkind.TK_STAR) {
+		// opt nil here means the operand was an inherent-IDENT bail
+		// (exprtype N_IDENT arm L1596-1599 — SK_USE / pseudo-builtin
+		// sym.decl == nil — or another helper's nil propagation);
+		// 5-lite-b #34, A.6.2.1c #24. The `u == nil` post-resolvealias
+		// check was eliminated here — unwrapbang(non-nil) returns
+		// non-nil (parser invariant N_TBANG.lhs always set) and
+		// resolvealias passes through non-nil unchanged (L513
+		// `for (cur != nil)` only exits via `return cur` or `return n`).
 		if (opt == nil) { return nil; };
 		let u: *node = resolvealias(c, unwrapbang(opt));
-		if (u == nil) { return nil; };
+		// Invalid input (non-pointer dereference); cstage errors at
+		// cmd/wcc/check.c:660. 5-lite-b #34.
 		if (u.kind != nkind.N_TPTR) { return nil; };
 		return u.lhs;
 	};
@@ -8412,23 +8437,33 @@ fn unoptype(c: *checker, e: *node) *node = {
 				};
 			};
 		};
+		// opt nil → propagation from inherent-IDENT bail (5-lite-b
+		// #34). Generic &expr widens to *opt; without opt we can't
+		// synthesize the pointer node.
 		if (opt == nil) { return nil; };
 		let pp: *node = newnode(nkind.N_TPTR, "", 0, 0);
 		pp.lhs = opt;
 		return pp;
 	};
+	// Unreachable for valid input: op is one of TK_MINUS/PLUS/NOT/
+	// TILDE/STAR/AMP per parser invariant (lib/ww/parse/expr.ww unary
+	// op set); all are handled above. 5-lite-b #34.
 	return nil;
 };
 
 // indexresult — derive the result tnode of an N_INDEX expression.
-// Mirrors cstage cmd/wcc/check.c:870-894. Slice/array → elem; str →
-// u8; `*[N]T` decays to T (pointer-to-array); `*[]T` does NOT decay
-// (yields []T via the generic *U → U fallback — Hare-faithful, a
-// pointer-to-slice is a 1D array of slices, not of T); generic *T → T.
+// Mirrors cstage cmd/wcc/check.c:870-894 and harec ref/harec/src/types.c
+// type_promote dispatch. Slice/array → elem; str → u8; `*[N]T` decays
+// to T (pointer-to-array); `*[]T` does NOT decay (yields []T via the
+// generic *U → U fallback — Hare-faithful, a pointer-to-slice is a 1D
+// array of slices, not of T); generic *T → T.
 fn indexresult(c: *checker, e: *node) *node = {
 	let basetn: *node = exprtype(c, e.lhs, nil);
 	let _idx: *node = exprtype(c, e.rhs, nil);
 	let u: *node = resolvealias(c, unwrapbang(basetn));
+	// basetn nil → propagation from inherent-IDENT bail at exprtype
+	// N_IDENT arm L1596-1599 (5-lite-b #34, A.6.2.1c #24).
+	// unwrapbang(nil)=nil and resolvealias(nil)=nil pass through.
 	if (u == nil) { return nil; };
 	if (u.kind == nkind.N_TSLICE) { return u.lhs; };
 	if (u.kind == nkind.N_TARRAY) { return u.lhs; };
@@ -8443,6 +8478,8 @@ fn indexresult(c: *checker, e: *node) *node = {
 		};
 		return inner;
 	};
+	// Invalid input (non-indexable base — cstage errors at
+	// cmd/wcc/check.c:893). 5-lite-b #34.
 	return nil;
 };
 
@@ -8459,6 +8496,19 @@ fn indexresult(c: *checker, e: *node) *node = {
 // follows doesn't ripple a fresh signature change. Mirrors harec's
 // `check_expression(..., result_type, ...)` per
 // `feedback_hare_frontend_reference.md`.
+//
+// Dispatcher invariant (5-lite-a #33): every value-producing nkind
+// listed in resolvewalk's post-order dispatch (L474-489) reaches a
+// stamping arm here that sets e.type_ before returning. No
+// fall-through. Arms that return nil (binoptype trailing, unoptype
+// TK_STAR opt-nil, indexresult u-nil, N_DOT outer fold-miss, N_SLICE
+// non-sliceable base, etc.) are propagation from a callee's nil —
+// not silent gaps. Mirror of harec's
+// `assert(expr->result)` at ref/harec/src/check.c:3810. The
+// asserttyped pass at L2871 enforces the invariant on every
+// dispatched node post-checker, with gates for the residual
+// inherent-IDENT bails (SK_USE, pseudo-builtin sym.decl==nil,
+// N_DOT-LHS syntactic position) until #19 retires the bail shape.
 fn exprtype(c: *checker, e: *node, hint: *node) *node = {
 	if (e == nil) { return nil; };
 	let k: nkind = e.kind;
@@ -9753,6 +9803,101 @@ fn resolvefnbody(c: *checker, fnnode: *node) void = {
 	c.cur = outer;
 };
 
+// asserttyped — post-checker invariant gate (#15, A.6.2.1e). Walks the
+// file tree and fires (writes a one-line diagnostic to stderr) for any
+// node in resolvewalk's value-producing dispatch set (L474-489) whose
+// n.type_ remained nil. Mirror of harec's `assert(expr->result)` at
+// ref/harec/src/check.c:3810 — wwstage's checker is lenient (rule 7),
+// so this is a soft assertion (diagnostic, not abort) used by the
+// 990_selfhost probes to catch regressions in the stamping discipline.
+//
+// Gates (per Drew 2026-05-22 — "guards value-producing expression
+// nodes; SK_USE refs and bare builtin callees are syntactic positions,
+// gate them out with WHY pointing at #19"):
+//
+//   1. N_IDENT whose resolved sym kind is SK_USE — module references
+//      (`os` in `os.write`). Harec models these via EXPR_ACCESS whose
+//      lookup-target is an OBJ_USE directly; there is no intermediate
+//      "ident-as-value" expr. Until #19 ports that AST shape, skip.
+//   2. N_IDENT whose resolved sym has decl == nil — pseudo-builtin
+//      callees (len/append/free/alloc/size/align/offset, seeded in
+//      checkinit L85-97 with decl=nil). Harec spells these as
+//      dedicated EXPR_* kinds (EXPR_LEN, EXPR_APPEND, EXPR_FREE,
+//      EXPR_ALLOC at ref/harec/src/check.c:2630/745/2443/...).
+//      Drew's δ (#19) retires the seeded-SK_FN-with-nil-decl hack.
+//   3. N_IDENT at the LHS-of-N_DOT syntactic position — the bare
+//      name half of a member-access expr is a lookup target, not a
+//      value-producing sub-expression. Harec's EXPR_ACCESS stores the
+//      member as a string, not a node.
+//
+// `indot` tracks gate 3: true only when the immediate caller is an
+// N_DOT recursing into its .lhs.
+fn asserttyped(c: *checker, n: *node, indot: bool) void = {
+	if (n == nil) { return; };
+	let k: nkind = n.kind;
+	let isexpr: bool =
+		k == nkind.N_INTLIT    || k == nkind.N_FLOATLIT  ||
+		k == nkind.N_STRLIT    || k == nkind.N_RUNELIT   ||
+		k == nkind.N_TRUE      || k == nkind.N_FALSE     ||
+		k == nkind.N_NIL       || k == nkind.N_VOIDLIT   ||
+		k == nkind.N_IDENT     || k == nkind.N_BIN       ||
+		k == nkind.N_UN        || k == nkind.N_CALL      ||
+		k == nkind.N_INDEX     || k == nkind.N_CAST      ||
+		k == nkind.N_STRUCTLIT || k == nkind.N_ARRLIT    ||
+		k == nkind.N_RECV      || k == nkind.N_DOT       ||
+		k == nkind.N_SLICE     || k == nkind.N_SPREAD    ||
+		k == nkind.N_TUPLE     || k == nkind.N_TRYPROP   ||
+		k == nkind.N_TRYUNW    || k == nkind.N_TYPETEST  ||
+		k == nkind.N_TYPEASSERT || k == nkind.N_YIELD    ||
+		k == nkind.N_MATCH;
+	let skip: bool = false;
+	if (isexpr && k == nkind.N_IDENT) {
+		if (indot) { skip = true; };
+		if (!skip) {
+			let s: *sym = scopelookup(c.cur, n.str);
+			if (s != nil) {
+				if (s.skind == skind.SK_USE) { skip = true; };
+				if (s.decl == nil) { skip = true; };
+			};
+		};
+	};
+	if (isexpr && !skip) {
+		if (n.type_ == nil) {
+			os.write(2, "asserttyped: ".ptr, 13u64);
+			let kn: str = nkname(k);
+			os.write(2, kn.ptr, kn.len: u64);
+			os.write(2, " ".ptr, 1u64);
+			if (n.file.len > 0) {
+				os.write(2, n.file.ptr, n.file.len: u64);
+				os.write(2, ":".ptr, 1u64);
+				let ls: str = strconv.i32tos(n.line, strconv.base.DEC);
+				os.write(2, ls.ptr, ls.len: u64);
+			};
+			if (n.str.len > 0) {
+				os.write(2, " '".ptr, 2u64);
+				os.write(2, n.str.ptr, n.str.len: u64);
+				os.write(2, "'".ptr, 1u64);
+			};
+			os.write(2, "\n".ptr, 1u64);
+		};
+	};
+	if (k == nkind.N_DOT) {
+		if (n.lhs != nil) { asserttyped(c, n.lhs, true); };
+		return;
+	};
+	if (n.attr != nil) { asserttyped(c, n.attr, false); };
+	if (n.lhs  != nil) { asserttyped(c, n.lhs,  false); };
+	if (n.rhs  != nil) { asserttyped(c, n.rhs,  false); };
+	if (n.cond != nil) { asserttyped(c, n.cond, false); };
+	if (n.body != nil) { asserttyped(c, n.body, false); };
+	if (n.els  != nil) { asserttyped(c, n.els,  false); };
+	let m: *node = n.list;
+	for (m != nil) {
+		asserttyped(c, m, false);
+		m = m.next;
+	};
+};
+
 export fn checkinit(c: *checker, tc: *tctx) void = {
 	c.tc = tc;
 	c.top = newscope(nil);
@@ -9808,6 +9953,17 @@ export fn checkfile(c: *checker, file: *node) void = {
 		};};};};
 		d = d.next;
 	};
+
+	// Pass 3 (#15, A.6.2.1e): post-checker invariant gate. Walks each
+	// decl with its curmod set so asserttyped's gate lookups resolve
+	// against the same module context exprtype saw during pass 2.
+	d = file.list;
+	for (d != nil) {
+		c.curmod = declmod(file, d);
+		asserttyped(c, d, false);
+		d = d.next;
+	};
+
 	let empty: str;
 	c.curmod = empty;
 
diff --git a/selfhost/cmd/wcc/check.ww b/selfhost/cmd/wcc/check.ww
index efd7f631..9cb23d6f 100644
--- a/selfhost/cmd/wcc/check.ww
+++ b/selfhost/cmd/wcc/check.ww
@@ -21,6 +21,7 @@ package wcc;
 
 import os;
 import tok;
+import strconv;
 
 type checker = struct {
 	tc:       *tctx,
@@ -1346,10 +1347,17 @@ fn tinfofornode(c: *checker, n: *node) *tinfo = {
 };
 
 // unifyarith — usual-arithmetic-conversion analogue at the AST-tnode
-// layer. Mirrors cstage cmd/wcc/check.c:580-596 `unify_arith`. The
-// trailing typeeq fallback covers same-typed operands; mismatched typed
-// pairs silently return ltn (cstage flags the same shape — wwstage's
-// checker stays silent here per existing discipline).
+// layer. Mirrors cstage cmd/wcc/check.c:580-596 `unify_arith` and harec
+// ref/harec/src/types.c type_promote. Trailing `return ltn` covers
+// mismatched typed pairs; cstage flags the same shape — wwstage's
+// checker stays silent here per existing discipline.
+//
+// Nil-on-valid classification (5-lite-b #34, A.6.2.1c #24): both ltn
+// and rtn can be nil when an operand was an inherent-IDENT bail
+// (exprtype N_IDENT arm L1596-1599 — SK_USE module ref or pseudo-
+// builtin callee with sym.decl == nil; #19 retires these as
+// dedicated AST kinds). Propagation, not silent gap — asserttyped
+// gates those idents at the consumer layer.
 fn unifyarith(c: *checker, ltn: *node, rtn: *node) *node = {
 	let lu: bool = isuntypedint(ltn) || isuntypedfloat(ltn);
 	let ru: bool = isuntypedint(rtn) || isuntypedfloat(rtn);
@@ -1367,6 +1375,9 @@ fn unifyarith(c: *checker, ltn: *node, rtn: *node) *node = {
 		if (isassignable(c, ltn, rtn, &conf)) { return ltn; };
 	};
 	if (typeeqast(ltn, rtn)) { return ltn; };
+	// Mismatched typed pair — return ltn so the binop stamps something;
+	// 5-lite-b: the trailing nil-on-mismatch shape was eliminated when
+	// the helper was split out of binoptype.
 	return ltn;
 };
 
@@ -1408,13 +1419,18 @@ fn binoptype(c: *checker, e: *node) *node = {
 	    op == tkind.TK_AND || op == tkind.TK_OR) {
 		return mktname(c, "bool");
 	};
+	// Unreachable for valid input: op is one of TK_PLUS/MINUS/STAR/
+	// SLASH/PERCENT/AMP/PIPE/CARET/LSHIFT/RSHIFT/EQ/NEQ/LT/LE/GT/GE/
+	// AND/OR per parser invariant (lib/ww/parse/expr.ww binary-op
+	// table); all are handled above. 5-lite-b #34.
 	return nil;
 };
 
 // unoptype — derive the result tnode of an N_UN unary expression. Mirrors
-// cstage cmd/wcc/check.c:642-687 `cunop`. The slice/str .len/.cap
-// pseudo-field address-of widening to *i64 mirrors check.c:672-682
-// directly — its purpose is documented at the cstage site.
+// cstage cmd/wcc/check.c:642-687 `cunop` and harec ref/harec/src/types.c
+// type_promote. The slice/str .len/.cap pseudo-field address-of widening
+// to *i64 mirrors check.c:672-682 directly — its purpose is documented
+// at the cstage site.
 fn unoptype(c: *checker, e: *node) *node = {
 	let op: tkind = e.op;
 	let opt: *node = exprtype(c, e.lhs, nil);
@@ -1422,9 +1438,18 @@ fn unoptype(c: *checker, e: *node) *node = {
 	if (op == tkind.TK_NOT)   { return mktname(c, "bool"); };
 	if (op == tkind.TK_TILDE) { return opt; };
 	if (op == tkind.TK_STAR) {
+		// opt nil here means the operand was an inherent-IDENT bail
+		// (exprtype N_IDENT arm L1596-1599 — SK_USE / pseudo-builtin
+		// sym.decl == nil — or another helper's nil propagation);
+		// 5-lite-b #34, A.6.2.1c #24. The `u == nil` post-resolvealias
+		// check was eliminated here — unwrapbang(non-nil) returns
+		// non-nil (parser invariant N_TBANG.lhs always set) and
+		// resolvealias passes through non-nil unchanged (L513
+		// `for (cur != nil)` only exits via `return cur` or `return n`).
 		if (opt == nil) { return nil; };
 		let u: *node = resolvealias(c, unwrapbang(opt));
-		if (u == nil) { return nil; };
+		// Invalid input (non-pointer dereference); cstage errors at
+		// cmd/wcc/check.c:660. 5-lite-b #34.
 		if (u.kind != nkind.N_TPTR) { return nil; };
 		return u.lhs;
 	};
@@ -1448,23 +1473,33 @@ fn unoptype(c: *checker, e: *node) *node = {
 				};
 			};
 		};
+		// opt nil → propagation from inherent-IDENT bail (5-lite-b
+		// #34). Generic &expr widens to *opt; without opt we can't
+		// synthesize the pointer node.
 		if (opt == nil) { return nil; };
 		let pp: *node = newnode(nkind.N_TPTR, "", 0, 0);
 		pp.lhs = opt;
 		return pp;
 	};
+	// Unreachable for valid input: op is one of TK_MINUS/PLUS/NOT/
+	// TILDE/STAR/AMP per parser invariant (lib/ww/parse/expr.ww unary
+	// op set); all are handled above. 5-lite-b #34.
 	return nil;
 };
 
 // indexresult — derive the result tnode of an N_INDEX expression.
-// Mirrors cstage cmd/wcc/check.c:870-894. Slice/array → elem; str →
-// u8; `*[N]T` decays to T (pointer-to-array); `*[]T` does NOT decay
-// (yields []T via the generic *U → U fallback — Hare-faithful, a
-// pointer-to-slice is a 1D array of slices, not of T); generic *T → T.
+// Mirrors cstage cmd/wcc/check.c:870-894 and harec ref/harec/src/types.c
+// type_promote dispatch. Slice/array → elem; str → u8; `*[N]T` decays
+// to T (pointer-to-array); `*[]T` does NOT decay (yields []T via the
+// generic *U → U fallback — Hare-faithful, a pointer-to-slice is a 1D
+// array of slices, not of T); generic *T → T.
 fn indexresult(c: *checker, e: *node) *node = {
 	let basetn: *node = exprtype(c, e.lhs, nil);
 	let _idx: *node = exprtype(c, e.rhs, nil);
 	let u: *node = resolvealias(c, unwrapbang(basetn));
+	// basetn nil → propagation from inherent-IDENT bail at exprtype
+	// N_IDENT arm L1596-1599 (5-lite-b #34, A.6.2.1c #24).
+	// unwrapbang(nil)=nil and resolvealias(nil)=nil pass through.
 	if (u == nil) { return nil; };
 	if (u.kind == nkind.N_TSLICE) { return u.lhs; };
 	if (u.kind == nkind.N_TARRAY) { return u.lhs; };
@@ -1479,6 +1514,8 @@ fn indexresult(c: *checker, e: *node) *node = {
 		};
 		return inner;
 	};
+	// Invalid input (non-indexable base — cstage errors at
+	// cmd/wcc/check.c:893). 5-lite-b #34.
 	return nil;
 };
 
@@ -1495,6 +1532,19 @@ fn indexresult(c: *checker, e: *node) *node = {
 // follows doesn't ripple a fresh signature change. Mirrors harec's
 // `check_expression(..., result_type, ...)` per
 // `feedback_hare_frontend_reference.md`.
+//
+// Dispatcher invariant (5-lite-a #33): every value-producing nkind
+// listed in resolvewalk's post-order dispatch (L474-489) reaches a
+// stamping arm here that sets e.type_ before returning. No
+// fall-through. Arms that return nil (binoptype trailing, unoptype
+// TK_STAR opt-nil, indexresult u-nil, N_DOT outer fold-miss, N_SLICE
+// non-sliceable base, etc.) are propagation from a callee's nil —
+// not silent gaps. Mirror of harec's
+// `assert(expr->result)` at ref/harec/src/check.c:3810. The
+// asserttyped pass at L2871 enforces the invariant on every
+// dispatched node post-checker, with gates for the residual
+// inherent-IDENT bails (SK_USE, pseudo-builtin sym.decl==nil,
+// N_DOT-LHS syntactic position) until #19 retires the bail shape.
 fn exprtype(c: *checker, e: *node, hint: *node) *node = {
 	if (e == nil) { return nil; };
 	let k: nkind = e.kind;
@@ -2789,6 +2839,101 @@ fn resolvefnbody(c: *checker, fnnode: *node) void = {
 	c.cur = outer;
 };
 
+// asserttyped — post-checker invariant gate (#15, A.6.2.1e). Walks the
+// file tree and fires (writes a one-line diagnostic to stderr) for any
+// node in resolvewalk's value-producing dispatch set (L474-489) whose
+// n.type_ remained nil. Mirror of harec's `assert(expr->result)` at
+// ref/harec/src/check.c:3810 — wwstage's checker is lenient (rule 7),
+// so this is a soft assertion (diagnostic, not abort) used by the
+// 990_selfhost probes to catch regressions in the stamping discipline.
+//
+// Gates (per Drew 2026-05-22 — "guards value-producing expression
+// nodes; SK_USE refs and bare builtin callees are syntactic positions,
+// gate them out with WHY pointing at #19"):
+//
+//   1. N_IDENT whose resolved sym kind is SK_USE — module references
+//      (`os` in `os.write`). Harec models these via EXPR_ACCESS whose
+//      lookup-target is an OBJ_USE directly; there is no intermediate
+//      "ident-as-value" expr. Until #19 ports that AST shape, skip.
+//   2. N_IDENT whose resolved sym has decl == nil — pseudo-builtin
+//      callees (len/append/free/alloc/size/align/offset, seeded in
+//      checkinit L85-97 with decl=nil). Harec spells these as
+//      dedicated EXPR_* kinds (EXPR_LEN, EXPR_APPEND, EXPR_FREE,
+//      EXPR_ALLOC at ref/harec/src/check.c:2630/745/2443/...).
+//      Drew's δ (#19) retires the seeded-SK_FN-with-nil-decl hack.
+//   3. N_IDENT at the LHS-of-N_DOT syntactic position — the bare
+//      name half of a member-access expr is a lookup target, not a
+//      value-producing sub-expression. Harec's EXPR_ACCESS stores the
+//      member as a string, not a node.
+//
+// `indot` tracks gate 3: true only when the immediate caller is an
+// N_DOT recursing into its .lhs.
+fn asserttyped(c: *checker, n: *node, indot: bool) void = {
+	if (n == nil) { return; };
+	let k: nkind = n.kind;
+	let isexpr: bool =
+		k == nkind.N_INTLIT    || k == nkind.N_FLOATLIT  ||
+		k == nkind.N_STRLIT    || k == nkind.N_RUNELIT   ||
+		k == nkind.N_TRUE      || k == nkind.N_FALSE     ||
+		k == nkind.N_NIL       || k == nkind.N_VOIDLIT   ||
+		k == nkind.N_IDENT     || k == nkind.N_BIN       ||
+		k == nkind.N_UN        || k == nkind.N_CALL      ||
+		k == nkind.N_INDEX     || k == nkind.N_CAST      ||
+		k == nkind.N_STRUCTLIT || k == nkind.N_ARRLIT    ||
+		k == nkind.N_RECV      || k == nkind.N_DOT       ||
+		k == nkind.N_SLICE     || k == nkind.N_SPREAD    ||
+		k == nkind.N_TUPLE     || k == nkind.N_TRYPROP   ||
+		k == nkind.N_TRYUNW    || k == nkind.N_TYPETEST  ||
+		k == nkind.N_TYPEASSERT || k == nkind.N_YIELD    ||
+		k == nkind.N_MATCH;
+	let skip: bool = false;
+	if (isexpr && k == nkind.N_IDENT) {
+		if (indot) { skip = true; };
+		if (!skip) {
+			let s: *sym = scopelookup(c.cur, n.str);
+			if (s != nil) {
+				if (s.skind == skind.SK_USE) { skip = true; };
+				if (s.decl == nil) { skip = true; };
+			};
+		};
+	};
+	if (isexpr && !skip) {
+		if (n.type_ == nil) {
+			os.write(2, "asserttyped: ".ptr, 13u64);
+			let kn: str = nkname(k);
+			os.write(2, kn.ptr, kn.len: u64);
+			os.write(2, " ".ptr, 1u64);
+			if (n.file.len > 0) {
+				os.write(2, n.file.ptr, n.file.len: u64);
+				os.write(2, ":".ptr, 1u64);
+				let ls: str = strconv.i32tos(n.line, strconv.base.DEC);
+				os.write(2, ls.ptr, ls.len: u64);
+			};
+			if (n.str.len > 0) {
+				os.write(2, " '".ptr, 2u64);
+				os.write(2, n.str.ptr, n.str.len: u64);
+				os.write(2, "'".ptr, 1u64);
+			};
+			os.write(2, "\n".ptr, 1u64);
+		};
+	};
+	if (k == nkind.N_DOT) {
+		if (n.lhs != nil) { asserttyped(c, n.lhs, true); };
+		return;
+	};
+	if (n.attr != nil) { asserttyped(c, n.attr, false); };
+	if (n.lhs  != nil) { asserttyped(c, n.lhs,  false); };
+	if (n.rhs  != nil) { asserttyped(c, n.rhs,  false); };
+	if (n.cond != nil) { asserttyped(c, n.cond, false); };
+	if (n.body != nil) { asserttyped(c, n.body, false); };
+	if (n.els  != nil) { asserttyped(c, n.els,  false); };
+	let m: *node = n.list;
+	for (m != nil) {
+		asserttyped(c, m, false);
+		m = m.next;
+	};
+};
+
 export fn checkinit(c: *checker, tc: *tctx) void = {
 	c.tc = tc;
 	c.top = newscope(nil);
@@ -2844,6 +2989,17 @@ export fn checkfile(c: *checker, file: *node) void = {
 		};};};};
 		d = d.next;
 	};
+
+	// Pass 3 (#15, A.6.2.1e): post-checker invariant gate. Walks each
+	// decl with its curmod set so asserttyped's gate lookups resolve
+	// against the same module context exprtype saw during pass 2.
+	d = file.list;
+	for (d != nil) {
+		c.curmod = declmod(file, d);
+		asserttyped(c, d, false);
+		d = d.next;
+	};
+
 	let empty: str;
 	c.curmod = empty;
 
diff --git a/selfhost/cmd/wwdump/main.combined.ww b/selfhost/cmd/wwdump/main.combined.ww
index 356f8d80..3158ced0 100644
--- a/selfhost/cmd/wwdump/main.combined.ww
+++ b/selfhost/cmd/wwdump/main.combined.ww
@@ -4569,7 +4569,7 @@ export fn newnode(k: nkind, file: str, line: i32, col: i32) *node = {
 
 // ---- printer ----------------------------------------------------------
 
-fn nkname(k: nkind) str = {
+export fn nkname(k: nkind) str = {
 	if (k == nkind.N_NONE)      { return "none"; };
 	if (k == nkind.N_INTLIT)    { return "int"; };
 	if (k == nkind.N_FLOATLIT)  { return "float"; };
@@ -6985,6 +6985,7 @@ package wcc;
 
 import os;
 import tok;
+import strconv;
 
 type checker = struct {
 	tc:       *tctx,
@@ -8310,10 +8311,17 @@ fn tinfofornode(c: *checker, n: *node) *tinfo = {
 };
 
 // unifyarith — usual-arithmetic-conversion analogue at the AST-tnode
-// layer. Mirrors cstage cmd/wcc/check.c:580-596 `unify_arith`. The
-// trailing typeeq fallback covers same-typed operands; mismatched typed
-// pairs silently return ltn (cstage flags the same shape — wwstage's
-// checker stays silent here per existing discipline).
+// layer. Mirrors cstage cmd/wcc/check.c:580-596 `unify_arith` and harec
+// ref/harec/src/types.c type_promote. Trailing `return ltn` covers
+// mismatched typed pairs; cstage flags the same shape — wwstage's
+// checker stays silent here per existing discipline.
+//
+// Nil-on-valid classification (5-lite-b #34, A.6.2.1c #24): both ltn
+// and rtn can be nil when an operand was an inherent-IDENT bail
+// (exprtype N_IDENT arm L1596-1599 — SK_USE module ref or pseudo-
+// builtin callee with sym.decl == nil; #19 retires these as
+// dedicated AST kinds). Propagation, not silent gap — asserttyped
+// gates those idents at the consumer layer.
 fn unifyarith(c: *checker, ltn: *node, rtn: *node) *node = {
 	let lu: bool = isuntypedint(ltn) || isuntypedfloat(ltn);
 	let ru: bool = isuntypedint(rtn) || isuntypedfloat(rtn);
@@ -8331,6 +8339,9 @@ fn unifyarith(c: *checker, ltn: *node, rtn: *node) *node = {
 		if (isassignable(c, ltn, rtn, &conf)) { return ltn; };
 	};
 	if (typeeqast(ltn, rtn)) { return ltn; };
+	// Mismatched typed pair — return ltn so the binop stamps something;
+	// 5-lite-b: the trailing nil-on-mismatch shape was eliminated when
+	// the helper was split out of binoptype.
 	return ltn;
 };
 
@@ -8372,13 +8383,18 @@ fn binoptype(c: *checker, e: *node) *node = {
 	    op == tkind.TK_AND || op == tkind.TK_OR) {
 		return mktname(c, "bool");
 	};
+	// Unreachable for valid input: op is one of TK_PLUS/MINUS/STAR/
+	// SLASH/PERCENT/AMP/PIPE/CARET/LSHIFT/RSHIFT/EQ/NEQ/LT/LE/GT/GE/
+	// AND/OR per parser invariant (lib/ww/parse/expr.ww binary-op
+	// table); all are handled above. 5-lite-b #34.
 	return nil;
 };
 
 // unoptype — derive the result tnode of an N_UN unary expression. Mirrors
-// cstage cmd/wcc/check.c:642-687 `cunop`. The slice/str .len/.cap
-// pseudo-field address-of widening to *i64 mirrors check.c:672-682
-// directly — its purpose is documented at the cstage site.
+// cstage cmd/wcc/check.c:642-687 `cunop` and harec ref/harec/src/types.c
+// type_promote. The slice/str .len/.cap pseudo-field address-of widening
+// to *i64 mirrors check.c:672-682 directly — its purpose is documented
+// at the cstage site.
 fn unoptype(c: *checker, e: *node) *node = {
 	let op: tkind = e.op;
 	let opt: *node = exprtype(c, e.lhs, nil);
@@ -8386,9 +8402,18 @@ fn unoptype(c: *checker, e: *node) *node = {
 	if (op == tkind.TK_NOT)   { return mktname(c, "bool"); };
 	if (op == tkind.TK_TILDE) { return opt; };
 	if (op == tkind.TK_STAR) {
+		// opt nil here means the operand was an inherent-IDENT bail
+		// (exprtype N_IDENT arm L1596-1599 — SK_USE / pseudo-builtin
+		// sym.decl == nil — or another helper's nil propagation);
+		// 5-lite-b #34, A.6.2.1c #24. The `u == nil` post-resolvealias
+		// check was eliminated here — unwrapbang(non-nil) returns
+		// non-nil (parser invariant N_TBANG.lhs always set) and
+		// resolvealias passes through non-nil unchanged (L513
+		// `for (cur != nil)` only exits via `return cur` or `return n`).
 		if (opt == nil) { return nil; };
 		let u: *node = resolvealias(c, unwrapbang(opt));
-		if (u == nil) { return nil; };
+		// Invalid input (non-pointer dereference); cstage errors at
+		// cmd/wcc/check.c:660. 5-lite-b #34.
 		if (u.kind != nkind.N_TPTR) { return nil; };
 		return u.lhs;
 	};
@@ -8412,23 +8437,33 @@ fn unoptype(c: *checker, e: *node) *node = {
 				};
 			};
 		};
+		// opt nil → propagation from inherent-IDENT bail (5-lite-b
+		// #34). Generic &expr widens to *opt; without opt we can't
+		// synthesize the pointer node.
 		if (opt == nil) { return nil; };
 		let pp: *node = newnode(nkind.N_TPTR, "", 0, 0);
 		pp.lhs = opt;
 		return pp;
 	};
+	// Unreachable for valid input: op is one of TK_MINUS/PLUS/NOT/
+	// TILDE/STAR/AMP per parser invariant (lib/ww/parse/expr.ww unary
+	// op set); all are handled above. 5-lite-b #34.
 	return nil;
 };
 
 // indexresult — derive the result tnode of an N_INDEX expression.
-// Mirrors cstage cmd/wcc/check.c:870-894. Slice/array → elem; str →
-// u8; `*[N]T` decays to T (pointer-to-array); `*[]T` does NOT decay
-// (yields []T via the generic *U → U fallback — Hare-faithful, a
-// pointer-to-slice is a 1D array of slices, not of T); generic *T → T.
+// Mirrors cstage cmd/wcc/check.c:870-894 and harec ref/harec/src/types.c
+// type_promote dispatch. Slice/array → elem; str → u8; `*[N]T` decays
+// to T (pointer-to-array); `*[]T` does NOT decay (yields []T via the
+// generic *U → U fallback — Hare-faithful, a pointer-to-slice is a 1D
+// array of slices, not of T); generic *T → T.
 fn indexresult(c: *checker, e: *node) *node = {
 	let basetn: *node = exprtype(c, e.lhs, nil);
 	let _idx: *node = exprtype(c, e.rhs, nil);
 	let u: *node = resolvealias(c, unwrapbang(basetn));
+	// basetn nil → propagation from inherent-IDENT bail at exprtype
+	// N_IDENT arm L1596-1599 (5-lite-b #34, A.6.2.1c #24).
+	// unwrapbang(nil)=nil and resolvealias(nil)=nil pass through.
 	if (u == nil) { return nil; };
 	if (u.kind == nkind.N_TSLICE) { return u.lhs; };
 	if (u.kind == nkind.N_TARRAY) { return u.lhs; };
@@ -8443,6 +8478,8 @@ fn indexresult(c: *checker, e: *node) *node = {
 		};
 		return inner;
 	};
+	// Invalid input (non-indexable base — cstage errors at
+	// cmd/wcc/check.c:893). 5-lite-b #34.
 	return nil;
 };
 
@@ -8459,6 +8496,19 @@ fn indexresult(c: *checker, e: *node) *node = {
 // follows doesn't ripple a fresh signature change. Mirrors harec's
 // `check_expression(..., result_type, ...)` per
 // `feedback_hare_frontend_reference.md`.
+//
+// Dispatcher invariant (5-lite-a #33): every value-producing nkind
+// listed in resolvewalk's post-order dispatch (L474-489) reaches a
+// stamping arm here that sets e.type_ before returning. No
+// fall-through. Arms that return nil (binoptype trailing, unoptype
+// TK_STAR opt-nil, indexresult u-nil, N_DOT outer fold-miss, N_SLICE
+// non-sliceable base, etc.) are propagation from a callee's nil —
+// not silent gaps. Mirror of harec's
+// `assert(expr->result)` at ref/harec/src/check.c:3810. The
+// asserttyped pass at L2871 enforces the invariant on every
+// dispatched node post-checker, with gates for the residual
+// inherent-IDENT bails (SK_USE, pseudo-builtin sym.decl==nil,
+// N_DOT-LHS syntactic position) until #19 retires the bail shape.
 fn exprtype(c: *checker, e: *node, hint: *node) *node = {
 	if (e == nil) { return nil; };
 	let k: nkind = e.kind;
@@ -9753,6 +9803,101 @@ fn resolvefnbody(c: *checker, fnnode: *node) void = {
 	c.cur = outer;
 };
 
+// asserttyped — post-checker invariant gate (#15, A.6.2.1e). Walks the
+// file tree and fires (writes a one-line diagnostic to stderr) for any
+// node in resolvewalk's value-producing dispatch set (L474-489) whose
+// n.type_ remained nil. Mirror of harec's `assert(expr->result)` at
+// ref/harec/src/check.c:3810 — wwstage's checker is lenient (rule 7),
+// so this is a soft assertion (diagnostic, not abort) used by the
+// 990_selfhost probes to catch regressions in the stamping discipline.
+//
+// Gates (per Drew 2026-05-22 — "guards value-producing expression
+// nodes; SK_USE refs and bare builtin callees are syntactic positions,
+// gate them out with WHY pointing at #19"):
+//
+//   1. N_IDENT whose resolved sym kind is SK_USE — module references
+//      (`os` in `os.write`). Harec models these via EXPR_ACCESS whose
+//      lookup-target is an OBJ_USE directly; there is no intermediate
+//      "ident-as-value" expr. Until #19 ports that AST shape, skip.
+//   2. N_IDENT whose resolved sym has decl == nil — pseudo-builtin
+//      callees (len/append/free/alloc/size/align/offset, seeded in
+//      checkinit L85-97 with decl=nil). Harec spells these as
+//      dedicated EXPR_* kinds (EXPR_LEN, EXPR_APPEND, EXPR_FREE,
+//      EXPR_ALLOC at ref/harec/src/check.c:2630/745/2443/...).
+//      Drew's δ (#19) retires the seeded-SK_FN-with-nil-decl hack.
+//   3. N_IDENT at the LHS-of-N_DOT syntactic position — the bare
+//      name half of a member-access expr is a lookup target, not a
+//      value-producing sub-expression. Harec's EXPR_ACCESS stores the
+//      member as a string, not a node.
+//
+// `indot` tracks gate 3: true only when the immediate caller is an
+// N_DOT recursing into its .lhs.
+fn asserttyped(c: *checker, n: *node, indot: bool) void = {
+	if (n == nil) { return; };
+	let k: nkind = n.kind;
+	let isexpr: bool =
+		k == nkind.N_INTLIT    || k == nkind.N_FLOATLIT  ||
+		k == nkind.N_STRLIT    || k == nkind.N_RUNELIT   ||
+		k == nkind.N_TRUE      || k == nkind.N_FALSE     ||
+		k == nkind.N_NIL       || k == nkind.N_VOIDLIT   ||
+		k == nkind.N_IDENT     || k == nkind.N_BIN       ||
+		k == nkind.N_UN        || k == nkind.N_CALL      ||
+		k == nkind.N_INDEX     || k == nkind.N_CAST      ||
+		k == nkind.N_STRUCTLIT || k == nkind.N_ARRLIT    ||
+		k == nkind.N_RECV      || k == nkind.N_DOT       ||
+		k == nkind.N_SLICE     || k == nkind.N_SPREAD    ||
+		k == nkind.N_TUPLE     || k == nkind.N_TRYPROP   ||
+		k == nkind.N_TRYUNW    || k == nkind.N_TYPETEST  ||
+		k == nkind.N_TYPEASSERT || k == nkind.N_YIELD    ||
+		k == nkind.N_MATCH;
+	let skip: bool = false;
+	if (isexpr && k == nkind.N_IDENT) {
+		if (indot) { skip = true; };
+		if (!skip) {
+			let s: *sym = scopelookup(c.cur, n.str);
+			if (s != nil) {
+				if (s.skind == skind.SK_USE) { skip = true; };
+				if (s.decl == nil) { skip = true; };
+			};
+		};
+	};
+	if (isexpr && !skip) {
+		if (n.type_ == nil) {
+			os.write(2, "asserttyped: ".ptr, 13u64);
+			let kn: str = nkname(k);
+			os.write(2, kn.ptr, kn.len: u64);
+			os.write(2, " ".ptr, 1u64);
+			if (n.file.len > 0) {
+				os.write(2, n.file.ptr, n.file.len: u64);
+				os.write(2, ":".ptr, 1u64);
+				let ls: str = strconv.i32tos(n.line, strconv.base.DEC);
+				os.write(2, ls.ptr, ls.len: u64);
+			};
+			if (n.str.len > 0) {
+				os.write(2, " '".ptr, 2u64);
+				os.write(2, n.str.ptr, n.str.len: u64);
+				os.write(2, "'".ptr, 1u64);
+			};
+			os.write(2, "\n".ptr, 1u64);
+		};
+	};
+	if (k == nkind.N_DOT) {
+		if (n.lhs != nil) { asserttyped(c, n.lhs, true); };
+		return;
+	};
+	if (n.attr != nil) { asserttyped(c, n.attr, false); };
+	if (n.lhs  != nil) { asserttyped(c, n.lhs,  false); };
+	if (n.rhs  != nil) { asserttyped(c, n.rhs,  false); };
+	if (n.cond != nil) { asserttyped(c, n.cond, false); };
+	if (n.body != nil) { asserttyped(c, n.body, false); };
+	if (n.els  != nil) { asserttyped(c, n.els,  false); };
+	let m: *node = n.list;
+	for (m != nil) {
+		asserttyped(c, m, false);
+		m = m.next;
+	};
+};
+
 export fn checkinit(c: *checker, tc: *tctx) void = {
 	c.tc = tc;
 	c.top = newscope(nil);
@@ -9808,6 +9953,17 @@ export fn checkfile(c: *checker, file: *node) void = {
 		};};};};
 		d = d.next;
 	};
+
+	// Pass 3 (#15, A.6.2.1e): post-checker invariant gate. Walks each
+	// decl with its curmod set so asserttyped's gate lookups resolve
+	// against the same module context exprtype saw during pass 2.
+	d = file.list;
+	for (d != nil) {
+		c.curmod = declmod(file, d);
+		asserttyped(c, d, false);
+		d = d.next;
+	};
+
 	let empty: str;
 	c.curmod = empty;