mark lines for removal ??

[alex4482]

Hi, i have writen some functions with a fairly simple result to construct, yet a difficult condition to prove for that result.
To prove that the 'condition' is actually fulfilled, i have additional variables initialized using calls to other functions, and with many 'assert' statements, the condition was in the end proven to be true.
but, those variables do not contribute to the result itself.
yet, when compiling, the .ml files still contain those variables, and with no 'asserts' in the ml files, the variables are not used anywhere.
is there a way to use those variables to only prove the condition, but not transport them to the ml files when compiling?
maybe using them inside a Lemma?

-edit:
I have just tried to put all extra variables and asserts in a lemma which should prove the exact same condition and receives the same input variables, but i get an error right after the = sign, (prims.fst line :430) and i cant fix it

[nikswamy]

By default, F* preserves the let-binding structure of a source program when extracting it.

I guess you have something that looks like this:

module Extract

let incr (x:int) : y:int { y = x + 1} = x + 1

let lem (x:int) (y:int)
  : Lemma
      (requires y = x + 1 /\ y > 1)
      (ensures x >= 0)
  = ()


let test (x:int { x > 0 }) : nat =
  let y = incr x in
  let _ = lem x y in
  x

And the extracted code produced by fstar.exe --codegen OCaml looks like

$ cat Extract.ml
open Prims
let (incr : Prims.int -> Prims.int) = fun x -> x + Prims.int_one
let (test : Prims.int -> Prims.nat) = fun x -> let y = incr x in x

Notice the call to lem is erased (total let bindings of unit are erased). But the call to incr remains.

First, in general, F*'s extraction to OCaml could use some love ... the generated code is syntactically not very pretty. So, we should improve that.

But, here are few things you can do about your specific problem for additional sub-terms remaining:

Use Ghost.erased

See this chapter: http://fstar-lang.org/tutorial/book/part4/part4_ghost.html#erasure-and-the-ghost-effect

If you don't intend for the auxiliary function like incr to be extracted, you can mark it's result erased:

module Extract
open FStar.Ghost

let incr (x:int) : erased (y:int { y = x + 1}) = x + 1

let lem (x:int) (y:int)
  : Lemma
      (requires y = x + 1 /\ y > 1)
      (ensures x >= 0)
  = ()


let test (x:int { x > 0 }) : nat =
  let y = incr x in
  let _ = lem x y in
  x

Now you get:

$ cat Extract.ml
open Prims
let (test : Prims.int -> Prims.nat) = fun x -> x

If the incr function is generally useful and you only want to erase this one particular call to it, you can do:

module Extract
open FStar.Ghost

let incr (x:int) : y:int { y = x + 1 } = x + 1

let lem (x:int) (y:int)
  : Lemma (requires y = x + 1 /\ y > 1)
          (ensures x >= 0)
  = ()


let test (x:int { x > 0 }) : nat =
  let y : erased _ = incr x in
  let _ = lem x y in
  x

And you get:

$ cat Extract.ml
open Prims
let (incr : Prims.int -> Prims.int) = fun x -> x + Prims.int_one
let (test : Prims.int -> Prims.nat) = fun x -> x

(Equivalently, you can write let y = hide (incr x) in ...

Attributes: Inline let and noextract

If for whatever reason, you don't want to go with the type-and-effect based treatment of erasure, a more ad hoc approach is to use various attributes to control F*'s code generation. I would generally recommend preferring the erased type & ghost effect, but I'll include this here for completeness.

module Extract

noextract
let incr (x:int) : y:int { y = x + 1 } = x + 1

let lem (x:int) (y:int)
  : Lemma (requires y = x + 1 /\ y > 1)
          (ensures x >= 0)
  = ()

let test (x:int { x > 0 }) : nat =
  [@@inline_let]
  let y = incr x in
  let _ = lem x y in
  x

The noextract attribute on a top-level definition instructs F* to skip extracting it altogether.
But, then it's on you to make sure that no reference to incr remains in the extracted code.

The inline_let attribute on let y = ... instructs F* to inline y in the continuation when extracting it. Since y does not appear in the returned result term, it just disappears. The resulting code is:

$ cat Extract.ml
open Prims
let (test : Prims.int -> Prims.nat) = fun x -> x

Note, if you leave off the inline_let attribute on let y you get an error:

Extract.fst(12,10-12,16): (Error 342) Will not extract reference to variable `incr` since it is noextract; either remove its qualifier or add it to this definition. This error can be ignored with `--warn_error -342`.

See https://github.com/FStarLang/FStar/wiki/Custom-attributes
and https://github.com/FStarLang/FStar/wiki/Qualifiers-for-definitions-and-declarations

[alex4482]

hi
i tried your advice to write my variable like this:
let var : erased my_type = ....

and below i have an assert
assert( L.mem var vars_list);

and it throws and error
FStar.Ghost.erased (?u651) _ is not a subtype of the expected type DataTypes.variable_info

[nikswamy]

Behind the scenes, F* inserts implicit coercions for reveal and hide. It's described here: http://fstar-lang.org/tutorial/book/part4/part4_ghost.html#the-erased-type-reveal-and-hide

As mentioned there, this implicit coercion insertion mechanism does not work in polymorphic contexts.

So, I'm shooting in the dark a bit here, but I suspect it will work if you write

assert( L.mem (Ghost.reveal var) vars_list);

[alex4482]

well i have just tried using the [inline let]
and it seems to have worked
however i use the erased variables in quiet a few assert statements,
and would like to just write a couple [inline let]
is the efficiency different if i were to use [inline let] compared to hide () and Ghost.reveal?
efficiency of the final .exe i mean

[nikswamy]

As long as the variable you're inlining doesn't appear anywhere in the extracted code, then there are no performance implications for the .exe.

So, if I understand correctly, you're using a combination of inline_let and erased types to get the job done?

[alex4482]

no, i removed the erased parts, because i would have had to change many assert statements to contains Ghost.reveal var and didn't want to.
so i only used inline_let