pub fn carrier_interval_table(
inputs: &ProofLowerInputs<'_>,
) -> HashMap<String, (Interval, bool)>Expand description
ETAP-2 SLICE 0+1: derive, per refinement-via-opaque type in scope, the
constant interval its smart-constructor invariant proves over the
carrier. The table is keyed by the opaque type’s bare Aver name (e.g.
"IntRange"). The bare-i64 MIR pass matches a carrier
parameter/local/return slot against this key — it extracts the bare name
from the slot’s MirParam.ty (which the lowerer fills with the Debug
form Named { id: …, name: "IntRange" }, NOT the bare name; see
bare_named_type in bare_i64) and seeds the slot with the proven bound.
The value is interval_of_invariant(&predicate) — byte-identical to the
bound [populate_refined_type_intervals] persists on each
RefinedTypeDecl (both build the same Predicate from
[refinement_info_for_in_scope] + ProofLowerInputs::resolve_expr and
run the same interval recognizer). No forked logic.
Fail-closed. A type whose invariant the recognizer does not
understand returns interval_known == false; that entry is OMITTED from
the table entirely, so the MIR pass never sees it and the carrier stays
boxed. A carrier whose proven bound does not fits_i64 is also kept
(the table carries the raw (Interval, bool) so the seed site can apply
fits_i64 itself — see carrier_interval in bare_i64).