open import Ledger.Core.Foreign.ExternalFunctions

module Ledger.Dijkstra.Foreign.ExternalStructures (externalFunctions : ExternalFunctions) where

open import Data.Nat.Instances using (ℕ-≤-isDecTotalOrder)
open import Relation.Binary.Bundles using (DecTotalOrder)
open import Data.Product.Relation.Binary.Lex.NonStrict using (×-isDecTotalOrder)
open import Data.Sum.Relation.Binary.LeftOrder using (⊎-<-isDecTotalOrder)
open import Tactic.Derive.Show
import Data.Fin
import Data.List.Sort

open import Ledger.Prelude

open import Ledger.Core.Foreign.Epoch
open import Ledger.Core.Foreign.Address
open import Ledger.Dijkstra.Specification.Transaction public
open import Ledger.Core.Foreign.Crypto externalFunctions
open import Ledger.Dijkstra.Specification.Crypto using (LeiosCryptoStructure)
open import Ledger.Dijkstra.Foreign.Script externalFunctions public

open ExternalFunctions externalFunctions using (extIsSigned; extIsValidPoP)

instance
  _ = HSCryptoStructure
  _ = HSEpochStructure
  _ = HSGlobalConstants
  _ = HSScriptStructure

module Crypto = CryptoStructure it
open import Ledger.Dijkstra.Specification.PParams it it (GlobalConstants.Network it) it it hiding (Acnt; DrepThresholds; PoolThresholds)

HsGovParams : GovParams
HsGovParams = record
  { ppUpd = let open PParamsDiff in λ where
      .UpdateT      → PParamsUpdate
      .updateGroups → modifiedUpdateGroups
      .applyUpdate  → applyPParamsUpdate
      .ppWF? {u}    → ppWF u
  }
  where
    open PParamsUpdate
    -- FIXME Replace `trustMe` with an actual proof
    ppWF : (u : PParamsUpdate) →
      ((pp : PParams) →
      paramsWellFormed pp →
      paramsWellFormed (applyPParamsUpdate pp u))
      ⁇
    ppWF u with paramsUpdateWellFormed? u
    ... | yes _ = ⁇ (yes trustMe)
      where
        postulate
          trustMe :
            ((pp : PParams) →
            paramsWellFormed pp →
            paramsWellFormed (applyPParamsUpdate pp u))
    ... | no _  = ⁇ (no trustMe)
      where
        postulate
          trustMe :
            ¬((pp : PParams) →
            paramsWellFormed pp →
            paramsWellFormed (applyPParamsUpdate pp u))

open import Ledger.Conway.Specification.TokenAlgebra.Coin Crypto.ScriptHash
   using (Coin-TokenAlgebra)

instance
  HSLeiosCryptoStructure : LeiosCryptoStructure HSCryptoStructure
  HSLeiosCryptoStructure = record
    { BlsVKey              = ℕ
    ; BlsSig               = ℕ
    ; BlsPoP               = ℕ
    ; isValidPoP           = λ vk pop → extIsValidPoP vk pop ≡ true
    ; isSignedByAggregate  = λ vks m σ → extIsSigned (sum (setToList vks)) m σ ≡ true
    ; _≤ᵏʰ_                 = _≤_
    ; ≤ᵏʰ-isDTO             = ℕ-≤-isDecTotalOrder
    ; EBHash               = ℕ
    ; TxRefHash            = ℕ
    ; RBHeaderHash         = ℕ
    ; hashEBRefs           = λ refs → sum (map proj₁ refs)
    ; rbHeaderHashBytes    = id
    }

open LeiosCryptoStructure HSLeiosCryptoStructure

instance
  HSTransactionStructure : TransactionStructure
  HSTransactionStructure = record
    { TxId                      = ℕ
    ; Ix                        = ℕ
    ; AuxiliaryData             = ℕ
    ; epochStructure            = it
    ; globalConstants           = it
    ; cryptoStructure           = it
    ; leiosCryptoStructure      = HSLeiosCryptoStructure
    ; govParams                 = HsGovParams
    ; txidBytes                 = id
    ; scriptStructure           = it
    ; adHashingScheme           = isHashableSet-ℕ
    ; Hashable-ScriptIntegrity  = record { hash = λ x →  }
    ; tokenAlgebra              = Coin-TokenAlgebra
    }

open TransactionStructure HSTransactionStructure public
open import Ledger.Dijkstra.Specification.Certs govStructure public
-- open import Ledger.Dijkstra.Specification.Account govStructure public

open import Ledger.Dijkstra.Specification.Abstract it

instance
  HSAbstractFunctions : AbstractFunctions
  HSAbstractFunctions = record
    { txScriptFee    = λ tt y → 
    ; serializedSize = λ v → 
    ; indexOfImp  = record
      { indexOfDCert          =
          λ x xs → Data.Fin.toℕ <$> findIndexᵇ (_== x) xs
      ; indexOfRewardAddress  =
          λ x xs →
            Data.Fin.toℕ <$>
            findIndexᵇ
              (_== rewardAddressToSOP x)
              (Data.List.Sort.sort
                DecTotalOrder-RewardAddressSOP
                (setToList $ mapˢ rewardAddressToSOP $ dom xs)
              )

      ; indexOfTxIn           = λ x xs → Data.Fin.toℕ <$> findIndexᵇ (_== x) (setToList xs)
      ; indexOfPolicyId       = λ _ _ → nothing
      ; indexOfVote           = λ _ _ → nothing
      ; indexOfProposal       =
          λ x xs → Data.Fin.toℕ <$> findIndexᵇ (==-GovProposal x) xs
      ; indexOfGuard          =
          λ x xs → Data.Fin.toℕ <$> findIndexᵇ (_== x) xs
      }
    ; scriptSize = λ where
        (inj₁ x) → HSNativeScript.nsScriptSize x
        (inj₂ x) → HSPlutusScript.psScriptSize x
    ; valContext = λ _ _ → zero
    }
   where
    rewardAddressToSOP : RewardAddress → Network × (KeyHash ⊎ ScriptHash)
    rewardAddressToSOP ra@(RewardAddress.constructor n (KeyHashObj k)) =
      (n , inj₁ k)
    rewardAddressToSOP ra@(RewardAddress.constructor n (ScriptObj s)) =
      (n , inj₂ s)

    DecTotalOrder-RewardAddressSOP : DecTotalOrder _ _ _
    DecTotalOrder-RewardAddressSOP = record
      { isDecTotalOrder =
          ×-isDecTotalOrder
            ℕ-≤-isDecTotalOrder
            (⊎-<-isDecTotalOrder ℕ-≤-isDecTotalOrder ℕ-≤-isDecTotalOrder)
      }