Merge branch 'master' into 965-refactor-properties

Author: williamdemeo

build-tools/static/hs-src/src/MAlonzo/Code/Ledger/Foreign/API.hs

@@ -35,7 +35,8 @@ import MAlonzo.Code.Ledger.Conway.Foreign.HSLedger.Ledger            as X
 import MAlonzo.Code.Ledger.Conway.Foreign.HSLedger.NewEpoch          as X
   (NewEpochState(..), newEpochStep)
 import MAlonzo.Code.Ledger.Conway.Foreign.HSLedger.Ratify            as X
-  (StakeDistrs(..), RatifyEnv(..), RatifyState(..), ratifyStep)
+  (StakeDistrs(..), RatifyEnv(..), RatifyState(..), ratifyStep
+  ,acceptedBySPO, acceptedByDRep, acceptedByCC)
 import MAlonzo.Code.Ledger.Conway.Foreign.HSLedger.Rewards           as X
   (HsRewardUpdate(..), Snapshot(..), Snapshots(..))
 import MAlonzo.Code.Ledger.Conway.Foreign.HSLedger.Utxo              as X

src/Ledger/Conway/Conformance.agda

@@ -0,0 +1,76 @@
+This module provides the model used to do conformance testing of the Haskell
+implementation of the Ledger.
+
+The conformance model differs from the Conway specification in how deposits are
+stored in the Ledger state.
+
+In the Conway specification, deposits are stored in `LState.utxoSt.deposits`{.AgdaField}.
+The conformance model, on the other hand, separates deposits in three disjoint
+maps:
+
+* `LState.utxoSt.deposits`{.AgdaField}
+* `LState.certState.dState.deposits`{.AgdaField}
+* `LState.certState.gState.deposits`{.AgdaField}
+
+## Motivation
+
+The conformance model follows the way in which the Haskell implementation stores
+the deposits, which makes it possible to compare the behaviors of the conformance
+model and the implementation of the `UTXOS`{.AgdaDatatype} rule.
+
+The UTXOS rule transforms `UTxOState`s. While the specification updates the
+deposits in this rule, the implementation cannot do so because its input state
+does not contain the deposits in `DState` and `GState`.
+
+Other rules which use `UTXOS`{.AgdaDatatype} are in a similar predicament,
+namely `UTXO`{.AgdaDatatype} and `UTXOW`{.AgdaDatatype}. The
+`LEDGER`{.AgdaDatatype} rule, which uses `UTXOW`{.AgdaDatatype}, is the first
+rule where the implementation has all the state necessary to reconstruct the
+full deposits that the specification needs.
+
+## Guarantees
+
+Since we still want to check that the implementation behaves as the
+specification, there is a proof of the equivalence between the conformance model
+and the specification:
+
+* `Ledger.Conway.Conformance.Equivalence.bisimilarityProof`{.AgdaBound}
+
+## Alternatives
+
+Rather than providing a conformance model, we could have changed the Conway
+specification to match the implementation way of storing deposits. However,
+there are trade offs to consider. Putting the deposits together in one place
+makes some proofs simpler, while splitting them as in the implementation makes
+it more convenient to write the update functions for the separated pieces.
+
+While we could decide the tradeoff for a particular implementation, it would be
+difficult to adjust the specification when multiple implementations need to be
+accommodated.
+
+Yet another option could have been to skip testing specifically for the
+`UTXOS`{.AgdaDatatype} rule. This was a difficulty for testing, since spotting
+differences in a rule is harder when it is combined with other rules like the
+`LEDGER`{.AgdaDatatype} rule does.
+
+```agda
+{-# OPTIONS --safe #-}
+module Ledger.Conway.Conformance where
+
+import Ledger.Conway.Conformance.Certs
+import Ledger.Conway.Conformance.Certs.Properties
+import Ledger.Conway.Conformance.Chain
+import Ledger.Conway.Conformance.Chain.Properties
+import Ledger.Conway.Conformance.Equivalence
+import Ledger.Conway.Conformance.Epoch
+import Ledger.Conway.Conformance.Epoch.Properties
+import Ledger.Conway.Conformance.Gov
+import Ledger.Conway.Conformance.Ledger
+import Ledger.Conway.Conformance.Ledger.Properties
+import Ledger.Conway.Conformance.Properties
+import Ledger.Conway.Conformance.Utxo
+import Ledger.Conway.Conformance.Utxo.Properties
+import Ledger.Conway.Conformance.Utxow
+import Ledger.Conway.Conformance.Utxow.Properties
+import Ledger.Conway.Conformance.Script
+```

src/Ledger/Conway/Conformance.lagda.md

@@ -14,6 +14,8 @@ import Data.Rational.Show as Rational
 
 import Foreign.Haskell.Pair as F
 open import Ledger.Conway.Specification.Ratify it
+  hiding (acceptedByCC; acceptedByDRep; acceptedBySPO)
+import Ledger.Conway.Specification.Ratify it as Ratify
 open import Ledger.Conway.Specification.Ratify.Properties.Computational it
 
 instance
@@ -62,3 +64,18 @@ instance
   Show-RATIFIES : ∀ {Γ s sig s'}
     → Show (Γ ⊢ s ⇀⦇ sig  ,RATIFIES⦈ s')
   Show-RATIFIES {Γ} {s} {sig} .show r = "" -- ratify-debug (to Γ) (to s) (to sig)
+
+-- Expose acceptedBy predicates for conformance
+
+acceptedByCC : HsType (RatifyEnv → EnactState → GovActionState → Bool)
+acceptedByCC = λ Γ es st → to (does (acceptedByCC? (from Γ) (from es) (from st)))
+
+acceptedByDRep : HsType (RatifyEnv → EnactState → GovActionState → Bool)
+acceptedByDRep = λ Γ es st → to (does (acceptedByDRep? (from Γ) (from es) (from st)))
+
+acceptedBySPO : HsType (RatifyEnv → EnactState → GovActionState → Bool)
+acceptedBySPO = λ Γ es st → to (does (acceptedBySPO? (from Γ) (from es) (from st)))
+
+{-# COMPILE GHC acceptedByCC as acceptedByCC #-}
+{-# COMPILE GHC acceptedByDRep as acceptedByDRep #-}
+{-# COMPILE GHC acceptedBySPO as acceptedBySPO #-}

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

@@ -667,17 +667,17 @@ opaque
   Is-nothing? {x = x} = All.dec (const $ no id) x
     where import Data.Maybe.Relation.Unary.All as All
 
-  accepted? : ∀ Γ es st → Dec (accepted Γ es st)
-  accepted? Γ es st = acceptedByCC? Γ es st ×-dec acceptedByDRep? Γ es st ×-dec acceptedBySPO? Γ es st
-    where
-    acceptedByCC? : ∀ Γ es st → Dec (acceptedByCC Γ es st)
-    acceptedByCC? _ _ _ = _ ℚ.≤? _ ×-dec (_ ≥? _ ⊎-dec (Is-nothing? ×-dec ¿ _ ¿))
+  acceptedByCC? : ∀ Γ es st → Dec (acceptedByCC Γ es st)
+  acceptedByCC? _ _ _ = _ ℚ.≤? _ ×-dec (_ ≥? _ ⊎-dec (Is-nothing? ×-dec ¿ _ ¿))
+
+  acceptedByDRep? : ∀ Γ es st → Dec (acceptedByDRep Γ es st)
+  acceptedByDRep? _ _ _ = _ ℚ.≤? _
 
-    acceptedByDRep? : ∀ Γ es st → Dec (acceptedByDRep Γ es st)
-    acceptedByDRep? _ _ _ = _ ℚ.≤? _
+  acceptedBySPO? : ∀ Γ es st → Dec (acceptedBySPO Γ es st)
+  acceptedBySPO? _ _ _ = _ ℚ.≤? _
 
-    acceptedBySPO? : ∀ Γ es st → Dec (acceptedBySPO Γ es st)
-    acceptedBySPO? _ _ _ = _ ℚ.≤? _
+  accepted? : ∀ Γ es st → Dec (accepted Γ es st)
+  accepted? Γ es st = acceptedByCC? Γ es st ×-dec acceptedByDRep? Γ es st ×-dec acceptedBySPO? Γ es st
 
   expired? : ∀ e st → Dec (expired e st)
   expired? e st = ¿ expired e st ¿