# `gargamelle-sheaf` — Cellular Sheaves, Store Comonad Diffusion & Homological Fault Localization
[](https://haskell.org)
[](https://spdx.org/licenses/EUPL-1.2.html)
[](../../README.md#architectural-tier-map)
---
## 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)$.
<!-- See Note [Cellular Sheaf Restriction Maps and Stalk Functors] [ref:note-cellular-sheaf-stalks] -->
### 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.
<!-- See Note [Store Comonad Cellular Diffusion and Harmonic Consensus] [ref:note-store-comonad-diffusion] -->
### 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.
<!-- See Note [Sheaf Coboundary Operator and Cohomological Obstructions] [ref:note-sheaf-coboundary-obstructions] -->
---
## 3. Module Architecture & Repertoire Breadth
The package exports 4 modules providing topological data structures, comonadic diffusion, and cohomology:
| Module | Primary Types & Typeclasses | Architectural Purpose |
| :--- | :--- | :--- |
| [`Gargamelle.Sheaf.Complex`](src/Gargamelle/Sheaf/Complex.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-sheaf/docs/Gargamelle-Sheaf-Complex.html)) | [`CellComplex`](src/Gargamelle/Sheaf/Complex.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-sheaf/docs/Gargamelle-Sheaf-Complex.html#t:CellComplex)), [`fromEdges`](src/Gargamelle/Sheaf/Complex.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-sheaf/docs/Gargamelle-Sheaf-Complex.html#v:fromEdges)), [`Cell`](src/Gargamelle/Sheaf/Complex.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-sheaf/docs/Gargamelle-Sheaf-Complex.html#t:Cell)), [`star`](src/Gargamelle/Sheaf/Complex.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-sheaf/docs/Gargamelle-Sheaf-Complex.html#v:star)), [`boundary`](src/Gargamelle/Sheaf/Complex.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-sheaf/docs/Gargamelle-Sheaf-Complex.html#v:boundary)), [`eulerCharacteristic`](src/Gargamelle/Sheaf/Complex.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-sheaf/docs/Gargamelle-Sheaf-Complex.html#v:eulerCharacteristic)) | 1D cell complexes, graded face posets, star co-faces, and topological invariants. |
| [`Gargamelle.Sheaf.Diffusion`](src/Gargamelle/Sheaf/Diffusion.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-sheaf/docs/Gargamelle-Sheaf-Diffusion.html)) | [`CellularSheaf`](src/Gargamelle/Sheaf/Diffusion.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-sheaf/docs/Gargamelle-Sheaf-Diffusion.html#t:CellularSheaf)), [`symmetricSheaf`](src/Gargamelle/Sheaf/Diffusion.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-sheaf/docs/Gargamelle-Sheaf-Diffusion.html#v:symmetricSheaf)), [`directionalSheaf`](src/Gargamelle/Sheaf/Diffusion.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-sheaf/docs/Gargamelle-Sheaf-Diffusion.html#v:directionalSheaf)), [`Cochain0`](src/Gargamelle/Sheaf/Diffusion.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-sheaf/docs/Gargamelle-Sheaf-Diffusion.html#t:Cochain0)), [`cochainToStore`](src/Gargamelle/Sheaf/Diffusion.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-sheaf/docs/Gargamelle-Sheaf-Diffusion.html#v:cochainToStore)), [`diffuseUntilHarmonic`](src/Gargamelle/Sheaf/Diffusion.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-sheaf/docs/Gargamelle-Sheaf-Diffusion.html#v:diffuseUntilHarmonic)) | Cellular sheaves, 0-cochains, Store comonad cellular diffusion, and Knaster-Tarski fixed-point consensus. |
| [`Gargamelle.Sheaf.Cohomology`](src/Gargamelle/Sheaf/Cohomology.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-sheaf/docs/Gargamelle-Sheaf-Cohomology.html)) | [`coboundary`](src/Gargamelle/Sheaf/Cohomology.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-sheaf/docs/Gargamelle-Sheaf-Cohomology.html#v:coboundary)), [`isHarmonicCochain`](src/Gargamelle/Sheaf/Cohomology.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-sheaf/docs/Gargamelle-Sheaf-Cohomology.html#v:isHarmonicCochain)), [`GlobalSection`](src/Gargamelle/Sheaf/Cohomology.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-sheaf/docs/Gargamelle-Sheaf-Cohomology.html#t:GlobalSection)), [`locateObstructions`](src/Gargamelle/Sheaf/Cohomology.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-sheaf/docs/Gargamelle-Sheaf-Cohomology.html#v:locateObstructions)), [`verifyModelAmalgamation`](src/Gargamelle/Sheaf/Cohomology.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-sheaf/docs/Gargamelle-Sheaf-Cohomology.html#v:verifyModelAmalgamation)) | Sheaf coboundary operator, $H^0$ global sections, Model Amalgamation Theorem, and $H^1$ fault localization. |
| [`Gargamelle.Sheaf`](src/Gargamelle/Sheaf.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-sheaf/docs/Gargamelle-Sheaf.html)) | — | Convenience umbrella re-exporting `Complex`, `Diffusion`, and `Cohomology`. |
---
## 4. Executable Worked Examples
### 4.1 Comonadic Consensus Diffusion Over Cell Complex
```haskell
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
```haskell
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](../../README.md).*