From Undecidability Require Import SeparationLogic.MSL.
From Undecidability Require Import Shared.ListAutomation.
Import ListAutomationNotations.

Separation logic
Syntax
Semantics

Definition disjoint (h h' : heap) :=
   l p p', (l, p) h (l, p') h'.

Definition equiv (h h' : heap) :=
  h h' h' h.

Fixpoint sp_sat (s : stack) (h : heap) (P : sp_form) :=
  match P with
  | pointer E l, sp_eval s E = Some l h = [(l, (sp_eval s , sp_eval s ))]
  | equality sp_eval s = sp_eval s
  | bot False
  | imp sp_sat s h sp_sat s h
  | and sp_sat s h sp_sat s h
  | or sp_sat s h sp_sat s h
  | all P v, sp_sat (update_stack s v) h P
  | ex P v, sp_sat (update_stack s v) h P
  | emp h = nil
  | sand h1 h2, equiv h ( ) sp_sat s sp_sat s
  | simp h', disjoint h h' sp_sat s h' sp_sat s (h h')
  end.

Satisfiability problem

Definition SLSAT (P : sp_form) :=
   s h, functional h sp_sat s h P.