copilot-verifier demo from YouTube video

This is the code from a demo for a video that I recorded. I have found myself
using it to introduce people to the code, so we ought to just merge this for
future use.

Author: RyanGlScott

cabal.project

@@ -6,6 +6,7 @@
 
 packages:
   copilot-verifier/
+  copilot-verifier-demo/
 
   deps/copilot/copilot/
   deps/copilot/copilot-core/

copilot-verifier-demo/.gitignore

@@ -0,0 +1,15 @@
+demo1.c
+demo1.h
+demo1_types.h
+demo1-driver
+demo1-driver.exe
+
+demo2.c
+demo2.h
+demo2_types.h
+demo2-driver
+demo2-driver.exe
+
+demo3.c
+demo3.h
+demo3_types.h

copilot-verifier-demo/LICENSE

@@ -0,0 +1,30 @@
+Copyright (c) 2021 Galois Inc.
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions
+are met:
+
+  * Redistributions of source code must retain the above copyright
+    notice, this list of conditions and the following disclaimer.
+
+  * Redistributions in binary form must reproduce the above copyright
+    notice, this list of conditions and the following disclaimer in
+    the documentation and/or other materials provided with the
+    distribution.
+
+  * Neither the name of Galois, Inc. nor the names of its contributors
+    may be used to endorse or promote products derived from this
+    software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS
+IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
+TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
+PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER
+OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

copilot-verifier-demo/copilot-verifier-demo.cabal

@@ -0,0 +1,42 @@
+Cabal-version: 2.2
+Name:          copilot-verifier-demo
+Version:       0.0
+Author:        Galois Inc.
+Maintainer:    rscott@galois.com
+Copyright:     (c) Galois, Inc 2022
+License:       BSD-3-Clause
+License-file:  LICENSE
+Build-type:    Simple
+Category:      Language
+Synopsis:      Demo programs for copilot-verifier
+Description:
+
+common bldflags
+  ghc-options: -Wall
+               -Werror=incomplete-patterns
+               -Werror=missing-methods
+               -Werror=overlapping-patterns
+               -Wpartial-fields
+               -Wincomplete-uni-patterns
+  ghc-prof-options: -O2 -fprof-auto-top
+  default-language: Haskell2010
+  default-extensions:
+     NondecreasingIndentation
+  build-depends:
+    base,
+    copilot,
+    copilot-c99,
+    copilot-core,
+    copilot-libraries,
+    copilot-language,
+    copilot-theorem,
+    copilot-verifier
+
+library
+  import: bldflags
+
+  hs-source-dirs: src
+  exposed-modules:
+    Demo1
+    Demo2
+    Demo3

copilot-verifier-demo/demo1-driver.c

@@ -0,0 +1,20 @@
+#include <stdint.h>
+#include <stdio.h>
+#include "demo1.h"
+
+#define ITERATIONS 6
+
+void even(uint32_t even_arg0) {
+  printf("Even Fibonacci number: %d\n", even_arg0);
+}
+
+void odd(uint32_t odd_arg0) {
+  printf("Odd  Fibonacci number: %d\n", odd_arg0);
+}
+
+int main(void) {
+  for (int i = 0; i < ITERATIONS; i++) {
+    step();
+  }
+  return 0;
+}

copilot-verifier-demo/demo2-driver.c

@@ -0,0 +1,24 @@
+#include <stdint.h>
+#include <stdio.h>
+#include "demo2.h"
+
+uint8_t temperature;
+
+#define ITERATIONS 4
+uint8_t temperature_vals[ITERATIONS] = { 100, 120, 120, 120 };
+
+void heaton(float heaton_arg0) {
+  printf("Temperature below 18.0: %f\n", heaton_arg0);
+}
+
+void heatoff(float heatoff_arg0) {
+  printf("Temperature above 21.0: %f\n", heatoff_arg0);
+}
+
+int main(void) {
+  for (int i = 0; i < ITERATIONS; i++) {
+    temperature = temperature_vals[i];
+    step();
+  }
+  return 0;
+}

copilot-verifier-demo/src/Demo1.hs

@@ -0,0 +1,32 @@
+-- A simple example involving a stream of Fibonacci numbers.
+
+{-# LANGUAGE RebindableSyntax #-}
+module Demo1 (main) where
+
+import qualified Prelude as P ()
+
+import Language.Copilot
+import Copilot.Compile.C99
+import Copilot.Verifier
+
+fibs :: Stream Word32
+fibs = [1, 1] ++ (fibs + drop 1 fibs)
+
+evenStream :: Stream Word32 -> Stream Bool
+evenStream n = (n `mod` constant 2) == constant 0
+
+oddStream :: Stream Word32 -> Stream Bool
+oddStream n = not (evenStream n)
+
+spec :: Spec
+spec = do
+  trigger "even" (evenStream fibs) [arg fibs]
+  trigger "odd"  (oddStream fibs) [arg fibs]
+
+main :: IO ()
+main = do
+  interpret 6 spec
+
+  -- spec' <- reify spec
+  -- compile "demo1" spec'
+  -- verify mkDefaultCSettings [] "demo1" spec'

copilot-verifier-demo/src/Demo2.hs

@@ -0,0 +1,44 @@
+-- This is a simple example with basic usage. It implements a simple home
+-- heating system: It heats when temp gets too low, and stops when it is high
+-- enough. It read temperature as a byte (range -50C to 100C) and translates
+-- this to Celcius.
+
+{-# LANGUAGE RebindableSyntax #-}
+module Demo2 (main) where
+
+import qualified Prelude as P ()
+
+import Language.Copilot
+import Copilot.Compile.C99
+import Copilot.Verifier
+
+-- External temperature as a byte, range of -50C to 100C
+temp :: Stream Word8
+temp = extern "temperature"
+              Nothing
+              -- (Just [100, 120, 120, 120])
+
+-- Calculate temperature in Celcius.
+-- We need to cast the Word8 to a Float. Note that it is an unsafeCast, as there
+-- is no direct relation between Word8 and Float.
+ctemp :: Stream Float
+ctemp = (unsafeCast temp * constant (150.0/255.0)) - constant 50.0
+
+-- Compute the sliding average of the last 5 temps
+-- (Here, 19.5 is the average of 18.0 and 21.0, the two temperature extremes
+-- that we check for in the spec.)
+avgTemp :: Stream Float
+avgTemp = (sum 5 (replicate 5 19.5 ++ ctemp)) / fromIntegral 5
+
+spec :: Spec
+spec = do
+  trigger "heaton"  (avgTemp < 18.0) [arg avgTemp]
+  trigger "heatoff" (avgTemp > 21.0) [arg avgTemp]
+
+main :: IO ()
+main = do
+  -- interpret 4 spec
+
+  spec' <- reify spec
+  compile "demo2" spec'
+  verify mkDefaultCSettings [] "demo2" spec'