Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
I
Iris
  • Project overview
    • Project overview
    • Details
    • Activity
    • Releases
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 122
    • Issues 122
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
  • Merge Requests 18
    • Merge Requests 18
  • CI / CD
    • CI / CD
    • Pipelines
    • Jobs
    • Schedules
  • Operations
    • Operations
    • Incidents
    • Environments
  • Analytics
    • Analytics
    • CI / CD
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Members
    • Members
  • Collapse sidebar
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
  • Iris
  • Iris
  • Merge Requests
  • !225

Merged
Opened Mar 19, 2019 by Rodolphe Lepigre@lepigreDeveloper

Prophecy variables with lists

  • Overview 19
  • Commits 5
  • 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
Reviewer
Request review from
None
Milestone
None
Assign milestone
Time tracking
Reference: iris/iris!225
Source branch: prophecy_list

Revert this merge request

This will create a new commit in order to revert the existing changes.

Switch branch
Cancel
A new branch will be created in your fork and a new merge request will be started.

Cherry-pick this merge request

Switch branch
Cancel
A new branch will be created in your fork and a new merge request will be started.