Function active_lease_fraction 

pub open spec fn active_lease_fraction<K, W>(
    active: Map<nat, RcuActiveReadLeaseRecord<K, W>>,
    key: K,
    upto: nat,
) -> real

{
    if upto == 0 {
        0real
    } else {
        let id = (upto - 1) as nat;
        active_lease_fraction(active, key, id)
            + if active.contains_key(id) && active[id].key() == key {
                active[id].fraction()
            } else {
                0real
            }
    }
}

Sum of active lease fractions for key among record IDs below upto.