Struct RefinedTypeDecl 

pub struct RefinedTypeDecl {
    pub name: String,
    pub carrier_type: String,
    pub carrier_field: String,
    pub predicate_param: String,
    pub invariant: Predicate,
    pub witness: Option<String>,
    pub interval: Option<Interval>,
    pub op_classes: Vec<(String, OpClass)>,
}

A refinement-lifted user type — opaque record with a single carrier field, paired with a validating smart constructor. The presence of this decl in ProofIR.refined_types is the decision: “emit this as a subtype on Lean and a subset type on Dafny”. Backends never re-decide.

Fields

name: String

Source-level type name (e.g. "Natural"). NOT canonicalised — backends emit using the source name; canonical form is the map key.

carrier_type: String

Carrier annotation from the record’s single field (typically "Int"). Drives the Lean Subtype underlying type and the Dafny subset type’s base.

carrier_field: String

Carrier-field source name (e.g. "value"). Lean uses .val to project Subtype values regardless of source name; Dafny’s subset binds the source name in its predicate.

predicate_param: String

Smart constructor’s input parameter name (e.g. "n") — the invariant predicate’s free variable.

invariant: Predicate

Bool predicate that every value of the refined type must satisfy, in terms of predicate_param. Comes from the smart constructor’s match <pred> { true -> Ok(...); false -> Err(...) } subject.

witness: Option<String>

Inhabitation witness: a literal value of carrier_type that the lowerer verified satisfies invariant. Resolved by first trying the smart constructor’s verify block (fromX(K) => Ok(...) for some literal K — verified by the user via aver verify), then evaluating the predicate against small candidates as a fallback.

Why the IR carries this even though only Dafny’s subset type strictly requires a non-emptiness witness: it’s a fact about the type (∃ v : carrier, invariant(v) holds), not a Dafny-specific syntactic obligation. Backends use it as they see fit:

• Dafny: emits type X = v: int | P v witness <W>. Required for the subset type to be inhabited and elaborable.
• Lean: currently unused — propositional Subtype may be empty, so { v : Int // P v } elaborates regardless. Step N+1 could emit a def sample_X : X := ⟨W, by decide⟩ for roundtrip / test convenience.
• Future Z3 / Coq / etc.: same fact, rendered per target.

None when no satisfier was found. Backends that require a witness must either reject the type or fall back to a target- default (Dafny picks 0 and crosses fingers).

interval: Option<Interval>

Constant integer interval over-approximating invariant, as derived by crate::ir::interval::interval_of_invariant from the same predicate. Some([lo, hi]) when the invariant shape was recognized (a comparison / Bool.and against integer literals); None when the analysis declined (unrecognized shape — Bool.or, non-literal bound, structural carrier).

Persisted here so a carrier-lowering codegen recognizer (the next slice of the Int-semantics effort) can read the bound directly off the TypeId-keyed decl — the same identity key the interval analysis uses — without re-running the analysis behind the --explain-passes diagnostic flag. The value is identical to what aver compile --explain-passes reports for the same type; both paths call the one interval analysis.

op_classes: Vec<(String, OpClass)>

Per-arithmetic-op overflow classification, in module-walk order. Each entry pairs the operation’s source name with its crate::ir::interval::OpClass — OverflowFree when every i64 intermediate across the op body provably fits i64 (the carrier-lowering candidate), NeedsWiderScratch / Unbounded otherwise. Empty when the type exposes no carrier arithmetic or when interval is None.

Populated by crate::ir::interval::analyze over the same ProofLowerInputs populate_refined_types consumed, so the classification is byte-identical to the --explain-passes report. The codegen recognizer reads this to flag a carrier “raw-i64-eligible” per op.

Implementations

impl RefinedTypeDecl

pub fn raw_i64_eligible(&self) -> bool

Whether this refined type may have a raw i64 carrier — the gate a later codegen slice will trust to lower the bignum Int carrier to a machine word. Derived ONLY from the persisted Self::interval and Self::op_classes facts; it never re-runs the interval analysis or inspects the invariant syntax.

Returns true IFF, conservatively, the type is provably safe to store and operate on as a raw i64:

• Self::interval is Some — the analysis recognized the invariant shape (a None is the analysis’s conservative decline, never eligible); AND
• that interval fits i64 (crate::ir::interval::Interval::fits_i64), which holds IFF both bounds are finite and within [i64::MIN, i64::MAX]. This single test subsumes “two-sided” (an open / one-sided bound is ±inf, which never fits) and the i64-range check — a Natural ([0, +inf]) or any interval wider than i64 is rejected here; AND
• every entry in Self::op_classes is crate::ir::interval::OpClass::OverflowFree — a single NeedsWiderScratch or Unbounded op means some carrier arithmetic can wrap a raw i64 before the smart constructor’s guard re-validates, so the whole carrier stays bignum.

Anything else → false. This is conservative in exactly the soundness-critical direction: a wrongly-true answer would let slice 4 lower a carrier whose ops can wrap, silently reintroducing the model-vs-runtime gap the whole mechanism exists to close. The predicate declines whenever the facts do not prove safety.

Empty op_classes

A type with a finite-i64 interval but no carrier-reading arithmetic ops (e.g. only fromInt / toInt, which [crate::ir::interval::classify_ops_in_scope] skips) is reported eligible. The decision is defensible because both soundness obligations are met vacuously: storage of any inhabitant fits i64 (it is within the proven interval), and there is no op that could overflow a raw i64 (the all(...) over an empty op set is true). The only thing the raw carrier adds over bignum — an op that must not wrap before the guard — has nothing to apply to. This is “eligible for storage”, which is exactly what the gate asks. If a future op is added to the type, it is re-classified and can demote the type then; the determination is recomputed from the persisted facts every time, never cached.

Trait Implementations

impl Clone for RefinedTypeDecl

fn clone(&self) -> RefinedTypeDecl

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for RefinedTypeDecl

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.