Add type files for proving system, compliance proving system, delta, and kind.

.github/workflows/clean-up.yaml

@@ -20,7 +20,7 @@ jobs:
   cleanup:
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v4.2.0
+      - uses: actions/checkout@v4
         with:
           ref: gh-pages
           clean: true

.github/workflows/deploy.yml

@@ -28,7 +28,7 @@ jobs:
   deploy:
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v4.2.0
+      - uses: actions/checkout@v4
         with:
           submodules: true
           fetch-depth: 0
@@ -41,14 +41,14 @@ jobs:
           MSG: "The build is in progress. Please wait for the preview link."
           GH_FLAGS: pr -R anoma/nspec comment ${{ github.event.pull_request.number }}
       - name: Install the right Juvix for the Specs
-        uses: jaxxstorm/action-install-gh-release@v1.12.0
+        uses: jaxxstorm/action-install-gh-release@v1
         with:
           repo: anoma/juvix
           tag: ${{ env.JUVIX_VERSION }}
           cache: enable
           rename-to: juvix
           chmod: 0755
-      - uses: actions/cache@v4.0.2
+      - uses: actions/cache@v4
         with:
           key: juvix-cache-${{ hashFiles('**/*.juvix.md') }}-${{ hashFiles('**/*.juvix') }}
           path: .juvix-build
@@ -59,11 +59,11 @@ jobs:
         run: |
           juvix typecheck docs/everything.juvix.md
       - name: Install Python
-        uses: actions/setup-python@v5.2.0
+        uses: actions/setup-python@v5
         with:
           python-version: ${{ env.PYTHON_VERSION }}
       - name: Install Poetry
-        uses: abatilo/actions-poetry@v3.0.0
+        uses: abatilo/actions-poetry@v3
         with:
           poetry-version: ${{ env.POETRY_VERSION }}
       - name: Setup a local virtual environment (if no poetry.toml file)
@@ -72,14 +72,14 @@ jobs:
           poetry config virtualenvs.in-project true --local
       - run: echo "cache_id=$(date --utc '+%V')-${{ hashFiles( '**/poetry.lock' )}}-${{ hashFiles( '**/*.py' )}}" >> $GITHUB_ENV
       - name: Cache .cache
-        uses: actions/cache@v4.0.2
+        uses: actions/cache@v4
         with:
           key: mkdocs-material-${{ env.cache_id }}
           path: .cache
           restore-keys: |
             mkdocs-material-
       - name: Cache .cache-juvix-mkdocs
-        uses: actions/cache@v4.0.2
+        uses: actions/cache@v4
         with:
           key: cache-juvix-mkdocs-${{ env.cache_id }}
           path: .cache-juvix-mkdocs
@@ -109,15 +109,15 @@ jobs:
           PROCESS_JUVIX: true
           TIMELIMIT: 100
       - if: success()
-        uses: JamesIves/github-pages-deploy-action@v4.6.4
+        uses: JamesIves/github-pages-deploy-action@v4
         with:
           folder: ${{ env.BRANCH_NAME }}
           target-folder: ${{ env.BRANCH_NAME }}
           token: ${{ secrets.GITHUB_TOKEN }}
           clean: false
           git-config-name: Anoma Research
           git-config-email: arts@heliax.dev
-      - uses: JamesIves/github-pages-deploy-action@v4.6.4
+      - uses: JamesIves/github-pages-deploy-action@v4
         with:
           folder: ${{ env.BRANCH_NAME }}
           target-folder: ${{ env.BRANCH_NAME }}

.github/workflows/pull-requests.yml

@@ -4,8 +4,6 @@
       - opened
       - synchronize
       - reopened
-      - edited
-      - ready_for_review
 env:
   CI: true
   GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}
@@ -32,7 +30,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout repository
-        uses: actions/checkout@v4.2.0
+        uses: actions/checkout@v4
         with:
           fetch-depth: 0
           ref: ${{ github.event.pull_request.head.ref }}
@@ -57,7 +55,7 @@ jobs:
     runs-on: ubuntu-latest
     concurrency: ci-${{ github.ref }}
     steps:
-      - uses: actions/checkout@v4.2.0
+      - uses: actions/checkout@v4
         with:
           submodules: true
           fetch-depth: 0
@@ -71,14 +69,14 @@ jobs:
           MSG: "The build is in progress. Please wait for the preview link."
           GH_FLAGS: pr -R anoma/nspec comment ${{ github.event.pull_request.number }}
       - name: Install the right Juvix for the Specs
-        uses: jaxxstorm/action-install-gh-release@v1.12.0
+        uses: jaxxstorm/action-install-gh-release@v1
         with:
           repo: anoma/juvix
           tag: ${{ env.JUVIX_VERSION }}
           cache: enable
           rename-to: juvix
           chmod: 0755
-      - uses: actions/cache@v4.0.2
+      - uses: actions/cache@v4
         with:
           key: juvix-cache-${{ hashFiles('**/*.juvix.md') }}-${{ hashFiles('**/*.juvix') }}
           path: .juvix-build
@@ -93,11 +91,11 @@ jobs:
         run: |
           juvix typecheck docs/everything.juvix.md
       - name: Install Python
-        uses: actions/setup-python@v5.2.0
+        uses: actions/setup-python@v5
         with:
           python-version: ${{ env.PYTHON_VERSION }}
       - name: Install Poetry
-        uses: abatilo/actions-poetry@v3.0.0
+        uses: abatilo/actions-poetry@v3
         with:
           poetry-version: ${{ env.POETRY_VERSION }}
       - name: Setup a local virtual environment (if no poetry.toml file)
@@ -106,14 +104,14 @@ jobs:
           poetry config virtualenvs.in-project true --local
       - run: echo "cache_id=$(date --utc '+%V')-${{ hashFiles( '**/poetry.lock' )}}-${{ hashFiles( '**/*.py' )}}" >> $GITHUB_ENV
       - name: Cache .cache
-        uses: actions/cache@v4.0.2
+        uses: actions/cache@v4
         with:
           key: mkdocs-material-${{ env.cache_id }}
           path: .cache
           restore-keys: |
             mkdocs-material-
       - name: Cache .cache-juvix-mkdocs
-        uses: actions/cache@v4.0.2
+        uses: actions/cache@v4
         with:
           key: .cache-juvix-mkdocs-${{ env.cache_id }}
           path: .cache-juvix-mkdocs
@@ -123,20 +121,6 @@ jobs:
         run: sudo apt-get install -y libcairo2-dev libfreetype6-dev libffi-dev libjpeg-dev libpng-dev libz-dev pngquant graphviz
       - name: Install Python dependencies
         run: poetry install
-      - name: Build MkDocs
-        id: mkdocs-basic
-        run: |
-          poetry run mkdocs build --clean --config-file mkdocs.yml --site-dir $SITE_DIR
-        env:
-          SITE_DIR: pr-${{ github.event.pull_request.number }}
-          SITE_URL: https://specs.anoma.net/pr-${{ github.event.pull_request.number }}/
-          SITE_VERSION: (PR ${{ github.event.pull_request.number }})
-          PROCESS_JUVIX: true
-          TIMELIMIT: 100
-      - name: The build failed comment
-        if: failure()
-        run: |
-          gh pr -R anoma/nspec comment ${{ github.event.pull_request.number }} --edit-last --body "The build failed. Please check the logs."
       - name: get the last commit short hash
         id: commit
         run: echo "::set-output name=commit::$(git rev-parse --short HEAD)"
@@ -165,7 +149,7 @@ jobs:
         continue-on-error: true
       - name: Deploy MkDocs with insiders theme
         if: success()
-        uses: JamesIves/github-pages-deploy-action@v4.6.4
+        uses: JamesIves/github-pages-deploy-action@v4
         with:
           repository-name: anoma/nspec
           branch: gh-pages
@@ -194,3 +178,49 @@ jobs:
         run: |
           gh pr -R anoma/nspec comment ${{ github.event.pull_request.number }} --edit-last --body "The preview of this PR failed to build. Check the logs."
         continue-on-error: true
+  build-basic: # without insiders and juvix
+    runs-on: ubuntu-latest
+    concurrency: ci-basic-${{ github.ref }}
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          submodules: true
+          fetch-depth: 0
+      - name: Install Python
+        uses: actions/setup-python@v5
+        with:
+          python-version: ${{ env.PYTHON_VERSION }}
+      - name: Install Poetry
+        uses: abatilo/actions-poetry@v3
+        with:
+          poetry-version: ${{ env.POETRY_VERSION }}
+      - name: Setup a local virtual environment (if no poetry.toml file)
+        run: |
+          poetry config virtualenvs.create true --local
+          poetry config virtualenvs.in-project true --local
+      - run: echo "cache_id=$(date --utc '+%V')-${{ hashFiles( '**/poetry.lock' )}}-${{ hashFiles( '**/*.py' )}}" >> $GITHUB_ENV
+      - name: Cache .cache
+        uses: actions/cache@v4
+        with:
+          key: mkdocs-basic-material-${{ env.cache_id }}
+          path: .cache
+          restore-keys: |
+            mkdocs-basic-material-
+      - name: Install Linux dependencies
+        run: sudo apt-get install -y libcairo2-dev libfreetype6-dev libffi-dev libjpeg-dev libpng-dev libz-dev pngquant graphviz
+      - name: Install Python dependencies
+        run: poetry install
+      - name: Build MkDocs
+        id: mkdocs-basic
+        run: |
+          poetry run mkdocs build --clean --config-file mkdocs.yml --site-dir $SITE_DIR
+        env:
+          SITE_DIR: pr-${{ github.event.pull_request.number }}
+          SITE_URL: https://specs.anoma.net/pr-${{ github.event.pull_request.number }}/
+          SITE_VERSION: (PR ${{ github.event.pull_request.number }})
+          PROCESS_JUVIX: false
+          TIMELIMIT: 100
+      - name: The build failed comment
+        if: failure()
+        run: |
+          gh pr -R anoma/nspec comment ${{ github.event.pull_request.number }} --edit-last --body "The build failed. Please check the logs."

docs/arch/system/state/resource_machine/prelude.juvix.md

@@ -67,6 +67,42 @@ syntax alias LabelHash := Digest;
 syntax alias LogicHash := Digest;
 ```
 
+#### `LogicRef`
+
+```juvix
+syntax alias LogicRef := LogicHash;
+```
+
+#### `KindHash`
+
+```juvix
+syntax alias KindHash := Digest;
+```
+
+#### `ExtraInput`
+
+```juvix
+syntax alias ExtraInput := ByteString;
+```
+
+#### `NullifierRef`
+
+```juvix
+syntax alias NullifierRef := Digest;
+```
+
+#### `RootRef`
+
+```juvix
+syntax alias RootRef      := Digest;
+```
+
+#### `CommitmentRef`
+
+```juvix
+syntax alias CommitmentRef := Digest;
+```
+
 #### `Quantity`
 
 There are two numeric types of unspecified character mentioned in the RM, which
@@ -380,6 +416,16 @@ orderedSetFromList
     (mkOrderedSet Set.empty []);
 ```
 
+#### `orderedSetMap`
+
+```juvix
+orderedSetMap
+  {A B} {{Ord A}} {{Ord B}}
+  (f : A -> B)
+  (s : OrderedSet A) : OrderedSet B :=
+  orderedSetFromList (map f (orderedSetToList s));
+```
+
 #### `IOrderedSet` instance for `OrderedSet`
 
 ```juvix