Skip to content

Commit 6a7e723

Browse files
claudeclaude
committed
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 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx
1 parent 31f6d0c commit 6a7e723

2 files changed

Lines changed: 172 additions & 0 deletions

File tree

‎src/interface/abi/Phronesiser/ABI/Semantics.idr‎

Lines changed: 171 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,171 @@
1+
-- SPDX-License-Identifier: MPL-2.0
2+
-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
3+
--
4+
||| Flagship semantic proof for Phronesiser: ethical safety of action gating.
5+
|||
6+
||| Headline domain property ("Add provably safe ethical constraints to AI
7+
||| agents"): a deontic policy partitions an agent's candidate actions into
8+
||| PERMITTED and FORBIDDEN. We define an `ActionPermitted` proposition that
9+
||| has NO constructor for a forbidden action. Therefore a forbidden action
10+
||| can NEVER be certified permitted — the safety guarantee an ethical
11+
||| constraint engine must provide. The decision procedure is sound AND
12+
||| complete (returns a genuine `Dec`), and the certifier's soundness is
13+
||| machine-checked: if `certifyPermitted a = Permitted`, then `ActionPermitted`
14+
||| holds. Positive and negative controls pin non-vacuity.
15+
|||
16+
||| This is not a runtime test: every fact below is discharged by the Idris2
17+
||| type checker. The negative control `forbiddenNeverPermitted` is the core
18+
||| safety theorem in `Not (...)` form.
19+
20+
module Phronesiser.ABI.Semantics
21+
22+
import Phronesiser.ABI.Types
23+
import Data.So
24+
import Decidable.Equality
25+
26+
%default total
27+
28+
--------------------------------------------------------------------------------
29+
-- A faithful, minimal model of agent actions.
30+
--------------------------------------------------------------------------------
31+
32+
||| The classification a policy assigns to an action.
33+
||| - Allow: the action is permissible.
34+
||| - Deny : the action is forbidden (a prohibition applies).
35+
public export
36+
data Verdict = Allow | Deny
37+
38+
||| A candidate agent action, carrying the policy verdict the ethical engine
39+
||| has resolved for it. `DeployHarm` models an action a sound policy must
40+
||| forbid (it carries harm); `Inform` / `Query` model benign actions.
41+
|||
42+
||| The verdict field is the faithful link to the deontic model in Types.idr:
43+
||| a `Prohibition`-modality constraint that fires yields `Deny`, an
44+
||| absent/`Permission` constraint yields `Allow`.
45+
public export
46+
data Action : Type where
47+
||| A purely informational action (e.g. answer a question). Policy: Allow.
48+
Inform : (verdict : Verdict) -> Action
49+
||| A read-only query action. Policy: Allow.
50+
Query : (verdict : Verdict) -> Action
51+
||| An action that deploys harm of a given domain/severity. A sound ethical
52+
||| policy assigns this `Deny`. This is the "bad case".
53+
DeployHarm : (domain : HarmDomain) -> (severity : HarmSeverity) ->
54+
(verdict : Verdict) -> Action
55+
56+
||| Project the policy verdict out of an action (total over all constructors).
57+
public export
58+
verdictOf : Action -> Verdict
59+
verdictOf (Inform v) = v
60+
verdictOf (Query v) = v
61+
verdictOf (DeployHarm _ _ v) = v
62+
63+
--------------------------------------------------------------------------------
64+
-- The safety proposition: NO constructor for a denied action.
65+
--------------------------------------------------------------------------------
66+
67+
||| `ActionPermitted a` is inhabited exactly when the policy verdict for `a`
68+
||| is `Allow`. There is deliberately NO constructor admitting `Deny`: a
69+
||| forbidden action is structurally uncertifiable. This is the core encoding
70+
||| of "provably safe ethical constraints".
71+
public export
72+
data ActionPermitted : Action -> Type where
73+
||| The sole way to obtain a permission witness: the verdict is `Allow`.
74+
PermitAllow : (prf : verdictOf a = Allow) -> ActionPermitted a
75+
76+
--------------------------------------------------------------------------------
77+
-- Verdicts are decidably equal (needed for a sound+complete decision).
78+
--------------------------------------------------------------------------------
79+
80+
||| `Deny = Allow` is absurd — the contradiction that powers safety.
81+
public export
82+
Uninhabited (Deny = Allow) where
83+
uninhabited Refl impossible
84+
85+
||| `Allow = Deny` is absurd too.
86+
public export
87+
Uninhabited (Allow = Deny) where
88+
uninhabited Refl impossible
89+
90+
||| Term-level transport helper (no case-of-Refl on stuck terms, per idioms):
91+
||| from `verdictOf a = Allow` rebuild any needed equality. Here we only need
92+
||| `Uninhabited` instances above, so no extra transport is required.
93+
94+
--------------------------------------------------------------------------------
95+
-- Sound + complete decision procedure returning a genuine `Dec`.
96+
--------------------------------------------------------------------------------
97+
98+
||| Decide whether an action is permitted. SOUND: a `Yes` carries a real
99+
||| `ActionPermitted` witness. COMPLETE: a `No` carries a real refutation,
100+
||| so nothing permitted is ever rejected.
101+
public export
102+
decActionPermitted : (a : Action) -> Dec (ActionPermitted a)
103+
decActionPermitted a with (verdictOf a) proof eq
104+
_ | Allow = Yes (PermitAllow eq)
105+
_ | Deny = No (\ (PermitAllow prf) =>
106+
-- prf : verdictOf a = Allow, eq : verdictOf a = Deny
107+
-- trans (sym eq) prf : Deny = Allow, which is absurd.
108+
absurd (trans (sym eq) prf))
109+
110+
--------------------------------------------------------------------------------
111+
-- Certifier + machine-checked soundness.
112+
--------------------------------------------------------------------------------
113+
114+
||| The ethical engine's certification verdict for an action.
115+
||| Reuses the ABI `Result` type from Types.idr for the FFI boundary:
116+
||| `Ok` == certified permitted, `ConstraintViolation` == refused.
117+
public export
118+
certifyPermitted : (a : Action) -> Result
119+
certifyPermitted a = case decActionPermitted a of
120+
Yes _ => Ok
121+
No _ => ConstraintViolation
122+
123+
||| SOUNDNESS of the certifier: if it returns `Ok`, the action really is
124+
||| permitted. The proof inspects the same `Dec` the certifier used.
125+
public export
126+
certifyPermittedSound : (a : Action) -> certifyPermitted a = Ok -> ActionPermitted a
127+
certifyPermittedSound a prf with (decActionPermitted a)
128+
certifyPermittedSound a prf | Yes w = w
129+
certifyPermittedSound a Refl | No _ impossible
130+
131+
--------------------------------------------------------------------------------
132+
-- Concrete sample actions.
133+
--------------------------------------------------------------------------------
134+
135+
||| A benign informational action the policy allows.
136+
public export
137+
safeInform : Action
138+
safeInform = Inform Allow
139+
140+
||| A harmful deployment action the policy forbids (critical physical harm).
141+
public export
142+
forbiddenDeploy : Action
143+
forbiddenDeploy = DeployHarm Physical Critical Deny
144+
145+
--------------------------------------------------------------------------------
146+
-- POSITIVE control: an explicit, inhabited permission witness.
147+
--------------------------------------------------------------------------------
148+
149+
||| The allowed action genuinely carries a permission witness.
150+
public export
151+
safeInformPermitted : ActionPermitted Semantics.safeInform
152+
safeInformPermitted = PermitAllow Refl
153+
154+
--------------------------------------------------------------------------------
155+
-- NEGATIVE control (the core safety theorem): a forbidden action can NEVER
156+
-- be certified permitted.
157+
--------------------------------------------------------------------------------
158+
159+
||| SAFETY: there is no permission witness for the forbidden action.
160+
||| `verdictOf forbiddenDeploy = Deny`, so any `PermitAllow prf` would give
161+
||| `Deny = Allow`, which is absurd. Machine-checked.
162+
public export
163+
forbiddenNeverPermitted : Not (ActionPermitted Semantics.forbiddenDeploy)
164+
forbiddenNeverPermitted (PermitAllow prf) = absurd prf
165+
166+
||| Corollary at the certifier level: the forbidden action is never `Ok`.
167+
||| If it were, soundness would hand us a witness the safety theorem refutes.
168+
public export
169+
forbiddenNeverCertifiedOk : Not (certifyPermitted Semantics.forbiddenDeploy = Ok)
170+
forbiddenNeverCertifiedOk prf =
171+
forbiddenNeverPermitted (certifyPermittedSound Semantics.forbiddenDeploy prf)

‎src/interface/abi/phronesiser-abi.ipkg‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,3 +9,4 @@ modules = Phronesiser.ABI.Types
99
, Phronesiser.ABI.Layout
1010
, Phronesiser.ABI.Foreign
1111
, Phronesiser.ABI.Proofs
12+
, Phronesiser.ABI.Semantics

0 commit comments

Comments
 (0)