Skip to content

Commit a088b15

Browse files
claudehyperpolymath
claude
authored and
hyperpolymath
committed
proof(lean4): mechanize Ethical Verdict Consistency (policy arbitration)
Formalize the previously-informal "priority-ordered first match" policy arbitration (lib/phronesis/state.ex policies_by_priority + the first-match evaluation in spec/SPEC.core.scm) as the ethics-specific soundness of the decision procedure, over the real PhrPolicy record. Model: bestMatch = the highest-priority MATCHING policy, ties broken in favour of the earlier policy (a fold equivalent to sort-by-priority then find-first). `matches` abstracts condition evaluation, decoupling arbitration soundness from the Eval expression semantics. Theorems (all sorry-free; #print axioms reports only Lean's standard propext / Quot.sound): * bestMatch_sound -- a verdict is produced only by a policy that really matches the situation and is in the policy set (no spurious verdicts); * bestMatch_none -- no verdict ⇒ no policy matched; hence * bestMatch_decisive -- a verdict is produced whenever some policy applies (the procedure never silently abstains on a live case); * bestMatch_maximal -- the deciding policy has MAXIMAL priority among all matching policies, so a higher-priority verdict is never overridden by a lower-priority one -- e.g. a high-priority REJECT cannot be undercut by a lower-priority ACCEPT (the core ethical override). Builds clean on Lean 4.12.0 core, no Mathlib, no warnings. Docs: safety_proofs.md gains §2.6 "Ethical Verdict Consistency" with the mechanization note, and the §5 status table adds the row "Ethical Verdict Consistency | Mechanized (Lean 4)". https://claude.ai/code/session_01DQACj3RFmAPZaBPgR9SAaS
1 parent e7032f4 commit a088b15

2 files changed

Lines changed: 162 additions & 0 deletions

File tree

‎academic/formal-verification/lean4/Phronesis.lean‎

Lines changed: 136 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -618,6 +618,136 @@ theorem no_escalation :
618618
· intro x hx; exact hx
619619
· intro x hx; exact (List.mem_filter.mp hx).1
620620

621+
/-! # 19b. Ethical Verdict Consistency (policy-arbitration soundness)
622+
623+
Phronesis resolves conflicting policies by *priority-ordered first match*
624+
(`lib/phronesis/state.ex` `policies_by_priority` + the first-match evaluation
625+
in `spec/SPEC.core.scm`). That arbitration was previously only informal. Here
626+
it is made a function `bestMatch` — the highest-priority *matching* policy,
627+
ties broken in favour of the earlier policy — and proved:
628+
629+
* `bestMatch_sound` — a verdict is produced only by a policy that really
630+
matches the situation and is in the policy set
631+
(no spurious verdicts);
632+
* `bestMatch_none` — if no verdict is produced, no policy matched; hence
633+
* `bestMatch_decisive` — whenever some policy applies, a verdict is produced;
634+
* `bestMatch_maximal` — the deciding policy has maximal priority among all
635+
matching policies, so a higher-priority verdict is
636+
never overridden by a lower-priority one (e.g. a
637+
high-priority REJECT cannot be undercut by a
638+
lower-priority ACCEPT — the core ethical override).
639+
640+
`matches` abstracts condition evaluation (does a policy apply at a situation),
641+
decoupling arbitration soundness from the expression semantics in `Eval`. -/
642+
643+
section Arbitration
644+
645+
variable {Situation : Type}
646+
647+
/-- Keep the higher-priority of a policy `p` and an optional incumbent. Ties
648+
(equal priority) go to `p` (the earlier policy in a left fold). -/
649+
def pickMax (p : PhrPolicy) : Option PhrPolicy → PhrPolicy
650+
| none => p
651+
| some q => if q.priority ≤ p.priority then p else q
652+
653+
/-- Priority-ordered first-match arbitration as a fold: the highest-priority
654+
matching policy, ties resolved in favour of the earlier policy. -/
655+
def bestMatch (m : PhrPolicy → Situation → Bool) :
656+
List PhrPolicy → Situation → Option PhrPolicy
657+
| [], _ => none
658+
| p :: ps, s =>
659+
match m p s with
660+
| true => some (pickMax p (bestMatch m ps s))
661+
| false => bestMatch m ps s
662+
663+
/-- **Soundness.** A verdict is produced only by a policy that genuinely matches
664+
the situation and belongs to the policy set — no spurious verdicts. -/
665+
theorem bestMatch_sound (m : PhrPolicy → Situation → Bool) :
666+
∀ ps s r, bestMatch m ps s = some r → m r s = true ∧ r ∈ ps := by
667+
intro ps
668+
induction ps with
669+
| nil => intro s r h; simp [bestMatch] at h
670+
| cons p ps ih =>
671+
intro s r h
672+
simp only [bestMatch] at h
673+
split at h
674+
· case _ hp =>
675+
cases hb : bestMatch m ps s with
676+
| none => rw [hb] at h; simp only [pickMax] at h; injection h with h; subst h
677+
exact ⟨hp, List.mem_cons_self _ _⟩
678+
| some q =>
679+
rw [hb] at h; simp only [pickMax] at h; injection h with h
680+
by_cases hpr : q.priority ≤ p.priority
681+
· rw [if_pos hpr] at h; subst h; exact ⟨hp, List.mem_cons_self _ _⟩
682+
· rw [if_neg hpr] at h; subst h
683+
exact ⟨(ih s q hb).1, List.mem_cons_of_mem _ (ih s q hb).2⟩
684+
· case _ _hp =>
685+
exact ⟨(ih s r h).1, List.mem_cons_of_mem _ (ih s r h).2⟩
686+
687+
/-- If no verdict is produced, no policy in the set matched. -/
688+
theorem bestMatch_none (m : PhrPolicy → Situation → Bool) :
689+
∀ ps s, bestMatch m ps s = none → ∀ q ∈ ps, m q s = false := by
690+
intro ps
691+
induction ps with
692+
| nil => intro s _ q hq; cases hq
693+
| cons p ps ih =>
694+
intro s hnone q hq
695+
simp only [bestMatch] at hnone
696+
split at hnone
697+
· case _ _hp => exact absurd hnone (by simp)
698+
· case _ hp =>
699+
cases hq with
700+
| head => exact Bool.not_eq_true _ |>.mp (by simp [hp])
701+
| tail _ hq' => exact ih s hnone q hq'
702+
703+
/-- **Decisiveness.** Whenever some policy in the set applies, a verdict is
704+
produced (the decision procedure never silently abstains on a live case). -/
705+
theorem bestMatch_decisive (m : PhrPolicy → Situation → Bool) :
706+
∀ ps s q, q ∈ ps → m q s = true → ∃ r, bestMatch m ps s = some r := by
707+
intro ps s q hq hm
708+
cases hb : bestMatch m ps s with
709+
| some r => exact ⟨r, rfl⟩
710+
| none => exact absurd hm (by rw [bestMatch_none m ps s hb q hq]; simp)
711+
712+
/-- **Priority-maximal override.** The deciding policy has maximal priority among
713+
all matching policies: no matching policy outranks the verdict. Hence a
714+
higher-priority verdict (e.g. a REJECT) is never overridden by a
715+
lower-priority one (e.g. an ACCEPT). -/
716+
theorem bestMatch_maximal (m : PhrPolicy → Situation → Bool) :
717+
∀ ps s r, bestMatch m ps s = some r →
718+
∀ q ∈ ps, m q s = true → q.priority ≤ r.priority := by
719+
intro ps
720+
induction ps with
721+
| nil => intro s r h; simp [bestMatch] at h
722+
| cons p ps ih =>
723+
intro s r h q hq hqm
724+
simp only [bestMatch] at h
725+
split at h
726+
· case _ _hp =>
727+
cases hb : bestMatch m ps s with
728+
| none =>
729+
rw [hb] at h; simp only [pickMax] at h; injection h with h; subst h
730+
cases hq with
731+
| head => exact Int.le_refl _
732+
| tail _ hq' => exact absurd hqm (by rw [bestMatch_none m ps s hb q hq']; simp)
733+
| some t =>
734+
rw [hb] at h; simp only [pickMax] at h; injection h with h
735+
by_cases hpr : t.priority ≤ p.priority
736+
· rw [if_pos hpr] at h; subst h
737+
cases hq with
738+
| head => exact Int.le_refl _
739+
| tail _ hq' => exact Int.le_trans (ih s t hb q hq' hqm) hpr
740+
· rw [if_neg hpr] at h; subst h
741+
cases hq with
742+
| head => omega
743+
| tail _ hq' => exact ih s t hb q hq' hqm
744+
· case _ hp =>
745+
cases hq with
746+
| head => simp [hp] at hqm
747+
| tail _ hq' => exact ih s r h q hq' hqm
748+
749+
end Arbitration
750+
621751
/-! # 20. Summary
622752
623753
Main theorems (all machine-checked on Lean 4 core; no `sorry`, only Lean's
@@ -632,6 +762,12 @@ theorem no_escalation :
632762
7. capability_soundness_ite — enforcement is preserved through conditionals
633763
8. least_privilege — a fresh context holds only granted capabilities
634764
9. no_escalation — a step never enlarges the capability set
765+
10. bestMatch_sound — policy arbitration yields no spurious verdict
766+
11. bestMatch_none — no verdict ⇒ no policy matched
767+
12. bestMatch_decisive — a verdict is produced whenever a policy applies
768+
13. bestMatch_maximal — the deciding policy has maximal priority among
769+
matches (higher-priority override; a high-priority
770+
REJECT is never undercut by a lower ACCEPT)
635771
Mirrors ../coq/Phronesis.v (preservation, eval_deterministic, totality).
636772
-/
637773

‎docs/safety_proofs.md‎

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -264,6 +264,31 @@ A policy cannot acquire capabilities it wasn't granted:
264264
This holds because capabilities are only set at context creation
265265
and never modified during execution. ∎
266266

267+
### 2.6 Ethical Verdict Consistency
268+
269+
**Theorem (Policy-Arbitration Soundness):**
270+
Phronesis resolves conflicting policies by *priority-ordered first match*
271+
(`lib/phronesis/state.ex` `policies_by_priority` + the first-match evaluation in
272+
`spec/SPEC.core.scm`). The decision procedure is sound, decisive, and respects
273+
priority:
274+
275+
1. **Soundness** — a verdict is produced only by a policy that genuinely matches
276+
the situation and is in the policy set (no spurious verdicts).
277+
2. **Decisiveness** — whenever some policy applies, a verdict is produced.
278+
3. **Priority-maximal override** — the deciding policy has maximal priority among
279+
all matching policies; hence a higher-priority verdict is never overridden by
280+
a lower-priority one (e.g. a high-priority `REJECT` cannot be undercut by a
281+
lower-priority `ACCEPT` — the core ethical override). ∎
282+
283+
**Mechanized (Lean 4):** Machine-checked in
284+
[`../academic/formal-verification/lean4/Phronesis.lean`](../academic/formal-verification/lean4/Phronesis.lean)
285+
as `bestMatch_sound`, `bestMatch_none`, `bestMatch_decisive`, and
286+
`bestMatch_maximal` over the real `PhrPolicy` record. Arbitration is modelled as
287+
the `bestMatch` fold (highest-priority matching policy, ties to the earlier
288+
policy); `matches` abstracts condition evaluation, decoupling arbitration
289+
soundness from the expression semantics. All four are `sorry`-free (only Lean's
290+
standard `propext`/`Quot.sound`; confirm with `#print axioms`).
291+
267292
---
268293

269294
## 3. Byzantine Fault Tolerance
@@ -411,6 +436,7 @@ Layer 5: Audit Log
411436
|----------|--------|--------------|
412437
| Sandbox Isolation | Mechanized (Lean 4) | `academic/formal-verification/lean4/Phronesis.lean` |
413438
| Capability Soundness | Mechanized (Lean 4) | `academic/formal-verification/lean4/Phronesis.lean` |
439+
| Ethical Verdict Consistency | Mechanized (Lean 4) | `academic/formal-verification/lean4/Phronesis.lean` |
414440
| BFT Safety | Model-checked (TLA+/TLC) | `formal/PhronesisConsensus.tla` |
415441
| BFT Liveness | Manual proof | This document |
416442
| Termination | Proven | Semantics doc |

0 commit comments

Comments
 (0)