{-# LANGUAGE DuplicateRecordFields #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE NoPolyKinds #-}
{-# OPTIONS_GHC -fno-specialize #-}
{-# OPTIONS_GHC -fplugin-opt Plinth.Plugin:conservative-optimisation #-}
{-# OPTIONS_GHC -fplugin-opt Plinth.Plugin:defer-errors #-}
{-# OPTIONS_GHC -fplugin-opt Plinth.Plugin:optimize #-}
{-# OPTIONS_GHC -fplugin-opt Plinth.Plugin:target-version=1.1.0 #-}

module Hydra.Contract.Head where

import PlutusTx.Prelude

import GHC.ByteOrder (ByteOrder (BigEndian))
import Hydra.Cardano.Api (
  PlutusScript,
  pattern PlutusScriptSerialised,
 )
import Hydra.Contract.CRS (CRSDatum, checkMembershipPairing)
import Hydra.Contract.Commit (Commit)
import Hydra.Contract.HeadError (HeadError (..), errorCode)
import Hydra.Contract.HeadState (
  CloseRedeemer (..),
  ClosedDatum (..),
  ContestRedeemer (..),
  DecrementRedeemer (..),
  FanoutProgressDatum (..),
  Hash,
  IncrementRedeemer (..),
  Input (..),
  OpenDatum (..),
  Signature,
  SnapshotNumber,
  SnapshotVersion,
  State (..),
  progressFromClosed,
 )
import Hydra.Contract.KZGTrustedSetup qualified as KZG
import Hydra.Contract.Util (hasST, hashPreSerializedCommits, hashTxOuts, mustBurnAllHeadTokens, mustNotMintOrBurn, mustPreserveHeadValue)
import Hydra.Data.ContestationPeriod (ContestationPeriod, addContestationPeriod, milliseconds)
import Hydra.Data.DepositPeriod (DepositPeriod)
import Hydra.Data.Party (Party (vkey))
import Hydra.Plutus.Extras (ValidatorType, wrapValidator)
import PlutusCore.Version (plcVersion110)
import PlutusLedgerApi.Common (serialiseCompiledCode)
import PlutusLedgerApi.V1.Time (fromMilliSeconds)
import PlutusLedgerApi.V1.Value (adaSymbol, adaToken, singleton)
import PlutusLedgerApi.V3 (
  Address (..),
  Credential (..),
  CurrencySymbol,
  Datum (..),
  Extended (Finite),
  Interval (..),
  LowerBound (LowerBound),
  OutputDatum (..),
  POSIXTime,
  PubKeyHash (getPubKeyHash),
  ScriptContext (..),
  TokenName (..),
  TxId (getTxId),
  TxInInfo (..),
  TxInfo (..),
  TxOut (..),
  TxOutRef (txOutRefId, txOutRefIdx),
  UpperBound (..),
  Value (Value),
  mintValueBurned,
 )
import PlutusLedgerApi.V3.Contexts (findOwnInput)
import PlutusTx (CompiledCode)
import PlutusTx qualified
import PlutusTx.AssocMap qualified as AssocMap
import PlutusTx.Builtins qualified as Builtins
import PlutusTx.Foldable qualified as F
import PlutusTx.List qualified as L

type DatumType = State
type RedeemerType = Input

--------------------------------------------------------------------------------
-- Validators
--------------------------------------------------------------------------------

{-# INLINEABLE headValidator #-}
headValidator ::
  BuiltinByteString ->
  State ->
  Input ->
  ScriptContext ->
  Bool
headValidator :: BuiltinByteString -> DatumType -> Input -> ScriptContext -> Bool
headValidator BuiltinByteString
crsDatumHash DatumType
oldState Input
input ScriptContext
ctx =
  case (DatumType
oldState, Input
input) of
    (Open OpenDatum
openDatum, Increment IncrementRedeemer
redeemer) ->
      ScriptContext -> OpenDatum -> IncrementRedeemer -> Bool
checkIncrement ScriptContext
ctx OpenDatum
openDatum IncrementRedeemer
redeemer
    (Open OpenDatum
openDatum, Decrement DecrementRedeemer
redeemer) ->
      ScriptContext -> OpenDatum -> DecrementRedeemer -> Bool
checkDecrement ScriptContext
ctx OpenDatum
openDatum DecrementRedeemer
redeemer
    (Open OpenDatum
openDatum, Close CloseRedeemer
redeemer) ->
      ScriptContext -> OpenDatum -> CloseRedeemer -> Bool
checkClose ScriptContext
ctx OpenDatum
openDatum CloseRedeemer
redeemer
    (Closed ClosedDatum
closedDatum, Contest ContestRedeemer
redeemer) ->
      ScriptContext -> ClosedDatum -> ContestRedeemer -> Bool
checkContest ScriptContext
ctx ClosedDatum
closedDatum ContestRedeemer
redeemer
    (Closed ClosedDatum
closedDatum, Fanout{SnapshotVersion
numberOfFanoutOutputs :: SnapshotVersion
$sel:numberOfFanoutOutputs:Increment :: Input -> SnapshotVersion
numberOfFanoutOutputs, BuiltinBLS12_381_G1_Element
proof :: BuiltinBLS12_381_G1_Element
$sel:proof:Increment :: Input -> BuiltinBLS12_381_G1_Element
proof, TxOutRef
crsRef :: TxOutRef
$sel:crsRef:Increment :: Input -> TxOutRef
crsRef}) ->
      BuiltinByteString
-> ScriptContext
-> ClosedDatum
-> SnapshotVersion
-> BuiltinBLS12_381_G1_Element
-> TxOutRef
-> Bool
headIsFinalizedWith BuiltinByteString
crsDatumHash ScriptContext
ctx ClosedDatum
closedDatum SnapshotVersion
numberOfFanoutOutputs BuiltinBLS12_381_G1_Element
proof TxOutRef
crsRef
    (Closed ClosedDatum
closedDatum, PartialFanout{SnapshotVersion
numberOfPartialOutputs :: SnapshotVersion
$sel:numberOfPartialOutputs:Increment :: Input -> SnapshotVersion
numberOfPartialOutputs, TxOutRef
$sel:crsRef:Increment :: Input -> TxOutRef
crsRef :: TxOutRef
crsRef}) ->
      BuiltinByteString
-> ScriptContext
-> FanoutProgressDatum
-> SnapshotVersion
-> TxOutRef
-> Bool
checkPartialFanout BuiltinByteString
crsDatumHash ScriptContext
ctx (ClosedDatum -> FanoutProgressDatum
progressFromClosed ClosedDatum
closedDatum) SnapshotVersion
numberOfPartialOutputs TxOutRef
crsRef
    (FanoutProgress FanoutProgressDatum
progressDatum, PartialFanout{SnapshotVersion
$sel:numberOfPartialOutputs:Increment :: Input -> SnapshotVersion
numberOfPartialOutputs :: SnapshotVersion
numberOfPartialOutputs, TxOutRef
$sel:crsRef:Increment :: Input -> TxOutRef
crsRef :: TxOutRef
crsRef}) ->
      BuiltinByteString
-> ScriptContext
-> FanoutProgressDatum
-> SnapshotVersion
-> TxOutRef
-> Bool
checkPartialFanout BuiltinByteString
crsDatumHash ScriptContext
ctx FanoutProgressDatum
progressDatum SnapshotVersion
numberOfPartialOutputs TxOutRef
crsRef
    (FanoutProgress FanoutProgressDatum
progressDatum, FinalPartialFanout{SnapshotVersion
$sel:numberOfPartialOutputs:Increment :: Input -> SnapshotVersion
numberOfPartialOutputs :: SnapshotVersion
numberOfPartialOutputs, BuiltinBLS12_381_G1_Element
$sel:proof:Increment :: Input -> BuiltinBLS12_381_G1_Element
proof :: BuiltinBLS12_381_G1_Element
proof, TxOutRef
$sel:crsRef:Increment :: Input -> TxOutRef
crsRef :: TxOutRef
crsRef}) ->
      BuiltinByteString
-> ScriptContext
-> FanoutProgressDatum
-> SnapshotVersion
-> BuiltinBLS12_381_G1_Element
-> TxOutRef
-> Bool
checkFinalPartialFanout BuiltinByteString
crsDatumHash ScriptContext
ctx FanoutProgressDatum
progressDatum SnapshotVersion
numberOfPartialOutputs BuiltinBLS12_381_G1_Element
proof TxOutRef
crsRef
    (DatumType, Input)
_ ->
      BuiltinString -> Bool
forall a. BuiltinString -> a
traceError $(errorCode InvalidHeadStateTransition)

-- | Verify a increment transaction.
checkIncrement ::
  ScriptContext ->
  -- | Open state before the increment
  OpenDatum ->
  IncrementRedeemer ->
  Bool
checkIncrement :: ScriptContext -> OpenDatum -> IncrementRedeemer -> Bool
checkIncrement ctx :: ScriptContext
ctx@ScriptContext{scriptContextTxInfo :: ScriptContext -> TxInfo
scriptContextTxInfo = TxInfo
txInfo} OpenDatum
openBefore IncrementRedeemer
redeemer =
  TxInfo -> Bool
mustNotMintOrBurn TxInfo
txInfo
    Bool -> Bool -> Bool
&& ([Party], [Party])
-> (ContestationPeriod, ContestationPeriod)
-> (CurrencySymbol, CurrencySymbol)
-> (DepositPeriod, DepositPeriod)
-> Bool
mustNotChangeParameters ([Party]
prevParties, [Party]
nextParties) (ContestationPeriod
prevCperiod, ContestationPeriod
nextCperiod) (CurrencySymbol
prevHeadId, CurrencySymbol
nextHeadId) (DepositPeriod
prevDepositPeriod, DepositPeriod
nextDepositPeriod)
    Bool -> Bool -> Bool
&& Bool
mustIncreaseVersion
    Bool -> Bool -> Bool
&& Bool
mustPreserveValue
    Bool -> Bool -> Bool
&& ScriptContext -> CurrencySymbol -> Bool
mustBeSignedByParticipant ScriptContext
ctx CurrencySymbol
prevHeadId
    Bool -> Bool -> Bool
&& Bool
checkSnapshotSignature
    Bool -> Bool -> Bool
&& Bool
claimedDepositIsSpent
    Bool -> Bool -> Bool
&& Bool
mustClaimFirstDepositOutput
    Bool -> Bool -> Bool
&& Bool
mustNotSpendOtherScripts
    Bool -> Bool -> Bool
&& SnapshotVersion -> SnapshotVersion -> Bool
mustPreserveHeadAdaOverhead SnapshotVersion
prevHeadAdaOverhead SnapshotVersion
nextHeadAdaOverhead
 where
  inputs :: [TxInInfo]
inputs = TxInfo -> [TxInInfo]
txInfoInputs TxInfo
txInfo

  headTxIn :: TxInInfo
headTxIn =
    case (TxInInfo -> Bool) -> [TxInInfo] -> Maybe TxInInfo
forall a. (a -> Bool) -> [a] -> Maybe a
L.find (CurrencySymbol -> Value -> Bool
hasST CurrencySymbol
prevHeadId (Value -> Bool) -> (TxInInfo -> Value) -> TxInInfo -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TxOut -> Value
txOutValue (TxOut -> Value) -> (TxInInfo -> TxOut) -> TxInInfo -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TxInInfo -> TxOut
txInInfoResolved) [TxInInfo]
inputs of
      Maybe TxInInfo
Nothing -> BuiltinString -> TxInInfo
forall a. BuiltinString -> a
traceError $(errorCode HeadInputNotFound)
      Just TxInInfo
i -> TxInInfo
i

  headInValue :: Value
headInValue = TxOut -> Value
txOutValue (TxInInfo -> TxOut
txInInfoResolved TxInInfo
headTxIn)
  headOutValue :: Value
headOutValue = TxOut -> Value
txOutValue (TxOut -> Value) -> TxOut -> Value
forall a b. (a -> b) -> a -> b
$ [TxOut] -> TxOut
forall a. [a] -> a
L.head ([TxOut] -> TxOut) -> [TxOut] -> TxOut
forall a b. (a -> b) -> a -> b
$ TxInfo -> [TxOut]
txInfoOutputs TxInfo
txInfo

  claimedDepositValue :: Value
claimedDepositValue = TxOut -> Value
txOutValue TxOut
claimedDeposit

  IncrementRedeemer{[BuiltinByteString]
signature :: [BuiltinByteString]
$sel:signature:IncrementRedeemer :: IncrementRedeemer -> [BuiltinByteString]
signature, SnapshotVersion
snapshotNumber :: SnapshotVersion
$sel:snapshotNumber:IncrementRedeemer :: IncrementRedeemer -> SnapshotVersion
snapshotNumber, TxOutRef
increment :: TxOutRef
$sel:increment:IncrementRedeemer :: IncrementRedeemer -> TxOutRef
increment, BuiltinByteString
decommitOutputsHash :: BuiltinByteString
$sel:decommitOutputsHash:IncrementRedeemer :: IncrementRedeemer -> BuiltinByteString
decommitOutputsHash} = IncrementRedeemer
redeemer

  claimedDepositIsSpent :: Bool
claimedDepositIsSpent =
    BuiltinString -> Bool -> Bool
traceIfFalse $(errorCode DepositNotSpent) (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$
      TxOutRef
increment TxOutRef -> [TxOutRef] -> Bool
forall a. Eq a => a -> [a] -> Bool
`L.elem` (TxInInfo -> TxOutRef
txInInfoOutRef (TxInInfo -> TxOutRef) -> [TxInInfo] -> [TxOutRef]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TxInfo -> [TxInInfo]
txInfoInputs TxInfo
txInfo)

  -- A deposit is the first output of its transaction. This is a protocol-wide
  -- invariant, not a rule local to this validator: 'Hydra.Tx.Deposit.depositTx'
  -- builds the deposit there, 'Hydra.Tx.Deposit.observeDepositTx' refuses to
  -- observe one anywhere else, 'Hydra.Tx.Recover.recoverTx' spends
  -- @TxIn depositTxId (TxIx 0)@, and the off-chain protocol identifies a deposit
  -- by transaction id alone throughout ('pendingDeposits', 'ReqSn', 'IncrementTx').
  --
  -- It is load-bearing here because 'commitOutputsHash' binds the deposit by
  -- transaction id: without this check, sibling outputs of the same transaction
  -- would be interchangeable, since a second output carrying a copied datum but
  -- less value hashes into the same signed message. Relaxing this — to allow
  -- deposits at other indices, or several per transaction — therefore requires
  -- binding the output index into the signed message first.
  mustClaimFirstDepositOutput :: Bool
mustClaimFirstDepositOutput =
    BuiltinString -> Bool -> Bool
traceIfFalse $(errorCode DepositNotFirstOutput) (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$
      TxOutRef -> SnapshotVersion
txOutRefIdx TxOutRef
increment SnapshotVersion -> SnapshotVersion -> Bool
forall a. Eq a => a -> a -> Bool
== SnapshotVersion
0

  -- The head input and the claimed deposit are the only script inputs an
  -- increment needs.
  --
  -- 'mustPreserveValue' is an equality, so it already stops an extra input's value
  -- being pushed INTO the head. What it cannot see is that value being routed OUT:
  -- the head output stays correct while the extra input is spent to wherever the
  -- transaction author likes. For a second deposit that is theft of a pending
  -- commit, otherwise caught only by the deposit validator's claim binding (D09)
  -- and single-recover rule (D10). This check is an independent barrier that does
  -- not rely on either, and extends to any other script.
  --
  -- Pub-key inputs are unrestricted, so fees and collateral are unaffected.
  mustNotSpendOtherScripts :: Bool
mustNotSpendOtherScripts =
    BuiltinString -> Bool -> Bool
traceIfFalse $(errorCode MustNotSpendOtherScripts) (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$
      (TxInInfo -> Bool) -> [TxInInfo] -> Bool
forall a. (a -> Bool) -> [a] -> Bool
L.all TxInInfo -> Bool
isHeadOrClaimedDeposit [TxInInfo]
inputs
   where
    isHeadOrClaimedDeposit :: TxInInfo -> Bool
isHeadOrClaimedDeposit TxInInfo
i =
      TxInInfo -> TxOutRef
txInInfoOutRef TxInInfo
i TxOutRef -> TxOutRef -> Bool
forall a. Eq a => a -> a -> Bool
== TxInInfo -> TxOutRef
txInInfoOutRef TxInInfo
headTxIn
        Bool -> Bool -> Bool
|| TxInInfo -> TxOutRef
txInInfoOutRef TxInInfo
i TxOutRef -> TxOutRef -> Bool
forall a. Eq a => a -> a -> Bool
== TxOutRef
increment
        Bool -> Bool -> Bool
|| Bool -> Bool
not (TxOut -> Bool
isScriptInput (TxInInfo -> TxOut
txInInfoResolved TxInInfo
i))

    isScriptInput :: TxOut -> Bool
isScriptInput TxOut
txOut =
      case Address -> Credential
addressCredential (TxOut -> Address
txOutAddress TxOut
txOut) of
        ScriptCredential ScriptHash
_ -> Bool
True
        PubKeyCredential PubKeyHash
_ -> Bool
False

  checkSnapshotSignature :: Bool
checkSnapshotSignature =
    [Party]
-> (CurrencySymbol, SnapshotVersion, SnapshotVersion,
    BuiltinByteString, BuiltinByteString, BuiltinByteString)
-> [BuiltinByteString]
-> Bool
verifySnapshotSignature [Party]
nextParties (CurrencySymbol
nextHeadId, SnapshotVersion
prevVersion, SnapshotVersion
snapshotNumber, BuiltinByteString
nextAccumulatorHash, BuiltinByteString
decommitOutputsHash, BuiltinByteString
commitOutputsHash) [BuiltinByteString]
signature

  -- Bind the exact committed deposit into the multi-signature: recompute the
  -- commit-outputs hash from the CLAIMED deposit input's own datum AND the id of
  -- the transaction that created it, so claiming a different deposit than the one
  -- parties approved changes the signed message and fails signature verification.
  --
  -- Hashing the deposit's content alone is not enough. A deposit datum is
  -- unauthenticated data that anyone can copy, and nothing forces a deposit to
  -- hold the value its commits describe, so a content-identical look-alike
  -- deposit hashes the same while carrying less value. Claiming it under a
  -- signature the parties gave for the real deposit would credit the full
  -- committed UTxO on L2 against whatever the look-alike actually paid into the
  -- head. Off-chain (see 'Hydra.Tx.Snapshot') the same hash is built from the
  -- committed UTxO and the deposit transaction id the parties agreed on.
  commitOutputsHash :: BuiltinByteString
commitOutputsHash =
    BuiltinByteString -> BuiltinByteString
sha2_256 (BuiltinByteString -> BuiltinByteString)
-> BuiltinByteString -> BuiltinByteString
forall a b. (a -> b) -> a -> b
$
      [Commit] -> BuiltinByteString
hashPreSerializedCommits [Commit]
claimedDepositCommits
        BuiltinByteString -> BuiltinByteString -> BuiltinByteString
forall a. Semigroup a => a -> a -> a
<> TxId -> BuiltinByteString
getTxId (TxOutRef -> TxId
txOutRefId TxOutRef
increment)

  claimedDeposit :: TxOut
claimedDeposit =
    case (TxInInfo -> Bool) -> [TxInInfo] -> Maybe TxInInfo
forall a. (a -> Bool) -> [a] -> Maybe a
L.find (\TxInInfo
i -> TxInInfo -> TxOutRef
txInInfoOutRef TxInInfo
i TxOutRef -> TxOutRef -> Bool
forall a. Eq a => a -> a -> Bool
== TxOutRef
increment) [TxInInfo]
inputs of
      Maybe TxInInfo
Nothing -> BuiltinString -> TxOut
forall a. BuiltinString -> a
traceError $(errorCode DepositInputNotFound)
      Just TxInInfo{TxOut
txInInfoResolved :: TxInInfo -> TxOut
txInInfoResolved :: TxOut
txInInfoResolved} -> TxOut
txInInfoResolved

  claimedDepositCommits :: [Commit]
claimedDepositCommits =
    case forall a. FromData a => BuiltinData -> Maybe a
fromBuiltinData @(CurrencySymbol, POSIXTime, [Commit]) (BuiltinData -> Maybe (CurrencySymbol, POSIXTime, [Commit]))
-> BuiltinData -> Maybe (CurrencySymbol, POSIXTime, [Commit])
forall a b. (a -> b) -> a -> b
$ Datum -> BuiltinData
getDatum (TxOut -> Datum
getTxOutDatum TxOut
claimedDeposit) of
      Just (CurrencySymbol
_, POSIXTime
_, [Commit]
commits) -> [Commit]
commits
      Maybe (CurrencySymbol, POSIXTime, [Commit])
Nothing -> BuiltinString -> [Commit]
forall a. BuiltinString -> a
traceError $(errorCode DepositDatumInvalid)

  mustIncreaseVersion :: Bool
mustIncreaseVersion =
    BuiltinString -> Bool -> Bool
traceIfFalse $(errorCode VersionNotIncremented) (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$
      SnapshotVersion
nextVersion SnapshotVersion -> SnapshotVersion -> Bool
forall a. Eq a => a -> a -> Bool
== SnapshotVersion
prevVersion SnapshotVersion -> SnapshotVersion -> SnapshotVersion
forall a. AdditiveSemigroup a => a -> a -> a
+ SnapshotVersion
1

  -- The head grows by exactly the claimed deposit, so no other input can push
  -- value into it: an unrelated script UTxO would otherwise over-fund the head and
  -- leave (partial) fanout's strict conservation unsatisfiable.
  --
  -- TODO: This is not as flexible as it could be and rejects deposits
  -- that are smaller than what the deposit output's min utxo value is.
  -- For example: a 1 ADA utxo can be deposited, but the deposit tx's
  -- output will require ~1.5 ADA because of the inline datum on it. An
  -- increment of that deposit will fail because the sum here is not
  -- exact.
  mustPreserveValue :: Bool
mustPreserveValue =
    BuiltinString -> Bool -> Bool
traceIfFalse $(errorCode HeadValueIsNotPreserved) (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$
      Value
headInValue Value -> Value -> Value
forall a. Semigroup a => a -> a -> a
<> Value
claimedDepositValue Value -> Value -> Bool
forall a. Eq a => a -> a -> Bool
== Value
headOutValue

  OpenDatum
    { $sel:parties:OpenDatum :: OpenDatum -> [Party]
parties = [Party]
prevParties
    , $sel:contestationPeriod:OpenDatum :: OpenDatum -> ContestationPeriod
contestationPeriod = ContestationPeriod
prevCperiod
    , $sel:depositPeriod:OpenDatum :: OpenDatum -> DepositPeriod
depositPeriod = DepositPeriod
prevDepositPeriod
    , $sel:headId:OpenDatum :: OpenDatum -> CurrencySymbol
headId = CurrencySymbol
prevHeadId
    , $sel:version:OpenDatum :: OpenDatum -> SnapshotVersion
version = SnapshotVersion
prevVersion
    , $sel:headAdaOverhead:OpenDatum :: OpenDatum -> SnapshotVersion
headAdaOverhead = SnapshotVersion
prevHeadAdaOverhead
    } = OpenDatum
openBefore

  OpenDatum
    { $sel:parties:OpenDatum :: OpenDatum -> [Party]
parties = [Party]
nextParties
    , $sel:contestationPeriod:OpenDatum :: OpenDatum -> ContestationPeriod
contestationPeriod = ContestationPeriod
nextCperiod
    , $sel:depositPeriod:OpenDatum :: OpenDatum -> DepositPeriod
depositPeriod = DepositPeriod
nextDepositPeriod
    , $sel:headId:OpenDatum :: OpenDatum -> CurrencySymbol
headId = CurrencySymbol
nextHeadId
    , $sel:version:OpenDatum :: OpenDatum -> SnapshotVersion
version = SnapshotVersion
nextVersion
    , $sel:accumulatorHash:OpenDatum :: OpenDatum -> BuiltinByteString
accumulatorHash = BuiltinByteString
nextAccumulatorHash
    , $sel:headAdaOverhead:OpenDatum :: OpenDatum -> SnapshotVersion
headAdaOverhead = SnapshotVersion
nextHeadAdaOverhead
    } = ScriptContext -> OpenDatum
decodeHeadOutputOpenDatum ScriptContext
ctx
{-# INLINEABLE checkIncrement #-}

-- | Verify a decrement transaction.
checkDecrement ::
  ScriptContext ->
  -- | Open state before the decrement
  OpenDatum ->
  DecrementRedeemer ->
  Bool
checkDecrement :: ScriptContext -> OpenDatum -> DecrementRedeemer -> Bool
checkDecrement ScriptContext
ctx OpenDatum
openBefore DecrementRedeemer
redeemer =
  TxInfo -> Bool
mustNotMintOrBurn TxInfo
txInfo
    Bool -> Bool -> Bool
&& ([Party], [Party])
-> (ContestationPeriod, ContestationPeriod)
-> (CurrencySymbol, CurrencySymbol)
-> (DepositPeriod, DepositPeriod)
-> Bool
mustNotChangeParameters ([Party]
prevParties, [Party]
nextParties) (ContestationPeriod
prevCperiod, ContestationPeriod
nextCperiod) (CurrencySymbol
prevHeadId, CurrencySymbol
nextHeadId) (DepositPeriod
prevDepositPeriod, DepositPeriod
nextDepositPeriod)
    Bool -> Bool -> Bool
&& Bool
mustIncreaseVersion
    Bool -> Bool -> Bool
&& Bool
mustHaveDecommitOutputs
    Bool -> Bool -> Bool
&& Bool
checkSnapshotSignature
    Bool -> Bool -> Bool
&& Bool
mustDecreaseValue
    Bool -> Bool -> Bool
&& ScriptContext -> CurrencySymbol -> Bool
mustBeSignedByParticipant ScriptContext
ctx CurrencySymbol
prevHeadId
    Bool -> Bool -> Bool
&& SnapshotVersion -> SnapshotVersion -> Bool
mustPreserveHeadAdaOverhead SnapshotVersion
prevHeadAdaOverhead SnapshotVersion
nextHeadAdaOverhead
 where
  checkSnapshotSignature :: Bool
checkSnapshotSignature =
    [Party]
-> (CurrencySymbol, SnapshotVersion, SnapshotVersion,
    BuiltinByteString, BuiltinByteString, BuiltinByteString)
-> [BuiltinByteString]
-> Bool
verifySnapshotSignature [Party]
nextParties (CurrencySymbol
nextHeadId, SnapshotVersion
prevVersion, SnapshotVersion
snapshotNumber, BuiltinByteString
nextAccumulatorHash, BuiltinByteString
decommitOutputsHash, BuiltinByteString
commitOutputsHash) [BuiltinByteString]
signature

  -- Bind the exact decommit output set into the multi-signature: the hash is
  -- recomputed from the transaction's own decommit outputs, so changing any
  -- output's address, datum, reference script, ordering or count changes the
  -- signed message and fails signature verification. Without this, only the
  -- aggregate value is checked and a single participant could reuse a valid
  -- all-party signature while redirecting the decommitted value elsewhere.
  decommitOutputsHash :: BuiltinByteString
decommitOutputsHash = [TxOut] -> BuiltinByteString
hashTxOuts [TxOut]
decommitOutputs

  -- A decrement must actually decommit something. Increment and decrement verify
  -- the same signed message, and with zero outputs this branch recomputes
  -- 'decommitOutputsHash' as the empty-list hash — exactly what a snapshot with no
  -- pending decommit produces. Its 'commitOutputsHash' comes from the redeemer, so
  -- without this guard an all-party signature for an INCREMENT snapshot verifies
  -- here too: the version advances and the output datum carries that snapshot's
  -- accumulator, which already counts the deposited UTxOs, while no deposit is
  -- spent and no value enters the head. The head would then credit UTxOs it does
  -- not hold and could never satisfy the strict conservation of (partial) fanout.
  --
  -- With one or more outputs required, the recomputed hash can no longer equal the
  -- empty-list hash, so an increment snapshot cannot authorize a decrement.
  -- NOTE: this must test the DERIVED list, not the redeemer's count.
  -- 'decommitOutputs' is @take numberOfDecommitOutputs (tail outputs)@, which
  -- truncates silently: a redeemer claiming one output in a transaction that
  -- carries only the head output yields an empty list, and the empty-list hash is
  -- exactly what makes the replay above work.
  mustHaveDecommitOutputs :: Bool
mustHaveDecommitOutputs =
    BuiltinString -> Bool -> Bool
traceIfFalse $(errorCode DecrementZeroOutputs) (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$
      Bool -> Bool
not ([TxOut] -> Bool
forall a. [a] -> Bool
L.null [TxOut]
decommitOutputs)

  mustDecreaseValue :: Bool
mustDecreaseValue =
    BuiltinString -> Bool -> Bool
traceIfFalse $(errorCode HeadValueIsNotPreserved) (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$
      Value
headInValue Value -> Value -> Bool
forall a. Eq a => a -> a -> Bool
== Value
headOutValue Value -> Value -> Value
forall a. Semigroup a => a -> a -> a
<> (TxOut -> Value) -> [TxOut] -> Value
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
F.foldMap TxOut -> Value
txOutValue [TxOut]
decommitOutputs

  mustIncreaseVersion :: Bool
mustIncreaseVersion =
    BuiltinString -> Bool -> Bool
traceIfFalse $(errorCode VersionNotIncremented) (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$
      SnapshotVersion
nextVersion SnapshotVersion -> SnapshotVersion -> Bool
forall a. Eq a => a -> a -> Bool
== SnapshotVersion
prevVersion SnapshotVersion -> SnapshotVersion -> SnapshotVersion
forall a. AdditiveSemigroup a => a -> a -> a
+ SnapshotVersion
1

  DecrementRedeemer{[BuiltinByteString]
signature :: [BuiltinByteString]
$sel:signature:DecrementRedeemer :: DecrementRedeemer -> [BuiltinByteString]
signature, SnapshotVersion
snapshotNumber :: SnapshotVersion
$sel:snapshotNumber:DecrementRedeemer :: DecrementRedeemer -> SnapshotVersion
snapshotNumber, SnapshotVersion
numberOfDecommitOutputs :: SnapshotVersion
$sel:numberOfDecommitOutputs:DecrementRedeemer :: DecrementRedeemer -> SnapshotVersion
numberOfDecommitOutputs, BuiltinByteString
commitOutputsHash :: BuiltinByteString
$sel:commitOutputsHash:DecrementRedeemer :: DecrementRedeemer -> BuiltinByteString
commitOutputsHash} = DecrementRedeemer
redeemer

  OpenDatum
    { $sel:parties:OpenDatum :: OpenDatum -> [Party]
parties = [Party]
prevParties
    , $sel:contestationPeriod:OpenDatum :: OpenDatum -> ContestationPeriod
contestationPeriod = ContestationPeriod
prevCperiod
    , $sel:depositPeriod:OpenDatum :: OpenDatum -> DepositPeriod
depositPeriod = DepositPeriod
prevDepositPeriod
    , $sel:headId:OpenDatum :: OpenDatum -> CurrencySymbol
headId = CurrencySymbol
prevHeadId
    , $sel:version:OpenDatum :: OpenDatum -> SnapshotVersion
version = SnapshotVersion
prevVersion
    , $sel:headAdaOverhead:OpenDatum :: OpenDatum -> SnapshotVersion
headAdaOverhead = SnapshotVersion
prevHeadAdaOverhead
    } = OpenDatum
openBefore

  OpenDatum
    { $sel:parties:OpenDatum :: OpenDatum -> [Party]
parties = [Party]
nextParties
    , $sel:contestationPeriod:OpenDatum :: OpenDatum -> ContestationPeriod
contestationPeriod = ContestationPeriod
nextCperiod
    , $sel:depositPeriod:OpenDatum :: OpenDatum -> DepositPeriod
depositPeriod = DepositPeriod
nextDepositPeriod
    , $sel:headId:OpenDatum :: OpenDatum -> CurrencySymbol
headId = CurrencySymbol
nextHeadId
    , $sel:version:OpenDatum :: OpenDatum -> SnapshotVersion
version = SnapshotVersion
nextVersion
    , $sel:accumulatorHash:OpenDatum :: OpenDatum -> BuiltinByteString
accumulatorHash = BuiltinByteString
nextAccumulatorHash
    , $sel:headAdaOverhead:OpenDatum :: OpenDatum -> SnapshotVersion
headAdaOverhead = SnapshotVersion
nextHeadAdaOverhead
    } = ScriptContext -> OpenDatum
decodeHeadOutputOpenDatum ScriptContext
ctx

  -- NOTE: head output + whatever is decommitted needs to be equal to the head input.
  headOutValue :: Value
headOutValue = TxOut -> Value
txOutValue (TxOut -> Value) -> TxOut -> Value
forall a b. (a -> b) -> a -> b
$ [TxOut] -> TxOut
forall a. [a] -> a
L.head [TxOut]
outputs
  headInValue :: Value
headInValue = Value -> (TxInInfo -> Value) -> Maybe TxInInfo -> Value
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Value
forall a. Monoid a => a
mempty (TxOut -> Value
txOutValue (TxOut -> Value) -> (TxInInfo -> TxOut) -> TxInInfo -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TxInInfo -> TxOut
txInInfoResolved) (Maybe TxInInfo -> Value) -> Maybe TxInInfo -> Value
forall a b. (a -> b) -> a -> b
$ ScriptContext -> Maybe TxInInfo
findOwnInput ScriptContext
ctx

  -- NOTE: we always assume Head output is the first one so we pick all other
  -- outputs of a decommit tx to calculate the expected hash.
  decommitOutputs :: [TxOut]
decommitOutputs = SnapshotVersion -> [TxOut] -> [TxOut]
forall a. SnapshotVersion -> [a] -> [a]
L.take SnapshotVersion
numberOfDecommitOutputs ([TxOut] -> [TxOut]
forall a. [a] -> [a]
L.tail [TxOut]
outputs)

  outputs :: [TxOut]
outputs = TxInfo -> [TxOut]
txInfoOutputs TxInfo
txInfo

  ScriptContext{scriptContextTxInfo :: ScriptContext -> TxInfo
scriptContextTxInfo = TxInfo
txInfo} = ScriptContext
ctx
{-# INLINEABLE checkDecrement #-}

-- | Check that the G1 commitment stored in the output datum is consistent with
-- the hash that parties signed. Prevents a malicious closer from storing a wrong
-- commitment while providing a valid signature over a correct hash.
mustMatchAccumulatorCommitmentHash :: BuiltinBLS12_381_G1_Element -> Hash -> Bool
mustMatchAccumulatorCommitmentHash :: BuiltinBLS12_381_G1_Element -> BuiltinByteString -> Bool
mustMatchAccumulatorCommitmentHash BuiltinBLS12_381_G1_Element
commitment BuiltinByteString
hash =
  BuiltinString -> Bool -> Bool
traceIfFalse $(errorCode AccumulatorCommitmentHashMismatch) (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$
    BuiltinByteString -> BuiltinByteString
Builtins.blake2b_256 (BuiltinBLS12_381_G1_Element -> BuiltinByteString
Builtins.bls12_381_G1_compress BuiltinBLS12_381_G1_Element
commitment) BuiltinByteString -> BuiltinByteString -> Bool
forall a. Eq a => a -> a -> Bool
== BuiltinByteString
hash
{-# INLINEABLE mustMatchAccumulatorCommitmentHash #-}

-- | Verify a close transaction.
checkClose ::
  ScriptContext ->
  -- | Open state before the close
  OpenDatum ->
  -- | Type of close transition.
  CloseRedeemer ->
  Bool
checkClose :: ScriptContext -> OpenDatum -> CloseRedeemer -> Bool
checkClose ScriptContext
ctx OpenDatum
openBefore CloseRedeemer
redeemer =
  TxInfo -> Bool
mustNotMintOrBurn TxInfo
txInfo
    Bool -> Bool -> Bool
&& Bool
hasBoundedValidity
    Bool -> Bool -> Bool
&& Bool
checkDeadline
    Bool -> Bool -> Bool
&& ScriptContext -> CurrencySymbol -> Bool
mustBeSignedByParticipant ScriptContext
ctx CurrencySymbol
headId
    Bool -> Bool -> Bool
&& Bool
mustNotChangeVersion
    Bool -> Bool -> Bool
&& Bool
mustBeValidSnapshot
    Bool -> Bool -> Bool
&& Bool
mustInitializeContesters
    Bool -> Bool -> Bool
&& ScriptContext -> Bool
mustPreserveHeadValue ScriptContext
ctx
    Bool -> Bool -> Bool
&& ([Party], [Party])
-> (ContestationPeriod, ContestationPeriod)
-> (CurrencySymbol, CurrencySymbol)
-> (DepositPeriod, DepositPeriod)
-> Bool
mustNotChangeParameters ([Party]
parties', [Party]
parties) (ContestationPeriod
cperiod', ContestationPeriod
cperiod) (CurrencySymbol
headId', CurrencySymbol
headId) (DepositPeriod
dperiod', DepositPeriod
dperiod)
    Bool -> Bool -> Bool
&& Bool
mustBindAccumulatorCommitment
    Bool -> Bool -> Bool
&& SnapshotVersion -> SnapshotVersion -> Bool
mustPreserveHeadAdaOverhead SnapshotVersion
headAdaOverhead SnapshotVersion
headAdaOverhead'
 where
  OpenDatum
    { [Party]
$sel:parties:OpenDatum :: OpenDatum -> [Party]
parties :: [Party]
parties
    , $sel:contestationPeriod:OpenDatum :: OpenDatum -> ContestationPeriod
contestationPeriod = ContestationPeriod
cperiod
    , $sel:depositPeriod:OpenDatum :: OpenDatum -> DepositPeriod
depositPeriod = DepositPeriod
dperiod
    , CurrencySymbol
$sel:headId:OpenDatum :: OpenDatum -> CurrencySymbol
headId :: CurrencySymbol
headId
    , SnapshotVersion
$sel:version:OpenDatum :: OpenDatum -> SnapshotVersion
version :: SnapshotVersion
version
    , SnapshotVersion
$sel:headAdaOverhead:OpenDatum :: OpenDatum -> SnapshotVersion
headAdaOverhead :: SnapshotVersion
headAdaOverhead
    } = OpenDatum
openBefore

  hasBoundedValidity :: Bool
hasBoundedValidity =
    BuiltinString -> Bool -> Bool
traceIfFalse $(errorCode HasBoundedValidityCheckFailed) (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$
      POSIXTime
tMax POSIXTime -> POSIXTime -> POSIXTime
forall a. AdditiveGroup a => a -> a -> a
- POSIXTime
tMin POSIXTime -> POSIXTime -> Bool
forall a. Ord a => a -> a -> Bool
<= POSIXTime
cp

  ClosedDatum
    { $sel:snapshotNumber:ClosedDatum :: ClosedDatum -> SnapshotVersion
snapshotNumber = SnapshotVersion
snapshotNumber'
    , $sel:parties:ClosedDatum :: ClosedDatum -> [Party]
parties = [Party]
parties'
    , $sel:contestationDeadline:ClosedDatum :: ClosedDatum -> POSIXTime
contestationDeadline = POSIXTime
deadline
    , $sel:contestationPeriod:ClosedDatum :: ClosedDatum -> ContestationPeriod
contestationPeriod = ContestationPeriod
cperiod'
    , $sel:depositPeriod:ClosedDatum :: ClosedDatum -> DepositPeriod
depositPeriod = DepositPeriod
dperiod'
    , $sel:headId:ClosedDatum :: ClosedDatum -> CurrencySymbol
headId = CurrencySymbol
headId'
    , $sel:contesters:ClosedDatum :: ClosedDatum -> [PubKeyHash]
contesters = [PubKeyHash]
contesters'
    , $sel:version:ClosedDatum :: ClosedDatum -> SnapshotVersion
version = SnapshotVersion
version'
    , $sel:accumulatorCommitment:ClosedDatum :: ClosedDatum -> BuiltinBLS12_381_G1_Element
accumulatorCommitment = BuiltinBLS12_381_G1_Element
accumulatorCommitment'
    , $sel:headAdaOverhead:ClosedDatum :: ClosedDatum -> SnapshotVersion
headAdaOverhead = SnapshotVersion
headAdaOverhead'
    } = ScriptContext -> ClosedDatum
decodeHeadOutputClosedDatum ScriptContext
ctx

  mustNotChangeVersion :: Bool
mustNotChangeVersion =
    BuiltinString -> Bool -> Bool
traceIfFalse $(errorCode MustNotChangeVersion) (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$
      SnapshotVersion
version' SnapshotVersion -> SnapshotVersion -> Bool
forall a. Eq a => a -> a -> Bool
== SnapshotVersion
version

  mustBeValidSnapshot :: Bool
mustBeValidSnapshot =
    case CloseRedeemer
redeemer of
      CloseRedeemer
CloseInitial ->
        -- For the initial snapshot the accumulator must commit to the empty UTxO set,
        -- whose KZG commitment is the G1 generator (constant polynomial 1).
        BuiltinString -> Bool -> Bool
traceIfFalse $(errorCode FailedCloseInitial) (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$
          SnapshotVersion
version SnapshotVersion -> SnapshotVersion -> Bool
forall a. Eq a => a -> a -> Bool
== SnapshotVersion
0
            Bool -> Bool -> Bool
&& SnapshotVersion
snapshotNumber' SnapshotVersion -> SnapshotVersion -> Bool
forall a. Eq a => a -> a -> Bool
== SnapshotVersion
0
            -- The empty-accumulator commitment is the G1 generator
            -- (getFinalPoly [] = [1], so getG1Commitment [G1] [1] = G1). Pin it
            -- so a closer cannot seed a degenerate commitment that would later
            -- be trusted by progressFromClosed and checkMembershipPairing.
            Bool -> Bool -> Bool
&& BuiltinBLS12_381_G1_Element -> Bool
isG1Generator BuiltinBLS12_381_G1_Element
accumulatorCommitment'
      CloseAny{[BuiltinByteString]
signature :: [BuiltinByteString]
$sel:signature:CloseInitial :: CloseRedeemer -> [BuiltinByteString]
signature, BuiltinByteString
accumulatorHash :: BuiltinByteString
$sel:accumulatorHash:CloseInitial :: CloseRedeemer -> BuiltinByteString
accumulatorHash, BuiltinByteString
decommitOutputsHash :: BuiltinByteString
$sel:decommitOutputsHash:CloseInitial :: CloseRedeemer -> BuiltinByteString
decommitOutputsHash, BuiltinByteString
commitOutputsHash :: BuiltinByteString
$sel:commitOutputsHash:CloseInitial :: CloseRedeemer -> BuiltinByteString
commitOutputsHash} ->
        BuiltinString -> Bool -> Bool
traceIfFalse $(errorCode FailedCloseAny) (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$
          SnapshotVersion
snapshotNumber' SnapshotVersion -> SnapshotVersion -> Bool
forall a. Ord a => a -> a -> Bool
> SnapshotVersion
0
            Bool -> Bool -> Bool
&& [Party]
-> (CurrencySymbol, SnapshotVersion, SnapshotVersion,
    BuiltinByteString, BuiltinByteString, BuiltinByteString)
-> [BuiltinByteString]
-> Bool
verifySnapshotSignature
              [Party]
parties
              (CurrencySymbol
headId, SnapshotVersion
version, SnapshotVersion
snapshotNumber', BuiltinByteString
accumulatorHash, BuiltinByteString
decommitOutputsHash, BuiltinByteString
commitOutputsHash)
              [BuiltinByteString]
signature
      CloseUnused{[BuiltinByteString]
$sel:signature:CloseInitial :: CloseRedeemer -> [BuiltinByteString]
signature :: [BuiltinByteString]
signature, BuiltinByteString
$sel:accumulatorHash:CloseInitial :: CloseRedeemer -> BuiltinByteString
accumulatorHash :: BuiltinByteString
accumulatorHash, BuiltinByteString
$sel:decommitOutputsHash:CloseInitial :: CloseRedeemer -> BuiltinByteString
decommitOutputsHash :: BuiltinByteString
decommitOutputsHash, BuiltinByteString
$sel:commitOutputsHash:CloseInitial :: CloseRedeemer -> BuiltinByteString
commitOutputsHash :: BuiltinByteString
commitOutputsHash} ->
        BuiltinString -> Bool -> Bool
traceIfFalse $(errorCode FailedCloseUnused) (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$
          [Party]
-> (CurrencySymbol, SnapshotVersion, SnapshotVersion,
    BuiltinByteString, BuiltinByteString, BuiltinByteString)
-> [BuiltinByteString]
-> Bool
verifySnapshotSignature
            [Party]
parties
            (CurrencySymbol
headId, SnapshotVersion
version, SnapshotVersion
snapshotNumber', BuiltinByteString
accumulatorHash, BuiltinByteString
decommitOutputsHash, BuiltinByteString
commitOutputsHash)
            [BuiltinByteString]
signature
      CloseUsed{[BuiltinByteString]
$sel:signature:CloseInitial :: CloseRedeemer -> [BuiltinByteString]
signature :: [BuiltinByteString]
signature, BuiltinByteString
$sel:accumulatorHash:CloseInitial :: CloseRedeemer -> BuiltinByteString
accumulatorHash :: BuiltinByteString
accumulatorHash, BuiltinByteString
$sel:decommitOutputsHash:CloseInitial :: CloseRedeemer -> BuiltinByteString
decommitOutputsHash :: BuiltinByteString
decommitOutputsHash, BuiltinByteString
$sel:commitOutputsHash:CloseInitial :: CloseRedeemer -> BuiltinByteString
commitOutputsHash :: BuiltinByteString
commitOutputsHash} ->
        BuiltinString -> Bool -> Bool
traceIfFalse $(errorCode FailedCloseUsed) (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$
          [Party]
-> (CurrencySymbol, SnapshotVersion, SnapshotVersion,
    BuiltinByteString, BuiltinByteString, BuiltinByteString)
-> [BuiltinByteString]
-> Bool
verifySnapshotSignature
            [Party]
parties
            (CurrencySymbol
headId, SnapshotVersion
version SnapshotVersion -> SnapshotVersion -> SnapshotVersion
forall a. AdditiveGroup a => a -> a -> a
- SnapshotVersion
1, SnapshotVersion
snapshotNumber', BuiltinByteString
accumulatorHash, BuiltinByteString
decommitOutputsHash, BuiltinByteString
commitOutputsHash)
            [BuiltinByteString]
signature

  checkDeadline :: Bool
checkDeadline =
    BuiltinString -> Bool -> Bool
traceIfFalse $(errorCode IncorrectClosedContestationDeadline) (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$
      POSIXTime
deadline POSIXTime -> POSIXTime -> Bool
forall a. Eq a => a -> a -> Bool
== ContestationPeriod -> ScriptContext -> POSIXTime
makeContestationDeadline ContestationPeriod
cperiod ScriptContext
ctx

  cp :: POSIXTime
cp = DiffMilliSeconds -> POSIXTime
fromMilliSeconds (ContestationPeriod -> DiffMilliSeconds
milliseconds ContestationPeriod
cperiod)

  tMax :: POSIXTime
tMax = case Interval POSIXTime -> UpperBound POSIXTime
forall a. Interval a -> UpperBound a
ivTo (Interval POSIXTime -> UpperBound POSIXTime)
-> Interval POSIXTime -> UpperBound POSIXTime
forall a b. (a -> b) -> a -> b
$ TxInfo -> Interval POSIXTime
txInfoValidRange TxInfo
txInfo of
    UpperBound (Finite POSIXTime
t) Bool
_ -> POSIXTime
t
    UpperBound POSIXTime
_InfiniteBound -> BuiltinString -> POSIXTime
forall a. BuiltinString -> a
traceError $(errorCode InfiniteUpperBound)

  tMin :: POSIXTime
tMin = case Interval POSIXTime -> LowerBound POSIXTime
forall a. Interval a -> LowerBound a
ivFrom (Interval POSIXTime -> LowerBound POSIXTime)
-> Interval POSIXTime -> LowerBound POSIXTime
forall a b. (a -> b) -> a -> b
$ TxInfo -> Interval POSIXTime
txInfoValidRange TxInfo
txInfo of
    LowerBound (Finite POSIXTime
t) Bool
_ -> POSIXTime
t
    LowerBound POSIXTime
_InfiniteBound -> BuiltinString -> POSIXTime
forall a. BuiltinString -> a
traceError $(errorCode InfiniteLowerBound)

  mustInitializeContesters :: Bool
mustInitializeContesters =
    BuiltinString -> Bool -> Bool
traceIfFalse $(errorCode ContestersNonEmpty) (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$
      [PubKeyHash] -> Bool
forall a. [a] -> Bool
L.null [PubKeyHash]
contesters'

  mustBindAccumulatorCommitment :: Bool
mustBindAccumulatorCommitment =
    case CloseRedeemer
redeemer of
      CloseRedeemer
CloseInitial -> Bool
True
      CloseAny{BuiltinByteString
$sel:accumulatorHash:CloseInitial :: CloseRedeemer -> BuiltinByteString
accumulatorHash :: BuiltinByteString
accumulatorHash} -> BuiltinByteString -> Bool
check' BuiltinByteString
accumulatorHash
      CloseUnused{BuiltinByteString
$sel:accumulatorHash:CloseInitial :: CloseRedeemer -> BuiltinByteString
accumulatorHash :: BuiltinByteString
accumulatorHash} -> BuiltinByteString -> Bool
check' BuiltinByteString
accumulatorHash
      CloseUsed{BuiltinByteString
$sel:accumulatorHash:CloseInitial :: CloseRedeemer -> BuiltinByteString
accumulatorHash :: BuiltinByteString
accumulatorHash} -> BuiltinByteString -> Bool
check' BuiltinByteString
accumulatorHash
   where
    check' :: BuiltinByteString -> Bool
check' = BuiltinBLS12_381_G1_Element -> BuiltinByteString -> Bool
mustMatchAccumulatorCommitmentHash BuiltinBLS12_381_G1_Element
accumulatorCommitment'

  ScriptContext{scriptContextTxInfo :: ScriptContext -> TxInfo
scriptContextTxInfo = TxInfo
txInfo} = ScriptContext
ctx
{-# INLINEABLE checkClose #-}

-- | Verify a contest transaction.
checkContest ::
  ScriptContext ->
  -- | Closed state before the close
  ClosedDatum ->
  -- | Type of contest transition.
  ContestRedeemer ->
  Bool
checkContest :: ScriptContext -> ClosedDatum -> ContestRedeemer -> Bool
checkContest ScriptContext
ctx ClosedDatum
closedDatum ContestRedeemer
redeemer =
  TxInfo -> Bool
mustNotMintOrBurn TxInfo
txInfo
    Bool -> Bool -> Bool
&& Bool
mustNotChangeVersion
    Bool -> Bool -> Bool
&& Bool
mustBeNewer
    Bool -> Bool -> Bool
&& Bool
mustBeValidSnapshot
    Bool -> Bool -> Bool
&& ScriptContext -> CurrencySymbol -> Bool
mustBeSignedByParticipant ScriptContext
ctx CurrencySymbol
headId
    Bool -> Bool -> Bool
&& Bool
checkSignedParticipantContestOnlyOnce
    Bool -> Bool -> Bool
&& Bool
mustBeWithinContestationPeriod
    Bool -> Bool -> Bool
&& Bool
mustUpdateContesters
    Bool -> Bool -> Bool
&& Bool
mustPushDeadline
    Bool -> Bool -> Bool
&& ([Party], [Party])
-> (ContestationPeriod, ContestationPeriod)
-> (CurrencySymbol, CurrencySymbol)
-> (DepositPeriod, DepositPeriod)
-> Bool
mustNotChangeParameters ([Party]
parties', [Party]
parties) (ContestationPeriod
contestationPeriod', ContestationPeriod
contestationPeriod) (CurrencySymbol
headId', CurrencySymbol
headId) (DepositPeriod
depositPeriod', DepositPeriod
depositPeriod)
    Bool -> Bool -> Bool
&& SnapshotVersion -> SnapshotVersion -> Bool
mustPreserveHeadAdaOverhead SnapshotVersion
headAdaOverhead SnapshotVersion
headAdaOverhead'
    Bool -> Bool -> Bool
&& ScriptContext -> Bool
mustPreserveHeadValue ScriptContext
ctx
    Bool -> Bool -> Bool
&& Bool
mustBindAccumulatorCommitment
 where
  mustBeNewer :: Bool
mustBeNewer =
    BuiltinString -> Bool -> Bool
traceIfFalse $(errorCode TooOldSnapshot) (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$
      SnapshotVersion
snapshotNumber' SnapshotVersion -> SnapshotVersion -> Bool
forall a. Ord a => a -> a -> Bool
> SnapshotVersion
snapshotNumber

  mustNotChangeVersion :: Bool
mustNotChangeVersion =
    BuiltinString -> Bool -> Bool
traceIfFalse $(errorCode MustNotChangeVersion) (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$
      SnapshotVersion
version' SnapshotVersion -> SnapshotVersion -> Bool
forall a. Eq a => a -> a -> Bool
== SnapshotVersion
version

  mustBeValidSnapshot :: Bool
mustBeValidSnapshot =
    case ContestRedeemer
redeemer of
      ContestUnused{[BuiltinByteString]
signature :: [BuiltinByteString]
$sel:signature:ContestUnused :: ContestRedeemer -> [BuiltinByteString]
signature, BuiltinByteString
accumulatorHash :: BuiltinByteString
$sel:accumulatorHash:ContestUnused :: ContestRedeemer -> BuiltinByteString
accumulatorHash, BuiltinByteString
decommitOutputsHash :: BuiltinByteString
$sel:decommitOutputsHash:ContestUnused :: ContestRedeemer -> BuiltinByteString
decommitOutputsHash, BuiltinByteString
commitOutputsHash :: BuiltinByteString
$sel:commitOutputsHash:ContestUnused :: ContestRedeemer -> BuiltinByteString
commitOutputsHash} ->
        BuiltinString -> Bool -> Bool
traceIfFalse $(errorCode FailedContestUnused) (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$
          [Party]
-> (CurrencySymbol, SnapshotVersion, SnapshotVersion,
    BuiltinByteString, BuiltinByteString, BuiltinByteString)
-> [BuiltinByteString]
-> Bool
verifySnapshotSignature
            [Party]
parties
            (CurrencySymbol
headId, SnapshotVersion
version, SnapshotVersion
snapshotNumber', BuiltinByteString
accumulatorHash, BuiltinByteString
decommitOutputsHash, BuiltinByteString
commitOutputsHash)
            [BuiltinByteString]
signature
      ContestUsed{[BuiltinByteString]
$sel:signature:ContestUnused :: ContestRedeemer -> [BuiltinByteString]
signature :: [BuiltinByteString]
signature, BuiltinByteString
$sel:accumulatorHash:ContestUnused :: ContestRedeemer -> BuiltinByteString
accumulatorHash :: BuiltinByteString
accumulatorHash, BuiltinByteString
$sel:decommitOutputsHash:ContestUnused :: ContestRedeemer -> BuiltinByteString
decommitOutputsHash :: BuiltinByteString
decommitOutputsHash, BuiltinByteString
$sel:commitOutputsHash:ContestUnused :: ContestRedeemer -> BuiltinByteString
commitOutputsHash :: BuiltinByteString
commitOutputsHash} ->
        BuiltinString -> Bool -> Bool
traceIfFalse $(errorCode FailedContestUsed) (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$
          [Party]
-> (CurrencySymbol, SnapshotVersion, SnapshotVersion,
    BuiltinByteString, BuiltinByteString, BuiltinByteString)
-> [BuiltinByteString]
-> Bool
verifySnapshotSignature
            [Party]
parties
            (CurrencySymbol
headId, SnapshotVersion
version SnapshotVersion -> SnapshotVersion -> SnapshotVersion
forall a. AdditiveGroup a => a -> a -> a
- SnapshotVersion
1, SnapshotVersion
snapshotNumber', BuiltinByteString
accumulatorHash, BuiltinByteString
decommitOutputsHash, BuiltinByteString
commitOutputsHash)
            [BuiltinByteString]
signature

  mustBeWithinContestationPeriod :: Bool
mustBeWithinContestationPeriod =
    case Interval POSIXTime -> UpperBound POSIXTime
forall a. Interval a -> UpperBound a
ivTo (TxInfo -> Interval POSIXTime
txInfoValidRange TxInfo
txInfo) of
      UpperBound (Finite POSIXTime
time) Bool
_ ->
        BuiltinString -> Bool -> Bool
traceIfFalse $(errorCode UpperBoundBeyondContestationDeadline) (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$
          POSIXTime
time POSIXTime -> POSIXTime -> Bool
forall a. Ord a => a -> a -> Bool
<= POSIXTime
contestationDeadline
      UpperBound POSIXTime
_ -> BuiltinString -> Bool
forall a. BuiltinString -> a
traceError $(errorCode ContestNoUpperBoundDefined)

  mustPushDeadline :: Bool
mustPushDeadline =
    if [PubKeyHash] -> SnapshotVersion
forall a. [a] -> SnapshotVersion
L.length [PubKeyHash]
contesters' SnapshotVersion -> SnapshotVersion -> Bool
forall a. Eq a => a -> a -> Bool
== [Party] -> SnapshotVersion
forall a. [a] -> SnapshotVersion
L.length [Party]
parties'
      then
        BuiltinString -> Bool -> Bool
traceIfFalse $(errorCode MustNotPushDeadline) (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$
          POSIXTime
contestationDeadline' POSIXTime -> POSIXTime -> Bool
forall a. Eq a => a -> a -> Bool
== POSIXTime
contestationDeadline
      else
        BuiltinString -> Bool -> Bool
traceIfFalse $(errorCode MustPushDeadline) (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$
          POSIXTime
contestationDeadline' POSIXTime -> POSIXTime -> Bool
forall a. Eq a => a -> a -> Bool
== POSIXTime -> ContestationPeriod -> POSIXTime
addContestationPeriod POSIXTime
contestationDeadline ContestationPeriod
contestationPeriod

  mustUpdateContesters :: Bool
mustUpdateContesters =
    BuiltinString -> Bool -> Bool
traceIfFalse $(errorCode ContesterNotIncluded) (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$
      [PubKeyHash]
contesters' [PubKeyHash] -> [PubKeyHash] -> Bool
forall a. Eq a => a -> a -> Bool
== PubKeyHash
contester PubKeyHash -> [PubKeyHash] -> [PubKeyHash]
forall a. a -> [a] -> [a]
: [PubKeyHash]
contesters

  ClosedDatum
    { POSIXTime
$sel:contestationDeadline:ClosedDatum :: ClosedDatum -> POSIXTime
contestationDeadline :: POSIXTime
contestationDeadline
    , ContestationPeriod
$sel:contestationPeriod:ClosedDatum :: ClosedDatum -> ContestationPeriod
contestationPeriod :: ContestationPeriod
contestationPeriod
    , DepositPeriod
$sel:depositPeriod:ClosedDatum :: ClosedDatum -> DepositPeriod
depositPeriod :: DepositPeriod
depositPeriod
    , [Party]
$sel:parties:ClosedDatum :: ClosedDatum -> [Party]
parties :: [Party]
parties
    , SnapshotVersion
$sel:snapshotNumber:ClosedDatum :: ClosedDatum -> SnapshotVersion
snapshotNumber :: SnapshotVersion
snapshotNumber
    , [PubKeyHash]
$sel:contesters:ClosedDatum :: ClosedDatum -> [PubKeyHash]
contesters :: [PubKeyHash]
contesters
    , CurrencySymbol
$sel:headId:ClosedDatum :: ClosedDatum -> CurrencySymbol
headId :: CurrencySymbol
headId
    , SnapshotVersion
$sel:version:ClosedDatum :: ClosedDatum -> SnapshotVersion
version :: SnapshotVersion
version
    , SnapshotVersion
$sel:headAdaOverhead:ClosedDatum :: ClosedDatum -> SnapshotVersion
headAdaOverhead :: SnapshotVersion
headAdaOverhead
    } = ClosedDatum
closedDatum

  ClosedDatum
    { $sel:snapshotNumber:ClosedDatum :: ClosedDatum -> SnapshotVersion
snapshotNumber = SnapshotVersion
snapshotNumber'
    , $sel:parties:ClosedDatum :: ClosedDatum -> [Party]
parties = [Party]
parties'
    , $sel:contestationDeadline:ClosedDatum :: ClosedDatum -> POSIXTime
contestationDeadline = POSIXTime
contestationDeadline'
    , $sel:contestationPeriod:ClosedDatum :: ClosedDatum -> ContestationPeriod
contestationPeriod = ContestationPeriod
contestationPeriod'
    , $sel:depositPeriod:ClosedDatum :: ClosedDatum -> DepositPeriod
depositPeriod = DepositPeriod
depositPeriod'
    , $sel:headId:ClosedDatum :: ClosedDatum -> CurrencySymbol
headId = CurrencySymbol
headId'
    , $sel:contesters:ClosedDatum :: ClosedDatum -> [PubKeyHash]
contesters = [PubKeyHash]
contesters'
    , $sel:version:ClosedDatum :: ClosedDatum -> SnapshotVersion
version = SnapshotVersion
version'
    , $sel:accumulatorCommitment:ClosedDatum :: ClosedDatum -> BuiltinBLS12_381_G1_Element
accumulatorCommitment = BuiltinBLS12_381_G1_Element
accumulatorCommitment'
    , $sel:headAdaOverhead:ClosedDatum :: ClosedDatum -> SnapshotVersion
headAdaOverhead = SnapshotVersion
headAdaOverhead'
    } = ScriptContext -> ClosedDatum
decodeHeadOutputClosedDatum ScriptContext
ctx

  ScriptContext{scriptContextTxInfo :: ScriptContext -> TxInfo
scriptContextTxInfo = TxInfo
txInfo} = ScriptContext
ctx

  contester :: PubKeyHash
contester =
    case TxInfo -> [PubKeyHash]
txInfoSignatories TxInfo
txInfo of
      [PubKeyHash
signer] -> PubKeyHash
signer
      [PubKeyHash]
_ -> BuiltinString -> PubKeyHash
forall a. BuiltinString -> a
traceError $(errorCode WrongNumberOfSigners)

  checkSignedParticipantContestOnlyOnce :: Bool
checkSignedParticipantContestOnlyOnce =
    BuiltinString -> Bool -> Bool
traceIfFalse $(errorCode SignerAlreadyContested) (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$
      PubKeyHash
contester PubKeyHash -> [PubKeyHash] -> Bool
forall a. Eq a => a -> [a] -> Bool
`L.notElem` [PubKeyHash]
contesters

  mustBindAccumulatorCommitment :: Bool
mustBindAccumulatorCommitment =
    case ContestRedeemer
redeemer of
      ContestUnused{BuiltinByteString
$sel:accumulatorHash:ContestUnused :: ContestRedeemer -> BuiltinByteString
accumulatorHash :: BuiltinByteString
accumulatorHash} -> BuiltinByteString -> Bool
check' BuiltinByteString
accumulatorHash
      ContestUsed{BuiltinByteString
$sel:accumulatorHash:ContestUnused :: ContestRedeemer -> BuiltinByteString
accumulatorHash :: BuiltinByteString
accumulatorHash} -> BuiltinByteString -> Bool
check' BuiltinByteString
accumulatorHash
   where
    check' :: BuiltinByteString -> Bool
check' = BuiltinBLS12_381_G1_Element -> BuiltinByteString -> Bool
mustMatchAccumulatorCommitmentHash BuiltinBLS12_381_G1_Element
accumulatorCommitment'
{-# INLINEABLE checkContest #-}

-- | Verify a fanout transaction using a KZG membership proof.
-- All distributed outputs are verified as members of the accumulator in a single proof.
headIsFinalizedWith ::
  BuiltinByteString ->
  ScriptContext ->
  -- | Closed state before the fanout
  ClosedDatum ->
  -- | Number of distributed UTxO outputs (excludes change output)
  Integer ->
  -- | Membership proof (quotient commitment G1 element)
  BuiltinBLS12_381_G1_Element ->
  -- | Reference input containing CRS
  TxOutRef ->
  Bool
headIsFinalizedWith :: BuiltinByteString
-> ScriptContext
-> ClosedDatum
-> SnapshotVersion
-> BuiltinBLS12_381_G1_Element
-> TxOutRef
-> Bool
headIsFinalizedWith BuiltinByteString
crsDatumHash ScriptContext
ctx ClosedDatum
closedDatum SnapshotVersion
numberOfFanoutOutputs BuiltinBLS12_381_G1_Element
proof TxOutRef
crsRef =
  MintValue -> CurrencySymbol -> [Party] -> Bool
mustBurnAllHeadTokens MintValue
minted CurrencySymbol
headId [Party]
parties
    Bool -> Bool -> Bool
&& TxInfo -> POSIXTime -> Bool
afterContestationDeadline TxInfo
txInfo POSIXTime
contestationDeadline
    Bool -> Bool -> Bool
&& Bool
checkCRSAndMembership
    Bool -> Bool -> Bool
&& Bool
mustConserveValue
 where
  ScriptContext{scriptContextTxInfo :: ScriptContext -> TxInfo
scriptContextTxInfo = TxInfo
txInfo} = ScriptContext
ctx

  minted :: MintValue
minted = TxInfo -> MintValue
txInfoMint TxInfo
txInfo

  TxInfo{[TxOut]
txInfoOutputs :: TxInfo -> [TxOut]
txInfoOutputs :: [TxOut]
txInfoOutputs} = TxInfo
txInfo

  ClosedDatum{BuiltinBLS12_381_G1_Element
$sel:accumulatorCommitment:ClosedDatum :: ClosedDatum -> BuiltinBLS12_381_G1_Element
accumulatorCommitment :: BuiltinBLS12_381_G1_Element
accumulatorCommitment, [Party]
$sel:parties:ClosedDatum :: ClosedDatum -> [Party]
parties :: [Party]
parties, CurrencySymbol
$sel:headId:ClosedDatum :: ClosedDatum -> CurrencySymbol
headId :: CurrencySymbol
headId, POSIXTime
$sel:contestationDeadline:ClosedDatum :: ClosedDatum -> POSIXTime
contestationDeadline :: POSIXTime
contestationDeadline, SnapshotVersion
$sel:headAdaOverhead:ClosedDatum :: ClosedDatum -> SnapshotVersion
headAdaOverhead :: SnapshotVersion
headAdaOverhead} = ClosedDatum
closedDatum

  fanoutOutputs :: [TxOut]
fanoutOutputs = SnapshotVersion -> [TxOut] -> [TxOut]
forall a. SnapshotVersion -> [a] -> [a]
L.take SnapshotVersion
numberOfFanoutOutputs [TxOut]
txInfoOutputs

  subsetScalars :: [Integer]
  subsetScalars :: [SnapshotVersion]
subsetScalars = [TxOut] -> [SnapshotVersion]
txOutsToSubsetScalars [TxOut]
fanoutOutputs

  -- Subset membership proof: all fanout outputs are members of the accumulator.
  -- isG1Generator is intentionally omitted — pre-settled UTxOs (decommitted/deposited
  -- before Close) remain in the accumulator but are not fanned out. Completeness is
  -- enforced by mustConserveValue instead.
  --
  -- NOTE: Unlike 'checkPartialFanout' and 'checkFinalPartialFanout' there is
  -- deliberately no @numberOfFanoutOutputs > 0@ guard here, even though an empty
  -- subset degenerates the pairing to e(A,G2) = e(proof,G2) and passes for
  -- proof = A. A head whose UTxO set is empty (nothing was ever committed, or
  -- everything was decommitted) fans out zero outputs on this path and on this
  -- path only, so rejecting them would leave its ADA overhead locked forever.
  -- The degenerate case is bounded by mustConserveValue: with no outputs the head
  -- input must equal the burned tokens plus 'headAdaOverhead', i.e. the head holds
  -- no L2 UTxO value at all.
  checkCRSAndMembership :: Bool
checkCRSAndMembership =
    BuiltinString -> Bool -> Bool
traceIfFalse $(errorCode FanoutUTxOHashMismatch) (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$
      BuiltinByteString
-> TxInfo -> TxOutRef -> (CRSDatum -> Bool) -> Bool
withCRSLookup BuiltinByteString
crsDatumHash TxInfo
txInfo TxOutRef
crsRef ((CRSDatum -> Bool) -> Bool) -> (CRSDatum -> Bool) -> Bool
forall a b. (a -> b) -> a -> b
$ \CRSDatum
crsData ->
        BuiltinBLS12_381_G1_Element
-> BuiltinBLS12_381_G1_Element
-> CRSDatum
-> [SnapshotVersion]
-> Bool
checkMembershipPairing BuiltinBLS12_381_G1_Element
accumulatorCommitment BuiltinBLS12_381_G1_Element
proof CRSDatum
crsData [SnapshotVersion]
subsetScalars

  -- Strict equality: fanout outputs + burned tokens + fixed overhead must equal the
  -- full head input value. headAdaOverhead is the lovelace locked in the head UTxO
  -- that is not part of any L2 UTxO (min-UTxO overhead set at Init).
  mustConserveValue :: Bool
mustConserveValue =
    BuiltinString -> Bool -> Bool
traceIfFalse $(errorCode HeadValueIsNotPreserved) (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$
      Value
headInValue
        Value -> Value -> Bool
forall a. Eq a => a -> a -> Bool
== (TxOut -> Value) -> [TxOut] -> Value
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
F.foldMap TxOut -> Value
txOutValue [TxOut]
fanoutOutputs
        Value -> Value -> Value
forall a. Semigroup a => a -> a -> a
<> MintValue -> Value
mintValueBurned MintValue
minted
        Value -> Value -> Value
forall a. Semigroup a => a -> a -> a
<> CurrencySymbol -> TokenName -> SnapshotVersion -> Value
singleton CurrencySymbol
adaSymbol TokenName
adaToken SnapshotVersion
headAdaOverhead
   where
    headInValue :: Value
headInValue = Value -> (TxInInfo -> Value) -> Maybe TxInInfo -> Value
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Value
forall a. Monoid a => a
mempty (TxOut -> Value
txOutValue (TxOut -> Value) -> (TxInInfo -> TxOut) -> TxInInfo -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TxInInfo -> TxOut
txInInfoResolved) (Maybe TxInInfo -> Value) -> Maybe TxInInfo -> Value
forall a b. (a -> b) -> a -> b
$ ScriptContext -> Maybe TxInInfo
findOwnInput ScriptContext
ctx
{-# INLINEABLE headIsFinalizedWith #-}

-- | Verify a partial fanout transaction. Transitions either Closed → FanoutProgress
-- or FanoutProgress → FanoutProgress: distributes a subset of UTxOs and continues
-- with a smaller FanoutProgressDatum.
--
-- The continuing head output must be the first transaction output. Distributed
-- UTxOs follow at indices [1 .. numberOfPartialOutputs].
checkPartialFanout ::
  BuiltinByteString ->
  ScriptContext ->
  -- | Progress state (extracted from either Closed or FanoutProgress input)
  FanoutProgressDatum ->
  -- | Number of outputs to distribute in this partial fanout
  Integer ->
  -- | Reference input containing CRS
  TxOutRef ->
  Bool
checkPartialFanout :: BuiltinByteString
-> ScriptContext
-> FanoutProgressDatum
-> SnapshotVersion
-> TxOutRef
-> Bool
checkPartialFanout BuiltinByteString
crsDatumHash ctx :: ScriptContext
ctx@ScriptContext{scriptContextTxInfo :: ScriptContext -> TxInfo
scriptContextTxInfo = TxInfo
txInfo} FanoutProgressDatum
progressDatum SnapshotVersion
numberOfPartialOutputs TxOutRef
crsRef =
  Bool
mustHaveOutputs
    Bool -> Bool -> Bool
&& Bool
mustNotBeLastBatch
    Bool -> Bool -> Bool
&& TxInfo -> Bool
mustNotMintOrBurn TxInfo
txInfo
    Bool -> Bool -> Bool
&& TxInfo -> POSIXTime -> Bool
afterContestationDeadline TxInfo
txInfo POSIXTime
contestationDeadline
    Bool -> Bool -> Bool
&& Bool
mustPreserveFanoutProgressState
    Bool -> Bool -> Bool
&& Bool
mustConserveValue
    Bool -> Bool -> Bool
&& Bool
checkCRSAndMembership
 where
  FanoutProgressDatum
    { [Party]
parties :: [Party]
$sel:parties:FanoutProgressDatum :: FanoutProgressDatum -> [Party]
parties
    , CurrencySymbol
headId :: CurrencySymbol
$sel:headId:FanoutProgressDatum :: FanoutProgressDatum -> CurrencySymbol
headId
    , POSIXTime
contestationDeadline :: POSIXTime
$sel:contestationDeadline:FanoutProgressDatum :: FanoutProgressDatum -> POSIXTime
contestationDeadline
    , BuiltinBLS12_381_G1_Element
accumulatorCommitment :: BuiltinBLS12_381_G1_Element
$sel:accumulatorCommitment:FanoutProgressDatum :: FanoutProgressDatum -> BuiltinBLS12_381_G1_Element
accumulatorCommitment
    , SnapshotVersion
headAdaOverhead :: SnapshotVersion
$sel:headAdaOverhead:FanoutProgressDatum :: FanoutProgressDatum -> SnapshotVersion
headAdaOverhead
    } = FanoutProgressDatum
progressDatum

  -- Decode continuing output datum as FanoutProgressDatum (first output, at head address)
  FanoutProgressDatum
    { $sel:parties:FanoutProgressDatum :: FanoutProgressDatum -> [Party]
parties = [Party]
parties'
    , $sel:headId:FanoutProgressDatum :: FanoutProgressDatum -> CurrencySymbol
headId = CurrencySymbol
headId'
    , $sel:contestationDeadline:FanoutProgressDatum :: FanoutProgressDatum -> POSIXTime
contestationDeadline = POSIXTime
contestationDeadline'
    , $sel:accumulatorCommitment:FanoutProgressDatum :: FanoutProgressDatum -> BuiltinBLS12_381_G1_Element
accumulatorCommitment = BuiltinBLS12_381_G1_Element
newAccumulatorCommitment
    , $sel:headAdaOverhead:FanoutProgressDatum :: FanoutProgressDatum -> SnapshotVersion
headAdaOverhead = SnapshotVersion
headAdaOverhead'
    } = ScriptContext -> FanoutProgressDatum
decodeHeadOutputFanoutProgressDatum ScriptContext
ctx

  -- Guard against numberOfPartialOutputs = 0: with an empty subset the KZG
  -- check degenerates to e(A,G2) = e(newAcc,G2), passing trivially when
  -- newAcc = A. The exact-equality value check (==) prevents fund theft, but
  -- the zero-output path is semantically meaningless and wastes budget.
  mustHaveOutputs :: Bool
mustHaveOutputs =
    BuiltinString -> Bool -> Bool
traceIfFalse $(errorCode PartialFanoutZeroOutputs) (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$
      SnapshotVersion
numberOfPartialOutputs SnapshotVersion -> SnapshotVersion -> Bool
forall a. Ord a => a -> a -> Bool
> SnapshotVersion
0

  -- Prevent distributing ALL remaining elements via PartialFanout instead of
  -- FinalPartialFanout. When newAccumulatorCommitment = G1_generator all
  -- elements have been removed, so the next step MUST be FinalPartialFanout
  -- (which burns tokens). Using PartialFanout for the last batch produces a
  -- stuck FanoutProgress UTxO whose tokens can never be burned.
  mustNotBeLastBatch :: Bool
mustNotBeLastBatch =
    BuiltinString -> Bool -> Bool
traceIfFalse $(errorCode PartialFanoutCannotBeLastBatch) (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$
      Bool -> Bool
not (BuiltinBLS12_381_G1_Element -> Bool
isG1Generator BuiltinBLS12_381_G1_Element
newAccumulatorCommitment)

  TxInfo{[TxOut]
txInfoOutputs :: TxInfo -> [TxOut]
txInfoOutputs :: [TxOut]
txInfoOutputs} = TxInfo
txInfo

  -- The distributed UTxO outputs are at indices [1..numberOfPartialOutputs].
  -- Index 0 is the continuing head output.
  distributedOutputs :: [TxOut]
distributedOutputs = SnapshotVersion -> [TxOut] -> [TxOut]
forall a. SnapshotVersion -> [a] -> [a]
L.take SnapshotVersion
numberOfPartialOutputs (SnapshotVersion -> [TxOut] -> [TxOut]
forall a. SnapshotVersion -> [a] -> [a]
L.drop SnapshotVersion
1 [TxOut]
txInfoOutputs)

  -- Ensure the continuing FanoutProgressDatum carries the correct parameters.
  -- accumulatorCommitment is NOT checked here — it is verified by checkCRSAndMembership.
  mustPreserveFanoutProgressState :: Bool
mustPreserveFanoutProgressState =
    BuiltinString -> Bool -> Bool
traceIfFalse $(errorCode PartialFanoutChangedParameters) (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$
      [Party]
parties' [Party] -> [Party] -> Bool
forall a. Eq a => a -> a -> Bool
== [Party]
parties
        Bool -> Bool -> Bool
&& CurrencySymbol
headId' CurrencySymbol -> CurrencySymbol -> Bool
forall a. Eq a => a -> a -> Bool
== CurrencySymbol
headId
        Bool -> Bool -> Bool
&& POSIXTime
contestationDeadline' POSIXTime -> POSIXTime -> Bool
forall a. Eq a => a -> a -> Bool
== POSIXTime
contestationDeadline
        Bool -> Bool -> Bool
&& SnapshotVersion
headAdaOverhead' SnapshotVersion -> SnapshotVersion -> Bool
forall a. Eq a => a -> a -> Bool
== SnapshotVersion
headAdaOverhead

  -- The head input value must equal the continuing head output value plus the
  -- sum of all distributed outputs. This prevents stealing Ada by adding extra
  -- outputs that are not counted by the membership proof.
  mustConserveValue :: Bool
mustConserveValue =
    BuiltinString -> Bool -> Bool
traceIfFalse $(errorCode HeadValueIsNotPreserved) (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$
      Value
headInValue Value -> Value -> Bool
forall a. Eq a => a -> a -> Bool
== Value
headOutValue Value -> Value -> Value
forall a. Semigroup a => a -> a -> a
<> (TxOut -> Value) -> [TxOut] -> Value
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
F.foldMap TxOut -> Value
txOutValue [TxOut]
distributedOutputs
   where
    headInValue :: Value
headInValue = Value -> (TxInInfo -> Value) -> Maybe TxInInfo -> Value
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Value
forall a. Monoid a => a
mempty (TxOut -> Value
txOutValue (TxOut -> Value) -> (TxInInfo -> TxOut) -> TxInInfo -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TxInInfo -> TxOut
txInInfoResolved) (Maybe TxInInfo -> Value) -> Maybe TxInInfo -> Value
forall a b. (a -> b) -> a -> b
$ ScriptContext -> Maybe TxInInfo
findOwnInput ScriptContext
ctx
    headOutValue :: Value
headOutValue = TxOut -> Value
txOutValue (TxOut -> Value) -> TxOut -> Value
forall a b. (a -> b) -> a -> b
$ [TxOut] -> TxOut
forall a. [a] -> a
L.head [TxOut]
txInfoOutputs

  subsetScalars :: [Integer]
  subsetScalars :: [SnapshotVersion]
subsetScalars = [TxOut] -> [SnapshotVersion]
txOutsToSubsetScalars [TxOut]
distributedOutputs

  -- CRS reference lookup and membership check.
  -- The newAccumulatorCommitment from the continuing output datum serves as
  -- the proof: checkMembership verifies that the subset elements were correctly
  -- removed from the accumulator.
  checkCRSAndMembership :: Bool
checkCRSAndMembership =
    BuiltinString -> Bool -> Bool
traceIfFalse $(errorCode PartialFanoutMembershipFailed) (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$
      BuiltinByteString
-> TxInfo -> TxOutRef -> (CRSDatum -> Bool) -> Bool
withCRSLookup BuiltinByteString
crsDatumHash TxInfo
txInfo TxOutRef
crsRef ((CRSDatum -> Bool) -> Bool) -> (CRSDatum -> Bool) -> Bool
forall a b. (a -> b) -> a -> b
$ \CRSDatum
crsData ->
        BuiltinBLS12_381_G1_Element
-> BuiltinBLS12_381_G1_Element
-> CRSDatum
-> [SnapshotVersion]
-> Bool
checkMembershipPairing BuiltinBLS12_381_G1_Element
accumulatorCommitment BuiltinBLS12_381_G1_Element
newAccumulatorCommitment CRSDatum
crsData [SnapshotVersion]
subsetScalars
{-# INLINEABLE checkPartialFanout #-}

-- | Verify the final partial fanout transaction. Transitions FanoutProgress → Final:
-- distributes all remaining UTxOs and burns all head tokens.
--
-- Unlike intermediate steps, there is no continuing head output. All distributed
-- UTxOs start at index 0. Tokens must be burned.
--
-- Note: headId, parties, and contestationDeadline are not re-verified explicitly.
-- headId and parties are validated implicitly by mustBurnAllHeadTokens (wrong values
-- would target the wrong token set). contestationDeadline was locked in by earlier
-- checkPartialFanout steps and is trustworthy from the on-chain datum.
checkFinalPartialFanout ::
  BuiltinByteString ->
  ScriptContext ->
  -- | FanoutProgress state before the final fanout
  FanoutProgressDatum ->
  -- | Number of outputs to distribute
  Integer ->
  -- | Membership proof (quotient commitment G1 element)
  BuiltinBLS12_381_G1_Element ->
  -- | Reference input containing CRS
  TxOutRef ->
  Bool
checkFinalPartialFanout :: BuiltinByteString
-> ScriptContext
-> FanoutProgressDatum
-> SnapshotVersion
-> BuiltinBLS12_381_G1_Element
-> TxOutRef
-> Bool
checkFinalPartialFanout BuiltinByteString
crsDatumHash ctx :: ScriptContext
ctx@ScriptContext{scriptContextTxInfo :: ScriptContext -> TxInfo
scriptContextTxInfo = TxInfo
txInfo} FanoutProgressDatum
progressDatum SnapshotVersion
numberOfPartialOutputs BuiltinBLS12_381_G1_Element
proof TxOutRef
crsRef =
  Bool
mustHaveOutputs
    Bool -> Bool -> Bool
&& MintValue -> CurrencySymbol -> [Party] -> Bool
mustBurnAllHeadTokens MintValue
minted CurrencySymbol
headId [Party]
parties
    Bool -> Bool -> Bool
&& TxInfo -> POSIXTime -> Bool
afterContestationDeadline TxInfo
txInfo POSIXTime
contestationDeadline
    Bool -> Bool -> Bool
&& Bool
checkCRSAndMembership
    Bool -> Bool -> Bool
&& Bool
mustConserveValue
 where
  FanoutProgressDatum{CurrencySymbol
$sel:headId:FanoutProgressDatum :: FanoutProgressDatum -> CurrencySymbol
headId :: CurrencySymbol
headId, [Party]
$sel:parties:FanoutProgressDatum :: FanoutProgressDatum -> [Party]
parties :: [Party]
parties, POSIXTime
$sel:contestationDeadline:FanoutProgressDatum :: FanoutProgressDatum -> POSIXTime
contestationDeadline :: POSIXTime
contestationDeadline, BuiltinBLS12_381_G1_Element
$sel:accumulatorCommitment:FanoutProgressDatum :: FanoutProgressDatum -> BuiltinBLS12_381_G1_Element
accumulatorCommitment :: BuiltinBLS12_381_G1_Element
accumulatorCommitment, SnapshotVersion
$sel:headAdaOverhead:FanoutProgressDatum :: FanoutProgressDatum -> SnapshotVersion
headAdaOverhead :: SnapshotVersion
headAdaOverhead} = FanoutProgressDatum
progressDatum

  minted :: MintValue
minted = TxInfo -> MintValue
txInfoMint TxInfo
txInfo

  TxInfo{[TxOut]
txInfoOutputs :: TxInfo -> [TxOut]
txInfoOutputs :: [TxOut]
txInfoOutputs} = TxInfo
txInfo

  -- Guard against numberOfPartialOutputs = 0: with an empty subset the KZG check
  -- degenerates to e(A,G2) = e(proof,G2), which passes whenever proof = A. Since A
  -- is public (from the datum), any third party could satisfy the check with zero
  -- distributed outputs and route all head ADA to themselves under the strict equality value check.
  mustHaveOutputs :: Bool
mustHaveOutputs =
    BuiltinString -> Bool -> Bool
traceIfFalse $(errorCode FinalPartialFanoutZeroOutputs) (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$
      SnapshotVersion
numberOfPartialOutputs SnapshotVersion -> SnapshotVersion -> Bool
forall a. Ord a => a -> a -> Bool
> SnapshotVersion
0

  distributedOutputs :: [TxOut]
distributedOutputs = SnapshotVersion -> [TxOut] -> [TxOut]
forall a. SnapshotVersion -> [a] -> [a]
L.take SnapshotVersion
numberOfPartialOutputs [TxOut]
txInfoOutputs

  -- Strict equality: distributed outputs + burned tokens + fixed overhead must equal
  -- the full head input value. isG1Generator is omitted for the same reason as in
  -- headIsFinalizedWith — pre-settled UTxOs may remain in the accumulator.
  mustConserveValue :: Bool
mustConserveValue =
    BuiltinString -> Bool -> Bool
traceIfFalse $(errorCode HeadValueIsNotPreserved) (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$
      Value
headInValue
        Value -> Value -> Bool
forall a. Eq a => a -> a -> Bool
== (TxOut -> Value) -> [TxOut] -> Value
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
F.foldMap TxOut -> Value
txOutValue [TxOut]
distributedOutputs
        Value -> Value -> Value
forall a. Semigroup a => a -> a -> a
<> MintValue -> Value
mintValueBurned MintValue
minted
        Value -> Value -> Value
forall a. Semigroup a => a -> a -> a
<> CurrencySymbol -> TokenName -> SnapshotVersion -> Value
singleton CurrencySymbol
adaSymbol TokenName
adaToken SnapshotVersion
headAdaOverhead
   where
    headInValue :: Value
headInValue = Value -> (TxInInfo -> Value) -> Maybe TxInInfo -> Value
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Value
forall a. Monoid a => a
mempty (TxOut -> Value
txOutValue (TxOut -> Value) -> (TxInInfo -> TxOut) -> TxInInfo -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TxInInfo -> TxOut
txInInfoResolved) (Maybe TxInInfo -> Value) -> Maybe TxInInfo -> Value
forall a b. (a -> b) -> a -> b
$ ScriptContext -> Maybe TxInInfo
findOwnInput ScriptContext
ctx

  subsetScalars :: [Integer]
  subsetScalars :: [SnapshotVersion]
subsetScalars = [TxOut] -> [SnapshotVersion]
txOutsToSubsetScalars [TxOut]
distributedOutputs

  checkCRSAndMembership :: Bool
checkCRSAndMembership =
    BuiltinString -> Bool -> Bool
traceIfFalse $(errorCode FinalPartialFanoutMembershipFailed) (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$
      BuiltinByteString
-> TxInfo -> TxOutRef -> (CRSDatum -> Bool) -> Bool
withCRSLookup BuiltinByteString
crsDatumHash TxInfo
txInfo TxOutRef
crsRef ((CRSDatum -> Bool) -> Bool) -> (CRSDatum -> Bool) -> Bool
forall a b. (a -> b) -> a -> b
$ \CRSDatum
crsData ->
        BuiltinBLS12_381_G1_Element
-> BuiltinBLS12_381_G1_Element
-> CRSDatum
-> [SnapshotVersion]
-> Bool
checkMembershipPairing BuiltinBLS12_381_G1_Element
accumulatorCommitment BuiltinBLS12_381_G1_Element
proof CRSDatum
crsData [SnapshotVersion]
subsetScalars
{-# INLINEABLE checkFinalPartialFanout #-}

--------------------------------------------------------------------------------
-- Helpers
--------------------------------------------------------------------------------

isG1Generator :: BuiltinBLS12_381_G1_Element -> Bool
isG1Generator :: BuiltinBLS12_381_G1_Element -> Bool
isG1Generator BuiltinBLS12_381_G1_Element
g = BuiltinBLS12_381_G1_Element -> BuiltinByteString
Builtins.bls12_381_G1_compress BuiltinBLS12_381_G1_Element
g BuiltinByteString -> BuiltinByteString -> Bool
forall a. Eq a => a -> a -> Bool
== BuiltinByteString
Builtins.bls12_381_G1_compressed_generator
{-# INLINEABLE isG1Generator #-}

makeContestationDeadline :: ContestationPeriod -> ScriptContext -> POSIXTime
makeContestationDeadline :: ContestationPeriod -> ScriptContext -> POSIXTime
makeContestationDeadline ContestationPeriod
cperiod ScriptContext{TxInfo
scriptContextTxInfo :: ScriptContext -> TxInfo
scriptContextTxInfo :: TxInfo
scriptContextTxInfo} =
  case Interval POSIXTime -> UpperBound POSIXTime
forall a. Interval a -> UpperBound a
ivTo (TxInfo -> Interval POSIXTime
txInfoValidRange TxInfo
scriptContextTxInfo) of
    UpperBound (Finite POSIXTime
time) Bool
_ -> POSIXTime -> ContestationPeriod -> POSIXTime
addContestationPeriod POSIXTime
time ContestationPeriod
cperiod
    UpperBound POSIXTime
_ -> BuiltinString -> POSIXTime
forall a. BuiltinString -> a
traceError $(errorCode CloseNoUpperBoundDefined)
{-# INLINEABLE makeContestationDeadline #-}

-- | This is safe only because usually Head transaction only consume one input.
getHeadInput :: ScriptContext -> TxInInfo
getHeadInput :: ScriptContext -> TxInInfo
getHeadInput ScriptContext
ctx = case ScriptContext -> Maybe TxInInfo
findOwnInput ScriptContext
ctx of
  Maybe TxInInfo
Nothing -> BuiltinString -> TxInInfo
forall a. BuiltinString -> a
traceError $(errorCode ScriptNotSpendingAHeadInput)
  Just TxInInfo
x -> TxInInfo
x
{-# INLINEABLE getHeadInput #-}

getHeadAddress :: ScriptContext -> Address
getHeadAddress :: ScriptContext -> Address
getHeadAddress = TxOut -> Address
txOutAddress (TxOut -> Address)
-> (ScriptContext -> TxOut) -> ScriptContext -> Address
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TxInInfo -> TxOut
txInInfoResolved (TxInInfo -> TxOut)
-> (ScriptContext -> TxInInfo) -> ScriptContext -> TxOut
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ScriptContext -> TxInInfo
getHeadInput
{-# INLINEABLE getHeadAddress #-}

mustNotChangeParameters ::
  ([Party], [Party]) ->
  (ContestationPeriod, ContestationPeriod) ->
  (CurrencySymbol, CurrencySymbol) ->
  (DepositPeriod, DepositPeriod) ->
  Bool
mustNotChangeParameters :: ([Party], [Party])
-> (ContestationPeriod, ContestationPeriod)
-> (CurrencySymbol, CurrencySymbol)
-> (DepositPeriod, DepositPeriod)
-> Bool
mustNotChangeParameters ([Party]
parties', [Party]
parties) (ContestationPeriod
contestationPeriod', ContestationPeriod
contestationPeriod) (CurrencySymbol
headId', CurrencySymbol
headId) (DepositPeriod
depositPeriod', DepositPeriod
depositPeriod) =
  BuiltinString -> Bool -> Bool
traceIfFalse $(errorCode ChangedParameters) (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$
    [Party]
parties' [Party] -> [Party] -> Bool
forall a. Eq a => a -> a -> Bool
== [Party]
parties
      Bool -> Bool -> Bool
&& ContestationPeriod
contestationPeriod' ContestationPeriod -> ContestationPeriod -> Bool
forall a. Eq a => a -> a -> Bool
== ContestationPeriod
contestationPeriod
      Bool -> Bool -> Bool
&& CurrencySymbol
headId' CurrencySymbol -> CurrencySymbol -> Bool
forall a. Eq a => a -> a -> Bool
== CurrencySymbol
headId
      Bool -> Bool -> Bool
&& DepositPeriod
depositPeriod' DepositPeriod -> DepositPeriod -> Bool
forall a. Eq a => a -> a -> Bool
== DepositPeriod
depositPeriod
{-# INLINEABLE mustNotChangeParameters #-}

mustPreserveHeadAdaOverhead :: Integer -> Integer -> Bool
mustPreserveHeadAdaOverhead :: SnapshotVersion -> SnapshotVersion -> Bool
mustPreserveHeadAdaOverhead SnapshotVersion
overhead SnapshotVersion
overhead' =
  BuiltinString -> Bool -> Bool
traceIfFalse $(errorCode ChangedHeadAdaOverhead) (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$
    SnapshotVersion
overhead' SnapshotVersion -> SnapshotVersion -> Bool
forall a. Eq a => a -> a -> Bool
== SnapshotVersion
overhead
{-# INLINEABLE mustPreserveHeadAdaOverhead #-}

-- XXX: We might not need to distinguish between the three cases here.
mustBeSignedByParticipant ::
  ScriptContext ->
  CurrencySymbol ->
  Bool
mustBeSignedByParticipant :: ScriptContext -> CurrencySymbol -> Bool
mustBeSignedByParticipant ScriptContext{scriptContextTxInfo :: ScriptContext -> TxInfo
scriptContextTxInfo = TxInfo
txInfo} CurrencySymbol
headCurrencySymbol =
  case PubKeyHash -> BuiltinByteString
getPubKeyHash (PubKeyHash -> BuiltinByteString)
-> [PubKeyHash] -> [BuiltinByteString]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TxInfo -> [PubKeyHash]
txInfoSignatories TxInfo
txInfo of
    [BuiltinByteString
signer] ->
      BuiltinString -> Bool -> Bool
traceIfFalse $(errorCode SignerIsNotAParticipant) (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$
        BuiltinByteString
signer BuiltinByteString -> [BuiltinByteString] -> Bool
forall a. Eq a => a -> [a] -> Bool
`L.elem` (TokenName -> BuiltinByteString
unTokenName (TokenName -> BuiltinByteString)
-> [TokenName] -> [BuiltinByteString]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [TokenName]
participationTokens)
    [] ->
      BuiltinString -> Bool
forall a. BuiltinString -> a
traceError $(errorCode NoSigners)
    [BuiltinByteString]
_ ->
      BuiltinString -> Bool
forall a. BuiltinString -> a
traceError $(errorCode TooManySigners)
 where
  participationTokens :: [TokenName]
participationTokens = [TxInInfo] -> [TokenName]
loop (TxInfo -> [TxInInfo]
txInfoInputs TxInfo
txInfo)
  loop :: [TxInInfo] -> [TokenName]
loop = \case
    [] -> []
    (TxInInfo{TxOut
txInInfoResolved :: TxInInfo -> TxOut
txInInfoResolved :: TxOut
txInInfoResolved} : [TxInInfo]
rest) ->
      CurrencySymbol -> Value -> [TokenName]
findParticipationTokens CurrencySymbol
headCurrencySymbol (TxOut -> Value
txOutValue TxOut
txInInfoResolved) [TokenName] -> [TokenName] -> [TokenName]
forall a. [a] -> [a] -> [a]
L.++ [TxInInfo] -> [TokenName]
loop [TxInInfo]
rest
{-# INLINEABLE mustBeSignedByParticipant #-}

findParticipationTokens :: CurrencySymbol -> Value -> [TokenName]
findParticipationTokens :: CurrencySymbol -> Value -> [TokenName]
findParticipationTokens CurrencySymbol
headCurrency (Value Map CurrencySymbol (Map TokenName SnapshotVersion)
val) =
  case Map TokenName SnapshotVersion -> [(TokenName, SnapshotVersion)]
forall k v. Map k v -> [(k, v)]
AssocMap.toList (Map TokenName SnapshotVersion -> [(TokenName, SnapshotVersion)])
-> Maybe (Map TokenName SnapshotVersion)
-> Maybe [(TokenName, SnapshotVersion)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CurrencySymbol
-> Map CurrencySymbol (Map TokenName SnapshotVersion)
-> Maybe (Map TokenName SnapshotVersion)
forall k v. Eq k => k -> Map k v -> Maybe v
AssocMap.lookup CurrencySymbol
headCurrency Map CurrencySymbol (Map TokenName SnapshotVersion)
val of
    Just [(TokenName, SnapshotVersion)]
tokens ->
      ((TokenName, SnapshotVersion) -> Maybe TokenName)
-> [(TokenName, SnapshotVersion)] -> [TokenName]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (\(TokenName
tokenName, SnapshotVersion
n) -> if SnapshotVersion
n SnapshotVersion -> SnapshotVersion -> Bool
forall a. Eq a => a -> a -> Bool
== SnapshotVersion
1 then TokenName -> Maybe TokenName
forall a. a -> Maybe a
Just TokenName
tokenName else Maybe TokenName
forall a. Maybe a
Nothing) [(TokenName, SnapshotVersion)]
tokens
    Maybe [(TokenName, SnapshotVersion)]
_ ->
      []
{-# INLINEABLE findParticipationTokens #-}

headOutputDatum :: ScriptContext -> Datum
headOutputDatum :: ScriptContext -> Datum
headOutputDatum ScriptContext
ctx =
  case TxInfo -> [TxOut]
txInfoOutputs TxInfo
txInfo of
    (TxOut
o : [TxOut]
_)
      | TxOut -> Address
txOutAddress TxOut
o Address -> Address -> Bool
forall a. Eq a => a -> a -> Bool
== Address
headAddress -> TxOut -> Datum
getTxOutDatum TxOut
o
    [TxOut]
_ -> BuiltinString -> Datum
forall a. BuiltinString -> a
traceError $(errorCode NotPayingToHead)
 where
  headAddress :: Address
headAddress = ScriptContext -> Address
getHeadAddress ScriptContext
ctx

  ScriptContext{scriptContextTxInfo :: ScriptContext -> TxInfo
scriptContextTxInfo = TxInfo
txInfo} = ScriptContext
ctx
{-# INLINEABLE headOutputDatum #-}

getTxOutDatum :: TxOut -> Datum
getTxOutDatum :: TxOut -> Datum
getTxOutDatum TxOut
o =
  case TxOut -> OutputDatum
txOutDatum TxOut
o of
    OutputDatum
NoOutputDatum -> BuiltinString -> Datum
forall a. BuiltinString -> a
traceError $(errorCode NoOutputDatumError)
    OutputDatumHash DatumHash
_dh -> BuiltinString -> Datum
forall a. BuiltinString -> a
traceError $(errorCode UnexpectedNonInlineDatum)
    OutputDatum Datum
d -> Datum
d
{-# INLINEABLE getTxOutDatum #-}

-- | Verify the multi-signature of a snapshot using given constituents 'headId',
-- 'version', 'number', and 'accumulatorHash'. See 'SignableRepresentation Snapshot'
-- for more details.
verifySnapshotSignature :: [Party] -> (CurrencySymbol, SnapshotVersion, SnapshotNumber, Hash, Hash, Hash) -> [Signature] -> Bool
verifySnapshotSignature :: [Party]
-> (CurrencySymbol, SnapshotVersion, SnapshotVersion,
    BuiltinByteString, BuiltinByteString, BuiltinByteString)
-> [BuiltinByteString]
-> Bool
verifySnapshotSignature [Party]
parties (CurrencySymbol, SnapshotVersion, SnapshotVersion,
 BuiltinByteString, BuiltinByteString, BuiltinByteString)
msg [BuiltinByteString]
sigs =
  BuiltinString -> Bool -> Bool
traceIfFalse $(errorCode SignatureVerificationFailed) (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$
    [Party] -> SnapshotVersion
forall a. [a] -> SnapshotVersion
L.length [Party]
parties SnapshotVersion -> SnapshotVersion -> Bool
forall a. Eq a => a -> a -> Bool
== [BuiltinByteString] -> SnapshotVersion
forall a. [a] -> SnapshotVersion
L.length [BuiltinByteString]
sigs
      Bool -> Bool -> Bool
&& ((Party, BuiltinByteString) -> Bool)
-> [(Party, BuiltinByteString)] -> Bool
forall a. (a -> Bool) -> [a] -> Bool
L.all ((Party -> BuiltinByteString -> Bool)
-> (Party, BuiltinByteString) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((Party -> BuiltinByteString -> Bool)
 -> (Party, BuiltinByteString) -> Bool)
-> (Party -> BuiltinByteString -> Bool)
-> (Party, BuiltinByteString)
-> Bool
forall a b. (a -> b) -> a -> b
$ (CurrencySymbol, SnapshotVersion, SnapshotVersion,
 BuiltinByteString, BuiltinByteString, BuiltinByteString)
-> Party -> BuiltinByteString -> Bool
verifyPartySignature (CurrencySymbol, SnapshotVersion, SnapshotVersion,
 BuiltinByteString, BuiltinByteString, BuiltinByteString)
msg) ([Party] -> [BuiltinByteString] -> [(Party, BuiltinByteString)]
forall a b. [a] -> [b] -> [(a, b)]
L.zip [Party]
parties [BuiltinByteString]
sigs)
{-# INLINEABLE verifySnapshotSignature #-}

-- | Verify individual party signature of a snapshot. See
-- 'SignableRepresentation Snapshot' for more details.
verifyPartySignature :: (CurrencySymbol, SnapshotVersion, SnapshotNumber, Hash, Hash, Hash) -> Party -> Signature -> Bool
verifyPartySignature :: (CurrencySymbol, SnapshotVersion, SnapshotVersion,
 BuiltinByteString, BuiltinByteString, BuiltinByteString)
-> Party -> BuiltinByteString -> Bool
verifyPartySignature (CurrencySymbol
headId, SnapshotVersion
snapshotVersion, SnapshotVersion
snapshotNumber, BuiltinByteString
accumulatorHash, BuiltinByteString
decommitOutputsHash, BuiltinByteString
commitOutputsHash) Party
party =
  BuiltinByteString -> BuiltinByteString -> BuiltinByteString -> Bool
verifyEd25519Signature (Party -> BuiltinByteString
vkey Party
party) BuiltinByteString
message
 where
  message :: BuiltinByteString
message =
    BuiltinData -> BuiltinByteString
Builtins.serialiseData (CurrencySymbol -> BuiltinData
forall a. ToData a => a -> BuiltinData
toBuiltinData CurrencySymbol
headId)
      BuiltinByteString -> BuiltinByteString -> BuiltinByteString
forall a. Semigroup a => a -> a -> a
<> BuiltinData -> BuiltinByteString
Builtins.serialiseData (SnapshotVersion -> BuiltinData
forall a. ToData a => a -> BuiltinData
toBuiltinData SnapshotVersion
snapshotVersion)
      BuiltinByteString -> BuiltinByteString -> BuiltinByteString
forall a. Semigroup a => a -> a -> a
<> BuiltinData -> BuiltinByteString
Builtins.serialiseData (SnapshotVersion -> BuiltinData
forall a. ToData a => a -> BuiltinData
toBuiltinData SnapshotVersion
snapshotNumber)
      BuiltinByteString -> BuiltinByteString -> BuiltinByteString
forall a. Semigroup a => a -> a -> a
<> BuiltinData -> BuiltinByteString
Builtins.serialiseData (BuiltinByteString -> BuiltinData
forall a. ToData a => a -> BuiltinData
toBuiltinData BuiltinByteString
accumulatorHash)
      BuiltinByteString -> BuiltinByteString -> BuiltinByteString
forall a. Semigroup a => a -> a -> a
<> BuiltinData -> BuiltinByteString
Builtins.serialiseData (BuiltinByteString -> BuiltinData
forall a. ToData a => a -> BuiltinData
toBuiltinData BuiltinByteString
decommitOutputsHash)
      BuiltinByteString -> BuiltinByteString -> BuiltinByteString
forall a. Semigroup a => a -> a -> a
<> BuiltinData -> BuiltinByteString
Builtins.serialiseData (BuiltinByteString -> BuiltinData
forall a. ToData a => a -> BuiltinData
toBuiltinData BuiltinByteString
commitOutputsHash)
{-# INLINEABLE verifyPartySignature #-}

unappliedValidator :: CompiledCode (BuiltinByteString -> ValidatorType)
unappliedValidator :: CompiledCode (BuiltinByteString -> ValidatorType)
unappliedValidator =
  $$(PlutusTx.compile [||wrap . headValidator||])
 where
  wrap :: (DatumType -> Input -> ScriptContext -> Bool) -> ValidatorType
wrap = forall datum redeemer.
(UnsafeFromData datum, UnsafeFromData redeemer) =>
(datum -> redeemer -> ScriptContext -> Bool) -> ValidatorType
wrapValidator @DatumType @RedeemerType

compiledValidator :: CompiledCode ValidatorType
compiledValidator :: CompiledCode ValidatorType
compiledValidator =
  CompiledCode (BuiltinByteString -> ValidatorType)
unappliedValidator
    CompiledCode (BuiltinByteString -> ValidatorType)
-> CompiledCodeIn DefaultUni DefaultFun BuiltinByteString
-> CompiledCode ValidatorType
forall (uni :: * -> *) fun a b.
(Closed uni, Everywhere uni Flat, Flat fun, Pretty fun,
 Everywhere uni PrettyConst,
 PrettyBy RenderContext (SomeTypeIn uni)) =>
CompiledCodeIn uni fun (a -> b)
-> CompiledCodeIn uni fun a -> CompiledCodeIn uni fun b
`PlutusTx.unsafeApplyCode` Version
-> BuiltinByteString
-> CompiledCodeIn DefaultUni DefaultFun BuiltinByteString
forall (uni :: * -> *) a fun.
(Lift uni a, GEq uni, Everywhere uni Eq, ThrowableBuiltins uni fun,
 Typecheckable uni fun, CaseBuiltin uni,
 Default (CostingPart uni fun), Default (BuiltinsInfo uni fun),
 Default (RewriteRules uni fun), Hashable fun) =>
Version -> a -> CompiledCodeIn uni fun a
PlutusTx.liftCode Version
plcVersion110 BuiltinByteString
canonicalCRSDatumHash

-- | BLAKE2b-256 of the canonical CRS datum: the published EIP-4844 trusted setup
-- (first 'KZG.defaultItems' G2 points) hashed by 'hashCRSDatum'. Baked into the
-- validator so every fanout rejects a reference input carrying any other
-- powers-of-tau setup. Computed directly from the embedded setup — no hardcoded value.
canonicalCRSDatumHash :: BuiltinByteString
canonicalCRSDatumHash :: BuiltinByteString
canonicalCRSDatumHash = CRSDatum -> BuiltinByteString
hashCRSDatum CRSDatum
KZG.canonicalG2Points

validatorScript :: PlutusScript
validatorScript :: PlutusScript
validatorScript = ShortByteString -> PlutusScript
PlutusScriptSerialised (ShortByteString -> PlutusScript)
-> ShortByteString -> PlutusScript
forall a b. (a -> b) -> a -> b
$ CompiledCode ValidatorType -> ShortByteString
forall a. CompiledCode a -> ShortByteString
serialiseCompiledCode CompiledCode ValidatorType
compiledValidator

decodeHeadOutputClosedDatum :: ScriptContext -> ClosedDatum
decodeHeadOutputClosedDatum :: ScriptContext -> ClosedDatum
decodeHeadOutputClosedDatum ScriptContext
ctx =
  -- XXX: fromBuiltinData is super big (and also expensive?)
  case forall a. FromData a => BuiltinData -> Maybe a
fromBuiltinData @DatumType (BuiltinData -> Maybe DatumType) -> BuiltinData -> Maybe DatumType
forall a b. (a -> b) -> a -> b
$ Datum -> BuiltinData
getDatum (ScriptContext -> Datum
headOutputDatum ScriptContext
ctx) of
    Just (Closed ClosedDatum
closedDatum) -> ClosedDatum
closedDatum
    Maybe DatumType
_ -> BuiltinString -> ClosedDatum
forall a. BuiltinString -> a
traceError $(errorCode WrongStateInOutputDatum)
{-# INLINEABLE decodeHeadOutputClosedDatum #-}

decodeHeadOutputFanoutProgressDatum :: ScriptContext -> FanoutProgressDatum
decodeHeadOutputFanoutProgressDatum :: ScriptContext -> FanoutProgressDatum
decodeHeadOutputFanoutProgressDatum ScriptContext
ctx =
  case forall a. FromData a => BuiltinData -> Maybe a
fromBuiltinData @DatumType (BuiltinData -> Maybe DatumType) -> BuiltinData -> Maybe DatumType
forall a b. (a -> b) -> a -> b
$ Datum -> BuiltinData
getDatum (ScriptContext -> Datum
headOutputDatum ScriptContext
ctx) of
    Just (FanoutProgress FanoutProgressDatum
progressDatum) -> FanoutProgressDatum
progressDatum
    Maybe DatumType
_ -> BuiltinString -> FanoutProgressDatum
forall a. BuiltinString -> a
traceError $(errorCode WrongStateInOutputDatum)
{-# INLINEABLE decodeHeadOutputFanoutProgressDatum #-}

decodeHeadOutputOpenDatum :: ScriptContext -> OpenDatum
decodeHeadOutputOpenDatum :: ScriptContext -> OpenDatum
decodeHeadOutputOpenDatum ScriptContext
ctx =
  -- XXX: fromBuiltinData is super big (and also expensive?)
  case forall a. FromData a => BuiltinData -> Maybe a
fromBuiltinData @DatumType (BuiltinData -> Maybe DatumType) -> BuiltinData -> Maybe DatumType
forall a b. (a -> b) -> a -> b
$ Datum -> BuiltinData
getDatum (ScriptContext -> Datum
headOutputDatum ScriptContext
ctx) of
    Just (Open OpenDatum
openDatum) -> OpenDatum
openDatum
    Maybe DatumType
_ -> BuiltinString -> OpenDatum
forall a. BuiltinString -> a
traceError $(errorCode WrongStateInOutputDatum)
{-# INLINEABLE decodeHeadOutputOpenDatum #-}

-- | Check that the lower validity bound of the transaction is strictly after
-- the contestation deadline. Used by all three fanout paths.
afterContestationDeadline :: TxInfo -> POSIXTime -> Bool
afterContestationDeadline :: TxInfo -> POSIXTime -> Bool
afterContestationDeadline TxInfo
txInfo POSIXTime
deadline =
  case Interval POSIXTime -> LowerBound POSIXTime
forall a. Interval a -> LowerBound a
ivFrom (TxInfo -> Interval POSIXTime
txInfoValidRange TxInfo
txInfo) of
    LowerBound (Finite POSIXTime
time) Bool
_ ->
      BuiltinString -> Bool -> Bool
traceIfFalse $(errorCode LowerBoundBeforeContestationDeadline) (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$
        POSIXTime
time POSIXTime -> POSIXTime -> Bool
forall a. Ord a => a -> a -> Bool
> POSIXTime
deadline
    LowerBound POSIXTime
_ -> BuiltinString -> Bool
forall a. BuiltinString -> a
traceError $(errorCode FanoutNoLowerBoundDefined)
{-# INLINEABLE afterContestationDeadline #-}

-- | Find a CRS reference input by 'TxOutRef' and decode its non-empty datum.
-- Errors on missing input, undecoded datum, or empty CRS list.
resolveCRS :: TxInfo -> TxOutRef -> CRSDatum
resolveCRS :: TxInfo -> TxOutRef -> CRSDatum
resolveCRS TxInfo
txInfo TxOutRef
crsRef =
  case (TxInInfo -> Bool) -> [TxInInfo] -> Maybe TxInInfo
forall a. (a -> Bool) -> [a] -> Maybe a
L.find (\TxInInfo
txin -> TxInInfo -> TxOutRef
txInInfoOutRef TxInInfo
txin TxOutRef -> TxOutRef -> Bool
forall a. Eq a => a -> a -> Bool
== TxOutRef
crsRef) (TxInfo -> [TxInInfo]
txInfoReferenceInputs TxInfo
txInfo) of
    Maybe TxInInfo
Nothing -> BuiltinString -> CRSDatum
forall a. BuiltinString -> a
traceError $(errorCode MissingCRSRefInput)
    Just TxInInfo
txInInfo ->
      case forall a. FromData a => BuiltinData -> Maybe a
fromBuiltinData @CRSDatum (BuiltinData -> Maybe CRSDatum) -> BuiltinData -> Maybe CRSDatum
forall a b. (a -> b) -> a -> b
$ Datum -> BuiltinData
getDatum (TxOut -> Datum
getTxOutDatum (TxInInfo -> TxOut
txInInfoResolved TxInInfo
txInInfo)) of
        Just d :: CRSDatum
d@(BuiltinBLS12_381_G2_Element
_ : CRSDatum
_) -> CRSDatum
d
        Maybe CRSDatum
_ -> BuiltinString -> CRSDatum
forall a. BuiltinString -> a
traceError $(errorCode MissingCRSDatum)
{-# INLINEABLE resolveCRS #-}

-- | Hash a CRS datum by its content: BLAKE2b-256 over the concatenation of the
-- compressed G2 points. Binding the datum content is what keeps the membership
-- proof sound — the trusted-setup τ is fixed and public, so any other setup would
-- let a crafted fanout forge proofs.
hashCRSDatum :: CRSDatum -> BuiltinByteString
hashCRSDatum :: CRSDatum -> BuiltinByteString
hashCRSDatum = BuiltinByteString -> BuiltinByteString
Builtins.blake2b_256 (BuiltinByteString -> BuiltinByteString)
-> (CRSDatum -> BuiltinByteString) -> CRSDatum -> BuiltinByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (BuiltinBLS12_381_G2_Element -> BuiltinByteString)
-> CRSDatum -> BuiltinByteString
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
F.foldMap BuiltinBLS12_381_G2_Element -> BuiltinByteString
Builtins.bls12_381_G2_compress
{-# INLINEABLE hashCRSDatum #-}

-- | Look up the CRS datum from a reference input and pass it to a continuation,
-- rejecting any reference input whose datum is not the canonical trusted setup.
withCRSLookup ::
  BuiltinByteString ->
  TxInfo ->
  TxOutRef ->
  (CRSDatum -> Bool) ->
  Bool
withCRSLookup :: BuiltinByteString
-> TxInfo -> TxOutRef -> (CRSDatum -> Bool) -> Bool
withCRSLookup BuiltinByteString
expectedDatumHash TxInfo
txInfo TxOutRef
crsRef CRSDatum -> Bool
cont =
  let crsData :: CRSDatum
crsData = TxInfo -> TxOutRef -> CRSDatum
resolveCRS TxInfo
txInfo TxOutRef
crsRef
   in if CRSDatum -> BuiltinByteString
hashCRSDatum CRSDatum
crsData BuiltinByteString -> BuiltinByteString -> Bool
forall a. Eq a => a -> a -> Bool
/= BuiltinByteString
expectedDatumHash
        then BuiltinString -> Bool
forall a. BuiltinString -> a
traceError $(errorCode InvalidCRSDatum)
        else CRSDatum -> Bool
cont CRSDatum
crsData
{-# INLINEABLE withCRSLookup #-}

-- | Compute the accumulator scalar for each output in the list.
-- Used by all three fanout validators ('headIsFinalizedWith', 'checkPartialFanout',
-- 'checkFinalPartialFanout') to produce subset scalars for 'checkMembershipPairing'.
-- Each scalar is blake2b_224(hashTxOuts [txOut]), which equals
-- blake2b_224(sha2_256(serialised)) because 'hashTxOuts' uses sha2_256 internally
-- (matching what 'Accumulator.addElement' computes off-chain).
txOutsToSubsetScalars :: [TxOut] -> [Integer]
txOutsToSubsetScalars :: [TxOut] -> [SnapshotVersion]
txOutsToSubsetScalars [TxOut]
outputs =
  let elementHash :: TxOut -> BuiltinByteString
elementHash TxOut
txOut = BuiltinByteString -> BuiltinByteString
blake2b_224 ([TxOut] -> BuiltinByteString
hashTxOuts [TxOut
txOut])
   in (TxOut -> SnapshotVersion) -> [TxOut] -> [SnapshotVersion]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ByteOrder -> BuiltinByteString -> SnapshotVersion
Builtins.byteStringToInteger ByteOrder
BigEndian (BuiltinByteString -> SnapshotVersion)
-> (TxOut -> BuiltinByteString) -> TxOut -> SnapshotVersion
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TxOut -> BuiltinByteString
elementHash) [TxOut]
outputs
{-# INLINEABLE txOutsToSubsetScalars #-}