Use Pulse for verified stateful programming: Remove heap model and witness/recall, etc#4155

Merged

nikswamy merged 12 commits intofstar2from

_fstar2_no_monotonic_heap

Apr 2, 2026

Commits on Apr 1, 2026

Remove heap model and witness/recall; replace with underspecified effects

nikswamy
and
Copilot
committed
Add ExampleHeap and restore HoareST layered effect examples

nikswamy
and
Copilot
committed
Restore HoareSTPolyBind, RW, and LatticeEff layered effect examples

nikswamy
and
Copilot
committed
Move ExampleHeap to ulib/FStar.SimpleHeap and restore Simplifier

nikswamy
and
Copilot
committed
Fix CI failures: remove stale examples and tests, update FStar_All OCaml support

nikswamy
and
Copilot
committed
Move SimpleHeap from ulib back to examples/layeredeffects

nikswamy
and
Copilot
committed
Remove unused HasEq_ref assumption from FStar.All

nikswamy
and
Copilot
committed
Promote FStar.OrdSet and FStar.OrdMap from experimental to ulib

nikswamy
and
Copilot
committed
Promote FStar.Sequence.* and FStar.Universe.PCM from experimental to ulib

nikswamy
and
Copilot
committed
Remove examples/old

nikswamy
and
Copilot
committed
Move tools/diff_smt2.sh into .scripts

nikswamy
and
Copilot
committed

Commits on Apr 2, 2026

Merge remote-tracking branch 'origin/fstar2' into _fstar2_no_monotonic_heap
nikswamy
committed