diff --git a/crates/epiphany-ops/src/reduce.rs b/crates/epiphany-ops/src/reduce.rs index f678ace..6f0a195 100644 --- a/crates/epiphany-ops/src/reduce.rs +++ b/crates/epiphany-ops/src/reduce.rs @@ -13221,13 +13221,24 @@ mod tests { } /// (s3) A re-write of an identical value is a **new write**, not a - /// no-op: assert the effect is `Applied` and not `AlreadyApplied`. This - /// test exists because pin 5 is the most likely thing for a subagent to - /// get wrong by pattern-matching on `create_staff`'s mint discipline. + /// no-op. This test exists because pin 5 is the most likely thing for a + /// subagent to get wrong by pattern-matching on `create_staff`'s mint + /// discipline. /// - /// **Mutation:** add an `AlreadyApplied` short-circuit to the setter fn - /// (skip the record-and-write when the new value equals the current one) - /// -> dies. + /// The contract requires proving **both** halves: that the effect is + /// `Applied`, *and* that the write chain grew. Asserting effects alone is + /// insufficient — a mutant that returns `Applied` while skipping + /// `WriteChain::record` for an unchanged value passes an effects-only + /// test, and the damage surfaces only later, when undoing the earlier + /// transaction restores the base instead of reporting that the identical + /// later write superseded it. So the two writes here sit in **different + /// transactions**, and a strict undo of the first must report + /// supersession naming the second. + /// + /// **Mutations, both required:** (a) add an `AlreadyApplied` + /// short-circuit to the setter fn -> the effect half dies; (b) keep + /// `Applied` but skip `record` when the value is unchanged -> the + /// supersession half dies while the effect half stays green. #[test] fn rewriting_an_identical_settings_value_is_a_new_write_not_a_no_op() { let identity = IdentityContext::new(ReplicaId(1)); @@ -13252,7 +13263,7 @@ mod tests { ); let mut set = OperationSet::new(); set.accept_all(vec![first.clone(), second.clone()]); - let out = reduce_operation_set_onto(&set, &Score::empty(identity)); + let out = reduce_operation_set_onto(&set, &Score::empty(identity.clone())); assert_eq!( effect_at(&out.state, 0), @@ -13264,6 +13275,65 @@ mod tests { Some(&OperationEffect::Applied), "a byte-identical re-write is still a new Applied write, not AlreadyApplied" ); + + // The chain-growth half. Effects alone cannot see a mutant that + // returns `Applied` without recording, so put the two identical + // writes in different transactions and strict-undo the first: the + // chain must report the identical second write as superseding it. + let tx_a = TransactionId::from_raw(91); + let tx_b = TransactionId::from_raw(92); + let declare_a = declare_transaction(1, 0, 10, CausalContext::new(), tx_a); + let declare_b = declare_transaction(1, 2, 30, seen_r1(1), tx_b); + let mut write_a = prim_env( + 1, + 1, + 20, + seen_r1(0), + OperationKind::SetSpellingPrecedence(SetSpellingPrecedenceOp { + precedence: precedence.clone(), + }), + ); + write_a.transaction = Some(tx_a); + let mut write_b = prim_env( + 1, + 3, + 40, + seen_r1(2), + OperationKind::SetSpellingPrecedence(SetSpellingPrecedenceOp { + precedence: precedence.clone(), + }), + ); + write_b.transaction = Some(tx_b); + let strict = undo_env(1, 4, 50, seen_r1(3), tx_a, UndoPolicy::StrictInverse); + let mut set = OperationSet::new(); + set.accept_all(vec![ + declare_a, + write_a, + declare_b, + write_b.clone(), + strict.clone(), + ]); + let out = reduce_operation_set_onto(&set, &Score::empty(identity)); + + assert!( + matches!( + effect_at(&out.state, 4), + Some(OperationEffect::Conflicted { .. }) + ), + "the identical later write must supersede tx_a's strict undo — if \ + this passes as Applied, the second write was never recorded" + ); + let record = out + .state + .conflicts + .records() + .iter() + .find(|record| record.caused_by.contains(&strict.id)) + .expect("the strict undo records a conflict"); + assert!( + record.caused_by.contains(&write_b.id), + "the supersession must name the identical second write" + ); } /// (s4) Value-restoring undo reaches the seeded base — run both diff --git a/crates/epiphany-ops/src/textproj_kind.rs b/crates/epiphany-ops/src/textproj_kind.rs index f210e88..f1646ca 100644 --- a/crates/epiphany-ops/src/textproj_kind.rs +++ b/crates/epiphany-ops/src/textproj_kind.rs @@ -646,9 +646,14 @@ mod tests { /// struct wrapping a sequence), so mislabeling one as the other is /// rejected rather than mis-round-tripped. /// - /// **Mutation:** none needed to demonstrate the reject — this test *is* - /// the reject-path exercise the contract asks for; a genuine defect - /// would be a decoder that silently accepted the mismatched shape. + /// **Mutation (required, and run):** make the parse arm silently accept a + /// mismatched shape — `TextValue::parse(layout_defaults).unwrap_or_default()` + /// in place of the `?` — which is exactly the defect this test names. The + /// assertion fires. An earlier note here claimed no mutation was needed + /// because the test *is* the reject-path exercise; that reasoning was + /// wrong. Being a reject-path test does not establish that the rejection + /// is caused by the mislabeling rather than by something incidental, and + /// only running the mutation shows the assertion is not vacuous. #[test] fn one_settings_kind_production_under_the_others_tag_is_rejected() { let precedence_sample = sample_kind(OperationKindTag::SetSpellingPrecedence); diff --git a/crates/epiphany-testkit/src/generators.rs b/crates/epiphany-testkit/src/generators.rs index 39ebf50..0603b1c 100644 --- a/crates/epiphany-testkit/src/generators.rs +++ b/crates/epiphany-testkit/src/generators.rs @@ -1832,35 +1832,64 @@ mod tests { /// stamps well within the `OperationEnvelopeBlock` accept-set no matter /// where that set's ceiling sits. /// - /// The other half of s6 — `max_supported_major(OperationEnvelopeBlock) == - /// 2` — is **not** assertable from this crate: `epiphany_bundle:: - /// max_supported_major` (`bundle.rs:67`) is defined in a private module - /// (`mod bundle;`, not `pub mod`) and is not among `epiphany-bundle`'s - /// `pub use` re-exports, so no outside crate can name it. Contract pin 4a - /// forbids touching `epiphany-bundle` in this packet (not even to add a - /// re-export), so that half of s6 is verified by reading - /// `crates/epiphany-bundle/src/bundle.rs:69` directly (`ChunkKind:: - /// OperationEnvelopeBlock => 2`, unedited by this packet) rather than by - /// a compiled assertion — a deviation from the contract's "assert it in - /// code" phrasing, reported rather than worked around. + /// The accept-set ceiling itself (`max_supported_major( + /// OperationEnvelopeBlock) == 2`) is **already** asserted in a compiled + /// test inside `epiphany-bundle` (`bundle.rs:1322`), which predates this + /// packet and which this packet leaves untouched. An earlier draft of + /// this comment claimed that half of s6 was unassertable because + /// `max_supported_major` is not re-exported — the privacy observation is + /// true but the conclusion was wrong, since the assertion does not need + /// to live *outside* the crate. **No re-export is needed, here or by the + /// G-minor rung.** + /// + /// What this test adds is the half the in-crate assertion cannot cover: + /// that a *staged block* carrying either new kind stamps major 0, which + /// is the contract's actual claim and which exercises the writer-side + /// derivation (`stage_operation_block`) rather than the bare kind. /// /// **Mutation:** stamp a payload carrying either new kind at a non-zero /// major (as if it had been wrongly placed in the `=> 2` arm alongside - /// `SetMetadata`, exactly the bug pin 3 and test s5 both name) — this - /// assertion fires. + /// `SetMetadata`, exactly the bug pin 3 and test s5 both name) — both + /// assertions fire. #[test] fn the_two_new_settings_kinds_stamp_within_the_accept_set() { - for major in [ + let kinds = [ OperationKind::SetCanvasLayoutDefaults(SetCanvasLayoutDefaultsOp { layout_defaults: valuegen::canvas_layout_defaults(1), - }) - .schema_major(), + }), OperationKind::SetSpellingPrecedence(SetSpellingPrecedenceOp { precedence: valuegen::spelling_precedence(1), - }) - .schema_major(), - ] { - assert_eq!(major, 0, "both new kinds must stamp at major 0"); + }), + ]; + for kind in &kinds { + assert_eq!( + kind.schema_major(), + 0, + "both new kinds must stamp at major 0" + ); + } + // The contract's claim is about the BLOCK, not the bare kind: a block + // carrying either kind must stamp major 0 through the writer-side + // derivation every real staging path uses. + for (n, kind) in kinds.into_iter().enumerate() { + let id = OperationId::new(ReplicaId(1), n as u64); + let env = OperationEnvelope { + id, + author: AuthorId(1), + stamp: OperationStamp::new( + HybridLogicalClock::new(WallClockTime(10 + n as i64), 0), + id, + ), + causal_context: CausalContext::new(), + transaction: None, + payload: OperationPayload::Primitive(kind), + }; + assert!(epiphany_ops::well_formed(&env).is_ok()); + let staged = crate::bundle_harness::stage_operation_block(&[env]); + assert_eq!( + staged.schema_version.major, 0, + "a staged block carrying a G2a setter stamps major 0" + ); } } diff --git a/spec/core_spec.pdf b/spec/core_spec.pdf index e83bf74..10b3577 100644 Binary files a/spec/core_spec.pdf and b/spec/core_spec.pdf differ diff --git a/spec/core_spec.tex b/spec/core_spec.tex index b6f3047..19866c5 100644 --- a/spec/core_spec.tex +++ b/spec/core_spec.tex @@ -12219,12 +12219,18 @@ operation layer, because \texttt{CreateRegion} embeds a full \texttt{Region}, so an operation-envelope block bearing a v1 \texttt{CreateRegion} is major~1. (As of the genesis operation tranche, \texttt{Canvas.layout\_defaults} and \texttt{Instrument.range} do too --- \texttt{SetCanvasLayoutDefaults} -(G2a) and \texttt{CreateInstrument} (G1) embed the values directly --- but -neither of those two payloads is itself major~1: the leaf value each embeds -has exactly one layout, versioned only through the containing -\texttt{Canvas}/\texttt{Instrument} walk, not through this schema-major-1 -bump. See the Binary Format companion \sectionsc{Schema Major 1} / -\sectionsc{Schema Major 2} for the operation-by-operation accounting.) +(G2a) and \texttt{CreateInstrument} (G1) embed them --- but neither payload +is major~1, and for \emph{different} reasons. +\texttt{SetCanvasLayoutDefaults} carries the leaf +\texttt{CanvasLayoutDefaults}, which has exactly one layout: the versioning +sits in the containing \texttt{Canvas} walk, never in the leaf, so the +payload stamps major~0. \texttt{CreateInstrument} carries a whole +\texttt{Instrument}, which does have distinct major-0, major-1, and major-2 +layouts --- so it is not major~1 because it is \emph{always major~2}: the +schema-major-2 appends are mandatory rather than \texttt{Option}-hidden, so +no lower-major layout for that payload exists at any value. See the Binary +Format companion \sectionsc{Schema Major 1} / \sectionsc{Schema Major 2} for +the operation-by-operation accounting.) Consequently a major-0-only reader opens a major-1 bundle \emph{fully} only when the bundle carries no v1 \texttt{CreateRegion} operation; otherwise it reads the major-0 canonical base and manifest but opens read-only (it cannot