corpus: structural cross-prover identity keys + 256-dim structural embedder

CHANGELOG.adoc

@@ -8,6 +8,42 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning].
 
 === [Unreleased]
 
+==== Added — structural cross-prover identity keys, 2026-10-22
+
+* *`+src/rust/corpus/canonical.rs+`* — normalises a declaration's *type*
+  into a nameless prefix term (variables renamed `+v0, v1, …+`, module
+  qualifiers dropped, operator spellings and binder keywords canonicalised,
+  sorts mapped to `+NAT+`/`+INT+`/`+TYPE+`/…, ascriptions unwrapped) and
+  hashes it with SHA-256 under scheme `+dk-shape-v1+`. No dictionary and no
+  per-prover naming convention is consulted.
+* *`+DeclGraph+`* gains `+cross_prover_identity_key+`,
+  `+cross_prover_skeleton_key+` (binders and sorts erased — the tier-2 join
+  for Isabelle and Why3), `+identity_scheme+` and `+canonical_type+`. All
+  are `+#[serde(default)]+`, so existing octad files still load;
+  `+cross_prover_id+` (the name-tail hash) is still emitted for
+  compatibility.
+* *`+GraphPayload+`* (VeriSim bridge) and `+QueryResultEntry+` (VCL-UT)
+  carry the structural key through to consumers.
+* *`+echidna corpus identity <pattern>+`* — groups declarations by
+  structural key, with `+--skeleton+` (print the tier-2 key) and
+  `+--cross-only+` (only groups spanning several adapters).
+
+==== Changed — structural 256-dim Vector octad, 2026-10-22
+
+* The default embedder is now `+StructuralEmbedder+`: 1–3-grams of the
+  canonical type atoms hashed into *256* buckets (L2-normalised, model
+  `+echidna-corpus-structural-v2+`). `+corpus near+` canonicalises the
+  query first, so a query written in one prover's syntax retrieves entries
+  written in another's.
+* `+HashEmbedder+` (32-dim, `+echidna-corpus-hash-v1+`) remains available
+  as `+Corpus::compute_embeddings_legacy+` for GNN `+FEATURE_DIM+` parity
+  and for replaying octads written before this change. The capnp
+  `+embedder+` / `+embedder_dim+` fields carry both, and consumers must
+  compare them before comparing vectors.
+* Supersedes the embedder half of D6 in
+  `+docs/decisions/2026-04-28-corpus-and-design-search.adoc+`; the decision
+  record is annotated in place.
+
 ==== Added — corpus adapters for the estate's own TCB languages, 2026-10-22
 
 * *`+src/rust/corpus/spark_ada.rs+`* — Ada/SPARK adapter (`+*.ads+` /

CLAUDE.md

@@ -131,6 +131,7 @@ Shape, by area:
 - **Trust pipeline**: solver integrity, certificate checking, axiom tracking, sandboxing, mutation testing, Pareto ranking, Bayesian confidence — wired into `dispatch.rs`.
 - **Idris2 ABI**: `EchidnaABI.TacticRecord` (fixed-point confidence, total-order proofs, in-range round-trip lemmas) + sibling modules; type-checked on every push by `idris2-abi-ci.yml`.
 - **GNN integration**: graph construction (7 node kinds, 8 edge kinds), 32-dim local term embeddings, GNN inference client, hybrid GNN + symbolic scoring, Julia `/gnn/rank` with cosine fallback.
+- **Corpus identity**: `src/rust/corpus/canonical.rs` hashes a declaration's canonical type shape (`dk-shape-v1`) so the same theorem matches across provers without a synonym table — tier 1 keeps binders and sorts, tier 2 (`skeleton`) erases them for Isabelle/Why3. The Vector octad defaults to a 256-dim structural n-gram embedder (`echidna-corpus-structural-v2`); the 32-dim `HashEmbedder` is legacy/GNN-parity only. See `docs/CORPUS.adoc`.
 - **Chapel parallel layer (`--features chapel`)**: `ChapelParallelSearch` invoked by `dispatch.rs::verify_proof_parallel`; per-prover cwd/filename hooks in `tryProver`; L2.3 cancel-token preemption shipped; `parallelProofSearchSpeculative` (first-success-wins atomic-CAS) alongside best-of `parallelProofSearch`; `proofs/agda/ParallelSoundness.agda` formalises soundness, completeness, and cancellation-safety with zero postulate / admit / believe_me. L2.4+ (mutation parallelism, multi-locale, numeric hot paths, bench) gated on L1 Cap'n Proto and (for L2.5) a cluster runtime — see [`docs/handover/TODO.adoc`](docs/handover/TODO.adoc).
 - **Wave-3 container infrastructure**: per-prover images in `.containerization/Containerfile.wave3`; weekly cron in `container-ci.yml` runs stub-sentinel detection across all 8 Tier-3 cells.
 - **Julia ML layer**: logistic-regression tactic prediction shipped; Flux.jl scaffolds for GNN/Transformer training present but not yet trained on real data — corpus ready under `training_data/`.

crates/echidna-wire/schemas/verisim_er.capnp

@@ -83,14 +83,25 @@ struct Graph {
   octadKey                  @0 :Text;
   dependsOn                 @1 :List(Text);   # UUIDv7 list
   dependedOnBy              @2 :List(Text);
+  # SHA-256 (hex) of the canonical type shape: variable names, module
+  # paths, binder keywords and operator spellings normalised away. See
+  # `src/rust/corpus/canonical.rs` (scheme `dk-shape-v1`). This joins a
+  # theorem across provers by *type*, not by name.
   crossProverIdentityKey    @3 :Text;
+  # Same shape with binders and sorts erased: the tier-2 join for provers
+  # that elide binders (Isabelle) or use a different numeric sort (Why3).
+  crossProverSkeletonKey    @4 :Text;
+  # Version of the normalisation rules, e.g. "dk-shape-v1".
+  identityScheme            @5 :Text;
 }
 
 # --- E7 — Vector ---
 struct Vector {
   octadKey         @0 :Text;
   goalEmbedding    @1 :List(Float32);
-  embedder         @2 :Text;    # "hash-v1" / "gnn-v1"
+  embedder         @2 :Text;    # "echidna-corpus-structural-v2" / "gnn-v1"
+  # 256 for the default structural (canonical type n-gram) embedder,
+  # 32 for the legacy raw-text "echidna-corpus-hash-v1" vectors.
   embedderDim      @3 :UInt32;
 }
 

docs/CORPUS.adoc

@@ -28,8 +28,10 @@ and an `+AxiomUsage+` hazard flag set.
 * A *per-entry metrics tensor* (`+EntryMetrics+`): size, connectivity,
 shape (recursive vs structural), hazards, K-elimination risk, head-
 symbol class.
-* A *per-entry embedding* (`+Vec<f32>+`, default 32-dim hashing-trick;
-GNN backend pluggable via the `+Embedder+` trait).
+* A *per-entry embedding* (`+Vec<f32>+`, default *256-dim* structural
+n-gram hashing over the declaration's canonical type shape; the legacy
+32-dim raw-text backend is still available, and a GNN backend is
+pluggable via the `+Embedder+` trait).
 * An *8-modality octad* (`+DeclarationOctad+`) form for VeriSim
 compatibility — semantic / temporal / provenance / document / graph /
 vector / tensor / spatial.
@@ -74,6 +76,9 @@ echidna corpus near "<query text>" [--top N]
 # Cross-prover semantic-class lookup (synonym table)
 echidna corpus crossquery <semantic-class>
 
+# Cross-prover identity, keyed on the canonical type shape (no dictionary)
+echidna corpus identity <pattern> [--skeleton] [--cross-only]
+
 # Octad emit / round-trip
 echidna corpus export-octads --index <X.json> --out <X.octads.jsonl>
 echidna corpus import-octads --octads <X.octads.jsonl> --out <X.json>
@@ -147,7 +152,7 @@ identifier.
 [cols=",",options="header",]
 |===
 |Method |What
-|`+near_text("…")+` |Embed via `+HashEmbedder+`, cosine-rank.
+|`+near_text("…")+` |Canonicalise the query, embed with `+StructuralEmbedder+` (256-dim), cosine-rank. A query written in one prover's syntax matches entries written in another's.
 |`+near_vector(Vec<f32>)+` |Pre-computed embedding (e.g. from a GNN).
 |===
 
@@ -165,7 +170,8 @@ src/rust/corpus/
 ├── lean.rs      # Lean 4 adapter
 ├── idris2.rs    # Idris 2 adapter
 ├── metrics.rs   # EntryMetrics tensor (Step 4)
-├── embed.rs     # Embedder trait + HashEmbedder (Step 5)
+├── canonical.rs # Canonical type shape → E6 structural identity key
+├── embed.rs     # Embedder trait + StructuralEmbedder (256-dim) + HashEmbedder (32-dim, legacy)
 ├── octad.rs     # DeclarationOctad (8-modality, Step 3)
 └── query.rs     # Multi-axis query DSL (capstone)
 
@@ -187,18 +193,70 @@ Each declaration becomes one `+DeclarationOctad+` with eight modalities
 |Modality |Carries
 |`+semantic+` |adapter, kind, name, qualified, statement, proof
 |`+document+` |searchable_text + aspect tags (incl. hazard tags)
-|`+graph+` |depends_on + depended_on_by + cross_prover_id
+|`+graph+` |depends_on + depended_on_by + cross_prover_id (name tail, legacy) + cross_prover_identity_key / cross_prover_skeleton_key / identity_scheme / canonical_type
 |`+provenance+` |SHA-256 hash chain over (parent, event, ts, file, line)
 |`+spatial+` |file path + line + adapter namespace
 |`+temporal+` |version chain — content_hash per rung
 |`+tensor+` |EntryMetrics serialised as `+HashMap<String, f64>+`
-|`+vector+` |embedding (default 32-dim HashEmbedder)
+|`+vector+` |embedding (default 256-dim StructuralEmbedder)
+|===
+
+==== Cross-prover identity (E6 `+Graph+`)
+
+There are three keys, in decreasing order of strength. The first two are
+computed from the declaration's *type*, with no dictionary involved; the
+third is the older name-based hash and survives only for compatibility.
+
+[cols="20%,40%,40%",options="header",]
+|===
+|Field |Computed from |Joins
+|`+cross_prover_identity_key+` |SHA-256 of the canonical type shape: variable names renamed `+v0, v1, …+`, module paths dropped, operator spellings and binder keywords normalised, sorts canonicalised |Statements of the *same theorem* across provers that keep their binders and agree on sorts
+|`+cross_prover_skeleton_key+` |The same shape with the binder prefix and sort atoms erased |Provers that elide binders (Isabelle writes `+"(x::nat) + y = y + x"+`) or use a different numeric sort (Why3: `+int+`)
+|`+cross_prover_id+` |SHA-256 of the qualified name's _local tail_ |Only declarations whose local names happen to agree — kept for existing octad files and query clients
 |===
 
-`+cross_prover_id+` is SHA-256 of the qualified-name’s _local tail_, so
-`+Foo.WellFounded+` (Agda) and `+Bar.WellFounded+` (Coq) share an
-identity — cross-prover joins fall out of the graph octad without going
-through the synonym layer.
+`+identity_scheme+` records which rules produced the key (`+dk-shape-v1+`),
+so a change of normalisation rules can never masquerade as a change of
+theorem, and `+canonical_type+` keeps the rendered shape itself for
+eyeballing and debugging.
+
+The canonicalisation is purely syntactic: it does not know that `+x + y+
+equals `+y + x+`, and deliberately does not try to. See
+`+src/rust/corpus/canonical.rs+` and
+`+docs/decisions/2026-10-22-structural-cross-prover-identity.adoc+`.
+
+[source,text]
+----
+Agda     +-comm : ∀ (x y : ℕ) → x + y ≡ y + x
+Coq      Lemma add_comm : forall x y : nat, x + y = y + x.
+Lean 4   theorem Nat.add_comm (x y : Nat) : x + y = y + x := by omega
+Idris2   addComm : (x, y : Nat) -> x + y = y + x
+SMT-LIB  (assert (forall ((x Nat) (y Nat)) (= (+ x y) (+ y x))))
+Dedukti  def add_comm : Π (x y : Nat), eq Nat (add x y) (add y x).
+         ⟹ (PI [NAT NAT] (EQ (ADD v0 v1) (ADD v1 v0)))
+----
+
+Isabelle writes the same fact without binders and Why3 states it over
+`+int+`; both land on
+`+(EQ (ADD v0 v1) (ADD v1 v0))+` — the skeleton key — instead. Matching is
+therefore *tiered*: exact structural key first, skeleton key second. Any
+consumer that only compares one field should compare both.
+
+The CLI surfaces it directly:
+
+[source,bash]
+----
+$ echidna corpus identity add_comm --skeleton
+<sha256-prefix>  [structural] 6 declaration(s) across 6 adapter(s)
+  type: (PI [NAT NAT] (EQ (ADD v0 v1) (ADD v1 v0)))
+  skeleton: (EQ (ADD v0 v1) (ADD v1 v0))
+    agda     Ordinal.Brouwer.+-comm
+    coq      Nat.add_comm
+    dedukti  arith.add_comm
+    idris2   Nat.addComm
+    lean4    Nat.add_comm
+    smtlib   bvadd_comm
+----
 
 === Synonym table cross-prover joins
 
@@ -239,9 +297,13 @@ gaps surface.
 widen reverse-closures (over-conservative, which is the safer side for
 impact analysis). Step 3’s `+cross_prover_id+` and octad provenance can
 underwrite a follow-up content-addressed dep resolver.
-* *Hashing-trick embeddings collide* at 32 dims on large corpora; swap
-in a GNN backend (`+Embedder+` trait) when the Julia ML pipeline is
-primed against real corpora.
+* *The structural embedder is a baseline, not a model.* It hashes
+1–3-grams of the canonical atom stream into 256 buckets, so it captures
+type structure but not proof structure, and unrelated declarations that
+share a type shape (e.g. two `+x = x+` lemmas) are near-identical by
+construction. Swap in a GNN backend (`+Embedder+` trait) when the Julia ML
+pipeline is primed against real corpora; the 256-dim structural vectors
+are the baseline those runs are measured against.
 
 === Verified end-to-end
 

docs/architecture/VERISIM-ER-SCHEMA.adoc

@@ -149,8 +149,17 @@ Dependency edges + cross-prover identity edges.
 
 |`+depended_on_by+` |`+List<UUIDv7>+` |reverse deps
 
-|`+cross_prover_identity_key+` |`+String+` |groups Octads representing
-the SAME mathematical object across adapters — see Rel-2 below
+|`+cross_prover_identity_key+` |`+String+` (64-hex SHA-256) |groups
+Octads representing the SAME theorem across adapters by the *canonical
+shape of its type* — see Rel-2 below
+|`+cross_prover_skeleton_key+` |`+String+` (64-hex SHA-256) |the same
+shape with binders and sorts erased; the tier-2 join for provers that
+elide binders (Isabelle) or use a different numeric sort (Why3)
+|`+identity_scheme+` |`+String+` |which normalisation rules produced the
+keys — currently `+"dk-shape-v1"+`
+|`+canonical_type+` |`+String+` |the rendered canonical shape itself,
+e.g. `+(PI [NAT NAT] (EQ (ADD v0 v1) (ADD v1 v0)))+`; debug/eyeball only,
+never a join key
 |===
 
 Rust: `+OctadPayload.graph+` VeriSimDB table: `+octads_graph+` Indexed
@@ -166,10 +175,15 @@ Goal embeddings for `+near_text+` and GNN-guided search.
 |Field |Type |Notes
 |`+octad_key+` (PK,FK→E1) |`+UUIDv7+` |
 
-|`+goal_embedding+` |`+List<f32>+` |currently 32-dim HashEmbedder,
-future 256-dim GNN
+|`+goal_embedding+` |`+List<f32>+` |256-dim structural 1–3-gram hashing
+over the canonical type shape (`+echidna-corpus-structural-v2+`);
+32-dim raw-text vectors (`+echidna-corpus-hash-v1+`) remain readable
 
-|`+embedder+` |`+String+` (`+"hash-v1"+`/`+"gnn-v1"+`) |versioning
+|`+embedder+` |`+String+` |`+echidna-corpus-structural-v2+` (default),
+`+echidna-corpus-hash-v1+` (legacy), `+gnn-v1+` (future)
+
+|`+embedder_dim+` |`+UInt32+` |256 for the structural embedder, 32 for the
+legacy hash embedder; consumers must check it before comparing vectors
 |===
 
 Rust: `+OctadPayload.vector+` VeriSimDB table: `+octads_vector+` Indexed
@@ -303,11 +317,24 @@ table holds at most one row per octad_key.
 `+GraphModality.cross_prover_identity_key+`.
 
 Semantics: two Octads `+o1+`, `+o2+` are _cross-prover-identified_ iff
+they have distinct adapters AND either
 `+o1.graph.cross_prover_identity_key == o2.graph.cross_prover_identity_key+`
-AND they have distinct adapters. Example: the Coq `+Nat.add_comm+` and
-the Lean `+Nat.add_comm+` both carry identity key
-`+"nat-add-commutativity"+`. Used to answer queries like _"`every prover
-that has formalised theorem X`"_.
+(tier 1) or
+`+o1.graph.cross_prover_skeleton_key == o2.graph.cross_prover_skeleton_key+`
+(tier 2). Tier 2 exists because some provers cannot produce a tier-1 key:
+Isabelle writes `+"(x::nat) + y = y + x"+` with no binders, and Why3 states
+arithmetic over `+int+` where others state it over `+nat+`.
+
+The key is the SHA-256 of a canonical, alpha-normalised prefix term
+derived from the declaration's *type*, not from its name. So the Coq
+`+Nat.add_comm+`, the Agda `+Ordinal.Brouwer.+-comm+` and the SMT-LIB
+`+bvadd_comm+` all carry the same key, because all three normalise to
+`+(PI [NAT NAT] (EQ (ADD v0 v1) (ADD v1 v0)))+`. No synonym table and no
+per-prover naming convention is consulted. Used to answer queries like
+_"'`every prover that has formalised theorem X`"_.
+
+`+identity_scheme+` must be compared along with the keys: a key produced
+by `+dk-shape-v1+` is not comparable with one produced by a later scheme.
 
 Materialised view: `+cross_prover_clusters+` in VeriSimDB.
 

docs/decisions/2026-04-28-corpus-and-design-search.adoc

@@ -138,6 +138,14 @@ to the GNN’s `+FEATURE_DIM+`. When the GNN server is primed, swap one
 trait impl. Vector octad’s `+model+` field reflects which embedder
 produced each row — replays distinguish them.
 
+NOTE: Superseded in part on 2026-10-22. The default `+Embedder+` is now
+`+StructuralEmbedder+` — 256-dim 1–3-gram hashing over the declaration's
+_canonical type shape_ rather than its raw text, so statements written in
+different provers' syntaxes land near each other. The 32-dim
+`+HashEmbedder+` is retained for GNN-compatible (`+FEATURE_DIM+`) vectors
+and for replaying pre-2026-10-22 octads. See
+`+docs/decisions/2026-10-22-structural-cross-prover-identity.adoc+`.
+
 ==== D7. Bennettian / Landauer caveat
 
 User asked whether the design-search stack is near-Landauer, very