datatype support for smtvcs

[kondylidou]

Summary

Programs with user-defined datatypes (constructors, selectors, testers) previously caused
smtVCsCorrect to silently reduce to False and gen_smt_vcs to throw a runtime error.
This PR fixes three coordinated gaps:

1. SanitizedContext.ofCore (MetaVerifier.lean) stripped all datatype UFs/sorts, so
   neither the translate nor the denote path could see constructor/selector/tester functions.

2. translateTerm (Translate.lean) had no datatype_op case, so gen_smt_vcs threw
   "datatype function not found in context" for any VC containing a selector or constructor.

3. denoteTerm (Denote.lean) had no datatype_op case, so denoteQuery returned
   none for any VC containing a datatype operation, causing smtVCsCorrect to reduce to
   False.

Test

StrataTest/Languages/Boole/datatype_selector_vcs.lean — a minimal Box { Box_mk(val : int) }
program whose inc_val procedure uses Box..val in both requires and ensures. All 4
generated VCs pass cvc5 and smtVCsCorrect boxSelectorSeed is fully proved by gen_smt_vcs

• grind.

[kondylidou]

@joscoh following the discussion in the meeting yesterday could you check if this would be the right fix?

[kondylidou]

@joscoh following the discussion in the meeting yesterday could you check if this would be the right fix?

@abdoo8080 fyi too

[abdoo8080]

A few notes from an offline discussion:

• Elimination passes should be implemented as core-to-core transformations where possible. This makes it easier to verify their correctness against Josh's denotational semantics and lets us reuse them in other verification pipelines.
• This pass is missing several datatype axioms: that constructors are exhaustive, that they're injective, that they can't be confused (e.g., foo(x) != bar(y) for constructors foo and bar), and the acyclicity and induction principles for inductive datatypes. Those principles can't be stated in FOL, so you won't be able to express them in the SMT IR. You may be able to state them in Core's IR, but then lowering to the SMT IR will probably fail.
• Model construction issues similar to the ones we have with nat.