FStar

FStar copied to clipboard

SMT Encoding issue (forcing thunked names)

2

Opening a GitHub issue to better track this. Original message below. --- I faced a curious issue in one of the proofs within code that I was writing in Vale,...

jaybosamiya

Incorrect erasure of function types

3

(Following up on the discussion we just had.) F* treats function types with an erasable codomain as erasable themselves. For example, `Type -> Type` is erasable. If such a function...

gebner

This is an MWE extracted from the issue I had in the thunk module I showed yesterday. There are three types here, `r` is a subtype of `s`, which is...

gebner

Normalizer has weird behavior with one-element lists (again)

1

Following the resolution of #3353, I can now use my `squash (norm ...)` construct in my proofs, however, I need to prove it first! I am again noticing a weird...

TWal

This has been happening on and off for a bit, where some seemingly innocuous changes to F* trigger this bug again, but trying to minimize it makes it disappear in...

mtzguido

I was surprised this is accepted: ```fstar val iname_of () : erased int let iname_of () : int = 1 ``` The body seems to get a `hide` coercion and...

mtzguido

Old issue, but something I'd like to revisit now. In the snippet below, we want to make a list of functions of `some_ty`, just like `f1`, but trying to write...

mtzguido

__FL__ added and tested

2

Two changes: 1) __FL__ lexeme in FStarC_Parser_LexFStar.ml 2) tests/validation-time with a Test.LexemeFL.fst that checks __FL__

briangmilnes

Inlining sometimes fails to inline FStar.Mul.op_Star into Prims.op_Multiply, so it shows up in the OCaml. E.g. ```fstar module X open FStar.Mul unfold let pow2_norm (n:nat) = normalize_term (pow2 n) let...

mtzguido

Milnes strings

1

I have 'thickened' strings quite a bit. There are additions to the end of FStar.String.fst that define a partial string equality and string equality and provide a string difference (for...

briangmilnes