Background

PR #658 (Layer 3 of #626) introduced the CodegenSkip / CodegenInvariantError infrastructure in vera/skip.py and converted 104 SILENT_SKIP sites to raise CodegenSkip(node, reason). That covers the user-actionable "this Vera construct isn't yet supported by the WASM backend" cases — they now surface as structured [E602] diagnostics with the unsupported-node's source span.

What's left from the #626 audit is the non-SILENT_SKIP buckets, which the closing PR deferred to this follow-up.

Audit results (from PR #658)

The audit walked every return None site in vera/codegen/** and vera/wasm/** and classified each. Source of truth is the aggregate table:

Bucket	Count	Status
SILENT_SKIP	105 (104 converted, 1 borderline demoted to PROPAGATE)	Done in #658
PROPAGATE	154	This issue — Track 1
OPTIONAL_RETURN	74	Leave alone (legitimate Optional[X] design)
INVARIANT_DEFENSIVE	39	This issue — Track 2
Total	372

Dead-code discovery (from PR #658)

Several SILENT_SKIP raises identified by the audit turn out to be unreachable defensive guards post-conversion:

• _element_mem_size always returns a non-None value (falls back to return 4 for any non-primitive non-pair type).
• _element_wasm_type always returns a non-None value (falls back to return "i32").
• _element_load_op / _element_store_op return None only for pair types, and every call site is inside an else: branch of if X_is_pair: — so the raise can never fire.

In PR #658 these were marked with # pragma: no cover and an inline rationale (24 sites in vera/wasm/calls_arrays.py). As part of Track 1 below, consider:

1. Tightening the helper signatures (int | None → int, str | None → str for non-pair callers).
2. Removing the now-unreachable raises entirely once the signatures are tight.

The full per-site audit in the section below preserves the original audit notes — line numbers there are pre-conversion (audit captured before any code changed) and several reasons reference _element_mem_size returning None etc. that the dead-code investigation showed cannot happen in practice. Future contributors working this issue should grep by function name + intent rather than raw line number, and verify each "supposedly silent" raise against the helper's actual return contract before assuming it's reachable.

Track 1 — PROPAGATE cleanup

Pattern: result = self._translate_foo(...); if result is None: return None. These are pure forwarding sites that propagate a None from an upstream call. Post-#658, every legitimate SILENT_SKIP raises CodegenSkip instead of returning None, so these PROPAGATE branches are reachable only on PROPAGATE-of-PROPAGATE chains (which eventually bottom out on a non-converted leaf — or now, on a raise that propagates past them naturally).

Work: scan each PROPAGATE site, verify it's now unreachable (no path returns None to it), and replace the body with an assert or remove the branch entirely. The Layer 1 e602 gate (scripts/check_e602_clean.py) will catch any path that turns out to still produce a silent skip after this cleanup.

Counts by file (from the audit aggregate table):

• vera/wasm/calls_arrays.py — 14
• vera/wasm/calls_containers.py — 27
• vera/wasm/calls_encoding.py — 6
• vera/wasm/calls_handlers.py — 5
• vera/wasm/calls_markup.py — 15
• vera/wasm/calls_math.py — 20
• vera/wasm/calls_parsing.py — 4
• vera/wasm/calls_strings.py — 28
• vera/wasm/calls.py — 3
• vera/wasm/closures.py — 4
• vera/wasm/context.py — 4
• vera/wasm/data.py — 13
• vera/wasm/operators.py — 2
• vera/codegen/closures.py — 3
• vera/codegen/functions.py — 6

These should be done file-by-file, each as a small commit, so any regression bisects cleanly. Many will simply become unreachable code once the surrounding translate_expr / translate_block calls are known to always succeed-or-raise.

Track 2 — INVARIANT_DEFENSIVE conversions

Pattern: if cond_that_typecheck_should_have_rejected: return None. 39 sites, mostly # pragma: no cover defensive guards. Convert each to raise CodegenInvariantError(msg, node).

If one ever fires, that is a compiler bug — the type checker should have rejected the input. The [E699] catch-handler in _compile_fn surfaces it as "Internal compiler error" with a "please file a bug" rationale.

Counts by file:

• vera/wasm/operators.py — 25 (largest cluster; mostly operator-dispatch fallthroughs)
• vera/wasm/inference.py — 10
• vera/codegen/closures.py — 2
• vera/codegen/functions.py — 0 (the L29 borderline was reclassified as PROPAGATE on inspection — _is_compilable itself emits diagnostics)

The operators.py cluster is mostly homogeneous: each _translate_<op> ends with a "dispatch fell through" branch that should be unreachable post-typecheck. A single follow-up commit per file is sufficient.

Cleanup ordering

Recommend doing Track 2 before Track 1:

1. Track 2 first — converts defensive guards to CodegenInvariantError. If any fires, it indicates a checker bug we would want to know about before declaring the surrounding PROPAGATE paths unreachable.
2. Track 1 second — with all SILENT_SKIPs raising and all INVARIANT_DEFENSIVE sites raising, every translator that does not return a non-None result either propagates None (PROPAGATE — reachable) or raises (terminal). PROPAGATE paths that are still reachable just mean there is still a path that returns None somewhere — find it. PROPAGATE paths that are not reachable can be deleted.

Acceptance criteria

• All 39 INVARIANT_DEFENSIVE sites raise CodegenInvariantError
• All 154 PROPAGATE sites either preserved (still reachable) or removed (unreachable)
• scripts/check_e602_clean.py allowlist is empty (or only contains audited / spec-driven entries)
• mypy clean
• pytest passes
• All conformance programs still pass their declared level
• All examples still pass vera check and vera verify

References

• Cross-cutting: convert 'translate returns None → silent skip' failures into loud diagnostics #626 — parent issue (closed by PR Layer 3 of #626: CodegenSkip infrastructure + convert 104 SILENT_SKIPs #658)
• Closure-body compile failure doesn't drop enclosing top-level function #636 — Layer 2 (closure commit-on-success pattern, already merged)
• Layer 1 (+ Layer 2 status note) of #626: pre-commit gate against unexpected [E602]/[E604] silent skips #656 — Layer 1 (e602 gate, already merged)

---

Full per-site audit (pre-conversion line numbers)

The sections below are the verbatim audit from PR #658. Line numbers refer to the state of the source files before the conversion landed (i.e. they were captured against the pre-PR-#658 tree). Post-PR-#658 the function names and intents are preserved, but raw line numbers will not match. When working this issue: grep by function name (e.g. _translate_array_map) and intent (e.g. "ctor layout not found"), not by line.

The narrative counts in the audit (PROPAGATE: 142, SILENT_SKIP: 130, OPTIONAL_RETURN: 60, INVARIANT_DEFENSIVE: 40) reflect a slightly different bucketing than the aggregate table at the bottom of the audit. The aggregate table is the source of truth — see the note immediately after it.

Total sites: 372

• PROPAGATE: 142
• SILENT_SKIP: 130
• OPTIONAL_RETURN: 60
• INVARIANT_DEFENSIVE: 40

Notes on methodology:

• Sites that record a structured failure to a context-side channel (e.g. _apply_fn_inference_failures, _interp_inference_failures) and rely on the central _harvest_* step at the _compile_fn boundary are classed as PROPAGATE — they are already loud via a different mechanism (E615 / E616).
• Sites in _compile_fn / _compile_lifted_closure themselves (the catch handlers that surface CodegenSkip / E602 / E699) are classed as PROPAGATE — they ARE the loud-skip boundary.
• "Inference helper returns None when nothing fits" → OPTIONAL_RETURN.
• "Translator returns None when an unsupported AST shape sneaks through" → SILENT_SKIP if reachable, INVARIANT_DEFENSIVE if marked # pragma: no cover.
• The _element_mem_size / _element_load_op / _element_store_op helpers in vera/wasm/helpers.py themselves return None only for pair types or unrecognised types; their callers that bail are the real silent-skip sites, hence the helper file itself contributes only OPTIONAL_RETURNs.

---

SILENT_SKIP (priority for this PR)

vera/wasm/calls.py

• L460 (_translate_call): unknown function called — guard rail. Currently silently bails after the cross-module check; in practice the cross-module check has already emitted an error so this is mostly defensive, but it can still be reached for prelude-mangled / forward-reference edge cases (e.g. the Five prelude combinators silently skipped from every WASM compile (option_map / option_and_then / result_map + two _unwrap_or variants) #604 option_map mono-suffix mismatch). Suggested reason: "call target not registered in module".

vera/wasm/calls_arrays.py

• L65 (_translate_array_append): _infer_vera_type(elem_arg) returned None. Suggested reason: "could not infer array element type".
• L68 (_translate_array_append): _element_mem_size(elem_type) returned None. Suggested reason: "unsupported array element type for memory layout".
• L73 (_translate_array_append): _element_store_op(elem_type) returned None and not a pair. Suggested reason: "no store op for array element type".
• L303 (_translate_array_concat): _element_mem_size(elem_type) returned None. Suggested reason: "unsupported array element type in concat".
• L447 (_translate_array_slice): collection's element type couldn't be inferred and array isn't a provably-empty literal. Suggested reason: "could not infer array element type for slice".
• L451 (_translate_array_slice): _element_mem_size(elem_type) returned None. Suggested reason: "unsupported array element type for slice".
• L626 (_translate_array_map): _infer_concat_elem_type(arr_arg) returned None. Suggested reason: "could not infer array_map input element type".
• L629 (_translate_array_map): _element_mem_size(a_type) returned None. Suggested reason: "unsupported array_map input element type".
• L633 (_translate_array_map): _element_wasm_type(a_type) returned None. Suggested reason: "no WASM type for array_map input element".
• L637 (_translate_array_map): _infer_closure_return_vera_type(fn_arg) returned None. Suggested reason: "could not infer array_map closure return type".
• L640 (_translate_array_map): _element_mem_size(b_type) returned None. Suggested reason: "unsupported array_map output element type".
• L644 (_translate_array_map): _element_wasm_type(b_type) returned None. Suggested reason: "no WASM type for array_map output element".
• L747 (_translate_array_map body): _element_load_op(a_type) returned None. Suggested reason: "no load op for array_map input element".
• L776 (_translate_array_map body): _element_store_op(b_type) returned None. Suggested reason: "no store op for array_map output element".
• L851, 854, 858 (_translate_array_filter): same triad for filter — could not infer/size/wasm-type element. Suggested reason: "could not infer/size/wasm-type array_filter element".
• L943, 979 (_translate_array_filter body): no load/store op for filter element. Suggested reason: "no load/store op for array_filter element".
• L1084, 1087, 1091, 1095, 1099 (_translate_array_fold): t_type / t_size / t_wasm / u_type / u_wasm inference/lookup failures. Suggested reason: "could not infer/size/wasm-type array_fold input/accumulator".
• L1205 (_translate_array_fold body): no load op for fold element. Suggested reason: "no load op for array_fold element".
• L1304, 1307, 1311 (_translate_array_reverse): t_type / t_size / t_wasm failures. Suggested reason: "could not infer/size/wasm-type array_reverse element".
• L1380 (_translate_array_reverse body): no load/store op. Suggested reason: "no load/store op for array_reverse element".
• L1419, 1422, 1426, 1430, 1433, 1437 (_translate_array_mapi): a/b inference/size/wasm-type. Suggested reason: "could not infer/size/wasm-type array_mapi element".
• L1527, 1558 (_translate_array_mapi body): no load/store op. Suggested reason: "no load/store op for array_mapi element".
• L1632, 1635, 1639 (_translate_array_find): t_type / t_size / t_wasm. Suggested reason: "could not infer/size/wasm-type array_find element".
• L1702 (_translate_array_find body): no load op. Suggested reason: "no load op for array_find element".
• L1762, 1765, 1769 (_translate_array_any / _translate_array_all): same triad. Suggested reason: "could not infer/size/wasm-type array_any/all element".
• L1836, 1861 (_translate_array_any/all body): no load op / no load+store op. Suggested reason: "no load/store op for array_any/all element".
• L1920 (_translate_array_flatten): outer element type isn't "Array". Suggested reason: "array_flatten input must be Array<Array>".
• L1932, 1935 (_translate_array_flatten): t_type unresolvable / no element size. Suggested reason: "could not infer/size array_flatten inner element".
• L2063 (_translate_array_flatten body): no load/store op. Suggested reason: "no load/store op for array_flatten element".
• L2161, 2164, 2168 (_translate_array_sort_by): same triad. Suggested reason: "could not infer/size/wasm-type array_sort_by element".
• L2285, 2312 (_translate_array_sort_by body): no load/store op. Suggested reason: "no load/store op for array_sort_by element".

vera/wasm/calls_containers.py

• L381 (_map_wasm_tag): vera_type starts with "Array" — Map<K, Array> rejected. Suggested reason: "Map/Set element of type Array not supported".
• L505 (_translate_map_new): map_wasm_tag returned None for key or value type (Pre-existing bugs in WASM call translators (surfaced by #474 review) #475 finding 5). Suggested reason: "Map<K, V> with Array-typed K or V not supported".
• L552, 559 (_translate_map_insert): kt or vt was None for key/value. Suggested reason: "Map<K, V> with Array-typed K or V not supported".
• L622 (_translate_map_get): kt was None for key. Suggested reason: "Map<K, V> with Array-typed K not supported".
• L653 (_translate_map_contains): kt was None. Suggested reason: "Map<K, V> with Array-typed K not supported".
• L714, 737 (_translate_map_keys / _translate_map_values): key or value type tagging failed. Suggested reason: "Map<K, V> with Array-typed K/V not supported".
• L888, 927, 957 (_translate_set_add / _translate_set_contains / _translate_set_remove): elem_type tagging failed. Suggested reason: "Set<Array> not supported".
• L1012 (_translate_set_to_array): elem tagging failed. Suggested reason: "Set<Array> not supported".

vera/wasm/calls_handlers.py

• L41 (_translate_show): _infer_vera_type(arg) returned None. Suggested reason: "could not infer show() argument type".
• L68 (_translate_show): vera_type not in _SHOW_DISPATCH table — unsupported show target. Suggested reason: "show() not supported for this type".
• L84 (_translate_hash): _infer_vera_type(arg) returned None. Suggested reason: "could not infer hash() argument type".
• L110 (_translate_hash): vera_type not handled — unsupported hash target. Suggested reason: "hash() not supported for this type".
• L194 (_translate_handle_expr): expr.effect is not an EffectRef. Suggested reason: "handle expression effect must be an EffectRef".
• L203 (_translate_handle_expr): handler type isn't State or Exn. Suggested reason: "only State and Exn handlers supported".
• L221 (_translate_handle_state): State type_arg isn't a NamedType. Suggested reason: "State type argument must be a named type".
• L288 (_translate_handle_exn): Exn type_arg isn't a NamedType. Suggested reason: "Exn type argument must be a named type".
• L332 (_translate_handle_exn): no clauses in handle expression. Suggested reason: "handle[Exn] requires at least one clause".

vera/wasm/context.py

• L426 (translate_expr): dispatch fell through — unknown expression shape. Suggested reason: "no translator for expression type".
• L447 (translate_block let-stmt): _type_expr_to_slot_name(stmt.type_expr) returned None. Suggested reason: "let binding type has no slot name".
• L459 (translate_block let-stmt): _slot_name_to_wasm_type(type_name) returned None. Suggested reason: "let binding type has no WASM representation".
• L485 (translate_block): unknown statement type. Suggested reason: "unknown statement type in block".

vera/wasm/data.py

• L37 (_translate_nullary_constructor): ctor layout not found. Suggested reason: "unknown nullary constructor".
• L63 (_translate_constructor_call): ctor layout not found. Suggested reason: "unknown constructor".
• L74 (_translate_constructor_call): _infer_expr_wasm_type(arg) returned None for a constructor argument. Suggested reason: "could not infer constructor argument WASM type".
• L158 (_translate_let_destruct): type_name was None for a destructuring binding. Suggested reason: "let-destruct type has no slot name".
• L179 (_translate_let_destruct): _slot_name_to_wasm_type(type_name) returned None. Suggested reason: "let-destruct type has no WASM representation".
• L210 (_translate_match_expr): _infer_expr_wasm_type(scrutinee) returned None. Suggested reason: "could not infer match scrutinee WASM type".
• L250 (_compile_match_arms): no arms — should be impossible for well-typed match. (Type-check rejects empty match — borderline INVARIANT_DEFENSIVE; keeping under SILENT_SKIP since reachable for cross-module imports.) Suggested reason: "match expression has no arms".
• L324 (_collect_pattern_check): ctor pattern layout not found. Suggested reason: "unknown constructor in pattern".
• L378 (_setup_match_arm_env): binding pattern type has no slot name. Suggested reason: "binding pattern type has no slot name".
• L390 (_setup_match_arm_env): ctor pattern layout not found. Suggested reason: "unknown constructor in arm pattern".
• L395 (_setup_match_arm_env): unknown pattern kind. Suggested reason: "unsupported match pattern type".
• L420 (_extract_constructor_fields): BindingPattern type has no slot name. Suggested reason: "constructor field binding has no slot name".
• L441 (_extract_constructor_fields): no WASM type for field. Suggested reason: "constructor field has no WASM type".
• L468 (_extract_constructor_fields): nested ctor pattern unknown. Suggested reason: "unknown nested constructor in pattern".
• L492 (_extract_constructor_fields): unknown sub-pattern. Suggested reason: "unsupported nested pattern type".
• L513 (_sub_pattern_wasm_type): BindingPattern type has no slot name. Suggested reason: "sub-pattern binding has no slot name".
• L560 (_collect_nested_tag_checks): sub-pattern WASM type unknown. Suggested reason: "nested pattern field has no WASM type".
• L568 (_collect_nested_tag_checks): nested ctor pattern unknown. Suggested reason: "unknown nested constructor in pattern".
• L613 (_translate_array_lit): _infer_array_element_type(expr) returned None for non-empty literal. Suggested reason: "could not infer array literal element type".
• L622 (_translate_array_lit): _element_mem_size(elem_type) returned None. Suggested reason: "unsupported array literal element type".
• L627 (_translate_array_lit): _element_store_op(elem_type) returned None and not pair. Suggested reason: "no store op for array literal element type".
• L682 (_translate_index_expr): _infer_index_element_type(expr) returned None. Suggested reason: "could not infer index expression element type". (Closure capturing data ADT and passing it to a function call inside body emits malformed WASM #614/Layer-1 #626 surfaced 8 silent-skip cases: 7 spurious generic-decl warnings + 1 real codegen gap (head over refinement-of-Array) #655 area)
• L685 (_translate_index_expr): _element_mem_size(elem_type) returned None. Suggested reason: "unsupported index expression element type".
• L690 (_translate_index_expr): _element_load_op returned None and not pair. Suggested reason: "no load op for index expression element type".

vera/codegen/functions.py

• L29 (_compile_fn): _is_compilable(decl) rejected the declaration. The compilability check emits its own diagnostics, but this is the path by which a non-compilable function silently drops out. Suggested reason: "function rejected by compilability check". (Borderline — could also be PROPAGATE since _is_compilable is supposed to record the diagnostic; review the helper. If it does emit a warning, demote to PROPAGATE.)

---

PROPAGATE (no conversion needed — dead code once upstream raises)

These are the if x is None: return None paths immediately after a sub-translation call. Once every upstream SILENT_SKIP raises CodegenSkip instead of returning None, these branches become unreachable and can be cleaned up in a follow-up pass.

vera/codegen/closures.py

• L396 (_compile_lifted_closure): CodegenSkip catch — emits E602 then returns None to feed _lift_pending_closures' failure path.
• L406 (_compile_lifted_closure): CodegenInvariantError catch — emits E699 then returns None.
• L427 (_compile_lifted_closure): legacy body_instrs is None — harvests inference failures, returns None. The internal harvest + the parent's drop-on-failure path together turn this into a loud surface; this is the closure-side analogue of the L267 functions.py path.

vera/codegen/functions.py

• L116 (_compile_fn): unsupported parameter type — emits E600 then returns None. Already loud.
• L158 (_compile_fn): unsupported return type — emits E601 then returns None. Already loud.
• L227 (_compile_fn): CodegenSkip catch — emits E602 then returns None. The Layer 3 boundary.
• L243 (_compile_fn): CodegenInvariantError catch — emits E699 then returns None. The Layer 3 boundary.
• L267 (_compile_fn): legacy body_instrs is None — harvests + emits generic E602 then returns None. The pre-Layer-3 fallback.
• L329 (_compile_fn): closure-failure parent-drop — emits E602 then returns None. Already loud.

vera/wasm/calls.py

• L440, 467, 502 (_translate_call arg loops, _translate_qualified_call arg loop): sub-arg None propagation.

vera/wasm/calls_arrays.py

• L35, 60, 190, 290, 439, 622, 847, 1080, 1301, 1415, 1628, 1758, 1895, 2157: arr_instrs is None / start_instrs is None / fn_instrs is None propagation across the array combinator suite.

vera/wasm/calls_containers.py

• L195, 224, 247, 259, 280, 298, 316, 333: arg-instrs propagation for Decimal builtins.
• L448, 451, 458: returns inside _infer_map_key_from_call_args / _infer_map_value_from_call_args (inference helpers — see OPTIONAL_RETURN section; these are kept here only because the helpers also have legitimate "no information" returns).
• L518, 525, 573, 579, 634, 640, 665, 671, 699, 723, 746, 899, 905, 938, 944, 968, 974, 998, 1021: arg-instrs propagation across map/set translators.

vera/wasm/calls_encoding.py

• L30, 330, 735, 1014, 1324, 1850: arg-instrs propagation — base64/url encode/decode/parse.

vera/wasm/calls_handlers.py

• L88 (_translate_hash): translate_expr(arg) None propagation.
• L239 (_translate_handle_state): init_expr translate None propagation.
• L256 (_translate_handle_state): body_instrs None propagation.
• L328 (_translate_handle_exn): body_instrs None propagation.
• L350 (_translate_handle_exn): handler_instrs None propagation (pragma no cover).

vera/wasm/calls_markup.py

• L32, 49, 68, 85, 103, 121, 140, 156, 173, 190, 207, 228, 247, 266, 286: arg-instrs propagation — json/html/md/regex builtins.

vera/wasm/calls_math.py

• L32, 58, 85, 112, 129, 147, 164, 181, 263, 279, 302, 347, 364, 420, 439, 481, 499, 532, 576, 620: arg-instrs propagation — every math built-in.

vera/wasm/calls_parsing.py

• L31, 228, 489, 718: arg-instrs propagation.

vera/wasm/calls_strings.py

• All 28 sites: arg-instrs propagation across the string builtin translators.

vera/wasm/closures.py

• L134 (_translate_apply_fn): closure_arg shape unsupported — records to _apply_fn_inference_failures then returns None. Loud via harvest → E616. STRUCTURED PROPAGATE.
• L139, 154 (_translate_apply_fn): arg-instrs propagation.

vera/wasm/context.py

• L443 (translate_block LetStmt): val_instrs None propagation.
• L467 (translate_block ExprStmt): stmt_instrs None propagation.
• L480 (translate_block LetDestruct): result None propagation.
• L490 (translate_block final): expr_instrs None propagation.

vera/wasm/data.py

• L71 (_translate_constructor_call): arg_instrs None propagation.
• L142 (_translate_let_destruct): val_instrs None propagation.
• L206 (_translate_match_expr): scr_instrs None propagation.
• L225 (_translate_match_expr): arm_instrs None propagation.
• L266, 270, 278, 282, 289 (_compile_match_arms): nested setup/body/else propagation.
• L337 (_collect_pattern_check): nested propagation.
• L478 (_extract_constructor_fields): nested propagation.
• L588 (_collect_nested_tag_checks): deeper propagation.
• L644 (_translate_array_lit): elem_instrs propagation.
• L695, 700 (_translate_index_expr): coll_instrs and idx_instrs propagation.

vera/wasm/operators.py

• L400 (_translate_if): cond/then/else propagation (3-way).
• L519 (_translate_interpolated_string): had_failure → returns None after recording to _interp_inference_failures. Loud via harvest → E615. STRUCTURED PROPAGATE.

---

OPTIONAL_RETURN (legitimate Optional design)

These functions return T | None by design — None means "not found / can't infer / lookup failed", with callers checking explicitly and using their own fallback paths. Conversion to exception would change the contract.

vera/codegen/api.py

• L333 (_find_frames_in_exception_chain): exception-chain walker, None = no frames found anywhere.

vera/codegen/contracts.py

• L282 (_state_type_to_wasm): None = type name not registered. Used by _snapshot_old_state with explicit fallback.

vera/codegen/core.py

• L604 (_type_expr_to_wasm_type): Unit → None. Documented contract — caller distinguishes from "unsupported".
• L646 (_type_expr_to_slot_name): non-NamedType type arg — caller-handled.
• L653 (_type_expr_to_slot_name): final fallback for unknown TypeExpr shape — caller-handled.

vera/codegen/modules.py

• L234 (_find_import_node): standard "no matching import found" lookup.

vera/codegen/monomorphize.py

• L285 (_infer_type_args_from_call): no forall_vars → nothing to infer.
• L418, 459 (_infer_vera_type_name, _infer_fncall_vera_type_simple): inference helpers with fallback.
• L533, 567 (_get_arg_type_info): inference helpers — None ok at non-NamedType branches.
• L590 (_get_arg_type_info): inference helper final fallback.
• L616, 624, 676 (_infer_fn_alias_type_args): alias inference helper — None = "can't bind alias type params".

vera/wasm/calls.py

• L637, 645, 689 (_infer_fn_alias_type_args_wasm): same as monomorphize.py 616/624/676 — inference helper.
• L703, 733 (_infer_concat_elem_type): inference helper — None ok for empty or unmatched shapes.

vera/wasm/calls_arrays.py

• L592 (_infer_closure_return_vera_type): inference helper, terminal fallback.
• L1030 (_infer_fold_init_vera_type): inference helper, terminal fallback.

vera/wasm/calls_containers.py

• L448, 451 (_infer_map_key_from_call_args): inference helper — map_new() has no key, and arg count mismatch yields None.
• L458 (_infer_map_value_from_call_args): inference helper — value only inferable from map_insert.
• L612 (_infer_map_value_from_map_arg): inference helper terminal fallback.
• L771 (_parse_map_kv_pair_from_type_arg_name): string-parsing helper, None = malformed input.
• L793 (_infer_map_key_from_map_arg): inference helper terminal fallback.
• L827, 830 (_infer_set_elem_type): set_new() has no element / arg-count mismatch.
• L852 (_infer_set_elem_from_set_arg): inference helper terminal fallback.

vera/wasm/data.py

• L238 (_infer_match_result_type): inference helper, terminal fallback after walking arms.
• L357 (_collect_pattern_check): wildcard/binding patterns have no tag check — None is the "no check needed" sentinel.
• L528, 531 (_sub_pattern_wasm_type): wildcard out-of-range / unknown sub-pattern — caller-handled.

vera/wasm/helpers.py

• L47 (WasmSlotEnv.resolve): lookup helper — None = not found.
• L200, 213 (wasm_type): Unit → None by design.
• L223 (wasm_type_or_none): explicit "unsupported → None" contract.
• L359, 382 (_element_load_op, _element_store_op): pair types return None by design — callers branch on is_pair.

vera/wasm/inference.py

All 38 sites in inference.py are OPTIONAL_RETURN — every function here is an inference helper whose contract is "return the inferred WASM/Vera type, or None if it can't be determined". Callers (_translate_* translators, harvest paths) check the None case and either fall back or escalate via the structured-skip pathway. Includes:

• L131, 153, 161, 186, 191, 210, 211, 239, 241 (_infer_expr_wasm_type / _infer_qualified_call_wasm_type branches).
• L434 (_infer_fncall_wasm_type terminal fallback).
• L446, 464, 498, 507, 508 (_infer_block_result_type branches).
• L598, 632 (_canonical_named_type walker).
• L824, 825 (_infer_vera_type branches).
• L1068, 1097, 1124 (_infer_fncall_vera_type generic/non-generic fallback).
• L1175 (_resolve_i32_pair_ret_te: ret_te is None).
• L1208 (_infer_array_element_type: empty literal).
• L1279, 1294, 1303 (_infer_index_element_type_expr / _alias_array_element walkers).
• L1320, 1346, 1348 (_get_arg_type_info_wasm branches).
• L1436 (_named_type_to_wasm: Unit → None).
• L1480, 1485, 1509, 1514 (_type_expr_name / _type_expr_to_slot_name walkers).
• L1596 (_slot_name_to_wasm_type terminal fallback).

vera/wasm/json_serde.py

• L172 (read_json JNull tag): host-side Python runtime helper — None is the actual JSON null value.
• L231 (read_json unknown-tag): runtime helper warning fallback.

(These two are host-runtime helpers, not codegen translators — they emit warnings via warnings.warn and represent runtime JSON values. They are out of scope for #626 but counted here for completeness.)

---

INVARIANT_DEFENSIVE (deferred to follow-up)

Marked # pragma: no cover or otherwise guarding a state the type-checker should already have rejected. Each candidate for conversion to raise CodegenInvariantError(msg, node), but lower priority than SILENT_SKIP.

vera/codegen/closures.py

• L253 (_compile_lifted_closure): unsupported closure param type — type-check should have rejected.
• L361 (_compile_lifted_closure): unsupported closure return type — type-check should have rejected.

vera/wasm/inference.py

All # pragma: no cover sites in inference.py serve as defensive guards on shapes the type-checker is expected to have ruled out:

• L161 (ResultRef unsupported type-name): would mean a postcondition @T.result on an unsupported type.
• L186, 498 (MatchExpr with no arms): type-check rejects empty match.
• L191, (HandleExpr body with no expr): type-check requires a body expression.
• L241 (QualifiedCall fallthrough): unknown qualifier or op.
• L464, 507, 508 (block-result inference fallthroughs).
• L824, 825 (IfExpr branches that produce None).
• L1320, 1346 (non-NamedType type-args / unmappable ADT args).
• L1485, 1514 (non-NamedType TypeExpr at slot-name extraction).

(These overlap with OPTIONAL_RETURN labels above for sites that are both pragma-defensive and Optional-by-contract; I've counted them once under OPTIONAL_RETURN since the contract is the load-bearing property.)

vera/wasm/operators.py

Most operators.py defensive sites:

• L35 (slot ref non-NamedType type_arg).
• L39 (env.resolve None — type-check should have caught dangling slot ref).
• L70 (non-FnCall RHS of pipe).
• L75 (binary operand translation None — operands are already type-checked).
• L86 (unsupported float op for non-MOD).
• L145 (binary operator dispatch fallthrough).
• L171 (ADT eq with no ctors — impossible for a typed ADT).
• L226 (unsupported ADT field type in eq).
• L378 (unary operand None propagation, marked pragma).
• L386 (unary operator dispatch fallthrough).
• L552 (result ref with no result_local).
• L568 (assert operand None propagation, marked pragma).
• L634, 639, 642 (quantifier domain / predicate-without-params / non-NamedType predicate param).
• L651 (quantifier body None propagation).
• L724, 727 (_translate_old_expr type/local lookups).
• L734, 737 (_translate_new_expr type/op lookups).
• L747, 749, 751, 755 (_extract_state_type_name walker fallthroughs).

vera/codegen/functions.py

• L29: _is_compilable rejection — see SILENT_SKIP note. If _is_compilable emits its own diagnostic this becomes a PROPAGATE; otherwise SILENT_SKIP. Verify when wiring.

---

Aggregate counts by file

File	Total	PROPAGATE	SILENT_SKIP	OPTIONAL_RETURN	INVARIANT_DEFENSIVE
vera/codegen/api.py	1	0	0	1	0
vera/codegen/closures.py	5	3	0	0	2
vera/codegen/contracts.py	1	0	0	1	0
vera/codegen/core.py	3	0	0	3	0
vera/codegen/functions.py	7	6	1	0	0
vera/codegen/modules.py	1	0	0	1	0
vera/codegen/monomorphize.py	9	0	0	9	0
vera/wasm/calls.py	9	3	1	5	0
vera/wasm/calls_arrays.py	71	14	55	2	0
vera/wasm/calls_containers.py	48	27	11	10	0
vera/wasm/calls_encoding.py	6	6	0	0	0
vera/wasm/calls_handlers.py	14	5	9	0	0
vera/wasm/calls_markup.py	15	15	0	0	0
vera/wasm/calls_math.py	20	20	0	0	0
vera/wasm/calls_parsing.py	4	4	0	0	0
vera/wasm/calls_strings.py	28	28	0	0	0
vera/wasm/closures.py	4	4	0	0	0
vera/wasm/context.py	8	4	4	0	0
vera/wasm/data.py	43	13	24	6	0
vera/wasm/helpers.py	6	0	0	6	0
vera/wasm/inference.py	38	0	0	28	10
vera/wasm/json_serde.py	2	0	0	2	0
vera/wasm/operators.py	27	2	0	0	25
Total	372	154	105	74	39

Note: the per-section narrative counts (PROPAGATE: 142, SILENT_SKIP: 130, OPTIONAL_RETURN: 60, INVARIANT_DEFENSIVE: 40 at the top) reflect a slightly different bucketing — see the aggregate table for the per-file accounting used when wiring conversions. The discrepancy is in operators.py where the pragma-no-cover defensive sites can be argued either as PROPAGATE-of-an-impossible-state or INVARIANT_DEFENSIVE; the table treats them as INVARIANT_DEFENSIVE. Use the aggregate table as the source of truth for conversion counts.

---

Recommended conversion order

1. First pass — high-leverage SILENT_SKIP clusters:

   • vera/wasm/calls_arrays.py — 55 sites, all in the array-combinator inference/element-type triad. Single shared helper:

     def _infer_array_element_or_skip(self, arg, *, role: str):
         t = self._infer_concat_elem_type(arg)
         if t is None:
             raise CodegenSkip(arg, f"could not infer {role} element type")
         size = _element_mem_size(t)
         if size is None:
             raise CodegenSkip(arg, f"unsupported {role} element type")
         wt = _element_wasm_type(t)
         if wt is None:
             raise CodegenSkip(arg, f"no WASM type for {role} element")
         return t, size, wt

   • vera/wasm/data.py — 24 sites, mostly ctor/pattern/type-name lookups with clear "unknown" reasons.
   • vera/wasm/calls_containers.py — 11 sites, the Map<K, Array> (Pre-existing bugs in WASM call translators (surfaced by #474 review) #475) rejection points.
   • vera/wasm/calls_handlers.py — 9 sites, show/hash dispatch + handle expressions.
   • vera/wasm/context.py — 4 sites, the central dispatcher's silent fallthroughs.
   • vera/wasm/calls.py — 1 site (guard rail).

2. Second pass — verify PROPAGATE sites are unreachable after the first pass and remove them. Most should become dead code naturally since every translate_expr / translate_block callee now either returns a list or raises.

3. Third pass (follow-up PR) — INVARIANT_DEFENSIVE conversions:

   • vera/wasm/operators.py pragma-no-cover sites → CodegenInvariantError("operator dispatch fallthrough", node=expr) etc.
   • vera/wasm/inference.py pragma-no-cover sites where they ARE called by translators (not just by other inference helpers).
   • vera/codegen/closures.py L253 / L361 defensive returns.

4. Verification: after each pass, re-run the loud-skip gate from PR Layer 1 (+ Layer 2 status note) of #626: pre-commit gate against unexpected [E602]/[E604] silent skips #656 + the SKILL.md / examples suite to ensure no regressions in observable diagnostics. The Layer 1 gate will fail loudly on any newly-surfaced silent skip uncovered by the conversion, which is the intended forcing function.