{-# LANGUAGE AllowAmbiguousTypes  #-}
{-# LANGUAGE DeriveAnyClass       #-}
{-# LANGUAGE OverloadedStrings    #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE UndecidableInstances #-}

module ZkFold.Symbolic.Data.JWT
    ( Certificate (..)
    , SigningKey (..)
    , TokenHeader (..)
    , TokenPayload (..)
    , Signature
    , ClientSecret (..)
    , IsSymbolicJSON (..)
    , SecretBits
    , secretBits
    , toAsciiBits
    , signPayload
    , verifySignature
    ) where

import           Control.DeepSeq                    (NFData, force)
import           Data.Aeson                         (FromJSON (..), genericParseJSON)
import qualified Data.Aeson                         as JSON
import           Data.Aeson.Casing                  (aesonPrefix, snakeCase)
import           Data.Constraint                    (Dict (..), withDict, (:-) (..))
import           Data.Constraint.Nat                (Max, divNat, minusNat, plusNat, timesNat)
import           Data.Constraint.Unsafe             (unsafeAxiom, unsafeSNat)
import           Data.Maybe                         (fromMaybe)
import           Data.Scientific                    (toBoundedInteger)
import qualified Data.Text                          as T
import           Generic.Random                     (genericArbitrary, uniform)
import           GHC.Generics                       (Generic, Par1 (..))
import           GHC.TypeLits                       (withKnownNat)
import           Prelude                            (fmap, pure, type (~), ($), (.), (<$>))
import qualified Prelude                            as P
import           Test.QuickCheck                    (Arbitrary (..))

import           ZkFold.Base.Algebra.Basic.Class
import           ZkFold.Base.Algebra.Basic.Number
import           ZkFold.Base.Data.HFunctor          (hmap)
import qualified ZkFold.Base.Data.Vector            as V
import           ZkFold.Base.Data.Vector            ((!!))
import           ZkFold.Symbolic.Algorithms.RSA
import           ZkFold.Symbolic.Class
import           ZkFold.Symbolic.Data.Bool
import           ZkFold.Symbolic.Data.ByteString    (ByteString (..), concat, toWords)
import           ZkFold.Symbolic.Data.Class
import           ZkFold.Symbolic.Data.Combinators
import           ZkFold.Symbolic.Data.Eq
import           ZkFold.Symbolic.Data.FieldElement
import           ZkFold.Symbolic.Data.Input         (SymbolicInput)
import           ZkFold.Symbolic.Data.UInt
import qualified ZkFold.Symbolic.Data.VarByteString as VB
import           ZkFold.Symbolic.Data.VarByteString (VarByteString (..), wipeUnassigned, (@+))
import           ZkFold.Symbolic.MonadCircuit       (newAssigned)


class IsSymbolicJSON a where
    type MaxLength a :: Natural

    toJsonBits :: a -> VarByteString (MaxLength a) (Context a)


-- | RSA Public key with Key ID
--
data Certificate ctx
    = Certificate
        { forall (ctx :: (Type -> Type) -> Type).
Certificate ctx -> VarByteString 320 ctx
pubKid :: VarByteString 320 ctx
        , forall (ctx :: (Type -> Type) -> Type).
Certificate ctx -> PublicKey 2048 ctx
pubKey :: PublicKey 2048 ctx
        }
    deriving (forall x. Certificate ctx -> Rep (Certificate ctx) x)
-> (forall x. Rep (Certificate ctx) x -> Certificate ctx)
-> Generic (Certificate ctx)
forall x. Rep (Certificate ctx) x -> Certificate ctx
forall x. Certificate ctx -> Rep (Certificate ctx) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (ctx :: (Type -> Type) -> Type) x.
Rep (Certificate ctx) x -> Certificate ctx
forall (ctx :: (Type -> Type) -> Type) x.
Certificate ctx -> Rep (Certificate ctx) x
$cfrom :: forall (ctx :: (Type -> Type) -> Type) x.
Certificate ctx -> Rep (Certificate ctx) x
from :: forall x. Certificate ctx -> Rep (Certificate ctx) x
$cto :: forall (ctx :: (Type -> Type) -> Type) x.
Rep (Certificate ctx) x -> Certificate ctx
to :: forall x. Rep (Certificate ctx) x -> Certificate ctx
Generic

deriving instance
    ( P.Eq (PublicKey 2048 ctx)
    , P.Eq (VarByteString 320 ctx)
    ) => P.Eq (Certificate ctx)
deriving instance
    ( P.Show (PublicKey 2048 ctx)
    , P.Show (VarByteString 320 ctx)
    ) => P.Show (Certificate ctx)
deriving instance
    ( NFData (PublicKey 2048 ctx)
    , NFData (VarByteString 320 ctx)
    ) => NFData (Certificate ctx)
instance
    ( SymbolicData (PublicKey 2048 ctx)
    , Symbolic ctx
    ) => SymbolicData (Certificate ctx)
instance
    ( SymbolicInput (PublicKey 2048 ctx)
    , Symbolic ctx
    ) => SymbolicInput (Certificate ctx)


-- | RSA Private key with Key ID
--
data SigningKey ctx
    = SigningKey
        { forall (ctx :: (Type -> Type) -> Type).
SigningKey ctx -> VarByteString 320 ctx
prvKid :: VarByteString 320 ctx
        , forall (ctx :: (Type -> Type) -> Type).
SigningKey ctx -> PrivateKey 2048 ctx
prvKey :: PrivateKey 2048 ctx
        }
    deriving (forall x. SigningKey ctx -> Rep (SigningKey ctx) x)
-> (forall x. Rep (SigningKey ctx) x -> SigningKey ctx)
-> Generic (SigningKey ctx)
forall x. Rep (SigningKey ctx) x -> SigningKey ctx
forall x. SigningKey ctx -> Rep (SigningKey ctx) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (ctx :: (Type -> Type) -> Type) x.
Rep (SigningKey ctx) x -> SigningKey ctx
forall (ctx :: (Type -> Type) -> Type) x.
SigningKey ctx -> Rep (SigningKey ctx) x
$cfrom :: forall (ctx :: (Type -> Type) -> Type) x.
SigningKey ctx -> Rep (SigningKey ctx) x
from :: forall x. SigningKey ctx -> Rep (SigningKey ctx) x
$cto :: forall (ctx :: (Type -> Type) -> Type) x.
Rep (SigningKey ctx) x -> SigningKey ctx
to :: forall x. Rep (SigningKey ctx) x -> SigningKey ctx
Generic

deriving instance
    ( P.Eq (PrivateKey 2048 ctx)
    , P.Eq (VarByteString 320 ctx)
    ) => P.Eq (SigningKey ctx)
deriving instance
    ( P.Show (PrivateKey 2048 ctx)
    , P.Show (VarByteString 320 ctx)
    ) => P.Show (SigningKey ctx)
deriving instance
    ( NFData (PrivateKey 2048 ctx)
    , NFData (VarByteString 320 ctx)
    ) => NFData (SigningKey ctx)
instance
    ( SymbolicData (PrivateKey 2048 ctx)
    , Symbolic ctx
    ) => SymbolicData (SigningKey ctx)
instance
    ( SymbolicInput (PrivateKey 2048 ctx)
    , Symbolic ctx
    ) => SymbolicInput (SigningKey ctx)

-- | Json Web Token header with information about encryption algorithm and signature
--
data TokenHeader ctx
    = TokenHeader
        { forall (ctx :: (Type -> Type) -> Type).
TokenHeader ctx -> VarByteString 72 ctx
hdAlg :: VarByteString 72 ctx
        -- ^ Signature or encryption algorithm
        , forall (ctx :: (Type -> Type) -> Type).
TokenHeader ctx -> VarByteString 320 ctx
hdKid :: VarByteString 320 ctx
        -- ^ Key ID
        , forall (ctx :: (Type -> Type) -> Type).
TokenHeader ctx -> VarByteString 32 ctx
hdTyp :: VarByteString 32 ctx
        -- ^ Type of token
        }
    deriving (forall x. TokenHeader ctx -> Rep (TokenHeader ctx) x)
-> (forall x. Rep (TokenHeader ctx) x -> TokenHeader ctx)
-> Generic (TokenHeader ctx)
forall x. Rep (TokenHeader ctx) x -> TokenHeader ctx
forall x. TokenHeader ctx -> Rep (TokenHeader ctx) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (ctx :: (Type -> Type) -> Type) x.
Rep (TokenHeader ctx) x -> TokenHeader ctx
forall (ctx :: (Type -> Type) -> Type) x.
TokenHeader ctx -> Rep (TokenHeader ctx) x
$cfrom :: forall (ctx :: (Type -> Type) -> Type) x.
TokenHeader ctx -> Rep (TokenHeader ctx) x
from :: forall x. TokenHeader ctx -> Rep (TokenHeader ctx) x
$cto :: forall (ctx :: (Type -> Type) -> Type) x.
Rep (TokenHeader ctx) x -> TokenHeader ctx
to :: forall x. Rep (TokenHeader ctx) x -> TokenHeader ctx
Generic

deriving instance
    ( P.Eq (ctx (V.Vector 72))
    , P.Eq (ctx (V.Vector 320))
    , P.Eq (ctx (V.Vector 32))
    , P.Eq (ctx Par1)
    ) => P.Eq (TokenHeader ctx)
deriving instance
    ( P.Show (ctx (V.Vector 72))
    , P.Show (ctx (V.Vector 320))
    , P.Show (ctx (V.Vector 32))
    , P.Show (ctx Par1)
    ) => P.Show (TokenHeader ctx)
deriving instance
    ( NFData (ctx (V.Vector 72))
    , NFData (ctx (V.Vector 320))
    , NFData (ctx (V.Vector 32))
    , NFData (ctx Par1)
    ) => NFData (TokenHeader ctx)

deriving instance Symbolic ctx => SymbolicData (TokenHeader ctx)
deriving instance Symbolic ctx => SymbolicInput (TokenHeader ctx)

instance Symbolic ctx => FromJSON (TokenHeader ctx) where
    parseJSON :: Value -> Parser (TokenHeader ctx)
parseJSON = Options -> Value -> Parser (TokenHeader ctx)
forall a.
(Generic a, GFromJSON Zero (Rep a)) =>
Options -> Value -> Parser a
genericParseJSON (Options -> Value -> Parser (TokenHeader ctx))
-> Options -> Value -> Parser (TokenHeader ctx)
forall a b. (a -> b) -> a -> b
$ ShowS -> Options
aesonPrefix ShowS
snakeCase

instance
    ( Symbolic ctx
    , Context (TokenHeader ctx) ~ ctx
    , NFData (VarByteString (MaxLength (TokenHeader ctx)) ctx)
    ) => IsSymbolicJSON (TokenHeader ctx) where

    type MaxLength (TokenHeader ctx) = 648
    toJsonBits :: TokenHeader ctx
-> VarByteString
     (MaxLength (TokenHeader ctx)) (Context (TokenHeader ctx))
toJsonBits TokenHeader{VarByteString 32 ctx
VarByteString 72 ctx
VarByteString 320 ctx
hdAlg :: forall (ctx :: (Type -> Type) -> Type).
TokenHeader ctx -> VarByteString 72 ctx
hdKid :: forall (ctx :: (Type -> Type) -> Type).
TokenHeader ctx -> VarByteString 320 ctx
hdTyp :: forall (ctx :: (Type -> Type) -> Type).
TokenHeader ctx -> VarByteString 32 ctx
hdAlg :: VarByteString 72 ctx
hdKid :: VarByteString 320 ctx
hdTyp :: VarByteString 32 ctx
..} = VarByteString
  (MaxLength (TokenHeader ctx)) (Context (TokenHeader ctx))
-> VarByteString
     (MaxLength (TokenHeader ctx)) (Context (TokenHeader ctx))
forall a. NFData a => a -> a
force (VarByteString
   (MaxLength (TokenHeader ctx)) (Context (TokenHeader ctx))
 -> VarByteString
      (MaxLength (TokenHeader ctx)) (Context (TokenHeader ctx)))
-> VarByteString
     (MaxLength (TokenHeader ctx)) (Context (TokenHeader ctx))
-> VarByteString
     (MaxLength (TokenHeader ctx)) (Context (TokenHeader ctx))
forall a b. (a -> b) -> a -> b
$
                    (forall (s :: Symbol) a. IsTypeString s a => a
fromType @"{\"alg\":\"")   VarByteString 64 ctx
-> VarByteString (72 + 72) ctx
-> VarByteString (64 + (72 + 72)) ctx
forall (m :: Natural) (n :: Natural)
       (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, KnownNat m, KnownNat (m + n)) =>
VarByteString m ctx
-> VarByteString n ctx -> VarByteString (m + n) ctx
@+ VarByteString 72 ctx
hdAlg
        VarByteString 72 ctx
-> VarByteString 72 ctx -> VarByteString (72 + 72) ctx
forall (m :: Natural) (n :: Natural)
       (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, KnownNat m, KnownNat (m + n)) =>
VarByteString m ctx
-> VarByteString n ctx -> VarByteString (m + n) ctx
`VB.append` (forall (s :: Symbol) a. IsTypeString s a => a
fromType @"\",\"kid\":\"") VarByteString (64 + (72 + 72)) ctx
-> VarByteString (320 + 72) ctx
-> VarByteString ((64 + (72 + 72)) + (320 + 72)) ctx
forall (m :: Natural) (n :: Natural)
       (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, KnownNat m, KnownNat (m + n)) =>
VarByteString m ctx
-> VarByteString n ctx -> VarByteString (m + n) ctx
@+ VarByteString 320 ctx
hdKid
        VarByteString 320 ctx
-> VarByteString 72 ctx -> VarByteString (320 + 72) ctx
forall (m :: Natural) (n :: Natural)
       (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, KnownNat m, KnownNat (m + n)) =>
VarByteString m ctx
-> VarByteString n ctx -> VarByteString (m + n) ctx
`VB.append` (forall (s :: Symbol) a. IsTypeString s a => a
fromType @"\",\"typ\":\"") VarByteString ((64 + (72 + 72)) + (320 + 72)) ctx
-> VarByteString (32 + 16) ctx
-> VarByteString (((64 + (72 + 72)) + (320 + 72)) + (32 + 16)) ctx
forall (m :: Natural) (n :: Natural)
       (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, KnownNat m, KnownNat (m + n)) =>
VarByteString m ctx
-> VarByteString n ctx -> VarByteString (m + n) ctx
@+ VarByteString 32 ctx
hdTyp
        VarByteString 32 ctx
-> VarByteString 16 ctx -> VarByteString (32 + 16) ctx
forall (m :: Natural) (n :: Natural)
       (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, KnownNat m, KnownNat (m + n)) =>
VarByteString m ctx
-> VarByteString n ctx -> VarByteString (m + n) ctx
`VB.append` (forall (s :: Symbol) a. IsTypeString s a => a
fromType @"\"}")


-- | Json Web Token payload with information about the issuer, bearer and TTL
--
data TokenPayload ctx
    = TokenPayload
        { forall (ctx :: (Type -> Type) -> Type).
TokenPayload ctx -> VarByteString 256 ctx
plIss           :: VarByteString 256 ctx
        -- ^ Issuer (who created and signed the token)
        , forall (ctx :: (Type -> Type) -> Type).
TokenPayload ctx -> VarByteString 1024 ctx
plAzp           :: VarByteString 1024 ctx
        -- ^ Authorized party (the party to which the token was issued)
        , forall (ctx :: (Type -> Type) -> Type).
TokenPayload ctx -> VarByteString 1024 ctx
plAud           :: VarByteString 1024 ctx
        -- ^ Audience (who or what the token is intended for)
        , forall (ctx :: (Type -> Type) -> Type).
TokenPayload ctx -> VarByteString 256 ctx
plSub           :: VarByteString 256 ctx
        -- ^ Subject (whom the token refers to)
        , forall (ctx :: (Type -> Type) -> Type).
TokenPayload ctx -> VarByteString 256 ctx
plHd            :: VarByteString 256 ctx
        -- ^ Hosted domain
        , forall (ctx :: (Type -> Type) -> Type).
TokenPayload ctx -> VarByteString 512 ctx
plEmail         :: VarByteString 512 ctx
        -- ^ User email limited to 64 characters
        , forall (ctx :: (Type -> Type) -> Type).
TokenPayload ctx -> VarByteString 40 ctx
plEmailVerified :: VarByteString 40 ctx
        -- ^ "true" or "false", max 5 bytes
        , forall (ctx :: (Type -> Type) -> Type).
TokenPayload ctx -> VarByteString 256 ctx
plAtHash        :: VarByteString 256 ctx
        -- ^ Access token hash value
        , forall (ctx :: (Type -> Type) -> Type).
TokenPayload ctx -> VarByteString 512 ctx
plName          :: VarByteString 512 ctx
        -- ^ Full name limited to 64 characters
        , forall (ctx :: (Type -> Type) -> Type).
TokenPayload ctx -> VarByteString 1024 ctx
plPicture       :: VarByteString 1024 ctx
        -- ^ URL to the profile picture limited to 128 characters
        , forall (ctx :: (Type -> Type) -> Type).
TokenPayload ctx -> VarByteString 256 ctx
plGivenName     :: VarByteString 256 ctx
        -- ^ Given name limited to 32 characters
        , forall (ctx :: (Type -> Type) -> Type).
TokenPayload ctx -> VarByteString 256 ctx
plFamilyName    :: VarByteString 256 ctx
        -- ^ Family name limited to 32 characters
        , forall (ctx :: (Type -> Type) -> Type).
TokenPayload ctx -> VarByteString 80 ctx
plIat           :: VarByteString 80 ctx
        -- ^ Issued at (seconds since Unix epoch), a decimal number
        , forall (ctx :: (Type -> Type) -> Type).
TokenPayload ctx -> VarByteString 80 ctx
plExp           :: VarByteString 80 ctx
        -- ^ Expiration time (seconds since Unix epoch), a decimal number
        }
    deriving (forall x. TokenPayload ctx -> Rep (TokenPayload ctx) x)
-> (forall x. Rep (TokenPayload ctx) x -> TokenPayload ctx)
-> Generic (TokenPayload ctx)
forall x. Rep (TokenPayload ctx) x -> TokenPayload ctx
forall x. TokenPayload ctx -> Rep (TokenPayload ctx) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (ctx :: (Type -> Type) -> Type) x.
Rep (TokenPayload ctx) x -> TokenPayload ctx
forall (ctx :: (Type -> Type) -> Type) x.
TokenPayload ctx -> Rep (TokenPayload ctx) x
$cfrom :: forall (ctx :: (Type -> Type) -> Type) x.
TokenPayload ctx -> Rep (TokenPayload ctx) x
from :: forall x. TokenPayload ctx -> Rep (TokenPayload ctx) x
$cto :: forall (ctx :: (Type -> Type) -> Type) x.
Rep (TokenPayload ctx) x -> TokenPayload ctx
to :: forall x. Rep (TokenPayload ctx) x -> TokenPayload ctx
Generic

deriving instance
    ( P.Eq (ctx (V.Vector 40))
    , P.Eq (ctx (V.Vector 80))
    , P.Eq (ctx (V.Vector 256))
    , P.Eq (ctx (V.Vector 512))
    , P.Eq (ctx (V.Vector 1024))
    , P.Eq (ctx Par1)
    ) => P.Eq (TokenPayload ctx)
deriving instance
    ( P.Show (ctx (V.Vector 40))
    , P.Show (ctx (V.Vector 80))
    , P.Show (ctx (V.Vector 256))
    , P.Show (ctx (V.Vector 512))
    , P.Show (ctx (V.Vector 1024))
    , P.Show (ctx Par1)
    ) => P.Show (TokenPayload ctx)
deriving instance Symbolic ctx => SymbolicData (TokenPayload ctx)
deriving instance Symbolic ctx => SymbolicInput (TokenPayload ctx)
instance Symbolic ctx => Arbitrary (TokenPayload ctx) where
    arbitrary :: Gen (TokenPayload ctx)
arbitrary = Weights (TokenPayload ctx) -> Gen (TokenPayload ctx)
forall a. GArbitrary UnsizedOpts a => Weights a -> Gen a
genericArbitrary Weights (TokenPayload ctx)
forall a. UniformWeight_ (Rep a) => Weights a
uniform

instance Symbolic ctx => FromJSON (TokenPayload ctx) where
    parseJSON :: Value -> Parser (TokenPayload ctx)
parseJSON = Options -> Value -> Parser (TokenPayload ctx)
forall a.
(Generic a, GFromJSON Zero (Rep a)) =>
Options -> Value -> Parser a
genericParseJSON (ShowS -> Options
aesonPrefix ShowS
snakeCase) (Value -> Parser (TokenPayload ctx))
-> (Value -> Value) -> Value -> Parser (TokenPayload ctx)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value -> Value
stringify
        where
            -- We store everything as ByteStrings for simplicity.
            -- We need to convert ints and bools to strings to avoid conversion errors
            --
            stringify :: JSON.Value -> JSON.Value
            stringify :: Value -> Value
stringify (JSON.Number Scientific
s) =
                Text -> Value
JSON.String (String -> Text
T.pack (String -> Text) -> (Scientific -> String) -> Scientific -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> String
forall a. Show a => a -> String
P.show (Int -> String) -> (Scientific -> Int) -> Scientific -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe (String -> Int
forall a. HasCallStack => String -> a
P.error String
"instance FromJSON JWT :: Invalid integer") (Maybe Int -> Int)
-> (Scientific -> Maybe Int) -> Scientific -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall i. (Integral i, Bounded i) => Scientific -> Maybe i
toBoundedInteger @P.Int (Scientific -> Text) -> Scientific -> Text
forall a b. (a -> b) -> a -> b
$ Scientific
s)
            stringify (JSON.Bool Bool
b)   = Text -> Value
JSON.String (String -> Text
T.pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ Bool -> String
forall a. Show a => a -> String
P.show Bool
b)
            stringify (JSON.Object Object
o) = Object -> Value
JSON.Object (Object -> Value) -> Object -> Value
forall a b. (a -> b) -> a -> b
$ (Value -> Value) -> Object -> Object
forall a b. (a -> b) -> KeyMap a -> KeyMap b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Value -> Value
stringify Object
o
            stringify Value
rest            = Value
rest

instance (Symbolic ctx, Context (TokenPayload ctx) ~ ctx) => IsSymbolicJSON (TokenPayload ctx) where
    type MaxLength (TokenPayload ctx) = 7088
    toJsonBits :: TokenPayload ctx
-> VarByteString
     (MaxLength (TokenPayload ctx)) (Context (TokenPayload ctx))
toJsonBits TokenPayload{VarByteString 40 ctx
VarByteString 80 ctx
VarByteString 256 ctx
VarByteString 512 ctx
VarByteString 1024 ctx
plIss :: forall (ctx :: (Type -> Type) -> Type).
TokenPayload ctx -> VarByteString 256 ctx
plAzp :: forall (ctx :: (Type -> Type) -> Type).
TokenPayload ctx -> VarByteString 1024 ctx
plAud :: forall (ctx :: (Type -> Type) -> Type).
TokenPayload ctx -> VarByteString 1024 ctx
plSub :: forall (ctx :: (Type -> Type) -> Type).
TokenPayload ctx -> VarByteString 256 ctx
plHd :: forall (ctx :: (Type -> Type) -> Type).
TokenPayload ctx -> VarByteString 256 ctx
plEmail :: forall (ctx :: (Type -> Type) -> Type).
TokenPayload ctx -> VarByteString 512 ctx
plEmailVerified :: forall (ctx :: (Type -> Type) -> Type).
TokenPayload ctx -> VarByteString 40 ctx
plAtHash :: forall (ctx :: (Type -> Type) -> Type).
TokenPayload ctx -> VarByteString 256 ctx
plName :: forall (ctx :: (Type -> Type) -> Type).
TokenPayload ctx -> VarByteString 512 ctx
plPicture :: forall (ctx :: (Type -> Type) -> Type).
TokenPayload ctx -> VarByteString 1024 ctx
plGivenName :: forall (ctx :: (Type -> Type) -> Type).
TokenPayload ctx -> VarByteString 256 ctx
plFamilyName :: forall (ctx :: (Type -> Type) -> Type).
TokenPayload ctx -> VarByteString 256 ctx
plIat :: forall (ctx :: (Type -> Type) -> Type).
TokenPayload ctx -> VarByteString 80 ctx
plExp :: forall (ctx :: (Type -> Type) -> Type).
TokenPayload ctx -> VarByteString 80 ctx
plIss :: VarByteString 256 ctx
plAzp :: VarByteString 1024 ctx
plAud :: VarByteString 1024 ctx
plSub :: VarByteString 256 ctx
plHd :: VarByteString 256 ctx
plEmail :: VarByteString 512 ctx
plEmailVerified :: VarByteString 40 ctx
plAtHash :: VarByteString 256 ctx
plName :: VarByteString 512 ctx
plPicture :: VarByteString 1024 ctx
plGivenName :: VarByteString 256 ctx
plFamilyName :: VarByteString 256 ctx
plIat :: VarByteString 80 ctx
plExp :: VarByteString 80 ctx
..} =
                    (forall (s :: Symbol) a. IsTypeString s a => a
fromType @"{\"iss\":\"")   VarByteString 64 ctx
-> VarByteString (256 + 72) ctx
-> VarByteString (64 + (256 + 72)) ctx
forall (m :: Natural) (n :: Natural)
       (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, KnownNat m, KnownNat (m + n)) =>
VarByteString m ctx
-> VarByteString n ctx -> VarByteString (m + n) ctx
@+ VarByteString 256 ctx
plIss
        VarByteString 256 ctx
-> VarByteString 72 ctx -> VarByteString (256 + 72) ctx
forall (m :: Natural) (n :: Natural)
       (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, KnownNat m, KnownNat (m + n)) =>
VarByteString m ctx
-> VarByteString n ctx -> VarByteString (m + n) ctx
`VB.append` (forall (s :: Symbol) a. IsTypeString s a => a
fromType @"\",\"azp\":\"") VarByteString (64 + (256 + 72)) ctx
-> VarByteString (1024 + 72) ctx
-> VarByteString ((64 + (256 + 72)) + (1024 + 72)) ctx
forall (m :: Natural) (n :: Natural)
       (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, KnownNat m, KnownNat (m + n)) =>
VarByteString m ctx
-> VarByteString n ctx -> VarByteString (m + n) ctx
@+ VarByteString 1024 ctx
plAzp
        VarByteString 1024 ctx
-> VarByteString 72 ctx -> VarByteString (1024 + 72) ctx
forall (m :: Natural) (n :: Natural)
       (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, KnownNat m, KnownNat (m + n)) =>
VarByteString m ctx
-> VarByteString n ctx -> VarByteString (m + n) ctx
`VB.append` (forall (s :: Symbol) a. IsTypeString s a => a
fromType @"\",\"aud\":\"") VarByteString ((64 + (256 + 72)) + (1024 + 72)) ctx
-> VarByteString (1024 + 72) ctx
-> VarByteString
     (((64 + (256 + 72)) + (1024 + 72)) + (1024 + 72)) ctx
forall (m :: Natural) (n :: Natural)
       (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, KnownNat m, KnownNat (m + n)) =>
VarByteString m ctx
-> VarByteString n ctx -> VarByteString (m + n) ctx
@+ VarByteString 1024 ctx
plAud
        VarByteString 1024 ctx
-> VarByteString 72 ctx -> VarByteString (1024 + 72) ctx
forall (m :: Natural) (n :: Natural)
       (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, KnownNat m, KnownNat (m + n)) =>
VarByteString m ctx
-> VarByteString n ctx -> VarByteString (m + n) ctx
`VB.append` (forall (s :: Symbol) a. IsTypeString s a => a
fromType @"\",\"sub\":\"") VarByteString (((64 + (256 + 72)) + (1024 + 72)) + (1024 + 72)) ctx
-> VarByteString (256 + 64) ctx
-> VarByteString
     ((((64 + (256 + 72)) + (1024 + 72)) + (1024 + 72)) + (256 + 64))
     ctx
forall (m :: Natural) (n :: Natural)
       (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, KnownNat m, KnownNat (m + n)) =>
VarByteString m ctx
-> VarByteString n ctx -> VarByteString (m + n) ctx
@+ VarByteString 256 ctx
plSub
        VarByteString 256 ctx
-> VarByteString 64 ctx -> VarByteString (256 + 64) ctx
forall (m :: Natural) (n :: Natural)
       (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, KnownNat m, KnownNat (m + n)) =>
VarByteString m ctx
-> VarByteString n ctx -> VarByteString (m + n) ctx
`VB.append` (forall (s :: Symbol) a. IsTypeString s a => a
fromType @"\",\"hd\":\"")  VarByteString
  ((((64 + (256 + 72)) + (1024 + 72)) + (1024 + 72)) + (256 + 64))
  ctx
-> VarByteString (256 + 88) ctx
-> VarByteString
     (((((64 + (256 + 72)) + (1024 + 72)) + (1024 + 72)) + (256 + 64))
      + (256 + 88))
     ctx
forall (m :: Natural) (n :: Natural)
       (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, KnownNat m, KnownNat (m + n)) =>
VarByteString m ctx
-> VarByteString n ctx -> VarByteString (m + n) ctx
@+ VarByteString 256 ctx
plHd
        VarByteString 256 ctx
-> VarByteString 88 ctx -> VarByteString (256 + 88) ctx
forall (m :: Natural) (n :: Natural)
       (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, KnownNat m, KnownNat (m + n)) =>
VarByteString m ctx
-> VarByteString n ctx -> VarByteString (m + n) ctx
`VB.append` (forall (s :: Symbol) a. IsTypeString s a => a
fromType @"\",\"email\":\"") VarByteString
  (((((64 + (256 + 72)) + (1024 + 72)) + (1024 + 72)) + (256 + 64))
   + (256 + 88))
  ctx
-> VarByteString (512 + 152) ctx
-> VarByteString
     ((((((64 + (256 + 72)) + (1024 + 72)) + (1024 + 72)) + (256 + 64))
       + (256 + 88))
      + (512 + 152))
     ctx
forall (m :: Natural) (n :: Natural)
       (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, KnownNat m, KnownNat (m + n)) =>
VarByteString m ctx
-> VarByteString n ctx -> VarByteString (m + n) ctx
@+ VarByteString 512 ctx
plEmail
        VarByteString 512 ctx
-> VarByteString 152 ctx -> VarByteString (512 + 152) ctx
forall (m :: Natural) (n :: Natural)
       (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, KnownNat m, KnownNat (m + n)) =>
VarByteString m ctx
-> VarByteString n ctx -> VarByteString (m + n) ctx
`VB.append` (forall (s :: Symbol) a. IsTypeString s a => a
fromType @"\",\"email_verified\":") VarByteString
  ((((((64 + (256 + 72)) + (1024 + 72)) + (1024 + 72)) + (256 + 64))
    + (256 + 88))
   + (512 + 152))
  ctx
-> VarByteString (40 + 96) ctx
-> VarByteString
     (((((((64 + (256 + 72)) + (1024 + 72)) + (1024 + 72)) + (256 + 64))
        + (256 + 88))
       + (512 + 152))
      + (40 + 96))
     ctx
forall (m :: Natural) (n :: Natural)
       (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, KnownNat m, KnownNat (m + n)) =>
VarByteString m ctx
-> VarByteString n ctx -> VarByteString (m + n) ctx
@+ VarByteString 40 ctx
plEmailVerified
        VarByteString 40 ctx
-> VarByteString 96 ctx -> VarByteString (40 + 96) ctx
forall (m :: Natural) (n :: Natural)
       (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, KnownNat m, KnownNat (m + n)) =>
VarByteString m ctx
-> VarByteString n ctx -> VarByteString (m + n) ctx
`VB.append` (forall (s :: Symbol) a. IsTypeString s a => a
fromType @",\"at_hash\":\"") VarByteString
  (((((((64 + (256 + 72)) + (1024 + 72)) + (1024 + 72)) + (256 + 64))
     + (256 + 88))
    + (512 + 152))
   + (40 + 96))
  ctx
-> VarByteString (256 + 80) ctx
-> VarByteString
     ((((((((64 + (256 + 72)) + (1024 + 72)) + (1024 + 72))
          + (256 + 64))
         + (256 + 88))
        + (512 + 152))
       + (40 + 96))
      + (256 + 80))
     ctx
forall (m :: Natural) (n :: Natural)
       (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, KnownNat m, KnownNat (m + n)) =>
VarByteString m ctx
-> VarByteString n ctx -> VarByteString (m + n) ctx
@+ VarByteString 256 ctx
plAtHash
        VarByteString 256 ctx
-> VarByteString 80 ctx -> VarByteString (256 + 80) ctx
forall (m :: Natural) (n :: Natural)
       (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, KnownNat m, KnownNat (m + n)) =>
VarByteString m ctx
-> VarByteString n ctx -> VarByteString (m + n) ctx
`VB.append` (forall (s :: Symbol) a. IsTypeString s a => a
fromType @"\",\"name\":\"")  VarByteString
  ((((((((64 + (256 + 72)) + (1024 + 72)) + (1024 + 72))
       + (256 + 64))
      + (256 + 88))
     + (512 + 152))
    + (40 + 96))
   + (256 + 80))
  ctx
-> VarByteString (512 + 104) ctx
-> VarByteString
     (((((((((64 + (256 + 72)) + (1024 + 72)) + (1024 + 72))
           + (256 + 64))
          + (256 + 88))
         + (512 + 152))
        + (40 + 96))
       + (256 + 80))
      + (512 + 104))
     ctx
forall (m :: Natural) (n :: Natural)
       (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, KnownNat m, KnownNat (m + n)) =>
VarByteString m ctx
-> VarByteString n ctx -> VarByteString (m + n) ctx
@+ VarByteString 512 ctx
plName
        VarByteString 512 ctx
-> VarByteString 104 ctx -> VarByteString (512 + 104) ctx
forall (m :: Natural) (n :: Natural)
       (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, KnownNat m, KnownNat (m + n)) =>
VarByteString m ctx
-> VarByteString n ctx -> VarByteString (m + n) ctx
`VB.append` (forall (s :: Symbol) a. IsTypeString s a => a
fromType @"\",\"picture\":\"") VarByteString
  (((((((((64 + (256 + 72)) + (1024 + 72)) + (1024 + 72))
        + (256 + 64))
       + (256 + 88))
      + (512 + 152))
     + (40 + 96))
    + (256 + 80))
   + (512 + 104))
  ctx
-> VarByteString (1024 + 128) ctx
-> VarByteString
     ((((((((((64 + (256 + 72)) + (1024 + 72)) + (1024 + 72))
            + (256 + 64))
           + (256 + 88))
          + (512 + 152))
         + (40 + 96))
        + (256 + 80))
       + (512 + 104))
      + (1024 + 128))
     ctx
forall (m :: Natural) (n :: Natural)
       (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, KnownNat m, KnownNat (m + n)) =>
VarByteString m ctx
-> VarByteString n ctx -> VarByteString (m + n) ctx
@+ VarByteString 1024 ctx
plPicture
        VarByteString 1024 ctx
-> VarByteString 128 ctx -> VarByteString (1024 + 128) ctx
forall (m :: Natural) (n :: Natural)
       (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, KnownNat m, KnownNat (m + n)) =>
VarByteString m ctx
-> VarByteString n ctx -> VarByteString (m + n) ctx
`VB.append` (forall (s :: Symbol) a. IsTypeString s a => a
fromType @"\",\"given_name\":\"")  VarByteString
  ((((((((((64 + (256 + 72)) + (1024 + 72)) + (1024 + 72))
         + (256 + 64))
        + (256 + 88))
       + (512 + 152))
      + (40 + 96))
     + (256 + 80))
    + (512 + 104))
   + (1024 + 128))
  ctx
-> VarByteString (256 + 136) ctx
-> VarByteString
     (((((((((((64 + (256 + 72)) + (1024 + 72)) + (1024 + 72))
             + (256 + 64))
            + (256 + 88))
           + (512 + 152))
          + (40 + 96))
         + (256 + 80))
        + (512 + 104))
       + (1024 + 128))
      + (256 + 136))
     ctx
forall (m :: Natural) (n :: Natural)
       (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, KnownNat m, KnownNat (m + n)) =>
VarByteString m ctx
-> VarByteString n ctx -> VarByteString (m + n) ctx
@+ VarByteString 256 ctx
plGivenName
        VarByteString 256 ctx
-> VarByteString 136 ctx -> VarByteString (256 + 136) ctx
forall (m :: Natural) (n :: Natural)
       (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, KnownNat m, KnownNat (m + n)) =>
VarByteString m ctx
-> VarByteString n ctx -> VarByteString (m + n) ctx
`VB.append` (forall (s :: Symbol) a. IsTypeString s a => a
fromType @"\",\"family_name\":\"") VarByteString
  (((((((((((64 + (256 + 72)) + (1024 + 72)) + (1024 + 72))
          + (256 + 64))
         + (256 + 88))
        + (512 + 152))
       + (40 + 96))
      + (256 + 80))
     + (512 + 104))
    + (1024 + 128))
   + (256 + 136))
  ctx
-> VarByteString (256 + 64) ctx
-> VarByteString
     ((((((((((((64 + (256 + 72)) + (1024 + 72)) + (1024 + 72))
              + (256 + 64))
             + (256 + 88))
            + (512 + 152))
           + (40 + 96))
          + (256 + 80))
         + (512 + 104))
        + (1024 + 128))
       + (256 + 136))
      + (256 + 64))
     ctx
forall (m :: Natural) (n :: Natural)
       (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, KnownNat m, KnownNat (m + n)) =>
VarByteString m ctx
-> VarByteString n ctx -> VarByteString (m + n) ctx
@+ VarByteString 256 ctx
plFamilyName
        VarByteString 256 ctx
-> VarByteString 64 ctx -> VarByteString (256 + 64) ctx
forall (m :: Natural) (n :: Natural)
       (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, KnownNat m, KnownNat (m + n)) =>
VarByteString m ctx
-> VarByteString n ctx -> VarByteString (m + n) ctx
`VB.append` (forall (s :: Symbol) a. IsTypeString s a => a
fromType @"\",\"iat\":") VarByteString
  ((((((((((((64 + (256 + 72)) + (1024 + 72)) + (1024 + 72))
           + (256 + 64))
          + (256 + 88))
         + (512 + 152))
        + (40 + 96))
       + (256 + 80))
      + (512 + 104))
     + (1024 + 128))
    + (256 + 136))
   + (256 + 64))
  ctx
-> VarByteString (80 + 56) ctx
-> VarByteString
     (((((((((((((64 + (256 + 72)) + (1024 + 72)) + (1024 + 72))
               + (256 + 64))
              + (256 + 88))
             + (512 + 152))
            + (40 + 96))
           + (256 + 80))
          + (512 + 104))
         + (1024 + 128))
        + (256 + 136))
       + (256 + 64))
      + (80 + 56))
     ctx
forall (m :: Natural) (n :: Natural)
       (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, KnownNat m, KnownNat (m + n)) =>
VarByteString m ctx
-> VarByteString n ctx -> VarByteString (m + n) ctx
@+ VarByteString 80 ctx
plIat
        VarByteString 80 ctx
-> VarByteString 56 ctx -> VarByteString (80 + 56) ctx
forall (m :: Natural) (n :: Natural)
       (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, KnownNat m, KnownNat (m + n)) =>
VarByteString m ctx
-> VarByteString n ctx -> VarByteString (m + n) ctx
`VB.append` (forall (s :: Symbol) a. IsTypeString s a => a
fromType @",\"exp\":")   VarByteString
  (((((((((((((64 + (256 + 72)) + (1024 + 72)) + (1024 + 72))
            + (256 + 64))
           + (256 + 88))
          + (512 + 152))
         + (40 + 96))
        + (256 + 80))
       + (512 + 104))
      + (1024 + 128))
     + (256 + 136))
    + (256 + 64))
   + (80 + 56))
  ctx
-> VarByteString (80 + 8) ctx
-> VarByteString
     ((((((((((((((64 + (256 + 72)) + (1024 + 72)) + (1024 + 72))
                + (256 + 64))
               + (256 + 88))
              + (512 + 152))
             + (40 + 96))
            + (256 + 80))
           + (512 + 104))
          + (1024 + 128))
         + (256 + 136))
        + (256 + 64))
       + (80 + 56))
      + (80 + 8))
     ctx
forall (m :: Natural) (n :: Natural)
       (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, KnownNat m, KnownNat (m + n)) =>
VarByteString m ctx
-> VarByteString n ctx -> VarByteString (m + n) ctx
@+ VarByteString 80 ctx
plExp
        VarByteString 80 ctx
-> VarByteString 8 ctx -> VarByteString (80 + 8) ctx
forall (m :: Natural) (n :: Natural)
       (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, KnownNat m, KnownNat (m + n)) =>
VarByteString m ctx
-> VarByteString n ctx -> VarByteString (m + n) ctx
`VB.append` (forall (s :: Symbol) a. IsTypeString s a => a
fromType @"}")

data ClientSecret ctx
    = ClientSecret
        { forall (ctx :: (Type -> Type) -> Type).
ClientSecret ctx -> TokenHeader ctx
csHeader    :: TokenHeader ctx
        , forall (ctx :: (Type -> Type) -> Type).
ClientSecret ctx -> TokenPayload ctx
csPayload   :: TokenPayload ctx
        , forall (ctx :: (Type -> Type) -> Type).
ClientSecret ctx -> Signature 2048 ctx
csSignature :: Signature 2048 ctx
        }
    deriving (forall x. ClientSecret ctx -> Rep (ClientSecret ctx) x)
-> (forall x. Rep (ClientSecret ctx) x -> ClientSecret ctx)
-> Generic (ClientSecret ctx)
forall x. Rep (ClientSecret ctx) x -> ClientSecret ctx
forall x. ClientSecret ctx -> Rep (ClientSecret ctx) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (ctx :: (Type -> Type) -> Type) x.
Rep (ClientSecret ctx) x -> ClientSecret ctx
forall (ctx :: (Type -> Type) -> Type) x.
ClientSecret ctx -> Rep (ClientSecret ctx) x
$cfrom :: forall (ctx :: (Type -> Type) -> Type) x.
ClientSecret ctx -> Rep (ClientSecret ctx) x
from :: forall x. ClientSecret ctx -> Rep (ClientSecret ctx) x
$cto :: forall (ctx :: (Type -> Type) -> Type) x.
Rep (ClientSecret ctx) x -> ClientSecret ctx
to :: forall x. Rep (ClientSecret ctx) x -> ClientSecret ctx
Generic

deriving instance
    ( NFData (TokenHeader ctx)
    , NFData (TokenPayload ctx)
    , NFData (Signature 2048 ctx)
    ) => NFData (ClientSecret ctx)
deriving instance Symbolic ctx => SymbolicData (ClientSecret ctx)
deriving instance Symbolic ctx => SymbolicInput (ClientSecret ctx)

-- | The lowest number of bits to store the padded length of a bytestring of @n@ bits
--
type BufLen n = Max (Log2 n + 1) 3

-- | The smallest multiple of 6 not less than @n@
--
type Next6 (n :: Natural) = (Div (n + 5) 6) * 6

-- | The number of bits required to store a base64 representation as an ASCII string
-- Each symbol in base64 requires 6 bits, but in ASCII it takes 8 bits, hence the ratio of 8/6
--
type ASCII (n :: Natural) = (Div n 6) * 8

---------------------------------------------------------------------------------------------------
    -- Helper axioms
---------------------------------------------------------------------------------------------------

knownBufLen' :: forall n . KnownNat n :- KnownNat (BufLen n)
knownBufLen' :: forall (n :: Natural). KnownNat n :- KnownNat (BufLen n)
knownBufLen' = (KnownNat n => Dict (KnownNat (BufLen n)))
-> KnownNat n :- KnownNat (BufLen n)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub ((KnownNat n => Dict (KnownNat (BufLen n)))
 -> KnownNat n :- KnownNat (BufLen n))
-> (KnownNat n => Dict (KnownNat (BufLen n)))
-> KnownNat n :- KnownNat (BufLen n)
forall a b. (a -> b) -> a -> b
$ forall (n :: Natural) r. SNat n -> (KnownNat n => r) -> r
withKnownNat @(BufLen n) (Natural -> SNat (BufLen n)
forall (n :: Natural). Natural -> SNat n
unsafeSNat (Natural -> SNat (BufLen n)) -> Natural -> SNat (BufLen n)
forall a b. (a -> b) -> a -> b
$ Natural -> Natural -> Natural
forall a. Ord a => a -> a -> a
P.max (Natural -> Natural
ilog2 (forall (n :: Natural). KnownNat n => Natural
value @n) Natural -> Natural -> Natural
forall a. AdditiveSemigroup a => a -> a -> a
+ Natural
1) Natural
3) Dict
  (KnownNat
     (If
        (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
        (Log2 n + 1)
        3))
KnownNat (BufLen n) =>
Dict
  (KnownNat
     (If
        (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
        (Log2 n + 1)
        3))
forall (a :: Constraint). a => Dict a
Dict

knownBufLen :: forall n {r} . KnownNat n => (KnownNat (BufLen n) => r) -> r
knownBufLen :: forall (n :: Natural) {r}.
KnownNat n =>
(KnownNat (BufLen n) => r) -> r
knownBufLen = (KnownNat n
 :- KnownNat
      (If
         (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
         (Log2 n + 1)
         3))
-> (KnownNat
      (If
         (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
         (Log2 n + 1)
         3) =>
    r)
-> r
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (forall (n :: Natural). KnownNat n :- KnownNat (BufLen n)
knownBufLen' @n)

monoAdd :: forall (a :: Natural) (b :: Natural) (c :: Natural) . (a <= b) :- (a <= (c + b))
monoAdd :: forall (a :: Natural) (b :: Natural) (c :: Natural).
(a <= b) :- (a <= (c + b))
monoAdd = (Assert
   (OrdCond (CmpNat a b) 'True 'True 'False) (TypeError ...) =>
 Dict
   (Assert
      (OrdCond (CmpNat a (c + b)) 'True 'True 'False) (TypeError ...)))
-> Assert (OrdCond (CmpNat a b) 'True 'True 'False) (TypeError ...)
   :- Assert
        (OrdCond (CmpNat a (c + b)) 'True 'True 'False) (TypeError ...)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub Dict
  (Assert
     (OrdCond (CmpNat a (c + b)) 'True 'True 'False) (TypeError ...))
Assert (OrdCond (CmpNat a b) 'True 'True 'False) (TypeError ...) =>
Dict
  (Assert
     (OrdCond (CmpNat a (c + b)) 'True 'True 'False) (TypeError ...))
forall (c :: Constraint). Dict c
unsafeAxiom

oneReg :: forall n c . Dict (NumberOfRegisters (BaseField c) (BufLen n) ('Fixed (BufLen n)) ~ 1)
oneReg :: forall (n :: Natural) (c :: (Type -> Type) -> Type).
Dict
  (NumberOfRegisters (BaseField c) (BufLen n) ('Fixed (BufLen n))
   ~ 1)
oneReg = Dict
  (NumberOfRegisters
     (BaseField c)
     (If
        (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
        (Log2 n + 1)
        3)
     ('Fixed
        (If
           (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
           (Log2 n + 1)
           3))
   ~ 1)
Dict
  (NumberOfRegisters
     (BaseField c) (Max (Log2 n + 1) 3) ('Fixed (Max (Log2 n + 1) 3))
   ~ 1)
forall (c :: Constraint). Dict c
unsafeAxiom -- @BufLen n@ is always greater than 2

knownOneReg' :: forall n c . Dict (KnownNat (NumberOfRegisters (BaseField c) (BufLen n) ('Fixed (BufLen n))))
knownOneReg' :: forall (n :: Natural) (c :: (Type -> Type) -> Type).
Dict
  (KnownNat
     (NumberOfRegisters (BaseField c) (BufLen n) ('Fixed (BufLen n))))
knownOneReg' = forall (n :: Natural) r. SNat n -> (KnownNat n => r) -> r
withKnownNat @(NumberOfRegisters (BaseField c) (BufLen n) ('Fixed (BufLen n))) (Natural
-> SNat
     (NumberOfRegisters
        (BaseField c)
        (If
           (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
           (Log2 n + 1)
           3)
        ('Fixed
           (If
              (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
              (Log2 n + 1)
              3)))
forall (n :: Natural). Natural -> SNat n
unsafeSNat Natural
1) Dict
  (KnownNat
     (NumberOfRegisters
        (BaseField c)
        (If
           (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
           (Log2 n + 1)
           3)
        ('Fixed
           (If
              (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
              (Log2 n + 1)
              3))))
KnownNat
  (NumberOfRegisters
     (BaseField c)
     (Max (Log2 n + 1) 3)
     ('Fixed (Max (Log2 n + 1) 3))) =>
Dict
  (KnownNat
     (NumberOfRegisters
        (BaseField c)
        (If
           (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
           (Log2 n + 1)
           3)
        ('Fixed
           (If
              (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
              (Log2 n + 1)
              3))))
forall (a :: Constraint). a => Dict a
Dict

knownOneReg :: forall n c {r} . (KnownNat (NumberOfRegisters (BaseField c) (BufLen n) ('Fixed (BufLen n))) => r) -> r
knownOneReg :: forall (n :: Natural) (c :: (Type -> Type) -> Type) {r}.
(KnownNat
   (NumberOfRegisters (BaseField c) (BufLen n) ('Fixed (BufLen n))) =>
 r)
-> r
knownOneReg = Dict
  (KnownNat
     (NumberOfRegisters
        (BaseField c)
        (If
           (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
           (Log2 n + 1)
           3)
        ('Fixed
           (If
              (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
              (Log2 n + 1)
              3))))
-> (KnownNat
      (NumberOfRegisters
         (BaseField c)
         (If
            (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
            (Log2 n + 1)
            3)
         ('Fixed
            (If
               (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
               (Log2 n + 1)
               3))) =>
    r)
-> r
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (forall (n :: Natural) (c :: (Type -> Type) -> Type).
Dict
  (KnownNat
     (NumberOfRegisters (BaseField c) (BufLen n) ('Fixed (BufLen n))))
knownOneReg' @n @c)

knownNumWords' :: forall n c . KnownNat n :- KnownNat (Div (GetRegisterSize (BaseField c) (BufLen n) ('Fixed (BufLen n)) + OrdWord - 1) OrdWord)
knownNumWords' :: forall (n :: Natural) (c :: (Type -> Type) -> Type).
KnownNat n
:- KnownNat
     (Div
        ((GetRegisterSize (BaseField c) (BufLen n) ('Fixed (BufLen n))
          + 16)
         - 1)
        16)
knownNumWords' = (KnownNat n =>
 Dict
   (KnownNat
      (Div
         ((GetRegisterSize (BaseField c) (BufLen n) ('Fixed (BufLen n))
           + 16)
          - 1)
         16)))
-> KnownNat n
   :- KnownNat
        (Div
           ((GetRegisterSize (BaseField c) (BufLen n) ('Fixed (BufLen n))
             + 16)
            - 1)
           16)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub ((KnownNat n =>
  Dict
    (KnownNat
       (Div
          ((GetRegisterSize (BaseField c) (BufLen n) ('Fixed (BufLen n))
            + 16)
           - 1)
          16)))
 -> KnownNat n
    :- KnownNat
         (Div
            ((GetRegisterSize (BaseField c) (BufLen n) ('Fixed (BufLen n))
              + 16)
             - 1)
            16))
-> (KnownNat n =>
    Dict
      (KnownNat
         (Div
            ((GetRegisterSize (BaseField c) (BufLen n) ('Fixed (BufLen n))
              + 16)
             - 1)
            16)))
-> KnownNat n
   :- KnownNat
        (Div
           ((GetRegisterSize (BaseField c) (BufLen n) ('Fixed (BufLen n))
             + 16)
            - 1)
           16)
forall a b. (a -> b) -> a -> b
$
    forall (n :: Natural) r. SNat n -> (KnownNat n => r) -> r
withKnownNat @(Div (GetRegisterSize (BaseField c) (BufLen n) ('Fixed (BufLen n)) + OrdWord - 1) OrdWord)
        (Natural
-> SNat
     (Div
        ((GetRegisterSize (BaseField c) (BufLen n) ('Fixed (BufLen n))
          + 16)
         - 1)
        16)
forall (n :: Natural). Natural -> SNat n
unsafeSNat (Natural
 -> SNat
      (Div
         ((GetRegisterSize (BaseField c) (BufLen n) ('Fixed (BufLen n))
           + 16)
          - 1)
         16))
-> Natural
-> SNat
     (Div
        ((GetRegisterSize (BaseField c) (BufLen n) ('Fixed (BufLen n))
          + 16)
         - 1)
        16)
forall a b. (a -> b) -> a -> b
$ forall (n :: Natural) {r}.
KnownNat n =>
(KnownNat (BufLen n) => r) -> r
knownBufLen @n ((KnownNat (BufLen n) => Natural) -> Natural)
-> (KnownNat (BufLen n) => Natural) -> Natural
forall a b. (a -> b) -> a -> b
$ Natural -> Natural
wordSize (forall (n :: Natural). KnownNat n => Natural
value @(BufLen n)))
        Dict
  (KnownNat
     (Div
        ((GetRegisterSize
            (BaseField c)
            (If
               (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
               (Log2 n + 1)
               3)
            ('Fixed
               (If
                  (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
                  (Log2 n + 1)
                  3))
          + 16)
         - 1)
        16))
KnownNat
  (Div
     ((GetRegisterSize (BaseField c) (BufLen n) ('Fixed (BufLen n))
       + 16)
      - 1)
     16) =>
Dict
  (KnownNat
     (Div
        ((GetRegisterSize
            (BaseField c)
            (If
               (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
               (Log2 n + 1)
               3)
            ('Fixed
               (If
                  (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
                  (Log2 n + 1)
                  3))
          + 16)
         - 1)
        16))
forall (a :: Constraint). a => Dict a
Dict
    where
        wordSize :: Natural -> Natural
        wordSize :: Natural -> Natural
wordSize Natural
n = (Natural
n Natural -> Natural -> Natural
forall a. AdditiveSemigroup a => a -> a -> a
+ (forall (n :: Natural). KnownNat n => Natural
value @OrdWord) Natural -> Natural -> Natural
-! Natural
1) Natural -> Natural -> Natural
forall a. SemiEuclidean a => a -> a -> a
`div` (forall (n :: Natural). KnownNat n => Natural
value @OrdWord)

knownNumWords :: forall n c {r} . KnownNat n => (KnownNat (Div (GetRegisterSize (BaseField c) (BufLen n) ('Fixed (BufLen n)) + OrdWord - 1) OrdWord) => r) -> r
knownNumWords :: forall (n :: Natural) (c :: (Type -> Type) -> Type) {r}.
KnownNat n =>
(KnownNat
   (Div
      ((GetRegisterSize (BaseField c) (BufLen n) ('Fixed (BufLen n))
        + 16)
       - 1)
      16) =>
 r)
-> r
knownNumWords = (KnownNat n
 :- KnownNat
      (Div
         ((GetRegisterSize
             (BaseField c)
             (If
                (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
                (Log2 n + 1)
                3)
             ('Fixed
                (If
                   (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
                   (Log2 n + 1)
                   3))
           + 16)
          - 1)
         16))
-> (KnownNat
      (Div
         ((GetRegisterSize
             (BaseField c)
             (If
                (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
                (Log2 n + 1)
                3)
             ('Fixed
                (If
                   (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
                   (Log2 n + 1)
                   3))
           + 16)
          - 1)
         16) =>
    r)
-> r
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (forall (n :: Natural) (c :: (Type -> Type) -> Type).
KnownNat n
:- KnownNat
     (Div
        ((GetRegisterSize (BaseField c) (BufLen n) ('Fixed (BufLen n))
          + 16)
         - 1)
        16)
knownNumWords' @n @c)

withDiv :: forall n {r}. KnownNat n => (KnownNat (Div ((n + OrdWord) - 1) OrdWord) => r) -> r
withDiv :: forall (n :: Natural) {r}.
KnownNat n =>
(KnownNat (Div ((n + 16) - 1) 16) => r) -> r
withDiv =
    ((KnownNat n, KnownNat 16) :- KnownNat (n + 16))
-> (KnownNat (n + 16) =>
    (KnownNat (Div ((n + 16) - 1) 16) => r) -> r)
-> (KnownNat (Div ((n + 16) - 1) 16) => r)
-> r
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (forall (n :: Natural) (m :: Natural).
(KnownNat n, KnownNat m) :- KnownNat (n + m)
plusNat @n @OrdWord) ((KnownNat (n + 16) =>
  (KnownNat (Div ((n + 16) - 1) 16) => r) -> r)
 -> (KnownNat (Div ((n + 16) - 1) 16) => r) -> r)
-> (KnownNat (n + 16) =>
    (KnownNat (Div ((n + 16) - 1) 16) => r) -> r)
-> (KnownNat (Div ((n + 16) - 1) 16) => r)
-> r
forall a b. (a -> b) -> a -> b
$
        ((() :: Constraint)
 :- Assert
      (OrdCond (CmpNat 1 (n + 16)) 'True 'True 'False) (TypeError ...))
-> (Assert
      (OrdCond (CmpNat 1 (n + 16)) 'True 'True 'False) (TypeError ...) =>
    (KnownNat (Div ((n + 16) - 1) 16) => r) -> r)
-> (KnownNat (Div ((n + 16) - 1) 16) => r)
-> r
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (forall (a :: Natural) (b :: Natural) (c :: Natural).
(a <= b) :- (a <= (c + b))
monoAdd @1 @OrdWord @n) ((Assert
    (OrdCond (CmpNat 1 (n + 16)) 'True 'True 'False) (TypeError ...) =>
  (KnownNat (Div ((n + 16) - 1) 16) => r) -> r)
 -> (KnownNat (Div ((n + 16) - 1) 16) => r) -> r)
-> (Assert
      (OrdCond (CmpNat 1 (n + 16)) 'True 'True 'False) (TypeError ...) =>
    (KnownNat (Div ((n + 16) - 1) 16) => r) -> r)
-> (KnownNat (Div ((n + 16) - 1) 16) => r)
-> r
forall a b. (a -> b) -> a -> b
$
            ((KnownNat (n + 16), KnownNat 1,
  Assert
    (OrdCond (CmpNat 1 (n + 16)) 'True 'True 'False) (TypeError ...))
 :- KnownNat ((n + 16) - 1))
-> (KnownNat ((n + 16) - 1) =>
    (KnownNat (Div ((n + 16) - 1) 16) => r) -> r)
-> (KnownNat (Div ((n + 16) - 1) 16) => r)
-> r
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (forall (n :: Natural) (m :: Natural).
(KnownNat n, KnownNat m, m <= n) :- KnownNat (n - m)
minusNat @(n + OrdWord) @1) ((KnownNat ((n + 16) - 1) =>
  (KnownNat (Div ((n + 16) - 1) 16) => r) -> r)
 -> (KnownNat (Div ((n + 16) - 1) 16) => r) -> r)
-> (KnownNat ((n + 16) - 1) =>
    (KnownNat (Div ((n + 16) - 1) 16) => r) -> r)
-> (KnownNat (Div ((n + 16) - 1) 16) => r)
-> r
forall a b. (a -> b) -> a -> b
$
                ((KnownNat ((n + 16) - 1), KnownNat 16, () :: Constraint)
 :- KnownNat (Div ((n + 16) - 1) 16))
-> (KnownNat (Div ((n + 16) - 1) 16) => r) -> r
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (forall (n :: Natural) (m :: Natural).
(KnownNat n, KnownNat m, 1 <= m) :- KnownNat (Div n m)
divNat @(n + OrdWord - 1) @OrdWord)

withNext6 :: forall n {r}. KnownNat n => (KnownNat (Next6 n) => r) -> r
withNext6 :: forall (n :: Natural) {r}.
KnownNat n =>
(KnownNat (Next6 n) => r) -> r
withNext6 =
    ((KnownNat n, KnownNat 5) :- KnownNat (n + 5))
-> (KnownNat (n + 5) => (KnownNat (Next6 n) => r) -> r)
-> (KnownNat (Next6 n) => r)
-> r
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (forall (n :: Natural) (m :: Natural).
(KnownNat n, KnownNat m) :- KnownNat (n + m)
plusNat @n @5) ((KnownNat (n + 5) => (KnownNat (Next6 n) => r) -> r)
 -> (KnownNat (Next6 n) => r) -> r)
-> (KnownNat (n + 5) => (KnownNat (Next6 n) => r) -> r)
-> (KnownNat (Next6 n) => r)
-> r
forall a b. (a -> b) -> a -> b
$
        ((KnownNat (n + 5), KnownNat 6, () :: Constraint)
 :- KnownNat (Div (n + 5) 6))
-> (KnownNat (Div (n + 5) 6) => (KnownNat (Next6 n) => r) -> r)
-> (KnownNat (Next6 n) => r)
-> r
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (forall (n :: Natural) (m :: Natural).
(KnownNat n, KnownNat m, 1 <= m) :- KnownNat (Div n m)
divNat @(n + 5) @6) ((KnownNat (Div (n + 5) 6) => (KnownNat (Next6 n) => r) -> r)
 -> (KnownNat (Next6 n) => r) -> r)
-> (KnownNat (Div (n + 5) 6) => (KnownNat (Next6 n) => r) -> r)
-> (KnownNat (Next6 n) => r)
-> r
forall a b. (a -> b) -> a -> b
$
            ((KnownNat (Div (n + 5) 6), KnownNat 6) :- KnownNat (Next6 n))
-> (KnownNat (Next6 n) => r) -> r
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (forall (n :: Natural) (m :: Natural).
(KnownNat n, KnownNat m) :- KnownNat (n * m)
timesNat @(Div (n + 5) 6) @6)

withAscii :: forall n {r}. KnownNat n => (KnownNat (ASCII n) => r) -> r
withAscii :: forall (n :: Natural) {r}.
KnownNat n =>
(KnownNat (ASCII n) => r) -> r
withAscii =
    ((KnownNat n, KnownNat 6, () :: Constraint) :- KnownNat (Div n 6))
-> (KnownNat (Div n 6) => (KnownNat (ASCII n) => r) -> r)
-> (KnownNat (ASCII n) => r)
-> r
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (forall (n :: Natural) (m :: Natural).
(KnownNat n, KnownNat m, 1 <= m) :- KnownNat (Div n m)
divNat @n @6) ((KnownNat (Div n 6) => (KnownNat (ASCII n) => r) -> r)
 -> (KnownNat (ASCII n) => r) -> r)
-> (KnownNat (Div n 6) => (KnownNat (ASCII n) => r) -> r)
-> (KnownNat (ASCII n) => r)
-> r
forall a b. (a -> b) -> a -> b
$
        ((KnownNat (Div n 6), KnownNat 8) :- KnownNat (ASCII n))
-> (KnownNat (ASCII n) => r) -> r
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (forall (n :: Natural) (m :: Natural).
(KnownNat n, KnownNat m) :- KnownNat (n * m)
timesNat @(Div n 6) @8)

divMul :: forall a b . (Mod a b ~ 0) :- ((Div a b) * b ~ a)
divMul :: forall (a :: Natural) (b :: Natural).
(Mod a b ~ 0) :- ((Div a b * b) ~ a)
divMul = ((Mod a b ~ 0) => Dict ((Div a b * b) ~ a))
-> (Mod a b ~ 0) :- ((Div a b * b) ~ a)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub Dict ((Div a b * b) ~ a)
(Mod a b ~ 0) => Dict ((Div a b * b) ~ a)
forall (c :: Constraint). Dict c
unsafeAxiom

mulMod :: forall n . Dict (Mod (Next6 n) 6 ~ 0)
mulMod :: forall (n :: Natural). Dict (Mod (Next6 n) 6 ~ 0)
mulMod = Dict (Mod (Div (n + 5) 6 * 6) 6 ~ 0)
forall (c :: Constraint). Dict c
unsafeAxiom

withDivMul :: forall a b {r}. (Mod a b ~ 0) => ((Div a b) * b ~ a => r) -> r
withDivMul :: forall (a :: Natural) (b :: Natural) {r}.
(Mod a b ~ 0) =>
(((Div a b * b) ~ a) => r) -> r
withDivMul = ((0 ~ 0) :- ((Div a b * b) ~ a)) -> (((Div a b * b) ~ a) => r) -> r
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (forall (a :: Natural) (b :: Natural).
(Mod a b ~ 0) :- ((Div a b * b) ~ a)
divMul @a @b)

---------------------------------------------------------------------------------------------------

feToUInt :: forall n ctx . Symbolic ctx => FieldElement ctx -> UInt (BufLen n) ('Fixed (BufLen n)) ctx
feToUInt :: forall (n :: Natural) (ctx :: (Type -> Type) -> Type).
Symbolic ctx =>
FieldElement ctx -> UInt (BufLen n) ('Fixed (BufLen n)) ctx
feToUInt (FieldElement ctx Par1
c) = ctx
  (Vector
     (NumberOfRegisters (BaseField ctx) (BufLen n) ('Fixed (BufLen n))))
-> UInt (BufLen n) ('Fixed (BufLen n)) ctx
forall (n :: Natural) (r :: RegisterSize)
       (context :: (Type -> Type) -> Type).
context (Vector (NumberOfRegisters (BaseField context) n r))
-> UInt n r context
UInt (ctx
   (Vector
      (NumberOfRegisters (BaseField ctx) (BufLen n) ('Fixed (BufLen n))))
 -> UInt (BufLen n) ('Fixed (BufLen n)) ctx)
-> ctx
     (Vector
        (NumberOfRegisters (BaseField ctx) (BufLen n) ('Fixed (BufLen n))))
-> UInt (BufLen n) ('Fixed (BufLen n)) ctx
forall a b. (a -> b) -> a -> b
$ Dict
  (NumberOfRegisters
     (BaseField ctx)
     (If
        (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
        (Log2 n + 1)
        3)
     ('Fixed
        (If
           (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
           (Log2 n + 1)
           3))
   ~ 1)
-> ((NumberOfRegisters
       (BaseField ctx)
       (If
          (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
          (Log2 n + 1)
          3)
       ('Fixed
          (If
             (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
             (Log2 n + 1)
             3))
     ~ 1) =>
    ctx
      (Vector
         (NumberOfRegisters
            (BaseField ctx) (BufLen n) ('Fixed (BufLen n)))))
-> ctx
     (Vector
        (NumberOfRegisters (BaseField ctx) (BufLen n) ('Fixed (BufLen n))))
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (forall (n :: Natural) (c :: (Type -> Type) -> Type).
Dict
  (NumberOfRegisters (BaseField c) (BufLen n) ('Fixed (BufLen n))
   ~ 1)
oneReg @n @ctx) (((NumberOfRegisters
     (BaseField ctx)
     (If
        (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
        (Log2 n + 1)
        3)
     ('Fixed
        (If
           (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
           (Log2 n + 1)
           3))
   ~ 1) =>
  ctx
    (Vector
       (NumberOfRegisters
          (BaseField ctx) (BufLen n) ('Fixed (BufLen n)))))
 -> ctx
      (Vector
         (NumberOfRegisters
            (BaseField ctx) (BufLen n) ('Fixed (BufLen n)))))
-> ((NumberOfRegisters
       (BaseField ctx)
       (If
          (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
          (Log2 n + 1)
          3)
       ('Fixed
          (If
             (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
             (Log2 n + 1)
             3))
     ~ 1) =>
    ctx
      (Vector
         (NumberOfRegisters
            (BaseField ctx) (BufLen n) ('Fixed (BufLen n)))))
-> ctx
     (Vector
        (NumberOfRegisters (BaseField ctx) (BufLen n) ('Fixed (BufLen n))))
forall a b. (a -> b) -> a -> b
$ (forall a. Par1 a -> Vector 1 a) -> ctx Par1 -> ctx (Vector 1)
forall {k} (c :: (k -> Type) -> Type) (f :: k -> Type)
       (g :: k -> Type).
HFunctor c =>
(forall (a :: k). f a -> g a) -> c f -> c g
forall (f :: Type -> Type) (g :: Type -> Type).
(forall a. f a -> g a) -> ctx f -> ctx g
hmap (a -> Vector 1 a
forall a. a -> Vector 1 a
V.singleton (a -> Vector 1 a) -> (Par1 a -> a) -> Par1 a -> Vector 1 a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Par1 a -> a
forall p. Par1 p -> p
unPar1) ctx Par1
c

uintToFe :: forall n ctx . Symbolic ctx => UInt (BufLen n) ('Fixed (BufLen n)) ctx -> FieldElement ctx
uintToFe :: forall (n :: Natural) (ctx :: (Type -> Type) -> Type).
Symbolic ctx =>
UInt (BufLen n) ('Fixed (BufLen n)) ctx -> FieldElement ctx
uintToFe (UInt ctx
  (Vector
     (NumberOfRegisters (BaseField ctx) (BufLen n) ('Fixed (BufLen n))))
v) = ctx Par1 -> FieldElement ctx
forall (c :: (Type -> Type) -> Type). c Par1 -> FieldElement c
FieldElement (ctx Par1 -> FieldElement ctx) -> ctx Par1 -> FieldElement ctx
forall a b. (a -> b) -> a -> b
$ Dict
  (NumberOfRegisters
     (BaseField ctx)
     (If
        (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
        (Log2 n + 1)
        3)
     ('Fixed
        (If
           (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
           (Log2 n + 1)
           3))
   ~ 1)
-> ((NumberOfRegisters
       (BaseField ctx)
       (If
          (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
          (Log2 n + 1)
          3)
       ('Fixed
          (If
             (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
             (Log2 n + 1)
             3))
     ~ 1) =>
    ctx Par1)
-> ctx Par1
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (forall (n :: Natural) (c :: (Type -> Type) -> Type).
Dict
  (NumberOfRegisters (BaseField c) (BufLen n) ('Fixed (BufLen n))
   ~ 1)
oneReg @n @ctx) (((NumberOfRegisters
     (BaseField ctx)
     (If
        (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
        (Log2 n + 1)
        3)
     ('Fixed
        (If
           (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
           (Log2 n + 1)
           3))
   ~ 1) =>
  ctx Par1)
 -> ctx Par1)
-> ((NumberOfRegisters
       (BaseField ctx)
       (If
          (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
          (Log2 n + 1)
          3)
       ('Fixed
          (If
             (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
             (Log2 n + 1)
             3))
     ~ 1) =>
    ctx Par1)
-> ctx Par1
forall a b. (a -> b) -> a -> b
$ (forall a. Vector 1 a -> Par1 a) -> ctx (Vector 1) -> ctx Par1
forall {k} (c :: (k -> Type) -> Type) (f :: k -> Type)
       (g :: k -> Type).
HFunctor c =>
(forall (a :: k). f a -> g a) -> c f -> c g
forall (f :: Type -> Type) (g :: Type -> Type).
(forall a. f a -> g a) -> ctx f -> ctx g
hmap (a -> Par1 a
forall p. p -> Par1 p
Par1 (a -> Par1 a) -> (Vector 1 a -> a) -> Vector 1 a -> Par1 a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vector 1 a -> a
forall a. Vector 1 a -> a
V.item) ctx (Vector 1)
ctx
  (Vector
     (NumberOfRegisters (BaseField ctx) (BufLen n) ('Fixed (BufLen n))))
v

-- | The smallest multiple of 6 not less than the given UInt
--
padTo6
    :: forall n ctx
    .  Symbolic ctx
    => KnownNat n
    => UInt (BufLen n) ('Fixed (BufLen n)) ctx
    -> FieldElement ctx
padTo6 :: forall (n :: Natural) (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, KnownNat n) =>
UInt (BufLen n) ('Fixed (BufLen n)) ctx -> FieldElement ctx
padTo6 UInt (BufLen n) ('Fixed (BufLen n)) ctx
ui = ctx Par1 -> FieldElement ctx
forall (c :: (Type -> Type) -> Type). c Par1 -> FieldElement c
FieldElement (ctx Par1 -> FieldElement ctx) -> ctx Par1 -> FieldElement ctx
forall a b. (a -> b) -> a -> b
$ ctx
  (Vector
     (NumberOfRegisters
        (BaseField ctx)
        (If
           (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
           (Log2 n + 1)
           3)
        ('Fixed
           (If
              (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
              (Log2 n + 1)
              3))))
-> (forall {i} {m :: Type -> Type}.
    (NFData i, MonadCircuit i (BaseField ctx) (WitnessField ctx) m) =>
    FunBody
      '[Vector
          (NumberOfRegisters
             (BaseField ctx)
             (If
                (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
                (Log2 n + 1)
                3)
             ('Fixed
                (If
                   (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
                   (Log2 n + 1)
                   3)))]
      Par1
      i
      m)
-> ctx Par1
forall (f :: Type -> Type) (g :: Type -> Type).
ctx f -> CircuitFun '[f] g ctx -> ctx g
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type)
       (g :: Type -> Type).
Symbolic c =>
c f -> CircuitFun '[f] g c -> c g
fromCircuitF ctx
  (Vector
     (NumberOfRegisters
        (BaseField ctx)
        (If
           (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
           (Log2 n + 1)
           3)
        ('Fixed
           (If
              (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
              (Log2 n + 1)
              3))))
v ((forall {i} {m :: Type -> Type}.
  (NFData i, MonadCircuit i (BaseField ctx) (WitnessField ctx) m) =>
  FunBody
    '[Vector
        (NumberOfRegisters
           (BaseField ctx)
           (If
              (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
              (Log2 n + 1)
              3)
           ('Fixed
              (If
                 (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
                 (Log2 n + 1)
                 3)))]
    Par1
    i
    m)
 -> ctx Par1)
-> (forall {i} {m :: Type -> Type}.
    (NFData i, MonadCircuit i (BaseField ctx) (WitnessField ctx) m) =>
    FunBody
      '[Vector
          (NumberOfRegisters
             (BaseField ctx)
             (If
                (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
                (Log2 n + 1)
                3)
             ('Fixed
                (If
                   (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
                   (Log2 n + 1)
                   3)))]
      Par1
      i
      m)
-> ctx Par1
forall a b. (a -> b) -> a -> b
$ \Vector
  (NumberOfRegisters
     (BaseField ctx)
     (If
        (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
        (Log2 n + 1)
        3)
     ('Fixed
        (If
           (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
           (Log2 n + 1)
           3)))
  i
bits ->
    do
        i
val <- [i] -> m i
forall i a w (m :: Type -> Type).
MonadCircuit i a w m =>
[i] -> m i
horner ([i] -> m i) -> [i] -> m i
forall a b. (a -> b) -> a -> b
$ Vector
  (NumberOfRegisters
     (BaseField ctx)
     (If
        (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
        (Log2 n + 1)
        3)
     ('Fixed
        (If
           (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
           (Log2 n + 1)
           3)))
  i
-> [i]
forall (size :: Natural) a. Vector size a -> [a]
V.fromVector Vector
  (NumberOfRegisters
     (BaseField ctx)
     (If
        (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
        (Log2 n + 1)
        3)
     ('Fixed
        (If
           (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
           (Log2 n + 1)
           3)))
  i
bits

        i
toPad <- ClosedPoly i (BaseField ctx) -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m var
newAssigned (ClosedPoly i (BaseField ctx) -> m i)
-> ClosedPoly i (BaseField ctx) -> m i
forall a b. (a -> b) -> a -> b
$ \i -> x
p -> forall a b. FromConstant a b => a -> b
fromConstant @Natural Natural
6 x -> x -> x
forall a. AdditiveGroup a => a -> a -> a
- i -> x
p i
val
        Vector 3 i
valBits <- forall (size :: Natural) a. [a] -> Vector size a
V.unsafeToVector @3 ([i] -> Vector 3 i) -> m [i] -> m (Vector 3 i)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Natural -> i -> m [i]
forall i a w (m :: Type -> Type).
(MonadCircuit i a w m, Arithmetic a) =>
Natural -> i -> m [i]
expansion Natural
3 i
toPad

        i
f <- ClosedPoly i (BaseField ctx) -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m var
newAssigned (ClosedPoly i (BaseField ctx) -> m i)
-> ClosedPoly i (BaseField ctx) -> m i
forall a b. (a -> b) -> a -> b
$ \i -> x
p -> x
forall a. MultiplicativeMonoid a => a
one x -> x -> x
forall a. AdditiveGroup a => a -> a -> a
- i -> x
p (Vector 3 i
valBits Vector 3 i -> Natural -> i
forall (size :: Natural) a. Vector size a -> Natural -> a
!! Natural
1) x -> x -> x
forall a. MultiplicativeSemigroup a => a -> a -> a
* i -> x
p (Vector 3 i
valBits Vector 3 i -> Natural -> i
forall (size :: Natural) a. Vector size a -> Natural -> a
!! Natural
2)
        i
hi1 <- ClosedPoly i (BaseField ctx) -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m var
newAssigned (ClosedPoly i (BaseField ctx) -> m i)
-> ClosedPoly i (BaseField ctx) -> m i
forall a b. (a -> b) -> a -> b
$ \i -> x
p -> i -> x
p i
f x -> x -> x
forall a. MultiplicativeSemigroup a => a -> a -> a
* i -> x
p (Vector 3 i
valBits Vector 3 i -> Natural -> i
forall (size :: Natural) a. Vector size a -> Natural -> a
!! Natural
1)
        i
hi2 <- ClosedPoly i (BaseField ctx) -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m var
newAssigned (ClosedPoly i (BaseField ctx) -> m i)
-> ClosedPoly i (BaseField ctx) -> m i
forall a b. (a -> b) -> a -> b
$ \i -> x
p -> i -> x
p i
f x -> x -> x
forall a. MultiplicativeSemigroup a => a -> a -> a
* i -> x
p (Vector 3 i
valBits Vector 3 i -> Natural -> i
forall (size :: Natural) a. Vector size a -> Natural -> a
!! Natural
2)
        i
res <- [i] -> m i
forall i a w (m :: Type -> Type).
MonadCircuit i a w m =>
[i] -> m i
horner [Vector 3 i
valBits Vector 3 i -> Natural -> i
forall (size :: Natural) a. Vector size a -> Natural -> a
!! Natural
0, i
hi1, i
hi2]

        Par1 i -> m (Par1 i)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Par1 i -> m (Par1 i)) -> Par1 i -> m (Par1 i)
forall a b. (a -> b) -> a -> b
$ i -> Par1 i
forall p. p -> Par1 p
Par1 i
res
    where
        UInt ctx
  (Vector
     (NumberOfRegisters
        (BaseField ctx)
        (If
           (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
           (Log2 n + 1)
           3)
        ('Fixed
           (If
              (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
              (Log2 n + 1)
              3))))
v =
            forall (n :: Natural) {r}.
KnownNat n =>
(KnownNat (BufLen n) => r) -> r
knownBufLen @n ((KnownNat (BufLen n) =>
  UInt
    (If
       (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
       (Log2 n + 1)
       3)
    ('Fixed
       (If
          (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
          (Log2 n + 1)
          3))
    ctx)
 -> UInt
      (If
         (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
         (Log2 n + 1)
         3)
      ('Fixed
         (If
            (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
            (Log2 n + 1)
            3))
      ctx)
-> (KnownNat (BufLen n) =>
    UInt
      (If
         (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
         (Log2 n + 1)
         3)
      ('Fixed
         (If
            (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
            (Log2 n + 1)
            3))
      ctx)
-> UInt
     (If
        (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
        (Log2 n + 1)
        3)
     ('Fixed
        (If
           (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
           (Log2 n + 1)
           3))
     ctx
forall a b. (a -> b) -> a -> b
$
                forall (n :: Natural) (c :: (Type -> Type) -> Type) {r}.
KnownNat n =>
(KnownNat
   (Div
      ((GetRegisterSize (BaseField c) (BufLen n) ('Fixed (BufLen n))
        + 16)
       - 1)
      16) =>
 r)
-> r
knownNumWords @n @ctx ((KnownNat
    (Div
       ((GetRegisterSize (BaseField ctx) (BufLen n) ('Fixed (BufLen n))
         + 16)
        - 1)
       16) =>
  UInt
    (If
       (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
       (Log2 n + 1)
       3)
    ('Fixed
       (If
          (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
          (Log2 n + 1)
          3))
    ctx)
 -> UInt
      (If
         (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
         (Log2 n + 1)
         3)
      ('Fixed
         (If
            (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
            (Log2 n + 1)
            3))
      ctx)
-> (KnownNat
      (Div
         ((GetRegisterSize (BaseField ctx) (BufLen n) ('Fixed (BufLen n))
           + 16)
          - 1)
         16) =>
    UInt
      (If
         (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
         (Log2 n + 1)
         3)
      ('Fixed
         (If
            (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
            (Log2 n + 1)
            3))
      ctx)
-> UInt
     (If
        (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
        (Log2 n + 1)
        3)
     ('Fixed
        (If
           (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
           (Log2 n + 1)
           3))
     ctx
forall a b. (a -> b) -> a -> b
$
                    forall (n :: Natural) (c :: (Type -> Type) -> Type) {r}.
(KnownNat
   (NumberOfRegisters (BaseField c) (BufLen n) ('Fixed (BufLen n))) =>
 r)
-> r
knownOneReg @n @ctx ((KnownNat
    (NumberOfRegisters
       (BaseField ctx) (BufLen n) ('Fixed (BufLen n))) =>
  UInt
    (If
       (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
       (Log2 n + 1)
       3)
    ('Fixed
       (If
          (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
          (Log2 n + 1)
          3))
    ctx)
 -> UInt
      (If
         (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
         (Log2 n + 1)
         3)
      ('Fixed
         (If
            (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
            (Log2 n + 1)
            3))
      ctx)
-> (KnownNat
      (NumberOfRegisters
         (BaseField ctx) (BufLen n) ('Fixed (BufLen n))) =>
    UInt
      (If
         (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
         (Log2 n + 1)
         3)
      ('Fixed
         (If
            (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
            (Log2 n + 1)
            3))
      ctx)
-> UInt
     (If
        (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
        (Log2 n + 1)
        3)
     ('Fixed
        (If
           (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
           (Log2 n + 1)
           3))
     ctx
forall a b. (a -> b) -> a -> b
$
                        forall (n :: Natural) {r}.
KnownNat n =>
(KnownNat (Div ((n + 16) - 1) 16) => r) -> r
withDiv @(BufLen n) ((KnownNat (Div ((BufLen n + 16) - 1) 16) =>
  UInt
    (If
       (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
       (Log2 n + 1)
       3)
    ('Fixed
       (If
          (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
          (Log2 n + 1)
          3))
    ctx)
 -> UInt
      (If
         (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
         (Log2 n + 1)
         3)
      ('Fixed
         (If
            (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
            (Log2 n + 1)
            3))
      ctx)
-> (KnownNat (Div ((BufLen n + 16) - 1) 16) =>
    UInt
      (If
         (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
         (Log2 n + 1)
         3)
      ('Fixed
         (If
            (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
            (Log2 n + 1)
            3))
      ctx)
-> UInt
     (If
        (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
        (Log2 n + 1)
        3)
     ('Fixed
        (If
           (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
           (Log2 n + 1)
           3))
     ctx
forall a b. (a -> b) -> a -> b
$
                            UInt
  (If
     (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
     (Log2 n + 1)
     3)
  ('Fixed
     (If
        (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
        (Log2 n + 1)
        3))
  ctx
UInt (BufLen n) ('Fixed (BufLen n)) ctx
ui UInt
  (If
     (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
     (Log2 n + 1)
     3)
  ('Fixed
     (If
        (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
        (Log2 n + 1)
        3))
  ctx
-> UInt
     (If
        (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
        (Log2 n + 1)
        3)
     ('Fixed
        (If
           (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
           (Log2 n + 1)
           3))
     ctx
-> UInt
     (If
        (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
        (Log2 n + 1)
        3)
     ('Fixed
        (If
           (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
           (Log2 n + 1)
           3))
     ctx
forall a. SemiEuclidean a => a -> a -> a
`mod` (forall a b. FromConstant a b => a -> b
fromConstant @Natural Natural
6)


-- | Increase capacity of a VarByteString and increase its length to the nearest multiple of 6
-- Required for base64 encoding.
--
padBytestring6
    :: forall n ctx
    .  Symbolic ctx
    => KnownNat n
    => VarByteString n ctx -> VarByteString (Next6 n) ctx
padBytestring6 :: forall (n :: Natural) (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, KnownNat n) =>
VarByteString n ctx -> VarByteString (Next6 n) ctx
padBytestring6 VarByteString{FieldElement ctx
ByteString n ctx
bsLength :: FieldElement ctx
bsBuffer :: ByteString n ctx
bsLength :: forall (maxLen :: Natural) (context :: (Type -> Type) -> Type).
VarByteString maxLen context -> FieldElement context
bsBuffer :: forall (maxLen :: Natural) (context :: (Type -> Type) -> Type).
VarByteString maxLen context -> ByteString maxLen context
..} = FieldElement ctx
-> ByteString (Div (n + 5) 6 * 6) ctx
-> VarByteString (Div (n + 5) 6 * 6) ctx
forall (maxLen :: Natural) (context :: (Type -> Type) -> Type).
FieldElement context
-> ByteString maxLen context -> VarByteString maxLen context
VarByteString (FieldElement ctx
bsLength FieldElement ctx -> FieldElement ctx -> FieldElement ctx
forall a. AdditiveSemigroup a => a -> a -> a
+ FieldElement ctx
mod6) (forall (n :: Natural) {r}.
KnownNat n =>
(KnownNat (Next6 n) => r) -> r
withNext6 @n ((KnownNat (Div (n + 5) 6 * 6) =>
  ByteString (Div (n + 5) 6 * 6) ctx)
 -> ByteString (Div (n + 5) 6 * 6) ctx)
-> (KnownNat (Div (n + 5) 6 * 6) =>
    ByteString (Div (n + 5) 6 * 6) ctx)
-> ByteString (Div (n + 5) 6 * 6) ctx
forall a b. (a -> b) -> a -> b
$ ByteString (Div (n + 5) 6 * 6) ctx
-> FieldElement ctx -> ByteString (Div (n + 5) 6 * 6) ctx
forall (n :: Natural) (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, KnownNat n) =>
ByteString n ctx -> FieldElement ctx -> ByteString n ctx
VB.shiftL ByteString (Div (n + 5) 6 * 6) ctx
newBuf FieldElement ctx
mod6)
    where
        mod6 :: FieldElement ctx
mod6 = forall (n :: Natural) (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, KnownNat n) =>
UInt (BufLen n) ('Fixed (BufLen n)) ctx -> FieldElement ctx
padTo6 @n (UInt (BufLen n) ('Fixed (BufLen n)) ctx -> FieldElement ctx)
-> UInt (BufLen n) ('Fixed (BufLen n)) ctx -> FieldElement ctx
forall a b. (a -> b) -> a -> b
$ forall (n :: Natural) (ctx :: (Type -> Type) -> Type).
Symbolic ctx =>
FieldElement ctx -> UInt (BufLen n) ('Fixed (BufLen n)) ctx
feToUInt @n FieldElement ctx
bsLength
        newBuf :: ByteString (Div (n + 5) 6 * 6) ctx
newBuf = forall (n :: Natural) {r}.
KnownNat n =>
(KnownNat (Next6 n) => r) -> r
withNext6 @n ((KnownNat (Div (n + 5) 6 * 6) =>
  ByteString (Div (n + 5) 6 * 6) ctx)
 -> ByteString (Div (n + 5) 6 * 6) ctx)
-> (KnownNat (Div (n + 5) 6 * 6) =>
    ByteString (Div (n + 5) 6 * 6) ctx)
-> ByteString (Div (n + 5) 6 * 6) ctx
forall a b. (a -> b) -> a -> b
$ ByteString n ctx -> ByteString (Div (n + 5) 6 * 6) ctx
forall a b. Resize a b => a -> b
resize ByteString n ctx
bsBuffer


-- | Convert a base64-encoded string into an ASCII-encoded string
-- It is expected that both capacity and length of the input bytestring are divisible by 6
-- If either of them is not, apply @padBytestring6@ first.
--
base64ToAscii
    :: forall n ctx
    .  Symbolic ctx
    => KnownNat n
    => Mod n 6 ~ 0
    => NFData (ctx (V.Vector 8))
    => NFData (ctx (V.Vector (ASCII n)))
    => VarByteString n ctx -> VarByteString (ASCII n) ctx
base64ToAscii :: forall (n :: Natural) (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, KnownNat n, Mod n 6 ~ 0, NFData (ctx (Vector 8)),
 NFData (ctx (Vector (ASCII n)))) =>
VarByteString n ctx -> VarByteString (ASCII n) ctx
base64ToAscii VarByteString{FieldElement ctx
ByteString n ctx
bsLength :: forall (maxLen :: Natural) (context :: (Type -> Type) -> Type).
VarByteString maxLen context -> FieldElement context
bsBuffer :: forall (maxLen :: Natural) (context :: (Type -> Type) -> Type).
VarByteString maxLen context -> ByteString maxLen context
bsLength :: FieldElement ctx
bsBuffer :: ByteString n ctx
..} = forall (n :: Natural) {r}.
KnownNat n =>
(KnownNat (ASCII n) => r) -> r
withAscii @n ((KnownNat (ASCII n) => VarByteString (ASCII n) ctx)
 -> VarByteString (ASCII n) ctx)
-> (KnownNat (ASCII n) => VarByteString (ASCII n) ctx)
-> VarByteString (ASCII n) ctx
forall a b. (a -> b) -> a -> b
$ VarByteString (ASCII n) ctx -> VarByteString (ASCII n) ctx
forall (n :: Natural) (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, KnownNat n) =>
VarByteString n ctx -> VarByteString n ctx
wipeUnassigned (VarByteString (ASCII n) ctx -> VarByteString (ASCII n) ctx)
-> VarByteString (ASCII n) ctx -> VarByteString (ASCII n) ctx
forall a b. (a -> b) -> a -> b
$ FieldElement ctx
-> ByteString (ASCII n) ctx -> VarByteString (ASCII n) ctx
forall (maxLen :: Natural) (context :: (Type -> Type) -> Type).
FieldElement context
-> ByteString maxLen context -> VarByteString maxLen context
VarByteString FieldElement ctx
newLen ByteString (ASCII n) ctx
result
    where
        words6 :: Vector (Div n 6) (ByteString 6 ctx)
words6 = forall (a :: Natural) (b :: Natural) {r}.
(Mod a b ~ 0) =>
(((Div a b * b) ~ a) => r) -> r
withDivMul @n @6 ((((Div n 6 * 6) ~ n) => Vector (Div n 6) (ByteString 6 ctx))
 -> Vector (Div n 6) (ByteString 6 ctx))
-> (((Div n 6 * 6) ~ n) => Vector (Div n 6) (ByteString 6 ctx))
-> Vector (Div n 6) (ByteString 6 ctx)
forall a b. (a -> b) -> a -> b
$ forall (m :: Natural) (wordSize :: Natural)
       (c :: (Type -> Type) -> Type).
(Symbolic c, KnownNat wordSize) =>
ByteString (m * wordSize) c -> Vector m (ByteString wordSize c)
toWords @(Div n 6) @6 ByteString n ctx
ByteString (Div n 6 * 6) ctx
bsBuffer
        ascii :: Vector (Div n 6) (ByteString 8 ctx)
ascii  = ByteString 6 ctx -> ByteString 8 ctx
forall (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, NFData (ctx (Vector 8))) =>
ByteString 6 ctx -> ByteString 8 ctx
word6ToAscii (ByteString 6 ctx -> ByteString 8 ctx)
-> Vector (Div n 6) (ByteString 6 ctx)
-> Vector (Div n 6) (ByteString 8 ctx)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Vector (Div n 6) (ByteString 6 ctx)
words6
        result :: ByteString (ASCII n) ctx
result = ByteString (ASCII n) ctx -> ByteString (ASCII n) ctx
forall a. NFData a => a -> a
force (ByteString (ASCII n) ctx -> ByteString (ASCII n) ctx)
-> ByteString (ASCII n) ctx -> ByteString (ASCII n) ctx
forall a b. (a -> b) -> a -> b
$ Vector (Div n 6) (ByteString 8 ctx) -> ByteString (ASCII n) ctx
forall (k :: Natural) (m :: Natural) (c :: (Type -> Type) -> Type).
Symbolic c =>
Vector k (ByteString m c) -> ByteString (k * m) c
concat Vector (Div n 6) (ByteString 8 ctx)
ascii

        newLen :: FieldElement ctx
newLen =
            forall (n :: Natural) {r}.
KnownNat n =>
(KnownNat (BufLen n) => r) -> r
knownBufLen @n ((KnownNat (BufLen n) => FieldElement ctx) -> FieldElement ctx)
-> (KnownNat (BufLen n) => FieldElement ctx) -> FieldElement ctx
forall a b. (a -> b) -> a -> b
$
                forall (n :: Natural) {r}.
KnownNat n =>
(KnownNat (Div ((n + 16) - 1) 16) => r) -> r
withDiv @(BufLen n) ((KnownNat (Div ((BufLen n + 16) - 1) 16) => FieldElement ctx)
 -> FieldElement ctx)
-> (KnownNat (Div ((BufLen n + 16) - 1) 16) => FieldElement ctx)
-> FieldElement ctx
forall a b. (a -> b) -> a -> b
$
                    forall (n :: Natural) (c :: (Type -> Type) -> Type) {r}.
(KnownNat
   (NumberOfRegisters (BaseField c) (BufLen n) ('Fixed (BufLen n))) =>
 r)
-> r
knownOneReg @n @ctx ((KnownNat
    (NumberOfRegisters
       (BaseField ctx) (BufLen n) ('Fixed (BufLen n))) =>
  FieldElement ctx)
 -> FieldElement ctx)
-> (KnownNat
      (NumberOfRegisters
         (BaseField ctx) (BufLen n) ('Fixed (BufLen n))) =>
    FieldElement ctx)
-> FieldElement ctx
forall a b. (a -> b) -> a -> b
$
                        forall (n :: Natural) (c :: (Type -> Type) -> Type) {r}.
KnownNat n =>
(KnownNat
   (Div
      ((GetRegisterSize (BaseField c) (BufLen n) ('Fixed (BufLen n))
        + 16)
       - 1)
      16) =>
 r)
-> r
knownNumWords @n @ctx ((KnownNat
    (Div
       ((GetRegisterSize (BaseField ctx) (BufLen n) ('Fixed (BufLen n))
         + 16)
        - 1)
       16) =>
  FieldElement ctx)
 -> FieldElement ctx)
-> (KnownNat
      (Div
         ((GetRegisterSize (BaseField ctx) (BufLen n) ('Fixed (BufLen n))
           + 16)
          - 1)
         16) =>
    FieldElement ctx)
-> FieldElement ctx
forall a b. (a -> b) -> a -> b
$
                            Natural -> FieldElement ctx -> FieldElement ctx
forall b a. Scale b a => b -> a -> a
scale (Natural
4 :: Natural) (FieldElement ctx -> FieldElement ctx)
-> (FieldElement ctx -> FieldElement ctx)
-> FieldElement ctx
-> FieldElement ctx
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (n :: Natural) (ctx :: (Type -> Type) -> Type).
Symbolic ctx =>
UInt (BufLen n) ('Fixed (BufLen n)) ctx -> FieldElement ctx
uintToFe @n) (UInt
   (If
      (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
      (Log2 n + 1)
      3)
   ('Fixed
      (If
         (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
         (Log2 n + 1)
         3))
   ctx
 -> FieldElement ctx)
-> (FieldElement ctx
    -> UInt
         (If
            (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
            (Log2 n + 1)
            3)
         ('Fixed
            (If
               (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
               (Log2 n + 1)
               3))
         ctx)
-> FieldElement ctx
-> FieldElement ctx
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (UInt
  (If
     (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
     (Log2 n + 1)
     3)
  ('Fixed
     (If
        (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
        (Log2 n + 1)
        3))
  ctx
-> UInt
     (If
        (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
        (Log2 n + 1)
        3)
     ('Fixed
        (If
           (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
           (Log2 n + 1)
           3))
     ctx
-> UInt
     (If
        (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
        (Log2 n + 1)
        3)
     ('Fixed
        (If
           (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
           (Log2 n + 1)
           3))
     ctx
forall a. SemiEuclidean a => a -> a -> a
`div` (forall a b. FromConstant a b => a -> b
fromConstant @Natural Natural
3)) (UInt
   (If
      (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
      (Log2 n + 1)
      3)
   ('Fixed
      (If
         (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
         (Log2 n + 1)
         3))
   ctx
 -> UInt
      (If
         (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
         (Log2 n + 1)
         3)
      ('Fixed
         (If
            (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
            (Log2 n + 1)
            3))
      ctx)
-> (FieldElement ctx
    -> UInt
         (If
            (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
            (Log2 n + 1)
            3)
         ('Fixed
            (If
               (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
               (Log2 n + 1)
               3))
         ctx)
-> FieldElement ctx
-> UInt
     (If
        (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
        (Log2 n + 1)
        3)
     ('Fixed
        (If
           (OrdCond (CmpNat 3 (Log2 n + 1)) 'True 'True 'False)
           (Log2 n + 1)
           3))
     ctx
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (n :: Natural) (ctx :: (Type -> Type) -> Type).
Symbolic ctx =>
FieldElement ctx -> UInt (BufLen n) ('Fixed (BufLen n)) ctx
feToUInt @n) (FieldElement ctx -> FieldElement ctx)
-> FieldElement ctx -> FieldElement ctx
forall a b. (a -> b) -> a -> b
$ FieldElement ctx
bsLength


{-
    Symbols  |  Base64url  |  ASCII
    A..Z         0..25       65..90
    a..z         26..51      97..122
    0..9         52..61      48..57
    -            62          45
    _            63          95
-}
word6ToAscii :: forall ctx . (Symbolic ctx, NFData (ctx (V.Vector 8))) => ByteString 6 ctx -> ByteString 8 ctx
word6ToAscii :: forall (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, NFData (ctx (Vector 8))) =>
ByteString 6 ctx -> ByteString 8 ctx
word6ToAscii (ByteString ctx (Vector 6)
bs) = ByteString 8 ctx -> ByteString 8 ctx
forall a. NFData a => a -> a
force (ByteString 8 ctx -> ByteString 8 ctx)
-> ByteString 8 ctx -> ByteString 8 ctx
forall a b. (a -> b) -> a -> b
$ ctx (Vector 8) -> ByteString 8 ctx
forall (n :: Natural) (context :: (Type -> Type) -> Type).
context (Vector n) -> ByteString n context
ByteString (ctx (Vector 8) -> ByteString 8 ctx)
-> ctx (Vector 8) -> ByteString 8 ctx
forall a b. (a -> b) -> a -> b
$ ctx (Vector 6)
-> (forall {i} {m :: Type -> Type}.
    (NFData i, MonadCircuit i (BaseField ctx) (WitnessField ctx) m) =>
    FunBody '[Vector 6] (Vector 8) i m)
-> ctx (Vector 8)
forall (f :: Type -> Type) (g :: Type -> Type).
ctx f -> CircuitFun '[f] g ctx -> ctx g
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type)
       (g :: Type -> Type).
Symbolic c =>
c f -> CircuitFun '[f] g c -> c g
fromCircuitF ctx (Vector 6)
bs ((forall {i} {m :: Type -> Type}.
  (NFData i, MonadCircuit i (BaseField ctx) (WitnessField ctx) m) =>
  FunBody '[Vector 6] (Vector 8) i m)
 -> ctx (Vector 8))
-> (forall {i} {m :: Type -> Type}.
    (NFData i, MonadCircuit i (BaseField ctx) (WitnessField ctx) m) =>
    FunBody '[Vector 6] (Vector 8) i m)
-> ctx (Vector 8)
forall a b. (a -> b) -> a -> b
$ \Vector 6 i
bits ->
    do
        let bitsSym :: [i]
bitsSym = Vector 6 i -> [i]
forall (size :: Natural) a. Vector size a -> [a]
V.fromVector Vector 6 i
bits

        i
fe <- [i] -> m i
forall i a w (m :: Type -> Type).
MonadCircuit i a w m =>
[i] -> m i
horner ([i] -> [i]
forall a. [a] -> [a]
P.reverse [i]
bitsSym)

        i
z <- ClosedPoly i (BaseField ctx) -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m var
newAssigned (x -> (i -> x) -> x
forall a b. a -> b -> a
P.const x
forall a. AdditiveMonoid a => a
zero)
        i
o <- ClosedPoly i (BaseField ctx) -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m var
newAssigned (x -> (i -> x) -> x
forall a b. a -> b -> a
P.const x
forall a. MultiplicativeMonoid a => a
one)

        let bits25 :: [i]
bits25 = [i
z,i
o,i
o,i
z,i
z,i
o]
            bits51 :: [i]
bits51 = [i
o,i
o,i
z,i
z,i
o,i
o]
            bits61 :: [i]
bits61 = [i
o,i
o,i
o,i
o,i
z,i
o]
            bits62 :: [i]
bits62 = [i
o,i
o,i
o,i
o,i
o,i
z]

        i
isAZ   <- forall (r :: Natural) i a w (m :: Type -> Type)
       (f :: Type -> Type).
(Arithmetic a, MonadCircuit i a w m, Zip f, Foldable f,
 KnownNat r) =>
f i -> f i -> m i
blueprintGE @6 [i]
bits25 [i]
bitsSym
        i
leaz   <- forall (r :: Natural) i a w (m :: Type -> Type)
       (f :: Type -> Type).
(Arithmetic a, MonadCircuit i a w m, Zip f, Foldable f,
 KnownNat r) =>
f i -> f i -> m i
blueprintGE @6 [i]
bits51 [i]
bitsSym
        i
le09   <- forall (r :: Natural) i a w (m :: Type -> Type)
       (f :: Type -> Type).
(Arithmetic a, MonadCircuit i a w m, Zip f, Foldable f,
 KnownNat r) =>
f i -> f i -> m i
blueprintGE @6 [i]
bits61 [i]
bitsSym
        i
ledash <- forall (r :: Natural) i a w (m :: Type -> Type)
       (f :: Type -> Type).
(Arithmetic a, MonadCircuit i a w m, Zip f, Foldable f,
 KnownNat r) =>
f i -> f i -> m i
blueprintGE @6 [i]
bits62 [i]
bitsSym

        i
isaz   <- ClosedPoly i (BaseField ctx) -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m var
newAssigned (ClosedPoly i (BaseField ctx) -> m i)
-> ClosedPoly i (BaseField ctx) -> m i
forall a b. (a -> b) -> a -> b
$ \i -> x
p -> i -> x
p i
leaz x -> x -> x
forall a. MultiplicativeSemigroup a => a -> a -> a
* (x
forall a. MultiplicativeMonoid a => a
one x -> x -> x
forall a. AdditiveGroup a => a -> a -> a
- i -> x
p i
isAZ)
        i
is09   <- ClosedPoly i (BaseField ctx) -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m var
newAssigned (ClosedPoly i (BaseField ctx) -> m i)
-> ClosedPoly i (BaseField ctx) -> m i
forall a b. (a -> b) -> a -> b
$ \i -> x
p -> i -> x
p i
le09 x -> x -> x
forall a. MultiplicativeSemigroup a => a -> a -> a
* (x
forall a. MultiplicativeMonoid a => a
one x -> x -> x
forall a. AdditiveGroup a => a -> a -> a
- i -> x
p i
leaz)
        i
isdash <- ClosedPoly i (BaseField ctx) -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m var
newAssigned (ClosedPoly i (BaseField ctx) -> m i)
-> ClosedPoly i (BaseField ctx) -> m i
forall a b. (a -> b) -> a -> b
$ \i -> x
p -> i -> x
p i
ledash x -> x -> x
forall a. MultiplicativeSemigroup a => a -> a -> a
* (x
forall a. MultiplicativeMonoid a => a
one x -> x -> x
forall a. AdditiveGroup a => a -> a -> a
- i -> x
p i
le09)
        i
isus   <- ClosedPoly i (BaseField ctx) -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m var
newAssigned (ClosedPoly i (BaseField ctx) -> m i)
-> ClosedPoly i (BaseField ctx) -> m i
forall a b. (a -> b) -> a -> b
$ \i -> x
p -> x
forall a. MultiplicativeMonoid a => a
one x -> x -> x
forall a. AdditiveGroup a => a -> a -> a
- i -> x
p i
ledash

        i
asciiAZ   <- ClosedPoly i (BaseField ctx) -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m var
newAssigned (ClosedPoly i (BaseField ctx) -> m i)
-> ClosedPoly i (BaseField ctx) -> m i
forall a b. (a -> b) -> a -> b
$ \i -> x
p -> i -> x
p i
isAZ   x -> x -> x
forall a. MultiplicativeSemigroup a => a -> a -> a
* (i -> x
p i
fe x -> x -> x
forall a. AdditiveSemigroup a => a -> a -> a
+ (forall a b. FromConstant a b => a -> b
fromConstant @Natural Natural
65))
        i
asciiaz   <- ClosedPoly i (BaseField ctx) -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m var
newAssigned (ClosedPoly i (BaseField ctx) -> m i)
-> ClosedPoly i (BaseField ctx) -> m i
forall a b. (a -> b) -> a -> b
$ \i -> x
p -> i -> x
p i
isaz   x -> x -> x
forall a. MultiplicativeSemigroup a => a -> a -> a
* (i -> x
p i
fe x -> x -> x
forall a. AdditiveSemigroup a => a -> a -> a
+ (forall a b. FromConstant a b => a -> b
fromConstant @Natural Natural
71))
        i
ascii09   <- ClosedPoly i (BaseField ctx) -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m var
newAssigned (ClosedPoly i (BaseField ctx) -> m i)
-> ClosedPoly i (BaseField ctx) -> m i
forall a b. (a -> b) -> a -> b
$ \i -> x
p -> i -> x
p i
is09   x -> x -> x
forall a. MultiplicativeSemigroup a => a -> a -> a
* (i -> x
p i
fe x -> x -> x
forall a. AdditiveGroup a => a -> a -> a
- (forall a b. FromConstant a b => a -> b
fromConstant @Natural Natural
4 ))
        i
asciidash <- ClosedPoly i (BaseField ctx) -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m var
newAssigned (ClosedPoly i (BaseField ctx) -> m i)
-> ClosedPoly i (BaseField ctx) -> m i
forall a b. (a -> b) -> a -> b
$ \i -> x
p -> i -> x
p i
isdash x -> x -> x
forall a. MultiplicativeSemigroup a => a -> a -> a
* (i -> x
p i
fe x -> x -> x
forall a. AdditiveGroup a => a -> a -> a
- (forall a b. FromConstant a b => a -> b
fromConstant @Natural Natural
17))
        i
asciius   <- ClosedPoly i (BaseField ctx) -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m var
newAssigned (ClosedPoly i (BaseField ctx) -> m i)
-> ClosedPoly i (BaseField ctx) -> m i
forall a b. (a -> b) -> a -> b
$ \i -> x
p -> i -> x
p i
isus   x -> x -> x
forall a. MultiplicativeSemigroup a => a -> a -> a
* (i -> x
p i
fe x -> x -> x
forall a. AdditiveSemigroup a => a -> a -> a
+ (forall a b. FromConstant a b => a -> b
fromConstant @Natural Natural
32))

        i
s1 <- ClosedPoly i (BaseField ctx) -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m var
newAssigned (ClosedPoly i (BaseField ctx) -> m i)
-> ClosedPoly i (BaseField ctx) -> m i
forall a b. (a -> b) -> a -> b
$ \i -> x
p -> i -> x
p i
asciiAZ   x -> x -> x
forall a. AdditiveSemigroup a => a -> a -> a
+ i -> x
p i
asciiaz
        i
s2 <- ClosedPoly i (BaseField ctx) -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m var
newAssigned (ClosedPoly i (BaseField ctx) -> m i)
-> ClosedPoly i (BaseField ctx) -> m i
forall a b. (a -> b) -> a -> b
$ \i -> x
p -> i -> x
p i
ascii09   x -> x -> x
forall a. AdditiveSemigroup a => a -> a -> a
+ i -> x
p i
s1
        i
s3 <- ClosedPoly i (BaseField ctx) -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m var
newAssigned (ClosedPoly i (BaseField ctx) -> m i)
-> ClosedPoly i (BaseField ctx) -> m i
forall a b. (a -> b) -> a -> b
$ \i -> x
p -> i -> x
p i
asciidash x -> x -> x
forall a. AdditiveSemigroup a => a -> a -> a
+ i -> x
p i
s2
        i
s4 <- ClosedPoly i (BaseField ctx) -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m var
newAssigned (ClosedPoly i (BaseField ctx) -> m i)
-> ClosedPoly i (BaseField ctx) -> m i
forall a b. (a -> b) -> a -> b
$ \i -> x
p -> i -> x
p i
asciius   x -> x -> x
forall a. AdditiveSemigroup a => a -> a -> a
+ i -> x
p i
s3

        [i] -> Vector 8 i
forall (size :: Natural) a. [a] -> Vector size a
V.unsafeToVector ([i] -> Vector 8 i) -> ([i] -> [i]) -> [i] -> Vector 8 i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [i] -> [i]
forall a. [a] -> [a]
P.reverse ([i] -> Vector 8 i) -> m [i] -> m (Vector 8 i)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Natural -> i -> m [i]
forall i a w (m :: Type -> Type).
(MonadCircuit i a w m, Arithmetic a) =>
Natural -> i -> m [i]
expansion Natural
8 i
s4


toAsciiBits
    :: forall a ctx
    .  IsSymbolicJSON a
    => Context a ~ ctx
    => KnownNat (MaxLength a)
    => Symbolic ctx
    => NFData (ctx (V.Vector 8))
    => NFData (ctx (V.Vector (ASCII (Next6 (MaxLength a)))))
    => a -> VarByteString (ASCII (Next6 (MaxLength a))) ctx
toAsciiBits :: forall a (ctx :: (Type -> Type) -> Type).
(IsSymbolicJSON a, Context a ~ ctx, KnownNat (MaxLength a),
 Symbolic ctx, NFData (ctx (Vector 8)),
 NFData (ctx (Vector (ASCII (Next6 (MaxLength a)))))) =>
a -> VarByteString (ASCII (Next6 (MaxLength a))) ctx
toAsciiBits = forall (n :: Natural) {r}.
KnownNat n =>
(KnownNat (Next6 n) => r) -> r
withNext6 @(MaxLength a) ((KnownNat (Next6 (MaxLength a)) =>
  a -> VarByteString (ASCII (Next6 (MaxLength a))) ctx)
 -> a -> VarByteString (ASCII (Next6 (MaxLength a))) ctx)
-> (KnownNat (Next6 (MaxLength a)) =>
    a -> VarByteString (ASCII (Next6 (MaxLength a))) ctx)
-> a
-> VarByteString (ASCII (Next6 (MaxLength a))) ctx
forall a b. (a -> b) -> a -> b
$ Dict (Mod (Next6 (MaxLength a)) 6 ~ 0)
-> ((Mod (Next6 (MaxLength a)) 6 ~ 0) =>
    a -> VarByteString (ASCII (Next6 (MaxLength a))) ctx)
-> a
-> VarByteString (ASCII (Next6 (MaxLength a))) ctx
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (forall (n :: Natural). Dict (Mod (Next6 n) 6 ~ 0)
mulMod @(MaxLength a)) (((Mod (Next6 (MaxLength a)) 6 ~ 0) =>
  a -> VarByteString (ASCII (Next6 (MaxLength a))) ctx)
 -> a -> VarByteString (ASCII (Next6 (MaxLength a))) ctx)
-> ((Mod (Next6 (MaxLength a)) 6 ~ 0) =>
    a -> VarByteString (ASCII (Next6 (MaxLength a))) ctx)
-> a
-> VarByteString (ASCII (Next6 (MaxLength a))) ctx
forall a b. (a -> b) -> a -> b
$ VarByteString (Next6 (MaxLength a)) ctx
-> VarByteString (ASCII (Next6 (MaxLength a))) ctx
forall (n :: Natural) (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, KnownNat n, Mod n 6 ~ 0, NFData (ctx (Vector 8)),
 NFData (ctx (Vector (ASCII n)))) =>
VarByteString n ctx -> VarByteString (ASCII n) ctx
base64ToAscii (VarByteString (Next6 (MaxLength a)) ctx
 -> VarByteString (ASCII (Next6 (MaxLength a))) ctx)
-> (a -> VarByteString (Next6 (MaxLength a)) ctx)
-> a
-> VarByteString (ASCII (Next6 (MaxLength a))) ctx
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VarByteString (MaxLength a) ctx
-> VarByteString (Next6 (MaxLength a)) ctx
forall (n :: Natural) (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, KnownNat n) =>
VarByteString n ctx -> VarByteString (Next6 n) ctx
padBytestring6 (VarByteString (MaxLength a) ctx
 -> VarByteString (Next6 (MaxLength a)) ctx)
-> (a -> VarByteString (MaxLength a) ctx)
-> a
-> VarByteString (Next6 (MaxLength a)) ctx
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> VarByteString (MaxLength a) ctx
a -> VarByteString (MaxLength a) (Context a)
forall a.
IsSymbolicJSON a =>
a -> VarByteString (MaxLength a) (Context a)
toJsonBits


type SecretBits ctx =
    ( NFData (ctx (V.Vector 8))
    , NFData (ctx (V.Vector 648))
    , NFData (ctx (V.Vector 864))
    , NFData (ctx (V.Vector 9456))
    , NFData (ctx (V.Vector 10328))
    , NFData (ctx Par1)
    )


secretBits'
    :: forall ctx
    .  Symbolic ctx
    => SecretBits ctx
    => TokenHeader ctx
    -> TokenPayload ctx
    -> VarByteString 10328 ctx
secretBits' :: forall (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, SecretBits ctx) =>
TokenHeader ctx -> TokenPayload ctx -> VarByteString 10328 ctx
secretBits' TokenHeader ctx
h TokenPayload ctx
p =  VarByteString 10328 ctx -> VarByteString 10328 ctx
forall a. NFData a => a -> a
force (VarByteString 10328 ctx -> VarByteString 10328 ctx)
-> VarByteString 10328 ctx -> VarByteString 10328 ctx
forall a b. (a -> b) -> a -> b
$
       TokenHeader ctx
-> VarByteString (ASCII (Next6 (MaxLength (TokenHeader ctx)))) ctx
forall a (ctx :: (Type -> Type) -> Type).
(IsSymbolicJSON a, Context a ~ ctx, KnownNat (MaxLength a),
 Symbolic ctx, NFData (ctx (Vector 8)),
 NFData (ctx (Vector (ASCII (Next6 (MaxLength a)))))) =>
a -> VarByteString (ASCII (Next6 (MaxLength a))) ctx
toAsciiBits TokenHeader ctx
h
    VarByteString 864 ctx
-> VarByteString 8 ctx -> VarByteString (864 + 8) ctx
forall (m :: Natural) (n :: Natural)
       (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, KnownNat m, KnownNat (m + n)) =>
VarByteString m ctx
-> VarByteString n ctx -> VarByteString (m + n) ctx
@+ (forall (s :: Symbol) a. IsTypeString s a => a
fromType @".")
    VarByteString (864 + 8) ctx
-> VarByteString 9456 ctx -> VarByteString ((864 + 8) + 9456) ctx
forall (m :: Natural) (n :: Natural)
       (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, KnownNat m, KnownNat (m + n)) =>
VarByteString m ctx
-> VarByteString n ctx -> VarByteString (m + n) ctx
@+ TokenPayload ctx
-> VarByteString (ASCII (Next6 (MaxLength (TokenPayload ctx)))) ctx
forall a (ctx :: (Type -> Type) -> Type).
(IsSymbolicJSON a, Context a ~ ctx, KnownNat (MaxLength a),
 Symbolic ctx, NFData (ctx (Vector 8)),
 NFData (ctx (Vector (ASCII (Next6 (MaxLength a)))))) =>
a -> VarByteString (ASCII (Next6 (MaxLength a))) ctx
toAsciiBits TokenPayload ctx
p


-- | Client secret as a ByteString: @ASCII(base64UrlEncode(header) + "." + base64UrlEncode(payload))@
--
secretBits
    :: forall ctx
    .  Symbolic ctx
    => SecretBits ctx
    => ClientSecret ctx -> VarByteString 10328 ctx
secretBits :: forall (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, SecretBits ctx) =>
ClientSecret ctx -> VarByteString 10328 ctx
secretBits ClientSecret {Signature 2048 ctx
TokenPayload ctx
TokenHeader ctx
csHeader :: forall (ctx :: (Type -> Type) -> Type).
ClientSecret ctx -> TokenHeader ctx
csPayload :: forall (ctx :: (Type -> Type) -> Type).
ClientSecret ctx -> TokenPayload ctx
csSignature :: forall (ctx :: (Type -> Type) -> Type).
ClientSecret ctx -> Signature 2048 ctx
csHeader :: TokenHeader ctx
csPayload :: TokenPayload ctx
csSignature :: Signature 2048 ctx
..} = TokenHeader ctx -> TokenPayload ctx -> VarByteString 10328 ctx
forall (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, SecretBits ctx) =>
TokenHeader ctx -> TokenPayload ctx -> VarByteString 10328 ctx
secretBits' TokenHeader ctx
csHeader TokenPayload ctx
csPayload

-- | Sign token payload and form a ClientSecret
--
signPayload :: (SecretBits ctx, RSA 2048 10328 ctx) => SigningKey ctx -> TokenPayload ctx -> ClientSecret ctx
signPayload :: forall (ctx :: (Type -> Type) -> Type).
(SecretBits ctx, RSA 2048 10328 ctx) =>
SigningKey ctx -> TokenPayload ctx -> ClientSecret ctx
signPayload SigningKey{VarByteString 320 ctx
PrivateKey 2048 ctx
prvKid :: forall (ctx :: (Type -> Type) -> Type).
SigningKey ctx -> VarByteString 320 ctx
prvKey :: forall (ctx :: (Type -> Type) -> Type).
SigningKey ctx -> PrivateKey 2048 ctx
prvKid :: VarByteString 320 ctx
prvKey :: PrivateKey 2048 ctx
..} TokenPayload ctx
csPayload = ClientSecret{Signature 2048 ctx
TokenPayload ctx
TokenHeader ctx
csHeader :: TokenHeader ctx
csPayload :: TokenPayload ctx
csSignature :: Signature 2048 ctx
csPayload :: TokenPayload ctx
csHeader :: TokenHeader ctx
csSignature :: Signature 2048 ctx
..}
    where
        csHeader :: TokenHeader ctx
csHeader = VarByteString 72 ctx
-> VarByteString 320 ctx -> VarByteString 32 ctx -> TokenHeader ctx
forall (ctx :: (Type -> Type) -> Type).
VarByteString 72 ctx
-> VarByteString 320 ctx -> VarByteString 32 ctx -> TokenHeader ctx
TokenHeader VarByteString 72 ctx
"RS256" VarByteString 320 ctx
prvKid VarByteString 32 ctx
"JWT"
        csSignature :: Signature 2048 ctx
csSignature = VarByteString 10328 ctx
-> PrivateKey 2048 ctx -> Signature 2048 ctx
forall (keyLen :: Natural) (msgLen :: Natural)
       (ctx :: (Type -> Type) -> Type).
RSA keyLen msgLen ctx =>
VarByteString msgLen ctx
-> PrivateKey keyLen ctx -> Signature keyLen ctx
signVar (TokenHeader ctx -> TokenPayload ctx -> VarByteString 10328 ctx
forall (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, SecretBits ctx) =>
TokenHeader ctx -> TokenPayload ctx -> VarByteString 10328 ctx
secretBits' TokenHeader ctx
csHeader TokenPayload ctx
csPayload) PrivateKey 2048 ctx
prvKey

-- | Verify that the given JWT was correctly signed with a matching key (i.e. Key IDs match and the signature is correct).
--
verifySignature :: (SecretBits ctx, RSA 2048 10328 ctx) => Certificate ctx -> ClientSecret ctx -> (Bool ctx, ByteString 256 ctx)
verifySignature :: forall (ctx :: (Type -> Type) -> Type).
(SecretBits ctx, RSA 2048 10328 ctx) =>
Certificate ctx
-> ClientSecret ctx -> (Bool ctx, ByteString 256 ctx)
verifySignature Certificate{VarByteString 320 ctx
PublicKey 2048 ctx
pubKid :: forall (ctx :: (Type -> Type) -> Type).
Certificate ctx -> VarByteString 320 ctx
pubKey :: forall (ctx :: (Type -> Type) -> Type).
Certificate ctx -> PublicKey 2048 ctx
pubKid :: VarByteString 320 ctx
pubKey :: PublicKey 2048 ctx
..} cs :: ClientSecret ctx
cs@ClientSecret{Signature 2048 ctx
TokenPayload ctx
TokenHeader ctx
csHeader :: forall (ctx :: (Type -> Type) -> Type).
ClientSecret ctx -> TokenHeader ctx
csPayload :: forall (ctx :: (Type -> Type) -> Type).
ClientSecret ctx -> TokenPayload ctx
csSignature :: forall (ctx :: (Type -> Type) -> Type).
ClientSecret ctx -> Signature 2048 ctx
csHeader :: TokenHeader ctx
csPayload :: TokenPayload ctx
csSignature :: Signature 2048 ctx
..} =
    let (Bool ctx
sigVerified, ByteString 256 ctx
secretHash) = VarByteString 10328 ctx
-> Signature 2048 ctx
-> PublicKey 2048 ctx
-> (Bool ctx, ByteString 256 ctx)
forall (keyLen :: Natural) (msgLen :: Natural)
       (ctx :: (Type -> Type) -> Type).
RSA keyLen msgLen ctx =>
VarByteString msgLen ctx
-> Signature keyLen ctx
-> PublicKey keyLen ctx
-> (Bool ctx, ByteString 256 ctx)
verifyVar (ClientSecret ctx -> VarByteString 10328 ctx
forall (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, SecretBits ctx) =>
ClientSecret ctx -> VarByteString 10328 ctx
secretBits ClientSecret ctx
cs) Signature 2048 ctx
csSignature PublicKey 2048 ctx
pubKey
     in (VarByteString 320 ctx
pubKid VarByteString 320 ctx
-> VarByteString 320 ctx -> BooleanOf (VarByteString 320 ctx)
forall a. Eq a => a -> a -> BooleanOf a
== TokenHeader ctx -> VarByteString 320 ctx
forall (ctx :: (Type -> Type) -> Type).
TokenHeader ctx -> VarByteString 320 ctx
hdKid TokenHeader ctx
csHeader Bool ctx -> Bool ctx -> Bool ctx
forall b. BoolType b => b -> b -> b
&& Bool ctx
sigVerified, ByteString 256 ctx
secretHash)