[Leios] LLF1-2: single-vote BLS verification and voting-crypto prose (#1298) - #1305
Open
williamdemeo wants to merge 2 commits into
Open
[Leios] LLF1-2: single-vote BLS verification and voting-crypto prose (#1298)#1305williamdemeo wants to merge 2 commits into
williamdemeo wants to merge 2 commits into
Conversation
Open
4 tasks
Contributor
There was a problem hiding this comment.
🟡 Changes recommended
The documented proof-of-possession size conflicts with the linked CIP’s CDDL schema.
Once you've addressed the issues Copilot identified, you can request another Copilot review.
Pull request overview
Adds singleton BLS vote verification to the shared crypto abstraction and documents Leios voting cryptography.
Changes:
- Adds decidable
isSignedBy. - Implements foreign and test predicates.
- Exposes voting-crypto documentation.
File summaries
| File | Description |
|---|---|
src/Ledger/Core/Specification/Crypto.lagda.md |
Extends and documents the crypto interface. |
src/Ledger/Core/Foreign/Crypto/Structure.agda |
Implements foreign singleton verification. |
formal-ledger-test/src/Test/LedgerImplementation.lagda.md |
Supplies the test implementation. |
Review details
- Files reviewed: 3/3 changed files
- Comments generated: 1
- Review effort level: Balanced
💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.
Comment on lines
+93
to
+94
| instantiates it with BLS12-381 MinSig, 96-byte verification keys with 48-byte | ||
| signatures and proofs of possession. It lives here, beside the payment |
williamdemeo
force-pushed
the
1298-llf1-2-leios-bls-verification
branch
from
September 10, 2026 05:47
3a80fc2 to
4509457
Compare
isSignedBy verifies one vote under one key: validateVote in the proposed consensus↔ledger interface needs the ledger-side meaning, and aggregate verification does not subsume the singleton case, since the spec fixes no relation between the two. The Foreign instance and the test implementation mirror the field. The voting-crypto block also moves out of the hidden region: the rendered page now carries the fields, with prose for the MinSig instantiation, the rogue-key rationale for proofs of possession, the verification-only discipline, and the committee tie-break order; the Peras-sharing intent of the core placement is recorded where it applies. Decidability instances stay hidden, as elsewhere in the module. AI-assisted development: Claude Fable 5 (Anthropic)
williamdemeo
force-pushed
the
1298-llf1-2-leios-bls-verification
branch
from
September 10, 2026 06:13
4509457 to
eb83dbc
Compare
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
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.
Ports the surviving scope of the fork trial's abstract voting-crypto interface onto the core placement of #1304, per the re-scoped issue.
isSignedBy : BlsVKey → Ser → BlsSig → Typejoins the crypto structure with a decidability instance:validateVotein the proposed consensus↔ledger interface needs the ledger-side meaning of one properly signed vote, and aggregate verification does not subsume the singleton case, since the specification fixes no relation between the two abstract predicates. TheForeigninstance and the test implementation mirror the field.The voting-crypto block also leaves the hidden literate region: the rendered page now shows the fields, with prose for the BLS12-381 MinSig instantiation (96-byte verification keys, 48-byte signatures and proofs of possession), the rogue-key rationale for mandatory proofs of possession, the verification-only discipline (the ledger never creates votes or certificates), and the committee tie-break order on key hashes. Decidability instances stay hidden, as elsewhere in the module.
Stacked on #1304 (base
leios-bls-primitives); re-targetsleios-mainwhen #1304 merges. The fork module this replaces is closed with pointers (williamdemeo#16); the remaining carriers (EBHash,TxRefHash,hashEBRefs) land with [LLF1-3] (#1301).Both the
Ledger.DijkstraandLedgerimport closures type-check locally at this head.Closes #1298.
🤖 AI-assisted development: Claude Fable 5 (Anthropic)