Library zoo.language.state

Require Import stdpp.gmap.

Require Import iris.algebra.ofe.

Require Import zoo.prelude.
Require Export zoo.language.syntax.
Require Import zoo.options.

Implicit Type l : location.
Implicit Type v w : val.
Implicit Type vs : list val.
Implicit Type h : gmap location val.

Record := Header
  { header ۰ tag : nat
  ; header ۰ size : nat
  }.
Add Printing Constructor header.

Record state :=
  { state ۰ headers : gmap location header
  ; state ۰ heap : gmap location val
  ; state ۰ locals : list val
  ; state ۰ prophets : gset prophet_id
  }.
Implicit Type σ : state.

Canonical state ۰ O {SI : sidx} :=
  leibnizO state.

#[global] Instance state ｰ inhabited : Inhabited state :=
  populate
    {|state ۰ headers := inhabitant
    ; state ۰ heap := inhabitant
    ; state ۰ locals := inhabitant
    ; state ۰ prophets := inhabitant
    |}.

Definition state ۰ update_heap f σ :=
  {|state ۰ headers := σ.(state ۰ headers)
  ; state ۰ heap := f σ.(state ۰ heap)
  ; state ۰ locals := σ.(state ۰ locals)
  ; state ۰ prophets := σ.(state ۰ prophets)
  |}.
Definition state ۰ update_headers f σ :=
  {|state ۰ headers := f σ.(state ۰ headers)
  ; state ۰ heap := σ.(state ۰ heap)
  ; state ۰ locals := σ.(state ۰ locals)
  ; state ۰ prophets := σ.(state ۰ prophets)
  |}.
Definition state ۰ update_locals f σ :=
  {|state ۰ headers := σ.(state ۰ headers)
  ; state ۰ heap := σ.(state ۰ heap)
  ; state ۰ locals := f σ.(state ۰ locals)
  ; state ۰ prophets := σ.(state ۰ prophets)
  |}.
Definition state ۰ update_prophets f σ :=
  {|state ۰ headers := σ.(state ۰ headers)
  ; state ۰ heap := σ.(state ۰ heap)
  ; state ۰ locals := σ.(state ۰ locals)
  ; state ۰ prophets := f σ.(state ۰ prophets)
  |}.

Definition state ۰ set_location l v :=
  state ۰ update_heap $ insert l v.
Definition state ۰ set_header l hdr :=
  state ۰ update_headers $ insert l hdr.
Definition state ۰ set_local tid v :=
  state ۰ update_locals $ insert tid v.
Definition state ۰ add_local v :=
  state ۰ update_locals $ (.++ [v]).
Definition state ۰ add_prophet pid :=
  state ۰ update_prophets $ ({[pid ]} ∪.).

Section chunk.
  Context {A : Type}.

  Implicit Type x y : A.
  Implicit Type xs : list A.
  Implicit Type m : gmap location A.

  Fixpoint chunk l xs : gmap location A :=
    match xs with
    | [] ⇒
        ∅
    | x :: xs ⇒
        <[l := x]> (chunk (l +ₗ 1) xs )
    end.
  #[global] Arguments chunk _ !_ / : assert.

  Lemma chunk ｰ singleton l x :
    chunk l [x] = {[l := x ]}.
  Lemma chunk ｰ lookup l xs 𝑙 y :
    chunk l xs !! 𝑙 = Some y ↔
      ∃ i,
      (0 ≤ i)%Z ∧
      𝑙 = l +ₗ i ∧
      xs !! ₊i = Some y.
  Lemma chunk ｰ map ｰ disjoint m l xs :
    ( ∀ i,
      i < length xs →
      m !! (l +ₗ i ) = None
    ) →
    chunk l xs ##ₘ m.
End chunk.

Definition state ۰ alloc l hdr vs σ :=
  {|state ۰ headers := <[l := hdr ]> σ.(state ۰ headers )
  ; state ۰ heap := chunk l vs ∪ σ.(state ۰ heap)
  ; state ۰ locals := σ.(state ۰ locals)
  ; state ۰ prophets := σ.(state ۰ prophets)
  |}.

Definition state ۰ alloc_condition l sz σ :=
  σ.(state ۰ headers) !! l = None ∧
  σ.(state ۰ heap) !! l = None ∧
    ∀ i,
    i < sz →
      σ.(state ۰ headers) !! (l +ₗ i ) = None ∧
      σ.(state ۰ heap) !! (l +ₗ i ) = None.

Definition state ۰ fresh ۰ dom σ :=
  dom σ.(state ۰ headers) ∪
  dom σ.(state ۰ heap).
Definition state ۰ fresh σ :=
  location ۰ fresh $ state ۰ fresh ۰ dom σ.

Lemma state ۰ alloc_condition ｰ fresh sz σ :
  state ۰ alloc_condition (state ۰ fresh σ) sz σ.