FStar

FStar copied to clipboard

Steel: issue with subcomp framing rule for return?

4

Hi, I noticed the following small bug while using Steel with selectors, that also affects Steel without selectors. It can be demonstrated with the following minimal example using a dummy...

cmovcc

`l_to_r` fails when there is subtyping?

1

`l_to_r` do not work in this case: ```fstar open FStar.Tactics assume val length_cons: #a:Type -> x:a -> l:list a -> Lemma (List.Tot.Base.length (x::l) == (List.Tot.Base.length l) + 1) [@@ expect_failure]...

TWal

I’m running an error message that mentions: ``` (Error 18) ASSERTION FAILURE: Impossible : trying to reify a lift between unrelated effects (Prims.GHOST and FStar.DM4F.GRandom.GRAND) F* may be in an...

klinvill

Hi, I noticed the following bug while using Steel with selectors, that also affects Steel without selectors. It can be demonstrated with the following minimal example using a dummy structure...

cmovcc

When clauses within match block sometimes supported?

1

Hello, I noticed the following strange behavior: match clauses seem to be in some cases usable and not completely disabled. It can be demonstrated with the following minimal example. ```fstar...

cmovcc

Type ascriptions on parameterised let expressions ignore type refinement

1

Expressions of the form let f x : t2 = e1

VisualMelon

Hi, Tactics that pack embedded values depending on a local let binding declared outside the tactic seem to get stuck. For instance, below I pack some `term_view`, but as soon...

W95Psp

Steel effect: Assume requires clause when typechecking ensures

1

Consider the following toy example, as reported by @cmovcc: ```fstar let test (x: nat) : Steel nat emp (fun _ -> emp) (requires (fun _ -> x > 0)) (ensures...

R1kM

Hello, I noticed the following bug while using Steel with selectors, that can be demonstrated with the following minimal example, which contains a simple workaround. ```fstar module Reqens open Steel.Memory...

cmovcc

FStar does not compile on arm64, arm32 and ppc64

6

arm64 and ppc64: ``` #=== ERROR while compiling fstar.2021.06.06 ===================================# # context 2.1.0 | linux/arm64 | ocaml-base-compiler.4.12.0 | pinned(https://github.com/FStarLang/FStar/archive/refs/tags/v2021.06.06.tar.gz) # path ~/.opam/4.12/.opam-switch/build/fstar.2021.06.06 # command ~/.opam/opam-init/hooks/sandbox.sh build make PREFIX=/home/opam/.opam/4.12 -j 31...

kit-ty-kate