From 25761783890530a0c45b57f797938b5190394ed7 Mon Sep 17 00:00:00 2001 From: Oz Date: Thu, 4 Aug 2022 15:13:22 +0300 Subject: [PATCH 1/7] Adding a remote container of docker with certoraRun app --- .devcontainer/Dockerfile | 20 ++++++++++++++++++++ .devcontainer/devcontainer.json | 6 ++++++ 2 files changed, 26 insertions(+) create mode 100644 .devcontainer/Dockerfile create mode 100644 .devcontainer/devcontainer.json diff --git a/.devcontainer/Dockerfile b/.devcontainer/Dockerfile new file mode 100644 index 00000000..a5c6b3b4 --- /dev/null +++ b/.devcontainer/Dockerfile @@ -0,0 +1,20 @@ +# Using the official solc alpine image from ethereum org +FROM ethereum/solc:stable-alpine + +# Installing Python3 with pip +ENV PYTHONUNBUFFERED=1 +RUN apk add --update --no-cache python3 && ln -sf python3 /usr/bin/python +RUN python3 -m ensurepip +RUN pip3 install --no-cache --upgrade pip setuptools + +# Installing JDK 11 +RUN apk add --no-cache openjdk11 + +# Installing gcc and other build apps +RUN apk add --no-cache build-base + +# Installing certora python pacakge +RUN pip install certora-cli + +# Changing the entrypoint from solc to certoraRun app +ENTRYPOINT ["certoraRun"] \ No newline at end of file diff --git a/.devcontainer/devcontainer.json b/.devcontainer/devcontainer.json new file mode 100644 index 00000000..c0b8533a --- /dev/null +++ b/.devcontainer/devcontainer.json @@ -0,0 +1,6 @@ +{ + "name": "CertoraRun", + "build": { + "dockerfile": "Dockerfile" + } +} \ No newline at end of file From 6225cc1baf53ca126d4a64193aa281b99b96c434 Mon Sep 17 00:00:00 2001 From: Oz Date: Mon, 8 Aug 2022 10:54:33 +0300 Subject: [PATCH 2/7] Adding a remote container of docker with certoraRun app --- .devcontainer/Dockerfile | 20 -------------------- .devcontainer/devcontainer.json | 4 +--- 2 files changed, 1 insertion(+), 23 deletions(-) delete mode 100644 .devcontainer/Dockerfile diff --git a/.devcontainer/Dockerfile b/.devcontainer/Dockerfile deleted file mode 100644 index a5c6b3b4..00000000 --- a/.devcontainer/Dockerfile +++ /dev/null @@ -1,20 +0,0 @@ -# Using the official solc alpine image from ethereum org -FROM ethereum/solc:stable-alpine - -# Installing Python3 with pip -ENV PYTHONUNBUFFERED=1 -RUN apk add --update --no-cache python3 && ln -sf python3 /usr/bin/python -RUN python3 -m ensurepip -RUN pip3 install --no-cache --upgrade pip setuptools - -# Installing JDK 11 -RUN apk add --no-cache openjdk11 - -# Installing gcc and other build apps -RUN apk add --no-cache build-base - -# Installing certora python pacakge -RUN pip install certora-cli - -# Changing the entrypoint from solc to certoraRun app -ENTRYPOINT ["certoraRun"] \ No newline at end of file diff --git a/.devcontainer/devcontainer.json b/.devcontainer/devcontainer.json index c0b8533a..7b960dde 100644 --- a/.devcontainer/devcontainer.json +++ b/.devcontainer/devcontainer.json @@ -1,6 +1,4 @@ { "name": "CertoraRun", - "build": { - "dockerfile": "Dockerfile" - } + "image": "ozcertora/certorarun:latest" } \ No newline at end of file From ba22be7d60ca4ca9a359044ba669b4ece600146b Mon Sep 17 00:00:00 2001 From: Taz <46790424+ozcodes@users.noreply.github.com> Date: Tue, 16 Aug 2022 21:55:20 +0300 Subject: [PATCH 3/7] Update devcontainer.json --- .devcontainer/devcontainer.json | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.devcontainer/devcontainer.json b/.devcontainer/devcontainer.json index 7b960dde..bc17a364 100644 --- a/.devcontainer/devcontainer.json +++ b/.devcontainer/devcontainer.json @@ -1,4 +1,4 @@ { "name": "CertoraRun", - "image": "ozcertora/certorarun:latest" -} \ No newline at end of file + "image": "ozcertora/certorarun:ubuntu" +} From 135a7213dca162a4f1fb5888068c28af15053986 Mon Sep 17 00:00:00 2001 From: Michael George Date: Wed, 17 Aug 2022 12:39:22 -0400 Subject: [PATCH 4/7] solc version bump --- .../RunScriptExample/verifyIntegrityOfDeposit.sh | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/01.Lesson_GettingStarted/RunScriptExample/verifyIntegrityOfDeposit.sh b/01.Lesson_GettingStarted/RunScriptExample/verifyIntegrityOfDeposit.sh index 7c4378c2..30fe3f7b 100644 --- a/01.Lesson_GettingStarted/RunScriptExample/verifyIntegrityOfDeposit.sh +++ b/01.Lesson_GettingStarted/RunScriptExample/verifyIntegrityOfDeposit.sh @@ -1,7 +1,7 @@ # format: : --verify : certoraRun BankLesson1/Bank.sol:Bank --verify Bank:BankLesson1/IntegrityOfDeposit.spec \ - --solc solc7.6 \ + --solc solc-0.7.6 \ --rule integrityOfDeposit \ --msg "$1" @@ -9,4 +9,4 @@ certoraRun BankLesson1/Bank.sol:Bank --verify Bank:BankLesson1/IntegrityOfDeposi # more on backslash before new line here: https://superuser.com/questions/794963/in-a-linux-shell-why-does-backslash-newline-not-introduce-whitespace#:~:text=The%20Backslash%2Dnewline%20is%20used,purposes%20of%20executing%20the%20script. # The $1 is the first argument given to the script, so we can change the msg of a run without changing the actual script -# more on $1 here: https://bash.cyberciti.biz/guide/$1 \ No newline at end of file +# more on $1 here: https://bash.cyberciti.biz/guide/$1 From 7a420cc6401d10928264aa5b24f1652102a2bda4 Mon Sep 17 00:00:00 2001 From: Taz <46790424+ozcodes@users.noreply.github.com> Date: Thu, 25 Aug 2022 10:42:36 +0300 Subject: [PATCH 5/7] change docker repo to our official repo --- .devcontainer/devcontainer.json | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.devcontainer/devcontainer.json b/.devcontainer/devcontainer.json index bc17a364..4cc238df 100644 --- a/.devcontainer/devcontainer.json +++ b/.devcontainer/devcontainer.json @@ -1,4 +1,4 @@ { - "name": "CertoraRun", - "image": "ozcertora/certorarun:ubuntu" + "name": "certora-prover", + "image": "certora/certora-prover:ubuntu" } From 919f083c52748d715216b51c162897ec07cce061 Mon Sep 17 00:00:00 2001 From: Taz <46790424+ozcodes@users.noreply.github.com> Date: Thu, 25 Aug 2022 11:08:13 +0300 Subject: [PATCH 6/7] Revert back to Certora naming convention before merging --- .../RunScriptExample/verifyIntegrityOfDeposit.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/01.Lesson_GettingStarted/RunScriptExample/verifyIntegrityOfDeposit.sh b/01.Lesson_GettingStarted/RunScriptExample/verifyIntegrityOfDeposit.sh index 30fe3f7b..9845374c 100644 --- a/01.Lesson_GettingStarted/RunScriptExample/verifyIntegrityOfDeposit.sh +++ b/01.Lesson_GettingStarted/RunScriptExample/verifyIntegrityOfDeposit.sh @@ -1,7 +1,7 @@ # format: : --verify : certoraRun BankLesson1/Bank.sol:Bank --verify Bank:BankLesson1/IntegrityOfDeposit.spec \ - --solc solc-0.7.6 \ + --solc solc7.6 \ --rule integrityOfDeposit \ --msg "$1" From 81bb8ef60154a0d82810ae2ed59fedf1b93223f1 Mon Sep 17 00:00:00 2001 From: Taz <46790424+ozcodes@users.noreply.github.com> Date: Thu, 25 Aug 2022 11:10:32 +0300 Subject: [PATCH 7/7] Removed last line