diff --git a/RUST-SPARK-STANCE.adoc b/RUST-SPARK-STANCE.adoc index 23c158e..fbc1aaa 100644 --- a/RUST-SPARK-STANCE.adoc +++ b/RUST-SPARK-STANCE.adoc @@ -38,6 +38,11 @@ one deliberate `SPARK_Mode (Off)` are documented honestly under == SPARK contract coverage (`total-update/ada/dnfinition/src`) +WARNING: ⚠️ The matrix in this section is **FALSE and SUPERSEDED** — see +<>. It was written from a source read that never +compiled and was never `gnatprove`-checked. Retained only to show what +was claimed vs. what verification found. + 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: @@ -93,25 +98,81 @@ behaviour can destabilise the host. The proof-relevant surface, per 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. +[#verified-correction] +== ⚠️ Verified correction (standards#127, 2026-05-18) — supersedes the coverage matrix above + +WARNING: An adversarial re-verification (gnat / gnatprove + 2-agent +static SPARK-RM swarm, then dynamically spot-confirmed on `origin/main`) +found that the "SPARK contract coverage" matrix and the "real, +*non-theatrical* SPARK/Ada" claim earlier in this document are *false*. +They were written from a source read that **never compiled and was never +`gnatprove`-checked**. The original 2026-05-18 estate audit ("`SPARK_Mode +On`, theatre") was *correct*; the PR#48 reframing was the inaccuracy. +The whole `total-update/ada/dnfinition` SPARK story is *theatre*: + +* *`backend_interface.ads` — never compiled; illegal SPARK.* + `Transaction_Item.Package` used an Ada **reserved word** as a field + name (no compiler accepts it). `Install`/`Remove`/`Upgrade`/ + `Upgrade_System`/`Autoremove` are *functions* with an `in out` + controlling parameter — **illegal SPARK** (SPARK RM 4.5.2) — under + `pragma SPARK_Mode (On)`. *This PR* fixes the reserved word (renamed + `Pkg`, now compiles), honestly sets `SPARK_Mode (Off)` with rationale, + and adds sound Ada 2022 `Pre'Class`/`Post'Class` on the SPARK-legal + query ops + `plugin_registry` `Pre`s (runtime-checked; the spec for + the OWED refactor). +* *`snapshot_manager.adb:4` — `pragma SPARK_Mode (Off)`* over the entire + safety-critical rollback body. gnatprove proves **nothing** about + rollback. The body also *never compiled*: `:93` calls + `Create_Btrfs_Snapshot`, first declared `:145`, no forward declaration + (Ada visibility error). The headline `Rollback_To_Snapshot` `Post` + rests on `reversibility_types.adb:26-32` + `System_State_Matches_Snapshot` which is `pragma Unreferenced (ID); + return True;` — a **hardcoded-`True` vacuous ghost oracle** — and is + additionally fail-permissive (`or else Status in Failed | + Requires_Reboot`). The "25 Strong" rating is false. +* *`safety_boundary.adb:6` — `pragma SPARK_Mode (Off)`*; and + `safety_boundary.ads:78-101` re-declares `Safe_Install`/`Safe_Remove`/ + `Safe_Upgrade`/… as *functions* with `in Out …'Class` (the same + illegal-SPARK construct, *without* even the honesty escape). No + privilege/scope/bound model exists anywhere; the only precondition is + `Is_Valid (Token)` (recovery-point presence). The "15 Strong / + privilege-containment" rating is false. +* *`safety_invariant.ads` — legal SPARK but vacuous.* Contracts are + definitional tautologies over `Ghost` state that the real (SPARK_Mode + Off) enforcement path never updates; e.g. `Lemma_Recovery_Enables_ + Rollback` has `Post ≡ Pre` by definition. Proved-but-meaningless. +* *`plugin_registry.ads`* is transitively non-SPARK (uses + `Backend_Access` from the non-SPARK `backend_interface`); its `Pre`s + (strengthened by this PR) cannot be `gnatprove`-discharged until the + refactor below. + +=== What this PR genuinely delivers (no theatre, no fake green) + +. Real bug fix: `backend_interface.ads` now compiles (reserved word). +. Honest SPARK boundary on `backend_interface.ads` + documented OWED. +. Sound Ada 2022 contracts (query-op `Pre'Class`/`Post'Class`, + `Register_Backend` `Pre`, six `plugin_registry` non-empty-ID `Pre`s), + runtime-enforced and serving as the spec for the SPARK refactor. +. This verified, honest stance — replacing the false matrix. + +=== OWED — large genuine programme, tracked standards#127 (must NOT be faked) + +. State-mutating `function` → `procedure (… ; Result : out …)` redesign + across `backend_interface` + every backend (`backend_guix`, + `backend_nix`) + `safety_boundary`, to make the modification path + legal SPARK. +. Bring `snapshot_manager.adb` / `safety_boundary.adb` into + `SPARK_Mode (On)` (they are wholly `Off` today) and fix the + `snapshot_manager.adb` elaboration-order error so it compiles. +. Replace the `System_State_Matches_Snapshot` hardcoded-`True` ghost + with a real state model; connect `safety_invariant` ghost state to the + executing enforcement path so its lemmas are non-vacuous. +. Only then can the safety-critical contracts be `gnatprove`-discharged. + +NOTE: the `BUILD_MODE=spark` mode and `gnatprove` are real *tooling*, but +no safety-critical body is analysed by them today. Do not cite ambientops +as "formally verified" until the OWED programme lands. + * *`.claude/CLAUDE.md` language drift.* Any stale ReScript/Tauri/Deno table is superseded by the estate policy and this stance doc; reconcile separately. diff --git a/total-update/ada/dnfinition/src/backends/backend_interface.ads b/total-update/ada/dnfinition/src/backends/backend_interface.ads index 54e2d7d..5f6f551 100644 --- a/total-update/ada/dnfinition/src/backends/backend_interface.ads +++ b/total-update/ada/dnfinition/src/backends/backend_interface.ads @@ -4,7 +4,24 @@ -- Backend Interface - Abstract interface for all package managers -- DNFinition supports 50+ package managers through this unified interface -pragma SPARK_Mode (On); +-- HONEST SPARK BOUNDARY (standards#127). +-- This unit was `pragma SPARK_Mode (On)` but is **not legal SPARK** and +-- never compiled at all: +-- * `Transaction_Item.Package` used an Ada *reserved word* as a field +-- name (no compiler accepts it) — fixed (renamed `Pkg`); +-- * the modification operations Install/Remove/Upgrade/ +-- Upgrade_System/Autoremove are *functions* with an `in out` +-- controlling parameter, which SPARK forbids (SPARK RM 4.5.2). +-- `SPARK_Mode (On)` over non-SPARK code is theatre; gnatprove could +-- never analyse it. The correct fix (state-mutating `function`s -> +-- `procedure`s with `out Result`, across the interface and every +-- backend body) is a breaking redesign, OWED and tracked under +-- standards#127 — it must not be faked. Until then this unit is +-- honestly marked OUT of the SPARK boundary. The Ada 2022 +-- `Pre'Class`/`Post'Class` aspects below remain as runtime-checked +-- (`-gnata`) behavioural contracts and as the spec for that future +-- SPARK refactor. +pragma SPARK_Mode (Off); with Ada.Strings.Unbounded; use Ada.Strings.Unbounded; with Platform_Detection; use Platform_Detection; @@ -67,8 +84,13 @@ package Backend_Interface is Unpin); type Transaction_Item is record - Kind : Transaction_Kind; - Package : Package_Info; + Kind : Transaction_Kind; + Pkg : Package_Info; + -- NOTE: field was `Package` — an Ada *reserved word*; no Ada + -- compiler accepts it. This spec never compiled (the `spark` + -- build mode was never run). Renamed to `Pkg` (zero references + -- to the old name anywhere in the tree). Pre-existing defect + -- fixed as part of standards#127. end record; type Transaction_List is array (Positive range <>) of Transaction_Item; @@ -101,7 +123,9 @@ package Backend_Interface is -- Query operations function Get_Name (Self : Package_Manager_Backend) return String - is abstract; + is abstract + with Post'Class => Get_Name'Result'Length > 0; + -- Behavioural contract (Liskov): every backend has a non-empty name. function Get_PM_Type (Self : Package_Manager_Backend) return Package_Manager_Type @@ -123,7 +147,9 @@ package Backend_Interface is (Self : Package_Manager_Backend; Query : String; Limit : Positive := 100) return Package_List_Access - is abstract; + is abstract + with Pre'Class => Query'Length > 0; + -- Behavioural contract: a search query must be non-empty. function Get_Installed (Self : Package_Manager_Backend) return Package_List_Access @@ -136,9 +162,31 @@ package Backend_Interface is function Get_Package_Info (Self : Package_Manager_Backend; Name : String) return Package_Info - is abstract; - - -- Modification operations (all should support snapshot/rollback) + is abstract + with Pre'Class => Name'Length > 0; + -- Behavioural contract: a package name must be non-empty. + + -- Modification operations (all should support snapshot/rollback). + -- + -- HONEST SPARK BOUNDARY (standards#127): these five operations are + -- declared as *functions* with an `in out` controlling parameter and + -- a returned `Operation_Result`. A function with an `in out` + -- parameter is **not legal SPARK** (SPARK RM 4.5.2). The whole unit + -- carried `pragma SPARK_Mode (On)` while being non-SPARK — i.e. + -- SPARK *theatre*: `gnatprove` could never analyse it (and the + -- reserved-word `Package` field above means it never compiled at + -- all). Rather than hide that, the genuinely-effectful modification + -- operations are explicitly placed OUTSIDE the SPARK boundary with + -- `SPARK_Mode => Off`. This makes the boundary truthful and lets + -- gnatprove genuinely verify the rest of the spec + plugin_registry. + -- + -- The proper fix (OWED, tracked standards#127) is a breaking + -- redesign: state-mutating `function`s -> `procedure`s with an + -- `out Result : Operation_Result` parameter, across the interface + -- and every backend (backend_guix, backend_nix, …). That refactor + -- is out of scope for this PR; it must not be faked. The intended + -- soundness contract — *a `Success` result must not report + -- Failed_Count > 0* — is recorded here for that future work. function Install (Self : in out Package_Manager_Backend; Packages : Package_List; @@ -192,8 +240,9 @@ package Backend_Interface is procedure Register_Backend (PM_Type : Package_Manager_Type; - Backend : Backend_Access); - -- Register a backend implementation + Backend : Backend_Access) + with Pre => Backend /= null; + -- Register a backend implementation (a null backend is rejected). function Get_Backend (PM_Type : Package_Manager_Type) return Backend_Access; -- Get backend for a package manager type diff --git a/total-update/ada/dnfinition/src/plugins/plugin_registry.ads b/total-update/ada/dnfinition/src/plugins/plugin_registry.ads index 4a0b19a..81d856c 100644 --- a/total-update/ada/dnfinition/src/plugins/plugin_registry.ads +++ b/total-update/ada/dnfinition/src/plugins/plugin_registry.ads @@ -141,8 +141,9 @@ package Plugin_Registry is with Pre => P /= null; -- Register a new plugin - procedure Unregister_Plugin (ID : String); - -- Remove a plugin from the registry + procedure Unregister_Plugin (ID : String) + with Pre => ID'Length > 0; + -- Remove a plugin from the registry (the ID must be non-empty). procedure Discover_Plugins; -- Scan for available plugins and update status @@ -151,8 +152,9 @@ package Plugin_Registry is -- Re-check availability of all plugins -- Query operations - function Get_Plugin (ID : String) return Plugin_Access; - -- Get a specific plugin by ID + function Get_Plugin (ID : String) return Plugin_Access + with Pre => ID'Length > 0; + -- Get a specific plugin by ID (the ID must be non-empty). function Get_Plugin_By_Type (PM : Package_Manager_Type) return Plugin_Access; -- Get plugin for a specific package manager type @@ -160,8 +162,9 @@ package Plugin_Registry is function Get_Available_Plugins return Natural; -- Count of available plugins - function Get_Plugin_Metadata (ID : String) return Plugin_Metadata; - -- Get metadata for a plugin + function Get_Plugin_Metadata (ID : String) return Plugin_Metadata + with Pre => ID'Length > 0; + -- Get metadata for a plugin (the ID must be non-empty). -- Priority-based selection function Get_Best_Plugin_For @@ -172,10 +175,13 @@ package Plugin_Registry is (Cap : Plugin_Capability) return Natural; -- Count plugins with a specific capability - -- Status management - procedure Enable_Plugin (ID : String); - procedure Disable_Plugin (ID : String); - function Is_Plugin_Enabled (ID : String) return Boolean; + -- Status management (all keyed by a non-empty plugin ID) + procedure Enable_Plugin (ID : String) + with Pre => ID'Length > 0; + procedure Disable_Plugin (ID : String) + with Pre => ID'Length > 0; + function Is_Plugin_Enabled (ID : String) return Boolean + with Pre => ID'Length > 0; -- ═══════════════════════════════════════════════════════════════════════ -- Built-in Plugin Factories