test(adr-0180): T-1..T-4 Delta-CRDT pre-refactor obligations (Python, green) (#463)
ADR-0180 §1.5.4 + CLAUDE.md work-sequencing item 5 require these four
properties green on main before any core-rs/src/vault.rs change. They are
also the foundation ADR-0181 PR-5 (audio Delta-CRDT wiring) rides on.
T-1 set-equality of vault writes under shuffled ingest (+ idempotent
re-ingest at the content-addressed layer)
T-2 trace-hash invariance to vault order, + recall result-set invariance
to insertion order (the genuinely-failable half)
T-3 versor_apply non-commutativity (negative guard)
T-4 ProjectionHead.project purity across calls and threads
Findings (docs/audit/ADR-0180-t1-t4-findings.md):
- compute_trace_hash folds only vault_hits (a count), NOT vault contents, so
ADR-0180 §1.5.3's "re-sort vault state in content-addressed order" is
currently vacuous at the trace-hash layer; the live order-invariance
obligation is at recall() (result-set + count). Recommend amending §1.5.3.
- equal-score recall ties are index-sensitive; the Merge Kernel needs a
content-addressed tiebreak (mirrors ADR-0181 §2.2 merge key). Recommend
amending §2.2.
- append is genuinely semilattice-eligible; versor_apply is non-commutative.
7 passed; smoke suite green. No runtime/core mutation — tests + audit only.
This commit is contained in:
parent
7451e7cd74
commit
cecf7b82cc
2 changed files with 343 additions and 0 deletions
89
docs/audit/ADR-0180-t1-t4-findings.md
Normal file
89
docs/audit/ADR-0180-t1-t4-findings.md
Normal file
|
|
@ -0,0 +1,89 @@
|
||||||
|
# ADR-0180 §1.5.4 — T-1…T-4 Foundation: Findings
|
||||||
|
|
||||||
|
**Date:** 2026-05-29
|
||||||
|
**Branch:** `adr-0180-crdt-t1-t4-foundation`
|
||||||
|
**Tests:** `tests/test_adr_0180_crdt_foundation.py`
|
||||||
|
**Scope:** the Python-side pre-refactor obligations that must be green on `main`
|
||||||
|
before any `core-rs/src/vault.rs` change (CLAUDE.md work-sequencing item 5; ADR-0180 §1.5.4).
|
||||||
|
Also the foundation ADR-0181 PR-5 (audio Delta-CRDT wiring) rides on.
|
||||||
|
|
||||||
|
## Status
|
||||||
|
|
||||||
|
All four obligations are now covered and green (7 tests, all passing). Below
|
||||||
|
are the substantive findings discovered while grounding them against the
|
||||||
|
actual substrate, not the abstract baseline ADR-0180 §1.5 assumed.
|
||||||
|
|
||||||
|
## Finding 1 (load-bearing) — `compute_trace_hash` does not fold vault contents
|
||||||
|
|
||||||
|
ADR-0180 §1.5.3 point 2 worried that "the trace-hash reduction must consume
|
||||||
|
vault state in a content-addressed order … not in wall-clock arrival order"
|
||||||
|
and that §4.3 "cannot hold under [a time-driven flush] policy unless the
|
||||||
|
*hashing* step re-sorts."
|
||||||
|
|
||||||
|
**Actual code** (`core/cognition/trace.py:27`): `compute_trace_hash` folds
|
||||||
|
`vault_hits` — an **int count** — plus a serialized prefix of upstream turn
|
||||||
|
fields. It does **not** fold vault *contents* at all.
|
||||||
|
|
||||||
|
**Consequence:** the §1.5.3 "re-sort vault state in content-addressed order"
|
||||||
|
obligation is currently **vacuous at the trace-hash layer** — there is nothing
|
||||||
|
order-sensitive about vault contents in the payload to re-sort, because contents
|
||||||
|
are not in the payload. The CRDT merge may reorder the vault deque freely and
|
||||||
|
`compute_trace_hash` is unaffected, *provided* the recalled result *count*
|
||||||
|
(`vault_hits`) is order-invariant.
|
||||||
|
|
||||||
|
This shifts where the real obligation lives:
|
||||||
|
|
||||||
|
- It is **not** at `compute_trace_hash` today (T-2a confirms count-stability).
|
||||||
|
- It **is** at `recall()` — the count and content of recall results must be
|
||||||
|
order-invariant under a reordered deque. T-2b (`recall_result_set_invariant
|
||||||
|
_to_insertion_order`) pins this for distinct-score entries and is the
|
||||||
|
genuinely-failable half of T-2.
|
||||||
|
|
||||||
|
The §1.5.3 re-sort obligation becomes live only if/when vault contents (not just
|
||||||
|
a count) enter the trace-hash payload. **Recommendation:** ADR-0180 §1.5.3
|
||||||
|
should be amended to say the content-addressed-sort requirement applies to the
|
||||||
|
*recall result set* and to any *future* contents-bearing hash, not to today's
|
||||||
|
count-based `compute_trace_hash`.
|
||||||
|
|
||||||
|
## Finding 2 (edge) — equal-score recall ties are index-sensitive
|
||||||
|
|
||||||
|
`vault_recall` breaks score ties by ascending index (`vault/store.py`). Index
|
||||||
|
is assigned by storage order, so two entries with *exactly equal* CGA inner
|
||||||
|
scores can surface in an order that depends on insertion order. For distinct
|
||||||
|
scores (the common case, and what T-2b asserts) recall is order-invariant.
|
||||||
|
|
||||||
|
**Consequence for the CRDT merge:** the merge must content-address tie-scored
|
||||||
|
entries (e.g. sort by versor bytes) before assigning deque indices, or the
|
||||||
|
sub-50ms reorder window (ADR-0180 §3.2) could change which of two equal-score
|
||||||
|
entries a recall returns. This is exactly the role ADR-0181 §2.2's
|
||||||
|
`(canonical, ir, projection)` merge key plays for audio — it gives a total,
|
||||||
|
content-addressed order independent of arrival. **Recommendation:** ADR-0180's
|
||||||
|
Merge Kernel spec (§2.2) should adopt a content-addressed tiebreak for the
|
||||||
|
general path, mirroring ADR-0181 §2.2.
|
||||||
|
|
||||||
|
## Finding 3 (confirmed) — append is genuinely semilattice-eligible
|
||||||
|
|
||||||
|
T-1 confirms `VaultStore.store` is set-equal under any write permutation
|
||||||
|
(append never dedups/drops/order-mutates), and re-ingest is set-stable at the
|
||||||
|
content-addressed layer. This validates ADR-0180 §1.5.2 row 5 ("vault/store
|
||||||
|
write … commutative, associative, idempotent — semilattice-eligible") against
|
||||||
|
the real implementation. Note the deque itself appends duplicates (length
|
||||||
|
grows on re-ingest); idempotence holds at the content-addressed layer the CRDT
|
||||||
|
merge dedups on, not at the raw deque.
|
||||||
|
|
||||||
|
## Finding 4 (confirmed) — `versor_apply` is non-commutative; barrier is justified
|
||||||
|
|
||||||
|
T-3 confirms the sandwich `V·F·rev(V)` does not commute. This is the load
|
||||||
|
under ADR-0181 §2.1: in-chunk audio composition is a serialization barrier
|
||||||
|
*because* this product is order-sensitive, and only the order-invariant
|
||||||
|
`AudioCompilationUnit` crosses into the sharded merge layer. If a refactor ever
|
||||||
|
makes `versor_apply` commutative, T-3 fails loudly before the substrate can
|
||||||
|
wrongly shard it.
|
||||||
|
|
||||||
|
## Net
|
||||||
|
|
||||||
|
- T-1, T-3, T-4 hold against the real code as ADR-0180 §1.5.4 assumed.
|
||||||
|
- T-2 holds, but the obligation moved: the order-invariance that matters today
|
||||||
|
lives at `recall()` (result-set + count), not at `compute_trace_hash` (which
|
||||||
|
is count-only). Two small amendments to ADR-0180 §1.5.3 and §2.2 are
|
||||||
|
recommended above. Neither blocks the substrate; both sharpen it.
|
||||||
254
tests/test_adr_0180_crdt_foundation.py
Normal file
254
tests/test_adr_0180_crdt_foundation.py
Normal file
|
|
@ -0,0 +1,254 @@
|
||||||
|
"""
|
||||||
|
ADR-0180 §1.5.4 — Pre-refactor test obligations for the Delta-CRDT substrate.
|
||||||
|
|
||||||
|
CLAUDE.md work-sequencing item 5 ("Rust backend parity only after Python
|
||||||
|
semantics are locked by tests") and ADR-0180 §1.5.4 both require these four
|
||||||
|
properties to exist as Python tests and be GREEN on `main` *before* any change
|
||||||
|
to `core-rs/src/vault.rs`. They are also the foundation ADR-0181 PR-5 (audio
|
||||||
|
Delta-CRDT wiring) rides on — the audio A-1..A-6 obligations are written as
|
||||||
|
analogs of these.
|
||||||
|
|
||||||
|
T-1 Set-equality of vault writes under shuffled single-thread ingest.
|
||||||
|
T-2 compute_trace_hash invariance under set-equal vault states with
|
||||||
|
identical upstream serialized prefixes.
|
||||||
|
T-3 versor_apply non-commutativity (negative guard — must NOT silently
|
||||||
|
become commutative, which would let the substrate wrongly shard it).
|
||||||
|
T-4 ProjectionHead.project purity: same S -> byte-identical (32,) across
|
||||||
|
repeated calls and across threads.
|
||||||
|
|
||||||
|
T-1 and T-2 are the load-bearing ones (ADR-0180 §1.5.4). T-3 and T-4 are
|
||||||
|
guards against silent drift.
|
||||||
|
|
||||||
|
Per CLAUDE.md §Schema-Defined Proof Obligations, each test must be able to
|
||||||
|
*meaningfully fail* under the violation it names — see the inline notes.
|
||||||
|
"""
|
||||||
|
|
||||||
|
from __future__ import annotations
|
||||||
|
|
||||||
|
import itertools
|
||||||
|
from concurrent.futures import ThreadPoolExecutor
|
||||||
|
|
||||||
|
import numpy as np
|
||||||
|
|
||||||
|
from algebra.versor import unitize_versor, versor_apply
|
||||||
|
from core.cognition.trace import compute_trace_hash
|
||||||
|
from sensorium.protocol import CL41_DIM, ModalityVocabulary
|
||||||
|
from sensorium.adapters.text import TextProjectionHead
|
||||||
|
from vault.store import VaultStore
|
||||||
|
from teaching.epistemic import EpistemicStatus
|
||||||
|
|
||||||
|
|
||||||
|
# ---------------------------------------------------------------------------
|
||||||
|
# Helpers
|
||||||
|
# ---------------------------------------------------------------------------
|
||||||
|
|
||||||
|
def _unit_versor(seed: int) -> np.ndarray:
|
||||||
|
"""A reproducible positive-norm Cl(4,1) grade-1 unit versor.
|
||||||
|
|
||||||
|
Mirrors the construction idiom in tests/test_versor_closure.py: a grade-1
|
||||||
|
vector with its e5 component bounded below the four-space norm so that
|
||||||
|
V * reverse(V) = +1.
|
||||||
|
"""
|
||||||
|
rng = np.random.default_rng(seed)
|
||||||
|
vec4 = rng.standard_normal(4).astype(np.float32)
|
||||||
|
norm4 = float(np.linalg.norm(vec4))
|
||||||
|
if norm4 < 1e-6:
|
||||||
|
vec4[0] = 1.0
|
||||||
|
norm4 = 1.0
|
||||||
|
vec = np.zeros(5, dtype=np.float32)
|
||||||
|
vec[:4] = vec4
|
||||||
|
vec[4] = 0.25 * norm4 * np.tanh(float(rng.standard_normal()))
|
||||||
|
mv = np.zeros(CL41_DIM, dtype=np.float32)
|
||||||
|
mv[1:6] = vec
|
||||||
|
return unitize_versor(mv)
|
||||||
|
|
||||||
|
|
||||||
|
def _versor_bytes(v: np.ndarray) -> bytes:
|
||||||
|
return np.asarray(v, dtype=np.float32).tobytes()
|
||||||
|
|
||||||
|
|
||||||
|
def _store_all(pairs: list[tuple[np.ndarray, dict]]) -> VaultStore:
|
||||||
|
"""Store (versor, metadata) pairs into a fresh vault.
|
||||||
|
|
||||||
|
reproject_interval=0 disables the periodic null-reprojection so the test
|
||||||
|
isolates the *append* semilattice (ADR-0180 §1.5.2 row 5) rather than
|
||||||
|
reprojection bookkeeping.
|
||||||
|
"""
|
||||||
|
store = VaultStore(reproject_interval=0)
|
||||||
|
for F, meta in pairs:
|
||||||
|
store.store(F, meta, epistemic_status=EpistemicStatus.SPECULATIVE)
|
||||||
|
return store
|
||||||
|
|
||||||
|
|
||||||
|
def _vault_contents_set(store: VaultStore) -> set[tuple[bytes, str]]:
|
||||||
|
"""Content-addressed view of vault state: {(versor_bytes, status)}.
|
||||||
|
|
||||||
|
This is the 'as a set, not as a sequence' projection ADR-0180 §1.5.3
|
||||||
|
point 1 requires the sequential and concurrent runs to agree on.
|
||||||
|
"""
|
||||||
|
return {
|
||||||
|
(_versor_bytes(v), m.get("epistemic_status", "speculative"))
|
||||||
|
for v, m in zip(store._versors, store._metadata)
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
# ---------------------------------------------------------------------------
|
||||||
|
# T-1 — set-equality of vault writes under shuffled ingest (load-bearing)
|
||||||
|
# ---------------------------------------------------------------------------
|
||||||
|
|
||||||
|
def test_t1_vault_writes_set_equal_under_permutation():
|
||||||
|
"""For any ingest sequence and any permutation, vault contents are equal
|
||||||
|
*as a set*. This is the property that makes write-accumulation
|
||||||
|
semilattice-eligible (ADR-0180 §1.5.2 row 5 / §2.2 commutativity).
|
||||||
|
|
||||||
|
Fails loudly if store() ever dedups, drops, or order-mutates entries.
|
||||||
|
"""
|
||||||
|
pairs = [
|
||||||
|
(_unit_versor(s), {"src": f"entry-{s}"})
|
||||||
|
for s in range(8)
|
||||||
|
]
|
||||||
|
canonical = _vault_contents_set(_store_all(pairs))
|
||||||
|
|
||||||
|
# Exercise several distinct permutations of the same multiset of writes.
|
||||||
|
perms = list(itertools.islice(itertools.permutations(range(len(pairs))), 0, 5040, 720))
|
||||||
|
for perm in perms:
|
||||||
|
shuffled = [pairs[i] for i in perm]
|
||||||
|
assert _vault_contents_set(_store_all(shuffled)) == canonical
|
||||||
|
|
||||||
|
|
||||||
|
def test_t1_idempotent_reingest_is_set_stable():
|
||||||
|
"""Re-ingesting an already-stored entry keeps the content-addressed set
|
||||||
|
stable (the idempotence leg of the join semilattice, ADR-0180 §2.2).
|
||||||
|
|
||||||
|
Note: the vault deque itself appends duplicates (len grows); idempotence
|
||||||
|
is asserted at the *content-addressed* layer the CRDT merge dedups on,
|
||||||
|
which is exactly the layer ADR-0181 §2.2 keys audio deltas by.
|
||||||
|
"""
|
||||||
|
pairs = [(_unit_versor(s), {"src": f"e{s}"}) for s in range(4)]
|
||||||
|
once = _vault_contents_set(_store_all(pairs))
|
||||||
|
twice = _vault_contents_set(_store_all(pairs + pairs))
|
||||||
|
assert once == twice
|
||||||
|
|
||||||
|
|
||||||
|
# ---------------------------------------------------------------------------
|
||||||
|
# T-2 — trace-hash invariance under set-equal vault states (load-bearing)
|
||||||
|
# ---------------------------------------------------------------------------
|
||||||
|
|
||||||
|
def test_t2_trace_hash_invariant_to_vault_order():
|
||||||
|
"""compute_trace_hash is invariant to the *order* vault entries were
|
||||||
|
written, given identical upstream serialized fields.
|
||||||
|
|
||||||
|
FINDING (recorded in docs/audit/ADR-0180-t1-t4-findings.md): the current
|
||||||
|
compute_trace_hash folds only `vault_hits` (an int count) plus the
|
||||||
|
serialized upstream prefix — it does NOT fold vault *contents*. So
|
||||||
|
ADR-0180 §1.5.3 point 2 ("the hashing step must re-sort vault state in
|
||||||
|
content-addressed order") is currently *vacuous at the trace-hash layer*:
|
||||||
|
there is nothing order-sensitive to re-sort because contents are not in
|
||||||
|
the payload. The obligation becomes live only if vault contents later
|
||||||
|
enter the payload. This test pins that the count-based hash is stable.
|
||||||
|
"""
|
||||||
|
def _hash(vault_hits: int) -> str:
|
||||||
|
return compute_trace_hash(
|
||||||
|
input_text="what is truth",
|
||||||
|
filtered_tokens=("truth",),
|
||||||
|
surface="truth is coherent",
|
||||||
|
walk_surface="truth",
|
||||||
|
articulation_surface="truth is coherent",
|
||||||
|
dialogue_role="assistant",
|
||||||
|
versor_condition=1e-9,
|
||||||
|
vault_hits=vault_hits,
|
||||||
|
intent_tag="definition",
|
||||||
|
)
|
||||||
|
|
||||||
|
assert _hash(3) == _hash(3)
|
||||||
|
# Different hit COUNT must change the hash (count is load-bearing).
|
||||||
|
assert _hash(4) != _hash(3)
|
||||||
|
|
||||||
|
|
||||||
|
def test_t2_recall_result_set_invariant_to_insertion_order():
|
||||||
|
"""The genuinely-failable half of T-2: with distinct scores, recall
|
||||||
|
returns the same result set (by content) regardless of insertion order.
|
||||||
|
|
||||||
|
This is what guarantees `vault_hits` (the count folded into the trace
|
||||||
|
hash) AND the recalled content are order-invariant across a CRDT merge
|
||||||
|
that reorders the deque. Fails if the recall scan or its tiebreak is
|
||||||
|
corrupted by storage order.
|
||||||
|
|
||||||
|
(Tie-scored entries are deliberately avoided: ascending-index tiebreak is
|
||||||
|
index-sensitive, so equal-score entries are an order-dependent edge the
|
||||||
|
CRDT merge must content-address — noted in the findings doc.)
|
||||||
|
"""
|
||||||
|
versors = [_unit_versor(s) for s in range(6)]
|
||||||
|
query = versors[0]
|
||||||
|
|
||||||
|
forward = VaultStore(reproject_interval=0)
|
||||||
|
for v in versors:
|
||||||
|
forward.store(v, {}, epistemic_status=EpistemicStatus.SPECULATIVE)
|
||||||
|
|
||||||
|
reverse_store = VaultStore(reproject_interval=0)
|
||||||
|
for v in reversed(versors):
|
||||||
|
reverse_store.store(v, {}, epistemic_status=EpistemicStatus.SPECULATIVE)
|
||||||
|
|
||||||
|
fwd = {_versor_bytes(r["versor"]) for r in forward.recall(query, top_k=3)}
|
||||||
|
rev = {_versor_bytes(r["versor"]) for r in reverse_store.recall(query, top_k=3)}
|
||||||
|
assert fwd == rev
|
||||||
|
assert len(fwd) == 3 # count (→ vault_hits) is stable
|
||||||
|
|
||||||
|
|
||||||
|
# ---------------------------------------------------------------------------
|
||||||
|
# T-3 — versor_apply non-commutativity (negative guard)
|
||||||
|
# ---------------------------------------------------------------------------
|
||||||
|
|
||||||
|
def test_t3_versor_apply_is_non_commutative():
|
||||||
|
"""The sandwich V·F·rev(V) is non-commutative (ADR-0180 §1.5.2 row 3).
|
||||||
|
|
||||||
|
This negative guard exists so a future refactor that accidentally makes
|
||||||
|
versor_apply commutative is caught HERE, rather than silently masked by
|
||||||
|
the CRDT substrate sharding an operation that is not order-invariant.
|
||||||
|
ADR-0181 §2.1 relies on this: in-chunk composition is the serialization
|
||||||
|
barrier *precisely because* this product does not commute.
|
||||||
|
"""
|
||||||
|
V1 = _unit_versor(11)
|
||||||
|
V2 = _unit_versor(23)
|
||||||
|
F = _unit_versor(101)
|
||||||
|
|
||||||
|
ab = versor_apply(V1, versor_apply(V2, F))
|
||||||
|
ba = versor_apply(V2, versor_apply(V1, F))
|
||||||
|
|
||||||
|
assert not np.allclose(ab, ba, atol=1e-6), (
|
||||||
|
"versor_apply became commutative — the Delta-CRDT substrate must NOT "
|
||||||
|
"shard versor_apply; see ADR-0180 §1.5.2."
|
||||||
|
)
|
||||||
|
|
||||||
|
|
||||||
|
# ---------------------------------------------------------------------------
|
||||||
|
# T-4 — ProjectionHead.project purity (negative guard)
|
||||||
|
# ---------------------------------------------------------------------------
|
||||||
|
|
||||||
|
def _en_head() -> tuple[TextProjectionHead, str]:
|
||||||
|
vocab = ModalityVocabulary()
|
||||||
|
point = _unit_versor(7)
|
||||||
|
vocab.register_point("beginning", point)
|
||||||
|
return TextProjectionHead(vocab), "beginning"
|
||||||
|
|
||||||
|
|
||||||
|
def test_t4_projection_is_pure_across_calls():
|
||||||
|
"""Same S -> byte-identical (32,) float32 across repeated calls
|
||||||
|
(ADR-0180 T-4). Fails if any hidden state leaks into project()."""
|
||||||
|
head, token = _en_head()
|
||||||
|
v1 = head.project(token)
|
||||||
|
v2 = head.project(token)
|
||||||
|
assert v1.shape == (CL41_DIM,)
|
||||||
|
assert v1.dtype == np.float32
|
||||||
|
assert np.array_equal(v1, v2)
|
||||||
|
|
||||||
|
|
||||||
|
def test_t4_projection_is_pure_across_threads():
|
||||||
|
"""Same S -> byte-identical (32,) across threads. The audio
|
||||||
|
ProjectionHead (ADR-0181) inherits this purity requirement so a delayed
|
||||||
|
CRDT merge can never change what a thread-local arena compiled
|
||||||
|
(ADR-0181 §2.4)."""
|
||||||
|
head, token = _en_head()
|
||||||
|
with ThreadPoolExecutor(max_workers=8) as pool:
|
||||||
|
results = list(pool.map(lambda _: head.project(token).tobytes(), range(32)))
|
||||||
|
assert len(set(results)) == 1
|
||||||
Loading…
Reference in a new issue