search

DeepSpec / InteractionTrees

A Library for Representing Recursive and Impure Programs in Coq
MIT License
198 stars 50 forks source link

Secure #215

Closed lag47 closed 2 years ago

lag47 commented 2 years ago

This pull request brings the work done with Dijkstra Monads over ITrees and secure indistinguishability over ITrees into the master branch. This includes the formalization of ITraces, now contained in a separate directory from Dijkstra Monads.

lag47 commented 2 years ago

Appears to have some build issues I did not notice, I will close this request, fix it and then recreate it

YaZko commented 2 years ago

Is there any hope to disentangle it into smaller PRs by any chance? I'd be interested into looking into the code in details but the diff is a bit daunting right now and mixes in a lot of orthogonal stuffs.

lag47 commented 2 years ago

Sure, given a little time I could make it three pull requests. The dependencies would make it easy to first introduce ITraces, then Dijkstra monads, then Secure as separate pull requests