P13-S26 EXECUTED: invariant 10 names its derived reference surface
Item 10 said only that "every cross-cutting structure's references resolve to extant objects", naming no individual class, while the checker enforced a surface spanning cross-cutting structures, structural top-level references, meter references at every level a MeterChange appears, an attachment-internal reference, event-internal references and the tempo map's segment anchors. The Rust doc comment named many of those and not all. The two were incomplete in different places, so neither could be repaired from the other; both are now written from one table derived by reading every emitted condition in the four functions that raise the tag -- 41 tokens, each with its resolution target and a symbolic anchor back to the control flow that enforces it. Two of the ledger row's own claims did not survive scoping and were corrected at ratification rather than carried: the G3a aside is ambiguous, not false, and the two-sided repair stands on incompleteness rather than on a falsehood. Guarded by exact (token, target) set equality in a new testkit suite, against an oracle validated before use. Ordering and vocabulary are separate assertions because an out-of-vocabulary term sorts perfectly well. Duplicates are checked on the raw extraction, which set comparison cannot see. Item 10's opening sentence is the slice anchor as a complete literal, required to occur exactly once, so pin 3's retention of it is machine-observed rather than asserted. t12 is narrowed and renamed, not deleted: cargo test -p epiphany-core must still fail when the doc block is destroyed, and testkit is another crate. Chapter 3 gains req:time:aleatoric-reference-locality -- an aleatoric region's ordering and bounds references must name events of that same region, a locality rule the checker always enforced and no requirement stated. Its three count constants were measured at execution, never predicted: 214/285/285 -> 215/286/286. 38 mutations, 38 matching radii, every one against the full workspace with --no-fail-fast and restored by hand write-back. M3 is the single passing control: with equality weakened to actual.is_subset(&expected), M1-B stops failing, which is what makes exactness load-bearing rather than assumed. Two harness faults halted the run and are recorded in the annex rather than smoothed over; the second exposed a real weakness in the requirement guard, reported and left for amendment 3. Files two candidates this rung does not repair: P13-S29, the invariant-10 tag multiplexing Chapter 3/4 failures through a public API and its Display; and P13-S30, the repository-wide assumption that TeX is spelled exactly, whose requirement-block branch is demonstrated by this rung's own M20. Baseline 42 suites/1583 -> 43/1586: one new suite, three tests, none removed. Clippy and the pinned fmt gate clean on 1.95.0; core_spec.pdf rebuilt with zero undefined references. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Ps1szk2mSfgp4Cz21eVH9x
This commit is contained in:
parent
86bf7c65b9
commit
eddf6e9c6d
|
|
@ -66,18 +66,67 @@ pub enum GraphInvariant {
|
|||
MeasureSingleInstance,
|
||||
/// 9. Each anchor's offset variant agrees with its target's time model.
|
||||
AnchorOffsetModel,
|
||||
/// 10. Every graph reference resolves to an extant object: cross-cutting
|
||||
/// structures (incl. anchor targets, annotation layers, tuplet parents,
|
||||
/// graphic objects) and event-internal references (indeterminate
|
||||
/// alternatives, trajectory event-pitches, graphic objects, cue sources);
|
||||
/// structural top-level references (a staff's declared instrument, a
|
||||
/// staff's group, a staff group's members, a part's staves, a view's
|
||||
/// active layers — genesis tranche G3a repairs this prose to name what
|
||||
/// the check body already enforced); and meter/time-signature
|
||||
/// references at every level a `MeterChange` can appear (a region's
|
||||
/// time-model meter changes, a region's default metric grid, a
|
||||
/// measure's declared time signature, a staff instance's local metric
|
||||
/// grid).
|
||||
/// 10. Every graph reference resolves to an extant object, except where
|
||||
/// the re-anchoring rules explicitly permit transient dangling states
|
||||
/// during edits. This surface is **derived from the check bodies**, not
|
||||
/// copied from prose: `spec/CONTRACT_P13S26_INVARIANT10_SURFACE.md`
|
||||
/// pin 1 is the sole origin for both this list and `core_spec.tex`'s
|
||||
/// item 10, because the two were incomplete in different places and
|
||||
/// neither could be repaired from the other (P13-S26).
|
||||
///
|
||||
/// - Slur.start_event — live event.
|
||||
/// - Slur.end_event — live event.
|
||||
/// - Tie.start_event — live event.
|
||||
/// - Tie.end_event — live event.
|
||||
/// - Beam.events — live event.
|
||||
/// - SubBeam.events — live event.
|
||||
/// - Tuplet.members — live event.
|
||||
/// - Tuplet.parent — extant tuplet.
|
||||
/// - Spanner.staves — declared staff.
|
||||
/// - Spanner.start — anchor target.
|
||||
/// - Spanner.end — anchor target.
|
||||
/// - Marker.anchor — anchor target.
|
||||
/// - RepeatStructure.start — anchor target.
|
||||
/// - RepeatStructure.end — anchor target.
|
||||
/// - RepeatStructure.kind — anchor target.
|
||||
/// - RepeatStructure.voltas — anchor target.
|
||||
/// - ChordSymbol.anchor — anchor target.
|
||||
/// - AnalyticalAnnotation.anchor — anchor target, extant region, live event.
|
||||
/// - AnalyticalAnnotation.layer — declared analysis layer.
|
||||
/// - Comment.anchor — anchor target, extant region, live event.
|
||||
/// - GraphicGesture.objects — stored graphic object.
|
||||
/// - GraphicGesture.anchoring — anchor target, declared staff, live event.
|
||||
/// - LyricLine.events — live event.
|
||||
/// - Staff.instrument — declared instrument.
|
||||
/// - StaffInstance.instrument_override — declared instrument.
|
||||
/// - Staff.group — declared staff group.
|
||||
/// - StaffGroup.members — declared staff.
|
||||
/// - PartDefinition.staves — declared staff.
|
||||
/// - ViewDefinition.active_layers — declared analysis layer.
|
||||
/// - MetricTimeModel.meters — declared time signature.
|
||||
/// - StaffBasedContent.default_metric_grid — declared time signature.
|
||||
/// - Measure.time_signature — declared time signature.
|
||||
/// - StaffInstance.local_metric_grid — declared time signature.
|
||||
/// - NotatedComponent.tuplet — extant tuplet.
|
||||
/// - IndeterminacyHints.alternatives — live event.
|
||||
/// - TrajectoryEvent.start — live pitch.
|
||||
/// - TrajectoryEvent.end — live pitch.
|
||||
/// - GraphicEvent.graphics — stored graphic object.
|
||||
/// - CueEvent.source — live event.
|
||||
/// - TempoSegment.start — anchor target.
|
||||
/// - TempoSegment.end — anchor target.
|
||||
///
|
||||
/// Beyond that surface, further checks are reported under this same tag
|
||||
/// and are NOT part of the normative invariant 10: tempo-map segment
|
||||
/// shape, ordering and non-overlap (Chapter 3,
|
||||
/// `req:time:tempo-segment-order`); aleatoric ordering and bounds
|
||||
/// region locality (Chapter 3,
|
||||
/// `req:time:aleatoric-reference-locality`); and accidental
|
||||
/// modification expressibility (Chapter 4,
|
||||
/// `req:tuning:accidental-modification-compatibility`). That
|
||||
/// multiplexing is filed as P13-S29 — the public `check_invariant`
|
||||
/// filter and this violation's `Display` attribute those failures to
|
||||
/// invariant 10. Repairing it is a behaviour change, out of scope here.
|
||||
CrossCuttingRefsResolve,
|
||||
/// 11. Identifiers are unique within their kind (every id kind), with
|
||||
/// reserved-namespace (`SYSTEM_DERIVED`) misuse, tombstone/live
|
||||
|
|
@ -4645,7 +4694,12 @@ mod g3a_tests {
|
|||
/// **Mutation:** revert the doc comment to its pre-G3a text (naming only
|
||||
/// cross-cutting structures and event-internal references); must fail.
|
||||
#[test]
|
||||
fn t12_invariant_10_doc_comment_names_the_four_reference_classes() {
|
||||
fn t12_invariant_10_doc_block_slices_and_is_non_empty() {
|
||||
// Narrowed by P13-S26 pin 8. The exact (token, target) comparison lives
|
||||
// in epiphany-testkit's `invariant_ten_surface` guard, which reads both
|
||||
// this block and `core_spec.tex`. This one stays because
|
||||
// `cargo test -p epiphany-core` must still fail when the block is
|
||||
// destroyed, and testkit is a different crate.
|
||||
let source = production_source();
|
||||
let start = source
|
||||
.find(" /// 10. Every graph reference resolves")
|
||||
|
|
@ -4656,17 +4710,18 @@ mod g3a_tests {
|
|||
.expect("the CrossCuttingRefsResolve variant follows its doc comment");
|
||||
let doc_block = &source[start..end];
|
||||
|
||||
for needle in [
|
||||
"staff's group",
|
||||
"group's members",
|
||||
"part's staves",
|
||||
"active layers",
|
||||
] {
|
||||
assert!(
|
||||
doc_block.contains(needle),
|
||||
"invariant 10's doc comment must name `{needle}`; block was:\n{doc_block}"
|
||||
);
|
||||
}
|
||||
let tokens: Vec<&str> = doc_block
|
||||
.lines()
|
||||
.filter_map(|line| line.trim_start().strip_prefix("/// "))
|
||||
.filter_map(|rest| rest.trim_start().strip_prefix("- "))
|
||||
.filter_map(|rest| rest.split_whitespace().next())
|
||||
.collect();
|
||||
|
||||
assert!(
|
||||
!tokens.is_empty(),
|
||||
"invariant 10's doc block must list its reference surface, one \
|
||||
`- Token — target.` line per class; block was:\n{doc_block}"
|
||||
);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -0,0 +1,412 @@
|
|||
//! Invariant 10's reference surface, compared against both documents that
|
||||
//! summarise it.
|
||||
//!
|
||||
//! P13-S26. `core_spec.tex`'s item 10 and `invariants.rs`' `/// 10.` doc block
|
||||
//! are summaries of one thing: the reference classes
|
||||
//! `GraphIndex::check_cross_cutting_refs` and the tempo-map check enforce.
|
||||
//! Before this rung they were incomplete in *different* places, so neither
|
||||
//! could be repaired from the other. `INVARIANT_TEN_SURFACE` below is the
|
||||
//! contract's pin-1 table in machine-readable form, derived from the check
|
||||
//! bodies, and both documents are compared against **it** rather than against
|
||||
//! each other.
|
||||
//!
|
||||
//! It is not a second list of something derivable: the derivation source is
|
||||
//! Rust control flow, which is not parseable. The contract's gate 8 re-derives
|
||||
//! this table by hand after every edit; that is the standing compensation.
|
||||
|
||||
use std::collections::{BTreeMap, BTreeSet};
|
||||
use std::fs;
|
||||
use std::path::{Path, PathBuf};
|
||||
|
||||
/// Pin 1's (token, target) table, verbatim. The ratified origin.
|
||||
const INVARIANT_TEN_SURFACE: &[(&str, &str)] = &[
|
||||
("Slur.start_event", "live event"),
|
||||
("Slur.end_event", "live event"),
|
||||
("Tie.start_event", "live event"),
|
||||
("Tie.end_event", "live event"),
|
||||
("Beam.events", "live event"),
|
||||
("SubBeam.events", "live event"),
|
||||
("Tuplet.members", "live event"),
|
||||
("Tuplet.parent", "extant tuplet"),
|
||||
("Spanner.staves", "declared staff"),
|
||||
("Spanner.start", "anchor target"),
|
||||
("Spanner.end", "anchor target"),
|
||||
("Marker.anchor", "anchor target"),
|
||||
("RepeatStructure.start", "anchor target"),
|
||||
("RepeatStructure.end", "anchor target"),
|
||||
("RepeatStructure.kind", "anchor target"),
|
||||
("RepeatStructure.voltas", "anchor target"),
|
||||
("ChordSymbol.anchor", "anchor target"),
|
||||
(
|
||||
"AnalyticalAnnotation.anchor",
|
||||
"anchor target, extant region, live event",
|
||||
),
|
||||
("AnalyticalAnnotation.layer", "declared analysis layer"),
|
||||
("Comment.anchor", "anchor target, extant region, live event"),
|
||||
("GraphicGesture.objects", "stored graphic object"),
|
||||
(
|
||||
"GraphicGesture.anchoring",
|
||||
"anchor target, declared staff, live event",
|
||||
),
|
||||
("LyricLine.events", "live event"),
|
||||
("Staff.instrument", "declared instrument"),
|
||||
("StaffInstance.instrument_override", "declared instrument"),
|
||||
("Staff.group", "declared staff group"),
|
||||
("StaffGroup.members", "declared staff"),
|
||||
("PartDefinition.staves", "declared staff"),
|
||||
("ViewDefinition.active_layers", "declared analysis layer"),
|
||||
("MetricTimeModel.meters", "declared time signature"),
|
||||
(
|
||||
"StaffBasedContent.default_metric_grid",
|
||||
"declared time signature",
|
||||
),
|
||||
("Measure.time_signature", "declared time signature"),
|
||||
("StaffInstance.local_metric_grid", "declared time signature"),
|
||||
("NotatedComponent.tuplet", "extant tuplet"),
|
||||
("IndeterminacyHints.alternatives", "live event"),
|
||||
("TrajectoryEvent.start", "live pitch"),
|
||||
("TrajectoryEvent.end", "live pitch"),
|
||||
("GraphicEvent.graphics", "stored graphic object"),
|
||||
("CueEvent.source", "live event"),
|
||||
("TempoSegment.start", "anchor target"),
|
||||
("TempoSegment.end", "anchor target"),
|
||||
];
|
||||
|
||||
/// Pin 1a's closed target vocabulary. A term outside it fails, and that is a
|
||||
/// *separate* assertion from ordering: an out-of-vocabulary term sorts
|
||||
/// perfectly well, so the canonical-form check cannot see it.
|
||||
const TARGET_VOCABULARY: &[&str] = &[
|
||||
"anchor target",
|
||||
"declared analysis layer",
|
||||
"declared instrument",
|
||||
"declared staff",
|
||||
"declared staff group",
|
||||
"declared time signature",
|
||||
"extant region",
|
||||
"extant tuplet",
|
||||
"live event",
|
||||
"live pitch",
|
||||
"stored graphic object",
|
||||
];
|
||||
|
||||
/// Item 10's opening sentence, pinned as the **complete** literal rather than a
|
||||
/// prefix, so that pin 3's retention of it is machine-observed. Whitespace is
|
||||
/// normalised on both sides before matching, because the `.tex` source is
|
||||
/// hard-wrapped and rewrapping is presentational.
|
||||
const ITEM_TEN_ANCHOR: &str = "\\item Except where the re-anchoring rules of \
|
||||
Chapter~\\ref{ch:semops} explicitly permit transient dangling states during \
|
||||
edits, every graph reference resolves to an extant object.";
|
||||
|
||||
fn repository_root() -> PathBuf {
|
||||
Path::new(env!("CARGO_MANIFEST_DIR")).join("../..")
|
||||
}
|
||||
|
||||
fn read(relative: &str) -> String {
|
||||
let path = repository_root().join(relative);
|
||||
fs::read_to_string(&path)
|
||||
.unwrap_or_else(|error| panic!("failed to read {}: {error}", path.display()))
|
||||
}
|
||||
|
||||
/// Collapse every run of whitespace to one space.
|
||||
fn normalise(text: &str) -> String {
|
||||
text.split_whitespace().collect::<Vec<_>>().join(" ")
|
||||
}
|
||||
|
||||
/// Sort a comma-separated target into pin 1a's canonical order.
|
||||
fn canonical_target(target: &str) -> String {
|
||||
let mut terms: Vec<&str> = target.split(',').map(str::trim).collect();
|
||||
terms.sort_unstable();
|
||||
terms.join(", ")
|
||||
}
|
||||
|
||||
/// Step 0. Validate the oracle before using it as one: a duplicate token would
|
||||
/// vanish when the expected side becomes a set, and an out-of-vocabulary target
|
||||
/// would be asserted and never observed.
|
||||
fn validated_oracle() -> BTreeSet<(String, String)> {
|
||||
let mut seen: BTreeMap<&str, usize> = BTreeMap::new();
|
||||
for (token, _) in INVARIANT_TEN_SURFACE {
|
||||
*seen.entry(token).or_default() += 1;
|
||||
}
|
||||
let repeated: Vec<&str> = seen
|
||||
.iter()
|
||||
.filter(|(_, count)| **count > 1)
|
||||
.map(|(token, _)| *token)
|
||||
.collect();
|
||||
assert!(
|
||||
repeated.is_empty(),
|
||||
"INVARIANT_TEN_SURFACE repeats {repeated:?}; a repeat collapses silently \
|
||||
into the expected set and would let both documents drop a class"
|
||||
);
|
||||
|
||||
for (token, target) in INVARIANT_TEN_SURFACE {
|
||||
for term in target.split(',').map(str::trim) {
|
||||
assert!(
|
||||
TARGET_VOCABULARY.contains(&term),
|
||||
"INVARIANT_TEN_SURFACE target {target:?} for {token} uses \
|
||||
{term:?}, which is outside pin 1a's vocabulary"
|
||||
);
|
||||
}
|
||||
assert_eq!(
|
||||
*target,
|
||||
canonical_target(target),
|
||||
"INVARIANT_TEN_SURFACE target for {token} is not in canonical order"
|
||||
);
|
||||
}
|
||||
|
||||
INVARIANT_TEN_SURFACE
|
||||
.iter()
|
||||
.map(|(token, target)| ((*token).to_owned(), (*target).to_owned()))
|
||||
.collect()
|
||||
}
|
||||
|
||||
/// Duplicate-token check on a raw extraction, plus the canonical-form checks.
|
||||
/// Run before the set comparison, which cannot see any of them.
|
||||
fn check_extraction(pairs: &[(String, String)], where_: &str) {
|
||||
let mut seen: BTreeMap<&str, usize> = BTreeMap::new();
|
||||
for (token, _) in pairs {
|
||||
*seen.entry(token.as_str()).or_default() += 1;
|
||||
}
|
||||
let repeated: Vec<&str> = seen
|
||||
.iter()
|
||||
.filter(|(_, count)| **count > 1)
|
||||
.map(|(token, _)| *token)
|
||||
.collect();
|
||||
assert!(
|
||||
repeated.is_empty(),
|
||||
"{where_} lists {repeated:?} more than once; set comparison cannot see a \
|
||||
duplicate, so it is checked here"
|
||||
);
|
||||
|
||||
for (token, target) in pairs {
|
||||
assert_eq!(
|
||||
*target,
|
||||
canonical_target(target),
|
||||
"{where_}: target for {token} is not in pin 1a's canonical order"
|
||||
);
|
||||
for term in target.split(',').map(str::trim) {
|
||||
assert!(
|
||||
TARGET_VOCABULARY.contains(&term),
|
||||
"{where_}: target for {token} uses {term:?}, outside pin 1a's \
|
||||
vocabulary. Ordering cannot catch this -- a bad term sorts fine"
|
||||
);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/// The `requirement` block that carries the graph invariants, normalised.
|
||||
///
|
||||
/// Slicing is mandatory, and stated here because it is not obvious: unsliced,
|
||||
/// the extractor would collect every `\texttt{}` in `core_spec.tex` and
|
||||
/// equality would fail on a flood of spurious pairs. The slice is what makes
|
||||
/// the guard *function*, not what gives it teeth.
|
||||
fn graph_invariants_block() -> String {
|
||||
let spec = normalise(&read("spec/core_spec.tex"));
|
||||
let label = r"\label{req:graph:score-graph-invariants}";
|
||||
let at = spec
|
||||
.find(label)
|
||||
.expect("core_spec.tex declares req:graph:score-graph-invariants");
|
||||
let start = spec[..at]
|
||||
.rfind(r"\begin{requirement}")
|
||||
.expect("the graph-invariants label sits inside a requirement block");
|
||||
let end = spec[start..]
|
||||
.find(r"\end{requirement}")
|
||||
.map(|offset| start + offset)
|
||||
.expect("that requirement block is closed");
|
||||
spec[start..end].to_owned()
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn specification_item_ten_names_exactly_the_derived_surface() {
|
||||
let expected = validated_oracle();
|
||||
let block = graph_invariants_block();
|
||||
|
||||
// The anchor is the complete opening sentence, not a prefix of it, so that
|
||||
// pin 3's retention of that sentence is machine-observed. It must occur
|
||||
// exactly once in the block, or the outer slice is ambiguous and nothing
|
||||
// else would notice.
|
||||
let anchor = normalise(ITEM_TEN_ANCHOR);
|
||||
let occurrences = block.matches(anchor.as_str()).count();
|
||||
assert_eq!(
|
||||
occurrences, 1,
|
||||
"item 10's opening sentence must occur exactly once inside \
|
||||
req:graph:score-graph-invariants; found {occurrences}"
|
||||
);
|
||||
|
||||
let outer_start = block.find(anchor.as_str()).expect("checked above");
|
||||
let outer_end = outer_start + item_ten_length(&block[outer_start..]);
|
||||
let outer = &block[outer_start..outer_end];
|
||||
|
||||
// Pin 3 forbids both of these inside item 10, and nothing else would catch
|
||||
// them: an accidental well-formed label is absorbed the moment pin 4's
|
||||
// count constants are remeasured. Recognition is whitespace-tolerant
|
||||
// because TeX accepts `\label {x}` and the repository's own parser does
|
||||
// not -- a guard shaped like that parser would inherit its blind spot.
|
||||
assert!(
|
||||
!contains_command(outer, "label"),
|
||||
"item 10 must contain no \\label: pin 3 adds no label and no \
|
||||
requirement block.\nSlice was:\n{outer}"
|
||||
);
|
||||
assert!(
|
||||
!contains_begin_requirement(outer),
|
||||
"item 10 must contain no requirement block.\nSlice was:\n{outer}"
|
||||
);
|
||||
|
||||
let inner_start = outer
|
||||
.find(r"\begin{itemize}")
|
||||
.map(|offset| offset + r"\begin{itemize}".len())
|
||||
.expect("item 10 carries its nested itemize");
|
||||
let inner_end = outer[inner_start..]
|
||||
.find(r"\end{itemize}")
|
||||
.map(|offset| inner_start + offset)
|
||||
.expect("that itemize is closed");
|
||||
let inner = &outer[inner_start..inner_end];
|
||||
|
||||
let pairs = extract_tex_pairs(inner);
|
||||
check_extraction(&pairs, "core_spec.tex item 10");
|
||||
let actual: BTreeSet<(String, String)> = pairs.into_iter().collect();
|
||||
assert_eq!(actual, expected);
|
||||
}
|
||||
|
||||
/// Item 10 runs from its opening sentence to the next `\item` **at the
|
||||
/// enumeration's own level**. Nested `itemize` environments carry `\item`s of
|
||||
/// their own, so the scan tracks depth; a naive "next `\item`" ends the slice
|
||||
/// inside the nested list and loses everything after it.
|
||||
fn item_ten_length(rest: &str) -> usize {
|
||||
let mut depth = 0usize;
|
||||
let mut cursor = 0usize;
|
||||
while cursor < rest.len() {
|
||||
let tail = &rest[cursor..];
|
||||
if tail.starts_with(r"\begin{itemize}") {
|
||||
depth += 1;
|
||||
cursor += r"\begin{itemize}".len();
|
||||
} else if tail.starts_with(r"\end{itemize}") {
|
||||
depth = depth.saturating_sub(1);
|
||||
cursor += r"\end{itemize}".len();
|
||||
} else if depth == 0 && cursor > 0 && tail.starts_with(r"\item ") {
|
||||
return cursor;
|
||||
} else {
|
||||
cursor += tail.chars().next().map_or(1, char::len_utf8);
|
||||
}
|
||||
}
|
||||
rest.len()
|
||||
}
|
||||
|
||||
/// Whitespace-tolerant `\command{` recognition.
|
||||
fn contains_command(text: &str, command: &str) -> bool {
|
||||
let needle = format!("\\{command}");
|
||||
let mut cursor = 0;
|
||||
while let Some(relative) = text[cursor..].find(&needle) {
|
||||
let after = cursor + relative + needle.len();
|
||||
if text[after..].trim_start().starts_with('{') || command.ends_with('}') {
|
||||
return true;
|
||||
}
|
||||
cursor = after;
|
||||
}
|
||||
false
|
||||
}
|
||||
|
||||
/// `\begin` followed by optional whitespace then `{requirement}`.
|
||||
fn contains_begin_requirement(text: &str) -> bool {
|
||||
let mut cursor = 0;
|
||||
while let Some(relative) = text[cursor..].find("\\begin") {
|
||||
let after = cursor + relative + "\\begin".len();
|
||||
if text[after..].trim_start().starts_with("{requirement}") {
|
||||
return true;
|
||||
}
|
||||
cursor = after;
|
||||
}
|
||||
false
|
||||
}
|
||||
|
||||
/// Per `\item`: the first `\texttt{}` argument is the token, the text between
|
||||
/// `---` and the terminating period is the target.
|
||||
fn extract_tex_pairs(inner: &str) -> Vec<(String, String)> {
|
||||
let mut pairs = Vec::new();
|
||||
for chunk in inner.split(r"\item ").skip(1) {
|
||||
let Some(open) = chunk.find(r"\texttt{") else {
|
||||
continue;
|
||||
};
|
||||
let token_start = open + r"\texttt{".len();
|
||||
let Some(close) = chunk[token_start..].find('}') else {
|
||||
continue;
|
||||
};
|
||||
let token = chunk[token_start..token_start + close].replace("\\_", "_");
|
||||
let rest = &chunk[token_start + close..];
|
||||
let Some(dash) = rest.find("---") else {
|
||||
continue;
|
||||
};
|
||||
let after_dash = &rest[dash + "---".len()..];
|
||||
let Some(period) = after_dash.find('.') else {
|
||||
continue;
|
||||
};
|
||||
pairs.push((token, after_dash[..period].trim().to_owned()));
|
||||
}
|
||||
pairs
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn implementation_doc_names_exactly_the_derived_surface() {
|
||||
let expected = validated_oracle();
|
||||
let source = read("crates/epiphany-core/src/invariants.rs");
|
||||
let start = source
|
||||
.find(" /// 10. Every graph reference resolves")
|
||||
.expect("invariant 10's doc comment is present");
|
||||
let end = source[start..]
|
||||
.find("CrossCuttingRefsResolve,")
|
||||
.map(|offset| start + offset)
|
||||
.expect("the CrossCuttingRefsResolve variant follows its doc comment");
|
||||
|
||||
let mut pairs = Vec::new();
|
||||
for line in source[start..end].lines() {
|
||||
let Some(rest) = line.trim_start().strip_prefix("/// ") else {
|
||||
continue;
|
||||
};
|
||||
let Some(rest) = rest.trim_start().strip_prefix("- ") else {
|
||||
continue;
|
||||
};
|
||||
let Some(token) = rest.split_whitespace().next() else {
|
||||
continue;
|
||||
};
|
||||
let Some(dash) = rest.find('\u{2014}') else {
|
||||
continue;
|
||||
};
|
||||
let after_dash = &rest[dash + '\u{2014}'.len_utf8()..];
|
||||
let Some(period) = after_dash.find('.') else {
|
||||
continue;
|
||||
};
|
||||
pairs.push((token.to_owned(), after_dash[..period].trim().to_owned()));
|
||||
}
|
||||
|
||||
check_extraction(&pairs, "invariants.rs invariant-10 doc block");
|
||||
let actual: BTreeSet<(String, String)> = pairs.into_iter().collect();
|
||||
assert_eq!(actual, expected);
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn aleatoric_reference_locality_states_both_referents_and_locality() {
|
||||
// Phrase presence, not exact comparison -- weaker than the two tests above,
|
||||
// and stated as such rather than presented as equivalent coverage. What it
|
||||
// buys: neither referent, nor the locality claim, nor the requirement's
|
||||
// normative force can silently leave.
|
||||
let spec = normalise(&read("spec/core_spec.tex"));
|
||||
let label = r"\label{req:time:aleatoric-reference-locality}";
|
||||
let at = spec
|
||||
.find(label)
|
||||
.expect("core_spec.tex declares req:time:aleatoric-reference-locality");
|
||||
let start = spec[..at]
|
||||
.rfind(r"\begin{requirement}")
|
||||
.expect("that label sits inside a requirement block");
|
||||
let end = spec[start..]
|
||||
.find(r"\end{requirement}")
|
||||
.map(|offset| start + offset)
|
||||
.expect("that requirement block is closed");
|
||||
let block = &spec[start..end];
|
||||
|
||||
for needle in ["ordering", "bounds", "same region", "\\MUST{}"] {
|
||||
assert!(
|
||||
block.contains(needle),
|
||||
"req:time:aleatoric-reference-locality must state {needle:?}; \
|
||||
block was:\n{block}"
|
||||
);
|
||||
}
|
||||
}
|
||||
|
|
@ -12,11 +12,16 @@ use std::path::{Path, PathBuf};
|
|||
// +1 for req:format:container-epoch (the format-epoch rung, pin 7:
|
||||
// spec/CONTRACT_FORMAT_EPOCH_MAJOR1.md) — the container major becomes an epoch,
|
||||
// and Chapter 8 states the classification and the epoch matrix normatively.
|
||||
const CORE_REQUIREMENT_COUNT: usize = 214;
|
||||
// +1 for req:time:aleatoric-reference-locality (P13-S26, pin 4:
|
||||
// spec/CONTRACT_P13S26_INVARIANT10_SURFACE.md) — an aleatoric region's ordering
|
||||
// and bounds references must name events of that same region. Measured at
|
||||
// execution, never predicted.
|
||||
const CORE_REQUIREMENT_COUNT: usize = 215;
|
||||
// +1 for req:textproj:manifest-schema-carried (G-minor, pins 8/11:
|
||||
// spec/PLAN_GMINOR_SCHEMA_MINOR.md); +1 for req:format:container-epoch (above).
|
||||
const SUITE_REQUIREMENT_COUNT: usize = 285;
|
||||
const SUITE_LABEL_COUNT: usize = 285;
|
||||
// spec/PLAN_GMINOR_SCHEMA_MINOR.md); +1 for req:format:container-epoch (above);
|
||||
// +1 for req:time:aleatoric-reference-locality (above).
|
||||
const SUITE_REQUIREMENT_COUNT: usize = 286;
|
||||
const SUITE_LABEL_COUNT: usize = 286;
|
||||
|
||||
/// The normative chapter-to-area assignment. Keeping this as data makes adding a
|
||||
/// requirement under the wrong chapter fail without encoding chapter names in
|
||||
|
|
@ -385,23 +390,6 @@ const DISCUSSED_NOT_CITED: &[(&str, &str)] = &[
|
|||
governs. Named in spec/PLAN_P13S1_LABELS.md as the finding that motivated \
|
||||
this checker.",
|
||||
),
|
||||
// --- P13-S26 REVIEW SCAFFOLDING (pre-execution) -------------------------
|
||||
//
|
||||
// The citation scan reads the filesystem, not git, so the contract at
|
||||
// spec/CONTRACT_P13S26_INVARIANT10_SURFACE.md is scanned like any other
|
||||
// repository text — tracked or not, staged or not. It names both labels
|
||||
// below, neither of which exists yet, which broke the mandated green
|
||||
// baseline for three review rounds before it was measured. Euphemism is not
|
||||
// the remedy — see this const's own doc comment. Authorized as prerequisite
|
||||
// review scaffolding, NOT as dispatch of P13-S26; no other pin work is
|
||||
// licensed by it.
|
||||
//
|
||||
// Deliberately says nothing about its own staging or tracking state: both
|
||||
// change at ratification, while pin 10 of that contract deletes this banner
|
||||
// only at execution, so any such claim would spend that interval false.
|
||||
//
|
||||
// If S26 is abandoned, or either label changes before the rung lands,
|
||||
// remove the corresponding row by hand.
|
||||
(
|
||||
"req:graph:aleatoric-reference-locality",
|
||||
"not defined in the restored tree; P13-S26's M6 mutation defines it only \
|
||||
|
|
@ -409,14 +397,6 @@ const DISCUSSED_NOT_CITED: &[(&str, &str)] = &[
|
|||
spec/CONTRACT_P13S26_INVARIANT10_SURFACE.md and recorded in \
|
||||
spec/EVIDENCE_P13S26_EXECUTION.md as M6's verbatim diagnostic. PERMANENT.",
|
||||
),
|
||||
(
|
||||
"req:time:aleatoric-reference-locality",
|
||||
"proposed by spec/CONTRACT_P13S26_INVARIANT10_SURFACE.md; the requirement \
|
||||
does not exist until that contract's pin 4 lands. TEMPORARY — pin 4 \
|
||||
REMOVES this row when it creates the requirement, because this row's own \
|
||||
claim (discussed, never cited) becomes false at that moment. A stale row \
|
||||
is inert, so nothing else will catch it; that contract's gate 12 does.",
|
||||
),
|
||||
];
|
||||
|
||||
fn requirement_strings(text: &str) -> BTreeSet<String> {
|
||||
|
|
|
|||
|
|
@ -1,11 +1,15 @@
|
|||
# Contract — P13-S26: invariant 10's reference surface, derived
|
||||
|
||||
**Status:** **RATIFIED 2026-08-11, on the authority of the repository owner**,
|
||||
after the independent whole-artifact passes recorded above §0 — the last
|
||||
returning zero findings. **DISPATCHED 2026-08-11.** Amendment 1 ratified;
|
||||
execution resumes. Which passes closed and what each found are those records;
|
||||
this line does not restate them, and states no count of them, per the rule
|
||||
this contract adopted after its own tallies went stale twice.
|
||||
STATUS: LANDED by this commit.
|
||||
|
||||
**Lifecycle record.** RATIFIED 2026-08-11 on the authority of the repository
|
||||
owner, after the independent whole-artifact passes recorded below — the last
|
||||
returning zero findings. DISPATCHED 2026-08-11; amendment 1 ratified at
|
||||
`f9170b0`, amendment 2 at `86bf7c6`. Which passes closed and what each found
|
||||
are those records; this does not restate them, and states no count of them, per
|
||||
the rule this contract adopted after its own tallies went stale twice. **No hash
|
||||
of the landing commit appears above**: a commit cannot carry its own id, so if
|
||||
one is wanted it arrives by a later administrative amendment.
|
||||
|
||||
**THE PINS ARE FROZEN. They may be executed, not edited.** A defect found during
|
||||
execution is **reported, not patched in place** — if it needs a pin change, that
|
||||
|
|
@ -36,6 +40,12 @@ same round. This is a review method, not another execution gate for S26.
|
|||
|
||||
---
|
||||
|
||||
> **DATED HISTORICAL RECORD — every review block below, through to §0, is an
|
||||
> account of what a pass found on the date it ran. None of it states current
|
||||
> state. The rung landed; the pins were executed, not edited.**
|
||||
|
||||
---
|
||||
|
||||
### RATIFICATION CHECK 2 — independent, whole-artifact. **NO-GO: one completeness correction.** ACCEPTED.
|
||||
|
||||
1. **[P1] S30's "exhaustive" inventory covered only the opening delimiter.**
|
||||
|
|
@ -1641,14 +1651,17 @@ that does not exist.
|
|||
|
||||
## §6. AMENDMENT 1 — PIN 3, PIN 6 AND PIN 11, PRE-FIRST-EDIT
|
||||
|
||||
STATUS: RATIFIED. Pins 3, 6 and 11 amended. Execution resumes.
|
||||
STATUS: LANDED by this commit.
|
||||
|
||||
Ratified 2026-08-11 on the authority of the repository owner, review round 5
|
||||
returning zero findings. The amended pins are executed, not edited; a further
|
||||
defect is its own amendment with its own review round.
|
||||
|
||||
**DATED RECORD — the hold this amendment describes ENDED at `f9170b0`.** What
|
||||
follows is an account of 2026-08-11, not a statement of current state.
|
||||
**DATED HISTORICAL RECORD — this amendment is ratified, its pin changes are
|
||||
executed, and the hold it describes ENDED at `f9170b0`.** Everything in §6,
|
||||
including its revision records, its lifecycle statements and §6.8's disposition,
|
||||
is an account of what was found and decided on 2026-08-11. None of it states
|
||||
current state.
|
||||
|
||||
On that date the contract was dispatched for implementation, execution began,
|
||||
and it stopped on reaching pin 3; the top status paragraph still read NOT YET
|
||||
|
|
|
|||
File diff suppressed because it is too large
Load Diff
File diff suppressed because one or more lines are too long
Binary file not shown.
|
|
@ -2758,6 +2758,18 @@ encoding admits both as cases.
|
|||
unordered.
|
||||
\end{requirement}
|
||||
|
||||
\begin{requirement}
|
||||
\label{req:time:aleatoric-reference-locality}
|
||||
Every event referenced by an aleatoric region's \texttt{ordering}
|
||||
DAG, and every event used as a key in its \texttt{bounds} map,
|
||||
\MUST{} be an event of that same region. Naming an event that does
|
||||
not exist is a dangling reference, governed by graph
|
||||
invariant~10; naming an event that exists in a \emph{different}
|
||||
region is a distinct defect, and this requirement is what forbids
|
||||
it. Neither the ordering DAG nor the bounds map may reach outside
|
||||
the region whose time model declares them.
|
||||
\end{requirement}
|
||||
|
||||
\begin{rationale}
|
||||
A DAG with optional interval bounds expresses every aleatoric form
|
||||
the project intends to support: unordered collections (empty DAG),
|
||||
|
|
@ -6572,10 +6584,59 @@ The score graph maintains a set of structural invariants. Implementations
|
|||
\item Every \texttt{TimeAnchor}'s \texttt{AnchorOffset} variant
|
||||
agrees with the time model of the target object's enclosing
|
||||
region (Section~\ref{sec:time:anchors}).
|
||||
\item Every cross-cutting structure's references resolve to extant
|
||||
\item Except where the re-anchoring rules of
|
||||
Chapter~\ref{ch:semops} explicitly permit transient dangling
|
||||
states during edits, every graph reference resolves to an extant
|
||||
object. Every cross-cutting structure's references resolve to extant
|
||||
objects in the graph, except where explicit re-anchoring rules
|
||||
permit transient dangling states during edits (see
|
||||
Chapter~\ref{ch:semops}).
|
||||
Chapter~\ref{ch:semops}). Tempo-map conditions that are not
|
||||
reference resolution --- segment ordering and non-overlap --- are
|
||||
governed by Requirement~\ref{req:time:tempo-segment-order}, not by
|
||||
this invariant. The complete reference surface is:
|
||||
\begin{itemize}
|
||||
\item \texttt{Slur.start\_event} --- live event.
|
||||
\item \texttt{Slur.end\_event} --- live event.
|
||||
\item \texttt{Tie.start\_event} --- live event.
|
||||
\item \texttt{Tie.end\_event} --- live event.
|
||||
\item \texttt{Beam.events} --- live event.
|
||||
\item \texttt{SubBeam.events} --- live event.
|
||||
\item \texttt{Tuplet.members} --- live event.
|
||||
\item \texttt{Tuplet.parent} --- extant tuplet.
|
||||
\item \texttt{Spanner.staves} --- declared staff.
|
||||
\item \texttt{Spanner.start} --- anchor target.
|
||||
\item \texttt{Spanner.end} --- anchor target.
|
||||
\item \texttt{Marker.anchor} --- anchor target.
|
||||
\item \texttt{RepeatStructure.start} --- anchor target.
|
||||
\item \texttt{RepeatStructure.end} --- anchor target.
|
||||
\item \texttt{RepeatStructure.kind} --- anchor target.
|
||||
\item \texttt{RepeatStructure.voltas} --- anchor target.
|
||||
\item \texttt{ChordSymbol.anchor} --- anchor target.
|
||||
\item \texttt{AnalyticalAnnotation.anchor} --- anchor target, extant region, live event.
|
||||
\item \texttt{AnalyticalAnnotation.layer} --- declared analysis layer.
|
||||
\item \texttt{Comment.anchor} --- anchor target, extant region, live event.
|
||||
\item \texttt{GraphicGesture.objects} --- stored graphic object.
|
||||
\item \texttt{GraphicGesture.anchoring} --- anchor target, declared staff, live event.
|
||||
\item \texttt{LyricLine.events} --- live event.
|
||||
\item \texttt{Staff.instrument} --- declared instrument.
|
||||
\item \texttt{StaffInstance.instrument\_override} --- declared instrument.
|
||||
\item \texttt{Staff.group} --- declared staff group.
|
||||
\item \texttt{StaffGroup.members} --- declared staff.
|
||||
\item \texttt{PartDefinition.staves} --- declared staff.
|
||||
\item \texttt{ViewDefinition.active\_layers} --- declared analysis layer.
|
||||
\item \texttt{MetricTimeModel.meters} --- declared time signature.
|
||||
\item \texttt{StaffBasedContent.default\_metric\_grid} --- declared time signature.
|
||||
\item \texttt{Measure.time\_signature} --- declared time signature.
|
||||
\item \texttt{StaffInstance.local\_metric\_grid} --- declared time signature.
|
||||
\item \texttt{NotatedComponent.tuplet} --- extant tuplet.
|
||||
\item \texttt{IndeterminacyHints.alternatives} --- live event.
|
||||
\item \texttt{TrajectoryEvent.start} --- live pitch.
|
||||
\item \texttt{TrajectoryEvent.end} --- live pitch.
|
||||
\item \texttt{GraphicEvent.graphics} --- stored graphic object.
|
||||
\item \texttt{CueEvent.source} --- live event.
|
||||
\item \texttt{TempoSegment.start} --- anchor target.
|
||||
\item \texttt{TempoSegment.end} --- anchor target.
|
||||
\end{itemize}
|
||||
\item Every identifier in the graph is unique within its kind.
|
||||
Identifiers reserved for system-derived objects (notably
|
||||
\texttt{VoiceId}s of system-promoted voices) \MUST{} be derived
|
||||
|
|
@ -16944,6 +17005,30 @@ layouts they own versus inherit:
|
|||
invariant~10's reference-resolution concern, not a disagreement. The
|
||||
enumeration count moves from 20 to 21 accordingly.
|
||||
\\
|
||||
\today & \sectionsc{Graph Invariants}, \sectionsc{Aleatoric Time} &
|
||||
\textbf{P13-S26: graph invariant~10 names its complete reference surface,
|
||||
and aleatoric reference locality becomes a labelled requirement.} Invariant~10
|
||||
previously read only that ``every cross-cutting structure's references resolve
|
||||
to extant objects'', naming no individual class --- while the checker enforces
|
||||
a surface spanning cross-cutting structures, structural top-level references,
|
||||
meter and time-signature references at every level a \texttt{MeterChange}
|
||||
appears, an attachment-internal reference, event-internal references and the
|
||||
tempo map's segment anchors. That sentence is also scoped to cross-cutting
|
||||
structures alone, a defined term narrower than the surface beneath it, so the
|
||||
item now opens with a universal subordinated to the re-anchoring rules that
|
||||
explicitly permit transient dangling, and retains the original sentence
|
||||
unchanged beneath it. The surface is enumerated, derived from the checker
|
||||
rather than copied from either prior summary, since the normative enumeration
|
||||
and the implementation's own doc comment were incomplete in different places
|
||||
and neither could be repaired from the other. Tempo-map ordering and
|
||||
non-overlap are named as \emph{not} this invariant's, being governed by
|
||||
Requirement~\ref{req:time:tempo-segment-order}. Separately,
|
||||
\sectionsc{Aleatoric Time} gains
|
||||
Requirement~\ref{req:time:aleatoric-reference-locality}: an aleatoric
|
||||
region's ordering and bounds references \MUST{} name events of that same
|
||||
region --- a locality rule the checker has always enforced and no requirement
|
||||
stated.
|
||||
\\
|
||||
\bottomrule
|
||||
\end{longtable}
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue