gargamelle-sheaf — Cellular Sheaves, Store Comonad Diffusion & Homological Fault Localization

1. Executive Summary & Problem Framing

Verifying distributed software architectures, multi-agent microservices, and modular contract networks typically relies on monolithic whole-program SMT encoding. As systems scale, this monolithic approach suffers from three critical bottlenecks:

1. Combinatorial State Explosion: Encoding every module simultaneously produces exponential solver slowdowns and out-of-memory timeouts.
2. Opaque Global Failure Reports: When a composite system fails to satisfy a specification, provers return a monolithic counterexample without pinpointing which subsystem interface caused the contradiction.
3. Fragile Contract Reconciliation: Components developed independently lack an automated algebraic mechanism to negotiate mutually acceptable contract relaxations across boundaries.

gargamelle-sheaf transforms software verification using applied algebraic topology:

• Cellular Graph Complexes: Formalizes architectures as 1-dimensional cell complexes \(G = (V, E)\), modeling modules as 0-cells and shared interfaces as 1-cells.
• Cellular Sheaves: Assigns contract and model stalks over cells, with directional restriction maps (\(\rho_{u \trianglelefteq e}, \rho_{v \trianglelefteq e}\)) projecting internal specifications to interface boundaries.
• Store Comonad Consensus Diffusion: Models cellular space comonadically via Store vId stalk, evaluating parallel discrete diffusion across all vertices via comonadic extend.
• Knaster-Tarski Harmonic Convergence: Iterates meet semi-lattice contractions (diffuseUntilHarmonic) to compute the greatest lower bound contract refinement satisfying all interfaces.
• Sheaf Coboundary (\(\delta^0\)) & Homological Fault Localization (\(H^1\)): Detects vanishing coboundaries as certified global sections (\(H^0(G; \mathcal{F}) = \ker \delta^0\)) and uses cohomological obstructions (\(H^1 = \operatorname{coker} \delta^0\)) to pinpoint the exact failing interface boundaries to guide automated repair.

2. Mathematical Foundations & Theoretical Invariants

2.1 Software Architectures as Cell Complexes

A 1-dimensional cell complex (graph complex) \(G = (V, E)\) consists of:

• 0-cells (Vertices \(v \in V\)): Component scopes or module stalks.
• 1-cells (Edges \(e \in E\)): Communication channels or shared interface contracts.
• Graded Poset: Faces satisfy \(\sigma \trianglelefteq \tau\), with incidence signs \([e : u] = -1\) (source) and \([e : v] = +1\) (target).
• Euler Characteristic: \(\chi(G) = |V| - |E|\).

2.2 Cellular Sheaves & Stalk Assignments

A cellular sheaf \(\mathcal{F}\) over \(G\) associates:

1. To each vertex \(v \in V\), a stalk \(\mathcal{F}(v)\) (e.g. assume-guarantee contract or model).
2. To each edge \(e = (u, v) \in E\), an edge stalk \(\mathcal{F}(e)\) (shared interface schema).
3. To each face relation \(u \trianglelefteq e\), a restriction morphism \(\rho_{u \trianglelefteq e} : \mathcal{F}(u) \to \mathcal{F}(e)\).

2.3 Store Comonad Cellular Diffusion & Knaster-Tarski Consensus

Evaluating cellular diffusion across all vertices simultaneously is expressed comonadically using Control.Comonad.Store: \[\text{Store } s \; a \cong (s \to a) \times s\]

              ┌───────────────────────────────────────────┐
              │  Store vId stalk (Comonadic Space)        │
              │  - pos w      : Focused active vertex     │
              │  - extract w  : Current vertex stalk      │
              │  - peek nbr w : Stalk at neighbor nbr     │
              └─────────────────────┬─────────────────────┘
                                    │
                       extend diffuseLocalRule
                                    │
                                    ▼
              ┌───────────────────────────────────────────┐
              │  Updated Cochain0 across all V in ||      │
              └───────────────────────────────────────────┘

By the Knaster-Tarski fixed-point theorem, because contract meet semi-lattices are monotonic and contractive (\(c_{t+1} \le c_t\)), the diffusion sequence \(c_0 \ge c_1 \ge c_2 \dots\) generated by diffuseUntilHarmonic converges monotonically to the unique greatest lower bound.

2.4 Sheaf Coboundary (\(\delta^0\)) & Cohomological Obstructions (\(H^1\))

The 0-th coboundary operator \(\delta^0 : C^0(G; \mathcal{F}) \to C^1(G; \mathcal{F})\) evaluates boundary discrepancies along every edge \(e = (u, v)\): \[\delta^0(x)_e = (\rho_{u \trianglelefteq e}(x_u), \rho_{v \trianglelefteq e}(x_v))\]

          F(u) (Vertex u)                      F(v) (Vertex v)
            │                                    │
            │ ρ_{u ⊴ e}                         │ ρ_{v ⊴ e}
            ▼                                    ▼
          F(e) ───────── Discrepancy? ─────────► F(e)
                     (s == t) => H^0 Section
                     (s /= t) => H^1 Obstruction

• Harmonic Global Sections (\(H^0(G; \mathcal{F}) = \ker \delta^0\)): When all boundary evaluations match (\(\forall e: \rho_u(x_u) = \rho_v(x_v)\)), \(x\) forms a global section certifying system-wide compatibility.
• Model Amalgamation Theorem: \(H^0(G; \mathbf{Mod}) \cong \mathbf{Mod}(\operatorname{colim} D)\).
• Cohomological Obstructions (\(H^1 = \operatorname{coker} \delta^0\)): When \(\delta^0(x) \neq 0\), locateObstructions pinpoints the exact failing edges \(e\) and mismatched values \((s, t)\) to guide directed repair.

3. Module Architecture & Repertoire Breadth

The package exports 4 modules providing topological data structures, comonadic diffusion, and cohomology:

4. Executable Worked Examples

4.1 Comonadic Consensus Diffusion Over Cell Complex

module ExampleSheafDiffusion where

import Algebra.Lattice (Lattice(..), BoundedMeetSemiLattice(..))
import Gargamelle.Sheaf

-- Define contract lattice: meet strengthens the requirement
data SecLevel = Public | Confidential | TopSecret deriving (Eq, Ord, Show)

instance Lattice SecLevel where
  (/\) = max
  (\/) = min

instance BoundedMeetSemiLattice SecLevel where
  top = Public

diffuseSecurityPolicy :: IO ()
diffuseSecurityPolicy = do
  -- Graph: ServiceA <---> ServiceB <---> ServiceC
  let complex = fromEdges [("e1", "ServiceA", "ServiceB"), ("e2", "ServiceB", "ServiceC")]
      sheaf = symmetricSheaf (\_ c -> c) (\_ e -> e)
      initial = fromListCochain0
        [ ("ServiceA", TopSecret)
        , ("ServiceB", Public)
        , ("ServiceC", Public)
        ]
      -- Diffuse until consensus is reached
      harmonic = diffuseUntilHarmonic 10 complex sheaf initial

  putStrLn $ "Diffused consensus: " ++ show harmonic
  -- Evaluates to TopSecret across all three vertices

4.2 Pinpointing Failing Interfaces via \(H^1\) Cohomology

module ExampleFaultLocalization where

import Gargamelle.Sheaf

localizeFailingInterface :: IO ()
localizeFailingInterface = do
  let complex = fromEdges [("api_edge", "AuthService", "BillingService")]
      sheaf = symmetricSheaf (\_ (v :: String) -> v) (\_ e -> e)
      candidate = fromListCochain0
        [ ("AuthService", "BearerTokenV2")
        , ("BillingService", "BasicAuthLegacy")
        ]
      obstructions = locateObstructions complex sheaf candidate

  case obstructions of
    [] -> putStrLn "System globally consistent (H^1 = 0)."
    obs -> mapM_ (\o -> putStrLn $ "Interface failure on: " ++ obstructedEdge o) obs

5. Integration Points & Subsystem Boundaries

gargamelle-sheaf forms Tier 4 (Applied Topology) of the architecture:

┌────────────────────────────────────────────────────────┐
│               Downstream Consumers                     │
│  - gargamelle-workflow: Sheaf-Gated CEGIS Synthesis    │
│  - Automated Repair Engines: H¹ Obstruction Guided Fix │
└──────────────────────────▲─────────────────────────────┘
                           │
                  [gargamelle-sheaf]
                           │
┌──────────────────────────▼─────────────────────────────┐
│               Upstream Substrates                      │
│  - comonad (>= 5.0): Store Comonad                     │
│  - lattices (>= 2.2): BoundedMeetSemiLattice           │
│  - gargamelle-core: Institutions, Colimits             │
│  - gargamelle-logic: Contracts, Galois Connections     │
└────────────────────────────────────────────────────────┘

6. Diagnostic & Troubleshooting Guide

6.1 Diffusion Oscillation or Non-Termination

• Symptom: diffuseUntilHarmonic exhausts max step limit without reaching a fixed point.
• Root Cause: The underlying stalk lattice violates the descending chain condition or the local update rule is non-monotonic.
• Remedy: Ensure the stalk type implements BoundedMeetSemiLattice where (/\) is strictly monotonic (\(x \wedge y \le x\)), guaranteeing finite convergence on finite graphs.

6.2 Missing Vertex in Coboundary Lookup

• Symptom: Runtime error coboundary: source vertex missing.
• Root Cause: A 0-cochain was constructed missing an entry for a vertex declared in the cell complex.
• Remedy: Use fromListCochain0 covering all vertices complex, or initialize via cochainToStore top c0.

Part of the Gargamelle Verification Suite.