what4-transition-system: v0.0.1.0

.gitmodules

@@ -7,3 +7,10 @@
 [submodule "dependencies/blt"]
 	path = dependencies/blt
 	url = https://github.com/GaloisInc/blt
+[submodule "dependencies/parameterized-utils"]
+	path = dependencies/parameterized-utils
+	url = https://github.com/GaloisInc/parameterized-utils
+[submodule "dependencies/language-sally"]
+	path = dependencies/language-sally
+	url = https://github.com/GaloisInc/language-sally.git
+

dependencies/language-sally

@@ -0,0 +1 @@
+Subproject commit a52404a9d3f2ff88809f0ad2832ffa518b7ac89b

what4-transition-system/LICENSE

@@ -0,0 +1,30 @@
+Copyright (c) 2020 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.

what4-transition-system/package.yaml

@@ -0,0 +1,45 @@
+author:
+  - Valentin Robert <valentin.robert.42@gmail.com>
+
+copyright: Galois, Inc. 2020
+
+dependencies:
+  - ansi-wl-pprint ^>= 0.6
+  - base ^>= 4.13
+  - bytestring
+  - containers ^>= 0.6
+  - io-streams
+  - lens
+  - language-sally ^>= 0.2
+  - mtl
+  - parameterized-utils ^>= 2.0
+  - text
+  - what4
+
+description: Generates transition systems from What4 descriptions
+
+ghc-options:
+  - -Wall
+  - -Werror=incomplete-patterns
+  - -Werror=missing-methods
+  - -Werror=overlapping-patterns
+
+library:
+  exposed-modules:
+    - What4.TransitionSystem
+  source-dirs: src
+
+license: BSD3
+
+name: what4-transition-system
+
+synopsis: Generates transition systems from What4 descriptions
+
+tests:
+  transition-system-tests:
+    dependencies:
+      - what4-transition-system
+    main: TransitionSystemTest.hs
+    source-dirs: test
+
+version: 0.0.1.0

what4-transition-system/src/What4/TransitionSystem.hs

@@ -0,0 +1,339 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE NamedFieldPuns #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE ViewPatterns #-}
+
+-- | TODO
+module What4.TransitionSystem
+  ( CtxState,
+    TransitionSystem (..),
+    createStateStruct,
+    mkAccessors,
+    mySallyNames,
+    -- stateField,
+    transitionSystemToSally,
+    userSymbol',
+  )
+where
+
+import qualified Control.Lens as L
+import Control.Monad.Identity
+import Data.Functor.Const
+import qualified Data.Parameterized.Context as Ctx
+import Data.Parameterized.TraversableFC
+import qualified Language.Sally as S
+import What4.BaseTypes
+import What4.Expr
+import qualified What4.Interface as What4
+import Prelude hiding (init)
+
+userSymbol' :: String -> What4.SolverSymbol
+userSymbol' s = case What4.userSymbol s of
+  Left e -> error $ show e
+  Right symbol -> symbol
+
+-- | @TransitionSystem@ can be used to describe a transition system, which can
+-- then be elaborated into a set of SMT formulas.  We try to have this type
+-- **not** depend on Sally.
+data TransitionSystem sym state = TransitionSystem
+  { -- | representations for the fields of the state type, can be computed
+    -- automatically using @knownRepr@ for a concrete value of @state@
+    stateReprs :: Ctx.Assignment BaseTypeRepr state,
+    -- | names of the field accessor for each state field
+    stateNames :: Ctx.Assignment (Const What4.SolverSymbol) state,
+    -- | initial state predicate
+    initialStatePredicate ::
+      What4.SymStruct sym state ->
+      IO (What4.Pred sym),
+    -- | Binary relations over states for the transition, parameterized by
+    -- the current state and the next state.  Returns a name for each
+    -- transition, and their boolean formula.
+    -- NOTE: it is now important that each transition receives its own,
+    -- fresh copy of the state structs, so that What4 knows not to try and
+    -- share them, and to declare them in each Sally transition.
+    stateTransitions ::
+      What4.SymStruct sym state ->
+      What4.SymStruct sym state ->
+      IO [(S.Name, What4.Pred sym)],
+    queries :: IO [What4.Pred sym]
+  }
+
+data SallyNames = SallyNames
+  { -- | name of the initial state predicate
+    initialName :: S.Name,
+    -- | name of the main transition
+    mainTransitionName :: S.Name,
+    -- | name of the state type
+    stateName :: S.Name,
+    -- | name of the transition system
+    systemName :: S.Name
+  }
+
+-- | @mySallyNames@ has some default names since we currently don't care too
+-- much about changing them
+mySallyNames :: SallyNames
+mySallyNames =
+  SallyNames
+    { initialName = userSymbol' "InitialState",
+      mainTransitionName = userSymbol' "MainTransition",
+      stateName = userSymbol' "State",
+      systemName = userSymbol' "System"
+    }
+
+sallyState ::
+  SallyNames ->
+  TransitionSystem sym stateType ->
+  S.SallyState stateType Ctx.EmptyCtx
+sallyState
+  SallyNames
+    { stateName
+    }
+  TransitionSystem
+    { stateNames,
+      stateReprs
+    } =
+    S.SallyState
+      { S.sallyStateName = stateName,
+        S.sallyStateVars = stateReprs,
+        S.sallyStateVarsNames = stateNames,
+        S.sallyStateInputs = Ctx.Empty,
+        S.sallyStateInputsNames = Ctx.Empty
+      }
+
+-- | Computes a set of side conditions we must add to state formulas to account
+-- for the mismatch between What4 types and sally types.  For instance, a What4
+-- @Nat@ must be translated as a Sally @Int@ (since Sally does not have natural
+-- numbers), with a side condition of positivity.
+sideConditions ::
+  forall t st fs state.
+  ExprBuilder t st fs ->
+  -- | state type
+  Ctx.Assignment BaseTypeRepr state ->
+  -- | state on which to operate
+  What4.SymStruct (ExprBuilder t st fs) state ->
+  IO (S.SallyPred t)
+sideConditions sym stateReprs state =
+  do
+    preds <- concat <$> toListFC getConst <$> Ctx.traverseWithIndex createSideCondition stateReprs
+    What4.andAllOf sym L.folded preds
+  where
+    createSideCondition :: Ctx.Index state bt -> BaseTypeRepr bt -> IO (Const [S.SallyPred t] bt)
+    createSideCondition _index _tp = pure (Const []) -- FIXME
+          -- do
+          --   let zipped = Ctx.zipWith Pair stateReprs accessors
+          --   natConditions <- foldrMFC' addSideCondition [] zipped
+          --   What4.andAllOf sym L.folded natConditions
+          -- where
+          --   addSideCondition ::
+          --     Product BaseTypeRepr (ExprSymFn t (CtxState state)) tp ->
+          --     [S.SallyPred t] ->
+          --     IO [S.SallyPred t]
+          --   addSideCondition p acc = do
+          --     c <- sideCondition p
+          --     return $ c ++ acc
+          --   sideCondition ::
+          --     Product BaseTypeRepr (ExprSymFn t (CtxState state)) tp ->
+          --     IO [S.SallyPred t]
+          --   sideCondition (Pair BaseBoolRepr _) = return []
+          --   sideCondition (Pair BaseNatRepr e) =
+          --     do
+          --       nZ <- What4.natLit sym 0
+          --       natFieldValue <- What4.applySymFn sym e (Ctx.Empty Ctx.:> state)
+          --       (: []) <$> What4.natLe sym nZ natFieldValue
+          --   sideCondition (Pair BaseIntegerRepr _) = return []
+          --   sideCondition (Pair BaseRealRepr _) = return []
+          --   sideCondition (Pair (BaseBVRepr _) _) = return []
+          --   sideCondition (Pair _ _) = error "Not implemented"
+
+createStateStruct ::
+  What4.IsSymExprBuilder sym =>
+  sym ->
+  String ->
+  Ctx.Assignment BaseTypeRepr state ->
+  IO (What4.SymStruct sym state)
+createStateStruct sym namespace stateType =
+  What4.freshConstant sym (userSymbol' namespace) (What4.BaseStructRepr stateType)
+
+-- actually I think it'll be better to have a fresh struct rather than having fields
+-- What4.mkStruct sym =<< freshStateVars sym namespace stateType
+
+sallyInitialState ::
+  ExprBuilder t st fs ->
+  TransitionSystem (ExprBuilder t st fs) state ->
+  IO (S.SallyPred t)
+sallyInitialState
+  sym
+  TransitionSystem
+    { initialStatePredicate,
+      stateReprs
+    } =
+    do
+      init <- createStateStruct sym "init" stateReprs
+      initP <- initialStatePredicate init
+      sideP <- sideConditions sym stateReprs init
+      What4.andPred sym initP sideP
+
+makeSallyTransitions ::
+  ExprBuilder t st fs ->
+  SallyNames ->
+  TransitionSystem (ExprBuilder t st fs) state ->
+  IO [S.SallyTransition t]
+makeSallyTransitions
+  sym
+  ( SallyNames
+      { mainTransitionName,
+        stateName
+      }
+    )
+  ( TransitionSystem
+      { stateReprs,
+        stateTransitions
+      }
+    ) =
+    do
+      state <- createStateStruct sym "state" stateReprs
+      next <- createStateStruct sym "next" stateReprs
+      transitions <- stateTransitions state next
+      allTransitions <- forM transitions $ \(name, transitionP) ->
+        do
+          stateSideP <- sideConditions sym stateReprs state
+          nextSideP <- sideConditions sym stateReprs next
+          transitionRelation <- What4.andAllOf sym L.folded [transitionP, stateSideP, nextSideP]
+          return $
+            S.SallyTransition
+              { S.transitionName = name,
+                S.transitionDomain = stateName,
+                -- traLet = [],
+                S.transitionRelation
+              }
+      -- the main transition is the conjunction of all transitions
+      -- FIXME: turn the name of the transition into an expression
+      transitionsPreds <- forM (S.transitionName <$> allTransitions) $ \transitionName ->
+        What4.freshConstant sym transitionName BaseBoolRepr
+      transitionRelation <- What4.orOneOf sym L.folded transitionsPreds
+      let mainTransition =
+            S.SallyTransition
+              { S.transitionName = mainTransitionName,
+                S.transitionDomain = stateName,
+                -- traLet = [],
+                S.transitionRelation
+              }
+      -- a transition may only refer to previously-defined transitions, so
+      -- @mainTransition@ must be last
+      return (allTransitions ++ [mainTransition])
+
+makeSallyQueries ::
+  S.Name ->
+  [What4.Pred (ExprBuilder t st fs)] ->
+  [S.SallyQuery t]
+makeSallyQueries systemName = map (sallyQuery systemName)
+
+sallyQuery :: S.Name -> What4.Pred (ExprBuilder t st fs) -> S.SallyQuery t
+sallyQuery systemName sallyQueryPredicate =
+  S.SallyQuery
+    { S.sallyQuerySystemName = systemName,
+      -- sqLet = [],
+      S.sallyQueryPredicate,
+      S.sallyQueryComment = ""
+    }
+
+transitionSystemToSally ::
+  ExprBuilder t st fs ->
+  SallyNames ->
+  TransitionSystem (ExprBuilder t st fs) stateType ->
+  IO (S.Sally t stateType Ctx.EmptyCtx Ctx.EmptyCtx)
+transitionSystemToSally
+  sym
+  sn@SallyNames
+    { initialName,
+      mainTransitionName,
+      stateName,
+      systemName
+    }
+  ts@TransitionSystem
+    { queries
+    } =
+    do
+      sallyStateFormulaPredicate <- sallyInitialState sym ts
+      sallyTransitions <- makeSallyTransitions sym sn ts
+      sallyQueries <- makeSallyQueries systemName <$> queries
+      let sallyInitialFormula =
+            S.SallyStateFormula
+              { S.sallyStateFormulaName = initialName,
+                S.sallyStateFormulaDomain = stateName,
+                S.sallyStateFormulaPredicate
+              }
+      let sallySystem =
+            S.SallySystem
+              { S.sallySystemName = systemName,
+                S.sallySystemStateName = stateName,
+                S.sallySystemInitialStateName = initialName,
+                S.sallySystemTransitionName = mainTransitionName
+              }
+      return $
+        S.Sally
+          { S.sallyState = sallyState sn ts,
+            S.sallyFormulas = [],
+            S.sallyConstants = Ctx.Empty,
+            S.sallyInitialFormula,
+            S.sallyTransitions,
+            S.sallySystem,
+            S.sallyQueries
+          }
+
+-- | @mkAccessors@ creates an assignment of function symbols to each state field.  The
+-- name is given by the @Const String@ assignment, the input type is the whole
+-- state type, and the return type is the type of the given field.
+mkAccessors ::
+  What4.IsSymExprBuilder sym =>
+  sym ->
+  Ctx.Assignment BaseTypeRepr state ->
+  Ctx.Assignment (Const What4.SolverSymbol) state ->
+  IO (Ctx.Assignment (What4.SymFn sym (CtxState state)) state)
+mkAccessors sym stateType =
+  Ctx.traverseWithIndex
+    ( \index (Const symbol) ->
+        What4.freshTotalUninterpFn
+          sym
+          symbol
+          (Ctx.Empty Ctx.:> BaseStructRepr stateType)
+          (stateType Ctx.! index)
+    )
+
+-- | @freshStateVars@ instantiates a state type with fresh variables, and
+-- returns the assignment of fields to variables.  This can be used any time a
+-- new state is needed.
+-- freshStateVars ::
+--   What4.IsSymExprBuilder sym =>
+--   sym ->
+--   String ->
+--   -- | state type
+--   Ctx.Assignment BaseTypeRepr state ->
+--   IO (Ctx.Assignment (SymExpr sym) state)
+-- freshStateVars sym name ctx =
+--   Ctx.traverseWithIndex (\ ndx -> What4.freshConstant sym (userSymbol' (name ++ "_" ++ show (Ctx.indexVal ndx)))) ctx
+
+-- | A context with just one field, a struct type for the state
+type CtxState state = Ctx.EmptyCtx Ctx.::> BaseStructType state
+
+-- stateField ::
+--   What4.IsSymExprBuilder sym =>
+--   sym ->
+--   -- Ctx.Assignment (What4.SymFn sym (CtxState state)) state ->
+--   -- L.Lens' (Ctx.Assignment (What4.SymFn sym (CtxState state)) state) (What4.SymFn sym (CtxState state) ret) ->
+--   Ctx.Index state ret ->
+--   What4.SymStruct sym state ->
+--   IO (SymExpr sym ret)
+-- stateField sym state index =
+--   What4.structField sym state index
+--   -- What4.applySymFn sym (L.view field fields) (Ctx.Empty Ctx.:> state)

what4-transition-system/test/TransitionSystemTest.hs

@@ -0,0 +1,245 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+-- |
+-- Module      : TransitionSystemTest
+-- Copyright   : (c) Galois Inc, 2020
+-- License     : BSD3
+-- Maintainer  : valentin.robert.42@gmail.com
+-- |
+module Main where
+
+import qualified Control.Lens as L
+import Control.Monad (join)
+import qualified Data.Parameterized.Context as Ctx
+import Data.Parameterized.Nonce
+-- import Data.Parameterized.Some
+-- import Data.Parameterized.TraversableFC
+-- import qualified Data.Set as Set
+-- import Data.Text (Text)
+-- import qualified Data.Text.Lazy as Lazy
+-- import qualified Data.Text.Lazy.Builder as Builder
+import Language.Sally
+import Language.Sally.Writer
+import qualified System.IO.Streams as Streams
+-- import qualified Text.PrettyPrint.ANSI.Leijen as PP
+import What4.BaseTypes
+import What4.Expr
+import What4.Expr.Builder
+import qualified What4.Interface as What4
+-- import What4.ProblemFeatures
+-- import What4.Protocol.SMTLib2 hiding (newWriter)
+-- import What4.Protocol.SMTLib2.Syntax as SMT2
+import What4.Protocol.SMTWriter as SMTWriter
+import What4.Solver.Adapter
+import What4.TransitionSystem
+import Prelude hiding (init)
+
+showBinding :: SymbolBinding t -> String
+showBinding (VarSymbolBinding x) = show x
+showBinding (FnSymbolBinding x) = show x
+
+displayTransitionSystem ::
+  sym ~ ExprBuilder t st fs =>
+  sym ->
+  TransitionSystem sym stateFields ->
+  IO ()
+displayTransitionSystem sym transitionSystem =
+  do
+    sts <- transitionSystemToSally sym mySallyNames transitionSystem
+    sexp <- sexpOfTrResult sym sts
+    print . sxPretty $ sexp
+
+main :: IO ()
+main =
+  do
+    withIONonceGenerator $ \nonceGen -> do
+      sym <- newExprBuilder FloatIEEERepr State nonceGen
+      ts <- counterTransitionSystem sym
+      displayTransitionSystem sym ts
+    withIONonceGenerator $ \nonceGen -> do
+      sym <- newExprBuilder FloatIEEERepr State nonceGen
+      ts <- realsTransitionSystem sym
+      displayTransitionSystem sym ts
+
+-- We don't need any information in the state
+data State t = State
+
+makeFieldNames ::
+  forall stateType.
+  [What4.SolverSymbol] ->
+  Ctx.Assignment BaseTypeRepr stateType ->
+  Ctx.Assignment (L.Const What4.SolverSymbol) stateType
+makeFieldNames fields rep = Ctx.generate (Ctx.size rep) generator
+  where
+    generator :: Ctx.Index stateType tp -> L.Const What4.SolverSymbol tp
+    generator index = L.Const (fields !! (Ctx.indexVal index))
+
+--
+-- Example 1: a simple counter
+--
+type CounterStateType = Ctx.EmptyCtx Ctx.::> BaseBoolType Ctx.::> BaseNatType
+
+counterStateFields :: [What4.SolverSymbol]
+counterStateFields = userSymbol' <$> ["counterIsEven", "counter"]
+
+counterFieldNames :: Ctx.Assignment (L.Const What4.SolverSymbol) CounterStateType
+counterFieldNames = makeFieldNames counterStateFields knownRepr
+
+counterIsEven :: Ctx.Index CounterStateType BaseBoolType
+counterIsEven = Ctx.natIndex @0
+
+counter :: Ctx.Index CounterStateType BaseNatType
+counter = Ctx.natIndex @1
+
+-- | Example initial state predicate, this one constrains the `bool` field to be
+-- true, and the `nat` field to be equal to zero
+counterInitial ::
+  What4.IsSymExprBuilder sym =>
+  sym ->
+  -- | mapping to a variable for each state field
+  What4.SymStruct sym CounterStateType ->
+  IO (What4.Pred sym)
+counterInitial sym init =
+  do
+    initCounterIsEven <- What4.structField sym init counterIsEven
+    initCounter <- What4.structField sym init counter
+    nZero <- What4.natLit sym 0
+    natCond <- What4.natEq sym initCounter nZero
+    andCond <- What4.andPred sym initCounterIsEven natCond
+    return andCond
+
+-- | Example state transition, here, during a transition, the boolean gets
+-- negated, and the natural number gets incremented.  One property of such a
+-- system would be that when the boolean is false, the number is even (assuming
+-- a false and zero initial state).
+counterTransitions ::
+  What4.IsSymExprBuilder sym =>
+  sym ->
+  -- | current state
+  What4.SymStruct sym CounterStateType ->
+  -- | next state
+  What4.SymStruct sym CounterStateType ->
+  IO [(String, What4.Pred sym)]
+counterTransitions sym state next =
+  do
+    stateCounterIsEven <- What4.structField sym state counterIsEven
+    stateCounter <- What4.structField sym state counter
+    nextCounterIsEven <- What4.structField sym next counterIsEven
+    nextCounter <- What4.structField sym next counter
+    -- (= next.counter (+ 1 state.counter))
+    nOne <- What4.natLit sym 1
+    nStatePlusOne <- What4.natAdd sym nOne stateCounter
+    natCond <- What4.natEq sym nextCounter nStatePlusOne
+    -- (= next.counterIsEven (not state.counterIsEven))
+    bStateNeg <- What4.notPred sym stateCounterIsEven
+    boolCond <- What4.eqPred sym nextCounterIsEven bStateNeg
+    andCond <- What4.andPred sym boolCond natCond
+    return [("CounterTransition", andCond)]
+
+-- | TODO
+counterTransitionSystem ::
+  ExprBuilder t st fs ->
+  IO (TransitionSystem (ExprBuilder t st fs) CounterStateType)
+counterTransitionSystem sym =
+  do
+    return $
+      TransitionSystem
+        { stateFieldsRepr = knownRepr,
+          stateFieldsNames = counterFieldNames,
+          initialStatePred = counterInitial sym,
+          stateTransitions = counterTransitions sym,
+          queries = pure []
+        }
+
+--
+-- Example 2: using real numbers
+--
+
+-- based on sally/test/regress/bmc/nra/algebraic.mcmt
+
+type RealsStateType =
+  Ctx.EmptyCtx
+    Ctx.::> BaseRealType
+    Ctx.::> BaseRealType
+    Ctx.::> BaseRealType
+
+realsStateFields :: [What4.SolverSymbol]
+realsStateFields = userSymbol' <$> ["P", "x", "n"]
+
+realsFieldNames :: Ctx.Assignment (L.Const What4.SolverSymbol) RealsStateType
+realsFieldNames = makeFieldNames realsStateFields knownRepr
+
+pReals :: Ctx.Index RealsStateType BaseRealType
+pReals = Ctx.natIndex @0
+
+xReals :: Ctx.Index RealsStateType BaseRealType
+xReals = Ctx.natIndex @1
+
+nReals :: Ctx.Index RealsStateType BaseRealType
+nReals = Ctx.natIndex @2
+
+realsInitial ::
+  What4.IsSymExprBuilder sym =>
+  sym ->
+  -- | mapping to a variable for each state field
+  What4.SymStruct sym RealsStateType ->
+  IO (What4.Pred sym)
+realsInitial sym init =
+  do
+    pInit <- What4.structField sym init pReals
+    nInit <- What4.structField sym init nReals
+    -- (and (= P 1) (= n 0))
+    join
+      ( What4.andPred sym
+          <$> (What4.realEq sym pInit =<< What4.realLit sym 1)
+          <*> (What4.realEq sym nInit =<< What4.realLit sym 0)
+      )
+
+realsTransitions ::
+  What4.IsSymExprBuilder sym =>
+  sym ->
+  -- | current state
+  What4.SymStruct sym RealsStateType ->
+  -- | next state
+  What4.SymStruct sym RealsStateType ->
+  IO [(String, What4.Pred sym)]
+realsTransitions sym state next =
+  do
+    pState <- What4.structField sym state pReals
+    xState <- What4.structField sym state xReals
+    nState <- What4.structField sym state nReals
+    pNext <- What4.structField sym next pReals
+    xNext <- What4.structField sym next xReals
+    nNext <- What4.structField sym next nReals
+    -- (= next.P (* state.P state.x)
+    c1 <- join $ What4.realEq sym pNext <$> What4.realMul sym pState xState
+    -- (= next.n (+ state.n 1))
+    c2 <- join $ What4.realEq sym nNext <$> (What4.realAdd sym nState =<< What4.realLit sym 1)
+    -- (= next.x state.x)
+    c3 <- What4.realEq sym xNext xState
+    t <- What4.andPred sym c1 =<< What4.andPred sym c2 c3
+    return [("RealsTransition", t)]
+
+-- | TODO
+realsTransitionSystem ::
+  ExprBuilder t st fs ->
+  IO (TransitionSystem (ExprBuilder t st fs) RealsStateType)
+realsTransitionSystem sym =
+  do
+    return $
+      TransitionSystem
+        { stateFieldsRepr = knownRepr,
+          stateFieldsNames = realsFieldNames,
+          initialStatePred = realsInitial sym,
+          stateTransitions = realsTransitions sym,
+          queries = pure []
+        }

what4-transition-system/what4-transition-system.cabal

@@ -0,0 +1,62 @@
+cabal-version: 1.12
+
+-- This file has been generated from package.yaml by hpack version 0.33.0.
+--
+-- see: https://github.com/sol/hpack
+--
+-- hash: d51f186fc63bb5e8b1476af71e4f661d2ca4f5df1f64d4686a18e2ad6351f6c4
+
+name:           what4-transition-system
+version:        0.0.1.0
+synopsis:       Generates transition systems from What4 descriptions
+description:    Generates transition systems from What4 descriptions
+author:         Valentin Robert <valentin.robert.42@gmail.com>
+maintainer:     Valentin Robert <valentin.robert.42@gmail.com>
+copyright:      Galois, Inc. 2020
+license:        ISC
+build-type:     Simple
+
+library
+  exposed-modules:
+      What4.TransitionSystem
+  other-modules:
+      Paths_what4_transition_system
+  hs-source-dirs:
+      src
+  ghc-options: -Wall -Werror=incomplete-patterns -Werror=missing-methods -Werror=overlapping-patterns
+  build-depends:
+      ansi-wl-pprint >=0.6 && <0.7
+    , base >=4.13 && <4.14
+    , bytestring
+    , containers >=0.6 && <0.7
+    , io-streams
+    , language-sally >=0.2 && <0.3
+    , lens
+    , mtl
+    , parameterized-utils >=2.0 && <2.1
+    , text
+    , what4
+  default-language: Haskell2010
+
+test-suite transition-system-tests
+  type: exitcode-stdio-1.0
+  main-is: TransitionSystemTest.hs
+  other-modules:
+      Paths_what4_transition_system
+  hs-source-dirs:
+      test
+  ghc-options: -Wall -Werror=incomplete-patterns -Werror=missing-methods -Werror=overlapping-patterns
+  build-depends:
+      ansi-wl-pprint >=0.6 && <0.7
+    , base >=4.13 && <4.14
+    , bytestring
+    , containers >=0.6 && <0.7
+    , io-streams
+    , language-sally >=0.2 && <0.3
+    , lens
+    , mtl
+    , parameterized-utils >=2.0 && <2.1
+    , text
+    , what4
+    , what4-transition-system
+  default-language: Haskell2010