Module idem 

IdemKey: the dedup key for outward actions. The part crates/kernel/spec/Idem.lean specifies this module.

Derivation is the whole point: BLAKE3-XOF(run(16B) || seq(8B LE) || action_canonical) taken as a direct 16-byte output (not a truncation), plus one version byte carried alongside so a future derivation change cannot collide old keys with new ones. No From<Uuid>, no randomness, no timestamps: resume and replay must re-derive the identical key, or the double-payment defense dies exactly on the recovery path.

Structs

Duplicate

A key that was already claimed. The caller answers with what the first claim produced rather than doing the work twice.

IdemGuard

The right to perform one unreplayable side effect, once.

IdemKey

Idempotency key: 16 digest bytes plus the derivation version. Private fields; IdemKey::derive is the only mint.

Constants

IDEM_DERIVE_V

Current derivation-scheme version byte.

Functions

claim

Claims key in the caller’s seen set, handing back the right to act once.