diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 --- /dev/null +++ b/CHANGELOG.md @@ -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. 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,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$. + + + +--- + +## 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).* diff --git a/gargamelle-persistence.cabal b/gargamelle-persistence.cabal new file mode 100644 --- /dev/null +++ b/gargamelle-persistence.cabal @@ -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 diff --git a/src/Persistence/Beam.hs b/src/Persistence/Beam.hs new file mode 100644 --- /dev/null +++ b/src/Persistence/Beam.hs @@ -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) diff --git a/src/Persistence/Queries.hs b/src/Persistence/Queries.hs new file mode 100644 --- /dev/null +++ b/src/Persistence/Queries.hs @@ -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 diff --git a/src/Persistence/Schema.hs b/src/Persistence/Schema.hs new file mode 100644 --- /dev/null +++ b/src/Persistence/Schema.hs @@ -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 diff --git a/test/Main.hs b/test/Main.hs new file mode 100644 --- /dev/null +++ b/test/Main.hs @@ -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