Pulse v2024.06.02

What's Changed

• Fixing VS Code configs by @mtzguido in #1
• Misc changes to task pool by @mtzguido in #2
• Show that Array.length always SizeT.fits. by @gebner in #3
• Refactor Makefiles, maximize parallel verification for CI by @tahina-pro in #4
• Some utilities on invariant names by @nikswamy in #5
• Enforcing in PulseCore that ghost computations cannot use witness/recall by @nikswamy in #6
• Ghost functions have a model supporting their erasure by @nikswamy in #10
• Core: remove explicit preconditions for compatible x x by @mtzguido in #12
• Use HNF to normalize annotated computation types. by @gebner in #14
• Bump rlimit. by @gebner in #16
• A stratified heap with two universes, enabling storing "small" heap predicates in the larger heap by @nikswamy in #19
• Extract DPE to C by @tahina-pro in #20
• Fixing #11 by @aseemr in #23
• Misc patches by @mtzguido in #26
• Use a typeclass for non informative types by @mtzguido in #27
• Pulse.Lib.SmallTrade: add a small version of trades by @mtzguido in #28
• Extract Pulse.Lib.SpinLock.release to C by @aseemr in #25
• Removing term from Pulse AST, instead use F* reflection terms and expose a term view to the Pulse checker by @aseemr in #30
• Resourceful invariants and associated libraries by @aseemr in #38
• Some internal cleanup by @aseemr in #39
• Fix for #33 by @aseemr in #40
• bump rlimits by @mtzguido in #43
• Misc changes by @mtzguido in #44
• Pulse.Class.Small: a class for small vprops by @mtzguido in #45
• Arrays: proving the smallness of pts_to and pts_to_range by @mtzguido in #47
• library: rename Pulse.Lib.Par.Pledge.* into Pulse.Lib.Pledge.* by @mtzguido in #48
• SpinLock: prove (a version of) the injectivity lemma by @mtzguido in #46
• Nik injectivity by @nikswamy in #53
• Trying to remove fractional permission from the cells in PulseCore heap by @aseemr in #41
• Misc pcm libs and examples by @aseemr in #42
• Misc async changes by @mtzguido in #54
• Redefining permissions directly as reals by @aseemr in #51
• Misc by @mtzguido in #56
• Fixing pretty printing of contexts by @mtzguido in #58
• snap, bracing for FStarLang/FStar#3256 by @mtzguido in #57
• Misc usablity improvement by @mtzguido in #61
• Mutex guard based Mutex API by @aseemr in #62
• DPE top-level theorem by @aseemr in #63
• Fix ML module + pulse2rust for new sets by @mtzguido in #64
• Misc by @mtzguido in #65
• Adding only tick variables as implicit binders by @aseemr in #66
• FlippableInv: eta expand by @mtzguido in #68
• Support for directly writing extension definitions against vals by @aseemr in #67
• Fixes for new F* debug module by @mtzguido in #69
• Pulse.Lib.OnRange implementation and tweaks to stick interface by @aseemr in #70
• A library for condition variables by @nikswamy in #71
• Pulse.Lib.Codeable: a class for codeable vprops by @mtzguido in #72
• Core: expose extensionality of op_exists_Star by @mtzguido in #73
• Misc by @mtzguido in #74
• Libraries for top-level spinlock and mutex, and their use in DPE by @aseemr in #76
• Makefile: fix boot-checker to not build library by @mtzguido in #77
• Some changes for linking with DICE* + certify key and sign DPE APIs by @aseemr in #78
• DPE: Generate Rust bindings as part of CI by @tahina-pro in #80
• Misc changes by @mtzguido in #81
• Pulse.Lib.HashTable: this branch is unreachable by @mtzguido in #82
• doc: building: mention KRML_HOME environment variable by @amosr in #75

New Contributors

• @mtzguido made their first contribution in #1
• @gebner made their first contribution in #3
• @tahina-pro made their first contribution in #4
• @nikswamy made their first contribution in #5
• @aseemr made their first contribution in #23
• @amosr made their first contribution in #75

Full Changelog: https://github.com/FStarLang/pulse/commits/v2024.06.02