[DRAFT] KDF groups impl

prelude.smt2

@@ -268,6 +268,8 @@
     :pattern (dh_combine (dhpk x) y)
     :qid dh_combine_comm
 )))
+
+; Below two axioms are only sound if we have the "unique subgroup" property for the DH group
 (assert (forall ((x Bits) (y Bits) (z Bits)) (!
     (=> (and (IsExponent x) (IsExponent y) (= TRUE (is_group_elem z))
              (= TRUE (eq (dh_combine z x) (dh_combine z y))))
@@ -330,7 +332,6 @@
 ; intersect. For soundness, this set must have measure zero
 
 (declare-fun KDF (Bits Bits Bits Int Int) Bits)
-(declare-fun KDFName (Bits Bits Bits Int Int) Name)
 
 (assert (forall ((x Bits) (y Bits) (z Bits) (i Int) (j Int)) (!
     (=>

src/AST.hs

@@ -130,8 +130,9 @@ data KDFStrictness = KDFStrict | KDFPub | KDFUnstrict
 
 data NameExpX = 
     NameConst ([Idx], [Idx]) Path [AExpr]
-    | KDFName AExpr AExpr AExpr [NameKind] Int NameType (Ignore Bool)
+    | KDFName [NameKind] Int (Ignore Bool) KDFScopeRuleRef
            -- Ignore Bool is whether we trust that the name is well-formed
+           -- KDFScopeRuleRef identifies the kdf_scope rule that produced this name
     deriving (Show, Generic, Typeable)
 
 
@@ -236,21 +237,16 @@ pHappened :: Path -> ([Idx], [Idx]) -> [AExpr] -> Prop
 pHappened s ids xs = mkSpanned $ PHappened s ids xs
 
 
-data KDFPos = KDF_SaltPos | KDF_IKMPos
-    deriving (Show, Generic, Typeable, Eq)
-
 data NameTypeX =
     NT_DH
     | NT_Sig Ty
-    | NT_Nonce String 
+    | NT_Nonce String
     | NT_Enc Ty
-    | NT_StAEAD Ty (Bind (DataVar, DataVar) Prop) Path (Bind DataVar AExpr) 
+    | NT_StAEAD Ty (Bind (DataVar, DataVar) Prop) Path (Bind DataVar AExpr)
     | NT_PKE Ty
     | NT_MAC Ty
     | NT_App Path ([Idx], [Idx]) [AExpr]
-    | NT_KDF KDFPos 
-        -- (Maybe (NameExp, Int, Int)) (Maybe (NameExp, Int, Int)) 
-        KDFBody
+    | NT_KDF  -- bare kdfkey marker; no payload
     deriving (Show, Generic, Typeable)
 
 
@@ -319,14 +315,37 @@ type ModuleExp = Spanned ModuleExpX
 data DepBind a = DPDone a | DPVar Ty String (Bind DataVar (DepBind a))
     deriving (Show, Generic, Typeable)
 
-type KDFBody =  Bind ((String, DataVar), (String, DataVar), (String, DataVar)) 
-        [Bind [IdxVar] (Prop, [(KDFStrictness, NameType)])]
+-- New kdf_scope AST types
+
+data KDFOutputSpec = KDFOutputSpec [(KDFStrictness, NameType)]
+    deriving (Show, Generic, Typeable)
+
+data KDFScopeRuleBody = KDFScopeRuleBody {
+    _ksrbWhere  :: Prop,        -- PTrue when no where clause
+    _ksrbSalt   :: AExpr,
+    _ksrbIkm    :: AExpr,
+    _ksrbInfo   :: AExpr,
+    _ksrbOutput :: KDFOutputSpec
+} deriving (Show, Generic, Typeable)
+
+data KDFScopeRuleX = KDFScopeRule {
+    _ksrIsODH :: Bool,
+    _ksrLabel :: String,
+    _ksrBody  :: Bind (([IdxVar], [IdxVar]), [DataVar]) KDFScopeRuleBody
+} deriving (Show, Generic, Typeable)
+
+type KDFScopeRule = Spanned KDFScopeRuleX
 
+data KDFScopeRuleRef = KDFScopeRuleRef {
+    _ksrrLabel :: String,
+    _ksrrIdxs  :: ([Idx], [Idx]),
+    _ksrrArgs  :: [AExpr]
+} deriving (Show, Generic, Typeable)
 
 -- Decls are surface syntax
-data DeclX = 
-    DeclName String (Bind ([IdxVar], [IdxVar]) NameDecl) 
-      | DeclSMTOption String String   
+data DeclX =
+    DeclName String (Bind ([IdxVar], [IdxVar]) NameDecl)
+      | DeclSMTOption String String
     | DeclDefHeader String (Bind ([IdxVar], [IdxVar]) Locality)
     | DeclPredicate String (Bind ([IdxVar], [DataVar]) Prop)
     | DeclFun       String (Bind (([IdxVar], [IdxVar]), [DataVar]) AExpr)
@@ -336,17 +355,18 @@ data DeclX =
                         ))
     | DeclEnum String (Bind [IdxVar] [(String, Maybe Ty)]) -- Int is arity of indices
     | DeclInclude String
-    | DeclCounter String (Bind ([IdxVar], [IdxVar]) Locality) 
+    | DeclCounter String (Bind ([IdxVar], [IdxVar]) Locality)
     | DeclStruct String (Bind [IdxVar] (DepBind ())) -- Int is arity of indices
-    | DeclODH String (Bind ([IdxVar], [IdxVar]) (NameExp, NameExp, KDFBody)) 
     | DeclTy String (Maybe Ty)
     | DeclNameType String (Bind (([IdxVar], [IdxVar]), [DataVar]) NameType)
     | DeclDetFunc String DetFuncOps Int
     | DeclTable String Ty Locality -- Only valid for localities without indices, for now
     | DeclCorr (Bind ([IdxVar], [DataVar]) (Label, Label))
-    | DeclCorrGroup (Bind ([IdxVar], [DataVar]) [Label])  
+    | DeclCorrGroup (Bind ([IdxVar], [DataVar]) [Label])
     | DeclLocality String (Either Int Path)
-    | DeclModule String IsModuleType ModuleExp (Maybe ModuleExp) 
+    | DeclModule String IsModuleType ModuleExp (Maybe ModuleExp)
+    | DeclKDFScope String [Decl]
+    | DeclKDFRule KDFScopeRuleX
     deriving (Show, Generic, Typeable)
 
 type Decl = Spanned DeclX
@@ -435,12 +455,8 @@ data ExprX =
 
 type Expr = Spanned ExprX
 
-type KDFSelector = (Int, [Idx])
-
-data CryptOp = 
-      CKDF [KDFSelector] [Either KDFSelector (String, ([Idx], [Idx]), KDFSelector)]
-           [NameKind]
-           Int 
+data CryptOp =
+      CKDF [KDFScopeRuleRef] [NameKind] Int
       | CLemma BuiltinLemma
       | CAEnc 
       | CADec 
@@ -492,6 +508,10 @@ data FuncParam =
       deriving (Show, Generic, Typeable)
 
 
+makeLenses ''KDFScopeRuleBody
+makeLenses ''KDFScopeRuleX
+makeLenses ''KDFScopeRuleRef
+
 -- LocallyNameless instances
 
 $(makeClosedAlpha ''Position)
@@ -550,10 +570,25 @@ instance Subst Idx NameExpX
 instance Subst AExpr NameExpX
 instance Subst ResolvedPath NameExpX
 
-instance Alpha KDFPos
-instance Subst Idx KDFPos
-instance Subst AExpr KDFPos
-instance Subst ResolvedPath KDFPos
+instance Alpha KDFOutputSpec
+instance Subst Idx KDFOutputSpec
+instance Subst AExpr KDFOutputSpec
+instance Subst ResolvedPath KDFOutputSpec
+
+instance Alpha KDFScopeRuleBody
+instance Subst Idx KDFScopeRuleBody
+instance Subst AExpr KDFScopeRuleBody
+instance Subst ResolvedPath KDFScopeRuleBody
+
+instance Alpha KDFScopeRuleX
+instance Subst Idx KDFScopeRuleX
+instance Subst AExpr KDFScopeRuleX
+instance Subst ResolvedPath KDFScopeRuleX
+
+instance Alpha KDFScopeRuleRef
+instance Subst Idx KDFScopeRuleRef
+instance Subst AExpr KDFScopeRuleRef
+instance Subst ResolvedPath KDFScopeRuleRef
 
 instance Alpha NameTypeX
 instance Subst Idx NameTypeX
@@ -672,3 +707,11 @@ mkExistsIdx :: [IdxVar] -> Prop -> Prop
 mkExistsIdx [] p = p
 mkExistsIdx (x:xs) p = mkSpanned $ PQuantIdx Exists (ignore $ show x) $ bind x $ mkExistsIdx xs p
 
+mkForallBv :: [DataVar] -> Prop -> Prop
+mkForallBv [] p = p
+mkForallBv (x:xs) p = mkSpanned $ PQuantBV Forall (ignore $ show x) $ bind x $ mkForallBv xs p
+
+mkExistsBv :: [DataVar] -> Prop -> Prop
+mkExistsBv [] p = p
+mkExistsBv (x:xs) p = mkSpanned $ PQuantBV Exists (ignore $ show x) $ bind x $ mkExistsBv xs p
+

src/CmdArgs.hs

@@ -18,12 +18,15 @@ data Flags = Flags {
     _fDebugExtraction :: Bool,
     _fExtractBufOpt :: Bool,
     _fDoTests :: Bool,
+    _fTestWithSMTCache :: Bool,
     _fLax :: Bool,
     _fSkipRODisj :: Bool,
     _fFilePath :: String, 
     _fLocalTypeError :: Bool,
     _fLogTypecheck :: Bool,
     _fOnlyCheck :: Maybe String,
+    _fOnlyParse :: Bool,
+    _fNoColor :: Bool,
     _fFileContents :: String
                    }
 
@@ -48,6 +51,9 @@ parseArgs =
       <*>
           switch
           ( long "test" <> help "Do tests")
+      <*>
+          switch
+          ( long "test-with-smtcache" <> help "Do tests without clearing the SMT cache" )
       <*>
           switch
           ( long "lax" <> help "Lax checking (skip some SMT queries)" )
@@ -62,6 +68,10 @@ parseArgs =
           switch
           ( long "log-typecheck" <> help "Log typechecker progress" )
       <*> option (Just <$> str) (long "only-check" <> help "Only check the given function" <> value Nothing)
+      <*> switch
+          ( long "only-parse" <> help "Run parser only; print parsed module and exit" )
+      <*> switch
+          ( long "no-color-output" <> help "Print errors without terminal colors (suitable for file output)" )
       <*> (pure "")
     where
         extractAllFlag = switch (long "extract" <> short 'e' <> help "Extract all specs and code")
@@ -81,7 +91,8 @@ doParseArgs = do
 
 postProcessFlags :: Flags -> Flags
 postProcessFlags f = 
-    f { _fCleanCache = _fCleanCache f || _fLogSMT f || _fDoTests f }
+    f { _fCleanCache = _fCleanCache f || _fLogSMT f || _fDoTests f,
+        _fDoTests = _fTestWithSMTCache f || _fDoTests f }
 
 getHelpMessage :: String
 getHelpMessage = 

src/Extraction/ConcreteAST.hs

@@ -464,7 +464,7 @@ instance Subst AExpr (CExpr t)
 compatTys :: CTy -> CTy -> Bool
 compatTys (CTName n1) (CTName n2) =
     case (n1 ^. val, n2 ^. val) of
-        (KDFName _ _ _ nks1 i1 _ _, KDFName _ _ _ nks2 i2 _ _) ->
+        (KDFName nks1 i1 _ _, KDFName nks2 i2 _ _) ->
             (nks1 !! i1) `aeq` (nks2 !! i2)
         _ -> n1 `aeq` n2
 compatTys (CTDH_PK _) (CTDH_PK _) = True

src/Extraction/Concretify.hs

@@ -184,7 +184,7 @@ formatTyOfNameExp ne = do
             fl <- fLenOfNameTy nt
             sec <- secrecyOfNameTy nt
             return $ FBuf sec $ Just fl
-        KDFName _ _ _ nks i _ _ -> do
+        KDFName nks i _ _ -> do
             let nk = nks !! i
             sec <- secrecyOfNameKind nk
             FBuf sec . Just <$> fLenOfNameKind nk
@@ -748,7 +748,7 @@ tySigOfCall p = do
 
 
 concretifyCryptOp :: [AExpr] -> CryptOp -> [CAExpr FormatTy] -> EM (CExpr FormatTy, [CLetBinding])
-concretifyCryptOp resolvedArgs (CKDF _ _ nks nkidx) [salt, ikm, info] = do
+concretifyCryptOp resolvedArgs (CKDF _ nks nkidx) [salt, ikm, info] = do
     let nk = nks !! nkidx
     kdfLen <- kdfLenOf nks
     outLen <- fLenOfNameKind nk

src/LabelChecking.hs

@@ -78,34 +78,7 @@ nameDefFlows n nt = do
           lv <- symLabel l
           ln <- symLabel $ mkSpanned $ LName n
           return $ sFlows lv ln
-      NT_KDF pos bnd -> do 
-          ctr <- getFreshCtr
-          (((sx, x), (sy, y), (sz, z)), cases) <- liftCheck $ unbind bnd
-          -- TODO: below, we need to generealize
-          axs <- withSMTVars [x, y, z] $ do
-              axis <- forM [0 .. (length cases - 1)] $ \i -> do
-                  (ixs, (p, nts)) <- liftCheck $ unbind $ cases !! i
-                  axijs <- forM [0 .. (length nts - 1)] $ \j -> do
-                      let (strictness, nt) = nts !! j
-                      ne_axioms <- withSMTIndices (map (\i -> (i, IdxGhost)) ixs) $ do
-                          nks <- liftCheck $ mapM (\(_, nt) -> getNameKind nt) nts
-                          let ne = case pos of 
-                                     KDF_SaltPos -> 
-                                         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
-                      ctr <- getFreshCtr
-                      vp <- interpretProp p
-                      return $ sForall (map (\i -> (SAtom $ cleanSMTIdent $ show i, indexSort)) ixs) 
-                                (sImpl vp ne_axioms)
-                                []
-                                ("ax_" ++ show ctr)
-                  return $ sAnd axijs
-              return $ sAnd axis
-          let vx = SAtom (show x)
-          let vy = SAtom (show y)
-          return $ sForall [(vx, bitstringSort), (vy, bitstringSort)] axs [] ("kdfFlows_" ++ show ctr)
+      NT_KDF -> return $ SAtom "true" -- bare kdfkey marker; no flow axioms
 
 smtLabelSetup :: Sym ()
 smtLabelSetup = do

src/Main.hs

@@ -11,6 +11,7 @@ import Prettyprinter
 import TypingBase
 import System.FilePath
 import CmdArgs
+import Pretty
 import System.Directory
 import System.Process
 import System.CPUTime
@@ -41,6 +42,9 @@ main = do
               putStrLn $ "parse error: " ++ show err 
               exitFailure
             Right ast -> do
+                when (args^.fOnlyParse) $ do
+                    mapM_ (putStrLn . show . owlpretty) ast
+                    exitSuccess
                 do
                     res <- typeCheckDecls (set fFileContents s args) ast
                     case res of