diff --git a/copilot-language.cabal b/copilot-language.cabal
--- a/copilot-language.cabal
+++ b/copilot-language.cabal
@@ -1,6 +1,6 @@
 cabal-version:       >=1.10
 name:                copilot-language
-version:             2.1.2
+version:             2.2.0
 synopsis:            A Haskell-embedded DSL for monitoring hard real-time
                      distributed systems.
 description:
@@ -37,17 +37,20 @@
                , data-reify >= 0.6
                , mtl >= 2.0 && < 3
                , ghc-prim >= 0.2
-               , copilot-core >= 0.1
+               , copilot-core == 2.2.0
+               , copilot-theorem == 0.2
   exposed-modules: Copilot
                  , Copilot.Language
                  , Copilot.Language.Operators.BitWise
                  , Copilot.Language.Operators.Boolean
+                 , Copilot.Language.Operators.Propositional
                  , Copilot.Language.Operators.Cast
                  , Copilot.Language.Operators.Constant
                  , Copilot.Language.Operators.Eq
                  , Copilot.Language.Operators.Extern
                  , Copilot.Language.Operators.Integral
                  , Copilot.Language.Operators.Local
+                 , Copilot.Language.Operators.Label
                  , Copilot.Language.Operators.Mux
                  , Copilot.Language.Operators.Ord
                  , Copilot.Language.Operators.Temporal
@@ -68,8 +71,8 @@
 
     -fpackage-trust
     -- Trusted packages:
-    -trust base
-    -trust containers
-    -trust array
+    -trust=base
+    -trust=containers
+    -trust=array
 
 
diff --git a/src/Copilot/Language.hs b/src/Copilot/Language.hs
--- a/src/Copilot/Language.hs
+++ b/src/Copilot/Language.hs
@@ -18,6 +18,7 @@
   , module Copilot.Language.Operators.Eq
   , module Copilot.Language.Operators.Extern
   , module Copilot.Language.Operators.Local
+  , module Copilot.Language.Operators.Label
   , module Copilot.Language.Operators.Integral
   , module Copilot.Language.Operators.Mux
   , module Copilot.Language.Operators.Ord
@@ -30,6 +31,8 @@
   , trigger
   , arg
   , prop
+  , theorem
+  , forall, exists
   , prettyPrint
   ) where
 
@@ -46,6 +49,7 @@
 import Copilot.Language.Operators.Extern
 import Copilot.Language.Operators.Integral
 import Copilot.Language.Operators.Local
+import Copilot.Language.Operators.Label
 import Copilot.Language.Operators.Mux
 import Copilot.Language.Operators.Ord
 import Copilot.Language.Operators.Temporal
@@ -53,7 +57,6 @@
 import Copilot.Language.Reify
 import Copilot.Language.Prelude
 import Copilot.Language.Spec
-  (Spec, trigger, arg, observer, prop)
 import Copilot.Language.Stream (Stream)
 
 --------------------------------------------------------------------------------
diff --git a/src/Copilot/Language/Analyze.hs b/src/Copilot/Language/Analyze.hs
--- a/src/Copilot/Language/Analyze.hs
+++ b/src/Copilot/Language/Analyze.hs
@@ -38,7 +38,8 @@
   | DropMaxViolation
   | NestedExternFun
   | NestedArray
-  | TooMuchRecussion
+  | TooMuchRecursion
+  | InvalidField
   | DifferentTypes String
   | Redeclared String
   | BadNumberOfArgs String
@@ -49,22 +50,24 @@
   show DropAppliedToNonAppend = badUsage $  "Drop applied to non-append operation!"
   show DropIndexOverflow      = badUsage $  "Drop index overflow!"
   show ReferentialCycle       = badUsage $  "Referential cycle!"
-  show DropMaxViolation       = badUsage $  "Maximum drop violation (" ++ 
+  show DropMaxViolation       = badUsage $  "Maximum drop violation (" ++
                                   show (maxBound :: DropIdx) ++ ")!"
-  show NestedExternFun        = badUsage $  
+  show NestedExternFun        = badUsage $
     "An external function cannot take another external function or external array as an argument.  Try defining a stream, and using the stream values in the other definition."
-  show NestedArray            = badUsage $  
+  show NestedArray            = badUsage $
     "An external function cannot take another external function or external array as an argument.  Try defining a stream, and using the stream values in the other definition."
-  show TooMuchRecussion       = badUsage $ 
-    "You have exceeded the limit of " ++ show maxRecursion ++ " recursive calls in a stream definition.  Likely, you have accidently defined a circular stream, such as 'x = x'.  Another possibility is you have defined a a polymorphic function with type constraints that references other streams.  For example,\n\n  nats :: (Typed a, Num a) => Stream a\n  nats = [0] ++ nats + 1\n\nis not allowed.  Make the definition monomorphic, or add a level of indirection, like \n\n  nats :: (Typed a, Num a) => Stream a\n  nats = n\n    where n = [0] ++ nats + 1\n\nFinally, you may have intended to generate a very large expression.  You can try shrinking the expression by using local variables.  It all else fails, you can increase the maximum size of ecursive calls by modifying 'maxRecursion' in copilot-language."
-  show (DifferentTypes name) = badUsage $  
-    "The external symbol " ++ name ++ " has been declared to have two different types!"
-  show (Redeclared name) = badUsage $ 
-    "The external symbol " ++ name ++ " has been redeclared to be a different symbol (e.g., a variable and an array, or a variable and a funciton symbol, etc.)."
-  show (BadNumberOfArgs name) = badUsage $ 
-    "The function symbol " ++ name ++ " has been redeclared to have different number of arguments."
-  show (BadFunctionArgType name) = badUsage $ 
-    "The funciton symbol " ++ name ++ " has been redeclared to an argument with different types."
+  show TooMuchRecursion       = badUsage $
+    "You have exceeded the limit of " ++ show maxRecursion ++ " recursive calls in a stream definition.  Likely, you have accidently defined a circular stream, such as 'x = x'.  Another possibility is you have defined a a polymorphic function with type constraints that references other streams.  For example,\n\n  nats :: (Typed a, Num a) => Stream a\n  nats = [0] ++ nats + 1\n\nis not allowed.  Make the definition monomorphic, or add a level of indirection, like \n\n  nats :: (Typed a, Num a) => Stream a\n  nats = n\n    where n = [0] ++ n + 1\n\nFinally, you may have intended to generate a very large expression.  You can try shrinking the expression by using local variables.  It all else fails, you can increase the maximum size of ecursive calls by modifying 'maxRecursion' in copilot-language."
+  show InvalidField           = badUsage $
+    "A struct can only take external variables, arrays, or other structs as fields."
+  show (DifferentTypes name) = badUsage $
+    "The external symbol \'" ++ name ++ "\' has been declared to have two different types!"
+  show (Redeclared name) = badUsage $
+    "The external symbol \'" ++ name ++ "\' has been redeclared to be a different symbol (e.g., a variable and an array, or a variable and a funciton symbol, etc.)."
+  show (BadNumberOfArgs name) = badUsage $
+    "The function symbol \'" ++ name ++ "\' has been redeclared to have different number of arguments."
+  show (BadFunctionArgType name) = badUsage $
+    "The function symbol \'" ++ name ++ "\' has been redeclared to an argument with different types."
 
 instance Exception AnalyzeException
 
@@ -77,17 +80,19 @@
 
 --------------------------------------------------------------------------------
 
-analyze :: Spec -> IO ()
+analyze :: Spec' a -> IO ()
 analyze spec = do
   refStreams <- newIORef M.empty
   mapM_ (analyzeTrigger  refStreams) (triggers  $ runSpec spec)
   mapM_ (analyzeObserver refStreams) (observers $ runSpec spec)
-  specExts refStreams spec >>= analyzeExts 
+  mapM_ (analyzeProperty refStreams) (properties $ runSpec spec)
+  mapM_ (analyzeProperty refStreams) (map fst $ theorems $ runSpec spec)
+  specExts refStreams spec >>= analyzeExts
 
 --------------------------------------------------------------------------------
 
 analyzeTrigger :: IORef Env -> Trigger -> IO ()
-analyzeTrigger refStreams (Trigger _ e0 args) = 
+analyzeTrigger refStreams (Trigger _ e0 args) =
   analyzeExpr refStreams e0 >> mapM_ analyzeTriggerArg args
 
   where
@@ -101,16 +106,22 @@
 
 --------------------------------------------------------------------------------
 
+analyzeProperty :: IORef Env -> Property -> IO ()
+analyzeProperty refStreams (Property _ e) = analyzeExpr refStreams e
+
+--------------------------------------------------------------------------------
+
 data SeenExtern = NoExtern
                 | SeenFun
                 | SeenArr
+                | SeenStruct
 
 --------------------------------------------------------------------------------
 
 analyzeExpr :: IORef Env -> Stream a -> IO ()
 analyzeExpr refStreams s = do
   b <- mapCheck refStreams
-  when b (throw TooMuchRecussion)
+  when b (throw TooMuchRecursion)
   go NoExtern M.empty s
 
   where
@@ -124,30 +135,41 @@
       Const _             -> return ()
       Drop k e1           -> analyzeDrop (fromIntegral k) e1
       Extern _ _          -> return ()
-      ExternFun _ args me -> 
+      ExternFun _ args me ->
         checkInterp >> checkArgs
         where
-        checkInterp = case me of 
+        checkInterp = case me of
                         Nothing -> return ()
                         Just e  -> go seenExt nodes' e
-        checkArgs = case seenExt of 
-                      NoExtern -> mapM_ (\(Arg a) -> 
+        checkArgs = case seenExt of
+                      NoExtern -> mapM_ (\(Arg a) ->
                                              go SeenFun nodes' a) args
                       SeenFun  -> throw NestedExternFun
                       SeenArr  -> throw NestedArray
-      ExternArray _ idx _ _ -> case seenExt of 
-                                 NoExtern -> go SeenArr nodes' idx
-                                 SeenFun  -> throw NestedExternFun
-                                 SeenArr  -> throw NestedArray
-      Local e f           -> go seenExt nodes' e >> 
+                      SeenStruct-> throw InvalidField
+      ExternArray _ idx _ _ -> case seenExt of
+                                 NoExtern  -> go SeenArr nodes' idx
+                                 SeenFun   -> throw NestedExternFun
+                                 SeenArr   -> throw NestedArray
+                                 SeenStruct-> go SeenStruct nodes' idx
+      ExternStruct _ sargs -> case seenExt of
+                                NoExtern  ->
+                                  mapM_ (\(_, Arg a) -> go SeenStruct nodes' a) sargs
+                                SeenFun   -> throw NestedExternFun
+                                SeenArr   -> throw NestedArray
+                                SeenStruct->
+                                  mapM_ (\(_, Arg a) -> go SeenStruct nodes' a) sargs
+      GetField e _        -> analyzeAppend refStreams dstn e () analyzeExpr --Copied from `Append` case
+      Local e f           -> go seenExt nodes' e >>
                              go seenExt nodes' (f (Var "dummy"))
       Var _               -> return ()
       Op1 _ e             -> go seenExt nodes' e
-      Op2 _ e1 e2         -> go seenExt nodes' e1 >> 
+      Op2 _ e1 e2         -> go seenExt nodes' e1 >>
                              go seenExt nodes' e2
-      Op3 _ e1 e2 e3      -> go seenExt nodes' e1 >> 
-                             go seenExt nodes' e2 >> 
+      Op3 _ e1 e2 e3      -> go seenExt nodes' e1 >>
+                             go seenExt nodes' e2 >>
                              go seenExt nodes' e3
+      Label _ e           -> go seenExt nodes' e
 
 --------------------------------------------------------------------------------
 
@@ -167,7 +189,7 @@
 
 --------------------------------------------------------------------------------
 
-analyzeAppend :: 
+analyzeAppend ::
      IORef Env -> DynStableName -> Stream a -> b
   -> (IORef Env -> Stream a -> IO b) -> IO b
 analyzeAppend refStreams dstn e b f = do
@@ -194,89 +216,105 @@
 -- typed arguments.
 --------------------------------------------------------------------------------
 
--- An environment to store external variables, arrays, and functions, so that we
+-- An environment to store external variables, arrays, functions and structs, so that we
 -- can check types in the expression---e.g., if we declare the same external to
 -- have two different types.
 data ExternEnv = ExternEnv
   { externVarEnv  :: [(String, C.SimpleType)]
   , externArrEnv  :: [(String, C.SimpleType)]
-  , externFunEnv  :: [(String, C.SimpleType)] 
-  , externFunArgs :: [(String, [C.SimpleType])] 
+  , externFunEnv  :: [(String, C.SimpleType)]
+  , externFunArgs :: [(String, [C.SimpleType])]
+  , externStructEnv  :: [(String, C.SimpleType)]
+  , externStructArgs :: [(String, [C.SimpleType])]
   }
 
 --------------------------------------------------------------------------------
 
--- Make sure external variables, functions, and arrays are correctly typed.
+-- Make sure external variables, functions, arrays, and structs are correctly typed.
 
 analyzeExts :: ExternEnv -> IO ()
 analyzeExts ExternEnv { externVarEnv  = vars
                       , externArrEnv  = arrs
-                      , externFunEnv  = funs 
-                      , externFunArgs = args }
+                      , externFunEnv  = funs
+                      , externFunArgs = args
+                      , externStructEnv  = datastructs
+                      , externStructArgs = struct_args }
     = do
     -- symbol names redeclared?
     findDups vars arrs
     findDups vars funs
+    --findDups vars struct_args
+    findDups vars datastructs
     findDups arrs funs
+    --findDups arrs struct_args
+    findDups arrs datastructs
+    --findDups funs struct_args
+    findDups funs datastructs
     -- conflicting types?
     conflictingTypes vars
     conflictingTypes arrs
     conflictingTypes funs
     -- symbol names given different number of args and right types?
     funcArgCheck args
-  
+    --funcArgCheck struct_args
+    funcArgCheck struct_args
+
   where
-  findDups :: [(String, C.SimpleType)] -> [(String, C.SimpleType)] -> IO ()
+  findDups :: [(String, a)] -> [(String, b)] -> IO ()
   findDups ls0 ls1 = mapM_ (\(name,_) -> dup name) ls0
     where
-    dup nm = mapM_ ( \(name',_) -> if name' == nm 
+    dup nm = mapM_ ( \(name',_) -> if name' == nm
                                      then throw (Redeclared nm)
-                                     else return () 
+                                     else return ()
                    ) ls1
 
   conflictingTypes :: [(String, C.SimpleType)] -> IO ()
-  conflictingTypes ls = 
+  conflictingTypes ls =
     let grps = groupByPred ls in
     mapM_ sameType grps
-    where 
+    where
     sameType :: [(String, C.SimpleType)] -> IO ()
-    sameType grp = foldCheck check grp 
+    sameType grp = foldCheck check grp
     check name c0 c1 = if c0 == c1 then return (name,c0) -- a dummy---we
                                                          -- discard the result
                          else throw (DifferentTypes name)
 
   funcArgCheck :: [(String, [C.SimpleType])] -> IO ()
-  funcArgCheck ls = 
+  funcArgCheck ls =
     let grps = groupByPred ls in
     mapM_ argCheck grps
-    where 
+    where
     argCheck :: [(String, [C.SimpleType])] -> IO ()
     argCheck grp = foldCheck check grp
-    check name args0 args1 = 
-      if length args0 == length args1 
+    check name args0 args1 =
+      if length args0 == length args1
         then if args0 == args1
                then return (name,args0) -- a dummy---we discard the
                                         -- result
                else throw (BadFunctionArgType name)
-        else throw (BadNumberOfArgs name) 
+        else throw (BadNumberOfArgs name)
 
+  {-structArgCheck :: [(String, [C.SimpleType])] -> IO ()
+  structArgCheck ls = foldr (\sarg' _ -> findDups (getArgName sarg', sarg') (getArgName sarg', sarg'))
+                        (return ()) $ map snd ls-}
+
   groupByPred :: [(String, a)] -> [[(String, a)]]
   groupByPred = groupBy (\(n0,_) (n1,_) -> n0 == n1)
 
   foldCheck :: (String -> a -> a -> IO (String, a)) -> [(String, a)] -> IO ()
-  foldCheck check grp = 
+  foldCheck check grp =
     foldM_ ( \(name, c0) (_, c1) -> check name c0 c1)
            (head grp) -- should be typesafe, since this is from groupBy
            grp
 
 --------------------------------------------------------------------------------
 
-specExts :: IORef Env -> Spec -> IO ExternEnv
+specExts :: IORef Env -> Spec' a -> IO ExternEnv
 specExts refStreams spec = do
   env <- foldM triggerExts
-           (ExternEnv [] [] [] []) 
+           (ExternEnv [] [] [] [] [] [])
            (triggers $ runSpec spec)
-  foldM observerExts env (observers $ runSpec spec) 
+  foldM observerExts env (observers $ runSpec spec)
 
   where
   observerExts :: ExternEnv -> Observer -> IO ExternEnv
@@ -284,14 +322,14 @@
 
   triggerExts :: ExternEnv -> Trigger -> IO ExternEnv
   triggerExts env (Trigger _ guard args) = do
-    env' <- collectExts refStreams guard env 
+    env' <- collectExts refStreams guard env
     foldM (\env'' (Arg arg_) -> collectExts refStreams arg_ env'')
           env' args
 
 collectExts :: C.Typed a => IORef Env -> Stream a -> ExternEnv -> IO ExternEnv
 collectExts refStreams stream_ env_ = do
   b <- mapCheck refStreams
-  when b (throw TooMuchRecussion)
+  when b (throw TooMuchRecursion)
   go M.empty env_ stream_
 
   where
@@ -301,22 +339,22 @@
     assertNotVisited stream dstn nodes
 
     case stream of
-      Append _ _ e           -> analyzeAppend refStreams dstn e env 
+      Append _ _ e           -> analyzeAppend refStreams dstn e env
                                   (\refs str -> collectExts refs str env)
       Const _                -> return env
       Drop _ e1              -> go nodes env e1
-      Extern name _          -> 
+      Extern name _          ->
         let ext = ( name, getSimpleType stream ) in
         return env { externVarEnv = ext : externVarEnv env }
 
       ExternFun name args me -> do
         env' <- case me of
-                  Nothing -> return env 
+                  Nothing -> return env
                   Just e  -> go nodes env e
         env'' <- foldM (\env'' (Arg arg_) -> go nodes env'' arg_)
-                   env' args 
-        let argTypes = map (\(Arg arg_) -> getSimpleType arg_) args 
-        let fun = (name, getSimpleType stream) 
+                   env' args
+        let argTypes = map (\(Arg arg_) -> getSimpleType arg_) args
+        let fun = (name, getSimpleType stream)
         return env'' { externFunEnv  = fun : externFunEnv env''
                      , externFunArgs = (name, argTypes) : externFunArgs env''
                      }
@@ -326,17 +364,38 @@
         let arr = ( name, getSimpleType stream )
         return env' { externArrEnv = arr : externArrEnv env' }
 
-      Local e _              -> go nodes env e 
+      ExternStruct name sargs -> do
+        env' <- foldM (\env' (_, Arg arg_) -> go nodes env' arg_)
+                  env sargs
+        --let argTypes = map (\(Arg arg_) -> (n, getSimpleType arg_)) sargs
+        let argTypes = map (\(_, Arg arg_) -> getSimpleType arg_) sargs
+        let struct = (name, getSimpleType stream)
+        return env' { externStructEnv = struct : externStructEnv env'
+                    , externStructArgs = (name, argTypes) : externStructArgs env' }
+
+      GetField _ _           -> return env
+
+      Local e _              -> go nodes env e
       Var _                  -> return env
-      Op1 _ e                -> go nodes env e 
+      Op1 _ e                -> go nodes env e
       Op2 _ e1 e2            -> do env' <- go nodes env e1
                                    go nodes env' e2
-      Op3 _ e1 e2 e3         -> do env' <- go nodes env e1  
-                                   env'' <- go nodes env' e2 
-                                   go nodes env'' e3 
+      Op3 _ e1 e2 e3         -> do env' <- go nodes env e1
+                                   env'' <- go nodes env' e2
+                                   go nodes env'' e3
+      Label _ e              -> go nodes env e
 
 --------------------------------------------------------------------------------
-
+{-
+getArgName :: forall a. C.Typed a => Stream a -> String
+getArgName arg_stream =
+  case arg_stream of
+    Extern cs _          -> cs
+    ExternFun cs _ _     -> cs
+    ExternArray cs _ _ _ -> cs
+    ExternStruct cs _    -> cs
+    _                    -> ""
+-}
 getSimpleType :: forall a. C.Typed a => Stream a -> C.SimpleType
 getSimpleType _ = C.simpleType (C.typeOf :: C.Type a)
 
diff --git a/src/Copilot/Language/Operators/BitWise.hs b/src/Copilot/Language/Operators/BitWise.hs
--- a/src/Copilot/Language/Operators/BitWise.hs
+++ b/src/Copilot/Language/Operators/BitWise.hs
@@ -21,21 +21,21 @@
 import Data.Bits
 
 instance (Typed a, Bits a) => Bits (Stream a) where
-  (.&.)      = Op2 (Core.BwAnd typeOf)
-  complement = Op1 (Core.BwNot typeOf)
-  (.|.)      = Op2 (Core.BwOr  typeOf)
-  xor        = Op2 (Core.BwXor typeOf)
-  shiftL     = P.error "shiftL undefined, for left-shifting use .<<."
-  shiftR     = P.error "shiftR undefined, for right-shifting use .>>."
-  rotate     = P.error "tbd: rotate"
-  bitSize    = P.error "tbd: bitSize"
-  isSigned   = P.error "tbd: issigned"
+  (.&.)        = Op2 (Core.BwAnd typeOf)
+  complement   = Op1 (Core.BwNot typeOf)
+  (.|.)        = Op2 (Core.BwOr  typeOf)
+  xor          = Op2 (Core.BwXor typeOf)
+  shiftL       = P.error "shiftL undefined, for left-shifting use .<<."
+  shiftR       = P.error "shiftR undefined, for right-shifting use .>>."
+  rotate       = P.error "tbd: rotate"
+  bitSize      = P.error "tbd: bitSize"
+  isSigned     = P.error "tbd: issigned"
 
 -- Avoid redefinition of the Operators.Boolean xor
 (.^.) :: Bits a => a -> a -> a
 (.^.) = xor
 
-(.<<.), (.>>.) :: (Bits a, Typed a, Typed b, P.Integral b) 
+(.<<.), (.>>.) :: (Bits a, Typed a, Typed b, P.Integral b)
                => Stream a -> Stream b -> Stream a
 (.<<.) = Op2 (Core.BwShiftL typeOf typeOf)
 (.>>.) = Op2 (Core.BwShiftR typeOf typeOf)
diff --git a/src/Copilot/Language/Operators/Cast.hs b/src/Copilot/Language/Operators/Cast.hs
--- a/src/Copilot/Language/Operators/Cast.hs
+++ b/src/Copilot/Language/Operators/Cast.hs
@@ -7,8 +7,8 @@
 {-# LANGUAGE Trustworthy #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 
-module Copilot.Language.Operators.Cast 
-  ( cast ) where
+module Copilot.Language.Operators.Cast
+  ( cast, unsafeCast ) where
 
 import qualified Copilot.Core.Operators as C
 import Copilot.Core.Type
@@ -22,6 +22,9 @@
 class Cast a b where
   cast :: (Typed a, Typed b) => Stream a -> Stream b
 
+class UnsafeCast a b where
+  unsafeCast :: (Typed a, Typed b) => Stream a -> Stream b
+
 --------------------------------------------------------------------------------
 
 castBool :: (Eq a, Num a, Typed a) => Stream Bool -> Stream a
@@ -136,4 +139,93 @@
   cast = castIntegral
 
 --------------------------------------------------------------------------------
+-- | Unsafe downcasting to smaller sizes
+--------------------------------------------------------------------------------
 
+instance UnsafeCast Word64 Word32 where
+  unsafeCast = castIntegral
+instance UnsafeCast Word64 Word16 where
+  unsafeCast = castIntegral
+instance UnsafeCast Word64 Word8 where
+  unsafeCast = castIntegral
+instance UnsafeCast Word32 Word16 where
+  unsafeCast = castIntegral
+instance UnsafeCast Word32 Word8 where
+  unsafeCast = castIntegral
+instance UnsafeCast Word16 Word8 where
+  unsafeCast = castIntegral
+
+instance UnsafeCast Int64 Int32 where
+  unsafeCast = castIntegral
+instance UnsafeCast Int64 Int16 where
+  unsafeCast = castIntegral
+instance UnsafeCast Int64 Int8 where
+  unsafeCast = castIntegral
+instance UnsafeCast Int32 Int16 where
+  unsafeCast = castIntegral
+instance UnsafeCast Int32 Int8 where
+  unsafeCast = castIntegral
+instance UnsafeCast Int16 Int8 where
+  unsafeCast = castIntegral
+
+--------------------------------------------------------------------------------
+-- | Unsafe unsigned and signed promotion to floating point values
+--------------------------------------------------------------------------------
+
+instance UnsafeCast Int64 Float where
+  unsafeCast = castIntegral
+instance UnsafeCast Int32 Float where
+  unsafeCast = castIntegral
+instance UnsafeCast Int16 Float where
+  unsafeCast = castIntegral
+instance UnsafeCast Int8 Float where
+  unsafeCast = castIntegral
+
+instance UnsafeCast Int64 Double where
+  unsafeCast = castIntegral
+instance UnsafeCast Int32 Double where
+  unsafeCast = castIntegral
+instance UnsafeCast Int16 Double where
+  unsafeCast = castIntegral
+instance UnsafeCast Int8 Double where
+  unsafeCast = castIntegral
+
+instance UnsafeCast Word64 Float where
+  unsafeCast = castIntegral
+instance UnsafeCast Word32 Float where
+  unsafeCast = castIntegral
+instance UnsafeCast Word16 Float where
+  unsafeCast = castIntegral
+instance UnsafeCast Word8 Float where
+  unsafeCast = castIntegral
+
+instance UnsafeCast Word64 Double where
+  unsafeCast = castIntegral
+instance UnsafeCast Word32 Double where
+  unsafeCast = castIntegral
+instance UnsafeCast Word16 Double where
+  unsafeCast = castIntegral
+instance UnsafeCast Word8 Double where
+  unsafeCast = castIntegral
+
+--------------------------------------------------------------------------------
+-- | Signed to unsigned and vice versa
+--------------------------------------------------------------------------------
+
+instance UnsafeCast Word64 Int64 where
+  unsafeCast = castIntegral
+instance UnsafeCast Word32 Int32 where
+  unsafeCast = castIntegral
+instance UnsafeCast Word16 Int16 where
+  unsafeCast = castIntegral
+instance UnsafeCast Word8 Int8 where
+  unsafeCast = castIntegral
+
+instance UnsafeCast Int64 Word64 where
+  unsafeCast = castIntegral
+instance UnsafeCast Int32 Word32 where
+  unsafeCast = castIntegral
+instance UnsafeCast Int16 Word16 where
+  unsafeCast = castIntegral
+instance UnsafeCast Int8 Word8 where
+  unsafeCast = castIntegral
diff --git a/src/Copilot/Language/Operators/Extern.hs b/src/Copilot/Language/Operators/Extern.hs
--- a/src/Copilot/Language/Operators/Extern.hs
+++ b/src/Copilot/Language/Operators/Extern.hs
@@ -32,6 +32,7 @@
   , externArrayI64
   , externArrayF
   , externArrayD
+  , externStruct
   , funArg -- * Deprecated.
   ) where
 
@@ -50,7 +51,7 @@
 externFun :: Typed a => String -> [Arg] -> Maybe (Stream a) -> Stream a
 externFun = ExternFun
 
-externArray :: (Typed a, Typed b, Integral a) 
+externArray :: (Typed a, Typed b, Integral a)
             => String -> Stream a -> Size -> Maybe [[b]] -> Stream b
 externArray = ExternArray
 
@@ -58,12 +59,26 @@
 funArg :: Typed a => Stream a -> Arg
 funArg = Arg
 
+externStruct :: Typed a => String -> [(String, Arg)] -> Stream a
+externStruct = ExternStruct
+
+{-(#) :: Typed a => Core.StructData -> String -> Stream a
+(Core.StructData {Core.structName = x, Core.structInst = y})#z = getField x z
+  where
+    getField struct_nm field_nm =
+      let test = find (\(Core.StructData name _) -> name == struct_nm) structs in
+      case test of
+        Nothing -> error "No struct named \"" ++ struct_nm ++ "\" in the spec"
+        Just element ->
+          fromMaybe (find (\(Core.SExpr name _) -> name == field_nm) (element Core.structInst))
+            (error "No field by the name of \"" ++ field_nm ++ "\"") element
+-}
 --------------------------------------------------------------------------------
 
 externB   :: String -> Maybe [Bool] -> Stream Bool
-externB   = extern 
+externB   = extern
 externW8  :: String -> Maybe [Word8] -> Stream Word8
-externW8  = extern 
+externW8  = extern
 externW16 :: String -> Maybe [Word16] -> Stream Word16
 externW16 = extern
 externW32 :: String -> Maybe [Word32] -> Stream Word32
@@ -85,47 +100,47 @@
 
 --------------------------------------------------------------------------------
 
-externArrayB   :: (Typed a, Integral a) 
-               => String -> Stream a -> Size 
+externArrayB   :: (Typed a, Integral a)
+               => String -> Stream a -> Size
                          -> Maybe [[Bool]] -> Stream Bool
-externArrayB   = externArray 
-externArrayW8  :: (Typed a, Integral a) 
-               => String -> Stream a -> Size 
+externArrayB   = externArray
+externArrayW8  :: (Typed a, Integral a)
+               => String -> Stream a -> Size
                          -> Maybe [[Word8]] -> Stream Word8
-externArrayW8  = externArray 
+externArrayW8  = externArray
 externArrayW16 :: (Typed a, Integral a)
-               => String -> Stream a -> Size 
+               => String -> Stream a -> Size
                          -> Maybe [[Word16]] -> Stream Word16
 externArrayW16 = externArray
 externArrayW32 :: (Typed a, Integral a)
-               => String -> Stream a -> Size 
+               => String -> Stream a -> Size
                          -> Maybe [[Word32]] -> Stream Word32
 externArrayW32 = externArray
 externArrayW64 :: (Typed a, Integral a)
-               => String -> Stream a -> Size 
+               => String -> Stream a -> Size
                          -> Maybe [[Word64]] -> Stream Word64
 externArrayW64 = externArray
 externArrayI8  :: (Typed a, Integral a)
-               => String -> Stream a -> Size 
+               => String -> Stream a -> Size
                          -> Maybe [[Int8]] -> Stream Int8
 externArrayI8  = externArray
 externArrayI16 :: (Typed a, Integral a)
-               => String -> Stream a -> Size 
+               => String -> Stream a -> Size
                          -> Maybe [[Int16]] -> Stream Int16
 externArrayI16 = externArray
 externArrayI32 :: (Typed a, Integral a)
-               => String -> Stream a -> Size 
+               => String -> Stream a -> Size
                          -> Maybe [[Int32]] -> Stream Int32
 externArrayI32 = externArray
 externArrayI64 :: (Typed a, Integral a)
-               => String -> Stream a -> Size 
+               => String -> Stream a -> Size
                          -> Maybe [[Int64]] -> Stream Int64
 externArrayI64 = externArray
 externArrayF   :: (Typed a, Integral a)
-               => String -> Stream a -> Size 
+               => String -> Stream a -> Size
                          -> Maybe [[Float]] -> Stream Float
 externArrayF   = externArray
 externArrayD   :: (Typed a, Integral a)
-               => String -> Stream a -> Size 
+               => String -> Stream a -> Size
                          -> Maybe [[Double]] -> Stream Double
 externArrayD   = externArray
diff --git a/src/Copilot/Language/Operators/Integral.hs b/src/Copilot/Language/Operators/Integral.hs
--- a/src/Copilot/Language/Operators/Integral.hs
+++ b/src/Copilot/Language/Operators/Integral.hs
@@ -37,10 +37,11 @@
 
 (^) :: (Typed a, Typed b, P.Num a, B.Bits a, P.Integral b) 
     => Stream a -> Stream b -> Stream a
-(Const 0) ^ _          = Const 0
+(Const 0) ^ (Const 0)  = Const 1
+(Const 0) ^ x          = Op3 (Core.Mux typeOf) (Op2 (Core.Eq typeOf) x 0) (1) (0)
 (Const 1) ^ _          = Const 1
 (Const x) ^ (Const y)  = Const (x P.^ y)
-(Const 2) ^ y          = (Const 2) .<<. y
+(Const 2) ^ y          = (Const 1) .<<. y
 x ^ (Const y)          = foldl' ((P.*)) (Const 1) (replicate (P.fromIntegral y) x)
 _ ^ _                  = Core.badUsage "in ^: in x ^ y, either x must be the constant 2, or y must be a constant.  (Do not confuse ^ with bitwise XOR (.^.) or with ** for exponentation of floats/doubles.)"
 
diff --git a/src/Copilot/Language/Operators/Label.hs b/src/Copilot/Language/Operators/Label.hs
new file mode 100644
--- /dev/null
+++ b/src/Copilot/Language/Operators/Label.hs
@@ -0,0 +1,21 @@
+--------------------------------------------------------------------------------
+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
+--------------------------------------------------------------------------------
+
+-- | Let expressions.
+
+{-# LANGUAGE Trustworthy #-}
+
+module Copilot.Language.Operators.Label
+  ( label
+  ) where
+
+import Copilot.Core (Typed)
+import Copilot.Language.Stream (Stream (..))
+
+--------------------------------------------------------------------------------
+
+label :: (Typed a) => String -> Stream a -> Stream a
+label = Label
+
+--------------------------------------------------------------------------------
diff --git a/src/Copilot/Language/Operators/Propositional.hs b/src/Copilot/Language/Operators/Propositional.hs
new file mode 100644
--- /dev/null
+++ b/src/Copilot/Language/Operators/Propositional.hs
@@ -0,0 +1,27 @@
+--------------------------------------------------------------------------------
+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
+--------------------------------------------------------------------------------
+
+{-# LANGUAGE Trustworthy, FlexibleInstances, GADTs, MultiParamTypeClasses #-}
+
+module Copilot.Language.Operators.Propositional (not) where
+
+import Prelude (($))
+
+import Copilot.Language.Spec (Prop (..))
+import qualified Copilot.Language.Operators.Boolean as B
+
+import Copilot.Theorem
+
+--------------------------------------------------------------------------------
+
+class Negatable a b where
+  not :: a -> b
+
+instance Negatable (Prop Existential) (Prop Universal) where
+  not (Exists p)  = Forall $ B.not p
+
+instance Negatable (Prop Universal) (Prop Existential) where
+  not (Forall p)  = Exists $ B.not p
+
+--------------------------------------------------------------------------------
diff --git a/src/Copilot/Language/Operators/Temporal.hs b/src/Copilot/Language/Operators/Temporal.hs
--- a/src/Copilot/Language/Operators/Temporal.hs
+++ b/src/Copilot/Language/Operators/Temporal.hs
@@ -9,6 +9,7 @@
 module Copilot.Language.Operators.Temporal
   ( (++)
   , drop
+  , (#)
   ) where
 
 import Copilot.Core (Typed)
@@ -28,3 +29,11 @@
 drop _ ( Const j )   = Const j
 drop i ( Drop  j s ) = Drop (fromIntegral i + j) s
 drop i s             = Drop (fromIntegral i)     s
+
+(#) :: (Typed a, Typed b) => Stream a -> String -> Stream b
+(#) = GetField
+{-(ExternStruct cs sargs) # (Extern nm i) 		 				= Extern nm i
+(ExternStruct cs sargs) # (ExternFun nm args i) 		= ExternFun nm args i
+(ExternStruct cs sargs) # (ExternArray nm strm j i)	= ExternArray nm strm j i
+(ExternStruct cs sargs) # (ExternStruct nm args)	  = ExternStruct nm args-}
+--(ExternStruct cs sargs) # name = GetField (ExternStruct cs sargs) name
diff --git a/src/Copilot/Language/Reify.hs b/src/Copilot/Language/Reify.hs
--- a/src/Copilot/Language/Reify.hs
+++ b/src/Copilot/Language/Reify.hs
@@ -20,36 +20,45 @@
 import Copilot.Language.Spec
 import Copilot.Language.Stream (Stream (..), Arg (..))
 
+import Copilot.Theorem.Prove
+
 import Prelude hiding (id)
 import Data.IORef
 import System.Mem.StableName.Dynamic
 import System.Mem.StableName.Map (Map)
 import qualified System.Mem.StableName.Map as M
-import Control.Monad (liftM)
-
+import Control.Monad (liftM, unless)
 --------------------------------------------------------------------------------
 
-reify :: Spec -> IO Core.Spec
-reify spec =
-  do 
-    analyze spec
-    let trigs = triggers   $ runSpec spec
-    let obsvs = observers  $ runSpec spec
-    let props = properties $ runSpec spec
-    refMkId         <- newIORef 0
-    refVisited      <- newIORef M.empty
-    refMap          <- newIORef []
-    coreTriggers    <- mapM (mkTrigger  refMkId refVisited refMap) trigs
-    coreObservers   <- mapM (mkObserver refMkId refVisited refMap) obsvs
-    coreProperties  <- mapM (mkProperty refMkId refVisited refMap) props
-    coreStreams     <- readIORef refMap
-    return $
-      Core.Spec
+reify :: Spec' a -> IO Core.Spec
+reify spec = do
+  analyze spec
+  let trigs = triggers   $ runSpec spec
+  let obsvs = observers  $ runSpec spec
+  let props = properties $ runSpec spec
+  let thms  = reverse $ theorems $ runSpec spec
+  --let strs  = structs    $ runSpec spec
+  refMkId         <- newIORef 0
+  refVisited      <- newIORef M.empty
+  refMap          <- newIORef []
+  coreTriggers    <- mapM (mkTrigger  refMkId refVisited refMap) trigs
+  coreObservers   <- mapM (mkObserver refMkId refVisited refMap) obsvs
+  coreProperties  <- mapM (mkProperty refMkId refVisited refMap) $ props ++ (map fst thms)
+  --coreStructs     <- mapM (mkStruct   refMkId refVisited refMap) strs
+  coreStreams     <- readIORef refMap
+
+  let cspec = Core.Spec
         { Core.specStreams    = reverse coreStreams
         , Core.specObservers  = coreObservers
         , Core.specTriggers   = coreTriggers
         , Core.specProperties = coreProperties }
+        --, Core.specStructs    = coreStructs }
 
+  results <- sequence $ zipWith (prove cspec) (map (\(Property n _,_) -> n) thms) $ map snd thms
+  unless (and results) $ putStrLn "Warning: failed to check some proofs."
+
+  return cspec
+
 --------------------------------------------------------------------------------
 
 {-# INLINE mkObserver #-}
@@ -60,12 +69,11 @@
   -> Observer
   -> IO Core.Observer
 mkObserver refMkId refStreams refMap (Observer name e) = do
-    w <- mkExpr refMkId refStreams refMap e
-    return $
-      Core.Observer
-         { Core.observerName     = name
-         , Core.observerExpr     = w
-         , Core.observerExprType = typeOf }
+  w <- mkExpr refMkId refStreams refMap e
+  return Core.Observer
+    { Core.observerName     = name
+    , Core.observerExpr     = w
+    , Core.observerExprType = typeOf }
 
 --------------------------------------------------------------------------------
 
@@ -77,20 +85,19 @@
   -> Trigger
   -> IO Core.Trigger
 mkTrigger refMkId refStreams refMap (Trigger name guard args) = do
-    w1 <- mkExpr refMkId refStreams refMap guard 
-    args' <- mapM mkTriggerArg args
-    return $
-      Core.Trigger
-        { Core.triggerName  = name
-        , Core.triggerGuard = w1 
-        , Core.triggerArgs  = args' }
+  w1 <- mkExpr refMkId refStreams refMap guard
+  args' <- mapM mkTriggerArg args
+  return Core.Trigger
+    { Core.triggerName  = name
+    , Core.triggerGuard = w1
+    , Core.triggerArgs  = args' }
 
   where
 
   mkTriggerArg :: Arg -> IO Core.UExpr
   mkTriggerArg (Arg e) = do
-      w <- mkExpr refMkId refStreams refMap e
-      return $ Core.UExpr typeOf w
+    w <- mkExpr refMkId refStreams refMap e
+    return $ Core.UExpr typeOf w
 
 --------------------------------------------------------------------------------
 
@@ -102,14 +109,37 @@
   -> Property
   -> IO Core.Property
 mkProperty refMkId refStreams refMap (Property name guard) = do
-    w1 <- mkExpr refMkId refStreams refMap guard 
+  w1 <- mkExpr refMkId refStreams refMap guard
+  return Core.Property
+    { Core.propertyName  = name
+    , Core.propertyExpr  = w1 }
+
+--------------------------------------------------------------------------------
+
+--{-# INLINE mkStruct #-}
+{-mkStruct
+  :: IORef Int
+  -> IORef (Map Core.Id)
+  -> IORef [Core.Stream]
+  -> StructData
+  -> IO Core.StructData
+mkStruct refMkId refStreams refMap (StructData name fields) = do
+    fields' <- mapM mkStructField fields
     return $
-      Core.Property
-        { Core.propertyName  = name
-        , Core.propertyExpr  = w1 }
+      Core.StructData
+        { Core.structName    = name
+        , Core.structFields  = fields' }
 
+    where
+
+    mkStructField :: String -> Arg -> IO (Core.Name, Core.UExpr)
+    mkStructField cs (Arg e) = do
+      w <- mkExpr refMkId refStreams refMap e
+      return (cs, $ Core.UExpr typeOf w)
+-}
 --------------------------------------------------------------------------------
 
+
 {-# INLINE mkExpr #-}
 mkExpr
   :: Typed a
@@ -124,90 +154,139 @@
 
   where
   go :: Typed a => Stream a -> IO (Core.Expr a)
-  go e0 =
-    case e0 of
+  go e0 = case e0 of
 
-      ------------------------------------------------------
+    ------------------------------------------------------
 
+    Append _ _ _ -> do
+      s <- mkStream refMkId refStreams refMap e0
+      return $ Core.Drop typeOf 0 s
+
+    ------------------------------------------------------
+
+    Drop k e1 -> case e1 of
       Append _ _ _ -> do
-        s <- mkStream refMkId refStreams refMap e0
-        return $ Core.Drop typeOf 0 s
+          s <- mkStream refMkId refStreams refMap e1
+          return $ Core.Drop typeOf (fromIntegral k) s
+      _ -> impossible "mkExpr" "copilot-language"
 
-      ------------------------------------------------------
+    ------------------------------------------------------
 
-      Drop k e1 ->
-        case e1 of
-          Append _ _ _ -> do
-              s <- mkStream refMkId refStreams refMap e1
-              return $ Core.Drop typeOf (fromIntegral k) s
-          _ -> impossible "mkExpr" "copilot-language"
+    Const x -> return $ Core.Const typeOf x
 
-      ------------------------------------------------------
+    ------------------------------------------------------
 
-      Const x -> return $ Core.Const typeOf x
+    Local e f -> do
+        id <- mkId refMkId
+        let cs = "local_" ++ show id
+        w1 <- go e
+        w2 <- go (f (Var cs))
+        return $ Core.Local typeOf typeOf cs w1 w2
 
-      ------------------------------------------------------
+    ------------------------------------------------------
 
-      Local e f -> do
-          id <- mkId refMkId
-          let cs = "local_" ++ show id
-          w1 <- go e
-          w2 <- go (f (Var cs))
-          return $ Core.Local typeOf typeOf cs w1 w2
+    Label s e -> do
+        w <- go e
+        return $ Core.Label typeOf s w
 
-      ------------------------------------------------------
+    ------------------------------------------------------
 
-      Var cs -> return $ Core.Var typeOf cs
+    Var cs -> return $ Core.Var typeOf cs
 
-      ------------------------------------------------------
+    ------------------------------------------------------
 
-      Extern cs mXs -> return $ Core.ExternVar typeOf cs mXs
+    Extern cs mXs -> return $ Core.ExternVar typeOf cs mXs
 
-      ------------------------------------------------------
+    ------------------------------------------------------
 
-      ExternFun cs args interpExpr -> do
-          args' <- mapM mkFunArg args
-          w <- case interpExpr of
-                 Nothing -> return Nothing
-                 Just e  -> liftM Just (go e)
-          return $ Core.ExternFun typeOf cs args' w Nothing
+    ExternFun cs args interpExpr -> do
+      args' <- mapM mkFunArg args
+      w <- case interpExpr of
+             Nothing -> return Nothing
+             Just e  -> liftM Just (go e)
+      return $ Core.ExternFun typeOf cs args' w Nothing
 
-      ------------------------------------------------------
+    ------------------------------------------------------
 
-      ExternArray cs e size mXs -> do
-          w <- go e
-          return $ Core.ExternArray typeOf typeOf cs size w mXs Nothing
+    ExternArray cs e size mXs -> do
+      w <- go e
+      return $ Core.ExternArray typeOf typeOf cs size w mXs Nothing
 
-      ------------------------------------------------------
+    ------------------------------------------------------
 
-      Op1 op e -> do
-          w <- go e
-          return $ Core.Op1 op w
+    ExternStruct cs sargs -> do
+      args' <- mapM (\(name, Arg e) -> mkStrArg (name, Arg e)) sargs
+      return $ Core.ExternStruct typeOf cs args' Nothing
 
-      ------------------------------------------------------
+    ------------------------------------------------------
 
-      Op2 op e1 e2 -> do
-          w1 <- go e1
-          w2 <- go e2
-          return $ Core.Op2 op w1 w2
+    GetField struct field -> do
+      s <- go struct
+      return $ Core.GetField typeOf typeOf s field
+      {-  ISSUE: UNLIKE APPEND, GETFIELD DOES NOT HAVE CONSISTENT RETURN TYPE
+            --> NEED TO PROPERLY DEFINE GETFIELD IN EXPR
+              --> IMPLEMENT GETFIELD FROM CORE THROUGH LANGUAGE -}
 
-      ------------------------------------------------------
+    ------------------------------------------------------
 
-      Op3 op e1 e2 e3 -> do
-          w1 <- go e1
-          w2 <- go e2
-          w3 <- go e3
-          return $ Core.Op3 op w1 w2 w3
+    Op1 op e -> do
+      w <- go e
+      return $ Core.Op1 op w
 
-      ------------------------------------------------------
+    ------------------------------------------------------
 
+    Op2 op e1 e2 -> do
+      w1 <- go e1
+      w2 <- go e2
+      return $ Core.Op2 op w1 w2
+
+    ------------------------------------------------------
+
+    Op3 op e1 e2 e3 -> do
+      w1 <- go e1
+      w2 <- go e2
+      w3 <- go e3
+      return $ Core.Op3 op w1 w2 w3
+
+    ------------------------------------------------------
+
   mkFunArg :: Arg -> IO Core.UExpr
   mkFunArg (Arg e) = do
-      w <- mkExpr refMkId refStreams refMap e
-      return $ Core.UExpr typeOf w
+    w <- mkExpr refMkId refStreams refMap e
+    return $ Core.UExpr typeOf w
 
+  mkStrArg :: (Core.Name, Arg) -> IO (Core.Name, Core.UExpr)
+  mkStrArg (name, Arg e) = do
+    w <- mkExpr refMkId refStreams refMap e
+    return $ (name, Core.UExpr typeOf w)
+
+  {-mkStructArg :: StructArg -> IO Core.SExpr
+  mkStructArg (StructArg { name_ = n, arg' = Arg a }) = do
+      w <- mkExpr refMkId refStreams refMap a
+      return $ Core.SExpr n $ Core.UExpr typeOf w
+-}
 --------------------------------------------------------------------------------
 
+--{-# INLINE mkStruct #-}
+{-mkStruct
+  :: IORef Int
+  -> IORef (Map Core.Id)
+  -> IORef [Core.Stream]
+  -> StructData
+  -> IO Core.StructData
+mkStruct refMkId refStreams refMap (StructData name sargs) = trace (show name) $ do
+  args' <- mapM mkStructArg sargs
+  return $
+    Core.StructData
+      { Core.structName     = name
+      , Core.structInst     = Core.ExternStruct typeOf "" args' Nothing }
+    where
+      mkStructArg (StructArg { name_ = n, arg' = Arg a }) = do
+        w <- mkExpr refMkId refStreams refMap a
+        return $ Core.SExpr n $ Core.UExpr typeOf w-}
+
+--------------------------------------------------------------------------------
+
 {-# INLINE mkStream #-}
 mkStream
   :: Typed a
@@ -216,23 +295,21 @@
   -> IORef [Core.Stream]
   -> Stream a
   -> IO Id
-mkStream refMkId refStreams refMap e0 =
-  do
-    dstn <- makeDynStableName e0
-    let Append buf _ e = e0 -- avoids warning
-    mk <- haveVisited dstn
-    case mk of
-      Just id_ -> return id_
-      Nothing  -> addToVisited dstn buf e
+mkStream refMkId refStreams refMap e0 = do
+  dstn <- makeDynStableName e0
+  let Append buf _ e = e0 -- avoids warning
+  mk <- haveVisited dstn
+  case mk of
+    Just id_ -> return id_
+    Nothing  -> addToVisited dstn buf e
 
   where
 
   {-# INLINE haveVisited #-}
   haveVisited :: DynStableName -> IO (Maybe Int)
-  haveVisited dstn =
-    do
-      tab <- readIORef refStreams
-      return (M.lookup dstn tab)
+  haveVisited dstn = do
+    tab <- readIORef refStreams
+    return (M.lookup dstn tab)
 
   {-# INLINE addToVisited #-}
   addToVisited
@@ -241,18 +318,17 @@
     -> [a]
     -> Stream a
     -> IO Id
-  addToVisited dstn buf e =
-    do
-      id <- mkId refMkId
-      modifyIORef refStreams (M.insert dstn id)
-      w <- mkExpr refMkId refStreams refMap e
-      modifyIORef refMap $ (:)
-        Core.Stream
-          { Core.streamId         = id
-          , Core.streamBuffer     = buf
-          , Core.streamExpr       = w
-          , Core.streamExprType   = typeOf }
-      return id
+  addToVisited dstn buf e = do
+    id <- mkId refMkId
+    modifyIORef refStreams (M.insert dstn id)
+    w <- mkExpr refMkId refStreams refMap e
+    modifyIORef refMap $ (:)
+      Core.Stream
+        { Core.streamId         = id
+        , Core.streamBuffer     = buf
+        , Core.streamExpr       = w
+        , Core.streamExprType   = typeOf }
+    return id
 
 --------------------------------------------------------------------------------
 
diff --git a/src/Copilot/Language/Spec.hs b/src/Copilot/Language/Spec.hs
--- a/src/Copilot/Language/Spec.hs
+++ b/src/Copilot/Language/Spec.hs
@@ -7,56 +7,66 @@
 {-# LANGUAGE Trustworthy #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE RankNTypes #-}
 
 module Copilot.Language.Spec
-  ( Spec
+  ( Spec, Spec'
   , runSpec
   , SpecItem
   , Observer (..)
-  , observer
-  , observers
+  , observer, observers
   , Trigger (..)
-  , triggers
-  , trigger
+  , trigger, triggers
   , arg
   , Property (..)
-  , prop
-  , properties
+  , Prop (..)
+  , prop, properties
+  , theorem, theorems
+  , forall, exists
+  , extractProp
+  , Universal, Existential
   ) where
 
+import Prelude hiding (not)
+
 import Control.Monad.Writer
 import Data.List (foldl')
+--import Data.Maybe (fromMaybe)
 
+--import Copilot.Core (Typed, Struct)
 import Copilot.Core (Typed)
 import qualified Copilot.Core as Core
 import Copilot.Language.Stream
 
+import Copilot.Theorem.Prove
+
 --------------------------------------------------------------------------------
 
 type Spec = Writer [SpecItem] ()
+type Spec' a = Writer [SpecItem] a
 
 --------------------------------------------------------------------------------
 
-runSpec :: Spec -> [SpecItem]
-runSpec = execWriter 
+runSpec :: Spec' a -> [SpecItem]
+runSpec = execWriter
 
 --------------------------------------------------------------------------------
 
 observers :: [SpecItem] -> [Observer]
-observers = 
+observers =
   foldl' lets' []
   where
   lets' ls e =
-    case e of 
+    case e of
       ObserverItem l -> l : ls
       _              -> ls
 
 triggers :: [SpecItem] -> [Trigger]
-triggers = 
+triggers =
   foldl' triggers' []
   where
   triggers' ls e =
-    case e of 
+    case e of
       TriggerItem t -> t : ls
       _             -> ls
 
@@ -69,12 +79,22 @@
       PropertyItem p -> p : ls
       _              -> ls
 
+theorems :: [SpecItem] -> [(Property, UProof)]
+theorems =
+  foldl' theorems' []
+  where
+  theorems' ls e =
+    case e of
+      TheoremItem p -> p : ls
+      _              -> ls
+
 --------------------------------------------------------------------------------
 
 data SpecItem
   = ObserverItem Observer
   | TriggerItem  Trigger
   | PropertyItem Property
+  | TheoremItem (Property, UProof)
 
 --------------------------------------------------------------------------------
 
@@ -83,32 +103,73 @@
 
 --------------------------------------------------------------------------------
 
+observer :: Typed a => String -> Stream a -> Spec
+observer name e = tell [ObserverItem $ Observer name e]
+
+--------------------------------------------------------------------------------
+
+data Trigger where
+  Trigger :: Core.Name -> Stream Bool -> [Arg] -> Trigger
+
+--------------------------------------------------------------------------------
+
+trigger :: String -> Stream Bool -> [Arg] -> Spec
+trigger name e args = tell [TriggerItem $ Trigger name e args]
+
+--------------------------------------------------------------------------------
+
 data Property where
   Property :: String -> Stream Bool -> Property
 
 --------------------------------------------------------------------------------
 
-prop :: String -> Stream Bool -> Spec
-prop name e = tell [PropertyItem $ Property name e]
+data Prop a where
+  Forall :: Stream Bool -> Prop Universal
+  Exists :: Stream Bool -> Prop Existential
 
---------------------------------------------------------------------------------
+forall :: Stream Bool -> Prop Universal
+forall = Forall
 
-observer :: Typed a => String -> Stream a -> Spec
-observer name e = tell [ObserverItem $ Observer name e]
+exists :: Stream Bool -> Prop Existential
+exists = Exists
 
+extractProp :: Prop a -> Stream Bool
+extractProp (Forall p) = p
+extractProp (Exists p) = p
+
 --------------------------------------------------------------------------------
 
-data Trigger where
-  Trigger :: Core.Name -> Stream Bool -> [Arg] -> Trigger
+prop :: String -> Prop a -> Writer [SpecItem] (PropRef a)
+prop name e = tell [PropertyItem $ Property name (extractProp e)]
+  >> return (PropRef name)
 
 --------------------------------------------------------------------------------
 
-trigger :: String -> Stream Bool -> [Arg] -> Spec
-trigger name e args = tell [TriggerItem $ Trigger name e args]
+theorem :: String -> Prop a -> Proof a -> Writer [SpecItem] (PropRef a)
+theorem name e (Proof p) = tell [TheoremItem (Property name (extractProp e), p)]
+  >> return (PropRef name)
 
 --------------------------------------------------------------------------------
 
 arg :: Typed a => Stream a -> Arg
 arg = Arg
 
+--------------------------------------------------------------------------------
+
+{-
+-- | Struct operator.
+
+-- Look up the given struct x, and return field y (which should be a stream?)
+(#) :: Typed a => Core.StructData -> String -> Stream a
+(Core.StructData {Core.structName = x, Core.structArgs = y})#z = getField x z
+  where
+    getField struct_nm field_nm =
+      let test = find (\(Core.StructData name _) -> name == struct_nm) structs in
+      case test of
+        Nothing -> error "No struct named \"" ++ struct_nm ++ "\" in the spec"
+        Just element ->
+          fromMaybe (find (\(Core.SExpr name _) -> name == field_nm) (element Core.structArgs))
+            (error "No field by the name of \"" ++ field_nm ++ "\"") element
+--(Core.StructData l m)#n = Op2 (Core.GetField Core.typeOf) (Core.StructData l m) n
+-}
 --------------------------------------------------------------------------------
diff --git a/src/Copilot/Language/Stream.hs b/src/Copilot/Language/Stream.hs
--- a/src/Copilot/Language/Stream.hs
+++ b/src/Copilot/Language/Stream.hs
@@ -12,6 +12,7 @@
 module Copilot.Language.Stream
   ( Stream (..) 
   , Arg (..) 
+  , StructArg (..)
   ) where
 
 import Copilot.Core (Typed, typeOf)
@@ -34,6 +35,10 @@
               => String -> [Arg] -> Maybe (Stream a) -> Stream a
   ExternArray :: (Typed a, Typed b, Integral a)
               => String -> Stream a -> Int -> Maybe [[b]] -> Stream b
+  ExternStruct:: Typed a
+              => String -> [(String, Arg)] -> Stream a
+  GetField    :: (Typed a, Typed b)
+              => Stream a -> String -> Stream b
   Local       :: (Typed a, Typed b) 
               => Stream a -> (Stream a -> Stream b) -> Stream b
   Var         :: Typed a 
@@ -44,11 +49,14 @@
               => Core.Op2 a b c -> Stream a -> Stream b -> Stream c
   Op3         :: (Typed a, Typed b, Typed c, Typed d)
               => Core.Op3 a b c d -> Stream a -> Stream b -> Stream c -> Stream d
+  Label       :: Typed a => String -> Stream a -> Stream a
 
 --------------------------------------------------------------------------------
 
 data Arg where
   Arg :: Typed a => Stream a -> Arg
+
+data StructArg = StructArg { name_ :: String, arg' :: Arg }
 
 --------------------------------------------------------------------------------