import "dotprod.cry";
m <- llvm_load_module "dotprod.bc";


xs <- fresh_symbolic "xs" {| [12][32] |};
ys <- fresh_symbolic "ys" {| [12][32] |};
let allocs = [ ("x", 12), ("y", 12) ];
let inputs = [ ("*x", xs, 12) , ("*y", ys, 12) , ("size", {{ 12:[32] }}, 1) ];
let outputs = [("return", 1)];

t <- llvm_symexec m "dotprod" allocs inputs outputs true;
thm1 <- abstract_symbolic {{ t == dotprod xs ys }};
prove_print abc thm1;


llvm_verify m "mod_dotprod" [] do {
  llvm_ptr "x" (llvm_array  12 (llvm_int 8));
  x <- llvm_var "*x" (llvm_array  12 (llvm_int 8));
  llvm_ptr "y" (llvm_array  12 (llvm_int 8));
  y <- llvm_var "*y" (llvm_array  12 (llvm_int 8));

  size <- llvm_var "size" (llvm_int 32);
  llvm_assert {{size == 12}};


  let res = {{ mod_dotprod x y }};

  //for very bad output comment the following line
  llvm_ensure_eq "return" {{ res.0 }};


  llvm_ensure_eq "*x" {{ res.1 }};

  llvm_verify_tactic abc;
};