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
  • #359

Closed
Open
Opened Oct 12, 2020 by Tej Chajed@tchajedDeveloper

Use the IPM to prove some example IPM extension theorems

The current proofs for some HeapLang tactics use a bunch of separation logic theorems manually, like this proof:

Lemma tac_wp_free Δ Δ' s E i K l v Φ :
  MaybeIntoLaterNEnvs 1 Δ Δ' →
  envs_lookup i Δ' = Some (false, l ↦ v)%I →
  (let Δ'' := envs_delete false i false Δ' in
   envs_entails Δ'' (WP fill K (Val $ LitV LitUnit) @ s; E {{ Φ }})) →
  envs_entails Δ (WP fill K (Free (LitV l)) @ s; E {{ Φ }}).
Proof.
  rewrite envs_entails_eq=> ? Hlk Hfin.
  rewrite -wp_bind. eapply wand_apply; first exact: wp_free.
  rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
  rewrite -Hfin wand_elim_r (envs_lookup_sound' _ _ _ _ _ Hlk).
  apply later_mono, sep_mono_r, wand_intro_r. rewrite right_id //.
Qed.

It would be much nicer to use the proof mode to do these proofs, which is also nicely circular because we're extending the proof mode using the proof mode. For example, the above proof can be written:

  rewrite envs_entails_eq=> ? Hlk Hfin.
  rewrite into_laterN_env_sound.
  iIntros "HΔ'".
  iApply wp_bind.
  pose proof (envs_lookup_sound' _ false _ _ _ Hlk) as HΔ'split.
  set (Δ'':=envs_delete false i false Δ') in *.
  iDestruct (HΔ'split with "HΔ'") as "[Hl HΔ'']".
  iApply (wp_free with "Hl").
  iNext. iIntros "_".
  iApply (Hfin with "HΔ''").

This proof isn't shorter but you can figure out how to write such a proof using only the proof mode rather than convoluted uses of theorems like sep_mono_r and wand_intro_r. This particular case become slightly messier because if you do iDestruct envs_lookup_sound with "HΔ'" then the proof mode reduces envs_delete and the result is horrendous.

I don't think we need to re-do all of the proofs; I'm thinking having a few such examples would go a long way as examples that demonstrate how to extend the IPM in a nice way. We couldn't port all of the theorems anyway since of course some of these theorems are actually used to implement the IPM.

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