|
| 1 | +-- SPDX-License-Identifier: PMPL-1.0-or-later |
| 2 | +-- |
| 3 | +-- SPARK companion spec for src/rust/verification/axiom_tracker.rs |
| 4 | +-- |
| 5 | +-- Proved properties |
| 6 | +-- 1. DangerLevel total order (Safe < Noted < Warning < Reject) is |
| 7 | +-- given definitionally by Ada enumeration ordering. |
| 8 | +-- 2. Enforce_Policy cap-at-Reject monotonicity: if any usage carries |
| 9 | +-- Reject, the returned policy is always Rejected. |
| 10 | +-- 3. Enforce_Policy is fully deterministic and total (no Precondition). |
| 11 | +-- 4. Is_Acceptable <=> Kind /= Rejected (exact Rust semantics). |
| 12 | +-- 5. Worst_Danger is a pure function of the policy kind. |
| 13 | + |
| 14 | +pragma Ada_2022; |
| 15 | + |
| 16 | +package Axiom_Tracker |
| 17 | + with SPARK_Mode => On |
| 18 | +is |
| 19 | + -- ── DangerLevel ──────────────────────────────────────────────────── |
| 20 | + -- Mirrors Rust enum DangerLevel (ordered Safe < Noted < Warning < Reject). |
| 21 | + -- Ada enumeration types carry a built-in discrete order matching |
| 22 | + -- declaration order, so the 4-level hierarchy is axiomatic here. |
| 23 | + type Danger_Level is (Safe, Noted, Warning, Reject); |
| 24 | + |
| 25 | + -- ── AxiomUsage (proof-relevant fields only) ──────────────────────── |
| 26 | + -- The full Rust AxiomUsage also carries prover, construct string, and |
| 27 | + -- optional line number. For the policy proof only Danger matters. |
| 28 | + type Axiom_Usage is record |
| 29 | + Danger : Danger_Level := Safe; |
| 30 | + end record; |
| 31 | + |
| 32 | + -- Bounded usage array (mirrors Vec<AxiomUsage>). |
| 33 | + -- Upper bound 1_024 is generous for any realistic proof run. |
| 34 | + Max_Usages : constant := 1_024; |
| 35 | + subtype Usage_Index is Positive range 1 .. Max_Usages; |
| 36 | + type Usage_Array is array (Usage_Index range <>) of Axiom_Usage; |
| 37 | + |
| 38 | + -- ── AxiomPolicy ──────────────────────────────────────────────────── |
| 39 | + -- Mirrors Rust enum AxiomPolicy (Clean / ClassicalAxioms / |
| 40 | + -- IncompleteProof / Rejected). The Vec payloads are omitted here; |
| 41 | + -- only the discriminant drives the proofs below. |
| 42 | + type Policy_Kind is (Clean, Classical_Axioms, Incomplete_Proof, Rejected); |
| 43 | + |
| 44 | + type Axiom_Policy is record |
| 45 | + Kind : Policy_Kind; |
| 46 | + end record; |
| 47 | + |
| 48 | + -- ── Enforce_Policy ───────────────────────────────────────────────── |
| 49 | + -- Mirrors AxiomTracker::enforce_policy. |
| 50 | + -- |
| 51 | + -- Post-condition encodes the four determinism branches and |
| 52 | + -- cap-at-Reject monotonicity: |
| 53 | + -- |
| 54 | + -- (a) any Reject usage => policy is Rejected |
| 55 | + -- (b) no Reject, some Warning => Incomplete_Proof |
| 56 | + -- (c) no Reject, no Warning, some Noted => Classical_Axioms |
| 57 | + -- (d) empty or all-Safe => Clean |
| 58 | + -- |
| 59 | + -- Branch (a) is cap-at-Reject monotonicity; branches (b)-(d) complete |
| 60 | + -- the total characterisation so gnatprove can verify the body. |
| 61 | + function Enforce_Policy (Usages : Usage_Array) return Axiom_Policy |
| 62 | + with Post => |
| 63 | + -- (a) cap-at-Reject |
| 64 | + (if (for some J in Usages'Range => Usages (J).Danger = Reject) |
| 65 | + then Enforce_Policy'Result.Kind = Rejected) |
| 66 | + and then |
| 67 | + -- (b) |
| 68 | + (if (for all J in Usages'Range => Usages (J).Danger /= Reject) |
| 69 | + and (for some J in Usages'Range => Usages (J).Danger = Warning) |
| 70 | + then Enforce_Policy'Result.Kind = Incomplete_Proof) |
| 71 | + and then |
| 72 | + -- (c) |
| 73 | + (if (for all J in Usages'Range => Usages (J).Danger /= Reject) |
| 74 | + and (for all J in Usages'Range => Usages (J).Danger /= Warning) |
| 75 | + and (for some J in Usages'Range => Usages (J).Danger = Noted) |
| 76 | + then Enforce_Policy'Result.Kind = Classical_Axioms) |
| 77 | + and then |
| 78 | + -- (d) empty input |
| 79 | + (if Usages'Length = 0 |
| 80 | + then Enforce_Policy'Result.Kind = Clean); |
| 81 | + |
| 82 | + -- ── Is_Acceptable ────────────────────────────────────────────────── |
| 83 | + -- Mirrors AxiomPolicy::is_acceptable. |
| 84 | + -- Post is an exact boolean characterisation (not just implication). |
| 85 | + function Is_Acceptable (P : Axiom_Policy) return Boolean |
| 86 | + with Post => Is_Acceptable'Result = (P.Kind /= Rejected); |
| 87 | + |
| 88 | + -- ── Worst_Danger ─────────────────────────────────────────────────── |
| 89 | + -- Mirrors AxiomPolicy::worst_danger. |
| 90 | + -- Exhaustive case equation lets gnatprove discharge callers that |
| 91 | + -- reason about the returned level without opening the body. |
| 92 | + function Worst_Danger (P : Axiom_Policy) return Danger_Level |
| 93 | + with Post => |
| 94 | + (case P.Kind is |
| 95 | + when Clean => Worst_Danger'Result = Safe, |
| 96 | + when Classical_Axioms => Worst_Danger'Result = Noted, |
| 97 | + when Incomplete_Proof => Worst_Danger'Result = Warning, |
| 98 | + when Rejected => Worst_Danger'Result = Reject); |
| 99 | + |
| 100 | + -- ── Monotonicity lemma (ghost) ────────────────────────────────────── |
| 101 | + -- For any single usage U and the policy derived from a set containing U, |
| 102 | + -- the policy's worst danger is >= U.Danger. |
| 103 | + -- |
| 104 | + -- Stated as a ghost function so callers can use it in their own |
| 105 | + -- contracts without runtime cost. The body (in the .adb) is proved |
| 106 | + -- by gnatprove from Enforce_Policy's post-condition. |
| 107 | + function Policy_Dominates_Usage |
| 108 | + (Policy : Axiom_Policy; U : Axiom_Usage) return Boolean |
| 109 | + is (Worst_Danger (Policy) >= U.Danger) |
| 110 | + with Ghost; |
| 111 | + |
| 112 | +end Axiom_Tracker; |
0 commit comments