Bunched Fuzz: Sensitivity for Vector Metrics

To appearInternational audienceProgram sensitivity measures the distance between the outputs of a program when it is run on tworelated inputs. This notion, which plays an important role in areas such as data privacy and optimization,has been the focus of several program analysis techniques introduced in recent years. One approach thathas proved particularly fruitful for this domain is the use of type systems inspired by linear logic, aspioneered by Reed and Pierce in the Fuzz programming language. In Fuzz, each type is equipped withits own notion of distance, and the typing rules explain how those distances can be treated soundly whenanalyzing the sensitivity of a program. In particular, Fuzz features two products types, correspondingto two different sensitivity analyses: the tensor product combines the distances of each component byadding them, while the with product takes their maximum.In this work, we show that products in Fuzz can be generalized to arbitrary Lp distances, metricsthat are often used in privacy and optimization. The original Fuzz products, tensor and with, correspondto the special cases L1 and L∞ . To simplify the handling of such products, we extend the Fuzz typesystem with bunches—as in the logic of bunched implications—where the distances of different groupsof variables can be combined using different Lp distances. We show that our extension can be naturallyused to reason about important metrics between probability distributions