Use Pulse for verified stateful programming: Remove heap model and witness/recall, etc#4155
Merged
Use Pulse for verified stateful programming: Remove heap model and witness/recall, etc#4155
Conversation
…ects Replace the heap-based ST/ML effects with underspecified versions that are decoupled from any concrete heap model. The new FStar.All.fsti defines: - STATE = DIV (underspecified state, same WP as DIV) - ALL = EXN (underspecified state+exceptions, same WP as EXN) - Abstract ref type with assumed hasEq and strictly_positive attribute - Underspecified alloc/read/write operations - ML effect as trivial ALL, St effect as trivial STATE Deleted modules: - FStar.Monotonic.Heap, FStar.Heap, FStar.ST, FStar.Ref, FStar.MRef - FStar.Monotonic.Witnessed, FStar.Witnessed.Core - FStar.MST, FStar.MSTTotal, FStar.NMST, FStar.NMSTTotal - FStar.SquashProperties, FStar.Tcp, FStar.Udp - ulib/legacy/ (Array, Axiomatic.Array, TwoLevelHeap, Relational.*) - Restored FStar.Constructive, FStar.ErasedLogic, FStar.Matrix2, FStar.Error from legacy/ to ulib/ (no heap dependencies) Deleted examples/tests using heap model: - examples/preorders/ (entire directory) - examples/old/csl/, examples/old/seplogic/ - examples/layeredeffects/HoareST*, RW, LatticeEff - Various heap-dependent test files Updated examples/tests to use FStar.All instead of FStar.ST/Heap/Ref. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
- ExampleHeap.fsti/.fst: Simple heap model where ref a is abstract (internally a positive nat), heap is a map from addresses to typed cells, with sel/upd/alloc/contains operations. sel/upd require a contains precondition. - ExampleST.fst: Instantiates STATE_h with ExampleHeap.heap, providing ExST effect with assumed get/put/st_alloc/st_read/st_write actions. - HoareST.fst: Hoare-style layered effect built on top of ExST, with library with index, upd, length, swap, and concatenation. - TestHoareST.fst: Tests adapted from the original, covering pure lifts, bind composition, pattern matching, reification, and heap operations. The original HoareST/TestHoareST files were deleted when removing FStar.Monotonic.Heap. These restored versions use ExampleHeap instead, without preorders or witness/recall. HoareSTPolyBind, LatticeEff, and RW are not restored as they require deeper changes. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Adapt the three deleted examples to use ExampleHeap/ExampleST/ExampleALL instead of FStar.Heap/FStar.ST/FStar.All: - HoareSTPolyBind.fst: Polymonadic binds between PURE and HoareST, adapted to use ExST. Removed recall/mref/preorder usage. Added contains preconditions to array operations. - RW.fst: Read-only vs read-write indexed effect tracking, adapted to use ExST as the base state effect instead of FStar.ST. - LatticeEff.fst: Lattice of effect labels (WR, EXN) with repr over ExALL (ALL_h ExampleHeap.heap). Includes catch/try_with. - ExampleALL.fst: Instantiates ALL_h with ExampleHeap.heap, providing ExALL effect with get/put/raise/st_read/st_write actions, and a sub_effect from ExST to ExALL. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
- Move ExampleHeap.fsti/.fst from examples/layeredeffects/ to ulib/FStar.SimpleHeap.fsti/.fst - Remove the unused contains_decidable assumption - Update all layered effect examples to use FStar.SimpleHeap - Restore examples/native_tactics/Simplifier.fst with: - Pure logic simplification tests (unchanged from original) - Stateful tests using FStar.All's underspecified ST effect - Native plugin extraction and loading works Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
…aml support - Remove examples/crypto/ (depends on deleted heap model) - Remove doc/old/ and doc/ref/ (stale documentation) - Remove tests that depend on old ALL/ST WP shape with heap args: Bug581, Bug623, Neg, Unit1.Basic - Fix tests/micro-benchmarks/MAC.fst: ST.alloc -> alloc - Fix tests/machine_integers/TestShift.fst: increase rlimit for underspecified ML effect - Add ref, alloc, op_Bang, op_Colon_Equals, try_with to ulib/ml/app/FStar_All.ml for OCaml extraction support Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
It is only used by the layered effect examples, not by ulib or anything else, so it belongs in examples/. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
These modules are clean (no admits/assumes), well-tested, and already depended on by ulib/FStar.OrdSetProps.fst. Move them out of experimental. Remaining in experimental: - FStar.Reflection.Typing: has admits, not yet production-ready - FStar.Sequence.*: clean but unused outside experimental - FStar.Universe.PCM: clean but unused outside experimental - FStar.ConstantTime.Integers: clean but only used by tests Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
…ulib Clean modules with no admits. Move them out of experimental. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Stale examples that are no longer maintained. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
The tools/ directory only contained diff_smt2.sh. Move it to .scripts/ where other project scripts live. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
With this PR, the only recommended way to build verified programs with mutable heaps is to use Pulse.
Replace the heap-based ST/ML effects with underspecified versions that are decoupled from any concrete heap model. The new FStar.All.fsti defines:
Deleted modules:
Deleted examples/tests using heap model:
Updated examples/tests to use FStar.All instead of FStar.ST/Heap/Ref.
Modules in examples/old ulib/legacy etc. have been deleted.
Some modules from ulib/experimental are now in ulib