Add boundary proofs to dfold and smap

[kleinreact]

The PR extends dfold with a boundary proof for the folded function and introduces smapWithBounds offering a boundary proof as well. smapWithBounds is introduced in addition to smap, as the served proof may lead to untouchable errors requiring additional type annotations. While this is fine for dfold, 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 letter L) to n to make them better distinguishable from the constant 1.

[martijnbastiaan]

I'm curious; what motivated you to implement this? Any concrete example where you need the boundary proof?

[kleinreact]

I would use it here, but the currently used workaround is also sufficient. It is required to use the Resize class in that case.

[rowanG077]

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.

[martijnbastiaan]

Could you write a changelog entry? See changelog/README.md for instructions.

[martijnbastiaan]

Why did we change dfold, but introduced an additional function for smap?

Because the evaluator rules aren't easy to review: could you add a test for the evaluator (and primitive reduction?) of these functions? It's a bit cumbersome to write these functions as you'd:

• Need to make sure GHC doesn't do any constant folding for you
• Clash does do the constant folding (perhaps with -fclash-ultra)

You can do something similar to T2542.hs in terms of checking whether some constant ended up in the HDL.

I'm also not sure what the difference is between "primitive reduction" and "evaluating", maybe @christiaanb can comment on that / how to write a test for both.

[kleinreact]

Why did we change dfold, but introduced an additional function for smap?

The primary argument was that smap may be used by beginners, which may be overwhelmed by the extended type signature required for the proof. On the other hand, dfold is not beginner friendly in terms of the type signature anyway, which is why it shouldn't hurt to introduce the changes directly there.

[martijnbastiaan]

Makes sense!

[martijnbastiaan]

@christiaanb Are you happy with the applied changes?