Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
32 commits
Select commit Hold shift + click to select a range
d20b899
Make required-v2-native's envelope, flags, budget, and main occupancy…
Sep 10, 2026
fe8e5be
Scope P0a to native-job supersession and a 360-minute envelope.
Sep 10, 2026
1091c67
Make PR-head native supersession reachable: unique workflow run_id.
Sep 10, 2026
b875898
Supersede stale witnesses.yml runs at whole-workflow PR and main grain.
Sep 10, 2026
6bc0a18
Merge origin/main so P0a.1 is not based behind the publication-witnes…
Sep 10, 2026
662b29a
Join witnesses.yml cancel to occupancy standing, not a second policy …
Sep 10, 2026
c434c88
Split occupancy grouping from fleet-safe running cancel.
Sep 11, 2026
da99984
Delete the witness-only cancel join; four-cell the production chain.
Sep 11, 2026
1171ef2
Retire the 2026-08-17 unique-run_id grouping annotation.
Sep 11, 2026
8b3dee1
Derive the concurrency group from the event-name and heal-input autho…
Sep 11, 2026
b49128b
Fold concurrency-group GHA from modeled event/subject rows and resolv…
Sep 11, 2026
6b088db
Require joined event-and-subject group patterns and a crossed-pairing…
Sep 11, 2026
11345f9
Declare the main per-commit floor drop and bind the heal resolver to …
Sep 11, 2026
ba68bd5
Correct the main-floor drop trigger and unbind timeout from the group…
Sep 11, 2026
9a9adc2
Delete the required-v2-native CI job; the route stays as an operator-…
Sep 11, 2026
55fa347
Merge occupancy grouping onto the native-job deletion.
Sep 11, 2026
5ea0164
Emit occupancy grouping and cancel expressions through extdeps.github…
Sep 11, 2026
ef52ded
Merge origin/main into prep/lark.
Sep 11, 2026
52909e7
Model NotEquals in GitHub expressions and drop the heal gap row.
Sep 11, 2026
bb591f3
Delete the producer-side event-name string serializer.
Sep 11, 2026
b80c7c5
Move GHA evaluation into extdeps.github.expressions and refuse unmode…
Sep 11, 2026
e481e1d
Merge origin/main into session/sharp-tern-402.
Sep 11, 2026
d752595
Derive mutable-head event membership and cancel OR from one roster.
Sep 11, 2026
99d0f59
Treat only the empty string as falsy in the GHA expression evaluator.
Sep 11, 2026
7ef183d
Keep running-cancel restoration to pull_request; do not cancel runnin…
Sep 11, 2026
cab3525
Merge origin/main into session/sharp-tern-402.
Sep 11, 2026
b13a3b9
Wire the safe fleet arm to SupersedeMutableHeadRuns over the PR-only …
Sep 11, 2026
7133546
Delete the unused SupersedeMutableHeadRuns surface.
Sep 11, 2026
8f9c28f
Name grouping and the main-verdict drop instead of citing the group a…
Sep 11, 2026
db677c9
Split grouping and PR-activity witnesses off the full YAML serialize.
Sep 11, 2026
f052982
Restore trigger-types emission coverage without a full workflow seria…
Sep 11, 2026
608c9ad
Record that trigger-types coverage is the on: fragment plus the YAML …
Sep 11, 2026
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
2 changes: 1 addition & 1 deletion .github/workflows/witnesses.yml
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ on:
permissions:
contents: read
concurrency:
group: witness-floor-${{ github.event.pull_request.number || github.run_id }}
group: witness-floor-${{ github.event_name == 'merge_group' && format('mg-{0}', github.sha) || github.event_name == 'workflow_dispatch' && github.event.inputs.expected_healed_sha != '' && format('heal-{0}', github.event.inputs.expected_healed_sha) || github.event_name == 'pull_request' && format('pr-{0}', github.event.pull_request.number) || github.event_name == 'push' && github.ref || format('run-{0}', github.run_id) }}
cancel-in-progress: false
env:
CARGO_TERM_COLOR: always
Expand Down
196 changes: 186 additions & 10 deletions dag/extdeps/github/expressions.dag
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,8 @@ module extdeps.github.expressions
import extdeps.external_authority { ExternalAuthority }
import extdeps.uri { Uri, Https }
import extdeps.communication.medium { Lossless }
import v2.std.algebra { fold_list, list_head, skip, HeadFound, HeadAbsent, length }
import std.types { Bool, List, String, Int }

data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority {
uri: Uri {
Expand All @@ -11,6 +13,20 @@ data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority {
}
}

data github_expression_operators_authority: ExternalAuthority = ExternalAuthority {
uri: Uri {
scheme: Https
locator: "docs.github.com/en/actions/writing-workflows/choosing-what-your-workflow-does/evaluate-expressions-in-workflows-and-actions#operators"
}
}

data github_expression_format_authority: ExternalAuthority = ExternalAuthority {
uri: Uri {
scheme: Https
locator: "docs.github.com/en/actions/writing-workflows/choosing-what-your-workflow-does/evaluate-expressions-in-workflows-and-actions#format"
}
}

type ExpressionContext
= Github
| Env
Expand Down Expand Up @@ -46,6 +62,7 @@ type Expression
| LogicalOr { left: Expression, right: Expression }
| LogicalAnd { left: Expression, right: Expression }
| Equals { left: Expression, right: Expression }
| NotEquals { left: Expression, right: Expression }

type TemplateSegment
= LiteralText { text: String }
Expand Down Expand Up @@ -98,6 +115,7 @@ type ExpressionSpellings {
or_op: String
and_op: String
eq_op: String
neq_op: String
interp_open: String
interp_close: String
index_open: String
Expand All @@ -113,6 +131,7 @@ data default_expression_spellings: ExpressionSpellings = {
or_op: " || ",
and_op: " && ",
eq_op: " == ",
neq_op: " != ",
interp_open: "${{ ",
interp_close: " }}",
index_open: "['",
Expand Down Expand Up @@ -207,6 +226,8 @@ fn serialize_expression_with(expression: Expression, sp: ExpressionSpellings) ->
join([serialize_expression_with(expression: l, sp: sp), serialize_expression_with(expression: r, sp: sp)], sp.and_op)
Equals { left: l, right: r } =>
join([serialize_expression_with(expression: l, sp: sp), serialize_expression_with(expression: r, sp: sp)], sp.eq_op)
NotEquals { left: l, right: r } =>
join([serialize_expression_with(expression: l, sp: sp), serialize_expression_with(expression: r, sp: sp)], sp.neq_op)
}
}

Expand Down Expand Up @@ -451,6 +472,9 @@ fn expression_accesses_runner_var_via_env(expression: Expression) -> Bool {
Equals { left: l, right: r } =>
expression_accesses_runner_var_via_env(expression: l) ||
expression_accesses_runner_var_via_env(expression: r)
NotEquals { left: l, right: r } =>
expression_accesses_runner_var_via_env(expression: l) ||
expression_accesses_runner_var_via_env(expression: r)
StringLiteral { value: _ } => false
}
}
Expand All @@ -469,6 +493,9 @@ fn expression_uses_context(expression: Expression, target: ExpressionContext) ->
Equals { left: l, right: r } =>
expression_uses_context(expression: l, target: target) ||
expression_uses_context(expression: r, target: target)
NotEquals { left: l, right: r } =>
expression_uses_context(expression: l, target: target) ||
expression_uses_context(expression: r, target: target)
StringLiteral { value: _ } => false
}
}
Expand Down Expand Up @@ -513,18 +540,167 @@ fn template_uses_context(template: ExpressionTemplate, target: ExpressionContext
// to BOTH directions plus the goldens that pin them, not a serializer edit.
//
// DECLARED ASYMMETRY, NAMED RATHER THAN LEFT IMPLIED (review 49460): parse_expression_with reads
// Or, calls, context accesses and string literals; it does NOT read && or ==. So these two
// operators are EMISSION-ONLY today, and this module is bidirectional for the constructs that
// predate them and one-way for these. That is a real §4 asymmetry, admissible here only because no
// consumer reads these forms BACK — the sole use is lowering a job condition that GitHub evaluates
// and nothing in this tree re-ingests. It stops being admissible the moment any consumer parses a
// condition containing && or ==, which is the trigger: ingest arms for both operators plus
// round-trip witnesses covering them land before that consumer, not after it. Stated explicitly
// because the previous revision of this row broke bidirectionality by accident and shipped it; an
// asymmetry that is declared and triggered is a frontier, one that is merely true is a defect
// waiting to be discovered.
// Or, calls, context accesses and string literals; it does NOT read &&, ==, or !=. So those
// operators remain UNPARSED from surface syntax. That is a real §4 ingest asymmetry. A
// structural evaluator over an already-constructed Expression AST is not that trigger: it
// does not ingest operator text, so it does not fire the "ingest arms plus round-trip witnesses
// land before a parse consumer" row. The trigger remains a consumer that parses &&, ==, or !=
// from a string. This PR's concurrency-group fixture resolver is the first in-tree consumer
// that reads the AST back by evaluation; it is not a re-ingestion of serialized operator
// spellings. NotEquals is emitted and evaluated; it is still not ingested from text.

fn any_template_accesses_runner_var_via_env(templates: List<ExpressionTemplate>) -> Bool {
fold(templates, init: false, f: (acc, template) =>
acc || template_accesses_runner_var_via_env(template: template))
}

// GITHUB ACTIONS TRUTHINESS (github_expression_operators_authority, operators): the falsy
// values are the boolean false, the numbers 0 and -0, empty string, and null. Non-empty strings
// are truthy, including the strings "false" and "0" — `${{ 'false' && 'x' }}` is `'x'`. This
// evaluator is string-only; Equals/NotEquals encode a boolean false as the empty string, so
// treating the string "false" as falsy would invent a string-typed boolean GitHub does not have.
// format() substitution is github_expression_format_authority `format` with replaceValue0 as `{0}`.
fn gha_value_is_truthy(s: String) -> Bool {
s != ""
}

fn github_path_key(path: List<String>) -> String {
fold_list(
xs: path,
empty: "",
cons: fn(acc, s) {
if acc == "" {
s
} else {
concat(concat(acc, "."), s)
}
}
)
}

type GithubPathResolution
= GithubPathValue { value: String }
| GithubPathUnmodeled

type FormatEvaluationRefusal
= FormatTemplateNotLiteral
| FormatArityNotOneSubstitution { argument_count: Int }
| FormatPlaceholderNotArg0 { template: String }

type ExpressionEvaluationRefusal
= UnmodeledContext { context: ExpressionContext, path: List<String> }
| UnmodeledFunction { function: ExpressionFunction }
| UnmodeledFormat { cause: FormatEvaluationRefusal }

type ExpressionEvaluation
= ExpressionValue { value: String }
| ExpressionEvaluationRefused { cause: ExpressionEvaluationRefusal }

fn apply_format_arg0(template: String, arg0: String) -> ExpressionEvaluation {
let n = string_length(s: template)
let m = string_length(s: "{0}")
if string_contains(template, "{1}") || !(n >= m && substring(s: template, start: n - m, end: n) == "{0}") {
ExpressionEvaluationRefused { cause: UnmodeledFormat { cause: FormatPlaceholderNotArg0 { template: template } } }
} else {
ExpressionValue { value: concat(substring(s: template, start: 0, end: n - m), arg0) }
}
}

fn eval_format_args(args: List<Expression>, github_path: fn(List<String>) -> GithubPathResolution) -> ExpressionEvaluation {
let n = length(xs: args)
if n != 2 {
ExpressionEvaluationRefused { cause: UnmodeledFormat { cause: FormatArityNotOneSubstitution { argument_count: n } } }
} else {
match list_head(xs: args) {
HeadAbsent => ExpressionEvaluationRefused { cause: UnmodeledFormat { cause: FormatArityNotOneSubstitution { argument_count: 0 } } }
HeadFound { value: tmpl } =>
match tmpl {
StringLiteral { value: t } =>
match list_head(xs: skip(xs: args, n: 1)) {
HeadAbsent => ExpressionEvaluationRefused { cause: UnmodeledFormat { cause: FormatArityNotOneSubstitution { argument_count: n } } }
HeadFound { value: arg } =>
match evaluate_expression(expression: arg, github_path: github_path) {
ExpressionEvaluationRefused { cause: c } => ExpressionEvaluationRefused { cause: c }
ExpressionValue { value: arg0 } => apply_format_arg0(template: t, arg0: arg0)
}
}
ContextAccess { context: _, path: _ } =>
ExpressionEvaluationRefused { cause: UnmodeledFormat { cause: FormatTemplateNotLiteral } }
FunctionCall { function: _, args: _ } =>
ExpressionEvaluationRefused { cause: UnmodeledFormat { cause: FormatTemplateNotLiteral } }
LogicalOr { left: _, right: _ } =>
ExpressionEvaluationRefused { cause: UnmodeledFormat { cause: FormatTemplateNotLiteral } }
LogicalAnd { left: _, right: _ } =>
ExpressionEvaluationRefused { cause: UnmodeledFormat { cause: FormatTemplateNotLiteral } }
Equals { left: _, right: _ } =>
ExpressionEvaluationRefused { cause: UnmodeledFormat { cause: FormatTemplateNotLiteral } }
NotEquals { left: _, right: _ } =>
ExpressionEvaluationRefused { cause: UnmodeledFormat { cause: FormatTemplateNotLiteral } }
}
}
}
}

fn evaluate_expression(expression: Expression, github_path: fn(List<String>) -> GithubPathResolution) -> ExpressionEvaluation {
match expression {
ContextAccess { context: Github, path: p } =>
match github_path(p) {
GithubPathValue { value: v } => ExpressionValue { value: v }
GithubPathUnmodeled => ExpressionEvaluationRefused { cause: UnmodeledContext { context: Github, path: p } }
}
ContextAccess { context: c, path: p } =>
ExpressionEvaluationRefused { cause: UnmodeledContext { context: c, path: p } }
FunctionCall { function: Format, args: a } => eval_format_args(args: a, github_path: github_path)
FunctionCall { function: f, args: _ } =>
ExpressionEvaluationRefused { cause: UnmodeledFunction { function: f } }
StringLiteral { value: v } => ExpressionValue { value: v }
LogicalOr { left: l, right: r } =>
match evaluate_expression(expression: l, github_path: github_path) {
ExpressionEvaluationRefused { cause: c } => ExpressionEvaluationRefused { cause: c }
ExpressionValue { value: lv } =>
if gha_value_is_truthy(s: lv) {
ExpressionValue { value: lv }
} else {
evaluate_expression(expression: r, github_path: github_path)
}
}
LogicalAnd { left: l, right: r } =>
match evaluate_expression(expression: l, github_path: github_path) {
ExpressionEvaluationRefused { cause: c } => ExpressionEvaluationRefused { cause: c }
ExpressionValue { value: lv } =>
if gha_value_is_truthy(s: lv) {
evaluate_expression(expression: r, github_path: github_path)
} else {
ExpressionValue { value: lv }
}
}
Equals { left: l, right: r } =>
match evaluate_expression(expression: l, github_path: github_path) {
ExpressionEvaluationRefused { cause: c } => ExpressionEvaluationRefused { cause: c }
ExpressionValue { value: lv } =>
match evaluate_expression(expression: r, github_path: github_path) {
ExpressionEvaluationRefused { cause: c } => ExpressionEvaluationRefused { cause: c }
ExpressionValue { value: rv } =>
if lv == rv {
ExpressionValue { value: "true" }
} else {
ExpressionValue { value: "" }
}
}
}
NotEquals { left: l, right: r } =>
match evaluate_expression(expression: l, github_path: github_path) {
ExpressionEvaluationRefused { cause: c } => ExpressionEvaluationRefused { cause: c }
ExpressionValue { value: lv } =>
match evaluate_expression(expression: r, github_path: github_path) {
ExpressionEvaluationRefused { cause: c } => ExpressionEvaluationRefused { cause: c }
ExpressionValue { value: rv } =>
if lv == rv {
ExpressionValue { value: "" }
} else {
ExpressionValue { value: "true" }
}
}
}
}
}
2 changes: 1 addition & 1 deletion dag/gunbc/doc_graph_roots.dag
Original file line number Diff line number Diff line change
Expand Up @@ -1614,7 +1614,7 @@ data hand_authored_doc_bind_incomings: List<HandAuthoredDocBind> = [
additional_works: [
DeclarationRef { module_path: "gunbc.witness_floor_workflow", decl_name: "witness_floor_concurrency_group", field: WholeDeclaration },
],
dissolution: PlanRetiresWhen { condition: unbound_dissolution(description: "the six findings this note records outlive their archived lanes only until each has a carrier of its own: the rejected_with_pending diagnostic-order defect, the entry-vs-member position divergence, the three-entrypoint admission divergence, the standing section 4c population that makes a full-corpus compile exit 1, the floor-gated deploy, and the run_id concurrency key -- that last one now carried by gunbc.witness_floor_workflow witness_floor_concurrency_group, which states the run_id fallback as the 2026-08-17 operator ruling that every push to main must finish, and by witness_floor_concurrency_policy, which derives the cancel axis from the observed fleet standing; the note is repointed there because the ci.yml-era second authority it used to cite was deleted with its workflow. When each is either fixed or carried as a typed row, the note is a historical account and deletes with this bind. It is registered rather than deleted today because four sessions were archived holding these measurements and nothing else records them — but a cross-lane status narrative is the parallel-ledger shape DESIGN section 6 warns about, so its home is a question for the operator, not a settled one.") },
dissolution: PlanRetiresWhen { condition: unbound_dissolution(description: "the six findings this note records outlive their archived lanes only until each has a carrier of its own: the rejected_with_pending diagnostic-order defect, the entry-vs-member position divergence, the three-entrypoint admission divergence, the standing section 4c population that makes a full-corpus compile exit 1, the floor-gated deploy, and the concurrency-group key -- that last one now carried by gunbc.witness_floor_workflow witness_floor_concurrency_group, which keys merge_group by sha, heal dispatch by expected_healed_sha, pull_request by number, push by github.ref, and run_id only as the bare-dispatch fallback, with the 2026-08-17 every-main-must-finish unique-run_id reading retired as gunbc.rung_drop main_per_commit_floor_verdict, and by witness_floor_concurrency_policy, which derives the cancel axis from the observed fleet standing; the note is repointed there because the ci.yml-era second authority it used to cite was deleted with its workflow. When each is either fixed or carried as a typed row, the note is a historical account and deletes with this bind. It is registered rather than deleted today because four sessions were archived holding these measurements and nothing else records them — but a cross-lane status narrative is the parallel-ledger shape DESIGN section 6 warns about, so its home is a question for the operator, not a settled one.") },
},
HandAuthoredDocBind {
home: PlanDoc,
Expand Down
2 changes: 1 addition & 1 deletion dag/gunbc/plans/ci_process_end_to_end.dag
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,7 @@ fn ci_process_end_to_end_body() -> List<MarkdownBlock> {
rows: [
row(cells: [cell(text: "1"), cell(text: "push branch / open-sync PR"), cell(text: "🔴"), cell(text: "—"), cell(text: "git + GitHub native")]),
row(cells: [cell(text: "2"), cell(text: "GitHub reads committed `ci.yml` triggers, starts run"), cell(text: "🟢 *file* / 🔴 *act*"), cell(text: "~0"), cell(text: "file derived+gated; dispatch engine native. **Bootstrap seam**: reads the *committed* file → stale-on-invocation-surface is uncaught")]),
row(cells: [cell(text: "3"), cell(text: "concurrency group + cancel-in-progress"), cell(text: "🟢 *key* / 🔴 *eval*"), cell(text: "~0"), cell(text: "key modeled (`witness_floor_concurrency_group`); the `run_id` fallback this row read as a dup bug is the declared main-coverage ruling, not a defect; evaluated by GitHub")]),
row(cells: [cell(text: "3"), cell(text: "concurrency group + cancel-in-progress"), cell(text: "🟢 *key* / 🔴 *eval*"), cell(text: "~0"), cell(text: "key modeled (`witness_floor_concurrency_group`); run_id is the bare-dispatch fallback only; per-main unique-run_id coverage is the declared drop `gunbc.rung_drop` `main_per_commit_floor_verdict`; cancel is `witness_floor_concurrency_policy`; evaluated by GitHub")]),
row(cells: [cell(text: "3′"), cell(text: "dashboard *also* fires `workflow_dispatch` same SHA"), cell(text: "🔴"), cell(text: "—"), cell(text: "ctrl/dashboard — **the dup source**")]),
row(cells: [cell(text: "4"), cell(text: "GitHub matches labels & **places the job on a host**"), cell(text: "🟢 *labels* / 🔴 *placement*"), cell(text: "~0 (queue)"), cell(text: "labels derived (`runner_spec_from_offer`); **placement is native, demand-blind, first-idle** ← **underutilization root (G1)**")]),
row(cells: [cell(text: "5"), cell(text: "a runner daemon on srv1/srv2 picks it up"), cell(text: "🔴 (🟡 inventory)"), cell(text: "—"), cell(text: "runners/host, registration, on-box labels = **hand-run shell, no repo artifact (G2)**; `operator_fleet` only *describes* the hosts")]),
Expand Down
Loading
Loading