 we are in the calling context, the trace leads to an access to the value invalidated in <code>invalidation_trace</code> without further assumptions</p><span class="comment-delim">*)</span></td></tr><tr id="type-access_to_invalid_address.must_be_valid_reason" class="anchored"><td class="def record field"><a href="#type-access_to_invalid_address.must_be_valid_reason" class="anchor"></a><code><span>must_be_valid_reason : <span><a href="../PulseInvalidation/index.html#type-must_be_valid_reason">Invalidation.mu