ambientops #127: expose SPARK theatre, fix non-compiling backend_interface, honest verified stance#49
Open
hyperpolymath wants to merge 2 commits into
Open
ambientops #127: expose SPARK theatre, fix non-compiling backend_interface, honest verified stance#49hyperpolymath wants to merge 2 commits into
hyperpolymath wants to merge 2 commits into
Conversation
…oundary + sound contracts Foundation-first verification (gnatprove + gnat) found backend_interface.ads was SPARK theatre that NEVER COMPILED: - Transaction_Item.Package used an Ada reserved word as a field name (no compiler accepts it) -> renamed Pkg (zero references anywhere). - Install/Remove/Upgrade/Upgrade_System/Autoremove are *functions* with an in-out controlling parameter -> illegal SPARK (RM 4.5.2), yet the unit was pragma SPARK_Mode (On). gnatprove could never analyse it. Changes (genuine, no theatre, no fake green): - backend_interface.ads: real bug fix (Package->Pkg, now compiles, gnat exit 0); honest pragma SPARK_Mode (Off) with documented rationale; added sound Ada 2022 Pre'Class/Post'Class on the SPARK-legal query ops (Get_Name/Search/Get_Package_Info) + Pre on Register_Backend (runtime -gnata enforced; also the spec for the OWED SPARK refactor). - plugin_registry.ads: strengthened with non-empty-ID preconditions on Unregister/Get_Plugin/Get_Plugin_Metadata/Enable/Disable/ Is_Plugin_Enabled (was: only Register_Plugin had a Pre). OWED (tracked standards#127, must NOT be faked): state-mutating function->procedure redesign across backend_interface + backend_guix + backend_nix to make the modification path legal SPARK; only then can backend_interface/plugin_registry be gnatprove-discharged. Refs hyperpolymath/standards#124 Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Adversarial re-verification (gnat/gnatprove + 2-agent static SPARK-RM
swarm, dynamically spot-confirmed on origin/main) found PR#48's 'Strong'
SPARK coverage matrix comprehensively FALSE:
- snapshot_manager.adb:4 pragma SPARK_Mode(Off) — entire rollback body
unanalysed; never compiled (call@:93 of fn declared@:145, no fwd decl);
headline Post rests on reversibility_types.adb:31
System_State_Matches_Snapshot = hardcoded 'return True'.
- safety_boundary.adb:6 SPARK_Mode(Off); safety_boundary.ads:78+ Safe_*
are functions with in Out param (illegal SPARK), no escape; no
privilege/scope/bound model exists (only Is_Valid(Token)).
- safety_invariant.ads legal SPARK but tautologies over ghost state the
real (SPARK_Mode Off) path never updates.
Original 2026-05-18 audit ('SPARK theatre') was right; #48 was wrong.
RUST-SPARK-STANCE.adoc: false coverage matrix flagged SUPERSEDED;
added verified-correction section with file:line evidence, what this PR
genuinely delivers, and the precisely-scoped OWED programme.
Refs hyperpolymath/standards#124
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Refs hyperpolymath/standards#124 (estate proof-debt epic, sub-issue #127).
TL;DR — foundation-first verification overturned PR#48
PR#48 (merged, prior session) added
RUST-SPARK-STANCE.adocclaiming the audit's "SPARK theatre" finding was inaccurate and the safety-critical specs were "Strong". Adversarial re-verification (gnat/gnatprove + a 2-agent static SPARK-RM swarm, then dynamically spot-confirmed onorigin/main) found PR#48's coverage matrix is comprehensively FALSE. The original 2026-05-18 audit was right: the entiretotal-update/ada/dnfinitionSPARK story is theatre — and it never even compiled.Verified evidence (file:line, on origin/main)
backend_interface.ads:Transaction_Item.Packageused an Ada reserved word as a field name → no compiler accepts it (never compiled).Install/Remove/Upgrade/Upgrade_System/Autoremoveare functions within outparams = illegal SPARK (RM 4.5.2) underSPARK_Mode (On).snapshot_manager.adb:4→pragma SPARK_Mode (Off)(entire rollback body unanalysed) and never compiled (:93callsCreate_Btrfs_Snapshotdeclared:145, no forward decl). HeadlineRollback_To_SnapshotPostdepends onreversibility_types.adb:26-32System_State_Matches_Snapshot=pragma Unreferenced (ID); return True;(hardcoded vacuous oracle) + fail-permissive disjunction.safety_boundary.adb:6→pragma SPARK_Mode (Off);safety_boundary.ads:78+Safe_*are functions within Outparams (illegal SPARK). No privilege/scope/bound model exists at all.safety_invariant.ads: legal SPARK but tautologies over ghost state the real (SPARK_Mode Off) enforcement path never updates.What this PR genuinely delivers (no theatre, no fake green)
backend_interface.adsPackage→Pkg(zero references anywhere) — the unit now compiles (gnatexit 0).backend_interface.ads→pragma SPARK_Mode (Off)with documented rationale (it is genuinely non-SPARK by design).Pre'Class/Post'Classon the SPARK-legal query ops (Get_Name/Search/Get_Package_Info),PreonRegister_Backend, and six non-empty-IDPres onplugin_registry.ads— runtime-enforced (-gnata) and the spec for the OWED refactor.verified-correctionsection with the evidence above + precisely-scoped OWED programme.Honest scope — NOT closeable here
The real fix is a large genuine programme (tracked #127, must not be faked): state-mutating
function→procedureredesign across the interface + every backend +safety_boundary; bring the safety bodies intoSPARK_Mode (On); fix the elaboration error; replace the hardcoded-Trueghost oracle with a real state model. Only then can the safety-critical contracts begnatprove-discharged. This PR makes the truth visible and the foundation honest; it does not claim verification that does not exist.🤖 Generated with Claude Code