gargamelle-logic — Pure Syntax, Order-Theoretic Contracts & Defunctionalized Morphisms

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

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\]

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

3. Module Architecture & Repertoire Breadth

The package exports 8 modules structured cleanly around algebraic logic and defunctionalization:

4. Executable Worked Examples

4.1 Order-Theoretic Contract Composition

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

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.