Rocket/core/lib/fuzz/corpus/collision-matching
Sergio Benitez 908a918e8b Fuzz to validate routing collision safety.
The fuzzing target introduced in this commit attemps to assert
"collision safety". Formally, this is the property that:

  matches(request, route) := request is matched to route
  collides(route1, route2) := there is a a collision between routes

  forall requests req. !exist routes r1, r2 s.t.
    matches(req, r1) AND matches(req, r2) AND not collides(r1, r2)

Alternatively:

  forall requests req, routes r1, r2.
    matches(req, r1) AND matches(req, r2) => collides(r1, r2)

The target was run for 20 CPU hours without failure.
2023-04-07 20:27:56 -07:00
..
another.seed Fuzz to validate routing collision safety. 2023-04-07 20:27:56 -07:00
base.seed Fuzz to validate routing collision safety. 2023-04-07 20:27:56 -07:00
complex.seed Fuzz to validate routing collision safety. 2023-04-07 20:27:56 -07:00
large.seed Fuzz to validate routing collision safety. 2023-04-07 20:27:56 -07:00