From a492ed920da0b531947ad00f9daff031e168a7e7 Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Fri, 15 Nov 2024 13:16:12 -0500 Subject: [PATCH 01/97] ci --- .github/workflows/ci.yml | 0 1 file changed, 0 insertions(+), 0 deletions(-) create mode 100644 .github/workflows/ci.yml diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml new file mode 100644 index 00000000..e69de29b From f428ba1235da308403c9831b076022a689c21ab1 Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Fri, 15 Nov 2024 13:23:01 -0500 Subject: [PATCH 02/97] add stylebot --- .github/workflows/ci.yml | 0 .github/workflows/stylebot.yaml | 67 +++++++++++++++++++++++++++++++++ 2 files changed, 67 insertions(+) delete mode 100644 .github/workflows/ci.yml create mode 100644 .github/workflows/stylebot.yaml diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml deleted file mode 100644 index e69de29b..00000000 diff --git a/.github/workflows/stylebot.yaml b/.github/workflows/stylebot.yaml new file mode 100644 index 00000000..dcaac271 --- /dev/null +++ b/.github/workflows/stylebot.yaml @@ -0,0 +1,67 @@ +name: stylebot +on: + push: + branches: + - master +concurrency: + group: "stylebot" + cancel-in-progress: true +permissions: + id-token: write + contents: write + packages: write + pull-requests: write +jobs: + fix: + runs-on: ubuntu-latest + + steps: + - uses: actions/create-github-app-token@v1 + id: app-token + with: + app-id: ${{ secrets.STYLEBOT_GITHUB_APP_ID }} + private-key: ${{ secrets.STYLEBOT_GITHUB_APP_KEY }} + - uses: actions/checkout@master + - id: nodeversion + run: echo "version=$(grep nodejs .tool-versions | sed -e 's/[^[:space:]]*[[:space:]]*//')" >> $GITHUB_OUTPUT + - uses: actions/setup-node@v4 + with: + node-version: ${{ steps.nodeversion.outputs.version }} + cache: yarn + - run: yarn install --immutable + # Run fixes, save stdout. + - run: | + echo 'ESLINT_RESULTS<> ${GITHUB_ENV} + yarn fix:eslint >> ${GITHUB_ENV} || true + echo 'EOF' >> ${GITHUB_ENV} + - run: | + echo 'PRETTIER_RESULTS<> ${GITHUB_ENV} + yarn fix:prettier >> ${GITHUB_ENV} + echo 'EOF' >> ${GITHUB_ENV} + - run: git restore .yarn .yarnrc.yml + # Make PR from local changes. + - name: Create Pull Request + uses: peter-evans/create-pull-request@v7 + with: + token: ${{ steps.app-token.outputs.token }} + commit-message: "[stylebot] Fixes for code style" + branch: stylebot/patch + title: "[stylebot] Fixes for code style" + body: | + Stylebot detected automatically fix-able code style issues. + +
`yarn fix:eslint` + + ``` + ${{ env.ESLINT_RESULTS }} + ``` + +
+ +
`yarn fix:prettier` + + ``` + ${{ env.PRETTIER_RESULTS }} + ``` + +
From c4b628a6843399664335d115c8bf6e373e6cb8bc Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Fri, 15 Nov 2024 13:37:15 -0500 Subject: [PATCH 03/97] ci again --- .github/workflows/ci.yaml | 32 ++++++++++++++++++++++++++++++++ 1 file changed, 32 insertions(+) create mode 100644 .github/workflows/ci.yaml diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml new file mode 100644 index 00000000..6d8c2cb3 --- /dev/null +++ b/.github/workflows/ci.yaml @@ -0,0 +1,32 @@ +name: CI +on: [push] +jobs: + test: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@master + with: + fetch-depth: 0 + submodules: recursive + - uses: foundry-rs/foundry-toolchain@v1 + - run: forge test -vvv + - run: forge snapshot + formal-verification: + runs-on: ubuntu-latest + needs: test + steps: + - uses: actions/checkout@master + with: + fetch-depth: 0 + submodules: recursive + - name: Install Kontrol + run: | + bash <(curl https://kframework.org/install) + kup install kontrol + - name: Build and Run Proofs + run: | + kontrol build + kontrol prove --config-profile setup + kontrol prove --config-profile tests + - name: View Results + run: kontrol list \ No newline at end of file From 612bee4286aee1ccfb8487b9d2e31ca58f580dc4 Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Fri, 15 Nov 2024 13:43:43 -0500 Subject: [PATCH 04/97] update ci with forge update --- .github/workflows/ci.yaml | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index 6d8c2cb3..727c038e 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -9,6 +9,12 @@ jobs: fetch-depth: 0 submodules: recursive - uses: foundry-rs/foundry-toolchain@v1 + with: + version: nightly + - name: Install forge-std + run: | + forge install foundry-rs/forge-std --no-commit + forge remappings > remappings.txt - run: forge test -vvv - run: forge snapshot formal-verification: From f4341924f36d17ef2c57b681c6e58ebdba5761ac Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Fri, 15 Nov 2024 13:46:41 -0500 Subject: [PATCH 05/97] non-kontrol unit tests only --- .github/workflows/ci.yaml | 4 +++- lib/forge-std | 2 +- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index 727c038e..658aec66 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -15,7 +15,9 @@ jobs: run: | forge install foundry-rs/forge-std --no-commit forge remappings > remappings.txt - - run: forge test -vvv + - name: Run non-Kontrol tests + run: | + forge test --no-match-path "src/test/kontrol/*" -vvv - run: forge snapshot formal-verification: runs-on: ubuntu-latest diff --git a/lib/forge-std b/lib/forge-std index fc560fa3..0e709775 160000 --- a/lib/forge-std +++ b/lib/forge-std @@ -1 +1 @@ -Subproject commit fc560fa34fa12a335a50c35d92e55a6628ca467c +Subproject commit 0e7097750918380d84dd3cfdef595bee74dabb70 From ad183887ad57c7eb71965e05b3fb71b253d34be4 Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Fri, 15 Nov 2024 13:49:06 -0500 Subject: [PATCH 06/97] non-kontrol snapshot --- .github/workflows/ci.yaml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index 658aec66..4ca56203 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -18,7 +18,8 @@ jobs: - name: Run non-Kontrol tests run: | forge test --no-match-path "src/test/kontrol/*" -vvv - - run: forge snapshot + - name: Run snapshot without Kontrol tests + run: forge snapshot --no-match-path "src/test/kontrol/*" formal-verification: runs-on: ubuntu-latest needs: test From f1f378533104b45a55a21d20ab44d27360319ff0 Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Fri, 15 Nov 2024 13:52:36 -0500 Subject: [PATCH 07/97] kontrol docker image --- .github/workflows/ci.yaml | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index 4ca56203..88fc357f 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -1,7 +1,7 @@ name: CI on: [push] jobs: - test: + foundry-test: runs-on: ubuntu-latest steps: - uses: actions/checkout@master @@ -22,16 +22,14 @@ jobs: run: forge snapshot --no-match-path "src/test/kontrol/*" formal-verification: runs-on: ubuntu-latest - needs: test + needs: foundry-test + container: + image: runtimeverification/kontrol:latest steps: - uses: actions/checkout@master with: fetch-depth: 0 submodules: recursive - - name: Install Kontrol - run: | - bash <(curl https://kframework.org/install) - kup install kontrol - name: Build and Run Proofs run: | kontrol build From f30e9cdf491b07491600937a680961be178ce383 Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Fri, 15 Nov 2024 14:35:08 -0500 Subject: [PATCH 08/97] try to install kontrol again --- .github/workflows/ci.yaml | 36 ++++++++++++++++++++++++++++-------- 1 file changed, 28 insertions(+), 8 deletions(-) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index 88fc357f..f56832e3 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -1,5 +1,6 @@ name: CI on: [push] + jobs: foundry-test: runs-on: ubuntu-latest @@ -20,20 +21,39 @@ jobs: forge test --no-match-path "src/test/kontrol/*" -vvv - name: Run snapshot without Kontrol tests run: forge snapshot --no-match-path "src/test/kontrol/*" + formal-verification: runs-on: ubuntu-latest needs: foundry-test - container: - image: runtimeverification/kontrol:latest steps: - uses: actions/checkout@master with: fetch-depth: 0 submodules: recursive - - name: Build and Run Proofs + + # Install dependencies for K Framework + - name: Install K Framework run: | - kontrol build - kontrol prove --config-profile setup - kontrol prove --config-profile tests - - name: View Results - run: kontrol list \ No newline at end of file + sudo apt update + sudo apt install -y openjdk-11-jdk maven curl + curl -LO https://github.com/runtimeverification/k/releases/download/v1.0/kframework.tar.gz + tar -xvzf kframework.tar.gz + cd kframework + export PATH=$PATH:$(pwd)/bin + + # Verify KEVM setup + - name: Install KEVM + run: | + curl -LO https://github.com/runtimeverification/evm-semantics/releases/download/v1.0/evm.tar.gz + tar -xvzf evm.tar.gz + cd evm + export PATH=$PATH:$(pwd)/bin + make deps # Install KEVM dependencies + make build # Build KEVM + + # Run the formal verification job + - name: Formal Verification with KEVM + run: | + cd evm + # Assuming `verification.k` exists and contains the formal specification + krun verification.k From a21cc95368db95e41978d5981c330c45ad114ca3 Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Fri, 15 Nov 2024 14:40:42 -0500 Subject: [PATCH 09/97] fix k framework install --- .github/workflows/ci.yaml | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index f56832e3..c35c2c63 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -34,13 +34,10 @@ jobs: # Install dependencies for K Framework - name: Install K Framework run: | - sudo apt update - sudo apt install -y openjdk-11-jdk maven curl - curl -LO https://github.com/runtimeverification/k/releases/download/v1.0/kframework.tar.gz + curl -LO https://github.com/runtimeverification/k/releases/download/v5.4.0/kframework.tar.gz tar -xvzf kframework.tar.gz cd kframework export PATH=$PATH:$(pwd)/bin - # Verify KEVM setup - name: Install KEVM run: | From edff6b081039aed43f2f11a78a9a86202549f5a8 Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Fri, 15 Nov 2024 14:52:08 -0500 Subject: [PATCH 10/97] fix k framework install --- .github/workflows/ci.yaml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index c35c2c63..bec35d0f 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -34,8 +34,8 @@ jobs: # Install dependencies for K Framework - name: Install K Framework run: | - curl -LO https://github.com/runtimeverification/k/releases/download/v5.4.0/kframework.tar.gz - tar -xvzf kframework.tar.gz + curl -LO kframework.tar.gz https://github.com/runtimeverification/k/releases/download/v7.1.170/kframework-7.1.170-src.tar.gz + tar -xvzf kframework cd kframework export PATH=$PATH:$(pwd)/bin # Verify KEVM setup From 28f6f2c6c1a92a45505f07dae6a3507380baeeaa Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Fri, 15 Nov 2024 14:57:10 -0500 Subject: [PATCH 11/97] fix k framework install --- .github/workflows/ci.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index bec35d0f..e0e42224 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -34,7 +34,7 @@ jobs: # Install dependencies for K Framework - name: Install K Framework run: | - curl -LO kframework.tar.gz https://github.com/runtimeverification/k/releases/download/v7.1.170/kframework-7.1.170-src.tar.gz + curl -L -o kframework.tar.gz https://github.com/runtimeverification/k/releases/download/v7.1.170/kframework-7.1.170-src.tar.gz tar -xvzf kframework cd kframework export PATH=$PATH:$(pwd)/bin From a2a687329858dba229713dae4c6e2e64bd905c3b Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Fri, 15 Nov 2024 15:01:46 -0500 Subject: [PATCH 12/97] fix k framework install --- .github/workflows/ci.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index e0e42224..496f2917 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -35,7 +35,7 @@ jobs: - name: Install K Framework run: | curl -L -o kframework.tar.gz https://github.com/runtimeverification/k/releases/download/v7.1.170/kframework-7.1.170-src.tar.gz - tar -xvzf kframework + tar -xvzf kframework.tar.gz cd kframework export PATH=$PATH:$(pwd)/bin # Verify KEVM setup From d7c4d2ed155df3118932515a99ee95b976a4279e Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Fri, 15 Nov 2024 15:12:46 -0500 Subject: [PATCH 13/97] fix k framework install with github token --- .github/workflows/ci.yaml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index 496f2917..5584ceb5 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -32,9 +32,11 @@ jobs: submodules: recursive # Install dependencies for K Framework - - name: Install K Framework + - name: Download K Framework + env: + GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} run: | - curl -L -o kframework.tar.gz https://github.com/runtimeverification/k/releases/download/v7.1.170/kframework-7.1.170-src.tar.gz + curl -H "Authorization: token $GITHUB_TOKEN" -L -o kframework.tar.gz https://github.com/runtimeverification/k/releases/download/v7.1.170/kframework-7.1.170-src.tar.gz tar -xvzf kframework.tar.gz cd kframework export PATH=$PATH:$(pwd)/bin From 58dcc13190e85aaf503f9f073c5d7e89d44cff6a Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Fri, 15 Nov 2024 15:14:30 -0500 Subject: [PATCH 14/97] fix k framework install with github token --- .github/workflows/ci.yaml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index 5584ceb5..8c51487a 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -34,9 +34,9 @@ jobs: # Install dependencies for K Framework - name: Download K Framework env: - GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} + REPOSITORY_TOKEN: ${{ secrets.REPOSITORY_TOKEN }} run: | - curl -H "Authorization: token $GITHUB_TOKEN" -L -o kframework.tar.gz https://github.com/runtimeverification/k/releases/download/v7.1.170/kframework-7.1.170-src.tar.gz + curl -H "Authorization: token $REPOSITORY_TOKEN" -L -o kframework.tar.gz https://github.com/runtimeverification/k/releases/download/v7.1.170/kframework-7.1.170-src.tar.gz tar -xvzf kframework.tar.gz cd kframework export PATH=$PATH:$(pwd)/bin From fdde143b564a3cabeeab7ba06f10d84a8a2cc044 Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Fri, 15 Nov 2024 15:18:01 -0500 Subject: [PATCH 15/97] fix k framework install with github token --- .github/workflows/ci.yaml | 13 +++++-------- 1 file changed, 5 insertions(+), 8 deletions(-) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index 8c51487a..ec3d3052 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -31,8 +31,7 @@ jobs: fetch-depth: 0 submodules: recursive - # Install dependencies for K Framework - - name: Download K Framework + - name: Download K Framework env: REPOSITORY_TOKEN: ${{ secrets.REPOSITORY_TOKEN }} run: | @@ -40,19 +39,17 @@ jobs: tar -xvzf kframework.tar.gz cd kframework export PATH=$PATH:$(pwd)/bin - # Verify KEVM setup + - name: Install KEVM run: | curl -LO https://github.com/runtimeverification/evm-semantics/releases/download/v1.0/evm.tar.gz tar -xvzf evm.tar.gz cd evm export PATH=$PATH:$(pwd)/bin - make deps # Install KEVM dependencies - make build # Build KEVM + make deps + make build - # Run the formal verification job - name: Formal Verification with KEVM run: | cd evm - # Assuming `verification.k` exists and contains the formal specification - krun verification.k + krun verification.k \ No newline at end of file From e15936cbff52009bc0da4a84cbdeff581a428f4d Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Fri, 15 Nov 2024 15:22:45 -0500 Subject: [PATCH 16/97] fix k framework install with github token --- .github/workflows/ci.yaml | 30 +++++++++++++++++++++++++----- 1 file changed, 25 insertions(+), 5 deletions(-) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index ec3d3052..eccf6a4d 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -31,25 +31,45 @@ jobs: fetch-depth: 0 submodules: recursive + # Download and Extract K Framework - name: Download K Framework env: REPOSITORY_TOKEN: ${{ secrets.REPOSITORY_TOKEN }} run: | + echo "Downloading K Framework..." curl -H "Authorization: token $REPOSITORY_TOKEN" -L -o kframework.tar.gz https://github.com/runtimeverification/k/releases/download/v7.1.170/kframework-7.1.170-src.tar.gz - tar -xvzf kframework.tar.gz - cd kframework - export PATH=$PATH:$(pwd)/bin + echo "Validating tarball..." + file kframework.tar.gz || { echo "Download failed"; exit 1; } + + echo "Extracting K Framework..." + mkdir -p kframework + tar -xvzf kframework.tar.gz -C kframework --strip-components=1 || { echo "Extraction failed"; exit 1; } + ls -l kframework || { echo "Extraction directory not found"; exit 1; } + + echo "Setting up K Framework..." + export PATH=$PATH:$(pwd)/kframework/bin + + # Download and Build KEVM - name: Install KEVM run: | + echo "Downloading KEVM..." curl -LO https://github.com/runtimeverification/evm-semantics/releases/download/v1.0/evm.tar.gz - tar -xvzf evm.tar.gz + + echo "Extracting KEVM..." + mkdir -p evm + tar -xvzf evm.tar.gz -C evm --strip-components=1 || { echo "Extraction failed"; exit 1; } + ls -l evm || { echo "EVM directory not found"; exit 1; } + + echo "Building KEVM..." cd evm export PATH=$PATH:$(pwd)/bin make deps make build + # Run the Formal Verification Job - name: Formal Verification with KEVM run: | + echo "Running formal verification..." cd evm - krun verification.k \ No newline at end of file + krun verification.k || { echo "Formal verification failed"; exit 1; } From 6c67f8c371527b00bb97e3dc3f232fc0425e354a Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Fri, 15 Nov 2024 15:28:20 -0500 Subject: [PATCH 17/97] fix kevm install --- .github/workflows/ci.yaml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index eccf6a4d..8f130579 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -52,9 +52,11 @@ jobs: # Download and Build KEVM - name: Install KEVM + env: + REPOSITORY_TOKEN: ${{ secrets.REPOSITORY_TOKEN }} run: | echo "Downloading KEVM..." - curl -LO https://github.com/runtimeverification/evm-semantics/releases/download/v1.0/evm.tar.gz + curl -H "Authorization: token $REPOSITORY_TOKEN" -L -o evm.tar.gz https://github.com/runtimeverification/evm-semantics/archive/refs/tags/v1.0.753.tar.gz echo "Extracting KEVM..." mkdir -p evm From 0a9a8777e5e9f66bd0eeb0d058ac775e09c3629b Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Fri, 15 Nov 2024 15:33:06 -0500 Subject: [PATCH 18/97] fix kevm install --- .github/workflows/ci.yaml | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index 8f130579..ab44e588 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -66,6 +66,15 @@ jobs: echo "Building KEVM..." cd evm export PATH=$PATH:$(pwd)/bin + + echo "Listing KEVM directory contents..." + + if [ -f Makefile ]; then + make help || make -pRrq : 2>/dev/null | grep -E '^[a-zA-Z_-]+:' + else + echo "No Makefile found in the evm directory." + exit 1 + fi make deps make build From 328925b07d62faff4ebd2599e7a6d317c21f4cbc Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Fri, 15 Nov 2024 15:36:54 -0500 Subject: [PATCH 19/97] fix kevm install --- .github/workflows/ci.yaml | 18 ++++++++---------- 1 file changed, 8 insertions(+), 10 deletions(-) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index ab44e588..20fec8d1 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -67,17 +67,15 @@ jobs: cd evm export PATH=$PATH:$(pwd)/bin - echo "Listing KEVM directory contents..." - - if [ -f Makefile ]; then - make help || make -pRrq : 2>/dev/null | grep -E '^[a-zA-Z_-]+:' - else - echo "No Makefile found in the evm directory." - exit 1 - fi - make deps - make build + echo "Checking available Makefile targets..." + cd evm + make -pRrq : 2>/dev/null | grep -E '^[a-zA-Z_-]+:' | sed 's/:$//' || echo "No targets found in Makefile" + echo "Building KEVM..." + # Run the default 'all' target or fallback to specific targets + make all || echo "Default 'all' target failed" + make kevm-pyk || echo "'kevm-pyk' target failed" + make test || echo "'test' target failed" # Run the Formal Verification Job - name: Formal Verification with KEVM run: | From e85fa22fa742af5ec32621192b65f85d5a6a9874 Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Fri, 15 Nov 2024 15:41:29 -0500 Subject: [PATCH 20/97] remove extra cd in kevm install --- .github/workflows/ci.yaml | 1 - 1 file changed, 1 deletion(-) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index 20fec8d1..d96a6d36 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -68,7 +68,6 @@ jobs: export PATH=$PATH:$(pwd)/bin echo "Checking available Makefile targets..." - cd evm make -pRrq : 2>/dev/null | grep -E '^[a-zA-Z_-]+:' | sed 's/:$//' || echo "No targets found in Makefile" echo "Building KEVM..." From 7a48bcbd8bd850ee6d8f470fb8a0d6f32ba9ac87 Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Fri, 15 Nov 2024 15:47:42 -0500 Subject: [PATCH 21/97] remove extra cd in kevm install --- .github/workflows/ci.yaml | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index d96a6d36..aa45e8d9 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -49,6 +49,11 @@ jobs: echo "Setting up K Framework..." export PATH=$PATH:$(pwd)/kframework/bin + - name: Install Poetry + run: | + curl -sSL https://install.python-poetry.org | python3 - + export PATH=$HOME/.local/bin:$PATH + poetry --version # Download and Build KEVM - name: Install KEVM From 4728713faecd631e57771856c7b562fd88670e11 Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Fri, 15 Nov 2024 15:56:11 -0500 Subject: [PATCH 22/97] remove extra cd in kevm install --- .github/workflows/ci.yaml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index aa45e8d9..e6b1826b 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -81,8 +81,12 @@ jobs: make kevm-pyk || echo "'kevm-pyk' target failed" make test || echo "'test' target failed" # Run the Formal Verification Job + - name: Verify krun Installation + run: | + echo "Checking for krun..." + find . -name krun + ls -l $(find . -name krun | head -n 1) || echo "krun not found" - name: Formal Verification with KEVM run: | echo "Running formal verification..." - cd evm krun verification.k || { echo "Formal verification failed"; exit 1; } From eabf20ebbbef2d76bad472d16ef7591cf9ed7705 Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Fri, 15 Nov 2024 16:02:32 -0500 Subject: [PATCH 23/97] krun --- .github/workflows/ci.yaml | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index e6b1826b..c2060cb1 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -86,7 +86,12 @@ jobs: echo "Checking for krun..." find . -name krun ls -l $(find . -name krun | head -n 1) || echo "krun not found" - - name: Formal Verification with KEVM + - name: Run Formal Verification with KEVM run: | echo "Running formal verification..." + KRUN_PATH=$(find . -name krun | head -n 1 | xargs dirname) + export PATH=$KRUN_PATH:$PATH + echo "Updated PATH: $PATH" + which krun || { echo "krun not found in PATH"; exit 1; } krun verification.k || { echo "Formal verification failed"; exit 1; } + From 685a2bf80022a68701b46557c79a8d5c65cc04fc Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Fri, 15 Nov 2024 16:09:46 -0500 Subject: [PATCH 24/97] krun --- .github/workflows/ci.yaml | 16 +++++++++++++++- 1 file changed, 15 insertions(+), 1 deletion(-) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index c2060cb1..a874885e 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -86,12 +86,26 @@ jobs: echo "Checking for krun..." find . -name krun ls -l $(find . -name krun | head -n 1) || echo "krun not found" + - name: Verify Directory Structure + run: | + echo "Checking for k-util.sh..." + find . -name k-util.sh || echo "k-util.sh not found" + ls -l ./kframework/k-distribution/src/main/lib/kframework || echo "Directory not found" + - name: Build Missing K Framework Components + run: | + cd kframework + make || echo "Make failed" - name: Run Formal Verification with KEVM run: | echo "Running formal verification..." KRUN_PATH=$(find . -name krun | head -n 1 | xargs dirname) + K_LIB_PATH=$(find . -name k-util.sh | head -n 1 | xargs dirname) export PATH=$KRUN_PATH:$PATH + export K_LIB_PATH echo "Updated PATH: $PATH" + echo "Library Path: $K_LIB_PATH" which krun || { echo "krun not found in PATH"; exit 1; } - krun verification.k || { echo "Formal verification failed"; exit 1; } + KRUN_SCRIPT=$(find . -name krun | head -n 1) + bash $KRUN_SCRIPT verification.k || { echo "Formal verification failed"; exit 1; } + From 41731258cf56a372bdf63e2fa10edb863afd674a Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Fri, 15 Nov 2024 16:14:56 -0500 Subject: [PATCH 25/97] krun path --- .github/workflows/ci.yaml | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index a874885e..1d70e897 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -106,6 +106,12 @@ jobs: echo "Library Path: $K_LIB_PATH" which krun || { echo "krun not found in PATH"; exit 1; } KRUN_SCRIPT=$(find . -name krun | head -n 1) + + # Override the environment variable for k-util.sh path + export K_LIB_OVERRIDE=$K_LIB_PATH + sed -i "s|../lib/kframework|$K_LIB_OVERRIDE|" $KRUN_SCRIPT + bash $KRUN_SCRIPT verification.k || { echo "Formal verification failed"; exit 1; } + From faa8016fd4a4f56c58e52a02233add8aeacdcf41 Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Fri, 15 Nov 2024 16:19:27 -0500 Subject: [PATCH 26/97] krun path --- .github/workflows/ci.yaml | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index 1d70e897..ed0145db 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -101,17 +101,16 @@ jobs: KRUN_PATH=$(find . -name krun | head -n 1 | xargs dirname) K_LIB_PATH=$(find . -name k-util.sh | head -n 1 | xargs dirname) export PATH=$KRUN_PATH:$PATH - export K_LIB_PATH echo "Updated PATH: $PATH" echo "Library Path: $K_LIB_PATH" which krun || { echo "krun not found in PATH"; exit 1; } KRUN_SCRIPT=$(find . -name krun | head -n 1) - # Override the environment variable for k-util.sh path - export K_LIB_OVERRIDE=$K_LIB_PATH - sed -i "s|../lib/kframework|$K_LIB_OVERRIDE|" $KRUN_SCRIPT + # Replace incorrect library path reference in krun script + sed -i "s|../lib/kframework|$K_LIB_PATH|" $KRUN_SCRIPT bash $KRUN_SCRIPT verification.k || { echo "Formal verification failed"; exit 1; } + From 45024ca5d1906a358b95b825e9575ca4b63276da Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Fri, 15 Nov 2024 16:24:02 -0500 Subject: [PATCH 27/97] krun path --- .github/workflows/ci.yaml | 15 +++++++++++++-- 1 file changed, 13 insertions(+), 2 deletions(-) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index ed0145db..2c957488 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -98,19 +98,30 @@ jobs: - name: Run Formal Verification with KEVM run: | echo "Running formal verification..." + + # Locate the paths for krun and k-util.sh KRUN_PATH=$(find . -name krun | head -n 1 | xargs dirname) K_LIB_PATH=$(find . -name k-util.sh | head -n 1 | xargs dirname) + export PATH=$KRUN_PATH:$PATH echo "Updated PATH: $PATH" echo "Library Path: $K_LIB_PATH" + + # Ensure krun is available which krun || { echo "krun not found in PATH"; exit 1; } + + # Update the krun script to use the absolute K_LIB_PATH KRUN_SCRIPT=$(find . -name krun | head -n 1) - - # Replace incorrect library path reference in krun script sed -i "s|../lib/kframework|$K_LIB_PATH|" $KRUN_SCRIPT + # Debug the updated krun script + echo "Updated krun script:" + head -n 10 $KRUN_SCRIPT + + # Run krun with the fixed paths bash $KRUN_SCRIPT verification.k || { echo "Formal verification failed"; exit 1; } + From 0091f59d0bc8e3985322f5a62d1bfb484f33ba6e Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Fri, 15 Nov 2024 16:30:30 -0500 Subject: [PATCH 28/97] krun path --- .github/workflows/ci.yaml | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index 2c957488..946a729e 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -101,18 +101,21 @@ jobs: # Locate the paths for krun and k-util.sh KRUN_PATH=$(find . -name krun | head -n 1 | xargs dirname) - K_LIB_PATH=$(find . -name k-util.sh | head -n 1 | xargs dirname) + K_UTIL_PATH=$(find . -name k-util.sh | head -n 1 | xargs dirname) export PATH=$KRUN_PATH:$PATH echo "Updated PATH: $PATH" - echo "Library Path: $K_LIB_PATH" + echo "k-util.sh Path: $K_UTIL_PATH" # Ensure krun is available which krun || { echo "krun not found in PATH"; exit 1; } - # Update the krun script to use the absolute K_LIB_PATH + # Locate the krun script KRUN_SCRIPT=$(find . -name krun | head -n 1) - sed -i "s|../lib/kframework|$K_LIB_PATH|" $KRUN_SCRIPT + echo "Found krun script at: $KRUN_SCRIPT" + + # Update the krun script to reference the correct k-util.sh path + sed -i "s|\.\./lib/kframework|$K_UTIL_PATH|" $KRUN_SCRIPT # Debug the updated krun script echo "Updated krun script:" From b2b7193dea870e86e52ecf36d03128ed6d089ce6 Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Fri, 15 Nov 2024 16:35:19 -0500 Subject: [PATCH 29/97] do local on github --- .github/workflows/ci.yaml | 82 +-------------------------------------- 1 file changed, 2 insertions(+), 80 deletions(-) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index 946a729e..df93036e 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -37,93 +37,15 @@ jobs: REPOSITORY_TOKEN: ${{ secrets.REPOSITORY_TOKEN }} run: | echo "Downloading K Framework..." - curl -H "Authorization: token $REPOSITORY_TOKEN" -L -o kframework.tar.gz https://github.com/runtimeverification/k/releases/download/v7.1.170/kframework-7.1.170-src.tar.gz + curl -H "Authorization: token $REPOSITORY_TOKEN" https://kframework.org/install - echo "Validating tarball..." - file kframework.tar.gz || { echo "Download failed"; exit 1; } - - echo "Extracting K Framework..." - mkdir -p kframework - tar -xvzf kframework.tar.gz -C kframework --strip-components=1 || { echo "Extraction failed"; exit 1; } - ls -l kframework || { echo "Extraction directory not found"; exit 1; } - - echo "Setting up K Framework..." - export PATH=$PATH:$(pwd)/kframework/bin + kup install kontrol - name: Install Poetry run: | curl -sSL https://install.python-poetry.org | python3 - export PATH=$HOME/.local/bin:$PATH poetry --version - # Download and Build KEVM - - name: Install KEVM - env: - REPOSITORY_TOKEN: ${{ secrets.REPOSITORY_TOKEN }} - run: | - echo "Downloading KEVM..." - curl -H "Authorization: token $REPOSITORY_TOKEN" -L -o evm.tar.gz https://github.com/runtimeverification/evm-semantics/archive/refs/tags/v1.0.753.tar.gz - - echo "Extracting KEVM..." - mkdir -p evm - tar -xvzf evm.tar.gz -C evm --strip-components=1 || { echo "Extraction failed"; exit 1; } - ls -l evm || { echo "EVM directory not found"; exit 1; } - - echo "Building KEVM..." - cd evm - export PATH=$PATH:$(pwd)/bin - - echo "Checking available Makefile targets..." - make -pRrq : 2>/dev/null | grep -E '^[a-zA-Z_-]+:' | sed 's/:$//' || echo "No targets found in Makefile" - - echo "Building KEVM..." - # Run the default 'all' target or fallback to specific targets - make all || echo "Default 'all' target failed" - make kevm-pyk || echo "'kevm-pyk' target failed" - make test || echo "'test' target failed" - # Run the Formal Verification Job - - name: Verify krun Installation - run: | - echo "Checking for krun..." - find . -name krun - ls -l $(find . -name krun | head -n 1) || echo "krun not found" - - name: Verify Directory Structure - run: | - echo "Checking for k-util.sh..." - find . -name k-util.sh || echo "k-util.sh not found" - ls -l ./kframework/k-distribution/src/main/lib/kframework || echo "Directory not found" - - name: Build Missing K Framework Components - run: | - cd kframework - make || echo "Make failed" - - name: Run Formal Verification with KEVM - run: | - echo "Running formal verification..." - - # Locate the paths for krun and k-util.sh - KRUN_PATH=$(find . -name krun | head -n 1 | xargs dirname) - K_UTIL_PATH=$(find . -name k-util.sh | head -n 1 | xargs dirname) - - export PATH=$KRUN_PATH:$PATH - echo "Updated PATH: $PATH" - echo "k-util.sh Path: $K_UTIL_PATH" - - # Ensure krun is available - which krun || { echo "krun not found in PATH"; exit 1; } - - # Locate the krun script - KRUN_SCRIPT=$(find . -name krun | head -n 1) - echo "Found krun script at: $KRUN_SCRIPT" - - # Update the krun script to reference the correct k-util.sh path - sed -i "s|\.\./lib/kframework|$K_UTIL_PATH|" $KRUN_SCRIPT - - # Debug the updated krun script - echo "Updated krun script:" - head -n 10 $KRUN_SCRIPT - - # Run krun with the fixed paths - bash $KRUN_SCRIPT verification.k || { echo "Formal verification failed"; exit 1; } - From 89ea4f791588064c92c998275050ad844bdcc606 Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Fri, 15 Nov 2024 16:41:18 -0500 Subject: [PATCH 30/97] do local on github --- .github/workflows/ci.yaml | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index df93036e..89ad923f 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -38,8 +38,12 @@ jobs: run: | echo "Downloading K Framework..." curl -H "Authorization: token $REPOSITORY_TOKEN" https://kframework.org/install + echo "Checking for kup..." + find /nix -name kup || echo "kup not found" + nix profile list --experimental-features 'nix-command flakes' || echo "No kup profile installed" kup install kontrol + - name: Install Poetry run: | curl -sSL https://install.python-poetry.org | python3 - From 9b1e4011a0db70c9b9ecaec2b34d15de9a7bba72 Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Fri, 15 Nov 2024 16:44:57 -0500 Subject: [PATCH 31/97] do local on github --- .github/workflows/ci.yaml | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index 89ad923f..b0797f32 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -32,6 +32,27 @@ jobs: submodules: recursive # Download and Extract K Framework + - name: Check Nix Installation + run: | + if ! command -v nix &> /dev/null; then + echo "Installing nix..." + curl -L https://install.determinate.systems/nix | sh -s -- install --no-confirm \ + --extra-conf "trusted-public-keys = cache.nixos.org-1:k-framework.cachix.org-1:k-framework-binary.cachix.org-1" \ + --extra-conf "substituters = https://cache.nixos.org https://k-framework.cachix.org" + . /nix/var/nix/profiles/default/etc/profile.d/nix-daemon.sh + fi + nix --version || { echo "Nix installation failed"; exit 1; } + - name: Install kup + run: | + echo "Installing kup..." + nix profile install github:runtimeverification/kup#kup \ + --option extra-substituters 'https://k-framework.cachix.org' \ + --option extra-trusted-public-keys 'k-framework.cachix.org-1:jeyMXB2h28gpNRjuVkehg+zLj62ma1RnyyopA/20yFE=' \ + --experimental-features 'nix-command flakes' + + # Add kup to PATH + export PATH="/nix/var/nix/profiles/per-user/$USER/profile/bin:$PATH" + which kup || { echo "kup not found in PATH after installation"; exit 1; } - name: Download K Framework env: REPOSITORY_TOKEN: ${{ secrets.REPOSITORY_TOKEN }} From 5d400078279d69439bc4c7385887d1ea6772cc66 Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Fri, 15 Nov 2024 16:48:54 -0500 Subject: [PATCH 32/97] do local on github --- .github/workflows/ci.yaml | 11 ----------- 1 file changed, 11 deletions(-) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index b0797f32..f38effd1 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -42,17 +42,6 @@ jobs: . /nix/var/nix/profiles/default/etc/profile.d/nix-daemon.sh fi nix --version || { echo "Nix installation failed"; exit 1; } - - name: Install kup - run: | - echo "Installing kup..." - nix profile install github:runtimeverification/kup#kup \ - --option extra-substituters 'https://k-framework.cachix.org' \ - --option extra-trusted-public-keys 'k-framework.cachix.org-1:jeyMXB2h28gpNRjuVkehg+zLj62ma1RnyyopA/20yFE=' \ - --experimental-features 'nix-command flakes' - - # Add kup to PATH - export PATH="/nix/var/nix/profiles/per-user/$USER/profile/bin:$PATH" - which kup || { echo "kup not found in PATH after installation"; exit 1; } - name: Download K Framework env: REPOSITORY_TOKEN: ${{ secrets.REPOSITORY_TOKEN }} From e2641d82c01dc1ba08430cf7edfb09bff8af81ff Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Fri, 15 Nov 2024 16:54:05 -0500 Subject: [PATCH 33/97] do local on github --- .github/workflows/ci.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index f38effd1..da1c1680 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -47,7 +47,7 @@ jobs: REPOSITORY_TOKEN: ${{ secrets.REPOSITORY_TOKEN }} run: | echo "Downloading K Framework..." - curl -H "Authorization: token $REPOSITORY_TOKEN" https://kframework.org/install + bash <(curl -H "Authorization: token $REPOSITORY_TOKEN" https://kframework.org/install) echo "Checking for kup..." find /nix -name kup || echo "kup not found" nix profile list --experimental-features 'nix-command flakes' || echo "No kup profile installed" From 38df6c81390e9ab682cb5d1a83100f232cf53c43 Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Fri, 15 Nov 2024 17:03:13 -0500 Subject: [PATCH 34/97] do local on github --- .github/workflows/ci.yaml | 93 ++++++++++++++++++++++++++++++++------- 1 file changed, 78 insertions(+), 15 deletions(-) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index da1c1680..435fa7b2 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -32,34 +32,97 @@ jobs: submodules: recursive # Download and Extract K Framework - - name: Check Nix Installation - run: | - if ! command -v nix &> /dev/null; then - echo "Installing nix..." - curl -L https://install.determinate.systems/nix | sh -s -- install --no-confirm \ - --extra-conf "trusted-public-keys = cache.nixos.org-1:k-framework.cachix.org-1:k-framework-binary.cachix.org-1" \ - --extra-conf "substituters = https://cache.nixos.org https://k-framework.cachix.org" - . /nix/var/nix/profiles/default/etc/profile.d/nix-daemon.sh - fi - nix --version || { echo "Nix installation failed"; exit 1; } - name: Download K Framework env: REPOSITORY_TOKEN: ${{ secrets.REPOSITORY_TOKEN }} run: | echo "Downloading K Framework..." - bash <(curl -H "Authorization: token $REPOSITORY_TOKEN" https://kframework.org/install) - echo "Checking for kup..." - find /nix -name kup || echo "kup not found" - nix profile list --experimental-features 'nix-command flakes' || echo "No kup profile installed" + curl -H "Authorization: token $REPOSITORY_TOKEN" -L -o kframework.tar.gz https://github.com/runtimeverification/k/releases/download/v7.1.170/kframework-7.1.170-src.tar.gz + + echo "Validating tarball..." + file kframework.tar.gz || { echo "Download failed"; exit 1; } - kup install kontrol + echo "Extracting K Framework..." + mkdir -p kframework + tar -xvzf kframework.tar.gz -C kframework --strip-components=1 || { echo "Extraction failed"; exit 1; } + ls -l kframework || { echo "Extraction directory not found"; exit 1; } + echo "Setting up K Framework..." + export PATH=$PATH:$(pwd)/kframework/bin - name: Install Poetry run: | curl -sSL https://install.python-poetry.org | python3 - export PATH=$HOME/.local/bin:$PATH poetry --version + # Download and Build KEVM + - name: Install KEVM + env: + REPOSITORY_TOKEN: ${{ secrets.REPOSITORY_TOKEN }} + run: | + echo "Downloading KEVM..." + curl -H "Authorization: token $REPOSITORY_TOKEN" -L -o evm.tar.gz https://github.com/runtimeverification/evm-semantics/archive/refs/tags/v1.0.753.tar.gz + + echo "Extracting KEVM..." + mkdir -p evm + tar -xvzf evm.tar.gz -C evm --strip-components=1 || { echo "Extraction failed"; exit 1; } + ls -l evm || { echo "EVM directory not found"; exit 1; } + + echo "Building KEVM..." + cd evm + export PATH=$PATH:$(pwd)/bin + + echo "Checking available Makefile targets..." + make -pRrq : 2>/dev/null | grep -E '^[a-zA-Z_-]+:' | sed 's/:$//' || echo "No targets found in Makefile" + + echo "Building KEVM..." + # Run the default 'all' target or fallback to specific targets + make all || echo "Default 'all' target failed" + make kevm-pyk || echo "'kevm-pyk' target failed" + make test || echo "'test' target failed" + # Run the Formal Verification Job + - name: Verify krun Installation + run: | + echo "Checking for krun..." + find . -name krun + ls -l $(find . -name krun | head -n 1) || echo "krun not found" + - name: Verify Directory Structure + run: | + echo "Checking for k-util.sh..." + find . -name k-util.sh || echo "k-util.sh not found" + ls -l ./kframework/k-distribution/src/main/lib/kframework || echo "Directory not found" + - name: Build Missing K Framework Components + run: | + cd kframework + make || echo "Make failed" + - name: Run Formal Verification with KEVM + run: | + echo "Running formal verification..." + + # Locate the paths for krun and k-util.sh + KRUN_PATH=$(find . -name krun | head -n 1 | xargs dirname) + K_UTIL_PATH=$(find . -name k-util.sh | head -n 1 | xargs dirname) + + export PATH=$KRUN_PATH:$PATH + echo "Updated PATH: $PATH" + echo "k-util.sh Path: $K_UTIL_PATH" + + # Ensure krun is available + which krun || { echo "krun not found in PATH"; exit 1; } + + # Locate the krun script + KRUN_SCRIPT=$(find . -name krun | head -n 1) + echo "Found krun script at: $KRUN_SCRIPT" + + # Update the krun script to reference the correct k-util.sh path + sed -i "s|\.\./lib/kframework|$K_UTIL_PATH|" $KRUN_SCRIPT + + # Debug the updated krun script + echo "Updated krun script:" + head -n 10 $KRUN_SCRIPT + + # Run krun with the fixed paths + bash $KRUN_SCRIPT verification.k || { echo "Formal verification failed"; exit 1; } From eb1c5573bf17d30e52ebe1523deeba902f545aab Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Fri, 15 Nov 2024 17:09:09 -0500 Subject: [PATCH 35/97] formal verification on files --- .github/workflows/ci.yaml | 45 +++++++++++++++++++-------------------- 1 file changed, 22 insertions(+), 23 deletions(-) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index 435fa7b2..608a9115 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -97,32 +97,31 @@ jobs: make || echo "Make failed" - name: Run Formal Verification with KEVM run: | - echo "Running formal verification..." + # Set up environment + export K_BIN=$(find . -name krun | head -n 1 | xargs dirname) + export PATH=$K_BIN:$PATH - # Locate the paths for krun and k-util.sh - KRUN_PATH=$(find . -name krun | head -n 1 | xargs dirname) - K_UTIL_PATH=$(find . -name k-util.sh | head -n 1 | xargs dirname) + # Print environment for debugging + echo "K Framework version:" + krun --version - export PATH=$KRUN_PATH:$PATH - echo "Updated PATH: $PATH" - echo "k-util.sh Path: $K_UTIL_PATH" + # Run verifications for each spec file + for spec in src/test/kontrol/*.k; do + echo "Verifying $spec..." + krun --directory src/test/kontrol \ + --debug \ + --output-file "verification-results/$(basename $spec .k).out" \ + "$spec" + done - # Ensure krun is available - which krun || { echo "krun not found in PATH"; exit 1; } - - # Locate the krun script - KRUN_SCRIPT=$(find . -name krun | head -n 1) - echo "Found krun script at: $KRUN_SCRIPT" - - # Update the krun script to reference the correct k-util.sh path - sed -i "s|\.\./lib/kframework|$K_UTIL_PATH|" $KRUN_SCRIPT - - # Debug the updated krun script - echo "Updated krun script:" - head -n 10 $KRUN_SCRIPT - - # Run krun with the fixed paths - bash $KRUN_SCRIPT verification.k || { echo "Formal verification failed"; exit 1; } + # Check results + if [ -d verification-results ]; then + echo "Verification Results:" + cat verification-results/*.out + else + echo "No verification results found" + exit 1 + fi From 714be6ed7ebd960f7594f7287d1cec6a18709049 Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Fri, 15 Nov 2024 17:14:03 -0500 Subject: [PATCH 36/97] formal verification on files --- .github/workflows/ci.yaml | 54 +++++++++++++++++++++++++++------------ 1 file changed, 37 insertions(+), 17 deletions(-) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index 608a9115..d4d7e42b 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -95,34 +95,54 @@ jobs: run: | cd kframework make || echo "Make failed" - - name: Run Formal Verification with KEVM + - name: Setup K Framework Environment run: | - # Set up environment - export K_BIN=$(find . -name krun | head -n 1 | xargs dirname) - export PATH=$K_BIN:$PATH + # Find the k-util.sh file + K_UTIL=$(find . -name k-util.sh | head -n 1) + K_UTIL_DIR=$(dirname "$K_UTIL") + + # Find krun + KRUN=$(find . -name krun | head -n 1) + KRUN_DIR=$(dirname "$KRUN") + + # Export necessary environment variables + export K_LIB="$K_UTIL_DIR" + export PATH="$KRUN_DIR:$PATH" - # Print environment for debugging - echo "K Framework version:" - krun --version + # Create symbolic links if needed + mkdir -p "$KRUN_DIR/../lib/kframework" + ln -sf "$K_UTIL" "$KRUN_DIR/../lib/kframework/k-util.sh" + + # Verify setup + echo "K Framework paths:" + echo "K_LIB=$K_LIB" + echo "PATH=$PATH" + ls -l "$KRUN_DIR/../lib/kframework/" + + - name: Run Formal Verification with KEVM + run: | + # Create results directory + mkdir -p verification-results # Run verifications for each spec file for spec in src/test/kontrol/*.k; do - echo "Verifying $spec..." - krun --directory src/test/kontrol \ - --debug \ - --output-file "verification-results/$(basename $spec .k).out" \ - "$spec" + if [ -f "$spec" ]; then + echo "Verifying $spec..." + K_OPTS="--directory $(dirname $spec) --debug" \ + "$KRUN" \ + --output "verification-results/$(basename $spec .k).out" \ + "$spec" + else + echo "No .k files found in src/test/kontrol/" + exit 1 + fi done # Check results - if [ -d verification-results ]; then + if [ -d verification-results ] && [ "$(ls -A verification-results)" ]; then echo "Verification Results:" cat verification-results/*.out else echo "No verification results found" exit 1 fi - - - - From 752c965ab174ccb109e3447170827576eb9483be Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Fri, 15 Nov 2024 17:21:59 -0500 Subject: [PATCH 37/97] formal verification on files --- .github/workflows/ci.yaml | 57 ++++++++++++++++++++++++++++++--------- 1 file changed, 44 insertions(+), 13 deletions(-) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index d4d7e42b..f1449191 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -121,28 +121,59 @@ jobs: - name: Run Formal Verification with KEVM run: | + # Set up environment + echo "Setting up K Framework environment..." + export K_BIN=$(find . -name krun | head -n 1 | xargs dirname) + export K_LIB=$(find . -name k-util.sh | head -n 1 | xargs dirname) + export PATH=$K_BIN:$PATH + + # Debug environment + echo "K_BIN: $K_BIN" + echo "K_LIB: $K_LIB" + echo "PATH: $PATH" + + # Ensure required binaries are found + if [[ -z "$K_BIN" || -z "$K_LIB" ]]; then + echo "Error: K_BIN or K_LIB is empty. Ensure K Framework is installed correctly." + exit 1 + fi + + KRUN_SCRIPT=$(find . -name krun | head -n 1) + if [[ -z "$KRUN_SCRIPT" ]]; then + echo "Error: KRUN_SCRIPT is empty. Cannot find krun." + exit 1 + fi + echo "KRUN_SCRIPT: $KRUN_SCRIPT" + + # Patch the krun script to fix k-util.sh path + sed -i "s|\.\./lib/kframework|$K_LIB|" $KRUN_SCRIPT + + # Verify patching + echo "Patched krun script:" + head -n 10 $KRUN_SCRIPT + + # Verify K Framework installation + echo "K Framework version:" + krun --version || { echo "Failed to run krun"; exit 1; } + # Create results directory mkdir -p verification-results - + # Run verifications for each spec file for spec in src/test/kontrol/*.k; do - if [ -f "$spec" ]; then - echo "Verifying $spec..." - K_OPTS="--directory $(dirname $spec) --debug" \ - "$KRUN" \ - --output "verification-results/$(basename $spec .k).out" \ - "$spec" - else - echo "No .k files found in src/test/kontrol/" - exit 1 - fi + echo "Verifying $spec..." + krun --directory src/test/kontrol \ + --debug \ + --output-file "verification-results/$(basename $spec .k).out" \ + "$spec" || { echo "Verification failed for $spec"; exit 1; } done - + # Check results - if [ -d verification-results ] && [ "$(ls -A verification-results)" ]; then + if [ -d verification-results ]; then echo "Verification Results:" cat verification-results/*.out else echo "No verification results found" exit 1 fi + From 50fe48d3e8435182c1f9d52fa91b4e66bf270273 Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Fri, 15 Nov 2024 17:27:10 -0500 Subject: [PATCH 38/97] formal verification on files --- .github/workflows/ci.yaml | 222 +++++++++++++++++--------------------- 1 file changed, 100 insertions(+), 122 deletions(-) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index f1449191..5be61ad1 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -1,4 +1,5 @@ name: CI + on: [push] jobs: @@ -31,149 +32,126 @@ jobs: fetch-depth: 0 submodules: recursive - # Download and Extract K Framework - - name: Download K Framework + - name: Setup Environment Variables + run: | + echo "K_ROOT=$GITHUB_WORKSPACE/kframework" >> $GITHUB_ENV + echo "KEVM_ROOT=$GITHUB_WORKSPACE/evm" >> $GITHUB_ENV + echo "PATH=$GITHUB_WORKSPACE/kframework/k-distribution/target/release/k/bin:$GITHUB_WORKSPACE/evm/bin:$PATH" >> $GITHUB_ENV + + - name: Download and Extract K Framework env: REPOSITORY_TOKEN: ${{ secrets.REPOSITORY_TOKEN }} run: | - echo "Downloading K Framework..." - curl -H "Authorization: token $REPOSITORY_TOKEN" -L -o kframework.tar.gz https://github.com/runtimeverification/k/releases/download/v7.1.170/kframework-7.1.170-src.tar.gz - - echo "Validating tarball..." - file kframework.tar.gz || { echo "Download failed"; exit 1; } - - echo "Extracting K Framework..." - mkdir -p kframework - tar -xvzf kframework.tar.gz -C kframework --strip-components=1 || { echo "Extraction failed"; exit 1; } - ls -l kframework || { echo "Extraction directory not found"; exit 1; } + curl -H "Authorization: token $REPOSITORY_TOKEN" \ + -L -o kframework.tar.gz \ + https://github.com/runtimeverification/k/releases/download/v7.1.170/kframework-7.1.170-src.tar.gz + + mkdir -p "$K_ROOT" + tar -xzf kframework.tar.gz -C "$K_ROOT" --strip-components=1 + + echo "K Framework contents:" + ls -la "$K_ROOT" - echo "Setting up K Framework..." - export PATH=$PATH:$(pwd)/kframework/bin - name: Install Poetry - run: | - curl -sSL https://install.python-poetry.org | python3 - - export PATH=$HOME/.local/bin:$PATH - poetry --version + uses: snok/install-poetry@v1 + with: + version: 1.4.0 + virtualenvs-create: true + virtualenvs-in-project: true - # Download and Build KEVM - name: Install KEVM env: - REPOSITORY_TOKEN: ${{ secrets.REPOSITORY_TOKEN }} + REPOSITORY_TOKEN: ${{ secrets.REPOSITORY_TOKEN }} run: | - echo "Downloading KEVM..." - curl -H "Authorization: token $REPOSITORY_TOKEN" -L -o evm.tar.gz https://github.com/runtimeverification/evm-semantics/archive/refs/tags/v1.0.753.tar.gz + curl -H "Authorization: token $REPOSITORY_TOKEN" \ + -L -o evm.tar.gz \ + https://github.com/runtimeverification/evm-semantics/archive/refs/tags/v1.0.753.tar.gz - echo "Extracting KEVM..." - mkdir -p evm - tar -xvzf evm.tar.gz -C evm --strip-components=1 || { echo "Extraction failed"; exit 1; } - ls -l evm || { echo "EVM directory not found"; exit 1; } + mkdir -p "$KEVM_ROOT" + tar -xzf evm.tar.gz -C "$KEVM_ROOT" --strip-components=1 - echo "Building KEVM..." - cd evm - export PATH=$PATH:$(pwd)/bin + cd "$KEVM_ROOT" + make deps + make build + make test - echo "Checking available Makefile targets..." - make -pRrq : 2>/dev/null | grep -E '^[a-zA-Z_-]+:' | sed 's/:$//' || echo "No targets found in Makefile" - - echo "Building KEVM..." - # Run the default 'all' target or fallback to specific targets - make all || echo "Default 'all' target failed" - make kevm-pyk || echo "'kevm-pyk' target failed" - make test || echo "'test' target failed" - # Run the Formal Verification Job - - name: Verify krun Installation - run: | - echo "Checking for krun..." - find . -name krun - ls -l $(find . -name krun | head -n 1) || echo "krun not found" - - name: Verify Directory Structure - run: | - echo "Checking for k-util.sh..." - find . -name k-util.sh || echo "k-util.sh not found" - ls -l ./kframework/k-distribution/src/main/lib/kframework || echo "Directory not found" - - name: Build Missing K Framework Components + - name: Setup K Framework run: | - cd kframework - make || echo "Make failed" - - name: Setup K Framework Environment - run: | - # Find the k-util.sh file - K_UTIL=$(find . -name k-util.sh | head -n 1) - K_UTIL_DIR=$(dirname "$K_UTIL") - - # Find krun - KRUN=$(find . -name krun | head -n 1) - KRUN_DIR=$(dirname "$KRUN") - - # Export necessary environment variables - export K_LIB="$K_UTIL_DIR" - export PATH="$KRUN_DIR:$PATH" - - # Create symbolic links if needed - mkdir -p "$KRUN_DIR/../lib/kframework" - ln -sf "$K_UTIL" "$KRUN_DIR/../lib/kframework/k-util.sh" - - # Verify setup - echo "K Framework paths:" - echo "K_LIB=$K_LIB" - echo "PATH=$PATH" - ls -l "$KRUN_DIR/../lib/kframework/" + cd "$K_ROOT" + + # Build K Framework + mvn package -DskipTests + + # Setup paths + K_BIN="$K_ROOT/k-distribution/target/release/k/bin" + K_LIB="$K_ROOT/k-distribution/target/release/k/lib/kframework" + + # Verify directory structure + echo "K Framework directory structure:" + ls -R "$K_BIN" + ls -R "$K_LIB" + + # Export paths + echo "K_BIN=$K_BIN" >> $GITHUB_ENV + echo "K_LIB=$K_LIB" >> $GITHUB_ENV + echo "PATH=$K_BIN:$PATH" >> $GITHUB_ENV - - name: Run Formal Verification with KEVM + - name: Configure KRUN run: | - # Set up environment - echo "Setting up K Framework environment..." - export K_BIN=$(find . -name krun | head -n 1 | xargs dirname) - export K_LIB=$(find . -name k-util.sh | head -n 1 | xargs dirname) - export PATH=$K_BIN:$PATH - - # Debug environment - echo "K_BIN: $K_BIN" - echo "K_LIB: $K_LIB" - echo "PATH: $PATH" - - # Ensure required binaries are found - if [[ -z "$K_BIN" || -z "$K_LIB" ]]; then - echo "Error: K_BIN or K_LIB is empty. Ensure K Framework is installed correctly." - exit 1 - fi - - KRUN_SCRIPT=$(find . -name krun | head -n 1) - if [[ -z "$KRUN_SCRIPT" ]]; then - echo "Error: KRUN_SCRIPT is empty. Cannot find krun." + KRUN_SCRIPT="$K_BIN/krun" + + if [ ! -f "$KRUN_SCRIPT" ]; then + echo "Error: krun script not found at $KRUN_SCRIPT" exit 1 fi - echo "KRUN_SCRIPT: $KRUN_SCRIPT" - - # Patch the krun script to fix k-util.sh path - sed -i "s|\.\./lib/kframework|$K_LIB|" $KRUN_SCRIPT - - # Verify patching - echo "Patched krun script:" - head -n 10 $KRUN_SCRIPT - - # Verify K Framework installation - echo "K Framework version:" - krun --version || { echo "Failed to run krun"; exit 1; } + + # Backup original script + cp "$KRUN_SCRIPT" "${KRUN_SCRIPT}.backup" + + # Update paths in krun script + sed -i "s|source \"\$dir/\.\./lib/kframework/k-util\.sh\"|source \"$K_LIB/k-util.sh\"|g" "$KRUN_SCRIPT" + + echo "Modified krun script:" + head -n 10 "$KRUN_SCRIPT" + + # Test krun + "$KRUN_SCRIPT" --version - # Create results directory + - name: Run Formal Verification + run: | mkdir -p verification-results - - # Run verifications for each spec file + + # Initialize counter for verified specs + verified_count=0 + for spec in src/test/kontrol/*.k; do - echo "Verifying $spec..." - krun --directory src/test/kontrol \ - --debug \ - --output-file "verification-results/$(basename $spec .k).out" \ - "$spec" || { echo "Verification failed for $spec"; exit 1; } + if [ -f "$spec" ]; then + echo "Verifying $spec..." + + if "$K_BIN/krun" \ + --directory src/test/kontrol \ + --debug \ + --output-file "verification-results/$(basename "$spec" .k).out" \ + "$spec"; then + echo "✓ Verification successful for $spec" + ((verified_count++)) + else + echo "✗ Verification failed for $spec" + exit 1 + fi + fi done - - # Check results - if [ -d verification-results ]; then - echo "Verification Results:" - cat verification-results/*.out - else - echo "No verification results found" + + if [ $verified_count -eq 0 ]; then + echo "No specification files found to verify" exit 1 + else + echo "Successfully verified $verified_count specification(s)" fi + - name: Upload Verification Results + uses: actions/upload-artifact@v2 + with: + name: verification-results + path: verification-results/ + if-no-files-found: error \ No newline at end of file From 2065f1e10256a69264cbc4068faaf3deb4f976d8 Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Fri, 15 Nov 2024 17:31:01 -0500 Subject: [PATCH 39/97] formal verification on files --- .github/workflows/ci.yaml | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index 5be61ad1..87364f1b 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -27,7 +27,7 @@ jobs: runs-on: ubuntu-latest needs: foundry-test steps: - - uses: actions/checkout@master + - uses: actions/checkout@v4 with: fetch-depth: 0 submodules: recursive @@ -150,8 +150,9 @@ jobs: fi - name: Upload Verification Results - uses: actions/upload-artifact@v2 + uses: actions/upload-artifact@v3 with: name: verification-results path: verification-results/ - if-no-files-found: error \ No newline at end of file + if-no-files-found: error + retention-days: 30 \ No newline at end of file From 58c6c337665f3fcda397a33f9d11794489446da0 Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Fri, 15 Nov 2024 17:39:12 -0500 Subject: [PATCH 40/97] formal verification on files with krun path set --- .github/workflows/ci.yaml | 125 ++++++++++++++++++++++---------------- 1 file changed, 74 insertions(+), 51 deletions(-) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index 87364f1b..34d909a5 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -6,7 +6,7 @@ jobs: foundry-test: runs-on: ubuntu-latest steps: - - uses: actions/checkout@master + - uses: actions/checkout@v4 with: fetch-depth: 0 submodules: recursive @@ -32,72 +32,91 @@ jobs: fetch-depth: 0 submodules: recursive - - name: Setup Environment Variables - run: | - echo "K_ROOT=$GITHUB_WORKSPACE/kframework" >> $GITHUB_ENV - echo "KEVM_ROOT=$GITHUB_WORKSPACE/evm" >> $GITHUB_ENV - echo "PATH=$GITHUB_WORKSPACE/kframework/k-distribution/target/release/k/bin:$GITHUB_WORKSPACE/evm/bin:$PATH" >> $GITHUB_ENV - - - name: Download and Extract K Framework + # Download and Extract K Framework + - name: Download K Framework env: REPOSITORY_TOKEN: ${{ secrets.REPOSITORY_TOKEN }} run: | - curl -H "Authorization: token $REPOSITORY_TOKEN" \ - -L -o kframework.tar.gz \ - https://github.com/runtimeverification/k/releases/download/v7.1.170/kframework-7.1.170-src.tar.gz - - mkdir -p "$K_ROOT" - tar -xzf kframework.tar.gz -C "$K_ROOT" --strip-components=1 - - echo "K Framework contents:" - ls -la "$K_ROOT" + echo "Downloading K Framework..." + curl -H "Authorization: token $REPOSITORY_TOKEN" -L -o kframework.tar.gz \ + https://github.com/runtimeverification/k/releases/download/v7.1.170/kframework-7.1.170-src.tar.gz + + echo "Validating tarball..." + file kframework.tar.gz || { echo "Download failed"; exit 1; } + + echo "Extracting K Framework..." + mkdir -p kframework + tar -xzf kframework.tar.gz -C kframework --strip-components=1 || { echo "Extraction failed"; exit 1; } + ls -l kframework || { echo "Extraction directory not found"; exit 1; } - name: Install Poetry uses: snok/install-poetry@v1 with: version: 1.4.0 virtualenvs-create: true - virtualenvs-in-project: true + # Download and Build KEVM - name: Install KEVM env: REPOSITORY_TOKEN: ${{ secrets.REPOSITORY_TOKEN }} run: | - curl -H "Authorization: token $REPOSITORY_TOKEN" \ - -L -o evm.tar.gz \ - https://github.com/runtimeverification/evm-semantics/archive/refs/tags/v1.0.753.tar.gz + echo "Downloading KEVM..." + curl -H "Authorization: token $REPOSITORY_TOKEN" -L -o evm.tar.gz \ + https://github.com/runtimeverification/evm-semantics/archive/refs/tags/v1.0.753.tar.gz - mkdir -p "$KEVM_ROOT" - tar -xzf evm.tar.gz -C "$KEVM_ROOT" --strip-components=1 + mkdir -p evm + tar -xzf evm.tar.gz -C evm --strip-components=1 || { echo "Extraction failed"; exit 1; } - cd "$KEVM_ROOT" - make deps - make build - make test + cd evm + make deps || true + make build || true + make test || true - - name: Setup K Framework + - name: Setup K Framework Environment run: | - cd "$K_ROOT" + # Set absolute paths + WORKSPACE="$GITHUB_WORKSPACE" + K_ROOT="$WORKSPACE/kframework" + + # Create necessary directories + mkdir -p "$K_ROOT/k-distribution/lib/kframework" - # Build K Framework - mvn package -DskipTests + # Find and copy k-util.sh + K_UTIL=$(find "$K_ROOT" -name k-util.sh | head -n 1) + if [ -z "$K_UTIL" ]; then + echo "Error: k-util.sh not found" + exit 1 + fi - # Setup paths - K_BIN="$K_ROOT/k-distribution/target/release/k/bin" - K_LIB="$K_ROOT/k-distribution/target/release/k/lib/kframework" + # Copy k-util.sh to the expected location + cp "$K_UTIL" "$K_ROOT/k-distribution/lib/kframework/" + + # Find krun + KRUN=$(find "$K_ROOT" -name krun | head -n 1) + if [ -z "$KRUN" ]; then + echo "Error: krun not found" + exit 1 + fi - # Verify directory structure - echo "K Framework directory structure:" - ls -R "$K_BIN" - ls -R "$K_LIB" + KRUN_DIR=$(dirname "$KRUN") # Export paths - echo "K_BIN=$K_BIN" >> $GITHUB_ENV - echo "K_LIB=$K_LIB" >> $GITHUB_ENV - echo "PATH=$K_BIN:$PATH" >> $GITHUB_ENV + echo "K_BIN=$KRUN_DIR" >> $GITHUB_ENV + echo "K_LIB=$K_ROOT/k-distribution/lib/kframework" >> $GITHUB_ENV + echo "PATH=$KRUN_DIR:$PATH" >> $GITHUB_ENV + + # Verify setup + echo "K Framework paths:" + echo "K_BIN=$KRUN_DIR" + echo "K_LIB=$K_ROOT/k-distribution/lib/kframework" + ls -l "$K_ROOT/k-distribution/lib/kframework" - name: Configure KRUN run: | + # Get paths from environment + K_BIN="$K_BIN" + K_LIB="$K_LIB" + KRUN_SCRIPT="$K_BIN/krun" if [ ! -f "$KRUN_SCRIPT" ]; then @@ -105,20 +124,24 @@ jobs: exit 1 fi - # Backup original script + # Create backup cp "$KRUN_SCRIPT" "${KRUN_SCRIPT}.backup" - # Update paths in krun script - sed -i "s|source \"\$dir/\.\./lib/kframework/k-util\.sh\"|source \"$K_LIB/k-util.sh\"|g" "$KRUN_SCRIPT" + # Update source path in krun script + sed -i "s|source.*k-util\.sh|source \"$K_LIB/k-util.sh\"|g" "$KRUN_SCRIPT" echo "Modified krun script:" head -n 10 "$KRUN_SCRIPT" - # Test krun - "$KRUN_SCRIPT" --version + # Test k-util.sh exists + if [ ! -f "$K_LIB/k-util.sh" ]; then + echo "Error: k-util.sh not found at $K_LIB/k-util.sh" + exit 1 + fi - - name: Run Formal Verification + - name: Run Formal Verification with KEVM run: | + # Create results directory mkdir -p verification-results # Initialize counter for verified specs @@ -129,10 +152,10 @@ jobs: echo "Verifying $spec..." if "$K_BIN/krun" \ - --directory src/test/kontrol \ - --debug \ - --output-file "verification-results/$(basename "$spec" .k).out" \ - "$spec"; then + --directory src/test/kontrol \ + --debug \ + --output-file "verification-results/$(basename "$spec" .k).out" \ + "$spec"; then echo "✓ Verification successful for $spec" ((verified_count++)) else From fbe46539e62d38549e3730d54cd2651b0540f1f8 Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Fri, 15 Nov 2024 17:43:29 -0500 Subject: [PATCH 41/97] kontrol env --- .github/workflows/ci.yaml | 42 +++++++++++++++++++++++++++------------ 1 file changed, 29 insertions(+), 13 deletions(-) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index 34d909a5..9d5ef52b 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -77,39 +77,55 @@ jobs: # Set absolute paths WORKSPACE="$GITHUB_WORKSPACE" K_ROOT="$WORKSPACE/kframework" + K_LIB_DIR="$K_ROOT/k-distribution/lib/kframework" - # Create necessary directories - mkdir -p "$K_ROOT/k-distribution/lib/kframework" + # Create directory if it doesn't exist (with -p to avoid errors if it exists) + mkdir -p "$K_LIB_DIR" - # Find and copy k-util.sh + # Find k-util.sh K_UTIL=$(find "$K_ROOT" -name k-util.sh | head -n 1) if [ -z "$K_UTIL" ]; then echo "Error: k-util.sh not found" + find "$K_ROOT" -type f -name "*k-util*" # Debug: look for similar files exit 1 fi - # Copy k-util.sh to the expected location - cp "$K_UTIL" "$K_ROOT/k-distribution/lib/kframework/" + echo "Found k-util.sh at: $K_UTIL" + + # Copy k-util.sh to the expected location (use -f to force overwrite if exists) + cp -f "$K_UTIL" "$K_LIB_DIR/" # Find krun KRUN=$(find "$K_ROOT" -name krun | head -n 1) if [ -z "$KRUN" ]; then echo "Error: krun not found" + find "$K_ROOT" -type f -name "*krun*" # Debug: look for similar files exit 1 fi + echo "Found krun at: $KRUN" KRUN_DIR=$(dirname "$KRUN") # Export paths - echo "K_BIN=$KRUN_DIR" >> $GITHUB_ENV - echo "K_LIB=$K_ROOT/k-distribution/lib/kframework" >> $GITHUB_ENV - echo "PATH=$KRUN_DIR:$PATH" >> $GITHUB_ENV - - # Verify setup - echo "K Framework paths:" + { + echo "K_BIN=$KRUN_DIR" + echo "K_LIB=$K_LIB_DIR" + echo "PATH=$KRUN_DIR:$PATH" + } >> $GITHUB_ENV + + # Debug: Show directory structure + echo "K Framework directory structure:" + echo "K_ROOT=$K_ROOT" echo "K_BIN=$KRUN_DIR" - echo "K_LIB=$K_ROOT/k-distribution/lib/kframework" - ls -l "$K_ROOT/k-distribution/lib/kframework" + echo "K_LIB=$K_LIB_DIR" + ls -la "$K_ROOT/k-distribution/lib" || echo "lib directory not accessible" + ls -la "$K_LIB_DIR" || echo "kframework directory not accessible" + + # Verify k-util.sh was copied correctly + if [ ! -f "$K_LIB_DIR/k-util.sh" ]; then + echo "Error: Failed to copy k-util.sh to $K_LIB_DIR" + exit 1 + fi - name: Configure KRUN run: | From 06dbc0ab5a3bf892cc89a539244021810d10f7c9 Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Fri, 15 Nov 2024 17:48:34 -0500 Subject: [PATCH 42/97] kontrol env --- .github/workflows/ci.yaml | 48 ++++++++++++++++++++++++--------------- 1 file changed, 30 insertions(+), 18 deletions(-) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index 9d5ef52b..9344bcd5 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -77,53 +77,65 @@ jobs: # Set absolute paths WORKSPACE="$GITHUB_WORKSPACE" K_ROOT="$WORKSPACE/kframework" - K_LIB_DIR="$K_ROOT/k-distribution/lib/kframework" - # Create directory if it doesn't exist (with -p to avoid errors if it exists) - mkdir -p "$K_LIB_DIR" + echo "Current directory structure before setup:" + ls -R "$K_ROOT" - # Find k-util.sh + # Try to locate existing directories + echo "Searching for existing k-util.sh..." + find "$K_ROOT" -name k-util.sh + + echo "Searching for existing krun..." + find "$K_ROOT" -name krun + + # Check directory structure + echo "Checking directory structure..." + ls -la "$K_ROOT/k-distribution" || echo "k-distribution not found" + ls -la "$K_ROOT/k-distribution/lib" || echo "lib directory not found" + + # Find k-util.sh first K_UTIL=$(find "$K_ROOT" -name k-util.sh | head -n 1) if [ -z "$K_UTIL" ]; then echo "Error: k-util.sh not found" - find "$K_ROOT" -type f -name "*k-util*" # Debug: look for similar files exit 1 fi echo "Found k-util.sh at: $K_UTIL" - # Copy k-util.sh to the expected location (use -f to force overwrite if exists) - cp -f "$K_UTIL" "$K_LIB_DIR/" + # Get the directory where k-util.sh currently resides + K_UTIL_DIR=$(dirname "$K_UTIL") + echo "k-util.sh directory: $K_UTIL_DIR" # Find krun KRUN=$(find "$K_ROOT" -name krun | head -n 1) if [ -z "$KRUN" ]; then echo "Error: krun not found" - find "$K_ROOT" -type f -name "*krun*" # Debug: look for similar files exit 1 fi echo "Found krun at: $KRUN" KRUN_DIR=$(dirname "$KRUN") + echo "krun directory: $KRUN_DIR" + + # Use the existing directory structure instead of creating new ones + K_LIB="$K_UTIL_DIR" # Export paths { echo "K_BIN=$KRUN_DIR" - echo "K_LIB=$K_LIB_DIR" + echo "K_LIB=$K_LIB" echo "PATH=$KRUN_DIR:$PATH" } >> $GITHUB_ENV - # Debug: Show directory structure - echo "K Framework directory structure:" - echo "K_ROOT=$K_ROOT" + # Debug: Show final paths + echo "Final K Framework paths:" echo "K_BIN=$KRUN_DIR" - echo "K_LIB=$K_LIB_DIR" - ls -la "$K_ROOT/k-distribution/lib" || echo "lib directory not accessible" - ls -la "$K_LIB_DIR" || echo "kframework directory not accessible" + echo "K_LIB=$K_LIB" + echo "PATH=$KRUN_DIR:$PATH" - # Verify k-util.sh was copied correctly - if [ ! -f "$K_LIB_DIR/k-util.sh" ]; then - echo "Error: Failed to copy k-util.sh to $K_LIB_DIR" + # Verify k-util.sh is accessible + if [ ! -f "$K_LIB/k-util.sh" ]; then + echo "Error: Cannot access k-util.sh at $K_LIB/k-util.sh" exit 1 fi From e34bac89aa156b0ad000c3c0105a970cc6aa1d8c Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Fri, 15 Nov 2024 17:54:14 -0500 Subject: [PATCH 43/97] debug krun problems --- .github/workflows/ci.yaml | 135 ++++++++++++++------------------------ 1 file changed, 50 insertions(+), 85 deletions(-) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index 9344bcd5..438f591d 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -78,132 +78,97 @@ jobs: WORKSPACE="$GITHUB_WORKSPACE" K_ROOT="$WORKSPACE/kframework" - echo "Current directory structure before setup:" - ls -R "$K_ROOT" - - # Try to locate existing directories - echo "Searching for existing k-util.sh..." - find "$K_ROOT" -name k-util.sh - - echo "Searching for existing krun..." - find "$K_ROOT" -name krun - - # Check directory structure - echo "Checking directory structure..." - ls -la "$K_ROOT/k-distribution" || echo "k-distribution not found" - ls -la "$K_ROOT/k-distribution/lib" || echo "lib directory not found" - - # Find k-util.sh first + # Find core files K_UTIL=$(find "$K_ROOT" -name k-util.sh | head -n 1) - if [ -z "$K_UTIL" ]; then - echo "Error: k-util.sh not found" - exit 1 - fi - - echo "Found k-util.sh at: $K_UTIL" - - # Get the directory where k-util.sh currently resides - K_UTIL_DIR=$(dirname "$K_UTIL") - echo "k-util.sh directory: $K_UTIL_DIR" - - # Find krun KRUN=$(find "$K_ROOT" -name krun | head -n 1) - if [ -z "$KRUN" ]; then - echo "Error: krun not found" + + if [ -z "$K_UTIL" ] || [ -z "$KRUN" ]; then + echo "Error: Required files not found" + echo "K_UTIL: $K_UTIL" + echo "KRUN: $KRUN" exit 1 fi - echo "Found krun at: $KRUN" + # Set directories + K_UTIL_DIR=$(dirname "$K_UTIL") KRUN_DIR=$(dirname "$KRUN") - echo "krun directory: $KRUN_DIR" - - # Use the existing directory structure instead of creating new ones - K_LIB="$K_UTIL_DIR" # Export paths { echo "K_BIN=$KRUN_DIR" - echo "K_LIB=$K_LIB" + echo "K_LIB=$K_UTIL_DIR" echo "PATH=$KRUN_DIR:$PATH" } >> $GITHUB_ENV - # Debug: Show final paths - echo "Final K Framework paths:" + echo "Path setup complete" echo "K_BIN=$KRUN_DIR" - echo "K_LIB=$K_LIB" - echo "PATH=$KRUN_DIR:$PATH" - - # Verify k-util.sh is accessible - if [ ! -f "$K_LIB/k-util.sh" ]; then - echo "Error: Cannot access k-util.sh at $K_LIB/k-util.sh" - exit 1 - fi + echo "K_LIB=$K_UTIL_DIR" - - name: Configure KRUN + - name: Debug KRUN Script run: | - # Get paths from environment - K_BIN="$K_BIN" - K_LIB="$K_LIB" - KRUN_SCRIPT="$K_BIN/krun" - if [ ! -f "$KRUN_SCRIPT" ]; then - echo "Error: krun script not found at $KRUN_SCRIPT" - exit 1 - fi + echo "Original KRUN script content:" + cat "$KRUN_SCRIPT" # Create backup cp "$KRUN_SCRIPT" "${KRUN_SCRIPT}.backup" - # Update source path in krun script - sed -i "s|source.*k-util\.sh|source \"$K_LIB/k-util.sh\"|g" "$KRUN_SCRIPT" + # Clean up any DOS line endings + dos2unix "$KRUN_SCRIPT" - echo "Modified krun script:" - head -n 10 "$KRUN_SCRIPT" + # Fix common script issues + sed -i 's/\r//g' "$KRUN_SCRIPT" # Remove any remaining CR characters + sed -i 's/\t/ /g' "$KRUN_SCRIPT" # Replace tabs with spaces - # Test k-util.sh exists - if [ ! -f "$K_LIB/k-util.sh" ]; then - echo "Error: k-util.sh not found at $K_LIB/k-util.sh" - exit 1 - fi + echo "Modified KRUN script:" + cat "$KRUN_SCRIPT" + + echo "Testing KRUN script syntax:" + bash -n "$KRUN_SCRIPT" || echo "Syntax check failed" - name: Run Formal Verification with KEVM run: | - # Create results directory mkdir -p verification-results - # Initialize counter for verified specs - verified_count=0 + # Debug variables + echo "Current environment:" + env | grep -E 'K_|PATH' + + # Test krun directly + echo "Testing krun directly:" + "$K_BIN/krun" --version || echo "krun version check failed" + # Process each spec file with extra debugging for spec in src/test/kontrol/*.k; do if [ -f "$spec" ]; then - echo "Verifying $spec..." + echo "Processing spec file: $spec" + echo "File contents:" + head -n 10 "$spec" + + echo "Running verification with full command:" + CMD="$K_BIN/krun --directory src/test/kontrol --debug --output-file verification-results/$(basename "$spec" .k).out $spec" + echo "$CMD" - if "$K_BIN/krun" \ - --directory src/test/kontrol \ - --debug \ - --output-file "verification-results/$(basename "$spec" .k).out" \ - "$spec"; then + if eval "$CMD"; then echo "✓ Verification successful for $spec" - ((verified_count++)) else echo "✗ Verification failed for $spec" + echo "Error output:" + cat "verification-results/$(basename "$spec" .k).out" 2>/dev/null || echo "No output file generated" + echo "Full environment:" + env exit 1 fi fi done - - if [ $verified_count -eq 0 ]; then - echo "No specification files found to verify" - exit 1 - else - echo "Successfully verified $verified_count specification(s)" - fi - name: Upload Verification Results + if: always() uses: actions/upload-artifact@v3 with: - name: verification-results - path: verification-results/ - if-no-files-found: error - retention-days: 30 \ No newline at end of file + name: verification-debug + path: | + verification-results/ + ${{ env.K_BIN }}/krun* + retention-days: 5 \ No newline at end of file From e52b4ab9326b6efb3666fd9ae4034d19f660e39b Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Fri, 15 Nov 2024 17:56:13 -0500 Subject: [PATCH 44/97] use control instead of k --- .github/workflows/ci.yaml | 150 ++++++++------------------------------ 1 file changed, 30 insertions(+), 120 deletions(-) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index 438f591d..e608f0a8 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -23,7 +23,7 @@ jobs: - name: Run snapshot without Kontrol tests run: forge snapshot --no-match-path "src/test/kontrol/*" - formal-verification: + kontrol-verification: runs-on: ubuntu-latest needs: foundry-test steps: @@ -32,143 +32,53 @@ jobs: fetch-depth: 0 submodules: recursive - # Download and Extract K Framework - - name: Download K Framework - env: - REPOSITORY_TOKEN: ${{ secrets.REPOSITORY_TOKEN }} - run: | - echo "Downloading K Framework..." - curl -H "Authorization: token $REPOSITORY_TOKEN" -L -o kframework.tar.gz \ - https://github.com/runtimeverification/k/releases/download/v7.1.170/kframework-7.1.170-src.tar.gz - - echo "Validating tarball..." - file kframework.tar.gz || { echo "Download failed"; exit 1; } - - echo "Extracting K Framework..." - mkdir -p kframework - tar -xzf kframework.tar.gz -C kframework --strip-components=1 || { echo "Extraction failed"; exit 1; } - ls -l kframework || { echo "Extraction directory not found"; exit 1; } - - - name: Install Poetry - uses: snok/install-poetry@v1 + - name: Setup Python + uses: actions/setup-python@v4 with: - version: 1.4.0 - virtualenvs-create: true + python-version: '3.10' + cache: 'pip' - # Download and Build KEVM - - name: Install KEVM - env: - REPOSITORY_TOKEN: ${{ secrets.REPOSITORY_TOKEN }} + - name: Install Kontrol run: | - echo "Downloading KEVM..." - curl -H "Authorization: token $REPOSITORY_TOKEN" -L -o evm.tar.gz \ - https://github.com/runtimeverification/evm-semantics/archive/refs/tags/v1.0.753.tar.gz - - mkdir -p evm - tar -xzf evm.tar.gz -C evm --strip-components=1 || { echo "Extraction failed"; exit 1; } - - cd evm - make deps || true - make build || true - make test || true + python3 -m pip install --upgrade pip + pip install kontrol - - name: Setup K Framework Environment - run: | - # Set absolute paths - WORKSPACE="$GITHUB_WORKSPACE" - K_ROOT="$WORKSPACE/kframework" - - # Find core files - K_UTIL=$(find "$K_ROOT" -name k-util.sh | head -n 1) - KRUN=$(find "$K_ROOT" -name krun | head -n 1) - - if [ -z "$K_UTIL" ] || [ -z "$KRUN" ]; then - echo "Error: Required files not found" - echo "K_UTIL: $K_UTIL" - echo "KRUN: $KRUN" - exit 1 - fi - - # Set directories - K_UTIL_DIR=$(dirname "$K_UTIL") - KRUN_DIR=$(dirname "$KRUN") - - # Export paths - { - echo "K_BIN=$KRUN_DIR" - echo "K_LIB=$K_UTIL_DIR" - echo "PATH=$KRUN_DIR:$PATH" - } >> $GITHUB_ENV - - echo "Path setup complete" - echo "K_BIN=$KRUN_DIR" - echo "K_LIB=$K_UTIL_DIR" + - name: Install Foundry + uses: foundry-rs/foundry-toolchain@v1 + with: + version: nightly - - name: Debug KRUN Script + - name: Build Contracts run: | - KRUN_SCRIPT="$K_BIN/krun" - - echo "Original KRUN script content:" - cat "$KRUN_SCRIPT" - - # Create backup - cp "$KRUN_SCRIPT" "${KRUN_SCRIPT}.backup" - - # Clean up any DOS line endings - dos2unix "$KRUN_SCRIPT" - - # Fix common script issues - sed -i 's/\r//g' "$KRUN_SCRIPT" # Remove any remaining CR characters - sed -i 's/\t/ /g' "$KRUN_SCRIPT" # Replace tabs with spaces - - echo "Modified KRUN script:" - cat "$KRUN_SCRIPT" - - echo "Testing KRUN script syntax:" - bash -n "$KRUN_SCRIPT" || echo "Syntax check failed" + forge build --build-info --force + ls -la out/ - - name: Run Formal Verification with KEVM + - name: Run Kontrol Verification run: | + # Create results directory mkdir -p verification-results - # Debug variables - echo "Current environment:" - env | grep -E 'K_|PATH' - - # Test krun directly - echo "Testing krun directly:" - "$K_BIN/krun" --version || echo "krun version check failed" - - # Process each spec file with extra debugging + # Run verification for each specification for spec in src/test/kontrol/*.k; do if [ -f "$spec" ]; then - echo "Processing spec file: $spec" - echo "File contents:" - head -n 10 "$spec" - - echo "Running verification with full command:" - CMD="$K_BIN/krun --directory src/test/kontrol --debug --output-file verification-results/$(basename "$spec" .k).out $spec" - echo "$CMD" + echo "Verifying $(basename "$spec")..." - if eval "$CMD"; then - echo "✓ Verification successful for $spec" - else - echo "✗ Verification failed for $spec" - echo "Error output:" - cat "verification-results/$(basename "$spec" .k).out" 2>/dev/null || echo "No output file generated" - echo "Full environment:" - env - exit 1 - fi + kontrol prove "$spec" \ + --contract-dir ./src/contracts \ + --output-dir ./verification-results \ + --verbose || { + echo "Verification failed for $spec" + exit 1 + } fi done + + echo "Verification completed successfully!" - name: Upload Verification Results if: always() uses: actions/upload-artifact@v3 with: - name: verification-debug - path: | - verification-results/ - ${{ env.K_BIN }}/krun* + name: kontrol-verification-results + path: verification-results/ retention-days: 5 \ No newline at end of file From b4642145e2749f597f582a44c3ef1b22aeae5c72 Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Fri, 15 Nov 2024 18:01:13 -0500 Subject: [PATCH 45/97] install kontrol using k and then run fv on kontrol --- .github/workflows/ci.yaml | 67 ++++++++++++++++++++++++++++----------- 1 file changed, 48 insertions(+), 19 deletions(-) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index e608f0a8..78be082c 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -23,7 +23,7 @@ jobs: - name: Run snapshot without Kontrol tests run: forge snapshot --no-match-path "src/test/kontrol/*" - kontrol-verification: + formal-verification: runs-on: ubuntu-latest needs: foundry-test steps: @@ -32,16 +32,31 @@ jobs: fetch-depth: 0 submodules: recursive - - name: Setup Python - uses: actions/setup-python@v4 - with: - python-version: '3.10' - cache: 'pip' - - - name: Install Kontrol + - name: Install K Framework and Kontrol run: | - python3 -m pip install --upgrade pip - pip install kontrol + # Install dependencies + sudo apt-get update + sudo apt-get install -y curl gcc git g++ cmake maven openjdk-11-jdk flex z3 libz3-dev libsecp256k1-dev + + # Install K Framework via kup + echo "Installing K Framework..." + curl -sSL https://kframework.org/install | bash + export PATH=$PATH:$HOME/.kup/bin + + # Verify kup installation + echo "Verifying kup installation..." + which kup || { echo "kup not found"; exit 1; } + + # Install Kontrol using kup + echo "Installing Kontrol..." + kup install kontrol + + # Add Kontrol to PATH + echo "$HOME/.kup/bin" >> $GITHUB_PATH + + # Verify Kontrol installation + echo "Verifying Kontrol installation..." + kontrol --version || { echo "Kontrol installation failed"; exit 1; } - name: Install Foundry uses: foundry-rs/foundry-toolchain@v1 @@ -53,27 +68,41 @@ jobs: forge build --build-info --force ls -la out/ - - name: Run Kontrol Verification + - name: Run Formal Verification with Kontrol run: | # Create results directory mkdir -p verification-results + # Initialize counter for verified specs + verified_count=0 + # Run verification for each specification for spec in src/test/kontrol/*.k; do if [ -f "$spec" ]; then echo "Verifying $(basename "$spec")..." - kontrol prove "$spec" \ - --contract-dir ./src/contracts \ - --output-dir ./verification-results \ - --verbose || { - echo "Verification failed for $spec" - exit 1 - } + # Run Kontrol verification + if kontrol prove "$spec" \ + --contract-dir ./src/contracts \ + --output-dir ./verification-results \ + --verbose; then + echo "✓ Verification successful for $spec" + ((verified_count++)) + else + echo "✗ Verification failed for $spec" + cat "./verification-results/$(basename "$spec" .k).out" 2>/dev/null || echo "No output file found" + exit 1 + fi fi done - echo "Verification completed successfully!" + # Check if any specs were verified + if [ $verified_count -eq 0 ]; then + echo "No specification files found to verify" + exit 1 + else + echo "Successfully verified $verified_count specification(s)" + fi - name: Upload Verification Results if: always() From 2ecdfe12950ba687226b3a71f187accd18ac4367 Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Fri, 15 Nov 2024 18:06:04 -0500 Subject: [PATCH 46/97] install kontrol using k and then run fv on kontrol --- .github/workflows/ci.yaml | 49 ++++++++++++++++++++++----------------- 1 file changed, 28 insertions(+), 21 deletions(-) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index 78be082c..5e05ae86 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -32,29 +32,42 @@ jobs: fetch-depth: 0 submodules: recursive - - name: Install K Framework and Kontrol + # Download and Extract K Framework + - name: Download K Framework + env: + REPOSITORY_TOKEN: ${{ secrets.REPOSITORY_TOKEN }} + run: | + echo "Downloading K Framework..." + curl -H "Authorization: token $REPOSITORY_TOKEN" -L -o kframework.tar.gz \ + https://github.com/runtimeverification/k/releases/download/v7.1.170/kframework-7.1.170-src.tar.gz + + echo "Extracting K Framework..." + mkdir -p kframework + tar -xzf kframework.tar.gz -C kframework --strip-components=1 + + echo "Adding K to PATH..." + echo "$PWD/kframework/k-distribution/target/release/k/bin" >> $GITHUB_PATH + + - name: Install Dependencies run: | - # Install dependencies sudo apt-get update sudo apt-get install -y curl gcc git g++ cmake maven openjdk-11-jdk flex z3 libz3-dev libsecp256k1-dev - # Install K Framework via kup - echo "Installing K Framework..." - curl -sSL https://kframework.org/install | bash - export PATH=$PATH:$HOME/.kup/bin + - name: Install Kontrol with KUP + env: + REPOSITORY_TOKEN: ${{ secrets.REPOSITORY_TOKEN }} + run: | + # Set up kup with authentication + echo "Installing kup..." + curl -H "Authorization: token $REPOSITORY_TOKEN" -sSL https://kframework.org/install | bash - # Verify kup installation - echo "Verifying kup installation..." - which kup || { echo "kup not found"; exit 1; } + echo "Adding kup to PATH..." + export PATH=$PATH:$HOME/.kup/bin + echo "$HOME/.kup/bin" >> $GITHUB_PATH - # Install Kontrol using kup echo "Installing Kontrol..." - kup install kontrol + GITHUB_TOKEN=$REPOSITORY_TOKEN kup install kontrol - # Add Kontrol to PATH - echo "$HOME/.kup/bin" >> $GITHUB_PATH - - # Verify Kontrol installation echo "Verifying Kontrol installation..." kontrol --version || { echo "Kontrol installation failed"; exit 1; } @@ -70,18 +83,13 @@ jobs: - name: Run Formal Verification with Kontrol run: | - # Create results directory mkdir -p verification-results - - # Initialize counter for verified specs verified_count=0 - # Run verification for each specification for spec in src/test/kontrol/*.k; do if [ -f "$spec" ]; then echo "Verifying $(basename "$spec")..." - # Run Kontrol verification if kontrol prove "$spec" \ --contract-dir ./src/contracts \ --output-dir ./verification-results \ @@ -96,7 +104,6 @@ jobs: fi done - # Check if any specs were verified if [ $verified_count -eq 0 ]; then echo "No specification files found to verify" exit 1 From f99eb732e5208f4f9eb3a49b9236d1b1f0d4f7c0 Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Fri, 15 Nov 2024 18:10:44 -0500 Subject: [PATCH 47/97] install kontrol using k and then run fv on kontrol --- .github/workflows/ci.yaml | 56 +++++++++++++-------------------------- 1 file changed, 18 insertions(+), 38 deletions(-) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index 5e05ae86..531a3bd4 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -31,55 +31,43 @@ jobs: with: fetch-depth: 0 submodules: recursive - - # Download and Extract K Framework - - name: Download K Framework - env: - REPOSITORY_TOKEN: ${{ secrets.REPOSITORY_TOKEN }} - run: | - echo "Downloading K Framework..." - curl -H "Authorization: token $REPOSITORY_TOKEN" -L -o kframework.tar.gz \ - https://github.com/runtimeverification/k/releases/download/v7.1.170/kframework-7.1.170-src.tar.gz - - echo "Extracting K Framework..." - mkdir -p kframework - tar -xzf kframework.tar.gz -C kframework --strip-components=1 - - echo "Adding K to PATH..." - echo "$PWD/kframework/k-distribution/target/release/k/bin" >> $GITHUB_PATH - - name: Install Dependencies run: | sudo apt-get update sudo apt-get install -y curl gcc git g++ cmake maven openjdk-11-jdk flex z3 libz3-dev libsecp256k1-dev - - name: Install Kontrol with KUP + - name: Install KUp and Kontrol env: REPOSITORY_TOKEN: ${{ secrets.REPOSITORY_TOKEN }} run: | - # Set up kup with authentication + # Install kup without authentication echo "Installing kup..." - curl -H "Authorization: token $REPOSITORY_TOKEN" -sSL https://kframework.org/install | bash + curl -sSL https://kframework.org/install | bash + # Add kup to PATH echo "Adding kup to PATH..." export PATH=$PATH:$HOME/.kup/bin echo "$HOME/.kup/bin" >> $GITHUB_PATH + # Configure git for kup + git config --global url."https://${REPOSITORY_TOKEN}:x-oauth-basic@github.com/".insteadOf "https://github.com/" + + # Install Kontrol with auth echo "Installing Kontrol..." - GITHUB_TOKEN=$REPOSITORY_TOKEN kup install kontrol + export GITHUB_TOKEN=$REPOSITORY_TOKEN + kup install kontrol + # Verify installation echo "Verifying Kontrol installation..." + which kontrol || { echo "kontrol not found in PATH"; exit 1; } kontrol --version || { echo "Kontrol installation failed"; exit 1; } - - name: Install Foundry - uses: foundry-rs/foundry-toolchain@v1 - with: - version: nightly - - - name: Build Contracts + - name: Configure Git Authentication + env: + REPOSITORY_TOKEN: ${{ secrets.REPOSITORY_TOKEN }} run: | - forge build --build-info --force - ls -la out/ + echo "machine github.com login ${REPOSITORY_TOKEN}" > ~/.netrc + chmod 600 ~/.netrc - name: Run Formal Verification with Kontrol run: | @@ -109,12 +97,4 @@ jobs: exit 1 else echo "Successfully verified $verified_count specification(s)" - fi - - - name: Upload Verification Results - if: always() - uses: actions/upload-artifact@v3 - with: - name: kontrol-verification-results - path: verification-results/ - retention-days: 5 \ No newline at end of file + fi \ No newline at end of file From efaa2aa8af405f83aab256fa35d84d4ff2f02091 Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Fri, 15 Nov 2024 18:16:09 -0500 Subject: [PATCH 48/97] debug kup install --- .github/workflows/ci.yaml | 71 +++++++++++++++++++++++++++------------ 1 file changed, 50 insertions(+), 21 deletions(-) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index 531a3bd4..1dbf08e4 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -36,38 +36,67 @@ jobs: sudo apt-get update sudo apt-get install -y curl gcc git g++ cmake maven openjdk-11-jdk flex z3 libz3-dev libsecp256k1-dev - - name: Install KUp and Kontrol - env: - REPOSITORY_TOKEN: ${{ secrets.REPOSITORY_TOKEN }} + - name: Debug and Install KUP run: | - # Install kup without authentication + # Debug: Show environment + echo "Current directory: $(pwd)" + echo "Home directory: $HOME" + echo "Python version: $(python3 --version)" + + # Install kup with debug output echo "Installing kup..." - curl -sSL https://kframework.org/install | bash + curl -sSL https://kframework.org/install -o install.sh + + # Debug: Show install script + echo "Install script content:" + cat install.sh + + # Run installation with debug output + bash -x install.sh - # Add kup to PATH - echo "Adding kup to PATH..." - export PATH=$PATH:$HOME/.kup/bin + # Debug: Check kup installation + echo "Checking kup installation..." + ls -la $HOME/.kup || echo ".kup directory not found" + ls -la $HOME/.kup/bin || echo ".kup/bin directory not found" + + # Add to PATH + export PATH="$HOME/.kup/bin:$PATH" echo "$HOME/.kup/bin" >> $GITHUB_PATH - # Configure git for kup + # Verify kup installation + echo "Verifying kup command..." + which kup || echo "kup not found in PATH" + kup --version || echo "kup version check failed" + + - name: Install Kontrol via KUP + env: + REPOSITORY_TOKEN: ${{ secrets.REPOSITORY_TOKEN }} + run: | + # Configure git authentication git config --global url."https://${REPOSITORY_TOKEN}:x-oauth-basic@github.com/".insteadOf "https://github.com/" - # Install Kontrol with auth - echo "Installing Kontrol..." + # Set up netrc for authentication + echo "machine github.com login ${REPOSITORY_TOKEN}" > $HOME/.netrc + chmod 600 $HOME/.netrc + + # Debug: Show git config + echo "Git config:" + git config --global --list | grep -v "url" + + # Install Kontrol with debug output + echo "Installing Kontrol via kup..." export GITHUB_TOKEN=$REPOSITORY_TOKEN - kup install kontrol + kup install kontrol --verbose || { + echo "kup install kontrol failed" + echo "kup debug output:" + kup --debug install kontrol + exit 1 + } - # Verify installation + # Verify Kontrol installation echo "Verifying Kontrol installation..." which kontrol || { echo "kontrol not found in PATH"; exit 1; } - kontrol --version || { echo "Kontrol installation failed"; exit 1; } - - - name: Configure Git Authentication - env: - REPOSITORY_TOKEN: ${{ secrets.REPOSITORY_TOKEN }} - run: | - echo "machine github.com login ${REPOSITORY_TOKEN}" > ~/.netrc - chmod 600 ~/.netrc + kontrol --version || { echo "Kontrol failed to run"; exit 1; } - name: Run Formal Verification with Kontrol run: | From c0e25d493db7c20915a11f03d654fcae2fdad895 Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Fri, 15 Nov 2024 18:20:08 -0500 Subject: [PATCH 49/97] debug kup install with prereq nix --- .github/workflows/ci.yaml | 95 +++++++++++++++++---------------------- 1 file changed, 40 insertions(+), 55 deletions(-) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index 1dbf08e4..f3b67895 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -31,72 +31,49 @@ jobs: with: fetch-depth: 0 submodules: recursive - - name: Install Dependencies + + - name: Install System Dependencies run: | sudo apt-get update - sudo apt-get install -y curl gcc git g++ cmake maven openjdk-11-jdk flex z3 libz3-dev libsecp256k1-dev + sudo apt-get install -y curl gcc git g++ cmake maven openjdk-11-jdk flex \ + z3 libz3-dev libsecp256k1-dev python3 python3-pip build-essential - - name: Debug and Install KUP - run: | - # Debug: Show environment - echo "Current directory: $(pwd)" - echo "Home directory: $HOME" - echo "Python version: $(python3 --version)" - - # Install kup with debug output - echo "Installing kup..." - curl -sSL https://kframework.org/install -o install.sh - - # Debug: Show install script - echo "Install script content:" - cat install.sh - - # Run installation with debug output - bash -x install.sh - - # Debug: Check kup installation - echo "Checking kup installation..." - ls -la $HOME/.kup || echo ".kup directory not found" - ls -la $HOME/.kup/bin || echo ".kup/bin directory not found" - - # Add to PATH - export PATH="$HOME/.kup/bin:$PATH" - echo "$HOME/.kup/bin" >> $GITHUB_PATH - - # Verify kup installation - echo "Verifying kup command..." - which kup || echo "kup not found in PATH" - kup --version || echo "kup version check failed" + # Install Nix + - uses: DeterminateSystems/nix-installer-action@main + with: + extra-conf: | + trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= k-framework.cachix.org-1:jeyMXB2h28gpNRjuVkehg+zLj62ma1RnyyopA/20yFE= k-framework-binary.cachix.org-1:pJedQ8iG19BW3v/DMMmiRVtwRBGO3fyMv2Ws0OpBADs= + substituters = https://cache.nixos.org https://k-framework.cachix.org + + # Install Cachix + - uses: cachix/cachix-action@v12 + with: + name: k-framework + extraPullNames: k-framework-binary - - name: Install Kontrol via KUP + - name: Install KUP and Kontrol env: REPOSITORY_TOKEN: ${{ secrets.REPOSITORY_TOKEN }} run: | - # Configure git authentication + # Configure git for private repository access git config --global url."https://${REPOSITORY_TOKEN}:x-oauth-basic@github.com/".insteadOf "https://github.com/" - # Set up netrc for authentication - echo "machine github.com login ${REPOSITORY_TOKEN}" > $HOME/.netrc - chmod 600 $HOME/.netrc + echo "Installing kup..." + GC_DONT_GC=1 nix profile install github:runtimeverification/kup#kup \ + --option extra-substituters 'https://k-framework.cachix.org' \ + --option extra-trusted-public-keys 'k-framework.cachix.org-1:jeyMXB2h28gpNRjuVkehg+zLj62ma1RnyyopA/20yFE=' \ + --experimental-features 'nix-command flakes' - # Debug: Show git config - echo "Git config:" - git config --global --list | grep -v "url" + # Add kup to PATH + export PATH=$PATH:$HOME/.nix-profile/bin + echo "$HOME/.nix-profile/bin" >> $GITHUB_PATH - # Install Kontrol with debug output - echo "Installing Kontrol via kup..." - export GITHUB_TOKEN=$REPOSITORY_TOKEN - kup install kontrol --verbose || { - echo "kup install kontrol failed" - echo "kup debug output:" - kup --debug install kontrol - exit 1 - } + echo "Installing Kontrol..." + GITHUB_TOKEN=$REPOSITORY_TOKEN kup install kontrol - # Verify Kontrol installation - echo "Verifying Kontrol installation..." - which kontrol || { echo "kontrol not found in PATH"; exit 1; } - kontrol --version || { echo "Kontrol failed to run"; exit 1; } + echo "Verifying installations..." + kup --version + kontrol --version - name: Run Formal Verification with Kontrol run: | @@ -126,4 +103,12 @@ jobs: exit 1 else echo "Successfully verified $verified_count specification(s)" - fi \ No newline at end of file + fi + + - name: Upload Verification Results + if: always() + uses: actions/upload-artifact@v3 + with: + name: kontrol-verification-results + path: verification-results/ + retention-days: 5 \ No newline at end of file From f9cf0796276b0dee8ad7d3ebb662dd83ca8a33e2 Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Fri, 15 Nov 2024 18:29:34 -0500 Subject: [PATCH 50/97] debug kup install with prereq nix --- .github/workflows/ci.yaml | 1 - 1 file changed, 1 deletion(-) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index f3b67895..828bb679 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -72,7 +72,6 @@ jobs: GITHUB_TOKEN=$REPOSITORY_TOKEN kup install kontrol echo "Verifying installations..." - kup --version kontrol --version - name: Run Formal Verification with Kontrol From 3ed123092261b276ac92e969a6740cc9a38698e1 Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Fri, 15 Nov 2024 20:24:24 -0500 Subject: [PATCH 51/97] debug kup install with prereq nix --- .github/workflows/ci.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index 828bb679..2bc849ae 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -72,7 +72,7 @@ jobs: GITHUB_TOKEN=$REPOSITORY_TOKEN kup install kontrol echo "Verifying installations..." - kontrol --version + kontrol version - name: Run Formal Verification with Kontrol run: | From 1392f3b9ad8380d5c21e106147f60127cda94c90 Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Fri, 15 Nov 2024 20:38:18 -0500 Subject: [PATCH 52/97] kontrol build --- .github/workflows/ci.yaml | 97 +++++++++++++++++++++++++++++---------- 1 file changed, 72 insertions(+), 25 deletions(-) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index 2bc849ae..12a30295 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -68,40 +68,84 @@ jobs: export PATH=$PATH:$HOME/.nix-profile/bin echo "$HOME/.nix-profile/bin" >> $GITHUB_PATH + echo "Verifying kup installation..." + which kup || { echo "kup not found in PATH"; exit 1; } + kup list || { echo "kup not working properly"; exit 1; } + echo "Installing Kontrol..." GITHUB_TOKEN=$REPOSITORY_TOKEN kup install kontrol - echo "Verifying installations..." - kontrol version + echo "Verifying Kontrol installation..." + which kontrol || { echo "kontrol not found in PATH"; exit 1; } + echo "Kontrol version:" + kontrol version || { echo "kontrol not working properly"; exit 1; } + + - name: Check Kontrol Configuration + run: | + echo "Checking Kontrol configuration..." + + # Check for config file + if [ -f "./kontrol.toml" ]; then + echo "Found kontrol.toml:" + cat ./kontrol.toml + else + echo "kontrol.toml not found, checking for kontrol.json..." + if [ -f "./kontrol.json" ]; then + echo "Found kontrol.json:" + cat ./kontrol.json + else + echo "No Kontrol configuration file found" + echo "Creating default configuration..." + kontrol init + fi + fi + + # Show available profiles + echo "Available configuration profiles:" + kontrol prove --list-profiles || echo "No profiles configured" - name: Run Formal Verification with Kontrol run: | mkdir -p verification-results - verified_count=0 - for spec in src/test/kontrol/*.k; do - if [ -f "$spec" ]; then - echo "Verifying $(basename "$spec")..." - - if kontrol prove "$spec" \ - --contract-dir ./src/contracts \ - --output-dir ./verification-results \ - --verbose; then - echo "✓ Verification successful for $spec" - ((verified_count++)) - else - echo "✗ Verification failed for $spec" - cat "./verification-results/$(basename "$spec" .k).out" 2>/dev/null || echo "No output file found" - exit 1 - fi - fi - done + # Debug: Show working directory and files + echo "Current directory: $(pwd)" + echo "Contracts directory content:" + ls -R ./src/contracts + echo "Specification directory content:" + ls -R ./src/test/kontrol - if [ $verified_count -eq 0 ]; then - echo "No specification files found to verify" + # Step 1: Build Kontrol project + echo "Building Kontrol project..." + kontrol build || { + echo "Failed to build Kontrol project" + exit 1 + } + + # Step 2: Run setup profile + echo "Running setup profile..." + kontrol prove --config-profile setup || { + echo "Setup profile verification failed" + kontrol list + exit 1 + } + + # Step 3: Run tests profile + echo "Running tests profile..." + kontrol prove --config-profile tests || { + echo "Tests profile verification failed" + kontrol list + exit 1 + } + + # Step 4: Show verification results + echo "Listing all verification results..." + kontrol list | tee verification-results/final-results.txt + + # Check if any verifications failed + if ! grep -q "Status: proved" verification-results/final-results.txt; then + echo "Some verifications failed. Check the results above." exit 1 - else - echo "Successfully verified $verified_count specification(s)" fi - name: Upload Verification Results @@ -109,5 +153,8 @@ jobs: uses: actions/upload-artifact@v3 with: name: kontrol-verification-results - path: verification-results/ + path: | + verification-results/ + .build/ + .kontrol/ retention-days: 5 \ No newline at end of file From 7437546bf61ed8d5ad9f66acf6671060ead5fa33 Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Fri, 15 Nov 2024 20:46:36 -0500 Subject: [PATCH 53/97] kontrol run fv get rid of src/contracts ls --- .github/workflows/ci.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index 12a30295..c42e0e7d 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -111,7 +111,7 @@ jobs: # Debug: Show working directory and files echo "Current directory: $(pwd)" echo "Contracts directory content:" - ls -R ./src/contracts + ls -R ./src echo "Specification directory content:" ls -R ./src/test/kontrol From 73c4afcf5f6864256674671506e681eab55bbfb7 Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Fri, 15 Nov 2024 20:58:05 -0500 Subject: [PATCH 54/97] kontrol wiuth foundry --- .github/workflows/ci.yaml | 24 +++++++++++++++++++++++- 1 file changed, 23 insertions(+), 1 deletion(-) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index c42e0e7d..722285d2 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -32,6 +32,18 @@ jobs: fetch-depth: 0 submodules: recursive + # Install Foundry first + - name: Install Foundry + uses: foundry-rs/foundry-toolchain@v1 + with: + version: nightly + + - name: Install forge-std and build + run: | + forge install foundry-rs/forge-std --no-commit + forge build --build-info --force + forge remappings > remappings.txt + - name: Install System Dependencies run: | sudo apt-get update @@ -100,6 +112,10 @@ jobs: fi fi + # Verify forge is available + echo "Verifying forge installation:" + forge --version + # Show available profiles echo "Available configuration profiles:" kontrol prove --list-profiles || echo "No profiles configured" @@ -111,10 +127,15 @@ jobs: # Debug: Show working directory and files echo "Current directory: $(pwd)" echo "Contracts directory content:" - ls -R ./src + ls -R ./src/contracts echo "Specification directory content:" ls -R ./src/test/kontrol + # Verify forge is in PATH + echo "Verifying forge is available:" + which forge + forge --version + # Step 1: Build Kontrol project echo "Building Kontrol project..." kontrol build || { @@ -157,4 +178,5 @@ jobs: verification-results/ .build/ .kontrol/ + out/ retention-days: 5 \ No newline at end of file From 719f461c0cade436af82c3f81b10e8297bb2459a Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Fri, 15 Nov 2024 21:11:45 -0500 Subject: [PATCH 55/97] kontrol wiuth foundry --- .github/workflows/ci.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index 722285d2..b2a56f7d 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -127,7 +127,7 @@ jobs: # Debug: Show working directory and files echo "Current directory: $(pwd)" echo "Contracts directory content:" - ls -R ./src/contracts + ls -R ./src echo "Specification directory content:" ls -R ./src/test/kontrol From b53553d0186cc904ccfa62fbc904840597ca52d8 Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Sat, 16 Nov 2024 10:22:07 -0500 Subject: [PATCH 56/97] split up fv tests --- .github/workflows/ci.yaml | 176 +++++++++++++++++++++----------------- 1 file changed, 98 insertions(+), 78 deletions(-) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index b2a56f7d..c28bfe94 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -23,16 +23,17 @@ jobs: - name: Run snapshot without Kontrol tests run: forge snapshot --no-match-path "src/test/kontrol/*" - formal-verification: - runs-on: ubuntu-latest + setup-verification: needs: foundry-test + runs-on: ubuntu-latest + timeout-minutes: 60 # 1 hour for setup steps: - uses: actions/checkout@v4 with: fetch-depth: 0 submodules: recursive - # Install Foundry first + # Install Foundry - name: Install Foundry uses: foundry-rs/foundry-toolchain@v1 with: @@ -67,7 +68,6 @@ jobs: env: REPOSITORY_TOKEN: ${{ secrets.REPOSITORY_TOKEN }} run: | - # Configure git for private repository access git config --global url."https://${REPOSITORY_TOKEN}:x-oauth-basic@github.com/".insteadOf "https://github.com/" echo "Installing kup..." @@ -76,7 +76,6 @@ jobs: --option extra-trusted-public-keys 'k-framework.cachix.org-1:jeyMXB2h28gpNRjuVkehg+zLj62ma1RnyyopA/20yFE=' \ --experimental-features 'nix-command flakes' - # Add kup to PATH export PATH=$PATH:$HOME/.nix-profile/bin echo "$HOME/.nix-profile/bin" >> $GITHUB_PATH @@ -89,94 +88,115 @@ jobs: echo "Verifying Kontrol installation..." which kontrol || { echo "kontrol not found in PATH"; exit 1; } - echo "Kontrol version:" kontrol version || { echo "kontrol not working properly"; exit 1; } - - name: Check Kontrol Configuration + - name: Run Setup Verification run: | - echo "Checking Kontrol configuration..." - - # Check for config file - if [ -f "./kontrol.toml" ]; then - echo "Found kontrol.toml:" - cat ./kontrol.toml - else - echo "kontrol.toml not found, checking for kontrol.json..." - if [ -f "./kontrol.json" ]; then - echo "Found kontrol.json:" - cat ./kontrol.json - else - echo "No Kontrol configuration file found" - echo "Creating default configuration..." - kontrol init - fi - fi - - # Verify forge is available - echo "Verifying forge installation:" - forge --version + mkdir -p verification-results + echo "Building Kontrol project..." + kontrol build --verbose - # Show available profiles - echo "Available configuration profiles:" - kontrol prove --list-profiles || echo "No profiles configured" + echo "Running setup verification..." + kontrol prove --config-profile setup --verbose + + - name: Upload Setup Results + if: always() + uses: actions/upload-artifact@v3 + with: + name: setup-verification-results + path: | + verification-results/ + .build/ + .kontrol/ + retention-days: 5 - - name: Run Formal Verification with Kontrol + repo-token-tests: + needs: setup-verification + runs-on: ubuntu-latest + timeout-minutes: 350 # Maximum safe timeout for GitHub-hosted runners + steps: + # Copy all setup steps from setup-verification job + # (Previous steps remain identical until verification) + + - name: Run RepoToken Tests run: | mkdir -p verification-results - - # Debug: Show working directory and files - echo "Current directory: $(pwd)" - echo "Contracts directory content:" - ls -R ./src - echo "Specification directory content:" - ls -R ./src/test/kontrol - - # Verify forge is in PATH - echo "Verifying forge is available:" - which forge - forge --version - - # Step 1: Build Kontrol project echo "Building Kontrol project..." - kontrol build || { - echo "Failed to build Kontrol project" - exit 1 - } + kontrol build --verbose - # Step 2: Run setup profile - echo "Running setup profile..." - kontrol prove --config-profile setup || { - echo "Setup profile verification failed" - kontrol list - exit 1 - } - - # Step 3: Run tests profile - echo "Running tests profile..." - kontrol prove --config-profile tests || { - echo "Tests profile verification failed" - kontrol list - exit 1 - } - - # Step 4: Show verification results - echo "Listing all verification results..." - kontrol list | tee verification-results/final-results.txt - - # Check if any verifications failed - if ! grep -q "Status: proved" verification-results/final-results.txt; then - echo "Some verifications failed. Check the results above." - exit 1 - fi + echo "Running RepoToken tests..." + kontrol prove \ + --verbose \ + --include "src%test%kontrol%RepoTokenListInvariantsTest.*" \ + --config-profile tests + + - name: Upload RepoToken Results + if: always() + uses: actions/upload-artifact@v3 + with: + name: repo-token-verification-results + path: | + verification-results/ + .build/ + .kontrol/ + retention-days: 5 - - name: Upload Verification Results + term-auction-tests: + needs: setup-verification + runs-on: ubuntu-latest + timeout-minutes: 350 # Maximum safe timeout for GitHub-hosted runners + steps: + # Copy all setup steps from setup-verification job + # (Previous steps remain identical until verification) + + - name: Run TermAuction Tests + run: | + mkdir -p verification-results + echo "Building Kontrol project..." + kontrol build --verbose + + echo "Running TermAuction tests..." + kontrol prove \ + --verbose \ + --include "src%test%kontrol%TermAuctionListInvariantsTest.*" \ + --config-profile tests + + - name: Upload TermAuction Results if: always() uses: actions/upload-artifact@v3 with: - name: kontrol-verification-results + name: term-auction-verification-results path: | verification-results/ .build/ .kontrol/ - out/ + retention-days: 5 + + results-summary: + needs: [setup-verification, repo-token-tests, term-auction-tests] + runs-on: ubuntu-latest + if: always() + steps: + - name: Download All Results + uses: actions/download-artifact@v3 + with: + path: all-results + + - name: Generate Summary + run: | + echo "# Kontrol Verification Summary" > summary.md + echo "## Setup Verification" >> summary.md + find all-results/setup-verification-results -type f -name "*.out" -exec cat {} \; >> summary.md 2>/dev/null || echo "No setup results found" >> summary.md + + echo "## RepoToken Tests" >> summary.md + find all-results/repo-token-verification-results -type f -name "*.out" -exec cat {} \; >> summary.md 2>/dev/null || echo "No RepoToken results found" >> summary.md + + echo "## TermAuction Tests" >> summary.md + find all-results/term-auction-verification-results -type f -name "*.out" -exec cat {} \; >> summary.md 2>/dev/null || echo "No TermAuction results found" >> summary.md + + - name: Upload Summary + uses: actions/upload-artifact@v3 + with: + name: verification-summary + path: summary.md retention-days: 5 \ No newline at end of file From 8c7323a0e6f8d45983901679f9ef855d012f872a Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Sat, 16 Nov 2024 11:33:55 -0500 Subject: [PATCH 57/97] split up fv tests --- .github/workflows/ci.yaml | 144 +++++++++++++++++++++++++++++++++++--- 1 file changed, 134 insertions(+), 10 deletions(-) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index c28bfe94..3e4c5620 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -2,6 +2,9 @@ name: CI on: [push] +env: + NIX_INSTALLABLE_PACKAGE: github:runtimeverification/kup#kup + jobs: foundry-test: runs-on: ubuntu-latest @@ -76,7 +79,7 @@ jobs: --option extra-trusted-public-keys 'k-framework.cachix.org-1:jeyMXB2h28gpNRjuVkehg+zLj62ma1RnyyopA/20yFE=' \ --experimental-features 'nix-command flakes' - export PATH=$PATH:$HOME/.nix-profile/bin + export PATH="$HOME/.nix-profile/bin:$PATH" echo "$HOME/.nix-profile/bin" >> $GITHUB_PATH echo "Verifying kup installation..." @@ -98,7 +101,7 @@ jobs: echo "Running setup verification..." kontrol prove --config-profile setup --verbose - + - name: Upload Setup Results if: always() uses: actions/upload-artifact@v3 @@ -115,9 +118,69 @@ jobs: runs-on: ubuntu-latest timeout-minutes: 350 # Maximum safe timeout for GitHub-hosted runners steps: - # Copy all setup steps from setup-verification job - # (Previous steps remain identical until verification) - + - uses: actions/checkout@v4 + with: + fetch-depth: 0 + submodules: recursive + + - name: Install Foundry + uses: foundry-rs/foundry-toolchain@v1 + with: + version: nightly + + - name: Install forge-std and build + run: | + forge install foundry-rs/forge-std --no-commit + forge build --build-info --force + forge remappings > remappings.txt + + - name: Install System Dependencies + run: | + sudo apt-get update + sudo apt-get install -y curl gcc git g++ cmake maven openjdk-11-jdk flex \ + z3 libz3-dev libsecp256k1-dev python3 python3-pip build-essential + + # Install Nix + - uses: DeterminateSystems/nix-installer-action@main + with: + extra-conf: | + trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= k-framework.cachix.org-1:jeyMXB2h28gpNRjuVkehg+zLj62ma1RnyyopA/20yFE= k-framework-binary.cachix.org-1:pJedQ8iG19BW3v/DMMmiRVtwRBGO3fyMv2Ws0OpBADs= + substituters = https://cache.nixos.org https://k-framework.cachix.org + + # Install Cachix + - uses: cachix/cachix-action@v12 + with: + name: k-framework + extraPullNames: k-framework-binary + + - name: Install KUP and Kontrol + env: + REPOSITORY_TOKEN: ${{ secrets.REPOSITORY_TOKEN }} + run: | + git config --global url."https://${REPOSITORY_TOKEN}:x-oauth-basic@github.com/".insteadOf "https://github.com/" + + echo "Installing kup..." + GC_DONT_GC=1 nix profile install github:runtimeverification/kup#kup \ + --option extra-substituters 'https://k-framework.cachix.org' \ + --option extra-trusted-public-keys 'k-framework.cachix.org-1:jeyMXB2h28gpNRjuVkehg+zLj62ma1RnyyopA/20yFE=' \ + --experimental-features 'nix-command flakes' + + export PATH="$HOME/.nix-profile/bin:$PATH" + echo "$HOME/.nix-profile/bin" >> $GITHUB_PATH + + echo "Installing Kontrol..." + GITHUB_TOKEN=$REPOSITORY_TOKEN kup install kontrol + + echo "Verifying Kontrol installation..." + which kontrol || { echo "kontrol not found in PATH"; exit 1; } + kontrol version || { echo "kontrol not working properly"; exit 1; } + + - name: Download Setup Results + uses: actions/download-artifact@v3 + with: + name: setup-verification-results + path: . + - name: Run RepoToken Tests run: | mkdir -p verification-results @@ -129,7 +192,7 @@ jobs: --verbose \ --include "src%test%kontrol%RepoTokenListInvariantsTest.*" \ --config-profile tests - + - name: Upload RepoToken Results if: always() uses: actions/upload-artifact@v3 @@ -146,9 +209,70 @@ jobs: runs-on: ubuntu-latest timeout-minutes: 350 # Maximum safe timeout for GitHub-hosted runners steps: - # Copy all setup steps from setup-verification job - # (Previous steps remain identical until verification) - + # Copy all installation steps from repo-token-tests + - uses: actions/checkout@v4 + with: + fetch-depth: 0 + submodules: recursive + + - name: Install Foundry + uses: foundry-rs/foundry-toolchain@v1 + with: + version: nightly + + - name: Install forge-std and build + run: | + forge install foundry-rs/forge-std --no-commit + forge build --build-info --force + forge remappings > remappings.txt + + - name: Install System Dependencies + run: | + sudo apt-get update + sudo apt-get install -y curl gcc git g++ cmake maven openjdk-11-jdk flex \ + z3 libz3-dev libsecp256k1-dev python3 python3-pip build-essential + + # Install Nix + - uses: DeterminateSystems/nix-installer-action@main + with: + extra-conf: | + trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= k-framework.cachix.org-1:jeyMXB2h28gpNRjuVkehg+zLj62ma1RnyyopA/20yFE= k-framework-binary.cachix.org-1:pJedQ8iG19BW3v/DMMmiRVtwRBGO3fyMv2Ws0OpBADs= + substituters = https://cache.nixos.org https://k-framework.cachix.org + + # Install Cachix + - uses: cachix/cachix-action@v12 + with: + name: k-framework + extraPullNames: k-framework-binary + + - name: Install KUP and Kontrol + env: + REPOSITORY_TOKEN: ${{ secrets.REPOSITORY_TOKEN }} + run: | + git config --global url."https://${REPOSITORY_TOKEN}:x-oauth-basic@github.com/".insteadOf "https://github.com/" + + echo "Installing kup..." + GC_DONT_GC=1 nix profile install github:runtimeverification/kup#kup \ + --option extra-substituters 'https://k-framework.cachix.org' \ + --option extra-trusted-public-keys 'k-framework.cachix.org-1:jeyMXB2h28gpNRjuVkehg+zLj62ma1RnyyopA/20yFE=' \ + --experimental-features 'nix-command flakes' + + export PATH="$HOME/.nix-profile/bin:$PATH" + echo "$HOME/.nix-profile/bin" >> $GITHUB_PATH + + echo "Installing Kontrol..." + GITHUB_TOKEN=$REPOSITORY_TOKEN kup install kontrol + + echo "Verifying Kontrol installation..." + which kontrol || { echo "kontrol not found in PATH"; exit 1; } + kontrol version || { echo "kontrol not working properly"; exit 1; } + + - name: Download Setup Results + uses: actions/download-artifact@v3 + with: + name: setup-verification-results + path: . + - name: Run TermAuction Tests run: | mkdir -p verification-results @@ -160,7 +284,7 @@ jobs: --verbose \ --include "src%test%kontrol%TermAuctionListInvariantsTest.*" \ --config-profile tests - + - name: Upload TermAuction Results if: always() uses: actions/upload-artifact@v3 From 87b7ec6ca5cd098b247174eace52a79721c0986f Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Sat, 16 Nov 2024 14:23:47 -0500 Subject: [PATCH 58/97] more library caching --- .github/workflows/ci.yaml | 263 ++++++++++++++++++++++---------------- 1 file changed, 155 insertions(+), 108 deletions(-) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index 3e4c5620..fd068251 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -36,7 +36,6 @@ jobs: fetch-depth: 0 submodules: recursive - # Install Foundry - name: Install Foundry uses: foundry-rs/foundry-toolchain@v1 with: @@ -82,10 +81,6 @@ jobs: export PATH="$HOME/.nix-profile/bin:$PATH" echo "$HOME/.nix-profile/bin" >> $GITHUB_PATH - echo "Verifying kup installation..." - which kup || { echo "kup not found in PATH"; exit 1; } - kup list || { echo "kup not working properly"; exit 1; } - echo "Installing Kontrol..." GITHUB_TOKEN=$REPOSITORY_TOKEN kup install kontrol @@ -93,6 +88,16 @@ jobs: which kontrol || { echo "kontrol not found in PATH"; exit 1; } kontrol version || { echo "kontrol not working properly"; exit 1; } + - name: Cache Kontrol Build + uses: actions/cache@v3 + with: + path: | + .build + .kontrol + key: kontrol-cache-${{ github.sha }} + restore-keys: | + kontrol-cache- + - name: Run Setup Verification run: | mkdir -p verification-results @@ -109,11 +114,110 @@ jobs: name: setup-verification-results path: | verification-results/ - .build/ - .kontrol/ retention-days: 5 - repo-token-tests: + needs: setup-verification + runs-on: ubuntu-latest + timeout-minutes: 350 # Maximum safe timeout for GitHub-hosted runners + steps: + - uses: actions/checkout@v4 + with: + fetch-depth: 0 + submodules: recursive + + - name: Install Foundry + uses: foundry-rs/foundry-toolchain@v1 + with: + version: nightly + + - name: Install forge-std and build + run: | + forge install foundry-rs/forge-std --no-commit + forge build --build-info --force + forge remappings > remappings.txt + + - name: Install System Dependencies + run: | + sudo apt-get update + sudo apt-get install -y curl gcc git g++ cmake maven openjdk-11-jdk flex \ + z3 libz3-dev libsecp256k1-dev python3 python3-pip build-essential + + # Install Nix + - uses: DeterminateSystems/nix-installer-action@main + with: + extra-conf: | + trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= k-framework.cachix.org-1:jeyMXB2h28gpNRjuVkehg+zLj62ma1RnyyopA/20yFE= k-framework-binary.cachix.org-1:pJedQ8iG19BW3v/DMMmiRVtwRBGO3fyMv2Ws0OpBADs= + substituters = https://cache.nixos.org https://k-framework.cachix.org + + # Install Cachix + - uses: cachix/cachix-action@v12 + with: + name: k-framework + extraPullNames: k-framework-binary + + - name: Install KUP and Kontrol + env: + REPOSITORY_TOKEN: ${{ secrets.REPOSITORY_TOKEN }} + run: | + git config --global url."https://${REPOSITORY_TOKEN}:x-oauth-basic@github.com/".insteadOf "https://github.com/" + + echo "Installing kup..." + GC_DONT_GC=1 nix profile install github:runtimeverification/kup#kup \ + --option extra-substituters 'https://k-framework.cachix.org' \ + --option extra-trusted-public-keys 'k-framework.cachix.org-1:jeyMXB2h28gpNRjuVkehg+zLj62ma1RnyyopA/20yFE=' \ + --experimental-features 'nix-command flakes' + + export PATH="$HOME/.nix-profile/bin:$PATH" + echo "$HOME/.nix-profile/bin" >> $GITHUB_PATH + + echo "Installing Kontrol..." + GITHUB_TOKEN=$REPOSITORY_TOKEN kup install kontrol + + echo "Verifying Kontrol installation..." + which kontrol || { echo "kontrol not found in PATH"; exit 1; } + kontrol version || { echo "kontrol not working properly"; exit 1; } + + - name: Cache Kontrol Build + uses: actions/cache@v3 + with: + path: | + .build + .kontrol + key: kontrol-cache-${{ github.sha }} + restore-keys: | + kontrol-cache- + + - name: Restore or Initialize Kontrol State + run: | + if [ -d ".build" ] && [ -d ".kontrol" ]; then + echo "Restored Kontrol state from cache" + ls -la .build + ls -la .kontrol + else + echo "No cached state found, initializing..." + mkdir -p .build .kontrol + kontrol build --verbose + fi + + - name: Run RepoToken Tests + run: | + mkdir -p verification-results + + echo "Running RepoToken tests..." + kontrol prove \ + --verbose \ + --include "src%test%kontrol%RepoTokenListInvariantsTest.*" \ + --config-profile tests + + - name: Upload RepoToken Results + if: always() + uses: actions/upload-artifact@v3 + with: + name: repo-token-verification-results + path: | + verification-results/ + retention-days: 5 + term-auction-tests: needs: setup-verification runs-on: ubuntu-latest timeout-minutes: 350 # Maximum safe timeout for GitHub-hosted runners @@ -174,110 +278,32 @@ jobs: echo "Verifying Kontrol installation..." which kontrol || { echo "kontrol not found in PATH"; exit 1; } kontrol version || { echo "kontrol not working properly"; exit 1; } - - - name: Download Setup Results - uses: actions/download-artifact@v3 - with: - name: setup-verification-results - path: . - - name: Run RepoToken Tests - run: | - mkdir -p verification-results - echo "Building Kontrol project..." - kontrol build --verbose - - echo "Running RepoToken tests..." - kontrol prove \ - --verbose \ - --include "src%test%kontrol%RepoTokenListInvariantsTest.*" \ - --config-profile tests - - - name: Upload RepoToken Results - if: always() - uses: actions/upload-artifact@v3 + - name: Cache Kontrol Build + uses: actions/cache@v3 with: - name: repo-token-verification-results path: | - verification-results/ - .build/ - .kontrol/ - retention-days: 5 + .build + .kontrol + key: kontrol-cache-${{ github.sha }} + restore-keys: | + kontrol-cache- - term-auction-tests: - needs: setup-verification - runs-on: ubuntu-latest - timeout-minutes: 350 # Maximum safe timeout for GitHub-hosted runners - steps: - # Copy all installation steps from repo-token-tests - - uses: actions/checkout@v4 - with: - fetch-depth: 0 - submodules: recursive - - - name: Install Foundry - uses: foundry-rs/foundry-toolchain@v1 - with: - version: nightly - - - name: Install forge-std and build + - name: Restore or Initialize Kontrol State run: | - forge install foundry-rs/forge-std --no-commit - forge build --build-info --force - forge remappings > remappings.txt - - - name: Install System Dependencies - run: | - sudo apt-get update - sudo apt-get install -y curl gcc git g++ cmake maven openjdk-11-jdk flex \ - z3 libz3-dev libsecp256k1-dev python3 python3-pip build-essential - - # Install Nix - - uses: DeterminateSystems/nix-installer-action@main - with: - extra-conf: | - trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= k-framework.cachix.org-1:jeyMXB2h28gpNRjuVkehg+zLj62ma1RnyyopA/20yFE= k-framework-binary.cachix.org-1:pJedQ8iG19BW3v/DMMmiRVtwRBGO3fyMv2Ws0OpBADs= - substituters = https://cache.nixos.org https://k-framework.cachix.org - - # Install Cachix - - uses: cachix/cachix-action@v12 - with: - name: k-framework - extraPullNames: k-framework-binary - - - name: Install KUP and Kontrol - env: - REPOSITORY_TOKEN: ${{ secrets.REPOSITORY_TOKEN }} - run: | - git config --global url."https://${REPOSITORY_TOKEN}:x-oauth-basic@github.com/".insteadOf "https://github.com/" - - echo "Installing kup..." - GC_DONT_GC=1 nix profile install github:runtimeverification/kup#kup \ - --option extra-substituters 'https://k-framework.cachix.org' \ - --option extra-trusted-public-keys 'k-framework.cachix.org-1:jeyMXB2h28gpNRjuVkehg+zLj62ma1RnyyopA/20yFE=' \ - --experimental-features 'nix-command flakes' - - export PATH="$HOME/.nix-profile/bin:$PATH" - echo "$HOME/.nix-profile/bin" >> $GITHUB_PATH - - echo "Installing Kontrol..." - GITHUB_TOKEN=$REPOSITORY_TOKEN kup install kontrol - - echo "Verifying Kontrol installation..." - which kontrol || { echo "kontrol not found in PATH"; exit 1; } - kontrol version || { echo "kontrol not working properly"; exit 1; } - - - name: Download Setup Results - uses: actions/download-artifact@v3 - with: - name: setup-verification-results - path: . + if [ -d ".build" ] && [ -d ".kontrol" ]; then + echo "Restored Kontrol state from cache" + ls -la .build + ls -la .kontrol + else + echo "No cached state found, initializing..." + mkdir -p .build .kontrol + kontrol build --verbose + fi - name: Run TermAuction Tests run: | mkdir -p verification-results - echo "Building Kontrol project..." - kontrol build --verbose echo "Running TermAuction tests..." kontrol prove \ @@ -292,8 +318,6 @@ jobs: name: term-auction-verification-results path: | verification-results/ - .build/ - .kontrol/ retention-days: 5 results-summary: @@ -309,14 +333,37 @@ jobs: - name: Generate Summary run: | echo "# Kontrol Verification Summary" > summary.md + echo "## Setup Verification" >> summary.md - find all-results/setup-verification-results -type f -name "*.out" -exec cat {} \; >> summary.md 2>/dev/null || echo "No setup results found" >> summary.md + if [ -d "all-results/setup-verification-results" ]; then + echo "\`\`\`" >> summary.md + find all-results/setup-verification-results -type f -exec cat {} \; >> summary.md || echo "No setup results found" + echo "\`\`\`" >> summary.md + else + echo "No setup verification results found" >> summary.md + fi echo "## RepoToken Tests" >> summary.md - find all-results/repo-token-verification-results -type f -name "*.out" -exec cat {} \; >> summary.md 2>/dev/null || echo "No RepoToken results found" >> summary.md + if [ -d "all-results/repo-token-verification-results" ]; then + echo "\`\`\`" >> summary.md + find all-results/repo-token-verification-results -type f -exec cat {} \; >> summary.md || echo "No RepoToken results found" + echo "\`\`\`" >> summary.md + else + echo "No RepoToken verification results found" >> summary.md + fi echo "## TermAuction Tests" >> summary.md - find all-results/term-auction-verification-results -type f -name "*.out" -exec cat {} \; >> summary.md 2>/dev/null || echo "No TermAuction results found" >> summary.md + if [ -d "all-results/term-auction-verification-results" ]; then + echo "\`\`\`" >> summary.md + find all-results/term-auction-verification-results -type f -exec cat {} \; >> summary.md || echo "No TermAuction results found" + echo "\`\`\`" >> summary.md + else + echo "No TermAuction verification results found" >> summary.md + fi + + # Add timestamp + echo -e "\n## Run Information" >> summary.md + echo "Generated at: $(date)" >> summary.md - name: Upload Summary uses: actions/upload-artifact@v3 From ed709abf660c6fb77686c2ea6785ee03fa44ae3c Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Sat, 16 Nov 2024 18:24:02 -0500 Subject: [PATCH 59/97] out of memory on tests --- .github/workflows/ci.yaml | 541 ++++++++++++++++++++++++++++---------- 1 file changed, 407 insertions(+), 134 deletions(-) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index fd068251..c72448f5 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -29,7 +29,7 @@ jobs: setup-verification: needs: foundry-test runs-on: ubuntu-latest - timeout-minutes: 60 # 1 hour for setup + timeout-minutes: 60 steps: - uses: actions/checkout@v4 with: @@ -88,12 +88,41 @@ jobs: which kontrol || { echo "kontrol not found in PATH"; exit 1; } kontrol version || { echo "kontrol not working properly"; exit 1; } + - name: Verify Kontrol Environment + run: | + echo "Checking Kontrol environment..." + + # Check for required directories + for dir in .build .kontrol "out/proofs"; do + if [ ! -d "$dir" ]; then + echo "Creating $dir..." + mkdir -p "$dir" + fi + echo "Contents of $dir:" + ls -la "$dir" + done + + # Test Kontrol functionality + echo "Testing Kontrol..." + kontrol version + kontrol list + + # Check proof directory permissions + echo "Checking permissions..." + stat out/proofs + + # Verify forge build info + echo "Checking forge build..." + test -d out/proofs || echo "out/proofs missing" + forge build --build-info --force + - name: Cache Kontrol Build uses: actions/cache@v3 with: path: | .build .kontrol + out/proofs key: kontrol-cache-${{ github.sha }} restore-keys: | kontrol-cache- @@ -115,112 +144,228 @@ jobs: path: | verification-results/ retention-days: 5 - repo-token-tests: - needs: setup-verification - runs-on: ubuntu-latest - timeout-minutes: 350 # Maximum safe timeout for GitHub-hosted runners - steps: - - uses: actions/checkout@v4 - with: - fetch-depth: 0 - submodules: recursive - - - name: Install Foundry - uses: foundry-rs/foundry-toolchain@v1 - with: - version: nightly - - - name: Install forge-std and build - run: | - forge install foundry-rs/forge-std --no-commit - forge build --build-info --force - forge remappings > remappings.txt - - - name: Install System Dependencies - run: | - sudo apt-get update - sudo apt-get install -y curl gcc git g++ cmake maven openjdk-11-jdk flex \ - z3 libz3-dev libsecp256k1-dev python3 python3-pip build-essential - - # Install Nix - - uses: DeterminateSystems/nix-installer-action@main - with: - extra-conf: | - trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= k-framework.cachix.org-1:jeyMXB2h28gpNRjuVkehg+zLj62ma1RnyyopA/20yFE= k-framework-binary.cachix.org-1:pJedQ8iG19BW3v/DMMmiRVtwRBGO3fyMv2Ws0OpBADs= - substituters = https://cache.nixos.org https://k-framework.cachix.org - - # Install Cachix - - uses: cachix/cachix-action@v12 - with: - name: k-framework - extraPullNames: k-framework-binary - - - name: Install KUP and Kontrol - env: - REPOSITORY_TOKEN: ${{ secrets.REPOSITORY_TOKEN }} - run: | - git config --global url."https://${REPOSITORY_TOKEN}:x-oauth-basic@github.com/".insteadOf "https://github.com/" +repo-token-tests: + needs: setup-verification + runs-on: ubuntu-latest + timeout-minutes: 350 + steps: + - uses: actions/checkout@v4 + with: + fetch-depth: 0 + submodules: recursive + + - name: Install Foundry + uses: foundry-rs/foundry-toolchain@v1 + with: + version: nightly + + - name: Install forge-std and build + run: | + forge install foundry-rs/forge-std --no-commit + forge build --build-info --force + forge remappings > remappings.txt + + - name: Install System Dependencies + run: | + sudo apt-get update + sudo apt-get install -y curl gcc git g++ cmake maven openjdk-11-jdk flex \ + z3 libz3-dev libsecp256k1-dev python3 python3-pip build-essential + + - uses: DeterminateSystems/nix-installer-action@main + with: + extra-conf: | + trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= k-framework.cachix.org-1:jeyMXB2h28gpNRjuVkehg+zLj62ma1RnyyopA/20yFE= k-framework-binary.cachix.org-1:pJedQ8iG19BW3v/DMMmiRVtwRBGO3fyMv2Ws0OpBADs= + substituters = https://cache.nixos.org https://k-framework.cachix.org + + - uses: cachix/cachix-action@v12 + with: + name: k-framework + extraPullNames: k-framework-binary + + - name: Install KUP and Kontrol + env: + REPOSITORY_TOKEN: ${{ secrets.REPOSITORY_TOKEN }} + run: | + git config --global url."https://${REPOSITORY_TOKEN}:x-oauth-basic@github.com/".insteadOf "https://github.com/" + + echo "Installing kup..." + GC_DONT_GC=1 nix profile install github:runtimeverification/kup#kup \ + --option extra-substituters 'https://k-framework.cachix.org' \ + --option extra-trusted-public-keys 'k-framework.cachix.org-1:jeyMXB2h28gpNRjuVkehg+zLj62ma1RnyyopA/20yFE=' \ + --experimental-features 'nix-command flakes' + + export PATH="$HOME/.nix-profile/bin:$PATH" + echo "$HOME/.nix-profile/bin" >> $GITHUB_PATH + + echo "Installing Kontrol..." + GITHUB_TOKEN=$REPOSITORY_TOKEN kup install kontrol + + echo "Verifying Kontrol installation..." + which kontrol || { echo "kontrol not found in PATH"; exit 1; } + kontrol version || { echo "kontrol not working properly"; exit 1; } + + - name: Configure System Resources + run: | + # Show available memory + echo "Available memory:" + free -h + + # Clear system cache + sudo sh -c 'echo 3 > /proc/sys/vm/drop_caches' + + # Configure swap + sudo fallocate -l 8G /swapfile + sudo chmod 600 /swapfile + sudo mkswap /swapfile + sudo swapon /swapfile + + echo "Memory after swap configuration:" + free -h + + - name: Cache Kontrol Build + uses: actions/cache@v3 + with: + path: | + .build + .kontrol + out/proofs + key: kontrol-cache-${{ github.sha }} + restore-keys: | + kontrol-cache- + + - name: Prepare Verification Environment + run: | + mkdir -p .build .kontrol "out/proofs" + chmod -R 755 .build .kontrol "out/proofs" + rm -rf out/proofs/* + + # Clean any previous build artifacts + rm -rf out/kompiled + + if [ -d ".build" ] && [ -d ".kontrol" ]; then + echo "Restored Kontrol state from cache" + ls -la .build + ls -la .kontrol + else + echo "No cached state found, initializing..." + kontrol build --verbose + fi + + - name: Run RepoToken Tests with Memory Management + run: | + mkdir -p verification-results + + # Function to run verification with memory monitoring + run_verification() { + # Start memory monitoring in background + while true; do + free -h >> verification-results/memory-usage.log + sleep 30 + done & + MONITOR_PID=$! - echo "Installing kup..." - GC_DONT_GC=1 nix profile install github:runtimeverification/kup#kup \ - --option extra-substituters 'https://k-framework.cachix.org' \ - --option extra-trusted-public-keys 'k-framework.cachix.org-1:jeyMXB2h28gpNRjuVkehg+zLj62ma1RnyyopA/20yFE=' \ - --experimental-features 'nix-command flakes' + # List of test functions to run separately + TESTS=( + "testInsertSortedNewToken()" + "testInsertSortedDuplicateToken(address)" + "testRemoveAndRedeemMaturedTokens()" + ) - export PATH="$HOME/.nix-profile/bin:$PATH" - echo "$HOME/.nix-profile/bin" >> $GITHUB_PATH + # Run each test separately + for test in "${TESTS[@]}"; do + echo "Running test: $test" + kontrol prove \ + --verbose \ + --debug \ + --include "src%test%kontrol%RepoTokenListInvariantsTest.$test" \ + --config-profile tests \ + 2>&1 | tee -a verification-results/verification.log + + TEST_RESULT=$? + if [ $TEST_RESULT -ne 0 ]; then + echo "Test $test failed with exit code $TEST_RESULT" + return $TEST_RESULT + fi + + # Clear caches between tests + sudo sh -c 'echo 3 > /proc/sys/vm/drop_caches' + sleep 10 + done - echo "Installing Kontrol..." - GITHUB_TOKEN=$REPOSITORY_TOKEN kup install kontrol + # Stop memory monitoring + kill $MONITOR_PID + return 0 + } + + # Clean up function + cleanup() { + echo "Cleaning up..." + # Save debug information + tar czf verification-results/debug-state.tar.gz \ + .build .kontrol out/proofs verification-results \ + 2>/dev/null || true + } + + # Set trap for cleanup + trap cleanup EXIT + + # Run verification with retry logic + MAX_RETRIES=3 + RETRY_COUNT=0 + + while [ $RETRY_COUNT -lt $MAX_RETRIES ]; do + echo "Attempt $((RETRY_COUNT + 1)) of $MAX_RETRIES" - echo "Verifying Kontrol installation..." - which kontrol || { echo "kontrol not found in PATH"; exit 1; } - kontrol version || { echo "kontrol not working properly"; exit 1; } - - - name: Cache Kontrol Build - uses: actions/cache@v3 - with: - path: | - .build - .kontrol - key: kontrol-cache-${{ github.sha }} - restore-keys: | - kontrol-cache- - - - name: Restore or Initialize Kontrol State - run: | - if [ -d ".build" ] && [ -d ".kontrol" ]; then - echo "Restored Kontrol state from cache" - ls -la .build - ls -la .kontrol + if run_verification; then + echo "Verification successful!" + exit 0 else - echo "No cached state found, initializing..." - mkdir -p .build .kontrol - kontrol build --verbose + RETRY_COUNT=$((RETRY_COUNT + 1)) + echo "Verification failed. Exit code: $?" + + if [ $RETRY_COUNT -lt $MAX_RETRIES ]; then + echo "Cleaning up and retrying..." + sudo sh -c 'echo 3 > /proc/sys/vm/drop_caches' + sleep 30 + fi fi + done + + echo "All retry attempts failed" + exit 1 - - name: Run RepoToken Tests - run: | - mkdir -p verification-results + - name: Analyze Verification Results + if: always() + run: | + echo "Analyzing verification results..." + + if [ -f "verification-results/verification.log" ]; then + echo "Last 50 lines of verification log:" + tail -n 50 verification-results/verification.log + + echo "Memory usage during verification:" + cat verification-results/memory-usage.log - echo "Running RepoToken tests..." - kontrol prove \ - --verbose \ - --include "src%test%kontrol%RepoTokenListInvariantsTest.*" \ - --config-profile tests - - - name: Upload RepoToken Results - if: always() - uses: actions/upload-artifact@v3 - with: - name: repo-token-verification-results - path: | - verification-results/ - retention-days: 5 - term-auction-tests: + if grep -q "Out of memory" verification-results/verification.log; then + echo "Out of memory condition detected" + fi + fi + + - name: Upload Results + if: always() + uses: actions/upload-artifact@v3 + with: + name: repo-token-verification-results + path: | + verification-results/ + out/proofs/ + .build/ + .kontrol/ + retention-days: 5 +term-auction-tests: needs: setup-verification runs-on: ubuntu-latest - timeout-minutes: 350 # Maximum safe timeout for GitHub-hosted runners + timeout-minutes: 350 steps: - uses: actions/checkout@v4 with: @@ -244,14 +389,12 @@ jobs: sudo apt-get install -y curl gcc git g++ cmake maven openjdk-11-jdk flex \ z3 libz3-dev libsecp256k1-dev python3 python3-pip build-essential - # Install Nix - uses: DeterminateSystems/nix-installer-action@main with: extra-conf: | trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= k-framework.cachix.org-1:jeyMXB2h28gpNRjuVkehg+zLj62ma1RnyyopA/20yFE= k-framework-binary.cachix.org-1:pJedQ8iG19BW3v/DMMmiRVtwRBGO3fyMv2Ws0OpBADs= substituters = https://cache.nixos.org https://k-framework.cachix.org - # Install Cachix - uses: cachix/cachix-action@v12 with: name: k-framework @@ -279,45 +422,155 @@ jobs: which kontrol || { echo "kontrol not found in PATH"; exit 1; } kontrol version || { echo "kontrol not working properly"; exit 1; } + - name: Configure System Resources + run: | + echo "Available memory:" + free -h + + sudo sh -c 'echo 3 > /proc/sys/vm/drop_caches' + + sudo fallocate -l 8G /swapfile + sudo chmod 600 /swapfile + sudo mkswap /swapfile + sudo swapon /swapfile + + echo "Memory after swap configuration:" + free -h + - name: Cache Kontrol Build uses: actions/cache@v3 with: path: | .build .kontrol + out/proofs key: kontrol-cache-${{ github.sha }} restore-keys: | kontrol-cache- - - name: Restore or Initialize Kontrol State + - name: Prepare Verification Environment run: | + # Create necessary directories + mkdir -p .build .kontrol "out/proofs" + chmod -R 755 .build .kontrol "out/proofs" + + # Clean stale files + rm -rf out/proofs/* + rm -rf out/kompiled + if [ -d ".build" ] && [ -d ".kontrol" ]; then echo "Restored Kontrol state from cache" ls -la .build ls -la .kontrol else echo "No cached state found, initializing..." - mkdir -p .build .kontrol kontrol build --verbose fi - - name: Run TermAuction Tests + - name: Run TermAuction Tests with Memory Management run: | mkdir -p verification-results - echo "Running TermAuction tests..." - kontrol prove \ - --verbose \ - --include "src%test%kontrol%TermAuctionListInvariantsTest.*" \ - --config-profile tests + # Function to run verification with memory monitoring + run_verification() { + while true; do + free -h >> verification-results/memory-usage.log + sleep 30 + done & + MONITOR_PID=$! + + # List of test functions to run separately + TESTS=( + "testInsertPendingNewOffer(bytes32,address)" + "testInsertPendingDuplicateOffer(bytes32,(address,uint256,address,address),address)" + "testRemoveCompleted(address)" + ) + + # Run each test separately + for test in "${TESTS[@]}"; do + echo "Running test: $test" + kontrol prove \ + --verbose \ + --debug \ + --include "src%test%kontrol%TermAuctionListInvariantsTest.$test" \ + --config-profile tests \ + 2>&1 | tee -a verification-results/verification.log + + TEST_RESULT=$? + if [ $TEST_RESULT -ne 0 ]; then + echo "Test $test failed with exit code $TEST_RESULT" + return $TEST_RESULT + fi + + # Clear caches between tests + sudo sh -c 'echo 3 > /proc/sys/vm/drop_caches' + sleep 10 + done + + kill $MONITOR_PID + return 0 + } + + cleanup() { + echo "Cleaning up..." + tar czf verification-results/debug-state.tar.gz \ + .build .kontrol out/proofs verification-results \ + 2>/dev/null || true + } + + trap cleanup EXIT + + MAX_RETRIES=3 + RETRY_COUNT=0 + + while [ $RETRY_COUNT -lt $MAX_RETRIES ]; do + echo "Attempt $((RETRY_COUNT + 1)) of $MAX_RETRIES" + + if run_verification; then + echo "Verification successful!" + exit 0 + else + RETRY_COUNT=$((RETRY_COUNT + 1)) + echo "Verification failed. Exit code: $?" + + if [ $RETRY_COUNT -lt $MAX_RETRIES ]; then + echo "Cleaning up and retrying..." + sudo sh -c 'echo 3 > /proc/sys/vm/drop_caches' + sleep 30 + fi + fi + done + + echo "All retry attempts failed" + exit 1 + + - name: Analyze Verification Results + if: always() + run: | + echo "Analyzing verification results..." + + if [ -f "verification-results/verification.log" ]; then + echo "Last 50 lines of verification log:" + tail -n 50 verification-results/verification.log + + echo "Memory usage during verification:" + cat verification-results/memory-usage.log + + if grep -q "Out of memory" verification-results/verification.log; then + echo "Out of memory condition detected" + fi + fi - - name: Upload TermAuction Results + - name: Upload Results if: always() uses: actions/upload-artifact@v3 with: name: term-auction-verification-results path: | verification-results/ + out/proofs/ + .build/ + .kontrol/ retention-days: 5 results-summary: @@ -333,37 +586,57 @@ jobs: - name: Generate Summary run: | echo "# Kontrol Verification Summary" > summary.md + echo "Generated at: $(date)" >> summary.md + echo "" >> summary.md - echo "## Setup Verification" >> summary.md - if [ -d "all-results/setup-verification-results" ]; then - echo "\`\`\`" >> summary.md - find all-results/setup-verification-results -type f -exec cat {} \; >> summary.md || echo "No setup results found" - echo "\`\`\`" >> summary.md - else - echo "No setup verification results found" >> summary.md - fi - - echo "## RepoToken Tests" >> summary.md - if [ -d "all-results/repo-token-verification-results" ]; then + # Function to process results + process_results() { + local dir="$1" + local section="$2" + + echo "## $section" >> summary.md echo "\`\`\`" >> summary.md - find all-results/repo-token-verification-results -type f -exec cat {} \; >> summary.md || echo "No RepoToken results found" + + if [ -d "$dir" ]; then + # Check verification log + if [ -f "$dir/verification.log" ]; then + echo "### Verification Output" >> summary.md + tail -n 50 "$dir/verification.log" >> summary.md + fi + + # Check memory usage + if [ -f "$dir/memory-usage.log" ]; then + echo "### Memory Usage" >> summary.md + tail -n 10 "$dir/memory-usage.log" >> summary.md + fi + + # Check for specific errors + if grep -q "Out of memory" "$dir"/*.log 2>/dev/null; then + echo "⚠️ Out of Memory conditions detected" >> summary.md + fi + + # Add any successful proofs + if grep -q "PROOF PASSED" "$dir"/*.log 2>/dev/null; then + echo "✅ Successful proofs detected" >> summary.md + grep "PROOF PASSED" "$dir"/*.log >> summary.md + fi + else + echo "No results found for $section" >> summary.md + fi + echo "\`\`\`" >> summary.md - else - echo "No RepoToken verification results found" >> summary.md - fi + echo "" >> summary.md + } - echo "## TermAuction Tests" >> summary.md - if [ -d "all-results/term-auction-verification-results" ]; then - echo "\`\`\`" >> summary.md - find all-results/term-auction-verification-results -type f -exec cat {} \; >> summary.md || echo "No TermAuction results found" - echo "\`\`\`" >> summary.md - else - echo "No TermAuction verification results found" >> summary.md - fi + process_results "all-results/setup-verification-results" "Setup Verification" + process_results "all-results/repo-token-verification-results" "RepoToken Tests" + process_results "all-results/term-auction-verification-results" "TermAuction Tests" - # Add timestamp - echo -e "\n## Run Information" >> summary.md - echo "Generated at: $(date)" >> summary.md + # Add overall status + echo "## Overall Status" >> summary.md + echo "- Setup: $(test -d all-results/setup-verification-results && echo '✅' || echo '❌')" >> summary.md + echo "- RepoToken: $(test -d all-results/repo-token-verification-results && echo '✅' || echo '❌')" >> summary.md + echo "- TermAuction: $(test -d all-results/term-auction-verification-results && echo '✅' || echo '❌')" >> summary.md - name: Upload Summary uses: actions/upload-artifact@v3 From 4bf04dc76cc59bbf808fb0cf6e126a818e479f17 Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Sat, 16 Nov 2024 21:04:06 -0500 Subject: [PATCH 60/97] yaml format --- .github/workflows/ci.yaml | 808 +++++++++++++++++++------------------- 1 file changed, 404 insertions(+), 404 deletions(-) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index c72448f5..2125a464 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -144,434 +144,434 @@ jobs: path: | verification-results/ retention-days: 5 -repo-token-tests: - needs: setup-verification - runs-on: ubuntu-latest - timeout-minutes: 350 - steps: - - uses: actions/checkout@v4 - with: - fetch-depth: 0 - submodules: recursive - - - name: Install Foundry - uses: foundry-rs/foundry-toolchain@v1 - with: - version: nightly - - - name: Install forge-std and build - run: | - forge install foundry-rs/forge-std --no-commit - forge build --build-info --force - forge remappings > remappings.txt - - - name: Install System Dependencies - run: | - sudo apt-get update - sudo apt-get install -y curl gcc git g++ cmake maven openjdk-11-jdk flex \ - z3 libz3-dev libsecp256k1-dev python3 python3-pip build-essential - - - uses: DeterminateSystems/nix-installer-action@main - with: - extra-conf: | - trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= k-framework.cachix.org-1:jeyMXB2h28gpNRjuVkehg+zLj62ma1RnyyopA/20yFE= k-framework-binary.cachix.org-1:pJedQ8iG19BW3v/DMMmiRVtwRBGO3fyMv2Ws0OpBADs= - substituters = https://cache.nixos.org https://k-framework.cachix.org - - - uses: cachix/cachix-action@v12 - with: - name: k-framework - extraPullNames: k-framework-binary - - - name: Install KUP and Kontrol - env: - REPOSITORY_TOKEN: ${{ secrets.REPOSITORY_TOKEN }} - run: | - git config --global url."https://${REPOSITORY_TOKEN}:x-oauth-basic@github.com/".insteadOf "https://github.com/" - - echo "Installing kup..." - GC_DONT_GC=1 nix profile install github:runtimeverification/kup#kup \ - --option extra-substituters 'https://k-framework.cachix.org' \ - --option extra-trusted-public-keys 'k-framework.cachix.org-1:jeyMXB2h28gpNRjuVkehg+zLj62ma1RnyyopA/20yFE=' \ - --experimental-features 'nix-command flakes' - - export PATH="$HOME/.nix-profile/bin:$PATH" - echo "$HOME/.nix-profile/bin" >> $GITHUB_PATH - - echo "Installing Kontrol..." - GITHUB_TOKEN=$REPOSITORY_TOKEN kup install kontrol - - echo "Verifying Kontrol installation..." - which kontrol || { echo "kontrol not found in PATH"; exit 1; } - kontrol version || { echo "kontrol not working properly"; exit 1; } - - - name: Configure System Resources - run: | - # Show available memory - echo "Available memory:" - free -h - - # Clear system cache - sudo sh -c 'echo 3 > /proc/sys/vm/drop_caches' - - # Configure swap - sudo fallocate -l 8G /swapfile - sudo chmod 600 /swapfile - sudo mkswap /swapfile - sudo swapon /swapfile - - echo "Memory after swap configuration:" - free -h - - - name: Cache Kontrol Build - uses: actions/cache@v3 - with: - path: | - .build - .kontrol - out/proofs - key: kontrol-cache-${{ github.sha }} - restore-keys: | - kontrol-cache- + repo-token-tests: + needs: setup-verification + runs-on: ubuntu-latest + timeout-minutes: 350 + steps: + - uses: actions/checkout@v4 + with: + fetch-depth: 0 + submodules: recursive + + - name: Install Foundry + uses: foundry-rs/foundry-toolchain@v1 + with: + version: nightly + + - name: Install forge-std and build + run: | + forge install foundry-rs/forge-std --no-commit + forge build --build-info --force + forge remappings > remappings.txt + + - name: Install System Dependencies + run: | + sudo apt-get update + sudo apt-get install -y curl gcc git g++ cmake maven openjdk-11-jdk flex \ + z3 libz3-dev libsecp256k1-dev python3 python3-pip build-essential + + - uses: DeterminateSystems/nix-installer-action@main + with: + extra-conf: | + trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= k-framework.cachix.org-1:jeyMXB2h28gpNRjuVkehg+zLj62ma1RnyyopA/20yFE= k-framework-binary.cachix.org-1:pJedQ8iG19BW3v/DMMmiRVtwRBGO3fyMv2Ws0OpBADs= + substituters = https://cache.nixos.org https://k-framework.cachix.org + + - uses: cachix/cachix-action@v12 + with: + name: k-framework + extraPullNames: k-framework-binary + + - name: Install KUP and Kontrol + env: + REPOSITORY_TOKEN: ${{ secrets.REPOSITORY_TOKEN }} + run: | + git config --global url."https://${REPOSITORY_TOKEN}:x-oauth-basic@github.com/".insteadOf "https://github.com/" + + echo "Installing kup..." + GC_DONT_GC=1 nix profile install github:runtimeverification/kup#kup \ + --option extra-substituters 'https://k-framework.cachix.org' \ + --option extra-trusted-public-keys 'k-framework.cachix.org-1:jeyMXB2h28gpNRjuVkehg+zLj62ma1RnyyopA/20yFE=' \ + --experimental-features 'nix-command flakes' + + export PATH="$HOME/.nix-profile/bin:$PATH" + echo "$HOME/.nix-profile/bin" >> $GITHUB_PATH + + echo "Installing Kontrol..." + GITHUB_TOKEN=$REPOSITORY_TOKEN kup install kontrol + + echo "Verifying Kontrol installation..." + which kontrol || { echo "kontrol not found in PATH"; exit 1; } + kontrol version || { echo "kontrol not working properly"; exit 1; } + + - name: Configure System Resources + run: | + # Show available memory + echo "Available memory:" + free -h + + # Clear system cache + sudo sh -c 'echo 3 > /proc/sys/vm/drop_caches' + + # Configure swap + sudo fallocate -l 8G /swapfile + sudo chmod 600 /swapfile + sudo mkswap /swapfile + sudo swapon /swapfile + + echo "Memory after swap configuration:" + free -h + + - name: Cache Kontrol Build + uses: actions/cache@v3 + with: + path: | + .build + .kontrol + out/proofs + key: kontrol-cache-${{ github.sha }} + restore-keys: | + kontrol-cache- + + - name: Prepare Verification Environment + run: | + mkdir -p .build .kontrol "out/proofs" + chmod -R 755 .build .kontrol "out/proofs" + rm -rf out/proofs/* + + # Clean any previous build artifacts + rm -rf out/kompiled + + if [ -d ".build" ] && [ -d ".kontrol" ]; then + echo "Restored Kontrol state from cache" + ls -la .build + ls -la .kontrol + else + echo "No cached state found, initializing..." + kontrol build --verbose + fi - - name: Prepare Verification Environment - run: | - mkdir -p .build .kontrol "out/proofs" - chmod -R 755 .build .kontrol "out/proofs" - rm -rf out/proofs/* - - # Clean any previous build artifacts - rm -rf out/kompiled - - if [ -d ".build" ] && [ -d ".kontrol" ]; then - echo "Restored Kontrol state from cache" - ls -la .build - ls -la .kontrol - else - echo "No cached state found, initializing..." - kontrol build --verbose - fi - - - name: Run RepoToken Tests with Memory Management - run: | - mkdir -p verification-results - - # Function to run verification with memory monitoring - run_verification() { - # Start memory monitoring in background - while true; do - free -h >> verification-results/memory-usage.log - sleep 30 - done & - MONITOR_PID=$! - - # List of test functions to run separately - TESTS=( - "testInsertSortedNewToken()" - "testInsertSortedDuplicateToken(address)" - "testRemoveAndRedeemMaturedTokens()" - ) - - # Run each test separately - for test in "${TESTS[@]}"; do - echo "Running test: $test" - kontrol prove \ - --verbose \ - --debug \ - --include "src%test%kontrol%RepoTokenListInvariantsTest.$test" \ - --config-profile tests \ - 2>&1 | tee -a verification-results/verification.log + - name: Run RepoToken Tests with Memory Management + run: | + mkdir -p verification-results + + # Function to run verification with memory monitoring + run_verification() { + # Start memory monitoring in background + while true; do + free -h >> verification-results/memory-usage.log + sleep 30 + done & + MONITOR_PID=$! - TEST_RESULT=$? - if [ $TEST_RESULT -ne 0 ]; then - echo "Test $test failed with exit code $TEST_RESULT" - return $TEST_RESULT - fi + # List of test functions to run separately + TESTS=( + "testInsertSortedNewToken()" + "testInsertSortedDuplicateToken(address)" + "testRemoveAndRedeemMaturedTokens()" + ) - # Clear caches between tests - sudo sh -c 'echo 3 > /proc/sys/vm/drop_caches' - sleep 10 + # Run each test separately + for test in "${TESTS[@]}"; do + echo "Running test: $test" + kontrol prove \ + --verbose \ + --debug \ + --include "src%test%kontrol%RepoTokenListInvariantsTest.$test" \ + --config-profile tests \ + 2>&1 | tee -a verification-results/verification.log + + TEST_RESULT=$? + if [ $TEST_RESULT -ne 0 ]; then + echo "Test $test failed with exit code $TEST_RESULT" + return $TEST_RESULT + fi + + # Clear caches between tests + sudo sh -c 'echo 3 > /proc/sys/vm/drop_caches' + sleep 10 + done + + # Stop memory monitoring + kill $MONITOR_PID + return 0 + } + + # Clean up function + cleanup() { + echo "Cleaning up..." + # Save debug information + tar czf verification-results/debug-state.tar.gz \ + .build .kontrol out/proofs verification-results \ + 2>/dev/null || true + } + + # Set trap for cleanup + trap cleanup EXIT + + # Run verification with retry logic + MAX_RETRIES=3 + RETRY_COUNT=0 + + while [ $RETRY_COUNT -lt $MAX_RETRIES ]; do + echo "Attempt $((RETRY_COUNT + 1)) of $MAX_RETRIES" + + if run_verification; then + echo "Verification successful!" + exit 0 + else + RETRY_COUNT=$((RETRY_COUNT + 1)) + echo "Verification failed. Exit code: $?" + + if [ $RETRY_COUNT -lt $MAX_RETRIES ]; then + echo "Cleaning up and retrying..." + sudo sh -c 'echo 3 > /proc/sys/vm/drop_caches' + sleep 30 + fi + fi done - # Stop memory monitoring - kill $MONITOR_PID - return 0 - } - - # Clean up function - cleanup() { - echo "Cleaning up..." - # Save debug information - tar czf verification-results/debug-state.tar.gz \ - .build .kontrol out/proofs verification-results \ - 2>/dev/null || true - } - - # Set trap for cleanup - trap cleanup EXIT - - # Run verification with retry logic - MAX_RETRIES=3 - RETRY_COUNT=0 - - while [ $RETRY_COUNT -lt $MAX_RETRIES ]; do - echo "Attempt $((RETRY_COUNT + 1)) of $MAX_RETRIES" + echo "All retry attempts failed" + exit 1 + + - name: Analyze Verification Results + if: always() + run: | + echo "Analyzing verification results..." - if run_verification; then - echo "Verification successful!" - exit 0 - else - RETRY_COUNT=$((RETRY_COUNT + 1)) - echo "Verification failed. Exit code: $?" + if [ -f "verification-results/verification.log" ]; then + echo "Last 50 lines of verification log:" + tail -n 50 verification-results/verification.log - if [ $RETRY_COUNT -lt $MAX_RETRIES ]; then - echo "Cleaning up and retrying..." - sudo sh -c 'echo 3 > /proc/sys/vm/drop_caches' - sleep 30 + echo "Memory usage during verification:" + cat verification-results/memory-usage.log + + if grep -q "Out of memory" verification-results/verification.log; then + echo "Out of memory condition detected" fi fi - done - - echo "All retry attempts failed" - exit 1 - - name: Analyze Verification Results - if: always() - run: | - echo "Analyzing verification results..." - - if [ -f "verification-results/verification.log" ]; then - echo "Last 50 lines of verification log:" - tail -n 50 verification-results/verification.log + - name: Upload Results + if: always() + uses: actions/upload-artifact@v3 + with: + name: repo-token-verification-results + path: | + verification-results/ + out/proofs/ + .build/ + .kontrol/ + retention-days: 5 + term-auction-tests: + needs: setup-verification + runs-on: ubuntu-latest + timeout-minutes: 350 + steps: + - uses: actions/checkout@v4 + with: + fetch-depth: 0 + submodules: recursive + + - name: Install Foundry + uses: foundry-rs/foundry-toolchain@v1 + with: + version: nightly + + - name: Install forge-std and build + run: | + forge install foundry-rs/forge-std --no-commit + forge build --build-info --force + forge remappings > remappings.txt + + - name: Install System Dependencies + run: | + sudo apt-get update + sudo apt-get install -y curl gcc git g++ cmake maven openjdk-11-jdk flex \ + z3 libz3-dev libsecp256k1-dev python3 python3-pip build-essential + + - uses: DeterminateSystems/nix-installer-action@main + with: + extra-conf: | + trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= k-framework.cachix.org-1:jeyMXB2h28gpNRjuVkehg+zLj62ma1RnyyopA/20yFE= k-framework-binary.cachix.org-1:pJedQ8iG19BW3v/DMMmiRVtwRBGO3fyMv2Ws0OpBADs= + substituters = https://cache.nixos.org https://k-framework.cachix.org + + - uses: cachix/cachix-action@v12 + with: + name: k-framework + extraPullNames: k-framework-binary + + - name: Install KUP and Kontrol + env: + REPOSITORY_TOKEN: ${{ secrets.REPOSITORY_TOKEN }} + run: | + git config --global url."https://${REPOSITORY_TOKEN}:x-oauth-basic@github.com/".insteadOf "https://github.com/" + + echo "Installing kup..." + GC_DONT_GC=1 nix profile install github:runtimeverification/kup#kup \ + --option extra-substituters 'https://k-framework.cachix.org' \ + --option extra-trusted-public-keys 'k-framework.cachix.org-1:jeyMXB2h28gpNRjuVkehg+zLj62ma1RnyyopA/20yFE=' \ + --experimental-features 'nix-command flakes' + + export PATH="$HOME/.nix-profile/bin:$PATH" + echo "$HOME/.nix-profile/bin" >> $GITHUB_PATH + + echo "Installing Kontrol..." + GITHUB_TOKEN=$REPOSITORY_TOKEN kup install kontrol + + echo "Verifying Kontrol installation..." + which kontrol || { echo "kontrol not found in PATH"; exit 1; } + kontrol version || { echo "kontrol not working properly"; exit 1; } + + - name: Configure System Resources + run: | + echo "Available memory:" + free -h + + sudo sh -c 'echo 3 > /proc/sys/vm/drop_caches' + + sudo fallocate -l 8G /swapfile + sudo chmod 600 /swapfile + sudo mkswap /swapfile + sudo swapon /swapfile - echo "Memory usage during verification:" - cat verification-results/memory-usage.log + echo "Memory after swap configuration:" + free -h + + - name: Cache Kontrol Build + uses: actions/cache@v3 + with: + path: | + .build + .kontrol + out/proofs + key: kontrol-cache-${{ github.sha }} + restore-keys: | + kontrol-cache- + + - name: Prepare Verification Environment + run: | + # Create necessary directories + mkdir -p .build .kontrol "out/proofs" + chmod -R 755 .build .kontrol "out/proofs" - if grep -q "Out of memory" verification-results/verification.log; then - echo "Out of memory condition detected" + # Clean stale files + rm -rf out/proofs/* + rm -rf out/kompiled + + if [ -d ".build" ] && [ -d ".kontrol" ]; then + echo "Restored Kontrol state from cache" + ls -la .build + ls -la .kontrol + else + echo "No cached state found, initializing..." + kontrol build --verbose fi - fi - - - name: Upload Results - if: always() - uses: actions/upload-artifact@v3 - with: - name: repo-token-verification-results - path: | - verification-results/ - out/proofs/ - .build/ - .kontrol/ - retention-days: 5 -term-auction-tests: - needs: setup-verification - runs-on: ubuntu-latest - timeout-minutes: 350 - steps: - - uses: actions/checkout@v4 - with: - fetch-depth: 0 - submodules: recursive - - - name: Install Foundry - uses: foundry-rs/foundry-toolchain@v1 - with: - version: nightly - - - name: Install forge-std and build - run: | - forge install foundry-rs/forge-std --no-commit - forge build --build-info --force - forge remappings > remappings.txt - - - name: Install System Dependencies - run: | - sudo apt-get update - sudo apt-get install -y curl gcc git g++ cmake maven openjdk-11-jdk flex \ - z3 libz3-dev libsecp256k1-dev python3 python3-pip build-essential - - - uses: DeterminateSystems/nix-installer-action@main - with: - extra-conf: | - trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= k-framework.cachix.org-1:jeyMXB2h28gpNRjuVkehg+zLj62ma1RnyyopA/20yFE= k-framework-binary.cachix.org-1:pJedQ8iG19BW3v/DMMmiRVtwRBGO3fyMv2Ws0OpBADs= - substituters = https://cache.nixos.org https://k-framework.cachix.org - - - uses: cachix/cachix-action@v12 - with: - name: k-framework - extraPullNames: k-framework-binary - - - name: Install KUP and Kontrol - env: - REPOSITORY_TOKEN: ${{ secrets.REPOSITORY_TOKEN }} - run: | - git config --global url."https://${REPOSITORY_TOKEN}:x-oauth-basic@github.com/".insteadOf "https://github.com/" - - echo "Installing kup..." - GC_DONT_GC=1 nix profile install github:runtimeverification/kup#kup \ - --option extra-substituters 'https://k-framework.cachix.org' \ - --option extra-trusted-public-keys 'k-framework.cachix.org-1:jeyMXB2h28gpNRjuVkehg+zLj62ma1RnyyopA/20yFE=' \ - --experimental-features 'nix-command flakes' - - export PATH="$HOME/.nix-profile/bin:$PATH" - echo "$HOME/.nix-profile/bin" >> $GITHUB_PATH - - echo "Installing Kontrol..." - GITHUB_TOKEN=$REPOSITORY_TOKEN kup install kontrol - - echo "Verifying Kontrol installation..." - which kontrol || { echo "kontrol not found in PATH"; exit 1; } - kontrol version || { echo "kontrol not working properly"; exit 1; } - - - name: Configure System Resources - run: | - echo "Available memory:" - free -h - - sudo sh -c 'echo 3 > /proc/sys/vm/drop_caches' - - sudo fallocate -l 8G /swapfile - sudo chmod 600 /swapfile - sudo mkswap /swapfile - sudo swapon /swapfile - - echo "Memory after swap configuration:" - free -h - - name: Cache Kontrol Build - uses: actions/cache@v3 - with: - path: | - .build - .kontrol - out/proofs - key: kontrol-cache-${{ github.sha }} - restore-keys: | - kontrol-cache- - - - name: Prepare Verification Environment - run: | - # Create necessary directories - mkdir -p .build .kontrol "out/proofs" - chmod -R 755 .build .kontrol "out/proofs" - - # Clean stale files - rm -rf out/proofs/* - rm -rf out/kompiled - - if [ -d ".build" ] && [ -d ".kontrol" ]; then - echo "Restored Kontrol state from cache" - ls -la .build - ls -la .kontrol - else - echo "No cached state found, initializing..." - kontrol build --verbose - fi - - - name: Run TermAuction Tests with Memory Management - run: | - mkdir -p verification-results - - # Function to run verification with memory monitoring - run_verification() { - while true; do - free -h >> verification-results/memory-usage.log - sleep 30 - done & - MONITOR_PID=$! - - # List of test functions to run separately - TESTS=( - "testInsertPendingNewOffer(bytes32,address)" - "testInsertPendingDuplicateOffer(bytes32,(address,uint256,address,address),address)" - "testRemoveCompleted(address)" - ) - - # Run each test separately - for test in "${TESTS[@]}"; do - echo "Running test: $test" - kontrol prove \ - --verbose \ - --debug \ - --include "src%test%kontrol%TermAuctionListInvariantsTest.$test" \ - --config-profile tests \ - 2>&1 | tee -a verification-results/verification.log + - name: Run TermAuction Tests with Memory Management + run: | + mkdir -p verification-results + + # Function to run verification with memory monitoring + run_verification() { + while true; do + free -h >> verification-results/memory-usage.log + sleep 30 + done & + MONITOR_PID=$! - TEST_RESULT=$? - if [ $TEST_RESULT -ne 0 ]; then - echo "Test $test failed with exit code $TEST_RESULT" - return $TEST_RESULT - fi + # List of test functions to run separately + TESTS=( + "testInsertPendingNewOffer(bytes32,address)" + "testInsertPendingDuplicateOffer(bytes32,(address,uint256,address,address),address)" + "testRemoveCompleted(address)" + ) - # Clear caches between tests - sudo sh -c 'echo 3 > /proc/sys/vm/drop_caches' - sleep 10 - done + # Run each test separately + for test in "${TESTS[@]}"; do + echo "Running test: $test" + kontrol prove \ + --verbose \ + --debug \ + --include "src%test%kontrol%TermAuctionListInvariantsTest.$test" \ + --config-profile tests \ + 2>&1 | tee -a verification-results/verification.log + + TEST_RESULT=$? + if [ $TEST_RESULT -ne 0 ]; then + echo "Test $test failed with exit code $TEST_RESULT" + return $TEST_RESULT + fi + + # Clear caches between tests + sudo sh -c 'echo 3 > /proc/sys/vm/drop_caches' + sleep 10 + done + + kill $MONITOR_PID + return 0 + } - kill $MONITOR_PID - return 0 - } - - cleanup() { - echo "Cleaning up..." - tar czf verification-results/debug-state.tar.gz \ - .build .kontrol out/proofs verification-results \ - 2>/dev/null || true - } - - trap cleanup EXIT - - MAX_RETRIES=3 - RETRY_COUNT=0 - - while [ $RETRY_COUNT -lt $MAX_RETRIES ]; do - echo "Attempt $((RETRY_COUNT + 1)) of $MAX_RETRIES" + cleanup() { + echo "Cleaning up..." + tar czf verification-results/debug-state.tar.gz \ + .build .kontrol out/proofs verification-results \ + 2>/dev/null || true + } - if run_verification; then - echo "Verification successful!" - exit 0 - else - RETRY_COUNT=$((RETRY_COUNT + 1)) - echo "Verification failed. Exit code: $?" + trap cleanup EXIT + + MAX_RETRIES=3 + RETRY_COUNT=0 + + while [ $RETRY_COUNT -lt $MAX_RETRIES ]; do + echo "Attempt $((RETRY_COUNT + 1)) of $MAX_RETRIES" - if [ $RETRY_COUNT -lt $MAX_RETRIES ]; then - echo "Cleaning up and retrying..." - sudo sh -c 'echo 3 > /proc/sys/vm/drop_caches' - sleep 30 + if run_verification; then + echo "Verification successful!" + exit 0 + else + RETRY_COUNT=$((RETRY_COUNT + 1)) + echo "Verification failed. Exit code: $?" + + if [ $RETRY_COUNT -lt $MAX_RETRIES ]; then + echo "Cleaning up and retrying..." + sudo sh -c 'echo 3 > /proc/sys/vm/drop_caches' + sleep 30 + fi fi - fi - done - - echo "All retry attempts failed" - exit 1 - - - name: Analyze Verification Results - if: always() - run: | - echo "Analyzing verification results..." - - if [ -f "verification-results/verification.log" ]; then - echo "Last 50 lines of verification log:" - tail -n 50 verification-results/verification.log + done - echo "Memory usage during verification:" - cat verification-results/memory-usage.log + echo "All retry attempts failed" + exit 1 + + - name: Analyze Verification Results + if: always() + run: | + echo "Analyzing verification results..." - if grep -q "Out of memory" verification-results/verification.log; then - echo "Out of memory condition detected" + if [ -f "verification-results/verification.log" ]; then + echo "Last 50 lines of verification log:" + tail -n 50 verification-results/verification.log + + echo "Memory usage during verification:" + cat verification-results/memory-usage.log + + if grep -q "Out of memory" verification-results/verification.log; then + echo "Out of memory condition detected" + fi fi - fi - - name: Upload Results - if: always() - uses: actions/upload-artifact@v3 - with: - name: term-auction-verification-results - path: | - verification-results/ - out/proofs/ - .build/ - .kontrol/ - retention-days: 5 + - name: Upload Results + if: always() + uses: actions/upload-artifact@v3 + with: + name: term-auction-verification-results + path: | + verification-results/ + out/proofs/ + .build/ + .kontrol/ + retention-days: 5 results-summary: needs: [setup-verification, repo-token-tests, term-auction-tests] From aebc4667cf951007ff16a55fce64939b723b0f5d Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Sun, 17 Nov 2024 00:10:20 -0500 Subject: [PATCH 61/97] try proofs list --- .github/workflows/ci.yaml | 119 ++++++++++++++------------------------ 1 file changed, 43 insertions(+), 76 deletions(-) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index 2125a464..6b06e548 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -257,13 +257,20 @@ jobs: # Function to run verification with memory monitoring run_verification() { - # Start memory monitoring in background while true; do free -h >> verification-results/memory-usage.log sleep 30 done & MONITOR_PID=$! + # Ensure proofs directory exists and is clean + mkdir -p out/proofs + rm -rf out/proofs/* + + # Build project first + echo "Building Kontrol project..." + kontrol build --verbose + # List of test functions to run separately TESTS=( "testInsertSortedNewToken()" @@ -274,16 +281,30 @@ jobs: # Run each test separately for test in "${TESTS[@]}"; do echo "Running test: $test" + + # Clean proof directory for each test + rm -rf "out/proofs/src%test%kontrol%RepoTokenListInvariantsTest.$test"* + + # Run individual test kontrol prove \ --verbose \ --debug \ --include "src%test%kontrol%RepoTokenListInvariantsTest.$test" \ --config-profile tests \ + --build-dir ./out \ + --proofs-dir ./out/proofs \ 2>&1 | tee -a verification-results/verification.log TEST_RESULT=$? if [ $TEST_RESULT -ne 0 ]; then echo "Test $test failed with exit code $TEST_RESULT" + + # Debug information + echo "Contents of proof directory:" + ls -la out/proofs + echo "Contents of build directory:" + ls -la out + return $TEST_RESULT fi @@ -292,47 +313,9 @@ jobs: sleep 10 done - # Stop memory monitoring kill $MONITOR_PID return 0 } - - # Clean up function - cleanup() { - echo "Cleaning up..." - # Save debug information - tar czf verification-results/debug-state.tar.gz \ - .build .kontrol out/proofs verification-results \ - 2>/dev/null || true - } - - # Set trap for cleanup - trap cleanup EXIT - - # Run verification with retry logic - MAX_RETRIES=3 - RETRY_COUNT=0 - - while [ $RETRY_COUNT -lt $MAX_RETRIES ]; do - echo "Attempt $((RETRY_COUNT + 1)) of $MAX_RETRIES" - - if run_verification; then - echo "Verification successful!" - exit 0 - else - RETRY_COUNT=$((RETRY_COUNT + 1)) - echo "Verification failed. Exit code: $?" - - if [ $RETRY_COUNT -lt $MAX_RETRIES ]; then - echo "Cleaning up and retrying..." - sudo sh -c 'echo 3 > /proc/sys/vm/drop_caches' - sleep 30 - fi - fi - done - - echo "All retry attempts failed" - exit 1 - name: Analyze Verification Results if: always() @@ -471,7 +454,6 @@ jobs: run: | mkdir -p verification-results - # Function to run verification with memory monitoring run_verification() { while true; do free -h >> verification-results/memory-usage.log @@ -479,30 +461,48 @@ jobs: done & MONITOR_PID=$! - # List of test functions to run separately + # Ensure proofs directory exists and is clean + mkdir -p out/proofs + rm -rf out/proofs/* + + # Build project first + echo "Building Kontrol project..." + kontrol build --verbose + TESTS=( "testInsertPendingNewOffer(bytes32,address)" "testInsertPendingDuplicateOffer(bytes32,(address,uint256,address,address),address)" "testRemoveCompleted(address)" ) - # Run each test separately for test in "${TESTS[@]}"; do echo "Running test: $test" + + # Clean proof directory for each test + rm -rf "out/proofs/src%test%kontrol%TermAuctionListInvariantsTest.$test"* + kontrol prove \ --verbose \ --debug \ --include "src%test%kontrol%TermAuctionListInvariantsTest.$test" \ --config-profile tests \ + --build-dir ./out \ + --proofs-dir ./out/proofs \ 2>&1 | tee -a verification-results/verification.log TEST_RESULT=$? if [ $TEST_RESULT -ne 0 ]; then echo "Test $test failed with exit code $TEST_RESULT" + + # Debug information + echo "Contents of proof directory:" + ls -la out/proofs + echo "Contents of build directory:" + ls -la out + return $TEST_RESULT fi - # Clear caches between tests sudo sh -c 'echo 3 > /proc/sys/vm/drop_caches' sleep 10 done @@ -510,39 +510,6 @@ jobs: kill $MONITOR_PID return 0 } - - cleanup() { - echo "Cleaning up..." - tar czf verification-results/debug-state.tar.gz \ - .build .kontrol out/proofs verification-results \ - 2>/dev/null || true - } - - trap cleanup EXIT - - MAX_RETRIES=3 - RETRY_COUNT=0 - - while [ $RETRY_COUNT -lt $MAX_RETRIES ]; do - echo "Attempt $((RETRY_COUNT + 1)) of $MAX_RETRIES" - - if run_verification; then - echo "Verification successful!" - exit 0 - else - RETRY_COUNT=$((RETRY_COUNT + 1)) - echo "Verification failed. Exit code: $?" - - if [ $RETRY_COUNT -lt $MAX_RETRIES ]; then - echo "Cleaning up and retrying..." - sudo sh -c 'echo 3 > /proc/sys/vm/drop_caches' - sleep 30 - fi - fi - done - - echo "All retry attempts failed" - exit 1 - name: Analyze Verification Results if: always() From 31015b7df980d815b8b014ae7cf32fbb95ca8dbb Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Mon, 18 Nov 2024 13:59:26 -0500 Subject: [PATCH 62/97] remove fv for now --- .github/workflows/ci.yaml | 589 +------------------------------------- 1 file changed, 1 insertion(+), 588 deletions(-) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index 6b06e548..80956bb1 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -2,9 +2,6 @@ name: CI on: [push] -env: - NIX_INSTALLABLE_PACKAGE: github:runtimeverification/kup#kup - jobs: foundry-test: runs-on: ubuntu-latest @@ -26,588 +23,4 @@ jobs: - name: Run snapshot without Kontrol tests run: forge snapshot --no-match-path "src/test/kontrol/*" - setup-verification: - needs: foundry-test - runs-on: ubuntu-latest - timeout-minutes: 60 - steps: - - uses: actions/checkout@v4 - with: - fetch-depth: 0 - submodules: recursive - - - name: Install Foundry - uses: foundry-rs/foundry-toolchain@v1 - with: - version: nightly - - - name: Install forge-std and build - run: | - forge install foundry-rs/forge-std --no-commit - forge build --build-info --force - forge remappings > remappings.txt - - - name: Install System Dependencies - run: | - sudo apt-get update - sudo apt-get install -y curl gcc git g++ cmake maven openjdk-11-jdk flex \ - z3 libz3-dev libsecp256k1-dev python3 python3-pip build-essential - - # Install Nix - - uses: DeterminateSystems/nix-installer-action@main - with: - extra-conf: | - trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= k-framework.cachix.org-1:jeyMXB2h28gpNRjuVkehg+zLj62ma1RnyyopA/20yFE= k-framework-binary.cachix.org-1:pJedQ8iG19BW3v/DMMmiRVtwRBGO3fyMv2Ws0OpBADs= - substituters = https://cache.nixos.org https://k-framework.cachix.org - - # Install Cachix - - uses: cachix/cachix-action@v12 - with: - name: k-framework - extraPullNames: k-framework-binary - - - name: Install KUP and Kontrol - env: - REPOSITORY_TOKEN: ${{ secrets.REPOSITORY_TOKEN }} - run: | - git config --global url."https://${REPOSITORY_TOKEN}:x-oauth-basic@github.com/".insteadOf "https://github.com/" - - echo "Installing kup..." - GC_DONT_GC=1 nix profile install github:runtimeverification/kup#kup \ - --option extra-substituters 'https://k-framework.cachix.org' \ - --option extra-trusted-public-keys 'k-framework.cachix.org-1:jeyMXB2h28gpNRjuVkehg+zLj62ma1RnyyopA/20yFE=' \ - --experimental-features 'nix-command flakes' - - export PATH="$HOME/.nix-profile/bin:$PATH" - echo "$HOME/.nix-profile/bin" >> $GITHUB_PATH - - echo "Installing Kontrol..." - GITHUB_TOKEN=$REPOSITORY_TOKEN kup install kontrol - - echo "Verifying Kontrol installation..." - which kontrol || { echo "kontrol not found in PATH"; exit 1; } - kontrol version || { echo "kontrol not working properly"; exit 1; } - - - name: Verify Kontrol Environment - run: | - echo "Checking Kontrol environment..." - - # Check for required directories - for dir in .build .kontrol "out/proofs"; do - if [ ! -d "$dir" ]; then - echo "Creating $dir..." - mkdir -p "$dir" - fi - echo "Contents of $dir:" - ls -la "$dir" - done - - # Test Kontrol functionality - echo "Testing Kontrol..." - kontrol version - kontrol list - - # Check proof directory permissions - echo "Checking permissions..." - stat out/proofs - - # Verify forge build info - echo "Checking forge build..." - test -d out/proofs || echo "out/proofs missing" - forge build --build-info --force - - - name: Cache Kontrol Build - uses: actions/cache@v3 - with: - path: | - .build - .kontrol - out/proofs - key: kontrol-cache-${{ github.sha }} - restore-keys: | - kontrol-cache- - - - name: Run Setup Verification - run: | - mkdir -p verification-results - echo "Building Kontrol project..." - kontrol build --verbose - - echo "Running setup verification..." - kontrol prove --config-profile setup --verbose - - - name: Upload Setup Results - if: always() - uses: actions/upload-artifact@v3 - with: - name: setup-verification-results - path: | - verification-results/ - retention-days: 5 - repo-token-tests: - needs: setup-verification - runs-on: ubuntu-latest - timeout-minutes: 350 - steps: - - uses: actions/checkout@v4 - with: - fetch-depth: 0 - submodules: recursive - - - name: Install Foundry - uses: foundry-rs/foundry-toolchain@v1 - with: - version: nightly - - - name: Install forge-std and build - run: | - forge install foundry-rs/forge-std --no-commit - forge build --build-info --force - forge remappings > remappings.txt - - - name: Install System Dependencies - run: | - sudo apt-get update - sudo apt-get install -y curl gcc git g++ cmake maven openjdk-11-jdk flex \ - z3 libz3-dev libsecp256k1-dev python3 python3-pip build-essential - - - uses: DeterminateSystems/nix-installer-action@main - with: - extra-conf: | - trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= k-framework.cachix.org-1:jeyMXB2h28gpNRjuVkehg+zLj62ma1RnyyopA/20yFE= k-framework-binary.cachix.org-1:pJedQ8iG19BW3v/DMMmiRVtwRBGO3fyMv2Ws0OpBADs= - substituters = https://cache.nixos.org https://k-framework.cachix.org - - - uses: cachix/cachix-action@v12 - with: - name: k-framework - extraPullNames: k-framework-binary - - - name: Install KUP and Kontrol - env: - REPOSITORY_TOKEN: ${{ secrets.REPOSITORY_TOKEN }} - run: | - git config --global url."https://${REPOSITORY_TOKEN}:x-oauth-basic@github.com/".insteadOf "https://github.com/" - - echo "Installing kup..." - GC_DONT_GC=1 nix profile install github:runtimeverification/kup#kup \ - --option extra-substituters 'https://k-framework.cachix.org' \ - --option extra-trusted-public-keys 'k-framework.cachix.org-1:jeyMXB2h28gpNRjuVkehg+zLj62ma1RnyyopA/20yFE=' \ - --experimental-features 'nix-command flakes' - - export PATH="$HOME/.nix-profile/bin:$PATH" - echo "$HOME/.nix-profile/bin" >> $GITHUB_PATH - - echo "Installing Kontrol..." - GITHUB_TOKEN=$REPOSITORY_TOKEN kup install kontrol - - echo "Verifying Kontrol installation..." - which kontrol || { echo "kontrol not found in PATH"; exit 1; } - kontrol version || { echo "kontrol not working properly"; exit 1; } - - - name: Configure System Resources - run: | - # Show available memory - echo "Available memory:" - free -h - - # Clear system cache - sudo sh -c 'echo 3 > /proc/sys/vm/drop_caches' - - # Configure swap - sudo fallocate -l 8G /swapfile - sudo chmod 600 /swapfile - sudo mkswap /swapfile - sudo swapon /swapfile - - echo "Memory after swap configuration:" - free -h - - - name: Cache Kontrol Build - uses: actions/cache@v3 - with: - path: | - .build - .kontrol - out/proofs - key: kontrol-cache-${{ github.sha }} - restore-keys: | - kontrol-cache- - - - name: Prepare Verification Environment - run: | - mkdir -p .build .kontrol "out/proofs" - chmod -R 755 .build .kontrol "out/proofs" - rm -rf out/proofs/* - - # Clean any previous build artifacts - rm -rf out/kompiled - - if [ -d ".build" ] && [ -d ".kontrol" ]; then - echo "Restored Kontrol state from cache" - ls -la .build - ls -la .kontrol - else - echo "No cached state found, initializing..." - kontrol build --verbose - fi - - - name: Run RepoToken Tests with Memory Management - run: | - mkdir -p verification-results - - # Function to run verification with memory monitoring - run_verification() { - while true; do - free -h >> verification-results/memory-usage.log - sleep 30 - done & - MONITOR_PID=$! - - # Ensure proofs directory exists and is clean - mkdir -p out/proofs - rm -rf out/proofs/* - - # Build project first - echo "Building Kontrol project..." - kontrol build --verbose - - # List of test functions to run separately - TESTS=( - "testInsertSortedNewToken()" - "testInsertSortedDuplicateToken(address)" - "testRemoveAndRedeemMaturedTokens()" - ) - - # Run each test separately - for test in "${TESTS[@]}"; do - echo "Running test: $test" - - # Clean proof directory for each test - rm -rf "out/proofs/src%test%kontrol%RepoTokenListInvariantsTest.$test"* - - # Run individual test - kontrol prove \ - --verbose \ - --debug \ - --include "src%test%kontrol%RepoTokenListInvariantsTest.$test" \ - --config-profile tests \ - --build-dir ./out \ - --proofs-dir ./out/proofs \ - 2>&1 | tee -a verification-results/verification.log - - TEST_RESULT=$? - if [ $TEST_RESULT -ne 0 ]; then - echo "Test $test failed with exit code $TEST_RESULT" - - # Debug information - echo "Contents of proof directory:" - ls -la out/proofs - echo "Contents of build directory:" - ls -la out - - return $TEST_RESULT - fi - - # Clear caches between tests - sudo sh -c 'echo 3 > /proc/sys/vm/drop_caches' - sleep 10 - done - - kill $MONITOR_PID - return 0 - } - - - name: Analyze Verification Results - if: always() - run: | - echo "Analyzing verification results..." - - if [ -f "verification-results/verification.log" ]; then - echo "Last 50 lines of verification log:" - tail -n 50 verification-results/verification.log - - echo "Memory usage during verification:" - cat verification-results/memory-usage.log - - if grep -q "Out of memory" verification-results/verification.log; then - echo "Out of memory condition detected" - fi - fi - - - name: Upload Results - if: always() - uses: actions/upload-artifact@v3 - with: - name: repo-token-verification-results - path: | - verification-results/ - out/proofs/ - .build/ - .kontrol/ - retention-days: 5 - term-auction-tests: - needs: setup-verification - runs-on: ubuntu-latest - timeout-minutes: 350 - steps: - - uses: actions/checkout@v4 - with: - fetch-depth: 0 - submodules: recursive - - - name: Install Foundry - uses: foundry-rs/foundry-toolchain@v1 - with: - version: nightly - - - name: Install forge-std and build - run: | - forge install foundry-rs/forge-std --no-commit - forge build --build-info --force - forge remappings > remappings.txt - - - name: Install System Dependencies - run: | - sudo apt-get update - sudo apt-get install -y curl gcc git g++ cmake maven openjdk-11-jdk flex \ - z3 libz3-dev libsecp256k1-dev python3 python3-pip build-essential - - - uses: DeterminateSystems/nix-installer-action@main - with: - extra-conf: | - trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= k-framework.cachix.org-1:jeyMXB2h28gpNRjuVkehg+zLj62ma1RnyyopA/20yFE= k-framework-binary.cachix.org-1:pJedQ8iG19BW3v/DMMmiRVtwRBGO3fyMv2Ws0OpBADs= - substituters = https://cache.nixos.org https://k-framework.cachix.org - - - uses: cachix/cachix-action@v12 - with: - name: k-framework - extraPullNames: k-framework-binary - - - name: Install KUP and Kontrol - env: - REPOSITORY_TOKEN: ${{ secrets.REPOSITORY_TOKEN }} - run: | - git config --global url."https://${REPOSITORY_TOKEN}:x-oauth-basic@github.com/".insteadOf "https://github.com/" - - echo "Installing kup..." - GC_DONT_GC=1 nix profile install github:runtimeverification/kup#kup \ - --option extra-substituters 'https://k-framework.cachix.org' \ - --option extra-trusted-public-keys 'k-framework.cachix.org-1:jeyMXB2h28gpNRjuVkehg+zLj62ma1RnyyopA/20yFE=' \ - --experimental-features 'nix-command flakes' - - export PATH="$HOME/.nix-profile/bin:$PATH" - echo "$HOME/.nix-profile/bin" >> $GITHUB_PATH - - echo "Installing Kontrol..." - GITHUB_TOKEN=$REPOSITORY_TOKEN kup install kontrol - - echo "Verifying Kontrol installation..." - which kontrol || { echo "kontrol not found in PATH"; exit 1; } - kontrol version || { echo "kontrol not working properly"; exit 1; } - - - name: Configure System Resources - run: | - echo "Available memory:" - free -h - - sudo sh -c 'echo 3 > /proc/sys/vm/drop_caches' - - sudo fallocate -l 8G /swapfile - sudo chmod 600 /swapfile - sudo mkswap /swapfile - sudo swapon /swapfile - - echo "Memory after swap configuration:" - free -h - - - name: Cache Kontrol Build - uses: actions/cache@v3 - with: - path: | - .build - .kontrol - out/proofs - key: kontrol-cache-${{ github.sha }} - restore-keys: | - kontrol-cache- - - - name: Prepare Verification Environment - run: | - # Create necessary directories - mkdir -p .build .kontrol "out/proofs" - chmod -R 755 .build .kontrol "out/proofs" - - # Clean stale files - rm -rf out/proofs/* - rm -rf out/kompiled - - if [ -d ".build" ] && [ -d ".kontrol" ]; then - echo "Restored Kontrol state from cache" - ls -la .build - ls -la .kontrol - else - echo "No cached state found, initializing..." - kontrol build --verbose - fi - - - name: Run TermAuction Tests with Memory Management - run: | - mkdir -p verification-results - - run_verification() { - while true; do - free -h >> verification-results/memory-usage.log - sleep 30 - done & - MONITOR_PID=$! - - # Ensure proofs directory exists and is clean - mkdir -p out/proofs - rm -rf out/proofs/* - - # Build project first - echo "Building Kontrol project..." - kontrol build --verbose - - TESTS=( - "testInsertPendingNewOffer(bytes32,address)" - "testInsertPendingDuplicateOffer(bytes32,(address,uint256,address,address),address)" - "testRemoveCompleted(address)" - ) - - for test in "${TESTS[@]}"; do - echo "Running test: $test" - - # Clean proof directory for each test - rm -rf "out/proofs/src%test%kontrol%TermAuctionListInvariantsTest.$test"* - - kontrol prove \ - --verbose \ - --debug \ - --include "src%test%kontrol%TermAuctionListInvariantsTest.$test" \ - --config-profile tests \ - --build-dir ./out \ - --proofs-dir ./out/proofs \ - 2>&1 | tee -a verification-results/verification.log - - TEST_RESULT=$? - if [ $TEST_RESULT -ne 0 ]; then - echo "Test $test failed with exit code $TEST_RESULT" - - # Debug information - echo "Contents of proof directory:" - ls -la out/proofs - echo "Contents of build directory:" - ls -la out - - return $TEST_RESULT - fi - - sudo sh -c 'echo 3 > /proc/sys/vm/drop_caches' - sleep 10 - done - - kill $MONITOR_PID - return 0 - } - - - name: Analyze Verification Results - if: always() - run: | - echo "Analyzing verification results..." - - if [ -f "verification-results/verification.log" ]; then - echo "Last 50 lines of verification log:" - tail -n 50 verification-results/verification.log - - echo "Memory usage during verification:" - cat verification-results/memory-usage.log - - if grep -q "Out of memory" verification-results/verification.log; then - echo "Out of memory condition detected" - fi - fi - - - name: Upload Results - if: always() - uses: actions/upload-artifact@v3 - with: - name: term-auction-verification-results - path: | - verification-results/ - out/proofs/ - .build/ - .kontrol/ - retention-days: 5 - - results-summary: - needs: [setup-verification, repo-token-tests, term-auction-tests] - runs-on: ubuntu-latest - if: always() - steps: - - name: Download All Results - uses: actions/download-artifact@v3 - with: - path: all-results - - - name: Generate Summary - run: | - echo "# Kontrol Verification Summary" > summary.md - echo "Generated at: $(date)" >> summary.md - echo "" >> summary.md - - # Function to process results - process_results() { - local dir="$1" - local section="$2" - - echo "## $section" >> summary.md - echo "\`\`\`" >> summary.md - - if [ -d "$dir" ]; then - # Check verification log - if [ -f "$dir/verification.log" ]; then - echo "### Verification Output" >> summary.md - tail -n 50 "$dir/verification.log" >> summary.md - fi - - # Check memory usage - if [ -f "$dir/memory-usage.log" ]; then - echo "### Memory Usage" >> summary.md - tail -n 10 "$dir/memory-usage.log" >> summary.md - fi - - # Check for specific errors - if grep -q "Out of memory" "$dir"/*.log 2>/dev/null; then - echo "⚠️ Out of Memory conditions detected" >> summary.md - fi - - # Add any successful proofs - if grep -q "PROOF PASSED" "$dir"/*.log 2>/dev/null; then - echo "✅ Successful proofs detected" >> summary.md - grep "PROOF PASSED" "$dir"/*.log >> summary.md - fi - else - echo "No results found for $section" >> summary.md - fi - - echo "\`\`\`" >> summary.md - echo "" >> summary.md - } - - process_results "all-results/setup-verification-results" "Setup Verification" - process_results "all-results/repo-token-verification-results" "RepoToken Tests" - process_results "all-results/term-auction-verification-results" "TermAuction Tests" - - # Add overall status - echo "## Overall Status" >> summary.md - echo "- Setup: $(test -d all-results/setup-verification-results && echo '✅' || echo '❌')" >> summary.md - echo "- RepoToken: $(test -d all-results/repo-token-verification-results && echo '✅' || echo '❌')" >> summary.md - echo "- TermAuction: $(test -d all-results/term-auction-verification-results && echo '✅' || echo '❌')" >> summary.md - - - name: Upload Summary - uses: actions/upload-artifact@v3 - with: - name: verification-summary - path: summary.md - retention-days: 5 \ No newline at end of file + \ No newline at end of file From dc9dda98f7055cbd9111fba8c5d55a84555b9002 Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Mon, 18 Nov 2024 14:06:30 -0500 Subject: [PATCH 63/97] use governance factory as management address --- .github/workflows/deploy-sepolia-strategy.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/deploy-sepolia-strategy.yaml b/.github/workflows/deploy-sepolia-strategy.yaml index b4a86d9f..5d5500ad 100644 --- a/.github/workflows/deploy-sepolia-strategy.yaml +++ b/.github/workflows/deploy-sepolia-strategy.yaml @@ -67,6 +67,6 @@ jobs: ADMIN_ADDRESS: ${{ vars.ADMIN_ADDRESS }} DEVOPS_ADDRESS: ${{ vars.DEVOPS_ADDRESS }} GOVERNOR_ROLE_ADDRESS: ${{ github.event.inputs.governorRoleAddress }} - STRATEGY_MANAGEMENT_ADDRESS: ${{ github.event.inputs.strategyManagementAddress }} + STRATEGY_MANAGEMENT_ADDRESS: ${{ vars.GOVERNANCE_FACTORY }} NEW_REQUIRED_RESERVE_RATIO: ${{ github.event.inputs.requiredReserveRatio }} \ No newline at end of file From 1a39f6b87fa342f5b2a76f8937c1fa39d93feb7a Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Mon, 18 Nov 2024 15:38:48 -0500 Subject: [PATCH 64/97] governance deploy script --- .../workflows/deploy-sepolia-governance.yaml | 42 +++++++++++++++++++ script/DeployGovernance.s.sol | 33 +++++++++++++++ 2 files changed, 75 insertions(+) create mode 100644 .github/workflows/deploy-sepolia-governance.yaml create mode 100644 script/DeployGovernance.s.sol diff --git a/.github/workflows/deploy-sepolia-governance.yaml b/.github/workflows/deploy-sepolia-governance.yaml new file mode 100644 index 00000000..a7715f2c --- /dev/null +++ b/.github/workflows/deploy-sepolia-governance.yaml @@ -0,0 +1,42 @@ +name: "[sepolia-deploy] deploy governance for strategy" +on: + workflow_dispatch: + inputs: + proposer: + description: 'Proposer address' + required: true + default: '0x' + strategy: + description: 'Strategy Address' + required: true + default: '0x' + governorRoleAddress: + description: 'Governor role address' + required: true + default: '0x' + +jobs: + deploy: + runs-on: ubuntu-latest + environment: + name: sepolia + url: https://term-finance.github.io/yearn-v3-term-vault/ + steps: + - uses: actions/checkout@master + with: + fetch-depth: 0 + submodules: recursive + - uses: foundry-rs/foundry-toolchain@v1 + - run: forge install + - run: forge build + - run: forge tree + - run: forge script script/DeployGovernance.s.sol:DeployGovernance --rpc-url $RPC_URL --broadcast --gas-price 500000000000 --verify --verbosity 4 + env: + RPC_URL: ${{ secrets.RPC_URL }} + PRIVATE_KEY: ${{ secrets.GOVERNANCE_DEPLOYER_KEY }} + ETHERSCAN_API_KEY: ${{ secrets.ETHERSCAN_API_KEY }} + PROPOSER: ${{ github.event.inputs.proposer }} + STRATEGY: ${{ github.event.inputs.strategy }} + GOVERNOR: ${{ github.event.inputs.governorRoleAddress }} + + \ No newline at end of file diff --git a/script/DeployGovernance.s.sol b/script/DeployGovernance.s.sol new file mode 100644 index 00000000..45b3768f --- /dev/null +++ b/script/DeployGovernance.s.sol @@ -0,0 +1,33 @@ +import "forge-std/Script.sol"; + +interface TermVaultGovernanceFactory { + function deploySafe( + address proposer, + address strategy, + address governor, + uint256 saltNonce + ) external; +} + +contract DeployGovernance is Script { + + function run() external { + uint256 deployerPK = vm.envUint("PRIVATE_KEY"); + + // Set up the RPC URL (optional if you're using the default foundry config) + string memory rpcUrl = vm.envString("RPC_URL"); + + vm.startBroadcast(deployerPK); + + TermVaultGovernanceFactory factory = TermVaultGovernanceFactory(vm.envAddress("GOVERNANCE_FACTORY")); + address proposer = vm.envAddress("PROPOSER"); + address strategy = vm.envAddress("STRATEGY"); + address governor = vm.envAddress("GOVERNOR"); + uint256 saltNonce = block.number; + + factory.deploySafe(proposer, strategy, governor, saltNonce); + + vm.stopBroadcast(); + } + +} \ No newline at end of file From 50a6082eee74b8a1342bcf840e931bba196a510e Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Mon, 18 Nov 2024 15:42:20 -0500 Subject: [PATCH 65/97] remove governor and management from deploy script for strategies --- .github/workflows/deploy-sepolia-strategy.yaml | 10 +--------- 1 file changed, 1 insertion(+), 9 deletions(-) diff --git a/.github/workflows/deploy-sepolia-strategy.yaml b/.github/workflows/deploy-sepolia-strategy.yaml index 5d5500ad..1fcb0134 100644 --- a/.github/workflows/deploy-sepolia-strategy.yaml +++ b/.github/workflows/deploy-sepolia-strategy.yaml @@ -10,14 +10,6 @@ on: description: 'Yearn strategy name' required: true default: '0x' - governorRoleAddress: - description: 'Governor role address' - required: true - default: '0x' - strategyManagementAddress: - description: 'Strategy management address' - required: false - default: '0x' discountRateMarkup: description: 'Discount rate markup' required: false @@ -66,7 +58,7 @@ jobs: REPOTOKEN_CONCENTRATION_LIMIT: ${{ github.event.inputs.repoTokenConcentrationLimit }} ADMIN_ADDRESS: ${{ vars.ADMIN_ADDRESS }} DEVOPS_ADDRESS: ${{ vars.DEVOPS_ADDRESS }} - GOVERNOR_ROLE_ADDRESS: ${{ github.event.inputs.governorRoleAddress }} + GOVERNOR_ROLE_ADDRESS: ${{ vars.GOVERNANCE_FACTORY }} STRATEGY_MANAGEMENT_ADDRESS: ${{ vars.GOVERNANCE_FACTORY }} NEW_REQUIRED_RESERVE_RATIO: ${{ github.event.inputs.requiredReserveRatio }} \ No newline at end of file From af79fe360b953cb2582c7ff31a632f374162232d Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Mon, 18 Nov 2024 15:51:52 -0500 Subject: [PATCH 66/97] governance added to deploy script --- .github/workflows/deploy-sepolia-governance.yaml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/.github/workflows/deploy-sepolia-governance.yaml b/.github/workflows/deploy-sepolia-governance.yaml index a7715f2c..f38099b5 100644 --- a/.github/workflows/deploy-sepolia-governance.yaml +++ b/.github/workflows/deploy-sepolia-governance.yaml @@ -38,5 +38,8 @@ jobs: PROPOSER: ${{ github.event.inputs.proposer }} STRATEGY: ${{ github.event.inputs.strategy }} GOVERNOR: ${{ github.event.inputs.governorRoleAddress }} + GOVERNANCE_FACTORY: ${{ vars.GOVERNANCE_FACTORY }} + + \ No newline at end of file From 991636df0f24ad4b24d5ad8b85cd8012bf309e0a Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Mon, 18 Nov 2024 15:56:41 -0500 Subject: [PATCH 67/97] governance added to deploy script --- .github/workflows/deploy-sepolia-strategy.yaml | 6 +++++- script/Strategy.s.sol | 2 +- 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/.github/workflows/deploy-sepolia-strategy.yaml b/.github/workflows/deploy-sepolia-strategy.yaml index 1fcb0134..9c428ff8 100644 --- a/.github/workflows/deploy-sepolia-strategy.yaml +++ b/.github/workflows/deploy-sepolia-strategy.yaml @@ -10,6 +10,10 @@ on: description: 'Yearn strategy name' required: true default: '0x' + governorRoleAddress: + description: 'Governor role address' + required: true + default: '0x' discountRateMarkup: description: 'Discount rate markup' required: false @@ -58,7 +62,7 @@ jobs: REPOTOKEN_CONCENTRATION_LIMIT: ${{ github.event.inputs.repoTokenConcentrationLimit }} ADMIN_ADDRESS: ${{ vars.ADMIN_ADDRESS }} DEVOPS_ADDRESS: ${{ vars.DEVOPS_ADDRESS }} - GOVERNOR_ROLE_ADDRESS: ${{ vars.GOVERNANCE_FACTORY }} + GOVERNOR_ROLE_ADDRESS: ${{ github.event.inputs.governorRoleAddress }} STRATEGY_MANAGEMENT_ADDRESS: ${{ vars.GOVERNANCE_FACTORY }} NEW_REQUIRED_RESERVE_RATIO: ${{ github.event.inputs.requiredReserveRatio }} \ No newline at end of file diff --git a/script/Strategy.s.sol b/script/Strategy.s.sol index 3d6e7c85..e7da879c 100644 --- a/script/Strategy.s.sol +++ b/script/Strategy.s.sol @@ -137,6 +137,7 @@ contract DeployStrategy is Script { // Retrieve environment variables string memory name = vm.envString("STRATEGY_NAME"); address strategyManagement = vm.envAddress("STRATEGY_MANAGEMENT_ADDRESS"); + address newGovernor = vm.envAddress("NEW_GOVERNOR"); bool isTest = vm.envBool("IS_TEST"); @@ -156,7 +157,6 @@ contract DeployStrategy is Script { console.log("set pending management"); console.log(strategyManagement); - if (isTest) { eventEmitter.pairVaultContract(address(strategy)); console.log("paired strategy contract with event emitter"); From 41a0fd85dd35e2e2277f30ebcc82c74dd1e58cfa Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Mon, 18 Nov 2024 15:59:35 -0500 Subject: [PATCH 68/97] remove governor role --- script/Strategy.s.sol | 1 - 1 file changed, 1 deletion(-) diff --git a/script/Strategy.s.sol b/script/Strategy.s.sol index e7da879c..f7664243 100644 --- a/script/Strategy.s.sol +++ b/script/Strategy.s.sol @@ -137,7 +137,6 @@ contract DeployStrategy is Script { // Retrieve environment variables string memory name = vm.envString("STRATEGY_NAME"); address strategyManagement = vm.envAddress("STRATEGY_MANAGEMENT_ADDRESS"); - address newGovernor = vm.envAddress("NEW_GOVERNOR"); bool isTest = vm.envBool("IS_TEST"); From ca4d27fd4a41776a9ec1b309c11c0119550c0679 Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Mon, 18 Nov 2024 16:09:43 -0500 Subject: [PATCH 69/97] governance added to deploy script --- .github/workflows/deploy-sepolia-strategy.yaml | 2 +- script/Strategy.s.sol | 12 ++++++++---- 2 files changed, 9 insertions(+), 5 deletions(-) diff --git a/.github/workflows/deploy-sepolia-strategy.yaml b/.github/workflows/deploy-sepolia-strategy.yaml index 9c428ff8..e2df2375 100644 --- a/.github/workflows/deploy-sepolia-strategy.yaml +++ b/.github/workflows/deploy-sepolia-strategy.yaml @@ -62,7 +62,7 @@ jobs: REPOTOKEN_CONCENTRATION_LIMIT: ${{ github.event.inputs.repoTokenConcentrationLimit }} ADMIN_ADDRESS: ${{ vars.ADMIN_ADDRESS }} DEVOPS_ADDRESS: ${{ vars.DEVOPS_ADDRESS }} - GOVERNOR_ROLE_ADDRESS: ${{ github.event.inputs.governorRoleAddress }} + GOVERNOR_ROLE_ADDRESS: ${{ vars.GOVERNANCE_FACTORY }} STRATEGY_MANAGEMENT_ADDRESS: ${{ vars.GOVERNANCE_FACTORY }} NEW_REQUIRED_RESERVE_RATIO: ${{ github.event.inputs.requiredReserveRatio }} \ No newline at end of file diff --git a/script/Strategy.s.sol b/script/Strategy.s.sol index f7664243..82a8ed23 100644 --- a/script/Strategy.s.sol +++ b/script/Strategy.s.sol @@ -137,12 +137,15 @@ contract DeployStrategy is Script { // Retrieve environment variables string memory name = vm.envString("STRATEGY_NAME"); address strategyManagement = vm.envAddress("STRATEGY_MANAGEMENT_ADDRESS"); + address governorRoleAddress = vm.envAddress("GOVERNOR_ROLE_ADDRESS"); bool isTest = vm.envBool("IS_TEST"); TermVaultEventEmitter eventEmitter = _deployEventEmitter(); - Strategy.StrategyParams memory params = buildStrategyParams(address(eventEmitter)); + address deployer = vm.addr(deployerPK); + + Strategy.StrategyParams memory params = buildStrategyParams(address(eventEmitter), deployer); Strategy strategy = new Strategy( name, @@ -156,6 +159,8 @@ contract DeployStrategy is Script { console.log("set pending management"); console.log(strategyManagement); + strategy.setPendingGovernor(governorRoleAddress); + if (isTest) { eventEmitter.pairVaultContract(address(strategy)); console.log("paired strategy contract with event emitter"); @@ -164,11 +169,10 @@ contract DeployStrategy is Script { vm.stopBroadcast(); } - function buildStrategyParams(address eventEmitter) internal returns(Strategy.StrategyParams memory) { + function buildStrategyParams(address eventEmitter, address deployer) internal returns(Strategy.StrategyParams memory) { address asset = vm.envAddress("ASSET_ADDRESS"); address yearnVaultAddress = vm.envAddress("YEARN_VAULT_ADDRESS"); address discountRateAdapterAddress = vm.envAddress("DISCOUNT_RATE_ADAPTER_ADDRESS"); - address governorRoleAddress = vm.envAddress("GOVERNOR_ROLE_ADDRESS"); address termController = vm.envAddress("TERM_CONTROLLER_ADDRESS"); uint256 discountRateMarkup = vm.envUint("DISCOUNT_RATE_MARKUP"); uint256 timeToMaturityThreshold = vm.envUint("TIME_TO_MATURITY_THRESHOLD"); @@ -182,7 +186,7 @@ contract DeployStrategy is Script { yearnVaultAddress, discountRateAdapterAddress, address(eventEmitter), - governorRoleAddress, + deployer, termController, repoTokenConcentrationLimit, timeToMaturityThreshold, From ca32eafd12fb7f028a9004aa10a013c186f89b07 Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Mon, 18 Nov 2024 16:10:50 -0500 Subject: [PATCH 70/97] governance input removed from deploy script --- .github/workflows/deploy-sepolia-strategy.yaml | 4 ---- 1 file changed, 4 deletions(-) diff --git a/.github/workflows/deploy-sepolia-strategy.yaml b/.github/workflows/deploy-sepolia-strategy.yaml index e2df2375..1fcb0134 100644 --- a/.github/workflows/deploy-sepolia-strategy.yaml +++ b/.github/workflows/deploy-sepolia-strategy.yaml @@ -10,10 +10,6 @@ on: description: 'Yearn strategy name' required: true default: '0x' - governorRoleAddress: - description: 'Governor role address' - required: true - default: '0x' discountRateMarkup: description: 'Discount rate markup' required: false From f5bea30fafb06d89d22d28eec33e032e3735b458 Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Mon, 18 Nov 2024 16:40:50 -0500 Subject: [PATCH 71/97] governance input removed from deploy script --- .github/workflows/deploy-sepolia-strategy.yaml | 1 + script/DeployGovernance.s.sol | 4 ++++ script/Strategy.s.sol | 5 ++--- 3 files changed, 7 insertions(+), 3 deletions(-) diff --git a/.github/workflows/deploy-sepolia-strategy.yaml b/.github/workflows/deploy-sepolia-strategy.yaml index 1fcb0134..f547f812 100644 --- a/.github/workflows/deploy-sepolia-strategy.yaml +++ b/.github/workflows/deploy-sepolia-strategy.yaml @@ -46,6 +46,7 @@ jobs: env: RPC_URL: ${{ secrets.RPC_URL }} PRIVATE_KEY: ${{ secrets.PRIVATE_KEY }} + GOVERNOR_DEPLOYER_KEY: ${{ secrets.GOVERNANCE_DEPLOYER_KEY }} ETHERSCAN_API_KEY: ${{ secrets.ETHERSCAN_API_KEY }} ASSET_ADDRESS: ${{ github.event.inputs.asset }} YEARN_VAULT_ADDRESS: ${{ vars.YEARN_VAULT_ADDRESS }} diff --git a/script/DeployGovernance.s.sol b/script/DeployGovernance.s.sol index 45b3768f..d6f2521f 100644 --- a/script/DeployGovernance.s.sol +++ b/script/DeployGovernance.s.sol @@ -1,4 +1,5 @@ import "forge-std/Script.sol"; +import "../src/Strategy.sol"; interface TermVaultGovernanceFactory { function deploySafe( @@ -25,6 +26,9 @@ contract DeployGovernance is Script { address governor = vm.envAddress("GOVERNOR"); uint256 saltNonce = block.number; + Strategy strategy = Strategy(strategy); + strategy.setPendingGovernor(governor); + factory.deploySafe(proposer, strategy, governor, saltNonce); vm.stopBroadcast(); diff --git a/script/Strategy.s.sol b/script/Strategy.s.sol index 82a8ed23..c8f99d53 100644 --- a/script/Strategy.s.sol +++ b/script/Strategy.s.sol @@ -128,6 +128,7 @@ contract DeployStrategy is Script { function run() external { uint256 deployerPK = vm.envUint("PRIVATE_KEY"); + uint256 governorDeployerPK = vm.envUint("GOVERNOR_DEPLOYER_KEY"); // Set up the RPC URL (optional if you're using the default foundry config) string memory rpcUrl = vm.envString("RPC_URL"); @@ -143,7 +144,7 @@ contract DeployStrategy is Script { TermVaultEventEmitter eventEmitter = _deployEventEmitter(); - address deployer = vm.addr(deployerPK); + address deployer = vm.addr(governorDeployerPK); Strategy.StrategyParams memory params = buildStrategyParams(address(eventEmitter), deployer); @@ -159,8 +160,6 @@ contract DeployStrategy is Script { console.log("set pending management"); console.log(strategyManagement); - strategy.setPendingGovernor(governorRoleAddress); - if (isTest) { eventEmitter.pairVaultContract(address(strategy)); console.log("paired strategy contract with event emitter"); From 217bd18e7d586a815070804345d74d7310a46ac4 Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Mon, 18 Nov 2024 16:44:52 -0500 Subject: [PATCH 72/97] governance input removed from deploy script --- script/DeployGovernance.s.sol | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/script/DeployGovernance.s.sol b/script/DeployGovernance.s.sol index d6f2521f..0b46f0d1 100644 --- a/script/DeployGovernance.s.sol +++ b/script/DeployGovernance.s.sol @@ -26,8 +26,8 @@ contract DeployGovernance is Script { address governor = vm.envAddress("GOVERNOR"); uint256 saltNonce = block.number; - Strategy strategy = Strategy(strategy); - strategy.setPendingGovernor(governor); + Strategy strategyContract = Strategy(strategy); + strategyContract.setPendingGovernor(governor); factory.deploySafe(proposer, strategy, governor, saltNonce); From 7d979bd50bc2b5dfe7d0d2bdd9e2d3efee1f8dea Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Mon, 18 Nov 2024 17:16:02 -0500 Subject: [PATCH 73/97] accept governor then set pending in gov deploy --- script/DeployGovernance.s.sol | 1 + 1 file changed, 1 insertion(+) diff --git a/script/DeployGovernance.s.sol b/script/DeployGovernance.s.sol index 0b46f0d1..d0504fff 100644 --- a/script/DeployGovernance.s.sol +++ b/script/DeployGovernance.s.sol @@ -27,6 +27,7 @@ contract DeployGovernance is Script { uint256 saltNonce = block.number; Strategy strategyContract = Strategy(strategy); + strategyContract.acceptGovernor(); strategyContract.setPendingGovernor(governor); factory.deploySafe(proposer, strategy, governor, saltNonce); From eb0b29952a7ac3e817e0d600d80b3f44602eebec Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Mon, 18 Nov 2024 17:22:07 -0500 Subject: [PATCH 74/97] fix deploy governance set governor to factory --- script/DeployGovernance.s.sol | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/script/DeployGovernance.s.sol b/script/DeployGovernance.s.sol index d0504fff..20350fb3 100644 --- a/script/DeployGovernance.s.sol +++ b/script/DeployGovernance.s.sol @@ -27,8 +27,7 @@ contract DeployGovernance is Script { uint256 saltNonce = block.number; Strategy strategyContract = Strategy(strategy); - strategyContract.acceptGovernor(); - strategyContract.setPendingGovernor(governor); + strategyContract.setPendingGovernor(factory); factory.deploySafe(proposer, strategy, governor, saltNonce); From 6b19639ca97430b3c906a6bb4ac25d6bc9578e29 Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Mon, 18 Nov 2024 17:25:42 -0500 Subject: [PATCH 75/97] set governor to factory and set manager to input --- .github/workflows/deploy-sepolia-strategy.yaml | 6 +++++- script/DeployGovernance.s.sol | 3 --- script/Strategy.s.sol | 8 +++----- 3 files changed, 8 insertions(+), 9 deletions(-) diff --git a/.github/workflows/deploy-sepolia-strategy.yaml b/.github/workflows/deploy-sepolia-strategy.yaml index f547f812..daa9bcde 100644 --- a/.github/workflows/deploy-sepolia-strategy.yaml +++ b/.github/workflows/deploy-sepolia-strategy.yaml @@ -10,6 +10,10 @@ on: description: 'Yearn strategy name' required: true default: '0x' + strategyManagementAddress: + description: 'Strategy management address' + required: true + default: '0x' discountRateMarkup: description: 'Discount rate markup' required: false @@ -60,6 +64,6 @@ jobs: ADMIN_ADDRESS: ${{ vars.ADMIN_ADDRESS }} DEVOPS_ADDRESS: ${{ vars.DEVOPS_ADDRESS }} GOVERNOR_ROLE_ADDRESS: ${{ vars.GOVERNANCE_FACTORY }} - STRATEGY_MANAGEMENT_ADDRESS: ${{ vars.GOVERNANCE_FACTORY }} + STRATEGY_MANAGEMENT_ADDRESS: ${{ github.events.strategyManagementAddress }} NEW_REQUIRED_RESERVE_RATIO: ${{ github.event.inputs.requiredReserveRatio }} \ No newline at end of file diff --git a/script/DeployGovernance.s.sol b/script/DeployGovernance.s.sol index 20350fb3..3066be8b 100644 --- a/script/DeployGovernance.s.sol +++ b/script/DeployGovernance.s.sol @@ -26,9 +26,6 @@ contract DeployGovernance is Script { address governor = vm.envAddress("GOVERNOR"); uint256 saltNonce = block.number; - Strategy strategyContract = Strategy(strategy); - strategyContract.setPendingGovernor(factory); - factory.deploySafe(proposer, strategy, governor, saltNonce); vm.stopBroadcast(); diff --git a/script/Strategy.s.sol b/script/Strategy.s.sol index c8f99d53..9e318551 100644 --- a/script/Strategy.s.sol +++ b/script/Strategy.s.sol @@ -138,14 +138,11 @@ contract DeployStrategy is Script { // Retrieve environment variables string memory name = vm.envString("STRATEGY_NAME"); address strategyManagement = vm.envAddress("STRATEGY_MANAGEMENT_ADDRESS"); - address governorRoleAddress = vm.envAddress("GOVERNOR_ROLE_ADDRESS"); bool isTest = vm.envBool("IS_TEST"); TermVaultEventEmitter eventEmitter = _deployEventEmitter(); - address deployer = vm.addr(governorDeployerPK); - Strategy.StrategyParams memory params = buildStrategyParams(address(eventEmitter), deployer); Strategy strategy = new Strategy( @@ -168,12 +165,13 @@ contract DeployStrategy is Script { vm.stopBroadcast(); } - function buildStrategyParams(address eventEmitter, address deployer) internal returns(Strategy.StrategyParams memory) { + function buildStrategyParams(address eventEmitter) internal returns(Strategy.StrategyParams memory) { address asset = vm.envAddress("ASSET_ADDRESS"); address yearnVaultAddress = vm.envAddress("YEARN_VAULT_ADDRESS"); address discountRateAdapterAddress = vm.envAddress("DISCOUNT_RATE_ADAPTER_ADDRESS"); address termController = vm.envAddress("TERM_CONTROLLER_ADDRESS"); uint256 discountRateMarkup = vm.envUint("DISCOUNT_RATE_MARKUP"); + address governorRoleAddress = vm.envAddress("GOVERNOR_ROLE_ADDRESS"); uint256 timeToMaturityThreshold = vm.envUint("TIME_TO_MATURITY_THRESHOLD"); uint256 repoTokenConcentrationLimit = vm.envUint("REPOTOKEN_CONCENTRATION_LIMIT"); uint256 newRequiredReserveRatio = vm.envUint("NEW_REQUIRED_RESERVE_RATIO"); @@ -185,7 +183,7 @@ contract DeployStrategy is Script { yearnVaultAddress, discountRateAdapterAddress, address(eventEmitter), - deployer, + governorRoleAddress, termController, repoTokenConcentrationLimit, timeToMaturityThreshold, From f1f2add7571071750b0744df60a02112ffca1b5b Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Mon, 18 Nov 2024 17:28:09 -0500 Subject: [PATCH 76/97] set governor to factory and set manager to input --- script/Strategy.s.sol | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/script/Strategy.s.sol b/script/Strategy.s.sol index 9e318551..12ca6015 100644 --- a/script/Strategy.s.sol +++ b/script/Strategy.s.sol @@ -143,7 +143,7 @@ contract DeployStrategy is Script { TermVaultEventEmitter eventEmitter = _deployEventEmitter(); - Strategy.StrategyParams memory params = buildStrategyParams(address(eventEmitter), deployer); + Strategy.StrategyParams memory params = buildStrategyParams(address(eventEmitter)); Strategy strategy = new Strategy( name, From c5a39856161fa33d425c2686e130a848ad0f4c5e Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Mon, 18 Nov 2024 17:32:00 -0500 Subject: [PATCH 77/97] fix strategy management input --- .github/workflows/deploy-sepolia-strategy.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/deploy-sepolia-strategy.yaml b/.github/workflows/deploy-sepolia-strategy.yaml index daa9bcde..24b694ef 100644 --- a/.github/workflows/deploy-sepolia-strategy.yaml +++ b/.github/workflows/deploy-sepolia-strategy.yaml @@ -64,6 +64,6 @@ jobs: ADMIN_ADDRESS: ${{ vars.ADMIN_ADDRESS }} DEVOPS_ADDRESS: ${{ vars.DEVOPS_ADDRESS }} GOVERNOR_ROLE_ADDRESS: ${{ vars.GOVERNANCE_FACTORY }} - STRATEGY_MANAGEMENT_ADDRESS: ${{ github.events.strategyManagementAddress }} + STRATEGY_MANAGEMENT_ADDRESS: ${{ github.event.inputs.strategyManagementAddress }} NEW_REQUIRED_RESERVE_RATIO: ${{ github.event.inputs.requiredReserveRatio }} \ No newline at end of file From 5678fd48ebbc17b95551235b59b3a390aacf22a9 Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Mon, 18 Nov 2024 22:30:42 -0500 Subject: [PATCH 78/97] remove salt nonce from governance deploy --- script/DeployGovernance.s.sol | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/script/DeployGovernance.s.sol b/script/DeployGovernance.s.sol index 3066be8b..b21ee799 100644 --- a/script/DeployGovernance.s.sol +++ b/script/DeployGovernance.s.sol @@ -24,9 +24,8 @@ contract DeployGovernance is Script { address proposer = vm.envAddress("PROPOSER"); address strategy = vm.envAddress("STRATEGY"); address governor = vm.envAddress("GOVERNOR"); - uint256 saltNonce = block.number; - factory.deploySafe(proposer, strategy, governor, saltNonce); + factory.deploySafe(proposer, strategy, governor); vm.stopBroadcast(); } From da3eb4db8c68de6a88c5b9637dbf6ae131e98a6e Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Mon, 18 Nov 2024 22:33:15 -0500 Subject: [PATCH 79/97] remove salt nonce from governance deploy --- script/DeployGovernance.s.sol | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/script/DeployGovernance.s.sol b/script/DeployGovernance.s.sol index b21ee799..b055829d 100644 --- a/script/DeployGovernance.s.sol +++ b/script/DeployGovernance.s.sol @@ -5,8 +5,7 @@ interface TermVaultGovernanceFactory { function deploySafe( address proposer, address strategy, - address governor, - uint256 saltNonce + address governor ) external; } From 99f16d6d039d60e7493d65482f72a607eedd0ed1 Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Mon, 18 Nov 2024 22:42:21 -0500 Subject: [PATCH 80/97] remove salt nonce from governance deploy --- .github/workflows/deploy-sepolia-governance.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/deploy-sepolia-governance.yaml b/.github/workflows/deploy-sepolia-governance.yaml index f38099b5..34658478 100644 --- a/.github/workflows/deploy-sepolia-governance.yaml +++ b/.github/workflows/deploy-sepolia-governance.yaml @@ -30,7 +30,7 @@ jobs: - run: forge install - run: forge build - run: forge tree - - run: forge script script/DeployGovernance.s.sol:DeployGovernance --rpc-url $RPC_URL --broadcast --gas-price 500000000000 --verify --verbosity 4 + - run: forge script script/DeployGovernance.s.sol:DeployGovernance --rpc-url $RPC_URL --broadcast --gas-price 500000000000 --skip-simulation --verify --verbosity 4 env: RPC_URL: ${{ secrets.RPC_URL }} PRIVATE_KEY: ${{ secrets.GOVERNANCE_DEPLOYER_KEY }} From a4d7d3b2155c69ea1c313c974d95178a71b0fe26 Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Mon, 18 Nov 2024 22:46:58 -0500 Subject: [PATCH 81/97] force tx thru --- .github/workflows/deploy-sepolia-governance.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/deploy-sepolia-governance.yaml b/.github/workflows/deploy-sepolia-governance.yaml index 34658478..f7334369 100644 --- a/.github/workflows/deploy-sepolia-governance.yaml +++ b/.github/workflows/deploy-sepolia-governance.yaml @@ -30,7 +30,7 @@ jobs: - run: forge install - run: forge build - run: forge tree - - run: forge script script/DeployGovernance.s.sol:DeployGovernance --rpc-url $RPC_URL --broadcast --gas-price 500000000000 --skip-simulation --verify --verbosity 4 + - run: forge script script/DeployGovernance.s.sol:DeployGovernance --rpc-url $RPC_URL --broadcast --gas-price 500000000000 --skip-simulation --force --verify --verbosity 4 env: RPC_URL: ${{ secrets.RPC_URL }} PRIVATE_KEY: ${{ secrets.GOVERNANCE_DEPLOYER_KEY }} From e7325406b4ddabf1e645201e2168365f3cf90408 Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Mon, 18 Nov 2024 22:52:34 -0500 Subject: [PATCH 82/97] force tx thru --- .github/workflows/deploy-sepolia-governance.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/deploy-sepolia-governance.yaml b/.github/workflows/deploy-sepolia-governance.yaml index f7334369..189f27c6 100644 --- a/.github/workflows/deploy-sepolia-governance.yaml +++ b/.github/workflows/deploy-sepolia-governance.yaml @@ -30,7 +30,7 @@ jobs: - run: forge install - run: forge build - run: forge tree - - run: forge script script/DeployGovernance.s.sol:DeployGovernance --rpc-url $RPC_URL --broadcast --gas-price 500000000000 --skip-simulation --force --verify --verbosity 4 + - run: forge script script/DeployGovernance.s.sol:DeployGovernance --rpc-url $RPC_URL --broadcast --gas-price 500000000000 --skip-simulation --force --legacy --no-auto-detect --verify --verbosity 4 env: RPC_URL: ${{ secrets.RPC_URL }} PRIVATE_KEY: ${{ secrets.GOVERNANCE_DEPLOYER_KEY }} From 3708d3bffe09b90ce42cfdae18fb27e5673179db Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Mon, 18 Nov 2024 22:59:26 -0500 Subject: [PATCH 83/97] force tx thru --- .github/workflows/deploy-sepolia-governance.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/deploy-sepolia-governance.yaml b/.github/workflows/deploy-sepolia-governance.yaml index 189f27c6..e719fa45 100644 --- a/.github/workflows/deploy-sepolia-governance.yaml +++ b/.github/workflows/deploy-sepolia-governance.yaml @@ -30,7 +30,7 @@ jobs: - run: forge install - run: forge build - run: forge tree - - run: forge script script/DeployGovernance.s.sol:DeployGovernance --rpc-url $RPC_URL --broadcast --gas-price 500000000000 --skip-simulation --force --legacy --no-auto-detect --verify --verbosity 4 + - run: forge script script/DeployGovernance.s.sol:DeployGovernance --rpc-url $RPC_URL --broadcast --gas-price 500000000000 --verify --verbosity 4 env: RPC_URL: ${{ secrets.RPC_URL }} PRIVATE_KEY: ${{ secrets.GOVERNANCE_DEPLOYER_KEY }} From 2fbb1a58560f4c28e7bdb948ff0c518317aef2c5 Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Mon, 18 Nov 2024 23:01:31 -0500 Subject: [PATCH 84/97] force tx thru --- script/DeployGovernance.s.sol | 2 ++ 1 file changed, 2 insertions(+) diff --git a/script/DeployGovernance.s.sol b/script/DeployGovernance.s.sol index b055829d..ec34aee2 100644 --- a/script/DeployGovernance.s.sol +++ b/script/DeployGovernance.s.sol @@ -1,3 +1,5 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.18; import "forge-std/Script.sol"; import "../src/Strategy.sol"; From 63afb1d18d474c828b6e1bfc64f025609a4e3ae9 Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Mon, 18 Nov 2024 23:09:25 -0500 Subject: [PATCH 85/97] force tx thru --- foundry.toml | 1 + 1 file changed, 1 insertion(+) diff --git a/foundry.toml b/foundry.toml index d6ff1518..7d7cf7f1 100644 --- a/foundry.toml +++ b/foundry.toml @@ -3,6 +3,7 @@ src = 'src' out = 'out' libs = ['lib'] solc = "0.8.23" +evm_version = "shanghai" remappings = [ "@openzeppelin/contracts-upgradeable/=lib/openzeppelin-contracts-upgradeable/", From 6908e241d984d681860768f556da6474c789b185 Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Mon, 18 Nov 2024 23:14:27 -0500 Subject: [PATCH 86/97] force tx thru --- foundry.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/foundry.toml b/foundry.toml index 7d7cf7f1..984c28da 100644 --- a/foundry.toml +++ b/foundry.toml @@ -1,9 +1,9 @@ [profile.default] +evm_version = 'shanghai' src = 'src' out = 'out' libs = ['lib'] solc = "0.8.23" -evm_version = "shanghai" remappings = [ "@openzeppelin/contracts-upgradeable/=lib/openzeppelin-contracts-upgradeable/", From c3dfeb988c7b332d2a5479af91941bd53b4566b5 Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Wed, 20 Nov 2024 14:30:02 -0500 Subject: [PATCH 87/97] set collateral min ratios in deploy strategy --- .../workflows/deploy-sepolia-strategy.yaml | 10 ++++++++ script/Strategy.s.sol | 23 +++++++++++++++---- 2 files changed, 28 insertions(+), 5 deletions(-) diff --git a/.github/workflows/deploy-sepolia-strategy.yaml b/.github/workflows/deploy-sepolia-strategy.yaml index 24b694ef..864e326a 100644 --- a/.github/workflows/deploy-sepolia-strategy.yaml +++ b/.github/workflows/deploy-sepolia-strategy.yaml @@ -30,6 +30,14 @@ on: description: 'Required reserve ratio' required: false default: '0.01' + collateralTokens: + description: 'Collateral tokens comma separated' + required: false + default: '0x' + minCollateralRatios: + description: 'Minimum collateral ratio comma separated' + required: false + default: '0.01' jobs: deploy: @@ -66,4 +74,6 @@ jobs: GOVERNOR_ROLE_ADDRESS: ${{ vars.GOVERNANCE_FACTORY }} STRATEGY_MANAGEMENT_ADDRESS: ${{ github.event.inputs.strategyManagementAddress }} NEW_REQUIRED_RESERVE_RATIO: ${{ github.event.inputs.requiredReserveRatio }} + COLLATERAL_TOKENS: ${{ github.event.inputs.collateralTokens }} + MIN_COLLATERAL_RATIOS: ${{ github.event.inputs.minCollateralRatios }} \ No newline at end of file diff --git a/script/Strategy.s.sol b/script/Strategy.s.sol index 12ca6015..4e1dbce3 100644 --- a/script/Strategy.s.sol +++ b/script/Strategy.s.sol @@ -128,7 +128,6 @@ contract DeployStrategy is Script { function run() external { uint256 deployerPK = vm.envUint("PRIVATE_KEY"); - uint256 governorDeployerPK = vm.envUint("GOVERNOR_DEPLOYER_KEY"); // Set up the RPC URL (optional if you're using the default foundry config) string memory rpcUrl = vm.envString("RPC_URL"); @@ -138,18 +137,29 @@ contract DeployStrategy is Script { // Retrieve environment variables string memory name = vm.envString("STRATEGY_NAME"); address strategyManagement = vm.envAddress("STRATEGY_MANAGEMENT_ADDRESS"); + address[] memory collateralTokens = stringToAddressArray(vm.envString("COLLATERAL_TOKEN_ADDRESSES")); + uint256[] memory minCollateralRatios = stringToUintArray(vm.envString("MIN_COLLATERAL_RATIO")); + address governorRoleAddress = vm.envAddress("GOVERNOR_ROLE_ADDRESS"); + bool isTest = vm.envBool("IS_TEST"); TermVaultEventEmitter eventEmitter = _deployEventEmitter(); - Strategy.StrategyParams memory params = buildStrategyParams(address(eventEmitter)); + address deployer = vm.addr(deployerPK); + + Strategy.StrategyParams memory params = buildStrategyParams(address(eventEmitter), deployer); Strategy strategy = new Strategy( name, params ); + for (uint256 i = 0; i < collateralTokens.length; i++) { + strategy.setCollateralTokenParams(collateralTokens[i], minCollateralRatios[i]); + } + + console.log("deployed strategy contract to"); console.log(address(strategy)); @@ -157,6 +167,10 @@ contract DeployStrategy is Script { console.log("set pending management"); console.log(strategyManagement); + strategy.setPendingGovernor(governorRoleAddress); + console.log("set pending governor"); + console.log(governorRoleAddress); + if (isTest) { eventEmitter.pairVaultContract(address(strategy)); console.log("paired strategy contract with event emitter"); @@ -165,13 +179,12 @@ contract DeployStrategy is Script { vm.stopBroadcast(); } - function buildStrategyParams(address eventEmitter) internal returns(Strategy.StrategyParams memory) { + function buildStrategyParams(address eventEmitter, address deployer) internal returns(Strategy.StrategyParams memory) { address asset = vm.envAddress("ASSET_ADDRESS"); address yearnVaultAddress = vm.envAddress("YEARN_VAULT_ADDRESS"); address discountRateAdapterAddress = vm.envAddress("DISCOUNT_RATE_ADAPTER_ADDRESS"); address termController = vm.envAddress("TERM_CONTROLLER_ADDRESS"); uint256 discountRateMarkup = vm.envUint("DISCOUNT_RATE_MARKUP"); - address governorRoleAddress = vm.envAddress("GOVERNOR_ROLE_ADDRESS"); uint256 timeToMaturityThreshold = vm.envUint("TIME_TO_MATURITY_THRESHOLD"); uint256 repoTokenConcentrationLimit = vm.envUint("REPOTOKEN_CONCENTRATION_LIMIT"); uint256 newRequiredReserveRatio = vm.envUint("NEW_REQUIRED_RESERVE_RATIO"); @@ -183,7 +196,7 @@ contract DeployStrategy is Script { yearnVaultAddress, discountRateAdapterAddress, address(eventEmitter), - governorRoleAddress, + deployer, termController, repoTokenConcentrationLimit, timeToMaturityThreshold, From 5a72418fb32c94f6d630bf04ab10c48157bf35ea Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Wed, 20 Nov 2024 15:04:12 -0500 Subject: [PATCH 88/97] deploy governance with optional governor vaults --- .../workflows/deploy-sepolia-governance.yaml | 5 ++ script/DeployGovernance.s.sol | 89 ++++++++++++++++++- 2 files changed, 92 insertions(+), 2 deletions(-) diff --git a/.github/workflows/deploy-sepolia-governance.yaml b/.github/workflows/deploy-sepolia-governance.yaml index e719fa45..35b3d573 100644 --- a/.github/workflows/deploy-sepolia-governance.yaml +++ b/.github/workflows/deploy-sepolia-governance.yaml @@ -14,6 +14,10 @@ on: description: 'Governor role address' required: true default: '0x' + governorVaults: + description: 'Governor vaults as comma separated' + required: false + default: '' jobs: deploy: @@ -38,6 +42,7 @@ jobs: PROPOSER: ${{ github.event.inputs.proposer }} STRATEGY: ${{ github.event.inputs.strategy }} GOVERNOR: ${{ github.event.inputs.governorRoleAddress }} + GOVERNOR_VAULTS: ${{ github.event.inputs.governorVaults }} GOVERNANCE_FACTORY: ${{ vars.GOVERNANCE_FACTORY }} diff --git a/script/DeployGovernance.s.sol b/script/DeployGovernance.s.sol index ec34aee2..41101470 100644 --- a/script/DeployGovernance.s.sol +++ b/script/DeployGovernance.s.sol @@ -7,11 +7,95 @@ interface TermVaultGovernanceFactory { function deploySafe( address proposer, address strategy, - address governor + address governor, + address[] calldata vaultGovernors ) external; } contract DeployGovernance is Script { + /** + * @dev Converts a comma-separated string of addresses to an array of addresses. + * @param _input A string containing comma-separated addresses. + * @return addressArray An array of addresses parsed from the input string. + */ + function stringToAddressArray(string memory _input) public pure returns (address[] memory) { + // Step 1: Split the input string by commas + string[] memory parts = splitString(_input, ","); + + // Step 2: Convert each part to an address + address[] memory addressArray = new address[](parts.length); + for (uint256 i = 0; i < parts.length; i++) { + addressArray[i] = parseAddress(parts[i]); + } + + return addressArray; + } + + + /** + * @dev Helper function to split a string by a delimiter + * @param _str The input string + * @param _delimiter The delimiter to split by + * @return An array of substrings + */ + function splitString(string memory _str, string memory _delimiter) internal pure returns (string[] memory) { + bytes memory strBytes = bytes(_str); + bytes memory delimiterBytes = bytes(_delimiter); + uint256 partsCount = 1; + + // Count the parts to split the string + for (uint256 i = 0; i < strBytes.length - 1; i++) { + if (strBytes[i] == delimiterBytes[0]) { + partsCount++; + } + } + + string[] memory parts = new string[](partsCount); + uint256 partIndex = 0; + bytes memory part; + + for (uint256 i = 0; i < strBytes.length; i++) { + if (strBytes[i] == delimiterBytes[0]) { + parts[partIndex] = string(part); + part = ""; + partIndex++; + } else { + part = abi.encodePacked(part, strBytes[i]); + } + } + + // Add the last part + parts[partIndex] = string(part); + + return parts; + } + + /** + * @dev Helper function to parse a string and convert it to an address + * @param _str The string representation of an address + * @return The address parsed from the input string + */ + function parseAddress(string memory _str) internal pure returns (address) { + bytes memory tmp = bytes(_str); + require(tmp.length == 42, "Invalid address length"); // Must be 42 characters long (0x + 40 hex chars) + + uint160 addr = 0; + for (uint256 i = 2; i < 42; i++) { + uint160 b = uint160(uint8(tmp[i])); + + if (b >= 48 && b <= 57) { // 0-9 + addr = addr * 16 + (b - 48); + } else if (b >= 65 && b <= 70) { // A-F + addr = addr * 16 + (b - 55); + } else if (b >= 97 && b <= 102) { // a-f + addr = addr * 16 + (b - 87); + } else { + revert("Invalid address character"); + } + } + + return address(addr); + } function run() external { uint256 deployerPK = vm.envUint("PRIVATE_KEY"); @@ -25,8 +109,9 @@ contract DeployGovernance is Script { address proposer = vm.envAddress("PROPOSER"); address strategy = vm.envAddress("STRATEGY"); address governor = vm.envAddress("GOVERNOR"); + address[] memory vaultGovernors = stringToAddressArray(vm.envString("VAULT_GOVERNORS")); - factory.deploySafe(proposer, strategy, governor); + factory.deploySafe(proposer, strategy, governor, vaultGovernors); vm.stopBroadcast(); } From f70d6d9f18b1067381fc36e52f2516da65266b2c Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Wed, 20 Nov 2024 15:16:58 -0500 Subject: [PATCH 89/97] collateral addresses in strategy deploy --- .github/workflows/deploy-sepolia-strategy.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/deploy-sepolia-strategy.yaml b/.github/workflows/deploy-sepolia-strategy.yaml index 864e326a..1328e57d 100644 --- a/.github/workflows/deploy-sepolia-strategy.yaml +++ b/.github/workflows/deploy-sepolia-strategy.yaml @@ -74,6 +74,6 @@ jobs: GOVERNOR_ROLE_ADDRESS: ${{ vars.GOVERNANCE_FACTORY }} STRATEGY_MANAGEMENT_ADDRESS: ${{ github.event.inputs.strategyManagementAddress }} NEW_REQUIRED_RESERVE_RATIO: ${{ github.event.inputs.requiredReserveRatio }} - COLLATERAL_TOKENS: ${{ github.event.inputs.collateralTokens }} + COLLATERAL_TOKEN_ADDRESSES: ${{ github.event.inputs.collateralTokens }} MIN_COLLATERAL_RATIOS: ${{ github.event.inputs.minCollateralRatios }} \ No newline at end of file From 55d05aadb601ef37ee4d46c05fa762ed6123480d Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Wed, 20 Nov 2024 15:20:10 -0500 Subject: [PATCH 90/97] collateral addresses in strategy deploy --- script/Strategy.s.sol | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/script/Strategy.s.sol b/script/Strategy.s.sol index 4e1dbce3..c96d5aab 100644 --- a/script/Strategy.s.sol +++ b/script/Strategy.s.sol @@ -138,7 +138,7 @@ contract DeployStrategy is Script { string memory name = vm.envString("STRATEGY_NAME"); address strategyManagement = vm.envAddress("STRATEGY_MANAGEMENT_ADDRESS"); address[] memory collateralTokens = stringToAddressArray(vm.envString("COLLATERAL_TOKEN_ADDRESSES")); - uint256[] memory minCollateralRatios = stringToUintArray(vm.envString("MIN_COLLATERAL_RATIO")); + uint256[] memory minCollateralRatios = stringToUintArray(vm.envString("MIN_COLLATERAL_RATIOS")); address governorRoleAddress = vm.envAddress("GOVERNOR_ROLE_ADDRESS"); bool isTest = vm.envBool("IS_TEST"); From cb53b941a8a10e53a89571b4391ccfe844bf33bf Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Wed, 20 Nov 2024 15:25:09 -0500 Subject: [PATCH 91/97] collateral addresses in strategy deploy --- script/Strategy.s.sol | 17 ++++++++--------- 1 file changed, 8 insertions(+), 9 deletions(-) diff --git a/script/Strategy.s.sol b/script/Strategy.s.sol index c96d5aab..47fd133e 100644 --- a/script/Strategy.s.sol +++ b/script/Strategy.s.sol @@ -155,11 +155,6 @@ contract DeployStrategy is Script { params ); - for (uint256 i = 0; i < collateralTokens.length; i++) { - strategy.setCollateralTokenParams(collateralTokens[i], minCollateralRatios[i]); - } - - console.log("deployed strategy contract to"); console.log(address(strategy)); @@ -167,14 +162,18 @@ contract DeployStrategy is Script { console.log("set pending management"); console.log(strategyManagement); - strategy.setPendingGovernor(governorRoleAddress); - console.log("set pending governor"); - console.log(governorRoleAddress); - if (isTest) { eventEmitter.pairVaultContract(address(strategy)); console.log("paired strategy contract with event emitter"); } + + for (uint256 i = 0; i < collateralTokens.length; i++) { + strategy.setCollateralTokenParams(collateralTokens[i], minCollateralRatios[i]); + } + + strategy.setPendingGovernor(governorRoleAddress); + console.log("set pending governor"); + console.log(governorRoleAddress); vm.stopBroadcast(); } From 4c2970b3622f1dd8e06ecbc0b8ac3a6523152a29 Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Wed, 20 Nov 2024 15:47:11 -0500 Subject: [PATCH 92/97] optional governor vaults for deploy governance: --- .github/workflows/deploy-sepolia-governance.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/deploy-sepolia-governance.yaml b/.github/workflows/deploy-sepolia-governance.yaml index 35b3d573..11ec0be5 100644 --- a/.github/workflows/deploy-sepolia-governance.yaml +++ b/.github/workflows/deploy-sepolia-governance.yaml @@ -42,7 +42,7 @@ jobs: PROPOSER: ${{ github.event.inputs.proposer }} STRATEGY: ${{ github.event.inputs.strategy }} GOVERNOR: ${{ github.event.inputs.governorRoleAddress }} - GOVERNOR_VAULTS: ${{ github.event.inputs.governorVaults }} + VAULT_GOVERNORS: ${{ github.event.inputs.governorVaults }} GOVERNANCE_FACTORY: ${{ vars.GOVERNANCE_FACTORY }} From f27da69f4bbbbffa8c144e6d41b1d4553aea7488 Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Wed, 20 Nov 2024 15:50:44 -0500 Subject: [PATCH 93/97] optional governor vaults for deploy governance: --- .github/workflows/deploy-sepolia-governance.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/deploy-sepolia-governance.yaml b/.github/workflows/deploy-sepolia-governance.yaml index 11ec0be5..19b9b71e 100644 --- a/.github/workflows/deploy-sepolia-governance.yaml +++ b/.github/workflows/deploy-sepolia-governance.yaml @@ -17,7 +17,7 @@ on: governorVaults: description: 'Governor vaults as comma separated' required: false - default: '' + default: ' ' jobs: deploy: From 1f96813c200e90233e69151146a7162f95b07dfb Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Wed, 20 Nov 2024 15:58:46 -0500 Subject: [PATCH 94/97] optional governor vaults for deploy governance: --- .github/workflows/deploy-sepolia-governance.yaml | 2 +- script/DeployGovernance.s.sol | 3 +++ script/Strategy.s.sol | 6 ++++++ 3 files changed, 10 insertions(+), 1 deletion(-) diff --git a/.github/workflows/deploy-sepolia-governance.yaml b/.github/workflows/deploy-sepolia-governance.yaml index 19b9b71e..11ec0be5 100644 --- a/.github/workflows/deploy-sepolia-governance.yaml +++ b/.github/workflows/deploy-sepolia-governance.yaml @@ -17,7 +17,7 @@ on: governorVaults: description: 'Governor vaults as comma separated' required: false - default: ' ' + default: '' jobs: deploy: diff --git a/script/DeployGovernance.s.sol b/script/DeployGovernance.s.sol index 41101470..2fc34c9f 100644 --- a/script/DeployGovernance.s.sol +++ b/script/DeployGovernance.s.sol @@ -19,6 +19,9 @@ contract DeployGovernance is Script { * @return addressArray An array of addresses parsed from the input string. */ function stringToAddressArray(string memory _input) public pure returns (address[] memory) { + if (_input == "") { + return new address[](0); + } // Step 1: Split the input string by commas string[] memory parts = splitString(_input, ","); diff --git a/script/Strategy.s.sol b/script/Strategy.s.sol index 47fd133e..8113798d 100644 --- a/script/Strategy.s.sol +++ b/script/Strategy.s.sol @@ -14,6 +14,9 @@ contract DeployStrategy is Script { * @return addressArray An array of addresses parsed from the input string. */ function stringToAddressArray(string memory _input) public pure returns (address[] memory) { + if (_input == "") { + return new address[](0); + } // Step 1: Split the input string by commas string[] memory parts = splitString(_input, ","); @@ -32,6 +35,9 @@ contract DeployStrategy is Script { * @return uintArray An array of uint256 parsed from the input string. */ function stringToUintArray(string memory _input) public pure returns (uint256[] memory) { + if (_input == "") { + return new uint256[](0); + } // Step 1: Split the input string by commas string[] memory parts = splitString(_input, ","); From acbad35bf3305875230827f07bc914ea647f4831 Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Wed, 20 Nov 2024 16:08:58 -0500 Subject: [PATCH 95/97] optional governor vaults for deploy governance: --- script/DeployGovernance.s.sol | 3 ++- script/Strategy.s.sol | 6 ++++-- 2 files changed, 6 insertions(+), 3 deletions(-) diff --git a/script/DeployGovernance.s.sol b/script/DeployGovernance.s.sol index 2fc34c9f..3a83580f 100644 --- a/script/DeployGovernance.s.sol +++ b/script/DeployGovernance.s.sol @@ -19,7 +19,8 @@ contract DeployGovernance is Script { * @return addressArray An array of addresses parsed from the input string. */ function stringToAddressArray(string memory _input) public pure returns (address[] memory) { - if (_input == "") { + // Check if the input string is empty + if (bytes(_input).length == 0) { return new address[](0); } // Step 1: Split the input string by commas diff --git a/script/Strategy.s.sol b/script/Strategy.s.sol index 8113798d..054289f1 100644 --- a/script/Strategy.s.sol +++ b/script/Strategy.s.sol @@ -14,7 +14,8 @@ contract DeployStrategy is Script { * @return addressArray An array of addresses parsed from the input string. */ function stringToAddressArray(string memory _input) public pure returns (address[] memory) { - if (_input == "") { + // Check if the input string is empty + if (bytes(_input).length == 0) { return new address[](0); } // Step 1: Split the input string by commas @@ -35,7 +36,8 @@ contract DeployStrategy is Script { * @return uintArray An array of uint256 parsed from the input string. */ function stringToUintArray(string memory _input) public pure returns (uint256[] memory) { - if (_input == "") { + // Check if the input string is empty + if (bytes(_input).length == 0) { return new uint256[](0); } // Step 1: Split the input string by commas From 9c684d8621106ae42b7cdedbb189f1942aac5774 Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Wed, 20 Nov 2024 20:31:26 -0500 Subject: [PATCH 96/97] new governor is always zero emit --- src/Strategy.sol | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Strategy.sol b/src/Strategy.sol index e77682bd..6364ab43 100644 --- a/src/Strategy.sol +++ b/src/Strategy.sol @@ -162,8 +162,8 @@ contract Strategy is BaseStrategy, Pausable, AccessControl { _revokeRole(GOVERNOR_ROLE, strategyState.governorAddress); _grantRole(GOVERNOR_ROLE, pendingGovernor); strategyState.governorAddress = pendingGovernor; - pendingGovernor = address(0); TERM_VAULT_EVENT_EMITTER.emitNewGovernor(pendingGovernor); + pendingGovernor = address(0); } /** From 51e7032aebe7f8b28b6388fbbb1aaae5e998f2fe Mon Sep 17 00:00:00 2001 From: aazhou1 Date: Thu, 21 Nov 2024 12:56:57 -0500 Subject: [PATCH 97/97] set profit max unlock time for strategy deploy --- .github/workflows/deploy-sepolia-strategy.yaml | 5 +++++ script/Strategy.s.sol | 4 ++++ 2 files changed, 9 insertions(+) diff --git a/.github/workflows/deploy-sepolia-strategy.yaml b/.github/workflows/deploy-sepolia-strategy.yaml index 1328e57d..849adb30 100644 --- a/.github/workflows/deploy-sepolia-strategy.yaml +++ b/.github/workflows/deploy-sepolia-strategy.yaml @@ -30,6 +30,10 @@ on: description: 'Required reserve ratio' required: false default: '0.01' + profitMaxUnlock: + description: 'Profit max unlock time' + required: false + default: '0' collateralTokens: description: 'Collateral tokens comma separated' required: false @@ -76,4 +80,5 @@ jobs: NEW_REQUIRED_RESERVE_RATIO: ${{ github.event.inputs.requiredReserveRatio }} COLLATERAL_TOKEN_ADDRESSES: ${{ github.event.inputs.collateralTokens }} MIN_COLLATERAL_RATIOS: ${{ github.event.inputs.minCollateralRatios }} + PROFIT_MAX_UNLOCK_TIME: ${{ github.event.inputs.profitMaxUnlock }} \ No newline at end of file diff --git a/script/Strategy.s.sol b/script/Strategy.s.sol index 054289f1..56eba271 100644 --- a/script/Strategy.s.sol +++ b/script/Strategy.s.sol @@ -148,6 +148,7 @@ contract DeployStrategy is Script { address[] memory collateralTokens = stringToAddressArray(vm.envString("COLLATERAL_TOKEN_ADDRESSES")); uint256[] memory minCollateralRatios = stringToUintArray(vm.envString("MIN_COLLATERAL_RATIOS")); address governorRoleAddress = vm.envAddress("GOVERNOR_ROLE_ADDRESS"); + uint256 profitMaxUnlockTime = vm.envUint("PROFIT_MAX_UNLOCK_TIME"); bool isTest = vm.envBool("IS_TEST"); @@ -166,6 +167,8 @@ contract DeployStrategy is Script { console.log("deployed strategy contract to"); console.log(address(strategy)); + ITokenizedStrategy(address(strategy)).setProfitMaxUnlockTime(profitMaxUnlockTime); + ITokenizedStrategy(address(strategy)).setPendingManagement(strategyManagement); console.log("set pending management"); console.log(strategyManagement); @@ -179,6 +182,7 @@ contract DeployStrategy is Script { strategy.setCollateralTokenParams(collateralTokens[i], minCollateralRatios[i]); } + strategy.setPendingGovernor(governorRoleAddress); console.log("set pending governor"); console.log(governorRoleAddress);