add Some? and None?

Author: pratapsingh1729

extraction/src/execlib.rs

@@ -327,6 +327,19 @@ pub open spec fn view_first_byte_pair_opt(x: Option<(u8, SecretBuf<'_>)>) -> Seq
     }
 }
 
+
+pub fn owl_is_some<T>(x: Option<T>) -> (res: bool)
+    ensures res <==> x.is_some()
+{
+    x.is_some()   
+}
+
+pub fn owl_is_none<T>(x: Option<T>) -> (res: bool)
+    ensures res <==> x.is_none()
+{
+    x.is_none()   
+}
+
 }
 
 

extraction/src/speclib.rs

@@ -249,6 +249,17 @@ pub open spec fn ghost_unit() -> Ghost<()>
     Ghost(())
 }
 
+pub open spec fn is_some<T>(x: Option<T>) -> bool
+{
+    vstd::std_specs::option::is_some(&x)
+}
+
+pub open spec fn is_none<T>(x: Option<T>) -> bool
+{
+    vstd::std_specs::option::is_none(&x)
+}
+
+
 // pub open spec fn owl_ghost_unit() -> Ghost<()>
 // {
 //     Ghost(())

src/Extraction/Concretify.hs

@@ -305,6 +305,8 @@ concretifyApp (PRes (PDot PTop f)) params args = do
                         -- This is probably fine, since some other branch should constrain the type
                         -- debugPrint "WARNING: Can't infer type of None, using dummy type"
                         return $ mkAppNoLets f $  FOption FDummy
+        ("Some?", [x]) -> return $ mkAppNoLets "is_some" $ FBool
+        ("None?", [x]) -> return $ mkAppNoLets "is_none" $ FBool
         ("andb", [x, y]) -> return $ mkAppNoLets f FBool
         ("andp", [x, y]) -> return $ mkAppNoLets f FGhost
         ("notb", [x]) -> return $ mkAppNoLets f FBool

src/Extraction/SpecExtraction.hs

@@ -283,7 +283,7 @@ extractCEnum (CEnum n cs isVest _ _) = do
                     return [__di|
                     #{lhs} => #{specname}::#{caseName}(#{rhsX}),
                     |]
-            debugPrint $ show $ owlpretty $ map fst speccases
+            -- debugPrint $ show $ owlpretty $ map fst speccases
             parseBranches <- mapM mkParseBranch (zip speccases [0..])
             let parse = [__di|
             \#[verifier::opaque]
@@ -513,7 +513,10 @@ extractCAExpr aexpr = do
                             let [a] = args
                             a' <- extractCAExpr a
                             return [di|Option::Some(#{a'})|]
-                        "None" -> return [di|Option::None|]
+                        "None" -> case aexpr ^. tty of
+                                FOption FDummy -> return [di|Option::None|]
+                                FOption t -> return [di|Option::<#{pretty $ specTyOf t}>::None|]
+                                _ -> throwError $ TypeError $ "None on non-option type: " ++ show (owlpretty $ aexpr ^. tty)
                         "eq" -> do
                             let [a,b] = args
                             a' <- extractCAExpr a

src/Pass/PathResolution.hs

@@ -32,7 +32,7 @@ import Prettyprinter
 import Data.IORef
 
 builtinFuncs :: [String]
-builtinFuncs = ["UNIT", "TRUE", "FALSE", "eq", "Some", "None", "andb", "length", "plus", "mult", "zero", "concat", "cipherlen", "pk_cipherlen", "vk", "dhpk", "enc_pk", "dh_combine", "sign", "pkdec", "dec", "vrfy", "mac", "mac_vrfy", "checknonce", "prf", "H", "is_group_elem", "crh", "xor"]
+builtinFuncs = ["UNIT", "TRUE", "FALSE", "eq", "Some", "None", "andb", "length", "plus", "mult", "zero", "concat", "cipherlen", "pk_cipherlen", "vk", "dhpk", "enc_pk", "dh_combine", "sign", "pkdec", "dec", "vrfy", "mac", "mac_vrfy", "checknonce", "prf", "H", "is_group_elem", "crh", "xor", "Some?", "None?"]
 
 data PathType = 
     PTName

src/Typing.hs

@@ -205,6 +205,24 @@ initDetFuncs = withNormalizedTys $ [
                       TOption _ -> return $ t^.val
                       _ -> typeError $ show $ owlpretty "Expected type is not option type: " <> owlpretty t
           _ -> typeError $ show $ ErrBadArgs "None" (map snd args))),
+    mkSimpleFunc "Some?" 1 $ \args -> 
+            case args of
+            [t] -> 
+                case (stripRefinements t)^.val of
+                    TOption t' -> return $ TBool advLbl
+                    _ -> do
+                        l <- coveringLabel t
+                        return $ TBool l
+            _ -> typeError $ show $ ErrBadArgs "Some?" args,
+    mkSimpleFunc "None?" 1 $ \args -> 
+            case args of
+            [t] -> 
+                case (stripRefinements t)^.val of
+                    TOption t' -> return $ TBool advLbl
+                    _ -> do
+                        l <- coveringLabel t
+                        return $ TBool l
+            _ -> typeError $ show $ ErrBadArgs "None?" args,
     ("andb", (2, \ps args -> do
         assert ("Bad params") $ length ps == 0
         case args of

tests/success/option.owl

@@ -15,4 +15,7 @@ def alice<i>() @ A : Unit =
     let tst3 : Data<[M]> = Some<type Name(N<i>)>(get(M)) in 
     // None always requires the option
     let tst4 : Option Name(N<i>) = None<type Name(N<i>)>() in
+    let tst5 : Bool<adv> = None?(tst4) in
+    let tst6 : Bool<adv> = Some?(tst4) in
+    let tst7 : Bool<[M]> = Some?(tst3) in // ill-typed case
     ()