{-# OPTIONS --safe #-}

open import Algebra
open import Data.Nat.Properties using (+-0-monoid)

open import Ledger.Prelude; open Equivalence
open import Ledger.Transaction
open import Ledger.Abstract
open import Ledger.TokenAlgebra 
open import Ledger.TokenAlgebra.ValueSet


module ScriptVerification.StructuredContracts
  (txs : _) (open TransactionStructure txs)
  (abs : AbstractFunctions txs) (open AbstractFunctions abs)
  where

open import Ledger.Ledger txs abs
open import Ledger.ScriptValidation txs abs
open import Ledger.Utxo txs abs


SSRel : Type → Type → Type → Type₁
SSRel Env State Input = Env → State → Input → State → Type

record StrucSimulation S I (_⊢_⇀⦇_,STRUC⦈_ : SSRel ⊤ S I) : Type₁ where
  field
    πˢ : LState → Maybe S
    πⁱ : TxInfo → I
    -- here, add optional extra assumptions about ledger state, env, and transaction that may be too difficult to prove without reasoning about complete ledger traces
    -- e.g. transaction does not re-add a UTxO entry it spends
    -- e.g. current Slot is after the validity interval of some previous transaction
    extraAssmp : LEnv → LState → Tx → Type 

  _~ˢ_ : LState → S → Type -- R
  u ~ˢ s = πˢ u ≡ just s

    -- only for PlutusV3
  _~ᵉ_ : LEnv × Tx × LState → ⊤ × I → Type
  _~ᵉ_ = λ (le , tx , u) (tt , i) → πⁱ (txInfo PlutusV3 (le .LEnv.pparams) (u .LState.utxoSt .UTxOState.utxo) tx) ≡ i

  field
    simulates : ∀ Γ s u tx i′ u′ → extraAssmp Γ u tx →
      ∙ Γ ⊢ u ⇀⦇ tx ,LEDGER⦈ u′
      ∙ (Γ , tx , u) ~ᵉ (tt , i′)
      ∙ u ~ˢ s
      ────────────────────────────────
        ∃[ s′ ] u′ ~ˢ s′
               × tt ⊢ s ⇀⦇ i′ ,STRUC⦈ s′