HYDRA scheduler core: multi-source download scheduler state machine with no I/O dependencies.
Key principles:
- Dynamic range partitioning: HTTP byte ranges are tracked client-side, allowing slow or stalled connections to be repartitioned and assigned to faster connections dynamically.
- Liveness: every reachable state has an enabled transition that decreases remaining work within a bounded window.
- Safety: byte coverage invariants are strictly verified without gaps or duplicate allocations.
Safety (coverage_holds) and liveness (liveness_holds) properties are
both verified through property-based testing.