diff --git a/.github/workflows/spark-proof-gate.yml b/.github/workflows/spark-proof-gate.yml new file mode 100644 index 0000000..c89289a --- /dev/null +++ b/.github/workflows/spark-proof-gate.yml @@ -0,0 +1,95 @@ +# SPDX-License-Identifier: PMPL-1.0 +name: SPARK Proof Gate + +# ambientops anti-theatre gate (P0 of the estate Rust/SPARK audit; +# hyperpolymath/standards#124 / #135). +# +# Self-contained on purpose: it does not `uses:` the standards reusable +# SPARK Theatre Gate yet, so it works the moment this lands rather than +# waiting on hyperpolymath/standards#141 to merge. Once #141 is on +# standards@main this file SHOULD be reduced to a 3-line caller: +# +# jobs: +# gate: +# uses: hyperpolymath/standards/.github/workflows/spark-theatre-gate.yml@ +# with: { paths: "total-update/ada", enforce_zero_contract: false } +# +# It exists specifically so the safety_boundary / reversibility_types / +# safety_invariant honest-demotion cannot silently regress to a false +# "formally verified" banner. T1 is a hard failure; T2 (zero-contract +# SPARK_Mode) is a warning while the Ada/SPARK->Rust/SPARK migration tail +# clears (tracked in PROOF-NEEDS.md). + +on: + push: + branches: [main, master] + paths: ["total-update/ada/**", ".github/workflows/spark-proof-gate.yml"] + pull_request: + paths: ["total-update/ada/**", ".github/workflows/spark-proof-gate.yml"] + +concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: true + +permissions: + contents: read + +jobs: + spark-proof-gate: + name: SPARK Proof Gate (dnfinition) + runs-on: ubuntu-latest + steps: + - name: Checkout + uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v4 + + - name: Scan total-update/ada for SPARK proof theatre + run: | + set -uo pipefail + SCAN_ROOT="total-update/ada" + + prover_evidence=0 + if grep -rIlE 'gnatprove' .github/workflows 2>/dev/null | grep -q .; then + prover_evidence=1 + fi + for bf in Justfile justfile Mustfile Dustfile; do + [ -f "$bf" ] && grep -qI 'gnatprove' "$bf" && prover_evidence=1 + done + if find . \( -name 'gnatprove.out' -o -name '*.spark' \ + -o -path '*/gnatprove/*.json' \) \ + -not -path '*/.git/*' 2>/dev/null | grep -q .; then + prover_evidence=1 + fi + echo "prover_evidence=$prover_evidence" + + claim_re='formally verified|SPARK Proof Level|\(Gold\)|all preconditions and postconditions are verified|proving the invariant holds' + contract_re='Pre[[:space:]]*=>|Post[[:space:]]*=>|Global[[:space:]]*=>|Depends[[:space:]]*=>|Contract_Cases' + sparkon_re='pragma[[:space:]]+SPARK_Mode[[:space:]]*\([[:space:]]*On[[:space:]]*\)|with[[:space:]]+SPARK_Mode[[:space:]]*=>[[:space:]]*On' + + fail=0 + while IFS= read -r f; do + [ -z "$f" ] && continue + grep -vE '^[[:space:]]*--' "$f" | grep -qE "$sparkon_re" || continue + header="$(awk ' + /^[[:space:]]*--/ || /^[[:space:]]*$/ { print; next } + { exit }' "$f")" + has_header_claim=0 + printf '%s\n' "$header" | grep -qiE "$claim_re" && has_header_claim=1 + has_contract=0 + grep -qE "$contract_re" "$f" && has_contract=1 + + [ "$prover_evidence" -eq 1 ] && continue + + if [ "$has_header_claim" -eq 1 ]; then + echo "::error file=$f::T1 SPARK theatre regression: header banner claims formal proof but no GNATprove run exists. Demote (SPARK_Mode Off + tracked obligation in PROOF-NEEDS.md) or wire gnatprove into CI." + fail=1 + elif [ "$has_contract" -eq 0 ]; then + echo "::warning file=$f::T2 zero-contract SPARK_Mode (standards#135): proves nothing here. Demote to SPARK_Mode Off or add contracts." + fi + done < <(find "$SCAN_ROOT" \( -name '*.ads' -o -name '*.adb' \) \ + -not -path '*/.git/*' -not -path '*/obj/*' 2>/dev/null) + + if [ "$fail" -ne 0 ]; then + echo "::error::SPARK Proof Gate FAILED — a demoted unit regressed to a hollow 'verified' claim. See PROOF-NEEDS.md (O-REV-*/O-SAFE-*)." + exit 1 + fi + echo "✓ SPARK Proof Gate passed — no hollow proof claims in total-update/ada." diff --git a/PROOF-NEEDS.md b/PROOF-NEEDS.md index 35493be..905f962 100644 --- a/PROOF-NEEDS.md +++ b/PROOF-NEEDS.md @@ -15,6 +15,30 @@ - **Privilege escalation prevention**: Prove system operations respect the principle of least privilege (no operation escalates beyond its declared scope) - **Rollback atomicity**: Prove that failed operations roll back completely (no partial state) +## Tracked unproven obligations — dnfinition reversibility subsystem + +The following obligations are referenced by the `PROOF STATUS` / `HONESTY +NOTE` headers in `total-update/ada/dnfinition/src/{reversibility,safety}/*`. +They were previously expressed as SPARK ghost/lemma bodies stubbed to +`return True` / `null;` (proof theatre). SPARK_Mode is now `Off` on those +units and the obligations are recorded here as the authoritative, +**UNPROVEN** list (Idris2 is the intended model — see Recommended prover). +The SPARK Theatre Gate (`.github/workflows/spark-proof-gate.yml`) prevents +any of these units silently regressing to a false "verified" claim. + +| ID | Unit | Obligation | +|----|------|------------| +| O-REV-1 | `reversibility_types.ads` | `Snapshot_Exists`: a snapshot referenced by a non-null `Snapshot_ID` is actually present in backend storage. | +| O-REV-2 | `reversibility_types.ads` | `Snapshot_Is_Valid`: a `Valid`-state snapshot is restorable. | +| O-REV-3 | `reversibility_types.ads` | `System_State_Matches_Snapshot`: after a `Completed` rollback, on-disk system state equals the snapshot's captured state (rollback atomicity / no partial state). Subsumes the "Rollback atomicity" item above. | +| O-REV-4 | `reversibility_types.ads` | Monotonic snapshot IDs: issued IDs strictly increase and are never reused after deletion. | +| O-SAFE-1 | `safety_invariant.ads` | The invariant "every modifying operation is preceded by a recovery point" (`Invariant_Holds`) is preserved by all state-update operations. | +| O-SAFE-2 | `safety_boundary.ads` | The token-typed API (`Recovery_Point_Token`) admits no path that performs a modifying `Safe_*` operation without a valid recovery point, i.e. the runtime-enforced invariant is also statically unviolable. | + +Status: **none of O-REV-1..4 / O-SAFE-1..2 are checked at compile time or +runtime today.** They are honest debt, not regressions, and are +deliberately *not* claimed as proven anywhere in the source. + ## Recommended prover - **Idris2** — State machines and idempotency properties are natural fits for dependent types diff --git a/total-update/ada/dnfinition/.gitignore b/total-update/ada/dnfinition/.gitignore new file mode 100644 index 0000000..8b1f9a2 --- /dev/null +++ b/total-update/ada/dnfinition/.gitignore @@ -0,0 +1 @@ +obj-check/ diff --git a/total-update/ada/dnfinition/checkonly.gpr b/total-update/ada/dnfinition/checkonly.gpr new file mode 100644 index 0000000..4b7ab5a --- /dev/null +++ b/total-update/ada/dnfinition/checkonly.gpr @@ -0,0 +1,26 @@ +-- SPDX-License-Identifier: PMPL-1.0-or-later +-- Scoped compile-check project: verifies the reversibility/safety +-- subsystem (the units touched by the SPARK honest-demotion) WITHOUT +-- pulling the unrelated, unprovided `ncurses` TUI dependency. Not for +-- shipping — a verification harness only. + +project Checkonly is + + for Source_Dirs use + ("src/reversibility", + "src/safety", + "src/backends", + "src/platform"); + for Object_Dir use "obj-check"; + -- No `for Main`: compile-only, no bind/link, no ncurses needed. + + package Compiler is + for Switches ("Ada") use + ("-gnat2022", + "-gnatwa", + "-gnato13", + "-gnatf", + "-gnata"); -- assertions on: exercises the retained Pre/Post + end Compiler; + +end Checkonly; diff --git a/total-update/ada/dnfinition/src/backends/backend_interface.ads b/total-update/ada/dnfinition/src/backends/backend_interface.ads index 54e2d7d..6555445 100644 --- a/total-update/ada/dnfinition/src/backends/backend_interface.ads +++ b/total-update/ada/dnfinition/src/backends/backend_interface.ads @@ -68,7 +68,13 @@ package Backend_Interface is type Transaction_Item is record Kind : Transaction_Kind; - Package : Package_Info; + Pkg : Package_Info; + -- Renamed from `Package`: that is an Ada reserved word and was a + -- hard legality error (backend_interface.ads:71) that prevented the + -- dnfinition subsystem from compiling at all — the concrete reason + -- the old SPARK "formally verified" banners were pure theatre + -- (GNATprove can prove nothing about code that does not compile). + -- Field is unreferenced anywhere; rename is purely local. end record; type Transaction_List is array (Positive range <>) of Transaction_Item; diff --git a/total-update/ada/dnfinition/src/reversibility/reversibility_types.adb b/total-update/ada/dnfinition/src/reversibility/reversibility_types.adb deleted file mode 100644 index a17c542..0000000 --- a/total-update/ada/dnfinition/src/reversibility/reversibility_types.adb +++ /dev/null @@ -1,40 +0,0 @@ --- SPDX-License-Identifier: PMPL-1.0-or-later --- SPDX-FileCopyrightText: 2025 Jonathan D.A. Jewell - -pragma SPARK_Mode (On); - -package body Reversibility_Types is - - -- ═══════════════════════════════════════════════════════════════════════ - -- Ghost Function Implementations - -- These are only evaluated during SPARK proof, not at runtime - -- ═══════════════════════════════════════════════════════════════════════ - - function Snapshot_Exists (ID : Snapshot_ID) return Boolean is - begin - -- Ghost implementation - would check actual snapshot storage - -- For now, any non-null ID is considered existing - return ID /= Null_Snapshot; - end Snapshot_Exists; - - function Snapshot_Is_Valid (ID : Snapshot_ID) return Boolean is - begin - -- Ghost implementation - snapshot exists and is in valid state - return Snapshot_Exists (ID); - end Snapshot_Is_Valid; - - function System_State_Matches_Snapshot (ID : Snapshot_ID) return Boolean is - begin - -- Ghost implementation - would verify system state - -- This is checked after rollback operations - pragma Unreferenced (ID); - return True; - end System_State_Matches_Snapshot; - - function Current_System_State_ID return Snapshot_ID is - begin - -- Ghost implementation - conceptual current state - return Null_Snapshot; - end Current_System_State_ID; - -end Reversibility_Types; diff --git a/total-update/ada/dnfinition/src/reversibility/reversibility_types.ads b/total-update/ada/dnfinition/src/reversibility/reversibility_types.ads index 224bd1a..df6af16 100644 --- a/total-update/ada/dnfinition/src/reversibility/reversibility_types.ads +++ b/total-update/ada/dnfinition/src/reversibility/reversibility_types.ads @@ -2,9 +2,18 @@ -- SPDX-FileCopyrightText: 2025 Jonathan D.A. Jewell -- Reversibility Types - Core types for transaction safety and rollback --- This module uses SPARK for formal verification of reversibility guarantees - -pragma SPARK_Mode (On); +-- +-- HONESTY NOTE (2026-05-18 audit): This unit was previously marked +-- SPARK_Mode (On) and carried ghost functions +-- (Snapshot_Exists / System_State_Matches_Snapshot / ...) whose bodies +-- are stubbed to return True. No GNATprove proof has ever been run or +-- passed (the unit does not even pass SPARK Phase-2 legality: see the +-- record-component / type name clash on Rollback_Result.Snapshot_ID). +-- SPARK_Mode is therefore set Off until a genuine proof obligation +-- exists. The real reversibility obligations are tracked as proof debt +-- in PROOF-NEEDS.md (Idris2), NOT claimed as proven here. + +pragma SPARK_Mode (Off); with Ada.Calendar; with Ada.Strings.Unbounded; use Ada.Strings.Unbounded; @@ -87,33 +96,33 @@ package Reversibility_Types is Requires_Reboot); type Rollback_Result is record - Status : Rollback_Status := Not_Started; - Message : Unbounded_String; - Snapshot_ID : Snapshot_ID := Null_Snapshot; + Status : Rollback_Status := Not_Started; + Message : Unbounded_String; + Target_Snapshot : Snapshot_ID := Null_Snapshot; + -- Renamed from Snapshot_ID: a record component named identically to + -- the type Snapshot_ID is a SPARK/Ada name clash and was one of the + -- legality errors that blocked GNATprove Phase 2. end record; -- ═══════════════════════════════════════════════════════════════════════ - -- SPARK Contracts for Reversibility Guarantees + -- Reversibility Obligations (UNPROVEN — tracked proof debt) -- ═══════════════════════════════════════════════════════════════════════ - - -- Ghost functions for formal verification - function Snapshot_Exists (ID : Snapshot_ID) return Boolean - with Ghost; - -- True if snapshot with given ID exists in the system - - function Snapshot_Is_Valid (ID : Snapshot_ID) return Boolean - with Ghost, - Post => (if Snapshot_Is_Valid'Result then Snapshot_Exists (ID)); - -- True if snapshot exists and is in Valid state - - function System_State_Matches_Snapshot (ID : Snapshot_ID) return Boolean - with Ghost, - Pre => Snapshot_Exists (ID); - -- True if current system state matches the snapshot - - function Current_System_State_ID return Snapshot_ID - with Ghost; - -- Conceptual ID of current system state (for verification) + -- + -- These properties are NOT formally verified. They were previously + -- expressed as SPARK ghost functions with stub bodies (return True), + -- which constitutes proof theatre. They are recorded here as prose + -- obligations and tracked in PROOF-NEEDS.md for an Idris2 model: + -- + -- O-REV-1 Snapshot_Exists: a snapshot referenced by a non-null + -- Snapshot_ID is actually present in backend storage. + -- O-REV-2 Snapshot_Is_Valid: a "Valid"-state snapshot is restorable. + -- O-REV-3 System_State_Matches_Snapshot: after a Completed rollback, + -- on-disk system state equals the snapshot's captured state + -- (rollback atomicity / no partial state). + -- O-REV-4 Monotonic snapshot IDs: issued IDs strictly increase and + -- are never reused after deletion. + -- + -- None of O-REV-1..4 are checked at compile time or runtime today. -- ═══════════════════════════════════════════════════════════════════════ -- Configuration diff --git a/total-update/ada/dnfinition/src/reversibility/snapshot_manager.adb b/total-update/ada/dnfinition/src/reversibility/snapshot_manager.adb index 1257b32..215e211 100644 --- a/total-update/ada/dnfinition/src/reversibility/snapshot_manager.adb +++ b/total-update/ada/dnfinition/src/reversibility/snapshot_manager.adb @@ -183,21 +183,21 @@ package body Snapshot_Manager is Result := ( Status => Completed, Message => To_Unbounded_String ("Native rollback complete"), - Snapshot_ID => ID + Target_Snapshot => ID ); when Platform_Detection.Btrfs | Platform_Detection.ZFS => Result := ( Status => Requires_Reboot, Message => To_Unbounded_String ("Snapshot restored, reboot required"), - Snapshot_ID => ID + Target_Snapshot => ID ); when others => Result := ( Status => Failed, Message => To_Unbounded_String ("Manual rollback required"), - Snapshot_ID => ID + Target_Snapshot => ID ); end case; @@ -209,7 +209,7 @@ package body Snapshot_Manager is Result := ( Status => Failed, Message => To_Unbounded_String ("Snapshot not found"), - Snapshot_ID => Null_Snapshot + Target_Snapshot => Null_Snapshot ); end Rollback_To_Snapshot; @@ -221,7 +221,7 @@ package body Snapshot_Manager is Result := ( Status => Not_Started, Message => Ada.Strings.Unbounded.To_Unbounded_String ("No snapshots"), - Snapshot_ID => Null_Snapshot + Target_Snapshot => Null_Snapshot ); else Rollback_To_Snapshot (Snapshots (Snapshot_Count).ID, Result); diff --git a/total-update/ada/dnfinition/src/reversibility/snapshot_manager.ads b/total-update/ada/dnfinition/src/reversibility/snapshot_manager.ads index d7f5aa8..e79286b 100644 --- a/total-update/ada/dnfinition/src/reversibility/snapshot_manager.ads +++ b/total-update/ada/dnfinition/src/reversibility/snapshot_manager.ads @@ -1,10 +1,19 @@ -- SPDX-License-Identifier: PMPL-1.0-or-later -- SPDX-FileCopyrightText: 2025 Jonathan D.A. Jewell --- Snapshot Manager - Core reversibility layer with SPARK verification +-- Snapshot Manager - Core reversibility layer -- This is the CRITICAL module that ensures all operations can be rolled back - -pragma SPARK_Mode (On); +-- +-- HONESTY NOTE (2026-05-18 audit): this spec was SPARK_Mode (On) while its +-- body was SPARK_Mode (Off), so GNATprove never verified ANY postcondition +-- here. The postconditions also referenced ghost functions stubbed to +-- return True (e.g. System_State_Matches_Snapshot), making the headline +-- "reversibility guarantee" vacuous even if it had been proved. SPARK_Mode +-- is now Off. The retained Pre/Post are ordinary Ada 2022 assertions +-- (runtime-checked under -gnata only), NOT formal proofs. The real +-- reversibility obligations are tracked as proof debt in PROOF-NEEDS.md. + +pragma SPARK_Mode (Off); with Ada.Strings.Unbounded; use Ada.Strings.Unbounded; with Platform_Detection; use Platform_Detection; @@ -16,13 +25,9 @@ package Snapshot_Manager is -- Module State (for SPARK contracts) -- ═══════════════════════════════════════════════════════════════════════ - Initialized : Boolean := False - with Ghost; - -- Ghost variable tracking initialization state - - function Is_Initialized return Boolean - with Ghost, - Global => Initialized; + function Is_Initialized return Boolean; + -- True once Initialize has been called. Backed by the body's real + -- Is_Init flag (no longer a Ghost stub). -- ═══════════════════════════════════════════════════════════════════════ -- Initialization @@ -55,13 +60,14 @@ package Snapshot_Manager is Snapshot.State = Valid); -- Create a new snapshot. On failure, Success is False. -- NEVER proceed with package operations if snapshot creation fails. + -- NOTE: the Post above is a runtime assertion only (SPARK_Mode Off). function Create_Pre_Transaction_Snapshot (Description : String) return Snapshot_ID - with Pre => Is_Initialized, - Post => (if Create_Pre_Transaction_Snapshot'Result /= Null_Snapshot - then Snapshot_Exists (Create_Pre_Transaction_Snapshot'Result)); - -- Convenience function: returns Null_Snapshot on failure + with Pre => Is_Initialized; + -- Convenience function: returns Null_Snapshot on failure. + -- Obligation O-REV-1 (result refers to a really-stored snapshot) is + -- UNPROVEN — tracked in PROOF-NEEDS.md. -- ═══════════════════════════════════════════════════════════════════════ -- Rollback Operations (CRITICAL - Core Safety Feature) @@ -71,14 +77,13 @@ package Snapshot_Manager is (ID : Snapshot_ID; Result : out Rollback_Result) with Pre => Is_Initialized and then - Valid_Snapshot (ID) and then - Snapshot_Exists (ID), - Post => (if Result.Status = Completed then - System_State_Matches_Snapshot (ID)) - or else - (Result.Status in Failed | Requires_Reboot); + Valid_Snapshot (ID); -- Restore system to snapshot state. - -- On success, system state matches snapshot exactly. + -- CRITICAL UNPROVEN OBLIGATION O-REV-3: "on Completed, on-disk system + -- state matches the snapshot exactly (rollback atomicity, no partial + -- state)" is NOT verified. The previous Post asserting this was vacuous + -- (System_State_Matches_Snapshot was a `return True` stub). Tracked in + -- PROOF-NEEDS.md. -- May require reboot for immutable systems. procedure Rollback_Last @@ -105,10 +110,9 @@ package Snapshot_Manager is -- Get detailed info about a specific snapshot function Get_Latest_Snapshot return Snapshot_ID - with Pre => Is_Initialized, - Post => Get_Latest_Snapshot'Result = Null_Snapshot or else - Snapshot_Exists (Get_Latest_Snapshot'Result); - -- Get the most recent snapshot ID, or Null_Snapshot if none + with Pre => Is_Initialized; + -- Get the most recent snapshot ID, or Null_Snapshot if none. + -- Obligation O-REV-1 (result is a really-stored snapshot) UNPROVEN. function Count_Snapshots return Natural with Pre => Is_Initialized; @@ -121,9 +125,9 @@ package Snapshot_Manager is procedure Delete_Snapshot (ID : Snapshot_ID; Success : out Boolean) - with Pre => Is_Initialized and then Valid_Snapshot (ID), - Post => (if Success then not Snapshot_Exists (ID)); - -- Delete a specific snapshot + with Pre => Is_Initialized and then Valid_Snapshot (ID); + -- Delete a specific snapshot. + -- Obligation (on Success the snapshot is truly gone) UNPROVEN. procedure Cleanup_Old_Snapshots (Keep_Count : Positive := 10; diff --git a/total-update/ada/dnfinition/src/safety/safety_boundary.ads b/total-update/ada/dnfinition/src/safety/safety_boundary.ads index e13aeaa..8fbb732 100644 --- a/total-update/ada/dnfinition/src/safety/safety_boundary.ads +++ b/total-update/ada/dnfinition/src/safety/safety_boundary.ads @@ -4,7 +4,7 @@ -- Safety_Boundary - CRITICAL module enforcing reversibility invariants -- -- ╔═══════════════════════════════════════════════════════════════════════════╗ --- ║ SAFETY INVARIANT (formally verified): ║ +-- ║ SAFETY INVARIANT (runtime-enforced; NOT formally verified): ║ -- ║ ║ -- ║ "Every modifying package operation MUST be preceded by a valid ║ -- ║ recovery point. Operations without recovery points are REJECTED." ║ @@ -13,12 +13,30 @@ -- ║ state, preventing unrecoverable system corruption. ║ -- ╚═══════════════════════════════════════════════════════════════════════════╝ -- +-- PROOF STATUS (2026-05-19 audit, P0 ambientops): NOT PROVEN. This unit +-- previously declared SPARK_Mode (On) and the banner claimed the invariant +-- was "formally verified". That claim was false on the same grounds as the +-- rest of the dnfinition reversibility subsystem (see reversibility_types.ads +-- and safety_invariant.ads HONESTY NOTEs): +-- * GNATprove was never wired into any build or CI; no proof obligation +-- has ever been discharged for this package. +-- * The Pre/Post contracts below (Is_Valid (Token) etc.) are genuine +-- *runtime-checked* contracts — they constrain execution but prove +-- nothing at analysis time. The token type gives a useful defence-in- +-- depth API discipline, not a machine-checked guarantee. +-- SPARK_Mode is therefore Off and the "(formally verified)" / "SPARK +-- contracts proving the invariant holds" wording removed. The invariant +-- "every modifying operation is preceded by a recovery point" is a tracked, +-- UNPROVEN obligation: PROOF-NEEDS.md, O-SAFE-2 (Idris2 model). The +-- anti-theatre CI gate (.github/workflows/spark-proof-gate.yml) prevents +-- this from silently regressing back to a false "verified" claim. +-- -- This module provides: --- 1. SPARK contracts proving the invariant holds +-- 1. Token-typed API discipline for modifying operations (runtime-enforced) -- 2. Runtime enforcement as a defense-in-depth layer -- 3. Safe wrappers for all modifying operations -pragma SPARK_Mode (On); +pragma SPARK_Mode (Off); with Ada.Strings.Unbounded; use Ada.Strings.Unbounded; with Backend_Interface; use Backend_Interface; @@ -37,9 +55,12 @@ package Safety_Boundary is type Recovery_Point_Token is private; Null_Token : constant Recovery_Point_Token; - function Is_Valid (Token : Recovery_Point_Token) return Boolean - with Ghost; - -- Ghost function: True if token represents a valid recovery point + function Is_Valid (Token : Recovery_Point_Token) return Boolean; + -- True if the token represents a valid recovery point. This is a REAL + -- runtime function, not Ghost: the bodies below call it for actual + -- defense-in-depth checks. The former `with Ghost` was residual proof + -- theatre — a ghost entity with no proof, used in executable code, + -- which is also an Ada legality error once SPARK_Mode is Off. function Token_Snapshot_ID (Token : Recovery_Point_Token) return Snapshot_ID with Pre => Is_Valid (Token); diff --git a/total-update/ada/dnfinition/src/safety/safety_invariant.adb b/total-update/ada/dnfinition/src/safety/safety_invariant.adb index 44f9487..5e619f0 100644 --- a/total-update/ada/dnfinition/src/safety/safety_invariant.adb +++ b/total-update/ada/dnfinition/src/safety/safety_invariant.adb @@ -1,15 +1,16 @@ -- SPDX-License-Identifier: PMPL-1.0-or-later -- SPDX-FileCopyrightText: 2025 Jonathan D.A. Jewell --- Safety_Invariant - Implementation of SPARK proof specifications +-- Safety_Invariant - implementation. NOT SPARK-verified (see spec +-- PROOF STATUS note). The lemma bodies are `null;` and prove nothing; +-- they are retained only as executable no-ops documenting the intended +-- argument. The broken Refined_State aspect (the legality error that +-- blocked GNATprove Phase 2) has been removed along with the spec's +-- Abstract_State. -pragma SPARK_Mode (On); +pragma SPARK_Mode (Off); -package body Safety_Invariant - with Refined_State => (Global_State => (Active_Recovery_Point, - Last_Operation_Had_Recovery, - Operations_Since_Recovery)) -is +package body Safety_Invariant is -- ═══════════════════════════════════════════════════════════════════════ -- Invariant Definition diff --git a/total-update/ada/dnfinition/src/safety/safety_invariant.ads b/total-update/ada/dnfinition/src/safety/safety_invariant.ads index c68474f..052df2c 100644 --- a/total-update/ada/dnfinition/src/safety/safety_invariant.ads +++ b/total-update/ada/dnfinition/src/safety/safety_invariant.ads @@ -10,21 +10,24 @@ -- ║ point. The system can ALWAYS roll back to a known-good state.║ -- ╚═══════════════════════════════════════════════════════════════════════════╝ -- --- SPARK Proof Level: 2 (Gold) --- - All preconditions and postconditions are verified --- - No runtime checks can fail --- - Memory safety is guaranteed --- --- To verify: gnatprove -P dnfinition.gpr --level=2 - -pragma SPARK_Mode (On); +-- PROOF STATUS (2026-05-18 audit): NOT PROVEN. This unit previously +-- claimed "SPARK Proof Level: 2 (Gold) - All preconditions and +-- postconditions are verified". That claim was false: +-- * GNATprove was never wired into any build or CI; `just prove` +-- cannot run (the project does not even resolve its ncurses import). +-- * The unit fails SPARK Phase-2 legality: the body's Refined_State +-- lists constituents that are not hidden state of this package. +-- * Every "lemma" body is `null;` with a comment asserting the +-- property is "trivially true" — assumed, not proved. +-- SPARK_Mode is now Off and the Gold claim removed. The invariant +-- "every modifying operation is preceded by a recovery point" is a +-- tracked, UNPROVEN obligation (PROOF-NEEDS.md, Idris2 model O-SAFE-1). + +pragma SPARK_Mode (Off); with Reversibility_Types; use Reversibility_Types; -package Safety_Invariant - with Abstract_State => Global_State, - Initializes => Global_State -is +package Safety_Invariant is -- ═══════════════════════════════════════════════════════════════════════ -- Ghost State for Formal Verification