Grey.hs

{-# LANGUAGE RebindableSyntax #-}

module Grey where

import Copilot.Language
import Copilot.Theorem
import Copilot.Theorem.Prover.SMT (def, Options (..), z3, kInduction, induction)

import Prelude ()
import Data.String (fromString)

intCounter :: Stream Bool -> Stream Word64
intCounter reset = time
  where
    time = if reset then 0
           else [0] ++ if time == 3 then 0 else time + 1

greyTick :: Stream Bool -> Stream Bool
greyTick reset = a && b
  where
    a = (not reset) && ([False] ++ not b)
    b = (not reset) && ([False] ++ a)

spec = do
  theorem "iResetOk"   (forAll $ r ==> (ic == 0)) induct
  theorem "eqCounters" (forAll $ it == gt) $ kinduct 3

  where
    ic = intCounter r
    it = ic == 2
    gt = greyTick r
    r  = extern "reset" Nothing

induct :: Proof Universal
induct = induction def { debug = False } z3

kinduct :: Word32 -> Proof Universal
kinduct k = kInduction def { startK = k, maxK = k, debug = False } z3