315 lines
13 KiB
Rust
315 lines
13 KiB
Rust
//! A scoped guard on `spec/binary_format.tex`'s Revision History chapter
|
|
//! (Packet B of `spec/CONTRACT_GENESIS_G3A_UNDO_REPAIR.md`, pins B5/B6),
|
|
//! filed against P13-S17: the chapter once ran genesis tranche G2a straight
|
|
//! to G-minor to G3a, omitting G2b entirely — including the accept-set
|
|
//! raise `OperationEnvelopeBlock` 2 -> 3 that G2b performed, which reached
|
|
//! the normative tables but never the history.
|
|
//!
|
|
//! Two constraints from pin B6 pull against each other and both must hold:
|
|
//!
|
|
//! * Bare name-presence is not enough. `"G2b"` already occurs inside the
|
|
//! chapter in prose — the G3a row observes that the accept-set "stays at
|
|
//! 3 where genesis tranche G2b left it" — so a guard that only checked
|
|
//! for the substring `"G2b"` would stay green even with the G2b row
|
|
//! deleted. The guard below requires a *principal marker*: the rung name
|
|
//! immediately preceded by the row's `---` separator (e.g.
|
|
//! `--- Genesis tranche G2b`), which a prose mention where the separator
|
|
//! *follows* the name (as in "genesis tranche G1 --- landed at",
|
|
//! `binary_format.tex:3603`) cannot satisfy.
|
|
//! * No document version number appears anywhere in this file — not in the
|
|
//! assertions and not in this comment, which is why none is quoted here
|
|
//! even as an example. Encoding one would pin a number a future chronology
|
|
//! correction would have to move, reintroducing the stale hand-maintained
|
|
//! parallel list this project keeps rediscovering. Assert rung identity and
|
|
//! ordering; never the number attached to a rung.
|
|
//!
|
|
//! **G1 is deliberately unguarded.** `binary_format.tex:3603` states
|
|
//! outright that genesis tranche G1 has no standalone Revision History row
|
|
//! — it is recorded retroactively *inside* the G2a row ("genesis tranche G1
|
|
//! --- landed at `3b09595` with no matching entry here"). Demanding a
|
|
//! principal marker for G1 would make this guard born red against a
|
|
//! document that pin B2 leaves correct, so only G2a, G-minor, G2b, G3a, and
|
|
//! G3b get principal-marker assertions here. Do not "fix" this by adding a
|
|
//! sixth marker; that rediscovers the contradiction pin B6 already resolved.
|
|
//!
|
|
//! **G3b** (`spec/CONTRACT_GENESIS_G3B_MEASURE.md` pin 14) extends this same
|
|
//! guard to its own Revision History row, closing the genesis ladder: the
|
|
//! contract's own M71 deletes the G3b row, observes this guard fail, and
|
|
//! restores it by hand.
|
|
//!
|
|
//! **P13-S21** extends the file past rung identity to one vocabulary gap of
|
|
//! the same shape: `PreconditionFailureReason` 14 and 15 entered at Push 4a
|
|
//! and reached this document at neither of the two places that owe them —
|
|
//! not the bounded enumeration that assigns discriminants, and not Push 4a's
|
|
//! own history row. See
|
|
//! `precondition_failure_reasons_14_and_15_are_documented` below.
|
|
|
|
use std::fs;
|
|
use std::path::Path;
|
|
|
|
/// The rung name immediately preceded by the row's `---` separator, in the
|
|
/// exact spelling each row uses (G-minor is never prefixed "Genesis
|
|
/// tranche" in the document; the other four are).
|
|
const PRINCIPAL_MARKERS: [(&str, &str); 5] = [
|
|
("G2a", "--- Genesis tranche G2a"),
|
|
("G-minor", "--- G-minor"),
|
|
("G2b", "--- Genesis tranche G2b"),
|
|
("G3a", "--- Genesis tranche G3a"),
|
|
("G3b", "--- Genesis tranche G3b"),
|
|
];
|
|
|
|
fn binary_format_source() -> String {
|
|
let path = Path::new(env!("CARGO_MANIFEST_DIR")).join("../../spec/binary_format.tex");
|
|
fs::read_to_string(&path).unwrap_or_else(|error| {
|
|
panic!("failed to read {}: {error}", path.display());
|
|
})
|
|
}
|
|
|
|
/// Collapse whitespace runs to a single space so a future rewrap of a row's
|
|
/// LaTeX source lines cannot silently break a substring search that this
|
|
/// guard depends on. Byte offsets after this pass are relative to the
|
|
/// normalized string, which is all the ordering assertion needs — nothing
|
|
/// here reports a source line number.
|
|
fn normalize_whitespace(text: &str) -> String {
|
|
let mut out = String::with_capacity(text.len());
|
|
let mut last_was_space = true;
|
|
for ch in text.chars() {
|
|
if ch.is_whitespace() {
|
|
if !last_was_space {
|
|
out.push(' ');
|
|
last_was_space = true;
|
|
}
|
|
} else {
|
|
out.push(ch);
|
|
last_was_space = false;
|
|
}
|
|
}
|
|
out
|
|
}
|
|
|
|
/// Every non-overlapping byte offset at which `needle` occurs in `haystack`.
|
|
fn find_all(haystack: &str, needle: &str) -> Vec<usize> {
|
|
let mut offsets = Vec::new();
|
|
let mut cursor = 0;
|
|
while let Some(relative) = haystack[cursor..].find(needle) {
|
|
let offset = cursor + relative;
|
|
offsets.push(offset);
|
|
cursor = offset + needle.len();
|
|
}
|
|
offsets
|
|
}
|
|
|
|
/// Slice the normalized document down to the Revision History chapter: from
|
|
/// its own `\chapter{Revision History}` heading to the next `\chapter{`
|
|
/// (there is none after it today, so this also tolerates a future chapter
|
|
/// being appended afterward) or the end of the document.
|
|
fn revision_history_slice(normalized: &str) -> &str {
|
|
const CHAPTER: &str = r"\chapter{Revision History}";
|
|
const NEXT_CHAPTER: &str = r"\chapter{";
|
|
|
|
let start = normalized
|
|
.find(CHAPTER)
|
|
.expect("binary_format.tex has no \\chapter{Revision History}");
|
|
let after = start + CHAPTER.len();
|
|
let end = normalized[after..]
|
|
.find(NEXT_CHAPTER)
|
|
.map(|relative| after + relative)
|
|
.unwrap_or(normalized.len());
|
|
&normalized[start..end]
|
|
}
|
|
|
|
/// Each rung's principal marker exactly once in the slice. A prose-only
|
|
/// mention (bare name, no preceding `---`) does not count, and neither
|
|
/// does a duplicated row.
|
|
#[test]
|
|
fn revision_history_has_exactly_one_principal_marker_per_rung() {
|
|
let source = binary_format_source();
|
|
let normalized = normalize_whitespace(&source);
|
|
let slice = revision_history_slice(&normalized);
|
|
|
|
for (rung, marker) in PRINCIPAL_MARKERS {
|
|
let offsets = find_all(slice, marker);
|
|
assert_eq!(
|
|
offsets.len(),
|
|
1,
|
|
"expected exactly one principal marker {marker:?} for rung {rung} in the \
|
|
Revision History chapter, found {} (offsets {offsets:?})",
|
|
offsets.len()
|
|
);
|
|
}
|
|
}
|
|
|
|
/// The five marked rungs appear in ladder order: G1 -> G2a -> G-minor ->
|
|
/// G2b -> G3a -> G3b. G1 has no marker of its own (see the module comment),
|
|
/// so this checks the remaining five.
|
|
#[test]
|
|
fn revision_history_rungs_are_strictly_ordered() {
|
|
let source = binary_format_source();
|
|
let normalized = normalize_whitespace(&source);
|
|
let slice = revision_history_slice(&normalized);
|
|
|
|
let offsets: Vec<(&str, usize)> = PRINCIPAL_MARKERS
|
|
.iter()
|
|
.map(|(rung, marker)| {
|
|
let found = find_all(slice, marker);
|
|
assert_eq!(
|
|
found.len(),
|
|
1,
|
|
"expected exactly one principal marker {marker:?} for rung {rung}, found \
|
|
{found:?}"
|
|
);
|
|
(*rung, found[0])
|
|
})
|
|
.collect();
|
|
|
|
for window in offsets.windows(2) {
|
|
let (earlier_rung, earlier_offset) = window[0];
|
|
let (later_rung, later_offset) = window[1];
|
|
assert!(
|
|
earlier_offset < later_offset,
|
|
"expected {earlier_rung} (offset {earlier_offset}) to precede {later_rung} \
|
|
(offset {later_offset}) in the Revision History chapter; ladder order is \
|
|
G2a < G-minor < G2b < G3a < G3b"
|
|
);
|
|
}
|
|
}
|
|
|
|
/// The G2b row states what G2b actually did (pin B3), and the search is
|
|
/// bounded to the G2b row's own segment — from its principal marker to the
|
|
/// next principal marker (or the slice end) — so that G3a's row, which also
|
|
/// names `OperationEnvelopeBlock` 3 and mentions G2b in prose, cannot
|
|
/// satisfy this after the G2b row itself is deleted. Unbounded searching is
|
|
/// exactly the hole P13-S17 was filed over.
|
|
#[test]
|
|
fn revision_history_g2b_row_states_what_g2b_did() {
|
|
let source = binary_format_source();
|
|
let normalized = normalize_whitespace(&source);
|
|
let slice = revision_history_slice(&normalized);
|
|
|
|
const G2B_MARKER: &str = "--- Genesis tranche G2b";
|
|
let g2b_offsets = find_all(slice, G2B_MARKER);
|
|
assert_eq!(
|
|
g2b_offsets.len(),
|
|
1,
|
|
"expected exactly one G2b principal marker, found {g2b_offsets:?}"
|
|
);
|
|
let g2b_start = g2b_offsets[0];
|
|
let after_g2b = g2b_start + G2B_MARKER.len();
|
|
|
|
let next_marker_offset = PRINCIPAL_MARKERS
|
|
.iter()
|
|
.filter_map(|(_, marker)| {
|
|
find_all(&slice[after_g2b..], marker)
|
|
.first()
|
|
.map(|relative| after_g2b + relative)
|
|
})
|
|
.min()
|
|
.unwrap_or(slice.len());
|
|
|
|
let row_segment = &slice[g2b_start..next_marker_offset];
|
|
|
|
assert!(
|
|
row_segment.contains("SetTuningContext"),
|
|
"G2b row segment does not name SetTuningContext: {row_segment:?}"
|
|
);
|
|
assert!(
|
|
row_segment.contains(r"\tablenums{34}"),
|
|
"G2b row segment does not carry discriminant 34: {row_segment:?}"
|
|
);
|
|
assert!(
|
|
row_segment.contains("TuningContextSettings"),
|
|
"G2b row segment does not name the TuningContextSettings payload subset: \
|
|
{row_segment:?}"
|
|
);
|
|
assert!(
|
|
row_segment.contains("OperationEnvelopeBlock")
|
|
&& row_segment.contains(r"\tablenums{2}~$\rightarrow$~\tablenums{3}"),
|
|
"G2b row segment does not record the OperationEnvelopeBlock accept-set raise \
|
|
2 -> 3: {row_segment:?}"
|
|
);
|
|
}
|
|
|
|
/// Slice one `longtable` row: from `marker` to the `\\` that terminates the
|
|
/// row. Rows in this document carry no internal `\\`, so the first
|
|
/// terminator after the marker ends that row and nothing else.
|
|
fn row_segment<'a>(haystack: &'a str, marker: &str) -> &'a str {
|
|
let offsets = find_all(haystack, marker);
|
|
assert_eq!(
|
|
offsets.len(),
|
|
1,
|
|
"expected exactly one occurrence of the row marker {marker:?}, found {} \
|
|
(offsets {offsets:?})",
|
|
offsets.len()
|
|
);
|
|
let start = offsets[0];
|
|
let end = haystack[start..]
|
|
.find(r"\\")
|
|
.map(|relative| start + relative)
|
|
.unwrap_or(haystack.len());
|
|
&haystack[start..end]
|
|
}
|
|
|
|
/// `PreconditionFailureReason` 14 (`AcousticRealizationPinned`) and 15
|
|
/// (`TranspositionOutOfRange`) entered the vocabulary at Push 4a — the
|
|
/// Operation Catalog documented both at its own 0.8.0, and `effect.rs` has
|
|
/// carried both ever since — but this document named neither anywhere, its
|
|
/// bounded enumeration running 13 straight to G3b's 16. That is P13-S21, and
|
|
/// it is why P13-S20's decoder could stop at 13 unchallenged: an implementer
|
|
/// reading only the wire specification would have built exactly that decoder
|
|
/// and been right.
|
|
///
|
|
/// **Both sites are checked, each bounded to its own row**, because either
|
|
/// alone is satisfiable by the wrong thing. The G3b history row and the
|
|
/// bounded enumeration both discuss `PreconditionFailureReason` at length, so
|
|
/// an unbounded search for these names would go green the moment any row
|
|
/// mentioned them — the same hole P13-S17 was filed over, one vocabulary
|
|
/// down. No document version number appears here either; the Push 4a row is
|
|
/// located by its version-free `--- Transpose algebra (Push~4a)` separator
|
|
/// form, for the reason the module comment gives.
|
|
///
|
|
/// The enumeration is asserted as a **discriminant/name adjacency**, since it
|
|
/// is the normative assignment and must be exact. The history row is asserted
|
|
/// by name and discriminant presence within its own bounded segment: it is
|
|
/// prose, its wording may legitimately be rewritten, and the bounding is what
|
|
/// makes presence load-bearing there.
|
|
#[test]
|
|
fn precondition_failure_reasons_14_and_15_are_documented() {
|
|
let source = binary_format_source();
|
|
let normalized = normalize_whitespace(&source);
|
|
|
|
let enumeration = row_segment(
|
|
&normalized,
|
|
r"\texttt{Precondition\allowbreak FailureReason} &",
|
|
);
|
|
for pairing in [
|
|
r"\tablenums{14} AcousticRealizationPinned",
|
|
r"\tablenums{15} TranspositionOutOfRange",
|
|
] {
|
|
assert!(
|
|
enumeration.contains(pairing),
|
|
"the bounded PreconditionFailureReason enumeration does not assign \
|
|
{pairing:?}; it is the normative discriminant assignment and the \
|
|
pairing must be exact: {enumeration:?}"
|
|
);
|
|
}
|
|
|
|
let push4a = row_segment(
|
|
revision_history_slice(&normalized),
|
|
"--- Transpose algebra (Push~4a)",
|
|
);
|
|
for owed in [
|
|
"AcousticRealizationPinned",
|
|
"TranspositionOutOfRange",
|
|
r"\tablenums{14}",
|
|
r"\tablenums{15}",
|
|
] {
|
|
assert!(
|
|
push4a.contains(owed),
|
|
"Push 4a's own Revision History row does not record {owed:?}. Both \
|
|
reasons were appended in Push 4a's epoch alongside OperationKind 30, \
|
|
and a row that records only the kind leaves the append unattributable: \
|
|
{push4a:?}"
|
|
);
|
|
}
|
|
}
|