{-# OPTIONS --rewriting #-} -- needed for UTxO hashing
module Main where

-------------------------
-- ** Linear bank ledgers
-------------------------

-- Shallow states, shallow predicates
-- ∙ S := K → Value
-- ∙ ⟦_⟧ := S → S
-- ∙ P := S → Set
-- ∙ Separation := IMPOSSIBLE
open import Shallow.Main

-- Deep states, shallow predicates
-- ∙ S := Map⟨ K ↦ Value ⟩
-- ∙ ⟦_⟧ := S → S
-- ∙ P := S → Set
-- ∙ Separation := _⊎_
open import Middle.Main

-- Deep states, deep predicates
-- ∙ S := Map⟨ K ↦ Value ⟩
-- ∙ ⟦_⟧ := S → S
-- ∙ P := Assertion
-- ∙ Separation := _⊎_
open import Deep.Main

-- <Deep> + shallow embedding of Hoare triples
--   ⋮
--   ∙ {P}l{Q} = ∀ s. P(s) → Q(⟦l⟧s)
open import ShallowHoare.Main

-- Simplest possible design: allowing negative values without explicit errors.
-- ∙ S := K → ℤ
-- ∙ ⟦_⟧ := S → S
-- ∙ P := S → Set
-- ∙ Separation := _◇_
open import ValueSepInt.Main

-- Monoidal separatation on values instead of participants.
-- ∙ S := Map⟨ K ↦ Value ⟩
-- ∙ ⟦_⟧ := S → Maybe S
-- ∙ P := S → Set
-- ∙ Separation := _◇_
open import ValueSep.Main

-- Simplified version of <ValueSep>.
-- ∙ S := K → ℕ
-- ∙ ⟦_⟧ := S → Maybe S
-- ∙ P := S → Set
-- ∙ Separation := _◇_
open import ValueSepSimple.Main

-- <ValueSepSimple>, but with exact maps-to/↦ predicate.
-- ∙ S := K → ℕ
-- ∙ ⟦_⟧ := S → Maybe S
-- ∙ P := S → Set
-- ∙ Separation := _◇_
open import ValueSepExact.Main

-----------------------------
-- ** UTxO blockchain ledgers
-----------------------------

-- Initial prototype for extending to the UTxO case.
-- ∙ S := Set⟨ UTXO ⟩
-- ∙ ⟦_⟧ := S → S
-- ∙ P := S → Set
-- ∙ Separation := _⊎_
open import UTxO.Main

-- <UTxO> variant that explicitly errors/invalidity.
-- ∙ S := Map⟨ TxOutputRef ↦ TxOutput ⟩
-- ∙ ⟦_⟧ := S → Maybe S
-- ∙ P := S → Set
-- ∙ Separation := _⊎_
open import UTxOErr.Main

-- Value-separated Abstract UTxO (AUTxO).
-- ∙ S := Bag⟨ Address × Value ⟩
-- ∙ ⟦_⟧ := S → Maybe S
-- ∙ P := S → Set
-- ∙ Separation := _◇_
open import ValueSepUTxO.Main

-- Sound abstraction for UTxO↔AUTxO.
open import ConcreteToAbstract

------------------------------
-- ** EUTxO blockchain ledgers
------------------------------

-- Extended UTXO (EUTXO) with explicit errors.
-- ∙ S := Map⟨ TxOutputRef ↦ TxOutput ⟩
-- ∙ ⟦_⟧ := S → Maybe S
-- ∙ P := S → Set
-- ∙ Separation := _⊎_
open import EUTxOErr.Main

-- Value-separated Abstract EUTxO (AEUTxO).
-- ∙ S := Bag⟨ Address × Value ⟩
-- ∙ ⟦_⟧ := S → Maybe S
-- ∙ P := S → Set
-- ∙ Separation := _◇_
-- open import ValueSepEUTxO.Main

-- Sound abstraction for EUTxO↔AEUTxO.
-- open import ConcreteToAbstractEutxo