This issue is to track progress on handling node and edge maps in kirigami, which currently cause issues when we remap nodes and edges once an SRP is partitioned.

Background

NV allows a user to create a total map (associative array) data type where the keys of the map are nodes or edges. This can be useful for various purposes, e.g. tracking which edges or nodes a given solution considers or uses. Maps in NV are total: that is, they are functions that return a value if it is present, or a default value if it is not. For instance, a dict[tnode, bool] containing the nodes 0n and 2n would return false (as a default) if we asked if 3n was in the map (map[3n]).

For reasons I am not familiar with, we have to unroll the maps into tuples before passing them into Z3 (I assume they are not supported). To do so, we replace instances of types like dict[tnode, bool] with a tuple, where each expression or symbolic variable we use to access the map is converted into an index: see the code here.

As an example, suppose we have the following NV code (taken from map.nv):

include "utils.nv" (* defines mapbetter and mapo *)

type attribute = dict[tnode,option[int]]

let nodes = 2

let edges = {
  0=1;
}

let merge node x y = (* create a new dict using the minimum distance *)
  let f = mapbetter (fun x y -> if x < y then x else y) in
  combine f x y

let trans edge x = (* increase all map values by 1 *)
  map (fun x -> mapo (fun x -> x + 1) x) x

let init node = (* create a new dict with this node's distance as 0 *)
  let m = createDict None in
  match node with
  | 0n -> m[tnode := Some 0]
  | 1n -> m[tnode := Some 0]

Here, I have a map (called a dict in NV) which maps from nodes to option integers, and returns None if an integer is not found. The simulation solution will be:

Label(0):[1n:=Some(1u32),0n:=Some(0u32),default:=None]
Label(1):[1n:=Some(0u32),0n:=Some(1u32),default:=None]

Here is the network NV looks at after map unrolling:

type attribute = (option[int32],option[int32])

let nodes = 2

let edges = {1n-0n;0n-1n;}

let merge = fun node~78 -> fun x~79 -> fun y~80 -> (match (x~79,y~80) with
 |
((UnrollingMergeVar1~122,UnrollingMergeVar1~123),(UnrollingMergeVar2~120,UnrollingMergeVar2~121))
-> ((match (UnrollingMergeVar1~122,UnrollingMergeVar2~120) with
 | (None,x~68) -> x~68
 | (x~69,None) -> x~69
 | (Some x~70,Some y~71) -> Some(if x~70 <u32 y~71 then
x~70 else
y~71)
),(match (UnrollingMergeVar1~123,UnrollingMergeVar2~121) with
 | (None,x~68) -> x~68
 | (x~69,None) -> x~69
 | (Some x~70,Some y~71) -> Some(if x~70 <u32 y~71 then
x~70 else
y~71)
))
)

let trans = fun edge~74 -> fun x~75 -> (match x~75 with
 | (UnrollingMapVar~118,UnrollingMapVar~119) -> ((match
UnrollingMapVar~118 with
 | None -> None
 | Some x~63 -> Some(x~63 +u32 1u32)
),(match UnrollingMapVar~119 with
 | None -> None
 | Some x~63 -> Some(x~63 +u32 1u32)
))
)

let init = fun node~72 -> let m~73=(None,None) in
(match node~72 with
 | 0n -> (match node~72 with
 | 1n -> tuple2Set1-1(m~73,Some(0u32))
 | 0n -> tuple2Set0-0(m~73,Some(0u32))
)
 | 1n -> (match node~72 with
 | 1n -> tuple2Set1-1(m~73,Some(0u32))
 | 0n -> tuple2Set0-0(m~73,Some(0u32))
)
)

What's important to see here is that the attribute is now (option[int32], option[int32]). Hence, merge and trans now operate over UnrollingMapVars (the first and second elements of the tuple) and the init function sets a value in the tuple.

Where partitioning fails

Now, suppose I wanted to partition this network and compute the solutions separately.

First, the side containing 0n:

type attribute = dict[tnode, option[int]]

symbolic h_1_0 : dict[tnode, option[int]]

let nodes = 3 (* one new input node, one new output node *)

let edges = {0-1; 2-0;} (* 1 is the input, 2 is the output *)

let merge n x y = match n with
 | 1n -> x (* don't care what this is *)
 | 2n -> y (* use the solution sent to us; this is a hack and breaks
commutativity *)
 | 0n -> let f = mapbetter (fun x y -> if x < y then x else y) in
  combine f x y

let trans e x = match e with
 | 0-1 -> map (fun x -> mapo (fun x -> x + 1) x) x (* old trans *)
 | 2-0 -> x (* input-to-base does identity *)

let init n = match n with
 (* the base node: I've partially interpreted the expression *)
 | 0n -> let m = createDict None in m[0n := Some 0]
 (* the input node: use a symbolic variable *)
 | 1n -> h_1_0
 (* the output node: use the base node + trans, also a hack *)
 | 2n -> let m = createDict None in m[0n := Some 1]

This all seems fine. We don't have anything too weird going on here, although I haven't given any restrictions on h_1_0 yet. I did have to do something kind of ugly where (init 2n) needs to actually run (init 0n), but I have a separate solution under consideration to avoid that.

Now, let's see what map unrolling this program gives us.

type attribute = (option[int32],option[int32],option[int32])

symbolic h_1_0~62 : (option[int32],option[int32],option[int32])

let nodes = 3

let edges = {0n-2n;1n-0n;}

let merge = fun node~82 -> fun x~83 -> fun y~84 -> (match node~82 with
 | 1n -> x~83
 | 2n -> y~84
 | 0n -> (match (x~83,y~84) with (* ... *))

let trans = fun edge~78 -> fun x~79 -> (match edge~78 with
 | 0n~2n -> (match x~79 with (* ... *))
 | 1n~0n -> x~79
)

let init = fun node~75 -> (match node~75 with
 | 0n -> let m~76=(None,None,None) in
tuple3Set0-0(m~76,Some(0u32))
 | 1n -> h_1_0~62
 | 2n -> let m~77=(None,None,None) in
tuple3Set0-0(m~77,Some(1u32))
)

In the interest of space, I've chosen to hide some of what merge and trans get unrolled to this time. The important thing is we now have a different attribute from before! Our attribute type is now a 3-tuple of option[int32], where each index represents one of the nodes in this SRP, not the original SRP.

So first off, we no longer have the same attributes in both the original SRP and the partitioned SRP. Could this be a problem? Well, fortunately for us, we still have a node named 1n here, so we can actually write a require clause like this:

let pred x = x[1n] = Some 1
require (pred h_1_0)

This constrains h_1_0 to have Some 1 for the index representing the node 1n. This works, giving us the solution:

Label(0):[1n:=Some(1u32),0n:=Some(0u32),default:=None]

But it only works because there happened to be a node named 1n in the partitioned SRP. If instead we had this kind of network:

0 -- 1 -- 2 -- 3

And we cut the edge between 0n and 1n, then the NV program for the side containing 0n would look exactly the same, but we wouldn't be able to create a dictionary referring to node 3n. So, this code would fail:

let pred x = x[3n] = Some 3
require (pred h_1_0)

We get back the following error:

In examples/kirigami/map-a.nv:

5|  let pred x = x[3n] = Some 3
                   ~~

error: examples/kirigami/map-a.nv: Node 3 does not appear in the
network! (The highest node value is 2)

This is a wellformedness check, so we could see what happens when we just tell NV not to check the wellformedness of our program. I recently added a flag allowing us to do that (very bad, I know, but useful for testing this). I'll only show the part that causes problems:

type attribute = (option[int32],option[int32],option[int32])

symbolic h_1_0~67 : (option[int32],option[int32],option[int32])

(* uh oh! *)
require ((match 3n with
 | 2n -> tuple3Get2-2(h_1_0~67)
 | 1n -> tuple3Get1-1(h_1_0~67)
 | 0n -> tuple3Get0-0(h_1_0~67)
)) = Some(3u32)

let nodes = 3

let edges = {0n-2n;1n-0n;}

As you can see, 3n doesn't match any statement in the match pattern of require. The NV error we get back is:

error: internal error (encode_pattern): (0n, node)

Much less clear than before.

Essentially, what this means is that any maps over nodes or edges aren't going to work if we unroll them before partitioning. You might say, that doesn't seem so bad, let's just do map unrolling after partitioning. But then we have a different problem: just doing map unrolling takes longer in a partitioned network than verifying the original network! How can this be? I'm not quite sure, but @DKLoehr believes it's due to the implementation of map unrolling.

An alternative option is to use integers instead of nodes. If I replace type attribute = dict[tnode, option[int]] with type attribute = dict[int, option[int]], map unrolling produces this code:

type attribute = (option[int32],option[int32])

symbolic h_1_0~67 : (option[int32],option[int32])

require tuple2Get1-1(h_1_0~67) = Some(3u32)

Here, the requirement on node 3n (now just 3) was converted into index 1, since map unrolling only creates tuples to capture all of the integers we create in the program. As an aside, we explicitly forbid non-constant map keys with the exception of nodes and edges, so you wouldn't be able to write code that computes a new integer map key to add to the map forever.

What this basically means is that because maps of nodes and edges are typed based on the network topology, we can't refer to nodes outside the partition in our maps. This also prevents us from doing something like:

let init node =
 let m = createDict None in
 let k = node_to_key node in
 m[k := Some 0]

NV will complain during map unrolling:

Encountered non-variable, non constant map key whose type isn't node or edge: key~78

Now, at this point, I am inclined to ask, "Does checking for a node like 3n violate the whole premise of hiding information about one SRP's internals from another?" Well, perhaps that is true, in which case we'd prefer to simply require that our hypothesis only let us talk about the information we receive from our neighbour on the other side of the interface, i.e. for this network:

0 -/- 1 -- 2 -- 3

Our hypotheses should only be able to ask things about 0n and 1n, but not 2n or 3n. In that case, because each cut edge introduces an input node, we can successfully remap any tests on extrapartition nodes to tests on the input node. This introduces a new wrinkle for how we should rewrite code like this:

let assert node x =
  match node with
  | 0n -> x[1n] = 1 && x[2n] = 2 && x[3n] = 3
  | _ -> true

which is perfectly acceptable in the original network. Should it become:

let assert node x =
  match node with
  | 0n -> x[1n] = 1 (* remove all nodes we can't remap *)
  | _ -> true

One might like to know if the tests are bad to begin with, e.g.

let assert node x =
  match node with
  | 0n -> x[1n] = 1 && x[2n] = 15 && x[3n] = 200
  | _ -> true

For the topology above, this property is clearly false, but in order to determine that here, we would need to be able to recompute what values could be computed at 2n and 3n without seeing that part of the topology. My belief is that this type of case is one where we simply can't help the user in the partitioned world: if we want to be able to test these types of programs efficiently, having to compute a way to go from a query on the value for 2n and the value for 3n here would be isomorphic to computing queries on the global network.

Ways forward

As you can see, it's a tricky problem. Also to note is that currently, regardless of when map unrolling is performed, the code will still break if given this require clause on the 0n side:

require (h_1_0[3n] = Some 3)

Hence, I think there are a few ways to solve this issue:

Disallow maps with nodes or edges as keys when partitioning. This would mean users would have to use constants instead. We'd essentially be restricting what kinds of problems we can solve.
Remove all references (perhaps with a warning) to nodes or edges that we can no longer access after the network has been partitioned. There are possible implications to this that I haven't considered yet, and this is effectively also restricting what kinds of problems we can solve, but it fits with the logic that the partitioned networks shouldn't be reasoning about things they can't "see".
Make map unrolling respect partitioning and allow references to nodes and edges that were in the original SRP but not in the partitioned SRP. This could lead to more complicated code that may be slower to transform, but might also be the most intuitive. If it leads to additional slowness, that's something else we can look into fixing in the map unrolling code.

NetworkVerification / nv

Node and edge maps in kirigami #51

Background

Where partitioning fails

Ways forward