WIP

Author: uhbif19

docs/goals_and_soa.md

@@ -48,16 +48,14 @@ 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
   * Hydra
 * Plutonomicon patterns
 * plutus-usecases
 
-@todo #3: Add more links to specific bugs and code size blowups in existing DApps.
-
 ## On-chain correctness
 
 ### Known common vulnerabilities
@@ -77,27 +75,36 @@ 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:
 
 * https://github.com/mlabs-haskell/hydra-auction/issues/146
 
-Another important case is maintaining invariants
-of token value or immutable UTxOs.
-Such kind of constraints naturally lead to script
-for which more performant implementation should
-eliminate some constraint following from others.
-Such kind of manual SMT solving exercises are
-known source for security bugs and complicated code.
-
 Making Plutus contract invariant to `TxIn` ordering
 and participation in multi-script scenarios lead to
 similar kind of complications.
@@ -106,6 +113,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.
 
 ### Single script safety and liveliness
@@ -169,6 +179,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
 
@@ -195,15 +218,38 @@ is much less obvious to implement,
 and out of scope of current Catalyst project,
 but it is very much possible feature as well.
 
-### On-/Off-chain and spec code duplication
+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
 
 @todo #3: Add more off-chain code duplication examples from existing PABs.
     Include problems with querying coin-selection, tests, retrying and errors.
 
-### 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.
 
 ### Common backend features
 
@@ -274,12 +320,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