# `gargamelle-logic` — Pure Syntax, Order-Theoretic Contracts & Defunctionalized Morphisms
[](https://haskell.org)
[](https://spdx.org/licenses/EUPL-1.2.html)
[](../../README.md#architectural-tier-map)
---
## 1. Executive Summary & Problem Framing
In autonomous multi-agent verification and sheaf-theoretic program synthesis, software specifications must satisfy three competing criteria:
1. **Unambiguous Compositional Semantics:** Subsystems must compose algebraically without hidden side effects or ad-hoc casing.
2. **First-Class Introspectability:** SMT solvers, AI agents, and refactoring engines must inspect, rewrite, and verify transformation pipelines without executing opaque host closures `(->)`.
3. **Sound Contract Dualization:** When refining or composing assume-guarantee contracts, assumptions and guarantees must vary contravariantly (weakening assumptions while strengthening guarantees).
`gargamelle-logic` provides the foundational mathematical substrates for the Gargamelle engine:
- Order-theoretic contract refinement via functorial order dualization (`Algebra.Lattice.Op`).
- Defunctionalized observable morphisms (`ObsMor`) that reify function arrows into an inspectable GADT obeying `Category`, `Profunctor`, `Strong`, and `Choice` laws.
- Contravariant Galois connections ($\alpha \dashv \gamma$) between interior component stalks and boundary communication interfaces.
- Flat First-Order Logic ASTs (`LogicAST`) designed for $O(N)$ linear SMT-LIB2 emission and zero recursive stack blowups.
- Multiparty Session Types (`MPST`) choreography specifications and contextual hole specifications (`HoleSpec`) for resilient grammar parsing.
---
## 2. Mathematical Foundations & Theoretical Invariants
### 2.1 Order-Theoretic Inversion via `Op` Dualization
In contract-based design, contract refinement $C_1 \sqsubseteq C_2$ (evaluated as lattice meet $C_1 \wedge C_2$) establishes that $C_1$ is a strictly safer, more capable specification that can substitute for $C_2$ in any environment.
For guarantees $G$, refinement requires strengthening ($G_1 \wedge G_2$). For assumptions $A$, refinement requires *weakening* ($A_1 \vee A_2$), because a more refined component makes fewer demands upon its environment:
```
Base Lattice L Order-Dual Lattice Op L
(Guarantees: Meet) (Assumptions: Join)
⊤ (Weak) ⊤ = Op ⊥ (Demanding)
/ \ / \
/ \ / \
/ \ / \
g1 g2 Op a1 Op a2
\ / \ /
\ / \ /
\ / \ /
g1 ∧ g2 (Strong) Op a1 ∧ Op a2 = Op (a1 ∨ a2) (Relaxed)
... ...
⊥ (Impossible) ⊥ = Op ⊤ (Trivial)
```
By wrapping assumptions inside `Op a` from `Algebra.Lattice.Op`, the contract meet becomes the standard cartesian product meet:
$$(Op(A_1), G_1) \wedge (Op(A_2), G_2) = (Op(A_1 \vee A_2), G_1 \wedge G_2)$$
<!-- See Note [Lattice Inversion via Op Dualization] [ref:note-lattice-op-dualization] -->
### 2.2 Circular Assume-Guarantee Soundness
For mutually dependent components $C_1 = (A_1, G_1)$ and $C_2 = (A_2, G_2)$ communicating across a shared boundary, circular reasoning is sound in any Heyting algebra if and only if both entailments hold simultaneously:
$$(A_1 \wedge G_2 \implies G_1) \wedge (A_2 \wedge G_1 \implies G_2) = \top$$
<!-- See Note [Circular Assume-Guarantee Soundness] [ref:note-circular-ag-soundness] -->
### 2.3 Galois Adjunction Between Cell Stalks
To transfer contracts soundly between interior vertex stalks $\mathcal{V}$ and boundary communication channels $\mathcal{E}$, `Galois` defines an adjunction $\alpha \dashv \gamma$:
$$\operatorname{restrict}(v) \le_{\mathcal{E}} e \iff v \le_{\mathcal{V}} \operatorname{coRestrict}(e)$$
- **Unit:** $v \le_{\mathcal{V}} \operatorname{coRestrict}(\operatorname{restrict}(v))$ (projecting to boundary and lifting over-approximates).
- **Counit:** $\operatorname{restrict}(\operatorname{coRestrict}(e)) \le_{\mathcal{E}} e$ (lifting from boundary and restricting is contractive).
<!-- See Note [Adjoint Restrict-CoRestrict Galois Connections] [ref:note-galois-connection-stalks] -->
---
## 3. Module Architecture & Repertoire Breadth
The package exports 8 modules structured cleanly around algebraic logic and defunctionalization:
| Module | Primary Types & Typeclasses | Architectural Purpose |
| :--- | :--- | :--- |
| [`Gargamelle.Logic.Contract`](src/Gargamelle/Logic/Contract.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-logic/docs/Gargamelle-Logic-Contract.html)) | [`AGContract`](src/Gargamelle/Logic/Contract.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-logic/docs/Gargamelle-Logic-Contract.html#t:AGContract)), [`contract`](src/Gargamelle/Logic/Contract.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-logic/docs/Gargamelle-Logic-Contract.html#v:contract)), [`verifyCircularAG`](src/Gargamelle/Logic/Contract.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-logic/docs/Gargamelle-Logic-Contract.html#v:verifyCircularAG)) | Order-theoretic assume-guarantee contracts with functorial `Op` inversion. |
| [`Gargamelle.Logic.Defunctionalize`](src/Gargamelle/Logic/Defunctionalize.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-logic/docs/Gargamelle-Logic-Defunctionalize.html)) | [`ObsMor`](src/Gargamelle/Logic/Defunctionalize.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-logic/docs/Gargamelle-Logic-Defunctionalize.html#t:ObsMor)), [`evalObsMor`](src/Gargamelle/Logic/Defunctionalize.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-logic/docs/Gargamelle-Logic-Defunctionalize.html#v:evalObsMor)), [`inspectObsMor`](src/Gargamelle/Logic/Defunctionalize.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-logic/docs/Gargamelle-Logic-Defunctionalize.html#v:inspectObsMor)) | 100% observable morphism GADT replacing opaque `(->)` closures. |
| [`Gargamelle.Logic.Galois`](src/Gargamelle/Logic/Galois.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-logic/docs/Gargamelle-Logic-Galois.html)) | [`Galois`](src/Gargamelle/Logic/Galois.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-logic/docs/Gargamelle-Logic-Galois.html#t:Galois)), [`composeGalois`](src/Gargamelle/Logic/Galois.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-logic/docs/Gargamelle-Logic-Galois.html#v:composeGalois)), [`galoisObsMor`](src/Gargamelle/Logic/Galois.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-logic/docs/Gargamelle-Logic-Galois.html#v:galoisObsMor)) | Categorical Galois connections between vertex stalks and boundary edges. |
| [`Gargamelle.Logic.Signature`](src/Gargamelle/Logic/Signature.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-logic/docs/Gargamelle-Logic-Signature.html)) | [`LogicAST`](src/Gargamelle/Logic/Signature.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-logic/docs/Gargamelle-Logic-Signature.html#t:LogicAST)), [`UniversalAlgebraSig`](src/Gargamelle/Logic/Signature.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-logic/docs/Gargamelle-Logic-Signature.html#t:UniversalAlgebraSig)), [`Entailment`](src/Gargamelle/Logic/Signature.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-logic/docs/Gargamelle-Logic-Signature.html#t:Entailment)) | Flat, non-recursive $O(N)$ first-order logic sentences and Lawvere signatures. |
| [`Gargamelle.Logic.Order`](src/Gargamelle/Logic/Order.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-logic/docs/Gargamelle-Logic-Order.html)) | [`HeytingLattice`](src/Gargamelle/Logic/Order.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-logic/docs/Gargamelle-Logic-Order.html#t:HeytingLattice)), [`BoundedLattice`](src/Gargamelle/Logic/Order.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-logic/docs/Gargamelle-Logic-Order.html#t:BoundedLattice)) | Re-exports bundled order-theoretic lattices and Heyting algebras. |
| [`Gargamelle.Logic.Hole`](src/Gargamelle/Logic/Hole.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-logic/docs/Gargamelle-Logic-Hole.html)) | [`HoleSpec`](src/Gargamelle/Logic/Hole.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-logic/docs/Gargamelle-Logic-Hole.html#t:HoleSpec)), [`mkHoleSpec`](src/Gargamelle/Logic/Hole.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-logic/docs/Gargamelle-Logic-Hole.html#v:mkHoleSpec)) | Contextual Hole $E[\square_\tau]$ specifications carrying raw gangue and contracts. |
| [`Gargamelle.Logic.MPST`](src/Gargamelle/Logic/MPST.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-logic/docs/Gargamelle-Logic-MPST.html)) | [`GlobalType`](src/Gargamelle/Logic/MPST.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-logic/docs/Gargamelle-Logic-MPST.html#t:GlobalType)), [`LocalType`](src/Gargamelle/Logic/MPST.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-logic/docs/Gargamelle-Logic-MPST.html#t:LocalType)), [`Role`](src/Gargamelle/Logic/MPST.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-logic/docs/Gargamelle-Logic-MPST.html#t:Role)) | Multiparty session type choreographies and local role projections. |
| [`Gargamelle.Logic.Syntax`](src/Gargamelle/Logic/Syntax.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-logic/docs/Gargamelle-Logic-Syntax.html)) | — | Convenience umbrella re-exporting `Signature` and `Defunctionalize`. |
---
## 4. Executable Worked Examples
### 4.1 Order-Theoretic Contract Composition
```haskell
module ExampleContract where
import Algebra.Lattice (Lattice(..))
import Gargamelle.Logic.Contract
-- Define two boolean contracts
-- C1 assumes False (strictest requirement), guarantees True (strongest promise)
-- C2 assumes True (weak requirement), guarantees False (weak promise)
exampleRefine :: (Bool, Bool)
exampleRefine =
let c1 = contract False True
c2 = contract True False
refined = c1 /\ c2
in (getAssumption refined, getGuarantee refined)
-- Evaluates to (True, False):
-- Assumption was weakened (False \/ True = True)
-- Guarantee was strengthened (True /\ False = False)
```
### 4.2 Observable Morphism Pipeline Inspection
```haskell
module ExampleObsMor where
import Control.Category (Category(..))
import Prelude hiding (id, (.))
import Gargamelle.Logic.Defunctionalize
-- Compose a multi-stage data transformation
pipeline :: ObsMor Int String
pipeline =
SymbolicStep "showResult" show
. SymbolicStep "double" (* 2)
. SymbolicStep "validatePositive" (\x -> if x >= 0 then x else 0)
-- Statically inspect steps without running any evaluation
steps :: [String]
steps = inspectObsMor pipeline
-- Evaluates to: ["Step:validatePositive", "Step:double", "Step:showResult"]
-- Run the compiled function
result :: String
result = evalObsMor pipeline 21 -- "42"
```
---
## 5. Integration Points & Subsystem Boundaries
`gargamelle-logic` resides at **Tier 2 (Semantic Foundations)** of the monorepo architecture:
```
┌────────────────────────────────────────────────────────┐
│ Downstream Consumers │
│ - gargamelle-model: ObsMor in Verifier AST & Evidence │
│ - gargamelle-core: Institutions, Weaving, Signatures │
│ - gargamelle-fol: Hyperdoctrines, SMT Pipe │
│ - gargamelle-sheaf: Cellular Sheaf Restrictions │
└──────────────────────────▲─────────────────────────────┘
│
[gargamelle-logic]
│
┌──────────────────────────▼─────────────────────────────┐
│ Upstream Substrates │
│ - lattices (>= 2.2): Heyting algebras, Op functor │
│ - profunctors (>= 5.6): Strong, Choice, Category │
│ - polytropos-core (>= 0.1.0.1): Open records/variants │
└────────────────────────────────────────────────────────┘
```
---
## 6. Diagnostic & Troubleshooting Guide
### 6.1 Refinement Direction Inversion Errors
- **Symptom:** Composing contracts results in an unexpectedly strict assumption or relaxed guarantee.
- **Root Cause:** Attempting to manually invert assumptions (e.g. `not a`) instead of using `Op a`.
- **Remedy:** Use `contract a g` smart constructor and standard meet `c1 /\ c2`. The `Op` wrapper mechanically maps `/\` to join `\/` on assumptions.
### 6.2 Opaque Closure Contamination
- **Symptom:** An autonomous agent or verifier is unable to explain or serialize a transformation pipeline.
- **Root Cause:** Introducing raw Haskell functions `(a -> b)` or `Kleisli m a b` directly into signatures instead of `ObsMor a b`.
- **Remedy:** Wrap all custom logic into `SymbolicStep "step-name" fn` or use the standard category and profunctor combinators (`first'`, `left'`).
---
*Part of the [Gargamelle Verification Suite](../../README.md).*