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

* Fix BLST regression test and update pinned commit * Only run memory safety proofs * Update to current HEAD of main on blst-verification
GaloisInc · Mar 23, 2022 · 5115afb · 5115afb
1 parent dbab6e9
commit 5115afb
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 2 deletions.
diff --git a/s2nTests/docker/blst.dockerfile b/s2nTests/docker/blst.dockerfile
@@ -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 f7c50e400d18066cc4849513418c3f407ba3c608 && \
     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

diff --git a/s2nTests/scripts/blst-entrypoint.sh b/s2nTests/scripts/blst-entrypoint.sh
@@ -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