Skip to content

Commit 2448a98

Browse files
claudeclaude
committed
Add Layer-3 ABI invariants: monotone safety under policy composition
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 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx
1 parent 6a7e723 commit 2448a98

2 files changed

Lines changed: 305 additions & 0 deletions

File tree

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

Lines changed: 304 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,304 @@
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+
||| Layer-3 invariants for Phronesiser: MONOTONE SAFETY under policy
5+
||| composition — a strictly deeper property than the Layer-2 flagship.
6+
|||
7+
||| Layer 2 (`Phronesiser.ABI.Semantics`) proves a property of ONE action under
8+
||| ONE fixed static verdict: a forbidden action can never be certified
9+
||| permitted. This module proves properties of WHOLE POLICIES and their
10+
||| composition — quantified over all actions and over the space of policies:
11+
|||
12+
||| 1. DOWNWARD-CLOSURE OF PERMISSION (monotone safety): if a policy `p2`
13+
||| *tightens* `p1` (everything `p2` permits, `p1` already permitted),
14+
||| then everything `p1` forbids, `p2` still forbids. Adding constraints
15+
||| NEVER re-permits a previously-forbidden action — the permitted set
16+
||| only shrinks. This is the safety-preservation law an ethical engine
17+
||| must satisfy when policies are strengthened at runtime.
18+
|||
19+
||| 2. CONJUNCTION COMPOSITION: an action permitted under the conjunction
20+
||| `andPolicy p1 p2` is permitted under `p1` AND under `p2` separately;
21+
||| and `andPolicy p1 p2` provably tightens each conjunct. So composing
22+
||| policies by conjunction is sound: it can only forbid more.
23+
|||
24+
||| Both are reused over the SAME model from `Semantics` (Action / Verdict /
25+
||| verdictOf) — no datatype is redefined. A sound+complete `Dec (Permits ...)`
26+
||| is provided. Positive and negative/non-vacuity controls are machine-checked.
27+
|||
28+
||| Every fact below is discharged by the Idris2 type checker. No `believe_me`,
29+
||| `idris_crash`, `assert_total`, `postulate`, `sorry`, or asserted equalities.
30+
31+
module Phronesiser.ABI.Invariants
32+
33+
import Phronesiser.ABI.Types
34+
import Phronesiser.ABI.Semantics
35+
36+
%default total
37+
38+
--------------------------------------------------------------------------------
39+
-- Verdict trichotomy (here, dichotomy): Allow or Deny, nothing else.
40+
--------------------------------------------------------------------------------
41+
42+
||| Every verdict is `Allow` or `Deny`. This total case analysis is the engine
43+
||| behind monotone safety: "not Allow" forces "Deny".
44+
public export
45+
verdictDichotomy : (v : Verdict) -> Either (v = Allow) (v = Deny)
46+
verdictDichotomy Allow = Left Refl
47+
verdictDichotomy Deny = Right Refl
48+
49+
--------------------------------------------------------------------------------
50+
-- Policies as verdict-assignments over the shared Action model.
51+
--------------------------------------------------------------------------------
52+
53+
||| A policy assigns a verdict to every candidate action. This refines the
54+
||| static `verdictOf` from `Semantics`: different ethical rule-sets induce
55+
||| different policies over the same action space.
56+
public export
57+
Policy : Type
58+
Policy = Action -> Verdict
59+
60+
||| `Permits p a` : the policy `p` permits action `a`.
61+
public export
62+
Permits : Policy -> Action -> Type
63+
Permits p a = p a = Allow
64+
65+
||| `Forbids p a` : the policy `p` forbids action `a`.
66+
public export
67+
Forbids : Policy -> Action -> Type
68+
Forbids p a = p a = Deny
69+
70+
||| A policy cannot both permit and forbid the same action (Allow /= Deny).
71+
||| This is the local consistency of any single policy.
72+
public export
73+
permitForbidExclusive : (p : Policy) -> (a : Action) ->
74+
Permits p a -> Forbids p a -> Void
75+
permitForbidExclusive p a perm forb =
76+
-- perm : p a = Allow ; forb : p a = Deny ; so Allow = Deny, absurd.
77+
absurd (trans (sym perm) forb)
78+
79+
--------------------------------------------------------------------------------
80+
-- Policy tightening (the ordering on policies).
81+
--------------------------------------------------------------------------------
82+
83+
||| `Tightens p2 p1` : `p2` is at least as strict as `p1` — every action `p2`
84+
||| permits was already permitted by `p1`. Equivalently the permitted set of
85+
||| `p2` is contained in that of `p1`.
86+
public export
87+
Tightens : Policy -> Policy -> Type
88+
Tightens p2 p1 = (a : Action) -> Permits p2 a -> Permits p1 a
89+
90+
||| Tightening is reflexive: a policy is at least as strict as itself.
91+
public export
92+
tightensRefl : (p : Policy) -> Tightens p p
93+
tightensRefl p = \a, perm => perm
94+
95+
||| Tightening is transitive: it is a genuine preorder on policies.
96+
public export
97+
tightensTrans : {p1, p2, p3 : Policy} ->
98+
Tightens p3 p2 -> Tightens p2 p1 -> Tightens p3 p1
99+
tightensTrans t32 t21 = \a, perm => t21 a (t32 a perm)
100+
101+
--------------------------------------------------------------------------------
102+
-- THEOREM 1: Monotone safety — the forbidden set only grows under tightening.
103+
--------------------------------------------------------------------------------
104+
105+
||| MONOTONE SAFETY (downward-closure of permission, in forbidden form):
106+
||| if `p2` tightens `p1`, then anything `p1` forbids is still forbidden by
107+
||| `p2`. Tightening a policy never re-permits a previously-forbidden action.
108+
|||
109+
||| Proof: suppose `p1` forbids `a` but `p2` does NOT forbid it. By dichotomy
110+
||| `p2 a = Allow`, i.e. `p2` permits `a`; tightening then gives `p1` permits
111+
||| `a`, contradicting `p1` forbids `a`. So `p2 a = Deny`.
112+
public export
113+
tighteningPreservesForbidden : {p1, p2 : Policy} -> {a : Action} ->
114+
Tightens p2 p1 -> Forbids p1 a -> Forbids p2 a
115+
tighteningPreservesForbidden t forb1 =
116+
case verdictDichotomy (p2 a) of
117+
Right denyEq => denyEq
118+
Left allowEq =>
119+
-- allowEq : p2 a = Allow = Permits p2 a ; t a allowEq : Permits p1 a
120+
-- forb1 : p1 a = Deny ; contradiction.
121+
absurd (permitForbidExclusive p1 a (t a allowEq) forb1)
122+
123+
||| Equivalent CONTRAPOSITIVE phrasing kept for the API surface: under
124+
||| tightening, if `p2` permits an action then `p1` permitted it (this is just
125+
||| the definition of `Tightens`, restated as a named law).
126+
public export
127+
tighteningShrinksPermitted : {p1, p2 : Policy} -> {a : Action} ->
128+
Tightens p2 p1 -> Permits p2 a -> Permits p1 a
129+
tighteningShrinksPermitted t perm2 = t a perm2
130+
131+
--------------------------------------------------------------------------------
132+
-- Conjunction of policies.
133+
--------------------------------------------------------------------------------
134+
135+
||| Conjoin two policies: the result permits an action only when BOTH permit it,
136+
||| and forbids it otherwise. This is how an ethical engine layers an extra
137+
||| constraint set on top of an existing one.
138+
public export
139+
andPolicy : Policy -> Policy -> Policy
140+
andPolicy p1 p2 a =
141+
case p1 a of
142+
Allow => p2 a
143+
Deny => Deny
144+
145+
--------------------------------------------------------------------------------
146+
-- THEOREM 2: Conjunction composition is sound.
147+
--------------------------------------------------------------------------------
148+
149+
||| If the conjunction permits an action, then the FIRST conjunct permits it.
150+
||| Proof by case on `p1 a`: if it were `Deny`, the conjunction would be `Deny`,
151+
||| contradicting the `= Allow` hypothesis.
152+
public export
153+
andPermitsLeft : (p1, p2 : Policy) -> (a : Action) ->
154+
Permits (andPolicy p1 p2) a -> Permits p1 a
155+
andPermitsLeft p1 p2 a perm with (p1 a) proof eqp1
156+
andPermitsLeft p1 p2 a perm | Allow = Refl
157+
andPermitsLeft p1 p2 a perm | Deny =
158+
-- with p1 a = Deny, andPolicy reduces to Deny, so perm : Deny = Allow.
159+
absurd perm
160+
161+
||| If the conjunction permits an action, then the SECOND conjunct permits it.
162+
||| When `p1 a = Allow`, `andPolicy p1 p2 a` reduces to `p2 a`, so the
163+
||| hypothesis IS `p2 a = Allow`.
164+
public export
165+
andPermitsRight : (p1, p2 : Policy) -> (a : Action) ->
166+
Permits (andPolicy p1 p2) a -> Permits p2 a
167+
andPermitsRight p1 p2 a perm with (p1 a) proof eqp1
168+
andPermitsRight p1 p2 a perm | Allow = perm
169+
andPermitsRight p1 p2 a perm | Deny = absurd perm
170+
171+
||| Full composition soundness: conjunction-permission gives BOTH permissions.
172+
public export
173+
andPermitsBoth : (p1, p2 : Policy) -> (a : Action) ->
174+
Permits (andPolicy p1 p2) a -> (Permits p1 a, Permits p2 a)
175+
andPermitsBoth p1 p2 a perm =
176+
(andPermitsLeft p1 p2 a perm, andPermitsRight p1 p2 a perm)
177+
178+
||| Conversely, if both conjuncts permit, the conjunction permits.
179+
||| Together with `andPermitsBoth` this is an iff: conjunction-permission is
180+
||| exactly the pairwise conjunction of permissions.
181+
public export
182+
bothPermitsAnd : (p1, p2 : Policy) -> (a : Action) ->
183+
Permits p1 a -> Permits p2 a -> Permits (andPolicy p1 p2) a
184+
bothPermitsAnd p1 p2 a perm1 perm2 with (p1 a) proof eqp1
185+
bothPermitsAnd p1 p2 a perm1 perm2 | Allow = perm2
186+
bothPermitsAnd p1 p2 a perm1 perm2 | Deny =
187+
-- with p1 a = Deny, perm1 : Deny = Allow is absurd.
188+
absurd perm1
189+
190+
||| Conjunction tightens its first conjunct: `andPolicy p1 p2` is at least as
191+
||| strict as `p1`. (Hence, by Theorem 1, it can only forbid more than `p1`.)
192+
public export
193+
andTightensLeft : (p1, p2 : Policy) -> Tightens (andPolicy p1 p2) p1
194+
andTightensLeft p1 p2 = \a, perm => andPermitsLeft p1 p2 a perm
195+
196+
||| Conjunction tightens its second conjunct too.
197+
public export
198+
andTightensRight : (p1, p2 : Policy) -> Tightens (andPolicy p1 p2) p2
199+
andTightensRight p1 p2 = \a, perm => andPermitsRight p1 p2 a perm
200+
201+
--------------------------------------------------------------------------------
202+
-- Sound + complete decision procedure for permission under a policy.
203+
--------------------------------------------------------------------------------
204+
205+
||| Decide whether a policy permits an action. SOUND: a `Yes` carries a real
206+
||| `Permits` proof. COMPLETE: a `No` carries a real refutation.
207+
public export
208+
decPermits : (p : Policy) -> (a : Action) -> Dec (Permits p a)
209+
decPermits p a with (p a) proof eq
210+
decPermits p a | Allow = Yes Refl
211+
decPermits p a | Deny =
212+
No (\perm => absurd perm)
213+
214+
--------------------------------------------------------------------------------
215+
-- Sample policies built over the SHARED model.
216+
--------------------------------------------------------------------------------
217+
218+
||| The static base policy: read the verdict already attached to the action.
219+
public export
220+
basePolicy : Policy
221+
basePolicy = verdictOf
222+
223+
||| A strictly stronger policy that additionally forbids EVERY `DeployHarm`
224+
||| action regardless of its attached verdict (e.g. a freshly added "no harm
225+
||| deployment, ever" constraint). On non-DeployHarm actions it agrees with
226+
||| the base policy.
227+
public export
228+
noHarmDeployPolicy : Policy
229+
noHarmDeployPolicy (DeployHarm _ _ _) = Deny
230+
noHarmDeployPolicy a = verdictOf a
231+
232+
--------------------------------------------------------------------------------
233+
-- POSITIVE controls.
234+
--------------------------------------------------------------------------------
235+
236+
||| The base policy permits the benign informational action from `Semantics`.
237+
public export
238+
basePermitsSafeInform : Permits Invariants.basePolicy Semantics.safeInform
239+
basePermitsSafeInform = Refl
240+
241+
||| `noHarmDeployPolicy` genuinely tightens the base policy (machine-checked,
242+
||| quantified over all actions). This is a positive instance of Theorem 1's
243+
||| hypothesis.
244+
public export
245+
noHarmTightensBase : Tightens Invariants.noHarmDeployPolicy Invariants.basePolicy
246+
noHarmTightensBase (Inform v) perm = perm
247+
noHarmTightensBase (Query v) perm = perm
248+
noHarmTightensBase (DeployHarm d s v) perm = absurd perm
249+
-- For DeployHarm, noHarmDeployPolicy = Deny, so perm : Deny = Allow is absurd.
250+
251+
||| Live application of Theorem 1: because `noHarmDeployPolicy` tightens the
252+
||| base policy and the base policy forbids `forbiddenDeploy`, the tightened
253+
||| policy still forbids it. (Both base and tightened forbid here; the point is
254+
||| that monotone safety is witnessed on a concrete pair.)
255+
public export
256+
forbiddenStaysForbidden :
257+
Forbids Invariants.noHarmDeployPolicy Semantics.forbiddenDeploy
258+
forbiddenStaysForbidden =
259+
tighteningPreservesForbidden
260+
{p1 = basePolicy} {p2 = noHarmDeployPolicy} {a = forbiddenDeploy}
261+
noHarmTightensBase Refl
262+
263+
||| Composition positive control: under `andPolicy basePolicy basePolicy`,
264+
||| the benign action is permitted, and decomposes to both conjuncts.
265+
public export
266+
andPermitsSafeInform :
267+
( Permits Invariants.basePolicy Semantics.safeInform
268+
, Permits Invariants.basePolicy Semantics.safeInform )
269+
andPermitsSafeInform =
270+
andPermitsBoth basePolicy basePolicy safeInform Refl
271+
272+
--------------------------------------------------------------------------------
273+
-- NEGATIVE / non-vacuity controls.
274+
--------------------------------------------------------------------------------
275+
276+
||| Non-vacuity of monotone safety: the tightened policy does NOT permit the
277+
||| forbidden action. Any such permission would, with `forbiddenStaysForbidden`,
278+
||| give `Deny = Allow`. Machine-checked `Not (...)`.
279+
public export
280+
tightenedRefusesForbidden :
281+
Not (Permits Invariants.noHarmDeployPolicy Semantics.forbiddenDeploy)
282+
tightenedRefusesForbidden perm =
283+
absurd (trans (sym perm) forbiddenStaysForbidden)
284+
285+
||| Non-vacuity of composition: the conjunction of the base policy with the
286+
||| all-DeployHarm-denying policy does NOT permit `forbiddenDeploy`. If it did,
287+
||| `andPermitsRight` would extract a `noHarmDeployPolicy` permission, which
288+
||| `tightenedRefusesForbidden` refutes.
289+
public export
290+
andRefusesForbidden :
291+
Not (Permits (andPolicy Invariants.basePolicy Invariants.noHarmDeployPolicy)
292+
Semantics.forbiddenDeploy)
293+
andRefusesForbidden perm =
294+
tightenedRefusesForbidden
295+
(andPermitsRight basePolicy noHarmDeployPolicy forbiddenDeploy perm)
296+
297+
||| A policy can NEVER both permit and forbid the same action — restated as a
298+
||| concrete refutation that `basePolicy` simultaneously permits and forbids
299+
||| the benign action (it permits it, so "forbids" is impossible).
300+
public export
301+
baseNotForbidsSafeInform :
302+
Not (Forbids Invariants.basePolicy Semantics.safeInform)
303+
baseNotForbidsSafeInform forb =
304+
permitForbidExclusive basePolicy safeInform basePermitsSafeInform forb

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,3 +10,4 @@ modules = Phronesiser.ABI.Types
1010
, Phronesiser.ABI.Foreign
1111
, Phronesiser.ABI.Proofs
1212
, Phronesiser.ABI.Semantics
13+
, Phronesiser.ABI.Invariants

0 commit comments

Comments
 (0)