packages feed

gargamelle-sheaf (empty) → 0.1.0.0

raw patch · 9 files changed

+1223/−0 lines, 9 filesdep +basedep +comonaddep +containers

Dependencies added: base, comonad, containers, gargamelle-core, gargamelle-logic, gargamelle-model, gargamelle-sheaf, hspec, lattices, proarrow, profunctors

Files

+ CHANGELOG.md view
@@ -0,0 +1,7 @@+# Changelog for gargamelle-sheaf++## 0.1.0.0 — Initial Release++- Cellular sheaves and Store comonad diffusion for fault localization.+- Cell complexes, sheaf cohomology, and harmonic diffusion.+- Algebraic topology algorithms for invariant localization.
+ LICENSE view
@@ -0,0 +1,189 @@+EUROPEAN UNION PUBLIC LICENCE v. 1.2+EUPL © the European Union 2007, 2016++This European Union Public Licence (the ‘EUPL’) applies to the Work (as defined below) which is provided under the+terms of this Licence. Any use of the Work, other than as authorised under this Licence is prohibited (to the extent such+use is covered by a right of the copyright holder of the Work).+The Work is provided under the terms of this Licence when the Licensor (as defined below) has placed the following+notice immediately following the copyright notice for the Work:+                          Licensed under the EUPL+or has expressed by any other means his willingness to license under the EUPL.++1.Definitions+In this Licence, the following terms have the following meaning:+— ‘The Licence’:this Licence.+— ‘The Original Work’:the work or software distributed or communicated by the Licensor under this Licence, available+as Source Code and also as Executable Code as the case may be.+— ‘Derivative Works’:the works or software that could be created by the Licensee, based upon the Original Work or+modifications thereof. This Licence does not define the extent of modification or dependence on the Original Work+required in order to classify a work as a Derivative Work; this extent is determined by copyright law applicable in+the country mentioned in Article 15.+— ‘The Work’:the Original Work or its Derivative Works.+— ‘The Source Code’:the human-readable form of the Work which is the most convenient for people to study and+modify.+— ‘The Executable Code’:any code which has generally been compiled and which is meant to be interpreted by+a computer as a program.+— ‘The Licensor’:the natural or legal person that distributes or communicates the Work under the Licence.+— ‘Contributor(s)’:any natural or legal person who modifies the Work under the Licence, or otherwise contributes to+the creation of a Derivative Work.+— ‘The Licensee’ or ‘You’:any natural or legal person who makes any usage of the Work under the terms of the+Licence.+— ‘Distribution’ or ‘Communication’:any act of selling, giving, lending, renting, distributing, communicating,+transmitting, or otherwise making available, online or offline, copies of the Work or providing access to its essential+functionalities at the disposal of any other natural or legal person.++2.Scope of the rights granted by the Licence+The Licensor hereby grants You a worldwide, royalty-free, non-exclusive, sublicensable licence to do the following, for+the duration of copyright vested in the Original Work:+— use the Work in any circumstance and for all usage,+— reproduce the Work,+— modify the Work, and make Derivative Works based upon the Work,+— communicate to the public, including the right to make available or display the Work or copies thereof to the public+and perform publicly, as the case may be, the Work,+— distribute the Work or copies thereof,+— lend and rent the Work or copies thereof,+— sublicense rights in the Work or copies thereof.+Those rights can be exercised on any media, supports and formats, whether now known or later invented, as far as the+applicable law permits so.+In the countries where moral rights apply, the Licensor waives his right to exercise his moral right to the extent allowed+by law in order to make effective the licence of the economic rights here above listed.+The Licensor grants to the Licensee royalty-free, non-exclusive usage rights to any patents held by the Licensor, to the+extent necessary to make use of the rights granted on the Work under this Licence.++3.Communication of the Source Code+The Licensor may provide the Work either in its Source Code form, or as Executable Code. If the Work is provided as+Executable Code, the Licensor provides in addition a machine-readable copy of the Source Code of the Work along with+each copy of the Work that the Licensor distributes or indicates, in a notice following the copyright notice attached to+the Work, a repository where the Source Code is easily and freely accessible for as long as the Licensor continues to+distribute or communicate the Work.++4.Limitations on copyright+Nothing in this Licence is intended to deprive the Licensee of the benefits from any exception or limitation to the+exclusive rights of the rights owners in the Work, of the exhaustion of those rights or of other applicable limitations+thereto.++5.Obligations of the Licensee+The grant of the rights mentioned above is subject to some restrictions and obligations imposed on the Licensee. Those+obligations are the following:++Attribution right: The Licensee shall keep intact all copyright, patent or trademarks notices and all notices that refer to+the Licence and to the disclaimer of warranties. The Licensee must include a copy of such notices and a copy of the+Licence with every copy of the Work he/she distributes or communicates. The Licensee must cause any Derivative Work+to carry prominent notices stating that the Work has been modified and the date of modification.++Copyleft clause: If the Licensee distributes or communicates copies of the Original Works or Derivative Works, this+Distribution or Communication will be done under the terms of this Licence or of a later version of this Licence unless+the Original Work is expressly distributed only under this version of the Licence — for example by communicating+‘EUPL v. 1.2 only’. The Licensee (becoming Licensor) cannot offer or impose any additional terms or conditions on the+Work or Derivative Work that alter or restrict the terms of the Licence.++Compatibility clause: If the Licensee Distributes or Communicates Derivative Works or copies thereof based upon both+the Work and another work licensed under a Compatible Licence, this Distribution or Communication can be done+under the terms of this Compatible Licence. For the sake of this clause, ‘Compatible Licence’ refers to the licences listed+in the appendix attached to this Licence. Should the Licensee's obligations under the Compatible Licence conflict with+his/her obligations under this Licence, the obligations of the Compatible Licence shall prevail.++Provision of Source Code: When distributing or communicating copies of the Work, the Licensee will provide+a machine-readable copy of the Source Code or indicate a repository where this Source will be easily and freely available+for as long as the Licensee continues to distribute or communicate the Work.+Legal Protection: This Licence does not grant permission to use the trade names, trademarks, service marks, or names+of the Licensor, except as required for reasonable and customary use in describing the origin of the Work and+reproducing the content of the copyright notice.++6.Chain of Authorship+The original Licensor warrants that the copyright in the Original Work granted hereunder is owned by him/her or+licensed to him/her and that he/she has the power and authority to grant the Licence.+Each Contributor warrants that the copyright in the modifications he/she brings to the Work are owned by him/her or+licensed to him/her and that he/she has the power and authority to grant the Licence.+Each time You accept the Licence, the original Licensor and subsequent Contributors grant You a licence to their contributions+to the Work, under the terms of this Licence.++7.Disclaimer of Warranty+The Work is a work in progress, which is continuously improved by numerous Contributors. It is not a finished work+and may therefore contain defects or ‘bugs’ inherent to this type of development.+For the above reason, the Work is provided under the Licence on an ‘as is’ basis and without warranties of any kind+concerning the Work, including without limitation merchantability, fitness for a particular purpose, absence of defects or+errors, accuracy, non-infringement of intellectual property rights other than copyright as stated in Article 6 of this+Licence.+This disclaimer of warranty is an essential part of the Licence and a condition for the grant of any rights to the Work.++8.Disclaimer of Liability+Except in the cases of wilful misconduct or damages directly caused to natural persons, the Licensor will in no event be+liable for any direct or indirect, material or moral, damages of any kind, arising out of the Licence or of the use of the+Work, including without limitation, damages for loss of goodwill, work stoppage, computer failure or malfunction, loss+of data or any commercial damage, even if the Licensor has been advised of the possibility of such damage. However,+the Licensor will be liable under statutory product liability laws as far such laws apply to the Work.++9.Additional agreements+While distributing the Work, You may choose to conclude an additional agreement, defining obligations or services+consistent with this Licence. However, if accepting obligations, You may act only on your own behalf and on your sole+responsibility, not on behalf of the original Licensor or any other Contributor, and only if You agree to indemnify,+defend, and hold each Contributor harmless for any liability incurred by, or claims asserted against such Contributor by+the fact You have accepted any warranty or additional liability.++10.Acceptance of the Licence+The provisions of this Licence can be accepted by clicking on an icon ‘I agree’ placed under the bottom of a window+displaying the text of this Licence or by affirming consent in any other similar way, in accordance with the rules of+applicable law. Clicking on that icon indicates your clear and irrevocable acceptance of this Licence and all of its terms+and conditions.+Similarly, you irrevocably accept this Licence and all of its terms and conditions by exercising any rights granted to You+by Article 2 of this Licence, such as the use of the Work, the creation by You of a Derivative Work or the Distribution+or Communication by You of the Work or copies thereof.++11.Information to the public+In case of any Distribution or Communication of the Work by means of electronic communication by You (for example,+by offering to download the Work from a remote location) the distribution channel or media (for example, a website)+must at least provide to the public the information requested by the applicable law regarding the Licensor, the Licence+and the way it may be accessible, concluded, stored and reproduced by the Licensee.++12.Termination of the Licence+The Licence and the rights granted hereunder will terminate automatically upon any breach by the Licensee of the terms+of the Licence.+Such a termination will not terminate the licences of any person who has received the Work from the Licensee under+the Licence, provided such persons remain in full compliance with the Licence.++13.Miscellaneous+Without prejudice of Article 9 above, the Licence represents the complete agreement between the Parties as to the+Work.+If any provision of the Licence is invalid or unenforceable under applicable law, this will not affect the validity or+enforceability of the Licence as a whole. Such provision will be construed or reformed so as necessary to make it valid+and enforceable.+The European Commission may publish other linguistic versions or new versions of this Licence or updated versions of+the Appendix, so far this is required and reasonable, without reducing the scope of the rights granted by the Licence.+New versions of the Licence will be published with a unique version number.+All linguistic versions of this Licence, approved by the European Commission, have identical value. Parties can take+advantage of the linguistic version of their choice.++14.Jurisdiction+Without prejudice to specific agreement between parties,+— any litigation resulting from the interpretation of this License, arising between the European Union institutions,+bodies, offices or agencies, as a Licensor, and any Licensee, will be subject to the jurisdiction of the Court of Justice+of the European Union, as laid down in article 272 of the Treaty on the Functioning of the European Union,+— any litigation arising between other parties and resulting from the interpretation of this License, will be subject to+the exclusive jurisdiction of the competent court where the Licensor resides or conducts its primary business.++15.Applicable Law+Without prejudice to specific agreement between parties,+— this Licence shall be governed by the law of the European Union Member State where the Licensor has his seat,+resides or has his registered office,+— this licence shall be governed by Belgian law if the Licensor has no seat, residence or registered office inside+a European Union Member State.++Appendix++‘Compatible Licences’ according to Article 5 EUPL are:+— GNU General Public License (GPL) v. 2, v. 3+— GNU Affero General Public License (AGPL) v. 3+— Open Software License (OSL) v. 2.1, v. 3.0+— Eclipse Public License (EPL) v. 1.0+— CeCILL v. 2.0, v. 2.1+— Mozilla Public Licence (MPL) v. 2+— GNU Lesser General Public Licence (LGPL) v. 2.1, v. 3+— Creative Commons Attribution-ShareAlike v. 3.0 Unported (CC BY-SA 3.0) for works other than software+— European Union Public Licence (EUPL) v. 1.1, v. 1.2+— Québec Free and Open-Source Licence — Reciprocity (LiLiQ-R) or Strong Reciprocity (LiLiQ-R+).++The European Commission may update this Appendix to later versions of the above licences without producing+a new version of the EUPL, as long as they provide the rights granted in Article 2 of this Licence and protect the+covered Source Code from exclusive appropriation.+All other changes or additions to this Appendix require the production of a new EUPL version.
+ README.md view
@@ -0,0 +1,198 @@+# `gargamelle-sheaf` — Cellular Sheaves, Store Comonad Diffusion & Homological Fault Localization++[![Haskell](https://img.shields.io/badge/Language-Haskell2010-purple.svg)](https://haskell.org)+[![License: EUPL-1.2](https://img.shields.io/badge/License-EUPL--1.2-blue.svg)](https://spdx.org/licenses/EUPL-1.2.html)+[![Tier 4 Applied Topology](https://img.shields.io/badge/Tier-4%20Applied%20Topology%20%26%20Sheaf%20Cohomology-teal.svg)](../../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).*
+ gargamelle-sheaf.cabal view
@@ -0,0 +1,69 @@+cabal-version: 3.0+name: gargamelle-sheaf+version: 0.1.0.0+synopsis: Cellular sheaves and Store comonad diffusion for fault localization+description:+  Cellular sheaves, Store comonad diffusion, and homological fault+  localization for Gargamelle. Provides cell complexes, sheaf cohomology,+  harmonic diffusion, and algebraic topology algorithms for invariant+  localization.+license: EUPL-1.2+license-file: LICENSE+author: Nadia Yvette Chambers+maintainer: nadia.yvette.chambers@ik.me+category: Math+homepage: https://github.com/NadiaYvette/gargamelle+bug-reports: https://github.com/NadiaYvette/gargamelle/issues+extra-doc-files:+  README.md+  CHANGELOG.md+build-type: Simple+tested-with:+  GHC == 9.6.7,+  GHC == 9.8.4,+  GHC == 9.10.3,+  GHC == 9.12.4,+  GHC == 9.14.1++source-repository head+  type: git+  location: https://github.com/NadiaYvette/gargamelle+  subdir: packages/gargamelle-sheaf++library+  exposed-modules:+    Gargamelle.Sheaf+    Gargamelle.Sheaf.Complex+    Gargamelle.Sheaf.Diffusion+    Gargamelle.Sheaf.Cohomology+  hs-source-dirs: src+  default-language: Haskell2010+  ghc-options: -Wall -Wcompat -Wredundant-constraints+  build-depends:+    base >= 4.18 && < 5,+    containers >= 0.6 && < 0.9,+    comonad >= 5.0 && < 5.1,+    lattices >= 2.2 && < 2.3,+    profunctors >= 5.6 && < 5.7,+    gargamelle-logic >= 0.1 && < 0.2,+    gargamelle-model >= 0.1 && < 0.2,+    gargamelle-core >= 0.1 && < 0.2,+    proarrow >= 0.2 && < 0.3++test-suite tests+  type: exitcode-stdio-1.0+  main-is: Main.hs+  hs-source-dirs: test+  default-language: Haskell2010+  ghc-options: -Wall+  build-depends:+    base >= 4.18 && < 5,+    gargamelle-sheaf,+    gargamelle-logic >= 0.1 && < 0.2,+    gargamelle-model >= 0.1 && < 0.2,+    gargamelle-core >= 0.1 && < 0.2,+    containers >= 0.6 && < 0.9,+    lattices >= 2.2 && < 2.3,+    comonad >= 5.0 && < 5.1,+    proarrow >= 0.2 && < 0.3,+    hspec >= 2.10 && < 2.12
+ src/Gargamelle/Sheaf.hs view
@@ -0,0 +1,14 @@+{-# LANGUAGE BlockArguments #-}++module Gargamelle.Sheaf+  ( -- * Cell Complexes & Topology+    module Gargamelle.Sheaf.Complex+    -- * Cellular Sheaf & Store Comonad Diffusion+  , module Gargamelle.Sheaf.Diffusion+    -- * Coboundary, H0 Amalgamation & H1 Obstructions+  , module Gargamelle.Sheaf.Cohomology+  ) where++import Gargamelle.Sheaf.Complex+import Gargamelle.Sheaf.Diffusion+import Gargamelle.Sheaf.Cohomology
+ src/Gargamelle/Sheaf/Cohomology.hs view
@@ -0,0 +1,187 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeOperators #-}++module Gargamelle.Sheaf.Cohomology+  ( -- * Coboundary Operator+    coboundary+  , isHarmonicCochain+    -- * Cohomological Invariants+  , CohomologyResult(..)+  , computeCohomology+  , GlobalSection(..)+  , globalSection+    -- * Homological Fault Localization+  , InterfaceObstruction(..)+  , locateObstructions+    -- * Model Amalgamation Bridge+  , verifyModelAmalgamation+  ) where++import Data.Map.Strict (Map)+import qualified Data.Map.Strict as Map+import Proarrow.Core (type (~>))+import Gargamelle.Core.Institution (Sig, Mod)+import Gargamelle.Core.Weaving (PushoutWeaving(..))+import Gargamelle.Sheaf.Complex (CellComplex(..))+import Gargamelle.Sheaf.Diffusion (CellularSheaf(..), Cochain0(..), Cochain1(..))++{- Note [Sheaf Coboundary Operator and Cohomological Obstructions]+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~+[tag:note-sheaf-coboundary-obstructions]+In applied algebraic topology (Curry 2014, Ghrist 2014), the Sheaf Coboundary+operator \delta^0 maps assignments of vertex stalks (0-cochains C^0) to interface+discrepancies across boundary edges (1-cochains C^1):+  \delta^0 : C^0(G; F) -> C^1(G; F)+  \delta^0(x)_e = (ρ_{u ⊴ e}(x_u), ρ_{v ⊴ e}(x_v))++Mathematical Invariants & Verification Semantics:+  1. Harmonic Global Sections (0-th Cohomology H^0):+       H^0(G; F) = ker \delta^0 = { x ∈ C^0 | \forall e=(u,v): ρ_{u ⊴ e}(x_u) == ρ_{v ⊴ e}(x_v) }+     A 0-cochain is harmonic (isHarmonicCochain == True) if and only if all boundary+     projections coincide across every 1-cell. This formally certifies that the local+     specifications glue into a globally coherent system.++  2. The Model Amalgamation Theorem:+       H^0(G; Mod) ≅ Mod(colim D)+     When vertex stalks represent institution models, global sections H^0 are naturally+     isomorphic to models over the colimit apex of the diagram D ('verifyModelAmalgamation').+     Global consistency is verified locally at interfaces rather than globally on giant ASTs.++  3. Cohomological Obstructions (1-st Cohomology H^1):+       H^1(G; F) = coker \delta^0+     When \delta^0(x) fails to vanish, the non-zero cochains represent cohomological+     obstructions to global consistency. 'locateObstructions' extracts the exact failing+     edges e and mismatched values (sourceRestriction, targetRestriction).++  4. Inductive Repair Guidance:+     Rather than treating verification failures as opaque rejections, CEGIS synthesis loops+     inspect H^1 obstructions to identify which subsystem interface breached its contract,+     transforming verification from binary testing into directed homological program repair.+-}++-- | Sheaf Coboundary Operator \delta^0 : C^0(G; F) -> C^1(G; F).+-- Computes the boundary discrepancy pair (\rho_{u \trianglelefteq e}(x_u), \rho_{v \trianglelefteq e}(x_v))+-- for every 1-cell e = (u, v) in the complex.+-- Returns the 1-cochain of discrepancies and a boolean indicating whether the cochain is harmonic (no discrepancies).+--+-- See Note [Sheaf Coboundary Operator and Cohomological Obstructions] [ref:note-sheaf-coboundary-obstructions].+coboundary+  :: forall vId eId stalk edgeStalk.+     (Ord vId, Eq edgeStalk)+  => CellComplex vId eId+  -> CellularSheaf vId eId stalk edgeStalk+  -> Cochain0 vId stalk+  -> (Cochain1 eId (edgeStalk, edgeStalk), Bool)+coboundary complex sheaf (Cochain0 vMap) =+  let edgeDiffs = Map.mapWithKey computeEdge (edges complex)+      harmonic = all (uncurry (==)) edgeDiffs+  in (Cochain1 edgeDiffs, harmonic)+  where+    computeEdge eId (u, v) =+      let stU = Map.findWithDefault (error "coboundary: source vertex missing") u vMap+          stV = Map.findWithDefault (error "coboundary: target vertex missing") v vMap+      in (restrictSrc sheaf eId stU, restrictTgt sheaf eId stV)++-- | Predicate checking if a 0-cochain satisfies the sheaf gluing condition (zero coboundary).+isHarmonicCochain+  :: (Ord vId, Eq edgeStalk)+  => CellComplex vId eId+  -> CellularSheaf vId eId stalk edgeStalk+  -> Cochain0 vId stalk+  -> Bool+isHarmonicCochain complex sheaf = snd . coboundary complex sheaf++-- | Result of cohomology computation at dimension 0 and 1.+data CohomologyResult eId edgeStalk+  = HarmonicSection+  | ObstructionMap (Map eId (edgeStalk, edgeStalk))+  deriving (Eq, Show)++-- | Compute cohomology: returns 'HarmonicSection' if all boundary restrictions agree,+-- or 'ObstructionMap' detailing the non-vanishing cocycles.+computeCohomology+  :: (Ord vId, Eq edgeStalk)+  => CellComplex vId eId+  -> CellularSheaf vId eId stalk edgeStalk+  -> Cochain0 vId stalk+  -> CohomologyResult eId edgeStalk+computeCohomology complex sheaf c0 =+  let (Cochain1 diffs, harmonic) = coboundary complex sheaf c0+  in if harmonic+       then HarmonicSection+       else ObstructionMap (Map.filter (uncurry (/=)) diffs)++-- | A verified global section H^0(G; F) = ker \delta^0.+-- Represents a family of local models or specifications that seamlessly glue across all cell boundaries.+newtype GlobalSection vId stalk = GlobalSection+  { unGlobalSection :: Cochain0 vId stalk+  } deriving (Eq, Show)++-- | Validate and wrap a 0-cochain as a global section.+-- Fails if any boundary discrepancy exists.+globalSection+  :: (Ord vId, Eq edgeStalk)+  => CellComplex vId eId+  -> CellularSheaf vId eId stalk edgeStalk+  -> Cochain0 vId stalk+  -> Maybe (GlobalSection vId stalk)+globalSection complex sheaf c0 =+  if isHarmonicCochain complex sheaf c0+    then Just (GlobalSection c0)+    else Nothing++-- | Detailed diagnostic report for an interface obstruction along an edge.+data InterfaceObstruction eId edgeStalk = InterfaceObstruction+  { obstructedEdge    :: eId+  , sourceRestriction :: edgeStalk+  , targetRestriction :: edgeStalk+  } deriving (Eq, Show)++-- | Locate all failing interface boundaries where H^1 cohomological obstructions prevent composition.+-- Directly informs the CEGIS counterexample-guided repair loop.+--+-- See Note [Sheaf Coboundary Operator and Cohomological Obstructions] [ref:note-sheaf-coboundary-obstructions].+locateObstructions+  :: (Ord vId, Eq edgeStalk)+  => CellComplex vId eId+  -> CellularSheaf vId eId stalk edgeStalk+  -> Cochain0 vId stalk+  -> [InterfaceObstruction eId edgeStalk]+locateObstructions complex sheaf c0 =+  let (Cochain1 diffs, _) = coboundary complex sheaf c0+  in [ InterfaceObstruction+         { obstructedEdge    = e+         , sourceRestriction = s+         , targetRestriction = t+         }+     | (e, (s, t)) <- Map.toList diffs+     , s /= t+     ]++-- | Theorem: Model Amalgamation via Sheaves.+-- H^0(G; Mod) \cong Mod(colim D).+-- When base model mB and aspect model mW restrict to identical interface models on c,+-- the sheaf coboundary vanishes and 'amalgamate' produces a verified amalgamated model.+--+-- See Note [Sheaf Coboundary Operator and Cohomological Obstructions] [ref:note-sheaf-coboundary-obstructions].+verifyModelAmalgamation+  :: forall inst (c :: Sig inst) (b :: Sig inst) (w :: Sig inst) (p :: Sig inst).+     (PushoutWeaving inst, Eq (Mod inst c))+  => (c ~> b) -> (c ~> w) -> (b ~> p) -> (w ~> p)+  -> Mod inst b+  -> Mod inst w+  -> (Mod inst b -> Mod inst c)+  -> (Mod inst w -> Mod inst c)+  -> Maybe (Mod inst p)+verifyModelAmalgamation f g inB inW mb mw reductB reductW =+  let restrB = reductB mb+      restrW = reductW mw+  in if restrB == restrW+       then amalgamate @inst f g inB inW mb mw+       else Nothing
+ src/Gargamelle/Sheaf/Complex.hs view
@@ -0,0 +1,154 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE ScopedTypeVariables #-}++module Gargamelle.Sheaf.Complex+  ( -- * Cell Complex+    CellComplex(..)+  , emptyComplex+  , fromEdges+  , addVertex+  , addEdge+    -- * Cells & Poset Structure+  , Cell(..)+  , cellDimension+  , cellFaces+  , isFaceOf+  , Orientation(..)+  , orientationSign+  , incidenceSign+    -- * Complex Queries+  , incidentEdges+  , star+  , boundary+  , numVertices+  , numEdges+  , eulerCharacteristic+  ) where++import Data.List (nub)+import Data.Map.Strict (Map)+import qualified Data.Map.Strict as Map++-- | A finite 1-dimensional cell complex (graph complex) G = (V, E).+-- 0-cells represent component spaces/loci, and 1-cells represent interface boundaries.+data CellComplex vId eId = CellComplex+  { vertices :: [vId]+  , edges    :: Map eId (vId, vId) -- ^ Map from edge ID to (source, target)+  } deriving (Eq, Show)++-- | Orientation of an incident edge relative to a vertex.+data Orientation+  = Forward   -- ^ Directed away from the vertex (vertex is source: sign -1 in boundary)+  | Backward  -- ^ Directed into the vertex (vertex is target: sign +1 in boundary)+  deriving (Eq, Ord, Show)++-- | Numeric homological sign for an orientation.+orientationSign :: Orientation -> Int+orientationSign = \case+  Forward  -> -1+  Backward -> 1++-- | The cells of a 1-dimensional cell complex, forming a graded face poset.+data Cell vId eId+  = Cell0 vId  -- ^ 0-cell (vertex)+  | Cell1 eId  -- ^ 1-cell (edge)+  deriving (Eq, Ord, Show)++-- | Dimension of a cell in the complex.+cellDimension :: Cell vId eId -> Int+cellDimension = \case+  Cell0 _ -> 0+  Cell1 _ -> 1++-- | Empty cell complex.+emptyComplex :: CellComplex vId eId+emptyComplex = CellComplex+  { vertices = []+  , edges    = Map.empty+  }++-- | Construct a cell complex from a list of directed edges (eId, source, target).+-- Vertices are automatically collected and deduplicated.+fromEdges :: forall vId eId. (Eq vId, Ord eId) => [(eId, vId, vId)] -> CellComplex vId eId+fromEdges edgeList = CellComplex+  { vertices = nub [ v | (_, u, w) <- edgeList, v <- [u, w] ]+  , edges    = Map.fromList [ (e, (u, w)) | (e, u, w) <- edgeList ]+  }++-- | Add a vertex to the cell complex if not already present.+addVertex :: (Eq vId) => vId -> CellComplex vId eId -> CellComplex vId eId+addVertex v complex+  | v `elem` vertices complex = complex+  | otherwise = complex { vertices = v : vertices complex }++-- | Add an edge and ensure its endpoints are in the vertex set.+addEdge :: (Ord eId, Eq vId) => eId -> vId -> vId -> CellComplex vId eId -> CellComplex vId eId+addEdge e u w complex = complex+  { vertices = nub (u : w : vertices complex)+  , edges    = Map.insert e (u, w) (edges complex)+  }++-- | Boundary of a 1-cell (source, target).+boundary :: (Ord eId) => CellComplex vId eId -> eId -> Maybe (vId, vId)+boundary complex e = Map.lookup e (edges complex)++-- | Incident edges for a given vertex, including orientation and adjacent vertex.+incidentEdges :: (Eq vId) => CellComplex vId eId -> vId -> [(eId, Orientation, vId)]+incidentEdges complex v =+  [ (e, orient, other)+  | (e, (u, w)) <- Map.toList (edges complex)+  , (orient, other) <-+      let isSrc = u == v+          isTgt = w == v+      in case (isSrc, isTgt) of+           (True, False) -> [(Forward, w)]+           (False, True) -> [(Backward, u)]+           (True, True)  -> [(Forward, w), (Backward, u)]+           (False, False)-> []+  ]++-- | Star (co-faces) of a vertex: all edges incident to v.+star :: (Eq vId) => CellComplex vId eId -> vId -> [eId]+star complex v = [ e | (e, _, _) <- incidentEdges complex v ]++-- | Faces of a cell in the cell complex.+cellFaces :: (Ord eId) => CellComplex vId eId -> Cell vId eId -> [Cell vId eId]+cellFaces complex = \case+  Cell0 v -> [Cell0 v]+  Cell1 e -> case boundary complex e of+    Nothing     -> [Cell1 e]+    Just (u, w) -> [Cell1 e, Cell0 u, Cell0 w]++-- | Partial order predicate: checks whether sigma is a face of tau (sigma <= tau).+isFaceOf :: (Ord eId, Eq vId) => CellComplex vId eId -> Cell vId eId -> Cell vId eId -> Bool+isFaceOf complex sigma tau = case (sigma, tau) of+  (Cell0 u, Cell0 v) -> u == v+  (Cell1 a, Cell1 b) -> a == b+  (Cell0 u, Cell1 e) -> case boundary complex e of+    Just (src, tgt) -> u == src || u == tgt+    Nothing         -> False+  (Cell1 _, Cell0 _) -> False++-- | Homological incidence sign [e : v] of vertex v in edge e.+-- Returns -1 if v is source, +1 if v is target, 0 if not incident.+incidenceSign :: (Ord eId, Eq vId) => CellComplex vId eId -> eId -> vId -> Int+incidenceSign complex e v = case boundary complex e of+  Just (src, tgt) -> case (v == src, v == tgt) of+    (True, False) -> -1+    (False, True) -> 1+    (True, True)  -> 0 -- Self-loop cancels in standard homology+    (False, False)-> 0+  Nothing -> 0++-- | Count of 0-cells.+numVertices :: CellComplex vId eId -> Int+numVertices = length . vertices++-- | Count of 1-cells.+numEdges :: CellComplex vId eId -> Int+numEdges = Map.size . edges++-- | Euler characteristic chi = |V| - |E| = beta_0 - beta_1.+eulerCharacteristic :: CellComplex vId eId -> Int+eulerCharacteristic c = numVertices c - numEdges c
+ src/Gargamelle/Sheaf/Diffusion.hs view
@@ -0,0 +1,262 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE ScopedTypeVariables #-}++module Gargamelle.Sheaf.Diffusion+  ( -- * Cellular Sheaf+    CellularSheaf(..)+  , symmetricSheaf+  , directionalSheaf+  , liftEdge+    -- * Cochains+  , Cochain0(..)+  , Cochain1(..)+  , lookupCochain0+  , lookupCochain1+  , fromListCochain0+  , fromListCochain1+    -- * Store Comonad Cellular Diffusion+  , cochainToStore+  , diffuseLocalRule+  , stepDiffusion+  , diffuseUntilHarmonic+  , diffuseTrace+  , meet+  , join+  ) where++import Algebra.Lattice (Lattice(..), BoundedMeetSemiLattice(..))+import Control.Comonad (extend, extract)+import Control.Comonad.Store (Store, store, pos, peek)+import Data.Map.Strict (Map)+import qualified Data.Map.Strict as Map+import Gargamelle.Sheaf.Complex (CellComplex(..), incidentEdges, Orientation(..))++-- | Infix meet operator synonym.+meet :: Lattice a => a -> a -> a+meet = (/\)++-- | Infix join operator synonym.+join :: Lattice a => a -> a -> a+join = (\/)++{- Note [Cellular Sheaf Restriction Maps and Stalk Functors]+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~+[tag:note-cellular-sheaf-stalks]+In applied algebraic topology and distributed systems verification, a software+architecture is formalized as a 1-dimensional cell complex (graph complex) G = (V, E):+  - 0-cells (vertices v ∈ V) represent local component scopes, module stalks, or actor states.+  - 1-cells (edges e ∈ E) represent shared communication interfaces, network channels, or contracts.++A Cellular Sheaf F over G consists of:+  1. Stalk Assignments:+     - For each vertex v, a stalk F(v) containing local contract or model data.+     - For each edge e = (u, v), an edge stalk F(e) representing the shared interface contract.+  2. Restriction Maps:+     Along face inclusions u ⊴ e and v ⊴ e, directional restriction morphisms:+       ρ_{u ⊴ e} : F(u) -> F(e)+       ρ_{v ⊴ e} : F(v) -> F(e)+     project vertex-level internal invariants into the shared interface language.+  3. Adjoint Lifting Maps:+     Adjoint or Galois dual maps lift edge-level interface contracts back into vertex stalks:+       liftSrc : F(e) -> F(u)+       liftTgt : F(e) -> F(v)++Operational Role:+  - Symmetric Sheaves ('symmetricSheaf'): Useful when communication channels are non-directional+    and contracts are symmetric across client and server.+  - Directional Sheaves ('directionalSheaf'): Essential when interfaces distinguish caller+    assumptions from callee guarantees.+-}++-- | A cellular sheaf F over a cell complex G = (V, E).+-- Assigns stalks to 0-cells and 1-cells, restriction maps along cell face inclusions,+-- and comonadic diffusion lifting maps back to the vertex stalks.+--+-- See Note [Cellular Sheaf Restriction Maps and Stalk Functors] [ref:note-cellular-sheaf-stalks].+data CellularSheaf vId eId stalk edgeStalk = CellularSheaf+  { restrictSrc :: eId -> stalk -> edgeStalk  -- ^ \rho_{u \trianglelefteq e} (source restriction)+  , restrictTgt :: eId -> stalk -> edgeStalk  -- ^ \rho_{v \trianglelefteq e} (target restriction)+  , liftSrc     :: eId -> edgeStalk -> stalk  -- ^ Lift edge stalk back to source vertex+  , liftTgt     :: eId -> edgeStalk -> stalk  -- ^ Lift edge stalk back to target vertex+  }++-- | Backward-compatible alias for lifting an edge stalk to a vertex stalk.+liftEdge :: CellularSheaf vId eId stalk edgeStalk -> eId -> edgeStalk -> stalk+liftEdge = liftSrc++-- | Construct a cellular sheaf where source and target restrictions/lifts are symmetric.+symmetricSheaf+  :: (eId -> stalk -> edgeStalk)+  -> (eId -> edgeStalk -> stalk)+  -> CellularSheaf vId eId stalk edgeStalk+symmetricSheaf restr lift_ = CellularSheaf+  { restrictSrc = restr+  , restrictTgt = restr+  , liftSrc     = lift_+  , liftTgt     = lift_+  }++-- | Construct a cellular sheaf with explicit directional restriction and lifting maps.+directionalSheaf+  :: (eId -> stalk -> edgeStalk)+  -> (eId -> stalk -> edgeStalk)+  -> (eId -> edgeStalk -> stalk)+  -> (eId -> edgeStalk -> stalk)+  -> CellularSheaf vId eId stalk edgeStalk+directionalSheaf = CellularSheaf++-- | 0-Cochain: an assignment of stalk elements across 0-cells (vertices).+newtype Cochain0 vId stalk = Cochain0+  { unCochain0 :: Map vId stalk+  } deriving (Eq, Show, Functor)++-- | 1-Cochain: an assignment of edge stalk elements across 1-cells (edges).+newtype Cochain1 eId edgeStalk = Cochain1+  { unCochain1 :: Map eId edgeStalk+  } deriving (Eq, Show, Functor)++instance (Ord vId, Lattice stalk) => Lattice (Cochain0 vId stalk) where+  (/\) (Cochain0 m1) (Cochain0 m2) = Cochain0 (Map.unionWith (/\) m1 m2)+  (\/) (Cochain0 m1) (Cochain0 m2) = Cochain0 (Map.unionWith (\/) m1 m2)++-- | Safe lookup in a 0-cochain.+lookupCochain0 :: (Ord vId) => vId -> Cochain0 vId stalk -> Maybe stalk+lookupCochain0 v (Cochain0 m) = Map.lookup v m++-- | Safe lookup in a 1-cochain.+lookupCochain1 :: (Ord eId) => eId -> Cochain1 eId edgeStalk -> Maybe edgeStalk+lookupCochain1 e (Cochain1 m) = Map.lookup e m++-- | Create a 0-cochain from an association list.+fromListCochain0 :: (Ord vId) => [(vId, stalk)] -> Cochain0 vId stalk+fromListCochain0 = Cochain0 . Map.fromList++-- | Create a 1-cochain from an association list.+fromListCochain1 :: (Ord eId) => [(eId, edgeStalk)] -> Cochain1 eId edgeStalk+fromListCochain1 = Cochain1 . Map.fromList++-- | Represent a 0-cochain as a Store comonad focused at an initial vertex position.+-- Lookups outside the cochain return the provided fallback default.+cochainToStore :: (Ord vId) => stalk -> Cochain0 vId stalk -> vId -> Store vId stalk+cochainToStore defaultStalk (Cochain0 m) =+  store (\v -> Map.findWithDefault defaultStalk v m)++{- Note [Store Comonad Cellular Diffusion and Harmonic Consensus]+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~+[tag:note-store-comonad-diffusion]+Traditional graph algorithms process networks via imperative mutation or iterative loops.+Gargamelle models cellular space comonadically using 'Control.Comonad.Store':+  data Store s a = Store (s -> a) s++In cellular diffusion:+  - Focus 's = vId': The focused vertex currently under evaluation ('pos w').+  - Local Value: The current stalk contract at that vertex ('extract w').+  - Neighborhood Access: Neighboring contract stalks across incident cell boundaries+    are queried via 'peek other w'.++Parallel Global Diffusion via Comonadic 'extend':+  The local rule 'diffuseLocalRule' inspects the focused vertex and takes the meet (/\)+  of its current contract with all incoming restricted and lifted neighbor contracts.+  By invoking:+    diffusedStore = extend (diffuseLocalRule complex sheaf) baseStore+  the comonad simultaneously computes updated stalks across all vertices in the cell+  complex in a single pure, parallel evaluation step.++Knaster-Tarski Fixed-Point Convergence:+  Because the meet operation (/\) in a meet-semi-lattice is monotonic and contracting:+    c_{t+1} ⩽ c_t+  the sequence of 0-cochains produced by 'diffuseUntilHarmonic':+    c_0 ⩾ c_1 ⩾ c_2 ⩾ ...+  is guaranteed by the Knaster-Tarski fixed-point theorem to converge to the greatest+  lower bound (the most permissive common contract refinement that satisfies all interface+  boundary constraints simultaneously).+-}++-- | Local cellular diffusion step evaluated comonadically at the current focused vertex.+-- Uses 'pos' to determine the active vertex, 'extract' for its current stalk value,+-- and 'peek' to inspect neighboring stalks across incident cell boundaries.+--+-- See Note [Store Comonad Cellular Diffusion and Harmonic Consensus] [ref:note-store-comonad-diffusion].+diffuseLocalRule+  :: forall vId eId stalk edgeStalk.+     (Ord vId, BoundedMeetSemiLattice stalk)+  => CellComplex vId eId+  -> CellularSheaf vId eId stalk edgeStalk+  -> Store vId stalk+  -> stalk+diffuseLocalRule complex sheaf w =+  let v = pos w+      curr = extract w+      incident = incidentEdges complex v+      incomingStalks =+        [ case orient of+            Forward  ->+              -- v is source of e; neighbor 'other' is target.+              -- Restrict other's stalk via restrictTgt, then lift to v via liftSrc.+              liftSrc sheaf e (restrictTgt sheaf e (peek other w))+            Backward ->+              -- v is target of e; neighbor 'other' is source.+              -- Restrict other's stalk via restrictSrc, then lift to v via liftTgt.+              liftTgt sheaf e (restrictSrc sheaf e (peek other w))+        | (e, orient, other) <- incident+        ]+  in foldr meet curr incomingStalks++-- | Advance diffusion by one discrete comonadic step across all vertices in the complex.+-- Uses 'extend' on the Store comonad to simultaneously compute new values everywhere.+stepDiffusion+  :: forall vId eId stalk edgeStalk.+     (Ord vId, BoundedMeetSemiLattice stalk)+  => CellComplex vId eId+  -> CellularSheaf vId eId stalk edgeStalk+  -> Cochain0 vId stalk+  -> Cochain0 vId stalk+stepDiffusion complex sheaf c0@(Cochain0 m) = case vertices complex of+  [] -> c0+  (v0:_) ->+    let baseStore = cochainToStore top c0 v0+        diffusedStore = extend (diffuseLocalRule complex sheaf) baseStore+        newM = Map.fromList [ (v, peek v diffusedStore) | v <- vertices complex ]+    in Cochain0 (Map.union newM m)++-- | Knaster-Tarski fixed-point iteration via Store comonad diffusion.+-- Iterates until a fixed point is reached (new state == current state)+-- or the step limit is reached.+--+-- See Note [Store Comonad Cellular Diffusion and Harmonic Consensus] [ref:note-store-comonad-diffusion].+diffuseUntilHarmonic+  :: (Ord vId, BoundedMeetSemiLattice stalk, Eq stalk)+  => Int  -- ^ Maximum iterations+  -> CellComplex vId eId+  -> CellularSheaf vId eId stalk edgeStalk+  -> Cochain0 vId stalk+  -> Cochain0 vId stalk+diffuseUntilHarmonic maxSteps complex sheaf = go 0+  where+    go step c0+      | step >= maxSteps = c0+      | otherwise =+          let cNext = stepDiffusion complex sheaf c0+          in if cNext == c0+               then c0+               else go (step + 1) cNext++-- | Trace diffusion steps until a fixed point is reached or the limit is reached.+-- Produces the sequence of intermediate 0-cochains.+diffuseTrace+  :: (Ord vId, BoundedMeetSemiLattice stalk, Eq stalk)+  => Int+  -> CellComplex vId eId+  -> CellularSheaf vId eId stalk edgeStalk+  -> Cochain0 vId stalk+  -> [Cochain0 vId stalk]+diffuseTrace maxSteps complex sheaf = go 0+  where+    go step c0+      | step >= maxSteps = [c0]+      | otherwise =+          let cNext = stepDiffusion complex sheaf c0+          in if cNext == c0+               then [c0]+               else c0 : go (step + 1) cNext
+ test/Main.hs view
@@ -0,0 +1,143 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeFamilies #-}++module Main (main) where++import Test.Hspec+import qualified Data.Map.Strict as Map+import Algebra.Lattice (Lattice(..), BoundedMeetSemiLattice(..))++import Gargamelle.Sheaf.Complex+import Gargamelle.Sheaf.Diffusion+import Gargamelle.Sheaf.Cohomology++-- A simple bounded lattice of contract specifications for testing diffusion+-- Ordered by specificity / constraint strength: Top is least constrained (True),+-- Safe is constrained, Critical is most constrained, Bottom is contradictory (False).+data ContractLevel = Unconstrained | StandardSecurity | HighIntegrity | Contradiction+  deriving (Eq, Ord, Show)++instance Lattice ContractLevel where+  (/\) = max -- Meet strengthens the contract (higher constraint level)+  (\/) = min -- Join weakens the contract++instance BoundedMeetSemiLattice ContractLevel where+  top = Unconstrained++main :: IO ()+main = hspec do+  describe "Gargamelle.Sheaf.Complex (Finite Cell Complexes & Graded Posets)" do+    it "constructs cell complexes with vertices, edges, and boundary maps" do+      let complex = fromEdges [("e1", "v1", "v2"), ("e2", "v2", "v3")]+      numVertices complex `shouldBe` 3+      numEdges complex `shouldBe` 2+      boundary complex "e1" `shouldBe` Just ("v1", "v2")+      boundary complex "e2" `shouldBe` Just ("v2", "v3")++    it "evaluates face relations (sigma <= tau) and cell dimensions" do+      let complex = fromEdges [("e1", "v1", "v2")]+      cellDimension (Cell0 "v1") `shouldBe` 0+      cellDimension (Cell1 "e1") `shouldBe` 1+      isFaceOf complex (Cell0 "v1") (Cell1 "e1") `shouldBe` True+      isFaceOf complex (Cell0 "v2") (Cell1 "e1") `shouldBe` True+      isFaceOf complex (Cell0 "v3") (Cell1 "e1") `shouldBe` False+      isFaceOf complex (Cell1 "e1") (Cell0 "v1") `shouldBe` False++    it "computes star co-faces and homological incidence signs" do+      let complex = fromEdges [("e1", "v1", "v2"), ("e2", "v2", "v3")]+      star complex "v2" `shouldBe` ["e1", "e2"]+      incidenceSign complex "e1" "v1" `shouldBe` (-1) -- source+      incidenceSign complex "e1" "v2" `shouldBe` 1    -- target+      incidenceSign complex "e1" "v3" `shouldBe` 0    -- non-incident++    it "computes topological Euler characteristic chi = |V| - |E|" do+      let triangle = fromEdges [("e1", "v1", "v2"), ("e2", "v2", "v3"), ("e3", "v3", "v1")]+      eulerCharacteristic triangle `shouldBe` 0+      let tree = fromEdges [("e1", "v1", "v2"), ("e2", "v2", "v3")]+      eulerCharacteristic tree `shouldBe` 1++  -- Tested against Note [Cellular Sheaf Restriction Maps and Stalk Functors] [ref:note-cellular-sheaf-stalks]+  -- and Note [Store Comonad Cellular Diffusion and Harmonic Consensus] [ref:note-store-comonad-diffusion]+  describe "Gargamelle.Sheaf.Diffusion (Store Comonad & Knaster-Tarski)" do+    it "diffuses specifications comonadically across cell boundaries" do+      let complex = fromEdges [("e1", "A", "B"), ("e2", "B", "C")]+          -- Symmetric sheaf where restriction is identity and lifting is identity+          sheaf = symmetricSheaf (\_ c -> c) (\_ e -> e)+          -- Initial cochain: A has HighIntegrity, B and C are Unconstrained+          initialC0 = fromListCochain0+            [ ("A", HighIntegrity)+            , ("B", Unconstrained)+            , ("C", Unconstrained)+            ]+          -- Step 1: HighIntegrity propagates to B+          step1 = stepDiffusion complex sheaf initialC0+      lookupCochain0 "A" step1 `shouldBe` Just HighIntegrity+      lookupCochain0 "B" step1 `shouldBe` Just HighIntegrity+      lookupCochain0 "C" step1 `shouldBe` Just Unconstrained++      -- Step 2: HighIntegrity propagates from B to C+      let step2 = stepDiffusion complex sheaf step1+      lookupCochain0 "C" step2 `shouldBe` Just HighIntegrity++    it "converges to a Knaster-Tarski harmonic fixed point" do+      let complex = fromEdges [("e1", "A", "B"), ("e2", "B", "C")]+          sheaf = symmetricSheaf (\_ c -> c) (\_ e -> e)+          initialC0 = fromListCochain0+            [ ("A", StandardSecurity)+            , ("B", HighIntegrity)+            , ("C", Unconstrained)+            ]+          fixedPoint = diffuseUntilHarmonic 10 complex sheaf initialC0+      -- In the contract meet lattice, HighIntegrity meet StandardSecurity is HighIntegrity+      lookupCochain0 "A" fixedPoint `shouldBe` Just HighIntegrity+      lookupCochain0 "B" fixedPoint `shouldBe` Just HighIntegrity+      lookupCochain0 "C" fixedPoint `shouldBe` Just HighIntegrity++  -- Tested against Note [Sheaf Coboundary Operator and Cohomological Obstructions] [ref:note-sheaf-coboundary-obstructions]+  describe "Gargamelle.Sheaf.Cohomology (Coboundaries, H0 & H1 Localization)" do+    it "identifies harmonic global sections (H0) when boundary restrictions agree" do+      let complex = fromEdges [("e1", "A", "B")]+          sheaf = symmetricSheaf (\_ (portVal :: Int) -> portVal) (\_ e -> e)+          harmonicC0 = fromListCochain0 [("A", 42), ("B", 42)]+          (Cochain1 diffs, harmonic) = coboundary complex sheaf harmonicC0+      harmonic `shouldBe` True+      diffs `shouldBe` Map.fromList [("e1", (42, 42))]+      computeCohomology complex sheaf harmonicC0 `shouldBe` HarmonicSection+      globalSection complex sheaf harmonicC0 `shouldNotBe` Nothing++    it "detects H1 cohomological obstructions and localizes failing interface boundaries" do+      let complex = fromEdges [("e1", "A", "B"), ("e2", "B", "C")]+          sheaf = symmetricSheaf (\_ (v :: String) -> v) (\_ e -> e)+          -- A and B agree on "token_auth", but C provides "cert_auth"+          inconsistentC0 = fromListCochain0+            [ ("A", "token_auth")+            , ("B", "token_auth")+            , ("C", "cert_auth")+            ]+          (Cochain1 diffs, harmonic) = coboundary complex sheaf inconsistentC0+      harmonic `shouldBe` False+      diffs `shouldBe` Map.fromList [("e1", ("token_auth", "token_auth")), ("e2", ("token_auth", "cert_auth"))]++      let obstructions = locateObstructions complex sheaf inconsistentC0+      case obstructions of+        [obs] -> do+          obstructedEdge obs `shouldBe` "e2"+          sourceRestriction obs `shouldBe` "token_auth"+          targetRestriction obs `shouldBe` "cert_auth"+        _ -> expectationFailure "Expected exactly one obstruction"++    it "verifies model amalgamation when boundary restrictions match" do+      -- Pushout diagram model verification:+      -- Component A produces (10, True), Component B produces (True, "ok")+      -- Interface edge requires boolean flag agreement+      let modelA = (10 :: Int, True)+          modelB = (True, "ok" :: String)+          reductA = snd+          reductB = fst+      -- When restrictions agree on True, amalgamation is sound+      (reductA modelA == reductB modelB) `shouldBe` True+      let amalgamated = if reductA modelA == reductB modelB+                          then Just (fst modelA, fst modelB, snd modelB)+                          else Nothing+      amalgamated `shouldBe` Just (10, True, "ok")