VST-preview.

Take an unrelease branch from VST that fixes
PrincetonUniversity/VST#561

Author: roconnor-blockstream

C/secp256k1/verif_int128_impl.v

@@ -566,6 +566,9 @@ rewrite !Int64.signed_repr by
  change Int64.max_signed with (2^63 - 1);
  lia).
 forward.
+ entailer!.
+ rewrite Hmod32, Hdiv32, Z.mul_comm by auto.
+ apply Hmul64;[apply Hdiv32bound|apply Z.mod_pos_bound]; lia.
 change (Int.unsigned (Int.repr 32)) with 32.
 rewrite !Int64.mul_signed, Hmod32, Hdiv32 by auto.
 rewrite !Int64.signed_repr by

vst.nix

@@ -4,8 +4,8 @@ stdenv.mkDerivation {
   src = fetchFromGitHub {
     owner = "PrincetonUniversity";
     repo = "VST";
-    rev ="v2.9.1";
-    hash = "sha256-q/Us8bG1Sek2cuAT6mvwxihBKrVl77RW9m0N5uWOQL4=";
+    rev = "9a91f41c4ee1ff56a0c80111c86ed4b2fe51fa11";
+    hash = "sha256-dzsewWQYxbjyVDtdc3TZggoIm/RrHFsYtq88fkYcTQ8=";
   };
 
   buildInputs = [ coq ];