EdwardsXYZT.v: drop 4 vestigial imports#2333
Merged
JasonGross merged 1 commit intoMay 17, 2026
Merged
Conversation
Drops: - bedrock2.FE310CSemantics - compiler.MMIO - compiler.Pipeline - compiler.Symbols None of these are actually used in the file. The imports were likely copy-pasted from an upstream LAN9250-style example. Removing them allows the file to be built in environments where the [compiler] package isn't available (e.g., AUCurves' bedrock2-only setup). Verified clean build (rocq-9, fiat-crypto pairing-proofs branch) both with and without these imports — same .vo size, same proof terms.
spitters
added a commit
to AU-COBRA/AUCurves
that referenced
this pull request
May 17, 2026
…plans
This commit bundles two related cleanups so a fresh clone is sane.
* .gitmodules URL bshvass/fiat-crypto -> spitters/fiat-crypto. The previous
pin (2b3e635) lived only on a local 'pairing-proofs' branch on a laptop
and was not fetchable on a fresh recursive clone — every CI run and
every new contributor's clone hit
fatal: No url found for submodule path '.claude/worktrees/agent-...'
because the 2b3e635 commit tracked 8 .claude/worktrees/agent-* dirs as
160000 gitlinks without entries in fiat-crypto's .gitmodules.
* fiat-crypto pointer 2b3e635 -> 7c30b5a56, on spitters/fiat-crypto's
branch pairing-proofs-merge-202605. The new pin carries:
- merge of mit-plv/fiat-crypto upstream/master (catches up the 41
upstream commits since 2026-03-03)
- removal of 8 .claude/worktrees + 5 rocq_mcp_cache_*.v scratch files
(the CI fix)
- deletion of 13 dead Jasmin extract/bridge .v files whose imports
(Crypto.Bedrock.Field.Synthesis.Examples.*_prime etc.) now live
in AUCurves
- deletion of stale src/Spec/XEdDSA.v duplicate (canonical version
is in AUCurves at src/Spec/XEdDSA.v)
- deletion of orphan CurveAddInplace.v (AUCurves has
CurveAddInplaceWrapper.v as the replacement)
- sanitized _CoqProject (dropped hardcoded user-home -Q paths and
dead-file refs)
- EdwardsXYZT.v import cleanup (also upstreamed as
mit-plv/fiat-crypto#2333)
* Drops 15 stale tracked .md files (cumulative ~4400 LoC):
- 3 root-level session plans (BEDROCK2_REFLECTIVE_PLAN.md,
RUSTCMD_ED25519_PLAN.md, AGENTS.md) — point-in-time planning, not
reference docs; replaced by paper-section material under docs/
- 12 dated docs/*.md snapshots (signal-stack-{roadmap,status}-2026-05-13,
trust-audit-2026-05-13{,-refresh}, axiom-closure-plan-2026-05-13,
whole-protocol-jasmin-bench-2026-05-14, rustcmd-rupicola-{roadmap,
final-status}, pipeline-metrics-for-paper, bedrock2-vs-rustcmd,
jasmin-extraction-progress, upstream-pr-draft-extended-scalarmult)
— all either superseded by docs/rustcmd-paper-section.md or
explicit point-in-time captures
See docs/INDEX.md for the resulting topical structure.
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
2 participants
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.
Summary
Drops 4 unused imports from
src/Bedrock/End2End/X25519/EdwardsXYZT.v:bedrock2.FE310CSemanticscompiler.MMIOcompiler.Pipelinecompiler.SymbolsNone of these are referenced in the file. They appear to have been copy-pasted from an upstream LAN9250-style example. Removing them allows the file to be built in environments where the
compilerpackage isn't available (e.g., downstream consumers running on a bedrock2-only setup).Test plan
.vosize, same proof terms.