Module version 

Optimistic concurrency: writes carry a base_version; a stale base yields a verdict, never a silent merge. The part crates/kernel/spec/Version.lean specifies this module.

The mapping from VersionVerdict::Stale to E_VERSION_CONFLICT plus a fresh diff lives with the edit tool; kernel only judges freshness and knows nothing about diffs.

Structs

Version

Monotonic per-subject version; starts at Version::FIRST.

Enums

VersionVerdict

Freshness verdict — exhaustive, not a bool (decision-function shape).

Functions

check_base

Pure freshness judgment. A base ahead of current is caller fiction and reports Stale too: only current is the truth.