diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 --- /dev/null +++ b/CHANGELOG.md @@ -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. diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -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)$. + + + +### 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: + +| 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).* diff --git a/gargamelle-sheaf.cabal b/gargamelle-sheaf.cabal new file mode 100644 --- /dev/null +++ b/gargamelle-sheaf.cabal @@ -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 diff --git a/src/Gargamelle/Sheaf.hs b/src/Gargamelle/Sheaf.hs new file mode 100644 --- /dev/null +++ b/src/Gargamelle/Sheaf.hs @@ -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 diff --git a/src/Gargamelle/Sheaf/Cohomology.hs b/src/Gargamelle/Sheaf/Cohomology.hs new file mode 100644 --- /dev/null +++ b/src/Gargamelle/Sheaf/Cohomology.hs @@ -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 diff --git a/src/Gargamelle/Sheaf/Complex.hs b/src/Gargamelle/Sheaf/Complex.hs new file mode 100644 --- /dev/null +++ b/src/Gargamelle/Sheaf/Complex.hs @@ -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 diff --git a/src/Gargamelle/Sheaf/Diffusion.hs b/src/Gargamelle/Sheaf/Diffusion.hs new file mode 100644 --- /dev/null +++ b/src/Gargamelle/Sheaf/Diffusion.hs @@ -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 diff --git a/test/Main.hs b/test/Main.hs new file mode 100644 --- /dev/null +++ b/test/Main.hs @@ -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")