satAdd and satMul produce errors for Index 1

[rowanG077]

satAdd and satMul with any of the SaturationModes results in out of bounds exceptions when used with Index 1 even though the operations should be safe. satSub works fine.

satModes = [SatWrap, SatBound, SatZero, SatSymmetric]
operations = [satAdd, satSub, satMul]
n = 0 :: Index 1
results = showX [f n n | f <- operations <*> satModes] -- [X,X,X,X,0,0,0,0,X,X,X,X]

It's due to usage of the following code in each of those operations:

m :: AResult (Index 1) (Index 1)  or m :: MResult (Index 1) (Index 1) 
m = fromInteger# (natVal (Proxy @ n))

m thus has value 1 and since AResult (Index 1) (Index 1) ~ Index 1 and MResult (Index 1) (Index 1) ~ Index 1 this is never a valid value and the error is triggered.

See here.

[martijnbastiaan]

Good catch. So we should change bound checking to 'greater than', instead of 'greater than or equal to'. For example, in satAdd SatWrap:

--- a/clash-prelude/src/Clash/Sized/Internal/Index.hs
+++ b/clash-prelude/src/Clash/Sized/Internal/Index.hs
@@ -281,8 +281,8 @@ instance (KnownNat n, 1 <= n) => SaturatingNum (Index n) where
   satAdd SatWrap a b =
     leToPlusKN @1 @n $
       case plus# a b of
-        z | let m = fromInteger# (natVal (Proxy @ n))
-          , z >= m -> resize# (z - m)
+        z | let m = fromInteger# (natVal (Proxy @ (n - 1)))
+          , z > m -> resize# (z - m)
         z -> resize# z
   satAdd SatZero a b =
     leToPlusKN @1 @n $

..would presumably fix the issue.

[rowanG077]

Good catch. So we should change bound checking to 'greater than', instead of 'greater than or equal to'. For example, in satAdd SatWrap:

--- a/clash-prelude/src/Clash/Sized/Internal/Index.hs
+++ b/clash-prelude/src/Clash/Sized/Internal/Index.hs
@@ -281,8 +281,8 @@ instance (KnownNat n, 1 <= n) => SaturatingNum (Index n) where
   satAdd SatWrap a b =
     leToPlusKN @1 @n $
       case plus# a b of
-        z | let m = fromInteger# (natVal (Proxy @ n))
-          , z >= m -> resize# (z - m)
+        z | let m = fromInteger# (natVal (Proxy @ (n - 1)))
+          , z > m -> resize# (z - m)
         z -> resize# z
   satAdd SatZero a b =
     leToPlusKN @1 @n $

..would presumably fix the issue.

Unfortunately it's not so simple. When you make m one smaller then (z - m) no longer has the correct value when an overflow occurs for SatWrap. The same issue occurs in SatMul as well.

[martijnbastiaan]

Oh darn, of course. Would

--- a/clash-prelude/src/Clash/Sized/Internal/Index.hs
+++ b/clash-prelude/src/Clash/Sized/Internal/Index.hs
@@ -281,8 +281,8 @@ instance (KnownNat n, 1 <= n) => SaturatingNum (Index n) where
   satAdd SatWrap a b =
     leToPlusKN @1 @n $
       case plus# a b of
-        z | let m = fromInteger# (natVal (Proxy @ n))
-          , z >= m -> resize# (z - m)
+        z | let m0 = fromInteger# (natVal (Proxy @ (n - 1)))
+                m1 = fromInteger# (natVal (Proxy @ n))
+          , z > m0 -> resize# (z - m1)
         z -> resize# z
   satAdd SatZero a b =
     leToPlusKN @1 @n $

work? I guess this case only happens for Index 1, and you can't get an overflow whatever you do, so m1 would never be evaluated. Alternatively, we could just special case for Index 1, to make it more explicit.

[martijnbastiaan]

Maybe even something "radical" like:

instance SaturatingNum (Index 1) where 

[rowanG077]

I think special casing it is the most simple and obvious. You could also do something like this at the type level:

I created a new function so I can quickly iterate on it:

satAdd'
  :: forall (n      :: Nat) 
            (aWidth :: Nat)
            (addOne :: Nat)
   . ( KnownNat n
     , KnownNat aWidth
     , KnownNat addOne
     , 1 <= n
     , Index aWidth ~ AResult (Index n) (Index n)
     , addOne ~ Max aWidth (n + 1)
     )
  => SaturationMode -> Index n -> Index n -> Index n 
satAdd' SatWrap a b =
  leToPlusKN @1 @n $
    case (resize $ add a b) of
      z | let m :: Index addOne = fromInteger (natVal (Proxy @ n))
        , z >= (m) -> resize (z - m)
      z -> resize z

However This would add quite a few constraints.

[martijnbastiaan]

We can't really add constraints to satAdd, so I don't think we can go that route. I think a separate instance would simply be best, which would look something like:

{-# LANGUAGE BangPatterns #-} 

instance {-# OVERLAPPING #-} SaturatingNum (Index 1) where
  satAdd _ !a !b = 0
  satSub _ !a !b = 0
  ...

and change the original instance to:

instance (KnownNat n, 2 <= n) => SaturatingNum (Index n) where

[rowanG077]

It's not possible to do this with the {-# OVERLAPPING #-} pragma as far as I understand it. The documentation says the following:

• Find all instances (I) that match the target constraint; that is, the target constraint is a substitution instance of (I). These instance declarations are the candidates.
• Eliminate any candidate (IX) for which both of the following hold:
  • There is another candidate (IY) that is strictly more specific; that is, (IY) is a substitution instance of (IX) but not vice versa.
  • Either (IX) is overlappable, or (IY) is overlapping. (This “either/or” design, rather than a “both/and” design, allow a client to deliberately override an instance from a library, without requiring a change to the library.)
• If exactly one non-incoherent candidate remains, select it. If all remaining candidates are incoherent, select an arbitrary one. Otherwise the search fails (i.e. when more than one surviving candidate is not incoherent).
• If the selected candidate (from the previous step) is incoherent, the search succeeds, returning that candidate.
• If not, find all instances that unify with the target constraint, but do not match it. Such non-candidate instances might match when the target constraint is further instantiated. If all of them are incoherent, the search succeeds, returning the selected candidate; if not, the search fails.

https://downloads.haskell.org/ghc/8.6.5/docs/html/users_guide/glasgow_exts.html#overlapping-instances

1 is not more specific then n in this context. They are both just Nat and thus no instance is ever eliminated as per the first elimination condition.

[martijnbastiaan]

You're right that, by default, Index 1 is not more specific than Index n. But after:

There is another candidate (IY) that is strictly more specific; that is, (IY) is a substitution instance of (IX) but not vice versa.

.. it explains how specificness works in face of Overlapp{ing,able} pragmas:

• Either (IX) is overlappable (no)
• or (IY) is overlapping. (yes!)

Because Index 1 (IY) is overlapping, it is more specific.

Usually, overlapping instances are frowned upon in the Haskell world (due to them potentially breaking consistency), but they're perfectly okay if you use them next to the definition of the type you're making an instance for.

[rowanG077]

I interpret this specificity as the specifity of types. E.g. Int would be more specific then Num.

Tried it just now and I can't get it to work. It always complains about the overlapping instances.

[martijnbastiaan]

Blimey, you're right! Looks like this isn't going to work! I could have sworn the conditions mentioned were either not and.

[martijnbastiaan]

I guess that just forces us to case on the /n/ then. Something like:

+{-# LANGUAGE BangPatterns          #-}
 {-# LANGUAGE CPP                   #-}
 {-# LANGUAGE DataKinds             #-}
 {-# LANGUAGE DeriveAnyClass        #-}
@@ -101,7 +102,7 @@ import Clash.Class.Resize         (Resize (..))
 import Clash.Prelude.BitIndex     (replaceBit)
 import {-# SOURCE #-} Clash.Sized.Internal.BitVector (BitVector (BV), high, low, undefError)
 import qualified Clash.Sized.Internal.BitVector as BV
-import Clash.Promoted.Nat         (SNat, snatToNum, leToPlusKN)
+import Clash.Promoted.Nat         (SNat(..), snatToNum, leToPlusKN)
 import Clash.XException
   (ShowX (..), Undefined (..), errorX, showsPrecXWith, rwhnfX)
 
@@ -278,12 +279,14 @@ times# :: Index m -> Index n -> Index (((m - 1) * (n - 1)) + 1)
 times# (I a) (I b) = I (a * b)
 
 instance (KnownNat n, 1 <= n) => SaturatingNum (Index n) where
-  satAdd SatWrap a b =
-    leToPlusKN @1 @n $
-      case plus# a b of
-        z | let m = fromInteger# (natVal (Proxy @ n))
-          , z >= m -> resize# (z - m)
-        z -> resize# z
+  satAdd SatWrap !a !b =
+    case snatToNum @Int (SNat @n) of
+      1 -> 0
+      _ -> leToPlusKN @1 @n $
+        case plus# a b of
+          z | let m = fromInteger# (natVal (Proxy @ n))
+            , z >= m -> resize# (z - m)
+          z -> resize# z
   satAdd SatZero a b =
     leToPlusKN @1 @n $
       case plus# a b of

Clash eliminates Index 1 in HDL completely and will eliminate the branch, so we don't have to worry about blackboxes. (He said confidently. I'll write a test once we fix this.)

[rowanG077]

Actually I discovered something more sinister. For all numeric types which have bitSize 0 HDL generation is broken. See the topEntity below with the resulting generated HDL below it.

topEntity
  :: Clock System
  -> Reset System
  -> Signal System (Signed 0)
  -- -> Signal System (Unsigned 0)
  -- -> Signal System (Index 1)
  -- -> Signal System (SFixed 0 0)
  -- -> Signal System (UFixed 0 0)
topEntity clk rst = pure $ satAdd SatWrap 0 0

VHDL

-- Automatically generated VHDL-93
library IEEE;
use IEEE.STD_LOGIC_1164.ALL;
use IEEE.NUMERIC_STD.ALL;
use IEEE.MATH_REAL.ALL;
use std.textio.all;
use work.all;
use work.test2_types.all;

entity test2_topentity is
  port(-- clock
       clk : in test2_types.clk_system;
       -- reset
       rst : in test2_types.rst_system);
end;

architecture structural of test2_topentity is


begin

end;

Verilog

/* AUTOMATICALLY GENERATED VERILOG-2001 SOURCE CODE.
** GENERATED BY CLASH 0.9999. DO NOT MODIFY.
*/
`timescale 100fs/100fs
module Test2_topEntity
    ( // Inputs
      input  clk // clock
    , input  rst // reset

      // No outputs
    );

I know that at least in VHDL you can't have an signed, unsigned or std_logic_vector with 0 length. I think we have two options:

• Disallow creation of such types by introducing a constraint on each type by making them GADTs.
  I'm not sure if making all of these type GADTs introduces other problems though. It will certainly break backwards compatibility due to the new constraints.

• Change the BitPack instance of these types to always have at least a BitSize of 1. This opens a different can of worm though because then many operations have to be special cased.

[martijnbastiaan]

We actually do this on purpose! It's quite common in Haskell to write code in such a way that you end up with zero-width constructs. Because HDL tools don't handle zero-width constructs well, we strip it out entirely.

[rowanG077]

I See. My panic was for nothing then 😅.

[martijnbastiaan]

Fixed after merging #686