Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix blst-verification regression test and update pinned commit #1622

Merged
merged 4 commits into from
Mar 23, 2022
Merged

Fix blst-verification regression test and update pinned commit #1622

Show file tree
Hide file tree
Changes from 2 commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
dfbe858
Fix BLST regression test and update pinned commit
chameco Mar 18, 2022
32cf7e9
Only run memory safety proofs
chameco Mar 18, 2022
c18a694
Update to current HEAD of main on blst-verification
chameco Mar 23, 2022
267fc70
Merge branch 'master' into sb/update-blst
chameco Mar 23, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 3 additions & 1 deletion s2nTests/docker/blst.dockerfile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,8 +5,10 @@ RUN pip3 install wllvm

RUN git clone https://github.com/GaloisInc/blst-verification.git /workdir && \
cd /workdir && \
git checkout 05d29b0e9d826053185e5bdba287045aab0b4669 && \
git checkout e8181fb9f5ebe4d5234b16837b86384849523730 && \
git config --file=.gitmodules submodule.blst.url https://github.com/supranational/blst && \
git config --file=.gitmodules submodule.blst_patched.url https://github.com/supranational/blst && \
git config --file=.gitmodules submodule.blst_bulk_addition.url https://github.com/supranational/blst && \
git config --file=.gitmodules submodule.cryptol-specs.url https://github.com/GaloisInc/cryptol-specs && \
git submodule sync && \
git submodule update --init
Expand Down
3 changes: 2 additions & 1 deletion s2nTests/scripts/blst-entrypoint.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,5 +20,6 @@ yices-smt2 --version
./scripts/build_x86.sh
./scripts/build_llvm.sh

./scripts/prove.sh
saw proof/memory_safety.saw

./scripts/check.sh | if grep False; then exit 1; fi