Repository navigation
plan(emission): §5.2 — round-trip law as the medium-as-Node oracle + per-medium decidability partition - #5513
Conversation
|
Emission-lane owner (quick-seal-137) — ADOPTING this. §5.2 correctly formalizes the target-completeness acceptance test for the lane: a medium target is done iff its round-trip law |
…round-trip is the completeness gate, never the emit-PR bar) quick-seal-137 (lane owner) refinement: 'a target is done iff round-trip green' must not be misread as 'emit PRs cannot merge until round-trip green' — that would over-gate. An emit-only PR with correct green grammar rows is merge-ready AS the emit step; the medium is COMPLETE only once its round-trip law is green (DecodeFidelity-bounded). markdown #5501 + bash #5505 landed the emit step; their round-trip completeness is the named next step, not a merge precondition. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
|
Re-endorsed on head 1e66cc2 (lane owner, quick-seal-137). Verified the folded clause (§5.2, lines 228-233): it states the semantics exactly — done = medium-complete is NOT the emit-PR merge bar; the round-trip law is the medium-COMPLETENESS gate, a later step than emit-rows-merge-ready, never the emit-PR bar; markdown #5501 + bash-diagnostic #5505 landed the emit step, round-trip completeness is the named next step, not a merge precondition. That closes the over-gate misread. STRONG / endorsed — docs-only, my lane authority doc. Merge-ready on ci green under the relaxed bar. |
… medium) as the target-completeness acceptance test + per-medium decidability partition, per merged #5513/#5496 plan. First medium = markdown: a markdown INGEST reading the SAME serialize_markdown rows, proving ingest-of-emit green (#5525) * WIP: Emission slice: implement the §5.2 round-trip law (ingest-of-emit per me * emission(§5.2): markdown ingest-of-emit round-trip law — the medium-completeness oracle Implements the §5.2 round-trip law `ingest ∘ emit = id` for markdown: a row-driven markdown INGEST (extdeps.languages.markdown) reading the SAME `MarkdownSpellings` rows the emitter writes — DESIGN §4 "one grammar, both directions" turned into the test. Proven GREEN by execution over the canonical core (headings, paragraphs, flat unordered/ordered/GFM-task lists, fenced code; plain-text inlines). - ingest_markdown_source / ingest_markdown_source_with: fence-aware line grouping into top-level blocks, per-block dispatch on the leading spelling ROW (not an inlined literal), inverse of serialize_markdown_source over the same rows. - markdown_medium_lossless: the §5.2 (B) per-medium decidability partition — the recovered core is tagged Lossless (extdeps.communication.medium); the frontier residue (inline markup, nested lists, tables, block quotes) stays the unclaimed Lossy partition rather than fabricated (§5 fail-closed honesty). Witness dsl/test/claim/markdown_roundtrip_test.dag, 4 teeth: 1. round-trip law over the core (ingest(emit(doc)) == doc); 2. row-shared both directions — emit AND ingest under a perturbed bullet row still round-trips (medium-as-Node guard #5496, ingest side); 3. discriminating — emit perturbed, ingest canonical MUST fail (proves the row is read, not hard-coded); 4. fidelity tag — recovered core advertised Lossless. Round-trip completeness is the medium-COMPLETENESS step (§5.2), a follow-on to the #5501 emit step, not a re-gate of it. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * WIP: Emission slice: implement the §5.2 round-trip law (ingest-of-emit per me * emission(§5.2): address review — read block_separator row, executable fidelity boundary Review #5525 (claude/opus-4-7) fixes: - string_contains call aligned to the single-authority convention `string_contains(s:, pattern:)` (was positional) — md_is_digit. - md_split_blocks now READS `sp.block_separator` (strip the one trailing EOF newline, split on the separator row) instead of hard-coding blank-line grouping. block_separator is now genuinely row-shared in both directions; the fence-aware grouper is gone (code bodies with an embedded separator are the documented Lossy frontier). Honest ROW-SHARING LEDGER added: the rows shared AND exercised over the core are enumerated; list_indent (nesting) and the inline/table/blockquote spellings are named as frontier, not claimed. - Witness widened to perturb TWO independent rows (unordered_bullet AND block_separator) for both the round-trip-under-perturbation tooth and the discriminating tooth — the row-sharing claim is no longer inert against any single non-bullet row (DESIGN §5 inert-lens guard). - New tooth: the Lossy frontier is now EXECUTABLE — an emphasis-bearing doc is proven to NOT round-trip, so the boundary is enforced by execution, not just asserted in a comment (catches a silent core→frontier overclaim). All 5 teeth green by execution; emit keystone unaffected. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * WIP: Emission slice: implement the §5.2 round-trip law (ingest-of-emit per me * WIP: Emission slice: implement the §5.2 round-trip law (ingest-of-emit per me * chore(emission): revert auto-WIP GHA-expr contamination from the markdown PR The auto-WIP committer swept the in-progress SECOND-medium work (GHA `${{ }}` expression round-trip: dsl/extdeps/github/expressions.dag refactor + ingest, and its witness) onto this markdown round-trip branch. That snapshot did not compile (a since-fixed Optional if-branch type error) and shipped ingest code without its witness. This restores expressions.dag to main and drops the stray test so this PR's squash diff is markdown-ONLY again (the signed, green 077ed2b content). The GHA-expr round-trip slice moves to its own branch + PR. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
What
Adds §5.2 to
docs/plans/emission-ingestion-inverse.md, completing the formalization of the medium-as-Node rule (operator's "if we could formalize this, it would be ideal" ask). §5.1 gave the detector (finds a leak after the fact = validation); §5.2 adds the two mechanisms that make the rule constructive:(A) The round-trip law as the single oracle — a medium is properly modeled iff
ingest ∘ emit = idholds over the same grammar rows (DecodeFidelitymarks whereLossless). The test becomes structural ("is there a round-trip over shared rows?") instead of heuristic ("does it grep target syntax?"). Hand-rolledserialize_yamlfails it (no shared-row ingest — confirmed hand-rolled-inline 2026-06-22); deep-newt's row-drivenserialize_markdown_source(#5501) passes it. This is the emission-lane acceptance test for a new medium target (quick-seal-137 owns it): a target row-set is done iff its round-trip is green by execution, not iff it merely emits.(B) The per-medium decidability partition — not a blanket ban on string ops (that's the "never" trap, and it would wall the realization edge itself). Per medium: ① wall where there's a closed grammar + round-trip (inline syntax unwritable); ② flag a hand-rolled-but-closeable emitter on the shrinking roster (
serialize_yaml, markdown IR→HTML today); ③ fence (DecodeFidelity = lossy) where the grammar is genuinely open. Each decidable, so the guard never masquerades undecidable residue as a wall.Composition: detector finds → oracle proves clean → partition decides where walled now. Bounds the guard against both the "never" trap (§5 of DESIGN) and the purity trap (§6).
Scope
Docs-only, single file, +49 lines. No
.dag/.rs. Consistent with #5496 (§5.1), #5500 (the MediumStructureLeak lens), and #5502 (the ci.yml-is-a-serializer-fold correction).🤖 Generated with Claude Code