lambda-rust merge requestshttps://gitlab.rts.mpi-sws.org/iris/lambda-rust/-/merge_requests2024-09-09T14:26:34Zhttps://gitlab.rts.mpi-sws.org/iris/lambda-rust/-/merge_requests/37Expose atomic lifetimes in the API, end many in a single step2024-09-09T14:26:34ZIsaac van Bakelisaac.vanbakel@inf.ethz.chExpose atomic lifetimes in the API, end many in a single stepThis turns out to be useful for my borrow-checker proofs, which require the ability to mass-end lifetimes to model loan termination without generating an inordinate number of laters.
This extracts the proof that atomic lifetimes can end...This turns out to be useful for my borrow-checker proofs, which require the ability to mass-end lifetimes to model loan termination without generating an inordinate number of laters.
This extracts the proof that atomic lifetimes can end from `lft_create_strong` as a standalone lemma, and then proves a stronger
version of that lemma that terminates arbitrarily many atomic lifetimes at the same time (which is allowed because they don't overlap.) In fact, I think this generalises to being allowed to terminate any number of lifetimes at in the same step, but that requires some more set/multiset theory to prove, I think.
To prove this, I require a few data structure lemmas which I am trying to upstream. Two are going into iris/iris!1049. The `gset_to_map` mass-update lemma is harder to generalise - I thought about including it upstream, but it's rather specific here and it doesn't seem to have a nice "kernel" to extract out that would keep the proof burden in these changes small.https://gitlab.rts.mpi-sws.org/iris/lambda-rust/-/merge_requests/27add more operations to the language2023-03-23T21:04:22ZJason Huadd more operations to the languageThis is the first MR to split https://gitlab.mpi-sws.org/iris/lambda-rust/-/merge_requests/26 into multiple ones.This is the first MR to split https://gitlab.mpi-sws.org/iris/lambda-rust/-/merge_requests/26 into multiple ones.https://gitlab.rts.mpi-sws.org/iris/lambda-rust/-/merge_requests/26create various data types including bounded integers and array2022-12-22T23:21:41ZJason Hucreate various data types including bounded integers and arrayhttps://gitlab.rts.mpi-sws.org/iris/lambda-rust/-/merge_requests/25RefMut can be considered as Sync2022-02-20T15:28:37ZJacques-Henri JourdanRefMut can be considered as SyncI figured out that RefMut could be considered as Sync even though Rust stdlib does not consider it as such.
I find this is an interesting fact, so I added it to our formalization. This is not particularly useful for writing programs, be...I figured out that RefMut could be considered as Sync even though Rust stdlib does not consider it as such.
I find this is an interesting fact, so I added it to our formalization. This is not particularly useful for writing programs, because a value of type `&RefMut<T>` can be WLOG unnested to a `&T`, but still this is interesting from a type system's perspective.https://gitlab.rts.mpi-sws.org/iris/lambda-rust/-/merge_requests/21Pinning2021-08-04T11:40:58ZMichael SammlerPinning