Days and Ghost Refinements
Contents
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:


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


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 ValueDependent Types” paper:
Concrete refinements are 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 refinements are used to state specifications for which proof terms are not maintained at run time. Ghost refinements have the form $x:t\{\phi\}$ where $x$ is a value variable, $t$ is a type, and $\phi$ is a logical formula, itself represented as a type that must have kind $E$ and may depend on $x$ and other inscope 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\{\phi\}$ is a subtype of $t$; this structural subtyping is convenient to write and verify higherorder 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 =).


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


Well, 12 was supposed to be here:


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


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


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:


The last line gives the following error:


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:


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:


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 multiparty 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 ValueDependent 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 endofFeb 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.
Author Natallie
LastMod 20130707