FStar

FStar copied to clipboard

I only change module SimplePrintfReify to Program, otherwise is not clear. ``` Program.fst(48,28-54,1): (Warning 337) DM4Free feature is deprecated and will be removed soon, use layered effects to define XEXN...

kant2002

Enable subtyping in ctrl_rewrite (and hence, l_to_r)

2

#2476 reported issues when using `l_to_r` to perform rewritings. `l_to_r` is based on the primitive `ctrl_rewrite`, which traverses all subterms `t` of a given term, creates a goal of the...

R1kM

I'm trying to use some OCaml files extracted from F* codes in our OCaml project to verify some cryptographic properties. To build the project, I tried using `fstarlib` library which...

satos---jp

The type of `/\` and related connectives does not reflect their left-to-right bias (Was: The typechecking of `l_and` as a lazy operator is unsound)

1

In F*, the type-checking of `l_and` (`⋀`) reflects its laziness. That is in `p ⋀ q`, the type-checking of `q` can assume that `p` holds. Hence it is possible to...

857b

Subtyping and unification in the tactics engine requires re-checking solutions (Was: The unification in tactics is unsound)

3

On can prove `⊥` using the unification of uvars in tactics (F* https://github.com/FStarLang/FStar/commit/a46a208c59b502b427e300e7a9e7b7cf9fb58ad7): ```fstar module Main open FStar.Tactics #set-options "--ifuel 0 --fuel 0" let prove_False (pf : squash False) (_...

857b

Encode String literals in SMT

5

Based on #1380 by @A-Manning I added a switch to enable encoding (`smtencoding.encode_string`), and the example in #1380 is able to typecheck.

fangyi-zhou

Can we somehow make `fstar-mode` in emacs break the input file into parts according to top-level definitions, and submit as many as it could one by one so that I...

hacklex

Add support for data constructors attributes

2

Hi, This PR adds support for decorating data constructors (and records) with attributes, as @TWal was suggesting a few days ago on Slack. The syntax follows the one for binders,...

W95Psp

Post-condition failures are not localized to the failing branch

2

The example below is ripped out of context, so don't be surprised at the absurd conditions. Append was something else originally. Thing is, fstar fails to localize the problem and...

hacklex

`term_to_string` being total implies ⊥

2

Hi, `term_to_string` is a `Tot` computation despite being impure because sensitive to the options `hide_uvar_nums`, `print_bound_var_types`, `print_effect_args`, `print_implicits`, `print_real_names`, `print_universes` and `ugly`. Thus one can derive `⊥` easily by observing...

W95Psp