Star War Sex Parrot posted:

hell yeah check out the sweet invariants I wrote for my hash table

code:

  type hashtbl 'a = {
    mutable size: int ;
    mutable data: data 'a ;
    ghost mutable model: model 'a }

    invariant { length self.data > 0 }
    invariant {
      forall u:key. forall v:'a.
      mem (u, v) self.data[bucket u (length self.data)] <->
      Map.get self.model u = Some v }
    invariant {
      forall u:key. forall v:'a. forall w:'a.
      (mem (u,v) self.data[bucket u (length self.data)] /\
      mem (u,w) self.data[bucket u (length self.data)]) ->
      v = w }
    invariant {
      forall i: int. 0 <= i < length self.data ->
      forall u: key, v: 'a. mem (u,v) self.data[i] ->
      bucket u (length self.data) = i }

proving these during resize was sort of a bitch. this is the signature and contracts for a resize function whose body is like 6 lines

code:

    let rec rehash (new_data : data 'a) (l : bucket 'a) (ghost i : int) : unit =
      requires {
        forall j: int. 0 <= j < new_size ->
        forall u: key, v: 'a. mem (u,v) new_data[j] ->
        bucket u new_size = j }
      requires {
        forall u: key, v: 'a. mem (u,v) l ->
        bucket u old_size = i }
      requires {
        forall u:key. forall v:'a.
        0 <= bucket u old_size < i ->
        (mem (u, v) new_data[bucket u new_size] <->
        Map.get t.model u = Some v) }
      requires {
        forall u:key. forall v:'a.
        bucket u old_size = i ->
        (Map.get t.model u = Some v <-> mem (u, v) l \/
        (mem (u, v) new_data[bucket u new_size])) }
      requires {
        forall u:key. forall v:'a.
        bucket u old_size > i ->
        not (mem (u, v) new_data[bucket u new_size]) }
      requires { new_size = length new_data }
      ensures {
        forall j: int. 0 <= j < new_size ->
        forall u: key, v: 'a. mem (u,v) new_data[j] ->
        bucket u new_size = j }
      ensures {
        forall u:key. forall v:'a.
        0 <= bucket u old_size <= i ->
        (mem (u, v) new_data[bucket u new_size] <->
        Map.get t.model u = Some v) }
      ensures {
        forall u:key. forall v:'a.
        bucket u old_size > i ->
        not (mem (u, v) new_data[bucket u new_size]) }
      variant { l }