[saw-remote-api] xxHash verification stalls #1411
Comments
|
I don't think this has anything to do with Cryptol, but rather what solver you're using. --- xxhash32-ref.py.old 2021-08-09 10:22:30.460947226 -0400
+++ xxhash32-ref.py.new 2021-08-09 10:22:20.329042338 -0400
@@ -2,6 +2,7 @@
from saw_client import LogResults, connect, cryptol_load_file, llvm_load_module, llvm_verify, view
from saw_client.llvm import Contract, cryptol, i32
+from saw_client.proofscript import ProofScript, z3
class Contract_XXH_rotl32(Contract):
def specification(self) -> None:
@@ -44,7 +45,8 @@
result_XXH_rotl32 = llvm_verify(
module=mod,
function='XXH_rotl32',
- contract=Contract_XXH_rotl32()
+ contract=Contract_XXH_rotl32(),
+ script=ProofScript([z3([])])
)
# hangs
@@ -52,12 +54,14 @@
module=mod,
function='XXH32_round',
contract=Contract_XXH32_round(),
- lemmas=[result_XXH_rotl32]
+ lemmas=[result_XXH_rotl32],
+ script=ProofScript([z3([])])
)
# also hangs, even with other `llvm_verify` calls commented out
result_XXH32_avalanche = llvm_verify(
module=mod,
function='XXH32_avalanche',
- contract=Contract_XXH32_avalanche()
+ contract=Contract_XXH32_avalanche(),
+ script=ProofScript([z3([])])
)Then the verification succeeds. |
Looks good! Thank you for the demo on how to change the proof script. I saw that detail in the SAW proofs but wasn't sure how to convey it through the Python API. |
|
Here is a full Python script to verify Some points of amusement:
from typing import Optional, Tuple
from unittest import TestCase, main
from saw_client import LogResults, connect, cryptol_load_file, llvm_load_module, llvm_verify, view
from saw_client.llvm import Contract, FreshVar, LLVMArrayType, LLVMType, SetupVal, cryptol, i8, i32, i64, null
from saw_client.proofscript import ProofScript, yices, z3
class UtilContract(Contract):
def ptr_to_fresh(self, ty : LLVMType, name : Optional[str] = None, read_only: Optional[bool] = False) -> Tuple[FreshVar, SetupVal]:
"""Add to``Contract`` ``c`` an allocation of a pointer of type ``ty`` initialized to an unknown fresh value.
:returns A fresh variable bound to the pointers initial value and the newly allocated pointer. (The fresh
variable will be assigned ``name`` if provided/available.)"""
var = self.fresh_var(ty, name)
ptr = self.alloc(ty, points_to = var, read_only = read_only)
return (var, ptr)
class Contract_XXH_rotl32(Contract):
def specification(self) -> None:
value = self.fresh_var(i32, "value")
amt = self.fresh_var(i32, "amt")
self.execute_func(value, amt)
self.returns( cryptol("(<<<)")(value, amt) )
class Contract_XXH32_round(Contract):
def specification(self) -> None:
acc = self.fresh_var(i32, "acc")
input_ = self.fresh_var(i32, "input")
self.execute_func(acc, input_)
self.returns( cryptol("XXH32_round")(acc, input_) )
class Contract_XXH32_avalanche(Contract):
def specification(self) -> None:
hash_ = self.fresh_var(i32, "hash")
self.execute_func(hash_)
self.returns( cryptol("XXH32_avalanche")(hash_) )
class UtilContract_XXH32(UtilContract):
@property
def length(self) -> Optional[int]:
return self._length
def __init__(self, length: Optional[int] = None) -> None:
super().__init__()
self._length = length
def specification(self) -> None:
nbytes = self.length or 0
((input, input_p), length) = (
(self.ptr_to_fresh(LLVMArrayType(i8, nbytes), "input", read_only = True), cryptol(f"{self.length}:[64]")) if self.length
else ((cryptol("zero"), null()), self.fresh_var(i64, "length"))
)
seed = self.fresh_var(i32, "seed")
self.execute_func(input_p, length, seed)
self.returns(cryptol(f"XXH32`{{L={ nbytes }}}")(cryptol(input), cryptol(seed)))
class XXH32RefTest(TestCase):
def test_xxhash32_ref(self) -> None:
connect(reset_server=True)
view(LogResults())
bcname = 'xxhash32-ref.bc'
cryname = 'xxhash.cry'
cryptol_load_file(cryname)
mod = llvm_load_module(bcname)
self.assertTrue(
lemma_XXH_rotl32 := llvm_verify(
module=mod,
function='XXH_rotl32',
contract=Contract_XXH_rotl32()
)
)
self.assertTrue(
lemma_XXH32_round := llvm_verify(
module=mod,
function='XXH32_round',
contract=Contract_XXH32_round(),
lemmas=[lemma_XXH_rotl32],
script=ProofScript([z3([])])
)
)
self.assertTrue(
lemma_XXH32_avalanche := llvm_verify(
module=mod,
function='XXH32_avalanche',
contract=Contract_XXH32_avalanche(),
script=ProofScript([z3([])])
)
)
lemmas_XXH32 = {}
for size in [None,0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,32,64,128]:
print(f"lemma_Contract_XXH32_{size}")
self.assertTrue(
lemmas_XXH32.setdefault(size, llvm_verify(
module=mod,
function='XXH32',
contract=UtilContract_XXH32(size),
lemmas=[lemma_XXH_rotl32, lemma_XXH32_round, lemma_XXH32_avalanche],
script=ProofScript([yices([])]),
lemma_name_hint=f"lemma_UtilContract_XXH32_{size}"
))
)
if __name__ == "__main__":
main() |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
I'm trying to verify a reference implementation of 32-bit xxHash (the same one as in saw-demos) using the most recent PyPI version of the SAW Remote API for Python, but my attempt stalls when trying to verify
XXH32_avalancheorXXH32_roundagainst a respective contract based on xxhash.cry:This suggests some problem with loading and calling a declaration from
xxhash.cry, asXXH_rotl32can be verified and does not depend onxxhash.cry.The text was updated successfully, but these errors were encountered: