Repository navigation

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

Merged

hyperpolymath merged 28 commits into

mainfrom

arena/5b8efe75-echidna

Oct 22, 2026

Merged

corpus: structural cross-prover identity keys + 256-dim structural embedder#449
hyperpolymath merged 28 commits into
mainfrom
arena/5b8efe75-echidna

Commits on Oct 22, 2026
- vocab: add _verification_systems dictionary and expand MSC2020
  
  hyperpolymath
  and
  arena-agent
  committed
  b8e06df
- vocab: wire crossquery consumer, Julia preload, verify MSC rows, expand idris2
  
  hyperpolymath
  and
  arena-agent
  committed
  8265b05
- corpus: add Ada/SPARK, Rust/Creusot and the estate profile adapters
  
  hyperpolymath
  and
  arena-agent
  committed
  d33fccb
- creusot-core: adapter_of_layer only names layers that have an adapter
  
  hyperpolymath
  and
  arena-agent
  committed
  8b42389
- ci: temporary diagnostic workflow (posts compiler output as a PR comment)
  
  hyperpolymath
  and
  arena-agent
  committed
  e29d860
- ci: trigger the diagnostic workflow on push to this branch
  
  hyperpolymath
  and
  arena-agent
  committed
  b23b24b
- ci: probe minimal workflow
  
  hyperpolymath
  and
  arena-agent
  committed
  369697b
- ci: bisect the diagnostic workflow
  
  hyperpolymath
  and
  arena-agent
  committed
  4db5142
- ci: bisect actions
  
  hyperpolymath
  and
  arena-agent
  committed
  07aebc7
- ci: diagnostic workflow that avoids action refs
  
  hyperpolymath
  and
  arena-agent
  committed
  66f36f3
- ci: publish diagnostics to a paste and record the comment status
  
  hyperpolymath
  and
  arena-agent
  committed
  c99472a
- ci: publish the diagnostics in chunks over a pollable topic
  
  hyperpolymath
  and
  arena-agent
  committed
  c51fa6c
- ci: capture a rustfmt patch and the test results; fix the SPARK_Mode assertion
  
  hyperpolymath
  and
  arena-agent
  committed
  37529c2
- ci: report the rustfmt patch and targeted test runs through a PR comment
  
  hyperpolymath
  and
  arena-agent
  committed
  311b40b
- test: make the profile and creusot adapter tests independent of the checkout
  
  hyperpolymath
  and
  arena-agent
  committed
  7a56cc4
- Update src/rust/corpus/creusot.rs
  
  hyperpolymath
  and
  coderabbitai[bot]
  authored
  6873646
- Update src/rust/corpus/spark_ada.rs
  
  hyperpolymath
  and
  coderabbitai[bot]
  authored
  a3f6b06
- Update tests/corpus_estate_adapters.rs
  
  hyperpolymath
  and
  coderabbitai[bot]
  authored
  c97aeca
- Update tests/corpus_fixtures/spark_ada/smoke.ads
  
  hyperpolymath
  and
  coderabbitai[bot]
  authored
  339290a
- ci: temporary workflow that commits cargo fmt output onto this branch
  
  hyperpolymath
  and
  arena-agent
  committed
  4c448ec
- style: cargo fmt
  fmt-bot
  committed
  e2074b3
- docs(corpus): Clarify ingestion, synonym loading, and training loader behavior and errors
  coderabbitai[bot]
  committed
  d9b0a83
- ci: drop the temporary diagnostics workflows
  
  hyperpolymath
  and
  arena-agent
  committed
  e0c29ec
- corpus: structural cross-prover identity keys and a 256-dim structural embedder
  
  hyperpolymath
  and
  arena-agent
  committed
  3f965dd
- style: cargo fmt (bot)
  echidna-fmt-bot
  committed
  32dcdb7
- ci: run the gates on the formatted tree
  
  hyperpolymath
  and
  arena-agent
  committed
  c6a239b
- ci: drop the temporary formatting workflow
  
  hyperpolymath
  and
  arena-agent
  committed
  dc8b433
- Merge branch 'main' into arena/5b8efe75-echidna
  hyperpolymath
  authored
  b05ec6f

Commits

Commits on Oct 22, 2026