Skip to content

Expose checkpoint state projections#1

Open
Th0rgal wants to merge 1 commit into
mainfrom
fix/checkpoint-state-queries
Open

Expose checkpoint state projections#1
Th0rgal wants to merge 1 commit into
mainfrom
fix/checkpoint-state-queries

Conversation

@Th0rgal
Copy link
Copy Markdown
Member

@Th0rgal Th0rgal commented May 19, 2026

Summary

  • Project checkpoint states through their carried shared state, execution env, machine state, external state, and variable store instead of default.
  • This makes raw state[name]! lookup agree with checkpoint payload lookup when execution resumes after Leave/Break/Continue checkpoints.

Verification

  • lake build EvmYul.Yul.StateOps
  • Downstream Verity tiny Lean probe for revived checkpoint lookup passed.
  • Downstream lake build Compiler.Proofs.YulGeneration.Backends.EvmYulLeanNativeHarness passed.
  • Downstream lake build Compiler.Proofs.EndToEnd passed.

Note

Low Risk
Low risk: this only changes how Checkpoint variants are projected to shared/execution/machine/external state and varstore, avoiding unintended default values during control-flow jumps.

Overview
Updates Yul State projection helpers (toSharedState, executionEnv, toMachineState, toState, store) to extract values from Checkpoint (Continue/Break/Leave) payloads instead of falling back to default.

This makes state projections and var lookups consistent when execution resumes from checkpoints, while keeping OutOfFuel behavior unchanged (still projects to default).

Reviewed by Cursor Bugbot for commit 7785a9b. Bugbot is set up for automated code reviews on this repo. Configure here.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant