verifiable-expressions 0.6.2 → 0.6.3

raw patch · 13 files changed

+474/−7 lines, 13 filesdep ~lensdep ~sbv

Dependency ranges changed: lens, sbv

Files

• .github/workflows/ci.yml +97/−0
• .gitignore +5/−0
• CHANGELOG.md +4/−0
• Language/Expression/Lambda.hs +87/−0
• Language/Verification/Continuity.hs +75/−0
• Language/Verification/Core.hs +1/−0
• Language/While/Hoare.hs +1/−0
• README.md +6/−0
• notes.org +72/−0
• package.yaml +52/−0
• stack.yaml +13/−0
• stack.yaml.lock +47/−0
• verifiable-expressions.cabal +14/−7

@@ -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

@@ -0,0 +1,5 @@+/.stack-work+/dist-newstyle+/cabal.project.freeze++.DS_Store

@@ -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 

@@ -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 _

@@ -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

@@ -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

@@ -9,6 +9,7 @@  module Language.While.Hoare where +import Control.Monad (void, mzero) import Control.Monad.Writer  import           Language.While.Syntax

@@ -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.

@@ -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)

@@ -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

@@ -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

@@ -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

@@ -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