G2a review fixes: a false deviation, and two tests that proved less than claimed

Four findings, all confirmed against the tree.

The accept-set "deviation" was not real, and I propagated it. bundle.rs:1322
has asserted max_supported_major(OperationEnvelopeBlock) == 2 since before
this packet, so the gate was always satisfiable; the privacy observation about
the symbol not being re-exported is true but irrelevant, because the assertion
never needed to live outside the crate. I checked the premise and not the
conclusion, then reported it as verified. No re-export is needed here or by
G-minor. The test now also asserts what the contract actually asked for -- that
a staged block carrying either kind stamps major 0, exercising the writer-side
derivation rather than the bare kind.

s3 asserted effects only, though the contract required chain growth too. A
mutant returning Applied while skipping WriteChain::record for an unchanged
value passed it, and the damage would surface only later as an undo restoring
the base instead of reporting supersession. The two identical writes now sit in
different transactions and a strict undo of the first must report the second as
superseding; mutation (b) kills exactly that half while the effects half stays
green.

s9 claimed no mutation was needed because the test is itself a reject-path
exercise. That reasoning was wrong: being a reject-path test does not show the
rejection is caused by the mislabeling rather than something incidental. The
mutation -- a parse arm that silently accepts a mismatched shape -- was both
performable and killing.

core_spec grouped SetCanvasLayoutDefaults and CreateInstrument as leaves with a
single layout. True only of the first. Instrument has distinct major-0/1/2
layouts and stamps major 2 unconditionally because its major-2 appends are
mandatory, so it is not major 1 for the opposite reason. Split.

All ten contract mutations now have observed kill evidence: s1, s2, s4, s8 and
s10's row-28 half were run here alongside the four recorded earlier. s8 killed
only the two pinned literal-byte vectors while 217 round-trip tests stayed
green -- the 3b-i property, demonstrated rather than asserted.

Gate: fmt clean, clippy 0, 1371 passed / 0 failed, conformance 8/8 and 9/9,
labels 6/6, core_spec PDF 0 undefined refs, goldens byte-identical,
epiphany-bundle diff empty.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01QjsEnYhm1gPpf6ii2iFxFV

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
+    /// no-op. This test exists because pin 5 is the most likely thing for a
-    /// test exists because pin 5 is the most likely thing for a subagent to
+    /// subagent to get wrong by pattern-matching on `create_staff`'s mint
-    /// get wrong by pattern-matching on `create_staff`'s mint discipline.
+    /// discipline.
     ///
-    /// **Mutation:** add an `AlreadyApplied` short-circuit to the setter fn
+    /// The contract requires proving **both** halves: that the effect is
-    /// (skip the record-and-write when the new value equals the current one)
+    /// `Applied`, *and* that the write chain grew. Asserting effects alone is
-    /// -> dies.
+    /// 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

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*
+    /// **Mutation (required, and run):** make the parse arm silently accept a
-    /// the reject-path exercise the contract asks for; a genuine defect
+    /// mismatched shape — `TextValue::parse(layout_defaults).unwrap_or_default()`
-    /// would be a decoder that silently accepted the mismatched shape.
+    /// 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);

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) ==
+    /// The accept-set ceiling itself (`max_supported_major(
-    /// 2` — is **not** assertable from this crate: `epiphany_bundle::
+    /// OperationEnvelopeBlock) == 2`) is **already** asserted in a compiled
-    /// max_supported_major` (`bundle.rs:67`) is defined in a private module
+    /// test inside `epiphany-bundle` (`bundle.rs:1322`), which predates this
-    /// (`mod bundle;`, not `pub mod`) and is not among `epiphany-bundle`'s
+    /// packet and which this packet leaves untouched. An earlier draft of
-    /// `pub use` re-exports, so no outside crate can name it. Contract pin 4a
+    /// this comment claimed that half of s6 was unassertable because
-    /// forbids touching `epiphany-bundle` in this packet (not even to add a
+    /// `max_supported_major` is not re-exported — the privacy observation is
-    /// re-export), so that half of s6 is verified by reading
+    /// true but the conclusion was wrong, since the assertion does not need
-    /// `crates/epiphany-bundle/src/bundle.rs:69` directly (`ChunkKind::
+    /// to live *outside* the crate. **No re-export is needed, here or by the
-    /// OperationEnvelopeBlock => 2`, unedited by this packet) rather than by
+    /// G-minor rung.**
-    /// a compiled assertion — a deviation from the contract's "assert it in
+    ///
-    /// code" phrasing, reported rather than worked around.
+    /// 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
+    /// `SetMetadata`, exactly the bug pin 3 and test s5 both name) — both
-    /// assertion fires.
+    /// 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(),
+        ];
-        ] {
+        for kind in &kinds {
-            assert_eq!(major, 0, "both new kinds must stamp at major 0");
+            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"
+            );
         }
     }
 

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
+(G2a) and \texttt{CreateInstrument} (G1) embed them --- but neither payload
-neither of those two payloads is itself major~1: the leaf value each embeds
+is major~1, and for \emph{different} reasons.
-has exactly one layout, versioned only through the containing
+\texttt{SetCanvasLayoutDefaults} carries the leaf
-\texttt{Canvas}/\texttt{Instrument} walk, not through this schema-major-1
+\texttt{CanvasLayoutDefaults}, which has exactly one layout: the versioning
-bump. See the Binary Format companion \sectionsc{Schema Major 1} /
+sits in the containing \texttt{Canvas} walk, never in the leaf, so the
-\sectionsc{Schema Major 2} for the operation-by-operation accounting.)
+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