5 ms·
We mean Haskell-style software transactional memory (STM). We call it a primitive because it is not defined in Rocq itself; instead, it is only exposed to the R
by joomy 8mo ago
We mean Haskell-style software transactional memory (STM). We call it a primitive because it is not defined in Rocq itself; instead, it is only exposed to the Rocq programmer through an interface.
- GregarianChild 8mo agoSince the point of program extraction from a prover is correctness, I wonder what kind of assertions you prove for STM in Rocq.
- mzweav 8mo agoI'm the other dev of Crane. Our current plan is to use BRiCk (https://skylabsai.github.io/BRiCk/index.html https://skylabsai.github.io/BRiCk/index.html) to directly verify that the C++ implementation our STM primitives are extracted to matches the functional specification of STM. Having done that, we can then axiomatize the functional specification over our monadic, interaction tree interface and reason directly over the functional code in Rocq without needing to worry about the gritty details of the C++ interpretation.
- GregarianChild 8mo agoThanks. I hope you publish this. I imagine https://github.com/bloomberg/crane/blob/main/theories/Monads/STM.v https://github.com/bloomberg/crane/blob/main/theories/Monads... is the functional specification of STM. I see that you use ITrees. WHat's the reason for not using Choice Trees that tend to be easier for handling non-determinism?
- joomy 8mo agoOur 2 page extended abstract was more like a preannouncement. We hope to have a draft of the full paper by the end of the year. And we're not opposed to choice trees. I personally am not too familiar with them but there's time to catch up on literature. :)
- GregarianChild 8mo agoI'm not an expert in this field, but the way I understand it is that Choice Trees extend the ITree signature by adding a choice operator. Some variant of this: ITrees: CoInductive itree (E : Type -> Type) (R : Type) : Type := | Ret (r : R) | Tau (t : itree E R) | Vis {T : Type} (e : E T) (k : T -> itree E R) ChoiceTrees: CoInductive ctree (E : Type -> Type) (C : Type -> Type) (R : Type) : Type := | Ret (r : R) | Tau (t : ctree E C R) | Vis {T : Type} (e : E T) (k : T -> ctree E C R) | Choice {T : Type} (c : C T) (k : T -> ctree E C R) One can see "Choice" constructor as modelling internal non-determinism, complementing the external non-determinism that ITrees already allow with "Vis" and that arises from interaction with the environment. (Process calculi like CCS, CSP and Pi, as well as session types and linear logic also make this distinction).
- mzweav 8mo agoOoooh! Those indeed look fun! :)
- GregarianChild 8mo agoThere are some issues arising from size inconsistencies (AKA Cantor's Paradox) if / when you try to fit the representation of all internal choices (this could be infinite) into a small universe of a theorem prover's inductive types. The ChoiceTree paper solves this with a specific encoding. I'm currently wondering how to port this trick from COq/Rocq to Lean4.