------------------------------------------------------------------------
-- |
-- 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 :: forall s. ST s (NonceGenerator s)
newNonceGenerator = forall s. STRef s Word64 -> NonceGenerator s
NonceGenerator forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` forall a s. a -> ST s (STRef s a)
newSTRef (forall a. Enum a => Int -> a
toEnum Int
0)

-- | An index generated by the counter.
newtype Nonce (tp :: k) = Nonce { forall k (tp :: k). Nonce tp -> Word64
indexValue :: Word64 }
  deriving (Nonce tp -> Nonce tp -> Bool
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, 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
Ord, Int -> Nonce tp -> Int
Nonce tp -> Int
forall a. Eq a -> (Int -> a -> Int) -> (a -> Int) -> Hashable a
forall k (tp :: k). Eq (Nonce tp)
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
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 :: forall (a :: k) (b :: k). Nonce a -> Nonce b -> Maybe (a :~: b)
testEquality Nonce a
x Nonce b
y | forall k (tp :: k). Nonce tp -> Word64
indexValue Nonce a
x forall a. Eq a => a -> a -> Bool
== forall k (tp :: k). Nonce tp -> Word64
indexValue Nonce b
y = forall a. a -> Maybe a
Just forall {k} (a :: k) (b :: k). a :~: b
unsafeAxiom
                   | Bool
otherwise = forall a. Maybe a
Nothing

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

instance HashableF Nonce where
  hashWithSaltF :: forall (tp :: k). Int -> Nonce tp -> Int
hashWithSaltF Int
s (Nonce Word64
x) = 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 :: forall {k} s (tp :: k). NonceGenerator s -> ST s (Nonce tp)
freshNonce (NonceGenerator STRef s Word64
r) = do
  Word64
i <- forall s a. STRef s a -> ST s a
readSTRef STRef s Word64
r
  forall s a. STRef s a -> a -> ST s ()
writeSTRef STRef s Word64
r forall a b. (a -> b) -> a -> b
$! forall a. Enum a => a -> a
succ Word64
i
  forall (m :: * -> *) a. Monad m => a -> m a
return (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 :: forall s. NonceGenerator s -> ST s Bool
atLimit (NonceGenerator STRef s Word64
r) = do
  Word64
i <- forall s a. STRef s a -> ST s a
readSTRef STRef s Word64
r
  forall (m :: * -> *) a. Monad m => a -> m a
return (Word64
i forall a. Eq a => a -> a -> Bool
== forall a. Bounded a => a
maxBound)