Merge pull request mlabs-haskell#11 from mlabs-haskell/uhbif19/initia…

…l-docs

Initial docs

.gitignore

@@ -21,3 +21,4 @@ cabal.project.local
 cabal.project.local~
 .HTF/
 .ghc.environment.*
+.vscode

README.md

@@ -10,7 +10,7 @@
 Define and reuse Cardano DApp logic via annotated CEM-machines, resulting in free implementations for:
 
 * On-chain scripts
-* Tx building/submission/resubmission on L1/L2/emulated testnet
+* Tx building/submission/resubmission on L1/emulated testnet
 * Tx parsing/indexing
 * Automatically testing invariants
 * Human-readable specs

docs/arch_principles.md

@@ -0,0 +1,42 @@
+# Constraints design
+
+## Principles
+
+* Generic compilation across: on-chain code,
+offchain Tx construction and indexing backend
+* Simple normalization and SMT conversion for:
+    * Equivalence checking
+    * Bi-simulation checking
+* Constraints determine TxIn/Outs up to UTxO coin-selection
+(we call it almost-determinacy)
+* Datum properties encoded as class types
+* Common on-chain optimizations are performed if possible
+    * Constraints normalization,  and CSE
+    * Best error short-cutting
+    * Common security problems prevention
+
+## Potential obstacles
+
+* Ease and optimality of backend compilation
+* Robustness of SMT conversion and overall normalization
+* Possibility for parsing and correct offchain usage
+of almost-determinacy
+* Having enough information for Tx submit retrying strategies
+* Design for using custom Datum properties is not obvious
+
+# CEM machine design
+
+As it is done on top of constraints language,
+all their principles and obstacles are affecting CEM as well.
+
+## Principles
+
+* State-machine is deterministic modulo coin-change
+    * Transaction can always be parsed back into SM transitions
+    * Potential non-deterministic on-chain optimizations
+    should not affect this principle.
+
+## Potential obstacles
+
+* Some scripts inexpressible by such model (as it happens in PAB)
+* Sub-optimal code from deterministic transitions model