LinkedLists.lean

import Iris.HeapLang

namespace LinkedLists
open Iris HeapLang

-- # Case Study: Linked Lists
section linked_lists
variable [HeapLangGS hlc GF]

-- In this chapter, we will study several functions on linked lists. To
-- do this, we must first agree on what a linked list is. In HeapLang, we
-- can implement linked lists as chains of pointers. We define this
-- formally with a predicate, which we denote [isList]. This predicate
-- turns a list of values [xs] into a predicate describing the structure
-- of the linked list.

def isList (l : Val) (xs : List Val) : IProp GF :=
  match xs with
  | [] => iprop(⌜l = hl_val(none())⌝)
  | x :: xs => iprop%
    ∃ (hd : Loc) (l' : Val), ⌜l = hl_val(some(#hd))⌝ ∗ hd ↦ hl_val((&x, &l')) ∗ isList l' xs

-- We can now define HeapLang functions that act on lists, such as [inc].
-- The [inc] function recursively increments all the values of a list.

def inc : Val := hl_val%
  rec inc l :=
    match l with
    | none() => #()
    | some(hd) =>
      let x := fst(!hd);
      let l' := snd(!hd);
      hd ← (x + #1, l');
      inc l'

-- Intuitively, the specification we give for this function should state
-- that the linked list should only contain integers and that, after
-- executing the function, each integer has been incremented. As such, we
-- parametrise the specification not by a list of values, but by a list
-- of integers. We then map each integer to a HeapLang value using [# _],
-- allowing us to use the [isList] predicate.
theorem inc_spec (l : Val) (xs : List Int) :
    {{ (isList l ((fun x : Int => hl_val(#x)) <$> xs) : IProp GF) }}
      hl(&inc &l)
    {{ RET hl_val(#()); isList l ((fun x => hl_val(#(x + 1 : Int))) <$> xs) }} := by
  -- The proof proceeds by structural induction in [xs]. As [l] changes in each
  -- iteration, we must universally quantify over it to strengthen the induction
  -- hypothesis.
  induction xs generalizing l with
  | nil =>
    -- PORTING: iris-lean does not support iintro with [→] and [←]
    iintro %Φ Hil HΦ
    isimp [Functor.map, List.map_nil, isList] in Hil HΦ
    icases Hil with %Hil
    wp_rec
    isimp [Hil]
    wp_match
    imodintro
    iapply HΦ $$ %Hil
  | cons x xs ih =>
    iintro %Φ Hil HΦ
    isimp [Functor.map, List.map_cons, isList] in Hil HΦ
    icases Hil with ⟨%hd, %l', %hl, hhd, hxs⟩
    ihave iH := ih l' $$ %Φ hxs
    -- PROBLEM: wp_rec does not remove ▷ from iH
    wp_rec
    isimp [hl]
    wp_load
    wp_load
    wp_store
    wp_pures
    sorry

end linked_lists