Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
ZkFold.Symbolic.Data.VarByteString
Synopsis
- data VarByteString (maxLen :: Natural) (context :: (Type -> Type) -> Type) = VarByteString {
- bsLength :: FieldElement context
- bsBuffer :: ByteString maxLen context
- fromNatural :: forall n ctx. (Symbolic ctx, KnownNat n) => Natural -> Natural -> VarByteString n ctx
- fromByteString :: forall n ctx. (Symbolic ctx, KnownNat n) => ByteString n ctx -> VarByteString n ctx
- toAsciiString :: forall n p. (KnownNat (Div n 8), (Div n 8 * 8) ~ n, KnownNat p) => VarByteString n (Interpreter (Zp p)) -> String
- append :: forall m n ctx. Symbolic ctx => KnownNat m => KnownNat (m + n) => VarByteString m ctx -> VarByteString n ctx -> VarByteString (m + n) ctx
- (@+) :: forall m n ctx. Symbolic ctx => KnownNat m => KnownNat (m + n) => VarByteString m ctx -> VarByteString n ctx -> VarByteString (m + n) ctx
- shiftL :: forall n ctx. Symbolic ctx => KnownNat n => ByteString n ctx -> FieldElement ctx -> ByteString n ctx
- shiftR :: forall n ctx. Symbolic ctx => KnownNat n => ByteString n ctx -> FieldElement ctx -> ByteString n ctx
- wipeUnassigned :: forall n ctx. Symbolic ctx => KnownNat n => VarByteString n ctx -> VarByteString n ctx
Documentation
data VarByteString (maxLen :: Natural) (context :: (Type -> Type) -> Type) Source #
A ByteString that has length unknown at compile time but guaranteed to not exceed maxLen
.
The unassigned buffer space (i.e. bits past bsLength
) should be set to zero at all times.
TODO: Declare all the instances ByteString has for VarByteString
Constructors
VarByteString | |
Fields
|
Instances
fromNatural :: forall n ctx. (Symbolic ctx, KnownNat n) => Natural -> Natural -> VarByteString n ctx Source #
fromByteString :: forall n ctx. (Symbolic ctx, KnownNat n) => ByteString n ctx -> VarByteString n ctx Source #
toAsciiString :: forall n p. (KnownNat (Div n 8), (Div n 8 * 8) ~ n, KnownNat p) => VarByteString n (Interpreter (Zp p)) -> String Source #
append :: forall m n ctx. Symbolic ctx => KnownNat m => KnownNat (m + n) => VarByteString m ctx -> VarByteString n ctx -> VarByteString (m + n) ctx Source #
Join two variable-length ByteStrings and move all the unsaaigned space towards lower indices.
Let u
denote the unassigned space. Then,
uu1010 append
u10010 == uuu101010010
(@+) :: forall m n ctx. Symbolic ctx => KnownNat m => KnownNat (m + n) => VarByteString m ctx -> VarByteString n ctx -> VarByteString (m + n) ctx infixl 6 Source #
shiftL :: forall n ctx. Symbolic ctx => KnownNat n => ByteString n ctx -> FieldElement ctx -> ByteString n ctx Source #
shiftR :: forall n ctx. Symbolic ctx => KnownNat n => ByteString n ctx -> FieldElement ctx -> ByteString n ctx Source #
wipeUnassigned :: forall n ctx. Symbolic ctx => KnownNat n => VarByteString n ctx -> VarByteString n ctx Source #
Set all the unassigned bits to zero