# Days and Ghost Refinements

*[This blog was moved here]*

Let’s look at the simple function, which calculates the number of days between dates, when there’re 30 days in a month (and 360 in a year). Something like this F# code:

1: let days360 sy sm sd ey em ed = 2: (ey - sy)*360 + (em - sm)*30 + (ed - sd)

We can even write a bunch of tests to be sure the function works:

1: let tests = [ 2: DateTime(2012,2,29), DateTime(2013,2,28), 359 3: DateTime(2012,2,29), DateTime(2012,3,01), 2 4: DateTime(2012,2,29), DateTime(2013,3,01), 362 5: DateTime(2012,3,01), DateTime(2013,3,01), 360 6: DateTime(2011,2,28), DateTime(2013,2,28), 720 7: DateTime(2012,5,31), DateTime(2012,7,31), 60 8: ] 9: 10: //true 11: tests |> Seq.forall(fun (s,e,res) -> 12: days360 s.Year s.Month s.Day e.Year e.Month e.Day = res)

As you see days360 doesn’t take .NET DateTime as parameters, but ints. Would be nice to check them. Say, a month can take value from 1 to 12 – so what we need is a refinement type. F* supports two types of refinements: concrete and ghost. Here is how they are defined in “Secure Distributed Programming with Value-Dependent Types” paper:

Concrete refinementsare pairs representing a value and a proof term serving as a logical evidence of the refinement property, similar to those in Coq and Fine.

Ghost refinementsare used to state specifications for which proof terms are not maintained at run time. Ghost refinements have the formx:t{φ }wherexis a value variable,tis a type, andφis a logical formula, itself represented as a type that must have kindEand may depend onxand other in-scope variables. Ghost refinements provide the following benefits:– they enable precise symbolic models for many cryptographic patterns and primitives, and evidence for ghost refinement properties can be constructed and communicated using cryptographic constructions, such as digital signatures;

– they benefit from a powerful subtyping relation:

x:t{φ }is a subtype oft; this structural subtyping is convenient to write and verify higher-order programs;– they provide precise specification to legacy code without requiring any modifications;

– when used in conjunction with concrete refinements, they support selective erasure and dynamic reconstruction of evidence, enabling a variety of new applications and greatly reducing the performance penalty for runtime proofs.

Here we use the numbers as an example, because they are simple and intersections/unions of types are obvious. Note that we don’t verify that the dates are entirely valid. This is an artificial example – small enough to try it online =).

1: type year = x:int{ 1900 <= x /\ x <= 9999 } 2: type month = x:int{ 1 <= x /\ x <= 12 } 3: type day = x:int{ 1 <= x /\ x <= 31 } 4: 5: val days360: year -> month -> day -> int 6: 7: let days360 sy sm sd ey em ed = 8: (ey - sy)*360 + (em - sm)*30 + (ed - sd) 9: 10: let _ = days360 2013 6 1 2013 6 42

We run F* – and get a type check time failure!

input(12,8-12,34) : Error : Expected an expression of type: x_5_1:int{((LTE 1 x_5_1) && (LTE x_5_1 31))} but got (42): int Type checking failed

Well, 12 was supposed to be here:

1: let _ = days360 2013 6 1 2013 6 12 //ok

But wait, there’re still 31-day months… and February. With EU 30/360 convention 31 is simply replaced with 30, so we modify the function:

1: let adjDay d = if d = 31 then 30 else d 2: 3: let days360 sy sm sd ey em ed = 4: let sd, ed = adjDay sd, adjDay ed 5: (ey - sy)*360 + (em - sm)*30 + (ed - sd) 6: 7: //DateTime(2012,4,25), DateTime(2012,7,31), 95 8: //DateTime(2012,6,30), DateTime(2012,7,31), 30 9: //DateTime(2012,2,28), DateTime(2012,3,31), 32 10: //DateTime(2012,2,29), DateTime(2012,3,31), 31

In this case start and end dates can’t be greater than 30. Can we define that with types? Sure!

1: type day30 = x:day{ x <> 31 } 2: 3: val adjDay: day -> day30 4: let adjDay d = if d = 31 then 30 else d //try to leave only d here - it fails to typecheck

What if we want to add another convention? US 30/360 handles EOM dates differently, so if a start date is greater than end date the function results can become inconsistent. So we expect start date to be less than (or equal to) end date. A type checker can verify this requirement too:

1: val daysInMonth: year -> month -> day 2: 3: val lastDay: year -> month -> day -> bool -> bool 4: //EU 30/360: the last day of Feb is not changed to 30 5: let lastDay y m d eu = 6: if eu && (m = 2) then false 7: else d = (daysInMonth y m) 8: 9: let adjDay d last = if last then 30 else d 10: 11: val days360: sy:year -> sm:month -> sd: day 12: -> ey:year{ey >= sy} 13: -> em:month{ey > sy \/ (ey = sy /\ em >= sm)} 14: -> ed:day{ey > sy \/ em > sm \/ ed >= sd} 15: -> bool 16: -> int 17: 18: let days360 sy sm sd ey em ed convEU = 19: let slast, elast = lastDay sy sm sd convEU, lastDay ey em ed convEU in 20: 21: //EU: 31 -> 30 22: //US: 31 -> 30; end of Feb -> 30 23: let sd = adjDay sd slast in 24: //EU: 31 -> 30 25: //US: 31 -> 30 if sd is EOM; end of Feb -> 30 if sd was end of Feb too 26: let checkEndDate = convEU || (slast && ((sm = 2) || not (em = 2))) in 27: let ed = adjDay ed (elast && (convEU || checkEndDate)) in 28: 29: (ey - sy)*360 + (em - sm)*30 + (ed - sd) 30: 31: let _ = days360 2013 7 6 2015 7 6 true 32: let _ = days360 2015 7 6 2013 7 6 true //error

The last line gives the following error:

input(44,8-44,29) : Error : Expected an expression of type: x_23_6: Dates.year{GTE x_23_6 2013} but got (2013): int Type checking failed

All these >, \/, /\, < look funny, if it’s not enough – just imagine the effect of adding time components. Fortunately, the relation between the dates can be defined as a separate type:

1: //start date <= end date 2: type LTE = fun sy sm sd ey em ed => 3: ey > sy \/ (ey = sy /\ (em > sm \/ (em = sm /\ ed >= sd))) 4: 5: val days360: sy:year -> sm:month -> sd:day 6: -> ey:year -> em:month -> ed:day{LTE sy sm sd ey em ed} 7: -> bool 8: -> int

Now let’s assume that a date is valid when it’s not 2/30 or 2/31. We can define a logical function using `logic val`

construct. Such functions can be used in refinements but not in code itself. The axioms are defined using the `assume`

construct:

1: logic val isValidDate: year -> month -> day -> bool 2: assume Valid: forall y m (d:day{m <> 2 \/ d < 30}). isValidDate y m d = true 3: 4: val days360: sy:year -> sm:month -> sd:day{isValidDate sy sm sd = true} 5: -> ey:year -> em:month -> ed:day{isValidDate ey em ed = true /\ LTE sy sm sd ey em ed} 6: -> bool 7: -> int

Well, quite enough of refinements for a start. There’s much more ways to apply them: for example, refinements with affine values are great for verification of stateful programs (see the “Secure multi-party sessions in F*” section in the paper). With rise4fun you may get a request timeout in more complex cases, so I’d recommend to download the F* package for your experiments.

**References**

**1.** “Secure Distributed Programming with Value-Dependent Types” paper

**2.** F* home page

**3.** Rise4fun tutorial

**Bonus**

Time to get back to the good old tests: the obvious idea is to compare the results with Excel. We are interested in two functions: DAYS360 and YEARFRAC – multiplying the result with 360. Look at the following comparison (when the spreadsheet was converted to Google Docs format, the results were changed, so I added separate rows with Excel output):

There’re obvious problems with DAYS360 when the dates are swapped (start date > end date) and end-of-Feb cases. But our function is different from YEARFRAC too.

Date adjustments rules for 30/360US:

1. If the investment is EOM and D1, D2 are the last day of Feb, then D2 = 30

2. If the investment is EOM and D1 is the last day of Feb, then D1 = 30

3. If D2 is 31 and D1 is 30 or 31, then D2 = 30

4. If D1 is 31, then D1 = 30

Let the start and end dates be 2/29/2012 and 3/31/2012 respectively. The rules are applied in order:

`D2 - D1 = D2 - 30 = 30 - 30 = 0`

But in Excel the rule 3 goes before the rule 2 (our function can be simply modified to behave the same way: `sm = 2 || em <> 2`

should be replaced with `(sm = 2) = (em = 2)`

):

`D2 - D1 = 31 - D1 = 31 - 30 = 1`

So we expect to see `(2012 – 2012)*360 + (3 – 2)*30 + 0 = 30`

and not `31`

.

F# version is available here.

Pingback: F# Weekly #27 2013 | Sergey Tihon's Blog()