Keyval find specs

[plredmond]

Added specs for find to state that the return value i either refers to the correct index for the given key k, or refers to a value outside of the assigned indexes.

Test file test.ivy:

#lang ivy1.8

include collections

instance k : unbounded_sequence
instance v : unbounded_sequence
instance kv : keyval(index, k, v)

export kv.find

Test command:

$ ivy_check isolate=kv.iso test.ivy

Review request: @nano-o

• I've written the postcondition for find using implications to separate the two cases. I'm not sure if that's the right approach.

• Should I include assertions in the postcondition that the keyval structure is not changed? is assert s = old s enough, or do I need all of

    assert s.end = old s.end;                  
    assert s.key_at(I, K) = old s.key_at(I, K);
    assert s.value_at(I) = old s.value_at(I);