gargamelle-logic (empty) → 0.1.0.0

raw patch · 13 files changed

+1015/−0 lines, 13 filesdep +basedep +constraintsdep +containers

Dependencies added: base, constraints, containers, gargamelle-logic, hspec, lattices, polytropos-core, profunctors

Files

• CHANGELOG.md +7/−0
• LICENSE +189/−0
• README.md +176/−0
• gargamelle-logic.cabal +67/−0
• src/Gargamelle/Logic/Contract.hs +129/−0
• src/Gargamelle/Logic/Defunctionalize.hs +130/−0
• src/Gargamelle/Logic/Galois.hs +64/−0
• src/Gargamelle/Logic/Hole.hs +16/−0
• src/Gargamelle/Logic/MPST.hs +36/−0
• src/Gargamelle/Logic/Order.hs +18/−0
• src/Gargamelle/Logic/Signature.hs +85/−0
• src/Gargamelle/Logic/Syntax.hs +7/−0
• test/Main.hs +91/−0

@@ -0,0 +1,7 @@+# Changelog for gargamelle-logic++## 0.1.0.0 — Initial Release++- Pure syntax, defunctionalized arrows, order theory, and refinement calculi.+- Signature definitions and syntax AST representations.+- Galois connections, behavioral contracts, holes, and MPST session types.

@@ -0,0 +1,189 @@+EUROPEAN UNION PUBLIC LICENCE v. 1.2+EUPL © the European Union 2007, 2016++This European Union Public Licence (the ‘EUPL’) applies to the Work (as defined below) which is provided under the+terms of this Licence. Any use of the Work, other than as authorised under this Licence is prohibited (to the extent such+use is covered by a right of the copyright holder of the Work).+The Work is provided under the terms of this Licence when the Licensor (as defined below) has placed the following+notice immediately following the copyright notice for the Work:+                          Licensed under the EUPL+or has expressed by any other means his willingness to license under the EUPL.++1.Definitions+In this Licence, the following terms have the following meaning:+— ‘The Licence’:this Licence.+— ‘The Original Work’:the work or software distributed or communicated by the Licensor under this Licence, available+as Source Code and also as Executable Code as the case may be.+— ‘Derivative Works’:the works or software that could be created by the Licensee, based upon the Original Work or+modifications thereof. This Licence does not define the extent of modification or dependence on the Original Work+required in order to classify a work as a Derivative Work; this extent is determined by copyright law applicable in+the country mentioned in Article 15.+— ‘The Work’:the Original Work or its Derivative Works.+— ‘The Source Code’:the human-readable form of the Work which is the most convenient for people to study and+modify.+— ‘The Executable Code’:any code which has generally been compiled and which is meant to be interpreted by+a computer as a program.+— ‘The Licensor’:the natural or legal person that distributes or communicates the Work under the Licence.+— ‘Contributor(s)’:any natural or legal person who modifies the Work under the Licence, or otherwise contributes to+the creation of a Derivative Work.+— ‘The Licensee’ or ‘You’:any natural or legal person who makes any usage of the Work under the terms of the+Licence.+— ‘Distribution’ or ‘Communication’:any act of selling, giving, lending, renting, distributing, communicating,+transmitting, or otherwise making available, online or offline, copies of the Work or providing access to its essential+functionalities at the disposal of any other natural or legal person.++2.Scope of the rights granted by the Licence+The Licensor hereby grants You a worldwide, royalty-free, non-exclusive, sublicensable licence to do the following, for+the duration of copyright vested in the Original Work:+— use the Work in any circumstance and for all usage,+— reproduce the Work,+— modify the Work, and make Derivative Works based upon the Work,+— communicate to the public, including the right to make available or display the Work or copies thereof to the public+and perform publicly, as the case may be, the Work,+— distribute the Work or copies thereof,+— lend and rent the Work or copies thereof,+— sublicense rights in the Work or copies thereof.+Those rights can be exercised on any media, supports and formats, whether now known or later invented, as far as the+applicable law permits so.+In the countries where moral rights apply, the Licensor waives his right to exercise his moral right to the extent allowed+by law in order to make effective the licence of the economic rights here above listed.+The Licensor grants to the Licensee royalty-free, non-exclusive usage rights to any patents held by the Licensor, to the+extent necessary to make use of the rights granted on the Work under this Licence.++3.Communication of the Source Code+The Licensor may provide the Work either in its Source Code form, or as Executable Code. If the Work is provided as+Executable Code, the Licensor provides in addition a machine-readable copy of the Source Code of the Work along with+each copy of the Work that the Licensor distributes or indicates, in a notice following the copyright notice attached to+the Work, a repository where the Source Code is easily and freely accessible for as long as the Licensor continues to+distribute or communicate the Work.++4.Limitations on copyright+Nothing in this Licence is intended to deprive the Licensee of the benefits from any exception or limitation to the+exclusive rights of the rights owners in the Work, of the exhaustion of those rights or of other applicable limitations+thereto.++5.Obligations of the Licensee+The grant of the rights mentioned above is subject to some restrictions and obligations imposed on the Licensee. Those+obligations are the following:++Attribution right: The Licensee shall keep intact all copyright, patent or trademarks notices and all notices that refer to+the Licence and to the disclaimer of warranties. The Licensee must include a copy of such notices and a copy of the+Licence with every copy of the Work he/she distributes or communicates. The Licensee must cause any Derivative Work+to carry prominent notices stating that the Work has been modified and the date of modification.++Copyleft clause: If the Licensee distributes or communicates copies of the Original Works or Derivative Works, this+Distribution or Communication will be done under the terms of this Licence or of a later version of this Licence unless+the Original Work is expressly distributed only under this version of the Licence — for example by communicating+‘EUPL v. 1.2 only’. The Licensee (becoming Licensor) cannot offer or impose any additional terms or conditions on the+Work or Derivative Work that alter or restrict the terms of the Licence.++Compatibility clause: If the Licensee Distributes or Communicates Derivative Works or copies thereof based upon both+the Work and another work licensed under a Compatible Licence, this Distribution or Communication can be done+under the terms of this Compatible Licence. For the sake of this clause, ‘Compatible Licence’ refers to the licences listed+in the appendix attached to this Licence. Should the Licensee's obligations under the Compatible Licence conflict with+his/her obligations under this Licence, the obligations of the Compatible Licence shall prevail.++Provision of Source Code: When distributing or communicating copies of the Work, the Licensee will provide+a machine-readable copy of the Source Code or indicate a repository where this Source will be easily and freely available+for as long as the Licensee continues to distribute or communicate the Work.+Legal Protection: This Licence does not grant permission to use the trade names, trademarks, service marks, or names+of the Licensor, except as required for reasonable and customary use in describing the origin of the Work and+reproducing the content of the copyright notice.++6.Chain of Authorship+The original Licensor warrants that the copyright in the Original Work granted hereunder is owned by him/her or+licensed to him/her and that he/she has the power and authority to grant the Licence.+Each Contributor warrants that the copyright in the modifications he/she brings to the Work are owned by him/her or+licensed to him/her and that he/she has the power and authority to grant the Licence.+Each time You accept the Licence, the original Licensor and subsequent Contributors grant You a licence to their contributions+to the Work, under the terms of this Licence.++7.Disclaimer of Warranty+The Work is a work in progress, which is continuously improved by numerous Contributors. It is not a finished work+and may therefore contain defects or ‘bugs’ inherent to this type of development.+For the above reason, the Work is provided under the Licence on an ‘as is’ basis and without warranties of any kind+concerning the Work, including without limitation merchantability, fitness for a particular purpose, absence of defects or+errors, accuracy, non-infringement of intellectual property rights other than copyright as stated in Article 6 of this+Licence.+This disclaimer of warranty is an essential part of the Licence and a condition for the grant of any rights to the Work.++8.Disclaimer of Liability+Except in the cases of wilful misconduct or damages directly caused to natural persons, the Licensor will in no event be+liable for any direct or indirect, material or moral, damages of any kind, arising out of the Licence or of the use of the+Work, including without limitation, damages for loss of goodwill, work stoppage, computer failure or malfunction, loss+of data or any commercial damage, even if the Licensor has been advised of the possibility of such damage. However,+the Licensor will be liable under statutory product liability laws as far such laws apply to the Work.++9.Additional agreements+While distributing the Work, You may choose to conclude an additional agreement, defining obligations or services+consistent with this Licence. However, if accepting obligations, You may act only on your own behalf and on your sole+responsibility, not on behalf of the original Licensor or any other Contributor, and only if You agree to indemnify,+defend, and hold each Contributor harmless for any liability incurred by, or claims asserted against such Contributor by+the fact You have accepted any warranty or additional liability.++10.Acceptance of the Licence+The provisions of this Licence can be accepted by clicking on an icon ‘I agree’ placed under the bottom of a window+displaying the text of this Licence or by affirming consent in any other similar way, in accordance with the rules of+applicable law. Clicking on that icon indicates your clear and irrevocable acceptance of this Licence and all of its terms+and conditions.+Similarly, you irrevocably accept this Licence and all of its terms and conditions by exercising any rights granted to You+by Article 2 of this Licence, such as the use of the Work, the creation by You of a Derivative Work or the Distribution+or Communication by You of the Work or copies thereof.++11.Information to the public+In case of any Distribution or Communication of the Work by means of electronic communication by You (for example,+by offering to download the Work from a remote location) the distribution channel or media (for example, a website)+must at least provide to the public the information requested by the applicable law regarding the Licensor, the Licence+and the way it may be accessible, concluded, stored and reproduced by the Licensee.++12.Termination of the Licence+The Licence and the rights granted hereunder will terminate automatically upon any breach by the Licensee of the terms+of the Licence.+Such a termination will not terminate the licences of any person who has received the Work from the Licensee under+the Licence, provided such persons remain in full compliance with the Licence.++13.Miscellaneous+Without prejudice of Article 9 above, the Licence represents the complete agreement between the Parties as to the+Work.+If any provision of the Licence is invalid or unenforceable under applicable law, this will not affect the validity or+enforceability of the Licence as a whole. Such provision will be construed or reformed so as necessary to make it valid+and enforceable.+The European Commission may publish other linguistic versions or new versions of this Licence or updated versions of+the Appendix, so far this is required and reasonable, without reducing the scope of the rights granted by the Licence.+New versions of the Licence will be published with a unique version number.+All linguistic versions of this Licence, approved by the European Commission, have identical value. Parties can take+advantage of the linguistic version of their choice.++14.Jurisdiction+Without prejudice to specific agreement between parties,+— any litigation resulting from the interpretation of this License, arising between the European Union institutions,+bodies, offices or agencies, as a Licensor, and any Licensee, will be subject to the jurisdiction of the Court of Justice+of the European Union, as laid down in article 272 of the Treaty on the Functioning of the European Union,+— any litigation arising between other parties and resulting from the interpretation of this License, will be subject to+the exclusive jurisdiction of the competent court where the Licensor resides or conducts its primary business.++15.Applicable Law+Without prejudice to specific agreement between parties,+— this Licence shall be governed by the law of the European Union Member State where the Licensor has his seat,+resides or has his registered office,+— this licence shall be governed by Belgian law if the Licensor has no seat, residence or registered office inside+a European Union Member State.++Appendix++‘Compatible Licences’ according to Article 5 EUPL are:+— GNU General Public License (GPL) v. 2, v. 3+— GNU Affero General Public License (AGPL) v. 3+— Open Software License (OSL) v. 2.1, v. 3.0+— Eclipse Public License (EPL) v. 1.0+— CeCILL v. 2.0, v. 2.1+— Mozilla Public Licence (MPL) v. 2+— GNU Lesser General Public Licence (LGPL) v. 2.1, v. 3+— Creative Commons Attribution-ShareAlike v. 3.0 Unported (CC BY-SA 3.0) for works other than software+— European Union Public Licence (EUPL) v. 1.1, v. 1.2+— Québec Free and Open-Source Licence — Reciprocity (LiLiQ-R) or Strong Reciprocity (LiLiQ-R+).++The European Commission may update this Appendix to later versions of the above licences without producing+a new version of the EUPL, as long as they provide the rights granted in Article 2 of this Licence and protect the+covered Source Code from exclusive appropriation.+All other changes or additions to this Appendix require the production of a new EUPL version.

@@ -0,0 +1,176 @@+# `gargamelle-logic` — Pure Syntax, Order-Theoretic Contracts & Defunctionalized Morphisms++[![Haskell](https://img.shields.io/badge/Language-Haskell2010-purple.svg)](https://haskell.org)+[![License: EUPL-1.2](https://img.shields.io/badge/License-EUPL--1.2-blue.svg)](https://spdx.org/licenses/EUPL-1.2.html)+[![Tier 2 Substrate](https://img.shields.io/badge/Tier-2%20Substrate%20%26%20Semantics-teal.svg)](../../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).*

@@ -0,0 +1,67 @@+cabal-version: 3.0+name: gargamelle-logic+version: 0.1.0.0+synopsis: Pure syntax, order theory, and refinement calculi for Gargamelle+description:+  Pure syntax, defunctionalized arrows, order theory, and refinement+  calculi for the Gargamelle institutional synthesis framework.+  Provides Galois connections, behavioral contracts, holes, and MPST+  multiparty session types.+license: EUPL-1.2+license-file: LICENSE+author: Nadia Yvette Chambers+maintainer: nadia.yvette.chambers@ik.me+category: Logic+homepage: https://github.com/NadiaYvette/gargamelle+bug-reports: https://github.com/NadiaYvette/gargamelle/issues+extra-doc-files:+  README.md+  CHANGELOG.md+build-type: Simple+tested-with:+  GHC == 9.6.7,+  GHC == 9.8.4,+  GHC == 9.10.3,+  GHC == 9.12.4,+  GHC == 9.14.1++source-repository head+  type: git+  location: https://github.com/NadiaYvette/gargamelle+  subdir: packages/gargamelle-logic++library+  exposed-modules:+    Gargamelle.Logic.Signature+    Gargamelle.Logic.Syntax+    Gargamelle.Logic.Defunctionalize+    Gargamelle.Logic.Order+    Gargamelle.Logic.Galois+    Gargamelle.Logic.Contract+    Gargamelle.Logic.Hole+    Gargamelle.Logic.MPST+  hs-source-dirs: src+  default-language: Haskell2010+  ghc-options: -Wall -Wcompat -Wredundant-constraints+  build-depends:+    base >= 4.18 && < 5,+    containers >= 0.6 && < 0.9,+    polytropos-core >= 0.1.0.1 && < 0.2,+    lattices >= 2.2 && < 2.3,+    constraints >= 0.14 && < 0.15,+    profunctors >= 5.6 && < 5.7++test-suite tests+  type: exitcode-stdio-1.0+  main-is: Main.hs+  hs-source-dirs: test+  default-language: Haskell2010+  ghc-options: -Wall+  build-depends:+    base >= 4.18 && < 5,+    gargamelle-logic,+    polytropos-core >= 0.1.0.1 && < 0.2,+    lattices >= 2.2 && < 2.3,+    constraints >= 0.14 && < 0.15,+    profunctors >= 5.6 && < 5.7,+    hspec >= 2.10 && < 2.12

@@ -0,0 +1,129 @@+{-# LANGUAGE FlexibleContexts #-}++module Gargamelle.Logic.Contract+  ( AGContract(..)+  , contract+  , getAssumption+  , getGuarantee+  , deriveAGGalois+  , verifyCircularAG+  ) where++import Algebra.Lattice (Lattice(..), BoundedJoinSemiLattice(..), BoundedMeetSemiLattice(..))+import Algebra.Lattice.Op (Op(..))+import Algebra.Heyting (Heyting(..))+import Gargamelle.Logic.Defunctionalize (ObsMor(..))+import Gargamelle.Logic.Galois (Galois(..))++{- Note [Lattice Inversion via Op Dualization]+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~+[tag:note-lattice-op-dualization]+In formal verification and contract-based design, contract refinement+(C1 ⊑ C2, or meet C1 ∧ C2) means that C1 is a stricter, more capable specification+that can safely substitute for C2 in any environment.++For guarantees G, substitution requires strengthening: if C2 promised G2, C1 must+promise at least G2 (i.e. G1 ⊑ G2, which in standard logic or lattice refinement+corresponds to meet G1 ∧ G2).++For assumptions A, the direction of refinement is fundamentally reversed: if C2+required the environment to satisfy demanding assumption A2, a more capable component+C1 should require LESS of its environment (i.e. accept a wider range of behaviors,+A2 ⊑ A1, or A1 ∨ A2 in the base lattice).++Rather than writing manual ad-hoc case analyses or bifurcated order checks, Gargamelle+exploits the functorial order-dual operator 'Algebra.Lattice.Op' from the @lattices@+package:+  Op a ∧ Op b = Op (a ∨ b)+  Op a ∨ Op b = Op (a ∧ b)++By wrapping assumptions inside 'Op a', contract refinement becomes the standard product+meet:+  (Op A1, G1) ∧ (Op A2, G2) = (Op (A1 ∨ A2), G1 ∧ G2)++This mechanically weakens assumptions (expands admitted environments) while simultaneously+strengthening guarantees (restricts emitted behaviors) with zero runtime branching or+heuristic case splits.+-}++{- Note [Circular Assume-Guarantee Soundness]+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~+[tag:note-circular-ag-soundness]+When two components C1 = (A1, G1) and C2 = (A2, G2) interact concurrently across a shared+interface, mutual dependencies can lead to apparent cyclic reasoning:+  - C1 guarantees G1 provided C2 satisfies assumption A1.+  - C2 guarantees G2 provided C1 satisfies assumption A2.++In a Heyting algebra or intuitionistic logic lattice, circular reasoning is sound if and+only if each component's guarantee discharges the other component's assumption under the+shared interface context:+  dir1 = (A1 ∧ G2) ⟹ G1+  dir2 = (A2 ∧ G1) ⟹ G2++Sound composition holds when both entailments evaluate to the top element of the lattice:+  (dir1 ∧ dir2) == ⊤++If either component fails to establish its guarantee under the environment provided by+its partner, the circular check evaluates to a non-top element, pinpointing an interface+mismatch before deployment.+-}++-- | Assume-Guarantee contract using 'Algebra.Lattice.Op' from @lattices@.+--+-- See Note [Lattice Inversion via Op Dualization] [ref:note-lattice-op-dualization].+--+-- Because refinement is meet (/\), wrapping assumptions in 't:Op' ensures that+-- contract refinement automatically weakens assumptions (as joins \/ in the base lattice)+-- while strengthening guarantees (as meets /\ in the base lattice).+data AGContract a g = AGContract+  { assumptions :: Op a+  , guarantees  :: g+  } deriving (Eq, Show)++-- | Smart constructor for AGContract.+contract :: a -> g -> AGContract a g+contract a = AGContract (Op a)++-- | Extract the raw assumption value.+getAssumption :: AGContract a g -> a+getAssumption (AGContract (Op a) _) = a++-- | Extract the guarantee value.+getGuarantee :: AGContract a g -> g+getGuarantee (AGContract _ g) = g++instance (Lattice a, Lattice g) => Lattice (AGContract a g) where+  AGContract a1 g1 /\ AGContract a2 g2 = AGContract (a1 /\ a2) (g1 /\ g2)+  AGContract a1 g1 \/ AGContract a2 g2 = AGContract (a1 \/ a2) (g1 \/ g2)++instance (BoundedMeetSemiLattice a, BoundedJoinSemiLattice a, BoundedMeetSemiLattice g)+         => BoundedMeetSemiLattice (AGContract a g) where+  top = AGContract (Op bottom) top++instance (BoundedMeetSemiLattice a, BoundedJoinSemiLattice g)+         => BoundedJoinSemiLattice (AGContract a g) where+  bottom = AGContract (Op top) bottom++-- | Lift component projections/liftings to an observable Galois connection on AGContracts.+deriveAGGalois+  :: (a1 -> a2) -> (a2 -> a1)+  -> (g1 -> g2) -> (g2 -> g1)+  -> Galois ObsMor (AGContract a1 g1) (AGContract a2 g2)+deriveAGGalois aRestrict aCoRestrict gRestrict gCoRestrict = Galois+  { restrict   = SymbolicStep "ag-restrict"   $ \(AGContract (Op a) g) -> AGContract (Op (aRestrict a)) (gRestrict g)+  , coRestrict = SymbolicStep "ag-coRestrict" $ \(AGContract (Op a) g) -> AGContract (Op (aCoRestrict a)) (gCoRestrict g)+  }++-- | Circular Assume-Guarantee Soundness Check on a shared interface:+-- Checks that (A1 /\ G2 ==> G1) /\ (A2 /\ G1 ==> G2) == top.+--+-- See Note [Circular Assume-Guarantee Soundness] [ref:note-circular-ag-soundness].+verifyCircularAG+  :: (Heyting l, Eq l)+  => AGContract l l+  -> AGContract l l+  -> Bool+verifyCircularAG (AGContract (Op a1) g1) (AGContract (Op a2) g2) =+  let dir1 = (a1 /\ g2) ==> g1+      dir2 = (a2 /\ g1) ==> g2+  in (dir1 /\ dir2) == top

@@ -0,0 +1,130 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE MultiParamTypeClasses #-}++module Gargamelle.Logic.Defunctionalize+  ( TyFun+  , type (~>)+  , Apply+  , SingSymbol(..)+  , ObsMor(..)+  , evalObsMor+  , inspectObsMor+  ) where++import Control.Category (Category(..))+import Data.Kind (Type)+import Data.Profunctor (Profunctor(..), Strong(..), Choice(..))+import Data.Bifunctor (first, second)+import Prelude hiding (id, (.))++-- ============================================================================+-- 1. TYPE-LEVEL DEFUNCTIONALIZATION (For PolyKinds Signature Morphisms)+-- ============================================================================++-- | Dummy type constructor representing a defunctionalized type-level function+-- from kind @k1@ to kind @k2@.+data TyFun (k1 :: Type) (k2 :: Type) :: Type++-- | Type-level arrow kind @k1 ~> k2@ that can be partially applied and passed+-- to typeclasses without triggering GHC's unsaturated type family restriction.+type (k1 :: Type) ~> (k2 :: Type) = TyFun k1 k2 -> Type++-- | Open evaluation type family interpreting defunctionalized symbols.+type family Apply (f :: k1 ~> k2) (x :: k1) :: k2++-- | Runtime Singleton witness for a defunctionalized type-level symbol,+-- allowing runtime code analyzers to inspect type-level signature mappings.+data SingSymbol (f :: k1 ~> k2) = SingSymbol+  { symbolName        :: String+  , mappedIdentifiers :: [(String, String)]+  } deriving (Eq, Show)++-- ============================================================================+-- 2. TERM-LEVEL OBSERVABLE MORPHISM GADT (Replaces Opaque `->` Closures)+-- ============================================================================++{- Note [Defunctionalized Observable Morphisms]+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~+[tag:note-defunctionalized-obsmor]+In standard Haskell architectures, transformations and signature morphisms are+represented as native function closures @(a -> b)@. However, Haskell function+closures are completely opaque:+  1. A function closure cannot be inspected: an autonomous agent or verifier cannot+     determine whether @f@ reads a database, modifies a field, or drops information.+  2. A function closure cannot be serialized or translated: it cannot be mapped to an+     SMT-LIB2 relation or emitted into an explainable proof certificate.+  3. A function closure prevents algebraic rewriting: categorical laws like+     @f . id = f@ or @first (g . h) = first g . first h@ cannot be applied at compile+     or run time.++To resolve this opacity, 'ObsMor a b' defunctionalizes morphism arrows into a first-class+GADT. Every pipeline step—whether an identity, a composition, a tagged field projection,+a tagged variant injection, or a profunctor splitting—is represented as an inspectable term.++Autonomous reasoning engines can:+  - Statically inspect the transformation plan via 'inspectObsMor' without evaluating code.+  - Compile the AST to native executable code via 'evalObsMor'.+  - Verify functorial and profunctorial preservation across institutional boundaries.+-}++-- | Deeply embedded, inspectable morphism AST replacing native @(->)@.+--+-- See Note [Defunctionalized Observable Morphisms] [ref:note-defunctionalized-obsmor].+--+-- Autonomous agents can pattern-match on @ObsMor@ to extract symbolic dependencies,+-- or compile it to a native Haskell function via @evalObsMor@.+data ObsMor a b where+  IdMor        :: ObsMor a a+  CompMor      :: ObsMor b c -> ObsMor a b -> ObsMor a c+  ProjectTag   :: String -> (a -> b) -> ObsMor a b+  InjectTag    :: String -> (a -> b) -> ObsMor a b+  FirstMor     :: ObsMor a b -> ObsMor (a, c) (b, c)+  SecondMor    :: ObsMor a b -> ObsMor (c, a) (c, b)+  LeftMor      :: ObsMor a b -> ObsMor (Either a c) (Either b c)+  RightMor     :: ObsMor a b -> ObsMor (Either c a) (Either c b)+  SymbolicStep :: String -> (a -> b) -> ObsMor a b++instance Category ObsMor where+  id  = IdMor+  (.) = CompMor++instance Profunctor ObsMor where+  dimap f g m = SymbolicStep "post" g . m . SymbolicStep "pre" f++instance Strong ObsMor where+  first'  = FirstMor+  second' = SecondMor++instance Choice ObsMor where+  left'  = LeftMor+  right' = RightMor++-- | Interpret the observable morphism AST as an executable Haskell function.+evalObsMor :: ObsMor a b -> (a -> b)+evalObsMor IdMor                    = id+evalObsMor (CompMor g f)            = evalObsMor g . evalObsMor f+evalObsMor (ProjectTag _ f)         = f+evalObsMor (InjectTag _ f)          = f+evalObsMor (FirstMor f)             = first (evalObsMor f)+evalObsMor (SecondMor f)            = second (evalObsMor f)+evalObsMor (LeftMor f)              = either (Left . evalObsMor f) Right+evalObsMor (RightMor f)             = fmap (evalObsMor f)+evalObsMor (SymbolicStep _ fn)      = fn++-- | Extract a structural trace of all transformations inside a morphism without running it.+inspectObsMor :: ObsMor a b -> [String]+inspectObsMor IdMor                = ["id"]+inspectObsMor (CompMor g f)        = inspectObsMor f ++ inspectObsMor g+inspectObsMor (ProjectTag tag _)   = ["ProjectTag:" ++ tag]+inspectObsMor (InjectTag tag _)    = ["InjectTag:" ++ tag]+inspectObsMor (FirstMor f)         = map ("First(" ++) (inspectObsMor f)+inspectObsMor (SecondMor f)        = map ("Second(" ++) (inspectObsMor f)+inspectObsMor (LeftMor f)          = map ("Left(" ++) (inspectObsMor f)+inspectObsMor (RightMor f)         = map ("Right(" ++) (inspectObsMor f)+inspectObsMor (SymbolicStep tag _) = ["Step:" ++ tag]

@@ -0,0 +1,64 @@+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}++module Gargamelle.Logic.Galois+  ( Galois(..)+  , composeGalois+  , galoisObsMor+  ) where++import Data.Kind (Type)+import Control.Category (Category(..))+import Gargamelle.Logic.Defunctionalize (ObsMor(..))+import Prelude hiding (id, (.))++{- Note [Adjoint Restrict-CoRestrict Galois Connections]+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~+[tag:note-galois-connection-stalks]+In sheaf-theoretic program analysis and cell complex verification, individual components+or subsystems reside at vertices (v ∈ V), while shared interfaces, protocol buses, and+network channels reside at boundary edges (e ∈ E).++To transfer contracts and refinement obligations soundly between interior component stalks+and boundary edge stalks, we employ a Galois connection (an adjunction between posets):+  restrict ⊣ coRestrict   (i.e. α ⊣ γ)++Formally, for vertex state/contract v ∈ V and boundary state/contract e ∈ E:+  restrict(v) ≤_E e   ⟺   v ≤_V coRestrict(e)++Where:+  1. 'restrict' (lower adjoint α) projects an interior vertex contract onto the shared+     boundary edge. It represents the interface footprint exposed to the outside world.+  2. 'coRestrict' (upper adjoint γ) takes a boundary guarantee or requirement and lifts it+     back into the interior vertex state space.++Adjunction invariants:+  - Unit:     v ≤_V coRestrict (restrict v)   (round-trip through boundary is an over-approximation)+  - Counit:   restrict (coRestrict e) ≤_E e   (round-trip from boundary is contractive)++By parameterizing 'Galois' over the underlying arrow category 'arr :: k -> k -> Type',+we can instantiate it with 'ObsMor', ensuring that interface projection and lifting+remain completely inspectable by autonomous agents and SMT solvers without executing+opaque closures.+-}++-- | Galois connection (restrict ⊣ coRestrict) between a Vertex Stalk and an Edge Stalk,+-- parameterized over the arrow category @arr@.+--+-- See Note [Adjoint Restrict-CoRestrict Galois Connections] [ref:note-galois-connection-stalks].+data Galois (arr :: k -> k -> Type) vStalk eStalk = Galois+  { restrict   :: arr vStalk eStalk   -- ^ Lower adjoint α (projects specification to boundary)+  , coRestrict :: arr eStalk vStalk   -- ^ Upper adjoint γ (lifts boundary specification to vertex)+  }++-- | Compose two Galois connections in series.+composeGalois :: Category arr => Galois arr b c -> Galois arr a b -> Galois arr a c+composeGalois g2 g1 = Galois+  (restrict g2 . restrict g1)+  (coRestrict g1 . coRestrict g2)++-- | Construct an observable Galois connection from named projection/lifting functions.+galoisObsMor :: String -> (v -> e) -> (e -> v) -> Galois ObsMor v e+galoisObsMor label proj lift' = Galois+  (SymbolicStep (label ++ "-restrict") proj)+  (SymbolicStep (label ++ "-coRestrict") lift')

@@ -0,0 +1,16 @@+module Gargamelle.Logic.Hole+  ( HoleSpec(..)+  , mkHoleSpec+  ) where++-- | Contextual Hole E[□_τ] carrying its expected Assume-Guarantee contract+-- and unparsed gangue text for resilient parsing ("stope and winze" architecture).+data HoleSpec contract = HoleSpec+  { holeSpan     :: (Int, Int)+  , rawGangue    :: String+  , holeContract :: contract+  } deriving (Eq, Show)++-- | Smart constructor for HoleSpec.+mkHoleSpec :: (Int, Int) -> String -> contract -> HoleSpec contract+mkHoleSpec = HoleSpec

@@ -0,0 +1,36 @@+module Gargamelle.Logic.MPST+  ( Role(..)+  , Message(..)+  , GlobalType(..)+  , LocalType(..)+  ) where++-- | Participant role identifier in a multiparty protocol.+newtype Role = Role { getRole :: String }+  deriving (Eq, Show, Ord)++-- | Message label and payload sort.+data Message = Message+  { msgLabel :: String+  , msgSort  :: String+  } deriving (Eq, Show, Ord)++-- | Global session type representing the protocol choreography.+data GlobalType+  = GEnd+  | GComm Role Role Message GlobalType+  | GBranch Role Role [(Message, GlobalType)]+  | GRec String GlobalType+  | GVar String+  deriving (Eq, Show)++-- | Projected local session type for an individual participant role.+data LocalType+  = LEnd+  | LSend Role Message LocalType+  | LRecv Role Message LocalType+  | LSelect Role [(Message, LocalType)]+  | LBranch Role [(Message, LocalType)]+  | LRec String LocalType+  | LVar String+  deriving (Eq, Show)

@@ -0,0 +1,18 @@+{-# LANGUAGE ConstraintKinds #-}++module Gargamelle.Logic.Order+  ( Lattice(..)+  , BoundedJoinSemiLattice(..)+  , BoundedMeetSemiLattice(..)+  , BoundedLattice+  , Heyting(..)+  , HeytingLattice+  , Op(..)+  ) where++import Algebra.Lattice+import Algebra.Lattice.Op (Op(..))+import Algebra.Heyting (Heyting(..))++-- | Bundled constraint alias for a complete Heyting refinement lattice.+type HeytingLattice l = (Eq l, BoundedLattice l, Heyting l)

@@ -0,0 +1,85 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE RankNTypes #-}++module Gargamelle.Logic.Signature+  ( Arity(..)+  , UniversalAlgebraSig(..)+  , LawvereSort(..)+  , LogicAST(..)+  , Entailment(..)+  ) where++import Data.Kind (Type)+import GHC.TypeLits (Nat)++-- | Promoted Arity kind for universal algebra signatures.+data Arity+  = Nullary+  | Unary+  | Binary+  | Nary Nat+  deriving (Eq, Show, Ord)++-- | Textbook Universal Algebra 4-tuple Signature promoted to a Kind via DataKinds.+data UniversalAlgebraSig = UASig+  { functions :: [(String, Arity)]+  , relations :: [(String, Arity)]+  , constants :: [String]+  } deriving (Eq, Show)++-- | Multi-sorted Lawvere theory sort signature mapping input product sorts to output sort.+data LawvereSort sort = LawvereOp [sort] sort+  deriving (Eq, Show)++{- Note [Flat Logic AST Representation]+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~+[tag:note-flat-logic-ast]+In formal verification, SMT piping, and sheaf-theoretic restriction solvers, formulas+frequently contain dozens or hundreds of simultaneous clauses (e.g., global state+invariants, cell complex boundary matchings, and frame conditions).++Representing large n-ary conjunctions as nested binary trees+  (And (And (And A B) C) D)+induces three severe performance penalties:+  1. O(N^2) recursive traversal cost for deep flattening and SMT-LIB2 syntax generation.+  2. High heap allocation from intermediate binary constructor nodes.+  3. GHC call-stack depth exhaustion on deeply nested formulas during pattern matching.++To eliminate this bottleneck, 'LogicAST' incorporates 'FlatConj' and 'FlatDisj' alongside+binary 'And' and 'Or'. 'FlatConj' stores clauses as a flat contiguous list of subformulas,+enabling O(N) linear serialization into SMT-LIB2 s-expressions, trivial constant folding+(pruning 'LitTrue' / 'LitFalse' in a single pass), and cache-friendly iteration.+-}++-- | Observable deep embedding of First-Order Logic indexed by signature kind @k@.+--+-- See Note [Flat Logic AST Representation] [ref:note-flat-logic-ast].+--+-- Avoids native (->) opacity so autonomous agents and SMT pipes can inspect,+-- serialize, and rewrite formulas.+data LogicAST (sig :: k) where+  LitTrue   :: LogicAST sig+  LitFalse  :: LogicAST sig+  AtomPred  :: String -> [String] -> LogicAST sig+  Not       :: LogicAST sig -> LogicAST sig+  And       :: LogicAST sig -> LogicAST sig -> LogicAST sig+  Or        :: LogicAST sig -> LogicAST sig -> LogicAST sig+  Implies   :: LogicAST sig -> LogicAST sig -> LogicAST sig+  Iff       :: LogicAST sig -> LogicAST sig -> LogicAST sig+  Forall    :: String -> LogicAST sig -> LogicAST sig+  Exists    :: String -> LogicAST sig -> LogicAST sig+  -- | Flat contiguous conjunction (prevents O(N^2) nested binary trees)+  FlatConj  :: [LogicAST sig] -> LogicAST sig+  -- | Flat variant disjunction+  FlatDisj  :: [LogicAST sig] -> LogicAST sig++deriving instance Show (LogicAST sig)+deriving instance Eq (LogicAST sig)++-- | Syntactic deductive entailment (⊢) independent of runtime execution.+class Entailment (sen :: k -> Type) where+  entails :: forall (sig :: k). [sen sig] -> sen sig -> Bool

@@ -0,0 +1,7 @@+module Gargamelle.Logic.Syntax+  ( module Gargamelle.Logic.Signature+  , module Gargamelle.Logic.Defunctionalize+  ) where++import Gargamelle.Logic.Signature+import Gargamelle.Logic.Defunctionalize

@@ -0,0 +1,91 @@+{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}+{-# HLINT ignore "Redundant id" #-}++module Main (main) where++import Test.Hspec+import Control.Category (Category(..))+import Data.Profunctor (Strong(..), Choice(..))+import Algebra.Lattice (Lattice(..), BoundedMeetSemiLattice(..))+import Gargamelle.Logic.Signature+import Gargamelle.Logic.Defunctionalize+import Gargamelle.Logic.Contract+import Gargamelle.Logic.Galois+import Prelude hiding (id, (.))++main :: IO ()+main = hspec $ do+  describe "Gargamelle.Logic.Signature" $ do+    -- See Note [Flat Logic AST Representation] [ref:note-flat-logic-ast]+    it "constructs first-order LogicAST trees and flat connectives" $ do+      let phi = Implies (AtomPred "P" ["x"]) (Or (AtomPred "Q" ["x"]) LitFalse)+      phi `shouldBe` Implies (AtomPred "P" ["x"]) (Or (AtomPred "Q" ["x"]) LitFalse)+      let flat = FlatConj [LitTrue, AtomPred "R" ["y"]]+      flat `shouldBe` FlatConj [LitTrue, AtomPred "R" ["y"]]++  describe "Gargamelle.Logic.Defunctionalize (ObsMor)" $ do+    -- See Note [Defunctionalized Observable Morphisms] [ref:note-defunctionalized-obsmor]+    it "obeys Category identity and composition laws" $ do+      let stepA = SymbolicStep "add1" (+ (1 :: Int))+      let stepB = SymbolicStep "mul2" (* (2 :: Int))+      let comp = stepB . stepA+      evalObsMor comp 5 `shouldBe` 12+      -- Left and right identities+      evalObsMor (id . stepA) 5 `shouldBe` 6+      evalObsMor (stepA . id) 5 `shouldBe` 6++    it "supports Profunctor, Strong, and Choice combinators" $ do+      let step = SymbolicStep "double" (* (2 :: Int))+      let strongStep = first' step+      evalObsMor strongStep (3, "hello") `shouldBe` (6, "hello")+      let choiceStep = left' step+      evalObsMor choiceStep (Left 4 :: Either Int String) `shouldBe` Left 8+      evalObsMor choiceStep (Right "world" :: Either Int String) `shouldBe` Right "world"++    it "provides 100% static inspection without executing steps" $ do+      let stepA = SymbolicStep "validateInput" (+ (1 :: Int))+      let stepB = ProjectTag "payload" (* (2 :: Int))+      let stepC = InjectTag "envelope" (+ (10 :: Int))+      let pipe = stepC . stepB . stepA+      inspectObsMor pipe `shouldBe` ["Step:validateInput", "ProjectTag:payload", "InjectTag:envelope"]++  describe "Gargamelle.Logic.Contract (Assume-Guarantee via Op)" $ do+    -- See Note [Lattice Inversion via Op Dualization] [ref:note-lattice-op-dualization]+    it "dualizes refinement: meet weakens assumptions and strengthens guarantees" $ do+      -- In Bool lattice: False <= True (False is bottom, True is top)+      -- A1 = False (demanding assumption), G1 = False (weak guarantee)+      -- A2 = True (relaxed assumption), G2 = True (strong guarantee)+      let c1 = contract False False+      let c2 = contract True True+      -- Refinement (meet)+      let refined = c1 /\ c2+      -- Refined assumption: Op False /\ Op True = Op (False \/ True) = Op True (relaxed/weakened)+      getAssumption refined `shouldBe` True+      -- Refined guarantee: False /\ True = False (strengthened/meet)+      getGuarantee refined `shouldBe` False++    it "respects top and bottom contract bounds" $ do+      let topContract = top :: AGContract Bool Bool+      -- Top has minimum assumption (bottom of base lattice: False) and maximum guarantee (True)+      getAssumption topContract `shouldBe` False+      getGuarantee topContract `shouldBe` True++    -- See Note [Circular Assume-Guarantee Soundness] [ref:note-circular-ag-soundness]+    it "verifies circular assume-guarantee soundness on shared interfaces" $ do+      -- C1 assumes True, guarantees True+      -- C2 assumes True, guarantees True+      let c1 = contract True True+      let c2 = contract True True+      verifyCircularAG c1 c2 `shouldBe` True+      -- If C1 guarantees False while C2 assumes True, verification fails+      let cBroken = contract True False+      verifyCircularAG cBroken c2 `shouldBe` False++  describe "Gargamelle.Logic.Galois" $ do+    -- See Note [Adjoint Restrict-CoRestrict Galois Connections] [ref:note-galois-connection-stalks]+    it "composes Galois connections in series" $ do+      let g1 = galoisObsMor "g1" (+ (1 :: Int)) (\x -> x - (1 :: Int))+      let g2 = galoisObsMor "g2" (* (2 :: Int)) (`div` (2 :: Int))+      let gComp = composeGalois g2 g1+      evalObsMor (restrict gComp) 4 `shouldBe` 10  -- (4 + 1) * 2+      evalObsMor (coRestrict gComp) 10 `shouldBe` 4 -- (10 `div` 2) - 1