Skip to content

feat(storage): add declarative disk layout reconciliation and kcoreOS… #14

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
rtacconi merged 2 commits into from
Apr 21, 2026
Merged

feat(storage): add declarative disk layout reconciliation and kcoreOS… #14

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
009aafd
feat(storage): add declarative disk layout reconciliation and kcoreOS…
rtacconi Apr 21, 2026
5cb1d41
fix(kctl): fallback certs dir when home is not writable
rtacconi Apr 21, 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
67 changes: 46 additions & 21 deletions .github/workflows/formal-checks.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -76,27 +76,51 @@ jobs:
# toolchain is identical), so the first shard to finish install
# warms the cache for all the others on subsequent runs.
kani-shard:
name: kani-shard / ${{ matrix.harness }}
name: kani-shard / ${{ matrix.crate }} :: ${{ matrix.harness }}
runs-on: ubuntu-latest
timeout-minutes: 15
strategy:
# `fail-fast: false` lets all 9 harnesses report results even
# `fail-fast: false` lets all harnesses report results even
# if one regresses; otherwise GHA cancels the rest and we lose
# signal on the others.
fail-fast: false
matrix:
# Fully-qualified harness paths from
# `crates/kcore-sanitize/src/lib.rs::kani_proofs`.
harness:
- kani_proofs::nix_escape_never_panics
- kani_proofs::nix_escape_output_is_always_safe
- kani_proofs::sanitize_nix_attr_key_preserves_char_count
- kani_proofs::sanitize_nix_attr_key_charset
- kani_proofs::dot_dot_check_never_panics
- kani_proofs::assert_safe_path_never_panics
- kani_proofs::assert_safe_path_acceptance_implies_safe
- kani_proofs::segment_validation_never_panics
- kani_proofs::segment_acceptance_implies_safe
# Fully-qualified harness paths from each crate's
# `kani_proofs` module. `crate` selects which workspace
# member `cargo kani -p` operates on.
include:
- crate: kcore-sanitize
harness: kani_proofs::nix_escape_never_panics
- crate: kcore-sanitize
harness: kani_proofs::nix_escape_output_is_always_safe
- crate: kcore-sanitize
harness: kani_proofs::sanitize_nix_attr_key_preserves_char_count
- crate: kcore-sanitize
harness: kani_proofs::sanitize_nix_attr_key_charset
- crate: kcore-sanitize
harness: kani_proofs::dot_dot_check_never_panics
- crate: kcore-sanitize
harness: kani_proofs::assert_safe_path_never_panics
- crate: kcore-sanitize
harness: kani_proofs::assert_safe_path_acceptance_implies_safe
- crate: kcore-sanitize
harness: kani_proofs::segment_validation_never_panics
- crate: kcore-sanitize
harness: kani_proofs::segment_acceptance_implies_safe
# `kcore-disko-types` is the shared, std-only crate used by
# both the controller pre-flight classifier and the node-
# agent authoritative classifier. The harnesses below cover
# the layout-diff parser (`extract_target_devices` +
# `strip_nix_comments`) — its post-conditions are what
# downstream classifier safety arguments rest on.
- crate: kcore-disko-types
harness: kani_proofs::extract_target_devices_never_panics
- crate: kcore-disko-types
harness: kani_proofs::strip_nix_comments_preserves_length
- crate: kcore-disko-types
harness: kani_proofs::extract_target_devices_outputs_dev_prefixed_paths
- crate: kcore-disko-types
harness: kani_proofs::extract_target_devices_is_deterministic
# Pinned kani-verifier version. Bumping this single env var
# (here AND in the cache key below) is the only change needed
# to roll forward; the install step honours it and the cache
Expand Down Expand Up @@ -125,7 +149,7 @@ jobs:
- name: Cache cargo registry + target
uses: Swatinem/rust-cache@v2
with:
shared-key: kani-${{ matrix.harness }}
shared-key: kani-${{ matrix.crate }}-${{ matrix.harness }}

# Caches the Kani toolchain itself (CBMC + symex binaries +
# ~/.kani layout). Cold install of kani-verifier from crates.io
Expand Down Expand Up @@ -216,11 +240,12 @@ jobs:
~/.kani
key: ${{ steps.kani-cache.outputs.cache-primary-key }}

# All proofs live in `kcore-sanitize`, a leaf crate with **no
# non-std dependencies**, so Kani only has to compile that one
# crate (a few seconds) instead of the full controller dep
# graph (rusqlite-bundled SQLite, rcgen+aws-lc-rs, tonic, ...
# which takes >20 min on a 4-vCPU GHA runner).
# Each proof lives in a leaf crate with **no non-std
# dependencies** (`kcore-sanitize`, `kcore-disko-types`), so
# Kani only has to compile that one crate (a few seconds)
# instead of the full controller dep graph (rusqlite-bundled
# SQLite, rcgen+aws-lc-rs, tonic, ... which takes >20 min on
# a 4-vCPU GHA runner).
#
# `--harness` is a substring match; we anchor with the full
# `kani_proofs::` module path so a future harness with a
Expand All @@ -232,7 +257,7 @@ jobs:
run: |
set -euo pipefail
cargo-kani --version
cargo kani -p kcore-sanitize \
cargo kani -p '${{ matrix.crate }}' \
--harness '${{ matrix.harness }}' \
--output-format terse

Expand Down
9 changes: 9 additions & 0 deletions Cargo.lock
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

1 change: 1 addition & 0 deletions Cargo.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
[workspace]
members = [
"crates/kcore-sanitize",
"crates/kcore-disko-types",
"crates/node-agent",
"crates/controller",
"crates/kctl",
Expand Down
2 changes: 1 addition & 1 deletion Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -92,7 +92,7 @@ iso:
@echo ""
@ls -lh result-iso/iso/*.iso
@echo ""
@echo "ISO built: result-iso/iso/nixos-kcore-$(VERSION)-x86_64-linux.iso"
@echo "ISO built: result-iso/iso/kcoreos-$(VERSION)-x86_64-linux.iso"

@coderabbitai coderabbitai Bot Apr 21, 2026

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

⚠️ Potential issue | 🟡 Minor

Update the help text to match the kcoreOS ISO rename.

Line 95 now reports a kcoreos-* ISO, but make help still describes the iso and iso-remote targets as “NixOS ISO”.

Suggested help text update 
-	`@echo` "  iso         Build NixOS ISO (Linux only)"
-	`@echo` "  iso-remote  Build NixOS ISO on remote Linux server (from macOS)"
+	`@echo` "  iso         Build kcoreOS ISO (Linux only)"
+	`@echo` "  iso-remote  Build kcoreOS ISO on remote Linux server (from macOS)"

Also applies to: 140-141

🤖 Prompt for AI Agents 
Verify each finding against the current code and only fix it if needed.

In `@Makefile` at line 95, The help text in the Makefile still calls the targets
"NixOS ISO" while the produced artifact and echo message use the new kcoreOS
name; update the help strings for the Makefile targets iso and iso-remote (and
any accompanying echo/help lines near the echo "@echo "ISO built:
result-iso/iso/kcoreos-$(VERSION)-x86_64-linux.iso" ) to refer to "kcoreOS ISO"
and the new kcoreos-$(VERSION)-x86_64-linux.iso naming so the output of make
help matches the actual ISO name and the iso/iso-remote target descriptions.


iso-remote:
@echo "Building kcore ISO $(V) on remote Linux server..."
Expand Down
1 change: 1 addition & 0 deletions crates/controller/Cargo.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ edition = "2021"
[dependencies]
anyhow = "1.0.102"
kcore-sanitize = { path = "../kcore-sanitize" }
kcore-disko-types = { path = "../kcore-disko-types" }
clap = { version = "4", features = ["derive"] }
pem = "3"
prost = "0.13"
Expand Down
Loading
Loading