From a62092eceff17be0cf7456d777d48be3e3988371 Mon Sep 17 00:00:00 2001 From: Transaction Science Date: Mon, 2 Nov 2026 03:30:36 -0500 Subject: [PATCH] joulespec: a bullet whose label could not be read was corrupting the obligation above it MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Pointing the extractor at this family's other specifications — documents written without this producer in mind — found a soundness bug in the producer and a gap in a sibling standard. The bug: a list item carrying a bold label the splitter could not read was classified as *body* and appended to whichever item was open. On one sibling specification a `- **C-neg:**` bullet ended up inside C5's text, so C5's obligation address covered words belonging to a different clause. An obligation that says something nobody wrote is the one failure this standard cannot tolerate, because every grade below it is then about the wrong sentence. Three changes, and the ordering of them matters: - the splitter accepts the separators that appear in practice, and a bold segment carrying only a label — `**C-neg:**` — is an item whose name is empty, addressed over its body alone rather than over a separator nobody wrote; - a bare segment counts as a label only when it carries no whitespace, so a bolded *sentence* leading an ordinary list is still not an item. That rule already existed for the em dash and dropping it would have invented obligations out of prose; the core's own label validation refuses whitespace for the same reason, so this is that rule read one step earlier; - an item-shaped line that still cannot be read fails closed instead of becoming body — but only where an item is open, since that is the only case where folding corrupts anything. With nothing open there is nothing to append to, and a section of ordinary prose should report that it holds no items of the declared shape rather than name one of its sentences as malformed. The pinned obligation address for the default shape is unchanged, which is what makes the first two safe to land. New `joulespec clauses` subcommand: show what the extractor reads out of a document and the obligation address each item would carry. Authoring a manifest starts by agreeing with the producer about what the clauses *are*, and without this an operator discovers a mis-declared shape through an item count, which says nothing about which items were missed. The gap, reported and not fixed here because it belongs to another standard: `sandbox/SPEC.md` §10 enumerates C12 (locality evidence, §7.7) among its test obligations, and the normative companion it points at defines C1 through C11 and C13 with no C12 anywhere. Nothing could ever have evidenced it. Co-Authored-By: Claude Opus 5 --- joulespec/README.md | 18 +++ .../crates/joulespec-cli/src/main.rs | 39 +++++ .../crates/joulespec-cli/src/specdoc.rs | 142 ++++++++++++++++-- 3 files changed, 183 insertions(+), 16 deletions(-) diff --git a/joulespec/README.md b/joulespec/README.md index 11618ca99..f8b5fd8ba 100644 --- a/joulespec/README.md +++ b/joulespec/README.md @@ -303,6 +303,24 @@ shape = "heading-label" # or bulleted-bold-label; omitted = numbered expect_at_least = 14 # the floor still fails closed ``` +Run against this family's other specifications — documents written without +this producer in mind — the bulleted shape reads their conformance lists and +the heading shape reads a normative companion kept as one section per +obligation. What does not read is reported rather than returned empty: a +conformance section written as a table of profiles, or as numbered prose with +no labels, says it holds no items of the declared shape. `joulespec clauses` +exists for exactly this, because the alternative is discovering a mis-declared +shape through an item count, which says nothing about which items were missed. + +Doing that found two things. In the producer: a bullet carrying a bold label +the splitter could not read was being folded into the item above, which +appended a *different* item's words to that obligation's addressed text — +a soundness bug, since the obligation then says something nobody wrote. It now +fails closed, and a bare label like `**C-neg:**` reads as the item it is. In a +sibling standard: its conformance section enumerates a clause its own +normative companion never defines, so that obligation could never have been +evidenced by anything. + Nothing else about the extraction varies, and a heading that states no requirement is not read as one — addressing the empty string would create an obligation nobody wrote and then grade it. Changing the declared shape moves diff --git a/joulespec/joulespec-rs/crates/joulespec-cli/src/main.rs b/joulespec/joulespec-rs/crates/joulespec-cli/src/main.rs index 4f38250ac..608649dee 100644 --- a/joulespec/joulespec-rs/crates/joulespec-cli/src/main.rs +++ b/joulespec/joulespec-rs/crates/joulespec-cli/src/main.rs @@ -196,6 +196,41 @@ fn cmd_verify(args: &Args) -> Result { Ok(0) } +/// Show what the extractor reads out of a specification document, and the +/// obligation address each item would carry. +/// +/// Authoring a manifest starts by agreeing with the producer about what the +/// clauses *are*. Without this an operator discovers a mis-declared shape +/// through a clause count, which says nothing about which items were missed. +fn cmd_clauses(args: &Args) -> Result { + let path = args.need("document")?; + let section = args.need("section")?; + let shape = match args.get("shape") { + Some(name) => specdoc::Shape::parse(name).map_err(|e| e.to_string())?, + None => specdoc::Shape::default(), + }; + let floor: usize = match args.get("expect-at-least") { + Some(v) => v.parse().map_err(|_| format!("--expect-at-least {v:?} is not a number"))?, + None => 1, + }; + let text = std::fs::read_to_string(path).map_err(|e| format!("{path}: {e}"))?; + let items = specdoc::items(&text, section, floor, shape).map_err(|e| e.to_string())?; + let clauses = specdoc::clauses(&items); + + println!("document {path}"); + println!("section {section}"); + println!("shape {}", shape.label()); + println!("items {}", items.len()); + println!(); + for (item, clause) in items.iter().zip(&clauses) { + let obligation = clause.obligation().map_err(|e| e.to_string())?; + println!("{:<6} {}", item.label, obligation.as_str()); + println!(" {} — {}", item.name, item.text); + println!(); + } + Ok(0) +} + fn cmd_drift(args: &Args) -> Result { let read = |p: &str| -> Result { let text = std::fs::read_to_string(p).map_err(|e| format!("{p}: {e}"))?; @@ -243,6 +278,9 @@ joulespec — the reference producer and checker for joulespec/1 [--author-seed N] [--witness-seed N] [--steward-seed N] joulespec verify --receipt --steward --key <64 hex chars> joulespec drift --from --to + joulespec clauses --document --section + [--shape numbered-bold-label|bulleted-bold-label|heading-label] + [--expect-at-least N] harvest exits 2 when it has a finding (a check that did not run, or one that passed while its subject was broken) and 3 when an owed obligation falls below @@ -257,6 +295,7 @@ fn main() { "harvest" => cmd_harvest(&args), "verify" => cmd_verify(&args), "drift" => cmd_drift(&args), + "clauses" => cmd_clauses(&args), "" | "help" | "--help" | "-h" => { print!("{USAGE}"); Ok(0) diff --git a/joulespec/joulespec-rs/crates/joulespec-cli/src/specdoc.rs b/joulespec/joulespec-rs/crates/joulespec-cli/src/specdoc.rs index e20732309..ae342ed64 100644 --- a/joulespec/joulespec-rs/crates/joulespec-cli/src/specdoc.rs +++ b/joulespec/joulespec-rs/crates/joulespec-cli/src/specdoc.rs @@ -59,6 +59,22 @@ pub enum SpecDocError { /// The shape that matched nothing. shape: &'static str, }, + /// A line opens something shaped like an item but cannot be read as one. + /// + /// Fails closed rather than guessing. The alternative — folding it into + /// the item above — changes that item's addressed text without saying so. + #[error( + "in section {section:?} under shape {shape:?}, this looks like an item \ + but cannot be read as one: {line:?}" + )] + UnreadableItem { + /// The section searched. + section: String, + /// The declared shape. + shape: &'static str, + /// The offending line, truncated. + line: String, + }, /// The declared shape is not one this producer implements. #[error("unknown clause shape {got:?}; expected one of {known}")] UnknownShape { @@ -165,17 +181,41 @@ fn is_section_heading(line: &str, section: &str) -> bool { /// Split `**C1 — Addressing.** rest…` into its three parts. /// -/// The em dash is required: it is what distinguishes a labelled conformance -/// item from an ordinary bolded sentence in a numbered list. +/// The bold segment holds a label and, usually, a short name. Three +/// separators appear in practice and all three are accepted, because which +/// one a document uses is punctuation rather than meaning. A bold segment +/// carrying only a label — `**C-neg:** …` — is also an item: the name is +/// then empty and the obligation is addressed over the body alone. +/// +/// Returns `None` only when the segment is not bold at all, or when the label +/// itself is empty. Those are the cases where there is nothing to name. fn split_item(body: &str) -> Option<(String, String, String)> { let rest = body.strip_prefix("**")?; let (head, tail) = rest.split_once("**")?; - let (label, name) = head.split_once(" — ")?; - let name = name.trim().trim_end_matches('.'); - if label.trim().is_empty() || name.is_empty() { + let (label, name) = match head + .split_once(" — ") + .or_else(|| head.split_once(": ")) + .or_else(|| head.split_once(" - ")) + { + Some((l, n)) => (l, n.trim().trim_end_matches(['.', ':']).to_string()), + // A bold segment with no separator is a bare label — but only if it + // looks like one. `**C-neg:**` is an item; `**Bolded sentence.**` is + // a lead-in to an ordinary list and naming it would invent an + // obligation. A label carries no whitespace, which is also what the + // core refuses when it validates one, so this is the same rule read + // one step earlier. + None => { + let bare = head.trim_end_matches([':', '.', ' ']); + if bare.contains(char::is_whitespace) { + return None; + } + (bare, String::new()) + } + }; + if label.trim().is_empty() { return None; } - Some((label.trim().to_string(), name.to_string(), tail.trim().to_string())) + Some((label.trim().to_string(), name, tail.trim().to_string())) } /// Split a heading's text into `label`, `name` on either an em dash or a @@ -200,6 +240,9 @@ enum Line<'a> { Opens(String, String, String), /// This line continues the open item, or closes it if blank. Body(&'a str), + /// This line opens something shaped like an item that cannot be read as + /// one. Never treated as body — see [`classify`]. + Unreadable, } /// Classify one line. The shape decides only what *opens* an item and what @@ -226,11 +269,21 @@ fn classify<'a>(line: &'a str, shape: Shape, section_depth: usize) -> Line<'a> { .strip_prefix("- ") .or_else(|| trimmed.strip_prefix("* ")), }; - match body.and_then(split_item) { - Some((label, name, text)) => Line::Opens(label, name, text), - // A list item that does not carry a label is body: it may be - // a sub-list under the open item. - None => Line::Body(line), + match body { + // A list item carrying a bold segment is an item. If it + // cannot be read as one, it is **not** quietly folded into + // the item above: doing that appends a different item's words + // to an obligation's addressed text, which silently changes + // what that obligation says. Observed on a sibling + // specification, where a `**C-neg:**` bullet ended up inside + // C5's address. + Some(b) if b.trim_start().starts_with("**") => match split_item(b) { + Some((label, name, text)) => Line::Opens(label, name, text), + None => Line::Unreadable, + }, + // A list item with no bold segment is body: a genuine + // sub-point under the open item. + _ => Line::Body(line), } } // Here the items *are* headings, so the section ends only at a @@ -287,6 +340,19 @@ pub fn items( for line in lines { match classify(line, shape, section_depth) { Line::SectionEnd => break, + // Only an *open* item can be corrupted by folding a line into + // it, so that is the only case this refuses. With nothing open + // there is nothing to append to, and a section whose bolded + // lines are ordinary prose should report that it holds no items + // of this shape rather than name one of them as malformed. + Line::Unreadable if pending.is_some() => { + return Err(SpecDocError::UnreadableItem { + section: section.to_string(), + shape: shape.label(), + line: line.trim().chars().take(72).collect(), + }); + } + Line::Unreadable => {} Line::Opens(label, name, text) => { if let Some(item) = pending.take() { out.push(item); @@ -352,11 +418,15 @@ pub fn clauses(items: &[Item]) -> Vec { items .iter() .map(|i| { - Clause::new( - i.label.clone(), - ClauseKind::Requirement, - format!("{} — {}", i.name, i.text), - ) + // An item with no name is addressed over its body alone. Joining + // an empty name with a separator would put punctuation nobody + // wrote into the obligation's text. + let text = if i.name.is_empty() { + i.text.clone() + } else { + format!("{} — {}", i.name, i.text) + }; + Clause::new(i.label.clone(), ClauseKind::Requirement, text) }) .collect() } @@ -453,6 +523,46 @@ The reference implementation is conformant by construction. assert!(matches!(err, SpecDocError::TooFew { found: 3, expected: 11, .. }), "{err}"); } + /// Observed on a sibling specification: `- **C-neg:** text` carries a + /// label and no name. Before this was handled, the line failed to parse + /// and was folded into the item above, appending a different item's words + /// to that obligation's addressed text. + #[test] + fn a_bare_label_is_an_item_and_does_not_leak_into_the_item_above() { + let doc = concat!( + "## 7. Conformance\n\n", + "- **C1 — Named.** The first item.\n", + "- **C-neg:** The negative pack.\n", + ); + let got = items(doc, "7. Conformance", 2, Shape::BulletedBold).expect("parses"); + assert_eq!(got.len(), 2, "{got:#?}"); + assert_eq!(got[1].label, "C-neg"); + assert!(got[1].name.is_empty(), "a bare label has no name"); + assert_eq!( + got[0].text, "The first item.", + "the next item's words must not appear in this obligation" + ); + // With no name, the obligation is addressed over the body alone + // rather than over a separator nobody wrote. + let c = clauses(&got); + assert_eq!(c[1].text, "The negative pack."); + } + + /// A line that looks like an item and cannot be read as one fails the + /// parse rather than joining the item above, for the same reason. + #[test] + fn an_item_shaped_line_that_cannot_be_read_fails_closed() { + let doc = concat!( + "## 7. Conformance\n\n", + "- **C1 — Named.** The first item.\n", + "- **** empty label.\n", + ); + assert!(matches!( + items(doc, "7. Conformance", 1, Shape::BulletedBold), + Err(SpecDocError::UnreadableItem { .. }) + )); + } + #[test] fn an_unlabelled_numbered_line_is_not_an_item() { let doc = "## 7. Conformance\n\n1. **Bolded but unlabelled.** No em dash.\n"; -- 2.54.0 (Apple Git-157)