Simple Refinement Types

10: {-@ LIQUID "--no-termination" @-}
11: module SimpleRefinements where
12: import Language.Haskell.Liquid.Prelude
13: import Prelude hiding (abs, max)
14: 
15: -- boring haskell type sigs
16: zero    :: Int
17: zero'   :: Int
18: safeDiv :: Int -> Int -> Int
19: abs     :: Int -> Int
20: nats    :: L Int
21: range   :: Int -> Int -> L Int

Simple Refinement Types

Types + Predicates

Example: Integers equal to `0`

41: {-@ type Zero = {v:Int | v = 0} @-}
42: 
43: {-@ zero :: Zero @-}
44: {v : Int | v == 0}zero     =  x1:Int# -> {v : Int | v == (x1  :  int)}0

Refinement types via special comments {-@ ... @-}

Demo

Refinements Are Predicates

From A Decidable Logic

Expressions
Predicates

Refinement Logic: QF-UFLIA

Quant.-Free. Uninterpreted Functions and Linear Arithmetic

Expressions

88: e := x, y, z,...    -- variable
89:    | 0, 1, 2,...    -- constant
90:    | (e + e)        -- addition
91:    | (e - e)        -- subtraction
92:    | (c * e)        -- linear multiplication
93:    | (f e1 ... en)  -- uninterpreted function

Predicates

102: p := e           -- atom 
103:    | e1 == e2    -- equality
104:    | e1 <  e2    -- ordering 
105:    | (p && p)    -- and
106:    | (p || p)    -- or
107:    | (not p)     -- negation

Subtyping Judgment

\[\boxed{\Gamma \vdash t_1 \preceq t_2}\]

Where environment \(\Gamma\) is a sequence of binders

\[\Gamma \defeq \overline{\bindx{x_i}{t_i}}\]

Subtyping is Implication

PVS' Predicate Subtyping

(For Base Types ...)

Subtyping is Implication

\[ \begin{array}{rl} {\mathbf{If\ VC\ is\ Valid}} & \bigwedge_i P_i \Rightarrow Q \Rightarrow R \\ & \\ {\mathbf{Then}} & \overline{\bindx{x_i}{P_i}} \vdash \reft{v}{b}{Q} \subty \reft{v}{b}{R} \\ \end{array} \]

Example: Natural Numbers

183:         type Nat = {v:Int | 0 <= v}

\[ \begin{array}{rcrccll} \mathbf{VC\ is\ Valid:} & \True & \Rightarrow & v = 0 & \Rightarrow & 0 \leq v & \mbox{(by SMT)} \\ % & & & & & \\ \mathbf{So:} & \emptyset & \vdash & \Zero & \subty & \Nat & \\ \end{array} \]

Hence, we can type:

206: {-@ zero' :: Nat @-}
207: {v : Int | v >= 0}zero'     =  {v : Int | v == 0 && v == SimpleRefinements.zero}zero   -- zero :: Zero <: Nat

Contracts: Function Types

Pre-Conditions

224: Int -> {v : Int | v /= 0} -> IntsafeDiv Intn {v : Int | v /= 0}d = {v : Int | v == n}n x1:Int
-> x2:Int
-> {v : Int | x1 >= 0 && x2 >= 0 => v >= 0 && x1 >= 0 && x2 >= 1 => v <= x1 && v == x1 / x2}`div` {v : Int | v == d && v /= 0}d   -- crashes if d==0

Requires non-zero input divisor d

233: {-@ type NonZero = {v:Int | v /= 0} @-}

Specify pre-condition as input type

244: {-@ safeDiv :: n:Int -> d:NonZero -> Int @-}

Precondition: `safeDiv`

Specify pre-condition as input type

256: {-@ safeDiv :: n:Int -> d:NonZero -> Int @-}

Precondition is checked at call-site

264: {-@ bad :: Nat -> Int @-}
265: {v : Int | v >= 0} -> Intbad {v : Int | v >= 0}n   = {v : Int | v == (10  :  int)}10 Int -> {v : Int | v /= 0} -> Int`safeDiv` {v : Int | v == n && v >= 0}n

Rejected As

\[\bindx{n}{\Nat} \vdash \reftx{v}{v = n} \not \subty \reftx{v}{v \not = 0}\]

Precondition: `safeDiv`

Specify pre-condition as input type

283: {-@ safeDiv :: n:Int -> d:NonZero -> Int @-}

Precondition is checked at call-site

292: {-@ ok  :: Nat -> Int @-}
293: {v : Int | v >= 0} -> Intok {v : Int | v >= 0}n    = {v : Int | v == (10  :  int)}10 Int -> {v : Int | v /= 0} -> Int`safeDiv` ({v : Int | v == n && v >= 0}nx1:Int -> x2:Int -> {v : Int | v == x1 + x2}+{v : Int | v == (1  :  int)}1)

Verifies As

\(\bindx{n}{\Nat} \vdash \reftx{v}{v = n+1} \subty \reftx{v}{v \not = 0}\)

Precondition: `safeDiv`

Specify pre-condition as input type

310: {-@ safeDiv :: n:Int -> d:NonZero -> Int @-}

Precondition is checked at call-site

318: {-@ ok  :: Nat -> Int @-}
319: ok n    = 10 `safeDiv` (n+1)

Verifies As

\[(0 \leq n) \Rightarrow (v = n+1) \Rightarrow (v \not = 0)\]

Post-Conditions

Ensures output is a Nat greater than input x.

336: x1:Int -> {v : Int | v >= 0 && x1 <= v}abs Intx | {v : Int | v == (0  :  int)}0 x1:Int -> x2:Int -> {v : Bool | Prop v <=> x1 <= v}<= {v : Int | v == x}x    = {v : Int | v == x}x 
337:       | otherwise = {v : Int | v == (0  :  int)}0 x1:Int -> x2:Int -> {v : Int | v == x1 - x2}- {v : Int | v == x}x

Specify post-condition as output type

346: {-@ abs :: x:Int -> {v:Nat | x <= v} @-}

Dependent Function Types

Outputs refer to inputs

Postcondition: `abs`

Specify post-condition as output type

364: {-@ abs :: x:Int -> {v:Nat | x <= v} @-}
365: abs x | 0 <= x    = x 
366:       | otherwise = 0 - x

Postcondition is checked at return-site

Postcondition: `abs`

Specify post-condition as output type

381: {-@ abs :: x:Int -> {v:Nat | x <= v} @-}
382: abs x | 0 <= x    = x 
383:       | otherwise = 0 - x

Verified As

\[\begin{array}{rll} \bindx{x}{\Int},\bindx{\_}{0 \leq x} & \vdash \reftx{v}{v = x} & \subty \reftx{v}{0 \leq v \wedge x \leq v} \\ \bindx{x}{\Int},\bindx{\_}{0 \not \leq x} & \vdash \reftx{v}{v = 0 - x} & \subty \reftx{v}{0 \leq v \wedge x \leq v} \\ \end{array}\]

Postcondition: `abs`

Specify post-condition as output type

403: {-@ abs :: x:Int -> {v:Nat | x <= v} @-}
404: abs x | 0 <= x    = x 
405:       | otherwise = 0 - x

Verified As

\[\begin{array}{rll} (0 \leq x) & \Rightarrow (v = x) & \Rightarrow (0 \leq v \wedge x \leq v) \\ (0 \not \leq x) & \Rightarrow (v = 0 - x) & \Rightarrow (0 \leq v \wedge x \leq v) \\ \end{array}\]

From Checking To Inference

So far

How to check code against given signature

Next

How to infer signatures from code

From Checking To Inference

2-Phase Process

Hindley-Milner infers types
Abstract Interpr. infers refinements

Lets quickly look at 2.

From Checking To Inference

Recipe

Step 1. Templates

Types with variables \(\kvar{}\) for unknown refinements

Step 2. Constraints

Typecheck templates: VCs \(\rightarrow\) Horn constraints over \(\kvar{}\)

Step 3. Solve

Via least-fixpoint over suitable abstract domain

Step 1. Templates (`abs`)

Type

\[\bindx{x}{\Int} \rightarrow \Int\]

Template

\[\ereft{x}{\Int}{\kvar{1}} \rightarrow \reft{v}{\Int}{\kvar{2}}\]

Step 2. Constraints (`abs`)

Subtyping Queries

\[ \begin{array}{rll} \bindx{x}{\kvar{1}},\bindx{\_}{0 \leq x} & \vdash \reftx{v}{v = x} & \subty \reftx{v}{\kvar{2}} \\ \bindx{x}{\kvar{1}},\bindx{\_}{0 \not \leq x} & \vdash \reftx{v}{v = 0 - x} & \subty \reftx{v}{\kvar{2}} \\ \end{array} \]

Step 2. Constraints (`abs`)

Verification Conditions

\[\begin{array}{rll} {\kvar{1}} \wedge (0 \leq x) & \Rightarrow (v = x) & \Rightarrow \kvar{2} \\ {\kvar{1}} \wedge (0 \not \leq x) & \Rightarrow (v = 0 - x) & \Rightarrow \kvar{2} \\ \end{array}\]

Step 2. Constraints (`abs`)

Horn Constraints over \(\kvar{}\)

\[\begin{array}{rll} {\kvar{1}} \wedge (0 \leq x) & \Rightarrow (v = x) & \Rightarrow \kvar{2} \\ {\kvar{1}} \wedge (0 \not \leq x) & \Rightarrow (v = 0 - x) & \Rightarrow \kvar{2} \\ \end{array}\]

Note: \(\kvar{}\) occur positively, hence constraints are monotone.

Step 3. Solve (`abs`)

Least-fixpoint over abstract domain

Step 3. Solve (`abs`)

Predicate Abstraction

Conjunction of predicates from (finite) ground set \(\quals\)

\[\mbox{e.g.}\ \quals \defeq \{ c \sim X \}\]

\[\begin{array}{ccll} c & \in & \{0,1,\ldots \} & \mbox{program constants} \\ X & \in & \{n,x,v,\ldots \} & \mbox{program variables} \\ \sim & \in & \{<, \leq, >, \geq, =, \not =\} & \mbox{comparisons} \\ \end{array}\]

Step 3. Solve (`abs`)

Least-fixpoint over abstract domain

Predicate Abstraction

Conjunction of predicates from (finite) ground set \(\quals\)

Obtain \(\quals\) via CEGAR
Or use other domains

[Houdini, HMC]

Recipe Scales Up

1. Templates \(\rightarrow\) 2. Horn Constraints \(\rightarrow\) 3. Fixpoint

Define type checker and get inference for free
Scales to Collections, HOFs, Polymorphism

Next: Collections

Types = Universal Invariants

(Notoriously hard with pure SMT)

Types Yield Universal Invariants

Example: Lists

677: infixr `C`

686: data L a = N          -- Empty 
687:          | C a (L a)  -- Cons

How to specify every element in nats is non-negative?

698: (L {v : Int | v >= 0})nats     =  {v : Int | v == (0  :  int)}0 {v : Int | v >= 0}
-> (L {v : Int | v >= 0}) -> (L {v : Int | v >= 0})`C` {v : Int | v == (1  :  int)}1 {v : Int | v /= 0 && v > 0 && v >= 0}
-> (L {v : Int | v /= 0 && v > 0 && v >= 0})
-> (L {v : Int | v /= 0 && v > 0 && v >= 0})`C` {v : Int | v == (3  :  int)}3 {v : Int | v /= 0 && v > 0 && v >= 0}
-> (L {v : Int | v /= 0 && v > 0 && v >= 0})
-> (L {v : Int | v /= 0 && v > 0 && v >= 0})`C` (L {v : Int | false})N

Example: Lists

How to specify every element in nats is non-negative?

711: nats     =  0 `C` 1 `C` 2 `C` N

Logic

\[\forall x \in \mathtt{nats}. 0 \leq x\]

VCs over quantified formulas ... challenging for SMT

Example: Lists

How to specify every element in nats is non-negative?

735: nats     =  0 `C` 1 `C` 2 `C` N

Refinement Types

743: {-@ nats :: L Nat @-}

Type implicitly has quantification
Sub-typing eliminates quantifiers
Robust verification via quantifier-free VCs

Example: Lists

How to verify ?

758: {-@ nats :: L Nat @-}
759: nats   = l0
760:   where
761:     l0 = 0 `C` l1  -- Nat `C` L Nat >>> L Nat
762:     l1 = 1 `C` l2  -- Nat `C` L Nat >>> L Nat
763:     l2 = 2 `C` l3  -- Nat `C` L Nat >>> L Nat
764:     l3 = N         -- L Nat

Example: `range`

(range i j) returns Ints between i and j

Example: `range`

(range i j) returns Ints between i and j

783: {-@ type Btwn I J = { v:_ | I<=v && v<J } @-}

Example: `range`

(range i j) returns Ints between i and j

795: {-@ range :: i:Int -> j:Int -> L (Btwn i j) @-}
796: x1:Int -> x2:Int -> (L {v : Int | v < x2 && x1 <= v})range Inti Intj            = x1:{v : Int | v >= i && i <= v}
-> (L {v : Int | v >= x1 && v >= i && v < j && x1 <= v && i <= v})go {v : Int | v == i}i
797:   where
798:     x1:{v : Int | v >= i && i <= v}
-> (L {v : Int | v >= x1 && v >= i && v < j && x1 <= v && i <= v})go {VV : Int | VV >= i && i <= VV}n | {v : Int | v == n && v >= i && i <= v}n x1:Int -> x2:Int -> {v : Bool | Prop v <=> x1 < v}< {v : Int | v == j}j     = {v : Int | v == n && v >= i && i <= v}n {v : Int | v >= n && v >= i && v < j && n <= v && i <= v}
-> (L {v : Int | v >= n && v >= i && v < j && n <= v && i <= v})
-> (L {v : Int | v >= n && v >= i && v < j && n <= v && i <= v})`C` x1:{VV : Int | VV >= i && i <= VV}
-> (L {VV : Int | VV >= x1 && VV >= i && VV < j && x1 <= VV && i <= VV})go ({v : Int | v == n && v >= i && i <= v}n x1:Int -> x2:Int -> {v : Int | v == x1 + x2}+ {v : Int | v == (1  :  int)}1)  
799:          | otherwise = (L {v : Int | false})N

Note: Type of go is automatically inferred

Example: Indexing Into List

813: (!)          :: L a -> Int -> a
814: (C x _)  forall a. (L a) -> Int -> a! 0 = {VV : a | VV == x}x
815: (C _ xs) ! i = (L a)xs forall a. (L a) -> Int -> a! (Inti x1:Int -> x2:Int -> {v : Int | v == x1 - x2}- {v : Int | v == (1  :  int)}1)
816: _        ! _ = {v : [Char] | false} -> aliquidError {v : [Char] | len v >= 0}"Oops!"

(Mouseover to view type of liquidError)

To ensure safety, require i between 0 and list length

Need way to measure the length of a list [continue...]