test+docs: property-test the core guarantees; add Guarantees page

docs/concepts/guarantees.md

@@ -0,0 +1,62 @@
+---
+title: Guarantees & invariants
+description: The properties model-ledger guarantees — append-only history, content-addressed snapshots, ordered history, point-in-time reconstruction — each property-tested in CI.
+---
+
+# Guarantees & invariants
+
+A system of record is only as trustworthy as the properties it can promise. These are
+model-ledger's — stated precisely, and **property-tested in CI** against randomized event
+sequences (not just examples). Each guarantee below names the test that enforces it in
+[`tests/test_invariants.py`](https://github.com/block/model-ledger/blob/main/tests/test_invariants.py).
+
+## 1. Append-only
+
+Snapshots are never deleted or modified. Recording an event only ever *appends*; the
+history of a model never shrinks, and every prior snapshot persists byte-for-byte.
+
+- **Contract:** for any sequence of `record()` calls, `len(history)` is non-decreasing and
+  every previously seen `snapshot_hash` remains present and unchanged.
+- **Enforced by:** `test_history_is_append_only`.
+
+## 2. Content-addressed identity (tamper-evident)
+
+A snapshot's hash is derived from its content — the model identity, the timestamp, and the
+payload. Identical content always yields the same hash; any difference in content yields a
+different hash. You cannot alter a recorded payload after the fact without the hash
+diverging from what was stored.
+
+- **Contract:** `snapshot_hash` is a deterministic function of `(model_hash, timestamp,
+  payload)`; equal content ⇒ equal hash, differing content ⇒ differing hash.
+- **Enforced by:** `test_snapshot_hash_is_deterministic_and_content_addressed`.
+
+!!! note "Scope, stated honestly"
+    The hash content-addresses each snapshot individually over `(model_hash, timestamp,
+    payload)`. It is **not yet** a chained Merkle hash that folds in `parent_hash`,
+    `actor`, and `event_type` — so the *sequence* is ordered and individually
+    content-addressed, but not cryptographically linked end-to-end. Strengthening the hash
+    to chain the full event is a deliberate future change (it alters existing hashes, so it
+    will land as its own decision record), not an accidental gap.
+
+## 3. Ordered history
+
+`history()` returns a model's snapshots newest-first by timestamp — a stable, total order
+you can rely on for "what happened, in what sequence."
+
+- **Contract:** the returned list is sorted by `timestamp`, descending.
+- **Enforced by:** `test_history_is_ordered_newest_first`.
+
+## 4. Point-in-time reconstruction
+
+Because nothing is overwritten, `inventory_at(t)` reconstructs the inventory as it stood at
+time `t`: a model appears if and only if it existed at `t`.
+
+- **Contract:** `inventory_at(t)` includes a model iff it was created at or before `t` (and
+  its latest state as of `t` is not a removal).
+- **Enforced by:** `test_point_in_time_reflects_only_models_that_existed`.
+
+---
+
+These four are the foundation the [event-log architecture](architecture.md) trades for —
+see [ADR 0001](../adr/0001-event-log-not-a-registry.md). If a change to the SDK ever broke
+one of them, the property tests would fail the build before it shipped.

mkdocs.yml

@@ -148,6 +148,7 @@ nav:
       - Architecture: concepts/architecture.md
       - DataNode & the graph: concepts/datanode.md
       - Snapshots & the event log: concepts/snapshot.md
+      - Guarantees & invariants: concepts/guarantees.md
       - Composites: concepts/composite.md
   - Guides:
       - Agents (MCP): guides/agents.md

pyproject.toml

@@ -37,6 +37,7 @@ introspect-lightgbm = ["lightgbm>=3.0"]
 dev = [
     "pytest>=8.0",
     "pytest-cov>=5.0",
+    "hypothesis>=6.0",
     "ruff>=0.8",
     "mypy>=1.0",
 ]

tests/test_invariants.py

@@ -0,0 +1,104 @@
+"""Property-based tests for model-ledger's core guarantees.
+
+These prove the claims the event-log architecture rests on — not by example, but
+by generating random event sequences with Hypothesis and asserting the invariants
+hold. They are the executable counterpart to the Guarantees documentation
+(docs/concepts/guarantees.md), which cites this module by name.
+
+Invariants covered:
+  1. Append-only       — history never shrinks; prior snapshots persist unchanged.
+  2. Content-addressed — a snapshot's hash is deterministic from its content, and
+                         differing content yields a differing hash (tamper-evident).
+  3. Ordered history   — history() returns snapshots newest-first by timestamp.
+  4. Point-in-time     — inventory_at(t) reflects only models that existed at t.
+"""
+
+from __future__ import annotations
+
+import json
+from datetime import datetime, timedelta, timezone
+
+from hypothesis import assume, given, settings
+from hypothesis import strategies as st
+
+from model_ledger import Ledger
+from model_ledger.backends.ledger_memory import InMemoryLedgerBackend
+from model_ledger.core.ledger_models import Snapshot
+
+# Safe alphabets keep the focus on the invariants, not unicode-encoding edge cases.
+_TOKEN = st.text(alphabet="abcdefghijklmnopqrstuvwxyz0123456789_-", min_size=1, max_size=12)
+_VALUES = st.one_of(st.integers(), st.booleans(), st.none(), st.text(max_size=16))
+_PAYLOADS = st.dictionaries(_TOKEN, _VALUES, max_size=4)
+_EVENT_SEQ = st.lists(st.tuples(_TOKEN, _PAYLOADS), max_size=10)
+
+
+def _ledger() -> Ledger:
+    return Ledger(backend=InMemoryLedgerBackend())
+
+
+def _register(ledger: Ledger, name: str = "m") -> None:
+    ledger.register(name=name, owner="owner", model_type="ml_model", tier="high", purpose="p")
+
+
+@settings(deadline=None, max_examples=40)
+@given(seq=_EVENT_SEQ)
+def test_history_is_append_only(seq: list[tuple[str, dict]]) -> None:
+    """Recording events never deletes or mutates prior snapshots; history only grows."""
+    ledger = _ledger()
+    _register(ledger)
+    prev_len = len(ledger.history("m"))
+    seen = {s.snapshot_hash for s in ledger.history("m")}
+    for event, payload in seq:
+        ledger.record("m", event=event, payload=payload, actor="actor")
+        history = ledger.history("m")
+        assert len(history) >= prev_len  # never shrinks
+        assert seen <= {s.snapshot_hash for s in history}  # prior snapshots persist unchanged
+        prev_len = len(history)
+        seen = {s.snapshot_hash for s in history}
+
+
+@settings(deadline=None, max_examples=60)
+@given(
+    p1=_PAYLOADS,
+    p2=_PAYLOADS,
+    ts=st.datetimes(timezones=st.just(timezone.utc)),
+    model_hash=_TOKEN,
+)
+def test_snapshot_hash_is_deterministic_and_content_addressed(
+    p1: dict, p2: dict, ts: datetime, model_hash: str
+) -> None:
+    """Same content → same hash (deterministic); different content → different hash."""
+    a = Snapshot(model_hash=model_hash, timestamp=ts, actor="x", event_type="e", payload=p1)
+    b = Snapshot(model_hash=model_hash, timestamp=ts, actor="x", event_type="e", payload=p1)
+    assert a.snapshot_hash == b.snapshot_hash and a.snapshot_hash != ""
+
+    dumps = lambda p: json.dumps(p, sort_keys=True, default=str)  # noqa: E731
+    assume(dumps(p1) != dumps(p2))  # only assert sensitivity when content actually differs
+    c = Snapshot(model_hash=model_hash, timestamp=ts, actor="x", event_type="e", payload=p2)
+    assert c.snapshot_hash != a.snapshot_hash
+
+
+@settings(deadline=None, max_examples=40)
+@given(seq=_EVENT_SEQ)
+def test_history_is_ordered_newest_first(seq: list[tuple[str, dict]]) -> None:
+    """history() returns snapshots in non-increasing timestamp order."""
+    ledger = _ledger()
+    _register(ledger)
+    for event, payload in seq:
+        ledger.record("m", event=event, payload=payload, actor="actor")
+    timestamps = [s.timestamp for s in ledger.history("m")]
+    assert timestamps == sorted(timestamps, reverse=True)
+
+
+@settings(deadline=None, max_examples=30)
+@given(names=st.lists(_TOKEN, unique=True, max_size=5))
+def test_point_in_time_reflects_only_models_that_existed(names: list[str]) -> None:
+    """inventory_at(t) includes a model iff it existed at t."""
+    ledger = _ledger()
+    a_day_ago = datetime.now(timezone.utc) - timedelta(days=1)
+    for name in names:
+        _register(ledger, name)
+    soon = datetime.now(timezone.utc) + timedelta(seconds=1)
+
+    assert {m.name for m in ledger.inventory_at(soon)} == set(names)  # all exist now
+    assert ledger.inventory_at(a_day_ago) == []  # none existed yesterday