CDDL

docs/cddl/diffs/common/endorser-blocks.md

@@ -0,0 +1,83 @@
+# Endorser Blocks - Leios CDDL
+
+Endorser Blocks (EBs) are new block types in Leios that aggregate multiple Input Blocks from the current pipeline.
+
+## Endorser Block Sortition
+
+**Single EB Limit**: Each producer can generate **at most one Endorser Block per pipeline**, following the crypto-benchmarks implementation approach rather than the full Poisson sortition used in simulations.
+
+**VRF Lottery**: Eligibility uses the simplified probability model:
+
+$$P = 1 - e^{-f_{EB} \cdot \sigma}$$
+
+Where $f_{EB}$ is the per-pipeline EB generation rate and $\sigma$ is the producer's stake fraction.
+
+<sub>[1] [Crypto-benchmarks Sortition](https://github.com/input-output-hk/ouroboros-leios/blob/main/crypto-benchmarks.rs/Specification.md#L63-L65), [2] [Rust Simulation EB Generation](https://github.com/input-output-hk/ouroboros-leios/blob/main/sim-rs/sim-core/src/sim/node.rs#L606-L641)</sub>
+
+## Block Structure
+
+```cddl
+endorser_block =
+  [ eb_header         : eb_header
+  , ib_references     : [* ib_reference]                            ; References to input blocks
+  ]
+```
+
+## Header Structure
+
+```cddl
+eb_header =
+  [ eb_header_body       : eb_header_body
+  , body_signature       : kes_signature
+  ]
+
+eb_header_body =
+  [ slot                 : slot_no                                  ; Slot when EB was created
+  , producer             : node_id                                  ; Block producer identifier
+  , input_blocks         : [* ib_reference]                         ; References to input blocks
+  , ? endorser_blocks    : [* eb_reference]                         ; References to earlier endorser blocks (Full Leios)
+  , ? vrf_proof          : vrf_cert                                 ; VRF proof of eligibility to produce EB
+  ]
+```
+<sub>[1] [Haskell Simulation EndorserBlock](https://github.com/input-output-hk/ouroboros-leios/blob/main/simulation/src/LeiosProtocol/Common.hs#L160-L171), [2] [Rust Simulation EndorserBlock](https://github.com/input-output-hk/ouroboros-leios/blob/main/sim-rs/sim-core/src/model.rs#L167-L176), [3] [Formal Spec EndorserBlockOSig](https://github.com/input-output-hk/ouroboros-leios-formal-spec/blob/main/formal-spec/Leios/Blocks.agda#L97-L106)</sub>
+
+## Input Block Reference Structure
+
+```cddl
+; References to input blocks within endorser blocks
+ib_reference = [
+  ib_id               : ib_id,                                      ; Hash identifier of the input block
+  slot                : slot_no,                                    ; Slot when IB was created
+  producer            : node_id                                     ; IB producer identifier
+]
+
+; Supporting types
+ib_id                 = hash32                                      ; Input block identifier
+```
+<sub>[1] [Haskell Simulation - InputBlockId](https://github.com/input-output-hk/ouroboros-leios/blob/main/simulation/src/LeiosProtocol/Common.hs#L100-L105), [2] [Rust Simulation - InputBlockId](https://github.com/input-output-hk/ouroboros-leios/blob/main/sim-rs/sim-core/src/model.rs#L98-L105), [3] [Formal Spec - IBRef](https://github.com/input-output-hk/ouroboros-leios-formal-spec/blob/main/formal-spec/Leios/Blocks.agda#L33), [4] [Formal Spec - ibRefs](https://github.com/input-output-hk/ouroboros-leios-formal-spec/blob/main/formal-spec/Leios/Blocks.agda#L101)</sub>
+
+## Endorser Block Reference Structure
+
+```cddl
+; References to earlier endorser blocks (for Full Leios)
+eb_reference = [
+  eb_id               : eb_id,                                      ; Hash identifier of the endorser block  
+  slot                : slot_no,                                    ; Slot when EB was created
+  producer            : node_id                                     ; EB producer identifier
+]
+
+; Supporting types
+eb_id                 = hash32                                      ; Endorser block identifier
+```
+<sub>[1] [Haskell Simulation](https://github.com/input-output-hk/ouroboros-leios/blob/main/simulation/src/LeiosProtocol/Common.hs#L161-L163), [2] [Rust Simulation](https://github.com/input-output-hk/ouroboros-leios/blob/main/sim-rs/sim-core/src/model.rs#L148-L152), [3] [Formal Spec](https://github.com/input-output-hk/ouroboros-leios-formal-spec/blob/main/formal-spec/Leios/Blocks.agda#L34)</sub>
+
+## Supporting Types
+
+```cddl
+node_id               = uint32                                      ; Node identifier (simulation)
+slot_no               = uint64                                      ; Slot number
+hash32                = bytes .size 32                              ; 32-byte hash
+```
+
+## Next
+**→ [Input Block - CDDL](input-blocks.md)**

docs/cddl/diffs/common/input-blocks.md

@@ -0,0 +1,58 @@
+# Input Blocks - Leios CDDL
+
+**Single IB Limit**: Each producer can generate **at most one Input Block per slot**, following the crypto-benchmarks implementation approach rather than the full Poisson sortition used in simulations.
+
+**VRF Lottery**: Eligibility uses the simplified probability model:
+
+$$P = 1 - e^{-f_{IB} \cdot \sigma}$$
+
+Where $f_{IB}$ is the per-slot IB generation rate and $\sigma$ is the producer's stake fraction.
+
+<sub>[1] [Crypto-benchmarks Sortition](https://github.com/input-output-hk/ouroboros-leios/blob/main/crypto-benchmarks.rs/Specification.md?plain=1#L64), [2] [Rust Simulation IB Generation](https://github.com/input-output-hk/ouroboros-leios/blob/main/sim-rs/sim-core/src/sim/node.rs#L561-L597)</sub>
+
+## Block Structure
+
+```cddl
+ input_block =
+   [ ib_header                  : ib_header
+   , transaction_bodies         : [* transaction_body]
+   , transaction_witness_sets   : [* transaction_witness_set]
+   , auxiliary_data_set         : {* transaction_index => auxiliary_data}
+   , invalid_transactions       : [* transaction_index]
+   ]
+```
+<sub>[1] [Formal Spec](https://github.com/input-output-hk/ouroboros-leios-formal-spec/blob/main/formal-spec/Leios/Blocks.agda#L40-L57), [2] [Haskell Simulation](https://github.com/input-output-hk/ouroboros-leios/blob/main/simulation/src/LeiosProtocol/Common.hs#L138-L142), [3] [Rust Simulation](https://github.com/input-output-hk/ouroboros-leios/blob/main/sim-rs/sim-core/src/model.rs#L136-L141)</sub>
+
+## Header Structure
+
+```cddl
+ ib_header =
+   [ ib_header_body       : ib_header_body
+   , body_signature       : kes_signature
+   ]
+
+ ib_header_body =
+   [ slot                 : slot_no                                  ; Slot when IB was created
+   , producer_id          : pool_id                                  ; Block producer identifier
+   , vrf_proof            : vrf_cert                                 ; VRF proof of eligibility to produce IB
+   , block_body_hash      : hash32                                   ; Hash of the block body
+   , ? ranking_block_ref  : hash32                                   ; Reference to ranking block for ledger state
+   ]
+```
+<sub>[1] [Formal Spec](https://github.com/input-output-hk/ouroboros-leios-formal-spec/blob/main/formal-spec/Leios/Blocks.agda#L40-L45), [2] [Haskell Simulation](https://github.com/input-output-hk/ouroboros-leios/blob/main/simulation/src/LeiosProtocol/Common.hs#L114-L124), [3] [Rust Simulation](https://github.com/input-output-hk/ouroboros-leios/blob/main/sim-rs/sim-core/src/model.rs#L127-L133)</sub>
+
+## Supporting Types
+
+```cddl
+ ; Block identifiers
+ ib_id = hash32                                                      ; Input block identifier (hash)
+
+ ; Basic types
+ pool_id = bytes                                                     ; Pool/producer identifier
+ slot_no = uint64                                                    ; Slot number
+ hash32 = bytes .size 32                                             ; 32-byte hash
+ vrf_cert = bytes                                                    ; VRF certificate/proof
+ kes_signature = bytes                                               ; KES signature
+``` 
+
+**→ [Endorser Block - CDDL](endorser-blocks.md)**

docs/cddl/diffs/common/ranking-blocks.md

@@ -0,0 +1,20 @@
+# Ranking Blocks - Leios CDDL
+
+Ranking Blocks (RBs) are extended Praos blocks that include optional Leios certificates.
+
+## Block Structure - (Conway) Extension
+
+```diff
+ ranking_block =
+   [ header                   : block_header
+   , transaction_bodies       : [* transaction_body]
+   , transaction_witness_sets : [* transaction_witness_set]
+   , auxiliary_data_set       : {* transaction_index => auxiliary_data}
+   , invalid_transactions     : [* transaction_index]
++  , ? leios_cert             : leios_certificate
+   ]
+```
+<sub>[1] [Conway Base](https://github.com/IntersectMBO/cardano-ledger/blob/master/eras/conway/impl/cddl-files/conway.cddl#L8-L14), [2] [Leios Base](https://github.com/input-output-hk/ouroboros-leios-formal-spec/blob/main/formal-spec/Leios/Base.agda#L21-L22)</sub>
+
+## Next
+**→ [Votes and Certificates - CDDL](votes-certificates.md)**

docs/cddl/diffs/common/votes-certificates.md

@@ -0,0 +1,141 @@
+# Votes and Certificates - Leios CDDL
+
+Leios introduces a new BLS-based voting system with certificates for endorser block validation.
+
+## Certificate Structure
+
+Leios certificates are embedded in Ranking Blocks as described in [Ranking Blocks - CDDL Changes](ranking-blocks.md). These certificates attest to the validity of Endorser Blocks as described in [Endorser Blocks - CDDL Changes](endorser-blocks.md). Here is the complete certificate structure:
+
+```cddl
+; Complete Leios certificate structure (from crypto-benchmarks implementation)
+leios_certificate =
+  [ election_id            : election_id                             ; 8-byte election identifier (EID)
+  , endorser_block_hash    : hash32                                  ; Hash of the endorsed block (EB)  
+  , persistent_voters      : [* persistent_voter_id]                 ; Set of persistent voter IDs
+  , nonpersistent_voters   : {* pool_id => bls_signature}            ; Non-persistent voters with eligibility proofs
+  , ? aggregate_elig_sig   : bls_signature                           ; Aggregate eligibility signature (present when non-persistent voters exist)
+  , aggregate_vote_sig     : bls_signature                           ; Aggregate BLS signature on (election_id || endorser_block_hash)
+  ]
+```
+<sub>[1] [Certificate Reference Implementation](https://github.com/input-output-hk/ouroboros-leios/blob/main/crypto-benchmarks.rs/src/cert.rs#L13-L21), [2] [Certificate Abstract Interface](https://github.com/input-output-hk/ouroboros-leios-formal-spec/blob/main/formal-spec/Leios/Base.agda#L24-L28)</sub>
+
+## Vote Structure
+
+The Leios voting system supports two types of voters: persistent voters (selected per epoch) and non-persistent voters (selected per election via local sortition).
+
+> [!Note]
+> Individual votes are ephemeral data structures used during the voting process. They are aggregated into certificates and do not appear on the ledger or persistent storage. Only the resulting certificates are stored permanently.
+
+```cddl
+; Vote bundle containing votes for multiple endorser blocks from same voter
+leios_vote_bundle = persistent_vote_bundle / non_persistent_vote_bundle
+
+persistent_vote_bundle =
+  [ 0                        ; Vote type identifier for persistent voter
+  , election_id              ; 8-byte election identifier  
+  , persistent_voter_id      ; 2-byte epoch-specific pool identifier
+  , vote_entries             ; Map of endorser blocks to signatures
+  ]
+
+non_persistent_vote_bundle =
+  [ 1                        ; Vote type identifier for non-persistent voter
+  , election_id              ; 8-byte election identifier
+  , pool_id                  ; 28-byte pool identifier
+  , eligibility_signature    ; 48-byte BLS signature proving eligibility
+  , vote_entries             ; Map of endorser blocks to signatures
+  ]
+
+vote_entries = {* endorser_block_hash => vote_signature}
+```
+<sub>[1] [Vote Reference Implementation](https://github.com/input-output-hk/ouroboros-leios/blob/main/crypto-benchmarks.rs/src/vote.rs#L13-L27), [2] [Formal Specification - Vote Abstract Interface](https://github.com/input-output-hk/ouroboros-leios-formal-spec/blob/main/formal-spec/Leios/Abstract.agda#L24-L27), [3] [Haskell Bundle Usage](https://github.com/input-output-hk/ouroboros-leios/blob/main/simulation/src/LeiosProtocol/Short.hs#L231-L234), [4] [Rust Vote Bundle](https://github.com/input-output-hk/ouroboros-leios/blob/main/sim-rs/sim-core/src/model.rs#L208-L212)</sub>
+
+## BLS Key Registration
+
+For pools to participate in Leios voting, they must register BLS keys in their operational certificates:
+
+```diff
+ operational_cert = 
+   [ hot_vkey          : kes_vkey    
+   , sequence_number   : uint .size 8
+   , kes_period        : uint        
+   , sigma             : signature   
++  , ? bls_key_reg     : bls_key_registration
+   ]
+```
+<sub>[1] [Conway Base](https://github.com/IntersectMBO/cardano-ledger/blob/master/eras/conway/impl/cddl-files/conway.cddl#L114-L119)</sub>
+
+```cddl
+; BLS key registration for voting (included in operational certificates)
+bls_key_registration =
+  [ pool_id               : pool_id                                    ; Pool identifier (28 bytes)
+  , bls_public_key        : bls_vkey                                   ; BLS12-381 G2 public key (96 bytes)
+  , proof_of_possession   : bls_proof_of_possession                    ; Proof of secret key possession (96 bytes)
+  , kes_signature         : kes_signature                              ; KES signature over the registration (448 bytes)
+  ]
+
+; Total size: 28 + 96 + 96 + 448 = 668 bytes
+```
+<sub>[1] [Registration Struct](https://github.com/input-output-hk/ouroboros-leios/blob/main/crypto-benchmarks.rs/src/key.rs#L156-L162), [2] [Proof Generation](https://github.com/input-output-hk/ouroboros-leios/blob/main/crypto-benchmarks.rs/src/bls_vote.rs#L19-L23)</sub>
+
+## Cryptographic Types
+
+```cddl
+; Core BLS cryptographic primitives
+bls_signature           = bytes .size 48                             ; BLS12-381 G1 signature (compressed)
+bls_vkey                = bytes .size 96                             ; BLS12-381 G2 public key (compressed)  
+bls_proof_of_possession =
+  [ mu1                 : bls_signature                              ; Signature on public key
+  , mu2                 : bls_signature                              ; Signature on empty message  
+  ]
+
+; Leios-specific identifiers  
+election_id             = bytes .size 8                              ; Slot-based election identifier
+persistent_voter_id     = uint .size 2                               ; Epoch-specific voter identifier (0-65535)
+pool_id                 = bytes .size 28                             ; Stake pool identifier
+endorser_block_hash     = bytes .size 32                             ; Hash of endorser block
+
+; Additional Cardano types used
+kes_signature           = bytes .size 448                            ; KES signature
+hash32                  = bytes .size 32                             ; 32-byte hash (used for endorser_block_hash)
+```
+<sub>[1] [Sig](https://github.com/input-output-hk/ouroboros-leios/blob/main/crypto-benchmarks.rs/src/key.rs#L100), [2] [PubKey](https://github.com/input-output-hk/ouroboros-leios/blob/main/crypto-benchmarks.rs/src/key.rs#L62), [3] [PoP](https://github.com/input-output-hk/ouroboros-leios/blob/main/crypto-benchmarks.rs/src/key.rs#L139-L143), [4] [Eid](https://github.com/input-output-hk/ouroboros-leios/blob/main/crypto-benchmarks.rs/src/primitive.rs#L76), [5] [PersistentId](https://github.com/input-output-hk/ouroboros-leios/blob/main/crypto-benchmarks.rs/src/registry.rs#L14), [6] [PoolKeyhash](https://github.com/input-output-hk/ouroboros-leios/blob/main/crypto-benchmarks.rs/src/primitive.rs#L14), [7] [EbHash](https://github.com/input-output-hk/ouroboros-leios/blob/main/crypto-benchmarks.rs/src/primitive.rs#L117), [8] [KesSig](https://github.com/input-output-hk/ouroboros-leios/blob/main/crypto-benchmarks.rs/src/primitive.rs#L170)</sub>
+
+## Committee Selection
+
+The Fait Accompli algorithm determines persistent voters for each epoch, while local sortition selects non-persistent voters for each election.
+
+```cddl
+; Result of Fait Accompli committee selection for an epoch
+fait_accompli_result =
+  [ epoch                 : epoch                                     ; Epoch this applies to
+  , persistent_voters     : [* persistent_voter_designation]          ; Designated persistent voters  
+  , total_persistent_stake : stake_weight                             ; Total stake of persistent voters
+  , non_persistent_stake  : stake_weight                              ; Remaining stake for local sortition
+  ]
+
+; Persistent voter designation
+persistent_voter_designation =
+  [ pool_id               : pool_id                                   ; Pool identifier  
+  , persistent_voter_id   : persistent_voter_id                       ; Epoch-specific short identifier
+  , stake_weight          : stake_weight                              ; Stake weight of this voter
+  ]
+
+; Local sortition result for non-persistent voters
+local_sortition_result =
+  [ pool_id               : pool_id                                   ; Pool identifier
+  , election_id           : election_id                               ; Election identifier  
+  , vrf_proof             : vrf_cert                                  ; VRF proof of eligibility
+  , vote_count            : vote_count                                ; Number of votes awarded (usually 0 or 1)
+  , stake_weight          : stake_weight                              ; Stake weight for this election
+  ]
+
+; Supporting types
+epoch                     = uint64                                    ; Epoch number
+stake_weight              = uint64                                    ; Stake amount in lovelace
+vrf_cert                  = bytes                                     ; VRF certificate from existing Cardano types
+vote_count                = uint8                                     ; Number of votes (typically 0 or 1)
+```
+<sub>[1] [FaSortition](https://github.com/input-output-hk/ouroboros-leios/blob/main/crypto-benchmarks.rs/src/fait_accompli.rs#L9-L17)</sub>
+
+## Next
+**→ [Endorser Block - CDDL](endorser-blocks.md)**

docs/cddl/diffs/full-sharding/input-blocks.md

@@ -0,0 +1,39 @@
+# Input Blocks - Full Sharding CDDL
+
+The common [`input_block`](../common/input-blocks.md#block-structure) structure is used with shard assignment in the IB header.
+
+## Sharded IB Header
+
+```diff
+; Common IB header body from leios-common.cddl
+ ib_header_body =
+   [ slot                  : slot_no
+   , producer              : node_id
+   , ib_certificate        : ib_cert
+   , ? vrf_proof           : vrf_cert
++  , shard                 : shard_id                              ; Shard assignment from VRF
+   ]
+```
+<sub>[1] [Common CDDL](../common/input-blocks.md#block-structure), [2] [Rust simulation](https://github.com/input-output-hk/ouroboros-leios/blob/main/sim-rs/sim-core/src/model.rs#L130)</sub>
+
+## Shard Assignment
+
+```cddl
+; Shard identifier (16-bit allows up to 65,536 shards)
+; Current simulation configs use 1-900 shards
+shard_id = uint .size 2
+
+; Shard assignment based on VRF value
+; Implementation: shard = vrf_value mod total_shards
+```
+<sub>[1] Ledger v0.2: "each IB has a shard id (determined through its VRF value)", [2] [Rust Shard Assignment](https://github.com/input-output-hk/ouroboros-leios/blob/main/sim-rs/sim-core/src/sim/node.rs#L599-L604)</sub>
+
+## Supporting Types
+
+```cddl
+; Basic types
+shard_id = uint .size 2                                             ; 16-bit shard identifier (current range: 1-900)
+slot_no = uint64                                                    ; Slot number
+```
+
+**→ [Sharded Transactions - CDDL](transactions.md)**