[Leios] LLF1-2: single-vote BLS verification and voting-crypto prose (#1298)

formal-ledger-test/src/Test/LedgerImplementation.lagda.md

@@ -65,6 +65,8 @@ module Implementation where
   BlsPoP  = ℕ
   isValidPoP : BlsVKey → BlsPoP → Type
   isValidPoP = _≡_
+  isSignedBy : BlsVKey → Ser → BlsSig → Type
+  isSignedBy = λ vk m σ → vk + m ≡ σ
   isSignedByAggregate : List BlsVKey → Ser → BlsSig → Type
   isSignedByAggregate = λ vks m σ → foldr _+_ 0 vks + m ≡ σ
 

src/Ledger/Core/Foreign/Crypto/Structure.agda

@@ -41,6 +41,7 @@ HSCryptoStructure = record {
   ; BlsSig = ℕ
   ; BlsPoP = ℕ
   ; isValidPoP = λ vk pop → extIsSigned vk vk pop ≡ true
+  ; isSignedBy = λ vk m σ → extIsSigned vk m σ ≡ true
   ; isSignedByAggregate = λ vks m σ → extIsSigned (sum vks) m σ ≡ true
   }
 

src/Ledger/Dijkstra/Specification/Crypto.lagda.md

@@ -19,40 +19,69 @@ open import Ledger.Core.Specification.Crypto hiding (CryptoStructure)
 
 ## Leios Voting Crypto
 
-In Leios the committee consists of a certain number of pools with the largest
-stake, with ties broken by pool id.  Therefore the `KeyHash`{AgdaDatatype} type
-carries a strict total order, the implementation's byte-wise comparison.
-(See the [Epoch Boundary section] of [CIP-0164].)
+Leios ([CIP-164]) adds a second signature scheme beside the payment scheme
+above: an epoch's voting committee signs endorser-block announcements with
+registered voting keys, and a certificate compresses a quorum of votes into
+one aggregate signature.  The scheme enters the specification abstractly and
+verification-only, like `isSigned`{.AgdaField} above; the implementation
+instantiates it with BLS12-381 MinSig, 96-byte verification keys with 48-byte
+signatures and proofs of possession.  It lives here, beside the payment
+scheme, so other protocol extensions that aggregate votes (Peras) can share
+it.
 
 ```agda
 record CryptoStructure : Type₁ where
-  field pkk : PKKScheme
+  field
+    pkk : PKKScheme
 
   open PKKScheme pkk public
 
-  field ⦃ khs ⦄    : isHashableSet VKey
-        ScriptHash : Type; ⦃ DecEq-ScriptHash ⦄ : DecEq ScriptHash ; ⦃ Show-ScriptHash ⦄ : Show ScriptHash
+  field
+    ScriptHash             : Type
+    VRF                    : Type
+    BlsVKey BlsSig BlsPoP  : Type
+    isValidPoP             : BlsVKey → BlsPoP → Type
+    isSignedBy             : BlsVKey → Ser → BlsSig → Type
+    isSignedByAggregate    : List BlsVKey → Ser → BlsSig → Type
+```
+
+`isValidPoP`{.AgdaField} checks a key's *proof of possession*, required with
+every registration because aggregation is otherwise open to rogue-key attacks
+(a key crafted relative to others' keys, making an aggregate appear to include
+voters who never signed).  `isSignedBy`{.AgdaField} verifies a single vote,
+the meaning by which consensus filters votes before aggregation;
+`isSignedByAggregate`{.AgdaField} verifies a certificate's aggregate signature
+against its signers' keys.  Only verification enters the rules: the ledger
+never creates votes or certificates, so the scheme has no signing side and no
+correctness law relating one.
+
+<!--
+```agda
+  field ⦃ khs ⦄                      : isHashableSet VKey
+        ⦃ DecEq-ScriptHash ⦄         : DecEq ScriptHash
+        ⦃ Show-ScriptHash ⦄          : Show ScriptHash
+        ⦃ DecEq-VRF ⦄                : DecEq VRF
+        ⦃ DecEq-BlsVKey ⦄            : DecEq BlsVKey
+        ⦃ DecEq-BlsSig ⦄             : DecEq BlsSig
+        ⦃ DecEq-BlsPoP ⦄             : DecEq BlsPoP
+        ⦃ Dec-isValidPoP ⦄           : isValidPoP ⁇²
+        ⦃ Dec-isSignedByAggregate ⦄  : isSignedByAggregate ⁇³
 
   open isHashableSet khs renaming (THash to KeyHash) hiding (DecEq-T) public
+```
+-->
 
-  field VRF : Type
-        ⦃ DecEq-VRF ⦄ : DecEq VRF
+In Leios the committee consists of a certain number of pools with the largest
+stake, with ties broken by pool id.  Therefore the `KeyHash`{AgdaDatatype} type
+carries a strict total order, `_<ᵏʰ_`{.AgdaField}, analogous to the
+implementation's byte-wise comparison.
+(See the [Epoch Boundary section] of [CIP-0164].)
 
+```agda
   -- Byte-wise ascending order on key hashes; the Leios committee tie-break.
   field _<ᵏʰ_ : KeyHash → KeyHash → Type
         <ᵏʰ-isSTO : IsStrictTotalOrder _≡_ _<ᵏʰ_
-        ⦃ Dec-<ᵏʰ ⦄ : _<ᵏʰ_ ⁇²
-
-  -- BLS12-381 signature scheme used for Leios voting (CIP-0164).
-  field BlsVKey BlsSig BlsPoP : Type
-        isValidPoP          : BlsVKey → BlsPoP → Type
-        isSignedByAggregate : List BlsVKey → Ser → BlsSig → Type
-        ⦃ DecEq-BlsVKey ⦄ : DecEq BlsVKey
-        ⦃ DecEq-BlsSig  ⦄ : DecEq BlsSig
-        ⦃ DecEq-BlsPoP  ⦄ : DecEq BlsPoP
-        ⦃ Dec-isValidPoP ⦄ : isValidPoP ⁇²
-        ⦃ Dec-isSignedByAggregate ⦄ : isSignedByAggregate ⁇³
-
+        ⦃ Dec-<ᵏʰ ⦄                  : _<ᵏʰ_ ⁇²
 ```
 
 [CIP-164]: https://github.com/cardano-foundation/CIPs/blob/master/CIP-0164/README.md