Zulip Chat Archive

Stream: lean4 dev

Is it possible to have a flag in Elab.Term.Context, when enabled, prevents all instances of the unsafe term elaborator from running?

This way, we can prevent the execution of arbitrary code during type checking, and it doesn't seem to be very hard to implement.

This will not prevent arbitrary codes in top-level declarations, but it can prevent such behaviour during type checking of proofs.

What meaning of "unsafe" do you intend here?

Eric Wieser said:

What meaning of "unsafe" do you intend here?

I want to prohibit the execution of arbitrary code including the unsafe elaborator, evalTerm, and any other cases where a tactic author sees fit.

So evalExpr as well?

Yes, and this would be optional. Existing code will not be affected.

Ultimately I think yo uonly need to attempt to ban evalConst

But what about a tactic that uses eval on a controlled type like a natural number expression?

If the tactic author sees that its safe, then there would not be a check for the prohibit unsafe flag.

The trust is on the tactics and elaborators, rather than whatever thing wrote a proof.

It's not clear to me why you'd care about banning the unsafe keyword.

It sounds like the meaning you want this flag to have is not really related to the meaning of that keyword

(maybe I'm reading too much into your code example)

I call it prohibitUnsafe because my starting point is run_tac, which uses the unsafe keyword. A better terminology is possible.

@Leni Aniva, you would need to write a much more detailed RFC to get traction here.

Kim Morrison said:

Leni Aniva, you would need to write a much more detailed RFC to get traction here.

let me discuss with amazon people on this matter...

Last updated: Dec 20 2025 at 21:32 UTC