From 8ec43806584d34fa78f97119543b48e8e53d456b Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 23 Jun 2026 18:30:34 +0000 Subject: [PATCH 1/9] WIP: S2: gunbhub react/html SERVE page green-by-exec via gunbc-run program + --- dsl/extdeps/languages/html.dag | 14 +++++ dsl/gunbc/gunbhub_serve.dag | 104 +++++++++++++++++++++++++++------ 2 files changed, 100 insertions(+), 18 deletions(-) diff --git a/dsl/extdeps/languages/html.dag b/dsl/extdeps/languages/html.dag index 31053fcd7e0..5a2781b0cdc 100644 --- a/dsl/extdeps/languages/html.dag +++ b/dsl/extdeps/languages/html.dag @@ -9,6 +9,7 @@ import std.markup { unescape_text, unescape_attribute, unescape_url, validate_href, SafeHref, RejectedHref, attr_is_url_attr, + find_first_rejected_url, } data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority { @@ -307,3 +308,16 @@ fn ingest_html_source(src: String) -> HtmlIngestResult { fn html_medium_lossless(node: MarkupNode) -> Medium { Medium { carried: node, fidelity: Lossless } } + +type HtmlEmitResult + = EmitOk { html: String } + | EmitRejected { reason: String } + +fn try_serialize_html_source(node: MarkupNode) -> HtmlEmitResult { + match find_first_rejected_url(node: node) { + Present { value: r } => + EmitRejected { reason: r.url } + Absent => + EmitOk { html: serialize_html_source(node: node) } + } +} diff --git a/dsl/gunbc/gunbhub_serve.dag b/dsl/gunbc/gunbhub_serve.dag index da11b3dae1e..5b8b4608690 100644 --- a/dsl/gunbc/gunbhub_serve.dag +++ b/dsl/gunbc/gunbhub_serve.dag @@ -14,11 +14,10 @@ import std.markup { MarkupAttr, MarkupNode, } -import std.react_markup { +import extdeps.languages.html { EmitOk, EmitRejected, - UntrustedUrlScheme, - serialize_react_markup, + try_serialize_html_source, } import extdeps.http.server { HttpServerRoute, @@ -56,14 +55,39 @@ type GunbhubRenderResult = RenderedHtml { html: String } | RenderRejected { reason: String } -fn gunbhub_browse_entry(name: String) -> MarkupNode { +fn gunbhub_header() -> MarkupNode { + ElementNode { + tag: "header", + attrs: [], + children: [ + ElementNode { + tag: "h1", + attrs: [], + children: [ TextNode { text: "gunbc" } ], + }, + ElementNode { + tag: "nav", + attrs: [], + children: [ + ElementNode { + tag: "a", + attrs: [ MarkupAttr { name: "href", value: "/" } ], + children: [ TextNode { text: "Browse" } ], + }, + ], + }, + ], + } +} + +fn gunbhub_browse_entry(name: String, path: String) -> MarkupNode { ElementNode { tag: "li", attrs: [], children: [ ElementNode { tag: "a", - attrs: [], + attrs: [ MarkupAttr { name: "href", value: path } ], children: [ TextNode { text: name } ], }, ], @@ -72,21 +96,40 @@ fn gunbhub_browse_entry(name: String) -> MarkupNode { fn gunbhub_browse_page() -> MarkupNode { ElementNode { - tag: "div", + tag: "html", attrs: [], children: [ ElementNode { - tag: "h1", + tag: "head", attrs: [], - children: [ TextNode { text: "gunbc" } ], + children: [ + ElementNode { + tag: "title", + attrs: [], + children: [ TextNode { text: "gunbc" } ], + }, + ], }, ElementNode { - tag: "ul", + tag: "body", attrs: [], children: [ - gunbhub_browse_entry(name: "dsl"), - gunbhub_browse_entry(name: "src"), - gunbhub_browse_entry(name: "ROADMAP.md"), + gunbhub_header(), + ElementNode { + tag: "main", + attrs: [], + children: [ + ElementNode { + tag: "ul", + attrs: [], + children: [ + gunbhub_browse_entry(name: "dsl", path: "/dsl"), + gunbhub_browse_entry(name: "src", path: "/src"), + gunbhub_browse_entry(name: "ROADMAP.md", path: "/ROADMAP.md"), + ], + }, + ], + }, ], }, ], @@ -103,20 +146,45 @@ fn gunbhub_hostile_page() -> MarkupNode { fn gunbhub_readme_page() -> MarkupNode { ElementNode { - tag: "article", + tag: "html", attrs: [], children: [ ElementNode { - tag: "h1", + tag: "head", attrs: [], - children: [ TextNode { text: "gunbc" } ], + children: [ + ElementNode { + tag: "title", + attrs: [], + children: [ TextNode { text: "gunbc — README" } ], + }, + ], }, ElementNode { - tag: "p", + tag: "body", attrs: [], children: [ - TextNode { - text: "DAG-modeled compiler and language project. Rust is bootstrap seed.", + gunbhub_header(), + ElementNode { + tag: "main", + attrs: [], + children: [ + ElementNode { + tag: "article", + attrs: [], + children: [ + ElementNode { + tag: "p", + attrs: [], + children: [ + TextNode { + text: "DAG-modeled compiler and language project. Rust is bootstrap seed.", + }, + ], + }, + ], + }, + ], }, ], }, From a165839455ccc0291829bcf0db25b4b1f0077691 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 23 Jun 2026 18:34:38 +0000 Subject: [PATCH 2/9] =?UTF-8?q?S2:=20gunbhub=20SERVE=20page=20green-by-exe?= =?UTF-8?q?c=20=E2=80=94=20try=5Fserialize=5Fhtml=5Fsource=20+=20full=20pa?= =?UTF-8?q?ge=20+=20W-A/W-B=20witnesses?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - Add try_serialize_html_source(node) -> HtmlEmitResult to extdeps.languages.html (composes serialize_html_source with find_first_rejected_url, the single §3 authority) - Promote gunbhub_browse_page / gunbhub_readme_page to full html/head/body/header/nav/main pages with real hrefs; gunbhub_browse_entry gains path: String param - Repoint both gunbhub serve entry points (gunbhub_serve.dag + gunbhub_serve_html.dag) from serialize_react_markup / try_serialize_html_node to try_serialize_html_source - gunbhub_served_static_route_table is row-driven: calls try_serialize_html_source per row - Delete std.react_markup (all consumers repointed; do NOT delete serialize_fragment/markup_node — shared with markdown) - react_markup_witness_test.dag → html_emit_witness; gunbhub browse/serve witnesses repointed - Add func main() -> ProcessExit serve program with W-A (unknown path → RouteNotFound) and W-B (unsafe href → EmitRejected; RED-ON-REMOVAL if try_ wrapper removed) discriminating witnesses - Add Rust test gunbhub_serve_program_test.rs mirroring html_markup_smoke_test pattern - Honest deferral: gunbhub serves the modeled HTTP response by execution (gunbc-run, exit-checked on served bytes); binds a real socket when Lane C emits the server to a host language All three claim witnesses (html_emit_keystone_holds, gunbhub_browse_keystone_holds, gunbhub_serve_keystone_holds) return true; func main() returns ExitSuccess — green-by-execution. Co-Authored-By: Claude Sonnet 4.6 --- .../gunbhub_serve_program.dag | 78 +++++++++++++++++++ dsl/gunbc/gunbhub_serve.dag | 20 ++--- dsl/gunbc/gunbhub_serve_html.dag | 14 ++-- dsl/std/react_markup.dag | 22 ------ .../gunbhub_react_browse_witness_test.dag | 8 +- dsl/test/claim/gunbhub_serve_witness_test.dag | 5 -- dsl/test/claim/react_markup_witness_test.dag | 39 +++++----- .../tests/src/gunbhub_serve_program_test.rs | 48 ++++++++++++ src/v1/tests/src/lib.rs | 2 + 9 files changed, 166 insertions(+), 70 deletions(-) create mode 100644 dsl/examples/gunbhub_serve_program/gunbhub_serve_program.dag delete mode 100644 dsl/std/react_markup.dag create mode 100644 src/v1/tests/src/gunbhub_serve_program_test.rs diff --git a/dsl/examples/gunbhub_serve_program/gunbhub_serve_program.dag b/dsl/examples/gunbhub_serve_program/gunbhub_serve_program.dag new file mode 100644 index 00000000000..316356dbb5a --- /dev/null +++ b/dsl/examples/gunbhub_serve_program/gunbhub_serve_program.dag @@ -0,0 +1,78 @@ +module examples.gunbhub_serve_program + +import gunbc.gunbhub_serve { + GunbhubServeRequest, + GunbhubPageSource, + ReactPage, + Served, + RenderRejectedBeforeServe, + RouteNotFound, + MethodNotAllowed, + gunbhub_hostile_page, + serve_gunbhub_request, + serve_gunbhub_page_source, +} +import extdeps.languages.html { + try_serialize_html_source, + EmitOk, + EmitRejected, +} +import std.process { ProcessExit, ExitSuccess, ExitFailure, exit_code_general_error } +import std.types { GET } + +fn wa_unknown_path_is_not_found() -> Bool { + match serve_gunbhub_request( + req: GunbhubServeRequest { method: GET, path: "/unknown/nonexistent" } + ) { + RouteNotFound => true + Served { response: _ } => false + RenderRejectedBeforeServe { reason: _ } => false + MethodNotAllowed => false + } +} + +fn wb_unsafe_href_is_rejected() -> Bool { + match try_serialize_html_source(node: gunbhub_hostile_page()) { + EmitRejected { reason: _ } => true + EmitOk { html: _ } => false + } +} + +fn wb_unsafe_href_rejected_before_serve() -> Bool { + match serve_gunbhub_page_source( + source: ReactPage { node: gunbhub_hostile_page() } + ) { + RenderRejectedBeforeServe { reason: _ } => true + Served { response: _ } => false + RouteNotFound => false + MethodNotAllowed => false + } +} + +fn browse_root_serves_200() -> Bool { + match serve_gunbhub_request( + req: GunbhubServeRequest { method: GET, path: "/" } + ) { + Served { response: r } => r.status == 200 && r.body != "" + RouteNotFound => false + RenderRejectedBeforeServe { reason: _ } => false + MethodNotAllowed => false + } +} + +data honest_deferral: String = "gunbhub serves the modeled HTTP response by execution (gunbc-run, exit-checked on served bytes); binds a real socket when Lane C emits the server to a host language" + +func main() -> ProcessExit { + if wa_unknown_path_is_not_found() + && wb_unsafe_href_is_rejected() + && wb_unsafe_href_rejected_before_serve() + && browse_root_serves_200() + { + ExitSuccess + } else { + ExitFailure { + code: exit_code_general_error, + reason: "gunbhub serve program assertion failed", + } + } +} diff --git a/dsl/gunbc/gunbhub_serve.dag b/dsl/gunbc/gunbhub_serve.dag index 5b8b4608690..269d4647ebf 100644 --- a/dsl/gunbc/gunbhub_serve.dag +++ b/dsl/gunbc/gunbhub_serve.dag @@ -197,10 +197,9 @@ type GunbhubComposeResult | ComposeRejected { reason: String } fn gunbhub_compose_body(node: MarkupNode) -> GunbhubComposeResult { - match serialize_react_markup(node: node) { + match try_serialize_html_source(node: node) { EmitOk { html: h } => ComposedOk { html: h } - EmitRejected { reason: UntrustedUrlScheme { url: u } } => - ComposeRejected { reason: concat("react markup rejected: ", u) } + EmitRejected { reason: r } => ComposeRejected { reason: r } } } @@ -282,10 +281,9 @@ fn path_matches_template(template: PathTemplate, path: String) -> Bool { fn render_gunbhub_page(source: GunbhubPageSource) -> GunbhubRenderResult { match source { ReactPage { node } => - match serialize_react_markup(node: node) { + match try_serialize_html_source(node: node) { EmitOk { html: h } => RenderedHtml { html: h } - EmitRejected { reason: UntrustedUrlScheme { url: u } } => - RenderRejected { reason: concat("react markup rejected: ", u) } + EmitRejected { reason: r } => RenderRejected { reason: r } } } } @@ -352,12 +350,10 @@ fn gunbhub_served_static_route_table() -> ServedStaticRouteTable { xs: gunbhub_route_table(), init: [], f: (acc, row) => - match gunbhub_compose_body( - node: match row.page { - ReactPage { node: n } => n - } + match try_serialize_html_source( + node: match row.page { ReactPage { node: n } => n } ) { - ComposedOk { html: h } => + EmitOk { html: h } => concat( acc, [ @@ -370,7 +366,7 @@ fn gunbhub_served_static_route_table() -> ServedStaticRouteTable { }, ] ) - ComposeRejected { reason: _ } => acc + EmitRejected { reason: _ } => acc } ) ServedStaticRouteTable { routes: routes } diff --git a/dsl/gunbc/gunbhub_serve_html.dag b/dsl/gunbc/gunbhub_serve_html.dag index b44e8472d5b..fc47fc5522f 100644 --- a/dsl/gunbc/gunbhub_serve_html.dag +++ b/dsl/gunbc/gunbhub_serve_html.dag @@ -2,13 +2,13 @@ module gunbc.gunbhub_serve_html import std.markup { MarkupNode, - Serialized, - Rejected, ElementNode, TextNode, } -import std.html_markup { - try_serialize_html_node, +import extdeps.languages.html { + try_serialize_html_source, + EmitOk, + EmitRejected, } fn sample_html_page() -> MarkupNode { @@ -20,9 +20,9 @@ fn sample_html_page() -> MarkupNode { } fn witness_html_consumer_serializes() -> Bool { - match try_serialize_html_node(node: sample_html_page()) { - Serialized { html: h } => h == "

gunbhub

" - Rejected { reason: _ } => false + match try_serialize_html_source(node: sample_html_page()) { + EmitOk { html: h } => h == "

gunbhub

" + EmitRejected { reason: _ } => false } } diff --git a/dsl/std/react_markup.dag b/dsl/std/react_markup.dag deleted file mode 100644 index 4596e422371..00000000000 --- a/dsl/std/react_markup.dag +++ /dev/null @@ -1,22 +0,0 @@ -module std.react_markup - -import std.markup { - MarkupNode, - find_first_rejected_url, - serialize_markup_node, -} - -type MarkupRejectReason = UntrustedUrlScheme { url: String } - -type MarkupEmitResult - = EmitOk { html: String } - | EmitRejected { reason: MarkupRejectReason } - -fn serialize_react_markup(node: MarkupNode) -> MarkupEmitResult { - match find_first_rejected_url(node: node) { - Present { value: ru } => - EmitRejected { reason: UntrustedUrlScheme { url: ru.url } } - Absent => - EmitOk { html: serialize_markup_node(node: node) } - } -} diff --git a/dsl/test/claim/gunbhub_react_browse_witness_test.dag b/dsl/test/claim/gunbhub_react_browse_witness_test.dag index 67013d4a7d2..121329f3ad0 100644 --- a/dsl/test/claim/gunbhub_react_browse_witness_test.dag +++ b/dsl/test/claim/gunbhub_react_browse_witness_test.dag @@ -1,14 +1,14 @@ module test.claim.gunbhub_react_browse_witness import gunbc.gunbhub_serve { gunbhub_browse_page } -import std.react_markup { +import extdeps.languages.html { EmitOk, EmitRejected, - serialize_react_markup, + try_serialize_html_source, } fn browse_page_html() -> String { - match serialize_react_markup(node: gunbhub_browse_page()) { + match try_serialize_html_source(node: gunbhub_browse_page()) { EmitOk { html: h } => h EmitRejected { reason: _ } => "" } @@ -18,7 +18,7 @@ data gunbhub_browse_html: String = browse_page_html() fn gunbhub_browse_page_serializes_holds() -> Bool { gunbhub_browse_html == - "

gunbc

" + "gunbc

gunbc

" } test fn gunbhub_browse_keystone_holds() -> Bool { diff --git a/dsl/test/claim/gunbhub_serve_witness_test.dag b/dsl/test/claim/gunbhub_serve_witness_test.dag index a2b5bb15464..4696683d97c 100644 --- a/dsl/test/claim/gunbhub_serve_witness_test.dag +++ b/dsl/test/claim/gunbhub_serve_witness_test.dag @@ -28,11 +28,6 @@ import gunbc.gunbhub_serve { import gunbc.gunbhub_serve_html { gunbhub_html_render_keystone_holds } import extdeps.http.server { http_content_type_wire_label } import std.markup { MarkupNode } -import std.react_markup { - EmitOk, - EmitRejected, - serialize_react_markup, -} import std.types { GET, POST } fn witness_compose_ok_html(node: MarkupNode) -> String { diff --git a/dsl/test/claim/react_markup_witness_test.dag b/dsl/test/claim/react_markup_witness_test.dag index d0bd064295d..4984ab5757c 100644 --- a/dsl/test/claim/react_markup_witness_test.dag +++ b/dsl/test/claim/react_markup_witness_test.dag @@ -1,4 +1,4 @@ -module test.claim.react_markup_witness +module test.claim.html_emit_witness import std.markup { ElementNode, @@ -7,11 +7,10 @@ import std.markup { MarkupNode, serialize_markup_node, } -import std.react_markup { +import extdeps.languages.html { EmitOk, EmitRejected, - UntrustedUrlScheme, - serialize_react_markup, + try_serialize_html_source, } fn sample_button() -> MarkupNode { @@ -22,15 +21,15 @@ fn sample_button() -> MarkupNode { } } -fn witness_react_consumer_reduces_and_serializes() -> Bool { - match serialize_react_markup(node: sample_button()) { +fn witness_html_emit_reduces_and_serializes() -> Bool { + match try_serialize_html_source(node: sample_button()) { EmitOk { html: h } => h == "" EmitRejected { reason: _ } => false } } -fn witness_react_fragment_matches_markup_fold() -> Bool { - match serialize_react_markup(node: sample_button()) { +fn witness_html_emit_matches_markup_fold() -> Bool { + match try_serialize_html_source(node: sample_button()) { EmitOk { html: h } => h == serialize_markup_node(node: sample_button()) EmitRejected { reason: _ } => false } @@ -53,7 +52,7 @@ fn hostile_data_href() -> MarkupNode { } fn witness_javascript_reject_discriminates_from_char_escape() -> Bool { - match serialize_react_markup(node: hostile_javascript_href()) { + match try_serialize_html_source(node: hostile_javascript_href()) { EmitRejected { reason: _ } => { let unchecked = serialize_markup_node(node: hostile_javascript_href()) unchecked == "click" @@ -63,7 +62,7 @@ fn witness_javascript_reject_discriminates_from_char_escape() -> Bool { } fn witness_data_reject_discriminates_from_char_escape() -> Bool { - match serialize_react_markup(node: hostile_data_href()) { + match try_serialize_html_source(node: hostile_data_href()) { EmitRejected { reason: _ } => { let unchecked = serialize_markup_node(node: hostile_data_href()) starts_with(s: unchecked, prefix: " Bool { } fn witness_serialize_rejects_javascript_href() -> Bool { - match serialize_react_markup(node: hostile_javascript_href()) { - EmitRejected { reason: UntrustedUrlScheme { url: u } } => + match try_serialize_html_source(node: hostile_javascript_href()) { + EmitRejected { reason: u } => u == "javascript:alert(1)" EmitOk { html: _ } => false } } fn witness_serialize_rejects_data_href() -> Bool { - match serialize_react_markup(node: hostile_data_href()) { - EmitRejected { reason: UntrustedUrlScheme { url: u } } => + match try_serialize_html_source(node: hostile_data_href()) { + EmitRejected { reason: u } => starts_with(s: u, prefix: "data:") EmitOk { html: _ } => false } } fn witness_http_href_serializes() -> Bool { - match serialize_react_markup( + match try_serialize_html_source( node: ElementNode { tag: "a", attrs: [ MarkupAttr { name: "href", value: "https://gunbc.dev" } ], @@ -118,23 +117,23 @@ fn req_a_hostile_but_trusted_scheme() -> MarkupNode { } fn witness_trusted_href_serializes() -> Bool { - match serialize_react_markup(node: trusted_relative_link()) { + match try_serialize_html_source(node: trusted_relative_link()) { EmitOk { html: h } => h == "dsl" EmitRejected { reason: _ } => false } } fn witness_req_a_hostile_href_still_emits_with_escaping() -> Bool { - match serialize_react_markup(node: req_a_hostile_but_trusted_scheme()) { + match try_serialize_html_source(node: req_a_hostile_but_trusted_scheme()) { EmitOk { html: h } => h == "" EmitRejected { reason: _ } => false } } -test fn react_markup_keystone_holds() -> Bool { - witness_react_consumer_reduces_and_serializes() - && witness_react_fragment_matches_markup_fold() +test fn html_emit_keystone_holds() -> Bool { + witness_html_emit_reduces_and_serializes() + && witness_html_emit_matches_markup_fold() && witness_javascript_reject_discriminates_from_char_escape() && witness_data_reject_discriminates_from_char_escape() && witness_serialize_rejects_javascript_href() diff --git a/src/v1/tests/src/gunbhub_serve_program_test.rs b/src/v1/tests/src/gunbhub_serve_program_test.rs new file mode 100644 index 00000000000..e917e24dc49 --- /dev/null +++ b/src/v1/tests/src/gunbhub_serve_program_test.rs @@ -0,0 +1,48 @@ +use crate::helpers::workspace_root; + +#[test] +fn gunbhub_serve_program_runs_green() { + let ws = workspace_root(); + let gunbc = ws.join("target/release/gunbc"); + if !gunbc.is_file() { + eprintln!( + "skipping gunbhub_serve_program_runs_green: release binary not found (run `cargo build --release -p v1-compiler` first)" + ); + return; + } + + let entry = ws.join("dsl/examples/gunbhub_serve_program/gunbhub_serve_program.dag"); + let program_root = ws.join("dsl/examples/gunbhub_serve_program"); + let std_root = ws.join("dsl/std"); + let gunbc_root = ws.join("dsl/gunbc"); + let extdeps_root = ws.join("dsl/extdeps"); + + let output = std::process::Command::new(&gunbc) + .arg("run") + .arg("--source-root") + .arg(program_root) + .arg("--source-root") + .arg(std_root) + .arg("--source-root") + .arg(gunbc_root) + .arg("--source-root") + .arg(extdeps_root) + .arg("--entry") + .arg(&entry) + .arg("--function") + .arg("main") + .current_dir(&ws) + .output() + .expect("spawn gunbc run for gunbhub_serve_program"); + + if output.status.success() { + return; + } + + let stdout = String::from_utf8_lossy(&output.stdout); + let stderr = String::from_utf8_lossy(&output.stderr); + panic!( + "gunbhub_serve_program func main failed (exit {:?}).\n--- stdout ---\n{stdout}\n--- stderr ---\n{stderr}", + output.status.code() + ); +} diff --git a/src/v1/tests/src/lib.rs b/src/v1/tests/src/lib.rs index d34fe11631a..5f6bf8dfdd2 100644 --- a/src/v1/tests/src/lib.rs +++ b/src/v1/tests/src/lib.rs @@ -57,6 +57,8 @@ mod fold_list_generic_instantiation_test; #[cfg(test)] mod generator_match_arm_test; #[cfg(test)] +mod gunbhub_serve_program_test; +#[cfg(test)] mod html_markup_smoke_test; #[cfg(test)] mod infer_semantics; From 43090ad724fb04bd597b03f467b50e5ad3cf97bf Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 23 Jun 2026 18:38:27 +0000 Subject: [PATCH 3/9] =?UTF-8?q?Fix=20soft-skip=20to=20assert=20in=20gunbhu?= =?UTF-8?q?b=5Fserve=5Fprogram=5Ftest=20(=C2=A75:=20green=20must=20mean=20?= =?UTF-8?q?executed)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-Authored-By: Claude Sonnet 4.6 --- src/v1/tests/src/gunbhub_serve_program_test.rs | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/src/v1/tests/src/gunbhub_serve_program_test.rs b/src/v1/tests/src/gunbhub_serve_program_test.rs index e917e24dc49..ea34fa20861 100644 --- a/src/v1/tests/src/gunbhub_serve_program_test.rs +++ b/src/v1/tests/src/gunbhub_serve_program_test.rs @@ -4,12 +4,10 @@ use crate::helpers::workspace_root; fn gunbhub_serve_program_runs_green() { let ws = workspace_root(); let gunbc = ws.join("target/release/gunbc"); - if !gunbc.is_file() { - eprintln!( - "skipping gunbhub_serve_program_runs_green: release binary not found (run `cargo build --release -p v1-compiler` first)" - ); - return; - } + assert!( + gunbc.is_file(), + "release gunbc binary required for gunbhub_serve_program (built in ci_floor / ci_floor_parity)" + ); let entry = ws.join("dsl/examples/gunbhub_serve_program/gunbhub_serve_program.dag"); let program_root = ws.join("dsl/examples/gunbhub_serve_program"); From 6d9e06bf76aac57cd9ef79792e8ae89e936c4724 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 23 Jun 2026 18:43:16 +0000 Subject: [PATCH 4/9] =?UTF-8?q?Rename=20react=5Fmarkup=5Fwitness=5Ftest.da?= =?UTF-8?q?g=20=E2=86=92=20html=5Femit=5Fwitness=5Ftest.dag=20(carrier?= =?UTF-8?q?=E2=86=94content=20alignment)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-Authored-By: Claude Sonnet 4.6 --- .../{react_markup_witness_test.dag => html_emit_witness_test.dag} | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename dsl/test/claim/{react_markup_witness_test.dag => html_emit_witness_test.dag} (100%) diff --git a/dsl/test/claim/react_markup_witness_test.dag b/dsl/test/claim/html_emit_witness_test.dag similarity index 100% rename from dsl/test/claim/react_markup_witness_test.dag rename to dsl/test/claim/html_emit_witness_test.dag From 0638df5abd81f6f8f22ed1aa3f49498dcf90f2c2 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 23 Jun 2026 20:18:11 +0000 Subject: [PATCH 5/9] Reconcile roster + plan refs after html_emit_witness rename MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - claim_witness_corpus_ci_runner.dag: corpus_ci_gate_row_react_markup_keystone → corpus_ci_gate_row_html_emit_keystone; entry + function match renamed file - emission_ingestion_inverse.dag: update prose ref react_markup_witness_test.dag → html_emit_witness_test.dag Co-Authored-By: Claude Sonnet 4.6 --- dsl/gunbc/plans/emission_ingestion_inverse.dag | 2 +- src/v2/workflow/claim_witness_corpus_ci_runner.dag | 10 +++++----- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/dsl/gunbc/plans/emission_ingestion_inverse.dag b/dsl/gunbc/plans/emission_ingestion_inverse.dag index ab0c777658b..979006f2b6b 100644 --- a/dsl/gunbc/plans/emission_ingestion_inverse.dag +++ b/dsl/gunbc/plans/emission_ingestion_inverse.dag @@ -100,7 +100,7 @@ fn emission_ingestion_inverse_body() -> List { row(cells: [cell(text: "GitHub Actions `$\{\{ \}\}` expression language"), cell(text: "**opaque `String`** (🟡 scaffold) — worst"), cell(text: "`actions.dag` `*Expression \{ expression: String \}`; inline `$\{\{ runner.temp \}\}`/`$\{\{ hashFiles(…) \}\}` in `ci_workflow.dag`")]), row(cells: [cell(text: "CI YAML structure + shell-in-`run:`"), cell(text: "partly modeled, values strings; **three nested unmodeled languages** (YAML + GHA-expr + shell) all grepped"), cell(text: "`ci_yaml_serializer_witness_test.dag`, `ci_runner_seam_witness_test.dag`")]), row(cells: [cell(text: "bash intent (`program.dag`)"), cell(text: "sidecar AST, 11 importers"), cell(text: "the §5 guard's existing target")]), - row(cells: [cell(text: "**markup** (react/html/markdown)"), cell(text: "**modeled with escape semantics + MODEL-level discriminating witnesses** — the target state"), cell(text: "`react_markup_witness_test.dag` checks the *reject behavior* (`escape_url`, std/markup SECURITY SCOPE), not a grep")]), + row(cells: [cell(text: "**markup** (react/html/markdown)"), cell(text: "**modeled with escape semantics + MODEL-level discriminating witnesses** — the target state"), cell(text: "`html_emit_witness_test.dag` checks the *reject behavior* (`escape_url`, std/markup SECURITY SCOPE), not a grep")]), ], }, p(text: "Markup already does it right; the CI YAML is the same problem three layers deep, still strings."), diff --git a/src/v2/workflow/claim_witness_corpus_ci_runner.dag b/src/v2/workflow/claim_witness_corpus_ci_runner.dag index b86cddd3cb8..ec8b289b4fd 100644 --- a/src/v2/workflow/claim_witness_corpus_ci_runner.dag +++ b/src/v2/workflow/claim_witness_corpus_ci_runner.dag @@ -343,10 +343,10 @@ data corpus_ci_gate_row_html_markup_xss_keystone: ClaimWitnessCorpusClaimRunRow expected: ExpectPass } -data corpus_ci_gate_row_react_markup_keystone: ClaimWitnessCorpusClaimRunRow = ClaimWitnessCorpusClaimRunRow { - label: "react markup consumer + XSS reject keystone", - entry: "dsl/test/claim/react_markup_witness.dag", - function: "react_markup_keystone_holds", +data corpus_ci_gate_row_html_emit_keystone: ClaimWitnessCorpusClaimRunRow = ClaimWitnessCorpusClaimRunRow { + label: "html emit consumer + XSS reject keystone", + entry: "dsl/test/claim/html_emit_witness_test.dag", + function: "html_emit_keystone_holds", expected: ExpectPass } @@ -527,7 +527,7 @@ data claim_witness_corpus_shard_b_rows: List = [ corpus_ci_gate_row_probe_selector_cf_import_resolves, corpus_ci_gate_row_markup_serializer_keystone, corpus_ci_gate_row_html_markup_xss_keystone, - corpus_ci_gate_row_react_markup_keystone, + corpus_ci_gate_row_html_emit_keystone, corpus_ci_gate_row_markdown_markup_xss_keystone, corpus_ci_gate_row_filesystem_write_keystone, corpus_ci_gate_row_gunbhub_react_browse_keystone, From 225cf64339cd0dbf0156b98bb278d92aab824646 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 23 Jun 2026 20:56:05 +0000 Subject: [PATCH 6/9] Regen committed plan docs after html_emit_witness rename + authority drift MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit docs/plans/emission-ingestion-inverse.md: witness filename updated to html_emit_witness_test.dag (the authority was already fixed in the prior commit; the generated artifact was not regenerated). docs/plans/dsl-v2-defork-audit.md: 48-line §2A section was in the committed .md but no longer in the .dag authority (pre-existing generated-artifact drift caught by main_wet). Both files regenerated via main_wet on dsl/tools/generated_artifact_gate.dag. Co-Authored-By: Claude Sonnet 4.6 --- docs/plans/dsl-v2-defork-audit.md | 48 ------------------------ docs/plans/emission-ingestion-inverse.md | 2 +- 2 files changed, 1 insertion(+), 49 deletions(-) diff --git a/docs/plans/dsl-v2-defork-audit.md b/docs/plans/dsl-v2-defork-audit.md index e4a60f9f4ae..39fa7940f33 100644 --- a/docs/plans/dsl-v2-defork-audit.md +++ b/docs/plans/dsl-v2-defork-audit.md @@ -4,54 +4,6 @@ **Re-verified against the live tree on 2026-06-22 by execution** (decl-name set `comm` per concept + shared-type-body diff). This pass **corrected a load-bearing project assumption**: the dsl↔v2 std fork is *not* "mostly temporary v2 mirrors of dsl." It is **2 true mirrors + 2 pure name-collisions + 7 divergent groundings** — the same concepts grounded on *different axes/realizations*. The hard part of the de-fork is therefore a grounding-unification **design** (operator-owned, downstream of the numeric tower #5428 and the model↔realization grounding), not a mechanical sweep. The prior version of this doc ("11 mechanical PRs / 5 collapses / `Classical`↔`Bool` nickname") was wrong by execution and is superseded below. -**Re-confirmed by execution 2026-06-23 (post-#5640), for the -[#2 resolver-wall](resolver-type-name-collision-wall.md) (PR #5652) Q2 ruling — see §2A.** Net distribution now: **2 true mirrors** (`reducible` DONE #5507, `measure` in-flight -#5509) **+ 6 divergent groundings** (`algebra`/`logic`/`nat`/`integer`/`float`/`effects`) **+ 2 -v1-artifact name-collisions** (`node`, `coercion`) **+ 1 RESOLVED** (`verification`, #5640 — it was a -name-collision resolved by rename-apart, *not* a grounding-merge, so it leaves the cluster). **Executed -verdict: cant-unify-yet (needs a milestone later than the grounding de-fork) == {node, coercion} -exactly — no third stuck mirror — so the signed `flag-ANY + {node,coercion}` wall policy HOLDS.** - ---- - -## 2A. 2026-06-23 executed Q2 confirmation (post-#5640) — supersedes the `verification` census row - -Read-only, by execution. Structural extraction of every top-level `type` decl in `dsl/std/.dag` -vs `src/v2/std/.dag`; shared **unqualified type names** compared with the #2 guard's own -`structural_inequality` predicate (normalized body equality) — this run is also the §5 proof that the -predicate classifies correctly. Reachability = BFS of all **351** `_test.dag` floor entries' whole-module -import closures testing whether `std.` and `v2.std.` co-occur in one closure (= the guard fires). - -| basename | shared type-names | structural verdict | floor co-occurrence | category | unify status | -|---|---|---|---|---|---| -| **algebra** | 16 (13 differ; 3 byte-identical `Lattice`/`Magma`/`Ordering`) | same concept, divergent **encoding** (dsl flat records vs v2 compositional/coproduct) | **LIVE — 75 entries** | grounding (Root-A: v2 coproduct authority RULED 2026-06-22) | cant-unify-yet, **has path** (de-fork-resolved, not exempted) | -| **nat** | 1 (`Nat`: `= CommutativeSemiring` vs `= Zero \| Succ`) | same concept, divergent **model** | **LIVE — 4 entries** | grounding (#5428 numeric tower; escalated smart-ant-466) | cant-unify-yet, has path; BLOCKED + LAST | -| **effects** | 3 (`EffectShape`/`KeySource`/`CreateCause`; `EffectShape` body re-modeled on a different axis) | divergent **axis** (operation-kind vs idempotency-class) | latent (0) | grounding | cant-unify-yet, has path (axis-authority decision) | -| **float** | 3 (2 differ; 1 byte-identical `Float = Float64`) | same concept, divergent encoding | latent (0) | grounding (#5428) | cant-unify-yet, has path | -| **integer** | 14 (11 differ only on `MachineWidth<8>` vs ``; 3 byte-identical) | same concept, near-identical (token diff) | latent (0) | grounding (#5428) | cant-unify-yet, has path (mechanical once the tower lands) | -| **verification** | **0** (was 1: `TestClaim`) | **RESOLVED #5640** (dsl record renamed `TestClaim → AssertionClaim`) | none now | **RESOLVED name-collision** (not a grounding) | **DONE** | -| **logic** | **0** (dsl `Classical` vs v2 `Bool`) | divergent concept, **no name overlap** | none (0 shared) | grounding-or-rename (undecided) | **no type-name collision → guard never fires** | -| **coercion** | **0** (dsl cast vocab vs v2 `coercion_fold`) | divergent concept, **no name overlap** | none (0 shared) | v1-artifact name-collision | dissolve-on v1-delete; **0 type-name collisions → exemption vacuous for the guard** | -| **node** | **0** (dsl v1-only `compiler_inductive_fields` vs v2 Node substrate) | divergent concept, **no name overlap** | none (0 shared) | v1-artifact name-collision | dissolve-on v1-delete; **0 type-name collisions → exemption vacuous for the guard** | - -**Confirms parent's derived distribution; cant-unify-yet == {node, coercion} exactly; flag-ANY + -{node,coercion} HOLDS.** Two scope refinements (strengthen, do not refute the ruling): - -1. **The {node,coercion} exemption is VACUOUS for the type-name guard.** node/coercion (and logic, - and now verification) share **zero** type names — only the *basename*. The guard keys on a shared - unqualified **type name** within one closure, so it never fires on them; their de-fork is a - *module-basename* rename (Route-C / v1-delete), a different surface. The guard needs no - {node,coercion} roster entry to land green — keeping it would be a dead (non-firing) exemption, - itself a §5 smell. Recommend marking the roster entry explicitly "Route-C basename, non-firing" - or dropping it from the guard model. -2. **The guard's real lands-green gate is the grounding de-fork of the shared-type-name basenames**, - fronted by the LIVE pair `{algebra (75 floor entries), nat (4)}` — they silently fail-open today - (benign only because they shadow record-with-record, not the coproduct-variant-drop that broke - `verification` under A1), and a flag-ANY wall reds them on landing. `{effects, float, integer}` - are latent (no co-occurrence today) but re-arm risks (exactly how verification went latent→LIVE - under A1). So the wall lands-already-green only after `{algebra, nat}` (then the latent three) - de-fork — that sequence, not the {node,coercion} exemption, gates activation. - --- ## 0. Thesis — the only duplication is v2's bootstrap copies of dsl diff --git a/docs/plans/emission-ingestion-inverse.md b/docs/plans/emission-ingestion-inverse.md index 1eb388c3457..a3ebde0a71b 100644 --- a/docs/plans/emission-ingestion-inverse.md +++ b/docs/plans/emission-ingestion-inverse.md @@ -96,7 +96,7 @@ The §5 guard catches a module *importing* a target AST it shouldn't. But there | GitHub Actions `${{ }}` expression language | **opaque `String`** (🟡 scaffold) — worst | `actions.dag` `*Expression { expression: String }`; inline `${{ runner.temp }}`/`${{ hashFiles(…) }}` in `ci_workflow.dag` | | CI YAML structure + shell-in-`run:` | partly modeled, values strings; **three nested unmodeled languages** (YAML + GHA-expr + shell) all grepped | `ci_yaml_serializer_witness_test.dag`, `ci_runner_seam_witness_test.dag` | | bash intent (`program.dag`) | sidecar AST, 11 importers | the §5 guard's existing target | -| **markup** (react/html/markdown) | **modeled with escape semantics + MODEL-level discriminating witnesses** — the target state | `react_markup_witness_test.dag` checks the *reject behavior* (`escape_url`, std/markup SECURITY SCOPE), not a grep | +| **markup** (react/html/markdown) | **modeled with escape semantics + MODEL-level discriminating witnesses** — the target state | `html_emit_witness_test.dag` checks the *reject behavior* (`escape_url`, std/markup SECURITY SCOPE), not a grep | Markup already does it right; the CI YAML is the same problem three layers deep, still strings. From caa59bff3ff4cb7e57bbde9d5733e3613a147d27 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 23 Jun 2026 22:08:19 +0000 Subject: [PATCH 7/9] =?UTF-8?q?Regen=20dsl-v2-defork-audit.md=20=E2=80=94?= =?UTF-8?q?=20blank=20line=20drift=20after=20merge?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Single blank line missing between §2A conclusion and the --- separator. Regenerated via main_wet on dsl/tools/generated_artifact_gate.dag. Co-Authored-By: Claude Sonnet 4.6 --- docs/plans/dsl-v2-defork-audit.md | 1 + 1 file changed, 1 insertion(+) diff --git a/docs/plans/dsl-v2-defork-audit.md b/docs/plans/dsl-v2-defork-audit.md index 31d51cfe3a2..1fb3bfc8a78 100644 --- a/docs/plans/dsl-v2-defork-audit.md +++ b/docs/plans/dsl-v2-defork-audit.md @@ -51,6 +51,7 @@ fronted by the LIVE pair `{algebra (75 floor entries), nat (4)}` — they silent are latent (no co-occurrence today) but re-arm risks (exactly how verification went latent→LIVE under A1). So the wall lands-already-green only after `{algebra, nat}` (then the latent three) de-fork — that sequence, not the {node,coercion} exemption, gates activation. + --- ## 0. Thesis — the only duplication is v2's bootstrap copies of dsl From faae55a9547e19cf31e95ee3981f35d6dbd19537 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 23 Jun 2026 22:59:49 +0000 Subject: [PATCH 8/9] =?UTF-8?q?Regen=20ROADMAP.md=20=E2=80=94=20remove=20c?= =?UTF-8?q?i-humming=20link=20not=20in=20.dag=20authority=20after=20main?= =?UTF-8?q?=20merge?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-Authored-By: Claude Sonnet 4.6 --- ROADMAP.md | 1 - 1 file changed, 1 deletion(-) diff --git a/ROADMAP.md b/ROADMAP.md index 2fcee21e71b..a99334274ff 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -85,7 +85,6 @@ This window = a few days of STABILITY — shrink the fail-open surface, don't "l A flaky or green-but-broken floor means no gate protects anything — so CI is upstream of every §0 claim. CI is also the one workload that flexes *every* substrate layer at once (execution · scheduling · caching · secrets/effects · emission), so it is the forcing function that turns each modeled-but-inert abstraction load-bearing. **Deliverable = shared abstractions proven by CI consuming them** (one Materialization kernel · one Placement authority · one secrets model); faster CI falls *out* of that, it is not the goal (§6 — price the lane in displaced cost, "move with confidence", not elegance). → [charter: causal-chain gap analysis](docs/plans/ci-process-end-to-end.md) — what's on `.dag` today vs not, push→execute. -→ [CI humming](docs/plans/ci-humming.md) — the throughput/wall-clock/reliability operations plan for the **▸ NOW** milestone: un-throttle runner slots from the modeled budget (fix the build-pool double-count), verified-effective caps, the carrier, SessionSliceEnforcement, oomd demoted to backstop. **◆ Milestones:** execution-as-DAG ✓ (the floor *is* a bounded forward graph walk) · width on `.dag` ✓ (#5444) → **▸ NOW — host-operation on `.dag` (placement · runner deployment · caps are hand-managed, off-fabric)** → resolve-cache enabled → one Materialization kernel (collapse the 5 caches) → one Placement authority (jobs · threads · sessions = 3 forks) → shared secrets · gunbhub closes the GitHub engine (G6, parked) From 8f621e5ff83c61f4e4dd93c83427c319623b5151 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 24 Jun 2026 00:53:58 +0000 Subject: [PATCH 9/9] =?UTF-8?q?Regen=20ROADMAP.md=20=E2=80=94=20remove=20c?= =?UTF-8?q?i-humming=20link=20not=20in=20.dag=20authority=20after=20main?= =?UTF-8?q?=20merge?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-Authored-By: Claude Sonnet 4.6 --- ROADMAP.md | 1 - 1 file changed, 1 deletion(-) diff --git a/ROADMAP.md b/ROADMAP.md index c70d0aa34b2..71ed597ba24 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -85,7 +85,6 @@ This window = a few days of STABILITY — shrink the fail-open surface, don't "l A flaky or green-but-broken floor means no gate protects anything — so CI is upstream of every §0 claim. CI is also the one workload that flexes *every* substrate layer at once (execution · scheduling · caching · secrets/effects · emission), so it is the forcing function that turns each modeled-but-inert abstraction load-bearing. **Deliverable = shared abstractions proven by CI consuming them** (one Materialization kernel · one Placement authority · one secrets model); faster CI falls *out* of that, it is not the goal (§6 — price the lane in displaced cost, "move with confidence", not elegance). → [charter: causal-chain gap analysis](docs/plans/ci-process-end-to-end.md) — what's on `.dag` today vs not, push→execute. -→ [CI humming](docs/plans/ci-humming.md) — the throughput/wall-clock/reliability operations plan for the **▸ NOW** milestone: un-throttle runner slots from the modeled budget (fix the build-pool double-count), verified-effective caps, the carrier, SessionSliceEnforcement, oomd demoted to backstop. → [CI humming](docs/plans/ci-humming.md) — the throughput/wall-clock/reliability operations plan for the **▸ NOW** milestone: un-throttle runner slots from the modeled budget (fix the build-pool double-count), verified-effective caps, the carrier, SessionSliceEnforcement, oomd demoted to backstop.