-
Notifications
You must be signed in to change notification settings - Fork 147
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Add boundary proofs to dfold
and smap
#2686
base: master
Are you sure you want to change the base?
Conversation
I'm curious; what motivated you to implement this? Any concrete example where you need the boundary proof? |
I would use it here, but the currently used workaround is also sufficient. It is required to use the |
I have ran into this a few times. And just now I ran into it again. I was trying to do some type magics to allow dynamic(As in type level configurable) multi lane CRC to work. I tried to do something like this: data CRCLaneParams (crcWidth :: Nat) (dataWidth :: Nat) (lanes :: Nat) where
CRCLane0
:: CircuitCRCParams crcWidth dataWidth
-> CRCLaneParams crcWidth dataWidth 0
CRCLaneN
:: 1 <= lanes
=> SNat lanes
-> CircuitCRCParams crcWidth ((lanes + 1) * dataWidth)
-> CRCLaneParams crcWidth dataWidth (lanes - 1)
-> CRCLaneParams crcWidth dataWidth lanes
-- | Get the Circuit params for a given lane
getCircuitParams
:: lane <= lanes
=> CRCLaneParams crcWidth dataWidth lanes
-> SNat lane
-> CircuitCRCParams crcWidth ((lane + 1) * dataWidth)
getCircuitParams = ...
-- | Create a CRC step function that takes a larger input of which a subset is ignored to make types match.
mkStep
:: forall (crcWidth :: Nat)
(dataWidth :: Nat)
(dataWidthFull :: Nat)
. SNat dataWidthFull
-> CircuitCRCParams crcWidth dataWidth
-> BitVector crcWidth
-- ^ The current CRC state
-> BitVector dataWidthFull
-- ^ The input
-> BitVector crcWidth
-- ^ The next CRC state
mkStep = ...
-- | A multi-lane CRC engine
crcEngine
:: forall (nLanes :: Nat)
(dom :: Domain)
(crcWidth :: Nat)
(dataWidth :: Nat)
. HiddenClockResetEnable dom
=> KnownNat nLanes
=> KnownNat crcWidth
=> KnownNat dataWidth
=> 1 <= nLanes
=> CRCLaneParams crcWidth dataWidth (nLanes - 1)
-> Signal dom (Maybe (Vec nLanes (BitVector dataWidth)))
-> Signal dom (Index nLanes)
-> ( Signal dom (BitVector crcWidth)
, Signal dom Bool
)
crcEngine laneParams dataIn validLane = ...
where
-- Cannot satisfy: v <= nLanes - 1
engines = smap (\v _ -> mkStep SNat $ getCircuitParams laneParams v) (repeat @nLanes ())
engine :: Signal dom (BitVector crcWidth -> BitVector (dataWidth * nLanes) -> BitVector crcWidth)
engine = fmap (\n -> engines !! n) validLane Note that I'm not sure whether this is the way to go here it was just experimentation. But it came up naturally at least. |
e60d4a3
to
46e7be3
Compare
41f0b7e
to
15579b4
Compare
Could you write a changelog entry? See |
15579b4
to
795312c
Compare
Co-authored-by: Christiaan Baaij <christiaan.baaij@gmail.com>
795312c
to
17d3142
Compare
The PR extends
dfold
with a boundary proof for the folded function and introducessmapWithBounds
offering a boundary proof as well.smapWithBounds
is introduced in addition tosmap
, as the served proof may lead tountouchable
errors requiring additional type annotations. While this is fine fordfold
, which requires advanced knowledge of the type system for usage anyway,smap
should stay intuitive for beginners, which is why we introduce an additional version instead.The PR also renames typenat variables
l
(small letterL
) ton
to make them better distinguishable from the constant1
.