{-# LANGUAGE RebindableSyntax #-}

module Copilot.Verifier.Examples.ShouldPass.Arith where

import Control.Monad (when)
import qualified Prelude as P

import Language.Copilot
import Copilot.Compile.C99
import Copilot.Verifier ( Verbosity(..), VerifierOptions(..)
                        , defaultVerifierOptions, verifyWithOptions )
import Copilot.Theorem.What4 (prove, Solver(..))

-- The largest unsigned 32-bit prime
lastPrime :: Stream Word32
lastPrime :: Stream Word32
lastPrime = Stream Word32
31
--lastPrime = 4294967291 -- Whelp, this prime seems too big for the solvers to handle well

multRingSpec :: Spec
multRingSpec :: Spec
multRingSpec = do
  PropRef Universal
_ <- Name -> Prop Universal -> Writer [SpecItem] (PropRef Universal)
forall a. Name -> Prop a -> Writer [SpecItem] (PropRef a)
prop Name
"clamp nonzero" (Stream Bool -> Prop Universal
forAll ((Stream Word32
clamp Stream Word32 -> Stream Word32 -> Stream Bool
forall a. (Ord a, Typed a) => Stream a -> Stream a -> Stream Bool
> Stream Word32
0) Stream Bool -> Stream Bool -> Stream Bool
&& (Stream Word32
clamp Stream Word32 -> Stream Word32 -> Stream Bool
forall a. (Ord a, Typed a) => Stream a -> Stream a -> Stream Bool
< Stream Word32
lastPrime)))
  PropRef Universal
_ <- Name -> Prop Universal -> Writer [SpecItem] (PropRef Universal)
forall a. Name -> Prop a -> Writer [SpecItem] (PropRef a)
prop Name
"reduced" (Stream Bool -> Prop Universal
forAll (Stream Word32
acc Stream Word32 -> Stream Word32 -> Stream Bool
forall a. (Ord a, Typed a) => Stream a -> Stream a -> Stream Bool
< Stream Word32
lastPrime))
  PropRef Universal
_ <- Name -> Prop Universal -> Writer [SpecItem] (PropRef Universal)
forall a. Name -> Prop a -> Writer [SpecItem] (PropRef a)
prop Name
"nonzero" (Stream Bool -> Prop Universal
forAll (Stream Word32
acc Stream Word32 -> Stream Word32 -> Stream Bool
forall a. (Ord a, Typed a) => Stream a -> Stream a -> Stream Bool
> Stream Word32
0 Stream Bool -> Stream Bool -> Stream Bool
&& (Stream Word32
acc Stream Word32 -> Stream Word32 -> Stream Bool
forall a. (Ord a, Typed a) => Stream a -> Stream a -> Stream Bool
< Stream Word32
lastPrime)))

  Name -> Stream Bool -> [Arg] -> Spec
trigger Name
"outofrange" (Stream Bool -> Stream Bool
not (Stream Word32
acc Stream Word32 -> Stream Word32 -> Stream Bool
forall a. (Ord a, Typed a) => Stream a -> Stream a -> Stream Bool
> Stream Word32
0 Stream Bool -> Stream Bool -> Stream Bool
&& Stream Word32
acc Stream Word32 -> Stream Word32 -> Stream Bool
forall a. (Ord a, Typed a) => Stream a -> Stream a -> Stream Bool
< Stream Word32
lastPrime)) [Stream Word32 -> Arg
forall a. Typed a => Stream a -> Arg
arg Stream Word32
acc]

  () -> Spec
forall a. a -> WriterT [SpecItem] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

  where
  -- a stream of external values
  vals :: Stream Word32
vals  = Name -> Maybe [Word32] -> Stream Word32
externW32 Name
"values" Maybe [Word32]
forall a. Maybe a
Nothing

  -- Generate a value in [1, lastPrime), which
  -- is the multiplictive group of Z_p
  clamp :: Stream Word32
  clamp :: Stream Word32
clamp = (Stream Word32
vals Stream Word32 -> Stream Word32 -> Stream Word32
forall a. (Typed a, Integral a) => Stream a -> Stream a -> Stream a
`mod` (Stream Word32
lastPrime Stream Word32 -> Stream Word32 -> Stream Word32
forall a. Num a => a -> a -> a
- Stream Word32
1)) Stream Word32 -> Stream Word32 -> Stream Word32
forall a. Num a => a -> a -> a
+ Stream Word32
1

  -- Successively multiply new values
  acc :: Stream Word32
  acc :: Stream Word32
acc = [Word32
1] [Word32] -> Stream Word32 -> Stream Word32
forall a. Typed a => [a] -> Stream a -> Stream a
++ Stream Word64 -> Stream Word32
forall a b.
(UnsafeCast a b, Typed a, Typed b) =>
Stream a -> Stream b
unsafeCast ((Stream Word32 -> Stream Word64
forall a b. (Cast a b, Typed a, Typed b) => Stream a -> Stream b
cast Stream Word32
acc Stream Word64 -> Stream Word64 -> Stream Word64
forall a. Num a => a -> a -> a
* Stream Word32 -> Stream Word64
forall a b. (Cast a b, Typed a, Typed b) => Stream a -> Stream b
cast Stream Word32
clamp) Stream Word64 -> Stream Word64 -> Stream Word64
forall a. (Typed a, Integral a) => Stream a -> Stream a -> Stream a
`mod` (Stream Word32 -> Stream Word64
forall a b. (Cast a b, Typed a, Typed b) => Stream a -> Stream b
cast Stream Word32
lastPrime :: Stream Word64))

verifySpec :: Verbosity -> IO ()
verifySpec :: Verbosity -> IO ()
verifySpec Verbosity
verb =
  do Spec
s <- Spec -> IO Spec
forall a. Spec' a -> IO Spec
reify Spec
multRingSpec
     [(Name, SatResult)]
r <- Solver -> Spec -> IO [(Name, SatResult)]
prove Solver
Z3 Spec
s
     Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Verbosity
verb Verbosity -> Verbosity -> Bool
forall a. Ord a => a -> a -> Bool
P.>= Verbosity
Default) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
       [(Name, SatResult)] -> IO ()
forall a. Show a => a -> IO ()
print [(Name, SatResult)]
r
     VerifierOptions -> CSettings -> [Name] -> Name -> Spec -> IO ()
verifyWithOptions VerifierOptions
defaultVerifierOptions{verbosity = verb}
                       CSettings
mkDefaultCSettings [Name
"reduced"] Name
"multRingSpec" Spec
s

--verifySpec _ = interpret 10 engineMonitor