diff --git a/dsl/std/markup.dag b/dsl/std/markup.dag new file mode 100644 index 00000000000..606af8a9f17 --- /dev/null +++ b/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, children: List } + | 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 `&` LAST for the same reason. + +fn escape_text(s: String) -> String { + replace(replace(replace(s, "&", "&"), "<", "<"), ">", ">") +} + +fn unescape_text(s: String) -> String { + replace(replace(replace(s, "<", "<"), ">", ">"), "&", "&") +} + +fn escape_attribute(s: String) -> String { + replace(replace(replace(replace(s, "&", "&"), "<", "<"), ">", ">"), "\"", """) +} + +fn unescape_attribute(s: String) -> String { + replace(replace(replace(replace(s, "<", "<"), ">", ">"), """, "\""), "&", "&") +} + +// 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"), "&", "&"), "\"", "%22"), " ", "%20"), "<", "%3C") +} + +fn unescape_url(s: String) -> String { + replace(replace(replace(replace(replace(s, "%22", "\""), "%20", " "), "%3C", "<"), "&", "&"), "%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) -> 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("") + ) + } +} diff --git a/dsl/std/render.dag b/dsl/std/render.dag index 7e159d0d819..994718e4695 100644 --- a/dsl/std/render.dag +++ b/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. diff --git a/dsl/test/claim/markup_serializer_witness.dag b/dsl/test/claim/markup_serializer_witness.dag new file mode 100644 index 00000000000..ff703bdc25f --- /dev/null +++ b/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 +// --function --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 & c") == "a <b> & c" +} + +fn witness_attribute_escaping_by_execution() -> Bool { + escape_attribute(s: "a \"q\" <&>") == "a "q" <&>" +} + +fn witness_url_escaping_by_execution() -> Bool { + escape_url(s: "/p?x=a b&y=\"z\"<") == "/p?x=a%20b&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 & \"q\"" }, + Element { tag: "span", attributes: [], children: [ TextNode { content: ">end" } ] } + ] + } +} + +fn witness_serialize_fragment_full() -> Bool { + serialize_fragment(frag: sample_fragment()) == + "hi <b> & \"q\">end" +} + +// -- 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 `` 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 == "") +} + +// -- emit->parse round-trip (escaping inverse, per context) ---------- + +fn witness_round_trip_text() -> Bool { + unescape_text(s: escape_text(s: "x & \"q\" y")) == "x & \"q\" y" +} + +fn witness_round_trip_attribute() -> Bool { + unescape_attribute(s: escape_attribute(s: "x & \"q\" y")) == "x & \"q\" y" +} + +fn witness_round_trip_url() -> Bool { + unescape_url(s: escape_url(s: "x & \"q\" y")) == "x & \"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 ")) == "a %3C %22 %25 " +} + +// -- 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\"& Bool { + serialize_fragment(frag: req_a_breakout_fragment()) == + "" +} + +// -- 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, "&", "&"), ">", ">") +} + +fn witness_perturb_break_escape_goes_red() -> Bool { + (escape_text(s: "a ") != escape_text_drop_lt(s: "a ")) && + (escape_text(s: "a ") == "a <b>") && + (escape_text_drop_lt(s: "a ") == "a 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() +} diff --git a/src/v4/test/claim/workflow/claim_witness_corpus_ci_runner.dag b/src/v4/test/claim/workflow/claim_witness_corpus_ci_runner.dag index 42f5f371f36..bac224f39dd 100644 --- a/src/v4/test/claim/workflow/claim_witness_corpus_ci_runner.dag +++ b/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 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 = 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 = [ 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"