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

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,18 @@ evalCore (ObjTake argTy _keys obj) = withSing argTy $ do
 evalCore (ObjLength (SObjectUnsafe (SingList hlist)) _obj) = pure $ literalS $
   hListLength hlist
 
+evalCore (IsPrincipal p) = eval p <&> unliteralS >>= \case
+  Nothing -> throwErrorNoLoc (FailureMessage "`is-principal` requires statically known content")
+  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 "`is-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/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/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

@@ -1740,15 +1740,13 @@ translateNode astNode = withAstContext astNode $ case astNode of
       _ -> 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)
@@ -1902,7 +1921,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

tests/AnalyzeSpec.hs

@@ -2692,6 +2692,28 @@ spec = describe "analyze" $ do
           |]
     expectPass code $ Valid Success'
 
+  describe "is-principal" $ do
+    let code =
+         [text|
+          (defun test:bool ()
+            @model[ (property (= result (is-principal "k:462e97a099987f55f6a2b52e7bfd52a36b4b5b470fed0816a3d9b26f9450ba69")))]
+            (enforce (is-principal "k:462e97a099987f55f6a2b52e7bfd52a36b4b5b470fed0816a3d9b26f9450ba69") "")
+            )
+        |]
+    expectPass code$ Valid Success'
+    expectVerified code
+
+  describe "typeof-principal" $ do
+    let code =
+         [text|
+          (defun test:string ()
+            @model[ (property (= result (typeof-principal "k:462e97a099987f55f6a2b52e7bfd52a36b4b5b470fed0816a3d9b26f9450ba69")))]
+            (enforce (= "k:" (typeof-principal "k:462e97a099987f55f6a2b52e7bfd52a36b4b5b470fed0816a3d9b26f9450ba69")) "")
+            "k:")
+        |]
+    expectPass code$ Valid Success'
+    expectVerified code
+
   describe "enforce-keyset.row-level.read" $ do
     let code =
           [text|