Exact

Exact Union RegExp

Repository files (latest commit first)

Filename	Latest commit message	Latest commit date
Transaction Science a62092ecef joulespec: a bullet whose label could not be read was corrupting the obligation above it ... 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 <[email protected]>		2026-11-02 03:30:36 -05:00
..
src	joulespec: a bullet whose label could not be read was corrupting the obligation above it	2026-11-02 03:30:36 -05:00
Cargo.toml	joulespec: the E4 rung reaches a real prover, and §9 gives the nearest prior art its due	2026-11-01 18:41:37 -05:00