From 1440119c21b2d635521b74b4da4fd42212fe978f Mon Sep 17 00:00:00 2001
From: Michael Heuer <michael.heuer@rwth-aachen.de>
Date: Mon, 23 Sep 2024 16:27:41 +0200
Subject: [PATCH] refactor: use hash placeholder for IFC predicate

---
 Anoma/Resource/Index.juvix              |  2 +-
 Anoma/Transaction/InformationFlow.juvix | 39 ++++++++++++-------------
 2 files changed, 20 insertions(+), 21 deletions(-)

diff --git a/Anoma/Resource/Index.juvix b/Anoma/Resource/Index.juvix
index 13afff2..20a30e3 100644
--- a/Anoma/Resource/Index.juvix
+++ b/Anoma/Resource/Index.juvix
@@ -1,7 +1,7 @@
 module Anoma.Resource.Index;
 
 import Anoma.Resource.Types open using {Resource} public;
-import Anoma.Resource.Logic open using {Instance; Witness} public;
+import Anoma.Resource.Logic open using {Tag; Instance; Witness} public;
 import Anoma.Resource.Computable.Commitment open using {Commitment; commitment} public;
 import Anoma.Resource.Computable.Nullifier open using {Nullifier; NullifierKey; nullifier} public;
 import Anoma.Resource.Computable.Delta open using {delta} public;
diff --git a/Anoma/Transaction/InformationFlow.juvix b/Anoma/Transaction/InformationFlow.juvix
index 80cd3a4..b491f12 100644
--- a/Anoma/Transaction/InformationFlow.juvix
+++ b/Anoma/Transaction/InformationFlow.juvix
@@ -1,39 +1,38 @@
 module Anoma.Transaction.InformationFlow;
 
-import Stdlib.Prelude open using {Bool; List; true; false; all; any};
+import Stdlib.Prelude open using {Bool; List; true; false; all; any; not};
 import Data.Set as Set open using {Set; toList; member?};
-
-import Anoma.Identity open;
-import Anoma.Transaction.Types as Transaction open;
+import Anoma.Identity open using {ExternalIdentity};
+import Anoma.Transaction.Types as Transaction open using {Transaction};
 
 --- The information flow predicate function type definition.
 InformationFlowControlPredicate : Type := (tx : Transaction) -> (id : ExternalIdentity) -> Bool;
 
---- A fixed-size data type encoding a hash.
---- TODO: Is this type definition needed? Should this be Anoma.Resource.Logic.Tag?
-axiom Hash : Type;
+--- A placeholder for an unspecified hash type.
+--- NOTE: this will be concretized in an upcoming RM specs version.
+axiom HashPlaceholder : Type;
 
---- TODO This type is here to prevent the Juvix compiler from getting stuck in a loop in the type definition below.
-BaseDataSet : Type := Set BaseData;
+--- A placeholder for a function checking if a ;Transaction; does not include ;HashPlaceholder; ;Set;.
+--- NOTE: this will be concretized in an upcoming RM specs version.
+axiom requireShieldedCheckPlaceholder : (tx : Transaction)
+  -> (hashes : Set HashPlaceholder)
+  -> Bool;
 
 --- The input data of the basePredicate function.
 type BaseData :=
   | AllowAny
   | AllowOnly (Set ExternalIdentity)
-  | RequireShielded (Set Hash)
-  -- TODO Use ;Set; instead of ;List;
-  | And (BaseDataSet)
-  | Or (BaseDataSet);
-
+  | RequireShielded (Set HashPlaceholder)
+  -- TODO Use ;Set; instead of ;List; once https://github.com/anoma/juvix/issues/3048 is resolved.
+  | And (List BaseData)
+  | Or (List BaseData);
 
 --- Returns the ;InformationFlowControlPredicate; depending on the provided ;BaseData;.
 terminating
 basePredicate (baseData : BaseData) : InformationFlowControlPredicate :=
   case baseData of
-    | None := \ {_ _ := true}
+    | AllowAny := \ {_ _ := true}
     | AllowOnly identites := \ {_ self := member? self identites}
-    -- TODO How to handle the hashes?
-    -- | RequireShielded hashes := \ {tx _ := not (any (h in hashes) member? h ??)}
-    | RequireShielded hashes := \ {_ _ := false}
-    | And predicates := \ {tx id := all (p in Set.toList predicates) basePredicate p tx id}
-    | Or predicates := \ {tx id := any (p in Set.toList predicates) basePredicate p tx id};
+    | RequireShielded hashes := \ {tx _ := requireShieldedCheckPlaceholder tx hashes}
+    | And predicates := \ {tx id := all (p in predicates) basePredicate p tx id}
+    | Or predicates := \ {tx id := any (p in predicates) basePredicate p tx id};