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
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • Iris
  • Issues
  • #349

Closed
Open
Opened Sep 21, 2020 by Ralf Jung@jungOwner

Parameterize WP (and more) by the notion of fancy update

For Perennial, @jtassaro developed a notion of "fancy updates" that satisfies all the laws we have in Iris, plus way more. Unfortunately this means we cannot directly use anything from base_logc/lib and above, even though all these proofs do go through unchanged.

This change is likely not canonical enough to be upstreamable, and I see no way to make our notion of fancy updates itself general enough that @jtassaro's update are an instance of them. The design space is very wide open here.

It would thus be useful if we could parameterize the definition of WP by the notion of fancy update, and similar for some of the things in base_logic/lib -- everything that mentions fancy updates, basically (or at least anything useful; I don't think it is worth doing this with STS and auth). Maybe some things can be changed to use basic updates instead of fancy updates, which would avoid the need for parameterization.

Even semantic invariants themselves can be defined generally for any fancy update; the only thing that each update would need to prove is the allocation lemma(s).

@robbertkrebbers what do you think?

Assignee
Assign to
None
Milestone
None
Assign milestone
Time tracking
None
Due date
None
Reference: iris/iris#349