From 7ee5d2060329b9b960891af1d0574b0c8c0ed748 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ondrej=20Kur=C3=A1k?= Date: Tue, 10 Dec 2024 18:08:35 +0100 Subject: [PATCH] Add comments --- .github/workflows/main.yml | 9 +- .gitignore | 411 +++++++++++++++++++++++++++++++++++++ tests/conf2.conf | 2 +- workflow.yml | 133 +++++++++++- 4 files changed, 544 insertions(+), 11 deletions(-) create mode 100644 .gitignore diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index b00130b..02568ca 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -1,12 +1,17 @@ on: + push: + branches: + - main + pull_request: + branches: + - main workflow_dispatch: jobs: test: - uses: ./workflow.yml + uses: ./workflow.yml@feat/initial-setup secrets: inherit with: - version: 7.0.0 use-beta: true configurations: |- tests/conf1.conf diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..9741e8a --- /dev/null +++ b/.gitignore @@ -0,0 +1,411 @@ +/tmp +emv-* +.certora_internal/ + +# MacOS +# General +.DS_Store +.AppleDouble +.LSOverride + +# Icon must end with two \r +Icon + +# Thumbnails +._* + +# Files that might appear in the root of a volume +.DocumentRevisions-V100 +.fseventsd +.Spotlight-V100 +.TemporaryItems +.Trashes +.VolumeIcon.icns +.com.apple.timemachine.donotpresent + +# Directories potentially created on remote AFP share +.AppleDB +.AppleDesktop +Network Trash Folder +Temporary Items +.apdisk + +# Byte-compiled / optimized / DLL files +__pycache__/ +*.py[cod] +*$py.class + +# C extensions +*.so + +# Distribution / packaging +.Python +build/ +develop-eggs/ +dist/ +downloads/ +eggs/ +.eggs/ +lib/ +lib64/ +parts/ +sdist/ +var/ +wheels/ +share/python-wheels/ +*.egg-info/ +.installed.cfg +*.egg +MANIFEST + +# PyInstaller +# Usually these files are written by a python script from a template +# before PyInstaller builds the exe, so as to inject date/other infos into it. +*.manifest +*.spec +!tests/*.spec + +# Installer logs +pip-log.txt +pip-delete-this-directory.txt + +# Unit test / coverage reports +htmlcov/ +.tox/ +.nox/ +.coverage* +.coverage.* +.cache +nosetests.xml +coverage.xml +*.cover +*.py,cover +.hypothesis/ +.pytest_cache/ +cover/ + +# Translations +*.mo +*.pot + +# Django stuff: +*.log +local_settings.py +db.sqlite3 +db.sqlite3-journal + +# Flask stuff: +instance/ +.webassets-cache + +# Scrapy stuff: +.scrapy + +# Sphinx documentation +docs/_build/ + +# PyBuilder +.pybuilder/ +target/ + +# Jupyter Notebook +.ipynb_checkpoints + +# IPython +profile_default/ +ipython_config.py + +# pyenv +# For a library or package, you might want to ignore these files since the code is +# intended to run in multiple environments; otherwise, check them in: +# .python-version + +# pipenv +# According to pypa/pipenv#598, it is recommended to include Pipfile.lock in version control. +# However, in case of collaboration, if having platform-specific dependencies or dependencies +# having no cross-platform support, pipenv may install dependencies that don't work, or not +# install all needed dependencies. +#Pipfile.lock + +# poetry +# Similar to Pipfile.lock, it is generally recommended to include poetry.lock in version control. +# This is especially recommended for binary packages to ensure reproducibility, and is more +# commonly ignored for libraries. +# https://python-poetry.org/docs/basic-usage/#commit-your-poetrylock-file-to-version-control +#poetry.lock + +# pdm +# Similar to Pipfile.lock, it is generally recommended to include pdm.lock in version control. +#pdm.lock +# pdm stores project-wide configurations in .pdm.toml, but it is recommended to not include it +# in version control. +# https://pdm.fming.dev/#use-with-ide +.pdm.toml + +# PEP 582; used by e.g. github.com/David-OConnor/pyflow and github.com/pdm-project/pdm +__pypackages__/ + +# Celery stuff +celerybeat-schedule +celerybeat.pid + +# SageMath parsed files +*.sage.py + +# Environments +.env +.venv +env/ +venv/ +ENV/ +env.bak/ +venv.bak/ + +# Spyder project settings +.spyderproject +.spyproject + +# Rope project settings +.ropeproject + +# mkdocs documentation +/site + +# mypy +.mypy_cache/ +.dmypy.json +dmypy.json + +# Pyre type checker +.pyre/ + +# pytype static type analyzer +.pytype/ + +# Cython debug symbols +cython_debug/ + +# VS Code +.vscode/* +# !.vscode/settings.json +# !.vscode/tasks.json +# !.vscode/launch.json +# !.vscode/extensions.json +# !.vscode/*.code-snippets + +# Local History for Visual Studio Code +.history/ + +# Built Visual Studio Code Extensions +*.vsix + +# Covers JetBrains IDEs: IntelliJ, RubyMine, PhpStorm, AppCode, PyCharm, CLion, Android Studio, WebStorm and Rider +# Reference: https://intellij-support.jetbrains.com/hc/en-us/articles/206544839 + +# User-specific stuff +.idea/**/workspace.xml +.idea/**/tasks.xml +.idea/**/usage.statistics.xml +.idea/**/dictionaries +.idea/**/shelf + +# AWS User-specific +.idea/**/aws.xml + +# Generated files +.idea/**/contentModel.xml + +# Sensitive or high-churn files +.idea/**/dataSources/ +.idea/**/dataSources.ids +.idea/**/dataSources.local.xml +.idea/**/sqlDataSources.xml +.idea/**/dynamic.xml +.idea/**/uiDesigner.xml +.idea/**/dbnavigator.xml + +# Gradle +.idea/**/gradle.xml +.idea/**/libraries + +# Gradle and Maven with auto-import +# When using Gradle or Maven with auto-import, you should exclude module files, +# since they will be recreated, and may cause churn. Uncomment if using +# auto-import. +# .idea/artifacts +# .idea/compiler.xml +# .idea/jarRepositories.xml +# .idea/modules.xml +# .idea/*.iml +# .idea/modules +# *.iml +# *.ipr + +# CMake +cmake-build-*/ + +# Mongo Explorer plugin +.idea/**/mongoSettings.xml + +# File-based project format +*.iws + +# IntelliJ +out/ + +# mpeltonen/sbt-idea plugin +.idea_modules/ + +# JIRA plugin +atlassian-ide-plugin.xml + +# Cursive Clojure plugin +.idea/replstate.xml + +# SonarLint plugin +.idea/sonarlint/ + +# Crashlytics plugin (for Android Studio and IntelliJ) +com_crashlytics_export_strings.xml +crashlytics.properties +crashlytics-build.properties +fabric.properties + +# Editor-based Rest Client +.idea/httpRequests + +# Android studio 3.1+ serialized cache file +.idea/caches/build_file_checksums.ser +Footer + +# Logs +logs +*.log +npm-debug.log* +yarn-debug.log* +yarn-error.log* +lerna-debug.log* +.pnpm-debug.log* + +# Diagnostic reports (https://nodejs.org/api/report.html) +report.[0-9]*.[0-9]*.[0-9]*.[0-9]*.json + +# Runtime data +pids +*.pid +*.seed +*.pid.lock + +# Directory for instrumented libs generated by jscoverage/JSCover +lib-cov + +# Coverage directory used by tools like istanbul +coverage +*.lcov + +# nyc test coverage +.nyc_output + +# Grunt intermediate storage (https://gruntjs.com/creating-plugins#storing-task-files) +.grunt + +# Bower dependency directory (https://bower.io/) +bower_components + +# node-waf configuration +.lock-wscript + +# Compiled binary addons (https://nodejs.org/api/addons.html) +build/Release + +# Dependency directories +node_modules/ +jspm_packages/ + +# Snowpack dependency directory (https://snowpack.dev/) +web_modules/ + +# TypeScript cache +*.tsbuildinfo + +# Optional npm cache directory +.npm + +# Optional eslint cache +.eslintcache + +# Optional stylelint cache +.stylelintcache + +# Microbundle cache +.rpt2_cache/ +.rts2_cache_cjs/ +.rts2_cache_es/ +.rts2_cache_umd/ + +# Optional REPL history +.node_repl_history + +# Output of 'npm pack' +*.tgz + +# Yarn Integrity file +.yarn-integrity + +# dotenv environment variable files +.env +.env.development.local +.env.test.local +.env.production.local +.env.local + +# parcel-bundler cache (https://parceljs.org/) +.cache +.parcel-cache + +# Next.js build output +.next +out + +# Nuxt.js build / generate output +.nuxt +dist + +# Gatsby files +.cache/ +# Comment in the public line in if your project uses Gatsby and not Next.js +# https://nextjs.org/blog/next-9-1#public-directory-support +# public + +# vuepress build output +.vuepress/dist + +# vuepress v2.x temp and cache directory +.temp +.cache + +# Docusaurus cache and generated files +.docusaurus + +# Serverless directories +.serverless/ + +# FuseBox cache +.fusebox/ + +# DynamoDB Local files +.dynamodb/ + +# TernJS port file +.tern-port + +# Stores VSCode versions used for testing VSCode extensions +.vscode-test + +# yarn v2 +.yarn/cache +.yarn/unplugged +.yarn/build-state.yml +.yarn/install-state.gz +.pnp.* +**.idea** diff --git a/tests/conf2.conf b/tests/conf2.conf index fd86974..619aec2 100644 --- a/tests/conf2.conf +++ b/tests/conf2.conf @@ -3,6 +3,6 @@ "tests/Invertible.sol:InvertibleBroken" ], "process": "emv", - "solc": "solc0.8.1", + "solc": "solc8.1", "verify": "InvertibleBroken:tests/Invertible.spec" } diff --git a/workflow.yml b/workflow.yml index c2b0997..256aea4 100644 --- a/workflow.yml +++ b/workflow.yml @@ -43,6 +43,18 @@ on: 0.6.12 0.7.6 ``` + solc-remove-version-prefix: + required: false + type: string + description: |- + The prefix to remove from the Solidity version when saving binaries. + server: + required: true + default: production + type: string + description: |- + The server to run the tests on. Default is `production`. + Options: `production`, `staging`, or `vaas-dev`. use-alpha: required: false type: boolean @@ -53,8 +65,15 @@ on: type: boolean description: |- Whether to use the beta version of the `certora-cli`. + add-status: + required: true + default: true + type: boolean + description: |- + Whether to add status checks to the commit. + secrets: - certora-key: + CERTORAKEY: required: true env: @@ -87,11 +106,12 @@ jobs: else COMMIT_SHA="$(git rev-parse HEAD)" fi - echo "COMMIT_SHA=${COMMIT_SHA:0:12}" >> $GITHUB_ENV + echo "COMMIT_SHA=${COMMIT_SHA}" >> $GITHUB_ENV + echo "SHORT_COMMIT_SHA=${COMMIT_SHA:0:12}" >> $GITHUB_ENV - name: Group ID and Message run: | - echo "MESSAGE_SUFFIX=${{ github.repository }}/${COMMIT_SHA}" >> $GITHUB_ENV + echo "MESSAGE_SUFFIX=GH:${{ github.repository }}/${SHORT_COMMIT_SHA}" >> $GITHUB_ENV echo "GROUP_ID=$(cat /proc/sys/kernel/random/uuid)" >> $GITHUB_ENV - name: Cache CLI Dependencies Key @@ -137,7 +157,13 @@ jobs: for version in $VERSIONS; do version="${version#v}" - BIN_PATH="/opt/solc-bin/solc$version" + if [ -z "${{ inputs.solc-remove-version-prefix }}" ]; then + use_version=$version + else + use_version="${version#${{ inputs.solc-remove-version-prefix }}}" + fi + + BIN_PATH="/opt/solc-bin/solc$use_version" if [ ! -f "$BIN_PATH" ]; then echo "Downloading Solidity $version" @@ -157,7 +183,7 @@ jobs: # Verify the binary chmod +x "$BIN_PATH" - "solc$version" --version + "solc$use_version" --version fi done @@ -174,11 +200,102 @@ jobs: done - name: Run Certora + id: certora-run run: | CONFIGURATIONS="${{ inputs.configurations }}" + MAX_MSG_LEN=254 + SUFFIX_LEN=${#MESSAGE_SUFFIX} + REMAINING_LEN=$((MAX_MSG_LEN - SUFFIX_LEN)) + jobs=0 + + LOG_DIR="/tmp/certora-logs/" + mkdir -p "$LOG_DIR" + + for conf in $CONFIGURATIONS; do + echo "Starting $conf" + + if [[ ${#conf} -gt $conf_max_length ]]; then + msg_conf=${conf: -$REMAINING_LEN} + else + msg_conf=$conf + fi + + # Create log files + STDOUT="$LOG_DIR/$conf.stdout" + mkdir -p "$(dirname "$STDOUT")" + STDERR="$LOG_DIR/$conf.stderr" + mkdir -p "$(dirname "$STDERR")" + + uvx --from "$CERT_CLI_PACKAGE" certoraRun \ + $conf \ + --msg "${msg_conf} ${MESSAGE_SUFFIX}" \ + --server "${{ inputs.server }}" \ + --group_id "${GROUP_ID}" \ + --send_only \ + --wait_for_results none >"$STDERR" 2>"$STDERR" & + + ((jobs++)) || true + done + + # Wait for all jobs to finish and mark if any failed + total_ret=0 + failed_jobs=0 for conf in $CONFIGURATIONS; do - echo "Running $conf" - uvx --from "$CERT_CLI_PACKAGE" certoraRun $conf --msg "${MESSAGE_SUFFIX}" --group_id "${GROUP_ID}" + ret=0 + wait -n || ret=$? + if [ $ret -ne 0 ]; then + ((jobs--)) || true + ((failed_jobs++)) || true + total_ret=$ret + fi done + + # Add jobs to output + echo "total_jobs=$jobs" >> $GITHUB_OUTPUT + echo "failed_jobs=$failed_jobs" >> $GITHUB_OUTPUT + + # Remove empty log files + find "$LOG_DIR" -type f -empty -delete + + if [ $ret -ne 0 ]; then + echo "Some configurations failed! Please check the logs." + exit $ret + fi + + env: + CERTORAKEY: ${{ secrets.CERTORAKEY }} + + - name: Add GH Status + if: ${{ inputs.add-status }} + run: | + curl -L \ + -X POST \ + -H "Accept: application/vnd.github+json" \ + -H "Authorization: Bearer ${GITHUB_TOKEN}" \ + -H "X-GitHub-Api-Version: 2022-11-28" \ + https://api.github.com/repos/${{ github.repository }}/statuses/$COMMIT_SHA \ + -d '{"state":"pending","target_url":"https://prover.certora.com","description":"0/${{ steps.certora-run.outputs.total_jobs }} jobs finished.","context":"certora-run"}' + env: + GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} + + - name: Upload Logs + uses: actions/upload-artifact@v4 + id: upload-logs + if: always() + with: + name: logs + path: /tmp/certora-logs/* + + # Add comment with log link + - name: Add Comment With Logs Link + if: ${{ steps.upload-logs.outputs.artifact-url }} + run: | + curl -L \ + -X POST \ + -H "Accept: application/vnd.github+json" \ + -H "Authorization: Bearer ${GITHUB_TOKEN}" \ + -H "X-GitHub-Api-Version: 2022-11-28" \ + https://api.github.com/repos/${{ github.repository }}/commits/$COMMIT_SHA/comments \ + -d '{"body":"# Started Certora Run\n\n- Started ${{ steps.certora-run.outputs.total_jobs }} jobs\n- ${{ steps.certora-run.outputs.failed_jobs }} jobs failed\n\n[Logs](${{ steps.upload-logs.outputs.artifact-url }})\n"}' env: - CERTORAKEY: ${{ secrets.certora-key }} + GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}