Cryptol and SAW differ, and a performance surprise.

[msaaltink]

Here's a simple function to see if an array element appears at an earlier place:

#include <stdint.h>

uint32_t is_new(uint32_t *list, const uint32_t where) {
  for(int i = 0; i < where; i++) {
    if (list[i] == list[where]) return 0;
  };
  return 1;
}

I've rendered this into Cryptol in two different ways, which Cryptol can show give the same answer so long as the index is less than the length of the list. SAW cannot do that proof:

m <- llvm_load_module "is-new.bc";

let {{
  is_new: {n} (fin n, 32 >= width n) => [n][32] -> [32] -> [32]
  is_new list index = if ok then 1 else 0 where
    ok = and [i < index ==> w != v | w <- list | i <- [0 ..] ]
    v = list @ index

  is_new': {n} (fin n, 32 >= width n) => [n][32] -> [32] -> [32]
  is_new' list index = if index < `n /\ ok @ index then 1 else 0 where
    ok = [True] # [o /\ w != v | w <- list | o <- ok ]
    v = list @ index
}};

// This works in cryptol, but not here in SAW:
// prove yices {{ \xs i -> is_new (xs:[8][32]) (zext (i:[3])) == is_new' xs (zext i) }};

That just grinds away with z3, too, although z3 seems to exhaust memory while yices does not.

There is something else going on:

let is_new_spec n fn = do {
  let ty = llvm_array n (llvm_int 32);
  lp <- crucible_alloc ty;
  l <- crucible_fresh_var "list" ty;
  crucible_points_to lp (crucible_term l);
  w <- crucible_fresh_var "where" (llvm_int 32);
  crucible_precond {{w < `n}};
  crucible_execute_func [lp, crucible_term w];
  crucible_return (crucible_term {{ fn l w }});
  };

let test fn n = time (crucible_llvm_verify m "is_new" [] false (is_new_spec n fn) yices);

for [1,2,3,4,5] (test {{is_new'}});

// for [1,2,3,4] (test {{is_new}});

For n = 1,2,3,4 the proof using is_new' is fairly fast. For n=5, it really locks up my machine, although changing yices to z3 lets me get n=5. But z3 struggles with n=10.

Even for n=1, the proof using {{is_new}} just churns.

[brianhuffman]

The prove command runs seemingly forever even with the offline_smtlib2 proof tactic. I'm testing with a profiling build now.

[brianhuffman]

Ah, I should have noticed this earlier. The problem is entirely because of the use of [0 ..] in is_new, which (at type [32]) is shorthand for [0 .. 4294967295]. Replacing it with [0 ...] fixes everything.

Cryptol has multiple representations for vector types, and heuristics for choosing which one to use; saw-script is less sophisticated in this regard. As a result saw-script actually builds a vector with 2^32 elements in it, just like you asked for.

I really think we should remove the [x..] construct from Cryptol altogether. Using it invariably leads to nasty surprises. And if you really want a list with 2^32 elements, you can always just write [0 .. 4294967295], so we don't lose any expressiveness.

[msaaltink]

I agree about the [x..] construct. I think that I intended to write [0...] here, but when I write without referring to the manual I sometimes mix these two forms up. I don't see a lot of value in omitting the upper bound in the .. form.

[robdockins]

Is there anything still to address in this issue?

[brianhuffman]

I don't think so. Closing.