lean/proofs/SovereignJudge.lean

-- SovereignJudge.lean
-- Canonical verdict algebra — single source of truth
-- Bridges: Lean4PolicyKernel/Policies/Core.lean + holy-agents/TheologyValidator.lean
--          + SnaklTalk Verdict (evidence/silence) + Prolog sovereign_kernel.pl

--
-- Architecture:
--   Verdict          — operational (5-case): approve|reject|defer|escalate|human_required

--   MoralVerdict     — theological (3-case): approve|reject|repent  [TheologyValidator]

--   MoralAction      — boolean action fields shared across layers

--   MoralVerdict.toVerdict — bridge: moral → operational

--   SnaklVerdict     — Smalltalk wire format bridge: evidence|silence

--

-- Cross-language map:

--   Lean4 Verdict.approve    ↔  Prolog approve  ↔  Smalltalk Verdict evidence:

--   Lean4 Verdict.reject     ↔  Prolog reject   ↔  Smalltalk Verdict silence:

--   Lean4 Verdict.escalate   ↔  Prolog escalate ↔  VortexAgent audit escalation

--   Haskell EREPass          ↔  Lean4 .approve  ↔  five-pass pipeline

--   Idris2 (1 qt : QuantumTemp) ↔ Lean4 WormSeal subtype ↔ Haskell %1

--

-- Ahmad Ali Parr · SnapKitty Collective · 2026

-- SEIT NGO — Sovereign Enochian Institute of Technology



namespace Sovereign.Judge



-- ── Type aliases ──────────────────────────────────────────────────────────────

abbrev PolicyId       := String

abbrev DID            := String

abbrev HashURI        := String

abbrev Role           := String

abbrev CorrelationId  := String



-- ── WORM seal: dependent subtype ─────────────────────────────────────────────

-- Mirrors SovereignMorphism.lean WormSeal and SnaklTalk Seal

-- The length constraint lives in the TYPE — no runtime check needed

def WormSeal := { s : String // s.length = 64 }



-- ── Evidence bundle ───────────────────────────────────────────────────────────

structure Evidence where

  refs       : List HashURI

  hashes     : List ByteArray

  signatures : List (DID × ByteArray)

  deriving Repr



-- ── Evaluation context ────────────────────────────────────────────────────────

structure EvalContext where

  correlation_id : CorrelationId

  actor          : DID

  task_type      : String

  evidence       : Evidence

  timestamp      : UInt64

  nonce          : ByteArray

  deriving Repr



-- ── Operational Verdict (5 cases) ────────────────────────────────────────────

-- Canonical verdict algebra for policy enforcement.

-- Matches Prolog sovereign_kernel.pl approve|reject|defer|escalate|human_required.

-- Priority (strict): escalate > human_required > reject > defer > approve.

-- A chain of policies is as strict as its strictest member.



inductive Verdict where

  | approve        (policy_id   : PolicyId)        : Verdict

  | reject         (policy_id   : PolicyId)        : Verdict

  | defer          (reason      : String)          : Verdict

  | escalate       (target      : Role)            : Verdict

  | human_required (policy_ids  : List PolicyId)  : Verdict

  deriving Repr, BEq



def Verdict.priority : Verdict → Nat

  | .escalate _       => 4

  | .human_required _ => 3

  | .reject _         => 2

  | .defer _          => 1

  | .approve _        => 0



def Verdict.combine : List Verdict → Verdict

  | []        => .approve "SOV-DEFAULT-PASS"

  | v :: rest =>

    rest.foldl (fun acc cur =>

      if cur.priority > acc.priority then

        match acc, cur with

        | .human_required ps, .human_required qs => .human_required (ps ++ qs)

        | _, _                                    => cur

      else

        match acc, cur with

        | .human_required ps, .human_required qs => .human_required (ps ++ qs)

        | _, _                                    => acc

    ) v



def Verdict.isFinal : Verdict → Bool

  | .approve _ | .reject _ => true

  | _                      => false



def Verdict.requiresHuman : Verdict → Bool

  | .human_required _ => true

  | _                 => false



def Verdict.toNatsSubject : Verdict → String

  | .approve _        => "sovereign.audit.bifrost.commit.v1"

  | .reject _         => "sovereign.audit.bifrost.commit.v1"

  | .defer _          => "sovereign.governance.decision.pending.v1"

  | .escalate _       => "sovereign.governance.decision.pending.v1"

  | .human_required _ => "sovereign.governance.decision.pending.v1"



-- ── Moral Verdict (3 cases) ───────────────────────────────────────────────────

-- Theological verdict for the holy-agents moral judgement layer.

-- Simpler than the operational Verdict — no policy IDs, no escalation targets.

-- Previously duplicated in TheologyValidator.lean; canonical here.



inductive MoralVerdict where

  | approve : MoralVerdict

  | reject  : MoralVerdict

  | repent  : MoralVerdict   -- unique to the moral layer: calls for correction

  deriving Repr, DecidableEq



-- ── Moral Action ──────────────────────────────────────────────────────────────

-- Shared across moral judgement and theological reasoning.

-- Seven boolean predicates form the lawfulness check.



structure MoralAction where

  truthful        : Bool

  harmful         : Bool

  exploitative    : Bool

  requiresConsent : Bool

  hasConsent      : Bool

  witnessed       : Bool

  cited           : Bool

  deriving Repr



-- ── Lawfulness predicate ──────────────────────────────────────────────────────

def lawful (a : MoralAction) : Bool :=

  a.truthful &&

  !a.harmful &&

  !a.exploitative &&

  (!a.requiresConsent || a.hasConsent) &&

  a.witnessed &&

  a.cited



-- ── Moral judge ───────────────────────────────────────────────────────────────

def judge (a : MoralAction) : MoralVerdict :=

  if lawful a then .approve else .repent



-- ── Bridge: MoralVerdict → Verdict ───────────────────────────────────────────

-- Converts the theological 3-case verdict to the operational 5-case verdict.

-- repent → escalate: the moral arbiter escalates for review, does not silently reject.

def MoralVerdict.toVerdict (policyId : PolicyId) : MoralVerdict → Verdict

  | .approve => .approve policyId

  | .reject  => .reject  policyId

  | .repent  => .escalate "moral_arbiter"



-- ── SnaklVerdict bridge ───────────────────────────────────────────────────────

-- Maps Smalltalk SnaklTalk Verdict (evidence/silence) to operational Verdict.

-- SnaklTalk: Verdict evidence: aSeal  ↔  Lean4: .approve policyId

-- SnaklTalk: Verdict silence: aString ↔  Lean4: .reject  policyId

inductive SnaklVerdict where

  | evidence (seal    : WormSeal) : SnaklVerdict

  | silence  (reason  : String)   : SnaklVerdict

  deriving Repr



def SnaklVerdict.toVerdict (policyId : PolicyId) : SnaklVerdict → Verdict

  | .evidence _ => .approve policyId

  | .silence  _ => .reject  policyId



-- ── Sovereign critical tasks ──────────────────────────────────────────────────

-- Actions that always require human oversight — sovereignty boundary.

-- Any policy evaluating these MUST return human_required.

def sovereignCriticalTasks : List String :=

  [ "deploy_mainnet", "rotate_root_keys", "modify_trust_deed",

    "corpus_training_export", "capability_grant", "treasury_transfer",

    "worm_chain_reset", "agent_revocation", "seal_override" ]



def requiresHumanGate (taskType : String) : Bool :=

  taskType ∈ sovereignCriticalTasks



-- ── Policy typeclass ──────────────────────────────────────────────────────────

class Policy (π : PolicyId) where

  eval : EvalContext → Verdict



-- ── Proofs ────────────────────────────────────────────────────────────────────



theorem approved_is_lawful (a : MoralAction) :

    judge a = .approve → lawful a = true := by

  intro h

  unfold judge at h

  by_cases hl : lawful a = true

  · exact hl

  · simp [hl] at h



theorem repent_implies_not_lawful (a : MoralAction) :

    judge a = .repent → lawful a = false := by

  intro h

  unfold judge at h

  by_cases hl : lawful a = true

  · simp [hl] at h

  · rfl



theorem verdict_exhaustive (a : MoralAction) :

    judge a = .approve ∨ judge a = .repent := by

  unfold judge

  by_cases h : lawful a = true <;> simp [h]



theorem combine_singleton (v : Verdict) :

    Verdict.combine [v] = v := by

  simp [Verdict.combine]



-- Priority ordering is strict

theorem priority_bounded (v : Verdict) : v.priority ≤ 4 := by

  match v with

  | .approve _        => simp [Verdict.priority]

  | .reject _         => simp [Verdict.priority]

  | .defer _          => simp [Verdict.priority]

  | .escalate _       => simp [Verdict.priority]

  | .human_required _ => simp [Verdict.priority]



-- Bridge round-trip: evidence → approve, silence → reject

theorem snakl_evidence_approves (seal : WormSeal) (pid : PolicyId) :

    (SnaklVerdict.evidence seal).toVerdict pid = .approve pid := by

  rfl



theorem snakl_silence_rejects (reason : String) (pid : PolicyId) :

    (SnaklVerdict.silence reason).toVerdict pid = .reject pid := by

  rfl



-- repent always escalates (never silently absorbs)

theorem repent_escalates (a : MoralAction) (pid : PolicyId)

    (h : judge a = .repent) :

    (judge a).toVerdict pid = .escalate "moral_arbiter" := by

  rw [h]; rfl



-- ── Example actions ───────────────────────────────────────────────────────────

-- Kept for smoke-testing the predicate logic.



def lawfulAction : MoralAction :=

  { truthful := true, harmful := false, exploitative := false,

    requiresConsent := false, hasConsent := false,

    witnessed := true, cited := true }



def dishonestAction : MoralAction :=

  { truthful := false, harmful := false, exploitative := false,

    requiresConsent := false, hasConsent := false,

    witnessed := true, cited := true }



def harmfulAction : MoralAction :=

  { truthful := true, harmful := true, exploitative := false,

    requiresConsent := false, hasConsent := false,

    witnessed := true, cited := true }



theorem example_lawful_approves    : judge lawfulAction   = .approve  := by native_decide

theorem example_dishonest_repents  : judge dishonestAction = .repent  := by native_decide

theorem example_harmful_repents    : judge harmfulAction  = .repent   := by native_decide

end Sovereign.Judge