fstarlang/pulse issues and pull requests

#98 - Printing improvements

Pull Request - State: closed - Opened by mtzguido 5 months ago

#97 - Tame Pulse.Typing.FV

Pull Request - State: closed - Opened by mtzguido 5 months ago

#96 - Sort vprop context for printing

Issue - State: closed - Opened by mtzguido 5 months ago

#95 - fold/unfold can fail

Issue - State: closed - Opened by mtzguido 5 months ago - 1 comment

#94 - Some bad error messages

Issue - State: open - Opened by mtzguido 5 months ago - 1 comment
Labels: bug

#93 - Non-informative types vs erased types

Issue - State: open - Opened by mtzguido 5 months ago
Labels: bug, question

#92 - Bad error when forgetting function name

Issue - State: open - Opened by mtzguido 5 months ago
Labels: bug

#91 - Fix parser

Pull Request - State: closed - Opened by mtzguido 5 months ago

#90 - Names for variables introduced by STApp

Pull Request - State: open - Opened by mtzguido 5 months ago

#89 - Make admit() print the context when in interactive mode

Pull Request - State: closed - Opened by mtzguido 5 months ago

#88 - Give a name starting with '?' to uvars introduced by the Pulse checker

Pull Request - State: closed - Opened by mtzguido 6 months ago

#87 - Should `with (bs). _` instantiate all binders?

Issue - State: open - Opened by mtzguido 6 months ago

#86 - No longer need preorder state monad

Pull Request - State: closed - Opened by nikswamy 6 months ago

#85 - ci.Dockerfile: also install libclang, bindgen, etc

Pull Request - State: closed - Opened by mtzguido 6 months ago - 2 comments

#84 - Add a cached devcontainer and update script

Pull Request - State: closed - Opened by mtzguido 6 months ago

#83 - FractionalPermission: use a literal 0.0R

Pull Request - State: closed - Opened by mtzguido 6 months ago

#82 - Pulse.Lib.HashTable: this branch is unreachable

Pull Request - State: closed - Opened by mtzguido 6 months ago

#81 - Misc changes

Pull Request - State: closed - Opened by mtzguido 6 months ago

#80 - DPE: Generate Rust bindings as part of CI

Pull Request - State: closed - Opened by tahina-pro 6 months ago

#79 - Stop using Set.set

Issue - State: open - Opened by mtzguido 6 months ago
Labels: enhancement

#78 - Some changes for linking with DICE* + certify key and sign DPE APIs

Pull Request - State: closed - Opened by aseemr 6 months ago

#77 - Makefile: fix boot-checker to not build library

Pull Request - State: closed - Opened by mtzguido 6 months ago

#76 - Libraries for top-level spinlock and mutex, and their use in DPE

Pull Request - State: closed - Opened by aseemr 6 months ago

#75 - doc: building: mention KRML_HOME environment variable

Pull Request - State: closed - Opened by amosr 7 months ago - 1 comment

#74 - Misc

Pull Request - State: closed - Opened by mtzguido 7 months ago

#73 - Core: expose extensionality of op_exists_Star

Pull Request - State: closed - Opened by mtzguido 7 months ago

#72 - Pulse.Lib.Codeable: a class for codeable vprops

Pull Request - State: closed - Opened by mtzguido 7 months ago

#71 - A library for condition variables

Pull Request - State: closed - Opened by nikswamy 7 months ago

#70 - Pulse.Lib.OnRange implementation and tweaks to stick interface

Pull Request - State: closed - Opened by aseemr 7 months ago

#69 - Fixes for new F* debug module

Pull Request - State: closed - Opened by mtzguido 7 months ago

#68 - FlippableInv: eta expand

Pull Request - State: closed - Opened by mtzguido 7 months ago

#67 - Support for directly writing extension definitions against vals

Pull Request - State: closed - Opened by aseemr 7 months ago

#66 - Adding only tick variables as implicit binders

Pull Request - State: closed - Opened by aseemr 7 months ago

#65 - Misc

Pull Request - State: closed - Opened by mtzguido 7 months ago

#64 - Fix ML module + pulse2rust for new sets

Pull Request - State: closed - Opened by mtzguido 7 months ago - 2 comments

#63 - DPE top-level theorem

Pull Request - State: closed - Opened by aseemr 7 months ago

#62 - Mutex guard based Mutex API

Pull Request - State: closed - Opened by aseemr 7 months ago

#61 - Misc usablity improvement

Pull Request - State: closed - Opened by mtzguido 7 months ago

#60 - Speculative non_informative typeclass queries pollute output

Issue - State: closed - Opened by mtzguido 7 months ago

#59 - Stop checking if signature is wrong

Issue - State: closed - Opened by mtzguido 7 months ago - 1 comment

#58 - Fixing pretty printing of contexts

Pull Request - State: closed - Opened by mtzguido 7 months ago

#57 - snap, bracing for https://github.com/FStarLang/FStar/pull/3256

Pull Request - State: closed - Opened by mtzguido 7 months ago

#56 - Misc

Pull Request - State: closed - Opened by mtzguido 7 months ago

#55 - `inline_for_extraction` breaks extraction

Issue - State: closed - Opened by gebner 7 months ago - 1 comment

#54 - Misc async changes

Pull Request - State: closed - Opened by mtzguido 7 months ago

#53 - Nik injectivity

Pull Request - State: closed - Opened by nikswamy 7 months ago

#52 - Annotated function types incorrectly type-check conjunctions

Issue - State: closed - Opened by gebner 7 months ago - 1 comment

#51 - Redefining permissions directly as reals

Pull Request - State: closed - Opened by aseemr 7 months ago

#50 - Fixes for new real numbers interface in F*

Pull Request - State: closed - Opened by mtzguido 7 months ago - 1 comment

#49 - The task pool implementation (WIP)

Pull Request - State: closed - Opened by mtzguido 7 months ago - 2 comments

#48 - library: rename Pulse.Lib.Par.Pledge.* into Pulse.Lib.Pledge.*

Pull Request - State: closed - Opened by mtzguido 7 months ago

#47 - Arrays: proving the smallness of pts_to and pts_to_range

Pull Request - State: closed - Opened by mtzguido 7 months ago

#46 - SpinLock: prove (a version of) the injectivity lemma

Pull Request - State: closed - Opened by mtzguido 7 months ago

#45 - Pulse.Class.Small: a class for small vprops

Pull Request - State: closed - Opened by mtzguido 7 months ago

#44 - Misc changes

Pull Request - State: closed - Opened by mtzguido 7 months ago

#43 - bump rlimits

Pull Request - State: closed - Opened by mtzguido 8 months ago

#42 - Misc pcm libs and examples

Pull Request - State: closed - Opened by aseemr 8 months ago

#41 - Trying to remove fractional permission from the cells in PulseCore heap

Pull Request - State: closed - Opened by aseemr 8 months ago - 1 comment

#40 - Fix for #33

Pull Request - State: closed - Opened by aseemr 8 months ago

#39 - Some internal cleanup

Pull Request - State: closed - Opened by aseemr 8 months ago

#38 - Resourceful invariants and associated libraries

Pull Request - State: closed - Opened by aseemr 8 months ago

#37 - "Not well-typed" with weak invariant

Issue - State: open - Opened by gebner 8 months ago

#36 - Incorrect error position for implicit instantiation

Issue - State: open - Opened by gebner 8 months ago

#35 - Assertion failure when arguments are filled in via unification

Issue - State: open - Opened by gebner 8 months ago

#34 - Typeclass arguments in Pulse functions

Issue - State: closed - Opened by mtzguido 8 months ago

#33 - Cannot admit existential

Issue - State: closed - Opened by mtzguido 8 months ago

#32 - rewrite components not checked?

Issue - State: open - Opened by mtzguido 8 months ago - 1 comment

#31 - Should not accept `opens` in ghost functions (at least for now)

Issue - State: closed - Opened by mtzguido 8 months ago

#30 - Removing term from Pulse AST, instead use F* reflection terms and expose a term view to the Pulse checker

Pull Request - State: closed - Opened by aseemr 8 months ago

#29 - Strange stack overflow

Issue - State: closed - Opened by mtzguido 8 months ago - 2 comments

#28 - Pulse.Lib.SmallTrade: add a small version of trades

Pull Request - State: closed - Opened by mtzguido 8 months ago

#27 - Use a typeclass for non informative types

Pull Request - State: closed - Opened by mtzguido 8 months ago

#26 - Misc patches

Pull Request - State: closed - Opened by mtzguido 8 months ago

#25 - Extract `Pulse.Lib.SpinLock.release` to C

Pull Request - State: closed - Opened by aseemr 8 months ago

#24 - Stack overflow on rewrite

Issue - State: closed - Opened by mtzguido 8 months ago - 1 comment

#23 - Fixing #11

Pull Request - State: closed - Opened by aseemr 8 months ago

#22 - Unification of arguments in matcher: syntatic equality, unifier, SMT...?

Issue - State: open - Opened by mtzguido 8 months ago - 2 comments

#21 - Cannot extract Pulse.Lib.SpinLock.release

Issue - State: closed - Opened by tahina-pro 8 months ago - 1 comment

#20 - Extract DPE to C

Pull Request - State: closed - Opened by tahina-pro 9 months ago - 3 comments

#19 - A stratified heap with two universes, enabling storing "small" heap predicates in the larger heap

Pull Request - State: closed - Opened by nikswamy 9 months ago - 1 comment

#18 - Error when building locally with make.

Issue - State: open - Opened by mushrm88 9 months ago - 1 comment

#17 - Spurious `()` function arguments in ML terms extracted from Pulse

Issue - State: closed - Opened by tahina-pro 9 months ago - 2 comments

#16 - Bump rlimit.

Pull Request - State: closed - Opened by gebner 9 months ago - 1 comment

#15 - Refactor examples makefile to simplify extraction tests.

Pull Request - State: open - Opened by gebner 9 months ago

#14 - Use HNF to normalize annotated computation types.

Pull Request - State: closed - Opened by gebner 9 months ago - 2 comments

#13 - Type annotations cannot have more than one layer of definitions

Issue - State: closed - Opened by gebner 9 months ago

#12 - Core: remove explicit preconditions for `compatible x x`

Pull Request - State: closed - Opened by mtzguido 9 months ago

#11 - Pulse re-typechecks postconditions of called functions

Issue - State: closed - Opened by gebner 9 months ago - 1 comment

#10 - Ghost functions have a model supporting their erasure

Pull Request - State: closed - Opened by nikswamy 9 months ago

#9 - Cannot extract functions with type annotations using Karamel

Issue - State: closed - Opened by gebner 9 months ago - 1 comment

#8 - Miscompilation with `inline_for_extraction` on recursive functions

Issue - State: closed - Opened by gebner 9 months ago

#7 - Wishlist: use real literals instead of the current fractional permission inductive

Issue - State: closed - Opened by mtzguido 9 months ago - 1 comment

#6 - Enforcing in PulseCore that ghost computations cannot use witness/recall

Pull Request - State: closed - Opened by nikswamy 9 months ago

#5 - Some utilities on invariant names

Pull Request - State: closed - Opened by nikswamy 9 months ago

#4 - Refactor Makefiles, maximize parallel verification for CI

Pull Request - State: closed - Opened by tahina-pro 9 months ago

#3 - Show that Array.length always SizeT.fits.

Pull Request - State: closed - Opened by gebner 9 months ago

#2 - Misc changes to task pool

Pull Request - State: closed - Opened by mtzguido 9 months ago

#1 - Fixing VS Code configs

Pull Request - State: closed - Opened by mtzguido 9 months ago

GitHub / fstarlang/pulse issues and pull requests