Initial API and examples closing M1

README.md

@@ -10,11 +10,20 @@
 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
 
+## Building
+
+Building is performed with cabal.
+Building requires `libblst` and `libsodium` installed.
+
+Arch Linux has `libblst` in AUR, nix are exemplified by IOHK,
+and manual installation is described here:
+https://github.com/input-output-hk/cardano-node-wiki/blob/main/docs/getting-started/install.md#installing-blst
+
 ## Project status
 
 Project is in early development stage and is funded by

cabal.project

@@ -11,8 +11,8 @@ repository cardano-haskell-packages
     d4a35cd3121aa00d18544bb0ac01c3e1691d618f462c46129271bccf39f7e8ee
 
 index-state:
-  , hackage.haskell.org 2023-11-03T12:09:05Z
-  , cardano-haskell-packages 2023-11-03T12:09:05Z
+  , hackage.haskell.org 2023-12-24T05:49:51Z
+  , cardano-haskell-packages 2023-12-24T05:54:15Z
 
 tests: true
 

cem-script.cabal

@@ -85,6 +85,7 @@ common common-lang
 common common-onchain
   import:        common-lang
   build-depends:
+    , plutus-core
     , plutus-ledger-api
     , plutus-tx
     , plutus-tx-plugin
@@ -106,7 +107,6 @@ common common-offchain
   build-depends:
     , bytestring
     , cardano-api
-    , cardano-ledger-core
     , containers
     , filepath
     , text
@@ -118,5 +118,15 @@ common common-executable
   ghc-options: -threaded -rtsopts
 
 library cem-sdk
-  import:          common-onchain
+  import:
+    common-onchain,
+    common-offchain
+
   hs-source-dirs:  src/
+  exposed-modules:
+    Cardano.CEM
+    Cardano.CEM.Examples.Auction
+    Cardano.CEM.Examples.Compilation
+    Cardano.CEM.Examples.Voting
+    Cardano.CEM.Monads
+    Cardano.CEM.OnChain

docs/arch_principles.md

@@ -0,0 +1,43 @@
+# 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)
+@todo #3: wording for almost-determinacy
+* Datum properties encoded as class types
+* Common on-chain optimizations are perfomed if possible
+    * Constraints normalization,  and CSE
+    * Best error short-cutting
+    * Common security problems prevention
+
+## Potential obstacles
+
+* Ease and optimality of backend compilation
+* Robustnes of SMT conversion and overall normalization
+* Possibility for parsing and correct offchain usage
+of almost-determinacy
+* Having enough information for Tx submit retrying strategies
+* Desing 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 determenistic transitions model