Skip to content

Commit

Permalink
Order clauses as in spec and resolve todos
Browse files Browse the repository at this point in the history
  • Loading branch information
ch1bo committed Jul 11, 2024
1 parent 9681e48 commit 830b916
Show file tree
Hide file tree
Showing 2 changed files with 27 additions and 27 deletions.
45 changes: 23 additions & 22 deletions hydra-plutus/src/Hydra/Contract/Head.hs
Original file line number Diff line number Diff line change
Expand Up @@ -232,8 +232,8 @@ checkDecrement ctx openBefore redeemer =
mustNotChangeParameters (prevParties, nextParties) (prevCperiod, nextCperiod) (prevHeadId, nextHeadId)
&& mustIncreaseVersion
&& checkSnapshotSignature
&& mustBeSignedByParticipant ctx prevHeadId
&& mustDecreaseValue
&& mustBeSignedByParticipant ctx prevHeadId
where
checkSnapshotSignature =
verifySnapshotSignature nextParties (nextHeadId, prevVersion, snapshotNumber, nextUtxoHash, decommitUtxoHash) signature
Expand Down Expand Up @@ -267,6 +267,7 @@ checkDecrement ctx openBefore redeemer =

-- NOTE: head output + whatever is decommitted needs to be equal to the head input.
headOutValue = txOutValue $ head outputs

headInValue = maybe mempty (txOutValue . txInInfoResolved) $ findOwnInput ctx

-- NOTE: we always assume Head output is the first one so we pick all other
Expand All @@ -287,15 +288,15 @@ checkClose ::
CloseRedeemer ->
Bool
checkClose ctx openBefore redeemer =
mustNotMintOrBurn txInfo
&& hasBoundedValidity
&& checkDeadline
&& mustBeSignedByParticipant ctx headId
mustNotChangeParameters (parties', parties) (cperiod', cperiod) (headId', headId)
&& mustNotChangeVersion
&& mustBeValidSnapshot
&& mustInitializeContesters
&& checkDeadline
&& hasBoundedValidity
&& mustPreserveValue
&& mustNotChangeParameters (parties', parties) (cperiod', cperiod) (headId', headId)
&& mustBeSignedByParticipant ctx headId
&& mustNotMintOrBurn txInfo
where
OpenDatum
{ parties
Expand All @@ -305,18 +306,6 @@ checkClose ctx openBefore redeemer =
, version
} = openBefore

mustPreserveValue =
traceIfFalse $(errorCode HeadValueIsNotPreserved) $
val === val'

val' = txOutValue . head $ txInfoOutputs txInfo

val = maybe mempty (txOutValue . txInInfoResolved) $ findOwnInput ctx

hasBoundedValidity =
traceIfFalse $(errorCode HasBoundedValidityCheckFailed) $
tMax - tMin <= cp

(snapshotNumber', utxoHash', utxoDeltaHash', parties', deadline, cperiod', headId', contesters', version') =
extractClosedDatum ctx

Expand Down Expand Up @@ -349,6 +338,18 @@ checkClose ctx openBefore redeemer =
traceIfFalse $(errorCode IncorrectClosedContestationDeadline) $
deadline == makeContestationDeadline cperiod ctx

mustPreserveValue =
traceIfFalse $(errorCode HeadValueIsNotPreserved) $
val === val'

val' = txOutValue . head $ txInfoOutputs txInfo

val = maybe mempty (txOutValue . txInInfoResolved) $ findOwnInput ctx

hasBoundedValidity =
traceIfFalse $(errorCode HasBoundedValidityCheckFailed) $
tMax - tMin <= cp

cp = fromMilliSeconds (milliseconds cperiod)

tMax = case ivTo $ txInfoValidRange txInfo of
Expand Down Expand Up @@ -383,17 +384,17 @@ checkContest ::
ContestRedeemer ->
Bool
checkContest ctx contestationDeadline contestationPeriod parties snapshotNumber contesters headId version redeemer =
mustNotMintOrBurn txInfo
mustNotChangeParameters (parties', parties) (contestationPeriod', contestationPeriod) (headId', headId)
&& mustNotChangeVersion
&& mustBeNewer
&& mustBeValidSnapshot
&& mustBeSignedByParticipant ctx headId
&& checkSignedParticipantContestOnlyOnce
&& mustBeWithinContestationPeriod
&& mustUpdateContesters
&& mustBeWithinContestationPeriod
&& mustPushDeadline
&& mustNotChangeParameters (parties', parties) (contestationPeriod', contestationPeriod) (headId', headId)
&& mustPreserveValue
&& mustBeSignedByParticipant ctx headId
&& mustNotMintOrBurn txInfo
where
mustPreserveValue =
traceIfFalse $(errorCode HeadValueIsNotPreserved) $
Expand Down
9 changes: 4 additions & 5 deletions spec/onchain.tex
Original file line number Diff line number Diff line change
Expand Up @@ -330,15 +330,14 @@ \subsection{\red{Decrement Transaction}}\label{sec:decrement-tx}
\end{itemize}

\noindent The state-machine validator $\nuHead$ is spent with
$\redeemerHead = (\mathsf{decrement}, \xi, s, m)$, where $\xi$ is a multi-signature of
the decrement snapshot which authorizes removal of some UTxO, $s$ is the
used \todo{Decrement redeemer doesn't contain snapshot number} snapshot number and $m$ is the number of outputs to distribute. The
validator checks:
$\redeemerHead = (\mathsf{decrement}, \xi, s, m)$, where $\xi$ is a multi-signature
of the decrement snapshot which authorizes removal of some UTxO, $s$ is the used
snapshot number and $m$ is the number of outputs to distribute. The validator
checks:
\begin{menumerate}
\item State is advanced from $\datumHead \sim \stOpen$ to
$\datumHead' \sim \stOpen$, parameters $\cid,\hydraKeys,\cPer$ stay
unchanged and the new state is governed again by $\nuHead$
\todo{Open datum should contain snapshot number}
\[
(\stOpen,\cid,\hydraKeys,\cPer,v,\eta) \xrightarrow[\xi, s, m]{\mathsf{decrement}} (\stOpen,\cid,\hydraKeys,\cPer,v',\eta')
\]
Expand Down

0 comments on commit 830b916

Please sign in to comment.