gargamelle-core — Categorical Institutions, Colimit Pushout Weaving & Interface Discovery

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 σ

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.

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\).

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.

3. Module Architecture & Repertoire Breadth

The package exports 10 modules providing category-theoretic institution infrastructure:

4. Executable Worked Examples

4.1 Checking Satisfaction Condition Invariance

{-# 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

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.