diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 --- /dev/null +++ b/CHANGELOG.md @@ -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. diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -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)$$ + + + +### 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: + +| 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).* diff --git a/gargamelle-logic.cabal b/gargamelle-logic.cabal new file mode 100644 --- /dev/null +++ b/gargamelle-logic.cabal @@ -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 diff --git a/src/Gargamelle/Logic/Contract.hs b/src/Gargamelle/Logic/Contract.hs new file mode 100644 --- /dev/null +++ b/src/Gargamelle/Logic/Contract.hs @@ -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 diff --git a/src/Gargamelle/Logic/Defunctionalize.hs b/src/Gargamelle/Logic/Defunctionalize.hs new file mode 100644 --- /dev/null +++ b/src/Gargamelle/Logic/Defunctionalize.hs @@ -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] diff --git a/src/Gargamelle/Logic/Galois.hs b/src/Gargamelle/Logic/Galois.hs new file mode 100644 --- /dev/null +++ b/src/Gargamelle/Logic/Galois.hs @@ -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') diff --git a/src/Gargamelle/Logic/Hole.hs b/src/Gargamelle/Logic/Hole.hs new file mode 100644 --- /dev/null +++ b/src/Gargamelle/Logic/Hole.hs @@ -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 diff --git a/src/Gargamelle/Logic/MPST.hs b/src/Gargamelle/Logic/MPST.hs new file mode 100644 --- /dev/null +++ b/src/Gargamelle/Logic/MPST.hs @@ -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) diff --git a/src/Gargamelle/Logic/Order.hs b/src/Gargamelle/Logic/Order.hs new file mode 100644 --- /dev/null +++ b/src/Gargamelle/Logic/Order.hs @@ -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) diff --git a/src/Gargamelle/Logic/Signature.hs b/src/Gargamelle/Logic/Signature.hs new file mode 100644 --- /dev/null +++ b/src/Gargamelle/Logic/Signature.hs @@ -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 diff --git a/src/Gargamelle/Logic/Syntax.hs b/src/Gargamelle/Logic/Syntax.hs new file mode 100644 --- /dev/null +++ b/src/Gargamelle/Logic/Syntax.hs @@ -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 diff --git a/test/Main.hs b/test/Main.hs new file mode 100644 --- /dev/null +++ b/test/Main.hs @@ -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