Problem
#1727 has mostly moved from broad type-system enrichment to a narrower remaining gap: Verity still lacks a first-class Call.Result-style type for modeling fallible external calls and returndata-bearing operations as typed values.
Newtypes and ADTs are already present, so keeping this inside the original umbrella makes the remaining work harder to track.
Scope
- Design a first-class result type suitable for call-style APIs, including success/failure and optional returndata payload shape.
- Expose ergonomic macro syntax that does not require ad hoc tuple/status plumbing at each call site.
- Lower to the existing low-level call / returndata primitives where possible.
- Add executable fallback semantics and focused smoke/property tests.
- Define the proof boundary: either keep it outside
SupportedSpec with an explicit diagnostic, or add the source/interpreter lemmas needed for the first supported subset.
Problem
#1727 has mostly moved from broad type-system enrichment to a narrower remaining gap: Verity still lacks a first-class
Call.Result-style type for modeling fallible external calls and returndata-bearing operations as typed values.Newtypes and ADTs are already present, so keeping this inside the original umbrella makes the remaining work harder to track.
Scope
SupportedSpecwith an explicit diagnostic, or add the source/interpreter lemmas needed for the first supported subset.