Show and Tell: SortingNetworkTools

Stream: general

[Michael MacLeod]

Hi everyone. I used Lean to make a suite of tools for evolving, verifying, and visualizing sorting networks. The tool can be found on GitHub (warning: alpha stage; expect some jank.)

Some Lean-specific highlights:

Lean InfoView Integration

The #network <network> command displays a visual representation of <network> in the Lean InfoView using the Widget API:

I think this is a really cool feature of Lean. It makes development a lot easier since it eliminates the need to manually stringify a network, copy it, paste it into an external visualization command, and then open the output of said command in an image viewer. Instead, you just move your cursor onto #network and immediately see it on the right-hand side.

Safe array accesses with no runtime bounds checking

Verifying if a network is correct involves completing 2ⁿ tests, where n is the size of the network. I use a technique for running these tests in parallel using bitwise operations, which requires evaluating array access expressions. Through liberal use of grind, I was able to eliminate all superfluous runtime bounds checks while writing only a couple proofs manually. Thank you to the people behind grind; this is a really great tactic!

... If only we had arrays of unboxed UInt64s: this would make the verification code more or less indistinguishable from an equivalent C/C++ version.

Stack-safe bottom-up tree folds

Converting a sorting network to an SVG (so it can be viewed, e.g., in the InfoView) involves a bottom-up fold on a SVG node tree. Naively implemented, such SVG to String code could lead to stack overflows if the SVG nodes are nested deep enough. To address this, I created a Trampoline type which stores would-be stack frames on the heap, so non-tail-recursive functions can be run with constant stack space. The fold itself is then implemented using a technique borrowed from the Haskell package recursion-schemes.

I searched through here and on the web for anyone else who had done something similar (i.e., implemented trampolines or something related to them), but I couldn't find anything. Are my search powers lacking? If there's an existing, similarly general solution for this, I'd love to hear about it.

[Alok Singh]

If you add a license and star it on github (I did), it will auto build on reservoir

[Michael MacLeod]

Thanks! It has a license, so it should eventually build on Reservoir. I think there's just some lag in Reservoir pulling from GitHub.

[Bryan Gin-ge Chen]

Note that a project also needs to have at least two stars to be included on Reservoir; I've also starred it so it should be picked up within a day or so.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

@Michael MacLeod regarding your Trampoline type, I think it's semi-common practice to make a function tail-recursive by describing the heap-allocated stack manually and then taking it as an additional argument. It might be nice to have general machinery for this, though.

[Michael MacLeod]

@𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒 Yeah, it's a lot nicer to have a general way of doing, e.g., bottom-up folds on tree structures that don't run the risk of stack overflows. Not having this is kind of like doing programming without map or fold (or imperitive programming without for loops), i.e., resorting to ad-hoc implementations every time one wishes to traverse a data structure in some way.

When it comes to implemening the general bottom-up fold function, I know of two approaches. The first is the way taken by the recursion-schemes Haskell package, where Haskell's laziness is exploited to achieve stack-safety while still encoding the traversal recursively. The second approach, followed by the recursion Rust crate, uses heap-allocated stacks (in the way you specified) and loops to implement the fold.

I actually tried to implement the second way first, that is, I thought that it would be better to write the generic bottom-up fold function via looping on heap-allocated stacks. But I ran into some performance issues, probably due to Nat-based indexing (technically avoidable in Lean) and/or boxed array elements (both of which are absent in Rust). Maybe these could have been somehow resolved. In the end, I decided to just rewrite the code in the Haskell style, with manually encoded laziness via the Trampoline type. This proved to be a lot simpler to implement and was much more efficient.