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: evens   :: L Int
22: odds    :: L Int
23: range   :: Int -> Int -> L Int

Simple Refinement Types

Types + Predicates

Example: Integers equal to `0`

43: {-@ type Zero = {v:Int | v = 0} @-}
44: 
45: {-@ zero :: Zero @-}
46: {v : Int | (v == 0)}zero     =  x1:Int# -> {x2 : Int | (x2 == (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

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

Predicates

104: p := e           -- atom 
105:    | e1 == e2    -- equality
106:    | e1 <  e2    -- ordering 
107:    | (p && p)    -- and
108:    | (p || p)    -- or
109:    | (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}{v}{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'     =  {x3 : Int | (x3 == 0) && (x3 == SimpleRefinements.zero)}zero   -- zero :: Zero <: Nat

Contracts: Function Types

Pre-Conditions

224: Int -> {v : Int | (v /= 0)} -> IntsafeDiv Intn {v : Int | (v /= 0)}d = {x2 : Int | (x2 == n)}n x1:Int
-> x2:Int
-> {x6 : Int | (((x1 >= 0) && (x2 >= 0)) => (x6 >= 0)) && (((x1 >= 0) && (x2 >= 1)) => (x6 <= x1)) && (x6 == (x1 / x2))}`div` {x3 : Int | (x3 == d) && (x3 /= 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   = {x2 : Int | (x2 == (10  :  int))}10 Int -> {x3 : Int | (x3 /= 0)} -> Int`safeDiv` {x3 : Int | (x3 == n) && (x3 >= 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

291: {-@ ok  :: Nat -> Int @-}
292: {v : Int | (v >= 0)} -> Intok {v : Int | (v >= 0)}n    = {x2 : Int | (x2 == (10  :  int))}10 Int -> {x3 : Int | (x3 /= 0)} -> Int`safeDiv` ({x3 : Int | (x3 == n) && (x3 >= 0)}nx1:Int -> x2:Int -> {x4 : Int | (x4 == (x1 + x2))}+{x2 : Int | (x2 == (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

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

Precondition is checked at call-site

317: {-@ ok  :: Nat -> Int @-}
318: 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.

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

Specify post-condition as output type

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

Dependent Function Types

Outputs refer to inputs

Postcondition: `abs`

Specify post-condition as output type

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

Postcondition is checked at return-site

Postcondition: `abs`

Specify post-condition as output type

380: {-@ abs :: x:Int -> {v:Nat | x <= v} @-}
381: abs x | 0 <= x    = x 
382:       | 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

402: {-@ abs :: x:Int -> {v:Nat | x <= v} @-}
403: abs x | 0 <= x    = x 
404:       | 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 synthesize signatures from code

2-Phase Process

H-M to synthesize types
A-I to synthesize 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

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

[Rybalchenko et al., CAV 2011]

Recipe Scales Up

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

Define type checker, get inference for free
Scales to Data types, HO functions, Polymorphism

Key Requirement

Refinements belong in abstract domain, e.g. QF-UFLIA

Types = Universal Invariants

(Notoriously hard with pure SMT)

Types Yield Universal Invariants

Example: Lists

659: infixr `C`

670: data L a = N          -- Empty 
671:          | C a (L a)  -- Cons

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

682: (L {v : Int | (v >= 0)})nats     =  {x2 : Int | (x2 == (0  :  int))}0 {x8 : Int | (x8 >= 0)}
-> (L {x8 : Int | (x8 >= 0)}) -> (L {x8 : Int | (x8 >= 0)})`C` {x2 : Int | (x2 == (1  :  int))}1 {x14 : Int | ((x14 mod 2) == 1) && (x14 > 0) && (x14 >= 0)}
-> (L {x14 : Int | ((x14 mod 2) == 1) && (x14 > 0) && (x14 >= 0)})
-> (L {x14 : Int | ((x14 mod 2) == 1) && (x14 > 0) && (x14 >= 0)})`C` {x2 : Int | (x2 == (3  :  int))}3 {x14 : Int | ((x14 mod 2) == 1) && (x14 > 0) && (x14 >= 0)}
-> (L {x14 : Int | ((x14 mod 2) == 1) && (x14 > 0) && (x14 >= 0)})
-> (L {x14 : Int | ((x14 mod 2) == 1) && (x14 > 0) && (x14 >= 0)})`C` (L {x2 : Int | false})N

Example: Lists

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

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

Logic

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

VCs over quantified formulas ... terrible for SMT

Example: Lists

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

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

Refinement Types

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

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

Example: Lists

How to verify ?

738: {-@ nats :: L Nat @-}
739: nats   = l0
740:   where
741:     l0 = 0 `C` l1  -- Nat `C` L Nat >>> L Nat
742:     l1 = 1 `C` l2  -- Nat `C` L Nat >>> L Nat
743:     l2 = 2 `C` l3  -- Nat `C` L Nat >>> L Nat
744:     l3 = N         -- L Nat

Demo: What if nats contained -2?

Example: `range`

(range i j) returns Ints between i and j

Example: `range`

(range i j) returns Ints between i and j

802: {-@ type Btwn I J = {v:_ | (I<=v && v<J)} @-}

Example: `range`

(range i j) returns Ints between i and j

814: {-@ range :: i:Int -> j:Int -> L (Btwn i j) @-}
815: x1:Int -> x2:Int -> (L {v : Int | (v < x2) && (x1 <= v)})range Inti Intj            = x1:{x10 : Int | (x10 >= i) && (i <= x10)}
-> (L {x7 : Int | (x7 >= i) && (x7 >= x1) && (x7 < j) && (i <= x7) && (x1 <= x7)})go {x2 : Int | (x2 == i)}i
816:   where
817:     x1:{VV : Int | (VV >= i) && (i <= VV)}
-> (L {VV : Int | (VV >= i) && (VV >= x1) && (VV < j) && (i <= VV) && (x1 <= VV)})go {VV : Int | (VV >= i) && (i <= VV)}n | {x4 : Int | (x4 == n) && (x4 >= i) && (i <= x4)}n x1:Int -> x2:Int -> {x2 : Bool | (((Prop x2)) <=> (x1 < x2))}< {x2 : Int | (x2 == j)}j     = {x4 : Int | (x4 == n) && (x4 >= i) && (i <= x4)}n {x20 : Int | (x20 >= i) && (x20 >= n) && (x20 < j) && (i <= x20) && (n <= x20)}
-> (L {x20 : Int | (x20 >= i) && (x20 >= n) && (x20 < j) && (i <= x20) && (n <= x20)})
-> (L {x20 : Int | (x20 >= i) && (x20 >= n) && (x20 < j) && (i <= x20) && (n <= x20)})`C` x1:{VV : Int | (VV >= i) && (i <= VV)}
-> (L {VV : Int | (VV >= i) && (VV >= x1) && (VV < j) && (i <= VV) && (x1 <= VV)})go ({x4 : Int | (x4 == n) && (x4 >= i) && (i <= x4)}n x1:Int -> x2:Int -> {x4 : Int | (x4 == (x1 + x2))}+ {x2 : Int | (x2 == (1  :  int))}1)  
818:          | otherwise = (L {x2 : Int | false})N

Note: Type of go is automatically inferred

Example: Indexing Into List

832: (!)          :: L a -> Int -> a
833: (C x _)  forall a. (L a) -> Int -> a! 0 = {VV : a | (VV == x)}x
834: (C _ xs) ! i = (L a)xs forall a. (L a) -> Int -> a! (Inti x1:Int -> x2:Int -> {x4 : Int | (x4 == (x1 - x2))}- {x2 : Int | (x2 == (1  :  int))}1)
835: _        ! _ = {x1 : [Char] | false} -> aliquidError {x2 : [Char] | ((len x2) >= 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...]