Merge pull request #15 from input-output-hk/andre/extend-model

Various extensions to the model

.gitignore

@@ -1,3 +1,3 @@
 *.agdai
-result*
-.DS_Store
+.DS_Store
+result*

default.nix

@@ -106,6 +106,7 @@ in {
     })];
     buildPhase = ''
       agda --latex Ledger.lagda
+      ls Ledger/*.lagda | xargs -n 1 agda --latex
       cd latex && latexmk -xelatex Ledger.tex && cd ..
     '';
     installPhase = ''

src/ComputationalRelation.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe #-}
 
 module ComputationalRelation where
 
@@ -67,3 +67,7 @@ module _ {STS : C → S → Sig → S → Set} (comp comp' : Computational STS)
 
   compute-ext≡ : compute₁ c s sig ≡ compute₂ c s sig
   compute-ext≡ = ExtendedRel-rightUnique comp (ExtendedRel-compute comp) (ExtendedRel-compute comp')
+
+Computational⇒Dec' : ⦃ _ : DecEq S ⦄ {STS : C → S → Sig → S → Set} ⦃ comp : Computational STS ⦄
+                      → Dec (STS c s sig s')
+Computational⇒Dec' ⦃ comp = comp ⦄ = Computational⇒Dec comp

src/DecEq.agda

@@ -1,19 +1,17 @@
-{-# OPTIONS --without-K --safe #-}
+{-# OPTIONS --safe #-}
 
+open import Prelude
+
+open import Relation.Binary hiding (_⇔_)
+open import Relation.Binary.PropositionalEquality.WithK
 open import Relation.Nullary
 open import Relation.Nullary.Decidable
-open import Relation.Binary.PropositionalEquality
-open import Relation.Binary
-open import Data.Bool using (Bool; true; false)
-open import Data.Nat using (ℕ)
-open import Data.Maybe using (Maybe)
-open import Data.Maybe.Properties
-open import Data.Product
-import Data.Product.Properties
-open import Data.Empty
 
 module DecEq where
 
+private variable a : Level
+                 A B : Set a
+
 record DecEq {a} (A : Set a) : Set a where
   field
     _≟_ : DecidableEquality A
@@ -28,12 +26,41 @@ a ≡ᵇ a' = ⌊ a ≟ a' ⌋
 ... | no ¬p = ⊥-elim (¬p refl)
 ... | yes p = refl
 
+↔-DecEq : A ↔ B → DecEq A → DecEq B
+↔-DecEq A↔B record { _≟_ = _≟_ } ._≟_ b₁ b₂ =
+  Relation.Nullary.Decidable.map record
+    { to = λ fb₁≡fb₂ → trans (sym $ inverseˡ b₁) (trans (cong to fb₁≡fb₂) (inverseˡ b₂))
+    ; from = from-cong
+    ; to-cong = λ _ → ≡-irrelevant _ _
+    ; from-cong = λ _ → ≡-irrelevant _ _ }
+    (from b₁ ≟ from b₂)
+    where open Inverse A↔B
+
+import Data.List.Properties
+import Data.Maybe.Properties
+import Data.Product.Properties
+import Data.Sum.Properties
+import Data.Nat
+import Data.Unit
+
 instance
-  DecEq-Nat : DecEq ℕ
-  DecEq-Nat = record { _≟_ = Data.Nat._≟_ }
+  DecEq-⊥ : DecEq ⊥
+  DecEq-⊥ = record { _≟_ = λ () }
+
+  DecEq-⊤ : DecEq ⊤
+  DecEq-⊤ = record { _≟_ = Data.Unit._≟_ }
+
+  DecEq-ℕ : DecEq ℕ
+  DecEq-ℕ = record { _≟_ = Data.Nat._≟_ }
 
   DecEq-Maybe : ∀ {a} {A : Set a} → {{DecEq A}} → DecEq (Maybe A)
   DecEq-Maybe {{h}} = record { _≟_ = Data.Maybe.Properties.≡-dec (DecEq._≟_ h) }
 
+  DecEq-List : ∀ {a} {A : Set a} → {{DecEq A}} → DecEq (List A)
+  DecEq-List {{h}} = record { _≟_ = Data.List.Properties.≡-dec (DecEq._≟_ h) }
+
   DecEq-Product : ∀ {a} {A B : Set a} → {{DecEq A}} → {{DecEq B}} → DecEq (A × B)
   DecEq-Product {{h}} {{h'}} = record { _≟_ = Data.Product.Properties.≡-dec (DecEq._≟_ h) (DecEq._≟_ h') }
+
+  DecEq-Sum : ∀ {a} {A B : Set a} → {{DecEq A}} → {{DecEq B}} → DecEq (A ⊎ B)
+  DecEq-Sum {{h}} {{h'}} = record { _≟_ = Data.Sum.Properties.≡-dec (DecEq._≟_ h) (DecEq._≟_ h') }

src/FinMap.agda

@@ -5,11 +5,12 @@ open import Data.Maybe hiding (map)
 open import Data.Product using (_×_; _,_; proj₁; proj₂; curry; uncurry)
 open import Function hiding (Inverse)
 open import Relation.Nullary
+import Relation.Nullary.Decidable
 open import Relation.Nullary.Negation
 open import Relation.Unary using (Pred)
 open import DecEq
 open import FiniteSubset hiding (_∪_; _∩_)
-open import FinSet hiding (∅; map; indexedSum; _∈_; All)
+open import FinSet hiding (∅; map; indexedSum; _∈_; All; all?)
 open import Utilities.ListProperties using (_SubSetOf_)
 open import Algebra using (CommutativeMonoid)
 open import Level
@@ -38,6 +39,12 @@ module _ {K V : Set} {{_ : DecEq K}} {{_ : DecEq V}} where
   _⋪_ : FinSet K → FinMap K V → FinMap K V
   set ⋪ map = filterᵐ (λ x → ¬? (proj₁ x ∈? set)) map
 
+  _|^_ : FinMap K V → FinSet V → FinMap K V
+  map |^ set = filterᵐ (λ x → proj₂ x ∈? set) map
+
+  _|^'_ : {P : V → Set} → FinMap K V → (∀ a → Dec (P a)) → FinMap K V
+  map |^' set = filterᵐ (λ x → set (proj₂ x)) map
+
   values : FinMap K V → List V
   values m = map proj₂ $ listOfᵐ m
 
@@ -62,10 +69,13 @@ module _ {K V : Set} {{_ : DecEq K}} {{_ : DecEq V}} where
   _⊆ᵐ_ : FinMap K V → FinMap K V → Set
   m ⊆ᵐ m' = (listOfᵐ m) SubSetOf (listOfᵐ m')
 
-  All : ∀ {ℓ} → Pred (K × V) ℓ → FinMap K V → Set ℓ
-  All P s = FinSet.All P (FinSet.fromList $ listOfᵐ s)
+  record All {ℓ} (P : Pred (K × V) ℓ) (m : FinMap K V) : Set ℓ where
+    field FMAll : FinSet.All P (FinSet.fromList $ listOfᵐ m)
 
-module _ {K V : Set} {{_ : DecEq K}}{{_ : DecEq V}} {p} {{M : CommutativeMonoid 0ℓ p}} where
+  all? : ∀ {ℓ} → {P : Pred (K × V) ℓ} → Relation.Unary.Decidable P → (m : FinMap K V) → Dec (All P m)
+  all? P? m = Relation.Nullary.Decidable.map (mk⇔ (λ x → record { FMAll = x }) (λ where record { FMAll = x } → x)) (FinSet.all? P? (FinSet.fromList $ listOfᵐ m))
+
+module _ {K V : Set} {{_ : DecEq K}} {{_ : DecEq V}} {p} {{M : CommutativeMonoid 0ℓ p}} where
   open CommutativeMonoid M
 
   indexedSumLᵐ : ((K × V) → Carrier) → List (K × V) → Carrier
@@ -74,4 +84,8 @@ module _ {K V : Set} {{_ : DecEq K}}{{_ : DecEq V}} {p} {{M : CommutativeMonoid
   indexedSumᵐ : ((K × V) → Carrier) → FinMap K V → Carrier
   indexedSumᵐ f (fs-nojunk els) = foldr (λ x → f x ∙_) ε els
 
-  syntax indexedSumᵐ (λ a → x) m = Σᵐ[ a ← m ] x
+  indexedSumᵐ' : (V → Carrier) → FinMap K V → Carrier
+  indexedSumᵐ' f (fs-nojunk els) = foldr (λ x → f (proj₂ x) ∙_) ε els
+
+  syntax indexedSumᵐ  (λ a → x) m = Σᵐ[ a ← m ] x
+  syntax indexedSumᵐ' (λ a → x) m = Σᵐ'[ a ← m ] x

src/FinSet.agda

@@ -27,6 +27,7 @@ open import Function
 open import FiniteSubset hiding (_∪_; _∩_; fromList)
 open import DecEq
 open import Utilities.ListProperties hiding (head) renaming (_∈_ to _∈l_)
+import Function.Related.Propositional as P
 
 module FinSet where
 
@@ -47,18 +48,34 @@ module _ {A : Set} {{h : DecEq A}} where
   filter : {P : A → Set} → (∀ a → Dec (P a)) → FinSet A → FinSet A
   filter P? s = fromList (Data.List.filter P? $ elements s)
 
-  All : ∀ {ℓ} → Pred A ℓ → FinSet A → Set ℓ
-  All P s = Data.List.Relation.Unary.All.All P (elements s)
+  record All {ℓ} (P : Pred A ℓ) (s : FinSet A) : Set ℓ where
+    field FSAll : Data.List.Relation.Unary.All.All P (elements s)
 
   all? : ∀ {ℓ} → {P : Pred A ℓ} → Relation.Unary.Decidable P → Relation.Unary.Decidable (All P)
-  all? P? s = Data.List.Relation.Unary.All.all? P? (elements s)
+  all? P? s = Relation.Nullary.Decidable.map (mk⇔ (λ x → record { FSAll = x }) (λ where record { FSAll = x } → x)) (Data.List.Relation.Unary.All.all? P? (elements s))
 
   infix 5 _∈_
   _∈_ : A → FinSet A → Set
   a ∈ s = a ∈l elements s
 
   _∈?_ : Decidable _∈_
-  a ∈? s = Utilities.ListProperties.eq2in _≟_ a (elements s) 
+  a ∈? s = Utilities.ListProperties.eq2in _≟_ a (elements s)
+
+  infix 5 _∈'_
+  record _∈'_ (a : A) (s : FinSet A) : Set where
+     field FS∈ : a ∈ s
+
+  _∈'?_ : Decidable _∈'_
+  a ∈'? s = Relation.Nullary.Decidable.map (mk⇔ (λ x → record { FS∈ = x }) (λ where record { FS∈ = x } → x)) (a ∈? s)
+
+  ∈⇒∈' : ∀ {a s} → a ∈ s → a ∈' s
+  ∈⇒∈' h = record { FS∈ = h }
+
+  ∈'⇒∈ : ∀ {a s} → a ∈' s → a ∈ s
+  ∈'⇒∈ record { FS∈ = h } = h
+
+  ∈⇔∈' : ∀ {a s} → a ∈ s ⇔ a ∈' s
+  ∈⇔∈' = mk⇔ ∈⇒∈' ∈'⇒∈
 
   _∈ᵇ_ : A → FinSet A → Bool
   a ∈ᵇ s = ⌊ a ∈? s ⌋
@@ -67,6 +84,26 @@ module _ {A : Set} {{h : DecEq A}} where
   _≡ᵉ_ : FinSet A → FinSet A → Set
   s ≡ᵉ s' = ∀ a → a ∈ s ⇔ a ∈ s'
 
+  infix 4 _≡ᵉ'_
+  _≡ᵉ'_ : FinSet A → FinSet A → Set
+  s ≡ᵉ' s' = ∀ a → a ∈' s ⇔ a ∈' s'
+
+  ≡ᵉ'⇒≡ᵉ : ∀ {s s'} → s ≡ᵉ' s' → s ≡ᵉ s'
+  ≡ᵉ'⇒≡ᵉ {s} {s'} h a =
+    a ∈  s  ∼⟨ ∈⇔∈' ⟩
+    a ∈' s  ∼⟨ h a ⟩
+    a ∈' s' ∼⟨ P.SK-sym ∈⇔∈' ⟩
+    a ∈  s' ∎
+    where open P.EquationalReasoning
+
+  ≡ᵉ⇒≡ᵉ' : ∀ {s s'} → s ≡ᵉ s' → s ≡ᵉ' s'
+  ≡ᵉ⇒≡ᵉ' {s} {s'} h a =
+    a ∈' s  ∼⟨ P.SK-sym ∈⇔∈' ⟩
+    a ∈  s  ∼⟨ h a ⟩
+    a ∈  s' ∼⟨ ∈⇔∈' ⟩
+    a ∈' s' ∎
+    where open P.EquationalReasoning
+
   _⊆_ : FinSet A → FinSet A → Set
   s ⊆ s' = (elements s) Utilities.ListProperties.SubSetOf (elements s')
 
@@ -76,6 +113,21 @@ module _ {A : Set} {{h : DecEq A}} where
   _⊆ᵇ_ : FinSet A → FinSet A → Bool
   s ⊆ᵇ s' = ⌊ s ⊆? s' ⌋
 
+  _⊆'_ : FinSet A → FinSet A → Set
+  s ⊆' s' = All (λ e → e ∈' s') s
+
+  _⊆''_ : FinSet A → FinSet A → Set
+  s ⊆'' s' = ∀ {a} → a ∈' s → a ∈' s'
+
+  _⊆'?_ : Decidable _⊆'_
+  s ⊆'? s' = all? (λ e → e ∈'? s') s
+
+  ⊆⇒⊆' : ∀ {s s'} → s ⊆ s' → s ⊆' s'
+  ⊆⇒⊆' h = record { FSAll = Data.List.Relation.Unary.All.tabulate (∈⇒∈' ∘ h) }
+
+  ⊆'⇒⊆ : ∀ {s s'} → s ⊆' s' → s ⊆ s'
+  ⊆'⇒⊆ record { FSAll = h } = ∈'⇒∈ ∘ Data.List.Relation.Unary.All.lookup h
+
   _∪_ : FinSet A → FinSet A → FinSet A
   s ∪ s' = s FiniteSubset.∪ s'
 
@@ -90,9 +142,12 @@ module _ {A : Set} {{h : DecEq A}} {B : Set} {{_ : DecEq B}} where
   map : (A → B) → FinSet A → FinSet B
   map f (fs-nojunk els) = fromList (Data.List.map f els)
 
+  mapPartial : (A → Maybe B) → FinSet A → FinSet B
+  mapPartial f (fs-nojunk els) = fromList (Data.List.mapMaybe f els)
+
 module _ {A : Set} {{_ : DecEq A}} {p} {{M : CommutativeMonoid 0ℓ p}} where
   open CommutativeMonoid M
-  
+
   indexedSumL : (A → Carrier) → List A → Carrier
   indexedSumL f l = foldr (λ x → f x ∙_) ε l
 

src/Foreign/Convertible.agda

@@ -0,0 +1,19 @@
+module Foreign.Convertible where
+
+open import Prelude
+open import Foreign.Haskell.Coerce
+
+record Convertible (A B : Set) : Set where
+  field to   : A → B
+        from : B → A
+
+open Convertible ⦃...⦄ public
+
+Convertible-Refl : ∀ {A} → Convertible A A
+Convertible-Refl .to   = id
+Convertible-Refl .from = id
+
+instance
+  Coercible⇒Convertible : ∀ {A B} → ⦃ _ : Coercible A B ⦄ → Convertible A B
+  Coercible⇒Convertible .to   = coerce
+  Coercible⇒Convertible .from = coerce ⦃ TrustMe ⦄ -- coercibility is symmetric

src/Foreign/LedgerTypes.agda

@@ -0,0 +1,110 @@
+module Foreign.LedgerTypes where
+
+open import Prelude
+
+open import Foreign.Haskell
+open import Foreign.Haskell.Coerce
+
+data Empty : Set where
+
+{-# FOREIGN GHC data AgdaEmpty #-}
+{-# COMPILE GHC Empty = data AgdaEmpty () #-}
+
+HSMap : Set → Set → Set
+HSMap K V = List (Pair K V)
+
+Coin          = ℕ
+Addr          = ℕ -- just payment credential
+
+TxId          = ℕ
+Ix            = ℕ
+Epoch         = ℕ
+AuxiliaryData = ⊤
+Network       = ⊤
+
+TxIn          = Pair TxId Ix
+TxOut         = Pair Addr Coin
+UTxO          = HSMap TxIn TxOut
+
+{-# FOREIGN GHC
+  type Coin  = Integer
+  type Addr  = Integer
+
+  type TxId  = Integer
+  type Ix    = Integer
+  type TxIn  = (TxId, Ix)
+  type TxOut = (Addr, Coin)
+  type UTxO  = [(TxIn, TxOut)]
+#-}
+
+record TxBody : Set where
+  field txins    : List TxIn
+        txouts   : HSMap Ix TxOut
+        txfee    : Coin
+        txvldt   : Pair (Maybe ℕ) (Maybe ℕ)
+        --txwdrls  : Wdrl
+        --txup     : Maybe Update
+        --txADhash : Maybe ADHash
+        txsize   : ℕ
+        txid     : TxId
+
+{-# FOREIGN GHC
+  data TxBody = MkTxBody
+    { txins  :: [TxIn]
+    , txouts :: [(Ix, TxOut)]
+    , txfee  :: Coin
+    , txvldt :: (Maybe Integer, Maybe Integer)
+    , txsize :: Integer
+    , txid   :: TxId } deriving Show
+#-}
+{-# COMPILE GHC TxBody = data MAlonzo.Code.Foreign.LedgerTypes.TxBody (MkTxBody) #-}
+
+record TxWitnesses : Set where
+  field vkSigs  : List (Pair ℕ ℕ)
+        scripts : List Empty
+
+{-# FOREIGN GHC data TxWitnesses = MkTxWitnesses { vkSigs :: [(Integer, Integer)], scripts :: [AgdaEmpty] } #-}
+{-# COMPILE GHC TxWitnesses = data MAlonzo.Code.Foreign.LedgerTypes.TxWitnesses (MkTxWitnesses) #-}
+
+record Tx : Set where
+  field body : TxBody
+        wits : TxWitnesses
+        txAD : Maybe ⊤
+
+{-# FOREIGN GHC data Tx = MkTx { body :: TxBody, wits :: TxWitnesses, txAD :: Maybe () } #-}
+{-# COMPILE GHC Tx = data MAlonzo.Code.Foreign.LedgerTypes.Tx (MkTx) #-}
+
+record PParams : Set where
+  field a             : ℕ
+        b             : ℕ
+        maxBlockSize  : ℕ
+        maxTxSize     : ℕ
+        maxHeaderSize : ℕ
+        poolDeposit   : Coin
+        Emax          : Epoch
+
+{-# FOREIGN GHC
+  data PParams = MkPParams
+    { a :: Integer
+    , b :: Integer
+    , maxBlockSize :: Integer
+    , maxTxSize :: Integer
+    , maxHeaderSize :: Integer
+    , poolDeposit :: Integer
+    , emax :: Integer } deriving Show
+#-}
+{-# COMPILE GHC PParams = data MAlonzo.Code.Foreign.LedgerTypes.PParams (MkPParams) #-}
+
+record UTxOEnv : Set where
+  field slot    : ℕ
+        pparams : PParams
+
+{-# FOREIGN GHC data UTxOEnv = MkUTxOEnv { slot :: Integer, pparams :: PParams } deriving Show #-}
+{-# COMPILE GHC UTxOEnv = data MAlonzo.Code.Foreign.LedgerTypes.UTxOEnv (MkUTxOEnv) #-}
+
+record UTxOState : Set where
+  field utxo : UTxO
+        fees : Coin
+
+{-# FOREIGN GHC data UTxOState = MkUTxOState { utxo :: UTxO, fees :: Coin } deriving Show #-}
+{-# COMPILE GHC UTxOState = data MAlonzo.Code.Foreign.LedgerTypes.UTxOState (MkUTxOState) #-}