Update Core's evaluator do symbolic execution only without partial evaluation#921
Update Core's evaluator do symbolic execution only without partial evaluation#921
Conversation
|
I would love to see how this PR could be influenced by or influence this other PR I'm working on: |
MikaelMayer
left a comment
MikaelMayer
left a comment
There was a problem hiding this comment.
Clean simplification that removes the partial-evaluation output (transformed programs) from the evaluator, keeping only the symbolic environments. The core idea is sound: the proof obligations and path conditions already live in the Env, so carrying the rewritten program through the pipeline was unnecessary overhead.
A few items to address:
-
Bug — missed rename in
Strata/MetaVerifier.lean:genVCs(line 60) still callsCore.typeCheckAndPartialEval, which was renamed toCore.typeCheckAndEval. This will fail to compile. -
Dead code —
StmtsStackinStatementEval.lean: TheStmtsStacktype alias and its four methods (push,pop,top,appendToTop, lines 371–389) are no longer referenced after removing thestkfield fromEnvWithNext. They should be removed. -
See inline comments for two smaller nits.
|
@keyboardDrummer-bot can you please look at this comment |
I think in high level it goes well with #753 (even if it might have some merge conflicts), because the direction is towards simplifying the PE engine and factoring out program-transforming logics to program transformations. Every transformation that is newly defined in #753 will still be valid ones. |
|
Addressed comments |
Co-authored-by: Michael Tautschnig <mt@debian.org>
…ould-b Main PR #921 changed the evaluator to do symbolic execution only (no PE). This removed the stk mechanism that built transformed programs, making the branch's ObligationExtraction and Deduplication incompatible. Resolve by reverting to main's evaluator and test outputs. The ObligationExtraction and Deduplication modules remain in the codebase but are not wired into the pipeline. Remove PEAssumeTest which tested PE-specific behavior that no longer exists.
Rename Deduplication.lean to ANFEncoder.lean and update all identifiers (deduplicateProgram -> anfEncodeProgram, etc.) to clarify this is the same concept as the SMT-level ANF encoder but operating on Core programs. ObligationExtraction and ANFEncoder are not yet wired into the pipeline because main's evaluator (#921) does symbolic execution without producing a transformed program. These modules will be integrated once the evaluator produces a program that ObligationExtraction can walk.
4 participants
Strata's Core evaluator is truly a partially evaluator in the sense that it can simplify the given program for every possible execution path, and returns portfolio of simplified programs. It means that there are N diverging control flows in a program, it can return N different programs.
However, this can cause certain benchmarks' memory usage of Strata increase quickly to maintain a set of variants of programs after partial evaluation. I think that without explicitly keeping the partially evaluated programs Strata will still simplify symbolic expressions pretty well and the ultimate verification conditions will virtually look the same. It is because partial evaluator not only returns the partially evaluated programs, but also the symbolic environment after executing the program. The symbolic environment will already contain path conditions and proof obligations - these are independent from the partially evaluated program. The benchmark seems unregressed after this change.
This patch renames
Core.typeCheckAndPartialEvaltoCore.typeCheckAndEval, and its underlying partial evaluators to purely do symbolic simulations only. :)CLARIFICATION: The Lambda's evaluator will still remain as a partial evaluator, as it wasn't designed to diverge into multpiple different evaluation results for now
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.