Text Projection 0.7.0: single-version headers, and blob lines are rejected
Scoping the document layer found that no blob can be canonical. A blob is canonical iff referenced by a canonical operation or by canonical reduced state (`req:textproj:canonical-blobs`; core_spec §"Canonical and Non-Canonical Manifest Roots"), and nothing in epiphany-core or epiphany-ops references a `BlobId` -- there is no mechanism by which one can be reached. So today every real bundle projects to zero blob lines. The first instinct was to let a parser accept blob lines anyway, for forward compatibility. That is wrong twice over. Forward compatibility is owned by header gating -- a future writer's text carries a future version, which this parser rejects at line one -- and a blob line accepted today would be staged into a bundle that the next projection silently drops, losing data *and* falsifying `project(serialize(parse(T))) == T` for that text. `req:textproj:reject-unreferenced-blobs` therefore requires rejection, and the conformance equation holds unconditionally over parse-accepted texts rather than only over texts in the image of `project`. `req:textproj:header-version` pins the other half: a parser accepts exactly one header version, the companion's own. Multi-version acceptance and text migrate-on-read are deferred in the same posture as op-payload migrate-on-read rather than improvised. Auditing the worked example against its own grammar found three defects in it: it carried a blob line, which is now by construction an example of an *invalid* document; its byte strings used literal ellipses, which `bytes ::= "#x" hexdigit*` cannot derive; and its header still claimed 0.3.0. All three fixed, and the preamble no longer promises elisions it does not contain -- an example that cannot be parsed teaches the wrong lesson. The version now appears in six places here. Two were locked; the two dangerous ones were not, because they are *normative* -- a bump that updated the title and missed them would leave the companion requiring parsers to accept a version it no longer is. `requirements_name_only_this_companion_version` scans every requirement block and holds any version literal to the title, deliberately exempting the revision history, where old versions are the point. Twelve grammar-gate tests, all mutation-verified. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This commit is contained in:
parent
fdb4a57885
commit
50ad97a31b
|
|
@ -31,6 +31,10 @@
|
|||
//! 7. `transpose-interval` takes target bytes followed by a `value`; `interval`
|
||||
//! is not allowed to become a grammar production parallel to the canonical
|
||||
//! `TranspositionInterval` value spelling.
|
||||
//! 8. The worked example's header is the one implemented companion version.
|
||||
//! 9. Unreferenced blob lines have an explicitly labelled, cited rejection rule
|
||||
//! with the round-trip and version-gating rationale that makes rejection
|
||||
//! necessary.
|
||||
|
||||
use std::collections::{BTreeSet, VecDeque};
|
||||
|
||||
|
|
@ -64,6 +68,19 @@ fn grammar() -> &'static str {
|
|||
&SPEC[start..start + end]
|
||||
}
|
||||
|
||||
/// The worked example's complete projection listing.
|
||||
fn worked_example() -> &'static str {
|
||||
SPEC.split_once("\\chapter{A Worked Example}")
|
||||
.expect("the specification contains the worked example")
|
||||
.1
|
||||
.split_once("\\begin{lstlisting}\n")
|
||||
.expect("the worked example contains a projection listing")
|
||||
.1
|
||||
.split_once("\\end{lstlisting}")
|
||||
.expect("the worked projection listing is closed")
|
||||
.0
|
||||
}
|
||||
|
||||
/// 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.
|
||||
|
|
@ -515,3 +532,191 @@ fn the_derived_ordering_requirement_is_cited_where_it_applies() {
|
|||
requirement and the extension requirement; found {citations}"
|
||||
);
|
||||
}
|
||||
|
||||
/// The envelope already has a byte-exact production-code lock in
|
||||
/// `epiphany-ops`; the companion header above it must be locked as well. Derive
|
||||
/// the expected spelling from the title version so a future bump cannot update
|
||||
/// only one of the two.
|
||||
#[test]
|
||||
fn worked_example_header_is_the_implemented_companion_version() {
|
||||
let title_version = SPEC
|
||||
.lines()
|
||||
.find_map(|line| {
|
||||
line.split_once("Version ")
|
||||
.and_then(|(_, rest)| rest.split_once(" ---"))
|
||||
.map(|(version, _)| version)
|
||||
})
|
||||
.expect("the title page declares the companion version");
|
||||
assert_eq!(
|
||||
title_version, "0.7.0",
|
||||
"this implementation targets exactly companion 0.7.0"
|
||||
);
|
||||
|
||||
let expected = format!("(text-projection ({}))", title_version.replace('.', " "));
|
||||
let actual = worked_example()
|
||||
.lines()
|
||||
.next()
|
||||
.expect("the worked projection has a header");
|
||||
assert_eq!(
|
||||
actual, expected,
|
||||
"the worked example header must match the implemented companion version"
|
||||
);
|
||||
}
|
||||
|
||||
/// At 0.7.0 no canonical state can reference a blob, so accepting a blob line
|
||||
/// would make the text round trip lossy. Lock both the normative rejection and
|
||||
/// the rationale/citations that prevent a future reader from treating it as an
|
||||
/// accidental incompatibility.
|
||||
#[test]
|
||||
fn unreferenced_blob_rejection_is_normative_labelled_and_cited() {
|
||||
const LABEL: &str = "req:textproj:reject-unreferenced-blobs";
|
||||
let label = format!("\\label{{{LABEL}}}");
|
||||
let label_at = SPEC
|
||||
.find(&label)
|
||||
.unwrap_or_else(|| panic!("the blob rejection must be labelled `{LABEL}`"));
|
||||
let requirement_start = SPEC[..label_at]
|
||||
.rfind("\\begin{requirement}")
|
||||
.expect("the blob-rejection label is on a normative requirement");
|
||||
let section_end = SPEC[label_at..]
|
||||
.find("\\section{Profile Declarations}")
|
||||
.map(|offset| label_at + offset)
|
||||
.expect("the blob rejection precedes profile declarations");
|
||||
let rule_and_rationale = &SPEC[requirement_start..section_end];
|
||||
|
||||
assert!(
|
||||
rule_and_rationale
|
||||
.contains("A parser \\MUST{} reject every \\texttt{(blob ...)} line whose blob is"),
|
||||
"the labelled requirement must reject every unreferenced blob line"
|
||||
);
|
||||
assert!(
|
||||
rule_and_rationale.contains("req:textproj:canonical-blobs"),
|
||||
"the rejection rule must cite the canonical-blob definition"
|
||||
);
|
||||
assert!(
|
||||
SPEC.matches(LABEL).count() >= 2,
|
||||
"`{LABEL}` must be both declared and cited"
|
||||
);
|
||||
for rationale_anchor in [
|
||||
"necessarily non-canonical",
|
||||
"next projection silently drops",
|
||||
"causing data loss and falsifying",
|
||||
"\\textrm{project}(\\textrm{serialize}(\\textrm{parse}(T))) = T",
|
||||
"Forward compatibility belongs to header-version gating",
|
||||
"req:textproj:header-version",
|
||||
] {
|
||||
assert!(
|
||||
rule_and_rationale.contains(rationale_anchor),
|
||||
"the blob-rejection rationale must retain `{rationale_anchor}`"
|
||||
);
|
||||
}
|
||||
}
|
||||
|
||||
/// The companion version declared on the title page.
|
||||
fn title_version() -> &'static str {
|
||||
SPEC.lines()
|
||||
.find_map(|line| {
|
||||
line.split_once("Version ")
|
||||
.and_then(|(_, rest)| rest.split_once(" ---"))
|
||||
.map(|(version, _)| version)
|
||||
})
|
||||
.expect("the title page declares the companion version")
|
||||
}
|
||||
|
||||
/// Every `\begin{requirement}`…`\end{requirement}` body.
|
||||
fn requirement_blocks() -> Vec<&'static str> {
|
||||
let mut out = Vec::new();
|
||||
let mut rest = SPEC;
|
||||
while let Some((_, after)) = rest.split_once("\\begin{requirement}") {
|
||||
let (body, tail) = after
|
||||
.split_once("\\end{requirement}")
|
||||
.expect("every requirement block is closed");
|
||||
out.push(body);
|
||||
rest = tail;
|
||||
}
|
||||
out
|
||||
}
|
||||
|
||||
/// Version literals in `0.7.0` and `(0 7 0)` form, as `(major, minor, patch)`.
|
||||
fn version_literals(text: &str) -> Vec<String> {
|
||||
let bytes: Vec<char> = text.chars().collect();
|
||||
let mut out = Vec::new();
|
||||
for i in 0..bytes.len() {
|
||||
// `D.D.D`
|
||||
if bytes[i].is_ascii_digit() {
|
||||
let mut j = i;
|
||||
let mut parts = Vec::new();
|
||||
let mut cur = String::new();
|
||||
while j < bytes.len() && (bytes[j].is_ascii_digit() || bytes[j] == '.') {
|
||||
if bytes[j] == '.' {
|
||||
if cur.is_empty() {
|
||||
break;
|
||||
}
|
||||
parts.push(std::mem::take(&mut cur));
|
||||
} else {
|
||||
cur.push(bytes[j]);
|
||||
}
|
||||
j += 1;
|
||||
}
|
||||
if !cur.is_empty() {
|
||||
parts.push(cur);
|
||||
}
|
||||
if parts.len() == 3 && (i == 0 || !bytes[i - 1].is_ascii_digit()) {
|
||||
out.push(parts.join("."));
|
||||
}
|
||||
}
|
||||
// `(D D D)`
|
||||
if bytes[i] == '(' {
|
||||
let mut j = i + 1;
|
||||
let mut parts = Vec::new();
|
||||
let mut cur = String::new();
|
||||
while j < bytes.len() && (bytes[j].is_ascii_digit() || bytes[j] == ' ') {
|
||||
if bytes[j] == ' ' {
|
||||
if !cur.is_empty() {
|
||||
parts.push(std::mem::take(&mut cur));
|
||||
}
|
||||
} else {
|
||||
cur.push(bytes[j]);
|
||||
}
|
||||
j += 1;
|
||||
}
|
||||
if !cur.is_empty() {
|
||||
parts.push(cur);
|
||||
}
|
||||
if j < bytes.len() && bytes[j] == ')' && parts.len() == 3 {
|
||||
out.push(parts.join("."));
|
||||
}
|
||||
}
|
||||
}
|
||||
out
|
||||
}
|
||||
|
||||
/// A version number named inside a **normative** block must be *this* companion's
|
||||
/// version.
|
||||
///
|
||||
/// The version lives in six places in this document: the title page, two
|
||||
/// requirements, the worked example, and two revision-history cells. Only the
|
||||
/// title and the example were locked. The two requirements are the dangerous
|
||||
/// ones — they are normative, so a bump that misses them leaves the companion
|
||||
/// *requiring* parsers to accept a version it no longer is. The revision history
|
||||
/// is deliberately not covered: old rows name old versions, which is the point of
|
||||
/// a history.
|
||||
#[test]
|
||||
fn requirements_name_only_this_companion_version() {
|
||||
let title = title_version();
|
||||
let mut found = 0usize;
|
||||
for block in requirement_blocks() {
|
||||
for literal in version_literals(block) {
|
||||
found += 1;
|
||||
assert_eq!(
|
||||
literal, title,
|
||||
"a requirement names version `{literal}` but the companion is \
|
||||
`{title}`; normative text must not outlive a bump"
|
||||
);
|
||||
}
|
||||
}
|
||||
assert!(
|
||||
found >= 2,
|
||||
"expected the header-version and blob-rejection requirements to name a \
|
||||
version; found {found} — this lock has stopped reaching them"
|
||||
);
|
||||
}
|
||||
|
|
|
|||
Binary file not shown.
|
|
@ -229,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.6.0 --- The operation vocabulary is grammar-directed; values enter exactly where named}\\[4pt]
|
||||
{\normalsize\color{epiphanyink}Version 0.7.0 --- Canonical blob rejection and single-version header gating}\\[4pt]
|
||||
{\small\color{epiphanyslate}Normative for the text form it defines}
|
||||
\vfill
|
||||
\end{titlepage}
|
||||
|
|
@ -459,6 +459,18 @@ A projection is, in order:
|
|||
(core specification Appendix~D).
|
||||
\end{enumerate}
|
||||
|
||||
\begin{requirement}
|
||||
\label{req:textproj:header-version}
|
||||
A parser implementing this companion \MUST{} accept exactly one header
|
||||
version: \texttt{(0 7 0)}, the version of the companion it implements. It
|
||||
\MUST{} reject any other version at line one.
|
||||
|
||||
Multi-version acceptance and text migrate-on-read are deferred in the same
|
||||
posture as op-payload migrate-on-read: support belongs in an explicit,
|
||||
version-keyed migration path when a real consumer requires it. The current
|
||||
parser \MUSTNOT{} speculate by accepting another version.
|
||||
\end{requirement}
|
||||
|
||||
Every sequence is written in the normative order its binary counterpart uses. The
|
||||
projection introduces no ordering of its own.
|
||||
|
||||
|
|
@ -481,6 +493,9 @@ projection introduces no ordering of its own.
|
|||
|
||||
A blob referenced only by acceleration structures is non-canonical and
|
||||
\MUSTNOT{} be projected.
|
||||
|
||||
Parser handling of unreferenced blob lines is specified by
|
||||
Requirement~\ref{req:textproj:reject-unreferenced-blobs}.
|
||||
\end{requirement}
|
||||
|
||||
\begin{rationale}
|
||||
|
|
@ -493,6 +508,25 @@ projection introduces no ordering of its own.
|
|||
projection preserves; both are corrected.
|
||||
\end{rationale}
|
||||
|
||||
\begin{requirement}
|
||||
\label{req:textproj:reject-unreferenced-blobs}
|
||||
A parser \MUST{} reject every \texttt{(blob ...)} line whose blob is
|
||||
unreferenced by canonical state
|
||||
(Requirement~\ref{req:textproj:canonical-blobs}). At companion
|
||||
version~0.7.0, neither a canonical operation nor canonical reduced state can
|
||||
carry a \texttt{BlobId}; canonical state therefore cannot reference a blob,
|
||||
and a parser \MUST{} reject every \texttt{(blob ...)} line.
|
||||
\end{requirement}
|
||||
|
||||
\begin{rationale}
|
||||
A blob-bearing text at this version is necessarily non-canonical. Accepting
|
||||
one stages a blob into the bundle that the next projection silently drops,
|
||||
causing data loss and falsifying
|
||||
$\textrm{project}(\textrm{serialize}(\textrm{parse}(T))) = T$ for that text.
|
||||
Forward compatibility belongs to header-version gating
|
||||
(Requirement~\ref{req:textproj:header-version}), not to leniency here.
|
||||
\end{rationale}
|
||||
|
||||
\section{Profile Declarations}
|
||||
\label{sec:content:profiles}
|
||||
|
||||
|
|
@ -1069,19 +1103,19 @@ the tag.
|
|||
\chapter{A Worked Example}
|
||||
\label{ch:example}
|
||||
|
||||
\emph{Non-normative.} The byte strings below are illustrative. The conformance
|
||||
vectors that pin real bytes are a deliverable of the implementation, not of this
|
||||
gate; elisions are marked \texttt{\dots}.
|
||||
\emph{Non-normative.} The byte strings below are illustrative but
|
||||
\emph{well-formed}: every one is a grammar-valid \texttt{bytes} terminal, because
|
||||
an example that cannot be parsed teaches the wrong lesson. The conformance vectors
|
||||
that pin \emph{real} bytes are a deliverable of the implementation.
|
||||
|
||||
A document of one operation --- a transposition of two pitches up a perfect
|
||||
fifth, over a compacted base and one embedded image --- projects to six lines:
|
||||
fifth, over a compacted base --- projects to five lines:
|
||||
|
||||
\begin{lstlisting}
|
||||
(text-projection (0 3 0))
|
||||
(text-projection (0 7 0))
|
||||
(document #x05050505050505050505050505050505)
|
||||
(profile full (0 1 0) (constraints 67108864 (retention 1 () true)))
|
||||
(canonical-base #x1f8b... #x00 1 full (schema 0 1) #x0000...)
|
||||
(blob "image/png" () #x89504e47...)
|
||||
(canonical-base #x1f8b0000000000000000000000000000 #x 1 full (schema 0 1) #x0000)
|
||||
(envelope #x00000000000000070000000000000001 #x00000000000000000000000011223344 (stamp 42 7 #x00000000000000070000000000000001) (causal ((#x0000000000000001 3)) (#x00000000000000020000000000000009)) (some #x00000000000000070000000000000005) (primitive (transpose-interval (#x00000000000000070000000000000001 #x00000000000000070000000000000002) (transposition-interval 4 7))))
|
||||
\end{lstlisting}
|
||||
|
||||
|
|
@ -1248,6 +1282,24 @@ absorb it, exactly as the binary decoder does.
|
|||
position, and the grammar has no special \texttt{interval} production. The
|
||||
committed grammar gate locks the requirement, its reliance-point citations,
|
||||
and that absence. \\
|
||||
\today & Chapters 3, 5 & 0.7.0 --- Canonical blob rejection and
|
||||
single-version header gating. At this version no canonical operation or
|
||||
canonical reduced state can reference a \texttt{BlobId}; every
|
||||
\texttt{(blob ...)} line is therefore unreferenced and non-canonical, and a
|
||||
parser must reject it
|
||||
(\texttt{req:textproj:reject-unreferenced-blobs}). Accepting it would stage
|
||||
content the next projection silently drops, lose data, and falsify the
|
||||
text-to-binary-to-text round trip. Forward compatibility belongs to
|
||||
header-version gating, not lenient blob acceptance.
|
||||
|
||||
The parser accepts exactly the implemented companion header,
|
||||
\texttt{(0 7 0)}, and rejects every other version
|
||||
(\texttt{req:textproj:header-version}). Multi-version acceptance and text
|
||||
migrate-on-read remain deferred, in the same posture as op-payload
|
||||
migrate-on-read: a future real consumer must bring an explicit,
|
||||
version-keyed migration path rather than teaching the current parser to
|
||||
speculate. The worked example now uses the implemented header and contains
|
||||
only grammar-valid, canonical lines. \\
|
||||
\bottomrule
|
||||
\end{longtable}
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue