Proving non-terminating functions in F*

[Caroline-xinyue]

I am an undergraduate senior writing a thesis on the dual comparison between Dependent Haskell and F. I am specifically interested in exploring how F proves properties about non-terminating(divergent) functions. To begin with, I chose an educational example proving div (mult a b) a = b, where div is defined to be divergent with zero divisors. I have trouble proving the above property for the divergent div, since div cannot be directly lifted to logic and be used in the post-condition of the peanoDivPf proof. At POPL, with the help from Ramananandro, we together came up with a work-around solution. I pasted the 3 major functions below and attached the full implementation zeroPeanoDivision.fst in Gist.

val div_terminating: a:peano -> b:peano{toNat b > 0} -> Tot (c:peano)
(decreases (toNat a))
let rec div_terminating a b = if a = Zero then Zero else plus (div_terminating (minus a b) b) (Succ Zero)

val div: a:peano -> b:peano -> Div (c:peano) (requires True) (ensures (fun y -> toNat b > 0 ==> y == div_terminating a b))
(decreases (toNat a))
let rec div a b = if a = Zero then Zero
                  else let denom = (div (minus a b) b)
                       in plus denom (Succ Zero)

val peanoDivPf: a:peano -> b:peano{toNat b > 0} -> Lemma (ensures (div_terminating (mult a b) b == a))
let rec peanoDivPf a b = match a with
  | Zero    -> ()
  | Succ a' -> plusMinus (mult a' b) b;
               peanoDivPf a' b;
               plusSucc a' Zero;
               plusZero a'

Though the above proof implementation successfully discharges, it requires programmers to manually implement the terminating version of div. In reality beyond this educational example, however, programmers can't easily prove termination of any divergent functions.

Per offline discussion with @nikswamy , we found that F currently have limited ability to deal with non-terminating function extrinsically. It seems that through the above example, F also might not fully support proving properties on non-terminating functions intrinsically either. I am wondering if there are ways to discharge the proof without requiring the knowledge that div terminates as long as divisor is nonzero. I would also be interested to discuss the methodologies F* take in supporting non-terminating functions in general?

Thanks all in advance! Xinyue(Elise)

[nikswamy]

Hi Xinyue,

F* indeed does not extrinsic proofs of non-terminating computations.

However, F* includes a Hoare logic for partial correctness of non-terminating computations (which may include other effects as well). You can use this logic to do intrinsic proofs of partial correctness.

One way to structure such a proof is to follow the style of your example: i.e., prove the non-terminating computation partially equivalent to a total variant of the same computation (e.g., on a restricted domain). But this is by no means the common approach.

Usually, with partial correctness verification, one aims to find invariants that hold inductively of loops (including recursive functions) that appear in your program. Hoare logics of this form are generally designed to be "relatively complete", i.e., so long as we can decide the validity of individual assertions, we can use the Hoare logic to decide partial correctness specifications. A quick search for "Hoare logic completeness" led me to these simple lecture notes which you may find useful: https://www.cs.cornell.edu/courses/cs4110/2010fa/lectures/lecture09.pdf

[Caroline-xinyue]

Thanks for the detailed answer.

Just a quick update: I continue to work on the Simply Typed Lambda Calculus and attempt to prove the equivalence between multistep and bigstep evaluators. As proving totality for multistep and bigstep is a challenge, I am curious to see if the equivalence proof is possible. The theoretical result is based on Benjamin Pierce's Types and Programming Languages and Software Foundations. I will follow up with the findings later.

[Caroline-xinyue]

Hi F* developers,

In the "Dependent Types and Multi-monadic Effects in F" paper, it's stated at the end of pp.262 that "Of course, with more effort, one can also prove that an evaluator for the simply typed lambda calculus is normalizing. We provide several such proofs online, e.g., using hereditary substitutions." It seems to me that F is able to define a multi-step evaluator with effect Tot. Following the link, I found some development in examples/metatheory/HereditarySubst.fst on stratified_last branch that might illustrate a terminating multi-step evaluator. Yet I didn't find a complete proof there; only norm.fst in the attic folder defined multi and attempts to prove its halting property. The definition also seems to be relationally defined as in Coq, instead of functional as usual in F*.

I am wondering if I find in the wrong place or if the normalization proof for multi-step evaluator is still an ongoing project?

Any help or insight is highly appreciated.

Sincerely, Xinyue

[nikswamy]

@ckeller : Do you remember the status of this?

[nikswamy]

From a quick glance: https://github.com/FStarLang/FStar/blob/stratified_last/examples/metatheory/HereditarySubst.fst#L252

Looks like this is the normalizer with its type showing that it is total. @Caroline-xinyue does this not satisfy your needs?

Of course, the example has not been maintained and carried along with F* master, but I don't see a reason why it couldn't.

[Caroline-xinyue]

Thanks so much! I will look into this code in more details. May I ask what's nf stands for in this function? I think it stands for Normalized Form and a quick look suggests that nf seems to be the bigstep evaluator instead of multistep. Then, can we use the same hereditary substitution method to prove the normalization of multistep evaluator. Eventually, I want to verify the equivalence of multistep and bigstep evaluators to explore how F* approaches verifications on divergent functions or functions whose totality is super hard to prove.

Also, from my explorations the past few weeks, it seems like any functions marked as Dv cannot be bring into logic and reasoned about in pre- and post-conditions as in requires and ensures. Similarly, per thread discussion before, Dv functions cannot be verified in most verifiers extrinsically through lemmas. Therefore, I am wondering, in cases like Simply Typed Lambda Calculus, as both multistep and bigstep are hard to be verified as normalizing if not impossible, do we generally use dependent types to encode the specifications and verify relevant properties of interests? If not, would that make our language incomplete and less applicable as a general-purpose language.

Thanks! Xinyue(Elise)

[Caroline-xinyue]

Hi @nikswamy ,

Sorry to bother again! One last question --------

I am trying to explain the reason why we have trouble supporting extrinsic proofs of non-terminating functions in F*. Specifically, in the simple Peano Division example below:

[1]val division: a:peano -> b:peano{toNat b > 0} -> Tot (c:peano)
(decreases (toNat a))
let rec division a b = match a with
  | Zero   -> Zero
  | Succ _ -> if (toNat a < toNat b) then Zero else Succ (division (minus a b) b)

val peanoDivPf: m:peano -> n:peano{toNat n > 0} -> Lemma (ensures (division (mult m n) n == m))
let rec peanoDivPf a b = match a with
  | Zero    -> ()
  | Succ a' -> plusMinus (mult a' b) b;
               peanoDivPf a' b;
               plusSucc a' Zero;
               plusZero a'

If I simply change the type signature of division from Tot to Dv(also removing the decreases termination metric), i.e. val division: a:peano -> b:peano{toNat b > 0} -> Dv (c:peano), the F* compiler fails to type check. It returns error saying that a ghost expression is expected, but got an expression of with effect "DIV".

I was wondering if the compiler simply disallows any divergent functions with effect Dv in type-level propositions? If so, what are we trying to protect by making this design decision. If not, what might be the reason why we never try to evaluate the postcondition (division (mult m n) n == m that could actually terminate, like in this above case.

Context on Dependent Haskell: Since Dependent Haskell's type safety does not depend on termination checking, it simply does not care about termination. The approach Dependent Haskell takes is to try to evaluate the promoted type-level function division. As a result, the compiler either proves the potentially-divergent properties or it loops forever. In this case, since the property (a*b)/b = a with b > 0 we are trying to prove in peanoDivPf actually terminates, DH will terminate with a correct proof.

In general, only when a program type checks and actually terminates can the program correctness be verified. Even though the actual verification is sometimes defer to run time, Dependent Haskell's approach directly supports proving potentially divergent functions such as the equivalence of bigstep and multistep evaluators in STLC (without the need for hereditary substitutions, which I actually don't fully understand).

Thanks, Xinyue

[ckeller]

Hi @Caroline-xinyue and @nikswamy

Sorry for answering really late, I missed the alert.

Regarding hereditary substituions: the mutually recursive functions napp, substNF, substSp and appNfSp are recursively applying small-step β-reduction as you can see in the definition of napp: napp _ _ _ (NLam _ f) u reduces to f[0 <- u] (bound variables are represented with De Bruijn indices). You can find more details in the paper from which this F* implementation is inspired.

Regarding your last question: in the logic, one can only call total functions, otherwise one could derive False in F*. Indeed, the following is provable:

val unsound: int -> Div x:int{0 == 1}
let rec unsound x = unsound x

and you clearly do not want to use unsound in the logic.