Recursive name and nametype definitions

prelude.smt2

@@ -496,6 +496,7 @@
 
 (declare-sort Index)
 (declare-fun Happened (String (List Index) (List Bits)) Bool)
+(declare-fun IndexSucc (Index) Index)
 
 ;; Builtin function axioms
 (assert (distinct TRUE FALSE UNIT))

src/AST.hs

@@ -96,6 +96,8 @@ instance Show ResolvedPath where
 
 
 data Idx = IVar (Ignore Position) (Ignore String) IdxVar
+         | ISucc (Ignore Position) Idx
+         | IZero (Ignore Position)
     deriving (Show, Generic, Typeable)
 
 
@@ -506,6 +508,7 @@ instance Alpha Idx
 instance Alpha Endpoint
 instance Subst Idx Idx where
     isvar (IVar _ _ v) = Just (SubstName v)
+    isvar _ = Nothing
 instance Subst AExpr Idx
 instance Subst ResolvedPath Idx
 

src/LabelChecking.hs

@@ -48,9 +48,18 @@ removeGhost l =
       LTop -> return l
 
 nameDefFlows :: NameExp -> NameType -> Sym SExp
-nameDefFlows n nt = do
+nameDefFlows = nameDefFlows' Nothing
+
+nameDefFlows' :: Maybe String -> NameExp -> NameType -> Sym SExp
+nameDefFlows' rec_nt n nt = do
     case nt^.val of 
-      NT_App p is as -> (liftCheck $ resolveNameTypeApp p is as) >>= nameDefFlows n
+      NT_App p@(PRes (PDot _ name)) is as ->
+        case rec_nt of
+            -- For recursive name types
+            -- TODO: is this right?
+            Just name' | name == name' -> return sTrue
+            _ ->
+                (liftCheck $ resolveNameTypeApp p is as) >>= nameDefFlows' (Just name) n
       NT_Nonce _ -> return sTrue
       NT_DH -> return sTrue
       NT_Enc t -> do
@@ -94,7 +103,7 @@ nameDefFlows n nt = do
                                          mkSpanned $ KDFName (mkSpanned $ AEGet n) (aeVar' x) (aeVar' y) nks j nt (ignore True)
                                      KDF_IKMPos -> 
                                          mkSpanned $ KDFName (aeVar' x) (mkSpanned $ AEGet n) (aeVar' y) nks j nt (ignore True)
-                          nameDefFlows ne nt
+                          nameDefFlows' rec_nt ne nt
                       ctr <- getFreshCtr
                       vp <- interpretProp p
                       return $ sForall (map (\i -> (SAtom $ cleanSMTIdent $ show i, indexSort)) ixs) 

src/Parse.hs

@@ -29,7 +29,7 @@ owlStyle   = P.LanguageDef
                 , P.identLetter    = alphaNum <|> oneOf "_'?"
                 , P.opStart        = oneOf ":!#$%&*+./<=>?@\\^|-~"
                 , P.opLetter       = oneOf ":!#$%&*+./<=>?@\\^|-~"
-                , P.reservedNames  = ["adv",  "ghost", "Ghost", "bool", "Option", "name", "Name",  "SecName", "PubName", "st_aead",  "mackey", "sec", "st_aead_enc", "st_aead_dec", "let", "DH", "nonce", "if", "then", "else", "enum", "Data", "sigkey", "type", "Unit", "Lemma", "random_oracle", "return", "corr", "RO", "debug", "assert",  "assume", "admit", "ensures", "true", "false", "True", "False", "call", "static", "corr_case", "false_elim", "union_case", "exists", "get",  "getpk", "getvk", "pack", "def", "Union", "pkekey", "pke_sk", "pke_pk", "label", "aexp", "type", "idx", "table", "lookup", "write", "unpack", "to", "include", "maclen",  "begin", "end", "module", "aenc", "adec", "pkenc", "pkdec", "mac", "mac_vrfy", "sign", "vrfy", "prf",  "PRF", "forall", "bv", "pcase", "choose_idx", "choose_bv", "crh_lemma", "ro", "is_constant_lemma", "strict", "aad", "Const", "proof", "gkdf"]
+                , P.reservedNames  = ["adv",  "ghost", "Ghost", "bool", "Option", "name", "Name",  "SecName", "PubName", "st_aead",  "mackey", "sec", "st_aead_enc", "st_aead_dec", "let", "DH", "nonce", "if", "then", "else", "enum", "Data", "sigkey", "type", "Unit", "Lemma", "random_oracle", "return", "corr", "RO", "debug", "assert",  "assume", "admit", "ensures", "true", "false", "True", "False", "call", "static", "corr_case", "false_elim", "union_case", "exists", "get",  "getpk", "getvk", "pack", "def", "Union", "pkekey", "pke_sk", "pke_pk", "label", "aexp", "type", "idx", "table", "lookup", "write", "unpack", "to", "include", "maclen",  "begin", "end", "module", "aenc", "adec", "pkenc", "pkdec", "mac", "mac_vrfy", "sign", "vrfy", "prf",  "PRF", "forall", "bv", "pcase", "choose_idx", "choose_bv", "crh_lemma", "ro", "is_constant_lemma", "strict", "aad", "Const", "proof", "gkdf", "succ"]
                 , P.reservedOpNames= ["(", ")", "->", ":", "=", "==", "!", "<=", "!<=", "!=", "*", "|-", "+x"]
                 , P.caseSensitive  = True
                 }
@@ -1738,7 +1738,7 @@ parseParam =
             (reserved "session" >> (return $ Just IdxSession))
             <|>
             (reserved "pid" >> (return $ Just IdxPId))
-        i <- parseIdx
+        i <- parseIdxExp
         return $ ParamIdx i ot)
     <|>
     (try $ do
@@ -1757,11 +1757,34 @@ parseIdx = do
     p' <- getPosition
     return $ IVar (ignore $ mkPos p p') (ignore i) (s2n i)
 
+parseIdxExp :: Parser Idx
+parseIdxExp =
+    (do
+        p <- getPosition
+        i <- identifier
+        p' <- getPosition
+        return $ IVar (ignore $ mkPos p p') (ignore i) (s2n i)
+    ) <|> (do
+        p <- getPosition
+        reserved "succ"
+        symbol "("
+        i <- parseIdxExp
+        symbol ")"
+        p' <- getPosition
+        return $ ISucc (ignore $ mkPos p p') i
+    ) <|> (do
+        p <- getPosition
+        reserved "0"
+        p' <- getPosition
+        return $ IZero (ignore $ mkPos p p')
+    )
+
+
 parseIdxParams :: Parser ([Idx], [Idx])
 parseIdxParams = do
     inds <- optionMaybe $ do
         symbol "<"
-        is <- parseIdx `sepBy` symbol ","
+        is <- parseIdxExp `sepBy` symbol ","
         ps <- optionMaybe $ do
             symbol "@"
             parseIdx `sepBy` symbol ","
@@ -1775,7 +1798,7 @@ parseIdxParams1 :: Parser [Idx]
 parseIdxParams1 = do
     inds <- optionMaybe $ do
         symbol "<"
-        is <- parseIdx `sepBy` symbol ","
+        is <- parseIdxExp `sepBy` symbol ","
         symbol ">"
         return is
     return $ case inds of
@@ -1785,7 +1808,7 @@ parseIdxParams1 = do
 parseIdxParamsNoAngles :: Parser ([Idx], [Idx])
 parseIdxParamsNoAngles = do
     inds <- optionMaybe $ do
-        is <- parseIdx `sepBy` symbol ","
+        is <- parseIdxExp `sepBy` symbol ","
         ps <- optionMaybe $ do
             symbol "@"
             parseIdx `sepBy` symbol ","

src/Pass/PathResolution.hs

@@ -161,20 +161,22 @@ resolveDecls (d:ds) =
           return (d' : ds')
       DeclName s ixs -> do
           (is, ndecl) <- unbind ixs
-          ndecl' <- case ndecl of
-                      DeclAbstractName -> return DeclAbstractName
-                      DeclAbbrev bne2 -> do
-                          (xs, ne2) <- unbind bne2
-                          ne2' <- resolveNameExp ne2
-                          return $ DeclAbbrev $ bind xs ne2'
-                      DeclBaseName nt ls -> do
-                          nt' <- resolveNameType nt
-                          ls' <- mapM (resolveLocality (d^.spanOf)) ls
-                          return $ DeclBaseName nt' ls'
           p <- view curPath
-          let d' = Spanned (d^.spanOf) $ DeclName s $ bind is ndecl' 
-          ds' <- local (over namePaths $ T.insert s p) $ resolveDecls ds
-          return $ d' : ds'
+          -- TODO: adding both name and nameType paths for now
+          local (over namePaths $ T.insert s p) $ do
+            ndecl' <- case ndecl of
+                        DeclAbstractName -> return DeclAbstractName
+                        DeclAbbrev bne2 -> do
+                            (xs, ne2) <- unbind bne2
+                            ne2' <- resolveNameExp ne2
+                            return $ DeclAbbrev $ bind xs ne2'
+                        DeclBaseName nt ls -> do
+                            nt' <- resolveNameType nt
+                            ls' <- mapM (resolveLocality (d^.spanOf)) ls
+                            return $ DeclBaseName nt' ls'
+            let d' = Spanned (d^.spanOf) $ DeclName s $ bind is ndecl'
+            ds' <- resolveDecls ds
+            return $ d' : ds'
       DeclDefHeader s isl -> do
           (is, l) <- unbind isl
           l' <- resolveLocality (d^.spanOf) l
@@ -221,13 +223,13 @@ resolveDecls (d:ds) =
                     Right dcls -> local (over includes $ S.insert fn) $ resolveDecls (dcls ++ ds)
             _ -> resolveError (d^.spanOf) $ "include statements only allowed at top level"
       DeclNameType s b -> do
-          (is, nt) <- unbind b
-          nt' <- resolveNameType nt
-          let d' = Spanned (d^.spanOf) $ DeclNameType s $ bind is nt'
           p <- view curPath
-          ds' <- local (over nameTypePaths $ T.insert s p) $ 
-              resolveDecls ds
-          return (d' : ds')
+          local (over nameTypePaths $ T.insert s p) $ do
+            (is, nt) <- unbind b
+            nt' <- resolveNameType nt
+            let d' = Spanned (d^.spanOf) $ DeclNameType s $ bind is nt'
+            ds' <- resolveDecls ds
+            return (d' : ds')
       DeclStruct  s xs -> do
           (is, vs) <- unbind xs
           vs' <- resolveDepBind vs $ \_ -> return ()

src/Pretty.hs

@@ -51,6 +51,8 @@ instance (OwlPretty a, OwlPretty b) => OwlPretty (a, b) where
 
 instance OwlPretty Idx where
     owlpretty (IVar _ s _) = pretty $ unignore s
+    owlpretty (ISucc _ i) = pretty "succ(" <> owlpretty i <> pretty ")"
+    owlpretty (IZero _) = pretty "0"
 
 owlprettyIdxParams :: ([Idx], [Idx]) -> Doc AnsiStyle
 owlprettyIdxParams  ([], []) = mempty

src/SMTBase.hs

@@ -635,6 +635,9 @@ symIndex idx@(IVar ispan iname v) = do
           indices <- view $ inScopeIndices
           liftIO $ putStrLn $ "Unknown index: " ++ show (unignore iname)
           liftCheck $ typeError (show $ owlpretty "SMT ERROR: unknown index " <> owlpretty iname <> owlpretty " under inScopeIndices " <> (list $ map (owlpretty . fst) indices) <> owlpretty " and iEnv " <> (list $ map (owlpretty . fst) $ M.toList iEnv))
+symIndex succ@(ISucc pos i) = do
+    iv <- symIndex i
+    return $ SApp [SAtom "IndexSucc", iv]
 
 data SMTNameDef = 
     SMTBaseName (SExp, ResolvedPath) (Bind ([IdxVar], [IdxVar]) (Maybe NameType))