# `gargamelle-core` — Categorical Institutions, Colimit Pushout Weaving & Interface Discovery
[](https://haskell.org)
[](https://spdx.org/licenses/EUPL-1.2.html)
[](../../README.md#architectural-tier-map)
---
## 1. Executive Summary & Problem Framing
Formal verification and automated program synthesis across complex systems encounter three fundamental architectural challenges:
1. **Heterogeneous Specification Logics:** Real-world systems mix propositional assertions, first-order relational constraints, equational graph rewrites, and temporal choreographies. Hardcoding a single logical framework fractures tooling and prevents compositional reasoning.
2. **Invasive Aspect Mutation:** Augmenting a verified component with auxiliary capabilities (logging, authentication, persistent storage, or transactional safety) frequently mutates the base AST directly, invalidating existing safety proofs and risking name/sort collisions.
3. **Implicit Interface Mismatches:** Distributed and multi-agent components evolve independently, making manual schema coordination fragile, unscalable, and error-prone.
`gargamelle-core` resolves these challenges through classical and modern category theory:
- **Goguen-Burstall Institutions:** Formalizes logical systems via signatures $\mathbf{Sig}$, covariant sentence translation $\mathbf{Sen}$, contravariant model reduction $\mathbf{Mod}$, and executable satisfaction invariance.
- **Categorical Pushout Feature Weaving ($B \amalg_C W$):** Non-invasively synthesizes composite system specifications by amalgamating a base specification $B$ and an aspect extension $W$ along their shared boundary $C$.
- **Pullback Protocol Discovery ($A \times_E B$):** Automatically discovers the maximal compatible communication interface between two independently specified components interacting with an ambient host environment $E$.
- **Colimit Mediating Morphisms:** Computes universal semantic deltas (`factorSemanticDelta`) that propagate updates and proofs incrementally across structural modifications.
---
## 2. Mathematical Foundations & Theoretical Invariants
### 2.1 The Goguen-Burstall Satisfaction Invariance Condition
An institution $\mathcal{I} = (\mathbf{Sig}, \mathbf{Sen}, \mathbf{Mod}, \models)$ consists of:
1. A category of signatures $\mathbf{Sig}$ and signature morphisms $\sigma : \Sigma_1 \to \Sigma_2$.
2. A functor $\mathbf{Sen} : \mathbf{Sig} \to \mathbf{Set}$ translating sentences.
3. A contravariant functor $\mathbf{Mod} : \mathbf{Sig}^{\mathrm{op}} \to \mathbf{Cat}$ reducing models.
4. A family of satisfaction relations $\models_\Sigma \;\subseteq |\mathbf{Mod}(\Sigma)| \times \mathbf{Sen}(\Sigma)$ satisfying:
$$M' \models_{\Sigma_2} \mathbf{Sen}(\sigma)(\varphi) \iff \mathbf{Mod}(\sigma)(M') \models_{\Sigma_1} \varphi$$
In `gargamelle-core`, this condition is verified operationally through inspectable `Verifier` ASTs:
```
translateSen σ
Sen(Σ1) ──────────────► Sen(Σ2)
│ │
│ ⊨_Σ1 │ ⊨_Σ2
▼ ▼
Mod(Σ1) ◄────────────── Mod(Σ2)
reductMod σ
```
<!-- See Note [Goguen-Burstall Categorical Institution Satisfaction Invariance] [ref:note-institution-satisfaction-invariance] -->
### 2.2 Pushout Feature Weaving ($B \amalg_C W$)
Given a base specification $B$, an aspect concern $W$, and their common interface $C$, feature weaving is formalized as the categorical pushout in the category of signatures:
```
C ──────────────► W (Aspect Extension)
│ │
│ inclB │ injAspect
▼ ▼
B ──────────────► P = B ⨿_C W (Woven Specification)
(Base System) injBase
```
- **Commutativity:** $\operatorname{injBase} \circ \operatorname{inclB} = \operatorname{injAspect} \circ \operatorname{inclW}$.
- **Model Amalgamation:** By contravariance of $\mathbf{Mod}$, the pushout in $\mathbf{Sig}$ induces a pullback in $\mathbf{Cat}$. Any pair of models $(M_B, M_W)$ that coincide on $C$ amalgamate into a unique model $M_P$ over $P$.
- **Proof Preservation:** Invariants proven on $B$ translate functorially along $\operatorname{injBase}$ into $P$ with zero re-verification overhead.
<!-- See Note [Categorical Pushout Feature Weaving] [ref:note-pushout-feature-weaving] -->
### 2.3 Pullback Interface Discovery ($A \times_E B$)
When two components $A$ and $B$ interact with an ambient environment $E$ via morphisms $f : A \to E$ and $g : B \to E$, the universal shared interface $P$ through which they communicate is given by the categorical pullback:
```
P = A ×_E B ────────► B (Component 2)
│ │
│ projA │ g
▼ ▼
A ─────────────► E (Environment / Host)
(Component 1) f
```
- **Interface Compatibility:** The square commutes ($f \circ \operatorname{projA} = g \circ \operatorname{projB}$), guaranteeing environmental compatibility.
- **Universal Factorization:** For any candidate protocol $Q$ with $f \circ q_A = g \circ q_B$, `factorInterface` calculates the unique mediating arrow $u : Q \to P$.
<!-- See Note [Pullback Interface Discovery] [ref:note-pullback-interface-discovery] -->
### 2.4 Colimit Mediating Morphisms & Semantic Deltas
When an architectural specification $P$ undergoes evolution to candidate cocone $Q$, `factorSemanticDelta` evaluates the unique arrow $u : P \to Q$ mediating between the colimit legs. This mediating arrow reifies the exact structural delta required to migrate proofs and properties to the new architecture.
<!-- See Note [Colimit Mediating Morphisms and Semantic Delta Propagation] [ref:note-colimit-semantic-delta] -->
---
## 3. Module Architecture & Repertoire Breadth
The package exports 10 modules providing category-theoretic institution infrastructure:
| Module | Primary Types & Typeclasses | Architectural Purpose |
| :--- | :--- | :--- |
| [`Gargamelle.Core.Institution`](src/Gargamelle/Core/Institution.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-core/docs/Gargamelle-Core-Institution.html)) | [`CategoricalInstitution`](src/Gargamelle/Core/Institution.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-core/docs/Gargamelle-Core-Institution.html#t:CategoricalInstitution)), [`LogicalSyntax`](src/Gargamelle/Core/Institution.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-core/docs/Gargamelle-Core-Institution.html#t:LogicalSyntax)), [`ModelTheory`](src/Gargamelle/Core/Institution.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-core/docs/Gargamelle-Core-Institution.html#t:ModelTheory)), [`checkSatisfactionInvariance`](src/Gargamelle/Core/Institution.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-core/docs/Gargamelle-Core-Institution.html#v:checkSatisfactionInvariance)) | Goguen-Burstall categorical institutions with executable satisfaction verification. |
| [`Gargamelle.Core.Weaving`](src/Gargamelle/Core/Weaving.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-core/docs/Gargamelle-Core-Weaving.html)) | [`PushoutWeaving`](src/Gargamelle/Core/Weaving.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-core/docs/Gargamelle-Core-Weaving.html#t:PushoutWeaving)), [`AmalgamatedModel`](src/Gargamelle/Core/Weaving.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-core/docs/Gargamelle-Core-Weaving.html#t:AmalgamatedModel)), [`weaveAspect`](src/Gargamelle/Core/Weaving.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-core/docs/Gargamelle-Core-Weaving.html#v:weaveAspect)) | Pushout feature weaving combining base systems with aspect extensions over shared boundaries. |
| [`Gargamelle.Core.Discovery`](src/Gargamelle/Core/Discovery.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-core/docs/Gargamelle-Core-Discovery.html)) | [`discoverInterface`](src/Gargamelle/Core/Discovery.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-core/docs/Gargamelle-Core-Discovery.html#v:discoverInterface)), [`factorInterface`](src/Gargamelle/Core/Discovery.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-core/docs/Gargamelle-Core-Discovery.html#v:factorInterface)) | Pullback protocol discovery and universal interface candidate factorization. |
| [`Gargamelle.Core.Colimit`](src/Gargamelle/Core/Colimit.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-core/docs/Gargamelle-Core-Colimit.html)) | [`Cocone`](src/Gargamelle/Core/Colimit.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-core/docs/Gargamelle-Core-Colimit.html#t:Cocone)), [`factorSemanticDelta`](src/Gargamelle/Core/Colimit.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-core/docs/Gargamelle-Core-Colimit.html#v:factorSemanticDelta)) | Colimit mediating morphisms and semantic delta propagation between system architectures. |
| [`Propositional`](src/Propositional.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-core/docs/Propositional.html)) | [`PropSig`](src/Propositional.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-core/docs/Propositional.html#t:PropSig)), [`SentProp`](src/Propositional.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-core/docs/Propositional.html#t:SentProp)), [`ModProp`](src/Propositional.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-core/docs/Propositional.html#t:ModProp)) | Canonical propositional institution with type-level variable symbols. |
| [`Institution`](src/Institution.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-core/docs/Institution.html)) | [`Institution`](src/Institution.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-core/docs/Institution.html#t:Institution)), [`satisfies`](src/Institution.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-core/docs/Institution.html#v:satisfies)) | Legacy institution typeclass for backwards compatibility. |
| [`SessionTypes`](src/SessionTypes.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-core/docs/SessionTypes.html)) | [`SessionType`](src/SessionTypes.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-core/docs/SessionTypes.html#t:SessionType)) | Binary session types specification and duality relations. |
| [`Sheaf`](src/Sheaf.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-core/docs/Sheaf.html)) | [`CellularSheaf`](src/Sheaf.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-core/docs/Sheaf.html#t:CellularSheaf)) | Transitional bridge re-exporting cellular sheaf definitions. |
| [`CEGIS`](src/CEGIS.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-core/docs/CEGIS.html)) | [`CEGISState`](src/CEGIS.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-core/docs/CEGIS.html#t:CEGISState)) | Counterexample-Guided Inductive Synthesis loop state definitions. |
| [`Core.AST`](src/Core/AST.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-core/docs/Core-AST.html)) | [`Expr`](src/Core/AST.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-core/docs/Core-AST.html#t:Expr)) | Core expression AST for symbolic evaluation. |
---
## 4. Executable Worked Examples
### 4.1 Checking Satisfaction Condition Invariance
```haskell
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
module ExampleInstitution where
import Proarrow.Core (type (~>))
import Gargamelle.Core.Institution
-- Given a signature morphism morph :: s1 ~> s2,
-- a sentence phi, and a target model mPrime:
verifyPreservation
:: forall i s1 s2. CategoricalInstitution i
=> (s1 ~> s2)
-> Sen i s1
-> Mod i s2
-> Bool
verifyPreservation morph phi mPrime =
let (evLHS, evRHS, isPreserved) = checkSatisfactionInvariance @i morph phi mPrime
in isPreserved && evLHS == evRHS
```
### 4.2 Non-Invasive Feature Weaving
```haskell
module ExampleWeaving where
import Proarrow.Category.Instance.Unit (Unit(..))
import Gargamelle.Core.Weaving
-- Weave an aspect into a base specification along their common interface:
weaveSystem :: IO ()
weaveSystem = do
let inclBase = Unit
inclAspect = Unit
weaveAspect inclBase inclAspect $ \_injBase _injAspect -> do
putStrLn "Weaving completed: canonical injection morphisms established."
```
---
## 5. Integration Points & Subsystem Boundaries
`gargamelle-core` occupies **Tier 3 (Logic & Institution Engine)** in the Gargamelle hierarchy:
```
┌────────────────────────────────────────────────────────┐
│ Downstream Consumers │
│ - gargamelle-fol: First-Order Logic Institution │
│ - gargamelle-equational: DPO Graph Rewriting │
│ - gargamelle-sheaf: Sheaf Restriction Functors │
│ - gargamelle-workflow: Full CEGIS Synthesis Pipelines │
└──────────────────────────▲─────────────────────────────┘
│
[gargamelle-core]
│
┌──────────────────────────▼─────────────────────────────┐
│ Upstream Substrates │
│ - gargamelle-logic: Contracts, Galois, ObsMor │
│ - gargamelle-model: Free Verifier AST, Evidence │
│ - proarrow (>= 0.2): Thin categories, Colimits │
│ - polytropos-core (>= 0.1.0.1): Structural Rep │
└────────────────────────────────────────────────────────┘
```
---
## 6. Diagnostic & Troubleshooting Guide
### 6.1 Satisfaction Invariance Failure
- **Symptom:** `checkSatisfactionInvariance` returns `isPreserved = False` or `evLHS /= evRHS`.
- **Root Cause:** Either the sentence translation functor $\mathbf{Sen}(\sigma)$ did not preserve the semantics of operators, or the model reduction functor $\mathbf{Mod}(\sigma)$ dropped necessary interpretations during pullback.
- **Remedy:** Inspect the `Evidence` produced by `evLHS` and `evRHS`. If `evLHS` contains a `Counterexample` but `evRHS` returns `VerifiedSection`, verify that variables in the reduct model are mapped correctly.
### 6.2 Pushout Apex Ambiguity
- **Symptom:** GHC complains of ambiguous type variables when invoking `weaveAspect`.
- **Root Cause:** The pushout apex type is existential in `weaveAspect`.
- **Remedy:** Use rank-N continuation pattern `weaveAspect inclB inclW $ \injB injW -> ...` and ensure the continuation consumes the injections polymorphically.
---
*Part of the [Gargamelle Verification Suite](../../README.md).*