packages feed

liquid-finfield (empty) → 0.9.12.2.1

raw patch · 4 files changed

+87/−0 lines, 4 filesdep +basedep +liquidhaskell

Dependencies added: base, liquidhaskell

Files

+ LICENSE view
@@ -0,0 +1,30 @@+Copyright (c) 2013-2014, Ranjit Jhala++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 Ranjit Jhala nor the names of other+      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.
+ liquid-finfield.cabal view
@@ -0,0 +1,21 @@+cabal-version:      1.24+name:               liquid-finfield+version:            0.9.12.2.1+synopsis:           Finite field utilities for LiquidHaskell (requires cvc5)+description:        Finite field utilities for LiquidHaskell (requires cvc5)+license:            BSD3+license-file:       LICENSE+copyright:          2010-19 Ranjit Jhala & Niki Vazou & Eric L. Seidel, University of California, San Diego.+author:             Alex Gryzlov, Niki Vazou+maintainer:         Ranjit Jhala <jhala@cs.ucsd.edu>+category:           Language+homepage:           https://github.com/ucsd-progsys/liquidhaskell+build-type:         Simple++library+  exposed-modules:  Language.Haskell.Liquid.FinField+                    Language.Haskell.Liquid.FinField.FF17+  hs-source-dirs:     src+  build-depends:      base          < 5+                    , liquidhaskell        >= 0.9.12.2.1+  default-language:   Haskell2010
+ src/Language/Haskell/Liquid/FinField.hs view
@@ -0,0 +1,10 @@+{-# OPTIONS_GHC -fplugin=LiquidHaskell #-}+{-# LANGUAGE KindSignatures, DataKinds #-}++module Language.Haskell.Liquid.FinField where++import GHC.TypeLits++newtype FFld (o :: Nat) = FFld { ffToInteger :: Integer } deriving Eq++-- see /tests/pos/FF17.hs and /tests/pos/FF2131.hs for usage examples
+ src/Language/Haskell/Liquid/FinField/FF17.hs view
@@ -0,0 +1,26 @@+{-# LANGUAGE DataKinds #-}+{-# OPTIONS_GHC -fplugin=LiquidHaskell #-}+{-@ LIQUID "--smtsolver=cvc5"  @-}++module Language.Haskell.Liquid.FinField.FF17 where++import Language.Haskell.Liquid.FinField++-- instantiate FFld for a specific prime value of 17+data FF17 = FF17 { toFFld :: FFld 17 }+{-@ embed FF17 as (FFld_t 17) @-}++{-@ assume val :: n : Integer -> {v:FF17 | v = FF_val n} @-}+{-@ define val    n                          = (FF_val n) @-}+val :: Integer -> FF17+val n = FF17 (FFld (n `mod` 17))++{-@ assume add :: x : FF17 -> y : FF17 -> {v:FF17 | v = FF_add x y} @-}+{-@ define add    x           y                      = (FF_add x y) @-}+add :: FF17 -> FF17 -> FF17+add x y = FF17 (FFld (ffToInteger (toFFld x) + ffToInteger (toFFld y) `mod` 17))++{-@ assume mul :: x : FF17 -> y : FF17 -> {v:FF17 | v = FF_mul x y} @-}+{-@ define mul    x           y                      = (FF_mul x y) @-}+mul :: FF17 -> FF17 -> FF17+mul x y = FF17 (FFld (ffToInteger (toFFld x) * ffToInteger (toFFld y) `mod` 17))