Move non-computational properties to separate submodules

build-tools/static/md/nav.yml

@@ -32,28 +32,35 @@
         - BlockBody: Ledger.Conway.Specification.BlockBody.md
         - BlockBody/:
             - Properties: Ledger.Conway.Specification.BlockBody.Properties.md
+            - Properties/:
+              - Computational: Ledger.Conway.Specification.BlockBody.Properties.Computational.md
         - Certs: Ledger.Conway.Specification.Certs.md
         - Certs/:
           - Properties: Ledger.Conway.Specification.Certs.Properties.md
           - Properties/:
+            - Computational: Ledger.Conway.Specification.Certs.Properties.Computational.md
             - PoV: Ledger.Conway.Specification.Certs.Properties.PoV.md
             - PoVLemmas: Ledger.Conway.Specification.Certs.Properties.PoVLemmas.md
             - VoteDelegsVDeleg: Ledger.Conway.Specification.Certs.Properties.VoteDelegsVDeleg.md
         - Chain: Ledger.Conway.Specification.Chain.md
         - Chain/:
           - Properties: Ledger.Conway.Specification.Chain.Properties.md
           - Properties/:
+            - Computational: Ledger.Conway.Specification.Chain.Properties.Computational.md
             - CredDepsEqualDomRwds: Ledger.Conway.Specification.Chain.Properties.CredDepsEqualDomRwds.md
             - EpochStep: Ledger.Conway.Specification.Chain.Properties.EpochStep.md
             - GovDepsMatch: Ledger.Conway.Specification.Chain.Properties.GovDepsMatch.md
             - PParamsWellFormed: Ledger.Conway.Specification.Chain.Properties.PParamsWellFormed.md
         - Enact: Ledger.Conway.Specification.Enact.md
         - Enact/:
-          - Properties: Ledger.Conway.Specification.Enact.Properties.md
+            - Properties: Ledger.Conway.Specification.Enact.Properties.md
+            - Properties/:
+              - Computational: Ledger.Conway.Specification.Enact.Properties.Computational.md
         - Epoch: Ledger.Conway.Specification.Epoch.md
         - Epoch/:
           - Properties: Ledger.Conway.Specification.Epoch.Properties.md
           - Properties/:
+            - Computational: Ledger.Conway.Specification.Epoch.Properties.Computational.md
             - ConstRwds: Ledger.Conway.Specification.Epoch.Properties.ConstRwds.md
             - GovDepsMatch: Ledger.Conway.Specification.Epoch.Properties.GovDepsMatch.md
             - NoPropSameDReps: Ledger.Conway.Specification.Epoch.Properties.NoPropSameDReps.md
@@ -64,11 +71,14 @@
           - Actions: Ledger.Conway.Specification.Gov.Actions.md
           - Properties: Ledger.Conway.Specification.Gov.Properties.md
           - Properties/:
+            - Computational: Ledger.Conway.Specification.Gov.Properties.Computational.md
             - ChangePPGroup: Ledger.Conway.Specification.Gov.Properties.ChangePPGroup.md
         - Ledger.Ledger: Ledger.Conway.Specification.Ledger.md
         - Ledger.Ledger/:
           - Properties: Ledger.Conway.Specification.Ledger.Properties.md
           - Properties/:
+            - Base: Ledger.Conway.Specification.Ledger.Properties.Base.md
+            - Computational: Ledger.Conway.Specification.Ledger.Properties.Computational.md
             - GovDepsMatch: Ledger.Conway.Specification.Ledger.Properties.GovDepsMatch.md
             - PoV: Ledger.Conway.Specification.Ledger.Properties.PoV.md
         - PoolReap: Ledger.Conway.Specification.PoolReap.md
@@ -77,10 +87,14 @@
         - Ratify: Ledger.Conway.Specification.Ratify.md
         - Ratify/:
           - Properties: Ledger.Conway.Specification.Ratify.Properties.md
+          - Properties/:
+            - Computational: Ledger.Conway.Specification.Ratify.Properties.Computational.md
         - Rewards: Ledger.Conway.Specification.Rewards.md
         - RewardUpdate: Ledger.Conway.Specification.RewardUpdate.md
         - RewardUpdate/:
             - Properties: Ledger.Conway.Specification.RewardUpdate.Properties.md
+            - Properties/:
+              - Computational: Ledger.Conway.Specification.RewardUpdate.Properties.Computational.md
         - Script: Ledger.Conway.Specification.Script.md
         - Script/:
           - Base: Ledger.Conway.Specification.Script.Base.md
@@ -96,11 +110,16 @@
         - Utxo/:
           - Properties: Ledger.Conway.Specification.Utxo.Properties.md
           - Properties/:
+            - Base: Ledger.Conway.Specification.Utxo.Properties.Base.md
+            - Computational: Ledger.Conway.Specification.Utxo.Properties.Computational.md
+            - GenMinspend: Ledger.Conway.Specification.Utxo.Properties.GenMinSpend.md
             - MinSpend: Ledger.Conway.Specification.Utxo.Properties.MinSpend.md
             - PoV: Ledger.Conway.Specification.Utxo.Properties.PoV.md
         - Utxow: Ledger.Conway.Specification.Utxow.md
         - Utxow/:
-          - Properties: Ledger.Conway.Specification.Utxow.Properties.md
+            - Properties: Ledger.Conway.Specification.Utxow.Properties.md
+            - Properties/:
+              - Computational: Ledger.Conway.Specification.Utxow.Properties.Computational.md
         - Test:
           - Examples: Ledger.Conway.Specification.Test.Examples.md
           - Examples/:

src/Ledger/Conway/Conformance/Epoch/Properties.agda

@@ -14,7 +14,7 @@ module Ledger.Conway.Conformance.Epoch.Properties
 open import Ledger.Conway.Conformance.Epoch txs abs
 open import Ledger.Conway.Conformance.Ledger txs abs
 open import Ledger.Conway.Specification.Ratify txs
-open import Ledger.Conway.Specification.Ratify.Properties txs
+open import Ledger.Conway.Specification.Ratify.Properties.Computational txs
 open import Ledger.Conway.Conformance.Certs govStructure
 open import Ledger.Conway.Conformance.Rewards txs abs
 

src/Ledger/Conway/Conformance/Ledger/Properties.agda

@@ -16,7 +16,7 @@ open import Ledger.Conway.Specification.Enact govStructure
 open import Ledger.Conway.Conformance.Epoch txs abs
 open import Ledger.Conway.Conformance.Certs.Properties govStructure
 open import Ledger.Conway.Specification.Gov txs
-open import Ledger.Conway.Specification.Gov.Properties txs
+open import Ledger.Conway.Specification.Gov.Properties.Computational txs
 open import Ledger.Conway.Conformance.Ledger txs abs
 open import Ledger.Conway.Specification.Ratify txs hiding (vote)
 open import Ledger.Conway.Conformance.Utxo txs abs

src/Ledger/Conway/Foreign/HSLedger/Enact.agda

@@ -7,7 +7,7 @@ open import Ledger.Conway.Foreign.HSLedger.PParams
 open import Ledger.Conway.Foreign.HSLedger.Gov.Actions
 
 open import Ledger.Conway.Specification.Enact govStructure
-open import Ledger.Conway.Specification.Enact.Properties govStructure
+open import Ledger.Conway.Specification.Enact.Properties.Computational govStructure
 
 instance
   HsTy-EnactState = autoHsType EnactState ⊣ withConstructor "MkEnactState"

src/Ledger/Conway/Foreign/HSLedger/Gov.agda

@@ -14,7 +14,7 @@ open import Ledger.Conway.Conformance.Certs govStructure
 open import Ledger.Conway.Specification.Enact govStructure
 open import Ledger.Conway.Conformance.Gov it it
 import Ledger.Conway.Specification.Gov it as L
-open import Ledger.Conway.Specification.Gov.Properties it
+open import Ledger.Conway.Specification.Gov.Properties.Computational it
 
 instance
 

src/Ledger/Conway/Foreign/HSLedger/Ratify.agda

@@ -14,7 +14,7 @@ import Data.Rational.Show as Rational
 
 import Foreign.Haskell.Pair as F
 open import Ledger.Conway.Specification.Ratify it
-open import Ledger.Conway.Specification.Ratify.Properties it
+open import Ledger.Conway.Specification.Ratify.Properties.Computational it
 
 instance
   HsTy-StakeDistrs = autoHsType StakeDistrs

src/Ledger/Conway/Specification.agda

@@ -1,38 +1,30 @@
 {-# OPTIONS --safe #-}
 module Ledger.Conway.Specification where
 
+import Ledger.Conway.Specification.BlockBody
+import Ledger.Conway.Specification.BlockBody.Properties
 import Ledger.Conway.Specification.Certs
 import Ledger.Conway.Specification.Certs.Properties
-import Ledger.Conway.Specification.Certs.Properties.PoV
-import Ledger.Conway.Specification.Certs.Properties.PoVLemmas
-import Ledger.Conway.Specification.Certs.Properties.VoteDelegsVDeleg
 import Ledger.Conway.Specification.Chain
 import Ledger.Conway.Specification.Chain.Properties
-import Ledger.Conway.Specification.Chain.Properties.CredDepsEqualDomRwds
-import Ledger.Conway.Specification.Chain.Properties.EpochStep
-import Ledger.Conway.Specification.Chain.Properties.GovDepsMatch
-import Ledger.Conway.Specification.Chain.Properties.PParamsWellFormed
 import Ledger.Conway.Specification.Enact
 import Ledger.Conway.Specification.Enact.Properties
 import Ledger.Conway.Specification.Epoch
 import Ledger.Conway.Specification.Epoch.Properties
-import Ledger.Conway.Specification.Epoch.Properties.ConstRwds
-import Ledger.Conway.Specification.Epoch.Properties.GovDepsMatch
-import Ledger.Conway.Specification.Epoch.Properties.NoPropSameDReps
 import Ledger.Conway.Specification.Fees
 import Ledger.Conway.Specification.Gov
 import Ledger.Conway.Specification.Gov.Actions
 import Ledger.Conway.Specification.Gov.Properties
 import Ledger.Conway.Specification.Gov.Properties.ChangePPGroup
 import Ledger.Conway.Specification.Ledger
 import Ledger.Conway.Specification.Ledger.Properties
-import Ledger.Conway.Specification.Ledger.Properties.GovDepsMatch
-import Ledger.Conway.Specification.Ledger.Properties.PoV
 import Ledger.Conway.Specification.PParams
 import Ledger.Conway.Specification.Properties
 import Ledger.Conway.Specification.Ratify
 import Ledger.Conway.Specification.Ratify.Properties
 import Ledger.Conway.Specification.Rewards
+import Ledger.Conway.Specification.RewardUpdate
+import Ledger.Conway.Specification.RewardUpdate.Properties
 import Ledger.Conway.Specification.Script
 import Ledger.Conway.Specification.Script.Validation
 import Ledger.Conway.Specification.Test.Examples
@@ -45,7 +37,5 @@ import Ledger.Conway.Specification.Transaction
 import Ledger.Conway.Specification.Types.GovStructure
 import Ledger.Conway.Specification.Utxo
 import Ledger.Conway.Specification.Utxo.Properties
-import Ledger.Conway.Specification.Utxo.Properties.MinSpend
-import Ledger.Conway.Specification.Utxo.Properties.PoV
 import Ledger.Conway.Specification.Utxow
 import Ledger.Conway.Specification.Utxow.Properties

src/Ledger/Conway/Specification/BlockBody/Properties.agda

@@ -0,0 +1,5 @@
+{-# OPTIONS --safe #-}
+
+module Ledger.Conway.Specification.BlockBody.Properties where
+
+open import Ledger.Conway.Specification.BlockBody.Properties.Computational

src/Ledger/Conway/Specification/BlockBody/Properties.lagda.md → src/Ledger/Conway/Specification/BlockBody/Properties/Computational.agda

@@ -1,15 +1,14 @@
-```agda
 {-# OPTIONS --safe #-}
 
 open import Ledger.Conway.Specification.Transaction using (TransactionStructure)
 open import Ledger.Conway.Specification.Abstract using (AbstractFunctions)
 
-module Ledger.Conway.Specification.BlockBody.Properties
+module Ledger.Conway.Specification.BlockBody.Properties.Computational
   (txs : _) (open TransactionStructure txs)
   (abs : AbstractFunctions txs) (open AbstractFunctions abs)
   where
 open import Ledger.Conway.Specification.BlockBody txs abs
-open import Ledger.Conway.Specification.Ledger.Properties txs abs
+open import Ledger.Conway.Specification.Ledger.Properties.Computational txs abs
 open import Ledger.Prelude
 
 open Computational ⦃...⦄
@@ -26,4 +25,3 @@ instance
     (BBODY-Block-Body (_ , _ , lsStep))
     with recomputeProof lsStep | completeness _ _ _ _ lsStep
   ... | success _ | refl = refl
-```