gargamelle-fol — First-Order Logic Institution, Hyperdoctrines & Streaming Z3 SMT-LIB2

1. Executive Summary & Problem Framing

Predicate logic with quantifiers and relational constraints is fundamental to system verification, contract refinement, and theorem proving. However, embedding first-order logic (FOL) into modern multi-agent synthesis loops introduces major architectural hurdles:

1. FFI Brittleness & ABI Drift: Direct C/C++ FFI bindings to solvers like Z3 cause crashes across varying GHC versions (9.6–9.14) and complicate packaging across Nix, Stack, and Cabal.
2. Opaque Solver Outputs: Traditional solver interfaces return bare booleans (Sat/Unsat), discarding the countermodel witnesses necessary for automated fault repair and inductive learning.
3. Context Weakening & Quantifier Inconsistency: Ad-hoc substitution engines frequently introduce variable capture and fail to preserve the adjunction laws governing universal (\(\forall\)) and existential (\(\exists\)) quantifiers.

gargamelle-fol resolves these issues via rigorous categorical foundations and POSIX streaming:

• First-Order Institution: Embeds FOL into the Goguen-Burstall framework, supporting Herbrand universe evaluation and signature morphisms.
• Lawvere Hyperdoctrines: Formalizes quantifiers functorially as adjoints (\(\exists_t \dashv t^* \dashv \forall_t\)) to substitution functors over context categories.
• Streaming SMT-LIB2 Pipe: Emits standard SMT-LIB2 scripts streamed over POSIX pipes directly to host Z3 without FFI overhead.
• Structured Evidence Extraction: Automatically transforms Z3 countermodels into inspectable Counterexample witnesses and verified proofs into VerifiedSection.

2. Mathematical Foundations & Theoretical Invariants

2.1 Categorical Hyperdoctrine Quantifier Adjunctions

In Lawvere's categorical logic, a First-Order Hyperdoctrine is a functor \(\mathcal{P} : \mathbf{C}^{\mathrm{op}} \to \mathbf{HeytAlg}\) indexing propositional fibers over a cartesian category of contexts \(\mathbf{C}\):

                       P(X × Y) (Fiber over extended context)
                       ▲      ▲
         Substitution  │      │  Universal Quantifier
          π* (Pullback)│      │  ∀_π (Right Adjoint)
                       │      ▼
                         P(X)   (Fiber over base context)

1. Pullback (Substitution): For any projection or term substitution \(\pi : X \times Y \to X\), the contravariant functorial action \(\pi^* : \mathcal{P}(X) \to \mathcal{P}(X \times Y)\) models context weakening.
2. Existential Quantifier as Left Adjoint: \[\exists_\pi \dashv \pi^* \iff (\exists_\pi(\varphi) \le \psi \iff \varphi \le \pi^*(\psi))\]
3. Universal Quantifier as Right Adjoint: \[\pi^* \dashv \forall_\pi \iff (\pi^*(\psi) \le \varphi \iff \psi \le \forall_\pi(\varphi))\]
4. Beck-Chevalley Invariance: For any pullback square in \(\mathbf{C}\), the canonical comparison between quantification and substitution commutes.

2.2 Streaming SMT-LIB2 Piping & Dual Refutation

Interfacing with external solvers avoids foreign function bindings by utilizing streaming POSIX pipes:

┌─────────────────────┐       formulaToSMTLib        ┌───────────────────────┐
│ FirstOrder Formula  │ ───────────────────────────► │ SMT-LIB2 Script       │
└─────────────────────┘                              └───────────┬───────────┘
                                                                 │
                                                      readProcessWithExitCode
                                                                 ▼
┌─────────────────────┐        parseZ3Model          ┌───────────────────────┐
│ Evidence Witness    │ ◄─────────────────────────── │ Host Z3 stdout/stderr │
│ (Counterexample /   │                              │ (sat / unsat)         │
│  VerifiedSection)   │                              └───────────────────────┘
└─────────────────────┘

• Dual Refutation: To verify that formula \(\varphi\) is valid, verifyValidityZ3 tests whether \(\neg \varphi\) is unsatisfiable.
• Evidence Soundness:
  • \(\neg \varphi\) is \(\mathrm{UNSAT} \implies \varphi\) holds universally, producing VerifiedSection.
  • \(\neg \varphi\) is \(\mathrm{SAT} \implies\) Z3 produces a model \(\mathcal{M} \models \neg \varphi\). Parsing this model yields a concrete Counterexample containing the exact falsifying variable assignments.

3. Module Architecture & Repertoire Breadth

The package exports 4 modules providing complete first-order verification and solver piping:

4. Executable Worked Examples

4.1 Automated Validity Verification via Z3 Pipe

{-# LANGUAGE DataKinds #-}

module ExampleZ3Validity where

import Data.Proxy (Proxy(..))
import FirstOrder (Formula(..))
import Gargamelle.FOL.Z3 (verifyValidityZ3)
import Gargamelle.Model.Satisfaction (Evidence(..))

-- Verify the Law of Excluded Middle: (P \/ not P)
verifyLEM :: IO ()
verifyLEM = do
  let p = Pred (Proxy @"P") []
      tautology = Or p (Not p)
  evidence <- verifyValidityZ3 tautology
  case evidence of
    VerifiedSection -> putStrLn "Formally verified: tautology holds across all models."
    Counterexample sym _witness -> putStrLn $ "Disproved: countermodel found in " ++ sym

4.2 Satisfiability Model Extraction

{-# LANGUAGE DataKinds #-}

module ExampleZ3Model where

import Data.Proxy (Proxy(..))
import FirstOrder (Formula(..))
import Gargamelle.FOL.Z3 (checkFormulaZ3, SMTResult(..))

-- Find satisfying model for (P /\ not Q)
findWitness :: IO ()
findWitness = do
  let p = Pred (Proxy @"P") []
      q = Pred (Proxy @"Q") []
      formula = And p (Not q)
  result <- checkFormulaZ3 formula
  case result of
    Sat model -> putStrLn $ "Satisfying model: " ++ show model
    Unsat     -> putStrLn "Formula is unsatisfiable."
    Unknown e -> putStrLn $ "Solver inconclusive: " ++ e

5. Integration Points & Subsystem Boundaries

gargamelle-fol serves at Tier 3 (Logic Engine) of the architecture:

┌────────────────────────────────────────────────────────┐
│               Downstream Consumers                     │
│  - gargamelle-workflow: CEGIS Induction & SMT Guidance │
│  - gargamelle-persistence: Logging SMT Run Records     │
└──────────────────────────▲─────────────────────────────┘
                           │
                  [gargamelle-fol]
                           │
┌──────────────────────────▼─────────────────────────────┐
│               Upstream Substrates                      │
│  - gargamelle-core: Institutions, Signatures           │
│  - gargamelle-model: Evidence, Verifier AST            │
│  - Host OS: /usr/bin/z3 executable (POSIX pipe)        │
└────────────────────────────────────────────────────────┘

6. Diagnostic & Troubleshooting Guide

6.1 z3 Binary Not Found

• Symptom: solveZ3Raw crashes with readProcess: z3: does not exist (No such file or directory).
• Root Cause: Host system lacks z3 on $PATH.
• Remedy: Ensure z3 is installed via system packages (apt install z3 or nix-shell -p z3).

6.2 Unknown SMT Results

• Symptom: verifyValidityZ3 returns Counterexample "Z3-Unknown" "...".
• Root Cause: Nonlinear arithmetic, unbounded quantifiers, or timeout limits triggered Z3's incomplete heuristic engine.
• Remedy: Skolemize existential quantifiers or restrict assertions to decidable SMT fragments (e.g. QF_LIA / QF_UF).

Part of the Gargamelle Verification Suite.