------------------------------------------------------------------------
-- |
-- Module           : Data.Parameterized.Nonce.Unsafe
-- Description      : A counter in the ST monad.
-- Copyright        : (c) Galois, Inc 2014
-- Maintainer       : Joe Hendrix <jhendrix@galois.com>
-- Stability        : provisional
--
-- This module provides a simple generator of new indexes in the ST monad.
-- It is predictable and not intended for cryptographic purposes.
--
-- NOTE: the 'TestEquality' and 'OrdF' instances for the 'Nonce' type simply
-- compare the generated nonce values and then assert to the compiler
-- (via 'unsafeCoerce') that the types ascribed to the nonces are equal
-- if their values are equal.  This is only OK because of the discipline
-- by which nonces should be used: they should only be generated from
-- a 'NonceGenerator' (i.e., should not be built directly), and nonces from
-- different generators must never be compared!  Arranging to compare
-- Nonces from different origins would allow users to build 'unsafeCoerce'
-- via the 'testEquality' function.
--
-- This module is deprecated, and should not be used in new code.
-- Clients of this module should migrate to use "Data.Parameterized.Nonce".
-------------------------------------------------------------------------
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE Unsafe #-}
module Data.Parameterized.Nonce.Unsafe
  {-# DEPRECATED "Migrate to use Data.Parameterized.Nonce instead, this module will be removed soon." #-}
  ( NonceGenerator
  , newNonceGenerator
  , freshNonce
  , atLimit
  , Nonce
  , indexValue
  ) where

import Control.Monad.ST
import Data.Hashable
import Data.STRef
import Data.Word
import Unsafe.Coerce

import Data.Parameterized.Axiom
import Data.Parameterized.Classes

-- | A simple type that for getting fresh indices in the 'ST' monad.
-- The type parameter @s@ is used for the 'ST' monad parameter.
newtype NonceGenerator s = NonceGenerator (STRef s Word64)

-- | Create a new counter.
newNonceGenerator :: ST s (NonceGenerator s)
newNonceGenerator :: ST s (NonceGenerator s)
newNonceGenerator = STRef s Word64 -> NonceGenerator s
forall s. STRef s Word64 -> NonceGenerator s
NonceGenerator (STRef s Word64 -> NonceGenerator s)
-> ST s (STRef s Word64) -> ST s (NonceGenerator s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` Word64 -> ST s (STRef s Word64)
forall a s. a -> ST s (STRef s a)
newSTRef (Int -> Word64
forall a. Enum a => Int -> a
toEnum Int
0)

-- | An index generated by the counter.
newtype Nonce (tp :: k) = Nonce { Nonce tp -> Word64
indexValue :: Word64 }
  deriving (Nonce tp -> Nonce tp -> Bool
(Nonce tp -> Nonce tp -> Bool)
-> (Nonce tp -> Nonce tp -> Bool) -> Eq (Nonce tp)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall k (tp :: k). Nonce tp -> Nonce tp -> Bool
/= :: Nonce tp -> Nonce tp -> Bool
$c/= :: forall k (tp :: k). Nonce tp -> Nonce tp -> Bool
== :: Nonce tp -> Nonce tp -> Bool
$c== :: forall k (tp :: k). Nonce tp -> Nonce tp -> Bool
Eq, Eq (Nonce tp)
Eq (Nonce tp)
-> (Nonce tp -> Nonce tp -> Ordering)
-> (Nonce tp -> Nonce tp -> Bool)
-> (Nonce tp -> Nonce tp -> Bool)
-> (Nonce tp -> Nonce tp -> Bool)
-> (Nonce tp -> Nonce tp -> Bool)
-> (Nonce tp -> Nonce tp -> Nonce tp)
-> (Nonce tp -> Nonce tp -> Nonce tp)
-> Ord (Nonce tp)
Nonce tp -> Nonce tp -> Bool
Nonce tp -> Nonce tp -> Ordering
Nonce tp -> Nonce tp -> Nonce tp
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall k (tp :: k). Eq (Nonce tp)
forall k (tp :: k). Nonce tp -> Nonce tp -> Bool
forall k (tp :: k). Nonce tp -> Nonce tp -> Ordering
forall k (tp :: k). Nonce tp -> Nonce tp -> Nonce tp
min :: Nonce tp -> Nonce tp -> Nonce tp
$cmin :: forall k (tp :: k). Nonce tp -> Nonce tp -> Nonce tp
max :: Nonce tp -> Nonce tp -> Nonce tp
$cmax :: forall k (tp :: k). Nonce tp -> Nonce tp -> Nonce tp
>= :: Nonce tp -> Nonce tp -> Bool
$c>= :: forall k (tp :: k). Nonce tp -> Nonce tp -> Bool
> :: Nonce tp -> Nonce tp -> Bool
$c> :: forall k (tp :: k). Nonce tp -> Nonce tp -> Bool
<= :: Nonce tp -> Nonce tp -> Bool
$c<= :: forall k (tp :: k). Nonce tp -> Nonce tp -> Bool
< :: Nonce tp -> Nonce tp -> Bool
$c< :: forall k (tp :: k). Nonce tp -> Nonce tp -> Bool
compare :: Nonce tp -> Nonce tp -> Ordering
$ccompare :: forall k (tp :: k). Nonce tp -> Nonce tp -> Ordering
$cp1Ord :: forall k (tp :: k). Eq (Nonce tp)
Ord, Int -> Nonce tp -> Int
Nonce tp -> Int
(Int -> Nonce tp -> Int)
-> (Nonce tp -> Int) -> Hashable (Nonce tp)
forall a. (Int -> a -> Int) -> (a -> Int) -> Hashable a
forall k (tp :: k). Int -> Nonce tp -> Int
forall k (tp :: k). Nonce tp -> Int
hash :: Nonce tp -> Int
$chash :: forall k (tp :: k). Nonce tp -> Int
hashWithSalt :: Int -> Nonce tp -> Int
$chashWithSalt :: forall k (tp :: k). Int -> Nonce tp -> Int
Hashable, Int -> Nonce tp -> ShowS
[Nonce tp] -> ShowS
Nonce tp -> String
(Int -> Nonce tp -> ShowS)
-> (Nonce tp -> String) -> ([Nonce tp] -> ShowS) -> Show (Nonce tp)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (tp :: k). Int -> Nonce tp -> ShowS
forall k (tp :: k). [Nonce tp] -> ShowS
forall k (tp :: k). Nonce tp -> String
showList :: [Nonce tp] -> ShowS
$cshowList :: forall k (tp :: k). [Nonce tp] -> ShowS
show :: Nonce tp -> String
$cshow :: forall k (tp :: k). Nonce tp -> String
showsPrec :: Int -> Nonce tp -> ShowS
$cshowsPrec :: forall k (tp :: k). Int -> Nonce tp -> ShowS
Show)

--  Force the type role of Nonce to be nominal: this prevents Data.Coerce.coerce
--  from casting the types of nonces, which it would otherwise be able to do
--  because tp is a phantom type parameter.  This partially helps to protect
--  the nonce abstraction.
type role Nonce nominal

instance TestEquality Nonce where
  testEquality :: Nonce a -> Nonce b -> Maybe (a :~: b)
testEquality Nonce a
x Nonce b
y | Nonce a -> Word64
forall k (tp :: k). Nonce tp -> Word64
indexValue Nonce a
x Word64 -> Word64 -> Bool
forall a. Eq a => a -> a -> Bool
== Nonce b -> Word64
forall k (tp :: k). Nonce tp -> Word64
indexValue Nonce b
y = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: b
forall k (a :: k) (b :: k). a :~: b
unsafeAxiom
                   | Bool
otherwise = Maybe (a :~: b)
forall a. Maybe a
Nothing

instance OrdF Nonce where
  compareF :: Nonce x -> Nonce y -> OrderingF x y
compareF Nonce x
x Nonce y
y =
    case Word64 -> Word64 -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Nonce x -> Word64
forall k (tp :: k). Nonce tp -> Word64
indexValue Nonce x
x) (Nonce y -> Word64
forall k (tp :: k). Nonce tp -> Word64
indexValue Nonce y
y) of
      Ordering
LT -> OrderingF x y
forall k (x :: k) (y :: k). OrderingF x y
LTF
      Ordering
EQ -> OrderingF Any Any -> OrderingF x y
forall a b. a -> b
unsafeCoerce OrderingF Any Any
forall k (x :: k). OrderingF x x
EQF
      Ordering
GT -> OrderingF x y
forall k (x :: k) (y :: k). OrderingF x y
GTF

instance HashableF Nonce where
  hashWithSaltF :: Int -> Nonce tp -> Int
hashWithSaltF Int
s (Nonce Word64
x) = Int -> Word64 -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
s Word64
x

instance ShowF Nonce

{-# INLINE freshNonce #-}
-- | Get a fresh index and increment the counter.
freshNonce :: NonceGenerator s -> ST s (Nonce tp)
freshNonce :: NonceGenerator s -> ST s (Nonce tp)
freshNonce (NonceGenerator STRef s Word64
r) = do
  Word64
i <- STRef s Word64 -> ST s Word64
forall s a. STRef s a -> ST s a
readSTRef STRef s Word64
r
  STRef s Word64 -> Word64 -> ST s ()
forall s a. STRef s a -> a -> ST s ()
writeSTRef STRef s Word64
r (Word64 -> ST s ()) -> Word64 -> ST s ()
forall a b. (a -> b) -> a -> b
$! Word64 -> Word64
forall a. Enum a => a -> a
succ Word64
i
  Nonce tp -> ST s (Nonce tp)
forall (m :: * -> *) a. Monad m => a -> m a
return (Word64 -> Nonce tp
forall k (tp :: k). Word64 -> Nonce tp
Nonce Word64
i)

-- | Return true if counter has reached the limit, and can't be
-- incremented without risk of error.
atLimit :: NonceGenerator s -> ST s Bool
atLimit :: NonceGenerator s -> ST s Bool
atLimit (NonceGenerator STRef s Word64
r) = do
  Word64
i <- STRef s Word64 -> ST s Word64
forall s a. STRef s a -> ST s a
readSTRef STRef s Word64
r
  Bool -> ST s Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Word64
i Word64 -> Word64 -> Bool
forall a. Eq a => a -> a -> Bool
== Word64
forall a. Bounded a => a
maxBound)