Implement Kirigami network partitioning in NV

[alberdingk-thijm]

This PR is to merge the implementation of Kirigami, an algorithm for partitioning an SRP and verifying properties modularly in each cut to approximate the full network behaviour.

High-level idea

Given user-provided partition and interface functions, Kirigami partitions the network following NV's transformation passes and before encoding. Each partition is then encoded as a separate SMT query and checked separately (currently queries are checked sequentially, but there is nothing stopping them from being run in parallel too). This transforms very large SMT queries over large networks into smaller SMT queries over subnetworks. Its central concept involves cutting edges across subnetworks and annotating them with sufficient information that the network can still be proven to satisfy the given properties.

The user-provided partition has type tnode -> int 32. It designates which partition each node belongs to. The user-provided interface has type tedge -> attribute -> bool. Given an edge between two nodes u and v such that partition u != partition v (the interface is only ever called on this subset of the graph's edges), the interface returns true if the given predicate applies to the solution sent from u to v.

Changes

• Adds many new examples for showcasing partitioning, and some other behaviours. New benchmarks have been added to demonstrate partitioning on fattrees. New assertions have been added in some benchmarks.
• Add two new utility functions to examples/utils.nv for sets: subset and disjoint.
• Add a directory of scripts, scripts/, to use for generating, running and managing partitioned benchmarks.
• Change nv_lang.Input.ml to allow (almost) arbitrary ordering of declarations in the NV file. Declarations will be topologically sorted when the file is parsed: if a topological sorting is not possible, then parsing will fail.
• Syntax.solve has an additional field, part, which optionally stores partitioning information from a partition datatype. partition contains the interface function and the decomposition decomp of the trans function across the base\~output virtual edge and the input\~base virtual edge. This information is allowed as optional fields to solution in NV:

  let sol = solution { init = init; trans = trans; merge = merge; interface = interface; rtrans = trans; }

  Either ltrans or rtrans can be given, or both, with a function with the type of trans. ltrans is applied on the base\~output virtual edge and rtrans is applied on the input\~base virtual edge.

• Solution.t has an additional field, guarantees, which lists the Kirigami guarantees that have been checked. Guarantees are generated during encoding: they are SMT constraints, like assertions, but apply specifically to the input and output solutions on nodes. Solutions also print the original node names when given partitioned networks, to help users understand the counterexamples in terms of the monolithic network.
• Add nv_kirigami library, which provides a means to partition the declarations (Partition.ml), a method for cutting nodes and edges across partitions and storing that information in a datatype partitioned_srp (SrpRemapping.ml), and a set of pseudo-transformations for remapping nodes and edges using the partitioned_srp and deleting cases from assertions over dropped nodes (TransformDecls.ml).
• Add three new commandline flags: -kirigami or -k to activate Kirigami features, -ranked to use Kirigami's ranked checker instead of the exact checker, and -print-partitions to print the declarations after partitioning.
• The code for Smt.ml now takes both a number representing the assertions and a number representing the guarantees. The ClassicSmtEncoding.ml module now describes how to encode a solution when given an accompanying partitioned_srp datatype, for use with SmtKirigami. kirigami_encode_z3 is now a function that an encoding must implement, which takes a partitioned_srp as an additional argument over encode_z3.
• SmtKirigami.ml describes how to encode a Kirigami-partitioned network to SMT, potentially in multiple passes if -ranked is set.
• Add a few new OCamlUtils: ostring for printing options, list_seq for converting a positive integer to a list up to that integer, and split3 which splits a list of three-tuples into a three-tuple of lists.

Limitations

• assert statements must be of the following form:

  let sol = solution { (* ... *) }
  let assert_node u v = (* some boolean statement *)
  assert foldNodes (fun u v acc -> acc && assert_node u v) sol true

  This is so that the statements can be divided across the partitions easily. Due to a ~kludge~ design feature, this does require this specific ordering of acc && assert_node u v. This may eventually be fixed more elegantly.

• Kirigami only succeeds if the user provides a correct interface. If the interface is incorrect (i.e., does not capture the network's behaviour), then NV will fail with a counterexample where the interface does not hold.
• That ltrans and rtrans compose to the equivalent of trans is not checked: users can implement badly-behaved decompositions without being stopped, but it's assumed they will not want to do anything too fancy.

[nickgian]

Tim I am assuming this does not break anything, such as the existing SMT or simulation backends, i.e., you can ignore Kirigami if you don't use the features it offers? If so, I'll just go ahead and merge this.

[alberdingk-thijm]

Yes, the Kirigami features are ignored if the user doesn't use the -kirigami or -ranked flags, which are only used for SMT: simulation is basically untouched.

There are of course some small changes in the existing non-Kirigami code to support the Kirigami features, namely:

• a new field in a few datatypes like Syntax.solve and Solution.t;
• new argument(s) to some SMT functions, with sensible defaults when Kirigami is not used; and
• topological sorting of declarations when parsing input files.

I can run the test suites for master and kirigami-2 side-by-side and compare the output if we want to double check that nothing else will break.

[nickgian]

That is ok, I am merging this.

[alberdingk-thijm]

Great! I just caught a small bug in the topological sorter for Input.ml. :sweat_smile: But it's pretty easy to correct, so I think I can do that now and then everything should work as before.