examples/IFLDemos.hs

   1 {-# OPTIONS_GHC -XModalTypes -dcore-lint -XScopedTypeVariables -ddump-types -XTypeFamilies -XNoMonomorphismRestriction #-}
   2 module Demo (demo, demo2) where
   3
   4 {-
   5 demo ::
   6   <[ \input ->
   7         let delayed = ~~reg output
   8             output  = ~~xor input delayed
   9         in output ]>
  10 -}
  11
  12 demo  z   = <[ \y -> ~~z ]>
  13
  14 demo2 :: <[ (a,b) ~~> c ]>@d -> <[ () ~~> a ]>@d -> <[ b ~~>c ]>@d
  15 demo2 x y = <[ ~~x ~~y ]>
  16
  17 swap :: <[ (a,(b,c)) ~~> d ]>@e -> <[ (b,(a,c)) ~~> d ]>@e
  18 swap f = <[ \x -> \y -> ~~f y x ]>
  19
  20 -- bad = <[ \f -> \x -> f x ]>
  21
  22 demo3 x y z q = <[ ~~q (~~x ~~y ~~z) ]>
  23
  24
  25
  26 class BitSerialHardwarePrimitives g where
  27   type Wire
  28
  29   <[ not ]>    :: <[             (Wire,())    ~~> Wire ]>@g
  30   <[ xor ]>    :: <[       (Wire,(Wire,()))   ~~> Wire ]>@g
  31   <[ or  ]>    :: <[       (Wire,(Wire,()))   ~~> Wire ]>@g
  32   <[ and ]>    :: <[       (Wire,(Wire,()))   ~~> Wire ]>@g
  33   <[ mux2 ]>   :: <[ (Wire,(Wire,(Wire,())))  ~~> Wire ]>@g
  34   <[ maj3 ]>   :: <[ (Wire,(Wire,(Wire,())))  ~~> Wire ]>@g
  35   <[ reg ]>    :: <[             (Wire,())    ~~> Wire ]>@g
  36   <[ zero ]>   :: <[             ()    ~~> Wire ]>@g
  37   <[ one ]>    :: <[             ()    ~~> Wire ]>@g
  38
  39   loop   :: [Bool] -> <[ () ~~> Wire ]>@g
  40   <[ lfsr ]>   :: Int ->  [ <[ Wire ]>@g ]
  41   <[ adder ]>  :: <[  (Wire,(Wire,())) ~~> Wire ]>@g
  42   fifo         :: Int -> <[  (Wire,()) ~~> Wire ]>@g
  43
  44   <[ probe ]>  :: Int -> <[ (Wire,())  ~~> Wire ]>@g
  45   <[ oracle ]> :: Int -> <[                Wire ]>@g
  46
  47 xor3 :: forall g . BitSerialHardwarePrimitives g => <[ (Wire,(Wire,(Wire,()))) ~~> Wire ]>@g
  48 xor3 = <[ \x -> \y -> \z -> xor (xor x y) z ]>
  49
  50 adder =
  51    <[ \in1 ->
  52       \in2 ->
  53       let firstBitMarker = ~~(loop [ i/=0 | i <- [0..31] ])
  54           carry_out      = reg (mux2 firstBitMarker zero carry_in)
  55           carry_in       = maj3 carry_out in1 in2
  56       in  ~~xor3 carry_out in1 in2
  57     ]>
  58
  59
  60 rotRight n =
  61   <[ \input ->
  62      let sel   = ~~(loop [ i >= 32-n | i<-[0..31] ])
  63          fifo1 = ~~(fifo (32-n)) input
  64          fifo2 = ~~(fifo  32   ) fifo1
  65      in  mux2 sel fifo1 fifo2
  66    ]>
  67
  68 sha256round =
  69   <[ \load ->
  70      \input ->
  71      \k_plus_w ->
  72      let a    = ~~(fifo 32) (mux2 load a_in input)
  73          b    = ~~(fifo 32) a
  74          c    = ~~(fifo 32) b
  75          d    = ~~(fifo 32) c
  76          e    = ~~(fifo 32) (mux2 load e_in d)
  77          f    = ~~(fifo 32) e
  78          g    = ~~(fifo 32) f
  79          h    = ~~(fifo 32) g
  80          s0   = ~~xor3
  81                     (~~(rotRight  2) a_in)
  82                     (~~(rotRight 13) a_in)
  83                     (~~(rotRight 22) a_in)
  84          s1   = ~~xor3
  85                     (~~(rotRight  6) e_in)
  86                     (~~(rotRight 11) e_in)
  87                     (~~(rotRight 25) e_in)
  88          a_in = adder t1 t2
  89          e_in = adder t1 d
  90          t1   = adder
  91                    (adder h s1)
  92                    (adder (mux2 e g f)
  93                           k_plus_w)
  94          t2   = adder s0 (maj3 a b c)
  95      in h
  96    ]>