Merge pull request #104 from mlabs-haskell/uhbif19/update-soa-docs

Update docs

Author: euonymos

docs/goals_and_soa.md

@@ -49,7 +49,7 @@ what we use to demonstrate problems in following:
   * Fracada
   * JPG Vesting Contract
   * Indigo Protocol
-* DApp project we participate, audited or otherwise know it codebase
+* DApp projects we participated, audited or otherwise know their codebase
   * Hydra Auction
   * POCRE
   * CNS
@@ -61,8 +61,6 @@ what we use to demonstrate problems in following:
   * [Game Model](https://github.com/IntersectMBO/plutus-apps/blob/dbafa0ffdc1babcf8e9143ca5a7adde78d021a9a/doc/plutus/tutorials/GameModel.hs)
 * plutus-usecases
 
-@todo #3: Add more links to specific bugs and code size blowups in existing DApps.
-
 ## On-chain correctness
 
 ### Known common vulnerabilities
@@ -82,14 +80,31 @@ taking that burden from developers and auditors.
 
 Those problems are similar to previous in that they tend to
 arise in naive Plutus implementations,
-if developer was did not make measures to prevent them.
+if developer was did not take measures to prevent them.
+
+Plutus forces developers to write TxIn/TxOut constraints from scratch,
+leading by subtle bugs from copy-pasting logic or
+trying to optimize them by hand.
+
+Examples:
+
+* Security bug in MinSwap audit - 2.2.1.3 Unauthorized Hijacking of Pools Funds
+* Non-security bug in MinSwap audit - 2.2.2.2 Batcher Is Not Allowed to Apply Their Own Order
+
+Such constraints naturally lead to conditions
+for which more performant implementation should
+omit some constraints always following from others.
+Such kind of manual SMT solving exercises are
+known source for security bugs and complicated code.
 
-Almost all transactions which require fungible tokens as input,
+One of important cases is maintaining invariants of token value.
+TODO - add explanation
+
+Most of transactions which require fungible tokens as input,
 should not depend from exact UTxO coin-change distribution.
 
 Failure to expect that leads to prohibition of correct transactions.
-On other side too broad constraint might lead to
-fund stealing.
+On other side too broad constraint might lead to fund stealing.
 
 Example of bugs:
 
@@ -114,6 +129,9 @@ Examples:
 
 * Non-security bug: https://github.com/mlabs-haskell/hydra-auction/issues/129
 * Non-security bug: https://github.com/mlabs-haskell/hydra-auction/commit/8152720c43732f8fb74181b7509de503b8371997
+* Non-intentionally under-specified behavior in MinSwap audit:
+  * `2.2.2.1 Batchers Can Choose Batching Order`
+  * Triggered by `2.2.4.1 "Reliance on Indexes Into ScriptContexts' txInputs and txOutputs"`
 * Multiple kind of code complication was observed in CNS audit.
 * Utilities [from Indigo](https://github.com/IndigoProtocol/indigo-smart-contracts/blob/main/src/Indigo/Utils/Spooky/Helpers.hs)
 
@@ -179,6 +197,19 @@ Our script stages abstraction cover all those kind of problems.
 * @todo #3: document problems with slots in Plutus/Cardano API
   * https://github.com/mlabs-haskell/hydra-auction/issues/236
 
+## Matching off-chain logic
+
+Problem of duplicating logic between on- and off-chain is twofold.
+Testing is essentially offchain, thus, you may miss that your onchain code
+is not actually enforcing part of Tx provided in tests.
+
+CEM Script is constructing Tx for submission from same specification,
+which is used for onchain script. Thus it is much harder to miss constraint
+to be checked.
+
+Examples:
+
+* MinSwap audit - 2.2.1.2 LP Tokens Can Be Duplicated
 
 ## Logic duplication and spec subtleness
 
@@ -208,6 +239,33 @@ is much less obvious to implement,
 and out of scope of current Catalyst project,
 but it is very much possible feature as well.
 
+Examples of diagrams in DApp specifications:
+
+* ...
+* ...
+* ...
+
+### On-/Off-chain and spec logic duplication
+
+Writing on-chain contracts manually encodes non-deterministic state machine,
+which cannot be used for off-chain transaction construction.
+Thus developer need to write them again in different style in off-chain code,
+which is tedious and error prone.
+
+They should add checks for all errors possible,
+like coins being available and correct script states being present,
+to prevent cryptic errors and provide retrying strategies
+for possible utxo changes.
+
+Our project encodes scripts in deterministic machine,
+containing enough information to construct transaction automatically.
+This also gives a way to check for potential on/off-chain logic differences
+semi-automatically.
+
+Example:
+* MinSwap Audit - 2.2.4.3 Large Refactoring Opportunities
+* `availableVestings` - пример чего-то подобного для SimpleAuction
+
 Examples of this done by hand:
 
 * [State graph for Agora](https://github.com/Liqwid-Labs/agora/blob/staging/docs/diagrams/ProposalStateMachine.png)
@@ -241,10 +299,8 @@ Examples of boilerplate:
 
 * https://github.com/MELD-labs/cardano-defi-public/tree/eacaa527823031105eba1730f730e1b32f1470bc/lending-index/src/Lending/Index
 
-### Correct off-chain Tx construction logic
+Timing ...
 
-A lot of on-chain problems, like timing and coin change issues
-have their counterpart on Tx submission side.
 
 @todo #3: Add more off-chain code duplication examples from existing PABs.
   Include problems with coin-selection, tests, retrying and errors.
@@ -302,12 +358,19 @@ and multiple commiters schemes (used in `hydra`).
 
 ### Atlas
 
-Atlas provides (emulate-everything) and overall more humane DX
-on top of cardano-api. But it has no feature related to goals
+Atlas provides more humane DX on top of cardano-api.
+But it has no features related to goals
 (synced-by-construction), (secure-by-construction)
 and (declarative-spec).
+(emulate-everything) is planned, but is not implemented currently.
+
+Atlas includes connectors to Blockfrost and other backends,
+which our project lacks.
+
+Also our project has slight differences in API design decisions.
+Our monad interfaces is meant to be slightly more modular.
+We use much less custom type wrappers, resorting to Plutus types where possible.
 
-@todo #3: Add more specifics on Atlas to docs.
 
 ## Testing tools