Reach while-loop invariant rejected when referencing interact-supplied value

Reach supports while loops in local steps, but each loop must carry an invariant and a decrease measure so the built-in verifier can discharge termination and safety obligations at compile time. The goal is to write a loop whose invariant references a value obtained from the frontend through interact. The uncertainty is whether the verifier treats that value as opaque, making the invariant unprovable even when the frontend guarantees the property.

Because interact crosses the consensus boundary, the verifier may model the result as unknown. This raises an unresolved semantic question: should an invariant justified only by a frontend promise be accepted locally, or must the loop body re-establish the fact from consensus-known state? The distinction between assume and checked assertions is central, and misclassifying a frontend guarantee as a consensus fact is the likely source of the impasse.

This behavior is version-sensitive; simplification rules and accepted proof obligations have changed across Reach releases, so a program that verifies on one toolchain may fail on another without code changes.

Should the verifier accept an invariant that quantifies over an interact-provided value when the frontend guarantees it, or is an explicit assume required to bridge the boundary? If the latter, must the loop re-derive the property from consensus state, or is there a supported way to document the frontend contract for the prover?