fix(spark): honest-demote dnfinition reversibility claim + theatre gate (P0)

[hyperpolymath]

What

Closes the P0 of the estate Rust/SPARK audit
(PROOF-DEBT-AND-RUST-SPARK-AUDIT-2026-05-18.adoc): ambientops bannered the
dnfinition reversibility subsystem as "formally verified" SPARK while
GNATprove was never wired in, the ghost/lemma bodies were stubbed to
return True / null;, and the subsystem did not even compile — so the
proof claims were pure theatre.

Honest demotion (no false proof claims remain)

Unit	Change
safety_boundary.ads/.adb	banner (formally verified) → (runtime-enforced; NOT formally verified), SPARK_Mode → Off, honest PROOF STATUS note, Is_Valid de-ghosted (real runtime fn), obligation O-SAFE-2
reversibility_types.ads	SPARK_Mode Off, O-REV-1..4; Rollback_Result.Snapshot_ID→Target_Snapshot (name-clash)
reversibility_types.adb	deleted — spec is types + expression functions only
snapshot_manager.ads/.adb	SPARK_Mode Off + HONESTY NOTE; consumer updated for the Target_Snapshot rename
safety_invariant.ads/.adb	SPARK_Mode Off, broken Refined_State removed

PROOF-NEEDS.md records O-REV-1..4 / O-SAFE-1..2 as the authoritative
UNPROVEN obligation list (Idris2 model).

Build verification — now actually performed

The first revision could not gprbuild (project with "ncurses", no
provider). Resolved by adding checkonly.gpr, a scoped compile-check over
reversibility/safety/backends/platform that omits the unrelated, unprovided
ncurses TUI dependency. Doing so exposed — and this PR fixes — 3 real
legality blockers that were the concrete reason the subsystem never built
(hence why the proof claims could be theatre at all):

1. backend_interface.ads — record field named Package (Ada reserved
   word). Hard legality error. Renamed → Pkg (unreferenced; local).
2. safety_boundary.ads — Is_Valid was with Ghost but called in real
   runtime checks: ghost-without-proof in executable code, also illegal once
   SPARK_Mode is Off. Aspect removed.
3. snapshot_manager.adb — un-propagated fallout of the
   Rollback_Result.Snapshot_ID → Target_Snapshot demotion rename. 5 refs
   fixed.

Result (gprbuild -gnatc via checkonly.gpr):

Unit	Result
safety_boundary.adb	compiles, 0 errors
safety_invariant.adb	compiles, 0 errors
reversibility_types.ads	compiles, 0 errors
snapshot_manager.adb	only 3 residual errors — all pre-existing undefined Create_{Btrfs,ZFS,LVM}_Snapshot stubs, unrelated to the SPARK demotion (separate "never implemented" debt, out of P0 scope)

The demotion is now proven legal Ada, not merely asserted.

Regression guard

.github/workflows/spark-proof-gate.yml — self-contained SPARK Theatre Gate
over total-update/ada: T1 (header proof-claim, no prover) hard-fails;
T2 (zero-contract SPARK_Mode) warns during the migration tail. Mirrors
the estate reusable gate (hyperpolymath/standards#141); collapses to a
3-line uses: caller once that merges. Verified to PASS on the final tree and
to catch the pre-demotion safety_boundary banner regression (T1).

Refs hyperpolymath/standards#124
Refs hyperpolymath/standards#127

[github-actions]

🔍 Hypatia Security Scan

Findings: 97 issues detected

Severity	Count
🔴 Critical	37
🟠 High	34
🟡 Medium	26

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Issue in quality.yml",
    "type": "missing_workflow",
    "file": "quality.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in security-policy.yml",
    "type": "missing_workflow",
    "file": "security-policy.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Action hyperpolymath/standards/.github/workflows/governance-reusable.yml@main needs attention",
    "type": "unpinned_action",
    "file": "governance.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Nickel file missing SPDX-License-Identifier header (1 occurrences, CWE-1104)",
    "type": "ncl_missing_spdx",
    "file": "/home/runner/work/ambientops/ambientops/_pathroot/ncl/lib/schema.ncl",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "getExn on external data -- use pattern matching (1 occurrences, CWE-754)",
    "type": "getexn_on_external",
    "file": "/home/runner/work/ambientops/ambientops/_pathroot/src/nicaug/NicaugCLI.res",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  },
  {
    "reason": "getExn on external data -- use pattern matching (1 occurrences, CWE-754)",
    "type": "getexn_on_external",
    "file": "/home/runner/work/ambientops/ambientops/_pathroot/src/nicaug/PlatformOrchestrator.res",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  },
  {
    "reason": "getExn on external data -- use pattern matching (7 occurrences, CWE-754)",
    "type": "getexn_on_external",
    "file": "/home/runner/work/ambientops/ambientops/_pathroot/src/Discovery.res",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  },
  {
    "reason": "expect() in hot path (1 occurrences, CWE-754)",
    "type": "expect_in_hot_path",
    "file": "/home/runner/work/ambientops/ambientops/panoptes/src/ollama.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "unwrap_or(0) with dangerous default (2 occurrences, CWE-754)",
    "type": "unwrap_dangerous_default",
    "file": "/home/runner/work/ambientops/ambientops/panoptes/src/web/mod.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  },
  {
    "reason": "unwrap_or(0) with dangerous default (1 occurrences, CWE-754)",
    "type": "unwrap_dangerous_default",
    "file": "/home/runner/work/ambientops/ambientops/personal-sysadmin/src/correlation.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence