FStar
FStar copied to clipboard
FStarLang
A Proof-oriented Programming Language
```let r : UInt64.t = UInt64.of_string "0xFFFFff80"``` is accepted by F*. While this is valid in C we have examples when this is causing trouble for instance with CVE-2019-8741 in...
I was writing some test code. Yes, I know you all probably think its a bit passe, but it helps while learning to see that my specifications are what I...
We've got some version skew and some problems defining (let!) so I built from source. But what is the right target to run the tests in the makefile and how...
```fstar module Bad let f (y:int) : x:int -> int = fun x -> x+y let vquote = `%Prims._assert let f = fun x -> match x with | 0...
```fstar module Bug noeq type ty #a (x:a) = | I : (a:nat) -> ty x let _ = assert (forall x. x + 1 > x) // just here...
Due to #2840, for certain type definitions, I need to disable the positivity checker. I use the `--__no_positivity` flag for this. If I only have an `.fst` file, the option...
"F* may be in an inconsistent state" error when trying to define parameterized raise in DM4F effect
I was working on parameterizing the RAND DM4F effect on a type. It seems to fail when I include the `raise` function with an error that reports: ``` ASSERTION FAILURE:...
The normalizer is not currently reducing lambdas in the types of residual comps in Tm_abs and Tm_match nodes. This simple patch makes it so, opening the PR just to: -...
@raulraja et al. requested an option to print the parser AST in full detail. This PR provides two options: * --print_ast: Which takes a module/namespace selector for the names of...
This is a follow-up to #2815: while F* itself is now built with dune, not all of its examples are. As proposed by @msprotz in https://github.com/FStarLang/karamel/pull/333#issuecomment-1429090137, we should remove support...
