From 385c422d3995b7f13b64b01a60aeeec04165d2f6 Mon Sep 17 00:00:00 2001 From: Zhengyao Lin Date: Thu, 20 Feb 2025 15:39:05 -0500 Subject: [PATCH 1/7] Add succ(..) function for indices and allow recursive name definition (no well-foundedness check yet) --- prelude.smt2 | 1 + src/AST.hs | 1 + src/Parse.hs | 24 ++++++++-- src/Pass/PathResolution.hs | 27 ++++++----- src/SMTBase.hs | 3 ++ src/Typing.hs | 5 +- src/TypingBase.hs | 98 ++++++++++++++++++++++---------------- 7 files changed, 99 insertions(+), 60 deletions(-) diff --git a/prelude.smt2 b/prelude.smt2 index 7aa81f0f..ab10e332 100644 --- a/prelude.smt2 +++ b/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)) diff --git a/src/AST.hs b/src/AST.hs index 1b7c61ad..fc621993 100644 --- a/src/AST.hs +++ b/src/AST.hs @@ -96,6 +96,7 @@ instance Show ResolvedPath where data Idx = IVar (Ignore Position) (Ignore String) IdxVar + | ISucc (Ignore Position) Idx deriving (Show, Generic, Typeable) diff --git a/src/Parse.hs b/src/Parse.hs index 5e8fbc07..71309e3a 100644 --- a/src/Parse.hs +++ b/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 } @@ -1757,11 +1757,29 @@ 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 <- parseIdx + symbol ")" + p' <- getPosition + return $ ISucc (ignore $ mkPos p p') i + ) + + 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 +1793,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 diff --git a/src/Pass/PathResolution.hs b/src/Pass/PathResolution.hs index 63165b1d..415b4775 100644 --- a/src/Pass/PathResolution.hs +++ b/src/Pass/PathResolution.hs @@ -161,20 +161,21 @@ 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' + 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 diff --git a/src/SMTBase.hs b/src/SMTBase.hs index d62ac8e3..d0a3597c 100644 --- a/src/SMTBase.hs +++ b/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)) diff --git a/src/Typing.hs b/src/Typing.hs index ce006e8e..c1932c7c 100644 --- a/src/Typing.hs +++ b/src/Typing.hs @@ -67,7 +67,7 @@ emptyEnv f = do m <- newIORef $ M.empty rs <- newIORef [] memo <- mkMemoEntry - return $ Env mempty mempty mempty Nothing f initDetFuncs (TcGhost False) mempty [(Nothing, emptyModBody ModConcrete)] mempty + return $ Env mempty Nothing mempty mempty Nothing f initDetFuncs (TcGhost False) mempty [(Nothing, emptyModBody ModConcrete)] mempty interpUserFunc r m [memo] mempty rs r' r'' (typeError') checkNameType normalizeTy normalizeProp decideProp Nothing [] False False def @@ -984,7 +984,8 @@ addNameDef n (is1, is2) (nt, nls) k = do withSpan (nt^.spanOf) $ assert (show $ owlpretty "Indices on abstract and concrete def of name" <+> owlpretty n <+> owlpretty "do not match") $ (length is1 == length is1' && length is2 == length is2') _ -> typeError $ "Duplicate name: " ++ n withSpan (nt^.spanOf) $ assert (show $ owlpretty "Duplicate indices in definition: " <> owlpretty (is1 ++ is2)) $ UL.allUnique (is1 ++ is2) - withIndices (map (\i -> (i, (ignore $ show i, IdxSession))) is1 ++ map (\i -> (i, (ignore $ show i, IdxPId))) is2) $ do + withIndices (map (\i -> (i, (ignore $ show i, IdxSession))) is1 ++ map (\i -> (i, (ignore $ show i, IdxPId))) is2) $ + local (over curNameDef $ \_ -> Just (n, bind (is1, is2) (BaseDef (nt, nls)))) $ do forM_ nls normLocality checkNameType nt local (over (curMod . nameDefs) $ insert n (bind (is1, is2) (BaseDef (nt, nls)))) $ k diff --git a/src/TypingBase.hs b/src/TypingBase.hs index 9bc15f50..d1e2d44e 100644 --- a/src/TypingBase.hs +++ b/src/TypingBase.hs @@ -168,6 +168,7 @@ data Env senv = Env { -- These below must only be modified by the trusted functions, since memoization -- depends on them _inScopeIndices :: Map IdxVar (Ignore String, IdxType), + _curNameDef :: Maybe (String, Bind ([IdxVar], [IdxVar]) NameDef), _tyContext :: Map DataVar (Ignore String, (Maybe AExpr), Ty), _pathCondition :: [Prop], _expectedTy :: Maybe Ty, @@ -503,6 +504,12 @@ inferIdx (IVar pos iname i) = do typeError $ "Index should be nonghost: " ++ show (owlpretty iname) _ -> return t Nothing -> typeError $ "Unknown index: " ++ show (owlpretty iname) +inferIdx (ISucc pos i) = do + t <- inferIdx i + case t of + IdxSession -> return t + IdxPId -> typeError $ "Successor can only be applied to session or ghost indices: " ++ show (owlpretty i) + IdxGhost -> return t checkIdx :: Idx -> Check' senv () checkIdx i = do @@ -510,7 +517,7 @@ checkIdx i = do return () checkIdxSession :: Idx -> Check' senv () -checkIdxSession i@(IVar pos _ _) = do +checkIdxSession i = do it <- inferIdx i tc <- view tcScope case tc of @@ -518,7 +525,7 @@ checkIdxSession i@(IVar pos _ _) = do TcDef _ -> assert (show $ owlpretty "Wrong index type: " <> owlpretty i <> owlpretty ", got " <> owlpretty it <+> owlpretty " expected Session ID") $ it == IdxSession checkIdxPId :: Idx -> Check' senv () -checkIdxPId i@(IVar pos _ _) = do +checkIdxPId i = do it <- inferIdx i tc <- view tcScope case tc of @@ -697,32 +704,42 @@ pushRoutine s k = do local (over tcRoutineStack $ (s:)) k else k +lookupNameDef :: Path -> Check' senv (Bind ([IdxVar], [IdxVar]) NameDef) +lookupNameDef pth@(PRes (PDot p n)) = do + md <- view curMod + case lookup n (md^.nameDefs) of + Just b -> return b + Nothing -> do + cur_def <- view curNameDef + case cur_def of + Just (n', b) | n == n' -> return b + _ -> typeError $ show $ ErrUnknownName pth + getNameInfo :: NameExp -> Check' senv (Maybe (NameType, Maybe (ResolvedPath, [Locality]))) getNameInfo = withMemoize (memogetNameInfo) $ \ne -> pushRoutine "getNameInfo" $ withSpan (ne^.spanOf) $ do - res <- case ne^.val of + res <- case ne^.val of NameConst (vs1, vs2) pth@(PRes (PDot p n)) as -> do - md <- openModule p - tc <- view tcScope - forM_ vs1 checkIdxSession - forM_ vs2 checkIdxPId - case lookup n (md^.nameDefs) of - Nothing -> typeError $ show $ ErrUnknownName pth - Just b_nd -> do - ((is, ps), nd') <- unbind b_nd - assert ("Wrong index arity for name " ++ show n) $ (length vs1, length vs2) == (length is, length ps) - let nd = substs (zip is vs1) $ substs (zip ps vs2) nd' - case nd of - AbbrevNameDef bne2 -> do - (xs, ne2) <- unbind bne2 - assert ("Wrong arity for name abbreviation") $ length as == length xs - _ <- mapM inferAExpr as - getNameInfo $ substs (zip xs as) ne2 - AbstractName -> do - assert ("Value parameters not allowed for abstract names") $ length as == 0 - return Nothing - BaseDef (nt, lcls) -> do - assert ("Value parameters not allowed for base names") $ length as == 0 - return $ Just (nt, Just (PDot p n, lcls)) + tc <- view tcScope + forM_ vs1 checkIdxSession + forM_ vs2 checkIdxPId + + b_nd <- lookupNameDef pth + ((is, ps), nd') <- unbind b_nd + assert ("Wrong index arity for name " ++ show n) $ (length vs1, length vs2) == (length is, length ps) + let nd = substs (zip is vs1) $ substs (zip ps vs2) nd' + case nd of + AbbrevNameDef bne2 -> do + (xs, ne2) <- unbind bne2 + assert ("Wrong arity for name abbreviation") $ length as == length xs + _ <- mapM inferAExpr as + getNameInfo $ substs (zip xs as) ne2 + AbstractName -> do + assert ("Value parameters not allowed for abstract names") $ length as == 0 + return Nothing + BaseDef (nt, lcls) -> do + assert ("Value parameters not allowed for base names") $ length as == 0 + return $ Just (nt, Just (PDot p n, lcls)) + KDFName a b c nks j nt ib -> do _ <- local (set tcScope $ TcGhost False) $ mapM inferAExpr [a, b, c] when (not $ unignore ib) $ do @@ -1307,25 +1324,22 @@ owlprettyContext e = -- _ -> return False normalizeNameExp :: NameExp -> Check' senv NameExp -normalizeNameExp ne = +normalizeNameExp ne = case ne^.val of - NameConst (vs1, vs2) pth@(PRes (PDot p n)) as -> do - md <- openModule p - case lookup n (md^.nameDefs) of - Nothing -> typeError $ show $ ErrUnknownName pth - Just b_nd -> do - ((is, ps), nd') <- unbind b_nd - let nd = substs (zip is vs1) $ substs (zip ps vs2) nd' - case nd of - AbbrevNameDef bne2 -> do - (xs, ne2) <- unbind bne2 - assert ("Wrong arity") $ length xs == length as - normalizeNameExp $ substs (zip xs as) ne2 - _ -> return ne + NameConst (vs1, vs2) pth as -> do + b_nd <- lookupNameDef pth + ((is, ps), nd') <- unbind b_nd + let nd = substs (zip is vs1) $ substs (zip ps vs2) nd' + case nd of + AbbrevNameDef bne2 -> do + (xs, ne2) <- unbind bne2 + assert ("Wrong arity") $ length xs == length as + normalizeNameExp $ substs (zip xs as) ne2 + _ -> return ne KDFName a b c nks j nt ib -> do - a' <- resolveANF a >>= normalizeAExpr - b' <- resolveANF b >>= normalizeAExpr - c' <- resolveANF c >>= normalizeAExpr + a' <- resolveANF a >>= normalizeAExpr + b' <- resolveANF b >>= normalizeAExpr + c' <- resolveANF c >>= normalizeAExpr nt' <- normalizeNameType nt return $ Spanned (ne^.spanOf) $ KDFName a' b' c' nks j nt' ib From 7de402a206b2cd8de1d694ee7707ddb7f5e585c6 Mon Sep 17 00:00:00 2001 From: Zhengyao Lin Date: Thu, 20 Feb 2025 17:03:32 -0500 Subject: [PATCH 2/7] Allow recursive name type to appear in kdf --- src/Pass/PathResolution.hs | 30 ++++++++++++++++-------------- src/Typing.hs | 17 ++++++++++++++--- tests/success/recursive_name.owl | 12 ++++++++++++ 3 files changed, 42 insertions(+), 17 deletions(-) create mode 100644 tests/success/recursive_name.owl diff --git a/src/Pass/PathResolution.hs b/src/Pass/PathResolution.hs index 415b4775..349ce315 100644 --- a/src/Pass/PathResolution.hs +++ b/src/Pass/PathResolution.hs @@ -162,20 +162,22 @@ resolveDecls (d:ds) = DeclName s ixs -> do (is, ndecl) <- unbind ixs p <- view curPath - 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' + -- TODO: adding both name and nameType paths for now + local (over namePaths $ T.insert s p) $ + local (over nameTypePaths $ 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 diff --git a/src/Typing.hs b/src/Typing.hs index c1932c7c..b64d7832 100644 --- a/src/Typing.hs +++ b/src/Typing.hs @@ -1378,7 +1378,13 @@ nameTypeUniform nt = NT_Nonce _ -> return () NT_StAEAD _ _ _ _ -> return () NT_Enc _ -> return () - NT_App p ps as -> resolveNameTypeApp p ps as >>= nameTypeUniform + NT_App p@(PRes (PDot _ n)) ps as -> do + cur_def <- view curNameDef + case cur_def of + Just (n', _) | n == n' -> + -- TODO: check that ps contains strictly increasing indices + return () + _ -> resolveNameTypeApp p ps as >>= nameTypeUniform NT_MAC _ -> return () NT_KDF _ _ -> return () _ -> typeError $ "Name type must be uniform: " ++ show (owlpretty nt) @@ -1492,8 +1498,13 @@ checkNameType nt = withSpan (nt^.spanOf) $ checkTy t checkNoTopTy False t checkTyPubLen t - NT_App p ps as -> do - resolveNameTypeApp p ps as >>= checkNameType + NT_App p@(PRes (PDot _ n)) ps as -> do + cur_def <- view curNameDef + case cur_def of + Just (n', _) | n == n' -> + -- TODO: check that ps contains strictly increasing indices + return () + _ -> resolveNameTypeApp p ps as >>= checkNameType NT_StAEAD t xsaad p ypat -> do checkTy t checkNoTopTy False t diff --git a/tests/success/recursive_name.owl b/tests/success/recursive_name.owl new file mode 100644 index 00000000..ff7b9ef8 --- /dev/null +++ b/tests/success/recursive_name.owl @@ -0,0 +1,12 @@ +name n : nonce +name k1 : enckey Name(n) + +// Should fail parser +// name k2 : nonce + +name k2 : enckey Name(k2) + +name k3 : kdf {ikm info. + info == 0x01 -> nonce, + info == 0x02 -> k3 +} From 36d2611a38ccc81096c62b63a635f0762a19f8b7 Mon Sep 17 00:00:00 2001 From: Zhengyao Lin Date: Thu, 20 Feb 2025 20:02:59 -0500 Subject: [PATCH 3/7] WIP adding recursive name types --- src/AST.hs | 2 + src/LabelChecking.hs | 15 +++- src/Parse.hs | 5 ++ src/Pass/PathResolution.hs | 41 +++++----- src/Pretty.hs | 2 + src/Typing.hs | 130 ++++++++++++++++++------------- src/TypingBase.hs | 19 +++-- tests/success/recursive_name.owl | 24 +++++- 8 files changed, 150 insertions(+), 88 deletions(-) diff --git a/src/AST.hs b/src/AST.hs index fc621993..dafbb907 100644 --- a/src/AST.hs +++ b/src/AST.hs @@ -97,6 +97,7 @@ instance Show ResolvedPath where data Idx = IVar (Ignore Position) (Ignore String) IdxVar | ISucc (Ignore Position) Idx + | IZero (Ignore Position) deriving (Show, Generic, Typeable) @@ -507,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 diff --git a/src/LabelChecking.hs b/src/LabelChecking.hs index f4d034e8..97299c39 100644 --- a/src/LabelChecking.hs +++ b/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) diff --git a/src/Parse.hs b/src/Parse.hs index 71309e3a..eb8e9396 100644 --- a/src/Parse.hs +++ b/src/Parse.hs @@ -1772,6 +1772,11 @@ parseIdxExp = symbol ")" p' <- getPosition return $ ISucc (ignore $ mkPos p p') i + ) <|> (do + p <- getPosition + reserved "0" + p' <- getPosition + return $ IZero (ignore $ mkPos p p') ) diff --git a/src/Pass/PathResolution.hs b/src/Pass/PathResolution.hs index 349ce315..fd884519 100644 --- a/src/Pass/PathResolution.hs +++ b/src/Pass/PathResolution.hs @@ -163,21 +163,20 @@ resolveDecls (d:ds) = (is, ndecl) <- unbind ixs p <- view curPath -- TODO: adding both name and nameType paths for now - local (over namePaths $ T.insert s p) $ - local (over nameTypePaths $ 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' + 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 @@ -224,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 () diff --git a/src/Pretty.hs b/src/Pretty.hs index 8efa1904..0ed4e5af 100644 --- a/src/Pretty.hs +++ b/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 diff --git a/src/Typing.hs b/src/Typing.hs index b64d7832..345cb440 100644 --- a/src/Typing.hs +++ b/src/Typing.hs @@ -67,7 +67,7 @@ emptyEnv f = do m <- newIORef $ M.empty rs <- newIORef [] memo <- mkMemoEntry - return $ Env mempty Nothing mempty mempty Nothing f initDetFuncs (TcGhost False) mempty [(Nothing, emptyModBody ModConcrete)] mempty + return $ Env mempty Nothing Nothing mempty mempty Nothing f initDetFuncs (TcGhost False) mempty [(Nothing, emptyModBody ModConcrete)] mempty interpUserFunc r m [memo] mempty rs r' r'' (typeError') checkNameType normalizeTy normalizeProp decideProp Nothing [] False False def @@ -815,48 +815,62 @@ allM (x:xs) f = do subNameType :: NameType -> NameType -> Check Bool subNameType nt1 nt2 = do - res <- withPushLog $ case (nt1^.val, nt2^.val) of - _ | nt1 `aeq` nt2 -> return True - (NT_DH, NT_DH) -> return True - (NT_Sig t1, NT_Sig t2) -> isSubtype t1 t2 - (NT_Nonce s1, NT_Nonce s2) -> return $ s1 == s2 - (NT_Enc t1, NT_Enc t2) -> isSubtype t1 t2 - (NT_StAEAD t1 xp1 pth1 xpat1, NT_StAEAD t2 xp2 pth2 xpat2) -> do - b1 <- isSubtype t1 t2 - ((x, slf), p1) <- unbind xp1 - ((x', slf'), p2_) <- unbind xp2 - let p2 = subst x' (aeVar' x) $ subst slf' (aeVar' slf) $ p2_ - b2 <- withVars [(x, (ignore $ show x, Nothing, tGhost)), (slf, (ignore $ show slf, Nothing, tGhost))] $ decideProp $ p1 `pImpl` p2 - b3 <- return $ pth1 `aeq` pth2 - (z, pat1) <- unbind xpat1 - (w, pat2) <- unbind xpat2 - b4 <- withVars [(z, (ignore $ show z, Nothing, tGhost))] $ decideProp $ pat1 `pEq` (subst w (aeVar' z) pat2) - return $ b1 && (b2 == Just True) && b3 && (b4 == Just True) - (NT_KDF pos1 body1, NT_KDF pos2 body2) -> do - (((sx, x), (sy, y), (sz, z)), bnds) <- unbind body1 - (((sx', x'), (sy', y'), (sz', z')), bnds') <- unbind body2 - withVars [(x, (ignore sx, Nothing, tGhost)), (y, (ignore sy, Nothing, tGhost)), (z, (ignore sz, Nothing, tGhost))] $ - if pos1 == pos2 && length bnds == length bnds' then go bnds (substs [(x', aeVar' x), (y', aeVar' y), (z', aeVar' z)] bnds') else return False - where - go :: [Bind [IdxVar] (Prop, [(KDFStrictness, NameType)])] -> - [Bind [IdxVar] (Prop, [(KDFStrictness, NameType)])] -> - Check Bool - go [] [] = return True - go (b1:xs) (b2:ys) = do - (is1, rest1) <- unbind b1 - (is2, rest2_) <- unbind b2 - bhere <- if length is1 == length is2 then do - let rest2 = substs (map (\(i1, i2) -> (i2, mkIVar i1)) (zip is1 is2)) rest2_ - withIndices (map (\i -> (i, (ignore $ show i, IdxGhost))) is1) $ do - b1 <- decideProp $ pImpl (fst rest1) (fst rest2) - if (b1 == Just True) then do - allM (zip (snd rest1) (snd rest2)) $ \(nt1, nt2) -> - if (fst nt1 == fst nt2) then subNameType (snd nt1) (snd nt2) else return False - else return False - else return False - if bhere then go xs ys else return False - _ -> return False - return res + -- Some special handling of recursive name types + case (nt1^.val, nt2^.val) of + -- If both are applications, it suffices to directly check names and arguments + (NT_App _ _ _, NT_App _ _ _) -> return $ nt1 `aeq` nt2 + + -- Otherwise we unfold one of them and continue + -- Since we don't have mutually recursive types, this should terminate + (NT_App p@(PRes (PDot _ n)) is as, _) -> + resolveNameTypeApp p is as >>= (`subNameType` nt2) + + (_, NT_App p@(PRes (PDot _ n)) is as) -> + resolveNameTypeApp p is as >>= (nt1 `subNameType`) + + _ -> do + res <- withPushLog $ case (nt1^.val, nt2^.val) of + _ | nt1 `aeq` nt2 -> return True + (NT_DH, NT_DH) -> return True + (NT_Sig t1, NT_Sig t2) -> isSubtype t1 t2 + (NT_Nonce s1, NT_Nonce s2) -> return $ s1 == s2 + (NT_Enc t1, NT_Enc t2) -> isSubtype t1 t2 + (NT_StAEAD t1 xp1 pth1 xpat1, NT_StAEAD t2 xp2 pth2 xpat2) -> do + b1 <- isSubtype t1 t2 + ((x, slf), p1) <- unbind xp1 + ((x', slf'), p2_) <- unbind xp2 + let p2 = subst x' (aeVar' x) $ subst slf' (aeVar' slf) $ p2_ + b2 <- withVars [(x, (ignore $ show x, Nothing, tGhost)), (slf, (ignore $ show slf, Nothing, tGhost))] $ decideProp $ p1 `pImpl` p2 + b3 <- return $ pth1 `aeq` pth2 + (z, pat1) <- unbind xpat1 + (w, pat2) <- unbind xpat2 + b4 <- withVars [(z, (ignore $ show z, Nothing, tGhost))] $ decideProp $ pat1 `pEq` (subst w (aeVar' z) pat2) + return $ b1 && (b2 == Just True) && b3 && (b4 == Just True) + (NT_KDF pos1 body1, NT_KDF pos2 body2) -> do + (((sx, x), (sy, y), (sz, z)), bnds) <- unbind body1 + (((sx', x'), (sy', y'), (sz', z')), bnds') <- unbind body2 + withVars [(x, (ignore sx, Nothing, tGhost)), (y, (ignore sy, Nothing, tGhost)), (z, (ignore sz, Nothing, tGhost))] $ + if pos1 == pos2 && length bnds == length bnds' then go bnds (substs [(x', aeVar' x), (y', aeVar' y), (z', aeVar' z)] bnds') else return False + where + go :: [Bind [IdxVar] (Prop, [(KDFStrictness, NameType)])] -> + [Bind [IdxVar] (Prop, [(KDFStrictness, NameType)])] -> + Check Bool + go [] [] = return True + go (b1:xs) (b2:ys) = do + (is1, rest1) <- unbind b1 + (is2, rest2_) <- unbind b2 + bhere <- if length is1 == length is2 then do + let rest2 = substs (map (\(i1, i2) -> (i2, mkIVar i1)) (zip is1 is2)) rest2_ + withIndices (map (\i -> (i, (ignore $ show i, IdxGhost))) is1) $ do + b1 <- decideProp $ pImpl (fst rest1) (fst rest2) + if (b1 == Just True) then do + allM (zip (snd rest1) (snd rest2)) $ \(nt1, nt2) -> + if (fst nt1 == fst nt2) then subNameType (snd nt1) (snd nt2) else return False + else return False + else return False + if bhere then go xs ys else return False + _ -> return False + return res @@ -1285,9 +1299,10 @@ checkDecl d cont = withSpan (d^.spanOf) $ tds <- view $ curMod . nameTypeDefs assert ("Duplicate name type name: " ++ s) $ not $ member s tds (((is, ps), xs), nt) <- unbind bnt - withIndices (map (\i -> (i, (ignore $ show i, IdxSession))) is ++ map (\i -> (i, (ignore $ show i, IdxPId))) ps) $ do - withVars (map (\x -> (x, (ignore $ show x, Nothing, tGhost))) xs) $ do - checkNameType nt + local (over curNameTypeDef $ \_ -> Just (s, bnt)) $ + withIndices (map (\i -> (i, (ignore $ show i, IdxSession))) is ++ map (\i -> (i, (ignore $ show i, IdxPId))) ps) $ do + withVars (map (\x -> (x, (ignore $ show x, Nothing, tGhost))) xs) $ do + checkNameType nt local (over (curMod . nameTypeDefs) $ insert s bnt) $ cont DeclODH s b -> do ensureNoConcreteDefs @@ -1379,10 +1394,10 @@ nameTypeUniform nt = NT_StAEAD _ _ _ _ -> return () NT_Enc _ -> return () NT_App p@(PRes (PDot _ n)) ps as -> do - cur_def <- view curNameDef - case cur_def of + nt_def <- view curNameTypeDef + case nt_def of Just (n', _) | n == n' -> - -- TODO: check that ps contains strictly increasing indices + -- TODO: check that ps contains strictly increasing indices return () _ -> resolveNameTypeApp p ps as >>= nameTypeUniform NT_MAC _ -> return () @@ -1462,10 +1477,11 @@ checkNoTopTy allowGhost t = _ -> return () - - checkNameType :: NameType -> Check () -checkNameType nt = withSpan (nt^.spanOf) $ +checkNameType = checkNameType' Nothing + +checkNameType' :: Maybe String -> NameType -> Check () +checkNameType' rec_nt nt = withSpan (nt^.spanOf) $ case nt^.val of NT_DH -> return () NT_Sig t -> do @@ -1488,7 +1504,7 @@ checkNameType nt = withSpan (nt^.spanOf) $ not $ xself `elem` (toListOf fv p) checkProp p forM_ nts $ \(str, nt) -> do - checkNameType nt + checkNameType' rec_nt nt nameTypeUniform nt return $ mkExistsIdx ixs p (_, b) <- SMT.smtTypingQuery "disjoint" $ SMT.disjointProps ps @@ -1499,12 +1515,14 @@ checkNameType nt = withSpan (nt^.spanOf) $ checkNoTopTy False t checkTyPubLen t NT_App p@(PRes (PDot _ n)) ps as -> do - cur_def <- view curNameDef - case cur_def of + nt_def <- view curNameTypeDef + case nt_def of Just (n', _) | n == n' -> -- TODO: check that ps contains strictly increasing indices return () - _ -> resolveNameTypeApp p ps as >>= checkNameType + _ -> case rec_nt of + Just n' | n == n' -> return () + _ -> resolveNameTypeApp p ps as >>= checkNameType' (Just n) NT_StAEAD t xsaad p ypat -> do checkTy t checkNoTopTy False t diff --git a/src/TypingBase.hs b/src/TypingBase.hs index d1e2d44e..b38cd23e 100644 --- a/src/TypingBase.hs +++ b/src/TypingBase.hs @@ -169,6 +169,7 @@ data Env senv = Env { -- depends on them _inScopeIndices :: Map IdxVar (Ignore String, IdxType), _curNameDef :: Maybe (String, Bind ([IdxVar], [IdxVar]) NameDef), + _curNameTypeDef :: Maybe (String, Bind (([IdxVar], [IdxVar]), [DataVar]) NameType), _tyContext :: Map DataVar (Ignore String, (Maybe AExpr), Ty), _pathCondition :: [Prop], _expectedTy :: Maybe Ty, @@ -510,6 +511,7 @@ inferIdx (ISucc pos i) = do IdxSession -> return t IdxPId -> typeError $ "Successor can only be applied to session or ghost indices: " ++ show (owlpretty i) IdxGhost -> return t +-- TODO: inferIdx (IZero _) = ... checkIdx :: Idx -> Check' senv () checkIdx i = do @@ -677,11 +679,15 @@ inODHProp salt ikm info = do -- return $ substs (zip xs as) p -- _ -> typeError $ "Not an RO name: " ++ n --- Resolves all App nodes -normalizeNameType :: NameType -> Check' senv NameType -normalizeNameType nt = pushRoutine "normalizeNameType" $ +-- Resolves all App nodes (except for recursive name types) +-- TODO: assuming no mutually recursive name types yet +normalizeNameType' :: Maybe String -> NameType -> Check' senv NameType +normalizeNameType' rec_nt nt = pushRoutine "normalizeNameType" $ case nt^.val of - NT_App p is as -> resolveNameTypeApp p is as >>= normalizeNameType + NT_App p@(PRes (PDot _ n)) is as -> + case rec_nt of + Just n' | n == n' -> return nt -- Recursive name types are unfolded at most once + _ -> resolveNameTypeApp p is as >>= normalizeNameType' (Just n) NT_KDF pos bcases -> do (((sx, x), (sy, y), (sz, z)), cases) <- unbind bcases cases' <- withVars @@ -691,12 +697,15 @@ normalizeNameType nt = pushRoutine "normalizeNameType" $ (is, (p, nts)) <- unbind bcase withIndices (map (\i -> (i, (ignore $ show i, IdxGhost))) is) $ do nts' <- forM nts $ \(str, nt) -> do - nt' <- normalizeNameType nt + nt' <- normalizeNameType' rec_nt nt return (str, nt') return $ bind is (p, nts') return $ Spanned (nt^.spanOf) $ NT_KDF pos (bind ((sx, x), (sy, y), (sz, z)) cases') _ -> return nt +normalizeNameType :: NameType -> Check' senv NameType +normalizeNameType = normalizeNameType' Nothing + pushRoutine :: MonadReader (Env senv) m => String -> m a -> m a pushRoutine s k = do b <- view $ envFlags . fLogTypecheck diff --git a/tests/success/recursive_name.owl b/tests/success/recursive_name.owl index ff7b9ef8..1548c1c5 100644 --- a/tests/success/recursive_name.owl +++ b/tests/success/recursive_name.owl @@ -1,12 +1,30 @@ +locality alice + name n : nonce name k1 : enckey Name(n) -// Should fail parser +// Parser should fail // name k2 : nonce +// TODO: do we want to allow this? name k2 : enckey Name(k2) -name k3 : kdf {ikm info. +nametype rec3 = kdf {ikm info. info == 0x01 -> nonce, - info == 0x02 -> k3 + info == 0x02 -> rec3 } +name k3 : rec3 + +nametype rec4 = kdf {ikm info. + info == 0x01 -> nonce, + info == 0x02 -> kdf {ikm info. + info == 0x01 -> rec4 + } +} +name k4 : rec4 + +def derive(k: Name(k3)) @ alice : Unit + = + let k1 = kdf<1;;kdfkey;0>(k, 0x00, 0x02) in + let _ = kdf<0;;nonce;0>(k1, 0x00, 0x01) in + () From 904a1c64a0193be5286cbb36df85e8414f0ec2df Mon Sep 17 00:00:00 2001 From: Zhengyao Lin Date: Mon, 24 Feb 2025 12:15:38 -0500 Subject: [PATCH 4/7] Example works --- tests/success/recursive_name.owl | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/success/recursive_name.owl b/tests/success/recursive_name.owl index 1548c1c5..f24e0276 100644 --- a/tests/success/recursive_name.owl +++ b/tests/success/recursive_name.owl @@ -11,7 +11,7 @@ name k2 : enckey Name(k2) nametype rec3 = kdf {ikm info. info == 0x01 -> nonce, - info == 0x02 -> rec3 + info == 0x02 -> strict rec3 } name k3 : rec3 From ca5bfb01912dc7977b2e56604a6af9eaf4c8b1bd Mon Sep 17 00:00:00 2001 From: Zhengyao Lin Date: Tue, 25 Feb 2025 10:57:49 -0500 Subject: [PATCH 5/7] Add increasing index check --- src/Typing.hs | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/src/Typing.hs b/src/Typing.hs index 345cb440..4bde446e 100644 --- a/src/Typing.hs +++ b/src/Typing.hs @@ -1393,12 +1393,18 @@ nameTypeUniform nt = NT_Nonce _ -> return () NT_StAEAD _ _ _ _ -> return () NT_Enc _ -> return () - NT_App p@(PRes (PDot _ n)) ps as -> do + NT_App p@(PRes (PDot _ n)) ps@(sess_ids, _) as -> do nt_def <- view curNameTypeDef case nt_def of Just (n', _) | n == n' -> - -- TODO: check that ps contains strictly increasing indices - return () + -- Check that ps contains strictly increasing indices + if any (\i -> case i of + ISucc _ _ -> True + _ -> False) sess_ids then + return () + else + typeError $ "Recursive name type application should have at least one strictly increasing index: " + ++ show (owlpretty nt) _ -> resolveNameTypeApp p ps as >>= nameTypeUniform NT_MAC _ -> return () NT_KDF _ _ -> return () From 292be2a5cd84ed28f9d4a4139b52275182e68b50 Mon Sep 17 00:00:00 2001 From: Zhengyao Lin Date: Tue, 25 Feb 2025 16:55:01 -0500 Subject: [PATCH 6/7] More examples and fix parsing --- src/Parse.hs | 6 ++-- src/Typing.hs | 22 ++++++------ src/TypingBase.hs | 22 ++++++++---- tests/success/recursive_name.owl | 60 +++++++++++++++++++++++++++----- 4 files changed, 79 insertions(+), 31 deletions(-) diff --git a/src/Parse.hs b/src/Parse.hs index eb8e9396..abd68cdf 100644 --- a/src/Parse.hs +++ b/src/Parse.hs @@ -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 @@ -1768,7 +1768,7 @@ parseIdxExp = p <- getPosition reserved "succ" symbol "(" - i <- parseIdx + i <- parseIdxExp symbol ")" p' <- getPosition return $ ISucc (ignore $ mkPos p p') i @@ -1808,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 "," diff --git a/src/Typing.hs b/src/Typing.hs index 4bde446e..83c3274f 100644 --- a/src/Typing.hs +++ b/src/Typing.hs @@ -1396,15 +1396,7 @@ nameTypeUniform nt = NT_App p@(PRes (PDot _ n)) ps@(sess_ids, _) as -> do nt_def <- view curNameTypeDef case nt_def of - Just (n', _) | n == n' -> - -- Check that ps contains strictly increasing indices - if any (\i -> case i of - ISucc _ _ -> True - _ -> False) sess_ids then - return () - else - typeError $ "Recursive name type application should have at least one strictly increasing index: " - ++ show (owlpretty nt) + Just (n', _) | n == n' -> return () _ -> resolveNameTypeApp p ps as >>= nameTypeUniform NT_MAC _ -> return () NT_KDF _ _ -> return () @@ -1520,12 +1512,18 @@ checkNameType' rec_nt nt = withSpan (nt^.spanOf) $ checkTy t checkNoTopTy False t checkTyPubLen t - NT_App p@(PRes (PDot _ n)) ps as -> do + NT_App p@(PRes (PDot _ n)) ps@(sess_ids, _) as -> do nt_def <- view curNameTypeDef case nt_def of Just (n', _) | n == n' -> - -- TODO: check that ps contains strictly increasing indices - return () + -- Check that ps contains strictly increasing indices + if any (\i -> case i of + ISucc _ _ -> True + _ -> False) sess_ids then + return () + else + typeError $ "Recursive name type application should have at least one strictly increasing index: " + ++ show (owlpretty nt) _ -> case rec_nt of Just n' | n == n' -> return () _ -> resolveNameTypeApp p ps as >>= checkNameType' (Just n) diff --git a/src/TypingBase.hs b/src/TypingBase.hs index b38cd23e..545acc60 100644 --- a/src/TypingBase.hs +++ b/src/TypingBase.hs @@ -511,7 +511,7 @@ inferIdx (ISucc pos i) = do IdxSession -> return t IdxPId -> typeError $ "Successor can only be applied to session or ghost indices: " ++ show (owlpretty i) IdxGhost -> return t --- TODO: inferIdx (IZero _) = ... +inferIdx (IZero _) = return IdxSession checkIdx :: Idx -> Check' senv () checkIdx i = do @@ -713,15 +713,16 @@ pushRoutine s k = do local (over tcRoutineStack $ (s:)) k else k -lookupNameDef :: Path -> Check' senv (Bind ([IdxVar], [IdxVar]) NameDef) +-- Returns (is_recursive, definition) +lookupNameDef :: Path -> Check' senv (Bool, Bind ([IdxVar], [IdxVar]) NameDef) lookupNameDef pth@(PRes (PDot p n)) = do - md <- view curMod + md <- openModule p case lookup n (md^.nameDefs) of - Just b -> return b + Just b -> return (False, b) Nothing -> do cur_def <- view curNameDef case cur_def of - Just (n', b) | n == n' -> return b + Just (n', b) | n == n' -> return (True, b) _ -> typeError $ show $ ErrUnknownName pth getNameInfo :: NameExp -> Check' senv (Maybe (NameType, Maybe (ResolvedPath, [Locality]))) @@ -732,7 +733,14 @@ getNameInfo = withMemoize (memogetNameInfo) $ \ne -> pushRoutine "getNameInfo" $ forM_ vs1 checkIdxSession forM_ vs2 checkIdxPId - b_nd <- lookupNameDef pth + (is_rec, b_nd) <- lookupNameDef pth + + -- If recursive, check that the indices are strictly increasing + assert ("Recursive name uses should have at least one strictly increasing index: " ++ show (owlpretty ne)) $ + not is_rec || any (\i -> case i of + ISucc _ _ -> True + _ -> False) vs1 + ((is, ps), nd') <- unbind b_nd assert ("Wrong index arity for name " ++ show n) $ (length vs1, length vs2) == (length is, length ps) let nd = substs (zip is vs1) $ substs (zip ps vs2) nd' @@ -1336,7 +1344,7 @@ normalizeNameExp :: NameExp -> Check' senv NameExp normalizeNameExp ne = case ne^.val of NameConst (vs1, vs2) pth as -> do - b_nd <- lookupNameDef pth + (_, b_nd) <- lookupNameDef pth ((is, ps), nd') <- unbind b_nd let nd = substs (zip is vs1) $ substs (zip ps vs2) nd' case nd of diff --git a/tests/success/recursive_name.owl b/tests/success/recursive_name.owl index f24e0276..44f51cff 100644 --- a/tests/success/recursive_name.owl +++ b/tests/success/recursive_name.owl @@ -7,7 +7,10 @@ name k1 : enckey Name(n) // name k2 : nonce // TODO: do we want to allow this? -name k2 : enckey Name(k2) +name k2: enckey Name(k2) + +// Should fail +// name k3 : enckey Name(k3) nametype rec3 = kdf {ikm info. info == 0x01 -> nonce, @@ -15,16 +18,55 @@ nametype rec3 = kdf {ikm info. } name k3 : rec3 +name a : DH @ alice +name b : DH @ alice +name data : nonce @ alice + nametype rec4 = kdf {ikm info. - info == 0x01 -> nonce, - info == 0x02 -> kdf {ikm info. - info == 0x01 -> rec4 - } + info == 0x01 -> enckey Name(data), + // info == 0x02 -> strict kdf {ikm info. + // info == 0x01 -> strict rec4 + // } + info == 0x02 -> strict rec4 } -name k4 : rec4 -def derive(k: Name(k3)) @ alice : Unit +odh schedule : a, b -> {salt info. + info == 0x01 -> enckey Name(data), + info == 0x02 -> strict rec4<0> +} + +def pasta(k: Name(k3)) @ alice : Unit = - let k1 = kdf<1;;kdfkey;0>(k, 0x00, 0x02) in - let _ = kdf<0;;nonce;0>(k1, 0x00, 0x01) in + let k = kdf<1;;kdfkey;0>(k, 0x00, 0x02) in + let k = kdf<1;;kdfkey;0>(k, 0x00, 0x02) in + let k = kdf<1;;kdfkey;0>(k, 0x00, 0x02) in + let k = kdf<1;;kdfkey;0>(k, 0x00, 0x02) in + let _ = kdf<0;;nonce;0>(k, 0x00, 0x01) in () + +def pasta2(k_pre: Ghost, k: SecName(KDF>(k_pre, 0x00, 0x02))) @ alice + : SecName(KDF>(k, 0x00, 0x02)) + = kdf<1;;kdfkey;0>(k, 0x00, 0x02) + +def pasta3(k_pre: Ghost, k: SecName(KDF>(k_pre, 0x00, 0x02))) @ alice + : SecName(KDF>(gkdf(k, 0x00, 0x02), 0x00, 0x02)) + = + let k = kdf<1;;kdfkey;0>(k, 0x00, 0x02) in + let k = kdf<1;;kdfkey;0>(k, 0x00, 0x02) in + k + +struct Ticket { + k_pre: Ghost, + k: SecName(KDF>(k_pre, 0x00, 0x02)) +} + +def pasta4(ticket: Option(Ticket)) @ alice + : Option(Ticket) + = + case ticket { + | Some ticket => + parse ticket as Ticket(k_pre, k) in + let new_k = kdf<1;;kdfkey;0>(k, 0x00, 0x02) in + Some(Ticket(k, new_k)) + | None => None() + } From da2cbf4a95e8415002d4fd919a5e7561c8a9afa0 Mon Sep 17 00:00:00 2001 From: Zhengyao Lin Date: Thu, 27 Feb 2025 10:38:01 -0500 Subject: [PATCH 7/7] Example with base index --- tests/success/recursive_name.owl | 31 +++++++++++++++++++++++-------- 1 file changed, 23 insertions(+), 8 deletions(-) diff --git a/tests/success/recursive_name.owl b/tests/success/recursive_name.owl index 44f51cff..0aa62a13 100644 --- a/tests/success/recursive_name.owl +++ b/tests/success/recursive_name.owl @@ -56,17 +56,32 @@ def pasta3(k_pre: Ghost, k: SecName(KDF>(k_pre, 0x00, 0x02 k struct Ticket { - k_pre: Ghost, - k: SecName(KDF>(k_pre, 0x00, 0x02)) + pre_salt: Ghost, + pre_ikm: Ghost, + k: SecName(KDF>(pre_salt, pre_ikm, 0x02)) } -def pasta4(ticket: Option(Ticket)) @ alice - : Option(Ticket) +enum Maybe { + | Just Ticket + | Nothing +} + +def pasta4(ticket: Maybe) @ alice + : if Just?(ticket) then Ticket + else (if sec(a) /\ sec(b) then Ticket else Data) = case ticket { - | Some ticket => - parse ticket as Ticket(k_pre, k) in + | Just t => + parse t as Ticket(_, _, k) in let new_k = kdf<1;;kdfkey;0>(k, 0x00, 0x02) in - Some(Ticket(k, new_k)) - | None => None() + Ticket(k, 0x00, new_k) + | Nothing => + + let a = get(a) in + let b = get(b) in + let secret = dh_combine(dhpk(a), b) in + corr_case a in + corr_case b in + let k = kdf<;odh schedule[1];kdfkey;0>(0x00, secret, 0x02) in + Ticket(0x00, secret, k) }