Skip to content
GitLab
Projects Groups Topics Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Register
  • Sign in
  • Iris Iris
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributor statistics
    • Graph
    • Compare revisions
  • Issues 171
    • Issues 171
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 15
    • Merge requests 15
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • IrisIris
  • Merge requests
  • !225

Prophecy variables with lists

  • Review changes

  • Download
  • Email patches
  • Plain diff
Merged Rodolphe Lepigre requested to merge lepigre/iris:prophecy_list into master Mar 19, 2019
  • Overview 19
  • Commits 5
  • Pipelines 0
  • Changes 5

We generalize the prophecy variable mechanism so that prophecy variables can be resolved several times. A prophecy variable is hence associated to a list of values. This means that several "observations" can be made for a given prophecy variables, but the overall intuition remains the same. The main difference is in the specification of the resolve operation:

Lemma wp_resolve_proph (p : proph_id) (vs : list val) (v : val) :
  {{{ proph p vs }}}
    ResolveProph (Val $ LitV $ LitProphecy p) (Val v)
  {{{ vs', RET (LitV LitUnit); ⌜vs = v::vs'⌝ ∗ proph p vs' }}}.

Note that resolving p consumes only the first of the list vs, and the ownership of proph p vs' (where vs' is the tail of vs) is asserted in the postcondition.

In any case, everything remains very simple, and even simpler than before. The main difference being that we replace an option by a list.

@jung do you have anything to add?

Assignee
Assign to
Reviewers
Request review from
Time tracking
Source branch: prophecy_list