FStar.Reflection.Typing.subst_term extracts to dangerous code

[gebner]

The reflection API only exposes a portion of the syntax AST. Since FStar.Reflection.Typing.subst_term is written as a syntax traversal using this limited API, it will silently drop various flags when used as executable code. It should also used delayed substitions, obviously.

I ran into this the other day in FStarLang/pulse#209. This subst_term function silently dropped the effect flag in the let, breaking extraction.

This implementation of substitution should clearly not be executable, whether from extracted code or tactics. Some ideas:

1. We could mark the function as ghost. This currently fails because equiv_arrow references it, and the reflected typing judgements are not erased. Is it intentional that typing and co. are not erased?
2. We could use the correctly implemented FStar.Stubs.Reflection.V2.Builtins.subst_term function instead and assume the equalities as axioms.

@mtzguido Any thoughts?

[mtzguido]

I suppose the first problem here is that Tv_Let does not accurately represent effectful letbindings. This was intentional at first, tactics were only handling the pure subset of F* used for propositions and proofs. Ignoring the effect label is bad, however, and maybe we should have returned Tv_Unsupp (though doing this now will probably break things in pulse).

I was also thinking the typing judgments in Reflection.Typing could be made ghost. We mostly used them under an erased in Pulse. A separate question is about the Pulse judgments, which we may need to keep concrete if we want to extract the program from a typing derivation (instead of from the synax, like we do now). Maybe @nikswamy or @aseemr better remember if there's a reason this cannot be made ghost (otherwise I'd attempt it).

For assuming the equality, I think we do something exactly that in Pulse (Pulse.Syntax.Naming.subst_host_term). Ideally we would avoid it altogether with the previous bullet?

[nikswamy]

My thinking was that forcing Reflection.Typing.typing to be erased could preclude some applications, whereas defining it as concrete still allows applications to work with erased typing if they don't need the concrete derivation.

That said, making it erased from the get go would make most applications simpler, rather than forcing them to pay the cost of working with erased types & coercions, for hypothetical applications that might need a concrete derivation.

(May a not so hypothetical application is bootstrapping a certifier, as in this self-certification paper https://dl.acm.org/doi/10.1145/2103621.2103723 which involved generating a concrete typing derivation and exporting it to Coq to be re-checked there.)

With Pulse typing, the reason it's not erased is as Guido says: to support extraction from derivations. But, we don't do that anymore.

[gebner]

Okay, I tried to make the typings and the associated functions ghost. But to my suprise, there were plenty more functions with a questionable implementation based on the tactic/reflection API ("questionable" in the sense that they give different and incorrect results compared to the built-in versions):

• freevars
• ln'
• Reflection.TermEq.*
• substitution

Should we redefine all of them in terms of their built-in versions?

I suppose the first problem here is that Tv_Let does not accurately represent effectful letbindings. This was intentional at first, tactics were only handling the pure subset of F* used for propositions and proofs. Ignoring the effect label is bad, however, and maybe we should have returned Tv_Unsupp (though doing this now will probably break things in pulse).

Is there a reason we can't just reflect the full syntax? Providing partial views will always result in information loss in corner cases like this.

FWIW, returning Tv_Unsupp doesn't fix the general issue at all: freevars, ln', etc. would still be silently (!) incorrect.

For assuming the equality, I think we do something exactly that in Pulse (Pulse.Syntax.Naming.subst_host_term).

There we are converting between the reflection substitution type and the regular one. Could we consolidate on a single substitution type?

(May a not so hypothetical application is bootstrapping a certifier, as in this self-certification paper https://dl.acm.org/doi/10.1145/2103621.2103723 which involved generating a concrete typing derivation and exporting it to Coq to be re-checked there.)

That's an interesting paper! Obviously that kind of approach only becomes interesting once the F* type checker uses reflection typings, so this is probably really far away from becoming a concern.