[fstar-club] Slack forum open to all

[Nikhil Swamy via fstar-club]

Dear all,

We recently opened up a slack forum https://everestexpedition.slack.com/ that 
was previously used mainly by members of Project Everest. Many F* experts, 
including the F* developers, hang out there regularly---it's a good place to 
ask questions about F* as well as many projects that use it, including things 
like HACL*, EverCrypt, EverParse, Kremlin, Steel, etc.

You might be interested to sign up by going to https://aka.ms/JoinEverestSlack.

Best wishes,
Nik


Sent from Outlook
___
fstar-club mailing list
fstar-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/fstar-club

Re: [fstar-club] fibonacci_greater_than_arg solution

[Nikhil Swamy via fstar-club]

Hi Michael,

Thanks for your note.

The explanation for that proof isn't quite right---it supposes that Z3 
automatically proves that fibonacci(n) >= 1, which it cannot do, since that 
requires an induction.

Instead, the proof goes something like what's shown below. Thanks to Aseem for 
coming up with this explanation.

I'll update the tutorial accordingly.

Best wishes,
Nik

val fibonacci : nat -> Tot nat
let rec fibonacci n =
  if n <= 1 then 1 else fibonacci (n - 1) + fibonacci (n - 2)

val fibonacci_greater_than_arg : n:nat{n >= 2} -> Lemma (fibonacci n >= n)
// BEGIN: FibonacciGreaterThanArgProof
let rec fibonacci_greater_than_arg n =
  match n with
  | 2 -> ()
  | _ -> fibonacci_greater_than_arg (n-1)

(*
 The proof uses the induction hypothesis:
   forall x, 2 <= x < n ==> fibonacci x >= x

 Z3 proves the base case, when n=2.

 Our remaining goal is to prove that for n >= 3
  fibonacci n >= n or equivalently fibonacci (n-1) + fibonacci (n-2) > n

 From the induction hypothesis we have,
   fibonacci(n - 1) >= n - 1

 To conclude, it suffices to prove that prove that fibonacci(n - 2) >= 1.

 Z3 is able to prove this as follows:

 We have: fibonacci(n - 1) = fib (n - 2) + fib (n - 3) >= n - 1 > 1

 Assume, for contradiction, that fibonacci (n - 2) = 0.
   Then fibonacci (n - 3) > 1. (H)

   If n = 3, then fibonacci(n - 2) = fibonacci(1) = 1. Which is a contradiction.

   If n > 3, then
 0 = //by assumption
 fibonacci (n - 2) = //by definition
 fibonacci (n - 3) + fibonacci (n - 4) >= //since fibonacci(n-4) : nat >= 0
 fibonacci (n - 3) > //by (H), above
 1

   So, we have a contradiction.

 So fibonacci (n - 2) >= 1
*)

// END: FibonacciGreaterThanArgProof



Sent from Outlook


From: fstar-club  on behalf of 
Michael Delorimier via fstar-club 
Sent: Monday, January 4, 2021 10:09 PM
To: fstar-club@lists.gforge.inria.fr 
Subject: [fstar-club] fibonacci_greater_than_arg solution

In the solution to fibonacci_greater_than_arg in the tutorial 
https://nam06.safelinks.protection.outlook.com/?url=http%3A%2F%2Ffstar-lang.org%2Ftutorialdata=04%7C01%7Cnswamy%40microsoft.com%7Ccaf43eaff1694c43ddf108d8b15efe8e%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637454369355635374%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000sdata=MtLggjQZM0AeVR%2F60vFSod7oATBbt9rbZpK6DDHDp3c%3Dreserved=0
 it looks like

For fibonacci (n-1) we use the property
   forall x, fibonacci x > 1

should be changed to

For fibonacci (n-2) we use the property
   forall x, fibonacci x > 1

Nice tutorial by the way.
-Michael
___
fstar-club mailing list
fstar-club@lists.gforge.inria.fr
https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Flists.gforge.inria.fr%2Fmailman%2Flistinfo%2Ffstar-clubdata=04%7C01%7Cnswamy%40microsoft.com%7Ccaf43eaff1694c43ddf108d8b15efe8e%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637454369355635374%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000sdata=69Y%2FWoYQkTjMvZfckSnDfu0BdvAgnR0w6Gg0ydPfigw%3Dreserved=0
___
fstar-club mailing list
fstar-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/fstar-club

Re: [fstar-club] Execute F* using ocaml/opam package

[Nikhil Swamy via fstar-club]

Hello Marius,

Some responses to your questions are below.


Sent from Outlook


From: fstar-club  on behalf of Marius 
Melzer via fstar-club 
Sent: Tuesday, September 1, 2020 3:00 PM
To: fstar-club@lists.gforge.inria.fr 
Subject: [fstar-club] Execute F* using ocaml/opam package

Hi,

I'm just starting off with Fstar and I have a little bit setup problems.
I installed fstar via opam and now I'm trying to get my project to
compile via the ocaml code generation.

1) I exported to ocaml via: fstar.exe --codegen OCaml project.fst (this
generated a lot of "Pattern uses these theory symbols or terms that
should not be in an smt pattern: ..." warnings, is that ok to ignore?
What do they mean exactly?). This anyways generates a bunch of ocaml files.
The warning relates to the use of quantifiers encoded to the SMT solver.

You can read more about it here:
https://github.com/FStarLang/FStar/wiki/Quantifiers-and-patterns
and
http://fstar-lang.org/tutorial/tutorial.html#sec-smt-lemmas--bridging-the-gap-between-intrinsic-and-extrinsic-proofs

It is safe to ignore this warning, at least as far as code extraction is 
concerned.
However, the improper use of quantifier patterns can impact proof automation 
and stability.

2) I now want to compile the ocaml code and must as I read include the
ml support library. The library is part of the installed opam package,
at least this exists: ~/.opam/4.07.1/lib/fstarlib/, but an "ocamlfind
ocamlopt -package fstarlib *.ml" only gets me ocamlfind: Package
`fstarlib' not found - why doesn't this work and how can I get to a
runnable executable here?
Take a look at examples/hello/Makefile. It provides a template that you can 
follow for an F* project extracted to OCaml.

In particular, it does (simplifying it a bit):

fstar.exe --odir out --codegen OCaml --extract 'Hello' Hello.fst

OCAMLPATH="../../bin" ocamlfind opt -package fstarlib -linkpkg -g  out/Hello.ml 
-o hello.exe

./hello.exe

It looks like your invocation of ocamlfind may be missing an OCAMLPATH setting?

Hope that helps,
Nik


I realize that this might rather be an ocaml question and if this is the
wrong place to ask it, please let me know then I will try to find
another mailing list to ask about it.

Thanks in advance,
Marius
___
fstar-club mailing list
fstar-club@lists.gforge.inria.fr
https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Flists.gforge.inria.fr%2Fmailman%2Flistinfo%2Ffstar-clubdata=02%7C01%7Cnswamy%40microsoft.com%7C633dbc379e324b9270cd08d84f05c374%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637346233897233895sdata=NUEuPNwoMPCngt8ZcijJfklweC7nPd5Nf24jYZpsaOg%3Dreserved=0
___
fstar-club mailing list
fstar-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/fstar-club

Re: [fstar-club] FStar school

[Nikhil Swamy via fstar-club]

And also one covering Meta-F* (tactics etc.) in Buenos Aires in July
https://eci2019.dc.uba.ar/cursos.html
-Nik

> -Original Message-
> From: fstar-club  On Behalf Of 
> Catalin
> Hritcu via fstar-club
> Sent: Tuesday, April 2, 2019 1:02 PM
> To: Marc Gourjon 
> Cc: FStar Club 
> Subject: Re: [fstar-club] FStar school
> 
> Hi Marc,
> 
> Not sure about the "in depth" part, but otherwise there are 2 summer schools
> that will have F* courses coming up soon:
> 
> * The Oregon Programming Languages Summer School, Eugene, OR, USA
> - Application Deadline: April 15, School: June 17-29
> 
> * Summer School on Verification Technology, Systems, and Applications,
> Luxembourg
> - Application deadline: 10 May, School: 1-5 July
> 
> Cheers,
> Catalin
> 
> On Tue, Apr 2, 2019 at 9:46 PM Marc Gourjon via fstar-club  c...@lists.gforge.inria.fr> wrote:
> >
> > Dear FStar-experts,
> > will there be another occasion to learn Fstar interactively with you?
> > Something like the EUTypes meeting in Aarhus last year.
> >
> > An in-depth session would be really beneficial (at least to me),
> > despite the good amount of papers, tutorials, wiki and zulip assistance!
> > Maybe Tactics benefit from some special treatment as well ;)
> >
> > KR
> > Marc
> >
> > --
> > Marc Gourjon
> > Security in Distributed Applications
> > Hamburg University of Technology (TUHH)
> > https://nam06.safelinks.protection.outlook.com/?url=http%3A%2F%2Fwww.t
> >
> uhh.de%2Fsvadata=02%7C01%7Cnswamy%40microsoft.com%7C5d9990
> 14fa484
> >
> e038d5208d6b7a6186c%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C1%
> 7C63689
> >
> 8321354717259sdata=AFET8V63YJRJS%2Bb%2B6P1cuqdmN5fVed7OwD
> Mqq1gRbv
> > I%3Dreserved=0
> ___
> > fstar-club mailing list
> > fstar-club@lists.gforge.inria.fr
> > https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Flist
> > s.gforge.inria.fr%2Fmailman%2Flistinfo%2Ffstar-clubdata=02%7C01%7
> >
> Cnswamy%40microsoft.com%7C5d999014fa484e038d5208d6b7a6186c%7C72
> f988bf8
> >
> 6f141af91ab2d7cd011db47%7C1%7C1%7C636898321354717259sdata
> =ZiVq8T8
> >
> td4hr%2F0jZeSh71yY%2F6Xq%2FA%2BAjkrX%2BJsZoslg%3Dreserved=0
> ___
> fstar-club mailing list
> fstar-club@lists.gforge.inria.fr
> https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Flists.gfo
> rge.inria.fr%2Fmailman%2Flistinfo%2Ffstar-
> clubdata=02%7C01%7Cnswamy%40microsoft.com%7C5d999014fa484e
> 038d5208d6b7a6186c%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C1%7
> C636898321354717259sdata=ZiVq8T8td4hr%2F0jZeSh71yY%2F6Xq%2F
> A%2BAjkrX%2BJsZoslg%3Dreserved=0
___
fstar-club mailing list
fstar-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/fstar-club

Re: [fstar-club] Noob questions

[Nikhil Swamy via fstar-club]

Dear Christian,

Thanks for your interest in F*!

I respond to some of your questions quite broadly below. I’ll let others 
respond further with more specifics.

-Nik

From: fstar-club  On Behalf Of 
Christian Nyumbayire via fstar-club
Sent: Wednesday, January 9, 2019 6:42 PM
To: fstar-club@lists.gforge.inria.fr
Subject: [fstar-club] Noob questions

Hi,
I'm a programmer working in crypto (both cryptography and cryptocurrency). I've 
learned about KreMLin from the Hacl slides and youtube video. I got quite 
interested in FStar since then. I'm trying to learn more and figure out how I 
could use it on a daily basis (if possible/advisable). So far I can read the 
hacl mitls and I'm quite reassured that Meta FStar or things I still don't grok 
properly are not generally used. My public code is mostly in Rust. I have 
really a lot of questions but these ones are the most pressing:

  1.  What is the best way to extend the fstar library? I was thinking about 
I/O in particular.[NS] fsa
[NS] We are happy to consider pull requests for library improvements. Please 
see CONTRIBUTIONS.md for some general guidelines.
About IO in particular: there are many choices for how best to model it with 
various tradeoffs. As a baseline, one can assume an effectful operation and 
provide an implementation for it in whatever target language you’re interested 
in running your program, e.g., OCaml, C etc.

  1.  Is there any reason there is no stdin in kremlib, even as a channel?
  2.  What is the proper way to extend kremlib? (I've seen the include)
  3.  Anyone working on a builder to supplant the actual use of Makefiles? E.g. 
in ocaml? Could be useful for a package manager in a second phase.
[NS] No one is working on this, as far as I know. We rely heavily on F*’s 
dependence analysis (fstar –dep) and Makefiles for builds currently. We are not 
necessarily looking to remove our reliance on Make, but are open to proposals. 
A package manager would be useful, but, as you note, we are some ways off from 
that as yet.

  1.  Anyone working on the docs?
[NS] The tutorials on F* and Low*, the wiki and our papers are what we have so 
far as documentation. We expect to write more tutorials, including one for 
Meta-F* in the near future. We often discuss consolidating all our existing 
documentation (such as it is) into a manual, but no one is working on that yet.

  1.  Are there community groups for those and other tasks?
[NS] We have an fstar channel on functionalprogramming.slack.com: I encourage 
you to sign up there and ask questions. FYI, many of us who work heavily on F* 
are members of a private slack group.
Slack is nice for some reasons, but it isn’t great especially because it 
doesn’t preserve history very well. We are discussing alternatives, but have 
not settled on anything yet.
Thanks again,
Nik
Quite a lot in retrospective...

All the best,
Christian Nyumbayire
___
fstar-club mailing list
fstar-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/fstar-club

Re: [fstar-club] Consistency of F-star ?

[Nikhil Swamy via fstar-club]

Hi Bas,

We've made several attempts at formalizing various fragments of F*, none of 
which establish consistency of the full language (unsurprisingly).

Our most recent attempt is in a paper at POPL 2017: 
https://www.fstar-lang.org/papers/dm4free/

There, we present a calculus called Explicitly Monadic F* (EMF*) which includes 
the pure fragment of F*, with dependent types, refinement types and 
user-defined monadic effects. EMF* excludes many F* features too (especially 
the following, which are particularly relevant for consistency):

1. inductive types and pattern matching
2. F*'s let-rec primitive (and its semantic termination check)
3. a typing rule that supports type conversion based on provable equality
4. divergence encapsulated in another effect
5. the encoding of F*'s logic to first-order logic provided by an SMT solver

For this limited EMF* calculus, we have a syntactic metatheory proving total 
correctness of the WP-based program logic we derive for effectful terms. 
Extending EMF* at least with features 1, 2, and 3 above and studying its 
consistency would be very interesting ... well, at least to the few of us who 
work on F*.

That said, the main theorem of this POPL '17 paper is to establish the 
correctness of a CPS-based transformation to derive WP calculi from definitions 
of a monad. This is done by a logical relations proof on EMF*.

Other papers have attempted to study some of these other consistency-related 
features of F* in slightly different settings: 
-- https://www.fstar-lang.org/papers/mumon/  this one includes a proof of 
normalization of a small calculus ("pico F*") with recursion, refinement types 
and our termination check
-- This short paper 
https://hatt2016.inria.fr/files/2016/06/HaTT_2016_paper_1-5.pdf formalizes a 
core of F*'s encoding to first-order logic 

Aside from all this, there's the question of the correctness of F*'s 
implementation: of course, F* is under active development and we find, fix and 
(sadly) introduce correctness bugs from time to time. We hope someday to 
revisit our work on "self-certification" 
(https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/popl2012-paper211.pdf)
  and apply a technique like it to the current implementation of F*.

Hope that helps,
Nik

> -Original Message-
> From: fstar-club  On Behalf Of Bas
> Spitters via fstar-club
> Sent: Friday, June 29, 2018 3:30 AM
> To: fstar-club@lists.gforge.inria.fr
> Subject: [fstar-club] Consistency of F-star ?
> 
> What are the current conjectures, thoughts about the consistency/semantics
> of F*?
> 
> Could you point me to a paper I should read?
> 
> Thanks,
> 
> Bas
> ___
> fstar-club mailing list
> fstar-club@lists.gforge.inria.fr
> https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Flists.gf
> orge.inria.fr%2Fmailman%2Flistinfo%2Ffstar-
> clubdata=02%7C01%7Cnswamy%40microsoft.com%7C428fa932a4c04
> d1ce84708d5ddabaec4%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%
> 7C636658651809180794sdata=EEKoy3UGxk%2BOKuLGPDTQb%2F0AZ
> %2FhMKcc7PzI09bvk5Og%3Dreserved=0
___
fstar-club mailing list
fstar-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/fstar-club