Refinement types for Cogent

Tests for Refinement Type in Cogent

Cogent information:

• branch: wip-reftypes
• commit: 8e43ce3666331980a116ce9842584dbb77a4a1f0

NOTE: the following two programs are very different. The first one ends up with an addition with incompatible unsigned int types, whereas the latter one is valid. (This has nothing to do with ref.types though.)

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

-- should pass
foo : U8 -> U8
foo x = x + 255 + 1

As unsigned int under/over-flow is very widely used, well-behaved, well-understood among researshers and engineers, and formally specified, there’s no reason we reject under/over-flow. However, whenever desired, the user can use refinement types to check that it doesn’t happen, just as we all learn in first-year computing courses, that the result of an addition is larger than either argument.

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

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}