DO NOT REVIEW: Wasm erc20

.github/workflows/test-pr.yml

@@ -1,48 +1,24 @@
 name: 'Run Tests'
 on:
   pull_request:
+  push:
+    branches:
+      - 'master-update'
   workflow_dispatch:
 concurrency:
   group: ${{ github.workflow }}-${{ github.ref }}
   cancel-in-progress: true
 
 jobs:
 
-  version-bump:
-    name: 'Version Bump'
-    runs-on: [self-hosted, linux, flyweight-ephemeral]
-    steps:
-      - name: 'Check out code'
-        uses: actions/checkout@v3
-        with:
-          token: ${{ secrets.JENKINS_GITHUB_PAT }}
-          # fetch-depth 0 means deep clone the repo
-          fetch-depth: 0
-          ref: ${{ github.event.pull_request.head.sha }}
-      - name: 'Configure GitHub user'
-        run: |
-          git config user.name devops
-          git config user.email [email protected]
-      - name: 'Update version'
-        run: |
-          og_version=$(git show origin/${GITHUB_BASE_REF}:package/version)
-          ./package/version.sh bump ${og_version}
-          ./package/version.sh sub
-          new_version=$(cat package/version)
-          git add --update && git commit --message "Set Version: ${new_version}" || true
-      - name: 'Push updates'
-        run: git push origin HEAD:${GITHUB_HEAD_REF}
-
   pykwasm-code-quality-checks:
     name: 'Code Quality Checks'
     runs-on: ubuntu-latest
     steps:
       - name: 'Check out code'
-        uses: actions/checkout@v3
-        with:
-          submodules: recursive
+        uses: actions/checkout@v4
       - name: 'Install Poetry'
-        uses: Gr1N/setup-poetry@v8
+        uses: Gr1N/setup-poetry@v9
       - name: 'Build pykwasm'
         run: poetry -C pykwasm install
       - name: 'Run code quality checks'
@@ -82,52 +58,3 @@ jobs:
         if: always()
         run: |
           docker stop --time=0 kwasm-ci-conformance-${GITHUB_SHA}
-
-  prove-tests:
-    name: 'Prover Tests'
-    needs: pykwasm-code-quality-checks
-    runs-on: [self-hosted, linux, normal]
-    timeout-minutes: 30
-    steps:
-      - name: 'Check out code'
-        uses: actions/checkout@v3
-        with:
-          submodules: recursive
-      - name: 'Set up Docker'
-        uses: ./.github/actions/with-docker
-        with:
-          container-name: kwasm-ci-prove-${{ github.sha }}
-      - name: 'Build pykwasm'
-        run: docker exec -u user kwasm-ci-prove-${GITHUB_SHA} poetry -C pykwasm install
-      - name: 'Build Haskell definitions'
-        run: docker exec -u user kwasm-ci-prove-${GITHUB_SHA} poetry -C pykwasm run kdist -v build wasm-semantics.{kwasm-lemmas,wrc20} -j2
-      - name: 'Run prover tests'
-        run: docker exec -u user kwasm-ci-prove-${GITHUB_SHA} make -j6 test-prove
-      - name: 'Tear down Docker'
-        if: always()
-        run: |
-          docker stop --time=0 kwasm-ci-prove-${GITHUB_SHA}
-
-  nix:
-    name: 'Nix'
-    strategy:
-      fail-fast: false
-      matrix:
-        include:
-          - runner: normal
-          - runner: ARM64
-    needs: pykwasm-code-quality-checks
-    runs-on: ${{ matrix.runner }}
-    timeout-minutes: 60
-    steps:
-      - name: 'Check out code'
-        uses: actions/checkout@v3
-        with:
-          # Check out pull request HEAD instead of merge commit.
-          ref: ${{ github.event.pull_request.head.sha }}
-      - name: 'Build KWASM'
-        run: GC_DONT_GC=1 nix build .#kwasm --extra-experimental-features 'nix-command flakes' --print-build-logs
-      - name: 'Build KWASM-Pyk'
-        run: GC_DONT_GC=1 nix build .#kwasm-pyk --extra-experimental-features 'nix-command flakes' --print-build-logs
-      - name: 'Test KWASM'
-        run: GC_DONT_GC=1 nix build .#kwasm-test --extra-experimental-features 'nix-command flakes' --print-build-logs

.github/workflows/update-version.yml

@@ -15,7 +15,7 @@ jobs:
     runs-on: ubuntu-22.04
     steps:
       - name: 'Check out code'
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           submodules: recursive
           token: ${{ secrets.JENKINS_GITHUB_PAT }}
@@ -24,30 +24,11 @@ jobs:
           git config user.email [email protected]
       - name: 'Install Poetry'
         uses: Gr1N/setup-poetry@v8
-      - name: 'Install Nix'
-        uses: cachix/install-nix-action@v22
-        with:
-          install_url: https://releases.nixos.org/nix/nix-2.13.3/install
-          extra_nix_config: |
-            access-tokens = github.com=${{ secrets.GITHUB_TOKEN }}
-            substituters = http://cache.nixos.org https://hydra.iohk.io
-            trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= hydra.iohk.io:f/Ea+s+dFdN+3Y/G+FDgSq+a5NEWhJGzdjvKNGv0/EQ=
-      - name: 'Install Cachix'
-        uses: cachix/cachix-action@v14
-        with:
-          name: k-framework
-          authToken: '${{ secrets.CACHIX_PUBLIC_TOKEN }}'
       - name: 'Update pyk release tag'
         run: |
           K_VERSION=$(cat deps/k_release)
           sed -i 's!kframework = "[v0-9\.]*"!kframework = "'${K_VERSION}'"!' pykwasm/pyproject.toml
           poetry -C pykwasm update
           git add pykwasm/ && git commit -m "pykwasm/: sync poetry files ${K_VERSION}" || true
-      - name: 'Update Nix flake inputs'
-        run: |
-          K_VERSION=v"$(cat deps/k_release)"
-          sed -i 's!    k-framework.url = "github:runtimeverification/k/v[[:digit:]]\+\.[[:digit:]]\+\.[[:digit:]]\+"!    k-framework.url = "github:runtimeverification/k/'"${K_VERSION}"'"!' flake.nix
-          nix flake update
-          git add flake.nix flake.lock && git commit -m 'flake.{nix,lock}: update Nix derivations' || true
       - name: 'Push updates'
         run: git push

pykwasm/src/pykwasm/kdist/plugin.py

@@ -30,8 +30,16 @@ def __init__(self, kompile_args: Callable[[Path], Mapping[str, Any]]):
         self._kompile_args = kompile_args
 
     def build(self, output_dir: Path, deps: dict[str, Path], args: dict[str, Any], verbose: bool) -> None:
+        llvm_proof_hint_debugging = bool(args.get('llvm-proof-hint-debugging', ''))
+        llvm_proof_hint_instrumentation = bool(args.get('llvm-proof-hint-instrumentation', ''))
         kompile_args = self._kompile_args(deps['wasm-semantics.source'])
-        kompile(output_dir=output_dir, verbose=verbose, **kompile_args)
+        kompile(
+            output_dir=output_dir,
+            verbose=verbose,
+            llvm_proof_hint_debugging=llvm_proof_hint_debugging,
+            llvm_proof_hint_instrumentation=llvm_proof_hint_instrumentation,
+            **kompile_args,
+        )
 
     def context(self) -> dict[str, str]:
         return {'k-version': k_version().text}

pykwasm/src/pykwasm/kdist/wasm-semantics/auxil.md

@@ -24,7 +24,7 @@ module WASM-AUXIL
          <instrs> #clearConfig => .K ...    </instrs>
          <curModIdx>         _ => .Int      </curModIdx>
          <valstack>          _ => .ValStack </valstack>
-         <locals>            _ => .Map      </locals>
+         <locals>            _ => .List     </locals>
          <moduleInstances>   _ => .Bag      </moduleInstances>
          <moduleIds>         _ => .Map      </moduleIds>
          <nextModuleIdx>     _ => 0         </nextModuleIdx>
@@ -34,8 +34,7 @@ module WASM-AUXIL
            <funcs>           _ => .Bag      </funcs>
            <nextTabAddr>     _ => 0         </nextTabAddr>
            <tabs>            _ => .Bag      </tabs>
-           <nextMemAddr>     _ => 0         </nextMemAddr>
-           <mems>            _ => .Bag      </mems>
+           <mems>            _ => .List     </mems>
            <nextGlobAddr>    _ => 0         </nextGlobAddr>
            <globals>         _ => .Bag      </globals>
            <nextElemAddr>    _ => 0         </nextElemAddr>

pykwasm/src/pykwasm/kdist/wasm-semantics/test.md

@@ -430,7 +430,8 @@ The operator `#assertLocal`/`#assertGlobal` operators perform a check for a loca
 
 ```k
     rule <instrs> #assertLocal INDEX VALUE _ => .K ... </instrs>
-         <locals> ... INDEX |-> VALUE ... </locals>
+         <locals> LOCALS </locals>
+      requires LOCALS[INDEX] ==K VALUE
 
     rule <instrs> #assertGlobal TFIDX VALUE _ => .K ... </instrs>
          <curModIdx> CUR </curModIdx>
@@ -569,37 +570,25 @@ This checks that the last allocated memory has the given size and max value.
          <moduleInst>
            <modIdx> CUR </modIdx>
            <memIds> IDS </memIds>
-           <memAddrs> #ContextLookup(IDS, TFIDX) |-> ADDR </memAddrs>
+           <memAddrs> ListItem(ADDR) </memAddrs>
            ...
          </moduleInst>
-         <mems>
-           <memInst>
-             <mAddr>   ADDR  </mAddr>
-             <mmax>    MAX   </mmax>
-             <msize>   SIZE  </msize>
-             ...
-           </memInst>
-           ...
-         </mems>
+         <mems> MEMS </mems>
+      requires ADDR <Int size(MEMS)
+        andBool #ContextLookup(IDS, TFIDX) ==K 0 andBool (#let memInst(MAX', SIZE', _) = MEMS[ADDR] #in MAX ==K MAX' andBool SIZE ==K SIZE')
 
     rule <instrs> #assertMemoryData (KEY , VAL) MSG => #assertMemoryData CUR (KEY, VAL) MSG ... </instrs>
          <curModIdx> CUR </curModIdx>
 
     rule <instrs> #assertMemoryData MODIDX (KEY , VAL) _MSG => .K ... </instrs>
          <moduleInst>
            <modIdx> MODIDX </modIdx>
-           <memAddrs> 0 |-> ADDR </memAddrs>
+           <memAddrs> ListItem(ADDR) </memAddrs>
            ...
          </moduleInst>
-         <mems>
-           <memInst>
-             <mAddr> ADDR </mAddr>
-             <mdata> BM </mdata>
-             ...
-           </memInst>
-           ...
-         </mems>
-      requires #getRange(BM, KEY, 1) ==Int VAL
+         <mems> MEMS </mems>
+      requires ADDR <Int size(MEMS)
+        andBool (#let memInst(_, _, BM) = MEMS[ADDR] #in #getRange(BM, KEY, 1) ==Int VAL)
 ```
 
 ### Module Assertions

pykwasm/src/pykwasm/kdist/wasm-semantics/wasm-text.md

@@ -1188,7 +1188,6 @@ They are currently supported in KWasm text files, but may be deprecated.
 
     rule #t2aInstr<C>(#block(VT:VecType, IS:Instrs, BLOCKINFO)) => #block(VT, #t2aInstrs<C>(IS), BLOCKINFO)
 
-    rule #t2aInstr<_>(init_local I V) => init_local I V
     rule #t2aInstr<_>(init_locals VS) => init_locals VS
 ```