A renew reuses an earlier check's bounds: renewLo, 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/2check_reuse.plrenew_checks+M₀, -MdetM is the checked module M0 with each heap check replaced by a renew (docs/m7.md, round 4) when an earlier heap check of a pointer related to it at distance 0 dominates it and covers its bounds and alignment, rights aside, and both that check's proof and pointer have one definition. The renew reads that proof, the topmost such check on the dominator chain: no…, m7.md, round 4).

• Validator: Q1 is a renew sourcerenew source nanofilA renew source is an earlier proof 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., and P is at a pointer distancepointer distance nanofilThe pointer distance from P1 to P is a constant D such that P's address is P1's plus D modulo 2^64, and P has P1's capability. The validator finds it when both pointers reach one exact base on their guard chains: D is the difference of their offsets from it. from its pointer, inside its span.

• interp.pl: interp:renew_res/4interp.plrenew_res+Res₀, +P, +Mem, -ResdetA renew (docs/m7.md, round 4) of P whose access_res/7 is Res0 yields P, proven, or traps as the check it replaced would: a read-only trap stands, and a freed object traps out of bounds. Any other failure means the earlier check's bounds did not cover this access, which a valid renew rules out, so it is unchecked(span), a broken pass.; Q1 of another capability is uncheckedalias, a failing check not on a freed object uncheckedspan. Rocq: the op Renew, renew_res; Renew.v's renew_not_unchecked and, along runs, run_reuse_checked.

Why it is sound: an object's bounds change only by free, which the flag test catches.