gargamelle-evidence — Evidence Preservation & Structural Tree-Diff AST Tracking

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

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.

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\]

3. Module Architecture & Repertoire Breadth

The package exports 1 comprehensive module:

4. Executable Worked Examples

4.1 Caching Known Failures and Checking Proposals

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

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.