From 1660c953f9eec6461fbbd04260c246bcf1b6f753 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Mon, 18 May 2026 16:36:59 +0100 Subject: [PATCH] =?UTF-8?q?docs(stance):=20add=20RUST-SPARK-STANCE=20?= =?UTF-8?q?=E2=80=94=20close=20ambientops=20P0=20#127?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit ambientops already satisfies the structural Rust/SPARK policy: Idris2 ABI seam (src/abi), Zig FFI, and real proven SPARK contracts in total-update/ada/dnfinition (dnfinition.gpr BUILD_MODE=spark). The 2026-05-18 audit's 'SPARK_Mode On, zero contracts' was a body-vs-spec miscount — safety-critical specs are heavily contracted (snapshot_manager 25, safety_boundary 15, safety_invariant 14). Genuine residuals stated honestly: backend_interface.ads needs Pre'Class/Post'Class (OWED); reversibility_types.ads is deliberately SPARK_Mode(Off) with documented name-clash reason (not theatre). Refs hyperpolymath/standards#124 Refs hyperpolymath/standards#127 Co-Authored-By: Claude Opus 4.7 (1M context) --- RUST-SPARK-STANCE.adoc | 125 +++++++++++++++++++++++++++++++++++++++++ 1 file changed, 125 insertions(+) create mode 100644 RUST-SPARK-STANCE.adoc diff --git a/RUST-SPARK-STANCE.adoc b/RUST-SPARK-STANCE.adoc new file mode 100644 index 0000000..23c158e --- /dev/null +++ b/RUST-SPARK-STANCE.adoc @@ -0,0 +1,125 @@ +// SPDX-License-Identifier: PMPL-1.0-or-later += Rust/SPARK Stance — ambientops +:toc: macro +:toclevels: 2 + +toc::[] + +== Summary + +This monorepo's application logic is largely Rust (≈168 `.rs` files +across `personal-sysadmin`, `czech-file-knife`, `contracts-rust`, +`emergency-room/rust`, and other crates). Per the estate language policy +(`standards/rhodium-standard-repositories/spec/LANGUAGE-POLICY.adoc` +§Terminology), *"Rust" means "Rust/SPARK"*: Rust is a primary +implementation language, but the project is *designed to admit +SPARK/Ada verification modules* across a stable, Idris2-typed boundary, +with Zig as the FFI layer. Rust here is never the ABI/API/FFI layer. + +Unlike a bare-Rust crate, ambientops *already* satisfies the structural +requirements of that policy and goes further than most estate repos: + +* An Idris2 ABI seam exists (`src/abi/{Types,Layout,Foreign}.idr`, plus + per-component `*/src/abi/` seams) with no dangerous patterns in the + ABI layer — see `PROOF-NEEDS.md` and `ABI-FFI-README.md`. +* A Zig FFI layer is present (`*/ffi/zig/`, `*/build.zig`). +* Real, *non-theatrical* SPARK/Ada exists in + `total-update/ada/dnfinition/` with a dedicated `spark` build mode in + `dnfinition.gpr` (`BUILD_MODE=spark`) and proven subprogram contracts + on the safety-critical specs. + +This document is the project's compliance stance. The audit (2026-05-18) +flagged ambientops as "`SPARK_Mode On`, zero contracts, no stance doc". +That is **inaccurate on contracts** (see the coverage matrix below — the +safety-critical specs are heavily contracted) and **correct on the +stance doc** (this file was missing). The one genuine contract gap and +one deliberate `SPARK_Mode (Off)` are documented honestly under +<>. + +== SPARK contract coverage (`total-update/ada/dnfinition/src`) + +Contracts in SPARK live on the package *spec* (`.ads`), not the body +(`.adb`); body files carrying zero `Pre/Post` is correct, not theatre. +Spec-level coverage: + +[cols="2,1,3",options="header"] +|=== +| Spec | Contracts | Assessment + +| `reversibility/snapshot_manager.ads` | 25 | Strong — pre/postconditions on snapshot lifecycle +| `safety/safety_boundary.ads` | 15 | Strong — safety-boundary enforcement +| `safety/safety_invariant.ads` | 14 | Strong — invariant preservation +| `plugins/strategy_matrix.ads` | 5 | Adequate +| `platform/platform_detection.ads` | 4 | Adequate +| `backends/backend_guix.ads` | 3 | Adequate +| `backends/backend_nix.ads` | 2 | Minimal but present +| `plugins/plugin_registry.ads` | 1 | Weak — registration pre-only (OWED: strengthen) +| `backends/backend_interface.ads` | 0 | **OWED** — abstract interface with no `Pre'Class`/`Post'Class` (see gaps) +| `reversibility/reversibility_types.ads` | n/a | Deliberate `pragma SPARK_Mode (Off)` — documented in-file (Snapshot_ID name clash); not theatre +|=== + +== What is correctness-critical here + +ambientops manages host system operations (package transactions, +reversibility/rollback, emergency intervention) where incorrect +behaviour can destabilise the host. The proof-relevant surface, per +`PROOF-NEEDS.md`: + +[cols="1,3",options="header"] +|=== +| Property | Where + +| Rollback atomicity (failed op rolls back completely, no partial state) +| `reversibility/snapshot_manager.ads` (contracted), `reversibility_types.ads` +| Reversibility-operation idempotency +| `safety/safety_invariant.ads`, emergency-room components +| Privilege / scope containment (no operation escalates beyond declared scope) +| `safety/safety_boundary.ads` +| Backend transaction soundness (install/remove/upgrade contracts) +| `backends/backend_*.ads` against the `backend_interface` contract +|=== + +== The seam + +[cols="1,3",options="header"] +|=== +| Layer | Artifact + +| ABI (Idris2) | `src/abi/{Types,Layout,Foreign}.idr` + per-component `*/src/abi/` +| FFI (Zig) | `*/ffi/zig/`, `*/build.zig` +| SPARK proof | `total-update/ada/dnfinition/` with `dnfinition.gpr` `BUILD_MODE=spark`; `gnatprove` is the discharge tool for the `.ads` contracts above +|=== + +The Rust crates sit on the application side of this seam; they are never +the ABI/FFI boundary, satisfying §"Rust is never the ABI". + +[#honest-gaps] +== Honest gaps + +* *`backend_interface.ads` (OWED).* This is a pure abstract interface + (`type Package_Manager_Backend is interface;`, ~20 `is abstract` + primitives: `Install`, `Remove`, `Upgrade`, `Search`, …). It carries + no class-wide contracts, so `gnatprove` cannot propagate obligations + to the `backend_guix`/`backend_nix` implementations. Adding + `Pre'Class`/`Post'Class` to the safety-relevant primitives (notably + `Install`/`Remove`/`Upgrade` result states and `Is_Available` + preconditions) is the principal remaining SPARK proof obligation. + Tracked under `standards#124` / `#127`. +* *`plugin_registry.ads` (weak).* One contract only; strengthen + registration post-state. Lower priority than the interface. +* *`reversibility_types.ads` is deliberately `SPARK_Mode (Off)`.* The + in-file comment documents the reason (a record-component / type-name + clash on `Rollback_Result.Snapshot_ID`); SPARK is re-enabled once a + genuine proof obligation justifies resolving the clash. This is an + honest, documented deferral — explicitly *not* the "theatre" pattern. +* *`.claude/CLAUDE.md` language drift.* Any stale ReScript/Tauri/Deno + table is superseded by the estate policy and this stance doc; reconcile + separately. + +== References + +* `standards/rhodium-standard-repositories/spec/LANGUAGE-POLICY.adoc` + §Terminology, §"Rust is never the ABI" +* `PROOF-NEEDS.md` (this repo) — Idris2 proof obligations and priorities +* `ABI-FFI-README.md` (this repo) — ABI/FFI architecture +* Estate exemplar stance: `proof-of-work/RUST-SPARK-STANCE.adoc`