Merge subtree raduom/hysterical screams into plutus-hysterical-screams

.stylish-haskell.yaml

@@ -28,4 +28,6 @@ language_extensions:
   - PackageImports
   - QuasiQuotes
   - ScopedTypeVariables
-  - TemplateHaskell
+  - TemplateHaskell
+  - TypeApplications
+  - ImportQualifiedPost

plutus-hysterical-screams/.github/workflows/haskell-ci.yml

@@ -0,0 +1,183 @@
+# This GitHub workflow config has been generated by a script via
+#
+#   haskell-ci 'github' 'hysterical-screams.cabal'
+#
+# To regenerate the script (for example after adjusting tested-with) run
+#
+#   haskell-ci regenerate
+#
+# For more information, see https://github.com/haskell-CI/haskell-ci
+#
+# version: 0.14.1
+#
+# REGENDATA ("0.14.1",["github","hysterical-screams.cabal"])
+#
+name: Haskell-CI
+on:
+  - push
+  - pull_request
+jobs:
+  linux:
+    name: Haskell-CI - Linux - ${{ matrix.compiler }}
+    runs-on: ubuntu-18.04
+    timeout-minutes:
+      60
+    container:
+      image: buildpack-deps:bionic
+    continue-on-error: ${{ matrix.allow-failure }}
+    strategy:
+      matrix:
+        include:
+          - compiler: ghc-8.10.7
+            compilerKind: ghc
+            compilerVersion: 8.10.7
+            setup-method: ghcup
+            allow-failure: false
+      fail-fast: false
+    steps:
+      - name: apt
+        run: |
+          apt-get update
+          apt-get install -y --no-install-recommends gnupg ca-certificates dirmngr curl git software-properties-common libtinfo5
+          mkdir -p "$HOME/.ghcup/bin"
+          curl -sL https://downloads.haskell.org/ghcup/0.1.17.3/x86_64-linux-ghcup-0.1.17.3 > "$HOME/.ghcup/bin/ghcup"
+          chmod a+x "$HOME/.ghcup/bin/ghcup"
+          "$HOME/.ghcup/bin/ghcup" install ghc "$HCVER"
+          "$HOME/.ghcup/bin/ghcup" install cabal 3.6.2.0
+        env:
+          HCKIND: ${{ matrix.compilerKind }}
+          HCNAME: ${{ matrix.compiler }}
+          HCVER: ${{ matrix.compilerVersion }}
+      - name: Set PATH and environment variables
+        run: |
+          echo "$HOME/.cabal/bin" >> $GITHUB_PATH
+          echo "LANG=C.UTF-8" >> "$GITHUB_ENV"
+          echo "CABAL_DIR=$HOME/.cabal" >> "$GITHUB_ENV"
+          echo "CABAL_CONFIG=$HOME/.cabal/config" >> "$GITHUB_ENV"
+          HCDIR=/opt/$HCKIND/$HCVER
+          HC=$HOME/.ghcup/bin/$HCKIND-$HCVER
+          echo "HC=$HC" >> "$GITHUB_ENV"
+          echo "HCPKG=$HOME/.ghcup/bin/$HCKIND-pkg-$HCVER" >> "$GITHUB_ENV"
+          echo "HADDOCK=$HOME/.ghcup/bin/haddock-$HCVER" >> "$GITHUB_ENV"
+          echo "CABAL=$HOME/.ghcup/bin/cabal-3.6.2.0 -vnormal+nowrap" >> "$GITHUB_ENV"
+          HCNUMVER=$(${HC} --numeric-version|perl -ne '/^(\d+)\.(\d+)\.(\d+)(\.(\d+))?$/; print(10000 * $1 + 100 * $2 + ($3 == 0 ? $5 != 1 : $3))')
+          echo "HCNUMVER=$HCNUMVER" >> "$GITHUB_ENV"
+          echo "ARG_TESTS=--enable-tests" >> "$GITHUB_ENV"
+          echo "ARG_BENCH=--enable-benchmarks" >> "$GITHUB_ENV"
+          echo "HEADHACKAGE=false" >> "$GITHUB_ENV"
+          echo "ARG_COMPILER=--$HCKIND --with-compiler=$HC" >> "$GITHUB_ENV"
+          echo "GHCJSARITH=0" >> "$GITHUB_ENV"
+        env:
+          HCKIND: ${{ matrix.compilerKind }}
+          HCNAME: ${{ matrix.compiler }}
+          HCVER: ${{ matrix.compilerVersion }}
+      - name: env
+        run: |
+          env
+      - name: write cabal config
+        run: |
+          mkdir -p $CABAL_DIR
+          cat >> $CABAL_CONFIG <<EOF
+          remote-build-reporting: anonymous
+          write-ghc-environment-files: never
+          remote-repo-cache: $CABAL_DIR/packages
+          logs-dir:          $CABAL_DIR/logs
+          world-file:        $CABAL_DIR/world
+          extra-prog-path:   $CABAL_DIR/bin
+          symlink-bindir:    $CABAL_DIR/bin
+          installdir:        $CABAL_DIR/bin
+          build-summary:     $CABAL_DIR/logs/build.log
+          store-dir:         $CABAL_DIR/store
+          install-dirs user
+            prefix: $CABAL_DIR
+          repository hackage.haskell.org
+            url: http://hackage.haskell.org/
+          EOF
+          cat >> $CABAL_CONFIG <<EOF
+          program-default-options
+            ghc-options: $GHCJOBS +RTS -M3G -RTS
+          EOF
+          cat $CABAL_CONFIG
+      - name: versions
+        run: |
+          $HC --version || true
+          $HC --print-project-git-commit-id || true
+          $CABAL --version || true
+      - name: update cabal index
+        run: |
+          $CABAL v2-update -v
+      - name: install cabal-plan
+        run: |
+          mkdir -p $HOME/.cabal/bin
+          curl -sL https://github.com/haskell-hvr/cabal-plan/releases/download/v0.6.2.0/cabal-plan-0.6.2.0-x86_64-linux.xz > cabal-plan.xz
+          echo 'de73600b1836d3f55e32d80385acc055fd97f60eaa0ab68a755302685f5d81bc  cabal-plan.xz' | sha256sum -c -
+          xz -d < cabal-plan.xz > $HOME/.cabal/bin/cabal-plan
+          rm -f cabal-plan.xz
+          chmod a+x $HOME/.cabal/bin/cabal-plan
+          cabal-plan --version
+      - name: checkout
+        uses: actions/checkout@v2
+        with:
+          path: source
+      - name: initial cabal.project for sdist
+        run: |
+          touch cabal.project
+          echo "packages: $GITHUB_WORKSPACE/source/." >> cabal.project
+          cat cabal.project
+      - name: sdist
+        run: |
+          mkdir -p sdist
+          $CABAL sdist all --output-dir $GITHUB_WORKSPACE/sdist
+      - name: unpack
+        run: |
+          mkdir -p unpacked
+          find sdist -maxdepth 1 -type f -name '*.tar.gz' -exec tar -C $GITHUB_WORKSPACE/unpacked -xzvf {} \;
+      - name: generate cabal.project
+        run: |
+          PKGDIR_hysterical_screams="$(find "$GITHUB_WORKSPACE/unpacked" -maxdepth 1 -type d -regex '.*/hysterical-screams-[0-9.]*')"
+          echo "PKGDIR_hysterical_screams=${PKGDIR_hysterical_screams}" >> "$GITHUB_ENV"
+          rm -f cabal.project cabal.project.local
+          touch cabal.project
+          touch cabal.project.local
+          echo "packages: ${PKGDIR_hysterical_screams}" >> cabal.project
+          echo "package hysterical-screams" >> cabal.project
+          echo "    ghc-options: -Werror=missing-methods" >> cabal.project
+          cat >> cabal.project <<EOF
+          EOF
+          $HCPKG list --simple-output --names-only | perl -ne 'for (split /\s+/) { print "constraints: $_ installed\n" unless /^(hysterical-screams)$/; }' >> cabal.project.local
+          cat cabal.project
+          cat cabal.project.local
+      - name: dump install plan
+        run: |
+          $CABAL v2-build $ARG_COMPILER $ARG_TESTS $ARG_BENCH --dry-run all
+          cabal-plan
+      - name: cache
+        uses: actions/cache@v2
+        with:
+          key: ${{ runner.os }}-${{ matrix.compiler }}-${{ github.sha }}
+          path: ~/.cabal/store
+          restore-keys: ${{ runner.os }}-${{ matrix.compiler }}-
+      - name: install dependencies
+        run: |
+          $CABAL v2-build $ARG_COMPILER --disable-tests --disable-benchmarks --dependencies-only -j2 all
+          $CABAL v2-build $ARG_COMPILER $ARG_TESTS $ARG_BENCH --dependencies-only -j2 all
+      - name: build w/o tests
+        run: |
+          $CABAL v2-build $ARG_COMPILER --disable-tests --disable-benchmarks all
+      - name: build
+        run: |
+          $CABAL v2-build $ARG_COMPILER $ARG_TESTS $ARG_BENCH all --write-ghc-environment-files=always
+      - name: tests
+        run: |
+          $CABAL v2-test $ARG_COMPILER $ARG_TESTS $ARG_BENCH all --test-show-details=direct
+      - name: cabal check
+        run: |
+          cd ${PKGDIR_hysterical_screams} || false
+          ${CABAL} -vnormal check
+      - name: haddock
+        run: |
+          $CABAL v2-haddock $ARG_COMPILER --with-haddock $HADDOCK $ARG_TESTS $ARG_BENCH all
+      - name: unconstrained build
+        run: |
+          rm -f cabal.project.local
+          $CABAL v2-build $ARG_COMPILER --disable-tests --disable-benchmarks all

plutus-hysterical-screams/.gitignore

@@ -0,0 +1,3 @@
+.stack-work/
+dist-newstyle/
+*~

plutus-hysterical-screams/ChangeLog.md

@@ -0,0 +1,3 @@
+# Changelog for utxo-index
+
+## Unreleased changes

plutus-hysterical-screams/LICENSE

@@ -0,0 +1,30 @@
+Copyright Author name here (c) 2022
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of Author name here nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

plutus-hysterical-screams/README.md

@@ -0,0 +1,62 @@
+# historical-streams
+
+[![Haskell-CI](https://github.com/raduom/hysterical-screams/actions/workflows/haskell-ci.yml/badge.svg)](https://github.com/raduom/hysterical-screams/actions/workflows/haskell-ci.yml)
+
+# A study of algebraic specification.
+
+## Define a simplified model.
+
+We want to define an indexing data structure that has the capacity of maintaining a current state (viewed as a fold over a stream of events) and which can rewind to a previous value in case a rollback happens on the stream. We only store K (we call it depth) versions of the previous accumulator (since we know that we will only rollback at most K blocks).
+
+The model is split between constructors and observations. You can identify the constructors with a grammar that generates a program in your algebra and observations define the semantics of this defined language.
+
+Example of a program in this algebra: `rewind 1 $ insert 1 $ new (+) 5`. We can think as the value of the accumulator at the end of running this program as an observation which has value `5`.
+
+I our case we have three constructors:
+* new => creates a new index, and takes as arguments a function used to fold events into an accumulator and an initial value for the accumulator.
+* insert => adds a new event into the index
+* rewind => returns the data structure to a previous version.
+
+.. and 3 observations:
+* view:
+ * depth - how many versions do we remember
+ * size - how many versions do we currently store.
+ * accumulator value - what is the current value of the accumulator.
+* history (the historical accumulator values)
+* function (looks up the function used for folding)
+
+One of the mistakes I made initially was to include the possiblity of failing when building syntax (new and review could return `Nothing`). In retrospect this was a bad decision because it would not allow me to test the negative of the property for other data types. I removed all possibilities of errors from the constructors and moved them to the observations.
+
+On this model we identify some properties by specifying how our observations are influenced by the chaining of constructors.
+
+1) *observeNew* talks about what we can observe from viewing or getting the history after a call to `new`. If the depth is negative then all observations should return `Nothing`.
+
+2) *rewindDepth* checks that observations of rewind are only valid when the number of events we want to undo is lower than what we have stored (and by proxy is lower than the maximum depth of the data structure).
+
+3) *rewindInverse* captures that intuition that (under very specific conditions) insert and rewind behave a bit like inverses.
+
+4) *observeInsert* captures the way insert changes observations. This is one of the gripes I've had with testing for a while when you write tests that duplicate the code used to implement the functions you are testing. However, in this case it makes sense, since this property is not used to check our model as much as check other, more complex data structures that we check for conformity with the model.
+
+5) *sizeLEDepth* this is an invariant for the data structure. Size should always be less than the maximum size. I am not sure I want to keep this property. It does not seem very useful, but it's an example of an invariant.
+
+## Define a more complex data type
+
+I define a more efficient data type based on the observation that part of the chain is immutable and the part that is immutable could be stored fully on disk. Then we would only use RAM to store the changes that happened in the mutable part of the blockchain.
+
+The structure is a bit more complex in order to support batching events to be persisted more efficiently.
+
+The way I implemented the verification that this data structure is compliant with the properties identified for the model previously defined is by generalising the properties themselves by providing functions that convert between model programs and observations of the complex data structures.
+
+To test the properties for the initial model we use the `Identity` monad and the view conversion functions are the ones defined by the `Index` module.
+
+For the complex data structure the flow is as follow: given an Index program that has one pure observation derived from the model, it must match the complex observation of the data structure.
+
+## Lessons learned
+
+* The first implementation of the simplified model was not algebraic and it was awkward to think of a more complex data structure as a interpretation of a language. So, when defining a model, thinking in terms of constructors and observations seems very important. Then what we get is something equivalent to a free algebra (hence algebraic specification).
+* The process of developing things in this manner is fairly slow and tenuous, but it does force one to contemplate the design choices that were made and think deeply about the meaning of the used data structures (do we need to expose a size or a depth in our views? why? what happens if we do not do that?).
+* The process *is* an interative one, where the model changes informed by requirements from the software, and the software changes to satisfy the properties required by the model. Both the model and the implementation have changed several times, and they will probably keep on changing (test don't pass yet for the complex data structure).
+* Thinking about these problems has given me a lot more insight into the problem that we are trying to solve and I could identify easily shortcomings, inefficiencies or unwaranted complexity of other approaches.
+* The amount of bugs that only 5 properties can detect is impresive. Not all of those were actual reasoning failings, but some were (a couple of bugs were off-by-one errors).
+* The amount of bugs that can fit into a more complex than the model, but not really that complex data structure is also quite impressive.
+* Finding the cause of property violations is not very fun, but not incredibly annoying either. I think there are improvements to be made in this area.

plutus-hysterical-screams/Setup.hs

@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain