Skip to content
Snippets Groups Projects

Repository graph

You can move around the graph by using the arrow keys.
Select Git revision
  • ci/debug
  • ci/for_proph
  • ci/janno/debug-opam
  • ci/janno/let_bind_envs
  • ci/janno/vmcast
  • ci/joe/compact_ipm
  • ci/joe/compact_ipm_remaining
  • ci/joe/compact_ipm_simple
  • ci/msammler/iris-coq-seal_big_opM
  • ci/ralf/pm_red
  • ci/ralf/retime
  • ci/ralf/set_unfold_elements
  • ci/ralf/transfinite
  • ci/robbert/faster_iDestruct
  • ci/robbert/faster_iDestruct2
  • ci/robbert/faster_iFresh_joe
  • ci/robbert/into_val_pures
  • ci/robbert/kill_locked_value_lambdas
  • ci/robbert/naive_solver
  • ci/robbert/set_unfold
  • iris-3.2.0
  • iris-3.1.0
  • iris-3.0.0
  • iris-2.0
  • iris-2.0-rc2
  • iris-2.0-rc1
  • iris-1.1
  • iris-1.0
  • hope-2015-coq-1
  • appendix-1.0.0
  • appendix-1
31 results
Created with Raphaël 2.2.01Jun31May302928272625161514131211723Apr141311109872131Mar30292827252423201918171613121186543228Feb27262423222120191817161514131195432131Jan3024Oct76517Jul1198621Jun2019654331May2928come more small commentsdocument some thingsconstruct a CMRAExt for Agreement. This completes the CMRAExt for the final world, which completes the entire construction - it's all admit-free! :-))show that finite partial functions preserve "CMRAExt"adapt Iris to the less-dependant Agreement constructionmake the library work without any axiomsfix iris_check. "make" works again! First time in months! Yay :Dshow stateless lifting, completing iris_metaestablish stateful liftingintroduce "CMRAExt", and extension property on CMRAs. We will need it to show that later commutes with star. For now, just assume it holds.complete proofs of derived rulesshow the derived view shift rulesplay with the simplification parametersprove WP rulesprove allocation of invariantsprove ghost update rulereestablish general adequacyMerge remote-tracking branch 'origin/master' into hackgreementprove some wp rules: ret, bind, preVS, postVSprove pvsTrans, pvsImpl, pvsFrameprove pvsOpen and pvsCloseworld satisfaction was wrong. fix it.redo the way we define ownershiptune simplification of equiv, pord, distdefine view shifts and weakest-pre, and show they are all the things though ought to be (downclosed, non-expansive, monotone)show that world satisfaction is non-expansivedefine world satisfaction and show it is downclosedchange SPred to be "bounded": they must hold a step-index 0. Change SPred-n-equality to require equivalence even at level n.nicer PI tacticstowards defining world satisfactionshow the lemmas we need about composing a finmapWeaken axiom fill_value to is_value K[e] -> is_value e.make everything (up until iris_core) compile againmove them all to the new Finmapcomplete the new finmap CMRAprove equivalence of the two ways to get an order on finmapsprovide pointwise composition of two maps; use to to establish an RAcomplete the reordering proofreduce extensionality of fdFold to a commutativity lemma about fold_right (on lists) and permutations (of lists)srengthen the induction principle and show euqalities such that the characterization of fdFold can be shown using fdRect