IndisputableMonolith.Ethics.StakeGraph

   1import Mathlib
   2
   3namespace IndisputableMonolith
   4namespace Ethics
   5
   6/-- Stakeholder label. -/
   7abbrev Stakeholder := String
   8
   9/-- Stakeholder graph for COI detection. -/
  10structure StakeGraph where
  11  edge : Stakeholder → Stakeholder → Bool
  12
  13namespace StakeGraph
  14
  15def contains (xs : List Stakeholder) (s : Stakeholder) : Bool :=
  16  xs.any (fun x => decide (x = s))
  17
  18def neighbors (G : StakeGraph) (nodes : List Stakeholder) (s : Stakeholder) : List Stakeholder :=
  19  nodes.filter (fun t => G.edge s t)
  20
  21def reachable (G : StakeGraph) (nodes : List Stakeholder) (src dst : Stakeholder) : Bool :=
  22  let rec dfs (front : List Stakeholder) (visited : List Stakeholder) : Bool :=
  23    match front with
  24    | [] => False
  25    | v :: vs =>
  26        if decide (v = dst) then True else
  27        let nbrs := neighbors G nodes v
  28        let fresh := nbrs.filter (fun w => ¬ contains visited w)
  29        dfs (vs ++ fresh) (v :: visited)
  30  dfs [src] []
  31
  32def mutualReachable (G : StakeGraph) (nodes : List Stakeholder) (s t : Stakeholder) : Bool :=
  33  reachable G nodes s t && reachable G nodes t s
  34
  35def hasCycle (G : StakeGraph) (nodes : List Stakeholder) : Bool :=
  36  nodes.any (fun s => G.edge s s)
  37  || nodes.any (fun s =>
  38        nodes.any (fun t => (¬ decide (s = t)) && mutualReachable G nodes s t))
  39
  40end StakeGraph
  41end Ethics
  42end IndisputableMonolith
  43
  44