diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml new file mode 100644 --- /dev/null +++ b/.github/workflows/ci.yml @@ -0,0 +1,97 @@ +name: CI + +on: + push: + branches: + - master + pull_request: + types: + - opened + - synchronize + +jobs: + build-test-ubuntu-stack: + runs-on: ubuntu-latest + name: Ubuntu / Stack + steps: + - uses: actions/checkout@v2 + + # relative paths are relative to the project directory + - name: Cache Stack build artifacts (user + project) + uses: actions/cache@v4 + with: + path: | + ~/.stack + .stack-work + # best effort for cache: tie it to Stack resolver and package config + key: ${{ runner.os }}-stack-${{ hashFiles('stack.yaml.lock', 'package.yaml') }} + restore-keys: | + ${{ runner.os }}-stack + + - name: Install project dependencies + run: stack --no-terminal test --only-dependencies + + - name: Build and run tests + run: stack --no-terminal haddock --test --no-haddock-deps + + build-test-ubuntu-cabal: + runs-on: ubuntu-latest + name: Ubuntu / GHC ${{ matrix.ghc }}, Cabal ${{ matrix.cabal }} + strategy: + fail-fast: false # don't stop if one job (= GHC version) fails + matrix: + cabal: ["3.4"] # latest as of 2021-06-16 + ghc: + - "8.6.5" + - "9.2.4" + - "9.4.2" + env: + # note that all flags must be passed to every command even when + # irrelevant, else Cabal will trigger arbitrary rebuilds + CABAL_FLAGS: --enable-tests --enable-benchmarks --test-show-details=streaming + steps: + + # TODO: GHC decides to recompile based on timestamp, so cache isn't used + # Preferably GHC would work via hashes instead. Stack had this feature + # merged in Aug 2020. + # Upstream GHC issue: https://gitlab.haskell.org/ghc/ghc/-/issues/16495 + # My issue on haskell/actions: https://github.com/haskell/actions/issues/41 + # This also requires us to do a deep fetch, else we don't get the Git commit + # history we need to rewrite mod times. + - uses: actions/checkout@v2 + with: + fetch-depth: 0 + - name: Set all tracked file modification times to the time of their last commit + run: | + rev=HEAD + for f in $(git ls-tree -r -t --full-name --name-only "$rev") ; do + touch -d $(git log --pretty=format:%cI -1 "$rev" -- "$f") "$f"; + done + + - name: Setup Haskell build environment + id: setup-haskell-build-env + uses: haskell/actions/setup@v1 + with: + ghc-version: ${{ matrix.ghc }} + cabal-version: ${{ matrix.cabal }} + + - name: Freeze Cabal plan + run: cabal freeze + + - name: Cache Cabal build artifacts + uses: actions/cache@v4 + with: + path: | + ${{ steps.setup-haskell-build-env.outputs.cabal-store }} + dist-newstyle + key: ${{ runner.os }}-cabal-${{ matrix.ghc }}-${{ hashFiles('cabal.project.freeze') }} + restore-keys: | + ${{ runner.os }}-cabal-${{ matrix.ghc }} + + - name: Build + run: cabal build + + - name: Test + run: cabal test --test-show-details=streaming + env: + HSPEC_OPTIONS: --color diff --git a/.gitignore b/.gitignore new file mode 100644 --- /dev/null +++ b/.gitignore @@ -0,0 +1,5 @@ +/.stack-work +/dist-newstyle +/cabal.project.freeze + +.DS_Store diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,3 +1,7 @@ +## 0.6.3 (23 Sep 2025) +* Stack builds using LTS-24.2 +* Cabal builds under GHC 9.0 thru 9.12 + ## 0.6.2 (16 Jun 2021) * Support GHC 9.0 diff --git a/Language/Expression/Lambda.hs b/Language/Expression/Lambda.hs new file mode 100644 --- /dev/null +++ b/Language/Expression/Lambda.hs @@ -0,0 +1,87 @@ +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE NoMonomorphismRestriction #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeOperators #-} + +module Language.Expression.Lambda where + +import Data.Semigroup (Max (..)) + +import Data.Typeable ((:~:) (..), Typeable, eqT) + +import Control.Lens + +import Language.Expression +import Language.Expression.Scope + +data LambdaOp s t a where + App :: t (a -> b) -> t a -> LambdaOp s t b + + -- | Abstracts a scope where bound variables are in the @(':~:') a@ functor, + -- meaning they have the same type as @a@. Free variables ignore the argument + -- and have type @b@. + Abs :: s ((:~:) a) b -> LambdaOp s t (a -> b) + +instance HDuofunctor LambdaOp where + hduomap = defaultHduomap + +instance HDuotraversable LambdaOp where + hduotraverse f g = \case + App x y -> App <$> g x <*> g y + Abs x -> Abs <$> f pure x + +instance HFunctor (LambdaOp s) where + hmap f = \case + App x y -> App (f x) (f y) + Abs x -> Abs x + +instance (HTraversable s) => HTraversable (LambdaOp s) where + htraverse = hduotraverseSecond + +instance HDuofoldableAt Identity LambdaOp where + hduofoldMapAt f = \case + App (Identity g) (Identity x) -> Identity (g x) + Abs y -> Identity (\x -> runIdentity (f (\Refl -> Identity x) y)) + + +type LambdaExpr = SFree LambdaOp + +-- var :: v a -> LambdaExpr + +app :: LambdaExpr v (a -> b) -> LambdaExpr v a -> LambdaExpr v b +app f x = SWrap (App f x) + +-- newtype Scope g h f a = Scope { unscope :: h (BV g (h f)) a } + +lam' :: Scope ((:~:) a) LambdaExpr v b -> LambdaExpr v (a -> b) +lam' = SWrap . Abs . Scoped + + +data TVar k a where + TVar :: Typeable a => { tvarKey :: k } -> TVar k a + + +uniqueTVarKey :: (HTraversable h, Ord k, Bounded k, Enum k) => h (TVar k) a -> k +uniqueTVarKey x = + let Max highestUsed = hfoldMap (Max . tvarKey) x + in succ highestUsed + + +abstractTVar :: (HMonad h, Typeable a, Eq k) => k -> h (TVar k) b -> Scope ((:~:) a) h (TVar k) b +abstractTVar nm = abstract (\case TVar nm' | nm == nm' -> eqT + _ -> Nothing) + +-- abstractTVar' +-- :: (HMonad h, HTraversable h, Typeable a, Ord k, Bounded k, Enum k, Typeable b) +-- => h (TVar k) b -> Scope ((:~:) a) h (TVar k) b +-- abstractTVar' x = abstractTVar (uniqueTVarKey x) x + +-- -- | "Wow! This works?" +-- lam :: (Ord k, Bounded k, Enum k, Typeable a, Typeable b) => (LambdaExpr (TVar k) a -> LambdaExpr (TVar k) b) -> LambdaExpr (TVar k) (a -> b) +-- lam f = +-- let k = uniqueTVarKey +-- -- lam' $ abstractTVar' $ f _ diff --git a/Language/Verification/Continuity.hs b/Language/Verification/Continuity.hs new file mode 100644 --- /dev/null +++ b/Language/Verification/Continuity.hs @@ -0,0 +1,75 @@ +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DeriveTraversable #-} +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiParamTypeClasses #-} + +module Language.While.Continuity where + +import Data.SBV + +import Data.Set (Set) +import qualified Data.Set as Set + +import Language.While.Hoare +import Language.While.Syntax + +import Language.Expression + + + + +-- data OpSpec = +-- OpSpec +-- { _osPrecondition :: Prop Int +-- , _osOpContinuity :: Set Int +-- } +-- deriving (Show) + + +-- exprOpSpecs :: ExprOp a -> [OpSpec] +-- exprOpSpecs = \case +-- OAdd _ _ -> [OpSpec (PLit True) (Set.fromList [0, 1])] +-- OMul _ _ -> [OpSpec (PLit True) (Set.fromList [0, 1])] +-- OSub _ _ -> [OpSpec (PLit True) (Set.fromList [0, 1])] + + +-- -- | @'exprContinuous' allVars prop inputs expr@ judges whether @expr@ is +-- -- continuous with respect to the given input variables, whenever the current +-- -- program state is one in which @prop@ is true. @allVars@ constrains the +-- -- variables in the program. +-- exprContinuous :: (Ord l) => Set l -> WhileProp l -> Set l -> Expr l -> Bool +-- exprContinuous = undefined + + +-- newtype SetVar = SetVar Int + + +-- data SetExpr l v +-- = SVar v +-- | SLit (Set l) +-- | SUnion (SetExpr l v) (SetExpr l v) +-- | SDiff + + +-- data SetProp l v +-- = Subset (SetExpr l v) (SetExpr l v) + + +-- class Monad m => MonadProveCont l m | m -> l where +-- -- Fresh variables +-- -- Adding proof obligations +-- -- Discharging some of the existing proof obligations +-- -- Querying state + +-- -- | @'findContinuity' prop inputs command@ yields the largest set of output +-- -- variables such that the outputs vary continuously in the inputs when +-- -- @command@ from a state which satisfies @prop@. +-- findContinuity :: (MonadProveCont l m) => Prop l -> Set l -> Command l a -> m (Set l) +-- findContinuity prop inputs command = undefined + +-- -- | @'continuityVcs' subspace inputs outputs command@ computes the verification +-- -- conditions for each of the variables in @outputs@ to vary continuously with +-- -- respect to each of the variables in @inputs@, after running @command@. +-- continuityVcs :: Prop l -> [l] -> [l] -> Command l a -> SBool +-- continuityVcs prop inputs outputs = undefined diff --git a/Language/Verification/Core.hs b/Language/Verification/Core.hs --- a/Language/Verification/Core.hs +++ b/Language/Verification/Core.hs @@ -25,6 +25,7 @@ import Data.Functor.Compose import Control.Lens hiding ((.>)) +import Control.Monad ((<=<)) import Control.Monad.Except import Control.Monad.Reader import Control.Monad.State diff --git a/Language/While/Hoare.hs b/Language/While/Hoare.hs --- a/Language/While/Hoare.hs +++ b/Language/While/Hoare.hs @@ -9,6 +9,7 @@ module Language.While.Hoare where +import Control.Monad (void, mzero) import Control.Monad.Writer import Language.While.Syntax diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,6 @@ +# Verifiable Expressions + +Intermediate language for Hoare Logic style verification and useful combinators. + +Please see +[Language.Expression.Example](https://github.com/camfort/verifiable-expressions/blob/master/Language/Expression/Example.hs) for how to use this library. diff --git a/notes.org b/notes.org new file mode 100644 --- /dev/null +++ b/notes.org @@ -0,0 +1,72 @@ +#+TITLE: Chaudhuri vs Fuzz + +Notes on the suitability of the Chaudhuri and Fuzz methods of sensitivity analysis for application to Fortran. + +* Chaudhuri + +** Papers + +|------------+----------------------| +| Continuity | Chaudhuri et al 2010 | +| Robustness | Chaudhuri et al 2011 | + +** Notes + +This method determines K-sensitivity (called robustness in the paper) in two steps: +- Prove continuity +- Prove piecewise K-linearity + +Due to a theorem in the paper, these together imply K-robustness. + +Continuity is proved using a complex abstract interpretation method which requires discharging many complex proofs through external solvers (which may or may not currently exist...). + +Piecewise K-linearity is proved using a simple abstract interpretation method. + +** Major Challenges +*** Program Equivalence + +Godlin and Strichman 2009 + +*** Hoare Triple Verification + +** Limitations + +- Minimal sensitivity can't be inferred, only verified. +- Considers only terminating programs with a priori bounds on the number of loop iterations +- Proof obligations are not always automatically solvable + + +* Fuzz + +** Papers + +|-----------------------------------------------------------------+-------------------------------------------------------------------------------------------| +| Original Fuzz Paper | Reed and Pierce 2010 | +| Description of an efficient type/sensitivity analysis algorithm | Type-based Sensitivity Analysis, D'Antoni and Gaboardi and Arias and Haeberlen and Pierce | +| Category-theoretical formalisation | Gaboardi et al 2017 | + +** Notes + +Fuzz is a programming language which encodes program sensitivity at the type level. Types and therefore sensitivity can be inferred using the algorithm by Gaboardi et al. Some user annotation may be required. + +Fuzz is purely functional, and resembles PCF. Its type system is linear, where linear means something slightly different to the standard interpretation of linear logic. If a function argument ~x~ has grade ~k~, then the output of the function may not change more than ~k~ times faster than ~x~. Infinite grades are required to encode discontinuous or non-robust functions (i.e. the exponential function is continuous but non-robust because its rate of change cannot be bounded by any constant). + +** Major Challenges + +*** Converting Fortran to Fuzz + +- Fuzz is purely functional with linear types! +- For Fortran that doesn't have side-effects and doesn't access arrays, convert it to SSA and the translation to a pure functional language should follow. +- We might be able to only handle pure code and still have a useful analysis. +- Array access with ~forall~ should be fine to handle. Arbitrary indexing could be much more difficult. + +*** Arrays + +- We might be able to model arrays as lists, as some versions of Fuzz support μ-types +- Alternatively add arrays as a native data type in our version of Fuzz, and figure out how to extend type-checking +- Mutable access will be more difficult to encode. Create a fresh version of the array for each mutation? + +** Limitations + +- Might not be able to handle conditional branching (a more refined type system might help, see Gaboardi et al 2013) +- No ability to reason about sensitivity dependent on size of input (e.g. arrays) diff --git a/package.yaml b/package.yaml new file mode 100644 --- /dev/null +++ b/package.yaml @@ -0,0 +1,52 @@ +name: verifiable-expressions +version: '0.6.3' +category: Language +author: Bradley Hardy +maintainer: madgenhetic@gmail.com +github: camfort/verifiable-expressions +license: Apache-2.0 +synopsis: An intermediate language for Hoare logic style verification. +description: + A typed intermediate language for Hoare logic style verification. It defines + the intermediate language and combinators to interact it. +tested-with: GHC == 9.0, GHC == 9.2, GHC == 9.4, GHC == 9.6, GHC == 9.8, GHC == 9.10, GHC == 9.12 + +extra-source-files: +- CHANGELOG.md + +dependencies: +- base >=4.9 && <5 +- containers >=0.5.7 && <0.7 +- transformers >=0.5 && <0.7 +- mtl >=2.0 && <3 +- lens >=4.16.1 && <5.5 +- union >=0.1.2 && <0.2 +- vinyl >=0.14.3 && <0.15 + +when: +- condition: impl(ghc >= 9.6) + dependencies: + - sbv >=10.0 && <11 +- condition: impl(ghc < 9.6) + dependencies: + - sbv >=8.0 && <10 + +library: + ghc-options: -Wall + exposed-modules: + - Language.Expression + - Language.Expression.Example + - Language.Expression.Choice + - Language.Expression.Scope + - Language.Expression.GeneralOp + - Language.Expression.Prop + - Language.Expression.Pretty + - Language.Expression.Util + - Language.Verification + - Language.Verification.Conditions + - Language.Verification.Core + - Language.While.Hoare + - Language.While.Hoare.Prover + - Language.While.Syntax + - Language.While.Syntax.Sugar + - Language.While.Test diff --git a/stack.yaml b/stack.yaml new file mode 100644 --- /dev/null +++ b/stack.yaml @@ -0,0 +1,13 @@ +resolver: lts-24.2 +packages: +- '.' + +flags: {} +extra-package-dbs: [] + +extra-deps: + - union-0.1.2@dd8da96d3d15c71a75d648377e6b55bd2614010db80f8cf4bda5b49a8a9684af + - sbv-10.12 + - containers-0.6.8@sha256:bb2bec1bbc6b39a7c97cd95e056a5698ec45beb5d8feb6caae12af64e4bd823c,2670 + - binary-0.8.9.3@sha256:8b03c7fd5a7f6803280fba87e38d534beb1dc92fec975de5bd36200633996ef2,6576 + - text-2.1.3@sha256:1907e0f6914e376df3a3a1fbc5a04e49c729d333de34babba4da30075048c60f,11185 diff --git a/stack.yaml.lock b/stack.yaml.lock new file mode 100644 --- /dev/null +++ b/stack.yaml.lock @@ -0,0 +1,47 @@ +# This file was autogenerated by Stack. +# You should not edit this file by hand. +# For more information, please see the documentation at: +# https://docs.haskellstack.org/en/stable/topics/lock_files + +packages: +- completed: + hackage: union-0.1.2@sha256:04e5fe3a3a2b1235cf5d2fc193e6d6d2624ee762d7b2145fce975afbc8c40686,2134 + pantry-tree: + sha256: 4b313bcf19a558f0e2f915aa4b37c22623db89ae34d5441d1041fff4a148d2cd + size: 330 + original: + hackage: union-0.1.2 +- completed: + hackage: sbv-10.12@sha256:b4642dfef053e15ad3628ea517298ba4afd6f3f994bd0d6021ea6e647bf49383,24547 + pantry-tree: + sha256: 1d061bfb8d77ee81316c05e0091b0cb3982946b7ea2b8f32d814256a762eb774 + size: 72702 + original: + hackage: sbv-10.12 +- completed: + hackage: containers-0.6.8@sha256:bb2bec1bbc6b39a7c97cd95e056a5698ec45beb5d8feb6caae12af64e4bd823c,2670 + pantry-tree: + sha256: 62d0b7f21a9f298867bbf0acae201d1fe4e32d309b4085a52c037eb551852811 + size: 2954 + original: + hackage: containers-0.6.8@sha256:bb2bec1bbc6b39a7c97cd95e056a5698ec45beb5d8feb6caae12af64e4bd823c,2670 +- completed: + hackage: binary-0.8.9.3@sha256:8b03c7fd5a7f6803280fba87e38d534beb1dc92fec975de5bd36200633996ef2,6576 + pantry-tree: + sha256: 32834cef5d28bfbe4ba230c12bdae4363a30911f898df9e6d5074fbbabcd549a + size: 1976 + original: + hackage: binary-0.8.9.3@sha256:8b03c7fd5a7f6803280fba87e38d534beb1dc92fec975de5bd36200633996ef2,6576 +- completed: + hackage: text-2.1.3@sha256:1907e0f6914e376df3a3a1fbc5a04e49c729d333de34babba4da30075048c60f,11185 + pantry-tree: + sha256: 44a1a038eafd6d59998c0b327b231e344252a64b083300e56649ebf2b7c20646 + size: 8725 + original: + hackage: text-2.1.3@sha256:1907e0f6914e376df3a3a1fbc5a04e49c729d333de34babba4da30075048c60f,11185 +snapshots: +- completed: + sha256: cd28bd74375205718f1d5fa221730a9c17a203059708b1eb95f4b20d68bf82d9 + size: 724943 + url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/24/2.yaml + original: lts-24.2 diff --git a/verifiable-expressions.cabal b/verifiable-expressions.cabal --- a/verifiable-expressions.cabal +++ b/verifiable-expressions.cabal @@ -1,11 +1,11 @@ cabal-version: 1.12 --- This file has been generated from package.yaml by hpack version 0.34.4. +-- This file has been generated from package.yaml by hpack version 0.38.1. -- -- see: https://github.com/sol/hpack name: verifiable-expressions -version: 0.6.2 +version: 0.6.3 synopsis: An intermediate language for Hoare logic style verification. description: A typed intermediate language for Hoare logic style verification. It defines the intermediate language and combinators to interact it. category: Language @@ -16,6 +16,8 @@ license: Apache-2.0 license-file: LICENSE build-type: Simple +tested-with: + GHC == 9.0, GHC == 9.2, GHC == 9.4, GHC == 9.6, GHC == 9.8, GHC == 9.10, GHC == 9.12 extra-source-files: CHANGELOG.md @@ -47,10 +49,15 @@ build-depends: base >=4.9 && <5 , containers >=0.5.7 && <0.7 - , lens >=4.16.1 && <5.1 + , lens >=4.16.1 && <5.5 , mtl >=2.0 && <3 - , sbv >=8.0 && <9 - , transformers ==0.5.* - , union >=0.1.1 && <0.2 - , vinyl >=0.9 && <0.14 + , transformers >=0.5 && <0.7 + , union >=0.1.2 && <0.2 + , vinyl >=0.14.3 && <0.15 default-language: Haskell2010 + if impl(ghc >= 9.6) + build-depends: + sbv >=10.0 && <11 + if impl(ghc < 9.6) + build-depends: + sbv >=8.0 && <10