WIP

Author: Soupstraw

cabal.project

@@ -19,9 +19,10 @@ source-repository-package
   tag: cccfde6934ab0988fee3885ee160fffe04aa8274
 
 source-repository-package
+  --sha256: sha256-Q5DiWdyrAaZ18k8ZqYCMG6ChWkozjYGzBnKX382ZX0c=
   type: git
   location: https://github.com/input-output-hk/cuddle.git
-  tag: 11bf04472123122ae579ff3b913aa7adf35cf321
+  tag: 3a56bae35d8ed515fc65feb341afb4f74d8d11e7
 
 -- NOTE: If you would like to update the above,
 -- see CONTRIBUTING.md#to-update-the-referenced-agda-ledger-spec

eras/allegra/impl/cddl-files/allegra.cddl

@@ -1,6 +1,4 @@
 ; This file was auto-generated from huddle. Please do not modify it directly!
-;Pseudo-rule introduced by Cuddle to collect root elements
-huddle_root_defs = [block, transaction]
 
 block = 
   [ header
@@ -10,5 +8,332 @@ block =
   ]
 
 
+header = [header_body, body_signature: kes_signature]
+
+header_body = 
+  [ block_number: uint
+  , slot           : uint          
+  , prev_hash      : hash32/ nil   
+  , issuer_vkey    : vkey          
+  , vrf_vkey       : vrf_vkey      
+  , nonce_vrf      : vrf_cert      
+  , leader_vrf     : vrf_cert      
+  , block_body_size: uint .size 4  
+  , block_body_hash: hash32        
+  ,                operational_cert
+  ,                protocol_version
+  ]
+
+
+hash32 = bytes .size 32
+
+vkey = bytes .size 32
+
+vrf_vkey = bytes .size 32
+
+vrf_cert = [bytes, bytes .size 80]
+
+operational_cert = 
+  ( hot_vkey: kes_vkey
+  , sequence_number: uint     
+  , kes_period     : uint     
+  , sigma          : signature
+  )
+
+kes_vkey = bytes .size 32
+
+signature = bytes .size 64
+
+protocol_version = (major_protocol_version, uint)
+
+major_protocol_version = 1 .. 3
+
+kes_signature = bytes .size 448
+
+;Allegra transaction body adds the validity interval start at index 8
+transaction_body = 
+  { 0: set<transaction_input>
+   , 1: [*transaction_output]
+   , 2: coin                     
+   , 3: uint                     
+  , ?4: [*certificate]       
+  , ?5: withdrawals              
+  , ?6: update                   
+  , ?7: metadata_hash            
+  , ?8: uint                     
+  }
+
+
+set<a0> = [*a0]
+
+transaction_input = [transaction_id: hash32, index: uint .size 2]
+
+transaction_output = [address, amount: coin]
+
+;address = bytes
+;
+;address format:
+;  [ 8 bit header | payload ];
+;
+;shelley payment addresses:
+;     bit 7: 0
+;     bit 6: base/other
+;     bit 5: pointer/enterprise [for base: stake cred is keyhash/scripthash]
+;     bit 4: payment cred is keyhash/scripthash
+;  bits 3-0: network id
+;
+;reward addresses:
+;  bits 7-5: 111
+;     bit 4: credential is keyhash/scripthash
+;  bits 3-0: network id
+;
+;byron addresses:
+;  bits 7-4: 1000
+;
+;     0000: base address: keyhash28,keyhash28
+;     0001: base address: scripthash28,keyhash28
+;     0010: base address: keyhash28,scripthash28
+;     0011: base address: scripthash28,scripthash28
+;     0100: pointer address: keyhash28, 3 variable length uint
+;     0101: pointer address: scripthash28, 3 variable length uint
+;     0110: enterprise address: keyhash28
+;     0111: enterprise address: scripthash28
+;     1000: byron address
+;     1110: reward account: keyhash28
+;     1111: reward account: scripthash28
+;1001-1101: future formats
+address = 
+  h'001000000000000000000000000000000000000000000000000000000011000000000000000000000000000000000000000000000000000000'
+  / h'102000000000000000000000000000000000000000000000000000000022000000000000000000000000000000000000000000000000000000'
+  / h'203000000000000000000000000000000000000000000000000000000033000000000000000000000000000000000000000000000000000000'
+  / h'304000000000000000000000000000000000000000000000000000000044000000000000000000000000000000000000000000000000000000'
+  / h'405000000000000000000000000000000000000000000000000000000087680203'                                                
+  / h'506000000000000000000000000000000000000000000000000000000087680203'                                                
+  / h'6070000000000000000000000000000000000000000000000000000000'                                                        
+  / h'7080000000000000000000000000000000000000000000000000000000'                                                        
+
+coin = uint
+
+certificate = 
+  [  stake_registration             
+  // stake_deregistration           
+  // stake_delegation               
+  // pool_registration              
+  // pool_retirement                
+  // genesis_key_delegation         
+  // move_instantaneous_rewards_cert
+  ]
+
+
+;This will be deprecated in a future era
+stake_registration = (0, stake_credential)
+
+stake_credential = credential
+
+credential = [0, addr_keyhash// 1, script_hash]
+
+addr_keyhash = hash28
+
+hash28 = bytes .size 28
+
+;To compute a script hash, note that you must prepend
+;a tag to the bytes of the script before hashing.
+;The tag is determined by the language.
+;The tags in the Conway era are:
+;  "\x00" for multisig scripts
+;  "\x01" for Plutus V1 scripts
+;  "\x02" for Plutus V2 scripts
+;  "\x03" for Plutus V3 scripts
+script_hash = hash28
+
+;This will be deprecated in a future era
+stake_deregistration = (1, stake_credential)
+
+stake_delegation = (2, stake_credential, pool_keyhash)
+
+pool_keyhash = hash28
+
+pool_registration = (3, pool_params)
+
+pool_params = 
+  ( operator: pool_keyhash
+  , vrf_keyhash   : vrf_keyhash       
+  , pledge        : coin              
+  , cost          : coin              
+  , margin        : unit_interval     
+  , reward_account: reward_account    
+  , pool_owners   : set<addr_keyhash>
+  , relays        : [*relay]      
+  , pool_metadata : pool_metadata/ nil
+  )
+
+vrf_keyhash = hash32
+
+;The real unit_interval is: #6.30([uint, uint])
+;
+;A unit interval is a number in the range between 0 and 1, which
+;means there are two extra constraints:
+;  1. numerator <= denominator
+;  2. denominator > 0
+;
+;The relation between numerator and denominator can be
+;expressed in CDDL, but we have a limitation currently
+;(see: https://github.com/input-output-hk/cuddle/issues/30)
+;which poses a problem for testing. We need to be able to
+;generate random valid data for testing implementation of
+;our encoders/decoders. Which means we cannot use the actual
+;definition here and we hard code the value to 1/2
+unit_interval = #6.30([1, 2])
+
+;reward_account = bytes
+reward_account = 
+  h'E090000000000000000000000000000000000000000000000000000000'
+  / h'F0A0000000000000000000000000000000000000000000000000000000'
+
+relay = [single_host_addr// single_host_name// multi_host_name]
+
+single_host_addr = (0, port/ nil, ipv4/ nil, ipv6/ nil)
+
+port = uint .le 65535
+
+ipv4 = bytes .size 4
+
+ipv6 = bytes .size 16
+
+;dns_name: An A or AAAA DNS record
+single_host_name = (1, port/ nil, dns_name)
+
+dns_name = text .size (0 .. 64)
+
+;dns_name: An SRV DNS record
+multi_host_name = (2, dns_name)
+
+pool_metadata = [url, metadata_hash]
+
+url = text .size (0 .. 64)
+
+metadata_hash = hash32
+
+pool_retirement = (4, pool_keyhash, epoch)
+
+epoch = uint
+
+genesis_key_delegation = (5, genesis_hash, genesis_delegate_hash, vrf_keyhash)
+
+genesis_hash = hash28
+
+genesis_delegate_hash = hash28
+
+move_instantaneous_rewards_cert = (6, move_instantaneous_reward)
+
+;The first field determines where the funds are drawn from.
+;  0 denotes the reserves,
+;  1 denotes the treasury.
+;If the second field is a map, funds are moved to stake credentials.
+;Otherwise, the funds are given to the other accounting pot.
+;NOTE:
+;  This has been safely backported to Shelley from Alonzo.
+move_instantaneous_reward = [0/ 1, {*stake_credential: delta_coin}/ coin]
+
+;This too has been introduced in Shelley as a backport from Alonzo.
+delta_coin = int
+
+withdrawals = {*reward_account: coin}
+
+update = [proposed_protocol_parameter_updates, epoch]
+
+proposed_protocol_parameter_updates = {*genesis_hash: protocol_param_update}
+
+protocol_param_update = 
+  { ?0: uint ;minfee A
+  , ?1 : uint                   ;minfee B                            
+  , ?2 : uint                   ;max block body size                 
+  , ?3 : uint                   ;max transaction size                
+  , ?4 : uint .size 2           ;max block header size               
+  , ?5 : coin                   ;key deposit                         
+  , ?6 : coin                   ;pool deposit                        
+  , ?7 : epoch                  ;maximum epoch                       
+  , ?8 : uint .size 2           ;n_opt: desired number of stake pools
+  , ?9 : nonnegative_interval   ;pool pledge influence               
+  , ?10: unit_interval          ;expansion rate                      
+  , ?11: unit_interval          ;treasury growth rate                
+  , ?12: unit_interval          ;decentralization constant           
+  , ?13: nonce                  ;extra entropy                       
+  , ?14: [protocol_version] ;protocol version                    
+  , ?15: coin                   ;min utxo value                      
+  }
+
+
+nonnegative_interval = #6.30([uint, positive_int])
+
+positive_int = 1 .. maxWord64
+
+maxWord64 = 18446744073709551615
+
+nonce = [0// 1, bytes .size 32]
+
+transaction_witness_set = 
+  {?0: [*vkeywitness], ?1: [*native_script], ?2: [*bootstrap_witness]}
+
+vkeywitness = [vkey, signature]
+
+;Timelock validity intervals are half-open intervals [a, b).
+;
+;  invalid_before:
+;    specifies the left (included) endpoint a.
+;
+;  invalid_hereafter:
+;    specifies the right (excluded) endpoint b.
+native_script = 
+  [  script_pubkey    
+  // script_all       
+  // script_any       
+  // script_n_of_k    
+  // invalid_before   
+  // invalid_hereafter
+  ]
+
+
+script_pubkey = (0, addr_keyhash)
+
+script_all = (1, [*native_script])
+
+script_any = (2, [*native_script])
+
+script_n_of_k = (3, n: int64, [*native_script])
+
+int64 = -9223372036854775808 .. 9223372036854775807
+
+invalid_before = (4, uint)
+
+invalid_hereafter = (5, uint)
+
+bootstrap_witness = 
+  [ public_key: vkey
+  , signature : signature     
+  , chain_code: bytes .size 32
+  , attributes: bytes         
+  ]
+
+
+transaction_index = uint .size 2
+
+auxiliary_data = 
+  metadata
+  / [transaction_metadata: metadata, auxiliary_scripts: auxiliary_scripts]
+
+metadata = {*transaction_metadatum_label: transaction_metadatum}
+
+transaction_metadatum_label = uint
+
+transaction_metadatum = 
+  {*transaction_metadatum: transaction_metadatum}
+  / [*transaction_metadatum]
+  / int                         
+  / bytes .size (0 .. 64)    
+  / text .size (0 .. 64)     
+
+auxiliary_scripts = [*native_script]
+
 transaction = [transaction_body, transaction_witness_set, auxiliary_data/ nil]