From e1b471215b076f88d2614f2d877df4b18eb5abe7 Mon Sep 17 00:00:00 2001
From: Andy Jewell <ajewell@amazon.com>
Date: Thu, 26 Oct 2023 18:13:10 -0400
Subject: [PATCH] feat: remove recursion from FilterItems

---
 .../DynamoDbEncryption/src/FilterExpr.dfy      | 18 ++++++++----------
 1 file changed, 8 insertions(+), 10 deletions(-)

diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/FilterExpr.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/FilterExpr.dfy
index a84a119fa..2393d5ebe 100644
--- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/FilterExpr.dfy
+++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/FilterExpr.dfy
@@ -1429,17 +1429,15 @@ module DynamoDBFilterExpr {
     ensures b.ValidState()
     modifies b.Modifies()
   {
-    if |ItemList| == 0 {
-      return Success([]);
-    }
-    var newAttrs :- b.GeneratePlainBeacons(ItemList[0]);
-    var doesMatch :- EvalExpr(parsed, ItemList[0] + newAttrs, names, values);
-    var rest :- FilterItems(b, parsed, ItemList[1..], names, values);
-    if doesMatch {
-      return Success(ItemList[..1] + rest);
-    } else {
-      return Success(rest);
+    var acc : DDB.ItemList := [];
+    for i := 0 to |ItemList| {
+      var newAttrs :- b.GeneratePlainBeacons(ItemList[i]);
+      var doesMatch :- EvalExpr(parsed, ItemList[i] + newAttrs, names, values);
+      if doesMatch {
+        acc := acc + [ItemList[i]];
+      }
     }
+    return Success(acc);
   }
 
   // return the results for which the expression is true