BUG FIX: basis2 lemma only valid for bit sizes < 254. #31
Workflow file for this run
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
name: Docker Image CI | |
on: | |
push: | |
branches: [ "main" ] | |
pull_request: | |
branches: [ "main" ] | |
workflow_dispatch: | |
jobs: | |
publish-docker: | |
name: "Publish Docker image to DockerHub" | |
if: "github.event_name == 'push'" | |
concurrency: docker_publish | |
runs-on: ubuntu-latest | |
steps: | |
- name: Set up Docker Buildx | |
uses: docker/setup-buildx-action@v2 | |
- name: Login to DockerHub | |
uses: docker/login-action@v2 | |
with: | |
username: ${{ secrets.DOCKERHUB_USERNAME }} | |
password: ${{ secrets.DOCKERHUB_TOKEN }} | |
- name: Build and push to DockerHub | |
uses: docker/build-push-action@v3 | |
with: | |
push: true | |
file: Dockerfile | |
tags: veridise/picus:git-latest , veridise/picus:git-${{ github.sha }} | |
test-compile-circomlib: | |
needs: publish-docker | |
runs-on: ubuntu-latest | |
container: | |
image: veridise/picus:git-${{ github.sha }} | |
credentials: | |
username: ${{ secrets.DOCKERHUB_USERNAME }} | |
password: ${{ secrets.DOCKERHUB_TOKEN }} | |
steps: | |
- uses: actions/checkout@v1 | |
- name: linking circom | |
run: ln -s /root/.cargo/bin/circom /usr/bin/circom | |
- name: compile circomlib | |
run: bash ./scripts/prepare-circomlib.sh | |
test-solve-with-z3: | |
needs: test-compile-circomlib | |
runs-on: ubuntu-latest | |
container: | |
image: veridise/picus:git-${{ github.sha }} | |
credentials: | |
username: ${{ secrets.DOCKERHUB_USERNAME }} | |
password: ${{ secrets.DOCKERHUB_TOKEN }} | |
steps: | |
- uses: actions/checkout@v1 | |
- name: linking circom | |
run: ln -s /root/.cargo/bin/circom /usr/bin/circom | |
- name: compile circomlib | |
run: bash ./scripts/prepare-circomlib.sh | |
- name: preparing rosette | |
run: raco pkg install --auto rosette | |
- name: preparing csv-reading | |
run: raco pkg install --auto csv-reading | |
- name: run picus with z3, using v3 | |
run: racket ./picus-dpvl-uniqueness.rkt --solver z3 --r1cs ./benchmarks/circomlib-cff5ab6/[email protected] --weak | |
test-solve-with-cvc5: | |
needs: test-compile-circomlib | |
runs-on: ubuntu-latest | |
container: | |
image: veridise/picus:git-${{ github.sha }} | |
credentials: | |
username: ${{ secrets.DOCKERHUB_USERNAME }} | |
password: ${{ secrets.DOCKERHUB_TOKEN }} | |
steps: | |
- uses: actions/checkout@v1 | |
- name: linking circom | |
run: ln -s /root/.cargo/bin/circom /usr/bin/circom | |
- name: compile circomlib | |
run: bash ./scripts/prepare-circomlib.sh | |
- name: preparing rosette | |
run: raco pkg install --auto rosette | |
- name: preparing csv-reading | |
run: raco pkg install --auto csv-reading | |
- name: run picus with cvc5, using v3 | |
run: racket ./picus-dpvl-uniqueness.rkt --solver cvc5 --r1cs ./benchmarks/circomlib-cff5ab6/[email protected] --weak |