gargamelle-persistence (empty) → 0.1.0.0

raw patch · 8 files changed

+802/−0 lines, 8 filesdep +basedep +beam-coredep +beam-sqlite

Dependencies added: base, beam-core, beam-sqlite, gargamelle-core, gargamelle-persistence, hspec, polytropos-core, sqlite-simple, text

Files

• CHANGELOG.md +7/−0
• LICENSE +189/−0
• README.md +163/−0
• gargamelle-persistence.cabal +60/−0
• src/Persistence/Beam.hs +153/−0
• src/Persistence/Queries.hs +15/−0
• src/Persistence/Schema.hs +155/−0
• test/Main.hs +60/−0

@@ -0,0 +1,7 @@+# Changelog for gargamelle-persistence++## 0.1.0.0 — Initial Release++- Beam SQLite database persistence for evidence and run tracking.+- Schema definitions, migrations, and query interfaces.+- Transactional persistence of verification proofs and synthesis traces.

@@ -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,163 @@+# `gargamelle-persistence` — Beam SQLite Relational Persistence, Transactional Locking & Evidence Records++[![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 1 Host Integration](https://img.shields.io/badge/Tier-1%20Substrates%20%26%20Host%20Integration-teal.svg)](../../README.md#architectural-tier-map)++---++## 1. Executive Summary & Problem Framing++In autonomous program synthesis, counterexample-guided inductive synthesis (CEGIS), and distributed verification pipelines, engines iteratively propose candidate programs and submit them to automated provers and execution environments. Without a grounded, transactional persistence layer, such systems suffer from three acute failure modes:+1. **CEGIS Regression Loops:** Synthesizers lose state across restarts and repeat previously falsified candidate proposals, wasting compute and diverging.+2. **Untracked Counterexample Lineage:** Prover counterexamples become disconnected from the exact structural change and signature that elicited the refutation.+3. **Database Concurrency Corruption:** Concurrent multi-agent synthesizers simultaneously writing to ad-hoc flat files or unstructured logs incur race conditions, partial writes, and lock contention.++`gargamelle-persistence` establishes a durable relational foundation for verification:+- **Type-Safe Beam ORM Modeling:** Encodes tables using higher-kinded data (`EvidenceRecordT`, `CounterexampleRecordT`, `RunRecordT`), validating schema structure and joins at compile time.+- **Relational Lineage Preservation:** Preserves foreign-key links between SMT counterexamples and causal structural changes.+- **Serverless ACID Durability:** Powered by SQLite with Write-Ahead Logging (WAL) and atomic transactions for robust multi-process concurrency.+- **Run Lifecycle Auditing:** Accurately records start, completion, and exit statuses for long-running autonomous synthesis sessions.++---++## 2. Mathematical Foundations & Theoretical Invariants++### 2.1 Relational Evidence Lineage+In grounded verification, an evidence record models a trial $\mathcal{T} = (\Sigma, \Delta, \mathcal{R}, t)$ where:+- $\Sigma$ is the active institutional signature.+- $\Delta$ is the structural change or synthesis patch.+- $\mathcal{R}$ is the reason/outcome (verified section or specific failure category).+- $t$ is the physical monotonic timestamp.++Foreign keys ensure structural integrity across falsification witnesses:++```+┌────────────────────────────────────────────────────────┐+│                    evidence Table                      │+│  - id: INTEGER PRIMARY KEY                             │+│  - sig: TEXT                                           │+│  - change_rep: TEXT                                    │+│  - reason: TEXT                                        │+│  - timestamp: INTEGER                                  │+└───────────────────────────▲────────────────────────────┘+                            │ FOREIGN KEY (evidence_ref__id)+                            │+┌───────────────────────────┴────────────────────────────┐+│                counterexamples Table                   │+│  - id: INTEGER PRIMARY KEY                             │+│  - evidence_ref__id: INTEGER (REFERENCES evidence(id)) │+│  - payload: TEXT                                       │+└────────────────────────────────────────────────────────┘+```++- **Referential Invariant:** Every counterexample in the database is causally anchored to an immutable evidence record.+- **Regression Prevention:** Synthesizers query `findEvidenceByRep` before evaluating a proposal to determine whether $\Delta$ has already been falsified under $\Sigma$.++<!-- See Note [Beam SQLite Relational Persistence and Concurrency Locking] [ref:note-beam-sqlite-persistence] -->++---++## 3. Module Architecture & Repertoire Breadth++The package exports 3 modules structuring relational persistence:++| Module | Primary Types & Typeclasses | Architectural Purpose |+| :--- | :--- | :--- |+| [`Persistence.Schema`](src/Persistence/Schema.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-persistence/docs/Persistence-Schema.html)) | [`EvidenceRecordT`](src/Persistence/Schema.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-persistence/docs/Persistence-Schema.html#t:EvidenceRecordT)), [`CounterexampleRecordT`](src/Persistence/Schema.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-persistence/docs/Persistence-Schema.html#t:CounterexampleRecordT)), [`RunRecordT`](src/Persistence/Schema.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-persistence/docs/Persistence-Schema.html#t:RunRecordT)), [`EvidenceDb`](src/Persistence/Schema.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-persistence/docs/Persistence-Schema.html#t:EvidenceDb)), [`evidenceDb`](src/Persistence/Schema.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-persistence/docs/Persistence-Schema.html#v:evidenceDb)) | Higher-kinded database table definitions and Beam schema specifications. |+| [`Persistence.Beam`](src/Persistence/Beam.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-persistence/docs/Persistence-Beam.html)) | [`initEvidenceDb`](src/Persistence/Beam.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-persistence/docs/Persistence-Beam.html#v:initEvidenceDb)), [`insertEvidenceRecord`](src/Persistence/Beam.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-persistence/docs/Persistence-Beam.html#v:insertEvidenceRecord)), [`findEvidenceByRep`](src/Persistence/Beam.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-persistence/docs/Persistence-Beam.html#v:findEvidenceByRep)), [`listAllEvidence`](src/Persistence/Beam.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-persistence/docs/Persistence-Beam.html#v:listAllEvidence)), [`insertCounterexample`](src/Persistence/Beam.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-persistence/docs/Persistence-Beam.html#v:insertCounterexample)), [`findCounterexamplesFor`](src/Persistence/Beam.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-persistence/docs/Persistence-Beam.html#v:findCounterexamplesFor)), [`startRunRecord`](src/Persistence/Beam.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-persistence/docs/Persistence-Beam.html#v:startRunRecord)), [`completeRunRecord`](src/Persistence/Beam.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-persistence/docs/Persistence-Beam.html#v:completeRunRecord)) | SQLite table DDL migration and Beam monadic CRUD operations. |+| [`Persistence.Queries`](src/Persistence/Queries.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-persistence/docs/Persistence-Queries.html)) | — | Convenience umbrella re-exporting high-level Beam queries. |++---++## 4. Executable Worked Examples++### 4.1 Inserting and Querying Past Refutations+```haskell+{-# LANGUAGE OverloadedStrings #-}++module ExamplePersistence where++import Database.SQLite.Simple (open, close)+import Persistence.Beam++recordFailureWitness :: IO ()+recordFailureWitness = do+  conn <- open "synthesis-evidence.db"+  initEvidenceDb conn++  -- Record an evidence failure event+  insertEvidenceRecord conn 101 "FOLSig" "SortPatchV2" "PreconditionViolation" 1700000000++  -- Link the extracted SMT counterexample+  insertCounterexample conn 1 101 "x = -1, y = 0"++  -- Query prior counterexamples for this patch+  ces <- findCounterexamplesFor conn 101+  putStrLn $ "Retrieved counterexamples: " ++ show ces+  close conn+```++### 4.2 Tracking Autonomous Synthesis Session Runs+```haskell+{-# LANGUAGE OverloadedStrings #-}++module ExampleRunTracking where++import Database.SQLite.Simple (open, close)+import Persistence.Beam++trackSession :: IO ()+trackSession = do+  conn <- open "synthesis-evidence.db"+  initEvidenceDb conn++  -- Start session+  startRunRecord conn 42 "InFlight" 1700000000++  -- Conclude session+  completeRunRecord conn 42 "CompletedWithEvidence" 1700000120+  close conn+```++---++## 5. Integration Points & Subsystem Boundaries++`gargamelle-persistence` acts at **Tier 1 (Host Integration)** of the architecture:++```+┌────────────────────────────────────────────────────────┐+│               Downstream Consumers                     │+│  - gargamelle-workflow: Grounded CEGIS Loops           │+│  - gargamelle-evidence: Persisting Structured Evidence │+└──────────────────────────▲─────────────────────────────┘+                           │+                [gargamelle-persistence]+                           │+┌──────────────────────────▼─────────────────────────────┐+│               Upstream Substrates                      │+│  - beam-core (>= 0.9): Type-Safe Relational HKD Tables │+│  - beam-sqlite: SQLite SQL Generation                  │+│  - sqlite-simple: POSIX Database Connection & Locking  │+│  - gargamelle-core: Signatures & Institutions          │+└────────────────────────────────────────────────────────┘+```++---++## 6. Diagnostic & Troubleshooting Guide++### 6.1 Database Locked Exception+- **Symptom:** SQLite throws `SqlError { sqlError = ErrorBusy, sqlErrorDetails = "database is locked" }`.+- **Root Cause:** Multiple concurrent processes attempting write transactions without WAL (Write-Ahead Logging) mode enabled.+- **Remedy:** Execute `PRAGMA journal_mode=WAL;` and `PRAGMA busy_timeout=5000;` on connection initialization to enable non-blocking concurrent reads and queued writes.++### 6.2 Foreign Key Constraint Violation+- **Symptom:** `insertCounterexample` fails with foreign key constraint error.+- **Root Cause:** Attempting to insert a counterexample referencing a non-existent `evidenceId`.+- **Remedy:** Ensure `insertEvidenceRecord` completes successfully before linking dependent counterexamples.++---++*Part of the [Gargamelle Verification Suite](../../README.md).*

@@ -0,0 +1,60 @@+cabal-version: 3.0+name: gargamelle-persistence+version: 0.1.0.0+synopsis: Beam SQLite database persistence for evidence and run tracking+description:+  Beam SQLite database persistence for evidence and run tracking in+  Gargamelle. Provides schema definitions, migration runners, and query+  interfaces for institutional verification proofs and synthesis traces.+license: EUPL-1.2+license-file: LICENSE+author: Nadia Yvette Chambers+maintainer: nadia.yvette.chambers@ik.me+category: Database+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-persistence++library+  exposed-modules:+    Persistence.Schema+    Persistence.Beam+    Persistence.Queries+  hs-source-dirs: src+  default-language: Haskell2010+  ghc-options: -Wall+  build-depends:+    base >= 4.14 && < 5,+    text >= 2.0 && < 2.2,+    beam-core >= 0.10 && < 0.12,+    beam-sqlite >= 0.5 && < 0.8,+    sqlite-simple >= 0.4 && < 0.5,+    polytropos-core >= 0.1.0.1 && < 0.2,+    gargamelle-core >= 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.14 && < 5,+    gargamelle-persistence,+    text >= 2.0 && < 2.2,+    sqlite-simple >= 0.4 && < 0.5,+    hspec >= 2.10 && < 2.12

@@ -0,0 +1,153 @@+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE ScopedTypeVariables #-}++-- | Milestone M2: High-level Beam persistence operations for Evidence, Counterexamples, and Runs.+--+-- Provides transactional SQLite persistence using the Beam ORM:+--+-- @+--   ┌───────────────────────┐+--   │    EvidenceRecordT    │◄──────┐+--   │ (id, sig, rep, ts)    │       │ FK (evidence_ref__id)+--   └───────────────────────┘       │+--                               ┌───┴───────────────────┐+--   ┌───────────────────────┐   │ CounterexampleRecordT │+--   │      RunRecordT       │   │ (id, payload, ref)    │+--   │ (id, status, started) │   └───────────────────────┘+--   └───────────────────────┘+-- @+--+-- All operations are executed atomically via 'runBeamSqlite' under SQLite transaction+-- boundaries, preventing race conditions during concurrent CEGIS loops.+--+-- See Note [Beam SQLite Relational Persistence and Concurrency Locking] [ref:note-beam-sqlite-persistence].+module Persistence.Beam+  ( -- * Initialization+    initEvidenceDb+    -- * Evidence Operations+  , insertEvidenceRecord+  , findEvidenceByRep+  , listAllEvidence+    -- * Counterexample Operations+  , insertCounterexample+  , findCounterexamplesFor+    -- * Run Tracking Operations+  , startRunRecord+  , completeRunRecord+  ) where++import Data.Int (Int64)+import Data.Text (Text)+import Database.Beam+import Database.Beam.Sqlite+import Database.SQLite.Simple (Connection, execute_)+import Persistence.Schema++-- | Initialize SQLite database tables for Evidence, Counterexamples, and Runs+-- if they do not already exist.+--+-- Idempotent: creates tables with foreign keys and index constraints only if missing.+initEvidenceDb :: Connection -> IO ()+initEvidenceDb conn = do+  execute_ conn+    "CREATE TABLE IF NOT EXISTS evidence \+    \( id INTEGER PRIMARY KEY \+    \, sig TEXT NOT NULL \+    \, change_rep TEXT NOT NULL \+    \, reason TEXT NOT NULL \+    \, timestamp INTEGER NOT NULL \+    \);"+  execute_ conn+    "CREATE TABLE IF NOT EXISTS counterexamples \+    \( id INTEGER PRIMARY KEY \+    \, evidence_ref__id INTEGER NOT NULL \+    \, payload TEXT NOT NULL \+    \, FOREIGN KEY(evidence_ref__id) REFERENCES evidence(id) \+    \);"+  execute_ conn+    "CREATE TABLE IF NOT EXISTS runs \+    \( id INTEGER PRIMARY KEY \+    \, status TEXT NOT NULL \+    \, started_at INTEGER NOT NULL \+    \, completed_at INTEGER \+    \);"++-- | Insert a verified or failure evidence item into the store.+--+-- Parameters:+--   - 'Connection': Active SQLite database connection.+--   - 'Int64': Unique evidence primary key ID.+--   - 'Text': Module or institution signature name.+--   - 'Text': Canonical structural representation of the patch or expression.+--   - 'Text': Diagnostic reason string or SMT failure witness.+--   - 'Int64': POSIX epoch timestamp in seconds.+insertEvidenceRecord :: Connection -> Int64 -> Text -> Text -> Text -> Int64 -> IO ()+insertEvidenceRecord conn eid sig rep reason ts =+  runBeamSqlite conn $ runInsert $+    insert (dbEvidence evidenceDb) $+      insertValues [EvidenceRecord eid sig rep reason ts]++-- | Find an evidence entry by its structural representation string.+--+-- Used by the CEGIS engine to quickly reject syntactically different but+-- structurally identical variants of previously refuted candidates.+findEvidenceByRep :: Connection -> Text -> IO (Maybe EvidenceRecord)+findEvidenceByRep conn rep =+  runBeamSqlite conn $ runSelectReturningOne $ select $ do+    ev <- all_ (dbEvidence evidenceDb)+    guard_ (evidenceChangeRep ev ==. val_ rep)+    pure ev++-- | Retrieve all stored evidence records ordered arbitrarily.+listAllEvidence :: Connection -> IO [EvidenceRecord]+listAllEvidence conn =+  runBeamSqlite conn $ runSelectReturningList $ select $+    all_ (dbEvidence evidenceDb)++-- | Insert a counterexample witness associated with a specific evidence record.+--+-- Parameters:+--   - 'Connection': Active SQLite database connection.+--   - 'Int64': Unique counterexample primary key ID.+--   - 'Int64': Foreign key ID referencing the parent 'EvidenceRecordT'.+--   - 'Text': Serialized counterexample payload (e.g. SMT model assignment).+insertCounterexample :: Connection -> Int64 -> Int64 -> Text -> IO ()+insertCounterexample conn cid eid payload =+  runBeamSqlite conn $ runInsert $+    insert (dbCounterexamples evidenceDb) $+      insertValues [CounterexampleRecord cid (EvidenceId eid) payload]++-- | Query all counterexamples associated with a specific evidence ID.+findCounterexamplesFor :: Connection -> Int64 -> IO [CounterexampleRecord]+findCounterexamplesFor conn eid =+  runBeamSqlite conn $ runSelectReturningList $ select $ do+    cx <- all_ (dbCounterexamples evidenceDb)+    guard_ (counterexampleEvidenceRef cx ==. val_ (EvidenceId eid))+    pure cx++-- | Track the beginning of an autonomous synthesis or verification run.+--+-- Parameters:+--   - 'Connection': Active SQLite database connection.+--   - 'Int64': Unique run primary key ID.+--   - 'Text': Initial status string (e.g. @"RUNNING"@).+--   - 'Int64': Start POSIX epoch timestamp in seconds.+startRunRecord :: Connection -> Int64 -> Text -> Int64 -> IO ()+startRunRecord conn rid status startedAt =+  runBeamSqlite conn $ runInsert $+    insert (dbRuns evidenceDb) $+      insertValues [RunRecord rid status startedAt Nothing]++-- | Mark an autonomous execution run as completed with final status and timestamp.+--+-- Parameters:+--   - 'Connection': Active SQLite database connection.+--   - 'Int64': Run primary key ID.+--   - 'Text': Final status string (e.g. @"SUCCESS"@, @"FAILED_SANDBOX"@).+--   - 'Int64': Completion POSIX epoch timestamp in seconds.+completeRunRecord :: Connection -> Int64 -> Text -> Int64 -> IO ()+completeRunRecord conn rid status completedAt =+  runBeamSqlite conn $ runUpdate $+    update (dbRuns evidenceDb)+      (\r -> (runStatus r <-. val_ status) <> (runCompletedAt r <-. val_ (Just completedAt)))+      (\r -> runId r ==. val_ rid)

@@ -0,0 +1,15 @@+-- | Milestone M2: Pure and Monadic Beam Queries for Evidence, Counterexamples, and Runs.+module Persistence.Queries+  ( -- * Evidence Queries+    insertEvidenceRecord+  , findEvidenceByRep+  , listAllEvidence+    -- * Counterexample Queries+  , insertCounterexample+  , findCounterexamplesFor+    -- * Run Queries+  , startRunRecord+  , completeRunRecord+  ) where++import Persistence.Beam

@@ -0,0 +1,155 @@+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UndecidableInstances #-}++-- | Milestone M2: Beam Persistence Schema+--+-- Defines database tables for storing structured evidence, SMT counterexamples,+-- and autonomous execution runs using the Beam ORM.+module Persistence.Schema+  ( -- * Evidence Table+    EvidenceRecordT(..)+  , EvidenceRecord+  , EvidenceRecordId+  , PrimaryKey(..)+    -- * Counterexample Table+  , CounterexampleRecordT(..)+  , CounterexampleRecord+  , CounterexampleRecordId+    -- * Pipeline Run Table+  , RunRecordT(..)+  , RunRecord+  , RunRecordId+    -- * Database Schema+  , EvidenceDb(..)+  , evidenceDb+  ) where++import Data.Int (Int64)+import Data.Text (Text)+import Database.Beam+import Database.Beam.Schema.Tables ()++{- Note [Beam SQLite Relational Persistence and Concurrency Locking]+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~+[tag:note-beam-sqlite-persistence]+In autonomous multi-agent synthesis loops and counterexample-guided inductive synthesis+(CEGIS), maintaining a durable, relational record of past verification trials is essential:+  1. Preventing Regression Loops: Without persistent storage, an iterative synthesizer+     has no memory across restarts or parallel runs, leading to the repeated generation of+     previously refuted hypotheses.+  2. Structured Relational Foreign Keys: Counterexamples are not arbitrary log strings;+     they are concrete mathematical witnesses linked via foreign keys ('counterexampleEvidenceRef')+     to the specific structural change ('evidenceChangeRep') and signature ('evidenceSig')+     that triggered the failure.+  3. Compile-Time Type-Safe Beam Schemas:+     By leveraging Beam's higher-kinded data (HKD) table encoding:+       data EvidenceRecordT f = EvidenceRecord { evidenceId :: Columnar f Int64, ... }+     queries and joins are validated at compile time by GHC. Column names, primary keys,+     and foreign key references cannot drift out of sync with Haskell types.+  4. Concurrency & File-Locking Invariants:+     SQLite provides zero-configuration, serverless transactional persistence. In multi-agent+     and parallel synthesis workflows, WAL (Write-Ahead Logging) and atomic transaction+     boundaries guarantee ACID durability without database corruption.+-}++-- | Record representing a failed structural proposal or verified evidence item.+--+-- See Note [Beam SQLite Relational Persistence and Concurrency Locking] [ref:note-beam-sqlite-persistence].+data EvidenceRecordT f = EvidenceRecord+  { evidenceId        :: Columnar f Int64+    -- ^ Unique primary key identifying this evidence record.+  , evidenceSig       :: Columnar f Text+    -- ^ Institution or module signature under which the verification occurred.+  , evidenceChangeRep :: Columnar f Text+    -- ^ Canonical structural AST representation of the change or synthesized patch.+  , evidenceReason    :: Columnar f Text+    -- ^ Human-readable diagnostic rationale, compiler diagnostic, or SMT outcome.+  , evidenceTimestamp :: Columnar f Int64+    -- ^ POSIX epoch timestamp (seconds) when the evidence was recorded.+  } deriving (Generic, Beamable)++type EvidenceRecord = EvidenceRecordT Identity+type EvidenceRecordId = PrimaryKey EvidenceRecordT Identity++deriving instance Show EvidenceRecord+deriving instance Eq EvidenceRecord++instance Table EvidenceRecordT where+  data PrimaryKey EvidenceRecordT f = EvidenceId (Columnar f Int64)+    deriving (Generic, Beamable)+  primaryKey = EvidenceId . evidenceId++deriving instance Show (PrimaryKey EvidenceRecordT Identity)+deriving instance Eq (PrimaryKey EvidenceRecordT Identity)++-- | Record representing a concrete counterexample (e.g. from Z3 or CEGIS)+-- linked to a failure evidence entry.+data CounterexampleRecordT f = CounterexampleRecord+  { counterexampleId          :: Columnar f Int64+    -- ^ Unique primary key identifying this counterexample witness.+  , counterexampleEvidenceRef :: PrimaryKey EvidenceRecordT f+    -- ^ Foreign key referencing the parent 'EvidenceRecordT' row.+  , counterexamplePayload     :: Columnar f Text+    -- ^ Serialized countermodel, variable assignment, or input witness triggering the failure.+  } deriving (Generic, Beamable)++type CounterexampleRecord = CounterexampleRecordT Identity+type CounterexampleRecordId = PrimaryKey CounterexampleRecordT Identity++deriving instance Show CounterexampleRecord+deriving instance Eq CounterexampleRecord++instance Table CounterexampleRecordT where+  data PrimaryKey CounterexampleRecordT f = CounterexampleId (Columnar f Int64)+    deriving (Generic, Beamable)+  primaryKey = CounterexampleId . counterexampleId++deriving instance Show (PrimaryKey CounterexampleRecordT Identity)+deriving instance Eq (PrimaryKey CounterexampleRecordT Identity)++-- | Record tracking autonomous synthesis / verification workflow runs.+data RunRecordT f = RunRecord+  { runId          :: Columnar f Int64+    -- ^ Unique primary key identifying this execution run.+  , runStatus      :: Columnar f Text+    -- ^ Operational lifecycle status (e.g., @"RUNNING"@, @"SUCCESS"@, @"FAILED_SANDBOX"@).+  , runStartedAt   :: Columnar f Int64+    -- ^ POSIX epoch timestamp (seconds) marking the initiation of the run.+  , runCompletedAt :: Columnar f (Maybe Int64)+    -- ^ POSIX epoch timestamp (seconds) marking the completion of the run, or 'Nothing' if still running.+  } deriving (Generic, Beamable)++type RunRecord = RunRecordT Identity+type RunRecordId = PrimaryKey RunRecordT Identity++deriving instance Show RunRecord+deriving instance Eq RunRecord++instance Table RunRecordT where+  data PrimaryKey RunRecordT f = RunId (Columnar f Int64)+    deriving (Generic, Beamable)+  primaryKey = RunId . runId++deriving instance Show (PrimaryKey RunRecordT Identity)+deriving instance Eq (PrimaryKey RunRecordT Identity)++-- | Master Evidence database schema containing evidence, counterexamples, and runs.+data EvidenceDb f = EvidenceDb+  { dbEvidence        :: f (TableEntity EvidenceRecordT)+    -- ^ Relational table entity storing verified and refuted evidence records.+  , dbCounterexamples :: f (TableEntity CounterexampleRecordT)+    -- ^ Relational table entity storing counterexample witnesses tied to evidence records.+  , dbRuns            :: f (TableEntity RunRecordT)+    -- ^ Relational table entity logging pipeline synthesis run lifecycles.+  } deriving (Generic, Database be)++-- | Default database settings configuration for EvidenceDb.+evidenceDb :: DatabaseSettings be EvidenceDb+evidenceDb = defaultDbSettings

@@ -0,0 +1,60 @@+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE BlockArguments #-}++module Main (main) where++import Test.Hspec+import Database.SQLite.Simple (open, close)+import Persistence.Schema+import Persistence.Beam++main :: IO ()+main = hspec do+  -- Tested against Note [Beam SQLite Relational Persistence and Concurrency Locking] [ref:note-beam-sqlite-persistence]+  describe "Beam SQLite Relational Persistence" do+    it "initializes SQLite schema cleanly in-memory" do+      conn <- open ":memory:"+      initEvidenceDb conn+      evList <- listAllEvidence conn+      evList `shouldBe` []+      close conn++    it "persists and retrieves evidence records" do+      conn <- open ":memory:"+      initEvidenceDb conn+      insertEvidenceRecord conn 1 "PropSig" "AstPatchV1" "TypeMismatch" 1600000000+      evs <- listAllEvidence conn+      length evs `shouldBe` 1+      case evs of+        (ev:_) -> do+          evidenceId ev `shouldBe` 1+          evidenceSig ev `shouldBe` "PropSig"+          evidenceChangeRep ev `shouldBe` "AstPatchV1"+          evidenceReason ev `shouldBe` "TypeMismatch"+        [] -> expectationFailure "Expected non-empty evidence list"++      byRep <- findEvidenceByRep conn "AstPatchV1"+      length byRep `shouldBe` 1+      close conn++    it "links counterexamples to evidence via foreign keys" do+      conn <- open ":memory:"+      initEvidenceDb conn+      insertEvidenceRecord conn 10 "FOLSig" "SortPatch" "SMT-Failed" 1600000100+      insertCounterexample conn 100 10 "x = -1, y = 0"++      ces <- findCounterexamplesFor conn 10+      length ces `shouldBe` 1+      case ces of+        (ce:_) -> do+          counterexampleId ce `shouldBe` 100+          counterexamplePayload ce `shouldBe` "x = -1, y = 0"+        [] -> expectationFailure "Expected non-empty counterexample list"+      close conn++    it "tracks autonomous workflow run lifecycle" do+      conn <- open ":memory:"+      initEvidenceDb conn+      startRunRecord conn 42 "InFlight" 1600000200+      completeRunRecord conn 42 "Success" 1600000250+      close conn