[hyperpolymath]

What this does

Two things: it lands the fixes that were still sitting on the branch after #448
merged, and it replaces the corpus's name-based cross-prover identity with a
structural one.

1. Corpus identity is now the shape of the type, not the name

E6 GraphModality.cross_prover_identity_key used to be the SHA-256 of a
declaration's name tail, so +-comm (Agda), Nat.add_comm (Coq/Lean),
addComm (Idris 2) and bvadd_comm (SMT-LIB) shared nothing. The new
src/rust/corpus/canonical.rs normalises the statement into a nameless prefix
term — variables renamed v0, v1, …, module paths dropped, operator
spellings and binder keywords canonicalised, sorts mapped to
NAT/INT/TYPE, Isabelle ascriptions unwrapped, Dedukti's explicit sort
argument dropped — and hashes it (scheme dk-shape-v1). No dictionary is
consulted on the identity path.

Because some provers cannot state the same shape (Isabelle writes
lemma add_comm: "(x::nat) + y = y + x" with no binders; Why3 uses int
where the others use nat), a second tier is emitted:

field	meaning
cross_prover_identity_key	SHA-256 of the canonical shape, binders and sorts included
cross_prover_skeleton_key	same shape with the binder prefix and sort atoms erased — the tier-2 join
identity_scheme	which rules produced the keys (dk-shape-v1)
canonical_type	the rendered shape, for debugging
cross_prover_id	the old name-tail hash, still emitted for existing octads/clients

Validated against the fixtures before porting: Agda, Coq, Lean 4, Idris 2,
SMT-LIB and Dedukti agree on (PI [NAT NAT] (EQ (ADD v0 v1) (ADD v1 v0))) for
add_comm; Isabelle and Why3 join on (EQ (ADD v0 v1) (ADD v1 v0)); add_zero
agrees across four provers; associativity and commutativity stay distinct.
The unit tests pin all of it. Equational rewriting is deliberately not
applied — x + y and y + x are different keys.

2. The Vector octad is 256-dim and structural

StructuralEmbedder hashes 1–3-grams of the canonical atom stream into 256
buckets (model echidna-corpus-structural-v2), replacing the 32-dim raw-text
HashEmbedder as the default. corpus near canonicalises the query too, so a
query written in SMT-LIB syntax retrieves entries written in Coq syntax
(tested). HashEmbedder stays as Corpus::compute_embeddings_legacy for GNN
FEATURE_DIM parity and for replaying older octads; the capnp embedder /
embedder_dim fields carry both and consumers are told to check them.

New CLI: echidna corpus identity <pattern> [--skeleton] [--cross-only].

3. Carried fixes from earlier in the branch

• estate_layers.rs::adapter_of_layer only names layers that actually have an
  adapter (creusot-core is not spark_ada).
• The SPARK adapter test asserts SPARK_Mode rather than the bare SPARK the
  parser emits; the profile/creusot adapter tests no longer depend on the
  checkout layout.
• cargo fmt applied (bot commit — this branch is prepared without a local
  Rust toolchain, so formatting is done in CI).

4. Honesty pass over docs, ADR, wiki

docs/CORPUS.adoc, docs/architecture/VERISIM-ER-SCHEMA.adoc,
docs/handover/STATE.adoc, CLAUDE.md, CHANGELOG.adoc, the 2026-04-28 ADR
(annotated as superseded in part) and the wiki source pages
(docs/wikis/{Home,Architecture}.md) now describe what the code actually
does — 20 adapters, 256-dim structural embeddings, two-tier identity. New ADR:
docs/decisions/2026-10-22-structural-cross-prover-identity.adoc.

Notes for the reviewer

• DeclGraph, GraphPayload and QueryResultEntry gained fields; all are
  #[serde(default)], so existing octad JSONL still loads.
• The 32-dim embedder is not deleted: dropping it would break GNN parity and
  old octads.
• .github/workflows/zz-fmt.yml is temporary scaffolding for this branch
  (no local toolchain) and is removed in a follow-up commit; it has no uses:
  steps because newly added workflows in this repo fail at startup when they
  reference an action.
• Python: none added — the canonicaliser prototype lived outside the tree and
  the Rust module is the artefact of record.

[chatgpt-codex-connector]

Codex Review Summary

This comment shows the latest Codex review activity on this pull request.

Review	Status	Commit	Review trigger
📝 Code Review	✅ Completed 2026-10-22T17:48:06.580182Z	c6a239b	PR opened

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review" or "@codex security review".

Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings.

[coderabbitai]

Note

Currently processing new changes in this PR. This may take a few minutes, please wait...

⚙️ Run configuration

• Source mode: Auto
• Repository: Unavailable
• Branch: Unavailable
• File: No configuration file from this repository applied
• Commit: Unavailable
• Layers: Organization UI
• Review profile: ASSERTIVE
• Plan: Advanced
• Run ID: cd757cfd-48b4-4cf2-a55e-9aa8d1785a8c

📥 Commits

Reviewing files that changed from the base of the PR and between 852a374 and dc8b433.

📒 Files selected for processing: 55

• .machine_readable/descriptiles/ECOSYSTEM.a2ml
• .machine_readable/descriptiles/META.a2ml
• .machine_readable/descriptiles/STATE.a2ml
• CHANGELOG.adoc
• CLAUDE.md
• EXPLAINME.adoc
• Justfile
• README.adoc
• crates/echidna-core-creusot/src/estate_layers.rs
• crates/echidna-core-creusot/src/lib.rs
• crates/echidna-wire/schemas/verisim_er.capnp
• data/corpus-profiles/hyperpolymath-estate.toml
• data/synonyms/README.adoc
• data/synonyms/_disciplines.toml
• data/synonyms/_msc2020.toml
• data/synonyms/_verification_systems.toml
• data/synonyms/idris2.toml
• docs/CORPUS-ADAPTERS.adoc
• docs/CORPUS.adoc
• docs/architecture/CHAPEL-SATURATION-HOOKS.adoc
• docs/architecture/JULIA-SATURATION-HOOKS.adoc
• docs/architecture/TYPE-DISCIPLINE-EMBEDDING.adoc
• docs/architecture/VERISIM-ER-SCHEMA.adoc
• docs/decisions/2026-04-28-corpus-and-design-search.adoc
• docs/decisions/2026-10-22-structural-cross-prover-identity.adoc
• docs/handover/STATE.adoc
• docs/reports/2026-10-22-vocabulary-recon.adoc
• docs/wikis/Architecture.md
• docs/wikis/FAQ.md
• docs/wikis/Getting-Started.md
• docs/wikis/Guides.md
• docs/wikis/Home.md
• docs/wikis/Troubleshooting.md
• src/julia/README.adoc
• src/julia/corpus_loader.jl
• src/julia/run_training.jl
• src/julia/saturation_synonyms.jl
• src/rust/corpus/canonical.rs
• src/rust/corpus/creusot.rs
• src/rust/corpus/embed.rs
• src/rust/corpus/mod.rs
• src/rust/corpus/octad.rs
• src/rust/corpus/profile.rs
• src/rust/corpus/query.rs
• src/rust/corpus/spark_ada.rs
• src/rust/main.rs
• src/rust/suggest/synonyms.rs
• src/rust/vcl_ut.rs
• src/rust/verisim_bridge.rs
• tests/corpus_cli_dispatch.rs
• tests/corpus_estate_adapters.rs
• tests/corpus_fixtures/creusot/smoke.rs
• tests/corpus_fixtures/spark_ada/smoke.adb
• tests/corpus_fixtures/spark_ada/smoke.ads
• tests/lexicon_v2_test.rs

✨ Finishing Touches

📝 Generate docstrings

- 🤖 [Coding Agent task started](https://app.coderabbit.ai/code/tasks/c22f808c-abd9-51cd-b181-ec3d7fd4865c?source=coding_agent_github_finishing_touch) for docstring generation. - [ ] Create a new PR

• Autofix · Keep fixing CodeRabbit findings and required CI, and resolving merge conflicts

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

• X
• Mastodon
• Reddit
• LinkedIn

_{Comment @coderabbitai help to get the list of available commands.}

[coderabbitai]

Add Carrot credits or activate Agent usage billing to use Autofix

[coderabbitai]

⚠️ Coding task changes are ready, but delivery needs attention

Open the task to resolve the delivery issue or retry.

[chatgpt-codex-connector]

💡 Codex Review

echidna/src/rust/corpus/profile.rs

Line 122 in c6a239b

paths: vec!["src".to_string(), String::new()],

Avoid scanning each Agda src tree twice

Each Agda rule includes both src and the repository root, but the Agda adapter recursively walks its base, so when src exists every file below it is ingested once from repo/src and again from repo. The two sub-corpora are then merged without declaration deduplication, producing duplicate modules and entries (and overwriting one copy in by_qualified), which doubles corpus/training counts for the five primary estate repositories. Select the existing directory layout rather than ingesting both overlapping roots.

---

echidna/src/rust/corpus/canonical.rs

Lines 1051 to 1054 in c6a239b

	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,

Preserve short free constants in identity keys

For statements containing unrecognized short lowercase constants, this heuristic renames the constants as variables even though they are not binders. For example, forall x, f x and forall x, g x both canonicalize to the same shape and therefore receive the same cross-prover identity key. Since these keys are used to assert theorem identity, common one-to-three-character predicates and functions can incorrectly join unrelated declarations; alpha-renaming should be limited to actual binders or otherwise distinguish term heads from variables.

---

echidna/src/rust/corpus/creusot.rs

Lines 734 to 738 in c6a239b

	if statement.contains("#[requires") {
	push_once(&mut hz.other, "creusot:requires");
	}
	if statement.contains("#[ensures") {
	push_once(&mut hz.other, "creusot:ensures");

Keep specification tags out of the hazard bucket

Ordinary Creusot contracts now add creusot:requires and creusot:ensures to AxiomUsage::other, but AxiomUsage::any() treats every nonempty other list as an axiom hazard. Consequently a normal proved function with a requires/ensures contract is counted as hazardous and is excluded by where_axiom_free(), even without #[trusted] or unsafe constructs. These descriptive specification tags need separate metadata or must be excluded from hazard evaluation.

---

echidna/src/rust/corpus/creusot.rs

Lines 599 to 601 in c6a239b

	if p.kind == TokKind::Str && p.text == "\"C\"" {
	i -= 1;
	continue;

Recognize cleaned extern ABI string tokens

For any extern "C" fn, clean_source blanks the string payload before tokenization, so the preceding Str token is " ", never "C". This condition therefore fails, modifier_start stops at fn, and the captured statement omits extern "C"; as a result creusot:ffi_edge is not recorded, and attributes before extern (including #[trusted] and contracts) are also detached from the function. Match the string-token shape independently of its blanked payload or preserve the ABI spelling for this scan.

---

echidna/src/rust/main.rs

Lines 1656 to 1657 in c6a239b

	slot.1
	.push((corpus.adapter.clone(), entry.qualified.clone()));

Retain sub-adapter identity in estate identity groups

When the index is produced by hyperpolymath_estate, every member is labeled with the aggregate corpus.adapter value rather than the Agda/Idris2 adapter that created its module. Thus the adapter set always has size one and corpus identity --cross-only suppresses every group, even when a structural key is shared across the profile's different source adapters; exported profile octads likewise lose this provenance. Store and use the originating sub-adapter when merging profile entries.

---

echidna/src/rust/corpus/query.rs

Lines 230 to 239 in c6a239b

	// 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 = <super::embed::StructuralEmbedder as super::embed::Embedder>::embed(
	&embedder, hit.entry,
	);
	hit.similarity = Some(cosine(qv, &v));

Keep GNN vectors comparable in near_vector

near_vector is still documented as accepting a precomputed GNN embedding, but the repository's GNN feature dimension is 32 while this execution path now embeds every corpus entry with the 256-dimensional structural embedder. cosine returns 0.0 for every dimension mismatch, so a normal GNN query produces corpus-order results with no meaningful ranking. Select the compatible legacy/GNN embedding space from the query dimension or reject incompatible vectors instead of silently returning all-zero similarities.

---

echidna/src/rust/main.rs

Lines 1652 to 1655 in c6a239b

	let key = echidna::corpus::canonical::structural_key(&entry.statement);
	let slot = groups
	.entry(key.key.clone())
	.or_insert_with(|| (key, Vec::new()));

Group fallback identity matches by skeleton key

Groups are always keyed by the primary structural key, so declarations that are only supposed to match through the advertised skeleton fallback—such as Isabelle with elided binders or Why3 with a different numeric sort—remain in separate groups. The --skeleton option only prints each already-separated group's skeleton and cannot reveal the cross-prover match; with --cross-only, those declarations may be hidden entirely. Implement the documented second-tier grouping or lookup using skeleton_key when primary keys do not join.

---

echidna/src/rust/corpus/profile.rs

Lines 316 to 318 in c6a239b

	for mut module in sub.modules {
	module.name = format!("{}::{}", repo, module.name);
	module.options.push(format!("repo:{}", repo));

Preserve profile-relative source paths

A sub-corpus module path is relative to the adapter base, but merging only prefixes the module name and leaves that path unchanged. For example, an ABI ingested from alpha/src/abi is stored as Layout.idr even though the combined corpus root is the estate directory and the actual path is alpha/src/abi/Layout.idr. Exported spatial/provenance paths therefore cannot be resolved against Corpus.root and collide across repositories; prefix each path with its repository and configured base path during the merge.

---

echidna/src/rust/corpus/creusot.rs

Lines 104 to 108 in c6a239b

	for d in parsed.decls {
	let entry_idx = corpus.entries.len();
	let qualified = format!("{}.{}", corpus.modules[module_idx].name, d.name);
	all_names.insert(d.name.clone());
	all_names.insert(qualified.clone());

Qualify Rust methods by their owning type

The Creusot parser indexes functions inside traits and impl blocks, but every entry is qualified only as <file-module>.<method-name>. Rust routinely has multiple implementations in one file with the same method name (for example, several new, fmt, or trait methods), so those entries receive identical qualified names and Corpus::reindex_links overwrites all but one in by_qualified. Track the enclosing trait/impl type in the qualified name so every legal Rust declaration remains addressable.

---

echidna/crates/echidna-core-creusot/src/estate_layers.rs

Lines 150 to 152 in c6a239b

	"ex" | "exs" => Some(Layer::Beam),
	"agda" | "thy" | "v" | "lean" | "dfy" | "fst" => Some(Layer::Types),
	_ => None,

Make extension and adapter layer mappings agree

layer_of_adapter assigns Dafny, F* and Why3 to Layer::Spark, while this extension mapping assigns .dfy and .fst files to Layer::Types and does not recognize Why3 extensions at all. This directly violates the module's stated PO-L5 agreement property, but the corresponding test omits those adapters. Any extension-based policy check can therefore disagree with the adapter-based result for the same source file; map each owned extension to its adapter's layer and test every supported adapter.

---

echidna/data/synonyms/_verification_systems.toml

Lines 1042 to 1044 in c6a239b

	canonical = "atomic_access"
	aliases = ["atomic", "atomicLoad", "atomicStore", "acquire", "release"]
	tactic_class = "memory"

Mark ambiguous dictionary spellings as non-synonyms

The new dictionary declares release as an interchangeable alias of both deallocation (line 910) and atomic_access here. After merge_cross_prover_dicts, SynonymTable::alternatives("release") therefore offers memory deallocation and atomic ordering as substitutions for one another, which can generate semantically invalid tactic variants. Ambiguous terms such as this (and similarly reused frame and sp) need scoped spellings or non-interchangeable/false-friend relations rather than duplicate default synonym rows.

---

echidna/src/rust/corpus/spark_ada.rs

Lines 412 to 416 in c6a239b

	if at < toks.len() && is_kw(&toks[at], "is") && parsed.unit.is_none() {
	parsed.unit = Some(name);
	if has_pragma(&toks, "spark_mode") {
	parsed.options.push("SPARK_Mode".to_string());
	}

Propagate package-level SPARK_Mode Off

For the standard package-level form package P with SPARK_Mode => Off is, this code records only the generic SPARK_Mode option. The package aspect is outside every declaration's statement, and apply_out_of_decl_hazards does not process it, so flag_spark_aspects never adds spark:spark_mode_off; all declarations in an explicitly unproved unit can therefore appear as SPARK-verified and hazard-free. Detect the Off value at package/pragma scope and propagate it to every declaration in that unit.

---

echidna/src/rust/corpus/canonical.rs

Lines 235 to 239 in c6a239b

	| "data"
	| "record"
	| "function"
	| "procedure"
	| "declare-fun"

Strip Rust fn headers before deriving identity keys

The declaration-header recognizer includes the word function but not Rust's fn, and it also does not skip leading Rust visibility/modifier tokens such as pub. Consequently statements emitted by the new Creusot adapter retain fn, the declared function name, and often pub in their canonical shape, so renaming a Rust function changes its identity key and an otherwise equivalent Rust/Creusot declaration cannot join a theorem from another prover. Normalize Rust attributes/modifiers and recognize fn before hashing.

---

echidna/src/rust/corpus/octad.rs

Lines 260 to 263 in c6a239b

	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(),

Serialize the structural-key confidence tier

structural_key can return KeyTier::Text when a statement does not parse, but the octad stores its hash in cross_prover_identity_key exactly like a structural key and discards identity.tier. Downstream consumers therefore cannot tell a canonical type-shape identity from the weaker normalized-text fallback and will apply the documented tier-1 join to both. Carry the tier in DeclGraph and the wire schema, or leave the structural field empty for non-structural fallbacks.

---

echidna/src/rust/corpus/creusot.rs

Lines 764 to 771 in c6a239b

	if text.contains("transmute") {
	push_once(&mut hz.other, "creusot:transmute");
	}
	if text.contains("unimplemented!") || text.contains("todo!") {
	push_once(&mut hz.other, "creusot:unimplemented");
	}
	if text.contains("unsafe") {
	push_once(&mut hz.other, "creusot:unsafe_surface");

Exclude comments and identifiers from unsafe hazard scans

Hazards are searched in the original statement/body using unrestricted substring checks, even though the parser already has a comment- and string-cleaned source. A safe function containing a comment such as // no unsafe or transmute here, a string with that text, or an identifier such as unsafe_count is tagged as using an unsafe surface or transmutation. Since these tags feed hazard filtering and corpus statistics, scan cleaned tokens or matched Rust syntax rather than raw substrings.

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".