Add Core-to-Core datatype partial evaluation transform with correctness proof

[tautschnig]

Add a general Core-to-Core transform that simplifies datatype tester and selector applications on known constructor terms:

• tester(C(args)) → true/false depending on whether tester matches C
• selector_i(C(args)) → args[i] when selector matches C

Components:

• DatatypeInfo + collectDatatypeInfo: collect constructor, tester, and selector metadata from Core datatype declarations
• matchConstrApp: decompose an expression into constructor + arguments
• partialEvalDatatypesCore: recursive expression simplifier
• partialEvalDatatypesInProgram: apply across all procedure bodies, axioms, and specifications

Correctness proof (zero sorry):

• Define DtEquiv inductive relation capturing datatype axiom equivalence (reflexivity, symmetry, transitivity, congruence, tester/selector axioms)
• Prove partialEvalDatatypesCore_correct by structural induction on LExpr: all rewrite cases justified by DtEquiv axioms applied to simplified subexpressions, composed with congruence and transitivity

Wired into the GOTO pipeline after procedure inlining. Includes unit tests for collectDatatypeInfo, tester simplification (positive and negative), and selector projection.

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

[Copilot]

Pull request overview

Adds a Core-to-Core transformation that partially evaluates datatype tester/selector applications when applied to known constructor terms, proves the rewrite relation correct, and integrates the pass into the CBMC GOTO pipeline.

Changes:

• Implement DatatypeInfo collection plus a recursive Core expression simplifier for datatype tester/selector applications.
• Add a correctness development (DtEquiv + partialEvalDatatypesCore_correct) with no sorry.
• Wire the pass into inlineCoreToGotoFiles and add unit tests covering metadata collection and key simplifications.

Reviewed changes

Copilot reviewed 4 out of 4 changed files in this pull request and generated 6 comments.

File	Description
Strata/Transform/DatatypePartialEval.lean	New datatype partial-evaluation transform and program-wide traversal.
Strata/Transform/DatatypePartialEvalCorrect.lean	Correctness proof for the Core expression simplifier via DtEquiv.
Strata/Backends/CBMC/GOTO/CoreToGOTOPipeline.lean	Integrates the transform into the Core→GOTO pipeline after inlining.
StrataTest/Transform/DatatypePartialEval.lean	Unit tests for datatype info collection and tester/selector simplification.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[joscoh]

I am a bit confused about this transformation's purpose. These simplifications are already part of the Lambda (and hence Core) partial evaluator.

[tautschnig]

I am a bit confused about this transformation's purpose. These simplifications are already part of the Lambda (and hence Core) partial evaluator.

My primary intended use for this transform is the GOTO pipeline: The Lambda evaluator handles these simplifications during symbolic evaluation via inlineIfConstr and concreteEval. The GOTO pipeline, however, translates Core to CProver GOTO without running the Lambda evaluator — after procedure inlining, tester/selector applications on known constructors remain unsimplified.

To address the duplication concern, I've factored out the shared piece in 6ca07fc: DatatypeInfo (the constructor/tester/selector name mappings) now lives in Lambda.TypeFactory with a DatatypeInfo.ofDatatypes builder that works on List (LDatatype IDMeta). The standalone transform uses this shared structure, and matchConstrApp now delegates to the existing getLFuncCall from Lambda.Factory instead of reimplementing application decomposition. The Lambda evaluator could adopt DatatypeInfo in the future to replace its ad-hoc tester/selector dispatch.

[joscoh]

Two general comments (I haven't looked at this in close detail yet).

1. I would prefer to see something that pulls the datatype simplification out of the partial evaluator into a separate function so that it can be called both in the Lambda partial evaluator and in the Core -> GOTO transformation. Right now, this PR results in two separate implementations of the same thing, and this means we need to keep them in sync.
2. The proofs of correctness should not be given with respect to a new equivalence relation (and it is better to not include a proof than to include a sorry one). The datatype simplification is already proved correct wrt the Lambda denotational semantics in LExprSemanticsConsistent.lean. I would prefer to modify this proof and prove this transformation correct wrt an already existing semantics. I am happy to help with this once the datatype simplification has been fully abstracted.

[aqjune-aws]

For the top-level statement of correctness, github.com/strata-org/Strata/blob/main/Strata/Transform/Specification.lean has a few styles and I think Overapproximates is probably the closest definition. https://github.com/strata-org/Strata/blob/main/Strata/Transform/DetToKleeneCorrect.lean#L637-L640 is an example that uses the definition. However, since this is supposed to be equivalent, I can add the notion in a separate pull request (or even directly push to this PR, if you want).