A block's exit facts are what a validator pass knows at its jump; its entry facts are what it knows before its phis. Two passes keep them, over the same edge rule: entry facts are the meet over incoming edges, nothing comes over a poll edge, and an edge from a block the pass has not yet reached carries nothing.

• The evidence passevidence pass nanofilThe evidence pass is the validator's forward walk over a checked function: it tracks live facts and accepts each raw access only where its own check, a live fact or a reuse rule covers it. It visits the blocks once, in order; a block's entry facts are the meet over its incoming edges, with nothing carried over a poll edge or from a block not yet visited., forward: exit facts are live factslive fact nanofilA live fact live(Q, P, Lo, Hi, Rights, Align) is the validator's record that the proof Q came from a check of P over [Lo, Hi) that still holds: no safepoint since, and neither Q nor P redefined. A later raw access through Q that the fact covers needs no check of its own. at the block's end, kept per label (ir:stage_func/6ir.plstage_func+Stage, +Symbols, +Fn, +Mode, +Params, +BlocksdetFn's blocks are well formed for the module's Stage. A checked function accesses memory only by raw accesses, each covered by a check whose evidence still holds, and polls on every cycle.). Walk.v's pass_exits reads them back; Invariant.v's point_ok asks a block's entry, from a predecessor by an unpolled edge, to see that predecessor's exit facts hold.

• The needneed nanofilA need is the validator's backward fact for check_ahead: need(B) = H at a point says every path from it reaches a raw heap access through a pointer of which B is an exact base, whose bytes reach B + H, and reaches it first: before any instruction that is not ahead-transparent, any poll edge, edge back or end, and before B is redefined. analysis, backward: exit needs are the meet over a block's own edges of its targets' entry needs, keeping the least (ir:ahead_edge/5ir.plahead_edge/5not documented, ir:ahead_meet/2ir.plahead_meet+Facts, -Meetthe bases in every one of Facts, each with its least need; none for no facts.). Ahead.v's block_exit and ahead_entry.

The subtlety: the meet over no edges is empty, so a block reached first by a back edge, or a function's entry, starts with no facts at all.

See schedule.md, Validator rule.