Add Cardadno/Ledger/Shelley finetypes files

lib/fine-types/fine-types.cabal

@@ -97,5 +97,6 @@ test-suite unit
     Spec.hs
   other-modules:
     Language.FineTypes.Export.OpenAPI.TypSpec
+    Language.FineTypes.Cardano.Ledger.ShelleySpec
     Language.FineTypes.ParserSpec
     Language.FineTypes.ValueSpec

lib/fine-types/test/Language/FineTypes/Cardano/Ledger/ShelleySpec.hs

@@ -0,0 +1,30 @@
+module Language.FineTypes.Cardano.Ledger.ShelleySpec where
+
+import Prelude
+
+import Language.FineTypes.Module (collectNotInScope)
+import Language.FineTypes.Parser (parseFineTypes, parseFineTypes')
+import Test.Hspec (Spec, describe, it, shouldBe, shouldSatisfy)
+
+import Data.Either (isRight)
+import qualified Data.Set as Set
+
+ledgerShelleySpec :: FilePath -> Spec
+ledgerShelleySpec fp = do
+    describe ("parseFineTypes applied to " <> fp) $ do
+        it "parses the file" $ do
+            file <- readFile fp
+            parseFineTypes' file `shouldSatisfy` isRight
+        it "detects constants" $ do
+            file <- readFile fp
+            Just m <- pure $ parseFineTypes file
+            collectNotInScope m `shouldBe` Set.empty
+
+spec :: Spec
+spec = do
+    ledgerShelleySpec "test/data/Cardano/Ledger/Shelley/Crypto.fine"
+    ledgerShelleySpec "test/data/Cardano/Ledger/Shelley/PParams.fine"
+    ledgerShelleySpec "test/data/Cardano/Ledger/Shelley/Address.fine"
+    ledgerShelleySpec "test/data/Cardano/Ledger/Shelley/Block.fine"
+    ledgerShelleySpec "test/data/Cardano/Ledger/Shelley/Tx.fine"
+    ledgerShelleySpec "test/data/Cardano/Ledger/Shelley/Delegation.fine"

lib/fine-types/test/data/Cardano/Ledger/Shelley/Address.fine

@@ -0,0 +1,60 @@
+module Address where 
+
+import PParams(Slot, Ix);
+import Crypto(KeyHash, ScriptHash);
+
+{-----------------------------------------------------------------------------
+    Addresses, Shelley spec , fig 6
+------------------------------------------------------------------------------}
+
+Ix = ℕ; -- index
+Slot = ℕ; -- absolute slot number
+
+Network = 
+    Σ{ testnet : Unit
+     , mainnet : Unit
+     };
+
+Credential = KeyHash + ScriptHash;
+
+-- certificate pointer
+Ptr = Slot × Ix × Ix; 
+
+-- base address
+Addr-base = 
+    { network : Network
+    , credential-pay : Credential
+    , credential-stake : Credential
+    };
+
+-- pointer address
+Addr-ptr = 
+    { network : Network
+    , credential-pay : Credential
+    , ptr : Ptr
+    };
+
+-- enterprise address
+Addr-enterprise = 
+    { network : Network
+    , credential-pay : Credential
+    };
+
+-- bootstrap address
+Addr-bootstrap = 
+    { network : Network
+    , key-hash-pay : KeyHash
+    };
+
+-- reward account
+Addr-rwd = 
+    { network : Network
+    , credential-stake : Credential
+    };
+
+-- output address
+Addr = Addr-base 
+    + Addr-ptr 
+    + Addr-enterprise 
+    + Addr-bootstrap 
+    + Addr-rwd;

lib/fine-types/test/data/Cardano/Ledger/Shelley/Block.fine

@@ -0,0 +1,42 @@
+module Block where
+
+import Crypto(VKey,Sig);
+import PParams(Slot,Seed,ProtVer);
+import Tx(Tx);
+
+HashHeader = _;  -- hash of a block header
+HashBBody = _; -- hash of a block body
+BlockNo = _; -- block number
+Proof = _; -- VRF proof
+KESPeriod = _; -- KES period
+VKey-ev = _; -- public verifying key
+
+-- Operational Certificate
+OCert = 
+    { vkhot : VKey-ev -- operational (hot) key
+    , n : ℕ -- certificate issue number
+    , c0 : KESPeriod -- start KES period
+    , σ : Sig -- cold key signature
+    };
+
+-- Block Header Body
+BHBody = 
+    { prev : HashHeader? -- hash of previous block header
+    , vk : VKey -- block issuer
+    , vrfVk : VKey  -- VRF verification key
+    , blockno : BlockNo -- block number
+    , slot : Slot -- block slot
+    , η : Seed -- nonce
+    , prf-η : Proof -- nonce proof
+    , ℓ : {x : ℚ | x ∈ [0, 1]}  -- leader election value
+    , prf-ℓ : Proof -- leader election proof
+    , bsize : ℕ -- size of the block body
+    , bhash : HashBBody -- block body hash
+    , oc : OCert -- operational certificate
+    , pv : ProtVer -- protocol version
+    };
+
+-- Block Types
+
+BHeader = BHBody × Sig;
+Block = BHeader × Tx∗;

lib/fine-types/test/data/Cardano/Ledger/Shelley/Crypto.fine

@@ -0,0 +1,7 @@
+module Crypto where 
+
+VKey = _ ; -- public verifying key
+KeyHash = _ ; -- hash of a public key
+ScriptHash = _ ; -- hash of a script
+Script = _ ; -- multi-signature script
+Sig = _ ; -- signature

lib/fine-types/test/data/Cardano/Ledger/Shelley/Delegation.fine

@@ -0,0 +1,82 @@
+module Delegation where 
+
+import Address(Addr-rwd, Credential);
+import PParams(Coin, Epoch);
+import Crypto(KeyHash);
+
+
+Credential-stake = _;
+KeyHash-vrf = _;
+KeyHashG = _;
+PoolMDHash = _;
+Url = _ ; -- URL
+ReservesMIR = _ ; -- reserves pot
+TreasuryMIR = _ ; -- treasury pot
+
+MIRPot = ReservesMIR + TreasuryMIR;
+
+DCert-regkey = 
+    { regCred : Credential
+    };
+
+DCert-deregkey = 
+    { cwitness : Credential
+    };
+
+DCert-delegate = 
+    { cwitness : Credential
+    , dpool : KeyHash
+    };
+
+DCert-regpool = 
+    { cwitness : Credential 
+    , poolParam : PoolParam
+    };
+
+DCert-retirepool = 
+    { cwitness : Credential
+    , retire : Epoch
+    };
+
+DCert-genesis = 
+    { cwitness : Credential
+    , genesisDeleg : KeyHashG × KeyHash × KeyHash-vrf
+    };
+
+DCert-mir = 
+    { credCoinMap : Credential-stake → Coin
+    , mirPot : MIRPot
+    };
+
+-- Delegation Certificate types
+DCert 
+    = DCert-regkey 
+    + DCert-deregkey 
+    + DCert-delegate
+    + DCert-regpool 
+    + DCert-retirepool 
+    + DCert-genesis
+    + DCert-mir;
+
+-- stake pool metadata
+PoolMD = Url × PoolMDHash; -- stake pool metadata
+
+-- Stake pool parameters
+PoolParam 
+    = ℙ KeyHash 
+    × Coin 
+    × {x : ℚ | [0, 1]}
+    × Coin
+    × Addr-rwd 
+    × KeyHash-vrf
+    × Url*
+    × PoolMD?; 
+
+PoolParam = 
+    { poolOwners : ℙ KeyHash -- stake pool owners
+    , poolCost : Coin -- stake pool cost
+    , poolMargin : {x : ℚ | [0, 1]} -- stake pool margin
+    , poolPledge : Coin -- stake pool pledge
+    , poolRAcnt : Addr-rwd -- stake pool reward account
+    , poolVRF : KeyHash-vrf -- stake pool VRF key hash
+    };

lib/fine-types/test/data/Cardano/Ledger/Shelley/PParams.fine

@@ -0,0 +1,31 @@
+module PParams where
+
+
+{-----------------------------------------------------------------------------
+    Protocol parameters
+    Shelley spec, Figure 7
+------------------------------------------------------------------------------}
+
+Coin = ℤ; -- unit of value
+Epoch = ℕ;  -- epoch number
+Seed = ℕ; -- seed for random number generator
+ProtVer = ℕ × ℕ; -- protocol version
+
+PParams = 
+    { a : ℤ  -- min fee factor
+    , b : ℤ  -- min fee constant
+    , maxBlockSize : ℕ  -- max block body size
+    , maxTxSize : ℕ  -- max transaction size
+    , maxHeaderSize : ℕ  -- max block header size
+    , poolDeposit : Coin  -- stake pool deposit
+    , Emax : Epoch  -- epoch bound on pool retirement
+    , nopt : { x : ℕ | x > 0 }  -- desired number of pools
+    , a0 : { x : ℚ | x ∈ [0, ∞) }  -- pool influence
+    , τ :  { y : ℚ | y ∈ [0, 1] }  -- treasury expansion
+    , ρ : { x : ℚ | x ∈ [0, 1] }  -- monetary expansion
+    , d : { x : ℚ | x ∈ {0 , 1/100, 2/100, .... , 1} }  -- decentralization parameter
+    , extraEntropy : Seed  -- extra entropy
+    , pv : ProtVer  -- protocol version
+    , minUTxOValue : Coin  -- minimum allowed value of a new TxOut
+    , minPoolCost : Coin  -- minimum allowed stake pool cost
+    };

lib/fine-types/test/data/Cardano/Ledger/Shelley/Tx.fine

@@ -0,0 +1,42 @@
+module Tx where
+
+import Address(Addr, Addr-rwd, Ix);
+import Crypto(VKey, Sig, ScriptHash, Script);
+import PParams(Coin, Slot);
+import Delegation(DCert);
+
+-- Abstract 
+
+TxId = _ ; -- transaction identifier
+Metadatum = _ ; -- metadatum
+MetadataHash = _ ; -- hash of transaction metadata
+Update = _ ; -- protocol parameter update
+
+
+-- Derived 
+TxIn = TxId × Ix; -- transaction input
+TxOut = Addr × Coin; -- transaction output
+UTxO = TxIn → TxOut; -- unspent tx outputs
+Wdrl = Addr-rwd → Coin; -- reward withdrawal
+Metadata = ℕ → Metadatum; -- metadata
+
+TxBody = 
+    { txins : ℙ TxIn  -- transaction inputs
+    , txouts : Ix → TxOut  --  transaction outputs
+    , txcerts : DCert∗  -- delegation certificates
+    , txfee : Coin  -- transaction fee
+    , txttl : Slot  -- time to live
+    , txwdrls : Wdrl  -- withdrawals
+    , txwitsVKey : VKey → Sig --  VKey witnesses
+    , txwitsScript : ScriptHash → Script --  script witnesses
+    , txMDhash : MetadataHash? --  metadata hash  
+    , txbody : TxBody  -- transaction body
+    };
+
+Tx = 
+    { txup : Update? --  protocol parameter update
+    , txMD : Metadata? --  metadata
+    , txWitness : TxWitness --  transaction witnesses
+    };
+
+TxWitness = (VKey → Sig) × (ScriptHash → Script);