Skip to content

[move-prover] Support folds_of snapshots for non-copy or non-drop captures #20372

Description

@wrwg

Context

PR #20360 infers specifications for inline HOF lambdas. folds_of currently records each mutated capture at loop entry. That requires the captured value to have both copy and drop.

This rejects useful framework call sites such as:

  • appending RistrettoPoint values to captured vectors;
  • mutating captured statement builders containing non-copy points;
  • building generic vectors whose element types do not guarantee drop;
  • building a captured SmartTable, which lacks copy.

A representative diagnostic is:

cannot resolve folds_of ... the captured variable must have the copy and drop abilities, so its value at loop entry can be recorded

Missing feature

Represent the entry state and evolving fold accumulator without requiring a Move-level copy/drop snapshot of the whole captured value. The solution must preserve sound treatment of linear values.

Expected result

The affected for_each_ref calls should verify without explicit-loop workarounds or stronger abilities on user types.

Tracked from #20360.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions