Library zoo.program_logic.structural_equality

Require Import zoo.prelude.
Require Import zoo.common.list.
Require Import zoo.base.
Require Import zoo.options.

Implicit Type b : bool.
Implicit Type tag : nat.
Implicit Type n : Z.
Implicit Type l : location.
Implicit Type gen : generativity.
Implicit Type v w : val.
Implicit Type vs : list val.
Implicit Type lv : lowval.

#[local] Definition __zoo_recs := (
  𝗿𝗲𝗰𝘀 "structeq" "v1" "v2" →
    𝗶𝗳 𝗶𝗺𝗺𝗲𝗱𝗶𝗮𝘁𝗲 "v1" 𝘁𝗵𝗲𝗻
      𝗶𝗳 𝗶𝗺𝗺𝗲𝗱𝗶𝗮𝘁𝗲 "v2" 𝘁𝗵𝗲𝗻
        "v1" == "v2"
      𝗲𝗹𝘀𝗲
        false
    𝗲𝗹𝘀𝗲 𝗶𝗳 𝗶𝗺𝗺𝗲𝗱𝗶𝗮𝘁𝗲 "v2" 𝘁𝗵𝗲𝗻
      false
    𝗲𝗹𝘀𝗲 (
      𝘁𝗮𝗴 "v1" == 𝘁𝗮𝗴 "v2" 𝗮𝗻𝗱
      𝗹𝗲𝘁 "sz" = 𝘀𝗶𝘇𝗲 "v1" 𝗶𝗻
      "sz" == 𝘀𝗶𝘇𝗲 "v2" 𝗮𝗻𝗱
      "structeq_aux" "v1" "v2" "sz"
    )
  𝘄𝗶𝘁𝗵 "structeq_aux" "v1" "v2" "i" →
    𝗶𝗳 "i" == 0 𝘁𝗵𝗲𝗻
      true
    𝗲𝗹𝘀𝗲
      𝗹𝗲𝘁 "i" = "i" - 1 𝗶𝗻
      "structeq" (𝗹𝗼𝗮𝗱 "v1" "i") (𝗹𝗼𝗮𝗱 "v2" "i") 𝗮𝗻𝗱
      "structeq_aux" "v1" "v2" "i"
)%zoo_recs.
Definition structeq :=
  ValRecs 0 __zoo_recs.
#[local] Definition structeq۰aux :=
  ValRecs 1 __zoo_recs.
#[global] Instance :
  AsValRecs' structeq 0 __zoo_recs [
    structeq ;
    structeq۰aux
  ].
#[global] Instance :
  AsValRecs' structeq۰aux 1 __zoo_recs [
    structeq ;
    structeq۰aux
  ].

Notation "e1 = e2" := (
  App (App (Val structeq) e1%E) e2%E
)(at level 70,
  no associativity
) : expr_scope.
Notation "e1 ≠ e2" := (
  Unop UnopNeg (App (App (Val structeq) e1%E) e2%E)
)(at level 70,
  no associativity
) : expr_scope.

Record structeq۰field := StructeqField
  { structeq۰field۰dfrac : dfrac
  ; structeq۰field۰val : val
  }.
Add Printing Constructor structeq۰field.
Implicit Type fld : structeq۰field.

#[global] Instance structeq۰fieldｰinhabited : Inhabited structeq۰field :=
  populate
    {|structeq۰field۰dfrac := inhabitant
    ; structeq۰field۰val := inhabitant
    |}.

Record structeq۰block := StructeqBlock
  { structeq۰block۰tag : nat
  ; structeq۰block۰fields : list structeq۰field
  }.
Add Printing Constructor structeq۰block.
Implicit Type blk : structeq۰block.
Implicit Type footprint : gmap location structeq۰block.

#[global] Instance structeq۰blockｰinhabited : Inhabited structeq۰block :=
  populate
    {|structeq۰block۰tag := inhabitant
    ; structeq۰block۰fields := inhabitant
    |}.

Fixpoint val۰traversable footprint v :=
  match v with
  | ValBool _
  | ValInt _ ⇒
      True
  | ValLoc l ⇒
      l ∈ dom footprint
  | ValBlock _ _ vs ⇒
      Forall' (val۰traversable footprint) vs
  | _ ⇒
      False
  end.
#[global] Arguments val۰traversable _ !_ / : assert.

Section zoo۰G.
  Context `{zoo۰G : !ZooG Σ}.

  Definition structeq۰footprint footprint : iProp Σ :=
    [∗ map] l ↦ blk ∈ footprint,
      l ↦ₕ Header blk.(structeq۰block۰tag) (length blk.(structeq۰block۰fields)) ∗
      [∗ list] i ↦ fld ∈ blk.(structeq۰block۰fields),
        (l +ₗ i) ↦{fld.(structeq۰field۰dfrac)} fld.(structeq۰field۰val) ∗
        ⌜val۰traversable footprint fld.(structeq۰field۰val)⌝.

  Lemma structeq۰footprintｰempty :
    ⊢ structeq۰footprint ∅.

  Lemma structeq۰footprintｰheader {footprint} l blk :
    footprint !! l = Some blk →
    structeq۰footprint footprint ⊢
    l ↦ₕ Header blk.(structeq۰block۰tag) (length blk.(structeq۰block۰fields)).

  Lemma structeq۰footprintｰlookup {footprint} l blk (i : nat) fld :
    footprint !! l = Some blk →
    blk.(structeq۰block۰fields) !! i = Some fld →
    structeq۰footprint footprint ⊢
      (l +ₗ i) ↦{fld.(structeq۰field۰dfrac)} fld.(structeq۰field۰val) ∗
      ⌜val۰traversable footprint fld.(structeq۰field۰val)⌝ ∗
      ( (l +ₗ i) ↦{fld.(structeq۰field۰dfrac)} fld.(structeq۰field۰val) -∗
        structeq۰footprint footprint
      ).
  Lemma structeq۰footprintｰlookup' {footprint} l blk i :
    footprint !! l = Some blk →
    i < length blk.(structeq۰block۰fields) →
    structeq۰footprint footprint ⊢
      ∃ fld,
      ⌜blk.(structeq۰block۰fields) !! i = Some fld⌝ ∗
      (l +ₗ i) ↦{fld.(structeq۰field۰dfrac)} fld.(structeq۰field۰val) ∗
      ⌜val۰traversable footprint fld.(structeq۰field۰val)⌝ ∗
      ( (l +ₗ i) ↦{fld.(structeq۰field۰dfrac)} fld.(structeq۰field۰val) -∗
        structeq۰footprint footprint
      ).

  Lemma structeq۰footprintｰwpｰtag {footprint} l blk :
    footprint !! l = Some blk →
    {{{
      structeq۰footprint footprint
    }}}
      GetTag #l
    {{{
      RET #(encode_tag blk.(structeq۰block۰tag));
      structeq۰footprint footprint
    }}}.
  Lemma structeq۰footprintｰwpｰsize {footprint} l blk :
    footprint !! l = Some blk →
    {{{
      structeq۰footprint footprint
    }}}
      GetSize #l
    {{{
      RET #(length blk.(structeq۰block۰fields));
      structeq۰footprint footprint
    }}}.

  Lemma structeq۰footprintｰwpｰload {footprint} l blk (i : nat) fld :
    footprint !! l = Some blk →
    blk.(structeq۰block۰fields) !! i = Some fld →
    {{{
      structeq۰footprint footprint
    }}}
      Load #l #i
    {{{
      RET fld.(structeq۰field۰val);
      ⌜val۰traversable footprint fld.(structeq۰field۰val)⌝ ∗
      structeq۰footprint footprint
    }}}.
  Lemma structeq۰footprintｰwpｰload' {footprint} l blk i :
    footprint !! l = Some blk →
    i < length blk.(structeq۰block۰fields) →
    {{{
      structeq۰footprint footprint
    }}}
      Load #l #i
    {{{
      fld
    , RET fld.(structeq۰field۰val);
      ⌜blk.(structeq۰block۰fields) !! i = Some fld⌝ ∗
      ⌜val۰traversable footprint fld.(structeq۰field۰val)⌝ ∗
      structeq۰footprint footprint
    }}}.
End zoo۰G.

Fixpoint val۰reachable footprint src path dst :=
  match path with
  | [] ⇒
      src = dst
  | i :: path ⇒
      match src with
      | ValLoc l ⇒
          match footprint !! l with
          | None ⇒
              False
          | Some blk ⇒
              match blk.(structeq۰block۰fields) !! i with
              | None ⇒
                  False
              | Some fld ⇒
                  val۰reachable footprint fld.(structeq۰field۰val) path dst
              end
          end
      | ValBlock _ _ vs ⇒
          match vs !! i with
          | None ⇒
              False
          | Some src ⇒
              val۰reachable footprint src path dst
          end
      | _ ⇒
          False
      end
  end.
#[global] Arguments val۰reachable _ !_ !_ / _ : assert.

#[global] Instance val۰reachableｰdec footprint src path dst :
  Decision (val۰reachable footprint src path dst).

Definition lowval۰compatible footprint lv1 lv2 :=
  match lv1 with
  | LowvalLit lit1 ⇒
      match lit1 with
      | LowlitLoc l1 ⇒
          match lv2 with
          | LowvalLoc l2 ⇒
              let blk1 := footprint !!! l1 in
              let blk2 := footprint !!! l2 in
              blk1.(structeq۰block۰tag) ≟ blk2.(structeq۰block۰tag) &&
              length blk1.(structeq۰block۰fields) ≟ length blk2.(structeq۰block۰fields)
          | LowvalBlock _ tag2 vs2 _ ⇒
              let blk1 := footprint !!! l1 in
              blk1.(structeq۰block۰tag) ≟ tag2 &&
              length blk1.(structeq۰block۰fields) ≟ length vs2
          | _ ⇒
              false
          end
      | _ ⇒
          bool_decide (lv2 = LowvalLit lit1)
      end
  | LowvalRecs ⇒
      bool_decide (lv2 = LowvalRecs)
  | LowvalBlock _ tag1 vs1 _ ⇒
      match lv2 with
      | LowvalLoc l2 ⇒
          let blk2 := footprint !!! l2 in
          tag1 ≟ blk2.(structeq۰block۰tag) &&
          length vs1 ≟ length blk2.(structeq۰block۰fields)
      | LowvalBlock _ tag2 vs2 _ ⇒
          tag1 ≟ tag2 &&
          length vs1 ≟ length vs2
      | _ ⇒
          false
      end
  end.
#[global] Arguments lowval۰compatible _ !_ !_ / : assert.

Definition val۰compatible footprint v1 v2 :=
  lowval۰compatible footprint (val۰to_low v1) (val۰to_low v2).

Definition val۰structeq footprint v1 v2 :=
  ∀ path v1' v2',
  val۰reachable footprint v1 path v1' →
  val۰reachable footprint v2 path v2' →
  val۰compatible footprint v1' v2' = true.

Definition val۰structneq footprint v1 v2 :=
  ∃ path v1' v2',
  val۰reachable footprint v1 path v1' ∧
  val۰reachable footprint v2 path v2' ∧
  val۰compatible footprint v1' v2' = false.

Lemma valｰimmediateｰstructeq footprint v1 v2 :
  val۰immediate v1 →
  val۰immediate v2 →
  v1 ≈ v2 →
  val۰structeq footprint v1 v2.
Lemma valｰimmediateｰstructneq footprint v1 v2 :
  val۰immediate v1 →
  val۰immediate v2 →
  v1 ≉ v2 →
  val۰structneq footprint v1 v2.

Lemma val۰structeqｰrefl footprint v :
  val۰immediate v →
  val۰structeq footprint v v.
Lemma val۰structeqｰrefl' footprint v1 v2 :
  v1 = v2 →
  val۰immediate v1 →
  val۰structeq footprint v1 v2.

Section zoo۰G.
  Context `{zoo۰G : !ZooG Σ}.

  #[local] Lemma structeqｰspecｰaux :
    ⊢ (
      ∀ v1 v2 footprint,
      {{{
        ⌜val۰traversable footprint v1⌝ ∗
        ⌜val۰traversable footprint v2⌝ ∗
        structeq۰footprint footprint
      }}}
        v1 = v2
      {{{
        b
      , RET #b;
        ⌜(if b then val۰structeq else val۰structneq) footprint v1 v2⌝ ∗
        structeq۰footprint footprint
      }}}
    ) ∧ (
      ∀ l1 blk1 l2 blk2 footprint i,
      {{{
        ⌜0 ≤ i ≤ length blk1.(structeq۰block۰fields)⌝%Z ∗
        ⌜footprint !! l1 = Some blk1⌝ ∗
        ⌜footprint !! l2 = Some blk2⌝ ∗
        ⌜blk1.(structeq۰block۰tag) = blk2.(structeq۰block۰tag)⌝ ∗
        ⌜length blk1.(structeq۰block۰fields) = length blk2.(structeq۰block۰fields)⌝ ∗
        structeq۰footprint footprint ∗
        ⌜ ∀ j fld1 fld2,
          blk1.(structeq۰block۰fields) !! j = Some fld1 →
          blk2.(structeq۰block۰fields) !! j = Some fld2 →
          ₊i ≤ j →
          val۰structeq footprint fld1.(structeq۰field۰val) fld2.(structeq۰field۰val)
        ⌝
      }}}
        structeq۰aux #l1 #l2 #i
      {{{
        b
      , RET #b;
        ⌜(if b then val۰structeq else val۰structneq) footprint #l1 #l2⌝ ∗
        structeq۰footprint footprint
      }}}
    ) ∧ (
      ∀ l1 blk1 gen2 tag2 vs2 footprint i,
      let v2 := ValBlock gen2 tag2 vs2 in
      {{{
        ⌜0 ≤ i ≤ length vs2⌝%Z ∗
        ⌜footprint !! l1 = Some blk1⌝ ∗
        ⌜blk1.(structeq۰block۰tag) = tag2⌝ ∗
        ⌜length blk1.(structeq۰block۰fields) = length vs2⌝ ∗
        ⌜0 < length vs2⌝ ∗
        ⌜val۰traversable footprint v2⌝ ∗
        structeq۰footprint footprint ∗
        ⌜ ∀ j fld1 v2,
          blk1.(structeq۰block۰fields) !! j = Some fld1 →
          vs2 !! j = Some v2 →
          ₊i ≤ j →
          val۰structeq footprint fld1.(structeq۰field۰val) v2
        ⌝
      }}}
        structeq۰aux #l1 v2 #i
      {{{
        b
      , RET #b;
        ⌜(if b then val۰structeq else val۰structneq) footprint #l1 v2⌝ ∗
        structeq۰footprint footprint
      }}}
    ) ∧ (
      ∀ gen1 tag1 vs1 l2 blk2 footprint i,
      let v1 := ValBlock gen1 tag1 vs1 in
      {{{
        ⌜0 ≤ i ≤ length vs1⌝%Z ∗
        ⌜footprint !! l2 = Some blk2⌝ ∗
        ⌜tag1 = blk2.(structeq۰block۰tag)⌝ ∗
        ⌜length vs1 = length blk2.(structeq۰block۰fields)⌝ ∗
        ⌜0 < length vs1⌝ ∗
        ⌜val۰traversable footprint v1⌝ ∗
        structeq۰footprint footprint ∗
        ⌜ ∀ j v1 fld2,
          vs1 !! j = Some v1 →
          blk2.(structeq۰block۰fields) !! j = Some fld2 →
          ₊i ≤ j →
          val۰structeq footprint v1 fld2.(structeq۰field۰val)
        ⌝
      }}}
        structeq۰aux v1 #l2 #i
      {{{
        b
      , RET #b;
        ⌜(if b then val۰structeq else val۰structneq) footprint v1 #l2⌝ ∗
        structeq۰footprint footprint
      }}}
    ) ∧ (
      ∀ gen1 tag1 vs1 gen2 tag2 vs2 footprint i,
      let v1 := ValBlock gen1 tag1 vs1 in
      let v2 := ValBlock gen2 tag2 vs2 in
      {{{
        ⌜0 ≤ i ≤ length vs1⌝%Z ∗
        ⌜tag1 = tag2⌝ ∗
        ⌜length vs1 = length vs2⌝ ∗
        ⌜0 < length vs1⌝ ∗
        ⌜val۰traversable footprint v1⌝ ∗
        ⌜val۰traversable footprint v2⌝ ∗
        structeq۰footprint footprint ∗
        ⌜ ∀ j v1 v2,
          vs1 !! j = Some v1 →
          vs2 !! j = Some v2 →
          ₊i ≤ j →
          val۰structeq footprint v1 v2
        ⌝
      }}}
        structeq۰aux v1 v2 #i
      {{{
        b
      , RET #b;
        ⌜(if b then val۰structeq else val۰structneq) footprint v1 v2⌝ ∗
        structeq۰footprint footprint
      }}}
    ).
  Lemma structeqｰspec {v1 v2} footprint :
    val۰traversable footprint v1 →
    val۰traversable footprint v2 →
    {{{
      structeq۰footprint footprint
    }}}
      v1 = v2
    {{{
      b
    , RET #b;
      ⌜(if b then val۰structeq else val۰structneq) footprint v1 v2⌝ ∗
      structeq۰footprint footprint
    }}}.
End zoo۰G.

#[global] Opaque structeq.


Fixpoint val۰abstract v :=
  match v with
  | ValBool _
  | ValInt _ ⇒
      True
  | ValBlock Nongenerative _ vs ⇒
      Forall' val۰abstract vs
  | _ ⇒
      False
  end.
#[global] Arguments val۰abstract !_ / : assert.

Lemma val۰abstractｰtraversable v :
  val۰abstract v →
  val۰traversable ∅ v.

Lemma val۰compatibleｰreflｰabstract footprint v1 v2 :
  val۰abstract v1 →
  val۰abstract v2 →
  v1 ≈ v2 →
  val۰compatible footprint v1 v2 = true.

Lemma valｰstructeqｰabstract₁ footprint v1 v2 :
  val۰abstract v1 →
  val۰abstract v2 →
  val۰structeq footprint v1 v2 →
  v1 ≈ v2.
Lemma valｰstructeqｰabstract₂ v1 v2 :
  val۰abstract v1 →
  val۰abstract v2 →
  v1 ≈ v2 →
  val۰structeq ∅ v1 v2.
Lemma valｰstructeqｰabstract v1 v2 :
  val۰abstract v1 →
  val۰abstract v2 →
  val۰structeq ∅ v1 v2 ↔
  v1 ≈ v2.

Lemma valｰstructneqｰabstract v1 v2 :
  val۰abstract v1 →
  val۰abstract v2 →
  val۰structneq ∅ v1 v2 →
  v1 ≉ v2.

Lemma structeqｰspecｰabstract `{zoo۰G : !ZooG Σ} {v1 v2} :
  val۰abstract v1 →
  val۰abstract v2 →
  {{{
    True
  }}}
    v1 = v2
  {{{
    b
  , RET #b;
    ⌜(if b then (≈) else (≉)) v1 v2⌝
  }}}.