ValueSet

Value Set

{-# OPTIONS --safe --no-import-sorts #-}

open import Prelude using (Type)

module Ledger.Conway.Specification.TokenAlgebra.ValueSet (PolicyId AssetName : Type) where

open import Ledger.Prelude                         hiding (lookup ; update ; isMagma ; isEquivalence) renaming (TotalMap to _⇒_)
open _⇒_
open import Ledger.Conway.Specification.TokenAlgebra.Base PolicyId using (TokenAlgebra)

open import Algebra                                using (Op₂ ; IsSemigroup ; IsMonoid ; IsMagma ; IsCommutativeMonoid)
open import Algebra.Morphism                       using (IsMonoidHomomorphism ; IsMagmaHomomorphism)
open import Data.Nat.Properties                    using (+-comm ; +-assoc ; +-identityʳ ; +-0-commutativeMonoid)
open import Relation.Binary                        using (IsEquivalence)
open import Relation.Binary.Morphism               using (IsRelHomomorphism)
open import Relation.Binary.PropositionalEquality  using (module ≡-Reasoning)

import Relation.Binary.PropositionalEquality as ≡
import Relation.Binary.Core  as stdlib

Derived Types

(See Fig 3 of the Mary ledger specification.)

• AssetName is a byte string used to distinguish different assets with the same PolicyId.

• AssetId is a product type consisting of a PolicyId and an AssetName.

• AdaId is the Id for the asset Ada.

• Quantity is the type of amounts of assets.

In the formal ledger specification AssetId is sometimes viewed as a direct sum type, the inhabitants of which belong to either AdaIdType or the product PolicyId × AssetName; if we were adhering to that point of view, then we would have defined AssetId = AdaIdType ⊎ (PolicyId × AssetName).

Finally, we define a record type with a single inhabitant with which we may wish to represent the type of Ada (rather than viewing Ada as just another asset).

record AdaIdType : Type where
  instance constructor AdaId

Value Monoid Definition

An inhabitant of ‘Value‘ is a map denoting a finite collection of quantities of assets.

open Algebra.CommutativeMonoid renaming (_∙_ to _⋆_) hiding (refl ; sym ; trans)

AssetId  = PolicyId × AssetName
Quantity = ℕ

module _

  {X : ℙ AssetId}
  {⋁A : isMaximal X}
  ⦃ DecEq-PolicyId  : DecEq PolicyId ⦄
  ⦃ DecEq-AssetName : DecEq AssetName ⦄
  ⦃ DecEq-Tot : DecEq (AssetId ⇒ ℕ) ⦄
  (Dec-lookup≤ : ∀ {u v : AssetId ⇒ ℕ}
    → (∀ {a p q} → lookup u (a , p) ≤ lookup v (a , q)) ⁇)

  where
  open ≡-Reasoning
  open FunTot X ⋁A

  _⊕_ : Op₂ (AssetId ⇒ Quantity)
  u ⊕ v = Fun⇒TotalMap λ aa → (lookup u) aa + (lookup v) aa

  ⊕-lemma :  (u v : AssetId ⇒ Quantity){aa : AssetId}
             → lookup (u ⊕ v) aa ≡ lookup u aa + lookup v aa
  ⊕-lemma _ _ = lookup∘Fun⇒TotalMap-id

  zeroFun : AssetId → Quantity
  zeroFun = λ _ → 

  ι : AssetId ⇒ Quantity
  ι = Fun⇒TotalMap zeroFun

  lookupι≡0 :  ∀{a} → lookup ι a ≡ 
  lookupι≡0 = ∈-rel⇒lookup-≡ ι (∈-map′ ⋁A)

  _≋_ : stdlib.Rel (AssetId ⇒ Quantity) 0ℓ
  u ≋ v = ∀{aa} → (lookup u) aa ≡ (lookup v) aa

  ≋-isEquivalence : IsEquivalence {0ℓ} _≋_
  ≋-isEquivalence = record { refl = ≡.refl ; sym = λ x → ≡.sym x ; trans = λ x y → ≡.trans x y }

  ⊕-cong : Algebra.Congruent₂ _≋_ _⊕_
  ⊕-cong {x}{y}{u}{v} x≋y u≋v {a} = begin
    lookup (x ⊕ u) a         ≡⟨ ⊕-lemma x u ⟩
    lookup x a + lookup u a  ≡⟨ cong₂ _+_ x≋y u≋v ⟩
    lookup y a + lookup v a  ≡⟨ ≡.sym (⊕-lemma y v) ⟩
    lookup (y ⊕ v) a         ∎

  ⊕-comm : Algebra.Commutative _≋_ _⊕_
  ⊕-comm u v {aa} = begin
    lookup (u ⊕ v) aa          ≡⟨ ⊕-lemma u v ⟩
    lookup u aa + lookup v aa  ≡⟨ +-comm (lookup u aa) (lookup v aa) ⟩
    lookup v aa + lookup u aa  ≡⟨ ≡.sym (⊕-lemma v u) ⟩
    lookup (v ⊕ u) aa          ∎

  ⊕-assoc : Algebra.Associative _≋_ _⊕_
  ⊕-assoc x y z {a} = begin
    lookup ((x ⊕ y) ⊕ z) a                  ≡⟨ ⊕-lemma (x ⊕ y) z ⟩
    lookup (x ⊕ y) a + lookup z a           ≡⟨ cong (_+ lookup z a) (⊕-lemma x y) ⟩
    lookup x a + lookup y a + lookup z a    ≡⟨ +-assoc (lookup x a) (lookup y a) (lookup z a) ⟩
    lookup x a + (lookup y a + lookup z a)  ≡⟨ cong (lookup x a +_) (≡.sym (⊕-lemma y z)) ⟩
    lookup x a + lookup (y ⊕ z) a           ≡⟨ ≡.sym (⊕-lemma x (y ⊕ z)) ⟩
    lookup (x ⊕ (y ⊕ z)) a                  ∎

  ι-identity : Algebra.Identity _≋_ ι _⊕_
  ι-identity .proj₁ tm {aa} = begin
    lookup (ι ⊕ tm) aa          ≡⟨ ⊕-lemma ι tm ⟩
    lookup ι aa + lookup tm aa  ≡⟨ cong (_+ lookup tm aa) lookupι≡0 ⟩
    lookup tm aa                ∎
  ι-identity .proj₂ tm {aa} = begin
    lookup (tm ⊕ ι) aa          ≡⟨ ⊕-lemma tm ι ⟩
    lookup tm aa + lookup ι aa  ≡⟨ cong (lookup tm aa +_) lookupι≡0 ⟩
    lookup tm aa +             ≡⟨ +-identityʳ (lookup tm aa) ⟩
    lookup tm aa                ∎

  open IsSemigroup
  open IsMagma
  isSemigrp : IsSemigroup _≋_ _⊕_
  isSemigrp .isMagma .isEquivalence        = ≋-isEquivalence
  isSemigrp .isMagma .∙-cong {u}{v}{x}{y}  = ⊕-cong {u}{v}{x}{y}
  isSemigrp .assoc                         = ⊕-assoc

  open IsMonoid
  ≋-⊕-ι-isMonoid : IsMonoid _≋_ _⊕_ ι
  ≋-⊕-ι-isMonoid .isSemigroup  = isSemigrp
  ≋-⊕-ι-isMonoid .identity     = ι-identity

We are now in a position to define the commutative monoid.

  open IsCommutativeMonoid

  Vcm : Algebra.CommutativeMonoid 0ℓ 0ℓ
  Vcm .Carrier                        = AssetId ⇒ Quantity
  Vcm ._≈_                            = _≋_
  Vcm ._⋆_                            = _⊕_
  Vcm .ε                              = ι
  Vcm .isCommutativeMonoid .isMonoid  = ≋-⊕-ι-isMonoid
  Vcm .isCommutativeMonoid .comm      = ⊕-comm

  instance _ = Conversion.fromBundle Vcm

  Value-TokenAlgebra :
    (specialPolicy : PolicyId)
    (specialAsset : AssetName)
    (size : AssetId ⇒ Quantity → ℕ)
    --------------------------------------
    → TokenAlgebra
  Value-TokenAlgebra specialPolicy specialAsset size = record
    { coin                      = totalMap↠coin
    ; inject                    = coin↪totalMap
    ; policies                  = policies
    ; size                      = size
    ; _≤ᵗ_                      = leq
    ; coin∘inject≗id            = compose-to-id
    ; coinIsMonoidHomomorphism  = CoinMonHom
    ; Dec-≤ᵗ = λ {x}{y} → Dec-lookup≤ {x}{y}
    }
    where

    specId : AssetId
    specId = (specialPolicy , specialAsset)

    open Update

    totalMap↠coin : AssetId ⇒ Quantity → Coin
    totalMap↠coin tm = lookup tm specId

    coin↪totalMap : Coin → AssetId ⇒ Quantity
    coin↪totalMap c = update specId c ι

    policies : AssetId ⇒ Quantity → ℙ PolicyId
    policies tm = mapˢ proj₁ $ dom tm

    leq : AssetId ⇒ Quantity → AssetId ⇒ Quantity → Type
    leq u v = ∀ {a}{p}{q} → lookup u (a , p) ≤ lookup v (a , q)

    compose-to-id : totalMap↠coin ∘ coin↪totalMap ≗ id
    compose-to-id _ = lookup-update-id ι
      where open LookupUpdate {X = X} {specId} {a∈X = ⋁A}

    open Algebra.CommutativeMonoid Vcm                    using () renaming (rawMonoid to Vcm-mon)
    open Algebra.CommutativeMonoid +-0-commutativeMonoid  using () renaming (rawMonoid to ℕ-mon)
    open IsMonoidHomomorphism                             using (isMagmaHomomorphism ; ε-homo)
    open IsMagmaHomomorphism                              using (isRelHomomorphism ; homo)
    open IsRelHomomorphism                                using () renaming (cong to ⟦⟧-cong)

    CoinMonHom : IsMonoidHomomorphism Vcm-mon ℕ-mon totalMap↠coin
    CoinMonHom .isMagmaHomomorphism .isRelHomomorphism .⟦⟧-cong  = λ x → x
    CoinMonHom .isMagmaHomomorphism .homo                        = λ x y → ⊕-lemma x y
    CoinMonHom .ε-homo                                           = lookupι≡0