Remove is-principal and typeof-principal, create-principal, and validate-principal shim

docs/en/pact-properties-api.md

@@ -635,6 +635,21 @@ List / string / object contains
 
 Supported in either invariants or properties.
 
+### enumerate {#FEnumerate}
+
+```lisp
+(drop n xs)
+```
+
+* takes `from`: `integer`
+* takes `to`: `integer`
+* takes `step`: `integer`
+* produces [`integer`]
+
+Returns a sequence of numbers as a list
+
+Supported in either invariants or properties.
+
 ### reverse {#FReverse}
 
 ```lisp
@@ -1181,6 +1196,32 @@ Whether the keyset in the row is enforced by the function under analysis
 
 Supported in properties only.
 
+### is-principal {#FIsPrincipal}
+
+```lisp
+(is-principal s)
+```
+
+* takes `s`: `string`
+* produces `bool`
+
+Whether `s` conforms to the principal format without proving validity
+
+Supported in either invariants or properties.
+
+### typeof-principal {#FTypeOfPrincipal}
+
+```lisp
+(typeof-principal s)
+```
+
+* takes `s`: `string`
+* produces `string`
+
+Return the protocol type of the given `s` value. If input value is not a principal type, then the empty string is returned.
+
+Supported in either invariants or properties.
+
 ## Function operators {#Function}
 
 ### identity {#FIdentity}

src-tool/Pact/Analyze/Eval/Core.hs

@@ -8,6 +8,8 @@
 {-# LANGUAGE TypeApplications    #-}
 {-# LANGUAGE TypeOperators       #-}
 {-# options_ghc -fno-warn-redundant-constraints #-}
+{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
+{-# HLINT ignore "Redundant <&>" #-}
 
 -- | Symbolic evaluation for the functionally pure subset of expressions that
 -- are shared by all three languages: 'Term', 'Prop', and 'Invariant'.
@@ -39,6 +41,11 @@ import           Pact.Analyze.Types.Eval
 import           Pact.Analyze.Util           (Boolean (..), vacuousMatch)
 import qualified Pact.Native                 as Pact
 import           Pact.Types.Pretty           (renderCompactString)
+import Data.Attoparsec.Text (parseOnly)
+import Pact.Types.Principal (principalParser, showPrincipalType)
+import Pact.Types.Info (Info(..))
+
+import Data.Functor ((<&>))
 
 -- | Bound on the size of lists we check. This may be user-configurable in the
 -- future.
@@ -407,6 +414,21 @@ evalCore (ObjTake argTy _keys obj) = withSing argTy $ do
 evalCore (ObjLength (SObjectUnsafe (SingList hlist)) _obj) = pure $ literalS $
   hListLength hlist
 
+evalCore (IsPrincipal p) = do
+  p' <- eval p
+  case unliteralS p' of
+    Nothing -> let (S _ str) = coerceS @Str @String p'
+               in pure $ sansProv (literal "internal-principal-" `SBVS.isPrefixOf` str)
+    Just (Str str) ->case parseOnly (principalParser (Info Nothing)) (T.pack str) of
+      Left _ -> pure (literalS sFalse)
+      Right _ -> pure (literalS sTrue)
+
+evalCore (TypeOfPrincipal p) =eval p <&> unliteralS >>= \case
+  Nothing -> throwErrorNoLoc (FailureMessage "`typeof-principal` requires statically known content")
+  Just (Str str) ->case parseOnly (principalParser (Info Nothing)) (T.pack str) of
+    Left _ -> pure (literalS "")
+    Right pt -> pure (literalS (Str (T.unpack (showPrincipalType pt))))
+
 -- | Implementation for both drop and take. The "sub" schema must be a sub-list
 -- of the "sup(er)" schema. See 'subObjectS' for a variant that works over 'S'.
 subObject

src-tool/Pact/Analyze/Eval/Term.hs

@@ -839,6 +839,26 @@ evalTerm = \case
         tagResume tid $ mkAVal' $ SBV.fromJust mVal
         pure $ S prov $ SBV.fromJust mVal
 
+  CreatePrincipal g -> do
+    guard <- evalTerm g
+    let
+      (S _ iGuard) = coerceS @Guard @Integer guard
+      sGuard = SBV.natToStr iGuard
+      prefix = literal "internal-principal-"
+      guardStr = SBV.concat prefix sGuard
+    pure $ coerceS @String @Str (sansProv guardStr)
+
+  ValidatePrincipal g s -> do
+    guard    <- evalTerm g
+    S _ guardStr <- evalTerm s
+    let
+      (S _ iGuard) = coerceS @Guard @Integer guard
+      sGuard = SBV.natToStr iGuard
+      prefix = literal "internal-principal-"
+      S _ guardStr' = coerceS @String @Str (sansProv (SBV.concat prefix sGuard))
+    pure $ sansProv (guardStr .== guardStr')
+
+
 -- | Private pacts must be evaluated by the right entity. Fail if the current
 -- entity doesn't match the provided.
 evalTermWithEntity

src-tool/Pact/Analyze/Feature.hs

@@ -160,6 +160,9 @@ data Feature
   -- Other
   | FWhere
   | FTypeof
+  -- Principals
+  | FIsPrincipal
+  | FTypeOfPrincipal
   deriving (Eq, Ord, Show, Bounded, Enum)
 
 data Availability
@@ -1685,6 +1688,33 @@ doc FTypeof = Doc
         (TyCon str)
   ]
 
+-- Principals
+doc FIsPrincipal = Doc
+  "is-principal"
+  CAuthorization
+  InvAndProp
+  "Whether `s` conforms to the principal format without proving validity"
+  [ Usage "(is-principal s)"
+    Map.empty
+    $ Fun
+    Nothing
+    [ ("s", TyCon str)
+    ]
+    (TyCon bool)
+  ]
+doc FTypeOfPrincipal = Doc
+  "typeof-principal"
+  CAuthorization
+  InvAndProp
+  "Return the protocol type of the given `s` value. If input value is not a principal type, then the empty string is returned."
+  [ Usage "(typeof-principal s)"
+    Map.empty
+    $ Fun
+    Nothing
+    [ ("s", TyCon str)
+    ]
+    (TyCon str)
+  ]
 allFeatures :: Set Feature
 allFeatures = Set.fromList $ enumFrom minBound
 
@@ -1799,6 +1829,8 @@ PAT(SConstantly, FConstantly)
 PAT(SCompose, FCompose)
 PAT(SWhere, FWhere)
 PAT(STypeof, FTypeof)
+PAT(SIsPrincipal, FIsPrincipal)
+PAT(STypeOfPrincipal, FTypeOfPrincipal)
 
 -- 'Text'/op prisms
 

src-tool/Pact/Analyze/Parse/Prop.hs

@@ -405,6 +405,20 @@ inferPreProp preProp = case preProp of
           [from, to, step] -> pure $ Some (SList SInteger) $ CoreProp $ Enumerate from to step
           _otherwise -> throwErrorIn preProp "expected 2 or 3 integer arguments"
 
+  PreApp s [arg]
+    | s == SIsPrincipal -> do
+        arg' <- inferPreProp arg
+        case arg' of
+          Some SStr str -> pure $ Some SBool $ CoreProp $ IsPrincipal str
+          _otherwise -> throwErrorIn preProp "expected string argument"
+
+  PreApp s [arg]
+    | s == STypeOfPrincipal -> do
+        arg' <- inferPreProp arg
+        case arg' of
+          Some SStr str -> pure $ Some SStr $ CoreProp $ TypeOfPrincipal str
+          _otherwise -> throwErrorIn preProp "expected string argument"
+
   PreApp s [arg] | s == SStringLength -> do
     arg' <- inferPreProp arg
     case arg' of

src-tool/Pact/Analyze/Patterns.hs

@@ -102,6 +102,14 @@ pattern AST_CreateCapabilityPactGuard :: AST Node -> AST Node
 pattern AST_CreateCapabilityPactGuard app <-
   App _node (NativeFunc "create-capability-pact-guard") [app]
 
+pattern AST_CreatePrincipal :: forall a. AST a -> AST a
+pattern AST_CreatePrincipal guard <-
+  App _node (NativeFunc "create-principal") [guard]
+
+pattern AST_ValidatePrincipal :: forall a. AST a -> AST a -> AST a
+pattern AST_ValidatePrincipal guard name <-
+  App _node (NativeFunc "validate-principal") [guard, name]
+
 pattern AST_Enforce :: forall a. a -> AST a -> AST a
 pattern AST_Enforce node cond <-
   App node (NativeFunc "enforce") (cond:_rest)

src-tool/Pact/Analyze/PrenexNormalize.hs

@@ -191,7 +191,10 @@ singFloat ty p = case p of
   CoreProp ObjMerge{}      -> ([], p)
   CoreProp (Where objty tya a b c) -> CoreProp <$>
     (Where objty tya <$> float a <*> floatOpen b <*> singFloat objty c)
-
+  CoreProp (IsPrincipal a) -> CoreProp <$>
+    (IsPrincipal <$> float a)
+  CoreProp (TypeOfPrincipal a) -> CoreProp <$>
+    (TypeOfPrincipal <$> float a)
   where
 
     floatOpen :: SingI b => Open a Prop b -> ([Quantifier], Open a Prop b)

src-tool/Pact/Analyze/Translate.hs

@@ -1728,27 +1728,23 @@ translateNode astNode = withAstContext astNode $ case astNode of
     Some SStr _ -> shimNative' node fn [b] "format string" a'
     _ -> unexpectedNode astNode
 
-  AST_NFun node fn@"create-principal" [a] -> translateNode a >>= \case
-    -- assuming we have a guard as input, yield an empty string
-    Some SGuard _ -> shimNative astNode node fn []
+  AST_CreatePrincipal guard -> translateNode guard >>= \case
+    Some SGuard g -> pure (Some SStr (CreatePrincipal g))
     _ -> unexpectedNode astNode
 
-  AST_NFun node fn@"validate-principal" [a, b] -> translateNode a >>= \case
-    -- term check inputs and produce an empty string
-    Some SGuard _ -> translateNode b >>= \case
-      Some SStr _ -> shimNative astNode node fn []
+  AST_ValidatePrincipal guard name -> translateNode guard >>= \case
+    Some SGuard g -> translateNode name >>= \case
+      Some SStr s -> pure $ Some SBool (ValidatePrincipal g s)
       _ -> unexpectedNode astNode
     _ -> unexpectedNode astNode
 
-  AST_NFun node fn@"is-principal" [a] -> translateNode a >>= \case
-    -- assuming we have a principal string as input, yield true
-    Some SStr _ -> shimNative astNode node fn []
-    _ -> unexpectedNode astNode
+  AST_NFun _ "is-principal" [a] -> translateNode a >>= \xs' -> case xs' of
+    Some SStr l -> pure $ Some SBool $ CoreTerm $ IsPrincipal l
+    _otherwise -> unexpectedNode astNode
 
-  AST_NFun node fn@"typeof-principal" [a] -> translateNode a >>= \a' -> case a' of
-    -- assuming we have a principal string as input, yield empty string
-    Some SStr _ -> shimNative' node fn [] "principal" a'
-    _ -> unexpectedNode astNode
+  AST_NFun _ "typeof-principal" [a] -> translateNode a >>= \xs' -> case xs' of
+    Some SStr l -> pure $ Some SStr $ CoreTerm $ TypeOfPrincipal l
+    _otherwise -> unexpectedNode astNode
 
   AST_NFun _ fn@"describe-namespace" _ ->
     throwError' (InvalidNativeInModule fn)

src-tool/Pact/Analyze/Types/Languages.hs

@@ -307,6 +307,9 @@ data Core (t :: Ty -> K.Type) (a :: Ty) where
 
   Typeof :: SingTy a -> t a -> Core t 'TyStr
 
+  IsPrincipal     :: t 'TyStr -> Core t 'TyBool
+  TypeOfPrincipal :: t 'TyStr -> Core t 'TyStr
+
 mkLiteralObject
   :: (IsTerm tm, Monad m)
   => (forall a. String -> Existential (Core tm) -> m a)
@@ -689,6 +692,11 @@ eqCoreTm _ (Typeof ty1 a1) (Typeof ty2 a2)
     Nothing   -> False
     Just Refl -> singEqTm ty1 a1 a2
 
+eqCoreTm _ (IsPrincipal a) (IsPrincipal b)
+  = eqTm a b
+eqCoreTm _ (TypeOfPrincipal a) (TypeOfPrincipal b)
+  = eqTm a b
+
 eqCoreTm _ _ _                          = False
 
 showsPrecCore :: IsTerm tm => SingTy a -> Int -> Core tm a -> ShowS
@@ -950,6 +958,14 @@ showsPrecCore ty p core = showParen (p > 10) $ case core of
     . showsPrec 11 tya
     . showChar ' '
     . singShowsTm tya 11 a
+  IsPrincipal a ->
+      showString "is-principal"
+    . showChar ' '
+    . showsTm 11 a
+  TypeOfPrincipal a ->
+      showString "typeof-principal"
+      . showChar ' '
+      . showsTm 11 a
 
 prettyCore :: IsTerm tm => SingTy ty -> Core tm ty -> Doc
 prettyCore ty = \case
@@ -1033,6 +1049,9 @@ prettyCore ty = \case
     ]
   Typeof ty' a -> parensSep [pretty STypeof, singPrettyTm ty' a]
 
+  IsPrincipal a     -> parensSep [pretty SIsPrincipal, prettyTm a]
+  TypeOfPrincipal a -> parensSep [pretty STypeOfPrincipal, prettyTm a]
+
 
 data BeforeOrAfter = Before | After
   deriving (Eq, Show)
@@ -1417,6 +1436,10 @@ data Term (a :: Ty) where
   Yield  :: TagId -> Term a -> Term a
   Resume :: TagId ->           Term a
 
+  -- Principals
+  CreatePrincipal   :: Term 'TyGuard -> Term 'TyStr
+  ValidatePrincipal :: Term 'TyGuard -> Term 'TyStr -> Term 'TyBool
+
 data PactStep where
   Step
     :: (Term a, SingTy a)  -- exec
@@ -1569,6 +1592,9 @@ showsTerm ty p tm = withSing ty $ showParen (p > 10) $ case tm of
   Yield tid a      ->
     showString "Yield " . showsPrec 11 tid . showChar ' ' . singShowsTm ty 11 a
   Resume tid       -> showString "Resume " . showsPrec 11 tid
+  CreatePrincipal g -> showString "CreatePrincipal " . showsPrec 11 g
+  ValidatePrincipal g s ->  showString "ValidatePrincipal " . showsPrec 11 g . showChar ' ' . showsPrec 11 s
+
 
 instance Show PactStep where
   showsPrec _ (Step (exec , execTy) path mEntity mCancelVid mRollback) =
@@ -1660,6 +1686,8 @@ prettyTerm ty = \case
   Pact steps -> vsep (pretty <$> steps)
   Yield _tid tm -> parensSep [ "yield", singPrettyTm ty tm ]
   Resume _tid -> "resume"
+  CreatePrincipal g -> parensSep ["create-principal", pretty g]
+  ValidatePrincipal g s -> parensSep ["validate-principal", pretty g, pretty s]
 
 instance Pretty PactStep where
   pretty (Step (exec , execTy) _ mEntity _ mRollback) = parensSep $
@@ -1706,6 +1734,8 @@ eqTerm _ty (Format a1 b1) (Format a2 b2) = a1 == a2 && b1 == b2
 eqTerm _ty (FormatTime a1 b1) (FormatTime a2 b2) = a1 == a2 && b1 == b2
 eqTerm _ty (ParseTime a1 b1) (ParseTime a2 b2) = a1 == a2 && b1 == b2
 eqTerm _ty (Hash a1) (Hash a2) = a1 == a2
+eqTerm _ty (CreatePrincipal a) (CreatePrincipal b) = a == b
+eqTerm _ty (ValidatePrincipal a a') (ValidatePrincipal b b') = a == b && a' == b'
 eqTerm _ _ _ = False
 
 instance S :*<: Term where
@@ -1902,7 +1932,10 @@ propToInvariant (CoreProp core) = CoreInvariant <$> case core of
     Where ty1 ty2 <$> f tm1 <*> openF o <*> f tm2
   Typeof ty tm ->
     Typeof ty <$> f tm
-
+  IsPrincipal tm ->
+    IsPrincipal <$> f tm
+  TypeOfPrincipal tm ->
+    TypeOfPrincipal <$> f tm
   where
     f = propToInvariant
     openF = openPropToInv