feat: introduce `sym1_n` tactic as a more intelligent version of `sym1_i_n`

[alexkeizer]

Description:

This refactors the symbolic evaluation using pre-generated theorems to maintain a context structure which tracks the names of the various theorems needed for eval, rather than relying on these theorems to be available with hard-coded names.

In the process, we also define a way to infer the initial context by searching through the local context for variables and hypothesis that are def-eq to what we expect (basically doing by assumption). This has two big benefits:

• It allows us to generate more meaningful error messages when the contract is broken, and
• During this search we also infer and assert more information. For example, we assert that the m in sf = run m s0 is a numeric literal and reflect the value (we can use this in future to throw a meaningful error when the user asks to simulate more than m steps). Similarly, we reflect the PC (which is also assumed to be a concrete literal) and determine the name of the program; this information will be useful to more intelligently find the right stepi lemma to apply in future (in contrast to the current approach which assumes the right lemmas to be present in a simp-set).

Since the search matches up-to defeq, it might impact performance slightly. That said, the search only happens once per sym_n call, independent of the amount of steps we simulate, so this cost should pale in comparison to the cost of the actual symbolic eval.

I've demonstrated the new tactic works on gcm_gmult_v8. In a next PR, I intend to remove sym_i_n and replace all uses with sym_n.

Testing:

make all passed on the cloud desktop, including conformance testing

License:

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.

[alexkeizer]

I've refactored the error messages to include the highlighting suggested and generally made them a bit more informative. Also, I've refactored the reflection of Nats to include reduction (of ground terms).

@bollu Could you please have another look and confirm I've addressed your comments

I've also re-run conformance testing, still passes

[alexkeizer]

@alexkeizer and I chatted about this in-person. He corrected my faulty memory that we could throwErrorAt for hypotheses. He suggested that we should try to throw a more informative error message regardless.

My memory now suggests that it maybe possible to build a MessageData with the FVarId, and it will then correctly interpolate into the nice hover-with-type-information.

For future reference: FVarId does not have a ToMessageData instance, but Expr does have one which can be used through Expr.fvar _ (this is how I've implemented it)

[alexkeizer]

@shigoel I've addressed your comments, another round of review would be appreciated! Also did another run of conformance checking, all is still good.

(I did mess up the history, sorry about that, but the diff w.r.t. the comment you last reviewed would be uninformative because of the line-wrapping anyway, so it's hopefully not too bad)