A renew source is an earlier proofproof nanofilA proof is a temporary of class a or f, the result of a check: it holds the checked pointer itself and certifies that the check passed. A raw access names the proof it relies on, so evidence is structural (ir:proof_use/6). that a reuse form trusts for bounds: a single-definition proof Q1 of a single-definition pointer P1, made by a check, check_ahead, renew_if, check_limit or half_check, recorded with its range and alignment.

• ir:renew_source_op/6ir.plrenew_source_op/6not documented lists the ops and what each proves; ir:stage_sources/4ir.plstage_sources/4not documented builds the table, empty in a function with setjmp, whose second return the CFG does not show. Validate.v: renew_source.

• Readers: renewrenew nanofilA renew reuses an earlier check's bounds: renew(Lo, Hi, Rights, Align) of [Q1, P] trusts the dominating check that made Q1 for P's bounds and tests again only what a free changes, that the object is not freed (and, for a write, not read-only). It is the -O default (check_reuse:renew_checks/2, m7.md, round 4)., renew_hullrenew_hull nanofilThe hull of several passed checks of one object is the interval from the least lower end to the greatest upper end of their spans; since an object is one interval, every byte of the hull is in it. renew_hull(Lo, Hi, Rights, Align) of [QL, QH, P] is a renew whose bounds two such checks give: QL's from at or below P+Lo, QH's to at or above P+Hi. (two sources) and half_checkhalf_check nanofilhalf_check(Bound, Lo, Hi, Rights, Align) of [Q1, P] is exactly a check of [Lo, Hi) at P that natively tests only one bound, upper or lower; the other end is known from Q1's earlier check of the same object, P being at a known distance from Q1's pointer..

• Renew.v's renew_source_holds: Q1 is an operand, so its definition dominates the point and replaysreplay nanofilA single definition replays at a point when its name holds what its own instruction's step made, in some earlier frame that agrees with the current one on the instruction's single-definition operands, and the current memory persists from the memory that step left, which lay in the address space.; it holds the pointer P1 held when the check passed, and memory has persisted since, so the object is as the check saw it or freed.

The subtlety: a check_ahead can be a source, and a doomed one did not pass, so Renew.v asks every single definition to replay, not only scope_plain's. A renew trusts only the source's bounds; it asks its own rightsrights Fil-CRights are what an access asks of a capability: read or write, where write allows reading too. Every check, renew and raw access names the rights it needs..

See rocq.md, Renew and the half check.