Land M3 (Agent F): make criteria 1 & 4 honest
The audit flagged Agent F's criterion 1 (convergence) and criterion 4
(serialization) as testing the reducer-bookkeeping projection
(MaterializedState) while claiming to be full-Score gates. This makes them
honest, per item 4 of the v0 follow-up plan.
Criterion 1 — real-Score convergence:
- generators::graph_edit_session builds a real ~50-bar, two-voice edit
session targeting a base Score's actual voices (so it survives reduce_onto,
which rejects unknown voices).
- convergence::{assert_graph_convergence, run_graph_convergence} reduce that
session onto a real epiphany_core::Score via OperationSet::reduce_onto and
assert the entire GraphMaterialization (graph + bookkeeping) is identical
across delivery orders, passes check_invariants, and genuinely grows both
voices (non-vacuity).
- acceptance criterion_1_convergence now drives this; the former bookkeeping
convergence is retained and renamed reducer_bookkeeping_convergence.
Criterion 4 — honest serialization tiers:
- criterion_4_canonical_serialization_stability keeps the real typed/manifest
round-trips; the MaterializedState round-trip is split out as
reducer_bookkeeping_serialization.
- full_score_materialization_is_reproducible asserts the materialized Score is
reproducible across orders (the determinism precondition for a byte codec),
achievable without the codec.
- criterion_4_full_score_byte_roundtrip is #[ignore]'d pending item 5's
whole-score codec (visible as ignored, never falsely green).
Negative regression guards (src/negative.rs): one guard per audited M1 defect
(inverted causal/HLC order, missing predecessor via vector, HLC 100/200/50
quarantine-from-0, tx rollback of member conflicts, causally-ordered
same-position non-promotion, partial-duration overlap), driven through the real
epiphany_ops API with explicit negative controls. Wired into acceptance and the
conformance suite. Crate/README docs updated to match.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This commit is contained in:
parent
e9c4bad7a6
commit
9b0d3e8e2c
|
|
@ -11,12 +11,20 @@ It provides:
|
||||||
(`epiphany-determinism`), B (`epiphany-core`), C (`epiphany-ops`), D
|
(`epiphany-determinism`), B (`epiphany-core`), C (`epiphany-ops`), D
|
||||||
(`epiphany-bundle`), and E (`epiphany-layout-ir`). Agent B's score-graph
|
(`epiphany-bundle`), and E (`epiphany-layout-ir`). Agent B's score-graph
|
||||||
generators/shrinkers are re-exported as `generators::graph`.
|
generators/shrinkers are re-exported as `generators::graph`.
|
||||||
- **The canonical round-trip harness** (`roundtrip`) — v0 acceptance criterion 4.
|
- **The canonical round-trip harness** (`roundtrip`) — v0 acceptance criterion 4
|
||||||
- **The CRDT convergence harness** (`convergence`) — criteria 1 and 5.
|
(typed values + bundle container; the bookkeeping `MaterializedState` round-trip
|
||||||
|
is retained as `assert_reduction_serialization_stable`).
|
||||||
|
- **The CRDT convergence harness** (`convergence`) — criteria 1 and 5. Criterion
|
||||||
|
1 proper is **real-Score** convergence through `reduce_onto`
|
||||||
|
(`run_graph_convergence`); the byte-canonical bookkeeping-projection
|
||||||
|
convergence (`assert_convergence`) backs criterion 5.
|
||||||
- **The equivocation harness** (`equivocation`) — criterion 3.
|
- **The equivocation harness** (`equivocation`) — criterion 3.
|
||||||
- **The crash-recovery harness** (`bundle_harness`) — Agent D's gate, criterion 2.
|
- **The crash-recovery harness** (`bundle_harness`) — Agent D's gate, criterion 2.
|
||||||
- **The manifest-selection harness** (`bundle_harness`).
|
- **The manifest-selection harness** (`bundle_harness`).
|
||||||
- **The layout round-trip harness** (`layout_stub`) — criterion 6.
|
- **The layout round-trip harness** (`layout_stub`) — criterion 6.
|
||||||
|
- **The audit regression guards** (`negative`) — one guard per defect the Agent C
|
||||||
|
framework audit surfaced (the M1 fixes), so a regression trips this suite
|
||||||
|
directly.
|
||||||
|
|
||||||
## All harnesses are real
|
## All harnesses are real
|
||||||
|
|
||||||
|
|
@ -43,9 +51,32 @@ signature; the provenance-preservation contract is implemented and tested inside
|
||||||
that crate. (The "stub" in the module name now refers to the spec-sanctioned
|
that crate. (The "stub" in the module name now refers to the spec-sanctioned
|
||||||
*stub constraint solver*, not to a stubbed crate.)
|
*stub constraint solver*, not to a stubbed crate.)
|
||||||
|
|
||||||
|
## Criterion 1: real-Score vs. reducer-bookkeeping convergence
|
||||||
|
|
||||||
|
Criterion 1 proper (`convergence::run_graph_convergence`, the acceptance
|
||||||
|
`criterion_1_convergence` test) is **real-Score** convergence: a real ~50-bar,
|
||||||
|
two-voice base `epiphany_core::Score` is edited by two replicas through
|
||||||
|
`OperationSet::reduce_onto`, and the entire materialized graph — arena, voices,
|
||||||
|
tombstones, cross-cutting, *and* the bookkeeping state — must be **identical**
|
||||||
|
under every delivery order, pass `check_invariants`, and genuinely grow both
|
||||||
|
edited voices (non-vacuity). The session targets the base's actual voice ids
|
||||||
|
(`generators::graph_edit_session`), so it exercises the integration point, not a
|
||||||
|
synthetic id space.
|
||||||
|
|
||||||
|
The earlier, narrower gate is retained and honestly renamed
|
||||||
|
(`reducer_bookkeeping_convergence`): it converges the byte-canonical
|
||||||
|
**bookkeeping projection** (`OperationSet::reduce` →
|
||||||
|
`MaterializedState::canonical_bytes`) — the Chapter 6 §6.3 ledger (effects,
|
||||||
|
conflicts, anomalies, tombstones, spellings, pending), not the full musical
|
||||||
|
graph. It still backs criterion 5 and proves causal-first ordering
|
||||||
|
(`convergence::assert_causal_order_respected`,
|
||||||
|
`run_authoritative_reduction_gate`). The bookkeeping two-staff scenario remains
|
||||||
|
*instantiated* — a real ~50-bar (`TWO_STAFF_BARS`) session whose staves are
|
||||||
|
asserted populated by `generators::assert_two_staff_populated`, not just modeled.
|
||||||
|
|
||||||
## Criterion 4: what is and isn't tested
|
## Criterion 4: what is and isn't tested
|
||||||
|
|
||||||
Criterion 4 has two qualitatively different tiers:
|
Criterion 4 has three tiers — two asserted now, one pending item 5:
|
||||||
|
|
||||||
- **Real decode round-trips** (these catch decoder / canonicalization defects):
|
- **Real decode round-trips** (these catch decoder / canonicalization defects):
|
||||||
the generic `CanonicalEncode`/`CanonicalDecode` property swept across every
|
the generic `CanonicalEncode`/`CanonicalDecode` property swept across every
|
||||||
|
|
@ -58,33 +89,31 @@ Criterion 4 has two qualitatively different tiers:
|
||||||
(`assert_manifest_decode_rejects_corruption`,
|
(`assert_manifest_decode_rejects_corruption`,
|
||||||
`assert_header_decode_rejects_corruption`).
|
`assert_header_decode_rejects_corruption`).
|
||||||
|
|
||||||
- **A real score-state decode tier** (`assert_reduction_serialization_stable`): a real
|
- **A reducer-bookkeeping serialization tier** (`reducer_bookkeeping_serialization`,
|
||||||
`OperationSet` is reduced to its `MaterializedState::canonical_bytes()` — the
|
via `assert_reduction_serialization_stable`): a real `OperationSet` is reduced
|
||||||
canonical serialized score state (Chapter 6: *"the materialized graph is a
|
to its `MaterializedState::canonical_bytes()` — the canonical *bookkeeping*
|
||||||
deterministic reduction of the operation set"*) — which is stored as a
|
state, **not** the whole musical `Score` — which is stored as a `Snapshot`
|
||||||
`Snapshot` chunk referenced by the manifest's `canonical_base` (its correct
|
chunk referenced by the manifest's `canonical_base`, survives the bundle's
|
||||||
semantic home), survives the bundle's content-addressed store (hash-verified on
|
content-addressed store (hash-verified on reopen), decodes through
|
||||||
reopen), decodes through `MaterializedState::decode_canonical`, compares
|
`MaterializedState::decode_canonical`, compares structurally with the original
|
||||||
structurally with the original reduction, and re-serializes byte-identically.
|
reduction, and re-serializes byte-identically. The decoder validates nested
|
||||||
The decoder validates nested tags, lengths, primitive values, canonical form,
|
tags, lengths, primitive values, canonical form, and trailing bytes. Musical
|
||||||
and trailing bytes. Musical sensitivity is proven two ways:
|
sensitivity is proven two ways:
|
||||||
`assert_content_mutation_changes_serialization` (a cloned operation set with
|
`assert_content_mutation_changes_serialization` (a cloned operation set with
|
||||||
**identical** ids/stamps/causal contexts but one changed payload reduces to
|
**identical** ids/stamps/causal contexts but one changed payload reduces to
|
||||||
*different* bytes — the rebuttal to an id-only serializer) and
|
*different* bytes — the rebuttal to an id-only serializer) and
|
||||||
`assert_distinct_scores_serialize_differently`.
|
`assert_distinct_scores_serialize_differently`. The materialized real `Score`
|
||||||
|
itself is shown reproducible today (`full_score_materialization_is_reproducible`,
|
||||||
|
structural equality across delivery orders) — the determinism precondition a
|
||||||
|
byte codec depends on.
|
||||||
|
|
||||||
The convergence harness additionally proves the histories it generates honor the
|
- **The full-`Score` byte round-trip is pending item 5 (Agent B).** No
|
||||||
**HLC authoring contract** and that the canonical order is genuinely
|
whole-score canonical codec (`CanonicalEncode`/`CanonicalDecode for Score`)
|
||||||
**causal-first** (`convergence::assert_causal_order_respected`), not merely
|
exists yet, so `criterion_4_full_score_byte_roundtrip` is marked `#[ignore]`
|
||||||
permutation-invariant. `convergence::run_authoritative_reduction_gate` is the
|
(visible as *ignored*, never falsely green) rather than asserted on the
|
||||||
suite's authoritative criterion-1/5 gate: it asserts causal-order correctness
|
bookkeeping projection and passed off as a whole-Score gate. When item 5 lands
|
||||||
*and* reduction determinism over many conformant sets. Agent C's re-exported
|
the codec, drop the attribute and assert the real byte cycle through a bundle
|
||||||
`ops_reduction_determinism_fuzz` is run in addition; its baseline generator now
|
snapshot.
|
||||||
uses causal HLC authoring and retains explicit anomaly injection. The
|
|
||||||
criterion-1 two-staff scenario is
|
|
||||||
*instantiated* — a real ~50-bar (`TWO_STAFF_BARS`), two-staff editing session
|
|
||||||
whose staves are asserted populated by `generators::assert_two_staff_populated`,
|
|
||||||
not just modeled.
|
|
||||||
|
|
||||||
## Decisions (per QUICKSTART "Make each one once and document it")
|
## Decisions (per QUICKSTART "Make each one once and document it")
|
||||||
|
|
||||||
|
|
@ -103,10 +132,14 @@ not just modeled.
|
||||||
|
|
||||||
Per the QUICKSTART, implementation-discovered gaps are batched, not improvised:
|
Per the QUICKSTART, implementation-discovered gaps are batched, not improvised:
|
||||||
|
|
||||||
- **Whole-graph (`epiphany_core::Score`) wire format.** Criterion 4 is now a real
|
- **Whole-graph (`epiphany_core::Score`) wire format — pending item 5 (Agent B).**
|
||||||
decode round-trip at the canonical Chapter-6 `MaterializedState` layer. A
|
Criterion 4 is a real decode round-trip at the canonical Chapter-6
|
||||||
separate direct wire format for the richer core `Score` remains owned by the
|
`MaterializedState` layer; the materialized `Score` is shown *reproducible*
|
||||||
Binary Format companion.
|
today. A direct canonical byte codec for the richer core `Score` does not exist
|
||||||
|
yet (it is item 5's "whole-score codec", to be reconciled with the Binary
|
||||||
|
Format companion), so the whole-`Score` byte round-trip
|
||||||
|
(`criterion_4_full_score_byte_roundtrip`) is an explicit `#[ignore]`'d gate
|
||||||
|
rather than a falsely-green assertion.
|
||||||
- **Layout harness re-pointed.** `epiphany-layout-ir` has landed, so `layout_stub`
|
- **Layout harness re-pointed.** `epiphany-layout-ir` has landed, so `layout_stub`
|
||||||
now drives the real IR types behind the same `round_trip` signature (done). IR
|
now drives the real IR types behind the same `round_trip` signature (done). IR
|
||||||
coordinates are f32 staff spaces, quantized only when serializing canonical
|
coordinates are f32 staff spaces, quantized only when serializing canonical
|
||||||
|
|
|
||||||
|
|
@ -12,7 +12,8 @@
|
||||||
//! first violation.
|
//! first violation.
|
||||||
|
|
||||||
use epiphany_testkit::{
|
use epiphany_testkit::{
|
||||||
bundle_harness, convergence, equivocation, fixtures, generators, layout_stub, roundtrip, Rng,
|
bundle_harness, convergence, equivocation, fixtures, generators, layout_stub, negative,
|
||||||
|
roundtrip, Rng,
|
||||||
};
|
};
|
||||||
|
|
||||||
fn main() {
|
fn main() {
|
||||||
|
|
@ -37,8 +38,9 @@ fn main() {
|
||||||
eprintln!("[1/8] canonical round-trip corpus: {iters} iters");
|
eprintln!("[1/8] canonical round-trip corpus: {iters} iters");
|
||||||
roundtrip::run_roundtrip_corpus(iters, 0x00C0_FFEE_1234_5678);
|
roundtrip::run_roundtrip_corpus(iters, 0x00C0_FFEE_1234_5678);
|
||||||
|
|
||||||
// 1b. Bundle manifest + score serialization stability.
|
// 1b. Bundle manifest + reducer-bookkeeping serialization stability.
|
||||||
eprintln!("[1b ] manifest + score serialization stability");
|
// (Full-Score *byte* round-trip is pending item 5's whole-score codec.)
|
||||||
|
eprintln!("[1b ] manifest + reducer-bookkeeping serialization stability");
|
||||||
for seed in 0..n(64) {
|
for seed in 0..n(64) {
|
||||||
roundtrip::assert_manifest_roundtrip(&roundtrip::committed_manifest(seed));
|
roundtrip::assert_manifest_roundtrip(&roundtrip::committed_manifest(seed));
|
||||||
let mut rng = Rng::new(seed.wrapping_mul(0x0100_0193).wrapping_add(17));
|
let mut rng = Rng::new(seed.wrapping_mul(0x0100_0193).wrapping_add(17));
|
||||||
|
|
@ -67,8 +69,12 @@ fn main() {
|
||||||
bundle_harness::run_manifest_selection(seed);
|
bundle_harness::run_manifest_selection(seed);
|
||||||
}
|
}
|
||||||
|
|
||||||
// 5. Convergence (criterion 1): random sessions + the two-staff scenario.
|
// 5. Convergence (criterion 1): real-Score convergence through reduce_onto,
|
||||||
eprintln!("[5/8] convergence across delivery orders");
|
// plus the reducer-bookkeeping projection convergence.
|
||||||
|
eprintln!("[5/8] convergence across delivery orders (real Score + bookkeeping)");
|
||||||
|
for seed in 0..n(64) {
|
||||||
|
convergence::run_graph_convergence(6, seed.wrapping_mul(0x9E37_79B9).wrapping_add(11));
|
||||||
|
}
|
||||||
for seed in 0..n(500) {
|
for seed in 0..n(500) {
|
||||||
convergence::run_convergence(24, 8, seed.wrapping_mul(0x9E37_79B9));
|
convergence::run_convergence(24, 8, seed.wrapping_mul(0x9E37_79B9));
|
||||||
}
|
}
|
||||||
|
|
@ -76,6 +82,10 @@ fn main() {
|
||||||
convergence::run_two_staff_convergence(8, seed.wrapping_mul(0x9E37_79B9).wrapping_add(7));
|
convergence::run_two_staff_convergence(8, seed.wrapping_mul(0x9E37_79B9).wrapping_add(7));
|
||||||
}
|
}
|
||||||
|
|
||||||
|
// 5b. Audit regression guards (every defect the Agent C audit surfaced).
|
||||||
|
eprintln!("[5b ] audit defect regression guards");
|
||||||
|
negative::run_all();
|
||||||
|
|
||||||
// 6. Reduction determinism (criterion 5): a large set reduced many ways, the
|
// 6. Reduction determinism (criterion 5): a large set reduced many ways, the
|
||||||
// testkit's authoritative causal-order gate, + Agent C's own gate.
|
// testkit's authoritative causal-order gate, + Agent C's own gate.
|
||||||
let big = (1_000 * scale).max(1_000) as usize;
|
let big = (1_000 * scale).max(1_000) as usize;
|
||||||
|
|
|
||||||
|
|
@ -3,18 +3,34 @@
|
||||||
//! v0 acceptance criterion 1 (Convergence) and criterion 5 (Reduction
|
//! v0 acceptance criterion 1 (Convergence) and criterion 5 (Reduction
|
||||||
//! determinism) — the determinism heart of Chapter 6.
|
//! determinism) — the determinism heart of Chapter 6.
|
||||||
//!
|
//!
|
||||||
//! It drives the **real** [`epiphany_ops`] crate (Agent C has shipped): an
|
//! It drives the **real** [`epiphany_ops`] crate (Agent C has shipped). There
|
||||||
//! [`OperationSet`] accepts the envelopes, [`OperationSet::reduce`] materializes
|
//! are two levels of convergence, and this harness asserts both:
|
||||||
//! them, and the materialized state's `canonical_bytes` is the artifact compared
|
//!
|
||||||
//! across delivery orders. Because the canonical reduction order
|
//! * **Real-Score convergence** ([`assert_graph_convergence`],
|
||||||
|
//! [`run_graph_convergence`]) is the headline criterion 1: an edit session is
|
||||||
|
//! reduced onto a real base [`epiphany_core::Score`] via
|
||||||
|
//! [`OperationSet::reduce_onto`], and the entire materialized graph (the
|
||||||
|
//! `Score` *and* its bookkeeping state) must be identical across delivery
|
||||||
|
//! orders, pass `check_invariants`, and genuinely mutate the score.
|
||||||
|
//! * **Reducer-bookkeeping convergence** ([`assert_convergence`],
|
||||||
|
//! [`run_convergence`], [`run_two_staff_convergence`]) compares the canonical
|
||||||
|
//! *bookkeeping projection* — [`OperationSet::reduce`] →
|
||||||
|
//! `MaterializedState::canonical_bytes` — across delivery orders. This is the
|
||||||
|
//! Chapter 6 §6.3 ledger (effects, conflicts, anomalies, tombstones,
|
||||||
|
//! spellings, pending), not the full musical graph; it is retained as the
|
||||||
|
//! byte-canonical determinism gate and the basis of criterion 5.
|
||||||
|
//!
|
||||||
|
//! Because the canonical reduction order
|
||||||
//! ([`epiphany_ops::canonical_reduction_order`]) is a function of the operation
|
//! ([`epiphany_ops::canonical_reduction_order`]) is a function of the operation
|
||||||
//! *set* and not of delivery order, every delivery permutation must materialize
|
//! *set* and not of delivery order, every delivery permutation must materialize
|
||||||
//! byte-identically. The negative control in the tests proves the harness is not
|
//! identically at both levels. The negative control in the tests proves the
|
||||||
//! vacuous: a reducer that consumed *arrival* order instead would diverge, and
|
//! harness is not vacuous: a reducer that consumed *arrival* order instead would
|
||||||
//! this harness would catch it.
|
//! diverge, and this harness would catch it.
|
||||||
|
|
||||||
use epiphany_core::OperationId;
|
use epiphany_core::{check_invariants, OperationId, Score, StaffInstanceId, VoiceId};
|
||||||
use epiphany_ops::{canonical_reduction_order, OperationEnvelope, OperationSet};
|
use epiphany_ops::{
|
||||||
|
canonical_reduction_order, GraphMaterialization, OperationEnvelope, OperationSet,
|
||||||
|
};
|
||||||
|
|
||||||
use crate::rng::Rng;
|
use crate::rng::Rng;
|
||||||
|
|
||||||
|
|
@ -165,6 +181,106 @@ pub fn run_authoritative_reduction_gate(sets: usize, orders: usize, seed: u64) {
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
// === Real-Score convergence (acceptance criterion 1, graph level). ==========
|
||||||
|
|
||||||
|
/// Reduces `envelopes` onto `base` in the given delivery order via the real
|
||||||
|
/// [`OperationSet::reduce_onto`], returning the full graph materialization (the
|
||||||
|
/// `epiphany_core::Score` together with its canonical bookkeeping state).
|
||||||
|
fn materialize_onto_in_order(
|
||||||
|
base: &Score,
|
||||||
|
envelopes: &[OperationEnvelope],
|
||||||
|
) -> GraphMaterialization {
|
||||||
|
let mut set = OperationSet::new();
|
||||||
|
set.accept_all(envelopes.iter().cloned());
|
||||||
|
set.reduce_onto(base)
|
||||||
|
}
|
||||||
|
|
||||||
|
/// The number of events the given voice carries in `score`, or `None` if the
|
||||||
|
/// voice is absent.
|
||||||
|
fn voice_event_count(score: &Score, voice: VoiceId) -> Option<usize> {
|
||||||
|
score
|
||||||
|
.voices()
|
||||||
|
.find_map(|(_, _, v)| (v.id == voice).then_some(v.events.len()))
|
||||||
|
}
|
||||||
|
|
||||||
|
/// **Real-Score convergence (acceptance criterion 1).** Reduces the same
|
||||||
|
/// operation set onto `base` under `orders` independent delivery permutations
|
||||||
|
/// and asserts the entire [`GraphMaterialization`] — the real
|
||||||
|
/// [`epiphany_core::Score`] *and* its bookkeeping state — is identical every
|
||||||
|
/// time. Also asserts the materialized score satisfies every Chapter 5 graph
|
||||||
|
/// invariant ([`check_invariants`]) and that the session is non-vacuous: the
|
||||||
|
/// score actually changed and each targeted voice grew.
|
||||||
|
pub fn assert_graph_convergence(
|
||||||
|
base: &Score,
|
||||||
|
envelopes: &[OperationEnvelope],
|
||||||
|
targets: &[(StaffInstanceId, VoiceId)],
|
||||||
|
orders: usize,
|
||||||
|
rng: &mut Rng,
|
||||||
|
) {
|
||||||
|
let reference = materialize_onto_in_order(base, envelopes);
|
||||||
|
|
||||||
|
// The materialized real Score is structurally valid.
|
||||||
|
let violations = check_invariants(&reference.score);
|
||||||
|
assert!(
|
||||||
|
violations.is_empty(),
|
||||||
|
"materialized score violates graph invariants: {violations:?}"
|
||||||
|
);
|
||||||
|
|
||||||
|
// Non-vacuity: the session genuinely mutated the score, and each targeted
|
||||||
|
// voice grew (the generator inserts only at fresh positions, so no insert is
|
||||||
|
// lost to promotion).
|
||||||
|
assert!(
|
||||||
|
reference.score != *base,
|
||||||
|
"the edit session did not change the base score (vacuous convergence test)"
|
||||||
|
);
|
||||||
|
for &(_, voice) in targets {
|
||||||
|
let before = voice_event_count(base, voice).expect("target voice exists in base");
|
||||||
|
let after =
|
||||||
|
voice_event_count(&reference.score, voice).expect("target voice survives reduction");
|
||||||
|
assert!(
|
||||||
|
after > before,
|
||||||
|
"target voice {voice:?} did not grow under reduction ({before} -> {after})"
|
||||||
|
);
|
||||||
|
}
|
||||||
|
|
||||||
|
for k in 0..orders {
|
||||||
|
let perm = rng.permutation(envelopes.len());
|
||||||
|
let shuffled: Vec<OperationEnvelope> = perm.iter().map(|&i| envelopes[i].clone()).collect();
|
||||||
|
let got = materialize_onto_in_order(base, &shuffled);
|
||||||
|
assert_eq!(
|
||||||
|
reference, got,
|
||||||
|
"delivery permutation #{k} changed the materialized Score \
|
||||||
|
(graph reduction is not order-independent)"
|
||||||
|
);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
/// Selects a `valid_score` base with at least two voices (scanning successive
|
||||||
|
/// seeds), so the graph convergence gate genuinely edits two staves.
|
||||||
|
fn two_voice_base(seed: u64) -> Score {
|
||||||
|
let mut s = seed;
|
||||||
|
for _ in 0..64 {
|
||||||
|
let score = epiphany_core::generators::valid_score(s);
|
||||||
|
if score.voices().count() >= 2 {
|
||||||
|
return score;
|
||||||
|
}
|
||||||
|
s = s.wrapping_mul(0x9E37_79B9).wrapping_add(1);
|
||||||
|
}
|
||||||
|
epiphany_core::generators::valid_score(seed)
|
||||||
|
}
|
||||||
|
|
||||||
|
/// **The self-contained real-Score convergence driver (criterion 1).** Builds a
|
||||||
|
/// two-voice base score, authors a real ~50-bar edit session against its actual
|
||||||
|
/// voices ([`crate::generators::graph_edit_session`]), and asserts graph-level
|
||||||
|
/// convergence across `orders` delivery permutations. This is the graph
|
||||||
|
/// counterpart of [`run_two_staff_convergence`] (its reducer-bookkeeping twin).
|
||||||
|
pub fn run_graph_convergence(orders: usize, seed: u64) {
|
||||||
|
let base = two_voice_base(seed);
|
||||||
|
let mut rng = Rng::new(seed ^ 0x67A0_6FAC_E0B0_B0B0);
|
||||||
|
let (targets, envelopes) = crate::generators::graph_edit_session(&base, &mut rng);
|
||||||
|
assert_graph_convergence(&base, &envelopes, &targets, orders, &mut rng);
|
||||||
|
}
|
||||||
|
|
||||||
#[cfg(test)]
|
#[cfg(test)]
|
||||||
mod tests {
|
mod tests {
|
||||||
use super::*;
|
use super::*;
|
||||||
|
|
@ -190,6 +306,13 @@ mod tests {
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
#[test]
|
||||||
|
fn graph_sessions_converge_on_the_real_score() {
|
||||||
|
for seed in 0..8u64 {
|
||||||
|
run_graph_convergence(4, seed.wrapping_mul(0x9E37_79B9).wrapping_add(7));
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
#[test]
|
#[test]
|
||||||
fn empty_and_singleton_sets_are_trivially_stable() {
|
fn empty_and_singleton_sets_are_trivially_stable() {
|
||||||
let mut rng = Rng::new(1);
|
let mut rng = Rng::new(1);
|
||||||
|
|
|
||||||
|
|
@ -933,6 +933,101 @@ pub fn assert_two_staff_populated(envelopes: &[OperationEnvelope]) {
|
||||||
assert!(live_events(n, 2 * n) > 0, "staff 1 has no live events");
|
assert!(live_events(n, 2 * n) > 0, "staff 1 has no live events");
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/// Whole-note position past which [`graph_edit_session`] inserts, chosen to
|
||||||
|
/// clear `valid_score`'s base content (quarter-note events in `[0, 1)`).
|
||||||
|
const GRAPH_SESSION_OFFSET: i64 = 4;
|
||||||
|
|
||||||
|
/// An `InsertEvent` payload targeting a **real** base voice (`staff_instance`
|
||||||
|
/// must be the voice's actual container), minting `event`/`pitch` under
|
||||||
|
/// [`OBJ_REPLICA`] as the `index`-th half-note past the base content. Unlike
|
||||||
|
/// [`insert_at`], this addresses ids that already exist in a base [`graph`]
|
||||||
|
/// score, so the payload survives [`OperationSet::reduce_onto`] (which rejects
|
||||||
|
/// inserts into unknown voices) rather than only the base-free reducer.
|
||||||
|
fn insert_into(
|
||||||
|
staff_instance: StaffInstanceId,
|
||||||
|
voice: VoiceId,
|
||||||
|
event: u64,
|
||||||
|
pitch: u64,
|
||||||
|
index: u64,
|
||||||
|
) -> OperationPayload {
|
||||||
|
OperationPayload::Primitive(OperationKind::InsertEvent(InsertEventOp {
|
||||||
|
voice,
|
||||||
|
staff_instance,
|
||||||
|
event: obj_event(event),
|
||||||
|
// position = GRAPH_SESSION_OFFSET + index/2 (two half-notes per 4/4 bar).
|
||||||
|
position: MusicalPosition(
|
||||||
|
RationalTime::new(
|
||||||
|
GRAPH_SESSION_OFFSET * EVENTS_PER_BAR as i64 + index as i64,
|
||||||
|
2,
|
||||||
|
)
|
||||||
|
.unwrap(),
|
||||||
|
),
|
||||||
|
duration: MusicalDuration(RationalTime::new(1, 2).unwrap()),
|
||||||
|
pitches: vec![obj_pitch(pitch)],
|
||||||
|
}))
|
||||||
|
}
|
||||||
|
|
||||||
|
/// The graph-level twin of [`two_staff_edit_session`]: a real ~50-bar edit
|
||||||
|
/// session targeting the **actual** voices of `base`, for the
|
||||||
|
/// [`OperationSet::reduce_onto`] convergence gate (acceptance criterion 1).
|
||||||
|
///
|
||||||
|
/// Two replicas alternately insert [`TWO_STAFF_EVENTS_PER_STAFF`] half-note
|
||||||
|
/// events past the base content into the base's first two voices (so both
|
||||||
|
/// staves are genuinely edited), then concurrently respell and delete over the
|
||||||
|
/// shared minted id space, so the canonical reduction — not delivery order —
|
||||||
|
/// decides the materialized `Score`. Returns the targeted voices alongside the
|
||||||
|
/// envelopes (the convergence harness checks each one actually grew).
|
||||||
|
///
|
||||||
|
/// Requires a base with at least one voice; callers pass a base scanned for two
|
||||||
|
/// (see `epiphany_core::generators::valid_score`).
|
||||||
|
pub fn graph_edit_session(
|
||||||
|
base: &epiphany_core::Score,
|
||||||
|
rng: &mut Rng,
|
||||||
|
) -> (Vec<(StaffInstanceId, VoiceId)>, Vec<OperationEnvelope>) {
|
||||||
|
let targets: Vec<(StaffInstanceId, VoiceId)> = base
|
||||||
|
.voices()
|
||||||
|
.map(|(_, instance, voice)| (instance, voice.id))
|
||||||
|
.take(2)
|
||||||
|
.collect();
|
||||||
|
assert!(
|
||||||
|
!targets.is_empty(),
|
||||||
|
"graph_edit_session requires a base score with at least one voice"
|
||||||
|
);
|
||||||
|
|
||||||
|
let n = TWO_STAFF_EVENTS_PER_STAFF;
|
||||||
|
let mut session = Session::new(2);
|
||||||
|
for i in 0..n {
|
||||||
|
for (ti, &(instance, voice)) in targets.iter().enumerate() {
|
||||||
|
// Each target voice's consecutive half-notes alternate authoring
|
||||||
|
// replicas; the two voices are edited by opposite replicas at any
|
||||||
|
// given index. Positions are distinct within a voice (no
|
||||||
|
// same-position collision → clean inserts), while cross-replica
|
||||||
|
// causal sampling makes delivery order differ from reduction order.
|
||||||
|
let r = (i as usize + ti) % 2;
|
||||||
|
let object = ti as u64 * n + i;
|
||||||
|
session.author(rng, r, insert_into(instance, voice, object, object, i));
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
let total = targets.len() as u64 * n;
|
||||||
|
for _ in 0..80 {
|
||||||
|
let r = rng.below(2) as usize;
|
||||||
|
let payload = if rng.boolean() {
|
||||||
|
OperationPayload::Primitive(OperationKind::DeleteEvent(DeleteEventOp {
|
||||||
|
event: obj_event(rng.below(total)),
|
||||||
|
tuplet_compensation: TupletCompensation::NotInTuplet,
|
||||||
|
}))
|
||||||
|
} else {
|
||||||
|
OperationPayload::Primitive(OperationKind::RespellPitch(RespellPitchOp {
|
||||||
|
pitch: obj_pitch(rng.below(total)),
|
||||||
|
spelling: ContentHash([(rng.below(4) as u8) + 1; 32]),
|
||||||
|
}))
|
||||||
|
};
|
||||||
|
session.author(rng, r, payload);
|
||||||
|
}
|
||||||
|
(targets, session.out)
|
||||||
|
}
|
||||||
|
|
||||||
/// A `(base, mutated)` pair of operation sets whose operations have **identical
|
/// A `(base, mutated)` pair of operation sets whose operations have **identical
|
||||||
/// identities, stamps, and causal contexts** but differ in payload *content*
|
/// identities, stamps, and causal contexts** but differ in payload *content*
|
||||||
/// (one respelling's spelling). Both sets insert a pitch and respell it, so the
|
/// (one respelling's spelling). Both sets insert a pitch and respell it, so the
|
||||||
|
|
|
||||||
|
|
@ -29,11 +29,20 @@
|
||||||
//! manifest-selection harness, driving the real [`epiphany_bundle`] through
|
//! manifest-selection harness, driving the real [`epiphany_bundle`] through
|
||||||
//! its public API and re-exporting its in-crate gates.
|
//! its public API and re-exporting its in-crate gates.
|
||||||
//! * [`convergence`] — the CRDT convergence and reduction-determinism harnesses
|
//! * [`convergence`] — the CRDT convergence and reduction-determinism harnesses
|
||||||
//! (criteria 1 and 5), driving the real [`epiphany_ops::OperationSet`] /
|
//! (criteria 1 and 5). Criterion 1 proper is **real-Score** convergence
|
||||||
//! [`epiphany_ops::canonical_reduction_order`] / reduce, and re-exporting Agent
|
//! ([`convergence::run_graph_convergence`]): an edit session reduced onto a
|
||||||
//! C's own determinism gate.
|
//! real [`epiphany_core::Score`] via [`epiphany_ops::OperationSet::reduce_onto`]
|
||||||
|
//! must materialize an identical graph under every delivery order. The
|
||||||
|
//! byte-canonical **bookkeeping projection** convergence
|
||||||
|
//! ([`convergence::assert_convergence`], over
|
||||||
|
//! [`epiphany_ops::OperationSet::reduce`] →
|
||||||
|
//! [`epiphany_ops::MaterializedState`]) is retained as a determinism gate and
|
||||||
|
//! the basis of criterion 5. Re-exports Agent C's own determinism gate.
|
||||||
//! * [`equivocation`] — the equivocation harness (criterion 3), driving the real
|
//! * [`equivocation`] — the equivocation harness (criterion 3), driving the real
|
||||||
//! [`epiphany_ops::OperationSlot`] model and re-exporting Agent C's gate.
|
//! [`epiphany_ops::OperationSlot`] model and re-exporting Agent C's gate.
|
||||||
|
//! * [`negative`] — regression guards for every defect the Agent C framework
|
||||||
|
//! audit surfaced (the M1 fixes), so a regression in `epiphany-ops` trips this
|
||||||
|
//! suite directly rather than slipping past a generic convergence gate.
|
||||||
//!
|
//!
|
||||||
//! * [`layout_stub`] — the layout round-trip harness (criterion 6). Agent E
|
//! * [`layout_stub`] — the layout round-trip harness (criterion 6). Agent E
|
||||||
//! (`epiphany-layout-ir`, Chapters 7 & 9) has landed, so this module — once a
|
//! (`epiphany-layout-ir`, Chapters 7 & 9) has landed, so this module — once a
|
||||||
|
|
@ -65,12 +74,19 @@
|
||||||
//!
|
//!
|
||||||
//! | # | Criterion | Entry point |
|
//! | # | Criterion | Entry point |
|
||||||
//! |---|-----------|-------------|
|
//! |---|-----------|-------------|
|
||||||
//! | 1 | Convergence | [`convergence::assert_convergence`] |
|
//! | 1 | Convergence (real Score) | [`convergence::run_graph_convergence`] |
|
||||||
//! | 2 | Crash safety | [`bundle_harness::run_crash_recovery`] |
|
//! | 2 | Crash safety | [`bundle_harness::run_crash_recovery`] |
|
||||||
//! | 3 | Equivocation | [`equivocation::assert_equivocation_order_independent`] |
|
//! | 3 | Equivocation | [`equivocation::assert_equivocation_order_independent`] |
|
||||||
//! | 4 | Canonical serialization stability | [`roundtrip::run_roundtrip_corpus`] |
|
//! | 4 | Canonical serialization stability (typed + container) | [`roundtrip::run_roundtrip_corpus`] |
|
||||||
//! | 5 | Reduction determinism | [`convergence::assert_reduction_determinism`] |
|
//! | 5 | Reduction determinism | [`convergence::assert_reduction_determinism`] |
|
||||||
//! | 6 | Layout round-trip | [`layout_stub::round_trip`] |
|
//! | 6 | Layout round-trip | [`layout_stub::round_trip`] |
|
||||||
|
//!
|
||||||
|
//! Criterion 1's reducer-bookkeeping counterpart ([`convergence::assert_convergence`])
|
||||||
|
//! and criterion 4's bookkeeping-projection serialization
|
||||||
|
//! ([`roundtrip::assert_reduction_serialization_stable`]) are retained under
|
||||||
|
//! honest names. The full-`Score` **byte** round-trip is pending item 5 (Agent
|
||||||
|
//! B): no whole-score codec exists yet, so that one gate is marked `#[ignore]`
|
||||||
|
//! in `tests/acceptance.rs` rather than asserted falsely.
|
||||||
|
|
||||||
pub mod rng;
|
pub mod rng;
|
||||||
|
|
||||||
|
|
@ -80,6 +96,7 @@ pub mod roundtrip;
|
||||||
|
|
||||||
pub mod convergence;
|
pub mod convergence;
|
||||||
pub mod equivocation;
|
pub mod equivocation;
|
||||||
|
pub mod negative;
|
||||||
|
|
||||||
pub mod bundle_harness;
|
pub mod bundle_harness;
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -0,0 +1,426 @@
|
||||||
|
//! Negative / regression guards for the defects found in the Agent C audit
|
||||||
|
//! (the M1 framework fixes). Item 4 of the v0 follow-up plan charters Agent F's
|
||||||
|
//! suite to independently guard *every* defect the audit surfaced, so a
|
||||||
|
//! regression in `epiphany-ops` trips this tripwire rather than slipping past a
|
||||||
|
//! generic convergence gate.
|
||||||
|
//!
|
||||||
|
//! Each guard drives the **real** [`epiphany_ops`] public API and asserts the
|
||||||
|
//! post-fix behavior. Where the pre-fix bug had a concrete, observable
|
||||||
|
//! signature (an inverted order, an under-cut quarantine, an un-promoted
|
||||||
|
//! collision), the guard also pins the *negative* outcome — the thing the buggy
|
||||||
|
//! reducer would have produced — so the test is provably non-vacuous.
|
||||||
|
//!
|
||||||
|
//! The six audited defects:
|
||||||
|
//!
|
||||||
|
//! 1. A causal predecessor authored with a larger HLC than its successor sorted
|
||||||
|
//! *after* it ([`assert_causal_order_dominates_inverted_hlc`]).
|
||||||
|
//! 2. A missing predecessor expressed through the DVV *vector* (not a dot) was
|
||||||
|
//! not detected ([`assert_missing_vector_predecessor_pends`]).
|
||||||
|
//! 3. An HLC sequence `100, 200, 50` quarantined from counter 1, not the
|
||||||
|
//! counter 0 that also forms a violating pair
|
||||||
|
//! ([`assert_hlc_100_200_50_quarantines_from_zero`]).
|
||||||
|
//! 4. A failed transaction left its members' generated conflicts behind
|
||||||
|
//! ([`assert_failed_transaction_rolls_back_member_conflicts`]).
|
||||||
|
//! 5. A *causally ordered* same-position insert was promoted as if concurrent
|
||||||
|
//! ([`assert_causally_ordered_same_position_not_promoted`]).
|
||||||
|
//! 6. Partial-duration interval overlaps were mishandled
|
||||||
|
//! ([`assert_partial_overlap_promotes_but_adjacent_does_not`]).
|
||||||
|
|
||||||
|
use epiphany_core::{
|
||||||
|
EventId, MusicalDuration, MusicalPosition, OperationId, PitchId, RationalTime, ReplicaId,
|
||||||
|
StaffInstanceId, TransactionId, VoiceId, WallClockTime,
|
||||||
|
};
|
||||||
|
use epiphany_determinism::ContentHash;
|
||||||
|
use epiphany_ops::{
|
||||||
|
canonical_reduction_order, AuthorId, CausalContext, ConflictKind, DeleteEventOp,
|
||||||
|
HybridLogicalClock, InsertEventOp, IntegrityAnomalyKind, NoOpReason, OperationEffect,
|
||||||
|
OperationEnvelope, OperationKind, OperationPayload, OperationSet, OperationStamp,
|
||||||
|
PendingReason, PreconditionFailureReason, RepairKind, RespellPitchOp, TransactionDescriptor,
|
||||||
|
TupletCompensation,
|
||||||
|
};
|
||||||
|
|
||||||
|
/// The replica that owns the synthetic object id space these scenarios edit.
|
||||||
|
const OBJ: ReplicaId = ReplicaId(9);
|
||||||
|
|
||||||
|
fn op(replica: u64, counter: u64) -> OperationId {
|
||||||
|
OperationId::new(ReplicaId(replica), counter)
|
||||||
|
}
|
||||||
|
|
||||||
|
fn envelope(
|
||||||
|
replica: u64,
|
||||||
|
counter: u64,
|
||||||
|
physical: i64,
|
||||||
|
ctx: CausalContext,
|
||||||
|
transaction: Option<TransactionId>,
|
||||||
|
payload: OperationPayload,
|
||||||
|
) -> OperationEnvelope {
|
||||||
|
let id = op(replica, counter);
|
||||||
|
OperationEnvelope {
|
||||||
|
id,
|
||||||
|
author: AuthorId(replica as u128),
|
||||||
|
stamp: OperationStamp::new(HybridLogicalClock::new(WallClockTime(physical), 0), id),
|
||||||
|
causal_context: ctx,
|
||||||
|
transaction,
|
||||||
|
payload,
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
fn insert_span(
|
||||||
|
voice: u64,
|
||||||
|
event: u64,
|
||||||
|
position: RationalTime,
|
||||||
|
duration: RationalTime,
|
||||||
|
) -> OperationPayload {
|
||||||
|
OperationPayload::Primitive(OperationKind::InsertEvent(InsertEventOp {
|
||||||
|
voice: VoiceId::new(OBJ, voice),
|
||||||
|
staff_instance: StaffInstanceId::new(OBJ, 0),
|
||||||
|
event: EventId::new(OBJ, event),
|
||||||
|
position: MusicalPosition(position),
|
||||||
|
duration: MusicalDuration(duration),
|
||||||
|
pitches: vec![PitchId::new(OBJ, event)],
|
||||||
|
}))
|
||||||
|
}
|
||||||
|
|
||||||
|
fn insert(voice: u64, event: u64, pos: i64) -> OperationPayload {
|
||||||
|
insert_span(
|
||||||
|
voice,
|
||||||
|
event,
|
||||||
|
RationalTime::from_int(pos as i32),
|
||||||
|
RationalTime::one(),
|
||||||
|
)
|
||||||
|
}
|
||||||
|
|
||||||
|
fn respell(pitch: u64, spelling: u8) -> OperationPayload {
|
||||||
|
OperationPayload::Primitive(OperationKind::RespellPitch(RespellPitchOp {
|
||||||
|
pitch: PitchId::new(OBJ, pitch),
|
||||||
|
spelling: ContentHash([spelling; 32]),
|
||||||
|
}))
|
||||||
|
}
|
||||||
|
|
||||||
|
fn delete_event(event: u64) -> OperationPayload {
|
||||||
|
OperationPayload::Primitive(OperationKind::DeleteEvent(DeleteEventOp {
|
||||||
|
event: EventId::new(OBJ, event),
|
||||||
|
tuplet_compensation: TupletCompensation::NotInTuplet,
|
||||||
|
}))
|
||||||
|
}
|
||||||
|
|
||||||
|
fn declare_tx(replica: u64, counter: u64, physical: i64, tx: TransactionId) -> OperationEnvelope {
|
||||||
|
envelope(
|
||||||
|
replica,
|
||||||
|
counter,
|
||||||
|
physical,
|
||||||
|
CausalContext::new(),
|
||||||
|
None,
|
||||||
|
OperationPayload::Primitive(OperationKind::DeclareTransaction(TransactionDescriptor {
|
||||||
|
id: tx,
|
||||||
|
label: "edit".to_string(),
|
||||||
|
category: None,
|
||||||
|
})),
|
||||||
|
)
|
||||||
|
}
|
||||||
|
|
||||||
|
fn promotes(effect: Option<&OperationEffect>) -> bool {
|
||||||
|
matches!(
|
||||||
|
effect,
|
||||||
|
Some(OperationEffect::AppliedWithRepair { repairs })
|
||||||
|
if repairs.iter().any(|r| matches!(r.kind, RepairKind::VoicePromoted { .. }))
|
||||||
|
)
|
||||||
|
}
|
||||||
|
|
||||||
|
// --- Defect 1: causal order vs. an inverted HLC. ----------------------------
|
||||||
|
|
||||||
|
/// A predecessor carrying a *larger* physical stamp than its dot-linked
|
||||||
|
/// successor must still reduce first. A reducer that trusted the HLC tuple alone
|
||||||
|
/// (the pre-fix bug) would invert the pair; the canonical order must not.
|
||||||
|
pub fn assert_causal_order_dominates_inverted_hlc() {
|
||||||
|
let predecessor = envelope(1, 0, 100, CausalContext::new(), None, insert(0, 100, 0));
|
||||||
|
let successor = envelope(
|
||||||
|
2,
|
||||||
|
0,
|
||||||
|
1,
|
||||||
|
CausalContext::new().with_dot(predecessor.id),
|
||||||
|
None,
|
||||||
|
insert(0, 101, 1),
|
||||||
|
);
|
||||||
|
|
||||||
|
// Negative control: sorting by the HLC tuple alone *does* invert these.
|
||||||
|
let mut by_hlc = [&successor, &predecessor];
|
||||||
|
by_hlc.sort_by_key(|e| e.stamp.reduction_tuple());
|
||||||
|
assert_eq!(
|
||||||
|
by_hlc[0].id, successor.id,
|
||||||
|
"negative control mis-constructed: HLC-only order should place the successor first"
|
||||||
|
);
|
||||||
|
|
||||||
|
let ordered = canonical_reduction_order(&[&successor, &predecessor]);
|
||||||
|
assert_eq!(
|
||||||
|
ordered.iter().map(|e| e.id).collect::<Vec<_>>(),
|
||||||
|
vec![predecessor.id, successor.id],
|
||||||
|
"canonical reduction order must place the causal predecessor first despite its larger HLC"
|
||||||
|
);
|
||||||
|
}
|
||||||
|
|
||||||
|
// --- Defect 2: missing predecessor via the DVV vector. ----------------------
|
||||||
|
|
||||||
|
/// A dependent whose causal context covers a predecessor through the contiguous
|
||||||
|
/// *vector* (`with_seen`), not a dot, must be held pending when that predecessor
|
||||||
|
/// is absent. The pre-fix detector keyed only on dots and let this through.
|
||||||
|
pub fn assert_missing_vector_predecessor_pends() {
|
||||||
|
let present = envelope(1, 0, 1, CausalContext::new(), None, insert(0, 99, -1));
|
||||||
|
let dependent = envelope(
|
||||||
|
2,
|
||||||
|
0,
|
||||||
|
10,
|
||||||
|
CausalContext::new().with_seen(ReplicaId(1), 2),
|
||||||
|
None,
|
||||||
|
insert(0, 100, 0),
|
||||||
|
);
|
||||||
|
let mut set = OperationSet::new();
|
||||||
|
set.accept_all(vec![present.clone(), dependent.clone()]);
|
||||||
|
let state = set.reduce();
|
||||||
|
|
||||||
|
assert_eq!(state.effects.len(), 1, "only the present operation applies");
|
||||||
|
assert_eq!(state.effects[0].0, present.id);
|
||||||
|
assert_eq!(
|
||||||
|
state.pending,
|
||||||
|
vec![(
|
||||||
|
dependent.id,
|
||||||
|
PendingReason::MissingCausalPredecessor { missing: op(1, 1) }
|
||||||
|
)],
|
||||||
|
"the operation must pend on the vector-covered but absent predecessor (1,1)"
|
||||||
|
);
|
||||||
|
}
|
||||||
|
|
||||||
|
// --- Defect 3: HLC 100, 200, 50 quarantines from counter 0. -----------------
|
||||||
|
|
||||||
|
/// The cut must begin at the *earliest* counter participating in any violating
|
||||||
|
/// pair. With stamps `100, 200, 50` the violating pair is (counter 0 = 100,
|
||||||
|
/// counter 2 = 50), so even the monotone counter 0 is quarantined. The pre-fix
|
||||||
|
/// code cut from counter 1 (the first strict decrease) and left counter 0 live.
|
||||||
|
pub fn assert_hlc_100_200_50_quarantines_from_zero() {
|
||||||
|
let a = envelope(1, 0, 100, CausalContext::new(), None, insert(0, 100, 0));
|
||||||
|
let b = envelope(1, 1, 200, CausalContext::new(), None, insert(0, 101, 1));
|
||||||
|
let c = envelope(1, 2, 50, CausalContext::new(), None, insert(0, 102, 2));
|
||||||
|
let mut set = OperationSet::new();
|
||||||
|
set.accept_all(vec![a, b, c]);
|
||||||
|
let state = set.reduce();
|
||||||
|
|
||||||
|
assert!(
|
||||||
|
state.effects.is_empty(),
|
||||||
|
"the entire offending replica stream must be excluded, including counter 0"
|
||||||
|
);
|
||||||
|
assert!(
|
||||||
|
state.anomalies.iter().any(|an| matches!(
|
||||||
|
an.kind,
|
||||||
|
IntegrityAnomalyKind::ReplicaStreamQuarantined {
|
||||||
|
replica,
|
||||||
|
first_bad_counter,
|
||||||
|
..
|
||||||
|
} if replica == ReplicaId(1) && first_bad_counter == 0
|
||||||
|
)),
|
||||||
|
"the quarantine anomaly must report first_bad_counter == 0"
|
||||||
|
);
|
||||||
|
}
|
||||||
|
|
||||||
|
// --- Defect 4: failed transaction rolls back member-generated conflicts. -----
|
||||||
|
|
||||||
|
/// A transaction whose members would generate conflicts but whose block fails
|
||||||
|
/// must leave *no* member-generated conflict behind — only the wholesale
|
||||||
|
/// transaction conflict. The pre-fix snapshot did not restore the conflict
|
||||||
|
/// registry, so the member's structural-collision conflict survived.
|
||||||
|
pub fn assert_failed_transaction_rolls_back_member_conflicts() {
|
||||||
|
let seed = envelope(2, 0, 1, CausalContext::new(), None, insert(0, 100, 0));
|
||||||
|
let initial_spelling = envelope(
|
||||||
|
2,
|
||||||
|
1,
|
||||||
|
2,
|
||||||
|
CausalContext::new().with_seen(ReplicaId(2), 0),
|
||||||
|
None,
|
||||||
|
respell(100, 1),
|
||||||
|
);
|
||||||
|
let tx = TransactionId::from_raw(89);
|
||||||
|
let descriptor = declare_tx(1, 0, 10, tx);
|
||||||
|
let tx_ctx = CausalContext::new().with_seen(ReplicaId(1), 0);
|
||||||
|
let conflicting = envelope(1, 1, 11, tx_ctx.clone(), Some(tx), respell(100, 2));
|
||||||
|
let failing = envelope(1, 2, 12, tx_ctx, Some(tx), delete_event(999));
|
||||||
|
|
||||||
|
let mut set = OperationSet::new();
|
||||||
|
set.accept_all(vec![
|
||||||
|
seed,
|
||||||
|
initial_spelling,
|
||||||
|
descriptor,
|
||||||
|
conflicting,
|
||||||
|
failing,
|
||||||
|
]);
|
||||||
|
let state = set.reduce();
|
||||||
|
|
||||||
|
assert_eq!(
|
||||||
|
state.spellings.get(&PitchId::new(OBJ, 100)),
|
||||||
|
Some(&ContentHash([1; 32])),
|
||||||
|
"the pre-transaction spelling must survive the rollback"
|
||||||
|
);
|
||||||
|
assert_eq!(
|
||||||
|
state.conflicts.records().len(),
|
||||||
|
1,
|
||||||
|
"only the wholesale transaction conflict should remain"
|
||||||
|
);
|
||||||
|
assert!(matches!(
|
||||||
|
state.conflicts.records()[0].kind,
|
||||||
|
ConflictKind::TransactionConflict { .. }
|
||||||
|
));
|
||||||
|
}
|
||||||
|
|
||||||
|
// --- Defect 5: causally ordered same-position insert is not promoted. --------
|
||||||
|
|
||||||
|
/// A same-position insert that *causally follows* the first (so it is not
|
||||||
|
/// concurrent) must be a precondition failure, never a voice promotion.
|
||||||
|
/// Promotion is for concurrent collisions only.
|
||||||
|
pub fn assert_causally_ordered_same_position_not_promoted() {
|
||||||
|
let first = envelope(1, 0, 10, CausalContext::new(), None, insert(0, 100, 0));
|
||||||
|
let second = envelope(
|
||||||
|
1,
|
||||||
|
1,
|
||||||
|
11,
|
||||||
|
CausalContext::new().with_seen(ReplicaId(1), 0),
|
||||||
|
None,
|
||||||
|
insert(0, 101, 0),
|
||||||
|
);
|
||||||
|
let mut set = OperationSet::new();
|
||||||
|
set.accept_all(vec![first, second.clone()]);
|
||||||
|
let state = set.reduce();
|
||||||
|
|
||||||
|
let effect = state
|
||||||
|
.effects
|
||||||
|
.iter()
|
||||||
|
.find(|(id, _)| *id == second.id)
|
||||||
|
.map(|(_, e)| e);
|
||||||
|
assert_eq!(
|
||||||
|
effect,
|
||||||
|
Some(&OperationEffect::NoOp {
|
||||||
|
reason: NoOpReason::PreconditionFailedUnderReduction {
|
||||||
|
reason: PreconditionFailureReason::EventDurationInvalid,
|
||||||
|
},
|
||||||
|
}),
|
||||||
|
"a causally-ordered same-position insert must fail its precondition"
|
||||||
|
);
|
||||||
|
assert!(
|
||||||
|
!promotes(effect),
|
||||||
|
"a causally-ordered insert must not be promoted as if concurrent"
|
||||||
|
);
|
||||||
|
}
|
||||||
|
|
||||||
|
// --- Defect 6: partial-duration overlaps. -----------------------------------
|
||||||
|
|
||||||
|
/// Concurrent inserts whose intervals *partially* overlap collide (and promote
|
||||||
|
/// the greater id), while concurrent inserts at *adjacent* half-open intervals
|
||||||
|
/// do not. The pre-fix overlap test only compared start positions.
|
||||||
|
pub fn assert_partial_overlap_promotes_but_adjacent_does_not() {
|
||||||
|
// Partial overlap: [0, 1) and [1/2, 3/2).
|
||||||
|
let first = envelope(
|
||||||
|
1,
|
||||||
|
0,
|
||||||
|
10,
|
||||||
|
CausalContext::new(),
|
||||||
|
None,
|
||||||
|
insert_span(0, 100, RationalTime::zero(), RationalTime::one()),
|
||||||
|
);
|
||||||
|
let second = envelope(
|
||||||
|
2,
|
||||||
|
0,
|
||||||
|
10,
|
||||||
|
CausalContext::new(),
|
||||||
|
None,
|
||||||
|
insert_span(
|
||||||
|
0,
|
||||||
|
200,
|
||||||
|
RationalTime::new(1, 2).unwrap(),
|
||||||
|
RationalTime::one(),
|
||||||
|
),
|
||||||
|
);
|
||||||
|
let mut set = OperationSet::new();
|
||||||
|
set.accept_all(vec![first, second.clone()]);
|
||||||
|
let state = set.reduce();
|
||||||
|
assert!(
|
||||||
|
promotes(
|
||||||
|
state
|
||||||
|
.effects
|
||||||
|
.iter()
|
||||||
|
.find(|(id, _)| *id == second.id)
|
||||||
|
.map(|(_, e)| e)
|
||||||
|
),
|
||||||
|
"a concurrent partial-interval overlap must promote the greater id"
|
||||||
|
);
|
||||||
|
|
||||||
|
// Adjacent half-open intervals: [0, 1) and [1, 2) — no collision.
|
||||||
|
let a = envelope(
|
||||||
|
1,
|
||||||
|
0,
|
||||||
|
10,
|
||||||
|
CausalContext::new(),
|
||||||
|
None,
|
||||||
|
insert_span(0, 100, RationalTime::zero(), RationalTime::one()),
|
||||||
|
);
|
||||||
|
let b = envelope(
|
||||||
|
2,
|
||||||
|
0,
|
||||||
|
10,
|
||||||
|
CausalContext::new(),
|
||||||
|
None,
|
||||||
|
insert_span(0, 200, RationalTime::one(), RationalTime::one()),
|
||||||
|
);
|
||||||
|
let mut adjacent = OperationSet::new();
|
||||||
|
adjacent.accept_all(vec![a, b]);
|
||||||
|
let adjacent_state = adjacent.reduce();
|
||||||
|
assert!(
|
||||||
|
adjacent_state
|
||||||
|
.effects
|
||||||
|
.iter()
|
||||||
|
.all(|(_, e)| *e == OperationEffect::Applied),
|
||||||
|
"adjacent half-open intervals must not collide"
|
||||||
|
);
|
||||||
|
}
|
||||||
|
|
||||||
|
/// Runs every audited-defect regression guard. The acceptance suite calls this
|
||||||
|
/// as a single entry point (criterion-adjacent: the audit tripwire).
|
||||||
|
pub fn run_all() {
|
||||||
|
assert_causal_order_dominates_inverted_hlc();
|
||||||
|
assert_missing_vector_predecessor_pends();
|
||||||
|
assert_hlc_100_200_50_quarantines_from_zero();
|
||||||
|
assert_failed_transaction_rolls_back_member_conflicts();
|
||||||
|
assert_causally_ordered_same_position_not_promoted();
|
||||||
|
assert_partial_overlap_promotes_but_adjacent_does_not();
|
||||||
|
}
|
||||||
|
|
||||||
|
#[cfg(test)]
|
||||||
|
mod tests {
|
||||||
|
use super::*;
|
||||||
|
|
||||||
|
#[test]
|
||||||
|
fn causal_order_dominates_inverted_hlc() {
|
||||||
|
assert_causal_order_dominates_inverted_hlc();
|
||||||
|
}
|
||||||
|
|
||||||
|
#[test]
|
||||||
|
fn missing_vector_predecessor_pends() {
|
||||||
|
assert_missing_vector_predecessor_pends();
|
||||||
|
}
|
||||||
|
|
||||||
|
#[test]
|
||||||
|
fn hlc_100_200_50_quarantines_from_zero() {
|
||||||
|
assert_hlc_100_200_50_quarantines_from_zero();
|
||||||
|
}
|
||||||
|
|
||||||
|
#[test]
|
||||||
|
fn failed_transaction_rolls_back_member_conflicts() {
|
||||||
|
assert_failed_transaction_rolls_back_member_conflicts();
|
||||||
|
}
|
||||||
|
|
||||||
|
#[test]
|
||||||
|
fn causally_ordered_same_position_not_promoted() {
|
||||||
|
assert_causally_ordered_same_position_not_promoted();
|
||||||
|
}
|
||||||
|
|
||||||
|
#[test]
|
||||||
|
fn partial_overlap_promotes_but_adjacent_does_not() {
|
||||||
|
assert_partial_overlap_promotes_but_adjacent_does_not();
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
@ -9,15 +9,34 @@
|
||||||
//! module (Agent E has landed). See the crate docs for the harness policy.
|
//! module (Agent E has landed). See the crate docs for the harness policy.
|
||||||
|
|
||||||
use epiphany_testkit::{
|
use epiphany_testkit::{
|
||||||
bundle_harness, convergence, equivocation, fixtures, generators, layout_stub, roundtrip, Rng,
|
bundle_harness, convergence, equivocation, fixtures, generators, layout_stub, negative,
|
||||||
|
roundtrip, Rng,
|
||||||
};
|
};
|
||||||
|
|
||||||
/// Criterion 1 — **Convergence.** Overlapping edits to a (modeled) 50-bar,
|
/// Criterion 1 — **Convergence (real Score).** Overlapping edits to a real
|
||||||
/// two-staff score by two replicas converge to byte-identical materialized state
|
/// ~50-bar, two-voice base [`epiphany_core::Score`] by two replicas converge to
|
||||||
/// regardless of envelope delivery order (Chapter 6's canonical reduction).
|
/// an *identical materialized Score* — the real graph (arena, voices,
|
||||||
|
/// tombstones, cross-cutting) together with its bookkeeping state — regardless
|
||||||
|
/// of envelope delivery order, with every Chapter 5 invariant intact. Driven
|
||||||
|
/// through Agent C's `OperationSet::reduce_onto`. This is the headline criterion;
|
||||||
|
/// [`reducer_bookkeeping_convergence`] is its ledger-projection counterpart.
|
||||||
#[test]
|
#[test]
|
||||||
fn criterion_1_convergence() {
|
fn criterion_1_convergence() {
|
||||||
// The criterion's named shape: a two-staff, overlapping-edit session.
|
for seed in 0..24u64 {
|
||||||
|
convergence::run_graph_convergence(6, seed.wrapping_mul(0x9E37_79B9).wrapping_add(11));
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
/// **Reducer-bookkeeping convergence** (the former, weaker half of criterion 1,
|
||||||
|
/// retained and honestly renamed). The canonical Chapter 6 §6.3 *bookkeeping
|
||||||
|
/// projection* — `OperationSet::reduce` → `MaterializedState::canonical_bytes` —
|
||||||
|
/// is byte-identical across delivery orders. That projection is the ledger
|
||||||
|
/// (effects, conflicts, anomalies, tombstones, spellings, pending), **not** the
|
||||||
|
/// full musical graph; real-Score convergence is `criterion_1_convergence`.
|
||||||
|
/// Kept as a fast byte-level determinism gate (and the basis of criterion 5).
|
||||||
|
#[test]
|
||||||
|
fn reducer_bookkeeping_convergence() {
|
||||||
|
// The named shape: a two-staff, overlapping-edit session (bookkeeping bytes).
|
||||||
for seed in 0..16u64 {
|
for seed in 0..16u64 {
|
||||||
convergence::run_two_staff_convergence(8, seed.wrapping_mul(0x9E37_79B9).wrapping_add(11));
|
convergence::run_two_staff_convergence(8, seed.wrapping_mul(0x9E37_79B9).wrapping_add(11));
|
||||||
}
|
}
|
||||||
|
|
@ -27,6 +46,14 @@ fn criterion_1_convergence() {
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/// **Audit regression guards.** Every defect the Agent C framework audit
|
||||||
|
/// surfaced (the M1 fixes) is independently re-asserted here so a regression in
|
||||||
|
/// `epiphany-ops` trips Agent F's suite directly. See [`negative`].
|
||||||
|
#[test]
|
||||||
|
fn audit_defect_regressions() {
|
||||||
|
negative::run_all();
|
||||||
|
}
|
||||||
|
|
||||||
/// Criterion 2 — **Crash safety.** A crash between any two syscalls in the
|
/// Criterion 2 — **Crash safety.** A crash between any two syscalls in the
|
||||||
/// commit path leaves the bundle openable — possibly at the previous
|
/// commit path leaves the bundle openable — possibly at the previous
|
||||||
/// generation, never corrupt (Chapter 8's atomic commit). Runs the testkit's
|
/// generation, never corrupt (Chapter 8's atomic commit). Runs the testkit's
|
||||||
|
|
@ -60,11 +87,18 @@ fn criterion_3_equivocation() {
|
||||||
equivocation::ops_equivocation_fuzz(2_000, 0x1234_5678);
|
equivocation::ops_equivocation_fuzz(2_000, 0x1234_5678);
|
||||||
}
|
}
|
||||||
|
|
||||||
/// Criterion 4 — **Canonical serialization stability.** The same canonical
|
/// Criterion 4 — **Canonical serialization stability (typed + container).** The
|
||||||
/// state serialized → loaded → re-serialized produces byte-identical bytes
|
/// same canonical value serialized → loaded → re-serialized produces
|
||||||
/// (Appendix D's canonical-serialization layer): the type-level round-trip
|
/// byte-identical bytes (Appendix D's canonical-serialization layer): the
|
||||||
/// corpus, Agent A's determinism gate (a slice), the bundle manifest/header, and
|
/// type-level round-trip corpus over every `CanonicalEncode` type in Agents A
|
||||||
/// a real score (operation-set → materialized bytes) round-trip through a bundle.
|
/// and B, Agent A's determinism gate (a slice), and the real bundle
|
||||||
|
/// manifest/header — including decoder rejection of corruption.
|
||||||
|
///
|
||||||
|
/// The **full-Score** byte round-trip is split out below: its bookkeeping
|
||||||
|
/// projection ([`reducer_bookkeeping_serialization`]) and its reproducibility
|
||||||
|
/// ([`full_score_materialization_is_reproducible`]) are exercised now; the
|
||||||
|
/// whole-`Score` byte codec is pending item 5 (Agent B) —
|
||||||
|
/// [`criterion_4_full_score_byte_roundtrip`].
|
||||||
#[test]
|
#[test]
|
||||||
fn criterion_4_canonical_serialization_stability() {
|
fn criterion_4_canonical_serialization_stability() {
|
||||||
roundtrip::run_roundtrip_corpus(100_000, 0x00C0_FFEE_1234_5678);
|
roundtrip::run_roundtrip_corpus(100_000, 0x00C0_FFEE_1234_5678);
|
||||||
|
|
@ -81,7 +115,20 @@ fn criterion_4_canonical_serialization_stability() {
|
||||||
roundtrip::assert_manifest_roundtrip(&rich);
|
roundtrip::assert_manifest_roundtrip(&rich);
|
||||||
// The decoder actually validates: corruption is rejected.
|
// The decoder actually validates: corruption is rejected.
|
||||||
roundtrip::assert_manifest_decode_rejects_corruption(&rich);
|
roundtrip::assert_manifest_decode_rejects_corruption(&rich);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
/// **Reducer-bookkeeping serialization** (the former, narrower half of criterion
|
||||||
|
/// 4, retained and honestly renamed). The canonical *bookkeeping projection*
|
||||||
|
/// (`MaterializedState::canonical_bytes`) survives content-addressed storage in
|
||||||
|
/// a real bundle and re-serializes byte-identically, and is musically sensitive
|
||||||
|
/// (same identities + changed content → different bytes). This is the Chapter 6
|
||||||
|
/// ledger, **not** the whole musical `Score`; the full-Score byte round-trip is
|
||||||
|
/// [`criterion_4_full_score_byte_roundtrip`] (pending item 5).
|
||||||
|
#[test]
|
||||||
|
fn reducer_bookkeeping_serialization() {
|
||||||
|
for seed in 0..48u64 {
|
||||||
|
let mut rng = Rng::new(seed.wrapping_mul(0x0100_0193).wrapping_add(17));
|
||||||
// The reduced canonical state survives content-addressed storage, and is
|
// The reduced canonical state survives content-addressed storage, and is
|
||||||
// musically sensitive: same identities + changed content → different bytes.
|
// musically sensitive: same identities + changed content → different bytes.
|
||||||
let session = generators::operation_envelopes(&mut rng, 40, 3, 6, 6);
|
let session = generators::operation_envelopes(&mut rng, 40, 3, 6, 6);
|
||||||
|
|
@ -93,6 +140,37 @@ fn criterion_4_canonical_serialization_stability() {
|
||||||
roundtrip::assert_content_mutation_changes_serialization();
|
roundtrip::assert_content_mutation_changes_serialization();
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/// **Full-Score materialization reproducibility** (achievable without the byte
|
||||||
|
/// codec). Reducing the same edit session onto the same base `Score` twice —
|
||||||
|
/// once in authored order, once shuffled — yields the *identical* materialized
|
||||||
|
/// `epiphany_core::Score` and bookkeeping state. This is the determinism
|
||||||
|
/// precondition any future whole-Score byte codec depends on, asserted today via
|
||||||
|
/// structural equality of the real graph (`reduce_onto`).
|
||||||
|
#[test]
|
||||||
|
fn full_score_materialization_is_reproducible() {
|
||||||
|
for seed in 0..16u64 {
|
||||||
|
convergence::run_graph_convergence(4, seed.wrapping_mul(0x0100_0193).wrapping_add(23));
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
/// Criterion 4 (full-Score byte round-trip) — **pending item 5 (Agent B).** A
|
||||||
|
/// whole-`epiphany_core::Score` / `GraphMaterialization` `encode → decode →
|
||||||
|
/// re-encode` byte round-trip requires the whole-score canonical codec
|
||||||
|
/// (`CanonicalEncode`/`CanonicalDecode for Score`), which does not exist yet:
|
||||||
|
/// today only the bookkeeping `MaterializedState` and the A/B typed values have
|
||||||
|
/// codecs. This gate is intentionally `#[ignore]`'d (visible as *ignored*, never
|
||||||
|
/// falsely green) until item 5 lands the codec; then drop the attribute and
|
||||||
|
/// assert the real byte cycle through a bundle snapshot.
|
||||||
|
#[test]
|
||||||
|
#[ignore = "pending item 5 (Agent B): whole-score codec (CanonicalEncode/Decode for Score) does not exist yet"]
|
||||||
|
fn criterion_4_full_score_byte_roundtrip() {
|
||||||
|
unimplemented!(
|
||||||
|
"blocked on item 5: epiphany_core::Score has no canonical byte codec. \
|
||||||
|
When it lands, reduce_onto a base, encode the Score, decode, and assert \
|
||||||
|
a byte-identical re-encode through a real bundle snapshot."
|
||||||
|
);
|
||||||
|
}
|
||||||
|
|
||||||
/// Criterion 5 — **Reduction determinism.** A randomized 1,000-envelope set,
|
/// Criterion 5 — **Reduction determinism.** A randomized 1,000-envelope set,
|
||||||
/// reduced 10 times in 10 different orders, produces byte-identical materialized
|
/// reduced 10 times in 10 different orders, produces byte-identical materialized
|
||||||
/// states *and* an identical canonical reduction order (Appendix D's
|
/// states *and* an identical canonical reduction order (Appendix D's
|
||||||
|
|
|
||||||
Loading…
Reference in New Issue