Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
27 commits
Select commit Hold shift + click to select a range
1640cf2
plan: belt demotion into event-driven attempt obligations (dogfood #6…
Oct 3, 2026
f5d44fd
plan: record Q1/Q2 rulings; attempt-event spool as the exit-event store
Oct 3, 2026
7bdd607
plan: typed mkdir exit hook (no shell), per bold-bee-114 ruling
Oct 3, 2026
43942c3
plan: homes under factory controller + attempt lifecycle; one PR per …
Oct 3, 2026
ae6e44d
Merge remote-tracking branch 'origin/main' into belt/event-driven-obl…
Oct 6, 2026
6fce8f7
extdeps.systemd.service_exec: stop-time variables and Exec command-li…
Oct 6, 2026
5b52625
attempt-exit spool: host_layout stages, typed mkdir stop hook, record…
Oct 6, 2026
9d42be0
exit records for worker, reviewer and auditor units: RemainAfterExit …
Oct 6, 2026
2890d08
belt demoted to launch + discovery: per-attempt obligation units, ins…
Oct 6, 2026
4f64103
RLM launch receipt: belt event path units replace the timer row; even…
Oct 6, 2026
3316352
rung drop: belt liveness for unconsumed publication answers, restored…
Oct 6, 2026
81414b9
obligation claims (#6 and #4 reds), wet exit-drain witness over a rea…
Oct 6, 2026
51fd8d9
plan doc reflects the built model and rulings; deployment and receipt…
Oct 6, 2026
1b3306c
bootstrap quiesced-count claims; drop tick-freshness claim (freshness…
Oct 9, 2026
d3339b5
merge main; typed Second durations, derived queued bound, spool-stage…
Oct 9, 2026
693f2f9
event backlog: spool mtime is EpochSecs; a future mtime refuses as un…
Oct 9, 2026
a22a720
one authority for the 45min belt run bound (belt_cadence); exhaustive…
Oct 9, 2026
80e0179
belt durations are typed Second; systemd time-span text is rendered o…
Oct 9, 2026
ab169c2
bootstrap quiescence masks the exit-drain and discovery services too,…
Oct 9, 2026
1fc2c49
exit-record signal is a closed LinuxStandardSignal, refused at decode…
Oct 9, 2026
d744c5d
chore: regenerate drifted generated artifacts (ci auto-heal)
gunbai-bot[bot] Oct 9, 2026
4e73c1b
new receipt witnesses supply values at their interface (under the eva…
Oct 9, 2026
42660e7
Merge remote-tracking branch 'origin/belt/event-driven-obligations' i…
Oct 9, 2026
94fef72
belt exit handoff: queued is a level, acknowledgment bound to a run's…
Oct 9, 2026
0e2f470
belt: a lone orphaned running claim is rescued without a new event (c…
Oct 9, 2026
75af82e
belt: the drain's boot target is derived from the manager its unit is…
Oct 9, 2026
9f20643
WIP: dogfood #6+#4: demote the monolithic belt tick into event-driven…
Oct 9, 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
1 change: 1 addition & 0 deletions dag/extdeps/exec/command.dag
Original file line number Diff line number Diff line change
Expand Up @@ -156,6 +156,7 @@ fn argv_command(program: ProgramIdentity, arguments: List<String>) -> ArgvComman
decl_ref(module_path: "extdeps.tools.gnu_coreutils", decl_name: "mktemp_directory_command"),
decl_ref(module_path: "extdeps.tools.gnu_coreutils", decl_name: "dd_overwrite_path_command"),
decl_ref(module_path: "extdeps.tools.gnu_coreutils", decl_name: "mkdir_parents_command"),
decl_ref(module_path: "extdeps.tools.gnu_coreutils", decl_name: "mkdir_create_only_command"),
decl_ref(module_path: "extdeps.tools.gnu_coreutils", decl_name: "ln_hard_command"),
decl_ref(module_path: "extdeps.tools.gnu_coreutils", decl_name: "ls_long_directory_command"),
decl_ref(module_path: "extdeps.tools.gnu_coreutils", decl_name: "ls_long_directory_numeric_command"),
Expand Down
121 changes: 120 additions & 1 deletion dag/extdeps/posix/signal.dag
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
module extdeps.posix.signal

import std.types { NonEmptyStr, String, Bool }
import std.types { NonEmptyStr, String, Bool, Int }
import extdeps.external_authority { ExternalAuthority, ExternalModelScope, ExternalSubjectRef }
import std.decl_ref { DeclarationRef, WholeDeclaration }
import extdeps.uri { Uri, Https }
Expand Down Expand Up @@ -48,3 +48,122 @@ service posix.Signal {
}
}
}

// THE LINUX SIGNAL NUMBERS FOR THE STANDARD SIGNALS, by the name systemd reports them under
// ($EXIT_STATUS when $EXIT_CODE is killed or dumped: the name without its SIG prefix). signal(7),
// "Standard signals": the numbering below is the one shared by x86, ARM and most other Linux
// architectures (the table's middle column); alpha, sparc, mips and parisc number some of these
// differently, and no host this repository runs on is one of them. A name not listed is refused
// with Absent rather than guessed -- including the realtime signals, which have no fixed number.
data linux_signal_numbers_authority: ExternalAuthority = ExternalAuthority {
uri: Uri {
scheme: Https
locator: "man7.org/linux/man-pages/man7/signal.7.html"
}
}

// The closed set of names, so a misspelled or unlisted signal has no constructor; the one string
// parse is linux_standard_signal_of_name, at the systemd $EXIT_STATUS boundary.
type LinuxStandardSignal
= SignalHup
| SignalInt
| SignalQuit
| SignalIll
| SignalTrap
| SignalAbrt
| SignalBus
| SignalFpe
| SignalKill
| SignalUsr1
| SignalSegv
| SignalUsr2
| SignalPipe
| SignalAlrm
| SignalTerm
| SignalStkflt
| SignalChld
| SignalCont
| SignalStop
| SignalTstp
| SignalTtin
| SignalTtou
| SignalUrg
| SignalXcpu
| SignalXfsz
| SignalVtalrm
| SignalProf
| SignalWinch
| SignalIo
| SignalPwr
| SignalSys

fn linux_standard_signal_of_name(name: String) -> LinuxStandardSignal? {
if name == "HUP" { Present { value: SignalHup } }
else if name == "INT" { Present { value: SignalInt } }
else if name == "QUIT" { Present { value: SignalQuit } }
else if name == "ILL" { Present { value: SignalIll } }
else if name == "TRAP" { Present { value: SignalTrap } }
else if name == "ABRT" { Present { value: SignalAbrt } }
else if name == "BUS" { Present { value: SignalBus } }
else if name == "FPE" { Present { value: SignalFpe } }
else if name == "KILL" { Present { value: SignalKill } }
else if name == "USR1" { Present { value: SignalUsr1 } }
else if name == "SEGV" { Present { value: SignalSegv } }
else if name == "USR2" { Present { value: SignalUsr2 } }
else if name == "PIPE" { Present { value: SignalPipe } }
else if name == "ALRM" { Present { value: SignalAlrm } }
else if name == "TERM" { Present { value: SignalTerm } }
else if name == "STKFLT" { Present { value: SignalStkflt } }
else if name == "CHLD" { Present { value: SignalChld } }
else if name == "CONT" { Present { value: SignalCont } }
else if name == "STOP" { Present { value: SignalStop } }
else if name == "TSTP" { Present { value: SignalTstp } }
else if name == "TTIN" { Present { value: SignalTtin } }
else if name == "TTOU" { Present { value: SignalTtou } }
else if name == "URG" { Present { value: SignalUrg } }
else if name == "XCPU" { Present { value: SignalXcpu } }
else if name == "XFSZ" { Present { value: SignalXfsz } }
else if name == "VTALRM" { Present { value: SignalVtalrm } }
else if name == "PROF" { Present { value: SignalProf } }
else if name == "WINCH" { Present { value: SignalWinch } }
else if name == "IO" { Present { value: SignalIo } }
else if name == "PWR" { Present { value: SignalPwr } }
else if name == "SYS" { Present { value: SignalSys } }
else { none }
}

fn linux_standard_signal_number(signal: LinuxStandardSignal) -> Int {
match signal {
SignalHup => 1
SignalInt => 2
SignalQuit => 3
SignalIll => 4
SignalTrap => 5
SignalAbrt => 6
SignalBus => 7
SignalFpe => 8
SignalKill => 9
SignalUsr1 => 10
SignalSegv => 11
SignalUsr2 => 12
SignalPipe => 13
SignalAlrm => 14
SignalTerm => 15
SignalStkflt => 16
SignalChld => 17
SignalCont => 18
SignalStop => 19
SignalTstp => 20
SignalTtin => 21
SignalTtou => 22
SignalUrg => 23
SignalXcpu => 24
SignalXfsz => 25
SignalVtalrm => 26
SignalProf => 27
SignalWinch => 28
SignalIo => 29
SignalPwr => 30
SignalSys => 31
}
}
201 changes: 201 additions & 0 deletions dag/extdeps/systemd/service_exec.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,201 @@
module extdeps.systemd.service_exec

import std.types { String, NonEmptyStr, List, Bool }
import extdeps.external_authority { ExternalAuthority, ExternalModelScope, ExternalSubjectRef }
import std.decl_ref { DeclarationRef, WholeDeclaration }
import extdeps.uri { Uri, Https }
import extdeps.exec.command { ArgvCommand, argv_words }

// WHAT THE SERVICE MANAGER HANDS A STOP COMMAND, and how a command line is spelled to it. Two
// upstream facts, both from systemd's own manuals, and nothing about any one consumer: which unit
// carries a stop hook, what it writes and where are workflow facts that live with the workflow.

data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority {
uri: Uri {
scheme: Https
locator: "www.freedesktop.org/software/systemd/man/latest/systemd.exec.html#Environment%20Variables%20Set%20or%20Propagated%20by%20the%20Service%20Manager"
}
}

data systemd_service_command_lines_authority: ExternalAuthority = ExternalAuthority {
uri: Uri {
scheme: Https
locator: "www.freedesktop.org/software/systemd/man/latest/systemd.service.html#Command%20lines"
}
}

data extdeps_model_scope: ExternalModelScope = ExternalModelScope {
subject: ExternalSubjectRef {
declaration: DeclarationRef {
module_path: "extdeps.systemd.service_exec",
decl_name: "ServiceStopVariable",
field: WholeDeclaration
}
},
first_citation: extdeps_external_authority_anchor,
further_citations: [systemd_service_command_lines_authority]
}

// systemd.exec(5), "Environment Variables Set or Propagated by the Service Manager":
// $INVOCATION_ID -- set for every process the manager spawns for the unit: the unit's current
// invocation, a 128-bit id formatted as 32 lowercase hex characters.
// $SERVICE_RESULT -- set for ExecStop= and ExecStopPost= only: the service's result, one of the
// words below.
// $EXIT_CODE -- set for ExecStop= and ExecStopPost= only: how the main process ended:
// "exited", "killed" or "dumped" (empty if it never ran).
// $EXIT_STATUS -- set for ExecStop= and ExecStopPost= only: the numeric exit status when
// $EXIT_CODE is "exited", otherwise the signal NAME (e.g. "TERM").
// They exist only while the stop command runs, so a record of the main process's end that survives
// the unit has to be written by that command, from these values.
type ServiceStopVariable
= InvocationIdVariable
| ServiceResultVariable
| ExitCodeVariable
| ExitStatusVariable

fn service_stop_variable_name(variable: ServiceStopVariable) -> NonEmptyStr {
match variable {
InvocationIdVariable => "INVOCATION_ID" as NonEmptyStr
ServiceResultVariable => "SERVICE_RESULT" as NonEmptyStr
ExitCodeVariable => "EXIT_CODE" as NonEmptyStr
ExitStatusVariable => "EXIT_STATUS" as NonEmptyStr
}
}

// $SERVICE_RESULT's documented words (systemd.exec(5)). An unlisted word is carried, not dropped:
// a manager newer than this model may add one, and the reader must say so rather than guess.
type ServiceResult
= ServiceResultSuccess
| ServiceResultProtocol
| ServiceResultTimeout
| ServiceResultExitCode
| ServiceResultSignal
| ServiceResultCoreDump
| ServiceResultWatchdog
| ServiceResultStartLimitHit
| ServiceResultResources
| ServiceResultOomKill
| ServiceResultUnlisted { word: String }

fn service_result_of_wire(word: String) -> ServiceResult {
if word == "success" { ServiceResultSuccess }
else if word == "protocol" { ServiceResultProtocol }
else if word == "timeout" { ServiceResultTimeout }
else if word == "exit-code" { ServiceResultExitCode }
else if word == "signal" { ServiceResultSignal }
else if word == "core-dump" { ServiceResultCoreDump }
else if word == "watchdog" { ServiceResultWatchdog }
else if word == "start-limit-hit" { ServiceResultStartLimitHit }
else if word == "resources" { ServiceResultResources }
else if word == "oom-kill" { ServiceResultOomKill }
else { ServiceResultUnlisted { word: word } }
}

// $EXIT_CODE's documented words. "Exited" carries a numeric status; the other two carry a signal
// name, and the two are different facts -- a process killed by SIGTERM did not exit 15.
type ServiceExitCode
= ServiceExitCodeExited
| ServiceExitCodeKilled
| ServiceExitCodeDumped
| ServiceExitCodeUnlisted { word: String }

fn service_exit_code_of_wire(word: String) -> ServiceExitCode {
if word == "exited" { ServiceExitCodeExited }
else if word == "killed" { ServiceExitCodeKilled }
else if word == "dumped" { ServiceExitCodeDumped }
else { ServiceExitCodeUnlisted { word: word } }
}

// ONE PIECE OF A COMMAND-LINE WORD: text the manager passes through unchanged, or a variable it
// substitutes. systemd.service(5), "Command lines": "${FOO}" used as part of a word is replaced by
// the variable's value with no word splitting, which is the form used here; the bare "$FOO" form
// word-splits and is not modeled. Keeping the two pieces apart is what lets the renderer refuse a
// literal that would be read as an expansion, instead of trusting that a string happens not to
// contain one.
type ExecWordPart
= ExecLiteral { text: String }
| ExecVariable { variable: ServiceStopVariable }

type ExecWordRendering
= ExecWordRendered { word: NonEmptyStr }
| ExecWordRefused { reason: NonEmptyStr }

// A literal is refused, never escaped, when it holds a character the command-line parser would
// treat as syntax: whitespace or a quote (word boundaries), a backslash (escapes), "$" (expansion)
// or "%" (unit specifiers). Escaping would be a second grammar to get right; every literal this
// repository mints is a path or an identifier that has no need of those characters.
fn exec_literal_admissible(text: String) -> Bool {
!(string_contains(s: text, pattern: " ") || string_contains(s: text, pattern: "\t") || string_contains(s: text, pattern: "\n") || string_contains(s: text, pattern: "\"")
|| string_contains(s: text, pattern: "'") || string_contains(s: text, pattern: "\\") || string_contains(s: text, pattern: "$") || string_contains(s: text, pattern: "%"))
}

fn exec_word_render(parts: List<ExecWordPart>) -> ExecWordRendering {
let refused = parts |> flat_map(p => match p {
ExecLiteral { text } => if exec_literal_admissible(text: text) { [] as List<String> } else { [text] }
ExecVariable { variable: _ } => [] as List<String>
})
match refused.first() {
Present { value: bad } =>
ExecWordRefused { reason: join(["command-line literal carries a character systemd would read as syntax: ", bad], "") as NonEmptyStr }
Absent => {
let word = join(parts |> map(p => match p {
ExecLiteral { text } => text
ExecVariable { variable } => join(["${", service_stop_variable_name(variable: variable) as String, "}"], "")
}), "")
if string_length(s: word) == 0 {
ExecWordRefused { reason: "an empty command-line word cannot be spelled to systemd" as NonEmptyStr }
} else {
ExecWordRendered { word: word as NonEmptyStr }
}
}
}
}

type ExecCommandLineRendering
= ExecCommandLineRendered { line: NonEmptyStr }
| ExecCommandLineRefused { reason: NonEmptyStr }

// AN ARGV AS ONE ExecStart=/ExecStopPost= VALUE. The manager splits the value on whitespace into
// words, the first naming the program, and runs it directly: no shell is involved at any point
// (systemd.service(5), "Command lines"), which is why a typed argv can be handed over at all. Every
// word passes the same admissibility test as a literal part, except that a word rendered from parts
// by exec_word_render may carry the "${...}" its variables were spelled as; that form is re-checked
// below rather than trusted.
fn exec_command_line(command: ArgvCommand) -> ExecCommandLineRendering {
let words = argv_words(command: command)
let refused = words |> filter(w => !exec_literal_admissible(text: w) && !exec_word_is_rendered_expansion(word: w))
match refused.first() {
Present { value: bad } =>
ExecCommandLineRefused { reason: join(["argv word carries a character systemd would read as syntax: ", bad], "") as NonEmptyStr }
Absent => ExecCommandLineRendered { line: join(words, " ") as NonEmptyStr }
}
}

// THE "+" COMMAND-LINE PREFIX, from the special executable prefixes systemd.service(5) documents
// ("Command lines"): it runs that one command with full privileges -- outside the unit's file-system
// namespacing and sandboxing (ProtectSystem=, ProtectHome=, ReadWritePaths= and the rest), while the
// main process keeps them. That is what lets a stop hook write where the unit's own process may not.
// In a user manager "full privileges" are the user's own; the prefix never grants more than the
// manager's principal holds. It is the only prefix this repository uses, so it is one function rather
// than a coproduct of one.
data exec_full_privileges_prefix: String = "+"

fn exec_command_line_full_privileges(command: ArgvCommand) -> ExecCommandLineRendering {
match exec_command_line(command: command) {
ExecCommandLineRefused { reason } => ExecCommandLineRefused { reason: reason }
ExecCommandLineRendered { line } => ExecCommandLineRendered { line: join([exec_full_privileges_prefix, line as String], "") as NonEmptyStr }
}
}

// A WORD WHOSE ONLY SYNTAX IS "${NAME}" FOR A MODELED VARIABLE. Re-reading the rendered word, not
// trusting a flag beside it: strip every modeled expansion, and the remainder must be an
// admissible literal. A "$" anywhere else -- an unmodeled variable, a bare $FOO -- survives the
// strip and refuses.
fn exec_word_is_rendered_expansion(word: String) -> Bool {
let stripped = fold(
[InvocationIdVariable, ServiceResultVariable, ExitCodeVariable, ExitStatusVariable],
init: word,
f: (acc, v) => replace(acc, join(["${", service_stop_variable_name(variable: v) as String, "}"], ""), ""),
)
stripped != word && exec_literal_admissible(text: stripped)
}
15 changes: 14 additions & 1 deletion dag/extdeps/systemd/systemd.dag
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ import std.algebra { trim }
import std.types { List }
import std.nat { Nat }
import std.measure {
ByteSize, byte_size, byte_size_count, Microsecond, microsecond, microsecond_count,
ByteSize, byte_size, byte_size_count, Microsecond, microsecond, microsecond_count, Second, second_count,
HardwareThreadCount, hardware_thread_count_value,
milli_per_unit, micro_per_unit, seconds_per_minute, minutes_per_hour,
}
Expand Down Expand Up @@ -71,6 +71,7 @@ type SystemdUnitProperty
| Result
| ExecMainStatus
| ExecStartProperty
| ExecStopPostProperty
| User
| WorkingDirectoryProperty
| RuntimeDirectoryProperty
Expand All @@ -96,6 +97,8 @@ type SystemdUnitProperty
| PrivateTmpProperty
| ReadWritePathsProperty
| RemainAfterExitProperty
| RuntimeMaxSecProperty
| CollectModeProperty
| JobProperty

// THE WIRE SPELLING AS A SEALED WORD, SO THE CLOSED TYPE SURVIVES ALL THE WAY TO THE ARGV.
Expand Down Expand Up @@ -147,6 +150,7 @@ fn systemd_unit_property_wire(property: SystemdUnitProperty) -> NonEmptyStr {
Result => "Result" as NonEmptyStr
ExecMainStatus => "ExecMainStatus" as NonEmptyStr
ExecStartProperty => "ExecStart" as NonEmptyStr
ExecStopPostProperty => "ExecStopPost" as NonEmptyStr
User => "User" as NonEmptyStr
WorkingDirectoryProperty => "WorkingDirectory" as NonEmptyStr
RuntimeDirectoryProperty => "RuntimeDirectory" as NonEmptyStr
Expand All @@ -172,6 +176,8 @@ fn systemd_unit_property_wire(property: SystemdUnitProperty) -> NonEmptyStr {
PrivateTmpProperty => "PrivateTmp" as NonEmptyStr
ReadWritePathsProperty => "ReadWritePaths" as NonEmptyStr
RemainAfterExitProperty => "RemainAfterExit" as NonEmptyStr
RuntimeMaxSecProperty => "RuntimeMaxSec" as NonEmptyStr
CollectModeProperty => "CollectMode" as NonEmptyStr
JobProperty => "Job" as NonEmptyStr
}
}
Expand Down Expand Up @@ -257,6 +263,13 @@ fn systemd_time_span_split(part: String) -> SystemdTimeSpanPart? {
}
}

// THE TYPED QUANTITY RENDERED TO SYSTEMD'S TIME-SPAN SPELLING, at the boundary and nowhere else: a
// duration is authored as a Second and only its systemd text is a string, so no consumer parses text to
// recover the number. Whole seconds with the `s` unit are a spelling systemd_duration_usec reads back.
fn systemd_time_span_of_seconds(d: Second) -> NonEmptyStr {
join([to_string(second_count(s: d)), "s"], "") as NonEmptyStr
}

fn systemd_duration_usec(text: String) -> Microsecond? {
let parts = filter(split(s: trim(s: text), delimiter: " "), p => p != "")
if list_length(items: parts) == 0 {
Expand Down
Loading
Loading