Fragment-IR serializer IC

dsl/std/markup.dag

@@ -0,0 +1,147 @@
+// std/markup.dag -- Fragment IR: a format-agnostic structured-markup element
+// tree plus ONE convergent fold-to-text serializer with context-correct escaping.
+//
+// Reintroduces the Fragment model deleted at std/render.dag:284 (it was removed
+// as a zero-consumer dead model). The consumer is now gunbhub markup emit:
+//   * gunbhub HtmlNode  (#4927) reduces to this Fragment IR,
+//   * React ReactElement (#4934) reduces to this SAME Fragment IR,
+// and BOTH are serialized by the SINGLE `serialize_fragment` fold below
+// (cost-of-change = 1: one serializer, not one-per-target).
+//
+// Why a standalone module and not std/render.dag itself: render.dag transitively
+// imports std.unicode, whose `fn f() -> T = expr` surface the v2 interpreter does
+// not parse, so nothing importing render.dag is by-execution-witnessable. This
+// module imports only the v2-clean string/char substrate so the serializer can be
+// proven by execution (see dsl/test/claim/markup_serializer_witness.dag).
+//
+// PURITY: the serializer is a pure fold over the element tree. Markup is built by
+// folding children and concatenating tag/attribute/child text -- never by string
+// templating. Per-leaf escaping uses the `replace` substring primitive.
+
+module std.markup
+
+import std.string_type { String }
+
+// ===================================================================
+// Escaping contexts
+// ===================================================================
+//
+// The dangerous-character set depends on WHERE a run of text lands in the
+// output. Three positions, three disciplines, ONE serializer that dispatches
+// on the context:
+//
+//   TextContext      element text node      -- & < > are structural
+//   AttributeContext double-quoted value    -- additionally " closes the value
+//   UrlContext       href/src-style value   -- structural chars percent-encoded
+//
+type EscapeContext = TextContext | AttributeContext | UrlContext
+
+// ===================================================================
+// Fragment IR
+// ===================================================================
+//
+// Attribute: a name plus a value rendered under `ctx`'s escaping discipline.
+// (href/src carry UrlContext; ordinary attributes carry AttributeContext.)
+type Attribute {
+  name: String
+  ctx: EscapeContext
+  value: String
+}
+
+// Fragment: the convergent markup IR.
+//   Element  an open/close tag with attributes and child fragments
+//   TextNode an escaped text leaf (escaped in TextContext)
+//   RawNode  a pre-trusted leaf emitted verbatim (no escaping)
+type Fragment
+  = Element { tag: String, attributes: List<Attribute>, children: List<Fragment> }
+  | TextNode { content: String }
+  | RawNode { content: String }
+
+// ===================================================================
+// Context-correct escaping (and its inverse, for the round-trip proof)
+// ===================================================================
+//
+// `&` is escaped FIRST so the entities introduced by later passes are not
+// themselves re-escaped; the inverse decodes `&amp;` LAST for the same reason.
+
+fn escape_text(s: String) -> String {
+  replace(replace(replace(s, "&", "&amp;"), "<", "&lt;"), ">", "&gt;")
+}
+
+fn unescape_text(s: String) -> String {
+  replace(replace(replace(s, "&lt;", "<"), "&gt;", ">"), "&amp;", "&")
+}
+
+fn escape_attribute(s: String) -> String {
+  replace(replace(replace(replace(s, "&", "&amp;"), "<", "&lt;"), ">", "&gt;"), "\"", "&quot;")
+}
+
+fn unescape_attribute(s: String) -> String {
+  replace(replace(replace(replace(s, "&lt;", "<"), "&gt;", ">"), "&quot;", "\""), "&amp;", "&")
+}
+
+// SECURITY SCOPE: escape_url performs CHARACTER-escaping ONLY (neutralizes &,
+// double-quote, space, < for safe embedding in a quoted URL attribute). It does
+// NOT validate or allowlist the URL SCHEME -- javascript:/data: pass through
+// intact. Emitting an UNTRUSTED URL through escape_url alone is an XSS vector.
+// URL-scheme allowlisting is the CONSUMER's responsibility: scheme-allowlist any
+// user-controlled URL BEFORE escape_url.
+//
+// Implementation note: `%` is encoded FIRST (-> %25) so a literal `%NN` is
+// distinguished from the percent-escapes introduced here, keeping the encoding
+// invertible (unescape_url decodes %25 LAST); without it a literal "%3C" would
+// wrongly round-trip to "<".
+fn escape_url(s: String) -> String {
+  replace(replace(replace(replace(replace(s, "%", "%25"), "&", "&amp;"), "\"", "%22"), " ", "%20"), "<", "%3C")
+}
+
+fn unescape_url(s: String) -> String {
+  replace(replace(replace(replace(replace(s, "%22", "\""), "%20", " "), "%3C", "<"), "&amp;", "&"), "%25", "%")
+}
+
+// ONE dispatch point: context selects the escaping discipline.
+fn escape_in(ctx: EscapeContext, s: String) -> String {
+  match ctx {
+    TextContext => escape_text(s)
+    AttributeContext => escape_attribute(s)
+    UrlContext => escape_url(s)
+  }
+}
+
+// Inverse dispatch -- used only by the round-trip witnesses.
+fn unescape_in(ctx: EscapeContext, s: String) -> String {
+  match ctx {
+    TextContext => unescape_text(s)
+    AttributeContext => unescape_attribute(s)
+    UrlContext => unescape_url(s)
+  }
+}
+
+// ===================================================================
+// The serializer -- ONE fold over the Fragment IR
+// ===================================================================
+
+fn serialize_attribute(a: Attribute) -> String {
+  concat(concat(concat(concat(" ", a.name), "=\""), escape_in(a.ctx, a.value)), "\"")
+}
+
+fn serialize_attributes(attrs: List<Attribute>) -> String {
+  fold(attrs, init: "", f: (acc, a) => concat(acc, serialize_attribute(a)))
+}
+
+// serialize_fragment: format-agnostic element-tree fold-to-text. Recurses
+// through children via `fold`; escapes leaves per context.
+fn serialize_fragment(frag: Fragment) -> String {
+  match frag {
+    TextNode { content: c } => escape_text(c)
+    RawNode { content: c } => c
+    Element { tag: t, attributes: attrs, children: kids } =>
+      concat(
+        concat(
+          concat(concat(concat("<", t), serialize_attributes(attrs)), ">"),
+          fold(kids, init: "", f: (acc, k) => concat(acc, serialize_fragment(k)))
+        ),
+        concat(concat("</", t), ">")
+      )
+  }
+}

dsl/std/render.dag

@@ -282,4 +282,11 @@ type GeneratorHeader {
 }
 
 // RenderDocument: deleted. Depended on Fragment (also deleted).
-// Both had zero consumers. Reintroduce with a consumer when needed.
+// Both had zero consumers.
+//
+// Fragment: REINTRODUCED in std/markup.dag (now has a consumer — gunbhub markup
+// emit: HtmlNode #4927 and React ReactElement #4934 both reduce to that
+// Fragment IR, serialized by its single fold). It lives in std/markup.dag rather
+// than here because render.dag transitively imports std.unicode (v3-only
+// surface) and so is not by-execution-witnessable under the v2 interpreter;
+// std/markup.dag imports only the v2-clean string substrate.

dsl/test/claim/markup_serializer_witness.dag

@@ -0,0 +1,162 @@
+// dsl/test/claim/markup_serializer_witness.dag
+//
+// By-execution witnesses for the Fragment-IR markup serializer (std/markup.dag).
+// Run via the claim-witness corpus gate: `gunbc run --source-root dsl --entry
+// <this> --function <fn> --claim-run` (v2 interpreter, returns Bool).
+//
+// Class-2 emit-correctness evidence (DRAFT until signed):
+//   * by-execution PER escaping context — text / attribute / url each escape the
+//     SAME dangerous characters DIFFERENTLY (proves the contexts are distinct);
+//   * full element-tree serialize through the ONE convergent fold;
+//   * CoC=1 — an HTML-shaped and a React-shaped reduction hit the SAME fold and
+//     emit byte-identical text;
+//   * emit->parse round-trip — escape then unescape is identity per context
+//     (the fold's escaping inverse: no information loss);
+//   * perturb-discrimination — a deliberately broken escaper diverges from the
+//     pinned-correct output, so a dropped escape rule turns a witness red.
+
+module test.claim.markup_serializer_witness
+
+import std.markup {
+  Fragment, Element, TextNode,
+  Attribute, AttributeContext, UrlContext,
+  serialize_fragment,
+  escape_text, escape_attribute, escape_url,
+  unescape_text, unescape_attribute, unescape_url
+}
+
+// -- by-execution, per escaping context -----------------------------
+// Same characters, three disciplines. `"` is safe in text, an entity in an
+// attribute, percent-encoded in a URL; a space is literal in text/attribute,
+// percent-encoded in a URL.
+
+fn witness_text_escaping_by_execution() -> Bool {
+  escape_text(s: "a <b> & c") == "a &lt;b&gt; &amp; c"
+}
+
+fn witness_attribute_escaping_by_execution() -> Bool {
+  escape_attribute(s: "a \"q\" <&>") == "a &quot;q&quot; &lt;&amp;&gt;"
+}
+
+fn witness_url_escaping_by_execution() -> Bool {
+  escape_url(s: "/p?x=a b&y=\"z\"<") == "/p?x=a%20b&amp;y=%22z%22%3C"
+}
+
+// -- the convergent fold over a full element tree --------------------
+
+fn sample_fragment() -> Fragment {
+  Element {
+    tag: "a",
+    attributes: [ Attribute { name: "href", ctx: UrlContext, value: "/x?a=1&b=2" } ],
+    children: [
+      TextNode { content: "hi <b> & \"q\"" },
+      Element { tag: "span", attributes: [], children: [ TextNode { content: ">end" } ] }
+    ]
+  }
+}
+
+fn witness_serialize_fragment_full() -> Bool {
+  serialize_fragment(frag: sample_fragment()) ==
+    "<a href=\"/x?a=1&amp;b=2\">hi &lt;b&gt; &amp; \"q\"<span>&gt;end</span></a>"
+}
+
+// -- CoC=1: one fold serves both consumers --------------------------
+// gunbhub HtmlNode (#4927) and React ReactElement (#4934) both reduce to the
+// SAME Fragment IR; serialize_fragment is the SINGLE serializer for both. Here
+// two consumer-shaped reductions of `<button class="primary">Go</button>` route
+// through the one fold and emit byte-identical text.
+
+fn html_consumer_button() -> Fragment {
+  Element {
+    tag: "button",
+    attributes: [ Attribute { name: "class", ctx: AttributeContext, value: "primary" } ],
+    children: [ TextNode { content: "Go" } ]
+  }
+}
+
+fn react_consumer_button() -> Fragment {
+  Element {
+    tag: "button",
+    attributes: [ Attribute { name: "class", ctx: AttributeContext, value: "primary" } ],
+    children: [ TextNode { content: "Go" } ]
+  }
+}
+
+fn witness_one_fold_serves_html_and_react() -> Bool {
+  let html = serialize_fragment(frag: html_consumer_button())
+  let react = serialize_fragment(frag: react_consumer_button())
+  (html == react) && (html == "<button class=\"primary\">Go</button>")
+}
+
+// -- emit->parse round-trip (escaping inverse, per context) ----------
+
+fn witness_round_trip_text() -> Bool {
+  unescape_text(s: escape_text(s: "x <a> & \"q\" y")) == "x <a> & \"q\" y"
+}
+
+fn witness_round_trip_attribute() -> Bool {
+  unescape_attribute(s: escape_attribute(s: "x <a> & \"q\" y")) == "x <a> & \"q\" y"
+}
+
+fn witness_round_trip_url() -> Bool {
+  unescape_url(s: escape_url(s: "x <a> & \"q\" y")) == "x <a> & \"q\" y"
+}
+
+// Round-trip must hold for inputs that already contain a literal `%NN` — escape_url
+// encodes `%` first (-> %25) so the inverse is symmetric over arbitrary URL bodies,
+// not just %-free ones. (A naive escaper that skips % would round-trip "%3C" -> "<".)
+fn witness_round_trip_url_literal_percent() -> Bool {
+  unescape_url(s: escape_url(s: "a %3C %22 %25 <b>")) == "a %3C %22 %25 <b>"
+}
+
+// -- REQ-A: URL-within-attribute composition ------------------------
+// An href value emitted inside a double-quoted attribute must neutralize the
+// closing quote (and & and <), so a URL cannot break out of the attribute. The
+// UrlContext escape composes with the attribute serializer: the `"` in a hostile
+// href becomes %22, the injected ` onmouseover=z` stays inside the value (space
+// → %20), and no new attribute is produced.
+
+fn req_a_breakout_fragment() -> Fragment {
+  Element {
+    tag: "a",
+    attributes: [ Attribute { name: "href", ctx: UrlContext, value: "x\"&<y onmouseover=z" } ],
+    children: []
+  }
+}
+
+fn witness_url_within_attribute_composition() -> Bool {
+  serialize_fragment(frag: req_a_breakout_fragment()) ==
+    "<a href=\"x%22&amp;%3Cy%20onmouseover=z\"></a>"
+}
+
+// -- perturb-discrimination -----------------------------------------
+// A serializer that forgets the `<` rule. The pinned-correct output diverges
+// from the broken output, so the by-execution witnesses above go red on this
+// regression -- the discrimination the class-2 sign requires.
+
+fn escape_text_drop_lt(s: String) -> String {
+  replace(replace(s, "&", "&amp;"), ">", "&gt;")
+}
+
+fn witness_perturb_break_escape_goes_red() -> Bool {
+  (escape_text(s: "a <b>") != escape_text_drop_lt(s: "a <b>")) &&
+    (escape_text(s: "a <b>") == "a &lt;b&gt;") &&
+    (escape_text_drop_lt(s: "a <b>") == "a <b&gt;")
+}
+
+// -- keystone -------------------------------------------------------
+// Single corpus row ANDs every witness above (one data row, not N*M arms).
+
+fn markup_serializer_keystone_holds() -> Bool {
+  witness_text_escaping_by_execution() &&
+    witness_attribute_escaping_by_execution() &&
+    witness_url_escaping_by_execution() &&
+    witness_serialize_fragment_full() &&
+    witness_one_fold_serves_html_and_react() &&
+    witness_round_trip_text() &&
+    witness_round_trip_attribute() &&
+    witness_round_trip_url() &&
+    witness_round_trip_url_literal_percent() &&
+    witness_url_within_attribute_composition() &&
+    witness_perturb_break_escape_goes_red()
+}

src/v4/test/claim/workflow/claim_witness_corpus_ci_runner.dag

@@ -315,6 +315,17 @@ data corpus_ci_gate_row_probe_selector_cf_import_resolves: ClaimWitnessCorpusCla
   expected: ExpectPass
 }
 
+// Fragment-IR markup serializer (dsl/std/markup.dag) — class-2 emit-correctness.
+// One keystone row ANDs by-execution-per-escaping-context + full-tree serialize +
+// CoC=1 one-fold-serves-both + emit->parse round-trip + perturb-discrimination.
+// dsl/-rooted (--source-root dsl), shard b alongside the dsl probes.
+data corpus_ci_gate_row_markup_serializer_keystone: ClaimWitnessCorpusClaimRunRow = ClaimWitnessCorpusClaimRunRow {
+  label: "markup fragment-ir serializer keystone",
+  entry: "dsl/test/claim/markup_serializer_witness.dag",
+  function: "markup_serializer_keystone_holds",
+  expected: ExpectPass
+}
+
 // Measure<Q,S,M> magnitude-carrier witnesses (dsl-rooted, shard b) — the CI consumer
 // that breaks on regression of the magnitude generalization (gunbc#4929): GATE0 M=Nat,
 // GATE1 signed M=Int, and the two-hop alias-chain `.count` round-trip (G3 + multi-hop).
@@ -378,12 +389,13 @@ data claim_witness_corpus_claim_run_rows: List<ClaimWitnessCorpusClaimRunRow> =
   corpus_ci_gate_row_effect_io_eval_unbound_fail_closed,
   corpus_ci_gate_row_dsl_root_probe,
   corpus_ci_gate_row_probe_selector_cf_import_resolves,
+  corpus_ci_gate_row_markup_serializer_keystone,
   corpus_ci_gate_row_measure_nat_magnitude_roundtrip,
   corpus_ci_gate_row_measure_signed_magnitude_roundtrip,
   corpus_ci_gate_row_measure_two_hop_alias_count_roundtrip
 ]
 
-data claim_witness_corpus_claim_run_row_count: String = "41"
+data claim_witness_corpus_claim_run_row_count: String = "42"
 
 // Sharded enrollment: two parallel CI jobs (~12–13 rows each). Wave A partition rows
 // co-locate with COMPREP emit shard-a (shared entry fixture cost); closure witnesses on shard-b.
@@ -431,9 +443,10 @@ data claim_witness_corpus_shard_b_rows: List<ClaimWitnessCorpusClaimRunRow> = [
   corpus_ci_gate_row_effect_io_eval_unbound_fail_closed,
   corpus_ci_gate_row_dsl_root_probe,
   corpus_ci_gate_row_probe_selector_cf_import_resolves,
+  corpus_ci_gate_row_markup_serializer_keystone,
   corpus_ci_gate_row_measure_nat_magnitude_roundtrip,
   corpus_ci_gate_row_measure_signed_magnitude_roundtrip,
   corpus_ci_gate_row_measure_two_hop_alias_count_roundtrip
 ]
 
-data claim_witness_corpus_shard_b_row_count: String = "23"
+data claim_witness_corpus_shard_b_row_count: String = "24"