Haskell¶

libs¶

• concat (z3cat || smt example) — Compiling to categories — compiler plugin for translating normal Haskell functions (on standard types) to SMT, etc.
• SBV: SMT Based Verification — translates Haskell functions on custom symbolic types
• refined — refinement types

  type ProperFraction = Refined (And (Not (LessThan 0)) (Not (GreaterThan 1))) Double

• hedgehog — random test gen (QuickCheck)
• GHC.Stack — can get code position for DSL
• Data.Sequence — list with fast append on both sides

exts¶

• RebindableSyntax — overloading built-in operators / do notation
• NullaryTypeClasses — global implementation of one thing

snippets¶

Using Maybe Monad for checks¶

{-# LANGUAGE LambdaCase, RecordWildCards #-}

import Data.Maybe (isJust, mapMaybe)
import Data.List (nub)

data Group = X25519 | Secp384
           deriving (Eq)

data KeyShareData = KeyShareClientHello [Group]
                  | KeyShareHelloRetryRequest Group

data Ext = SupportedGroups [Group]
         | KeyShares KeyShareData

check :: [Ext] -> [Ext] -> Bool
check eCH eHRR = isJust $ do
  sgCH <- exactlyOne $ mapMaybe (\case SupportedGroups gs -> Just gs; _ -> Nothing) eCH
  continueIf $ nub sgCH == sgCH -- no duplicates allowed
  ksCH <- (\case KeyShareClientHello gs -> Just gs; _ -> Nothing) =<<
    exactlyOne (mapMaybe (\case KeyShares ks -> Just ks; _ -> Nothing) eCH)
  ksHRR <- (\case KeyShareHelloRetryRequest g -> Just g; _ -> Nothing) =<<
    exactlyOne (mapMaybe (\case KeyShares ks -> Just ks; _ -> Nothing) eHRR)
  continueIf $ nub ksCH == ksCH -- no duplicates allowed
  continueIf $ ksHRR `elem` sgCH -- group must be supported
  continueIf $ ksHRR `notElem` ksCH -- key share must not have been already sent

exactlyOne :: [a] -> Maybe a
exactlyOne [x] = Just x
exactlyOne _ = Nothing

continueIf :: Bool -> Maybe ()
continueIf True = Just ()
continueIf False = Nothing