[WIP] add finite field support

.circleci/config.yml

@@ -27,7 +27,7 @@ commands:
       - checkout
       - add_ssh_keys
       - run: git submodule sync
-      - run: git submodule update --init
+      - run: git submodule update --init --remote
 
   cabal_build_and_test:
     description: "Build the project and run the tests"

.gitmodules

@@ -1,3 +1,4 @@
 [submodule "liquid-fixpoint"]
 	path = liquid-fixpoint
-	url = https://github.com/ucsd-progsys/liquid-fixpoint.git
+	url = https://github.com/clayrat/liquid-fixpoint.git
+	branch = finfield

liquid-prelude/liquid-prelude.cabal

@@ -25,6 +25,7 @@ library
                     Language.Haskell.Liquid.Equational
                     Language.Haskell.Liquid.Bag
                     Language.Haskell.Liquid.ProofCombinators
+                    Language.Haskell.Liquid.FinField
   hs-source-dirs:     src
   build-depends:      base          < 5
                     , ghc-prim

liquid-prelude/src/Language/Haskell/Liquid/FinField.hs

@@ -0,0 +1,32 @@
+{-# OPTIONS_GHC -fplugin=LiquidHaskell #-}
+{-# LANGUAGE KindSignatures, DataKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module Language.Haskell.Liquid.FinField where
+
+import Data.Proxy
+import GHC.TypeLits
+import Language.Haskell.Liquid.Prelude
+
+data FFld (o :: Nat) = FFld { ffToInteger :: Integer } deriving Eq
+{-@ embed FFld as FFld_t @-}
+
+{-@ assume val :: forall o. KnownNat o => o : Nat -> n : Integer -> {v:FFld o | v = FF_val n} @-}
+{-@ define val                            o          n                           = (FF_val n) @-}
+val :: Int -> Integer -> FFld o
+val _ n = FFld n
+
+{-@ assume add :: forall o. KnownNat o => x : FFld o -> y : FFld o -> {v:FFld o | v = FF_add x y} @-}
+{-@ define add                            x             y                          = (FF_add x y) @-}
+add :: forall o. KnownNat o => FFld o -> FFld o -> FFld o
+add x y =
+  FFld (ffToInteger x + ffToInteger y `mod` liquidAssume (n /= 0) n)
+  where
+  n = natVal (Proxy :: Proxy o)
+
+{-@ assume mul :: forall o. KnownNat o => x : FFld o -> y : FFld o -> {v:FFld o | v = FF_mul x y} @-}
+{-@ define mul                            x             y                          = (FF_mul x y) @-}
+mul :: forall o. KnownNat o => FFld o -> FFld o -> FFld o
+mul x y = FFld (ffToInteger x * ffToInteger y `mod` liquidAssume (n /= 0) n)
+  where
+  n = natVal (Proxy :: Proxy o)

liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Elaborate.hs

@@ -556,6 +556,7 @@ renameBinderSort f = rename
   rename F.FInt             = F.FInt
   rename F.FReal            = F.FReal
   rename F.FNum             = F.FNum
+  rename (F.FNatNum n)      = F.FNatNum n
   rename F.FFrac            = F.FFrac
   rename (   F.FObj s     ) = F.FObj (f s)
   rename t'@(F.FVar _     ) = t'

liquidhaskell-boot/src/Language/Haskell/Liquid/WiredIn.hs

@@ -95,7 +95,7 @@ wiredTheorySortedSyms =
     | s <- wiredTheorySyms
     , let srt = F.tsSort $
                   fromMaybe (panic Nothing ("unknown symbol: " ++ show s)) $
-                    F.lookupSEnv s (F.theorySymbols F.Z3)
+                    F.lookupSEnv s (F.theorySymbols F.Z3 <> F.theorySymbols F.Cvc5)
     ]
   where
     wiredTheorySyms =
@@ -122,6 +122,10 @@ wiredTheorySortedSyms =
       , "Bag_union"
       , "Bag_union_max"
 
+      , "FF_val"
+      , "FF_add"
+      , "FF_mul"
+
       , "strLen"
       ]