195: {-@ loop :: forall a a -> Prop>. 196: lo:Int 197: -> hi:{v:Int|lo <= v} 198: -> base:a 199: -> f:(i:Int -> a -> a) 200: -> a @-}

212: p :: Int -> a -> Prop -- invt 213: base :: a -- base 214: f :: i:Int -> a -> a<p(i+1)> -- step 215: out :: a -- goal

224: {-@ add :: n:Nat -> m:Nat -> {v:Nat| v=m+n} @-} 225: n:{VV : (Int) | (VV >= 0)} -> m:{VV : (Int) | (VV >= 0)} -> {VV : (Int) | (VV == (m + n)) && (VV >= 0)}add {VV : (Int) | (VV >= 0)}n {VV : (Int) | (VV >= 0)}m = forall (GHC.Types.Int)-> Bool>. x1:(Int) -> x2:{x21 : (Int) | (x1 <= x21)} -> {x19 : (Int) | (x19 >= 0) && (x19 >= n) && (n <= x19)} -> (i:(Int) -> {x19 : (Int) | (x19 >= 0) && (x19 >= n) && (n <= x19)} -> forall [ex:{VV : (Int) | (VV == (i + 1))}].{x19 : (Int) | (x19 >= 0) && (x19 >= n) && (n <= x19)}) -> {x19 : (Int) | (x19 >= 0) && (x19 >= n) && (n <= x19)}loop {x2 : (Int) | (x2 == (0 : int))}0 {x3 : (Int) | (x3 == m) && (x3 >= 0)}m {x3 : (Int) | (x3 == n) && (x3 >= 0)}n (x1:(Int) -> x2:{x17 : (Int) | (x17 == (x1 + n)) && (x17 == (n + x1)) && (x17 >= 0) && (x17 >= x1) && (x17 >= n) && (x1 <= x17) && (n <= x17)} -> {x9 : (Int) | (x9 == (x2 + 1)) && (x9 > 0) && (x9 > x1) && (x9 > x2) && (x9 > n) && (x9 >= 0) && (x1 <= x9) && (n <= x9)}\_ {VV : (Int) | (VV >= 0) && (VV >= n) && (n <= VV)}z -> {x5 : (Int) | (x5 == z) && (x5 >= 0) && (x5 >= n) && (n <= x5)}z x1:(Int) -> x2:(Int) -> {x4 : (Int) | (x4 == (x1 + x2))}+ {x2 : (Int) | (x2 == (1 : int))}1)

239: {-@ add :: n:Nat -> m:Nat -> {v:Nat| v=m+n} @-}
240: add n m = loop 0 m n (\_ z -> z + 1)

Verified by instantiating `p := \i acc -> acc = i + n` -

**Base:** `n = 0 + n`

**Step:** `acc = i + n => acc + 1 = (i + 1) + n`

**Goal:** `out = m + n`

Generalizes To Structures ------------------------- Same idea applies for induction over *structures* ... Structural Induction ==================== Example: Lists --------------

269: data L a = N 
270:          | C a (L a)

Lets write a generic loop over such lists ...

Example: `foldr` ----------------

283: foldr f b N        = b
284: foldr f b (C x xs) = f xs x (foldr f b xs)

Lets brace ourselves for the type...

Example: `foldr` ----------------

297: {-@ foldr :: 
298:     forall a b <p :: L a -> b -> Prop>. 
299:       (xs:_ -> x:_ -> b<p xs> -> b<p(C x xs)>) 
300:     -> b<p N> 
301:     -> ys:L a
302:     -> b<p ys>                            @-}
303: forall a b <p :: (Loop.L a)-> b-> Bool>.
(xs:(L a)
 -> x:a
 -> {VV : b<p xs> | true}
 -> forall [ex:{VV : (L a) | (VV == (Loop.C x xs))}].{VV : b<p ex> | true})
-> forall [ex:{VV : (L a) | (VV == (Loop.N))}].{VV : b<p ex> | true}
-> ys:(L a)
-> {VV : b<p ys> | true}foldr xs:(L a)
-> x:a
-> {VV : b | ((papp2 p VV xs))}
-> forall [ex:{VV : (L a) | (VV == (Loop.C x xs))}].{VV : b | ((papp2 p VV ex))}f forall [ex:{VV : (L a) | (VV == (Loop.N))}].{VV : a | ((papp2 p VV ex))}b N        = forall [ex:{VV : (L a) | (VV == (Loop.N))}].{VV : a | ((papp2 p VV ex))}b
304: foldr f b (C x xs) = x1:(L a)
-> x2:a
-> {VV : b | ((papp2 p VV x1))}
-> forall [ex:{VV : (L a) | (VV == (Loop.C x2 x1))}].{VV : b | ((papp2 p VV ex))}f {x2 : (L a) | (x2 == xs)}xs {VV : a | (VV == x)}x (forall <p :: (Loop.L a)-> b-> Bool>.
(xs:(L a)
 -> x:a
 -> {VV : b<p xs> | true}
 -> forall [ex:{VV : (L a) | (VV == (Loop.C x xs))}].{VV : b<p ex> | true})
-> forall [ex:{VV : (L a) | (VV == (Loop.N))}].{VV : b<p ex> | true}
-> x4:(L a)
-> {VV : b<p x4> | true}foldr x1:(L a)
-> x2:a
-> {VV : b | ((papp2 p VV x1))}
-> forall [ex:{VV : (L a) | (VV == (Loop.C x2 x1))}].{VV : b | ((papp2 p VV ex))}f forall [ex:{VV : (L a) | (VV == (Loop.N))}].{VV : a | ((papp2 p VV ex))}b {x2 : (L a) | (x2 == xs)}xs)

Lets step through the type...

`foldr`: Abstract Refinement ----------------------------

318: p    :: L a -> b -> Prop   
319: step :: xs:_ -> x:_ -> b<p xs> -> b<p(C x xs)> 
320: base :: b<p N> 
321: ys   :: L a
322: out  ::  b<p ys>

`(p xs b)` relates `b` with folded `xs` `p :: L a -> b -> Prop` `foldr`: Base Case ------------------

336: p    :: L a -> b -> Prop   
337: step :: xs:_ -> x:_ -> b<p xs> -> b<p(C x xs)> 
338: base :: b<p N> 
339: ys   :: L a
340: out  :: b<p ys>

`base` is related to empty list `N` `base :: b

` states `foldr`: Ind. Step ------------------

355: p    :: L a -> b -> Prop   
356: step :: xs:_ -> x:_ -> b<p xs> -> b<p(C x xs)> 
357: base :: b<p N> 
358: ys   :: L a
359: out  :: b<p ys>

`step` extends relation from `xs` to `C x xs` `step :: xs:L a -> x:a -> b

-> b` `foldr`: Output ---------------

373: p    :: L a -> b -> Prop   
374: step :: xs:_ -> x:_ -> b<p xs> -> b<p(C x xs)> 
375: base :: b<p N> 
376: ys   :: L a
377: out  :: b<p ys>

Relation holds between `out` and input list `ys` `out :: b

` Using `foldr`: Size ------------------- We can now verify

392: {-@ size :: xs:_ -> {v:Int| v = (llen xs)} @-}
393: forall a. xs:(L a) -> {VV : (Int) | (VV == (llen xs))}size     = forall <p :: (Loop.L a)-> (GHC.Types.Int)-> Bool>.
(xs:(L a)
 -> x:a
 -> {x12 : (Int)<p xs> | (x12 >= 0)}
 -> forall [ex:{VV : (L a) | (VV == (Loop.C x xs))}].{x12 : (Int)<p ex> | (x12 >= 0)})
-> forall [ex:{VV : (L a) | (VV == (Loop.N))}].{x12 : (Int)<p ex> | (x12 >= 0)}
-> x4:(L a)
-> {x12 : (Int)<p x4> | (x12 >= 0)}foldr (x1:(L a)
-> a
-> x3:{x8 : (Int) | (x8 == (llen x1)) && (x8 >= 0)}
-> {x5 : (Int) | (x5 == (x3 + 1)) && (x5 > 0) && (x5 > x3) && (x5 >= 0)}\_ _ {VV : (Int) | (VV >= 0)}n -> {x3 : (Int) | (x3 == n) && (x3 >= 0)}n x1:(Int) -> x2:(Int) -> {x4 : (Int) | (x4 == (x1 + x2))}+ {x2 : (Int) | (x2 == (1  :  int))}1) {x2 : (Int) | (x2 == (0  :  int))}0

Verified by automatically instantiating `p := \xs acc -> acc = (llen xs)`

Using `foldr`: Append ---------------------

408: {-@ (++) :: xs:_ -> ys:_ -> (Cat a xs ys) @-} 
409: (L a)xs forall a.
xs:(L a)
-> ys:(L a)
-> {VV : (L a) | ((llen VV) == ((llen xs) + (llen ys)))}++ (L a)ys = forall <p :: (Loop.L a)-> (Loop.L a)-> Bool>.
(xs:(L a)
 -> x:a
 -> {x8 : (L a)<p xs> | true}
 -> forall [ex:{VV : (L a) | (VV == (Loop.C x xs))}].{x8 : (L a)<p ex> | true})
-> forall [ex:{VV : (L a) | (VV == (Loop.N))}].{x8 : (L a)<p ex> | true}
-> x4:(L a)
-> {x8 : (L a)<p x4> | true}foldr ((L a)
-> a -> x3:(L a) -> {x2 : (L a) | ((llen x2) == (1 + (llen x3)))}\_ -> a -> x2:(L a) -> {x2 : (L a) | ((llen x2) == (1 + (llen x2)))}C) {x2 : (L a) | (x2 == ys)}ys {x2 : (L a) | (x2 == xs)}xs

where the alias `Cat` is:

421: {-@ type Cat a X Y = 
422:     {v:L a|(llen v) = (llen X) + (llen Y)} @-}

Using `foldr`: Append ---------------------

431: {-@ (++) :: xs:_ -> ys:_ -> (Cat a xs ys) @-} 
432: xs ++ ys = foldr (\_ -> C) ys xs

Verified by automatically instantiating `p := \xs acc -> llen acc = llen xs + llen ys`

Recap ----- Abstract refinements decouple *invariant* from *traversal*
+

*reusable* specifications for higher-order functions.

*automatic* checking and instantiation by SMT.

Recap ----- 1. **Refinements:** Types + Predicates 2. **Subtyping:** SMT Implication 3. **Measures:** Strengthened Constructors 4. **Abstract:** Refinements over Type Signatures + *Dependencies* +

*Induction*