Timeout when trying to verify add operation on HashMap newtype

[janriemer]

Hi all,

disclaimer: I'm totally new to formal verification and creusot, so bear with me 😄

I try to verify a simple add operation on a HashMap newtype (see code below), but it seems I run into a timeout. My ultimate goal is to verify the diffing algorithm of csv-diff, which involves a lot of HashMap operations.

With this "toy example" I want to verify, if creusot is the right tool for this (suitable for verifying HashMap operations).

I've read that verifying HashMap operations is generally very hard for the SMT solver, so am I going down the wrong path here?

What follows is the toy example I'm trying to verify and the output of why3 IDE:

Code to verify

use ::std::collections::HashMap;

use creusot_contracts::{View, ensures, logic, open};

struct Foo(HashMap<u64, u8>);

impl View for Foo {
    type ViewTy = <HashMap<u64, u8> as View>::ViewTy; //FMap<Int, u8>;

    #[logic]
    #[open]
    fn view(self) -> Self::ViewTy {
        self.0.view()
    }
}

impl Foo {
    pub fn new() -> Self {
        Self(HashMap::new())
    }

    #[ensures((^self)@.get(num@) == Some(bar))]
    pub fn add(&mut self, num: u64, bar: u8) {
        *self.0.entry(num).or_insert(bar) = bar;
    }
}

Output of why3

--------------------------- Local Context ---------------------------

type t_RandomState =
  | t_RandomState'mk (t_RandomState__k0:t1) (t_RandomState__k1:t1)

type t_NonNull =
  | t_NonNull'mk (t_NonNull__pointer:ptr)

type t_RawTableInner =
  | t_RawTableInner'mk (t_RawTableInner__bucket_mask:t1)
      (t_RawTableInner__ctrl:t_NonNull) (t_RawTableInner__growth_left:t1)
      (t_RawTableInner__items:t1)

type t_RawTable =
  | t_RawTable'mk (t_RawTable__table:t_RawTableInner) (t_RawTable__alloc:
      unit) (t_RawTable__marker:unit)

type t_HashMap =
  | t_HashMap'mk (t_HashMap__hash_builder:t_RandomState) (t_HashMap__table:
      t_RawTable)

type t_HashMap'0 =
  | t_HashMap'0'mk (t_HashMap__base:t_HashMap)

type t_Foo =
  | t_Foo'mk (t_Foo__0:t_HashMap'0)

type t_NonNull'0 =
  | t_NonNull'0'mk (t_NonNull__pointer'0:ptr)

type t_Bucket =
  | t_Bucket'mk (t_Bucket__ptr:t_NonNull'0)

type t_RustcOccupiedEntry =
  | t_RustcOccupiedEntry'mk (t_RustcOccupiedEntry__elem:t_Bucket)
      (t_RustcOccupiedEntry__table:t2 t_RawTable)

type t_OccupiedEntry =
  | t_OccupiedEntry'mk (t_OccupiedEntry__base:t_RustcOccupiedEntry)

type t_RustcVacantEntry =
  | t_RustcVacantEntry'mk (t_RustcVacantEntry__hash:t1)
      (t_RustcVacantEntry__key:t1) (t_RustcVacantEntry__table:t2 t_RawTable)

type t_VacantEntry =
  | t_VacantEntry'mk (t_VacantEntry__base:t_RustcVacantEntry)

type t_Entry =
  | C_Occupied t_OccupiedEntry
  | C_Vacant t_VacantEntry

predicate resolve (self1:t2 t) = self1.final = self1.current

predicate resolve'0 (_0:t2 t) = resolve _0

predicate resolve'1 (self1:t2 t_Foo) = self1.final = self1.current

predicate resolve'2 (_0:t2 t_Foo) = resolve'1 _0

type t_FMap

type t_Option =
  | C_None
  | C_Some t

type t_Option'0 =
  | C_None'0
  | C_Some'0 t

function view t_FMap : int -> t_Option'0

axiom view_spec :
  forall m1:t_FMap, m2:t_FMap. not m1 = m2 -> not view m1 = view m2

function get_unsized (self1:t_FMap) (k:int) : t_Option'0 =
  get1 (view self1) k

function get (self1:t_FMap) (k:int) : t_Option =
  match get_unsized self1 k with
  | C_None'0 -> C_None
  | C_Some'0 x -> C_Some x
  end

function view'0 t_HashMap'0 : t_FMap

function view'1 (self1:t_Foo) : t_FMap = view'0 (self1.t_Foo__0)

constant self : t2 t_Foo

constant num : t1

constant bar : t

constant fin : t_HashMap

constant result : t2 t

Assert1 : resolve'0 (t'mk bar (result.final) (result.id))

Assert :
  resolve'2 (t'mk (t_Foo'mk (t_HashMap'0'mk fin)) (self.final) (self.id))

------------------------------- Goal --------------------------------

goal vc_add : get (view'1 (self.final)) (t'int1 num) = C_Some bar


====================> Prover: Z3 4.12.4
Timeout

The prover did not return counterexamples.

Command:

cargo creusot prove

Versions:

• creusot: 0.4.0
• Rust: 1.86.0

[jhjourdan]

Hi @janriemer, and think you for trying Creusot !

Unfortunately, we have not yet spend enough time in giving a formal specification to HashMap operations, which explains why your goal is not provable. The main difficulty here is to give the Hash trait a formal specification, which is both sound and not too tedious to use.

However, there should not be any fundamental difficulty here. You are welcome to contribute!

[xldenis]

Would it not be possible to sidestep the question of Hash if we only consider clients?

[jhjourdan]

That's unsound : if you don't give a spec to Hash, then any implementation would be considered correct.

But anyway the problem is the same: we need some manpower.

[xldenis]

That's unsound : if you don't give a spec to Hash, then any implementation would be considered correct.

Could we not somehow restrict ourselves to derived implementations of Hash using the stdlib derive (and trusting it)?

[jhjourdan]

That sounds like a big hack.

And frankly, that would require quite a lot of implementation effort, that would be as difficult as writing an actual spec for Hash.

[janriemer]

Unfortunately, we have not yet spend enough time in giving a formal specification to HashMap operations, which explains why your goal is not provable. The main difficulty here is to give the Hash trait a formal specification [...]

Oh, I see! Thank you for clearing things up for me.😊

You are welcome to contribute!

Thank you! Not sure, if I'm already competent enough for this, but I might have a look at other traits and their spec to see how it is done in general.👍

Thank you, both, for taking the time to answer and maintaining Creusot!❤

[jhjourdan]

(That being said, you are calling unspecified functions entry and or_insert, which should trigger a false verification condition. This does not happen, so this is a bug.