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
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
Expressions
Predicates
Refinement Logic: QF-UFLIA
Quant.-Free. Uninterpreted Functions and Linear Arithmetic
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
102: p := e -- atom 103: | e1 == e2 -- equality 104: | e1 < e2 -- ordering 105: | (p && p) -- and 106: | (p || p) -- or 107: | (not p) -- negation
120: b := Int 121: | Bool 122: | ... -- base types 123: | a, b, c -- type variables 124: 125: t := {x:b | p} -- refined base 126: | x:t -> t -- refined function
\[\boxed{\Gamma \vdash t_1 \preceq t_2}\]
Where environment \(\Gamma\) is a sequence of binders
\[\Gamma \defeq \overline{\bindx{x_i}{t_i}}\]
(For Base Types ...)
\[ \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} \]
183: type Nat = {v:Int | 0 <= v}
Hence, we can type:
206: {-@ zero' :: Nat @-} 207: {v : Int | v >= 0}zero' = {v : Int | v == 0 && v == SimpleRefinements.zero}zero -- zero :: Zero <: Nat
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 @-}
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}\]
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}\)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)\]
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 inputsabs
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
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}\]
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}\]
So far
How to check code against given signature
Next
How to infer signatures from code
2-Phase Process
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
abs
)Type
\[\bindx{x}{\Int} \rightarrow \Int\]Template
\[\ereft{x}{\Int}{\kvar{1}} \rightarrow \reft{v}{\Int}{\kvar{2}}\]abs
)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} \]
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}\]
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.
abs
)Least-fixpoint over abstract domain
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}\]
abs
)Least-fixpoint over abstract domain
Predicate Abstraction
Conjunction of predicates from (finite) ground set \(\quals\)
1. Templates \(\rightarrow\) 2. Horn Constraints \(\rightarrow\) 3. Fixpoint
Define type checker and get inference for free
Scales to Collections, HOFs, Polymorphism
(Notoriously hard with pure SMT)
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
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\]
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 @-}
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
range
(range i j)
returns Int
s between i
and j
range
(range i j)
returns Int
s between i
and j
783: {-@ type Btwn I J = { v:_ | I<=v && v<J } @-}
range
(range i j)
returns Int
s 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
go
is automatically inferred
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!"
liquidError
)
i
between 0
and list length