-- | Off-chain differential (real-node bindings): the Agda-extracted §6 handler decisions
-- ("Hydra.Agda.OffChainReference") checked against the REAL 'Hydra.HeadLogic.update' outcomes, not
-- against transcriptions of the figure. This extends 'Hydra.OffChainLeaderSpec' (which binds
-- @leaderRef@ to the real @isLeader@) to three more decisions, closing the figure↔Agda↔Haskell loop:
--
--   * @signEligibleRef@ vs @onOpenNetworkReqSn@: we drive 'update' with a @ReqSn@ over an open state
--     with version v̂ and a settled snapshot ŝ (confirmed = seen, nothing in flight) and binarise the
--     outcome: ACCEPT iff the node reaches the signing continuation ('SnapshotRequested' + an @AckSn@
--     effect). The node splits the figure's single @require@ into an Error (number:
--     'ReqSnNumberInvalid', leader: 'ReqSnNotLeader') and a Wait (version: 'WaitOnSnapshotVersion',
--     so a follower behind on the version bump does not drop the message); Error and Wait both map to
--     non-accept. The reference's leader input is resolved by the EXTRACTED @leaderRef@ (itself bound
--     to the real @isLeader@ in 'Hydra.OffChainLeaderSpec'), so the composed decision is fully Agda-derived.
--
--   * @reqDecEligibleRef@ vs @onOpenNetworkReqDec@: ACCEPT iff the node records the decommit
--     ('DecommitRecorded'). A PENDING deposit makes the node WAIT ('WaitOnUnresolvedCommit') at
--     ttl > 0, and so does an in-flight decommit ('WaitOnNotApplicableDecommitTx' with
--     'DecommitAlreadyInFlight'); both are non-accept. The commit axis is the reference's
--     'HsPendingCommit', not a Bool, so this test cannot decide which commits count: an expired or
--     already-recovered deposit is a state the node reaches (it clears @currentDepositTxId@ on
--     neither) and the reference is what says those do not block.
--
--   * @reqSnNotBothRef@ / @reqSnDecommitOutputsRef@ / @reqSnDepositSettledRef@ vs
--     @onOpenNetworkReqSn@'s incremental-action guards: a request carrying both a deposit and a
--     decommit is 'ReqSnBothCommitAndDecommit'; a decommit producing no outputs is
--     'ReqSnDecommitNoOutputs'; and settling a same-version pending commit requires the request to
--     name the deposit bound into the confirmed snapshot by tx-id ('ReqSnCommitNotSettled'
--     otherwise) - the look-alike-deposit case, where content matches and only identity differs.
--
--   * @depositStatusRef@ vs the deposit-status transition the node applies on a chain 'Tick'
--     ('onOpenChainTick' via @determineNextDepositStatus@): starting from a fresh Inactive deposit,
--     one tick at time t yields 'DepositExpired' / 'DepositActivated' / no status event, mapping to
--     ExpiredS / ActiveS / InactiveS.
--
--   * @notAlreadySignedRef@ vs @onOpenNetworkAckSn@'s @requireNotSignedYet@: over a directly
--     constructed in-flight 'SeenSnapshot' whose signatories map holds REAL signatures, an @AckSn@
--     from a sender already in the map is the node's 'SnapshotAlreadySigned'; a fresh sender is not.
--
--   * @allSignedRef@ vs the round completion of @onOpenNetworkAckSn@: a fresh sender's ack CONFIRMS
--     (the node aggregates the real signatures in order and verifies the real multisignature before
--     emitting 'SnapshotConfirmed') exactly when it completes the n-of-n signer set; the composed
--     decision is @notAlreadySignedRef ∧ allSignedRef (sender ∷ Σ̂)@.
--
--   * @contestEligibleRef@ vs @onOpenChainCloseTx@: observing a close of snapshot s_c while our
--     confirmed snapshot is S̄.s posts a 'ContestTx' exactly when S̄.s > s_c.
--
-- Domain note (deposit status): the extracted decision uses Nat truncated subtraction for
-- @deadline − T_deposit@ whereas the node subtracts over 'UTCTime'; the two agree whenever
-- @deadline ≥ T_deposit@, which the protocol guarantees (an observed deposit deadline sits a full
-- deposit period after creation). The property therefore quantifies over that domain, with all times
-- as whole POSIX seconds (exact in both representations).
--
-- Scope note (ackSn): the extracted guards model the COUNTING decisions (who signed, n-of-n); the
-- collected signatures themselves are held healthy, exactly as the on-chain reference holds crypto
-- conjuncts healthy. The real node additionally verifies the aggregate multisignature at
-- confirmation; a corrupt collected signature makes it reject ('InvalidMultisignature') where the
-- counting reference alone would accept, demonstrated as a validator-only rejection below.
module Hydra.OffChainAgreementSpec (spec) where

import Hydra.Prelude
import Test.Hydra.Prelude

import Data.Map.Strict qualified as Map
import Data.Time.Clock.POSIX (posixSecondsToUTCTime)
import Hydra.API.ServerOutput (DecommitInvalidReason (..))
import Hydra.Agda.OffChainReference (
  HsDepositStatus (..),
  HsPendingCommit (..),
  allSignedRef,
  contestEligibleRef,
  depositStatusRef,
  leaderRef,
  notAlreadySignedRef,
  reqDecEligibleRef,
  reqSnDecommitOutputsRef,
  reqSnDepositSettledRef,
  reqSnNotBothRef,
  signEligibleRef,
 )
import Hydra.Chain (ChainEvent (..), OnChainTx (..), PostChainTx (..))
import Hydra.HeadLogic (
  CoordinatedHeadState (..),
  Effect (..),
  Input (..),
  LogicError (..),
  Outcome (..),
  RequirementFailure (..),
  SeenSnapshot (..),
  StateChanged (..),
  WaitReason (..),
  mkSeenSnapshot,
  update,
 )
import Hydra.HeadLogicSpec (assertWait, inOpenState, inOpenState', observeTx, receiveMessageFrom, testSnapshot)
import Hydra.Ledger.Simple (SimpleTx (..), simpleLedger)
import Hydra.Network.Message (Message (..))
import Hydra.Node.Environment (Environment (..))
import Hydra.Node.State (Deposit (..), DepositStatus (..), NodeState (..))
import Hydra.Options (defaultContestationPeriod, defaultDepositActivation, defaultDepositPeriod, defaultUnsyncedPeriod)
import Hydra.Prelude qualified as Prelude
import Hydra.Tx.Accumulator qualified as Accumulator
import Hydra.Tx.Crypto (HydraKey, Signature, SigningKey, aggregate, sign)
import Hydra.Tx.IsTx (TxIdType, UTxOType)
import Hydra.Tx.Party (Party)
import Hydra.Tx.Secret (Secret)
import Hydra.Tx.Snapshot (ConfirmedSnapshot (..), Snapshot (..))
import Test.Hydra.Ledger.Simple (utxoRef)
import Test.Hydra.Tx.Fixture (alice, aliceSk, bob, bobSk, carol, carolSk, deriveOnChainId, testHeadId)
import Test.QuickCheck (choose, conjoin, counterexample, elements, forAll, sublistOf, (===))

threeParties :: [Party]
threeParties :: [Party]
threeParties = [Party
alice, Party
bob, Party
carol]

-- The node under test is alice; the handlers' guards concern the SENDER, so one env suffices.
aliceEnv :: Environment
aliceEnv :: Environment
aliceEnv =
  Environment
    { $sel:party:Environment :: Party
party = Party
alice
    , $sel:signingKey:Environment :: Secret (SigningKey HydraKey)
signingKey = Secret (SigningKey HydraKey)
aliceSk
    , $sel:otherParties:Environment :: [Party]
otherParties = [Party
bob, Party
carol]
    , $sel:contestationPeriod:Environment :: ContestationPeriod
contestationPeriod = ContestationPeriod
defaultContestationPeriod
    , $sel:depositPeriod:Environment :: DepositPeriod
depositPeriod = DepositPeriod
defaultDepositPeriod
    , $sel:depositActivation:Environment :: DepositPeriod
depositActivation = DepositPeriod
defaultDepositActivation
    , $sel:unsyncedPeriod:Environment :: UnsyncedPeriod
unsyncedPeriod = UnsyncedPeriod
defaultUnsyncedPeriod
    , $sel:participants:Environment :: [OnChainId]
participants = Party -> OnChainId
deriveOnChainId (Party -> OnChainId) -> [Party] -> [OnChainId]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Party]
threeParties
    , $sel:configuredPeers:Environment :: Text
configuredPeers = Text
""
    }

-- 'update' ignores the wall clock on the NetworkInput path; any fixed time works.
time0 :: UTCTime
time0 :: UTCTime
time0 = POSIXTime -> UTCTime
posixSecondsToUTCTime POSIXTime
0

posixTime :: Integer -> UTCTime
posixTime :: SimpleId -> UTCTime
posixTime = POSIXTime -> UTCTime
posixSecondsToUTCTime (POSIXTime -> UTCTime)
-> (SimpleId -> POSIXTime) -> SimpleId -> UTCTime
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SimpleId -> POSIXTime
forall a. Num a => SimpleId -> a
fromInteger

-- ── reqSn signing eligibility ────────────────────────────────────────────────────────────────────────

-- Open state with version v̂ and a settled snapshot ŝ: confirmed = seen (nothing in flight), so the
-- handler's wait-guards outside the modeled decision (ŝ = S̄.s) hold by construction.
reqSnState :: Integer -> Integer -> NodeState SimpleTx
reqSnState :: SimpleId -> SimpleId -> NodeState SimpleTx
reqSnState SimpleId
vHat SimpleId
sHat =
  [Party] -> CoordinatedHeadState SimpleTx -> NodeState SimpleTx
inOpenState' [Party]
threeParties (CoordinatedHeadState SimpleTx -> NodeState SimpleTx)
-> CoordinatedHeadState SimpleTx -> NodeState SimpleTx
forall a b. (a -> b) -> a -> b
$
    CoordinatedHeadState
      { $sel:localUTxO:CoordinatedHeadState :: UTxOType SimpleTx
localUTxO = Set SimpleTxOut
UTxOType SimpleTx
forall a. Monoid a => a
mempty
      , $sel:allTxs:CoordinatedHeadState :: Map (TxIdType SimpleTx) SimpleTx
allTxs = Map SimpleId SimpleTx
Map (TxIdType SimpleTx) SimpleTx
forall a. Monoid a => a
mempty
      , $sel:localTxs:CoordinatedHeadState :: Seq SimpleTx
localTxs = Seq SimpleTx
forall a. Monoid a => a
mempty
      , $sel:confirmedSnapshot:CoordinatedHeadState :: ConfirmedSnapshot SimpleTx
confirmedSnapshot =
          if SimpleId
sHat SimpleId -> SimpleId -> Bool
forall a. Eq a => a -> a -> Bool
== SimpleId
0
            then HeadId -> ConfirmedSnapshot SimpleTx
forall tx. HeadId -> ConfirmedSnapshot tx
InitialSnapshot HeadId
testHeadId
            else Snapshot SimpleTx
-> MultiSignature (Snapshot SimpleTx) -> ConfirmedSnapshot SimpleTx
forall tx.
Snapshot tx -> MultiSignature (Snapshot tx) -> ConfirmedSnapshot tx
ConfirmedSnapshot (SnapshotNumber
-> SnapshotVersion
-> [SimpleTx]
-> UTxOType SimpleTx
-> Snapshot SimpleTx
forall tx.
IsTx tx =>
SnapshotNumber
-> SnapshotVersion -> [tx] -> UTxOType tx -> Snapshot tx
testSnapshot (SimpleId -> SnapshotNumber
forall a. Num a => SimpleId -> a
fromInteger SimpleId
sHat) (SimpleId -> SnapshotVersion
forall a. Num a => SimpleId -> a
fromInteger SimpleId
vHat) [] Set SimpleTxOut
UTxOType SimpleTx
forall a. Monoid a => a
mempty) ([Signature (Snapshot SimpleTx)]
-> MultiSignature (Snapshot SimpleTx)
forall a. [Signature a] -> MultiSignature a
aggregate [])
      , $sel:seenSnapshot:CoordinatedHeadState :: SeenSnapshot SimpleTx
seenSnapshot = if SimpleId
sHat SimpleId -> SimpleId -> Bool
forall a. Eq a => a -> a -> Bool
== SimpleId
0 then SeenSnapshot SimpleTx
forall tx. SeenSnapshot tx
NoSeenSnapshot else SnapshotNumber -> SeenSnapshot SimpleTx
forall tx. SnapshotNumber -> SeenSnapshot tx
LastSeenSnapshot (SimpleId -> SnapshotNumber
forall a. Num a => SimpleId -> a
fromInteger SimpleId
sHat)
      , $sel:currentDepositTxId:CoordinatedHeadState :: Maybe (TxIdType SimpleTx)
currentDepositTxId = Maybe SimpleId
Maybe (TxIdType SimpleTx)
forall a. Maybe a
Nothing
      , $sel:decommitTx:CoordinatedHeadState :: Maybe SimpleTx
decommitTx = Maybe SimpleTx
forall a. Maybe a
Nothing
      , $sel:version:CoordinatedHeadState :: SnapshotVersion
version = SimpleId -> SnapshotVersion
forall a. Num a => SimpleId -> a
fromInteger SimpleId
vHat
      }

-- Run the REAL handler on a (v, s) request from the given sender.
reqSnOutcome :: Integer -> Integer -> Integer -> Integer -> Party -> Outcome SimpleTx
reqSnOutcome :: SimpleId
-> SimpleId -> SimpleId -> SimpleId -> Party -> Outcome SimpleTx
reqSnOutcome SimpleId
vHat SimpleId
sHat SimpleId
v SimpleId
s Party
sender =
  Environment
-> Ledger SimpleTx
-> UTCTime
-> NodeState SimpleTx
-> Input SimpleTx
-> Outcome SimpleTx
forall tx.
IsChainState tx =>
Environment
-> Ledger tx -> UTCTime -> NodeState tx -> Input tx -> Outcome tx
update Environment
aliceEnv Ledger SimpleTx
simpleLedger UTCTime
time0 (SimpleId -> SimpleId -> NodeState SimpleTx
reqSnState SimpleId
vHat SimpleId
sHat) (Input SimpleTx -> Outcome SimpleTx)
-> Input SimpleTx -> Outcome SimpleTx
forall a b. (a -> b) -> a -> b
$
    Party -> Message SimpleTx -> Input SimpleTx
forall tx. Party -> Message tx -> Input tx
receiveMessageFrom Party
sender (SnapshotVersion
-> SnapshotNumber
-> [TxIdType SimpleTx]
-> Maybe SimpleTx
-> Maybe (TxIdType SimpleTx)
-> Message SimpleTx
forall tx.
SnapshotVersion
-> SnapshotNumber
-> [TxIdType tx]
-> Maybe tx
-> Maybe (TxIdType tx)
-> Message tx
ReqSn (SimpleId -> SnapshotVersion
forall a. Num a => SimpleId -> a
fromInteger SimpleId
v) (SimpleId -> SnapshotNumber
forall a. Num a => SimpleId -> a
fromInteger SimpleId
s) [] Maybe SimpleTx
forall a. Maybe a
Nothing Maybe SimpleId
Maybe (TxIdType SimpleTx)
forall a. Maybe a
Nothing)

-- ACCEPT iff the node reaches the signing continuation; Error and Wait are both non-accept.
reqSnAccepts :: Outcome SimpleTx -> Bool
reqSnAccepts :: Outcome SimpleTx -> Bool
reqSnAccepts = \case
  Continue{[StateChanged SimpleTx]
stateChanges :: [StateChanged SimpleTx]
$sel:stateChanges:Continue :: forall tx. Outcome tx -> [StateChanged tx]
stateChanges} -> (StateChanged SimpleTx -> Bool) -> [StateChanged SimpleTx] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any StateChanged SimpleTx -> Bool
isRequested [StateChanged SimpleTx]
stateChanges
  Outcome SimpleTx
_ -> Bool
False
 where
  isRequested :: StateChanged SimpleTx -> Bool
  isRequested :: StateChanged SimpleTx -> Bool
isRequested = \case
    SnapshotRequested{} -> Bool
True
    StateChanged SimpleTx
_ -> Bool
False

-- ── reqDec eligibility ───────────────────────────────────────────────────────────────────────────────

-- The requested decommit (no inputs, so it applies to any local UTxO) and a distinct in-flight one.
requestedDecommit :: SimpleTx
requestedDecommit :: SimpleTx
requestedDecommit = SimpleId -> UTxOType SimpleTx -> UTxOType SimpleTx -> SimpleTx
SimpleTx SimpleId
1 Set SimpleTxOut
UTxOType SimpleTx
forall a. Monoid a => a
mempty (SimpleId -> UTxOType SimpleTx
utxoRef SimpleId
1)

inFlightDecommit :: SimpleTx
inFlightDecommit :: SimpleTx
inFlightDecommit = SimpleId -> UTxOType SimpleTx -> UTxOType SimpleTx -> SimpleTx
SimpleTx SimpleId
2 Set SimpleTxOut
UTxOType SimpleTx
forall a. Monoid a => a
mempty (SimpleId -> UTxOType SimpleTx
utxoRef SimpleId
2)

-- Open state on the reqDec decision's domain: a recorded pending commit in each of the states the
-- reference distinguishes, and/or an in-flight decommit (tx_ω ≠ ⊥).
--
-- The commit axis is 'HsPendingCommit' and not a Bool, and the whole point is that this function has
-- no say in which of its cases blocks a decommit: it only has to build the state each case names,
-- and 'reqDecEligibleRef' decides. Recording a deposit id whose deposit has expired, or is no longer
-- registered, are both states the node reaches and clears the id in neither.
reqDecState :: HsPendingCommit -> Bool -> NodeState SimpleTx
reqDecState :: HsPendingCommit -> Bool -> NodeState SimpleTx
reqDecState HsPendingCommit
commit Bool
decommitInFlight =
  ([Party] -> CoordinatedHeadState SimpleTx -> NodeState SimpleTx
inOpenState' [Party]
threeParties CoordinatedHeadState SimpleTx
headState){pendingDeposits = registry}
 where
  headState :: CoordinatedHeadState SimpleTx
headState =
    CoordinatedHeadState
      { $sel:localUTxO:CoordinatedHeadState :: UTxOType SimpleTx
localUTxO = Set SimpleTxOut
UTxOType SimpleTx
forall a. Monoid a => a
mempty
      , $sel:allTxs:CoordinatedHeadState :: Map (TxIdType SimpleTx) SimpleTx
allTxs = Map SimpleId SimpleTx
Map (TxIdType SimpleTx) SimpleTx
forall a. Monoid a => a
mempty
      , $sel:localTxs:CoordinatedHeadState :: Seq SimpleTx
localTxs = Seq SimpleTx
forall a. Monoid a => a
mempty
      , $sel:confirmedSnapshot:CoordinatedHeadState :: ConfirmedSnapshot SimpleTx
confirmedSnapshot = HeadId -> ConfirmedSnapshot SimpleTx
forall tx. HeadId -> ConfirmedSnapshot tx
InitialSnapshot HeadId
testHeadId
      , $sel:seenSnapshot:CoordinatedHeadState :: SeenSnapshot SimpleTx
seenSnapshot = SeenSnapshot SimpleTx
forall tx. SeenSnapshot tx
NoSeenSnapshot
      , $sel:currentDepositTxId:CoordinatedHeadState :: Maybe (TxIdType SimpleTx)
currentDepositTxId = case HsPendingCommit
commit of
          HsPendingCommit
NoCommitP -> Maybe SimpleId
Maybe (TxIdType SimpleTx)
forall a. Maybe a
Nothing
          HsPendingCommit
_ -> SimpleId -> Maybe SimpleId
forall a. a -> Maybe a
Just SimpleId
TxIdType SimpleTx
reqDecDepositTxId
      , $sel:decommitTx:CoordinatedHeadState :: Maybe SimpleTx
decommitTx = if Bool
decommitInFlight then SimpleTx -> Maybe SimpleTx
forall a. a -> Maybe a
Just SimpleTx
inFlightDecommit else Maybe SimpleTx
forall a. Maybe a
Nothing
      , $sel:version:CoordinatedHeadState :: SnapshotVersion
version = SnapshotVersion
0
      }
  registry :: Map SimpleId (Deposit SimpleTx)
registry = case HsPendingCommit
commit of
    HsPendingCommit
NoCommitP -> Map SimpleId (Deposit SimpleTx)
forall a. Monoid a => a
mempty
    -- recorded but unregistered: what 'DepositRecovered' leaves behind
    HsPendingCommit
CommitGoneP -> Map SimpleId (Deposit SimpleTx)
forall a. Monoid a => a
mempty
    HsPendingCommit
CommitPendingP -> SimpleId -> Deposit SimpleTx -> Map SimpleId (Deposit SimpleTx)
forall k a. k -> a -> Map k a
Map.singleton SimpleId
TxIdType SimpleTx
reqDecDepositTxId (DepositStatus -> Deposit SimpleTx
mkReqDecDeposit DepositStatus
Active)
    HsPendingCommit
CommitExpiredP -> SimpleId -> Deposit SimpleTx -> Map SimpleId (Deposit SimpleTx)
forall k a. k -> a -> Map k a
Map.singleton SimpleId
TxIdType SimpleTx
reqDecDepositTxId (DepositStatus -> Deposit SimpleTx
mkReqDecDeposit DepositStatus
Expired)

reqDecDepositTxId :: TxIdType SimpleTx
reqDecDepositTxId :: TxIdType SimpleTx
reqDecDepositTxId = SimpleId
TxIdType SimpleTx
7

reqDecDepositedUTxO :: UTxOType SimpleTx
reqDecDepositedUTxO :: UTxOType SimpleTx
reqDecDepositedUTxO = SimpleId -> UTxOType SimpleTx
utxoRef SimpleId
9

mkReqDecDeposit :: DepositStatus -> Deposit SimpleTx
mkReqDecDeposit :: DepositStatus -> Deposit SimpleTx
mkReqDecDeposit DepositStatus
status =
  Deposit
    { $sel:headId:Deposit :: HeadId
headId = HeadId
testHeadId
    , $sel:deposited:Deposit :: UTxOType SimpleTx
deposited = UTxOType SimpleTx
reqDecDepositedUTxO
    , $sel:created:Deposit :: UTCTime
created = UTCTime
time0
    , $sel:deadline:Deposit :: UTCTime
deadline = POSIXTime -> UTCTime -> UTCTime
addUTCTime POSIXTime
3600 UTCTime
time0
    , DepositStatus
status :: DepositStatus
$sel:status:Deposit :: DepositStatus
status
    }

reqDecOutcome :: HsPendingCommit -> Bool -> Outcome SimpleTx
reqDecOutcome :: HsPendingCommit -> Bool -> Outcome SimpleTx
reqDecOutcome HsPendingCommit
commit Bool
decommitInFlight =
  Environment
-> Ledger SimpleTx
-> UTCTime
-> NodeState SimpleTx
-> Input SimpleTx
-> Outcome SimpleTx
forall tx.
IsChainState tx =>
Environment
-> Ledger tx -> UTCTime -> NodeState tx -> Input tx -> Outcome tx
update Environment
aliceEnv Ledger SimpleTx
simpleLedger UTCTime
time0 (HsPendingCommit -> Bool -> NodeState SimpleTx
reqDecState HsPendingCommit
commit Bool
decommitInFlight) (Input SimpleTx -> Outcome SimpleTx)
-> Input SimpleTx -> Outcome SimpleTx
forall a b. (a -> b) -> a -> b
$
    Party -> Message SimpleTx -> Input SimpleTx
forall tx. Party -> Message tx -> Input tx
receiveMessageFrom Party
bob ReqDec{$sel:transaction:ReqTx :: SimpleTx
transaction = SimpleTx
requestedDecommit}

reqDecAccepts :: Outcome SimpleTx -> Bool
reqDecAccepts :: Outcome SimpleTx -> Bool
reqDecAccepts = \case
  Continue{[StateChanged SimpleTx]
$sel:stateChanges:Continue :: forall tx. Outcome tx -> [StateChanged tx]
stateChanges :: [StateChanged SimpleTx]
stateChanges} -> (StateChanged SimpleTx -> Bool) -> [StateChanged SimpleTx] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any StateChanged SimpleTx -> Bool
isRecorded [StateChanged SimpleTx]
stateChanges
  Outcome SimpleTx
_ -> Bool
False
 where
  isRecorded :: StateChanged SimpleTx -> Bool
  isRecorded :: StateChanged SimpleTx -> Bool
isRecorded = \case
    DecommitRecorded{} -> Bool
True
    StateChanged SimpleTx
_ -> Bool
False

-- ── reqSn incremental-action guards ──────────────────────────────────────────────────────────────────

-- A decommit producing no outputs: could never settle on-chain (the decrement validator requires a
-- materialized output), so the node rejects it at request time.
noOutputDecommit :: SimpleTx
noOutputDecommit :: SimpleTx
noOutputDecommit = SimpleId -> UTxOType SimpleTx -> UTxOType SimpleTx -> SimpleTx
SimpleTx SimpleId
3 Set SimpleTxOut
UTxOType SimpleTx
forall a. Monoid a => a
mempty Set SimpleTxOut
UTxOType SimpleTx
forall a. Monoid a => a
mempty

-- An Active deposit recording `utxoRef 9`, registered under the given tx-id. Two of these under
-- different ids share their content and are distinguishable only by identity.
activeDeposit9 :: Deposit SimpleTx
activeDeposit9 :: Deposit SimpleTx
activeDeposit9 =
  Deposit
    { $sel:headId:Deposit :: HeadId
headId = HeadId
testHeadId
    , $sel:deposited:Deposit :: UTxOType SimpleTx
deposited = SimpleId -> UTxOType SimpleTx
utxoRef SimpleId
9
    , $sel:created:Deposit :: UTCTime
created = SimpleId -> UTCTime
posixTime SimpleId
0
    , $sel:deadline:Deposit :: UTCTime
deadline = SimpleId -> UTCTime
posixTime SimpleId
100
    , $sel:status:Deposit :: DepositStatus
status = DepositStatus
Active
    }

-- Fresh open state with deposit 7 registered Active: the domain of the both/no-outputs guards
-- (the request is the first snapshot, alice leads it).
incActionState :: NodeState SimpleTx
incActionState :: NodeState SimpleTx
incActionState = ([Party] -> NodeState SimpleTx
inOpenState [Party]
threeParties){pendingDeposits = Map.fromList [(7, activeDeposit9)]}

reqSnIncActionOutcome :: Maybe SimpleTx -> Maybe Integer -> Outcome SimpleTx
reqSnIncActionOutcome :: Maybe SimpleTx -> Maybe SimpleId -> Outcome SimpleTx
reqSnIncActionOutcome Maybe SimpleTx
mDecommit Maybe SimpleId
mDeposit =
  Environment
-> Ledger SimpleTx
-> UTCTime
-> NodeState SimpleTx
-> Input SimpleTx
-> Outcome SimpleTx
forall tx.
IsChainState tx =>
Environment
-> Ledger tx -> UTCTime -> NodeState tx -> Input tx -> Outcome tx
update Environment
aliceEnv Ledger SimpleTx
simpleLedger UTCTime
time0 NodeState SimpleTx
incActionState (Input SimpleTx -> Outcome SimpleTx)
-> Input SimpleTx -> Outcome SimpleTx
forall a b. (a -> b) -> a -> b
$
    Party -> Message SimpleTx -> Input SimpleTx
forall tx. Party -> Message tx -> Input tx
receiveMessageFrom Party
alice (SnapshotVersion
-> SnapshotNumber
-> [TxIdType SimpleTx]
-> Maybe SimpleTx
-> Maybe (TxIdType SimpleTx)
-> Message SimpleTx
forall tx.
SnapshotVersion
-> SnapshotNumber
-> [TxIdType tx]
-> Maybe tx
-> Maybe (TxIdType tx)
-> Message tx
ReqSn SnapshotVersion
0 SnapshotNumber
1 [] Maybe SimpleTx
mDecommit Maybe SimpleId
Maybe (TxIdType SimpleTx)
mDeposit)

-- Same-version settlement: the confirmed snapshot (number 1, version 0) carries the pending commit
-- of deposit 7; deposits 7 and its look-alike 8 are both registered Active. A request for snapshot 2
-- at the same version must name deposit 7 - naming 8 settles a different deposit under the same
-- content.
settleState :: NodeState SimpleTx
settleState :: NodeState SimpleTx
settleState =
  ([Party] -> CoordinatedHeadState SimpleTx -> NodeState SimpleTx
inOpenState' [Party]
threeParties CoordinatedHeadState SimpleTx
chs){pendingDeposits = Map.fromList [(7, activeDeposit9), (8, activeDeposit9)]}
 where
  chs :: CoordinatedHeadState SimpleTx
chs =
    CoordinatedHeadState
      { $sel:localUTxO:CoordinatedHeadState :: UTxOType SimpleTx
localUTxO = Set SimpleTxOut
UTxOType SimpleTx
forall a. Monoid a => a
mempty
      , $sel:allTxs:CoordinatedHeadState :: Map (TxIdType SimpleTx) SimpleTx
allTxs = Map SimpleId SimpleTx
Map (TxIdType SimpleTx) SimpleTx
forall a. Monoid a => a
mempty
      , $sel:localTxs:CoordinatedHeadState :: Seq SimpleTx
localTxs = Seq SimpleTx
forall a. Monoid a => a
mempty
      , $sel:confirmedSnapshot:CoordinatedHeadState :: ConfirmedSnapshot SimpleTx
confirmedSnapshot = Snapshot SimpleTx
-> MultiSignature (Snapshot SimpleTx) -> ConfirmedSnapshot SimpleTx
forall tx.
Snapshot tx -> MultiSignature (Snapshot tx) -> ConfirmedSnapshot tx
ConfirmedSnapshot Snapshot SimpleTx
settleSnapshot ([Signature (Snapshot SimpleTx)]
-> MultiSignature (Snapshot SimpleTx)
forall a. [Signature a] -> MultiSignature a
aggregate [])
      , $sel:seenSnapshot:CoordinatedHeadState :: SeenSnapshot SimpleTx
seenSnapshot = SnapshotNumber -> SeenSnapshot SimpleTx
forall tx. SnapshotNumber -> SeenSnapshot tx
LastSeenSnapshot SnapshotNumber
1
      , $sel:currentDepositTxId:CoordinatedHeadState :: Maybe (TxIdType SimpleTx)
currentDepositTxId = SimpleId -> Maybe SimpleId
forall a. a -> Maybe a
Just SimpleId
7
      , $sel:decommitTx:CoordinatedHeadState :: Maybe SimpleTx
decommitTx = Maybe SimpleTx
forall a. Maybe a
Nothing
      , $sel:version:CoordinatedHeadState :: SnapshotVersion
version = SnapshotVersion
0
      }
  -- testSnapshot with the pending commit of deposit 7 bound in; spelled out because a record
  -- update on the shared-field Snapshot type is ambiguous under DuplicateRecordFields.
  settleSnapshot :: Snapshot SimpleTx
  settleSnapshot :: Snapshot SimpleTx
settleSnapshot =
    Snapshot
      { $sel:headId:Snapshot :: HeadId
headId = HeadId
testHeadId
      , $sel:version:Snapshot :: SnapshotVersion
version = SnapshotVersion
0
      , $sel:number:Snapshot :: SnapshotNumber
number = SnapshotNumber
1
      , $sel:confirmed:Snapshot :: [SimpleTx]
confirmed = []
      , $sel:utxo:Snapshot :: UTxOType SimpleTx
utxo = Set SimpleTxOut
UTxOType SimpleTx
forall a. Monoid a => a
mempty
      , $sel:utxoToCommit:Snapshot :: Maybe (UTxOType SimpleTx)
utxoToCommit = Set SimpleTxOut -> Maybe (Set SimpleTxOut)
forall a. a -> Maybe a
Just (SimpleId -> UTxOType SimpleTx
utxoRef SimpleId
9)
      , $sel:utxoToDecommit:Snapshot :: Maybe (UTxOType SimpleTx)
utxoToDecommit = Maybe (Set SimpleTxOut)
Maybe (UTxOType SimpleTx)
forall a. Monoid a => a
mempty
      , $sel:depositTxId:Snapshot :: Maybe (TxIdType SimpleTx)
depositTxId = SimpleId -> Maybe SimpleId
forall a. a -> Maybe a
Just SimpleId
7
      , $sel:accumulator:Snapshot :: HydraAccumulator
accumulator = forall tx. IsTx tx => UTxOType tx -> HydraAccumulator
Accumulator.buildFromUTxO @SimpleTx Set SimpleTxOut
UTxOType SimpleTx
forall a. Monoid a => a
mempty
      }

-- Snapshot 2's leader among the three parties is bob ((2 - 1) mod 3 = 1).
reqSnSettleOutcome :: Integer -> Outcome SimpleTx
reqSnSettleOutcome :: SimpleId -> Outcome SimpleTx
reqSnSettleOutcome SimpleId
depositTxId =
  Environment
-> Ledger SimpleTx
-> UTCTime
-> NodeState SimpleTx
-> Input SimpleTx
-> Outcome SimpleTx
forall tx.
IsChainState tx =>
Environment
-> Ledger tx -> UTCTime -> NodeState tx -> Input tx -> Outcome tx
update Environment
aliceEnv Ledger SimpleTx
simpleLedger UTCTime
time0 NodeState SimpleTx
settleState (Input SimpleTx -> Outcome SimpleTx)
-> Input SimpleTx -> Outcome SimpleTx
forall a b. (a -> b) -> a -> b
$
    Party -> Message SimpleTx -> Input SimpleTx
forall tx. Party -> Message tx -> Input tx
receiveMessageFrom Party
bob (SnapshotVersion
-> SnapshotNumber
-> [TxIdType SimpleTx]
-> Maybe SimpleTx
-> Maybe (TxIdType SimpleTx)
-> Message SimpleTx
forall tx.
SnapshotVersion
-> SnapshotNumber
-> [TxIdType tx]
-> Maybe tx
-> Maybe (TxIdType tx)
-> Message tx
ReqSn SnapshotVersion
0 SnapshotNumber
2 [] Maybe SimpleTx
forall a. Maybe a
Nothing (SimpleId -> Maybe SimpleId
forall a. a -> Maybe a
Just SimpleId
depositTxId))

-- ── deposit status on tick ───────────────────────────────────────────────────────────────────────────

-- An env with the two deposit periods set INDEPENDENTLY (whole seconds): 'depositPeriod' bounds
-- expiry, 'depositActivation' the Inactive->Active transition (#2802). The extracted
-- 'depositStatusRef' takes both, so the oracle can be checked against the node on configurations
-- where they differ - which is where a model collapsing them into one would diverge silently.
tickEnv :: Integer -> Integer -> Environment
tickEnv :: SimpleId -> SimpleId -> Environment
tickEnv SimpleId
tDep SimpleId
tAct = Environment
aliceEnv{depositPeriod = fromInteger tDep, depositActivation = fromInteger tAct}

-- Open state holding one FRESH (Inactive) pending deposit with the given creation time and deadline.
depositState :: Integer -> Integer -> NodeState SimpleTx
depositState :: SimpleId -> SimpleId -> NodeState SimpleTx
depositState SimpleId
created SimpleId
deadline =
  ([Party] -> NodeState SimpleTx
inOpenState [Party]
threeParties)
    { pendingDeposits =
        Map.fromList
          [
            ( 1
            , Deposit
                { headId = testHeadId
                , deposited = utxoRef 1
                , created = posixTime created
                , deadline = posixTime deadline
                , status = Inactive
                }
            )
          ]
    }

-- One REAL tick at time t (now = chainTime, so the node stays in sync) over the fresh deposit; the
-- resulting status is read off the emitted transition event (none = still Inactive).
realTickStatus :: Integer -> Integer -> Integer -> Integer -> Integer -> HsDepositStatus
realTickStatus :: SimpleId
-> SimpleId -> SimpleId -> SimpleId -> SimpleId -> HsDepositStatus
realTickStatus SimpleId
created SimpleId
deadline SimpleId
tDep SimpleId
tAct SimpleId
t =
  case Environment
-> Ledger SimpleTx
-> UTCTime
-> NodeState SimpleTx
-> Input SimpleTx
-> Outcome SimpleTx
forall tx.
IsChainState tx =>
Environment
-> Ledger tx -> UTCTime -> NodeState tx -> Input tx -> Outcome tx
update (SimpleId -> SimpleId -> Environment
tickEnv SimpleId
tDep SimpleId
tAct) Ledger SimpleTx
simpleLedger (SimpleId -> UTCTime
posixTime SimpleId
t) (SimpleId -> SimpleId -> NodeState SimpleTx
depositState SimpleId
created SimpleId
deadline) Input SimpleTx
tick of
    Continue{[StateChanged SimpleTx]
$sel:stateChanges:Continue :: forall tx. Outcome tx -> [StateChanged tx]
stateChanges :: [StateChanged SimpleTx]
stateChanges}
      | (StateChanged SimpleTx -> Bool) -> [StateChanged SimpleTx] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any StateChanged SimpleTx -> Bool
isExpired [StateChanged SimpleTx]
stateChanges -> HsDepositStatus
ExpiredS
      | (StateChanged SimpleTx -> Bool) -> [StateChanged SimpleTx] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any StateChanged SimpleTx -> Bool
isActivated [StateChanged SimpleTx]
stateChanges -> HsDepositStatus
ActiveS
      | Bool
otherwise -> HsDepositStatus
InactiveS
    Outcome SimpleTx
outcome -> Text -> HsDepositStatus
forall a t. (HasCallStack, IsText t) => t -> a
Prelude.error (Text -> HsDepositStatus) -> Text -> HsDepositStatus
forall a b. (a -> b) -> a -> b
$ Text
"tick produced a non-Continue outcome: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Outcome SimpleTx -> Text
forall b a. (Show a, IsString b) => a -> b
show Outcome SimpleTx
outcome
 where
  tick :: Input SimpleTx
tick = ChainEvent SimpleTx -> Input SimpleTx
forall tx. ChainEvent tx -> Input tx
ChainInput Tick{$sel:chainTime:Observation :: UTCTime
chainTime = SimpleId -> UTCTime
posixTime SimpleId
t, $sel:chainPoint:Observation :: ChainPointType SimpleTx
chainPoint = ChainSlot
ChainPointType SimpleTx
1}

  isExpired :: StateChanged SimpleTx -> Bool
  isExpired :: StateChanged SimpleTx -> Bool
isExpired = \case
    DepositExpired{} -> Bool
True
    StateChanged SimpleTx
_ -> Bool
False

  isActivated :: StateChanged SimpleTx -> Bool
  isActivated :: StateChanged SimpleTx -> Bool
isActivated = \case
    DepositActivated{} -> Bool
True
    StateChanged SimpleTx
_ -> Bool
False

-- ── ackSn collect/confirm ────────────────────────────────────────────────────────────────────────────

-- Index ↔ party ↔ signing key, positional in 'threeParties' (as everywhere in this module).
partySks :: [(Party, Secret (SigningKey HydraKey))]
partySks :: [(Party, Secret (SigningKey HydraKey))]
partySks = [(Party
alice, Secret (SigningKey HydraKey)
aliceSk), (Party
bob, Secret (SigningKey HydraKey)
bobSk), (Party
carol, Secret (SigningKey HydraKey)
carolSk)]

partySkAt :: Integer -> (Party, Secret (SigningKey HydraKey))
partySkAt :: SimpleId -> (Party, Secret (SigningKey HydraKey))
partySkAt SimpleId
i = case Int
-> [(Party, Secret (SigningKey HydraKey))]
-> [(Party, Secret (SigningKey HydraKey))]
forall a. Int -> [a] -> [a]
drop (SimpleId -> Int
forall a. Num a => SimpleId -> a
fromInteger SimpleId
i) [(Party, Secret (SigningKey HydraKey))]
partySks of
  (Party, Secret (SigningKey HydraKey))
x : [(Party, Secret (SigningKey HydraKey))]
_ -> (Party, Secret (SigningKey HydraKey))
x
  [] -> Text -> (Party, Secret (SigningKey HydraKey))
forall a t. (HasCallStack, IsText t) => t -> a
Prelude.error Text
"partySkAt: index out of range"

-- The in-flight round's snapshot (ŝ = 1 on v̂ = 0) and its real per-party signatures.
ackSnapshot :: Snapshot SimpleTx
ackSnapshot :: Snapshot SimpleTx
ackSnapshot = SnapshotNumber
-> SnapshotVersion
-> [SimpleTx]
-> UTxOType SimpleTx
-> Snapshot SimpleTx
forall tx.
IsTx tx =>
SnapshotNumber
-> SnapshotVersion -> [tx] -> UTxOType tx -> Snapshot tx
testSnapshot SnapshotNumber
1 SnapshotVersion
0 [] Set SimpleTxOut
UTxOType SimpleTx
forall a. Monoid a => a
mempty

ackSigFor :: Integer -> (Party, Signature (Snapshot SimpleTx))
ackSigFor :: SimpleId -> (Party, Signature (Snapshot SimpleTx))
ackSigFor SimpleId
i = let (Party
p, Secret (SigningKey HydraKey)
sk) = SimpleId -> (Party, Secret (SigningKey HydraKey))
partySkAt SimpleId
i in (Party
p, Secret (SigningKey HydraKey)
-> Snapshot SimpleTx -> Signature (Snapshot SimpleTx)
forall a.
SignableRepresentation a =>
Secret (SigningKey HydraKey) -> a -> Signature a
sign Secret (SigningKey HydraKey)
sk Snapshot SimpleTx
ackSnapshot)

-- Open state mid-round: the seen snapshot is in flight with the given parties' REAL signatures
-- already collected ('mkSeenSnapshot' caches the signable bytes the verification runs over).
ackState :: [(Party, Signature (Snapshot SimpleTx))] -> NodeState SimpleTx
ackState :: [(Party, Signature (Snapshot SimpleTx))] -> NodeState SimpleTx
ackState [(Party, Signature (Snapshot SimpleTx))]
collected =
  [Party] -> CoordinatedHeadState SimpleTx -> NodeState SimpleTx
inOpenState' [Party]
threeParties (CoordinatedHeadState SimpleTx -> NodeState SimpleTx)
-> CoordinatedHeadState SimpleTx -> NodeState SimpleTx
forall a b. (a -> b) -> a -> b
$
    CoordinatedHeadState
      { $sel:localUTxO:CoordinatedHeadState :: UTxOType SimpleTx
localUTxO = Set SimpleTxOut
UTxOType SimpleTx
forall a. Monoid a => a
mempty
      , $sel:allTxs:CoordinatedHeadState :: Map (TxIdType SimpleTx) SimpleTx
allTxs = Map SimpleId SimpleTx
Map (TxIdType SimpleTx) SimpleTx
forall a. Monoid a => a
mempty
      , $sel:localTxs:CoordinatedHeadState :: Seq SimpleTx
localTxs = Seq SimpleTx
forall a. Monoid a => a
mempty
      , $sel:confirmedSnapshot:CoordinatedHeadState :: ConfirmedSnapshot SimpleTx
confirmedSnapshot = HeadId -> ConfirmedSnapshot SimpleTx
forall tx. HeadId -> ConfirmedSnapshot tx
InitialSnapshot HeadId
testHeadId
      , $sel:seenSnapshot:CoordinatedHeadState :: SeenSnapshot SimpleTx
seenSnapshot = Snapshot SimpleTx
-> Map Party (Signature (Snapshot SimpleTx))
-> SeenSnapshot SimpleTx
forall tx.
IsTx tx =>
Snapshot tx
-> Map Party (Signature (Snapshot tx)) -> SeenSnapshot tx
mkSeenSnapshot Snapshot SimpleTx
ackSnapshot ([(Party, Signature (Snapshot SimpleTx))]
-> Map Party (Signature (Snapshot SimpleTx))
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Party, Signature (Snapshot SimpleTx))]
collected)
      , $sel:currentDepositTxId:CoordinatedHeadState :: Maybe (TxIdType SimpleTx)
currentDepositTxId = Maybe SimpleId
Maybe (TxIdType SimpleTx)
forall a. Maybe a
Nothing
      , $sel:decommitTx:CoordinatedHeadState :: Maybe SimpleTx
decommitTx = Maybe SimpleTx
forall a. Maybe a
Nothing
      , $sel:version:CoordinatedHeadState :: SnapshotVersion
version = SnapshotVersion
0
      }

-- Run the REAL handler on sender's (real-signature) AckSn over the given collected subset.
ackOutcome :: [Integer] -> Integer -> Outcome SimpleTx
ackOutcome :: [SimpleId] -> SimpleId -> Outcome SimpleTx
ackOutcome [SimpleId]
signedIdxs SimpleId
senderIdx =
  Environment
-> Ledger SimpleTx
-> UTCTime
-> NodeState SimpleTx
-> Input SimpleTx
-> Outcome SimpleTx
forall tx.
IsChainState tx =>
Environment
-> Ledger tx -> UTCTime -> NodeState tx -> Input tx -> Outcome tx
update Environment
aliceEnv Ledger SimpleTx
simpleLedger UTCTime
time0 ([(Party, Signature (Snapshot SimpleTx))] -> NodeState SimpleTx
ackState (SimpleId -> (Party, Signature (Snapshot SimpleTx))
ackSigFor (SimpleId -> (Party, Signature (Snapshot SimpleTx)))
-> [SimpleId] -> [(Party, Signature (Snapshot SimpleTx))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SimpleId]
signedIdxs)) (Input SimpleTx -> Outcome SimpleTx)
-> Input SimpleTx -> Outcome SimpleTx
forall a b. (a -> b) -> a -> b
$
    Party -> Message SimpleTx -> Input SimpleTx
forall tx. Party -> Message tx -> Input tx
receiveMessageFrom Party
sender (Signature (Snapshot SimpleTx) -> SnapshotNumber -> Message SimpleTx
forall tx. Signature (Snapshot tx) -> SnapshotNumber -> Message tx
AckSn Signature (Snapshot SimpleTx)
senderSig SnapshotNumber
1)
 where
  (Party
sender, Secret (SigningKey HydraKey)
_) = SimpleId -> (Party, Secret (SigningKey HydraKey))
partySkAt SimpleId
senderIdx
  (Party
_, Signature (Snapshot SimpleTx)
senderSig) = SimpleId -> (Party, Signature (Snapshot SimpleTx))
ackSigFor SimpleId
senderIdx

-- The already-signed reject direction: the node's SnapshotAlreadySigned require failure.
ackAlreadySigned :: Outcome SimpleTx -> Bool
ackAlreadySigned :: Outcome SimpleTx -> Bool
ackAlreadySigned = \case
  Error (RequireFailed SnapshotAlreadySigned{}) -> Bool
True
  Outcome SimpleTx
_ -> Bool
False

-- The round completes: SnapshotConfirmed is emitted (behind the real multisignature verification).
ackConfirms :: Outcome SimpleTx -> Bool
ackConfirms :: Outcome SimpleTx -> Bool
ackConfirms = \case
  Continue{[StateChanged SimpleTx]
$sel:stateChanges:Continue :: forall tx. Outcome tx -> [StateChanged tx]
stateChanges :: [StateChanged SimpleTx]
stateChanges} -> (StateChanged SimpleTx -> Bool) -> [StateChanged SimpleTx] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any StateChanged SimpleTx -> Bool
isConfirmed [StateChanged SimpleTx]
stateChanges
  Outcome SimpleTx
_ -> Bool
False
 where
  isConfirmed :: StateChanged SimpleTx -> Bool
  isConfirmed :: StateChanged SimpleTx -> Bool
isConfirmed = \case
    SnapshotConfirmed{} -> Bool
True
    StateChanged SimpleTx
_ -> Bool
False

-- Validator-only rejection (the crypto boundary): alice's COLLECTED signature is over garbage, and
-- carol's final ack completes the signer set, so the counting guards pass but the real aggregate
-- verification fails.
ackOutcomeCorrupt :: Outcome SimpleTx
ackOutcomeCorrupt :: Outcome SimpleTx
ackOutcomeCorrupt =
  Environment
-> Ledger SimpleTx
-> UTCTime
-> NodeState SimpleTx
-> Input SimpleTx
-> Outcome SimpleTx
forall tx.
IsChainState tx =>
Environment
-> Ledger tx -> UTCTime -> NodeState tx -> Input tx -> Outcome tx
update Environment
aliceEnv Ledger SimpleTx
simpleLedger UTCTime
time0 ([(Party, Signature (Snapshot SimpleTx))] -> NodeState SimpleTx
ackState [(Party, Signature (Snapshot SimpleTx))
corrupt, SimpleId -> (Party, Signature (Snapshot SimpleTx))
ackSigFor SimpleId
1]) (Input SimpleTx -> Outcome SimpleTx)
-> Input SimpleTx -> Outcome SimpleTx
forall a b. (a -> b) -> a -> b
$
    Party -> Message SimpleTx -> Input SimpleTx
forall tx. Party -> Message tx -> Input tx
receiveMessageFrom Party
sender (Signature (Snapshot SimpleTx) -> SnapshotNumber -> Message SimpleTx
forall tx. Signature (Snapshot tx) -> SnapshotNumber -> Message tx
AckSn Signature (Snapshot SimpleTx)
senderSig SnapshotNumber
1)
 where
  corrupt :: (Party, Signature (Snapshot SimpleTx))
corrupt = (Party
alice, Signature ByteString -> Signature (Snapshot SimpleTx)
forall a b. Coercible a b => a -> b
coerce (Secret (SigningKey HydraKey) -> ByteString -> Signature ByteString
forall a.
SignableRepresentation a =>
Secret (SigningKey HydraKey) -> a -> Signature a
sign Secret (SigningKey HydraKey)
aliceSk (ByteString
"garbage" :: ByteString)))
  (Party
sender, Secret (SigningKey HydraKey)
_) = SimpleId -> (Party, Secret (SigningKey HydraKey))
partySkAt SimpleId
2
  (Party
_, Signature (Snapshot SimpleTx)
senderSig) = SimpleId -> (Party, Signature (Snapshot SimpleTx))
ackSigFor SimpleId
2

ackInvalidMultisig :: Outcome SimpleTx -> Bool
ackInvalidMultisig :: Outcome SimpleTx -> Bool
ackInvalidMultisig = \case
  Error (RequireFailed InvalidMultisignature{}) -> Bool
True
  Outcome SimpleTx
_ -> Bool
False

-- ── contest eligibility on a close observation ───────────────────────────────────────────────────────

-- Observe a close of snapshot s_c while our confirmed snapshot is S̄.s ('reqSnState' already builds
-- exactly the open state with a confirmed snapshot at a given number; version 0 here).
contestOutcome :: Integer -> Integer -> Outcome SimpleTx
contestOutcome :: SimpleId -> SimpleId -> Outcome SimpleTx
contestOutcome SimpleId
sBar SimpleId
sc =
  Environment
-> Ledger SimpleTx
-> UTCTime
-> NodeState SimpleTx
-> Input SimpleTx
-> Outcome SimpleTx
forall tx.
IsChainState tx =>
Environment
-> Ledger tx -> UTCTime -> NodeState tx -> Input tx -> Outcome tx
update Environment
aliceEnv Ledger SimpleTx
simpleLedger UTCTime
time0 (SimpleId -> SimpleId -> NodeState SimpleTx
reqSnState SimpleId
0 SimpleId
sBar) (Input SimpleTx -> Outcome SimpleTx)
-> Input SimpleTx -> Outcome SimpleTx
forall a b. (a -> b) -> a -> b
$
    OnChainTx SimpleTx -> Input SimpleTx
observeTx
      OnCloseTx
        { $sel:headId:OnInitTx :: HeadId
headId = HeadId
testHeadId
        , $sel:snapshotNumber:OnInitTx :: SnapshotNumber
snapshotNumber = SimpleId -> SnapshotNumber
forall a. Num a => SimpleId -> a
fromInteger SimpleId
sc
        , $sel:contestationDeadline:OnInitTx :: UTCTime
contestationDeadline = SimpleId -> UTCTime
posixTime SimpleId
1_000
        }

contestPosts :: Outcome SimpleTx -> Bool
contestPosts :: Outcome SimpleTx -> Bool
contestPosts = \case
  Continue{[Effect SimpleTx]
effects :: [Effect SimpleTx]
$sel:effects:Continue :: forall tx. Outcome tx -> [Effect tx]
effects} -> (Effect SimpleTx -> Bool) -> [Effect SimpleTx] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Effect SimpleTx -> Bool
isContest [Effect SimpleTx]
effects
  Outcome SimpleTx
_ -> Bool
False
 where
  isContest :: Effect SimpleTx -> Bool
  isContest :: Effect SimpleTx -> Bool
isContest = \case
    OnChainEffect{$sel:postChainTx:ClientEffect :: forall tx. Effect tx -> PostChainTx tx
postChainTx = ContestTx{}} -> Bool
True
    Effect SimpleTx
_ -> Bool
False

spec :: Spec
spec :: Spec
spec = Spec -> Spec
forall a. SpecWith a -> SpecWith a
parallel (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
  String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"reqSn signing eligibility: extracted signEligibleRef vs the real onOpenNetworkReqSn" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
    String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"anchor: an eligible ReqSn (v = v̂, s = ŝ + 1, sender leads s) is signed by the real node" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$ do
      SimpleId -> SimpleId -> SimpleId -> SimpleId -> Bool -> Bool
signEligibleRef SimpleId
0 SimpleId
0 SimpleId
1 SimpleId
0 (SimpleId -> SimpleId -> SimpleId -> Bool
leaderRef SimpleId
2 SimpleId
1 SimpleId
0) Bool -> Bool -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` Bool
True
      Outcome SimpleTx -> Bool
reqSnAccepts (SimpleId
-> SimpleId -> SimpleId -> SimpleId -> Party -> Outcome SimpleTx
reqSnOutcome SimpleId
0 SimpleId
0 SimpleId
0 SimpleId
1 Party
alice) Bool -> Bool -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` Bool
True
    String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"a wrong snapshot number is the node's ReqSnNumberInvalid" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$
      SimpleId
-> SimpleId -> SimpleId -> SimpleId -> Party -> Outcome SimpleTx
reqSnOutcome SimpleId
0 SimpleId
0 SimpleId
0 SimpleId
2 Party
alice Outcome SimpleTx -> Outcome SimpleTx -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` LogicError SimpleTx -> Outcome SimpleTx
forall tx. LogicError tx -> Outcome tx
Error (RequirementFailure SimpleTx -> LogicError SimpleTx
forall tx. RequirementFailure tx -> LogicError tx
RequireFailed (RequirementFailure SimpleTx -> LogicError SimpleTx)
-> RequirementFailure SimpleTx -> LogicError SimpleTx
forall a b. (a -> b) -> a -> b
$ SnapshotNumber -> SnapshotNumber -> RequirementFailure SimpleTx
forall tx.
SnapshotNumber -> SnapshotNumber -> RequirementFailure tx
ReqSnNumberInvalid SnapshotNumber
2 SnapshotNumber
0)
    String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"a non-leader sender is the node's ReqSnNotLeader" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$
      SimpleId
-> SimpleId -> SimpleId -> SimpleId -> Party -> Outcome SimpleTx
reqSnOutcome SimpleId
0 SimpleId
0 SimpleId
0 SimpleId
1 Party
bob Outcome SimpleTx -> Outcome SimpleTx -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` LogicError SimpleTx -> Outcome SimpleTx
forall tx. LogicError tx -> Outcome tx
Error (RequirementFailure SimpleTx -> LogicError SimpleTx
forall tx. RequirementFailure tx -> LogicError tx
RequireFailed (RequirementFailure SimpleTx -> LogicError SimpleTx)
-> RequirementFailure SimpleTx -> LogicError SimpleTx
forall a b. (a -> b) -> a -> b
$ SnapshotNumber -> Party -> RequirementFailure SimpleTx
forall tx. SnapshotNumber -> Party -> RequirementFailure tx
ReqSnNotLeader SnapshotNumber
1 Party
bob)
    String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"a version mismatch WAITS (WaitOnSnapshotVersion), which is non-accept" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$
      SimpleId
-> SimpleId -> SimpleId -> SimpleId -> Party -> Outcome SimpleTx
reqSnOutcome SimpleId
0 SimpleId
0 SimpleId
1 SimpleId
1 Party
alice Outcome SimpleTx -> WaitReason SimpleTx -> IO ()
forall tx.
(HasCallStack, IsChainState tx) =>
Outcome tx -> WaitReason tx -> IO ()
`assertWait` SnapshotVersion -> WaitReason SimpleTx
forall tx. SnapshotVersion -> WaitReason tx
WaitOnSnapshotVersion SnapshotVersion
1
    String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"signEligibleRef === real ReqSn accept/reject across (v, v̂, s, ŝ, sender)" (Property -> Spec) -> Property -> Spec
forall a b. (a -> b) -> a -> b
$
      Gen SimpleId -> (SimpleId -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll ((SimpleId, SimpleId) -> Gen SimpleId
forall a. Random a => (a, a) -> Gen a
choose (SimpleId
0, SimpleId
1)) ((SimpleId -> Property) -> Property)
-> (SimpleId -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \SimpleId
vHat ->
        Gen SimpleId -> (SimpleId -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll ((SimpleId, SimpleId) -> Gen SimpleId
forall a. Random a => (a, a) -> Gen a
choose (SimpleId
0, SimpleId
2)) ((SimpleId -> Property) -> Property)
-> (SimpleId -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \SimpleId
v ->
          Gen SimpleId -> (SimpleId -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll ((SimpleId, SimpleId) -> Gen SimpleId
forall a. Random a => (a, a) -> Gen a
choose (SimpleId
0, SimpleId
2)) ((SimpleId -> Property) -> Property)
-> (SimpleId -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \SimpleId
sHat ->
            Gen SimpleId -> (SimpleId -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll ((SimpleId, SimpleId) -> Gen SimpleId
forall a. Random a => (a, a) -> Gen a
choose (SimpleId
0, SimpleId
4)) ((SimpleId -> Property) -> Property)
-> (SimpleId -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \SimpleId
s ->
              Gen (SimpleId, Party)
-> ((SimpleId, Party) -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll ([(SimpleId, Party)] -> Gen (SimpleId, Party)
forall a. HasCallStack => [a] -> Gen a
elements ([SimpleId] -> [Party] -> [(SimpleId, Party)]
forall a b. [a] -> [b] -> [(a, b)]
zip [SimpleId
0 ..] [Party]
threeParties)) (((SimpleId, Party) -> Property) -> Property)
-> ((SimpleId, Party) -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \(SimpleId
i, Party
sender) ->
                SimpleId -> SimpleId -> SimpleId -> SimpleId -> Bool -> Bool
signEligibleRef SimpleId
v SimpleId
vHat SimpleId
s SimpleId
sHat (SimpleId -> SimpleId -> SimpleId -> Bool
leaderRef SimpleId
2 SimpleId
s SimpleId
i)
                  Bool -> Bool -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Outcome SimpleTx -> Bool
reqSnAccepts (SimpleId
-> SimpleId -> SimpleId -> SimpleId -> Party -> Outcome SimpleTx
reqSnOutcome SimpleId
vHat SimpleId
sHat SimpleId
v SimpleId
s Party
sender)

  String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"reqDec eligibility: extracted reqDecEligibleRef vs the real onOpenNetworkReqDec" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
    String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"anchor: with nothing in flight the real node records the decommit" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$ do
      HsPendingCommit -> Bool -> Bool
reqDecEligibleRef HsPendingCommit
NoCommitP Bool
False Bool -> Bool -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` Bool
True
      Outcome SimpleTx -> Bool
reqDecAccepts (HsPendingCommit -> Bool -> Outcome SimpleTx
reqDecOutcome HsPendingCommit
NoCommitP Bool
False) Bool -> Bool -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` Bool
True
    String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"a pending deposit (commit in flight) makes the real node WAIT (WaitOnUnresolvedCommit)" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$
      HsPendingCommit -> Bool -> Outcome SimpleTx
reqDecOutcome HsPendingCommit
CommitPendingP Bool
False
        Outcome SimpleTx -> WaitReason SimpleTx -> IO ()
forall tx.
(HasCallStack, IsChainState tx) =>
Outcome tx -> WaitReason tx -> IO ()
`assertWait` WaitOnUnresolvedCommit{$sel:commitUTxO:WaitOnNotApplicableTx :: UTxOType SimpleTx
commitUTxO = UTxOType SimpleTx
reqDecDepositedUTxO}
    String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"an in-flight decommit makes the real node WAIT (DecommitAlreadyInFlight)" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$
      HsPendingCommit -> Bool -> Outcome SimpleTx
reqDecOutcome HsPendingCommit
NoCommitP Bool
True
        Outcome SimpleTx -> WaitReason SimpleTx -> IO ()
forall tx.
(HasCallStack, IsChainState tx) =>
Outcome tx -> WaitReason tx -> IO ()
`assertWait` WaitOnNotApplicableDecommitTx
          { $sel:notApplicableReason:WaitOnNotApplicableTx :: DecommitInvalidReason SimpleTx
notApplicableReason = DecommitAlreadyInFlight{$sel:otherDecommitTxId:DecommitTxInvalid :: TxIdType SimpleTx
otherDecommitTxId = SimpleId
TxIdType SimpleTx
2}
          }
    -- The two cases that gave this differential its point: the reference says an expired or
    -- already-recovered commit does not block, and the node has to agree. A node that blocked on
    -- either would disagree here instead of being sanctioned by an oracle taking a Bool it chose.
    String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"an expired commit blocks neither the reference nor the real node" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$ do
      HsPendingCommit -> Bool -> Bool
reqDecEligibleRef HsPendingCommit
CommitExpiredP Bool
False Bool -> Bool -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` Bool
True
      Outcome SimpleTx -> Bool
reqDecAccepts (HsPendingCommit -> Bool -> Outcome SimpleTx
reqDecOutcome HsPendingCommit
CommitExpiredP Bool
False) Bool -> Bool -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` Bool
True
    String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"a commit that is already gone blocks neither" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$ do
      HsPendingCommit -> Bool -> Bool
reqDecEligibleRef HsPendingCommit
CommitGoneP Bool
False Bool -> Bool -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` Bool
True
      Outcome SimpleTx -> Bool
reqDecAccepts (HsPendingCommit -> Bool -> Outcome SimpleTx
reqDecOutcome HsPendingCommit
CommitGoneP Bool
False) Bool -> Bool -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` Bool
True
    String -> (Bool -> Property) -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"reqDecEligibleRef === real ReqDec accept/non-accept across (commit state, decommit?)" ((Bool -> Property) -> Spec) -> (Bool -> Property) -> Spec
forall a b. (a -> b) -> a -> b
$
      \Bool
decommitInFlight ->
        [Property] -> Property
forall prop. Testable prop => [prop] -> Property
conjoin
          [ String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (HsPendingCommit -> String
forall b a. (Show a, IsString b) => a -> b
show HsPendingCommit
commit) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
            HsPendingCommit -> Bool -> Bool
reqDecEligibleRef HsPendingCommit
commit Bool
decommitInFlight
              Bool -> Bool -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Outcome SimpleTx -> Bool
reqDecAccepts (HsPendingCommit -> Bool -> Outcome SimpleTx
reqDecOutcome HsPendingCommit
commit Bool
decommitInFlight)
          | HsPendingCommit
commit <- [HsPendingCommit
NoCommitP, HsPendingCommit
CommitPendingP, HsPendingCommit
CommitExpiredP, HsPendingCommit
CommitGoneP]
          ]

  String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"reqSn incremental-action guards: extracted reqSn*Ref vs the real onOpenNetworkReqSn" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
    String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"anchor: a deposit-only and a decommit-only request are both signed by the real node" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$ do
      Bool -> Bool -> Bool
reqSnNotBothRef Bool
True Bool
False Bool -> Bool -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` Bool
True
      Outcome SimpleTx -> Bool
reqSnAccepts (Maybe SimpleTx -> Maybe SimpleId -> Outcome SimpleTx
reqSnIncActionOutcome Maybe SimpleTx
forall a. Maybe a
Nothing (SimpleId -> Maybe SimpleId
forall a. a -> Maybe a
Just SimpleId
7)) Bool -> Bool -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` Bool
True
      Outcome SimpleTx -> Bool
reqSnAccepts (Maybe SimpleTx -> Maybe SimpleId -> Outcome SimpleTx
reqSnIncActionOutcome (SimpleTx -> Maybe SimpleTx
forall a. a -> Maybe a
Just SimpleTx
requestedDecommit) Maybe SimpleId
forall a. Maybe a
Nothing) Bool -> Bool -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` Bool
True
    String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"carrying both a deposit and a decommit is the node's ReqSnBothCommitAndDecommit" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$
      Maybe SimpleTx -> Maybe SimpleId -> Outcome SimpleTx
reqSnIncActionOutcome (SimpleTx -> Maybe SimpleTx
forall a. a -> Maybe a
Just SimpleTx
requestedDecommit) (SimpleId -> Maybe SimpleId
forall a. a -> Maybe a
Just SimpleId
7)
        Outcome SimpleTx -> Outcome SimpleTx -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` LogicError SimpleTx -> Outcome SimpleTx
forall tx. LogicError tx -> Outcome tx
Error (RequirementFailure SimpleTx -> LogicError SimpleTx
forall tx. RequirementFailure tx -> LogicError tx
RequireFailed ReqSnBothCommitAndDecommit{$sel:depositTxId:ReqSnNumberInvalid :: TxIdType SimpleTx
depositTxId = SimpleId
TxIdType SimpleTx
7, $sel:decommitTxId:ReqSnNumberInvalid :: TxIdType SimpleTx
decommitTxId = SimpleId
TxIdType SimpleTx
1})
    String -> (Bool -> Bool -> Property) -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"reqSnNotBothRef === real ReqSn accept/reject across (deposit?, decommit?)" ((Bool -> Bool -> Property) -> Spec)
-> (Bool -> Bool -> Property) -> Spec
forall a b. (a -> b) -> a -> b
$
      \Bool
hasDep Bool
hasDec ->
        Bool -> Bool -> Bool
reqSnNotBothRef Bool
hasDep Bool
hasDec
          Bool -> Bool -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Outcome SimpleTx -> Bool
reqSnAccepts
            ( Maybe SimpleTx -> Maybe SimpleId -> Outcome SimpleTx
reqSnIncActionOutcome
                (if Bool
hasDec then SimpleTx -> Maybe SimpleTx
forall a. a -> Maybe a
Just SimpleTx
requestedDecommit else Maybe SimpleTx
forall a. Maybe a
Nothing)
                (if Bool
hasDep then SimpleId -> Maybe SimpleId
forall a. a -> Maybe a
Just SimpleId
7 else Maybe SimpleId
forall a. Maybe a
Nothing)
            )
    String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"a decommit producing no outputs is the node's ReqSnDecommitNoOutputs; the reference agrees" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$ do
      SimpleId -> Bool
reqSnDecommitOutputsRef SimpleId
0 Bool -> Bool -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` Bool
False
      SimpleId -> Bool
reqSnDecommitOutputsRef SimpleId
1 Bool -> Bool -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` Bool
True
      Maybe SimpleTx -> Maybe SimpleId -> Outcome SimpleTx
reqSnIncActionOutcome (SimpleTx -> Maybe SimpleTx
forall a. a -> Maybe a
Just SimpleTx
noOutputDecommit) Maybe SimpleId
forall a. Maybe a
Nothing
        Outcome SimpleTx -> Outcome SimpleTx -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` LogicError SimpleTx -> Outcome SimpleTx
forall tx. LogicError tx -> Outcome tx
Error (RequirementFailure SimpleTx -> LogicError SimpleTx
forall tx. RequirementFailure tx -> LogicError tx
RequireFailed ReqSnDecommitNoOutputs{$sel:decommitTxId:ReqSnNumberInvalid :: TxIdType SimpleTx
decommitTxId = SimpleId
TxIdType SimpleTx
3})
    String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"anchor: settling the same-version pending commit with the bound deposit is signed by the real node" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$ do
      Bool -> SimpleId -> SimpleId -> Bool
reqSnDepositSettledRef Bool
True SimpleId
7 SimpleId
7 Bool -> Bool -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` Bool
True
      Outcome SimpleTx -> Bool
reqSnAccepts (SimpleId -> Outcome SimpleTx
reqSnSettleOutcome SimpleId
7) Bool -> Bool -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` Bool
True
    String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"a look-alike deposit (same recorded UTxO, different tx-id) is the node's ReqSnCommitNotSettled" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$ do
      Bool -> SimpleId -> SimpleId -> Bool
reqSnDepositSettledRef Bool
True SimpleId
7 SimpleId
8 Bool -> Bool -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` Bool
False
      SimpleId -> Outcome SimpleTx
reqSnSettleOutcome SimpleId
8 Outcome SimpleTx -> Outcome SimpleTx -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` LogicError SimpleTx -> Outcome SimpleTx
forall tx. LogicError tx -> Outcome tx
Error (RequirementFailure SimpleTx -> LogicError SimpleTx
forall tx. RequirementFailure tx -> LogicError tx
RequireFailed RequirementFailure SimpleTx
forall tx. RequirementFailure tx
ReqSnCommitNotSettled)
    String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"reqSnDepositSettledRef === real same-version settlement across the registered deposits" (Property -> Spec) -> Property -> Spec
forall a b. (a -> b) -> a -> b
$
      Gen SimpleId -> (SimpleId -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll ([SimpleId] -> Gen SimpleId
forall a. HasCallStack => [a] -> Gen a
elements [SimpleId
7, SimpleId
8]) ((SimpleId -> Property) -> Property)
-> (SimpleId -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \SimpleId
d ->
        Bool -> SimpleId -> SimpleId -> Bool
reqSnDepositSettledRef Bool
True SimpleId
7 SimpleId
d Bool -> Bool -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Outcome SimpleTx -> Bool
reqSnAccepts (SimpleId -> Outcome SimpleTx
reqSnSettleOutcome SimpleId
d)

  String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"deposit status on tick: extracted depositStatusRef vs the real deposit transition" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
    -- The same boundary points the extracted checker pins, now against the real node.
    String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"Inactive before created + T_activate (both)" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$ do
      SimpleId
-> SimpleId -> SimpleId -> SimpleId -> SimpleId -> HsDepositStatus
depositStatusRef SimpleId
0 SimpleId
100 SimpleId
10 SimpleId
10 SimpleId
5 HsDepositStatus -> HsDepositStatus -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` HsDepositStatus
InactiveS
      SimpleId
-> SimpleId -> SimpleId -> SimpleId -> SimpleId -> HsDepositStatus
realTickStatus SimpleId
0 SimpleId
100 SimpleId
10 SimpleId
10 SimpleId
5 HsDepositStatus -> HsDepositStatus -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` HsDepositStatus
InactiveS
    String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"still Inactive AT created + T_activate (strictly-greater boundary, both)" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$ do
      SimpleId
-> SimpleId -> SimpleId -> SimpleId -> SimpleId -> HsDepositStatus
depositStatusRef SimpleId
0 SimpleId
100 SimpleId
10 SimpleId
10 SimpleId
10 HsDepositStatus -> HsDepositStatus -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` HsDepositStatus
InactiveS
      SimpleId
-> SimpleId -> SimpleId -> SimpleId -> SimpleId -> HsDepositStatus
realTickStatus SimpleId
0 SimpleId
100 SimpleId
10 SimpleId
10 SimpleId
10 HsDepositStatus -> HsDepositStatus -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` HsDepositStatus
InactiveS
    String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"Active once t > created + T_activate (both)" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$ do
      SimpleId
-> SimpleId -> SimpleId -> SimpleId -> SimpleId -> HsDepositStatus
depositStatusRef SimpleId
0 SimpleId
100 SimpleId
10 SimpleId
10 SimpleId
15 HsDepositStatus -> HsDepositStatus -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` HsDepositStatus
ActiveS
      SimpleId
-> SimpleId -> SimpleId -> SimpleId -> SimpleId -> HsDepositStatus
realTickStatus SimpleId
0 SimpleId
100 SimpleId
10 SimpleId
10 SimpleId
15 HsDepositStatus -> HsDepositStatus -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` HsDepositStatus
ActiveS
    String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"still Active AT deadline − T_deposit (not yet expired, both)" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$ do
      SimpleId
-> SimpleId -> SimpleId -> SimpleId -> SimpleId -> HsDepositStatus
depositStatusRef SimpleId
0 SimpleId
100 SimpleId
10 SimpleId
10 SimpleId
90 HsDepositStatus -> HsDepositStatus -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` HsDepositStatus
ActiveS
      SimpleId
-> SimpleId -> SimpleId -> SimpleId -> SimpleId -> HsDepositStatus
realTickStatus SimpleId
0 SimpleId
100 SimpleId
10 SimpleId
10 SimpleId
90 HsDepositStatus -> HsDepositStatus -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` HsDepositStatus
ActiveS
    String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"Expired once t > deadline − T_deposit (both)" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$ do
      SimpleId
-> SimpleId -> SimpleId -> SimpleId -> SimpleId -> HsDepositStatus
depositStatusRef SimpleId
0 SimpleId
100 SimpleId
10 SimpleId
10 SimpleId
95 HsDepositStatus -> HsDepositStatus -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` HsDepositStatus
ExpiredS
      SimpleId
-> SimpleId -> SimpleId -> SimpleId -> SimpleId -> HsDepositStatus
realTickStatus SimpleId
0 SimpleId
100 SimpleId
10 SimpleId
10 SimpleId
95 HsDepositStatus -> HsDepositStatus -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` HsDepositStatus
ExpiredS
    -- The activation period alone decides the Inactive->Active boundary: with a short activation and
    -- a long expiry period, a deposit is Active well before `deadline - T_deposit`. A model using one
    -- period for both would put this boundary an arbitrary distance away, and no test that held the
    -- two equal could see it.
    String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"the activation boundary follows T_activate, not T_deposit (both)" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$ do
      SimpleId
-> SimpleId -> SimpleId -> SimpleId -> SimpleId -> HsDepositStatus
depositStatusRef SimpleId
0 SimpleId
1000 SimpleId
500 SimpleId
10 SimpleId
20 HsDepositStatus -> HsDepositStatus -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` HsDepositStatus
ActiveS
      SimpleId
-> SimpleId -> SimpleId -> SimpleId -> SimpleId -> HsDepositStatus
realTickStatus SimpleId
0 SimpleId
1000 SimpleId
500 SimpleId
10 SimpleId
20 HsDepositStatus -> HsDepositStatus -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` HsDepositStatus
ActiveS
      SimpleId
-> SimpleId -> SimpleId -> SimpleId -> SimpleId -> HsDepositStatus
depositStatusRef SimpleId
0 SimpleId
1000 SimpleId
500 SimpleId
100 SimpleId
20 HsDepositStatus -> HsDepositStatus -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` HsDepositStatus
InactiveS
      SimpleId
-> SimpleId -> SimpleId -> SimpleId -> SimpleId -> HsDepositStatus
realTickStatus SimpleId
0 SimpleId
1000 SimpleId
500 SimpleId
100 SimpleId
20 HsDepositStatus -> HsDepositStatus -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` HsDepositStatus
InactiveS
    String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"depositStatusRef === real tick status transition (independent periods, incl. boundaries)" (Property -> Spec) -> Property -> Spec
forall a b. (a -> b) -> a -> b
$
      Gen SimpleId -> (SimpleId -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll ((SimpleId, SimpleId) -> Gen SimpleId
forall a. Random a => (a, a) -> Gen a
choose (SimpleId
0, SimpleId
3)) ((SimpleId -> Property) -> Property)
-> (SimpleId -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \SimpleId
created ->
        Gen SimpleId -> (SimpleId -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll ((SimpleId, SimpleId) -> Gen SimpleId
forall a. Random a => (a, a) -> Gen a
choose (SimpleId
1, SimpleId
3)) ((SimpleId -> Property) -> Property)
-> (SimpleId -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \SimpleId
tDep ->
          Gen SimpleId -> (SimpleId -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll ((SimpleId, SimpleId) -> Gen SimpleId
forall a. Random a => (a, a) -> Gen a
choose (SimpleId
1, SimpleId
4)) ((SimpleId -> Property) -> Property)
-> (SimpleId -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \SimpleId
tAct ->
            Gen SimpleId -> (SimpleId -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll ((SimpleId, SimpleId) -> Gen SimpleId
forall a. Random a => (a, a) -> Gen a
choose (SimpleId
0, SimpleId
4)) ((SimpleId -> Property) -> Property)
-> (SimpleId -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \SimpleId
slack ->
              let deadline :: SimpleId
deadline = SimpleId
created SimpleId -> SimpleId -> SimpleId
forall a. Num a => a -> a -> a
+ SimpleId
2 SimpleId -> SimpleId -> SimpleId
forall a. Num a => a -> a -> a
* SimpleId
tDep SimpleId -> SimpleId -> SimpleId
forall a. Num a => a -> a -> a
+ SimpleId
tAct SimpleId -> SimpleId -> SimpleId
forall a. Num a => a -> a -> a
+ SimpleId
slack
               in Gen SimpleId -> (SimpleId -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll ((SimpleId, SimpleId) -> Gen SimpleId
forall a. Random a => (a, a) -> Gen a
choose (SimpleId
0, SimpleId
deadline SimpleId -> SimpleId -> SimpleId
forall a. Num a => a -> a -> a
+ SimpleId
tDep SimpleId -> SimpleId -> SimpleId
forall a. Num a => a -> a -> a
+ SimpleId
1)) ((SimpleId -> Property) -> Property)
-> (SimpleId -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \SimpleId
t ->
                    SimpleId
-> SimpleId -> SimpleId -> SimpleId -> SimpleId -> HsDepositStatus
depositStatusRef SimpleId
created SimpleId
deadline SimpleId
tDep SimpleId
tAct SimpleId
t
                      HsDepositStatus -> HsDepositStatus -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== SimpleId
-> SimpleId -> SimpleId -> SimpleId -> SimpleId -> HsDepositStatus
realTickStatus SimpleId
created SimpleId
deadline SimpleId
tDep SimpleId
tAct SimpleId
t

  String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"ackSn collect/confirm: extracted notAlreadySignedRef/allSignedRef vs the real onOpenNetworkAckSn" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
    String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"anchor: a fresh, non-final ack is collected (neither already-signed nor confirmed)" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$ do
      [SimpleId] -> SimpleId -> Bool
notAlreadySignedRef [SimpleId
0] SimpleId
1 Bool -> Bool -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` Bool
True
      SimpleId -> [SimpleId] -> Bool
allSignedRef SimpleId
3 [SimpleId
1, SimpleId
0] Bool -> Bool -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` Bool
False
      Outcome SimpleTx -> Bool
ackAlreadySigned ([SimpleId] -> SimpleId -> Outcome SimpleTx
ackOutcome [SimpleId
0] SimpleId
1) Bool -> Bool -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` Bool
False
      Outcome SimpleTx -> Bool
ackConfirms ([SimpleId] -> SimpleId -> Outcome SimpleTx
ackOutcome [SimpleId
0] SimpleId
1) Bool -> Bool -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` Bool
False
    String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"anchor: the final ack CONFIRMS (real signatures aggregated in order and verified)" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$ do
      SimpleId -> [SimpleId] -> Bool
allSignedRef SimpleId
3 [SimpleId
2, SimpleId
0, SimpleId
1] Bool -> Bool -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` Bool
True
      Outcome SimpleTx -> Bool
ackConfirms ([SimpleId] -> SimpleId -> Outcome SimpleTx
ackOutcome [SimpleId
0, SimpleId
1] SimpleId
2) Bool -> Bool -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` Bool
True
    String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"a duplicate ack is the node's SnapshotAlreadySigned" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$ do
      [SimpleId] -> SimpleId -> Bool
notAlreadySignedRef [SimpleId
0, SimpleId
1] SimpleId
1 Bool -> Bool -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` Bool
False
      Outcome SimpleTx -> Bool
ackAlreadySigned ([SimpleId] -> SimpleId -> Outcome SimpleTx
ackOutcome [SimpleId
0, SimpleId
1] SimpleId
1) Bool -> Bool -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` Bool
True
    String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"notAlreadySignedRef === real not-already-signed across (signed subset, sender)" (Property -> Spec) -> Property -> Spec
forall a b. (a -> b) -> a -> b
$
      Gen [SimpleId] -> ([SimpleId] -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll ([SimpleId] -> Gen [SimpleId]
forall a. [a] -> Gen [a]
sublistOf [SimpleId
0, SimpleId
1, SimpleId
2]) (([SimpleId] -> Property) -> Property)
-> ([SimpleId] -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \[SimpleId]
signedIdxs ->
        Gen SimpleId -> (SimpleId -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll ([SimpleId] -> Gen SimpleId
forall a. HasCallStack => [a] -> Gen a
elements [SimpleId
0, SimpleId
1, SimpleId
2]) ((SimpleId -> Property) -> Property)
-> (SimpleId -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \SimpleId
senderIdx ->
          [SimpleId] -> SimpleId -> Bool
notAlreadySignedRef [SimpleId]
signedIdxs SimpleId
senderIdx
            Bool -> Bool -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Bool -> Bool
not (Outcome SimpleTx -> Bool
ackAlreadySigned ([SimpleId] -> SimpleId -> Outcome SimpleTx
ackOutcome [SimpleId]
signedIdxs SimpleId
senderIdx))
    String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"composed: the ack CONFIRMS iff the sender is fresh AND completes the n-of-n signer set" (Property -> Spec) -> Property -> Spec
forall a b. (a -> b) -> a -> b
$
      Gen [SimpleId] -> ([SimpleId] -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll ([SimpleId] -> Gen [SimpleId]
forall a. [a] -> Gen [a]
sublistOf [SimpleId
0, SimpleId
1, SimpleId
2]) (([SimpleId] -> Property) -> Property)
-> ([SimpleId] -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \[SimpleId]
signedIdxs ->
        Gen SimpleId -> (SimpleId -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll ([SimpleId] -> Gen SimpleId
forall a. HasCallStack => [a] -> Gen a
elements [SimpleId
0, SimpleId
1, SimpleId
2]) ((SimpleId -> Property) -> Property)
-> (SimpleId -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \SimpleId
senderIdx ->
          ([SimpleId] -> SimpleId -> Bool
notAlreadySignedRef [SimpleId]
signedIdxs SimpleId
senderIdx Bool -> Bool -> Bool
&& SimpleId -> [SimpleId] -> Bool
allSignedRef SimpleId
3 (SimpleId
senderIdx SimpleId -> [SimpleId] -> [SimpleId]
forall a. a -> [a] -> [a]
: [SimpleId]
signedIdxs))
            Bool -> Bool -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Outcome SimpleTx -> Bool
ackConfirms ([SimpleId] -> SimpleId -> Outcome SimpleTx
ackOutcome [SimpleId]
signedIdxs SimpleId
senderIdx)
    String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"scope: a corrupt collected signature fails the real multisignature verification (the counting reference alone would accept)" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$ do
      SimpleId -> [SimpleId] -> Bool
allSignedRef SimpleId
3 [SimpleId
2, SimpleId
0, SimpleId
1] Bool -> Bool -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` Bool
True
      Outcome SimpleTx -> Bool
ackInvalidMultisig Outcome SimpleTx
ackOutcomeCorrupt Bool -> Bool -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` Bool
True

  String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"contest eligibility: extracted contestEligibleRef vs the real onOpenChainCloseTx" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
    String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"anchor: a newer confirmed snapshot posts a ContestTx" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$ do
      SimpleId -> SimpleId -> Bool
contestEligibleRef SimpleId
1 SimpleId
0 Bool -> Bool -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` Bool
True
      Outcome SimpleTx -> Bool
contestPosts (SimpleId -> SimpleId -> Outcome SimpleTx
contestOutcome SimpleId
1 SimpleId
0) Bool -> Bool -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` Bool
True
    String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"an equal snapshot number does NOT contest (strictly-greater boundary)" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$ do
      SimpleId -> SimpleId -> Bool
contestEligibleRef SimpleId
1 SimpleId
1 Bool -> Bool -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` Bool
False
      Outcome SimpleTx -> Bool
contestPosts (SimpleId -> SimpleId -> Outcome SimpleTx
contestOutcome SimpleId
1 SimpleId
1) Bool -> Bool -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` Bool
False
    String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"contestEligibleRef === real contest re-post across (S̄.s, s_c)" (Property -> Spec) -> Property -> Spec
forall a b. (a -> b) -> a -> b
$
      Gen SimpleId -> (SimpleId -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll ((SimpleId, SimpleId) -> Gen SimpleId
forall a. Random a => (a, a) -> Gen a
choose (SimpleId
0, SimpleId
2)) ((SimpleId -> Property) -> Property)
-> (SimpleId -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \SimpleId
sBar ->
        Gen SimpleId -> (SimpleId -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll ((SimpleId, SimpleId) -> Gen SimpleId
forall a. Random a => (a, a) -> Gen a
choose (SimpleId
0, SimpleId
3)) ((SimpleId -> Property) -> Property)
-> (SimpleId -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \SimpleId
sc ->
          SimpleId -> SimpleId -> Bool
contestEligibleRef SimpleId
sBar SimpleId
sc Bool -> Bool -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Outcome SimpleTx -> Bool
contestPosts (SimpleId -> SimpleId -> Outcome SimpleTx
contestOutcome SimpleId
sBar SimpleId
sc)