struct signal_buffer {
    size_t len;
    uint8_t data[];
};

int signal_constant_memcmp(const void *s1, const void *s2, size_t n)
{
    size_t i;
    const unsigned char *c1 = (const unsigned char *) s1;
    const unsigned char *c2 = (const unsigned char *) s2;
    unsigned char result = 0;
    for (i = 0; i < n; i++) {
        result |= c1[i] ^ c2[i];
    }
    return result;
}

from saw_client.llvm import *
class ConstantMemcmpEqualSpec(Contract):
    def specification(self) -> None:
        _1
        self.execute_func(_2)
        _3

class ConstantMemcmpEqualSpec(Contract):
    n: int
    def __init__(self, n: int):
        super().__init__()
        self.n = n
    def specification(self) -> None:
        s1  = self.fresh_var(array_ty(self.n, i8), "s1")
        s1p = self.alloc(array_ty(self.n, i8), points_to = s1)
        s2  = self.fresh_var(array_ty(self.n, i8), "s2")
        s2p = self.alloc(array_ty(self.n, i8), points_to = s2)
        self.precondition(cryptol(f"{s1.name()} == {s2.name()}"))
        self.execute_func(s1p, s2p, cryptol(f"{self.n} : [64]"))
        self.returns(cryptol("0 : [32]"))

mod = llvm_load_module("libsignal-protocol-c.bc") # An LLVM bitcode file
array_len = 42 # Pick whichever length you want to check
llvm_verify(mod, "signal_constant_memcmp",
ConstantMemcmpEqualSpec(array_len))

Verified: lemma_ConstantMemcmpEqualSpec (defined at signal_protocol.py:122)

def ptr_to_fresh(spec: Contract, ty: LLVMType,
                 name: str) -> Tuple[FreshVar, SetupVal]:
    var = spec.fresh_var(ty, name)
    ptr = spec.alloc(ty, points_to = var)
    return (var, ptr)
class ConstantMemcmpEqualSpec(Contract):
    ...
    def specification(self) -> None:
        (s1, s1p) = ptr_to_fresh(self, array_ty(self.n, i8), "s1")
        (s2, s2p) = ptr_to_fresh(self, array_ty(self.n, i8), "s2")
        ...

hmac_init : {n} [n][8] -> HMACContext
hmac_init = undefined
hmac_update : {n} [n][8] -> HMACContext -> HMACContext
hmac_update = undefined
hmac_final : HMACContext -> [SIGNAL_MESSAGE_MAC_LENGTH][8]
hmac_final = undefined

class SignalHmacSha256InitSpec(Contract):
    key_len: int
    def specification(self) -> None:
        hmac_context_ptr = self.alloc(...)
        (key_data, key)  = ptr_to_fresh(self, array_ty(self.key_len, i8),
                                        "key_data")
        self.execute_func(..., hmac_context_ptr, key,
                          cryptol(f"{self.key_len} : [64]"))
        init = f"hmac_init`{{ {self.key_len} }} {key_data.name()}"
        dummy_hmac_context = self.alloc(..., points_to = cryptol(init))
        self.points_to(hmac_context_ptr, dummy_hmac_context)
        self.returns(cryptol("0 : [32]"))
key_len = 32
init_spec = llvm_assume(mod, "signal_hmac_sha256_init",
                        SignalHmacSha256InitSpec(key_len))

def mk_hmac(serialized_len: int, serialized_data: FreshVar,
          receiver_identity_key_data : FreshVar,
          sender_identity_key_data: FreshVar,
          mac_key_len: int, mac_key_data: FreshVar) -> SetupVal:
    sender_identity_buf = f"""
        [{DJB_TYPE}] # {sender_identity_key_data.name()}
            : [{DJB_KEY_LEN} + 1][8]
        """
    receiver_identity_buf = f"""
        [{DJB_TYPE}] # {receiver_identity_key_data.name()}
            : [{DJB_KEY_LEN} + 1][8]
        """
    hmac = f"""
        hmac_final
         (hmac_update`{{ {serialized_len} }} {serialized_data.name()}
          (hmac_update`{{ {DJB_KEY_LEN}+1 }} ({receiver_identity_buf})
           (hmac_update`{{ {DJB_KEY_LEN}+1 }} ({sender_identity_buf})
            (hmac_init`{{ {mac_key_len} }} {mac_key_data.name()}))))
        """
    return cryptol(hmac)

lass SignalMessageVerifyMacSpec(Contract):
    serialized_len: int
    def specification(self) -> None:
        ...
        mac_index = 8 + self.serialized_len - SIGNAL_MESSAGE_MAC_LENGTH
        ser_len   = f"{self.serialized_len} : [64]"
        self.points_to(serialized[0], cryptol(ser_len))
        self.points_to(serialized[8], serialized_message_data)
        self.points_to(serialized[mac_index], mk_hmac(...))
        self.execute_func(...)
        self.returns(cryptol("1 : [32]"))

uninterps = ["hmac_init", "hmac_update", "hmac_final"]
llvm_verify(mod, "signal_message_verify_mac",  SignalMessageVerifyMacSpec(...),
            lemmas=[init_spec, update_spec1, update_spec2, final_spec],
            script=ProofScript([z3(uninterps)]))