Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
51 commits
Select commit Hold shift + click to select a range
3e3b72c
Compute admission reserves observed host memory atomically, not a cou…
Sep 21, 2026
9bf00d7
The meminfo parse resolves each field by the lookup that proves it pr…
Sep 21, 2026
047bb3e
Three defects the first real run on srv1 found, and the controls for …
Sep 21, 2026
dd240f0
Body-position annotations refused by gunbc compile; move them to modu…
Sep 21, 2026
725d9c5
Four design defects: the double promise, the instance-keyed pool, the…
Sep 21, 2026
9172cf7
Quiescence is observed, obligations are per attempt, and the admissio…
Sep 21, 2026
5ee0cce
PR 1 rescoped to admission+pool: conservative release, declared disch…
Sep 21, 2026
773825c
The empty-ControlGroup release arm, the discarded host record, and tw…
Sep 21, 2026
73c570f
A completed wait never overrides a live cgroup; an uncertain completi…
Sep 21, 2026
1248df9
The bound termination policy is a fold a control can read, not a sent…
Sep 21, 2026
f5344b2
Merge remote-tracking branch 'origin/main' into session/bold-lynx-559
Sep 21, 2026
c901fc0
The release predicate is exactly four cases; a lost record reaches a …
Sep 21, 2026
1c670b8
The receipt stays parseable: the host-record fact gets its own file b…
Sep 21, 2026
bf58075
SeatRequest carries its dimension; the strip moves to where the pool …
Sep 21, 2026
afb46eb
The attached arm carried the loss it had just built into a discard
Sep 21, 2026
2700b01
File the partition-identity class the PoolAcquired argument would hav…
Sep 21, 2026
319edef
PR 2 spine: the attempt slot, the CAS-gated launch, the five-arm unio…
Sep 21, 2026
a67ccbe
The self-declared window gets a ceiling that refuses, and the clock i…
Sep 21, 2026
18b329d
Two unmigrated SeatRequest callers outside the gate, and the truncate…
Sep 21, 2026
decde15
Merge branch 'session/bold-lynx-559' into session/bold-lynx-559-pkg4-…
Sep 21, 2026
ac364a1
File the truncated-enumeration class, for the truncation and not for …
Sep 21, 2026
09b62f9
/proc/meminfo is not uniformly kB, and the witness asserted that it was
Sep 21, 2026
cae846a
Merge branch 'session/bold-lynx-559' into session/bold-lynx-559-pkg4-…
Sep 21, 2026
ce54fa4
The cited witness module is named with its _test suffix, unlike its s…
Sep 21, 2026
63c8ed2
Merge branch 'session/bold-lynx-559' into session/bold-lynx-559-pkg4-…
Sep 21, 2026
d3ab45b
File the shared-derivation class, and sharpen the enumeration rule
Sep 21, 2026
c3df024
Criteria 5 and 7: the attach decision moves inside the lease, and three
Sep 22, 2026
f0cd938
Merge remote-tracking branch 'origin/main' into session/bold-lynx-559…
Sep 22, 2026
db3e6a5
Wire the attempt slot into the provider route, and give the seat a do…
Sep 22, 2026
546c7cc
The settlement line says something on the good path, and the lease-un…
Sep 22, 2026
951df74
A cancellation carries why
Sep 22, 2026
17e06b6
The stale-lease claim forbade a word the repaired note legitimately k…
Sep 22, 2026
ec72c34
The attempt record carries what it means: Kibibyte and EpochSecs on t…
Sep 22, 2026
ec0c231
The window constants are Seconds, and the wet witness is on the route…
Sep 22, 2026
9d9f074
The honest instrument conflates anyway: a second specimen where the c…
Sep 22, 2026
3b2a04e
The token is the defect, not the cause: name the remedy as a distinct…
Sep 22, 2026
abfcb8c
A duplicated roster identity was unrepresented by every claim over th…
Sep 22, 2026
d2be498
A refused gate settled nothing, and the receipt said it settled the slot
Sep 22, 2026
67510f7
Merge remote-tracking branch 'origin/main' into pkg4-lifecycle-fix
Sep 22, 2026
3a60e2c
The discharge row failed the retirement condition it wrote for itself
Sep 22, 2026
9eb96c4
The control for the settlement fix ran nowhere, and the census that s…
Sep 22, 2026
7412d23
The note about a lifted claim was left at EOF, where an annotation na…
Sep 22, 2026
8efbc27
A seat the pool no longer holds was reported as a failed release
Sep 22, 2026
f4d0bb1
The note on the nothing-to-release arm sat inside a match body, where…
Sep 22, 2026
a2a19f9
A terminal verdict was any word, and the decode that refuses unknown …
Sep 22, 2026
b6d0b76
A manager that cannot be asked is a property not queried, not an abor…
gunbai-bot[bot] Sep 23, 2026
b7eab63
The note on the refused-spawn claim sat inside its body, where no ann…
Sep 23, 2026
9436fe2
Enrol the sixth host_capacity wet identity the floor refused as an un…
Sep 23, 2026
b84d29e
Merge origin/main into #12040: the ceiling retry is a new attempt thr…
Sep 23, 2026
bf63e3c
Recovery release names the attempt's granted seat as the capacity sub…
Sep 23, 2026
a308481
Enroll the ceiling-retry gate control: wet schedule row and DirWithTe…
Sep 23, 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: 2 additions & 0 deletions dag/extdeps/systemd/systemctl.dag
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
module extdeps.systemd.systemctl

import extdeps.transports.shell { ShellOutcome }
import std.types { NonEmptyStr, List, Bool, Int, Unit }
import std.string_type { String }
import std.algebra { trim }
Expand Down Expand Up @@ -595,6 +596,7 @@ service systemd.Systemctl {
operation ShowUserProperty {
input { unit: NonEmptyStr, property: NonEmptyStr }
output {
outcome: ShellOutcome
value: String from "stdout"
success: Bool from "exit_success"
}
Expand Down
14 changes: 14 additions & 0 deletions dag/gunbc/ci/ci_layer_roots.dag
Original file line number Diff line number Diff line change
Expand Up @@ -327,6 +327,10 @@ data excl_run_verdict_exit_status_dissolve: DissolutionCondition = unbound_disso

data excl_shell_spawn_refused_reason: String = "SUBSTANTIATED per-row: the subject of test.claim.shell_spawn_refused_real_execution_witness is whether the host can spawn argv[0], and whether the seed's shell transport turns a failed spawn into ShellSpawnRefused rather than aborting the evaluation. Both are facts about the real spawn, so the file cannot be made hermetic: a mock_response for test.ShellSpawnProbe.Observed would be authored data, and the discriminating red (an absent binary yields ShellSpawnRefused) would pass against a fabricated refusal whether or not the transport realizes one. Its fns are scheduled in v2.workflow.local_repo_wet_terminal local_repo_wet_schedule, which the required floor executes: the only effect is spawning a local program (true, false, an absent name) -- no network, no cargo, no remote host, no writes."

data excl_manager_unaskable_reason: String = "SUBSTANTIATED per-row, and it is its OWN row rather than a second use of excl_shell_spawn_refused_reason because that reason substantiates a DIFFERENT SUBJECT AND A DIFFERENT EFFECT SET (review 69970): it says in terms that the subject of test.claim.shell_spawn_refused_real_execution_witness is whether the host can spawn argv[0], and that its only effect is spawning a local program. The subject here is a SYSTEMD USER MANAGER -- whether gunbc.compute.work_provider_local read_user_unit_property folds a refused spawn of systemctl into a property that was NOT QUERIED, so the two unit readings reach their own unavailable arm instead of the whole evaluation ending as a shell-spawn-refused runtime error with the seat charged and the producer lease held. The effects are the manager probe, systemctl ShowUserProperty for four unit properties, and a cgroup events read: a superset of the neighbour row's one effect, over a different boundary. DESIGN section 3b: a home that resolves but owns only part of the scope a row claims is a scope/ownership mismatch on the row. The negative half that admits it to the same LANE is the one every member shares: no network, no cargo, no remote host, no install media, and nothing written outside what the witness creates."

data excl_manager_unaskable_dissolve: DissolutionCondition = unbound_dissolution(description: "mock_response coverage lands for the manager probe AND for systemd.Systemctl.ShowUserProperty, sufficient for the queried/not-queried fold to be re-checked hermetically against BOTH shell outcomes; then the fn re-enrols as an ordinary hermetic discovery row, drops off local_repo_wet_schedule and off floor_route_gap, and this row deletes. A mock for the probe ALONE does not discharge it: the subject is what the property reader does when the manager cannot be spawned, so a run that reaches ShowUserProperty through a fixture and never exercises the refusal arm re-checks the assertion against authored data rather than against the boundary.")

data excl_shell_spawn_refused_dissolve: DissolutionCondition = unbound_dissolution(description: "the spawn boundary of the shell transport becomes executable under the execution-corpus scope prefix as ExecutionWitnessKind rows in gunbc.commit_workflow, the same terminal excl_bin_wet_dissolve names; then this row and its four schedule rows delete together. Publishing a mock_response for ShellSpawnProbe.Observed does NOT discharge it: a mocked ShellSpawnRefused re-checks the assertions against a fixture, not against the spawn.")

// bin-execution witness class re-homed to the falsifier wet cadence (CI floor endgame D6): the
Expand Down Expand Up @@ -1031,6 +1035,16 @@ data witness_exclusion_frontier: List<WitnessExclusionRow> = [
classification: LocalRepoWetLane,
reason: excl_local_repo_wet_tempdir_write_reason,
dissolution: excl_local_repo_wet_dissolve},
WitnessExclusionRow {
pattern: "manager_unaskable_wet_witness_test.dag",
classification: LocalRepoWetLane,
reason: excl_manager_unaskable_reason,
dissolution: excl_manager_unaskable_dissolve},
WitnessExclusionRow {
pattern: "attempt_lifecycle_wet_witness_test.dag",
classification: LocalRepoWetLane,
reason: excl_local_repo_wet_tempdir_write_reason,
dissolution: excl_local_repo_wet_dissolve},
WitnessExclusionRow {
pattern: "review_sheet_legacy_declaration_wet_witness_test.dag",
classification: LocalRepoWetLane,
Expand Down
Loading