evaluate generic term to literal safely?

Stream: lean4

[Thomas Murrills]

Let's say I have some syntax $a:term that I'm using in a tactic elaboration. I'd like it to be a string literal before I use it, but I'd like it to be able to be specified some other way, e.g. by a prior declaration let myStr := "foo" or by a computation (so I really do want a term, or at least want something broader than a str). How can I unfold all definitions in the course of elaborating the syntax so that I can try to get a string literal?

I've tried using withTransparency .all before elaborating, using evalTerm (but it complains that this is unsafe), and a couple other things. (I would have liked to try something like isDefEq (.lit m) aExpr with m a metavariable under the appropriate transparency, but then I'd need some hypothetical mkFreshLiteralMVar instead of mkFreshExprMVar to make the types work.)

Is there a simple solution I'm missing?

[Mario Carneiro]

evalConstCheck or evalTerm

[Mario Carneiro]

import Lean.Elab.Eval
import Std.Util.TermUnsafe

open Lean Meta Elab Command

elab "eval_my_string" s:term : command => do
  let s ← liftTermElabM <|
    unsafe Term.evalTerm String (.const ``String []) s
  logInfo m!"got: {s}"

def head : String := "hello"

eval_my_string head ++ " world"

[Mario Carneiro]

and yes, this is unsafe

[Thomas Murrills]

Works like a charm! Thanks for pointing me to that Std file, I probably wouldn't have found that. :)

[Thomas Murrills]

As for safety I guess I can just live on the edge? Hopefully any breakages are caught by a standard try/catch?

[Mario Carneiro]

heh, no unsafe issues aren't caught by try/catch they are likely to crash lean at best

[Thomas Murrills]

ahh lol

[Mario Carneiro]

regarding what the unsafety here specifically is, we are trusting (1) that the type String corresponds to the expression .const ``String [] and (2) the environment at run time is at least an extension of the environment at compile time, so that it makes sense to trust that the types of things in the environment have something to do with the compiled functions also in the environment that we will be calling

[Mario Carneiro]

(1) is relatively easy to check locally and to some extent can be automated by a macro

[Mario Carneiro]

(2) is almost always the case unless you are running mathlib tactics in the context of a standalone executable with a def main which calls importModulesConst to get access to an environment, not necessarily related to the one that was used to compile the program

[Mario Carneiro]

basically unsafe in lean means something similar to unsafe in rust: it is an unchecked proof obligation of the programmer, such that the consequence of violating the preconditions are usually UB (undefined behavior)

[Mario Carneiro]

Of course since lean has a proof language we try to put these proof obligations as literal proof obligations where possible, but they aren't always expressible in the language of lean, if for example they involve interaction with lean runtime representations or other things not visible to the logic

[Thomas Murrills]

ohhkay, cool, that's really informative, thx—prior to that explanation unsafe just seemed like a black box that sometimes exploded. now I can see the kind of things that can make it explode! is that a totally exhaustive list?

[Mario Carneiro]

that's the list of things that can make evalTerm specifically explode

[Mario Carneiro]

every unsafe declaration has its own preconditions/postconditions for sound usage

[Thomas Murrills]

(deleted)

[David Renshaw]

can unsafe cause Lean to accept an unsound proof?

[Mario Carneiro]

yes, easily

[Mario Carneiro]

unsafe def foo : False := foo

[Mario Carneiro]

well, unsafe functions are taint-tracked by the kernel so you can't use them to prove things about non-unsafe