Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
53 commits
Select commit Hold shift + click to select a range
0f46242
FCI-1: bind exact Work through durable cell reservation
Aug 30, 2026
babdd79
FCI-1: restore reservation availability on every exit
Aug 30, 2026
f145b2e
FCI-1: wire fabric-only convergence and observed source
Aug 30, 2026
3da98de
Derive FCI-1 sudoers precondition from projection
Aug 30, 2026
324fa44
Repair FCI-1 allocation lifecycle evidence
Aug 31, 2026
2020e22
Strengthen FCI-1 terminal observations
Aug 31, 2026
2c1cac9
Strengthen FCI-1 wet failure receipts
Aug 31, 2026
c8eb7b2
Close FCI-1 wet failure paths
Aug 31, 2026
f4d1c09
Fix FCI-1 cleanup disposition closure
Aug 31, 2026
e825f0e
Repair rebased FCI-1 sources
Aug 31, 2026
ba4f9d3
Fix binding sample effect declaration
Aug 31, 2026
4803997
Close FCI-1 binding sample scope
Aug 31, 2026
76dda1c
Handle all reservation refusal outcomes
Aug 31, 2026
24d8207
Complete reservation refusal match
Aug 31, 2026
2b1e62a
Bind cleanup disposition within refusal fold
Aug 31, 2026
cea07c8
Keep cleanup disposition in decoded observation scope
Aug 31, 2026
298e661
Close FCI-1 reservation cleanup edges
Aug 31, 2026
e322781
Bind instrument processes to derived checkout root
Sep 2, 2026
ab345b8
Accept git worktree roots for cwd binding
Sep 2, 2026
42d4a0f
Carry typed properties through systemd transient runs
Sep 2, 2026
ca64d28
Render typed properties before transient transport
Sep 2, 2026
e916c54
Render systemd-run properties into the executed argv
Sep 2, 2026
93b618f
Compare argv by token identity, not by joined text
Sep 2, 2026
2513771
Model the bounded FCI-1 execution context
Sep 2, 2026
a396af6
Project the FCI-1 context to systemd
Sep 2, 2026
338ab82
Preserve exact exits from waited transient units
Sep 2, 2026
4c42c00
Roster the bounded FCI-1 bootstrap projection
Sep 2, 2026
95fc782
Run FCI-1 under bounded collected transient units
Sep 2, 2026
6b91a3c
Regenerate gitattributes for bounded context artifact
Sep 2, 2026
c01e056
Use generated ordering for gitattributes projection
Sep 2, 2026
81e15e6
Enroll FCI-1 witnesses in required floor
Sep 2, 2026
ca440bb
Make systemd property witness predicates total
Sep 2, 2026
88a8c85
Close FCI-1 declaration and projection witnesses
Sep 2, 2026
8265651
Require singleton held account before release
Sep 2, 2026
6d66d38
Roster FCI1 cleanup wildcard residues
Sep 2, 2026
bd8af1f
Make cleanup observation dispatch total
Sep 2, 2026
91b10cc
Avoid sentinel classification in cleanup authority
Sep 2, 2026
f3013cc
Validate replacement prestate before write
Sep 2, 2026
647fbcb
Return prestate refusal before actuation
Sep 2, 2026
3049061
Close checkpoint branch before replacement
Sep 2, 2026
91d61b2
Merge remote-tracking branch 'origin/main' into session/smart-wren-406
Sep 2, 2026
775e767
Update artifact roster witness count after main merge
Sep 2, 2026
7c9a21b
Make FCI1 artifact witness presence exact once
Sep 2, 2026
5aafd56
Derive emitted systemd property names from carrier
Sep 2, 2026
2a8cae8
Derive unbounded control property name
Sep 2, 2026
2096864
Derive MemoryMax names in FCI1 emit witness
Sep 2, 2026
a0e7476
Derive all property names in FCI1 witness
Sep 2, 2026
a133402
Import filter from algebra in artifact witness
Sep 2, 2026
f87bb48
Merge remote-tracking branch 'origin/main' into session/smart-wren-406
Sep 3, 2026
d9ce234
Regenerate witnesses workflow projection
Sep 3, 2026
4c99253
Remove inert FCI1 systemd projection witness
Sep 3, 2026
3698e28
Remove inert FCI1 systemd projection witness
Sep 3, 2026
68d3475
Resolve witness cleanup merge
Sep 3, 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 .gitattributes
Original file line number Diff line number Diff line change
Expand Up @@ -46,6 +46,7 @@ provisioning/srv3/gunbc-ghrunner.sudoers merge=generated-artifact
provisioning/srv4/gunbc-ghrunner.sudoers merge=generated-artifact
src/v1/stage0/src/bootstrap_stage0_crate_layout_generated.rs merge=generated-artifact
src/v1/stage0/src/v1_interpreter_dispatch_generated.rs merge=generated-artifact
tools/fabric_ci_fci1_bounded_execution_context.env merge=generated-artifact
src/v1/stage0/src/*.rs merge=generated-artifact
src/v1/stage0/Cargo.toml merge=generated-artifact
src/v1/stage0/src/behavioral_receipt_host.rs !merge
Expand Down
1 change: 1 addition & 0 deletions .github/workflows/witnesses.yml
Original file line number Diff line number Diff line change
Expand Up @@ -451,6 +451,7 @@ jobs:
if [ -e "dag/gunbc/stage0/stage0_crate_partition_generated.dag" ]; then git add "dag/gunbc/stage0/stage0_crate_partition_generated.dag"; else echo "chore-heal: registered generated artifact absent on this tree, not staging: dag/gunbc/stage0/stage0_crate_partition_generated.dag"; fi
if [ -e "dag/gunbc/stage0/stage0_executable_assembly_generated.dag" ]; then git add "dag/gunbc/stage0/stage0_executable_assembly_generated.dag"; else echo "chore-heal: registered generated artifact absent on this tree, not staging: dag/gunbc/stage0/stage0_executable_assembly_generated.dag"; fi
if [ -e "src/v1/stage0/src/v1_interpreter_dispatch_generated.rs" ]; then git add "src/v1/stage0/src/v1_interpreter_dispatch_generated.rs"; else echo "chore-heal: registered generated artifact absent on this tree, not staging: src/v1/stage0/src/v1_interpreter_dispatch_generated.rs"; fi
if [ -e "tools/fabric_ci_fci1_bounded_execution_context.env" ]; then git add "tools/fabric_ci_fci1_bounded_execution_context.env"; else echo "chore-heal: registered generated artifact absent on this tree, not staging: tools/fabric_ci_fci1_bounded_execution_context.env"; fi
if [ -e "provisioning/srv1/gunbc-ghrunner.sudoers" ]; then git add "provisioning/srv1/gunbc-ghrunner.sudoers"; else echo "chore-heal: registered generated artifact absent on this tree, not staging: provisioning/srv1/gunbc-ghrunner.sudoers"; fi
if [ -e "provisioning/srv2/gunbc-ghrunner.sudoers" ]; then git add "provisioning/srv2/gunbc-ghrunner.sudoers"; else echo "chore-heal: registered generated artifact absent on this tree, not staging: provisioning/srv2/gunbc-ghrunner.sudoers"; fi
if [ -e "provisioning/srv3/gunbc-ghrunner.sudoers" ]; then git add "provisioning/srv3/gunbc-ghrunner.sudoers"; else echo "chore-heal: registered generated artifact absent on this tree, not staging: provisioning/srv3/gunbc-ghrunner.sudoers"; fi
Expand Down
33 changes: 33 additions & 0 deletions dag/extdeps/systemd/systemctl.dag
Original file line number Diff line number Diff line change
Expand Up @@ -431,6 +431,39 @@ service systemd.Systemctl {
}
}

operation ListUnitsAllLoaded {
input {
pattern: NonEmptyStr,
unit_type: String = "service",
}
output {
stdout: String from "stdout"
success: Bool from "exit_success"
}
readonly
transport shell {
argv: [
"systemctl",
"list-units",
"--type={unit_type}",
"--all",
"--no-legend",
"--plain",
"{pattern}",
]
}
exit {
0 => Unit
nonzero => String "systemctl list-units --all failed"
}
mock_response {
0 => {
stdout: "actions-runner@srv3-01.service loaded active running GitHub Actions Runner\nactions-runner@srv3-02.service loaded inactive dead GitHub Actions Runner\n",
success: true,
} "hermetic systemd.Systemctl.ListUnitsAllLoaded (complete loaded-unit population)"
}
}

operation Status {
input { unit: NonEmptyStr }
output {
Expand Down
76 changes: 68 additions & 8 deletions dag/extdeps/systemd/systemd_run.dag
Original file line number Diff line number Diff line change
@@ -1,10 +1,16 @@
module extdeps.systemd.systemd_run

import std.types { NonEmptyStr, String, List, Bool }
import std.types { NonEmptyStr, String, List, Bool, Int }

import extdeps.external_authority { ExternalAuthority, ExternalModelScope, ExternalSubjectRef }
import std.decl_ref { DeclarationRef, WholeDeclaration }
import extdeps.uri { Uri, Https }
import extdeps.systemd { SystemdUnitProperty, systemd_unit_property_wire }

type SystemdRunProperty {
property: SystemdUnitProperty,
value: NonEmptyStr,
}

data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority {
uri: Uri {
Expand All @@ -17,7 +23,7 @@ data extdeps_model_scope: ExternalModelScope = ExternalModelScope {
subject: ExternalSubjectRef {
declaration: DeclarationRef {
module_path: "extdeps.systemd.systemd_run",
decl_name: "systemd_run_transient_unit_argv",
decl_name: "systemd.SystemdRun",
field: WholeDeclaration
}
},
Expand All @@ -27,23 +33,62 @@ data extdeps_model_scope: ExternalModelScope = ExternalModelScope {

data systemd_run_authority: ExternalAuthority = extdeps_external_authority_anchor

fn systemd_run_transient_unit_argv(unit: NonEmptyStr, command_argv: List<String>) -> List<String> {
// THE PROPERTY WORDS ARE RENDERED IN EXACTLY ONE PLACE, and that is the whole point of this
// function existing beside the full-line authority rather than inside it. A systemd unit property
// becomes an argv word here and nowhere else, so the operation's transport, the pure authority and
// every caller are reading one spelling. The transport CANNOT carry the typed record itself:
// push_shell_argv_tokens has arms for Str, List, ProcessArgvExpansion and a refusing arm for
// ambiguous free monoids, and a record reaches none of them — it lands in the catch-all, which
// Display-formats the value into a single argv word rather than refusing. So a record spliced into
// argv would hand systemd-run a fabricated argument at the exact seam that decides whether a unit
// is bounded. The typed population stays on this side of that boundary; only words cross it.
fn systemd_run_property_argv(properties: List<SystemdRunProperty>) -> List<String> {
fold(
command_argv,
init: ["systemd-run", concat("--unit=", unit as String), "--collect", "--"],
f: (acc, arg) => list_push(acc, arg),
properties,
init: [],
f: (acc, setting) => list_push(
acc,
concat(
"--property=",
concat(systemd_unit_property_wire(property: setting.property) as String, concat("=", setting.value as String)),
),
),
)
}

// The full invocation, and the authority the materialized operation argv is checked against. It
// COMPOSES the property words rather than re-deriving them; if this fold and the transport template
// ever disagree about word order, systemd_run_transient_operation_argv_matches_authority goes red.
fn systemd_run_transient_unit_argv(unit: NonEmptyStr, properties: List<SystemdRunProperty>, command_argv: List<String>) -> List<String> {
let launcher = ["systemd-run", concat("--unit=", unit as String), "--collect"]
let with_properties = fold(systemd_run_property_argv(properties: properties), init: launcher, f: (acc, word) => list_push(acc, word))
let with_separator = list_push(with_properties, "--")
fold(command_argv, init: with_separator, f: (acc, arg) => list_push(acc, arg))
}

// Waiting is a different operation from starting. It owns the complete wait/quiet/collect
// vocabulary and returns the process status as data: a nonzero child status is an observation,
// not an operation refusal. Default transient service semantics are deliberate. Type=oneshot is
// excluded because it collapses normal nonzero statuses to 1 (systemd issue 22812, observed on
// systemd 245 / 245.4-4ubuntu3.15); the same report establishes that signal death is not reliably
// recoverable as an exact child status through this boundary.
fn systemd_run_transient_wait_unit_argv(unit: NonEmptyStr, properties: List<SystemdRunProperty>, command_argv: List<String>) -> List<String> {
let launcher = ["systemd-run", concat("--unit=", unit as String), "--wait", "--quiet", "--collect"]
let with_properties = fold(systemd_run_property_argv(properties: properties), init: launcher, f: (acc, word) => list_push(acc, word))
let with_separator = list_push(with_properties, "--")
fold(command_argv, init: with_separator, f: (acc, arg) => list_push(acc, arg))
}


service systemd.SystemdRun {
operation RunTransient {
input { unit: NonEmptyStr, command_argv: List<String> }
input { unit: NonEmptyStr, property_argv: List<String>, command_argv: List<String> }
output {
success: Bool from "exit_success"
stdout: String from "stdout"
stderr: String from "stderr"
}
transport shell { argv: ["systemd-run", "--unit={unit}", "--collect", "--", command_argv] }
transport shell { argv: ["systemd-run", "--unit={unit}", "--collect", property_argv, "--", command_argv] }
exit {
0 => Unit
nonzero => String "systemd-run transient unit start failed"
Expand All @@ -52,4 +97,19 @@ service systemd.SystemdRun {
0 => { success: true, stdout: "Running as unit: demo.service", stderr: "" } "hermetic systemd.SystemdRun.RunTransient"
}
}


operation RunTransientAndWait {
input { unit: NonEmptyStr, property_argv: List<String>, command_argv: List<String> }
output {
exit_code: Int from "exit_code"
stdout: String from "stdout"
stderr: String from "stderr"
}
transport shell { argv: ["systemd-run", "--unit={unit}", "--wait", "--quiet", "--collect", property_argv, "--", command_argv] }
exit {
0 => Unit
nonzero => Unit
}
}
}
44 changes: 38 additions & 6 deletions dag/gunbc/fabric/fabric_cell_acquire.dag
Original file line number Diff line number Diff line change
Expand Up @@ -505,14 +505,30 @@ fn fabric_cell_unit_name_field(line: String) -> String {
// still returns a real probe: its namespaces were read, and the pure half decides what an empty
// expectation means. Supplying the roster from this side would be the observer reporting on what
// it happened to probe, which is the blindness the observe module's own header rules out.
func fabric_cell_probe_wet(host: HostIdentity) -> FabricCellHostProbe {
type FabricCellProbeReading sole_constructor {
probe: FabricCellHostProbe
boundary_readings: List<FabricCellBoundaryReading>
}

fn fabric_cell_probe_reading_probe(reading: FabricCellProbeReading) -> FabricCellHostProbe {
reading.probe
}

fn fabric_cell_probe_reading_boundaries(reading: FabricCellProbeReading) -> List<FabricCellBoundaryReading> {
reading.boundary_readings
}

// The receipt retains the same boundary readings used to construct the probe. Consumers needing
// raw values must project this value; independently re-reading the five properties would combine
// two host instants into one purported observation.
func fabric_cell_probe_reading_wet(host: HostIdentity) -> FabricCellProbeReading {
let root = fabric_cell_observe_cells_root()
let slices = fabric_cell_observe_slice_namespace()
let acquired = map(
fabric_cell_expected_slots(host: host),
s => fabric_cell_acquire_slot(slot: s, cells_root: root, slices: slices),
)
FabricCellHostProbe {
let probe = FabricCellHostProbe {
host: host,
namespaces: concat(
[
Expand All @@ -529,6 +545,14 @@ func fabric_cell_probe_wet(host: HostIdentity) -> FabricCellHostProbe {
),
addresses: flat_map(acquired, a => fabric_cell_acquisition_address_entries(acquisition: a)),
}
FabricCellProbeReading {
probe: probe,
boundary_readings: map(acquired, a => a.boundary_reading),
}
}

func fabric_cell_probe_wet(host: HostIdentity) -> FabricCellHostProbe {
fabric_cell_probe_reading_probe(reading: fabric_cell_probe_reading_wet(host: host))
}

// ONE SUBJECT IS ACQUIRED ONCE PER TICK, AND THE PROJECTIONS READ THE VALUE RATHER THAN THE HOST.
Expand All @@ -548,6 +572,7 @@ type FabricCellSlotAcquisition {
cell_root: FabricCellDirectoryObservation
attempt_root: FabricCellDirectoryObservation
boundary: List<FabricCellAddressProbeEntry>
boundary_reading: FabricCellBoundaryReading
}

func fabric_cell_acquire_slot(
Expand All @@ -556,14 +581,20 @@ func fabric_cell_acquire_slot(
slices: FabricCellNamespaceProbe,
) -> FabricCellSlotAcquisition {
let cell_root = fabric_cell_observe_cell_root(slot: slot, cells_root: cells_root)
let boundary_reading = match fabric_cell_boundary_standing(slot: slot, slices: slices) {
BoundaryAsk => fabric_cell_read_boundary(slot: slot)
BoundaryUnknownRefuse { cause: cause } => BoundaryReadRefused { cause: cause }
BoundaryAbsentNoAsk => BoundaryReadRefused { cause: "cell boundary slice is absent" }
}
FabricCellSlotAcquisition {
slot: slot,
cell_root: cell_root,
attempt_root: fabric_cell_observe_directory(
path: fabric_cell_attempt_root_path(slot: slot),
parent: fabric_cell_parent_standing_of(parent: cell_root, entry: fabric_cell_attempt_root_entry_name),
),
boundary: fabric_cell_boundary_address_entries(slot: slot, slices: slices),
boundary: fabric_cell_boundary_address_entries(slot: slot, slices: slices, reading: boundary_reading),
boundary_reading: boundary_reading,
}
}

Expand Down Expand Up @@ -687,6 +718,7 @@ fn fabric_cell_boundary_standing(
func fabric_cell_boundary_address_entries(
slot: RunnerSlotIdentity,
slices: FabricCellNamespaceProbe,
reading: FabricCellBoundaryReading,
) -> List<FabricCellAddressProbeEntry> {
match fabric_cell_boundary_standing(slot: slot, slices: slices) {
BoundaryAbsentNoAsk => []
Expand All @@ -696,21 +728,21 @@ func fabric_cell_boundary_address_entries(
address: FabricCellResourceBoundaryAddress,
probe: AddressStateReadRefused { cause: c },
}]
BoundaryAsk => [fabric_cell_boundary_probe_entry(slot: slot)]
BoundaryAsk => [fabric_cell_boundary_probe_entry(slot: slot, reading: reading)]
}
}

fn fabric_cell_entries_hold_name(entries: List<String>, name: String) -> Bool {
fold(entries, init: false, f: (acc, e) => acc || e == name)
}

func fabric_cell_boundary_probe_entry(slot: RunnerSlotIdentity) -> FabricCellAddressProbeEntry {
fn fabric_cell_boundary_probe_entry(slot: RunnerSlotIdentity, reading: FabricCellBoundaryReading) -> FabricCellAddressProbeEntry {
FabricCellAddressProbeEntry {
slot: slot,
address: FabricCellResourceBoundaryAddress,
probe: fabric_cell_boundary_address_probe(
slot: slot,
reading: fabric_cell_read_boundary(slot: slot),
reading: reading,
),
}
}
Expand Down
2 changes: 1 addition & 1 deletion dag/gunbc/fabric/fabric_ci_program.dag
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@ type FabricCiGate {
fn fabric_ci_gates() -> List<FabricCiGate> {
[
FabricCiGate { id: "FCI-0", owned_question: "What exactly will the fabric run?", exit_predicate: "The fabric possesses one exact required-witnesses-build Work carrying every execution-defining coordinate; moving or incomplete subjects refuse.", positive_control: "Identical semantic inputs derive the identical WorkKey.", discriminating_mutations: ["command-word", "environment-entry", "verified-tree", "toolchain-identity", "output-declaration"], frozen_output_identities: ["WorkKey", "source-tree-digest", "environment-materialization-digest"], non_goals: ["ExecutionGrant", "executor", "process-start", "cell-realization", "workflow-cutover"] },
FabricCiGate { id: "FCI-1", owned_question: "What bounded owned cell will realize this Work?", exit_predicate: "The exact Work realizes in exactly one bounded cell whose resources and ownership are explicit.", positive_control: "One exact Work realizes one bounded owned cell.", discriminating_mutations: ["unbounded-cell", "unowned-cell", "multiple-cells", "work-mismatch"], frozen_output_identities: ["cell-identity", "cell-resource-envelope", "cell-owner"], non_goals: ["ExecutionGrant", "process-start", "multi-host-scheduling"] },
FabricCiGate { id: "FCI-1", owned_question: "What durable reservation binds this exact Work to one already-converged bounded owned cell?", exit_predicate: "After installed-authorization, converged allocation-directory substrate, and exact-path owner/group readback succeed, one exact Work is bound to exactly one selected substrate-converged cell by one committed durable reservation generation. An independent observer reads the same reservation generation, demand/offer payload and content digest after the submitter terminates; release removes only the holding and returns the append-only allocation slot to Free at the exact next generation (SlotAbsent -> Held(1) -> Free(2), or SlotFree(N) -> Held(N+1) -> Free(N+2)), while leaving the persistent cell substrate unchanged. Directory mode remains explicitly unobserved and no Work process starts.", positive_control: "The exact-tree evidence calibration holds; installed sudoers, allocation-directory substrate, slot prestate, and cell owner/group readbacks match; a production reservation survives submitter termination, is independently re-observed byte-identically, releases through the production path, and leaves the slot semantically Free with durable generation history and the cell substrate unchanged.", discriminating_mutations: ["reservation-state-owned-by-submitter", "reservation-generation-changed-in-disposable-store", "reservation-payload-work-mismatch", "selected-offer-cell-mismatch", "cell-substrate-not-converged", "cell-resource-boundary-digest-mismatch", "reservation-release-not-observed", "reservation-unexpected-extra-generation", "reservation-release-destroys-cell-substrate", "multiple-cells", "unowned-cell"], frozen_output_identities: ["WorkKey", "DemandKey", "OfferKey", "CellId/slot-key", "committed-CAS-generation", "reservation-content-digest", "cell-resource-boundary-digest", "cell-owner-identity", "reservation-realization-digest", "allocation-store-path", "allocation-slot-prestate", "allocation-slot-exact-free-poststate"], non_goals: ["cell-supervisor", "passive-lease-unit", "InvocationID", "MainPID", "process-start-identity", "blocking-wait", "ExecutionGrant", "Work-process-start", "Attempt", "execution-Receipt", "source-to-application-structural-type-safety"] },
FabricCiGate { id: "FCI-2", owned_question: "Which sole grant authorizes this Work?", exit_predicate: "Selection, reservation and commitment yield exactly one fenced ExecutionGrant for the exact Work.", positive_control: "One admitted offer yields one committed grant.", discriminating_mutations: ["duplicate-grant", "expired-reservation", "work-mismatch"], frozen_output_identities: ["ExecutionGrant", "lease-epoch"], non_goals: ["process-start", "GitHub-conclusion"] },
FabricCiGate { id: "FCI-3", owned_question: "What causes the target process?", exit_predicate: "A persistent executor re-reads the committed Grant before starting; absent, corrupt or expired Grant yields zero target processes.", positive_control: "One live committed grant starts exactly one target process.", discriminating_mutations: ["grant-removed", "grant-corrupt", "grant-expired"], frozen_output_identities: ["attempt-identity", "process-observation"], non_goals: ["GitHub-conclusion", "multiple-host-scheduling"] },
FabricCiGate { id: "FCI-4", owned_question: "How is execution admitted once, deduplicated, released and sanitized?", exit_predicate: "One fenced Receipt is admitted at most once; duplicate delivery cannot duplicate standing, and the cell is released only after per-attempt sanitation is confirmed.", positive_control: "One matching Receipt is admitted once and its sanitized cell returns to supply.", discriminating_mutations: ["duplicate-receipt", "foreign-receipt", "release-before-sanitation", "failed-sanitation"], frozen_output_identities: ["admitted-receipt", "deduplication-key", "release-receipt", "sanitation-receipt"], non_goals: ["shadow-GitHub-job", "required-check-cutover"] },
Expand Down
Loading