Added starter code for formal verification of parts of pseudoplanarity.js.

formal_verification/find_pseudoface.dfy

+// Prove that if `findPseudoface` from `pseudoplanarity.js` does not return `undefined`, then it returns a pseudoface built from a cycle.
+
+include "prelude.dfy"
+
+method find_pseudoface(indexing: map<Vertex, nat>, rotation_system: RotationSystem, edge: Edge) returns (result: Pseudoface)
+  requires has_adjacency(get_graph(rotation_system), get_source(edge), get_destination(edge))
+  ensures result != undefined() ==>
+    |get_vertices(result)| > 2
+  ensures
+    result != undefined() ==>
+    forall i | i in range(0, |get_vertices(result)| - 1) ::
+    has_adjacency(get_graph(rotation_system), get_vertices(result)[i], get_vertices(result)[i + 1])
+  ensures
+    result != undefined() ==>
+    has_adjacency(get_graph(rotation_system), top(get_vertices(result), 0), get_vertices(result)[0])
+  decreases *
+{
+  return undefined(); // TODO
+}

formal_verification/index_vertices.dfy

+// Prove that `indexVertices` from `pseudoplanarity.js` maps distinct keys to distinct values.
+
+include "prelude.dfy"
+
+method index_vertices(graph: Graph) returns (indexing: map<Vertex, nat>)
+  requires
+    forall i | i in range(0, |get_vertices(graph)|) ::
+    forall j | j in range(0, |get_vertices(graph)|) && i != j ::
+    get_vertices(graph)[i] != get_vertices(graph)[j]
+  ensures
+    forall key | key in indexing ::
+    forall other_key | other_key in indexing && other_key != key ::
+    indexing[key] != indexing[other_key]
+{
+  var result: map<Vertex, nat> := map[];
+  return result; // TODO
+}

formal_verification/prelude.dfy

+// This file provides various Dafny helper functions for the verification of code from pseudoplanarity.js.
+
+// Returns the equivalent to JavaScript's `undefined`.
+function method undefined<T>(): T
+
+// Returns the set of integers between `low` (inclusive) and `high` (exclusive).
+// (For use in specifications only.)
+function range(low: int, high: int): set<int>
+  ensures forall i | low <= i < high :: i in range(low, high)
+  ensures forall i | i in range(low, high) :: low <= i < high
+
+// Returns the same as `range(low, high)`, but with every element reduced modulo `length`.
+// For example:
+//   range(3, 8)            == {3, 4, 5, 6, 7}
+//   wrapped_range(3, 8, 6) == {3, 4, 5, 0, 1}
+// (For use in specifications only.)
+function wrapped_range(low: nat, high: nat, length: nat): set<int>
+  ensures forall i | low <= i < high && i < length :: i in wrapped_range(low, high, length)
+  ensures forall i | 0 <= i < high - length :: i in wrapped_range(low, high, length)
+  ensures forall i | i in wrapped_range(low, high, length) :: 0 <= i < length
+  ensures forall i | i in wrapped_range(low, high, length) :: (low <= i < high && i < length) || (0 <= i < high - length)
+
+// Return the ith element from the end of a list.
+function method top<T>(list: seq<T>, i: nat): T
+  requires |list| > i
+  ensures top(list, i) == list[|list| - i - 1]
+
+// Return a list with its last element removed.
+function method popped<T>(stack: seq<T>): seq<T>
+  requires |stack| > 0
+  ensures popped(stack) == stack[..|stack| - 1]
+
+// Returns the set of values in a map.
+function method values<K, V>(mapping: map<K, V>): set<V> {
+  set key | key in mapping :: mapping[key]
+}
+
+// Return a copy of a map with `new_key` mapped to `new_value`.
+// (For use in imperative code only.)
+method update<K, V>(mapping: map<K, V>, new_key: K, new_value: V) returns (result: map<K, V>)
+  ensures result == mapping[new_key := new_value];
+  ensures forall key | key in mapping :: key in result
+  ensures new_key !in mapping ==> forall key | key in mapping :: result[key] == mapping[key]
+  ensures new_key in result
+  ensures result[new_key] == new_value
+  ensures new_key !in mapping ==> values(result) == values(mapping) + {new_value}
+{
+  return mapping[new_key := new_value];
+}
+
+// Various graph-related types, all of which support equality comparisons:
+type Vertex(==)
+type Edge(==)
+type Pseudoface(==)
+type Graph(==)
+type RotationSystem(==)
+
+// Get an edge's source vertex.
+function method get_source(edge: Edge): Vertex
+
+// Get an edge's destination vertex.
+function method get_destination(edge: Edge): Vertex
+
+// Get all of the edges in a pseudoface or a graph.
+function method get_vertices<T>(graphlike_object: T): seq<Vertex>
+
+// Create a Pseudoface from a vertex list and an indexing.
+function method create_pseudoface(vertices: seq<Vertex>, indexing: map<Vertex, nat>): Pseudoface
+  ensures get_vertices(create_pseudoface(vertices, indexing)) == vertices
+
+// Compute a hash code from a list of vertices.
+function method hash(vertices: seq<Vertex>): int
+
+// Get the hash code of a pseudoface.
+function method get_hash_code(pseudoface: Pseudoface): int {
+  hash(get_vertices(pseudoface))
+}
+
+// Test whether two vertices are adjacent in a graph.
+function method has_adjacency(graph: Graph, source: Vertex, destination: Vertex): bool
+
+// Recover a graph from its rotation system.
+function method get_graph(rotation_system: RotationSystem): Graph
+
+// Get the neighbor of `vertex` that comes after `neighbor` according to `rotation_system`.
+function method get_next_neighbor(rotation_system: RotationSystem, vertex: Vertex, neighbor: Vertex): Vertex
+  ensures has_adjacency(get_graph(rotation_system), vertex, get_next_neighbor(rotation_system, vertex, neighbor))
+  ensures has_adjacency(get_graph(rotation_system), get_next_neighbor(rotation_system, vertex, neighbor), vertex)

formal_verification/pseudoface_equals.dfy

+// Prove that the `equals` method from `pseudoplanarity.js` tests whether two pseudofaces have the same vertex lists.
+
+include "prelude.dfy"
+
+method equals(self: Pseudoface, other: Pseudoface) returns (result: bool)
+  ensures result <==> get_vertices(self) == get_vertices(other)
+{
+  return true; // TODO
+}

formal_verification/rotation_system_keys.dfy

+// Prove that the inner loop of the `RotationSystem` constructor from `pseudoplanarity.js` makes every neighbor into a map key.
+
+include "prelude.dfy"
+
+method find_successors(neighbors: seq<Vertex>) returns (result: map<Vertex, Vertex>)
+  requires |neighbors| > 0
+  requires
+    forall i | i in range(0, |neighbors|) ::
+    forall j | j in range(0, |neighbors|) && i != j ::
+    neighbors[i] != neighbors[j]
+  ensures
+    forall i | i in range(0, |neighbors|) ::
+    neighbors[i] in result
+{
+  var successors: map<Vertex, Vertex> := map[];
+  return successors; // TODO
+}

formal_verification/rotation_system_values.dfy

+// Prove that the inner loop of the `RotationSystem` constructor from `pseudoplanarity.js` makes every neighbor into a map value.
+
+include "prelude.dfy"
+
+method find_successors(neighbors: seq<Vertex>) returns (result: map<Vertex, Vertex>)
+  requires |neighbors| > 0
+  requires
+    forall i | i in range(0, |neighbors|) ::
+    forall j | j in range(0, |neighbors|) && i != j ::
+    neighbors[i] != neighbors[j]
+  ensures
+    forall i | i in range(0, |neighbors|) ::
+    neighbors[i] in values(result)
+{
+  var successors: map<Vertex, Vertex> := map[];
+  return successors; // TODO
+}