# Minerva
Minerva is a `no_std`-first Rust library for causal ordering in distributed
systems.
- `kairos` provides a lock-free Hybrid Logical Clock. Each 128-bit stamp packs
physical time, logical time, a caller-defined kairotic tag, and station
identity.
- `metis` provides causal delivery, exact dot sets, stability tracking,
causal stores, sequence CRDTs, and recorded membership.
- `chronos` provides OS-backed time sources with the optional `std` feature.
Minerva separates mechanism from policy. The crate validates structure,
preserves causal invariants, returns typed refusals, and offers explicit
resource bounds. Callers own trust, retry, conflict resolution, reclamation,
and membership policy.
The crate uses only safe Rust and has `#![forbid(unsafe_code)]`. Property tests,
fuzz targets, Kani models, Creusot proofs, Miri runs, and mutation tests cover
the applicable invariants. See [What is proven](docs/what-is-proven.adoc) for
the exact scope and limits.
## Example
Two replicas write one sequence and converge:
```rust
use minerva::kairos::{Clock, TickCounter};
use minerva::metis::{Anchor, Composer, DotSet, Locus, Rhapsody};
let clock = Clock::with_default_config(TickCounter::new(), 1).unwrap();
let mut ada = Composer::<Rhapsody>::new(1);
let mut bea = Composer::<Rhapsody>::new(2);
// Ada writes one element. The write mints a dot: the element's identity.
let rank = clock.now(0u16);
let owed = ada.owed_to(bea.state().context());
let _ = bea.absorb(1, &owed);
assert_eq!(ada.state().store().order(), bea.state().store().order());
```
[Day one](docs/day-one.adoc) extends this example to a full replicated
document with concurrent edits, removal, and witnessed garbage collection.
## Status
The public API is not stable. Version 2 membership frames remain dormant
until a joint registry decision activates them. Version 1 wire bytes remain
unchanged. See [CHANGELOG.md](CHANGELOG.md) for release notes and migration
rows.
## Features
| `rand` (default) | Adds entropy to contention backoff. Pulls in `std`; disable default features for bare targets. |
| `std` | Enables the `chronos` OS time sources. |
| `instrumentation` | Exposes bounded structural measurements. |
| `timing` | Adds wall-time measurements and enables `instrumentation` and `std`. |
The core requires `alloc`. For bare targets use
`minerva = { version = "0.2", default-features = false }`.
## Documentation
API documentation: [docs.rs/minerva](https://docs.rs/minerva).
Start with [Day one](docs/day-one.adoc) and the [consumer
guide](docs/consumer-guide.adoc). The [documentation guide](DOCS.adoc) maps the
architecture, PRDs, module notes, and glossary.
## License
Minerva is available under the [Apache License 2.0](LICENSE-APACHE) or the
[MIT License](LICENSE-MIT).