Stack Overflow
Stack Overflow

Questions tagged [fstar]

F* (pronounced F star) is an ML-like functional programming language aimed at program verification.

F* (pronounced F star) is an ML-like functional programming language aimed at program verification. Its type system includes polymorphism, dependent types, monadic effects, refinement types, and a weakest precondition calculus. Together, these features allow expressing precise and compact specifications for programs, including functional correctness and security properties. The F* type-checker aims to prove that programs meet their specifications using a combination of SMT solving and manual proofs. Programs written in F* can be translated to OCaml or F# for execution.

For more information see the F* language homepage.

30 questions
23
votes
1 answer

what's the difference between lean, f*, and dafny?

They are from Microsoft and seem like they are proof assistants? Besides syntactical differences are there practical aspects that make them different from one another (say ability to do automation, expressive power, etc)? I am new to formal…
JRR
  • 6,014
  • 6
  • 39
  • 59
4
votes
1 answer

Does F* support linear types?

According to Wikipedias article about substructural type-systems, F* support some kind of linear types. Is this true? If so, how? I can't find any information about it in the F* tutorial.
Olle Härstedt
  • 3,799
  • 1
  • 24
  • 57
4
votes
2 answers

How to declare a hasEq constraint?

I'm just starting out with F*, by which I mean I've written a few lines along with the tutorial. So far it's really interesting and I'd like to keep learning. The first thing I tried to do on my own was to write a type that represents a non-empty…
Richiban
  • 5,569
  • 3
  • 30
  • 42
3
votes
0 answers

Is there an proof search functionality for F*?

As we know, we have "auto" (proof search) in Agda (Ctrl+c Ctrl+a in Emacs) as well as Idris as well as Coq, but when I was digging into F*'s Emacs mode, I failed to find a similar functionality. Does F* have this feature? If so, how can I use it?
ice1000
  • 6,406
  • 4
  • 39
  • 85
3
votes
0 answers

How to prove statements of the form forall x. phi x in F*?

I have just started learning F*, going through the tutorial. One of the exercises there is to prove that the reverse function on lists is injective. Since this follows from the fact that involutions are injective I would like to express that fact…
Slawomir K.
  • 146
  • 4
3
votes
1 answer

Compile issue with FStar and mono

I'm trying to compile FStar language on latest Ubuntu and mono. GitHub repo provides some build instruction, but it doesn't work for me. After sudo apt-get install mono-complete fsharp mozroots --import --sync source setenv.sh make -C src I'm get…
John Ostin
  • 301
  • 2
  • 12
2
votes
0 answers

What language has equational rewrite?

A classic case of inefficiency in functional program is things like the reverse function written from specification import Prelude() [] ++ ys = ys (x:xs) ++ ys = x:(xs ++ ys) reverse [] = [] reverse (x:xs) = (reverse xs) ++ [x] Using…
nicolas
  • 9,549
  • 3
  • 39
  • 83
2
votes
1 answer

Gdb with emacs and F*

I would like to debug simple F* program using Emacs fstar-mode and gdb. At the very end of the wiki of fstar-mode https://github.com/FStarLang/fstar-mode.el is information: The fstar-gdb command (M-x) attaches GDB to the current F* process and…
Bartek Wójcik
  • 473
  • 3
  • 15
1
vote
1 answer

Unknown assertion failed in FStar

I'd like to understand what's wrong with this simple exercise. let even n = (n % 2) = 0 let rec even_sqr (n:nat {even n}) : Lemma (even (n * n)) = match n with | 0 -> () | _ -> even_sqr (n - 2) FStar returns '(Error) Unknown assertion…
Attila Karoly
  • 951
  • 5
  • 13
1
vote
1 answer

Lemmas / proofs about subtyping judgments

There are times when subtyping judgments are too difficult for f-star to figure out automatically, and f-star would like me to spell out my proofs in more detail. I am also running into cases where I would like to write a lemma that just proves…
Andrew Ferraiuolo
  • 47
  • 4
1
vote
1 answer

How to check equality of two FStar.Set's

How can you check whether two sets are equal in FStar? The following expression is of type Type0 not Tot Prims.bool so I'm not sure how to use it to determine if the sets are equal (for example in a conditional). Is there a different function that…
JDN
  • 509
  • 3
  • 8
  • 14
1
vote
2 answers

Precondition not satisfied when calling function in another module

I'm trying to call a function in another module that is responsible for ensuring the pre/post conditions on the heap are preserved. Specifically it ensures that the string passed in is "readable" before calling read: val readableFiles : ref…
JDN
  • 509
  • 3
  • 8
  • 14
1
vote
1 answer

F* Raising Exception in match body

I am trying to create a function in F* to determine the minimum element of a list, and I want to throw an exception if the list is empty. The code I have so far is below: module MinList exception EmptyList val min_list: list int -> Exn int let rec…
rlee827
  • 1,853
  • 2
  • 13
  • 32
1
vote
1 answer

Using the normalizer to reduce a recursive function

I want to prove a property parameterized over a finite number of cases. I would like to divide the problem to one instance per case and solve each instance separately. Here is an example to clear up things: module Minimal open FStar.List open…
Nick
  • 27
  • 3
1
vote
3 answers

How to get insights about a z3 query when not on Windows

The wiki page at https://github.com/FStarLang/FStar/wiki/Profiling-Z3-queries suggests using the Z3 Axiom Profiler; however, the Z3 Axiom Profiler seems to work reliably on Windows only. How can I easily get the quantifiers that fire the most…
Jonathan Protzenko
  • 1,709
  • 8
  • 13
1
2