test(aeneas): coverage guard — real relay primitive (CRC32) - #20
Merged
Conversation
Translates relay's crates/relay-primitives/plain/src/crc32.rs verbatim through the pipeline to discover Aeneas coverage on relay's verification-oriented code. Exercises features beyond the trivial example: a const-eval array, &[u8] slices, indexing, casts, , bit ops, while loops. Translate-only (light) + prints the generated Lean. Adds a relay-coverage CI job. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…32 error Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Aeneas (build-2026.04.22) hits an internal error translating a const-eval'd global array initializer (src/lib.rs:10-28, the CRC32_TABLE const). Charon handles it fine; the functions translate fine. Workaround: compute the table via a runtime fn instead of const. This is the confirmed mitigation for relay's crc32.rs pattern pending an upstream Aeneas fix. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
avrabe
marked this pull request as ready for review
July 22, 2026 05:28
avrabe
changed the title
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Discovery experiment, now a confirmed regression guard: translates relay's real
crates/relay-primitives/plain/src/crc32.rs(IEEE CRC32) through the Aeneas pipeline.Finding
&[u8]slices, indexing, casts, bit ops.build-2026.04.22, LLBC → Lean): hits[Error] Internal error, please file an issuespecifically on a const-eval'd global array initializer (src/lib.rs:10-28, theCRC32_TABLEconst) — a version-specific Aeneas bug, not a fundamental Rust-feature gap. Functions translate fine.fninstead ofconst. Confirmed green on CI:aeneas translated relay CRC32 -> ... (3666 bytes),Build completed successfully.Verdict for relay
Relay's verification-oriented
plaincode is Aeneas-translatable with one known idiom to avoid (const-eval'd global arrays) until upstream fixes the internal error. Worth filing with AeneasVerif.What this adds
A permanent CI job (
relay-coverage) translating real, external Rust — a stronger regression guard than the synthetichelloexample, and documentation of the const-array limitation + workaround for anyone adapting more relay code.🤖 Generated with Claude Code