feat: Rust reference lattice core + verisim store + Rust/SPARK compliance

Lands Deliverable 2's Rust reference core (the LatticeCore impl the migration
plan calls for behind the seam; the AffineScript->Wasm swap follows once the
bridge exists, ADR-006), plus the Rust/SPARK compliance the repo was missing.

Engine (src/lattice/mod.rs): Kosaraju SCC-condensation -> DAG/partial order,
LOD zoom (sound + complete), meet (LCA; meet-semilattice — full join NOT
claimed). 6 property tests assert the laws (PROOF-NEEDS P2a/P4/P1b — tested,
not proved).
Ingest (src/ingest.rs): std-only fail-soft filesystem walk -> lattice (git2
history ingest deferred). Store (src/store.rs): LatticeStore trait +
InMemoryStore default; VeriSimDB octad backend over HTTP behind --features
verisim (no federation).

Build: removed the unresolvable affinescript-runtime PATH dep (the cargo
blocker) — re-added as a git/published dep when the bridge lands; added the
verisim feature. cargo test green: 30 tests pass.

Rust/SPARK (estate "Rust means Rust/SPARK"): added
docs/decisions/rust-spark-stance.adoc (honest: no FFI seam yet -> Idris2/Zig
ABI N/A; verifiable core migrating to AffineScript) and the missing
.github/workflows/spark-theatre-gate.yml (lenient).

Docs: PROOF-NEEDS.md gains a categorised "Proof status"; STATE + TEST-NEEDS
updated to the real state.

https://claude.ai/code/session_01JNCDaWMB8NV6nAPrvmTg4w

Author: hyperpolymath

.github/workflows/spark-theatre-gate.yml

@@ -0,0 +1,21 @@
+# SPDX-License-Identifier: MPL-2.0
+# Estate SPARK Theatre Gate — thin caller of the reusable workflow in
+# hyperpolymath/standards (#135 / #141). Pinned by commit SHA per the
+# estate action-pinning policy. Regenerate the pin only when the reusable
+# workflow is intentionally bumped.
+name: SPARK Theatre Gate
+
+on:
+  pull_request:
+  push:
+    branches: [main, master]
+
+permissions:
+  contents: read
+
+jobs:
+  spark-theatre-gate:
+    uses: hyperpolymath/standards/.github/workflows/spark-theatre-gate.yml@462003782f3ebb93ea763e81d0d199ce13ef7d73
+    with:
+      paths: "."
+      enforce_zero_contract: false

.machine_readable/6a2/STATE.a2ml

@@ -22,38 +22,38 @@ db = "verisim standalone (HTTP client; octad store); no federation unless needed
 name = "git-reticulator"
 purpose = "Semantic-lattice builder for git repositories: the symbolic half of a neuro-symbolic (Graph-RAG, proof-carrying retrieval) stack."
 primary-language = "rust"          # host: CLI + REST shell
-core-language = "affinescript"     # intended lattice core (src/lattice/affine/*.affine)
-completion-percentage = 15
+core-language = "affinescript"     # intended core (future, ADR-006); Rust reference core today
+completion-percentage = 35
 
 [position]
-phase = "design+skeleton"   # design | skeleton | implementation | testing | maintenance
+phase = "implementation"   # design | skeleton | implementation | testing | maintenance
 maturity = "experimental"   # experimental | alpha | beta | production | lts
 
 # ════════════════════════════════════════════════════════════════════════════
 # HONEST STATUS — what is real vs. what is claimed
 # ════════════════════════════════════════════════════════════════════════════
 [honest-status]
-rust-host-loc = 237                 # src/{lib.rs,cli/main.rs,api/app.rs}
-rust-host-reality = "build_lattice/query_lattice are println! stubs; actix routes return canned JSON"
-affine-core-loc = "~100 (models/storage/lattice.affine)"
-affine-core-reality = "ASPIRATIONAL — AffineScript has no working compiler yet; these files cannot build, and as written they call Rust crates (git2/postgres) which AffineScript does not bind"
-git-parsing = "NOT WIRED (git2 feature off by default; .affine calls git2 but cannot run)"
+lattice-engine = "REAL (src/lattice/mod.rs): Kosaraju SCC-condensation + partial order + LOD zoom (sound+complete) + meet (LCA). cargo green; 10 property/unit tests."
+ingest = "REAL but filesystem-only (src/ingest.rs, std-only, fail-soft). git2 HISTORY ingest NOT yet wired."
+store = "REAL: LatticeStore trait + InMemoryStore default; VeriSimDB octad backend over HTTP behind --features verisim (src/store.rs). Not yet wired into CLI/REST."
+host-reality = "CLI/REST still thin; the compat affine::{build_lattice,query_lattice} shim is now IO-free (no more println-only stubs)."
 embeddings = "NOT WIRED (tch/PyTorch feature off by default)"
-persistence = "NOT WIRED (postgres feature off by default)"
-proofs = "ZERO (no .idr/.v/.lean/.agda). The 'lattice' noun is currently unearned — see PROOF-NEEDS.md"
-test-reality = "27 tests pass but they assert 'does not panic' over println stubs; honest as smoke tests, overstated as a 7-category pyramid"
+affine-core = "DEFERRED (ADR-006 bridge-first): the Rust engine is the reference core; the .affine core lands after the Rust↔AffineScript bridge."
+proofs = "ZERO mechanized (no .idr/.v/.ads). P2a/P4/P1b are TESTED not proved — see PROOF-NEEDS.md 'Proof status'. 'lattice' = meet-semilattice + digraph (full join not claimed)."
+rust-spark = "Stance documented (docs/decisions/rust-spark-stance.adoc) + spark-theatre-gate.yml added (lenient). Idris2/Zig ABI seam N/A until an FFI surface exists."
+tests = "30 pass (10 new lattice/ingest/store + 20 compat integration/property/api). cargo test exit 0."
 
 [crg]
 grade = "C"
 achieved = "2026-04-04"
-caveat = "Grade C reflects test-CATEGORY presence, not behavioural coverage of real lattice logic (none exists yet). See READINESS.md + TEST-NEEDS.md."
+caveat = "Superseded 2026-06-04: the lattice engine is real and its properties are tested (P2a/P4/P1b). Mechanized proofs still owed (PROOF-NEEDS.md). See READINESS.md + TEST-NEEDS.md."
 next = "Grade B requires 6 quality targets (lint/fmt/doc-coverage/etc.)"
 
 [blockers-and-issues]
 blockers = [
-  "affinescript-runtime path dep unresolvable without sibling repo (severity: low; feature-gated off)",
-  "the .affine core cannot compile (AffineScript compiler not ready) AND is written against Rust crates it cannot bind (severity: high; design rethink needed)",
-  "'lattice' is currently a typed DAG with no proven meet/join (severity: medium; see PROOF-NEEDS.md)",
+  "RESOLVED 2026-06-04: removed the unresolvable affinescript-runtime path dep from Cargo.toml (cargo build now green); re-add as git/published dep when the bridge lands (ADR-006)",
+  "Deliverable 1 (Rust↔AffineScript bridge, in affinescript repo) blocks the .affine core migration (severity: high; docs/MIGRATION-PLAN.adoc)",
+  "'lattice' is a meet-semilattice + digraph; meet/zoom tested not proved (severity: medium; PROOF-NEEDS.md)",
 ]
 template-debt = [
   "RESOLVED 2026-06-03: 0-AI-MANIFEST.a2ml had [YOUR-REPO-NAME]/{{AUTHOR}} placeholders",
@@ -70,7 +70,7 @@ template-debt = [
 # Core-language question DECIDED 2026-06-04 (ADR-006): AffineScript-first, bridge-first.
 actions = [
   "DELIVERABLE 1 (in affinescript repo, runtime/): build the Rust loader + marshalling for compiled AffineScript — the affine-js equivalent for Rust. Acceptance: a Rust test loads a compiled .affine fn, calls it, round-trips a string via a host extern fn. See docs/MIGRATION-PLAN.adoc.",
-  "DELIVERABLE 2 (here, once 1 lands): thin Rust host (git2 + verisim HTTP DB + actix) + pure .affine lattice core over Wasm, behind a `trait LatticeCore` seam.",
+  "LANDED 2026-06-04: Rust reference lattice core (SCC-condensation + partial order + LOD zoom + meet) + filesystem ingest + verisim store seam + 10 tests; cargo green; Rust/SPARK stance + spark-theatre-gate added. NEXT here: wire CLI/REST to ingest→lattice→store, add criterion benches, git2 history ingest.",
   "Earn the 'lattice' word: SCC-condensation + partial order in the core, then discharge PROOF-NEEDS.md P1-P2 (Idris2).",
   "Tests/benches: replace smoke-over-stubs with property tests (partial-order laws, zoom soundness/completeness) + criterion benches; strict-but-passable CI with an AffineScript compile gate.",
 ]

Cargo.lock

@@ -19,20 +19,22 @@ env_logger = "0.10"
 clap = { version = "4.0", features = ["derive"] }
 
 # Optional dependencies (feature-gated)
-affinescript = { package = "affinescript-runtime", path = "../nextgen-languages/affinescript/runtime", optional = true }
+# NOTE: the affinescript-runtime dependency is intentionally absent. AffineScript
+# integration is deferred until the Rust↔AffineScript bridge exists (ADR-006);
+# it will be re-added as a git/published dep (not a path dep) when that lands.
 reqwest = { version = "0.12", features = ["json"], optional = true }
 git2 = { version = "0.20", optional = true }               # Git repo parsing
 postgres = { version = "0.19", features = ["with-uuid-1"], optional = true }
 tch = { version = "0.13", optional = true }                 # PyTorch embeddings
 
 [features]
 default = []
-affinescript-engine = ["affinescript"]     # AffineScript runtime integration
+verisim = ["reqwest"]                     # VeriSimDB octad store over HTTP (src/store.rs)
 git-integration = ["git2"]                # Git repository parsing
-db = ["postgres"]                         # PostgreSQL connectivity
+db = ["postgres"]                         # PostgreSQL connectivity (legacy; superseded by verisim)
 embeddings = ["tch"]                      # PyTorch-based embeddings
 http-client = ["reqwest"]                 # HTTP client for external calls
-full = ["affinescript-engine", "git-integration", "db", "embeddings", "http-client"]
+full = ["verisim", "git-integration", "db", "embeddings", "http-client"]
 
 [dev-dependencies]
 criterion = { version = "0.4", features = ["html_reports"] }   # Benchmarks

Cargo.toml

@@ -29,6 +29,60 @@
   estate friction. The order-theory here is elementary; the value is in
   *connecting the proofs to the running code*, not in their depth.
 
+## Proof status (by category) — 2026-06-04
+
+Honest categorisation. **Proved** = mechanically checked (Idris2/Coq/SPARK).
+**Tested** = executable checks + unit tests in the Rust reference core
+(`src/lattice/mod.rs`) — a rung *below* proof. git-reticulator has **zero
+mechanized proofs**; what exists is tested.
+
+### Done (tested, not proved)
+- **P2a** SCC condensation is acyclic — `Condensation::is_acyclic` (Kahn
+  topological sort, a genuine runtime check, not a trust assertion) + tests
+  (the 3-node call cycle collapses to one component; condensation is a DAG).
+- **P4** LOD `zoom` soundness + completeness — tested on fixtures (defs in
+  other files excluded; every descendant returned).
+- **P1b (fragment)** `meet` = lowest common ancestor — tested (idempotent,
+  commutative, LCA correct).
+- **P1a (fragment)** reflexivity of ≤ — tested.
+
+### Not attempted
+- **P1** full lattice laws (associativity/absorption; **join**).
+- **P3** monotone abstraction (commit-DAG → lattice) — also: git-history ingest
+  isn't wired (`src/ingest.rs` is filesystem-only).
+- **P5** determinism/confluence. **P6** drift-predicate totality.
+- **P7** pgRouting≡lattice — now **N/A** (verisim is the store, not pgRouting).
+- In the *mechanized-proof* sense, **all of P1–P7 are unattempted** (zero `.idr`).
+
+### Sorries / `believe_me` / proof escapes
+- **Zero — but vacuously.** There are no proofs, so there are no escape hatches.
+  This is **not** vcl-ut's "zero `believe_me` in a real corpus" achievement; it
+  is zero-because-empty. Recorded so it is never mistaken for rigour we lack.
+
+### Structural blockers
+- No prover wired (Idris2 recommended, absent; no proof-corpus CI gate).
+- The verifiable core is migrating to AffineScript (ADR-006), itself alpha with
+  the CORE-01 soundness gap.
+- The Rust/SPARK Idris2/Zig ABI seam is **N/A until git-reticulator exposes an
+  FFI surface** (it's a CLI/REST app today) — see
+  `docs/decisions/rust-spark-stance.adoc`.
+
+### False (claims that would be untrue — and are correctly avoided)
+- "git-reticulator builds a **lattice**" (full lattice) is **false**: arbitrary
+  sibling nodes have no unique join. The code is honest — it implements `meet`
+  only and names the structure a **meet-semilattice** + typed digraph. The true,
+  scoped claim is evidenced by test; the false strong claim is not made.
+
+### What it means / how much to worry
+- **Low worry** for an early, non-safety-critical research tool. The property
+  that matters — and holds — is that **nothing is overclaimed**: code and docs
+  say "tested not proved", "meet-semilattice not lattice", "zero proofs". That
+  honesty *is* the estate bar (the doc-truthing / SPARK-theatre culture is about
+  not faking verification). The residual risk is correctness-confidence (a
+  zoom/meet edge case could ship), not safety. The path up is cheap and known:
+  P2→P1→P4 in Idris2, or largely for free from the AffineScript core's type
+  discipline post-migration.
+
 ## What Needs Proving
 
 ### P1 — It is actually a lattice (or: rename it) — **HIGH**

PROOF-NEEDS.md

@@ -2,30 +2,31 @@
 
 ## CRG Grade: C — ACHIEVED 2026-04-04
 
-All required test categories for CRG Grade C are present and passing.
+All required test categories present and passing; `cargo test` green.
 
-> **Honest caveat (2026-06-03):** these 27 tests are *smoke-level* — they call
-> `build_lattice`/`query_lattice` (which are `println!` stubs) and assert "does
-> not panic". They verify the host compiles and the API surface is reachable;
-> they do **not** exercise real lattice logic (there is none yet). The
-> property/contract/aspect/e2e labels describe test *categories*, not
-> behavioural depth. Behavioural + property tests over a real lattice are owed
-> alongside `PROOF-NEEDS.md` P1–P4.
+> **Update 2026-06-04:** the Rust lattice engine is now real, so the suite is no
+> longer smoke-over-stubs. The 10 new lib tests assert genuine lattice
+> **properties** (SCC-condensation acyclicity, zoom soundness+completeness,
+> meet=LCA, reflexivity) — *tested, not proved* (see PROOF-NEEDS.md "Proof
+> status"). The 20 pre-existing integration/property/api tests still pass via the
+> IO-free compat shim.
 
 ### Test Inventory
 
 | Category | Status | Location | Count |
 |---|---|---|---|
-| Unit | PASS | `src/lib.rs` (`#[cfg(test)]` `unit_tests` module) | 7 |
-| Smoke | PASS | `src/lib.rs` (`unit_tests` module) | 2 |
-| Property-based (P2P) | PASS | `tests/property_tests.rs` | 5 |
+| Lattice properties | PASS | `src/lattice/mod.rs` (`#[cfg(test)]`) | 6 |
+| Ingest | PASS | `src/ingest.rs` (`#[cfg(test)]`) | 3 |
+| Store | PASS | `src/store.rs` (`#[cfg(test)]`) | 1 |
+| Property-based | PASS | `tests/property_tests.rs` | 5 |
 | E2E / Reflexive | PASS | `tests/integration_tests.rs` | 4 |
 | Contract | PASS | `tests/integration_tests.rs` | 3 |
 | Aspect | PASS | `tests/integration_tests.rs` | 6 |
+| API / CLI | PASS | `tests/api_tests.rs` | 2 |
 | Benchmarks (baselined) | PASS | `benches/git_reticulator_bench.rs` | 6 |
 
-Total tests: **27**  
-Benchmarks: **6** (Criterion, compile-verified with `cargo bench --no-run`)
+Total tests: **30** (`cargo test` exit 0)  
+Benchmarks: **6** (Criterion; behavioural criterion benches over fixture repos are owed for the new engine)
 
 ### Commands
 

TEST-NEEDS.md

@@ -0,0 +1,86 @@
+// SPDX-License-Identifier: MPL-2.0
+// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+= Rust/SPARK Stance — git-reticulator
+:toc: macro
+:toclevels: 2
+
+toc::[]
+
+== Summary
+
+git-reticulator's application logic is written in Rust. Per the estate
+language policy (`standards/.../LANGUAGE-POLICY.adoc` §Terminology),
+*"Rust" means "Rust/SPARK"*: Rust is the primary implementation language
+now, but a repo must be *designed to admit SPARK/Ada verification modules*
+across a stable, Idris2-typed boundary, with Zig as the FFI layer — and
+**Rust is never the ABI/API/FFI layer**.
+
+This document records the stance honestly. git-reticulator is at an
+*earlier* stage than the exemplar (verisimdb): it is currently a CLI + REST
+**application** plus a pure, dependency-free lattice **engine**, and it
+does **not yet expose a C ABI**. The Idris2-typed seam + Zig FFI therefore
+do not exist yet — not as a hidden gap, but because there is no FFI surface
+to put them on. This document says so, and says where the seam *will* go.
+
+== What is correctness-critical here
+
+git-reticulator is a retrieval-geometry engine, not a ledger. The
+correctness-critical surface is the lattice algebra.
+
+[cols="1,3",options="header"]
+|===
+| Critical surface | Where | Status
+
+| SCC condensation is acyclic (a real partial order exists)
+| `src/lattice/mod.rs` — `Lattice::condense`, `Condensation::is_acyclic`
+| implemented + unit-tested; *not* mechanically proved (PROOF-NEEDS P2)
+
+| LOD `zoom` soundness + completeness (no spurious/dropped context)
+| `src/lattice/mod.rs` — `Lattice::zoom`
+| implemented + unit-tested; *not* proved (PROOF-NEEDS P4)
+
+| `meet` = lowest common ancestor (meet-semilattice fragment)
+| `src/lattice/mod.rs` — `Lattice::meet`
+| implemented + unit-tested; *not* proved (PROOF-NEEDS P1b)
+|===
+
+NOTE: full lattice `join` is **not** claimed — see PROOF-NEEDS.md. The
+structure is a meet-semilattice over the containment forest plus a typed
+digraph whose SCC-condensation is a partial order.
+
+== The seam (not yet present — and where it will go)
+
+There is no `src/abi/*.idr` / `ffi/zig/` seam today because git-reticulator
+exposes no C ABI. The seam will appear at the **AffineScript→Wasm boundary**
+once the migration (ADR-006) lands: the pure lattice core moves to
+AffineScript compiled to Wasm, the Rust host provides IO via `extern fn`
+host imports, and *that* typed boundary (AffineScript's own type discipline,
+with an Idris2/SPARK admission path on the host side) is where verification
+attaches. Until then, the honest status is **N/A — no FFI surface**.
+
+== SPARK/Ada admission path
+
+Deferred. No SPARK/Ada code exists. When a correctness-critical component
+(e.g. the condensation/zoom kernel) warrants it, it can be re-implemented in
+SPARK/Ada behind the future Wasm/C-ABI contract without redesigning the host
+— which is what §Terminology requires of a "designed to admit SPARK/Ada"
+Rust project.
+
+== Honest gaps
+
+* **Zero mechanized proofs.** No `.idr`/`.ads`/`.v` proof files. The
+  lattice obligations are *tested, not proved*; Idris2 is recommended
+  (PROOF-NEEDS.md) but not wired into CI. "Zero proof escapes" here is
+  vacuous (there are no proofs to escape from) — it is **not** the
+  vcl-ut-grade "zero `believe_me` in a real corpus" achievement.
+* The verifiable core is **migrating to AffineScript** (ADR-006), which is
+  itself alpha with a known soundness gap (CORE-01).
+* The `spark-theatre-gate` runs in **lenient mode**
+  (`enforce_zero_contract: false`) — appropriate for this stage; tighten
+  when a real ABI seam + proofs exist.
+
+== References
+
+* Estate exemplar: `verisimdb/docs/decisions/rust-spark-stance.adoc`
+* This repo's obligations: `PROOF-NEEDS.md`
+* Migration that introduces the seam: `docs/MIGRATION-PLAN.adoc`, META ADR-006