diff --git a/crates/epiphany-testkit/DECISIONS.md b/crates/epiphany-testkit/DECISIONS.md index 0829d5d..fc6e6bb 100644 --- a/crates/epiphany-testkit/DECISIONS.md +++ b/crates/epiphany-testkit/DECISIONS.md @@ -261,3 +261,59 @@ the catalog's own threshold-tuning open question anticipated this). (Minimal/Standard) are Chapter 9 conformance tiers. The companion carries the same caution; the harness resolves corpus entries by `name` string only and never reads the corpus tier. + +## The Text Projection grammar checker (`tests/text_projection_grammar.rs`) + +Text Projection 0.3.0 claimed a "machine-checked" grammar. It was checked by a +throwaway script, so the claim was **true of one run and of nothing durable**. +This test file is the durable form; 0.4.0 retracts the earlier claim in its own +revision history. It is the same evidence gap the P2–P4 decode work kept +finding: a green gate proves nothing about coverage until the harness states its +own reach. + +Six tests, and every one was **mutation-verified** — the mutation was applied to +the `.tex`, the anchor asserted present before substitution (a `str.replace` +that matches nothing looks exactly like a passing test), and the named test +observed to fail: + +| Mutation | Killed by | +|---|---| +| delete the `transpose-interval` production | `the_kind_productions_are_the_operation_vocabulary` | +| reference an undefined nonterminal | `every_nonterminal_is_defined_and_reachable` | +| let `unescaped` admit U+005C (the 0.3.0 bug) | `the_escape_grammar_agrees_with_the_escape_requirement` | +| drop the `derived-ordering` citations | `the_derived_ordering_requirement_is_cited_where_it_applies` | +| spell the escape introducer `"\\"` | `the_escape_grammar_agrees_with_the_escape_requirement` | +| drop the `\t` escape alternative | `the_escape_grammar_agrees_with_the_escape_requirement` | +| restore `Ligatures={TeX}` on the mono font | `the_mono_font_does_not_substitute_glyphs_in_the_grammar` | + +**The vocabularies are derived, never transcribed.** The 31 operation-kind +productions come from `OperationKindTag::PAYLOAD_FREE` plus `Registered`, mapped +to Catalog section names through an **exhaustive `match`** — so a kind added to +the enum and not to the grammar fails to compile, then fails the test. The chunk +productions come from `ChunkKind::from_discriminant`. This is the +`operation_kind_tag_vocabulary!` lesson applied to prose: a hand-maintained list +parallel to an enum is a latent false lock. + +**Every locator finds its production by name, not by column.** Writing the +checker exposed four bugs *in the checker*, three of them of this kind: a +column-anchored needle (`"projection ::="`) that a reflow broke — a checker +that cannot find the grammar silently checks nothing; a `defined()` that missed +three productions whose left-hand side sat on the line above their `::=`, which +would have **hidden** undefined nonterminals; and a per-line `<...>` stripper +that leaked `0022` and `005` out of multi-line prose spans, where they read as +nonterminals. Nonterminal tokens must now begin `[a-z]`, per `symbol` itself. + +**Two rendering rules are load-bearing, not cosmetic.** A document that +specifies a text syntax must not misprint that syntax. + +- The escape introducer and the string delimiter are written as **codepoints** + (`U+005C`, `U+0022`). A quoted terminal `"\\"` reads as *two* backslashes, + making every escape three characters where the requirement says two. This is + the audited 0.3.0 defect in a second disguise; it was written, caught by + review, and is now asserted against. +- The mono font must not enable **TeX ligatures**. `tlig` rewrites `"` as a + right curly quote and `--` as an en dash, so `string ::= '"' schar* '"'` + rendered as `’”’ schar* ’”’`. `core_spec.tex` already omitted `Ligatures={TeX}` + from its `\setmonofont`, which makes this the house convention rather than a + new one; the three companions that still enable it have no listing content the + feature would touch. diff --git a/crates/epiphany-testkit/tests/text_projection_grammar.rs b/crates/epiphany-testkit/tests/text_projection_grammar.rs new file mode 100644 index 0000000..6407daf --- /dev/null +++ b/crates/epiphany-testkit/tests/text_projection_grammar.rs @@ -0,0 +1,444 @@ +//! A committed completeness gate on the Text Projection companion's grammar. +//! +//! Version 0.3.0 claimed a "machine-checked" grammar. It was checked, once, by a +//! script that was never committed — true of that run and of nothing durable. +//! This is the durable form, and it is exactly the class of evidence P2–P4 +//! established: a claim about coverage is a lock, and an uncommitted check is not +//! one. +//! +//! What it enforces: +//! +//! 1. Every nonterminal the grammar references is defined, and every nonterminal +//! it defines is reachable from `projection`. +//! 2. The `kind` alternatives are **exactly** the operation vocabulary, *derived* +//! from `OperationKindTag` rather than transcribed. Adding a tag without +//! adding its production fails here, and the `match` below fails to compile +//! without a name for it — the same two-layer guarantee +//! `operation_kind_tag_vocabulary!` gives the decoder. +//! 3. The `chunk-kind` alternatives are exactly the `ChunkKind` vocabulary. +//! 4. The escape rule excludes the four codepoints +//! `req:textproj:string-escapes` requires a writer to escape — the +//! contradiction that 0.4.0 fixed. + +use std::collections::{BTreeSet, VecDeque}; + +use epiphany_bundle::ChunkKind; +use epiphany_ops::OperationKindTag; + +const SPEC: &str = include_str!("../../../spec/text_projection.tex"); + +/// The grammar block: from the `projection` production to the end of its listing. +/// +/// Located by name, never by column. The 0.4.0 reflow of the production headers +/// broke a column-anchored needle, and a checker that cannot find the grammar +/// silently checks nothing. +fn grammar() -> &'static str { + let start = SPEC + .lines() + .scan(0usize, |acc, l| { + let here = *acc; + *acc += l.len() + 1; + Some((here, l)) + }) + .find(|(_, l)| { + l.split_once("::=") + .is_some_and(|(lhs, _)| lhs.trim() == "projection") + }) + .map(|(at, _)| at) + .expect("the grammar block begins with the `projection` production"); + let end = SPEC[start..] + .find("\\end{lstlisting}") + .expect("the grammar block is a listing"); + &SPEC[start..start + end] +} + +/// Strips `;` line comments, then removes `<...>` prose spans, which may run +/// across lines. A per-line stripper leaks the second line's characters, and the +/// leaked fragments look like nonterminals. +fn uncommented(g: &str) -> String { + let no_comments: String = g + .lines() + .map(|l| l.split(';').next().unwrap_or("")) + .collect::>() + .join("\n"); + let mut out = String::new(); + let mut depth = 0usize; + for c in no_comments.chars() { + match c { + '<' => depth += 1, + '>' if depth > 0 => depth -= 1, + '\n' if depth > 0 => out.push('\n'), + _ if depth == 0 => out.push(c), + _ => {} + } + } + out +} + +fn is_name_char(c: char) -> bool { + c.is_ascii_lowercase() || c.is_ascii_digit() || c == '-' +} + +/// The left-hand side of every production. +fn defined(g: &str) -> BTreeSet { + uncommented(g) + .lines() + .filter_map(|l| { + let (lhs, _) = l.split_once("::=")?; + let name = lhs.trim(); + (!name.is_empty() && name.chars().all(is_name_char)).then(|| name.to_string()) + }) + .collect() +} + +/// Removes quoted terminals, angle-bracket prose, and character classes, leaving +/// only nonterminal references. +fn strip_terminals(line: &str) -> String { + let mut out = String::new(); + let mut chars = line.chars().peekable(); + while let Some(c) = chars.next() { + match c { + '"' => { + for d in chars.by_ref() { + if d == '"' { + break; + } + } + } + '\'' => { + for d in chars.by_ref() { + if d == '\'' { + break; + } + } + } + '[' => { + for d in chars.by_ref() { + if d == ']' { + break; + } + } + } + _ => out.push(c), + } + } + out +} + +/// Every nonterminal referenced on a right-hand side, per production. +fn references(g: &str) -> Vec<(String, BTreeSet)> { + let text = uncommented(g); + // A production may continue onto `|` continuation lines, which have no `::=`. + let mut out: Vec<(String, BTreeSet)> = Vec::new(); + for line in text.lines() { + let (lhs, rhs) = match line.split_once("::=") { + Some((l, r)) if l.trim().chars().all(is_name_char) && !l.trim().is_empty() => { + out.push((l.trim().to_string(), BTreeSet::new())); + (l.trim().to_string(), r) + } + _ => match out.last() { + Some((name, _)) => (name.clone(), line), + None => continue, + }, + }; + let _ = lhs; + let bare = strip_terminals(rhs); + let mut token = String::new(); + let entry = &mut out.last_mut().expect("a production is open").1; + for c in bare.chars().chain(std::iter::once(' ')) { + if is_name_char(c) { + token.push(c); + } else { + // A nonterminal is `[a-z] [a-z0-9-]*`, so a token that does not + // begin with a letter is not one. Without this, the `U+0022` in + // the escape production reads as a nonterminal named `0022`. + if token.starts_with(|c: char| c.is_ascii_lowercase()) { + entry.insert(std::mem::take(&mut token)); + } + token.clear(); + } + } + } + out +} + +#[test] +fn every_nonterminal_is_defined_and_reachable() { + let g = grammar(); + let defined = defined(g); + assert!(defined.contains("projection"), "the start symbol exists"); + + let refs = references(g); + let used: BTreeSet = refs.iter().flat_map(|(_, r)| r.iter().cloned()).collect(); + + let undefined: Vec<&String> = used.difference(&defined).collect(); + assert!( + undefined.is_empty(), + "grammar references undefined nonterminals: {undefined:?}" + ); + + // Reachability from `projection`. + let edges: std::collections::BTreeMap> = refs.into_iter().collect(); + let mut seen = BTreeSet::new(); + let mut queue = VecDeque::from(vec!["projection".to_string()]); + while let Some(n) = queue.pop_front() { + if !seen.insert(n.clone()) { + continue; + } + for next in edges.get(&n).into_iter().flatten() { + queue.push_back(next.clone()); + } + } + let unreachable: Vec<&String> = defined.difference(&seen).collect(); + assert!( + unreachable.is_empty(), + "grammar defines unreachable nonterminals: {unreachable:?}" + ); +} + +/// The Operation Catalog's section name, hyphenated, for each tag. +/// +/// Exhaustive over `OperationKindTag`, so a new operation kind cannot be added +/// without naming it here — and `the_kind_productions_are_the_operation_vocabulary` +/// then fails until the grammar carries it. The tag names are *not* the catalog +/// names: the tag space renamed three pairs (`InsertRegion`, `InsertStaff`, +/// `InsertStaffInstance`), and the projection follows the semantics. +fn catalog_name(tag: OperationKindTag) -> &'static str { + match tag { + OperationKindTag::InsertEvent => "insert-event", + OperationKindTag::DeleteEvent => "delete-event", + OperationKindTag::ModifyEvent => "modify-event", + OperationKindTag::RespellPitch => "respell-pitch", + OperationKindTag::Transpose => "transpose", + OperationKindTag::TransposeInterval => "transpose-interval", + OperationKindTag::CreateCrossCutting => "create-cross-cutting", + OperationKindTag::DeleteCrossCutting => "delete-cross-cutting", + OperationKindTag::ModifyCrossCutting => "modify-cross-cutting", + OperationKindTag::ChangeRegionTimeModel => "change-region-time-model", + OperationKindTag::InsertRegion => "create-region", + OperationKindTag::DeleteRegion => "delete-region", + OperationKindTag::InsertStaffInstance => "create-staff-instance", + OperationKindTag::DeleteStaffInstance => "delete-staff-instance", + OperationKindTag::SetUserSystemBreak => "set-user-system-break", + OperationKindTag::SetUserPageBreak => "set-user-page-break", + OperationKindTag::DeclareTransaction => "declare-transaction", + OperationKindTag::Registered(_) => "registered", + OperationKindTag::InsertIdentifiedPitch => "insert-identified-pitch", + OperationKindTag::DeleteIdentifiedPitch => "delete-identified-pitch", + OperationKindTag::ModifyIdentifiedPitch => "modify-identified-pitch", + OperationKindTag::CreateVoice => "create-voice", + OperationKindTag::DeleteVoice => "delete-voice", + OperationKindTag::SetMetadata => "set-metadata", + OperationKindTag::SetMetricGrid => "set-metric-grid", + OperationKindTag::InsertStaff => "create-staff", + OperationKindTag::SetTimeSignature => "set-time-signature", + OperationKindTag::SetTempoSegment => "set-tempo-segment", + OperationKindTag::SetStaffLayout => "set-staff-layout", + OperationKindTag::CreateRepeatStructure => "create-repeat-structure", + OperationKindTag::DeleteRepeatStructure => "delete-repeat-structure", + } +} + +/// The right-hand side of `production`, spanning its continuation lines. +/// +/// Located by name, not by column: a grammar reflow must not silently turn a +/// check off. Version 0.3.0's checks were column-anchored and did exactly that. +fn production_block(production: &str) -> &'static str { + let g = grammar(); + let start = g + .lines() + .scan(0usize, |acc, l| { + let here = *acc; + *acc += l.len() + 1; + Some((here, l)) + }) + .find(|(_, l)| { + l.split_once("::=") + .is_some_and(|(lhs, _)| lhs.trim() == production) + }) + .map(|(at, l)| at + l.find("::=").expect("has ::=") + 3) + .unwrap_or_else(|| panic!("the grammar defines `{production}`")); + let rest = &g[start..]; + let end = rest + .lines() + .scan(0usize, |acc, l| { + let here = *acc; + *acc += l.len() + 1; + Some((here, l)) + }) + .find(|(_, l)| l.contains("::=") && !l.trim_start().starts_with('|')) + .map(|(at, _)| at) + .unwrap_or(rest.len()); + &rest[..end] +} + +/// The alternatives of `production`, as the constructor symbol each opens with. +fn alternatives(production: &str) -> BTreeSet { + let block = production_block(production); + + let mut out = BTreeSet::new(); + for (i, _) in block.match_indices("\"(") { + let name: String = block[i + 2..] + .chars() + .take_while(|c| is_name_char(*c)) + .collect(); + if !name.is_empty() { + out.insert(name); + } + } + // Bare-symbol alternatives, e.g. `"not-in-tuplet"`. + for (i, _) in block.match_indices('"') { + let tail = &block[i + 1..]; + if tail.starts_with('(') { + continue; + } + let name: String = tail.chars().take_while(|c| is_name_char(*c)).collect(); + if !name.is_empty() && tail[name.len()..].starts_with('"') { + out.insert(name); + } + } + out +} + +#[test] +fn the_kind_productions_are_the_operation_vocabulary() { + let expected: BTreeSet = OperationKindTag::PAYLOAD_FREE + .iter() + .copied() + .chain(std::iter::once(OperationKindTag::Registered( + epiphany_ops::OperationKindRegistryId(0), + ))) + .map(|t| catalog_name(t).to_string()) + .collect(); + assert_eq!( + expected.len(), + 31, + "30 payload-free kinds plus `Registered`" + ); + + let actual = alternatives("kind"); + assert_eq!( + actual, + expected, + "the grammar's `kind` alternatives must be exactly the operation vocabulary.\n\ + missing from the grammar: {:?}\n\ + present but not a kind: {:?}", + expected.difference(&actual).collect::>(), + actual.difference(&expected).collect::>() + ); +} + +#[test] +fn the_chunk_kind_productions_are_the_chunk_vocabulary() { + let expected: BTreeSet = (0u8..=8) + .map(|d| { + let kind = + ChunkKind::from_discriminant(d).unwrap_or_else(|| panic!("chunk kind {d} exists")); + kebab(&format!("{kind:?}")) + }) + .collect(); + assert_eq!(expected.len(), 9); + assert_eq!(alternatives("chunk-kind"), expected); +} + +/// `OperationEnvelopeBlock` -> `operation-envelope-block`. +fn kebab(camel: &str) -> String { + let mut out = String::new(); + for (i, c) in camel.chars().enumerate() { + if c.is_ascii_uppercase() { + if i != 0 { + out.push('-'); + } + out.push(c.to_ascii_lowercase()); + } else { + out.push(c); + } + } + out +} + +/// `req:textproj:string-escapes` requires a writer to escape exactly the +/// quotation mark, the backslash, U+000A and U+0009, and a parser to reject a +/// literal one. Version 0.3.0's `unescaped` production admitted the backslash, +/// contradicting the requirement it sits beneath. +#[test] +fn the_escape_grammar_agrees_with_the_escape_requirement() { + assert!( + defined(grammar()).contains("escape"), + "the escape sequences must be a production of their own" + ); + + // `unescaped` must exclude every character the requirement obliges a writer to + // escape. Version 0.3.0 admitted the backslash here while requiring it escaped. + let unescaped = production_block("unescaped"); + for codepoint in ["U+0022", "U+005C", "U+000A", "U+0009"] { + assert!( + unescaped.contains(codepoint), + "`unescaped` must exclude {codepoint} by codepoint; it reads: {unescaped}" + ); + } + + // Each escape is *two* characters: the U+005C introducer and one more. Spelling + // the introducer as a quoted terminal `"\\"` reads as two backslashes and makes + // every escape three characters long -- the requirement says two. + let escapes: Vec> = uncommented(production_block("escape")) + .split('|') + .map(|alt| alt.split_whitespace().map(str::to_string).collect()) + .collect(); + let tails: BTreeSet = escapes + .iter() + .map(|alt| { + assert_eq!( + alt.len(), + 2, + "an escape is exactly two characters, the introducer and one more; \ + found {alt:?}" + ); + assert_eq!( + alt[0], "U+005C", + "every escape is introduced by U+005C, written as a codepoint so no \ + quoting convention can make it ambiguous; found {:?}", + alt[0] + ); + alt[1].clone() + }) + .collect(); + let expected: BTreeSet = ["U+0022", "U+005C", "\"n\"", "\"t\""] + .iter() + .map(|s| s.to_string()) + .collect(); + assert_eq!( + tails, expected, + "the escapes are exactly \\\", \\\\, \\n and \\t -- no more, no fewer" + ); +} + +/// The mono font must not apply TeX ligatures. `tlig` rewrites `\"` as a right +/// curly quote and `--` as an en dash, so the grammar -- which delimits terminals +/// with U+0022 and builds escapes from U+005C -- would render characters other +/// than the ones it specifies. A syntax document cannot misprint its own syntax. +#[test] +fn the_mono_font_does_not_substitute_glyphs_in_the_grammar() { + let mono = SPEC + .lines() + .find(|l| l.starts_with("\\setmonofont")) + .expect("the document sets a mono font"); + assert!( + !mono.contains("Ligatures"), + "the mono font must not enable ligatures; it reads: {mono}" + ); +} + +/// The two sequences whose binary order reads erased physical attributes must be +/// named by the derived-ordering requirement, and it must be cited where they are +/// defined. A rule nobody points at is a rule nobody applies. +#[test] +fn the_derived_ordering_requirement_is_cited_where_it_applies() { + assert!(SPEC.contains("\\label{req:textproj:derived-ordering}")); + let citations = SPEC.matches("req:textproj:derived-ordering").count(); + assert!( + citations >= 4, + "expected the label plus citations from the value rule, the blob \ + requirement and the extension requirement; found {citations}" + ); +} diff --git a/spec/text_projection.pdf b/spec/text_projection.pdf index e8d3cb1..51e57f5 100644 Binary files a/spec/text_projection.pdf and b/spec/text_projection.pdf differ diff --git a/spec/text_projection.tex b/spec/text_projection.tex index fc017b8..ccccb8d 100644 --- a/spec/text_projection.tex +++ b/spec/text_projection.tex @@ -61,7 +61,7 @@ urlcolor=epiphanygold, pdftitle={Epiphany --- Text Projection}, pdfauthor={The Epiphany Project}, - pdfsubject={Operation Catalog companion for the Epiphany music notation platform}, + pdfsubject={Text Projection companion for the Epiphany music notation platform}, pdfkeywords={music notation, operations, CRDT, reduction, serialization}, bookmarksnumbered=true, bookmarksopen=true @@ -72,7 +72,10 @@ % --------------------------------------------------------------------------- \setmainfont{TeX Gyre Pagella}[Numbers={OldStyle, Proportional}, Ligatures={TeX, Common}] \setsansfont{TeX Gyre Heros}[Scale=0.94, Ligatures={TeX, Common}] -\setmonofont{TeX Gyre Cursor}[Scale=0.88, Ligatures={TeX}] +% No TeX ligatures in the mono font: `tlig` maps " to a right curly quote and -- +% to an en dash. This document's grammar quotes terminals with U+0022 and spells +% escapes as backslash sequences, so a substituted glyph would misstate the syntax. +\setmonofont{TeX Gyre Cursor}[Scale=0.88] \newfontfamily\titlefont{TeX Gyre Pagella}[Numbers={OldStyle}, Ligatures={TeX, Common}] \newcommand{\tablenums}[1]{{\addfontfeatures{Numbers={Lining,Tabular}}#1}} \newcommand{\sectionsc}[1]{{\addfontfeatures{Letters=SmallCaps}#1}} @@ -226,7 +229,7 @@ {\Large\scshape\color{epiphanyslate}Text Projection}\\[6pt] {\large\itshape\color{epiphanyslate}A companion to the Core Specification}\\[14pt] {\color{epiphanygold}\rule{3in}{0.8pt}}\\[24pt] - {\normalsize\color{epiphanyink}Version 0.3.0 --- Every production expanded; the value-projection rule}\\[4pt] + {\normalsize\color{epiphanyink}Version 0.4.0 --- Derived ordering, and an escape grammar that matches its requirement}\\[4pt] {\small\color{epiphanyslate}Normative for the text form it defines} \vfill \end{titlepage} @@ -471,7 +474,10 @@ projection introduces no ordering of its own. maximum uncompressed length if it declares one, and its uncompressed payload. Its \texttt{BlobId}, content hash, offset, lengths, and compression are - re-derived (Requirement~\ref{req:textproj:derive-or-carry}). + re-derived (Requirement~\ref{req:textproj:derive-or-carry}). The blob lines are + ordered and de-duplicated by their projected form + (Requirement~\ref{req:textproj:derived-ordering}), not by the binary order, + which reads the offset. A blob referenced only by acceleration structures is non-canonical and \MUSTNOT{} be projected. @@ -524,7 +530,10 @@ version, and its constraints. \texttt{schema\_version}, and its uncompressed payload (Requirement~\ref{req:textproj:derive-or-carry}), never as a \texttt{ChunkRef}: a \texttt{ChunkRef} is a physical reference, and the - projection has no file to point into. + projection has no file to point into. The chunk list is ordered and + de-duplicated by projected form + (Requirement~\ref{req:textproj:derived-ordering}), because + \texttt{ChunkRef}'s binary order breaks ties on the offset. \end{requirement} \begin{rationale} @@ -550,6 +559,65 @@ version, and its constraints. of it does not determine the document. \end{rationale} +\section{Ordering What the Binary Form Ordered Physically} +\label{sec:content:derived-ordering} + +``Keep the binary form's order'' is available only where the binary order is a +function of data the projection preserves. Two sequences fail that test. + +\begin{requirement} + \label{req:textproj:derived-ordering} + Where a sequence's binary order depends on attributes + Requirement~\ref{req:textproj:derive-or-carry} erases, the projection \MUST{} + order its elements by their \textbf{projected form}, ascending, comparing the + UTF-8 bytes of the rendered element; and \MUST{} emit at most one element per + distinct projected form. + + In schema major~0 this applies to exactly two sequences: + + \begin{itemize} + \item the \texttt{(blob ...)} lines, whose binary counterpart + \texttt{blob\_roots} is sorted by the full \texttt{BlobRef} encoding --- + which contains the offset, the compressed length, and the compression + algorithm; and + \item an extension's preserved chunk roots, sorted in binary by + \texttt{ChunkRef}'s order, whose key is the kind, then the content hash, + then the \textbf{offset}, with the compressed length, the uncompressed + length, and the compression as further tie-breakers. + \end{itemize} + + Every other projected sequence keeps the binary order, because every other + binary order reads only preserved data. In particular the profile and extension + declarations are sorted in binary by the semantic keys + $(\texttt{profile\_id}, \texttt{version})$ and + $(\texttt{extension\_id}, \texttt{version})$, and the envelopes by canonical + operation order. +\end{requirement} + +\begin{rationale} + Two bundles that differ only in physical layout are the \emph{same document}, + and Requirement~\ref{req:textproj:canonical-text} obliges them to project to + byte-identical text. Inheriting the binary order for these two sequences would + let a chunk's file offset decide the order of the text --- so relocating a chunk, + which changes no semantics, would change the projection. That is precisely the + failure the requirement forbids. + + The de-duplication is the same point from the other side. A chunk is + content-addressed: two entries with identical kind, schema version, and payload + \emph{are} one chunk, and appear twice only because the writer stored the bytes + twice. A blob with identical media type, declared maximum, and payload is one + blob. Their projected forms are identical, so the binary form's distinction + between them is a physical fact --- and a duplicated line would smuggle that + physical fact into a text that claims to have erased it. Emitting one line is + not a loss; it is the erasure working. + + Ordering by the projected form is total and deterministic, and it reads nothing + but what is projected. For chunks it coincides with ordering by the derived + \texttt{ChunkId}, since that id is a function of exactly the kind, schema, and + payload the line carries --- which is a pleasing check that the rule is reading + the right thing. +\end{rationale} + \section{Projecting Canonical Values} \label{sec:content:values} @@ -578,10 +646,11 @@ are ratified. \item An \textbf{option} is \texttt{()} when absent and \texttt{(some )} when present. \item A \textbf{sequence}, \textbf{set}, or \textbf{map} is a parenthesised - list of its elements, \emph{in the order the binary form writes them}; a - map entry is \texttt{( )}. The projection introduces no - ordering of its own, and a set that the binary form writes strictly - increasing is written strictly increasing here + list of its elements, \emph{in the order the binary form writes them}, + except where Requirement~\ref{req:textproj:derived-ordering} applies; a + map entry is \texttt{( )}. The projection invents no ordering + of its own, and a set that the binary form writes strictly increasing is + written strictly increasing here (Requirement~\ref{req:textproj:strict-parse}). \item \textbf{Leaves.} An identifier or hash is a byte string. An integer is an integer. A boolean is \texttt{true} or \texttt{false}. Canonical text is @@ -765,61 +834,60 @@ are ratified. \label{ch:grammar} \begin{lstlisting} -projection ::= header document lineage? profile* extension* +projection ::= header document lineage? profile* extension* canonical-base? blob* envelope* -header ::= "(text-projection " version ")" LF -version ::= "(" integer " " integer " " integer ")" +header ::= "(text-projection " version ")" LF +version ::= "(" integer " " integer " " integer ")" -document ::= "(document " bytes ")" LF -lineage ::= "(lineage " bytes ")" LF +document ::= "(document " bytes ")" LF +lineage ::= "(lineage " bytes ")" LF -profile ::= "(profile " profile-id " " version " " constraints ")" LF -profile-id ::= "full" | "read-only" | "lite" | "(custom " bytes ")" -constraints ::= "(constraints " integer " " retention ")" -retention ::= "(retention " integer " " option " " bool ")" +profile ::= "(profile " profile-id " " version " " constraints ")" LF +profile-id ::= "full" | "read-only" | "lite" | "(custom " bytes ")" +constraints ::= "(constraints " integer " " retention ")" +retention ::= "(retention " integer " " option " " bool ")" -extension ::= "(extension " bytes " " version " " bool +extension ::= "(extension " bytes " " version " " bool " (" chunk* ") " bytes " " bytes ")" LF ; id, version, required, chunks, affected-kinds, barriers ; (the ratified declaration order) -chunk ::= "(chunk " chunk-kind " " schema " " bytes ")" -chunk-kind ::= "operation-envelope-block" | "operation-index" | "snapshot" +chunk ::= "(chunk " chunk-kind " " schema " " bytes ")" +chunk-kind ::= "operation-envelope-block" | "operation-index" | "snapshot" | "blob" | "extension-data" | "text-projection" | "layout-cache" | "integrity-index" | "manifest" -schema ::= "(schema " integer " " integer ")" +schema ::= "(schema " integer " " integer ")" -canonical-base - ::= "(canonical-base " bytes " " bytes " " integer +canonical-base ::= "(canonical-base " bytes " " bytes " " integer " " profile-id " " schema " " bytes ")" LF ; snapshot-id, frontier, reduction version, profile, ; root schema, root payload -blob ::= "(blob " string " " option " " bytes ")" LF +blob ::= "(blob " string " " option " " bytes ")" LF ; media type, declared max uncompressed length, payload -envelope ::= "(envelope " bytes " " bytes " " stamp " " causal +envelope ::= "(envelope " bytes " " bytes " " stamp " " causal " " option " " payload ")" LF ; id, author, stamp, causal context, transaction, payload -stamp ::= "(stamp " integer " " integer " " bytes ")" -causal ::= "(causal (" replica-seen* ") (" bytes* "))" -replica-seen ::= "(" bytes " " integer ")" +stamp ::= "(stamp " integer " " integer " " bytes ")" +causal ::= "(causal (" replica-seen* ") (" bytes* "))" +replica-seen ::= "(" bytes " " integer ")" -payload ::= "(primitive " kind ")" +payload ::= "(primitive " kind ")" | "(resolve-conflict " bytes " " action ")" | "(undo " bytes " " policy ")" | "(resolve-equivocation " bytes " " bytes ")" -action ::= "accept-loser" | "keep-winner" | "dismiss" +action ::= "accept-loser" | "keep-winner" | "dismiss" | "(override " bytes ")" | "(reanchor " bytes ")" | "(registered " bytes ")" -policy ::= "strict-inverse" | "best-effort" | "cascade" +policy ::= "strict-inverse" | "best-effort" | "cascade" ; --- Operation kinds. Fields are the Operation Catalog's payload schema, ; --- positionally, in declaration order. Embedded Chapter-5 values follow ; --- req:textproj:value-projection and are written below. -kind ::= "(insert-event " bytes " " value ")" +kind ::= "(insert-event " bytes " " value ")" | "(delete-event " bytes " " tuplet-comp ")" | "(respell-pitch " bytes " " value ")" | "(create-cross-cutting " cross-cutting ")" @@ -853,32 +921,35 @@ kind ::= "(insert-event " bytes " " value ")" | "(transpose-interval (" bytes* ") (interval " integer " " integer "))" -tuplet-comp ::= "not-in-tuplet" | "(replace-with-rest " value ")" +tuplet-comp ::= "not-in-tuplet" | "(replace-with-rest " value ")" | "(rewrite-tuplets (" bytes* "))" | "(cascade-delete-tuplets (" bytes* "))" -cross-cutting - ::= "(tie " value ")" | "(slur " value ")" +cross-cutting ::= "(tie " value ")" | "(slur " value ")" | "(beam " value ")" | "(spanner " value ")" -remapping ::= "preserve-time" | "(reassign (" reassign-entry* "))" -reassign-entry - ::= "(" bytes " " ratio ")" ; event id, musical position +remapping ::= "preserve-time" | "(reassign (" reassign-entry* "))" +reassign-entry ::= "(" bytes " " ratio ")" ; event id, musical position ; --- Values and leaves. -value ::= "(" symbol " " value* ")" ; req:textproj:value-projection +value ::= "(" symbol " " value* ")" ; req:textproj:value-projection | symbol | bytes | integer | bool | string | ratio | option -option ::= "()" | "(some " value ")" -ratio ::= "(ratio " integer " " integer ")" +option ::= "()" | "(some " value ")" +ratio ::= "(ratio " integer " " integer ")" -bytes ::= "#x" hexdigit* ; even count, lowercase -integer ::= "-"? digit+ ; no leading zeros, no "-0" -bool ::= "true" | "false" -symbol ::= [a-z] [a-z0-9-]* -string ::= '"' schar* '"' -digit ::= [0-9] -hexdigit ::= [0-9a-f] -schar ::= unescaped | '\"' | '\\' | '\n' | '\t' -unescaped ::= [^"\ LF TAB] ; any other character +bytes ::= "#x" hexdigit* ; even count, lowercase +integer ::= "-"? digit+ ; no leading zeros, no "-0" +bool ::= "true" | "false" +symbol ::= [a-z] [a-z0-9-]* +string ::= '"' schar* '"' +digit ::= [0-9] +hexdigit ::= [0-9a-f] +schar ::= unescaped | escape +unescaped ::= +escape ::= U+005C U+0022 ; the two characters \" + | U+005C U+005C ; the two characters \\ + | U+005C "n" ; the two characters \n + | U+005C "t" ; the two characters \t \end{lstlisting} Observe what does \emph{not} appear: no offset, no compressed length, no @@ -1012,6 +1083,43 @@ absorb it, exactly as the binary decoder does. Operation-kind names are the Operation Catalog's section names, not the \texttt{OperationKindTag} names, which renamed three pairs for reasons of the tag space. Still no implementation. \\ + \today & Chapters 3, 5 & 0.4.0 --- Two normative corrections found in review. + + \emph{The grammar contradicted its own escape requirement.} + \texttt{req:textproj:string-escapes} obliges a writer to escape the backslash + and a parser to reject a bare one, while \texttt{unescaped} admitted it. The + escape productions are now spelled out as two-character sequences and + \texttt{unescaped} excludes U+0022, U+005C, U+000A, and U+0009 by codepoint. + Both characters of an escape are written as codepoints where they are the + delimiter or the introducer: a quoted terminal for the backslash reads as + \emph{two} backslashes and would make every escape three characters long. For + the same reason the mono font no longer applies TeX ligatures, which rendered + U+0022 as a right curly quote and \texttt{-{}-} as an en dash --- a document + that specifies a text syntax must not misprint it. + + \emph{``Keep the binary order'' does not work for every sequence.} It is + available only where the binary order reads preserved data, and two sequences + fail that test: \texttt{blob\_roots} is sorted by the full \texttt{BlobRef} + encoding, which contains the offset, the compressed length, and the compression; + and an extension's preserved chunk roots are sorted by \texttt{ChunkRef}'s + order, whose key is kind, then content hash, then \emph{offset}. Under the + blanket rule, relocating a chunk --- which changes no semantics --- would have + changed the text, and two entries indistinguishable after erasure would have + produced duplicate lines. \texttt{req:textproj:derived-ordering} orders and + de-duplicates those two sequences by their \emph{projected form}. Every other + sequence keeps the binary order: the profile and extension declarations sort on + semantic \texttt{(id, version)} keys, and the envelopes on canonical operation + order. + + Also: a committed grammar-completeness test now checks that no nonterminal is + undefined or unreachable, that the escape rule excludes the four codepoints and + admits exactly the four two-character sequences, that the mono font substitutes + no glyphs, and that the operation-kind and chunk-kind productions are exactly + the tag vocabularies --- derived from \texttt{OperationKindTag} and + \texttt{ChunkKind}, not transcribed. Every locator in it finds its production by + name; the checks it replaced were anchored to a column, and a reflow would have + silently switched them off. The 0.3.0 claim of a ``machine-checked'' grammar was + true of one run and of nothing durable. Still no implementation. \\ \bottomrule \end{longtable}