You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Currently, a Layout (UInt n r c) is a Vector (NumberOfRegisters (BaseField c) n r), which is a can of worms:
To work with low and high registers, we need to push/pop them from the vector, which is suboptimal;
Most operations end up requiring KnownNat (NumberOfRegisters (BaseField c) n r) which clutter the constraints;
All in all, we need to compute NumberOfRegisters (BaseField c) n r, which leads to slow compilation and unreadable compilation errors.
All of this can be solved with a custom Layout (UInt n r c) with a custom Representable instance which would only require Symbolic c, KnownNat n and KnownRegisterSize r, which is much more tractable.
P.S. Note that we do not need to make a custom SymbolicData instance for UInt, it's the functor which is used inside that has to be changed from Vector to something else.
The text was updated successfully, but these errors were encountered:
Currently, a
Layout (UInt n r c)
is aVector (NumberOfRegisters (BaseField c) n r)
, which is a can of worms:KnownNat (NumberOfRegisters (BaseField c) n r)
which clutter the constraints;NumberOfRegisters (BaseField c) n r
, which leads to slow compilation and unreadable compilation errors.All of this can be solved with a custom
Layout (UInt n r c)
with a customRepresentable
instance which would only requireSymbolic c
,KnownNat n
andKnownRegisterSize r
, which is much more tractable.P.S. Note that we do not need to make a custom
SymbolicData
instance forUInt
, it's the functor which is used inside that has to be changed fromVector
to something else.The text was updated successfully, but these errors were encountered: