Releases · FStarLang/pulse

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