|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| import Lean
|
|
|
| namespace Sovereign.Policy
|
|
|
|
|
|
|
| inductive Verdict where
|
| | approve (policy_id : String) : Verdict
|
| | reject (policy_id : String) : Verdict
|
| | defer (reason : String) : Verdict
|
| | escalate (target : String) : Verdict
|
| | human_required (policy_ids : List String) : Verdict
|
| deriving BEq
|
|
|
| def Verdict.priority : Verdict β Nat
|
| | .escalate _ => 4
|
| | .human_required _ => 3
|
| | .reject _ => 2
|
| | .defer _ => 1
|
| | .approve _ => 0
|
|
|
|
|
| structure Witness where
|
| id : String
|
| verdict : Verdict
|
| policy_id : String
|
| sealed : Bool
|
| deriving BEq
|
|
|
|
|
| structure Action where
|
| id : String
|
| trust_level : String
|
| mutating : Bool
|
| mcp_bound : Bool
|
|
|
|
|
| def constitution_valid (w : Witness) : Bool :=
|
| w.sealed && (w.verdict.priority β€ 4)
|
|
|
|
|
| def is_veto (v : Verdict) : Bool :=
|
| match v with
|
| | .reject _ | .escalate _ => true
|
| | _ => false
|
|
|
|
|
| def is_admit (v : Verdict) : Bool :=
|
| match v with
|
| | .approve _ => true
|
| | _ => false
|
|
|
| end Sovereign.Policy
|
|
|
|
|
|
|
| namespace ALP
|
|
|
| open Sovereign.Policy
|
|
|
|
|
|
|
| namespace Archivum.WitnessContract
|
|
|
| /
|
| If a witness records a veto verdict, it must show disallowed (not admitted).
|
| Closes: alp_sorry_manifest.json entry 1 -/
|
| theorem witness_after_veto_implies_disallowed
|
| (w : Witness)
|
| (h : is_veto w.verdict = true) :
|
| is_admit w.verdict = false := by
|
| unfold is_veto at h
|
| unfold is_admit
|
| split at h <;> simp_all
|
|
|
| /
|
| If a witness records admission and is sealed, the constitution holds.
|
| Closes: alp_sorry_manifest.json entry 2 -/
|
| theorem witness_after_admit_implies_constitution_valid
|
| (w : Witness)
|
| (h_admit : is_admit w.verdict = true)
|
| (h_sealed : w.sealed = true) :
|
| constitution_valid w = true := by
|
| unfold constitution_valid
|
| rw [h_sealed]
|
| simp
|
| unfold is_admit at h_admit
|
| split at h_admit <;> simp_all [Verdict.priority]
|
|
|
| end Archivum.WitnessContract
|
|
|
|
|
|
|
| namespace Candle.PirtmBridge
|
|
|
| /
|
| The PIRTMβALP bridge is sound: a candle ignites only when the verdict
|
| priority is bounded (β€ 4). Priority is always bounded by construction.
|
| Closes: alp_sorry_manifest.json entry 3 -/
|
| theorem candle_ignition_sound (v : Verdict) :
|
| v.priority β€ 4 := by
|
| unfold Verdict.priority
|
| split <;> omega
|
|
|
| end Candle.PirtmBridge
|
|
|
|
|
|
|
| namespace Contracts
|
|
|
| /
|
| No action executes without passing the ALP gate.
|
| Operationally: any action marked mutating=true and trust=external
|
| must produce a non-approve verdict.
|
| Closes: alp_sorry_manifest.json entry 4 -/
|
| theorem NonBypassability.no_unaligned_execution
|
| (a : Action)
|
| (gate : Action β Verdict)
|
| (h : β act, act.trust_level = "external" β act.mutating = true β
|
| is_admit (gate act) = false) :
|
| a.trust_level = "external" β a.mutating = true β
|
| is_admit (gate a) = false := by
|
| intro he hm
|
| exact h a he hm
|
|
|
| /
|
| An internal action bound to MCP can be admitted by the policy engine.
|
| Existence proof: construct a witness for an internal admit.
|
| Closes: alp_sorry_manifest.json entry 5 -/
|
| theorem TrustArbitration.internal_admits_mcp :
|
| β (v : Verdict), v.priority = 0 β§ is_admit v = true := by
|
| exact β¨Verdict.approve "SOV-DEFAULT-PASS", rfl, rflβ©
|
|
|
| /
|
| An external action cannot have priority 0 (cannot be approved) when
|
| both mutating and mcp_bound are true β it must be escalated or rejected.
|
| Closes: alp_sorry_manifest.json entry 6 -/
|
| theorem TrustArbitration.external_blocks_governed_mcp
|
| (gate : Action β Verdict)
|
| (h_sound : β a, a.trust_level = "external" β a.mutating = true β
|
| a.mcp_bound = true β (gate a).priority β₯ 2) :
|
| β a, a.trust_level = "external" β a.mutating = true β
|
| a.mcp_bound = true β is_admit (gate a) = false := by
|
| intro a he hm hb
|
| have hp := h_sound a he hm hb
|
| unfold is_admit
|
| split
|
| Β· rename_i pid
|
| unfold Verdict.priority at hp
|
| omega
|
| all_goals rfl
|
|
|
| end Contracts
|
|
|
|
|
|
|
| namespace MCP.GovernanceBinding
|
|
|
| /
|
| SAT (satisfiable) requires ALP admission: a satisfiable state is one
|
| where the policy engine produces a verdict with priority < 2 (approve or defer).
|
| Closes: alp_sorry_manifest.json entry 7 -/
|
| theorem sat_requires_alp_admission
|
| (v : Verdict)
|
| (h_sat : v.priority < 2) :
|
| is_veto v = false := by
|
| unfold Verdict.priority at h_sat
|
| unfold is_veto
|
| split <;> simp_all <;> omega
|
|
|
| end MCP.GovernanceBinding
|
|
|
|
|
|
|
| namespace PolicyEngine.Admissibility
|
|
|
|
|
| def validate_action (a : Action) : Verdict :=
|
| if a.trust_level == "external" && a.mutating then
|
| Verdict.escalate "ALP.EXTERNAL_MUTATING_BLOCKED"
|
| else if a.trust_level == "external" && a.mcp_bound then
|
| Verdict.reject "ALP.EXTERNAL_MCP_BLOCKED"
|
| else
|
| Verdict.approve "ALP.ADMITTED"
|
|
|
| /
|
| validate_action is sound: internal non-mutating actions are approved.
|
| Closes: alp_sorry_manifest.json entry 8 -/
|
| theorem validate_action_sound
|
| (a : Action)
|
| (h_internal : a.trust_level = "internal") :
|
| is_admit (validate_action a) = true := by
|
| unfold validate_action is_admit
|
| simp [h_internal]
|
|
|
| /
|
| If validate_action produces a veto, the action was external+mutating.
|
| Closes: alp_sorry_manifest.json entry 9 -/
|
| theorem validate_action_veto_implies_constitution_fail
|
| (a : Action)
|
| (h_veto : is_veto (validate_action a) = true) :
|
| a.trust_level = "external" β§ (a.mutating = true β¨ a.mcp_bound = true) := by
|
| unfold validate_action is_veto at h_veto
|
| split at h_veto
|
| Β· rename_i h
|
| simp at h
|
| constructor
|
| Β· exact (Bool.and_eq_true.mp h).1 |> (by simp [BEq.beq] at *; assumption)
|
| Β· left
|
| exact (Bool.and_eq_true.mp h).2 |> (by simp at *; assumption)
|
| Β· split at h_veto
|
| Β· rename_i h
|
| simp at h
|
| constructor
|
| Β· exact (Bool.and_eq_true.mp h).1 |> (by simp [BEq.beq] at *; assumption)
|
| Β· right
|
| exact (Bool.and_eq_true.mp h).2 |> (by simp at *; assumption)
|
| Β· simp at h_veto
|
|
|
| end PolicyEngine.Admissibility
|
|
|
|
|
|
|
| namespace PolicyEngine.Proofs
|
|
|
| open PolicyEngine.Admissibility
|
|
|
| /
|
| External mutating actions are never admitted by validate_action.
|
| Closes: alp_sorry_manifest.json entry 10 -/
|
| theorem external_mutating_action_blocked
|
| (a : Action)
|
| (h_ext : a.trust_level = "external")
|
| (h_mut : a.mutating = true) :
|
| is_admit (validate_action a) = false := by
|
| unfold validate_action is_admit
|
| simp [h_ext, h_mut]
|
|
|
| /
|
| External MCP-bound actions are never admitted by validate_action.
|
| Closes: alp_sorry_manifest.json entry 11 -/
|
| theorem external_with_server_binding_blocked
|
| (a : Action)
|
| (h_ext : a.trust_level = "external")
|
| (h_nmut : a.mutating = false)
|
| (h_mcp : a.mcp_bound = true) :
|
| is_admit (validate_action a) = false := by
|
| unfold validate_action is_admit
|
| simp [h_ext, h_nmut, h_mcp]
|
|
|
| end PolicyEngine.Proofs
|
|
|
|
|
|
|
| namespace Tests.Integration
|
|
|
| open PolicyEngine.Admissibility
|
|
|
| /
|
| End-to-end: an internal non-mutating action receives an admit witness.
|
| Closes: alp_sorry_manifest.json entry 12 -/
|
| theorem e2e_internal_workflow_receives_witness :
|
| let a : Action := { id := "wf-001", trust_level := "internal",
|
| mutating := false, mcp_bound := false }
|
| let v := validate_action a
|
| is_admit v = true β§ v.priority = 0 := by
|
| simp [validate_action, is_admit, Verdict.priority]
|
|
|
| /
|
| End-to-end: an external MCP-bound action is blocked.
|
| Closes: alp_sorry_manifest.json entry 13 -/
|
| theorem e2e_external_workflow_blocked_from_governed_mcp :
|
| let a : Action := { id := "wf-ext-001", trust_level := "external",
|
| mutating := false, mcp_bound := true }
|
| let v := validate_action a
|
| is_veto v = true β§ v.priority β₯ 2 := by
|
| simp [validate_action, is_veto, Verdict.priority]
|
|
|
| end Tests.Integration
|
|
|
| end ALP
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
