Execution of impossible paths during verification

[sauclovian-g]

In the course of Formal VerSo work I ran into some cases where apparently impossible paths were executed during verification leading to hitting error in one of the Cryptol models. I have now cut down the Formal VerSo material to a (relatively) small example that still fails, as follows.

First, the ever-popular test.rs:

pub fn f(x: u32) -> u32 {
    x
}

Then, test.saw:

enable_experimental;

import "Test.cry";

mod <- mir_load_module "test.linked-mir.json";

let sym = {{ symbol_from_native 0xaa }};

auth_state <- declare_ghost_state "auth_state";

let f_spec = do {
  value <- mir_fresh_var "value" mir_u32;
  heap <- mir_fresh_cryptol_var "heap" {| Heap |};

  auth <- mir_fresh_cryptol_var "auth" {| Val |};
  mir_assert {{ symbol_valid auth }};
  mir_assert {{ eq auth sym heap }};

  let auth' = {{ checkauth auth }};

  mir_ghost_value auth_state auth;
  mir_execute_func [mir_term value];
  mir_ghost_value auth_state auth';

  mir_return (mir_term value);
};

mir_verify mod "test::f" [] true f_spec w4;

and finally, Test.cry:

module Test where
import Array

/*
 * A somewhat sketchy option type (it can't be a sum)
 */

type Option a = { is_ok : Bool, value : a }

some : {a} a -> Option a
some x = { is_ok = True, value = x }

none : {a} a -> Option a
none x = { is_ok = False, value = x }

crashing_unwrap : {a} Option a -> a
crashing_unwrap o = if o.is_ok then o.value else error "crashing_unwrap"

unwrap_or : {a} Option a -> a -> a
unwrap_or o def = if o.is_ok then o.value else def

/*
 * Sizes and types for values
 */

type TAG_BITS = 8
type VALUE_BITS = 8
type WORD_BITS = TAG_BITS + VALUE_BITS

type Tag = [TAG_BITS]
type Val = [WORD_BITS]

type Handle = [VALUE_BITS]
type Index = [VALUE_BITS]

/*
 * Type tags for values
 */

tag_u32val = 4 : Tag
tag_symbolsmall = 14 : Tag
small_tag_upper_bound = 15 : Tag
tag_vecobject = 75 : Tag

/*
 * Accessors for the fields inside values
 */

mask_of_width : Integer -> [WORD_BITS]
mask_of_width w = (1 << w) - 1

TAG_MASK   = mask_of_width `TAG_BITS
VALUE_MASK  = mask_of_width `VALUE_BITS

TAG_SHIFT   = 0 : Integer
VALUE_SHIFT  = `TAG_BITS

tag_of_val : Val -> Tag
tag_of_val v = drop ((v >> TAG_SHIFT) && TAG_MASK)

value_of_val : Val -> [VALUE_BITS]
value_of_val v = drop ((v >> VALUE_SHIFT) && VALUE_MASK)

val_of_value_and_tag : [VALUE_BITS] -> Tag -> Val
val_of_value_and_tag value tag = value' || tag'
   where
      value' = zext`{WORD_BITS} value << VALUE_SHIFT
      tag' = zext`{WORD_BITS} tag << TAG_SHIFT

/*
 * vector representation
 */

type VecData = Array Index Val

newtype VecRepresentation = {
   data: VecData,
   size: Index
}

invalid_vec_representation : VecRepresentation
invalid_vec_representation = VecRepresentation { data = arrayConstant 0, size = 0 }

vec_representation_equiv_at :
       (Val -> Val -> Heap -> Bool) ->
       VecRepresentation -> VecRepresentation -> Heap ->
       [VALUE_BITS] ->
       Bool
vec_representation_equiv_at subcmp rep1 rep2 heap i =
   if i >= rep1.size then True
   | subcmp x1 x2 heap == False then False
   else vec_representation_equiv_at subcmp rep1 rep2 heap (i + 1)
   where
      x1 = arrayLookup rep1.data i
      x2 = arrayLookup rep2.data i

vec_representation_equiv :
       (Val -> Val -> Heap -> Bool) ->
       VecRepresentation -> VecRepresentation -> Heap ->
       Bool
vec_representation_equiv subcmp rep1 rep2 heap =
   if rep1.size != rep2.size then False
   else vec_representation_equiv_at subcmp rep1 rep2 heap 0

/*
 * heap
 */

type HeapTag = [1]
TagU64 = 0
TagVec = 1

type Heap = {
   types: Array Handle HeapTag,
   values_vecdata: Array Handle VecData,
   values_vecsize: Array Handle [VALUE_BITS],
   next: Handle
}

present_as_vec : Handle -> Heap -> Bool
present_as_vec h s =
   if h >= s.next then False
   | arrayLookup s.types h != TagVec then False
   else True

lookup_vec : Handle -> Heap -> Option VecRepresentation
lookup_vec h s =
   if h >= s.next then none invalid_vec_representation
   | arrayLookup s.types h != TagVec then none invalid_vec_representation
   else
      some rep
      where
         data = arrayLookup s.values_vecdata h
         size = arrayLookup s.values_vecsize h
         rep = VecRepresentation { data = data, size = size }

/*
 * heap-aware equality
 */

eq : Val -> Val -> Heap -> Bool
eq v1 v2 heap =
   if tag1 != tag2 then False
   | tag1 < small_tag_upper_bound then v1 == v2
   | tag1 == tag_vecobject then (
        if handle1 == handle2 then True
        | present_as_vec handle1 heap == False then False
        | present_as_vec handle2 heap == False then False
        else (
           vec_representation_equiv eq rep1 rep2 heap
           where
              rep1 = crashing_unwrap (lookup_vec handle1 heap)
              rep2 = crashing_unwrap (lookup_vec handle2 heap)
              //rep1 = unwrap_or (lookup_vec handle1 heap) invalid_vec_representation
              //rep2 = unwrap_or (lookup_vec handle2 heap) invalid_vec_representation
        )
        where
           handle1 = value_of_val v1
           handle2 = value_of_val v2
   )
   else False
   where
      tag1 = tag_of_val v1
      tag2 = tag_of_val v2

/*
 * symbol values
 */

symbol_valid : Val -> Bool
symbol_valid v = (tag_of_val v) == tag_symbolsmall

symbol_from_native : [VALUE_BITS] -> Val
symbol_from_native s = val_of_value_and_tag s tag_symbolsmall

/*
 * authorization stub; this has to be here or the problem disappears
 * (but that's likely because it gets shortcut away rather than that
 * it doesn't happen)
 */

checkauth: Val -> Val
checkauth auth = auth

When run (saw test.saw) this produces the following output:

[23:31:55.701] Loading file ".../test.saw"
[23:31:55.844] Verifying test/24bff331::f[0] ...
[23:31:55.850] Simulating test/24bff331::f[0] ...
[23:31:55.851] Checking proof obligations test/24bff331::f[0] ...
[23:31:55.855] Run-time error: encountered call to the Cryptol 'error' function

Observe that there's only the one call to error anywhere in here, and while that has two call sites they're next to each other and equivalent, so it's clear where it must be going. (That's on lines 152-153 of Test.cry.)

HOWEVER, that code should be unreachable: the only cases in which lookup_vec produces none are the same cases where present_as_vec produces False.

Furthermore (though it's not as easily inspected) this whole enclosing case should not be reached either because the type tags on both values that are being compared are constrained to be tag_symbolsmall which is less than small_tag_upper_bound. So it should always take the path on line 144.

If you replace the crashing_unwrap with something that doesn't crash, as you can do by uncommenting what's on lines 154-155, then saw runs forever inspecting garbage heap states without any indication that it's spending that time investigating impossible executions. (Although it shouldn't do that either -- because the default value produced is an empty vector the comparison of those should terminate immediately instead of recursing into arbitrary other comparisons.) This is why I've marked it a performance problem.

I have no idea if it's possible to trigger unsoundness via whatever's going on. One would hope the worst that executing impossible paths could cause is spurious counterexamples rather than accepting invalid propositions.