LedgerImplementation.lagda.md

source_branch	master
source_path	src/Test/LedgerImplementation.lagda.md

module Implementation where
  Network          = ℕ
  SlotsPerEpochᶜ   = 100
  ActiveSlotCoeff  = ℤ.1ℤ ℚ./ 20
  StabilityWindowᶜ = 10
  RandomnessStabilisationWindowᶜ = 2
  MaxLovelaceSupplyᶜ = 1000000000000000000
  Quorum           = 1
  NetworkId        = 0
  BlsKeyMaxAgeᶜ    = 20

  SKey = ℕ
  VKey = ℕ
  Sig  = ℕ
  Ser  = ℕ

  isKeyPair  = _≡_
  sign       = _+_

  _<ᵏʰ_ : ℕ → ℕ → Type
  _<ᵏʰ_ = _<_
  <ᵏʰ-isSTO = <-isStrictTotalOrder
  BlsVKey = ℕ
  BlsSig  = ℕ
  BlsPoP  = ℕ
  isValidPoP : BlsVKey → BlsPoP → Type
  isValidPoP = _≡_
  isSignedBy : BlsVKey → Ser → BlsSig → Type
  isSignedBy = λ vk m σ → vk + m ≡ σ
  isSignedByAggregate : List BlsVKey → Ser → BlsSig → Type
  isSignedByAggregate = λ vks m σ → foldr _+_ 0 vks + m ≡ σ

  Data         = D
  Dataʰ        = mkHashableSet D

  PlutusScript = ℕ × (List Data → Bool)
  ScriptHash = ℕ
  VRF = ℕ

  ExUnits      = ℕ × ℕ
  ExUnit-CommutativeMonoid =
    Conversion.fromBundle (commutativeMonoid +-0-commutativeMonoid +-0-commutativeMonoid)
  ≥ᵉ-Dec = _≡_ {A = ExUnits} ⁇² ∋ it
  _≥ᵉ_ = _≡_
  instance
    Show-ExUnits : Show ExUnits
    Show-ExUnits = Show-×

  CostModel    = ⊤ -- changed from ⊥
  Language     = ⊤
  LangDepView  = ⊤
  Prices       = ⊤

  TxId            = ℕ
  Ix              = ℕ
  AuxiliaryData   = ℕ
  DocHash         = ℕ
  tokenAlgebra    = Coin-TokenAlgebra
    where open import Ledger.Conway.Specification.TokenAlgebra.Coin ScriptHash
            using (Coin-TokenAlgebra)

SVGlobalConstants = GlobalConstants ∋ record {Implementation}
SVEpochStructure  = EpochStructure  ∋ ℕEpochStructure SVGlobalConstants
instance _ = SVEpochStructure

SVCrypto : CryptoStructure
SVCrypto = record
  { Implementation
  ; pkk = SVPKKScheme
  }
  where
  -- Dummy private key crypto scheme
  SVPKKScheme : PKKScheme
  SVPKKScheme = record
    { Implementation
    ; isSigned         = λ a b m → a + b ≡ m
    ; sign             = _+_
    ; isSigned-correct = λ where (sk , sk , refl) _ _ h → h
    }

SVScriptStructure : ScriptStructure
SVScriptStructure = record
  { p1s = P1ScriptStructure-HTL
  ; hashRespectsUnion = hashRespectsUnion
  ; ps = SVP2ScriptStructure
  }
  where

    instance Hashable-PlutusScript : Hashable Implementation.PlutusScript ℕ
             Hashable-PlutusScript = record { hash = λ x → proj₁ x }

    hashRespectsUnion : ∀ {A B ℍ}
      → Hashable A ℍ → Hashable B ℍ
      → Hashable (A ⊎ B) ℍ
    hashRespectsUnion ha hb = record { hash = λ { (inj₁ x) → Hashable.hash ha x ; (inj₂ y) → Hashable.hash hb y }}

    SVP2ScriptStructure : PlutusStructure
    SVP2ScriptStructure =  record
      { Implementation
      ; validPlutusScript = λ _ d _ (_ , script) → script d ≡ true
      }

SVGovParams : GovParams
SVGovParams = record
  { Implementation
  ; ppUpd = let open PParamsDiff in λ where
      .UpdateT                → ⊤
      .updateGroups           → λ _ → ∅
      .applyUpdate            → λ p _ → p
      .ppWF?                  → ⁇ yes λ _ → id
  }

SVGovStructure : GovStructure
SVGovStructure = record
  { Implementation
  ; epochStructure  = SVEpochStructure
  ; govParams       = SVGovParams
  ; cryptoStructure = SVCrypto
  ; globalConstants = SVGlobalConstants
  }
instance _ = SVGovStructure

open import Ledger.Conway.Specification.Gov.Actions it hiding (Vote; GovRole; VDeleg; Anchor)
open import Ledger.Conway.Conformance.Certs it hiding (StakePoolParams; DCert)

SVTransactionStructure : TransactionStructure
SVTransactionStructure = record
  { Implementation
  ; POSIXTimeRange = ⊤
  ; epochStructure  = SVEpochStructure
  ; globalConstants = SVGlobalConstants
  ; adHashingScheme = it
  ; cryptoStructure = SVCrypto
  ; govParams       = SVGovParams
  ; txidBytes       = id
  ; scriptStructure = SVScriptStructure
    -- This value is inconsequential while scriptIntegrityHash is set to
    -- nothing
  ; Hashable-ScriptIntegrity = record { hash = λ x → 0 }
  }

indexOfTxInImp : TxIn → ℙ TxIn → Maybe Ix
indexOfTxInImp x y = lookupᵐ? (fromListᵐ (setToList y)) (proj₁ x)