Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 0 additions & 1 deletion ROADMAP.md
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand Down
2 changes: 1 addition & 1 deletion docs/plans/emission-ingestion-inverse.md
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand Down
78 changes: 78 additions & 0 deletions dsl/examples/gunbhub_serve_program/gunbhub_serve_program.dag
Original file line number Diff line number Diff line change
@@ -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",
}
}
}
14 changes: 14 additions & 0 deletions dsl/extdeps/languages/html.dag
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand Down Expand Up @@ -307,3 +308,16 @@ fn ingest_html_source(src: String) -> HtmlIngestResult {
fn html_medium_lossless(node: MarkupNode) -> Medium<MarkupNode> {
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) }
}
}
124 changes: 94 additions & 30 deletions dsl/gunbc/gunbhub_serve.dag
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down Expand Up @@ -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 } ],
},
],
Expand All @@ -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"),
],
},
],
},
],
},
],
Expand All @@ -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.",
},
],
},
],
},
],
},
],
},
Expand All @@ -129,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 }
}
}

Expand Down Expand Up @@ -214,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 }
}
}
}
Expand Down Expand Up @@ -284,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,
[
Expand All @@ -302,7 +366,7 @@ fn gunbhub_served_static_route_table() -> ServedStaticRouteTable {
},
]
)
ComposeRejected { reason: _ } => acc
EmitRejected { reason: _ } => acc
}
)
ServedStaticRouteTable { routes: routes }
Expand Down
14 changes: 7 additions & 7 deletions dsl/gunbc/gunbhub_serve_html.dag
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand All @@ -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 == "<p>gunbhub</p>"
Rejected { reason: _ } => false
match try_serialize_html_source(node: sample_html_page()) {
EmitOk { html: h } => h == "<p>gunbhub</p>"
EmitRejected { reason: _ } => false
}
}

Expand Down
2 changes: 1 addition & 1 deletion dsl/gunbc/plans/emission_ingestion_inverse.dag
Original file line number Diff line number Diff line change
Expand Up @@ -100,7 +100,7 @@ fn emission_ingestion_inverse_body() -> List<MarkdownBlock> {
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."),
Expand Down
22 changes: 0 additions & 22 deletions dsl/std/react_markup.dag

This file was deleted.

Loading