SAW reports Value not in scope: integerFromBV

[AlwaysPS]

I am currently doing a project that aims to provide a trustworthy implementation of the SM2 algorithm. After read the CAV21 paper, I think SAW might be a good tool to provide formal safety guarantee.

As a first step, I wanted to reproduce the verification results from https://github.com/awslabs/aws-lc-verification. However, when trying to import the very first BN.saw specification, SAW immediately complains that it cannot find the definition of integerToBV.

It seems that this definition should be in some .cry files, but even after a through search in the repo I did not find the suitable file.

Here is a minimal example that will reproduce the problem:

import "../cryptol-specs/Common/utils.cry";

disable_debug_intrinsics;

m <- llvm_load_module "./bn_add_words.bc";

include "../aws-lc-verification/SAW/proof/common/helpers.saw";
include "../aws-lc-verification/SAW/proof/internal.saw";

let bn_add_words_spec n = do {
  let num_bits = eval_size {| n * 64 |};
  rp <- crucible_alloc (llvm_int num_bits);
  (a, ap) <- ptr_to_fresh_readonly "a" (llvm_int num_bits);
  (b, bp) <- ptr_to_fresh_readonly "b" (llvm_int num_bits);
  crucible_execute_func [rp, ap, bp, (crucible_term {{ `n : [64] }})];
  crucible_points_to rp (crucible_term {{ integerToBV`{num_bits} (if (integerFromBV a) + (integerFromBV b) >= 2 ^^ `num_bits then (integerFromBV a) + (integerFromBV b) - 2 ^^ `num_bits else (integerFromBV a) + (integerFromBV b)) }});
  crucible_return (crucible_term {{ if (integerFromBV a) + (integerFromBV b) >= 2 ^^ `num_bits then 1 : [64] else 0 }});
};

llvm_verify m "bn_add_words" [] false (bn_add_words_spec 2) z3;

[RyanGlScott]

Just to be sure, have you cloned the cryptol-specs submodule in the aws-lc-verification repo? integerToBV is defined here in cryptol-specs, so it is possible that SAW wouldn't pick it up if the cryptol-specs subdirectory is empty.

[AlwaysPS]

Just to be sure, have you cloned the cryptol-specs submodule in the aws-lc-verification repo? integerToBV is defined here in cryptol-specs, so it is possible that SAW wouldn't pick it up if the cryptol-specs subdirectory is empty.

Thanks for the quick reply! After a quick check I find that I was using the master branch of the repo cryptol-specs, which does not have integerToBV in utils.cry. After checking out to the commit you provide I got SAW working.