Add update mechanism and related STS rules #598

mgudemann · 2019-06-20T16:32:40Z

This is rebased onto current master with the tighter compilation error settings and includes all changes from #585.

mgudemann · 2019-06-21T13:32:14Z

Found some small issues, marked as TODO
two things are undefined for the moment: the function overlaySchedule and the update of the PParams in EPOCH which seems to be a type mismatch

JaredCorduan · 2019-06-24T13:47:09Z

shelley/chain-and-ledger/executable-spec/src/STS/Chain.hs

-instance Embed OCERT CHAIN where
-  wrapFailed = OcertFailure
+  let ls' = setIssueNumbers ls cs' -- TODO: is this cs or cs' ?
+                                   -- (formal spec ignored cs')


it should be cs', good catch!

shelley/chain-and-ledger/executable-spec/test/PropertyTests.hs

JaredCorduan · 2019-06-24T15:01:16Z

shelley/chain-and-ledger/formal-spec/chain.tex

@@ -709,6 +709,7 @@ \subsection{Block Header Transition}
      }
      \\~\\
      (\wcard,~\wcard,~\var{b_{prev}},~\wcard,~\var{es},~\var{ru},~\wcard,~\wcard)\leteq\var{nes}
+      % TODO: is es = (_ _ _ pp) ?


yes, the protocol parameters are the fourth component of the epoch state. but I do not see what this is needed, we do not use the pp in the rule.

we extract the max header size and max block size from the paramters

JaredCorduan · 2019-06-24T15:01:58Z

shelley/chain-and-ledger/formal-spec/chain.tex

@@ -852,6 +853,7 @@ \subsection{Verifiable Random Function}
      & ~~~~\where \\
      & ~~~~~~~~~~\var{hk} \leteq \hashKey{(\bvkcold bhb)} \\
      & ~~~~~~~~~~\var{ss} \leteq \slotToSeed{(\bslot{bhb})} \\
+      % TODO : is vk = bvkcold bhb ?


yes, good catch!

JaredCorduan · 2019-06-24T15:05:34Z

shelley/chain-and-ledger/formal-spec/chain.tex

@@ -1381,7 +1383,8 @@ \subsection{Chain Transition}
              \eta_c' \\
        \end{array}\right)}
      } \\~\\~\\
-      \var{ls'}\leteq\fun{setIssueNumbers}~\var{ls}~\var{cs} \\
+      \var{ls'}\leteq\fun{setIssueNumbers}~\var{ls}~\var{cs} \\ % TODO should
+                                % this be cs' ?


JaredCorduan · 2019-06-24T15:29:41Z

shelley/chain-and-ledger/formal-spec/epoch.tex

@@ -900,6 +900,8 @@ \subsection{Complete Epoch Boundary Transition}
      \\~\\~\\
      \var{(\wcard,~\wcard,~\wcard,~(\var{pup},~\wcard,~\wcard,~\wcard))}\leteq\var{utxoSt'}\\
      \var{pp_{new}}\leteq\fun{votedValue_{PParams}}~\var{pup}\\
+      % TODO: I think this isn't the right type, `pup` is PPUpdate which is not
+      % a complete set of `PParams`.


I think it is okay, though it maybe does not translate well to Haskell. The type of PParams is a mapping of PPm to Value.

ok, I see. So that's a place where the executable spec deviates a bit PParams is a record with all values and the parameter update is a mapping. This comes in handy whenever a value of PParams is read as the mapping would require checking for presence of the element. I will create an issue for that.

JaredCorduan · 2019-06-24T15:31:53Z

shelley/chain-and-ledger/formal-spec/update.tex

@@ -244,7 +244,7 @@ \section{Updates}
      &
      \dom{\var{aup}}\subseteq\dom{\var{dms}}
      \\
-      \var{aup'}\leteq\var{aup_s}\unionoverrideRight\var{aup}
+      \var{aup'}\leteq\var{aup_s}\unionoverrideRight\var{aup} % TODO: not needed here?


yes, good catch! that was a copy past error 😬

JaredCorduan · 2019-06-24T15:32:37Z

shelley/chain-and-ledger/formal-spec/update.tex

@@ -327,7 +327,8 @@ \section{Updates}
  \begin{equation}\label{eq:update}
    \inference[Update]
    {
-      (\var{pup},~\var{aup})\leteq\var{up}
+      (\var{pup},~\var{aup})\leteq\var{up} % TODO: duplicate of state names in


yes, good catch!

`LedgerState` still contains a field for the current `Ix` in the slot. This doesn't appear in the formal spec.

We allow redundant witnesses to support mutli-sig which might require more than one valid signature for transactions.

- remove unit tests that tests exactly that situation - remove `UnneededWitnesses` from expected failures

…_mechanism Add update mechanism and related STS rules

598: Add ToCBOR and FromCBOR instances for UTxOValidationError r=mrBliss a=mrBliss These will be used by ouroboros-network to transmit validation errors over the local TxSubmission protocol. Co-authored-by: Thomas Winant <thomas@well-typed.com>

mgudemann requested a review from JaredCorduan as a code owner June 20, 2019 16:32

mgudemann self-assigned this Jun 20, 2019

mgudemann added shelley ⚙️ executable-model 🚧 work in progress labels Jun 20, 2019

mgudemann mentioned this pull request Jun 21, 2019

Adapt / add STS rules for PRTCL and below #585

Closed

mgudemann force-pushed the exec_spec/shelley/update_mechanism branch from 0815970 to 0815ab6 Compare June 21, 2019 13:30

mgudemann removed the 🚧 work in progress label Jun 24, 2019

mgudemann force-pushed the exec_spec/shelley/update_mechanism branch from 08159b2 to 08156c1 Compare June 24, 2019 09:07

JaredCorduan reviewed Jun 24, 2019

View reviewed changes

shelley/chain-and-ledger/executable-spec/test/PropertyTests.hs Outdated Show resolved Hide resolved

JaredCorduan reviewed Jun 24, 2019

View reviewed changes

JaredCorduan approved these changes Jun 24, 2019

View reviewed changes

mgudemann force-pushed the exec_spec/shelley/update_mechanism branch from 0815e08 to 0815e32 Compare June 24, 2019 16:24

mgudemann added 10 commits June 24, 2019 18:30

Add OVERLAY STS rule in exec spec

38ee155

Add PRTCL STS rule

9e59881

Adapt CHAIN STS rule with call to PRTCL

4df9ab3

Fix Environment type in CHAIN rule

17d2ddd

Adapt BHEAD STS rule

37d2dac

Call BHEAD from CHAIN

000a30a

Add Updates module

84bb4e2

Add PPUP STS rule

08084f0

Add ApplicationUpdate types and helper functions

a92c758

Add AVUP STS rule

da95f8f

mgudemann added 12 commits June 24, 2019 18:30

Add UP STS rule

4c0c4aa

Adapt UTXO STS rule

1b98e09

Simplify LedgerState, adapt tests

5681b79

`LedgerState` still contains a field for the current `Ix` in the slot. This doesn't appear in the formal spec.

Remove EEnt extra entropy type

f36fa5e

Fixes for compilation and layout

50692db

Adapt BBODY rule

b3c1f08

Adapt CHAIN STS rule

17b5d18

Adapt witsNeeded in UTXOW, remove UneededWitness failure

e908484

We allow redundant witnesses to support mutli-sig which might require more than one valid signature for transactions.

Remove UnneededWitnesses from expected results in unit test

7a8d231

- remove unit tests that tests exactly that situation - remove `UnneededWitnesses` from expected failures

Adapt property-based test for redundant witnesses

9849682

Remove UPIState from executable specification

49578b5

Fix TODOs in the formal spec

0815b93

mgudemann force-pushed the exec_spec/shelley/update_mechanism branch from 0815e32 to 0815b93 Compare June 24, 2019 16:30

mgudemann merged commit 1b4057c into master Jun 24, 2019

mgudemann deleted the exec_spec/shelley/update_mechanism branch June 24, 2019 16:36

kevinhammond pushed a commit that referenced this pull request Oct 28, 2019

Merge pull request #598 from input-output-hk/exec_spec/shelley/update…

694b3d4

…_mechanism Add update mechanism and related STS rules

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add update mechanism and related STS rules #598

Add update mechanism and related STS rules #598

mgudemann commented Jun 20, 2019

mgudemann commented Jun 21, 2019

JaredCorduan Jun 24, 2019

JaredCorduan Jun 24, 2019

mgudemann Jun 24, 2019

JaredCorduan Jun 24, 2019

JaredCorduan Jun 24, 2019

JaredCorduan Jun 24, 2019

mgudemann Jun 24, 2019

JaredCorduan Jun 24, 2019

JaredCorduan Jun 24, 2019

Add update mechanism and related STS rules #598

Add update mechanism and related STS rules #598

Conversation

mgudemann commented Jun 20, 2019

mgudemann commented Jun 21, 2019

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment