From 6a7e723b0f9c11808ebb64b8a66e044fd5c99556 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 27 Jun 2026 19:48:11 +0000 Subject: [PATCH 1/4] Add Semantics ABI proof: forbidden actions are never certified permitted Raises the Phronesiser Idris2 ABI to Layer 2 with a flagship, machine-checked semantic proof of the repo's headline property ("provably safe ethical constraints for AI agents"). Model: a deontic policy partitions agent actions into Allow/Deny. The `ActionPermitted` proposition has NO constructor admitting a `Deny` verdict, so a forbidden action is structurally uncertifiable. Proven: - decActionPermitted: sound + complete `Dec (ActionPermitted a)`. - certifyPermittedSound: certifier soundness (Ok => ActionPermitted). - safeInformPermitted: positive control (inhabited permission witness). - forbiddenNeverPermitted: negative control / core safety theorem `Not (ActionPermitted forbiddenDeploy)`. - forbiddenNeverCertifiedOk: corollary that the forbidden action is never Ok. Non-vacuity confirmed: a deliberately false witness `PermitAllow Refl : ActionPermitted forbiddenDeploy` is rejected by idris2 (Allow vs Deny mismatch). Build is clean (exit 0, zero warnings). Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx --- .../abi/Phronesiser/ABI/Semantics.idr | 171 ++++++++++++++++++ src/interface/abi/phronesiser-abi.ipkg | 1 + 2 files changed, 172 insertions(+) create mode 100644 src/interface/abi/Phronesiser/ABI/Semantics.idr diff --git a/src/interface/abi/Phronesiser/ABI/Semantics.idr b/src/interface/abi/Phronesiser/ABI/Semantics.idr new file mode 100644 index 0000000..92dd35d --- /dev/null +++ b/src/interface/abi/Phronesiser/ABI/Semantics.idr @@ -0,0 +1,171 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +||| Flagship semantic proof for Phronesiser: ethical safety of action gating. +||| +||| Headline domain property ("Add provably safe ethical constraints to AI +||| agents"): a deontic policy partitions an agent's candidate actions into +||| PERMITTED and FORBIDDEN. We define an `ActionPermitted` proposition that +||| has NO constructor for a forbidden action. Therefore a forbidden action +||| can NEVER be certified permitted — the safety guarantee an ethical +||| constraint engine must provide. The decision procedure is sound AND +||| complete (returns a genuine `Dec`), and the certifier's soundness is +||| machine-checked: if `certifyPermitted a = Permitted`, then `ActionPermitted` +||| holds. Positive and negative controls pin non-vacuity. +||| +||| This is not a runtime test: every fact below is discharged by the Idris2 +||| type checker. The negative control `forbiddenNeverPermitted` is the core +||| safety theorem in `Not (...)` form. + +module Phronesiser.ABI.Semantics + +import Phronesiser.ABI.Types +import Data.So +import Decidable.Equality + +%default total + +-------------------------------------------------------------------------------- +-- A faithful, minimal model of agent actions. +-------------------------------------------------------------------------------- + +||| The classification a policy assigns to an action. +||| - Allow: the action is permissible. +||| - Deny : the action is forbidden (a prohibition applies). +public export +data Verdict = Allow | Deny + +||| A candidate agent action, carrying the policy verdict the ethical engine +||| has resolved for it. `DeployHarm` models an action a sound policy must +||| forbid (it carries harm); `Inform` / `Query` model benign actions. +||| +||| The verdict field is the faithful link to the deontic model in Types.idr: +||| a `Prohibition`-modality constraint that fires yields `Deny`, an +||| absent/`Permission` constraint yields `Allow`. +public export +data Action : Type where + ||| A purely informational action (e.g. answer a question). Policy: Allow. + Inform : (verdict : Verdict) -> Action + ||| A read-only query action. Policy: Allow. + Query : (verdict : Verdict) -> Action + ||| An action that deploys harm of a given domain/severity. A sound ethical + ||| policy assigns this `Deny`. This is the "bad case". + DeployHarm : (domain : HarmDomain) -> (severity : HarmSeverity) -> + (verdict : Verdict) -> Action + +||| Project the policy verdict out of an action (total over all constructors). +public export +verdictOf : Action -> Verdict +verdictOf (Inform v) = v +verdictOf (Query v) = v +verdictOf (DeployHarm _ _ v) = v + +-------------------------------------------------------------------------------- +-- The safety proposition: NO constructor for a denied action. +-------------------------------------------------------------------------------- + +||| `ActionPermitted a` is inhabited exactly when the policy verdict for `a` +||| is `Allow`. There is deliberately NO constructor admitting `Deny`: a +||| forbidden action is structurally uncertifiable. This is the core encoding +||| of "provably safe ethical constraints". +public export +data ActionPermitted : Action -> Type where + ||| The sole way to obtain a permission witness: the verdict is `Allow`. + PermitAllow : (prf : verdictOf a = Allow) -> ActionPermitted a + +-------------------------------------------------------------------------------- +-- Verdicts are decidably equal (needed for a sound+complete decision). +-------------------------------------------------------------------------------- + +||| `Deny = Allow` is absurd — the contradiction that powers safety. +public export +Uninhabited (Deny = Allow) where + uninhabited Refl impossible + +||| `Allow = Deny` is absurd too. +public export +Uninhabited (Allow = Deny) where + uninhabited Refl impossible + +||| Term-level transport helper (no case-of-Refl on stuck terms, per idioms): +||| from `verdictOf a = Allow` rebuild any needed equality. Here we only need +||| `Uninhabited` instances above, so no extra transport is required. + +-------------------------------------------------------------------------------- +-- Sound + complete decision procedure returning a genuine `Dec`. +-------------------------------------------------------------------------------- + +||| Decide whether an action is permitted. SOUND: a `Yes` carries a real +||| `ActionPermitted` witness. COMPLETE: a `No` carries a real refutation, +||| so nothing permitted is ever rejected. +public export +decActionPermitted : (a : Action) -> Dec (ActionPermitted a) +decActionPermitted a with (verdictOf a) proof eq + _ | Allow = Yes (PermitAllow eq) + _ | Deny = No (\ (PermitAllow prf) => + -- prf : verdictOf a = Allow, eq : verdictOf a = Deny + -- trans (sym eq) prf : Deny = Allow, which is absurd. + absurd (trans (sym eq) prf)) + +-------------------------------------------------------------------------------- +-- Certifier + machine-checked soundness. +-------------------------------------------------------------------------------- + +||| The ethical engine's certification verdict for an action. +||| Reuses the ABI `Result` type from Types.idr for the FFI boundary: +||| `Ok` == certified permitted, `ConstraintViolation` == refused. +public export +certifyPermitted : (a : Action) -> Result +certifyPermitted a = case decActionPermitted a of + Yes _ => Ok + No _ => ConstraintViolation + +||| SOUNDNESS of the certifier: if it returns `Ok`, the action really is +||| permitted. The proof inspects the same `Dec` the certifier used. +public export +certifyPermittedSound : (a : Action) -> certifyPermitted a = Ok -> ActionPermitted a +certifyPermittedSound a prf with (decActionPermitted a) + certifyPermittedSound a prf | Yes w = w + certifyPermittedSound a Refl | No _ impossible + +-------------------------------------------------------------------------------- +-- Concrete sample actions. +-------------------------------------------------------------------------------- + +||| A benign informational action the policy allows. +public export +safeInform : Action +safeInform = Inform Allow + +||| A harmful deployment action the policy forbids (critical physical harm). +public export +forbiddenDeploy : Action +forbiddenDeploy = DeployHarm Physical Critical Deny + +-------------------------------------------------------------------------------- +-- POSITIVE control: an explicit, inhabited permission witness. +-------------------------------------------------------------------------------- + +||| The allowed action genuinely carries a permission witness. +public export +safeInformPermitted : ActionPermitted Semantics.safeInform +safeInformPermitted = PermitAllow Refl + +-------------------------------------------------------------------------------- +-- NEGATIVE control (the core safety theorem): a forbidden action can NEVER +-- be certified permitted. +-------------------------------------------------------------------------------- + +||| SAFETY: there is no permission witness for the forbidden action. +||| `verdictOf forbiddenDeploy = Deny`, so any `PermitAllow prf` would give +||| `Deny = Allow`, which is absurd. Machine-checked. +public export +forbiddenNeverPermitted : Not (ActionPermitted Semantics.forbiddenDeploy) +forbiddenNeverPermitted (PermitAllow prf) = absurd prf + +||| Corollary at the certifier level: the forbidden action is never `Ok`. +||| If it were, soundness would hand us a witness the safety theorem refutes. +public export +forbiddenNeverCertifiedOk : Not (certifyPermitted Semantics.forbiddenDeploy = Ok) +forbiddenNeverCertifiedOk prf = + forbiddenNeverPermitted (certifyPermittedSound Semantics.forbiddenDeploy prf) diff --git a/src/interface/abi/phronesiser-abi.ipkg b/src/interface/abi/phronesiser-abi.ipkg index 9f51a92..2a614cf 100644 --- a/src/interface/abi/phronesiser-abi.ipkg +++ b/src/interface/abi/phronesiser-abi.ipkg @@ -9,3 +9,4 @@ modules = Phronesiser.ABI.Types , Phronesiser.ABI.Layout , Phronesiser.ABI.Foreign , Phronesiser.ABI.Proofs + , Phronesiser.ABI.Semantics From 2448a98574c24d2236e136efcaee088d1977045c Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 28 Jun 2026 03:18:22 +0000 Subject: [PATCH 2/4] Add Layer-3 ABI invariants: monotone safety under policy composition MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit New module Phronesiser.ABI.Invariants, built over the existing Layer-2 Semantics model (Action / Verdict / verdictOf — nothing redefined). It proves two properties strictly deeper than the Layer-2 single-action safety theorem, both quantified over all actions and over policies: 1. Monotone safety (downward-closure of permission): if policy p2 tightens p1, every action p1 forbids stays forbidden under p2 — tightening never re-permits a previously-forbidden action; the permitted set only shrinks. Tightening is a proven preorder (reflexive + transitive). 2. Conjunction composition: an action permitted under andPolicy p1 p2 is permitted under each conjunct (iff via bothPermitsAnd), and the conjunction provably tightens each conjunct. Includes a sound+complete Dec (Permits p a), sample policies over the shared model, positive controls (witnesses + a live application of the monotone-safety theorem) and negative/non-vacuity controls in Not(...) form. %default total; no believe_me / postulate / assert_total / sorry / asserted equalities. Builds with zero warnings; an adversarial false proof (tightened policy permits the forbidden action) is rejected by the type checker. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx --- .../abi/Phronesiser/ABI/Invariants.idr | 304 ++++++++++++++++++ src/interface/abi/phronesiser-abi.ipkg | 1 + 2 files changed, 305 insertions(+) create mode 100644 src/interface/abi/Phronesiser/ABI/Invariants.idr diff --git a/src/interface/abi/Phronesiser/ABI/Invariants.idr b/src/interface/abi/Phronesiser/ABI/Invariants.idr new file mode 100644 index 0000000..077d4d4 --- /dev/null +++ b/src/interface/abi/Phronesiser/ABI/Invariants.idr @@ -0,0 +1,304 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +||| Layer-3 invariants for Phronesiser: MONOTONE SAFETY under policy +||| composition — a strictly deeper property than the Layer-2 flagship. +||| +||| Layer 2 (`Phronesiser.ABI.Semantics`) proves a property of ONE action under +||| ONE fixed static verdict: a forbidden action can never be certified +||| permitted. This module proves properties of WHOLE POLICIES and their +||| composition — quantified over all actions and over the space of policies: +||| +||| 1. DOWNWARD-CLOSURE OF PERMISSION (monotone safety): if a policy `p2` +||| *tightens* `p1` (everything `p2` permits, `p1` already permitted), +||| then everything `p1` forbids, `p2` still forbids. Adding constraints +||| NEVER re-permits a previously-forbidden action — the permitted set +||| only shrinks. This is the safety-preservation law an ethical engine +||| must satisfy when policies are strengthened at runtime. +||| +||| 2. CONJUNCTION COMPOSITION: an action permitted under the conjunction +||| `andPolicy p1 p2` is permitted under `p1` AND under `p2` separately; +||| and `andPolicy p1 p2` provably tightens each conjunct. So composing +||| policies by conjunction is sound: it can only forbid more. +||| +||| Both are reused over the SAME model from `Semantics` (Action / Verdict / +||| verdictOf) — no datatype is redefined. A sound+complete `Dec (Permits ...)` +||| is provided. Positive and negative/non-vacuity controls are machine-checked. +||| +||| Every fact below is discharged by the Idris2 type checker. No `believe_me`, +||| `idris_crash`, `assert_total`, `postulate`, `sorry`, or asserted equalities. + +module Phronesiser.ABI.Invariants + +import Phronesiser.ABI.Types +import Phronesiser.ABI.Semantics + +%default total + +-------------------------------------------------------------------------------- +-- Verdict trichotomy (here, dichotomy): Allow or Deny, nothing else. +-------------------------------------------------------------------------------- + +||| Every verdict is `Allow` or `Deny`. This total case analysis is the engine +||| behind monotone safety: "not Allow" forces "Deny". +public export +verdictDichotomy : (v : Verdict) -> Either (v = Allow) (v = Deny) +verdictDichotomy Allow = Left Refl +verdictDichotomy Deny = Right Refl + +-------------------------------------------------------------------------------- +-- Policies as verdict-assignments over the shared Action model. +-------------------------------------------------------------------------------- + +||| A policy assigns a verdict to every candidate action. This refines the +||| static `verdictOf` from `Semantics`: different ethical rule-sets induce +||| different policies over the same action space. +public export +Policy : Type +Policy = Action -> Verdict + +||| `Permits p a` : the policy `p` permits action `a`. +public export +Permits : Policy -> Action -> Type +Permits p a = p a = Allow + +||| `Forbids p a` : the policy `p` forbids action `a`. +public export +Forbids : Policy -> Action -> Type +Forbids p a = p a = Deny + +||| A policy cannot both permit and forbid the same action (Allow /= Deny). +||| This is the local consistency of any single policy. +public export +permitForbidExclusive : (p : Policy) -> (a : Action) -> + Permits p a -> Forbids p a -> Void +permitForbidExclusive p a perm forb = + -- perm : p a = Allow ; forb : p a = Deny ; so Allow = Deny, absurd. + absurd (trans (sym perm) forb) + +-------------------------------------------------------------------------------- +-- Policy tightening (the ordering on policies). +-------------------------------------------------------------------------------- + +||| `Tightens p2 p1` : `p2` is at least as strict as `p1` — every action `p2` +||| permits was already permitted by `p1`. Equivalently the permitted set of +||| `p2` is contained in that of `p1`. +public export +Tightens : Policy -> Policy -> Type +Tightens p2 p1 = (a : Action) -> Permits p2 a -> Permits p1 a + +||| Tightening is reflexive: a policy is at least as strict as itself. +public export +tightensRefl : (p : Policy) -> Tightens p p +tightensRefl p = \a, perm => perm + +||| Tightening is transitive: it is a genuine preorder on policies. +public export +tightensTrans : {p1, p2, p3 : Policy} -> + Tightens p3 p2 -> Tightens p2 p1 -> Tightens p3 p1 +tightensTrans t32 t21 = \a, perm => t21 a (t32 a perm) + +-------------------------------------------------------------------------------- +-- THEOREM 1: Monotone safety — the forbidden set only grows under tightening. +-------------------------------------------------------------------------------- + +||| MONOTONE SAFETY (downward-closure of permission, in forbidden form): +||| if `p2` tightens `p1`, then anything `p1` forbids is still forbidden by +||| `p2`. Tightening a policy never re-permits a previously-forbidden action. +||| +||| Proof: suppose `p1` forbids `a` but `p2` does NOT forbid it. By dichotomy +||| `p2 a = Allow`, i.e. `p2` permits `a`; tightening then gives `p1` permits +||| `a`, contradicting `p1` forbids `a`. So `p2 a = Deny`. +public export +tighteningPreservesForbidden : {p1, p2 : Policy} -> {a : Action} -> + Tightens p2 p1 -> Forbids p1 a -> Forbids p2 a +tighteningPreservesForbidden t forb1 = + case verdictDichotomy (p2 a) of + Right denyEq => denyEq + Left allowEq => + -- allowEq : p2 a = Allow = Permits p2 a ; t a allowEq : Permits p1 a + -- forb1 : p1 a = Deny ; contradiction. + absurd (permitForbidExclusive p1 a (t a allowEq) forb1) + +||| Equivalent CONTRAPOSITIVE phrasing kept for the API surface: under +||| tightening, if `p2` permits an action then `p1` permitted it (this is just +||| the definition of `Tightens`, restated as a named law). +public export +tighteningShrinksPermitted : {p1, p2 : Policy} -> {a : Action} -> + Tightens p2 p1 -> Permits p2 a -> Permits p1 a +tighteningShrinksPermitted t perm2 = t a perm2 + +-------------------------------------------------------------------------------- +-- Conjunction of policies. +-------------------------------------------------------------------------------- + +||| Conjoin two policies: the result permits an action only when BOTH permit it, +||| and forbids it otherwise. This is how an ethical engine layers an extra +||| constraint set on top of an existing one. +public export +andPolicy : Policy -> Policy -> Policy +andPolicy p1 p2 a = + case p1 a of + Allow => p2 a + Deny => Deny + +-------------------------------------------------------------------------------- +-- THEOREM 2: Conjunction composition is sound. +-------------------------------------------------------------------------------- + +||| If the conjunction permits an action, then the FIRST conjunct permits it. +||| Proof by case on `p1 a`: if it were `Deny`, the conjunction would be `Deny`, +||| contradicting the `= Allow` hypothesis. +public export +andPermitsLeft : (p1, p2 : Policy) -> (a : Action) -> + Permits (andPolicy p1 p2) a -> Permits p1 a +andPermitsLeft p1 p2 a perm with (p1 a) proof eqp1 + andPermitsLeft p1 p2 a perm | Allow = Refl + andPermitsLeft p1 p2 a perm | Deny = + -- with p1 a = Deny, andPolicy reduces to Deny, so perm : Deny = Allow. + absurd perm + +||| If the conjunction permits an action, then the SECOND conjunct permits it. +||| When `p1 a = Allow`, `andPolicy p1 p2 a` reduces to `p2 a`, so the +||| hypothesis IS `p2 a = Allow`. +public export +andPermitsRight : (p1, p2 : Policy) -> (a : Action) -> + Permits (andPolicy p1 p2) a -> Permits p2 a +andPermitsRight p1 p2 a perm with (p1 a) proof eqp1 + andPermitsRight p1 p2 a perm | Allow = perm + andPermitsRight p1 p2 a perm | Deny = absurd perm + +||| Full composition soundness: conjunction-permission gives BOTH permissions. +public export +andPermitsBoth : (p1, p2 : Policy) -> (a : Action) -> + Permits (andPolicy p1 p2) a -> (Permits p1 a, Permits p2 a) +andPermitsBoth p1 p2 a perm = + (andPermitsLeft p1 p2 a perm, andPermitsRight p1 p2 a perm) + +||| Conversely, if both conjuncts permit, the conjunction permits. +||| Together with `andPermitsBoth` this is an iff: conjunction-permission is +||| exactly the pairwise conjunction of permissions. +public export +bothPermitsAnd : (p1, p2 : Policy) -> (a : Action) -> + Permits p1 a -> Permits p2 a -> Permits (andPolicy p1 p2) a +bothPermitsAnd p1 p2 a perm1 perm2 with (p1 a) proof eqp1 + bothPermitsAnd p1 p2 a perm1 perm2 | Allow = perm2 + bothPermitsAnd p1 p2 a perm1 perm2 | Deny = + -- with p1 a = Deny, perm1 : Deny = Allow is absurd. + absurd perm1 + +||| Conjunction tightens its first conjunct: `andPolicy p1 p2` is at least as +||| strict as `p1`. (Hence, by Theorem 1, it can only forbid more than `p1`.) +public export +andTightensLeft : (p1, p2 : Policy) -> Tightens (andPolicy p1 p2) p1 +andTightensLeft p1 p2 = \a, perm => andPermitsLeft p1 p2 a perm + +||| Conjunction tightens its second conjunct too. +public export +andTightensRight : (p1, p2 : Policy) -> Tightens (andPolicy p1 p2) p2 +andTightensRight p1 p2 = \a, perm => andPermitsRight p1 p2 a perm + +-------------------------------------------------------------------------------- +-- Sound + complete decision procedure for permission under a policy. +-------------------------------------------------------------------------------- + +||| Decide whether a policy permits an action. SOUND: a `Yes` carries a real +||| `Permits` proof. COMPLETE: a `No` carries a real refutation. +public export +decPermits : (p : Policy) -> (a : Action) -> Dec (Permits p a) +decPermits p a with (p a) proof eq + decPermits p a | Allow = Yes Refl + decPermits p a | Deny = + No (\perm => absurd perm) + +-------------------------------------------------------------------------------- +-- Sample policies built over the SHARED model. +-------------------------------------------------------------------------------- + +||| The static base policy: read the verdict already attached to the action. +public export +basePolicy : Policy +basePolicy = verdictOf + +||| A strictly stronger policy that additionally forbids EVERY `DeployHarm` +||| action regardless of its attached verdict (e.g. a freshly added "no harm +||| deployment, ever" constraint). On non-DeployHarm actions it agrees with +||| the base policy. +public export +noHarmDeployPolicy : Policy +noHarmDeployPolicy (DeployHarm _ _ _) = Deny +noHarmDeployPolicy a = verdictOf a + +-------------------------------------------------------------------------------- +-- POSITIVE controls. +-------------------------------------------------------------------------------- + +||| The base policy permits the benign informational action from `Semantics`. +public export +basePermitsSafeInform : Permits Invariants.basePolicy Semantics.safeInform +basePermitsSafeInform = Refl + +||| `noHarmDeployPolicy` genuinely tightens the base policy (machine-checked, +||| quantified over all actions). This is a positive instance of Theorem 1's +||| hypothesis. +public export +noHarmTightensBase : Tightens Invariants.noHarmDeployPolicy Invariants.basePolicy +noHarmTightensBase (Inform v) perm = perm +noHarmTightensBase (Query v) perm = perm +noHarmTightensBase (DeployHarm d s v) perm = absurd perm + -- For DeployHarm, noHarmDeployPolicy = Deny, so perm : Deny = Allow is absurd. + +||| Live application of Theorem 1: because `noHarmDeployPolicy` tightens the +||| base policy and the base policy forbids `forbiddenDeploy`, the tightened +||| policy still forbids it. (Both base and tightened forbid here; the point is +||| that monotone safety is witnessed on a concrete pair.) +public export +forbiddenStaysForbidden : + Forbids Invariants.noHarmDeployPolicy Semantics.forbiddenDeploy +forbiddenStaysForbidden = + tighteningPreservesForbidden + {p1 = basePolicy} {p2 = noHarmDeployPolicy} {a = forbiddenDeploy} + noHarmTightensBase Refl + +||| Composition positive control: under `andPolicy basePolicy basePolicy`, +||| the benign action is permitted, and decomposes to both conjuncts. +public export +andPermitsSafeInform : + ( Permits Invariants.basePolicy Semantics.safeInform + , Permits Invariants.basePolicy Semantics.safeInform ) +andPermitsSafeInform = + andPermitsBoth basePolicy basePolicy safeInform Refl + +-------------------------------------------------------------------------------- +-- NEGATIVE / non-vacuity controls. +-------------------------------------------------------------------------------- + +||| Non-vacuity of monotone safety: the tightened policy does NOT permit the +||| forbidden action. Any such permission would, with `forbiddenStaysForbidden`, +||| give `Deny = Allow`. Machine-checked `Not (...)`. +public export +tightenedRefusesForbidden : + Not (Permits Invariants.noHarmDeployPolicy Semantics.forbiddenDeploy) +tightenedRefusesForbidden perm = + absurd (trans (sym perm) forbiddenStaysForbidden) + +||| Non-vacuity of composition: the conjunction of the base policy with the +||| all-DeployHarm-denying policy does NOT permit `forbiddenDeploy`. If it did, +||| `andPermitsRight` would extract a `noHarmDeployPolicy` permission, which +||| `tightenedRefusesForbidden` refutes. +public export +andRefusesForbidden : + Not (Permits (andPolicy Invariants.basePolicy Invariants.noHarmDeployPolicy) + Semantics.forbiddenDeploy) +andRefusesForbidden perm = + tightenedRefusesForbidden + (andPermitsRight basePolicy noHarmDeployPolicy forbiddenDeploy perm) + +||| A policy can NEVER both permit and forbid the same action — restated as a +||| concrete refutation that `basePolicy` simultaneously permits and forbids +||| the benign action (it permits it, so "forbids" is impossible). +public export +baseNotForbidsSafeInform : + Not (Forbids Invariants.basePolicy Semantics.safeInform) +baseNotForbidsSafeInform forb = + permitForbidExclusive basePolicy safeInform basePermitsSafeInform forb diff --git a/src/interface/abi/phronesiser-abi.ipkg b/src/interface/abi/phronesiser-abi.ipkg index 2a614cf..dc1f0d0 100644 --- a/src/interface/abi/phronesiser-abi.ipkg +++ b/src/interface/abi/phronesiser-abi.ipkg @@ -10,3 +10,4 @@ modules = Phronesiser.ABI.Types , Phronesiser.ABI.Foreign , Phronesiser.ABI.Proofs , Phronesiser.ABI.Semantics + , Phronesiser.ABI.Invariants From 057d422c680d8ee6713f0f5d475db29384cef193 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 28 Jun 2026 06:12:31 +0000 Subject: [PATCH 3/4] Add Layer-4 FfiSeam proof sealing the ABI<->FFI seam Prove the FFI result-code encoding is SOUND, not just structurally agreed (the abi-ffi-gate.py check): distinct ABI outcomes never collide on the wire, and the C integer faithfully round-trips back. New module Phronesiser.ABI.FfiSeam (imports Phronesiser.ABI.Types): - intToResult decoder + resultRoundTrip (left inverse of resultToInt) - resultToIntInjective derived from the round-trip via justInj + cong - same round-trip + injectivity for modalityToInt (DeonticModality) and severityToInt (HarmSeverity); no ProofStatus/statusToInt exists - positive controls (concrete decode = Refl) and non-vacuity controls (distinct codes have distinct ints, machine-checked) Genuine proof only: no believe_me/idris_crash/assert_total/postulate. %default total, SPDX header, zero warnings. abi package builds clean; an adversarial false claim (resultToInt Ok = resultToInt Error) is rejected by the type checker. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx --- src/interface/abi/Phronesiser/ABI/FfiSeam.idr | 199 ++++++++++++++++++ src/interface/abi/phronesiser-abi.ipkg | 1 + 2 files changed, 200 insertions(+) create mode 100644 src/interface/abi/Phronesiser/ABI/FfiSeam.idr diff --git a/src/interface/abi/Phronesiser/ABI/FfiSeam.idr b/src/interface/abi/Phronesiser/ABI/FfiSeam.idr new file mode 100644 index 0000000..5e18003 --- /dev/null +++ b/src/interface/abi/Phronesiser/ABI/FfiSeam.idr @@ -0,0 +1,199 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +||| Layer-4 proof: SEALING THE ABI<->FFI SEAM for Phronesiser. +||| +||| The structural gate (scripts/abi-ffi-gate.py) checks the Idris and Zig +||| result-code enums agree by name+value. This module is the PROOF-SIDE +||| guarantee that the encoding is SOUND: +||| +||| * distinct ABI outcomes never collide on the wire (injectivity), and +||| * the C integer faithfully round-trips back to the ABI value +||| (a total decoder `intToResult` is a left inverse of `resultToInt`). +||| +||| Injectivity is DERIVED from the round-trip via `justInj` + `cong`, +||| which is the cleanest route once the decoder's round-trip `Refl`s reduce. +||| The decoder is written with boolean `Bits32` `==` (which reduces on +||| concrete literals), so `resultRoundTrip Ok = Refl` etc. all check +||| definitionally. +||| +||| The same injectivity is also proved for the other FFI enum encoders +||| present in `Types`: `modalityToInt` (DeonticModality) and `severityToInt` +||| (HarmSeverity). (There is no `ProofStatus`/`statusToInt` in this repo.) +||| +||| Controls: positive (concrete decode = Refl), and a machine-checked +||| NON-VACUITY control that two DISTINCT result codes have distinct ints. +||| +||| Genuine proof only — no believe_me / idris_crash / assert_total / +||| postulate / sorry. %default total. + +module Phronesiser.ABI.FfiSeam + +import Phronesiser.ABI.Types + +%default total + +-------------------------------------------------------------------------------- +-- Generic helper +-------------------------------------------------------------------------------- + +||| `Just` is injective. Used to turn a round-trip equality through the +||| decoder back into an equality of the underlying ABI values. +public export +justInj : {0 a, b : ty} -> Just a = Just b -> a = b +justInj Refl = Refl + +-------------------------------------------------------------------------------- +-- Result: faithful decoder + round-trip + derived injectivity +-------------------------------------------------------------------------------- + +||| Decode a C integer back into a `Result`. +||| Written with boolean `Bits32` `==` so it reduces on concrete literals, +||| making the round-trip `Refl`s check definitionally. Unknown codes +||| decode to `Nothing` (the wire space is larger than the ABI space). +public export +intToResult : Bits32 -> Maybe Result +intToResult x = + if x == 0 then Just Ok + else if x == 1 then Just Error + else if x == 2 then Just InvalidParam + else if x == 3 then Just OutOfMemory + else if x == 4 then Just NullPointer + else if x == 5 then Just ConstraintViolation + else if x == 6 then Just ConstraintConflict + else Nothing + +||| The decoder is a left inverse of the encoder: every ABI value round-trips +||| losslessly through its C integer. FAITHFULNESS of the encoding. +public export +resultRoundTrip : (r : Result) -> intToResult (resultToInt r) = Just r +resultRoundTrip Ok = Refl +resultRoundTrip Error = Refl +resultRoundTrip InvalidParam = Refl +resultRoundTrip OutOfMemory = Refl +resultRoundTrip NullPointer = Refl +resultRoundTrip ConstraintViolation = Refl +resultRoundTrip ConstraintConflict = Refl + +||| The encoding is UNAMBIGUOUS: distinct ABI outcomes never collide on the +||| wire. Derived from the round-trip (a function with a left inverse is +||| injective) via `cong` + `justInj`. +public export +resultToIntInjective : (a, b : Result) -> resultToInt a = resultToInt b -> a = b +resultToIntInjective a b prf = + justInj $ + trans (sym (resultRoundTrip a)) + (trans (cong intToResult prf) (resultRoundTrip b)) + +-------------------------------------------------------------------------------- +-- DeonticModality: same guarantees (task (c)) +-------------------------------------------------------------------------------- + +||| Decode a C integer back into a `DeonticModality`. +public export +intToModality : Bits32 -> Maybe DeonticModality +intToModality x = + if x == 0 then Just Obligation + else if x == 1 then Just Permission + else if x == 2 then Just Prohibition + else Nothing + +||| Round-trip / faithfulness for the deontic-modality encoder. +public export +modalityRoundTrip : (m : DeonticModality) -> + intToModality (modalityToInt m) = Just m +modalityRoundTrip Obligation = Refl +modalityRoundTrip Permission = Refl +modalityRoundTrip Prohibition = Refl + +||| Injectivity for the deontic-modality encoder, derived from round-trip. +public export +modalityToIntInjective : (a, b : DeonticModality) -> + modalityToInt a = modalityToInt b -> a = b +modalityToIntInjective a b prf = + justInj $ + trans (sym (modalityRoundTrip a)) + (trans (cong intToModality prf) (modalityRoundTrip b)) + +-------------------------------------------------------------------------------- +-- HarmSeverity: same guarantees (task (c)) +-------------------------------------------------------------------------------- + +||| Decode a C integer back into a `HarmSeverity`. +public export +intToSeverity : Bits32 -> Maybe HarmSeverity +intToSeverity x = + if x == 0 then Just Negligible + else if x == 1 then Just Minor + else if x == 2 then Just Moderate + else if x == 3 then Just Severe + else if x == 4 then Just Critical + else Nothing + +||| Round-trip / faithfulness for the harm-severity encoder. +public export +severityRoundTrip : (s : HarmSeverity) -> + intToSeverity (severityToInt s) = Just s +severityRoundTrip Negligible = Refl +severityRoundTrip Minor = Refl +severityRoundTrip Moderate = Refl +severityRoundTrip Severe = Refl +severityRoundTrip Critical = Refl + +||| Injectivity for the harm-severity encoder, derived from round-trip. +public export +severityToIntInjective : (a, b : HarmSeverity) -> + severityToInt a = severityToInt b -> a = b +severityToIntInjective a b prf = + justInj $ + trans (sym (severityRoundTrip a)) + (trans (cong intToSeverity prf) (severityRoundTrip b)) + +-------------------------------------------------------------------------------- +-- Positive controls (concrete decode = Refl, machine-checked) +-------------------------------------------------------------------------------- + +||| Positive control: 0 decodes to Ok. +public export +decodeOkControl : FfiSeam.intToResult 0 = Just Ok +decodeOkControl = Refl + +||| Positive control: 6 decodes to ConstraintConflict (the top code). +public export +decodeConflictControl : FfiSeam.intToResult 6 = Just ConstraintConflict +decodeConflictControl = Refl + +||| Positive control: an out-of-range code decodes to Nothing. +public export +decodeUnknownControl : FfiSeam.intToResult 7 = Nothing +decodeUnknownControl = Refl + +-------------------------------------------------------------------------------- +-- Negative / non-vacuity controls (machine-checked) +-------------------------------------------------------------------------------- + +||| NON-VACUITY: two DISTINCT result codes have DISTINCT C integers. +||| If `resultToInt` were constant the seam would be vacuously "sound"; +||| this rules that out. `Ok` -> 0, `Error` -> 1, and `0 = 1` is impossible +||| for distinct primitive `Bits32` literals. +public export +okErrorDistinct : Not (resultToInt Ok = resultToInt Error) +okErrorDistinct = \case Refl impossible + +||| Non-vacuity at the other end of the enum: the two highest codes differ. +public export +violationConflictDistinct : + Not (resultToInt ConstraintViolation = resultToInt ConstraintConflict) +violationConflictDistinct = \case Refl impossible + +||| Non-vacuity for the deontic-modality encoder. +public export +obligationProhibitionDistinct : + Not (modalityToInt Obligation = modalityToInt Prohibition) +obligationProhibitionDistinct = \case Refl impossible + +||| Non-vacuity for the harm-severity encoder. +public export +negligibleCriticalDistinct : + Not (severityToInt Negligible = severityToInt Critical) +negligibleCriticalDistinct = \case Refl impossible diff --git a/src/interface/abi/phronesiser-abi.ipkg b/src/interface/abi/phronesiser-abi.ipkg index dc1f0d0..1f5a047 100644 --- a/src/interface/abi/phronesiser-abi.ipkg +++ b/src/interface/abi/phronesiser-abi.ipkg @@ -11,3 +11,4 @@ modules = Phronesiser.ABI.Types , Phronesiser.ABI.Proofs , Phronesiser.ABI.Semantics , Phronesiser.ABI.Invariants + , Phronesiser.ABI.FfiSeam From eae8ce0b78cdc976f49f6114f03ff53188f35545 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 28 Jun 2026 07:07:54 +0000 Subject: [PATCH 4/4] Add Layer-5 capstone ABI soundness certificate Assemble the existing Layer-2/3/4 proofs into one inhabited certificate record (ABISound) and value (abiContractDischarged) in Phronesiser.ABI.Capstone, tying the flagship safety property, the monotone-safety invariant, and the FFI-seam injectivity into one end-to-end soundness statement. Reuses only already-exported witnesses (safeInformPermitted, noHarmTightensBase, forbiddenStaysForbidden, resultToIntInjective). No new axioms; %default total; zero warnings. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx --- .../abi/Phronesiser/ABI/Capstone.idr | 106 ++++++++++++++++++ src/interface/abi/phronesiser-abi.ipkg | 1 + 2 files changed, 107 insertions(+) create mode 100644 src/interface/abi/Phronesiser/ABI/Capstone.idr diff --git a/src/interface/abi/Phronesiser/ABI/Capstone.idr b/src/interface/abi/Phronesiser/ABI/Capstone.idr new file mode 100644 index 0000000..a5649b1 --- /dev/null +++ b/src/interface/abi/Phronesiser/ABI/Capstone.idr @@ -0,0 +1,106 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +||| Layer-5 CAPSTONE: a single end-to-end ABI SOUNDNESS CERTIFICATE for +||| Phronesiser. +||| +||| This module proves NO new domain theorem. It ASSEMBLES the facts already +||| discharged by the prior proof layers into ONE inhabited record value, +||| `abiContractDischarged`. Because that value can only be constructed from +||| genuine witnesses exported by the lower layers, its mere existence (the +||| fact that this module type-checks) certifies that the whole ABI contract +||| is satisfied TOGETHER, end to end: +||| +||| manifest (phronesiser.toml: "provably safe ethical constraints") +||| -> Layer-2 FLAGSHIP semantics (Phronesiser.ABI.Semantics) +||| the canonical positive control `safeInformPermitted` witnesses +||| that the permitted action genuinely carries a permission proof, +||| the live half of the safety property whose negative half is +||| `forbiddenNeverPermitted`. +||| -> Layer-3 deeper INVARIANT (Phronesiser.ABI.Invariants) +||| `noHarmTightensBase` witnesses monotone safety's hypothesis +||| (the stronger policy really tightens the base policy, quantified +||| over all actions), and `forbiddenStaysForbidden` is the live +||| application: tightening never re-permits a forbidden action. +||| -> Layer-4 FFI SEAM (Phronesiser.ABI.FfiSeam) +||| `resultToIntInjective` witnesses that distinct ABI outcomes never +||| collide on the C wire — the boundary at which the proofs meet code. +||| +||| If ANY of those prior layers were unsound, the corresponding field below +||| would have no inhabitant and `abiContractDischarged` would not type-check. +||| The certificate is therefore a genuine composition, not a restatement. +||| +||| Genuine proof only — no believe_me / idris_crash / assert_total / +||| postulate / sorry / %hint hacks. Every field is an already-exported +||| witness from the layer named above. %default total. + +module Phronesiser.ABI.Capstone + +import Phronesiser.ABI.Types +import Phronesiser.ABI.Semantics +import Phronesiser.ABI.Invariants +import Phronesiser.ABI.FfiSeam + +%default total + +-------------------------------------------------------------------------------- +-- The capstone certificate type. +-------------------------------------------------------------------------------- + +||| `ABISound` bundles the key proven facts of the Phronesiser ABI, one field +||| per proof layer. An inhabitant is a machine-checked certificate that the +||| flagship safety property, the deeper monotone-safety invariant, and the +||| FFI-seam injectivity all hold simultaneously over the SAME shared model. +public export +record ABISound where + constructor MkABISound + + ||| Layer-2 flagship (positive control): the canonical benign action really + ||| is permitted — reuses `Semantics.safeInformPermitted`. + flagshipPermits : ActionPermitted Semantics.safeInform + + ||| Layer-3 invariant (hypothesis witness): the stronger "no harm deploy" + ||| policy genuinely tightens the base policy, quantified over all actions + ||| — reuses `Invariants.noHarmTightensBase`. + invariantTightens : Tightens Invariants.noHarmDeployPolicy Invariants.basePolicy + + ||| Layer-3 invariant (live application): tightening preserves the forbidden + ||| verdict on the canonical forbidden action — reuses + ||| `Invariants.forbiddenStaysForbidden`. + invariantPreservesForbidden : + Forbids Invariants.noHarmDeployPolicy Semantics.forbiddenDeploy + + ||| Layer-4 FFI seam: distinct ABI result codes never collide on the wire + ||| — reuses `FfiSeam.resultToIntInjective`. + seamInjective : + (a, b : Result) -> resultToInt a = resultToInt b -> a = b + +-------------------------------------------------------------------------------- +-- The capstone value: the ABI contract, discharged. +-------------------------------------------------------------------------------- + +||| THE CAPSTONE. A single inhabited certificate assembled purely from the +||| exported witnesses of Layers 2-4. It type-checks iff every prior layer is +||| sound; constructing it is the end-to-end soundness statement that ties the +||| manifest's promise, the ABI proofs (flagship + invariant), and the FFI seam +||| into one value. +public export +abiContractDischarged : ABISound +abiContractDischarged = MkABISound + { flagshipPermits = Semantics.safeInformPermitted + , invariantTightens = Invariants.noHarmTightensBase + , invariantPreservesForbidden = Invariants.forbiddenStaysForbidden + , seamInjective = FfiSeam.resultToIntInjective + } + +-------------------------------------------------------------------------------- +-- Projection sanity: the certificate's fields ARE the real theorems. +-------------------------------------------------------------------------------- + +||| The seam-injectivity field of the discharged certificate is exactly the +||| Layer-4 theorem (definitional). Confirms the capstone exposes, not shadows, +||| the underlying proof. +public export +capstoneSeamIsResultToIntInjective : + seamInjective Capstone.abiContractDischarged = FfiSeam.resultToIntInjective +capstoneSeamIsResultToIntInjective = Refl diff --git a/src/interface/abi/phronesiser-abi.ipkg b/src/interface/abi/phronesiser-abi.ipkg index 1f5a047..484deb6 100644 --- a/src/interface/abi/phronesiser-abi.ipkg +++ b/src/interface/abi/phronesiser-abi.ipkg @@ -12,3 +12,4 @@ modules = Phronesiser.ABI.Types , Phronesiser.ABI.Semantics , Phronesiser.ABI.Invariants , Phronesiser.ABI.FfiSeam + , Phronesiser.ABI.Capstone