pub fn site_loss_survivors(rf: i64, sites: i64) -> i64Expand description
The replica count that survives the loss of any one site.
Under the round-robin placement, round_robin_load, site 0 is a fullest
site. The contract proves that the result is what the loss of site 0
leaves, and that the loss of any other site leaves at least as many, so it
is the fewest replicas any single site loss leaves. The body computes it as
rf - ceil(rf / sites); the proof derives that ceiling from the model
rather than taking it as the definition.
An operator reads this number to pick min.insync.replicas. Three replicas
on three sites leave 2, because each site holds one replica. Three replicas
on two sites leave 1, because two of the three replicas share a site. One
site leaves 0, because the loss of that site is the loss of the partition.
The proof assumes both rf and sites are in 1..=1024. Normal Rust
builds do not check that proof precondition.
ยงPanics
Panics when sites is zero. Arithmetic outside the proof bounds can panic
when overflow checks are enabled.