R-BA: delete the unreachable to.schemaId tiebreak from both edge comparators
Soul could not construct a selection where To.SchemaId decides the EdgesFor/page_edges order once From, Role and To.RecordKey already tie, but flagged that as a claim, not a proof - the same shape of argument that was wrong twice before on this comparator (R-AT). Traced instead of asserted: TryResolveReferenceTarget (C#) and resolve_reference_target (Rust) resolve a reference purely from the citer's schema, the role, and the record key, against the evaluation's own fixed candidate index (byKey/by_key) - no edge- or caller-specific input steers which candidate wins. Once From and Role tie (pinning the citer's schema and the declared target type/leaves) and To.RecordKey also ties, the resolved row - schema included - is forced identical by construction, in both runtimes, every time. No mutation can distinguish it because no input can, so it was deleted rather than recorded as "equivalent": a component nothing can distinguish is a line every future reader must reason about for no behavioural gain. Deletes the To.Descriptor.SchemaId/to.schema_id() ThenBy/then_with from CultNetSelectionEvaluator.EdgesFor and selection.rs's page_edges sort, and updates the comments (in-code and the Survivor 5 test block) that described the old five-key chain. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
This commit is contained in:
parent
cda28fa2ae
commit
492dd0e754
3 changed files with 43 additions and 19 deletions
|
|
@ -1837,8 +1837,18 @@ pub fn select<R: Row + Clone>(
|
|||
// whole batch. A selection carrying both `cites` and `cited` puts edges from both functions
|
||||
// into one `Vec`, and each edge already knows which end (R-V: (schemaId, recordKey)) is the
|
||||
// page row that produced it (`EdgeAnchor`): `cites` anchors on the citer (`from`), `cited`
|
||||
// anchors on the citee (`to`). Order is deterministic: page-row order, then (from, role, to)
|
||||
// in code-point order - never a `HashMap`'s iteration order.
|
||||
// anchors on the citee (`to`). Order is deterministic: page-row order, then (from, role,
|
||||
// to.record_key) in code-point order - never a `HashMap`'s iteration order.
|
||||
//
|
||||
// R-BA (docs/cultnet-selection-cut.md, "Soul, the merge gate, fourth pass"): `to.schema_id`
|
||||
// used to sit last in this tiebreak and has been deleted. `resolve_reference_target` (this
|
||||
// file) resolves purely from `(role, record_key)` against the evaluation's own fixed `by_key`
|
||||
// and `target_leaves(role)` - neither depends on which edge or which `from` is asking - so
|
||||
// within one evaluation the same `(role, record_key)` pair always resolves to the same row,
|
||||
// schema included. That means once `from`, `role` and `to.record_key` already tie, `to.schema_id`
|
||||
// is forced equal; no input can make it decide an order the earlier four keys did not already
|
||||
// decide. Soul verified no construction breaks this (a component that cannot be distinguished
|
||||
// by any input is a line every future reader must reason about for no behavioural gain).
|
||||
let page_edges = if selection.has_hop() {
|
||||
let page_position: HashMap<(&str, &str), usize> = page
|
||||
.iter()
|
||||
|
|
@ -1861,7 +1871,6 @@ pub fn select<R: Row + Clone>(
|
|||
.then_with(|| a.from.schema_id().cmp(b.from.schema_id()))
|
||||
.then_with(|| a.from.record_key().cmp(b.from.record_key()))
|
||||
.then_with(|| a.role.cmp(&b.role))
|
||||
.then_with(|| a.to.schema_id().cmp(b.to.schema_id()))
|
||||
.then_with(|| a.to.record_key().cmp(b.to.record_key()))
|
||||
});
|
||||
kept
|
||||
|
|
|
|||
|
|
@ -286,11 +286,22 @@ namespace GameCult.Networking
|
|||
return new Evaluation { Rows = page, Edges = pageEdges, NextCursor = nextCursor, TotalMatched = ordered.Count };
|
||||
}
|
||||
|
||||
// R-B: the order is deterministic - the page-row order, then (from, role, to) in code-point
|
||||
// order. Grouping by the row an edge is anchored to (LINQ's OrderBy is stable, so the given
|
||||
// rows' own order survives as the primary key) and breaking ties by the edge's own identity
|
||||
// gives both without a second pass. Public because a v0/shard full walk (R-G, one evaluation
|
||||
// answering every page) reports edges against its whole matched set, not one 200-row page.
|
||||
// R-B: the order is deterministic - the page-row order, then (from, role, to.recordKey) in
|
||||
// code-point order. Grouping by the row an edge is anchored to (LINQ's OrderBy is stable, so
|
||||
// the given rows' own order survives as the primary key) and breaking ties by the edge's own
|
||||
// identity gives both without a second pass. Public because a v0/shard full walk (R-G, one
|
||||
// evaluation answering every page) reports edges against its whole matched set, not one
|
||||
// 200-row page.
|
||||
//
|
||||
// R-BA (docs/cultnet-selection-cut.md, "Soul, the merge gate, fourth pass"): a
|
||||
// `To.Descriptor.SchemaId` tiebreak used to sit last here and has been deleted.
|
||||
// TryResolveReferenceTarget (this file) resolves purely from a fixed target type - itself
|
||||
// determined only by the citer's schema and the role, both already pinned once `From` and
|
||||
// `Role` tie - plus the record key, against the evaluation's own fixed `byKey`; no edge or
|
||||
// caller-specific input steers it. So within one evaluation the same (citer schema, role,
|
||||
// recordKey) always resolves to the same row, schema included: once `From`, `Role` and
|
||||
// `To.RecordKey` already tie, `To.SchemaId` is forced equal and cannot decide an order the
|
||||
// earlier four keys did not already decide. Soul verified no construction breaks this.
|
||||
public static EdgeMatch[] EdgesFor(IReadOnlyList<Row> rows, FullEvaluation full)
|
||||
{
|
||||
// R-V: the anchor lookup is keyed by (schemaId, recordKey), not the bare key - two schemas'
|
||||
|
|
@ -307,7 +318,6 @@ namespace GameCult.Networking
|
|||
.ThenBy(pair => pair.Edge.From.Descriptor.SchemaId, CultNetCodePointComparer.Instance)
|
||||
.ThenBy(pair => pair.Edge.From.Key.Value, CultNetCodePointComparer.Instance)
|
||||
.ThenBy(pair => pair.Edge.Role, CultNetCodePointComparer.Instance)
|
||||
.ThenBy(pair => pair.Edge.To.Descriptor.SchemaId, CultNetCodePointComparer.Instance)
|
||||
.ThenBy(pair => pair.Edge.To.Key.Value, CultNetCodePointComparer.Instance)
|
||||
.Select(pair => pair.Edge)
|
||||
.ToArray();
|
||||
|
|
|
|||
|
|
@ -248,16 +248,21 @@ namespace GameCult.Networking.Tests
|
|||
}
|
||||
|
||||
// ---------------------------------------------------------------------------------------------
|
||||
// Survivor 5: CultNetSelectionEvaluator.EdgesFor - the five ordering keys after page-row
|
||||
// position (From.SchemaId, From.Key, Role, To.SchemaId, To.Key) each mutated ThenBy<->
|
||||
// ThenByDescending. Rule (R-B): "page-row order, then (from, role, to) in code-point order."
|
||||
// Two behavioural angles: the From.SchemaId tiebreak (two differently-schema'd citers, same
|
||||
// key, citing one target under the same role), and the Role tiebreak (one citer with two
|
||||
// reference members that both resolve to the same target, so From and To tie and only Role
|
||||
// differs). To.SchemaId/To.Key could not be isolated: within one hop direction, an edge's
|
||||
// (From, Role) already determines its To deterministically (one declared value per member), so
|
||||
// two edges sharing an anchor, From and Role always share To too - see the equivalence note at
|
||||
// the bottom of this file.
|
||||
// Survivor 5: CultNetSelectionEvaluator.EdgesFor - the ordering keys after page-row position
|
||||
// (From.SchemaId, From.Key, Role, To.Key) each mutated ThenBy<->ThenByDescending. Rule (R-B):
|
||||
// "page-row order, then (from, role, to.recordKey) in code-point order." Two behavioural
|
||||
// angles: the From.SchemaId tiebreak (two differently-schema'd citers, same key, citing one
|
||||
// target under the same role), and the Role tiebreak (one citer with two reference members
|
||||
// that both resolve to the same target, so From and To tie and only Role differs).
|
||||
//
|
||||
// A fifth component, To.SchemaId, used to sit last in this chain. R-BA (docs/cultnet-selection
|
||||
// -cut.md, "Soul, the merge gate, fourth pass") deleted it from both runtimes'
|
||||
// comparators: TryResolveReferenceTarget/resolve_reference_target resolve purely from
|
||||
// (the citer's schema, role, recordKey) against the evaluation's own fixed candidate index, so
|
||||
// once From and Role already tie (pinning the citer's schema and the target type/leaves) and
|
||||
// To.RecordKey also ties, To.SchemaId is forced equal - no input can make it decide an order
|
||||
// the earlier keys did not already decide, so a Stryker mutant on it cannot be killed and the
|
||||
// component bought nothing.
|
||||
// ---------------------------------------------------------------------------------------------
|
||||
[Test]
|
||||
public void EdgesFor_BreaksATiedAnchorByFromSchemaIdWhenFromKeysAreEqual()
|
||||
|
|
|
|||
Loading…
Reference in a new issue