Debugging coverage errors

From The Twelf Project
Jump to: navigation, search

This page lists techniques for debugging input coverage and output coverage errors.

Debugging input coverage errors by adding type annotations

Motivating example

As a motivating example, we define a simple subtyping relation on the types of a programming language. The language includes integers, floating point numbers, and functions. We consider int to be a subtype of float, and we give the usual contravariant rule for functions:

tp    : type.
int   : tp.
float : tp.
arrow : tp -> tp -> tp.

sub       : tp -> tp -> type.
sub-ii    : sub int int.
sub-ff    : sub float float.
sub-if    : sub int float.
sub-arrow : sub (arrow T S) (arrow T' S')
	     <- sub T' T
	     <- sub S S'.

Let's prove that this subtyping relation is transitive. When writing Twelf code, it's sometimes convenient to just blaze ahead with a proof without thinking to hard about what you're doing, and then think about what's going on only if Twelf reports an error. So a first proof attempt might look like this:

sub-trans : sub T1 T2 -> sub T2 T3 -> sub T1 T3 -> type.
%mode sub-trans +X1 +X2 -X3.

- : sub-trans (D : sub T T) (D' : sub T T) D.
- : sub-trans sub-ii sub-if sub-if.
- : sub-trans sub-if sub-ff sub-if.

-arrow : sub-trans 
         (sub-arrow DS DT)
         (sub-arrow DS' DT')
         (sub-arrow DS'' DT'')
         <- sub-trans DT DT' DT''
         <- sub-trans DS DS' DS''.

We let our fingers do the proving and came up with the straightforward inductive proof. Each case type checks. Does it work?

%worlds () (sub-trans _ _ _).
%total D (sub-trans D _ _).
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

%worlds () (sub-trans _ _ _). Error: Coverage error --- missing cases: {X1:tp} {X2:tp} {X3:tp} {X4:tp} {X5:tp} {X6:tp} {X7:sub X2 X4} {X8:sub X3 X1} {X9:sub X4 X6} {X10:sub X5 X3} {X11:sub (arrow X1 X2) (arrow X5 X6)} |- sub-trans (sub-arrow X7 X8) (sub-arrow X9 X10) X11.

%% ABORT %%

Twelf reports an input coverage error: we didn't cover the case for sub-arrow against sub-arrow. We think: "But I wrote a case for sub-arrow against sub-arrow right up there! What do you mean I didn't cover it?!"

Debugging technique

What Twelf is saying is that we didn't cover the general case for sub-arrow against sub-arrow. That is, the inferred type of the constant -arrow must be less general than required. One way to figure out the problem is to read the type of the constant:

-arrow : sub-trans 
         (sub-arrow DS DT)
         (sub-arrow DS' DT')
         (sub-arrow DS'' DT'')
         <- sub-trans DT DT' DT''
         <- sub-trans DS DS' DS''.
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

-arrow : {X1:tp} {X2:tp} {X3:tp} {DS:sub X1 X2} {DS':sub X2 X3} {DS'':sub X1 X3} {X4:tp} {DT:sub X4 X4} {DT':sub X4 X4} {DT'':sub X4 X4} sub-trans DS DS' DS'' -> sub-trans DT DT' DT'' -> sub-trans (sub-arrow DS DT) (sub-arrow DS' DT') (sub-arrow DS'' DT'').

%% OK %%

As you can see, the type that Twelf inferred has the same type X4 as all three types related by DT and DT'. Because Twelf unified these parameters, -arrow doesn't cover the whole space that we think it does.

Now, we have to figure out why Twelf inferred this type. What mistake did we actually make? One good way to figure this out is to start adding type annotations giving the constants fully general types. By doing so, we can turn a coverage error into a type error on the constant.

For example, let's annotate this constant more carefully with what we expect the inputs to be:

-arrow : sub-trans 
         (sub-arrow (DS : sub S1 S2) (DT : sub T2 T1))
         (sub-arrow (DS' : sub S2 S3) (DT' : sub T3 T2))
         (sub-arrow DS'' DT'')
         <- sub-trans DT DT' DT''
         <- sub-trans DS DS' DS''.
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

Error: Type mismatch Expected: sub `T3 `T2 Inferred: sub `T1 X1 Free variable clash Ascription did not hold (Index object(s) did not match) Error: Type mismatch Expected: sub (arrow `T1 `S1) (arrow `T3 `S3) Inferred: sub (arrow X1 `S1) (arrow `T2 `S3) Free variable clash Argument type did not match function domain type (Index object(s) did not match) Error: 2 errors found

%% ABORT %%

This causes Twelf to report a type error, so we know we're on the right track—the constant doesn't cover what we want it to.

We can make this type error more comprehensible by removing some of the constraints. Specifically, we can take out the return term to remove some of the constraints on DT:

-arrow : sub-trans 
         (sub-arrow (DS : sub S1 S2) (DT : sub T2 T1))
         (sub-arrow (DS' : sub S2 S3) (DT' : sub T3 T2))
         _
         <- sub-trans DT DT' DT''
         <- sub-trans DS DS' DS''.
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

Error: Type mismatch Expected: sub `T3 `T2 Inferred: sub `T1 X1 Free variable clash Ascription did not hold (Index object(s) did not match) Error: 1 error found

%% ABORT %%

Ah ha! Twelf is pointing us to the first premise, as saying that because DT has type sub T2 T1, the second argument DT' needs to have type sub T1 X1 for some X1; but we wrote a term with type sub T3 T2. If we annotate the constant enough that Twelf knows that T1 and T3 are supposed to be different, this is reported as a type error. Otherwise, Twelf unifies these two, coming up with a valid type for the constant; but because this type doesn't cover the part of the relation that we thought it did, we get an input coverage error.

As you may have figured out already, the problem is that the first recursive call should swap the two arguments:

-arrow : sub-trans 
         (sub-arrow (DS : sub S1 S2) (DT : sub T2 T1))
         (sub-arrow (DS' : sub S2 S3) (DT' : sub T3 T2))
         (sub-arrow DS'' DT'')
         <- sub-trans DT' DT DT''
         <- sub-trans DS DS' DS''.
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

-arrow : {S1:tp} {S2:tp} {S3:tp} {DS:sub S1 S2} {DS':sub S2 S3} {DS'':sub S1 S3} {T3:tp} {T2:tp} {T1:tp} {DT':sub T3 T2} {DT:sub T2 T1} {DT'':sub T3 T1} sub-trans DS DS' DS'' -> sub-trans DT' DT DT'' -> sub-trans (sub-arrow DS DT) (sub-arrow DS' DT') (sub-arrow DS'' DT'').

%% OK %%

In this example, this "fix" itself creates some termination trouble; see the article on mutual induction for a completed proof. But the broken proof illustrates a useful technique for coverage checking.

A Messy Example

In the previous example, adding types to some variables caused a coverage error to be converted into a type error. But a complex case may have many many variables. Coverage errors can be very hard to find in this case. In the following situation (from me=John Boyland), it is shown how to leverage the Twelf server to do most of the work. Suppose (and this happened to me), one has a coverage error that "should" have been covered by the following horrendous case:

- : wk-is/L ES 
       (access/read
          (ready/ (read (lit (object/ O)) F) TL1 L1 A))
       ML NFL XTL XSF FE ESG WA XPK XSM NHBP
       (incorrectly-synchronized/W 
          (eval-seq/+ ESN 
             (fulleval/ _ (lit (object/ O')) TL1N L1 
                (eRead ML' NFL' TL1N K>Z) TL1N TU1N))
          (eval-seq-get/ (eval-seq-includes/> ESI'))
          (eval-seq-get/ eval-seq-includes/=) WA'
          (access/read
             (ready/ (read (lit (object/ O)) F) TL1N L1 A))
          NHB')
    <- no-know-eval-seq-exists ES _ (no-know-state/ NM NTS) ESN ESM
        (state-match/ MM TSM)
    <- eval-seq-get-respects-match ESG ESM _ _ _ (eval-seq-get/ ESI') FEM
    <- mem-lookup-respects-match ML MM _ ML' (objs-match/ NFM _ _)
    <- no-know-mem-lookup-implies-no-know-contents ML' NM (no-know-objs/ NNF _ _)
    <- normal-fields-lookup-respects-match NFL NFM _ NFL'
    <- no-know-normal-fields-lookup-implies-no-know-contents NFL' NNF Z=W
    <- threads-lookup-respects-match TL1 TSM _ TL1N
    <- no-know-threads-lookup-implies-no-know-contents TL1N NTS Z=K
    <- set`member-respects-eq (set`lookup/= nat`eq/) Z=K Z=W K>Z
    <- threads`update-total TU1N
    <- hb-potential?-respects-match NHBP ESM NHBP'
    <- not-hb-potential-realized NHBP' _ (non-sw2-fulleval/ non-synch2-atomic/read) NHB'
    <- wk-is/L2 WA TSM WA'.

Now, even if the contents meant anything to you (just pretend...), typing in the types of all those variables is impractical. Instead, we replace the output with a new (or underscore) variable and terminate the case:

- : wk-is/L ES 
       (access/read
          (ready/ (read (lit (object/ O)) F) TL1 L1 A))
       ML NFL XTL XSF FE ESG WA XPK XSM NHBP _.

Then, we submit this to the server, which (of course) will complain that the output is not necessarily ground. But with chatter set to 3, it also outputs the types of all the variables, including the implicit ones. Then these can be copied into the buffer (after removing %name% types if you have any):

- :  {X1} {N1:nat} {X2:map} {X3} {N2:nat} {O:nat} {F:nat} {X4}
      {X5} {X6:lock-contents} {N3:nat} {N4:nat} {X7} {X8:term exprk}
      {N5:nat} {X9:map} {X10} {X11:map} {X12} {N6:nat}
      {X14} {ES:eval-seq X1 N1 (state/ X2 X3)} {X15}
      {X16:term exprk -> term exprk}
      {TL1:threads`lookup X3 N2 (thread/ X15 (X16 (read (lit (object/ O)) F)))}
      {L1:loc* exprk exprk ([x:term exprk] X16 x)}
      {A:atomic-lhs* exprk (read (lit (object/ O)) F)}
      {ML:lookup X2 O (objs/ X4 X5 X6)}
      {NFL:normal-fields`lookup X4 F (normal-contents/ N3 N4)}
      {XTL:threads`lookup X3 N2 (thread/ X7 X8)} {XSF:not-member X7 N3}
      {FE:fulleval X1 N5 (state/ X9 X10) (state/ X11 X12)}
      {ESG:eval-seq-get* X1 N5 N1 (state/ X2 X3) (state/ X9 X10)
              (state/ X11 X12) ES N6 FE}
      {WA:access* writek X10 N5 O F} {XPK:process-knowledge X12 N5 X14}
      {XSM:set`lookup X14 N3 unit/}
      {NHBP:hb-potential?* X1 N1 (state/ X2 X3) ES N6 N2 false}
wk-is/L ES 
       (access/read
          (ready/ (read (lit (object/ O)) F) TL1 L1 A))
       ML NFL XTL XSF FE ESG WA XPK XSM NHBP
       (incorrectly-synchronized/W 
          (eval-seq/+ ESN 
             (fulleval/ _ (lit (object/ O')) TL1N L1 
                (eRead ML' NFL' TL1N K>Z) TL1N TU1N))
          (eval-seq-get/ (eval-seq-includes/> ESI'))
          (eval-seq-get/ eval-seq-includes/=) WA'
          (access/read
             (ready/ (read (lit (object/ O)) F) TL1N L1 A))
          NHB')
    <- no-know-eval-seq-exists ES _ (no-know-state/ NM NTS) ESN ESM
        (state-match/ MM TSM)
    <- eval-seq-get-respects-match ESG ESM _ _ _ (eval-seq-get/ ESI') FEM
    <- mem-lookup-respects-match ML MM _ ML' (objs-match/ NFM _ _)
    <- no-know-mem-lookup-implies-no-know-contents ML' NM (no-know-objs/ NNF _ _)
    <- normal-fields-lookup-respects-match NFL NFM _ NFL'
    <- no-know-normal-fields-lookup-implies-no-know-contents NFL' NNF Z=W
    <- threads-lookup-respects-match TL1 TSM _ TL1N
    <- no-know-threads-lookup-implies-no-know-contents TL1N NTS Z=K
    <- set`member-respects-eq (set`lookup/= nat`eq/) Z=K Z=W K>Z
    <- threads`update-total TU1N
    <- hb-potential?-respects-match NHBP ESM NHBP'
    <- not-hb-potential-realized NHBP' _ (non-sw2-fulleval/ non-synch2-atomic/read) NHB'
    <- wk-is/L2 WA TSM WA'.

Now, we get new errors because the variables only occurring in the body of the proof may depend on the explicitly typed ones, and the type inference engine does not do this. To solve this, use Control-C Control-L to highlight the unbound variables, and then list them all (with unspecified type) right after the other variables. Don't list one twice! You can use Control-C Control after adding a few to see what remains. Eventually one has

- : {X1} {N1:nat} {X2:map} {X3} {N2:nat} {O:nat} {F:nat} {X4}
      {X5} {X6:lock-contents} {N3:nat} {N4:nat} {X7} {X8:term exprk}
      {N5:nat} {X9:map} {X10} {X11:map} {X12} {N6:nat}
      {X14} {ES:eval-seq X1 N1 (state/ X2 X3)} {X15}
      {X16:term exprk -> term exprk}
      {TL1:threads`lookup X3 N2 (thread/ X15 (X16 (read (lit (object/ O)) F)))}
      {L1:loc* exprk exprk ([x:term exprk] X16 x)}
      {A:atomic-lhs* exprk (read (lit (object/ O)) F)}
      {ML:lookup X2 O (objs/ X4 X5 X6)}
      {NFL:normal-fields`lookup X4 F (normal-contents/ N3 N4)}
      {XTL:threads`lookup X3 N2 (thread/ X7 X8)} {XSF:not-member X7 N3}
      {FE:fulleval X1 N5 (state/ X9 X10) (state/ X11 X12)}
      {ESG:eval-seq-get* X1 N5 N1 (state/ X2 X3) (state/ X9 X10)
              (state/ X11 X12) ES N6 FE}
      {WA:access* writek X10 N5 O F} {XPK:process-knowledge X12 N5 X14}
      {XSM:set`lookup X14 N3 unit/}
      {NHBP:hb-potential?* X1 N1 (state/ X2 X3) ES N6 N2 false}
      {ESN} {O'} {TL1N} {ML'} {NFL'} {K>Z} {ESI'} {WA'} {TU1N} {NHB'}
        {NM} {NTS} {ESM} {MM} {TSM} {NFM} {NNF} {Z=W} {Z=K} {NHBP'}
wk-is/L ES 
       (access/read
          (ready/ (read (lit (object/ O)) F) TL1 L1 A))
       ML NFL XTL XSF FE ESG WA XPK XSM NHBP
       (incorrectly-synchronized/W 
          (eval-seq/+ ESN 
             (fulleval/ _ (lit (object/ O')) TL1N L1 
                (eRead ML' NFL' TL1N K>Z) TL1N TU1N))
          (eval-seq-get/ (eval-seq-includes/> ESI'))
          (eval-seq-get/ eval-seq-includes/=) WA'
          (access/read
             (ready/ (read (lit (object/ O)) F) TL1N L1 A))
          NHB')
    <- no-know-eval-seq-exists ES _ (no-know-state/ NM NTS) ESN ESM
        (state-match/ MM TSM)
    <- eval-seq-get-respects-match ESG ESM _ _ _ (eval-seq-get/ ESI') FEM
    <- mem-lookup-respects-match ML MM _ ML' (objs-match/ NFM _ _)
    <- no-know-mem-lookup-implies-no-know-contents ML' NM (no-know-objs/ NNF _ _)
    <- normal-fields-lookup-respects-match NFL NFM _ NFL'
    <- no-know-normal-fields-lookup-implies-no-know-contents NFL' NNF Z=W
    <- threads-lookup-respects-match TL1 TSM _ TL1N
    <- no-know-threads-lookup-implies-no-know-contents TL1N NTS Z=K
    <- set`member-respects-eq (set`lookup/= nat`eq/) Z=K Z=W K>Z
    <- threads`update-total TU1N
    <- hb-potential?-respects-match NHBP ESM NHBP'
    <- not-hb-potential-realized NHBP' _ (non-sw2-fulleval/ non-synch2-atomic/read) NHB'
    <- wk-is/L2 WA TSM WA'.

Now when you check the declaration (Control-C Control-D), the coverage error will occur as a type error. Here it shows up that WA is constrained too much.

The details are irrelevant except to show that even (especially!) long proofs can use this technique.

Summary

If you encounter an input coverage error on a case you thought you covered, the problem is most likely that the constant you wrote has a less general type than you think. It can be helpful to read the type of constant, looking for variables that Twelf unified. Additionally, you can start introducing type annotations on the inputs to prevent Twelf from unifying the implicit parameters; this turns the input coverage error into a type error on the constant itself. If you comment out parts of the constant, such as outputs or later premises, you can find the exact premise that causes the type error, and get Twelf to give a more specific error message. This will help you figure out what mistake you made.

Unusual Situations

The input coverage checker has limitations. This section describes some of them. You won't encounter these symptoms unless you are using higher-order judgments.

Nontermination

Occasionally, the input coverage checker does not terminate. If chatter is set to six, you see the infinite loop progressing. Otherwise, it simply hangs. This happens sporadically when the input coverage checker attempts to split on a variable of higher-order (functional) type. It usually happens when there is a coverage error. Use chatter 6 to determine where the problem is.

Inactive Splits

Occasionally, the coverage checker "refuses" to split on a variable (i.e. enumerate its cases) even though doing so would determine that there are no cases to consider, in other words that coverage is not needed. In this case the coverage checker will try other variables until it runs out of candidates and gives up yielding (often) a long list of unhandled cases. This symptom can be verified by setting chatter to 7 in which the message "Inactive Split" is echoed. An inactive split is a split that will not be chosen because one of its cases causes unification to fail with unsolved constraints.

This situation can be solved by preventing unification of the higher-order terms (e.g., (F X) = (G X)) through the introduction of a trivial (syntactic) equality predicate. Make sure that this predicate is listed before the variable that needs to be split in your meta-theorem. Otherwise, the coverage checker will split the equality predicate and re-introduce the problem.


Read more Twelf tutorials and other Twelf documentation.