calc statements

[mtzguido]

This PR introduces support for calc statements, similar to the ones in Dafny, as asked for in issue #1549 by @parno.

Here's a brief overview of how they work:

• The FStar.Calc module defines a set of combinator to structure calculational proofs, and a way to eliminate them as Lemmas (which ensures they will be erased by extraction).

• A calculational proof is a sequence of expressions (of some type t) related by steps plus a top-level relation (i.e. a term of type t -> t -> Type0). Each step is composed of a relation and a justification (a proof that the expressions are indeed related). For instance:

let _ = 
  calc (>) {
    3;
    > { () }
    2;
    == { () }
    1 + 1;
  }

Is a proof that 3 > 1 + 1. This succeds since
a) 3 > 2 (with proof ())
b) 2 == 1 + 1 (with proof ())

and c) forall x,y,z, if x > y == z, then x > z.

This last condition is currently sent to the SMT solver.

• Justifications inside {} can be omitted in they are (). Internally, all justifications are thunked by the desugarer.

• All relations r are expanded to fun x y -> r x y <: Type0 in order to accept boolean operations like (>) : int -> int -> bool and properly obtain the b2t coercion where needed.

• Justifications and steps are not in "logical scope" of each other: admitting a step should not affect others. However, everything is encoded in a single VC for now. We might want to split some parts of it out.

[msftclas]

All CLA requirements met.

[nikswamy]

What's this remark about? In the next line, you correctly add FStar.Calc

[mtzguido]

I forgot to remove the comment :)

[nikswamy]

Looks great overall.

Couple of suggestions:
-- Record this briefly in CHANGES.md
-- A wiki page on calc would be great

Thanks!

Please merge once you're able to sign the cla.

[aseemr]

Can this type be abstract? We will also have to make calc_init and calc_step as abstract.

[aseemr]

Curious to understand how this works. To satisfy the precondition of the lemma, how is calc_chain_compatible proven? As in, would it involve unfolding of the recursive definition calc_chain_related by Z3 (and thus constrained by the fuel setting)?

[mtzguido]

Ah, yes, I forgot I wanted to add a normalize_term to this so the unfolding would happen in the normalizer, leaving Z3 only with a quantification to be proven. Without that, large chains do fail. I'm playing with that now.

[nikswamy]

This pattern may be useful: hacl-star/hacl-star@7623202#r31557851

[aseemr]

You can also mark calc_chain_compatible as opaque_to_smt.

[aseemr]

A small, say 2 steps example, that shows the desugaring in the comments would be useful here.

[mtzguido]

Yes, will add!

[nikswamy]

Maybe a version of the same program written without any syntactic sugar?

[aseemr]

We could add a pattern here calc_chain_related rs x y (Z3 could also be picking the same automatically).

[aseemr]

Looks good to me too. Added a few comments. Thanks!

[nikswamy]

This fails pointing to the calc_chain_compatible precondition of finish

module SeqCalc
open FStar.Mul
open FStar.Calc
open FStar.Preorder
open FStar.Seq

let seq_assoc_4 (s1 s2 s3 s4: seq 'a)
  : Lemma ( ((s1 @| s2) @| s3) @| s4 ==
              s1 @| (s2 @| (s3 @| s4)))
  = calc (==) {
      ((s1 @| s2) @| s3) @| s4;
      == { admit() }
      s1 @| (s2 @| (s3 @| s4));
    }

[nikswamy]

Would be great to test calc proofs in the wild.

For example, here's a proof that could have benefited from it:
https://github.com/project-everest/hacl-star/blob/master/secure_api/aead/Crypto.AEAD.Invariant.fst#L832

One thing to check, as also mentioned by @parno, is that error messages are reported properly for each failing step of a calc proof, rather than blaming the calc proof as a whole.

[parno]

FWIW, here's an example of a calc-style proof in the "wild":
https://github.com/project-everest/hacl-star/blob/_fast_mul/vale/code/crypto/sha/SHA_helpers.fst#L732
The calc steps are spelled out in the comments, with the appropriate lemmas called in between.

[mtzguido]

Added a wiki page and a paragraph in CHANGES.md. I have some unifier optimizations I was trying but 1) they don't seem to help a whole lot 2) the better normalization of the compatibility VC (7b5bfb9) seems good enough 3) I got a few regressions that I need to stare at. I think this can be merged as it is now.

[nikswamy]

please go ahead and merge.

[mtzguido]

Will do after refreshing the snapshot.

[parno]

Sweet!

[mtzguido]

@parno I'm also moving the proof you mentioned to calc-style. It's taking me a bit, it seems to be working---even with nesting, which I should have tried beforehand but I was glad to see it worked on a first try :).

[parno]

Nice! I'm running the Vale regression suite against the new version of F*, in the hopes of upgrading today.