diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index a3064712..d34ce627 100644 --- a/CHANGELOG.adoc +++ b/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 +`* — 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+` / diff --git a/CLAUDE.md b/CLAUDE.md index 96d270c5..3919d823 100644 --- a/CLAUDE.md +++ b/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/`. diff --git a/crates/echidna-wire/schemas/verisim_er.capnp b/crates/echidna-wire/schemas/verisim_er.capnp index 07e7725b..fcf927eb 100644 --- a/crates/echidna-wire/schemas/verisim_er.capnp +++ b/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; } diff --git a/docs/CORPUS.adoc b/docs/CORPUS.adoc index f0e7c55b..13d44e02 100644 --- a/docs/CORPUS.adoc +++ b/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+`, default 32-dim hashing-trick; -GNN backend pluggable via the `+Embedder+` trait). +* A *per-entry embedding* (`+Vec+`, 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 "" [--top N] # Cross-prover semantic-class lookup (synonym table) echidna corpus crossquery +# Cross-prover identity, keyed on the canonical type shape (no dictionary) +echidna corpus identity [--skeleton] [--cross-only] + # Octad emit / round-trip echidna corpus export-octads --index --out echidna corpus import-octads --octads --out @@ -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)+` |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+` -|`+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 + [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 diff --git a/docs/architecture/VERISIM-ER-SCHEMA.adoc b/docs/architecture/VERISIM-ER-SCHEMA.adoc index 599af165..b53e6701 100644 --- a/docs/architecture/VERISIM-ER-SCHEMA.adoc +++ b/docs/architecture/VERISIM-ER-SCHEMA.adoc @@ -149,8 +149,17 @@ Dependency edges + cross-prover identity edges. |`+depended_on_by+` |`+List+` |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+` |currently 32-dim HashEmbedder, -future 256-dim GNN +|`+goal_embedding+` |`+List+` |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. diff --git a/docs/decisions/2026-04-28-corpus-and-design-search.adoc b/docs/decisions/2026-04-28-corpus-and-design-search.adoc index 41204df2..ea12d96f 100644 --- a/docs/decisions/2026-04-28-corpus-and-design-search.adoc +++ b/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 diff --git a/docs/decisions/2026-10-22-structural-cross-prover-identity.adoc b/docs/decisions/2026-10-22-structural-cross-prover-identity.adoc new file mode 100644 index 00000000..1fdc31b5 --- /dev/null +++ b/docs/decisions/2026-10-22-structural-cross-prover-identity.adoc @@ -0,0 +1,151 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) += ADR: structural cross-prover identity keys and a 256-dim structural embedder +:revdate: 2026-10-22 +:status: accepted + +== Context + +Two claims in the tree were weaker than the documentation implied. + +. *Cross-prover identity was name-based.* + `+GraphModality.cross_prover_identity_key+` was populated from + `+cross_prover_key(&entry.qualified)+` — a SHA-256 of the qualified name's + local tail. Two declarations joined only if their authors happened to pick + the same local name. Across the estate's seventeen libraries that is + routinely false: `+-comm+` (Agda), `+Nat.add_comm+` (Lean/Coq), + `+addComm+` (Idris 2), `+bvadd_comm+` (SMT-LIB) are the same theorem and + shared nothing. The synonym tables papered over some of this with + per-name dictionary entries — expensive, incomplete, and wrong the moment + a library is added. + +. *The Vector octad was 32-dimensional and surface-text based.* + `+HashEmbedder+` hashed raw statement tokens into 32 buckets. Two + statements of the same theorem in different syntaxes shared almost no + vocabulary, so cross-prover similarity search was effectively + name-matching again. + +The owner's instruction was to use the *type signature* rather than the +name, on the grounds that the estate standardises on Dedukti and every +prover can render a type, then to raise the embedder dimension so there is +a usable baseline before the first Flux GNN run. + +== Decision + +=== D1. Identity is the hashed canonical shape of the type + +`+src/rust/corpus/canonical.rs+` normalises a declaration's statement into a +nameless prefix term and hashes it (SHA-256, scheme `+dk-shape-v1+`). + +[cols="25%,75%",options="header",] +|=== +|Step |Rule +|Header |Drop the declaration keyword (`+theorem+`, `+lemma+`, `+def+`, `+assert+`, …) and the declared name; cut the proof body at `+:=+` / `+by+` / `+where+`. +|Names |Dotted names reduce to their last component before lookup (`+Nat.add_comm+` → `+add_comm+`). +|Operators |Spellings collapse to canonical prefix operators: `+++`, `+plus+`, `+HAdd.hAdd+`, `+bvadd+` → `+ADD+`; `+=+`, `+≡+`, `+eq+` → `+EQ+`; `+->+`, `+→+` → `+ARROW+`. +|Associativity |Arrows and `+↔+` right-associative; arithmetic and comparisons left. +|Sorts |`+nat+`/`+ℕ+` → `+NAT+`, `+int+`/`+ℤ+` → `+INT+`, `+Prop+`/`+Set+`/`+Type+` → `+TYPE+`, … +|Variables |Every variable is renamed `+v0, v1, …+` by first appearance — alpha-normalisation, so `+(x, y)+` and `+(a, b)+` agree. +|Ascriptions |Isabelle's `+(x::nat)+` is unwrapped; Dedukti's explicit `+eq Nat a b+` sort argument is dropped. +|=== + +The same theorem, seven ways: + +[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))) +---- + +=== D2. Two tiers, because some provers cannot state the first + +Isabelle writes `+lemma add_comm: "(x::nat) + y = y + x"+` with no binders at +all; Why3 states arithmetic over `+int+` where the others use `+nat+`. Both +are the same theorem. Erasing aspects of a key to force a match would have +made the primary key weaker for everybody, so the module emits *both*: + +* `+cross_prover_identity_key+` — the shape as written (binders and sorts + included). Exact, sort-aware. +* `+cross_prover_skeleton_key+` — the same term with the binder prefix and + sort atoms erased. Isabelle and Why3 match here: + `+(EQ (ADD v0 v1) (ADD v1 v0))+`. + +Consumers join on tier 1 first, then tier 2. `+identity_scheme+` travels +with every key so a change of normalisation rules cannot masquerade as a +change of theorem, and `+canonical_type+` keeps the rendered shape for +debugging. + +=== D3. What is deliberately *not* normalised + +No equational theory is applied. `+x + y+` and `+y + x+` are different +shapes; so are `+x + (y + z)+` and `+(x + y) + z+`. The key is a syntactic +identity, not a decision procedure, and the tests pin that down so a future +"improvement" cannot silently merge distinct theorems. Neither is the +calculus rewritten: a statement mentioning `+WellFounded+` still mentions +`+WellFounded+`. + +=== D4. The Vector octad becomes 256-dim and structural + +`+StructuralEmbedder+` hashes 1-, 2- and 3-grams of the *canonical* atom +stream into 256 buckets (weights 1.0 / 0.6 / 0.35, L2-normalised), +model id `+echidna-corpus-structural-v2+`. Consequences: + +* `+corpus near +` canonicalises the query first, so a query written + in SMT-LIB syntax retrieves entries written in Coq syntax. This is tested. +* `+HashEmbedder+` (32-dim, `+echidna-corpus-hash-v1+`) remains available as + `+Corpus::compute_embeddings_legacy+` for GNN-compatible `+FEATURE_DIM+` + vectors and for replaying octads written before this change. +* The capnp schema's `+embedder+` / `+embedder_dim+` fields now carry the + model id and dimension explicitly; consumers must compare both before + computing cosine similarity (a 32-vs-256 comparison returns 0.0 rather + than a wrong number). + +This is a *baseline*, not a model: it captures type structure, not proof +structure, and two unrelated declarations with the same type shape are +near-identical by construction. It exists so the first GNN run has +something honest to beat. + +== Evidence + +The canonicaliser was prototyped and validated before being ported to Rust +(the prototype lived outside the tree, per the no-Python rule; the Rust +module is the artefact of record). On the fixture set: + +* Agda, Coq, Lean 4, Idris 2, SMT-LIB and Dedukti agree on the primary key + for `+add_comm+`; Isabelle agrees on the skeleton key; Why3 agrees on the + skeleton key and differs on the primary (`+int+` vs `+nat`), by design. +* `+add_zero+` agrees across Agda, Coq, Lean 4 and SMT-LIB; Isabelle joins + on the skeleton. +* Associativity and commutativity produce different keys; alpha-renaming + does not change the key. + +The unit tests in `+src/rust/corpus/canonical.rs+` pin every one of those +properties, and `+src/rust/corpus/octad.rs+` asserts that a Coq and an +SMT-LIB statement of the same theorem share the structural key while their +legacy name-tail hashes differ. + +== Consequences + +* `+DeclGraph+` gains `+cross_prover_identity_key+`, + `+cross_prover_skeleton_key+`, `+identity_scheme+` and `+canonical_type+`; + all are `+#[serde(default)]+`, so existing octad files still load. +* `+GraphPayload+` (VeriSim bridge) and `+QueryResultEntry+` (VCL-UT) carry + the structural key through to consumers. +* `+echidna corpus identity +` exposes the grouping directly. +* The synonym dictionaries are still useful for *names* and *concepts*; + they are no longer on the identity path. + +== Open + +* The canonicaliser handles the statement shapes in the fixtures and the + estate's corpora; it is not a grammar for any prover. Statements it + cannot parse fall back to a whitespace-normalised text key at tier 3 + (`+KeyTier::Text+`), which is honest but weak — worth measuring. +* Sorts are compared by name. `+Nat+` in Lean and `+nat+` in Coq agree + because both are aliased to `+NAT+`; type classes and universe levels are + not modelled. diff --git a/docs/handover/STATE.adoc b/docs/handover/STATE.adoc index 211032d2..ed39e012 100644 --- a/docs/handover/STATE.adoc +++ b/docs/handover/STATE.adoc @@ -4,7 +4,7 @@ `+ECHIDNA-TODO.md+` (actionable backlog) and the full continuation prompts at `+verification-ecosystem/echidna/docs/handover/+`. -Last updated: 2026-04-26. +Last updated: 2026-10-22. ''''' @@ -194,6 +194,28 @@ Rust C FFI bridge *(the Zig layer is done; dispatch-path integration is the L2 work above)*; Tamarin/ProVerif bridge *(already landed — stale in the roadmap)*. +=== Corpus identity (2026-10-22) + +The corpus lane no longer joins declarations by name. `+corpus/canonical.rs+` +normalises a declaration's type into a nameless prefix term (variables +renamed `+v0, v1, …+`, module paths and operator spellings erased, sorts +canonicalised) and hashes it: + +[cols="30%,70%",options="header",] +|=== +|Artefact |State +|`+cross_prover_identity_key+` |SHA-256 of the canonical type shape, scheme `+dk-shape-v1+`. Six provers agree on `+add_comm+` with no dictionary. +|`+cross_prover_skeleton_key+` |Same shape with binders and sorts erased — the tier-2 join for Isabelle and Why3 (validated). +|`+cross_prover_id+` |Legacy name-tail hash; still emitted so pre-existing octads and query clients keep working. +|Vector octad |256-dim structural 1–3-gram hashes (`+echidna-corpus-structural-v2+`), replacing the 32-dim raw-text `+HashEmbedder+` as default; the 32-dim backend remains for GNN `+FEATURE_DIM+` parity. +|CLI |`+echidna corpus identity +` groups matches by structural key; `+--skeleton+` prints the tier-2 key; `+--cross-only+` filters to multi-adapter groups. +|=== + +Not modelled: equational theories (`+x + y+` and `+y + x+` are different +keys, deliberately), type classes, universe levels. Statements that do not +parse fall back to whitespace-normalised text (`+KeyTier::Text+`). See +`+docs/decisions/2026-10-22-structural-cross-prover-identity.adoc+`. + === Handover artefacts (in-repo, canonical) [width="100%",cols="50%,50%",options="header",] diff --git a/docs/wikis/Architecture.md b/docs/wikis/Architecture.md index e6ddb128..19d78834 100644 --- a/docs/wikis/Architecture.md +++ b/docs/wikis/Architecture.md @@ -31,7 +31,7 @@ which can be opened directly in a browser. ## Corpus Ingest -Seventeen structural ingest adapters live under `src/rust/corpus/.rs`, +Twenty structural ingest adapters live under `src/rust/corpus/.rs`, each exposing `pub fn ingest(root: &Path) -> Result` that returns the canonical `Corpus` struct ([`src/rust/corpus/mod.rs:156`](https://github.com/hyperpolymath/echidna/blob/main/src/rust/corpus/mod.rs#L156)). The adapters use a **two-pass extraction pattern** @@ -63,6 +63,62 @@ wiring (`suggest` synonym table, `octad-emit` → VeriSimDB, GNN training data) are documented in [`docs/CORPUS-ADAPTERS.adoc`](https://github.com/hyperpolymath/echidna/blob/main/docs/CORPUS-ADAPTERS.adoc). +## Cross-prover Identity and Embeddings + +Declarations are joined across provers by the **shape of their type**, not by +their names. `src/rust/corpus/canonical.rs` normalises a statement into a +nameless prefix term — variables renamed `v0, v1, …` by first appearance, +module qualifiers dropped, operator spellings and binder keywords +canonicalised, sorts mapped to `NAT`/`INT`/`TYPE`/… — and hashes it +(SHA-256, scheme `dk-shape-v1`): + +``` +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))) +``` + +Two keys are emitted, and consumers join on tier 1 first, tier 2 second: + +| Field | Meaning | +|---|---| +| `graph.cross_prover_identity_key` | SHA-256 of the canonical type shape, binders and sorts included | +| `graph.cross_prover_skeleton_key` | The same shape with the binder prefix and sort atoms erased — the tier-2 join | +| `graph.identity_scheme` | Which rules produced the keys (`dk-shape-v1`) | +| `graph.canonical_type` | The rendered shape, for debugging | +| `graph.cross_prover_id` | Legacy name-tail hash, kept for existing octad files and clients | + +Tier 2 exists because some provers cannot produce a tier-1 key: Isabelle +writes `lemma add_comm: "(x::nat) + y = y + x"` with no binders, and Why3 +states arithmetic over `int` where the others state it over `nat`. Both +join on `(EQ (ADD v0 v1) (ADD v1 v0))`. + +No equational theory is applied — `x + y` and `y + x` are different keys, +deliberately — and no synonym table is consulted on the identity path. The +CLI exposes the grouping: + +``` +$ echidna corpus identity add_comm --skeleton +``` + +Vector octads carry a 256-dimensional embedding +(`echidna-corpus-structural-v2`): 1-, 2- and 3-grams of the canonical atom +stream hashed into 256 buckets and L2-normalised. Because the input is +canonical, a query written in SMT-LIB syntax retrieves entries written in +Coq syntax. The older 32-dim raw-text `HashEmbedder` +(`echidna-corpus-hash-v1`) is retained for GNN-compatible `FEATURE_DIM` +vectors and for replaying pre-2026-10-22 octads; consumers must compare +`embedder` and `embedder_dim` before comparing vectors. This embedder is a +baseline for the first Flux GNN run, not a trained model. + +See [`docs/CORPUS.adoc`](https://github.com/hyperpolymath/echidna/blob/main/docs/CORPUS.adoc) +and the ADR +[`docs/decisions/2026-10-22-structural-cross-prover-identity.adoc`](https://github.com/hyperpolymath/echidna/blob/main/docs/decisions/2026-10-22-structural-cross-prover-identity.adoc). + ## Cross-prover Vocabulary Three layers stack over the per-prover synonym tables to give the diff --git a/docs/wikis/Home.md b/docs/wikis/Home.md index 24446287..de773e9c 100644 --- a/docs/wikis/Home.md +++ b/docs/wikis/Home.md @@ -71,6 +71,7 @@ commit. - **12 core backends** exposed by default; the wider surface (external prover bindings plus TypeChecker disciplines routed via TypedWasm Sigma) is reachable through explicit `ProverKind` selection. Figures and their denominators: [`docs/PROVER_COUNT.adoc`](https://github.com/hyperpolymath/echidna/blob/main/docs/PROVER_COUNT.adoc). - **20 corpus adapters** — every major public proof corpus has a structural ingest path, plus Ada/SPARK, Rust/Creusot and the estate profile (see [`docs/CORPUS-ADAPTERS.adoc`](https://github.com/hyperpolymath/echidna/blob/main/docs/CORPUS-ADAPTERS.adoc)). +- **Dictionary-free cross-prover identity** — declarations are matched on a hashed canonical form of their *type* (`dk-shape-v1`), so `+-comm` (Agda), `Nat.add_comm` (Coq/Lean), `addComm` (Idris 2) and `bvadd_comm` (SMT-LIB) share a key; a 256-dim structural embedder backs `corpus near` (see Architecture → Cross-prover Identity). - **4 arbitration mechanisms** — portfolio majority-vote, Bayesian posterior, Dempster-Shafer belief combination, Pareto multi-objective frontier. - **6 cross-prover exchange formats** — OpenTheory, Dedukti, TPTP, SMT-LIB, SMTCoq, Lambdapi. - **11-step trust pipeline** — integrity → portfolio → certificates → axioms → confidence → mutation → pareto → statistics → emission (see Architecture page). diff --git a/src/rust/corpus/canonical.rs b/src/rust/corpus/canonical.rs new file mode 100644 index 00000000..c441c087 --- /dev/null +++ b/src/rust/corpus/canonical.rs @@ -0,0 +1,1275 @@ +// SPDX-FileCopyrightText: 2026 ECHIDNA Project Team +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +// SPDX-License-Identifier: MPL-2.0 + +//! Structural canonical form of a declaration's *type*, for cross-prover +//! identity keys (VeriSim E6 `GraphModality.cross_prover_identity_key`). +//! +//! The corpus stores one `statement` string per declaration, written in +//! whatever the source prover's surface syntax is. Matching those strings +//! by name (or by a synonym table) is what the estate did before: it needs +//! a dictionary entry per naming convention, and it silently fails for +//! anything the dictionary has never seen. +//! +//! This module takes the other route. It normalises the statement into a +//! *shape* — a nameless prefix term — and hashes that. Two declarations +//! that state the same theorem get the same shape even when their source +//! languages disagree about almost everything: +//! +//! ```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 elides the binders (`lemma add_comm: "(x::nat) + y = y + x"`), +//! and Why3 states the same arithmetic over `int` rather than `nat`. Those +//! two therefore miss the primary key but match the *skeleton* key, which +//! is the same shape with the binder prefix and sort atoms erased: +//! +//! ```text +//! ⟹ (EQ (ADD v0 v1) (ADD v1 v0)) +//! ``` +//! +//! So a lookup tries the primary key first (exact, sort-aware) and falls +//! back to the skeleton key (binder- and sort-free) — a two-tier join, not +//! a fuzzy one. Nothing here consults a dictionary: the normalisation is +//! purely syntactic. +//! +//! ## What is normalised +//! +//! 1. **Declaration header** — `theorem`/`lemma`/`def`/`opaque`/`assert`/… +//! plus the declared *name*, and any proof body after `:=`/`by`/`where`. +//! 2. **Module qualifiers** — `Nat.add_comm` and `bvadd` reduce to their +//! last component before the operator table is consulted. +//! 3. **Operator spelling** — `+`, `plus`, `add`, `HAdd.hAdd`, `bvadd` are +//! all `ADD`; `=`, `==`, `≡`, `eq` are `EQ`; `->`, `→` are `ARROW`. +//! Canonical operators are emitted in **prefix** form, so infix input +//! (`x + y`) and SMT-LIB prefix input (`(+ x y)`) agree. +//! 4. **Associativity** — arrows and `↔` are right-associative; arithmetic +//! and comparison are left-associative. +//! 5. **Sorts** — `nat`/`ℕ` → `NAT`, `int`/`ℤ` → `INT`, `Prop`/`Set`/ +//! `Type` → `TYPE`, and so on. Unknown sorts keep their (unqualified, +//! lower-cased) name. +//! 6. **Variables** — every variable, bound or free, is renamed `v0`, `v1`, +//! … in order of first appearance. That is the alpha-normalisation: the +//! *names* disappear, the *positions* do not, and a prover that writes +//! `(x, y : Nat)` and one that writes `(a, b : Nat)` land on the same +//! key. De Bruijn's point — that binding structure, not the spelling of +//! variables, carries the meaning — is what is being exploited; the +//! indices here are assigned by first use rather than by binder depth +//! because real corpus statements routinely elide binders entirely, and +//! depth indices would then not line up (see Isabelle above). +//! 7. **Type ascriptions** — Isabelle's `(x::nat)` is a term ascription, +//! not a binder, and is unwrapped; Dedukti's explicit `eq Nat a b` +//! type argument is dropped so it matches the infix form. +//! 8. **Agda operator names** — `_<_`, `_+_`, `_≡_` are read as the +//! operator they wrap rather than as three punctuation tokens. +//! +//! ## What is *not* normalised +//! +//! Commutativity, associativity and other equational theories are **not** +//! applied: `x + y` and `y + x` are different shapes, deliberately. Nor is +//! the calculus changed: a statement that mentions `WellFounded` keeps +//! `WellFounded`. This is a syntactic identity key, not a decision +//! procedure, and the docs say so. +//! +//! The Rust here is a transcription of a Python prototype that was run +//! against the spellings above before it was ported; the unit tests at the +//! bottom of the file pin each of them. + +#![allow(dead_code)] + +use sha2::{Digest, Sha256}; + +/// Version tag for the normalisation scheme, stored next to every key so a +/// future change of rules cannot be mistaken for a change of theorem. +pub const SCHEME: &str = "dk-shape-v1"; + +/// How much of the statement a key is known to preserve. +#[derive( + Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, serde::Serialize, serde::Deserialize, +)] +pub enum KeyTier { + /// Bindings and sorts survived: the strongest key. + Structural, + /// Binders/sorts were erased to get a match. + Skeleton, + /// The statement did not parse into a term; keyed on normalised text. + Text, +} + +impl KeyTier { + pub fn as_str(self) -> &'static str { + match self { + KeyTier::Structural => "structural", + KeyTier::Skeleton => "skeleton", + KeyTier::Text => "text", + } + } +} + +/// A declaration's structural identity. +#[derive(Debug, Clone, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct StructuralKey { + /// Version of the normalisation rules that produced this key. + pub scheme: String, + /// Canonical prefix shape, binders and sorts included. + pub shape: String, + /// Canonical prefix shape with binders and sorts erased. + pub skeleton: String, + /// SHA-256 of `shape`, hex. + pub key: String, + /// SHA-256 of `skeleton`, hex. + pub skeleton_key: String, + /// Which tier this declaration's shape is trustworthy at. + pub tier: KeyTier, +} + +// =========================================================================== +// Vocabulary +// =========================================================================== + +/// Operator spellings → canonical operator. Lookup is on the *last* +/// component of a dotted name and is case-insensitive. +fn op_of(name: &str) -> Option<&'static str> { + let raw = unqualify(name); + let low = raw.to_lowercase(); + let op = match low.as_str() { + // arithmetic + "+" | "add" | "plus" | "hadd" | "bvadd" | "addn" => "ADD", + "*" | "mul" | "times" | "hmul" | "bvmul" | "muln" => "MUL", + "-" | "sub" | "minus" | "hsub" | "bvsub" => "SUB", + "/" | "div" | "bvsdiv" => "DIV", + "%" | "mod" | "bvsmod" => "MOD", + // relations + "=" | "==" | "≡" | "eq" | "beq" => "EQ", + "≠" | "!=" | "<>" => "NEQ", + "<" | "lt" | "bvslt" => "LT", + "<=" | "≤" | "le" | "bvsle" => "LE", + ">" | "gt" | "bvsgt" => "GT", + ">=" | "≥" | "ge" | "bvsge" => "GE", + // logic + "∧" | "and" | "/\\" | "&&" | "conj" => "AND", + "∨" | "or" | "\\/" | "||" | "disj" => "OR", + "¬" | "not" => "NOT", + "→" | "->" | "⟶" => "ARROW", + "↔" | "<->" | "<=>" | "iff" => "IFF", + "∈" | "in" => "IN", + "++" | "append" => "APPEND", + _ => return None, + }; + Some(op) +} + +/// Infix precedence. `ARROW`/`IFF` are right-associative, the rest are +/// left-associative (see [`Parser::expr`]). +fn precedence(op: &str) -> Option { + let p = match op { + "IFF" => 5, + "ARROW" => 7, + "OR" => 8, + "AND" => 9, + "EQ" | "NEQ" | "IN" => 10, + "LT" | "LE" | "GT" | "GE" => 20, + "ADD" | "SUB" | "APPEND" => 30, + "MUL" | "DIV" | "MOD" => 40, + _ => return None, + }; + Some(p) +} + +/// Sort aliases. Deliberately does *not* include single letters (`n`, `z`, +/// `b`): those are variable names in real statements far more often than +/// they are sort names. +fn sort_of(name: &str) -> Option<&'static str> { + let low = unqualify(name).to_lowercase(); + let s = match low.as_str() { + "nat" | "ℕ" | "natural" => "NAT", + "int" | "ℤ" | "integer" => "INT", + "bool" | "𝔹" | "boolean" => "BOOL", + "real" | "ℝ" => "REAL", + "prop" | "set" | "type" | "sort" | "type0" | "universe" => "TYPE", + "string" | "text" => "STRING", + "list" => "LIST", + "vector" | "vect" => "VEC", + _ => return None, + }; + Some(s) +} + +fn is_pi_kw(name: &str) -> bool { + let low = unqualify(name).to_lowercase(); + matches!(low.as_str(), "forall" | "∀" | "pi" | "π" | "all") +} + +fn is_lam_kw(name: &str) -> bool { + let low = unqualify(name).to_lowercase(); + matches!(low.as_str(), "fun" | "lambda" | "λ" | "fn") +} + +fn is_decl_kw(name: &str) -> bool { + let low = unqualify(name).to_lowercase(); + matches!( + low.as_str(), + "theorem" + | "lemma" + | "def" + | "definition" + | "opaque" + | "axiom" + | "corollary" + | "proposition" + | "remark" + | "fact" + | "example" + | "goal" + | "assert" + | "fixpoint" + | "inductive" + | "coinductive" + | "data" + | "record" + | "function" + | "procedure" + | "declare-fun" + | "declare-const" + | "declare" + | "thm" + | "prop" + | "constant" + ) +} + +fn is_cut_kw(name: &str) -> bool { + matches!( + unqualify(name).to_lowercase().as_str(), + ":=" | "by" | "proof" | "qed" | "where" + ) +} + +/// Dotted names reduce to their last component before lookup. +fn unqualify(name: &str) -> &str { + match name.rfind('.') { + Some(i) if i + 1 < name.len() => &name[i + 1..], + _ => name, + } +} + +// =========================================================================== +// Lexer +// =========================================================================== + +#[derive(Debug, Clone, PartialEq, Eq)] +enum Tk { + /// A source identifier (candidate variable, sort, name or operator). + Id(String), + /// An identifier that must not be re-read as an operator (`_<_` …). + Name(String), + Num(String), + Sym(String), + Open(char), + Close(char), +} + +const MULTI: [&str; 19] = [ + "<->", "<=>", "-->", "->>", "::=", ":=", "->", "=>", "<=", ">=", "!=", "==", "/\\", "\\/", + "&&", "||", "::", "++", "<>", +]; + +fn is_ident_start(c: char) -> bool { + c.is_alphanumeric() || c == '_' || c == '\'' +} + +fn is_ident_char(c: char) -> bool { + c.is_alphanumeric() || c == '_' || c == '\'' +} + +fn lex(src: &str) -> Vec { + let chars: Vec = src.chars().collect(); + let n = chars.len(); + let mut out: Vec = Vec::new(); + let mut i = 0usize; + while i < n { + let c = chars[i]; + if c.is_whitespace() { + i += 1; + continue; + } + // line comments + if (c == '-' && i + 1 < n && chars[i + 1] == '-') + || (c == '/' && i + 1 < n && chars[i + 1] == '/') + { + while i < n && chars[i] != '\n' { + i += 1; + } + continue; + } + // block comment + if c == '(' && i + 1 < n && chars[i + 1] == '*' { + i += 2; + while i + 1 < n && !(chars[i] == '*' && chars[i + 1] == ')') { + i += 1; + } + i = (i + 2).min(n); + continue; + } + // quoted statement (Isabelle quotes the whole formula) + if c == '"' { + let mut j = i + 1; + while j < n && chars[j] != '"' { + j += 1; + } + let inner: String = chars[i + 1..j.min(n)].iter().collect(); + out.extend(lex(&inner)); + i = j + 1; + continue; + } + // multi-character symbols (longest match first) + let mut matched: Option<&str> = None; + for m in MULTI { + let mchars: Vec = m.chars().collect(); + if chars[i..].starts_with(&mchars) { + matched = Some(m); + break; + } + } + if let Some(m) = matched { + out.push(Tk::Sym(m.to_string())); + i += m.chars().count(); + continue; + } + if c == '(' || c == '[' || c == '{' { + out.push(Tk::Open(c)); + i += 1; + continue; + } + if c == ')' || c == ']' || c == '}' { + out.push(Tk::Close(c)); + i += 1; + continue; + } + if is_ident_start(c) || c == '.' { + let mut j = i; + while j < n && is_ident_char(chars[j]) { + j += 1; + } + // dotted qualification: only when an identifier continues + while j + 1 < n && chars[j] == '.' && is_ident_start(chars[j + 1]) { + j += 1; + while j < n && is_ident_char(chars[j]) { + j += 1; + } + } + if j == i { + out.push(Tk::Sym(c.to_string())); + i += 1; + continue; + } + let text: String = chars[i..j].iter().collect(); + let is_num = text.chars().all(|ch| ch.is_ascii_digit()); + out.push(if is_num { Tk::Num(text) } else { Tk::Id(text) }); + i = j; + continue; + } + out.push(Tk::Sym(c.to_string())); + i += 1; + } + out +} + +// =========================================================================== +// Token pre-pass +// =========================================================================== + +fn token_text(t: &Tk) -> String { + match t { + Tk::Id(s) | Tk::Name(s) | Tk::Num(s) | Tk::Sym(s) => s.clone(), + Tk::Open(c) | Tk::Close(c) => c.to_string(), + } +} + +fn is_open(t: &Tk) -> bool { + matches!(t, Tk::Open(_)) +} + +fn is_close(t: &Tk) -> bool { + matches!(t, Tk::Close(_)) +} + +/// Index of the bracket matching `toks[at]` (an opening bracket), or the +/// last index when unbalanced. +fn matching(toks: &[Tk], at: usize) -> usize { + let mut depth = 0usize; + for (j, t) in toks.iter().enumerate().skip(at) { + if is_open(t) { + depth += 1; + } else if is_close(t) { + depth = depth.saturating_sub(1); + if depth == 0 { + return j; + } + } + } + toks.len().saturating_sub(1) +} + +/// Agda writes operators as names: `_<_`, `_+_`, `_≡_`. Read the wrapped +/// symbol as one atom so it is not mistaken for three punctuation tokens. +fn glue_agda_operators(toks: &[Tk]) -> Vec { + let mut out: Vec = Vec::new(); + let mut i = 0usize; + while i < toks.len() { + let is_underscore = matches!(&toks[i], Tk::Id(s) if s == "_"); + if is_underscore && i + 2 < toks.len() { + let inner = match &toks[i + 1] { + Tk::Sym(s) => Some(s.clone()), + Tk::Id(s) if s == "_" => Some(s.clone()), + _ => None, + }; + let closes = matches!(&toks[i + 2], Tk::Id(s) if s == "_" || s == "'_" || s == "_'"); + if let (Some(sym), true) = (inner, closes) { + let canon = op_of(&sym).map(|s| s.to_string()).unwrap_or(sym); + out.push(Tk::Name(canon)); + i += 3; + if i < toks.len() && matches!(&toks[i], Tk::Id(s) if s == "'") { + i += 1; + } + continue; + } + } + out.push(toks[i].clone()); + i += 1; + } + out +} + +/// A binder group is `x y : T`; `(A -> B)` is a type and must not be +/// mistaken for one. +fn has_colon(toks: &[Tk]) -> bool { + toks.iter() + .any(|t| matches!(t, Tk::Sym(s) if s == ":" || s == "::")) +} + +/// `+-comm : body` and `addComm : body` and `: Π …` all have the declared +/// name before a top-level colon; drop it. A group that starts the +/// statement (`(x y : Nat) : body`) means there is no head to drop. +fn drop_declared_head(toks: Vec) -> Vec { + let mut depth = 0usize; + for (i, t) in toks.iter().enumerate() { + if is_open(t) { + if depth == 0 { + return toks[i..].to_vec(); + } + depth += 1; + } else if is_close(t) { + depth = depth.saturating_sub(1); + } else if depth == 0 { + if let Tk::Sym(s) = t { + if s == ":" || s == "::=" { + return toks[i + 1..].to_vec(); + } + } + if let Tk::Id(s) = t { + if is_pi_kw(s) || is_lam_kw(s) { + return toks[i..].to_vec(); + } + } + } + } + toks +} + +/// `(assert (forall …))` → `(forall …)`. +fn unwrap_assert(toks: Vec) -> Vec { + let mut cur = toks; + loop { + if !cur.first().map(is_open).unwrap_or(false) { + return cur; + } + let j = matching(&cur, 0); + if j + 1 != cur.len() { + return cur; + } + let inner = cur[1..j].to_vec(); + let head_is_assert = match inner.first() { + Some(Tk::Id(s)) => matches!( + s.to_lowercase().as_str(), + "assert" | "goal" | "check-sat" | "theorem" + ), + _ => false, + }; + if !head_is_assert { + return cur; + } + cur = inner[1..].to_vec(); + } +} + +fn strip_header(toks: &[Tk]) -> Vec { + let mut cur = unwrap_assert(glue_agda_operators(toks)); + // declaration keyword + declared name + loop { + let drops_kw = matches!(cur.first(), Some(Tk::Id(s)) if is_decl_kw(s)); + if !drops_kw { + break; + } + cur.remove(0); + if matches!(cur.first(), Some(Tk::Id(_))) { + cur.remove(0); + } + } + // proof body begins at a top-level `:=` / `by` / `where` + let mut depth = 0usize; + let mut cut: Option = None; + for (i, t) in cur.iter().enumerate() { + if is_open(t) { + depth += 1; + } else if is_close(t) { + depth = depth.saturating_sub(1); + } else if depth == 0 { + let text = token_text(t); + if is_cut_kw(&text) || text == ":=" { + cut = Some(i); + break; + } + } + } + let cur = match cut { + Some(i) => cur[..i].to_vec(), + None => cur, + }; + drop_declared_head(cur) +} + +/// `x y : Nat` → (["x","y"], NAT); SMT-LIB `x Nat` likewise. +fn split_binder_group(inner: &[Tk]) -> (Vec, String) { + let mut names: Vec = Vec::new(); + for (k, t) in inner.iter().enumerate() { + if let Tk::Sym(s) = t { + if s == ":" || s == "::" { + return (names, sort_name(&inner[k + 1..])); + } + } + if let Tk::Id(s) = t { + names.push(s.clone()); + } + } + if names.len() == 2 && !inner.iter().any(|t| matches!(t, Tk::Sym(_))) { + let sort = sort_of(&names[1]) + .map(|s| s.to_string()) + .unwrap_or_else(|| names[1].to_uppercase()); + return (vec![names[0].clone()], sort); + } + (names, "?".to_string()) +} + +fn sort_name(toks: &[Tk]) -> String { + for t in toks { + if let Tk::Id(s) = t { + return sort_of(s) + .map(|s| s.to_string()) + .unwrap_or_else(|| unqualify(s).to_uppercase()); + } + } + "?".to_string() +} + +/// Declared binders, in declaration order, with their sorts. +#[derive(Debug, Clone, Default)] +struct Binders { + names: Vec, + sorts: Vec, +} + +impl Binders { + fn push(&mut self, names: &[String], sort: &str) { + for n in names { + self.names.push(n.clone()); + self.sorts.push(sort.to_string()); + } + } +} + +/// Remove binder syntax from the stream, recording what was bound. +/// +/// Handles the four shapes that actually occur: SMT-LIB +/// `(forall ((x Nat) (y Nat)) …)`, keyword binders `forall x y : T, …` / +/// `∀ (x y : T) → …` / `Π (x y : Nat), …`, keyword-less leading groups +/// (`theorem f (x y : Nat) : …`, `f : (x, y : Nat) -> …`), and Isabelle's +/// `(x::nat)` ascriptions (which bind nothing). +fn extract_binders(toks: &[Tk]) -> (Vec, Binders) { + let mut bound = Binders::default(); + let mut cur: Vec = toks.to_vec(); + + // 1. leading binder group without a keyword + while cur.first().map(is_open).unwrap_or(false) { + let j = matching(&cur, 0); + let (names, sort) = split_binder_group(&cur[1..j]); + if names.is_empty() { + break; + } + let after_ok = cur + .get(j + 1) + .map(|t| matches!(t, Tk::Sym(s) if s == ":" || s == "->" || s == "→" || s == ",")) + .unwrap_or(false); + if !after_ok { + break; + } + if !has_colon(&cur[1..j]) { + break; + } + for n in &names { + bound.push(std::slice::from_ref(n), &sort); + } + cur = cur[(j + 2).min(cur.len())..].to_vec(); + } + + // 2. SMT-LIB: the whole statement is `(forall ((x Nat) (y Nat)) body)` + if cur.first().map(is_open).unwrap_or(false) { + let j = matching(&cur, 0); + if j + 1 == cur.len() { + let inner: Vec = cur[1..j].to_vec(); + let head_ok = matches!(inner.first(), Some(Tk::Id(s)) if is_pi_kw(s) || is_lam_kw(s)); + if head_ok { + let rest: Vec = inner[1..].to_vec(); + if rest.first().map(is_open).unwrap_or(false) { + let m = matching(&rest, 0); + let group: Vec = rest[1..m].to_vec(); + let mut names: Vec = Vec::new(); + let mut sorts: Vec = Vec::new(); + if group.first().map(is_open).unwrap_or(false) { + let mut k = 0usize; + while k < group.len() && is_open(&group[k]) { + let e = matching(&group, k); + let (n, s) = split_binder_group(&group[k + 1..e]); + for name in n { + names.push(name); + sorts.push(s.clone()); + } + k = e + 1; + } + } else { + let (n, s) = split_binder_group(&group); + for name in n { + names.push(name); + sorts.push(s.clone()); + } + } + if !names.is_empty() { + for (name, sort) in names.iter().zip(sorts.iter()) { + bound.push(std::slice::from_ref(name), sort); + } + cur = rest[m + 1..].to_vec(); + } + } + } + } + } + + // 3. keyword binders anywhere at the head of the remaining stream + let mut out: Vec = Vec::new(); + let mut i = 0usize; + while i < cur.len() { + let head_ok = match &cur[i] { + Tk::Id(s) => is_pi_kw(s) || is_lam_kw(s), + Tk::Sym(s) => is_pi_kw(s) || is_lam_kw(s), + _ => false, + }; + if !head_ok { + out.push(cur[i].clone()); + i += 1; + continue; + } + i += 1; + let mut names: Vec = Vec::new(); + let mut sorts: Vec = Vec::new(); + let mut pending: Vec = Vec::new(); + while i < cur.len() { + let stop = matches!(&cur[i], Tk::Sym(s) if s == "," || s == "." || s == "->" || s == "→" || s == "=>"); + if stop { + for n in pending.drain(..) { + names.push(n); + sorts.push("?".to_string()); + } + i += 1; + break; + } + if is_open(&cur[i]) { + let m = matching(&cur, i); + let (n, s) = split_binder_group(&cur[i + 1..m]); + if n.is_empty() { + break; + } + for name in n { + names.push(name); + sorts.push(s.clone()); + } + i = m + 1; + continue; + } + if let Tk::Id(name) = cur[i].clone() { + let next_colon = matches!( + cur.get(i + 1), + Some(Tk::Sym(s)) if s == ":" || s == "::" + ); + if next_colon { + let mut k = i + 2; + let mut st: Vec = Vec::new(); + while k < cur.len() { + let terminator = is_close(&cur[k]) + || matches!(&cur[k], Tk::Sym(s) if s == "," || s == "." || s == "->" || s == "→"); + if terminator { + break; + } + st.push(cur[k].clone()); + k += 1; + } + pending.push(name); + for n in pending.drain(..) { + names.push(n); + sorts.push(sort_name(&st)); + } + i = k; + continue; + } + pending.push(name); + i += 1; + continue; + } + break; + } + for n in pending.drain(..) { + names.push(n); + sorts.push("?".to_string()); + } + if !names.is_empty() { + for (name, sort) in names.iter().zip(sorts.iter()) { + bound.push(std::slice::from_ref(name), sort); + } + } + } + (out, bound) +} + +/// Isabelle's `(x :: nat)` is a term ascription, not a binder. +fn drop_ascriptions(toks: &[Tk]) -> Vec { + let mut out: Vec = Vec::new(); + let mut i = 0usize; + while i < toks.len() { + if is_open(&toks[i]) { + let j = matching(toks, i); + let inner: Vec = toks[i + 1..j].to_vec(); + let ids: Vec<&String> = inner + .iter() + .filter_map(|t| match t { + Tk::Id(s) => Some(s), + _ => None, + }) + .collect(); + let syms: Vec<&String> = inner + .iter() + .filter_map(|t| match t { + Tk::Sym(s) => Some(s), + _ => None, + }) + .collect(); + if ids.len() == 2 && syms.len() == 1 && syms[0] == "::" && sort_of(ids[1]).is_some() { + out.push(Tk::Id(ids[0].clone())); + i = j + 1; + continue; + } + } + out.push(toks[i].clone()); + i += 1; + } + out +} + +// =========================================================================== +// Term +// =========================================================================== + +#[derive(Debug, Clone, PartialEq, Eq)] +enum Node { + Var(String), + Name(String), + Num(String), + Sort(String), + Hole, + Op(&'static str, Vec), + App(Vec), +} + +struct Parser { + toks: Vec, + i: usize, + varmap: std::collections::HashMap, +} + +impl Parser { + fn new(toks: Vec, varmap: std::collections::HashMap) -> Self { + Parser { toks, i: 0, varmap } + } + + fn peek(&self) -> Option<&Tk> { + self.toks.get(self.i) + } + + /// Canonical operator starting at the cursor, if any. + fn op_at(&self) -> Option<&'static str> { + match self.peek()? { + Tk::Id(s) | Tk::Sym(s) => op_of(s), + _ => None, + } + } + + fn atom(&mut self) -> Option { + let t = self.peek()?.clone(); + match t { + Tk::Open(_) => { + self.i += 1; + let inner = self.expr(0); + if matches!(self.peek(), Some(Tk::Close(_))) { + self.i += 1; + } + Some(inner) + }, + Tk::Close(_) => None, + Tk::Num(s) => { + self.i += 1; + Some(Node::Num(s)) + }, + Tk::Name(s) => { + self.i += 1; + Some(Node::Name(s)) + }, + Tk::Sym(s) => { + if s == ":" || s == "::" || s == "," || s == "." { + self.i += 1; + return None; + } + match op_of(&s) { + Some(op) => { + self.i += 1; + Some(Node::Op(op, Vec::new())) + }, + None => { + self.i += 1; + Some(Node::Name(s)) + }, + } + }, + Tk::Id(s) => { + self.i += 1; + if let Some(v) = self.varmap.get(&s).cloned() { + return Some(Node::Var(v)); + } + if let Some(op) = op_of(&s) { + return Some(Node::Op(op, Vec::new())); + } + if let Some(sort) = sort_of(&s) { + return Some(Node::Sort(sort.to_string())); + } + Some(Node::Name(unqualify(&s).to_string())) + }, + } + } + + /// Application, including prefix operator use: `(+ x y)`. + fn app(&mut self) -> Node { + let head = match self.atom() { + Some(h) => h, + None => return Node::Hole, + }; + if let Node::Op(op, _) = head.clone() { + let mut args: Vec = Vec::new(); + loop { + let stop = match self.peek() { + None => true, + Some(t) => is_close(t) || self.op_at().is_some(), + }; + if stop { + break; + } + match self.atom() { + Some(a) => args.push(a), + None => break, + } + } + let op_name = op; + // Dedukti/SMT-LIB write the sort explicitly: `eq Nat a b`. + if args.len() == 3 + && matches!(args[0], Node::Sort(_)) + && matches!(op_name, "EQ" | "NEQ" | "LT" | "LE" | "GT" | "GE") + { + args.remove(0); + } + if args.is_empty() { + return Node::Name(op_name.to_string()); + } + return Node::Op(op_name, args); + } + let mut args: Vec = vec![head.clone()]; + loop { + match self.peek() { + None => break, + Some(t) => { + if is_close(t) || self.op_at().is_some() { + break; + } + if matches!(t, Tk::Sym(s) if s == "," || s == ":" || s == "::" || s == ".") { + break; + } + }, + } + match self.atom() { + Some(a) => args.push(a), + None => break, + } + } + if args.len() == 1 { + return args.remove(0); + } + Node::App(args) + } + + fn expr(&mut self, min_prec: u8) -> Node { + let mut left = self.app(); + loop { + let op = match self.op_at() { + Some(op) => op, + None => break, + }; + let prec = match precedence(op) { + Some(p) => p, + None => break, + }; + if prec < min_prec { + break; + } + self.i += 1; + let rhs_min = if op == "ARROW" || op == "IFF" { + prec + } else { + prec + 1 + }; + let right = self.expr(rhs_min); + left = Node::Op(op, vec![left, right]); + } + left + } +} + +fn render(node: &Node, skeleton: bool) -> String { + match node { + Node::Var(s) | Node::Name(s) | Node::Num(s) => s.clone(), + Node::Sort(s) => { + if skeleton { + "?".to_string() + } else { + s.clone() + } + }, + Node::Hole => "_".to_string(), + Node::Op(op, kids) => { + let mut out = String::from("("); + out.push_str(op); + for k in kids { + out.push(' '); + out.push_str(&render(k, skeleton)); + } + out.push(')'); + out + }, + Node::App(kids) => { + let mut out = String::from("("); + for (i, k) in kids.iter().enumerate() { + if i > 0 { + out.push(' '); + } + out.push_str(&render(k, skeleton)); + } + out.push(')'); + out + }, + } +} + +// =========================================================================== +// Public API +// =========================================================================== + +fn sha256_hex(s: &str) -> String { + let mut h = Sha256::new(); + h.update(s.as_bytes()); + let digest = h.finalize(); + let mut out = String::with_capacity(digest.len() * 2); + for b in digest.iter() { + out.push_str(&format!("{:02x}", b)); + } + out +} + +/// Normalised text, used as the last-resort tier when a statement does not +/// parse into a term at all (a bare type name, a stray data declaration). +fn text_shape(statement: &str) -> String { + statement + .split_whitespace() + .collect::>() + .join(" ") + .to_lowercase() +} + +fn is_blank_shape(shape: &str) -> bool { + let trimmed = shape.trim(); + trimmed.is_empty() || trimmed == "_" || trimmed == "()" || trimmed.chars().all(|c| c == '?') +} + +/// Number every variable `v0`, `v1`, … in order of first appearance. +/// +/// A name counts as a variable when it is a declared binder, a short +/// lower-case name (`x`, `xs`, `p'`), or a single upper-case letter (`A`, +/// the Coq/Lean convention for a type variable). Sorts and canonical +/// operators never become variables, whatever they look like. +fn number_variables(body: &[Tk], bound: &Binders) -> std::collections::HashMap { + let mut varmap: std::collections::HashMap = std::collections::HashMap::new(); + let mut next = 0usize; + for t in body { + let name = match t { + Tk::Id(name) => name, + _ => continue, + }; + if sort_of(name).is_some() || op_of(name).is_some() || is_pi_kw(name) || is_lam_kw(name) { + continue; + } + let tail = unqualify(name); + let looks_like_var = bound.names.iter().any(|n| n == name) + || match tail.chars().next() { + Some(c) if c.is_lowercase() => tail.chars().count() <= 3, + Some(c) if c.is_uppercase() => tail.chars().count() == 1, + _ => false, + }; + if looks_like_var && !varmap.contains_key(name) { + varmap.insert(name.clone(), format!("v{}", next)); + next += 1; + } + } + varmap +} + +/// Both canonical forms from one pass: `(shape, skeleton)`. +fn normalise(statement: &str) -> (String, String) { + let toks = strip_header(&lex(statement)); + let toks = drop_ascriptions(&toks); + let (body, bound) = extract_binders(&toks); + let varmap = number_variables(&body, &bound); + let ast = Parser::new(body, varmap).expr(0); + + let core = render(&ast, false); + let skel = render(&ast, true); + + let mut shape = if is_blank_shape(&core) { + String::new() + } else { + core + }; + if !shape.is_empty() && !bound.names.is_empty() { + shape = format!("(PI [{}] {})", bound.sorts.join(" "), shape); + } + let skeleton = if is_blank_shape(&skel) { + String::new() + } else { + skel + }; + (shape, skeleton) +} + +/// Canonical prefix shape of `statement`, binder prefix included. +pub fn canonical_shape(statement: &str) -> String { + normalise(statement).0 +} + +/// Same normalisation as [`canonical_shape`] with binders and sorts erased. +pub fn canonical_skeleton(statement: &str) -> String { + normalise(statement).1 +} + +/// Structural identity of a declaration's statement. +/// +/// The three tiers are tried in order: the shape as written; the shape with +/// binders and sorts erased (covers provers that elide them); and finally +/// whitespace-normalised text (covers statements that are not terms). +pub fn structural_key(statement: &str) -> StructuralKey { + let (shape, skeleton) = normalise(statement); + + let (shape, skeleton, tier) = if !shape.is_empty() { + (shape, skeleton, KeyTier::Structural) + } else if !skeleton.is_empty() { + (skeleton.clone(), skeleton, KeyTier::Skeleton) + } else { + let text = text_shape(statement); + (text.clone(), text, KeyTier::Text) + }; + + StructuralKey { + scheme: SCHEME.to_string(), + key: sha256_hex(&shape), + skeleton_key: sha256_hex(&skeleton), + shape, + skeleton, + tier, + } +} + +/// Canonical atoms of a statement, for the structural embedder's n-grams. +/// +/// Falls back to the lower-cased source tokens when the statement does not +/// parse, so every declaration contributes *something*. +pub fn canonical_tokens(statement: &str) -> Vec { + let shape = canonical_shape(statement); + let source = if shape.is_empty() { + text_shape(statement) + } else { + shape + }; + source + .split(|c: char| c.is_whitespace() || c == '(' || c == ')' || c == '[' || c == ']') + .filter(|t| !t.is_empty()) + .map(|t| t.to_string()) + .collect() +} + +#[cfg(test)] +mod tests { + use super::*; + + const ADD_COMM: [(&str, &str); 8] = [ + ("agda", "+-comm : ∀ (x y : ℕ) → x + y ≡ y + x"), + ("coq", "Lemma add_comm : forall x y : nat, x + y = y + x."), + ( + "lean4", + "theorem Nat.add_comm (x y : Nat) : x + y = y + x := by omega", + ), + ("idris2", "addComm : (x, y : Nat) -> x + y = y + x"), + ("isabelle", "lemma add_comm: \"(x::nat) + y = y + x\""), + ("why3", "lemma add_comm: forall x y: int. x + y = y + x"), + ( + "smtlib", + "(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).", + ), + ]; + + #[test] + fn add_comm_is_one_shape_across_the_explicit_binder_provers() { + let expected = "(PI [NAT NAT] (EQ (ADD v0 v1) (ADD v1 v0)))"; + for (lang, src) in ADD_COMM { + if lang == "isabelle" || lang == "why3" { + continue; // elided binders / different sort: see the skeleton test + } + assert_eq!(canonical_shape(src), expected, "{lang} disagrees"); + } + } + + #[test] + fn add_comm_skeleton_covers_the_eliding_provers() { + let expected = "(EQ (ADD v0 v1) (ADD v1 v0))"; + for (lang, src) in ADD_COMM { + assert_eq!(canonical_skeleton(src), expected, "{lang} disagrees"); + } + } + + #[test] + fn structural_key_agrees_across_languages() { + let coq = structural_key(ADD_COMM[1].1); + let lean = structural_key(ADD_COMM[2].1); + let idris = structural_key(ADD_COMM[3].1); + let smt = structural_key(ADD_COMM[6].1); + let dk = structural_key(ADD_COMM[7].1); + for k in [&lean, &idris, &smt, &dk] { + assert_eq!(k.key, coq.key, "primary key drifted: {}", k.shape); + } + // Isabelle states the same theorem without binders or an explicit + // sort; it must still join on the skeleton. + let isabelle = structural_key(ADD_COMM[4].1); + assert_eq!(isabelle.skeleton_key, coq.skeleton_key); + assert_eq!(coq.tier, KeyTier::Structural); + } + + #[test] + fn alpha_renaming_does_not_change_the_key() { + let a = structural_key("Lemma c : forall x y : nat, x + y = y + x."); + let b = structural_key("Lemma c : forall a b : nat, a + b = b + a."); + assert_eq!(a.key, b.key); + assert_eq!(a.shape, b.shape); + } + + #[test] + fn different_statements_keep_different_keys() { + let comm = structural_key("forall x y : nat, x + y = y + x"); + let assoc = structural_key("forall x y z : nat, (x + y) + z = x + (y + z)"); + assert_ne!(comm.key, assoc.key); + // a free-variable statement must not collapse into a constant + assert_ne!(comm.key, structural_key("").key); + } + + #[test] + fn arrows_are_right_associative_like_the_toolchains() { + let coq = canonical_shape("Definition compose : (B -> C) -> (A -> B) -> A -> C."); + let lean = canonical_shape("theorem compose : (B -> C) -> (A -> B) -> A -> C"); + assert_eq!( + coq, + "(ARROW (ARROW v0 v1) (ARROW (ARROW v2 v0) (ARROW v2 v1)))" + ); + assert_eq!(coq, lean); + } + + #[test] + fn deduction_headers_and_bodies_are_dropped() { + let with_body = structural_key("theorem add_zero (n : Nat) : n + 0 = n := by simp"); + let without = structural_key("theorem add_zero (n : Nat) : n + 0 = n"); + assert_eq!(with_body.key, without.key); + assert_eq!(with_body.shape, "(PI [NAT] (EQ (ADD v0 0) v0))"); + } + + #[test] + fn statements_with_no_term_fall_back_to_text() { + // `data … where …` has no type expression before the `where` cut, + // so there is nothing to key on structurally. + let k = structural_key("data Bool where true false"); + assert_eq!(k.tier, KeyTier::Text); + assert_eq!(k.shape, "data bool where true false"); + assert_eq!(k.key.len(), 64); + assert_ne!(k.key, structural_key("data Nat where zero suc").key); + // whitespace is not part of the text tier + assert_eq!( + k.key, + structural_key(" data Bool\n where true false ").key + ); + } + + #[test] + fn scheme_is_versioned() { + let k = structural_key("forall n : nat, n = n"); + assert_eq!(k.scheme, SCHEME); + assert_eq!(k.key.len(), 64); + assert_eq!(k.skeleton_key.len(), 64); + } + + #[test] + fn canonical_tokens_are_atoms_not_punctuation() { + let toks = canonical_tokens("forall x y : nat, x + y = y + x"); + assert!(toks.contains(&"ADD".to_string())); + assert!(toks.contains(&"EQ".to_string())); + assert!(toks.contains(&"v0".to_string())); + assert!(!toks.iter().any(|t| t.contains("forall"))); + } +} diff --git a/src/rust/corpus/creusot.rs b/src/rust/corpus/creusot.rs index 71b5a58c..8df3629d 100644 --- a/src/rust/corpus/creusot.rs +++ b/src/rust/corpus/creusot.rs @@ -478,10 +478,9 @@ pub(crate) fn parse_rust_file(src: &str) -> ParsedFile { let clean = clean_source(src); let toks = tokenise(&clean); let attrs = collect_attrs(src, &toks); - let mut parsed = ParsedFile { - imports: collect_uses(src, &toks), - ..ParsedFile::default() - }; + let mut parsed = ParsedFile::default(); + + parsed.imports = collect_uses(src, &toks); let mut k = 0; while k < toks.len() { @@ -492,10 +491,9 @@ pub(crate) fn parse_rust_file(src: &str) -> ParsedFile { (DeclKind::Data, k + 1) } else if is_kw(t, "trait") { (DeclKind::Record, k + 1) - } else if is_kw(t, "type") - || is_kw(t, "static") - || (is_kw(t, "const") && !(k + 1 < toks.len() && is_kw(&toks[k + 1], "fn"))) - { + } else if is_kw(t, "type") || is_kw(t, "static") { + (DeclKind::Data, k + 1) + } else if is_kw(t, "const") && !(k + 1 < toks.len() && is_kw(&toks[k + 1], "fn")) { (DeclKind::Data, k + 1) } else { k += 1; @@ -567,10 +565,10 @@ pub(crate) fn parse_rust_file(src: &str) -> ParsedFile { axiom_usage, }); - if has_attr(&leading, "cfg(creusot)") - && !parsed.options.iter().any(|o| o == "creusot-gated") - { - parsed.options.push("creusot-gated".to_string()); + if has_attr(&leading, "cfg(creusot)") { + if !parsed.options.iter().any(|o| o == "creusot-gated") { + parsed.options.push("creusot-gated".to_string()); + } } k = advance.max(k + 1); diff --git a/src/rust/corpus/embed.rs b/src/rust/corpus/embed.rs index a47955f0..0d7de3e6 100644 --- a/src/rust/corpus/embed.rs +++ b/src/rust/corpus/embed.rs @@ -4,20 +4,28 @@ //! Vector-octad embeddings for the corpus — Step 5 of the N-dim //! VeriSim plan. //! -//! Two backends: +//! Three backends: //! -//! 1. **Hashing-trick** (default, offline): tokenise statement + -//! proof on whitespace + Agda-syntax separators, hash each token -//! into one of 32 buckets, accumulate L2-normalised counts. Free, -//! deterministic, no network. Good enough for cosine-similarity -//! nearest-neighbour queries over shared vocabulary, which is -//! exactly what the SA / MCTS prior layer needs. +//! 1. **Structural n-gram hashing** (default, offline): normalise the +//! statement through [`super::canonical`], then hash its 1-, 2- and +//! 3-grams of canonical atoms into 256 buckets, weighted by n-gram +//! order and L2-normalised. Because the input is the *canonical* +//! token stream, `x + y = y + x` in Coq and `(+ x y) = (+ y x)` in +//! SMT-LIB land on the same buckets — the vector carries type +//! structure, not surface spelling. Still free, deterministic and +//! offline, and still no training run: it is the baseline the Flux +//! GNN is measured against, not a replacement for it. //! -//! 2. **GNN client** (future, online): for when the Julia server at +//! 2. **Hashing-trick over raw text** ([`HashEmbedder`], 32-dim): the +//! original backend, kept because `src/rust/gnn/embeddings.rs` +//! fixes `FEATURE_DIM = 32` for node features and some deployments +//! want the narrow, GNN-compatible vector. +//! +//! 3. **GNN client** (future, online): for when the Julia server at //! `/gnn/embed` is primed against real proof corpora (Wave-3 ML //! work tracked in `docs/handover/TODO.adoc`). The trait `Embedder` -//! abstracts the choice; replacing the default `HashEmbedder` -//! with a `GnnEmbedder` is one-line. +//! abstracts the choice; replacing the default +//! [`StructuralEmbedder`] with a `GnnEmbedder` is one-line. //! //! The corpus's `compute_embeddings` returns `Vec>` parallel //! to `entries`; `octad.rs::save_octads_jsonl` populates each Vector @@ -29,13 +37,24 @@ use serde::{Deserialize, Serialize}; use super::{Corpus, CorpusEntry}; -/// Embedding dimension used by the default hashing-trick embedder. -/// Chosen to match the 32-dim GNN local-term embeddings already -/// shipped in `src/rust/gnn/embeddings.rs` (`FEATURE_DIM = 32`), so -/// stored octads can be later re-embedded from the GNN client without +/// Embedding dimension of the *legacy* raw-text hashing-trick +/// embedder. Chosen to match the 32-dim GNN local-term embeddings +/// already shipped in `src/rust/gnn/embeddings.rs` (`FEATURE_DIM = 32`), +/// so stored octads can be re-embedded from the GNN client without /// changing dimensions. pub const HASH_EMBED_DIM: usize = 32; +/// Embedding dimension of the default structural embedder (E7 +/// `VectorModality`). 256 buckets is enough to keep 1–3-gram +/// collisions rare on the estate's corpora while staying trivially +/// hashable, sortable and comparable — the point is a usable +/// similarity baseline before any trained model exists. +pub const STRUCTURAL_EMBED_DIM: usize = 256; + +/// Weights applied to 1-, 2- and 3-grams respectively. Unigrams carry +/// the vocabulary, longer n-grams carry the type structure. +const NGRAM_WEIGHTS: [f32; 3] = [1.0, 0.6, 0.35]; + #[derive(Debug, Clone, Serialize, Deserialize)] pub struct EmbedderInfo { pub model: String, @@ -47,8 +66,11 @@ pub trait Embedder { fn embed(&self, entry: &CorpusEntry) -> Vec; } -/// Default offline embedder: hashing-trick over the entry's -/// statement + proof tokens, with L2 normalisation. +/// Legacy offline embedder: hashing-trick over the entry's raw +/// statement + proof tokens, with L2 normalisation. Superseded as the +/// default by [`StructuralEmbedder`]; retained because +/// `src/rust/gnn/embeddings.rs` fixes 32-dim features and some stored +/// octads carry `echidna-corpus-hash-v1` vectors. #[derive(Debug, Clone, Default)] pub struct HashEmbedder; @@ -76,6 +98,51 @@ impl Embedder for HashEmbedder { } } +/// Default offline embedder: n-gram hashing over the *canonical* type +/// shape (see [`super::canonical`]). +/// +/// Feature layout: every unigram, bigram and trigram of the canonical +/// atom stream is hashed into one of [`STRUCTURAL_EMBED_DIM`] buckets +/// and accumulated with [`NGRAM_WEIGHTS`]; the vector is L2-normalised +/// so cosine similarity is meaningful. Deterministic, dependency-free +/// and identical on every platform. +#[derive(Debug, Clone, Default)] +pub struct StructuralEmbedder; + +impl Embedder for StructuralEmbedder { + fn info(&self) -> EmbedderInfo { + EmbedderInfo { + model: "echidna-corpus-structural-v2".to_string(), + dimensions: STRUCTURAL_EMBED_DIM, + } + } + + fn embed(&self, entry: &CorpusEntry) -> Vec { + let atoms = super::canonical::canonical_tokens(&entry.statement); + embed_atoms(&atoms) + } +} + +/// Hash a canonical atom stream into a [`STRUCTURAL_EMBED_DIM`] vector. +/// +/// Shared by entry embedding and free-text query embedding so the two +/// always live in the same space. +pub fn embed_atoms(atoms: &[String]) -> Vec { + let mut buckets = vec![0.0_f32; STRUCTURAL_EMBED_DIM]; + for n in 1..=3usize { + if atoms.len() < n { + break; + } + let weight = NGRAM_WEIGHTS[n - 1]; + for window in atoms.windows(n) { + let key = window.join("\u{1f}"); + buckets[bucket_for_dim(&key, STRUCTURAL_EMBED_DIM)] += weight; + } + } + l2_normalise(&mut buckets); + buckets +} + fn tokenise(s: &str) -> impl Iterator { s.split(|c: char| { c.is_whitespace() @@ -89,12 +156,16 @@ fn tokenise(s: &str) -> impl Iterator { /// FxHash-style fast hash; we only need stable bucketing, not crypto. fn bucket_for(tok: &str) -> usize { + bucket_for_dim(tok, HASH_EMBED_DIM) +} + +fn bucket_for_dim(tok: &str, dim: usize) -> usize { let mut h: u64 = 0xcbf29ce484222325; // FNV-1a offset for b in tok.as_bytes() { h ^= *b as u64; h = h.wrapping_mul(0x100000001b3); } - (h as usize) % HASH_EMBED_DIM + (h as usize) % dim } fn l2_normalise(v: &mut [f32]) { @@ -124,27 +195,29 @@ pub fn cosine(a: &[f32], b: &[f32]) -> f32 { impl Corpus { /// Compute embeddings for every entry using the default - /// `HashEmbedder`. Result is parallel to `self.entries`. + /// [`StructuralEmbedder`] (256-dim). Result is parallel to + /// `self.entries`. pub fn compute_embeddings(&self) -> Vec> { + let embedder = StructuralEmbedder; + self.entries.iter().map(|e| embedder.embed(e)).collect() + } + + /// Compute 32-dim GNN-compatible embeddings with the legacy + /// raw-text hashing trick. Used where a consumer expects + /// `FEATURE_DIM` vectors. + pub fn compute_embeddings_legacy(&self) -> Vec> { let embedder = HashEmbedder; self.entries.iter().map(|e| embedder.embed(e)).collect() } - /// Embed a free-form text query using the same default - /// embedder. Used for `corpus query --near `. + /// Embed a free-form text query into the same space as + /// [`Corpus::compute_embeddings`]. Used for `corpus near `, + /// which runs the query through the *same* canonicaliser so a + /// query written in one prover's syntax matches statements written + /// in another's. pub fn embed_query(&self, query: &str) -> Vec { - let synthetic = CorpusEntry { - name: String::new(), - qualified: String::new(), - module_idx: 0, - kind: super::DeclKind::Function, - statement: query.to_string(), - proof: None, - line: 0, - dependencies: vec![], - axiom_usage: super::AxiomUsage::default(), - }; - HashEmbedder.embed(&synthetic) + let atoms = super::canonical::canonical_tokens(query); + embed_atoms(&atoms) } /// Top-k nearest entries to `query_vec` by cosine similarity. @@ -218,13 +291,72 @@ mod tests { } #[test] - fn hash_embedder_dimensions() { + fn structural_embedder_is_256_dimensional_by_default() { let c = sample_corpus(); let embeds = c.compute_embeddings(); assert_eq!(embeds.len(), 3); + for v in &embeds { + assert_eq!(v.len(), STRUCTURAL_EMBED_DIM); + assert_eq!(v.len(), 256); + } + let info = StructuralEmbedder.info(); + assert_eq!(info.dimensions, STRUCTURAL_EMBED_DIM); + assert_eq!(info.model, "echidna-corpus-structural-v2"); + } + + #[test] + fn legacy_hash_embedder_stays_32_dimensional() { + let c = sample_corpus(); + let embeds = c.compute_embeddings_legacy(); + assert_eq!(embeds.len(), 3); for v in &embeds { assert_eq!(v.len(), HASH_EMBED_DIM); } + assert_eq!(HashEmbedder.info().dimensions, 32); + } + + #[test] + fn queries_match_across_prover_syntaxes() { + // An entry written the way Coq writes it, queried the way SMT-LIB + // writes it: the canonical stream is what gets hashed, so the two + // must land close together — and far from an unrelated statement. + let mut c = Corpus { + adapter: "coq".into(), + ..Default::default() + }; + c.entries.push(CorpusEntry { + name: "add_comm".into(), + qualified: "Nat.add_comm".into(), + module_idx: 0, + kind: DeclKind::Function, + statement: "forall x y : nat, x + y = y + x".into(), + proof: None, + line: 1, + dependencies: vec![], + axiom_usage: AxiomUsage::default(), + }); + c.entries.push(CorpusEntry { + name: "mul_zero".into(), + qualified: "Nat.mul_zero".into(), + module_idx: 0, + kind: DeclKind::Function, + statement: "forall n : nat, n * 0 = 0".into(), + proof: None, + line: 2, + dependencies: vec![], + axiom_usage: AxiomUsage::default(), + }); + c.reindex(); + + let embeds = c.compute_embeddings(); + let q = c.embed_query("(assert (forall ((x Nat) (y Nat)) (= (+ x y) (+ y x))))"); + let same = cosine(&q, &embeds[0]); + let other = cosine(&q, &embeds[1]); + assert!( + same > other, + "cross-syntax query should match the same theorem: {same} vs {other}" + ); + assert!(same > 0.8, "expected a close match, got {same}"); } #[test] diff --git a/src/rust/corpus/mod.rs b/src/rust/corpus/mod.rs index 15b810ae..757f09ef 100644 --- a/src/rust/corpus/mod.rs +++ b/src/rust/corpus/mod.rs @@ -46,6 +46,7 @@ #![allow(dead_code)] pub mod agda; +pub mod canonical; // Structural (alpha-normalised) type shapes — E6 identity keys pub mod coq; pub mod embed; // Vector-octad embeddings (Step 5) pub mod idris2; diff --git a/src/rust/corpus/octad.rs b/src/rust/corpus/octad.rs index 3bed3eff..1e6ee3cb 100644 --- a/src/rust/corpus/octad.rs +++ b/src/rust/corpus/octad.rs @@ -114,19 +114,49 @@ pub struct DeclDocument { } /// Graph modality — both forward and reverse edges in one place. -/// Cross-prover identity is the SHA-256 of just the adapter-stripped -/// qualified name; two entries from different adapters with the same -/// qualified name (e.g. `Brouwer.WellFounded` in Agda and Coq) match -/// on this hash. +/// Cross-prover identity. +/// +/// Two keys, because they answer different questions: +/// +/// - `cross_prover_identity_key` — SHA-256 of the **structural shape** of +/// the declaration's type (see [`super::canonical`]). This is the E6 +/// identity key: `∀ (x y : ℕ) → x + y ≡ y + x` in Agda, `Nat.add_comm` +/// in Lean, `(+ x y)` in SMT-LIB and `eq Nat (add x y) (add y x)` in +/// Dedukti all normalise to `(PI [NAT NAT] (EQ (ADD v0 v1) (ADD v1 v0)))` +/// and therefore to the same key, with no dictionary involved. +/// - `cross_prover_skeleton_key` — the same shape with binders and sorts +/// erased, for provers that elide them (Isabelle's free variables, SMT +/// scripts without explicit binders). A tier-2 join. +/// - `cross_prover_id` — the older name-tail hash. Kept because existing +/// octad files and query clients carry it; it is a *fallback*, and it +/// only ever matched declarations whose local names happened to agree. #[derive(Debug, Clone, Serialize, Deserialize)] pub struct DeclGraph { pub depends_on: Vec, pub depended_on_by: Vec, + /// Name-tail hash (legacy: names, not types). + #[serde(default)] pub cross_prover_id: String, + /// Structural identity key (E6 `cross_prover_identity_key`). + #[serde(default)] + pub cross_prover_identity_key: String, + /// Structural identity with binders and sorts erased. + #[serde(default)] + pub cross_prover_skeleton_key: String, + /// Version of the normalisation rules, e.g. `dk-shape-v1`. + #[serde(default)] + pub identity_scheme: String, + /// The canonical prefix term itself, for eyeballing and debugging. + #[serde(default)] + pub canonical_type: String, pub adapter_id: String, } -/// Vector modality — reserved for Step 5 embeddings. +/// Vector modality — structural embeddings (E7). +/// +/// Populated by [`Corpus::save_octads_jsonl`] from the canonical atom +/// stream: 256-dim structural 1–3-gram hashing, model +/// `echidna-corpus-structural-v2`. See [`super::embed`]. #[derive(Debug, Clone, Serialize, Deserialize, Default)] pub struct DeclVector { pub goal_embedding: Vec, @@ -167,6 +197,7 @@ impl DeclarationOctad { ) -> Self { let key = octad_key(adapter, &entry.qualified, &entry.statement); let cross_prover_id = cross_prover_key(&entry.qualified); + let identity = super::canonical::structural_key(&entry.statement); let content_hash = content_hash_of(entry); let semantic = DeclSemantic { @@ -226,6 +257,10 @@ impl DeclarationOctad { depends_on: entry.dependencies.clone(), depended_on_by: reverse_deps.to_vec(), cross_prover_id, + cross_prover_identity_key: identity.key.clone(), + cross_prover_skeleton_key: identity.skeleton_key.clone(), + identity_scheme: identity.scheme.clone(), + canonical_type: identity.shape.clone(), adapter_id: format!("echidna:adapter:{}", adapter), }; @@ -444,8 +479,8 @@ impl Corpus { // whole corpus (Steps 4, 5). Tensor → tensor.metrics; vectors // → vector.goal_embedding. let metrics_per_entry = self.compute_metrics(); - let embedder = super::embed::HashEmbedder; - let info = ::info(&embedder); + let embedder = super::embed::StructuralEmbedder; + let info = ::info(&embedder); let embeddings = self.compute_embeddings(); let mut out = String::new(); for (i, entry) in self.entries.iter().enumerate() { @@ -662,6 +697,71 @@ mod tests { ); } + #[test] + fn structural_identity_joins_different_syntaxes() { + // Same theorem, three surface languages, one key. This is the + // whole point of the E6 structural key: no synonym table, no + // shared naming convention. + let coq = DeclarationOctad::from_entry( + &CorpusEntry { + name: "add_comm".into(), + qualified: "Nat.add_comm".into(), + module_idx: 0, + kind: DeclKind::Function, + statement: "forall x y : nat, x + y = y + x".into(), + proof: None, + line: 1, + dependencies: vec![], + axiom_usage: AxiomUsage::default(), + }, + &ModuleEntry { + name: "Nat".into(), + path: PathBuf::from("Nat.v"), + options: vec![], + imports: vec![], + entries: vec![], + }, + "coq", + &[], + "T", + ); + let smtlib = DeclarationOctad::from_entry( + &CorpusEntry { + name: "comm".into(), + qualified: "bvadd_comm".into(), + module_idx: 0, + kind: DeclKind::Function, + statement: "(assert (forall ((x Nat) (y Nat)) (= (+ x y) (+ y x))))".into(), + proof: None, + line: 1, + dependencies: vec![], + axiom_usage: AxiomUsage::default(), + }, + &ModuleEntry { + name: "bv".into(), + path: PathBuf::from("bv.smt2"), + options: vec![], + imports: vec![], + entries: vec![], + }, + "smtlib", + &[], + "T", + ); + // The legacy name-tail hashes necessarily differ… + assert_ne!(coq.graph.cross_prover_id, smtlib.graph.cross_prover_id); + // …but the structural keys agree. + assert_eq!( + coq.graph.cross_prover_identity_key, + smtlib.graph.cross_prover_identity_key + ); + assert_eq!(coq.graph.identity_scheme, super::canonical::SCHEME); + assert_eq!( + coq.graph.canonical_type, + "(PI [NAT NAT] (EQ (ADD v0 v1) (ADD v1 v0)))" + ); + } + #[test] fn round_trip_jsonl() { let tmp = tempfile::NamedTempFile::new().expect("tmpfile"); diff --git a/src/rust/corpus/query.rs b/src/rust/corpus/query.rs index 01e40f2e..b0f3cb02 100644 --- a/src/rust/corpus/query.rs +++ b/src/rust/corpus/query.rs @@ -227,9 +227,13 @@ impl<'c> CorpusQuery<'c> { // Compute similarity (post-filter is cheaper). if let Some(qv) = &self.near_query { - let embedder = super::embed::HashEmbedder; + // Same embedder the query vector came from: the structural + // 256-dim n-gram hasher. `near_vector` callers that supply a + // foreign vector simply get 0.0 from `cosine` (dim mismatch), + // which keeps ordering stable instead of panicking. + let embedder = super::embed::StructuralEmbedder; for hit in results.iter_mut() { - let v = ::embed( + let v = ::embed( &embedder, hit.entry, ); hit.similarity = Some(cosine(qv, &v)); diff --git a/src/rust/corpus/spark_ada.rs b/src/rust/corpus/spark_ada.rs index 11cf01f8..f4b67b53 100644 --- a/src/rust/corpus/spark_ada.rs +++ b/src/rust/corpus/spark_ada.rs @@ -725,7 +725,10 @@ fn collect_imports(toks: &[Tok]) -> Vec { let mut names: Vec = Vec::new(); let mut j = i + 1; let mut terminated = false; - while let Some((name, next)) = dotted_name(toks, j) { + loop { + let Some((name, next)) = dotted_name(&toks, j) else { + break; + }; names.push(name); if next < toks.len() && is_punct(&toks[next], ",") { j = next + 1; @@ -801,11 +804,10 @@ fn body_end_idx(toks: &[Tok], from: usize, name: &str) -> Option { fn find_end_name(toks: &[Tok], from: usize, name: &str) -> Option { let mut j = from; while j + 1 < toks.len() { - if is_kw(&toks[j], "end") - && toks[j + 1].kind == TokKind::Ident - && toks[j + 1].text.eq_ignore_ascii_case(name) - { - return Some(j); + if is_kw(&toks[j], "end") && toks[j + 1].kind == TokKind::Ident { + if toks[j + 1].text.eq_ignore_ascii_case(name) { + return Some(j); + } } j += 1; } diff --git a/src/rust/main.rs b/src/rust/main.rs index 8064c762..56a4d4f5 100644 --- a/src/rust/main.rs +++ b/src/rust/main.rs @@ -280,8 +280,9 @@ enum CorpusOp { /// Look up entries across every synonym table by `semantic_class`. /// Demonstrates cross-prover semantic equivalence — e.g. - /// `corpus crossquery well-foundedness` reports `WellFounded` in Agda, - /// `well_founded` in Coq, and `WellFounded` in Lean and Idris 2. + /// `corpus crossquery well-foundedness` reports `WellFounded` in Agda + /// + `well_founded` in Coq + `WellFounded` in Lean + `WellFounded` in + /// Idris 2. /// /// The cross-prover dictionaries are searched too, so classes that /// only exist there (`wrapping-arithmetic`, `frame-rule`, @@ -300,7 +301,10 @@ enum CorpusOp { /// Find the K nearest-neighbour entries to a free-form text /// query by cosine similarity over the Vector octad embeddings. - /// Useful for "find lemmas semantically near `WellFounded _<_`". + /// The query is canonicalised the same way the corpus is, so a + /// statement written in one prover's syntax matches entries written + /// in another's. Useful for "find lemmas structurally near + /// `WellFounded _<_`". Near { query: String, #[arg(short, long)] @@ -309,6 +313,32 @@ enum CorpusOp { top: usize, }, + /// Group matching declarations by their *structural* identity key. + /// + /// The key is the SHA-256 of the type's canonical shape — variable + /// names, module paths, operator spellings and binder keywords are + /// normalised away — so `+-comm` in Agda, `Nat.add_comm` in Lean and + /// `eq Nat (add x y) (add y x)` in Dedukti land on one key with no + /// synonym lookup. `--skeleton` additionally prints the binder- and + /// sort-free key, which is what provers that elide binders (Isabelle) + /// match on. + Identity { + /// Name pattern to match: a substring of the qualified or short + /// name, case-insensitive. `*` matches every declaration. + pattern: String, + /// Path to the corpus JSON. Defaults to + /// `data/corpus/.json` for the cwd's basename. + #[arg(short, long)] + index: Option, + /// Also print the skeleton key (binders and sorts erased). + #[arg(long)] + skeleton: bool, + /// Only show keys that group declarations from more than one + /// adapter. + #[arg(long)] + cross_only: bool, + }, + /// Convert a JSON corpus index into 8-modality octad JSONL /// (one DeclarationOctad per line). Streamable; compatible with /// VeriSim's `/api/v1/octads` endpoint when posted line-by-line. @@ -1583,6 +1613,86 @@ fn corpus_command(op: CorpusOp, formatter: &OutputFormatter) -> Result<()> { } }, + CorpusOp::Identity { + pattern, + index, + skeleton, + cross_only, + } => { + let path = match index { + Some(p) => p, + None => { + let basename = std::env::current_dir()? + .file_name() + .map(|s| s.to_string_lossy().into_owned()) + .unwrap_or_else(|| "project".to_string()); + default_index(&basename) + }, + }; + let corpus = Corpus::load_json(&path) + .with_context(|| format!("load corpus index {}", path.display()))?; + let needle = pattern.to_lowercase(); + let everything = needle == "*"; + + // Group by structural key, keeping the key itself for display. + let mut groups: std::collections::BTreeMap< + String, + ( + echidna::corpus::canonical::StructuralKey, + Vec<(String, String)>, + ), + > = std::collections::BTreeMap::new(); + for entry in &corpus.entries { + let matches = everything + || entry.qualified.to_lowercase().contains(&needle) + || entry.name.to_lowercase().contains(&needle); + if !matches { + continue; + } + let key = echidna::corpus::canonical::structural_key(&entry.statement); + let slot = groups + .entry(key.key.clone()) + .or_insert_with(|| (key, Vec::new())); + slot.1 + .push((corpus.adapter.clone(), entry.qualified.clone())); + } + + if groups.is_empty() { + formatter.info(&format!("no declarations matching '{}'", pattern))?; + return Ok(()); + } + + let mut shown = 0usize; + for (key, (structural, members)) in &groups { + let adapters: std::collections::BTreeSet<&str> = + members.iter().map(|(a, _)| a.as_str()).collect(); + if cross_only && adapters.len() < 2 { + continue; + } + shown += 1; + println!( + "{} [{}] {} declaration(s) across {} adapter(s)", + &key[..16.min(key.len())], + structural.tier.as_str(), + members.len(), + adapters.len() + ); + println!(" type: {}", structural.shape); + if skeleton { + println!(" skeleton: {}", structural.skeleton); + } + for (adapter, qualified) in members { + println!(" {} {}", adapter, qualified); + } + } + formatter.info(&format!( + "{} key(s) over {} declaration(s) in {}", + shown, + groups.values().map(|(_, m)| m.len()).sum::(), + path.display() + ))?; + }, + CorpusOp::ExportOctads { index, out } => { let corpus = Corpus::load_json(&index) .with_context(|| format!("load corpus index {}", index.display()))?; diff --git a/src/rust/vcl_ut.rs b/src/rust/vcl_ut.rs index 30d15eff..8618b3f1 100644 --- a/src/rust/vcl_ut.rs +++ b/src/rust/vcl_ut.rs @@ -162,8 +162,13 @@ pub struct QueryResultEntry { /// Axioms used pub axioms: Vec, - /// Cross-prover identity (goal-only hash) + /// Cross-prover identity (name-tail hash; legacy) pub cross_prover_id: String, + + /// Structural cross-prover identity — SHA-256 of the canonical type + /// shape (E6). Present when the producing build wrote it. + #[serde(default)] + pub cross_prover_identity_key: Option, } // ═══════════════════════════════════════════════════════════════════════ @@ -830,6 +835,15 @@ fn search_result_to_entry(value: &serde_json::Value) -> Option .and_then(|v| v.as_str()) .unwrap_or("") .to_string(), + cross_prover_identity_key: value + .get("cross_prover_identity_key") + .or_else(|| { + value + .get("graph") + .and_then(|g| g.get("cross_prover_identity_key")) + }) + .and_then(|v| v.as_str()) + .map(String::from), }) } @@ -866,6 +880,8 @@ fn octad_to_entry(octad: &OctadPayload) -> QueryResultEntry { aspects: octad.document.aspects.clone(), axioms: octad.semantic.axioms_used.clone(), cross_prover_id: octad.graph.cross_prover_id.clone(), + cross_prover_identity_key: Some(octad.graph.cross_prover_identity_key.clone()) + .filter(|k| !k.is_empty()), } } diff --git a/src/rust/verisim_bridge.rs b/src/rust/verisim_bridge.rs index 7bc8ab48..f2382f4c 100644 --- a/src/rust/verisim_bridge.rs +++ b/src/rust/verisim_bridge.rs @@ -228,6 +228,13 @@ pub struct GraphPayload { /// Cross-prover identity (goal-only hash, prover-agnostic) pub cross_prover_id: String, + /// Structural cross-prover identity: SHA-256 of the canonical type + /// shape of the goal (see `corpus::canonical`). This is the E6 + /// `cross_prover_identity_key`; two provers that state the same + /// theorem in different syntax share it. + #[serde(default)] + pub cross_prover_identity_key: String, + /// Prover that produced this proof pub prover_id: String, } @@ -448,6 +455,10 @@ impl ProofOctadBuilder { depends_on: self.parent_proofs, sub_goals: self.sub_goals, cross_prover_id, + cross_prover_identity_key: crate::corpus::canonical::structural_key( + &document.theorem_statement, + ) + .key, prover_id: format!("echidna:prover:{:?}", self.prover), };