From 7345329c83d0381a854045277103cb7116d4050c Mon Sep 17 00:00:00 2001
From: Bryan Parno <parno@cmu.edu>
Date: Thu, 16 Nov 2023 14:48:14 -0500
Subject: [PATCH] "Handle" macro_rules

---
 examples/wip.rs | 21 +++++++++++++++++++--
 src/lib.rs      |  2 +-
 2 files changed, 20 insertions(+), 3 deletions(-)

diff --git a/examples/wip.rs b/examples/wip.rs
index 0302fe9..2707203 100644
--- a/examples/wip.rs
+++ b/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!
diff --git a/src/lib.rs b/src/lib.rs
index 95c761d..6de9626 100644
--- a/src/lib.rs
+++ b/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),