"Handle" macro_rules

examples/wip.rs

@@ -1,7 +1,24 @@
 verus! {
 
-trait KeyTrait: Sized {
-    fn zero_spec() -> Self where Self: std::marker::Sized;
+#[allow(unused_macros)]
+macro_rules! no_usize_overflows {
+  ($e:expr,) => {
+    true
+  };
+  ($($e:expr),*) => {
+    no_usize_overflows!(@@internal 0, $($e),*)
+  };
+  (@@internal $total:expr,) => {
+    true
+  };
+  (@@internal $total:expr, $a:expr) => {
+    usize::MAX - $total >= $a
+  };
+  (@@internal $total:expr, $a:expr, $($rest:expr),*) => {
+    usize::MAX - $total >= $a
+      &&
+    no_usize_overflows!(@@internal ($total + $a), $($rest),*)
+  };
 }
 
 } // verus!

src/lib.rs

@@ -575,7 +575,7 @@ fn to_doc<'a>(
         //          Items          //
         //*************************//
         Rule::item => map_to_doc(ctx, arena, pair),
-        Rule::macro_rules => unsupported(pair),
+        Rule::macro_rules => s, // Don't attempt to format macro rules
         Rule::macro_def => unsupported(pair),
         Rule::module => unsupported(pair),
         Rule::item_list => unsupported(pair),