From 743927b743a070920f58fae4438fd545f671ef7f Mon Sep 17 00:00:00 2001
From: Emina Torlak <torlaket@amazon.com>
Date: Thu, 8 Feb 2024 21:01:34 -0800
Subject: [PATCH] Implement efficient wildcard matching (closes #173).

---
 cedar-lean/Cedar/Spec/Wildcard.lean | 69 ++++++++++++++++++-----------
 cedar-lean/UnitTest/Main.lean       |  8 +++-
 cedar-lean/UnitTest/Wildcard.lean   | 61 +++++++++++++++++++++++++
 3 files changed, 112 insertions(+), 26 deletions(-)
 create mode 100644 cedar-lean/UnitTest/Wildcard.lean

diff --git a/cedar-lean/Cedar/Spec/Wildcard.lean b/cedar-lean/Cedar/Spec/Wildcard.lean
index 8fcad98d5..fbeae32b0 100644
--- a/cedar-lean/Cedar/Spec/Wildcard.lean
+++ b/cedar-lean/Cedar/Spec/Wildcard.lean
@@ -14,38 +14,17 @@
  limitations under the License.
 -/
 
+import Std
+
 namespace Cedar.Spec
 
+open Std
+
 inductive PatElem where
   | star
   | justChar (c : Char)
 deriving Repr, DecidableEq, Inhabited
 
-abbrev Pattern := List PatElem
-
-def charMatch (textChar : Char) (patternChar : PatElem) : Bool :=
-  match patternChar with
-  | .justChar c => textChar == c
-  | _ => false
-
-def wildcard (patternChar : PatElem) : Bool :=
-  match patternChar with
-  | .star => true
-  | _ => false
-
-def wildcardMatch (text : String) (pattern : Pattern) : Bool :=
-  match pattern with
-  | [] => match text with
-    | .mk [] => true
-    | _ => false
-  | p::ps => match text with
-    | .mk [] => wildcard p && wildcardMatch (.mk []) ps
-    | .mk (c::cs) => match wildcard p with
-      | true => wildcardMatch (.mk (c::cs)) ps || wildcardMatch (.mk cs) (p::ps)
-      | false => charMatch c p && wildcardMatch (.mk cs) ps
-  termination_by
-    wildcardMatch text pattern => sizeOf text + sizeOf pattern
-
 def PatElem.lt : PatElem → PatElem → Bool
   | .justChar c₁, .justChar c₂ => c₁ < c₂
   | .star, .justChar _         => true
@@ -57,5 +36,45 @@ instance : LT PatElem where
 instance PatElem.decLt (x y : PatElem) : Decidable (x < y) :=
   if  h : PatElem.lt x y then isTrue h else isFalse h
 
+abbrev Pattern := List PatElem
+
+def charMatch (textChar : Char) : PatElem → Bool
+  | .justChar c => textChar == c
+  | _           => false
+
+def wildcard : PatElem → Bool
+  | .star => true
+  | _     => false
+
+abbrev Cache := HashMap (Nat × Nat) Bool
+
+abbrev CacheM (α) := StateM Cache α
+
+def wildcardMatchIdx (text : List Char) (pattern : Pattern) (i j : Nat)
+  (h₁ : i ≤ text.length)
+  (h₂ : j ≤ pattern.length) : CacheM Bool
+:= do
+  if let .some b := (← get).find? (i, j) then
+    return b
+  let mut r := false
+  if h₃ : j = pattern.length then
+    r := i = text.length
+  else if h₄ : i = text.length then
+    r := wildcard (pattern.get ⟨j, (by omega)⟩) &&
+         (← wildcardMatchIdx text pattern i (j + 1) h₁ (by omega))
+  else if wildcard (pattern.get ⟨j, (by omega)⟩) then
+    r := (← wildcardMatchIdx text pattern i (j + 1) h₁ (by omega)) ||
+         (← wildcardMatchIdx text pattern (i + 1) j (by omega) h₂)
+  else
+    r := charMatch (text.get ⟨i, (by omega)⟩) (pattern.get ⟨j, (by omega)⟩) &&
+         (← wildcardMatchIdx text pattern (i + 1) (j + 1) (by omega) (by omega))
+  modifyGet λ cache => (r, cache.insert (i, j) r)
+termination_by
+  wildcardMatchIdx text pattern i j _ _=> (text.length - i) + (pattern.length - j)
+decreasing_by
+  all_goals { simp_wf ; omega }
+
+def wildcardMatch (text : String) (pattern : Pattern) : Bool :=
+  wildcardMatchIdx text.toList pattern 0 0 (by simp) (by simp) |>.run' HashMap.empty
 
 end Cedar.Spec
diff --git a/cedar-lean/UnitTest/Main.lean b/cedar-lean/UnitTest/Main.lean
index 1b732260c..26c5ba937 100644
--- a/cedar-lean/UnitTest/Main.lean
+++ b/cedar-lean/UnitTest/Main.lean
@@ -16,8 +16,14 @@
 
 import UnitTest.Decimal
 import UnitTest.IPAddr
+import UnitTest.Wildcard
 
 open UnitTest
 
+def tests :=
+  Decimal.tests ++
+  IPAddr.tests ++
+  Wildcard.tests
+
 def main : IO UInt32 := do
-  TestSuite.runAll (Decimal.tests ++ IPAddr.tests)
+  TestSuite.runAll tests
diff --git a/cedar-lean/UnitTest/Wildcard.lean b/cedar-lean/UnitTest/Wildcard.lean
new file mode 100644
index 000000000..370a2e6b2
--- /dev/null
+++ b/cedar-lean/UnitTest/Wildcard.lean
@@ -0,0 +1,61 @@
+/-
+ Copyright 2022-2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+
+ Licensed under the Apache License, Version 2.0 (the "License");
+ you may not use this file except in compliance with the License.
+ You may obtain a copy of the License at
+
+      https://www.apache.org/licenses/LICENSE-2.0
+
+ Unless required by applicable law or agreed to in writing, software
+ distributed under the License is distributed on an "AS IS" BASIS,
+ WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ See the License for the specific language governing permissions and
+ limitations under the License.
+-/
+
+import Cedar.Spec.Wildcard
+import UnitTest.Run
+
+/-! This file defines unit tests for the wildcard matching functions. -/
+
+namespace UnitTest.Wildcard
+
+open Cedar.Spec
+
+private def testWildcardMatch (str : String) (pat : Pattern) (expected : Bool) : TestCase :=
+  test s!"{expected}: {str} like {reprStr pat}" (checkEq (wildcardMatch str pat) expected)
+
+private def justChars : String → Pattern
+  | .mk [] => []
+  | .mk (c::cs) => (.justChar c) :: (justChars (.mk cs))
+
+def testsForWildcardMatch :=
+  suite "wildcardMatch"
+  [
+    testWildcardMatch "" [] true,
+    testWildcardMatch "a" [] false,
+    testWildcardMatch "a" [.justChar 'a'] true,
+    testWildcardMatch "" [.star] true,
+    testWildcardMatch "a" [.star] true,
+    testWildcardMatch "abababa" (justChars "abababa") true,
+    testWildcardMatch "abababa" [.star] true,
+    testWildcardMatch "abababa" ([.star] ++ (justChars "aba")) true,
+    testWildcardMatch "abababa" ((justChars "aba") ++ [.star]) true,
+    testWildcardMatch "abababa" ([.star] ++ (justChars "aba") ++ [.star]) true,
+    testWildcardMatch "abababa" [.justChar 'a', .star] true,
+    testWildcardMatch "abababa" [.justChar 'a', .star, .justChar 'b'] false,
+    testWildcardMatch "abababa" [.star, .justChar 'a', .star, .star, .justChar 'b', .star, .star,.justChar 'b', .star] true,
+    testWildcardMatch "abababa" [.star, .justChar 'a', .star, .star, .justChar 'b', .star, .star,.justChar 'b'] false,
+    testWildcardMatch
+      "ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff"
+      [.star, .star, .star, .star, .star, .justChar '\\', .justChar '0', .justChar '\\', .justChar '0', .star]
+      false
+  ]
+
+def tests := [ testsForWildcardMatch  ]
+
+-- Uncomment for interactive debugging
+-- #eval TestSuite.runAll tests
+
+end UnitTest.Wildcard