Refinement types for Cogent

Tests for Refinement Type in Cogent

Cogent information:

• branch: wip-reftypes
• commit: 8e43ce3666331980a116ce9842584dbb77a4a1f0

integer underflow

We have an explicit integer overflow in this example. It won’t trigger any alerts:

type Ge255 = [x: U8 | x >= 255]

-- passed
-- should pass
foo : Ge255 -> U8
foo x = x + 255

However, the following code could be detected (because of incompatiable base types):

-- failed
-- should fail
foo : U8 -> U8
foo x = x + 256

This example will pass the compiler (unsafely) as well due to lack of constant propagation:

-- !!!! passed
-- should fail
foo : U8 -> U8
foo x = x + 255 + 1

Question:

• should we add default constraints for primitive type (e.g. type U8 = [x: U8 | x < 256])?
• should the compiler support constant propagation?

minus underflow

The SMT solver convert 0 - 1 to 255 under U8 bitvector:

type Range = [x: U8 | x <= 10]

-- !!!! failed
-- exptected cogent behavior, but should we be allowing underflow
foo : U8 -> Range
foo x = 0 - 1 -- equals to 255

If we allow the 255 in valid range, the test could pass:

type Range = [x: U8 | x <= 10 || x == 255]

-- !!!! failed
-- SMT solver phase failed; it should pass if x == 255
-- do we want to have underflow now that we have refinement types?
-- should we disallow underflow by default?
-- or only when the refinement type explicitly gives a range?
foo : U8 -> Range
foo x = 0 - 1

When only the primitive type is used, the test could pass:

-- passed
-- should pass
bar : U8 -> U8
bar x = 0 - 1

add within if range

The following example works. We will see examples later where if branching does not work:

-- passed
-- should pass
type Lt3 = [x: U8 | x < 3]

foo : Lt3 -> Lt3
foo x = if x < 3 then x + 1 else x * 1

casting

Let’s first try a simple example (type cast on primitive type):

-- passed
-- should pass
foo : (U32, U8) -> U32
foo (x, y) = x + upcast y

But the casting of refinement type does not work:

type U32_Lt3 = [x: U32 | x < 3]
type U8_Lt3 = [x: U8 | x < 3]
type U32_Lt5 = [x: U32 | x < 5 ]

-- !!!! failed
-- should pass (safe upcast)
foo1 : (U32_Lt3, U8_Lt3) -> U32_Lt5
foo1 (x, y) = let (z : U32_Lt3) = upcast y in z + x

array size restriction through if

The follwing code fails although it should pass. Maybe due to type normalization.

-- !!!! failed
-- should pass
-- the if branching is not added to SMT solver
bar : U32 -> U32
bar x = if x < 3   
        then [1,2,3,4] @ x
        else 0

But if we use refinement type to limit the array index, it will work:

type Lt3 = [x: U32 | x < 3]

-- passed
-- should pass
foo : Lt3 -> U32
foo x = [1,2,3,4] @ x

Neither this (with let) because it won’t apply if constraints.

-- !!!! failed
-- should pass
bar : U32 -> U32
bar x = if x < 3 then let y = x in [1,2,3,4] @ y else 0

But it works when the targeting output is refinement type.

type Lt4 = [x: U32 | x < 4]

-- passed
-- should pass
bar : U32 -> Lt4
bar x = if x < 3 then x + 1 else 0

if contradiction

We could add a contradition on refinement type and if branching, the compiler will pass the test:

type Lt3 = [x: U32 | x < 3]

-- !!!! passed
-- should we allow the contradition?
foo : Lt3 -> Lt3
foo x = if x > 100 then x else x

excluded middle

Exclude middle by if branch is not working yet.

type T = [v: Bool | v == True]

-- !!!! failed
-- should pass
foo : Bool -> T
foo x = let y = (x || (not x)) in y

But it looks rather an issue for the boolean solver, the current checker even failed in this example:

type T = [v: Bool | v == True]

-- !!!! failed
-- should pass
foo : T -> T
foo x = True

But it does pass when return type is refinement type:

type T = [v: Bool | v == True]

-- passed
-- should pass
foo : T -> T
foo x = x

The refinement type level exclude middle works:

type T = [v: Bool | v || not(v)]

-- passed
-- should pass
foo : Bool -> T
foo x = x   

mod operator

Mod operator is not supported yet.

type N0 = [x: U32 | x > 0]
type Lt3 = [x: U32 | x < 3]

-- !!!! failed
-- should pass (after implementation)
bar : N0 -> Lt3
bar x = x % 3

But we can use alternative implementation by div.

type N0 = [x: U32 | x > 0]
type Lt3 = [x: U32 | x < 3]

-- passed
-- should pass
mymod : N0 -> Lt3
mymod x = let y = x / 3
          and z = x - (y * 3)
           in z

record field initialization

Non-exhaustive pattern in cogent internal. Maybe due to type normalization.

type R = { f1 : U8, f2 : U8 }
type RR = [v : R | v.f1 < 10]

-- !!!! failed
-- should pass
foo : RR -> RR
foo (r {f1, f2}) = r {f1, f2}

temporary value refinement

In the following case, the compilation will fail as expected.

f1: U8 -> [v: U8 | v < 10]
f2: U8 -> [v: U8 | v < 2]

-- failed
-- should fail
bar : U8 -> [v: U8 | v > 100]
bar x = let y = f1 x and z = f2 x in y + z

However, if we don’t use any temporary variable to store the result, the SMT solving phase will fail.

f1: U8 -> [v: U8 | v < 10]
f1 x = 1

f2: U8 -> [v: U8 | v < 2]
f2 x = 1

-- !!!! failed
-- this example failed at SMT solver but not type checker
bar : U8 -> [v: U8 | v > 100]
bar x = let y = f1 x in (f2 x) + y

large array

The max range of unsigned 32 is 4,294,967,295, (array size should +1) thefore a U32 could fetch array with this size without limitation.

-- !!!! failed
-- should pass
foo : (U8[4294967296]!, U32) -> U8
foo (x, y) = x @ y

If we set refinement range equal to 4,294,967,296, it could infer the number to be U64.

-- failed
-- should fail (4294967296 is U64, different in base type)
type R32 = [v: U64 | v <= 4294967296]

We cannot retrieve array by index in unsigned 64.

type R64 = [v: U64 | v < 4294967296]

-- !!!! failed
-- should pass
foo : (U8[4294967296] !, R64) -> U8
foo (x, y) = x @ y

Unless we explicitly specify the range of refinement type, the checker cannot infer the range of U32.

dependent record field

Not sopported yet.

type R = { f1 : U8, f2 : U8 }
type RR = [v : R | v.f1 < v.f2]

-- !!!! passed
-- should fail
foo : RR -> RR
foo (r {f1, f2}) = let x = r {f1 = f2} in x {f2 = f2}

type R = { f1 : U8, f2 : U8 }
type RR = [v : R | v.f1 < v.f2]

-- !!!! passed
-- should fail
foo : RR -> RR
foo (r {f1}) = r {f1 = 100}