gargamelle-evidence (empty) → 0.1.0.0
raw patch · 6 files changed
+650/−0 lines, 6 filesdep +basedep +containersdep +gargamelle-core
Dependencies added: base, containers, gargamelle-core, gargamelle-evidence, hashable, hs-tree-sitter, hspec, polytropos-core, text, tree-diff, unordered-containers
Files
- CHANGELOG.md +7/−0
- LICENSE +189/−0
- README.md +164/−0
- gargamelle-evidence.cabal +62/−0
- src/Evidence.hs +180/−0
- test/Main.hs +48/−0
+ CHANGELOG.md view
@@ -0,0 +1,7 @@+# Changelog for gargamelle-evidence++## 0.1.0.0 — Initial Release++- Evidence preservation and structural tree-diff AST tracking.+- Tree-sitter integration for syntactic analysis and parse trees.+- Semantic diffing and patch verification.
+ LICENSE view
@@ -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.
+ README.md view
@@ -0,0 +1,164 @@+# `gargamelle-evidence` — Evidence Preservation & Structural Tree-Diff AST Tracking++[](https://haskell.org)+[](https://spdx.org/licenses/EUPL-1.2.html)+[](../../README.md#architectural-tier-map)++---++## 1. Executive Summary & Problem Framing++Automated program repair, AI coding agents, and Counterexample-Guided Inductive Synthesis (CEGIS) suffer from two chronic failure modes when tracking code modifications:+1. **False Negatives in Textual Diffs:** Tracking candidate patches as textual strings or unified diff lines causes trivial syntactic perturbations (such as whitespace alterations, import reordering, identifier renaming, or comment edits) to appear distinct. Autonomous agents repeatedly generate syntactically diverse variants of the exact same broken abstract syntax tree.+2. **Prohibitive Sandboxing Overhead:** Spawning container namespaces (`/usr/bin/bwrap`) and running heavy compilation passes (e.g., GHC, Cabal) to evaluate a candidate patch that is structurally isomorphic to an already failed experiment burns CPU cycles and drastically degrades synthesis throughput.++`gargamelle-evidence` lifts program change tracking into **structural AST space**:+- **Tree-Sitter Concrete Syntax Tree Ingestion:** Ingests source code via `hs-tree-sitter` and translates syntax nodes into canonical `Data.Tree String` representations.+- **Fast $O(1)$ Failure Deduplication:** Indexes previously failed changes by structural hash (`StructuralRep`), providing instant membership queries via `proposesKnownFailure`.+- **Tree Edit Distance Metric (`tree-diff`):** Evaluates structural tree edit distance (accounting for insertions, deletions, and node replacements). If a candidate patch is within a configurable distance ($\le 2$) of a known failure, `proposesSimilarFailure` rejects the proposal prior to compilation or container sandboxing.++---++## 2. Mathematical Foundations & Theoretical Invariants++### 2.1 Lifting Textual Modifications to Structural AST Equivalence+Given a program modification $p : \text{Source} \to \text{Source}'$, the textual representation is quotiented by the parser and AST extractor:+$$[\![ p ]\!] = \operatorname{tsTreeToDataTree}(\operatorname{parse}(p)) \in \operatorname{Tree}(\operatorname{String})$$++Two candidate patches $p_1$ and $p_2$ are structurally identical if and only if their extracted labeled trees are isomorphic:+$$p_1 \sim_{\text{AST}} p_2 \iff [\![ p_1 ]\!] = [\![ p_2 ]\!]$$++```+ Raw Patch Text (p1) ──► [hs-tree-sitter] ──► Data.Tree String (dt1) ──┐+ ├──► treeDiff dt1 dt2+ Raw Patch Text (p2) ──► [hs-tree-sitter] ──► Data.Tree String (dt2) ──┘ │+ ▼+ editDistance <= 2 ?+ ├─ YES: Preemptively Reject+ └─ NO: Proceed to Sandbox+```++<!-- See Note [Structural AST Change Tracking via Tree-Diff] [ref:note-structural-tree-diff] -->++### 2.2 Tree Edit Distance Metric+The distance between two ASTs $T_1$ and $T_2$ is computed over the free edit algebra generated by copy (`Cpy`), insertion (`Ins`), deletion (`Del`), and node swap (`Swp`):+$$\operatorname{dist}(T_1, T_2) = \operatorname{editDistance}(\operatorname{treeDiff}(T_1, T_2))$$++The cost function assigns:+- $\operatorname{cost}(\operatorname{Cpy}(T)) = \sum \operatorname{cost}(\operatorname{subedits})$ (zero added penalty for identical subtrees).+- $\operatorname{cost}(\operatorname{Ins}(T)) = 1 + \sum \operatorname{cost}(\operatorname{subedits})$+- $\operatorname{cost}(\operatorname{Del}(T)) = 1 + \sum \operatorname{cost}(\operatorname{subedits})$+- $\operatorname{cost}(\operatorname{Swp}(L, R)) = 2 + \sum \operatorname{cost}(\operatorname{subedits})$++When $\operatorname{dist}(T_{\text{proposed}}, T_{\text{failed}}) \le \tau$ (with default $\tau = 2$), the candidate is classified as a minor mutation of an already rejected approach.++<!-- See Note [Structural AST Change Tracking via Tree-Diff] [ref:note-structural-tree-diff] -->++### 2.3 Evidence Store Monoid+The evidence repository forms a commutative Monoid over union:+$$\operatorname{EvidenceStore}(\Sigma) = \operatorname{HashMap} \, \operatorname{StructuralRep} \, (\operatorname{Evidence} \, \Sigma)$$+$$S_1 \diamond S_2 = S_1 \cup S_2, \quad \operatorname{mempty} = \emptyset$$++<!-- See Note [Structural AST Change Tracking via Tree-Diff] [ref:note-structural-tree-diff] -->++---++## 3. Module Architecture & Repertoire Breadth++The package exports 1 comprehensive module:++| Module | Primary Types & Typeclasses | Architectural Purpose |+| :--- | :--- | :--- |+| [`Evidence`](src/Evidence.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-evidence/docs/Evidence.html)) | [`StructuralRep`](src/Evidence.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-evidence/docs/Evidence.html#t:StructuralRep)), [`FailureReason`](src/Evidence.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-evidence/docs/Evidence.html#t:FailureReason)), [`Evidence`](src/Evidence.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-evidence/docs/Evidence.html#t:Evidence)), [`EvidenceStore`](src/Evidence.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-evidence/docs/Evidence.html#t:EvidenceStore)), [`ToStructuralRep`](src/Evidence.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-evidence/docs/Evidence.html#t:ToStructuralRep)), [`proposesKnownFailure`](src/Evidence.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-evidence/docs/Evidence.html#v:proposesKnownFailure)), [`proposesSimilarFailure`](src/Evidence.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-evidence/docs/Evidence.html#v:proposesSimilarFailure)), [`editDistance`](src/Evidence.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-evidence/docs/Evidence.html#v:editDistance)) | Structural AST change tracking, tree-diff distance metric, and evidence failure caching. |++---++## 4. Executable Worked Examples++### 4.1 Caching Known Failures and Checking Proposals+```haskell+module ExampleEvidenceStore where++import Data.Proxy (Proxy(..))+import Data.Tree (Tree(..))+import Evidence++data SystemSig++-- Build a structural representation of a failing AST+repFail :: StructuralRep+repFail = StructuralRep "Defn" (Node "Defn" [Node "name" [], Node "Int" []])++-- Record the failure with its diagnostic reason+storeWithFailure :: EvidenceStore SystemSig+storeWithFailure =+ let ev = Evidence repFail (TypeError "expected Bool, got Int") Proxy+ in addEvidence ev emptyEvidenceStore++-- Check a proposed change before executing sandbox+validateCandidate :: StructuralRep -> Either String ()+validateCandidate candidate =+ case checkProposal candidate storeWithFailure of+ Just ev -> Left ("Preemptively rejected: " ++ show (evidenceReason ev))+ Nothing -> Right ()+```++### 4.2 Calculating Structural Tree Edit Distance+```haskell+module ExampleTreeDiff where++import Data.Tree (Tree(..))+import Data.TreeDiff.Tree (treeDiff)+import Evidence++distExample :: Int+distExample =+ let tree1 = Node "Call" [Node "f" [], Node "arg1" []]+ tree2 = Node "Call" [Node "f" [], Node "arg2" []]+ diff = treeDiff tree1 tree2+ in editDistance diff+ -- Evaluates to 2 (swap of leaf node "arg1" for "arg2")+```++---++## 5. Integration Points & Subsystem Boundaries++`gargamelle-evidence` resides at **Tier 3 (Substrate & Semantics)**:++```+┌────────────────────────────────────────────────────────┐+│ Downstream Consumers │+│ - gargamelle-workflow: Sheaf-Gated CEGIS Retry Loop │+│ - gargamelle-persistence: Beam SQLite Evidence Sync │+│ - gargamelle-sandbox: Pre-Sandbox Filter │+└──────────────────────────▲─────────────────────────────┘+ │+ [gargamelle-evidence]+ │+┌──────────────────────────▼─────────────────────────────┐+│ Upstream Substrates │+│ - gargamelle-core: Institutional Signatures & Proxies │+│ - hs-tree-sitter (>= 0.1): Concrete Syntax Trees │+│ - tree-diff (>= 0.3): Tree Edit Distances │+│ - unordered-containers: Fast HashMap Hash Indices │+└────────────────────────────────────────────────────────┘+```++---++## 6. Diagnostic & Troubleshooting Guide++### 6.1 Tree-Sitter Parser Version Mismatch+- **Symptom:** `tsNodeToDataTree` fails or returns malformed child node indices.+- **Root Cause:** Incompatible C library bindings or out-of-date grammar shared objects.+- **Remedy:** Ensure the tree-sitter grammars are compiled against matching `tree-sitter` ABI versions in the Nix/Cabal environment.++### 6.2 Threshold Sensitivity in CEGIS Synthesizer+- **Symptom:** Valid candidate patches are prematurely rejected as "similar failures."+- **Root Cause:** `threshold` in `proposesSimilarFailure` is set too high (e.g., $\ge 5$), catching legitimate divergent code edits.+- **Remedy:** Retain the default threshold of $\le 2$ (allowing single-node substitutions while pruning identical leaf mutations).++---++*Part of the [Gargamelle Verification Suite](../../README.md).*
+ gargamelle-evidence.cabal view
@@ -0,0 +1,62 @@+cabal-version: 3.0+name: gargamelle-evidence+version: 0.1.0.0+synopsis: Evidence preservation and structural tree-diff AST tracking+description:+ Evidence preservation and structural tree-diff AST tracking for+ Gargamelle. Provides tree-sitter syntactic integration, parse tree+ hashing, semantic AST diffing, and proof artifact tracking.+license: EUPL-1.2+license-file: LICENSE+author: Nadia Yvette Chambers+maintainer: nadia.yvette.chambers@ik.me+category: Development+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-evidence++library+ exposed-modules:+ Evidence+ hs-source-dirs: src+ default-language: Haskell2010+ ghc-options: -Wall+ build-depends:+ base >= 4.14 && < 5,+ containers >= 0.6 && < 0.9,+ unordered-containers >= 0.2 && < 0.3,+ hashable >= 1.4 && < 1.6,+ text >= 2.0 && < 2.2,+ polytropos-core >= 0.1.0.1 && < 0.2,+ gargamelle-core >= 0.1 && < 0.2,+ hs-tree-sitter >= 13.0 && < 14,+ tree-diff >= 0.3 && < 0.5++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-evidence,+ gargamelle-core >= 0.1 && < 0.2,+ containers >= 0.6 && < 0.9,+ unordered-containers >= 0.2 && < 0.3,+ tree-diff >= 0.3 && < 0.5,+ hspec >= 2.10 && < 2.12
+ src/Evidence.hs view
@@ -0,0 +1,180 @@+{-# LANGUAGE DataKinds, TypeFamilies, GADTs, PolyKinds, FlexibleInstances, MultiParamTypeClasses, DerivingStrategies #-}++module Evidence where++import Institution+import Data.Proxy+import Data.Hashable+import qualified Data.HashMap.Strict as HM+import qualified TreeSitter as TS+import Data.TreeDiff.Tree (treeDiff, EditTree(..), Edit(..))+import System.IO.Unsafe (unsafePerformIO)+import Data.Tree (Tree(..))++-- | A structural representation of a code change or experiment that can be stored as evidence.+-- We store the Data.Tree (converted from TreeSitter) and its root label string for equality and hashing.+data StructuralRep = StructuralRep { getRepString :: String, getDataTree :: Tree String }+ deriving (Eq, Show)++instance Hashable StructuralRep where+ hashWithSalt s (StructuralRep str _) = hashWithSalt s str++-- | The type of failure reason (e.g., type error, divergence, missing instance).+data FailureReason+ = TypeError String+ | Divergence+ | MissingInstance String+ | OtherReason String+ deriving (Eq, Show)++-- | A single piece of evidence: a failed change and why it failed.+data Evidence sig = Evidence+ { evidenceChange :: StructuralRep -- ^ The structural representation of the change that failed+ , evidenceReason :: FailureReason -- ^ Why the change failed+ , evidenceContext :: Proxy sig -- ^ The signature (institution) this evidence belongs to+ }+ deriving (Eq, Show)++{- Note [Structural AST Change Tracking via Tree-Diff]+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~+[tag:note-structural-tree-diff]+In autonomous program repair, AI-guided synthesis, and Counterexample-Guided Inductive+Synthesis (CEGIS), recording failed patches as raw text strings or line-based unified diffs+fails for two fundamental reasons:+ 1. False Negatives: An autonomous model will frequently propose patches with trivial+ syntactic variations (whitespace differences, identifier renaming, comment alterations)+ that produce distinct git diff hashes while representing the exact same failing AST.+ 2. Unnecessary Sandboxing Overhead: Spawning container namespaces (/usr/bin/bwrap) and+ running full compiler toolchains (GHC) to evaluate a patch that is structurally+ identical to an already known failure wastes enormous amounts of energy and time.++'gargamelle-evidence' solves this by lifting patch tracking into structural AST space:+ - 'StructuralRep' wraps a 'Data.Tree String' converted from a Tree-Sitter concrete syntax tree.+ - 'EvidenceStore' maintains an exact hash index of previously failed structural representations,+ permitting O(1) membership testing via 'proposesKnownFailure'.+ - 'proposesSimilarFailure' runs 'treeDiff' to compute structural tree edit distance+ (accounting for insertions, deletions, and node swaps). If a proposed AST is within a+ configurable edit distance (e.g., <= 2) of a known failure, the proposal is rejected+ immediately without compiling or executing it.+-}++-- | A collection of evidence for a given signature, stored as a hash map for quick lookup.+--+-- See Note [Structural AST Change Tracking via Tree-Diff] [ref:note-structural-tree-diff].+newtype EvidenceStore sig = EvidenceStore+ { unEvidenceStore :: HM.HashMap StructuralRep (Evidence sig)+ } deriving (Eq, Show)++instance Semigroup (EvidenceStore sig) where+ EvidenceStore a <> EvidenceStore b = EvidenceStore (HM.union a b)++instance Monoid (EvidenceStore sig) where+ mempty = EvidenceStore HM.empty++-- | Create an empty evidence store.+emptyEvidenceStore :: EvidenceStore sig+emptyEvidenceStore = EvidenceStore HM.empty++-- | Add a piece of evidence to the store.+addEvidence :: Evidence sig -> EvidenceStore sig -> EvidenceStore sig+addEvidence e (EvidenceStore store) =+ EvidenceStore (HM.insert (evidenceChange e) e store)++-- | Check if a proposed change matches any known evidence (i.e., we have seen this exact structural rep fail).+proposesKnownFailure :: StructuralRep -> EvidenceStore sig -> Bool+proposesKnownFailure rep (EvidenceStore store) = HM.member rep store++-- | Retrieve the evidence for a given structural representation, if it exists.+getEvidence :: StructuralRep -> EvidenceStore sig -> Maybe (Evidence sig)+getEvidence rep (EvidenceStore store) = HM.lookup rep store++-- | Given a proposal (as a StructuralRep) and an evidence store, decide whether to allow the proposal.+-- Returns Nothing if the proposal is safe (no known failure), or Just the conflicting evidence if it is known to fail.+checkProposal :: StructuralRep -> EvidenceStore sig -> Maybe (Evidence sig)+checkProposal rep store+ | proposesKnownFailure rep store = getEvidence rep store+ | otherwise = Nothing++-- | Example usage: suppose we have a function that proposes a change and returns its structural rep.+-- In practice, this would be generated from the actual code change via tree-sitter.+class ToStructuralRep a where+ toStructuralRep :: a -> StructuralRep++-- | A wrapper for proposing a change in the context of an institution.+proposeChange :: (Institution sig, ToStructuralRep a) => a -> Proxy sig -> EvidenceStore sig -> Either (Evidence sig) a+proposeChange change _sig store =+ case checkProposal (toStructuralRep change) store of+ Just ev -> Left ev+ Nothing -> Right change++-- | After attempting a change (e.g., building/testing), if it fails, we can record the evidence.+recordFailure :: (Institution sig, ToStructuralRep a) => a -> FailureReason -> Proxy sig -> EvidenceStore sig -> EvidenceStore sig+recordFailure change reason sig =+ addEvidence (Evidence (toStructuralRep change) reason sig)++-- | Levenshtein distance algorithm for strings (kept for reference, not used in similarity checking now).+levenshtein :: String -> String -> Int+levenshtein [] ys = length ys+levenshtein xs [] = length xs+levenshtein (x:xs) (y:ys) = minimum [ levenshtein xs ys + if x == y then 0 else 1+ , levenshtein xs (y:ys) + 1+ , levenshtein (x:xs) ys + 1 ]++-- | Compute the edit distance from an Edit (EditTree a) (number of Ins, Del, Swp operations).+editDistance :: Edit (EditTree a) -> Int+editDistance = go+ where+ go (Cpy sub) = editDistanceTree sub+ go (Ins sub) = 1 + editDistanceTree sub+ go (Del sub) = 1 + editDistanceTree sub+ go (Swp l r) = 2 + editDistanceTree l + editDistanceTree r+ editDistanceTree (EditNode _ edits) = sum (map go edits)++-- | Convert a TS.Tree to a Data.Tree.Tree String by traversing the tree and converting each node to its string representation.+tsTreeToDataTree :: TS.Tree -> Tree String+tsTreeToDataTree tree = + let rootNode = unsafePerformIO $ TS.treeRootNode tree+ in tsNodeToDataTree rootNode+ where+ tsNodeToDataTree :: TS.Node -> Tree String+ tsNodeToDataTree node = + let label' = unsafePerformIO $ TS.showNodeAsString node+ childCount' = unsafePerformIO $ TS.nodeChildCount node+ count :: Int+ count = fromIntegral childCount'+ in Node label' [ tsNodeToDataTree (unsafePerformIO $ TS.nodeChild node (fromIntegral i)) | i <- [0 .. count - 1] ]++-- | Extract the root label from a Data.Tree.Tree String.+getDataTreeRootLabel :: Tree String -> String+getDataTreeRootLabel (Node label _) = label++-- | A simple instance for TS.Tree (for sketching purposes).+-- We convert the TS.Tree to a Data.Tree.Tree String and set the string representation to the root label.+instance ToStructuralRep TS.Tree where+ toStructuralRep t = + let dt = tsTreeToDataTree t+ lbl = getDataTreeRootLabel dt+ in StructuralRep lbl dt++-- | Check if a proposed tree is structurally similar to any known failure in the evidence store.+--+-- See Note [Structural AST Change Tracking via Tree-Diff] [ref:note-structural-tree-diff].+--+-- Uses tree-diff to compute the edit distance on the Data.Tree representations and returns the evidence if the distance is <= similarityThreshold.+proposesSimilarFailure :: TS.Tree -> EvidenceStore sig -> Maybe (Evidence sig)+proposesSimilarFailure proposedTree (EvidenceStore store) =+ let threshold = 2 :: Int+ proposedDT = tsTreeToDataTree proposedTree+ found = foldr (\(evRep, ev) acc -> + case acc of+ Just _ -> acc -- Already found a match, keep it+ Nothing -> + let evTree = getDataTree evRep+ diff = treeDiff proposedDT evTree+ dist = editDistance diff+ in if dist <= threshold+ then Just ev+ else Nothing) + Nothing + (HM.toList store)+ in found
+ test/Main.hs view
@@ -0,0 +1,48 @@+module Main (main) where++import Test.Hspec+import Data.Proxy (Proxy(..))+import Data.Tree (Tree(..))+import qualified Data.HashMap.Strict as HM+import Data.TreeDiff.Tree (treeDiff)+import Evidence++-- Dummy signature for testing EvidenceContext+data DummySig++main :: IO ()+main = hspec $ do+ describe "Evidence (EvidenceStore & Exact Match)" $ do+ -- See Note [Structural AST Change Tracking via Tree-Diff] [ref:note-structural-tree-diff]+ it "treats emptyEvidenceStore as identity" $ do+ let store = emptyEvidenceStore :: EvidenceStore DummySig+ unEvidenceStore (store <> mempty) `shouldBe` HM.empty++ it "records failure and detects known failing proposal" $ do+ let rep1 = StructuralRep "RootA" (Node "RootA" [Node "Child1" []])+ let rep2 = StructuralRep "RootB" (Node "RootB" [Node "Child2" []])+ let ev1 = Evidence rep1 (TypeError "type mismatch: expected Int, got Bool") Proxy+ let store1 = addEvidence ev1 (emptyEvidenceStore :: EvidenceStore DummySig)++ proposesKnownFailure rep1 store1 `shouldBe` True+ proposesKnownFailure rep2 store1 `shouldBe` False++ case checkProposal rep1 store1 of+ Just ev -> evidenceReason ev `shouldBe` TypeError "type mismatch: expected Int, got Bool"+ Nothing -> expectationFailure "Expected known failure, got Nothing"++ checkProposal rep2 store1 `shouldBe` Nothing++ describe "Evidence (Structural Tree-Diff Edit Distance)" $ do+ -- See Note [Structural AST Change Tracking via Tree-Diff] [ref:note-structural-tree-diff]+ it "computes structural tree edit distance" $ do+ let treeA = Node "Func" [Node "ParamA" []]+ let treeB = Node "Func" [Node "ParamB" []]+ let diff = treeDiff treeA treeB+ -- Swap 1 leaf node = edit distance 2+ editDistance diff `shouldBe` 2++ it "identifies identical trees with 0 edit distance" $ do+ let tree = Node "App" [Node "f" [], Node "x" []]+ let diff = treeDiff tree tree+ editDistance diff `shouldBe` 0