more docs

LeanBoogie/Dsl.lean

@@ -163,6 +163,13 @@ variable {E : Q(Type -> Type)}
      and it decides to true. If no blocks match, we `spin`.
      We currently use this approach.
      This approach does not faithfully model Boogie semantics, and we should move away from it.
+
+  ### Obtaining executable code
+  When you do use `AssumeAssert` and `Choice` (See (2) in the previous section), you may want to obtain
+  executable code. For `AssumeAssert` this is easy: You simply provide a proof via an axiom, e.g. `sorry`.
+  For `Choice` this is not as straightforward. However, often programs are only non-deterministic on
+  the surface, and the leading assumes for each block are disjoint, in which case we would still
+  like to avoid forking the entire program state.
 -/
 
 

LeanBoogie/Spec/ITree0W.lean

@@ -4,7 +4,11 @@ import LeanBoogie.Spec.Theta
 namespace LeanBoogie
 open ITree
 
--- # ITree Specs Without Effects [DM4Ever]
+/- # ITree Specs Without Effects [DM4Ever]
+  Without effects, if our tree diverges, we know that `spin` is the canonical representative of it,
+  and for convergence it must be `.ret _`.
+  With effects, this gets non-trivial, and we might have
+-/
 -- See section 4 of "Dijkstra Monads for ever".
 
 -- Corresponding computation monad: `ITree Empty`.

lake-manifest.json

@@ -81,14 +81,14 @@
    "inputRev": "v4.12.0",
    "inherited": true,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/Kiiyya/QpfTypes.git",
+  {"url": "https://github.com/alexkeizer/QpfTypes.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "67e99ac5339969f1fe220100c3c5f05ea37e20f9",
+   "rev": "9cfc50cfa0dc561f5b7a1bf08e693b2a52172383",
    "name": "qpf",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "67e99ac5339969f1fe220100c3c5f05ea37e20f9",
+   "inputRev": "9cfc50cfa0dc561f5b7a1bf08e693b2a52172383",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/lean-auto.git",

lakefile.lean

@@ -6,11 +6,6 @@ package "lean-boogie" where
 
 @[default_target]
 lean_lib LeanBoogie where
-  -- ## for 4.12:
-  require qpf from git "https://github.com/Kiiyya/QpfTypes.git" @ "67e99ac5339969f1fe220100c3c5f05ea37e20f9" -- https://github.com/alexkeizer/QpfTypes/pull/52
+  require qpf from git "https://github.com/alexkeizer/QpfTypes.git" @ "9cfc50cfa0dc561f5b7a1bf08e693b2a52172383"
   require auto from git "https://github.com/leanprover-community/lean-auto.git" @ "680d6d58ce2bb65d15e5711d93111b2e5b22cb1a" -- 4.12
   require Duper from git "https://github.com/leanprover-community/duper.git" @ "25c3ea88da2505158998eea07f40b07c0cdfe5ba"
-
--- @[default_target]
--- lean_exe "lean-boogie" where
---   root := `Main