Emit a result-determining postcondition as rewrites_to - #240

Draft

nikswamy wants to merge 8 commits into

nswamy/pal-pr25-rvalue-memberfrom

nswamy/pal-pr26-rewrites-to

Commits on Aug 18, 2026

Let a refinement name an earlier parameter

nikswamy
and
Copilot
committed
00182c1
Resolve a parameter refinement in the definition's scope

nikswamy
and
Copilot
committed
28fb0d9
Verify writes through an optional output pointer

nikswamy
and
Copilot
committed
3538f42
Settle a guarded branch on one resource shape

nikswamy
and
Copilot
committed
7f4b7bf
Name a preserved nullable payload after the parameter

nikswamy
and
Copilot
committed
fd04baf
Take back what was handed to an optional parameter

nikswamy
and
Copilot
committed
32bddc9
Merge branch 'nswamy/pal-pr28-nullable-caller-transfer' into nswamy/pal-pr26-rewrites-to
nikswamy
committed
2e051d4
Emit a result-determining postcondition as rewrites_to

nikswamy
and
Copilot
committed
1a8c0f7