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/general-contractive
  • ci/hai/siProp
  • ci/janno/strict-tc-resolution
  • ci/msammler/nb_state
  • ci/ralf/Z_of_nat
  • ci/ralf/bi-language
  • ci/robbert/big_op_binder
  • ci/robbert/contractive_ne
  • ci/robbert/coq_bug_7773
  • ci/robbert/faster_iDestruct
  • ci/robbert/faster_iDestruct2
  • ci/robbert/faster_iFresh_joe
  • ci/robbert/frame_fractional
  • ci/robbert/iFrame
  • ci/robbert/into_fupd
  • ci/robbert/into_val_pures
  • ci/robbert/kill_locked_value_lambdas
  • ci/robbert/mapsto_persist
  • iris-4.0.0
  • iris-3.6.0
  • iris-3.5.0
  • iris-3.4.0
  • iris-3.3.0
  • 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
36 results
Created with Raphaël 2.2.03Jun2131May302928272625161514131211723Apr141311109872131Mar30292827252423201918171613121186543228Feb27262423222120191817161514131195432131Jan3024Oct76517Jul1198621Jun2019654331May2928prove the last missing view shift rulesadd sugar for defining SPreds, this also makes them print nicer in some caseswork on timelessnessshow the missing axioms for later and boxsimplify wsat a bitcome 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 CMRA